%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : LCL457+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/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 : Thu Sep 24 01:07:47 PM UTC 2026
% Result : Theorem 95.53s 12.69s
% Output : CNFRefutation 52.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 22
% Syntax : Number of formulae : 107 ( 50 unt; 0 def)
% Number of atoms : 216 ( 20 equ)
% Maximal formula atoms : 8 ( 2 avg)
% Number of connectives : 192 ( 83 ~; 74 |; 22 &)
% ( 8 <=>; 5 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 14 ( 12 usr; 12 prp; 0-2 aty)
% Number of functors : 21 ( 21 usr; 17 con; 0-2 aty)
% Number of variables : 198 ( 179 !; 19 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
( modus_ponens
<=> ! [X,Y] :
( ( is_a_theorem(implies(X,Y))
& is_a_theorem(X) )
=> is_a_theorem(Y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f4,axiom,
( implies_1
<=> ! [X,Y] : is_a_theorem(implies(X,implies(Y,X))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f6,axiom,
( implies_3
<=> ! [X,Y,Z] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f10,axiom,
( or_1
<=> ! [X,Y] : is_a_theorem(implies(X,or(X,Y))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f11,axiom,
( or_2
<=> ! [X,Y] : is_a_theorem(implies(Y,or(X,Y))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
( or_3
<=> ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f25,axiom,
( r4
<=> ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R)))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f27,axiom,
( op_or
=> ! [X,Y] : or(X,Y) = not(and(not(X),not(Y))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f28,axiom,
( op_and
=> ! [X,Y] : and(X,Y) = not(or(not(X),not(Y))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f29,axiom,
( op_implies_and
=> ! [X,Y] : implies(X,Y) = not(and(X,not(Y))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f30,axiom,
( op_implies_or
=> ! [X,Y] : implies(X,Y) = or(not(X),Y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f32,axiom,
op_or,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
op_implies_and,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f35,axiom,
modus_ponens,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
implies_1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f39,axiom,
implies_3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,axiom,
or_1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f44,axiom,
or_2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f45,axiom,
or_3,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f50,axiom,
op_implies_or,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f51,axiom,
op_and,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f53,conjecture,
r4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f54,negated_conjecture,
~ r4,
inference(negated_conjecture,[status(cth)],[f53]) ).
fof(f55,plain,
( modus_ponens
<=> ! [X,Y] :
( is_a_theorem(Y)
| ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X) ) ),
inference(pre_NNF_transformation,[status(thm)],[f1]) ).
fof(f56,plain,
( ( ? [X,Y] :
( ~ is_a_theorem(Y)
& is_a_theorem(implies(X,Y))
& is_a_theorem(X) )
| modus_ponens )
& ( ! [X,Y] :
( is_a_theorem(Y)
| ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X) )
| ~ modus_ponens ) ),
inference(NNF_transformation,[status(thm)],[f55]) ).
fof(f57,plain,
( ( ? [Y] :
( ~ is_a_theorem(Y)
& ? [X] :
( is_a_theorem(implies(X,Y))
& is_a_theorem(X) ) )
| modus_ponens )
& ( ! [Y] :
( is_a_theorem(Y)
| ! [X] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X) ) )
| ~ modus_ponens ) ),
inference(miniscoping,[status(thm)],[f56]) ).
fof(f58,plain,
( ( ( ~ is_a_theorem(sK0_skl)
& is_a_theorem(implies(sK1_skl,sK0_skl))
& is_a_theorem(sK1_skl) )
| modus_ponens )
& ( ! [Y] :
( is_a_theorem(Y)
| ! [X] :
( ~ is_a_theorem(implies(X,Y))
| ~ is_a_theorem(X) ) )
| ~ modus_ponens ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0_skl,sK1_skl]),skolemize(Y,sK0_skl),skolemize(X,sK1_skl)],[f57]) ).
fof(f59,plain,
! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0)
| ~ modus_ponens ),
inference(cnf_transformation,[status(thm)],[f58]) ).
fof(f73,plain,
( ( ? [X,Y] : ~ is_a_theorem(implies(X,implies(Y,X)))
| implies_1 )
& ( ! [X,Y] : is_a_theorem(implies(X,implies(Y,X)))
| ~ implies_1 ) ),
inference(NNF_transformation,[status(thm)],[f4]) ).
fof(f74,plain,
( ( ~ is_a_theorem(implies(sK6_skl,implies(sK7_skl,sK6_skl)))
| implies_1 )
& ( ! [X,Y] : is_a_theorem(implies(X,implies(Y,X)))
| ~ implies_1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6_skl,sK7_skl]),skolemize(X,sK6_skl),skolemize(Y,sK7_skl)],[f73]) ).
fof(f75,plain,
! [X0,X1] :
( is_a_theorem(implies(X0,implies(X1,X0)))
| ~ implies_1 ),
inference(cnf_transformation,[status(thm)],[f74]) ).
fof(f81,plain,
( ( ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z))))
| implies_3 )
& ( ! [X,Y,Z] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z))))
| ~ implies_3 ) ),
inference(NNF_transformation,[status(thm)],[f6]) ).
fof(f82,plain,
( ( ~ is_a_theorem(implies(implies(sK10_skl,sK11_skl),implies(implies(sK11_skl,sK12_skl),implies(sK10_skl,sK12_skl))))
| implies_3 )
& ( ! [X,Y,Z] : is_a_theorem(implies(implies(X,Y),implies(implies(Y,Z),implies(X,Z))))
| ~ implies_3 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl,sK11_skl,sK12_skl]),skolemize(X,sK10_skl),skolemize(Y,sK11_skl),skolemize(Z,sK12_skl)],[f81]) ).
fof(f83,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2))))
| ~ implies_3 ),
inference(cnf_transformation,[status(thm)],[f82]) ).
fof(f97,plain,
( ( ? [X,Y] : ~ is_a_theorem(implies(X,or(X,Y)))
| or_1 )
& ( ! [X,Y] : is_a_theorem(implies(X,or(X,Y)))
| ~ or_1 ) ),
inference(NNF_transformation,[status(thm)],[f10]) ).
fof(f98,plain,
( ( ~ is_a_theorem(implies(sK19_skl,or(sK19_skl,sK20_skl)))
| or_1 )
& ( ! [X,Y] : is_a_theorem(implies(X,or(X,Y)))
| ~ or_1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19_skl,sK20_skl]),skolemize(X,sK19_skl),skolemize(Y,sK20_skl)],[f97]) ).
fof(f99,plain,
! [X0,X1] :
( is_a_theorem(implies(X0,or(X0,X1)))
| ~ or_1 ),
inference(cnf_transformation,[status(thm)],[f98]) ).
fof(f101,plain,
( ( ? [X,Y] : ~ is_a_theorem(implies(Y,or(X,Y)))
| or_2 )
& ( ! [X,Y] : is_a_theorem(implies(Y,or(X,Y)))
| ~ or_2 ) ),
inference(NNF_transformation,[status(thm)],[f11]) ).
fof(f102,plain,
( ( ~ is_a_theorem(implies(sK22_skl,or(sK21_skl,sK22_skl)))
| or_2 )
& ( ! [X,Y] : is_a_theorem(implies(Y,or(X,Y)))
| ~ or_2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21_skl,sK22_skl]),skolemize(X,sK21_skl),skolemize(Y,sK22_skl)],[f101]) ).
fof(f103,plain,
! [X0,X1] :
( is_a_theorem(implies(X0,or(X1,X0)))
| ~ or_2 ),
inference(cnf_transformation,[status(thm)],[f102]) ).
fof(f105,plain,
( ( ? [X,Y,Z] : ~ is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z))))
| or_3 )
& ( ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z))))
| ~ or_3 ) ),
inference(NNF_transformation,[status(thm)],[f12]) ).
fof(f106,plain,
( ( ~ is_a_theorem(implies(implies(sK23_skl,sK25_skl),implies(implies(sK24_skl,sK25_skl),implies(or(sK23_skl,sK24_skl),sK25_skl))))
| or_3 )
& ( ! [X,Y,Z] : is_a_theorem(implies(implies(X,Z),implies(implies(Y,Z),implies(or(X,Y),Z))))
| ~ or_3 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23_skl,sK24_skl,sK25_skl]),skolemize(X,sK23_skl),skolemize(Y,sK24_skl),skolemize(Z,sK25_skl)],[f105]) ).
fof(f107,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(implies(X0,X1),implies(implies(X2,X1),implies(or(X0,X2),X1))))
| ~ or_3 ),
inference(cnf_transformation,[status(thm)],[f106]) ).
fof(f157,plain,
( ( ? [P,Q,R] : ~ is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R))))
| r4 )
& ( ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R))))
| ~ r4 ) ),
inference(NNF_transformation,[status(thm)],[f25]) ).
fof(f158,plain,
( ( ~ is_a_theorem(implies(or(sK49_skl,or(sK50_skl,sK51_skl)),or(sK50_skl,or(sK49_skl,sK51_skl))))
| r4 )
& ( ! [P,Q,R] : is_a_theorem(implies(or(P,or(Q,R)),or(Q,or(P,R))))
| ~ r4 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK49_skl,sK50_skl,sK51_skl]),skolemize(P,sK49_skl),skolemize(Q,sK50_skl),skolemize(R,sK51_skl)],[f157]) ).
fof(f160,plain,
( ~ is_a_theorem(implies(or(sK49_skl,or(sK50_skl,sK51_skl)),or(sK50_skl,or(sK49_skl,sK51_skl))))
| r4 ),
inference(cnf_transformation,[status(thm)],[f158]) ).
fof(f165,plain,
( ! [X,Y] : or(X,Y) = not(and(not(X),not(Y)))
| ~ op_or ),
inference(pre_NNF_transformation,[status(thm)],[f27]) ).
fof(f166,plain,
! [X0,X1] :
( or(X0,X1) = not(and(not(X0),not(X1)))
| ~ op_or ),
inference(cnf_transformation,[status(thm)],[f165]) ).
fof(f167,plain,
( ! [X,Y] : and(X,Y) = not(or(not(X),not(Y)))
| ~ op_and ),
inference(pre_NNF_transformation,[status(thm)],[f28]) ).
fof(f168,plain,
! [X0,X1] :
( and(X0,X1) = not(or(not(X0),not(X1)))
| ~ op_and ),
inference(cnf_transformation,[status(thm)],[f167]) ).
fof(f169,plain,
( ! [X,Y] : implies(X,Y) = not(and(X,not(Y)))
| ~ op_implies_and ),
inference(pre_NNF_transformation,[status(thm)],[f29]) ).
fof(f170,plain,
! [X0,X1] :
( implies(X0,X1) = not(and(X0,not(X1)))
| ~ op_implies_and ),
inference(cnf_transformation,[status(thm)],[f169]) ).
fof(f171,plain,
( ! [X,Y] : implies(X,Y) = or(not(X),Y)
| ~ op_implies_or ),
inference(pre_NNF_transformation,[status(thm)],[f30]) ).
fof(f172,plain,
! [X0,X1] :
( implies(X0,X1) = or(not(X0),X1)
| ~ op_implies_or ),
inference(cnf_transformation,[status(thm)],[f171]) ).
fof(f175,plain,
op_or,
inference(cnf_transformation,[status(thm)],[f32]) ).
fof(f176,plain,
op_implies_and,
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f178,plain,
modus_ponens,
inference(cnf_transformation,[status(thm)],[f35]) ).
fof(f180,plain,
implies_1,
inference(cnf_transformation,[status(thm)],[f37]) ).
fof(f182,plain,
implies_3,
inference(cnf_transformation,[status(thm)],[f39]) ).
fof(f186,plain,
or_1,
inference(cnf_transformation,[status(thm)],[f43]) ).
fof(f187,plain,
or_2,
inference(cnf_transformation,[status(thm)],[f44]) ).
fof(f188,plain,
or_3,
inference(cnf_transformation,[status(thm)],[f45]) ).
fof(f193,plain,
op_implies_or,
inference(cnf_transformation,[status(thm)],[f50]) ).
fof(f194,plain,
op_and,
inference(cnf_transformation,[status(thm)],[f51]) ).
fof(f196,plain,
~ r4,
inference(cnf_transformation,[status(thm)],[f54]) ).
fof(f197,plain,
! [X0,X1] : or(X0,X1) = not(and(not(X0),not(X1))),
inference(backward_subsumption_resolution,[status(thm)],[f166,f175]) ).
fof(f198,plain,
! [X0,X1] : implies(X0,X1) = not(and(X0,not(X1))),
inference(backward_subsumption_resolution,[status(thm)],[f170,f176]) ).
fof(f200,plain,
! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(implies(X0,X1))
| ~ is_a_theorem(X0) ),
inference(backward_subsumption_resolution,[status(thm)],[f59,f178]) ).
fof(f202,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(X1,X0))),
inference(backward_subsumption_resolution,[status(thm)],[f75,f180]) ).
fof(f204,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(implies(X1,X2),implies(X0,X2)))),
inference(backward_subsumption_resolution,[status(thm)],[f83,f182]) ).
fof(f208,plain,
! [X0,X1] : is_a_theorem(implies(X0,or(X0,X1))),
inference(backward_subsumption_resolution,[status(thm)],[f99,f186]) ).
fof(f209,plain,
! [X0,X1] : is_a_theorem(implies(X0,or(X1,X0))),
inference(backward_subsumption_resolution,[status(thm)],[f103,f187]) ).
fof(f210,plain,
! [X0,X1,X2] : is_a_theorem(implies(implies(X0,X1),implies(implies(X2,X1),implies(or(X0,X2),X1)))),
inference(backward_subsumption_resolution,[status(thm)],[f107,f188]) ).
fof(f215,plain,
! [X0,X1] : implies(X0,X1) = or(not(X0),X1),
inference(backward_subsumption_resolution,[status(thm)],[f172,f193]) ).
fof(f216,plain,
! [X0,X1] : and(X0,X1) = not(or(not(X0),not(X1))),
inference(backward_subsumption_resolution,[status(thm)],[f168,f194]) ).
fof(f217,plain,
~ is_a_theorem(implies(or(sK49_skl,or(sK50_skl,sK51_skl)),or(sK50_skl,or(sK49_skl,sK51_skl)))),
inference(backward_subsumption_resolution,[status(thm)],[f160,f196]) ).
fof(f218,plain,
! [X0,X1] : or(X0,X1) = implies(not(X0),X1),
inference(backward_demodulation,[status(thm)],[f198,f197]) ).
fof(f222,plain,
! [X0,X1] : and(X0,X1) = not(implies(X0,not(X1))),
inference(forward_demodulation,[status(thm)],[f215,f216]) ).
fof(f232,plain,
! [X0,X1] : is_a_theorem(implies(not(X0),implies(X0,X1))),
inference(paramodulation,[status(thm)],[f215,f208]) ).
fof(f233,plain,
! [X0,X1] : is_a_theorem(or(X0,implies(X0,X1))),
inference(forward_demodulation,[status(thm)],[f218,f232]) ).
fof(f238,plain,
! [X0,X1] : is_a_theorem(or(X0,implies(X1,not(X0)))),
inference(paramodulation,[status(thm)],[f218,f202]) ).
fof(f245,plain,
! [X0,X1] : is_a_theorem(implies(X0,implies(X1,not(not(X0))))),
inference(paramodulation,[status(thm)],[f215,f238]) ).
fof(f257,plain,
! [X0,X1] :
( is_a_theorem(X1)
| ~ is_a_theorem(or(X0,X1))
| ~ is_a_theorem(not(X0)) ),
inference(paramodulation,[status(thm)],[f218,f200]) ).
fof(f314,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(implies(X1,X2),implies(X0,X2)))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f204,f200]) ).
fof(f376,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(X0,X2))
| ~ is_a_theorem(implies(X1,X2))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f314,f200]) ).
fof(f378,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(implies(X1,X2),or(X0,X2)))
| ~ is_a_theorem(implies(not(X0),X1)) ),
inference(paramodulation,[status(thm)],[f218,f314]) ).
fof(f379,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(implies(X1,X2),or(X0,X2)))
| ~ is_a_theorem(or(X0,X1)) ),
inference(forward_demodulation,[status(thm)],[f218,f378]) ).
fof(f423,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(implies(X2,X1),implies(or(X0,X2),X1)))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f210,f200]) ).
fof(f514,plain,
! [X0,X1,X2] : and(X0,and(X1,not(X2))) = not(implies(X0,implies(X1,X2))),
inference(paramodulation,[status(thm)],[f198,f222]) ).
fof(f518,plain,
! [X0,X1,X2] : implies(X0,implies(X1,not(X2))) = not(and(X0,and(X1,X2))),
inference(paramodulation,[status(thm)],[f222,f198]) ).
fof(f525,plain,
! [X0,X1] : is_a_theorem(not(and(X0,and(X1,not(X0))))),
inference(backward_demodulation,[status(thm)],[f518,f245]) ).
fof(f535,plain,
! [X0,X1] : is_a_theorem(not(not(implies(X0,implies(X1,X0))))),
inference(forward_demodulation,[status(thm)],[f514,f525]) ).
fof(f1048,plain,
! [X0,X1,X2] :
( is_a_theorem(X2)
| ~ is_a_theorem(or(not(implies(X0,implies(X1,X0))),X2)) ),
inference(resolution,[status(thm)],[f257,f535]) ).
fof(f1053,plain,
! [X0,X1,X2] :
( is_a_theorem(X2)
| ~ is_a_theorem(implies(implies(X0,implies(X1,X0)),X2)) ),
inference(forward_demodulation,[status(thm)],[f215,f1048]) ).
fof(f1453,plain,
! [X0,X1,X2] :
( is_a_theorem(implies(or(X0,X2),X1))
| ~ is_a_theorem(implies(X2,X1))
| ~ is_a_theorem(implies(X0,X1)) ),
inference(resolution,[status(thm)],[f423,f200]) ).
fof(f4983,plain,
( ~ is_a_theorem(implies(or(sK50_skl,sK51_skl),or(sK50_skl,or(sK49_skl,sK51_skl))))
| ~ is_a_theorem(implies(sK49_skl,or(sK50_skl,or(sK49_skl,sK51_skl)))) ),
inference(resolution,[status(thm)],[f1453,f217]) ).
fof(f8560,plain,
! [X0,X1,X2] :
( ~ is_a_theorem(or(X0,X2))
| is_a_theorem(or(X0,implies(X1,X2))) ),
inference(resolution,[status(thm)],[f1053,f379]) ).
fof(f10207,plain,
! [X0,X1,X2] :
( ~ is_a_theorem(or(X0,X2))
| is_a_theorem(or(X0,or(X1,X2))) ),
inference(paramodulation,[status(thm)],[f218,f8560]) ).
fof(f10651,plain,
! [X0,X1,X2] : is_a_theorem(or(X0,or(X1,implies(X0,X2)))),
inference(resolution,[status(thm)],[f10207,f233]) ).
fof(f10705,plain,
! [X0,X1,X2] : is_a_theorem(implies(X0,or(X1,implies(not(X0),X2)))),
inference(paramodulation,[status(thm)],[f215,f10651]) ).
fof(f10713,plain,
~ is_a_theorem(implies(or(sK50_skl,sK51_skl),or(sK50_skl,or(sK49_skl,sK51_skl)))),
inference(backward_subsumption_resolution,[status(thm)],[f4983,f10715]) ).
fof(f10715,plain,
! [X0,X1,X2] : is_a_theorem(implies(X0,or(X1,or(X0,X2)))),
inference(forward_demodulation,[status(thm)],[f218,f10705]) ).
fof(f10891,plain,
( ~ is_a_theorem(implies(sK51_skl,or(sK50_skl,or(sK49_skl,sK51_skl))))
| ~ is_a_theorem(implies(sK50_skl,or(sK50_skl,or(sK49_skl,sK51_skl)))) ),
inference(resolution,[status(thm)],[f10713,f1453]) ).
fof(f10896,plain,
~ is_a_theorem(implies(sK51_skl,or(sK50_skl,or(sK49_skl,sK51_skl)))),
inference(forward_subsumption_resolution,[status(thm)],[f10891,f208]) ).
fof(f10898,plain,
! [X0] :
( ~ is_a_theorem(implies(X0,or(sK50_skl,or(sK49_skl,sK51_skl))))
| ~ is_a_theorem(implies(sK51_skl,X0)) ),
inference(resolution,[status(thm)],[f10896,f376]) ).
fof(f10920,plain,
~ is_a_theorem(implies(sK51_skl,or(sK49_skl,sK51_skl))),
inference(resolution,[status(thm)],[f10898,f209]) ).
fof(f10927,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f10920,f209]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL457+1 : TPTP v9.3.1. Bugfixed v9.2.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.08/0.35 % Computer : n020.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 : Mon Sep 21 00:34:02 UTC 2026
% 0.08/0.35 % CPUTime :
% 0.08/0.36 % Drodi V4.1.1
% 95.53/12.69 % Refutation found
% 95.53/12.69 % SZS status Theorem for theBenchmark: Theorem is valid
% 95.53/12.69 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 9.30/12.94 % Elapsed time: 12.560255 seconds
% 9.30/12.94 % CPU time: 98.799749 seconds
% 9.30/12.94 % Total memory used: 1.117 GB
% 9.30/12.94 % Net memory used: 1.050 GB
%------------------------------------------------------------------------------