%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LAT072-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 01:55:09 PM UTC 2026
% Result : Unsatisfiable 109.68s 21.27s
% Output : CNFRefutation 109.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 80
% Number of leaves : 8
% Syntax : Number of clauses : 467 ( 467 unt; 0 nHn; 158 RR)
% Number of literals : 467 ( 466 equ; 9 neg)
% Maximal clause size : 1 ( 1 avg)
% Maximal term depth : 13 ( 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 : 528 ( 329 sgn)
% Comments :
%------------------------------------------------------------------------------
cnf(t1,axiom,
sFlat0 = f(b,a),
introduced(definition) ).
cnf(t21,plain,
f(b,a) = sFlat0,
inference(orient,[status(thm)],[t1]) ).
cnf(t2,axiom,
sFlat1 = f(f(b,a),f(b,a)),
introduced(definition) ).
cnf(t13,plain,
f(f(b,a),f(b,a)) = sFlat1,
inference(orient,[status(thm)],[t2]) ).
cnf(t149726,plain,
f(sFlat0,f(b,a)) = sFlat1,
inference(step,[status(thm)],[t13,t21]) ).
cnf(t149727,plain,
f(sFlat0,sFlat0) = sFlat1,
inference(step,[status(thm)],[t149726,t21]) ).
cnf(t24,plain,
f(sFlat0,sFlat0) = sFlat1,
inference(rw,[status(thm)],[t149727]) ).
cnf(t35,plain,
f(sFlat0,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t24]) ).
cnf(t3,axiom,
sFlat2 = f(c,f(f(b,a),f(b,a))),
introduced(definition) ).
cnf(t149732,plain,
sFlat2 = f(c,f(sFlat0,f(b,a))),
inference(step,[status(thm)],[t3,t21]) ).
cnf(t149733,plain,
sFlat2 = f(c,f(sFlat0,sFlat0)),
inference(step,[status(thm)],[t149732,t21]) ).
cnf(t32,plain,
f(c,f(sFlat0,sFlat0)) = sFlat2,
inference(orient,[status(thm)],[t149733]) ).
cnf(t149734,plain,
f(c,sFlat1) = sFlat2,
inference(step,[status(thm)],[t32,t35]) ).
cnf(t39,plain,
f(c,sFlat1) = sFlat2,
inference(rw,[status(thm)],[t149734]) ).
cnf(t45,plain,
f(c,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t39]) ).
cnf(t4,axiom,
sFlat3 = f(b,c),
introduced(definition) ).
cnf(t25,plain,
f(b,c) = sFlat3,
inference(orient,[status(thm)],[t4]) ).
cnf(t5,axiom,
sFlat4 = f(f(b,c),f(b,c)),
introduced(definition) ).
cnf(t17,plain,
f(f(b,c),f(b,c)) = sFlat4,
inference(orient,[status(thm)],[t5]) ).
cnf(t149728,plain,
f(sFlat3,f(b,c)) = sFlat4,
inference(step,[status(thm)],[t17,t25]) ).
cnf(t149729,plain,
f(sFlat3,sFlat3) = sFlat4,
inference(step,[status(thm)],[t149728,t25]) ).
cnf(t28,plain,
f(sFlat3,sFlat3) = sFlat4,
inference(rw,[status(thm)],[t149729]) ).
cnf(t40,plain,
f(sFlat3,sFlat3) = sFlat4,
inference(orient,[status(thm)],[t28]) ).
cnf(t6,axiom,
sFlat5 = f(a,f(f(b,c),f(b,c))),
introduced(definition) ).
cnf(t149730,plain,
sFlat5 = f(a,f(sFlat3,f(b,c))),
inference(step,[status(thm)],[t6,t25]) ).
cnf(t149731,plain,
sFlat5 = f(a,f(sFlat3,sFlat3)),
inference(step,[status(thm)],[t149730,t25]) ).
cnf(t29,plain,
f(a,f(sFlat3,sFlat3)) = sFlat5,
inference(orient,[status(thm)],[t149731]) ).
cnf(t149735,plain,
f(a,sFlat4) = sFlat5,
inference(step,[status(thm)],[t29,t40]) ).
cnf(t44,plain,
f(a,sFlat4) = sFlat5,
inference(rw,[status(thm)],[t149735]) ).
cnf(t48,plain,
f(a,sFlat4) = sFlat5,
inference(orient,[status(thm)],[t44]) ).
cnf(t0,axiom,
f(f(f(f(X1,X2),f(X2,X3)),X4),f(X2,f(f(X3,f(f(X2,X2),X3)),X3))) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(t7,plain,
f(f(f(f(X1,X2),f(X2,X3)),X4),f(X2,f(f(X3,f(f(X2,X2),X3)),X3))) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t8,plain,
f(X1,X2) = f(X1,f(f(X1,X2),f(f(X3,f(f(f(X1,X2),f(X1,X2)),X3)),X3))),
inference(cp,[status(thm)],[t7,t7]) ).
cnf(t201,plain,
f(X1,f(f(X1,X2),f(f(X3,f(f(f(X1,X2),f(X1,X2)),X3)),X3))) = f(X1,X2),
inference(orient,[status(thm)],[t8]) ).
cnf(t316,plain,
f(X1,X2) = f(X1,f(f(X1,X2),f(f(f(f(f(f(X1,X2),f(X1,X2)),X3),f(f(X4,f(f(f(f(f(X1,X2),f(X1,X2)),X3),f(f(f(X1,X2),f(X1,X2)),X3)),X4)),X4)),f(f(f(X1,X2),f(X1,X2)),X3)),f(f(f(f(X1,X2),f(X1,X2)),X3),f(f(X4,f(f(f(f(f(X1,X2),f(X1,X2)),X3),f(f(f(X1,X2),f(X1,X2)),X3)),X4)),X4))))),
inference(cp,[status(thm)],[t201,t201]) ).
cnf(t9,plain,
X1 = f(f(X1,X2),f(X1,f(f(f(f(X3,f(f(X1,X1),X3)),X3),f(f(X1,X1),f(f(X3,f(f(X1,X1),X3)),X3))),f(f(X3,f(f(X1,X1),X3)),X3)))),
inference(cp,[status(thm)],[t7,t7]) ).
cnf(t546,plain,
f(f(X1,X2),f(X1,f(f(f(f(X3,f(f(X1,X1),X3)),X3),f(f(X1,X1),f(f(X3,f(f(X1,X1),X3)),X3))),f(f(X3,f(f(X1,X1),X3)),X3)))) = X1,
inference(orient,[status(thm)],[t9]) ).
cnf(t661,plain,
X1 = f(f(X2,X1),f(X1,f(f(X3,f(f(X1,X1),X3)),X3))),
inference(cp,[status(thm)],[t7,t546]) ).
cnf(t1102,plain,
f(f(X1,X2),f(X2,f(f(X3,f(f(X2,X2),X3)),X3))) = X2,
inference(orient,[status(thm)],[t661]) ).
cnf(t150610,plain,
f(X1,X2) = f(X1,f(f(X1,X2),f(f(f(X1,X2),f(X1,X2)),X3))),
inference(step,[status(thm)],[t316,t1102]) ).
cnf(t80351,plain,
f(X1,f(f(X1,X2),f(f(f(X1,X2),f(X1,X2)),X3))) = f(X1,X2),
inference(orient,[status(thm)],[t150610]) ).
cnf(t220,plain,
f(f(f(f(X1,X2),f(X2,X3)),X4),f(X2,f(f(X3,f(f(X2,X2),X3)),X3))) = f(f(f(f(X1,X2),f(X2,X3)),X4),f(X2,f(f(Y4,f(f(f(f(f(f(X1,X2),f(X2,X3)),X4),f(X2,f(f(X3,f(f(X2,X2),X3)),X3))),f(f(f(f(X1,X2),f(X2,X3)),X4),f(X2,f(f(X3,f(f(X2,X2),X3)),X3)))),Y4)),Y4))),
inference(cp,[status(thm)],[t201,t7]) ).
cnf(t150558,plain,
X2 = f(f(f(f(X1,X2),f(X2,X3)),X4),f(X2,f(f(Y4,f(f(f(f(f(f(X1,X2),f(X2,X3)),X4),f(X2,f(f(X3,f(f(X2,X2),X3)),X3))),f(f(f(f(X1,X2),f(X2,X3)),X4),f(X2,f(f(X3,f(f(X2,X2),X3)),X3)))),Y4)),Y4))),
inference(step,[status(thm)],[t220,t7]) ).
cnf(t150559,plain,
X2 = f(f(f(f(X1,X2),f(X2,X3)),X4),f(X2,f(f(Y4,f(f(X2,f(f(f(f(X1,X2),f(X2,X3)),X4),f(X2,f(f(X3,f(f(X2,X2),X3)),X3)))),Y4)),Y4))),
inference(step,[status(thm)],[t150558,t7]) ).
cnf(t150560,plain,
X2 = f(f(f(f(X1,X2),f(X2,X3)),X4),f(X2,f(f(Y4,f(f(X2,X2),Y4)),Y4))),
inference(step,[status(thm)],[t150559,t7]) ).
cnf(t73371,plain,
f(f(f(f(X1,X2),f(X2,X3)),X4),f(X2,f(f(Y4,f(f(X2,X2),Y4)),Y4))) = X2,
inference(orient,[status(thm)],[t150560]) ).
cnf(t1170,plain,
X1 = f(f(X2,X1),f(X1,f(f(X1,X1),f(f(f(X1,X1),f(f(f(X1,X1),f(X1,X1)),f(X1,X1))),f(X1,X1))))),
inference(cp,[status(thm)],[t1102,t1102]) ).
cnf(t149809,plain,
X1 = f(f(X2,X1),f(X1,X1)),
inference(step,[status(thm)],[t1170,t201]) ).
cnf(t1246,plain,
f(f(X1,X2),f(X2,X2)) = X2,
inference(orient,[status(thm)],[t149809]) ).
cnf(t1300,plain,
f(X1,X1) = f(f(X2,f(X1,X1)),X1),
inference(cp,[status(thm)],[t1246,t1246]) ).
cnf(t1362,plain,
f(f(X1,f(X2,X2)),X2) = f(X2,X2),
inference(orient,[status(thm)],[t1300]) ).
cnf(t75612,plain,
X1 = f(f(f(f(X2,X1),f(X1,X3)),X4),f(X1,f(f(X1,X1),f(X1,X1)))),
inference(cp,[status(thm)],[t73371,t1362]) ).
cnf(t1192,plain,
f(X1,X2) = f(X1,f(f(X1,X2),f(f(f(f(X1,X2),f(f(X3,f(f(f(X1,X2),f(X1,X2)),X3)),X3)),f(X1,X2)),f(f(X1,X2),f(f(X3,f(f(f(X1,X2),f(X1,X2)),X3)),X3))))),
inference(cp,[status(thm)],[t201,t1102]) ).
cnf(t149821,plain,
f(X1,X2) = f(X1,f(f(X1,X2),f(X1,X2))),
inference(step,[status(thm)],[t1192,t1102]) ).
cnf(t1687,plain,
f(X1,f(f(X1,X2),f(X1,X2))) = f(X1,X2),
inference(orient,[status(thm)],[t149821]) ).
cnf(t1164,plain,
X1 = f(f(X1,X2),f(X1,f(f(X2,f(f(X1,X1),X2)),X2))),
inference(cp,[status(thm)],[t7,t1102]) ).
cnf(t11046,plain,
f(f(X1,X2),f(X1,f(f(X2,f(f(X1,X1),X2)),X2))) = X1,
inference(orient,[status(thm)],[t1164]) ).
cnf(t11220,plain,
f(f(X1,X2),f(X1,f(f(X2,f(f(X1,X1),X2)),X2))) = f(f(X1,X2),f(X1,f(f(X1,X2),f(X1,f(f(X2,f(f(X1,X1),X2)),X2))))),
inference(cp,[status(thm)],[t1687,t11046]) ).
cnf(t149979,plain,
X1 = f(f(X1,X2),f(X1,f(f(X1,X2),f(X1,f(f(X2,f(f(X1,X1),X2)),X2))))),
inference(step,[status(thm)],[t11220,t11046]) ).
cnf(t149980,plain,
X1 = f(f(X1,X2),f(X1,X1)),
inference(step,[status(thm)],[t149979,t11046]) ).
cnf(t11288,plain,
f(f(X1,X2),f(X1,X1)) = X1,
inference(orient,[status(thm)],[t149980]) ).
cnf(t11342,plain,
f(X1,X2) = f(X2,f(f(X1,X2),f(X1,X2))),
inference(cp,[status(thm)],[t11288,t1102]) ).
cnf(t15706,plain,
f(X1,f(f(X2,X1),f(X2,X1))) = f(X2,X1),
inference(orient,[status(thm)],[t11342]) ).
cnf(t150567,plain,
X1 = f(f(f(f(X2,X1),f(X1,X3)),X4),f(X1,X1)),
inference(step,[status(thm)],[t75612,t15706]) ).
cnf(t76576,plain,
f(f(f(f(X1,X2),f(X2,X3)),X4),f(X2,X2)) = X2,
inference(orient,[status(thm)],[t150567]) ).
cnf(t1750,plain,
X1 = f(f(X2,X1),f(X1,f(f(f(f(f(X1,X1),X3),f(f(X1,X1),X3)),f(f(X1,X1),X3)),f(f(f(X1,X1),X3),f(f(X1,X1),X3))))),
inference(cp,[status(thm)],[t1102,t1687]) ).
cnf(t149908,plain,
X1 = f(f(X2,X1),f(X1,f(f(X1,X1),X3))),
inference(step,[status(thm)],[t1750,t1246]) ).
cnf(t4680,plain,
f(f(X1,X2),f(X2,f(f(X2,X2),X3))) = X2,
inference(orient,[status(thm)],[t149908]) ).
cnf(t4805,plain,
f(X1,X1) = f(f(X2,f(X1,X1)),f(f(X1,X1),f(X1,X3))),
inference(cp,[status(thm)],[t4680,t1246]) ).
cnf(t10071,plain,
f(f(X1,f(X2,X2)),f(f(X2,X2),f(X2,X3))) = f(X2,X2),
inference(orient,[status(thm)],[t4805]) ).
cnf(t23,plain,
b = f(f(f(f(X1,b),sFlat0),X2),f(b,f(f(a,f(f(b,b),a)),a))),
inference(cp,[status(thm)],[t7,t21]) ).
cnf(t112,plain,
f(f(f(f(X1,b),sFlat0),X2),f(b,f(f(a,f(f(b,b),a)),a))) = b,
inference(orient,[status(thm)],[t23]) ).
cnf(t1699,plain,
f(f(f(f(X1,b),sFlat0),X2),f(b,f(f(a,f(f(b,b),a)),a))) = f(f(f(f(X1,b),sFlat0),X2),f(b,f(f(f(f(X1,b),sFlat0),X2),f(b,f(f(a,f(f(b,b),a)),a))))),
inference(cp,[status(thm)],[t1687,t112]) ).
cnf(t149898,plain,
b = f(f(f(f(X1,b),sFlat0),X2),f(b,f(f(f(f(X1,b),sFlat0),X2),f(b,f(f(a,f(f(b,b),a)),a))))),
inference(step,[status(thm)],[t1699,t112]) ).
cnf(t149899,plain,
b = f(f(f(f(X1,b),sFlat0),X2),f(b,b)),
inference(step,[status(thm)],[t149898,t112]) ).
cnf(t4266,plain,
f(f(f(f(X1,b),sFlat0),X2),f(b,b)) = b,
inference(orient,[status(thm)],[t149899]) ).
cnf(t38,plain,
sFlat0 = f(f(f(f(X1,sFlat0),f(sFlat0,X2)),X3),f(sFlat0,f(f(X2,f(sFlat1,X2)),X2))),
inference(cp,[status(thm)],[t7,t35]) ).
cnf(t155,plain,
f(f(f(f(X1,sFlat0),f(sFlat0,X2)),X3),f(sFlat0,f(f(X2,f(sFlat1,X2)),X2))) = sFlat0,
inference(orient,[status(thm)],[t38]) ).
cnf(t654,plain,
sFlat0 = f(f(X1,sFlat0),f(sFlat0,f(f(X2,f(sFlat1,X2)),X2))),
inference(cp,[status(thm)],[t155,t546]) ).
cnf(t863,plain,
f(f(X1,sFlat0),f(sFlat0,f(f(X2,f(sFlat1,X2)),X2))) = sFlat0,
inference(orient,[status(thm)],[t654]) ).
cnf(t36,plain,
sFlat0 = f(f(f(sFlat1,f(sFlat0,X1)),X2),f(sFlat0,f(f(X1,f(f(sFlat0,sFlat0),X1)),X1))),
inference(cp,[status(thm)],[t7,t35]) ).
cnf(t149736,plain,
sFlat0 = f(f(f(sFlat1,f(sFlat0,X1)),X2),f(sFlat0,f(f(X1,f(sFlat1,X1)),X1))),
inference(step,[status(thm)],[t36,t35]) ).
cnf(t51,plain,
f(f(f(sFlat1,f(sFlat0,X1)),X2),f(sFlat0,f(f(X1,f(sFlat1,X1)),X1))) = sFlat0,
inference(orient,[status(thm)],[t149736]) ).
cnf(t651,plain,
sFlat0 = f(sFlat1,f(sFlat0,f(f(X1,f(sFlat1,X1)),X1))),
inference(cp,[status(thm)],[t51,t546]) ).
cnf(t696,plain,
f(sFlat1,f(sFlat0,f(f(X1,f(sFlat1,X1)),X1))) = sFlat0,
inference(orient,[status(thm)],[t651]) ).
cnf(t864,plain,
sFlat0 = f(f(X1,sFlat0),f(sFlat0,f(f(f(sFlat0,f(f(X2,f(sFlat1,X2)),X2)),sFlat0),f(sFlat0,f(f(X2,f(sFlat1,X2)),X2))))),
inference(cp,[status(thm)],[t863,t696]) ).
cnf(t149761,plain,
sFlat0 = f(f(X1,sFlat0),f(sFlat0,sFlat0)),
inference(step,[status(thm)],[t864,t863]) ).
cnf(t149762,plain,
sFlat0 = f(f(X1,sFlat0),sFlat1),
inference(step,[status(thm)],[t149761,t35]) ).
cnf(t879,plain,
f(f(X1,sFlat0),sFlat1) = sFlat0,
inference(orient,[status(thm)],[t149762]) ).
cnf(t880,plain,
sFlat0 = f(sFlat1,sFlat1),
inference(cp,[status(thm)],[t879,t35]) ).
cnf(t890,plain,
f(sFlat1,sFlat1) = sFlat0,
inference(orient,[status(thm)],[t880]) ).
cnf(t1298,plain,
sFlat1 = f(f(X1,sFlat1),sFlat0),
inference(cp,[status(thm)],[t1246,t890]) ).
cnf(t1342,plain,
f(f(X1,sFlat1),sFlat0) = sFlat1,
inference(orient,[status(thm)],[t1298]) ).
cnf(t1344,plain,
sFlat1 = f(f(f(f(X1,sFlat1),f(sFlat1,sFlat0)),X2),f(sFlat1,f(f(sFlat0,sFlat1),sFlat0))),
inference(cp,[status(thm)],[t7,t1342]) ).
cnf(t149862,plain,
sFlat1 = f(f(f(f(X1,sFlat1),f(sFlat1,sFlat0)),X2),f(sFlat1,sFlat1)),
inference(step,[status(thm)],[t1344,t1342]) ).
cnf(t149863,plain,
sFlat1 = f(f(f(f(X1,sFlat1),f(sFlat1,sFlat0)),X2),sFlat0),
inference(step,[status(thm)],[t149862,t890]) ).
cnf(t2173,plain,
f(f(f(f(X1,sFlat1),f(sFlat1,sFlat0)),X2),sFlat0) = sFlat1,
inference(orient,[status(thm)],[t149863]) ).
cnf(t2182,plain,
sFlat1 = f(f(f(sFlat2,f(sFlat1,sFlat0)),X1),sFlat0),
inference(cp,[status(thm)],[t2173,t45]) ).
cnf(t3640,plain,
f(f(f(sFlat2,f(sFlat1,sFlat0)),X1),sFlat0) = sFlat1,
inference(orient,[status(thm)],[t2182]) ).
cnf(t4268,plain,
b = f(f(sFlat1,X1),f(b,b)),
inference(cp,[status(thm)],[t4266,t3640]) ).
cnf(t4312,plain,
f(f(sFlat1,X1),f(b,b)) = b,
inference(orient,[status(thm)],[t4268]) ).
cnf(t1277,plain,
sFlat1 = f(sFlat2,f(sFlat1,sFlat1)),
inference(cp,[status(thm)],[t1246,t45]) ).
cnf(t149811,plain,
sFlat1 = f(sFlat2,sFlat0),
inference(step,[status(thm)],[t1277,t890]) ).
cnf(t1336,plain,
f(sFlat2,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t149811]) ).
cnf(t11339,plain,
sFlat2 = f(sFlat1,f(sFlat2,sFlat2)),
inference(cp,[status(thm)],[t11288,t1336]) ).
cnf(t11451,plain,
f(sFlat1,f(sFlat2,sFlat2)) = sFlat2,
inference(orient,[status(thm)],[t11339]) ).
cnf(t11454,plain,
b = f(sFlat2,f(b,b)),
inference(cp,[status(thm)],[t4312,t11451]) ).
cnf(t11569,plain,
f(sFlat2,f(b,b)) = b,
inference(orient,[status(thm)],[t11454]) ).
cnf(t11570,plain,
sFlat2 = f(b,f(sFlat2,sFlat2)),
inference(cp,[status(thm)],[t11288,t11569]) ).
cnf(t11681,plain,
f(b,f(sFlat2,sFlat2)) = sFlat2,
inference(orient,[status(thm)],[t11570]) ).
cnf(t11682,plain,
f(b,b) = f(f(X1,f(b,b)),f(f(b,b),sFlat2)),
inference(cp,[status(thm)],[t10071,t11681]) ).
cnf(t25621,plain,
f(f(X1,f(b,b)),f(f(b,b),sFlat2)) = f(b,b),
inference(orient,[status(thm)],[t11682]) ).
cnf(t11366,plain,
f(X1,X1) = f(f(f(X1,X1),X2),X1),
inference(cp,[status(thm)],[t11288,t1246]) ).
cnf(t11919,plain,
f(f(f(X1,X1),X2),X1) = f(X1,X1),
inference(orient,[status(thm)],[t11366]) ).
cnf(t25622,plain,
f(b,b) = f(f(f(b,b),sFlat2),f(f(b,b),sFlat2)),
inference(cp,[status(thm)],[t25621,t11919]) ).
cnf(t38725,plain,
f(f(f(b,b),sFlat2),f(f(b,b),sFlat2)) = f(b,b),
inference(orient,[status(thm)],[t25622]) ).
cnf(t38726,plain,
f(f(b,b),sFlat2) = f(f(f(f(b,b),sFlat2),X1),f(b,b)),
inference(cp,[status(thm)],[t11288,t38725]) ).
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(X2,f(f(X3,f(f(X2,X2),X3)),X3)),f(f(f(f(f(X1,X2),f(X2,X3)),X4),f(f(f(X1,X2),f(X2,X3)),X4)),f(X2,f(f(X3,f(f(X2,X2),X3)),X3)))),f(X2,f(f(X3,f(f(X2,X2),X3)),X3))))),
inference(cp,[status(thm)],[t7,t7]) ).
cnf(t2283,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(X3,f(f(X4,f(f(X3,X3),X4)),X4)),f(f(f(f(f(X2,X3),f(X3,X4)),Y4),f(f(f(X2,X3),f(X3,X4)),Y4)),f(X3,f(f(X4,f(f(X3,X3),X4)),X4)))),f(X3,f(f(X4,f(f(X3,X3),X4)),X4))))) = f(f(f(X2,X3),f(X3,X4)),Y4),
inference(orient,[status(thm)],[t11]) ).
cnf(t4267,plain,
b = f(f(f(f(X1,b),f(b,X2)),X3),f(b,b)),
inference(cp,[status(thm)],[t4266,t2283]) ).
cnf(t9196,plain,
f(f(f(f(X1,b),f(b,X2)),X3),f(b,b)) = b,
inference(orient,[status(thm)],[t4267]) ).
cnf(t11686,plain,
b = f(f(f(f(X1,b),sFlat2),X2),f(b,b)),
inference(cp,[status(thm)],[t9196,t11681]) ).
cnf(t19975,plain,
f(f(f(f(X1,b),sFlat2),X2),f(b,b)) = b,
inference(orient,[status(thm)],[t11686]) ).
cnf(t150221,plain,
f(f(b,b),sFlat2) = b,
inference(step,[status(thm)],[t38726,t19975]) ).
cnf(t38776,plain,
f(f(b,b),sFlat2) = b,
inference(orient,[status(thm)],[t150221]) ).
cnf(t77022,plain,
sFlat2 = f(f(f(b,f(sFlat2,X1)),X2),f(sFlat2,sFlat2)),
inference(cp,[status(thm)],[t76576,t38776]) ).
cnf(t108462,plain,
f(f(f(b,f(sFlat2,X1)),X2),f(sFlat2,sFlat2)) = sFlat2,
inference(orient,[status(thm)],[t77022]) ).
cnf(t26,plain,
c = f(f(f(sFlat3,f(c,X1)),X2),f(c,f(f(X1,f(f(c,c),X1)),X1))),
inference(cp,[status(thm)],[t7,t25]) ).
cnf(t125,plain,
f(f(f(sFlat3,f(c,X1)),X2),f(c,f(f(X1,f(f(c,c),X1)),X1))) = c,
inference(orient,[status(thm)],[t26]) ).
cnf(t126,plain,
c = f(f(f(sFlat3,sFlat2),X1),f(c,f(f(sFlat1,f(f(c,c),sFlat1)),sFlat1))),
inference(cp,[status(thm)],[t125,t45]) ).
cnf(t132,plain,
f(f(f(sFlat3,sFlat2),X1),f(c,f(f(sFlat1,f(f(c,c),sFlat1)),sFlat1))) = c,
inference(orient,[status(thm)],[t126]) ).
cnf(t1698,plain,
f(f(f(sFlat3,sFlat2),X1),f(c,f(f(sFlat1,f(f(c,c),sFlat1)),sFlat1))) = f(f(f(sFlat3,sFlat2),X1),f(c,f(f(f(sFlat3,sFlat2),X1),f(c,f(f(sFlat1,f(f(c,c),sFlat1)),sFlat1))))),
inference(cp,[status(thm)],[t1687,t132]) ).
cnf(t149836,plain,
c = f(f(f(sFlat3,sFlat2),X1),f(c,f(f(f(sFlat3,sFlat2),X1),f(c,f(f(sFlat1,f(f(c,c),sFlat1)),sFlat1))))),
inference(step,[status(thm)],[t1698,t132]) ).
cnf(t149837,plain,
c = f(f(f(sFlat3,sFlat2),X1),f(c,c)),
inference(step,[status(thm)],[t149836,t132]) ).
cnf(t1877,plain,
f(f(f(sFlat3,sFlat2),X1),f(c,c)) = c,
inference(orient,[status(thm)],[t149837]) ).
cnf(t1878,plain,
c = f(sFlat2,f(c,c)),
inference(cp,[status(thm)],[t1877,t1102]) ).
cnf(t1899,plain,
f(sFlat2,f(c,c)) = c,
inference(orient,[status(thm)],[t1878]) ).
cnf(t1902,plain,
f(sFlat2,f(c,c)) = f(sFlat2,f(c,f(f(X1,f(f(f(sFlat2,f(c,c)),f(sFlat2,f(c,c))),X1)),X1))),
inference(cp,[status(thm)],[t201,t1899]) ).
cnf(t149950,plain,
c = f(sFlat2,f(c,f(f(X1,f(f(f(sFlat2,f(c,c)),f(sFlat2,f(c,c))),X1)),X1))),
inference(step,[status(thm)],[t1902,t1899]) ).
cnf(t149951,plain,
c = f(sFlat2,f(c,f(f(X1,f(f(c,f(sFlat2,f(c,c))),X1)),X1))),
inference(step,[status(thm)],[t149950,t1899]) ).
cnf(t149952,plain,
c = f(sFlat2,f(c,f(f(X1,f(f(c,c),X1)),X1))),
inference(step,[status(thm)],[t149951,t1899]) ).
cnf(t8580,plain,
f(sFlat2,f(c,f(f(X1,f(f(c,c),X1)),X1))) = c,
inference(orient,[status(thm)],[t149952]) ).
cnf(t1697,plain,
f(f(f(sFlat3,f(c,X1)),X2),f(c,f(f(X1,f(f(c,c),X1)),X1))) = f(f(f(sFlat3,f(c,X1)),X2),f(c,f(f(f(sFlat3,f(c,X1)),X2),f(c,f(f(X1,f(f(c,c),X1)),X1))))),
inference(cp,[status(thm)],[t1687,t125]) ).
cnf(t149894,plain,
c = f(f(f(sFlat3,f(c,X1)),X2),f(c,f(f(f(sFlat3,f(c,X1)),X2),f(c,f(f(X1,f(f(c,c),X1)),X1))))),
inference(step,[status(thm)],[t1697,t125]) ).
cnf(t149895,plain,
c = f(f(f(sFlat3,f(c,X1)),X2),f(c,c)),
inference(step,[status(thm)],[t149894,t125]) ).
cnf(t4120,plain,
f(f(f(sFlat3,f(c,X1)),X2),f(c,c)) = c,
inference(orient,[status(thm)],[t149895]) ).
cnf(t43,plain,
sFlat3 = f(f(f(f(X1,sFlat3),f(sFlat3,X2)),X3),f(sFlat3,f(f(X2,f(sFlat4,X2)),X2))),
inference(cp,[status(thm)],[t7,t40]) ).
cnf(t167,plain,
f(f(f(f(X1,sFlat3),f(sFlat3,X2)),X3),f(sFlat3,f(f(X2,f(sFlat4,X2)),X2))) = sFlat3,
inference(orient,[status(thm)],[t43]) ).
cnf(t652,plain,
sFlat3 = f(f(X1,sFlat3),f(sFlat3,f(f(X2,f(sFlat4,X2)),X2))),
inference(cp,[status(thm)],[t167,t546]) ).
cnf(t752,plain,
f(f(X1,sFlat3),f(sFlat3,f(f(X2,f(sFlat4,X2)),X2))) = sFlat3,
inference(orient,[status(thm)],[t652]) ).
cnf(t41,plain,
sFlat3 = f(f(f(sFlat4,f(sFlat3,X1)),X2),f(sFlat3,f(f(X1,f(f(sFlat3,sFlat3),X1)),X1))),
inference(cp,[status(thm)],[t7,t40]) ).
cnf(t149738,plain,
sFlat3 = f(f(f(sFlat4,f(sFlat3,X1)),X2),f(sFlat3,f(f(X1,f(sFlat4,X1)),X1))),
inference(step,[status(thm)],[t41,t40]) ).
cnf(t73,plain,
f(f(f(sFlat4,f(sFlat3,X1)),X2),f(sFlat3,f(f(X1,f(sFlat4,X1)),X1))) = sFlat3,
inference(orient,[status(thm)],[t149738]) ).
cnf(t658,plain,
sFlat3 = f(sFlat4,f(sFlat3,f(f(X1,f(sFlat4,X1)),X1))),
inference(cp,[status(thm)],[t73,t546]) ).
cnf(t735,plain,
f(sFlat4,f(sFlat3,f(f(X1,f(sFlat4,X1)),X1))) = sFlat3,
inference(orient,[status(thm)],[t658]) ).
cnf(t753,plain,
sFlat3 = f(f(X1,sFlat3),f(sFlat3,f(f(f(sFlat3,f(f(X2,f(sFlat4,X2)),X2)),sFlat3),f(sFlat3,f(f(X2,f(sFlat4,X2)),X2))))),
inference(cp,[status(thm)],[t752,t735]) ).
cnf(t149746,plain,
sFlat3 = f(f(X1,sFlat3),f(sFlat3,sFlat3)),
inference(step,[status(thm)],[t753,t752]) ).
cnf(t149747,plain,
sFlat3 = f(f(X1,sFlat3),sFlat4),
inference(step,[status(thm)],[t149746,t40]) ).
cnf(t768,plain,
f(f(X1,sFlat3),sFlat4) = sFlat3,
inference(orient,[status(thm)],[t149747]) ).
cnf(t775,plain,
sFlat3 = f(f(sFlat3,X1),f(sFlat3,f(f(f(f(sFlat4,sFlat3),sFlat4),f(f(sFlat3,sFlat3),f(f(sFlat4,f(f(sFlat3,sFlat3),sFlat4)),sFlat4))),f(f(sFlat4,f(f(sFlat3,sFlat3),sFlat4)),sFlat4)))),
inference(cp,[status(thm)],[t546,t768]) ).
cnf(t149786,plain,
sFlat3 = f(f(sFlat3,X1),f(sFlat3,f(f(sFlat3,f(f(sFlat3,sFlat3),f(f(sFlat4,f(f(sFlat3,sFlat3),sFlat4)),sFlat4))),f(f(sFlat4,f(f(sFlat3,sFlat3),sFlat4)),sFlat4)))),
inference(step,[status(thm)],[t775,t768]) ).
cnf(t149787,plain,
sFlat3 = f(f(sFlat3,X1),f(sFlat3,f(f(sFlat3,f(sFlat4,f(f(sFlat4,f(f(sFlat3,sFlat3),sFlat4)),sFlat4))),f(f(sFlat4,f(f(sFlat3,sFlat3),sFlat4)),sFlat4)))),
inference(step,[status(thm)],[t149786,t40]) ).
cnf(t149788,plain,
sFlat3 = f(f(sFlat3,X1),f(sFlat3,f(f(sFlat3,f(sFlat4,f(f(sFlat4,sFlat3),sFlat4))),f(f(sFlat4,f(f(sFlat3,sFlat3),sFlat4)),sFlat4)))),
inference(step,[status(thm)],[t149787,t768]) ).
cnf(t149789,plain,
sFlat3 = f(f(sFlat3,X1),f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),f(f(sFlat4,f(f(sFlat3,sFlat3),sFlat4)),sFlat4)))),
inference(step,[status(thm)],[t149788,t768]) ).
cnf(t149790,plain,
sFlat3 = f(f(sFlat3,X1),f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),f(f(sFlat4,sFlat3),sFlat4)))),
inference(step,[status(thm)],[t149789,t768]) ).
cnf(t149791,plain,
sFlat3 = f(f(sFlat3,X1),f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),sFlat3))),
inference(step,[status(thm)],[t149790,t768]) ).
cnf(t1024,plain,
f(f(sFlat3,X1),f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),sFlat3))) = sFlat3,
inference(orient,[status(thm)],[t149791]) ).
cnf(t76,plain,
sFlat3 = f(f(sFlat3,X1),f(sFlat3,f(f(f(f(X2,f(sFlat4,X2)),X2),f(f(sFlat3,sFlat3),f(f(X2,f(sFlat4,X2)),X2))),f(f(X2,f(sFlat4,X2)),X2)))),
inference(cp,[status(thm)],[t7,t73]) ).
cnf(t149743,plain,
sFlat3 = f(f(sFlat3,X1),f(sFlat3,f(f(f(f(X2,f(sFlat4,X2)),X2),f(sFlat4,f(f(X2,f(sFlat4,X2)),X2))),f(f(X2,f(sFlat4,X2)),X2)))),
inference(step,[status(thm)],[t76,t40]) ).
cnf(t470,plain,
f(f(sFlat3,X1),f(sFlat3,f(f(f(f(X2,f(sFlat4,X2)),X2),f(sFlat4,f(f(X2,f(sFlat4,X2)),X2))),f(f(X2,f(sFlat4,X2)),X2)))) = sFlat3,
inference(orient,[status(thm)],[t149743]) ).
cnf(t489,plain,
c = f(sFlat3,f(c,f(f(X1,f(f(c,c),X1)),X1))),
inference(cp,[status(thm)],[t125,t470]) ).
cnf(t505,plain,
f(sFlat3,f(c,f(f(X1,f(f(c,c),X1)),X1))) = c,
inference(orient,[status(thm)],[t489]) ).
cnf(t1025,plain,
sFlat3 = f(c,f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),sFlat3))),
inference(cp,[status(thm)],[t1024,t505]) ).
cnf(t1042,plain,
f(c,f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),sFlat3))) = sFlat3,
inference(orient,[status(thm)],[t1025]) ).
cnf(t1046,plain,
f(c,f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),sFlat3))) = f(c,f(sFlat3,f(f(X1,f(f(f(c,f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),sFlat3))),f(c,f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),sFlat3)))),X1)),X1))),
inference(cp,[status(thm)],[t201,t1042]) ).
cnf(t149792,plain,
sFlat3 = f(c,f(sFlat3,f(f(X1,f(f(f(c,f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),sFlat3))),f(c,f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),sFlat3)))),X1)),X1))),
inference(step,[status(thm)],[t1046,t1042]) ).
cnf(t149793,plain,
sFlat3 = f(c,f(sFlat3,f(f(X1,f(f(sFlat3,f(c,f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),sFlat3)))),X1)),X1))),
inference(step,[status(thm)],[t149792,t1042]) ).
cnf(t149794,plain,
sFlat3 = f(c,f(sFlat3,f(f(X1,f(f(sFlat3,sFlat3),X1)),X1))),
inference(step,[status(thm)],[t149793,t1042]) ).
cnf(t149795,plain,
sFlat3 = f(c,f(sFlat3,f(f(X1,f(sFlat4,X1)),X1))),
inference(step,[status(thm)],[t149794,t40]) ).
cnf(t1049,plain,
f(c,f(sFlat3,f(f(X1,f(sFlat4,X1)),X1))) = sFlat3,
inference(orient,[status(thm)],[t149795]) ).
cnf(t237,plain,
f(sFlat4,f(sFlat3,X1)) = f(sFlat4,f(f(sFlat4,f(sFlat3,X1)),f(f(f(sFlat3,f(f(X1,f(sFlat4,X1)),X1)),sFlat3),f(sFlat3,f(f(X1,f(sFlat4,X1)),X1))))),
inference(cp,[status(thm)],[t201,t73]) ).
cnf(t339,plain,
f(sFlat4,f(f(sFlat4,f(sFlat3,X1)),f(f(f(sFlat3,f(f(X1,f(sFlat4,X1)),X1)),sFlat3),f(sFlat3,f(f(X1,f(sFlat4,X1)),X1))))) = f(sFlat4,f(sFlat3,X1)),
inference(orient,[status(thm)],[t237]) ).
cnf(t149745,plain,
f(sFlat4,f(f(sFlat4,f(sFlat3,X1)),sFlat3)) = f(sFlat4,f(sFlat3,X1)),
inference(step,[status(thm)],[t339,t752]) ).
cnf(t767,plain,
f(sFlat4,f(f(sFlat4,f(sFlat3,X1)),sFlat3)) = f(sFlat4,f(sFlat3,X1)),
inference(rw,[status(thm)],[t149745]) ).
cnf(t813,plain,
f(sFlat4,f(f(sFlat4,f(sFlat3,X1)),sFlat3)) = f(sFlat4,f(sFlat3,X1)),
inference(orient,[status(thm)],[t767]) ).
cnf(t27,plain,
b = f(f(f(f(X1,b),sFlat3),X2),f(b,f(f(c,f(f(b,b),c)),c))),
inference(cp,[status(thm)],[t7,t25]) ).
cnf(t142,plain,
f(f(f(f(X1,b),sFlat3),X2),f(b,f(f(c,f(f(b,b),c)),c))) = b,
inference(orient,[status(thm)],[t27]) ).
cnf(t758,plain,
b = f(sFlat3,f(b,f(f(c,f(f(b,b),c)),c))),
inference(cp,[status(thm)],[t142,t752]) ).
cnf(t1003,plain,
f(sFlat3,f(b,f(f(c,f(f(b,b),c)),c))) = b,
inference(orient,[status(thm)],[t758]) ).
cnf(t1004,plain,
f(sFlat4,f(sFlat3,f(b,f(f(c,f(f(b,b),c)),c)))) = f(sFlat4,f(f(sFlat4,b),sFlat3)),
inference(cp,[status(thm)],[t813,t1003]) ).
cnf(t149785,plain,
f(sFlat4,b) = f(sFlat4,f(f(sFlat4,b),sFlat3)),
inference(step,[status(thm)],[t1004,t1003]) ).
cnf(t1013,plain,
f(sFlat4,f(f(sFlat4,b),sFlat3)) = f(sFlat4,b),
inference(orient,[status(thm)],[t149785]) ).
cnf(t769,plain,
sFlat3 = f(sFlat4,sFlat4),
inference(cp,[status(thm)],[t768,t40]) ).
cnf(t779,plain,
f(sFlat4,sFlat4) = sFlat3,
inference(orient,[status(thm)],[t769]) ).
cnf(t1299,plain,
sFlat4 = f(f(X1,sFlat4),sFlat3),
inference(cp,[status(thm)],[t1246,t779]) ).
cnf(t1352,plain,
f(f(X1,sFlat4),sFlat3) = sFlat4,
inference(orient,[status(thm)],[t1299]) ).
cnf(t1354,plain,
sFlat4 = f(f(f(f(X1,sFlat4),f(sFlat4,sFlat3)),X2),f(sFlat4,f(f(sFlat3,sFlat4),sFlat3))),
inference(cp,[status(thm)],[t7,t1352]) ).
cnf(t149876,plain,
sFlat4 = f(f(f(f(X1,sFlat4),f(sFlat4,sFlat3)),X2),f(sFlat4,sFlat4)),
inference(step,[status(thm)],[t1354,t1352]) ).
cnf(t149877,plain,
sFlat4 = f(f(f(f(X1,sFlat4),f(sFlat4,sFlat3)),X2),sFlat3),
inference(step,[status(thm)],[t149876,t779]) ).
cnf(t3736,plain,
f(f(f(f(X1,sFlat4),f(sFlat4,sFlat3)),X2),sFlat3) = sFlat4,
inference(orient,[status(thm)],[t149877]) ).
cnf(t1704,plain,
f(f(f(sFlat4,f(sFlat3,X1)),X2),f(sFlat3,f(f(X1,f(sFlat4,X1)),X1))) = f(f(f(sFlat4,f(sFlat3,X1)),X2),f(sFlat3,f(f(f(sFlat4,f(sFlat3,X1)),X2),f(sFlat3,f(f(X1,f(sFlat4,X1)),X1))))),
inference(cp,[status(thm)],[t1687,t73]) ).
cnf(t149842,plain,
sFlat3 = f(f(f(sFlat4,f(sFlat3,X1)),X2),f(sFlat3,f(f(f(sFlat4,f(sFlat3,X1)),X2),f(sFlat3,f(f(X1,f(sFlat4,X1)),X1))))),
inference(step,[status(thm)],[t1704,t73]) ).
cnf(t149843,plain,
sFlat3 = f(f(f(sFlat4,f(sFlat3,X1)),X2),f(sFlat3,sFlat3)),
inference(step,[status(thm)],[t149842,t73]) ).
cnf(t149844,plain,
sFlat3 = f(f(f(sFlat4,f(sFlat3,X1)),X2),sFlat4),
inference(step,[status(thm)],[t149843,t40]) ).
cnf(t1945,plain,
f(f(f(sFlat4,f(sFlat3,X1)),X2),sFlat4) = sFlat3,
inference(orient,[status(thm)],[t149844]) ).
cnf(t1948,plain,
sFlat3 = f(f(f(sFlat4,c),X1),sFlat4),
inference(cp,[status(thm)],[t1945,t505]) ).
cnf(t1987,plain,
f(f(f(sFlat4,c),X1),sFlat4) = sFlat3,
inference(orient,[status(thm)],[t1948]) ).
cnf(t3740,plain,
sFlat4 = f(f(f(sFlat3,f(sFlat4,sFlat3)),X1),sFlat3),
inference(cp,[status(thm)],[t3736,t1987]) ).
cnf(t3798,plain,
f(f(f(sFlat3,f(sFlat4,sFlat3)),X1),sFlat3) = sFlat4,
inference(orient,[status(thm)],[t3740]) ).
cnf(t3804,plain,
f(sFlat3,f(sFlat4,sFlat3)) = f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),f(f(sFlat3,sFlat4),sFlat3))),
inference(cp,[status(thm)],[t201,t3798]) ).
cnf(t149878,plain,
f(sFlat3,f(sFlat4,sFlat3)) = f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),sFlat4)),
inference(step,[status(thm)],[t3804,t1352]) ).
cnf(t1253,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)],[t1246,t1024]) ).
cnf(t149812,plain,
f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),sFlat3)) = f(sFlat3,sFlat3),
inference(step,[status(thm)],[t1253,t1024]) ).
cnf(t149813,plain,
f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),sFlat3)) = sFlat4,
inference(step,[status(thm)],[t149812,t40]) ).
cnf(t1398,plain,
f(sFlat3,f(f(sFlat3,f(sFlat4,sFlat3)),sFlat3)) = sFlat4,
inference(orient,[status(thm)],[t149813]) ).
cnf(t1400,plain,
sFlat3 = f(f(f(f(X1,sFlat3),f(sFlat3,sFlat3)),X2),sFlat4),
inference(cp,[status(thm)],[t167,t1398]) ).
cnf(t149815,plain,
sFlat3 = f(f(sFlat3,X2),sFlat4),
inference(step,[status(thm)],[t1400,t1246]) ).
cnf(t1405,plain,
f(f(sFlat3,X1),sFlat4) = sFlat3,
inference(orient,[status(thm)],[t149815]) ).
cnf(t149879,plain,
f(sFlat3,f(sFlat4,sFlat3)) = f(sFlat3,sFlat3),
inference(step,[status(thm)],[t149878,t1405]) ).
cnf(t149880,plain,
f(sFlat3,f(sFlat4,sFlat3)) = sFlat4,
inference(step,[status(thm)],[t149879,t40]) ).
cnf(t3833,plain,
f(sFlat3,f(sFlat4,sFlat3)) = sFlat4,
inference(orient,[status(thm)],[t149880]) ).
cnf(t149881,plain,
f(f(sFlat4,X1),sFlat3) = sFlat4,
inference(step,[status(thm)],[t3798,t3833]) ).
cnf(t3849,plain,
f(f(sFlat4,X1),sFlat3) = sFlat4,
inference(rw,[status(thm)],[t149881]) ).
cnf(t3850,plain,
f(f(sFlat4,X1),sFlat3) = sFlat4,
inference(orient,[status(thm)],[t3849]) ).
cnf(t149884,plain,
f(sFlat4,sFlat4) = f(sFlat4,b),
inference(step,[status(thm)],[t1013,t3850]) ).
cnf(t149885,plain,
sFlat3 = f(sFlat4,b),
inference(step,[status(thm)],[t149884,t779]) ).
cnf(t3879,plain,
sFlat3 = f(sFlat4,b),
inference(rw,[status(thm)],[t149885]) ).
cnf(t3900,plain,
f(sFlat4,b) = sFlat3,
inference(orient,[status(thm)],[t3879]) ).
cnf(t3901,plain,
sFlat3 = f(c,f(sFlat3,f(f(b,sFlat3),b))),
inference(cp,[status(thm)],[t1049,t3900]) ).
cnf(t4003,plain,
f(c,f(sFlat3,f(f(b,sFlat3),b))) = sFlat3,
inference(orient,[status(thm)],[t3901]) ).
cnf(t4126,plain,
c = f(f(f(sFlat3,sFlat3),X1),f(c,c)),
inference(cp,[status(thm)],[t4120,t4003]) ).
cnf(t149896,plain,
c = f(f(sFlat4,X1),f(c,c)),
inference(step,[status(thm)],[t4126,t40]) ).
cnf(t4218,plain,
f(f(sFlat4,X1),f(c,c)) = c,
inference(orient,[status(thm)],[t149896]) ).
cnf(t1274,plain,
sFlat4 = f(sFlat5,f(sFlat4,sFlat4)),
inference(cp,[status(thm)],[t1246,t48]) ).
cnf(t149810,plain,
sFlat4 = f(sFlat5,sFlat3),
inference(step,[status(thm)],[t1274,t779]) ).
cnf(t1330,plain,
f(sFlat5,sFlat3) = sFlat4,
inference(orient,[status(thm)],[t149810]) ).
cnf(t11340,plain,
sFlat5 = f(sFlat4,f(sFlat5,sFlat5)),
inference(cp,[status(thm)],[t11288,t1330]) ).
cnf(t11497,plain,
f(sFlat4,f(sFlat5,sFlat5)) = sFlat5,
inference(orient,[status(thm)],[t11340]) ).
cnf(t11500,plain,
c = f(sFlat5,f(c,c)),
inference(cp,[status(thm)],[t4218,t11497]) ).
cnf(t11621,plain,
f(sFlat5,f(c,c)) = c,
inference(orient,[status(thm)],[t11500]) ).
cnf(t11622,plain,
sFlat5 = f(c,f(sFlat5,sFlat5)),
inference(cp,[status(thm)],[t11288,t11621]) ).
cnf(t11737,plain,
f(c,f(sFlat5,sFlat5)) = sFlat5,
inference(orient,[status(thm)],[t11622]) ).
cnf(t11738,plain,
f(c,c) = f(f(X1,f(c,c)),f(f(c,c),sFlat5)),
inference(cp,[status(thm)],[t10071,t11737]) ).
cnf(t25729,plain,
f(f(X1,f(c,c)),f(f(c,c),sFlat5)) = f(c,c),
inference(orient,[status(thm)],[t11738]) ).
cnf(t25730,plain,
f(c,c) = f(f(f(c,c),sFlat5),f(f(c,c),sFlat5)),
inference(cp,[status(thm)],[t25729,t11919]) ).
cnf(t39989,plain,
f(f(f(c,c),sFlat5),f(f(c,c),sFlat5)) = f(c,c),
inference(orient,[status(thm)],[t25730]) ).
cnf(t39990,plain,
f(f(c,c),sFlat5) = f(f(f(f(c,c),sFlat5),X1),f(c,c)),
inference(cp,[status(thm)],[t11288,t39989]) ).
cnf(t47,plain,
c = f(f(f(f(X1,c),sFlat2),X2),f(c,f(f(sFlat1,f(f(c,c),sFlat1)),sFlat1))),
inference(cp,[status(thm)],[t7,t45]) ).
cnf(t185,plain,
f(f(f(f(X1,c),sFlat2),X2),f(c,f(f(sFlat1,f(f(c,c),sFlat1)),sFlat1))) = c,
inference(orient,[status(thm)],[t47]) ).
cnf(t1696,plain,
f(f(f(f(X1,c),sFlat2),X2),f(c,f(f(sFlat1,f(f(c,c),sFlat1)),sFlat1))) = f(f(f(f(X1,c),sFlat2),X2),f(c,f(f(f(f(X1,c),sFlat2),X2),f(c,f(f(sFlat1,f(f(c,c),sFlat1)),sFlat1))))),
inference(cp,[status(thm)],[t1687,t185]) ).
cnf(t149892,plain,
c = f(f(f(f(X1,c),sFlat2),X2),f(c,f(f(f(f(X1,c),sFlat2),X2),f(c,f(f(sFlat1,f(f(c,c),sFlat1)),sFlat1))))),
inference(step,[status(thm)],[t1696,t185]) ).
cnf(t149893,plain,
c = f(f(f(f(X1,c),sFlat2),X2),f(c,c)),
inference(step,[status(thm)],[t149892,t185]) ).
cnf(t4079,plain,
f(f(f(f(X1,c),sFlat2),X2),f(c,c)) = c,
inference(orient,[status(thm)],[t149893]) ).
cnf(t4080,plain,
c = f(f(f(f(X1,c),f(c,X2)),X3),f(c,c)),
inference(cp,[status(thm)],[t4079,t2283]) ).
cnf(t9051,plain,
f(f(f(f(X1,c),f(c,X2)),X3),f(c,c)) = c,
inference(orient,[status(thm)],[t4080]) ).
cnf(t11740,plain,
c = f(f(f(f(X1,c),sFlat5),X2),f(c,c)),
inference(cp,[status(thm)],[t9051,t11737]) ).
cnf(t20301,plain,
f(f(f(f(X1,c),sFlat5),X2),f(c,c)) = c,
inference(orient,[status(thm)],[t11740]) ).
cnf(t150227,plain,
f(f(c,c),sFlat5) = c,
inference(step,[status(thm)],[t39990,t20301]) ).
cnf(t40040,plain,
f(f(c,c),sFlat5) = c,
inference(orient,[status(thm)],[t150227]) ).
cnf(t40052,plain,
c = f(sFlat2,f(c,f(f(sFlat5,c),sFlat5))),
inference(cp,[status(thm)],[t8580,t40040]) ).
cnf(t40285,plain,
f(sFlat2,f(c,f(f(sFlat5,c),sFlat5))) = c,
inference(orient,[status(thm)],[t40052]) ).
cnf(t108490,plain,
sFlat2 = f(f(f(b,c),X1),f(sFlat2,sFlat2)),
inference(cp,[status(thm)],[t108462,t40285]) ).
cnf(t150822,plain,
sFlat2 = f(f(sFlat3,X1),f(sFlat2,sFlat2)),
inference(step,[status(thm)],[t108490,t25]) ).
cnf(t108575,plain,
f(f(sFlat3,X1),f(sFlat2,sFlat2)) = sFlat2,
inference(orient,[status(thm)],[t150822]) ).
cnf(t3737,plain,
sFlat4 = f(f(f(f(X1,sFlat4),f(sFlat4,X2)),X3),sFlat3),
inference(cp,[status(thm)],[t3736,t2283]) ).
cnf(t6896,plain,
f(f(f(f(X1,sFlat4),f(sFlat4,X2)),X3),sFlat3) = sFlat4,
inference(orient,[status(thm)],[t3737]) ).
cnf(t772,plain,
sFlat3 = f(f(f(f(X1,sFlat3),f(sFlat3,sFlat4)),X2),f(sFlat3,f(f(sFlat4,sFlat3),sFlat4))),
inference(cp,[status(thm)],[t7,t768]) ).
cnf(t149757,plain,
sFlat3 = f(f(f(f(X1,sFlat3),f(sFlat3,sFlat4)),X2),f(sFlat3,sFlat3)),
inference(step,[status(thm)],[t772,t768]) ).
cnf(t149758,plain,
sFlat3 = f(f(f(f(X1,sFlat3),f(sFlat3,sFlat4)),X2),sFlat4),
inference(step,[status(thm)],[t149757,t40]) ).
cnf(t836,plain,
f(f(f(f(X1,sFlat3),f(sFlat3,sFlat4)),X2),sFlat4) = sFlat3,
inference(orient,[status(thm)],[t149758]) ).
cnf(t3571,plain,
sFlat3 = f(f(f(f(X1,sFlat3),f(sFlat3,X2)),X3),sFlat4),
inference(cp,[status(thm)],[t836,t2283]) ).
cnf(t6756,plain,
f(f(f(f(X1,sFlat3),f(sFlat3,X2)),X3),sFlat4) = sFlat3,
inference(orient,[status(thm)],[t3571]) ).
cnf(t6760,plain,
sFlat3 = f(f(f(f(X1,sFlat3),c),X2),sFlat4),
inference(cp,[status(thm)],[t6756,t505]) ).
cnf(t6852,plain,
f(f(f(f(X1,sFlat3),c),X2),sFlat4) = sFlat3,
inference(orient,[status(thm)],[t6760]) ).
cnf(t6897,plain,
sFlat4 = f(f(f(sFlat3,f(sFlat4,X1)),X2),sFlat3),
inference(cp,[status(thm)],[t6896,t6852]) ).
cnf(t6951,plain,
f(f(f(sFlat3,f(sFlat4,X1)),X2),sFlat3) = sFlat4,
inference(orient,[status(thm)],[t6897]) ).
cnf(t6961,plain,
f(sFlat3,f(sFlat4,X1)) = f(sFlat3,f(f(sFlat3,f(sFlat4,X1)),f(f(sFlat3,sFlat4),sFlat3))),
inference(cp,[status(thm)],[t201,t6951]) ).
cnf(t149918,plain,
f(sFlat3,f(sFlat4,X1)) = f(sFlat3,f(f(sFlat3,f(sFlat4,X1)),sFlat4)),
inference(step,[status(thm)],[t6961,t1352]) ).
cnf(t149919,plain,
f(sFlat3,f(sFlat4,X1)) = f(sFlat3,sFlat3),
inference(step,[status(thm)],[t149918,t1405]) ).
cnf(t149920,plain,
f(sFlat3,f(sFlat4,X1)) = sFlat4,
inference(step,[status(thm)],[t149919,t40]) ).
cnf(t6997,plain,
f(sFlat3,f(sFlat4,X1)) = sFlat4,
inference(orient,[status(thm)],[t149920]) ).
cnf(t11337,plain,
f(X1,sFlat4) = f(sFlat4,f(f(X1,sFlat4),f(X1,sFlat4))),
inference(cp,[status(thm)],[t11288,t1352]) ).
cnf(t15095,plain,
f(sFlat4,f(f(X1,sFlat4),f(X1,sFlat4))) = f(X1,sFlat4),
inference(orient,[status(thm)],[t11337]) ).
cnf(t15096,plain,
sFlat4 = f(sFlat3,f(X1,sFlat4)),
inference(cp,[status(thm)],[t6997,t15095]) ).
cnf(t15130,plain,
f(sFlat3,f(X1,sFlat4)) = sFlat4,
inference(orient,[status(thm)],[t15096]) ).
cnf(t108576,plain,
sFlat2 = f(sFlat4,f(sFlat2,sFlat2)),
inference(cp,[status(thm)],[t108575,t15130]) ).
cnf(t108680,plain,
f(sFlat4,f(sFlat2,sFlat2)) = sFlat2,
inference(orient,[status(thm)],[t108576]) ).
cnf(t108709,plain,
f(sFlat4,f(sFlat2,sFlat2)) = f(sFlat4,f(sFlat2,f(f(f(sFlat4,f(sFlat2,sFlat2)),f(sFlat4,f(sFlat2,sFlat2))),X1))),
inference(cp,[status(thm)],[t80351,t108680]) ).
cnf(t150905,plain,
sFlat2 = f(sFlat4,f(sFlat2,f(f(f(sFlat4,f(sFlat2,sFlat2)),f(sFlat4,f(sFlat2,sFlat2))),X1))),
inference(step,[status(thm)],[t108709,t108680]) ).
cnf(t150906,plain,
sFlat2 = f(sFlat4,f(sFlat2,f(f(sFlat2,f(sFlat4,f(sFlat2,sFlat2))),X1))),
inference(step,[status(thm)],[t150905,t108680]) ).
cnf(t150907,plain,
sFlat2 = f(sFlat4,f(sFlat2,f(f(sFlat2,sFlat2),X1))),
inference(step,[status(thm)],[t150906,t108680]) ).
cnf(t110054,plain,
f(sFlat4,f(sFlat2,f(f(sFlat2,sFlat2),X1))) = sFlat2,
inference(orient,[status(thm)],[t150907]) ).
cnf(t77103,plain,
sFlat5 = f(f(f(c,f(sFlat5,X1)),X2),f(sFlat5,sFlat5)),
inference(cp,[status(thm)],[t76576,t40040]) ).
cnf(t22,plain,
a = f(f(f(sFlat0,f(a,X1)),X2),f(a,f(f(X1,f(f(a,a),X1)),X1))),
inference(cp,[status(thm)],[t7,t21]) ).
cnf(t95,plain,
f(f(f(sFlat0,f(a,X1)),X2),f(a,f(f(X1,f(f(a,a),X1)),X1))) = a,
inference(orient,[status(thm)],[t22]) ).
cnf(t1701,plain,
f(f(f(sFlat0,f(a,X1)),X2),f(a,f(f(X1,f(f(a,a),X1)),X1))) = f(f(f(sFlat0,f(a,X1)),X2),f(a,f(f(f(sFlat0,f(a,X1)),X2),f(a,f(f(X1,f(f(a,a),X1)),X1))))),
inference(cp,[status(thm)],[t1687,t95]) ).
cnf(t149904,plain,
a = f(f(f(sFlat0,f(a,X1)),X2),f(a,f(f(f(sFlat0,f(a,X1)),X2),f(a,f(f(X1,f(f(a,a),X1)),X1))))),
inference(step,[status(thm)],[t1701,t95]) ).
cnf(t149905,plain,
a = f(f(f(sFlat0,f(a,X1)),X2),f(a,a)),
inference(step,[status(thm)],[t149904,t95]) ).
cnf(t4534,plain,
f(f(f(sFlat0,f(a,X1)),X2),f(a,a)) = a,
inference(orient,[status(thm)],[t149905]) ).
cnf(t54,plain,
sFlat0 = f(f(sFlat0,X1),f(sFlat0,f(f(f(f(X2,f(sFlat1,X2)),X2),f(f(sFlat0,sFlat0),f(f(X2,f(sFlat1,X2)),X2))),f(f(X2,f(sFlat1,X2)),X2)))),
inference(cp,[status(thm)],[t7,t51]) ).
cnf(t149742,plain,
sFlat0 = f(f(sFlat0,X1),f(sFlat0,f(f(f(f(X2,f(sFlat1,X2)),X2),f(sFlat1,f(f(X2,f(sFlat1,X2)),X2))),f(f(X2,f(sFlat1,X2)),X2)))),
inference(step,[status(thm)],[t54,t35]) ).
cnf(t375,plain,
f(f(sFlat0,X1),f(sFlat0,f(f(f(f(X2,f(sFlat1,X2)),X2),f(sFlat1,f(f(X2,f(sFlat1,X2)),X2))),f(f(X2,f(sFlat1,X2)),X2)))) = sFlat0,
inference(orient,[status(thm)],[t149742]) ).
cnf(t394,plain,
a = f(sFlat0,f(a,f(f(X1,f(f(a,a),X1)),X1))),
inference(cp,[status(thm)],[t95,t375]) ).
cnf(t410,plain,
f(sFlat0,f(a,f(f(X1,f(f(a,a),X1)),X1))) = a,
inference(orient,[status(thm)],[t394]) ).
cnf(t420,plain,
sFlat0 = f(a,f(sFlat0,f(f(f(f(X1,f(sFlat1,X1)),X1),f(sFlat1,f(f(X1,f(sFlat1,X1)),X1))),f(f(X1,f(sFlat1,X1)),X1)))),
inference(cp,[status(thm)],[t375,t410]) ).
cnf(t451,plain,
f(a,f(sFlat0,f(f(f(f(X1,f(sFlat1,X1)),X1),f(sFlat1,f(f(X1,f(sFlat1,X1)),X1))),f(f(X1,f(sFlat1,X1)),X1)))) = sFlat0,
inference(orient,[status(thm)],[t420]) ).
cnf(t897,plain,
sFlat0 = f(a,f(sFlat0,f(f(f(f(sFlat1,sFlat0),sFlat1),f(sFlat1,f(f(sFlat1,f(sFlat1,sFlat1)),sFlat1))),f(f(sFlat1,f(sFlat1,sFlat1)),sFlat1)))),
inference(cp,[status(thm)],[t451,t890]) ).
cnf(t149774,plain,
sFlat0 = f(a,f(sFlat0,f(f(sFlat0,f(sFlat1,f(f(sFlat1,f(sFlat1,sFlat1)),sFlat1))),f(f(sFlat1,f(sFlat1,sFlat1)),sFlat1)))),
inference(step,[status(thm)],[t897,t879]) ).
cnf(t149775,plain,
sFlat0 = f(a,f(sFlat0,f(f(sFlat0,f(sFlat1,f(f(sFlat1,sFlat0),sFlat1))),f(f(sFlat1,f(sFlat1,sFlat1)),sFlat1)))),
inference(step,[status(thm)],[t149774,t890]) ).
cnf(t149776,plain,
sFlat0 = f(a,f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),f(f(sFlat1,f(sFlat1,sFlat1)),sFlat1)))),
inference(step,[status(thm)],[t149775,t879]) ).
cnf(t149777,plain,
sFlat0 = f(a,f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),f(f(sFlat1,sFlat0),sFlat1)))),
inference(step,[status(thm)],[t149776,t890]) ).
cnf(t149778,plain,
sFlat0 = f(a,f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),sFlat0))),
inference(step,[status(thm)],[t149777,t879]) ).
cnf(t968,plain,
f(a,f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),sFlat0))) = sFlat0,
inference(orient,[status(thm)],[t149778]) ).
cnf(t972,plain,
f(a,f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),sFlat0))) = f(a,f(sFlat0,f(f(X1,f(f(f(a,f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),sFlat0))),f(a,f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),sFlat0)))),X1)),X1))),
inference(cp,[status(thm)],[t201,t968]) ).
cnf(t149779,plain,
sFlat0 = f(a,f(sFlat0,f(f(X1,f(f(f(a,f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),sFlat0))),f(a,f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),sFlat0)))),X1)),X1))),
inference(step,[status(thm)],[t972,t968]) ).
cnf(t149780,plain,
sFlat0 = f(a,f(sFlat0,f(f(X1,f(f(sFlat0,f(a,f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),sFlat0)))),X1)),X1))),
inference(step,[status(thm)],[t149779,t968]) ).
cnf(t149781,plain,
sFlat0 = f(a,f(sFlat0,f(f(X1,f(f(sFlat0,sFlat0),X1)),X1))),
inference(step,[status(thm)],[t149780,t968]) ).
cnf(t149782,plain,
sFlat0 = f(a,f(sFlat0,f(f(X1,f(sFlat1,X1)),X1))),
inference(step,[status(thm)],[t149781,t35]) ).
cnf(t990,plain,
f(a,f(sFlat0,f(f(X1,f(sFlat1,X1)),X1))) = sFlat0,
inference(orient,[status(thm)],[t149782]) ).
cnf(t242,plain,
f(sFlat1,f(sFlat0,X1)) = f(sFlat1,f(f(sFlat1,f(sFlat0,X1)),f(f(f(sFlat0,f(f(X1,f(sFlat1,X1)),X1)),sFlat0),f(sFlat0,f(f(X1,f(sFlat1,X1)),X1))))),
inference(cp,[status(thm)],[t201,t51]) ).
cnf(t357,plain,
f(sFlat1,f(f(sFlat1,f(sFlat0,X1)),f(f(f(sFlat0,f(f(X1,f(sFlat1,X1)),X1)),sFlat0),f(sFlat0,f(f(X1,f(sFlat1,X1)),X1))))) = f(sFlat1,f(sFlat0,X1)),
inference(orient,[status(thm)],[t242]) ).
cnf(t149759,plain,
f(sFlat1,f(f(sFlat1,f(sFlat0,X1)),sFlat0)) = f(sFlat1,f(sFlat0,X1)),
inference(step,[status(thm)],[t357,t863]) ).
cnf(t877,plain,
f(sFlat1,f(f(sFlat1,f(sFlat0,X1)),sFlat0)) = f(sFlat1,f(sFlat0,X1)),
inference(rw,[status(thm)],[t149759]) ).
cnf(t927,plain,
f(sFlat1,f(f(sFlat1,f(sFlat0,X1)),sFlat0)) = f(sFlat1,f(sFlat0,X1)),
inference(orient,[status(thm)],[t877]) ).
cnf(t928,plain,
f(sFlat1,f(sFlat0,f(a,f(f(X1,f(f(a,a),X1)),X1)))) = f(sFlat1,f(f(sFlat1,a),sFlat0)),
inference(cp,[status(thm)],[t927,t410]) ).
cnf(t149771,plain,
f(sFlat1,a) = f(sFlat1,f(f(sFlat1,a),sFlat0)),
inference(step,[status(thm)],[t928,t410]) ).
cnf(t942,plain,
f(sFlat1,f(f(sFlat1,a),sFlat0)) = f(sFlat1,a),
inference(orient,[status(thm)],[t149771]) ).
cnf(t1709,plain,
f(f(f(sFlat1,f(sFlat0,X1)),X2),f(sFlat0,f(f(X1,f(sFlat1,X1)),X1))) = f(f(f(sFlat1,f(sFlat0,X1)),X2),f(sFlat0,f(f(f(sFlat1,f(sFlat0,X1)),X2),f(sFlat0,f(f(X1,f(sFlat1,X1)),X1))))),
inference(cp,[status(thm)],[t1687,t51]) ).
cnf(t149845,plain,
sFlat0 = f(f(f(sFlat1,f(sFlat0,X1)),X2),f(sFlat0,f(f(f(sFlat1,f(sFlat0,X1)),X2),f(sFlat0,f(f(X1,f(sFlat1,X1)),X1))))),
inference(step,[status(thm)],[t1709,t51]) ).
cnf(t149846,plain,
sFlat0 = f(f(f(sFlat1,f(sFlat0,X1)),X2),f(sFlat0,sFlat0)),
inference(step,[status(thm)],[t149845,t51]) ).
cnf(t149847,plain,
sFlat0 = f(f(f(sFlat1,f(sFlat0,X1)),X2),sFlat1),
inference(step,[status(thm)],[t149846,t35]) ).
cnf(t2005,plain,
f(f(f(sFlat1,f(sFlat0,X1)),X2),sFlat1) = sFlat0,
inference(orient,[status(thm)],[t149847]) ).
cnf(t2008,plain,
sFlat0 = f(f(f(sFlat1,a),X1),sFlat1),
inference(cp,[status(thm)],[t2005,t410]) ).
cnf(t2047,plain,
f(f(f(sFlat1,a),X1),sFlat1) = sFlat0,
inference(orient,[status(thm)],[t2008]) ).
cnf(t2176,plain,
sFlat1 = f(f(f(sFlat0,f(sFlat1,sFlat0)),X1),sFlat0),
inference(cp,[status(thm)],[t2173,t2047]) ).
cnf(t2210,plain,
f(f(f(sFlat0,f(sFlat1,sFlat0)),X1),sFlat0) = sFlat1,
inference(orient,[status(thm)],[t2176]) ).
cnf(t2216,plain,
f(sFlat0,f(sFlat1,sFlat0)) = f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),f(f(sFlat0,sFlat1),sFlat0))),
inference(cp,[status(thm)],[t201,t2210]) ).
cnf(t149864,plain,
f(sFlat0,f(sFlat1,sFlat0)) = f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),sFlat1)),
inference(step,[status(thm)],[t2216,t1342]) ).
cnf(t886,plain,
sFlat0 = f(f(sFlat0,X1),f(sFlat0,f(f(f(f(sFlat1,sFlat0),sFlat1),f(f(sFlat0,sFlat0),f(f(sFlat1,f(f(sFlat0,sFlat0),sFlat1)),sFlat1))),f(f(sFlat1,f(f(sFlat0,sFlat0),sFlat1)),sFlat1)))),
inference(cp,[status(thm)],[t546,t879]) ).
cnf(t149799,plain,
sFlat0 = f(f(sFlat0,X1),f(sFlat0,f(f(sFlat0,f(f(sFlat0,sFlat0),f(f(sFlat1,f(f(sFlat0,sFlat0),sFlat1)),sFlat1))),f(f(sFlat1,f(f(sFlat0,sFlat0),sFlat1)),sFlat1)))),
inference(step,[status(thm)],[t886,t879]) ).
cnf(t149800,plain,
sFlat0 = f(f(sFlat0,X1),f(sFlat0,f(f(sFlat0,f(sFlat1,f(f(sFlat1,f(f(sFlat0,sFlat0),sFlat1)),sFlat1))),f(f(sFlat1,f(f(sFlat0,sFlat0),sFlat1)),sFlat1)))),
inference(step,[status(thm)],[t149799,t35]) ).
cnf(t149801,plain,
sFlat0 = f(f(sFlat0,X1),f(sFlat0,f(f(sFlat0,f(sFlat1,f(f(sFlat1,sFlat0),sFlat1))),f(f(sFlat1,f(f(sFlat0,sFlat0),sFlat1)),sFlat1)))),
inference(step,[status(thm)],[t149800,t879]) ).
cnf(t149802,plain,
sFlat0 = f(f(sFlat0,X1),f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),f(f(sFlat1,f(f(sFlat0,sFlat0),sFlat1)),sFlat1)))),
inference(step,[status(thm)],[t149801,t879]) ).
cnf(t149803,plain,
sFlat0 = f(f(sFlat0,X1),f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),f(f(sFlat1,sFlat0),sFlat1)))),
inference(step,[status(thm)],[t149802,t879]) ).
cnf(t149804,plain,
sFlat0 = f(f(sFlat0,X1),f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),sFlat0))),
inference(step,[status(thm)],[t149803,t879]) ).
cnf(t1085,plain,
f(f(sFlat0,X1),f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),sFlat0))) = sFlat0,
inference(orient,[status(thm)],[t149804]) ).
cnf(t1255,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)],[t1246,t1085]) ).
cnf(t149816,plain,
f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),sFlat0)) = f(sFlat0,sFlat0),
inference(step,[status(thm)],[t1255,t1085]) ).
cnf(t149817,plain,
f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),sFlat0)) = sFlat1,
inference(step,[status(thm)],[t149816,t35]) ).
cnf(t1667,plain,
f(sFlat0,f(f(sFlat0,f(sFlat1,sFlat0)),sFlat0)) = sFlat1,
inference(orient,[status(thm)],[t149817]) ).
cnf(t1669,plain,
sFlat0 = f(f(f(sFlat1,f(sFlat0,sFlat0)),X1),sFlat1),
inference(cp,[status(thm)],[t51,t1667]) ).
cnf(t149819,plain,
sFlat0 = f(f(f(sFlat1,sFlat1),X1),sFlat1),
inference(step,[status(thm)],[t1669,t35]) ).
cnf(t149820,plain,
sFlat0 = f(f(sFlat0,X1),sFlat1),
inference(step,[status(thm)],[t149819,t890]) ).
cnf(t1674,plain,
f(f(sFlat0,X1),sFlat1) = sFlat0,
inference(orient,[status(thm)],[t149820]) ).
cnf(t149865,plain,
f(sFlat0,f(sFlat1,sFlat0)) = f(sFlat0,sFlat0),
inference(step,[status(thm)],[t149864,t1674]) ).
cnf(t149866,plain,
f(sFlat0,f(sFlat1,sFlat0)) = sFlat1,
inference(step,[status(thm)],[t149865,t35]) ).
cnf(t2229,plain,
f(sFlat0,f(sFlat1,sFlat0)) = sFlat1,
inference(orient,[status(thm)],[t149866]) ).
cnf(t149867,plain,
f(f(sFlat1,X1),sFlat0) = sFlat1,
inference(step,[status(thm)],[t2210,t2229]) ).
cnf(t2237,plain,
f(f(sFlat1,X1),sFlat0) = sFlat1,
inference(rw,[status(thm)],[t149867]) ).
cnf(t2238,plain,
f(f(sFlat1,X1),sFlat0) = sFlat1,
inference(orient,[status(thm)],[t2237]) ).
cnf(t149870,plain,
f(sFlat1,sFlat1) = f(sFlat1,a),
inference(step,[status(thm)],[t942,t2238]) ).
cnf(t149871,plain,
sFlat0 = f(sFlat1,a),
inference(step,[status(thm)],[t149870,t890]) ).
cnf(t2255,plain,
sFlat0 = f(sFlat1,a),
inference(rw,[status(thm)],[t149871]) ).
cnf(t2272,plain,
f(sFlat1,a) = sFlat0,
inference(orient,[status(thm)],[t2255]) ).
cnf(t2274,plain,
sFlat0 = f(a,f(sFlat0,f(f(a,sFlat0),a))),
inference(cp,[status(thm)],[t990,t2272]) ).
cnf(t3701,plain,
f(a,f(sFlat0,f(f(a,sFlat0),a))) = sFlat0,
inference(orient,[status(thm)],[t2274]) ).
cnf(t4540,plain,
a = f(f(f(sFlat0,sFlat0),X1),f(a,a)),
inference(cp,[status(thm)],[t4534,t3701]) ).
cnf(t149906,plain,
a = f(f(sFlat1,X1),f(a,a)),
inference(step,[status(thm)],[t4540,t35]) ).
cnf(t4632,plain,
f(f(sFlat1,X1),f(a,a)) = a,
inference(orient,[status(thm)],[t149906]) ).
cnf(t11453,plain,
a = f(sFlat2,f(a,a)),
inference(cp,[status(thm)],[t4632,t11451]) ).
cnf(t11543,plain,
f(sFlat2,f(a,a)) = a,
inference(orient,[status(thm)],[t11453]) ).
cnf(t11544,plain,
sFlat2 = f(a,f(sFlat2,sFlat2)),
inference(cp,[status(thm)],[t11288,t11543]) ).
cnf(t11647,plain,
f(a,f(sFlat2,sFlat2)) = sFlat2,
inference(orient,[status(thm)],[t11544]) ).
cnf(t11648,plain,
f(a,a) = f(f(X1,f(a,a)),f(f(a,a),sFlat2)),
inference(cp,[status(thm)],[t10071,t11647]) ).
cnf(t25563,plain,
f(f(X1,f(a,a)),f(f(a,a),sFlat2)) = f(a,a),
inference(orient,[status(thm)],[t11648]) ).
cnf(t25564,plain,
f(a,a) = f(f(f(a,a),sFlat2),f(f(a,a),sFlat2)),
inference(cp,[status(thm)],[t25563,t11919]) ).
cnf(t38222,plain,
f(f(f(a,a),sFlat2),f(f(a,a),sFlat2)) = f(a,a),
inference(orient,[status(thm)],[t25564]) ).
cnf(t38223,plain,
f(f(a,a),sFlat2) = f(f(f(f(a,a),sFlat2),X1),f(a,a)),
inference(cp,[status(thm)],[t11288,t38222]) ).
cnf(t50,plain,
a = f(f(f(f(X1,a),sFlat5),X2),f(a,f(f(sFlat4,f(f(a,a),sFlat4)),sFlat4))),
inference(cp,[status(thm)],[t7,t48]) ).
cnf(t196,plain,
f(f(f(f(X1,a),sFlat5),X2),f(a,f(f(sFlat4,f(f(a,a),sFlat4)),sFlat4))) = a,
inference(orient,[status(thm)],[t50]) ).
cnf(t1695,plain,
f(f(f(f(X1,a),sFlat5),X2),f(a,f(f(sFlat4,f(f(a,a),sFlat4)),sFlat4))) = f(f(f(f(X1,a),sFlat5),X2),f(a,f(f(f(f(X1,a),sFlat5),X2),f(a,f(f(sFlat4,f(f(a,a),sFlat4)),sFlat4))))),
inference(cp,[status(thm)],[t1687,t196]) ).
cnf(t149890,plain,
a = f(f(f(f(X1,a),sFlat5),X2),f(a,f(f(f(f(X1,a),sFlat5),X2),f(a,f(f(sFlat4,f(f(a,a),sFlat4)),sFlat4))))),
inference(step,[status(thm)],[t1695,t196]) ).
cnf(t149891,plain,
a = f(f(f(f(X1,a),sFlat5),X2),f(a,a)),
inference(step,[status(thm)],[t149890,t196]) ).
cnf(t4038,plain,
f(f(f(f(X1,a),sFlat5),X2),f(a,a)) = a,
inference(orient,[status(thm)],[t149891]) ).
cnf(t4039,plain,
a = f(f(f(f(X1,a),f(a,X2)),X3),f(a,a)),
inference(cp,[status(thm)],[t4038,t2283]) ).
cnf(t8902,plain,
f(f(f(f(X1,a),f(a,X2)),X3),f(a,a)) = a,
inference(orient,[status(thm)],[t4039]) ).
cnf(t11650,plain,
a = f(f(f(f(X1,a),sFlat2),X2),f(a,a)),
inference(cp,[status(thm)],[t8902,t11647]) ).
cnf(t19812,plain,
f(f(f(f(X1,a),sFlat2),X2),f(a,a)) = a,
inference(orient,[status(thm)],[t11650]) ).
cnf(t150218,plain,
f(f(a,a),sFlat2) = a,
inference(step,[status(thm)],[t38223,t19812]) ).
cnf(t38273,plain,
f(f(a,a),sFlat2) = a,
inference(orient,[status(thm)],[t150218]) ).
cnf(t77097,plain,
sFlat2 = f(f(f(a,f(sFlat2,X1)),X2),f(sFlat2,sFlat2)),
inference(cp,[status(thm)],[t76576,t38273]) ).
cnf(t114418,plain,
f(f(f(a,f(sFlat2,X1)),X2),f(sFlat2,sFlat2)) = sFlat2,
inference(orient,[status(thm)],[t77097]) ).
cnf(t108588,plain,
f(sFlat3,sFlat3) = f(sFlat2,sFlat3),
inference(cp,[status(thm)],[t11919,t108575]) ).
cnf(t150823,plain,
sFlat4 = f(sFlat2,sFlat3),
inference(step,[status(thm)],[t108588,t40]) ).
cnf(t108651,plain,
f(sFlat2,sFlat3) = sFlat4,
inference(orient,[status(thm)],[t150823]) ).
cnf(t114432,plain,
sFlat2 = f(f(f(a,sFlat4),X1),f(sFlat2,sFlat2)),
inference(cp,[status(thm)],[t114418,t108651]) ).
cnf(t151014,plain,
sFlat2 = f(f(sFlat5,X1),f(sFlat2,sFlat2)),
inference(step,[status(thm)],[t114432,t48]) ).
cnf(t114544,plain,
f(f(sFlat5,X1),f(sFlat2,sFlat2)) = sFlat2,
inference(orient,[status(thm)],[t151014]) ).
cnf(t114554,plain,
f(sFlat5,sFlat5) = f(sFlat2,sFlat5),
inference(cp,[status(thm)],[t11919,t114544]) ).
cnf(t114618,plain,
f(sFlat5,sFlat5) = f(sFlat2,sFlat5),
inference(orient,[status(thm)],[t114554]) ).
cnf(t151222,plain,
sFlat5 = f(f(f(c,f(sFlat5,X1)),X2),f(sFlat2,sFlat5)),
inference(step,[status(thm)],[t77103,t114618]) ).
cnf(t149368,plain,
f(f(f(c,f(sFlat5,X1)),X2),f(sFlat2,sFlat5)) = sFlat5,
inference(orient,[status(thm)],[t151222]) ).
cnf(t1700,plain,
f(f(f(f(X1,b),sFlat3),X2),f(b,f(f(c,f(f(b,b),c)),c))) = f(f(f(f(X1,b),sFlat3),X2),f(b,f(f(f(f(X1,b),sFlat3),X2),f(b,f(f(c,f(f(b,b),c)),c))))),
inference(cp,[status(thm)],[t1687,t142]) ).
cnf(t149901,plain,
b = f(f(f(f(X1,b),sFlat3),X2),f(b,f(f(f(f(X1,b),sFlat3),X2),f(b,f(f(c,f(f(b,b),c)),c))))),
inference(step,[status(thm)],[t1700,t142]) ).
cnf(t149902,plain,
b = f(f(f(f(X1,b),sFlat3),X2),f(b,b)),
inference(step,[status(thm)],[t149901,t142]) ).
cnf(t4400,plain,
f(f(f(f(X1,b),sFlat3),X2),f(b,b)) = b,
inference(orient,[status(thm)],[t149902]) ).
cnf(t3747,plain,
sFlat4 = f(f(f(sFlat5,f(sFlat4,sFlat3)),X1),sFlat3),
inference(cp,[status(thm)],[t3736,t48]) ).
cnf(t3942,plain,
f(f(f(sFlat5,f(sFlat4,sFlat3)),X1),sFlat3) = sFlat4,
inference(orient,[status(thm)],[t3747]) ).
cnf(t4402,plain,
b = f(f(sFlat4,X1),f(b,b)),
inference(cp,[status(thm)],[t4400,t3942]) ).
cnf(t4446,plain,
f(f(sFlat4,X1),f(b,b)) = b,
inference(orient,[status(thm)],[t4402]) ).
cnf(t11499,plain,
b = f(sFlat5,f(b,b)),
inference(cp,[status(thm)],[t4446,t11497]) ).
cnf(t11595,plain,
f(sFlat5,f(b,b)) = b,
inference(orient,[status(thm)],[t11499]) ).
cnf(t11596,plain,
sFlat5 = f(b,f(sFlat5,sFlat5)),
inference(cp,[status(thm)],[t11288,t11595]) ).
cnf(t11709,plain,
f(b,f(sFlat5,sFlat5)) = sFlat5,
inference(orient,[status(thm)],[t11596]) ).
cnf(t11710,plain,
f(b,b) = f(f(X1,f(b,b)),f(f(b,b),sFlat5)),
inference(cp,[status(thm)],[t10071,t11709]) ).
cnf(t25675,plain,
f(f(X1,f(b,b)),f(f(b,b),sFlat5)) = f(b,b),
inference(orient,[status(thm)],[t11710]) ).
cnf(t25676,plain,
f(b,b) = f(f(f(b,b),sFlat5),f(f(b,b),sFlat5)),
inference(cp,[status(thm)],[t25675,t11919]) ).
cnf(t39184,plain,
f(f(f(b,b),sFlat5),f(f(b,b),sFlat5)) = f(b,b),
inference(orient,[status(thm)],[t25676]) ).
cnf(t39185,plain,
f(f(b,b),sFlat5) = f(f(f(f(b,b),sFlat5),X1),f(b,b)),
inference(cp,[status(thm)],[t11288,t39184]) ).
cnf(t11714,plain,
b = f(f(f(f(X1,b),sFlat5),X2),f(b,b)),
inference(cp,[status(thm)],[t9196,t11709]) ).
cnf(t20138,plain,
f(f(f(f(X1,b),sFlat5),X2),f(b,b)) = b,
inference(orient,[status(thm)],[t11714]) ).
cnf(t150224,plain,
f(f(b,b),sFlat5) = b,
inference(step,[status(thm)],[t39185,t20138]) ).
cnf(t39235,plain,
f(f(b,b),sFlat5) = b,
inference(orient,[status(thm)],[t150224]) ).
cnf(t77021,plain,
sFlat5 = f(f(f(b,f(sFlat5,X1)),X2),f(sFlat5,sFlat5)),
inference(cp,[status(thm)],[t76576,t39235]) ).
cnf(t92011,plain,
f(f(f(b,f(sFlat5,X1)),X2),f(sFlat5,sFlat5)) = sFlat5,
inference(orient,[status(thm)],[t77021]) ).
cnf(t96,plain,
a = f(f(f(sFlat0,sFlat5),X1),f(a,f(f(sFlat4,f(f(a,a),sFlat4)),sFlat4))),
inference(cp,[status(thm)],[t95,t48]) ).
cnf(t102,plain,
f(f(f(sFlat0,sFlat5),X1),f(a,f(f(sFlat4,f(f(a,a),sFlat4)),sFlat4))) = a,
inference(orient,[status(thm)],[t96]) ).
cnf(t1702,plain,
f(f(f(sFlat0,sFlat5),X1),f(a,f(f(sFlat4,f(f(a,a),sFlat4)),sFlat4))) = f(f(f(sFlat0,sFlat5),X1),f(a,f(f(f(sFlat0,sFlat5),X1),f(a,f(f(sFlat4,f(f(a,a),sFlat4)),sFlat4))))),
inference(cp,[status(thm)],[t1687,t102]) ).
cnf(t149839,plain,
a = f(f(f(sFlat0,sFlat5),X1),f(a,f(f(f(sFlat0,sFlat5),X1),f(a,f(f(sFlat4,f(f(a,a),sFlat4)),sFlat4))))),
inference(step,[status(thm)],[t1702,t102]) ).
cnf(t149840,plain,
a = f(f(f(sFlat0,sFlat5),X1),f(a,a)),
inference(step,[status(thm)],[t149839,t102]) ).
cnf(t1911,plain,
f(f(f(sFlat0,sFlat5),X1),f(a,a)) = a,
inference(orient,[status(thm)],[t149840]) ).
cnf(t1912,plain,
a = f(sFlat5,f(a,a)),
inference(cp,[status(thm)],[t1911,t1102]) ).
cnf(t1933,plain,
f(sFlat5,f(a,a)) = a,
inference(orient,[status(thm)],[t1912]) ).
cnf(t1936,plain,
f(sFlat5,f(a,a)) = f(sFlat5,f(a,f(f(X1,f(f(f(sFlat5,f(a,a)),f(sFlat5,f(a,a))),X1)),X1))),
inference(cp,[status(thm)],[t201,t1933]) ).
cnf(t149954,plain,
a = f(sFlat5,f(a,f(f(X1,f(f(f(sFlat5,f(a,a)),f(sFlat5,f(a,a))),X1)),X1))),
inference(step,[status(thm)],[t1936,t1933]) ).
cnf(t149955,plain,
a = f(sFlat5,f(a,f(f(X1,f(f(a,f(sFlat5,f(a,a))),X1)),X1))),
inference(step,[status(thm)],[t149954,t1933]) ).
cnf(t149956,plain,
a = f(sFlat5,f(a,f(f(X1,f(f(a,a),X1)),X1))),
inference(step,[status(thm)],[t149955,t1933]) ).
cnf(t8624,plain,
f(sFlat5,f(a,f(f(X1,f(f(a,a),X1)),X1))) = a,
inference(orient,[status(thm)],[t149956]) ).
cnf(t38285,plain,
a = f(sFlat5,f(a,f(f(sFlat2,a),sFlat2))),
inference(cp,[status(thm)],[t8624,t38273]) ).
cnf(t38518,plain,
f(sFlat5,f(a,f(f(sFlat2,a),sFlat2))) = a,
inference(orient,[status(thm)],[t38285]) ).
cnf(t92039,plain,
sFlat5 = f(f(f(b,a),X1),f(sFlat5,sFlat5)),
inference(cp,[status(thm)],[t92011,t38518]) ).
cnf(t150683,plain,
sFlat5 = f(f(sFlat0,X1),f(sFlat5,sFlat5)),
inference(step,[status(thm)],[t92039,t21]) ).
cnf(t92106,plain,
f(f(sFlat0,X1),f(sFlat5,sFlat5)) = sFlat5,
inference(orient,[status(thm)],[t150683]) ).
cnf(t92118,plain,
f(sFlat0,sFlat0) = f(sFlat5,sFlat0),
inference(cp,[status(thm)],[t11919,t92106]) ).
cnf(t150684,plain,
sFlat1 = f(sFlat5,sFlat0),
inference(step,[status(thm)],[t92118,t35]) ).
cnf(t92168,plain,
f(sFlat5,sFlat0) = sFlat1,
inference(orient,[status(thm)],[t150684]) ).
cnf(t149383,plain,
sFlat5 = f(f(f(c,sFlat1),X1),f(sFlat2,sFlat5)),
inference(cp,[status(thm)],[t149368,t92168]) ).
cnf(t151223,plain,
sFlat5 = f(f(sFlat2,X1),f(sFlat2,sFlat5)),
inference(step,[status(thm)],[t149383,t45]) ).
cnf(t149528,plain,
f(f(sFlat2,X1),f(sFlat2,sFlat5)) = sFlat5,
inference(orient,[status(thm)],[t151223]) ).
cnf(t149548,plain,
sFlat2 = f(sFlat4,f(sFlat2,sFlat5)),
inference(cp,[status(thm)],[t110054,t149528]) ).
cnf(t151035,plain,
f(sFlat4,f(sFlat2,sFlat5)) = sFlat5,
inference(step,[status(thm)],[t11497,t114618]) ).
cnf(t114687,plain,
f(sFlat4,f(sFlat2,sFlat5)) = sFlat5,
inference(rw,[status(thm)],[t151035]) ).
cnf(t114830,plain,
f(sFlat4,f(sFlat2,sFlat5)) = sFlat5,
inference(orient,[status(thm)],[t114687]) ).
cnf(t151224,plain,
sFlat2 = sFlat5,
inference(step,[status(thm)],[t149548,t114830]) ).
cnf(t149670,plain,
sFlat5 = sFlat2,
inference(orient,[status(thm)],[t151224]) ).
cnf(t151225,plain,
f(a,sFlat4) = sFlat2,
inference(step,[status(thm)],[t48,t149670]) ).
cnf(t149671,plain,
f(a,sFlat4) = sFlat2,
inference(orient,[status(thm)],[t151225]) ).
cnf(goal_0,negated_conjecture,
f(c,f(f(b,a),f(b,a))) != f(a,f(f(b,c),f(b,c))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
cnf(g0_0,plain,
f(c,f(sFlat0,f(b,a))) != f(a,f(f(b,c),f(b,c))),
inference(rw,[status(thm)],[goal_0,t21]) ).
cnf(g0_1,plain,
f(c,f(sFlat0,sFlat0)) != f(a,f(f(b,c),f(b,c))),
inference(rw,[status(thm)],[g0_0,t21]) ).
cnf(g0_2,plain,
f(c,sFlat1) != f(a,f(f(b,c),f(b,c))),
inference(rw,[status(thm)],[g0_1,t35]) ).
cnf(g0_3,plain,
sFlat2 != f(a,f(f(b,c),f(b,c))),
inference(rw,[status(thm)],[g0_2,t45]) ).
cnf(g0_4,plain,
sFlat2 != f(a,f(sFlat3,f(b,c))),
inference(rw,[status(thm)],[g0_3,t25]) ).
cnf(g0_5,plain,
sFlat2 != f(a,f(sFlat3,sFlat3)),
inference(rw,[status(thm)],[g0_4,t25]) ).
cnf(g0_6,plain,
sFlat2 != f(a,sFlat4),
inference(rw,[status(thm)],[g0_5,t40]) ).
cnf(g0_7,plain,
sFlat2 != sFlat2,
inference(rw,[status(thm)],[g0_6,t149671]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_7]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT072-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.12/5.40 % Computer : n016.cluster.edu
% 0.12/5.40 % Model : x86_64 x86_64
% 0.12/5.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/5.40 % Memory : 8046.5625MB
% 0.12/5.40 % OS : Linux 6.8.0-71-generic
% 0.12/5.40 % CPULimit : 300
% 0.12/5.40 % WCLimit : 300
% 0.12/5.40 % DateTime : Wed Sep 23 20:15:03 UTC 2026
% 0.12/5.40 % CPUTime :
% 0.16/5.40 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 109.68/21.27 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 109.68/21.27 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------