%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW102+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n019.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.13s 0.52s
% Output : CNFRefutation 0.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 22
% Syntax : Number of formulae : 142 ( 62 unt; 2 def)
% Number of atoms : 287 ( 189 equ)
% Maximal formula atoms : 9 ( 2 avg)
% Number of connectives : 219 ( 74 ~; 95 |; 39 &)
% ( 7 <=>; 4 =>; 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 : 14 ( 14 usr; 7 con; 0-2 aty)
% Number of variables : 91 ( 87 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X] :
( bool(X)
<=> ( X = true
| X = false ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f2,axiom,
( false != err
& true != err
& true != false ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f3,axiom,
( d(err)
& d(false)
& d(true) ),
file('/export/starexec/sandbox2/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/sandbox2/benchmark/theBenchmark.p') ).
fof(f6,axiom,
! [X] :
( ( phi(X) = err
& ~ d(X) )
| ( phi(X) = X
& d(X) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f7,axiom,
! [X] :
( prop(X) = true
<=> bool(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f8,axiom,
! [X] :
( prop(X) = false
<=> ~ bool(X) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f9,axiom,
! [A,B] :
( ~ bool(A)
=> impl(A,B) = phi(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f11,axiom,
! [B] :
( bool(B)
=> impl(false,B) = true ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [B] :
( bool(B)
=> impl(true,B) = B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f14,axiom,
! [B] : lazy_impl(false,B) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f15,axiom,
! [B] : lazy_impl(true,B) = phi(B),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f38,axiom,
false1 = false,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f39,axiom,
! [P] : f7(P) = lazy_impl(prop(P),P),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f40,axiom,
? [P] :
( ~ ? [P1] : forallprefers(f7(P1),f7(P))
& false2 = phi(f7(P)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f41,axiom,
! [A] :
( ~ bool(A)
=> not1(A) = phi(A) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f42,axiom,
not1(false) = true,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f43,axiom,
not1(true) = false,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f44,axiom,
! [P] : not2(P) = impl(P,false2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f45,conjecture,
! [P] : not1(P) = not2(P),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f46,negated_conjecture,
~ ! [P] : not1(P) = not2(P),
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(f52,plain,
true != false,
inference(cnf_transformation,[status(thm)],[f2]) ).
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(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(f86,plain,
! [A,B] :
( impl(A,B) = phi(A)
| bool(A) ),
inference(pre_NNF_transformation,[status(thm)],[f9]) ).
fof(f87,plain,
! [A] :
( ! [B] : impl(A,B) = phi(A)
| bool(A) ),
inference(miniscoping,[status(thm)],[f86]) ).
fof(f88,plain,
! [X0,X1] :
( impl(X0,X1) = phi(X0)
| bool(X0) ),
inference(cnf_transformation,[status(thm)],[f87]) ).
fof(f91,plain,
! [B] :
( impl(false,B) = true
| ~ bool(B) ),
inference(pre_NNF_transformation,[status(thm)],[f11]) ).
fof(f92,plain,
! [X0] :
( impl(false,X0) = true
| ~ bool(X0) ),
inference(cnf_transformation,[status(thm)],[f91]) ).
fof(f93,plain,
! [B] :
( impl(true,B) = B
| ~ bool(B) ),
inference(pre_NNF_transformation,[status(thm)],[f12]) ).
fof(f94,plain,
! [X0] :
( impl(true,X0) = X0
| ~ bool(X0) ),
inference(cnf_transformation,[status(thm)],[f93]) ).
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(f158,plain,
! [A] :
( not1(A) = phi(A)
| bool(A) ),
inference(pre_NNF_transformation,[status(thm)],[f41]) ).
fof(f159,plain,
! [X0] :
( not1(X0) = phi(X0)
| bool(X0) ),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f160,plain,
not1(false) = true,
inference(cnf_transformation,[status(thm)],[f42]) ).
fof(f161,plain,
not1(true) = false,
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f162,plain,
! [X0] : not2(X0) = impl(X0,false2),
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f163,plain,
? [P] : not1(P) != not2(P),
inference(pre_NNF_transformation,[status(thm)],[f46]) ).
fof(f164,plain,
not1(sK7_skl) != not2(sK7_skl),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl]),skolemize(P,sK7_skl)],[f163]) ).
fof(f165,plain,
not1(sK7_skl) != not2(sK7_skl),
inference(cnf_transformation,[status(thm)],[f164]) ).
fof(f186,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(f187,plain,
( ! [X] :
( phi(X) != X
| ~ d(X)
| sP2_prd(X) )
& ! [X] :
( ( phi(X) = X
& d(X) )
| ~ sP2_prd(X) ) ),
inference(miniscoping,[status(thm)],[f186]) ).
fof(f189,plain,
! [X0] :
( phi(X0) = X0
| ~ sP2_prd(X0) ),
inference(cnf_transformation,[status(thm)],[f187]) ).
fof(f201,plain,
bool(false),
inference(destructive_equality_resolution,[status(thm)],[f50]) ).
fof(f203,plain,
forallprefers(false,true),
inference(destructive_equality_resolution,[status(thm)],[f65]) ).
fof(f209,plain,
d(false1),
inference(backward_demodulation,[status(thm)],[f152,f56]) ).
fof(f211,plain,
true != false1,
inference(backward_demodulation,[status(thm)],[f152,f52]) ).
fof(f213,plain,
! [X0] :
( X0 = true
| X0 = false1
| ~ bool(X0) ),
inference(backward_demodulation,[status(thm)],[f152,f49]) ).
fof(f214,plain,
bool(false1),
inference(backward_demodulation,[status(thm)],[f152,f201]) ).
fof(f215,plain,
not1(true) = false1,
inference(backward_demodulation,[status(thm)],[f152,f161]) ).
fof(f216,plain,
not1(false1) = true,
inference(backward_demodulation,[status(thm)],[f152,f160]) ).
fof(f217,plain,
forallprefers(false1,true),
inference(forward_demodulation,[status(thm)],[f152,f203]) ).
fof(f221,plain,
! [X0] : lazy_impl(false1,X0) = true,
inference(forward_demodulation,[status(thm)],[f152,f98]) ).
fof(f227,plain,
! [X0] :
( ~ d(X0)
| phi(X0) = X0 ),
inference(resolution,[status(thm)],[f189,f76]) ).
fof(f228,plain,
phi(false1) = false1,
inference(resolution,[status(thm)],[f227,f209]) ).
fof(f234,plain,
prop(false1) = true,
inference(resolution,[status(thm)],[f81,f214]) ).
fof(f237,plain,
! [X0] :
( not1(X0) = phi(X0)
| prop(X0) = true ),
inference(resolution,[status(thm)],[f81,f159]) ).
fof(f269,plain,
! [X0] :
( bool(X0)
| prop(X0) = false1 ),
inference(forward_demodulation,[status(thm)],[f152,f85]) ).
fof(f271,plain,
! [X0] :
( prop(X0) = true
| prop(X0) = false1 ),
inference(resolution,[status(thm)],[f269,f81]) ).
fof(f273,plain,
! [X0,X1] :
( prop(X0) = true
| impl(X0,X1) = phi(X0) ),
inference(resolution,[status(thm)],[f88,f81]) ).
fof(f285,plain,
! [X0] :
( impl(false1,X0) = true
| ~ bool(X0) ),
inference(forward_demodulation,[status(thm)],[f152,f92]) ).
fof(f292,plain,
! [X0] :
( not1(X0) = phi(X0)
| impl(false1,X0) = true ),
inference(resolution,[status(thm)],[f285,f159]) ).
fof(f297,plain,
! [X0] :
( prop(X0) = false1
| impl(true,X0) = X0 ),
inference(resolution,[status(thm)],[f94,f269]) ).
fof(f488,plain,
f7(false1) = lazy_impl(true,false1),
inference(paramodulation,[status(thm)],[f234,f153]) ).
fof(f491,plain,
f7(false1) = phi(false1),
inference(forward_demodulation,[status(thm)],[f99,f488]) ).
fof(f492,plain,
f7(false1) = false1,
inference(forward_demodulation,[status(thm)],[f228,f491]) ).
fof(f493,plain,
~ forallprefers(false1,f7(sK6_skl)),
inference(paramodulation,[status(thm)],[f492,f157]) ).
fof(f585,plain,
! [X0] :
( prop(X0) = false1
| X0 = true
| X0 = false1 ),
inference(resolution,[status(thm)],[f213,f269]) ).
fof(f785,plain,
! [X0] :
( prop(X0) = true
| f7(X0) = lazy_impl(false1,X0) ),
inference(paramodulation,[status(thm)],[f271,f153]) ).
fof(f795,plain,
! [X0] :
( prop(X0) = true
| f7(X0) = true ),
inference(forward_demodulation,[status(thm)],[f221,f785]) ).
fof(f844,plain,
( prop(sK6_skl) = true
| ~ forallprefers(false1,true) ),
inference(paramodulation,[status(thm)],[f795,f493]) ).
fof(f852,plain,
prop(sK6_skl) = true,
inference(forward_subsumption_resolution,[status(thm)],[f844,f217]) ).
fof(f862,plain,
f7(sK6_skl) = lazy_impl(true,sK6_skl),
inference(paramodulation,[status(thm)],[f852,f153]) ).
fof(f869,plain,
f7(sK6_skl) = phi(sK6_skl),
inference(forward_demodulation,[status(thm)],[f99,f862]) ).
fof(f1242,plain,
( true = false1
| impl(true,sK6_skl) = sK6_skl ),
inference(paramodulation,[status(thm)],[f852,f297]) ).
fof(f1264,plain,
impl(true,sK6_skl) = sK6_skl,
inference(forward_subsumption_resolution,[status(thm)],[f1242,f211]) ).
fof(f1374,plain,
! [X0] :
( prop(X0) = true
| not2(X0) = phi(X0) ),
inference(paramodulation,[status(thm)],[f162,f273]) ).
fof(f1445,plain,
! [X0] :
( prop(X0) = true
| prop(X0) = true
| not2(X0) = not1(X0) ),
inference(paramodulation,[status(thm)],[f237,f1374]) ).
fof(f1468,plain,
! [X0] :
( prop(X0) = true
| not2(X0) = not1(X0) ),
inference(duplicate_literals_removal,[status(thm)],[f1445]) ).
fof(f1471,plain,
prop(sK7_skl) = true,
inference(resolution,[status(thm)],[f1468,f165]) ).
fof(f1845,plain,
( true = false1
| sK7_skl = true
| sK7_skl = false1 ),
inference(paramodulation,[status(thm)],[f1471,f585]) ).
fof(f1846,plain,
( true = false1
| sK6_skl = true
| sK6_skl = false1 ),
inference(paramodulation,[status(thm)],[f852,f585]) ).
fof(f1879,plain,
( sK7_skl = true
| sK7_skl = false1 ),
inference(forward_subsumption_resolution,[status(thm)],[f1845,f211]) ).
fof(f1880,plain,
( sK6_skl = true
| sK6_skl = false1 ),
inference(forward_subsumption_resolution,[status(thm)],[f1846,f211]) ).
fof(f1947,plain,
( sK7_skl = true
| not1(sK7_skl) = true ),
inference(paramodulation,[status(thm)],[f1879,f216]) ).
fof(f1998,plain,
( sK6_skl = false1
| forallprefers(false1,sK6_skl) ),
inference(paramodulation,[status(thm)],[f1880,f217]) ).
fof(f2001,plain,
( sK6_skl = false1
| d(sK6_skl) ),
inference(paramodulation,[status(thm)],[f1880,f55]) ).
fof(f2235,plain,
( phi(sK6_skl) = sK6_skl
| sK6_skl = false1 ),
inference(resolution,[status(thm)],[f2001,f227]) ).
fof(f2236,plain,
( f7(sK6_skl) = sK6_skl
| sK6_skl = false1 ),
inference(forward_demodulation,[status(thm)],[f869,f2235]) ).
fof(f2260,plain,
( sK7_skl = true
| true != not2(sK7_skl) ),
inference(paramodulation,[status(thm)],[f1947,f165]) ).
fof(f2525,plain,
( sK6_skl = false1
| ~ forallprefers(false1,sK6_skl) ),
inference(paramodulation,[status(thm)],[f2236,f493]) ).
fof(f2535,plain,
sK6_skl = false1,
inference(forward_subsumption_resolution,[status(thm)],[f2525,f1998]) ).
fof(f2555,plain,
( sK7_skl = true
| sK7_skl = sK6_skl ),
inference(backward_demodulation,[status(thm)],[f2535,f1879]) ).
fof(f2593,plain,
f7(false1) = sK6_skl,
inference(backward_demodulation,[status(thm)],[f2535,f492]) ).
fof(f2610,plain,
! [X0] :
( not1(X0) = phi(X0)
| impl(sK6_skl,X0) = true ),
inference(backward_demodulation,[status(thm)],[f2535,f292]) ).
fof(f2623,plain,
true != sK6_skl,
inference(backward_demodulation,[status(thm)],[f2535,f211]) ).
fof(f2627,plain,
not1(sK6_skl) = true,
inference(backward_demodulation,[status(thm)],[f2535,f216]) ).
fof(f2628,plain,
not1(true) = sK6_skl,
inference(backward_demodulation,[status(thm)],[f2535,f215]) ).
fof(f2640,plain,
f7(sK6_skl) = sK6_skl,
inference(forward_demodulation,[status(thm)],[f2535,f2593]) ).
fof(f2692,plain,
( sK7_skl = true
| sK7_skl = true
| true != not2(sK6_skl) ),
inference(paramodulation,[status(thm)],[f2555,f2260]) ).
fof(f2709,plain,
( sK7_skl = true
| true != not2(sK6_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f2692]) ).
fof(f2795,plain,
sK6_skl = phi(sK6_skl),
inference(backward_demodulation,[status(thm)],[f2640,f869]) ).
fof(f2802,plain,
false2 = phi(sK6_skl),
inference(backward_demodulation,[status(thm)],[f2640,f156]) ).
fof(f2952,plain,
! [X0] : not2(X0) = impl(X0,sK6_skl),
inference(backward_demodulation,[status(thm)],[f2953,f162]) ).
fof(f2953,plain,
false2 = sK6_skl,
inference(forward_demodulation,[status(thm)],[f2795,f2802]) ).
fof(f3044,plain,
not2(true) = sK6_skl,
inference(backward_demodulation,[status(thm)],[f2952,f1264]) ).
fof(f3045,plain,
( not1(sK6_skl) = phi(sK6_skl)
| not2(sK6_skl) = true ),
inference(paramodulation,[status(thm)],[f2610,f2952]) ).
fof(f3061,plain,
( true = phi(sK6_skl)
| not2(sK6_skl) = true ),
inference(forward_demodulation,[status(thm)],[f2627,f3045]) ).
fof(f3062,plain,
( true = sK6_skl
| not2(sK6_skl) = true ),
inference(forward_demodulation,[status(thm)],[f2795,f3061]) ).
fof(f3063,plain,
not2(sK6_skl) = true,
inference(forward_subsumption_resolution,[status(thm)],[f3062,f2623]) ).
fof(f3133,plain,
( sK7_skl = true
| true != true ),
inference(backward_demodulation,[status(thm)],[f3063,f2709]) ).
fof(f3134,plain,
sK7_skl = true,
inference(trivial_equality_resolution,[status(thm)],[f3133]) ).
fof(f3136,plain,
not2(sK7_skl) = sK6_skl,
inference(backward_demodulation,[status(thm)],[f3134,f3044]) ).
fof(f3151,plain,
not1(sK7_skl) = sK6_skl,
inference(backward_demodulation,[status(thm)],[f3134,f2628]) ).
fof(f3262,plain,
not1(sK7_skl) != sK6_skl,
inference(backward_demodulation,[status(thm)],[f3136,f165]) ).
fof(f3329,plain,
sK6_skl != sK6_skl,
inference(forward_demodulation,[status(thm)],[f3151,f3262]) ).
fof(f3330,plain,
$false,
inference(trivial_equality_resolution,[status(thm)],[f3329]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW102+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.07/0.33 % Computer : n019.cluster.edu
% 0.07/0.33 % Model : x86_64 x86_64
% 0.07/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.33 % Memory : 8046.5625MB
% 0.07/0.33 % OS : Linux 6.8.0-71-generic
% 0.07/0.34 % CPULimit : 300
% 0.07/0.34 % WCLimit : 300
% 0.07/0.34 % DateTime : Mon Sep 21 09:39:19 UTC 2026
% 0.07/0.34 % CPUTime :
% 0.07/0.35 % Drodi V4.1.1
% 0.13/0.52 % Refutation found
% 0.13/0.52 % SZS status Theorem for theBenchmark: Theorem is valid
% 0.13/0.52 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 0.74/0.54 % Elapsed time: 0.182317 seconds
% 0.74/0.54 % CPU time: 1.137859 seconds
% 0.74/0.54 % Total memory used: 130.230 MB
% 0.74/0.54 % Net memory used: 128.735 MB
%------------------------------------------------------------------------------