%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL084-2 : TPTP v9.3.1. Bugfixed v1.2.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 02:00:53 PM UTC 2026
% Result : Unsatisfiable 177.36s 23.05s
% Output : Proof 177.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 51
% Number of leaves : 4
% Syntax : Number of formulae : 132 ( 128 unt; 0 def)
% Number of atoms : 140 ( 115 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 22 ( 14 ~; 8 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 1 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 3 ( 1 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-4 aty)
% Number of variables : 462 ( 171 sgn 14 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
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(hi0,axiom,
ifeq(is_a_theorem(implies(X0,X1)),true,ifeq(is_a_theorem(X0),true,is_a_theorem(X1),true),true) = true,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(f1,axiom,
is_a_theorem(implies(implies(implies(X,Y),Z),implies(implies(Z,X),implies(U,X)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ic_JLukasiewicz) ).
fof(f1_nnf,plain,
! [X,Y,Z,U] : is_a_theorem(implies(implies(implies(X,Y),Z),implies(implies(Z,X),implies(U,X)))),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,Y,Z,U] : is_a_theorem(implies(implies(implies(X,Y),Z),implies(implies(Z,X),implies(U,X)))),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
is_a_theorem(implies(implies(implies(X0,X1),X2),implies(implies(X2,X0),implies(X3,X0)))),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(hi1,axiom,
is_a_theorem(implies(implies(implies(X0,X1),X2),implies(implies(X2,X0),implies(X3,X0)))) = true,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(f2,axiom,
is_a_theorem(implies(X,X)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ic_1) ).
fof(f2_nnf,plain,
! [X] : is_a_theorem(implies(X,X)),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X] : is_a_theorem(implies(X,X)),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
is_a_theorem(implies(X0,X0)),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(hi2,axiom,
is_a_theorem(implies(X0,X0)) = true,
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(h0,plain,
is_a_theorem(implies(implies(implies(V0,V1),V0),implies(V2,V0))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi1,hi2]) ).
cnf(h2,plain,
is_a_theorem(implies(implies(implies(V0,V1),implies(V1,V2)),implies(V3,implies(V1,V2)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi1,h0]) ).
cnf(h12,plain,
is_a_theorem(implies(implies(implies(V0,implies(V1,V2)),implies(V3,V1)),implies(V4,implies(V3,V1)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi1,h2]) ).
cnf(h18,plain,
is_a_theorem(implies(V0,implies(implies(implies(implies(V1,V2),V3),V2),implies(V1,V2)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h12,hi1]) ).
cnf(h19,plain,
is_a_theorem(implies(implies(implies(implies(V0,V1),V2),V1),implies(V0,V1))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h18,h18]) ).
cnf(h21,plain,
is_a_theorem(implies(V0,implies(V1,V0))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h19,h0]) ).
cnf(h23,plain,
is_a_theorem(implies(implies(implies(V0,implies(V1,V2)),V1),implies(V3,V1))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi1,h21]) ).
cnf(h38,plain,
is_a_theorem(implies(implies(implies(V0,V1),implies(implies(V0,V1),V2)),implies(V3,implies(implies(V0,V1),V2)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi1,h19]) ).
cnf(h50,plain,
is_a_theorem(implies(V0,implies(implies(implies(V1,implies(V2,V3)),V2),V2))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h38,h23]) ).
cnf(h1,plain,
is_a_theorem(implies(V0,implies(V1,V1))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h0,h0]) ).
cnf(h3,plain,
is_a_theorem(implies(implies(implies(V0,V0),V1),implies(V2,V1))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi1,h1]) ).
cnf(h5,plain,
is_a_theorem(implies(V0,implies(implies(implies(V1,V2),V1),implies(V3,V1)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h3,hi1]) ).
cnf(h7,plain,
is_a_theorem(implies(implies(implies(implies(implies(V0,V1),V0),implies(V2,V0)),V3),implies(V4,V3))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi1,h5]) ).
cnf(h20,plain,
is_a_theorem(implies(V0,implies(V1,implies(V2,V1)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h7,h19]) ).
cnf(h27,plain,
is_a_theorem(implies(implies(implies(V0,implies(V1,V0)),V2),implies(V3,V2))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi1,h20]) ).
cnf(h49,plain,
is_a_theorem(implies(V0,implies(implies(implies(V1,implies(V2,V1)),V3),V3))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h38,h27]) ).
cnf(h58,plain,
is_a_theorem(implies(V0,implies(implies(implies(V1,V2),V1),V1))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h38,h0]) ).
cnf(h56,plain,
is_a_theorem(implies(V0,implies(implies(implies(V1,V1),V2),V2))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h38,h3]) ).
cnf(h59,plain,
is_a_theorem(implies(implies(implies(V0,V0),V1),V1)) = true,
inference(hyper_resolution,[status(thm)],[hi0,h56,h56]) ).
cnf(h61,plain,
is_a_theorem(implies(implies(implies(V0,V1),V0),V0)) = true,
inference(hyper_resolution,[status(thm)],[hi0,h59,h58]) ).
cnf(h68,plain,
is_a_theorem(implies(implies(implies(V0,implies(V1,V0)),V2),V2)) = true,
inference(hyper_resolution,[status(thm)],[hi0,h61,h49]) ).
cnf(h71,plain,
is_a_theorem(implies(implies(implies(V0,implies(V1,V2)),V1),V1)) = true,
inference(hyper_resolution,[status(thm)],[hi0,h68,h50]) ).
cnf(h74,plain,
is_a_theorem(implies(implies(V0,implies(V1,implies(V0,V2))),implies(V3,implies(V1,implies(V0,V2))))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi1,h71]) ).
cnf(h63,plain,
is_a_theorem(implies(implies(V0,implies(V0,V1)),implies(V2,implies(V0,V1)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi1,h61]) ).
cnf(h78,plain,
is_a_theorem(implies(V0,implies(implies(V1,implies(V1,V2)),implies(V1,V2)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h63,h63]) ).
cnf(h80,plain,
is_a_theorem(implies(implies(V0,implies(V0,V1)),implies(V0,V1))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h78,h78]) ).
cnf(h139,plain,
is_a_theorem(implies(implies(V0,implies(V1,implies(V0,V2))),implies(V1,implies(V0,V2)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h80,h74]) ).
cnf(h143,plain,
is_a_theorem(implies(implies(V0,V1),implies(implies(implies(V1,V2),V0),V1))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h139,hi1]) ).
cnf(h185,plain,
is_a_theorem(implies(implies(implies(implies(implies(V0,V1),implies(V2,V1)),V3),implies(implies(V1,V4),V0)),implies(implies(V0,V1),implies(V2,V1)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h143,hi1]) ).
cnf(h187,plain,
is_a_theorem(implies(implies(implies(V0,V1),V2),implies(V1,V2))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h185,h12]) ).
cnf(h196,plain,
is_a_theorem(implies(V0,implies(implies(V0,V1),implies(V2,V1)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h187,hi1]) ).
cnf(h205,plain,
is_a_theorem(implies(implies(implies(implies(implies(V0,V1),V2),implies(V3,V2)),V0),implies(V4,V0))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi1,h196]) ).
cnf(h260,plain,
is_a_theorem(implies(implies(implies(implies(implies(V0,V1),V2),implies(V3,V2)),V0),V0)) = true,
inference(hyper_resolution,[status(thm)],[hi0,h80,h205]) ).
cnf(h182,plain,
is_a_theorem(implies(implies(implies(implies(V0,V1),V2),implies(implies(V3,implies(V1,V4)),V1)),implies(V0,V1))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h143,h23]) ).
cnf(h318,plain,
is_a_theorem(implies(implies(implies(implies(implies(V0,implies(implies(V1,V2),V3)),implies(V1,V2)),V4),V2),implies(V1,V2))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h182,h260]) ).
cnf(h91,plain,
is_a_theorem(implies(implies(implies(implies(implies(V0,V1),V0),implies(V2,V0)),V3),V3)) = true,
inference(hyper_resolution,[status(thm)],[hi0,h80,h7]) ).
cnf(h151,plain,
is_a_theorem(implies(implies(implies(implies(V0,V1),V2),implies(implies(V1,V3),V1)),implies(V0,V1))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h91,h143]) ).
cnf(h471,plain,
is_a_theorem(implies(implies(implies(V0,implies(implies(implies(V1,V2),V1),V3)),implies(implies(V1,V2),V1)),V1)) = true,
inference(hyper_resolution,[status(thm)],[hi0,h151,h318]) ).
cnf(h201,plain,
is_a_theorem(implies(implies(implies(implies(implies(V0,V1),implies(V2,V1)),V3),V0),implies(implies(V0,V1),implies(V2,V1)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h143,h196]) ).
cnf(h661,plain,
is_a_theorem(implies(implies(V0,V1),implies(implies(implies(V0,V2),V0),V1))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h201,h471]) ).
cnf(h199,plain,
is_a_theorem(implies(implies(implies(V0,implies(implies(V0,V1),implies(V2,V1))),V3),implies(V4,V3))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h196,h196]) ).
cnf(h257,plain,
is_a_theorem(implies(implies(implies(V0,implies(implies(V0,V1),implies(V2,V1))),V3),V3)) = true,
inference(hyper_resolution,[status(thm)],[hi0,h80,h199]) ).
cnf(h670,plain,
is_a_theorem(implies(implies(implies(V0,V1),V0),implies(implies(V0,V2),implies(V3,V2)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h257,h661]) ).
cnf(h92,plain,
is_a_theorem(implies(implies(implies(V0,V1),implies(V1,V2)),implies(V1,V2))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h80,h2]) ).
cnf(h93,plain,
is_a_theorem(implies(implies(implies(V0,V1),implies(V2,V0)),implies(V3,implies(V2,V0)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi1,h92]) ).
cnf(h109,plain,
is_a_theorem(implies(V0,implies(V1,implies(V2,V0)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h19,h93]) ).
cnf(h113,plain,
is_a_theorem(implies(V0,implies(V1,implies(V2,implies(V3,V1))))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h21,h109]) ).
cnf(h117,plain,
is_a_theorem(implies(implies(implies(V0,implies(V1,implies(V2,V0))),V3),implies(V4,V3))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi1,h113]) ).
cnf(h128,plain,
is_a_theorem(implies(implies(implies(V0,implies(V1,implies(V2,V0))),V3),V3)) = true,
inference(hyper_resolution,[status(thm)],[hi0,h80,h117]) ).
cnf(h146,plain,
is_a_theorem(implies(implies(implies(implies(V0,implies(V1,V2)),V3),V2),implies(V0,implies(V1,V2)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h128,h143]) ).
cnf(h694,plain,
is_a_theorem(implies(V0,implies(V1,implies(implies(V0,V2),implies(V3,V2))))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h146,h670]) ).
cnf(h178,plain,
is_a_theorem(implies(implies(implies(implies(V0,implies(V1,V2)),V3),implies(V1,implies(V1,V2))),implies(V0,implies(V1,V2)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h143,h63]) ).
cnf(h693,plain,
is_a_theorem(implies(V0,implies(implies(V0,V1),V1))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h178,h670]) ).
cnf(h200,plain,
is_a_theorem(implies(V0,implies(implies(implies(V1,V0),V2),implies(V3,V2)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h187,h196]) ).
cnf(h689,plain,
is_a_theorem(implies(implies(implies(implies(implies(V0,V1),V2),V3),implies(implies(V0,V1),V2)),implies(implies(V2,V0),implies(V4,V0)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h661,hi1]) ).
cnf(h708,plain,
is_a_theorem(implies(implies(implies(V0,V1),V2),implies(implies(V2,V0),V0))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h178,h689]) ).
cnf(h926,plain,
is_a_theorem(implies(implies(V0,implies(implies(implies(V0,V1),V2),implies(V3,V2))),implies(implies(implies(V0,V1),V2),implies(V3,V2)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h708,h260]) ).
cnf(h939,plain,
is_a_theorem(implies(implies(implies(V0,V1),implies(V2,V3)),implies(implies(V0,V3),implies(V2,V3)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h926,h694]) ).
cnf(h967,plain,
is_a_theorem(implies(implies(V0,implies(V1,V2)),implies(implies(implies(V3,implies(V0,V4)),V2),implies(V1,V2)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h939,h200]) ).
cnf(h1053,plain,
is_a_theorem(implies(implies(implies(V0,implies(V1,V2)),V3),implies(implies(V1,V3),V3))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h967,h693]) ).
cnf(h1562,plain,
is_a_theorem(implies(implies(implies(implies(V0,V1),V1),V2),implies(V0,V2))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h201,h1053]) ).
cnf(h716,plain,
is_a_theorem(implies(implies(implies(V0,implies(implies(V0,V1),V1)),V2),V2)) = true,
inference(hyper_resolution,[status(thm)],[hi0,h693,h693]) ).
cnf(h1574,plain,
is_a_theorem(implies(V0,implies(implies(implies(implies(V0,V1),V1),V2),V2))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h716,h1562]) ).
cnf(h4,plain,
is_a_theorem(implies(V0,implies(V1,implies(V2,V2)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h3,h3]) ).
cnf(h6,plain,
is_a_theorem(implies(implies(implies(V0,implies(V1,V1)),V2),implies(V3,V2))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi1,h4]) ).
cnf(h9,plain,
is_a_theorem(implies(V0,implies(implies(implies(V1,V1),V2),implies(V3,V2)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h6,hi1]) ).
cnf(h11,plain,
is_a_theorem(implies(implies(implies(implies(implies(V0,V0),V1),implies(V2,V1)),V3),implies(V4,V3))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi1,h9]) ).
cnf(h89,plain,
is_a_theorem(implies(implies(implies(implies(implies(V0,V0),V1),implies(V2,V1)),V3),V3)) = true,
inference(hyper_resolution,[status(thm)],[hi0,h80,h11]) ).
cnf(h152,plain,
is_a_theorem(implies(implies(implies(implies(V0,V1),V2),implies(implies(V3,V3),V1)),implies(V0,V1))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h89,h143]) ).
cnf(h470,plain,
is_a_theorem(implies(implies(implies(V0,implies(implies(implies(V1,V1),V2),V3)),implies(implies(V1,V1),V2)),V2)) = true,
inference(hyper_resolution,[status(thm)],[hi0,h152,h318]) ).
cnf(h473,plain,
is_a_theorem(implies(implies(V0,V1),implies(implies(implies(V2,V2),V0),V1))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h201,h470]) ).
cnf(h493,plain,
is_a_theorem(implies(implies(implies(V0,V0),V1),implies(implies(V1,V2),implies(V3,V2)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h257,h473]) ).
cnf(h682,plain,
is_a_theorem(implies(implies(implies(implies(implies(V0,V0),V1),V2),implies(implies(V0,V0),V1)),implies(implies(V1,V3),implies(V4,V3)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h661,h493]) ).
cnf(h963,plain,
is_a_theorem(implies(implies(implies(implies(implies(V0,V0),V1),V2),implies(V3,V4)),implies(implies(V1,V4),implies(V3,V4)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h939,h682]) ).
cnf(h22,plain,
is_a_theorem(implies(V0,implies(implies(V1,V0),implies(V2,V0)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h19,hi1]) ).
cnf(h28,plain,
is_a_theorem(implies(V0,implies(V1,implies(implies(V2,V1),implies(V3,V1))))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h21,h22]) ).
cnf(h34,plain,
is_a_theorem(implies(implies(implies(V0,implies(implies(V1,V0),implies(V2,V0))),V3),implies(V4,V3))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi1,h28]) ).
cnf(h86,plain,
is_a_theorem(implies(implies(implies(V0,implies(implies(V1,V0),implies(V2,V0))),V3),V3)) = true,
inference(hyper_resolution,[status(thm)],[hi0,h80,h34]) ).
cnf(h1082,plain,
is_a_theorem(implies(implies(V0,implies(V1,implies(implies(implies(V2,V2),V0),V3))),implies(implies(V4,implies(implies(implies(V2,V2),V0),V3)),implies(V1,implies(implies(implies(V2,V2),V0),V3))))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h86,h963]) ).
cnf(h1610,plain,
is_a_theorem(implies(implies(V0,implies(implies(implies(V1,V1),V2),V3)),implies(implies(implies(implies(V2,V4),V4),implies(implies(implies(V1,V1),V2),V3)),implies(implies(implies(V1,V1),V2),V3)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h1082,h1574]) ).
cnf(h208,plain,
is_a_theorem(implies(implies(implies(implies(V0,implies(V1,implies(V0,V2))),implies(V1,implies(V0,V2))),V3),implies(V4,V3))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h196,h139]) ).
cnf(h437,plain,
is_a_theorem(implies(implies(implies(implies(V0,implies(V1,implies(V0,V2))),implies(V1,implies(V0,V2))),V3),V3)) = true,
inference(hyper_resolution,[status(thm)],[hi0,h80,h208]) ).
cnf(h1657,plain,
is_a_theorem(implies(implies(implies(implies(V0,V1),V1),implies(implies(implies(V2,V2),V0),implies(V3,V4))),implies(implies(implies(V2,V2),V0),implies(V3,V4)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h437,h1610]) ).
cnf(h1662,plain,
is_a_theorem(implies(implies(implies(V0,V0),V1),implies(implies(implies(implies(V1,V2),V2),V3),implies(V4,V3)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h1657,h694]) ).
cnf(h687,plain,
is_a_theorem(implies(implies(implies(V0,V1),V0),implies(implies(implies(V2,V0),V3),implies(V4,V3)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h661,h200]) ).
cnf(h961,plain,
is_a_theorem(implies(implies(implies(V0,V1),implies(V2,V3)),implies(implies(implies(V4,V0),V3),implies(V2,V3)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h939,h687]) ).
cnf(h1028,plain,
is_a_theorem(implies(implies(implies(V0,V1),implies(V2,V3)),implies(implies(implies(V1,V4),V3),implies(V2,V3)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h257,h961]) ).
cnf(h1666,plain,
is_a_theorem(implies(implies(implies(V0,V1),implies(V2,V3)),implies(implies(implies(implies(V0,V4),V4),V3),implies(V2,V3)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h1028,h1662]) ).
cnf(h1711,plain,
is_a_theorem(implies(implies(implies(implies(V0,V1),V1),implies(V2,V3)),implies(implies(implies(V0,V4),V3),implies(V2,V3)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h257,h1666]) ).
cnf(h1029,plain,
is_a_theorem(implies(implies(implies(V0,implies(V1,V2)),implies(V3,V4)),implies(implies(V1,V4),implies(V3,V4)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h961,h939]) ).
cnf(h1063,plain,
is_a_theorem(implies(implies(implies(implies(V0,V1),implies(V2,V1)),V3),implies(V0,V3))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h201,h1029]) ).
cnf(h2435,plain,
is_a_theorem(implies(implies(V0,V1),implies(implies(implies(V0,V2),V1),implies(V3,V1)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h1063,h1711]) ).
cnf(h2475,plain,
is_a_theorem(implies(implies(implies(V0,V1),implies(V2,V3)),implies(implies(implies(implies(V0,V3),V4),V3),implies(V2,V3)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h1711,h2435]) ).
cnf(h958,plain,
is_a_theorem(implies(implies(V0,V1),implies(implies(implies(V0,V2),V1),V1))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h939,h693]) ).
cnf(h1331,plain,
is_a_theorem(implies(implies(implies(V0,V1),implies(implies(implies(V2,V0),V3),implies(V4,V3))),implies(implies(implies(V2,V0),V3),implies(V4,V3)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h958,h200]) ).
cnf(h2507,plain,
is_a_theorem(implies(implies(implies(implies(V0,V1),implies(V0,V2)),V1),implies(V3,V1))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h1331,h2475]) ).
cnf(h4428,plain,
is_a_theorem(implies(implies(implies(implies(V0,V1),implies(V0,V2)),V1),V1)) = true,
inference(hyper_resolution,[status(thm)],[hi0,h80,h2507]) ).
cnf(h697,plain,
is_a_theorem(implies(V0,implies(implies(implies(V1,V0),V2),V2))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h178,h687]) ).
cnf(h953,plain,
is_a_theorem(implies(implies(V0,implies(V1,V2)),implies(implies(implies(V0,V3),V2),implies(V1,V2)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h257,h939]) ).
cnf(h989,plain,
is_a_theorem(implies(implies(implies(V0,V1),V2),implies(implies(implies(V3,V0),V2),V2))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h953,h697]) ).
cnf(h4436,plain,
is_a_theorem(implies(implies(implies(V0,implies(implies(V1,V2),implies(V1,V3))),V2),V2)) = true,
inference(hyper_resolution,[status(thm)],[hi0,h989,h4428]) ).
cnf(h4543,plain,
is_a_theorem(implies(implies(V0,implies(V1,V2)),implies(implies(V1,V0),implies(V1,V2)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h201,h4436]) ).
cnf(h4674,plain,
is_a_theorem(implies(implies(V0,V1),implies(V0,implies(implies(V1,V2),implies(V3,V2))))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h4543,h694]) ).
cnf(h6532,plain,
is_a_theorem(implies(V0,implies(implies(V0,V1),implies(implies(V1,V2),implies(V3,V2))))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h1562,h4674]) ).
cnf(h114,plain,
is_a_theorem(implies(implies(implies(V0,implies(V1,implies(V2,V3))),V2),implies(V4,V2))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi1,h109]) ).
cnf(h125,plain,
is_a_theorem(implies(implies(implies(V0,implies(V1,implies(V2,V3))),V2),V2)) = true,
inference(hyper_resolution,[status(thm)],[hi0,h80,h114]) ).
cnf(h127,plain,
is_a_theorem(implies(implies(V0,implies(V1,implies(V2,implies(V0,V3)))),implies(V4,implies(V1,implies(V2,implies(V0,V3)))))) = true,
inference(hyper_resolution,[status(thm)],[hi0,hi1,h125]) ).
cnf(h378,plain,
is_a_theorem(implies(implies(V0,implies(V1,implies(V2,implies(V0,V3)))),implies(V1,implies(V2,implies(V0,V3))))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h80,h127]) ).
cnf(t2,plain,
is_a_theorem(implies(implies(X1,X2),implies(implies(X2,X3),implies(X1,X3)))) = true,
inference(hyper_resolution,[status(thm)],[hi0,h378,h6532]) ).
cnf(t260,plain,
is_a_theorem(implies(implies(X1,X2),implies(implies(X2,X3),implies(X1,X3)))) = true,
inference(orient,[status(thm)],[t2]) ).
cnf(f3,negated_conjecture,
~ is_a_theorem(implies(implies(a,b),implies(implies(b,c),implies(a,c)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_ic_4) ).
fof(f3_nnf,plain,
~ is_a_theorem(implies(implies(a,b),implies(implies(b,c),implies(a,c)))),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
~ is_a_theorem(implies(implies(a,b),implies(implies(b,c),implies(a,c)))),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
~ is_a_theorem(implies(implies(a,b),implies(implies(b,c),implies(a,c)))),
inference(cnf_transformation,[status(esa)],[f3_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)],[c3]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t260]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL084-2 : TPTP v9.3.1. Bugfixed v1.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.07/0.35 % Computer : n005.cluster.edu
% 0.07/0.35 % Model : x86_64 x86_64
% 0.07/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.35 % Memory : 8046.5625MB
% 0.07/0.35 % OS : Linux 6.8.0-71-generic
% 0.07/0.35 % CPULimit : 300
% 0.07/0.35 % WCLimit : 300
% 0.07/0.35 % DateTime : Wed Sep 23 21:51:47 UTC 2026
% 0.07/0.35 % CPUTime :
% 0.07/0.35 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 177.36/23.05 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 177.36/23.05 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------