%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW218+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:27 PM UTC 2026
% Result : Theorem 76.87s 10.41s
% Output : CNFRefutation 77.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 10
% Syntax : Number of formulae : 80 ( 14 unt; 0 def)
% Number of atoms : 248 ( 50 equ)
% Maximal formula atoms : 9 ( 3 avg)
% Number of connectives : 259 ( 91 ~; 129 |; 26 &)
% ( 3 <=>; 9 =>; 0 <=; 1 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 2 prp; 0-3 aty)
% Number of functors : 14 ( 14 usr; 5 con; 0-2 aty)
% Number of variables : 130 ( 112 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3,axiom,
? [B_s] :
! [B_y] :
( ? [B_x] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_x)
& ? [B_z] :
( c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_z)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,B_x)
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_z),v_r) ) )
<=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_s) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f12,axiom,
! [V_y_2,V_x_2] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)
<=> ( V_x_2 != V_y_2
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f43,axiom,
! [V_x,V_y,T_a] :
( class_Orderings_Oorder(T_a)
=> ( c_Orderings_Oord__class_Oless__eq(T_a,V_y,V_x)
=> ( c_Orderings_Oord__class_Oless__eq(T_a,V_x,V_y)
=> V_x = V_y ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f99,axiom,
! [V_x,V_y,T_a] :
( class_Orderings_Olinorder(T_a)
=> ( ~ c_Orderings_Oord__class_Oless__eq(T_a,V_y,V_x)
=> c_Orderings_Oord__class_Oless(T_a,V_x,V_y) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f142,axiom,
! [V_y,V_x,T_a] :
( class_Rings_Olinordered__idom(T_a)
=> ( V_x != V_y
=> ( ~ c_Orderings_Oord__class_Oless(T_a,V_x,V_y)
=> c_Orderings_Oord__class_Oless(T_a,V_y,V_x) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1134,axiom,
class_Rings_Olinordered__idom(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1142,axiom,
class_Orderings_Olinorder(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1150,axiom,
class_Orderings_Oorder(tc_RealDef_Oreal),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1259,hypothesis,
( ? [B_s] :
! [B_y] :
( ? [B_x] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_x)
& ? [B_z] :
( c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_z)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,B_x)
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_z),v_r) ) )
<=> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_s) )
=> v_thesis____ ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1260,conjecture,
v_thesis____,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f1261,negated_conjecture,
~ v_thesis____,
inference(negated_conjecture,[status(cth)],[f1260]) ).
fof(f1266,plain,
? [B_s] :
! [B_y] :
( ( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_s)
| ? [B_x] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_x)
& ? [B_z] :
( c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_z)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,B_x)
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_z),v_r) ) ) )
& ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_s)
| ! [B_x] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_x)
| ! [B_z] :
( c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_z)) != c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,B_x)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_z),v_r) ) ) ) ),
inference(NNF_transformation,[status(thm)],[f3]) ).
fof(f1267,plain,
? [B_s] :
( ! [B_y] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_s)
| ? [B_x] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_x)
& ? [B_z] :
( c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_z)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,B_x)
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_z),v_r) ) ) )
& ! [B_y] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_s)
| ! [B_x] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_x)
| ! [B_z] :
( c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_z)) != c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,B_x)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_z),v_r) ) ) ) ),
inference(miniscoping,[status(thm)],[f1266]) ).
fof(f1268,plain,
( ! [B_y] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,sK1_skl)
| ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,sK2_skl(B_y))
& c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK3_skl(B_y))) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sK2_skl(B_y))
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,sK3_skl(B_y)),v_r) ) )
& ! [B_y] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,sK1_skl)
| ! [B_x] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_x)
| ! [B_z] :
( c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_z)) != c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,B_x)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_z),v_r) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1_skl,sK2_skl,sK3_skl]),skolemize(B_s,sK1_skl),skolemize(B_x,sK2_skl(B_y)),skolemize(B_z,sK3_skl(B_y))],[f1267]) ).
fof(f1269,plain,
! [X0,X1,X2] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X2,sK1_skl)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X2,X1)
| c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0)) != c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0),v_r) ),
inference(cnf_transformation,[status(thm)],[f1268]) ).
fof(f1270,plain,
! [X0] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,sK1_skl)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,sK3_skl(X0)),v_r) ),
inference(cnf_transformation,[status(thm)],[f1268]) ).
fof(f1271,plain,
! [X0] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,sK1_skl)
| c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK3_skl(X0))) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sK2_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f1268]) ).
fof(f1272,plain,
! [X0] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,sK1_skl)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,sK2_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f1268]) ).
fof(f1295,plain,
! [V_y_2,V_x_2] :
( ( V_x_2 = V_y_2
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2) )
& ( ( V_x_2 != V_y_2
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2) )
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2) ) ),
inference(NNF_transformation,[status(thm)],[f12]) ).
fof(f1296,plain,
( ! [V_y_2,V_x_2] :
( V_x_2 = V_y_2
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2) )
& ! [V_y_2,V_x_2] :
( ( V_x_2 != V_y_2
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2) )
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2) ) ),
inference(miniscoping,[status(thm)],[f1295]) ).
fof(f1297,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,X1)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1296]) ).
fof(f1298,plain,
! [X0,X1] :
( X0 != X1
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1296]) ).
fof(f1421,plain,
! [V_x,V_y,T_a] :
( V_x = V_y
| ~ c_Orderings_Oord__class_Oless__eq(T_a,V_x,V_y)
| ~ c_Orderings_Oord__class_Oless__eq(T_a,V_y,V_x)
| ~ class_Orderings_Oorder(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f43]) ).
fof(f1422,plain,
! [T_a] :
( ! [V_x,V_y] :
( V_x = V_y
| ~ c_Orderings_Oord__class_Oless__eq(T_a,V_x,V_y)
| ~ c_Orderings_Oord__class_Oless__eq(T_a,V_y,V_x) )
| ~ class_Orderings_Oorder(T_a) ),
inference(miniscoping,[status(thm)],[f1421]) ).
fof(f1423,plain,
! [X0,X1,X2] :
( X2 = X1
| ~ c_Orderings_Oord__class_Oless__eq(X0,X2,X1)
| ~ c_Orderings_Oord__class_Oless__eq(X0,X1,X2)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(thm)],[f1422]) ).
fof(f1612,plain,
! [V_x,V_y,T_a] :
( c_Orderings_Oord__class_Oless(T_a,V_x,V_y)
| c_Orderings_Oord__class_Oless__eq(T_a,V_y,V_x)
| ~ class_Orderings_Olinorder(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f99]) ).
fof(f1613,plain,
! [T_a] :
( ! [V_x,V_y] :
( c_Orderings_Oord__class_Oless(T_a,V_x,V_y)
| c_Orderings_Oord__class_Oless__eq(T_a,V_y,V_x) )
| ~ class_Orderings_Olinorder(T_a) ),
inference(miniscoping,[status(thm)],[f1612]) ).
fof(f1614,plain,
! [X0,X1,X2] :
( c_Orderings_Oord__class_Oless(X0,X2,X1)
| c_Orderings_Oord__class_Oless__eq(X0,X1,X2)
| ~ class_Orderings_Olinorder(X0) ),
inference(cnf_transformation,[status(thm)],[f1613]) ).
fof(f1781,plain,
! [V_y,V_x,T_a] :
( c_Orderings_Oord__class_Oless(T_a,V_y,V_x)
| c_Orderings_Oord__class_Oless(T_a,V_x,V_y)
| V_x = V_y
| ~ class_Rings_Olinordered__idom(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f142]) ).
fof(f1782,plain,
! [T_a] :
( ! [V_y,V_x] :
( c_Orderings_Oord__class_Oless(T_a,V_y,V_x)
| c_Orderings_Oord__class_Oless(T_a,V_x,V_y)
| V_x = V_y )
| ~ class_Rings_Olinordered__idom(T_a) ),
inference(miniscoping,[status(thm)],[f1781]) ).
fof(f1783,plain,
! [X0,X1,X2] :
( c_Orderings_Oord__class_Oless(X0,X2,X1)
| c_Orderings_Oord__class_Oless(X0,X1,X2)
| X1 = X2
| ~ class_Rings_Olinordered__idom(X0) ),
inference(cnf_transformation,[status(thm)],[f1782]) ).
fof(f4664,plain,
class_Rings_Olinordered__idom(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1134]) ).
fof(f4672,plain,
class_Orderings_Olinorder(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1142]) ).
fof(f4680,plain,
class_Orderings_Oorder(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1150]) ).
fof(f4845,plain,
( v_thesis____
| ! [B_s] :
? [B_y] :
( ? [B_x] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_x)
& ? [B_z] :
( c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_z)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,B_x)
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_z),v_r) ) )
<~> c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_s) ) ),
inference(pre_NNF_transformation,[status(thm)],[f1259]) ).
fof(f4846,plain,
( v_thesis____
| ! [B_s] :
? [B_y] :
( ( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_s)
| ! [B_x] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_x)
| ! [B_z] :
( c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_z)) != c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,B_x)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_z),v_r) ) ) )
& ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_s)
| ? [B_x] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_y,B_x)
& ? [B_z] :
( c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_z)) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,B_x)
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_z),v_r) ) ) ) ) ),
inference(NNF_transformation,[status(thm)],[f4845]) ).
fof(f4847,plain,
( v_thesis____
| ! [B_s] :
( ( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(B_s),B_s)
| ! [B_x] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(B_s),B_x)
| ! [B_z] :
( c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),B_z)) != c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,B_x)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_z),v_r) ) ) )
& ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(B_s),B_s)
| ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(B_s),sK72_skl(B_s))
& c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK73_skl(B_s))) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sK72_skl(B_s))
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,sK73_skl(B_s)),v_r) ) ) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK71_skl,sK72_skl,sK73_skl]),skolemize(B_y,sK71_skl(B_s)),skolemize(B_x,sK72_skl(B_s)),skolemize(B_z,sK73_skl(B_s))],[f4846]) ).
fof(f4848,plain,
! [X0] :
( v_thesis____
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,sK73_skl(X0)),v_r) ),
inference(cnf_transformation,[status(thm)],[f4847]) ).
fof(f4849,plain,
! [X0] :
( v_thesis____
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0)
| c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK73_skl(X0))) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sK72_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f4847]) ).
fof(f4850,plain,
! [X0] :
( v_thesis____
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),sK72_skl(X0)) ),
inference(cnf_transformation,[status(thm)],[f4847]) ).
fof(f4851,plain,
! [X0,X1,X2] :
( v_thesis____
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X2),X2)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X2),X1)
| c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0)) != c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0),v_r) ),
inference(cnf_transformation,[status(thm)],[f4847]) ).
fof(f4852,plain,
~ v_thesis____,
inference(cnf_transformation,[status(thm)],[f1261]) ).
fof(f4875,plain,
! [X0] : ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X0),
inference(destructive_equality_resolution,[status(thm)],[f1298]) ).
fof(f5119,plain,
! [X0,X1,X2] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X2),X2)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X2),X1)
| c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),X0)) != c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,X1)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,X0),v_r) ),
inference(backward_subsumption_resolution,[status(thm)],[f4851,f4852]) ).
fof(f5120,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),sK72_skl(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f4850,f4852]) ).
fof(f5121,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0)
| c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),sK73_skl(X0))) = c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,sK72_skl(X0)) ),
inference(backward_subsumption_resolution,[status(thm)],[f4849,f4852]) ).
fof(f5122,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,sK73_skl(X0)),v_r) ),
inference(backward_subsumption_resolution,[status(thm)],[f4848,f4852]) ).
fof(f5128,plain,
! [X0,X1] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X1),X1)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X1),sK2_skl(X0))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,sK3_skl(X0)),v_r)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,sK1_skl) ),
inference(resolution,[status(thm)],[f1271,f5119]) ).
fof(f5130,plain,
! [X0,X1] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X1),X1)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X1),sK2_skl(X0))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,sK1_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f5128,f1270]) ).
fof(f5131,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,sK1_skl)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,sK72_skl(X0))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,sK73_skl(X0)),v_r)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0) ),
inference(resolution,[status(thm)],[f5121,f1269]) ).
fof(f5135,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,sK1_skl)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,sK72_skl(X0))
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f5131,f5122]) ).
fof(f5139,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),sK1_skl)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0) ),
inference(resolution,[status(thm)],[f5135,f5120]) ).
fof(f5140,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),sK1_skl)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0) ),
inference(duplicate_literals_removal,[status(thm)],[f5139]) ).
fof(f5147,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,sK1_skl)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sK72_skl(X0),X1)
| ~ class_Orderings_Olinorder(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1614,f5135]) ).
fof(f5149,plain,
! [X0,X1] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,sK1_skl)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sK72_skl(X0),X1) ),
inference(forward_subsumption_resolution,[status(thm)],[f5147,f4672]) ).
fof(f5285,plain,
! [X0] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),sK1_skl)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),sK1_skl) ),
inference(resolution,[status(thm)],[f1272,f5130]) ).
fof(f5287,plain,
! [X0] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),sK1_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f5285]) ).
fof(f5291,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,sK1_skl)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sK72_skl(sK1_skl),X0)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(sK1_skl),sK1_skl) ),
inference(resolution,[status(thm)],[f5287,f5149]) ).
fof(f5292,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK1_skl,sK71_skl(X0))
| sK1_skl = sK71_skl(X0)
| ~ class_Rings_Olinordered__idom(tc_RealDef_Oreal)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0) ),
inference(resolution,[status(thm)],[f5287,f1783]) ).
fof(f5296,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,sK1_skl)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sK72_skl(sK1_skl),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f5291,f5149]) ).
fof(f5297,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK1_skl,sK71_skl(X0))
| sK1_skl = sK71_skl(X0)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f5292,f4664]) ).
fof(f5336,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(sK1_skl),sK1_skl)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK1_skl,sK71_skl(sK1_skl))
| sK1_skl = sK71_skl(sK1_skl) ),
inference(resolution,[status(thm)],[f5297,f5140]) ).
fof(f5342,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK1_skl,sK71_skl(sK1_skl))
| sK1_skl = sK71_skl(sK1_skl) ),
inference(forward_subsumption_resolution,[status(thm)],[f5336,f5297]) ).
fof(f5760,plain,
( sK1_skl = sK71_skl(sK1_skl)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sK1_skl,sK71_skl(sK1_skl)) ),
inference(resolution,[status(thm)],[f1297,f5342]) ).
fof(f5798,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(X0),X0)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sK71_skl(X0),sK72_skl(X0)) ),
inference(resolution,[status(thm)],[f1297,f5120]) ).
fof(f8408,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,sK1_skl)
| sK72_skl(sK1_skl) = X0
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,sK72_skl(sK1_skl))
| ~ class_Orderings_Oorder(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1423,f5296]) ).
fof(f8512,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,sK1_skl)
| sK72_skl(sK1_skl) = X0
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,sK72_skl(sK1_skl)) ),
inference(forward_subsumption_resolution,[status(thm)],[f8408,f4680]) ).
fof(f8559,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(sK1_skl),sK1_skl)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(sK1_skl),sK1_skl)
| sK72_skl(sK1_skl) = sK71_skl(sK1_skl) ),
inference(resolution,[status(thm)],[f8512,f5798]) ).
fof(f8578,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(sK1_skl),sK1_skl)
| sK72_skl(sK1_skl) = sK71_skl(sK1_skl) ),
inference(duplicate_literals_removal,[status(thm)],[f8559]) ).
fof(f8580,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(sK1_skl),sK1_skl)
| sK72_skl(sK1_skl) = sK71_skl(sK1_skl) ),
inference(resolution,[status(thm)],[f8578,f5287]) ).
fof(f8587,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,sK1_skl)
| sK71_skl(sK1_skl) = X0
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,sK72_skl(sK1_skl)) ),
inference(backward_demodulation,[status(thm)],[f8641,f8512]) ).
fof(f8641,plain,
sK72_skl(sK1_skl) = sK71_skl(sK1_skl),
inference(forward_subsumption_resolution,[status(thm)],[f8580,f8578]) ).
fof(f8642,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,sK1_skl)
| sK71_skl(sK1_skl) = X0
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,X0,sK71_skl(sK1_skl)) ),
inference(forward_demodulation,[status(thm)],[f8641,f8587]) ).
fof(f8753,plain,
( sK1_skl = sK71_skl(sK1_skl)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK1_skl,sK1_skl)
| sK71_skl(sK1_skl) = sK1_skl ),
inference(resolution,[status(thm)],[f8642,f5760]) ).
fof(f8780,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK1_skl,sK1_skl)
| sK71_skl(sK1_skl) = sK1_skl ),
inference(duplicate_literals_removal,[status(thm)],[f8753]) ).
fof(f8845,plain,
sK71_skl(sK1_skl) = sK1_skl,
inference(forward_subsumption_resolution,[status(thm)],[f8780,f4875]) ).
fof(f11443,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK1_skl,sK1_skl)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK71_skl(sK1_skl),sK1_skl) ),
inference(paramodulation,[status(thm)],[f8845,f5140]) ).
fof(f11502,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK1_skl,sK1_skl)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK1_skl,sK1_skl) ),
inference(forward_demodulation,[status(thm)],[f8845,f11443]) ).
fof(f11503,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK1_skl,sK1_skl),
inference(duplicate_literals_removal,[status(thm)],[f11502]) ).
fof(f11504,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f11503,f4875]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : SWW218+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.45 % Computer : n014.cluster.edu
% 0.19/0.45 % Model : x86_64 x86_64
% 0.19/0.45 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.19/0.45 % Memory : 8046.5625MB
% 0.19/0.45 % OS : Linux 6.8.0-71-generic
% 0.19/0.45 % CPULimit : 300
% 0.19/0.45 % WCLimit : 300
% 0.19/0.45 % DateTime : Mon Sep 21 09:42:06 UTC 2026
% 0.19/0.46 % CPUTime :
% 0.37/0.61 % Drodi V4.1.1
% 76.87/10.41 % Refutation found
% 76.87/10.41 % SZS status Theorem for theBenchmark: Theorem is valid
% 76.87/10.41 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 10.07/10.52 % Elapsed time: 10.040562 seconds
% 10.07/10.52 % CPU time: 78.020245 seconds
% 10.07/10.52 % Total memory used: 572.227 MB
% 10.07/10.52 % Net memory used: 535.799 MB
%------------------------------------------------------------------------------