%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : COL006-2 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n005.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:01:41 PM UTC 2026
% Result : Unsatisfiable 19.71s 2.94s
% Output : Proof 19.71s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(f0,axiom,
apply(apply(apply(s,X),Y),Z) = apply(apply(X,Z),apply(Y,Z)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s_definition) ).
fof(f0_nnf,plain,
! [X,Y,Z] : apply(apply(apply(s,X),Y),Z) = apply(apply(X,Z),apply(Y,Z)),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,Y,Z] : apply(apply(apply(s,X),Y),Z) = apply(apply(X,Z),apply(Y,Z)),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
apply(apply(apply(s,X0),X1),X2) = apply(apply(X0,X2),apply(X1,X2)),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t3,plain,
apply(apply(apply(s,X1),X2),X3) = apply(apply(X1,X3),apply(X2,X3)),
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t22,plain,
apply(apply(X1,X2),apply(X3,X2)) = apply(apply(apply(s,X1),X3),X2),
inference(orient,[status(thm)],[t3]) ).
cnf(t15,axiom,
sFlat11 = apply(s,apply(k,s)),
introduced(definition) ).
cnf(t64,plain,
apply(s,apply(k,s)) = sFlat11,
inference(orient,[status(thm)],[t15]) ).
cnf(t14,axiom,
sFlat10 = apply(k,s),
introduced(definition) ).
cnf(t83,plain,
apply(k,s) = sFlat10,
inference(orient,[status(thm)],[t14]) ).
cnf(t18391,plain,
apply(s,sFlat10) = sFlat11,
inference(step,[status(thm)],[t64,t83]) ).
cnf(t85,plain,
apply(s,sFlat10) = sFlat11,
inference(rw,[status(thm)],[t18391]) ).
cnf(t101,plain,
apply(s,sFlat10) = sFlat11,
inference(orient,[status(thm)],[t85]) ).
cnf(t102,plain,
apply(apply(sFlat10,X1),apply(X2,X1)) = apply(apply(sFlat11,X2),X1),
inference(cp,[status(thm)],[t22,t101]) ).
cnf(f1,axiom,
apply(apply(k,X),Y) = X,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',k_definition) ).
fof(f1_nnf,plain,
! [X,Y] : apply(apply(k,X),Y) = X,
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,Y] : apply(apply(k,X),Y) = X,
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
apply(apply(k,X0),X1) = X0,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t0,plain,
apply(apply(k,X1),X2) = X1,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t20,plain,
apply(apply(k,X1),X2) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t84,plain,
s = apply(sFlat10,X1),
inference(cp,[status(thm)],[t20,t83]) ).
cnf(t96,plain,
apply(sFlat10,X1) = s,
inference(orient,[status(thm)],[t84]) ).
cnf(t18414,plain,
apply(s,apply(X2,X1)) = apply(apply(sFlat11,X2),X1),
inference(step,[status(thm)],[t102,t96]) ).
cnf(t140,plain,
apply(apply(sFlat11,X1),X2) = apply(s,apply(X1,X2)),
inference(orient,[status(thm)],[t18414]) ).
cnf(t16,axiom,
sFlat12 = apply(apply(s,apply(k,s)),k),
introduced(definition) ).
cnf(t44,plain,
apply(apply(s,apply(k,s)),k) = sFlat12,
inference(orient,[status(thm)],[t16]) ).
cnf(t18384,plain,
apply(sFlat11,k) = sFlat12,
inference(step,[status(thm)],[t44,t64]) ).
cnf(t68,plain,
apply(sFlat11,k) = sFlat12,
inference(rw,[status(thm)],[t18384]) ).
cnf(t93,plain,
apply(sFlat11,k) = sFlat12,
inference(orient,[status(thm)],[t68]) ).
cnf(t142,plain,
apply(s,apply(k,X1)) = apply(sFlat12,X1),
inference(cp,[status(thm)],[t140,t93]) ).
cnf(t147,plain,
apply(s,apply(k,X1)) = apply(sFlat12,X1),
inference(orient,[status(thm)],[t142]) ).
cnf(t28,plain,
apply(apply(X1,X2),apply(apply(X3,X1),X2)) = apply(apply(apply(apply(s,s),X3),X1),X2),
inference(cp,[status(thm)],[t22,t22]) ).
cnf(t6,axiom,
sFlat2 = apply(s,apply(apply(s,k),k)),
introduced(definition) ).
cnf(t5,axiom,
sFlat1 = apply(apply(s,k),k),
introduced(definition) ).
cnf(t51,plain,
apply(apply(s,k),k) = sFlat1,
inference(orient,[status(thm)],[t5]) ).
cnf(t18379,plain,
sFlat2 = apply(s,sFlat1),
inference(step,[status(thm)],[t6,t51]) ).
cnf(t54,plain,
apply(s,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t18379]) ).
cnf(t55,plain,
apply(apply(sFlat1,X1),apply(X2,X1)) = apply(apply(sFlat2,X2),X1),
inference(cp,[status(thm)],[t22,t54]) ).
cnf(t4,axiom,
sFlat0 = apply(s,k),
introduced(definition) ).
cnf(t72,plain,
apply(s,k) = sFlat0,
inference(orient,[status(thm)],[t4]) ).
cnf(t73,plain,
apply(apply(k,X1),apply(X2,X1)) = apply(apply(sFlat0,X2),X1),
inference(cp,[status(thm)],[t22,t72]) ).
cnf(t18411,plain,
X1 = apply(apply(sFlat0,X2),X1),
inference(step,[status(thm)],[t73,t20]) ).
cnf(t119,plain,
apply(apply(sFlat0,X1),X2) = X2,
inference(orient,[status(thm)],[t18411]) ).
cnf(t18386,plain,
apply(sFlat0,k) = sFlat1,
inference(step,[status(thm)],[t51,t72]) ).
cnf(t74,plain,
apply(sFlat0,k) = sFlat1,
inference(rw,[status(thm)],[t18386]) ).
cnf(t94,plain,
apply(sFlat0,k) = sFlat1,
inference(orient,[status(thm)],[t74]) ).
cnf(t121,plain,
X1 = apply(sFlat1,X1),
inference(cp,[status(thm)],[t119,t94]) ).
cnf(t126,plain,
apply(sFlat1,X1) = X1,
inference(orient,[status(thm)],[t121]) ).
cnf(t18425,plain,
apply(X1,apply(X2,X1)) = apply(apply(sFlat2,X2),X1),
inference(step,[status(thm)],[t55,t126]) ).
cnf(t183,plain,
apply(X1,apply(X2,X1)) = apply(apply(sFlat2,X2),X1),
inference(orient,[status(thm)],[t18425]) ).
cnf(t196,plain,
apply(apply(sFlat2,sFlat1),X1) = apply(X1,X1),
inference(cp,[status(thm)],[t183,t126]) ).
cnf(t7,axiom,
sFlat3 = apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)),
introduced(definition) ).
cnf(t31,plain,
apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)) = sFlat3,
inference(orient,[status(thm)],[t7]) ).
cnf(t18377,plain,
apply(apply(s,sFlat1),apply(apply(s,k),k)) = sFlat3,
inference(step,[status(thm)],[t31,t51]) ).
cnf(t18378,plain,
apply(apply(s,sFlat1),sFlat1) = sFlat3,
inference(step,[status(thm)],[t18377,t51]) ).
cnf(t53,plain,
apply(apply(s,sFlat1),sFlat1) = sFlat3,
inference(rw,[status(thm)],[t18378]) ).
cnf(t18404,plain,
apply(sFlat2,sFlat1) = sFlat3,
inference(step,[status(thm)],[t53,t54]) ).
cnf(t109,plain,
apply(sFlat2,sFlat1) = sFlat3,
inference(orient,[status(thm)],[t18404]) ).
cnf(t18426,plain,
apply(sFlat3,X1) = apply(X1,X1),
inference(step,[status(thm)],[t196,t109]) ).
cnf(t215,plain,
apply(sFlat3,X1) = apply(X1,X1),
inference(orient,[status(thm)],[t18426]) ).
cnf(t18561,plain,
apply(apply(X1,X2),apply(apply(X3,X1),X2)) = apply(apply(apply(apply(sFlat3,s),X3),X1),X2),
inference(step,[status(thm)],[t28,t215]) ).
cnf(t10,axiom,
sFlat6 = apply(s,s),
introduced(definition) ).
cnf(t69,plain,
apply(s,s) = sFlat6,
inference(orient,[status(thm)],[t10]) ).
cnf(t243,plain,
apply(s,s) = sFlat6,
inference(rw,[status(thm)],[t69]) ).
cnf(t18428,plain,
apply(sFlat3,s) = sFlat6,
inference(step,[status(thm)],[t243,t215]) ).
cnf(t261,plain,
apply(sFlat3,s) = sFlat6,
inference(orient,[status(thm)],[t18428]) ).
cnf(t18562,plain,
apply(apply(X1,X2),apply(apply(X3,X1),X2)) = apply(apply(apply(sFlat6,X3),X1),X2),
inference(step,[status(thm)],[t18561,t261]) ).
cnf(t2871,plain,
apply(apply(X1,X2),apply(apply(X3,X1),X2)) = apply(apply(apply(sFlat6,X3),X1),X2),
inference(orient,[status(thm)],[t18562]) ).
cnf(t3278,plain,
apply(apply(apply(sFlat6,sFlat0),X1),X2) = apply(apply(X1,X2),X2),
inference(cp,[status(thm)],[t2871,t119]) ).
cnf(t11,axiom,
sFlat7 = apply(apply(s,s),apply(s,k)),
introduced(definition) ).
cnf(t47,plain,
apply(apply(s,s),apply(s,k)) = sFlat7,
inference(orient,[status(thm)],[t11]) ).
cnf(t18385,plain,
apply(sFlat6,apply(s,k)) = sFlat7,
inference(step,[status(thm)],[t47,t69]) ).
cnf(t71,plain,
apply(sFlat6,apply(s,k)) = sFlat7,
inference(rw,[status(thm)],[t18385]) ).
cnf(t18406,plain,
apply(sFlat6,sFlat0) = sFlat7,
inference(step,[status(thm)],[t71,t72]) ).
cnf(t111,plain,
apply(sFlat6,sFlat0) = sFlat7,
inference(orient,[status(thm)],[t18406]) ).
cnf(t18853,plain,
apply(apply(sFlat7,X1),X2) = apply(apply(X1,X2),X2),
inference(step,[status(thm)],[t3278,t111]) ).
cnf(t9078,plain,
apply(apply(sFlat7,X1),X2) = apply(apply(X1,X2),X2),
inference(orient,[status(thm)],[t18853]) ).
cnf(t130,plain,
apply(apply(apply(s,X1),sFlat1),X2) = apply(apply(X1,X2),X2),
inference(cp,[status(thm)],[t22,t126]) ).
cnf(t13917,plain,
apply(apply(apply(s,X1),sFlat1),X2) = apply(apply(X1,X2),X2),
inference(orient,[status(thm)],[t130]) ).
cnf(t13935,plain,
apply(apply(s,X1),X1) = apply(apply(apply(sFlat3,s),sFlat1),X1),
inference(cp,[status(thm)],[t13917,t215]) ).
cnf(t19187,plain,
apply(apply(sFlat7,s),X1) = apply(apply(apply(sFlat3,s),sFlat1),X1),
inference(step,[status(thm)],[t13935,t9078]) ).
cnf(t19188,plain,
apply(apply(sFlat7,s),X1) = apply(apply(sFlat6,sFlat1),X1),
inference(step,[status(thm)],[t19187,t261]) ).
cnf(t14198,plain,
apply(apply(sFlat7,s),X1) = apply(apply(sFlat6,sFlat1),X1),
inference(orient,[status(thm)],[t19188]) ).
cnf(t3130,plain,
apply(apply(apply(sFlat6,X1),s),k) = apply(sFlat0,apply(apply(X1,s),k)),
inference(cp,[status(thm)],[t2871,t72]) ).
cnf(t229,plain,
apply(apply(apply(s,X1),X2),X1) = apply(apply(sFlat3,X1),apply(X2,X1)),
inference(cp,[status(thm)],[t22,t215]) ).
cnf(t1316,plain,
apply(apply(apply(s,X1),X2),X1) = apply(apply(sFlat3,X1),apply(X2,X1)),
inference(orient,[status(thm)],[t229]) ).
cnf(t1337,plain,
apply(apply(sFlat3,s),apply(X1,s)) = apply(apply(apply(sFlat3,s),X1),s),
inference(cp,[status(thm)],[t1316,t215]) ).
cnf(t18487,plain,
apply(sFlat6,apply(X1,s)) = apply(apply(apply(sFlat3,s),X1),s),
inference(step,[status(thm)],[t1337,t261]) ).
cnf(t18488,plain,
apply(sFlat6,apply(X1,s)) = apply(apply(sFlat6,X1),s),
inference(step,[status(thm)],[t18487,t261]) ).
cnf(t1346,plain,
apply(apply(sFlat6,X1),s) = apply(sFlat6,apply(X1,s)),
inference(orient,[status(thm)],[t18488]) ).
cnf(t18755,plain,
apply(apply(sFlat6,apply(X1,s)),k) = apply(sFlat0,apply(apply(X1,s),k)),
inference(step,[status(thm)],[t3130,t1346]) ).
cnf(t6989,plain,
apply(apply(sFlat6,apply(X1,s)),k) = apply(sFlat0,apply(apply(X1,s),k)),
inference(orient,[status(thm)],[t18755]) ).
cnf(t7048,plain,
apply(sFlat0,apply(apply(apply(k,X1),s),k)) = apply(apply(sFlat6,X1),k),
inference(cp,[status(thm)],[t6989,t20]) ).
cnf(t18774,plain,
apply(sFlat0,apply(X1,k)) = apply(apply(sFlat6,X1),k),
inference(step,[status(thm)],[t7048,t20]) ).
cnf(t7081,plain,
apply(apply(sFlat6,X1),k) = apply(sFlat0,apply(X1,k)),
inference(orient,[status(thm)],[t18774]) ).
cnf(t3131,plain,
apply(apply(apply(sFlat6,X1),s),sFlat1) = apply(sFlat2,apply(apply(X1,s),sFlat1)),
inference(cp,[status(thm)],[t2871,t54]) ).
cnf(t18776,plain,
apply(apply(sFlat6,apply(X1,s)),sFlat1) = apply(sFlat2,apply(apply(X1,s),sFlat1)),
inference(step,[status(thm)],[t3131,t1346]) ).
cnf(t7088,plain,
apply(apply(sFlat6,apply(X1,s)),sFlat1) = apply(sFlat2,apply(apply(X1,s),sFlat1)),
inference(orient,[status(thm)],[t18776]) ).
cnf(t7144,plain,
apply(sFlat2,apply(apply(apply(k,X1),s),sFlat1)) = apply(apply(sFlat6,X1),sFlat1),
inference(cp,[status(thm)],[t7088,t20]) ).
cnf(t18789,plain,
apply(sFlat2,apply(X1,sFlat1)) = apply(apply(sFlat6,X1),sFlat1),
inference(step,[status(thm)],[t7144,t20]) ).
cnf(t7201,plain,
apply(apply(sFlat6,X1),sFlat1) = apply(sFlat2,apply(X1,sFlat1)),
inference(orient,[status(thm)],[t18789]) ).
cnf(t8,axiom,
sFlat4 = apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k))),
introduced(definition) ).
cnf(t18387,plain,
sFlat4 = apply(k,apply(apply(s,apply(sFlat0,k)),apply(apply(s,k),k))),
inference(step,[status(thm)],[t8,t72]) ).
cnf(t18388,plain,
sFlat4 = apply(k,apply(apply(s,apply(sFlat0,k)),apply(sFlat0,k))),
inference(step,[status(thm)],[t18387,t72]) ).
cnf(t75,plain,
apply(k,apply(apply(s,apply(sFlat0,k)),apply(sFlat0,k))) = sFlat4,
inference(orient,[status(thm)],[t18388]) ).
cnf(t18399,plain,
apply(k,apply(apply(s,sFlat1),apply(sFlat0,k))) = sFlat4,
inference(step,[status(thm)],[t75,t94]) ).
cnf(t18400,plain,
apply(k,apply(sFlat2,apply(sFlat0,k))) = sFlat4,
inference(step,[status(thm)],[t18399,t54]) ).
cnf(t18401,plain,
apply(k,apply(sFlat2,sFlat1)) = sFlat4,
inference(step,[status(thm)],[t18400,t94]) ).
cnf(t95,plain,
apply(k,apply(sFlat2,sFlat1)) = sFlat4,
inference(rw,[status(thm)],[t18401]) ).
cnf(t18412,plain,
apply(k,sFlat3) = sFlat4,
inference(step,[status(thm)],[t95,t109]) ).
cnf(t131,plain,
apply(k,sFlat3) = sFlat4,
inference(orient,[status(thm)],[t18412]) ).
cnf(t148,plain,
apply(sFlat12,sFlat3) = apply(s,sFlat4),
inference(cp,[status(thm)],[t147,t131]) ).
cnf(t9,axiom,
sFlat5 = apply(s,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))),
introduced(definition) ).
cnf(t18380,plain,
sFlat5 = apply(s,apply(k,apply(apply(s,sFlat1),apply(apply(s,k),k)))),
inference(step,[status(thm)],[t9,t51]) ).
cnf(t18381,plain,
sFlat5 = apply(s,apply(k,apply(sFlat2,apply(apply(s,k),k)))),
inference(step,[status(thm)],[t18380,t54]) ).
cnf(t18382,plain,
sFlat5 = apply(s,apply(k,apply(sFlat2,sFlat1))),
inference(step,[status(thm)],[t18381,t51]) ).
cnf(t56,plain,
apply(s,apply(k,apply(sFlat2,sFlat1))) = sFlat5,
inference(orient,[status(thm)],[t18382]) ).
cnf(t18405,plain,
apply(s,apply(k,sFlat3)) = sFlat5,
inference(step,[status(thm)],[t56,t109]) ).
cnf(t110,plain,
apply(s,apply(k,sFlat3)) = sFlat5,
inference(rw,[status(thm)],[t18405]) ).
cnf(t18413,plain,
apply(s,sFlat4) = sFlat5,
inference(step,[status(thm)],[t110,t131]) ).
cnf(t138,plain,
apply(s,sFlat4) = sFlat5,
inference(orient,[status(thm)],[t18413]) ).
cnf(t18415,plain,
apply(sFlat12,sFlat3) = sFlat5,
inference(step,[status(thm)],[t148,t138]) ).
cnf(t154,plain,
apply(sFlat12,sFlat3) = sFlat5,
inference(orient,[status(thm)],[t18415]) ).
cnf(t12,axiom,
sFlat8 = apply(k,apply(apply(s,s),apply(s,k))),
introduced(definition) ).
cnf(t18389,plain,
sFlat8 = apply(k,apply(sFlat6,apply(s,k))),
inference(step,[status(thm)],[t12,t69]) ).
cnf(t18390,plain,
sFlat8 = apply(k,apply(sFlat6,sFlat0)),
inference(step,[status(thm)],[t18389,t72]) ).
cnf(t79,plain,
apply(k,apply(sFlat6,sFlat0)) = sFlat8,
inference(orient,[status(thm)],[t18390]) ).
cnf(t18409,plain,
apply(k,sFlat7) = sFlat8,
inference(step,[status(thm)],[t79,t111]) ).
cnf(t114,plain,
apply(k,sFlat7) = sFlat8,
inference(rw,[status(thm)],[t18409]) ).
cnf(t115,plain,
apply(k,sFlat7) = sFlat8,
inference(orient,[status(thm)],[t114]) ).
cnf(t150,plain,
apply(sFlat12,sFlat7) = apply(s,sFlat8),
inference(cp,[status(thm)],[t147,t115]) ).
cnf(t13,axiom,
sFlat9 = apply(s,apply(k,apply(apply(s,s),apply(s,k)))),
introduced(definition) ).
cnf(t18383,plain,
sFlat9 = apply(s,apply(k,sFlat7)),
inference(step,[status(thm)],[t13,t47]) ).
cnf(t60,plain,
apply(s,apply(k,sFlat7)) = sFlat9,
inference(orient,[status(thm)],[t18383]) ).
cnf(t18410,plain,
apply(s,sFlat8) = sFlat9,
inference(step,[status(thm)],[t60,t115]) ).
cnf(t116,plain,
apply(s,sFlat8) = sFlat9,
inference(rw,[status(thm)],[t18410]) ).
cnf(t117,plain,
apply(s,sFlat8) = sFlat9,
inference(orient,[status(thm)],[t116]) ).
cnf(t18417,plain,
apply(sFlat12,sFlat7) = sFlat9,
inference(step,[status(thm)],[t150,t117]) ).
cnf(t156,plain,
apply(sFlat12,sFlat7) = sFlat9,
inference(orient,[status(thm)],[t18417]) ).
cnf(t149,plain,
apply(sFlat12,s) = apply(s,sFlat10),
inference(cp,[status(thm)],[t147,t83]) ).
cnf(t18416,plain,
apply(sFlat12,s) = sFlat11,
inference(step,[status(thm)],[t149,t101]) ).
cnf(t155,plain,
apply(sFlat12,s) = sFlat11,
inference(orient,[status(thm)],[t18416]) ).
cnf(t17,axiom,
sFlat13 = apply(apply(s,apply(k,apply(apply(s,s),apply(s,k)))),apply(apply(s,apply(k,s)),k)),
introduced(definition) ).
cnf(t39,plain,
apply(apply(s,apply(k,apply(apply(s,s),apply(s,k)))),apply(apply(s,apply(k,s)),k)) = sFlat13,
inference(orient,[status(thm)],[t17]) ).
cnf(t18376,plain,
apply(apply(s,apply(k,apply(apply(s,s),apply(s,k)))),sFlat12) = sFlat13,
inference(step,[status(thm)],[t39,t44]) ).
cnf(t46,plain,
apply(apply(s,apply(k,apply(apply(s,s),apply(s,k)))),sFlat12) = sFlat13,
inference(rw,[status(thm)],[t18376]) ).
cnf(t18749,plain,
apply(apply(sFlat12,apply(apply(s,s),apply(s,k))),sFlat12) = sFlat13,
inference(step,[status(thm)],[t46,t147]) ).
cnf(t18750,plain,
apply(apply(sFlat12,apply(apply(sFlat3,s),apply(s,k))),sFlat12) = sFlat13,
inference(step,[status(thm)],[t18749,t215]) ).
cnf(t18751,plain,
apply(apply(sFlat12,apply(sFlat6,apply(s,k))),sFlat12) = sFlat13,
inference(step,[status(thm)],[t18750,t261]) ).
cnf(t18752,plain,
apply(apply(sFlat12,apply(sFlat6,sFlat0)),sFlat12) = sFlat13,
inference(step,[status(thm)],[t18751,t72]) ).
cnf(t18753,plain,
apply(apply(sFlat12,sFlat7),sFlat12) = sFlat13,
inference(step,[status(thm)],[t18752,t111]) ).
cnf(t18754,plain,
apply(sFlat9,sFlat12) = sFlat13,
inference(step,[status(thm)],[t18753,t156]) ).
cnf(t6848,plain,
apply(sFlat9,sFlat12) = sFlat13,
inference(orient,[status(thm)],[t18754]) ).
cnf(t18,axiom,
sFlat14 = apply(apply(s,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))),apply(apply(s,apply(k,apply(apply(s,s),apply(s,k)))),apply(apply(s,apply(k,s)),k))),
introduced(definition) ).
cnf(t18374,plain,
sFlat14 = apply(apply(s,apply(k,sFlat3)),apply(apply(s,apply(k,apply(apply(s,s),apply(s,k)))),apply(apply(s,apply(k,s)),k))),
inference(step,[status(thm)],[t18,t31]) ).
cnf(t35,plain,
apply(apply(s,apply(k,sFlat3)),apply(apply(s,apply(k,apply(apply(s,s),apply(s,k)))),apply(apply(s,apply(k,s)),k))) = sFlat14,
inference(orient,[status(thm)],[t18374]) ).
cnf(t18375,plain,
apply(apply(s,apply(k,sFlat3)),sFlat13) = sFlat14,
inference(step,[status(thm)],[t35,t39]) ).
cnf(t43,plain,
apply(apply(s,apply(k,sFlat3)),sFlat13) = sFlat14,
inference(rw,[status(thm)],[t18375]) ).
cnf(t18420,plain,
apply(apply(sFlat12,sFlat3),sFlat13) = sFlat14,
inference(step,[status(thm)],[t43,t147]) ).
cnf(t18421,plain,
apply(sFlat5,sFlat13) = sFlat14,
inference(step,[status(thm)],[t18420,t154]) ).
cnf(t169,plain,
apply(sFlat5,sFlat13) = sFlat14,
inference(orient,[status(thm)],[t18421]) ).
cnf(t19,axiom,
sFlat15 = fixed_point(apply(apply(s,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))),apply(apply(s,apply(k,apply(apply(s,s),apply(s,k)))),apply(apply(s,apply(k,s)),k)))),
introduced(definition) ).
cnf(t18392,plain,
sFlat15 = fixed_point(apply(apply(s,apply(k,apply(apply(s,apply(sFlat0,k)),apply(apply(s,k),k)))),apply(apply(s,apply(k,apply(apply(s,s),apply(s,k)))),apply(apply(s,apply(k,s)),k)))),
inference(step,[status(thm)],[t19,t72]) ).
cnf(t18393,plain,
sFlat15 = fixed_point(apply(apply(s,apply(k,apply(apply(s,apply(sFlat0,k)),apply(sFlat0,k)))),apply(apply(s,apply(k,apply(apply(s,s),apply(s,k)))),apply(apply(s,apply(k,s)),k)))),
inference(step,[status(thm)],[t18392,t72]) ).
cnf(t18394,plain,
sFlat15 = fixed_point(apply(apply(s,sFlat4),apply(apply(s,apply(k,apply(apply(s,s),apply(s,k)))),apply(apply(s,apply(k,s)),k)))),
inference(step,[status(thm)],[t18393,t75]) ).
cnf(t18395,plain,
sFlat15 = fixed_point(apply(apply(s,sFlat4),apply(apply(s,apply(k,apply(sFlat6,apply(s,k)))),apply(apply(s,apply(k,s)),k)))),
inference(step,[status(thm)],[t18394,t69]) ).
cnf(t18396,plain,
sFlat15 = fixed_point(apply(apply(s,sFlat4),apply(apply(s,apply(k,apply(sFlat6,sFlat0))),apply(apply(s,apply(k,s)),k)))),
inference(step,[status(thm)],[t18395,t72]) ).
cnf(t18397,plain,
sFlat15 = fixed_point(apply(apply(s,sFlat4),apply(apply(s,sFlat8),apply(apply(s,apply(k,s)),k)))),
inference(step,[status(thm)],[t18396,t79]) ).
cnf(t18398,plain,
sFlat15 = fixed_point(apply(apply(s,sFlat4),apply(apply(s,sFlat8),apply(apply(s,sFlat10),k)))),
inference(step,[status(thm)],[t18397,t83]) ).
cnf(t91,plain,
fixed_point(apply(apply(s,sFlat4),apply(apply(s,sFlat8),apply(apply(s,sFlat10),k)))) = sFlat15,
inference(orient,[status(thm)],[t18398]) ).
cnf(t18402,plain,
fixed_point(apply(apply(s,sFlat4),apply(apply(s,sFlat8),apply(sFlat11,k)))) = sFlat15,
inference(step,[status(thm)],[t91,t101]) ).
cnf(t18403,plain,
fixed_point(apply(apply(s,sFlat4),apply(apply(s,sFlat8),sFlat12))) = sFlat15,
inference(step,[status(thm)],[t18402,t93]) ).
cnf(t103,plain,
fixed_point(apply(apply(s,sFlat4),apply(apply(s,sFlat8),sFlat12))) = sFlat15,
inference(rw,[status(thm)],[t18403]) ).
cnf(t18894,plain,
fixed_point(apply(sFlat5,apply(apply(s,sFlat8),sFlat12))) = sFlat15,
inference(step,[status(thm)],[t103,t138]) ).
cnf(t18895,plain,
fixed_point(apply(sFlat5,apply(sFlat9,sFlat12))) = sFlat15,
inference(step,[status(thm)],[t18894,t117]) ).
cnf(t18896,plain,
fixed_point(apply(sFlat5,sFlat13)) = sFlat15,
inference(step,[status(thm)],[t18895,t6848]) ).
cnf(t18897,plain,
fixed_point(sFlat14) = sFlat15,
inference(step,[status(thm)],[t18896,t169]) ).
cnf(t10180,plain,
fixed_point(sFlat14) = sFlat15,
inference(orient,[status(thm)],[t18897]) ).
cnf(f2,axiom,
( fixed_point(Strong_fixed_point)
| apply(Strong_fixed_point,fixed_pt) != apply(fixed_pt,apply(Strong_fixed_point,fixed_pt)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',strong_fixed_point) ).
fof(f2_nnf,plain,
! [Strong_fixed_point] :
( fixed_point(Strong_fixed_point)
| apply(Strong_fixed_point,fixed_pt) != apply(fixed_pt,apply(Strong_fixed_point,fixed_pt)) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [Strong_fixed_point] :
( fixed_point(Strong_fixed_point)
| apply(Strong_fixed_point,fixed_pt) != apply(fixed_pt,apply(Strong_fixed_point,fixed_pt)) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( fixed_point(X0)
| apply(X0,fixed_pt) != apply(fixed_pt,apply(X0,fixed_pt)) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t2,plain,
ifeq(apply(X1,fixed_pt),apply(fixed_pt,apply(X1,fixed_pt)),fixed_point(X1),true) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t86,plain,
ifeq(apply(X1,fixed_pt),apply(fixed_pt,apply(X1,fixed_pt)),fixed_point(X1),true) = true,
inference(orient,[status(thm)],[t2]) ).
cnf(t230,plain,
apply(apply(apply(s,X1),X2),X2) = apply(apply(X1,X2),apply(sFlat3,X2)),
inference(cp,[status(thm)],[t22,t215]) ).
cnf(t1451,plain,
apply(apply(apply(s,X1),X2),X2) = apply(apply(X1,X2),apply(sFlat3,X2)),
inference(orient,[status(thm)],[t230]) ).
cnf(t9572,plain,
apply(apply(apply(s,X1),X2),X2) = apply(apply(X1,X2),apply(sFlat3,X2)),
inference(rw,[status(thm)],[t1451]) ).
cnf(t19309,plain,
apply(apply(sFlat7,apply(s,X1)),X2) = apply(apply(X1,X2),apply(sFlat3,X2)),
inference(step,[status(thm)],[t9572,t9078]) ).
cnf(t17496,plain,
apply(apply(sFlat7,apply(s,X1)),X2) = apply(apply(X1,X2),apply(sFlat3,X2)),
inference(orient,[status(thm)],[t19309]) ).
cnf(t17509,plain,
apply(apply(apply(k,X1),X2),apply(sFlat3,X2)) = apply(apply(sFlat7,apply(sFlat12,X1)),X2),
inference(cp,[status(thm)],[t17496,t147]) ).
cnf(t19310,plain,
apply(X1,apply(sFlat3,X2)) = apply(apply(sFlat7,apply(sFlat12,X1)),X2),
inference(step,[status(thm)],[t17509,t20]) ).
cnf(t118,plain,
apply(apply(sFlat8,X1),apply(X2,X1)) = apply(apply(sFlat9,X2),X1),
inference(cp,[status(thm)],[t22,t117]) ).
cnf(t80,plain,
apply(sFlat6,sFlat0) = apply(sFlat8,X1),
inference(cp,[status(thm)],[t20,t79]) ).
cnf(t104,plain,
apply(sFlat8,X1) = apply(sFlat6,sFlat0),
inference(orient,[status(thm)],[t80]) ).
cnf(t18407,plain,
apply(sFlat8,X1) = sFlat7,
inference(step,[status(thm)],[t104,t111]) ).
cnf(t112,plain,
apply(sFlat8,X1) = sFlat7,
inference(orient,[status(thm)],[t18407]) ).
cnf(t18418,plain,
apply(sFlat7,apply(X2,X1)) = apply(apply(sFlat9,X2),X1),
inference(step,[status(thm)],[t118,t112]) ).
cnf(t157,plain,
apply(apply(sFlat9,X1),X2) = apply(sFlat7,apply(X1,X2)),
inference(orient,[status(thm)],[t18418]) ).
cnf(t6849,plain,
apply(sFlat7,apply(sFlat12,X1)) = apply(sFlat13,X1),
inference(cp,[status(thm)],[t157,t6848]) ).
cnf(t6855,plain,
apply(sFlat7,apply(sFlat12,X1)) = apply(sFlat13,X1),
inference(orient,[status(thm)],[t6849]) ).
cnf(t19311,plain,
apply(X1,apply(sFlat3,X2)) = apply(apply(sFlat13,X1),X2),
inference(step,[status(thm)],[t19310,t6855]) ).
cnf(t18016,plain,
apply(apply(sFlat13,X1),X2) = apply(X1,apply(sFlat3,X2)),
inference(orient,[status(thm)],[t19311]) ).
cnf(t18025,plain,
apply(X1,apply(sFlat3,apply(sFlat13,X1))) = apply(sFlat3,apply(sFlat13,X1)),
inference(cp,[status(thm)],[t18016,t215]) ).
cnf(t139,plain,
apply(apply(sFlat4,X1),apply(X2,X1)) = apply(apply(sFlat5,X2),X1),
inference(cp,[status(thm)],[t22,t138]) ).
cnf(t132,plain,
sFlat3 = apply(sFlat4,X1),
inference(cp,[status(thm)],[t20,t131]) ).
cnf(t133,plain,
apply(sFlat4,X1) = sFlat3,
inference(orient,[status(thm)],[t132]) ).
cnf(t18419,plain,
apply(sFlat3,apply(X2,X1)) = apply(apply(sFlat5,X2),X1),
inference(step,[status(thm)],[t139,t133]) ).
cnf(t163,plain,
apply(apply(sFlat5,X1),X2) = apply(sFlat3,apply(X1,X2)),
inference(orient,[status(thm)],[t18419]) ).
cnf(t170,plain,
apply(sFlat3,apply(sFlat13,X1)) = apply(sFlat14,X1),
inference(cp,[status(thm)],[t163,t169]) ).
cnf(t171,plain,
apply(sFlat3,apply(sFlat13,X1)) = apply(sFlat14,X1),
inference(orient,[status(thm)],[t170]) ).
cnf(t19323,plain,
apply(X1,apply(sFlat14,X1)) = apply(sFlat3,apply(sFlat13,X1)),
inference(step,[status(thm)],[t18025,t171]) ).
cnf(t19324,plain,
apply(X1,apply(sFlat14,X1)) = apply(sFlat14,X1),
inference(step,[status(thm)],[t19323,t171]) ).
cnf(t18116,plain,
apply(X1,apply(sFlat14,X1)) = apply(sFlat14,X1),
inference(orient,[status(thm)],[t19324]) ).
cnf(t18238,plain,
true = ifeq(apply(sFlat14,fixed_pt),apply(sFlat14,fixed_pt),fixed_point(sFlat14),true),
inference(cp,[status(thm)],[t86,t18116]) ).
cnf(t1,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t21,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t1]) ).
cnf(t19325,plain,
true = fixed_point(sFlat14),
inference(step,[status(thm)],[t18238,t21]) ).
cnf(t19326,plain,
true = sFlat15,
inference(step,[status(thm)],[t19325,t10180]) ).
cnf(t18365,plain,
true = sFlat15,
inference(orient,[status(thm)],[t19326]) ).
cnf(f3,negated_conjecture,
~ fixed_point(apply(apply(s,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))),apply(apply(s,apply(k,apply(apply(s,s),apply(s,k)))),apply(apply(s,apply(k,s)),k)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_strong_fixed_point) ).
fof(f3_nnf,plain,
~ fixed_point(apply(apply(s,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))),apply(apply(s,apply(k,apply(apply(s,s),apply(s,k)))),apply(apply(s,apply(k,s)),k)))),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
~ fixed_point(apply(apply(s,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))),apply(apply(s,apply(k,apply(apply(s,s),apply(s,k)))),apply(apply(s,apply(k,s)),k)))),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
~ fixed_point(apply(apply(s,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))),apply(apply(s,apply(k,apply(apply(s,s),apply(s,k)))),apply(apply(s,apply(k,s)),k)))),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(goal_0,negated_conjecture,
fixed_point(apply(apply(s,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))),apply(apply(s,apply(k,apply(apply(s,s),apply(s,k)))),apply(apply(s,apply(k,s)),k)))) != true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(g0_0,plain,
fixed_point(apply(apply(sFlat12,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k))),apply(apply(s,apply(k,apply(apply(s,s),apply(s,k)))),apply(apply(s,apply(k,s)),k)))) != true,
inference(rw,[status(thm)],[goal_0,t147]) ).
cnf(g0_1,plain,
fixed_point(apply(apply(sFlat12,apply(apply(sFlat7,s),apply(apply(s,k),k))),apply(apply(s,apply(k,apply(apply(s,s),apply(s,k)))),apply(apply(s,apply(k,s)),k)))) != true,
inference(rw,[status(thm)],[g0_0,t9078]) ).
cnf(g0_2,plain,
fixed_point(apply(apply(sFlat12,apply(apply(sFlat6,sFlat1),apply(apply(s,k),k))),apply(apply(s,apply(k,apply(apply(s,s),apply(s,k)))),apply(apply(s,apply(k,s)),k)))) != true,
inference(rw,[status(thm)],[g0_1,t14198]) ).
cnf(g0_3,plain,
fixed_point(apply(apply(sFlat12,apply(apply(sFlat6,sFlat1),apply(apply(sFlat7,s),k))),apply(apply(s,apply(k,apply(apply(s,s),apply(s,k)))),apply(apply(s,apply(k,s)),k)))) != true,
inference(rw,[status(thm)],[g0_2,t9078]) ).
cnf(g0_4,plain,
fixed_point(apply(apply(sFlat12,apply(apply(sFlat6,sFlat1),apply(apply(sFlat6,sFlat1),k))),apply(apply(s,apply(k,apply(apply(s,s),apply(s,k)))),apply(apply(s,apply(k,s)),k)))) != true,
inference(rw,[status(thm)],[g0_3,t14198]) ).
cnf(g0_5,plain,
fixed_point(apply(apply(sFlat12,apply(apply(sFlat6,sFlat1),apply(sFlat0,apply(sFlat1,k)))),apply(apply(s,apply(k,apply(apply(s,s),apply(s,k)))),apply(apply(s,apply(k,s)),k)))) != true,
inference(rw,[status(thm)],[g0_4,t7081]) ).
cnf(g0_6,plain,
fixed_point(apply(apply(sFlat12,apply(apply(sFlat6,sFlat1),apply(sFlat0,k))),apply(apply(s,apply(k,apply(apply(s,s),apply(s,k)))),apply(apply(s,apply(k,s)),k)))) != true,
inference(rw,[status(thm)],[g0_5,t126]) ).
cnf(g0_7,plain,
fixed_point(apply(apply(sFlat12,apply(apply(sFlat6,sFlat1),sFlat1)),apply(apply(s,apply(k,apply(apply(s,s),apply(s,k)))),apply(apply(s,apply(k,s)),k)))) != true,
inference(rw,[status(thm)],[g0_6,t94]) ).
cnf(g0_8,plain,
fixed_point(apply(apply(sFlat12,apply(sFlat2,apply(sFlat1,sFlat1))),apply(apply(s,apply(k,apply(apply(s,s),apply(s,k)))),apply(apply(s,apply(k,s)),k)))) != true,
inference(rw,[status(thm)],[g0_7,t7201]) ).
cnf(g0_9,plain,
fixed_point(apply(apply(sFlat12,apply(sFlat2,sFlat1)),apply(apply(s,apply(k,apply(apply(s,s),apply(s,k)))),apply(apply(s,apply(k,s)),k)))) != true,
inference(rw,[status(thm)],[g0_8,t126]) ).
cnf(g0_10,plain,
fixed_point(apply(apply(sFlat12,sFlat3),apply(apply(s,apply(k,apply(apply(s,s),apply(s,k)))),apply(apply(s,apply(k,s)),k)))) != true,
inference(rw,[status(thm)],[g0_9,t109]) ).
cnf(g0_11,plain,
fixed_point(apply(sFlat5,apply(apply(s,apply(k,apply(apply(s,s),apply(s,k)))),apply(apply(s,apply(k,s)),k)))) != true,
inference(rw,[status(thm)],[g0_10,t154]) ).
cnf(g0_12,plain,
fixed_point(apply(sFlat5,apply(apply(sFlat12,apply(apply(s,s),apply(s,k))),apply(apply(s,apply(k,s)),k)))) != true,
inference(rw,[status(thm)],[g0_11,t147]) ).
cnf(g0_13,plain,
fixed_point(apply(sFlat5,apply(apply(sFlat12,apply(apply(sFlat3,s),apply(s,k))),apply(apply(s,apply(k,s)),k)))) != true,
inference(rw,[status(thm)],[g0_12,t215]) ).
cnf(g0_14,plain,
fixed_point(apply(sFlat5,apply(apply(sFlat12,apply(sFlat6,apply(s,k))),apply(apply(s,apply(k,s)),k)))) != true,
inference(rw,[status(thm)],[g0_13,t261]) ).
cnf(g0_15,plain,
fixed_point(apply(sFlat5,apply(apply(sFlat12,apply(sFlat6,sFlat0)),apply(apply(s,apply(k,s)),k)))) != true,
inference(rw,[status(thm)],[g0_14,t72]) ).
cnf(g0_16,plain,
fixed_point(apply(sFlat5,apply(apply(sFlat12,sFlat7),apply(apply(s,apply(k,s)),k)))) != true,
inference(rw,[status(thm)],[g0_15,t111]) ).
cnf(g0_17,plain,
fixed_point(apply(sFlat5,apply(sFlat9,apply(apply(s,apply(k,s)),k)))) != true,
inference(rw,[status(thm)],[g0_16,t156]) ).
cnf(g0_18,plain,
fixed_point(apply(sFlat5,apply(sFlat9,apply(apply(sFlat12,s),k)))) != true,
inference(rw,[status(thm)],[g0_17,t147]) ).
cnf(g0_19,plain,
fixed_point(apply(sFlat5,apply(sFlat9,apply(sFlat11,k)))) != true,
inference(rw,[status(thm)],[g0_18,t155]) ).
cnf(g0_20,plain,
fixed_point(apply(sFlat5,apply(sFlat9,sFlat12))) != true,
inference(rw,[status(thm)],[g0_19,t93]) ).
cnf(g0_21,plain,
fixed_point(apply(sFlat5,sFlat13)) != true,
inference(rw,[status(thm)],[g0_20,t6848]) ).
cnf(g0_22,plain,
fixed_point(sFlat14) != true,
inference(rw,[status(thm)],[g0_21,t169]) ).
cnf(g0_23,plain,
sFlat15 != true,
inference(rw,[status(thm)],[g0_22,t10180]) ).
cnf(g0_24,plain,
sFlat15 != sFlat15,
inference(rw,[status(thm)],[g0_23,t18365]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_24]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : COL006-2 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n005.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Fri Sep 25 07:10:32 UTC 2026
% 0.02/0.36 % CPUTime :
% 0.02/0.36 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 19.71/2.94 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 19.71/2.94 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------