%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SYN599-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Fri Sep 25 03:35:17 PM UTC 2026
% Result : Unsatisfiable 28.63s 4.10s
% Output : Proof 28.63s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t29,axiom,
sFlat0 = f16(c21),
introduced(definition) ).
cnf(t166,plain,
f16(c21) = sFlat0,
inference(orient,[status(thm)],[t29]) ).
cnf(t30,axiom,
sFlat1 = f15(f16(c21)),
introduced(definition) ).
cnf(t9401,plain,
sFlat1 = f15(sFlat0),
inference(step,[status(thm)],[t30,t166]) ).
cnf(t173,plain,
f15(sFlat0) = sFlat1,
inference(orient,[status(thm)],[t9401]) ).
cnf(t31,axiom,
sFlat2 = f11(c23),
introduced(definition) ).
cnf(t143,plain,
f11(c23) = sFlat2,
inference(orient,[status(thm)],[t31]) ).
cnf(t32,axiom,
sFlat3 = f13(f11(c23)),
introduced(definition) ).
cnf(t9388,plain,
sFlat3 = f13(sFlat2),
inference(step,[status(thm)],[t32,t143]) ).
cnf(t153,plain,
f13(sFlat2) = sFlat3,
inference(orient,[status(thm)],[t9388]) ).
cnf(t33,axiom,
sFlat4 = f10(f13(f11(c23))),
introduced(definition) ).
cnf(t9387,plain,
sFlat4 = f10(f13(sFlat2)),
inference(step,[status(thm)],[t33,t143]) ).
cnf(t150,plain,
f10(f13(sFlat2)) = sFlat4,
inference(orient,[status(thm)],[t9387]) ).
cnf(t9389,plain,
f10(sFlat3) = sFlat4,
inference(step,[status(thm)],[t150,t153]) ).
cnf(t156,plain,
f10(sFlat3) = sFlat4,
inference(rw,[status(thm)],[t9389]) ).
cnf(t202,plain,
f10(sFlat3) = sFlat4,
inference(orient,[status(thm)],[t156]) ).
cnf(t34,axiom,
sFlat5 = f12(f10(f13(f11(c23)))),
introduced(definition) ).
cnf(t9390,plain,
sFlat5 = f12(f10(f13(sFlat2))),
inference(step,[status(thm)],[t34,t143]) ).
cnf(t9391,plain,
sFlat5 = f12(f10(sFlat3)),
inference(step,[status(thm)],[t9390,t153]) ).
cnf(t157,plain,
f12(f10(sFlat3)) = sFlat5,
inference(orient,[status(thm)],[t9391]) ).
cnf(t9432,plain,
f12(sFlat4) = sFlat5,
inference(step,[status(thm)],[t157,t202]) ).
cnf(t205,plain,
f12(sFlat4) = sFlat5,
inference(rw,[status(thm)],[t9432]) ).
cnf(t209,plain,
f12(sFlat4) = sFlat5,
inference(orient,[status(thm)],[t205]) ).
cnf(t35,axiom,
sFlat6 = f14(c22),
introduced(definition) ).
cnf(t169,plain,
f14(c22) = sFlat6,
inference(orient,[status(thm)],[t35]) ).
cnf(t36,axiom,
sFlat7 = f9(f12(f10(f13(f11(c23)))),f14(c22)),
introduced(definition) ).
cnf(t9397,plain,
sFlat7 = f9(f12(f10(f13(sFlat2))),f14(c22)),
inference(step,[status(thm)],[t36,t143]) ).
cnf(t9398,plain,
sFlat7 = f9(f12(f10(sFlat3)),f14(c22)),
inference(step,[status(thm)],[t9397,t153]) ).
cnf(t9399,plain,
sFlat7 = f9(sFlat5,f14(c22)),
inference(step,[status(thm)],[t9398,t157]) ).
cnf(t163,plain,
f9(sFlat5,f14(c22)) = sFlat7,
inference(orient,[status(thm)],[t9399]) ).
cnf(t9400,plain,
f9(sFlat5,sFlat6) = sFlat7,
inference(step,[status(thm)],[t163,t169]) ).
cnf(t172,plain,
f9(sFlat5,sFlat6) = sFlat7,
inference(rw,[status(thm)],[t9400]) ).
cnf(t212,plain,
f9(sFlat5,sFlat6) = sFlat7,
inference(orient,[status(thm)],[t172]) ).
cnf(t37,axiom,
sFlat8 = f11(f11(c23)),
introduced(definition) ).
cnf(t139,plain,
f11(f11(c23)) = sFlat8,
inference(orient,[status(thm)],[t37]) ).
cnf(t9385,plain,
f11(sFlat2) = sFlat8,
inference(step,[status(thm)],[t139,t143]) ).
cnf(t146,plain,
f11(sFlat2) = sFlat8,
inference(rw,[status(thm)],[t9385]) ).
cnf(t198,plain,
f11(sFlat2) = sFlat8,
inference(orient,[status(thm)],[t146]) ).
cnf(t38,axiom,
sFlat9 = f11(f11(f11(c23))),
introduced(definition) ).
cnf(t135,plain,
f11(f11(f11(c23))) = sFlat9,
inference(orient,[status(thm)],[t38]) ).
cnf(t9384,plain,
f11(sFlat8) = sFlat9,
inference(step,[status(thm)],[t135,t139]) ).
cnf(t142,plain,
f11(sFlat8) = sFlat9,
inference(rw,[status(thm)],[t9384]) ).
cnf(t195,plain,
f11(sFlat8) = sFlat9,
inference(orient,[status(thm)],[t142]) ).
cnf(t39,axiom,
sFlat10 = f11(f11(f11(f11(c23)))),
introduced(definition) ).
cnf(t131,plain,
f11(f11(f11(f11(c23)))) = sFlat10,
inference(orient,[status(thm)],[t39]) ).
cnf(t9383,plain,
f11(sFlat9) = sFlat10,
inference(step,[status(thm)],[t131,t135]) ).
cnf(t138,plain,
f11(sFlat9) = sFlat10,
inference(rw,[status(thm)],[t9383]) ).
cnf(t191,plain,
f11(sFlat9) = sFlat10,
inference(orient,[status(thm)],[t138]) ).
cnf(t40,axiom,
sFlat11 = f11(f11(f11(f11(f11(c23))))),
introduced(definition) ).
cnf(t127,plain,
f11(f11(f11(f11(f11(c23))))) = sFlat11,
inference(orient,[status(thm)],[t40]) ).
cnf(t9382,plain,
f11(sFlat10) = sFlat11,
inference(step,[status(thm)],[t127,t131]) ).
cnf(t134,plain,
f11(sFlat10) = sFlat11,
inference(rw,[status(thm)],[t9382]) ).
cnf(t188,plain,
f11(sFlat10) = sFlat11,
inference(orient,[status(thm)],[t134]) ).
cnf(t41,axiom,
sFlat12 = f11(f11(f11(f11(f11(f11(c23)))))),
introduced(definition) ).
cnf(t123,plain,
f11(f11(f11(f11(f11(f11(c23)))))) = sFlat12,
inference(orient,[status(thm)],[t41]) ).
cnf(t9381,plain,
f11(sFlat11) = sFlat12,
inference(step,[status(thm)],[t123,t127]) ).
cnf(t130,plain,
f11(sFlat11) = sFlat12,
inference(rw,[status(thm)],[t9381]) ).
cnf(t185,plain,
f11(sFlat11) = sFlat12,
inference(orient,[status(thm)],[t130]) ).
cnf(t42,axiom,
sFlat13 = f11(f11(f11(f11(f11(f11(f11(c23))))))),
introduced(definition) ).
cnf(t118,plain,
f11(f11(f11(f11(f11(f11(f11(c23))))))) = sFlat13,
inference(orient,[status(thm)],[t42]) ).
cnf(t9380,plain,
f11(sFlat12) = sFlat13,
inference(step,[status(thm)],[t118,t123]) ).
cnf(t126,plain,
f11(sFlat12) = sFlat13,
inference(rw,[status(thm)],[t9380]) ).
cnf(t182,plain,
f11(sFlat12) = sFlat13,
inference(orient,[status(thm)],[t126]) ).
cnf(t43,axiom,
sFlat14 = f10(f11(f11(f11(f11(f11(f11(f11(c23)))))))),
introduced(definition) ).
cnf(t9386,plain,
sFlat14 = f10(f11(f11(f11(f11(f11(f11(sFlat2))))))),
inference(step,[status(thm)],[t43,t143]) ).
cnf(t147,plain,
f10(f11(f11(f11(f11(f11(f11(sFlat2))))))) = sFlat14,
inference(orient,[status(thm)],[t9386]) ).
cnf(t9426,plain,
f10(f11(f11(f11(f11(f11(sFlat8)))))) = sFlat14,
inference(step,[status(thm)],[t147,t198]) ).
cnf(t9427,plain,
f10(f11(f11(f11(f11(sFlat9))))) = sFlat14,
inference(step,[status(thm)],[t9426,t195]) ).
cnf(t9428,plain,
f10(f11(f11(f11(sFlat10)))) = sFlat14,
inference(step,[status(thm)],[t9427,t191]) ).
cnf(t9429,plain,
f10(f11(f11(sFlat11))) = sFlat14,
inference(step,[status(thm)],[t9428,t188]) ).
cnf(t9430,plain,
f10(f11(sFlat12)) = sFlat14,
inference(step,[status(thm)],[t9429,t185]) ).
cnf(t9431,plain,
f10(sFlat13) = sFlat14,
inference(step,[status(thm)],[t9430,t182]) ).
cnf(t201,plain,
f10(sFlat13) = sFlat14,
inference(rw,[status(thm)],[t9431]) ).
cnf(t206,plain,
f10(sFlat13) = sFlat14,
inference(orient,[status(thm)],[t201]) ).
cnf(t44,axiom,
sFlat15 = f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))),
introduced(definition) ).
cnf(t9392,plain,
sFlat15 = f9(f12(f10(f13(sFlat2))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))),
inference(step,[status(thm)],[t44,t143]) ).
cnf(t9393,plain,
sFlat15 = f9(f12(f10(sFlat3)),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))),
inference(step,[status(thm)],[t9392,t153]) ).
cnf(t9394,plain,
sFlat15 = f9(sFlat5,f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))),
inference(step,[status(thm)],[t9393,t157]) ).
cnf(t9395,plain,
sFlat15 = f9(sFlat5,f10(f11(f11(f11(f11(f11(f11(sFlat2)))))))),
inference(step,[status(thm)],[t9394,t143]) ).
cnf(t9396,plain,
sFlat15 = f9(sFlat5,sFlat14),
inference(step,[status(thm)],[t9395,t147]) ).
cnf(t160,plain,
f9(sFlat5,sFlat14) = sFlat15,
inference(orient,[status(thm)],[t9396]) ).
cnf(t45,axiom,
sFlat16 = f8(f9(f12(f10(f13(f11(c23)))),f14(c22)),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23)))))))))),
introduced(definition) ).
cnf(t9402,plain,
sFlat16 = f8(f9(f12(f10(f13(sFlat2))),f14(c22)),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23)))))))))),
inference(step,[status(thm)],[t45,t143]) ).
cnf(t9403,plain,
sFlat16 = f8(f9(f12(f10(sFlat3)),f14(c22)),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23)))))))))),
inference(step,[status(thm)],[t9402,t153]) ).
cnf(t9404,plain,
sFlat16 = f8(f9(sFlat5,f14(c22)),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23)))))))))),
inference(step,[status(thm)],[t9403,t157]) ).
cnf(t9405,plain,
sFlat16 = f8(f9(sFlat5,sFlat6),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23)))))))))),
inference(step,[status(thm)],[t9404,t169]) ).
cnf(t9406,plain,
sFlat16 = f8(f9(sFlat5,sFlat6),f9(f12(f10(f13(sFlat2))),f10(f11(f11(f11(f11(f11(f11(f11(c23)))))))))),
inference(step,[status(thm)],[t9405,t143]) ).
cnf(t9407,plain,
sFlat16 = f8(f9(sFlat5,sFlat6),f9(f12(f10(sFlat3)),f10(f11(f11(f11(f11(f11(f11(f11(c23)))))))))),
inference(step,[status(thm)],[t9406,t153]) ).
cnf(t9408,plain,
sFlat16 = f8(f9(sFlat5,sFlat6),f9(sFlat5,f10(f11(f11(f11(f11(f11(f11(f11(c23)))))))))),
inference(step,[status(thm)],[t9407,t157]) ).
cnf(t9409,plain,
sFlat16 = f8(f9(sFlat5,sFlat6),f9(sFlat5,f10(f11(f11(f11(f11(f11(f11(sFlat2))))))))),
inference(step,[status(thm)],[t9408,t143]) ).
cnf(t9410,plain,
sFlat16 = f8(f9(sFlat5,sFlat6),f9(sFlat5,sFlat14)),
inference(step,[status(thm)],[t9409,t147]) ).
cnf(t9411,plain,
sFlat16 = f8(f9(sFlat5,sFlat6),sFlat15),
inference(step,[status(thm)],[t9410,t160]) ).
cnf(t176,plain,
f8(f9(sFlat5,sFlat6),sFlat15) = sFlat16,
inference(orient,[status(thm)],[t9411]) ).
cnf(t9433,plain,
f8(sFlat7,sFlat15) = sFlat16,
inference(step,[status(thm)],[t176,t212]) ).
cnf(t215,plain,
f8(sFlat7,sFlat15) = sFlat16,
inference(rw,[status(thm)],[t9433]) ).
cnf(t216,plain,
f8(sFlat7,sFlat15) = sFlat16,
inference(orient,[status(thm)],[t215]) ).
cnf(t46,axiom,
sFlat17 = p19(f15(f16(c21)),f8(f9(f12(f10(f13(f11(c23)))),f14(c22)),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))),
introduced(definition) ).
cnf(t9412,plain,
sFlat17 = p19(f15(sFlat0),f8(f9(f12(f10(f13(f11(c23)))),f14(c22)),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))),
inference(step,[status(thm)],[t46,t166]) ).
cnf(t9413,plain,
sFlat17 = p19(sFlat1,f8(f9(f12(f10(f13(f11(c23)))),f14(c22)),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))),
inference(step,[status(thm)],[t9412,t173]) ).
cnf(t9414,plain,
sFlat17 = p19(sFlat1,f8(f9(f12(f10(f13(sFlat2))),f14(c22)),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))),
inference(step,[status(thm)],[t9413,t143]) ).
cnf(t9415,plain,
sFlat17 = p19(sFlat1,f8(f9(f12(f10(sFlat3)),f14(c22)),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))),
inference(step,[status(thm)],[t9414,t153]) ).
cnf(t9416,plain,
sFlat17 = p19(sFlat1,f8(f9(sFlat5,f14(c22)),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))),
inference(step,[status(thm)],[t9415,t157]) ).
cnf(t9417,plain,
sFlat17 = p19(sFlat1,f8(f9(sFlat5,sFlat6),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))),
inference(step,[status(thm)],[t9416,t169]) ).
cnf(t9418,plain,
sFlat17 = p19(sFlat1,f8(f9(sFlat5,sFlat6),f9(f12(f10(f13(sFlat2))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))),
inference(step,[status(thm)],[t9417,t143]) ).
cnf(t9419,plain,
sFlat17 = p19(sFlat1,f8(f9(sFlat5,sFlat6),f9(f12(f10(sFlat3)),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))),
inference(step,[status(thm)],[t9418,t153]) ).
cnf(t9420,plain,
sFlat17 = p19(sFlat1,f8(f9(sFlat5,sFlat6),f9(sFlat5,f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))),
inference(step,[status(thm)],[t9419,t157]) ).
cnf(t9421,plain,
sFlat17 = p19(sFlat1,f8(f9(sFlat5,sFlat6),f9(sFlat5,f10(f11(f11(f11(f11(f11(f11(sFlat2)))))))))),
inference(step,[status(thm)],[t9420,t143]) ).
cnf(t9422,plain,
sFlat17 = p19(sFlat1,f8(f9(sFlat5,sFlat6),f9(sFlat5,sFlat14))),
inference(step,[status(thm)],[t9421,t147]) ).
cnf(t9423,plain,
sFlat17 = p19(sFlat1,f8(f9(sFlat5,sFlat6),sFlat15)),
inference(step,[status(thm)],[t9422,t160]) ).
cnf(t9424,plain,
sFlat17 = p19(sFlat1,sFlat16),
inference(step,[status(thm)],[t9423,t176]) ).
cnf(t179,plain,
p19(sFlat1,sFlat16) = sFlat17,
inference(orient,[status(thm)],[t9424]) ).
cnf(f22,negated_conjecture,
( ~ p19(X6,X7)
| ~ p7(X7,X5)
| ~ p7(X6,X4)
| p19(X4,X5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p19_23) ).
fof(f22_nnf,plain,
! [X4,X5,X6,X7] :
( ~ p19(X6,X7)
| ~ p7(X7,X5)
| ~ p7(X6,X4)
| p19(X4,X5) ),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
! [X4,X5,X6,X7] :
( ~ p19(X6,X7)
| ~ p7(X7,X5)
| ~ p7(X6,X4)
| p19(X4,X5) ),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c22,plain,
( ~ p19(X2,X3)
| ~ p7(X3,X1)
| ~ p7(X2,X0)
| p19(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
cnf(t25,plain,
ifeq(p7(X1,X2),true,ifeq(p7(X3,X4),true,ifeq(p19(X1,X3),true,p19(X2,X4),true),true),true) = true,
inference(equality_encoding,[status(esa)],[c22]) ).
cnf(t48,plain,
ifeq(p7(X1,X2),true,ifeq(p7(X3,X4),true,ifeq(p19(X1,X3),true,p19(X2,X4),true),true),true) = true,
inference(orient,[status(thm)],[t25]) ).
cnf(f2,negated_conjecture,
p7(X34,X34),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p7_3) ).
fof(f2_nnf,plain,
! [X34] : p7(X34,X34),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X34] : p7(X34,X34),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
p7(X0,X0),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t5,plain,
p7(X1,X1) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t69,plain,
p7(X1,X1) = true,
inference(orient,[status(thm)],[t5]) ).
cnf(t75,plain,
true = ifeq(true,true,ifeq(p7(X1,X2),true,ifeq(p19(X3,X1),true,p19(X3,X2),true),true),true),
inference(cp,[status(thm)],[t48,t69]) ).
cnf(t6,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t47,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t6]) ).
cnf(t9499,plain,
true = ifeq(p7(X1,X2),true,ifeq(p19(X3,X1),true,p19(X3,X2),true),true),
inference(step,[status(thm)],[t75,t47]) ).
cnf(t890,plain,
ifeq(p7(X1,X2),true,ifeq(p19(X3,X1),true,p19(X3,X2),true),true) = true,
inference(orient,[status(thm)],[t9499]) ).
cnf(t905,plain,
true = ifeq(p7(X1,sFlat16),true,ifeq(p19(sFlat1,X1),true,sFlat17,true),true),
inference(cp,[status(thm)],[t890,t179]) ).
cnf(t6916,plain,
ifeq(p7(X1,sFlat16),true,ifeq(p19(sFlat1,X1),true,sFlat17,true),true) = true,
inference(orient,[status(thm)],[t905]) ).
cnf(f28,negated_conjecture,
( ~ p18(X8)
| p19(f15(f16(X8)),f8(f9(f12(f10(f13(f11(c23)))),f14(f4(f6(X8)))),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p19_29) ).
fof(f28_nnf,plain,
! [X8] :
( ~ p18(X8)
| p19(f15(f16(X8)),f8(f9(f12(f10(f13(f11(c23)))),f14(f4(f6(X8)))),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))) ),
inference(nnf_transformation,[status(thm)],[f28]) ).
fof(f28_sk,plain,
! [X8] :
( ~ p18(X8)
| p19(f15(f16(X8)),f8(f9(f12(f10(f13(f11(c23)))),f14(f4(f6(X8)))),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))) ),
inference(skolemisation,[status(esa)],[f28_nnf]) ).
cnf(c28,plain,
( ~ p18(X0)
| p19(f15(f16(X0)),f8(f9(f12(f10(f13(f11(c23)))),f14(f4(f6(X0)))),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))) ),
inference(cnf_transformation,[status(esa)],[f28_sk]) ).
cnf(t28,plain,
ifeq(p18(X1),true,p19(f15(f16(X1)),f8(f9(f12(f10(f13(f11(c23)))),f14(f4(f6(X1)))),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))),true) = true,
inference(equality_encoding,[status(esa)],[c28]) ).
cnf(t66,plain,
ifeq(p18(X1),true,p19(f15(f16(X1)),f8(f9(f12(f10(f13(f11(c23)))),f14(f4(f6(X1)))),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))),true) = true,
inference(orient,[status(thm)],[t28]) ).
cnf(t9378,plain,
ifeq(p18(X1),true,p19(f15(f16(X1)),f8(f9(f12(f10(f13(f11(c23)))),f14(f4(f6(X1)))),f9(f12(f10(f13(f11(c23)))),f10(sFlat13)))),true) = true,
inference(step,[status(thm)],[t66,t118]) ).
cnf(t121,plain,
ifeq(p18(X1),true,p19(f15(f16(X1)),f8(f9(f12(f10(f13(f11(c23)))),f14(f4(f6(X1)))),f9(f12(f10(f13(f11(c23)))),f10(sFlat13)))),true) = true,
inference(rw,[status(thm)],[t9378]) ).
cnf(t9992,plain,
ifeq(p18(X1),true,p19(f15(f16(X1)),f8(f9(f12(f10(f13(sFlat2))),f14(f4(f6(X1)))),f9(f12(f10(f13(f11(c23)))),f10(sFlat13)))),true) = true,
inference(step,[status(thm)],[t121,t143]) ).
cnf(t9993,plain,
ifeq(p18(X1),true,p19(f15(f16(X1)),f8(f9(f12(f10(sFlat3)),f14(f4(f6(X1)))),f9(f12(f10(f13(f11(c23)))),f10(sFlat13)))),true) = true,
inference(step,[status(thm)],[t9992,t153]) ).
cnf(t9994,plain,
ifeq(p18(X1),true,p19(f15(f16(X1)),f8(f9(f12(sFlat4),f14(f4(f6(X1)))),f9(f12(f10(f13(f11(c23)))),f10(sFlat13)))),true) = true,
inference(step,[status(thm)],[t9993,t202]) ).
cnf(t9995,plain,
ifeq(p18(X1),true,p19(f15(f16(X1)),f8(f9(sFlat5,f14(f4(f6(X1)))),f9(f12(f10(f13(f11(c23)))),f10(sFlat13)))),true) = true,
inference(step,[status(thm)],[t9994,t209]) ).
cnf(t9996,plain,
ifeq(p18(X1),true,p19(f15(f16(X1)),f8(f9(sFlat5,f14(f4(f6(X1)))),f9(f12(f10(f13(sFlat2))),f10(sFlat13)))),true) = true,
inference(step,[status(thm)],[t9995,t143]) ).
cnf(t9997,plain,
ifeq(p18(X1),true,p19(f15(f16(X1)),f8(f9(sFlat5,f14(f4(f6(X1)))),f9(f12(f10(sFlat3)),f10(sFlat13)))),true) = true,
inference(step,[status(thm)],[t9996,t153]) ).
cnf(t9998,plain,
ifeq(p18(X1),true,p19(f15(f16(X1)),f8(f9(sFlat5,f14(f4(f6(X1)))),f9(f12(sFlat4),f10(sFlat13)))),true) = true,
inference(step,[status(thm)],[t9997,t202]) ).
cnf(t9999,plain,
ifeq(p18(X1),true,p19(f15(f16(X1)),f8(f9(sFlat5,f14(f4(f6(X1)))),f9(sFlat5,f10(sFlat13)))),true) = true,
inference(step,[status(thm)],[t9998,t209]) ).
cnf(t10000,plain,
ifeq(p18(X1),true,p19(f15(f16(X1)),f8(f9(sFlat5,f14(f4(f6(X1)))),f9(sFlat5,sFlat14))),true) = true,
inference(step,[status(thm)],[t9999,t206]) ).
cnf(t10001,plain,
ifeq(p18(X1),true,p19(f15(f16(X1)),f8(f9(sFlat5,f14(f4(f6(X1)))),sFlat15)),true) = true,
inference(step,[status(thm)],[t10000,t160]) ).
cnf(t8167,plain,
ifeq(p18(X1),true,p19(f15(f16(X1)),f8(f9(sFlat5,f14(f4(f6(X1)))),sFlat15)),true) = true,
inference(orient,[status(thm)],[t10001]) ).
cnf(f1,negated_conjecture,
p18(c21),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',c21_is_p18_2) ).
fof(f1_nnf,plain,
p18(c21),
inference(nnf_transformation,[status(thm)],[f1]) ).
cnf(c1,plain,
p18(c21),
inference(cnf_transformation,[status(esa)],[f1_nnf]) ).
cnf(t1,plain,
p18(c21) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t110,plain,
p18(c21) = true,
inference(orient,[status(thm)],[t1]) ).
cnf(t8168,plain,
true = ifeq(true,true,p19(f15(f16(c21)),f8(f9(sFlat5,f14(f4(f6(c21)))),sFlat15)),true),
inference(cp,[status(thm)],[t8167,t110]) ).
cnf(t10002,plain,
true = p19(f15(f16(c21)),f8(f9(sFlat5,f14(f4(f6(c21)))),sFlat15)),
inference(step,[status(thm)],[t8168,t47]) ).
cnf(t10003,plain,
true = p19(f15(sFlat0),f8(f9(sFlat5,f14(f4(f6(c21)))),sFlat15)),
inference(step,[status(thm)],[t10002,t166]) ).
cnf(t10004,plain,
true = p19(sFlat1,f8(f9(sFlat5,f14(f4(f6(c21)))),sFlat15)),
inference(step,[status(thm)],[t10003,t173]) ).
cnf(t8170,plain,
p19(sFlat1,f8(f9(sFlat5,f14(f4(f6(c21)))),sFlat15)) = true,
inference(orient,[status(thm)],[t10004]) ).
cnf(t8171,plain,
true = ifeq(p7(f8(f9(sFlat5,f14(f4(f6(c21)))),sFlat15),sFlat16),true,ifeq(true,true,sFlat17,true),true),
inference(cp,[status(thm)],[t6916,t8170]) ).
cnf(f19,negated_conjecture,
( ~ p7(X34,X36)
| ~ p7(X34,X35)
| p7(X35,X36) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p7_20) ).
fof(f19_nnf,plain,
! [X35,X36,X34] :
( ~ p7(X34,X36)
| ~ p7(X34,X35)
| p7(X35,X36) ),
inference(nnf_transformation,[status(thm)],[f19]) ).
fof(f19_sk,plain,
! [X35,X36,X34] :
( ~ p7(X34,X36)
| ~ p7(X34,X35)
| p7(X35,X36) ),
inference(skolemisation,[status(esa)],[f19_nnf]) ).
cnf(c19,plain,
( ~ p7(X2,X1)
| ~ p7(X2,X0)
| p7(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f19_sk]) ).
cnf(t22,plain,
ifeq(p7(X1,X2),true,ifeq(p7(X1,X3),true,p7(X2,X3),true),true) = true,
inference(equality_encoding,[status(esa)],[c19]) ).
cnf(t51,plain,
ifeq(p7(X1,X2),true,ifeq(p7(X1,X3),true,p7(X2,X3),true),true) = true,
inference(orient,[status(thm)],[t22]) ).
cnf(t71,plain,
true = ifeq(p7(X1,X2),true,ifeq(true,true,p7(X2,X1),true),true),
inference(cp,[status(thm)],[t51,t69]) ).
cnf(t9449,plain,
true = ifeq(p7(X1,X2),true,p7(X2,X1),true),
inference(step,[status(thm)],[t71,t47]) ).
cnf(t327,plain,
ifeq(p7(X1,X2),true,p7(X2,X1),true) = true,
inference(orient,[status(thm)],[t9449]) ).
cnf(f25,negated_conjecture,
( ~ p7(X44,X46)
| ~ p7(X43,X45)
| p7(f8(X43,X44),f8(X45,X46)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p7_26) ).
fof(f25_nnf,plain,
! [X43,X44,X45,X46] :
( ~ p7(X44,X46)
| ~ p7(X43,X45)
| p7(f8(X43,X44),f8(X45,X46)) ),
inference(nnf_transformation,[status(thm)],[f25]) ).
fof(f25_sk,plain,
! [X43,X44,X45,X46] :
( ~ p7(X44,X46)
| ~ p7(X43,X45)
| p7(f8(X43,X44),f8(X45,X46)) ),
inference(skolemisation,[status(esa)],[f25_nnf]) ).
cnf(c25,plain,
( ~ p7(X1,X3)
| ~ p7(X0,X2)
| p7(f8(X0,X1),f8(X2,X3)) ),
inference(cnf_transformation,[status(esa)],[f25_sk]) ).
cnf(t24,plain,
ifeq(p7(X1,X2),true,ifeq(p7(X3,X4),true,p7(f8(X1,X3),f8(X2,X4)),true),true) = true,
inference(equality_encoding,[status(esa)],[c25]) ).
cnf(t50,plain,
ifeq(p7(X1,X2),true,ifeq(p7(X3,X4),true,p7(f8(X1,X3),f8(X2,X4)),true),true) = true,
inference(orient,[status(thm)],[t24]) ).
cnf(t80,plain,
true = ifeq(p7(X1,X2),true,ifeq(true,true,p7(f8(X1,X3),f8(X2,X3)),true),true),
inference(cp,[status(thm)],[t50,t69]) ).
cnf(t9659,plain,
true = ifeq(p7(X1,X2),true,p7(f8(X1,X3),f8(X2,X3)),true),
inference(step,[status(thm)],[t80,t47]) ).
cnf(t3068,plain,
ifeq(p7(X1,X2),true,p7(f8(X1,X3),f8(X2,X3)),true) = true,
inference(orient,[status(thm)],[t9659]) ).
cnf(t3124,plain,
true = ifeq(p7(sFlat7,X1),true,p7(sFlat16,f8(X1,sFlat15)),true),
inference(cp,[status(thm)],[t3068,t216]) ).
cnf(t3672,plain,
ifeq(p7(sFlat7,X1),true,p7(sFlat16,f8(X1,sFlat15)),true) = true,
inference(orient,[status(thm)],[t3124]) ).
cnf(f24,negated_conjecture,
( ~ p7(X47,X49)
| ~ p3(X48,X50)
| p7(f9(X47,X48),f9(X49,X50)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p7_25) ).
fof(f24_nnf,plain,
! [X47,X48,X49,X50] :
( ~ p7(X47,X49)
| ~ p3(X48,X50)
| p7(f9(X47,X48),f9(X49,X50)) ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [X47,X48,X49,X50] :
( ~ p7(X47,X49)
| ~ p3(X48,X50)
| p7(f9(X47,X48),f9(X49,X50)) ),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c24,plain,
( ~ p7(X0,X2)
| ~ p3(X1,X3)
| p7(f9(X0,X1),f9(X2,X3)) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
cnf(t23,plain,
ifeq(p3(X1,X2),true,ifeq(p7(X3,X4),true,p7(f9(X3,X1),f9(X4,X2)),true),true) = true,
inference(equality_encoding,[status(esa)],[c24]) ).
cnf(t53,plain,
ifeq(p3(X1,X2),true,ifeq(p7(X3,X4),true,p7(f9(X3,X1),f9(X4,X2)),true),true) = true,
inference(orient,[status(thm)],[t23]) ).
cnf(t77,plain,
true = ifeq(p3(X1,X2),true,ifeq(true,true,p7(f9(X3,X1),f9(X3,X2)),true),true),
inference(cp,[status(thm)],[t53,t69]) ).
cnf(t9558,plain,
true = ifeq(p3(X1,X2),true,p7(f9(X3,X1),f9(X3,X2)),true),
inference(step,[status(thm)],[t77,t47]) ).
cnf(t1608,plain,
ifeq(p3(X1,X2),true,p7(f9(X3,X1),f9(X3,X2)),true) = true,
inference(orient,[status(thm)],[t9558]) ).
cnf(f21,negated_conjecture,
( ~ p3(X18,X20)
| ~ p3(X18,X19)
| p3(X19,X20) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p3_22) ).
fof(f21_nnf,plain,
! [X19,X20,X18] :
( ~ p3(X18,X20)
| ~ p3(X18,X19)
| p3(X19,X20) ),
inference(nnf_transformation,[status(thm)],[f21]) ).
fof(f21_sk,plain,
! [X19,X20,X18] :
( ~ p3(X18,X20)
| ~ p3(X18,X19)
| p3(X19,X20) ),
inference(skolemisation,[status(esa)],[f21_nnf]) ).
cnf(c21,plain,
( ~ p3(X2,X1)
| ~ p3(X2,X0)
| p3(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f21_sk]) ).
cnf(t20,plain,
ifeq(p3(X1,X2),true,ifeq(p3(X1,X3),true,p3(X2,X3),true),true) = true,
inference(equality_encoding,[status(esa)],[c21]) ).
cnf(t54,plain,
ifeq(p3(X1,X2),true,ifeq(p3(X1,X3),true,p3(X2,X3),true),true) = true,
inference(orient,[status(thm)],[t20]) ).
cnf(f4,negated_conjecture,
p3(X18,X18),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p3_5) ).
fof(f4_nnf,plain,
! [X18] : p3(X18,X18),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X18] : p3(X18,X18),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
p3(X0,X0),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(t3,plain,
p3(X1,X1) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(t83,plain,
p3(X1,X1) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(t86,plain,
true = ifeq(p3(X1,X2),true,ifeq(true,true,p3(X2,X1),true),true),
inference(cp,[status(thm)],[t54,t83]) ).
cnf(t9453,plain,
true = ifeq(p3(X1,X2),true,p3(X2,X1),true),
inference(step,[status(thm)],[t86,t47]) ).
cnf(t359,plain,
ifeq(p3(X1,X2),true,p3(X2,X1),true) = true,
inference(orient,[status(thm)],[t9453]) ).
cnf(f14,negated_conjecture,
( ~ p3(X27,X28)
| p3(f14(X27),f14(X28)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p3_15) ).
fof(f14_nnf,plain,
! [X27,X28] :
( ~ p3(X27,X28)
| p3(f14(X27),f14(X28)) ),
inference(nnf_transformation,[status(thm)],[f14]) ).
fof(f14_sk,plain,
! [X27,X28] :
( ~ p3(X27,X28)
| p3(f14(X27),f14(X28)) ),
inference(skolemisation,[status(esa)],[f14_nnf]) ).
cnf(c14,plain,
( ~ p3(X0,X1)
| p3(f14(X0),f14(X1)) ),
inference(cnf_transformation,[status(esa)],[f14_sk]) ).
cnf(t12,plain,
ifeq(p3(X1,X2),true,p3(f14(X1),f14(X2)),true) = true,
inference(equality_encoding,[status(esa)],[c14]) ).
cnf(t59,plain,
ifeq(p3(X1,X2),true,p3(f14(X1),f14(X2)),true) = true,
inference(orient,[status(thm)],[t12]) ).
cnf(f6,negated_conjecture,
p3(f4(f6(c21)),c22),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',p3_7) ).
fof(f6_nnf,plain,
p3(f4(f6(c21)),c22),
inference(nnf_transformation,[status(thm)],[f6]) ).
cnf(c6,plain,
p3(f4(f6(c21)),c22),
inference(cnf_transformation,[status(esa)],[f6_nnf]) ).
cnf(t7,plain,
p3(f4(f6(c21)),c22) = true,
inference(equality_encoding,[status(esa)],[c6]) ).
cnf(t89,plain,
p3(f4(f6(c21)),c22) = true,
inference(orient,[status(thm)],[t7]) ).
cnf(t90,plain,
true = ifeq(true,true,p3(f14(f4(f6(c21))),f14(c22)),true),
inference(cp,[status(thm)],[t59,t89]) ).
cnf(t9434,plain,
true = p3(f14(f4(f6(c21))),f14(c22)),
inference(step,[status(thm)],[t90,t47]) ).
cnf(t9435,plain,
true = p3(f14(f4(f6(c21))),sFlat6),
inference(step,[status(thm)],[t9434,t169]) ).
cnf(t219,plain,
p3(f14(f4(f6(c21))),sFlat6) = true,
inference(orient,[status(thm)],[t9435]) ).
cnf(t366,plain,
true = ifeq(true,true,p3(sFlat6,f14(f4(f6(c21)))),true),
inference(cp,[status(thm)],[t359,t219]) ).
cnf(t9455,plain,
true = p3(sFlat6,f14(f4(f6(c21)))),
inference(step,[status(thm)],[t366,t47]) ).
cnf(t387,plain,
p3(sFlat6,f14(f4(f6(c21)))) = true,
inference(orient,[status(thm)],[t9455]) ).
cnf(t1676,plain,
true = ifeq(true,true,p7(f9(X1,sFlat6),f9(X1,f14(f4(f6(c21))))),true),
inference(cp,[status(thm)],[t1608,t387]) ).
cnf(t9561,plain,
true = p7(f9(X1,sFlat6),f9(X1,f14(f4(f6(c21))))),
inference(step,[status(thm)],[t1676,t47]) ).
cnf(t1725,plain,
p7(f9(X1,sFlat6),f9(X1,f14(f4(f6(c21))))) = true,
inference(orient,[status(thm)],[t9561]) ).
cnf(t1726,plain,
true = p7(sFlat7,f9(sFlat5,f14(f4(f6(c21))))),
inference(cp,[status(thm)],[t1725,t212]) ).
cnf(t1742,plain,
p7(sFlat7,f9(sFlat5,f14(f4(f6(c21))))) = true,
inference(orient,[status(thm)],[t1726]) ).
cnf(t3673,plain,
true = ifeq(true,true,p7(sFlat16,f8(f9(sFlat5,f14(f4(f6(c21)))),sFlat15)),true),
inference(cp,[status(thm)],[t3672,t1742]) ).
cnf(t9699,plain,
true = p7(sFlat16,f8(f9(sFlat5,f14(f4(f6(c21)))),sFlat15)),
inference(step,[status(thm)],[t3673,t47]) ).
cnf(t3674,plain,
p7(sFlat16,f8(f9(sFlat5,f14(f4(f6(c21)))),sFlat15)) = true,
inference(orient,[status(thm)],[t9699]) ).
cnf(t3675,plain,
true = ifeq(true,true,p7(f8(f9(sFlat5,f14(f4(f6(c21)))),sFlat15),sFlat16),true),
inference(cp,[status(thm)],[t327,t3674]) ).
cnf(t9700,plain,
true = p7(f8(f9(sFlat5,f14(f4(f6(c21)))),sFlat15),sFlat16),
inference(step,[status(thm)],[t3675,t47]) ).
cnf(t3692,plain,
p7(f8(f9(sFlat5,f14(f4(f6(c21)))),sFlat15),sFlat16) = true,
inference(orient,[status(thm)],[t9700]) ).
cnf(t10005,plain,
true = ifeq(true,true,ifeq(true,true,sFlat17,true),true),
inference(step,[status(thm)],[t8171,t3692]) ).
cnf(t10006,plain,
true = ifeq(true,true,sFlat17,true),
inference(step,[status(thm)],[t10005,t47]) ).
cnf(t10007,plain,
true = sFlat17,
inference(step,[status(thm)],[t10006,t47]) ).
cnf(t8179,plain,
true = sFlat17,
inference(orient,[status(thm)],[t10007]) ).
cnf(f26,negated_conjecture,
~ p19(f15(f16(c21)),f8(f9(f12(f10(f13(f11(c23)))),f14(c22)),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',not_p19_27) ).
fof(f26_nnf,plain,
~ p19(f15(f16(c21)),f8(f9(f12(f10(f13(f11(c23)))),f14(c22)),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))),
inference(nnf_transformation,[status(thm)],[f26]) ).
fof(f26_sk,plain,
~ p19(f15(f16(c21)),f8(f9(f12(f10(f13(f11(c23)))),f14(c22)),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))),
inference(skolemisation,[status(esa)],[f26_nnf]) ).
cnf(c26,plain,
~ p19(f15(f16(c21)),f8(f9(f12(f10(f13(f11(c23)))),f14(c22)),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))),
inference(cnf_transformation,[status(esa)],[f26_sk]) ).
cnf(goal_0,negated_conjecture,
p19(f15(f16(c21)),f8(f9(f12(f10(f13(f11(c23)))),f14(c22)),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))) != true,
inference(equality_encoding,[status(esa)],[c26]) ).
cnf(g0_0,plain,
p19(f15(sFlat0),f8(f9(f12(f10(f13(f11(c23)))),f14(c22)),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))) != true,
inference(rw,[status(thm)],[goal_0,t166]) ).
cnf(g0_1,plain,
p19(sFlat1,f8(f9(f12(f10(f13(f11(c23)))),f14(c22)),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))) != true,
inference(rw,[status(thm)],[g0_0,t173]) ).
cnf(g0_2,plain,
p19(sFlat1,f8(f9(f12(f10(f13(sFlat2))),f14(c22)),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))) != true,
inference(rw,[status(thm)],[g0_1,t143]) ).
cnf(g0_3,plain,
p19(sFlat1,f8(f9(f12(f10(sFlat3)),f14(c22)),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))) != true,
inference(rw,[status(thm)],[g0_2,t153]) ).
cnf(g0_4,plain,
p19(sFlat1,f8(f9(f12(sFlat4),f14(c22)),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))) != true,
inference(rw,[status(thm)],[g0_3,t202]) ).
cnf(g0_5,plain,
p19(sFlat1,f8(f9(sFlat5,f14(c22)),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))) != true,
inference(rw,[status(thm)],[g0_4,t209]) ).
cnf(g0_6,plain,
p19(sFlat1,f8(f9(sFlat5,sFlat6),f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))) != true,
inference(rw,[status(thm)],[g0_5,t169]) ).
cnf(g0_7,plain,
p19(sFlat1,f8(sFlat7,f9(f12(f10(f13(f11(c23)))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))) != true,
inference(rw,[status(thm)],[g0_6,t212]) ).
cnf(g0_8,plain,
p19(sFlat1,f8(sFlat7,f9(f12(f10(f13(sFlat2))),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))) != true,
inference(rw,[status(thm)],[g0_7,t143]) ).
cnf(g0_9,plain,
p19(sFlat1,f8(sFlat7,f9(f12(f10(sFlat3)),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))) != true,
inference(rw,[status(thm)],[g0_8,t153]) ).
cnf(g0_10,plain,
p19(sFlat1,f8(sFlat7,f9(f12(sFlat4),f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))) != true,
inference(rw,[status(thm)],[g0_9,t202]) ).
cnf(g0_11,plain,
p19(sFlat1,f8(sFlat7,f9(sFlat5,f10(f11(f11(f11(f11(f11(f11(f11(c23))))))))))) != true,
inference(rw,[status(thm)],[g0_10,t209]) ).
cnf(g0_12,plain,
p19(sFlat1,f8(sFlat7,f9(sFlat5,f10(f11(f11(f11(f11(f11(f11(sFlat2)))))))))) != true,
inference(rw,[status(thm)],[g0_11,t143]) ).
cnf(g0_13,plain,
p19(sFlat1,f8(sFlat7,f9(sFlat5,f10(f11(f11(f11(f11(f11(sFlat8))))))))) != true,
inference(rw,[status(thm)],[g0_12,t198]) ).
cnf(g0_14,plain,
p19(sFlat1,f8(sFlat7,f9(sFlat5,f10(f11(f11(f11(f11(sFlat9)))))))) != true,
inference(rw,[status(thm)],[g0_13,t195]) ).
cnf(g0_15,plain,
p19(sFlat1,f8(sFlat7,f9(sFlat5,f10(f11(f11(f11(sFlat10))))))) != true,
inference(rw,[status(thm)],[g0_14,t191]) ).
cnf(g0_16,plain,
p19(sFlat1,f8(sFlat7,f9(sFlat5,f10(f11(f11(sFlat11)))))) != true,
inference(rw,[status(thm)],[g0_15,t188]) ).
cnf(g0_17,plain,
p19(sFlat1,f8(sFlat7,f9(sFlat5,f10(f11(sFlat12))))) != true,
inference(rw,[status(thm)],[g0_16,t185]) ).
cnf(g0_18,plain,
p19(sFlat1,f8(sFlat7,f9(sFlat5,f10(sFlat13)))) != true,
inference(rw,[status(thm)],[g0_17,t182]) ).
cnf(g0_19,plain,
p19(sFlat1,f8(sFlat7,f9(sFlat5,sFlat14))) != true,
inference(rw,[status(thm)],[g0_18,t206]) ).
cnf(g0_20,plain,
p19(sFlat1,f8(sFlat7,sFlat15)) != true,
inference(rw,[status(thm)],[g0_19,t160]) ).
cnf(g0_21,plain,
p19(sFlat1,sFlat16) != true,
inference(rw,[status(thm)],[g0_20,t216]) ).
cnf(g0_22,plain,
sFlat17 != true,
inference(rw,[status(thm)],[g0_21,t179]) ).
cnf(g0_23,plain,
sFlat17 != sFlat17,
inference(rw,[status(thm)],[g0_22,t8179]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_23]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SYN599-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.38 % Computer : n015.cluster.edu
% 0.09/0.38 % Model : x86_64 x86_64
% 0.09/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.38 % Memory : 8046.5625MB
% 0.09/0.38 % OS : Linux 6.8.0-71-generic
% 0.09/0.38 % CPULimit : 300
% 0.09/0.38 % WCLimit : 300
% 0.09/0.38 % DateTime : Fri Sep 25 01:54:13 UTC 2026
% 0.09/0.39 % CPUTime :
% 0.09/0.39 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 28.63/4.10 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 28.63/4.10 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------