%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWW102+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n026.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 09:13:53 AM UTC 2026
% Result : Theorem 17.48s 2.66s
% Output : CNFRefutation 17.48s
% Verified :
% SZS Type : Refutation
% Derivation depth : 45
% Number of leaves : 19
% Syntax : Number of formulae : 153 ( 59 unt; 0 def)
% Number of atoms : 282 ( 211 equ)
% Maximal formula atoms : 9 ( 1 avg)
% Number of connectives : 197 ( 68 ~; 107 |; 14 &)
% ( 4 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 2 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 5 ( 3 usr; 1 prp; 0-2 aty)
% Number of functors : 13 ( 13 usr; 6 con; 0-2 aty)
% Number of variables : 68 ( 4 sgn 19 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(def_bool,axiom,
! [X] :
( bool(X)
<=> ( X = true
| X = false ) ),
file('theBenchmark.p',def_bool) ).
fof(distinct_false_true_err,axiom,
( false != err
& true != err
& true != false ),
file('theBenchmark.p',distinct_false_true_err) ).
fof(false_true_err_in_d,axiom,
( d(err)
& d(false)
& d(true) ),
file('theBenchmark.p',false_true_err_in_d) ).
fof(def_forallprefers,axiom,
! [X,Y] :
( forallprefers(X,Y)
<=> ( ( Y = true
& X = false )
| ( bool(Y)
& ~ bool(X)
& d(Y)
& d(X) )
| ( d(Y)
& ~ d(X) ) ) ),
file('theBenchmark.p',def_forallprefers) ).
fof(def_phi,axiom,
! [X] :
( ( phi(X) = err
& ~ d(X) )
| ( phi(X) = X
& d(X) ) ),
file('theBenchmark.p',def_phi) ).
fof(prop_true,axiom,
! [X] :
( prop(X) = true
<=> bool(X) ),
file('theBenchmark.p',prop_true) ).
fof(prop_false,axiom,
! [X] :
( prop(X) = false
<=> ~ bool(X) ),
file('theBenchmark.p',prop_false) ).
fof(impl_axiom1,axiom,
! [A,B] :
( ~ bool(A)
=> impl(A,B) = phi(A) ),
file('theBenchmark.p',impl_axiom1) ).
fof(impl_axiom3,axiom,
! [B] :
( bool(B)
=> impl(false,B) = true ),
file('theBenchmark.p',impl_axiom3) ).
fof(impl_axiom4,axiom,
! [B] :
( bool(B)
=> impl(true,B) = B ),
file('theBenchmark.p',impl_axiom4) ).
fof(lazy_impl_axiom2,axiom,
! [B] : lazy_impl(false,B) = true,
file('theBenchmark.p',lazy_impl_axiom2) ).
fof(lazy_impl_axiom3,axiom,
! [B] : lazy_impl(true,B) = phi(B),
file('theBenchmark.p',lazy_impl_axiom3) ).
fof(def_f7,axiom,
! [P] : f7(P) = lazy_impl(prop(P),P),
file('theBenchmark.p',def_f7) ).
fof(def_false2,axiom,
? [P] :
( ~ ? [P1] : forallprefers(f7(P1),f7(P))
& false2 = phi(f7(P)) ),
file('theBenchmark.p',def_false2) ).
fof(not1_axiom1,axiom,
! [A] :
( ~ bool(A)
=> not1(A) = phi(A) ),
file('theBenchmark.p',not1_axiom1) ).
fof(def_not2,axiom,
! [P] : not2(P) = impl(P,false2),
file('theBenchmark.p',def_not2) ).
fof(not1_not2,conjecture,
! [P] : not1(P) = not2(P),
file('theBenchmark.p',not1_not2) ).
fof(not1_not2_neg,negated_conjecture,
~ ! [P] : not1(P) = not2(P),
inference(assume_negation,[status(cth)],[not1_not2]) ).
cnf(c_43,plain,
( A = true
| A = false
| ~ bool(A) ),
inference(clausify,[status(thm)],[def_bool]) ).
cnf(c_3838,plain,
( A = true
| false = A
| ~ bool(A) ),
inference(copy,[status(thm)],[c_43]) ).
cnf(c_44,plain,
( true = A
| false = A
| ~ bool(A) ),
inference(copy,[status(thm)],[c_3838]) ).
cnf(c_45,plain,
( A != false
| bool(A) ),
inference(clausify,[status(thm)],[def_bool]) ).
cnf(c_46,plain,
( false != A
| bool(A) ),
inference(copy,[status(thm)],[c_45]) ).
cnf(c_49,plain,
true != false,
inference(clausify,[status(thm)],[distinct_false_true_err]) ).
cnf(c_50,plain,
false != true,
inference(copy,[status(thm)],[c_49]) ).
cnf(c_52,plain,
err != false,
inference(clausify,[status(thm)],[distinct_false_true_err]) ).
cnf(c_53,plain,
d(true),
inference(clausify,[status(thm)],[false_true_err_in_d]) ).
cnf(c_54,plain,
d(false),
inference(clausify,[status(thm)],[false_true_err_in_d]) ).
cnf(c_68,plain,
( ~ d(B)
| d(A)
| forallprefers(A,B) ),
inference(clausify,[status(thm)],[def_forallprefers]) ).
cnf(c_70,plain,
( B != true
| A != false
| forallprefers(A,B) ),
inference(clausify,[status(thm)],[def_forallprefers]) ).
cnf(c_3839,plain,
( B != true
| false != A
| forallprefers(A,B) ),
inference(copy,[status(thm)],[c_70]) ).
cnf(c_71,plain,
( true != B
| false != A
| forallprefers(A,B) ),
inference(copy,[status(thm)],[c_3839]) ).
cnf(c_88,plain,
( phi(A) = err
| d(A) ),
inference(clausify,[status(thm)],[def_phi]) ).
cnf(c_89,plain,
( ~ d(A)
| phi(A) = A ),
inference(clausify,[status(thm)],[def_phi]) ).
cnf(c_90,plain,
( phi(A) = err
| phi(A) = A ),
inference(clausify,[status(thm)],[def_phi]) ).
cnf(c_91,plain,
( bool(A)
| prop(A) != true ),
inference(clausify,[status(thm)],[prop_true]) ).
cnf(c_92,plain,
( ~ bool(A)
| prop(A) = true ),
inference(clausify,[status(thm)],[prop_true]) ).
cnf(c_94,plain,
( bool(A)
| prop(A) = false ),
inference(clausify,[status(thm)],[prop_false]) ).
cnf(c_95,plain,
( impl(A,B) = phi(A)
| bool(A) ),
inference(clausify,[status(thm)],[impl_axiom1]) ).
cnf(c_97,plain,
( impl(false,A) = true
| ~ bool(A) ),
inference(clausify,[status(thm)],[impl_axiom3]) ).
cnf(c_98,plain,
( impl(true,A) = A
| ~ bool(A) ),
inference(clausify,[status(thm)],[impl_axiom4]) ).
cnf(c_100,plain,
lazy_impl(false,A) = true,
inference(clausify,[status(thm)],[lazy_impl_axiom2]) ).
cnf(c_101,plain,
lazy_impl(true,A) = phi(A),
inference(clausify,[status(thm)],[lazy_impl_axiom3]) ).
cnf(c_142,plain,
f7(A) = lazy_impl(prop(A),A),
inference(clausify,[status(thm)],[def_f7]) ).
fof(nnf_39,plain,
? [P] :
( ! [P1] : ~ forallprefers(f7(P1),f7(P))
& phi(f7(P)) = false2 ),
inference(fof_nnf,[status(thm)],[def_false2]) ).
fof(sk_def_false2,plain,
( ! [P1] : ~ forallprefers(f7(P1),f7(sK0))
& phi(f7(sK0)) = false2 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(P,sK0)],[nnf_39]) ).
cnf(c_143,plain,
phi(f7(sK0)) = false2,
inference(split_conjunct,[status(thm)],[sk_def_false2]) ).
cnf(c_144,plain,
phi(lazy_impl(prop(sK0),sK0)) = false2,
inference(paramod,[status(thm)],[c_142,c_143]) ).
cnf(c_145,plain,
~ forallprefers(f7(A),f7(sK0)),
inference(split_conjunct,[status(thm)],[sk_def_false2]) ).
cnf(c_3840,plain,
~ forallprefers(lazy_impl(prop(A),A),f7(sK0)),
inference(paramod,[status(thm)],[c_142,c_145]) ).
cnf(c_146,plain,
~ forallprefers(lazy_impl(prop(A),A),lazy_impl(prop(sK0),sK0)),
inference(paramod,[status(thm)],[c_142,c_3840]) ).
cnf(c_147,plain,
( not1(A) = phi(A)
| bool(A) ),
inference(clausify,[status(thm)],[not1_axiom1]) ).
fof(not1_axiom2,axiom,
not1(false) = true,
file('theBenchmark.p',not1_axiom2) ).
cnf(c_148,plain,
not1(false) = true,
inference(clausify,[status(thm)],[not1_axiom2]) ).
fof(not1_axiom3,axiom,
not1(true) = false,
file('theBenchmark.p',not1_axiom3) ).
cnf(c_149,plain,
not1(true) = false,
inference(clausify,[status(thm)],[not1_axiom3]) ).
cnf(c_150,plain,
not2(A) = impl(A,false2),
inference(clausify,[status(thm)],[def_not2]) ).
cnf(c_151,plain,
impl(A,false2) = not2(A),
inference(copy,[status(thm)],[c_150]) ).
fof(nnf_42,plain,
? [P] : not2(P) != not1(P),
inference(fof_nnf,[status(thm)],[not1_not2_neg]) ).
fof(sk_not1_not2_neg,plain,
not2(sK1) != not1(sK1),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(P,sK1)],[nnf_42]) ).
cnf(c_152,negated_conjecture,
not2(sK1) != not1(sK1),
inference(split_conjunct,[status(thm)],[sk_not1_not2_neg]) ).
cnf(c_154,plain,
bool(false),
inference(xxres,[status(thm)],[c_46]) ).
cnf(c_163,plain,
( true != A
| forallprefers(false,A) ),
inference(xxres,[status(thm)],[c_71]) ).
cnf(c_3841,plain,
( true != A
| forallprefers(false,A) ),
inference(xxres,[status(thm)],[c_71]) ).
cnf(c_165,plain,
forallprefers(false,true),
inference(xxres,[status(thm)],[c_3841]) ).
cnf(c_180,plain,
( d(B)
| forallprefers(B,A)
| phi(A) = err ),
inference(resolve,[status(thm)],[c_88,c_68]) ).
cnf(c_181,plain,
phi(false) = false,
inference(resolve,[status(thm)],[c_89,c_54]) ).
cnf(c_182,plain,
phi(true) = true,
inference(resolve,[status(thm)],[c_89,c_53]) ).
cnf(c_183,plain,
( prop(A) = true
| prop(A) = false ),
inference(resolve,[status(thm)],[c_94,c_92]) ).
cnf(c_184,plain,
( true = A
| false = A
| prop(A) = false ),
inference(resolve,[status(thm)],[c_94,c_44]) ).
cnf(c_202,plain,
( prop(A) = true
| impl(A,B) = phi(A) ),
inference(resolve,[status(thm)],[c_95,c_92]) ).
cnf(c_3842,plain,
( phi(lazy_impl(prop(sK0),sK0)) = err
| false2 = lazy_impl(prop(sK0),sK0) ),
inference(paramod,[status(thm)],[c_144,c_90]) ).
cnf(c_3843,plain,
( false2 = err
| false2 = lazy_impl(prop(sK0),sK0) ),
inference(paramod,[status(thm)],[c_144,c_3842]) ).
cnf(c_345,plain,
( false2 = err
| lazy_impl(prop(sK0),sK0) = false2 ),
inference(copy,[status(thm)],[c_3843]) ).
cnf(c_356,plain,
( prop(A) = true
| not1(A) = phi(A) ),
inference(resolve,[status(thm)],[c_147,c_92]) ).
cnf(c_386,plain,
prop(false) = true,
inference(resolve,[status(thm)],[c_154,c_92]) ).
cnf(c_3844,plain,
~ forallprefers(lazy_impl(true,false),lazy_impl(prop(sK0),sK0)),
inference(paramod,[status(thm)],[c_386,c_146]) ).
cnf(c_3845,plain,
~ forallprefers(phi(false),lazy_impl(prop(sK0),sK0)),
inference(paramod,[status(thm)],[c_101,c_3844]) ).
cnf(c_435,plain,
~ forallprefers(false,lazy_impl(prop(sK0),sK0)),
inference(paramod,[status(thm)],[c_181,c_3845]) ).
cnf(c_3846,plain,
true != lazy_impl(prop(sK0),sK0),
inference(resolve,[status(thm)],[c_163,c_435]) ).
cnf(c_440,plain,
lazy_impl(prop(sK0),sK0) != true,
inference(copy,[status(thm)],[c_3846]) ).
cnf(c_3847,plain,
( ~ forallprefers(false,lazy_impl(false,sK0))
| prop(sK0) = true ),
inference(paramod,[status(thm)],[c_183,c_435]) ).
cnf(c_3848,plain,
( ~ forallprefers(false,true)
| prop(sK0) = true ),
inference(paramod,[status(thm)],[c_100,c_3847]) ).
cnf(c_545,plain,
prop(sK0) = true,
inference(resolve,[status(thm)],[c_165,c_3848]) ).
cnf(c_3849,plain,
lazy_impl(true,sK0) != true,
inference(paramod,[status(thm)],[c_545,c_440]) ).
cnf(c_557,plain,
phi(sK0) != true,
inference(paramod,[status(thm)],[c_101,c_3849]) ).
cnf(c_3850,plain,
( false2 = err
| lazy_impl(true,sK0) = false2 ),
inference(paramod,[status(thm)],[c_545,c_345]) ).
cnf(c_559,plain,
( false2 = err
| phi(sK0) = false2 ),
inference(paramod,[status(thm)],[c_101,c_3850]) ).
cnf(c_3851,plain,
~ forallprefers(lazy_impl(prop(A),A),lazy_impl(true,sK0)),
inference(paramod,[status(thm)],[c_545,c_146]) ).
cnf(c_560,plain,
~ forallprefers(lazy_impl(prop(A),A),phi(sK0)),
inference(paramod,[status(thm)],[c_101,c_3851]) ).
cnf(c_3852,plain,
phi(lazy_impl(true,sK0)) = false2,
inference(paramod,[status(thm)],[c_545,c_144]) ).
cnf(c_561,plain,
phi(phi(sK0)) = false2,
inference(paramod,[status(thm)],[c_101,c_3852]) ).
cnf(c_574,plain,
bool(sK0),
inference(resolve,[status(thm)],[c_545,c_91]) ).
cnf(c_3853,plain,
~ forallprefers(lazy_impl(true,sK0),phi(sK0)),
inference(paramod,[status(thm)],[c_545,c_560]) ).
cnf(c_586,plain,
~ forallprefers(phi(sK0),phi(sK0)),
inference(paramod,[status(thm)],[c_101,c_3853]) ).
cnf(c_594,plain,
impl(false,sK0) = true,
inference(resolve,[status(thm)],[c_574,c_97]) ).
cnf(c_3854,plain,
( true = sK0
| false = sK0 ),
inference(resolve,[status(thm)],[c_574,c_44]) ).
cnf(c_3855,plain,
( true = sK0
| sK0 = false ),
inference(copy,[status(thm)],[c_3854]) ).
cnf(c_596,plain,
( sK0 = true
| sK0 = false ),
inference(copy,[status(thm)],[c_3855]) ).
cnf(c_3856,plain,
( ~ forallprefers(phi(sK0),phi(false))
| sK0 = true ),
inference(paramod,[status(thm)],[c_596,c_586]) ).
cnf(c_629,plain,
( ~ forallprefers(phi(sK0),false)
| sK0 = true ),
inference(paramod,[status(thm)],[c_181,c_3856]) ).
cnf(c_3857,plain,
( false2 = err
| phi(sK0) = sK0
| false2 = err ),
inference(paramod,[status(thm)],[c_559,c_90]) ).
cnf(c_778,plain,
( phi(sK0) = sK0
| false2 = err ),
inference(copy,[status(thm)],[c_3857]) ).
cnf(c_3858,plain,
( d(phi(sK0))
| phi(false) = err
| sK0 = true ),
inference(resolve,[status(thm)],[c_629,c_180]) ).
cnf(c_3859,plain,
( d(phi(sK0))
| false = err
| sK0 = true ),
inference(paramod,[status(thm)],[c_181,c_3858]) ).
cnf(c_3860,plain,
( d(phi(sK0))
| err = false
| sK0 = true ),
inference(copy,[status(thm)],[c_3859]) ).
cnf(c_970,plain,
( d(phi(sK0))
| sK0 = true ),
inference(resolve,[status(thm)],[c_52,c_3860]) ).
cnf(c_3861,plain,
( phi(phi(sK0)) = phi(sK0)
| sK0 = true ),
inference(resolve,[status(thm)],[c_970,c_89]) ).
cnf(c_3862,plain,
( false2 = phi(sK0)
| sK0 = true ),
inference(paramod,[status(thm)],[c_561,c_3861]) ).
cnf(c_1030,plain,
( phi(sK0) = false2
| sK0 = true ),
inference(copy,[status(thm)],[c_3862]) ).
cnf(c_3863,plain,
( false2 = err
| sK0 = false2
| false2 = err ),
inference(paramod,[status(thm)],[c_778,c_559]) ).
cnf(c_1102,plain,
( sK0 = false2
| false2 = err ),
inference(copy,[status(thm)],[c_3863]) ).
cnf(c_1155,plain,
( bool(false2)
| false2 = err ),
inference(paramod,[status(thm)],[c_1102,c_574]) ).
cnf(c_3864,plain,
( impl(false,false2) = true
| false2 = err ),
inference(paramod,[status(thm)],[c_1102,c_594]) ).
cnf(c_1165,plain,
( not2(false) = true
| false2 = err ),
inference(paramod,[status(thm)],[c_151,c_3864]) ).
cnf(c_3865,plain,
( impl(true,false2) = false2
| false2 = err ),
inference(resolve,[status(thm)],[c_1155,c_98]) ).
cnf(c_1188,plain,
( not2(true) = false2
| false2 = err ),
inference(paramod,[status(thm)],[c_151,c_3865]) ).
cnf(c_3866,plain,
( phi(A) = not2(A)
| prop(A) = true ),
inference(paramod,[status(thm)],[c_202,c_151]) ).
cnf(c_1244,plain,
( not2(A) = phi(A)
| prop(A) = true ),
inference(copy,[status(thm)],[c_3866]) ).
cnf(c_3867,plain,
( phi(false) = false2
| sK0 = true
| sK0 = true ),
inference(paramod,[status(thm)],[c_596,c_1030]) ).
cnf(c_3868,plain,
( false = false2
| sK0 = true
| sK0 = true ),
inference(paramod,[status(thm)],[c_181,c_3867]) ).
cnf(c_3869,plain,
( false2 = false
| sK0 = true
| sK0 = true ),
inference(copy,[status(thm)],[c_3868]) ).
cnf(c_1858,plain,
( false2 = false
| sK0 = true ),
inference(copy,[status(thm)],[c_3869]) ).
cnf(c_3870,plain,
( phi(true) != true
| false2 = false ),
inference(paramod,[status(thm)],[c_1858,c_557]) ).
cnf(c_3871,plain,
( true != true
| false2 = false ),
inference(paramod,[status(thm)],[c_182,c_3870]) ).
cnf(c_1979,plain,
false2 = false,
inference(copy,[status(thm)],[c_3871]) ).
cnf(c_3872,plain,
( not2(true) = false2
| false = err ),
inference(paramod,[status(thm)],[c_1979,c_1188]) ).
cnf(c_3873,plain,
( not2(true) = false
| false = err ),
inference(paramod,[status(thm)],[c_1979,c_3872]) ).
cnf(c_3874,plain,
( not2(true) = false
| err = false ),
inference(copy,[status(thm)],[c_3873]) ).
cnf(c_2040,plain,
not2(true) = false,
inference(resolve,[status(thm)],[c_52,c_3874]) ).
cnf(c_3875,plain,
( not2(false) = true
| false = err ),
inference(paramod,[status(thm)],[c_1979,c_1165]) ).
cnf(c_3876,plain,
( not2(false) = true
| err = false ),
inference(copy,[status(thm)],[c_3875]) ).
cnf(c_2050,plain,
not2(false) = true,
inference(resolve,[status(thm)],[c_52,c_3876]) ).
cnf(c_3325,plain,
( not2(sK1) != phi(sK1)
| prop(sK1) = true ),
inference(paramod,[status(thm)],[c_356,c_152]) ).
cnf(c_3877,plain,
( prop(sK1) = true
| prop(sK1) = true ),
inference(resolve,[status(thm)],[c_3325,c_1244]) ).
cnf(c_3593,plain,
prop(sK1) = true,
inference(copy,[status(thm)],[c_3877]) ).
cnf(c_3878,plain,
( true = sK1
| false = sK1
| true = false ),
inference(paramod,[status(thm)],[c_3593,c_184]) ).
cnf(c_3879,plain,
( true = sK1
| false = sK1
| false = true ),
inference(copy,[status(thm)],[c_3878]) ).
cnf(c_3880,plain,
( true = sK1
| sK1 = false
| false = true ),
inference(copy,[status(thm)],[c_3879]) ).
cnf(c_3881,plain,
( sK1 = true
| sK1 = false
| false = true ),
inference(copy,[status(thm)],[c_3880]) ).
cnf(c_3601,plain,
( sK1 = true
| sK1 = false ),
inference(resolve,[status(thm)],[c_50,c_3881]) ).
cnf(c_3882,plain,
( not2(false) != not1(sK1)
| sK1 = true ),
inference(paramod,[status(thm)],[c_3601,c_152]) ).
cnf(c_3883,plain,
( true != not1(sK1)
| sK1 = true ),
inference(paramod,[status(thm)],[c_2050,c_3882]) ).
cnf(c_3754,plain,
( not1(sK1) != true
| sK1 = true ),
inference(copy,[status(thm)],[c_3883]) ).
cnf(c_3884,plain,
( not1(false) != true
| sK1 = true
| sK1 = true ),
inference(paramod,[status(thm)],[c_3601,c_3754]) ).
cnf(c_3885,plain,
( true != true
| sK1 = true
| sK1 = true ),
inference(paramod,[status(thm)],[c_148,c_3884]) ).
cnf(c_3886,plain,
( sK1 = true
| sK1 = true ),
inference(copy,[status(thm)],[c_3885]) ).
cnf(c_3836,plain,
sK1 = true,
inference(copy,[status(thm)],[c_3886]) ).
cnf(c_3887,negated_conjecture,
not2(true) != not1(sK1),
inference(paramod,[status(thm)],[c_3836,c_152]) ).
cnf(c_3888,negated_conjecture,
false != not1(sK1),
inference(paramod,[status(thm)],[c_2040,c_3887]) ).
cnf(c_3889,negated_conjecture,
false != not1(true),
inference(paramod,[status(thm)],[c_3836,c_3888]) ).
cnf(c_3890,negated_conjecture,
false != false,
inference(paramod,[status(thm)],[c_149,c_3889]) ).
cnf(c_3837,negated_conjecture,
$false,
inference(copy,[status(thm)],[c_3890]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW102+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n026.cluster.edu
% 0.08/0.35 % Model : x86_64 x86_64
% 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.35 % Memory : 8046.5625MB
% 0.08/0.35 % OS : Linux 6.8.0-71-generic
% 0.08/0.35 % CPULimit : 300
% 0.08/0.35 % WCLimit : 300
% 0.08/0.35 % DateTime : Sat Sep 26 15:26:56 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.08/0.36 % Process 1346995 was started by sandbox2 on n026,
% 0.08/0.36 % Sat Sep 26 15:26:56 2026
% 0.08/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.08/0.38
% 0.08/0.38 % From the command line: assign(max_seconds, 300).
% 17.48/2.66
% 17.48/2.66 % SZS status Theorem for theBenchmark
% 17.48/2.66
% 17.48/2.66 % Proof 1 at 1.62 (+ 0.61) seconds.
% 17.48/2.66 % Length of proof is 93.
% 17.48/2.66 % Level of proof is 17.
% 17.48/2.66 % Maximum clause weight is 27.000.
% 17.48/2.66 % Given clauses 452.
% 17.48/2.66
% 17.48/2.66 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------