%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL067-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n003.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 02:00:49 PM UTC 2026
% Result : Unsatisfiable 33.87s 4.78s
% Output : Proof 33.87s
% Verified :
% Comments :
%------------------------------------------------------------------------------
cnf(t5,axiom,
sFlat0 = implies(a,b),
introduced(definition) ).
cnf(t17,plain,
implies(a,b) = sFlat0,
inference(orient,[status(thm)],[t5]) ).
cnf(t6,axiom,
sFlat1 = implies(b,c),
introduced(definition) ).
cnf(t14,plain,
implies(b,c) = sFlat1,
inference(orient,[status(thm)],[t6]) ).
cnf(t7,axiom,
sFlat2 = implies(a,c),
introduced(definition) ).
cnf(t16,plain,
implies(a,c) = sFlat2,
inference(orient,[status(thm)],[t7]) ).
cnf(t8,axiom,
sFlat3 = implies(implies(b,c),implies(a,c)),
introduced(definition) ).
cnf(t12,plain,
implies(implies(b,c),implies(a,c)) = sFlat3,
inference(orient,[status(thm)],[t8]) ).
cnf(t5373,plain,
implies(sFlat1,implies(a,c)) = sFlat3,
inference(step,[status(thm)],[t12,t14]) ).
cnf(t15,plain,
implies(sFlat1,implies(a,c)) = sFlat3,
inference(rw,[status(thm)],[t5373]) ).
cnf(t5378,plain,
implies(sFlat1,sFlat2) = sFlat3,
inference(step,[status(thm)],[t15,t16]) ).
cnf(t61,plain,
implies(sFlat1,sFlat2) = sFlat3,
inference(orient,[status(thm)],[t5378]) ).
cnf(t9,axiom,
sFlat4 = implies(implies(a,b),implies(implies(b,c),implies(a,c))),
introduced(definition) ).
cnf(t5372,plain,
sFlat4 = implies(implies(a,b),sFlat3),
inference(step,[status(thm)],[t9,t12]) ).
cnf(t13,plain,
implies(implies(a,b),sFlat3) = sFlat4,
inference(orient,[status(thm)],[t5372]) ).
cnf(t5374,plain,
implies(sFlat0,sFlat3) = sFlat4,
inference(step,[status(thm)],[t13,t17]) ).
cnf(t18,plain,
implies(sFlat0,sFlat3) = sFlat4,
inference(rw,[status(thm)],[t5374]) ).
cnf(t54,plain,
implies(sFlat0,sFlat3) = sFlat4,
inference(orient,[status(thm)],[t18]) ).
cnf(t10,axiom,
sFlat5 = is_a_theorem(implies(implies(a,b),implies(implies(b,c),implies(a,c)))),
introduced(definition) ).
cnf(t5375,plain,
sFlat5 = is_a_theorem(implies(sFlat0,implies(implies(b,c),implies(a,c)))),
inference(step,[status(thm)],[t10,t17]) ).
cnf(t5376,plain,
sFlat5 = is_a_theorem(implies(sFlat0,implies(sFlat1,implies(a,c)))),
inference(step,[status(thm)],[t5375,t14]) ).
cnf(t5377,plain,
sFlat5 = is_a_theorem(implies(sFlat0,implies(sFlat1,sFlat2))),
inference(step,[status(thm)],[t5376,t16]) ).
cnf(t50,plain,
is_a_theorem(implies(sFlat0,implies(sFlat1,sFlat2))) = sFlat5,
inference(orient,[status(thm)],[t5377]) ).
cnf(t5379,plain,
is_a_theorem(implies(sFlat0,sFlat3)) = sFlat5,
inference(step,[status(thm)],[t50,t61]) ).
cnf(t5380,plain,
is_a_theorem(sFlat4) = sFlat5,
inference(step,[status(thm)],[t5379,t54]) ).
cnf(t68,plain,
is_a_theorem(sFlat4) = sFlat5,
inference(rw,[status(thm)],[t5380]) ).
cnf(t69,plain,
is_a_theorem(sFlat4) = sFlat5,
inference(orient,[status(thm)],[t68]) ).
cnf(f0,axiom,
( is_a_theorem(Y)
| ~ is_a_theorem(X)
| ~ is_a_theorem(implies(X,Y)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',condensed_detachment) ).
fof(f0_nnf,plain,
! [X,Y] :
( is_a_theorem(Y)
| ~ is_a_theorem(X)
| ~ is_a_theorem(implies(X,Y)) ),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X,Y] :
( is_a_theorem(Y)
| ~ is_a_theorem(X)
| ~ is_a_theorem(implies(X,Y)) ),
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
( is_a_theorem(X1)
| ~ is_a_theorem(X0)
| ~ is_a_theorem(implies(X0,X1)) ),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t3,plain,
ifeq(is_a_theorem(implies(X1,X2)),true,ifeq(is_a_theorem(X1),true,is_a_theorem(X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t37,plain,
ifeq(is_a_theorem(implies(X1,X2)),true,ifeq(is_a_theorem(X1),true,is_a_theorem(X2),true),true) = true,
inference(orient,[status(thm)],[t3]) ).
cnf(f3,axiom,
is_a_theorem(implies(implies(not(X),Z),implies(implies(Y,Z),implies(implies(X,Y),Z)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cn_59) ).
fof(f3_nnf,plain,
! [X,Z,Y] : is_a_theorem(implies(implies(not(X),Z),implies(implies(Y,Z),implies(implies(X,Y),Z)))),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X,Z,Y] : is_a_theorem(implies(implies(not(X),Z),implies(implies(Y,Z),implies(implies(X,Y),Z)))),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
is_a_theorem(implies(implies(not(X0),X1),implies(implies(X2,X1),implies(implies(X0,X2),X1)))),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t4,plain,
is_a_theorem(implies(implies(not(X1),X2),implies(implies(X3,X2),implies(implies(X1,X3),X2)))) = true,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t30,plain,
is_a_theorem(implies(implies(not(X1),X2),implies(implies(X3,X2),implies(implies(X1,X3),X2)))) = true,
inference(orient,[status(thm)],[t4]) ).
cnf(t38,plain,
true = ifeq(true,true,ifeq(is_a_theorem(implies(not(X1),X2)),true,is_a_theorem(implies(implies(X3,X2),implies(implies(X1,X3),X2))),true),true),
inference(cp,[status(thm)],[t37,t30]) ).
cnf(t0,plain,
ifeq(X1,X1,X2,X3) = X2,
introduced(definition) ).
cnf(t11,plain,
ifeq(X1,X1,X2,X3) = X2,
inference(orient,[status(thm)],[t0]) ).
cnf(t5494,plain,
true = ifeq(is_a_theorem(implies(not(X1),X2)),true,is_a_theorem(implies(implies(X3,X2),implies(implies(X1,X3),X2))),true),
inference(step,[status(thm)],[t38,t11]) ).
cnf(t710,plain,
ifeq(is_a_theorem(implies(not(X1),X2)),true,is_a_theorem(implies(implies(X3,X2),implies(implies(X1,X3),X2))),true) = true,
inference(orient,[status(thm)],[t5494]) ).
cnf(f2,axiom,
is_a_theorem(implies(implies(implies(X,Y),Z),implies(not(X),Z))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cn_37) ).
fof(f2_nnf,plain,
! [X,Y,Z] : is_a_theorem(implies(implies(implies(X,Y),Z),implies(not(X),Z))),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X,Y,Z] : is_a_theorem(implies(implies(implies(X,Y),Z),implies(not(X),Z))),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
is_a_theorem(implies(implies(implies(X0,X1),X2),implies(not(X0),X2))),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t2,plain,
is_a_theorem(implies(implies(implies(X1,X2),X3),implies(not(X1),X3))) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t26,plain,
is_a_theorem(implies(implies(implies(X1,X2),X3),implies(not(X1),X3))) = true,
inference(orient,[status(thm)],[t2]) ).
cnf(t65,plain,
true = is_a_theorem(implies(implies(sFlat3,X1),implies(not(sFlat1),X1))),
inference(cp,[status(thm)],[t26,t61]) ).
cnf(t154,plain,
is_a_theorem(implies(implies(sFlat3,X1),implies(not(sFlat1),X1))) = true,
inference(orient,[status(thm)],[t65]) ).
cnf(t155,plain,
true = ifeq(true,true,ifeq(is_a_theorem(implies(sFlat3,X1)),true,is_a_theorem(implies(not(sFlat1),X1)),true),true),
inference(cp,[status(thm)],[t37,t154]) ).
cnf(t5436,plain,
true = ifeq(is_a_theorem(implies(sFlat3,X1)),true,is_a_theorem(implies(not(sFlat1),X1)),true),
inference(step,[status(thm)],[t155,t11]) ).
cnf(t301,plain,
ifeq(is_a_theorem(implies(sFlat3,X1)),true,is_a_theorem(implies(not(sFlat1),X1)),true) = true,
inference(orient,[status(thm)],[t5436]) ).
cnf(f1,axiom,
is_a_theorem(implies(implies(implies(X,Y),Z),implies(Y,Z))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cn_19) ).
fof(f1_nnf,plain,
! [X,Y,Z] : is_a_theorem(implies(implies(implies(X,Y),Z),implies(Y,Z))),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,Y,Z] : is_a_theorem(implies(implies(implies(X,Y),Z),implies(Y,Z))),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
is_a_theorem(implies(implies(implies(X0,X1),X2),implies(X1,X2))),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t1,plain,
is_a_theorem(implies(implies(implies(X1,X2),X3),implies(X2,X3))) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t19,plain,
is_a_theorem(implies(implies(implies(X1,X2),X3),implies(X2,X3))) = true,
inference(orient,[status(thm)],[t1]) ).
cnf(t39,plain,
true = ifeq(true,true,ifeq(is_a_theorem(implies(implies(X1,X2),X3)),true,is_a_theorem(implies(X2,X3)),true),true),
inference(cp,[status(thm)],[t37,t19]) ).
cnf(t5445,plain,
true = ifeq(is_a_theorem(implies(implies(X1,X2),X3)),true,is_a_theorem(implies(X2,X3)),true),
inference(step,[status(thm)],[t39,t11]) ).
cnf(t361,plain,
ifeq(is_a_theorem(implies(implies(X1,X2),X3)),true,is_a_theorem(implies(X2,X3)),true) = true,
inference(orient,[status(thm)],[t5445]) ).
cnf(t57,plain,
true = is_a_theorem(implies(implies(implies(X1,sFlat0),sFlat3),sFlat4)),
inference(cp,[status(thm)],[t19,t54]) ).
cnf(t115,plain,
is_a_theorem(implies(implies(implies(X1,sFlat0),sFlat3),sFlat4)) = true,
inference(orient,[status(thm)],[t57]) ).
cnf(t371,plain,
true = ifeq(true,true,is_a_theorem(implies(sFlat3,sFlat4)),true),
inference(cp,[status(thm)],[t361,t115]) ).
cnf(t5447,plain,
true = is_a_theorem(implies(sFlat3,sFlat4)),
inference(step,[status(thm)],[t371,t11]) ).
cnf(t450,plain,
is_a_theorem(implies(sFlat3,sFlat4)) = true,
inference(orient,[status(thm)],[t5447]) ).
cnf(t457,plain,
true = ifeq(true,true,is_a_theorem(implies(not(sFlat1),sFlat4)),true),
inference(cp,[status(thm)],[t301,t450]) ).
cnf(t5467,plain,
true = is_a_theorem(implies(not(sFlat1),sFlat4)),
inference(step,[status(thm)],[t457,t11]) ).
cnf(t515,plain,
is_a_theorem(implies(not(sFlat1),sFlat4)) = true,
inference(orient,[status(thm)],[t5467]) ).
cnf(t711,plain,
true = ifeq(true,true,is_a_theorem(implies(implies(X1,sFlat4),implies(implies(sFlat1,X1),sFlat4))),true),
inference(cp,[status(thm)],[t710,t515]) ).
cnf(t5616,plain,
true = is_a_theorem(implies(implies(X1,sFlat4),implies(implies(sFlat1,X1),sFlat4))),
inference(step,[status(thm)],[t711,t11]) ).
cnf(t1442,plain,
is_a_theorem(implies(implies(X1,sFlat4),implies(implies(sFlat1,X1),sFlat4))) = true,
inference(orient,[status(thm)],[t5616]) ).
cnf(t1443,plain,
true = ifeq(true,true,ifeq(is_a_theorem(implies(X1,sFlat4)),true,is_a_theorem(implies(implies(sFlat1,X1),sFlat4)),true),true),
inference(cp,[status(thm)],[t37,t1442]) ).
cnf(t6132,plain,
true = ifeq(is_a_theorem(implies(X1,sFlat4)),true,is_a_theorem(implies(implies(sFlat1,X1),sFlat4)),true),
inference(step,[status(thm)],[t1443,t11]) ).
cnf(t4132,plain,
ifeq(is_a_theorem(implies(X1,sFlat4)),true,is_a_theorem(implies(implies(sFlat1,X1),sFlat4)),true) = true,
inference(orient,[status(thm)],[t6132]) ).
cnf(t40,plain,
true = ifeq(true,true,ifeq(is_a_theorem(implies(implies(X1,X2),X3)),true,is_a_theorem(implies(not(X1),X3)),true),true),
inference(cp,[status(thm)],[t37,t26]) ).
cnf(t5534,plain,
true = ifeq(is_a_theorem(implies(implies(X1,X2),X3)),true,is_a_theorem(implies(not(X1),X3)),true),
inference(step,[status(thm)],[t40,t11]) ).
cnf(t1083,plain,
ifeq(is_a_theorem(implies(implies(X1,X2),X3)),true,is_a_theorem(implies(not(X1),X3)),true) = true,
inference(orient,[status(thm)],[t5534]) ).
cnf(t27,plain,
true = is_a_theorem(implies(implies(sFlat2,X1),implies(not(a),X1))),
inference(cp,[status(thm)],[t26,t16]) ).
cnf(t128,plain,
is_a_theorem(implies(implies(sFlat2,X1),implies(not(a),X1))) = true,
inference(orient,[status(thm)],[t27]) ).
cnf(t129,plain,
true = ifeq(true,true,ifeq(is_a_theorem(implies(sFlat2,X1)),true,is_a_theorem(implies(not(a),X1)),true),true),
inference(cp,[status(thm)],[t37,t128]) ).
cnf(t5420,plain,
true = ifeq(is_a_theorem(implies(sFlat2,X1)),true,is_a_theorem(implies(not(a),X1)),true),
inference(step,[status(thm)],[t129,t11]) ).
cnf(t253,plain,
ifeq(is_a_theorem(implies(sFlat2,X1)),true,is_a_theorem(implies(not(a),X1)),true) = true,
inference(orient,[status(thm)],[t5420]) ).
cnf(t64,plain,
true = is_a_theorem(implies(implies(implies(X1,sFlat1),sFlat2),sFlat3)),
inference(cp,[status(thm)],[t19,t61]) ).
cnf(t123,plain,
is_a_theorem(implies(implies(implies(X1,sFlat1),sFlat2),sFlat3)) = true,
inference(orient,[status(thm)],[t64]) ).
cnf(t368,plain,
true = ifeq(true,true,is_a_theorem(implies(sFlat2,sFlat3)),true),
inference(cp,[status(thm)],[t361,t123]) ).
cnf(t5446,plain,
true = is_a_theorem(implies(sFlat2,sFlat3)),
inference(step,[status(thm)],[t368,t11]) ).
cnf(t442,plain,
is_a_theorem(implies(sFlat2,sFlat3)) = true,
inference(orient,[status(thm)],[t5446]) ).
cnf(t449,plain,
true = ifeq(true,true,is_a_theorem(implies(not(a),sFlat3)),true),
inference(cp,[status(thm)],[t253,t442]) ).
cnf(t5459,plain,
true = is_a_theorem(implies(not(a),sFlat3)),
inference(step,[status(thm)],[t449,t11]) ).
cnf(t502,plain,
is_a_theorem(implies(not(a),sFlat3)) = true,
inference(orient,[status(thm)],[t5459]) ).
cnf(t719,plain,
true = ifeq(true,true,is_a_theorem(implies(implies(X1,sFlat3),implies(implies(a,X1),sFlat3))),true),
inference(cp,[status(thm)],[t710,t502]) ).
cnf(t5622,plain,
true = is_a_theorem(implies(implies(X1,sFlat3),implies(implies(a,X1),sFlat3))),
inference(step,[status(thm)],[t719,t11]) ).
cnf(t1477,plain,
is_a_theorem(implies(implies(X1,sFlat3),implies(implies(a,X1),sFlat3))) = true,
inference(orient,[status(thm)],[t5622]) ).
cnf(t1479,plain,
true = is_a_theorem(implies(implies(b,sFlat3),implies(sFlat0,sFlat3))),
inference(cp,[status(thm)],[t1477,t17]) ).
cnf(t5623,plain,
true = is_a_theorem(implies(implies(b,sFlat3),sFlat4)),
inference(step,[status(thm)],[t1479,t54]) ).
cnf(t1484,plain,
is_a_theorem(implies(implies(b,sFlat3),sFlat4)) = true,
inference(orient,[status(thm)],[t5623]) ).
cnf(t1488,plain,
true = ifeq(true,true,is_a_theorem(implies(not(b),sFlat4)),true),
inference(cp,[status(thm)],[t1083,t1484]) ).
cnf(t5624,plain,
true = is_a_theorem(implies(not(b),sFlat4)),
inference(step,[status(thm)],[t1488,t11]) ).
cnf(t1489,plain,
is_a_theorem(implies(not(b),sFlat4)) = true,
inference(orient,[status(thm)],[t5624]) ).
cnf(t1493,plain,
true = ifeq(true,true,is_a_theorem(implies(implies(X1,sFlat4),implies(implies(b,X1),sFlat4))),true),
inference(cp,[status(thm)],[t710,t1489]) ).
cnf(t5705,plain,
true = is_a_theorem(implies(implies(X1,sFlat4),implies(implies(b,X1),sFlat4))),
inference(step,[status(thm)],[t1493,t11]) ).
cnf(t1795,plain,
is_a_theorem(implies(implies(X1,sFlat4),implies(implies(b,X1),sFlat4))) = true,
inference(orient,[status(thm)],[t5705]) ).
cnf(t1796,plain,
true = is_a_theorem(implies(implies(c,sFlat4),implies(sFlat1,sFlat4))),
inference(cp,[status(thm)],[t1795,t14]) ).
cnf(t1801,plain,
is_a_theorem(implies(implies(c,sFlat4),implies(sFlat1,sFlat4))) = true,
inference(orient,[status(thm)],[t1796]) ).
cnf(t1802,plain,
true = ifeq(true,true,ifeq(is_a_theorem(implies(c,sFlat4)),true,is_a_theorem(implies(sFlat1,sFlat4)),true),true),
inference(cp,[status(thm)],[t37,t1801]) ).
cnf(t5706,plain,
true = ifeq(is_a_theorem(implies(c,sFlat4)),true,is_a_theorem(implies(sFlat1,sFlat4)),true),
inference(step,[status(thm)],[t1802,t11]) ).
cnf(t20,plain,
true = is_a_theorem(implies(implies(sFlat2,X1),implies(c,X1))),
inference(cp,[status(thm)],[t19,t16]) ).
cnf(t72,plain,
is_a_theorem(implies(implies(sFlat2,X1),implies(c,X1))) = true,
inference(orient,[status(thm)],[t20]) ).
cnf(t73,plain,
true = ifeq(true,true,ifeq(is_a_theorem(implies(sFlat2,X1)),true,is_a_theorem(implies(c,X1)),true),true),
inference(cp,[status(thm)],[t37,t72]) ).
cnf(t5390,plain,
true = ifeq(is_a_theorem(implies(sFlat2,X1)),true,is_a_theorem(implies(c,X1)),true),
inference(step,[status(thm)],[t73,t11]) ).
cnf(t163,plain,
ifeq(is_a_theorem(implies(sFlat2,X1)),true,is_a_theorem(implies(c,X1)),true) = true,
inference(orient,[status(thm)],[t5390]) ).
cnf(t63,plain,
true = is_a_theorem(implies(implies(sFlat3,X1),implies(sFlat2,X1))),
inference(cp,[status(thm)],[t19,t61]) ).
cnf(t119,plain,
is_a_theorem(implies(implies(sFlat3,X1),implies(sFlat2,X1))) = true,
inference(orient,[status(thm)],[t63]) ).
cnf(t120,plain,
true = ifeq(true,true,ifeq(is_a_theorem(implies(sFlat3,X1)),true,is_a_theorem(implies(sFlat2,X1)),true),true),
inference(cp,[status(thm)],[t37,t119]) ).
cnf(t5401,plain,
true = ifeq(is_a_theorem(implies(sFlat3,X1)),true,is_a_theorem(implies(sFlat2,X1)),true),
inference(step,[status(thm)],[t120,t11]) ).
cnf(t189,plain,
ifeq(is_a_theorem(implies(sFlat3,X1)),true,is_a_theorem(implies(sFlat2,X1)),true) = true,
inference(orient,[status(thm)],[t5401]) ).
cnf(t454,plain,
true = ifeq(true,true,is_a_theorem(implies(sFlat2,sFlat4)),true),
inference(cp,[status(thm)],[t189,t450]) ).
cnf(t5457,plain,
true = is_a_theorem(implies(sFlat2,sFlat4)),
inference(step,[status(thm)],[t454,t11]) ).
cnf(t489,plain,
is_a_theorem(implies(sFlat2,sFlat4)) = true,
inference(orient,[status(thm)],[t5457]) ).
cnf(t493,plain,
true = ifeq(true,true,is_a_theorem(implies(c,sFlat4)),true),
inference(cp,[status(thm)],[t163,t489]) ).
cnf(t5458,plain,
true = is_a_theorem(implies(c,sFlat4)),
inference(step,[status(thm)],[t493,t11]) ).
cnf(t496,plain,
is_a_theorem(implies(c,sFlat4)) = true,
inference(orient,[status(thm)],[t5458]) ).
cnf(t5707,plain,
true = ifeq(true,true,is_a_theorem(implies(sFlat1,sFlat4)),true),
inference(step,[status(thm)],[t5706,t496]) ).
cnf(t5708,plain,
true = is_a_theorem(implies(sFlat1,sFlat4)),
inference(step,[status(thm)],[t5707,t11]) ).
cnf(t1806,plain,
is_a_theorem(implies(sFlat1,sFlat4)) = true,
inference(orient,[status(thm)],[t5708]) ).
cnf(t1808,plain,
true = ifeq(is_a_theorem(implies(implies(sFlat1,sFlat4),X1)),true,ifeq(true,true,is_a_theorem(X1),true),true),
inference(cp,[status(thm)],[t37,t1806]) ).
cnf(t5833,plain,
true = ifeq(is_a_theorem(implies(implies(sFlat1,sFlat4),X1)),true,is_a_theorem(X1),true),
inference(step,[status(thm)],[t1808,t11]) ).
cnf(t2487,plain,
ifeq(is_a_theorem(implies(implies(sFlat1,sFlat4),X1)),true,is_a_theorem(X1),true) = true,
inference(orient,[status(thm)],[t5833]) ).
cnf(t495,plain,
true = ifeq(true,true,is_a_theorem(implies(not(a),sFlat4)),true),
inference(cp,[status(thm)],[t253,t489]) ).
cnf(t5468,plain,
true = is_a_theorem(implies(not(a),sFlat4)),
inference(step,[status(thm)],[t495,t11]) ).
cnf(t520,plain,
is_a_theorem(implies(not(a),sFlat4)) = true,
inference(orient,[status(thm)],[t5468]) ).
cnf(t718,plain,
true = ifeq(true,true,is_a_theorem(implies(implies(X1,sFlat4),implies(implies(a,X1),sFlat4))),true),
inference(cp,[status(thm)],[t710,t520]) ).
cnf(t5618,plain,
true = is_a_theorem(implies(implies(X1,sFlat4),implies(implies(a,X1),sFlat4))),
inference(step,[status(thm)],[t718,t11]) ).
cnf(t1452,plain,
is_a_theorem(implies(implies(X1,sFlat4),implies(implies(a,X1),sFlat4))) = true,
inference(orient,[status(thm)],[t5618]) ).
cnf(t2490,plain,
true = ifeq(true,true,is_a_theorem(implies(implies(a,sFlat1),sFlat4)),true),
inference(cp,[status(thm)],[t2487,t1452]) ).
cnf(t5836,plain,
true = is_a_theorem(implies(implies(a,sFlat1),sFlat4)),
inference(step,[status(thm)],[t2490,t11]) ).
cnf(t2508,plain,
is_a_theorem(implies(implies(a,sFlat1),sFlat4)) = true,
inference(orient,[status(thm)],[t5836]) ).
cnf(t4147,plain,
true = ifeq(true,true,is_a_theorem(implies(implies(sFlat1,implies(a,sFlat1)),sFlat4)),true),
inference(cp,[status(thm)],[t4132,t2508]) ).
cnf(t6133,plain,
true = is_a_theorem(implies(implies(sFlat1,implies(a,sFlat1)),sFlat4)),
inference(step,[status(thm)],[t4147,t11]) ).
cnf(t4159,plain,
is_a_theorem(implies(implies(sFlat1,implies(a,sFlat1)),sFlat4)) = true,
inference(orient,[status(thm)],[t6133]) ).
cnf(t4160,plain,
true = ifeq(true,true,ifeq(is_a_theorem(implies(sFlat1,implies(a,sFlat1))),true,is_a_theorem(sFlat4),true),true),
inference(cp,[status(thm)],[t37,t4159]) ).
cnf(t6134,plain,
true = ifeq(is_a_theorem(implies(sFlat1,implies(a,sFlat1))),true,is_a_theorem(sFlat4),true),
inference(step,[status(thm)],[t4160,t11]) ).
cnf(t388,plain,
true = ifeq(true,true,is_a_theorem(implies(X1,implies(X2,X1))),true),
inference(cp,[status(thm)],[t361,t19]) ).
cnf(t5475,plain,
true = is_a_theorem(implies(X1,implies(X2,X1))),
inference(step,[status(thm)],[t388,t11]) ).
cnf(t625,plain,
is_a_theorem(implies(X1,implies(X2,X1))) = true,
inference(orient,[status(thm)],[t5475]) ).
cnf(t6135,plain,
true = ifeq(true,true,is_a_theorem(sFlat4),true),
inference(step,[status(thm)],[t6134,t625]) ).
cnf(t6136,plain,
true = is_a_theorem(sFlat4),
inference(step,[status(thm)],[t6135,t11]) ).
cnf(t6137,plain,
true = sFlat5,
inference(step,[status(thm)],[t6136,t69]) ).
cnf(t4169,plain,
true = sFlat5,
inference(orient,[status(thm)],[t6137]) ).
cnf(f4,negated_conjecture,
~ is_a_theorem(implies(implies(a,b),implies(implies(b,c),implies(a,c)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_cn_1) ).
fof(f4_nnf,plain,
~ is_a_theorem(implies(implies(a,b),implies(implies(b,c),implies(a,c)))),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
~ is_a_theorem(implies(implies(a,b),implies(implies(b,c),implies(a,c)))),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
~ is_a_theorem(implies(implies(a,b),implies(implies(b,c),implies(a,c)))),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(goal_0,negated_conjecture,
is_a_theorem(implies(implies(a,b),implies(implies(b,c),implies(a,c)))) != true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(g0_0,plain,
is_a_theorem(implies(sFlat0,implies(implies(b,c),implies(a,c)))) != true,
inference(rw,[status(thm)],[goal_0,t17]) ).
cnf(g0_1,plain,
is_a_theorem(implies(sFlat0,implies(sFlat1,implies(a,c)))) != true,
inference(rw,[status(thm)],[g0_0,t14]) ).
cnf(g0_2,plain,
is_a_theorem(implies(sFlat0,implies(sFlat1,sFlat2))) != true,
inference(rw,[status(thm)],[g0_1,t16]) ).
cnf(g0_3,plain,
is_a_theorem(implies(sFlat0,sFlat3)) != true,
inference(rw,[status(thm)],[g0_2,t61]) ).
cnf(g0_4,plain,
is_a_theorem(sFlat4) != true,
inference(rw,[status(thm)],[g0_3,t54]) ).
cnf(g0_5,plain,
sFlat5 != true,
inference(rw,[status(thm)],[g0_4,t69]) ).
cnf(g0_6,plain,
sFlat5 != sFlat5,
inference(rw,[status(thm)],[g0_5,t4169]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_6]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL067-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.10/0.37 % Computer : n003.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Wed Sep 23 21:50:05 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 33.87/4.78 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 33.87/4.78 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------