%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : COL006-3 : TPTP v9.3.1. Released v1.0.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:01:42 PM UTC 2026
% Result : Unsatisfiable 18.24s 7.79s
% Output : Proof 18.24s
% Verified :
% SZS Type : Refutation
% Derivation depth : 48
% Number of leaves : 17
% Syntax : Number of formulae : 196 ( 192 unt; 0 def)
% Number of atoms : 200 ( 191 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 17 ( 13 ~; 4 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 9 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 16 con; 0-4 aty)
% Number of variables : 159 ( 8 sgn 12 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f0,axiom,
apply(apply(apply(s,X),Y),Z) = apply(apply(X,Z),apply(Y,Z)),
file('/export/starexec/sandbox2/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(t19,plain,
apply(apply(X1,X2),apply(X3,X2)) = apply(apply(apply(s,X1),X3),X2),
inference(orient,[status(thm)],[t3]) ).
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/sandbox2/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(t62,plain,
ifeq(apply(X1,fixed_pt),apply(fixed_pt,apply(X1,fixed_pt)),fixed_point(X1),true) = true,
inference(orient,[status(thm)],[t2]) ).
cnf(t12,axiom,
sFlat8 = apply(apply(s,apply(k,s)),k),
introduced(definition) ).
cnf(t32,plain,
apply(apply(s,apply(k,s)),k) = sFlat8,
inference(orient,[status(thm)],[t12]) ).
cnf(t33,plain,
apply(apply(apply(k,s),X1),apply(k,X1)) = apply(sFlat8,X1),
inference(cp,[status(thm)],[t19,t32]) ).
cnf(f1,axiom,
apply(apply(k,X),Y) = X,
file('/export/starexec/sandbox2/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(t17,plain,
apply(apply(k,X1),X2) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t1481,plain,
apply(s,apply(k,X1)) = apply(sFlat8,X1),
inference(step,[status(thm)],[t33,t17]) ).
cnf(t92,plain,
apply(s,apply(k,X1)) = apply(sFlat8,X1),
inference(orient,[status(thm)],[t1481]) ).
cnf(t97,plain,
apply(apply(apply(k,X1),X2),apply(X3,X2)) = apply(apply(apply(sFlat8,X1),X3),X2),
inference(cp,[status(thm)],[t19,t92]) ).
cnf(t1491,plain,
apply(X1,apply(X3,X2)) = apply(apply(apply(sFlat8,X1),X3),X2),
inference(step,[status(thm)],[t97,t17]) ).
cnf(t176,plain,
apply(apply(apply(sFlat8,X1),X2),X3) = apply(X1,apply(X2,X3)),
inference(orient,[status(thm)],[t1491]) ).
cnf(t13,axiom,
sFlat9 = apply(s,apply(apply(s,apply(k,s)),k)),
introduced(definition) ).
cnf(t10,axiom,
sFlat6 = apply(k,s),
introduced(definition) ).
cnf(t42,plain,
apply(k,s) = sFlat6,
inference(orient,[status(thm)],[t10]) ).
cnf(t1457,plain,
sFlat9 = apply(s,apply(apply(s,sFlat6),k)),
inference(step,[status(thm)],[t13,t42]) ).
cnf(t45,plain,
apply(s,apply(apply(s,sFlat6),k)) = sFlat9,
inference(orient,[status(thm)],[t1457]) ).
cnf(t11,axiom,
sFlat7 = apply(s,apply(k,s)),
introduced(definition) ).
cnf(t1463,plain,
sFlat7 = apply(s,sFlat6),
inference(step,[status(thm)],[t11,t42]) ).
cnf(t56,plain,
apply(s,sFlat6) = sFlat7,
inference(orient,[status(thm)],[t1463]) ).
cnf(t1464,plain,
apply(s,apply(sFlat7,k)) = sFlat9,
inference(step,[status(thm)],[t45,t56]) ).
cnf(t58,plain,
apply(s,apply(sFlat7,k)) = sFlat9,
inference(rw,[status(thm)],[t1464]) ).
cnf(t1456,plain,
apply(apply(s,sFlat6),k) = sFlat8,
inference(step,[status(thm)],[t32,t42]) ).
cnf(t44,plain,
apply(apply(s,sFlat6),k) = sFlat8,
inference(rw,[status(thm)],[t1456]) ).
cnf(t1478,plain,
apply(sFlat7,k) = sFlat8,
inference(step,[status(thm)],[t44,t56]) ).
cnf(t84,plain,
apply(sFlat7,k) = sFlat8,
inference(orient,[status(thm)],[t1478]) ).
cnf(t1480,plain,
apply(s,sFlat8) = sFlat9,
inference(step,[status(thm)],[t58,t84]) ).
cnf(t90,plain,
apply(s,sFlat8) = sFlat9,
inference(orient,[status(thm)],[t1480]) ).
cnf(t91,plain,
apply(apply(sFlat8,X1),apply(X2,X1)) = apply(apply(sFlat9,X2),X1),
inference(cp,[status(thm)],[t19,t90]) ).
cnf(t185,plain,
apply(apply(sFlat8,X1),apply(X2,X1)) = apply(apply(sFlat9,X2),X1),
inference(orient,[status(thm)],[t91]) ).
cnf(t8,axiom,
sFlat4 = apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k))),
introduced(definition) ).
cnf(t5,axiom,
sFlat1 = apply(apply(s,k),k),
introduced(definition) ).
cnf(t35,plain,
apply(apply(s,k),k) = sFlat1,
inference(orient,[status(thm)],[t5]) ).
cnf(t1454,plain,
sFlat4 = apply(k,apply(apply(s,sFlat1),apply(apply(s,k),k))),
inference(step,[status(thm)],[t8,t35]) ).
cnf(t1455,plain,
sFlat4 = apply(k,apply(apply(s,sFlat1),sFlat1)),
inference(step,[status(thm)],[t1454,t35]) ).
cnf(t38,plain,
apply(k,apply(apply(s,sFlat1),sFlat1)) = sFlat4,
inference(orient,[status(thm)],[t1455]) ).
cnf(t6,axiom,
sFlat2 = apply(s,apply(apply(s,k),k)),
introduced(definition) ).
cnf(t1458,plain,
sFlat2 = apply(s,sFlat1),
inference(step,[status(thm)],[t6,t35]) ).
cnf(t49,plain,
apply(s,sFlat1) = sFlat2,
inference(orient,[status(thm)],[t1458]) ).
cnf(t1459,plain,
apply(k,apply(sFlat2,sFlat1)) = sFlat4,
inference(step,[status(thm)],[t38,t49]) ).
cnf(t51,plain,
apply(k,apply(sFlat2,sFlat1)) = sFlat4,
inference(rw,[status(thm)],[t1459]) ).
cnf(t7,axiom,
sFlat3 = apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)),
introduced(definition) ).
cnf(t24,plain,
apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)) = sFlat3,
inference(orient,[status(thm)],[t7]) ).
cnf(t1452,plain,
apply(apply(s,sFlat1),apply(apply(s,k),k)) = sFlat3,
inference(step,[status(thm)],[t24,t35]) ).
cnf(t1453,plain,
apply(apply(s,sFlat1),sFlat1) = sFlat3,
inference(step,[status(thm)],[t1452,t35]) ).
cnf(t37,plain,
apply(apply(s,sFlat1),sFlat1) = sFlat3,
inference(rw,[status(thm)],[t1453]) ).
cnf(t1476,plain,
apply(sFlat2,sFlat1) = sFlat3,
inference(step,[status(thm)],[t37,t49]) ).
cnf(t82,plain,
apply(sFlat2,sFlat1) = sFlat3,
inference(orient,[status(thm)],[t1476]) ).
cnf(t1479,plain,
apply(k,sFlat3) = sFlat4,
inference(step,[status(thm)],[t51,t82]) ).
cnf(t85,plain,
apply(k,sFlat3) = sFlat4,
inference(orient,[status(thm)],[t1479]) ).
cnf(t86,plain,
sFlat3 = apply(sFlat4,X1),
inference(cp,[status(thm)],[t17,t85]) ).
cnf(t87,plain,
apply(sFlat4,X1) = sFlat3,
inference(orient,[status(thm)],[t86]) ).
cnf(t204,plain,
apply(apply(sFlat9,sFlat4),X1) = apply(apply(sFlat8,X1),sFlat3),
inference(cp,[status(thm)],[t185,t87]) ).
cnf(t14,axiom,
sFlat10 = apply(apply(s,apply(apply(s,apply(k,s)),k)),apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))),
introduced(definition) ).
cnf(t20,plain,
apply(apply(s,apply(apply(s,apply(k,s)),k)),apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))) = sFlat10,
inference(orient,[status(thm)],[t14]) ).
cnf(t21,plain,
apply(apply(apply(s,apply(s,apply(apply(s,apply(k,s)),k))),X1),apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))) = apply(sFlat10,apply(X1,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k))))),
inference(cp,[status(thm)],[t19,t20]) ).
cnf(t1498,plain,
apply(apply(apply(s,apply(s,apply(apply(sFlat8,s),k))),X1),apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))) = apply(sFlat10,apply(X1,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k))))),
inference(step,[status(thm)],[t21,t92]) ).
cnf(t93,plain,
apply(sFlat8,s) = apply(s,sFlat6),
inference(cp,[status(thm)],[t92,t42]) ).
cnf(t1482,plain,
apply(sFlat8,s) = sFlat7,
inference(step,[status(thm)],[t93,t56]) ).
cnf(t98,plain,
apply(sFlat8,s) = sFlat7,
inference(orient,[status(thm)],[t1482]) ).
cnf(t1499,plain,
apply(apply(apply(s,apply(s,apply(sFlat7,k))),X1),apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))) = apply(sFlat10,apply(X1,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k))))),
inference(step,[status(thm)],[t1498,t98]) ).
cnf(t1500,plain,
apply(apply(apply(s,apply(s,sFlat8)),X1),apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))) = apply(sFlat10,apply(X1,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k))))),
inference(step,[status(thm)],[t1499,t84]) ).
cnf(t1501,plain,
apply(apply(apply(s,sFlat9),X1),apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))) = apply(sFlat10,apply(X1,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k))))),
inference(step,[status(thm)],[t1500,t90]) ).
cnf(t4,axiom,
sFlat0 = apply(s,k),
introduced(definition) ).
cnf(t59,plain,
apply(s,k) = sFlat0,
inference(orient,[status(thm)],[t4]) ).
cnf(t1502,plain,
apply(apply(apply(s,sFlat9),X1),apply(k,apply(apply(s,apply(sFlat0,k)),apply(apply(s,k),k)))) = apply(sFlat10,apply(X1,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k))))),
inference(step,[status(thm)],[t1501,t59]) ).
cnf(t1465,plain,
apply(sFlat0,k) = sFlat1,
inference(step,[status(thm)],[t35,t59]) ).
cnf(t61,plain,
apply(sFlat0,k) = sFlat1,
inference(rw,[status(thm)],[t1465]) ).
cnf(t77,plain,
apply(sFlat0,k) = sFlat1,
inference(orient,[status(thm)],[t61]) ).
cnf(t1503,plain,
apply(apply(apply(s,sFlat9),X1),apply(k,apply(apply(s,sFlat1),apply(apply(s,k),k)))) = apply(sFlat10,apply(X1,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k))))),
inference(step,[status(thm)],[t1502,t77]) ).
cnf(t1504,plain,
apply(apply(apply(s,sFlat9),X1),apply(k,apply(sFlat2,apply(apply(s,k),k)))) = apply(sFlat10,apply(X1,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k))))),
inference(step,[status(thm)],[t1503,t49]) ).
cnf(t1505,plain,
apply(apply(apply(s,sFlat9),X1),apply(k,apply(sFlat2,apply(sFlat0,k)))) = apply(sFlat10,apply(X1,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k))))),
inference(step,[status(thm)],[t1504,t59]) ).
cnf(t1506,plain,
apply(apply(apply(s,sFlat9),X1),apply(k,apply(sFlat2,sFlat1))) = apply(sFlat10,apply(X1,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k))))),
inference(step,[status(thm)],[t1505,t77]) ).
cnf(t1507,plain,
apply(apply(apply(s,sFlat9),X1),apply(k,sFlat3)) = apply(sFlat10,apply(X1,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k))))),
inference(step,[status(thm)],[t1506,t82]) ).
cnf(t1508,plain,
apply(apply(apply(s,sFlat9),X1),sFlat4) = apply(sFlat10,apply(X1,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k))))),
inference(step,[status(thm)],[t1507,t85]) ).
cnf(t1509,plain,
apply(apply(sFlat9,sFlat4),apply(X1,sFlat4)) = apply(sFlat10,apply(X1,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k))))),
inference(step,[status(thm)],[t1508,t19]) ).
cnf(t1510,plain,
apply(apply(sFlat9,sFlat4),apply(X1,sFlat4)) = apply(sFlat10,apply(X1,apply(k,apply(apply(s,apply(sFlat0,k)),apply(apply(s,k),k))))),
inference(step,[status(thm)],[t1509,t59]) ).
cnf(t1511,plain,
apply(apply(sFlat9,sFlat4),apply(X1,sFlat4)) = apply(sFlat10,apply(X1,apply(k,apply(apply(s,sFlat1),apply(apply(s,k),k))))),
inference(step,[status(thm)],[t1510,t77]) ).
cnf(t1512,plain,
apply(apply(sFlat9,sFlat4),apply(X1,sFlat4)) = apply(sFlat10,apply(X1,apply(k,apply(sFlat2,apply(apply(s,k),k))))),
inference(step,[status(thm)],[t1511,t49]) ).
cnf(t1513,plain,
apply(apply(sFlat9,sFlat4),apply(X1,sFlat4)) = apply(sFlat10,apply(X1,apply(k,apply(sFlat2,apply(sFlat0,k))))),
inference(step,[status(thm)],[t1512,t59]) ).
cnf(t1514,plain,
apply(apply(sFlat9,sFlat4),apply(X1,sFlat4)) = apply(sFlat10,apply(X1,apply(k,apply(sFlat2,sFlat1)))),
inference(step,[status(thm)],[t1513,t77]) ).
cnf(t1515,plain,
apply(apply(sFlat9,sFlat4),apply(X1,sFlat4)) = apply(sFlat10,apply(X1,apply(k,sFlat3))),
inference(step,[status(thm)],[t1514,t82]) ).
cnf(t1516,plain,
apply(apply(sFlat9,sFlat4),apply(X1,sFlat4)) = apply(sFlat10,apply(X1,sFlat4)),
inference(step,[status(thm)],[t1515,t85]) ).
cnf(t243,plain,
apply(apply(sFlat9,sFlat4),apply(X1,sFlat4)) = apply(sFlat10,apply(X1,sFlat4)),
inference(orient,[status(thm)],[t1516]) ).
cnf(t256,plain,
apply(sFlat10,apply(apply(k,X1),sFlat4)) = apply(apply(sFlat9,sFlat4),X1),
inference(cp,[status(thm)],[t243,t17]) ).
cnf(t1517,plain,
apply(sFlat10,X1) = apply(apply(sFlat9,sFlat4),X1),
inference(step,[status(thm)],[t256,t17]) ).
cnf(t264,plain,
apply(apply(sFlat9,sFlat4),X1) = apply(sFlat10,X1),
inference(orient,[status(thm)],[t1517]) ).
cnf(t1524,plain,
apply(sFlat10,X1) = apply(apply(sFlat8,X1),sFlat3),
inference(step,[status(thm)],[t204,t264]) ).
cnf(t280,plain,
apply(apply(sFlat8,X1),sFlat3) = apply(sFlat10,X1),
inference(orient,[status(thm)],[t1524]) ).
cnf(t282,plain,
apply(X1,apply(sFlat3,X2)) = apply(apply(sFlat10,X1),X2),
inference(cp,[status(thm)],[t176,t280]) ).
cnf(t304,plain,
apply(apply(sFlat10,X1),X2) = apply(X1,apply(sFlat3,X2)),
inference(orient,[status(thm)],[t282]) ).
cnf(t36,plain,
apply(apply(k,X1),apply(k,X1)) = apply(sFlat1,X1),
inference(cp,[status(thm)],[t19,t35]) ).
cnf(t1471,plain,
X1 = apply(sFlat1,X1),
inference(step,[status(thm)],[t36,t17]) ).
cnf(t69,plain,
apply(sFlat1,X1) = X1,
inference(orient,[status(thm)],[t1471]) ).
cnf(t72,plain,
apply(apply(apply(s,sFlat1),X1),X2) = apply(X2,apply(X1,X2)),
inference(cp,[status(thm)],[t19,t69]) ).
cnf(t1486,plain,
apply(apply(sFlat2,X1),X2) = apply(X2,apply(X1,X2)),
inference(step,[status(thm)],[t72,t49]) ).
cnf(t104,plain,
apply(apply(sFlat2,X1),X2) = apply(X2,apply(X1,X2)),
inference(orient,[status(thm)],[t1486]) ).
cnf(t105,plain,
apply(X1,apply(sFlat1,X1)) = apply(sFlat3,X1),
inference(cp,[status(thm)],[t104,t82]) ).
cnf(t1487,plain,
apply(X1,X1) = apply(sFlat3,X1),
inference(step,[status(thm)],[t105,t69]) ).
cnf(t113,plain,
apply(X1,X1) = apply(sFlat3,X1),
inference(orient,[status(thm)],[t1487]) ).
cnf(t305,plain,
apply(X1,apply(sFlat3,apply(sFlat10,X1))) = apply(sFlat3,apply(sFlat10,X1)),
inference(cp,[status(thm)],[t304,t113]) ).
cnf(t815,plain,
apply(X1,apply(sFlat3,apply(sFlat10,X1))) = apply(sFlat3,apply(sFlat10,X1)),
inference(orient,[status(thm)],[t305]) ).
cnf(t15,axiom,
sFlat11 = apply(apply(s,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))),apply(apply(s,apply(apply(s,apply(k,s)),k)),apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k))))),
introduced(definition) ).
cnf(t1449,plain,
sFlat11 = apply(apply(apply(s,s),apply(s,apply(apply(s,apply(k,s)),k))),apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))),
inference(step,[status(thm)],[t15,t19]) ).
cnf(t1450,plain,
sFlat11 = apply(apply(apply(s,s),apply(s,apply(apply(s,apply(k,s)),k))),apply(k,sFlat3)),
inference(step,[status(thm)],[t1449,t24]) ).
cnf(t29,plain,
apply(apply(apply(s,s),apply(s,apply(apply(s,apply(k,s)),k))),apply(k,sFlat3)) = sFlat11,
inference(orient,[status(thm)],[t1450]) ).
cnf(t30,plain,
apply(apply(apply(s,apply(apply(s,s),apply(s,apply(apply(s,apply(k,s)),k)))),X1),apply(k,sFlat3)) = apply(sFlat11,apply(X1,apply(k,sFlat3))),
inference(cp,[status(thm)],[t19,t29]) ).
cnf(t1588,plain,
apply(apply(apply(s,apply(apply(sFlat3,s),apply(s,apply(apply(s,apply(k,s)),k)))),X1),apply(k,sFlat3)) = apply(sFlat11,apply(X1,apply(k,sFlat3))),
inference(step,[status(thm)],[t30,t113]) ).
cnf(t1589,plain,
apply(apply(apply(s,apply(apply(sFlat3,s),apply(s,apply(apply(sFlat8,s),k)))),X1),apply(k,sFlat3)) = apply(sFlat11,apply(X1,apply(k,sFlat3))),
inference(step,[status(thm)],[t1588,t92]) ).
cnf(t1590,plain,
apply(apply(apply(s,apply(apply(sFlat3,s),apply(s,apply(sFlat7,k)))),X1),apply(k,sFlat3)) = apply(sFlat11,apply(X1,apply(k,sFlat3))),
inference(step,[status(thm)],[t1589,t98]) ).
cnf(t1591,plain,
apply(apply(apply(s,apply(apply(sFlat3,s),apply(s,sFlat8))),X1),apply(k,sFlat3)) = apply(sFlat11,apply(X1,apply(k,sFlat3))),
inference(step,[status(thm)],[t1590,t84]) ).
cnf(t1592,plain,
apply(apply(apply(s,apply(apply(sFlat3,s),sFlat9)),X1),apply(k,sFlat3)) = apply(sFlat11,apply(X1,apply(k,sFlat3))),
inference(step,[status(thm)],[t1591,t90]) ).
cnf(t1593,plain,
apply(apply(apply(s,apply(apply(sFlat3,s),sFlat9)),X1),sFlat4) = apply(sFlat11,apply(X1,apply(k,sFlat3))),
inference(step,[status(thm)],[t1592,t85]) ).
cnf(t1594,plain,
apply(apply(apply(apply(sFlat3,s),sFlat9),sFlat4),apply(X1,sFlat4)) = apply(sFlat11,apply(X1,apply(k,sFlat3))),
inference(step,[status(thm)],[t1593,t19]) ).
cnf(t123,plain,
apply(apply(s,X1),apply(X2,X1)) = apply(apply(apply(sFlat3,s),X2),X1),
inference(cp,[status(thm)],[t19,t113]) ).
cnf(t687,plain,
apply(apply(s,X1),apply(X2,X1)) = apply(apply(apply(sFlat3,s),X2),X1),
inference(orient,[status(thm)],[t123]) ).
cnf(t1595,plain,
apply(apply(apply(s,sFlat4),apply(sFlat9,sFlat4)),apply(X1,sFlat4)) = apply(sFlat11,apply(X1,apply(k,sFlat3))),
inference(step,[status(thm)],[t1594,t687]) ).
cnf(t22,plain,
apply(apply(apply(s,X1),apply(s,apply(apply(s,apply(k,s)),k))),apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))) = apply(apply(X1,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))),sFlat10),
inference(cp,[status(thm)],[t19,t20]) ).
cnf(t1538,plain,
apply(apply(apply(s,X1),apply(s,apply(apply(sFlat8,s),k))),apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))) = apply(apply(X1,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))),sFlat10),
inference(step,[status(thm)],[t22,t92]) ).
cnf(t1539,plain,
apply(apply(apply(s,X1),apply(s,apply(sFlat7,k))),apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))) = apply(apply(X1,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))),sFlat10),
inference(step,[status(thm)],[t1538,t98]) ).
cnf(t1540,plain,
apply(apply(apply(s,X1),apply(s,sFlat8)),apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))) = apply(apply(X1,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))),sFlat10),
inference(step,[status(thm)],[t1539,t84]) ).
cnf(t1541,plain,
apply(apply(apply(s,X1),sFlat9),apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))) = apply(apply(X1,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))),sFlat10),
inference(step,[status(thm)],[t1540,t90]) ).
cnf(t1542,plain,
apply(apply(apply(s,X1),sFlat9),apply(k,apply(apply(s,apply(sFlat0,k)),apply(apply(s,k),k)))) = apply(apply(X1,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))),sFlat10),
inference(step,[status(thm)],[t1541,t59]) ).
cnf(t1543,plain,
apply(apply(apply(s,X1),sFlat9),apply(k,apply(apply(s,sFlat1),apply(apply(s,k),k)))) = apply(apply(X1,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))),sFlat10),
inference(step,[status(thm)],[t1542,t77]) ).
cnf(t1544,plain,
apply(apply(apply(s,X1),sFlat9),apply(k,apply(sFlat2,apply(apply(s,k),k)))) = apply(apply(X1,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))),sFlat10),
inference(step,[status(thm)],[t1543,t49]) ).
cnf(t1545,plain,
apply(apply(apply(s,X1),sFlat9),apply(k,apply(sFlat2,apply(sFlat0,k)))) = apply(apply(X1,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))),sFlat10),
inference(step,[status(thm)],[t1544,t59]) ).
cnf(t1546,plain,
apply(apply(apply(s,X1),sFlat9),apply(k,apply(sFlat2,sFlat1))) = apply(apply(X1,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))),sFlat10),
inference(step,[status(thm)],[t1545,t77]) ).
cnf(t1547,plain,
apply(apply(apply(s,X1),sFlat9),apply(k,sFlat3)) = apply(apply(X1,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))),sFlat10),
inference(step,[status(thm)],[t1546,t82]) ).
cnf(t1548,plain,
apply(apply(apply(s,X1),sFlat9),sFlat4) = apply(apply(X1,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))),sFlat10),
inference(step,[status(thm)],[t1547,t85]) ).
cnf(t1549,plain,
apply(apply(X1,sFlat4),apply(sFlat9,sFlat4)) = apply(apply(X1,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))),sFlat10),
inference(step,[status(thm)],[t1548,t19]) ).
cnf(t1550,plain,
apply(apply(X1,sFlat4),apply(sFlat9,sFlat4)) = apply(apply(X1,apply(k,apply(apply(s,apply(sFlat0,k)),apply(apply(s,k),k)))),sFlat10),
inference(step,[status(thm)],[t1549,t59]) ).
cnf(t1551,plain,
apply(apply(X1,sFlat4),apply(sFlat9,sFlat4)) = apply(apply(X1,apply(k,apply(apply(s,sFlat1),apply(apply(s,k),k)))),sFlat10),
inference(step,[status(thm)],[t1550,t77]) ).
cnf(t1552,plain,
apply(apply(X1,sFlat4),apply(sFlat9,sFlat4)) = apply(apply(X1,apply(k,apply(sFlat2,apply(apply(s,k),k)))),sFlat10),
inference(step,[status(thm)],[t1551,t49]) ).
cnf(t1553,plain,
apply(apply(X1,sFlat4),apply(sFlat9,sFlat4)) = apply(apply(X1,apply(k,apply(sFlat2,apply(sFlat0,k)))),sFlat10),
inference(step,[status(thm)],[t1552,t59]) ).
cnf(t1554,plain,
apply(apply(X1,sFlat4),apply(sFlat9,sFlat4)) = apply(apply(X1,apply(k,apply(sFlat2,sFlat1))),sFlat10),
inference(step,[status(thm)],[t1553,t77]) ).
cnf(t1555,plain,
apply(apply(X1,sFlat4),apply(sFlat9,sFlat4)) = apply(apply(X1,apply(k,sFlat3)),sFlat10),
inference(step,[status(thm)],[t1554,t82]) ).
cnf(t1556,plain,
apply(apply(X1,sFlat4),apply(sFlat9,sFlat4)) = apply(apply(X1,sFlat4),sFlat10),
inference(step,[status(thm)],[t1555,t85]) ).
cnf(t570,plain,
apply(apply(X1,sFlat4),apply(sFlat9,sFlat4)) = apply(apply(X1,sFlat4),sFlat10),
inference(orient,[status(thm)],[t1556]) ).
cnf(t1596,plain,
apply(apply(apply(s,sFlat4),sFlat10),apply(X1,sFlat4)) = apply(sFlat11,apply(X1,apply(k,sFlat3))),
inference(step,[status(thm)],[t1595,t570]) ).
cnf(t94,plain,
apply(sFlat8,sFlat3) = apply(s,sFlat4),
inference(cp,[status(thm)],[t92,t85]) ).
cnf(t99,plain,
apply(s,sFlat4) = apply(sFlat8,sFlat3),
inference(orient,[status(thm)],[t94]) ).
cnf(t9,axiom,
sFlat5 = apply(s,apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))),
introduced(definition) ).
cnf(t1460,plain,
sFlat5 = apply(s,apply(k,apply(apply(s,sFlat1),apply(apply(s,k),k)))),
inference(step,[status(thm)],[t9,t35]) ).
cnf(t1461,plain,
sFlat5 = apply(s,apply(k,apply(sFlat2,apply(apply(s,k),k)))),
inference(step,[status(thm)],[t1460,t49]) ).
cnf(t1462,plain,
sFlat5 = apply(s,apply(k,apply(sFlat2,sFlat1))),
inference(step,[status(thm)],[t1461,t35]) ).
cnf(t52,plain,
apply(s,apply(k,apply(sFlat2,sFlat1))) = sFlat5,
inference(orient,[status(thm)],[t1462]) ).
cnf(t1477,plain,
apply(s,apply(k,sFlat3)) = sFlat5,
inference(step,[status(thm)],[t52,t82]) ).
cnf(t83,plain,
apply(s,apply(k,sFlat3)) = sFlat5,
inference(rw,[status(thm)],[t1477]) ).
cnf(t1483,plain,
apply(sFlat8,sFlat3) = sFlat5,
inference(step,[status(thm)],[t83,t92]) ).
cnf(t101,plain,
apply(sFlat8,sFlat3) = sFlat5,
inference(orient,[status(thm)],[t1483]) ).
cnf(t1484,plain,
apply(s,sFlat4) = sFlat5,
inference(step,[status(thm)],[t99,t101]) ).
cnf(t102,plain,
apply(s,sFlat4) = sFlat5,
inference(orient,[status(thm)],[t1484]) ).
cnf(t1597,plain,
apply(apply(sFlat5,sFlat10),apply(X1,sFlat4)) = apply(sFlat11,apply(X1,apply(k,sFlat3))),
inference(step,[status(thm)],[t1596,t102]) ).
cnf(t55,plain,
apply(apply(apply(k,apply(sFlat2,sFlat1)),X1),apply(X2,X1)) = apply(apply(sFlat5,X2),X1),
inference(cp,[status(thm)],[t19,t52]) ).
cnf(t1489,plain,
apply(apply(sFlat2,sFlat1),apply(X2,X1)) = apply(apply(sFlat5,X2),X1),
inference(step,[status(thm)],[t55,t17]) ).
cnf(t1490,plain,
apply(sFlat3,apply(X2,X1)) = apply(apply(sFlat5,X2),X1),
inference(step,[status(thm)],[t1489,t82]) ).
cnf(t160,plain,
apply(apply(sFlat5,X1),X2) = apply(sFlat3,apply(X1,X2)),
inference(orient,[status(thm)],[t1490]) ).
cnf(t1598,plain,
apply(sFlat3,apply(sFlat10,apply(X1,sFlat4))) = apply(sFlat11,apply(X1,apply(k,sFlat3))),
inference(step,[status(thm)],[t1597,t160]) ).
cnf(t1599,plain,
apply(sFlat3,apply(sFlat10,apply(X1,sFlat4))) = apply(sFlat11,apply(X1,sFlat4)),
inference(step,[status(thm)],[t1598,t85]) ).
cnf(t1243,plain,
apply(sFlat3,apply(sFlat10,apply(X1,sFlat4))) = apply(sFlat11,apply(X1,sFlat4)),
inference(orient,[status(thm)],[t1599]) ).
cnf(t1271,plain,
apply(sFlat11,apply(apply(k,X1),sFlat4)) = apply(sFlat3,apply(sFlat10,X1)),
inference(cp,[status(thm)],[t1243,t17]) ).
cnf(t1602,plain,
apply(sFlat11,X1) = apply(sFlat3,apply(sFlat10,X1)),
inference(step,[status(thm)],[t1271,t17]) ).
cnf(t1290,plain,
apply(sFlat3,apply(sFlat10,X1)) = apply(sFlat11,X1),
inference(orient,[status(thm)],[t1602]) ).
cnf(t1611,plain,
apply(X1,apply(sFlat11,X1)) = apply(sFlat3,apply(sFlat10,X1)),
inference(step,[status(thm)],[t815,t1290]) ).
cnf(t1612,plain,
apply(X1,apply(sFlat11,X1)) = apply(sFlat11,X1),
inference(step,[status(thm)],[t1611,t1290]) ).
cnf(t1308,plain,
apply(X1,apply(sFlat11,X1)) = apply(sFlat11,X1),
inference(rw,[status(thm)],[t1612]) ).
cnf(t1371,plain,
apply(X1,apply(sFlat11,X1)) = apply(sFlat11,X1),
inference(orient,[status(thm)],[t1308]) ).
cnf(t1409,plain,
true = ifeq(apply(sFlat11,fixed_pt),apply(sFlat11,fixed_pt),fixed_point(sFlat11),true),
inference(cp,[status(thm)],[t62,t1371]) ).
cnf(t1,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t18,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t1]) ).
cnf(t1621,plain,
true = fixed_point(sFlat11),
inference(step,[status(thm)],[t1409,t18]) ).
cnf(t1447,plain,
fixed_point(sFlat11) = true,
inference(orient,[status(thm)],[t1621]) ).
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(apply(s,apply(k,s)),k)),apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))))),
file('/export/starexec/sandbox2/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(apply(s,apply(k,s)),k)),apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),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(apply(s,apply(k,s)),k)),apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),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(apply(s,apply(k,s)),k)),apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),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(apply(s,apply(k,s)),k)),apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k)))))) != true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(g0_0,plain,
fixed_point(apply(apply(apply(s,s),apply(s,apply(apply(s,apply(k,s)),k))),apply(k,apply(apply(s,apply(apply(s,k),k)),apply(apply(s,k),k))))) != true,
inference(rw,[status(thm)],[goal_0,t19]) ).
cnf(g0_1,plain,
fixed_point(apply(apply(apply(s,s),apply(s,apply(apply(s,apply(k,s)),k))),apply(k,sFlat3))) != true,
inference(rw,[status(thm)],[g0_0]) ).
cnf(g0_2,plain,
fixed_point(sFlat11) != true,
inference(rw,[status(thm)],[g0_1]) ).
cnf(g0_3,plain,
true != true,
inference(rw,[status(thm)],[g0_2,t1447]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : COL006-3 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.12/5.37 % Computer : n016.cluster.edu
% 0.12/5.37 % Model : x86_64 x86_64
% 0.12/5.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/5.37 % Memory : 8046.5625MB
% 0.12/5.37 % OS : Linux 6.8.0-71-generic
% 0.12/5.37 % CPULimit : 300
% 0.12/5.37 % WCLimit : 300
% 0.12/5.37 % DateTime : Fri Sep 25 07:15:48 UTC 2026
% 0.12/5.38 % CPUTime :
% 0.12/5.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 18.24/7.79 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 18.24/7.79 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------