%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT393-2 : TPTP v9.3.1. Released v5.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n010.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 46.03s 6.36s
% Output : CNFRefutation 46.03s
% Verified :
% SZS Type : Refutation
% Derivation depth : 95
% Number of leaves : 8
% Syntax : Number of clauses : 528 ( 528 unt; 0 nHn; 244 RR)
% Number of literals : 528 ( 527 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 : 446 ( 225 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(t58888,plain,
f(sFlat0,f(x0,x2)) = sFlat1,
inference(step,[status(thm)],[t13,t24]) ).
cnf(t58889,plain,
f(sFlat0,sFlat0) = sFlat1,
inference(step,[status(thm)],[t58888,t24]) ).
cnf(t27,plain,
f(sFlat0,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t58889]) ).
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(t58890,plain,
sFlat2 = f(x1,f(sFlat0,f(x0,x2))),
inference(step,[status(thm)],[t3,t24]) ).
cnf(t58891,plain,
sFlat2 = f(x1,f(sFlat0,sFlat0)),
inference(step,[status(thm)],[t58890,t24]) ).
cnf(t28,plain,
f(x1,f(sFlat0,sFlat0)) = sFlat2,
inference(orient,[status(thm)],[t58891]) ).
cnf(t58894,plain,
f(x1,sFlat1) = sFlat2,
inference(step,[status(thm)],[t28,t35]) ).
cnf(t39,plain,
f(x1,sFlat1) = sFlat2,
inference(rw,[status(thm)],[t58894]) ).
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(t58892,plain,
f(sFlat3,f(x1,x2)) = sFlat4,
inference(step,[status(thm)],[t17,t31]) ).
cnf(t58893,plain,
f(sFlat3,sFlat3) = sFlat4,
inference(step,[status(thm)],[t58892,t31]) ).
cnf(t34,plain,
f(sFlat3,sFlat3) = sFlat4,
inference(rw,[status(thm)],[t58893]) ).
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(t58887,plain,
sFlat5 = f(x0,sFlat4),
inference(step,[status(thm)],[t6,t17]) ).
cnf(t21,plain,
f(x0,sFlat4) = sFlat5,
inference(orient,[status(thm)],[t58887]) ).
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(t9,plain,
X1 = f(f(X1,X2),f(X1,f(f(X1,f(f(f(f(X3,X1),f(X1,X4)),f(f(X3,X1),f(X1,X4))),f(f(X3,X1),f(X1,X4)))),f(f(X1,f(f(X3,X3),X3)),X4)))),
inference(cp,[status(thm)],[t7,t7]) ).
cnf(t1691,plain,
f(f(X1,X2),f(X1,f(f(X1,f(f(f(f(X3,X1),f(X1,X4)),f(f(X3,X1),f(X1,X4))),f(f(X3,X1),f(X1,X4)))),f(f(X1,f(f(X3,X3),X3)),X4)))) = X1,
inference(orient,[status(thm)],[t9]) ).
cnf(t2369,plain,
f(X1,X2) = f(X1,f(f(X1,X2),f(X1,X2))),
inference(cp,[status(thm)],[t459,t1691]) ).
cnf(t2607,plain,
f(X1,f(f(X1,X2),f(X1,X2))) = f(X1,X2),
inference(orient,[status(thm)],[t2369]) ).
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(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(t2631,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)],[t2607,t93]) ).
cnf(t58995,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)],[t2631,t93]) ).
cnf(t58996,plain,
sFlat4 = f(f(f(sFlat5,f(sFlat4,X1)),X2),f(sFlat4,sFlat4)),
inference(step,[status(thm)],[t58995,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(t58903,plain,
sFlat3 = f(f(f(f(X1,sFlat3),sFlat4),sFlat3),f(sFlat3,sFlat3)),
inference(step,[status(thm)],[t1197,t318]) ).
cnf(t58904,plain,
sFlat3 = f(f(f(f(X1,sFlat3),sFlat4),sFlat3),sFlat4),
inference(step,[status(thm)],[t58903,t40]) ).
cnf(t1362,plain,
f(f(f(f(X1,sFlat3),sFlat4),sFlat3),sFlat4) = sFlat3,
inference(orient,[status(thm)],[t58904]) ).
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(t58896,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)],[t58896]) ).
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(t58899,plain,
sFlat3 = f(f(f(sFlat4,sFlat4),sFlat3),f(sFlat3,sFlat3)),
inference(step,[status(thm)],[t1215,t71]) ).
cnf(t58900,plain,
sFlat3 = f(f(f(sFlat4,sFlat4),sFlat3),sFlat4),
inference(step,[status(thm)],[t58899,t40]) ).
cnf(t1334,plain,
f(f(f(sFlat4,sFlat4),sFlat3),sFlat4) = sFlat3,
inference(orient,[status(thm)],[t58900]) ).
cnf(t1363,plain,
sFlat3 = f(f(sFlat3,sFlat3),sFlat4),
inference(cp,[status(thm)],[t1362,t1334]) ).
cnf(t58905,plain,
sFlat3 = f(sFlat4,sFlat4),
inference(step,[status(thm)],[t1363,t40]) ).
cnf(t1378,plain,
f(sFlat4,sFlat4) = sFlat3,
inference(orient,[status(thm)],[t58905]) ).
cnf(t58997,plain,
sFlat4 = f(f(f(sFlat5,f(sFlat4,X1)),X2),sFlat3),
inference(step,[status(thm)],[t58996,t1378]) ).
cnf(t3187,plain,
f(f(f(sFlat5,f(sFlat4,X1)),X2),sFlat3) = sFlat4,
inference(orient,[status(thm)],[t58997]) ).
cnf(t3188,plain,
sFlat4 = f(sFlat5,sFlat3),
inference(cp,[status(thm)],[t3187,t1691]) ).
cnf(t3214,plain,
f(sFlat5,sFlat3) = sFlat4,
inference(orient,[status(thm)],[t3188]) ).
cnf(t3216,plain,
sFlat5 = f(f(f(f(sFlat3,sFlat5),sFlat4),X1),f(sFlat5,f(f(sFlat5,f(sFlat4,sFlat3)),sFlat3))),
inference(cp,[status(thm)],[t329,t3214]) ).
cnf(t2615,plain,
f(f(f(f(X1,sFlat3),sFlat4),X2),f(sFlat3,f(f(sFlat3,f(f(X1,X1),X1)),sFlat3))) = f(f(f(f(X1,sFlat3),sFlat4),X2),f(sFlat3,f(f(f(f(X1,sFlat3),sFlat4),X2),f(sFlat3,f(f(sFlat3,f(f(X1,X1),X1)),sFlat3))))),
inference(cp,[status(thm)],[t2607,t318]) ).
cnf(t58966,plain,
sFlat3 = f(f(f(f(X1,sFlat3),sFlat4),X2),f(sFlat3,f(f(f(f(X1,sFlat3),sFlat4),X2),f(sFlat3,f(f(sFlat3,f(f(X1,X1),X1)),sFlat3))))),
inference(step,[status(thm)],[t2615,t318]) ).
cnf(t58967,plain,
sFlat3 = f(f(f(f(X1,sFlat3),sFlat4),X2),f(sFlat3,sFlat3)),
inference(step,[status(thm)],[t58966,t318]) ).
cnf(t58968,plain,
sFlat3 = f(f(f(f(X1,sFlat3),sFlat4),X2),sFlat4),
inference(step,[status(thm)],[t58967,t40]) ).
cnf(t2955,plain,
f(f(f(f(X1,sFlat3),sFlat4),X2),sFlat4) = sFlat3,
inference(orient,[status(thm)],[t58968]) ).
cnf(t2956,plain,
sFlat3 = f(f(X1,sFlat3),sFlat4),
inference(cp,[status(thm)],[t2955,t1691]) ).
cnf(t2984,plain,
f(f(X1,sFlat3),sFlat4) = sFlat3,
inference(orient,[status(thm)],[t2956]) ).
cnf(t58969,plain,
f(f(sFlat3,X2),sFlat4) = sFlat3,
inference(step,[status(thm)],[t2955,t2984]) ).
cnf(t3005,plain,
f(f(sFlat3,X2),sFlat4) = sFlat3,
inference(rw,[status(thm)],[t58969]) ).
cnf(t3008,plain,
f(f(sFlat3,X1),sFlat4) = sFlat3,
inference(orient,[status(thm)],[t3005]) ).
cnf(t59156,plain,
sFlat5 = f(f(sFlat3,X1),f(sFlat5,f(f(sFlat5,f(sFlat4,sFlat3)),sFlat3))),
inference(step,[status(thm)],[t3216,t3008]) ).
cnf(t17576,plain,
f(f(sFlat3,X1),f(sFlat5,f(f(sFlat5,f(sFlat4,sFlat3)),sFlat3))) = sFlat5,
inference(orient,[status(thm)],[t59156]) ).
cnf(t17589,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)],[t2607,t17576]) ).
cnf(t59157,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)],[t17589,t17576]) ).
cnf(t59158,plain,
sFlat5 = f(f(sFlat3,X1),f(sFlat5,sFlat5)),
inference(step,[status(thm)],[t59157,t17576]) ).
cnf(t17654,plain,
f(f(sFlat3,X1),f(sFlat5,sFlat5)) = sFlat5,
inference(orient,[status(thm)],[t59158]) ).
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(t2992,plain,
x1 = f(sFlat3,f(x1,f(f(x1,f(f(X1,X1),X1)),x2))),
inference(cp,[status(thm)],[t198,t2984]) ).
cnf(t17106,plain,
f(sFlat3,f(x1,f(f(x1,f(f(X1,X1),X1)),x2))) = x1,
inference(orient,[status(thm)],[t2992]) ).
cnf(t2321,plain,
X1 = f(f(sFlat3,X1),f(X1,f(f(X1,f(sFlat4,sFlat3)),X2))),
inference(cp,[status(thm)],[t329,t1691]) ).
cnf(t13016,plain,
f(f(sFlat3,X1),f(X1,f(f(X1,f(sFlat4,sFlat3)),X2))) = X1,
inference(orient,[status(thm)],[t2321]) ).
cnf(t13042,plain,
X1 = f(f(sFlat3,X1),f(X1,X1)),
inference(cp,[status(thm)],[t13016,t1691]) ).
cnf(t13157,plain,
f(f(sFlat3,X1),f(X1,X1)) = X1,
inference(orient,[status(thm)],[t13042]) ).
cnf(t17109,plain,
x1 = f(sFlat3,f(x1,f(f(x1,f(sFlat3,f(sFlat3,sFlat3))),x2))),
inference(cp,[status(thm)],[t17106,t13157]) ).
cnf(t59150,plain,
x1 = f(sFlat3,f(x1,f(f(x1,f(sFlat3,sFlat4)),x2))),
inference(step,[status(thm)],[t17109,t40]) ).
cnf(t17195,plain,
f(sFlat3,f(x1,f(f(x1,f(sFlat3,sFlat4)),x2))) = x1,
inference(orient,[status(thm)],[t59150]) ).
cnf(t17655,plain,
sFlat5 = f(x1,f(sFlat5,sFlat5)),
inference(cp,[status(thm)],[t17654,t17195]) ).
cnf(t17729,plain,
f(x1,f(sFlat5,sFlat5)) = sFlat5,
inference(orient,[status(thm)],[t17655]) ).
cnf(t17733,plain,
f(f(X1,x1),f(x1,f(sFlat5,sFlat5))) = f(f(X1,x1),f(f(f(X1,x1),sFlat5),x1)),
inference(cp,[status(thm)],[t1132,t17729]) ).
cnf(t59166,plain,
f(f(X1,x1),sFlat5) = f(f(X1,x1),f(f(f(X1,x1),sFlat5),x1)),
inference(step,[status(thm)],[t17733,t17729]) ).
cnf(t18348,plain,
f(f(X1,x1),f(f(f(X1,x1),sFlat5),x1)) = f(f(X1,x1),sFlat5),
inference(orient,[status(thm)],[t59166]) ).
cnf(t13167,plain,
X1 = f(f(X1,X2),f(X1,f(f(X1,f(sFlat4,sFlat3)),X1))),
inference(cp,[status(thm)],[t329,t13157]) ).
cnf(t22041,plain,
f(f(X1,X2),f(X1,f(f(X1,f(sFlat4,sFlat3)),X1))) = X1,
inference(orient,[status(thm)],[t13167]) ).
cnf(t22201,plain,
f(f(X1,X2),f(X1,f(f(X1,f(sFlat4,sFlat3)),X1))) = f(f(X1,X2),f(X1,f(f(X1,X2),f(X1,f(f(X1,f(sFlat4,sFlat3)),X1))))),
inference(cp,[status(thm)],[t2607,t22041]) ).
cnf(t59218,plain,
X1 = f(f(X1,X2),f(X1,f(f(X1,X2),f(X1,f(f(X1,f(sFlat4,sFlat3)),X1))))),
inference(step,[status(thm)],[t22201,t22041]) ).
cnf(t59219,plain,
X1 = f(f(X1,X2),f(X1,X1)),
inference(step,[status(thm)],[t59218,t22041]) ).
cnf(t22306,plain,
f(f(X1,X2),f(X1,X1)) = X1,
inference(orient,[status(thm)],[t59219]) ).
cnf(t2624,plain,
f(f(f(f(X1,x1),sFlat3),X2),f(x1,f(f(x1,f(f(X1,X1),X1)),x2))) = f(f(f(f(X1,x1),sFlat3),X2),f(x1,f(f(f(f(X1,x1),sFlat3),X2),f(x1,f(f(x1,f(f(X1,X1),X1)),x2))))),
inference(cp,[status(thm)],[t2607,t198]) ).
cnf(t59036,plain,
x1 = f(f(f(f(X1,x1),sFlat3),X2),f(x1,f(f(f(f(X1,x1),sFlat3),X2),f(x1,f(f(x1,f(f(X1,X1),X1)),x2))))),
inference(step,[status(thm)],[t2624,t198]) ).
cnf(t59037,plain,
x1 = f(f(f(f(X1,x1),sFlat3),X2),f(x1,x1)),
inference(step,[status(thm)],[t59036,t198]) ).
cnf(t5061,plain,
f(f(f(f(X1,x1),sFlat3),X2),f(x1,x1)) = x1,
inference(orient,[status(thm)],[t59037]) ).
cnf(t5062,plain,
x1 = f(f(X1,x1),f(x1,x1)),
inference(cp,[status(thm)],[t5061,t1691]) ).
cnf(t5111,plain,
f(f(X1,x1),f(x1,x1)) = x1,
inference(orient,[status(thm)],[t5062]) ).
cnf(t22427,plain,
f(x1,x1) = f(f(f(x1,x1),X1),x1),
inference(cp,[status(thm)],[t22306,t5111]) ).
cnf(t23009,plain,
f(f(f(x1,x1),X1),x1) = f(x1,x1),
inference(orient,[status(thm)],[t22427]) ).
cnf(t23010,plain,
f(f(f(f(x1,x1),X1),x1),sFlat5) = f(f(x1,x1),f(f(f(f(f(x1,x1),X1),x1),sFlat5),x1)),
inference(cp,[status(thm)],[t18348,t23009]) ).
cnf(t59240,plain,
f(f(x1,x1),sFlat5) = f(f(x1,x1),f(f(f(f(f(x1,x1),X1),x1),sFlat5),x1)),
inference(step,[status(thm)],[t23010,t23009]) ).
cnf(t59241,plain,
f(f(x1,x1),sFlat5) = f(f(x1,x1),f(f(f(x1,x1),sFlat5),x1)),
inference(step,[status(thm)],[t59240,t23009]) ).
cnf(t59242,plain,
f(f(x1,x1),sFlat5) = f(f(x1,x1),f(x1,x1)),
inference(step,[status(thm)],[t59241,t23009]) ).
cnf(t5115,plain,
x1 = f(f(x1,X1),f(x1,f(f(x1,f(sFlat4,sFlat3)),x1))),
inference(cp,[status(thm)],[t329,t5111]) ).
cnf(t18530,plain,
f(f(x1,X1),f(x1,f(f(x1,f(sFlat4,sFlat3)),x1))) = x1,
inference(orient,[status(thm)],[t5115]) ).
cnf(t18548,plain,
f(f(x1,X1),f(x1,f(f(x1,f(sFlat4,sFlat3)),x1))) = f(f(x1,X1),f(x1,f(f(x1,X1),f(x1,f(f(x1,f(sFlat4,sFlat3)),x1))))),
inference(cp,[status(thm)],[t2607,t18530]) ).
cnf(t59169,plain,
x1 = f(f(x1,X1),f(x1,f(f(x1,X1),f(x1,f(f(x1,f(sFlat4,sFlat3)),x1))))),
inference(step,[status(thm)],[t18548,t18530]) ).
cnf(t59170,plain,
x1 = f(f(x1,X1),f(x1,x1)),
inference(step,[status(thm)],[t59169,t18530]) ).
cnf(t18630,plain,
f(f(x1,X1),f(x1,x1)) = x1,
inference(orient,[status(thm)],[t59170]) ).
cnf(t59243,plain,
f(f(x1,x1),sFlat5) = x1,
inference(step,[status(thm)],[t59242,t18630]) ).
cnf(t23081,plain,
f(f(x1,x1),sFlat5) = x1,
inference(orient,[status(thm)],[t59243]) ).
cnf(t23086,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,t23081]) ).
cnf(t59962,plain,
f(x1,f(sFlat5,X1)) = f(x1,f(f(f(f(x1,x1),sFlat5),f(sFlat5,X1)),sFlat5)),
inference(step,[status(thm)],[t23086,t23081]) ).
cnf(t59963,plain,
f(x1,f(sFlat5,X1)) = f(x1,f(f(x1,f(sFlat5,X1)),sFlat5)),
inference(step,[status(thm)],[t59962,t23081]) ).
cnf(t58814,plain,
f(x1,f(f(x1,f(sFlat5,X1)),sFlat5)) = f(x1,f(sFlat5,X1)),
inference(orient,[status(thm)],[t59963]) ).
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(t2327,plain,
X1 = f(f(sFlat0,X1),f(X1,f(f(X1,f(sFlat1,sFlat0)),X2))),
inference(cp,[status(thm)],[t234,t1691]) ).
cnf(t14946,plain,
f(f(sFlat0,X1),f(X1,f(f(X1,f(sFlat1,sFlat0)),X2))) = X1,
inference(orient,[status(thm)],[t2327]) ).
cnf(t14970,plain,
X1 = f(f(sFlat0,X1),f(X1,X1)),
inference(cp,[status(thm)],[t14946,t1691]) ).
cnf(t15132,plain,
f(f(sFlat0,X1),f(X1,X1)) = X1,
inference(orient,[status(thm)],[t14970]) ).
cnf(t22428,plain,
f(X1,X1) = f(f(f(X1,X1),X2),X1),
inference(cp,[status(thm)],[t22306,t22306]) ).
cnf(t23356,plain,
f(f(f(X1,X1),X2),X1) = f(X1,X1),
inference(orient,[status(thm)],[t22428]) ).
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(t2638,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)],[t2607,t120]) ).
cnf(t59060,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)],[t2638,t120]) ).
cnf(t59061,plain,
x0 = f(f(f(f(X1,x0),sFlat5),X2),f(x0,x0)),
inference(step,[status(thm)],[t59060,t120]) ).
cnf(t6139,plain,
f(f(f(f(X1,x0),sFlat5),X2),f(x0,x0)) = x0,
inference(orient,[status(thm)],[t59061]) ).
cnf(t2313,plain,
f(f(X1,X1),f(X1,f(f(X1,f(f(f(f(X2,X1),f(X1,X3)),f(f(X2,X1),f(X1,X3))),f(f(X2,X1),f(X1,X3)))),f(f(X1,f(f(X2,X2),X2)),X3)))) = f(f(X1,X1),f(X1,X1)),
inference(cp,[status(thm)],[t1132,t1691]) ).
cnf(t58937,plain,
X1 = f(f(X1,X1),f(X1,X1)),
inference(step,[status(thm)],[t2313,t1691]) ).
cnf(t2387,plain,
f(f(X1,X1),f(X1,X1)) = X1,
inference(orient,[status(thm)],[t58937]) ).
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(t521,plain,
f(f(X1,x0),sFlat0) = f(f(X1,x0),f(f(f(X1,x0),sFlat0),x0)),
inference(cp,[status(thm)],[t459,t157]) ).
cnf(t976,plain,
f(f(X1,x0),f(f(f(X1,x0),sFlat0),x0)) = f(f(X1,x0),sFlat0),
inference(orient,[status(thm)],[t521]) ).
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(t2613,plain,
f(f(f(sFlat2,f(sFlat1,X1)),X2),f(sFlat1,f(f(sFlat1,f(f(x1,x1),x1)),X1))) = f(f(f(sFlat2,f(sFlat1,X1)),X2),f(sFlat1,f(f(f(sFlat2,f(sFlat1,X1)),X2),f(sFlat1,f(f(sFlat1,f(f(x1,x1),x1)),X1))))),
inference(cp,[status(thm)],[t2607,t417]) ).
cnf(t58950,plain,
sFlat1 = f(f(f(sFlat2,f(sFlat1,X1)),X2),f(sFlat1,f(f(f(sFlat2,f(sFlat1,X1)),X2),f(sFlat1,f(f(sFlat1,f(f(x1,x1),x1)),X1))))),
inference(step,[status(thm)],[t2613,t417]) ).
cnf(t58951,plain,
sFlat1 = f(f(f(sFlat2,f(sFlat1,X1)),X2),f(sFlat1,sFlat1)),
inference(step,[status(thm)],[t58950,t417]) ).
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(t58914,plain,
sFlat0 = f(f(f(f(X1,sFlat0),sFlat1),sFlat0),f(sFlat0,sFlat0)),
inference(step,[status(thm)],[t1201,t218]) ).
cnf(t58915,plain,
sFlat0 = f(f(f(f(X1,sFlat0),sFlat1),sFlat0),sFlat1),
inference(step,[status(thm)],[t58914,t35]) ).
cnf(t1445,plain,
f(f(f(f(X1,sFlat0),sFlat1),sFlat0),sFlat1) = sFlat0,
inference(orient,[status(thm)],[t58915]) ).
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(t58895,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)],[t58895]) ).
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(t58901,plain,
sFlat0 = f(f(f(sFlat1,sFlat1),sFlat0),f(sFlat0,sFlat0)),
inference(step,[status(thm)],[t1220,t54]) ).
cnf(t58902,plain,
sFlat0 = f(f(f(sFlat1,sFlat1),sFlat0),sFlat1),
inference(step,[status(thm)],[t58901,t35]) ).
cnf(t1348,plain,
f(f(f(sFlat1,sFlat1),sFlat0),sFlat1) = sFlat0,
inference(orient,[status(thm)],[t58902]) ).
cnf(t1446,plain,
sFlat0 = f(f(sFlat0,sFlat0),sFlat1),
inference(cp,[status(thm)],[t1445,t1348]) ).
cnf(t58916,plain,
sFlat0 = f(sFlat1,sFlat1),
inference(step,[status(thm)],[t1446,t35]) ).
cnf(t1461,plain,
f(sFlat1,sFlat1) = sFlat0,
inference(orient,[status(thm)],[t58916]) ).
cnf(t58952,plain,
sFlat1 = f(f(f(sFlat2,f(sFlat1,X1)),X2),sFlat0),
inference(step,[status(thm)],[t58951,t1461]) ).
cnf(t2789,plain,
f(f(f(sFlat2,f(sFlat1,X1)),X2),sFlat0) = sFlat1,
inference(orient,[status(thm)],[t58952]) ).
cnf(t422,plain,
f(sFlat1,X1) = f(sFlat1,f(f(sFlat1,X1),f(f(f(sFlat1,X1),f(f(sFlat2,sFlat2),sFlat2)),X2))),
inference(cp,[status(thm)],[t7,t417]) ).
cnf(t427,plain,
f(sFlat1,f(f(sFlat1,X1),f(f(f(sFlat1,X1),f(f(sFlat2,sFlat2),sFlat2)),X2))) = f(sFlat1,X1),
inference(orient,[status(thm)],[t422]) ).
cnf(t714,plain,
f(sFlat1,X1) = f(sFlat1,f(f(sFlat1,X1),f(f(sFlat2,sFlat2),sFlat2))),
inference(cp,[status(thm)],[t427,t459]) ).
cnf(t792,plain,
f(sFlat1,f(f(sFlat1,X1),f(f(sFlat2,sFlat2),sFlat2))) = f(sFlat1,X1),
inference(orient,[status(thm)],[t714]) ).
cnf(t1465,plain,
f(sFlat1,sFlat1) = f(sFlat1,f(sFlat0,f(f(sFlat2,sFlat2),sFlat2))),
inference(cp,[status(thm)],[t792,t1461]) ).
cnf(t58928,plain,
sFlat0 = f(sFlat1,f(sFlat0,f(f(sFlat2,sFlat2),sFlat2))),
inference(step,[status(thm)],[t1465,t1461]) ).
cnf(t1559,plain,
f(sFlat1,f(sFlat0,f(f(sFlat2,sFlat2),sFlat2))) = sFlat0,
inference(orient,[status(thm)],[t58928]) ).
cnf(t2791,plain,
sFlat1 = f(f(f(sFlat2,sFlat0),X1),sFlat0),
inference(cp,[status(thm)],[t2789,t1559]) ).
cnf(t2790,plain,
sFlat1 = f(sFlat2,sFlat0),
inference(cp,[status(thm)],[t2789,t1691]) ).
cnf(t2817,plain,
f(sFlat2,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t2790]) ).
cnf(t58953,plain,
sFlat1 = f(f(sFlat1,X1),sFlat0),
inference(step,[status(thm)],[t2791,t2817]) ).
cnf(t2836,plain,
f(f(sFlat1,X1),sFlat0) = sFlat1,
inference(orient,[status(thm)],[t58953]) ).
cnf(t2840,plain,
f(f(sFlat1,x0),sFlat0) = f(f(sFlat1,x0),f(sFlat1,x0)),
inference(cp,[status(thm)],[t976,t2836]) ).
cnf(t58961,plain,
sFlat1 = f(f(sFlat1,x0),f(sFlat1,x0)),
inference(step,[status(thm)],[t2840,t2836]) ).
cnf(t2885,plain,
f(f(sFlat1,x0),f(sFlat1,x0)) = sFlat1,
inference(orient,[status(thm)],[t58961]) ).
cnf(t2886,plain,
f(sFlat1,x0) = f(f(f(sFlat1,x0),f(sFlat1,x0)),sFlat1),
inference(cp,[status(thm)],[t2387,t2885]) ).
cnf(t58962,plain,
f(sFlat1,x0) = f(sFlat1,sFlat1),
inference(step,[status(thm)],[t2886,t2885]) ).
cnf(t58963,plain,
f(sFlat1,x0) = sFlat0,
inference(step,[status(thm)],[t58962,t1461]) ).
cnf(t2915,plain,
f(sFlat1,x0) = sFlat0,
inference(orient,[status(thm)],[t58963]) ).
cnf(t6141,plain,
x0 = f(f(f(sFlat0,sFlat5),X1),f(x0,x0)),
inference(cp,[status(thm)],[t6139,t2915]) ).
cnf(t6231,plain,
f(f(f(sFlat0,sFlat5),X1),f(x0,x0)) = x0,
inference(orient,[status(thm)],[t6141]) ).
cnf(t23389,plain,
f(f(sFlat0,sFlat5),f(sFlat0,sFlat5)) = f(x0,f(sFlat0,sFlat5)),
inference(cp,[status(thm)],[t23356,t6231]) ).
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(t2625,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,f(f(f(sFlat3,f(x2,X1)),X2),f(x2,f(f(x2,f(f(x1,x1),x1)),X1))))),
inference(cp,[status(thm)],[t2607,t177]) ).
cnf(t59038,plain,
x2 = f(f(f(sFlat3,f(x2,X1)),X2),f(x2,f(f(f(sFlat3,f(x2,X1)),X2),f(x2,f(f(x2,f(f(x1,x1),x1)),X1))))),
inference(step,[status(thm)],[t2625,t177]) ).
cnf(t59039,plain,
x2 = f(f(f(sFlat3,f(x2,X1)),X2),f(x2,x2)),
inference(step,[status(thm)],[t59038,t177]) ).
cnf(t5197,plain,
f(f(f(sFlat3,f(x2,X1)),X2),f(x2,x2)) = x2,
inference(orient,[status(thm)],[t59039]) ).
cnf(t5198,plain,
x2 = f(sFlat3,f(x2,x2)),
inference(cp,[status(thm)],[t5197,t3008]) ).
cnf(t5245,plain,
f(sFlat3,f(x2,x2)) = x2,
inference(orient,[status(thm)],[t5198]) ).
cnf(t5247,plain,
sFlat3 = f(x2,sFlat4),
inference(cp,[status(thm)],[t3008,t5245]) ).
cnf(t5295,plain,
f(x2,sFlat4) = sFlat3,
inference(orient,[status(thm)],[t5247]) ).
cnf(t5297,plain,
x2 = f(f(f(sFlat3,sFlat3),X1),f(x2,x2)),
inference(cp,[status(thm)],[t5197,t5295]) ).
cnf(t59042,plain,
x2 = f(f(sFlat4,X1),f(x2,x2)),
inference(step,[status(thm)],[t5297,t40]) ).
cnf(t5437,plain,
f(f(sFlat4,X1),f(x2,x2)) = x2,
inference(orient,[status(thm)],[t59042]) ).
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(t2316,plain,
sFlat5 = f(f(sFlat3,sFlat5),f(sFlat5,f(sFlat4,sFlat3))),
inference(cp,[status(thm)],[t1001,t1691]) ).
cnf(t2431,plain,
f(f(sFlat3,sFlat5),f(sFlat5,f(sFlat4,sFlat3))) = sFlat5,
inference(orient,[status(thm)],[t2316]) ).
cnf(t2433,plain,
f(f(sFlat3,sFlat5),f(sFlat5,f(sFlat4,sFlat3))) = f(f(sFlat3,sFlat5),f(sFlat5,sFlat5)),
inference(cp,[status(thm)],[t1132,t2431]) ).
cnf(t58938,plain,
sFlat5 = f(f(sFlat3,sFlat5),f(sFlat5,sFlat5)),
inference(step,[status(thm)],[t2433,t2431]) ).
cnf(t2457,plain,
f(f(sFlat3,sFlat5),f(sFlat5,sFlat5)) = sFlat5,
inference(orient,[status(thm)],[t58938]) ).
cnf(t3215,plain,
f(f(X1,sFlat5),f(sFlat5,sFlat3)) = f(f(X1,sFlat5),f(f(f(X1,sFlat5),sFlat4),sFlat5)),
inference(cp,[status(thm)],[t1132,t3214]) ).
cnf(t59090,plain,
f(f(X1,sFlat5),sFlat4) = f(f(X1,sFlat5),f(f(f(X1,sFlat5),sFlat4),sFlat5)),
inference(step,[status(thm)],[t3215,t3214]) ).
cnf(t9325,plain,
f(f(X1,sFlat5),f(f(f(X1,sFlat5),sFlat4),sFlat5)) = f(f(X1,sFlat5),sFlat4),
inference(orient,[status(thm)],[t59090]) ).
cnf(t9329,plain,
f(f(sFlat3,sFlat5),sFlat4) = f(f(sFlat3,sFlat5),f(sFlat3,sFlat5)),
inference(cp,[status(thm)],[t9325,t3008]) ).
cnf(t59091,plain,
sFlat3 = f(f(sFlat3,sFlat5),f(sFlat3,sFlat5)),
inference(step,[status(thm)],[t9329,t3008]) ).
cnf(t9361,plain,
f(f(sFlat3,sFlat5),f(sFlat3,sFlat5)) = sFlat3,
inference(orient,[status(thm)],[t59091]) ).
cnf(t9362,plain,
f(sFlat3,sFlat5) = f(f(f(sFlat3,sFlat5),f(sFlat3,sFlat5)),sFlat3),
inference(cp,[status(thm)],[t2387,t9361]) ).
cnf(t59092,plain,
f(sFlat3,sFlat5) = f(sFlat3,sFlat3),
inference(step,[status(thm)],[t9362,t9361]) ).
cnf(t59093,plain,
f(sFlat3,sFlat5) = sFlat4,
inference(step,[status(thm)],[t59092,t40]) ).
cnf(t9406,plain,
f(sFlat3,sFlat5) = sFlat4,
inference(orient,[status(thm)],[t59093]) ).
cnf(t59094,plain,
f(sFlat4,f(sFlat5,sFlat5)) = sFlat5,
inference(step,[status(thm)],[t2457,t9406]) ).
cnf(t9431,plain,
f(sFlat4,f(sFlat5,sFlat5)) = sFlat5,
inference(rw,[status(thm)],[t59094]) ).
cnf(t9434,plain,
f(sFlat4,f(sFlat5,sFlat5)) = sFlat5,
inference(orient,[status(thm)],[t9431]) ).
cnf(t9435,plain,
x2 = f(sFlat5,f(x2,x2)),
inference(cp,[status(thm)],[t5437,t9434]) ).
cnf(t9475,plain,
f(sFlat5,f(x2,x2)) = x2,
inference(orient,[status(thm)],[t9435]) ).
cnf(t9476,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,t9475]) ).
cnf(t59111,plain,
f(f(X1,sFlat5),x2) = f(f(X1,sFlat5),f(f(f(X1,sFlat5),x2),sFlat5)),
inference(step,[status(thm)],[t9476,t9475]) ).
cnf(t11267,plain,
f(f(X1,sFlat5),f(f(f(X1,sFlat5),x2),sFlat5)) = f(f(X1,sFlat5),x2),
inference(orient,[status(thm)],[t59111]) ).
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(t6140,plain,
x0 = f(f(X1,x0),f(x0,x0)),
inference(cp,[status(thm)],[t6139,t1691]) ).
cnf(t6187,plain,
f(f(X1,x0),f(x0,x0)) = x0,
inference(orient,[status(thm)],[t6140]) ).
cnf(t22426,plain,
f(x0,x0) = f(f(f(x0,x0),X1),x0),
inference(cp,[status(thm)],[t22306,t6187]) ).
cnf(t22534,plain,
f(f(f(x0,x0),X1),x0) = f(x0,x0),
inference(orient,[status(thm)],[t22426]) ).
cnf(t22549,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,t22534]) ).
cnf(t59228,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)],[t22549,t22534]) ).
cnf(t59229,plain,
f(f(x0,x0),sFlat5) = f(f(x0,x0),f(f(f(x0,x0),sFlat5),x0)),
inference(step,[status(thm)],[t59228,t22534]) ).
cnf(t59230,plain,
f(f(x0,x0),sFlat5) = f(f(x0,x0),f(x0,x0)),
inference(step,[status(thm)],[t59229,t22534]) ).
cnf(t6191,plain,
x0 = f(f(x0,X1),f(x0,f(f(x0,f(sFlat4,sFlat3)),x0))),
inference(cp,[status(thm)],[t329,t6187]) ).
cnf(t19672,plain,
f(f(x0,X1),f(x0,f(f(x0,f(sFlat4,sFlat3)),x0))) = x0,
inference(orient,[status(thm)],[t6191]) ).
cnf(t19689,plain,
f(f(x0,X1),f(x0,f(f(x0,f(sFlat4,sFlat3)),x0))) = f(f(x0,X1),f(x0,f(f(x0,X1),f(x0,f(f(x0,f(sFlat4,sFlat3)),x0))))),
inference(cp,[status(thm)],[t2607,t19672]) ).
cnf(t59183,plain,
x0 = f(f(x0,X1),f(x0,f(f(x0,X1),f(x0,f(f(x0,f(sFlat4,sFlat3)),x0))))),
inference(step,[status(thm)],[t19689,t19672]) ).
cnf(t59184,plain,
x0 = f(f(x0,X1),f(x0,x0)),
inference(step,[status(thm)],[t59183,t19672]) ).
cnf(t19771,plain,
f(f(x0,X1),f(x0,x0)) = x0,
inference(orient,[status(thm)],[t59184]) ).
cnf(t59231,plain,
f(f(x0,x0),sFlat5) = x0,
inference(step,[status(thm)],[t59230,t19771]) ).
cnf(t22689,plain,
f(f(x0,x0),sFlat5) = x0,
inference(orient,[status(thm)],[t59231]) ).
cnf(t22694,plain,
f(f(f(x0,x0),sFlat5),x2) = f(x0,f(f(f(f(x0,x0),sFlat5),x2),sFlat5)),
inference(cp,[status(thm)],[t11267,t22689]) ).
cnf(t59232,plain,
f(x0,x2) = f(x0,f(f(f(f(x0,x0),sFlat5),x2),sFlat5)),
inference(step,[status(thm)],[t22694,t22689]) ).
cnf(t59233,plain,
sFlat0 = f(x0,f(f(f(f(x0,x0),sFlat5),x2),sFlat5)),
inference(step,[status(thm)],[t59232,t24]) ).
cnf(t59234,plain,
sFlat0 = f(x0,f(f(x0,x2),sFlat5)),
inference(step,[status(thm)],[t59233,t22689]) ).
cnf(t59235,plain,
sFlat0 = f(x0,f(sFlat0,sFlat5)),
inference(step,[status(thm)],[t59234,t24]) ).
cnf(t22732,plain,
f(x0,f(sFlat0,sFlat5)) = sFlat0,
inference(orient,[status(thm)],[t59235]) ).
cnf(t59311,plain,
f(f(sFlat0,sFlat5),f(sFlat0,sFlat5)) = sFlat0,
inference(step,[status(thm)],[t23389,t22732]) ).
cnf(t24324,plain,
f(f(sFlat0,sFlat5),f(sFlat0,sFlat5)) = sFlat0,
inference(orient,[status(thm)],[t59311]) ).
cnf(t24333,plain,
f(sFlat0,sFlat5) = f(sFlat0,sFlat0),
inference(cp,[status(thm)],[t2607,t24324]) ).
cnf(t59312,plain,
f(sFlat0,sFlat5) = sFlat1,
inference(step,[status(thm)],[t24333,t35]) ).
cnf(t24391,plain,
f(sFlat0,sFlat5) = sFlat1,
inference(orient,[status(thm)],[t59312]) ).
cnf(t24392,plain,
sFlat5 = f(sFlat1,f(sFlat5,sFlat5)),
inference(cp,[status(thm)],[t15132,t24391]) ).
cnf(t24431,plain,
f(sFlat1,f(sFlat5,sFlat5)) = sFlat5,
inference(orient,[status(thm)],[t24392]) ).
cnf(t24432,plain,
sFlat1 = f(sFlat5,f(sFlat1,sFlat1)),
inference(cp,[status(thm)],[t22306,t24431]) ).
cnf(t59313,plain,
sFlat1 = f(sFlat5,sFlat0),
inference(step,[status(thm)],[t24432,t1461]) ).
cnf(t24477,plain,
f(sFlat5,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t59313]) ).
cnf(t58819,plain,
f(x1,f(sFlat5,sFlat0)) = f(x1,f(f(x1,sFlat1),sFlat5)),
inference(cp,[status(thm)],[t58814,t24477]) ).
cnf(t59964,plain,
f(x1,sFlat1) = f(x1,f(f(x1,sFlat1),sFlat5)),
inference(step,[status(thm)],[t58819,t24477]) ).
cnf(t59965,plain,
sFlat2 = f(x1,f(f(x1,sFlat1),sFlat5)),
inference(step,[status(thm)],[t59964,t44]) ).
cnf(t59966,plain,
sFlat2 = f(x1,f(sFlat2,sFlat5)),
inference(step,[status(thm)],[t59965,t44]) ).
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(t6493,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(t7612,plain,
x1 = f(f(f(f(X1,x1),f(x1,X2)),X3),f(x1,x1)),
inference(cp,[status(thm)],[t5061,t6493]) ).
cnf(t20338,plain,
f(f(f(f(X1,x1),f(x1,X2)),X3),f(x1,x1)) = x1,
inference(orient,[status(thm)],[t7612]) ).
cnf(t20340,plain,
x1 = f(f(f(f(X1,x1),sFlat5),X2),f(x1,x1)),
inference(cp,[status(thm)],[t20338,t17729]) ).
cnf(t20485,plain,
f(f(f(f(X1,x1),sFlat5),X2),f(x1,x1)) = x1,
inference(orient,[status(thm)],[t20340]) ).
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(t13721,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(t13734,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)],[t2607,t13721]) ).
cnf(t59127,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)],[t13734,t13721]) ).
cnf(t59128,plain,
x1 = f(f(f(f(X1,x1),sFlat2),X2),f(x1,x1)),
inference(step,[status(thm)],[t59127,t13721]) ).
cnf(t14039,plain,
f(f(f(f(X1,x1),sFlat2),X2),f(x1,x1)) = x1,
inference(orient,[status(thm)],[t59128]) ).
cnf(t513,plain,
f(f(X1,x1),sFlat3) = f(f(X1,x1),f(f(f(X1,x1),sFlat3),x1)),
inference(cp,[status(thm)],[t459,t198]) ).
cnf(t916,plain,
f(f(X1,x1),f(f(f(X1,x1),sFlat3),x1)) = f(f(X1,x1),sFlat3),
inference(orient,[status(thm)],[t513]) ).
cnf(t94,plain,
f(sFlat4,X1) = f(sFlat4,f(f(sFlat4,X1),f(f(f(sFlat4,X1),f(f(sFlat5,sFlat5),sFlat5)),X2))),
inference(cp,[status(thm)],[t7,t93]) ).
cnf(t99,plain,
f(sFlat4,f(f(sFlat4,X1),f(f(f(sFlat4,X1),f(f(sFlat5,sFlat5),sFlat5)),X2))) = f(sFlat4,X1),
inference(orient,[status(thm)],[t94]) ).
cnf(t726,plain,
f(sFlat4,X1) = f(sFlat4,f(f(sFlat4,X1),f(f(sFlat5,sFlat5),sFlat5))),
inference(cp,[status(thm)],[t99,t459]) ).
cnf(t805,plain,
f(sFlat4,f(f(sFlat4,X1),f(f(sFlat5,sFlat5),sFlat5))) = f(sFlat4,X1),
inference(orient,[status(thm)],[t726]) ).
cnf(t1382,plain,
f(sFlat4,sFlat4) = f(sFlat4,f(sFlat3,f(f(sFlat5,sFlat5),sFlat5))),
inference(cp,[status(thm)],[t805,t1378]) ).
cnf(t58927,plain,
sFlat3 = f(sFlat4,f(sFlat3,f(f(sFlat5,sFlat5),sFlat5))),
inference(step,[status(thm)],[t1382,t1378]) ).
cnf(t1542,plain,
f(sFlat4,f(sFlat3,f(f(sFlat5,sFlat5),sFlat5))) = sFlat3,
inference(orient,[status(thm)],[t58927]) ).
cnf(t3189,plain,
sFlat4 = f(f(f(sFlat5,sFlat3),X1),sFlat3),
inference(cp,[status(thm)],[t3187,t1542]) ).
cnf(t58998,plain,
sFlat4 = f(f(sFlat4,X1),sFlat3),
inference(step,[status(thm)],[t3189,t3214]) ).
cnf(t3232,plain,
f(f(sFlat4,X1),sFlat3) = sFlat4,
inference(orient,[status(thm)],[t58998]) ).
cnf(t3236,plain,
f(f(sFlat4,x1),sFlat3) = f(f(sFlat4,x1),f(sFlat4,x1)),
inference(cp,[status(thm)],[t916,t3232]) ).
cnf(t59005,plain,
sFlat4 = f(f(sFlat4,x1),f(sFlat4,x1)),
inference(step,[status(thm)],[t3236,t3232]) ).
cnf(t3276,plain,
f(f(sFlat4,x1),f(sFlat4,x1)) = sFlat4,
inference(orient,[status(thm)],[t59005]) ).
cnf(t3277,plain,
f(sFlat4,x1) = f(f(f(sFlat4,x1),f(sFlat4,x1)),sFlat4),
inference(cp,[status(thm)],[t2387,t3276]) ).
cnf(t59006,plain,
f(sFlat4,x1) = f(sFlat4,sFlat4),
inference(step,[status(thm)],[t3277,t3276]) ).
cnf(t59007,plain,
f(sFlat4,x1) = sFlat3,
inference(step,[status(thm)],[t59006,t1378]) ).
cnf(t3304,plain,
f(sFlat4,x1) = sFlat3,
inference(orient,[status(thm)],[t59007]) ).
cnf(t14041,plain,
x1 = f(f(f(sFlat3,sFlat2),X1),f(x1,x1)),
inference(cp,[status(thm)],[t14039,t3304]) ).
cnf(t14114,plain,
f(f(f(sFlat3,sFlat2),X1),f(x1,x1)) = x1,
inference(orient,[status(thm)],[t14041]) ).
cnf(t14115,plain,
x1 = f(sFlat2,f(x1,x1)),
inference(cp,[status(thm)],[t14114,t13016]) ).
cnf(t14191,plain,
f(sFlat2,f(x1,x1)) = x1,
inference(orient,[status(thm)],[t14115]) ).
cnf(t14198,plain,
f(f(X1,sFlat2),f(sFlat2,f(x1,x1))) = f(f(X1,sFlat2),f(f(f(X1,sFlat2),x1),sFlat2)),
inference(cp,[status(thm)],[t1132,t14191]) ).
cnf(t59131,plain,
f(f(X1,sFlat2),x1) = f(f(X1,sFlat2),f(f(f(X1,sFlat2),x1),sFlat2)),
inference(step,[status(thm)],[t14198,t14191]) ).
cnf(t14853,plain,
f(f(X1,sFlat2),f(f(f(X1,sFlat2),x1),sFlat2)) = f(f(X1,sFlat2),x1),
inference(orient,[status(thm)],[t59131]) ).
cnf(t23437,plain,
f(f(f(f(sFlat2,sFlat2),X1),sFlat2),x1) = f(f(sFlat2,sFlat2),f(f(f(f(f(sFlat2,sFlat2),X1),sFlat2),x1),sFlat2)),
inference(cp,[status(thm)],[t14853,t23356]) ).
cnf(t59272,plain,
f(f(sFlat2,sFlat2),x1) = f(f(sFlat2,sFlat2),f(f(f(f(f(sFlat2,sFlat2),X1),sFlat2),x1),sFlat2)),
inference(step,[status(thm)],[t23437,t23356]) ).
cnf(t59273,plain,
f(f(sFlat2,sFlat2),x1) = f(f(sFlat2,sFlat2),f(f(f(sFlat2,sFlat2),x1),sFlat2)),
inference(step,[status(thm)],[t59272,t23356]) ).
cnf(t59274,plain,
f(f(sFlat2,sFlat2),x1) = f(f(sFlat2,sFlat2),f(sFlat2,sFlat2)),
inference(step,[status(thm)],[t59273,t23356]) ).
cnf(t59275,plain,
f(f(sFlat2,sFlat2),x1) = sFlat2,
inference(step,[status(thm)],[t59274,t22306]) ).
cnf(t23732,plain,
f(f(sFlat2,sFlat2),x1) = sFlat2,
inference(orient,[status(thm)],[t59275]) ).
cnf(t23733,plain,
x1 = f(f(f(sFlat2,sFlat5),X1),f(x1,x1)),
inference(cp,[status(thm)],[t20485,t23732]) ).
cnf(t29362,plain,
f(f(f(sFlat2,sFlat5),X1),f(x1,x1)) = x1,
inference(orient,[status(thm)],[t23733]) ).
cnf(t29368,plain,
f(f(sFlat2,sFlat5),f(sFlat2,sFlat5)) = f(x1,f(sFlat2,sFlat5)),
inference(cp,[status(thm)],[t23356,t29362]) ).
cnf(t24435,plain,
sFlat1 = f(f(f(sFlat2,sFlat5),X1),sFlat0),
inference(cp,[status(thm)],[t2789,t24431]) ).
cnf(t25203,plain,
f(f(f(sFlat2,sFlat5),X1),sFlat0) = sFlat1,
inference(orient,[status(thm)],[t24435]) ).
cnf(t25206,plain,
f(f(sFlat2,sFlat5),f(sFlat2,sFlat5)) = f(sFlat1,f(sFlat2,sFlat5)),
inference(cp,[status(thm)],[t23356,t25203]) ).
cnf(t27290,plain,
f(f(sFlat2,sFlat5),f(sFlat2,sFlat5)) = f(sFlat1,f(sFlat2,sFlat5)),
inference(orient,[status(thm)],[t25206]) ).
cnf(t59391,plain,
f(sFlat1,f(sFlat2,sFlat5)) = f(x1,f(sFlat2,sFlat5)),
inference(step,[status(thm)],[t29368,t27290]) ).
cnf(t29438,plain,
f(x1,f(sFlat2,sFlat5)) = f(sFlat1,f(sFlat2,sFlat5)),
inference(orient,[status(thm)],[t59391]) ).
cnf(t23474,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,t23356]) ).
cnf(t59314,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)],[t23474,t23356]) ).
cnf(t59315,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)],[t59314,t23356]) ).
cnf(t59316,plain,
f(f(X1,X1),f(X1,X3)) = f(f(X1,X1),f(X1,X1)),
inference(step,[status(thm)],[t59315,t23356]) ).
cnf(t59317,plain,
f(f(X1,X1),f(X1,X3)) = X1,
inference(step,[status(thm)],[t59316,t22306]) ).
cnf(t24617,plain,
f(f(X1,X1),f(X1,X2)) = X1,
inference(orient,[status(thm)],[t59317]) ).
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(t59115,plain,
X2 = f(f(f(f(X1,X2),f(X2,X3)),X2),f(X2,X2)),
inference(step,[status(thm)],[t1216,t7]) ).
cnf(t12271,plain,
f(f(f(f(X1,X2),f(X2,X3)),X2),f(X2,X2)) = X2,
inference(orient,[status(thm)],[t59115]) ).
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(t2626,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)],[t2607,t140]) ).
cnf(t59046,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)],[t2626,t140]) ).
cnf(t59047,plain,
x2 = f(f(f(sFlat0,f(x2,X1)),X2),f(x2,x2)),
inference(step,[status(thm)],[t59046,t140]) ).
cnf(t5558,plain,
f(f(f(sFlat0,f(x2,X1)),X2),f(x2,x2)) = x2,
inference(orient,[status(thm)],[t59047]) ).
cnf(t222,plain,
sFlat0 = f(f(f(f(sFlat3,sFlat0),sFlat1),X1),f(sFlat0,f(f(sFlat0,f(sFlat4,sFlat3)),sFlat0))),
inference(cp,[status(thm)],[t218,t40]) ).
cnf(t228,plain,
f(f(f(f(sFlat3,sFlat0),sFlat1),X1),f(sFlat0,f(f(sFlat0,f(sFlat4,sFlat3)),sFlat0))) = sFlat0,
inference(orient,[status(thm)],[t222]) ).
cnf(t2618,plain,
f(f(f(f(sFlat3,sFlat0),sFlat1),X1),f(sFlat0,f(f(sFlat0,f(sFlat4,sFlat3)),sFlat0))) = f(f(f(f(sFlat3,sFlat0),sFlat1),X1),f(sFlat0,f(f(f(f(sFlat3,sFlat0),sFlat1),X1),f(sFlat0,f(f(sFlat0,f(sFlat4,sFlat3)),sFlat0))))),
inference(cp,[status(thm)],[t2607,t228]) ).
cnf(t58980,plain,
sFlat0 = f(f(f(f(sFlat3,sFlat0),sFlat1),X1),f(sFlat0,f(f(f(f(sFlat3,sFlat0),sFlat1),X1),f(sFlat0,f(f(sFlat0,f(sFlat4,sFlat3)),sFlat0))))),
inference(step,[status(thm)],[t2618,t228]) ).
cnf(t58981,plain,
sFlat0 = f(f(f(f(sFlat3,sFlat0),sFlat1),X1),f(sFlat0,sFlat0)),
inference(step,[status(thm)],[t58980,t228]) ).
cnf(t58982,plain,
sFlat0 = f(f(f(f(sFlat3,sFlat0),sFlat1),X1),sFlat1),
inference(step,[status(thm)],[t58981,t35]) ).
cnf(t3051,plain,
f(f(f(f(sFlat3,sFlat0),sFlat1),X1),sFlat1) = sFlat0,
inference(orient,[status(thm)],[t58982]) ).
cnf(t3052,plain,
sFlat0 = f(f(sFlat3,sFlat0),sFlat1),
inference(cp,[status(thm)],[t3051,t1691]) ).
cnf(t3077,plain,
f(f(sFlat3,sFlat0),sFlat1) = sFlat0,
inference(orient,[status(thm)],[t3052]) ).
cnf(t58983,plain,
f(f(sFlat0,X1),sFlat1) = sFlat0,
inference(step,[status(thm)],[t3051,t3077]) ).
cnf(t3096,plain,
f(f(sFlat0,X1),sFlat1) = sFlat0,
inference(rw,[status(thm)],[t58983]) ).
cnf(t3098,plain,
f(f(sFlat0,X1),sFlat1) = sFlat0,
inference(orient,[status(thm)],[t3096]) ).
cnf(t5559,plain,
x2 = f(sFlat0,f(x2,x2)),
inference(cp,[status(thm)],[t5558,t3098]) ).
cnf(t5606,plain,
f(sFlat0,f(x2,x2)) = x2,
inference(orient,[status(thm)],[t5559]) ).
cnf(t5607,plain,
sFlat0 = f(x2,sFlat1),
inference(cp,[status(thm)],[t3098,t5606]) ).
cnf(t5635,plain,
f(x2,sFlat1) = sFlat0,
inference(orient,[status(thm)],[t5607]) ).
cnf(t5637,plain,
x2 = f(f(f(sFlat0,sFlat0),X1),f(x2,x2)),
inference(cp,[status(thm)],[t5558,t5635]) ).
cnf(t59050,plain,
x2 = f(f(sFlat1,X1),f(x2,x2)),
inference(step,[status(thm)],[t5637,t35]) ).
cnf(t5742,plain,
f(f(sFlat1,X1),f(x2,x2)) = x2,
inference(orient,[status(thm)],[t59050]) ).
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(t2317,plain,
sFlat2 = f(f(sFlat0,sFlat2),f(sFlat2,f(sFlat1,sFlat0))),
inference(cp,[status(thm)],[t986,t1691]) ).
cnf(t2482,plain,
f(f(sFlat0,sFlat2),f(sFlat2,f(sFlat1,sFlat0))) = sFlat2,
inference(orient,[status(thm)],[t2317]) ).
cnf(t2484,plain,
f(f(sFlat0,sFlat2),f(sFlat2,f(sFlat1,sFlat0))) = f(f(sFlat0,sFlat2),f(sFlat2,sFlat2)),
inference(cp,[status(thm)],[t1132,t2482]) ).
cnf(t58939,plain,
sFlat2 = f(f(sFlat0,sFlat2),f(sFlat2,sFlat2)),
inference(step,[status(thm)],[t2484,t2482]) ).
cnf(t2508,plain,
f(f(sFlat0,sFlat2),f(sFlat2,sFlat2)) = sFlat2,
inference(orient,[status(thm)],[t58939]) ).
cnf(t2818,plain,
f(f(X1,sFlat2),f(sFlat2,sFlat0)) = f(f(X1,sFlat2),f(f(f(X1,sFlat2),sFlat1),sFlat2)),
inference(cp,[status(thm)],[t1132,t2817]) ).
cnf(t59079,plain,
f(f(X1,sFlat2),sFlat1) = f(f(X1,sFlat2),f(f(f(X1,sFlat2),sFlat1),sFlat2)),
inference(step,[status(thm)],[t2818,t2817]) ).
cnf(t8882,plain,
f(f(X1,sFlat2),f(f(f(X1,sFlat2),sFlat1),sFlat2)) = f(f(X1,sFlat2),sFlat1),
inference(orient,[status(thm)],[t59079]) ).
cnf(t8886,plain,
f(f(sFlat0,sFlat2),sFlat1) = f(f(sFlat0,sFlat2),f(sFlat0,sFlat2)),
inference(cp,[status(thm)],[t8882,t3098]) ).
cnf(t59080,plain,
sFlat0 = f(f(sFlat0,sFlat2),f(sFlat0,sFlat2)),
inference(step,[status(thm)],[t8886,t3098]) ).
cnf(t8918,plain,
f(f(sFlat0,sFlat2),f(sFlat0,sFlat2)) = sFlat0,
inference(orient,[status(thm)],[t59080]) ).
cnf(t8919,plain,
f(sFlat0,sFlat2) = f(f(f(sFlat0,sFlat2),f(sFlat0,sFlat2)),sFlat0),
inference(cp,[status(thm)],[t2387,t8918]) ).
cnf(t59081,plain,
f(sFlat0,sFlat2) = f(sFlat0,sFlat0),
inference(step,[status(thm)],[t8919,t8918]) ).
cnf(t59082,plain,
f(sFlat0,sFlat2) = sFlat1,
inference(step,[status(thm)],[t59081,t35]) ).
cnf(t8963,plain,
f(sFlat0,sFlat2) = sFlat1,
inference(orient,[status(thm)],[t59082]) ).
cnf(t59083,plain,
f(sFlat1,f(sFlat2,sFlat2)) = sFlat2,
inference(step,[status(thm)],[t2508,t8963]) ).
cnf(t8988,plain,
f(sFlat1,f(sFlat2,sFlat2)) = sFlat2,
inference(rw,[status(thm)],[t59083]) ).
cnf(t8991,plain,
f(sFlat1,f(sFlat2,sFlat2)) = sFlat2,
inference(orient,[status(thm)],[t8988]) ).
cnf(t8993,plain,
x2 = f(sFlat2,f(x2,x2)),
inference(cp,[status(thm)],[t5742,t8991]) ).
cnf(t9064,plain,
f(sFlat2,f(x2,x2)) = x2,
inference(orient,[status(thm)],[t8993]) ).
cnf(t12440,plain,
sFlat2 = f(f(f(f(X1,sFlat2),x2),sFlat2),f(sFlat2,sFlat2)),
inference(cp,[status(thm)],[t12271,t9064]) ).
cnf(t12703,plain,
f(f(f(f(X1,sFlat2),x2),sFlat2),f(sFlat2,sFlat2)) = sFlat2,
inference(orient,[status(thm)],[t12440]) ).
cnf(t24702,plain,
f(X1,X2) = f(f(f(X1,X2),f(X1,X2)),X1),
inference(cp,[status(thm)],[t24617,t22306]) ).
cnf(t41052,plain,
f(f(f(X1,X2),f(X1,X2)),X1) = f(X1,X2),
inference(orient,[status(thm)],[t24702]) ).
cnf(t23369,plain,
f(f(sFlat3,sFlat2),f(sFlat3,sFlat2)) = f(x1,f(sFlat3,sFlat2)),
inference(cp,[status(thm)],[t23356,t14114]) ).
cnf(t9065,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,t9064]) ).
cnf(t59109,plain,
f(f(X1,sFlat2),x2) = f(f(X1,sFlat2),f(f(f(X1,sFlat2),x2),sFlat2)),
inference(step,[status(thm)],[t9065,t9064]) ).
cnf(t11191,plain,
f(f(X1,sFlat2),f(f(f(X1,sFlat2),x2),sFlat2)) = f(f(X1,sFlat2),x2),
inference(orient,[status(thm)],[t59109]) ).
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(t59078,plain,
f(f(X1,x1),sFlat2) = f(f(X1,x1),f(f(f(X1,x1),sFlat2),x1)),
inference(step,[status(thm)],[t1304,t44]) ).
cnf(t8850,plain,
f(f(X1,x1),f(f(f(X1,x1),sFlat2),x1)) = f(f(X1,x1),sFlat2),
inference(orient,[status(thm)],[t59078]) ).
cnf(t23018,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)],[t8850,t23009]) ).
cnf(t59244,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)],[t23018,t23009]) ).
cnf(t59245,plain,
f(f(x1,x1),sFlat2) = f(f(x1,x1),f(f(f(x1,x1),sFlat2),x1)),
inference(step,[status(thm)],[t59244,t23009]) ).
cnf(t59246,plain,
f(f(x1,x1),sFlat2) = f(f(x1,x1),f(x1,x1)),
inference(step,[status(thm)],[t59245,t23009]) ).
cnf(t59247,plain,
f(f(x1,x1),sFlat2) = x1,
inference(step,[status(thm)],[t59246,t18630]) ).
cnf(t23122,plain,
f(f(x1,x1),sFlat2) = x1,
inference(orient,[status(thm)],[t59247]) ).
cnf(t23125,plain,
f(f(f(x1,x1),sFlat2),x2) = f(x1,f(f(f(f(x1,x1),sFlat2),x2),sFlat2)),
inference(cp,[status(thm)],[t11191,t23122]) ).
cnf(t59252,plain,
f(x1,x2) = f(x1,f(f(f(f(x1,x1),sFlat2),x2),sFlat2)),
inference(step,[status(thm)],[t23125,t23122]) ).
cnf(t59253,plain,
sFlat3 = f(x1,f(f(f(f(x1,x1),sFlat2),x2),sFlat2)),
inference(step,[status(thm)],[t59252,t31]) ).
cnf(t59254,plain,
sFlat3 = f(x1,f(f(x1,x2),sFlat2)),
inference(step,[status(thm)],[t59253,t23122]) ).
cnf(t59255,plain,
sFlat3 = f(x1,f(sFlat3,sFlat2)),
inference(step,[status(thm)],[t59254,t31]) ).
cnf(t23204,plain,
f(x1,f(sFlat3,sFlat2)) = sFlat3,
inference(orient,[status(thm)],[t59255]) ).
cnf(t59308,plain,
f(f(sFlat3,sFlat2),f(sFlat3,sFlat2)) = sFlat3,
inference(step,[status(thm)],[t23369,t23204]) ).
cnf(t24132,plain,
f(f(sFlat3,sFlat2),f(sFlat3,sFlat2)) = sFlat3,
inference(orient,[status(thm)],[t59308]) ).
cnf(t24141,plain,
f(sFlat3,sFlat2) = f(sFlat3,sFlat3),
inference(cp,[status(thm)],[t2607,t24132]) ).
cnf(t59309,plain,
f(sFlat3,sFlat2) = sFlat4,
inference(step,[status(thm)],[t24141,t40]) ).
cnf(t24199,plain,
f(sFlat3,sFlat2) = sFlat4,
inference(orient,[status(thm)],[t59309]) ).
cnf(t24200,plain,
sFlat2 = f(sFlat4,f(sFlat2,sFlat2)),
inference(cp,[status(thm)],[t13157,t24199]) ).
cnf(t24239,plain,
f(sFlat4,f(sFlat2,sFlat2)) = sFlat2,
inference(orient,[status(thm)],[t24200]) ).
cnf(t24244,plain,
sFlat4 = f(f(f(sFlat5,sFlat2),X1),sFlat3),
inference(cp,[status(thm)],[t3187,t24239]) ).
cnf(t25096,plain,
f(f(f(sFlat5,sFlat2),X1),sFlat3) = sFlat4,
inference(orient,[status(thm)],[t24244]) ).
cnf(t25099,plain,
f(f(sFlat5,sFlat2),f(sFlat5,sFlat2)) = f(sFlat4,f(sFlat5,sFlat2)),
inference(cp,[status(thm)],[t23356,t25096]) ).
cnf(t27144,plain,
f(f(sFlat5,sFlat2),f(sFlat5,sFlat2)) = f(sFlat4,f(sFlat5,sFlat2)),
inference(orient,[status(thm)],[t25099]) ).
cnf(t2848,plain,
sFlat1 = f(f(f(f(X1,sFlat1),f(sFlat1,sFlat0)),X2),f(sFlat1,sFlat1)),
inference(cp,[status(thm)],[t7,t2836]) ).
cnf(t59066,plain,
sFlat1 = f(f(f(f(X1,sFlat1),f(sFlat1,sFlat0)),X2),sFlat0),
inference(step,[status(thm)],[t2848,t1461]) ).
cnf(t7679,plain,
f(f(f(f(X1,sFlat1),f(sFlat1,sFlat0)),X2),sFlat0) = sFlat1,
inference(orient,[status(thm)],[t59066]) ).
cnf(t7680,plain,
sFlat1 = f(f(f(f(X1,sFlat1),f(sFlat1,X2)),X3),sFlat0),
inference(cp,[status(thm)],[t7679,t6493]) ).
cnf(t8449,plain,
f(f(f(f(X1,sFlat1),f(sFlat1,X2)),X3),sFlat0) = sFlat1,
inference(orient,[status(thm)],[t7680]) ).
cnf(t8995,plain,
sFlat1 = f(f(f(f(X1,sFlat1),sFlat2),X2),sFlat0),
inference(cp,[status(thm)],[t8449,t8991]) ).
cnf(t9211,plain,
f(f(f(f(X1,sFlat1),sFlat2),X2),sFlat0) = sFlat1,
inference(orient,[status(thm)],[t8995]) ).
cnf(t24707,plain,
sFlat5 = f(f(sFlat5,sFlat5),sFlat1),
inference(cp,[status(thm)],[t24617,t24477]) ).
cnf(t24830,plain,
f(f(sFlat5,sFlat5),sFlat1) = sFlat5,
inference(orient,[status(thm)],[t24707]) ).
cnf(t24834,plain,
sFlat1 = f(f(f(sFlat5,sFlat2),X1),sFlat0),
inference(cp,[status(thm)],[t9211,t24830]) ).
cnf(t25265,plain,
f(f(f(sFlat5,sFlat2),X1),sFlat0) = sFlat1,
inference(orient,[status(thm)],[t24834]) ).
cnf(t25268,plain,
f(f(sFlat5,sFlat2),f(sFlat5,sFlat2)) = f(sFlat1,f(sFlat5,sFlat2)),
inference(cp,[status(thm)],[t23356,t25265]) ).
cnf(t59369,plain,
f(sFlat4,f(sFlat5,sFlat2)) = f(sFlat1,f(sFlat5,sFlat2)),
inference(step,[status(thm)],[t25268,t27144]) ).
cnf(t27436,plain,
f(sFlat4,f(sFlat5,sFlat2)) = f(sFlat1,f(sFlat5,sFlat2)),
inference(orient,[status(thm)],[t59369]) ).
cnf(t59370,plain,
f(f(sFlat5,sFlat2),f(sFlat5,sFlat2)) = f(sFlat1,f(sFlat5,sFlat2)),
inference(step,[status(thm)],[t27144,t27436]) ).
cnf(t27437,plain,
f(f(sFlat5,sFlat2),f(sFlat5,sFlat2)) = f(sFlat1,f(sFlat5,sFlat2)),
inference(orient,[status(thm)],[t59370]) ).
cnf(t41055,plain,
f(sFlat5,sFlat2) = f(f(sFlat1,f(sFlat5,sFlat2)),sFlat5),
inference(cp,[status(thm)],[t41052,t27437]) ).
cnf(t43873,plain,
f(f(sFlat1,f(sFlat5,sFlat2)),sFlat5) = f(sFlat5,sFlat2),
inference(orient,[status(thm)],[t41055]) ).
cnf(t59085,plain,
f(f(f(sFlat1,f(sFlat2,sFlat1)),X1),f(sFlat2,f(sFlat1,sFlat0))) = sFlat2,
inference(step,[status(thm)],[t986,t8963]) ).
cnf(t8990,plain,
f(f(f(sFlat1,f(sFlat2,sFlat1)),X1),f(sFlat2,f(sFlat1,sFlat0))) = sFlat2,
inference(rw,[status(thm)],[t59085]) ).
cnf(t20685,plain,
f(f(f(sFlat1,f(sFlat2,sFlat1)),X1),f(sFlat2,f(sFlat1,sFlat0))) = sFlat2,
inference(orient,[status(thm)],[t8990]) ).
cnf(t2639,plain,
f(f(f(f(X1,x0),sFlat0),X2),f(x0,f(f(x0,f(f(X1,X1),X1)),x2))) = f(f(f(f(X1,x0),sFlat0),X2),f(x0,f(f(f(f(X1,x0),sFlat0),X2),f(x0,f(f(x0,f(f(X1,X1),X1)),x2))))),
inference(cp,[status(thm)],[t2607,t157]) ).
cnf(t59062,plain,
x0 = f(f(f(f(X1,x0),sFlat0),X2),f(x0,f(f(f(f(X1,x0),sFlat0),X2),f(x0,f(f(x0,f(f(X1,X1),X1)),x2))))),
inference(step,[status(thm)],[t2639,t157]) ).
cnf(t59063,plain,
x0 = f(f(f(f(X1,x0),sFlat0),X2),f(x0,x0)),
inference(step,[status(thm)],[t59062,t157]) ).
cnf(t6278,plain,
f(f(f(f(X1,x0),sFlat0),X2),f(x0,x0)) = x0,
inference(orient,[status(thm)],[t59063]) ).
cnf(t6279,plain,
x0 = f(f(sFlat1,X1),f(x0,x0)),
inference(cp,[status(thm)],[t6278,t2836]) ).
cnf(t6327,plain,
f(f(sFlat1,X1),f(x0,x0)) = x0,
inference(orient,[status(thm)],[t6279]) ).
cnf(t20687,plain,
sFlat2 = f(x0,f(sFlat2,f(sFlat1,sFlat0))),
inference(cp,[status(thm)],[t20685,t6327]) ).
cnf(t20865,plain,
f(x0,f(sFlat2,f(sFlat1,sFlat0))) = sFlat2,
inference(orient,[status(thm)],[t20687]) ).
cnf(t20872,plain,
f(f(X1,x0),f(x0,f(sFlat2,f(sFlat1,sFlat0)))) = f(f(X1,x0),f(f(f(X1,x0),sFlat2),x0)),
inference(cp,[status(thm)],[t1132,t20865]) ).
cnf(t59208,plain,
f(f(X1,x0),sFlat2) = f(f(X1,x0),f(f(f(X1,x0),sFlat2),x0)),
inference(step,[status(thm)],[t20872,t20865]) ).
cnf(t21600,plain,
f(f(X1,x0),f(f(f(X1,x0),sFlat2),x0)) = f(f(X1,x0),sFlat2),
inference(orient,[status(thm)],[t59208]) ).
cnf(t22535,plain,
f(f(f(f(x0,x0),X1),x0),sFlat2) = f(f(x0,x0),f(f(f(f(f(x0,x0),X1),x0),sFlat2),x0)),
inference(cp,[status(thm)],[t21600,t22534]) ).
cnf(t59220,plain,
f(f(x0,x0),sFlat2) = f(f(x0,x0),f(f(f(f(f(x0,x0),X1),x0),sFlat2),x0)),
inference(step,[status(thm)],[t22535,t22534]) ).
cnf(t59221,plain,
f(f(x0,x0),sFlat2) = f(f(x0,x0),f(f(f(x0,x0),sFlat2),x0)),
inference(step,[status(thm)],[t59220,t22534]) ).
cnf(t59222,plain,
f(f(x0,x0),sFlat2) = f(f(x0,x0),f(x0,x0)),
inference(step,[status(thm)],[t59221,t22534]) ).
cnf(t59223,plain,
f(f(x0,x0),sFlat2) = x0,
inference(step,[status(thm)],[t59222,t19771]) ).
cnf(t22609,plain,
f(f(x0,x0),sFlat2) = x0,
inference(orient,[status(thm)],[t59223]) ).
cnf(t22614,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,t22609]) ).
cnf(t59814,plain,
f(x0,f(sFlat2,X1)) = f(x0,f(f(f(f(x0,x0),sFlat2),f(sFlat2,X1)),sFlat2)),
inference(step,[status(thm)],[t22614,t22609]) ).
cnf(t59815,plain,
f(x0,f(sFlat2,X1)) = f(x0,f(f(x0,f(sFlat2,X1)),sFlat2)),
inference(step,[status(thm)],[t59814,t22609]) ).
cnf(t55350,plain,
f(x0,f(f(x0,f(sFlat2,X1)),sFlat2)) = f(x0,f(sFlat2,X1)),
inference(orient,[status(thm)],[t59815]) ).
cnf(t24240,plain,
sFlat4 = f(sFlat2,f(sFlat4,sFlat4)),
inference(cp,[status(thm)],[t22306,t24239]) ).
cnf(t59310,plain,
sFlat4 = f(sFlat2,sFlat3),
inference(step,[status(thm)],[t24240,t1378]) ).
cnf(t24292,plain,
f(sFlat2,sFlat3) = sFlat4,
inference(orient,[status(thm)],[t59310]) ).
cnf(t55355,plain,
f(x0,f(sFlat2,sFlat3)) = f(x0,f(f(x0,sFlat4),sFlat2)),
inference(cp,[status(thm)],[t55350,t24292]) ).
cnf(t59816,plain,
f(x0,sFlat4) = f(x0,f(f(x0,sFlat4),sFlat2)),
inference(step,[status(thm)],[t55355,t24292]) ).
cnf(t59817,plain,
sFlat5 = f(x0,f(f(x0,sFlat4),sFlat2)),
inference(step,[status(thm)],[t59816,t21]) ).
cnf(t59818,plain,
sFlat5 = f(x0,f(sFlat5,sFlat2)),
inference(step,[status(thm)],[t59817,t21]) ).
cnf(t7610,plain,
x0 = f(f(f(f(X1,x0),f(x0,X2)),X3),f(x0,x0)),
inference(cp,[status(thm)],[t6278,t6493]) ).
cnf(t20193,plain,
f(f(f(f(X1,x0),f(x0,X2)),X3),f(x0,x0)) = x0,
inference(orient,[status(thm)],[t7610]) ).
cnf(t20868,plain,
x0 = f(f(f(f(X1,x0),sFlat2),X2),f(x0,x0)),
inference(cp,[status(thm)],[t20193,t20865]) ).
cnf(t21381,plain,
f(f(f(f(X1,x0),sFlat2),X2),f(x0,x0)) = x0,
inference(orient,[status(thm)],[t20868]) ).
cnf(t15022,plain,
x0 = f(sFlat5,f(x0,x0)),
inference(cp,[status(thm)],[t6231,t14946]) ).
cnf(t15090,plain,
f(sFlat5,f(x0,x0)) = x0,
inference(orient,[status(thm)],[t15022]) ).
cnf(t15097,plain,
f(f(X1,sFlat5),f(sFlat5,f(x0,x0))) = f(f(X1,sFlat5),f(f(f(X1,sFlat5),x0),sFlat5)),
inference(cp,[status(thm)],[t1132,t15090]) ).
cnf(t59147,plain,
f(f(X1,sFlat5),x0) = f(f(X1,sFlat5),f(f(f(X1,sFlat5),x0),sFlat5)),
inference(step,[status(thm)],[t15097,t15090]) ).
cnf(t16711,plain,
f(f(X1,sFlat5),f(f(f(X1,sFlat5),x0),sFlat5)) = f(f(X1,sFlat5),x0),
inference(orient,[status(thm)],[t59147]) ).
cnf(t23435,plain,
f(f(f(f(sFlat5,sFlat5),X1),sFlat5),x0) = f(f(sFlat5,sFlat5),f(f(f(f(f(sFlat5,sFlat5),X1),sFlat5),x0),sFlat5)),
inference(cp,[status(thm)],[t16711,t23356]) ).
cnf(t59268,plain,
f(f(sFlat5,sFlat5),x0) = f(f(sFlat5,sFlat5),f(f(f(f(f(sFlat5,sFlat5),X1),sFlat5),x0),sFlat5)),
inference(step,[status(thm)],[t23435,t23356]) ).
cnf(t59269,plain,
f(f(sFlat5,sFlat5),x0) = f(f(sFlat5,sFlat5),f(f(f(sFlat5,sFlat5),x0),sFlat5)),
inference(step,[status(thm)],[t59268,t23356]) ).
cnf(t59270,plain,
f(f(sFlat5,sFlat5),x0) = f(f(sFlat5,sFlat5),f(sFlat5,sFlat5)),
inference(step,[status(thm)],[t59269,t23356]) ).
cnf(t59271,plain,
f(f(sFlat5,sFlat5),x0) = sFlat5,
inference(step,[status(thm)],[t59270,t22306]) ).
cnf(t23676,plain,
f(f(sFlat5,sFlat5),x0) = sFlat5,
inference(orient,[status(thm)],[t59271]) ).
cnf(t23679,plain,
x0 = f(f(f(sFlat5,sFlat2),X1),f(x0,x0)),
inference(cp,[status(thm)],[t21381,t23676]) ).
cnf(t29184,plain,
f(f(f(sFlat5,sFlat2),X1),f(x0,x0)) = x0,
inference(orient,[status(thm)],[t23679]) ).
cnf(t29187,plain,
f(f(sFlat5,sFlat2),f(sFlat5,sFlat2)) = f(x0,f(sFlat5,sFlat2)),
inference(cp,[status(thm)],[t23356,t29184]) ).
cnf(t59389,plain,
f(sFlat1,f(sFlat5,sFlat2)) = f(x0,f(sFlat5,sFlat2)),
inference(step,[status(thm)],[t29187,t27437]) ).
cnf(t29257,plain,
f(x0,f(sFlat5,sFlat2)) = f(sFlat1,f(sFlat5,sFlat2)),
inference(orient,[status(thm)],[t59389]) ).
cnf(t59819,plain,
sFlat5 = f(sFlat1,f(sFlat5,sFlat2)),
inference(step,[status(thm)],[t59818,t29257]) ).
cnf(t55393,plain,
f(sFlat1,f(sFlat5,sFlat2)) = sFlat5,
inference(orient,[status(thm)],[t59819]) ).
cnf(t59836,plain,
f(sFlat5,sFlat5) = f(sFlat5,sFlat2),
inference(step,[status(thm)],[t43873,t55393]) ).
cnf(t55444,plain,
f(sFlat5,sFlat5) = f(sFlat5,sFlat2),
inference(rw,[status(thm)],[t59836]) ).
cnf(t55446,plain,
f(sFlat5,sFlat5) = f(sFlat5,sFlat2),
inference(orient,[status(thm)],[t55444]) ).
cnf(t55461,plain,
f(f(sFlat5,sFlat5),x2) = f(f(sFlat5,sFlat2),f(f(f(sFlat5,sFlat5),x2),sFlat5)),
inference(cp,[status(thm)],[t11267,t55446]) ).
cnf(t59873,plain,
f(f(sFlat5,sFlat2),x2) = f(f(sFlat5,sFlat2),f(f(f(sFlat5,sFlat5),x2),sFlat5)),
inference(step,[status(thm)],[t55461,t55446]) ).
cnf(t59874,plain,
f(f(sFlat5,sFlat2),x2) = f(f(sFlat5,sFlat2),f(sFlat5,sFlat5)),
inference(step,[status(thm)],[t59873,t23356]) ).
cnf(t59875,plain,
f(f(sFlat5,sFlat2),x2) = f(f(sFlat5,sFlat2),f(sFlat5,sFlat2)),
inference(step,[status(thm)],[t59874,t55446]) ).
cnf(t59820,plain,
f(f(sFlat5,sFlat2),f(sFlat5,sFlat2)) = sFlat5,
inference(step,[status(thm)],[t27437,t55393]) ).
cnf(t55394,plain,
f(f(sFlat5,sFlat2),f(sFlat5,sFlat2)) = sFlat5,
inference(orient,[status(thm)],[t59820]) ).
cnf(t59876,plain,
f(f(sFlat5,sFlat2),x2) = sFlat5,
inference(step,[status(thm)],[t59875,t55394]) ).
cnf(t55554,plain,
f(f(sFlat5,sFlat2),x2) = sFlat5,
inference(orient,[status(thm)],[t59876]) ).
cnf(t55555,plain,
sFlat2 = f(f(sFlat5,sFlat2),f(sFlat2,sFlat2)),
inference(cp,[status(thm)],[t12703,t55554]) ).
cnf(t56406,plain,
f(f(sFlat5,sFlat2),f(sFlat2,sFlat2)) = sFlat2,
inference(orient,[status(thm)],[t55555]) ).
cnf(t56407,plain,
f(sFlat5,sFlat2) = f(sFlat2,f(f(sFlat5,sFlat2),f(sFlat5,sFlat2))),
inference(cp,[status(thm)],[t22306,t56406]) ).
cnf(t59877,plain,
f(sFlat5,sFlat2) = f(sFlat2,sFlat5),
inference(step,[status(thm)],[t56407,t55394]) ).
cnf(t56456,plain,
f(sFlat5,sFlat2) = f(sFlat2,sFlat5),
inference(orient,[status(thm)],[t59877]) ).
cnf(t56459,plain,
sFlat5 = f(f(sFlat5,sFlat5),f(sFlat2,sFlat5)),
inference(cp,[status(thm)],[t24617,t56456]) ).
cnf(t59878,plain,
f(sFlat5,sFlat5) = f(sFlat2,sFlat5),
inference(step,[status(thm)],[t55446,t56456]) ).
cnf(t56457,plain,
f(sFlat5,sFlat5) = f(sFlat2,sFlat5),
inference(orient,[status(thm)],[t59878]) ).
cnf(t59911,plain,
sFlat5 = f(f(sFlat2,sFlat5),f(sFlat2,sFlat5)),
inference(step,[status(thm)],[t56459,t56457]) ).
cnf(t59912,plain,
sFlat5 = f(sFlat1,f(sFlat2,sFlat5)),
inference(step,[status(thm)],[t59911,t27290]) ).
cnf(t56532,plain,
f(sFlat1,f(sFlat2,sFlat5)) = sFlat5,
inference(orient,[status(thm)],[t59912]) ).
cnf(t59921,plain,
f(x1,f(sFlat2,sFlat5)) = sFlat5,
inference(step,[status(thm)],[t29438,t56532]) ).
cnf(t56541,plain,
f(x1,f(sFlat2,sFlat5)) = sFlat5,
inference(orient,[status(thm)],[t59921]) ).
cnf(t59967,plain,
sFlat2 = sFlat5,
inference(step,[status(thm)],[t59966,t56541]) ).
cnf(t58857,plain,
sFlat5 = sFlat2,
inference(orient,[status(thm)],[t59967]) ).
cnf(t59968,plain,
f(x0,sFlat4) = sFlat2,
inference(step,[status(thm)],[t21,t58857]) ).
cnf(t58858,plain,
f(x0,sFlat4) = sFlat2,
inference(orient,[status(thm)],[t59968]) ).
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,t58858]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_7]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LAT393-2 : TPTP v9.3.1. Released v5.4.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n010.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Wed Sep 23 21:32:44 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 46.03/6.36 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 46.03/6.36 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------