Resolution
Chosen clause
size
length
height
Max time of proof
Max size of clauses
notrace
trace
Support Clauses
p(x,y) p(y,x), -p(u,z) -p(z,u)
Usable Clauses
Proof
(1) [-p(u, z) -p(z, u)] Hyp (2) [-p(z, z)] Factor 1 u := z (3) [p(x, y) p(y, x)] Hyp (4) [p(y, y)] Factor 3 x := y (5) [] Res Bin 2, 4 z := y Proof duration (in seconds): 3.88622283936e-05
examples
|
syntax
|
info
|
home
|
download
Last Modified : 18-Dec-2019