twee-2.3: tests/minus.p
cnf(plus_zero, axiom,
'0' + X = X).
cnf(plus_zero, axiom,
X + '0' = X).
cnf(minus_minus, axiom,
- -X = X).
cnf(minus_plus, axiom,
-(X + Y) = -X + -Y).
cnf(goal, conjecture,
-'0' = '0').
cnf(plus_zero, axiom,
'0' + X = X).
cnf(plus_zero, axiom,
X + '0' = X).
cnf(minus_minus, axiom,
- -X = X).
cnf(minus_plus, axiom,
-(X + Y) = -X + -Y).
cnf(goal, conjecture,
-'0' = '0').