%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW101+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n014.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 : Thu Sep 24 03:07:22 PM UTC 2026
% Result : Theorem 0.11s 0.43s
% Output : CNFRefutation 0.11s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 14
% Syntax : Number of formulae : 87 ( 44 unt; 2 def)
% Number of atoms : 190 ( 105 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 160 ( 57 ~; 59 |; 37 &)
% ( 7 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 10 ( 10 usr; 6 con; 0-2 aty)
% Number of variables : 60 ( 57 !; 3 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] :
( bool(X)
<=> ( X = true
| X = false ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f3,axiom,
( d(err)
& d(false)
& d(true) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
! [X,Y] :
( forallprefers(X,Y)
<=> ( ( Y = true
& X = false )
| ( bool(Y)
& ~ bool(X)
& d(Y)
& d(X) )
| ( d(Y)
& ~ d(X) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X] :
( ( phi(X) = err
& ~ d(X) )
| ( phi(X) = X
& d(X) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X] :
( prop(X) = true
<=> bool(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X] :
( prop(X) = false
<=> ~ bool(X) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [B] : lazy_impl(false,B) = true,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [B] : lazy_impl(true,B) = phi(B),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f38,axiom,
false1 = false,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [P] : f7(P) = lazy_impl(prop(P),P),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f40,axiom,
? [P] :
( ~ ? [P1] : forallprefers(f7(P1),f7(P))
& false2 = phi(f7(P)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,conjecture,
false1 = false2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f46,negated_conjecture,
false1 != false2,
inference(negated_conjecture,[status(cth)],[f45]) ).
fof(f47,plain,
! [X] :
( ( ( X != true
& X != false )
| bool(X) )
& ( X = true
| X = false
| ~ bool(X) ) ),
inference(NNF_transformation,[status(thm)],[f1]) ).
fof(f48,plain,
( ! [X] :
( ( X != true
& X != false )
| bool(X) )
& ! [X] :
( X = true
| X = false
| ~ bool(X) ) ),
inference(miniscoping,[status(thm)],[f47]) ).
fof(f49,plain,
! [X0] :
( X0 = true
| X0 = false
| ~ bool(X0) ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f50,plain,
! [X0] :
( X0 != false
| bool(X0) ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f51,plain,
! [X0] :
( X0 != true
| bool(X0) ),
inference(cnf_transformation,[status(thm)],[f48]) ).
fof(f55,plain,
d(true),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f56,plain,
d(false),
inference(cnf_transformation,[status(thm)],[f3]) ).
fof(f58,definition,
! [X,Y] :
( sP0_prd(Y,X)
<=> ( ( bool(Y)
& ~ bool(X)
& d(Y)
& d(X) )
| ( d(Y)
& ~ d(X) ) ) ),
introduced(definition,[new_symbols(definition,[sP0_prd])],[]) ).
fof(f59,plain,
! [X,Y] :
( forallprefers(X,Y)
<=> ( ( Y = true
& X = false )
| sP0_prd(Y,X) ) ),
inference(formula_renaming,[status(thm)],[f4,f58]) ).
fof(f60,plain,
! [X,Y] :
( ( ( ( Y != true
| X != false )
& ~ sP0_prd(Y,X) )
| forallprefers(X,Y) )
& ( ( Y = true
& X = false )
| sP0_prd(Y,X)
| ~ forallprefers(X,Y) ) ),
inference(NNF_transformation,[status(thm)],[f59]) ).
fof(f61,plain,
( ! [X,Y] :
( ( ( Y != true
| X != false )
& ~ sP0_prd(Y,X) )
| forallprefers(X,Y) )
& ! [X,Y] :
( ( Y = true
& X = false )
| sP0_prd(Y,X)
| ~ forallprefers(X,Y) ) ),
inference(miniscoping,[status(thm)],[f60]) ).
fof(f65,plain,
! [X0,X1] :
( X1 != true
| X0 != false
| forallprefers(X0,X1) ),
inference(cnf_transformation,[status(thm)],[f61]) ).
fof(f74,definition,
! [X] :
( sP2_prd(X)
<=> ( phi(X) = X
& d(X) ) ),
introduced(definition,[new_symbols(definition,[sP2_prd])],[]) ).
fof(f75,plain,
! [X] :
( ( phi(X) = err
& ~ d(X) )
| sP2_prd(X) ),
inference(formula_renaming,[status(thm)],[f6,f74]) ).
fof(f76,plain,
! [X0] :
( ~ d(X0)
| sP2_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f75]) ).
fof(f78,plain,
! [X] :
( ( ~ bool(X)
| prop(X) = true )
& ( bool(X)
| prop(X) != true ) ),
inference(NNF_transformation,[status(thm)],[f7]) ).
fof(f79,plain,
( ! [X] :
( ~ bool(X)
| prop(X) = true )
& ! [X] :
( bool(X)
| prop(X) != true ) ),
inference(miniscoping,[status(thm)],[f78]) ).
fof(f80,plain,
! [X0] :
( bool(X0)
| prop(X0) != true ),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f81,plain,
! [X0] :
( ~ bool(X0)
| prop(X0) = true ),
inference(cnf_transformation,[status(thm)],[f79]) ).
fof(f82,plain,
! [X] :
( ( bool(X)
| prop(X) = false )
& ( ~ bool(X)
| prop(X) != false ) ),
inference(NNF_transformation,[status(thm)],[f8]) ).
fof(f83,plain,
( ! [X] :
( bool(X)
| prop(X) = false )
& ! [X] :
( ~ bool(X)
| prop(X) != false ) ),
inference(miniscoping,[status(thm)],[f82]) ).
fof(f85,plain,
! [X0] :
( bool(X0)
| prop(X0) = false ),
inference(cnf_transformation,[status(thm)],[f83]) ).
fof(f98,plain,
! [X0] : lazy_impl(false,X0) = true,
inference(cnf_transformation,[status(thm)],[f14]) ).
fof(f99,plain,
! [X0] : lazy_impl(true,X0) = phi(X0),
inference(cnf_transformation,[status(thm)],[f15]) ).
fof(f152,plain,
false1 = false,
inference(cnf_transformation,[status(thm)],[f38]) ).
fof(f153,plain,
! [X0] : f7(X0) = lazy_impl(prop(X0),X0),
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f154,plain,
? [P] :
( ! [P1] : ~ forallprefers(f7(P1),f7(P))
& false2 = phi(f7(P)) ),
inference(pre_NNF_transformation,[status(thm)],[f40]) ).
fof(f155,plain,
( ! [P1] : ~ forallprefers(f7(P1),f7(sK6_skl))
& false2 = phi(f7(sK6_skl)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl]),skolemize(P,sK6_skl)],[f154]) ).
fof(f156,plain,
false2 = phi(f7(sK6_skl)),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f157,plain,
! [X0] : ~ forallprefers(f7(X0),f7(sK6_skl)),
inference(cnf_transformation,[status(thm)],[f155]) ).
fof(f163,plain,
false1 != false2,
inference(cnf_transformation,[status(thm)],[f46]) ).
fof(f184,plain,
! [X] :
( ( phi(X) != X
| ~ d(X)
| sP2_prd(X) )
& ( ( phi(X) = X
& d(X) )
| ~ sP2_prd(X) ) ),
inference(NNF_transformation,[status(thm)],[f74]) ).
fof(f185,plain,
( ! [X] :
( phi(X) != X
| ~ d(X)
| sP2_prd(X) )
& ! [X] :
( ( phi(X) = X
& d(X) )
| ~ sP2_prd(X) ) ),
inference(miniscoping,[status(thm)],[f184]) ).
fof(f187,plain,
! [X0] :
( phi(X0) = X0
| ~ sP2_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f185]) ).
fof(f199,plain,
bool(false),
inference(destructive_equality_resolution,[status(thm)],[f50]) ).
fof(f200,plain,
bool(true),
inference(destructive_equality_resolution,[status(thm)],[f51]) ).
fof(f201,plain,
forallprefers(false,true),
inference(destructive_equality_resolution,[status(thm)],[f65]) ).
fof(f203,plain,
! [X0] :
( X0 = true
| X0 = false1
| ~ bool(X0) ),
inference(forward_demodulation,[status(thm)],[f152,f49]) ).
fof(f204,plain,
bool(false1),
inference(forward_demodulation,[status(thm)],[f152,f199]) ).
fof(f209,plain,
d(false1),
inference(forward_demodulation,[status(thm)],[f152,f56]) ).
fof(f210,plain,
forallprefers(false1,true),
inference(forward_demodulation,[status(thm)],[f152,f201]) ).
fof(f215,plain,
! [X0] : lazy_impl(false1,X0) = true,
inference(forward_demodulation,[status(thm)],[f152,f98]) ).
fof(f218,plain,
! [X0] :
( ~ d(X0)
| phi(X0) = X0 ),
inference(resolution,[status(thm)],[f187,f76]) ).
fof(f221,plain,
phi(false1) = false1,
inference(resolution,[status(thm)],[f218,f209]) ).
fof(f222,plain,
phi(true) = true,
inference(resolution,[status(thm)],[f218,f55]) ).
fof(f227,plain,
! [X0] :
( X0 = true
| X0 = false1
| prop(X0) != true ),
inference(resolution,[status(thm)],[f80,f203]) ).
fof(f228,plain,
prop(true) = true,
inference(resolution,[status(thm)],[f81,f200]) ).
fof(f229,plain,
prop(false1) = true,
inference(resolution,[status(thm)],[f81,f204]) ).
fof(f251,plain,
! [X0] :
( bool(X0)
| prop(X0) = false1 ),
inference(forward_demodulation,[status(thm)],[f152,f85]) ).
fof(f253,plain,
! [X0] :
( prop(X0) = true
| prop(X0) = false1 ),
inference(resolution,[status(thm)],[f251,f81]) ).
fof(f438,plain,
f7(true) = lazy_impl(true,true),
inference(paramodulation,[status(thm)],[f228,f153]) ).
fof(f439,plain,
f7(false1) = lazy_impl(true,false1),
inference(paramodulation,[status(thm)],[f229,f153]) ).
fof(f443,plain,
! [X0] :
( prop(X0) = true
| f7(X0) = lazy_impl(false1,X0) ),
inference(paramodulation,[status(thm)],[f253,f153]) ).
fof(f444,plain,
f7(true) = phi(true),
inference(forward_demodulation,[status(thm)],[f99,f438]) ).
fof(f445,plain,
f7(true) = true,
inference(forward_demodulation,[status(thm)],[f222,f444]) ).
fof(f446,plain,
f7(false1) = phi(false1),
inference(forward_demodulation,[status(thm)],[f99,f439]) ).
fof(f447,plain,
f7(false1) = false1,
inference(forward_demodulation,[status(thm)],[f221,f446]) ).
fof(f451,plain,
! [X0] :
( prop(X0) = true
| f7(X0) = true ),
inference(forward_demodulation,[status(thm)],[f215,f443]) ).
fof(f563,plain,
~ forallprefers(false1,f7(sK6_skl)),
inference(paramodulation,[status(thm)],[f447,f157]) ).
fof(f568,plain,
( prop(sK6_skl) = true
| ~ forallprefers(false1,true) ),
inference(paramodulation,[status(thm)],[f451,f563]) ).
fof(f569,plain,
prop(sK6_skl) = true,
inference(forward_subsumption_resolution,[status(thm)],[f568,f210]) ).
fof(f573,plain,
( sK6_skl = true
| sK6_skl = false1 ),
inference(resolution,[status(thm)],[f569,f227]) ).
fof(f579,plain,
f7(sK6_skl) = lazy_impl(true,sK6_skl),
inference(paramodulation,[status(thm)],[f569,f153]) ).
fof(f591,plain,
f7(sK6_skl) = phi(sK6_skl),
inference(forward_demodulation,[status(thm)],[f99,f579]) ).
fof(f606,plain,
( sK6_skl = false1
| f7(sK6_skl) = true ),
inference(paramodulation,[status(thm)],[f573,f445]) ).
fof(f790,plain,
( sK6_skl = false1
| ~ forallprefers(false1,true) ),
inference(paramodulation,[status(thm)],[f606,f563]) ).
fof(f795,plain,
sK6_skl = false1,
inference(forward_subsumption_resolution,[status(thm)],[f790,f210]) ).
fof(f814,plain,
f7(false1) = sK6_skl,
inference(backward_demodulation,[status(thm)],[f795,f447]) ).
fof(f858,plain,
sK6_skl != false2,
inference(backward_demodulation,[status(thm)],[f795,f163]) ).
fof(f862,plain,
f7(sK6_skl) = sK6_skl,
inference(forward_demodulation,[status(thm)],[f795,f814]) ).
fof(f900,plain,
sK6_skl = phi(sK6_skl),
inference(backward_demodulation,[status(thm)],[f862,f591]) ).
fof(f903,plain,
false2 = phi(sK6_skl),
inference(backward_demodulation,[status(thm)],[f862,f156]) ).
fof(f985,plain,
false2 = sK6_skl,
inference(forward_demodulation,[status(thm)],[f900,f903]) ).
fof(f986,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f985,f858]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW101+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.38 % Computer : n014.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 21 09:39:19 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.39 % Drodi V4.1.1
% 0.11/0.43 % Refutation found
% 0.11/0.43 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.11/0.43 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.11/0.48 % Elapsed time: 0.089961 seconds
% 0.11/0.48 % CPU time: 0.280370 seconds
% 0.11/0.48 % Total memory used: 106.743 MB
% 0.11/0.48 % Net memory used: 106.542 MB
%------------------------------------------------------------------------------