%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWW237+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n026.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 : Sun Sep 27 09:13:58 AM UTC 2026
% Result : Theorem 120.87s 17.27s
% Output : CNFRefutation 120.87s
% Verified :
% SZS Type : Refutation
% Derivation depth : 11
% Number of leaves : 17
% Syntax : Number of formulae : 63 ( 27 unt; 0 def)
% Number of atoms : 129 ( 7 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 111 ( 45 ~; 46 |; 3 &)
% ( 4 <=>; 13 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 8 ( 6 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-3 aty)
% Number of variables : 75 ( 0 sgn 28 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_real__le__antisym,axiom,
! [V_w,V_z] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_z,V_w)
=> ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_w,V_z)
=> V_z = V_w ) ),
file('theBenchmark.p',fact_real__le__antisym) ).
fof(fact_real__le__linear,axiom,
! [V_w,V_z] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_w,V_z)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_z,V_w) ),
file('theBenchmark.p',fact_real__le__linear) ).
fof(fact_real__le__refl,axiom,
! [V_w] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_w,V_w),
file('theBenchmark.p',fact_real__le__refl) ).
fof(fact_real__less__def,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('theBenchmark.p',fact_real__less__def) ).
fof(fact_order__trans,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__eq(T_a,V_y,V_z)
=> c_Orderings_Oord__class_Oless__eq(T_a,V_x,V_z) ) ) ),
file('theBenchmark.p',fact_order__trans) ).
fof(fact_add__le__imp__le__right,axiom,
! [V_b,V_c,V_a,T_a] :
( class_Groups_Oordered__ab__semigroup__add__imp__le(T_a)
=> ( c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Oplus__class_Oplus(T_a,V_a,V_c),c_Groups_Oplus__class_Oplus(T_a,V_b,V_c))
=> c_Orderings_Oord__class_Oless__eq(T_a,V_a,V_b) ) ),
file('theBenchmark.p',fact_add__le__imp__le__right) ).
fof(fact_order__less__le__trans,axiom,
! [V_z,V_y,V_x,T_a] :
( class_Orderings_Opreorder(T_a)
=> ( c_Orderings_Oord__class_Oless(T_a,V_x,V_y)
=> ( c_Orderings_Oord__class_Oless__eq(T_a,V_y,V_z)
=> c_Orderings_Oord__class_Oless(T_a,V_x,V_z) ) ) ),
file('theBenchmark.p',fact_order__less__le__trans) ).
fof(fact_less__le__not__le,axiom,
! [V_y_2,V_x_2,T_a] :
( class_Orderings_Opreorder(T_a)
=> ( c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2)
<=> ( ~ c_Orderings_Oord__class_Oless__eq(T_a,V_y_2,V_x_2)
& c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2) ) ) ),
file('theBenchmark.p',fact_less__le__not__le) ).
fof(fact_linorder__not__less,axiom,
! [V_y_2,V_x_2,T_a] :
( class_Orderings_Olinorder(T_a)
=> ( ~ c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2)
<=> c_Orderings_Oord__class_Oless__eq(T_a,V_y_2,V_x_2) ) ),
file('theBenchmark.p',fact_linorder__not__less) ).
fof(fact_abs__le__iff,axiom,
! [V_b_2,V_ab_2,T_a] :
( class_Groups_Oordered__ab__group__add__abs(T_a)
=> ( c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Oabs__class_Oabs(T_a,V_ab_2),V_b_2)
<=> ( c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Ouminus__class_Ouminus(T_a,V_ab_2),V_b_2)
& c_Orderings_Oord__class_Oless__eq(T_a,V_ab_2,V_b_2) ) ) ),
file('theBenchmark.p',fact_abs__le__iff) ).
fof(conj_2,conjecture,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_da____,v_mazh),
file('theBenchmark.p',conj_2) ).
fof(conj_2_neg,negated_conjecture,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_da____,v_mazh),
inference(assume_negation,[status(cth)],[conj_2]) ).
cnf(c_1088,plain,
( c_Orderings_Oord__class_Oless__eq(A,B,D)
| ~ c_Orderings_Oord__class_Oless__eq(A,C,D)
| ~ c_Orderings_Oord__class_Oless__eq(A,B,C)
| ~ class_Orderings_Opreorder(A) ),
inference(clausify,[status(thm)],[fact_order__trans]) ).
cnf(c_1113,plain,
( c_Orderings_Oord__class_Oless__eq(A,B,D)
| ~ c_Orderings_Oord__class_Oless__eq(A,c_Groups_Oplus__class_Oplus(A,B,C),c_Groups_Oplus__class_Oplus(A,D,C))
| ~ class_Groups_Oordered__ab__semigroup__add__imp__le(A) ),
inference(clausify,[status(thm)],[fact_add__le__imp__le__right]) ).
cnf(c_1185,plain,
( c_Orderings_Oord__class_Oless(A,B,D)
| ~ c_Orderings_Oord__class_Oless__eq(A,C,D)
| ~ c_Orderings_Oord__class_Oless(A,B,C)
| ~ class_Orderings_Opreorder(A) ),
inference(clausify,[status(thm)],[fact_order__less__le__trans]) ).
cnf(c_1204,plain,
( c_Orderings_Oord__class_Oless__eq(A,C,B)
| ~ c_Orderings_Oord__class_Oless__eq(A,B,C)
| c_Orderings_Oord__class_Oless(A,B,C)
| ~ class_Orderings_Opreorder(A) ),
inference(clausify,[status(thm)],[fact_less__le__not__le]) ).
cnf(c_1212,plain,
( ~ c_Orderings_Oord__class_Oless__eq(A,C,B)
| ~ c_Orderings_Oord__class_Oless(A,B,C)
| ~ class_Orderings_Olinorder(A) ),
inference(clausify,[status(thm)],[fact_linorder__not__less]) ).
cnf(c_1234,plain,
( c_Orderings_Oord__class_Oless__eq(A,B,C)
| ~ c_Orderings_Oord__class_Oless__eq(A,c_Groups_Oabs__class_Oabs(A,B),C)
| ~ class_Groups_Oordered__ab__group__add__abs(A) ),
inference(clausify,[status(thm)],[fact_abs__le__iff]) ).
fof(arity_RealDef__Oreal__Groups_Oordered__ab__semigroup__add__imp__le,axiom,
class_Groups_Oordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal),
file('theBenchmark.p',arity_RealDef__Oreal__Groups_Oordered__ab__semigroup__add__imp__le) ).
cnf(c_1889,plain,
class_Groups_Oordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal),
inference(clausify,[status(thm)],[arity_RealDef__Oreal__Groups_Oordered__ab__semigroup__add__imp__le]) ).
fof(arity_RealDef__Oreal__Groups_Oordered__ab__group__add__abs,axiom,
class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal),
file('theBenchmark.p',arity_RealDef__Oreal__Groups_Oordered__ab__group__add__abs) ).
cnf(c_1898,plain,
class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal),
inference(clausify,[status(thm)],[arity_RealDef__Oreal__Groups_Oordered__ab__group__add__abs]) ).
fof(arity_RealDef__Oreal__Orderings_Opreorder,axiom,
class_Orderings_Opreorder(tc_RealDef_Oreal),
file('theBenchmark.p',arity_RealDef__Oreal__Orderings_Opreorder) ).
cnf(c_1926,plain,
class_Orderings_Opreorder(tc_RealDef_Oreal),
inference(clausify,[status(thm)],[arity_RealDef__Oreal__Orderings_Opreorder]) ).
fof(arity_RealDef__Oreal__Orderings_Olinorder,axiom,
class_Orderings_Olinorder(tc_RealDef_Oreal),
file('theBenchmark.p',arity_RealDef__Oreal__Orderings_Olinorder) ).
cnf(c_1927,plain,
class_Orderings_Olinorder(tc_RealDef_Oreal),
inference(clausify,[status(thm)],[arity_RealDef__Oreal__Orderings_Olinorder]) ).
cnf(c_2040,plain,
( B = A
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,B,A)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,B) ),
inference(clausify,[status(thm)],[fact_real__le__antisym]) ).
cnf(c_2042,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,B,A)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,B) ),
inference(clausify,[status(thm)],[fact_real__le__linear]) ).
cnf(c_2043,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,A),
inference(clausify,[status(thm)],[fact_real__le__refl]) ).
cnf(c_2090,plain,
( B != A
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,A,B) ),
inference(clausify,[status(thm)],[fact_real__less__def]) ).
fof(conj_0,axiom,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_mzh,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_mazh,v_ma)),
file('theBenchmark.p',conj_0) ).
cnf(c_2812,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_mzh,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_mazh,v_ma)),
inference(clausify,[status(thm)],[conj_0]) ).
fof(conj_1,axiom,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_da____),v_ma),v_mzh),
file('theBenchmark.p',conj_1) ).
cnf(c_2813,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_da____),v_ma),v_mzh),
inference(clausify,[status(thm)],[conj_1]) ).
cnf(c_2814,negated_conjecture,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_da____,v_mazh),
inference(clausify,[status(thm)],[conj_2_neg]) ).
cnf(c_21290,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,A))
| ~ class_Groups_Oordered__ab__group__add__abs(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_2043,c_1234]) ).
cnf(c_3024,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,A)),
inference(resolve,[status(thm)],[c_1898,c_21290]) ).
cnf(c_21291,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,A,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,B))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,A,B)
| ~ class_Orderings_Opreorder(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_3024,c_1185]) ).
cnf(c_3193,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,A,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,B))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,A,B) ),
inference(resolve,[status(thm)],[c_1926,c_21291]) ).
cnf(c_21292,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_mazh,v_ma))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,v_mzh)
| ~ class_Orderings_Opreorder(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_2812,c_1088]) ).
cnf(c_3646,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_mazh,v_ma))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,v_mzh) ),
inference(resolve,[status(thm)],[c_1926,c_21292]) ).
cnf(c_3889,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_mazh,v_da____),
inference(resolve,[status(thm)],[c_2042,c_2814]) ).
cnf(c_21293,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,B)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B,A)
| ~ class_Orderings_Opreorder(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,B) ),
inference(resolve,[status(thm)],[c_2042,c_1204]) ).
cnf(c_21294,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B,A)
| ~ class_Orderings_Opreorder(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,B) ),
inference(copy,[status(thm)],[c_21293]) ).
cnf(c_3997,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B,A)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,B) ),
inference(resolve,[status(thm)],[c_1926,c_21294]) ).
cnf(c_21295,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_da____,v_mazh)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_mazh,v_da____)
| ~ class_Orderings_Opreorder(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_3889,c_1204]) ).
cnf(c_21296,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_da____,v_mazh)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_mazh,v_da____) ),
inference(resolve,[status(thm)],[c_1926,c_21295]) ).
cnf(c_4091,negated_conjecture,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_mazh,v_da____),
inference(resolve,[status(thm)],[c_2814,c_21296]) ).
cnf(c_21297,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_mazh,A)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_da____,A)
| ~ class_Orderings_Opreorder(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_3889,c_1088]) ).
cnf(c_4100,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_mazh,A)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_da____,A) ),
inference(resolve,[status(thm)],[c_1926,c_21297]) ).
cnf(c_5055,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_mazh,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_da____)),
inference(resolve,[status(thm)],[c_4100,c_3024]) ).
cnf(c_21298,plain,
( v_mazh = c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_da____)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_da____),v_mazh) ),
inference(resolve,[status(thm)],[c_5055,c_2040]) ).
cnf(c_5058,plain,
( c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_da____) = v_mazh
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_da____),v_mazh) ),
inference(copy,[status(thm)],[c_21298]) ).
cnf(c_21299,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_mzh,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_da____),v_ma))
| ~ class_Orderings_Olinorder(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_2813,c_1212]) ).
cnf(c_6553,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_mzh,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_da____),v_ma)),
inference(resolve,[status(thm)],[c_1927,c_21299]) ).
cnf(c_7388,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_mazh,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_da____)),
inference(resolve,[status(thm)],[c_3193,c_4091]) ).
cnf(c_7390,plain,
c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_da____) != v_mazh,
inference(resolve,[status(thm)],[c_7388,c_2090]) ).
cnf(c_7408,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_da____),v_mazh),
inference(resolve,[status(thm)],[c_7390,c_5058]) ).
cnf(c_13943,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_mzh,A)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_mazh,v_ma)) ),
inference(resolve,[status(thm)],[c_3646,c_3997]) ).
cnf(c_21300,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,v_mazh)
| ~ class_Groups_Oordered__ab__semigroup__add__imp__le(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_mzh,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,A,v_ma)) ),
inference(resolve,[status(thm)],[c_13943,c_1113]) ).
cnf(c_18595,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,v_mazh)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_mzh,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,A,v_ma)) ),
inference(resolve,[status(thm)],[c_1889,c_21300]) ).
cnf(c_21301,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_mzh,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_da____),v_ma)),
inference(resolve,[status(thm)],[c_18595,c_7408]) ).
cnf(c_21289,plain,
$false,
inference(resolve,[status(thm)],[c_6553,c_21301]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW237+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.07 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.17/0.44 % Computer : n026.cluster.edu
% 0.17/0.44 % Model : x86_64 x86_64
% 0.17/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.17/0.44 % Memory : 8046.5625MB
% 0.17/0.44 % OS : Linux 6.8.0-71-generic
% 0.17/0.44 % CPULimit : 300
% 0.17/0.44 % WCLimit : 300
% 0.17/0.44 % DateTime : Sat Sep 26 15:33:10 UTC 2026
% 0.17/0.44 % CPUTime :
% 0.17/0.45 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.17/0.45 % Process 1367047 was started by sandbox on n026,
% 0.17/0.45 % Sat Sep 26 15:33:10 2026
% 0.17/0.45 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.56/0.82
% 0.56/0.82 % From the command line: assign(max_seconds, 300).
% 0.56/0.82
% 0.56/0.82 % SInE: 608 to sos, 680 to usable, of 1288 axioms (tolerance 2.00, depth 0 fixpoint).
% 120.87/17.27
% 120.87/17.27 % given #500 (F,wt=10): 11541 -c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_da____),v_mazh)). [para(11508(a,1),8607(a,2))].
% 120.87/17.27
% 120.87/17.27 % given #1000 (W,wt=10): 17220 c_Groups_Oplus__class_Oplus(tc_Nat_Onat,A,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),B)) != B. [resolve(6720,a,2139,b),flip(a)].
% 120.87/17.27
% 120.87/17.27 % SZS status Theorem for theBenchmark
% 120.87/17.27
% 120.87/17.27 % Proof 1 at 14.06 (+ 2.08) seconds.
% 120.87/17.27 % Length of proof is 44.
% 120.87/17.27 % Level of proof is 7.
% 120.87/17.27 % Maximum clause weight is 11.000.
% 120.87/17.27 % Given clauses 1471.
% 120.87/17.27
% 120.87/17.27 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------