%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : CSR045+2 : TPTP v9.3.1. Released v3.4.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n015.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:05:27 PM UTC 2026
% Result : Theorem 65.56s 8.95s
% Output : Proof 65.56s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 24
% Syntax : Number of formulae : 120 ( 64 unt; 0 def)
% Number of atoms : 192 ( 29 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 167 ( 95 ~; 54 |; 10 &)
% ( 0 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 19 ( 17 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 10 con; 0-4 aty)
% Number of variables : 127 ( 2 sgn 81 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1112,axiom,
! [ARG1,OLD,NEW] :
( ( genls(OLD,NEW)
& genls(ARG1,OLD) )
=> genls(ARG1,NEW) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_1113) ).
fof(f1112_nnf,plain,
! [ARG1,OLD,NEW] :
( genls(ARG1,NEW)
| ~ genls(OLD,NEW)
| ~ genls(ARG1,OLD) ),
inference(nnf_transformation,[status(thm)],[f1112]) ).
fof(f1112_sk,plain,
! [ARG1,OLD,NEW] :
( genls(ARG1,NEW)
| ~ genls(OLD,NEW)
| ~ genls(ARG1,OLD) ),
inference(skolemisation,[status(esa)],[f1112_nnf]) ).
cnf(c1112,plain,
( genls(X0,X2)
| ~ genls(X1,X2)
| ~ genls(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1112_sk]) ).
cnf(hi1103,axiom,
ifeq(genls(X0,X1),true,ifeq(genls(X1,X2),true,genls(X0,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c1112]) ).
fof(f318,axiom,
genls(c_intangibleindividual,c_partiallyintangibleindividual),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_319) ).
fof(f318_nnf,plain,
genls(c_intangibleindividual,c_partiallyintangibleindividual),
inference(nnf_transformation,[status(thm)],[f318]) ).
cnf(c318,plain,
genls(c_intangibleindividual,c_partiallyintangibleindividual),
inference(cnf_transformation,[status(esa)],[f318_nnf]) ).
cnf(hi314,axiom,
genls(c_intangibleindividual,c_partiallyintangibleindividual) = true,
inference(equality_encoding,[status(esa)],[c318]) ).
fof(f31,axiom,
genls(c_partiallyintangibleindividual,c_individual),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_32) ).
fof(f31_nnf,plain,
genls(c_partiallyintangibleindividual,c_individual),
inference(nnf_transformation,[status(thm)],[f31]) ).
cnf(c31,plain,
genls(c_partiallyintangibleindividual,c_individual),
inference(cnf_transformation,[status(esa)],[f31_nnf]) ).
cnf(hi30,axiom,
genls(c_partiallyintangibleindividual,c_individual) = true,
inference(equality_encoding,[status(esa)],[c31]) ).
cnf(h500,plain,
genls(c_intangibleindividual,c_individual) = true,
inference(hyper_resolution,[status(thm)],[hi1103,hi314,hi30]) ).
fof(f1119,axiom,
! [X,Y] :
( disjointwith(X,Y)
=> disjointwith(Y,X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_1120) ).
fof(f1119_nnf,plain,
! [X,Y] :
( disjointwith(Y,X)
| ~ disjointwith(X,Y) ),
inference(nnf_transformation,[status(thm)],[f1119]) ).
fof(f1119_sk,plain,
! [X,Y] :
( disjointwith(Y,X)
| ~ disjointwith(X,Y) ),
inference(skolemisation,[status(esa)],[f1119_nnf]) ).
cnf(c1119,plain,
( disjointwith(X1,X0)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1119_sk]) ).
cnf(hi1110,axiom,
ifeq(disjointwith(X0,X1),true,disjointwith(X1,X0),true) = true,
inference(equality_encoding,[status(esa)],[c1119]) ).
fof(f289,axiom,
disjointwith(c_collection,c_individual),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_290) ).
fof(f289_nnf,plain,
disjointwith(c_collection,c_individual),
inference(nnf_transformation,[status(thm)],[f289]) ).
cnf(c289,plain,
disjointwith(c_collection,c_individual),
inference(cnf_transformation,[status(esa)],[f289_nnf]) ).
cnf(hi285,axiom,
disjointwith(c_collection,c_individual) = true,
inference(equality_encoding,[status(esa)],[c289]) ).
cnf(h460,plain,
disjointwith(c_individual,c_collection) = true,
inference(hyper_resolution,[status(thm)],[hi1110,hi285]) ).
fof(f1121,axiom,
! [OLD,ARG2,NEW] :
( ( genls(NEW,OLD)
& disjointwith(OLD,ARG2) )
=> disjointwith(NEW,ARG2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_1122) ).
fof(f1121_nnf,plain,
! [OLD,ARG2,NEW] :
( disjointwith(NEW,ARG2)
| ~ genls(NEW,OLD)
| ~ disjointwith(OLD,ARG2) ),
inference(nnf_transformation,[status(thm)],[f1121]) ).
fof(f1121_sk,plain,
! [OLD,ARG2,NEW] :
( disjointwith(NEW,ARG2)
| ~ genls(NEW,OLD)
| ~ disjointwith(OLD,ARG2) ),
inference(skolemisation,[status(esa)],[f1121_nnf]) ).
cnf(c1121,plain,
( disjointwith(X2,X1)
| ~ genls(X2,X0)
| ~ disjointwith(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1121_sk]) ).
cnf(hi1112,axiom,
ifeq(disjointwith(X0,X1),true,ifeq(genls(X2,X0),true,disjointwith(X2,X1),true),true) = true,
inference(equality_encoding,[status(esa)],[c1121]) ).
cnf(h1742,plain,
disjointwith(c_intangibleindividual,c_collection) = true,
inference(hyper_resolution,[status(thm)],[hi1112,h460,h500]) ).
fof(f1107,axiom,
! [INS,ARG2] :
( genls(INS,ARG2)
=> collection(INS) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_1108) ).
fof(f1107_nnf,plain,
! [INS,ARG2] :
( collection(INS)
| ~ genls(INS,ARG2) ),
inference(nnf_transformation,[status(thm)],[f1107]) ).
fof(f1107_sk,plain,
! [INS,ARG2] :
( collection(INS)
| ~ genls(INS,ARG2) ),
inference(skolemisation,[status(esa)],[f1107_nnf]) ).
cnf(c1107,plain,
( collection(X0)
| ~ genls(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1107_sk]) ).
cnf(hi1098,axiom,
ifeq(genls(X0,X1),true,collection(X0),true) = true,
inference(equality_encoding,[status(esa)],[c1107]) ).
fof(f1131,conjecture,
~ genls(c_wamt_evalinitial_p14,c_tptpcol_15_80088),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',query95) ).
fof(f1131_neg,negated_conjecture,
~ ~ genls(c_wamt_evalinitial_p14,c_tptpcol_15_80088),
inference(negated_conjecture,[status(cth)],[f1131]) ).
fof(f1131_nnf,plain,
genls(c_wamt_evalinitial_p14,c_tptpcol_15_80088),
inference(nnf_transformation,[status(thm)],[f1131_neg]) ).
cnf(c1131,plain,
genls(c_wamt_evalinitial_p14,c_tptpcol_15_80088),
inference(cnf_transformation,[status(esa)],[f1131_nnf]) ).
cnf(hi1122,negated_conjecture,
genls(c_wamt_evalinitial_p14,c_tptpcol_15_80088) = true,
inference(equality_encoding,[status(esa)],[c1131]) ).
cnf(h893,plain,
collection(c_wamt_evalinitial_p14) = true,
inference(hyper_resolution,[status(thm)],[hi1098,hi1122]) ).
fof(f813,axiom,
! [X] :
( collection(X)
=> isa(X,c_collection) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_814) ).
fof(f813_nnf,plain,
! [X] :
( isa(X,c_collection)
| ~ collection(X) ),
inference(nnf_transformation,[status(thm)],[f813]) ).
fof(f813_sk,plain,
! [X] :
( isa(X,c_collection)
| ~ collection(X) ),
inference(skolemisation,[status(esa)],[f813_nnf]) ).
cnf(c813,plain,
( isa(X0,c_collection)
| ~ collection(X0) ),
inference(cnf_transformation,[status(esa)],[f813_sk]) ).
cnf(hi805,axiom,
ifeq(collection(X0),true,isa(X0,c_collection),true) = true,
inference(equality_encoding,[status(esa)],[c813]) ).
cnf(h2415,plain,
isa(c_wamt_evalinitial_p14,c_collection) = true,
inference(hyper_resolution,[status(thm)],[hi805,h893]) ).
fof(f154,axiom,
genls(c_microtheory,c_aspatialinformationstore),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_155) ).
fof(f154_nnf,plain,
genls(c_microtheory,c_aspatialinformationstore),
inference(nnf_transformation,[status(thm)],[f154]) ).
cnf(c154,plain,
genls(c_microtheory,c_aspatialinformationstore),
inference(cnf_transformation,[status(esa)],[f154_nnf]) ).
cnf(hi152,axiom,
genls(c_microtheory,c_aspatialinformationstore) = true,
inference(equality_encoding,[status(esa)],[c154]) ).
fof(f380,axiom,
genls(c_aspatialinformationstore,c_intangibleindividual),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_381) ).
fof(f380_nnf,plain,
genls(c_aspatialinformationstore,c_intangibleindividual),
inference(nnf_transformation,[status(thm)],[f380]) ).
cnf(c380,plain,
genls(c_aspatialinformationstore,c_intangibleindividual),
inference(cnf_transformation,[status(esa)],[f380_nnf]) ).
cnf(hi375,axiom,
genls(c_aspatialinformationstore,c_intangibleindividual) = true,
inference(equality_encoding,[status(esa)],[c380]) ).
cnf(h619,plain,
genls(c_microtheory,c_intangibleindividual) = true,
inference(hyper_resolution,[status(thm)],[hi1103,hi152,hi375]) ).
fof(f170,axiom,
! [OBJ] :
( applicationcontext(OBJ)
=> microtheory(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_171) ).
fof(f170_nnf,plain,
! [OBJ] :
( microtheory(OBJ)
| ~ applicationcontext(OBJ) ),
inference(nnf_transformation,[status(thm)],[f170]) ).
fof(f170_sk,plain,
! [OBJ] :
( microtheory(OBJ)
| ~ applicationcontext(OBJ) ),
inference(skolemisation,[status(esa)],[f170_nnf]) ).
cnf(c170,plain,
( microtheory(X0)
| ~ applicationcontext(X0) ),
inference(cnf_transformation,[status(esa)],[f170_sk]) ).
cnf(hi167,axiom,
ifeq(applicationcontext(X0),true,microtheory(X0),true) = true,
inference(equality_encoding,[status(esa)],[c170]) ).
fof(f82,axiom,
applicationcontext(c_wamt_evalinitial_p14),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_83) ).
fof(f82_nnf,plain,
applicationcontext(c_wamt_evalinitial_p14),
inference(nnf_transformation,[status(thm)],[f82]) ).
cnf(c82,plain,
applicationcontext(c_wamt_evalinitial_p14),
inference(cnf_transformation,[status(esa)],[f82_nnf]) ).
cnf(hi81,axiom,
applicationcontext(c_wamt_evalinitial_p14) = true,
inference(equality_encoding,[status(esa)],[c82]) ).
cnf(h11,plain,
microtheory(c_wamt_evalinitial_p14) = true,
inference(hyper_resolution,[status(thm)],[hi167,hi81]) ).
fof(f1078,axiom,
! [X] :
( microtheory(X)
=> isa(X,c_microtheory) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_1079) ).
fof(f1078_nnf,plain,
! [X] :
( isa(X,c_microtheory)
| ~ microtheory(X) ),
inference(nnf_transformation,[status(thm)],[f1078]) ).
fof(f1078_sk,plain,
! [X] :
( isa(X,c_microtheory)
| ~ microtheory(X) ),
inference(skolemisation,[status(esa)],[f1078_nnf]) ).
cnf(c1078,plain,
( isa(X0,c_microtheory)
| ~ microtheory(X0) ),
inference(cnf_transformation,[status(esa)],[f1078_sk]) ).
cnf(hi1069,axiom,
ifeq(microtheory(X0),true,isa(X0,c_microtheory),true) = true,
inference(equality_encoding,[status(esa)],[c1078]) ).
cnf(h240,plain,
isa(c_wamt_evalinitial_p14,c_microtheory) = true,
inference(hyper_resolution,[status(thm)],[hi1069,h11]) ).
fof(f1093,axiom,
! [ARG1,OLD,NEW] :
( ( genls(OLD,NEW)
& isa(ARG1,OLD) )
=> isa(ARG1,NEW) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_1094) ).
fof(f1093_nnf,plain,
! [ARG1,OLD,NEW] :
( isa(ARG1,NEW)
| ~ genls(OLD,NEW)
| ~ isa(ARG1,OLD) ),
inference(nnf_transformation,[status(thm)],[f1093]) ).
fof(f1093_sk,plain,
! [ARG1,OLD,NEW] :
( isa(ARG1,NEW)
| ~ genls(OLD,NEW)
| ~ isa(ARG1,OLD) ),
inference(skolemisation,[status(esa)],[f1093_nnf]) ).
cnf(c1093,plain,
( isa(X0,X2)
| ~ genls(X1,X2)
| ~ isa(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f1093_sk]) ).
cnf(hi1084,axiom,
ifeq(isa(X0,X1),true,ifeq(genls(X1,X2),true,isa(X0,X2),true),true) = true,
inference(equality_encoding,[status(esa)],[c1093]) ).
cnf(h2026,plain,
isa(c_wamt_evalinitial_p14,c_intangibleindividual) = true,
inference(hyper_resolution,[status(thm)],[hi1084,h240,h619]) ).
fof(f362,axiom,
! [OBJ,COL1,COL2] :
~ ( disjointwith(COL1,COL2)
& isa(OBJ,COL2)
& isa(OBJ,COL1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_363) ).
fof(f362_nnf,plain,
! [OBJ,COL1,COL2] :
( ~ disjointwith(COL1,COL2)
| ~ isa(OBJ,COL2)
| ~ isa(OBJ,COL1) ),
inference(nnf_transformation,[status(thm)],[f362]) ).
fof(f362_sk,plain,
! [OBJ,COL1,COL2] :
( ~ disjointwith(COL1,COL2)
| ~ isa(OBJ,COL2)
| ~ isa(OBJ,COL1) ),
inference(skolemisation,[status(esa)],[f362_nnf]) ).
cnf(c362,plain,
( ~ disjointwith(X1,X2)
| ~ isa(X0,X2)
| ~ isa(X0,X1) ),
inference(cnf_transformation,[status(esa)],[f362_sk]) ).
cnf(hi1127,axiom,
ifeq(isa(X0,X1),true,ifeq(isa(X0,X2),true,ifeq(disjointwith(X1,X2),true,false,true),true),true) = true,
inference(equality_encoding,[status(esa)],[c362]) ).
cnf(t0,plain,
true = false,
inference(hyper_resolution,[status(thm)],[hi1127,h2026,h2415,h1742]) ).
cnf(t1010,plain,
false = true,
inference(orient,[status(thm)],[t0]) ).
fof(f2,axiom,
! [OBJ] :
~ ( partiallytangible(OBJ)
& intangible(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_3) ).
fof(f2_nnf,plain,
! [OBJ] :
( ~ partiallytangible(OBJ)
| ~ intangible(OBJ) ),
inference(nnf_transformation,[status(thm)],[f2]) ).
fof(f2_sk,plain,
! [OBJ] :
( ~ partiallytangible(OBJ)
| ~ intangible(OBJ) ),
inference(skolemisation,[status(esa)],[f2_nnf]) ).
cnf(c2,plain,
( ~ partiallytangible(X0)
| ~ intangible(X0) ),
inference(cnf_transformation,[status(esa)],[f2_sk]) ).
fof(f152,axiom,
! [OBJ] :
~ ( tptpcol_1_65536(OBJ)
& tptpcol_1_1(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_153) ).
fof(f152_nnf,plain,
! [OBJ] :
( ~ tptpcol_1_65536(OBJ)
| ~ tptpcol_1_1(OBJ) ),
inference(nnf_transformation,[status(thm)],[f152]) ).
fof(f152_sk,plain,
! [OBJ] :
( ~ tptpcol_1_65536(OBJ)
| ~ tptpcol_1_1(OBJ) ),
inference(skolemisation,[status(esa)],[f152_nnf]) ).
cnf(c152,plain,
( ~ tptpcol_1_65536(X0)
| ~ tptpcol_1_1(X0) ),
inference(cnf_transformation,[status(esa)],[f152_sk]) ).
fof(f166,axiom,
! [OBJ] :
~ ( setorcollection(OBJ)
& individual(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_167) ).
fof(f166_nnf,plain,
! [OBJ] :
( ~ setorcollection(OBJ)
| ~ individual(OBJ) ),
inference(nnf_transformation,[status(thm)],[f166]) ).
fof(f166_sk,plain,
! [OBJ] :
( ~ setorcollection(OBJ)
| ~ individual(OBJ) ),
inference(skolemisation,[status(esa)],[f166_nnf]) ).
cnf(c166,plain,
( ~ setorcollection(X0)
| ~ individual(X0) ),
inference(cnf_transformation,[status(esa)],[f166_sk]) ).
fof(f288,axiom,
! [OBJ] :
~ ( individual(OBJ)
& collection(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_289) ).
fof(f288_nnf,plain,
! [OBJ] :
( ~ individual(OBJ)
| ~ collection(OBJ) ),
inference(nnf_transformation,[status(thm)],[f288]) ).
fof(f288_sk,plain,
! [OBJ] :
( ~ individual(OBJ)
| ~ collection(OBJ) ),
inference(skolemisation,[status(esa)],[f288_nnf]) ).
cnf(c288,plain,
( ~ individual(X0)
| ~ collection(X0) ),
inference(cnf_transformation,[status(esa)],[f288_sk]) ).
fof(f487,axiom,
! [OBJ] :
~ ( tptpcol_3_114688(OBJ)
& tptpcol_3_98305(OBJ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_488) ).
fof(f487_nnf,plain,
! [OBJ] :
( ~ tptpcol_3_114688(OBJ)
| ~ tptpcol_3_98305(OBJ) ),
inference(nnf_transformation,[status(thm)],[f487]) ).
fof(f487_sk,plain,
! [OBJ] :
( ~ tptpcol_3_114688(OBJ)
| ~ tptpcol_3_98305(OBJ) ),
inference(skolemisation,[status(esa)],[f487_nnf]) ).
cnf(c487,plain,
( ~ tptpcol_3_114688(X0)
| ~ tptpcol_3_98305(X0) ),
inference(cnf_transformation,[status(esa)],[f487_sk]) ).
fof(f520,axiom,
! [X] : ~ affiliatedwith(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_521) ).
fof(f520_nnf,plain,
! [X] : ~ affiliatedwith(X,X),
inference(nnf_transformation,[status(thm)],[f520]) ).
fof(f520_sk,plain,
! [X] : ~ affiliatedwith(X,X),
inference(skolemisation,[status(esa)],[f520_nnf]) ).
cnf(c520,plain,
~ affiliatedwith(X0,X0),
inference(cnf_transformation,[status(esa)],[f520_sk]) ).
fof(f697,axiom,
! [X] : ~ objectfoundinlocation(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_698) ).
fof(f697_nnf,plain,
! [X] : ~ objectfoundinlocation(X,X),
inference(nnf_transformation,[status(thm)],[f697]) ).
fof(f697_sk,plain,
! [X] : ~ objectfoundinlocation(X,X),
inference(skolemisation,[status(esa)],[f697_nnf]) ).
cnf(c697,plain,
~ objectfoundinlocation(X0,X0),
inference(cnf_transformation,[status(esa)],[f697_sk]) ).
fof(f900,axiom,
! [X] : ~ borderson(X,X),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax1_901) ).
fof(f900_nnf,plain,
! [X] : ~ borderson(X,X),
inference(nnf_transformation,[status(thm)],[f900]) ).
fof(f900_sk,plain,
! [X] : ~ borderson(X,X),
inference(skolemisation,[status(esa)],[f900_nnf]) ).
cnf(c900,plain,
~ borderson(X0,X0),
inference(cnf_transformation,[status(esa)],[f900_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c2,c152,c166,c288,c362,c487,c520,c697,c900]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t1010]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : CSR045+2 : TPTP v9.3.1. Released v3.4.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.09/0.37 % Computer : n015.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Fri Sep 25 08:33:12 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 65.56/8.95 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 65.56/8.95 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------