%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW212+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 : 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:26 PM UTC 2026
% Result : Theorem 10.81s 7.06s
% Output : CNFRefutation 10.81s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 12
% Syntax : Number of formulae : 50 ( 13 unt; 6 def)
% Number of atoms : 101 ( 2 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 87 ( 36 ~; 32 |; 6 &)
% ( 6 <=>; 7 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 7 ( 2 avg)
% Number of predicates : 13 ( 11 usr; 7 prp; 0-3 aty)
% Number of functors : 19 ( 19 usr; 10 con; 0-5 aty)
% Number of variables : 44 ( 34 !; 10 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f17,axiom,
c_SEQ_Osubseq(c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f94,axiom,
! [V_e_2] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),V_e_2)
=> ? [B_N] :
! [B_n] :
( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_N,B_n)
=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex),hAPP(v_s,hAPP(c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____),B_n))),hAPP(hAPP(c_Complex_Ocomplex_OComplex,v_x____),v_y____))),V_e_2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1053,axiom,
class_Rings_Olinordered__idom(tc_Int_Oint),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1156,axiom,
class_Rings_Olinordered__idom(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1264,axiom,
! [T_1] :
( class_Rings_Olinordered__idom(T_1)
=> class_Orderings_Oord(tc_Polynomial_Opoly(T_1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1274,conjecture,
? [B_f] :
( ? [B_z] :
! [B_e] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),B_e)
=> ? [B_N] :
! [B_n] :
( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_N,B_n)
=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex),hAPP(v_s,hAPP(B_f,B_n))),B_z)),B_e) ) )
& c_SEQ_Osubseq(B_f) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1275,negated_conjecture,
~ ? [B_f] :
( ? [B_z] :
! [B_e] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),B_e)
=> ? [B_N] :
! [B_n] :
( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_N,B_n)
=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex),hAPP(v_s,hAPP(B_f,B_n))),B_z)),B_e) ) )
& c_SEQ_Osubseq(B_f) ),
inference(negated_conjecture,[status(cth)],[f1274]) ).
fof(f1327,plain,
c_SEQ_Osubseq(c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____)),
inference(cnf_transformation,[status(thm)],[f17]) ).
fof(f1616,plain,
! [V_e_2] :
( ? [B_N] :
! [B_n] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex),hAPP(v_s,hAPP(c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____),B_n))),hAPP(hAPP(c_Complex_Ocomplex_OComplex,v_x____),v_y____))),V_e_2)
| ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_N,B_n) )
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),V_e_2) ),
inference(pre_NNF_transformation,[status(thm)],[f94]) ).
fof(f1617,plain,
! [V_e_2] :
( ! [B_n] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex),hAPP(v_s,hAPP(c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____),B_n))),hAPP(hAPP(c_Complex_Ocomplex_OComplex,v_x____),v_y____))),V_e_2)
| ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,sK10_skl(V_e_2),B_n) )
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),V_e_2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10_skl]),skolemize(B_N,sK10_skl(V_e_2))],[f1616]) ).
fof(f1618,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex),hAPP(v_s,hAPP(c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____),X1))),hAPP(hAPP(c_Complex_Ocomplex_OComplex,v_x____),v_y____))),X0)
| ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,sK10_skl(X0),X1)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),X0) ),
inference(cnf_transformation,[status(thm)],[f1617]) ).
fof(f4517,plain,
class_Rings_Olinordered__idom(tc_Int_Oint),
inference(cnf_transformation,[status(thm)],[f1053]) ).
fof(f4620,plain,
class_Rings_Olinordered__idom(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1156]) ).
fof(f4773,plain,
! [T_1] :
( class_Orderings_Oord(tc_Polynomial_Opoly(T_1))
| ~ class_Rings_Olinordered__idom(T_1) ),
inference(pre_NNF_transformation,[status(thm)],[f1264]) ).
fof(f4774,plain,
! [X0] :
( class_Orderings_Oord(tc_Polynomial_Opoly(X0))
| ~ class_Rings_Olinordered__idom(X0) ),
inference(cnf_transformation,[status(thm)],[f4773]) ).
fof(f4789,plain,
! [B_f] :
( ! [B_z] :
? [B_e] :
( ! [B_N] :
? [B_n] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex),hAPP(v_s,hAPP(B_f,B_n))),B_z)),B_e)
& c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_N,B_n) )
& c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),B_e) )
| ~ c_SEQ_Osubseq(B_f) ),
inference(pre_NNF_transformation,[status(thm)],[f1275]) ).
fof(f4790,plain,
! [B_f] :
( ! [B_z] :
( ! [B_N] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex),hAPP(v_s,hAPP(B_f,sK50_skl(B_N,B_z,B_f)))),B_z)),sK49_skl(B_z,B_f))
& c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B_N,sK50_skl(B_N,B_z,B_f)) )
& c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),sK49_skl(B_z,B_f)) )
| ~ c_SEQ_Osubseq(B_f) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK49_skl,sK50_skl]),skolemize(B_e,sK49_skl(B_z,B_f)),skolemize(B_n,sK50_skl(B_N,B_z,B_f))],[f4789]) ).
fof(f4791,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),sK49_skl(X1,X0))
| ~ c_SEQ_Osubseq(X0) ),
inference(cnf_transformation,[status(thm)],[f4790]) ).
fof(f4792,plain,
! [X0,X1,X2] :
( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X1,sK50_skl(X1,X2,X0))
| ~ c_SEQ_Osubseq(X0) ),
inference(cnf_transformation,[status(thm)],[f4790]) ).
fof(f4793,plain,
! [X0,X1,X2] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex),hAPP(hAPP(c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex),hAPP(v_s,hAPP(X0,sK50_skl(X1,X2,X0)))),X2)),sK49_skl(X2,X0))
| ~ c_SEQ_Osubseq(X0) ),
inference(cnf_transformation,[status(thm)],[f4790]) ).
fof(f5285,plain,
! [X0,X1] : c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X0,sK50_skl(X0,X1,c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____))),
inference(resolution,[status(thm)],[f1327,f4792]) ).
fof(f11100,plain,
! [X0] :
( ~ c_SEQ_Osubseq(c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____))
| ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,sK10_skl(sK49_skl(hAPP(hAPP(c_Complex_Ocomplex_OComplex,v_x____),v_y____),c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____))),sK50_skl(X0,hAPP(hAPP(c_Complex_Ocomplex_OComplex,v_x____),v_y____),c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____)))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),sK49_skl(hAPP(hAPP(c_Complex_Ocomplex_OComplex,v_x____),v_y____),c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____))) ),
inference(resolution,[status(thm)],[f1618,f4793]) ).
fof(f11103,definition,
( sQ119_spl
<=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),sK49_skl(hAPP(hAPP(c_Complex_Ocomplex_OComplex,v_x____),v_y____),c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____))) ),
introduced(definition,[new_symbols(definition,[sQ119_spl])],[split_symbol_definition]) ).
fof(f11105,plain,
( sQ119_spl
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),sK49_skl(hAPP(hAPP(c_Complex_Ocomplex_OComplex,v_x____),v_y____),c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____))) ),
inference(component_clause,[status(thm)],[f11103]) ).
fof(f11106,definition,
! [X0] :
( sQ120_spl
<=> ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,sK10_skl(sK49_skl(hAPP(hAPP(c_Complex_Ocomplex_OComplex,v_x____),v_y____),c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____))),sK50_skl(X0,hAPP(hAPP(c_Complex_Ocomplex_OComplex,v_x____),v_y____),c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____))) ),
introduced(definition,[new_symbols(definition,[sQ120_spl])],[split_symbol_definition]) ).
fof(f11107,plain,
! [X0] :
( ~ sQ120_spl
| ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,sK10_skl(sK49_skl(hAPP(hAPP(c_Complex_Ocomplex_OComplex,v_x____),v_y____),c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____))),sK50_skl(X0,hAPP(hAPP(c_Complex_Ocomplex_OComplex,v_x____),v_y____),c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____))) ),
inference(component_clause,[status(thm)],[f11106]) ).
fof(f11109,definition,
( sQ121_spl
<=> c_SEQ_Osubseq(c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____)) ),
introduced(definition,[new_symbols(definition,[sQ121_spl])],[split_symbol_definition]) ).
fof(f11111,plain,
( sQ121_spl
| ~ c_SEQ_Osubseq(c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____)) ),
inference(component_clause,[status(thm)],[f11109]) ).
fof(f11112,plain,
( ~ sQ121_spl
| sQ120_spl
| ~ sQ119_spl ),
inference(split_clause,[status(thm)],[f11100,f11103,f11106,f11109]) ).
fof(f11113,plain,
( sQ121_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11111,f1327]) ).
fof(f11114,plain,
sQ121_spl,
inference(contradiction_clause,[status(thm)],[f11113]) ).
fof(f11650,plain,
( ~ sQ120_spl
| $false ),
inference(resolution,[status(thm)],[f11107,f5285]) ).
fof(f11655,plain,
~ sQ120_spl,
inference(contradiction_clause,[status(thm)],[f11650]) ).
fof(f11843,definition,
( sQ141_spl
<=> class_Orderings_Oord(tc_Polynomial_Opoly(tc_Int_Oint)) ),
introduced(definition,[new_symbols(definition,[sQ141_spl])],[split_symbol_definition]) ).
fof(f11845,plain,
( sQ141_spl
| ~ class_Orderings_Oord(tc_Polynomial_Opoly(tc_Int_Oint)) ),
inference(component_clause,[status(thm)],[f11843]) ).
fof(f11850,plain,
( sQ141_spl
| ~ class_Rings_Olinordered__idom(tc_Int_Oint) ),
inference(resolution,[status(thm)],[f11845,f4774]) ).
fof(f11851,plain,
( sQ141_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11850,f4517]) ).
fof(f11852,plain,
sQ141_spl,
inference(contradiction_clause,[status(thm)],[f11851]) ).
fof(f11854,definition,
( sQ143_spl
<=> class_Orderings_Oord(tc_Polynomial_Opoly(tc_RealDef_Oreal)) ),
introduced(definition,[new_symbols(definition,[sQ143_spl])],[split_symbol_definition]) ).
fof(f11856,plain,
( sQ143_spl
| ~ class_Orderings_Oord(tc_Polynomial_Opoly(tc_RealDef_Oreal)) ),
inference(component_clause,[status(thm)],[f11854]) ).
fof(f11861,plain,
( sQ143_spl
| ~ class_Rings_Olinordered__idom(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f11856,f4774]) ).
fof(f11862,plain,
( sQ143_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f11861,f4620]) ).
fof(f11863,plain,
sQ143_spl,
inference(contradiction_clause,[status(thm)],[f11862]) ).
fof(f11870,definition,
( sQ145_spl
<=> c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) = c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
introduced(definition,[new_symbols(definition,[sQ145_spl])],[split_symbol_definition]) ).
fof(f11872,plain,
( sQ145_spl
| c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) != c_Groups_Ozero__class_Ozero(tc_Complex_Ocomplex) ),
inference(component_clause,[status(thm)],[f11870]) ).
fof(f11882,plain,
( sQ145_spl
| $false ),
inference(trivial_equality_resolution,[status(thm)],[f11872]) ).
fof(f11883,plain,
sQ145_spl,
inference(contradiction_clause,[status(thm)],[f11882]) ).
fof(f11949,plain,
( sQ119_spl
| ~ c_SEQ_Osubseq(c_Fun_Ocomp(tc_Nat_Onat,tc_Nat_Onat,tc_Nat_Onat,v_f____,v_ga____)) ),
inference(resolution,[status(thm)],[f11105,f4791]) ).
fof(f11952,plain,
( sQ119_spl
| ~ sQ121_spl ),
inference(split_clause,[status(thm)],[f11949,f11109,f11103]) ).
fof(f11960,plain,
$false,
inference(sat_refutation,[status(thm)],[f11112,f11114,f11655,f11852,f11863,f11883,f11952]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW212+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.19/5.45 % Computer : n014.cluster.edu
% 0.19/5.45 % Model : x86_64 x86_64
% 0.19/5.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/5.45 % Memory : 8046.5625MB
% 0.19/5.45 % OS : Linux 6.8.0-71-generic
% 0.19/5.45 % CPULimit : 300
% 0.19/5.45 % WCLimit : 300
% 0.19/5.45 % DateTime : Mon Sep 21 09:41:11 UTC 2026
% 0.19/5.46 % CPUTime :
% 0.23/5.63 % Drodi V4.1.1
% 10.81/7.06 % Refutation found
% 10.81/7.06 % SZS status Theorem for theBenchmark: Theorem is valid
% 10.81/7.06 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 10.81/7.13 % Elapsed time: 1.656574 seconds
% 10.81/7.13 % CPU time: 11.489102 seconds
% 10.81/7.13 % Total memory used: 303.908 MB
% 10.81/7.13 % Net memory used: 296.423 MB
%------------------------------------------------------------------------------