%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PRO014+2 : TPTP v9.3.1. Released v4.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n020.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 : Sun Sep 27 08:20:58 AM UTC 2026
% Result : Theorem 0.23s 5.54s
% Output : CNFRefutation 0.23s
% Verified :
% SZS Type : Refutation
% Derivation depth : 16
% Number of leaves : 4
% Syntax : Number of formulae : 63 ( 16 unt; 0 def)
% Number of atoms : 274 ( 0 equ)
% Maximal formula atoms : 36 ( 4 avg)
% Number of connectives : 339 ( 128 ~; 147 |; 59 &)
% ( 1 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 5 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of predicates : 8 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 7 con; 0-2 aty)
% Number of variables : 80 ( 0 sgn 39 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(sos,axiom,
! [X0,X1,X2,X3] :
( ( min_precedes(X1,X2,X3)
& min_precedes(X0,X1,X3) )
=> min_precedes(X0,X2,X3) ),
file('theBenchmark.p',sos) ).
fof(sos_04,axiom,
! [X15,X16,X17] :
( next_subocc(X15,X16,X17)
<=> ( ~ ? [X18] :
( min_precedes(X18,X16,X17)
& min_precedes(X15,X18,X17) )
& min_precedes(X15,X16,X17) ) ),
file('theBenchmark.p',sos_04) ).
fof(sos_32,axiom,
! [X95,X96] :
( ( ~ leaf_occ(X95,X96)
& arboreal(X95)
& subactivity_occurrence(X95,X96)
& occurrence_of(X96,tptp0) )
=> ? [X97,X98,X99] :
( leaf(X99,tptp0)
& next_subocc(X98,X99,tptp0)
& ( occurrence_of(X99,tptp1)
| occurrence_of(X99,tptp2) )
& next_subocc(X97,X98,tptp0)
& occurrence_of(X98,tptp4)
& next_subocc(X95,X97,tptp0)
& occurrence_of(X97,tptp3) ) ),
file('theBenchmark.p',sos_32) ).
fof(goals,conjecture,
! [X100,X101] :
( ( ~ leaf_occ(X100,X101)
& arboreal(X100)
& subactivity_occurrence(X100,X101)
& occurrence_of(X101,tptp0) )
=> ? [X102,X103] :
( leaf(X103,tptp0)
& min_precedes(X102,X103,tptp0)
& ( occurrence_of(X103,tptp1)
| occurrence_of(X103,tptp2) )
& next_subocc(X100,X102,tptp0)
& occurrence_of(X102,tptp3) ) ),
file('theBenchmark.p',goals) ).
fof(goals_neg,negated_conjecture,
~ ! [X100,X101] :
( ( ~ leaf_occ(X100,X101)
& arboreal(X100)
& subactivity_occurrence(X100,X101)
& occurrence_of(X101,tptp0) )
=> ? [X102,X103] :
( leaf(X103,tptp0)
& min_precedes(X102,X103,tptp0)
& ( occurrence_of(X103,tptp1)
| occurrence_of(X103,tptp2) )
& next_subocc(X100,X102,tptp0)
& occurrence_of(X102,tptp3) ) ),
inference(assume_negation,[status(cth)],[goals]) ).
cnf(c_103,plain,
( min_precedes(A,D,C)
| ~ min_precedes(B,D,C)
| ~ min_precedes(A,B,C) ),
inference(clausify,[status(thm)],[sos]) ).
cnf(c_107,plain,
( min_precedes(A,B,C)
| ~ next_subocc(A,B,C) ),
inference(clausify,[status(thm)],[sos_04]) ).
fof(nnf_33,plain,
! [X95,X96] :
( ? [X97,X98,X99] :
( leaf(X99,tptp0)
& next_subocc(X98,X99,tptp0)
& ( occurrence_of(X99,tptp1)
| occurrence_of(X99,tptp2) )
& next_subocc(X97,X98,tptp0)
& occurrence_of(X98,tptp4)
& next_subocc(X95,X97,tptp0)
& occurrence_of(X97,tptp3) )
| leaf_occ(X95,X96)
| ~ arboreal(X95)
| ~ subactivity_occurrence(X95,X96)
| ~ occurrence_of(X96,tptp0) ),
inference(fof_nnf,[status(thm)],[sos_32]) ).
fof(sk_sos_32_sk,plain,
! [X95,X96] :
( ( leaf(sK2(X95,X96),tptp0)
& next_subocc(sK1(X95,X96),sK2(X95,X96),tptp0)
& ( occurrence_of(sK2(X95,X96),tptp1)
| occurrence_of(sK2(X95,X96),tptp2) )
& next_subocc(sK0(X95,X96),sK1(X95,X96),tptp0)
& occurrence_of(sK1(X95,X96),tptp4)
& next_subocc(X95,sK0(X95,X96),tptp0)
& occurrence_of(sK0(X95,X96),tptp3) )
| leaf_occ(X95,X96)
| ~ arboreal(X95)
| ~ subactivity_occurrence(X95,X96)
| ~ occurrence_of(X96,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1,sK2]),skolemize(X97,sK0(X95,X96)),skolemize(X98,sK1(X95,X96)),skolemize(X99,sK2(X95,X96))],[nnf_33]) ).
fof(sk_sos_32,plain,
( ! [VAR_0,VAR_1] :
( leaf(sK2(VAR_1,VAR_0),tptp0)
| leaf_occ(VAR_1,VAR_0)
| ~ arboreal(VAR_1)
| ~ subactivity_occurrence(VAR_1,VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0,VAR_1] :
( next_subocc(sK1(VAR_1,VAR_0),sK2(VAR_1,VAR_0),tptp0)
| leaf_occ(VAR_1,VAR_0)
| ~ arboreal(VAR_1)
| ~ subactivity_occurrence(VAR_1,VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0,VAR_1] :
( occurrence_of(sK2(VAR_1,VAR_0),tptp1)
| occurrence_of(sK2(VAR_1,VAR_0),tptp2)
| leaf_occ(VAR_1,VAR_0)
| ~ arboreal(VAR_1)
| ~ subactivity_occurrence(VAR_1,VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0,VAR_1] :
( next_subocc(sK0(VAR_1,VAR_0),sK1(VAR_1,VAR_0),tptp0)
| leaf_occ(VAR_1,VAR_0)
| ~ arboreal(VAR_1)
| ~ subactivity_occurrence(VAR_1,VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0,VAR_1] :
( occurrence_of(sK1(VAR_1,VAR_0),tptp4)
| leaf_occ(VAR_1,VAR_0)
| ~ arboreal(VAR_1)
| ~ subactivity_occurrence(VAR_1,VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0,VAR_1] :
( next_subocc(VAR_1,sK0(VAR_1,VAR_0),tptp0)
| leaf_occ(VAR_1,VAR_0)
| ~ arboreal(VAR_1)
| ~ subactivity_occurrence(VAR_1,VAR_0)
| ~ occurrence_of(VAR_0,tptp0) )
& ! [VAR_0,VAR_1] :
( occurrence_of(sK0(VAR_1,VAR_0),tptp3)
| leaf_occ(VAR_1,VAR_0)
| ~ arboreal(VAR_1)
| ~ subactivity_occurrence(VAR_1,VAR_0)
| ~ occurrence_of(VAR_0,tptp0) ) ),
inference(cnf_transformation,[status(thm)],[sk_sos_32_sk]) ).
cnf(c_140,plain,
( occurrence_of(sK0(B,A),tptp3)
| leaf_occ(B,A)
| ~ arboreal(B)
| ~ subactivity_occurrence(B,A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_32]) ).
cnf(c_141,plain,
( next_subocc(B,sK0(B,A),tptp0)
| leaf_occ(B,A)
| ~ arboreal(B)
| ~ subactivity_occurrence(B,A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_32]) ).
cnf(c_143,plain,
( next_subocc(sK0(B,A),sK1(B,A),tptp0)
| leaf_occ(B,A)
| ~ arboreal(B)
| ~ subactivity_occurrence(B,A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_32]) ).
cnf(c_144,plain,
( occurrence_of(sK2(B,A),tptp1)
| occurrence_of(sK2(B,A),tptp2)
| leaf_occ(B,A)
| ~ arboreal(B)
| ~ subactivity_occurrence(B,A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_32]) ).
cnf(c_145,plain,
( next_subocc(sK1(B,A),sK2(B,A),tptp0)
| leaf_occ(B,A)
| ~ arboreal(B)
| ~ subactivity_occurrence(B,A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_32]) ).
cnf(c_146,plain,
( leaf(sK2(B,A),tptp0)
| leaf_occ(B,A)
| ~ arboreal(B)
| ~ subactivity_occurrence(B,A)
| ~ occurrence_of(A,tptp0) ),
inference(split_conjunct,[status(thm)],[sk_sos_32]) ).
fof(nnf_34,plain,
? [X100,X101] :
( ! [X102,X103] :
( ~ leaf(X103,tptp0)
| ~ min_precedes(X102,X103,tptp0)
| ( ~ occurrence_of(X103,tptp1)
& ~ occurrence_of(X103,tptp2) )
| ~ next_subocc(X100,X102,tptp0)
| ~ occurrence_of(X102,tptp3) )
& ~ leaf_occ(X100,X101)
& arboreal(X100)
& subactivity_occurrence(X100,X101)
& occurrence_of(X101,tptp0) ),
inference(fof_nnf,[status(thm)],[goals_neg]) ).
fof(sk_goals_neg_sk,plain,
( ! [X102,X103] :
( ~ leaf(X103,tptp0)
| ~ min_precedes(X102,X103,tptp0)
| ( ~ occurrence_of(X103,tptp1)
& ~ occurrence_of(X103,tptp2) )
| ~ next_subocc(sK4,X102,tptp0)
| ~ occurrence_of(X102,tptp3) )
& ~ leaf_occ(sK4,sK3)
& arboreal(sK4)
& subactivity_occurrence(sK4,sK3)
& occurrence_of(sK3,tptp0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4]),skolemize(X100,sK4),skolemize(X101,sK3)],[nnf_34]) ).
fof(sk_goals_neg,plain,
( ! [VAR_0,VAR_1] :
( ~ leaf(VAR_1,tptp0)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp1)
| ~ next_subocc(sK4,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ! [VAR_0,VAR_1] :
( ~ leaf(VAR_1,tptp0)
| ~ min_precedes(VAR_0,VAR_1,tptp0)
| ~ occurrence_of(VAR_1,tptp2)
| ~ next_subocc(sK4,VAR_0,tptp0)
| ~ occurrence_of(VAR_0,tptp3) )
& ~ leaf_occ(sK4,sK3)
& arboreal(sK4)
& subactivity_occurrence(sK4,sK3)
& occurrence_of(sK3,tptp0) ),
inference(cnf_transformation,[status(thm)],[sk_goals_neg_sk]) ).
cnf(c_158,negated_conjecture,
occurrence_of(sK3,tptp0),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_159,negated_conjecture,
subactivity_occurrence(sK4,sK3),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_160,negated_conjecture,
arboreal(sK4),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_161,negated_conjecture,
~ leaf_occ(sK4,sK3),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_162,negated_conjecture,
( ~ leaf(B,tptp0)
| ~ min_precedes(A,B,tptp0)
| ~ occurrence_of(B,tptp2)
| ~ next_subocc(sK4,A,tptp0)
| ~ occurrence_of(A,tptp3) ),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_163,negated_conjecture,
( ~ leaf(B,tptp0)
| ~ min_precedes(A,B,tptp0)
| ~ occurrence_of(B,tptp1)
| ~ next_subocc(sK4,A,tptp0)
| ~ occurrence_of(A,tptp3) ),
inference(split_conjunct,[status(thm)],[sk_goals_neg]) ).
cnf(c_658,negated_conjecture,
( leaf(sK2(sK4,sK3),tptp0)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4)
| ~ occurrence_of(sK3,tptp0) ),
inference(resolve,[status(thm)],[c_159,c_146]) ).
cnf(c_659,negated_conjecture,
( leaf(sK2(sK4,sK3),tptp0)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4) ),
inference(resolve,[status(thm)],[c_158,c_658]) ).
cnf(c_660,negated_conjecture,
( leaf(sK2(sK4,sK3),tptp0)
| leaf_occ(sK4,sK3) ),
inference(resolve,[status(thm)],[c_160,c_659]) ).
cnf(c_198,negated_conjecture,
leaf(sK2(sK4,sK3),tptp0),
inference(resolve,[status(thm)],[c_161,c_660]) ).
cnf(c_661,negated_conjecture,
( next_subocc(sK1(sK4,sK3),sK2(sK4,sK3),tptp0)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4)
| ~ occurrence_of(sK3,tptp0) ),
inference(resolve,[status(thm)],[c_159,c_145]) ).
cnf(c_662,negated_conjecture,
( next_subocc(sK1(sK4,sK3),sK2(sK4,sK3),tptp0)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4) ),
inference(resolve,[status(thm)],[c_158,c_661]) ).
cnf(c_663,negated_conjecture,
( next_subocc(sK1(sK4,sK3),sK2(sK4,sK3),tptp0)
| leaf_occ(sK4,sK3) ),
inference(resolve,[status(thm)],[c_160,c_662]) ).
cnf(c_199,negated_conjecture,
next_subocc(sK1(sK4,sK3),sK2(sK4,sK3),tptp0),
inference(resolve,[status(thm)],[c_161,c_663]) ).
cnf(c_664,negated_conjecture,
( occurrence_of(sK2(sK4,sK3),tptp1)
| occurrence_of(sK2(sK4,sK3),tptp2)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4)
| ~ occurrence_of(sK3,tptp0) ),
inference(resolve,[status(thm)],[c_159,c_144]) ).
cnf(c_665,negated_conjecture,
( occurrence_of(sK2(sK4,sK3),tptp1)
| occurrence_of(sK2(sK4,sK3),tptp2)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4) ),
inference(resolve,[status(thm)],[c_158,c_664]) ).
cnf(c_666,negated_conjecture,
( occurrence_of(sK2(sK4,sK3),tptp1)
| occurrence_of(sK2(sK4,sK3),tptp2)
| leaf_occ(sK4,sK3) ),
inference(resolve,[status(thm)],[c_160,c_665]) ).
cnf(c_200,negated_conjecture,
( occurrence_of(sK2(sK4,sK3),tptp1)
| occurrence_of(sK2(sK4,sK3),tptp2) ),
inference(resolve,[status(thm)],[c_161,c_666]) ).
cnf(c_667,negated_conjecture,
( next_subocc(sK0(sK4,sK3),sK1(sK4,sK3),tptp0)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4)
| ~ occurrence_of(sK3,tptp0) ),
inference(resolve,[status(thm)],[c_159,c_143]) ).
cnf(c_668,negated_conjecture,
( next_subocc(sK0(sK4,sK3),sK1(sK4,sK3),tptp0)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4) ),
inference(resolve,[status(thm)],[c_158,c_667]) ).
cnf(c_669,negated_conjecture,
( next_subocc(sK0(sK4,sK3),sK1(sK4,sK3),tptp0)
| leaf_occ(sK4,sK3) ),
inference(resolve,[status(thm)],[c_160,c_668]) ).
cnf(c_201,negated_conjecture,
next_subocc(sK0(sK4,sK3),sK1(sK4,sK3),tptp0),
inference(resolve,[status(thm)],[c_161,c_669]) ).
cnf(c_670,negated_conjecture,
( next_subocc(sK4,sK0(sK4,sK3),tptp0)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4)
| ~ occurrence_of(sK3,tptp0) ),
inference(resolve,[status(thm)],[c_159,c_141]) ).
cnf(c_671,negated_conjecture,
( next_subocc(sK4,sK0(sK4,sK3),tptp0)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4) ),
inference(resolve,[status(thm)],[c_158,c_670]) ).
cnf(c_672,negated_conjecture,
( next_subocc(sK4,sK0(sK4,sK3),tptp0)
| leaf_occ(sK4,sK3) ),
inference(resolve,[status(thm)],[c_160,c_671]) ).
cnf(c_203,negated_conjecture,
next_subocc(sK4,sK0(sK4,sK3),tptp0),
inference(resolve,[status(thm)],[c_161,c_672]) ).
cnf(c_673,negated_conjecture,
( occurrence_of(sK0(sK4,sK3),tptp3)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4)
| ~ occurrence_of(sK3,tptp0) ),
inference(resolve,[status(thm)],[c_159,c_140]) ).
cnf(c_674,negated_conjecture,
( occurrence_of(sK0(sK4,sK3),tptp3)
| leaf_occ(sK4,sK3)
| ~ arboreal(sK4) ),
inference(resolve,[status(thm)],[c_158,c_673]) ).
cnf(c_675,negated_conjecture,
( occurrence_of(sK0(sK4,sK3),tptp3)
| leaf_occ(sK4,sK3) ),
inference(resolve,[status(thm)],[c_160,c_674]) ).
cnf(c_204,negated_conjecture,
occurrence_of(sK0(sK4,sK3),tptp3),
inference(resolve,[status(thm)],[c_161,c_675]) ).
cnf(c_296,plain,
min_precedes(sK1(sK4,sK3),sK2(sK4,sK3),tptp0),
inference(resolve,[status(thm)],[c_199,c_107]) ).
cnf(c_676,negated_conjecture,
( ~ leaf(A,tptp0)
| ~ min_precedes(sK0(sK4,sK3),A,tptp0)
| ~ occurrence_of(A,tptp1)
| ~ occurrence_of(sK0(sK4,sK3),tptp3) ),
inference(resolve,[status(thm)],[c_203,c_163]) ).
cnf(c_319,negated_conjecture,
( ~ leaf(A,tptp0)
| ~ min_precedes(sK0(sK4,sK3),A,tptp0)
| ~ occurrence_of(A,tptp1) ),
inference(resolve,[status(thm)],[c_204,c_676]) ).
cnf(c_677,negated_conjecture,
( ~ leaf(A,tptp0)
| ~ min_precedes(sK0(sK4,sK3),A,tptp0)
| ~ occurrence_of(A,tptp2)
| ~ occurrence_of(sK0(sK4,sK3),tptp3) ),
inference(resolve,[status(thm)],[c_203,c_162]) ).
cnf(c_320,negated_conjecture,
( ~ leaf(A,tptp0)
| ~ min_precedes(sK0(sK4,sK3),A,tptp0)
| ~ occurrence_of(A,tptp2) ),
inference(resolve,[status(thm)],[c_204,c_677]) ).
cnf(c_342,plain,
min_precedes(sK0(sK4,sK3),sK1(sK4,sK3),tptp0),
inference(resolve,[status(thm)],[c_201,c_107]) ).
cnf(c_385,plain,
( min_precedes(A,sK2(sK4,sK3),tptp0)
| ~ min_precedes(A,sK1(sK4,sK3),tptp0) ),
inference(resolve,[status(thm)],[c_296,c_103]) ).
cnf(c_638,plain,
min_precedes(sK0(sK4,sK3),sK2(sK4,sK3),tptp0),
inference(resolve,[status(thm)],[c_385,c_342]) ).
cnf(c_678,plain,
( ~ leaf(sK2(sK4,sK3),tptp0)
| ~ occurrence_of(sK2(sK4,sK3),tptp2) ),
inference(resolve,[status(thm)],[c_638,c_320]) ).
cnf(c_640,plain,
~ occurrence_of(sK2(sK4,sK3),tptp2),
inference(resolve,[status(thm)],[c_198,c_678]) ).
cnf(c_679,plain,
( ~ leaf(sK2(sK4,sK3),tptp0)
| ~ occurrence_of(sK2(sK4,sK3),tptp1) ),
inference(resolve,[status(thm)],[c_638,c_319]) ).
cnf(c_641,plain,
~ occurrence_of(sK2(sK4,sK3),tptp1),
inference(resolve,[status(thm)],[c_198,c_679]) ).
cnf(c_680,negated_conjecture,
occurrence_of(sK2(sK4,sK3),tptp1),
inference(resolve,[status(thm)],[c_640,c_200]) ).
cnf(c_657,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_641,c_680]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : PRO014+2 : TPTP v9.3.1. Released v4.0.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.17/5.45 % Computer : n020.cluster.edu
% 0.17/5.45 % Model : x86_64 x86_64
% 0.17/5.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/5.45 % Memory : 8046.5625MB
% 0.17/5.45 % OS : Linux 6.8.0-71-generic
% 0.17/5.45 % CPULimit : 300
% 0.17/5.45 % WCLimit : 300
% 0.17/5.45 % DateTime : Sat Sep 26 05:00:10 UTC 2026
% 0.17/5.45 % CPUTime :
% 0.17/5.46 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/5.46 % Process 660229 was started by sandbox2 on n020,
% 0.17/5.46 % Sat Sep 26 05:00:10 2026
% 0.17/5.46 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.17/5.48
% 0.17/5.48 % From the command line: assign(max_seconds, 300).
% 0.23/5.54
% 0.23/5.54 % SZS status Theorem for theBenchmark
% 0.23/5.54
% 0.23/5.54 % Proof 1 at 0.04 (+ 0.02) seconds.
% 0.23/5.54 % Length of proof is 33.
% 0.23/5.54 % Level of proof is 7.
% 0.23/5.54 % Maximum clause weight is 31.000.
% 0.23/5.54 % Given clauses 230.
% 0.23/5.54
% 0.23/5.54 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------