Resolution
Type of resolution
nor
pos
neg
Max time of proof
Max length of clauses
Max height of clauses
Max size of clauses
notrace
trace
Clauses
p(x) p(a),-p(x)
Proof
(1) [p(x) p(a)] Hyp (2) [p(a)] Factor 1 x := a (3) [-p(x)] Hyp (4) [-p(v0)] Copy 3 x := v0 (5) [] Res Bin 2, 4 v0 := a Proof duration (in seconds): 2.50339508057e-05
examples
|
syntax
|
info
|
home
|
download
Last Modified : 02-Dec-2019