%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW190+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 : n003.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:24 PM UTC 2026
% Result : Theorem 3.60s 1.31s
% Output : CNFRefutation 4.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 21
% Syntax : Number of formulae : 87 ( 26 unt; 8 def)
% Number of atoms : 210 ( 18 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 230 ( 107 ~; 84 |; 19 &)
% ( 13 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 16 ( 14 usr; 9 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 6 con; 0-3 aty)
% Number of variables : 126 ( 118 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f9,axiom,
! [V_Pa_2,T_a] : c_Set_OCollect(T_a,V_Pa_2) = V_Pa_2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f10,axiom,
? [B_x] : c_member(tc_RealDef_Oreal,B_x,c_Set_OCollect(tc_RealDef_Oreal,v_P)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f18,axiom,
! [V_xa_2,T_a] : c_member(T_a,V_xa_2,c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_HOL_Obool))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f22,axiom,
! [V_A_2,V_xa_2,T_a] :
( c_member(T_a,V_xa_2,V_A_2)
<=> hBOOL(hAPP(V_A_2,V_xa_2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f49,axiom,
! [V_R_2,V_xa_2,V_S_2,T_a] :
( class_Orderings_Oord(T_a)
=> ( c_Lubs_Osetle(T_a,V_S_2,V_xa_2)
=> ( c_member(T_a,V_xa_2,V_R_2)
=> hBOOL(hAPP(c_Lubs_OisUb(T_a,V_R_2,V_S_2),V_xa_2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f62,axiom,
~ ( ? [B_x1] : hBOOL(hAPP(v_P,B_x1))
=> ! [B_Y] :
~ ! [B_x] :
( hBOOL(hAPP(v_P,B_x))
=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_x,B_Y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f116,axiom,
! [V_xa_2,V_S_2,T_a] :
( class_Orderings_Oord(T_a)
=> ( c_Lubs_Osetle(T_a,V_S_2,V_xa_2)
<=> ! [B_x] :
( c_member(T_a,B_x,V_S_2)
=> c_Orderings_Oord__class_Oless__eq(T_a,B_x,V_xa_2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f126,axiom,
! [V_y_2,V_xa_2] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_xa_2,V_y_2)
<=> ( V_xa_2 = V_y_2
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_xa_2,V_y_2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f127,axiom,
! [V_y_2,V_xa_2] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_xa_2,V_y_2)
<=> ( V_xa_2 != V_y_2
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_xa_2,V_y_2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f186,axiom,
! [T_a] : c_Orderings_Otop__class_Otop(tc_fun(T_a,tc_HOL_Obool)) != c_Orderings_Obot__class_Obot(tc_fun(T_a,tc_HOL_Obool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1117,axiom,
class_Orderings_Oord(tc_HOL_Obool),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1180,axiom,
class_Orderings_Oord(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1189,conjecture,
? [B_x1] : hBOOL(hAPP(c_Lubs_OisUb(tc_RealDef_Oreal,c_Orderings_Otop__class_Otop(tc_fun(tc_RealDef_Oreal,tc_HOL_Obool)),c_Set_OCollect(tc_RealDef_Oreal,v_P)),B_x1)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1190,negated_conjecture,
~ ? [B_x1] : hBOOL(hAPP(c_Lubs_OisUb(tc_RealDef_Oreal,c_Orderings_Otop__class_Otop(tc_fun(tc_RealDef_Oreal,tc_HOL_Obool)),c_Set_OCollect(tc_RealDef_Oreal,v_P)),B_x1)),
inference(negated_conjecture,[status(cth)],[f1189]) ).
fof(f1209,plain,
! [X0,X1] : c_Set_OCollect(X0,X1) = X1,
inference(cnf_transformation,[status(thm)],[f9]) ).
fof(f1210,plain,
c_member(tc_RealDef_Oreal,sK3_skl,c_Set_OCollect(tc_RealDef_Oreal,v_P)),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3_skl]),skolemize(B_x,sK3_skl)],[f10]) ).
fof(f1211,plain,
c_member(tc_RealDef_Oreal,sK3_skl,c_Set_OCollect(tc_RealDef_Oreal,v_P)),
inference(cnf_transformation,[status(thm)],[f1210]) ).
fof(f1233,plain,
! [X0,X1] : c_member(X0,X1,c_Orderings_Otop__class_Otop(tc_fun(X0,tc_HOL_Obool))),
inference(cnf_transformation,[status(thm)],[f18]) ).
fof(f1249,plain,
! [V_A_2,V_xa_2,T_a] :
( ( ~ hBOOL(hAPP(V_A_2,V_xa_2))
| c_member(T_a,V_xa_2,V_A_2) )
& ( hBOOL(hAPP(V_A_2,V_xa_2))
| ~ c_member(T_a,V_xa_2,V_A_2) ) ),
inference(NNF_transformation,[status(thm)],[f22]) ).
fof(f1250,plain,
( ! [V_A_2,V_xa_2] :
( ~ hBOOL(hAPP(V_A_2,V_xa_2))
| ! [T_a] : c_member(T_a,V_xa_2,V_A_2) )
& ! [V_A_2,V_xa_2] :
( hBOOL(hAPP(V_A_2,V_xa_2))
| ! [T_a] : ~ c_member(T_a,V_xa_2,V_A_2) ) ),
inference(miniscoping,[status(thm)],[f1249]) ).
fof(f1251,plain,
! [X0,X1,X2] :
( hBOOL(hAPP(X2,X1))
| ~ c_member(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f1250]) ).
fof(f1342,plain,
! [V_R_2,V_xa_2,V_S_2,T_a] :
( hBOOL(hAPP(c_Lubs_OisUb(T_a,V_R_2,V_S_2),V_xa_2))
| ~ c_member(T_a,V_xa_2,V_R_2)
| ~ c_Lubs_Osetle(T_a,V_S_2,V_xa_2)
| ~ class_Orderings_Oord(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f49]) ).
fof(f1343,plain,
! [T_a] :
( ! [V_xa_2,V_S_2] :
( ! [V_R_2] :
( hBOOL(hAPP(c_Lubs_OisUb(T_a,V_R_2,V_S_2),V_xa_2))
| ~ c_member(T_a,V_xa_2,V_R_2) )
| ~ c_Lubs_Osetle(T_a,V_S_2,V_xa_2) )
| ~ class_Orderings_Oord(T_a) ),
inference(miniscoping,[status(thm)],[f1342]) ).
fof(f1344,plain,
! [X0,X1,X2,X3] :
( hBOOL(hAPP(c_Lubs_OisUb(X0,X3,X1),X2))
| ~ c_member(X0,X2,X3)
| ~ c_Lubs_Osetle(X0,X1,X2)
| ~ class_Orderings_Oord(X0) ),
inference(cnf_transformation,[status(thm)],[f1343]) ).
fof(f1385,plain,
( ? [B_Y] :
! [B_x] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_x,B_Y)
| ~ hBOOL(hAPP(v_P,B_x)) )
& ? [B_x1] : hBOOL(hAPP(v_P,B_x1)) ),
inference(pre_NNF_transformation,[status(thm)],[f62]) ).
fof(f1386,plain,
( ! [B_x] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_x,sK8_skl)
| ~ hBOOL(hAPP(v_P,B_x)) )
& hBOOL(hAPP(v_P,sK7_skl)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7_skl,sK8_skl]),skolemize(B_x1,sK7_skl),skolemize(B_Y,sK8_skl)],[f1385]) ).
fof(f1388,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,sK8_skl)
| ~ hBOOL(hAPP(v_P,X0)) ),
inference(cnf_transformation,[status(thm)],[f1386]) ).
fof(f1572,plain,
! [V_xa_2,V_S_2,T_a] :
( ( c_Lubs_Osetle(T_a,V_S_2,V_xa_2)
<=> ! [B_x] :
( c_Orderings_Oord__class_Oless__eq(T_a,B_x,V_xa_2)
| ~ c_member(T_a,B_x,V_S_2) ) )
| ~ class_Orderings_Oord(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f116]) ).
fof(f1573,plain,
! [V_xa_2,V_S_2,T_a] :
( ( ( ? [B_x] :
( ~ c_Orderings_Oord__class_Oless__eq(T_a,B_x,V_xa_2)
& c_member(T_a,B_x,V_S_2) )
| c_Lubs_Osetle(T_a,V_S_2,V_xa_2) )
& ( ! [B_x] :
( c_Orderings_Oord__class_Oless__eq(T_a,B_x,V_xa_2)
| ~ c_member(T_a,B_x,V_S_2) )
| ~ c_Lubs_Osetle(T_a,V_S_2,V_xa_2) ) )
| ~ class_Orderings_Oord(T_a) ),
inference(NNF_transformation,[status(thm)],[f1572]) ).
fof(f1574,plain,
! [T_a] :
( ( ! [V_xa_2,V_S_2] :
( ? [B_x] :
( ~ c_Orderings_Oord__class_Oless__eq(T_a,B_x,V_xa_2)
& c_member(T_a,B_x,V_S_2) )
| c_Lubs_Osetle(T_a,V_S_2,V_xa_2) )
& ! [V_xa_2,V_S_2] :
( ! [B_x] :
( c_Orderings_Oord__class_Oless__eq(T_a,B_x,V_xa_2)
| ~ c_member(T_a,B_x,V_S_2) )
| ~ c_Lubs_Osetle(T_a,V_S_2,V_xa_2) ) )
| ~ class_Orderings_Oord(T_a) ),
inference(miniscoping,[status(thm)],[f1573]) ).
fof(f1575,plain,
! [T_a] :
( ( ! [V_xa_2,V_S_2] :
( ( ~ c_Orderings_Oord__class_Oless__eq(T_a,sK12_skl(V_S_2,V_xa_2,T_a),V_xa_2)
& c_member(T_a,sK12_skl(V_S_2,V_xa_2,T_a),V_S_2) )
| c_Lubs_Osetle(T_a,V_S_2,V_xa_2) )
& ! [V_xa_2,V_S_2] :
( ! [B_x] :
( c_Orderings_Oord__class_Oless__eq(T_a,B_x,V_xa_2)
| ~ c_member(T_a,B_x,V_S_2) )
| ~ c_Lubs_Osetle(T_a,V_S_2,V_xa_2) ) )
| ~ class_Orderings_Oord(T_a) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12_skl]),skolemize(B_x,sK12_skl(V_S_2,V_xa_2,T_a))],[f1574]) ).
fof(f1577,plain,
! [X0,X1,X2] :
( c_member(X0,sK12_skl(X1,X2,X0),X1)
| c_Lubs_Osetle(X0,X1,X2)
| ~ class_Orderings_Oord(X0) ),
inference(cnf_transformation,[status(thm)],[f1575]) ).
fof(f1578,plain,
! [X0,X1,X2] :
( ~ c_Orderings_Oord__class_Oless__eq(X0,sK12_skl(X1,X2,X0),X2)
| c_Lubs_Osetle(X0,X1,X2)
| ~ class_Orderings_Oord(X0) ),
inference(cnf_transformation,[status(thm)],[f1575]) ).
fof(f1615,plain,
! [V_y_2,V_xa_2] :
( ( ( V_xa_2 != V_y_2
& ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_xa_2,V_y_2) )
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_xa_2,V_y_2) )
& ( V_xa_2 = V_y_2
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_xa_2,V_y_2)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_xa_2,V_y_2) ) ),
inference(NNF_transformation,[status(thm)],[f126]) ).
fof(f1616,plain,
( ! [V_y_2,V_xa_2] :
( ( V_xa_2 != V_y_2
& ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_xa_2,V_y_2) )
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_xa_2,V_y_2) )
& ! [V_y_2,V_xa_2] :
( V_xa_2 = V_y_2
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_xa_2,V_y_2)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_xa_2,V_y_2) ) ),
inference(miniscoping,[status(thm)],[f1615]) ).
fof(f1618,plain,
! [X0,X1] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1616]) ).
fof(f1620,plain,
! [V_y_2,V_xa_2] :
( ( V_xa_2 = V_y_2
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_xa_2,V_y_2)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_xa_2,V_y_2) )
& ( ( V_xa_2 != V_y_2
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_xa_2,V_y_2) )
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_xa_2,V_y_2) ) ),
inference(NNF_transformation,[status(thm)],[f127]) ).
fof(f1621,plain,
( ! [V_y_2,V_xa_2] :
( V_xa_2 = V_y_2
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_xa_2,V_y_2)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_xa_2,V_y_2) )
& ! [V_y_2,V_xa_2] :
( ( V_xa_2 != V_y_2
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_xa_2,V_y_2) )
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_xa_2,V_y_2) ) ),
inference(miniscoping,[status(thm)],[f1620]) ).
fof(f1623,plain,
! [X0,X1] :
( X0 != X1
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1621]) ).
fof(f1810,plain,
! [X0] : c_Orderings_Otop__class_Otop(tc_fun(X0,tc_HOL_Obool)) != c_Orderings_Obot__class_Obot(tc_fun(X0,tc_HOL_Obool)),
inference(cnf_transformation,[status(thm)],[f186]) ).
fof(f4370,plain,
class_Orderings_Oord(tc_HOL_Obool),
inference(cnf_transformation,[status(thm)],[f1117]) ).
fof(f4433,plain,
class_Orderings_Oord(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1180]) ).
fof(f4442,plain,
! [B_x1] : ~ hBOOL(hAPP(c_Lubs_OisUb(tc_RealDef_Oreal,c_Orderings_Otop__class_Otop(tc_fun(tc_RealDef_Oreal,tc_HOL_Obool)),c_Set_OCollect(tc_RealDef_Oreal,v_P)),B_x1)),
inference(pre_NNF_transformation,[status(thm)],[f1190]) ).
fof(f4443,plain,
! [X0] : ~ hBOOL(hAPP(c_Lubs_OisUb(tc_RealDef_Oreal,c_Orderings_Otop__class_Otop(tc_fun(tc_RealDef_Oreal,tc_HOL_Obool)),c_Set_OCollect(tc_RealDef_Oreal,v_P)),X0)),
inference(cnf_transformation,[status(thm)],[f4442]) ).
fof(f4498,plain,
! [X0] : ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f1623]) ).
fof(f4589,plain,
! [X0] : ~ hBOOL(hAPP(c_Lubs_OisUb(tc_RealDef_Oreal,c_Orderings_Otop__class_Otop(tc_fun(tc_RealDef_Oreal,tc_HOL_Obool)),v_P),X0)),
inference(backward_demodulation,[status(thm)],[f1209,f4443]) ).
fof(f4598,plain,
c_member(tc_RealDef_Oreal,sK3_skl,v_P),
inference(forward_demodulation,[status(thm)],[f1209,f1211]) ).
fof(f4654,definition,
( sQ1_spl
<=> class_Orderings_Oord(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f4656,plain,
( sQ1_spl
| ~ class_Orderings_Oord(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f4654]) ).
fof(f4708,plain,
( sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4656,f4433]) ).
fof(f4709,plain,
sQ1_spl,
inference(contradiction_clause,[status(thm)],[f4708]) ).
fof(f4774,plain,
! [X0] :
( ~ c_member(tc_RealDef_Oreal,X0,c_Orderings_Otop__class_Otop(tc_fun(tc_RealDef_Oreal,tc_HOL_Obool)))
| ~ c_Lubs_Osetle(tc_RealDef_Oreal,v_P,X0)
| ~ class_Orderings_Oord(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1344,f4589]) ).
fof(f4776,definition,
! [X0] :
( sQ9_spl
<=> ( ~ c_member(tc_RealDef_Oreal,X0,c_Orderings_Otop__class_Otop(tc_fun(tc_RealDef_Oreal,tc_HOL_Obool)))
| ~ c_Lubs_Osetle(tc_RealDef_Oreal,v_P,X0) ) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f4777,plain,
! [X0] :
( ~ sQ9_spl
| ~ c_member(tc_RealDef_Oreal,X0,c_Orderings_Otop__class_Otop(tc_fun(tc_RealDef_Oreal,tc_HOL_Obool)))
| ~ c_Lubs_Osetle(tc_RealDef_Oreal,v_P,X0) ),
inference(component_clause,[status(thm)],[f4776]) ).
fof(f4779,plain,
( sQ9_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f4774,f4654,f4776]) ).
fof(f4784,plain,
! [X0] :
( ~ sQ9_spl
| ~ c_Lubs_Osetle(tc_RealDef_Oreal,v_P,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f4777,f1233]) ).
fof(f4827,definition,
! [X0] :
( sQ16_spl
<=> X0 = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f4828,plain,
! [X0] :
( ~ sQ16_spl
| X0 = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(component_clause,[status(thm)],[f4827]) ).
fof(f4999,definition,
! [X0] :
( sQ37_spl
<=> ~ c_member(tc_RealDef_Oreal,X0,v_P) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f5000,plain,
! [X0] :
( ~ sQ37_spl
| ~ c_member(tc_RealDef_Oreal,X0,v_P) ),
inference(component_clause,[status(thm)],[f4999]) ).
fof(f5065,plain,
( ~ sQ37_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f4598,f5000]) ).
fof(f5067,plain,
~ sQ37_spl,
inference(contradiction_clause,[status(thm)],[f5065]) ).
fof(f5075,plain,
! [X0,X1] :
( ~ sQ16_spl
| X0 = X1 ),
inference(paramodulation,[status(thm)],[f4828,f4828]) ).
fof(f5118,plain,
( ~ sQ16_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1810,f5075]) ).
fof(f5119,plain,
~ sQ16_spl,
inference(contradiction_clause,[status(thm)],[f5118]) ).
fof(f5162,definition,
( sQ54_spl
<=> class_Orderings_Oord(tc_HOL_Obool) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f5164,plain,
( sQ54_spl
| ~ class_Orderings_Oord(tc_HOL_Obool) ),
inference(component_clause,[status(thm)],[f5162]) ).
fof(f5173,plain,
( sQ54_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5164,f4370]) ).
fof(f5174,plain,
sQ54_spl,
inference(contradiction_clause,[status(thm)],[f5173]) ).
fof(f5342,definition,
( sQ61_spl
<=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f5343,plain,
( ~ sQ61_spl
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
inference(component_clause,[status(thm)],[f5342]) ).
fof(f5361,plain,
( ~ sQ61_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5343,f4498]) ).
fof(f5362,plain,
~ sQ61_spl,
inference(contradiction_clause,[status(thm)],[f5361]) ).
fof(f6554,plain,
! [X0] :
( ~ sQ9_spl
| c_member(tc_RealDef_Oreal,sK12_skl(v_P,X0,tc_RealDef_Oreal),v_P)
| ~ class_Orderings_Oord(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1577,f4784]) ).
fof(f6556,definition,
! [X0] :
( sQ136_spl
<=> c_member(tc_RealDef_Oreal,sK12_skl(v_P,X0,tc_RealDef_Oreal),v_P) ),
introduced(definition,[new_symbols(definition,[sQ136_spl])],[split_symbol_definition]) ).
fof(f6557,plain,
! [X0] :
( ~ sQ136_spl
| c_member(tc_RealDef_Oreal,sK12_skl(v_P,X0,tc_RealDef_Oreal),v_P) ),
inference(component_clause,[status(thm)],[f6556]) ).
fof(f6559,plain,
( ~ sQ9_spl
| sQ136_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f6554,f4654,f6556,f4776]) ).
fof(f6561,plain,
! [X0] :
( ~ sQ9_spl
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sK12_skl(v_P,X0,tc_RealDef_Oreal),X0)
| ~ class_Orderings_Oord(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1578,f4784]) ).
fof(f6563,definition,
! [X0] :
( sQ137_spl
<=> ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sK12_skl(v_P,X0,tc_RealDef_Oreal),X0) ),
introduced(definition,[new_symbols(definition,[sQ137_spl])],[split_symbol_definition]) ).
fof(f6564,plain,
! [X0] :
( ~ sQ137_spl
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sK12_skl(v_P,X0,tc_RealDef_Oreal),X0) ),
inference(component_clause,[status(thm)],[f6563]) ).
fof(f6566,plain,
( ~ sQ9_spl
| sQ137_spl
| ~ sQ1_spl ),
inference(split_clause,[status(thm)],[f6561,f4654,f6563,f4776]) ).
fof(f6572,plain,
! [X0] :
( ~ sQ137_spl
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK12_skl(v_P,X0,tc_RealDef_Oreal),X0) ),
inference(resolution,[status(thm)],[f6564,f1618]) ).
fof(f7245,plain,
( ~ sQ137_spl
| ~ hBOOL(hAPP(v_P,sK12_skl(v_P,sK8_skl,tc_RealDef_Oreal))) ),
inference(resolution,[status(thm)],[f6572,f1388]) ).
fof(f8186,plain,
! [X0] :
( ~ sQ137_spl
| ~ c_member(X0,sK12_skl(v_P,sK8_skl,tc_RealDef_Oreal),v_P) ),
inference(resolution,[status(thm)],[f7245,f1251]) ).
fof(f8465,plain,
( ~ sQ136_spl
| ~ sQ137_spl
| $false ),
inference(resolution,[status(thm)],[f8186,f6557]) ).
fof(f8468,plain,
( ~ sQ136_spl
| ~ sQ137_spl ),
inference(contradiction_clause,[status(thm)],[f8465]) ).
fof(f8469,plain,
$false,
inference(sat_refutation,[status(thm)],[f4709,f4779,f5067,f5119,f5174,f5362,f6559,f6566,f8468]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW190+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n003.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 09:42:01 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.14/0.51 % Drodi V4.1.1
% 3.60/1.31 % Refutation found
% 3.60/1.31 % SZS status Theorem for theBenchmark: Theorem is valid
% 3.60/1.31 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 4.08/1.37 % Elapsed time: 0.987676 seconds
% 4.08/1.37 % CPU time: 6.453881 seconds
% 4.08/1.37 % Total memory used: 241.311 MB
% 4.08/1.37 % Net memory used: 237.638 MB
%------------------------------------------------------------------------------