%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT041-1 : TPTP v9.3.1. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n008.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:55:05 PM UTC 2026
% Result : Unsatisfiable 67.37s 9.12s
% Output : Proof 67.37s
% Verified :
% SZS Type : Refutation
% Derivation depth : 82
% Number of leaves : 26
% Syntax : Number of formulae : 693 ( 681 unt; 0 def)
% Number of atoms : 709 ( 674 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 47 ( 31 ~; 16 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 25 ( 25 usr; 20 con; 0-4 aty)
% Number of variables : 1324 ( 29 sgn 58 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(t65,axiom,
sFlat0 = plus(b,c),
introduced(definition) ).
cnf(t1105,plain,
plus(b,c) = sFlat0,
inference(orient,[status(thm)],[t65]) ).
cnf(t66,axiom,
sFlat1 = times(c,e),
introduced(definition) ).
cnf(t984,plain,
times(c,e) = sFlat1,
inference(orient,[status(thm)],[t66]) ).
cnf(t67,axiom,
sFlat2 = times(d,times(c,e)),
introduced(definition) ).
cnf(t32594,plain,
sFlat2 = times(d,sFlat1),
inference(step,[status(thm)],[t67,t984]) ).
cnf(t1015,plain,
times(d,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t32594]) ).
cnf(t68,axiom,
sFlat3 = times(plus(b,c),times(d,times(c,e))),
introduced(definition) ).
cnf(t32593,plain,
sFlat3 = times(plus(b,c),times(d,sFlat1)),
inference(step,[status(thm)],[t68,t984]) ).
cnf(t997,plain,
times(plus(b,c),times(d,sFlat1)) = sFlat3,
inference(orient,[status(thm)],[t32593]) ).
cnf(t32595,plain,
times(plus(b,c),sFlat2) = sFlat3,
inference(step,[status(thm)],[t997,t1015]) ).
cnf(t1028,plain,
times(plus(b,c),sFlat2) = sFlat3,
inference(rw,[status(thm)],[t32595]) ).
cnf(t32611,plain,
times(sFlat0,sFlat2) = sFlat3,
inference(step,[status(thm)],[t1028,t1105]) ).
cnf(t1164,plain,
times(sFlat0,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t32611]) ).
cnf(t69,axiom,
sFlat4 = plus(b,times(plus(b,c),times(d,times(c,e)))),
introduced(definition) ).
cnf(t32600,plain,
sFlat4 = plus(b,times(plus(b,c),times(d,sFlat1))),
inference(step,[status(thm)],[t69,t984]) ).
cnf(t32601,plain,
sFlat4 = plus(b,times(plus(b,c),sFlat2)),
inference(step,[status(thm)],[t32600,t1015]) ).
cnf(t1077,plain,
plus(b,times(plus(b,c),sFlat2)) = sFlat4,
inference(orient,[status(thm)],[t32601]) ).
cnf(t32606,plain,
plus(b,times(sFlat0,sFlat2)) = sFlat4,
inference(step,[status(thm)],[t1077,t1105]) ).
cnf(t1118,plain,
plus(b,times(sFlat0,sFlat2)) = sFlat4,
inference(rw,[status(thm)],[t32606]) ).
cnf(t32617,plain,
plus(b,sFlat3) = sFlat4,
inference(step,[status(thm)],[t1118,t1164]) ).
cnf(t1200,plain,
plus(b,sFlat3) = sFlat4,
inference(orient,[status(thm)],[t32617]) ).
cnf(t70,axiom,
sFlat5 = times(a,plus(b,times(plus(b,c),times(d,times(c,e))))),
introduced(definition) ).
cnf(t32596,plain,
sFlat5 = times(a,plus(b,times(plus(b,c),times(d,sFlat1)))),
inference(step,[status(thm)],[t70,t984]) ).
cnf(t32597,plain,
sFlat5 = times(a,plus(b,times(plus(b,c),sFlat2))),
inference(step,[status(thm)],[t32596,t1015]) ).
cnf(t1029,plain,
times(a,plus(b,times(plus(b,c),sFlat2))) = sFlat5,
inference(orient,[status(thm)],[t32597]) ).
cnf(t32602,plain,
times(a,sFlat4) = sFlat5,
inference(step,[status(thm)],[t1029,t1077]) ).
cnf(t1090,plain,
times(a,sFlat4) = sFlat5,
inference(rw,[status(thm)],[t32602]) ).
cnf(t1119,plain,
times(a,sFlat4) = sFlat5,
inference(orient,[status(thm)],[t1090]) ).
cnf(t71,axiom,
sFlat6 = plus(b,times(d,times(c,e))),
introduced(definition) ).
cnf(t32603,plain,
sFlat6 = plus(b,times(d,sFlat1)),
inference(step,[status(thm)],[t71,t984]) ).
cnf(t32604,plain,
sFlat6 = plus(b,sFlat2),
inference(step,[status(thm)],[t32603,t1015]) ).
cnf(t1091,plain,
plus(b,sFlat2) = sFlat6,
inference(orient,[status(thm)],[t32604]) ).
cnf(t72,axiom,
sFlat7 = times(a,plus(b,times(d,times(c,e)))),
introduced(definition) ).
cnf(t32598,plain,
sFlat7 = times(a,plus(b,times(d,sFlat1))),
inference(step,[status(thm)],[t72,t984]) ).
cnf(t32599,plain,
sFlat7 = times(a,plus(b,sFlat2)),
inference(step,[status(thm)],[t32598,t1015]) ).
cnf(t1044,plain,
times(a,plus(b,sFlat2)) = sFlat7,
inference(orient,[status(thm)],[t32599]) ).
cnf(t32605,plain,
times(a,sFlat6) = sFlat7,
inference(step,[status(thm)],[t1044,t1091]) ).
cnf(t1104,plain,
times(a,sFlat6) = sFlat7,
inference(rw,[status(thm)],[t32605]) ).
cnf(t1132,plain,
times(a,sFlat6) = sFlat7,
inference(orient,[status(thm)],[t1104]) ).
cnf(f13,hypothesis,
( big_p(W,big_p(W,X,Y),Z) = big_p(W,X,big_p(W,Y,Z))
| ~ term(W) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',q2) ).
fof(f13_nnf,plain,
! [W,X,Y,Z] :
( big_p(W,big_p(W,X,Y),Z) = big_p(W,X,big_p(W,Y,Z))
| ~ term(W) ),
inference(nnf_transformation,[status(thm)],[f13]) ).
fof(f13_sk,plain,
! [W,X,Y,Z] :
( big_p(W,big_p(W,X,Y),Z) = big_p(W,X,big_p(W,Y,Z))
| ~ term(W) ),
inference(skolemisation,[status(esa)],[f13_nnf]) ).
cnf(c13,plain,
( big_p(X0,big_p(X0,X1,X2),X3) = big_p(X0,X1,big_p(X0,X2,X3))
| ~ term(X0) ),
inference(cnf_transformation,[status(esa)],[f13_sk]) ).
cnf(hi13,axiom,
ifeq(term(X0),true,big_p(X0,big_p(X0,X1,X2),X3),big_p(X0,X1,big_p(X0,X2,X3))) = big_p(X0,X1,big_p(X0,X2,X3)),
inference(equality_encoding,[status(esa)],[c13]) ).
cnf(f9,axiom,
term(term3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',term3) ).
fof(f9_nnf,plain,
term(term3),
inference(nnf_transformation,[status(thm)],[f9]) ).
cnf(c9,plain,
term(term3),
inference(cnf_transformation,[status(esa)],[f9_nnf]) ).
cnf(hi9,axiom,
term(term3) = true,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(f6,axiom,
big_t(W,X,Y) = big_p(W,X,Y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',big_p_and_big_t) ).
fof(f6_nnf,plain,
! [W,X,Y] : big_t(W,X,Y) = big_p(W,X,Y),
inference(nnf_transformation,[status(thm)],[f6]) ).
fof(f6_sk,plain,
! [W,X,Y] : big_t(W,X,Y) = big_p(W,X,Y),
inference(skolemisation,[status(esa)],[f6_nnf]) ).
cnf(c6,plain,
big_t(X0,X1,X2) = big_p(X0,X1,X2),
inference(cnf_transformation,[status(esa)],[f6_sk]) ).
cnf(hi1,axiom,
big_t(X0,X1,X2) = big_p(X0,X1,X2),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t16,plain,
big_p(term3,big_p(term3,X1,X2),X3) = big_p(term3,X1,big_p(term3,X2,X3)),
inference(hyper_resolution,[status(thm)],[hi13,hi9,hi1]) ).
cnf(t13,plain,
big_t(X1,X2,X3) = big_p(X1,X2,X3),
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t76,plain,
big_p(X1,X2,X3) = big_t(X1,X2,X3),
inference(orient,[status(thm)],[t13]) ).
cnf(t32453,plain,
big_t(term3,big_p(term3,X1,X2),X3) = big_p(term3,X1,big_p(term3,X2,X3)),
inference(step,[status(thm)],[t16,t76]) ).
cnf(f2,axiom,
big_p(term3,X,Y) = times(X,Y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',big_p_term3) ).
fof(f2_nnf,plain,
! [X,Y] : big_p(term3,X,Y) = times(X,Y),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X,Y] : big_p(term3,X,Y) = times(X,Y),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
big_p(term3,X0,X1) = times(X0,X1),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t9,plain,
big_p(term3,X1,X2) = times(X1,X2),
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t32440,plain,
big_t(term3,X1,X2) = times(X1,X2),
inference(step,[status(thm)],[t9,t76]) ).
cnf(t685,plain,
big_t(term3,X1,X2) = times(X1,X2),
inference(orient,[status(thm)],[t32440]) ).
cnf(t32454,plain,
times(big_p(term3,X1,X2),X3) = big_p(term3,X1,big_p(term3,X2,X3)),
inference(step,[status(thm)],[t32453,t685]) ).
cnf(t32455,plain,
times(big_t(term3,X1,X2),X3) = big_p(term3,X1,big_p(term3,X2,X3)),
inference(step,[status(thm)],[t32454,t76]) ).
cnf(t32456,plain,
times(times(X1,X2),X3) = big_p(term3,X1,big_p(term3,X2,X3)),
inference(step,[status(thm)],[t32455,t685]) ).
cnf(t32457,plain,
times(times(X1,X2),X3) = big_t(term3,X1,big_p(term3,X2,X3)),
inference(step,[status(thm)],[t32456,t76]) ).
cnf(t32458,plain,
times(times(X1,X2),X3) = times(X1,big_p(term3,X2,X3)),
inference(step,[status(thm)],[t32457,t685]) ).
cnf(t32459,plain,
times(times(X1,X2),X3) = times(X1,big_t(term3,X2,X3)),
inference(step,[status(thm)],[t32458,t76]) ).
cnf(t32460,plain,
times(times(X1,X2),X3) = times(X1,times(X2,X3)),
inference(step,[status(thm)],[t32459,t685]) ).
cnf(t708,plain,
times(times(X1,X2),X3) = times(X1,times(X2,X3)),
inference(orient,[status(thm)],[t32460]) ).
cnf(t1133,plain,
times(a,times(sFlat6,X1)) = times(sFlat7,X1),
inference(cp,[status(thm)],[t708,t1132]) ).
cnf(t1314,plain,
times(a,times(sFlat6,X1)) = times(sFlat7,X1),
inference(orient,[status(thm)],[t1133]) ).
cnf(f14,hypothesis,
( big_p(W,big_p(W,X,Y),big_p(W,Z,V)) = big_p(W,big_p(W,X,Z),big_p(W,Y,V))
| ~ term(W) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',q5) ).
fof(f14_nnf,plain,
! [W,X,Y,Z,V] :
( big_p(W,big_p(W,X,Y),big_p(W,Z,V)) = big_p(W,big_p(W,X,Z),big_p(W,Y,V))
| ~ term(W) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [W,X,Y,Z,V] :
( big_p(W,big_p(W,X,Y),big_p(W,Z,V)) = big_p(W,big_p(W,X,Z),big_p(W,Y,V))
| ~ term(W) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( big_p(X0,big_p(X0,X1,X2),big_p(X0,X3,X4)) = big_p(X0,big_p(X0,X1,X3),big_p(X0,X2,X4))
| ~ term(X0) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(hi14,axiom,
ifeq(term(X0),true,big_p(X0,big_p(X0,X1,X2),big_p(X0,X3,X4)),big_p(X0,big_p(X0,X1,X3),big_p(X0,X2,X4))) = big_p(X0,big_p(X0,X1,X3),big_p(X0,X2,X4)),
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(t22,plain,
big_p(term3,big_p(term3,X1,X2),big_p(term3,X3,X4)) = big_p(term3,big_p(term3,X1,X3),big_p(term3,X2,X4)),
inference(hyper_resolution,[status(thm)],[hi14,hi9,hi1]) ).
cnf(t32461,plain,
big_t(term3,big_p(term3,X1,X2),big_p(term3,X3,X4)) = big_p(term3,big_p(term3,X1,X3),big_p(term3,X2,X4)),
inference(step,[status(thm)],[t22,t76]) ).
cnf(t32462,plain,
times(big_p(term3,X1,X2),big_p(term3,X3,X4)) = big_p(term3,big_p(term3,X1,X3),big_p(term3,X2,X4)),
inference(step,[status(thm)],[t32461,t685]) ).
cnf(t32463,plain,
times(big_t(term3,X1,X2),big_p(term3,X3,X4)) = big_p(term3,big_p(term3,X1,X3),big_p(term3,X2,X4)),
inference(step,[status(thm)],[t32462,t76]) ).
cnf(t32464,plain,
times(times(X1,X2),big_p(term3,X3,X4)) = big_p(term3,big_p(term3,X1,X3),big_p(term3,X2,X4)),
inference(step,[status(thm)],[t32463,t685]) ).
cnf(t32465,plain,
times(X1,times(X2,big_p(term3,X3,X4))) = big_p(term3,big_p(term3,X1,X3),big_p(term3,X2,X4)),
inference(step,[status(thm)],[t32464,t708]) ).
cnf(t32466,plain,
times(X1,times(X2,big_t(term3,X3,X4))) = big_p(term3,big_p(term3,X1,X3),big_p(term3,X2,X4)),
inference(step,[status(thm)],[t32465,t76]) ).
cnf(t32467,plain,
times(X1,times(X2,times(X3,X4))) = big_p(term3,big_p(term3,X1,X3),big_p(term3,X2,X4)),
inference(step,[status(thm)],[t32466,t685]) ).
cnf(t32468,plain,
times(X1,times(X2,times(X3,X4))) = big_t(term3,big_p(term3,X1,X3),big_p(term3,X2,X4)),
inference(step,[status(thm)],[t32467,t76]) ).
cnf(t32469,plain,
times(X1,times(X2,times(X3,X4))) = times(big_p(term3,X1,X3),big_p(term3,X2,X4)),
inference(step,[status(thm)],[t32468,t685]) ).
cnf(t32470,plain,
times(X1,times(X2,times(X3,X4))) = times(big_t(term3,X1,X3),big_p(term3,X2,X4)),
inference(step,[status(thm)],[t32469,t76]) ).
cnf(t32471,plain,
times(X1,times(X2,times(X3,X4))) = times(times(X1,X3),big_p(term3,X2,X4)),
inference(step,[status(thm)],[t32470,t685]) ).
cnf(t32472,plain,
times(X1,times(X2,times(X3,X4))) = times(X1,times(X3,big_p(term3,X2,X4))),
inference(step,[status(thm)],[t32471,t708]) ).
cnf(t32473,plain,
times(X1,times(X2,times(X3,X4))) = times(X1,times(X3,big_t(term3,X2,X4))),
inference(step,[status(thm)],[t32472,t76]) ).
cnf(t32474,plain,
times(X1,times(X2,times(X3,X4))) = times(X1,times(X3,times(X2,X4))),
inference(step,[status(thm)],[t32473,t685]) ).
cnf(t709,plain,
times(X1,times(X2,times(X3,X4))) = times(X1,times(X3,times(X2,X4))),
inference(orient,[status(thm)],[t32474]) ).
cnf(t1318,plain,
times(sFlat7,times(X1,X2)) = times(a,times(X1,times(sFlat6,X2))),
inference(cp,[status(thm)],[t1314,t709]) ).
cnf(t7936,plain,
times(a,times(X1,times(sFlat6,X2))) = times(sFlat7,times(X1,X2)),
inference(orient,[status(thm)],[t1318]) ).
cnf(f15,hypothesis,
( big_t(W1,big_p(W2,big_t(W1,X,Y),Z),big_p(W2,Y,Z)) = big_p(W2,big_t(W1,X,Y),Z)
| ~ term(W2)
| ~ term(W1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',q3) ).
fof(f15_nnf,plain,
! [W1,W2,X,Y,Z] :
( big_t(W1,big_p(W2,big_t(W1,X,Y),Z),big_p(W2,Y,Z)) = big_p(W2,big_t(W1,X,Y),Z)
| ~ term(W2)
| ~ term(W1) ),
inference(nnf_transformation,[status(thm)],[f15]) ).
fof(f15_sk,plain,
! [W1,W2,X,Y,Z] :
( big_t(W1,big_p(W2,big_t(W1,X,Y),Z),big_p(W2,Y,Z)) = big_p(W2,big_t(W1,X,Y),Z)
| ~ term(W2)
| ~ term(W1) ),
inference(skolemisation,[status(esa)],[f15_nnf]) ).
cnf(c15,plain,
( big_t(X0,big_p(X1,big_t(X0,X2,X3),X4),big_p(X1,X3,X4)) = big_p(X1,big_t(X0,X2,X3),X4)
| ~ term(X1)
| ~ term(X0) ),
inference(cnf_transformation,[status(esa)],[f15_sk]) ).
cnf(hi15,axiom,
ifeq(term(X0),true,ifeq(term(X1),true,big_t(X0,big_p(X1,big_t(X0,X2,X3),X4),big_p(X1,X3,X4)),big_p(X1,big_t(X0,X2,X3),X4)),big_p(X1,big_t(X0,X2,X3),X4)) = big_p(X1,big_t(X0,X2,X3),X4),
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(f12,axiom,
term(term6),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',term6) ).
fof(f12_nnf,plain,
term(term6),
inference(nnf_transformation,[status(thm)],[f12]) ).
cnf(c12,plain,
term(term6),
inference(cnf_transformation,[status(esa)],[f12_nnf]) ).
cnf(hi12,axiom,
term(term6) = true,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t43,plain,
big_t(term3,big_p(term6,big_t(term3,X1,X2),X3),big_p(term6,X2,X3)) = big_p(term6,big_t(term3,X1,X2),X3),
inference(hyper_resolution,[status(thm)],[hi15,hi9,hi12,hi1]) ).
cnf(t32428,plain,
big_t(term3,big_t(term6,big_t(term3,X1,X2),X3),big_p(term6,X2,X3)) = big_p(term6,big_t(term3,X1,X2),X3),
inference(step,[status(thm)],[t43,t76]) ).
cnf(f5,axiom,
big_p(term6,X,Y) = plus(Y,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',big_p_term6) ).
fof(f5_nnf,plain,
! [X,Y] : big_p(term6,X,Y) = plus(Y,X),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X,Y] : big_p(term6,X,Y) = plus(Y,X),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
big_p(term6,X0,X1) = plus(X1,X0),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(t12,plain,
big_p(term6,X1,X2) = plus(X2,X1),
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(t32382,plain,
big_t(term6,X1,X2) = plus(X2,X1),
inference(step,[status(thm)],[t12,t76]) ).
cnf(t524,plain,
big_t(term6,X1,X2) = plus(X2,X1),
inference(orient,[status(thm)],[t32382]) ).
cnf(t32429,plain,
big_t(term3,plus(X3,big_t(term3,X1,X2)),big_p(term6,X2,X3)) = big_p(term6,big_t(term3,X1,X2),X3),
inference(step,[status(thm)],[t32428,t524]) ).
cnf(t32430,plain,
big_t(term3,plus(X3,big_t(term3,X1,X2)),big_t(term6,X2,X3)) = big_p(term6,big_t(term3,X1,X2),X3),
inference(step,[status(thm)],[t32429,t76]) ).
cnf(t32431,plain,
big_t(term3,plus(X3,big_t(term3,X1,X2)),plus(X3,X2)) = big_p(term6,big_t(term3,X1,X2),X3),
inference(step,[status(thm)],[t32430,t524]) ).
cnf(t32432,plain,
big_t(term3,plus(X3,big_t(term3,X1,X2)),plus(X3,X2)) = big_t(term6,big_t(term3,X1,X2),X3),
inference(step,[status(thm)],[t32431,t76]) ).
cnf(t32433,plain,
big_t(term3,plus(X3,big_t(term3,X1,X2)),plus(X3,X2)) = plus(X3,big_t(term3,X1,X2)),
inference(step,[status(thm)],[t32432,t524]) ).
cnf(t639,plain,
big_t(term3,plus(X1,big_t(term3,X2,X3)),plus(X1,X3)) = plus(X1,big_t(term3,X2,X3)),
inference(orient,[status(thm)],[t32433]) ).
cnf(t32441,plain,
times(plus(X1,big_t(term3,X2,X3)),plus(X1,X3)) = plus(X1,big_t(term3,X2,X3)),
inference(step,[status(thm)],[t639,t685]) ).
cnf(t32442,plain,
times(plus(X1,times(X2,X3)),plus(X1,X3)) = plus(X1,big_t(term3,X2,X3)),
inference(step,[status(thm)],[t32441,t685]) ).
cnf(t32443,plain,
times(plus(X1,times(X2,X3)),plus(X1,X3)) = plus(X1,times(X2,X3)),
inference(step,[status(thm)],[t32442,t685]) ).
cnf(t704,plain,
times(plus(X1,times(X2,X3)),plus(X1,X3)) = plus(X1,times(X2,X3)),
inference(rw,[status(thm)],[t32443]) ).
cnf(t15029,plain,
times(plus(X1,times(X2,X3)),plus(X1,X3)) = plus(X1,times(X2,X3)),
inference(orient,[status(thm)],[t704]) ).
cnf(t58,plain,
big_t(term6,big_p(term3,big_t(term6,X1,X2),X3),big_p(term3,X2,X3)) = big_p(term3,big_t(term6,X1,X2),X3),
inference(hyper_resolution,[status(thm)],[hi15,hi12,hi9,hi1]) ).
cnf(t32496,plain,
plus(big_p(term3,X2,X3),big_p(term3,big_t(term6,X1,X2),X3)) = big_p(term3,big_t(term6,X1,X2),X3),
inference(step,[status(thm)],[t58,t524]) ).
cnf(t32497,plain,
plus(big_t(term3,X2,X3),big_p(term3,big_t(term6,X1,X2),X3)) = big_p(term3,big_t(term6,X1,X2),X3),
inference(step,[status(thm)],[t32496,t76]) ).
cnf(t32498,plain,
plus(times(X2,X3),big_p(term3,big_t(term6,X1,X2),X3)) = big_p(term3,big_t(term6,X1,X2),X3),
inference(step,[status(thm)],[t32497,t685]) ).
cnf(t32499,plain,
plus(times(X2,X3),big_t(term3,big_t(term6,X1,X2),X3)) = big_p(term3,big_t(term6,X1,X2),X3),
inference(step,[status(thm)],[t32498,t76]) ).
cnf(t32500,plain,
plus(times(X2,X3),times(big_t(term6,X1,X2),X3)) = big_p(term3,big_t(term6,X1,X2),X3),
inference(step,[status(thm)],[t32499,t685]) ).
cnf(t32501,plain,
plus(times(X2,X3),times(plus(X2,X1),X3)) = big_p(term3,big_t(term6,X1,X2),X3),
inference(step,[status(thm)],[t32500,t524]) ).
cnf(t32502,plain,
plus(times(X2,X3),times(plus(X2,X1),X3)) = big_t(term3,big_t(term6,X1,X2),X3),
inference(step,[status(thm)],[t32501,t76]) ).
cnf(t32503,plain,
plus(times(X2,X3),times(plus(X2,X1),X3)) = times(big_t(term6,X1,X2),X3),
inference(step,[status(thm)],[t32502,t685]) ).
cnf(t32504,plain,
plus(times(X2,X3),times(plus(X2,X1),X3)) = times(plus(X2,X1),X3),
inference(step,[status(thm)],[t32503,t524]) ).
cnf(t774,plain,
plus(times(X1,X2),times(plus(X1,X3),X2)) = times(plus(X1,X3),X2),
inference(orient,[status(thm)],[t32504]) ).
cnf(t15195,plain,
plus(X1,times(sFlat0,sFlat2)) = times(plus(X1,sFlat3),plus(X1,sFlat2)),
inference(cp,[status(thm)],[t15029,t1164]) ).
cnf(t33562,plain,
plus(X1,sFlat3) = times(plus(X1,sFlat3),plus(X1,sFlat2)),
inference(step,[status(thm)],[t15195,t1164]) ).
cnf(t16150,plain,
times(plus(X1,sFlat3),plus(X1,sFlat2)) = plus(X1,sFlat3),
inference(orient,[status(thm)],[t33562]) ).
cnf(t16168,plain,
plus(b,sFlat3) = times(sFlat4,plus(b,sFlat2)),
inference(cp,[status(thm)],[t16150,t1200]) ).
cnf(t33563,plain,
sFlat4 = times(sFlat4,plus(b,sFlat2)),
inference(step,[status(thm)],[t16168,t1200]) ).
cnf(t33564,plain,
sFlat4 = times(sFlat4,sFlat6),
inference(step,[status(thm)],[t33563,t1091]) ).
cnf(t16207,plain,
times(sFlat4,sFlat6) = sFlat4,
inference(orient,[status(thm)],[t33564]) ).
cnf(t16222,plain,
times(plus(sFlat4,X1),sFlat6) = plus(sFlat4,times(plus(sFlat4,X1),sFlat6)),
inference(cp,[status(thm)],[t774,t16207]) ).
cnf(t21467,plain,
plus(sFlat4,times(plus(sFlat4,X1),sFlat6)) = times(plus(sFlat4,X1),sFlat6),
inference(orient,[status(thm)],[t16222]) ).
cnf(t21477,plain,
plus(sFlat4,times(plus(sFlat4,X1),sFlat6)) = times(times(plus(sFlat4,X1),sFlat6),plus(sFlat4,sFlat6)),
inference(cp,[status(thm)],[t15029,t21467]) ).
cnf(t33828,plain,
times(plus(sFlat4,X1),sFlat6) = times(times(plus(sFlat4,X1),sFlat6),plus(sFlat4,sFlat6)),
inference(step,[status(thm)],[t21477,t21467]) ).
cnf(t33829,plain,
times(plus(sFlat4,X1),sFlat6) = times(plus(sFlat4,X1),times(sFlat6,plus(sFlat4,sFlat6))),
inference(step,[status(thm)],[t33828,t708]) ).
cnf(t61,plain,
big_t(term6,big_p(term6,big_t(term6,X1,X2),X3),big_p(term6,X2,X3)) = big_p(term6,big_t(term6,X1,X2),X3),
inference(hyper_resolution,[status(thm)],[hi15,hi12,hi12,hi1]) ).
cnf(t32418,plain,
plus(big_p(term6,X2,X3),big_p(term6,big_t(term6,X1,X2),X3)) = big_p(term6,big_t(term6,X1,X2),X3),
inference(step,[status(thm)],[t61,t524]) ).
cnf(t32419,plain,
plus(big_t(term6,X2,X3),big_p(term6,big_t(term6,X1,X2),X3)) = big_p(term6,big_t(term6,X1,X2),X3),
inference(step,[status(thm)],[t32418,t76]) ).
cnf(t32420,plain,
plus(plus(X3,X2),big_p(term6,big_t(term6,X1,X2),X3)) = big_p(term6,big_t(term6,X1,X2),X3),
inference(step,[status(thm)],[t32419,t524]) ).
cnf(f11,axiom,
term(term5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',term5) ).
fof(f11_nnf,plain,
term(term5),
inference(nnf_transformation,[status(thm)],[f11]) ).
cnf(c11,plain,
term(term5),
inference(cnf_transformation,[status(esa)],[f11_nnf]) ).
cnf(hi11,axiom,
term(term5) = true,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t18,plain,
big_p(term5,big_p(term5,X1,X2),X3) = big_p(term5,X1,big_p(term5,X2,X3)),
inference(hyper_resolution,[status(thm)],[hi13,hi11,hi1]) ).
cnf(t32318,plain,
big_t(term5,big_p(term5,X1,X2),X3) = big_p(term5,X1,big_p(term5,X2,X3)),
inference(step,[status(thm)],[t18,t76]) ).
cnf(f4,axiom,
big_p(term5,X,Y) = plus(X,Y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',big_p_term5) ).
fof(f4_nnf,plain,
! [X,Y] : big_p(term5,X,Y) = plus(X,Y),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X,Y] : big_p(term5,X,Y) = plus(X,Y),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
big_p(term5,X0,X1) = plus(X0,X1),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t11,plain,
big_p(term5,X1,X2) = plus(X1,X2),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t32311,plain,
big_t(term5,X1,X2) = plus(X1,X2),
inference(step,[status(thm)],[t11,t76]) ).
cnf(t400,plain,
big_t(term5,X1,X2) = plus(X1,X2),
inference(orient,[status(thm)],[t32311]) ).
cnf(t32319,plain,
plus(big_p(term5,X1,X2),X3) = big_p(term5,X1,big_p(term5,X2,X3)),
inference(step,[status(thm)],[t32318,t400]) ).
cnf(t32320,plain,
plus(big_t(term5,X1,X2),X3) = big_p(term5,X1,big_p(term5,X2,X3)),
inference(step,[status(thm)],[t32319,t76]) ).
cnf(t32321,plain,
plus(plus(X1,X2),X3) = big_p(term5,X1,big_p(term5,X2,X3)),
inference(step,[status(thm)],[t32320,t400]) ).
cnf(t32322,plain,
plus(plus(X1,X2),X3) = big_t(term5,X1,big_p(term5,X2,X3)),
inference(step,[status(thm)],[t32321,t76]) ).
cnf(t32323,plain,
plus(plus(X1,X2),X3) = plus(X1,big_p(term5,X2,X3)),
inference(step,[status(thm)],[t32322,t400]) ).
cnf(t32324,plain,
plus(plus(X1,X2),X3) = plus(X1,big_t(term5,X2,X3)),
inference(step,[status(thm)],[t32323,t76]) ).
cnf(t32325,plain,
plus(plus(X1,X2),X3) = plus(X1,plus(X2,X3)),
inference(step,[status(thm)],[t32324,t400]) ).
cnf(t421,plain,
plus(plus(X1,X2),X3) = plus(X1,plus(X2,X3)),
inference(orient,[status(thm)],[t32325]) ).
cnf(t32421,plain,
plus(X3,plus(X2,big_p(term6,big_t(term6,X1,X2),X3))) = big_p(term6,big_t(term6,X1,X2),X3),
inference(step,[status(thm)],[t32420,t421]) ).
cnf(t32422,plain,
plus(X3,plus(X2,big_t(term6,big_t(term6,X1,X2),X3))) = big_p(term6,big_t(term6,X1,X2),X3),
inference(step,[status(thm)],[t32421,t76]) ).
cnf(t32423,plain,
plus(X3,plus(X2,plus(X3,big_t(term6,X1,X2)))) = big_p(term6,big_t(term6,X1,X2),X3),
inference(step,[status(thm)],[t32422,t524]) ).
cnf(t32424,plain,
plus(X3,plus(X2,plus(X3,plus(X2,X1)))) = big_p(term6,big_t(term6,X1,X2),X3),
inference(step,[status(thm)],[t32423,t524]) ).
cnf(t32425,plain,
plus(X3,plus(X2,plus(X3,plus(X2,X1)))) = big_t(term6,big_t(term6,X1,X2),X3),
inference(step,[status(thm)],[t32424,t76]) ).
cnf(t32426,plain,
plus(X3,plus(X2,plus(X3,plus(X2,X1)))) = plus(X3,big_t(term6,X1,X2)),
inference(step,[status(thm)],[t32425,t524]) ).
cnf(t32427,plain,
plus(X3,plus(X2,plus(X3,plus(X2,X1)))) = plus(X3,plus(X2,X1)),
inference(step,[status(thm)],[t32426,t524]) ).
cnf(t622,plain,
plus(X1,plus(X2,plus(X1,plus(X2,X3)))) = plus(X1,plus(X2,X3)),
inference(orient,[status(thm)],[t32427]) ).
cnf(t55,plain,
big_t(term5,big_p(term6,big_t(term5,X1,X2),X3),big_p(term6,X2,X3)) = big_p(term6,big_t(term5,X1,X2),X3),
inference(hyper_resolution,[status(thm)],[hi15,hi11,hi12,hi1]) ).
cnf(t32407,plain,
plus(big_p(term6,big_t(term5,X1,X2),X3),big_p(term6,X2,X3)) = big_p(term6,big_t(term5,X1,X2),X3),
inference(step,[status(thm)],[t55,t400]) ).
cnf(t32408,plain,
plus(big_t(term6,big_t(term5,X1,X2),X3),big_p(term6,X2,X3)) = big_p(term6,big_t(term5,X1,X2),X3),
inference(step,[status(thm)],[t32407,t76]) ).
cnf(t32409,plain,
plus(plus(X3,big_t(term5,X1,X2)),big_p(term6,X2,X3)) = big_p(term6,big_t(term5,X1,X2),X3),
inference(step,[status(thm)],[t32408,t524]) ).
cnf(t32410,plain,
plus(X3,plus(big_t(term5,X1,X2),big_p(term6,X2,X3))) = big_p(term6,big_t(term5,X1,X2),X3),
inference(step,[status(thm)],[t32409,t421]) ).
cnf(t32411,plain,
plus(X3,plus(plus(X1,X2),big_p(term6,X2,X3))) = big_p(term6,big_t(term5,X1,X2),X3),
inference(step,[status(thm)],[t32410,t400]) ).
cnf(t32412,plain,
plus(X3,plus(X1,plus(X2,big_p(term6,X2,X3)))) = big_p(term6,big_t(term5,X1,X2),X3),
inference(step,[status(thm)],[t32411,t421]) ).
cnf(t32413,plain,
plus(X3,plus(X1,plus(X2,big_t(term6,X2,X3)))) = big_p(term6,big_t(term5,X1,X2),X3),
inference(step,[status(thm)],[t32412,t76]) ).
cnf(t32414,plain,
plus(X3,plus(X1,plus(X2,plus(X3,X2)))) = big_p(term6,big_t(term5,X1,X2),X3),
inference(step,[status(thm)],[t32413,t524]) ).
cnf(t32415,plain,
plus(X3,plus(X1,plus(X2,plus(X3,X2)))) = big_t(term6,big_t(term5,X1,X2),X3),
inference(step,[status(thm)],[t32414,t76]) ).
cnf(t32416,plain,
plus(X3,plus(X1,plus(X2,plus(X3,X2)))) = plus(X3,big_t(term5,X1,X2)),
inference(step,[status(thm)],[t32415,t524]) ).
cnf(t32417,plain,
plus(X3,plus(X1,plus(X2,plus(X3,X2)))) = plus(X3,plus(X1,X2)),
inference(step,[status(thm)],[t32416,t400]) ).
cnf(t598,plain,
plus(X1,plus(X2,plus(X3,plus(X1,X3)))) = plus(X1,plus(X2,X3)),
inference(orient,[status(thm)],[t32417]) ).
cnf(t1102,plain,
plus(b,plus(X1,sFlat2)) = plus(b,plus(X1,plus(sFlat2,sFlat6))),
inference(cp,[status(thm)],[t598,t1091]) ).
cnf(t3968,plain,
plus(b,plus(X1,plus(sFlat2,sFlat6))) = plus(b,plus(X1,sFlat2)),
inference(orient,[status(thm)],[t1102]) ).
cnf(t24,plain,
big_p(term5,big_p(term5,X1,X2),big_p(term5,X3,X4)) = big_p(term5,big_p(term5,X1,X3),big_p(term5,X2,X4)),
inference(hyper_resolution,[status(thm)],[hi14,hi11,hi1]) ).
cnf(t32326,plain,
big_t(term5,big_p(term5,X1,X2),big_p(term5,X3,X4)) = big_p(term5,big_p(term5,X1,X3),big_p(term5,X2,X4)),
inference(step,[status(thm)],[t24,t76]) ).
cnf(t32327,plain,
plus(big_p(term5,X1,X2),big_p(term5,X3,X4)) = big_p(term5,big_p(term5,X1,X3),big_p(term5,X2,X4)),
inference(step,[status(thm)],[t32326,t400]) ).
cnf(t32328,plain,
plus(big_t(term5,X1,X2),big_p(term5,X3,X4)) = big_p(term5,big_p(term5,X1,X3),big_p(term5,X2,X4)),
inference(step,[status(thm)],[t32327,t76]) ).
cnf(t32329,plain,
plus(plus(X1,X2),big_p(term5,X3,X4)) = big_p(term5,big_p(term5,X1,X3),big_p(term5,X2,X4)),
inference(step,[status(thm)],[t32328,t400]) ).
cnf(t32330,plain,
plus(X1,plus(X2,big_p(term5,X3,X4))) = big_p(term5,big_p(term5,X1,X3),big_p(term5,X2,X4)),
inference(step,[status(thm)],[t32329,t421]) ).
cnf(t32331,plain,
plus(X1,plus(X2,big_t(term5,X3,X4))) = big_p(term5,big_p(term5,X1,X3),big_p(term5,X2,X4)),
inference(step,[status(thm)],[t32330,t76]) ).
cnf(t32332,plain,
plus(X1,plus(X2,plus(X3,X4))) = big_p(term5,big_p(term5,X1,X3),big_p(term5,X2,X4)),
inference(step,[status(thm)],[t32331,t400]) ).
cnf(t32333,plain,
plus(X1,plus(X2,plus(X3,X4))) = big_t(term5,big_p(term5,X1,X3),big_p(term5,X2,X4)),
inference(step,[status(thm)],[t32332,t76]) ).
cnf(t32334,plain,
plus(X1,plus(X2,plus(X3,X4))) = plus(big_p(term5,X1,X3),big_p(term5,X2,X4)),
inference(step,[status(thm)],[t32333,t400]) ).
cnf(t32335,plain,
plus(X1,plus(X2,plus(X3,X4))) = plus(big_t(term5,X1,X3),big_p(term5,X2,X4)),
inference(step,[status(thm)],[t32334,t76]) ).
cnf(t32336,plain,
plus(X1,plus(X2,plus(X3,X4))) = plus(plus(X1,X3),big_p(term5,X2,X4)),
inference(step,[status(thm)],[t32335,t400]) ).
cnf(t32337,plain,
plus(X1,plus(X2,plus(X3,X4))) = plus(X1,plus(X3,big_p(term5,X2,X4))),
inference(step,[status(thm)],[t32336,t421]) ).
cnf(t32338,plain,
plus(X1,plus(X2,plus(X3,X4))) = plus(X1,plus(X3,big_t(term5,X2,X4))),
inference(step,[status(thm)],[t32337,t76]) ).
cnf(t32339,plain,
plus(X1,plus(X2,plus(X3,X4))) = plus(X1,plus(X3,plus(X2,X4))),
inference(step,[status(thm)],[t32338,t400]) ).
cnf(t422,plain,
plus(X1,plus(X2,plus(X3,X4))) = plus(X1,plus(X3,plus(X2,X4))),
inference(orient,[status(thm)],[t32339]) ).
cnf(t3971,plain,
plus(b,plus(X1,sFlat2)) = plus(b,plus(sFlat2,plus(X1,sFlat6))),
inference(cp,[status(thm)],[t3968,t422]) ).
cnf(t1092,plain,
plus(b,plus(sFlat2,X1)) = plus(sFlat6,X1),
inference(cp,[status(thm)],[t421,t1091]) ).
cnf(t1251,plain,
plus(b,plus(sFlat2,X1)) = plus(sFlat6,X1),
inference(orient,[status(thm)],[t1092]) ).
cnf(t32930,plain,
plus(b,plus(X1,sFlat2)) = plus(sFlat6,plus(X1,sFlat6)),
inference(step,[status(thm)],[t3971,t1251]) ).
cnf(t1265,plain,
plus(X1,plus(b,sFlat2)) = plus(X1,plus(sFlat6,plus(X1,sFlat2))),
inference(cp,[status(thm)],[t598,t1251]) ).
cnf(t32874,plain,
plus(X1,sFlat6) = plus(X1,plus(sFlat6,plus(X1,sFlat2))),
inference(step,[status(thm)],[t1265,t1091]) ).
cnf(t3402,plain,
plus(X1,plus(sFlat6,plus(X1,sFlat2))) = plus(X1,sFlat6),
inference(orient,[status(thm)],[t32874]) ).
cnf(t3411,plain,
plus(sFlat6,plus(X1,sFlat2)) = plus(sFlat6,plus(X1,sFlat6)),
inference(cp,[status(thm)],[t622,t3402]) ).
cnf(t3412,plain,
plus(sFlat6,plus(X1,sFlat6)) = plus(sFlat6,plus(X1,sFlat2)),
inference(orient,[status(thm)],[t3411]) ).
cnf(t32931,plain,
plus(b,plus(X1,sFlat2)) = plus(sFlat6,plus(X1,sFlat2)),
inference(step,[status(thm)],[t32930,t3412]) ).
cnf(t3986,plain,
plus(b,plus(X1,sFlat2)) = plus(sFlat6,plus(X1,sFlat2)),
inference(orient,[status(thm)],[t32931]) ).
cnf(t4006,plain,
plus(b,plus(X1,sFlat2)) = plus(b,plus(X1,plus(sFlat6,plus(X1,sFlat2)))),
inference(cp,[status(thm)],[t622,t3986]) ).
cnf(t32941,plain,
plus(sFlat6,plus(X1,sFlat2)) = plus(b,plus(X1,plus(sFlat6,plus(X1,sFlat2)))),
inference(step,[status(thm)],[t4006,t3986]) ).
cnf(t32942,plain,
plus(sFlat6,plus(X1,sFlat2)) = plus(b,plus(X1,sFlat6)),
inference(step,[status(thm)],[t32941,t3402]) ).
cnf(t4058,plain,
plus(b,plus(X1,sFlat6)) = plus(sFlat6,plus(X1,sFlat2)),
inference(orient,[status(thm)],[t32942]) ).
cnf(t64,plain,
ifeq(term(X1),true,ifeq(term(X2),true,big_t(X1,big_p(X2,big_t(X1,X3,X4),X5),big_p(X2,X4,X5)),big_p(X2,big_t(X1,X3,X4),X5)),big_p(X2,big_t(X1,X3,X4),X5)) = big_p(X2,big_t(X1,X3,X4),X5),
inference(equality_encoding,[status(esa)],[c15]) ).
cnf(t32238,plain,
ifeq(term(X1),true,ifeq(term(X2),true,big_t(X1,big_t(X2,big_t(X1,X3,X4),X5),big_p(X2,X4,X5)),big_p(X2,big_t(X1,X3,X4),X5)),big_p(X2,big_t(X1,X3,X4),X5)) = big_p(X2,big_t(X1,X3,X4),X5),
inference(step,[status(thm)],[t64,t76]) ).
cnf(t32239,plain,
ifeq(term(X1),true,ifeq(term(X2),true,big_t(X1,big_t(X2,big_t(X1,X3,X4),X5),big_t(X2,X4,X5)),big_p(X2,big_t(X1,X3,X4),X5)),big_p(X2,big_t(X1,X3,X4),X5)) = big_p(X2,big_t(X1,X3,X4),X5),
inference(step,[status(thm)],[t32238,t76]) ).
cnf(t32240,plain,
ifeq(term(X1),true,ifeq(term(X2),true,big_t(X1,big_t(X2,big_t(X1,X3,X4),X5),big_t(X2,X4,X5)),big_t(X2,big_t(X1,X3,X4),X5)),big_p(X2,big_t(X1,X3,X4),X5)) = big_p(X2,big_t(X1,X3,X4),X5),
inference(step,[status(thm)],[t32239,t76]) ).
cnf(t32241,plain,
ifeq(term(X1),true,ifeq(term(X2),true,big_t(X1,big_t(X2,big_t(X1,X3,X4),X5),big_t(X2,X4,X5)),big_t(X2,big_t(X1,X3,X4),X5)),big_t(X2,big_t(X1,X3,X4),X5)) = big_p(X2,big_t(X1,X3,X4),X5),
inference(step,[status(thm)],[t32240,t76]) ).
cnf(t32242,plain,
ifeq(term(X1),true,ifeq(term(X2),true,big_t(X1,big_t(X2,big_t(X1,X3,X4),X5),big_t(X2,X4,X5)),big_t(X2,big_t(X1,X3,X4),X5)),big_t(X2,big_t(X1,X3,X4),X5)) = big_t(X2,big_t(X1,X3,X4),X5),
inference(step,[status(thm)],[t32241,t76]) ).
cnf(t81,plain,
ifeq(term(X1),true,ifeq(term(X2),true,big_t(X1,big_t(X2,big_t(X1,X3,X4),X5),big_t(X2,X4,X5)),big_t(X2,big_t(X1,X3,X4),X5)),big_t(X2,big_t(X1,X3,X4),X5)) = big_t(X2,big_t(X1,X3,X4),X5),
inference(orient,[status(thm)],[t32242]) ).
cnf(f7,axiom,
term(term1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',term1) ).
fof(f7_nnf,plain,
term(term1),
inference(nnf_transformation,[status(thm)],[f7]) ).
cnf(c7,plain,
term(term1),
inference(cnf_transformation,[status(esa)],[f7_nnf]) ).
cnf(hi7,axiom,
term(term1) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t14,plain,
big_p(term1,big_p(term1,X1,X2),X3) = big_p(term1,X1,big_p(term1,X2,X3)),
inference(hyper_resolution,[status(thm)],[hi13,hi7,hi1]) ).
cnf(t32243,plain,
big_t(term1,big_p(term1,X1,X2),X3) = big_p(term1,X1,big_p(term1,X2,X3)),
inference(step,[status(thm)],[t14,t76]) ).
cnf(t32244,plain,
big_t(term1,big_t(term1,X1,X2),X3) = big_p(term1,X1,big_p(term1,X2,X3)),
inference(step,[status(thm)],[t32243,t76]) ).
cnf(t32245,plain,
big_t(term1,big_t(term1,X1,X2),X3) = big_t(term1,X1,big_p(term1,X2,X3)),
inference(step,[status(thm)],[t32244,t76]) ).
cnf(t32246,plain,
big_t(term1,big_t(term1,X1,X2),X3) = big_t(term1,X1,big_t(term1,X2,X3)),
inference(step,[status(thm)],[t32245,t76]) ).
cnf(t82,plain,
big_t(term1,big_t(term1,X1,X2),X3) = big_t(term1,X1,big_t(term1,X2,X3)),
inference(orient,[status(thm)],[t32246]) ).
cnf(t96,plain,
big_t(term1,big_t(X1,X2,big_t(term1,X3,X4)),X5) = ifeq(term(X1),true,ifeq(term(term1),true,big_t(X1,big_t(term1,big_t(X1,X2,big_t(term1,X3,X4)),X5),big_t(term1,X3,big_t(term1,X4,X5))),big_t(term1,big_t(X1,X2,big_t(term1,X3,X4)),X5)),big_t(term1,big_t(X1,X2,big_t(term1,X3,X4)),X5)),
inference(cp,[status(thm)],[t81,t82]) ).
cnf(f0,axiom,
big_p(term1,X,Y) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',big_p_term1) ).
fof(f0_nnf,plain,
! [X,Y] : big_p(term1,X,Y) = X,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,Y] : big_p(term1,X,Y) = X,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
big_p(term1,X0,X1) = X0,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t6,plain,
big_p(term1,X1,X2) = X1,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t73,plain,
big_p(term1,X1,X2) = X1,
inference(orient,[status(thm)],[t6]) ).
cnf(t32221,plain,
big_t(term1,X1,X2) = X1,
inference(step,[status(thm)],[t73,t76]) ).
cnf(t77,plain,
big_t(term1,X1,X2) = X1,
inference(rw,[status(thm)],[t32221]) ).
cnf(t1145,plain,
big_t(term1,X1,X2) = X1,
inference(orient,[status(thm)],[t77]) ).
cnf(t32723,plain,
big_t(X1,X2,big_t(term1,X3,X4)) = ifeq(term(X1),true,ifeq(term(term1),true,big_t(X1,big_t(term1,big_t(X1,X2,big_t(term1,X3,X4)),X5),big_t(term1,X3,big_t(term1,X4,X5))),big_t(term1,big_t(X1,X2,big_t(term1,X3,X4)),X5)),big_t(term1,big_t(X1,X2,big_t(term1,X3,X4)),X5)),
inference(step,[status(thm)],[t96,t1145]) ).
cnf(t32724,plain,
big_t(X1,X2,X3) = ifeq(term(X1),true,ifeq(term(term1),true,big_t(X1,big_t(term1,big_t(X1,X2,big_t(term1,X3,X4)),X5),big_t(term1,X3,big_t(term1,X4,X5))),big_t(term1,big_t(X1,X2,big_t(term1,X3,X4)),X5)),big_t(term1,big_t(X1,X2,big_t(term1,X3,X4)),X5)),
inference(step,[status(thm)],[t32723,t1145]) ).
cnf(t0,plain,
term(term1) = true,
inference(equality_encoding,[status(esa)],[c7]) ).
cnf(t1059,plain,
term(term1) = true,
inference(orient,[status(thm)],[t0]) ).
cnf(t32725,plain,
big_t(X1,X2,X3) = ifeq(term(X1),true,ifeq(true,true,big_t(X1,big_t(term1,big_t(X1,X2,big_t(term1,X3,X4)),X5),big_t(term1,X3,big_t(term1,X4,X5))),big_t(term1,big_t(X1,X2,big_t(term1,X3,X4)),X5)),big_t(term1,big_t(X1,X2,big_t(term1,X3,X4)),X5)),
inference(step,[status(thm)],[t32724,t1059]) ).
cnf(t8,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t75,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t8]) ).
cnf(t32726,plain,
big_t(X1,X2,X3) = ifeq(term(X1),true,big_t(X1,big_t(term1,big_t(X1,X2,big_t(term1,X3,X4)),X5),big_t(term1,X3,big_t(term1,X4,X5))),big_t(term1,big_t(X1,X2,big_t(term1,X3,X4)),X5)),
inference(step,[status(thm)],[t32725,t75]) ).
cnf(t32727,plain,
big_t(X1,X2,X3) = ifeq(term(X1),true,big_t(X1,big_t(X1,X2,big_t(term1,X3,X4)),big_t(term1,X3,big_t(term1,X4,X5))),big_t(term1,big_t(X1,X2,big_t(term1,X3,X4)),X5)),
inference(step,[status(thm)],[t32726,t1145]) ).
cnf(t32728,plain,
big_t(X1,X2,X3) = ifeq(term(X1),true,big_t(X1,big_t(X1,X2,X3),big_t(term1,X3,big_t(term1,X4,X5))),big_t(term1,big_t(X1,X2,big_t(term1,X3,X4)),X5)),
inference(step,[status(thm)],[t32727,t1145]) ).
cnf(t32729,plain,
big_t(X1,X2,X3) = ifeq(term(X1),true,big_t(X1,big_t(X1,X2,X3),X3),big_t(term1,big_t(X1,X2,big_t(term1,X3,X4)),X5)),
inference(step,[status(thm)],[t32728,t1145]) ).
cnf(t32730,plain,
big_t(X1,X2,X3) = ifeq(term(X1),true,big_t(X1,big_t(X1,X2,X3),X3),big_t(X1,X2,big_t(term1,X3,X4))),
inference(step,[status(thm)],[t32729,t1145]) ).
cnf(t32731,plain,
big_t(X1,X2,X3) = ifeq(term(X1),true,big_t(X1,big_t(X1,X2,X3),X3),big_t(X1,X2,X3)),
inference(step,[status(thm)],[t32730,t1145]) ).
cnf(t2053,plain,
ifeq(term(X1),true,big_t(X1,big_t(X1,X2,X3),X3),big_t(X1,X2,X3)) = big_t(X1,X2,X3),
inference(orient,[status(thm)],[t32731]) ).
cnf(t5,plain,
term(term6) = true,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(t1068,plain,
term(term6) = true,
inference(orient,[status(thm)],[t5]) ).
cnf(t2056,plain,
big_t(term6,X1,X2) = ifeq(true,true,big_t(term6,big_t(term6,X1,X2),X2),big_t(term6,X1,X2)),
inference(cp,[status(thm)],[t2053,t1068]) ).
cnf(t32754,plain,
plus(X2,X1) = ifeq(true,true,big_t(term6,big_t(term6,X1,X2),X2),big_t(term6,X1,X2)),
inference(step,[status(thm)],[t2056,t524]) ).
cnf(t32755,plain,
plus(X2,X1) = big_t(term6,big_t(term6,X1,X2),X2),
inference(step,[status(thm)],[t32754,t75]) ).
cnf(t32756,plain,
plus(X2,X1) = plus(X2,big_t(term6,X1,X2)),
inference(step,[status(thm)],[t32755,t524]) ).
cnf(t32757,plain,
plus(X2,X1) = plus(X2,plus(X2,X1)),
inference(step,[status(thm)],[t32756,t524]) ).
cnf(t2210,plain,
plus(X1,plus(X1,X2)) = plus(X1,X2),
inference(orient,[status(thm)],[t32757]) ).
cnf(t1201,plain,
plus(b,plus(sFlat3,X1)) = plus(sFlat4,X1),
inference(cp,[status(thm)],[t421,t1200]) ).
cnf(t1354,plain,
plus(b,plus(sFlat3,X1)) = plus(sFlat4,X1),
inference(orient,[status(thm)],[t1201]) ).
cnf(t2222,plain,
plus(b,plus(sFlat3,X1)) = plus(b,plus(sFlat4,X1)),
inference(cp,[status(thm)],[t2210,t1354]) ).
cnf(t32781,plain,
plus(sFlat4,X1) = plus(b,plus(sFlat4,X1)),
inference(step,[status(thm)],[t2222,t1354]) ).
cnf(t2396,plain,
plus(b,plus(sFlat4,X1)) = plus(sFlat4,X1),
inference(orient,[status(thm)],[t32781]) ).
cnf(t4059,plain,
plus(sFlat6,plus(sFlat4,sFlat2)) = plus(sFlat4,sFlat6),
inference(cp,[status(thm)],[t4058,t2396]) ).
cnf(t1254,plain,
plus(sFlat6,plus(X1,plus(b,X1))) = plus(b,plus(sFlat2,X1)),
inference(cp,[status(thm)],[t1251,t598]) ).
cnf(t32862,plain,
plus(sFlat6,plus(X1,plus(b,X1))) = plus(sFlat6,X1),
inference(step,[status(thm)],[t1254,t1251]) ).
cnf(t3322,plain,
plus(sFlat6,plus(X1,plus(b,X1))) = plus(sFlat6,X1),
inference(orient,[status(thm)],[t32862]) ).
cnf(t3327,plain,
plus(sFlat6,plus(sFlat3,X1)) = plus(sFlat6,plus(plus(sFlat3,X1),plus(sFlat4,X1))),
inference(cp,[status(thm)],[t3322,t1354]) ).
cnf(t32866,plain,
plus(sFlat6,plus(sFlat3,X1)) = plus(sFlat6,plus(sFlat4,plus(plus(sFlat3,X1),X1))),
inference(step,[status(thm)],[t3327,t422]) ).
cnf(t32867,plain,
plus(sFlat6,plus(sFlat3,X1)) = plus(sFlat6,plus(sFlat4,plus(sFlat3,plus(X1,X1)))),
inference(step,[status(thm)],[t32866,t421]) ).
cnf(t4,plain,
term(term5) = true,
inference(equality_encoding,[status(esa)],[c11]) ).
cnf(t1065,plain,
term(term5) = true,
inference(orient,[status(thm)],[t4]) ).
cnf(t2057,plain,
big_t(term5,X1,X2) = ifeq(true,true,big_t(term5,big_t(term5,X1,X2),X2),big_t(term5,X1,X2)),
inference(cp,[status(thm)],[t2053,t1065]) ).
cnf(t32764,plain,
plus(X1,X2) = ifeq(true,true,big_t(term5,big_t(term5,X1,X2),X2),big_t(term5,X1,X2)),
inference(step,[status(thm)],[t2057,t400]) ).
cnf(t32765,plain,
plus(X1,X2) = big_t(term5,big_t(term5,X1,X2),X2),
inference(step,[status(thm)],[t32764,t75]) ).
cnf(t32766,plain,
plus(X1,X2) = plus(big_t(term5,X1,X2),X2),
inference(step,[status(thm)],[t32765,t400]) ).
cnf(t32767,plain,
plus(X1,X2) = plus(plus(X1,X2),X2),
inference(step,[status(thm)],[t32766,t400]) ).
cnf(t32768,plain,
plus(X1,X2) = plus(X1,plus(X2,X2)),
inference(step,[status(thm)],[t32767,t421]) ).
cnf(t2267,plain,
plus(X1,plus(X2,X2)) = plus(X1,X2),
inference(orient,[status(thm)],[t32768]) ).
cnf(t32868,plain,
plus(sFlat6,plus(sFlat3,X1)) = plus(sFlat6,plus(sFlat4,plus(sFlat3,X1))),
inference(step,[status(thm)],[t32867,t2267]) ).
cnf(t2230,plain,
plus(sFlat4,plus(sFlat3,X1)) = plus(b,plus(sFlat3,X1)),
inference(cp,[status(thm)],[t1354,t2210]) ).
cnf(t32784,plain,
plus(sFlat4,plus(sFlat3,X1)) = plus(sFlat4,X1),
inference(step,[status(thm)],[t2230,t1354]) ).
cnf(t2432,plain,
plus(sFlat4,plus(sFlat3,X1)) = plus(sFlat4,X1),
inference(orient,[status(thm)],[t32784]) ).
cnf(t32869,plain,
plus(sFlat6,plus(sFlat3,X1)) = plus(sFlat6,plus(sFlat4,X1)),
inference(step,[status(thm)],[t32868,t2432]) ).
cnf(t3373,plain,
plus(sFlat6,plus(sFlat4,X1)) = plus(sFlat6,plus(sFlat3,X1)),
inference(orient,[status(thm)],[t32869]) ).
cnf(t32943,plain,
plus(sFlat6,plus(sFlat3,sFlat2)) = plus(sFlat4,sFlat6),
inference(step,[status(thm)],[t4059,t3373]) ).
cnf(t3990,plain,
plus(sFlat6,plus(sFlat4,sFlat2)) = plus(sFlat4,sFlat2),
inference(cp,[status(thm)],[t3986,t2396]) ).
cnf(t32937,plain,
plus(sFlat6,plus(sFlat3,sFlat2)) = plus(sFlat4,sFlat2),
inference(step,[status(thm)],[t3990,t3373]) ).
cnf(t4029,plain,
plus(sFlat6,plus(sFlat3,sFlat2)) = plus(sFlat4,sFlat2),
inference(orient,[status(thm)],[t32937]) ).
cnf(t32944,plain,
plus(sFlat4,sFlat2) = plus(sFlat4,sFlat6),
inference(step,[status(thm)],[t32943,t4029]) ).
cnf(t4072,plain,
plus(sFlat4,sFlat6) = plus(sFlat4,sFlat2),
inference(orient,[status(thm)],[t32944]) ).
cnf(t33830,plain,
times(plus(sFlat4,X1),sFlat6) = times(plus(sFlat4,X1),times(sFlat6,plus(sFlat4,sFlat2))),
inference(step,[status(thm)],[t33829,t4072]) ).
cnf(t63,plain,
ifeq(term(X1),true,big_p(X1,big_p(X1,X2,X3),big_p(X1,X4,X5)),big_p(X1,big_p(X1,X2,X4),big_p(X1,X3,X5))) = big_p(X1,big_p(X1,X2,X4),big_p(X1,X3,X5)),
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(t32229,plain,
ifeq(term(X1),true,big_t(X1,big_p(X1,X2,X3),big_p(X1,X4,X5)),big_p(X1,big_p(X1,X2,X4),big_p(X1,X3,X5))) = big_p(X1,big_p(X1,X2,X4),big_p(X1,X3,X5)),
inference(step,[status(thm)],[t63,t76]) ).
cnf(t32230,plain,
ifeq(term(X1),true,big_t(X1,big_t(X1,X2,X3),big_p(X1,X4,X5)),big_p(X1,big_p(X1,X2,X4),big_p(X1,X3,X5))) = big_p(X1,big_p(X1,X2,X4),big_p(X1,X3,X5)),
inference(step,[status(thm)],[t32229,t76]) ).
cnf(t32231,plain,
ifeq(term(X1),true,big_t(X1,big_t(X1,X2,X3),big_t(X1,X4,X5)),big_p(X1,big_p(X1,X2,X4),big_p(X1,X3,X5))) = big_p(X1,big_p(X1,X2,X4),big_p(X1,X3,X5)),
inference(step,[status(thm)],[t32230,t76]) ).
cnf(t32232,plain,
ifeq(term(X1),true,big_t(X1,big_t(X1,X2,X3),big_t(X1,X4,X5)),big_t(X1,big_p(X1,X2,X4),big_p(X1,X3,X5))) = big_p(X1,big_p(X1,X2,X4),big_p(X1,X3,X5)),
inference(step,[status(thm)],[t32231,t76]) ).
cnf(t32233,plain,
ifeq(term(X1),true,big_t(X1,big_t(X1,X2,X3),big_t(X1,X4,X5)),big_t(X1,big_t(X1,X2,X4),big_p(X1,X3,X5))) = big_p(X1,big_p(X1,X2,X4),big_p(X1,X3,X5)),
inference(step,[status(thm)],[t32232,t76]) ).
cnf(t32234,plain,
ifeq(term(X1),true,big_t(X1,big_t(X1,X2,X3),big_t(X1,X4,X5)),big_t(X1,big_t(X1,X2,X4),big_t(X1,X3,X5))) = big_p(X1,big_p(X1,X2,X4),big_p(X1,X3,X5)),
inference(step,[status(thm)],[t32233,t76]) ).
cnf(t32235,plain,
ifeq(term(X1),true,big_t(X1,big_t(X1,X2,X3),big_t(X1,X4,X5)),big_t(X1,big_t(X1,X2,X4),big_t(X1,X3,X5))) = big_t(X1,big_p(X1,X2,X4),big_p(X1,X3,X5)),
inference(step,[status(thm)],[t32234,t76]) ).
cnf(t32236,plain,
ifeq(term(X1),true,big_t(X1,big_t(X1,X2,X3),big_t(X1,X4,X5)),big_t(X1,big_t(X1,X2,X4),big_t(X1,X3,X5))) = big_t(X1,big_t(X1,X2,X4),big_p(X1,X3,X5)),
inference(step,[status(thm)],[t32235,t76]) ).
cnf(t32237,plain,
ifeq(term(X1),true,big_t(X1,big_t(X1,X2,X3),big_t(X1,X4,X5)),big_t(X1,big_t(X1,X2,X4),big_t(X1,X3,X5))) = big_t(X1,big_t(X1,X2,X4),big_t(X1,X3,X5)),
inference(step,[status(thm)],[t32236,t76]) ).
cnf(t80,plain,
ifeq(term(X1),true,big_t(X1,big_t(X1,X2,X3),big_t(X1,X4,X5)),big_t(X1,big_t(X1,X2,X4),big_t(X1,X3,X5))) = big_t(X1,big_t(X1,X2,X4),big_t(X1,X3,X5)),
inference(orient,[status(thm)],[t32237]) ).
cnf(t38,plain,
big_t(term3,big_p(term1,big_t(term3,X1,X2),X3),big_p(term1,X2,X3)) = big_p(term1,big_t(term3,X1,X2),X3),
inference(hyper_resolution,[status(thm)],[hi15,hi9,hi7,hi1]) ).
cnf(t32271,plain,
big_t(term3,big_t(term1,big_t(term3,X1,X2),X3),big_p(term1,X2,X3)) = big_p(term1,big_t(term3,X1,X2),X3),
inference(step,[status(thm)],[t38,t76]) ).
cnf(t32272,plain,
big_t(term3,big_t(term1,big_t(term3,X1,X2),X3),big_t(term1,X2,X3)) = big_p(term1,big_t(term3,X1,X2),X3),
inference(step,[status(thm)],[t32271,t76]) ).
cnf(t32273,plain,
big_t(term3,big_t(term1,big_t(term3,X1,X2),X3),big_t(term1,X2,X3)) = big_t(term1,big_t(term3,X1,X2),X3),
inference(step,[status(thm)],[t32272,t76]) ).
cnf(t195,plain,
big_t(term3,big_t(term1,big_t(term3,X1,X2),X3),big_t(term1,X2,X3)) = big_t(term1,big_t(term3,X1,X2),X3),
inference(orient,[status(thm)],[t32273]) ).
cnf(t200,plain,
big_t(term3,big_t(term3,X1,big_t(term1,big_t(term3,X2,X3),X4)),big_t(term3,X5,big_t(term1,X3,X4))) = ifeq(term(term3),true,big_t(term3,big_t(term3,X1,X5),big_t(term1,big_t(term3,X2,X3),X4)),big_t(term3,big_t(term3,X1,big_t(term1,big_t(term3,X2,X3),X4)),big_t(term3,X5,big_t(term1,X3,X4)))),
inference(cp,[status(thm)],[t80,t195]) ).
cnf(t33241,plain,
times(big_t(term3,X1,big_t(term1,big_t(term3,X2,X3),X4)),big_t(term3,X5,big_t(term1,X3,X4))) = ifeq(term(term3),true,big_t(term3,big_t(term3,X1,X5),big_t(term1,big_t(term3,X2,X3),X4)),big_t(term3,big_t(term3,X1,big_t(term1,big_t(term3,X2,X3),X4)),big_t(term3,X5,big_t(term1,X3,X4)))),
inference(step,[status(thm)],[t200,t685]) ).
cnf(t33242,plain,
times(times(X1,big_t(term1,big_t(term3,X2,X3),X4)),big_t(term3,X5,big_t(term1,X3,X4))) = ifeq(term(term3),true,big_t(term3,big_t(term3,X1,X5),big_t(term1,big_t(term3,X2,X3),X4)),big_t(term3,big_t(term3,X1,big_t(term1,big_t(term3,X2,X3),X4)),big_t(term3,X5,big_t(term1,X3,X4)))),
inference(step,[status(thm)],[t33241,t685]) ).
cnf(t33243,plain,
times(X1,times(big_t(term1,big_t(term3,X2,X3),X4),big_t(term3,X5,big_t(term1,X3,X4)))) = ifeq(term(term3),true,big_t(term3,big_t(term3,X1,X5),big_t(term1,big_t(term3,X2,X3),X4)),big_t(term3,big_t(term3,X1,big_t(term1,big_t(term3,X2,X3),X4)),big_t(term3,X5,big_t(term1,X3,X4)))),
inference(step,[status(thm)],[t33242,t708]) ).
cnf(t33244,plain,
times(X1,times(big_t(term3,X2,X3),big_t(term3,X5,big_t(term1,X3,X4)))) = ifeq(term(term3),true,big_t(term3,big_t(term3,X1,X5),big_t(term1,big_t(term3,X2,X3),X4)),big_t(term3,big_t(term3,X1,big_t(term1,big_t(term3,X2,X3),X4)),big_t(term3,X5,big_t(term1,X3,X4)))),
inference(step,[status(thm)],[t33243,t1145]) ).
cnf(t33245,plain,
times(X1,times(times(X2,X3),big_t(term3,X5,big_t(term1,X3,X4)))) = ifeq(term(term3),true,big_t(term3,big_t(term3,X1,X5),big_t(term1,big_t(term3,X2,X3),X4)),big_t(term3,big_t(term3,X1,big_t(term1,big_t(term3,X2,X3),X4)),big_t(term3,X5,big_t(term1,X3,X4)))),
inference(step,[status(thm)],[t33244,t685]) ).
cnf(t33246,plain,
times(X1,times(X2,times(X3,big_t(term3,X5,big_t(term1,X3,X4))))) = ifeq(term(term3),true,big_t(term3,big_t(term3,X1,X5),big_t(term1,big_t(term3,X2,X3),X4)),big_t(term3,big_t(term3,X1,big_t(term1,big_t(term3,X2,X3),X4)),big_t(term3,X5,big_t(term1,X3,X4)))),
inference(step,[status(thm)],[t33245,t708]) ).
cnf(t33247,plain,
times(X1,times(X2,times(X3,times(X5,big_t(term1,X3,X4))))) = ifeq(term(term3),true,big_t(term3,big_t(term3,X1,X5),big_t(term1,big_t(term3,X2,X3),X4)),big_t(term3,big_t(term3,X1,big_t(term1,big_t(term3,X2,X3),X4)),big_t(term3,X5,big_t(term1,X3,X4)))),
inference(step,[status(thm)],[t33246,t685]) ).
cnf(t33248,plain,
times(X1,times(X2,times(X3,times(X5,X3)))) = ifeq(term(term3),true,big_t(term3,big_t(term3,X1,X5),big_t(term1,big_t(term3,X2,X3),X4)),big_t(term3,big_t(term3,X1,big_t(term1,big_t(term3,X2,X3),X4)),big_t(term3,X5,big_t(term1,X3,X4)))),
inference(step,[status(thm)],[t33247,t1145]) ).
cnf(t2,plain,
term(term3) = true,
inference(equality_encoding,[status(esa)],[c9]) ).
cnf(t1071,plain,
term(term3) = true,
inference(orient,[status(thm)],[t2]) ).
cnf(t33249,plain,
times(X1,times(X2,times(X3,times(X5,X3)))) = ifeq(true,true,big_t(term3,big_t(term3,X1,X5),big_t(term1,big_t(term3,X2,X3),X4)),big_t(term3,big_t(term3,X1,big_t(term1,big_t(term3,X2,X3),X4)),big_t(term3,X5,big_t(term1,X3,X4)))),
inference(step,[status(thm)],[t33248,t1071]) ).
cnf(t33250,plain,
times(X1,times(X2,times(X3,times(X5,X3)))) = big_t(term3,big_t(term3,X1,X5),big_t(term1,big_t(term3,X2,X3),X4)),
inference(step,[status(thm)],[t33249,t75]) ).
cnf(t33251,plain,
times(X1,times(X2,times(X3,times(X5,X3)))) = times(big_t(term3,X1,X5),big_t(term1,big_t(term3,X2,X3),X4)),
inference(step,[status(thm)],[t33250,t685]) ).
cnf(t33252,plain,
times(X1,times(X2,times(X3,times(X5,X3)))) = times(times(X1,X5),big_t(term1,big_t(term3,X2,X3),X4)),
inference(step,[status(thm)],[t33251,t685]) ).
cnf(t33253,plain,
times(X1,times(X2,times(X3,times(X5,X3)))) = times(X1,times(X5,big_t(term1,big_t(term3,X2,X3),X4))),
inference(step,[status(thm)],[t33252,t708]) ).
cnf(t33254,plain,
times(X1,times(X2,times(X3,times(X5,X3)))) = times(X1,times(X5,big_t(term3,X2,X3))),
inference(step,[status(thm)],[t33253,t1145]) ).
cnf(t33255,plain,
times(X1,times(X2,times(X3,times(X5,X3)))) = times(X1,times(X5,times(X2,X3))),
inference(step,[status(thm)],[t33254,t685]) ).
cnf(t9600,plain,
times(X1,times(X2,times(X3,times(X4,X3)))) = times(X1,times(X4,times(X2,X3))),
inference(orient,[status(thm)],[t33255]) ).
cnf(f8,axiom,
term(term2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',term2) ).
fof(f8_nnf,plain,
term(term2),
inference(nnf_transformation,[status(thm)],[f8]) ).
cnf(c8,plain,
term(term2),
inference(cnf_transformation,[status(esa)],[f8_nnf]) ).
cnf(hi8,axiom,
term(term2) = true,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t32,plain,
big_t(term2,big_p(term1,big_t(term2,X1,X2),X3),big_p(term1,X2,X3)) = big_p(term1,big_t(term2,X1,X2),X3),
inference(hyper_resolution,[status(thm)],[hi15,hi8,hi7,hi1]) ).
cnf(t32262,plain,
big_t(term2,big_t(term1,big_t(term2,X1,X2),X3),big_p(term1,X2,X3)) = big_p(term1,big_t(term2,X1,X2),X3),
inference(step,[status(thm)],[t32,t76]) ).
cnf(t32263,plain,
big_t(term2,big_t(term1,big_t(term2,X1,X2),X3),big_t(term1,X2,X3)) = big_p(term1,big_t(term2,X1,X2),X3),
inference(step,[status(thm)],[t32262,t76]) ).
cnf(t32264,plain,
big_t(term2,big_t(term1,big_t(term2,X1,X2),X3),big_t(term1,X2,X3)) = big_t(term1,big_t(term2,X1,X2),X3),
inference(step,[status(thm)],[t32263,t76]) ).
cnf(t147,plain,
big_t(term2,big_t(term1,big_t(term2,X1,X2),X3),big_t(term1,X2,X3)) = big_t(term1,big_t(term2,X1,X2),X3),
inference(orient,[status(thm)],[t32264]) ).
cnf(t158,plain,
big_t(term2,big_t(X1,X2,big_t(term1,big_t(term2,X3,X4),X5)),big_t(term1,X4,X5)) = ifeq(term(X1),true,ifeq(term(term2),true,big_t(X1,big_t(term2,big_t(X1,X2,big_t(term1,big_t(term2,X3,X4),X5)),big_t(term1,X4,X5)),big_t(term1,big_t(term2,X3,X4),X5)),big_t(term2,big_t(X1,X2,big_t(term1,big_t(term2,X3,X4),X5)),big_t(term1,X4,X5))),big_t(term2,big_t(X1,X2,big_t(term1,big_t(term2,X3,X4),X5)),big_t(term1,X4,X5))),
inference(cp,[status(thm)],[t81,t147]) ).
cnf(f1,axiom,
big_p(term2,X,Y) = Y,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',big_p_term2) ).
fof(f1_nnf,plain,
! [X,Y] : big_p(term2,X,Y) = Y,
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,Y] : big_p(term2,X,Y) = Y,
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
big_p(term2,X0,X1) = X1,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t7,plain,
big_p(term2,X1,X2) = X2,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t74,plain,
big_p(term2,X1,X2) = X2,
inference(orient,[status(thm)],[t7]) ).
cnf(t32222,plain,
big_t(term2,X1,X2) = X2,
inference(step,[status(thm)],[t74,t76]) ).
cnf(t78,plain,
big_t(term2,X1,X2) = X2,
inference(rw,[status(thm)],[t32222]) ).
cnf(t1155,plain,
big_t(term2,X1,X2) = X2,
inference(orient,[status(thm)],[t78]) ).
cnf(t32794,plain,
big_t(term1,X4,X5) = ifeq(term(X1),true,ifeq(term(term2),true,big_t(X1,big_t(term2,big_t(X1,X2,big_t(term1,big_t(term2,X3,X4),X5)),big_t(term1,X4,X5)),big_t(term1,big_t(term2,X3,X4),X5)),big_t(term2,big_t(X1,X2,big_t(term1,big_t(term2,X3,X4),X5)),big_t(term1,X4,X5))),big_t(term2,big_t(X1,X2,big_t(term1,big_t(term2,X3,X4),X5)),big_t(term1,X4,X5))),
inference(step,[status(thm)],[t158,t1155]) ).
cnf(t32795,plain,
X4 = ifeq(term(X1),true,ifeq(term(term2),true,big_t(X1,big_t(term2,big_t(X1,X2,big_t(term1,big_t(term2,X3,X4),X5)),big_t(term1,X4,X5)),big_t(term1,big_t(term2,X3,X4),X5)),big_t(term2,big_t(X1,X2,big_t(term1,big_t(term2,X3,X4),X5)),big_t(term1,X4,X5))),big_t(term2,big_t(X1,X2,big_t(term1,big_t(term2,X3,X4),X5)),big_t(term1,X4,X5))),
inference(step,[status(thm)],[t32794,t1145]) ).
cnf(t1,plain,
term(term2) = true,
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(t1062,plain,
term(term2) = true,
inference(orient,[status(thm)],[t1]) ).
cnf(t32796,plain,
X4 = ifeq(term(X1),true,ifeq(true,true,big_t(X1,big_t(term2,big_t(X1,X2,big_t(term1,big_t(term2,X3,X4),X5)),big_t(term1,X4,X5)),big_t(term1,big_t(term2,X3,X4),X5)),big_t(term2,big_t(X1,X2,big_t(term1,big_t(term2,X3,X4),X5)),big_t(term1,X4,X5))),big_t(term2,big_t(X1,X2,big_t(term1,big_t(term2,X3,X4),X5)),big_t(term1,X4,X5))),
inference(step,[status(thm)],[t32795,t1062]) ).
cnf(t32797,plain,
X4 = ifeq(term(X1),true,big_t(X1,big_t(term2,big_t(X1,X2,big_t(term1,big_t(term2,X3,X4),X5)),big_t(term1,X4,X5)),big_t(term1,big_t(term2,X3,X4),X5)),big_t(term2,big_t(X1,X2,big_t(term1,big_t(term2,X3,X4),X5)),big_t(term1,X4,X5))),
inference(step,[status(thm)],[t32796,t75]) ).
cnf(t32798,plain,
X4 = ifeq(term(X1),true,big_t(X1,big_t(term1,X4,X5),big_t(term1,big_t(term2,X3,X4),X5)),big_t(term2,big_t(X1,X2,big_t(term1,big_t(term2,X3,X4),X5)),big_t(term1,X4,X5))),
inference(step,[status(thm)],[t32797,t1155]) ).
cnf(t32799,plain,
X4 = ifeq(term(X1),true,big_t(X1,X4,big_t(term1,big_t(term2,X3,X4),X5)),big_t(term2,big_t(X1,X2,big_t(term1,big_t(term2,X3,X4),X5)),big_t(term1,X4,X5))),
inference(step,[status(thm)],[t32798,t1145]) ).
cnf(t32800,plain,
X4 = ifeq(term(X1),true,big_t(X1,X4,big_t(term2,X3,X4)),big_t(term2,big_t(X1,X2,big_t(term1,big_t(term2,X3,X4),X5)),big_t(term1,X4,X5))),
inference(step,[status(thm)],[t32799,t1145]) ).
cnf(t32801,plain,
X4 = ifeq(term(X1),true,big_t(X1,X4,X4),big_t(term2,big_t(X1,X2,big_t(term1,big_t(term2,X3,X4),X5)),big_t(term1,X4,X5))),
inference(step,[status(thm)],[t32800,t1155]) ).
cnf(t32802,plain,
X4 = ifeq(term(X1),true,big_t(X1,X4,X4),big_t(term1,X4,X5)),
inference(step,[status(thm)],[t32801,t1155]) ).
cnf(t32803,plain,
X4 = ifeq(term(X1),true,big_t(X1,X4,X4),X4),
inference(step,[status(thm)],[t32802,t1145]) ).
cnf(t2542,plain,
ifeq(term(X1),true,big_t(X1,X2,X2),X2) = X2,
inference(orient,[status(thm)],[t32803]) ).
cnf(f10,axiom,
term(term4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',term4) ).
fof(f10_nnf,plain,
term(term4),
inference(nnf_transformation,[status(thm)],[f10]) ).
cnf(c10,plain,
term(term4),
inference(cnf_transformation,[status(esa)],[f10_nnf]) ).
cnf(t3,plain,
term(term4) = true,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t1074,plain,
term(term4) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(t2543,plain,
X1 = ifeq(true,true,big_t(term4,X1,X1),X1),
inference(cp,[status(thm)],[t2542,t1074]) ).
cnf(t32804,plain,
X1 = big_t(term4,X1,X1),
inference(step,[status(thm)],[t2543,t75]) ).
cnf(f3,axiom,
big_p(term4,X,Y) = times(Y,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',big_p_term4) ).
fof(f3_nnf,plain,
! [X,Y] : big_p(term4,X,Y) = times(Y,X),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X,Y] : big_p(term4,X,Y) = times(Y,X),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
big_p(term4,X0,X1) = times(X1,X0),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t10,plain,
big_p(term4,X1,X2) = times(X2,X1),
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t32523,plain,
big_t(term4,X1,X2) = times(X2,X1),
inference(step,[status(thm)],[t10,t76]) ).
cnf(t818,plain,
big_t(term4,X1,X2) = times(X2,X1),
inference(orient,[status(thm)],[t32523]) ).
cnf(t32805,plain,
X1 = times(X1,X1),
inference(step,[status(thm)],[t32804,t818]) ).
cnf(t2551,plain,
times(X1,X1) = X1,
inference(orient,[status(thm)],[t32805]) ).
cnf(t9645,plain,
times(X1,times(X2,times(times(X3,times(X2,X3)),X3))) = times(X1,times(X3,times(X2,X3))),
inference(cp,[status(thm)],[t9600,t2551]) ).
cnf(t33346,plain,
times(X1,times(X2,times(X3,times(times(X2,X3),X3)))) = times(X1,times(X3,times(X2,X3))),
inference(step,[status(thm)],[t9645,t708]) ).
cnf(t33347,plain,
times(X1,times(times(X2,X3),times(X2,X3))) = times(X1,times(X3,times(X2,X3))),
inference(step,[status(thm)],[t33346,t9600]) ).
cnf(t2055,plain,
big_t(term3,X1,X2) = ifeq(true,true,big_t(term3,big_t(term3,X1,X2),X2),big_t(term3,X1,X2)),
inference(cp,[status(thm)],[t2053,t1071]) ).
cnf(t32741,plain,
times(X1,X2) = ifeq(true,true,big_t(term3,big_t(term3,X1,X2),X2),big_t(term3,X1,X2)),
inference(step,[status(thm)],[t2055,t685]) ).
cnf(t32742,plain,
times(X1,X2) = big_t(term3,big_t(term3,X1,X2),X2),
inference(step,[status(thm)],[t32741,t75]) ).
cnf(t32743,plain,
times(X1,X2) = times(big_t(term3,X1,X2),X2),
inference(step,[status(thm)],[t32742,t685]) ).
cnf(t32744,plain,
times(X1,X2) = times(times(X1,X2),X2),
inference(step,[status(thm)],[t32743,t685]) ).
cnf(t32745,plain,
times(X1,X2) = times(X1,times(X2,X2)),
inference(step,[status(thm)],[t32744,t708]) ).
cnf(t2139,plain,
times(X1,times(X2,X2)) = times(X1,X2),
inference(orient,[status(thm)],[t32745]) ).
cnf(t33348,plain,
times(X1,times(X2,X3)) = times(X1,times(X3,times(X2,X3))),
inference(step,[status(thm)],[t33347,t2139]) ).
cnf(t11493,plain,
times(X1,times(X2,times(X3,X2))) = times(X1,times(X3,X2)),
inference(orient,[status(thm)],[t33348]) ).
cnf(t15561,plain,
plus(b,times(X1,sFlat3)) = times(plus(b,times(X1,sFlat3)),sFlat4),
inference(cp,[status(thm)],[t15029,t1200]) ).
cnf(t18456,plain,
times(plus(b,times(X1,sFlat3)),sFlat4) = plus(b,times(X1,sFlat3)),
inference(orient,[status(thm)],[t15561]) ).
cnf(t52,plain,
big_t(term5,big_p(term3,big_t(term5,X1,X2),X3),big_p(term3,X2,X3)) = big_p(term3,big_t(term5,X1,X2),X3),
inference(hyper_resolution,[status(thm)],[hi15,hi11,hi9,hi1]) ).
cnf(t32487,plain,
plus(big_p(term3,big_t(term5,X1,X2),X3),big_p(term3,X2,X3)) = big_p(term3,big_t(term5,X1,X2),X3),
inference(step,[status(thm)],[t52,t400]) ).
cnf(t32488,plain,
plus(big_t(term3,big_t(term5,X1,X2),X3),big_p(term3,X2,X3)) = big_p(term3,big_t(term5,X1,X2),X3),
inference(step,[status(thm)],[t32487,t76]) ).
cnf(t32489,plain,
plus(times(big_t(term5,X1,X2),X3),big_p(term3,X2,X3)) = big_p(term3,big_t(term5,X1,X2),X3),
inference(step,[status(thm)],[t32488,t685]) ).
cnf(t32490,plain,
plus(times(plus(X1,X2),X3),big_p(term3,X2,X3)) = big_p(term3,big_t(term5,X1,X2),X3),
inference(step,[status(thm)],[t32489,t400]) ).
cnf(t32491,plain,
plus(times(plus(X1,X2),X3),big_t(term3,X2,X3)) = big_p(term3,big_t(term5,X1,X2),X3),
inference(step,[status(thm)],[t32490,t76]) ).
cnf(t32492,plain,
plus(times(plus(X1,X2),X3),times(X2,X3)) = big_p(term3,big_t(term5,X1,X2),X3),
inference(step,[status(thm)],[t32491,t685]) ).
cnf(t32493,plain,
plus(times(plus(X1,X2),X3),times(X2,X3)) = big_t(term3,big_t(term5,X1,X2),X3),
inference(step,[status(thm)],[t32492,t76]) ).
cnf(t32494,plain,
plus(times(plus(X1,X2),X3),times(X2,X3)) = times(big_t(term5,X1,X2),X3),
inference(step,[status(thm)],[t32493,t685]) ).
cnf(t32495,plain,
plus(times(plus(X1,X2),X3),times(X2,X3)) = times(plus(X1,X2),X3),
inference(step,[status(thm)],[t32494,t400]) ).
cnf(t758,plain,
plus(times(plus(X1,X2),X3),times(X2,X3)) = times(plus(X1,X2),X3),
inference(orient,[status(thm)],[t32495]) ).
cnf(t1005,plain,
times(plus(b,c),times(d,sFlat1)) = plus(sFlat3,times(c,times(d,sFlat1))),
inference(cp,[status(thm)],[t758,t997]) ).
cnf(t32666,plain,
times(sFlat0,times(d,sFlat1)) = plus(sFlat3,times(c,times(d,sFlat1))),
inference(step,[status(thm)],[t1005,t1105]) ).
cnf(t32667,plain,
times(sFlat0,sFlat2) = plus(sFlat3,times(c,times(d,sFlat1))),
inference(step,[status(thm)],[t32666,t1015]) ).
cnf(t32668,plain,
sFlat3 = plus(sFlat3,times(c,times(d,sFlat1))),
inference(step,[status(thm)],[t32667,t1164]) ).
cnf(t32669,plain,
sFlat3 = plus(sFlat3,times(c,sFlat2)),
inference(step,[status(thm)],[t32668,t1015]) ).
cnf(t1574,plain,
plus(sFlat3,times(c,sFlat2)) = sFlat3,
inference(orient,[status(thm)],[t32669]) ).
cnf(hi10,axiom,
term(term4) = true,
inference(equality_encoding,[status(esa)],[c10]) ).
cnf(t41,plain,
big_t(term3,big_p(term4,big_t(term3,X1,X2),X3),big_p(term4,X2,X3)) = big_p(term4,big_t(term3,X1,X2),X3),
inference(hyper_resolution,[status(thm)],[hi15,hi9,hi10,hi1]) ).
cnf(t32572,plain,
times(big_p(term4,big_t(term3,X1,X2),X3),big_p(term4,X2,X3)) = big_p(term4,big_t(term3,X1,X2),X3),
inference(step,[status(thm)],[t41,t685]) ).
cnf(t32573,plain,
times(big_t(term4,big_t(term3,X1,X2),X3),big_p(term4,X2,X3)) = big_p(term4,big_t(term3,X1,X2),X3),
inference(step,[status(thm)],[t32572,t76]) ).
cnf(t32574,plain,
times(times(X3,big_t(term3,X1,X2)),big_p(term4,X2,X3)) = big_p(term4,big_t(term3,X1,X2),X3),
inference(step,[status(thm)],[t32573,t818]) ).
cnf(t32575,plain,
times(X3,times(big_t(term3,X1,X2),big_p(term4,X2,X3))) = big_p(term4,big_t(term3,X1,X2),X3),
inference(step,[status(thm)],[t32574,t708]) ).
cnf(t32576,plain,
times(X3,times(times(X1,X2),big_p(term4,X2,X3))) = big_p(term4,big_t(term3,X1,X2),X3),
inference(step,[status(thm)],[t32575,t685]) ).
cnf(t32577,plain,
times(X3,times(X1,times(X2,big_p(term4,X2,X3)))) = big_p(term4,big_t(term3,X1,X2),X3),
inference(step,[status(thm)],[t32576,t708]) ).
cnf(t32578,plain,
times(X3,times(X1,times(X2,big_t(term4,X2,X3)))) = big_p(term4,big_t(term3,X1,X2),X3),
inference(step,[status(thm)],[t32577,t76]) ).
cnf(t32579,plain,
times(X3,times(X1,times(X2,times(X3,X2)))) = big_p(term4,big_t(term3,X1,X2),X3),
inference(step,[status(thm)],[t32578,t818]) ).
cnf(t32580,plain,
times(X3,times(X1,times(X2,times(X3,X2)))) = big_t(term4,big_t(term3,X1,X2),X3),
inference(step,[status(thm)],[t32579,t76]) ).
cnf(t32581,plain,
times(X3,times(X1,times(X2,times(X3,X2)))) = times(X3,big_t(term3,X1,X2)),
inference(step,[status(thm)],[t32580,t818]) ).
cnf(t32582,plain,
times(X3,times(X1,times(X2,times(X3,X2)))) = times(X3,times(X1,X2)),
inference(step,[status(thm)],[t32581,t685]) ).
cnf(t939,plain,
times(X1,times(X2,times(X3,times(X1,X3)))) = times(X1,times(X2,X3)),
inference(orient,[status(thm)],[t32582]) ).
cnf(t995,plain,
times(c,times(X1,e)) = times(c,times(X1,times(e,sFlat1))),
inference(cp,[status(thm)],[t939,t984]) ).
cnf(t3760,plain,
times(c,times(X1,times(e,sFlat1))) = times(c,times(X1,e)),
inference(orient,[status(thm)],[t995]) ).
cnf(t3761,plain,
times(c,times(X1,e)) = times(c,times(e,times(X1,sFlat1))),
inference(cp,[status(thm)],[t3760,t709]) ).
cnf(t985,plain,
times(c,times(e,X1)) = times(sFlat1,X1),
inference(cp,[status(thm)],[t708,t984]) ).
cnf(t1209,plain,
times(c,times(e,X1)) = times(sFlat1,X1),
inference(orient,[status(thm)],[t985]) ).
cnf(t32909,plain,
times(c,times(X1,e)) = times(sFlat1,times(X1,sFlat1)),
inference(step,[status(thm)],[t3761,t1209]) ).
cnf(t3773,plain,
times(c,times(X1,e)) = times(sFlat1,times(X1,sFlat1)),
inference(orient,[status(thm)],[t32909]) ).
cnf(t1016,plain,
times(d,times(sFlat1,X1)) = times(sFlat2,X1),
inference(cp,[status(thm)],[t708,t1015]) ).
cnf(t1230,plain,
times(d,times(sFlat1,X1)) = times(sFlat2,X1),
inference(orient,[status(thm)],[t1016]) ).
cnf(t47,plain,
big_t(term4,big_p(term4,big_t(term4,X1,X2),X3),big_p(term4,X2,X3)) = big_p(term4,big_t(term4,X1,X2),X3),
inference(hyper_resolution,[status(thm)],[hi15,hi10,hi10,hi1]) ).
cnf(t32583,plain,
times(big_p(term4,X2,X3),big_p(term4,big_t(term4,X1,X2),X3)) = big_p(term4,big_t(term4,X1,X2),X3),
inference(step,[status(thm)],[t47,t818]) ).
cnf(t32584,plain,
times(big_t(term4,X2,X3),big_p(term4,big_t(term4,X1,X2),X3)) = big_p(term4,big_t(term4,X1,X2),X3),
inference(step,[status(thm)],[t32583,t76]) ).
cnf(t32585,plain,
times(times(X3,X2),big_p(term4,big_t(term4,X1,X2),X3)) = big_p(term4,big_t(term4,X1,X2),X3),
inference(step,[status(thm)],[t32584,t818]) ).
cnf(t32586,plain,
times(X3,times(X2,big_p(term4,big_t(term4,X1,X2),X3))) = big_p(term4,big_t(term4,X1,X2),X3),
inference(step,[status(thm)],[t32585,t708]) ).
cnf(t32587,plain,
times(X3,times(X2,big_t(term4,big_t(term4,X1,X2),X3))) = big_p(term4,big_t(term4,X1,X2),X3),
inference(step,[status(thm)],[t32586,t76]) ).
cnf(t32588,plain,
times(X3,times(X2,times(X3,big_t(term4,X1,X2)))) = big_p(term4,big_t(term4,X1,X2),X3),
inference(step,[status(thm)],[t32587,t818]) ).
cnf(t32589,plain,
times(X3,times(X2,times(X3,times(X2,X1)))) = big_p(term4,big_t(term4,X1,X2),X3),
inference(step,[status(thm)],[t32588,t818]) ).
cnf(t32590,plain,
times(X3,times(X2,times(X3,times(X2,X1)))) = big_t(term4,big_t(term4,X1,X2),X3),
inference(step,[status(thm)],[t32589,t76]) ).
cnf(t32591,plain,
times(X3,times(X2,times(X3,times(X2,X1)))) = times(X3,big_t(term4,X1,X2)),
inference(step,[status(thm)],[t32590,t818]) ).
cnf(t32592,plain,
times(X3,times(X2,times(X3,times(X2,X1)))) = times(X3,times(X2,X1)),
inference(step,[status(thm)],[t32591,t818]) ).
cnf(t965,plain,
times(X1,times(X2,times(X1,times(X2,X3)))) = times(X1,times(X2,X3)),
inference(orient,[status(thm)],[t32592]) ).
cnf(t1210,plain,
times(sFlat1,times(c,times(e,X1))) = times(c,times(e,X1)),
inference(cp,[status(thm)],[t1209,t965]) ).
cnf(t32618,plain,
times(sFlat1,times(sFlat1,X1)) = times(c,times(e,X1)),
inference(step,[status(thm)],[t1210,t1209]) ).
cnf(t32619,plain,
times(sFlat1,times(sFlat1,X1)) = times(sFlat1,X1),
inference(step,[status(thm)],[t32618,t1209]) ).
cnf(t1375,plain,
times(sFlat1,times(sFlat1,X1)) = times(sFlat1,X1),
inference(orient,[status(thm)],[t32619]) ).
cnf(t1379,plain,
times(sFlat2,times(sFlat1,X1)) = times(d,times(sFlat1,X1)),
inference(cp,[status(thm)],[t1230,t1375]) ).
cnf(t32659,plain,
times(sFlat2,times(sFlat1,X1)) = times(sFlat2,X1),
inference(step,[status(thm)],[t1379,t1230]) ).
cnf(t1521,plain,
times(sFlat2,times(sFlat1,X1)) = times(sFlat2,X1),
inference(orient,[status(thm)],[t32659]) ).
cnf(t2142,plain,
times(c,e) = times(sFlat1,e),
inference(cp,[status(thm)],[t2139,t1209]) ).
cnf(t32748,plain,
sFlat1 = times(sFlat1,e),
inference(step,[status(thm)],[t2142,t984]) ).
cnf(t2166,plain,
times(sFlat1,e) = sFlat1,
inference(orient,[status(thm)],[t32748]) ).
cnf(t2170,plain,
times(sFlat2,e) = times(sFlat2,sFlat1),
inference(cp,[status(thm)],[t1521,t2166]) ).
cnf(t40,plain,
big_t(term3,big_p(term3,big_t(term3,X1,X2),X3),big_p(term3,X2,X3)) = big_p(term3,big_t(term3,X1,X2),X3),
inference(hyper_resolution,[status(thm)],[hi15,hi9,hi9,hi1]) ).
cnf(t32505,plain,
times(big_p(term3,big_t(term3,X1,X2),X3),big_p(term3,X2,X3)) = big_p(term3,big_t(term3,X1,X2),X3),
inference(step,[status(thm)],[t40,t685]) ).
cnf(t32506,plain,
times(big_t(term3,big_t(term3,X1,X2),X3),big_p(term3,X2,X3)) = big_p(term3,big_t(term3,X1,X2),X3),
inference(step,[status(thm)],[t32505,t76]) ).
cnf(t32507,plain,
times(times(big_t(term3,X1,X2),X3),big_p(term3,X2,X3)) = big_p(term3,big_t(term3,X1,X2),X3),
inference(step,[status(thm)],[t32506,t685]) ).
cnf(t32508,plain,
times(big_t(term3,X1,X2),times(X3,big_p(term3,X2,X3))) = big_p(term3,big_t(term3,X1,X2),X3),
inference(step,[status(thm)],[t32507,t708]) ).
cnf(t32509,plain,
times(times(X1,X2),times(X3,big_p(term3,X2,X3))) = big_p(term3,big_t(term3,X1,X2),X3),
inference(step,[status(thm)],[t32508,t685]) ).
cnf(t32510,plain,
times(X1,times(X2,times(X3,big_p(term3,X2,X3)))) = big_p(term3,big_t(term3,X1,X2),X3),
inference(step,[status(thm)],[t32509,t708]) ).
cnf(t32511,plain,
times(X1,times(X2,times(X3,big_t(term3,X2,X3)))) = big_p(term3,big_t(term3,X1,X2),X3),
inference(step,[status(thm)],[t32510,t76]) ).
cnf(t32512,plain,
times(X1,times(X2,times(X3,times(X2,X3)))) = big_p(term3,big_t(term3,X1,X2),X3),
inference(step,[status(thm)],[t32511,t685]) ).
cnf(t32513,plain,
times(X1,times(X2,times(X3,times(X2,X3)))) = big_t(term3,big_t(term3,X1,X2),X3),
inference(step,[status(thm)],[t32512,t76]) ).
cnf(t32514,plain,
times(X1,times(X2,times(X3,times(X2,X3)))) = times(big_t(term3,X1,X2),X3),
inference(step,[status(thm)],[t32513,t685]) ).
cnf(t32515,plain,
times(X1,times(X2,times(X3,times(X2,X3)))) = times(times(X1,X2),X3),
inference(step,[status(thm)],[t32514,t685]) ).
cnf(t32516,plain,
times(X1,times(X2,times(X3,times(X2,X3)))) = times(X1,times(X2,X3)),
inference(step,[status(thm)],[t32515,t708]) ).
cnf(t789,plain,
times(X1,times(X2,times(X3,times(X2,X3)))) = times(X1,times(X2,X3)),
inference(orient,[status(thm)],[t32516]) ).
cnf(t1226,plain,
times(X1,times(c,e)) = times(X1,times(sFlat1,times(c,e))),
inference(cp,[status(thm)],[t789,t1209]) ).
cnf(t32620,plain,
times(X1,sFlat1) = times(X1,times(sFlat1,times(c,e))),
inference(step,[status(thm)],[t1226,t984]) ).
cnf(t32621,plain,
times(X1,sFlat1) = times(X1,times(sFlat1,sFlat1)),
inference(step,[status(thm)],[t32620,t984]) ).
cnf(t1386,plain,
times(X1,times(sFlat1,sFlat1)) = times(X1,sFlat1),
inference(orient,[status(thm)],[t32621]) ).
cnf(t1387,plain,
times(d,sFlat1) = times(sFlat2,sFlat1),
inference(cp,[status(thm)],[t1386,t1230]) ).
cnf(t32622,plain,
sFlat2 = times(sFlat2,sFlat1),
inference(step,[status(thm)],[t1387,t1015]) ).
cnf(t1391,plain,
times(sFlat2,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t32622]) ).
cnf(t32753,plain,
times(sFlat2,e) = sFlat2,
inference(step,[status(thm)],[t2170,t1391]) ).
cnf(t2201,plain,
times(sFlat2,e) = sFlat2,
inference(orient,[status(thm)],[t32753]) ).
cnf(t3777,plain,
times(sFlat1,times(sFlat2,sFlat1)) = times(c,sFlat2),
inference(cp,[status(thm)],[t3773,t2201]) ).
cnf(t32915,plain,
times(sFlat1,sFlat2) = times(c,sFlat2),
inference(step,[status(thm)],[t3777,t1391]) ).
cnf(t3801,plain,
times(c,sFlat2) = times(sFlat1,sFlat2),
inference(orient,[status(thm)],[t32915]) ).
cnf(t32917,plain,
plus(sFlat3,times(sFlat1,sFlat2)) = sFlat3,
inference(step,[status(thm)],[t1574,t3801]) ).
cnf(t3810,plain,
plus(sFlat3,times(sFlat1,sFlat2)) = sFlat3,
inference(rw,[status(thm)],[t32917]) ).
cnf(t3839,plain,
plus(sFlat3,times(sFlat1,sFlat2)) = sFlat3,
inference(orient,[status(thm)],[t3810]) ).
cnf(t15449,plain,
plus(sFlat3,times(X1,times(sFlat1,sFlat2))) = times(plus(sFlat3,times(X1,times(sFlat1,sFlat2))),sFlat3),
inference(cp,[status(thm)],[t15029,t3839]) ).
cnf(t1249,plain,
times(X1,times(sFlat1,times(d,X2))) = times(X1,times(sFlat2,X2)),
inference(cp,[status(thm)],[t709,t1230]) ).
cnf(t1234,plain,
times(sFlat2,times(X1,X2)) = times(d,times(X1,times(sFlat1,X2))),
inference(cp,[status(thm)],[t1230,t709]) ).
cnf(t5327,plain,
times(d,times(X1,times(sFlat1,X2))) = times(sFlat2,times(X1,X2)),
inference(orient,[status(thm)],[t1234]) ).
cnf(t5352,plain,
times(sFlat1,times(d,X1)) = times(sFlat1,times(sFlat2,times(X1,X1))),
inference(cp,[status(thm)],[t939,t5327]) ).
cnf(t32998,plain,
times(sFlat1,times(d,X1)) = times(sFlat1,times(sFlat2,X1)),
inference(step,[status(thm)],[t5352,t2139]) ).
cnf(t5355,plain,
times(sFlat1,times(d,X1)) = times(sFlat1,times(sFlat2,X1)),
inference(orient,[status(thm)],[t32998]) ).
cnf(t32999,plain,
times(X1,times(sFlat1,times(sFlat2,X2))) = times(X1,times(sFlat2,X2)),
inference(step,[status(thm)],[t1249,t5355]) ).
cnf(t5365,plain,
times(X1,times(sFlat1,times(sFlat2,X2))) = times(X1,times(sFlat2,X2)),
inference(orient,[status(thm)],[t32999]) ).
cnf(t5366,plain,
times(X1,times(sFlat2,times(X1,sFlat2))) = times(X1,times(sFlat1,sFlat2)),
inference(cp,[status(thm)],[t5365,t939]) ).
cnf(t2580,plain,
times(X1,times(times(X2,times(X1,X2)),X2)) = times(X1,times(X2,times(X1,X2))),
inference(cp,[status(thm)],[t939,t2551]) ).
cnf(t2681,plain,
times(X1,times(X2,times(X1,X2))) = times(X1,X2),
inference(orient,[status(thm)],[t2580]) ).
cnf(t33000,plain,
times(X1,sFlat2) = times(X1,times(sFlat1,sFlat2)),
inference(step,[status(thm)],[t5366,t2681]) ).
cnf(t5387,plain,
times(X1,times(sFlat1,sFlat2)) = times(X1,sFlat2),
inference(orient,[status(thm)],[t33000]) ).
cnf(t33715,plain,
plus(sFlat3,times(X1,sFlat2)) = times(plus(sFlat3,times(X1,times(sFlat1,sFlat2))),sFlat3),
inference(step,[status(thm)],[t15449,t5387]) ).
cnf(t33716,plain,
plus(sFlat3,times(X1,sFlat2)) = times(plus(sFlat3,times(X1,sFlat2)),sFlat3),
inference(step,[status(thm)],[t33715,t5387]) ).
cnf(t19295,plain,
times(plus(sFlat3,times(X1,sFlat2)),sFlat3) = plus(sFlat3,times(X1,sFlat2)),
inference(orient,[status(thm)],[t33716]) ).
cnf(t2054,plain,
big_t(term4,X1,X2) = ifeq(true,true,big_t(term4,big_t(term4,X1,X2),X2),big_t(term4,X1,X2)),
inference(cp,[status(thm)],[t2053,t1074]) ).
cnf(t32732,plain,
times(X2,X1) = ifeq(true,true,big_t(term4,big_t(term4,X1,X2),X2),big_t(term4,X1,X2)),
inference(step,[status(thm)],[t2054,t818]) ).
cnf(t32733,plain,
times(X2,X1) = big_t(term4,big_t(term4,X1,X2),X2),
inference(step,[status(thm)],[t32732,t75]) ).
cnf(t32734,plain,
times(X2,X1) = times(X2,big_t(term4,X1,X2)),
inference(step,[status(thm)],[t32733,t818]) ).
cnf(t32735,plain,
times(X2,X1) = times(X2,times(X2,X1)),
inference(step,[status(thm)],[t32734,t818]) ).
cnf(t2070,plain,
times(X1,times(X1,X2)) = times(X1,X2),
inference(orient,[status(thm)],[t32735]) ).
cnf(t2080,plain,
times(d,sFlat1) = times(d,sFlat2),
inference(cp,[status(thm)],[t2070,t1015]) ).
cnf(t32739,plain,
sFlat2 = times(d,sFlat2),
inference(step,[status(thm)],[t2080,t1015]) ).
cnf(t2125,plain,
times(d,sFlat2) = sFlat2,
inference(orient,[status(thm)],[t32739]) ).
cnf(t19302,plain,
plus(sFlat3,times(d,sFlat2)) = times(plus(sFlat3,sFlat2),sFlat3),
inference(cp,[status(thm)],[t19295,t2125]) ).
cnf(t33717,plain,
plus(sFlat3,sFlat2) = times(plus(sFlat3,sFlat2),sFlat3),
inference(step,[status(thm)],[t19302,t2125]) ).
cnf(t19330,plain,
times(plus(sFlat3,sFlat2),sFlat3) = plus(sFlat3,sFlat2),
inference(orient,[status(thm)],[t33717]) ).
cnf(t19338,plain,
plus(b,times(plus(sFlat3,sFlat2),sFlat3)) = times(plus(b,plus(sFlat3,sFlat2)),sFlat4),
inference(cp,[status(thm)],[t18456,t19330]) ).
cnf(t33729,plain,
plus(b,plus(sFlat3,sFlat2)) = times(plus(b,plus(sFlat3,sFlat2)),sFlat4),
inference(step,[status(thm)],[t19338,t19330]) ).
cnf(t33730,plain,
plus(sFlat4,sFlat2) = times(plus(b,plus(sFlat3,sFlat2)),sFlat4),
inference(step,[status(thm)],[t33729,t1354]) ).
cnf(t33731,plain,
plus(sFlat4,sFlat2) = times(plus(sFlat4,sFlat2),sFlat4),
inference(step,[status(thm)],[t33730,t1354]) ).
cnf(t19432,plain,
times(plus(sFlat4,sFlat2),sFlat4) = plus(sFlat4,sFlat2),
inference(orient,[status(thm)],[t33731]) ).
cnf(t19439,plain,
times(X1,times(plus(sFlat4,sFlat2),sFlat4)) = times(X1,times(sFlat4,plus(sFlat4,sFlat2))),
inference(cp,[status(thm)],[t11493,t19432]) ).
cnf(t33740,plain,
times(X1,plus(sFlat4,sFlat2)) = times(X1,times(sFlat4,plus(sFlat4,sFlat2))),
inference(step,[status(thm)],[t19439,t19432]) ).
cnf(t1575,plain,
plus(sFlat4,times(c,sFlat2)) = plus(b,sFlat3),
inference(cp,[status(thm)],[t1354,t1574]) ).
cnf(t32670,plain,
plus(sFlat4,times(c,sFlat2)) = sFlat4,
inference(step,[status(thm)],[t1575,t1200]) ).
cnf(t1584,plain,
plus(sFlat4,times(c,sFlat2)) = sFlat4,
inference(orient,[status(thm)],[t32670]) ).
cnf(t32916,plain,
plus(sFlat4,times(sFlat1,sFlat2)) = sFlat4,
inference(step,[status(thm)],[t1584,t3801]) ).
cnf(t3809,plain,
plus(sFlat4,times(sFlat1,sFlat2)) = sFlat4,
inference(rw,[status(thm)],[t32916]) ).
cnf(t3829,plain,
plus(sFlat4,times(sFlat1,sFlat2)) = sFlat4,
inference(orient,[status(thm)],[t3809]) ).
cnf(t15066,plain,
plus(sFlat4,times(sFlat1,sFlat2)) = times(sFlat4,plus(sFlat4,sFlat2)),
inference(cp,[status(thm)],[t15029,t3829]) ).
cnf(t33525,plain,
sFlat4 = times(sFlat4,plus(sFlat4,sFlat2)),
inference(step,[status(thm)],[t15066,t3829]) ).
cnf(t15623,plain,
times(sFlat4,plus(sFlat4,sFlat2)) = sFlat4,
inference(orient,[status(thm)],[t33525]) ).
cnf(t33741,plain,
times(X1,plus(sFlat4,sFlat2)) = times(X1,sFlat4),
inference(step,[status(thm)],[t33740,t15623]) ).
cnf(t19527,plain,
times(X1,plus(sFlat4,sFlat2)) = times(X1,sFlat4),
inference(orient,[status(thm)],[t33741]) ).
cnf(t33831,plain,
times(plus(sFlat4,X1),sFlat6) = times(plus(sFlat4,X1),times(sFlat6,sFlat4)),
inference(step,[status(thm)],[t33830,t19527]) ).
cnf(t16217,plain,
times(X1,times(sFlat4,sFlat6)) = times(X1,times(sFlat6,sFlat4)),
inference(cp,[status(thm)],[t11493,t16207]) ).
cnf(t33591,plain,
times(X1,sFlat4) = times(X1,times(sFlat6,sFlat4)),
inference(step,[status(thm)],[t16217,t16207]) ).
cnf(t16521,plain,
times(X1,times(sFlat6,sFlat4)) = times(X1,sFlat4),
inference(orient,[status(thm)],[t33591]) ).
cnf(t33832,plain,
times(plus(sFlat4,X1),sFlat6) = times(plus(sFlat4,X1),sFlat4),
inference(step,[status(thm)],[t33831,t16521]) ).
cnf(t21496,plain,
times(plus(sFlat4,X1),sFlat6) = times(plus(sFlat4,X1),sFlat4),
inference(orient,[status(thm)],[t33832]) ).
cnf(t1109,plain,
times(plus(b,c),X1) = plus(times(b,X1),times(sFlat0,X1)),
inference(cp,[status(thm)],[t774,t1105]) ).
cnf(t32721,plain,
times(sFlat0,X1) = plus(times(b,X1),times(sFlat0,X1)),
inference(step,[status(thm)],[t1109,t1105]) ).
cnf(t1999,plain,
plus(times(b,X1),times(sFlat0,X1)) = times(sFlat0,X1),
inference(orient,[status(thm)],[t32721]) ).
cnf(t2554,plain,
times(sFlat0,b) = plus(b,times(sFlat0,b)),
inference(cp,[status(thm)],[t1999,t2551]) ).
cnf(t2617,plain,
plus(b,times(sFlat0,b)) = times(sFlat0,b),
inference(orient,[status(thm)],[t2554]) ).
cnf(t2618,plain,
plus(b,plus(times(sFlat0,b),X1)) = plus(times(sFlat0,b),X1),
inference(cp,[status(thm)],[t421,t2617]) ).
cnf(t9912,plain,
plus(b,plus(times(sFlat0,b),X1)) = plus(times(sFlat0,b),X1),
inference(orient,[status(thm)],[t2618]) ).
cnf(t59,plain,
big_t(term6,big_p(term4,big_t(term6,X1,X2),X3),big_p(term4,X2,X3)) = big_p(term4,big_t(term6,X1,X2),X3),
inference(hyper_resolution,[status(thm)],[hi15,hi12,hi10,hi1]) ).
cnf(t32563,plain,
plus(big_p(term4,X2,X3),big_p(term4,big_t(term6,X1,X2),X3)) = big_p(term4,big_t(term6,X1,X2),X3),
inference(step,[status(thm)],[t59,t524]) ).
cnf(t32564,plain,
plus(big_t(term4,X2,X3),big_p(term4,big_t(term6,X1,X2),X3)) = big_p(term4,big_t(term6,X1,X2),X3),
inference(step,[status(thm)],[t32563,t76]) ).
cnf(t32565,plain,
plus(times(X3,X2),big_p(term4,big_t(term6,X1,X2),X3)) = big_p(term4,big_t(term6,X1,X2),X3),
inference(step,[status(thm)],[t32564,t818]) ).
cnf(t32566,plain,
plus(times(X3,X2),big_t(term4,big_t(term6,X1,X2),X3)) = big_p(term4,big_t(term6,X1,X2),X3),
inference(step,[status(thm)],[t32565,t76]) ).
cnf(t32567,plain,
plus(times(X3,X2),times(X3,big_t(term6,X1,X2))) = big_p(term4,big_t(term6,X1,X2),X3),
inference(step,[status(thm)],[t32566,t818]) ).
cnf(t32568,plain,
plus(times(X3,X2),times(X3,plus(X2,X1))) = big_p(term4,big_t(term6,X1,X2),X3),
inference(step,[status(thm)],[t32567,t524]) ).
cnf(t32569,plain,
plus(times(X3,X2),times(X3,plus(X2,X1))) = big_t(term4,big_t(term6,X1,X2),X3),
inference(step,[status(thm)],[t32568,t76]) ).
cnf(t32570,plain,
plus(times(X3,X2),times(X3,plus(X2,X1))) = times(X3,big_t(term6,X1,X2)),
inference(step,[status(thm)],[t32569,t818]) ).
cnf(t32571,plain,
plus(times(X3,X2),times(X3,plus(X2,X1))) = times(X3,plus(X2,X1)),
inference(step,[status(thm)],[t32570,t524]) ).
cnf(t919,plain,
plus(times(X1,X2),times(X1,plus(X2,X3))) = times(X1,plus(X2,X3)),
inference(orient,[status(thm)],[t32571]) ).
cnf(t1093,plain,
times(X1,plus(b,sFlat2)) = plus(times(X1,b),times(X1,sFlat6)),
inference(cp,[status(thm)],[t919,t1091]) ).
cnf(t32711,plain,
times(X1,sFlat6) = plus(times(X1,b),times(X1,sFlat6)),
inference(step,[status(thm)],[t1093,t1091]) ).
cnf(t1858,plain,
plus(times(X1,b),times(X1,sFlat6)) = times(X1,sFlat6),
inference(orient,[status(thm)],[t32711]) ).
cnf(t9926,plain,
plus(times(sFlat0,b),times(sFlat0,sFlat6)) = plus(b,times(sFlat0,sFlat6)),
inference(cp,[status(thm)],[t9912,t1858]) ).
cnf(t33262,plain,
times(sFlat0,sFlat6) = plus(b,times(sFlat0,sFlat6)),
inference(step,[status(thm)],[t9926,t1858]) ).
cnf(t1358,plain,
plus(sFlat4,plus(X1,X2)) = plus(b,plus(X1,plus(sFlat3,X2))),
inference(cp,[status(thm)],[t1354,t422]) ).
cnf(t8579,plain,
plus(b,plus(X1,plus(sFlat3,X2))) = plus(sFlat4,plus(X1,X2)),
inference(orient,[status(thm)],[t1358]) ).
cnf(t2545,plain,
X1 = ifeq(true,true,big_t(term6,X1,X1),X1),
inference(cp,[status(thm)],[t2542,t1068]) ).
cnf(t32806,plain,
X1 = big_t(term6,X1,X1),
inference(step,[status(thm)],[t2545,t75]) ).
cnf(t32807,plain,
X1 = plus(X1,X1),
inference(step,[status(thm)],[t32806,t524]) ).
cnf(t2581,plain,
plus(X1,X1) = X1,
inference(orient,[status(thm)],[t32807]) ).
cnf(t8604,plain,
plus(sFlat4,plus(X1,sFlat3)) = plus(b,plus(X1,sFlat3)),
inference(cp,[status(thm)],[t8579,t2581]) ).
cnf(t8691,plain,
plus(b,plus(X1,sFlat3)) = plus(sFlat4,plus(X1,sFlat3)),
inference(orient,[status(thm)],[t8604]) ).
cnf(t53,plain,
big_t(term5,big_p(term4,big_t(term5,X1,X2),X3),big_p(term4,X2,X3)) = big_p(term4,big_t(term5,X1,X2),X3),
inference(hyper_resolution,[status(thm)],[hi15,hi11,hi10,hi1]) ).
cnf(t32554,plain,
plus(big_p(term4,big_t(term5,X1,X2),X3),big_p(term4,X2,X3)) = big_p(term4,big_t(term5,X1,X2),X3),
inference(step,[status(thm)],[t53,t400]) ).
cnf(t32555,plain,
plus(big_t(term4,big_t(term5,X1,X2),X3),big_p(term4,X2,X3)) = big_p(term4,big_t(term5,X1,X2),X3),
inference(step,[status(thm)],[t32554,t76]) ).
cnf(t32556,plain,
plus(times(X3,big_t(term5,X1,X2)),big_p(term4,X2,X3)) = big_p(term4,big_t(term5,X1,X2),X3),
inference(step,[status(thm)],[t32555,t818]) ).
cnf(t32557,plain,
plus(times(X3,plus(X1,X2)),big_p(term4,X2,X3)) = big_p(term4,big_t(term5,X1,X2),X3),
inference(step,[status(thm)],[t32556,t400]) ).
cnf(t32558,plain,
plus(times(X3,plus(X1,X2)),big_t(term4,X2,X3)) = big_p(term4,big_t(term5,X1,X2),X3),
inference(step,[status(thm)],[t32557,t76]) ).
cnf(t32559,plain,
plus(times(X3,plus(X1,X2)),times(X3,X2)) = big_p(term4,big_t(term5,X1,X2),X3),
inference(step,[status(thm)],[t32558,t818]) ).
cnf(t32560,plain,
plus(times(X3,plus(X1,X2)),times(X3,X2)) = big_t(term4,big_t(term5,X1,X2),X3),
inference(step,[status(thm)],[t32559,t76]) ).
cnf(t32561,plain,
plus(times(X3,plus(X1,X2)),times(X3,X2)) = times(X3,big_t(term5,X1,X2)),
inference(step,[status(thm)],[t32560,t818]) ).
cnf(t32562,plain,
plus(times(X3,plus(X1,X2)),times(X3,X2)) = times(X3,plus(X1,X2)),
inference(step,[status(thm)],[t32561,t400]) ).
cnf(t898,plain,
plus(times(X1,plus(X2,X3)),times(X1,X3)) = times(X1,plus(X2,X3)),
inference(orient,[status(thm)],[t32562]) ).
cnf(t1094,plain,
times(X1,plus(b,sFlat2)) = plus(times(X1,sFlat6),times(X1,sFlat2)),
inference(cp,[status(thm)],[t898,t1091]) ).
cnf(t32712,plain,
times(X1,sFlat6) = plus(times(X1,sFlat6),times(X1,sFlat2)),
inference(step,[status(thm)],[t1094,t1091]) ).
cnf(t1869,plain,
plus(times(X1,sFlat6),times(X1,sFlat2)) = times(X1,sFlat6),
inference(orient,[status(thm)],[t32712]) ).
cnf(t1873,plain,
times(sFlat0,sFlat6) = plus(times(sFlat0,sFlat6),sFlat3),
inference(cp,[status(thm)],[t1869,t1164]) ).
cnf(t1883,plain,
plus(times(sFlat0,sFlat6),sFlat3) = times(sFlat0,sFlat6),
inference(orient,[status(thm)],[t1873]) ).
cnf(t8703,plain,
plus(sFlat4,plus(times(sFlat0,sFlat6),sFlat3)) = plus(b,times(sFlat0,sFlat6)),
inference(cp,[status(thm)],[t8691,t1883]) ).
cnf(t33205,plain,
plus(sFlat4,times(sFlat0,sFlat6)) = plus(b,times(sFlat0,sFlat6)),
inference(step,[status(thm)],[t8703,t1883]) ).
cnf(t8830,plain,
plus(b,times(sFlat0,sFlat6)) = plus(sFlat4,times(sFlat0,sFlat6)),
inference(orient,[status(thm)],[t33205]) ).
cnf(t33263,plain,
times(sFlat0,sFlat6) = plus(sFlat4,times(sFlat0,sFlat6)),
inference(step,[status(thm)],[t33262,t8830]) ).
cnf(t9981,plain,
plus(sFlat4,times(sFlat0,sFlat6)) = times(sFlat0,sFlat6),
inference(orient,[status(thm)],[t33263]) ).
cnf(t21498,plain,
times(plus(sFlat4,times(sFlat0,sFlat6)),sFlat4) = times(times(sFlat0,sFlat6),sFlat6),
inference(cp,[status(thm)],[t21496,t9981]) ).
cnf(t33833,plain,
times(times(sFlat0,sFlat6),sFlat4) = times(times(sFlat0,sFlat6),sFlat6),
inference(step,[status(thm)],[t21498,t9981]) ).
cnf(t33834,plain,
times(sFlat0,times(sFlat6,sFlat4)) = times(times(sFlat0,sFlat6),sFlat6),
inference(step,[status(thm)],[t33833,t708]) ).
cnf(t33835,plain,
times(sFlat0,sFlat4) = times(times(sFlat0,sFlat6),sFlat6),
inference(step,[status(thm)],[t33834,t16521]) ).
cnf(t33836,plain,
times(sFlat0,sFlat4) = times(sFlat0,times(sFlat6,sFlat6)),
inference(step,[status(thm)],[t33835,t708]) ).
cnf(t33837,plain,
times(sFlat0,sFlat4) = times(sFlat0,sFlat6),
inference(step,[status(thm)],[t33836,t2139]) ).
cnf(t21518,plain,
times(sFlat0,sFlat6) = times(sFlat0,sFlat4),
inference(orient,[status(thm)],[t33837]) ).
cnf(t21519,plain,
times(sFlat0,times(sFlat6,X1)) = times(times(sFlat0,sFlat4),X1),
inference(cp,[status(thm)],[t708,t21518]) ).
cnf(t33864,plain,
times(sFlat0,times(sFlat6,X1)) = times(sFlat0,times(sFlat4,X1)),
inference(step,[status(thm)],[t21519,t708]) ).
cnf(t21622,plain,
times(sFlat0,times(sFlat6,X1)) = times(sFlat0,times(sFlat4,X1)),
inference(orient,[status(thm)],[t33864]) ).
cnf(t21645,plain,
times(sFlat7,times(sFlat0,X1)) = times(a,times(sFlat0,times(sFlat4,X1))),
inference(cp,[status(thm)],[t7936,t21622]) ).
cnf(t1120,plain,
times(a,times(sFlat4,X1)) = times(sFlat5,X1),
inference(cp,[status(thm)],[t708,t1119]) ).
cnf(t1293,plain,
times(a,times(sFlat4,X1)) = times(sFlat5,X1),
inference(orient,[status(thm)],[t1120]) ).
cnf(t1297,plain,
times(sFlat5,times(X1,X2)) = times(a,times(X1,times(sFlat4,X2))),
inference(cp,[status(thm)],[t1293,t709]) ).
cnf(t7821,plain,
times(a,times(X1,times(sFlat4,X2))) = times(sFlat5,times(X1,X2)),
inference(orient,[status(thm)],[t1297]) ).
cnf(t33891,plain,
times(sFlat7,times(sFlat0,X1)) = times(sFlat5,times(sFlat0,X1)),
inference(step,[status(thm)],[t21645,t7821]) ).
cnf(t22145,plain,
times(sFlat7,times(sFlat0,X1)) = times(sFlat5,times(sFlat0,X1)),
inference(orient,[status(thm)],[t33891]) ).
cnf(t49,plain,
big_t(term4,big_p(term6,big_t(term4,X1,X2),X3),big_p(term6,X2,X3)) = big_p(term6,big_t(term4,X1,X2),X3),
inference(hyper_resolution,[status(thm)],[hi15,hi10,hi12,hi1]) ).
cnf(t32434,plain,
big_t(term4,big_t(term6,big_t(term4,X1,X2),X3),big_p(term6,X2,X3)) = big_p(term6,big_t(term4,X1,X2),X3),
inference(step,[status(thm)],[t49,t76]) ).
cnf(t32435,plain,
big_t(term4,plus(X3,big_t(term4,X1,X2)),big_p(term6,X2,X3)) = big_p(term6,big_t(term4,X1,X2),X3),
inference(step,[status(thm)],[t32434,t524]) ).
cnf(t32436,plain,
big_t(term4,plus(X3,big_t(term4,X1,X2)),big_t(term6,X2,X3)) = big_p(term6,big_t(term4,X1,X2),X3),
inference(step,[status(thm)],[t32435,t76]) ).
cnf(t32437,plain,
big_t(term4,plus(X3,big_t(term4,X1,X2)),plus(X3,X2)) = big_p(term6,big_t(term4,X1,X2),X3),
inference(step,[status(thm)],[t32436,t524]) ).
cnf(t32438,plain,
big_t(term4,plus(X3,big_t(term4,X1,X2)),plus(X3,X2)) = big_t(term6,big_t(term4,X1,X2),X3),
inference(step,[status(thm)],[t32437,t76]) ).
cnf(t32439,plain,
big_t(term4,plus(X3,big_t(term4,X1,X2)),plus(X3,X2)) = plus(X3,big_t(term4,X1,X2)),
inference(step,[status(thm)],[t32438,t524]) ).
cnf(t662,plain,
big_t(term4,plus(X1,big_t(term4,X2,X3)),plus(X1,X3)) = plus(X1,big_t(term4,X2,X3)),
inference(orient,[status(thm)],[t32439]) ).
cnf(t32530,plain,
times(plus(X1,X3),plus(X1,big_t(term4,X2,X3))) = plus(X1,big_t(term4,X2,X3)),
inference(step,[status(thm)],[t662,t818]) ).
cnf(t32531,plain,
times(plus(X1,X3),plus(X1,times(X3,X2))) = plus(X1,big_t(term4,X2,X3)),
inference(step,[status(thm)],[t32530,t818]) ).
cnf(t32532,plain,
times(plus(X1,X3),plus(X1,times(X3,X2))) = plus(X1,times(X3,X2)),
inference(step,[status(thm)],[t32531,t818]) ).
cnf(t838,plain,
times(plus(X1,X3),plus(X1,times(X3,X2))) = plus(X1,times(X3,X2)),
inference(rw,[status(thm)],[t32532]) ).
cnf(t30311,plain,
times(plus(X1,X2),plus(X1,times(X2,X3))) = plus(X1,times(X2,X3)),
inference(orient,[status(thm)],[t838]) ).
cnf(t30902,plain,
plus(X1,times(c,e)) = times(plus(X1,c),plus(X1,sFlat1)),
inference(cp,[status(thm)],[t30311,t984]) ).
cnf(t34315,plain,
plus(X1,sFlat1) = times(plus(X1,c),plus(X1,sFlat1)),
inference(step,[status(thm)],[t30902,t984]) ).
cnf(t32096,plain,
times(plus(X1,c),plus(X1,sFlat1)) = plus(X1,sFlat1),
inference(orient,[status(thm)],[t34315]) ).
cnf(t32108,plain,
plus(b,sFlat1) = times(sFlat0,plus(b,sFlat1)),
inference(cp,[status(thm)],[t32096,t1105]) ).
cnf(t32161,plain,
times(sFlat0,plus(b,sFlat1)) = plus(b,sFlat1),
inference(orient,[status(thm)],[t32108]) ).
cnf(t32163,plain,
times(sFlat5,times(sFlat0,plus(b,sFlat1))) = times(sFlat7,plus(b,sFlat1)),
inference(cp,[status(thm)],[t22145,t32161]) ).
cnf(t34316,plain,
times(sFlat5,plus(b,sFlat1)) = times(sFlat7,plus(b,sFlat1)),
inference(step,[status(thm)],[t32163,t32161]) ).
cnf(t2096,plain,
times(sFlat5,times(sFlat4,X1)) = times(a,times(sFlat4,X1)),
inference(cp,[status(thm)],[t1293,t2070]) ).
cnf(t32779,plain,
times(sFlat5,times(sFlat4,X1)) = times(sFlat5,X1),
inference(step,[status(thm)],[t2096,t1293]) ).
cnf(t2369,plain,
times(sFlat5,times(sFlat4,X1)) = times(sFlat5,X1),
inference(orient,[status(thm)],[t32779]) ).
cnf(t16212,plain,
times(sFlat5,sFlat6) = times(sFlat5,sFlat4),
inference(cp,[status(thm)],[t2369,t16207]) ).
cnf(t2140,plain,
times(a,sFlat4) = times(sFlat5,sFlat4),
inference(cp,[status(thm)],[t2139,t1293]) ).
cnf(t32746,plain,
sFlat5 = times(sFlat5,sFlat4),
inference(step,[status(thm)],[t2140,t1119]) ).
cnf(t2145,plain,
times(sFlat5,sFlat4) = sFlat5,
inference(orient,[status(thm)],[t32746]) ).
cnf(t33565,plain,
times(sFlat5,sFlat6) = sFlat5,
inference(step,[status(thm)],[t16212,t2145]) ).
cnf(t16229,plain,
times(sFlat5,sFlat6) = sFlat5,
inference(orient,[status(thm)],[t33565]) ).
cnf(t16232,plain,
times(sFlat5,times(sFlat6,X1)) = times(sFlat5,X1),
inference(cp,[status(thm)],[t708,t16229]) ).
cnf(t16324,plain,
times(sFlat5,times(sFlat6,X1)) = times(sFlat5,X1),
inference(orient,[status(thm)],[t16232]) ).
cnf(t15212,plain,
plus(X1,times(d,sFlat1)) = times(plus(X1,sFlat2),plus(X1,sFlat1)),
inference(cp,[status(thm)],[t15029,t1015]) ).
cnf(t33615,plain,
plus(X1,sFlat2) = times(plus(X1,sFlat2),plus(X1,sFlat1)),
inference(step,[status(thm)],[t15212,t1015]) ).
cnf(t16843,plain,
times(plus(X1,sFlat2),plus(X1,sFlat1)) = plus(X1,sFlat2),
inference(orient,[status(thm)],[t33615]) ).
cnf(t16859,plain,
plus(b,sFlat2) = times(sFlat6,plus(b,sFlat1)),
inference(cp,[status(thm)],[t16843,t1091]) ).
cnf(t33618,plain,
sFlat6 = times(sFlat6,plus(b,sFlat1)),
inference(step,[status(thm)],[t16859,t1091]) ).
cnf(t16931,plain,
times(sFlat6,plus(b,sFlat1)) = sFlat6,
inference(orient,[status(thm)],[t33618]) ).
cnf(t16933,plain,
times(sFlat5,plus(b,sFlat1)) = times(sFlat5,sFlat6),
inference(cp,[status(thm)],[t16324,t16931]) ).
cnf(t33642,plain,
times(sFlat5,plus(b,sFlat1)) = sFlat5,
inference(step,[status(thm)],[t16933,t16229]) ).
cnf(t17442,plain,
times(sFlat5,plus(b,sFlat1)) = sFlat5,
inference(orient,[status(thm)],[t33642]) ).
cnf(t34317,plain,
sFlat5 = times(sFlat7,plus(b,sFlat1)),
inference(step,[status(thm)],[t34316,t17442]) ).
cnf(t2095,plain,
times(sFlat7,times(sFlat6,X1)) = times(a,times(sFlat6,X1)),
inference(cp,[status(thm)],[t1314,t2070]) ).
cnf(t32778,plain,
times(sFlat7,times(sFlat6,X1)) = times(sFlat7,X1),
inference(step,[status(thm)],[t2095,t1314]) ).
cnf(t2356,plain,
times(sFlat7,times(sFlat6,X1)) = times(sFlat7,X1),
inference(orient,[status(thm)],[t32778]) ).
cnf(t16935,plain,
times(sFlat7,plus(b,sFlat1)) = times(sFlat7,sFlat6),
inference(cp,[status(thm)],[t2356,t16931]) ).
cnf(t2141,plain,
times(a,sFlat6) = times(sFlat7,sFlat6),
inference(cp,[status(thm)],[t2139,t1314]) ).
cnf(t32747,plain,
sFlat7 = times(sFlat7,sFlat6),
inference(step,[status(thm)],[t2141,t1132]) ).
cnf(t2155,plain,
times(sFlat7,sFlat6) = sFlat7,
inference(orient,[status(thm)],[t32747]) ).
cnf(t33644,plain,
times(sFlat7,plus(b,sFlat1)) = sFlat7,
inference(step,[status(thm)],[t16935,t2155]) ).
cnf(t17482,plain,
times(sFlat7,plus(b,sFlat1)) = sFlat7,
inference(orient,[status(thm)],[t33644]) ).
cnf(t34318,plain,
sFlat5 = sFlat7,
inference(step,[status(thm)],[t34317,t17482]) ).
cnf(t32179,plain,
sFlat7 = sFlat5,
inference(orient,[status(thm)],[t34318]) ).
cnf(t34319,plain,
times(a,sFlat6) = sFlat5,
inference(step,[status(thm)],[t1132,t32179]) ).
cnf(t32180,plain,
times(a,sFlat6) = sFlat5,
inference(orient,[status(thm)],[t34319]) ).
cnf(f16,negated_conjecture,
times(a,plus(b,times(d,times(c,e)))) != times(a,plus(b,times(plus(b,c),times(d,times(c,e))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_q4) ).
fof(f16_nnf,plain,
times(a,plus(b,times(d,times(c,e)))) != times(a,plus(b,times(plus(b,c),times(d,times(c,e))))),
inference(nnf_transformation,[status(thm)],[f16]) ).
fof(f16_sk,plain,
times(a,plus(b,times(d,times(c,e)))) != times(a,plus(b,times(plus(b,c),times(d,times(c,e))))),
inference(skolemisation,[status(esa)],[f16_nnf]) ).
cnf(c16,plain,
times(a,plus(b,times(d,times(c,e)))) != times(a,plus(b,times(plus(b,c),times(d,times(c,e))))),
inference(cnf_transformation,[status(esa)],[f16_sk]) ).
cnf(goal_0,negated_conjecture,
times(a,plus(b,times(plus(b,c),times(d,times(c,e))))) != times(a,plus(b,times(d,times(c,e)))),
inference(equality_encoding,[status(esa)],[c16]) ).
cnf(g0_0,plain,
times(a,plus(b,times(sFlat0,times(d,times(c,e))))) != times(a,plus(b,times(d,times(c,e)))),
inference(rw,[status(thm)],[goal_0,t1105]) ).
cnf(g0_1,plain,
times(a,plus(b,times(sFlat0,times(d,sFlat1)))) != times(a,plus(b,times(d,times(c,e)))),
inference(rw,[status(thm)],[g0_0,t984]) ).
cnf(g0_2,plain,
times(a,plus(b,times(sFlat0,sFlat2))) != times(a,plus(b,times(d,times(c,e)))),
inference(rw,[status(thm)],[g0_1,t1015]) ).
cnf(g0_3,plain,
times(a,plus(b,sFlat3)) != times(a,plus(b,times(d,times(c,e)))),
inference(rw,[status(thm)],[g0_2,t1164]) ).
cnf(g0_4,plain,
times(a,sFlat4) != times(a,plus(b,times(d,times(c,e)))),
inference(rw,[status(thm)],[g0_3,t1200]) ).
cnf(g0_5,plain,
sFlat5 != times(a,plus(b,times(d,times(c,e)))),
inference(rw,[status(thm)],[g0_4,t1119]) ).
cnf(g0_6,plain,
sFlat5 != times(a,plus(b,times(d,sFlat1))),
inference(rw,[status(thm)],[g0_5,t984]) ).
cnf(g0_7,plain,
sFlat5 != times(a,plus(b,sFlat2)),
inference(rw,[status(thm)],[g0_6,t1015]) ).
cnf(g0_8,plain,
sFlat5 != times(a,sFlat6),
inference(rw,[status(thm)],[g0_7,t1091]) ).
cnf(g0_9,plain,
sFlat5 != sFlat5,
inference(rw,[status(thm)],[g0_8,t32180]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_9]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT041-1 : TPTP v9.3.1. Released v2.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.13/0.39 % Computer : n008.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Wed Sep 23 20:05:41 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 67.37/9.12 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 67.37/9.12 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------