%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT393-1 : TPTP v9.3.1. Released v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n015.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:57:06 PM UTC 2026
% Result : Unsatisfiable 65.47s 8.86s
% Output : CNFRefutation 65.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 103
% Number of leaves : 8
% Syntax : Number of clauses : 530 ( 530 unt; 0 nHn; 264 RR)
% Number of literals : 530 ( 529 equ; 9 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 9 con; 0-2 aty)
% Number of variables : 405 ( 228 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t1,axiom,
sFlat0 = f(x0,x2),
introduced(definition) ).
cnf(t24,plain,
f(x0,x2) = sFlat0,
inference(orient,[status(thm)],[t1]) ).
cnf(t2,axiom,
sFlat1 = f(f(x0,x2),f(x0,x2)),
introduced(definition) ).
cnf(t13,plain,
f(f(x0,x2),f(x0,x2)) = sFlat1,
inference(orient,[status(thm)],[t2]) ).
cnf(t45074,plain,
f(sFlat0,f(x0,x2)) = sFlat1,
inference(step,[status(thm)],[t13,t24]) ).
cnf(t45075,plain,
f(sFlat0,sFlat0) = sFlat1,
inference(step,[status(thm)],[t45074,t24]) ).
cnf(t27,plain,
f(sFlat0,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t45075]) ).
cnf(t35,plain,
f(sFlat0,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t27]) ).
cnf(t3,axiom,
sFlat2 = f(x1,f(f(x0,x2),f(x0,x2))),
introduced(definition) ).
cnf(t45076,plain,
sFlat2 = f(x1,f(sFlat0,f(x0,x2))),
inference(step,[status(thm)],[t3,t24]) ).
cnf(t45077,plain,
sFlat2 = f(x1,f(sFlat0,sFlat0)),
inference(step,[status(thm)],[t45076,t24]) ).
cnf(t28,plain,
f(x1,f(sFlat0,sFlat0)) = sFlat2,
inference(orient,[status(thm)],[t45077]) ).
cnf(t45080,plain,
f(x1,sFlat1) = sFlat2,
inference(step,[status(thm)],[t28,t35]) ).
cnf(t39,plain,
f(x1,sFlat1) = sFlat2,
inference(rw,[status(thm)],[t45080]) ).
cnf(t44,plain,
f(x1,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t39]) ).
cnf(t4,axiom,
sFlat3 = f(x1,x2),
introduced(definition) ).
cnf(t31,plain,
f(x1,x2) = sFlat3,
inference(orient,[status(thm)],[t4]) ).
cnf(t5,axiom,
sFlat4 = f(f(x1,x2),f(x1,x2)),
introduced(definition) ).
cnf(t17,plain,
f(f(x1,x2),f(x1,x2)) = sFlat4,
inference(orient,[status(thm)],[t5]) ).
cnf(t45078,plain,
f(sFlat3,f(x1,x2)) = sFlat4,
inference(step,[status(thm)],[t17,t31]) ).
cnf(t45079,plain,
f(sFlat3,sFlat3) = sFlat4,
inference(step,[status(thm)],[t45078,t31]) ).
cnf(t34,plain,
f(sFlat3,sFlat3) = sFlat4,
inference(rw,[status(thm)],[t45079]) ).
cnf(t40,plain,
f(sFlat3,sFlat3) = sFlat4,
inference(orient,[status(thm)],[t34]) ).
cnf(t6,axiom,
sFlat5 = f(x0,f(f(x1,x2),f(x1,x2))),
introduced(definition) ).
cnf(t45073,plain,
sFlat5 = f(x0,sFlat4),
inference(step,[status(thm)],[t6,t17]) ).
cnf(t21,plain,
f(x0,sFlat4) = sFlat5,
inference(orient,[status(thm)],[t45073]) ).
cnf(t0,axiom,
f(f(f(f(X1,X2),f(X2,X3)),X4),f(X2,f(f(X2,f(f(X1,X1),X1)),X3))) = X2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(t7,plain,
f(f(f(f(X1,X2),f(X2,X3)),X4),f(X2,f(f(X2,f(f(X1,X1),X1)),X3))) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t8,plain,
f(X1,X2) = f(X1,f(f(X1,X2),f(f(f(X1,X2),f(f(f(X3,X1),f(X3,X1)),f(X3,X1))),X4))),
inference(cp,[status(thm)],[t7,t7]) ).
cnf(t459,plain,
f(X1,f(f(X1,X2),f(f(f(X1,X2),f(f(f(X3,X1),f(X3,X1)),f(X3,X1))),X4))) = f(X1,X2),
inference(orient,[status(thm)],[t8]) ).
cnf(t519,plain,
f(f(X1,X2),f(X2,X3)) = f(f(X1,X2),f(f(f(X1,X2),f(X2,X3)),X2)),
inference(cp,[status(thm)],[t459,t7]) ).
cnf(t1132,plain,
f(f(X1,X2),f(f(f(X1,X2),f(X2,X3)),X2)) = f(f(X1,X2),f(X2,X3)),
inference(orient,[status(thm)],[t519]) ).
cnf(t1216,plain,
f(f(f(f(X1,X2),f(X2,X3)),X2),f(X2,f(f(X2,f(f(X1,X1),X1)),X3))) = f(f(f(f(X1,X2),f(X2,X3)),X2),f(X2,X2)),
inference(cp,[status(thm)],[t1132,t7]) ).
cnf(t45147,plain,
X2 = f(f(f(f(X1,X2),f(X2,X3)),X2),f(X2,X2)),
inference(step,[status(thm)],[t1216,t7]) ).
cnf(t3364,plain,
f(f(f(f(X1,X2),f(X2,X3)),X2),f(X2,X2)) = X2,
inference(orient,[status(thm)],[t45147]) ).
cnf(t43,plain,
X1 = f(f(f(f(sFlat3,X1),f(X1,X2)),X3),f(X1,f(f(X1,f(sFlat4,sFlat3)),X2))),
inference(cp,[status(thm)],[t7,t40]) ).
cnf(t329,plain,
f(f(f(f(sFlat3,X1),f(X1,X2)),X3),f(X1,f(f(X1,f(sFlat4,sFlat3)),X2))) = X1,
inference(orient,[status(thm)],[t43]) ).
cnf(t3368,plain,
X1 = f(f(X1,X1),f(X1,X1)),
inference(cp,[status(thm)],[t3364,t329]) ).
cnf(t3633,plain,
f(f(X1,X1),f(X1,X1)) = X1,
inference(orient,[status(thm)],[t3368]) ).
cnf(t3649,plain,
X1 = f(f(X1,X2),f(X1,f(f(X1,f(f(X1,X1),X1)),X1))),
inference(cp,[status(thm)],[t7,t3633]) ).
cnf(t11262,plain,
f(f(X1,X2),f(X1,f(f(X1,f(f(X1,X1),X1)),X1))) = X1,
inference(orient,[status(thm)],[t3649]) ).
cnf(t11439,plain,
f(X1,X2) = f(X1,f(f(X1,X2),f(X1,X2))),
inference(cp,[status(thm)],[t459,t11262]) ).
cnf(t11799,plain,
f(X1,f(f(X1,X2),f(X1,X2))) = f(X1,X2),
inference(orient,[status(thm)],[t11439]) ).
cnf(t11811,plain,
f(f(X1,X2),f(X1,f(f(X1,f(f(X1,X1),X1)),X1))) = f(f(X1,X2),f(X1,f(f(X1,X2),f(X1,f(f(X1,f(f(X1,X1),X1)),X1))))),
inference(cp,[status(thm)],[t11799,t11262]) ).
cnf(t45306,plain,
X1 = f(f(X1,X2),f(X1,f(f(X1,X2),f(X1,f(f(X1,f(f(X1,X1),X1)),X1))))),
inference(step,[status(thm)],[t11811,t11262]) ).
cnf(t45307,plain,
X1 = f(f(X1,X2),f(X1,X1)),
inference(step,[status(thm)],[t45306,t11262]) ).
cnf(t12079,plain,
f(f(X1,X2),f(X1,X1)) = X1,
inference(orient,[status(thm)],[t45307]) ).
cnf(t12177,plain,
f(X1,X1) = f(f(f(X1,X1),X2),X1),
inference(cp,[status(thm)],[t12079,t12079]) ).
cnf(t13052,plain,
f(f(f(X1,X1),X2),X1) = f(X1,X1),
inference(orient,[status(thm)],[t12177]) ).
cnf(t22,plain,
sFlat4 = f(f(f(sFlat5,f(sFlat4,X1)),X2),f(sFlat4,f(f(sFlat4,f(f(x0,x0),x0)),X1))),
inference(cp,[status(thm)],[t7,t21]) ).
cnf(t93,plain,
f(f(f(sFlat5,f(sFlat4,X1)),X2),f(sFlat4,f(f(sFlat4,f(f(x0,x0),x0)),X1))) = sFlat4,
inference(orient,[status(thm)],[t22]) ).
cnf(t11826,plain,
f(f(f(sFlat5,f(sFlat4,X1)),X2),f(sFlat4,f(f(sFlat4,f(f(x0,x0),x0)),X1))) = f(f(f(sFlat5,f(sFlat4,X1)),X2),f(sFlat4,f(f(f(sFlat5,f(sFlat4,X1)),X2),f(sFlat4,f(f(sFlat4,f(f(x0,x0),x0)),X1))))),
inference(cp,[status(thm)],[t11799,t93]) ).
cnf(t45425,plain,
sFlat4 = f(f(f(sFlat5,f(sFlat4,X1)),X2),f(sFlat4,f(f(f(sFlat5,f(sFlat4,X1)),X2),f(sFlat4,f(f(sFlat4,f(f(x0,x0),x0)),X1))))),
inference(step,[status(thm)],[t11826,t93]) ).
cnf(t45426,plain,
sFlat4 = f(f(f(sFlat5,f(sFlat4,X1)),X2),f(sFlat4,sFlat4)),
inference(step,[status(thm)],[t45425,t93]) ).
cnf(t42,plain,
sFlat3 = f(f(f(f(X1,sFlat3),sFlat4),X2),f(sFlat3,f(f(sFlat3,f(f(X1,X1),X1)),sFlat3))),
inference(cp,[status(thm)],[t7,t40]) ).
cnf(t318,plain,
f(f(f(f(X1,sFlat3),sFlat4),X2),f(sFlat3,f(f(sFlat3,f(f(X1,X1),X1)),sFlat3))) = sFlat3,
inference(orient,[status(thm)],[t42]) ).
cnf(t1197,plain,
f(f(f(f(X1,sFlat3),sFlat4),sFlat3),f(sFlat3,f(f(sFlat3,f(f(X1,X1),X1)),sFlat3))) = f(f(f(f(X1,sFlat3),sFlat4),sFlat3),f(sFlat3,sFlat3)),
inference(cp,[status(thm)],[t1132,t318]) ).
cnf(t45089,plain,
sFlat3 = f(f(f(f(X1,sFlat3),sFlat4),sFlat3),f(sFlat3,sFlat3)),
inference(step,[status(thm)],[t1197,t318]) ).
cnf(t45090,plain,
sFlat3 = f(f(f(f(X1,sFlat3),sFlat4),sFlat3),sFlat4),
inference(step,[status(thm)],[t45089,t40]) ).
cnf(t1362,plain,
f(f(f(f(X1,sFlat3),sFlat4),sFlat3),sFlat4) = sFlat3,
inference(orient,[status(thm)],[t45090]) ).
cnf(t41,plain,
sFlat3 = f(f(f(sFlat4,f(sFlat3,X1)),X2),f(sFlat3,f(f(sFlat3,f(f(sFlat3,sFlat3),sFlat3)),X1))),
inference(cp,[status(thm)],[t7,t40]) ).
cnf(t45082,plain,
sFlat3 = f(f(f(sFlat4,f(sFlat3,X1)),X2),f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),X1))),
inference(step,[status(thm)],[t41,t40]) ).
cnf(t64,plain,
f(f(f(sFlat4,f(sFlat3,X1)),X2),f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),X1))) = sFlat3,
inference(orient,[status(thm)],[t45082]) ).
cnf(t65,plain,
sFlat3 = f(f(f(sFlat4,sFlat4),X1),f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),sFlat3))),
inference(cp,[status(thm)],[t64,t40]) ).
cnf(t71,plain,
f(f(f(sFlat4,sFlat4),X1),f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),sFlat3))) = sFlat3,
inference(orient,[status(thm)],[t65]) ).
cnf(t1215,plain,
f(f(f(sFlat4,sFlat4),sFlat3),f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),sFlat3))) = f(f(f(sFlat4,sFlat4),sFlat3),f(sFlat3,sFlat3)),
inference(cp,[status(thm)],[t1132,t71]) ).
cnf(t45085,plain,
sFlat3 = f(f(f(sFlat4,sFlat4),sFlat3),f(sFlat3,sFlat3)),
inference(step,[status(thm)],[t1215,t71]) ).
cnf(t45086,plain,
sFlat3 = f(f(f(sFlat4,sFlat4),sFlat3),sFlat4),
inference(step,[status(thm)],[t45085,t40]) ).
cnf(t1334,plain,
f(f(f(sFlat4,sFlat4),sFlat3),sFlat4) = sFlat3,
inference(orient,[status(thm)],[t45086]) ).
cnf(t1363,plain,
sFlat3 = f(f(sFlat3,sFlat3),sFlat4),
inference(cp,[status(thm)],[t1362,t1334]) ).
cnf(t45091,plain,
sFlat3 = f(sFlat4,sFlat4),
inference(step,[status(thm)],[t1363,t40]) ).
cnf(t1378,plain,
f(sFlat4,sFlat4) = sFlat3,
inference(orient,[status(thm)],[t45091]) ).
cnf(t45427,plain,
sFlat4 = f(f(f(sFlat5,f(sFlat4,X1)),X2),sFlat3),
inference(step,[status(thm)],[t45426,t1378]) ).
cnf(t14576,plain,
f(f(f(sFlat5,f(sFlat4,X1)),X2),sFlat3) = sFlat4,
inference(orient,[status(thm)],[t45427]) ).
cnf(t25,plain,
x2 = f(f(f(sFlat0,f(x2,X1)),X2),f(x2,f(f(x2,f(f(x0,x0),x0)),X1))),
inference(cp,[status(thm)],[t7,t24]) ).
cnf(t140,plain,
f(f(f(sFlat0,f(x2,X1)),X2),f(x2,f(f(x2,f(f(x0,x0),x0)),X1))) = x2,
inference(orient,[status(thm)],[t25]) ).
cnf(t32,plain,
x2 = f(f(f(sFlat3,f(x2,X1)),X2),f(x2,f(f(x2,f(f(x1,x1),x1)),X1))),
inference(cp,[status(thm)],[t7,t31]) ).
cnf(t177,plain,
f(f(f(sFlat3,f(x2,X1)),X2),f(x2,f(f(x2,f(f(x1,x1),x1)),X1))) = x2,
inference(orient,[status(thm)],[t32]) ).
cnf(t1207,plain,
f(f(f(sFlat3,f(x2,X1)),x2),f(x2,f(f(x2,f(f(x1,x1),x1)),X1))) = f(f(f(sFlat3,f(x2,X1)),x2),f(x2,x2)),
inference(cp,[status(thm)],[t1132,t177]) ).
cnf(t45126,plain,
x2 = f(f(f(sFlat3,f(x2,X1)),x2),f(x2,x2)),
inference(step,[status(thm)],[t1207,t177]) ).
cnf(t2624,plain,
f(f(f(sFlat3,f(x2,X1)),x2),f(x2,x2)) = x2,
inference(orient,[status(thm)],[t45126]) ).
cnf(t45094,plain,
f(f(sFlat3,X1),f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),sFlat3))) = sFlat3,
inference(step,[status(thm)],[t71,t1378]) ).
cnf(t1404,plain,
f(f(sFlat3,X1),f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),sFlat3))) = sFlat3,
inference(rw,[status(thm)],[t45094]) ).
cnf(t3930,plain,
f(f(sFlat3,X1),f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),sFlat3))) = sFlat3,
inference(orient,[status(thm)],[t1404]) ).
cnf(t3931,plain,
f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),sFlat3)) = f(sFlat3,f(f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),sFlat3)),f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),sFlat3)))),
inference(cp,[status(thm)],[t3633,t3930]) ).
cnf(t45156,plain,
f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),sFlat3)) = f(sFlat3,sFlat3),
inference(step,[status(thm)],[t3931,t3930]) ).
cnf(t45157,plain,
f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),sFlat3)) = sFlat4,
inference(step,[status(thm)],[t45156,t40]) ).
cnf(t3979,plain,
f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),sFlat3)) = sFlat4,
inference(orient,[status(thm)],[t45157]) ).
cnf(t3985,plain,
sFlat3 = f(f(f(f(sFlat3,sFlat3),f(sFlat3,sFlat3)),X1),sFlat4),
inference(cp,[status(thm)],[t329,t3979]) ).
cnf(t45159,plain,
sFlat3 = f(f(sFlat3,X1),sFlat4),
inference(step,[status(thm)],[t3985,t3633]) ).
cnf(t4946,plain,
f(f(sFlat3,X1),sFlat4) = sFlat3,
inference(orient,[status(thm)],[t45159]) ).
cnf(t4959,plain,
x2 = f(sFlat3,f(x2,f(f(x2,f(f(x1,x1),x1)),X1))),
inference(cp,[status(thm)],[t177,t4946]) ).
cnf(t5813,plain,
f(sFlat3,f(x2,f(f(x2,f(f(x1,x1),x1)),X1))) = x2,
inference(orient,[status(thm)],[t4959]) ).
cnf(t5819,plain,
sFlat3 = f(x2,sFlat4),
inference(cp,[status(thm)],[t4946,t5813]) ).
cnf(t5853,plain,
f(x2,sFlat4) = sFlat3,
inference(orient,[status(thm)],[t5819]) ).
cnf(t5857,plain,
x2 = f(f(f(sFlat3,sFlat3),x2),f(x2,x2)),
inference(cp,[status(thm)],[t2624,t5853]) ).
cnf(t45198,plain,
x2 = f(f(sFlat4,x2),f(x2,x2)),
inference(step,[status(thm)],[t5857,t40]) ).
cnf(t6028,plain,
f(f(sFlat4,x2),f(x2,x2)) = x2,
inference(orient,[status(thm)],[t45198]) ).
cnf(t6036,plain,
x2 = f(f(x2,X1),f(x2,f(f(x2,f(f(sFlat4,sFlat4),sFlat4)),x2))),
inference(cp,[status(thm)],[t7,t6028]) ).
cnf(t45217,plain,
x2 = f(f(x2,X1),f(x2,f(f(x2,f(sFlat3,sFlat4)),x2))),
inference(step,[status(thm)],[t6036,t1378]) ).
cnf(t6954,plain,
f(f(x2,X1),f(x2,f(f(x2,f(sFlat3,sFlat4)),x2))) = x2,
inference(orient,[status(thm)],[t45217]) ).
cnf(t6958,plain,
f(x2,f(f(x2,f(sFlat3,sFlat4)),x2)) = f(x2,f(f(x2,f(f(x2,f(sFlat3,sFlat4)),x2)),f(x2,f(f(x2,f(sFlat3,sFlat4)),x2)))),
inference(cp,[status(thm)],[t3633,t6954]) ).
cnf(t45218,plain,
f(x2,f(f(x2,f(sFlat3,sFlat4)),x2)) = f(x2,x2),
inference(step,[status(thm)],[t6958,t6954]) ).
cnf(t7019,plain,
f(x2,f(f(x2,f(sFlat3,sFlat4)),x2)) = f(x2,x2),
inference(orient,[status(thm)],[t45218]) ).
cnf(t45219,plain,
f(f(x2,X1),f(x2,x2)) = x2,
inference(step,[status(thm)],[t6954,t7019]) ).
cnf(t7044,plain,
f(f(x2,X1),f(x2,x2)) = x2,
inference(rw,[status(thm)],[t45219]) ).
cnf(t7045,plain,
f(f(x2,X1),f(x2,x2)) = x2,
inference(orient,[status(thm)],[t7044]) ).
cnf(t7066,plain,
x2 = f(f(f(sFlat0,f(x2,f(x2,x2))),X1),f(x2,x2)),
inference(cp,[status(thm)],[t140,t7045]) ).
cnf(t7270,plain,
f(f(f(sFlat0,f(x2,f(x2,x2))),X1),f(x2,x2)) = x2,
inference(orient,[status(thm)],[t7066]) ).
cnf(t38,plain,
X1 = f(f(f(f(sFlat0,X1),f(X1,X2)),X3),f(X1,f(f(X1,f(sFlat1,sFlat0)),X2))),
inference(cp,[status(thm)],[t7,t35]) ).
cnf(t234,plain,
f(f(f(f(sFlat0,X1),f(X1,X2)),X3),f(X1,f(f(X1,f(sFlat1,sFlat0)),X2))) = X1,
inference(orient,[status(thm)],[t38]) ).
cnf(t45,plain,
sFlat1 = f(f(f(sFlat2,f(sFlat1,X1)),X2),f(sFlat1,f(f(sFlat1,f(f(x1,x1),x1)),X1))),
inference(cp,[status(thm)],[t7,t44]) ).
cnf(t417,plain,
f(f(f(sFlat2,f(sFlat1,X1)),X2),f(sFlat1,f(f(sFlat1,f(f(x1,x1),x1)),X1))) = sFlat1,
inference(orient,[status(thm)],[t45]) ).
cnf(t502,plain,
f(sFlat2,f(sFlat1,X1)) = f(sFlat2,f(f(sFlat2,f(sFlat1,X1)),sFlat1)),
inference(cp,[status(thm)],[t459,t417]) ).
cnf(t774,plain,
f(sFlat2,f(f(sFlat2,f(sFlat1,X1)),sFlat1)) = f(sFlat2,f(sFlat1,X1)),
inference(orient,[status(thm)],[t502]) ).
cnf(t777,plain,
sFlat2 = f(f(f(f(sFlat0,sFlat2),f(sFlat2,sFlat1)),X1),f(sFlat2,f(sFlat1,sFlat0))),
inference(cp,[status(thm)],[t234,t774]) ).
cnf(t986,plain,
f(f(f(f(sFlat0,sFlat2),f(sFlat2,sFlat1)),X1),f(sFlat2,f(sFlat1,sFlat0))) = sFlat2,
inference(orient,[status(thm)],[t777]) ).
cnf(t3367,plain,
sFlat2 = f(f(sFlat2,sFlat2),f(sFlat2,sFlat2)),
inference(cp,[status(thm)],[t3364,t986]) ).
cnf(t3597,plain,
f(f(sFlat2,sFlat2),f(sFlat2,sFlat2)) = sFlat2,
inference(orient,[status(thm)],[t3367]) ).
cnf(t3606,plain,
sFlat2 = f(f(sFlat2,X1),f(sFlat2,f(f(sFlat2,f(f(sFlat2,sFlat2),sFlat2)),sFlat2))),
inference(cp,[status(thm)],[t7,t3597]) ).
cnf(t9524,plain,
f(f(sFlat2,X1),f(sFlat2,f(f(sFlat2,f(f(sFlat2,sFlat2),sFlat2)),sFlat2))) = sFlat2,
inference(orient,[status(thm)],[t3606]) ).
cnf(t9525,plain,
f(sFlat2,f(f(sFlat2,f(f(sFlat2,sFlat2),sFlat2)),sFlat2)) = f(sFlat2,f(f(sFlat2,f(f(sFlat2,f(f(sFlat2,sFlat2),sFlat2)),sFlat2)),f(sFlat2,f(f(sFlat2,f(f(sFlat2,sFlat2),sFlat2)),sFlat2)))),
inference(cp,[status(thm)],[t3633,t9524]) ).
cnf(t45262,plain,
f(sFlat2,f(f(sFlat2,f(f(sFlat2,sFlat2),sFlat2)),sFlat2)) = f(sFlat2,sFlat2),
inference(step,[status(thm)],[t9525,t9524]) ).
cnf(t9590,plain,
f(sFlat2,f(f(sFlat2,f(f(sFlat2,sFlat2),sFlat2)),sFlat2)) = f(sFlat2,sFlat2),
inference(orient,[status(thm)],[t45262]) ).
cnf(t9598,plain,
sFlat2 = f(f(f(f(sFlat2,sFlat2),f(sFlat2,sFlat2)),X1),f(sFlat2,sFlat2)),
inference(cp,[status(thm)],[t7,t9590]) ).
cnf(t45264,plain,
sFlat2 = f(f(sFlat2,X1),f(sFlat2,sFlat2)),
inference(step,[status(thm)],[t9598,t3597]) ).
cnf(t9619,plain,
f(f(sFlat2,X1),f(sFlat2,sFlat2)) = sFlat2,
inference(orient,[status(thm)],[t45264]) ).
cnf(t9634,plain,
sFlat1 = f(sFlat2,f(sFlat1,f(f(sFlat1,f(f(x1,x1),x1)),X1))),
inference(cp,[status(thm)],[t417,t9619]) ).
cnf(t9704,plain,
f(sFlat2,f(sFlat1,f(f(sFlat1,f(f(x1,x1),x1)),X1))) = sFlat1,
inference(orient,[status(thm)],[t9634]) ).
cnf(t9714,plain,
f(sFlat2,f(sFlat1,f(f(sFlat1,f(f(x1,x1),x1)),X1))) = f(sFlat2,f(sFlat1,sFlat1)),
inference(cp,[status(thm)],[t774,t9704]) ).
cnf(t45268,plain,
sFlat1 = f(sFlat2,f(sFlat1,sFlat1)),
inference(step,[status(thm)],[t9714,t9704]) ).
cnf(t37,plain,
sFlat0 = f(f(f(f(X1,sFlat0),sFlat1),X2),f(sFlat0,f(f(sFlat0,f(f(X1,X1),X1)),sFlat0))),
inference(cp,[status(thm)],[t7,t35]) ).
cnf(t218,plain,
f(f(f(f(X1,sFlat0),sFlat1),X2),f(sFlat0,f(f(sFlat0,f(f(X1,X1),X1)),sFlat0))) = sFlat0,
inference(orient,[status(thm)],[t37]) ).
cnf(t1201,plain,
f(f(f(f(X1,sFlat0),sFlat1),sFlat0),f(sFlat0,f(f(sFlat0,f(f(X1,X1),X1)),sFlat0))) = f(f(f(f(X1,sFlat0),sFlat1),sFlat0),f(sFlat0,sFlat0)),
inference(cp,[status(thm)],[t1132,t218]) ).
cnf(t45100,plain,
sFlat0 = f(f(f(f(X1,sFlat0),sFlat1),sFlat0),f(sFlat0,sFlat0)),
inference(step,[status(thm)],[t1201,t218]) ).
cnf(t45101,plain,
sFlat0 = f(f(f(f(X1,sFlat0),sFlat1),sFlat0),sFlat1),
inference(step,[status(thm)],[t45100,t35]) ).
cnf(t1445,plain,
f(f(f(f(X1,sFlat0),sFlat1),sFlat0),sFlat1) = sFlat0,
inference(orient,[status(thm)],[t45101]) ).
cnf(t36,plain,
sFlat0 = f(f(f(sFlat1,f(sFlat0,X1)),X2),f(sFlat0,f(f(sFlat0,f(f(sFlat0,sFlat0),sFlat0)),X1))),
inference(cp,[status(thm)],[t7,t35]) ).
cnf(t45081,plain,
sFlat0 = f(f(f(sFlat1,f(sFlat0,X1)),X2),f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),X1))),
inference(step,[status(thm)],[t36,t35]) ).
cnf(t47,plain,
f(f(f(sFlat1,f(sFlat0,X1)),X2),f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),X1))) = sFlat0,
inference(orient,[status(thm)],[t45081]) ).
cnf(t48,plain,
sFlat0 = f(f(f(sFlat1,sFlat1),X1),f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),sFlat0))),
inference(cp,[status(thm)],[t47,t35]) ).
cnf(t54,plain,
f(f(f(sFlat1,sFlat1),X1),f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),sFlat0))) = sFlat0,
inference(orient,[status(thm)],[t48]) ).
cnf(t1220,plain,
f(f(f(sFlat1,sFlat1),sFlat0),f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),sFlat0))) = f(f(f(sFlat1,sFlat1),sFlat0),f(sFlat0,sFlat0)),
inference(cp,[status(thm)],[t1132,t54]) ).
cnf(t45087,plain,
sFlat0 = f(f(f(sFlat1,sFlat1),sFlat0),f(sFlat0,sFlat0)),
inference(step,[status(thm)],[t1220,t54]) ).
cnf(t45088,plain,
sFlat0 = f(f(f(sFlat1,sFlat1),sFlat0),sFlat1),
inference(step,[status(thm)],[t45087,t35]) ).
cnf(t1348,plain,
f(f(f(sFlat1,sFlat1),sFlat0),sFlat1) = sFlat0,
inference(orient,[status(thm)],[t45088]) ).
cnf(t1446,plain,
sFlat0 = f(f(sFlat0,sFlat0),sFlat1),
inference(cp,[status(thm)],[t1445,t1348]) ).
cnf(t45102,plain,
sFlat0 = f(sFlat1,sFlat1),
inference(step,[status(thm)],[t1446,t35]) ).
cnf(t1461,plain,
f(sFlat1,sFlat1) = sFlat0,
inference(orient,[status(thm)],[t45102]) ).
cnf(t45269,plain,
sFlat1 = f(sFlat2,sFlat0),
inference(step,[status(thm)],[t45268,t1461]) ).
cnf(t9737,plain,
f(sFlat2,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t45269]) ).
cnf(t9742,plain,
sFlat2 = f(f(f(f(sFlat0,sFlat2),sFlat1),X1),f(sFlat2,f(f(sFlat2,f(sFlat1,sFlat0)),sFlat0))),
inference(cp,[status(thm)],[t234,t9737]) ).
cnf(t45105,plain,
f(f(sFlat0,X1),f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),sFlat0))) = sFlat0,
inference(step,[status(thm)],[t54,t1461]) ).
cnf(t1487,plain,
f(f(sFlat0,X1),f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),sFlat0))) = sFlat0,
inference(rw,[status(thm)],[t45105]) ).
cnf(t5347,plain,
f(f(sFlat0,X1),f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),sFlat0))) = sFlat0,
inference(orient,[status(thm)],[t1487]) ).
cnf(t5348,plain,
f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),sFlat0)) = f(sFlat0,f(f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),sFlat0)),f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),sFlat0)))),
inference(cp,[status(thm)],[t3633,t5347]) ).
cnf(t45176,plain,
f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),sFlat0)) = f(sFlat0,sFlat0),
inference(step,[status(thm)],[t5348,t5347]) ).
cnf(t45177,plain,
f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),sFlat0)) = sFlat1,
inference(step,[status(thm)],[t45176,t35]) ).
cnf(t5409,plain,
f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),sFlat0)) = sFlat1,
inference(orient,[status(thm)],[t45177]) ).
cnf(t5414,plain,
sFlat0 = f(f(f(sFlat1,f(sFlat0,sFlat0)),X1),sFlat1),
inference(cp,[status(thm)],[t47,t5409]) ).
cnf(t45179,plain,
sFlat0 = f(f(f(sFlat1,sFlat1),X1),sFlat1),
inference(step,[status(thm)],[t5414,t35]) ).
cnf(t45180,plain,
sFlat0 = f(f(sFlat0,X1),sFlat1),
inference(step,[status(thm)],[t45179,t1461]) ).
cnf(t5439,plain,
f(f(sFlat0,X1),sFlat1) = sFlat0,
inference(orient,[status(thm)],[t45180]) ).
cnf(t45276,plain,
sFlat2 = f(f(sFlat0,X1),f(sFlat2,f(f(sFlat2,f(sFlat1,sFlat0)),sFlat0))),
inference(step,[status(thm)],[t9742,t5439]) ).
cnf(t10157,plain,
f(f(sFlat0,X1),f(sFlat2,f(f(sFlat2,f(sFlat1,sFlat0)),sFlat0))) = sFlat2,
inference(orient,[status(thm)],[t45276]) ).
cnf(t10172,plain,
x2 = f(sFlat2,f(x2,x2)),
inference(cp,[status(thm)],[t7270,t10157]) ).
cnf(t10210,plain,
f(sFlat2,f(x2,x2)) = x2,
inference(orient,[status(thm)],[t10172]) ).
cnf(t10215,plain,
sFlat2 = f(f(f(f(X1,sFlat2),x2),sFlat2),f(sFlat2,sFlat2)),
inference(cp,[status(thm)],[t3364,t10210]) ).
cnf(t10714,plain,
f(f(f(f(X1,sFlat2),x2),sFlat2),f(sFlat2,sFlat2)) = sFlat2,
inference(orient,[status(thm)],[t10215]) ).
cnf(t13137,plain,
f(f(f(f(X1,X1),X2),X1),f(X1,X3)) = f(f(X1,X1),f(f(f(f(f(X1,X1),X2),X1),f(X1,X3)),X1)),
inference(cp,[status(thm)],[t1132,t13052]) ).
cnf(t45391,plain,
f(f(X1,X1),f(X1,X3)) = f(f(X1,X1),f(f(f(f(f(X1,X1),X2),X1),f(X1,X3)),X1)),
inference(step,[status(thm)],[t13137,t13052]) ).
cnf(t45392,plain,
f(f(X1,X1),f(X1,X3)) = f(f(X1,X1),f(f(f(X1,X1),f(X1,X3)),X1)),
inference(step,[status(thm)],[t45391,t13052]) ).
cnf(t45393,plain,
f(f(X1,X1),f(X1,X3)) = f(f(X1,X1),f(X1,X1)),
inference(step,[status(thm)],[t45392,t13052]) ).
cnf(t45394,plain,
f(f(X1,X1),f(X1,X3)) = X1,
inference(step,[status(thm)],[t45393,t12079]) ).
cnf(t13680,plain,
f(f(X1,X1),f(X1,X2)) = X1,
inference(orient,[status(thm)],[t45394]) ).
cnf(t13729,plain,
f(X1,X2) = f(f(f(X1,X2),f(X1,X2)),X1),
inference(cp,[status(thm)],[t13680,t12079]) ).
cnf(t17278,plain,
f(f(f(X1,X2),f(X1,X2)),X1) = f(X1,X2),
inference(orient,[status(thm)],[t13729]) ).
cnf(t46,plain,
x1 = f(f(f(f(X1,x1),sFlat2),X2),f(x1,f(f(x1,f(f(X1,X1),X1)),sFlat1))),
inference(cp,[status(thm)],[t7,t44]) ).
cnf(t6681,plain,
f(f(f(f(X1,x1),sFlat2),X2),f(x1,f(f(x1,f(f(X1,X1),X1)),sFlat1))) = x1,
inference(orient,[status(thm)],[t46]) ).
cnf(t11809,plain,
f(f(f(f(X1,x1),sFlat2),X2),f(x1,f(f(x1,f(f(X1,X1),X1)),sFlat1))) = f(f(f(f(X1,x1),sFlat2),X2),f(x1,f(f(f(f(X1,x1),sFlat2),X2),f(x1,f(f(x1,f(f(X1,X1),X1)),sFlat1))))),
inference(cp,[status(thm)],[t11799,t6681]) ).
cnf(t45648,plain,
x1 = f(f(f(f(X1,x1),sFlat2),X2),f(x1,f(f(f(f(X1,x1),sFlat2),X2),f(x1,f(f(x1,f(f(X1,X1),X1)),sFlat1))))),
inference(step,[status(thm)],[t11809,t6681]) ).
cnf(t45649,plain,
x1 = f(f(f(f(X1,x1),sFlat2),X2),f(x1,x1)),
inference(step,[status(thm)],[t45648,t6681]) ).
cnf(t21734,plain,
f(f(f(f(X1,x1),sFlat2),X2),f(x1,x1)) = x1,
inference(orient,[status(thm)],[t45649]) ).
cnf(t12176,plain,
sFlat4 = f(f(sFlat4,X1),sFlat3),
inference(cp,[status(thm)],[t12079,t1378]) ).
cnf(t12465,plain,
f(f(sFlat4,X1),sFlat3) = sFlat4,
inference(orient,[status(thm)],[t12176]) ).
cnf(t12471,plain,
f(f(f(sFlat4,X1),sFlat3),f(sFlat3,X2)) = f(sFlat4,f(f(f(f(sFlat4,X1),sFlat3),f(sFlat3,X2)),sFlat3)),
inference(cp,[status(thm)],[t1132,t12465]) ).
cnf(t45329,plain,
f(sFlat4,f(sFlat3,X2)) = f(sFlat4,f(f(f(f(sFlat4,X1),sFlat3),f(sFlat3,X2)),sFlat3)),
inference(step,[status(thm)],[t12471,t12465]) ).
cnf(t45330,plain,
f(sFlat4,f(sFlat3,X2)) = f(sFlat4,f(f(sFlat4,f(sFlat3,X2)),sFlat3)),
inference(step,[status(thm)],[t45329,t12465]) ).
cnf(t45331,plain,
f(sFlat4,f(sFlat3,X2)) = f(sFlat4,sFlat4),
inference(step,[status(thm)],[t45330,t12465]) ).
cnf(t45332,plain,
f(sFlat4,f(sFlat3,X2)) = sFlat3,
inference(step,[status(thm)],[t45331,t1378]) ).
cnf(t12862,plain,
f(sFlat4,f(sFlat3,X1)) = sFlat3,
inference(orient,[status(thm)],[t45332]) ).
cnf(t4958,plain,
sFlat3 = f(f(f(f(X1,sFlat3),f(sFlat3,sFlat4)),X2),f(sFlat3,sFlat3)),
inference(cp,[status(thm)],[t7,t4946]) ).
cnf(t45173,plain,
sFlat3 = f(f(f(f(X1,sFlat3),f(sFlat3,sFlat4)),X2),sFlat4),
inference(step,[status(thm)],[t4958,t40]) ).
cnf(t5135,plain,
f(f(f(f(X1,sFlat3),f(sFlat3,sFlat4)),X2),sFlat4) = sFlat3,
inference(orient,[status(thm)],[t45173]) ).
cnf(t33,plain,
x1 = f(f(f(f(X1,x1),sFlat3),X2),f(x1,f(f(x1,f(f(X1,X1),X1)),x2))),
inference(cp,[status(thm)],[t7,t31]) ).
cnf(t198,plain,
f(f(f(f(X1,x1),sFlat3),X2),f(x1,f(f(x1,f(f(X1,X1),X1)),x2))) = x1,
inference(orient,[status(thm)],[t33]) ).
cnf(t200,plain,
x1 = f(f(f(f(sFlat0,x1),sFlat3),X1),f(x1,f(f(x1,f(sFlat1,sFlat0)),x2))),
inference(cp,[status(thm)],[t198,t35]) ).
cnf(t212,plain,
f(f(f(f(sFlat0,x1),sFlat3),X1),f(x1,f(f(x1,f(sFlat1,sFlat0)),x2))) = x1,
inference(orient,[status(thm)],[t200]) ).
cnf(t5137,plain,
sFlat3 = f(x1,sFlat4),
inference(cp,[status(thm)],[t5135,t212]) ).
cnf(t5180,plain,
f(x1,sFlat4) = sFlat3,
inference(orient,[status(thm)],[t5137]) ).
cnf(t12161,plain,
x1 = f(sFlat3,f(x1,x1)),
inference(cp,[status(thm)],[t12079,t5180]) ).
cnf(t12306,plain,
f(sFlat3,f(x1,x1)) = x1,
inference(orient,[status(thm)],[t12161]) ).
cnf(t12863,plain,
sFlat3 = f(sFlat4,x1),
inference(cp,[status(thm)],[t12862,t12306]) ).
cnf(t12900,plain,
f(sFlat4,x1) = sFlat3,
inference(orient,[status(thm)],[t12863]) ).
cnf(t21741,plain,
x1 = f(f(f(sFlat3,sFlat2),X1),f(x1,x1)),
inference(cp,[status(thm)],[t21734,t12900]) ).
cnf(t22346,plain,
f(f(f(sFlat3,sFlat2),X1),f(x1,x1)) = x1,
inference(orient,[status(thm)],[t21741]) ).
cnf(t22352,plain,
f(f(sFlat3,sFlat2),f(sFlat3,sFlat2)) = f(x1,f(sFlat3,sFlat2)),
inference(cp,[status(thm)],[t13052,t22346]) ).
cnf(t10216,plain,
f(f(X1,sFlat2),f(sFlat2,f(x2,x2))) = f(f(X1,sFlat2),f(f(f(X1,sFlat2),x2),sFlat2)),
inference(cp,[status(thm)],[t1132,t10210]) ).
cnf(t45285,plain,
f(f(X1,sFlat2),x2) = f(f(X1,sFlat2),f(f(f(X1,sFlat2),x2),sFlat2)),
inference(step,[status(thm)],[t10216,t10210]) ).
cnf(t10885,plain,
f(f(X1,sFlat2),f(f(f(X1,sFlat2),x2),sFlat2)) = f(f(X1,sFlat2),x2),
inference(orient,[status(thm)],[t45285]) ).
cnf(t1304,plain,
f(f(X1,x1),f(x1,sFlat1)) = f(f(X1,x1),f(f(f(X1,x1),sFlat2),x1)),
inference(cp,[status(thm)],[t1132,t44]) ).
cnf(t45136,plain,
f(f(X1,x1),sFlat2) = f(f(X1,x1),f(f(f(X1,x1),sFlat2),x1)),
inference(step,[status(thm)],[t1304,t44]) ).
cnf(t2887,plain,
f(f(X1,x1),f(f(f(X1,x1),sFlat2),x1)) = f(f(X1,x1),sFlat2),
inference(orient,[status(thm)],[t45136]) ).
cnf(t13133,plain,
f(f(f(f(x1,x1),X1),x1),sFlat2) = f(f(x1,x1),f(f(f(f(f(x1,x1),X1),x1),sFlat2),x1)),
inference(cp,[status(thm)],[t2887,t13052]) ).
cnf(t45367,plain,
f(f(x1,x1),sFlat2) = f(f(x1,x1),f(f(f(f(f(x1,x1),X1),x1),sFlat2),x1)),
inference(step,[status(thm)],[t13133,t13052]) ).
cnf(t45368,plain,
f(f(x1,x1),sFlat2) = f(f(x1,x1),f(f(f(x1,x1),sFlat2),x1)),
inference(step,[status(thm)],[t45367,t13052]) ).
cnf(t45369,plain,
f(f(x1,x1),sFlat2) = f(f(x1,x1),f(x1,x1)),
inference(step,[status(thm)],[t45368,t13052]) ).
cnf(t45370,plain,
f(f(x1,x1),sFlat2) = x1,
inference(step,[status(thm)],[t45369,t12079]) ).
cnf(t13433,plain,
f(f(x1,x1),sFlat2) = x1,
inference(orient,[status(thm)],[t45370]) ).
cnf(t13434,plain,
f(f(f(x1,x1),sFlat2),x2) = f(x1,f(f(f(f(x1,x1),sFlat2),x2),sFlat2)),
inference(cp,[status(thm)],[t10885,t13433]) ).
cnf(t45383,plain,
f(x1,x2) = f(x1,f(f(f(f(x1,x1),sFlat2),x2),sFlat2)),
inference(step,[status(thm)],[t13434,t13433]) ).
cnf(t45384,plain,
sFlat3 = f(x1,f(f(f(f(x1,x1),sFlat2),x2),sFlat2)),
inference(step,[status(thm)],[t45383,t31]) ).
cnf(t45385,plain,
sFlat3 = f(x1,f(f(x1,x2),sFlat2)),
inference(step,[status(thm)],[t45384,t13433]) ).
cnf(t45386,plain,
sFlat3 = f(x1,f(sFlat3,sFlat2)),
inference(step,[status(thm)],[t45385,t31]) ).
cnf(t13547,plain,
f(x1,f(sFlat3,sFlat2)) = sFlat3,
inference(orient,[status(thm)],[t45386]) ).
cnf(t45657,plain,
f(f(sFlat3,sFlat2),f(sFlat3,sFlat2)) = sFlat3,
inference(step,[status(thm)],[t22352,t13547]) ).
cnf(t22401,plain,
f(f(sFlat3,sFlat2),f(sFlat3,sFlat2)) = sFlat3,
inference(orient,[status(thm)],[t45657]) ).
cnf(t22404,plain,
f(sFlat3,sFlat2) = f(sFlat3,sFlat3),
inference(cp,[status(thm)],[t17278,t22401]) ).
cnf(t45659,plain,
f(sFlat3,sFlat2) = sFlat4,
inference(step,[status(thm)],[t22404,t40]) ).
cnf(t22457,plain,
f(sFlat3,sFlat2) = sFlat4,
inference(orient,[status(thm)],[t45659]) ).
cnf(t22458,plain,
sFlat2 = f(f(f(sFlat4,x2),sFlat2),f(sFlat2,sFlat2)),
inference(cp,[status(thm)],[t10714,t22457]) ).
cnf(t5827,plain,
f(f(X1,sFlat3),f(sFlat3,f(x2,f(f(x2,f(f(x1,x1),x1)),X2)))) = f(f(X1,sFlat3),f(f(f(X1,sFlat3),x2),sFlat3)),
inference(cp,[status(thm)],[t1132,t5813]) ).
cnf(t45204,plain,
f(f(X1,sFlat3),x2) = f(f(X1,sFlat3),f(f(f(X1,sFlat3),x2),sFlat3)),
inference(step,[status(thm)],[t5827,t5813]) ).
cnf(t6304,plain,
f(f(X1,sFlat3),f(f(f(X1,sFlat3),x2),sFlat3)) = f(f(X1,sFlat3),x2),
inference(orient,[status(thm)],[t45204]) ).
cnf(t12467,plain,
f(f(f(sFlat4,X1),sFlat3),x2) = f(sFlat4,f(f(f(f(sFlat4,X1),sFlat3),x2),sFlat3)),
inference(cp,[status(thm)],[t6304,t12465]) ).
cnf(t45320,plain,
f(sFlat4,x2) = f(sFlat4,f(f(f(f(sFlat4,X1),sFlat3),x2),sFlat3)),
inference(step,[status(thm)],[t12467,t12465]) ).
cnf(t45321,plain,
f(sFlat4,x2) = f(sFlat4,f(f(sFlat4,x2),sFlat3)),
inference(step,[status(thm)],[t45320,t12465]) ).
cnf(t45322,plain,
f(sFlat4,x2) = f(sFlat4,sFlat4),
inference(step,[status(thm)],[t45321,t12465]) ).
cnf(t45323,plain,
f(sFlat4,x2) = sFlat3,
inference(step,[status(thm)],[t45322,t1378]) ).
cnf(t12517,plain,
f(sFlat4,x2) = sFlat3,
inference(orient,[status(thm)],[t45323]) ).
cnf(t45670,plain,
sFlat2 = f(f(sFlat3,sFlat2),f(sFlat2,sFlat2)),
inference(step,[status(thm)],[t22458,t12517]) ).
cnf(t45671,plain,
sFlat2 = f(sFlat4,f(sFlat2,sFlat2)),
inference(step,[status(thm)],[t45670,t22457]) ).
cnf(t22517,plain,
f(sFlat4,f(sFlat2,sFlat2)) = sFlat2,
inference(orient,[status(thm)],[t45671]) ).
cnf(t22523,plain,
sFlat4 = f(f(f(sFlat5,sFlat2),X1),sFlat3),
inference(cp,[status(thm)],[t14576,t22517]) ).
cnf(t22744,plain,
f(f(f(sFlat5,sFlat2),X1),sFlat3) = sFlat4,
inference(orient,[status(thm)],[t22523]) ).
cnf(t22750,plain,
f(f(sFlat5,sFlat2),f(sFlat5,sFlat2)) = f(sFlat4,f(sFlat5,sFlat2)),
inference(cp,[status(thm)],[t13052,t22744]) ).
cnf(t12180,plain,
f(f(f(X1,X2),f(X1,X1)),f(f(X1,X1),X3)) = f(X1,f(f(f(f(X1,X2),f(X1,X1)),f(f(X1,X1),X3)),f(X1,X1))),
inference(cp,[status(thm)],[t1132,t12079]) ).
cnf(t45397,plain,
f(X1,f(f(X1,X1),X3)) = f(X1,f(f(f(f(X1,X2),f(X1,X1)),f(f(X1,X1),X3)),f(X1,X1))),
inference(step,[status(thm)],[t12180,t12079]) ).
cnf(t45398,plain,
f(X1,f(f(X1,X1),X3)) = f(X1,f(f(X1,f(f(X1,X1),X3)),f(X1,X1))),
inference(step,[status(thm)],[t45397,t12079]) ).
cnf(t45399,plain,
f(X1,f(f(X1,X1),X3)) = f(X1,X1),
inference(step,[status(thm)],[t45398,t12079]) ).
cnf(t14064,plain,
f(X1,f(f(X1,X1),X2)) = f(X1,X1),
inference(orient,[status(thm)],[t45399]) ).
cnf(t518,plain,
f(sFlat5,f(sFlat4,X1)) = f(sFlat5,f(f(sFlat5,f(sFlat4,X1)),sFlat4)),
inference(cp,[status(thm)],[t459,t93]) ).
cnf(t783,plain,
f(sFlat5,f(f(sFlat5,f(sFlat4,X1)),sFlat4)) = f(sFlat5,f(sFlat4,X1)),
inference(orient,[status(thm)],[t518]) ).
cnf(t785,plain,
sFlat5 = f(f(f(f(sFlat3,sFlat5),f(sFlat5,sFlat4)),X1),f(sFlat5,f(sFlat4,sFlat3))),
inference(cp,[status(thm)],[t329,t783]) ).
cnf(t1001,plain,
f(f(f(f(sFlat3,sFlat5),f(sFlat5,sFlat4)),X1),f(sFlat5,f(sFlat4,sFlat3))) = sFlat5,
inference(orient,[status(thm)],[t785]) ).
cnf(t3365,plain,
sFlat5 = f(f(sFlat5,sFlat5),f(sFlat5,sFlat5)),
inference(cp,[status(thm)],[t3364,t1001]) ).
cnf(t3561,plain,
f(f(sFlat5,sFlat5),f(sFlat5,sFlat5)) = sFlat5,
inference(orient,[status(thm)],[t3365]) ).
cnf(t3570,plain,
sFlat5 = f(f(sFlat5,X1),f(sFlat5,f(f(sFlat5,f(f(sFlat5,sFlat5),sFlat5)),sFlat5))),
inference(cp,[status(thm)],[t7,t3561]) ).
cnf(t7844,plain,
f(f(sFlat5,X1),f(sFlat5,f(f(sFlat5,f(f(sFlat5,sFlat5),sFlat5)),sFlat5))) = sFlat5,
inference(orient,[status(thm)],[t3570]) ).
cnf(t7845,plain,
f(sFlat5,f(f(sFlat5,f(f(sFlat5,sFlat5),sFlat5)),sFlat5)) = f(sFlat5,f(f(sFlat5,f(f(sFlat5,f(f(sFlat5,sFlat5),sFlat5)),sFlat5)),f(sFlat5,f(f(sFlat5,f(f(sFlat5,sFlat5),sFlat5)),sFlat5)))),
inference(cp,[status(thm)],[t3633,t7844]) ).
cnf(t45234,plain,
f(sFlat5,f(f(sFlat5,f(f(sFlat5,sFlat5),sFlat5)),sFlat5)) = f(sFlat5,sFlat5),
inference(step,[status(thm)],[t7845,t7844]) ).
cnf(t7910,plain,
f(sFlat5,f(f(sFlat5,f(f(sFlat5,sFlat5),sFlat5)),sFlat5)) = f(sFlat5,sFlat5),
inference(orient,[status(thm)],[t45234]) ).
cnf(t7918,plain,
sFlat5 = f(f(f(f(sFlat5,sFlat5),f(sFlat5,sFlat5)),X1),f(sFlat5,sFlat5)),
inference(cp,[status(thm)],[t7,t7910]) ).
cnf(t45236,plain,
sFlat5 = f(f(sFlat5,X1),f(sFlat5,sFlat5)),
inference(step,[status(thm)],[t7918,t3561]) ).
cnf(t7939,plain,
f(f(sFlat5,X1),f(sFlat5,sFlat5)) = sFlat5,
inference(orient,[status(thm)],[t45236]) ).
cnf(t7959,plain,
sFlat4 = f(sFlat5,f(sFlat4,f(f(sFlat4,f(f(x0,x0),x0)),X1))),
inference(cp,[status(thm)],[t93,t7939]) ).
cnf(t8024,plain,
f(sFlat5,f(sFlat4,f(f(sFlat4,f(f(x0,x0),x0)),X1))) = sFlat4,
inference(orient,[status(thm)],[t7959]) ).
cnf(t8034,plain,
f(sFlat5,f(sFlat4,f(f(sFlat4,f(f(x0,x0),x0)),X1))) = f(sFlat5,f(sFlat4,sFlat4)),
inference(cp,[status(thm)],[t783,t8024]) ).
cnf(t45240,plain,
sFlat4 = f(sFlat5,f(sFlat4,sFlat4)),
inference(step,[status(thm)],[t8034,t8024]) ).
cnf(t45241,plain,
sFlat4 = f(sFlat5,sFlat3),
inference(step,[status(thm)],[t45240,t1378]) ).
cnf(t8057,plain,
f(sFlat5,sFlat3) = sFlat4,
inference(orient,[status(thm)],[t45241]) ).
cnf(t8061,plain,
sFlat5 = f(f(f(f(sFlat3,sFlat5),sFlat4),X1),f(sFlat5,f(f(sFlat5,f(sFlat4,sFlat3)),sFlat3))),
inference(cp,[status(thm)],[t329,t8057]) ).
cnf(t45248,plain,
sFlat5 = f(f(sFlat3,X1),f(sFlat5,f(f(sFlat5,f(sFlat4,sFlat3)),sFlat3))),
inference(step,[status(thm)],[t8061,t4946]) ).
cnf(t8477,plain,
f(f(sFlat3,X1),f(sFlat5,f(f(sFlat5,f(sFlat4,sFlat3)),sFlat3))) = sFlat5,
inference(orient,[status(thm)],[t45248]) ).
cnf(t11806,plain,
f(f(sFlat3,X1),f(sFlat5,f(f(sFlat5,f(sFlat4,sFlat3)),sFlat3))) = f(f(sFlat3,X1),f(sFlat5,f(f(sFlat3,X1),f(sFlat5,f(f(sFlat5,f(sFlat4,sFlat3)),sFlat3))))),
inference(cp,[status(thm)],[t11799,t8477]) ).
cnf(t45304,plain,
sFlat5 = f(f(sFlat3,X1),f(sFlat5,f(f(sFlat3,X1),f(sFlat5,f(f(sFlat5,f(sFlat4,sFlat3)),sFlat3))))),
inference(step,[status(thm)],[t11806,t8477]) ).
cnf(t45305,plain,
sFlat5 = f(f(sFlat3,X1),f(sFlat5,sFlat5)),
inference(step,[status(thm)],[t45304,t8477]) ).
cnf(t12039,plain,
f(f(sFlat3,X1),f(sFlat5,sFlat5)) = sFlat5,
inference(orient,[status(thm)],[t45305]) ).
cnf(t12307,plain,
sFlat5 = f(x1,f(sFlat5,sFlat5)),
inference(cp,[status(thm)],[t12039,t12306]) ).
cnf(t12543,plain,
f(x1,f(sFlat5,sFlat5)) = sFlat5,
inference(orient,[status(thm)],[t12307]) ).
cnf(t12544,plain,
x1 = f(sFlat5,f(x1,x1)),
inference(cp,[status(thm)],[t12079,t12543]) ).
cnf(t12942,plain,
f(sFlat5,f(x1,x1)) = x1,
inference(orient,[status(thm)],[t12544]) ).
cnf(t13732,plain,
sFlat5 = f(f(sFlat5,sFlat5),x1),
inference(cp,[status(thm)],[t13680,t12942]) ).
cnf(t13830,plain,
f(f(sFlat5,sFlat5),x1) = sFlat5,
inference(orient,[status(thm)],[t13732]) ).
cnf(t21739,plain,
x1 = f(f(f(sFlat5,sFlat2),X1),f(x1,x1)),
inference(cp,[status(thm)],[t21734,t13830]) ).
cnf(t22101,plain,
f(f(f(sFlat5,sFlat2),X1),f(x1,x1)) = x1,
inference(orient,[status(thm)],[t21739]) ).
cnf(t22106,plain,
f(f(sFlat5,sFlat2),f(sFlat5,sFlat2)) = f(f(sFlat5,sFlat2),x1),
inference(cp,[status(thm)],[t14064,t22101]) ).
cnf(t22155,plain,
f(f(sFlat5,sFlat2),f(sFlat5,sFlat2)) = f(f(sFlat5,sFlat2),x1),
inference(orient,[status(thm)],[t22106]) ).
cnf(t22107,plain,
f(f(sFlat5,sFlat2),f(sFlat5,sFlat2)) = f(x1,f(sFlat5,sFlat2)),
inference(cp,[status(thm)],[t13052,t22101]) ).
cnf(t45652,plain,
f(f(sFlat5,sFlat2),x1) = f(x1,f(sFlat5,sFlat2)),
inference(step,[status(thm)],[t22107,t22155]) ).
cnf(t22241,plain,
f(f(sFlat5,sFlat2),x1) = f(x1,f(sFlat5,sFlat2)),
inference(orient,[status(thm)],[t45652]) ).
cnf(t45653,plain,
f(f(sFlat5,sFlat2),f(sFlat5,sFlat2)) = f(x1,f(sFlat5,sFlat2)),
inference(step,[status(thm)],[t22155,t22241]) ).
cnf(t22242,plain,
f(f(sFlat5,sFlat2),f(sFlat5,sFlat2)) = f(x1,f(sFlat5,sFlat2)),
inference(orient,[status(thm)],[t45653]) ).
cnf(t45673,plain,
f(x1,f(sFlat5,sFlat2)) = f(sFlat4,f(sFlat5,sFlat2)),
inference(step,[status(thm)],[t22750,t22242]) ).
cnf(t22834,plain,
f(x1,f(sFlat5,sFlat2)) = f(sFlat4,f(sFlat5,sFlat2)),
inference(orient,[status(thm)],[t45673]) ).
cnf(t12175,plain,
sFlat1 = f(f(sFlat1,X1),sFlat0),
inference(cp,[status(thm)],[t12079,t1461]) ).
cnf(t12399,plain,
f(f(sFlat1,X1),sFlat0) = sFlat1,
inference(orient,[status(thm)],[t12175]) ).
cnf(t12415,plain,
sFlat1 = f(f(f(f(X1,sFlat1),f(sFlat1,sFlat0)),X2),f(sFlat1,sFlat1)),
inference(cp,[status(thm)],[t7,t12399]) ).
cnf(t45950,plain,
sFlat1 = f(f(f(f(X1,sFlat1),f(sFlat1,sFlat0)),X2),sFlat0),
inference(step,[status(thm)],[t12415,t1461]) ).
cnf(t33381,plain,
f(f(f(f(X1,sFlat1),f(sFlat1,sFlat0)),X2),sFlat0) = sFlat1,
inference(orient,[status(thm)],[t45950]) ).
cnf(t11,plain,
f(f(f(X1,X2),f(X2,X3)),X4) = f(f(f(f(Y4,f(f(f(X1,X2),f(X2,X3)),X4)),X2),Y5),f(f(f(f(X1,X2),f(X2,X3)),X4),f(f(f(f(f(X1,X2),f(X2,X3)),X4),f(f(Y4,Y4),Y4)),f(X2,f(f(X2,f(f(X1,X1),X1)),X3))))),
inference(cp,[status(thm)],[t7,t7]) ).
cnf(t4003,plain,
f(f(f(f(X1,f(f(f(X2,X3),f(X3,X4)),Y4)),X3),Y5),f(f(f(f(X2,X3),f(X3,X4)),Y4),f(f(f(f(f(X2,X3),f(X3,X4)),Y4),f(f(X1,X1),X1)),f(X3,f(f(X3,f(f(X2,X2),X2)),X4))))) = f(f(f(X2,X3),f(X3,X4)),Y4),
inference(orient,[status(thm)],[t11]) ).
cnf(t33382,plain,
sFlat1 = f(f(f(f(X1,sFlat1),f(sFlat1,X2)),X3),sFlat0),
inference(cp,[status(thm)],[t33381,t4003]) ).
cnf(t43844,plain,
f(f(f(f(X1,sFlat1),f(sFlat1,X2)),X3),sFlat0) = sFlat1,
inference(orient,[status(thm)],[t33382]) ).
cnf(t7064,plain,
x2 = f(f(f(sFlat3,f(x2,f(x2,x2))),X1),f(x2,x2)),
inference(cp,[status(thm)],[t177,t7045]) ).
cnf(t7223,plain,
f(f(f(sFlat3,f(x2,f(x2,x2))),X1),f(x2,x2)) = x2,
inference(orient,[status(thm)],[t7064]) ).
cnf(t8492,plain,
x2 = f(sFlat5,f(x2,x2)),
inference(cp,[status(thm)],[t7223,t8477]) ).
cnf(t8530,plain,
f(sFlat5,f(x2,x2)) = x2,
inference(orient,[status(thm)],[t8492]) ).
cnf(t8535,plain,
sFlat5 = f(f(f(f(X1,sFlat5),x2),sFlat5),f(sFlat5,sFlat5)),
inference(cp,[status(thm)],[t3364,t8530]) ).
cnf(t9019,plain,
f(f(f(f(X1,sFlat5),x2),sFlat5),f(sFlat5,sFlat5)) = sFlat5,
inference(orient,[status(thm)],[t8535]) ).
cnf(t23,plain,
x0 = f(f(f(f(X1,x0),sFlat5),X2),f(x0,f(f(x0,f(f(X1,X1),X1)),sFlat4))),
inference(cp,[status(thm)],[t7,t21]) ).
cnf(t120,plain,
f(f(f(f(X1,x0),sFlat5),X2),f(x0,f(f(x0,f(f(X1,X1),X1)),sFlat4))) = x0,
inference(orient,[status(thm)],[t23]) ).
cnf(t520,plain,
f(f(X1,x0),sFlat5) = f(f(X1,x0),f(f(f(X1,x0),sFlat5),x0)),
inference(cp,[status(thm)],[t459,t120]) ).
cnf(t966,plain,
f(f(X1,x0),f(f(f(X1,x0),sFlat5),x0)) = f(f(X1,x0),sFlat5),
inference(orient,[status(thm)],[t520]) ).
cnf(t13143,plain,
f(f(f(f(x0,x0),X1),x0),sFlat5) = f(f(x0,x0),f(f(f(f(f(x0,x0),X1),x0),sFlat5),x0)),
inference(cp,[status(thm)],[t966,t13052]) ).
cnf(t45375,plain,
f(f(x0,x0),sFlat5) = f(f(x0,x0),f(f(f(f(f(x0,x0),X1),x0),sFlat5),x0)),
inference(step,[status(thm)],[t13143,t13052]) ).
cnf(t45376,plain,
f(f(x0,x0),sFlat5) = f(f(x0,x0),f(f(f(x0,x0),sFlat5),x0)),
inference(step,[status(thm)],[t45375,t13052]) ).
cnf(t45377,plain,
f(f(x0,x0),sFlat5) = f(f(x0,x0),f(x0,x0)),
inference(step,[status(thm)],[t45376,t13052]) ).
cnf(t45378,plain,
f(f(x0,x0),sFlat5) = x0,
inference(step,[status(thm)],[t45377,t12079]) ).
cnf(t13490,plain,
f(f(x0,x0),sFlat5) = x0,
inference(orient,[status(thm)],[t45378]) ).
cnf(t13493,plain,
sFlat5 = f(f(f(x0,x2),sFlat5),f(sFlat5,sFlat5)),
inference(cp,[status(thm)],[t9019,t13490]) ).
cnf(t45396,plain,
sFlat5 = f(f(sFlat0,sFlat5),f(sFlat5,sFlat5)),
inference(step,[status(thm)],[t13493,t24]) ).
cnf(t14029,plain,
f(f(sFlat0,sFlat5),f(sFlat5,sFlat5)) = sFlat5,
inference(orient,[status(thm)],[t45396]) ).
cnf(t17318,plain,
f(f(sFlat0,sFlat5),f(sFlat5,sFlat5)) = f(f(sFlat5,f(f(sFlat0,sFlat5),f(sFlat5,sFlat5))),f(sFlat0,sFlat5)),
inference(cp,[status(thm)],[t17278,t14029]) ).
cnf(t45462,plain,
sFlat5 = f(f(sFlat5,f(f(sFlat0,sFlat5),f(sFlat5,sFlat5))),f(sFlat0,sFlat5)),
inference(step,[status(thm)],[t17318,t14029]) ).
cnf(t45463,plain,
sFlat5 = f(f(sFlat5,sFlat5),f(sFlat0,sFlat5)),
inference(step,[status(thm)],[t45462,t14029]) ).
cnf(t17831,plain,
f(f(sFlat5,sFlat5),f(sFlat0,sFlat5)) = sFlat5,
inference(orient,[status(thm)],[t45463]) ).
cnf(t49,plain,
f(sFlat0,X1) = f(sFlat0,f(f(sFlat0,X1),f(f(f(sFlat0,X1),f(f(sFlat1,sFlat1),sFlat1)),X2))),
inference(cp,[status(thm)],[t7,t47]) ).
cnf(t81,plain,
f(sFlat0,f(f(sFlat0,X1),f(f(f(sFlat0,X1),f(f(sFlat1,sFlat1),sFlat1)),X2))) = f(sFlat0,X1),
inference(orient,[status(thm)],[t49]) ).
cnf(t146,plain,
f(sFlat0,f(x2,X1)) = f(sFlat0,f(f(sFlat0,f(x2,X1)),x2)),
inference(cp,[status(thm)],[t81,t140]) ).
cnf(t147,plain,
f(sFlat0,f(f(sFlat0,f(x2,X1)),x2)) = f(sFlat0,f(x2,X1)),
inference(orient,[status(thm)],[t146]) ).
cnf(t8531,plain,
sFlat5 = f(x2,f(sFlat5,sFlat5)),
inference(cp,[status(thm)],[t7939,t8530]) ).
cnf(t8558,plain,
f(x2,f(sFlat5,sFlat5)) = sFlat5,
inference(orient,[status(thm)],[t8531]) ).
cnf(t8565,plain,
f(sFlat0,f(x2,f(sFlat5,sFlat5))) = f(sFlat0,f(f(sFlat0,sFlat5),x2)),
inference(cp,[status(thm)],[t147,t8558]) ).
cnf(t45252,plain,
f(sFlat0,sFlat5) = f(sFlat0,f(f(sFlat0,sFlat5),x2)),
inference(step,[status(thm)],[t8565,t8558]) ).
cnf(t8821,plain,
f(sFlat0,f(f(sFlat0,sFlat5),x2)) = f(sFlat0,sFlat5),
inference(orient,[status(thm)],[t45252]) ).
cnf(t11821,plain,
f(f(f(sFlat0,f(x2,X1)),X2),f(x2,f(f(x2,f(f(x0,x0),x0)),X1))) = f(f(f(sFlat0,f(x2,X1)),X2),f(x2,f(f(f(sFlat0,f(x2,X1)),X2),f(x2,f(f(x2,f(f(x0,x0),x0)),X1))))),
inference(cp,[status(thm)],[t11799,t140]) ).
cnf(t45765,plain,
x2 = f(f(f(sFlat0,f(x2,X1)),X2),f(x2,f(f(f(sFlat0,f(x2,X1)),X2),f(x2,f(f(x2,f(f(x0,x0),x0)),X1))))),
inference(step,[status(thm)],[t11821,t140]) ).
cnf(t45766,plain,
x2 = f(f(f(sFlat0,f(x2,X1)),X2),f(x2,x2)),
inference(step,[status(thm)],[t45765,t140]) ).
cnf(t26011,plain,
f(f(f(sFlat0,f(x2,X1)),X2),f(x2,x2)) = x2,
inference(orient,[status(thm)],[t45766]) ).
cnf(t7048,plain,
f(f(f(x2,X1),f(x2,x2)),f(f(x2,x2),X2)) = f(x2,f(f(f(f(x2,X1),f(x2,x2)),f(f(x2,x2),X2)),f(x2,x2))),
inference(cp,[status(thm)],[t1132,t7045]) ).
cnf(t45220,plain,
f(x2,f(f(x2,x2),X2)) = f(x2,f(f(f(f(x2,X1),f(x2,x2)),f(f(x2,x2),X2)),f(x2,x2))),
inference(step,[status(thm)],[t7048,t7045]) ).
cnf(t45221,plain,
f(x2,f(f(x2,x2),X2)) = f(x2,f(f(x2,f(f(x2,x2),X2)),f(x2,x2))),
inference(step,[status(thm)],[t45220,t7045]) ).
cnf(t45222,plain,
f(x2,f(f(x2,x2),X2)) = f(x2,x2),
inference(step,[status(thm)],[t45221,t7045]) ).
cnf(t7104,plain,
f(x2,f(f(x2,x2),X1)) = f(x2,x2),
inference(orient,[status(thm)],[t45222]) ).
cnf(t7112,plain,
x2 = f(f(f(f(x2,x2),f(x2,X1)),X2),f(x2,f(f(x2,x2),X1))),
inference(cp,[status(thm)],[t7,t7104]) ).
cnf(t45225,plain,
x2 = f(f(f(f(x2,x2),f(x2,X1)),X2),f(x2,x2)),
inference(step,[status(thm)],[t7112,t7104]) ).
cnf(t7317,plain,
f(f(f(f(x2,x2),f(x2,X1)),X2),f(x2,x2)) = x2,
inference(orient,[status(thm)],[t45225]) ).
cnf(t8561,plain,
x2 = f(f(f(f(x2,x2),sFlat5),X1),f(x2,x2)),
inference(cp,[status(thm)],[t7317,t8558]) ).
cnf(t9051,plain,
f(f(f(f(x2,x2),sFlat5),X1),f(x2,x2)) = x2,
inference(orient,[status(thm)],[t8561]) ).
cnf(t9059,plain,
sFlat5 = f(x2,f(sFlat5,f(f(sFlat5,f(f(f(x2,x2),f(x2,x2)),f(x2,x2))),X1))),
inference(cp,[status(thm)],[t7,t9051]) ).
cnf(t45261,plain,
sFlat5 = f(x2,f(sFlat5,f(f(sFlat5,f(x2,f(x2,x2))),X1))),
inference(step,[status(thm)],[t9059,t7045]) ).
cnf(t9469,plain,
f(x2,f(sFlat5,f(f(sFlat5,f(x2,f(x2,x2))),X1))) = sFlat5,
inference(orient,[status(thm)],[t45261]) ).
cnf(t9470,plain,
sFlat5 = f(x2,f(sFlat5,f(x2,f(x2,x2)))),
inference(cp,[status(thm)],[t9469,t459]) ).
cnf(t9497,plain,
f(x2,f(sFlat5,f(x2,f(x2,x2)))) = sFlat5,
inference(orient,[status(thm)],[t9470]) ).
cnf(t26025,plain,
x2 = f(f(f(sFlat0,sFlat5),X1),f(x2,x2)),
inference(cp,[status(thm)],[t26011,t9497]) ).
cnf(t26208,plain,
f(f(f(sFlat0,sFlat5),X1),f(x2,x2)) = x2,
inference(orient,[status(thm)],[t26025]) ).
cnf(t26214,plain,
f(f(sFlat0,sFlat5),f(sFlat0,sFlat5)) = f(x2,f(sFlat0,sFlat5)),
inference(cp,[status(thm)],[t13052,t26208]) ).
cnf(t26213,plain,
f(f(sFlat0,sFlat5),f(sFlat0,sFlat5)) = f(f(sFlat0,sFlat5),x2),
inference(cp,[status(thm)],[t14064,t26208]) ).
cnf(t26261,plain,
f(f(sFlat0,sFlat5),f(sFlat0,sFlat5)) = f(f(sFlat0,sFlat5),x2),
inference(orient,[status(thm)],[t26213]) ).
cnf(t45774,plain,
f(f(sFlat0,sFlat5),x2) = f(x2,f(sFlat0,sFlat5)),
inference(step,[status(thm)],[t26214,t26261]) ).
cnf(t26469,plain,
f(f(sFlat0,sFlat5),x2) = f(x2,f(sFlat0,sFlat5)),
inference(orient,[status(thm)],[t45774]) ).
cnf(t45782,plain,
f(sFlat0,f(x2,f(sFlat0,sFlat5))) = f(sFlat0,sFlat5),
inference(step,[status(thm)],[t8821,t26469]) ).
cnf(t26523,plain,
f(sFlat0,f(x2,f(sFlat0,sFlat5))) = f(sFlat0,sFlat5),
inference(rw,[status(thm)],[t45782]) ).
cnf(t26679,plain,
f(sFlat0,f(x2,f(sFlat0,sFlat5))) = f(sFlat0,sFlat5),
inference(orient,[status(thm)],[t26523]) ).
cnf(t11830,plain,
f(f(f(f(X1,x0),sFlat5),X2),f(x0,f(f(x0,f(f(X1,X1),X1)),sFlat4))) = f(f(f(f(X1,x0),sFlat5),X2),f(x0,f(f(f(f(X1,x0),sFlat5),X2),f(x0,f(f(x0,f(f(X1,X1),X1)),sFlat4))))),
inference(cp,[status(thm)],[t11799,t120]) ).
cnf(t45826,plain,
x0 = f(f(f(f(X1,x0),sFlat5),X2),f(x0,f(f(f(f(X1,x0),sFlat5),X2),f(x0,f(f(x0,f(f(X1,X1),X1)),sFlat4))))),
inference(step,[status(thm)],[t11830,t120]) ).
cnf(t45827,plain,
x0 = f(f(f(f(X1,x0),sFlat5),X2),f(x0,x0)),
inference(step,[status(thm)],[t45826,t120]) ).
cnf(t28766,plain,
f(f(f(f(X1,x0),sFlat5),X2),f(x0,x0)) = x0,
inference(orient,[status(thm)],[t45827]) ).
cnf(t12405,plain,
f(f(f(sFlat1,X1),sFlat0),f(sFlat0,X2)) = f(sFlat1,f(f(f(f(sFlat1,X1),sFlat0),f(sFlat0,X2)),sFlat0)),
inference(cp,[status(thm)],[t1132,t12399]) ).
cnf(t45324,plain,
f(sFlat1,f(sFlat0,X2)) = f(sFlat1,f(f(f(f(sFlat1,X1),sFlat0),f(sFlat0,X2)),sFlat0)),
inference(step,[status(thm)],[t12405,t12399]) ).
cnf(t45325,plain,
f(sFlat1,f(sFlat0,X2)) = f(sFlat1,f(f(sFlat1,f(sFlat0,X2)),sFlat0)),
inference(step,[status(thm)],[t45324,t12399]) ).
cnf(t45326,plain,
f(sFlat1,f(sFlat0,X2)) = f(sFlat1,sFlat1),
inference(step,[status(thm)],[t45325,t12399]) ).
cnf(t45327,plain,
f(sFlat1,f(sFlat0,X2)) = sFlat0,
inference(step,[status(thm)],[t45326,t1461]) ).
cnf(t12595,plain,
f(sFlat1,f(sFlat0,X1)) = sFlat0,
inference(orient,[status(thm)],[t45327]) ).
cnf(t5451,plain,
sFlat0 = f(f(f(f(X1,sFlat0),f(sFlat0,sFlat1)),X2),f(sFlat0,sFlat0)),
inference(cp,[status(thm)],[t7,t5439]) ).
cnf(t45194,plain,
sFlat0 = f(f(f(f(X1,sFlat0),f(sFlat0,sFlat1)),X2),sFlat1),
inference(step,[status(thm)],[t5451,t35]) ).
cnf(t5628,plain,
f(f(f(f(X1,sFlat0),f(sFlat0,sFlat1)),X2),sFlat1) = sFlat0,
inference(orient,[status(thm)],[t45194]) ).
cnf(t26,plain,
x0 = f(f(f(f(X1,x0),sFlat0),X2),f(x0,f(f(x0,f(f(X1,X1),X1)),x2))),
inference(cp,[status(thm)],[t7,t24]) ).
cnf(t157,plain,
f(f(f(f(X1,x0),sFlat0),X2),f(x0,f(f(x0,f(f(X1,X1),X1)),x2))) = x0,
inference(orient,[status(thm)],[t26]) ).
cnf(t159,plain,
x0 = f(f(f(f(sFlat0,x0),sFlat0),X1),f(x0,f(f(x0,f(sFlat1,sFlat0)),x2))),
inference(cp,[status(thm)],[t157,t35]) ).
cnf(t171,plain,
f(f(f(f(sFlat0,x0),sFlat0),X1),f(x0,f(f(x0,f(sFlat1,sFlat0)),x2))) = x0,
inference(orient,[status(thm)],[t159]) ).
cnf(t5630,plain,
sFlat0 = f(x0,sFlat1),
inference(cp,[status(thm)],[t5628,t171]) ).
cnf(t5673,plain,
f(x0,sFlat1) = sFlat0,
inference(orient,[status(thm)],[t5630]) ).
cnf(t12165,plain,
x0 = f(sFlat0,f(x0,x0)),
inference(cp,[status(thm)],[t12079,t5673]) ).
cnf(t12367,plain,
f(sFlat0,f(x0,x0)) = x0,
inference(orient,[status(thm)],[t12165]) ).
cnf(t12596,plain,
sFlat0 = f(sFlat1,x0),
inference(cp,[status(thm)],[t12595,t12367]) ).
cnf(t12833,plain,
f(sFlat1,x0) = sFlat0,
inference(orient,[status(thm)],[t12596]) ).
cnf(t28773,plain,
x0 = f(f(f(sFlat0,sFlat5),X1),f(x0,x0)),
inference(cp,[status(thm)],[t28766,t12833]) ).
cnf(t29261,plain,
f(f(f(sFlat0,sFlat5),X1),f(x0,x0)) = x0,
inference(orient,[status(thm)],[t28773]) ).
cnf(t29269,plain,
f(f(sFlat0,sFlat5),f(sFlat0,sFlat5)) = f(x0,f(sFlat0,sFlat5)),
inference(cp,[status(thm)],[t13052,t29261]) ).
cnf(t45775,plain,
f(f(sFlat0,sFlat5),f(sFlat0,sFlat5)) = f(x2,f(sFlat0,sFlat5)),
inference(step,[status(thm)],[t26261,t26469]) ).
cnf(t26470,plain,
f(f(sFlat0,sFlat5),f(sFlat0,sFlat5)) = f(x2,f(sFlat0,sFlat5)),
inference(orient,[status(thm)],[t45775]) ).
cnf(t45835,plain,
f(x2,f(sFlat0,sFlat5)) = f(x0,f(sFlat0,sFlat5)),
inference(step,[status(thm)],[t29269,t26470]) ).
cnf(t8536,plain,
f(f(X1,sFlat5),f(sFlat5,f(x2,x2))) = f(f(X1,sFlat5),f(f(f(X1,sFlat5),x2),sFlat5)),
inference(cp,[status(thm)],[t1132,t8530]) ).
cnf(t45257,plain,
f(f(X1,sFlat5),x2) = f(f(X1,sFlat5),f(f(f(X1,sFlat5),x2),sFlat5)),
inference(step,[status(thm)],[t8536,t8530]) ).
cnf(t9190,plain,
f(f(X1,sFlat5),f(f(f(X1,sFlat5),x2),sFlat5)) = f(f(X1,sFlat5),x2),
inference(orient,[status(thm)],[t45257]) ).
cnf(t13491,plain,
f(f(f(x0,x0),sFlat5),x2) = f(x0,f(f(f(f(x0,x0),sFlat5),x2),sFlat5)),
inference(cp,[status(thm)],[t9190,t13490]) ).
cnf(t45387,plain,
f(x0,x2) = f(x0,f(f(f(f(x0,x0),sFlat5),x2),sFlat5)),
inference(step,[status(thm)],[t13491,t13490]) ).
cnf(t45388,plain,
sFlat0 = f(x0,f(f(f(f(x0,x0),sFlat5),x2),sFlat5)),
inference(step,[status(thm)],[t45387,t24]) ).
cnf(t45389,plain,
sFlat0 = f(x0,f(f(x0,x2),sFlat5)),
inference(step,[status(thm)],[t45388,t13490]) ).
cnf(t45390,plain,
sFlat0 = f(x0,f(sFlat0,sFlat5)),
inference(step,[status(thm)],[t45389,t24]) ).
cnf(t13573,plain,
f(x0,f(sFlat0,sFlat5)) = sFlat0,
inference(orient,[status(thm)],[t45390]) ).
cnf(t45836,plain,
f(x2,f(sFlat0,sFlat5)) = sFlat0,
inference(step,[status(thm)],[t45835,t13573]) ).
cnf(t29318,plain,
f(x2,f(sFlat0,sFlat5)) = sFlat0,
inference(orient,[status(thm)],[t45836]) ).
cnf(t45841,plain,
f(sFlat0,sFlat0) = f(sFlat0,sFlat5),
inference(step,[status(thm)],[t26679,t29318]) ).
cnf(t45842,plain,
sFlat1 = f(sFlat0,sFlat5),
inference(step,[status(thm)],[t45841,t35]) ).
cnf(t29352,plain,
sFlat1 = f(sFlat0,sFlat5),
inference(rw,[status(thm)],[t45842]) ).
cnf(t29357,plain,
f(sFlat0,sFlat5) = sFlat1,
inference(orient,[status(thm)],[t29352]) ).
cnf(t45850,plain,
f(f(sFlat5,sFlat5),sFlat1) = sFlat5,
inference(step,[status(thm)],[t17831,t29357]) ).
cnf(t29383,plain,
f(f(sFlat5,sFlat5),sFlat1) = sFlat5,
inference(rw,[status(thm)],[t45850]) ).
cnf(t29453,plain,
f(f(sFlat5,sFlat5),sFlat1) = sFlat5,
inference(orient,[status(thm)],[t29383]) ).
cnf(t43849,plain,
sFlat1 = f(f(f(sFlat5,f(sFlat1,X1)),X2),sFlat0),
inference(cp,[status(thm)],[t43844,t29453]) ).
cnf(t43908,plain,
f(f(f(sFlat5,f(sFlat1,X1)),X2),sFlat0) = sFlat1,
inference(orient,[status(thm)],[t43849]) ).
cnf(t9708,plain,
sFlat2 = f(sFlat1,f(sFlat2,sFlat2)),
inference(cp,[status(thm)],[t9619,t9704]) ).
cnf(t9763,plain,
f(sFlat1,f(sFlat2,sFlat2)) = sFlat2,
inference(orient,[status(thm)],[t9708]) ).
cnf(t43913,plain,
sFlat1 = f(f(f(sFlat5,sFlat2),X1),sFlat0),
inference(cp,[status(thm)],[t43908,t9763]) ).
cnf(t44018,plain,
f(f(f(sFlat5,sFlat2),X1),sFlat0) = sFlat1,
inference(orient,[status(thm)],[t43913]) ).
cnf(t44027,plain,
f(f(sFlat5,sFlat2),f(sFlat5,sFlat2)) = f(sFlat1,f(sFlat5,sFlat2)),
inference(cp,[status(thm)],[t13052,t44018]) ).
cnf(t45674,plain,
f(f(sFlat5,sFlat2),f(sFlat5,sFlat2)) = f(sFlat4,f(sFlat5,sFlat2)),
inference(step,[status(thm)],[t22242,t22834]) ).
cnf(t22835,plain,
f(f(sFlat5,sFlat2),f(sFlat5,sFlat2)) = f(sFlat4,f(sFlat5,sFlat2)),
inference(orient,[status(thm)],[t45674]) ).
cnf(t46148,plain,
f(sFlat4,f(sFlat5,sFlat2)) = f(sFlat1,f(sFlat5,sFlat2)),
inference(step,[status(thm)],[t44027,t22835]) ).
cnf(t44124,plain,
f(sFlat4,f(sFlat5,sFlat2)) = f(sFlat1,f(sFlat5,sFlat2)),
inference(orient,[status(thm)],[t46148]) ).
cnf(t46155,plain,
f(x1,f(sFlat5,sFlat2)) = f(sFlat1,f(sFlat5,sFlat2)),
inference(step,[status(thm)],[t22834,t44124]) ).
cnf(t44131,plain,
f(x1,f(sFlat5,sFlat2)) = f(sFlat1,f(sFlat5,sFlat2)),
inference(orient,[status(thm)],[t46155]) ).
cnf(t45852,plain,
f(f(sFlat1,X1),f(x0,x0)) = x0,
inference(step,[status(thm)],[t29261,t29357]) ).
cnf(t29385,plain,
f(f(sFlat1,X1),f(x0,x0)) = x0,
inference(rw,[status(thm)],[t45852]) ).
cnf(t29507,plain,
f(f(sFlat1,X1),f(x0,x0)) = x0,
inference(orient,[status(thm)],[t29385]) ).
cnf(t29509,plain,
f(sFlat1,X1) = f(f(f(sFlat1,X1),f(sFlat1,X1)),x0),
inference(cp,[status(thm)],[t13680,t29507]) ).
cnf(t31005,plain,
f(f(f(sFlat1,X1),f(sFlat1,X1)),x0) = f(sFlat1,X1),
inference(orient,[status(thm)],[t29509]) ).
cnf(t31012,plain,
x0 = f(f(f(f(sFlat1,X1),sFlat5),X2),f(x0,x0)),
inference(cp,[status(thm)],[t28766,t31005]) ).
cnf(t42667,plain,
f(f(f(f(sFlat1,X1),sFlat5),X2),f(x0,x0)) = x0,
inference(orient,[status(thm)],[t31012]) ).
cnf(t22158,plain,
f(sFlat5,sFlat2) = f(f(f(sFlat5,sFlat2),x1),sFlat5),
inference(cp,[status(thm)],[t17278,t22155]) ).
cnf(t22204,plain,
f(f(f(sFlat5,sFlat2),x1),sFlat5) = f(sFlat5,sFlat2),
inference(orient,[status(thm)],[t22158]) ).
cnf(t45655,plain,
f(f(x1,f(sFlat5,sFlat2)),sFlat5) = f(sFlat5,sFlat2),
inference(step,[status(thm)],[t22204,t22241]) ).
cnf(t22282,plain,
f(f(x1,f(sFlat5,sFlat2)),sFlat5) = f(sFlat5,sFlat2),
inference(rw,[status(thm)],[t45655]) ).
cnf(t22284,plain,
f(f(x1,f(sFlat5,sFlat2)),sFlat5) = f(sFlat5,sFlat2),
inference(orient,[status(thm)],[t22282]) ).
cnf(t45681,plain,
f(f(sFlat4,f(sFlat5,sFlat2)),sFlat5) = f(sFlat5,sFlat2),
inference(step,[status(thm)],[t22284,t22834]) ).
cnf(t22869,plain,
f(f(sFlat4,f(sFlat5,sFlat2)),sFlat5) = f(sFlat5,sFlat2),
inference(rw,[status(thm)],[t45681]) ).
cnf(t23085,plain,
f(f(sFlat4,f(sFlat5,sFlat2)),sFlat5) = f(sFlat5,sFlat2),
inference(orient,[status(thm)],[t22869]) ).
cnf(t46161,plain,
f(f(sFlat1,f(sFlat5,sFlat2)),sFlat5) = f(sFlat5,sFlat2),
inference(step,[status(thm)],[t23085,t44124]) ).
cnf(t44197,plain,
f(f(sFlat1,f(sFlat5,sFlat2)),sFlat5) = f(sFlat5,sFlat2),
inference(rw,[status(thm)],[t46161]) ).
cnf(t44397,plain,
f(f(sFlat1,f(sFlat5,sFlat2)),sFlat5) = f(sFlat5,sFlat2),
inference(orient,[status(thm)],[t44197]) ).
cnf(t44405,plain,
x0 = f(f(f(sFlat5,sFlat2),X1),f(x0,x0)),
inference(cp,[status(thm)],[t42667,t44397]) ).
cnf(t44753,plain,
f(f(f(sFlat5,sFlat2),X1),f(x0,x0)) = x0,
inference(orient,[status(thm)],[t44405]) ).
cnf(t44759,plain,
f(f(sFlat5,sFlat2),f(sFlat5,sFlat2)) = f(x0,f(sFlat5,sFlat2)),
inference(cp,[status(thm)],[t13052,t44753]) ).
cnf(t46149,plain,
f(f(sFlat5,sFlat2),f(sFlat5,sFlat2)) = f(sFlat1,f(sFlat5,sFlat2)),
inference(step,[status(thm)],[t22835,t44124]) ).
cnf(t44125,plain,
f(f(sFlat5,sFlat2),f(sFlat5,sFlat2)) = f(sFlat1,f(sFlat5,sFlat2)),
inference(orient,[status(thm)],[t46149]) ).
cnf(t46173,plain,
f(sFlat1,f(sFlat5,sFlat2)) = f(x0,f(sFlat5,sFlat2)),
inference(step,[status(thm)],[t44759,t44125]) ).
cnf(t11804,plain,
f(f(sFlat0,X1),f(sFlat2,f(f(sFlat2,f(sFlat1,sFlat0)),sFlat0))) = f(f(sFlat0,X1),f(sFlat2,f(f(sFlat0,X1),f(sFlat2,f(f(sFlat2,f(sFlat1,sFlat0)),sFlat0))))),
inference(cp,[status(thm)],[t11799,t10157]) ).
cnf(t45302,plain,
sFlat2 = f(f(sFlat0,X1),f(sFlat2,f(f(sFlat0,X1),f(sFlat2,f(f(sFlat2,f(sFlat1,sFlat0)),sFlat0))))),
inference(step,[status(thm)],[t11804,t10157]) ).
cnf(t45303,plain,
sFlat2 = f(f(sFlat0,X1),f(sFlat2,sFlat2)),
inference(step,[status(thm)],[t45302,t10157]) ).
cnf(t11999,plain,
f(f(sFlat0,X1),f(sFlat2,sFlat2)) = sFlat2,
inference(orient,[status(thm)],[t45303]) ).
cnf(t12368,plain,
sFlat2 = f(x0,f(sFlat2,sFlat2)),
inference(cp,[status(thm)],[t11999,t12367]) ).
cnf(t12569,plain,
f(x0,f(sFlat2,sFlat2)) = sFlat2,
inference(orient,[status(thm)],[t12368]) ).
cnf(t13757,plain,
x0 = f(f(x0,x0),sFlat2),
inference(cp,[status(thm)],[t13680,t12569]) ).
cnf(t13970,plain,
f(f(x0,x0),sFlat2) = x0,
inference(orient,[status(thm)],[t13757]) ).
cnf(t13972,plain,
f(f(f(x0,x0),sFlat2),f(sFlat2,X1)) = f(x0,f(f(f(f(x0,x0),sFlat2),f(sFlat2,X1)),sFlat2)),
inference(cp,[status(thm)],[t1132,t13970]) ).
cnf(t45621,plain,
f(x0,f(sFlat2,X1)) = f(x0,f(f(f(f(x0,x0),sFlat2),f(sFlat2,X1)),sFlat2)),
inference(step,[status(thm)],[t13972,t13970]) ).
cnf(t45622,plain,
f(x0,f(sFlat2,X1)) = f(x0,f(f(x0,f(sFlat2,X1)),sFlat2)),
inference(step,[status(thm)],[t45621,t13970]) ).
cnf(t20800,plain,
f(x0,f(f(x0,f(sFlat2,X1)),sFlat2)) = f(x0,f(sFlat2,X1)),
inference(orient,[status(thm)],[t45622]) ).
cnf(t13436,plain,
sFlat2 = f(f(f(x1,x2),sFlat2),f(sFlat2,sFlat2)),
inference(cp,[status(thm)],[t10714,t13433]) ).
cnf(t45395,plain,
sFlat2 = f(f(sFlat3,sFlat2),f(sFlat2,sFlat2)),
inference(step,[status(thm)],[t13436,t31]) ).
cnf(t13994,plain,
f(f(sFlat3,sFlat2),f(sFlat2,sFlat2)) = sFlat2,
inference(orient,[status(thm)],[t45395]) ).
cnf(t13996,plain,
f(sFlat3,sFlat2) = f(sFlat2,f(f(sFlat3,sFlat2),f(sFlat3,sFlat2))),
inference(cp,[status(thm)],[t12079,t13994]) ).
cnf(t19517,plain,
f(sFlat2,f(f(sFlat3,sFlat2),f(sFlat3,sFlat2))) = f(sFlat3,sFlat2),
inference(orient,[status(thm)],[t13996]) ).
cnf(t20802,plain,
f(x0,f(sFlat2,f(f(sFlat3,sFlat2),f(sFlat3,sFlat2)))) = f(x0,f(f(x0,f(sFlat3,sFlat2)),sFlat2)),
inference(cp,[status(thm)],[t20800,t19517]) ).
cnf(t45642,plain,
f(x0,f(sFlat3,sFlat2)) = f(x0,f(f(x0,f(sFlat3,sFlat2)),sFlat2)),
inference(step,[status(thm)],[t20802,t19517]) ).
cnf(t21471,plain,
f(x0,f(f(x0,f(sFlat3,sFlat2)),sFlat2)) = f(x0,f(sFlat3,sFlat2)),
inference(orient,[status(thm)],[t45642]) ).
cnf(t45663,plain,
f(x0,f(f(x0,sFlat4),sFlat2)) = f(x0,f(sFlat3,sFlat2)),
inference(step,[status(thm)],[t21471,t22457]) ).
cnf(t45664,plain,
f(x0,f(sFlat5,sFlat2)) = f(x0,f(sFlat3,sFlat2)),
inference(step,[status(thm)],[t45663,t21]) ).
cnf(t45665,plain,
f(x0,f(sFlat5,sFlat2)) = f(x0,sFlat4),
inference(step,[status(thm)],[t45664,t22457]) ).
cnf(t45666,plain,
f(x0,f(sFlat5,sFlat2)) = sFlat5,
inference(step,[status(thm)],[t45665,t21]) ).
cnf(t22486,plain,
f(x0,f(sFlat5,sFlat2)) = sFlat5,
inference(rw,[status(thm)],[t45666]) ).
cnf(t22595,plain,
f(x0,f(sFlat5,sFlat2)) = sFlat5,
inference(orient,[status(thm)],[t22486]) ).
cnf(t46174,plain,
f(sFlat1,f(sFlat5,sFlat2)) = sFlat5,
inference(step,[status(thm)],[t46173,t22595]) ).
cnf(t44807,plain,
f(sFlat1,f(sFlat5,sFlat2)) = sFlat5,
inference(orient,[status(thm)],[t46174]) ).
cnf(t46181,plain,
f(x1,f(sFlat5,sFlat2)) = sFlat5,
inference(step,[status(thm)],[t44131,t44807]) ).
cnf(t44814,plain,
f(x1,f(sFlat5,sFlat2)) = sFlat5,
inference(orient,[status(thm)],[t46181]) ).
cnf(t13971,plain,
sFlat2 = f(f(f(x0,f(sFlat2,X1)),sFlat2),f(sFlat2,sFlat2)),
inference(cp,[status(thm)],[t3364,t13970]) ).
cnf(t38698,plain,
f(f(f(x0,f(sFlat2,X1)),sFlat2),f(sFlat2,sFlat2)) = sFlat2,
inference(orient,[status(thm)],[t13971]) ).
cnf(t45658,plain,
f(sFlat2,sFlat3) = f(sFlat3,sFlat2),
inference(step,[status(thm)],[t19517,t22401]) ).
cnf(t22456,plain,
f(sFlat2,sFlat3) = f(sFlat3,sFlat2),
inference(rw,[status(thm)],[t45658]) ).
cnf(t45669,plain,
f(sFlat2,sFlat3) = sFlat4,
inference(step,[status(thm)],[t22456,t22457]) ).
cnf(t22488,plain,
f(sFlat2,sFlat3) = sFlat4,
inference(orient,[status(thm)],[t45669]) ).
cnf(t38701,plain,
sFlat2 = f(f(f(x0,sFlat4),sFlat2),f(sFlat2,sFlat2)),
inference(cp,[status(thm)],[t38698,t22488]) ).
cnf(t46055,plain,
sFlat2 = f(f(sFlat5,sFlat2),f(sFlat2,sFlat2)),
inference(step,[status(thm)],[t38701,t21]) ).
cnf(t38738,plain,
f(f(sFlat5,sFlat2),f(sFlat2,sFlat2)) = sFlat2,
inference(orient,[status(thm)],[t46055]) ).
cnf(t38740,plain,
f(sFlat5,sFlat2) = f(sFlat2,f(f(sFlat5,sFlat2),f(sFlat5,sFlat2))),
inference(cp,[status(thm)],[t12079,t38738]) ).
cnf(t46059,plain,
f(sFlat5,sFlat2) = f(sFlat2,f(sFlat4,f(sFlat5,sFlat2))),
inference(step,[status(thm)],[t38740,t22835]) ).
cnf(t38827,plain,
f(sFlat2,f(sFlat4,f(sFlat5,sFlat2))) = f(sFlat5,sFlat2),
inference(orient,[status(thm)],[t46059]) ).
cnf(t46159,plain,
f(sFlat2,f(sFlat1,f(sFlat5,sFlat2))) = f(sFlat5,sFlat2),
inference(step,[status(thm)],[t38827,t44124]) ).
cnf(t44195,plain,
f(sFlat2,f(sFlat1,f(sFlat5,sFlat2))) = f(sFlat5,sFlat2),
inference(rw,[status(thm)],[t46159]) ).
cnf(t44330,plain,
f(sFlat2,f(sFlat1,f(sFlat5,sFlat2))) = f(sFlat5,sFlat2),
inference(orient,[status(thm)],[t44195]) ).
cnf(t46189,plain,
f(sFlat2,sFlat5) = f(sFlat5,sFlat2),
inference(step,[status(thm)],[t44330,t44807]) ).
cnf(t44849,plain,
f(sFlat2,sFlat5) = f(sFlat5,sFlat2),
inference(rw,[status(thm)],[t46189]) ).
cnf(t44965,plain,
f(sFlat5,sFlat2) = f(sFlat2,sFlat5),
inference(orient,[status(thm)],[t44849]) ).
cnf(t46252,plain,
f(x1,f(sFlat2,sFlat5)) = sFlat5,
inference(step,[status(thm)],[t44814,t44965]) ).
cnf(t13756,plain,
x1 = f(f(x1,x1),sFlat5),
inference(cp,[status(thm)],[t13680,t12543]) ).
cnf(t13946,plain,
f(f(x1,x1),sFlat5) = x1,
inference(orient,[status(thm)],[t13756]) ).
cnf(t13948,plain,
f(f(f(x1,x1),sFlat5),f(sFlat5,X1)) = f(x1,f(f(f(f(x1,x1),sFlat5),f(sFlat5,X1)),sFlat5)),
inference(cp,[status(thm)],[t1132,t13946]) ).
cnf(t45618,plain,
f(x1,f(sFlat5,X1)) = f(x1,f(f(f(f(x1,x1),sFlat5),f(sFlat5,X1)),sFlat5)),
inference(step,[status(thm)],[t13948,t13946]) ).
cnf(t45619,plain,
f(x1,f(sFlat5,X1)) = f(x1,f(f(x1,f(sFlat5,X1)),sFlat5)),
inference(step,[status(thm)],[t45618,t13946]) ).
cnf(t20750,plain,
f(x1,f(f(x1,f(sFlat5,X1)),sFlat5)) = f(x1,f(sFlat5,X1)),
inference(orient,[status(thm)],[t45619]) ).
cnf(t14031,plain,
f(sFlat0,sFlat5) = f(sFlat5,f(f(sFlat0,sFlat5),f(sFlat0,sFlat5))),
inference(cp,[status(thm)],[t12079,t14029]) ).
cnf(t19565,plain,
f(sFlat5,f(f(sFlat0,sFlat5),f(sFlat0,sFlat5))) = f(sFlat0,sFlat5),
inference(orient,[status(thm)],[t14031]) ).
cnf(t20752,plain,
f(x1,f(sFlat5,f(f(sFlat0,sFlat5),f(sFlat0,sFlat5)))) = f(x1,f(f(x1,f(sFlat0,sFlat5)),sFlat5)),
inference(cp,[status(thm)],[t20750,t19565]) ).
cnf(t45639,plain,
f(x1,f(sFlat0,sFlat5)) = f(x1,f(f(x1,f(sFlat0,sFlat5)),sFlat5)),
inference(step,[status(thm)],[t20752,t19565]) ).
cnf(t21392,plain,
f(x1,f(f(x1,f(sFlat0,sFlat5)),sFlat5)) = f(x1,f(sFlat0,sFlat5)),
inference(orient,[status(thm)],[t45639]) ).
cnf(t45853,plain,
f(x1,f(f(x1,sFlat1),sFlat5)) = f(x1,f(sFlat0,sFlat5)),
inference(step,[status(thm)],[t21392,t29357]) ).
cnf(t45854,plain,
f(x1,f(sFlat2,sFlat5)) = f(x1,f(sFlat0,sFlat5)),
inference(step,[status(thm)],[t45853,t44]) ).
cnf(t45855,plain,
f(x1,f(sFlat2,sFlat5)) = f(x1,sFlat1),
inference(step,[status(thm)],[t45854,t29357]) ).
cnf(t45856,plain,
f(x1,f(sFlat2,sFlat5)) = sFlat2,
inference(step,[status(thm)],[t45855,t44]) ).
cnf(t29386,plain,
f(x1,f(sFlat2,sFlat5)) = sFlat2,
inference(rw,[status(thm)],[t45856]) ).
cnf(t29482,plain,
f(x1,f(sFlat2,sFlat5)) = sFlat2,
inference(orient,[status(thm)],[t29386]) ).
cnf(t46253,plain,
sFlat2 = sFlat5,
inference(step,[status(thm)],[t46252,t29482]) ).
cnf(t45004,plain,
sFlat2 = sFlat5,
inference(rw,[status(thm)],[t46253]) ).
cnf(t45013,plain,
sFlat5 = sFlat2,
inference(orient,[status(thm)],[t45004]) ).
cnf(t46265,plain,
f(x0,sFlat4) = sFlat2,
inference(step,[status(thm)],[t21,t45013]) ).
cnf(t45014,plain,
f(x0,sFlat4) = sFlat2,
inference(orient,[status(thm)],[t46265]) ).
cnf(goal_0,negated_conjecture,
f(x1,f(f(x0,x2),f(x0,x2))) != f(x0,f(f(x1,x2),f(x1,x2))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
f(x1,f(sFlat0,f(x0,x2))) != f(x0,f(f(x1,x2),f(x1,x2))),
inference(rw,[status(thm)],[goal_0,t24]) ).
cnf(g0_1,plain,
f(x1,f(sFlat0,sFlat0)) != f(x0,f(f(x1,x2),f(x1,x2))),
inference(rw,[status(thm)],[g0_0,t24]) ).
cnf(g0_2,plain,
f(x1,sFlat1) != f(x0,f(f(x1,x2),f(x1,x2))),
inference(rw,[status(thm)],[g0_1,t35]) ).
cnf(g0_3,plain,
sFlat2 != f(x0,f(f(x1,x2),f(x1,x2))),
inference(rw,[status(thm)],[g0_2,t44]) ).
cnf(g0_4,plain,
sFlat2 != f(x0,f(sFlat3,f(x1,x2))),
inference(rw,[status(thm)],[g0_3,t31]) ).
cnf(g0_5,plain,
sFlat2 != f(x0,f(sFlat3,sFlat3)),
inference(rw,[status(thm)],[g0_4,t31]) ).
cnf(g0_6,plain,
sFlat2 != f(x0,sFlat4),
inference(rw,[status(thm)],[g0_5,t40]) ).
cnf(g0_7,plain,
sFlat2 != sFlat2,
inference(rw,[status(thm)],[g0_6,t45014]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_7]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT393-1 : TPTP v9.3.1. Released v5.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.35 % Computer : n015.cluster.edu
% 0.09/0.35 % Model : x86_64 x86_64
% 0.09/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.35 % Memory : 8046.5625MB
% 0.09/0.35 % OS : Linux 6.8.0-71-generic
% 0.09/0.35 % CPULimit : 300
% 0.09/0.35 % WCLimit : 300
% 0.09/0.35 % DateTime : Wed Sep 23 21:35:40 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 65.47/8.86 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 65.47/8.86 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------