%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWW208+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 : 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 : Sun Sep 27 09:13:56 AM UTC 2026
% Result : Theorem 106.35s 15.31s
% Output : CNFRefutation 106.35s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 13
% Syntax : Number of formulae : 50 ( 29 unt; 0 def)
% Number of atoms : 84 ( 30 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 60 ( 26 ~; 21 |; 2 &)
% ( 3 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 2 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 7 ( 5 usr; 1 prp; 0-2 aty)
% Number of functors : 15 ( 15 usr; 7 con; 0-3 aty)
% Number of variables : 51 ( 2 sgn 19 !; 1 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_th,axiom,
! [B_n] : hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,B_n)))),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))),
file('theBenchmark.p',fact_th) ).
fof(fact_abs__add__one__gt__zero,axiom,
! [V_x] : hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,V_x)))),
file('theBenchmark.p',fact_abs__add__one__gt__zero) ).
fof(fact_abs__eq__0,axiom,
! [V_a_2,T_a] :
( class_Groups_Oordered__ab__group__add__abs(T_a)
=> ( c_Groups_Oabs__class_Oabs(T_a,V_a_2) = c_Groups_Ozero__class_Ozero(T_a)
<=> V_a_2 = c_Groups_Ozero__class_Ozero(T_a) ) ),
file('theBenchmark.p',fact_abs__eq__0) ).
fof(fact_add__le__less__mono,axiom,
! [V_d,V_c,V_b,V_a,T_a] :
( class_Groups_Oordered__cancel__ab__semigroup__add(T_a)
=> ( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(T_a,V_a),V_b))
=> ( hBOOL(hAPP(c_Orderings_Oord__class_Oless(T_a,V_c),V_d))
=> hBOOL(hAPP(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_d))) ) ) ),
file('theBenchmark.p',fact_add__le__less__mono) ).
fof(fact_abs__of__nonneg,axiom,
! [V_a,T_a] :
( class_Groups_Oordered__ab__group__add__abs(T_a)
=> ( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Ozero__class_Ozero(T_a)),V_a))
=> c_Groups_Oabs__class_Oabs(T_a,V_a) = V_a ) ),
file('theBenchmark.p',fact_abs__of__nonneg) ).
fof(fact_add__0__iff,axiom,
! [V_a_2,V_b_2,T_a] :
( class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(T_a)
=> ( V_b_2 = hAPP(hAPP(c_Groups_Oplus__class_Oplus(T_a),V_b_2),V_a_2)
<=> V_a_2 = c_Groups_Ozero__class_Ozero(T_a) ) ),
file('theBenchmark.p',fact_add__0__iff) ).
fof(fact_right__minus__eq,axiom,
! [V_b_2,V_a_2,T_a] :
( class_Groups_Ogroup__add(T_a)
=> ( c_Groups_Ominus__class_Ominus(T_a,V_a_2,V_b_2) = c_Groups_Ozero__class_Ozero(T_a)
<=> V_a_2 = V_b_2 ) ),
file('theBenchmark.p',fact_right__minus__eq) ).
fof(conj_0,conjecture,
( ! [B_n] : hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,B_n)))))),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))))
& hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))) ),
file('theBenchmark.p',conj_0) ).
fof(conj_0_neg,negated_conjecture,
~ ( ! [B_n] : hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,B_n)))))),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))))
& hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))) ),
inference(assume_negation,[status(cth)],[conj_0]) ).
cnf(c_1077,plain,
( c_Groups_Ozero__class_Ozero(A) != B
| c_Groups_Oabs__class_Oabs(A,B) = c_Groups_Ozero__class_Ozero(A)
| ~ class_Groups_Oordered__ab__group__add__abs(A) ),
inference(clausify,[status(thm)],[fact_abs__eq__0]) ).
cnf(c_1102,plain,
( hBOOL(hAPP(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),E)))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless(A,D),E))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(A,B),C))
| ~ class_Groups_Oordered__cancel__ab__semigroup__add(A) ),
inference(clausify,[status(thm)],[fact_add__le__less__mono]) ).
cnf(c_1104,plain,
( c_Groups_Oabs__class_Oabs(A,B) = B
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(A,c_Groups_Ozero__class_Ozero(A)),B))
| ~ class_Groups_Oordered__ab__group__add__abs(A) ),
inference(clausify,[status(thm)],[fact_abs__of__nonneg]) ).
cnf(c_1163,plain,
( c_Groups_Ozero__class_Ozero(A) != C
| hAPP(hAPP(c_Groups_Oplus__class_Oplus(A),B),C) = B
| ~ class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(A) ),
inference(clausify,[status(thm)],[fact_add__0__iff]) ).
cnf(c_1414,plain,
( C != B
| c_Groups_Ominus__class_Ominus(A,B,C) = c_Groups_Ozero__class_Ozero(A)
| ~ class_Groups_Ogroup__add(A) ),
inference(clausify,[status(thm)],[fact_right__minus__eq]) ).
fof(arity_RealDef__Oreal__Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct,axiom,
class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(tc_RealDef_Oreal),
file('theBenchmark.p',arity_RealDef__Oreal__Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct) ).
cnf(c_1624,plain,
class_Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct(tc_RealDef_Oreal),
inference(clausify,[status(thm)],[arity_RealDef__Oreal__Semiring__Normalization_Ocomm__semiring__1__cancel__crossproduct]) ).
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_1625,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_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_1635,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__Groups_Ogroup__add,axiom,
class_Groups_Ogroup__add(tc_RealDef_Oreal),
file('theBenchmark.p',arity_RealDef__Oreal__Groups_Ogroup__add) ).
cnf(c_1672,plain,
class_Groups_Ogroup__add(tc_RealDef_Oreal),
inference(clausify,[status(thm)],[arity_RealDef__Oreal__Groups_Ogroup__add]) ).
fof(fact_rp,axiom,
hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),v_r)),
file('theBenchmark.p',fact_rp) ).
cnf(c_1771,plain,
hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),v_r)),
inference(clausify,[status(thm)],[fact_rp]) ).
cnf(c_1773,plain,
hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,A)))),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))),
inference(clausify,[status(thm)],[fact_th]) ).
cnf(c_1776,plain,
hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,A)))),
inference(clausify,[status(thm)],[fact_abs__add__one__gt__zero]) ).
fof(nnf_1026,plain,
( ? [B_n] : ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,B_n)))))),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))) ),
inference(fof_nnf,[status(thm)],[conj_0_neg]) ).
fof(sk_conj_0_neg,plain,
( ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,sK0)))))),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(B_n,sK0)],[nnf_1026]) ).
cnf(c_2804,negated_conjecture,
( ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,hAPP(c_Complex_OIm,hAPP(v_s,hAPP(v_f____,hAPP(v_ga____,sK0)))))),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))) ),
inference(split_conjunct,[status(thm)],[sk_conj_0_neg]) ).
cnf(c_2805,negated_conjecture,
~ hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))),
inference(resolve,[status(thm)],[c_1773,c_2804]) ).
cnf(c_5558,plain,
( c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,A) = A
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),A)) ),
inference(resolve,[status(thm)],[c_1104,c_1635]) ).
cnf(c_3002,plain,
c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r) = v_r,
inference(resolve,[status(thm)],[c_5558,c_1771]) ).
cnf(c_5559,plain,
( B != A
| c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,A,B) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_1414,c_1672]) ).
cnf(c_5560,plain,
c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,v_r,c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,v_r)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(resolve,[status(thm)],[c_5559,c_3002]) ).
cnf(c_3019,plain,
c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,v_r,v_r) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(paramod,[status(thm)],[c_3002,c_5560]) ).
cnf(c_5561,plain,
( c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) != B
| hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),A),B) = A ),
inference(resolve,[status(thm)],[c_1163,c_1624]) ).
cnf(c_5562,plain,
c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,v_r,v_r),
inference(copy,[status(thm)],[c_3019]) ).
cnf(c_5563,plain,
hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),A),c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,v_r,v_r)) = A,
inference(resolve,[status(thm)],[c_5561,c_5562]) ).
cnf(c_3205,plain,
hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),A),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) = A,
inference(paramod,[status(thm)],[c_3019,c_5563]) ).
cnf(c_5564,plain,
( c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) != A
| c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,A) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_1077,c_1635]) ).
cnf(c_5565,plain,
c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,v_r,v_r),
inference(copy,[status(thm)],[c_3019]) ).
cnf(c_5566,plain,
c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ominus__class_Ominus(tc_RealDef_Oreal,v_r,v_r)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(resolve,[status(thm)],[c_5564,c_5565]) ).
cnf(c_3207,plain,
c_Groups_Oabs__class_Oabs(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(paramod,[status(thm)],[c_3019,c_5566]) ).
cnf(c_5567,plain,
hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))),
inference(paramod,[status(thm)],[c_3207,c_1776]) ).
cnf(c_3504,plain,
hBOOL(hAPP(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(paramod,[status(thm)],[c_3205,c_5567]) ).
cnf(c_5568,plain,
( hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),A),C)),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),B),D)))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,C),D))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A),B)) ),
inference(resolve,[status(thm)],[c_1102,c_1625]) ).
cnf(c_5569,plain,
( hBOOL(hAPP(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),v_r),B)))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,A),B)) ),
inference(resolve,[status(thm)],[c_5568,c_1771]) ).
cnf(c_5570,plain,
hBOOL(hAPP(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)),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))),
inference(resolve,[status(thm)],[c_5569,c_3504]) ).
cnf(c_5571,plain,
hBOOL(hAPP(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),hAPP(hAPP(c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal),v_r),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)))),
inference(paramod,[status(thm)],[c_3205,c_5570]) ).
cnf(c_5557,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_2805,c_5571]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW208+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.06/0.34 % Computer : n014.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 : Sat Sep 26 15:28:04 UTC 2026
% 0.06/0.35 % CPUTime :
% 0.06/0.35 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.06/0.35 % Process 3487940 was started by sandbox on n014,
% 0.06/0.35 % Sat Sep 26 15:28:04 2026
% 0.06/0.35 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.31/0.59
% 0.31/0.59 % From the command line: assign(max_seconds, 300).
% 0.31/0.59
% 0.31/0.59 % SInE: 693 to sos, 575 to usable, of 1268 axioms (tolerance 2.00, depth 0 fixpoint).
% 106.35/15.31
% 106.35/15.31 % SZS status Theorem for theBenchmark
% 106.35/15.31
% 106.35/15.31 % Proof 1 at 5.06 (+ 0.70) seconds.
% 106.35/15.31 % Length of proof is 28.
% 106.35/15.31 % Level of proof is 6.
% 106.35/15.31 % Maximum clause weight is 36.000.
% 106.35/15.31 % Given clauses 203.
% 106.35/15.31
% 106.35/15.31 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------