%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWW259+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n006.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:14:00 AM UTC 2026
% Result : Theorem 54.52s 13.74s
% Output : CNFRefutation 54.52s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 4
% Syntax : Number of formulae : 21 ( 10 unt; 0 def)
% Number of atoms : 47 ( 0 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 45 ( 19 ~; 14 |; 8 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 3 ( 2 usr; 2 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 6 con; 0-3 aty)
% Number of variables : 14 ( 0 sgn 7 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact__096_B_Bd2_O_A0_A_060_Ad2_A_061_061_062_AEX_Ae_0620_O_Ae_A_060_A1_A_G_Ae_A_060_Ad2_096,axiom,
! [V_d2] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),V_d2)
=> ? [B_e] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_e,V_d2)
& c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_e,c_Groups_Oone__class_Oone(tc_RealDef_Oreal))
& c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),B_e) ) ),
file('theBenchmark.p',fact__096_B_Bd2_O_A0_A_060_Ad2_A_061_061_062_AEX_Ae_0620_O_Ae_A_060_A1_A_G_Ae_A_060_Ad2_096) ).
fof(conj_0,axiom,
! [B_t] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),B_t)
=> ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_t,c_Groups_Oone__class_Oone(tc_RealDef_Oreal))
=> ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_t,c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____)))
=> v_thesis____ ) ) ),
file('theBenchmark.p',conj_0) ).
fof(conj_1,conjecture,
v_thesis____,
file('theBenchmark.p',conj_1) ).
fof(conj_1_neg,negated_conjecture,
~ v_thesis____,
inference(assume_negation,[status(cth)],[conj_1]) ).
fof(nnf_2,plain,
! [V_d2] :
( ? [B_e] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_e,V_d2)
& c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,B_e,c_Groups_Oone__class_Oone(tc_RealDef_Oreal))
& c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),B_e) )
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),V_d2) ),
inference(fof_nnf,[status(thm)],[fact__096_B_Bd2_O_A0_A_060_Ad2_A_061_061_062_AEX_Ae_0620_O_Ae_A_060_A1_A_G_Ae_A_060_Ad2_096]) ).
fof(sk_fact__096_B_Bd2_O_A0_A_060_Ad2_A_061_061_062_AEX_Ae_0620_O_Ae_A_060_A1_A_G_Ae_A_060_Ad2_096_sk,plain,
! [V_d2] :
( ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK0(V_d2),V_d2)
& c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK0(V_d2),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))
& c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),sK0(V_d2)) )
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),V_d2) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(B_e,sK0(V_d2))],[nnf_2]) ).
fof(sk_fact__096_B_Bd2_O_A0_A_060_Ad2_A_061_061_062_AEX_Ae_0620_O_Ae_A_060_A1_A_G_Ae_A_060_Ad2_096,plain,
( ! [VAR_0] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK0(VAR_0),VAR_0)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),VAR_0) )
& ! [VAR_0] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK0(VAR_0),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),VAR_0) )
& ! [VAR_0] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),sK0(VAR_0))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),VAR_0) ) ),
inference(cnf_transformation,[status(thm)],[sk_fact__096_B_Bd2_O_A0_A_060_Ad2_A_061_061_062_AEX_Ae_0620_O_Ae_A_060_A1_A_G_Ae_A_060_Ad2_096_sk]) ).
cnf(c_1840,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),sK0(A))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),A) ),
inference(split_conjunct,[status(thm)],[sk_fact__096_B_Bd2_O_A0_A_060_Ad2_A_061_061_062_AEX_Ae_0620_O_Ae_A_060_A1_A_G_Ae_A_060_Ad2_096]) ).
cnf(c_1841,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK0(A),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),A) ),
inference(split_conjunct,[status(thm)],[sk_fact__096_B_Bd2_O_A0_A_060_Ad2_A_061_061_062_AEX_Ae_0620_O_Ae_A_060_A1_A_G_Ae_A_060_Ad2_096]) ).
cnf(c_1842,plain,
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK0(A),A)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),A) ),
inference(split_conjunct,[status(thm)],[sk_fact__096_B_Bd2_O_A0_A_060_Ad2_A_061_061_062_AEX_Ae_0620_O_Ae_A_060_A1_A_G_Ae_A_060_Ad2_096]) ).
fof(fact_inv0,axiom,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____))),
file('theBenchmark.p',fact_inv0) ).
cnf(c_1844,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____))),
inference(clausify,[status(thm)],[fact_inv0]) ).
cnf(c_2656,plain,
( v_thesis____
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,A,c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____)))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,A,c_Groups_Oone__class_Oone(tc_RealDef_Oreal))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),A) ),
inference(clausify,[status(thm)],[conj_0]) ).
cnf(c_2657,negated_conjecture,
~ v_thesis____,
inference(clausify,[status(thm)],[conj_1_neg]) ).
cnf(c_2711,negated_conjecture,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,A,c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____)))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,A,c_Groups_Oone__class_Oone(tc_RealDef_Oreal))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),A) ),
inference(resolve,[status(thm)],[c_2657,c_2656]) ).
cnf(c_2771,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK0(c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____))),c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____))),
inference(resolve,[status(thm)],[c_1844,c_1842]) ).
cnf(c_2772,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK0(c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
inference(resolve,[status(thm)],[c_1844,c_1841]) ).
cnf(c_2773,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),sK0(c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____)))),
inference(resolve,[status(thm)],[c_1844,c_1840]) ).
cnf(c_35251,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK0(c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal))
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),sK0(c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____)))) ),
inference(resolve,[status(thm)],[c_2771,c_2711]) ).
cnf(c_35252,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,sK0(c_Rings_Oinverse__class_Oinverse(tc_RealDef_Oreal,hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),hAPP(hAPP(c_Power_Opower__class_Opower(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_w____)),c_Groups_Oplus__class_Oplus(tc_Nat_Onat,v_k____,c_Groups_Oone__class_Oone(tc_Nat_Onat)))),v_m____))),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
inference(resolve,[status(thm)],[c_2773,c_35251]) ).
cnf(c_35250,plain,
$false,
inference(resolve,[status(thm)],[c_2772,c_35252]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWW259+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.06 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.18/5.65 % Computer : n006.cluster.edu
% 0.18/5.65 % Model : x86_64 x86_64
% 0.18/5.65 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.18/5.65 % Memory : 8046.5625MB
% 0.18/5.65 % OS : Linux 6.8.0-71-generic
% 0.18/5.65 % CPULimit : 300
% 0.18/5.65 % WCLimit : 300
% 0.18/5.65 % DateTime : Sat Sep 26 15:32:33 UTC 2026
% 0.18/5.65 % CPUTime :
% 0.18/5.65 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.18/5.65 % Process 1570751 was started by sandbox2 on n006,
% 0.18/5.65 % Sat Sep 26 15:32:33 2026
% 0.18/5.65 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.22/5.90
% 0.22/5.90 % From the command line: assign(max_seconds, 300).
% 0.22/5.90
% 0.22/5.90 % SInE: 647 to sos, 610 to usable, of 1257 axioms (tolerance 2.00, depth 0 fixpoint).
% 54.52/13.74
% 54.52/13.74 % given #500 (F,wt=23): 6351 -c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,f2(c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_m____)). [resolve(5021,a,1547,c),unit_del(a,1747)].
% 54.52/13.74
% 54.52/13.74 % given #1000 (W,wt=18): 15200 c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,A,A),c_Groups_Oone__class_Oone(tc_Nat_Onat)). [resolve(14907,a,2062,a(flip))].
% 54.52/13.74
% 54.52/13.74 % given #1500 (F,wt=24): 20556 -c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Nat_OSuc(A),c_Nat_OSuc(c_Groups_Ominus__class_Ominus(tc_Nat_Onat,B,B))). [resolve(2228,a,16685,a)].
% 54.52/13.74
% 54.52/13.74 % given #2000 (T,wt=20): 26559 c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat),c_Nat_OSuc(A)) | c_Nat_OSuc(B) != A. [resolve(25012,a,1987,b),flip(b)].
% 54.52/13.74
% 54.52/13.74 % given #2500 (F,wt=16): 31181 -c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c9,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,c6)). [resolve(31160,a,2422,b),unit_del(b,31167)].
% 54.52/13.74
% 54.52/13.74 % given #3000 (T,wt=13): 33765 class_Groups_Ocomm__monoid__add(tc_Polynomial_Opoly(tc_Int_Oint)). [resolve(2647,a,2613,a)].
% 54.52/13.74
% 54.52/13.74 % SZS status Theorem for theBenchmark
% 54.52/13.74
% 54.52/13.74 % Proof 1 at 6.25 (+ 1.38) seconds.
% 54.52/13.74 % Length of proof is 14.
% 54.52/13.74 % Level of proof is 3.
% 54.52/13.74 % Maximum clause weight is 164.000.
% 54.52/13.74 % Given clauses 3343.
% 54.52/13.74
% 54.52/13.74 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------