%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWW101+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 : n013.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 2.59s 0.89s
% Output : CNFRefutation 2.59s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 13
% Syntax : Number of formulae : 72 ( 47 unt; 0 def)
% Number of atoms : 114 ( 67 equ)
% Maximal formula atoms : 9 ( 1 avg)
% Number of connectives : 79 ( 37 ~; 26 |; 12 &)
% ( 4 <=>; 0 =>; 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 : 11 ( 11 usr; 6 con; 0-2 aty)
% Number of variables : 35 ( 2 sgn 11 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(def_bool,axiom,
! [X] :
( bool(X)
<=> ( X = true
| X = false ) ),
file('theBenchmark.p',def_bool) ).
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(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(false1_false2,conjecture,
false1 = false2,
file('theBenchmark.p',false1_false2) ).
fof(false1_false2_neg,negated_conjecture,
false1 != false2,
inference(assume_negation,[status(cth)],[false1_false2]) ).
cnf(c_43,plain,
( A = true
| A = false
| ~ bool(A) ),
inference(clausify,[status(thm)],[def_bool]) ).
cnf(c_1567,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_1567]) ).
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_54,plain,
d(true),
inference(clausify,[status(thm)],[false_true_err_in_d]) ).
cnf(c_55,plain,
d(false),
inference(clausify,[status(thm)],[false_true_err_in_d]) ).
cnf(c_71,plain,
( B != true
| A != false
| forallprefers(A,B) ),
inference(clausify,[status(thm)],[def_forallprefers]) ).
cnf(c_1568,plain,
( B != true
| false != A
| forallprefers(A,B) ),
inference(copy,[status(thm)],[c_71]) ).
cnf(c_72,plain,
( true != B
| false != A
| forallprefers(A,B) ),
inference(copy,[status(thm)],[c_1568]) ).
cnf(c_90,plain,
( ~ d(A)
| phi(A) = A ),
inference(clausify,[status(thm)],[def_phi]) ).
cnf(c_93,plain,
( ~ bool(A)
| prop(A) = true ),
inference(clausify,[status(thm)],[prop_true]) ).
cnf(c_95,plain,
( bool(A)
| prop(A) = false ),
inference(clausify,[status(thm)],[prop_false]) ).
cnf(c_101,plain,
lazy_impl(false,A) = true,
inference(clausify,[status(thm)],[lazy_impl_axiom2]) ).
cnf(c_102,plain,
lazy_impl(true,A) = phi(A),
inference(clausify,[status(thm)],[lazy_impl_axiom3]) ).
fof(def_false1,axiom,
false1 = false,
file('theBenchmark.p',def_false1) ).
cnf(c_142,plain,
false1 = false,
inference(clausify,[status(thm)],[def_false1]) ).
cnf(c_143,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_144,plain,
phi(f7(sK0)) = false2,
inference(split_conjunct,[status(thm)],[sk_def_false2]) ).
cnf(c_145,plain,
phi(lazy_impl(prop(sK0),sK0)) = false2,
inference(paramod,[status(thm)],[c_143,c_144]) ).
cnf(c_146,plain,
~ forallprefers(f7(A),f7(sK0)),
inference(split_conjunct,[status(thm)],[sk_def_false2]) ).
cnf(c_1569,plain,
~ forallprefers(lazy_impl(prop(A),A),f7(sK0)),
inference(paramod,[status(thm)],[c_143,c_146]) ).
cnf(c_147,plain,
~ forallprefers(lazy_impl(prop(A),A),lazy_impl(prop(sK0),sK0)),
inference(paramod,[status(thm)],[c_143,c_1569]) ).
fof(not1_axiom2,axiom,
not1(false) = true,
file('theBenchmark.p',not1_axiom2) ).
cnf(c_150,plain,
not1(false) = true,
inference(clausify,[status(thm)],[not1_axiom2]) ).
cnf(c_154,negated_conjecture,
false2 != false1,
inference(clausify,[status(thm)],[false1_false2_neg]) ).
cnf(c_155,negated_conjecture,
false2 != false,
inference(paramod,[status(thm)],[c_142,c_154]) ).
cnf(c_157,plain,
bool(false),
inference(xxres,[status(thm)],[c_46]) ).
cnf(c_169,plain,
( true != A
| forallprefers(false,A) ),
inference(xxres,[status(thm)],[c_72]) ).
cnf(c_196,plain,
phi(false) = false,
inference(resolve,[status(thm)],[c_90,c_55]) ).
cnf(c_197,plain,
phi(true) = true,
inference(resolve,[status(thm)],[c_90,c_54]) ).
cnf(c_421,plain,
prop(false) = true,
inference(resolve,[status(thm)],[c_157,c_93]) ).
cnf(c_1570,plain,
true = not1(false),
inference(copy,[status(thm)],[c_150]) ).
cnf(c_1571,plain,
forallprefers(false,not1(false)),
inference(resolve,[status(thm)],[c_169,c_1570]) ).
cnf(c_517,plain,
forallprefers(false,true),
inference(paramod,[status(thm)],[c_150,c_1571]) ).
cnf(c_1572,plain,
~ forallprefers(lazy_impl(true,false),lazy_impl(prop(sK0),sK0)),
inference(paramod,[status(thm)],[c_421,c_147]) ).
cnf(c_1573,plain,
~ forallprefers(phi(false),lazy_impl(prop(sK0),sK0)),
inference(paramod,[status(thm)],[c_102,c_1572]) ).
cnf(c_1004,plain,
~ forallprefers(false,lazy_impl(prop(sK0),sK0)),
inference(paramod,[status(thm)],[c_196,c_1573]) ).
cnf(c_1574,plain,
true != lazy_impl(prop(sK0),sK0),
inference(resolve,[status(thm)],[c_169,c_1004]) ).
cnf(c_1052,plain,
lazy_impl(prop(sK0),sK0) != true,
inference(copy,[status(thm)],[c_1574]) ).
cnf(c_1575,plain,
( ~ forallprefers(false,lazy_impl(false,sK0))
| bool(sK0) ),
inference(paramod,[status(thm)],[c_95,c_1004]) ).
cnf(c_1576,plain,
( ~ forallprefers(false,true)
| bool(sK0) ),
inference(paramod,[status(thm)],[c_101,c_1575]) ).
cnf(c_1053,plain,
bool(sK0),
inference(resolve,[status(thm)],[c_517,c_1576]) ).
cnf(c_1076,plain,
prop(sK0) = true,
inference(resolve,[status(thm)],[c_1053,c_93]) ).
cnf(c_1083,plain,
( true = sK0
| false = sK0 ),
inference(resolve,[status(thm)],[c_1053,c_44]) ).
cnf(c_1577,plain,
lazy_impl(true,sK0) != true,
inference(paramod,[status(thm)],[c_1076,c_1052]) ).
cnf(c_1084,plain,
phi(sK0) != true,
inference(paramod,[status(thm)],[c_102,c_1577]) ).
cnf(c_1578,plain,
phi(lazy_impl(true,sK0)) = false2,
inference(paramod,[status(thm)],[c_1076,c_145]) ).
cnf(c_1097,plain,
phi(phi(sK0)) = false2,
inference(paramod,[status(thm)],[c_102,c_1578]) ).
cnf(c_1579,plain,
( phi(sK0) = true
| false = sK0 ),
inference(paramod,[status(thm)],[c_1083,c_197]) ).
cnf(c_1264,plain,
false = sK0,
inference(resolve,[status(thm)],[c_1084,c_1579]) ).
cnf(c_1580,plain,
phi(sK0) = false,
inference(paramod,[status(thm)],[c_1264,c_196]) ).
cnf(c_1528,plain,
phi(sK0) = sK0,
inference(paramod,[status(thm)],[c_1264,c_1580]) ).
cnf(c_1542,negated_conjecture,
false2 != sK0,
inference(paramod,[status(thm)],[c_1264,c_155]) ).
cnf(c_1581,plain,
phi(sK0) = false2,
inference(paramod,[status(thm)],[c_1528,c_1097]) ).
cnf(c_1582,plain,
sK0 = false2,
inference(paramod,[status(thm)],[c_1528,c_1581]) ).
cnf(c_1583,plain,
false2 = sK0,
inference(copy,[status(thm)],[c_1582]) ).
cnf(c_1566,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_1542,c_1583]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW101+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.20/0.46 % Computer : n013.cluster.edu
% 0.20/0.46 % Model : x86_64 x86_64
% 0.20/0.46 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.20/0.46 % Memory : 8046.5625MB
% 0.20/0.46 % OS : Linux 6.8.0-71-generic
% 0.20/0.46 % CPULimit : 300
% 0.20/0.46 % WCLimit : 300
% 0.20/0.46 % DateTime : Sat Sep 26 15:23:51 UTC 2026
% 0.20/0.46 % CPUTime :
% 0.20/0.47 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.20/0.47 % Process 3040242 was started by sandbox2 on n013,
% 0.20/0.47 % Sat Sep 26 15:23:51 2026
% 0.20/0.47 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.20/0.49
% 0.20/0.49 % From the command line: assign(max_seconds, 300).
% 2.59/0.89
% 2.59/0.89 % SZS status Theorem for theBenchmark
% 2.59/0.89
% 2.59/0.89 % Proof 1 at 0.22 (+ 0.08) seconds.
% 2.59/0.89 % Length of proof is 50.
% 2.59/0.89 % Level of proof is 11.
% 2.59/0.89 % Maximum clause weight is 15.000.
% 2.59/0.89 % Given clauses 165.
% 2.59/0.89
% 2.59/0.89 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------