%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : HWV003-2 : TPTP v9.3.1. Released v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n003.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:37:36 PM UTC 2026
% Result : Unsatisfiable 241.79s 35.33s
% Output : Proof 241.79s
% Verified :
% SZS Type : Refutation
% Derivation depth : 121
% Number of leaves : 37
% Syntax : Number of formulae : 1173 (1169 unt; 0 def)
% Number of atoms : 1177 (1176 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 14 ( 10 ~; 4 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 23 ( 23 usr; 18 con; 0-4 aty)
% Number of variables : 762 ( 56 sgn 80 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f35,negated_conjecture,
( carry != carry_def
| sum != sum_def ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_circuit) ).
fof(f35_nnf,plain,
( carry != carry_def
| sum != sum_def ),
inference(nnf_transformation,[status(thm)],[f35]) ).
fof(f35_sk,plain,
( carry != carry_def
| sum != sum_def ),
inference(skolemisation,[status(esa)],[f35_nnf]) ).
cnf(c35,plain,
( carry != carry_def
| sum != sum_def ),
inference(cnf_transformation,[status(esa)],[f35_sk]) ).
cnf(t30,plain,
ifeq(sum,sum_def,ifeq(carry,carry_def,false,true),true) = true,
inference(equality_encoding,[status(esa)],[c35]) ).
cnf(t243,plain,
ifeq(sum,sum_def,ifeq(carry,carry_def,false,true),true) = true,
inference(orient,[status(thm)],[t30]) ).
cnf(f23,axiom,
xor(X,xor(Y,Z)) = xor(xor(X,Y),Z),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',xor_associative) ).
fof(f23_nnf,plain,
! [X,Y,Z] : xor(X,xor(Y,Z)) = xor(xor(X,Y),Z),
inference(nnf_transformation,[status(thm)],[f23]) ).
fof(f23_sk,plain,
! [X,Y,Z] : xor(X,xor(Y,Z)) = xor(xor(X,Y),Z),
inference(skolemisation,[status(esa)],[f23_nnf]) ).
cnf(c23,plain,
xor(X0,xor(X1,X2)) = xor(xor(X0,X1),X2),
inference(cnf_transformation,[status(esa)],[f23_sk]) ).
cnf(t32,plain,
xor(xor(X1,X2),X3) = xor(X1,xor(X2,X3)),
inference(equality_encoding,[status(esa)],[c23]) ).
cnf(t238,plain,
xor(xor(X1,X2),X3) = xor(X1,xor(X2,X3)),
inference(orient,[status(thm)],[t32]) ).
cnf(f21,axiom,
or(and(not(X),Y),and(X,not(Y))) = xor(X,Y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',xor_definition) ).
fof(f21_nnf,plain,
! [X,Y] : or(and(not(X),Y),and(X,not(Y))) = xor(X,Y),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [X,Y] : or(and(not(X),Y),and(X,not(Y))) = xor(X,Y),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
or(and(not(X0),X1),and(X0,not(X1))) = xor(X0,X1),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(t35,plain,
or(and(not(X1),X2),and(X1,not(X2))) = xor(X1,X2),
inference(equality_encoding,[status(esa)],[c21]) ).
cnf(f0,axiom,
or(X,Y) = or(Y,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_commutative) ).
fof(f0_nnf,plain,
! [X,Y] : or(X,Y) = or(Y,X),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,Y] : or(X,Y) = or(Y,X),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
or(X0,X1) = or(X1,X0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t23,plain,
or(X1,X2) = or(X2,X1),
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t164,plain,
or(X1,X2) = or(X2,X1),
inference(orient,[status(thm)],[t23]) ).
cnf(t66507,plain,
or(and(X1,not(X2)),and(not(X1),X2)) = xor(X1,X2),
inference(step,[status(thm)],[t35,t164]) ).
cnf(t192,plain,
or(and(X1,not(X2)),and(not(X1),X2)) = xor(X1,X2),
inference(orient,[status(thm)],[t66507]) ).
cnf(f9,axiom,
and(X,not(X)) = ll0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_complement) ).
fof(f9_nnf,plain,
! [X] : and(X,not(X)) = ll0,
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [X] : and(X,not(X)) = ll0,
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c9,plain,
and(X0,not(X0)) = ll0,
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
cnf(t9,plain,
and(X1,not(X1)) = ll0,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t54,plain,
and(X1,not(X1)) = ll0,
inference(orient,[status(thm)],[t9]) ).
cnf(t212,plain,
xor(X1,not(not(X1))) = or(and(X1,not(not(not(X1)))),ll0),
inference(cp,[status(thm)],[t192,t54]) ).
cnf(f12,axiom,
not(not(X)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_involution) ).
fof(f12_nnf,plain,
! [X] : not(not(X)) = X,
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [X] : not(not(X)) = X,
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
not(not(X0)) = X0,
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(t5,plain,
not(not(X1)) = X1,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t40,plain,
not(not(X1)) = X1,
inference(orient,[status(thm)],[t5]) ).
cnf(t66512,plain,
xor(X1,X1) = or(and(X1,not(not(not(X1)))),ll0),
inference(step,[status(thm)],[t212,t40]) ).
cnf(f4,axiom,
or(X,ll0) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_identity) ).
fof(f4_nnf,plain,
! [X] : or(X,ll0) = X,
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X] : or(X,ll0) = X,
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
or(X0,ll0) = X0,
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t7,plain,
or(X1,ll0) = X1,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t43,plain,
or(X1,ll0) = X1,
inference(orient,[status(thm)],[t7]) ).
cnf(t66513,plain,
xor(X1,X1) = and(X1,not(not(not(X1)))),
inference(step,[status(thm)],[t66512,t43]) ).
cnf(t66514,plain,
xor(X1,X1) = and(X1,not(X1)),
inference(step,[status(thm)],[t66513,t40]) ).
cnf(t66515,plain,
xor(X1,X1) = ll0,
inference(step,[status(thm)],[t66514,t54]) ).
cnf(t244,plain,
xor(X1,X1) = ll0,
inference(orient,[status(thm)],[t66515]) ).
cnf(t246,plain,
xor(X1,xor(X1,X2)) = xor(ll0,X2),
inference(cp,[status(thm)],[t238,t244]) ).
cnf(t1065,plain,
xor(X1,xor(X1,X2)) = xor(ll0,X2),
inference(orient,[status(thm)],[t246]) ).
cnf(f20,axiom,
not(and(X,Y)) = or(not(X),not(Y)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_demorgan) ).
fof(f20_nnf,plain,
! [X,Y] : not(and(X,Y)) = or(not(X),not(Y)),
inference(nnf_transformation,[status(thm)],[f20]) ).
fof(f20_sk,plain,
! [X,Y] : not(and(X,Y)) = or(not(X),not(Y)),
inference(skolemisation,[status(esa)],[f20_nnf]) ).
cnf(c20,plain,
not(and(X0,X1)) = or(not(X0),not(X1)),
inference(cnf_transformation,[status(esa)],[f20_sk]) ).
cnf(t28,plain,
or(not(X1),not(X2)) = not(and(X1,X2)),
inference(equality_encoding,[status(esa)],[c20]) ).
cnf(t87,plain,
or(not(X1),not(X2)) = not(and(X1,X2)),
inference(orient,[status(thm)],[t28]) ).
cnf(f14,axiom,
not(ll1) = ll0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ll1_inverse) ).
fof(f14_nnf,plain,
not(ll1) = ll0,
inference(nnf_transformation,[status(thm)],[f14]) ).
cnf(c14,plain,
not(ll1) = ll0,
inference(cnf_transformation,[status(esa)],[f14_nnf]) ).
cnf(t1,plain,
not(ll1) = ll0,
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(t155,plain,
not(ll1) = ll0,
inference(orient,[status(thm)],[t1]) ).
cnf(t156,plain,
not(and(ll1,X1)) = or(ll0,not(X1)),
inference(cp,[status(thm)],[t87,t155]) ).
cnf(t198,plain,
xor(X1,ll1) = or(and(X1,ll0),and(not(X1),ll1)),
inference(cp,[status(thm)],[t192,t155]) ).
cnf(f16,axiom,
and(X,ll0) = ll0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_boundedness) ).
fof(f16_nnf,plain,
! [X] : and(X,ll0) = ll0,
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
! [X] : and(X,ll0) = ll0,
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
and(X0,ll0) = ll0,
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(t3,plain,
and(X1,ll0) = ll0,
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(t67,plain,
and(X1,ll0) = ll0,
inference(orient,[status(thm)],[t3]) ).
cnf(t66526,plain,
xor(X1,ll1) = or(ll0,and(not(X1),ll1)),
inference(step,[status(thm)],[t198,t67]) ).
cnf(f5,axiom,
and(X,ll1) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_identity) ).
fof(f5_nnf,plain,
! [X] : and(X,ll1) = X,
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X] : and(X,ll1) = X,
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
and(X0,ll1) = X0,
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t4,plain,
and(X1,ll1) = X1,
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t39,plain,
and(X1,ll1) = X1,
inference(orient,[status(thm)],[t4]) ).
cnf(t66527,plain,
xor(X1,ll1) = or(ll0,not(X1)),
inference(step,[status(thm)],[t66526,t39]) ).
cnf(t297,plain,
or(ll0,not(X1)) = xor(X1,ll1),
inference(orient,[status(thm)],[t66527]) ).
cnf(t66528,plain,
not(and(ll1,X1)) = xor(X1,ll1),
inference(step,[status(thm)],[t156,t297]) ).
cnf(t357,plain,
not(and(ll1,X1)) = xor(X1,ll1),
inference(orient,[status(thm)],[t66528]) ).
cnf(f1,axiom,
and(X,Y) = and(Y,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_commutative) ).
fof(f1_nnf,plain,
! [X,Y] : and(X,Y) = and(Y,X),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,Y] : and(X,Y) = and(Y,X),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
and(X0,X1) = and(X1,X0),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t20,plain,
and(X1,X2) = and(X2,X1),
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t45,plain,
and(X1,X2) = and(X2,X1),
inference(orient,[status(thm)],[t20]) ).
cnf(t358,plain,
xor(X1,ll1) = not(and(X1,ll1)),
inference(cp,[status(thm)],[t357,t45]) ).
cnf(t66529,plain,
xor(X1,ll1) = not(X1),
inference(step,[status(thm)],[t358,t39]) ).
cnf(t370,plain,
xor(X1,ll1) = not(X1),
inference(orient,[status(thm)],[t66529]) ).
cnf(t375,plain,
not(xor(X1,X2)) = xor(X1,xor(X2,ll1)),
inference(cp,[status(thm)],[t370,t238]) ).
cnf(t66614,plain,
not(xor(X1,X2)) = xor(X1,not(X2)),
inference(step,[status(thm)],[t375,t370]) ).
cnf(t784,plain,
not(xor(X1,X2)) = xor(X1,not(X2)),
inference(orient,[status(thm)],[t66614]) ).
cnf(f19,axiom,
not(or(X,Y)) = and(not(X),not(Y)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_demorgan) ).
fof(f19_nnf,plain,
! [X,Y] : not(or(X,Y)) = and(not(X),not(Y)),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [X,Y] : not(or(X,Y)) = and(not(X),not(Y)),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c19,plain,
not(or(X0,X1)) = and(not(X0),not(X1)),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(t27,plain,
and(not(X1),not(X2)) = not(or(X1,X2)),
inference(equality_encoding,[status(esa)],[c19]) ).
cnf(t69,plain,
and(not(X1),not(X2)) = not(or(X1,X2)),
inference(orient,[status(thm)],[t27]) ).
cnf(t195,plain,
xor(not(X1),X2) = or(not(or(X1,X2)),and(not(not(X1)),X2)),
inference(cp,[status(thm)],[t192,t69]) ).
cnf(t68121,plain,
xor(not(X1),X2) = or(not(or(X1,X2)),and(X1,X2)),
inference(step,[status(thm)],[t195,t40]) ).
cnf(t68122,plain,
xor(not(X1),X2) = or(and(X1,X2),not(or(X1,X2))),
inference(step,[status(thm)],[t68121,t164]) ).
cnf(t25122,plain,
or(and(X1,X2),not(or(X1,X2))) = xor(not(X1),X2),
inference(orient,[status(thm)],[t68122]) ).
cnf(f26,negated_conjecture,
not(and(a,b)) = t1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1) ).
fof(f26_nnf,plain,
not(and(a,b)) = t1,
inference(nnf_transformation,[status(thm)],[f26]) ).
cnf(c26,plain,
not(and(a,b)) = t1,
inference(cnf_transformation,[status(esa)],[f26_nnf]) ).
cnf(t10,plain,
not(and(a,b)) = t1,
inference(equality_encoding,[status(esa)],[c26]) ).
cnf(t66500,plain,
not(and(b,a)) = t1,
inference(step,[status(thm)],[t10,t45]) ).
cnf(t92,plain,
not(and(b,a)) = t1,
inference(orient,[status(thm)],[t66500]) ).
cnf(t98,plain,
and(b,a) = not(t1),
inference(cp,[status(thm)],[t40,t92]) ).
cnf(t248,plain,
and(b,a) = not(t1),
inference(orient,[status(thm)],[t98]) ).
cnf(t25344,plain,
xor(not(b),a) = or(not(t1),not(or(b,a))),
inference(cp,[status(thm)],[t25122,t248]) ).
cnf(f22,axiom,
xor(X,Y) = xor(Y,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',xor_commutative) ).
fof(f22_nnf,plain,
! [X,Y] : xor(X,Y) = xor(Y,X),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [X,Y] : xor(X,Y) = xor(Y,X),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c22,plain,
xor(X0,X1) = xor(X1,X0),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(t25,plain,
xor(X1,X2) = xor(X2,X1),
inference(equality_encoding,[status(esa)],[c22]) ).
cnf(t237,plain,
xor(X1,X2) = xor(X2,X1),
inference(orient,[status(thm)],[t25]) ).
cnf(t68123,plain,
xor(a,not(b)) = or(not(t1),not(or(b,a))),
inference(step,[status(thm)],[t25344,t237]) ).
cnf(t240,plain,
xor(X1,xor(X2,X3)) = xor(xor(X2,X1),X3),
inference(cp,[status(thm)],[t238,t237]) ).
cnf(t66639,plain,
xor(X1,xor(X2,X3)) = xor(X2,xor(X1,X3)),
inference(step,[status(thm)],[t240,t238]) ).
cnf(t1033,plain,
xor(X1,xor(X2,X3)) = xor(X2,xor(X1,X3)),
inference(orient,[status(thm)],[t66639]) ).
cnf(t1034,plain,
xor(X1,xor(X2,ll1)) = xor(X2,not(X1)),
inference(cp,[status(thm)],[t1033,t370]) ).
cnf(t66640,plain,
xor(X1,not(X2)) = xor(X2,not(X1)),
inference(step,[status(thm)],[t1034,t370]) ).
cnf(t1035,plain,
xor(X1,not(X2)) = xor(X2,not(X1)),
inference(orient,[status(thm)],[t66640]) ).
cnf(t68124,plain,
xor(b,not(a)) = or(not(t1),not(or(b,a))),
inference(step,[status(thm)],[t68123,t1035]) ).
cnf(f2,axiom,
or(or(X,Y),Z) = or(X,or(Y,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_associative) ).
fof(f2_nnf,plain,
! [X,Y,Z] : or(or(X,Y),Z) = or(X,or(Y,Z)),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X,Y,Z] : or(or(X,Y),Z) = or(X,or(Y,Z)),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
or(or(X0,X1),X2) = or(X0,or(X1,X2)),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t31,plain,
or(or(X1,X2),X3) = or(X1,or(X2,X3)),
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t179,plain,
or(or(X1,X2),X3) = or(X1,or(X2,X3)),
inference(orient,[status(thm)],[t31]) ).
cnf(f17,axiom,
or(X,and(X,Y)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_absorption) ).
fof(f17_nnf,plain,
! [X,Y] : or(X,and(X,Y)) = X,
inference(nnf_transformation,[status(thm)],[f17]) ).
fof(f17_sk,plain,
! [X,Y] : or(X,and(X,Y)) = X,
inference(skolemisation,[status(esa)],[f17_nnf]) ).
cnf(c17,plain,
or(X0,and(X0,X1)) = X0,
inference(cnf_transformation,[status(esa)],[f17_sk]) ).
cnf(t24,plain,
or(X1,and(X1,X2)) = X1,
inference(equality_encoding,[status(esa)],[c17]) ).
cnf(t42,plain,
or(X1,and(X1,X2)) = X1,
inference(orient,[status(thm)],[t24]) ).
cnf(t186,plain,
or(X1,or(and(X1,X2),X3)) = or(X1,X3),
inference(cp,[status(thm)],[t179,t42]) ).
cnf(t4951,plain,
or(X1,or(and(X1,X2),X3)) = or(X1,X3),
inference(orient,[status(thm)],[t186]) ).
cnf(t4953,plain,
or(X1,and(not(X1),X2)) = or(X1,xor(X1,X2)),
inference(cp,[status(thm)],[t4951,t192]) ).
cnf(f7,axiom,
or(X,and(Y,Z)) = and(or(X,Y),or(X,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_distributive) ).
fof(f7_nnf,plain,
! [X,Y,Z] : or(X,and(Y,Z)) = and(or(X,Y),or(X,Z)),
inference(nnf_transformation,[status(thm)],[f7]) ).
fof(f7_sk,plain,
! [X,Y,Z] : or(X,and(Y,Z)) = and(or(X,Y),or(X,Z)),
inference(skolemisation,[status(esa)],[f7_nnf]) ).
cnf(c7,plain,
or(X0,and(X1,X2)) = and(or(X0,X1),or(X0,X2)),
inference(cnf_transformation,[status(esa)],[f7_sk]) ).
cnf(t33,plain,
and(or(X1,X2),or(X1,X3)) = or(X1,and(X2,X3)),
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t78,plain,
and(or(X1,X2),or(X1,X3)) = or(X1,and(X2,X3)),
inference(orient,[status(thm)],[t33]) ).
cnf(f8,axiom,
or(X,not(X)) = ll1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_complement) ).
fof(f8_nnf,plain,
! [X] : or(X,not(X)) = ll1,
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
! [X] : or(X,not(X)) = ll1,
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
or(X0,not(X0)) = ll1,
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(t19,plain,
or(X1,not(X1)) = ll1,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t167,plain,
or(X1,not(X1)) = ll1,
inference(orient,[status(thm)],[t19]) ).
cnf(t177,plain,
or(X1,and(not(X1),X2)) = and(ll1,or(X1,X2)),
inference(cp,[status(thm)],[t78,t167]) ).
cnf(t367,plain,
and(ll1,X1) = not(xor(X1,ll1)),
inference(cp,[status(thm)],[t40,t357]) ).
cnf(t66548,plain,
and(ll1,X1) = not(not(X1)),
inference(step,[status(thm)],[t367,t370]) ).
cnf(t66549,plain,
and(ll1,X1) = X1,
inference(step,[status(thm)],[t66548,t40]) ).
cnf(t437,plain,
and(ll1,X1) = X1,
inference(orient,[status(thm)],[t66549]) ).
cnf(t66838,plain,
or(X1,and(not(X1),X2)) = or(X1,X2),
inference(step,[status(thm)],[t177,t437]) ).
cnf(t2189,plain,
or(X1,and(not(X1),X2)) = or(X1,X2),
inference(orient,[status(thm)],[t66838]) ).
cnf(t67251,plain,
or(X1,X2) = or(X1,xor(X1,X2)),
inference(step,[status(thm)],[t4953,t2189]) ).
cnf(t5009,plain,
or(X1,xor(X1,X2)) = or(X1,X2),
inference(orient,[status(thm)],[t67251]) ).
cnf(f24,negated_conjecture,
xor(xor(a,b),cin) = sum_def,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sum_def) ).
fof(f24_nnf,plain,
xor(xor(a,b),cin) = sum_def,
inference(nnf_transformation,[status(thm)],[f24]) ).
cnf(c24,plain,
xor(xor(a,b),cin) = sum_def,
inference(cnf_transformation,[status(esa)],[f24_nnf]) ).
cnf(t26,plain,
xor(xor(a,b),cin) = sum_def,
inference(equality_encoding,[status(esa)],[c24]) ).
cnf(t66510,plain,
xor(a,xor(b,cin)) = sum_def,
inference(step,[status(thm)],[t26,t238]) ).
cnf(t66511,plain,
xor(a,xor(cin,b)) = sum_def,
inference(step,[status(thm)],[t66510,t237]) ).
cnf(t241,plain,
xor(a,xor(cin,b)) = sum_def,
inference(orient,[status(thm)],[t66511]) ).
cnf(t1016,plain,
xor(a,xor(cin,b)) = sum_def,
inference(rw,[status(thm)],[t241]) ).
cnf(t66659,plain,
xor(cin,xor(a,b)) = sum_def,
inference(step,[status(thm)],[t1016,t1033]) ).
cnf(t66660,plain,
xor(cin,xor(b,a)) = sum_def,
inference(step,[status(thm)],[t66659,t237]) ).
cnf(t1063,plain,
xor(cin,xor(b,a)) = sum_def,
inference(orient,[status(thm)],[t66660]) ).
cnf(t1066,plain,
xor(ll0,xor(b,a)) = xor(cin,sum_def),
inference(cp,[status(thm)],[t1065,t1063]) ).
cnf(t66841,plain,
xor(ll0,xor(b,a)) = xor(sum_def,cin),
inference(step,[status(thm)],[t1066,t237]) ).
cnf(t2219,plain,
xor(ll0,xor(b,a)) = xor(sum_def,cin),
inference(orient,[status(thm)],[t66841]) ).
cnf(t5017,plain,
or(ll0,xor(b,a)) = or(ll0,xor(sum_def,cin)),
inference(cp,[status(thm)],[t5009,t2219]) ).
cnf(t298,plain,
xor(not(X1),ll1) = or(ll0,X1),
inference(cp,[status(thm)],[t297,t40]) ).
cnf(t66546,plain,
not(not(X1)) = or(ll0,X1),
inference(step,[status(thm)],[t298,t370]) ).
cnf(t66547,plain,
X1 = or(ll0,X1),
inference(step,[status(thm)],[t66546,t40]) ).
cnf(t436,plain,
or(ll0,X1) = X1,
inference(orient,[status(thm)],[t66547]) ).
cnf(t67252,plain,
xor(b,a) = or(ll0,xor(sum_def,cin)),
inference(step,[status(thm)],[t5017,t436]) ).
cnf(t67253,plain,
xor(b,a) = xor(sum_def,cin),
inference(step,[status(thm)],[t67252,t436]) ).
cnf(t5037,plain,
xor(b,a) = xor(sum_def,cin),
inference(orient,[status(thm)],[t67253]) ).
cnf(t5040,plain,
xor(b,not(a)) = not(xor(sum_def,cin)),
inference(cp,[status(thm)],[t784,t5037]) ).
cnf(t67256,plain,
xor(b,not(a)) = xor(sum_def,not(cin)),
inference(step,[status(thm)],[t5040,t784]) ).
cnf(t5043,plain,
xor(b,not(a)) = xor(sum_def,not(cin)),
inference(orient,[status(thm)],[t67256]) ).
cnf(t68125,plain,
xor(sum_def,not(cin)) = or(not(t1),not(or(b,a))),
inference(step,[status(thm)],[t68124,t5043]) ).
cnf(t68126,plain,
xor(sum_def,not(cin)) = not(and(t1,or(b,a))),
inference(step,[status(thm)],[t68125,t87]) ).
cnf(t178,plain,
or(X1,and(X2,not(X1))) = and(or(X1,X2),ll1),
inference(cp,[status(thm)],[t78,t167]) ).
cnf(t66676,plain,
or(X1,and(X2,not(X1))) = or(X1,X2),
inference(step,[status(thm)],[t178,t39]) ).
cnf(t1140,plain,
or(X1,and(X2,not(X1))) = or(X1,X2),
inference(orient,[status(thm)],[t66676]) ).
cnf(t1188,plain,
or(not(X1),X2) = or(not(X1),and(X2,X1)),
inference(cp,[status(thm)],[t1140,t40]) ).
cnf(t3248,plain,
or(not(X1),and(X2,X1)) = or(not(X1),X2),
inference(orient,[status(thm)],[t1188]) ).
cnf(f6,axiom,
and(X,or(Y,Z)) = or(and(X,Y),and(X,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_distributive) ).
fof(f6_nnf,plain,
! [X,Y,Z] : and(X,or(Y,Z)) = or(and(X,Y),and(X,Z)),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [X,Y,Z] : and(X,or(Y,Z)) = or(and(X,Y),and(X,Z)),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
and(X0,or(X1,X2)) = or(and(X0,X1),and(X0,X2)),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(t34,plain,
or(and(X1,X2),and(X1,X3)) = and(X1,or(X2,X3)),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t57,plain,
or(and(X1,X2),and(X1,X3)) = and(X1,or(X2,X3)),
inference(orient,[status(thm)],[t34]) ).
cnf(t58,plain,
and(X1,or(not(X1),X2)) = or(ll0,and(X1,X2)),
inference(cp,[status(thm)],[t57,t54]) ).
cnf(t66775,plain,
and(X1,or(not(X1),X2)) = and(X1,X2),
inference(step,[status(thm)],[t58,t436]) ).
cnf(t1814,plain,
and(X1,or(not(X1),X2)) = and(X1,X2),
inference(orient,[status(thm)],[t66775]) ).
cnf(t1816,plain,
and(X1,not(X2)) = and(X1,not(and(X1,X2))),
inference(cp,[status(thm)],[t1814,t87]) ).
cnf(t3354,plain,
and(X1,not(and(X1,X2))) = and(X1,not(X2)),
inference(orient,[status(thm)],[t1816]) ).
cnf(t3393,plain,
and(b,not(a)) = and(b,not(not(t1))),
inference(cp,[status(thm)],[t3354,t248]) ).
cnf(t67041,plain,
and(b,not(a)) = and(b,t1),
inference(step,[status(thm)],[t3393,t40]) ).
cnf(t67042,plain,
and(b,not(a)) = and(t1,b),
inference(step,[status(thm)],[t67041,t45]) ).
cnf(f28,negated_conjecture,
not(and(b,t1)) = t3,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t3) ).
fof(f28_nnf,plain,
not(and(b,t1)) = t3,
inference(nnf_transformation,[status(thm)],[f28]) ).
cnf(c28,plain,
not(and(b,t1)) = t3,
inference(cnf_transformation,[status(esa)],[f28_nnf]) ).
cnf(t12,plain,
not(and(b,t1)) = t3,
inference(equality_encoding,[status(esa)],[c28]) ).
cnf(t66502,plain,
not(and(t1,b)) = t3,
inference(step,[status(thm)],[t12,t45]) ).
cnf(t106,plain,
not(and(t1,b)) = t3,
inference(orient,[status(thm)],[t66502]) ).
cnf(t112,plain,
and(t1,b) = not(t3),
inference(cp,[status(thm)],[t40,t106]) ).
cnf(t259,plain,
and(t1,b) = not(t3),
inference(orient,[status(thm)],[t112]) ).
cnf(t67043,plain,
and(b,not(a)) = not(t3),
inference(step,[status(thm)],[t67042,t259]) ).
cnf(t3484,plain,
and(b,not(a)) = not(t3),
inference(orient,[status(thm)],[t67043]) ).
cnf(t3485,plain,
or(not(not(a)),b) = or(not(not(a)),not(t3)),
inference(cp,[status(thm)],[t3248,t3484]) ).
cnf(t67047,plain,
or(b,not(not(a))) = or(not(not(a)),not(t3)),
inference(step,[status(thm)],[t3485,t164]) ).
cnf(t67048,plain,
or(b,a) = or(not(not(a)),not(t3)),
inference(step,[status(thm)],[t67047,t40]) ).
cnf(t67049,plain,
or(b,a) = not(and(not(a),t3)),
inference(step,[status(thm)],[t67048,t87]) ).
cnf(t88,plain,
not(and(not(X1),X2)) = or(X1,not(X2)),
inference(cp,[status(thm)],[t87,t40]) ).
cnf(t689,plain,
not(and(not(X1),X2)) = or(X1,not(X2)),
inference(orient,[status(thm)],[t88]) ).
cnf(t67050,plain,
or(b,a) = or(a,not(t3)),
inference(step,[status(thm)],[t67049,t689]) ).
cnf(t89,plain,
not(and(X1,not(X2))) = or(not(X1),X2),
inference(cp,[status(thm)],[t87,t40]) ).
cnf(t708,plain,
not(and(X1,not(X2))) = or(not(X1),X2),
inference(orient,[status(thm)],[t89]) ).
cnf(f3,axiom,
and(and(X,Y),Z) = and(X,and(Y,Z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_associative) ).
fof(f3_nnf,plain,
! [X,Y,Z] : and(and(X,Y),Z) = and(X,and(Y,Z)),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X,Y,Z] : and(and(X,Y),Z) = and(X,and(Y,Z)),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
and(and(X0,X1),X2) = and(X0,and(X1,X2)),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t29,plain,
and(and(X1,X2),X3) = and(X1,and(X2,X3)),
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t46,plain,
and(and(X1,X2),X3) = and(X1,and(X2,X3)),
inference(orient,[status(thm)],[t29]) ).
cnf(t262,plain,
and(t1,and(b,X1)) = and(not(t3),X1),
inference(cp,[status(thm)],[t46,t259]) ).
cnf(t1347,plain,
and(t1,and(b,X1)) = and(not(t3),X1),
inference(orient,[status(thm)],[t262]) ).
cnf(t1349,plain,
and(not(t3),a) = and(t1,not(t1)),
inference(cp,[status(thm)],[t1347,t248]) ).
cnf(t66711,plain,
and(a,not(t3)) = and(t1,not(t1)),
inference(step,[status(thm)],[t1349,t45]) ).
cnf(t66712,plain,
and(a,not(t3)) = ll0,
inference(step,[status(thm)],[t66711,t54]) ).
cnf(t1360,plain,
and(a,not(t3)) = ll0,
inference(orient,[status(thm)],[t66712]) ).
cnf(t1364,plain,
xor(a,t3) = or(ll0,and(not(a),t3)),
inference(cp,[status(thm)],[t192,t1360]) ).
cnf(t66720,plain,
xor(t3,a) = or(ll0,and(not(a),t3)),
inference(step,[status(thm)],[t1364,t237]) ).
cnf(t66721,plain,
xor(t3,a) = and(not(a),t3),
inference(step,[status(thm)],[t66720,t436]) ).
cnf(t66722,plain,
xor(t3,a) = and(t3,not(a)),
inference(step,[status(thm)],[t66721,t45]) ).
cnf(t1396,plain,
and(t3,not(a)) = xor(t3,a),
inference(orient,[status(thm)],[t66722]) ).
cnf(t1403,plain,
or(not(t3),a) = not(xor(t3,a)),
inference(cp,[status(thm)],[t708,t1396]) ).
cnf(t67008,plain,
or(a,not(t3)) = not(xor(t3,a)),
inference(step,[status(thm)],[t1403,t164]) ).
cnf(t67009,plain,
or(a,not(t3)) = xor(t3,not(a)),
inference(step,[status(thm)],[t67008,t784]) ).
cnf(f29,negated_conjecture,
not(and(t2,t3)) = t4,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4) ).
fof(f29_nnf,plain,
not(and(t2,t3)) = t4,
inference(nnf_transformation,[status(thm)],[f29]) ).
cnf(c29,plain,
not(and(t2,t3)) = t4,
inference(cnf_transformation,[status(esa)],[f29_nnf]) ).
cnf(t14,plain,
not(and(t2,t3)) = t4,
inference(equality_encoding,[status(esa)],[c29]) ).
cnf(t66506,plain,
not(and(t3,t2)) = t4,
inference(step,[status(thm)],[t14,t45]) ).
cnf(t148,plain,
not(and(t3,t2)) = t4,
inference(orient,[status(thm)],[t66506]) ).
cnf(t154,plain,
and(t3,t2) = not(t4),
inference(cp,[status(thm)],[t40,t148]) ).
cnf(t289,plain,
and(t3,t2) = not(t4),
inference(orient,[status(thm)],[t154]) ).
cnf(t292,plain,
and(t3,and(t2,X1)) = and(not(t4),X1),
inference(cp,[status(thm)],[t46,t289]) ).
cnf(t1642,plain,
and(t3,and(t2,X1)) = and(not(t4),X1),
inference(orient,[status(thm)],[t292]) ).
cnf(t73,plain,
not(or(X1,not(X2))) = and(not(X1),X2),
inference(cp,[status(thm)],[t69,t40]) ).
cnf(t573,plain,
not(or(X1,not(X2))) = and(not(X1),X2),
inference(orient,[status(thm)],[t73]) ).
cnf(f10,axiom,
or(X,X) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_idempotent) ).
fof(f10_nnf,plain,
! [X] : or(X,X) = X,
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [X] : or(X,X) = X,
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c10,plain,
or(X0,X0) = X0,
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
cnf(t6,plain,
or(X1,X1) = X1,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t41,plain,
or(X1,X1) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t80,plain,
or(X1,and(X2,X1)) = and(or(X1,X2),X1),
inference(cp,[status(thm)],[t78,t41]) ).
cnf(t66618,plain,
or(X1,and(X2,X1)) = and(X1,or(X1,X2)),
inference(step,[status(thm)],[t80,t45]) ).
cnf(f18,axiom,
and(X,or(X,Y)) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_absorption) ).
fof(f18_nnf,plain,
! [X,Y] : and(X,or(X,Y)) = X,
inference(nnf_transformation,[status(thm)],[f18]) ).
fof(f18_sk,plain,
! [X,Y] : and(X,or(X,Y)) = X,
inference(skolemisation,[status(esa)],[f18_nnf]) ).
cnf(c18,plain,
and(X0,or(X0,X1)) = X0,
inference(cnf_transformation,[status(esa)],[f18_sk]) ).
cnf(t21,plain,
and(X1,or(X1,X2)) = X1,
inference(equality_encoding,[status(esa)],[c18]) ).
cnf(t38,plain,
and(X1,or(X1,X2)) = X1,
inference(orient,[status(thm)],[t21]) ).
cnf(t66619,plain,
or(X1,and(X2,X1)) = X1,
inference(step,[status(thm)],[t66618,t38]) ).
cnf(t834,plain,
or(X1,and(X2,X1)) = X1,
inference(orient,[status(thm)],[t66619]) ).
cnf(f27,negated_conjecture,
not(and(a,t1)) = t2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2) ).
fof(f27_nnf,plain,
not(and(a,t1)) = t2,
inference(nnf_transformation,[status(thm)],[f27]) ).
cnf(c27,plain,
not(and(a,t1)) = t2,
inference(cnf_transformation,[status(esa)],[f27_nnf]) ).
cnf(t11,plain,
not(and(a,t1)) = t2,
inference(equality_encoding,[status(esa)],[c27]) ).
cnf(t66501,plain,
not(and(t1,a)) = t2,
inference(step,[status(thm)],[t11,t45]) ).
cnf(t99,plain,
not(and(t1,a)) = t2,
inference(orient,[status(thm)],[t66501]) ).
cnf(t105,plain,
and(t1,a) = not(t2),
inference(cp,[status(thm)],[t40,t99]) ).
cnf(t254,plain,
and(t1,a) = not(t2),
inference(orient,[status(thm)],[t105]) ).
cnf(t846,plain,
a = or(a,not(t2)),
inference(cp,[status(thm)],[t834,t254]) ).
cnf(t890,plain,
or(a,not(t2)) = a,
inference(orient,[status(thm)],[t846]) ).
cnf(t895,plain,
and(not(a),t2) = not(a),
inference(cp,[status(thm)],[t573,t890]) ).
cnf(t66633,plain,
and(t2,not(a)) = not(a),
inference(step,[status(thm)],[t895,t45]) ).
cnf(t973,plain,
and(t2,not(a)) = not(a),
inference(orient,[status(thm)],[t66633]) ).
cnf(t1644,plain,
and(not(t4),not(a)) = and(t3,not(a)),
inference(cp,[status(thm)],[t1642,t973]) ).
cnf(t66764,plain,
not(or(t4,a)) = and(t3,not(a)),
inference(step,[status(thm)],[t1644,t69]) ).
cnf(t66765,plain,
not(or(t4,a)) = xor(t3,a),
inference(step,[status(thm)],[t66764,t1396]) ).
cnf(t1682,plain,
not(or(t4,a)) = xor(t3,a),
inference(orient,[status(thm)],[t66765]) ).
cnf(t1691,plain,
or(t4,a) = not(xor(t3,a)),
inference(cp,[status(thm)],[t40,t1682]) ).
cnf(t66855,plain,
or(t4,a) = xor(t3,not(a)),
inference(step,[status(thm)],[t1691,t784]) ).
cnf(t2323,plain,
xor(t3,not(a)) = or(t4,a),
inference(orient,[status(thm)],[t66855]) ).
cnf(t62,plain,
and(X1,or(X2,not(X1))) = or(and(X1,X2),ll0),
inference(cp,[status(thm)],[t57,t54]) ).
cnf(t66671,plain,
and(X1,or(X2,not(X1))) = and(X1,X2),
inference(step,[status(thm)],[t62,t43]) ).
cnf(t1104,plain,
and(X1,or(X2,not(X1))) = and(X1,X2),
inference(orient,[status(thm)],[t66671]) ).
cnf(t1112,plain,
and(X1,not(X2)) = and(X1,not(and(X2,X1))),
inference(cp,[status(thm)],[t1104,t87]) ).
cnf(t2445,plain,
and(X1,not(and(X2,X1))) = and(X1,not(X2)),
inference(orient,[status(thm)],[t1112]) ).
cnf(t2473,plain,
and(a,not(t1)) = and(a,not(not(t2))),
inference(cp,[status(thm)],[t2445,t254]) ).
cnf(f11,axiom,
and(X,X) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',and_idempotent) ).
fof(f11_nnf,plain,
! [X] : and(X,X) = X,
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [X] : and(X,X) = X,
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c11,plain,
and(X0,X0) = X0,
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
cnf(t2,plain,
and(X1,X1) = X1,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t37,plain,
and(X1,X1) = X1,
inference(orient,[status(thm)],[t2]) ).
cnf(t61,plain,
and(X1,or(X2,X1)) = or(and(X1,X2),X1),
inference(cp,[status(thm)],[t57,t37]) ).
cnf(t66616,plain,
and(X1,or(X2,X1)) = or(X1,and(X1,X2)),
inference(step,[status(thm)],[t61,t164]) ).
cnf(t66617,plain,
and(X1,or(X2,X1)) = X1,
inference(step,[status(thm)],[t66616,t42]) ).
cnf(t825,plain,
and(X1,or(X2,X1)) = X1,
inference(orient,[status(thm)],[t66617]) ).
cnf(t848,plain,
a = or(a,not(t1)),
inference(cp,[status(thm)],[t834,t248]) ).
cnf(t902,plain,
or(a,not(t1)) = a,
inference(orient,[status(thm)],[t848]) ).
cnf(t903,plain,
not(t1) = and(not(t1),a),
inference(cp,[status(thm)],[t825,t902]) ).
cnf(t66636,plain,
not(t1) = and(a,not(t1)),
inference(step,[status(thm)],[t903,t45]) ).
cnf(t988,plain,
and(a,not(t1)) = not(t1),
inference(orient,[status(thm)],[t66636]) ).
cnf(t66882,plain,
not(t1) = and(a,not(not(t2))),
inference(step,[status(thm)],[t2473,t988]) ).
cnf(t66883,plain,
not(t1) = and(a,t2),
inference(step,[status(thm)],[t66882,t40]) ).
cnf(t66884,plain,
not(t1) = and(t2,a),
inference(step,[status(thm)],[t66883,t45]) ).
cnf(t2529,plain,
and(t2,a) = not(t1),
inference(orient,[status(thm)],[t66884]) ).
cnf(t2530,plain,
and(not(t4),a) = and(t3,not(t1)),
inference(cp,[status(thm)],[t1642,t2529]) ).
cnf(t66916,plain,
and(a,not(t4)) = and(t3,not(t1)),
inference(step,[status(thm)],[t2530,t45]) ).
cnf(t263,plain,
t1 = or(t1,not(t3)),
inference(cp,[status(thm)],[t42,t259]) ).
cnf(t329,plain,
or(t1,not(t3)) = t1,
inference(orient,[status(thm)],[t263]) ).
cnf(t581,plain,
and(not(t1),t3) = not(t1),
inference(cp,[status(thm)],[t573,t329]) ).
cnf(t66590,plain,
and(t3,not(t1)) = not(t1),
inference(step,[status(thm)],[t581,t45]) ).
cnf(t677,plain,
and(t3,not(t1)) = not(t1),
inference(orient,[status(thm)],[t66590]) ).
cnf(t66917,plain,
and(a,not(t4)) = not(t1),
inference(step,[status(thm)],[t66916,t677]) ).
cnf(t2626,plain,
and(a,not(t4)) = not(t1),
inference(orient,[status(thm)],[t66917]) ).
cnf(t3266,plain,
or(not(not(t4)),a) = or(not(not(t4)),not(t1)),
inference(cp,[status(thm)],[t3248,t2626]) ).
cnf(t66999,plain,
or(a,not(not(t4))) = or(not(not(t4)),not(t1)),
inference(step,[status(thm)],[t3266,t164]) ).
cnf(t67000,plain,
or(a,t4) = or(not(not(t4)),not(t1)),
inference(step,[status(thm)],[t66999,t40]) ).
cnf(t67001,plain,
or(t4,a) = or(not(not(t4)),not(t1)),
inference(step,[status(thm)],[t67000,t164]) ).
cnf(t67002,plain,
or(t4,a) = not(and(not(t4),t1)),
inference(step,[status(thm)],[t67001,t87]) ).
cnf(t67003,plain,
or(t4,a) = or(t4,not(t1)),
inference(step,[status(thm)],[t67002,t689]) ).
cnf(t293,plain,
t3 = or(t3,not(t4)),
inference(cp,[status(thm)],[t42,t289]) ).
cnf(t353,plain,
or(t3,not(t4)) = t3,
inference(orient,[status(thm)],[t293]) ).
cnf(t574,plain,
and(not(t3),t4) = not(t3),
inference(cp,[status(thm)],[t573,t353]) ).
cnf(t66583,plain,
and(t4,not(t3)) = not(t3),
inference(step,[status(thm)],[t574,t45]) ).
cnf(t599,plain,
and(t4,not(t3)) = not(t3),
inference(orient,[status(thm)],[t66583]) ).
cnf(t1167,plain,
or(t3,t4) = or(t3,not(t3)),
inference(cp,[status(thm)],[t1140,t599]) ).
cnf(t66682,plain,
or(t4,t3) = or(t3,not(t3)),
inference(step,[status(thm)],[t1167,t164]) ).
cnf(t66683,plain,
or(t4,t3) = ll1,
inference(step,[status(thm)],[t66682,t167]) ).
cnf(t1202,plain,
or(t4,t3) = ll1,
inference(orient,[status(thm)],[t66683]) ).
cnf(t1203,plain,
or(t4,and(t3,X1)) = and(ll1,or(t4,X1)),
inference(cp,[status(thm)],[t78,t1202]) ).
cnf(t66824,plain,
or(t4,and(t3,X1)) = or(t4,X1),
inference(step,[status(thm)],[t1203,t437]) ).
cnf(t2119,plain,
or(t4,and(t3,X1)) = or(t4,X1),
inference(orient,[status(thm)],[t66824]) ).
cnf(t2474,plain,
and(b,not(t1)) = and(b,not(not(t3))),
inference(cp,[status(thm)],[t2445,t259]) ).
cnf(t50,plain,
and(X1,and(X1,X2)) = and(X1,X2),
inference(cp,[status(thm)],[t46,t37]) ).
cnf(t438,plain,
and(X1,and(X1,X2)) = and(X1,X2),
inference(orient,[status(thm)],[t50]) ).
cnf(t448,plain,
and(b,a) = and(b,not(t1)),
inference(cp,[status(thm)],[t438,t248]) ).
cnf(t66558,plain,
not(t1) = and(b,not(t1)),
inference(step,[status(thm)],[t448,t248]) ).
cnf(t494,plain,
and(b,not(t1)) = not(t1),
inference(orient,[status(thm)],[t66558]) ).
cnf(t66885,plain,
not(t1) = and(b,not(not(t3))),
inference(step,[status(thm)],[t2474,t494]) ).
cnf(t66886,plain,
not(t1) = and(b,t3),
inference(step,[status(thm)],[t66885,t40]) ).
cnf(t66887,plain,
not(t1) = and(t3,b),
inference(step,[status(thm)],[t66886,t45]) ).
cnf(t2534,plain,
and(t3,b) = not(t1),
inference(orient,[status(thm)],[t66887]) ).
cnf(t2537,plain,
or(t4,b) = or(t4,not(t1)),
inference(cp,[status(thm)],[t2119,t2534]) ).
cnf(t2720,plain,
or(t4,not(t1)) = or(t4,b),
inference(orient,[status(thm)],[t2537]) ).
cnf(t67004,plain,
or(t4,a) = or(t4,b),
inference(step,[status(thm)],[t67003,t2720]) ).
cnf(t3303,plain,
or(t4,a) = or(t4,b),
inference(orient,[status(thm)],[t67004]) ).
cnf(t67005,plain,
xor(t3,not(a)) = or(t4,b),
inference(step,[status(thm)],[t2323,t3303]) ).
cnf(t3304,plain,
xor(t3,not(a)) = or(t4,b),
inference(orient,[status(thm)],[t67005]) ).
cnf(t67010,plain,
or(a,not(t3)) = or(t4,b),
inference(step,[status(thm)],[t67009,t3304]) ).
cnf(t3313,plain,
or(a,not(t3)) = or(t4,b),
inference(orient,[status(thm)],[t67010]) ).
cnf(t67051,plain,
or(b,a) = or(t4,b),
inference(step,[status(thm)],[t67050,t3313]) ).
cnf(t3504,plain,
or(b,a) = or(t4,b),
inference(orient,[status(thm)],[t67051]) ).
cnf(t2191,plain,
or(X1,not(X2)) = or(X1,not(or(X1,X2))),
inference(cp,[status(thm)],[t2189,t69]) ).
cnf(t3908,plain,
or(X1,not(or(X1,X2))) = or(X1,not(X2)),
inference(orient,[status(thm)],[t2191]) ).
cnf(t55,plain,
ll0 = and(X1,and(X2,not(and(X1,X2)))),
inference(cp,[status(thm)],[t54,t46]) ).
cnf(t1263,plain,
and(X1,and(X2,not(and(X1,X2)))) = ll0,
inference(orient,[status(thm)],[t55]) ).
cnf(t1265,plain,
ll0 = and(X1,not(or(X2,and(X1,not(X2))))),
inference(cp,[status(thm)],[t1263,t69]) ).
cnf(t66774,plain,
ll0 = and(X1,not(or(X2,X1))),
inference(step,[status(thm)],[t1265,t1140]) ).
cnf(t1750,plain,
and(X1,not(or(X2,X1))) = ll0,
inference(orient,[status(thm)],[t66774]) ).
cnf(t1771,plain,
xor(X1,not(or(X2,not(X1)))) = or(and(X1,not(not(or(X2,not(X1))))),ll0),
inference(cp,[status(thm)],[t192,t1750]) ).
cnf(t67316,plain,
xor(X1,and(not(X2),X1)) = or(and(X1,not(not(or(X2,not(X1))))),ll0),
inference(step,[status(thm)],[t1771,t573]) ).
cnf(t67317,plain,
xor(X1,and(not(X2),X1)) = and(X1,not(not(or(X2,not(X1))))),
inference(step,[status(thm)],[t67316,t43]) ).
cnf(t67318,plain,
xor(X1,and(not(X2),X1)) = and(X1,or(X2,not(X1))),
inference(step,[status(thm)],[t67317,t40]) ).
cnf(t67319,plain,
xor(X1,and(not(X2),X1)) = and(X1,X2),
inference(step,[status(thm)],[t67318,t1104]) ).
cnf(t6776,plain,
xor(X1,and(not(X2),X1)) = and(X1,X2),
inference(orient,[status(thm)],[t67319]) ).
cnf(t6824,plain,
and(X1,not(X2)) = xor(X1,and(X2,X1)),
inference(cp,[status(thm)],[t6776,t40]) ).
cnf(t6828,plain,
xor(X1,and(X2,X1)) = and(X1,not(X2)),
inference(orient,[status(thm)],[t6824]) ).
cnf(t51,plain,
and(X1,and(or(X1,X2),X3)) = and(X1,X3),
inference(cp,[status(thm)],[t46,t38]) ).
cnf(t1017,plain,
and(X1,and(or(X1,X2),X3)) = and(X1,X3),
inference(orient,[status(thm)],[t51]) ).
cnf(t258,plain,
t1 = or(t1,not(t2)),
inference(cp,[status(thm)],[t42,t254]) ).
cnf(t325,plain,
or(t1,not(t2)) = t1,
inference(orient,[status(thm)],[t258]) ).
cnf(t580,plain,
and(not(t1),t2) = not(t1),
inference(cp,[status(thm)],[t573,t325]) ).
cnf(t66589,plain,
and(t2,not(t1)) = not(t1),
inference(step,[status(thm)],[t580,t45]) ).
cnf(t635,plain,
and(t2,not(t1)) = not(t1),
inference(orient,[status(thm)],[t66589]) ).
cnf(t1646,plain,
and(not(t4),not(t1)) = and(t3,not(t1)),
inference(cp,[status(thm)],[t1642,t635]) ).
cnf(t66761,plain,
not(or(t4,t1)) = and(t3,not(t1)),
inference(step,[status(thm)],[t1646,t69]) ).
cnf(t66762,plain,
not(or(t4,t1)) = not(t1),
inference(step,[status(thm)],[t66761,t677]) ).
cnf(t1656,plain,
not(or(t4,t1)) = not(t1),
inference(orient,[status(thm)],[t66762]) ).
cnf(t1662,plain,
or(t4,t1) = not(not(t1)),
inference(cp,[status(thm)],[t40,t1656]) ).
cnf(t66763,plain,
or(t4,t1) = t1,
inference(step,[status(thm)],[t1662,t40]) ).
cnf(t1671,plain,
or(t4,t1) = t1,
inference(orient,[status(thm)],[t66763]) ).
cnf(t1675,plain,
and(t4,X1) = and(t4,and(t1,X1)),
inference(cp,[status(thm)],[t1017,t1671]) ).
cnf(t4845,plain,
and(t4,and(t1,X1)) = and(t4,X1),
inference(orient,[status(thm)],[t1675]) ).
cnf(f34,negated_conjecture,
not(and(t1,t5)) = carry,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',carry) ).
fof(f34_nnf,plain,
not(and(t1,t5)) = carry,
inference(nnf_transformation,[status(thm)],[f34]) ).
cnf(c34,plain,
not(and(t1,t5)) = carry,
inference(cnf_transformation,[status(esa)],[f34_nnf]) ).
cnf(t13,plain,
not(and(t1,t5)) = carry,
inference(equality_encoding,[status(esa)],[c34]) ).
cnf(t66503,plain,
not(and(t5,t1)) = carry,
inference(step,[status(thm)],[t13,t45]) ).
cnf(t120,plain,
not(and(t5,t1)) = carry,
inference(orient,[status(thm)],[t66503]) ).
cnf(t126,plain,
and(t5,t1) = not(carry),
inference(cp,[status(thm)],[t40,t120]) ).
cnf(t269,plain,
and(t5,t1) = not(carry),
inference(orient,[status(thm)],[t126]) ).
cnf(t2469,plain,
and(t1,not(t5)) = and(t1,not(not(carry))),
inference(cp,[status(thm)],[t2445,t269]) ).
cnf(t66900,plain,
and(t1,not(t5)) = and(t1,carry),
inference(step,[status(thm)],[t2469,t40]) ).
cnf(t2558,plain,
and(t1,not(t5)) = and(t1,carry),
inference(orient,[status(thm)],[t66900]) ).
cnf(t2565,plain,
or(not(t1),t5) = not(and(t1,carry)),
inference(cp,[status(thm)],[t708,t2558]) ).
cnf(t66923,plain,
or(t5,not(t1)) = not(and(t1,carry)),
inference(step,[status(thm)],[t2565,t164]) ).
cnf(f30,negated_conjecture,
not(and(t4,cin)) = t5,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t5) ).
fof(f30_nnf,plain,
not(and(t4,cin)) = t5,
inference(nnf_transformation,[status(thm)],[f30]) ).
cnf(c30,plain,
not(and(t4,cin)) = t5,
inference(cnf_transformation,[status(esa)],[f30_nnf]) ).
cnf(t15,plain,
not(and(t4,cin)) = t5,
inference(equality_encoding,[status(esa)],[c30]) ).
cnf(t127,plain,
not(and(t4,cin)) = t5,
inference(orient,[status(thm)],[t15]) ).
cnf(t133,plain,
and(t4,cin) = not(t5),
inference(cp,[status(thm)],[t40,t127]) ).
cnf(t274,plain,
and(t4,cin) = not(t5),
inference(orient,[status(thm)],[t133]) ).
cnf(t442,plain,
and(t4,cin) = and(t4,not(t5)),
inference(cp,[status(thm)],[t438,t274]) ).
cnf(t66552,plain,
not(t5) = and(t4,not(t5)),
inference(step,[status(thm)],[t442,t274]) ).
cnf(t464,plain,
and(t4,not(t5)) = not(t5),
inference(orient,[status(thm)],[t66552]) ).
cnf(t1168,plain,
or(t5,t4) = or(t5,not(t5)),
inference(cp,[status(thm)],[t1140,t464]) ).
cnf(t66684,plain,
or(t5,t4) = ll1,
inference(step,[status(thm)],[t1168,t167]) ).
cnf(t1205,plain,
or(t5,t4) = ll1,
inference(orient,[status(thm)],[t66684]) ).
cnf(t1206,plain,
or(t5,and(t4,X1)) = and(ll1,or(t5,X1)),
inference(cp,[status(thm)],[t78,t1205]) ).
cnf(t66826,plain,
or(t5,and(t4,X1)) = or(t5,X1),
inference(step,[status(thm)],[t1206,t437]) ).
cnf(t2140,plain,
or(t5,and(t4,X1)) = or(t5,X1),
inference(orient,[status(thm)],[t66826]) ).
cnf(t1020,plain,
and(X1,not(or(X1,X2))) = and(X1,ll0),
inference(cp,[status(thm)],[t1017,t54]) ).
cnf(t66766,plain,
and(X1,not(or(X1,X2))) = ll0,
inference(step,[status(thm)],[t1020,t67]) ).
cnf(t1702,plain,
and(X1,not(or(X1,X2))) = ll0,
inference(orient,[status(thm)],[t66766]) ).
cnf(t1707,plain,
ll0 = and(t4,not(t1)),
inference(cp,[status(thm)],[t1702,t1671]) ).
cnf(t1718,plain,
and(t4,not(t1)) = ll0,
inference(orient,[status(thm)],[t1707]) ).
cnf(t2141,plain,
or(t5,not(t1)) = or(t5,ll0),
inference(cp,[status(thm)],[t2140,t1718]) ).
cnf(t66828,plain,
or(t5,not(t1)) = t5,
inference(step,[status(thm)],[t2141,t43]) ).
cnf(t2160,plain,
or(t5,not(t1)) = t5,
inference(orient,[status(thm)],[t66828]) ).
cnf(t66924,plain,
t5 = not(and(t1,carry)),
inference(step,[status(thm)],[t66923,t2160]) ).
cnf(t2657,plain,
not(and(t1,carry)) = t5,
inference(orient,[status(thm)],[t66924]) ).
cnf(t2664,plain,
and(t1,carry) = not(t5),
inference(cp,[status(thm)],[t40,t2657]) ).
cnf(t2679,plain,
and(t1,carry) = not(t5),
inference(orient,[status(thm)],[t2664]) ).
cnf(t4846,plain,
and(t4,carry) = and(t4,not(t5)),
inference(cp,[status(thm)],[t4845,t2679]) ).
cnf(t67246,plain,
and(t4,carry) = not(t5),
inference(step,[status(thm)],[t4846,t464]) ).
cnf(t4866,plain,
and(t4,carry) = not(t5),
inference(orient,[status(thm)],[t67246]) ).
cnf(t6885,plain,
and(carry,not(t4)) = xor(carry,not(t5)),
inference(cp,[status(thm)],[t6828,t4866]) ).
cnf(t67394,plain,
and(carry,not(t4)) = xor(t5,not(carry)),
inference(step,[status(thm)],[t6885,t1035]) ).
cnf(t7415,plain,
and(carry,not(t4)) = xor(t5,not(carry)),
inference(orient,[status(thm)],[t67394]) ).
cnf(t7438,plain,
or(not(carry),t4) = not(xor(t5,not(carry))),
inference(cp,[status(thm)],[t708,t7415]) ).
cnf(t67403,plain,
or(t4,not(carry)) = not(xor(t5,not(carry))),
inference(step,[status(thm)],[t7438,t164]) ).
cnf(t67404,plain,
or(t4,not(carry)) = xor(t5,not(not(carry))),
inference(step,[status(thm)],[t67403,t784]) ).
cnf(t67405,plain,
or(t4,not(carry)) = xor(t5,carry),
inference(step,[status(thm)],[t67404,t40]) ).
cnf(t6909,plain,
and(carry,not(t1)) = xor(carry,not(t5)),
inference(cp,[status(thm)],[t6828,t2679]) ).
cnf(t845,plain,
t1 = or(t1,not(carry)),
inference(cp,[status(thm)],[t834,t269]) ).
cnf(t884,plain,
or(t1,not(carry)) = t1,
inference(orient,[status(thm)],[t845]) ).
cnf(t889,plain,
and(not(t1),carry) = not(t1),
inference(cp,[status(thm)],[t573,t884]) ).
cnf(t66631,plain,
and(carry,not(t1)) = not(t1),
inference(step,[status(thm)],[t889,t45]) ).
cnf(t963,plain,
and(carry,not(t1)) = not(t1),
inference(orient,[status(thm)],[t66631]) ).
cnf(t67395,plain,
not(t1) = xor(carry,not(t5)),
inference(step,[status(thm)],[t6909,t963]) ).
cnf(t67396,plain,
not(t1) = xor(t5,not(carry)),
inference(step,[status(thm)],[t67395,t1035]) ).
cnf(t7442,plain,
xor(t5,not(carry)) = not(t1),
inference(orient,[status(thm)],[t67396]) ).
cnf(t7446,plain,
xor(t5,not(not(carry))) = not(not(t1)),
inference(cp,[status(thm)],[t784,t7442]) ).
cnf(t67399,plain,
xor(t5,carry) = not(not(t1)),
inference(step,[status(thm)],[t7446,t40]) ).
cnf(t67400,plain,
xor(t5,carry) = t1,
inference(step,[status(thm)],[t67399,t40]) ).
cnf(t7447,plain,
xor(t5,carry) = t1,
inference(orient,[status(thm)],[t67400]) ).
cnf(t67406,plain,
or(t4,not(carry)) = t1,
inference(step,[status(thm)],[t67405,t7447]) ).
cnf(t7450,plain,
or(t4,not(carry)) = t1,
inference(orient,[status(thm)],[t67406]) ).
cnf(t7458,plain,
or(t4,not(not(carry))) = or(t4,not(t1)),
inference(cp,[status(thm)],[t3908,t7450]) ).
cnf(t67407,plain,
or(t4,carry) = or(t4,not(t1)),
inference(step,[status(thm)],[t7458,t40]) ).
cnf(t67408,plain,
or(t4,carry) = or(t4,b),
inference(step,[status(thm)],[t67407,t2720]) ).
cnf(t7460,plain,
or(t4,b) = or(t4,carry),
inference(orient,[status(thm)],[t67408]) ).
cnf(t67421,plain,
or(b,a) = or(t4,carry),
inference(step,[status(thm)],[t3504,t7460]) ).
cnf(t7473,plain,
or(b,a) = or(t4,carry),
inference(orient,[status(thm)],[t67421]) ).
cnf(t68127,plain,
xor(sum_def,not(cin)) = not(and(t1,or(t4,carry))),
inference(step,[status(thm)],[t68126,t7473]) ).
cnf(t255,plain,
and(t1,or(a,X1)) = or(not(t2),and(t1,X1)),
inference(cp,[status(thm)],[t57,t254]) ).
cnf(t16074,plain,
or(not(t2),and(t1,X1)) = and(t1,or(a,X1)),
inference(orient,[status(thm)],[t255]) ).
cnf(t447,plain,
and(t1,b) = and(t1,not(t3)),
inference(cp,[status(thm)],[t438,t259]) ).
cnf(t66557,plain,
not(t3) = and(t1,not(t3)),
inference(step,[status(thm)],[t447,t259]) ).
cnf(t489,plain,
and(t1,not(t3)) = not(t3),
inference(orient,[status(thm)],[t66557]) ).
cnf(t16081,plain,
and(t1,or(a,not(t3))) = or(not(t2),not(t3)),
inference(cp,[status(thm)],[t16074,t489]) ).
cnf(t67419,plain,
or(a,not(t3)) = or(t4,carry),
inference(step,[status(thm)],[t3313,t7460]) ).
cnf(t7471,plain,
or(a,not(t3)) = or(t4,carry),
inference(orient,[status(thm)],[t67419]) ).
cnf(t67865,plain,
and(t1,or(t4,carry)) = or(not(t2),not(t3)),
inference(step,[status(thm)],[t16081,t7471]) ).
cnf(t67866,plain,
and(t1,or(t4,carry)) = not(and(t2,t3)),
inference(step,[status(thm)],[t67865,t87]) ).
cnf(t67867,plain,
and(t1,or(t4,carry)) = not(and(t3,t2)),
inference(step,[status(thm)],[t67866,t45]) ).
cnf(t67868,plain,
and(t1,or(t4,carry)) = not(not(t4)),
inference(step,[status(thm)],[t67867,t289]) ).
cnf(t67869,plain,
and(t1,or(t4,carry)) = t4,
inference(step,[status(thm)],[t67868,t40]) ).
cnf(t16125,plain,
and(t1,or(t4,carry)) = t4,
inference(orient,[status(thm)],[t67869]) ).
cnf(t68128,plain,
xor(sum_def,not(cin)) = not(t4),
inference(step,[status(thm)],[t68127,t16125]) ).
cnf(t25896,plain,
xor(sum_def,not(cin)) = not(t4),
inference(orient,[status(thm)],[t68128]) ).
cnf(t25904,plain,
xor(sum_def,not(not(cin))) = not(not(t4)),
inference(cp,[status(thm)],[t784,t25896]) ).
cnf(t68131,plain,
xor(sum_def,cin) = not(not(t4)),
inference(step,[status(thm)],[t25904,t40]) ).
cnf(t68132,plain,
xor(sum_def,cin) = t4,
inference(step,[status(thm)],[t68131,t40]) ).
cnf(t25906,plain,
xor(sum_def,cin) = t4,
inference(orient,[status(thm)],[t68132]) ).
cnf(t25913,plain,
xor(ll0,cin) = xor(sum_def,t4),
inference(cp,[status(thm)],[t1065,t25906]) ).
cnf(f32,negated_conjecture,
not(and(t5,cin)) = t7,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7) ).
fof(f32_nnf,plain,
not(and(t5,cin)) = t7,
inference(nnf_transformation,[status(thm)],[f32]) ).
cnf(c32,plain,
not(and(t5,cin)) = t7,
inference(cnf_transformation,[status(esa)],[f32_nnf]) ).
cnf(t17,plain,
not(and(t5,cin)) = t7,
inference(equality_encoding,[status(esa)],[c32]) ).
cnf(t113,plain,
not(and(t5,cin)) = t7,
inference(orient,[status(thm)],[t17]) ).
cnf(t119,plain,
and(t5,cin) = not(t7),
inference(cp,[status(thm)],[t40,t113]) ).
cnf(t264,plain,
and(t5,cin) = not(t7),
inference(orient,[status(thm)],[t119]) ).
cnf(t3382,plain,
and(t5,not(cin)) = and(t5,not(not(t7))),
inference(cp,[status(thm)],[t3354,t264]) ).
cnf(t842,plain,
cin = or(cin,not(t5)),
inference(cp,[status(thm)],[t834,t274]) ).
cnf(t866,plain,
or(cin,not(t5)) = cin,
inference(orient,[status(thm)],[t842]) ).
cnf(t871,plain,
and(not(cin),t5) = not(cin),
inference(cp,[status(thm)],[t573,t866]) ).
cnf(t66625,plain,
and(t5,not(cin)) = not(cin),
inference(step,[status(thm)],[t871,t45]) ).
cnf(t933,plain,
and(t5,not(cin)) = not(cin),
inference(orient,[status(thm)],[t66625]) ).
cnf(t67019,plain,
not(cin) = and(t5,not(not(t7))),
inference(step,[status(thm)],[t3382,t933]) ).
cnf(t67020,plain,
not(cin) = and(t5,t7),
inference(step,[status(thm)],[t67019,t40]) ).
cnf(t67021,plain,
not(cin) = and(t7,t5),
inference(step,[status(thm)],[t67020,t45]) ).
cnf(t3436,plain,
and(t7,t5) = not(cin),
inference(orient,[status(thm)],[t67021]) ).
cnf(t6878,plain,
and(t5,not(t7)) = xor(t5,not(cin)),
inference(cp,[status(thm)],[t6828,t3436]) ).
cnf(t444,plain,
and(t5,cin) = and(t5,not(t7)),
inference(cp,[status(thm)],[t438,t264]) ).
cnf(t66554,plain,
not(t7) = and(t5,not(t7)),
inference(step,[status(thm)],[t444,t264]) ).
cnf(t474,plain,
and(t5,not(t7)) = not(t7),
inference(orient,[status(thm)],[t66554]) ).
cnf(t67331,plain,
not(t7) = xor(t5,not(cin)),
inference(step,[status(thm)],[t6878,t474]) ).
cnf(t6947,plain,
xor(t5,not(cin)) = not(t7),
inference(orient,[status(thm)],[t67331]) ).
cnf(t6949,plain,
xor(t5,not(not(cin))) = not(not(t7)),
inference(cp,[status(thm)],[t784,t6947]) ).
cnf(t67332,plain,
xor(t5,cin) = not(not(t7)),
inference(step,[status(thm)],[t6949,t40]) ).
cnf(t67333,plain,
xor(t5,cin) = t7,
inference(step,[status(thm)],[t67332,t40]) ).
cnf(t6950,plain,
xor(t5,cin) = t7,
inference(orient,[status(thm)],[t67333]) ).
cnf(t6951,plain,
xor(ll0,cin) = xor(t5,t7),
inference(cp,[status(thm)],[t1065,t6950]) ).
cnf(t67373,plain,
xor(ll0,cin) = xor(t7,t5),
inference(step,[status(thm)],[t6951,t237]) ).
cnf(t7383,plain,
xor(ll0,cin) = xor(t7,t5),
inference(orient,[status(thm)],[t67373]) ).
cnf(t7384,plain,
or(ll0,cin) = or(ll0,xor(t7,t5)),
inference(cp,[status(thm)],[t5009,t7383]) ).
cnf(t67382,plain,
cin = or(ll0,xor(t7,t5)),
inference(step,[status(thm)],[t7384,t436]) ).
cnf(t67383,plain,
cin = xor(t7,t5),
inference(step,[status(thm)],[t67382,t436]) ).
cnf(t7402,plain,
xor(t7,t5) = cin,
inference(orient,[status(thm)],[t67383]) ).
cnf(t67384,plain,
xor(ll0,cin) = cin,
inference(step,[status(thm)],[t7383,t7402]) ).
cnf(t7403,plain,
xor(ll0,cin) = cin,
inference(orient,[status(thm)],[t67384]) ).
cnf(t68138,plain,
cin = xor(sum_def,t4),
inference(step,[status(thm)],[t25913,t7403]) ).
cnf(t68139,plain,
cin = xor(t4,sum_def),
inference(step,[status(thm)],[t68138,t237]) ).
cnf(t25917,plain,
xor(t4,sum_def) = cin,
inference(orient,[status(thm)],[t68139]) ).
cnf(t25923,plain,
xor(ll0,sum_def) = xor(t4,cin),
inference(cp,[status(thm)],[t1065,t25917]) ).
cnf(t68159,plain,
xor(sum_def,ll0) = xor(t4,cin),
inference(step,[status(thm)],[t25923,t237]) ).
cnf(f13,axiom,
not(ll0) = ll1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ll0_inverse) ).
fof(f13_nnf,plain,
not(ll0) = ll1,
inference(nnf_transformation,[status(thm)],[f13]) ).
cnf(c13,plain,
not(ll0) = ll1,
inference(cnf_transformation,[status(esa)],[f13_nnf]) ).
cnf(t0,plain,
not(ll0) = ll1,
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(t160,plain,
not(ll0) = ll1,
inference(orient,[status(thm)],[t0]) ).
cnf(t197,plain,
xor(X1,ll0) = or(and(X1,ll1),and(not(X1),ll0)),
inference(cp,[status(thm)],[t192,t160]) ).
cnf(t66516,plain,
xor(X1,ll0) = or(X1,and(not(X1),ll0)),
inference(step,[status(thm)],[t197,t39]) ).
cnf(t66517,plain,
xor(X1,ll0) = or(X1,ll0),
inference(step,[status(thm)],[t66516,t67]) ).
cnf(t66518,plain,
xor(X1,ll0) = X1,
inference(step,[status(thm)],[t66517,t43]) ).
cnf(t247,plain,
xor(X1,ll0) = X1,
inference(orient,[status(thm)],[t66518]) ).
cnf(t68160,plain,
sum_def = xor(t4,cin),
inference(step,[status(thm)],[t68159,t247]) ).
cnf(t1840,plain,
xor(X1,or(not(not(X1)),X2)) = or(and(X1,not(or(not(not(X1)),X2))),and(not(X1),X2)),
inference(cp,[status(thm)],[t192,t1814]) ).
cnf(t66776,plain,
xor(X1,or(X1,X2)) = or(and(X1,not(or(not(not(X1)),X2))),and(not(X1),X2)),
inference(step,[status(thm)],[t1840,t40]) ).
cnf(t66777,plain,
xor(X1,or(X1,X2)) = or(and(not(X1),X2),and(X1,not(or(not(not(X1)),X2)))),
inference(step,[status(thm)],[t66776,t164]) ).
cnf(t72,plain,
not(or(not(X1),X2)) = and(X1,not(X2)),
inference(cp,[status(thm)],[t69,t40]) ).
cnf(t557,plain,
not(or(not(X1),X2)) = and(X1,not(X2)),
inference(orient,[status(thm)],[t72]) ).
cnf(t66778,plain,
xor(X1,or(X1,X2)) = or(and(not(X1),X2),and(X1,and(not(X1),not(X2)))),
inference(step,[status(thm)],[t66777,t557]) ).
cnf(t66779,plain,
xor(X1,or(X1,X2)) = or(and(not(X1),X2),and(X1,not(or(X1,X2)))),
inference(step,[status(thm)],[t66778,t69]) ).
cnf(t66780,plain,
xor(X1,or(X1,X2)) = or(and(not(X1),X2),ll0),
inference(step,[status(thm)],[t66779,t1702]) ).
cnf(t66781,plain,
xor(X1,or(X1,X2)) = and(not(X1),X2),
inference(step,[status(thm)],[t66780,t43]) ).
cnf(t1845,plain,
xor(X1,or(X1,X2)) = and(not(X1),X2),
inference(orient,[status(thm)],[t66781]) ).
cnf(t1867,plain,
xor(X1,not(or(X1,X2))) = not(and(not(X1),X2)),
inference(cp,[status(thm)],[t784,t1845]) ).
cnf(t67605,plain,
xor(X1,not(or(X1,X2))) = or(X1,not(X2)),
inference(step,[status(thm)],[t1867,t689]) ).
cnf(t10210,plain,
xor(X1,not(or(X1,X2))) = or(X1,not(X2)),
inference(orient,[status(thm)],[t67605]) ).
cnf(f33,negated_conjecture,
not(and(t6,t7)) = sum,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sum) ).
fof(f33_nnf,plain,
not(and(t6,t7)) = sum,
inference(nnf_transformation,[status(thm)],[f33]) ).
cnf(c33,plain,
not(and(t6,t7)) = sum,
inference(cnf_transformation,[status(esa)],[f33_nnf]) ).
cnf(t18,plain,
not(and(t6,t7)) = sum,
inference(equality_encoding,[status(esa)],[c33]) ).
cnf(t66505,plain,
not(and(t7,t6)) = sum,
inference(step,[status(thm)],[t18,t45]) ).
cnf(t141,plain,
not(and(t7,t6)) = sum,
inference(orient,[status(thm)],[t66505]) ).
cnf(t147,plain,
and(t7,t6) = not(sum),
inference(cp,[status(thm)],[t40,t141]) ).
cnf(t284,plain,
and(t7,t6) = not(sum),
inference(orient,[status(thm)],[t147]) ).
cnf(t287,plain,
and(t7,and(t6,X1)) = and(not(sum),X1),
inference(cp,[status(thm)],[t46,t284]) ).
cnf(t1627,plain,
and(t7,and(t6,X1)) = and(not(sum),X1),
inference(orient,[status(thm)],[t287]) ).
cnf(f31,negated_conjecture,
not(and(t4,t5)) = t6,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6) ).
fof(f31_nnf,plain,
not(and(t4,t5)) = t6,
inference(nnf_transformation,[status(thm)],[f31]) ).
cnf(c31,plain,
not(and(t4,t5)) = t6,
inference(cnf_transformation,[status(esa)],[f31_nnf]) ).
cnf(t16,plain,
not(and(t4,t5)) = t6,
inference(equality_encoding,[status(esa)],[c31]) ).
cnf(t66504,plain,
not(and(t5,t4)) = t6,
inference(step,[status(thm)],[t16,t45]) ).
cnf(t134,plain,
not(and(t5,t4)) = t6,
inference(orient,[status(thm)],[t66504]) ).
cnf(t140,plain,
and(t5,t4) = not(t6),
inference(cp,[status(thm)],[t40,t134]) ).
cnf(t279,plain,
and(t5,t4) = not(t6),
inference(orient,[status(thm)],[t140]) ).
cnf(t282,plain,
and(t5,and(t4,X1)) = and(not(t6),X1),
inference(cp,[status(thm)],[t46,t279]) ).
cnf(t1514,plain,
and(t5,and(t4,X1)) = and(not(t6),X1),
inference(orient,[status(thm)],[t282]) ).
cnf(t1518,plain,
and(not(t6),cin) = and(t5,not(t5)),
inference(cp,[status(thm)],[t1514,t274]) ).
cnf(t66734,plain,
and(cin,not(t6)) = and(t5,not(t5)),
inference(step,[status(thm)],[t1518,t45]) ).
cnf(t66735,plain,
and(cin,not(t6)) = ll0,
inference(step,[status(thm)],[t66734,t54]) ).
cnf(t1529,plain,
and(cin,not(t6)) = ll0,
inference(orient,[status(thm)],[t66735]) ).
cnf(t1535,plain,
or(not(cin),t6) = not(ll0),
inference(cp,[status(thm)],[t708,t1529]) ).
cnf(t66741,plain,
or(t6,not(cin)) = not(ll0),
inference(step,[status(thm)],[t1535,t164]) ).
cnf(t66742,plain,
or(t6,not(cin)) = ll1,
inference(step,[status(thm)],[t66741,t160]) ).
cnf(t1559,plain,
or(t6,not(cin)) = ll1,
inference(orient,[status(thm)],[t66742]) ).
cnf(t1562,plain,
and(cin,t6) = and(cin,ll1),
inference(cp,[status(thm)],[t1104,t1559]) ).
cnf(t66743,plain,
and(t6,cin) = and(cin,ll1),
inference(step,[status(thm)],[t1562,t45]) ).
cnf(t66744,plain,
and(t6,cin) = cin,
inference(step,[status(thm)],[t66743,t39]) ).
cnf(t1563,plain,
and(t6,cin) = cin,
inference(orient,[status(thm)],[t66744]) ).
cnf(t1629,plain,
and(not(sum),cin) = and(t7,cin),
inference(cp,[status(thm)],[t1627,t1563]) ).
cnf(t66850,plain,
and(cin,not(sum)) = and(t7,cin),
inference(step,[status(thm)],[t1629,t45]) ).
cnf(t2280,plain,
and(cin,not(sum)) = and(t7,cin),
inference(orient,[status(thm)],[t66850]) ).
cnf(t2468,plain,
and(cin,not(t5)) = and(cin,not(not(t7))),
inference(cp,[status(thm)],[t2445,t264]) ).
cnf(t867,plain,
not(t5) = and(not(t5),cin),
inference(cp,[status(thm)],[t825,t866]) ).
cnf(t66624,plain,
not(t5) = and(cin,not(t5)),
inference(step,[status(thm)],[t867,t45]) ).
cnf(t928,plain,
and(cin,not(t5)) = not(t5),
inference(orient,[status(thm)],[t66624]) ).
cnf(t66877,plain,
not(t5) = and(cin,not(not(t7))),
inference(step,[status(thm)],[t2468,t928]) ).
cnf(t66878,plain,
not(t5) = and(cin,t7),
inference(step,[status(thm)],[t66877,t40]) ).
cnf(t66879,plain,
not(t5) = and(t7,cin),
inference(step,[status(thm)],[t66878,t45]) ).
cnf(t2523,plain,
and(t7,cin) = not(t5),
inference(orient,[status(thm)],[t66879]) ).
cnf(t66880,plain,
and(cin,not(sum)) = not(t5),
inference(step,[status(thm)],[t2280,t2523]) ).
cnf(t2524,plain,
and(cin,not(sum)) = not(t5),
inference(orient,[status(thm)],[t66880]) ).
cnf(t3268,plain,
or(not(not(sum)),cin) = or(not(not(sum)),not(t5)),
inference(cp,[status(thm)],[t3248,t2524]) ).
cnf(t66993,plain,
or(cin,not(not(sum))) = or(not(not(sum)),not(t5)),
inference(step,[status(thm)],[t3268,t164]) ).
cnf(t66994,plain,
or(cin,sum) = or(not(not(sum)),not(t5)),
inference(step,[status(thm)],[t66993,t40]) ).
cnf(t66995,plain,
or(sum,cin) = or(not(not(sum)),not(t5)),
inference(step,[status(thm)],[t66994,t164]) ).
cnf(t66996,plain,
or(sum,cin) = not(and(not(sum),t5)),
inference(step,[status(thm)],[t66995,t87]) ).
cnf(t66997,plain,
or(sum,cin) = or(sum,not(t5)),
inference(step,[status(thm)],[t66996,t689]) ).
cnf(t2467,plain,
and(t4,not(t5)) = and(t4,not(not(t6))),
inference(cp,[status(thm)],[t2445,t279]) ).
cnf(t66874,plain,
not(t5) = and(t4,not(not(t6))),
inference(step,[status(thm)],[t2467,t464]) ).
cnf(t66875,plain,
not(t5) = and(t4,t6),
inference(step,[status(thm)],[t66874,t40]) ).
cnf(t66876,plain,
not(t5) = and(t6,t4),
inference(step,[status(thm)],[t66875,t45]) ).
cnf(t2518,plain,
and(t6,t4) = not(t5),
inference(orient,[status(thm)],[t66876]) ).
cnf(t2519,plain,
and(not(sum),t4) = and(t7,not(t5)),
inference(cp,[status(thm)],[t1627,t2518]) ).
cnf(t66908,plain,
and(t4,not(sum)) = and(t7,not(t5)),
inference(step,[status(thm)],[t2519,t45]) ).
cnf(t268,plain,
t5 = or(t5,not(t7)),
inference(cp,[status(thm)],[t42,t264]) ).
cnf(t333,plain,
or(t5,not(t7)) = t5,
inference(orient,[status(thm)],[t268]) ).
cnf(t578,plain,
and(not(t5),t7) = not(t5),
inference(cp,[status(thm)],[t573,t333]) ).
cnf(t66587,plain,
and(t7,not(t5)) = not(t5),
inference(step,[status(thm)],[t578,t45]) ).
cnf(t623,plain,
and(t7,not(t5)) = not(t5),
inference(orient,[status(thm)],[t66587]) ).
cnf(t66909,plain,
and(t4,not(sum)) = not(t5),
inference(step,[status(thm)],[t66908,t623]) ).
cnf(t2583,plain,
and(t4,not(sum)) = not(t5),
inference(orient,[status(thm)],[t66909]) ).
cnf(t2590,plain,
or(sum,t4) = or(sum,not(t5)),
inference(cp,[status(thm)],[t1140,t2583]) ).
cnf(t66940,plain,
or(t4,sum) = or(sum,not(t5)),
inference(step,[status(thm)],[t2590,t164]) ).
cnf(t2986,plain,
or(sum,not(t5)) = or(t4,sum),
inference(orient,[status(thm)],[t66940]) ).
cnf(t66998,plain,
or(sum,cin) = or(t4,sum),
inference(step,[status(thm)],[t66997,t2986]) ).
cnf(t3294,plain,
or(sum,cin) = or(t4,sum),
inference(orient,[status(thm)],[t66998]) ).
cnf(t10253,plain,
or(sum,not(cin)) = xor(sum,not(or(t4,sum))),
inference(cp,[status(thm)],[t10210,t3294]) ).
cnf(t3923,plain,
or(sum,not(cin)) = or(sum,not(or(t4,sum))),
inference(cp,[status(thm)],[t3908,t3294]) ).
cnf(t1181,plain,
or(X1,not(X2)) = or(X1,not(or(X2,X1))),
inference(cp,[status(thm)],[t1140,t69]) ).
cnf(t3133,plain,
or(X1,not(or(X2,X1))) = or(X1,not(X2)),
inference(orient,[status(thm)],[t1181]) ).
cnf(t67165,plain,
or(sum,not(cin)) = or(sum,not(t4)),
inference(step,[status(thm)],[t3923,t3133]) ).
cnf(t2591,plain,
or(not(t4),sum) = not(not(t5)),
inference(cp,[status(thm)],[t708,t2583]) ).
cnf(t66911,plain,
or(sum,not(t4)) = not(not(t5)),
inference(step,[status(thm)],[t2591,t164]) ).
cnf(t66912,plain,
or(sum,not(t4)) = t5,
inference(step,[status(thm)],[t66911,t40]) ).
cnf(t2603,plain,
or(sum,not(t4)) = t5,
inference(orient,[status(thm)],[t66912]) ).
cnf(t67166,plain,
or(sum,not(cin)) = t5,
inference(step,[status(thm)],[t67165,t2603]) ).
cnf(t3946,plain,
or(sum,not(cin)) = t5,
inference(orient,[status(thm)],[t67166]) ).
cnf(t67606,plain,
t5 = xor(sum,not(or(t4,sum))),
inference(step,[status(thm)],[t10253,t3946]) ).
cnf(t843,plain,
t4 = or(t4,not(t6)),
inference(cp,[status(thm)],[t834,t279]) ).
cnf(t872,plain,
or(t4,not(t6)) = t4,
inference(orient,[status(thm)],[t843]) ).
cnf(t877,plain,
and(not(t4),t6) = not(t4),
inference(cp,[status(thm)],[t573,t872]) ).
cnf(t66627,plain,
and(t6,not(t4)) = not(t4),
inference(step,[status(thm)],[t877,t45]) ).
cnf(t943,plain,
and(t6,not(t4)) = not(t4),
inference(orient,[status(thm)],[t66627]) ).
cnf(t1630,plain,
and(not(sum),not(t4)) = and(t7,not(t4)),
inference(cp,[status(thm)],[t1627,t943]) ).
cnf(t66851,plain,
not(or(sum,t4)) = and(t7,not(t4)),
inference(step,[status(thm)],[t1630,t69]) ).
cnf(t66852,plain,
not(or(t4,sum)) = and(t7,not(t4)),
inference(step,[status(thm)],[t66851,t164]) ).
cnf(t132,plain,
ll0 = and(and(t4,cin),t5),
inference(cp,[status(thm)],[t54,t127]) ).
cnf(t66569,plain,
ll0 = and(t4,and(cin,t5)),
inference(step,[status(thm)],[t132,t46]) ).
cnf(t66570,plain,
ll0 = and(t4,and(t5,cin)),
inference(step,[status(thm)],[t66569,t45]) ).
cnf(t66571,plain,
ll0 = and(t4,not(t7)),
inference(step,[status(thm)],[t66570,t264]) ).
cnf(t520,plain,
and(t4,not(t7)) = ll0,
inference(orient,[status(thm)],[t66571]) ).
cnf(t524,plain,
xor(t4,t7) = or(ll0,and(not(t4),t7)),
inference(cp,[status(thm)],[t192,t520]) ).
cnf(t66580,plain,
xor(t7,t4) = or(ll0,and(not(t4),t7)),
inference(step,[status(thm)],[t524,t237]) ).
cnf(t66581,plain,
xor(t7,t4) = and(not(t4),t7),
inference(step,[status(thm)],[t66580,t436]) ).
cnf(t66582,plain,
xor(t7,t4) = and(t7,not(t4)),
inference(step,[status(thm)],[t66581,t45]) ).
cnf(t550,plain,
and(t7,not(t4)) = xor(t7,t4),
inference(orient,[status(thm)],[t66582]) ).
cnf(t66853,plain,
not(or(t4,sum)) = xor(t7,t4),
inference(step,[status(thm)],[t66852,t550]) ).
cnf(t2291,plain,
not(or(t4,sum)) = xor(t7,t4),
inference(orient,[status(thm)],[t66853]) ).
cnf(t67607,plain,
t5 = xor(sum,xor(t7,t4)),
inference(step,[status(thm)],[t67606,t2291]) ).
cnf(t67608,plain,
t5 = xor(t7,xor(sum,t4)),
inference(step,[status(thm)],[t67607,t1033]) ).
cnf(t67609,plain,
t5 = xor(t7,xor(t4,sum)),
inference(step,[status(thm)],[t67608,t237]) ).
cnf(t10337,plain,
xor(t7,xor(t4,sum)) = t5,
inference(orient,[status(thm)],[t67609]) ).
cnf(t10340,plain,
xor(ll0,xor(t4,sum)) = xor(t7,t5),
inference(cp,[status(thm)],[t1065,t10337]) ).
cnf(t67646,plain,
xor(t4,xor(ll0,sum)) = xor(t7,t5),
inference(step,[status(thm)],[t10340,t1033]) ).
cnf(t67647,plain,
xor(t4,xor(sum,ll0)) = xor(t7,t5),
inference(step,[status(thm)],[t67646,t237]) ).
cnf(t67648,plain,
xor(t4,sum) = xor(t7,t5),
inference(step,[status(thm)],[t67647,t247]) ).
cnf(t67649,plain,
xor(t4,sum) = cin,
inference(step,[status(thm)],[t67648,t7402]) ).
cnf(t10487,plain,
xor(t4,sum) = cin,
inference(orient,[status(thm)],[t67649]) ).
cnf(t10488,plain,
xor(ll0,sum) = xor(t4,cin),
inference(cp,[status(thm)],[t1065,t10487]) ).
cnf(t67650,plain,
xor(sum,ll0) = xor(t4,cin),
inference(step,[status(thm)],[t10488,t237]) ).
cnf(t67651,plain,
sum = xor(t4,cin),
inference(step,[status(thm)],[t67650,t247]) ).
cnf(t10490,plain,
xor(t4,cin) = sum,
inference(orient,[status(thm)],[t67651]) ).
cnf(t68161,plain,
sum_def = sum,
inference(step,[status(thm)],[t68160,t10490]) ).
cnf(t25967,plain,
sum = sum_def,
inference(orient,[status(thm)],[t68161]) ).
cnf(t68319,plain,
ifeq(sum_def,sum_def,ifeq(carry,carry_def,false,true),true) = true,
inference(step,[status(thm)],[t243,t25967]) ).
cnf(t22,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t44,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t22]) ).
cnf(t68320,plain,
ifeq(carry,carry_def,false,true) = true,
inference(step,[status(thm)],[t68319,t44]) ).
cnf(t26106,plain,
ifeq(carry,carry_def,false,true) = true,
inference(rw,[status(thm)],[t68320]) ).
cnf(t32371,plain,
ifeq(carry,carry_def,false,true) = true,
inference(orient,[status(thm)],[t26106]) ).
cnf(t1021,plain,
and(X1,X2) = and(X1,and(X2,or(X1,X3))),
inference(cp,[status(thm)],[t1017,t45]) ).
cnf(t21945,plain,
and(X1,and(X2,or(X1,X3))) = and(X1,X2),
inference(orient,[status(thm)],[t1021]) ).
cnf(t5034,plain,
and(X1,xor(not(X1),X2)) = and(X1,or(not(X1),X2)),
inference(cp,[status(thm)],[t1814,t5009]) ).
cnf(t67516,plain,
and(X1,xor(not(X1),X2)) = and(X1,X2),
inference(step,[status(thm)],[t5034,t1814]) ).
cnf(t8387,plain,
and(X1,xor(not(X1),X2)) = and(X1,X2),
inference(orient,[status(thm)],[t67516]) ).
cnf(t376,plain,
xor(X1,xor(ll1,X2)) = xor(not(X1),X2),
inference(cp,[status(thm)],[t238,t370]) ).
cnf(t2188,plain,
xor(X1,xor(ll1,X2)) = xor(not(X1),X2),
inference(orient,[status(thm)],[t376]) ).
cnf(t8390,plain,
and(X1,xor(ll1,X2)) = and(X1,xor(not(not(X1)),X2)),
inference(cp,[status(thm)],[t8387,t2188]) ).
cnf(t67598,plain,
and(X1,xor(ll1,X2)) = and(X1,xor(X1,X2)),
inference(step,[status(thm)],[t8390,t40]) ).
cnf(t10119,plain,
and(X1,xor(ll1,X2)) = and(X1,xor(X1,X2)),
inference(orient,[status(thm)],[t67598]) ).
cnf(t10121,plain,
and(X1,xor(X1,X2)) = and(X1,xor(X2,ll1)),
inference(cp,[status(thm)],[t10119,t237]) ).
cnf(t67694,plain,
and(X1,xor(X1,X2)) = and(X1,not(X2)),
inference(step,[status(thm)],[t10121,t370]) ).
cnf(t11435,plain,
and(X1,xor(X1,X2)) = and(X1,not(X2)),
inference(orient,[status(thm)],[t67694]) ).
cnf(t25142,plain,
xor(not(X1),or(X1,X2)) = or(X1,not(or(X1,or(X1,X2)))),
inference(cp,[status(thm)],[t25122,t38]) ).
cnf(t68407,plain,
xor(not(X1),or(X1,X2)) = or(X1,not(or(X1,X2))),
inference(step,[status(thm)],[t25142,t3908]) ).
cnf(t68408,plain,
xor(not(X1),or(X1,X2)) = or(X1,not(X2)),
inference(step,[status(thm)],[t68407,t3908]) ).
cnf(t26830,plain,
xor(not(X1),or(X1,X2)) = or(X1,not(X2)),
inference(orient,[status(thm)],[t68408]) ).
cnf(t27052,plain,
or(not(X1),not(not(X2))) = xor(not(not(X1)),not(and(X1,X2))),
inference(cp,[status(thm)],[t26830,t87]) ).
cnf(t68489,plain,
not(and(X1,not(X2))) = xor(not(not(X1)),not(and(X1,X2))),
inference(step,[status(thm)],[t27052,t87]) ).
cnf(t68490,plain,
or(not(X1),X2) = xor(not(not(X1)),not(and(X1,X2))),
inference(step,[status(thm)],[t68489,t708]) ).
cnf(t68491,plain,
or(not(X1),X2) = xor(X1,not(and(X1,X2))),
inference(step,[status(thm)],[t68490,t40]) ).
cnf(t28534,plain,
xor(X1,not(and(X1,X2))) = or(not(X1),X2),
inference(orient,[status(thm)],[t68491]) ).
cnf(t28638,plain,
xor(X1,not(not(and(X1,X2)))) = not(or(not(X1),X2)),
inference(cp,[status(thm)],[t784,t28534]) ).
cnf(t68504,plain,
xor(X1,and(X1,X2)) = not(or(not(X1),X2)),
inference(step,[status(thm)],[t28638,t40]) ).
cnf(t68505,plain,
xor(X1,and(X1,X2)) = and(X1,not(X2)),
inference(step,[status(thm)],[t68504,t557]) ).
cnf(t28646,plain,
xor(X1,and(X1,X2)) = and(X1,not(X2)),
inference(orient,[status(thm)],[t68505]) ).
cnf(t166,plain,
or(X1,and(X2,X3)) = and(or(X1,X2),or(X3,X1)),
inference(cp,[status(thm)],[t78,t164]) ).
cnf(t14830,plain,
and(or(X1,X2),or(X3,X1)) = or(X1,and(X2,X3)),
inference(orient,[status(thm)],[t166]) ).
cnf(t210,plain,
xor(X1,not(X1)) = or(and(X1,not(not(X1))),not(X1)),
inference(cp,[status(thm)],[t192,t37]) ).
cnf(t66521,plain,
xor(X1,not(X1)) = or(not(X1),and(X1,not(not(X1)))),
inference(step,[status(thm)],[t210,t164]) ).
cnf(t66522,plain,
xor(X1,not(X1)) = or(not(X1),and(X1,X1)),
inference(step,[status(thm)],[t66521,t40]) ).
cnf(t66523,plain,
xor(X1,not(X1)) = or(not(X1),X1),
inference(step,[status(thm)],[t66522,t37]) ).
cnf(t66524,plain,
xor(X1,not(X1)) = or(X1,not(X1)),
inference(step,[status(thm)],[t66523,t164]) ).
cnf(t66525,plain,
xor(X1,not(X1)) = ll1,
inference(step,[status(thm)],[t66524,t167]) ).
cnf(t294,plain,
xor(X1,not(X1)) = ll1,
inference(orient,[status(thm)],[t66525]) ).
cnf(t1719,plain,
and(not(t6),not(t1)) = and(t5,ll0),
inference(cp,[status(thm)],[t1514,t1718]) ).
cnf(t66769,plain,
not(or(t6,t1)) = and(t5,ll0),
inference(step,[status(thm)],[t1719,t69]) ).
cnf(t66770,plain,
not(or(t6,t1)) = ll0,
inference(step,[status(thm)],[t66769,t67]) ).
cnf(t1728,plain,
not(or(t6,t1)) = ll0,
inference(orient,[status(thm)],[t66770]) ).
cnf(t1729,plain,
ll1 = xor(or(t6,t1),ll0),
inference(cp,[status(thm)],[t294,t1728]) ).
cnf(t66771,plain,
ll1 = or(t6,t1),
inference(step,[status(thm)],[t1729,t247]) ).
cnf(t1744,plain,
or(t6,t1) = ll1,
inference(orient,[status(thm)],[t66771]) ).
cnf(t15169,plain,
or(t1,and(X1,t6)) = and(or(t1,X1),ll1),
inference(cp,[status(thm)],[t14830,t1744]) ).
cnf(t67839,plain,
or(t1,and(X1,t6)) = or(t1,X1),
inference(step,[status(thm)],[t15169,t39]) ).
cnf(t15616,plain,
or(t1,and(X1,t6)) = or(t1,X1),
inference(orient,[status(thm)],[t67839]) ).
cnf(t15617,plain,
or(t1,t7) = or(t1,not(sum)),
inference(cp,[status(thm)],[t15616,t284]) ).
cnf(t67840,plain,
or(t7,t1) = or(t1,not(sum)),
inference(step,[status(thm)],[t15617,t164]) ).
cnf(t15639,plain,
or(t1,not(sum)) = or(t7,t1),
inference(orient,[status(thm)],[t67840]) ).
cnf(t15660,plain,
and(not(t1),sum) = not(or(t7,t1)),
inference(cp,[status(thm)],[t573,t15639]) ).
cnf(t67850,plain,
and(sum,not(t1)) = not(or(t7,t1)),
inference(step,[status(thm)],[t15660,t45]) ).
cnf(t1162,plain,
or(t5,t7) = or(t5,not(t5)),
inference(cp,[status(thm)],[t1140,t623]) ).
cnf(t66689,plain,
or(t7,t5) = or(t5,not(t5)),
inference(step,[status(thm)],[t1162,t164]) ).
cnf(t66690,plain,
or(t7,t5) = ll1,
inference(step,[status(thm)],[t66689,t167]) ).
cnf(t1217,plain,
or(t7,t5) = ll1,
inference(orient,[status(thm)],[t66690]) ).
cnf(t1218,plain,
or(t7,and(t5,X1)) = and(ll1,or(t7,X1)),
inference(cp,[status(thm)],[t78,t1217]) ).
cnf(t67208,plain,
or(t7,and(t5,X1)) = or(t7,X1),
inference(step,[status(thm)],[t1218,t437]) ).
cnf(t4272,plain,
or(t7,and(t5,X1)) = or(t7,X1),
inference(orient,[status(thm)],[t67208]) ).
cnf(t4278,plain,
or(t7,t1) = or(t7,not(carry)),
inference(cp,[status(thm)],[t4272,t269]) ).
cnf(t4305,plain,
or(t7,not(carry)) = or(t7,t1),
inference(orient,[status(thm)],[t4278]) ).
cnf(t4315,plain,
and(not(t7),carry) = not(or(t7,t1)),
inference(cp,[status(thm)],[t573,t4305]) ).
cnf(t67687,plain,
and(carry,not(t7)) = not(or(t7,t1)),
inference(step,[status(thm)],[t4315,t45]) ).
cnf(t11347,plain,
not(or(t7,t1)) = and(carry,not(t7)),
inference(orient,[status(thm)],[t67687]) ).
cnf(t1829,plain,
and(not(X1),X2) = and(not(X1),or(X1,X2)),
inference(cp,[status(thm)],[t1814,t40]) ).
cnf(t3700,plain,
and(not(X1),or(X1,X2)) = and(not(X1),X2),
inference(orient,[status(thm)],[t1829]) ).
cnf(t165,plain,
or(X1,and(X2,X3)) = and(or(X2,X1),or(X1,X3)),
inference(cp,[status(thm)],[t78,t164]) ).
cnf(t11488,plain,
and(or(X1,X2),or(X2,X3)) = or(X2,and(X1,X3)),
inference(orient,[status(thm)],[t165]) ).
cnf(t1672,plain,
t4 = and(t4,t1),
inference(cp,[status(thm)],[t38,t1671]) ).
cnf(t1676,plain,
and(t4,t1) = t4,
inference(orient,[status(thm)],[t1672]) ).
cnf(t2142,plain,
or(t5,t1) = or(t5,t4),
inference(cp,[status(thm)],[t2140,t1676]) ).
cnf(t66827,plain,
or(t5,t1) = ll1,
inference(step,[status(thm)],[t2142,t1205]) ).
cnf(t2156,plain,
or(t5,t1) = ll1,
inference(orient,[status(thm)],[t66827]) ).
cnf(t11727,plain,
or(t1,and(t5,X1)) = and(ll1,or(t1,X1)),
inference(cp,[status(thm)],[t11488,t2156]) ).
cnf(t67731,plain,
or(t1,and(t5,X1)) = or(t1,X1),
inference(step,[status(thm)],[t11727,t437]) ).
cnf(t13389,plain,
or(t1,and(t5,X1)) = or(t1,X1),
inference(orient,[status(thm)],[t67731]) ).
cnf(t13394,plain,
or(t1,cin) = or(t1,not(t7)),
inference(cp,[status(thm)],[t13389,t264]) ).
cnf(t13425,plain,
or(t1,not(t7)) = or(t1,cin),
inference(orient,[status(thm)],[t13394]) ).
cnf(t13428,plain,
and(not(t1),not(t7)) = and(not(t1),or(t1,cin)),
inference(cp,[status(thm)],[t3700,t13425]) ).
cnf(t67802,plain,
not(or(t1,t7)) = and(not(t1),or(t1,cin)),
inference(step,[status(thm)],[t13428,t69]) ).
cnf(t67803,plain,
not(or(t7,t1)) = and(not(t1),or(t1,cin)),
inference(step,[status(thm)],[t67802,t164]) ).
cnf(t67804,plain,
and(carry,not(t7)) = and(not(t1),or(t1,cin)),
inference(step,[status(thm)],[t67803,t11347]) ).
cnf(t67805,plain,
and(carry,not(t7)) = and(not(t1),cin),
inference(step,[status(thm)],[t67804,t3700]) ).
cnf(t67806,plain,
and(carry,not(t7)) = and(cin,not(t1)),
inference(step,[status(thm)],[t67805,t45]) ).
cnf(t14646,plain,
and(carry,not(t7)) = and(cin,not(t1)),
inference(orient,[status(thm)],[t67806]) ).
cnf(t67807,plain,
not(or(t7,t1)) = and(cin,not(t1)),
inference(step,[status(thm)],[t11347,t14646]) ).
cnf(t14647,plain,
not(or(t7,t1)) = and(cin,not(t1)),
inference(orient,[status(thm)],[t67807]) ).
cnf(t67851,plain,
and(sum,not(t1)) = and(cin,not(t1)),
inference(step,[status(thm)],[t67850,t14647]) ).
cnf(t15940,plain,
and(cin,not(t1)) = and(sum,not(t1)),
inference(orient,[status(thm)],[t67851]) ).
cnf(t270,plain,
and(t5,or(t1,X1)) = or(not(carry),and(t5,X1)),
inference(cp,[status(thm)],[t57,t269]) ).
cnf(t16901,plain,
or(not(carry),and(t5,X1)) = and(t5,or(t1,X1)),
inference(orient,[status(thm)],[t270]) ).
cnf(t283,plain,
t5 = or(t5,not(t6)),
inference(cp,[status(thm)],[t42,t279]) ).
cnf(t345,plain,
or(t5,not(t6)) = t5,
inference(orient,[status(thm)],[t283]) ).
cnf(t577,plain,
and(not(t5),t6) = not(t5),
inference(cp,[status(thm)],[t573,t345]) ).
cnf(t66586,plain,
and(t6,not(t5)) = not(t5),
inference(step,[status(thm)],[t577,t45]) ).
cnf(t617,plain,
and(t6,not(t5)) = not(t5),
inference(orient,[status(thm)],[t66586]) ).
cnf(t1631,plain,
and(not(sum),not(t5)) = and(t7,not(t5)),
inference(cp,[status(thm)],[t1627,t617]) ).
cnf(t66804,plain,
not(or(sum,t5)) = and(t7,not(t5)),
inference(step,[status(thm)],[t1631,t69]) ).
cnf(t66805,plain,
not(or(t5,sum)) = and(t7,not(t5)),
inference(step,[status(thm)],[t66804,t164]) ).
cnf(t66806,plain,
not(or(t5,sum)) = not(t5),
inference(step,[status(thm)],[t66805,t623]) ).
cnf(t1986,plain,
not(or(t5,sum)) = not(t5),
inference(orient,[status(thm)],[t66806]) ).
cnf(t1992,plain,
or(t5,sum) = not(not(t5)),
inference(cp,[status(thm)],[t40,t1986]) ).
cnf(t66807,plain,
or(t5,sum) = t5,
inference(step,[status(thm)],[t1992,t40]) ).
cnf(t2004,plain,
or(t5,sum) = t5,
inference(orient,[status(thm)],[t66807]) ).
cnf(t2006,plain,
sum = and(sum,t5),
inference(cp,[status(thm)],[t825,t2004]) ).
cnf(t66808,plain,
sum = and(t5,sum),
inference(step,[status(thm)],[t2006,t45]) ).
cnf(t2010,plain,
and(t5,sum) = sum,
inference(orient,[status(thm)],[t66808]) ).
cnf(t16905,plain,
and(t5,or(t1,sum)) = or(not(carry),sum),
inference(cp,[status(thm)],[t16901,t2010]) ).
cnf(t265,plain,
and(t5,or(cin,X1)) = or(not(t7),and(t5,X1)),
inference(cp,[status(thm)],[t57,t264]) ).
cnf(t16716,plain,
or(not(t7),and(t5,X1)) = and(t5,or(cin,X1)),
inference(orient,[status(thm)],[t265]) ).
cnf(t445,plain,
and(t5,t1) = and(t5,not(carry)),
inference(cp,[status(thm)],[t438,t269]) ).
cnf(t66555,plain,
not(carry) = and(t5,not(carry)),
inference(step,[status(thm)],[t445,t269]) ).
cnf(t479,plain,
and(t5,not(carry)) = not(carry),
inference(orient,[status(thm)],[t66555]) ).
cnf(t16722,plain,
and(t5,or(cin,not(carry))) = or(not(t7),not(carry)),
inference(cp,[status(thm)],[t16716,t479]) ).
cnf(t1145,plain,
or(t5,cin) = or(t5,not(t5)),
inference(cp,[status(thm)],[t1140,t928]) ).
cnf(t66695,plain,
or(t5,cin) = ll1,
inference(step,[status(thm)],[t1145,t167]) ).
cnf(t1232,plain,
or(t5,cin) = ll1,
inference(orient,[status(thm)],[t66695]) ).
cnf(t11732,plain,
or(cin,and(t5,X1)) = and(ll1,or(cin,X1)),
inference(cp,[status(thm)],[t11488,t1232]) ).
cnf(t67732,plain,
or(cin,and(t5,X1)) = or(cin,X1),
inference(step,[status(thm)],[t11732,t437]) ).
cnf(t13490,plain,
or(cin,and(t5,X1)) = or(cin,X1),
inference(orient,[status(thm)],[t67732]) ).
cnf(t13494,plain,
or(cin,t1) = or(cin,not(carry)),
inference(cp,[status(thm)],[t13490,t269]) ).
cnf(t67733,plain,
or(t1,cin) = or(cin,not(carry)),
inference(step,[status(thm)],[t13494,t164]) ).
cnf(t13549,plain,
or(cin,not(carry)) = or(t1,cin),
inference(orient,[status(thm)],[t67733]) ).
cnf(t11561,plain,
or(t1,and(t6,X1)) = and(ll1,or(t1,X1)),
inference(cp,[status(thm)],[t11488,t1744]) ).
cnf(t67726,plain,
or(t1,and(t6,X1)) = or(t1,X1),
inference(step,[status(thm)],[t11561,t437]) ).
cnf(t12698,plain,
or(t1,and(t6,X1)) = or(t1,X1),
inference(orient,[status(thm)],[t67726]) ).
cnf(t2460,plain,
and(t6,not(t7)) = and(t6,not(not(sum))),
inference(cp,[status(thm)],[t2445,t284]) ).
cnf(t1519,plain,
and(not(t6),not(t7)) = and(t5,ll0),
inference(cp,[status(thm)],[t1514,t520]) ).
cnf(t66736,plain,
not(or(t6,t7)) = and(t5,ll0),
inference(step,[status(thm)],[t1519,t69]) ).
cnf(t66737,plain,
not(or(t7,t6)) = and(t5,ll0),
inference(step,[status(thm)],[t66736,t164]) ).
cnf(t66738,plain,
not(or(t7,t6)) = ll0,
inference(step,[status(thm)],[t66737,t67]) ).
cnf(t1536,plain,
not(or(t7,t6)) = ll0,
inference(orient,[status(thm)],[t66738]) ).
cnf(t1537,plain,
ll1 = xor(or(t7,t6),ll0),
inference(cp,[status(thm)],[t294,t1536]) ).
cnf(t66739,plain,
ll1 = or(t7,t6),
inference(step,[status(thm)],[t1537,t247]) ).
cnf(t1552,plain,
or(t7,t6) = ll1,
inference(orient,[status(thm)],[t66739]) ).
cnf(t1856,plain,
and(not(t7),t6) = xor(t7,ll1),
inference(cp,[status(thm)],[t1845,t1552]) ).
cnf(t66782,plain,
and(t6,not(t7)) = xor(t7,ll1),
inference(step,[status(thm)],[t1856,t45]) ).
cnf(t66783,plain,
and(t6,not(t7)) = not(t7),
inference(step,[status(thm)],[t66782,t370]) ).
cnf(t1868,plain,
and(t6,not(t7)) = not(t7),
inference(orient,[status(thm)],[t66783]) ).
cnf(t66872,plain,
not(t7) = and(t6,not(not(sum))),
inference(step,[status(thm)],[t2460,t1868]) ).
cnf(t66873,plain,
not(t7) = and(t6,sum),
inference(step,[status(thm)],[t66872,t40]) ).
cnf(t2513,plain,
and(t6,sum) = not(t7),
inference(orient,[status(thm)],[t66873]) ).
cnf(t12701,plain,
or(t1,sum) = or(t1,not(t7)),
inference(cp,[status(thm)],[t12698,t2513]) ).
cnf(t67777,plain,
or(t1,sum) = or(t1,cin),
inference(step,[status(thm)],[t12701,t13425]) ).
cnf(t14221,plain,
or(t1,cin) = or(t1,sum),
inference(orient,[status(thm)],[t67777]) ).
cnf(t67780,plain,
or(cin,not(carry)) = or(t1,sum),
inference(step,[status(thm)],[t13549,t14221]) ).
cnf(t14224,plain,
or(cin,not(carry)) = or(t1,sum),
inference(orient,[status(thm)],[t67780]) ).
cnf(t67884,plain,
and(t5,or(t1,sum)) = or(not(t7),not(carry)),
inference(step,[status(thm)],[t16722,t14224]) ).
cnf(t67885,plain,
and(t5,or(t1,sum)) = not(and(t7,carry)),
inference(step,[status(thm)],[t67884,t87]) ).
cnf(t16767,plain,
and(t5,or(t1,sum)) = not(and(t7,carry)),
inference(orient,[status(thm)],[t67885]) ).
cnf(t67893,plain,
not(and(t7,carry)) = or(not(carry),sum),
inference(step,[status(thm)],[t16905,t16767]) ).
cnf(t67894,plain,
not(and(t7,carry)) = or(sum,not(carry)),
inference(step,[status(thm)],[t67893,t164]) ).
cnf(t16951,plain,
not(and(t7,carry)) = or(sum,not(carry)),
inference(orient,[status(thm)],[t67894]) ).
cnf(t16977,plain,
and(carry,not(t7)) = and(carry,or(sum,not(carry))),
inference(cp,[status(thm)],[t2445,t16951]) ).
cnf(t67854,plain,
and(carry,not(t7)) = and(sum,not(t1)),
inference(step,[status(thm)],[t14646,t15940]) ).
cnf(t15943,plain,
and(carry,not(t7)) = and(sum,not(t1)),
inference(orient,[status(thm)],[t67854]) ).
cnf(t67903,plain,
and(sum,not(t1)) = and(carry,or(sum,not(carry))),
inference(step,[status(thm)],[t16977,t15943]) ).
cnf(t67904,plain,
and(sum,not(t1)) = and(carry,sum),
inference(step,[status(thm)],[t67903,t1104]) ).
cnf(t67905,plain,
and(sum,not(t1)) = and(sum,carry),
inference(step,[status(thm)],[t67904,t45]) ).
cnf(t17037,plain,
and(sum,not(t1)) = and(sum,carry),
inference(orient,[status(thm)],[t67905]) ).
cnf(t67912,plain,
and(cin,not(t1)) = and(sum,carry),
inference(step,[status(thm)],[t15940,t17037]) ).
cnf(t17044,plain,
and(cin,not(t1)) = and(sum,carry),
inference(orient,[status(thm)],[t67912]) ).
cnf(t68198,plain,
and(cin,not(t1)) = and(sum_def,carry),
inference(step,[status(thm)],[t17044,t25967]) ).
cnf(t26004,plain,
and(cin,not(t1)) = and(sum_def,carry),
inference(orient,[status(thm)],[t68198]) ).
cnf(t28661,plain,
and(cin,not(not(t1))) = xor(cin,and(sum_def,carry)),
inference(cp,[status(thm)],[t28646,t26004]) ).
cnf(t69801,plain,
and(cin,t1) = xor(cin,and(sum_def,carry)),
inference(step,[status(thm)],[t28661,t40]) ).
cnf(t69802,plain,
and(t1,cin) = xor(cin,and(sum_def,carry)),
inference(step,[status(thm)],[t69801,t45]) ).
cnf(t59018,plain,
xor(cin,and(sum_def,carry)) = and(t1,cin),
inference(orient,[status(thm)],[t69802]) ).
cnf(t827,plain,
X1 = and(X1,or(X2,or(X3,X1))),
inference(cp,[status(thm)],[t825,t179]) ).
cnf(t5748,plain,
and(X1,or(X2,or(X3,X1))) = X1,
inference(orient,[status(thm)],[t827]) ).
cnf(t5754,plain,
and(X1,X2) = and(and(X1,X2),or(X3,X1)),
inference(cp,[status(thm)],[t5748,t42]) ).
cnf(t69553,plain,
and(X1,X2) = and(X1,and(X2,or(X3,X1))),
inference(step,[status(thm)],[t5754,t46]) ).
cnf(t54004,plain,
and(X1,and(X2,or(X3,X1))) = and(X1,X2),
inference(orient,[status(thm)],[t69553]) ).
cnf(f25,negated_conjecture,
or(and(cin,or(a,b)),and(not(cin),and(a,b))) = carry_def,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',carry_def) ).
fof(f25_nnf,plain,
or(and(cin,or(a,b)),and(not(cin),and(a,b))) = carry_def,
inference(nnf_transformation,[status(thm)],[f25]) ).
cnf(c25,plain,
or(and(cin,or(a,b)),and(not(cin),and(a,b))) = carry_def,
inference(cnf_transformation,[status(esa)],[f25_nnf]) ).
cnf(t36,plain,
or(and(cin,or(a,b)),and(not(cin),and(a,b))) = carry_def,
inference(equality_encoding,[status(esa)],[c25]) ).
cnf(t66508,plain,
or(and(cin,or(b,a)),and(not(cin),and(a,b))) = carry_def,
inference(step,[status(thm)],[t36,t164]) ).
cnf(t66509,plain,
or(and(cin,or(b,a)),and(not(cin),and(b,a))) = carry_def,
inference(step,[status(thm)],[t66508,t45]) ).
cnf(t232,plain,
or(and(cin,or(b,a)),and(not(cin),and(b,a))) = carry_def,
inference(orient,[status(thm)],[t66509]) ).
cnf(t235,plain,
or(and(cin,or(b,a)),and(and(not(cin),and(b,a)),X1)) = and(carry_def,or(and(cin,or(b,a)),X1)),
inference(cp,[status(thm)],[t78,t232]) ).
cnf(t69993,plain,
or(and(cin,or(t4,carry)),and(and(not(cin),and(b,a)),X1)) = and(carry_def,or(and(cin,or(b,a)),X1)),
inference(step,[status(thm)],[t235,t7473]) ).
cnf(t452,plain,
and(X1,or(X2,and(X1,X3))) = or(and(X1,X2),and(X1,X3)),
inference(cp,[status(thm)],[t57,t438]) ).
cnf(t69068,plain,
and(X1,or(X2,and(X1,X3))) = and(X1,or(X2,X3)),
inference(step,[status(thm)],[t452,t57]) ).
cnf(t39458,plain,
and(X1,or(X2,and(X1,X3))) = and(X1,or(X2,X3)),
inference(orient,[status(thm)],[t69068]) ).
cnf(t39637,plain,
and(cin,or(X1,not(t6))) = and(cin,or(X1,ll0)),
inference(cp,[status(thm)],[t39458,t1529]) ).
cnf(t69074,plain,
and(cin,or(X1,not(t6))) = and(cin,X1),
inference(step,[status(thm)],[t39637,t43]) ).
cnf(t40024,plain,
and(cin,or(X1,not(t6))) = and(cin,X1),
inference(orient,[status(thm)],[t69074]) ).
cnf(t273,plain,
t5 = or(t5,not(carry)),
inference(cp,[status(thm)],[t42,t269]) ).
cnf(t337,plain,
or(t5,not(carry)) = t5,
inference(orient,[status(thm)],[t273]) ).
cnf(t579,plain,
and(not(t5),carry) = not(t5),
inference(cp,[status(thm)],[t573,t337]) ).
cnf(t66588,plain,
and(carry,not(t5)) = not(t5),
inference(step,[status(thm)],[t579,t45]) ).
cnf(t629,plain,
and(carry,not(t5)) = not(t5),
inference(orient,[status(thm)],[t66588]) ).
cnf(t1147,plain,
or(t5,carry) = or(t5,not(t5)),
inference(cp,[status(thm)],[t1140,t629]) ).
cnf(t66685,plain,
or(t5,carry) = ll1,
inference(step,[status(thm)],[t1147,t167]) ).
cnf(t1208,plain,
or(t5,carry) = ll1,
inference(orient,[status(thm)],[t66685]) ).
cnf(t11733,plain,
or(carry,and(t5,X1)) = and(ll1,or(carry,X1)),
inference(cp,[status(thm)],[t11488,t1208]) ).
cnf(t67706,plain,
or(carry,and(t5,X1)) = or(carry,X1),
inference(step,[status(thm)],[t11733,t437]) ).
cnf(t12364,plain,
or(carry,and(t5,X1)) = or(carry,X1),
inference(orient,[status(thm)],[t67706]) ).
cnf(t12370,plain,
or(carry,t4) = or(carry,not(t6)),
inference(cp,[status(thm)],[t12364,t279]) ).
cnf(t67707,plain,
or(t4,carry) = or(carry,not(t6)),
inference(step,[status(thm)],[t12370,t164]) ).
cnf(t12401,plain,
or(carry,not(t6)) = or(t4,carry),
inference(orient,[status(thm)],[t67707]) ).
cnf(t40025,plain,
and(cin,carry) = and(cin,or(t4,carry)),
inference(cp,[status(thm)],[t40024,t12401]) ).
cnf(t40276,plain,
and(cin,or(t4,carry)) = and(cin,carry),
inference(orient,[status(thm)],[t40025]) ).
cnf(t69994,plain,
or(and(cin,carry),and(and(not(cin),and(b,a)),X1)) = and(carry_def,or(and(cin,or(b,a)),X1)),
inference(step,[status(thm)],[t69993,t40276]) ).
cnf(t69995,plain,
or(and(cin,carry),and(not(cin),and(and(b,a),X1))) = and(carry_def,or(and(cin,or(b,a)),X1)),
inference(step,[status(thm)],[t69994,t46]) ).
cnf(t69996,plain,
or(and(cin,carry),and(not(cin),and(b,and(a,X1)))) = and(carry_def,or(and(cin,or(b,a)),X1)),
inference(step,[status(thm)],[t69995,t46]) ).
cnf(t251,plain,
and(b,and(a,X1)) = and(not(t1),X1),
inference(cp,[status(thm)],[t46,t248]) ).
cnf(t1327,plain,
and(b,and(a,X1)) = and(not(t1),X1),
inference(orient,[status(thm)],[t251]) ).
cnf(t69997,plain,
or(and(cin,carry),and(not(cin),and(not(t1),X1))) = and(carry_def,or(and(cin,or(b,a)),X1)),
inference(step,[status(thm)],[t69996,t1327]) ).
cnf(t76,plain,
and(not(X1),and(not(X2),X3)) = and(not(or(X1,X2)),X3),
inference(cp,[status(thm)],[t46,t69]) ).
cnf(t6433,plain,
and(not(X1),and(not(X2),X3)) = and(not(or(X1,X2)),X3),
inference(orient,[status(thm)],[t76]) ).
cnf(t69998,plain,
or(and(cin,carry),and(not(or(cin,t1)),X1)) = and(carry_def,or(and(cin,or(b,a)),X1)),
inference(step,[status(thm)],[t69997,t6433]) ).
cnf(t69999,plain,
or(and(cin,carry),and(not(or(t1,cin)),X1)) = and(carry_def,or(and(cin,or(b,a)),X1)),
inference(step,[status(thm)],[t69998,t164]) ).
cnf(t68190,plain,
or(t1,cin) = or(t1,sum_def),
inference(step,[status(thm)],[t14221,t25967]) ).
cnf(t25996,plain,
or(t1,cin) = or(t1,sum_def),
inference(orient,[status(thm)],[t68190]) ).
cnf(t70000,plain,
or(and(cin,carry),and(not(or(t1,sum_def)),X1)) = and(carry_def,or(and(cin,or(b,a)),X1)),
inference(step,[status(thm)],[t69999,t25996]) ).
cnf(t296,plain,
xor(X1,xor(not(X1),X2)) = xor(ll1,X2),
inference(cp,[status(thm)],[t238,t294]) ).
cnf(t2363,plain,
xor(X1,xor(not(X1),X2)) = xor(ll1,X2),
inference(orient,[status(thm)],[t296]) ).
cnf(t27060,plain,
xor(ll1,or(X1,X2)) = xor(X1,or(X1,not(X2))),
inference(cp,[status(thm)],[t2363,t26830]) ).
cnf(t68434,plain,
xor(ll1,or(X1,X2)) = and(not(X1),not(X2)),
inference(step,[status(thm)],[t27060,t1845]) ).
cnf(t68435,plain,
xor(ll1,or(X1,X2)) = not(or(X1,X2)),
inference(step,[status(thm)],[t68434,t69]) ).
cnf(t27811,plain,
xor(ll1,or(X1,X2)) = not(or(X1,X2)),
inference(orient,[status(thm)],[t68435]) ).
cnf(t68188,plain,
or(cin,not(carry)) = or(t1,sum_def),
inference(step,[status(thm)],[t14224,t25967]) ).
cnf(t25994,plain,
or(cin,not(carry)) = or(t1,sum_def),
inference(orient,[status(thm)],[t68188]) ).
cnf(t27855,plain,
not(or(cin,not(carry))) = xor(ll1,or(t1,sum_def)),
inference(cp,[status(thm)],[t27811,t25994]) ).
cnf(t68454,plain,
and(not(cin),carry) = xor(ll1,or(t1,sum_def)),
inference(step,[status(thm)],[t27855,t573]) ).
cnf(t68455,plain,
and(carry,not(cin)) = xor(ll1,or(t1,sum_def)),
inference(step,[status(thm)],[t68454,t45]) ).
cnf(t2667,plain,
and(carry,not(t1)) = and(carry,t5),
inference(cp,[status(thm)],[t2445,t2657]) ).
cnf(t66927,plain,
not(t1) = and(carry,t5),
inference(step,[status(thm)],[t2667,t963]) ).
cnf(t66928,plain,
not(t1) = and(t5,carry),
inference(step,[status(thm)],[t66927,t45]) ).
cnf(t2687,plain,
and(t5,carry) = not(t1),
inference(orient,[status(thm)],[t66928]) ).
cnf(t13491,plain,
or(cin,carry) = or(cin,not(t1)),
inference(cp,[status(thm)],[t13490,t2687]) ).
cnf(t13525,plain,
or(cin,not(t1)) = or(cin,carry),
inference(orient,[status(thm)],[t13491]) ).
cnf(t13528,plain,
and(not(cin),not(t1)) = and(not(cin),or(cin,carry)),
inference(cp,[status(thm)],[t3700,t13525]) ).
cnf(t67809,plain,
not(or(cin,t1)) = and(not(cin),or(cin,carry)),
inference(step,[status(thm)],[t13528,t69]) ).
cnf(t67810,plain,
not(or(t1,cin)) = and(not(cin),or(cin,carry)),
inference(step,[status(thm)],[t67809,t164]) ).
cnf(t67811,plain,
not(or(t1,sum)) = and(not(cin),or(cin,carry)),
inference(step,[status(thm)],[t67810,t14221]) ).
cnf(t1118,plain,
and(not(X1),X2) = and(not(X1),or(X2,X1)),
inference(cp,[status(thm)],[t1104,t40]) ).
cnf(t3022,plain,
and(not(X1),or(X2,X1)) = and(not(X1),X2),
inference(orient,[status(thm)],[t1118]) ).
cnf(t3042,plain,
and(not(t1),t6) = and(not(t1),ll1),
inference(cp,[status(thm)],[t3022,t1744]) ).
cnf(t66953,plain,
and(t6,not(t1)) = and(not(t1),ll1),
inference(step,[status(thm)],[t3042,t45]) ).
cnf(t66954,plain,
and(t6,not(t1)) = not(t1),
inference(step,[status(thm)],[t66953,t39]) ).
cnf(t3081,plain,
and(t6,not(t1)) = not(t1),
inference(orient,[status(thm)],[t66954]) ).
cnf(t3084,plain,
and(not(sum),not(t1)) = and(t7,not(t1)),
inference(cp,[status(thm)],[t1627,t3081]) ).
cnf(t67660,plain,
not(or(sum,t1)) = and(t7,not(t1)),
inference(step,[status(thm)],[t3084,t69]) ).
cnf(t67661,plain,
not(or(t1,sum)) = and(t7,not(t1)),
inference(step,[status(thm)],[t67660,t164]) ).
cnf(t11152,plain,
not(or(t1,sum)) = and(t7,not(t1)),
inference(orient,[status(thm)],[t67661]) ).
cnf(t67812,plain,
and(t7,not(t1)) = and(not(cin),or(cin,carry)),
inference(step,[status(thm)],[t67811,t11152]) ).
cnf(t67813,plain,
and(t7,not(t1)) = and(not(cin),carry),
inference(step,[status(thm)],[t67812,t3700]) ).
cnf(t67814,plain,
and(t7,not(t1)) = and(carry,not(cin)),
inference(step,[status(thm)],[t67813,t45]) ).
cnf(t14676,plain,
and(carry,not(cin)) = and(t7,not(t1)),
inference(orient,[status(thm)],[t67814]) ).
cnf(t68456,plain,
and(t7,not(t1)) = xor(ll1,or(t1,sum_def)),
inference(step,[status(thm)],[t68455,t14676]) ).
cnf(t68457,plain,
and(t7,not(t1)) = not(or(t1,sum_def)),
inference(step,[status(thm)],[t68456,t27811]) ).
cnf(t27926,plain,
not(or(t1,sum_def)) = and(t7,not(t1)),
inference(orient,[status(thm)],[t68457]) ).
cnf(t70001,plain,
or(and(cin,carry),and(and(t7,not(t1)),X1)) = and(carry_def,or(and(cin,or(b,a)),X1)),
inference(step,[status(thm)],[t70000,t27926]) ).
cnf(t70002,plain,
or(and(cin,carry),and(t7,and(not(t1),X1))) = and(carry_def,or(and(cin,or(b,a)),X1)),
inference(step,[status(thm)],[t70001,t46]) ).
cnf(t70003,plain,
or(and(cin,carry),and(t7,and(not(t1),X1))) = and(carry_def,or(and(cin,or(t4,carry)),X1)),
inference(step,[status(thm)],[t70002,t7473]) ).
cnf(t70004,plain,
or(and(cin,carry),and(t7,and(not(t1),X1))) = and(carry_def,or(and(cin,carry),X1)),
inference(step,[status(thm)],[t70003,t40276]) ).
cnf(t63059,plain,
or(and(cin,carry),and(t7,and(not(t1),X1))) = and(carry_def,or(and(cin,carry),X1)),
inference(orient,[status(thm)],[t70004]) ).
cnf(t63111,plain,
and(carry_def,or(and(cin,carry),not(not(t1)))) = or(and(cin,carry),and(t7,ll0)),
inference(cp,[status(thm)],[t63059,t54]) ).
cnf(t70005,plain,
and(carry_def,or(and(cin,carry),t1)) = or(and(cin,carry),and(t7,ll0)),
inference(step,[status(thm)],[t63111,t40]) ).
cnf(t70006,plain,
and(carry_def,or(t1,and(cin,carry))) = or(and(cin,carry),and(t7,ll0)),
inference(step,[status(thm)],[t70005,t164]) ).
cnf(t184,plain,
or(X1,or(X1,X2)) = or(X1,X2),
inference(cp,[status(thm)],[t179,t41]) ).
cnf(t537,plain,
or(X1,or(X1,X2)) = or(X1,X2),
inference(orient,[status(thm)],[t184]) ).
cnf(t541,plain,
or(X1,and(or(X1,X2),X3)) = and(or(X1,X2),or(X1,X3)),
inference(cp,[status(thm)],[t78,t537]) ).
cnf(t69094,plain,
or(X1,and(or(X1,X2),X3)) = or(X1,and(X2,X3)),
inference(step,[status(thm)],[t541,t78]) ).
cnf(t40507,plain,
or(X1,and(or(X1,X2),X3)) = or(X1,and(X2,X3)),
inference(orient,[status(thm)],[t69094]) ).
cnf(t40996,plain,
or(t1,and(cin,X1)) = or(t1,and(or(t1,sum_def),X1)),
inference(cp,[status(thm)],[t40507,t25996]) ).
cnf(t69503,plain,
or(t1,and(cin,X1)) = or(t1,and(sum_def,X1)),
inference(step,[status(thm)],[t40996,t40507]) ).
cnf(t52712,plain,
or(t1,and(cin,X1)) = or(t1,and(sum_def,X1)),
inference(orient,[status(thm)],[t69503]) ).
cnf(t70007,plain,
and(carry_def,or(t1,and(sum_def,carry))) = or(and(cin,carry),and(t7,ll0)),
inference(step,[status(thm)],[t70006,t52712]) ).
cnf(t1148,plain,
or(t1,carry) = or(t1,not(t1)),
inference(cp,[status(thm)],[t1140,t963]) ).
cnf(t66697,plain,
or(t1,carry) = ll1,
inference(step,[status(thm)],[t1148,t167]) ).
cnf(t1238,plain,
or(t1,carry) = ll1,
inference(orient,[status(thm)],[t66697]) ).
cnf(t1240,plain,
or(t1,and(X1,carry)) = and(or(t1,X1),ll1),
inference(cp,[status(thm)],[t78,t1238]) ).
cnf(t67957,plain,
or(t1,and(X1,carry)) = or(t1,X1),
inference(step,[status(thm)],[t1240,t39]) ).
cnf(t18980,plain,
or(t1,and(X1,carry)) = or(t1,X1),
inference(orient,[status(thm)],[t67957]) ).
cnf(t70008,plain,
and(carry_def,or(t1,sum_def)) = or(and(cin,carry),and(t7,ll0)),
inference(step,[status(thm)],[t70007,t18980]) ).
cnf(t70009,plain,
and(carry_def,or(t1,sum_def)) = or(and(t7,ll0),and(cin,carry)),
inference(step,[status(thm)],[t70008,t164]) ).
cnf(t70010,plain,
and(carry_def,or(t1,sum_def)) = or(ll0,and(cin,carry)),
inference(step,[status(thm)],[t70009,t67]) ).
cnf(t70011,plain,
and(carry_def,or(t1,sum_def)) = and(cin,carry),
inference(step,[status(thm)],[t70010,t436]) ).
cnf(t63163,plain,
and(carry_def,or(t1,sum_def)) = and(cin,carry),
inference(orient,[status(thm)],[t70011]) ).
cnf(t63176,plain,
and(sum_def,carry_def) = and(sum_def,and(cin,carry)),
inference(cp,[status(thm)],[t54004,t63163]) ).
cnf(t6826,plain,
xor(X1,not(and(not(X2),X1))) = not(and(X1,X2)),
inference(cp,[status(thm)],[t784,t6776]) ).
cnf(t68938,plain,
xor(X1,or(X2,not(X1))) = not(and(X1,X2)),
inference(step,[status(thm)],[t6826,t689]) ).
cnf(t36598,plain,
xor(X1,or(X2,not(X1))) = not(and(X1,X2)),
inference(orient,[status(thm)],[t68938]) ).
cnf(t13435,plain,
or(t1,not(not(t7))) = xor(t1,not(or(t1,cin))),
inference(cp,[status(thm)],[t10210,t13425]) ).
cnf(t67782,plain,
or(t1,t7) = xor(t1,not(or(t1,cin))),
inference(step,[status(thm)],[t13435,t40]) ).
cnf(t67783,plain,
or(t7,t1) = xor(t1,not(or(t1,cin))),
inference(step,[status(thm)],[t67782,t164]) ).
cnf(t67784,plain,
or(t7,t1) = or(t1,not(cin)),
inference(step,[status(thm)],[t67783,t10210]) ).
cnf(t14248,plain,
or(t1,not(cin)) = or(t7,t1),
inference(orient,[status(thm)],[t67784]) ).
cnf(t36716,plain,
not(and(cin,t1)) = xor(cin,or(t7,t1)),
inference(cp,[status(thm)],[t36598,t14248]) ).
cnf(t69053,plain,
not(and(t1,cin)) = xor(cin,or(t7,t1)),
inference(step,[status(thm)],[t36716,t45]) ).
cnf(t38866,plain,
xor(cin,or(t7,t1)) = not(and(t1,cin)),
inference(orient,[status(thm)],[t69053]) ).
cnf(t38869,plain,
and(cin,not(or(t7,t1))) = and(cin,not(and(t1,cin))),
inference(cp,[status(thm)],[t11435,t38866]) ).
cnf(t67852,plain,
not(or(t7,t1)) = and(sum,not(t1)),
inference(step,[status(thm)],[t14647,t15940]) ).
cnf(t15941,plain,
not(or(t7,t1)) = and(sum,not(t1)),
inference(orient,[status(thm)],[t67852]) ).
cnf(t67906,plain,
not(or(t7,t1)) = and(sum,carry),
inference(step,[status(thm)],[t15941,t17037]) ).
cnf(t17038,plain,
not(or(t7,t1)) = and(sum,carry),
inference(orient,[status(thm)],[t67906]) ).
cnf(t68184,plain,
not(or(t7,t1)) = and(sum_def,carry),
inference(step,[status(thm)],[t17038,t25967]) ).
cnf(t25990,plain,
not(or(t7,t1)) = and(sum_def,carry),
inference(orient,[status(thm)],[t68184]) ).
cnf(t69839,plain,
and(cin,and(sum_def,carry)) = and(cin,not(and(t1,cin))),
inference(step,[status(thm)],[t38869,t25990]) ).
cnf(t52,plain,
and(X1,and(X2,X3)) = and(and(X2,X1),X3),
inference(cp,[status(thm)],[t46,t45]) ).
cnf(t66615,plain,
and(X1,and(X2,X3)) = and(X2,and(X1,X3)),
inference(step,[status(thm)],[t52,t46]) ).
cnf(t819,plain,
and(X1,and(X2,X3)) = and(X2,and(X1,X3)),
inference(orient,[status(thm)],[t66615]) ).
cnf(t69840,plain,
and(sum_def,and(cin,carry)) = and(cin,not(and(t1,cin))),
inference(step,[status(thm)],[t69839,t819]) ).
cnf(t69841,plain,
and(sum_def,and(cin,carry)) = and(cin,not(t1)),
inference(step,[status(thm)],[t69840,t2445]) ).
cnf(t69842,plain,
and(sum_def,and(cin,carry)) = and(sum_def,carry),
inference(step,[status(thm)],[t69841,t26004]) ).
cnf(t59899,plain,
and(sum_def,and(cin,carry)) = and(sum_def,carry),
inference(orient,[status(thm)],[t69842]) ).
cnf(t70012,plain,
and(sum_def,carry_def) = and(sum_def,carry),
inference(step,[status(thm)],[t63176,t59899]) ).
cnf(t63199,plain,
and(sum_def,carry) = and(sum_def,carry_def),
inference(orient,[status(thm)],[t70012]) ).
cnf(t70037,plain,
xor(cin,and(sum_def,carry_def)) = and(t1,cin),
inference(step,[status(thm)],[t59018,t63199]) ).
cnf(t63266,plain,
xor(cin,and(sum_def,carry_def)) = and(t1,cin),
inference(rw,[status(thm)],[t70037]) ).
cnf(t64319,plain,
xor(cin,and(sum_def,carry_def)) = and(t1,cin),
inference(orient,[status(thm)],[t63266]) ).
cnf(t64324,plain,
and(cin,not(and(sum_def,carry_def))) = and(cin,and(t1,cin)),
inference(cp,[status(thm)],[t11435,t64319]) ).
cnf(t67778,plain,
or(t1,not(t7)) = or(t1,sum),
inference(step,[status(thm)],[t13425,t14221]) ).
cnf(t14222,plain,
or(t1,not(t7)) = or(t1,sum),
inference(orient,[status(thm)],[t67778]) ).
cnf(t68186,plain,
or(t1,not(t7)) = or(t1,sum_def),
inference(step,[status(thm)],[t14222,t25967]) ).
cnf(t25992,plain,
or(t1,not(t7)) = or(t1,sum_def),
inference(orient,[status(thm)],[t68186]) ).
cnf(t27027,plain,
or(t1,not(not(t7))) = xor(not(t1),or(t1,sum_def)),
inference(cp,[status(thm)],[t26830,t25992]) ).
cnf(t68412,plain,
or(t1,t7) = xor(not(t1),or(t1,sum_def)),
inference(step,[status(thm)],[t27027,t40]) ).
cnf(t68413,plain,
or(t7,t1) = xor(not(t1),or(t1,sum_def)),
inference(step,[status(thm)],[t68412,t164]) ).
cnf(t68414,plain,
or(t7,t1) = or(t1,not(sum_def)),
inference(step,[status(thm)],[t68413,t26830]) ).
cnf(t27069,plain,
or(t1,not(sum_def)) = or(t7,t1),
inference(orient,[status(thm)],[t68414]) ).
cnf(t27093,plain,
and(not(t1),sum_def) = not(or(t7,t1)),
inference(cp,[status(thm)],[t573,t27069]) ).
cnf(t68424,plain,
and(sum_def,not(t1)) = not(or(t7,t1)),
inference(step,[status(thm)],[t27093,t45]) ).
cnf(t68425,plain,
and(sum_def,not(t1)) = and(sum_def,carry),
inference(step,[status(thm)],[t68424,t25990]) ).
cnf(t27697,plain,
and(sum_def,not(t1)) = and(sum_def,carry),
inference(orient,[status(thm)],[t68425]) ).
cnf(t27720,plain,
or(not(sum_def),t1) = not(and(sum_def,carry)),
inference(cp,[status(thm)],[t708,t27697]) ).
cnf(t68522,plain,
or(t1,not(sum_def)) = not(and(sum_def,carry)),
inference(step,[status(thm)],[t27720,t164]) ).
cnf(t68523,plain,
or(t7,t1) = not(and(sum_def,carry)),
inference(step,[status(thm)],[t68522,t27069]) ).
cnf(t28918,plain,
not(and(sum_def,carry)) = or(t7,t1),
inference(orient,[status(thm)],[t68523]) ).
cnf(t70053,plain,
not(and(sum_def,carry_def)) = or(t7,t1),
inference(step,[status(thm)],[t28918,t63199]) ).
cnf(t63280,plain,
not(and(sum_def,carry_def)) = or(t7,t1),
inference(rw,[status(thm)],[t70053]) ).
cnf(t63447,plain,
not(and(sum_def,carry_def)) = or(t7,t1),
inference(orient,[status(thm)],[t63280]) ).
cnf(t70219,plain,
and(cin,or(t7,t1)) = and(cin,and(t1,cin)),
inference(step,[status(thm)],[t64324,t63447]) ).
cnf(t66,plain,
and(X1,X2) = and(and(X1,X2),and(X1,or(X2,X3))),
inference(cp,[status(thm)],[t38,t57]) ).
cnf(t67124,plain,
and(X1,X2) = and(X1,and(X2,and(X1,or(X2,X3)))),
inference(step,[status(thm)],[t66,t46]) ).
cnf(t3647,plain,
and(X1,and(X2,and(X1,or(X2,X3)))) = and(X1,X2),
inference(orient,[status(thm)],[t67124]) ).
cnf(t16772,plain,
or(carry,or(t1,sum)) = or(carry,not(and(t7,carry))),
inference(cp,[status(thm)],[t12364,t16767]) ).
cnf(t189,plain,
or(X1,or(X2,X3)) = or(or(X2,X1),X3),
inference(cp,[status(thm)],[t179,t164]) ).
cnf(t66638,plain,
or(X1,or(X2,X3)) = or(X2,or(X1,X3)),
inference(step,[status(thm)],[t189,t179]) ).
cnf(t1008,plain,
or(X1,or(X2,X3)) = or(X2,or(X1,X3)),
inference(orient,[status(thm)],[t66638]) ).
cnf(t67886,plain,
or(t1,or(carry,sum)) = or(carry,not(and(t7,carry))),
inference(step,[status(thm)],[t16772,t1008]) ).
cnf(t67887,plain,
or(t1,or(sum,carry)) = or(carry,not(and(t7,carry))),
inference(step,[status(thm)],[t67886,t164]) ).
cnf(t185,plain,
or(X1,or(not(X1),X2)) = or(ll1,X2),
inference(cp,[status(thm)],[t179,t167]) ).
cnf(t157,plain,
not(or(ll1,X1)) = and(ll0,not(X1)),
inference(cp,[status(thm)],[t69,t155]) ).
cnf(t377,plain,
not(or(ll1,X1)) = and(ll0,not(X1)),
inference(orient,[status(thm)],[t157]) ).
cnf(t387,plain,
or(ll1,X1) = not(and(ll0,not(X1))),
inference(cp,[status(thm)],[t40,t377]) ).
cnf(t161,plain,
not(and(ll0,X1)) = or(ll1,not(X1)),
inference(cp,[status(thm)],[t87,t160]) ).
cnf(t396,plain,
not(and(ll0,X1)) = or(ll1,not(X1)),
inference(orient,[status(thm)],[t161]) ).
cnf(t399,plain,
or(ll1,not(X1)) = not(and(X1,ll0)),
inference(cp,[status(thm)],[t396,t45]) ).
cnf(t66538,plain,
or(ll1,not(X1)) = not(ll0),
inference(step,[status(thm)],[t399,t67]) ).
cnf(t66539,plain,
or(ll1,not(X1)) = ll1,
inference(step,[status(thm)],[t66538,t160]) ).
cnf(t410,plain,
or(ll1,not(X1)) = ll1,
inference(orient,[status(thm)],[t66539]) ).
cnf(t66540,plain,
not(and(ll0,X1)) = ll1,
inference(step,[status(thm)],[t396,t410]) ).
cnf(t411,plain,
not(and(ll0,X1)) = ll1,
inference(orient,[status(thm)],[t66540]) ).
cnf(t66670,plain,
or(ll1,X1) = ll1,
inference(step,[status(thm)],[t387,t411]) ).
cnf(t1103,plain,
or(ll1,X1) = ll1,
inference(orient,[status(thm)],[t66670]) ).
cnf(t66710,plain,
or(X1,or(not(X1),X2)) = ll1,
inference(step,[status(thm)],[t185,t1103]) ).
cnf(t1311,plain,
or(X1,or(not(X1),X2)) = ll1,
inference(orient,[status(thm)],[t66710]) ).
cnf(t1314,plain,
ll1 = or(X1,or(X2,not(X1))),
inference(cp,[status(thm)],[t1311,t164]) ).
cnf(t1796,plain,
or(X1,or(X2,not(X1))) = ll1,
inference(orient,[status(thm)],[t1314]) ).
cnf(t1803,plain,
ll1 = or(X1,not(and(X2,X1))),
inference(cp,[status(thm)],[t1796,t87]) ).
cnf(t2410,plain,
or(X1,not(and(X2,X1))) = ll1,
inference(orient,[status(thm)],[t1803]) ).
cnf(t67888,plain,
or(t1,or(sum,carry)) = ll1,
inference(step,[status(thm)],[t67887,t2410]) ).
cnf(t16798,plain,
or(t1,or(sum,carry)) = ll1,
inference(orient,[status(thm)],[t67888]) ).
cnf(t16815,plain,
and(X1,t1) = and(X1,and(t1,and(X1,ll1))),
inference(cp,[status(thm)],[t3647,t16798]) ).
cnf(t67890,plain,
and(X1,t1) = and(X1,and(t1,X1)),
inference(step,[status(thm)],[t16815,t39]) ).
cnf(t16833,plain,
and(X1,and(t1,X1)) = and(X1,t1),
inference(orient,[status(thm)],[t67890]) ).
cnf(t70220,plain,
and(cin,or(t7,t1)) = and(cin,t1),
inference(step,[status(thm)],[t70219,t16833]) ).
cnf(t70221,plain,
and(cin,or(t7,t1)) = and(t1,cin),
inference(step,[status(thm)],[t70220,t45]) ).
cnf(t65914,plain,
and(cin,or(t7,t1)) = and(t1,cin),
inference(orient,[status(thm)],[t70221]) ).
cnf(t65932,plain,
and(t7,cin) = and(t7,and(t1,cin)),
inference(cp,[status(thm)],[t21945,t65914]) ).
cnf(t70222,plain,
not(t5) = and(t7,and(t1,cin)),
inference(step,[status(thm)],[t65932,t2523]) ).
cnf(t63185,plain,
and(t1,carry_def) = and(t1,and(cin,carry)),
inference(cp,[status(thm)],[t21945,t63163]) ).
cnf(t844,plain,
cin = or(cin,not(t7)),
inference(cp,[status(thm)],[t834,t264]) ).
cnf(t878,plain,
or(cin,not(t7)) = cin,
inference(orient,[status(thm)],[t844]) ).
cnf(t879,plain,
not(t7) = and(not(t7),cin),
inference(cp,[status(thm)],[t825,t878]) ).
cnf(t66628,plain,
not(t7) = and(cin,not(t7)),
inference(step,[status(thm)],[t879,t45]) ).
cnf(t948,plain,
and(cin,not(t7)) = not(t7),
inference(orient,[status(thm)],[t66628]) ).
cnf(t1146,plain,
or(t7,cin) = or(t7,not(t7)),
inference(cp,[status(thm)],[t1140,t948]) ).
cnf(t66696,plain,
or(t7,cin) = ll1,
inference(step,[status(thm)],[t1146,t167]) ).
cnf(t1235,plain,
or(t7,cin) = ll1,
inference(orient,[status(thm)],[t66696]) ).
cnf(t1236,plain,
or(t7,and(cin,X1)) = and(ll1,or(t7,X1)),
inference(cp,[status(thm)],[t78,t1235]) ).
cnf(t67956,plain,
or(t7,and(cin,X1)) = or(t7,X1),
inference(step,[status(thm)],[t1236,t437]) ).
cnf(t18948,plain,
or(t7,and(cin,X1)) = or(t7,X1),
inference(orient,[status(thm)],[t67956]) ).
cnf(t26969,plain,
or(t7,not(and(cin,X1))) = xor(not(t7),or(t7,X1)),
inference(cp,[status(thm)],[t26830,t18948]) ).
cnf(t68885,plain,
or(t7,not(and(cin,X1))) = or(t7,not(X1)),
inference(step,[status(thm)],[t26969,t26830]) ).
cnf(t35727,plain,
or(t7,not(and(cin,X1))) = or(t7,not(X1)),
inference(orient,[status(thm)],[t68885]) ).
cnf(t35728,plain,
or(t7,not(and(t1,cin))) = or(t7,not(and(cin,t1))),
inference(cp,[status(thm)],[t35727,t16833]) ).
cnf(t69831,plain,
or(t7,not(and(t1,cin))) = or(t7,not(t1)),
inference(step,[status(thm)],[t35728,t35727]) ).
cnf(t4274,plain,
or(t7,carry) = or(t7,not(t1)),
inference(cp,[status(thm)],[t4272,t2687]) ).
cnf(t8350,plain,
or(t7,not(t1)) = or(t7,carry),
inference(orient,[status(thm)],[t4274]) ).
cnf(t69832,plain,
or(t7,not(and(t1,cin))) = or(t7,carry),
inference(step,[status(thm)],[t69831,t8350]) ).
cnf(t59760,plain,
or(t7,not(and(t1,cin))) = or(t7,carry),
inference(orient,[status(thm)],[t69832]) ).
cnf(t59783,plain,
and(and(t1,cin),t7) = and(and(t1,cin),or(t7,carry)),
inference(cp,[status(thm)],[t1104,t59760]) ).
cnf(t69933,plain,
and(t1,and(cin,t7)) = and(and(t1,cin),or(t7,carry)),
inference(step,[status(thm)],[t59783,t46]) ).
cnf(t49,plain,
and(X1,and(X2,X3)) = and(X3,and(X1,X2)),
inference(cp,[status(thm)],[t46,t45]) ).
cnf(t802,plain,
and(X1,and(X2,X3)) = and(X3,and(X1,X2)),
inference(orient,[status(thm)],[t49]) ).
cnf(t69934,plain,
and(t7,and(t1,cin)) = and(and(t1,cin),or(t7,carry)),
inference(step,[status(thm)],[t69933,t802]) ).
cnf(t69935,plain,
and(t7,and(t1,cin)) = and(t1,and(cin,or(t7,carry))),
inference(step,[status(thm)],[t69934,t46]) ).
cnf(t12371,plain,
or(carry,cin) = or(carry,not(t7)),
inference(cp,[status(thm)],[t12364,t264]) ).
cnf(t67708,plain,
or(cin,carry) = or(carry,not(t7)),
inference(step,[status(thm)],[t12371,t164]) ).
cnf(t12418,plain,
or(carry,not(t7)) = or(cin,carry),
inference(orient,[status(thm)],[t67708]) ).
cnf(t12432,plain,
or(carry,not(not(t7))) = or(carry,not(or(cin,carry))),
inference(cp,[status(thm)],[t3908,t12418]) ).
cnf(t67712,plain,
or(carry,t7) = or(carry,not(or(cin,carry))),
inference(step,[status(thm)],[t12432,t40]) ).
cnf(t67713,plain,
or(t7,carry) = or(carry,not(or(cin,carry))),
inference(step,[status(thm)],[t67712,t164]) ).
cnf(t67714,plain,
or(t7,carry) = or(carry,not(cin)),
inference(step,[status(thm)],[t67713,t3133]) ).
cnf(t12562,plain,
or(carry,not(cin)) = or(t7,carry),
inference(orient,[status(thm)],[t67714]) ).
cnf(t12566,plain,
and(not(not(cin)),carry) = and(not(not(cin)),or(t7,carry)),
inference(cp,[status(thm)],[t3022,t12562]) ).
cnf(t69666,plain,
and(carry,not(not(cin))) = and(not(not(cin)),or(t7,carry)),
inference(step,[status(thm)],[t12566,t45]) ).
cnf(t69667,plain,
and(carry,cin) = and(not(not(cin)),or(t7,carry)),
inference(step,[status(thm)],[t69666,t40]) ).
cnf(t69668,plain,
and(cin,carry) = and(not(not(cin)),or(t7,carry)),
inference(step,[status(thm)],[t69667,t45]) ).
cnf(t69669,plain,
and(cin,carry) = and(or(t7,carry),not(not(cin))),
inference(step,[status(thm)],[t69668,t45]) ).
cnf(t69670,plain,
and(cin,carry) = and(or(t7,carry),cin),
inference(step,[status(thm)],[t69669,t40]) ).
cnf(t69671,plain,
and(cin,carry) = and(cin,or(t7,carry)),
inference(step,[status(thm)],[t69670,t45]) ).
cnf(t57326,plain,
and(cin,or(t7,carry)) = and(cin,carry),
inference(orient,[status(thm)],[t69671]) ).
cnf(t69936,plain,
and(t7,and(t1,cin)) = and(t1,and(cin,carry)),
inference(step,[status(thm)],[t69935,t57326]) ).
cnf(t61418,plain,
and(t1,and(cin,carry)) = and(t7,and(t1,cin)),
inference(orient,[status(thm)],[t69936]) ).
cnf(t70177,plain,
and(t1,carry_def) = and(t7,and(t1,cin)),
inference(step,[status(thm)],[t63185,t61418]) ).
cnf(t65242,plain,
and(t7,and(t1,cin)) = and(t1,carry_def),
inference(orient,[status(thm)],[t70177]) ).
cnf(t70223,plain,
not(t5) = and(t1,carry_def),
inference(step,[status(thm)],[t70222,t65242]) ).
cnf(t65942,plain,
and(t1,carry_def) = not(t5),
inference(orient,[status(thm)],[t70223]) ).
cnf(t65976,plain,
and(t1,not(carry_def)) = and(t1,not(not(t5))),
inference(cp,[status(thm)],[t3354,t65942]) ).
cnf(t1770,plain,
xor(X1,or(X2,X1)) = or(ll0,and(not(X1),or(X2,X1))),
inference(cp,[status(thm)],[t192,t1750]) ).
cnf(t68602,plain,
xor(X1,or(X2,X1)) = and(not(X1),or(X2,X1)),
inference(step,[status(thm)],[t1770,t436]) ).
cnf(t68603,plain,
xor(X1,or(X2,X1)) = and(not(X1),X2),
inference(step,[status(thm)],[t68602,t3022]) ).
cnf(t30409,plain,
xor(X1,or(X2,X1)) = and(not(X1),X2),
inference(orient,[status(thm)],[t68603]) ).
cnf(t63490,plain,
ll1 = or(carry_def,or(t7,t1)),
inference(cp,[status(thm)],[t2410,t63447]) ).
cnf(t70126,plain,
ll1 = or(t7,or(carry_def,t1)),
inference(step,[status(thm)],[t63490,t1008]) ).
cnf(t70127,plain,
ll1 = or(t7,or(t1,carry_def)),
inference(step,[status(thm)],[t70126,t164]) ).
cnf(t234,plain,
or(and(cin,or(b,a)),or(and(not(cin),and(b,a)),X1)) = or(carry_def,X1),
inference(cp,[status(thm)],[t179,t232]) ).
cnf(t69914,plain,
or(and(cin,or(t4,carry)),or(and(not(cin),and(b,a)),X1)) = or(carry_def,X1),
inference(step,[status(thm)],[t234,t7473]) ).
cnf(t69915,plain,
or(and(cin,carry),or(and(not(cin),and(b,a)),X1)) = or(carry_def,X1),
inference(step,[status(thm)],[t69914,t40276]) ).
cnf(t69916,plain,
or(and(cin,carry),or(and(b,and(not(cin),a)),X1)) = or(carry_def,X1),
inference(step,[status(thm)],[t69915,t819]) ).
cnf(t69917,plain,
or(and(cin,carry),or(and(b,and(a,not(cin))),X1)) = or(carry_def,X1),
inference(step,[status(thm)],[t69916,t45]) ).
cnf(t69918,plain,
or(and(cin,carry),or(and(not(t1),not(cin)),X1)) = or(carry_def,X1),
inference(step,[status(thm)],[t69917,t1327]) ).
cnf(t69919,plain,
or(and(cin,carry),or(not(or(t1,cin)),X1)) = or(carry_def,X1),
inference(step,[status(thm)],[t69918,t69]) ).
cnf(t69920,plain,
or(and(cin,carry),or(not(or(t1,sum_def)),X1)) = or(carry_def,X1),
inference(step,[status(thm)],[t69919,t25996]) ).
cnf(t69921,plain,
or(and(cin,carry),or(and(t7,not(t1)),X1)) = or(carry_def,X1),
inference(step,[status(thm)],[t69920,t27926]) ).
cnf(t61162,plain,
or(and(cin,carry),or(and(t7,not(t1)),X1)) = or(carry_def,X1),
inference(orient,[status(thm)],[t69921]) ).
cnf(t61204,plain,
or(carry_def,not(and(t7,not(t1)))) = or(and(cin,carry),ll1),
inference(cp,[status(thm)],[t61162,t167]) ).
cnf(t69922,plain,
or(carry_def,or(not(t7),t1)) = or(and(cin,carry),ll1),
inference(step,[status(thm)],[t61204,t708]) ).
cnf(f15,axiom,
or(X,ll1) = ll1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',or_boundedness) ).
fof(f15_nnf,plain,
! [X] : or(X,ll1) = ll1,
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [X] : or(X,ll1) = ll1,
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
or(X0,ll1) = ll1,
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(t8,plain,
or(X1,ll1) = ll1,
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(t190,plain,
or(X1,ll1) = ll1,
inference(orient,[status(thm)],[t8]) ).
cnf(t69923,plain,
or(carry_def,or(not(t7),t1)) = ll1,
inference(step,[status(thm)],[t69922,t190]) ).
cnf(t183,plain,
or(X1,or(X2,X3)) = or(X3,or(X1,X2)),
inference(cp,[status(thm)],[t179,t164]) ).
cnf(t998,plain,
or(X1,or(X2,X3)) = or(X3,or(X1,X2)),
inference(orient,[status(thm)],[t183]) ).
cnf(t69924,plain,
or(t1,or(carry_def,not(t7))) = ll1,
inference(step,[status(thm)],[t69923,t998]) ).
cnf(t61256,plain,
or(t1,or(carry_def,not(t7))) = ll1,
inference(orient,[status(thm)],[t69924]) ).
cnf(t61277,plain,
or(t1,not(or(carry_def,not(t7)))) = or(t1,not(ll1)),
inference(cp,[status(thm)],[t3908,t61256]) ).
cnf(t69925,plain,
or(t1,and(not(carry_def),t7)) = or(t1,not(ll1)),
inference(step,[status(thm)],[t61277,t573]) ).
cnf(t69926,plain,
or(t1,and(t7,not(carry_def))) = or(t1,not(ll1)),
inference(step,[status(thm)],[t69925,t45]) ).
cnf(t69927,plain,
or(t1,and(t7,not(carry_def))) = or(t1,ll0),
inference(step,[status(thm)],[t69926,t155]) ).
cnf(t69928,plain,
or(t1,and(t7,not(carry_def))) = t1,
inference(step,[status(thm)],[t69927,t43]) ).
cnf(t61283,plain,
or(t1,and(t7,not(carry_def))) = t1,
inference(orient,[status(thm)],[t69928]) ).
cnf(t61306,plain,
ll0 = and(and(t7,not(carry_def)),not(t1)),
inference(cp,[status(thm)],[t1750,t61283]) ).
cnf(t69945,plain,
ll0 = and(t7,and(not(carry_def),not(t1))),
inference(step,[status(thm)],[t61306,t46]) ).
cnf(t69946,plain,
ll0 = and(t7,not(or(carry_def,t1))),
inference(step,[status(thm)],[t69945,t69]) ).
cnf(t69947,plain,
ll0 = and(t7,not(or(t1,carry_def))),
inference(step,[status(thm)],[t69946,t164]) ).
cnf(t61666,plain,
and(t7,not(or(t1,carry_def))) = ll0,
inference(orient,[status(thm)],[t69947]) ).
cnf(t61674,plain,
or(not(not(or(t1,carry_def))),t7) = or(not(not(or(t1,carry_def))),ll0),
inference(cp,[status(thm)],[t3248,t61666]) ).
cnf(t69951,plain,
or(t7,not(not(or(t1,carry_def)))) = or(not(not(or(t1,carry_def))),ll0),
inference(step,[status(thm)],[t61674,t164]) ).
cnf(t69952,plain,
or(t7,or(t1,carry_def)) = or(not(not(or(t1,carry_def))),ll0),
inference(step,[status(thm)],[t69951,t40]) ).
cnf(t69953,plain,
or(t7,or(t1,carry_def)) = not(not(or(t1,carry_def))),
inference(step,[status(thm)],[t69952,t43]) ).
cnf(t69954,plain,
or(t7,or(t1,carry_def)) = or(t1,carry_def),
inference(step,[status(thm)],[t69953,t40]) ).
cnf(t61770,plain,
or(t7,or(t1,carry_def)) = or(t1,carry_def),
inference(orient,[status(thm)],[t69954]) ).
cnf(t70128,plain,
ll1 = or(t1,carry_def),
inference(step,[status(thm)],[t70127,t61770]) ).
cnf(t64504,plain,
or(t1,carry_def) = ll1,
inference(orient,[status(thm)],[t70128]) ).
cnf(t64505,plain,
and(not(carry_def),t1) = xor(carry_def,ll1),
inference(cp,[status(thm)],[t30409,t64504]) ).
cnf(t70165,plain,
and(t1,not(carry_def)) = xor(carry_def,ll1),
inference(step,[status(thm)],[t64505,t45]) ).
cnf(t70166,plain,
and(t1,not(carry_def)) = not(carry_def),
inference(step,[status(thm)],[t70165,t370]) ).
cnf(t64885,plain,
and(t1,not(carry_def)) = not(carry_def),
inference(orient,[status(thm)],[t70166]) ).
cnf(t70234,plain,
not(carry_def) = and(t1,not(not(t5))),
inference(step,[status(thm)],[t65976,t64885]) ).
cnf(t70235,plain,
not(carry_def) = and(t1,t5),
inference(step,[status(thm)],[t70234,t40]) ).
cnf(t70236,plain,
not(carry_def) = and(t5,t1),
inference(step,[status(thm)],[t70235,t45]) ).
cnf(t70237,plain,
not(carry_def) = not(carry),
inference(step,[status(thm)],[t70236,t269]) ).
cnf(t66075,plain,
not(carry) = not(carry_def),
inference(orient,[status(thm)],[t70237]) ).
cnf(t66112,plain,
carry = not(not(carry_def)),
inference(cp,[status(thm)],[t40,t66075]) ).
cnf(t70315,plain,
carry = carry_def,
inference(step,[status(thm)],[t66112,t40]) ).
cnf(t66201,plain,
carry = carry_def,
inference(orient,[status(thm)],[t70315]) ).
cnf(t70411,plain,
ifeq(carry_def,carry_def,false,true) = true,
inference(step,[status(thm)],[t32371,t66201]) ).
cnf(t70412,plain,
false = true,
inference(step,[status(thm)],[t70411,t44]) ).
cnf(t66297,plain,
false = true,
inference(rw,[status(thm)],[t70412]) ).
cnf(t66499,plain,
false = true,
inference(orient,[status(thm)],[t66297]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c35]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t66499]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : HWV003-2 : TPTP v9.3.1. Released v2.7.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n003.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Wed Sep 23 16:21:36 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 241.79/35.33 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 241.79/35.33 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------