%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : LCL147-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n011.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:01:04 PM UTC 2026
% Result : Unsatisfiable 96.50s 27.68s
% Output : Proof 96.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 69
% Number of leaves : 17
% Syntax : Number of formulae : 316 ( 316 unt; 0 def)
% Number of atoms : 316 ( 315 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 17 ( 17 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 4 ( 1 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 18 ( 18 usr; 14 con; 0-2 aty)
% Number of variables : 219 ( 11 sgn 24 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
cnf(f2,axiom,
implies(implies(X,Y),Y) = implies(implies(Y,X),X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wajsberg_3) ).
fof(f2_nnf,plain,
! [X,Y] : implies(implies(X,Y),Y) = implies(implies(Y,X),X),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [X,Y] : implies(implies(X,Y),Y) = implies(implies(Y,X),X),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
implies(implies(X0,X1),X1) = implies(implies(X1,X0),X0),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
cnf(t4,plain,
implies(implies(X1,X2),X2) = implies(implies(X2,X1),X1),
inference(equality_encoding,[status(esa)],[c2]) ).
cnf(t51,plain,
implies(implies(X1,X2),X2) = implies(implies(X2,X1),X1),
inference(orient,[status(thm)],[t4]) ).
cnf(f1,axiom,
implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z))) = truth,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wajsberg_2) ).
fof(f1_nnf,plain,
! [X,Y,Z] : implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z))) = truth,
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
! [X,Y,Z] : implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z))) = truth,
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2))) = truth,
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
cnf(t6,plain,
implies(implies(X1,X2),implies(implies(X2,X3),implies(X1,X3))) = truth,
inference(equality_encoding,[status(esa)],[c1]) ).
cnf(t153,plain,
implies(implies(X1,X2),implies(implies(X2,X3),implies(X1,X3))) = truth,
inference(orient,[status(thm)],[t6]) ).
cnf(t225,plain,
implies(implies(implies(implies(X1,X2),implies(X3,X2)),implies(X3,X1)),implies(X3,X1)) = implies(truth,implies(implies(X1,X2),implies(X3,X2))),
inference(cp,[status(thm)],[t51,t153]) ).
cnf(f0,axiom,
implies(truth,X) = X,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wajsberg_1) ).
fof(f0_nnf,plain,
! [X] : implies(truth,X) = X,
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
! [X] : implies(truth,X) = X,
inference(skolemisation,[status(esa)],[f0_nnf]) ).
cnf(c0,plain,
implies(truth,X0) = X0,
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(t0,plain,
implies(truth,X1) = X1,
inference(equality_encoding,[status(esa)],[c0]) ).
cnf(t17,plain,
implies(truth,X1) = X1,
inference(orient,[status(thm)],[t0]) ).
cnf(t47113,plain,
implies(implies(implies(implies(X1,X2),implies(X3,X2)),implies(X3,X1)),implies(X3,X1)) = implies(implies(X1,X2),implies(X3,X2)),
inference(step,[status(thm)],[t225,t17]) ).
cnf(t15328,plain,
implies(implies(implies(implies(X1,X2),implies(X3,X2)),implies(X3,X1)),implies(X3,X1)) = implies(implies(X1,X2),implies(X3,X2)),
inference(orient,[status(thm)],[t47113]) ).
cnf(f3,axiom,
implies(implies(not(X),not(Y)),implies(Y,X)) = truth,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',wajsberg_4) ).
fof(f3_nnf,plain,
! [X,Y] : implies(implies(not(X),not(Y)),implies(Y,X)) = truth,
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
! [X,Y] : implies(implies(not(X),not(Y)),implies(Y,X)) = truth,
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
implies(implies(not(X0),not(X1)),implies(X1,X0)) = truth,
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
cnf(t5,plain,
implies(implies(not(X1),not(X2)),implies(X2,X1)) = truth,
inference(equality_encoding,[status(esa)],[c3]) ).
cnf(t85,plain,
implies(implies(not(X1),not(X2)),implies(X2,X1)) = truth,
inference(orient,[status(thm)],[t5]) ).
cnf(t86,plain,
truth = implies(implies(not(X1),not(truth)),X1),
inference(cp,[status(thm)],[t85,t17]) ).
cnf(t106,plain,
implies(implies(not(X1),not(truth)),X1) = truth,
inference(orient,[status(thm)],[t86]) ).
cnf(t194,plain,
truth = implies(truth,implies(implies(X1,X2),implies(implies(not(X1),not(truth)),X2))),
inference(cp,[status(thm)],[t153,t106]) ).
cnf(t46885,plain,
truth = implies(implies(X1,X2),implies(implies(not(X1),not(truth)),X2)),
inference(step,[status(thm)],[t194,t17]) ).
cnf(t8576,plain,
implies(implies(X1,X2),implies(implies(not(X1),not(truth)),X2)) = truth,
inference(orient,[status(thm)],[t46885]) ).
cnf(t8577,plain,
truth = implies(implies(X1,not(truth)),implies(implies(not(truth),not(X1)),not(X1))),
inference(cp,[status(thm)],[t8576,t51]) ).
cnf(t192,plain,
truth = implies(implies(X1,implies(not(X2),not(X3))),implies(truth,implies(X1,implies(X3,X2)))),
inference(cp,[status(thm)],[t153,t85]) ).
cnf(t46874,plain,
truth = implies(implies(X1,implies(not(X2),not(X3))),implies(X1,implies(X3,X2))),
inference(step,[status(thm)],[t192,t17]) ).
cnf(t8182,plain,
implies(implies(X1,implies(not(X2),not(X3))),implies(X1,implies(X3,X2))) = truth,
inference(orient,[status(thm)],[t46874]) ).
cnf(t154,plain,
truth = implies(X1,implies(implies(X1,X2),implies(truth,X2))),
inference(cp,[status(thm)],[t153,t17]) ).
cnf(t46331,plain,
truth = implies(X1,implies(implies(X1,X2),X2)),
inference(step,[status(thm)],[t154,t17]) ).
cnf(t233,plain,
implies(X1,implies(implies(X1,X2),X2)) = truth,
inference(orient,[status(thm)],[t46331]) ).
cnf(t52,plain,
implies(implies(X1,truth),truth) = implies(X1,X1),
inference(cp,[status(thm)],[t51,t17]) ).
cnf(t76,plain,
implies(implies(X1,truth),truth) = implies(X1,X1),
inference(orient,[status(thm)],[t52]) ).
cnf(t248,plain,
truth = implies(X1,implies(X1,X1)),
inference(cp,[status(thm)],[t233,t76]) ).
cnf(t234,plain,
truth = implies(implies(truth,X1),X1),
inference(cp,[status(thm)],[t233,t17]) ).
cnf(t46332,plain,
truth = implies(X1,X1),
inference(step,[status(thm)],[t234,t17]) ).
cnf(t259,plain,
implies(X1,X1) = truth,
inference(orient,[status(thm)],[t46332]) ).
cnf(t46353,plain,
truth = implies(X1,truth),
inference(step,[status(thm)],[t248,t259]) ).
cnf(t352,plain,
implies(X1,truth) = truth,
inference(orient,[status(thm)],[t46353]) ).
cnf(t356,plain,
truth = implies(truth,implies(implies(truth,X1),implies(X2,X1))),
inference(cp,[status(thm)],[t153,t352]) ).
cnf(t46376,plain,
truth = implies(implies(truth,X1),implies(X2,X1)),
inference(step,[status(thm)],[t356,t17]) ).
cnf(t46377,plain,
truth = implies(X1,implies(X2,X1)),
inference(step,[status(thm)],[t46376,t17]) ).
cnf(t407,plain,
implies(X1,implies(X2,X1)) = truth,
inference(orient,[status(thm)],[t46377]) ).
cnf(t8185,plain,
truth = implies(truth,implies(not(X1),implies(X1,X2))),
inference(cp,[status(thm)],[t8182,t407]) ).
cnf(t46875,plain,
truth = implies(not(X1),implies(X1,X2)),
inference(step,[status(thm)],[t8185,t17]) ).
cnf(t8256,plain,
implies(not(X1),implies(X1,X2)) = truth,
inference(orient,[status(thm)],[t46875]) ).
cnf(t8257,plain,
truth = implies(not(truth),X1),
inference(cp,[status(thm)],[t8256,t17]) ).
cnf(t8364,plain,
implies(not(truth),X1) = truth,
inference(orient,[status(thm)],[t8257]) ).
cnf(t47309,plain,
truth = implies(implies(X1,not(truth)),implies(truth,not(X1))),
inference(step,[status(thm)],[t8577,t8364]) ).
cnf(t47310,plain,
truth = implies(implies(X1,not(truth)),not(X1)),
inference(step,[status(thm)],[t47309,t17]) ).
cnf(t18617,plain,
implies(implies(X1,not(truth)),not(X1)) = truth,
inference(orient,[status(thm)],[t47310]) ).
cnf(t18619,plain,
implies(implies(not(X1),implies(X1,not(truth))),implies(X1,not(truth))) = implies(truth,not(X1)),
inference(cp,[status(thm)],[t51,t18617]) ).
cnf(t47311,plain,
implies(truth,implies(X1,not(truth))) = implies(truth,not(X1)),
inference(step,[status(thm)],[t18619,t8256]) ).
cnf(t47312,plain,
implies(X1,not(truth)) = implies(truth,not(X1)),
inference(step,[status(thm)],[t47311,t17]) ).
cnf(t47313,plain,
implies(X1,not(truth)) = not(X1),
inference(step,[status(thm)],[t47312,t17]) ).
cnf(t18639,plain,
implies(X1,not(truth)) = not(X1),
inference(orient,[status(thm)],[t47313]) ).
cnf(t18735,plain,
implies(implies(X1,not(truth)),implies(X2,not(truth))) = implies(implies(implies(not(X1),implies(X2,not(truth))),implies(X2,X1)),implies(X2,X1)),
inference(cp,[status(thm)],[t15328,t18639]) ).
cnf(t47347,plain,
implies(not(X1),implies(X2,not(truth))) = implies(implies(implies(not(X1),implies(X2,not(truth))),implies(X2,X1)),implies(X2,X1)),
inference(step,[status(thm)],[t18735,t18639]) ).
cnf(t47348,plain,
implies(not(X1),not(X2)) = implies(implies(implies(not(X1),implies(X2,not(truth))),implies(X2,X1)),implies(X2,X1)),
inference(step,[status(thm)],[t47347,t18639]) ).
cnf(t47349,plain,
implies(not(X1),not(X2)) = implies(implies(implies(not(X1),not(X2)),implies(X2,X1)),implies(X2,X1)),
inference(step,[status(thm)],[t47348,t18639]) ).
cnf(t47350,plain,
implies(not(X1),not(X2)) = implies(truth,implies(X2,X1)),
inference(step,[status(thm)],[t47349,t85]) ).
cnf(t47351,plain,
implies(not(X1),not(X2)) = implies(X2,X1),
inference(step,[status(thm)],[t47350,t17]) ).
cnf(t21169,plain,
implies(not(X1),not(X2)) = implies(X2,X1),
inference(orient,[status(thm)],[t47351]) ).
cnf(t9,axiom,
sF2 = implies(y,z),
introduced(definition) ).
cnf(t19,plain,
implies(y,z) = sF2,
inference(orient,[status(thm)],[t9]) ).
cnf(t7,axiom,
sF0 = implies(x,z),
introduced(definition) ).
cnf(t18,plain,
implies(x,z) = sF0,
inference(orient,[status(thm)],[t7]) ).
cnf(t8,axiom,
sF1 = not(implies(x,z)),
introduced(definition) ).
cnf(t46316,plain,
sF1 = not(sF0),
inference(step,[status(thm)],[t8,t18]) ).
cnf(t21,plain,
not(sF0) = sF1,
inference(orient,[status(thm)],[t46316]) ).
cnf(t90,plain,
truth = implies(implies(sF1,not(X1)),implies(X1,sF0)),
inference(cp,[status(thm)],[t85,t21]) ).
cnf(t1089,plain,
implies(implies(sF1,not(X1)),implies(X1,sF0)) = truth,
inference(orient,[status(thm)],[t90]) ).
cnf(t10,axiom,
sF3 = not(implies(y,z)),
introduced(definition) ).
cnf(t46317,plain,
sF3 = not(sF2),
inference(step,[status(thm)],[t10,t19]) ).
cnf(t22,plain,
not(sF2) = sF3,
inference(orient,[status(thm)],[t46317]) ).
cnf(t1090,plain,
truth = implies(implies(sF1,sF3),implies(sF2,sF0)),
inference(cp,[status(thm)],[t1089,t22]) ).
cnf(t11,axiom,
sF4 = implies(not(implies(x,z)),not(implies(y,z))),
introduced(definition) ).
cnf(t46336,plain,
sF4 = implies(not(sF0),not(implies(y,z))),
inference(step,[status(thm)],[t11,t18]) ).
cnf(t46337,plain,
sF4 = implies(sF1,not(implies(y,z))),
inference(step,[status(thm)],[t46336,t21]) ).
cnf(t46338,plain,
sF4 = implies(sF1,not(sF2)),
inference(step,[status(thm)],[t46337,t19]) ).
cnf(t46339,plain,
sF4 = implies(sF1,sF3),
inference(step,[status(thm)],[t46338,t22]) ).
cnf(t282,plain,
implies(sF1,sF3) = sF4,
inference(orient,[status(thm)],[t46339]) ).
cnf(t46444,plain,
truth = implies(sF4,implies(sF2,sF0)),
inference(step,[status(thm)],[t1090,t282]) ).
cnf(t1104,plain,
implies(sF4,implies(sF2,sF0)) = truth,
inference(orient,[status(thm)],[t46444]) ).
cnf(t1107,plain,
implies(implies(implies(sF2,sF0),sF4),sF4) = implies(truth,implies(sF2,sF0)),
inference(cp,[status(thm)],[t51,t1104]) ).
cnf(t46518,plain,
implies(implies(implies(sF2,sF0),sF4),sF4) = implies(sF2,sF0),
inference(step,[status(thm)],[t1107,t17]) ).
cnf(t1953,plain,
implies(implies(implies(sF2,sF0),sF4),sF4) = implies(sF2,sF0),
inference(orient,[status(thm)],[t46518]) ).
cnf(t11282,plain,
implies(truth,sF4) = implies(sF2,sF0),
inference(rw,[status(thm)],[t1953]) ).
cnf(t47036,plain,
sF4 = implies(sF2,sF0),
inference(step,[status(thm)],[t11282,t17]) ).
cnf(t11303,plain,
implies(sF2,sF0) = sF4,
inference(orient,[status(thm)],[t47036]) ).
cnf(t12,axiom,
sF5 = implies(implies(not(implies(x,z)),not(implies(y,z))),not(implies(y,z))),
introduced(definition) ).
cnf(t46344,plain,
sF5 = implies(implies(not(implies(y,z)),not(implies(x,z))),not(implies(x,z))),
inference(step,[status(thm)],[t12,t51]) ).
cnf(t46345,plain,
sF5 = implies(implies(not(sF2),not(implies(x,z))),not(implies(x,z))),
inference(step,[status(thm)],[t46344,t19]) ).
cnf(t46346,plain,
sF5 = implies(implies(not(implies(x,z)),not(sF2)),not(sF2)),
inference(step,[status(thm)],[t46345,t51]) ).
cnf(t46347,plain,
sF5 = implies(implies(not(sF0),not(sF2)),not(sF2)),
inference(step,[status(thm)],[t46346,t18]) ).
cnf(t46348,plain,
sF5 = implies(implies(sF1,not(sF2)),not(sF2)),
inference(step,[status(thm)],[t46347,t21]) ).
cnf(t46349,plain,
sF5 = implies(implies(not(sF2),sF1),sF1),
inference(step,[status(thm)],[t46348,t51]) ).
cnf(t46350,plain,
sF5 = implies(implies(sF3,sF1),sF1),
inference(step,[status(thm)],[t46349,t22]) ).
cnf(t46351,plain,
sF5 = implies(implies(sF1,sF3),sF3),
inference(step,[status(thm)],[t46350,t51]) ).
cnf(t46352,plain,
sF5 = implies(sF4,sF3),
inference(step,[status(thm)],[t46351,t282]) ).
cnf(t343,plain,
implies(sF4,sF3) = sF5,
inference(orient,[status(thm)],[t46352]) ).
cnf(t13,axiom,
sF6 = not(implies(implies(not(implies(x,z)),not(implies(y,z))),not(implies(y,z)))),
introduced(definition) ).
cnf(t46360,plain,
sF6 = not(implies(implies(not(implies(y,z)),not(implies(x,z))),not(implies(x,z)))),
inference(step,[status(thm)],[t13,t51]) ).
cnf(t46361,plain,
sF6 = not(implies(implies(not(sF2),not(implies(x,z))),not(implies(x,z)))),
inference(step,[status(thm)],[t46360,t19]) ).
cnf(t46362,plain,
sF6 = not(implies(implies(not(implies(x,z)),not(sF2)),not(sF2))),
inference(step,[status(thm)],[t46361,t51]) ).
cnf(t46363,plain,
sF6 = not(implies(implies(not(sF0),not(sF2)),not(sF2))),
inference(step,[status(thm)],[t46362,t18]) ).
cnf(t46364,plain,
sF6 = not(implies(implies(sF1,not(sF2)),not(sF2))),
inference(step,[status(thm)],[t46363,t21]) ).
cnf(t46365,plain,
sF6 = not(implies(implies(not(sF2),sF1),sF1)),
inference(step,[status(thm)],[t46364,t51]) ).
cnf(t46366,plain,
sF6 = not(implies(implies(sF3,sF1),sF1)),
inference(step,[status(thm)],[t46365,t22]) ).
cnf(t46367,plain,
sF6 = not(implies(implies(sF1,sF3),sF3)),
inference(step,[status(thm)],[t46366,t51]) ).
cnf(t46368,plain,
sF6 = not(implies(sF4,sF3)),
inference(step,[status(thm)],[t46367,t282]) ).
cnf(t46369,plain,
sF6 = not(sF5),
inference(step,[status(thm)],[t46368,t343]) ).
cnf(t381,plain,
not(sF5) = sF6,
inference(orient,[status(thm)],[t46369]) ).
cnf(t14,axiom,
sF7 = implies(x,y),
introduced(definition) ).
cnf(t20,plain,
implies(x,y) = sF7,
inference(orient,[status(thm)],[t14]) ).
cnf(t15,axiom,
sF8 = implies(implies(x,y),y),
introduced(definition) ).
cnf(t46318,plain,
sF8 = implies(sF7,y),
inference(step,[status(thm)],[t15,t20]) ).
cnf(t24,plain,
implies(sF7,y) = sF8,
inference(orient,[status(thm)],[t46318]) ).
cnf(t16,axiom,
sF9 = implies(implies(implies(x,y),y),z),
introduced(definition) ).
cnf(t46319,plain,
sF9 = implies(implies(sF7,y),z),
inference(step,[status(thm)],[t16,t20]) ).
cnf(t46320,plain,
sF9 = implies(sF8,z),
inference(step,[status(thm)],[t46319,t24]) ).
cnf(t25,plain,
implies(sF8,z) = sF9,
inference(orient,[status(thm)],[t46320]) ).
cnf(t170,plain,
truth = implies(implies(sF8,X1),implies(implies(X1,z),sF9)),
inference(cp,[status(thm)],[t153,t25]) ).
cnf(t4174,plain,
implies(implies(sF8,X1),implies(implies(X1,z),sF9)) = truth,
inference(orient,[status(thm)],[t170]) ).
cnf(t173,plain,
truth = implies(implies(implies(X1,X2),X3),implies(implies(X3,X2),implies(implies(X2,X1),X1))),
inference(cp,[status(thm)],[t153,t51]) ).
cnf(t5602,plain,
implies(implies(implies(X1,X2),X3),implies(implies(X3,X2),implies(implies(X2,X1),X1))) = truth,
inference(orient,[status(thm)],[t173]) ).
cnf(t164,plain,
truth = implies(implies(x,X1),implies(implies(X1,y),sF7)),
inference(cp,[status(thm)],[t153,t20]) ).
cnf(t3510,plain,
implies(implies(x,X1),implies(implies(X1,y),sF7)) = truth,
inference(orient,[status(thm)],[t164]) ).
cnf(t235,plain,
truth = implies(x,implies(sF0,z)),
inference(cp,[status(thm)],[t233,t18]) ).
cnf(t295,plain,
implies(x,implies(sF0,z)) = truth,
inference(orient,[status(thm)],[t235]) ).
cnf(t300,plain,
truth = implies(truth,implies(implies(implies(sF0,z),X1),implies(x,X1))),
inference(cp,[status(thm)],[t153,t295]) ).
cnf(t46807,plain,
truth = implies(implies(implies(sF0,z),X1),implies(x,X1)),
inference(step,[status(thm)],[t300,t17]) ).
cnf(t6816,plain,
implies(implies(implies(sF0,z),X1),implies(x,X1)) = truth,
inference(orient,[status(thm)],[t46807]) ).
cnf(t383,plain,
truth = implies(implies(not(X1),sF6),implies(sF5,X1)),
inference(cp,[status(thm)],[t85,t381]) ).
cnf(t2416,plain,
implies(implies(not(X1),sF6),implies(sF5,X1)) = truth,
inference(orient,[status(thm)],[t383]) ).
cnf(t196,plain,
truth = implies(implies(X1,implies(not(X2),not(truth))),implies(truth,implies(X1,X2))),
inference(cp,[status(thm)],[t153,t106]) ).
cnf(t46894,plain,
truth = implies(implies(X1,implies(not(X2),not(truth))),implies(X1,X2)),
inference(step,[status(thm)],[t196,t17]) ).
cnf(t9016,plain,
implies(implies(X1,implies(not(X2),not(truth))),implies(X1,X2)) = truth,
inference(orient,[status(thm)],[t46894]) ).
cnf(t9017,plain,
truth = implies(truth,implies(implies(not(not(truth)),not(not(X1))),X1)),
inference(cp,[status(thm)],[t9016,t85]) ).
cnf(t46902,plain,
truth = implies(implies(not(not(truth)),not(not(X1))),X1),
inference(step,[status(thm)],[t9017,t17]) ).
cnf(t58,plain,
implies(implies(X1,implies(X2,X1)),implies(X2,X1)) = implies(implies(implies(X1,X2),X2),X1),
inference(cp,[status(thm)],[t51,t51]) ).
cnf(t46380,plain,
implies(truth,implies(X2,X1)) = implies(implies(implies(X1,X2),X2),X1),
inference(step,[status(thm)],[t58,t407]) ).
cnf(t46381,plain,
implies(X2,X1) = implies(implies(implies(X1,X2),X2),X1),
inference(step,[status(thm)],[t46380,t17]) ).
cnf(t421,plain,
implies(implies(implies(X1,X2),X2),X1) = implies(X2,X1),
inference(orient,[status(thm)],[t46381]) ).
cnf(t430,plain,
implies(not(truth),not(not(truth))) = implies(truth,not(not(truth))),
inference(cp,[status(thm)],[t421,t106]) ).
cnf(t46399,plain,
implies(not(truth),not(not(truth))) = not(not(truth)),
inference(step,[status(thm)],[t430,t17]) ).
cnf(t672,plain,
implies(not(truth),not(not(truth))) = not(not(truth)),
inference(orient,[status(thm)],[t46399]) ).
cnf(t46878,plain,
truth = not(not(truth)),
inference(step,[status(thm)],[t672,t8364]) ).
cnf(t8365,plain,
truth = not(not(truth)),
inference(rw,[status(thm)],[t46878]) ).
cnf(t8392,plain,
not(not(truth)) = truth,
inference(orient,[status(thm)],[t8365]) ).
cnf(t46903,plain,
truth = implies(implies(truth,not(not(X1))),X1),
inference(step,[status(thm)],[t46902,t8392]) ).
cnf(t46904,plain,
truth = implies(not(not(X1)),X1),
inference(step,[status(thm)],[t46903,t17]) ).
cnf(t9191,plain,
implies(not(not(X1)),X1) = truth,
inference(orient,[status(thm)],[t46904]) ).
cnf(t9231,plain,
truth = implies(truth,implies(sF5,not(sF6))),
inference(cp,[status(thm)],[t2416,t9191]) ).
cnf(t46942,plain,
truth = implies(sF5,not(sF6)),
inference(step,[status(thm)],[t9231,t17]) ).
cnf(t9544,plain,
implies(sF5,not(sF6)) = truth,
inference(orient,[status(thm)],[t46942]) ).
cnf(t9547,plain,
implies(implies(not(sF6),sF5),sF5) = implies(truth,not(sF6)),
inference(cp,[status(thm)],[t51,t9544]) ).
cnf(t9194,plain,
truth = implies(not(sF6),sF5),
inference(cp,[status(thm)],[t9191,t381]) ).
cnf(t9312,plain,
implies(not(sF6),sF5) = truth,
inference(orient,[status(thm)],[t9194]) ).
cnf(t46943,plain,
implies(truth,sF5) = implies(truth,not(sF6)),
inference(step,[status(thm)],[t9547,t9312]) ).
cnf(t46944,plain,
sF5 = implies(truth,not(sF6)),
inference(step,[status(thm)],[t46943,t17]) ).
cnf(t46945,plain,
sF5 = not(sF6),
inference(step,[status(thm)],[t46944,t17]) ).
cnf(t9568,plain,
not(sF6) = sF5,
inference(orient,[status(thm)],[t46945]) ).
cnf(t9575,plain,
truth = implies(implies(sF1,sF5),implies(sF6,sF0)),
inference(cp,[status(thm)],[t1089,t9568]) ).
cnf(t290,plain,
truth = implies(sF1,implies(sF4,sF3)),
inference(cp,[status(thm)],[t233,t282]) ).
cnf(t46358,plain,
truth = implies(sF1,sF5),
inference(step,[status(thm)],[t290,t343]) ).
cnf(t374,plain,
implies(sF1,sF5) = truth,
inference(orient,[status(thm)],[t46358]) ).
cnf(t46947,plain,
truth = implies(truth,implies(sF6,sF0)),
inference(step,[status(thm)],[t9575,t374]) ).
cnf(t46948,plain,
truth = implies(sF6,sF0),
inference(step,[status(thm)],[t46947,t17]) ).
cnf(t9622,plain,
implies(sF6,sF0) = truth,
inference(orient,[status(thm)],[t46948]) ).
cnf(t9626,plain,
truth = implies(truth,implies(implies(sF0,X1),implies(sF6,X1))),
inference(cp,[status(thm)],[t153,t9622]) ).
cnf(t47557,plain,
truth = implies(implies(sF0,X1),implies(sF6,X1)),
inference(step,[status(thm)],[t9626,t17]) ).
cnf(t28723,plain,
implies(implies(sF0,X1),implies(sF6,X1)) = truth,
inference(orient,[status(thm)],[t47557]) ).
cnf(t28747,plain,
truth = implies(truth,implies(x,implies(sF6,z))),
inference(cp,[status(thm)],[t6816,t28723]) ).
cnf(t47558,plain,
truth = implies(x,implies(sF6,z)),
inference(step,[status(thm)],[t28747,t17]) ).
cnf(t28767,plain,
implies(x,implies(sF6,z)) = truth,
inference(orient,[status(thm)],[t47558]) ).
cnf(t28777,plain,
truth = implies(truth,implies(implies(implies(sF6,z),y),sF7)),
inference(cp,[status(thm)],[t3510,t28767]) ).
cnf(t48041,plain,
truth = implies(implies(implies(sF6,z),y),sF7),
inference(step,[status(thm)],[t28777,t17]) ).
cnf(t45894,plain,
implies(implies(implies(sF6,z),y),sF7) = truth,
inference(orient,[status(thm)],[t48041]) ).
cnf(t45907,plain,
truth = implies(truth,implies(implies(sF7,y),implies(implies(y,implies(sF6,z)),implies(sF6,z)))),
inference(cp,[status(thm)],[t5602,t45894]) ).
cnf(t48042,plain,
truth = implies(implies(sF7,y),implies(implies(y,implies(sF6,z)),implies(sF6,z))),
inference(step,[status(thm)],[t45907,t17]) ).
cnf(t48043,plain,
truth = implies(sF8,implies(implies(y,implies(sF6,z)),implies(sF6,z))),
inference(step,[status(thm)],[t48042,t24]) ).
cnf(t236,plain,
truth = implies(y,implies(sF2,z)),
inference(cp,[status(thm)],[t233,t19]) ).
cnf(t303,plain,
implies(y,implies(sF2,z)) = truth,
inference(orient,[status(thm)],[t236]) ).
cnf(t308,plain,
truth = implies(truth,implies(implies(implies(sF2,z),X1),implies(y,X1))),
inference(cp,[status(thm)],[t153,t303]) ).
cnf(t46820,plain,
truth = implies(implies(implies(sF2,z),X1),implies(y,X1)),
inference(step,[status(thm)],[t308,t17]) ).
cnf(t7112,plain,
implies(implies(implies(sF2,z),X1),implies(y,X1)) = truth,
inference(orient,[status(thm)],[t46820]) ).
cnf(t92,plain,
truth = implies(implies(sF3,not(X1)),implies(X1,sF2)),
inference(cp,[status(thm)],[t85,t22]) ).
cnf(t1268,plain,
implies(implies(sF3,not(X1)),implies(X1,sF2)) = truth,
inference(orient,[status(thm)],[t92]) ).
cnf(t9577,plain,
truth = implies(implies(sF3,sF5),implies(sF6,sF2)),
inference(cp,[status(thm)],[t1268,t9568]) ).
cnf(t415,plain,
truth = implies(sF3,sF5),
inference(cp,[status(thm)],[t407,t343]) ).
cnf(t470,plain,
implies(sF3,sF5) = truth,
inference(orient,[status(thm)],[t415]) ).
cnf(t46949,plain,
truth = implies(truth,implies(sF6,sF2)),
inference(step,[status(thm)],[t9577,t470]) ).
cnf(t46950,plain,
truth = implies(sF6,sF2),
inference(step,[status(thm)],[t46949,t17]) ).
cnf(t9641,plain,
implies(sF6,sF2) = truth,
inference(orient,[status(thm)],[t46950]) ).
cnf(t9645,plain,
truth = implies(truth,implies(implies(sF2,X1),implies(sF6,X1))),
inference(cp,[status(thm)],[t153,t9641]) ).
cnf(t47565,plain,
truth = implies(implies(sF2,X1),implies(sF6,X1)),
inference(step,[status(thm)],[t9645,t17]) ).
cnf(t28917,plain,
implies(implies(sF2,X1),implies(sF6,X1)) = truth,
inference(orient,[status(thm)],[t47565]) ).
cnf(t28939,plain,
truth = implies(truth,implies(y,implies(sF6,z))),
inference(cp,[status(thm)],[t7112,t28917]) ).
cnf(t47566,plain,
truth = implies(y,implies(sF6,z)),
inference(step,[status(thm)],[t28939,t17]) ).
cnf(t28959,plain,
implies(y,implies(sF6,z)) = truth,
inference(orient,[status(thm)],[t47566]) ).
cnf(t48044,plain,
truth = implies(sF8,implies(truth,implies(sF6,z))),
inference(step,[status(thm)],[t48043,t28959]) ).
cnf(t48045,plain,
truth = implies(sF8,implies(sF6,z)),
inference(step,[status(thm)],[t48044,t17]) ).
cnf(t45930,plain,
implies(sF8,implies(sF6,z)) = truth,
inference(orient,[status(thm)],[t48045]) ).
cnf(t45940,plain,
truth = implies(truth,implies(implies(implies(sF6,z),z),sF9)),
inference(cp,[status(thm)],[t4174,t45930]) ).
cnf(t48047,plain,
truth = implies(implies(implies(sF6,z),z),sF9),
inference(step,[status(thm)],[t45940,t17]) ).
cnf(t349,plain,
truth = implies(implies(X1,sF4),implies(sF5,implies(X1,sF3))),
inference(cp,[status(thm)],[t153,t343]) ).
cnf(t7588,plain,
implies(implies(X1,sF4),implies(sF5,implies(X1,sF3))) = truth,
inference(orient,[status(thm)],[t349]) ).
cnf(t21214,plain,
implies(sF2,X1) = implies(not(X1),sF3),
inference(cp,[status(thm)],[t21169,t22]) ).
cnf(t22351,plain,
implies(not(X1),sF3) = implies(sF2,X1),
inference(orient,[status(thm)],[t21214]) ).
cnf(t22363,plain,
implies(implies(sF3,not(X1)),not(X1)) = implies(implies(sF2,X1),sF3),
inference(cp,[status(thm)],[t51,t22351]) ).
cnf(t21213,plain,
implies(X1,sF2) = implies(sF3,not(X1)),
inference(cp,[status(thm)],[t21169,t22]) ).
cnf(t22215,plain,
implies(sF3,not(X1)) = implies(X1,sF2),
inference(orient,[status(thm)],[t21213]) ).
cnf(t47451,plain,
implies(implies(X1,sF2),not(X1)) = implies(implies(sF2,X1),sF3),
inference(step,[status(thm)],[t22363,t22215]) ).
cnf(t25086,plain,
implies(implies(X1,sF2),not(X1)) = implies(implies(sF2,X1),sF3),
inference(orient,[status(thm)],[t47451]) ).
cnf(t411,plain,
truth = implies(z,sF2),
inference(cp,[status(thm)],[t407,t19]) ).
cnf(t447,plain,
implies(z,sF2) = truth,
inference(orient,[status(thm)],[t411]) ).
cnf(t25089,plain,
implies(implies(sF2,z),sF3) = implies(truth,not(z)),
inference(cp,[status(thm)],[t25086,t447]) ).
cnf(t47452,plain,
implies(implies(sF2,z),sF3) = not(z),
inference(step,[status(thm)],[t25089,t17]) ).
cnf(t25153,plain,
implies(implies(sF2,z),sF3) = not(z),
inference(orient,[status(thm)],[t47452]) ).
cnf(t25173,plain,
truth = implies(implies(implies(sF2,z),sF4),implies(sF5,not(z))),
inference(cp,[status(thm)],[t7588,t25153]) ).
cnf(t410,plain,
truth = implies(z,sF0),
inference(cp,[status(thm)],[t407,t18]) ).
cnf(t442,plain,
implies(z,sF0) = truth,
inference(orient,[status(thm)],[t410]) ).
cnf(t446,plain,
truth = implies(implies(X1,z),implies(truth,implies(X1,sF0))),
inference(cp,[status(thm)],[t153,t442]) ).
cnf(t46431,plain,
truth = implies(implies(X1,z),implies(X1,sF0)),
inference(step,[status(thm)],[t446,t17]) ).
cnf(t942,plain,
implies(implies(X1,z),implies(X1,sF0)) = truth,
inference(orient,[status(thm)],[t46431]) ).
cnf(t11342,plain,
truth = implies(implies(sF2,z),sF4),
inference(cp,[status(thm)],[t942,t11303]) ).
cnf(t11670,plain,
implies(implies(sF2,z),sF4) = truth,
inference(orient,[status(thm)],[t11342]) ).
cnf(t47453,plain,
truth = implies(truth,implies(sF5,not(z))),
inference(step,[status(thm)],[t25173,t11670]) ).
cnf(t47454,plain,
truth = implies(sF5,not(z)),
inference(step,[status(thm)],[t47453,t17]) ).
cnf(t21221,plain,
implies(X1,sF6) = implies(sF5,not(X1)),
inference(cp,[status(thm)],[t21169,t9568]) ).
cnf(t23355,plain,
implies(sF5,not(X1)) = implies(X1,sF6),
inference(orient,[status(thm)],[t21221]) ).
cnf(t47455,plain,
truth = implies(z,sF6),
inference(step,[status(thm)],[t47454,t23355]) ).
cnf(t25198,plain,
implies(z,sF6) = truth,
inference(orient,[status(thm)],[t47455]) ).
cnf(t25203,plain,
implies(implies(sF6,z),z) = implies(truth,sF6),
inference(cp,[status(thm)],[t51,t25198]) ).
cnf(t47464,plain,
implies(implies(sF6,z),z) = sF6,
inference(step,[status(thm)],[t25203,t17]) ).
cnf(t25312,plain,
implies(implies(sF6,z),z) = sF6,
inference(orient,[status(thm)],[t47464]) ).
cnf(t48048,plain,
truth = implies(sF6,sF9),
inference(step,[status(thm)],[t48047,t25312]) ).
cnf(t45969,plain,
implies(sF6,sF9) = truth,
inference(orient,[status(thm)],[t48048]) ).
cnf(t45978,plain,
implies(implies(sF9,sF6),sF6) = implies(truth,sF9),
inference(cp,[status(thm)],[t51,t45969]) ).
cnf(t55,plain,
implies(implies(y,x),x) = implies(sF7,y),
inference(cp,[status(thm)],[t51,t20]) ).
cnf(t46321,plain,
implies(implies(y,x),x) = sF8,
inference(step,[status(thm)],[t55,t24]) ).
cnf(t69,plain,
implies(implies(y,x),x) = sF8,
inference(orient,[status(thm)],[t46321]) ).
cnf(t246,plain,
truth = implies(y,sF8),
inference(cp,[status(thm)],[t233,t69]) ).
cnf(t274,plain,
implies(y,sF8) = truth,
inference(orient,[status(thm)],[t246]) ).
cnf(t279,plain,
truth = implies(truth,implies(implies(sF8,X1),implies(y,X1))),
inference(cp,[status(thm)],[t153,t274]) ).
cnf(t46414,plain,
truth = implies(implies(sF8,X1),implies(y,X1)),
inference(step,[status(thm)],[t279,t17]) ).
cnf(t772,plain,
implies(implies(sF8,X1),implies(y,X1)) = truth,
inference(orient,[status(thm)],[t46414]) ).
cnf(t773,plain,
truth = implies(implies(sF8,z),sF2),
inference(cp,[status(thm)],[t772,t19]) ).
cnf(t46415,plain,
truth = implies(sF9,sF2),
inference(step,[status(thm)],[t773,t25]) ).
cnf(t786,plain,
implies(sF9,sF2) = truth,
inference(orient,[status(thm)],[t46415]) ).
cnf(t25090,plain,
implies(implies(sF2,sF9),sF3) = implies(truth,not(sF9)),
inference(cp,[status(thm)],[t25086,t786]) ).
cnf(t47457,plain,
implies(implies(sF2,sF9),sF3) = not(sF9),
inference(step,[status(thm)],[t25090,t17]) ).
cnf(t25234,plain,
implies(implies(sF2,sF9),sF3) = not(sF9),
inference(orient,[status(thm)],[t47457]) ).
cnf(t25253,plain,
truth = implies(implies(implies(sF2,sF9),sF4),implies(sF5,not(sF9))),
inference(cp,[status(thm)],[t7588,t25234]) ).
cnf(t237,plain,
truth = implies(x,implies(sF7,y)),
inference(cp,[status(thm)],[t233,t20]) ).
cnf(t46335,plain,
truth = implies(x,sF8),
inference(step,[status(thm)],[t237,t24]) ).
cnf(t266,plain,
implies(x,sF8) = truth,
inference(orient,[status(thm)],[t46335]) ).
cnf(t271,plain,
truth = implies(truth,implies(implies(sF8,X1),implies(x,X1))),
inference(cp,[status(thm)],[t153,t266]) ).
cnf(t46405,plain,
truth = implies(implies(sF8,X1),implies(x,X1)),
inference(step,[status(thm)],[t271,t17]) ).
cnf(t700,plain,
implies(implies(sF8,X1),implies(x,X1)) = truth,
inference(orient,[status(thm)],[t46405]) ).
cnf(t701,plain,
truth = implies(implies(sF8,z),sF0),
inference(cp,[status(thm)],[t700,t18]) ).
cnf(t46406,plain,
truth = implies(sF9,sF0),
inference(step,[status(thm)],[t701,t25]) ).
cnf(t714,plain,
implies(sF9,sF0) = truth,
inference(orient,[status(thm)],[t46406]) ).
cnf(t719,plain,
truth = implies(implies(X1,sF9),implies(truth,implies(X1,sF0))),
inference(cp,[status(thm)],[t153,t714]) ).
cnf(t46476,plain,
truth = implies(implies(X1,sF9),implies(X1,sF0)),
inference(step,[status(thm)],[t719,t17]) ).
cnf(t1532,plain,
implies(implies(X1,sF9),implies(X1,sF0)) = truth,
inference(orient,[status(thm)],[t46476]) ).
cnf(t11345,plain,
truth = implies(implies(sF2,sF9),sF4),
inference(cp,[status(thm)],[t1532,t11303]) ).
cnf(t11691,plain,
implies(implies(sF2,sF9),sF4) = truth,
inference(orient,[status(thm)],[t11345]) ).
cnf(t47458,plain,
truth = implies(truth,implies(sF5,not(sF9))),
inference(step,[status(thm)],[t25253,t11691]) ).
cnf(t47459,plain,
truth = implies(sF5,not(sF9)),
inference(step,[status(thm)],[t47458,t17]) ).
cnf(t47460,plain,
truth = implies(sF9,sF6),
inference(step,[status(thm)],[t47459,t23355]) ).
cnf(t25278,plain,
implies(sF9,sF6) = truth,
inference(orient,[status(thm)],[t47460]) ).
cnf(t48049,plain,
implies(truth,sF6) = implies(truth,sF9),
inference(step,[status(thm)],[t45978,t25278]) ).
cnf(t48050,plain,
sF6 = implies(truth,sF9),
inference(step,[status(thm)],[t48049,t17]) ).
cnf(t48051,plain,
sF6 = sF9,
inference(step,[status(thm)],[t48050,t17]) ).
cnf(t46002,plain,
sF9 = sF6,
inference(orient,[status(thm)],[t48051]) ).
cnf(t48052,plain,
implies(sF8,z) = sF6,
inference(step,[status(thm)],[t25,t46002]) ).
cnf(t46003,plain,
implies(sF8,z) = sF6,
inference(orient,[status(thm)],[t48052]) ).
cnf(f8,negated_conjecture,
implies(big_V(x,y),z) != big_hat(implies(x,z),implies(y,z)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_wajsberg_theorem) ).
fof(f8_nnf,plain,
implies(big_V(x,y),z) != big_hat(implies(x,z),implies(y,z)),
inference(nnf_transformation,[status(thm)],[f8]) ).
fof(f8_sk,plain,
implies(big_V(x,y),z) != big_hat(implies(x,z),implies(y,z)),
inference(skolemisation,[status(esa)],[f8_nnf]) ).
cnf(c8,plain,
implies(big_V(x,y),z) != big_hat(implies(x,z),implies(y,z)),
inference(cnf_transformation,[status(esa)],[f8_sk]) ).
cnf(u1,negated_conjecture,
implies(big_V(x,y),z) != big_hat(implies(x,z),implies(y,z)),
inference(equality_encoding,[status(esa)],[c8]) ).
cnf(f4,axiom,
big_V(X,Y) = implies(implies(X,Y),Y),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',big_V_definition) ).
fof(f4_nnf,plain,
! [X,Y] : big_V(X,Y) = implies(implies(X,Y),Y),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [X,Y] : big_V(X,Y) = implies(implies(X,Y),Y),
inference(skolemisation,[status(esa)],[f4_nnf]) ).
cnf(c4,plain,
big_V(X0,X1) = implies(implies(X0,X1),X1),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(d0,axiom,
big_V(X0,X1) = implies(implies(X0,X1),X1),
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(f5,axiom,
big_hat(X,Y) = not(big_V(not(X),not(Y))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',big_hat_definition) ).
fof(f5_nnf,plain,
! [X,Y] : big_hat(X,Y) = not(big_V(not(X),not(Y))),
inference(nnf_transformation,[status(thm)],[f5]) ).
fof(f5_sk,plain,
! [X,Y] : big_hat(X,Y) = not(big_V(not(X),not(Y))),
inference(skolemisation,[status(esa)],[f5_nnf]) ).
cnf(c5,plain,
big_hat(X0,X1) = not(big_V(not(X0),not(X1))),
inference(cnf_transformation,[status(esa)],[f5_sk]) ).
cnf(u0,axiom,
big_hat(X0,X1) = not(big_V(not(X0),not(X1))),
inference(equality_encoding,[status(esa)],[c5]) ).
cnf(d1,axiom,
big_hat(X0,X1) = not(implies(implies(not(X0),not(X1)),not(X1))),
inference(definition_unfolding,[status(thm)],[u0,d0]) ).
cnf(goal_0,negated_conjecture,
not(implies(implies(not(implies(x,z)),not(implies(y,z))),not(implies(y,z)))) != implies(implies(implies(x,y),y),z),
inference(definition_unfolding,[status(thm)],[u1,d0,d1]) ).
cnf(g0_0,plain,
not(implies(implies(implies(y,z),implies(x,z)),not(implies(y,z)))) != implies(implies(implies(x,y),y),z),
inference(rw,[status(thm)],[goal_0,t21169]) ).
cnf(g0_1,plain,
not(implies(implies(sF2,implies(x,z)),not(implies(y,z)))) != implies(implies(implies(x,y),y),z),
inference(rw,[status(thm)],[g0_0,t19]) ).
cnf(g0_2,plain,
not(implies(implies(sF2,sF0),not(implies(y,z)))) != implies(implies(implies(x,y),y),z),
inference(rw,[status(thm)],[g0_1,t18]) ).
cnf(g0_3,plain,
not(implies(sF4,not(implies(y,z)))) != implies(implies(implies(x,y),y),z),
inference(rw,[status(thm)],[g0_2,t11303]) ).
cnf(g0_4,plain,
not(implies(sF4,not(sF2))) != implies(implies(implies(x,y),y),z),
inference(rw,[status(thm)],[g0_3,t19]) ).
cnf(g0_5,plain,
not(implies(sF4,sF3)) != implies(implies(implies(x,y),y),z),
inference(rw,[status(thm)],[g0_4,t22]) ).
cnf(g0_6,plain,
not(sF5) != implies(implies(implies(x,y),y),z),
inference(rw,[status(thm)],[g0_5,t343]) ).
cnf(g0_7,plain,
sF6 != implies(implies(implies(x,y),y),z),
inference(rw,[status(thm)],[g0_6,t381]) ).
cnf(g0_8,plain,
sF6 != implies(implies(sF7,y),z),
inference(rw,[status(thm)],[g0_7,t20]) ).
cnf(g0_9,plain,
sF6 != implies(sF8,z),
inference(rw,[status(thm)],[g0_8,t24]) ).
cnf(g0_10,plain,
sF6 != sF6,
inference(rw,[status(thm)],[g0_9,t46003]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_10]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : LCL147-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.02 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.34 % Computer : n011.cluster.edu
% 0.08/0.34 % Model : x86_64 x86_64
% 0.08/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.34 % Memory : 8046.5625MB
% 0.08/0.34 % OS : Linux 6.8.0-71-generic
% 0.04/15.42 % CPULimit : 300
% 0.04/15.42 % WCLimit : 300
% 0.04/15.42 % DateTime : Wed Sep 23 22:04:57 UTC 2026
% 0.04/15.42 % CPUTime :
% 0.04/15.42 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 96.50/27.68 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 96.50/27.68 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------