%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : KRS108+1 : TPTP v9.3.1. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% Computer : n008.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:53:04 PM UTC 2026
% Result : Unsatisfiable 6.76s 1.36s
% Output : Proof 6.76s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 17
% Syntax : Number of formulae : 100 ( 33 unt; 0 def)
% Number of atoms : 270 ( 38 equ)
% Maximal formula atoms : 12 ( 2 avg)
% Number of connectives : 290 ( 120 ~; 98 |; 56 &)
% ( 13 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 29 ( 27 usr; 1 prp; 0-2 aty)
% Number of functors : 16 ( 16 usr; 3 con; 0-4 aty)
% Number of variables : 150 ( 9 sgn 80 !; 22 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f41,axiom,
! [X] :
( cUnsatisfiable(X)
<=> ( cp2(X)
& ? [Y] :
( ca_Ax14(Y)
& rinvR(X,Y) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_2) ).
fof(f41_nnf,plain,
! [X] :
( ( ~ cp2(X)
| ! [Y] :
( ~ ca_Ax14(Y)
| ~ rinvR(X,Y) )
| cUnsatisfiable(X) )
& ( ( cp2(X)
& ? [Y] :
( ca_Ax14(Y)
& rinvR(X,Y) ) )
| ~ cUnsatisfiable(X) ) ),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
! [X,Y] :
( ( ~ cp2(X)
| ~ ca_Ax14(Y)
| ~ rinvR(X,Y)
| cUnsatisfiable(X) )
& ( ( cp2(X)
& ca_Ax14(sk0(X))
& rinvR(X,sk0(X)) )
| ~ cUnsatisfiable(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f41_nnf]) ).
cnf(c45,plain,
( cp2(X0)
| ~ cUnsatisfiable(X0) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(hi44,axiom,
ifeq(cUnsatisfiable(X0),true,cp2(X0),true) = true,
inference(equality_encoding,[status(esa)],[c45]) ).
fof(f65,axiom,
cUnsatisfiable(i2003_11_14_17_21_04740),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_26) ).
fof(f65_nnf,plain,
cUnsatisfiable(i2003_11_14_17_21_04740),
inference(nnf_transformation,[status(thm)],[f65]) ).
cnf(c99,plain,
cUnsatisfiable(i2003_11_14_17_21_04740),
inference(cnf_transformation,[status(esa)],[f65_nnf]) ).
cnf(hi91,axiom,
cUnsatisfiable(i2003_11_14_17_21_04740) = true,
inference(equality_encoding,[status(esa)],[c99]) ).
cnf(h0,plain,
cp2(i2003_11_14_17_21_04740) = true,
inference(hyper_resolution,[status(thm)],[hi44,hi91]) ).
fof(f43,axiom,
! [X] :
( cp2(X)
<=> ? [Y0] : ra_Px5(X,Y0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_4) ).
fof(f43_nnf,plain,
! [X] :
( ( ! [Y0] : ~ ra_Px5(X,Y0)
| cp2(X) )
& ( ? [Y0] : ra_Px5(X,Y0)
| ~ cp2(X) ) ),
inference(nnf_transformation,[status(thm)],[f43]) ).
fof(f43_sk,plain,
! [X,Y0] :
( ( ~ ra_Px5(X,Y0)
| cp2(X) )
& ( ra_Px5(X,sk1(X))
| ~ cp2(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk1])],[f43_nnf]) ).
cnf(c48,plain,
( ra_Px5(X0,sk1(X0))
| ~ cp2(X0) ),
inference(cnf_transformation,[status(esa)],[f43_sk]) ).
cnf(hi47,axiom,
ifeq(cp2(X0),true,ra_Px5(X0,sk1(X0)),true) = true,
inference(equality_encoding,[status(esa)],[c48]) ).
cnf(h4,plain,
ra_Px5(i2003_11_14_17_21_04740,sk1(i2003_11_14_17_21_04740)) = true,
inference(hyper_resolution,[status(thm)],[hi47,h0]) ).
cnf(c44,plain,
( ca_Ax14(sk0(X0))
| ~ cUnsatisfiable(X0) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(hi43,axiom,
ifeq(cUnsatisfiable(X0),true,ca_Ax14(sk0(X0)),true) = true,
inference(equality_encoding,[status(esa)],[c44]) ).
cnf(h1,plain,
ca_Ax14(sk0(i2003_11_14_17_21_04740)) = true,
inference(hyper_resolution,[status(thm)],[hi43,hi91]) ).
fof(f54,axiom,
! [X] :
( ca_Ax14(X)
<=> ( ! [Y0,Y1] :
( ( rr(X,Y1)
& rr(X,Y0) )
=> Y0 = Y1 )
& ? [Y] :
( cp1(Y)
& rr(X,Y) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_15) ).
fof(f54_nnf,plain,
! [X] :
( ( ? [Y0,Y1] :
( Y0 != Y1
& rr(X,Y1)
& rr(X,Y0) )
| ! [Y] :
( ~ cp1(Y)
| ~ rr(X,Y) )
| ca_Ax14(X) )
& ( ( ! [Y0,Y1] :
( Y0 = Y1
| ~ rr(X,Y1)
| ~ rr(X,Y0) )
& ? [Y] :
( cp1(Y)
& rr(X,Y) ) )
| ~ ca_Ax14(X) ) ),
inference(nnf_transformation,[status(thm)],[f54]) ).
fof(f54_sk,plain,
! [X,Y0,Y1,Y] :
( ( ( sk10(X) != sk11(X)
& rr(X,sk11(X))
& rr(X,sk10(X)) )
| ~ cp1(Y)
| ~ rr(X,Y)
| ca_Ax14(X) )
& ( ( ( Y0 = Y1
| ~ rr(X,Y1)
| ~ rr(X,Y0) )
& cp1(sk9(X))
& rr(X,sk9(X)) )
| ~ ca_Ax14(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk9,sk10,sk11])],[f54_nnf]) ).
cnf(c68,plain,
( cp1(sk9(X0))
| ~ ca_Ax14(X0) ),
inference(cnf_transformation,[status(esa)],[f54_sk]) ).
cnf(hi63,axiom,
ifeq(ca_Ax14(X0),true,cp1(sk9(X0)),true) = true,
inference(equality_encoding,[status(esa)],[c68]) ).
cnf(h25,plain,
cp1(sk9(sk0(i2003_11_14_17_21_04740))) = true,
inference(hyper_resolution,[status(thm)],[hi63,h1]) ).
fof(f42,axiom,
! [X] :
( cp1(X)
=> ca_Cx1(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_3) ).
fof(f42_nnf,plain,
! [X] :
( ca_Cx1(X)
| ~ cp1(X) ),
inference(nnf_transformation,[status(thm)],[f42]) ).
fof(f42_sk,plain,
! [X] :
( ca_Cx1(X)
| ~ cp1(X) ),
inference(skolemisation,[status(esa)],[f42_nnf]) ).
cnf(c47,plain,
( ca_Cx1(X0)
| ~ cp1(X0) ),
inference(cnf_transformation,[status(esa)],[f42_sk]) ).
cnf(hi46,axiom,
ifeq(cp1(X0),true,ca_Cx1(X0),true) = true,
inference(equality_encoding,[status(esa)],[c47]) ).
cnf(h84,plain,
ca_Cx1(sk9(sk0(i2003_11_14_17_21_04740))) = true,
inference(hyper_resolution,[status(thm)],[hi46,h25]) ).
fof(f55,axiom,
! [X] :
( ca_Cx1(X)
<=> ( cp4xcomp(X)
& cp3xcomp(X)
& cp5xcomp(X)
& cp2xcomp(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_16) ).
fof(f55_nnf,plain,
! [X] :
( ( ~ cp4xcomp(X)
| ~ cp3xcomp(X)
| ~ cp5xcomp(X)
| ~ cp2xcomp(X)
| ca_Cx1(X) )
& ( ( cp4xcomp(X)
& cp3xcomp(X)
& cp5xcomp(X)
& cp2xcomp(X) )
| ~ ca_Cx1(X) ) ),
inference(nnf_transformation,[status(thm)],[f55]) ).
fof(f55_sk,plain,
! [X] :
( ( ~ cp4xcomp(X)
| ~ cp3xcomp(X)
| ~ cp5xcomp(X)
| ~ cp2xcomp(X)
| ca_Cx1(X) )
& ( ( cp4xcomp(X)
& cp3xcomp(X)
& cp5xcomp(X)
& cp2xcomp(X) )
| ~ ca_Cx1(X) ) ),
inference(skolemisation,[status(esa)],[f55_nnf]) ).
cnf(c73,plain,
( cp2xcomp(X0)
| ~ ca_Cx1(X0) ),
inference(cnf_transformation,[status(esa)],[f55_sk]) ).
cnf(hi68,axiom,
ifeq(ca_Cx1(X0),true,cp2xcomp(X0),true) = true,
inference(equality_encoding,[status(esa)],[c73]) ).
cnf(h95,plain,
cp2xcomp(sk9(sk0(i2003_11_14_17_21_04740))) = true,
inference(hyper_resolution,[status(thm)],[hi68,h84]) ).
cnf(c67,plain,
( rr(X0,sk9(X0))
| ~ ca_Ax14(X0) ),
inference(cnf_transformation,[status(esa)],[f54_sk]) ).
cnf(hi62,axiom,
ifeq(ca_Ax14(X0),true,rr(X0,sk9(X0)),true) = true,
inference(equality_encoding,[status(esa)],[c67]) ).
cnf(h26,plain,
rr(sk0(i2003_11_14_17_21_04740),sk9(sk0(i2003_11_14_17_21_04740))) = true,
inference(hyper_resolution,[status(thm)],[hi62,h1]) ).
cnf(c43,plain,
( rinvR(X0,sk0(X0))
| ~ cUnsatisfiable(X0) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
cnf(hi42,axiom,
ifeq(cUnsatisfiable(X0),true,rinvR(X0,sk0(X0)),true) = true,
inference(equality_encoding,[status(esa)],[c43]) ).
cnf(h2,plain,
rinvR(i2003_11_14_17_21_04740,sk0(i2003_11_14_17_21_04740)) = true,
inference(hyper_resolution,[status(thm)],[hi42,hi91]) ).
fof(f64,axiom,
! [X,Y] :
( rinvR(X,Y)
<=> rr(Y,X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_25) ).
fof(f64_nnf,plain,
! [X,Y] :
( ( ~ rr(Y,X)
| rinvR(X,Y) )
& ( rr(Y,X)
| ~ rinvR(X,Y) ) ),
inference(nnf_transformation,[status(thm)],[f64]) ).
fof(f64_sk,plain,
! [X,Y] :
( ( ~ rr(Y,X)
| rinvR(X,Y) )
& ( rr(Y,X)
| ~ rinvR(X,Y) ) ),
inference(skolemisation,[status(esa)],[f64_nnf]) ).
cnf(c97,plain,
( rr(X1,X0)
| ~ rinvR(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f64_sk]) ).
cnf(hi89,axiom,
ifeq(rinvR(X0,X1),true,rr(X1,X0),true) = true,
inference(equality_encoding,[status(esa)],[c97]) ).
cnf(h29,plain,
rr(sk0(i2003_11_14_17_21_04740),i2003_11_14_17_21_04740) = true,
inference(hyper_resolution,[status(thm)],[hi89,h2]) ).
cnf(c69,plain,
( X2 = X3
| ~ rr(X0,X3)
| ~ rr(X0,X2)
| ~ ca_Ax14(X0) ),
inference(cnf_transformation,[status(esa)],[f54_sk]) ).
cnf(hi64,axiom,
ifeq(ca_Ax14(X0),true,ifeq(rr(X0,X1),true,ifeq(rr(X0,X2),true,X1,X2),X2),X2) = X2,
inference(equality_encoding,[status(esa)],[c69]) ).
cnf(h133,plain,
i2003_11_14_17_21_04740 = sk9(sk0(i2003_11_14_17_21_04740)),
inference(hyper_resolution,[status(thm)],[hi64,h1,h29,h26]) ).
fof(f12,axiom,
! [A,B] :
( ( cp2xcomp(A)
& A = B )
=> cp2xcomp(B) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cp2xcomp_substitution_1) ).
fof(f12_nnf,plain,
! [A,B] :
( cp2xcomp(B)
| ~ cp2xcomp(A)
| A != B ),
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [A,B] :
( cp2xcomp(B)
| ~ cp2xcomp(A)
| A != B ),
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c12,plain,
( cp2xcomp(X1)
| ~ cp2xcomp(X0)
| X0 != X1 ),
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
cnf(hi14,axiom,
ifeq(X0,X1,ifeq(cp2xcomp(X0),true,cp2xcomp(X1),true),true) = true,
inference(equality_encoding,[status(esa)],[c12]) ).
cnf(h143,plain,
cp2xcomp(i2003_11_14_17_21_04740) = true,
inference(hyper_resolution,[status(thm)],[hi14,h133,h95]) ).
fof(f45,axiom,
! [X] :
( cp2xcomp(X)
<=> ~ ? [Y] : ra_Px5(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_6) ).
fof(f45_nnf,plain,
! [X] :
( ( ? [Y] : ra_Px5(X,Y)
| cp2xcomp(X) )
& ( ! [Y] : ~ ra_Px5(X,Y)
| ~ cp2xcomp(X) ) ),
inference(nnf_transformation,[status(thm)],[f45]) ).
fof(f45_sk,plain,
! [X,Y] :
( ( ra_Px5(X,sk2(X))
| cp2xcomp(X) )
& ( ~ ra_Px5(X,Y)
| ~ cp2xcomp(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk2])],[f45_nnf]) ).
cnf(c51,plain,
( ~ ra_Px5(X0,X1)
| ~ cp2xcomp(X0) ),
inference(cnf_transformation,[status(esa)],[f45_sk]) ).
cnf(hi94,axiom,
ifeq(cp2xcomp(X0),true,ifeq(ra_Px5(X0,X1),true,false,true),true) = true,
inference(equality_encoding,[status(esa)],[c51]) ).
cnf(t0,plain,
true = false,
inference(hyper_resolution,[status(thm)],[hi94,h143,h4]) ).
cnf(t280,plain,
false = true,
inference(orient,[status(thm)],[t0]) ).
fof(f39,axiom,
! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_0) ).
fof(f39_nnf,plain,
! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ),
inference(nnf_transformation,[status(thm)],[f39]) ).
fof(f39_sk,plain,
! [X] :
( ~ cowlNothing(X)
& cowlThing(X) ),
inference(skolemisation,[status(esa)],[f39_nnf]) ).
cnf(c40,plain,
~ cowlNothing(X0),
inference(cnf_transformation,[status(esa)],[f39_sk]) ).
fof(f40,axiom,
! [X] :
( xsd_string(X)
<=> ~ xsd_integer(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_1) ).
fof(f40_nnf,plain,
! [X] :
( ( xsd_integer(X)
| xsd_string(X) )
& ( ~ xsd_integer(X)
| ~ xsd_string(X) ) ),
inference(nnf_transformation,[status(thm)],[f40]) ).
fof(f40_sk,plain,
! [X] :
( ( xsd_integer(X)
| xsd_string(X) )
& ( ~ xsd_integer(X)
| ~ xsd_string(X) ) ),
inference(skolemisation,[status(esa)],[f40_nnf]) ).
cnf(c41,plain,
( ~ xsd_integer(X0)
| ~ xsd_string(X0) ),
inference(cnf_transformation,[status(esa)],[f40_sk]) ).
fof(f48,axiom,
! [X] :
( cp3xcomp(X)
<=> ~ ? [Y] : ra_Px6(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_9) ).
fof(f48_nnf,plain,
! [X] :
( ( ? [Y] : ra_Px6(X,Y)
| cp3xcomp(X) )
& ( ! [Y] : ~ ra_Px6(X,Y)
| ~ cp3xcomp(X) ) ),
inference(nnf_transformation,[status(thm)],[f48]) ).
fof(f48_sk,plain,
! [X,Y] :
( ( ra_Px6(X,sk4(X))
| cp3xcomp(X) )
& ( ~ ra_Px6(X,Y)
| ~ cp3xcomp(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk4])],[f48_nnf]) ).
cnf(c56,plain,
( ~ ra_Px6(X0,X1)
| ~ cp3xcomp(X0) ),
inference(cnf_transformation,[status(esa)],[f48_sk]) ).
fof(f49,axiom,
! [X] :
( cp4(X)
<=> ~ ? [Y] : ra_Px7(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_10) ).
fof(f49_nnf,plain,
! [X] :
( ( ? [Y] : ra_Px7(X,Y)
| cp4(X) )
& ( ! [Y] : ~ ra_Px7(X,Y)
| ~ cp4(X) ) ),
inference(nnf_transformation,[status(thm)],[f49]) ).
fof(f49_sk,plain,
! [X,Y] :
( ( ra_Px7(X,sk5(X))
| cp4(X) )
& ( ~ ra_Px7(X,Y)
| ~ cp4(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk5])],[f49_nnf]) ).
cnf(c58,plain,
( ~ ra_Px7(X0,X1)
| ~ cp4(X0) ),
inference(cnf_transformation,[status(esa)],[f49_sk]) ).
fof(f52,axiom,
! [X] :
( cp5(X)
<=> ~ ? [Y] : ra_Px4(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_13) ).
fof(f52_nnf,plain,
! [X] :
( ( ? [Y] : ra_Px4(X,Y)
| cp5(X) )
& ( ! [Y] : ~ ra_Px4(X,Y)
| ~ cp5(X) ) ),
inference(nnf_transformation,[status(thm)],[f52]) ).
fof(f52_sk,plain,
! [X,Y] :
( ( ra_Px4(X,sk7(X))
| cp5(X) )
& ( ~ ra_Px4(X,Y)
| ~ cp5(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk7])],[f52_nnf]) ).
cnf(c63,plain,
( ~ ra_Px4(X0,X1)
| ~ cp5(X0) ),
inference(cnf_transformation,[status(esa)],[f52_sk]) ).
fof(f57,axiom,
! [X] :
( ca_Cx1xcomp(X)
<=> ~ ? [Y] : ra_Px1(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_18) ).
fof(f57_nnf,plain,
! [X] :
( ( ? [Y] : ra_Px1(X,Y)
| ca_Cx1xcomp(X) )
& ( ! [Y] : ~ ra_Px1(X,Y)
| ~ ca_Cx1xcomp(X) ) ),
inference(nnf_transformation,[status(thm)],[f57]) ).
fof(f57_sk,plain,
! [X,Y] :
( ( ra_Px1(X,sk13(X))
| ca_Cx1xcomp(X) )
& ( ~ ra_Px1(X,Y)
| ~ ca_Cx1xcomp(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk13])],[f57_nnf]) ).
cnf(c80,plain,
( ~ ra_Px1(X0,X1)
| ~ ca_Cx1xcomp(X0) ),
inference(cnf_transformation,[status(esa)],[f57_sk]) ).
fof(f59,axiom,
! [X] :
( ca_Cx2(X)
<=> ~ ? [Y] : ra_Px2(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_20) ).
fof(f59_nnf,plain,
! [X] :
( ( ? [Y] : ra_Px2(X,Y)
| ca_Cx2(X) )
& ( ! [Y] : ~ ra_Px2(X,Y)
| ~ ca_Cx2(X) ) ),
inference(nnf_transformation,[status(thm)],[f59]) ).
fof(f59_sk,plain,
! [X,Y] :
( ( ra_Px2(X,sk14(X))
| ca_Cx2(X) )
& ( ~ ra_Px2(X,Y)
| ~ ca_Cx2(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk14])],[f59_nnf]) ).
cnf(c86,plain,
( ~ ra_Px2(X0,X1)
| ~ ca_Cx2(X0) ),
inference(cnf_transformation,[status(esa)],[f59_sk]) ).
fof(f61,axiom,
! [X] :
( ca_Cx3(X)
<=> ~ ? [Y] : ra_Px3(X,Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',axiom_22) ).
fof(f61_nnf,plain,
! [X] :
( ( ? [Y] : ra_Px3(X,Y)
| ca_Cx3(X) )
& ( ! [Y] : ~ ra_Px3(X,Y)
| ~ ca_Cx3(X) ) ),
inference(nnf_transformation,[status(thm)],[f61]) ).
fof(f61_sk,plain,
! [X,Y] :
( ( ra_Px3(X,sk16(X))
| ca_Cx3(X) )
& ( ~ ra_Px3(X,Y)
| ~ ca_Cx3(X) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk16])],[f61_nnf]) ).
cnf(c90,plain,
( ~ ra_Px3(X0,X1)
| ~ ca_Cx3(X0) ),
inference(cnf_transformation,[status(esa)],[f61_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c40,c41,c51,c56,c58,c63,c80,c86,c90]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t280]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : KRS108+1 : TPTP v9.3.1. Released v3.1.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 0.09/0.36 % Computer : n008.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Wed Sep 23 19:26:10 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox/benchmark/theBenchmark.p 300
% 6.76/1.36 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.76/1.36 % SZS output start Proof for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------