%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWW204+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 : n008.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 8.05s 21.95s
% Output : CNFRefutation 8.05s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 7
% Syntax : Number of formulae : 24 ( 14 unt; 0 def)
% Number of atoms : 42 ( 6 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 31 ( 13 ~; 13 |; 1 &)
% ( 1 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 4 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 5 con; 0-2 aty)
% Number of variables : 20 ( 2 sgn 9 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_assms,axiom,
! [B_n] : hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(v_s,B_n))),v_r)),
file('theBenchmark.p',fact_assms) ).
fof(fact_real__le__linear,axiom,
! [V_w,V_z] :
( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_w),V_z))
| hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_z),V_w)) ),
file('theBenchmark.p',fact_real__le__linear) ).
fof(fact_real__le__trans,axiom,
! [V_k,V_j,V_i] :
( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i),V_j))
=> ( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_j),V_k))
=> hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i),V_k)) ) ),
file('theBenchmark.p',fact_real__le__trans) ).
fof(fact_order__eq__iff,axiom,
! [V_y_2,V_x_2,T_a] :
( class_Orderings_Oorder(T_a)
=> ( V_x_2 = V_y_2
<=> ( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(T_a,V_y_2),V_x_2))
& hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(T_a,V_x_2),V_y_2)) ) ) ),
file('theBenchmark.p',fact_order__eq__iff) ).
fof(conj_0,conjecture,
hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),v_r)),
file('theBenchmark.p',conj_0) ).
fof(conj_0_neg,negated_conjecture,
~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),v_r)),
inference(assume_negation,[status(cth)],[conj_0]) ).
cnf(c_1691,plain,
hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(v_s,A))),v_r)),
inference(clausify,[status(thm)],[fact_assms]) ).
cnf(c_1694,plain,
( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,B),A))
| hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A),B)) ),
inference(clausify,[status(thm)],[fact_real__le__linear]) ).
cnf(c_1695,plain,
( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A),C))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,B),C))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A),B)) ),
inference(clausify,[status(thm)],[fact_real__le__trans]) ).
cnf(c_1702,plain,
( ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(A,B),C))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(A,C),B))
| B = C
| ~ class_Orderings_Oorder(A) ),
inference(clausify,[status(thm)],[fact_order__eq__iff]) ).
fof(fact__0960_A_060_061_Acmod_A_Is_A0_J_096,axiom,
hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(v_s,c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))),
file('theBenchmark.p',fact__0960_A_060_061_Acmod_A_Is_A0_J_096) ).
cnf(c_1704,plain,
hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(v_s,c_Groups_Ozero__class_Ozero(tc_Nat_Onat))))),
inference(clausify,[status(thm)],[fact__0960_A_060_061_Acmod_A_Is_A0_J_096]) ).
fof(arity_RealDef__Oreal__Orderings_Oorder,axiom,
class_Orderings_Oorder(tc_RealDef_Oreal),
file('theBenchmark.p',arity_RealDef__Oreal__Orderings_Oorder) ).
cnf(c_2760,plain,
class_Orderings_Oorder(tc_RealDef_Oreal),
inference(clausify,[status(thm)],[arity_RealDef__Oreal__Orderings_Oorder]) ).
cnf(c_2781,negated_conjecture,
~ 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)],[conj_0_neg]) ).
cnf(c_3366,plain,
hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_r),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),
inference(resolve,[status(thm)],[c_1694,c_2781]) ).
cnf(c_3530,plain,
( hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))
| ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A),v_r)) ),
inference(resolve,[status(thm)],[c_1695,c_3366]) ).
cnf(c_3645,plain,
hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(v_s,A))),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))),
inference(resolve,[status(thm)],[c_3530,c_1691]) ).
cnf(c_5344,plain,
( ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(v_s,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))
| c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) = c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(v_s,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))
| ~ class_Orderings_Oorder(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_1704,c_1702]) ).
cnf(c_5345,plain,
( ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(v_s,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))
| c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(v_s,c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ class_Orderings_Oorder(tc_RealDef_Oreal) ),
inference(copy,[status(thm)],[c_5344]) ).
cnf(c_5346,plain,
( ~ hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(v_s,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)))
| c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(v_s,c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_2760,c_5345]) ).
cnf(c_4759,plain,
c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(v_s,c_Groups_Ozero__class_Ozero(tc_Nat_Onat))) = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),
inference(resolve,[status(thm)],[c_3645,c_5346]) ).
cnf(c_5347,plain,
hBOOL(hAPP(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),v_r)),
inference(paramod,[status(thm)],[c_4759,c_1691]) ).
cnf(c_5343,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_2781,c_5347]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW204+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.12/20.41 % Computer : n008.cluster.edu
% 0.12/20.41 % Model : x86_64 x86_64
% 0.12/20.41 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/20.41 % Memory : 8046.5625MB
% 0.12/20.41 % OS : Linux 6.8.0-71-generic
% 0.12/20.41 % CPULimit : 300
% 0.12/20.41 % WCLimit : 300
% 0.12/20.41 % DateTime : Sat Sep 26 15:29:07 UTC 2026
% 0.12/20.42 % CPUTime :
% 0.12/20.42 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.12/20.42 % Process 3965159 was started by sandbox on n008,
% 0.12/20.42 % Sat Sep 26 15:29:07 2026
% 0.12/20.42 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.17/20.79
% 0.17/20.79 % From the command line: assign(max_seconds, 300).
% 0.17/20.79
% 0.17/20.79 % SInE: 774 to sos, 489 to usable, of 1263 axioms (tolerance 2.00, depth 0 fixpoint).
% 8.05/21.95
% 8.05/21.95 % SZS status Theorem for theBenchmark
% 8.05/21.95
% 8.05/21.95 % Proof 1 at 0.92 (+ 0.15) seconds.
% 8.05/21.95 % Length of proof is 17.
% 8.05/21.95 % Level of proof is 6.
% 8.05/21.95 % Maximum clause weight is 332.000.
% 8.05/21.95 % Given clauses 185.
% 8.05/21.95
% 8.05/21.95 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------