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