%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWW205+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 : n005.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:55 AM UTC 2026
% Result : Theorem 46.50s 7.30s
% Output : CNFRefutation 46.50s
% Verified :
% SZS Type : Refutation
% Derivation depth : 12
% Number of leaves : 16
% Syntax : Number of formulae : 57 ( 41 unt; 0 def)
% Number of atoms : 87 ( 39 equ)
% Maximal formula atoms : 8 ( 1 avg)
% Number of connectives : 51 ( 21 ~; 14 |; 6 &)
% ( 2 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 6 con; 0-5 aty)
% Number of variables : 120 ( 28 sgn 36 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_Im_Oadd,axiom,
! [V_y,V_x] : hAPP(c_Complex_OIm,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex),V_x),V_y)) = hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),hAPP(c_Complex_OIm,V_x)),hAPP(c_Complex_OIm,V_y)),
file('theBenchmark.p',fact_Im_Oadd) ).
fof(fact_plus__nat_Oadd__0,axiom,
! [V_n] : hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),V_n) = V_n,
file('theBenchmark.p',fact_plus__nat_Oadd__0) ).
fof(fact_o__def,axiom,
! [V_x_2,V_gb_2,V_fa_2,T_c,T_a,T_b] : hAPP(c_Fun_Ocomp(T_b,T_a,T_c,V_fa_2,V_gb_2),V_x_2) = hAPP(V_fa_2,hAPP(V_gb_2,V_x_2)),
file('theBenchmark.p',fact_o__def) ).
fof(fact_complex__of__real__add__Complex,axiom,
! [V_y,V_x,V_r] : hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex),hAPP(c_RealVector_Oof__real(tc_Complex_Ocomplex),V_r)),c_Complex_Ocomplex_OComplex(V_x,V_y)) = c_Complex_Ocomplex_OComplex(hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),V_r),V_x),V_y),
file('theBenchmark.p',fact_complex__of__real__add__Complex) ).
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_Re,axiom,
! [V_y,V_x] : hAPP(c_Complex_ORe,c_Complex_Ocomplex_OComplex(V_x,V_y)) = V_x,
file('theBenchmark.p',fact_Re) ).
fof(fact_Im,axiom,
! [V_y,V_x] : hAPP(c_Complex_OIm,c_Complex_Ocomplex_OComplex(V_x,V_y)) = V_y,
file('theBenchmark.p',fact_Im) ).
fof(fact_Im__complex__of__real,axiom,
! [V_z] : hAPP(c_Complex_OIm,hAPP(c_RealVector_Oof__real(tc_Complex_Ocomplex),V_z)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
file('theBenchmark.p',fact_Im__complex__of__real) ).
fof(fact_Re_Opos__bounded,axiom,
? [B_K] :
( ! [B_x] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(c_Complex_ORe,B_x)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_x)),B_K))
& c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),B_K) ),
file('theBenchmark.p',fact_Re_Opos__bounded) ).
fof(fact_add__strict__right__mono,axiom,
! [V_c,V_b,V_a,T_a] :
( class_Groups_Oordered__cancel__ab__semigroup__add(T_a)
=> ( c_Orderings_Oord__class_Oless(T_a,V_a,V_b)
=> c_Orderings_Oord__class_Oless(T_a,hAPP(hAPP(c_Groups_Oplus__class_Oplus(T_a),V_a),V_c),hAPP(hAPP(c_Groups_Oplus__class_Oplus(T_a),V_b),V_c)) ) ),
file('theBenchmark.p',fact_add__strict__right__mono) ).
fof(fact_sgn__greater,axiom,
! [V_a_2,T_a] :
( class_Rings_Olinordered__idom(T_a)
=> ( c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),c_Groups_Osgn__class_Osgn(T_a,V_a_2))
<=> c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),V_a_2) ) ),
file('theBenchmark.p',fact_sgn__greater) ).
fof(fact_sgn__if,axiom,
! [V_x,T_a] :
( class_Groups_Osgn__if(T_a)
=> ( ( V_x != c_Groups_Ozero__class_Ozero(T_a)
=> ( ( ~ c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),V_x)
=> c_Groups_Osgn__class_Osgn(T_a,V_x) = hAPP(c_Groups_Ouminus__class_Ouminus(T_a),c_Groups_Oone__class_Oone(T_a)) )
& ( c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),V_x)
=> c_Groups_Osgn__class_Osgn(T_a,V_x) = c_Groups_Oone__class_Oone(T_a) ) ) )
& ( V_x = c_Groups_Ozero__class_Ozero(T_a)
=> c_Groups_Osgn__class_Osgn(T_a,V_x) = c_Groups_Ozero__class_Ozero(T_a) ) ) ),
file('theBenchmark.p',fact_sgn__if) ).
fof(help_c__COMBS__1,axiom,
! [V_R_2,V_Q_2,V_P_2,T_a,T_c,T_b] : hAPP(c_COMBS(T_b,T_c,T_a,V_P_2,V_Q_2),V_R_2) = hAPP(hAPP(V_P_2,V_R_2),hAPP(V_Q_2,V_R_2)),
file('theBenchmark.p',help_c__COMBS__1) ).
cnf(c_1169,plain,
( c_Orderings_Oord__class_Oless(A,hAPP(hAPP(c_Groups_Oplus__class_Oplus(A),B),D),hAPP(hAPP(c_Groups_Oplus__class_Oplus(A),C),D))
| ~ c_Orderings_Oord__class_Oless(A,B,C)
| ~ class_Groups_Oordered__cancel__ab__semigroup__add(A) ),
inference(clausify,[status(thm)],[fact_add__strict__right__mono]) ).
cnf(c_1199,plain,
( ~ c_Orderings_Oord__class_Oless(A,c_Groups_Ozero__class_Ozero(A),B)
| c_Orderings_Oord__class_Oless(A,c_Groups_Ozero__class_Ozero(A),c_Groups_Osgn__class_Osgn(A,B))
| ~ class_Rings_Olinordered__idom(A) ),
inference(clausify,[status(thm)],[fact_sgn__greater]) ).
cnf(c_1229,plain,
( c_Groups_Osgn__class_Osgn(A,B) = c_Groups_Oone__class_Oone(A)
| ~ c_Orderings_Oord__class_Oless(A,c_Groups_Ozero__class_Ozero(A),B)
| c_Groups_Ozero__class_Ozero(A) = B
| ~ class_Groups_Osgn__if(A) ),
inference(clausify,[status(thm)],[fact_sgn__if]) ).
fof(arity_RealDef__Oreal__Groups_Oordered__cancel__ab__semigroup__add,axiom,
class_Groups_Oordered__cancel__ab__semigroup__add(tc_RealDef_Oreal),
file('theBenchmark.p',arity_RealDef__Oreal__Groups_Oordered__cancel__ab__semigroup__add) ).
cnf(c_1629,plain,
class_Groups_Oordered__cancel__ab__semigroup__add(tc_RealDef_Oreal),
inference(clausify,[status(thm)],[arity_RealDef__Oreal__Groups_Oordered__cancel__ab__semigroup__add]) ).
fof(arity_RealDef__Oreal__Groups_Osgn__if,axiom,
class_Groups_Osgn__if(tc_RealDef_Oreal),
file('theBenchmark.p',arity_RealDef__Oreal__Groups_Osgn__if) ).
cnf(c_1666,plain,
class_Groups_Osgn__if(tc_RealDef_Oreal),
inference(clausify,[status(thm)],[arity_RealDef__Oreal__Groups_Osgn__if]) ).
cnf(c_1744,plain,
hAPP(c_COMBS(A,B,C,D,E),F) = hAPP(hAPP(D,F),hAPP(E,F)),
inference(clausify,[status(thm)],[help_c__COMBS__1]) ).
cnf(c_1817,plain,
hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),hAPP(c_Complex_OIm,A)),hAPP(c_Complex_OIm,B)) = hAPP(c_Complex_OIm,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex),A),B)),
inference(clausify,[status(thm)],[fact_Im_Oadd]) ).
cnf(c_1927,plain,
hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),A) = A,
inference(clausify,[status(thm)],[fact_plus__nat_Oadd__0]) ).
cnf(c_1966,plain,
hAPP(c_Fun_Ocomp(A,B,C,D,E),F) = hAPP(D,hAPP(E,F)),
inference(clausify,[status(thm)],[fact_o__def]) ).
cnf(c_2020,plain,
c_Complex_Ocomplex_OComplex(hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),A),B),C) = hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex),hAPP(c_RealVector_Oof__real(tc_Complex_Ocomplex),A)),c_Complex_Ocomplex_OComplex(B,C)),
inference(clausify,[status(thm)],[fact_complex__of__real__add__Complex]) ).
cnf(c_2021,plain,
hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_Complex_Ocomplex),hAPP(c_RealVector_Oof__real(tc_Complex_Ocomplex),A)),c_Complex_Ocomplex_OComplex(B,C)) = c_Complex_Ocomplex_OComplex(hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),A),B),C),
inference(copy,[status(thm)],[c_2020]) ).
cnf(c_2040,plain,
( B != A
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,A,B) ),
inference(clausify,[status(thm)],[fact_real__less__def]) ).
cnf(c_2043,plain,
hAPP(c_Complex_ORe,c_Complex_Ocomplex_OComplex(A,B)) = A,
inference(clausify,[status(thm)],[fact_Re]) ).
cnf(c_2044,plain,
hAPP(c_Complex_OIm,c_Complex_Ocomplex_OComplex(A,B)) = B,
inference(clausify,[status(thm)],[fact_Im]) ).
cnf(c_2061,plain,
c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = hAPP(c_Complex_OIm,hAPP(c_RealVector_Oof__real(tc_Complex_Ocomplex),A)),
inference(clausify,[status(thm)],[fact_Im__complex__of__real]) ).
cnf(c_2062,plain,
hAPP(c_Complex_OIm,hAPP(c_RealVector_Oof__real(tc_Complex_Ocomplex),A)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(copy,[status(thm)],[c_2061]) ).
fof(nnf_495,plain,
? [B_K] :
( ! [B_x] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(c_Complex_ORe,B_x)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_x)),B_K))
& c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),B_K) ),
inference(fof_nnf,[status(thm)],[fact_Re_Opos__bounded]) ).
fof(sk_fact_Re_Opos__bounded,plain,
( ! [B_x] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_RealDef_Oreal,hAPP(c_Complex_ORe,B_x)),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_x)),sK0))
& c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),sK0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(B_K,sK0)],[nnf_495]) ).
cnf(c_2435,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),sK0),
inference(split_conjunct,[status(thm)],[sk_fact_Re_Opos__bounded]) ).
fof(arity_RealDef__Oreal__Rings_Olinordered__idom,axiom,
class_Rings_Olinordered__idom(tc_RealDef_Oreal),
file('theBenchmark.p',arity_RealDef__Oreal__Rings_Olinordered__idom) ).
cnf(c_2764,plain,
class_Rings_Olinordered__idom(tc_RealDef_Oreal),
inference(clausify,[status(thm)],[arity_RealDef__Oreal__Rings_Olinordered__idom]) ).
cnf(c_26076,plain,
hAPP(hAPP(D,F),hAPP(E,F)) = hAPP(c_COMBS(A,B,C,D,E),F),
inference(copy,[status(thm)],[c_1744]) ).
cnf(c_2912,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(c_COMBS(A,B,C,D,E),F),hAPP(hAPP(D,F),hAPP(E,F))),
inference(resolve,[status(thm)],[c_2040,c_26076]) ).
cnf(c_26077,plain,
sK0 != c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(resolve,[status(thm)],[c_2435,c_2040]) ).
cnf(c_3335,plain,
c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) != sK0,
inference(copy,[status(thm)],[c_26077]) ).
cnf(c_26078,plain,
( c_Groups_Osgn__class_Osgn(tc_RealDef_Oreal,sK0) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal)
| c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = sK0
| ~ class_Groups_Osgn__if(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_2435,c_1229]) ).
cnf(c_26079,plain,
( c_Groups_Osgn__class_Osgn(tc_RealDef_Oreal,sK0) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal)
| c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = sK0 ),
inference(resolve,[status(thm)],[c_1666,c_26078]) ).
cnf(c_3378,plain,
c_Groups_Osgn__class_Osgn(tc_RealDef_Oreal,sK0) = c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
inference(resolve,[status(thm)],[c_3335,c_26079]) ).
cnf(c_26080,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Osgn__class_Osgn(tc_RealDef_Oreal,sK0))
| ~ class_Rings_Olinordered__idom(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_2435,c_1199]) ).
cnf(c_26081,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))
| ~ class_Rings_Olinordered__idom(tc_RealDef_Oreal) ),
inference(paramod,[status(thm)],[c_3378,c_26080]) ).
cnf(c_3381,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
inference(resolve,[status(thm)],[c_2764,c_26081]) ).
cnf(c_26082,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),A),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),A))
| ~ class_Groups_Oordered__cancel__ab__semigroup__add(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_3381,c_1169]) ).
cnf(c_3877,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),A),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),A)),
inference(resolve,[status(thm)],[c_1629,c_26082]) ).
cnf(c_12750,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(c_COMBS(A,B,C,c_Complex_ORe,D),c_Complex_Ocomplex_OComplex(E,F)),hAPP(E,hAPP(D,c_Complex_Ocomplex_OComplex(E,F)))),
inference(paramod,[status(thm)],[c_2043,c_2912]) ).
cnf(c_19471,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(c_COMBS(A,B,C,c_Complex_ORe,hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),c_Complex_Ocomplex_OComplex(D,E)),hAPP(D,c_Complex_Ocomplex_OComplex(D,E))),
inference(paramod,[status(thm)],[c_1927,c_12750]) ).
cnf(c_22152,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(c_COMBS(A,B,C,c_Complex_ORe,hAPP(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),c_Complex_Ocomplex_OComplex(c_Fun_Ocomp(D,E,F,V6,V7),V8)),hAPP(V6,hAPP(V7,c_Complex_Ocomplex_OComplex(c_Fun_Ocomp(D,E,F,V6,V7),V8)))),
inference(paramod,[status(thm)],[c_1966,c_19471]) ).
cnf(c_26083,plain,
hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),hAPP(c_Complex_OIm,hAPP(c_RealVector_Oof__real(tc_Complex_Ocomplex),A))),hAPP(c_Complex_OIm,c_Complex_Ocomplex_OComplex(B,C))) = hAPP(c_Complex_OIm,c_Complex_Ocomplex_OComplex(hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),A),B),C)),
inference(paramod,[status(thm)],[c_2021,c_1817]) ).
cnf(c_26084,plain,
hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),hAPP(c_Complex_OIm,c_Complex_Ocomplex_OComplex(B,C))) = hAPP(c_Complex_OIm,c_Complex_Ocomplex_OComplex(hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),A),B),C)),
inference(paramod,[status(thm)],[c_2062,c_26083]) ).
cnf(c_26085,plain,
hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),C) = hAPP(c_Complex_OIm,c_Complex_Ocomplex_OComplex(hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),A),B),C)),
inference(paramod,[status(thm)],[c_2044,c_26084]) ).
cnf(c_25978,plain,
hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),A) = A,
inference(paramod,[status(thm)],[c_2044,c_26085]) ).
cnf(c_26074,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,A,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),A)),
inference(paramod,[status(thm)],[c_25978,c_3877]) ).
cnf(c_26075,plain,
$false,
inference(resolve,[status(thm)],[c_26074,c_22152]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW205+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.03 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.37 % Computer : n005.cluster.edu
% 0.09/0.37 % Model : x86_64 x86_64
% 0.09/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.37 % Memory : 8046.5625MB
% 0.09/0.37 % OS : Linux 6.8.0-71-generic
% 0.09/0.37 % CPULimit : 300
% 0.09/0.37 % WCLimit : 300
% 0.09/0.37 % DateTime : Sat Sep 26 15:27:31 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.37 % Process 2454812 was started by sandbox on n005,
% 0.09/0.37 % Sat Sep 26 15:27:31 2026
% 0.09/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.36/0.62
% 0.36/0.62 % From the command line: assign(max_seconds, 300).
% 0.36/0.62
% 0.36/0.62 % SInE: 766 to sos, 507 to usable, of 1273 axioms (tolerance 2.00, depth 0 fixpoint).
% 46.50/7.30
% 46.50/7.30 % given #500 (F,wt=34): 2900 -c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,A,hAPP(hAPP(c_Power_Opower_Opower(B,A,C),D),c_Groups_Ozero__class_Ozero(tc_Nat_Onat))). [resolve(2040,b,1427,a)].
% 46.50/7.30
% 46.50/7.30 % given #1000 (W,wt=22): 10508 c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,A,hAPP(c1,B)) | c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,B,hAPP(v_f____,A)). [resolve(10118,a,10077,a)].
% 46.50/7.30
% 46.50/7.30 % given #1500 (F,wt=45): 19592 -c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_Nat_Onat),hAPP(hAPP(c_COMBS(A,B,C,c_Complex_ORe,c_Complex_ORe),c_Complex_Ocomplex_OComplex(c_Groups_Oplus__class_Oplus(tc_Nat_Onat),D)),c_Groups_Ozero__class_Ozero(tc_Nat_Onat))). [para(1928(a,1),17715(a,2))].
% 46.50/7.30
% 46.50/7.30 % given #2000 (T,wt=22): 23852 c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,A) = A | -c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_r,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,A,v_r)). [resolve(23513,a,1162,b),unit_del(b,1659)].
% 46.50/7.30
% 46.50/7.30 % SZS status Theorem for theBenchmark
% 46.50/7.30
% 46.50/7.30 % Proof 1 at 5.48 (+ 0.99) seconds.
% 46.50/7.30 % Length of proof is 42.
% 46.50/7.30 % Level of proof is 7.
% 46.50/7.30 % Maximum clause weight is 207.000.
% 46.50/7.30 % Given clauses 2234.
% 46.50/7.30
% 46.50/7.30 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------