%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWW224+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 : n016.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:28 PM UTC 2026
% Result : Theorem 22.65s 3.74s
% Output : CNFRefutation 25.66s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 17
% Syntax : Number of formulae : 80 ( 32 unt; 0 def)
% Number of atoms : 184 ( 44 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 186 ( 82 ~; 77 |; 12 &)
% ( 5 <=>; 10 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 5 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 10 ( 8 usr; 1 prp; 0-3 aty)
% Number of functors : 11 ( 11 usr; 4 con; 0-3 aty)
% Number of variables : 164 ( 164 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [V_ra_2,V_a_2,V_x_2,T_a] :
( class_Rings_Olinordered__idom(T_a)
=> ( c_Orderings_Oord__class_Oless(T_a,c_Groups_Oabs__class_Oabs(T_a,c_Groups_Ominus__class_Ominus(T_a,V_x_2,V_a_2)),V_ra_2)
<=> ( c_Orderings_Oord__class_Oless(T_a,V_x_2,c_Groups_Oplus__class_Oplus(T_a,V_a_2,V_ra_2))
& c_Orderings_Oord__class_Oless(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a_2,V_ra_2),V_x_2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f63,axiom,
! [V_z,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(T_a,V_z,V_y)
=> c_Orderings_Oord__class_Oless(T_a,V_z,V_x) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f64,axiom,
! [V_z,V_y,V_x,T_a] :
( class_Orderings_Opreorder(T_a)
=> ( c_Orderings_Oord__class_Oless__eq(T_a,V_x,V_y)
=> ( c_Orderings_Oord__class_Oless(T_a,V_y,V_z)
=> c_Orderings_Oord__class_Oless(T_a,V_x,V_z) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f100,axiom,
! [V_b,V_a,T_a] :
( class_Groups_Ogroup__add(T_a)
=> c_Groups_Ominus__class_Ominus(T_a,c_Groups_Oplus__class_Oplus(T_a,V_a,V_b),V_b) = V_a ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f101,axiom,
! [V_b,V_a,T_a] :
( class_Groups_Ogroup__add(T_a)
=> c_Groups_Oplus__class_Oplus(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a,V_b),V_b) = V_a ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f108,axiom,
! [V_y_2,V_x_2] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)
<=> c_RealDef_Opositive(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,V_y_2,V_x_2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f238,axiom,
! [V_za_2,V_x_2,V_y_2,V_wa_2,T_a] :
( class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(T_a)
=> ( c_Groups_Oplus__class_Oplus(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_wa_2),V_y_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x_2),V_za_2)) = c_Groups_Oplus__class_Oplus(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_wa_2),V_za_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x_2),V_y_2))
<=> ( V_y_2 = V_za_2
| V_wa_2 = V_x_2 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f256,axiom,
! [V_z] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),V_z) = V_z,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f414,axiom,
! [V_r] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,V_r) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_r),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1097,axiom,
class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1131,axiom,
class_Rings_Olinordered__idom(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1137,axiom,
class_Orderings_Opreorder(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1143,axiom,
class_Groups_Ogroup__add(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1145,axiom,
class_Orderings_Oorder(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1186,hypothesis,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_m,v_x),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1187,hypothesis,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_x,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_m,v_e)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1188,conjecture,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,v_x,v_m)),v_e),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p') ).
fof(f1189,negated_conjecture,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,v_x,v_m)),v_e),
inference(negated_conjecture,[status(cth)],[f1188]) ).
fof(f1193,plain,
! [V_ra_2,V_a_2,V_x_2,T_a] :
( ( c_Orderings_Oord__class_Oless(T_a,c_Groups_Oabs__class_Oabs(T_a,c_Groups_Ominus__class_Ominus(T_a,V_x_2,V_a_2)),V_ra_2)
<=> ( c_Orderings_Oord__class_Oless(T_a,V_x_2,c_Groups_Oplus__class_Oplus(T_a,V_a_2,V_ra_2))
& c_Orderings_Oord__class_Oless(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a_2,V_ra_2),V_x_2) ) )
| ~ class_Rings_Olinordered__idom(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f2]) ).
fof(f1194,plain,
! [V_ra_2,V_a_2,V_x_2,T_a] :
( ( ( ~ c_Orderings_Oord__class_Oless(T_a,V_x_2,c_Groups_Oplus__class_Oplus(T_a,V_a_2,V_ra_2))
| ~ c_Orderings_Oord__class_Oless(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a_2,V_ra_2),V_x_2)
| c_Orderings_Oord__class_Oless(T_a,c_Groups_Oabs__class_Oabs(T_a,c_Groups_Ominus__class_Ominus(T_a,V_x_2,V_a_2)),V_ra_2) )
& ( ( c_Orderings_Oord__class_Oless(T_a,V_x_2,c_Groups_Oplus__class_Oplus(T_a,V_a_2,V_ra_2))
& c_Orderings_Oord__class_Oless(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a_2,V_ra_2),V_x_2) )
| ~ c_Orderings_Oord__class_Oless(T_a,c_Groups_Oabs__class_Oabs(T_a,c_Groups_Ominus__class_Ominus(T_a,V_x_2,V_a_2)),V_ra_2) ) )
| ~ class_Rings_Olinordered__idom(T_a) ),
inference(NNF_transformation,[status(thm)],[f1193]) ).
fof(f1195,plain,
! [T_a] :
( ( ! [V_ra_2,V_a_2,V_x_2] :
( ~ c_Orderings_Oord__class_Oless(T_a,V_x_2,c_Groups_Oplus__class_Oplus(T_a,V_a_2,V_ra_2))
| ~ c_Orderings_Oord__class_Oless(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a_2,V_ra_2),V_x_2)
| c_Orderings_Oord__class_Oless(T_a,c_Groups_Oabs__class_Oabs(T_a,c_Groups_Ominus__class_Ominus(T_a,V_x_2,V_a_2)),V_ra_2) )
& ! [V_ra_2,V_a_2,V_x_2] :
( ( c_Orderings_Oord__class_Oless(T_a,V_x_2,c_Groups_Oplus__class_Oplus(T_a,V_a_2,V_ra_2))
& c_Orderings_Oord__class_Oless(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a_2,V_ra_2),V_x_2) )
| ~ c_Orderings_Oord__class_Oless(T_a,c_Groups_Oabs__class_Oabs(T_a,c_Groups_Ominus__class_Ominus(T_a,V_x_2,V_a_2)),V_ra_2) ) )
| ~ class_Rings_Olinordered__idom(T_a) ),
inference(miniscoping,[status(thm)],[f1194]) ).
fof(f1198,plain,
! [X0,X1,X2,X3] :
( ~ c_Orderings_Oord__class_Oless(X0,X1,c_Groups_Oplus__class_Oplus(X0,X2,X3))
| ~ c_Orderings_Oord__class_Oless(X0,c_Groups_Ominus__class_Ominus(X0,X2,X3),X1)
| c_Orderings_Oord__class_Oless(X0,c_Groups_Oabs__class_Oabs(X0,c_Groups_Ominus__class_Ominus(X0,X1,X2)),X3)
| ~ class_Rings_Olinordered__idom(X0) ),
inference(cnf_transformation,[status(thm)],[f1195]) ).
fof(f1396,plain,
! [V_z,V_x,V_y,T_a] :
( c_Orderings_Oord__class_Oless(T_a,V_z,V_x)
| ~ c_Orderings_Oord__class_Oless(T_a,V_z,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)],[f63]) ).
fof(f1397,plain,
! [T_a] :
( ! [V_x,V_y] :
( ! [V_z] :
( c_Orderings_Oord__class_Oless(T_a,V_z,V_x)
| ~ c_Orderings_Oord__class_Oless(T_a,V_z,V_y) )
| ~ c_Orderings_Oord__class_Oless__eq(T_a,V_y,V_x) )
| ~ class_Orderings_Oorder(T_a) ),
inference(miniscoping,[status(thm)],[f1396]) ).
fof(f1398,plain,
! [X0,X1,X2,X3] :
( c_Orderings_Oord__class_Oless(X0,X3,X2)
| ~ c_Orderings_Oord__class_Oless(X0,X3,X1)
| ~ c_Orderings_Oord__class_Oless__eq(X0,X1,X2)
| ~ class_Orderings_Oorder(X0) ),
inference(cnf_transformation,[status(thm)],[f1397]) ).
fof(f1399,plain,
! [V_z,V_y,V_x,T_a] :
( c_Orderings_Oord__class_Oless(T_a,V_x,V_z)
| ~ c_Orderings_Oord__class_Oless(T_a,V_y,V_z)
| ~ c_Orderings_Oord__class_Oless__eq(T_a,V_x,V_y)
| ~ class_Orderings_Opreorder(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f64]) ).
fof(f1400,plain,
! [T_a] :
( ! [V_y,V_x] :
( ! [V_z] :
( c_Orderings_Oord__class_Oless(T_a,V_x,V_z)
| ~ c_Orderings_Oord__class_Oless(T_a,V_y,V_z) )
| ~ c_Orderings_Oord__class_Oless__eq(T_a,V_x,V_y) )
| ~ class_Orderings_Opreorder(T_a) ),
inference(miniscoping,[status(thm)],[f1399]) ).
fof(f1401,plain,
! [X0,X1,X2,X3] :
( c_Orderings_Oord__class_Oless(X0,X1,X3)
| ~ c_Orderings_Oord__class_Oless(X0,X2,X3)
| ~ c_Orderings_Oord__class_Oless__eq(X0,X1,X2)
| ~ class_Orderings_Opreorder(X0) ),
inference(cnf_transformation,[status(thm)],[f1400]) ).
fof(f1536,plain,
! [V_b,V_a,T_a] :
( c_Groups_Ominus__class_Ominus(T_a,c_Groups_Oplus__class_Oplus(T_a,V_a,V_b),V_b) = V_a
| ~ class_Groups_Ogroup__add(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f100]) ).
fof(f1537,plain,
! [T_a] :
( ! [V_b,V_a] : c_Groups_Ominus__class_Ominus(T_a,c_Groups_Oplus__class_Oplus(T_a,V_a,V_b),V_b) = V_a
| ~ class_Groups_Ogroup__add(T_a) ),
inference(miniscoping,[status(thm)],[f1536]) ).
fof(f1538,plain,
! [X0,X1,X2] :
( c_Groups_Ominus__class_Ominus(X0,c_Groups_Oplus__class_Oplus(X0,X1,X2),X2) = X1
| ~ class_Groups_Ogroup__add(X0) ),
inference(cnf_transformation,[status(thm)],[f1537]) ).
fof(f1539,plain,
! [V_b,V_a,T_a] :
( c_Groups_Oplus__class_Oplus(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a,V_b),V_b) = V_a
| ~ class_Groups_Ogroup__add(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f101]) ).
fof(f1540,plain,
! [T_a] :
( ! [V_b,V_a] : c_Groups_Oplus__class_Oplus(T_a,c_Groups_Ominus__class_Ominus(T_a,V_a,V_b),V_b) = V_a
| ~ class_Groups_Ogroup__add(T_a) ),
inference(miniscoping,[status(thm)],[f1539]) ).
fof(f1541,plain,
! [X0,X1,X2] :
( c_Groups_Oplus__class_Oplus(X0,c_Groups_Ominus__class_Ominus(X0,X1,X2),X2) = X1
| ~ class_Groups_Ogroup__add(X0) ),
inference(cnf_transformation,[status(thm)],[f1540]) ).
fof(f1564,plain,
! [V_y_2,V_x_2] :
( ( ~ c_RealDef_Opositive(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,V_y_2,V_x_2))
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2) )
& ( c_RealDef_Opositive(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,V_y_2,V_x_2))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2) ) ),
inference(NNF_transformation,[status(thm)],[f108]) ).
fof(f1565,plain,
( ! [V_y_2,V_x_2] :
( ~ c_RealDef_Opositive(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,V_y_2,V_x_2))
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2) )
& ! [V_y_2,V_x_2] :
( c_RealDef_Opositive(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,V_y_2,V_x_2))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2) ) ),
inference(miniscoping,[status(thm)],[f1564]) ).
fof(f1566,plain,
! [X0,X1] :
( c_RealDef_Opositive(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X1,X0))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1565]) ).
fof(f1567,plain,
! [X0,X1] :
( ~ c_RealDef_Opositive(c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X1,X0))
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,X1) ),
inference(cnf_transformation,[status(thm)],[f1565]) ).
fof(f1985,plain,
! [V_za_2,V_x_2,V_y_2,V_wa_2,T_a] :
( ( c_Groups_Oplus__class_Oplus(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_wa_2),V_y_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x_2),V_za_2)) = c_Groups_Oplus__class_Oplus(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_wa_2),V_za_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x_2),V_y_2))
<=> ( V_y_2 = V_za_2
| V_wa_2 = V_x_2 ) )
| ~ class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(T_a) ),
inference(pre_NNF_transformation,[status(thm)],[f238]) ).
fof(f1986,plain,
! [V_za_2,V_x_2,V_y_2,V_wa_2,T_a] :
( ( ( ( V_y_2 != V_za_2
& V_wa_2 != V_x_2 )
| c_Groups_Oplus__class_Oplus(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_wa_2),V_y_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x_2),V_za_2)) = c_Groups_Oplus__class_Oplus(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_wa_2),V_za_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x_2),V_y_2)) )
& ( V_y_2 = V_za_2
| V_wa_2 = V_x_2
| c_Groups_Oplus__class_Oplus(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_wa_2),V_y_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x_2),V_za_2)) != c_Groups_Oplus__class_Oplus(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_wa_2),V_za_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x_2),V_y_2)) ) )
| ~ class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(T_a) ),
inference(NNF_transformation,[status(thm)],[f1985]) ).
fof(f1987,plain,
! [T_a] :
( ( ! [V_za_2,V_x_2,V_y_2,V_wa_2] :
( ( V_y_2 != V_za_2
& V_wa_2 != V_x_2 )
| c_Groups_Oplus__class_Oplus(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_wa_2),V_y_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x_2),V_za_2)) = c_Groups_Oplus__class_Oplus(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_wa_2),V_za_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x_2),V_y_2)) )
& ! [V_za_2,V_x_2,V_y_2,V_wa_2] :
( V_y_2 = V_za_2
| V_wa_2 = V_x_2
| c_Groups_Oplus__class_Oplus(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_wa_2),V_y_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x_2),V_za_2)) != c_Groups_Oplus__class_Oplus(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_wa_2),V_za_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x_2),V_y_2)) ) )
| ~ class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(T_a) ),
inference(miniscoping,[status(thm)],[f1986]) ).
fof(f1989,plain,
! [X0,X1,X2,X3,X4] :
( X1 != X3
| c_Groups_Oplus__class_Oplus(X0,hAPP(hAPP(c_Groups_Otimes__class_Otimes(X0),X1),X2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X0),X3),X4)) = c_Groups_Oplus__class_Oplus(X0,hAPP(hAPP(c_Groups_Otimes__class_Otimes(X0),X1),X4),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X0),X3),X2))
| ~ class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(X0) ),
inference(cnf_transformation,[status(thm)],[f1987]) ).
fof(f2047,plain,
! [X0] : hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),X0) = X0,
inference(cnf_transformation,[status(thm)],[f256]) ).
fof(f2553,plain,
! [X0] : c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,X0) = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,X0),
inference(cnf_transformation,[status(thm)],[f414]) ).
fof(f4416,plain,
class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1097]) ).
fof(f4450,plain,
class_Rings_Olinordered__idom(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1131]) ).
fof(f4456,plain,
class_Orderings_Opreorder(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1137]) ).
fof(f4462,plain,
class_Groups_Ogroup__add(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1143]) ).
fof(f4464,plain,
class_Orderings_Oorder(tc_RealDef_Oreal),
inference(cnf_transformation,[status(thm)],[f1145]) ).
fof(f4505,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_m,v_x),
inference(cnf_transformation,[status(thm)],[f1186]) ).
fof(f4506,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_x,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_m,v_e)),
inference(cnf_transformation,[status(thm)],[f1187]) ).
fof(f4507,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,v_x,v_m)),v_e),
inference(cnf_transformation,[status(thm)],[f1189]) ).
fof(f4618,plain,
! [X0,X1,X2,X3] :
( c_Groups_Oplus__class_Oplus(X0,hAPP(hAPP(c_Groups_Otimes__class_Otimes(X0),X1),X2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X0),X1),X3)) = c_Groups_Oplus__class_Oplus(X0,hAPP(hAPP(c_Groups_Otimes__class_Otimes(X0),X1),X3),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X0),X1),X2))
| ~ class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(X0) ),
inference(destructive_equality_resolution,[status(thm)],[f1989]) ).
fof(f4735,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,v_x,v_m)),v_e),
inference(backward_demodulation,[status(thm)],[f2553,f4507]) ).
fof(f4747,plain,
! [X0,X1,X2] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X2))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X1,X2),X0)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,X1)),X2)
| ~ class_Rings_Olinordered__idom(tc_RealDef_Oreal) ),
inference(paramodulation,[status(thm)],[f2553,f1198]) ).
fof(f8471,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,v_x)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,v_m)
| ~ class_Orderings_Oorder(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1398,f4505]) ).
fof(f8508,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,v_x)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,v_m) ),
inference(forward_subsumption_resolution,[status(thm)],[f8471,f4464]) ).
fof(f8538,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_m,X0)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_x,X0)
| ~ class_Orderings_Opreorder(tc_RealDef_Oreal) ),
inference(resolution,[status(thm)],[f1401,f4505]) ).
fof(f8572,plain,
! [X0] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_m,X0)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_x,X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f8538,f4456]) ).
fof(f10193,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_m,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_m,v_e)),
inference(resolution,[status(thm)],[f8572,f4506]) ).
fof(f16331,plain,
! [X0,X1,X2] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X2))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X1,X2),X0)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,X1)),X2) ),
inference(forward_subsumption_resolution,[status(thm)],[f4747,f4450]) ).
fof(f16335,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_x,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_m,v_e))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,v_m,v_e),v_x) ),
inference(resolution,[status(thm)],[f16331,f4735]) ).
fof(f16363,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,v_m,v_e),v_x),
inference(forward_subsumption_resolution,[status(thm)],[f16335,f4506]) ).
fof(f16668,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,v_m,v_e),v_m),
inference(resolution,[status(thm)],[f16363,f8508]) ).
fof(f34139,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),X1)) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),X1),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),X0))
| ~ class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(tc_RealDef_Oreal) ),
inference(paramodulation,[status(thm)],[f2047,f4618]) ).
fof(f34186,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),X1),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),X0))
| ~ class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f2047,f34139]) ).
fof(f34187,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),X0))
| ~ class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f2047,f34186]) ).
fof(f34188,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0)
| ~ class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(tc_RealDef_Oreal) ),
inference(forward_demodulation,[status(thm)],[f2047,f34187]) ).
fof(f34189,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1) = c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X1,X0),
inference(forward_subsumption_resolution,[status(thm)],[f34188,f4416]) ).
fof(f34563,plain,
! [X0,X1] :
( c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X1,X0)) = X1
| ~ class_Groups_Ogroup__add(tc_RealDef_Oreal) ),
inference(paramodulation,[status(thm)],[f34189,f1541]) ).
fof(f34611,plain,
! [X0,X1] :
( c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1),X0) = X1
| ~ class_Groups_Ogroup__add(tc_RealDef_Oreal) ),
inference(paramodulation,[status(thm)],[f34189,f1538]) ).
fof(f34808,plain,
! [X0,X1] : c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X1,X0)) = X1,
inference(forward_subsumption_resolution,[status(thm)],[f34563,f4462]) ).
fof(f34853,plain,
! [X0,X1] : c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1),X0) = X1,
inference(forward_subsumption_resolution,[status(thm)],[f34611,f4462]) ).
fof(f35851,plain,
! [X0,X1] :
( c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,X1)) = X1
| ~ class_Groups_Ogroup__add(tc_RealDef_Oreal) ),
inference(paramodulation,[status(thm)],[f34808,f1538]) ).
fof(f35939,plain,
! [X0,X1] : c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,X1)) = X1,
inference(forward_subsumption_resolution,[status(thm)],[f35851,f4462]) ).
fof(f36796,plain,
! [X0,X1] :
( c_RealDef_Opositive(X1)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X0,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,X0,X1)) ),
inference(paramodulation,[status(thm)],[f34853,f1566]) ).
fof(f37445,plain,
! [X0,X1] :
( ~ c_RealDef_Opositive(X1)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,X0,X1),X0) ),
inference(paramodulation,[status(thm)],[f35939,f1567]) ).
fof(f42743,plain,
c_RealDef_Opositive(v_e),
inference(resolution,[status(thm)],[f36796,f10193]) ).
fof(f43224,plain,
~ c_RealDef_Opositive(v_e),
inference(resolution,[status(thm)],[f37445,f16668]) ).
fof(f43250,plain,
$false,
inference(forward_subsumption_resolution,[status(thm)],[f43224,f42743]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW224+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.06/0.34 % Computer : n016.cluster.edu
% 0.06/0.34 % Model : x86_64 x86_64
% 0.06/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.34 % Memory : 8046.5625MB
% 0.06/0.34 % OS : Linux 6.8.0-71-generic
% 0.06/0.34 % CPULimit : 300
% 0.06/0.34 % WCLimit : 300
% 0.06/0.34 % DateTime : Mon Sep 21 09:47:24 UTC 2026
% 0.06/0.34 % CPUTime :
% 0.11/0.44 % Drodi V4.1.1
% 22.65/3.74 % Refutation found
% 22.65/3.74 % SZS status Theorem for theBenchmark: Theorem is valid
% 22.65/3.74 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 3.65/3.83 % Elapsed time: 3.467639 seconds
% 3.65/3.83 % CPU time: 26.453955 seconds
% 3.65/3.83 % Total memory used: 376.366 MB
% 3.65/3.83 % Net memory used: 359.106 MB
%------------------------------------------------------------------------------