%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWW232+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 : n017.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 0.54s 0.82s
% Output : CNFRefutation 0.54s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 4
% Syntax : Number of formulae : 22 ( 10 unt; 0 def)
% Number of atoms : 44 ( 8 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 38 ( 16 ~; 15 |; 3 &)
% ( 0 <=>; 4 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 5 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 2 prp; 0-3 aty)
% Number of functors : 15 ( 15 usr; 6 con; 0-3 aty)
% Number of variables : 33 ( 2 sgn 17 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_pCons_Ohyps,axiom,
! [V_a,V_d] :
( v_cs____ != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex))
=> ? [B_r] :
! [B_z] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,B_r,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_z))
=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_d,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,V_a,v_cs____)),B_z))) ) ),
file('theBenchmark.p',fact_pCons_Ohyps) ).
fof(conj_0,axiom,
( ? [B_r] :
! [B_z] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,B_r,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_z))
=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_da____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_aa____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_c____,v_cs____)),B_z))) )
=> 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(fact_H,axiom,
v_cs____ != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
file('theBenchmark.p',fact_H) ).
cnf(c_1786,plain,
v_cs____ != c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)),
inference(clausify,[status(thm)],[fact_H]) ).
cnf(c_1787,plain,
c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) != v_cs____,
inference(copy,[status(thm)],[c_1786]) ).
fof(nnf_2,plain,
! [V_a,V_d] :
( ? [B_r] :
! [B_z] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_d,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,V_a,v_cs____)),B_z)))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,B_r,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_z)) )
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = v_cs____ ),
inference(fof_nnf,[status(thm)],[fact_pCons_Ohyps]) ).
fof(sk_fact_pCons_Ohyps_sk,plain,
! [V_a,V_d] :
( ! [B_z] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_d,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,V_a,v_cs____)),B_z)))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sK0(V_a,V_d),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_z)) )
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = v_cs____ ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(B_r,sK0(V_a,V_d))],[nnf_2]) ).
fof(sk_fact_pCons_Ohyps,plain,
! [VAR_0,VAR_1,VAR_2] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,VAR_1,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,VAR_0,v_cs____)),VAR_2)))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sK0(VAR_0,VAR_1),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,VAR_2))
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = v_cs____ ),
inference(cnf_transformation,[status(thm)],[sk_fact_pCons_Ohyps_sk]) ).
cnf(c_1789,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,B,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,A,v_cs____)),C)))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sK0(A,B),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,C))
| c_Groups_Ozero__class_Ozero(tc_Polynomial_Opoly(tc_Complex_Ocomplex)) = v_cs____ ),
inference(split_conjunct,[status(thm)],[sk_fact_pCons_Ohyps]) ).
cnf(c_1790,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,B,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,A,v_cs____)),C)))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,sK0(A,B),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,C)) ),
inference(resolve,[status(thm)],[c_1787,c_1789]) ).
fof(nnf_618,plain,
( v_thesis____
| ! [B_r] :
? [B_z] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_da____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_aa____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_c____,v_cs____)),B_z)))
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,B_r,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,B_z)) ) ),
inference(fof_nnf,[status(thm)],[conj_0]) ).
fof(sk_conj_0_sk,plain,
( v_thesis____
| ! [B_r] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_da____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_aa____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_c____,v_cs____)),sK1(B_r))))
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,B_r,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,sK1(B_r))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(B_z,sK1(B_r))],[nnf_618]) ).
fof(sk_conj_0,plain,
( ! [VAR_0] :
( v_thesis____
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_da____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_aa____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_c____,v_cs____)),sK1(VAR_0)))) )
& ! [VAR_0] :
( v_thesis____
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,VAR_0,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,sK1(VAR_0))) ) ),
inference(cnf_transformation,[status(thm)],[sk_conj_0_sk]) ).
cnf(c_2679,plain,
( v_thesis____
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,sK1(A))) ),
inference(split_conjunct,[status(thm)],[sk_conj_0]) ).
cnf(c_2680,plain,
( v_thesis____
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_da____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_aa____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_c____,v_cs____)),sK1(A)))) ),
inference(split_conjunct,[status(thm)],[sk_conj_0]) ).
cnf(c_2681,negated_conjecture,
~ v_thesis____,
inference(clausify,[status(thm)],[conj_1_neg]) ).
cnf(c_2735,negated_conjecture,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,v_da____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,v_aa____)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,v_c____,v_cs____)),sK1(A)))),
inference(resolve,[status(thm)],[c_2681,c_2680]) ).
cnf(c_2736,negated_conjecture,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,sK1(A))),
inference(resolve,[status(thm)],[c_2681,c_2679]) ).
cnf(c_2908,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,c_Polynomial_OpCons(tc_Complex_Ocomplex,B,v_cs____)),sK1(sK0(B,A))))),
inference(resolve,[status(thm)],[c_1790,c_2736]) ).
cnf(c_2909,plain,
$false,
inference(resolve,[status(thm)],[c_2908,c_2735]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW232+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.37 % Computer : n017.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sat Sep 26 15:25:33 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.37 % Process 1069441 was started by sandbox on n017,
% 0.10/0.37 % Sat Sep 26 15:25:33 2026
% 0.10/0.37 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.31/0.62
% 0.31/0.62 % From the command line: assign(max_seconds, 300).
% 0.31/0.62
% 0.31/0.62 % SInE: 691 to sos, 562 to usable, of 1253 axioms (tolerance 2.00, depth 0 fixpoint).
% 0.54/0.82
% 0.54/0.82 % SZS status Theorem for theBenchmark
% 0.54/0.82
% 0.54/0.82 % Proof 1 at 0.12 (+ 0.02) seconds.
% 0.54/0.82 % Length of proof is 14.
% 0.54/0.82 % Level of proof is 4.
% 0.54/0.82 % Maximum clause weight is 146.000.
% 0.54/0.82 % Given clauses 14.
% 0.54/0.82
% 0.54/0.82 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------