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