%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : SWW215+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 : n013.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 12.44s 2.46s
% Output : CNFRefutation 12.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 7
% Number of leaves : 7
% Syntax : Number of formulae : 24 ( 14 unt; 0 def)
% Number of atoms : 39 ( 0 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 30 ( 15 ~; 11 |; 0 &)
% ( 1 <=>; 3 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 4 ( 3 usr; 1 prp; 0-3 aty)
% Number of functors : 8 ( 8 usr; 5 con; 0-3 aty)
% Number of variables : 20 ( 0 sgn 8 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(fact_real__le__linear,axiom,
! [V_w,V_z] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_w,V_z)
| 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] :
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i,V_j)
=> ( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_j,V_k)
=> c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_i,V_k) ) ),
file('theBenchmark.p',fact_real__le__trans) ).
fof(fact_linorder__not__less,axiom,
! [V_y_2,V_x_2,T_a] :
( class_Orderings_Olinorder(T_a)
=> ( ~ c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2)
<=> c_Orderings_Oord__class_Oless__eq(T_a,V_y_2,V_x_2) ) ),
file('theBenchmark.p',fact_linorder__not__less) ).
fof(conj_0,conjecture,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
file('theBenchmark.p',conj_0) ).
fof(conj_0_neg,negated_conjecture,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
inference(assume_negation,[status(cth)],[conj_0]) ).
cnf(c_1060,plain,
( ~ c_Orderings_Oord__class_Oless__eq(A,C,B)
| ~ c_Orderings_Oord__class_Oless(A,B,C)
| ~ class_Orderings_Olinorder(A) ),
inference(clausify,[status(thm)],[fact_linorder__not__less]) ).
fof(arity_RealDef__Oreal__Orderings_Olinorder,axiom,
class_Orderings_Olinorder(tc_RealDef_Oreal),
file('theBenchmark.p',arity_RealDef__Oreal__Orderings_Olinorder) ).
cnf(c_1578,plain,
class_Orderings_Olinorder(tc_RealDef_Oreal),
inference(clausify,[status(thm)],[arity_RealDef__Oreal__Orderings_Olinorder]) ).
fof(fact_H_I2_J,axiom,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_da____,c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
file('theBenchmark.p',fact_H_I2_J) ).
cnf(c_1649,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,v_da____,c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
inference(clausify,[status(thm)],[fact_H_I2_J]) ).
fof(fact_H_I5_J,axiom,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z)),v_da____),
file('theBenchmark.p',fact_H_I5_J) ).
cnf(c_1650,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z)),v_da____),
inference(clausify,[status(thm)],[fact_H_I5_J]) ).
cnf(c_1655,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,B,A)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,B) ),
inference(clausify,[status(thm)],[fact_real__le__linear]) ).
cnf(c_1656,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,C)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,B,C)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,B) ),
inference(clausify,[status(thm)],[fact_real__le__trans]) ).
cnf(c_2831,negated_conjecture,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z)),c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
inference(clausify,[status(thm)],[conj_0_neg]) ).
cnf(c_6901,plain,
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),v_da____)
| ~ class_Orderings_Olinorder(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_1649,c_1060]) ).
cnf(c_3395,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),v_da____),
inference(resolve,[status(thm)],[c_1578,c_6901]) ).
cnf(c_3401,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_da____,c_Groups_Oone__class_Oone(tc_RealDef_Oreal)),
inference(resolve,[status(thm)],[c_3395,c_1655]) ).
cnf(c_6902,plain,
( ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_da____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z)))
| ~ class_Orderings_Olinorder(tc_RealDef_Oreal) ),
inference(resolve,[status(thm)],[c_1650,c_1060]) ).
cnf(c_3509,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_da____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z))),
inference(resolve,[status(thm)],[c_1578,c_6902]) ).
cnf(c_4231,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,C)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,C,B)
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,B) ),
inference(resolve,[status(thm)],[c_1656,c_1655]) ).
cnf(c_4364,plain,
( c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_da____,A)
| c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,A,c_Groups_Oone__class_Oone(tc_RealDef_Oreal)) ),
inference(resolve,[status(thm)],[c_4231,c_3401]) ).
cnf(c_6903,negated_conjecture,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,v_da____,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,c_Groups_Ominus__class_Ominus(tc_Complex_Ocomplex,v_w____,v_z))),
inference(resolve,[status(thm)],[c_2831,c_4364]) ).
cnf(c_6900,negated_conjecture,
$false,
inference(resolve,[status(thm)],[c_3509,c_6903]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW215+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n013.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sat Sep 26 15:28:36 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.09/0.36 % Process 3043900 was started by sandbox2 on n013,
% 0.09/0.36 % Sat Sep 26 15:28:36 2026
% 0.09/0.36 % The command was "/export/starexec/sandbox2/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox2/benchmark/theBenchmark.p".
% 0.37/0.63
% 0.37/0.63 % From the command line: assign(max_seconds, 300).
% 0.37/0.63
% 0.37/0.63 % SInE: 851 to sos, 426 to usable, of 1277 axioms (tolerance 2.00, depth 0 fixpoint).
% 12.44/2.46
% 12.44/2.46 % SZS status Theorem for theBenchmark
% 12.44/2.46
% 12.44/2.46 % Proof 1 at 1.50 (+ 0.19) seconds.
% 12.44/2.46 % Length of proof is 17.
% 12.44/2.46 % Level of proof is 5.
% 12.44/2.46 % Maximum clause weight is 115.000.
% 12.44/2.46 % Given clauses 225.
% 12.44/2.46
% 12.44/2.46 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------