Model Elimination
Max time of proof
Max length of proof
Clauses
p,-p q,-q r,-r
Proof
1: p Hypothesis 2: q [p]^0 Expansion on literal 1 with hypothesis -p q 3: r [q]^0 [p]^0 Expansion on literal 1 with hypothesis -q r 4: [r]^0 [q]^0 [p]^0 Expansion on literal 1 with hypothesis -r 5: [q]^0 [p]^0 Remove 6: [p]^0 Remove 7: F Remove Proof duration (in seconds): 4.98294830322e-05
examples
|
syntax
|
info
|
home
|
download
Last Modified : 02-Dec-2019