%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWW219+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% Computer : n015.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 : Fri Sep 25 03:26:50 PM UTC 2026
% Result : Theorem 99.72s 14.51s
% Output : Proof 99.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 63
% Syntax : Number of formulae : 268 ( 102 unt; 0 def)
% Number of atoms : 668 ( 187 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 869 ( 469 ~; 265 |; 73 &)
% ( 19 <=>; 43 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 8 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 2 prp; 0-3 aty)
% Number of functors : 26 ( 26 usr; 10 con; 0-4 aty)
% Number of variables : 483 ( 17 sgn 350 !; 4 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1265,hypothesis,
! [B_g] :
( ! [B_n] : c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(B_g,B_n)),v_r)
=> ( ! [B_n] : c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),hAPP(B_g,B_n))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(B_n)))))
=> v_thesis____ ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f1265_nnf,plain,
! [B_g] :
( v_thesis____
| ? [B_n] : ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),hAPP(B_g,B_n))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(B_n)))))
| ? [B_n] : ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(B_g,B_n)),v_r) ),
inference(nnf_transformation,[status(thm)],[f1265]) ).
fof(f1265_sk,plain,
! [B_g] :
( v_thesis____
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),hAPP(B_g,sk84(B_g)))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(sk84(B_g))))))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(B_g,sk83(B_g))),v_r) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk83,sk84])],[f1265_nnf]) ).
cnf(c1854,plain,
( v_thesis____
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),hAPP(X0,sk84(X0)))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(sk84(X0))))))
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(X0,sk83(X0))),v_r) ),
inference(cnf_transformation,[status(esa)],[f1265_sk]) ).
cnf(hi1767,axiom,
ifeq(c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(X0,sk83(X0))),v_r),true,ifeq(c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),hAPP(X0,sk84(X0)))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(sk84(X0)))))),true,v_thesis____,true),true) = true,
inference(equality_encoding,[status(esa)],[c1854]) ).
fof(f4,axiom,
? [B_f] :
! [B_x] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),hAPP(B_f,B_x))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(B_x)))))
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(B_f,B_x)),v_r) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact__096EX_Af_O_AALL_Ax_O_Acmod_A_If_Ax_h5dc79b9b0c1f8d64) ).
fof(f4_nnf,plain,
? [B_f] :
! [B_x] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),hAPP(B_f,B_x))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(B_x)))))
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(B_f,B_x)),v_r) ),
inference(nnf_transformation,[status(thm)],[f4]) ).
fof(f4_sk,plain,
! [B_x] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),hAPP(sk1,B_x))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(B_x)))))
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(sk1,B_x)),v_r) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk1])],[f4_nnf]) ).
cnf(c4,plain,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(sk1,X1)),v_r),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(hi4,axiom,
c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(sk1,X0)),v_r) = true,
inference(equality_encoding,[status(esa)],[c4]) ).
cnf(c5,plain,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),hAPP(sk1,X1))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(X1))))),
inference(cnf_transformation,[status(esa)],[f4_sk]) ).
cnf(hi5,axiom,
c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(tc_Complex_Ocomplex,hAPP(c_Polynomial_Opoly(tc_Complex_Ocomplex,v_p),hAPP(sk1,X0))),c_Groups_Oplus__class_Oplus(tc_RealDef_Oreal,c_Groups_Ouminus__class_Ouminus(tc_RealDef_Oreal,v_s____),c_Rings_Oinverse__class_Odivide(tc_RealDef_Oreal,c_Groups_Oone__class_Oone(tc_RealDef_Oreal),c_RealDef_Oreal(tc_Nat_Onat,c_Nat_OSuc(X0))))) = true,
inference(equality_encoding,[status(esa)],[c5]) ).
fof(f190,axiom,
! [V_n] : c_Nat_OSuc(V_n) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,V_n,c_Groups_Oone__class_Oone(tc_Nat_Onat)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Suc__eq__plus1) ).
fof(f190_nnf,plain,
! [V_n] : c_Nat_OSuc(V_n) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,V_n,c_Groups_Oone__class_Oone(tc_Nat_Onat)),
inference(nnf_transformation,[status(thm)],[f190]) ).
fof(f190_sk,plain,
! [V_n] : c_Nat_OSuc(V_n) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,V_n,c_Groups_Oone__class_Oone(tc_Nat_Onat)),
inference(skolemisation,[status(esa)],[f190_nnf]) ).
cnf(c293,plain,
c_Nat_OSuc(X0) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,c_Groups_Oone__class_Oone(tc_Nat_Onat)),
inference(cnf_transformation,[status(esa)],[f190_sk]) ).
cnf(hi6,axiom,
c_Nat_OSuc(X0) = c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X0,c_Groups_Oone__class_Oone(tc_Nat_Onat)),
inference(equality_encoding,[status(esa)],[c293]) ).
cnf(h90,plain,
v_thesis____ = true,
inference(hyper_resolution,[status(thm)],[hi1767,hi4,hi5,hi6]) ).
fof(f1266,conjecture,
v_thesis____,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_1) ).
fof(f1266_neg,negated_conjecture,
~ v_thesis____,
inference(negated_conjecture,[status(cth)],[f1266]) ).
fof(f1266_nnf,plain,
~ v_thesis____,
inference(nnf_transformation,[status(thm)],[f1266_neg]) ).
fof(f1266_sk,plain,
~ v_thesis____,
inference(skolemisation,[status(esa)],[f1266_nnf]) ).
cnf(c1855,plain,
~ v_thesis____,
inference(cnf_transformation,[status(esa)],[f1266_sk]) ).
cnf(hi1830,negated_conjecture,
ifeq(v_thesis____,true,false,true) = true,
inference(equality_encoding,[status(esa)],[c1855]) ).
cnf(t0,plain,
true = false,
inference(hyper_resolution,[status(thm)],[hi1830,h90]) ).
cnf(t163,plain,
false = true,
inference(orient,[status(thm)],[t0]) ).
fof(f22,axiom,
c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) != c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_real__zero__not__eq__one) ).
fof(f22_nnf,plain,
c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) != c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f22]) ).
fof(f22_sk,plain,
c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) != c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f22_nnf]) ).
cnf(c36,plain,
c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) != c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f22_sk]) ).
fof(f24,axiom,
! [V_x_2,T_a] :
( class_RealVector_Oreal__normed__vector(T_a)
=> ( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(T_a,V_x_2))
<=> V_x_2 != c_Groups_Ozero__class_Ozero(T_a) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_zero__less__norm__iff) ).
fof(f24_nnf,plain,
! [V_x_2,T_a] :
( ( ( V_x_2 = c_Groups_Ozero__class_Ozero(T_a)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(T_a,V_x_2)) )
& ( V_x_2 != c_Groups_Ozero__class_Ozero(T_a)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(T_a,V_x_2)) ) )
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(nnf_transformation,[status(thm)],[f24]) ).
fof(f24_sk,plain,
! [T_a,V_x_2] :
( ( ( V_x_2 = c_Groups_Ozero__class_Ozero(T_a)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(T_a,V_x_2)) )
& ( V_x_2 != c_Groups_Ozero__class_Ozero(T_a)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(T_a,V_x_2)) ) )
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(skolemisation,[status(esa)],[f24_nnf]) ).
cnf(c39,plain,
( X0 != c_Groups_Ozero__class_Ozero(X1)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),c_RealVector_Onorm__class_Onorm(X1,X0))
| ~ class_RealVector_Oreal__normed__vector(X1) ),
inference(cnf_transformation,[status(esa)],[f24_sk]) ).
fof(f41,axiom,
! [V_x,T_a] :
( class_RealVector_Oreal__normed__vector(T_a)
=> ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(T_a,V_x),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_norm__not__less__zero) ).
fof(f41_nnf,plain,
! [V_x,T_a] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(T_a,V_x),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(nnf_transformation,[status(thm)],[f41]) ).
fof(f41_sk,plain,
! [T_a,V_x] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(T_a,V_x),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| ~ class_RealVector_Oreal__normed__vector(T_a) ),
inference(skolemisation,[status(esa)],[f41_nnf]) ).
cnf(c79,plain,
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealVector_Onorm__class_Onorm(X1,X0),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal))
| ~ class_RealVector_Oreal__normed__vector(X1) ),
inference(cnf_transformation,[status(esa)],[f41_sk]) ).
fof(f44,axiom,
! [V_n] : ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,V_n),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_not__real__of__nat__less__zero) ).
fof(f44_nnf,plain,
! [V_n] : ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,V_n),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
inference(nnf_transformation,[status(thm)],[f44]) ).
fof(f44_sk,plain,
! [V_n] : ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,V_n),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
inference(skolemisation,[status(esa)],[f44_nnf]) ).
cnf(c87,plain,
~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_RealDef_Oreal(tc_Nat_Onat,X0),c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)),
inference(cnf_transformation,[status(esa)],[f44_sk]) ).
fof(f69,axiom,
! [V_y_2,V_x_2] :
( c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2)
<=> ( V_x_2 != V_y_2
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_real__less__def) ).
fof(f69_nnf,plain,
! [V_y_2,V_x_2] :
( ( V_x_2 = V_y_2
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2) )
& ( ( V_x_2 != V_y_2
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2) )
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2) ) ),
inference(nnf_transformation,[status(thm)],[f69]) ).
fof(f69_sk,plain,
! [V_x_2,V_y_2] :
( ( V_x_2 = V_y_2
| ~ c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2) )
& ( ( V_x_2 != V_y_2
& c_Orderings_Oord__class_Oless__eq(tc_RealDef_Oreal,V_x_2,V_y_2) )
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,V_x_2,V_y_2) ) ),
inference(skolemisation,[status(esa)],[f69_nnf]) ).
cnf(c123,plain,
( X1 != X0
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,X0) ),
inference(cnf_transformation,[status(esa)],[f69_sk]) ).
fof(f128,axiom,
! [T_a] :
( class_Rings_Ozero__neq__one(T_a)
=> c_Groups_Oone__class_Oone(T_a) != c_Groups_Ozero__class_Ozero(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_one__neq__zero) ).
fof(f128_nnf,plain,
! [T_a] :
( c_Groups_Oone__class_Oone(T_a) != c_Groups_Ozero__class_Ozero(T_a)
| ~ class_Rings_Ozero__neq__one(T_a) ),
inference(nnf_transformation,[status(thm)],[f128]) ).
fof(f128_sk,plain,
! [T_a] :
( c_Groups_Oone__class_Oone(T_a) != c_Groups_Ozero__class_Ozero(T_a)
| ~ class_Rings_Ozero__neq__one(T_a) ),
inference(skolemisation,[status(esa)],[f128_nnf]) ).
cnf(c204,plain,
( c_Groups_Oone__class_Oone(X0) != c_Groups_Ozero__class_Ozero(X0)
| ~ class_Rings_Ozero__neq__one(X0) ),
inference(cnf_transformation,[status(esa)],[f128_sk]) ).
fof(f129,axiom,
! [T_a] :
( class_Rings_Ozero__neq__one(T_a)
=> c_Groups_Ozero__class_Ozero(T_a) != c_Groups_Oone__class_Oone(T_a) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_zero__neq__one) ).
fof(f129_nnf,plain,
! [T_a] :
( c_Groups_Ozero__class_Ozero(T_a) != c_Groups_Oone__class_Oone(T_a)
| ~ class_Rings_Ozero__neq__one(T_a) ),
inference(nnf_transformation,[status(thm)],[f129]) ).
fof(f129_sk,plain,
! [T_a] :
( c_Groups_Ozero__class_Ozero(T_a) != c_Groups_Oone__class_Oone(T_a)
| ~ class_Rings_Ozero__neq__one(T_a) ),
inference(skolemisation,[status(esa)],[f129_nnf]) ).
cnf(c205,plain,
( c_Groups_Ozero__class_Ozero(X0) != c_Groups_Oone__class_Oone(X0)
| ~ class_Rings_Ozero__neq__one(X0) ),
inference(cnf_transformation,[status(esa)],[f129_sk]) ).
fof(f165,axiom,
! [T_a] :
( class_Rings_Olinordered__semidom(T_a)
=> ~ c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Oone__class_Oone(T_a),c_Groups_Ozero__class_Ozero(T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_not__one__le__zero) ).
fof(f165_nnf,plain,
! [T_a] :
( ~ c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Oone__class_Oone(T_a),c_Groups_Ozero__class_Ozero(T_a))
| ~ class_Rings_Olinordered__semidom(T_a) ),
inference(nnf_transformation,[status(thm)],[f165]) ).
fof(f165_sk,plain,
! [T_a] :
( ~ c_Orderings_Oord__class_Oless__eq(T_a,c_Groups_Oone__class_Oone(T_a),c_Groups_Ozero__class_Ozero(T_a))
| ~ class_Rings_Olinordered__semidom(T_a) ),
inference(skolemisation,[status(esa)],[f165_nnf]) ).
cnf(c257,plain,
( ~ c_Orderings_Oord__class_Oless__eq(X0,c_Groups_Oone__class_Oone(X0),c_Groups_Ozero__class_Ozero(X0))
| ~ class_Rings_Olinordered__semidom(X0) ),
inference(cnf_transformation,[status(esa)],[f165_sk]) ).
fof(f167,axiom,
! [T_a] :
( class_Rings_Olinordered__semidom(T_a)
=> ~ c_Orderings_Oord__class_Oless(T_a,c_Groups_Oone__class_Oone(T_a),c_Groups_Ozero__class_Ozero(T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_not__one__less__zero) ).
fof(f167_nnf,plain,
! [T_a] :
( ~ c_Orderings_Oord__class_Oless(T_a,c_Groups_Oone__class_Oone(T_a),c_Groups_Ozero__class_Ozero(T_a))
| ~ class_Rings_Olinordered__semidom(T_a) ),
inference(nnf_transformation,[status(thm)],[f167]) ).
fof(f167_sk,plain,
! [T_a] :
( ~ c_Orderings_Oord__class_Oless(T_a,c_Groups_Oone__class_Oone(T_a),c_Groups_Ozero__class_Ozero(T_a))
| ~ class_Rings_Olinordered__semidom(T_a) ),
inference(skolemisation,[status(esa)],[f167_nnf]) ).
cnf(c259,plain,
( ~ c_Orderings_Oord__class_Oless(X0,c_Groups_Oone__class_Oone(X0),c_Groups_Ozero__class_Ozero(X0))
| ~ class_Rings_Olinordered__semidom(X0) ),
inference(cnf_transformation,[status(esa)],[f167_sk]) ).
fof(f197,axiom,
! [V_n] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_less__zeroE) ).
fof(f197_nnf,plain,
! [V_n] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(nnf_transformation,[status(thm)],[f197]) ).
fof(f197_sk,plain,
! [V_n] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(skolemisation,[status(esa)],[f197_nnf]) ).
cnf(c305,plain,
~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(cnf_transformation,[status(esa)],[f197_sk]) ).
fof(f208,axiom,
! [V_n] : c_Nat_OSuc(V_n) != V_n,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Suc__n__not__n) ).
fof(f208_nnf,plain,
! [V_n] : c_Nat_OSuc(V_n) != V_n,
inference(nnf_transformation,[status(thm)],[f208]) ).
fof(f208_sk,plain,
! [V_n] : c_Nat_OSuc(V_n) != V_n,
inference(skolemisation,[status(esa)],[f208_nnf]) ).
cnf(c318,plain,
c_Nat_OSuc(X0) != X0,
inference(cnf_transformation,[status(esa)],[f208_sk]) ).
fof(f209,axiom,
! [V_n] : V_n != c_Nat_OSuc(V_n),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_n__not__Suc__n) ).
fof(f209_nnf,plain,
! [V_n] : V_n != c_Nat_OSuc(V_n),
inference(nnf_transformation,[status(thm)],[f209]) ).
fof(f209_sk,plain,
! [V_n] : V_n != c_Nat_OSuc(V_n),
inference(skolemisation,[status(esa)],[f209_nnf]) ).
cnf(c319,plain,
X0 != c_Nat_OSuc(X0),
inference(cnf_transformation,[status(esa)],[f209_sk]) ).
fof(f210,axiom,
! [V_m] : c_Nat_OSuc(V_m) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Suc__neq__Zero) ).
fof(f210_nnf,plain,
! [V_m] : c_Nat_OSuc(V_m) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(nnf_transformation,[status(thm)],[f210]) ).
fof(f210_sk,plain,
! [V_m] : c_Nat_OSuc(V_m) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(skolemisation,[status(esa)],[f210_nnf]) ).
cnf(c320,plain,
c_Nat_OSuc(X0) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(cnf_transformation,[status(esa)],[f210_sk]) ).
fof(f211,axiom,
! [V_m] : c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != c_Nat_OSuc(V_m),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Zero__neq__Suc) ).
fof(f211_nnf,plain,
! [V_m] : c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != c_Nat_OSuc(V_m),
inference(nnf_transformation,[status(thm)],[f211]) ).
fof(f211_sk,plain,
! [V_m] : c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != c_Nat_OSuc(V_m),
inference(skolemisation,[status(esa)],[f211_nnf]) ).
cnf(c321,plain,
c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != c_Nat_OSuc(X0),
inference(cnf_transformation,[status(esa)],[f211_sk]) ).
fof(f212,axiom,
! [V_nat_H_1] : c_Nat_OSuc(V_nat_H_1) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_nat_Osimps_I3_J) ).
fof(f212_nnf,plain,
! [V_nat_H_1] : c_Nat_OSuc(V_nat_H_1) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(nnf_transformation,[status(thm)],[f212]) ).
fof(f212_sk,plain,
! [V_nat_H_1] : c_Nat_OSuc(V_nat_H_1) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(skolemisation,[status(esa)],[f212_nnf]) ).
cnf(c322,plain,
c_Nat_OSuc(X0) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(cnf_transformation,[status(esa)],[f212_sk]) ).
fof(f213,axiom,
! [V_m] : c_Nat_OSuc(V_m) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Suc__not__Zero) ).
fof(f213_nnf,plain,
! [V_m] : c_Nat_OSuc(V_m) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(nnf_transformation,[status(thm)],[f213]) ).
fof(f213_sk,plain,
! [V_m] : c_Nat_OSuc(V_m) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(skolemisation,[status(esa)],[f213_nnf]) ).
cnf(c323,plain,
c_Nat_OSuc(X0) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(cnf_transformation,[status(esa)],[f213_sk]) ).
fof(f214,axiom,
! [V_nat_H] : c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != c_Nat_OSuc(V_nat_H),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_nat_Osimps_I2_J) ).
fof(f214_nnf,plain,
! [V_nat_H] : c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != c_Nat_OSuc(V_nat_H),
inference(nnf_transformation,[status(thm)],[f214]) ).
fof(f214_sk,plain,
! [V_nat_H] : c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != c_Nat_OSuc(V_nat_H),
inference(skolemisation,[status(esa)],[f214_nnf]) ).
cnf(c324,plain,
c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != c_Nat_OSuc(X0),
inference(cnf_transformation,[status(esa)],[f214_sk]) ).
fof(f215,axiom,
! [V_m] : c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != c_Nat_OSuc(V_m),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Zero__not__Suc) ).
fof(f215_nnf,plain,
! [V_m] : c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != c_Nat_OSuc(V_m),
inference(nnf_transformation,[status(thm)],[f215]) ).
fof(f215_sk,plain,
! [V_m] : c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != c_Nat_OSuc(V_m),
inference(skolemisation,[status(esa)],[f215_nnf]) ).
cnf(c325,plain,
c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != c_Nat_OSuc(X0),
inference(cnf_transformation,[status(esa)],[f215_sk]) ).
fof(f221,axiom,
! [V_n_2,V_m_2] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_m_2,V_n_2)
<=> c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_OSuc(V_n_2),V_m_2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_not__less__eq__eq) ).
fof(f221_nnf,plain,
! [V_n_2,V_m_2] :
( ( ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_OSuc(V_n_2),V_m_2)
| ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_m_2,V_n_2) )
& ( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_OSuc(V_n_2),V_m_2)
| c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_m_2,V_n_2) ) ),
inference(nnf_transformation,[status(thm)],[f221]) ).
fof(f221_sk,plain,
! [V_m_2,V_n_2] :
( ( ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_OSuc(V_n_2),V_m_2)
| ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_m_2,V_n_2) )
& ( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_OSuc(V_n_2),V_m_2)
| c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_m_2,V_n_2) ) ),
inference(skolemisation,[status(esa)],[f221_nnf]) ).
cnf(c335,plain,
( ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_OSuc(X0),X1)
| ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,X1,X0) ),
inference(cnf_transformation,[status(esa)],[f221_sk]) ).
fof(f222,axiom,
! [V_n] : ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_OSuc(V_n),V_n),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Suc__n__not__le__n) ).
fof(f222_nnf,plain,
! [V_n] : ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_OSuc(V_n),V_n),
inference(nnf_transformation,[status(thm)],[f222]) ).
fof(f222_sk,plain,
! [V_n] : ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_OSuc(V_n),V_n),
inference(skolemisation,[status(esa)],[f222_nnf]) ).
cnf(c336,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_OSuc(X0),X0),
inference(cnf_transformation,[status(esa)],[f222_sk]) ).
fof(f228,axiom,
! [V_t,V_s] :
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_s,V_t)
=> V_s != V_t ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_less__not__refl3) ).
fof(f228_nnf,plain,
! [V_t,V_s] :
( V_s != V_t
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_s,V_t) ),
inference(nnf_transformation,[status(thm)],[f228]) ).
fof(f228_sk,plain,
! [V_s,V_t] :
( V_s != V_t
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_s,V_t) ),
inference(skolemisation,[status(esa)],[f228_nnf]) ).
cnf(c350,plain,
( X1 != X0
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0) ),
inference(cnf_transformation,[status(esa)],[f228_sk]) ).
fof(f229,axiom,
! [V_m,V_n] :
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n,V_m)
=> V_m != V_n ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_less__not__refl2) ).
fof(f229_nnf,plain,
! [V_m,V_n] :
( V_m != V_n
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n,V_m) ),
inference(nnf_transformation,[status(thm)],[f229]) ).
fof(f229_sk,plain,
! [V_n,V_m] :
( V_m != V_n
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n,V_m) ),
inference(skolemisation,[status(esa)],[f229_nnf]) ).
cnf(c351,plain,
( X0 != X1
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0) ),
inference(cnf_transformation,[status(esa)],[f229_sk]) ).
fof(f230,axiom,
! [V_n,V_m] :
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m,V_n)
=> V_n != c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_gr__implies__not0) ).
fof(f230_nnf,plain,
! [V_n,V_m] :
( V_n != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m,V_n) ),
inference(nnf_transformation,[status(thm)],[f230]) ).
fof(f230_sk,plain,
! [V_m,V_n] :
( V_n != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m,V_n) ),
inference(skolemisation,[status(esa)],[f230_nnf]) ).
cnf(c352,plain,
( X0 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0) ),
inference(cnf_transformation,[status(esa)],[f230_sk]) ).
fof(f231,axiom,
! [V_n] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n,V_n),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_less__irrefl__nat) ).
fof(f231_nnf,plain,
! [V_n] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n,V_n),
inference(nnf_transformation,[status(thm)],[f231]) ).
fof(f231_sk,plain,
! [V_n] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n,V_n),
inference(skolemisation,[status(esa)],[f231_nnf]) ).
cnf(c353,plain,
~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,X0),
inference(cnf_transformation,[status(esa)],[f231_sk]) ).
fof(f234,axiom,
! [V_n_2,V_m_2] :
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_n_2)
<=> ( V_m_2 != V_n_2
& c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_m_2,V_n_2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_nat__less__le) ).
fof(f234_nnf,plain,
! [V_n_2,V_m_2] :
( ( V_m_2 = V_n_2
| ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_m_2,V_n_2)
| c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_n_2) )
& ( ( V_m_2 != V_n_2
& c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_m_2,V_n_2) )
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_n_2) ) ),
inference(nnf_transformation,[status(thm)],[f234]) ).
fof(f234_sk,plain,
! [V_m_2,V_n_2] :
( ( V_m_2 = V_n_2
| ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_m_2,V_n_2)
| c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_n_2) )
& ( ( V_m_2 != V_n_2
& c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_m_2,V_n_2) )
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_n_2) ) ),
inference(skolemisation,[status(esa)],[f234_nnf]) ).
cnf(c359,plain,
( X1 != X0
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0) ),
inference(cnf_transformation,[status(esa)],[f234_sk]) ).
fof(f235,axiom,
! [V_n] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_less__nat__zero__code) ).
fof(f235_nnf,plain,
! [V_n] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(nnf_transformation,[status(thm)],[f235]) ).
fof(f235_sk,plain,
! [V_n] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(skolemisation,[status(esa)],[f235_nnf]) ).
cnf(c361,plain,
~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(cnf_transformation,[status(esa)],[f235_sk]) ).
fof(f236,axiom,
! [V_n_2,V_m_2] :
( V_m_2 != V_n_2
<=> ( c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n_2,V_m_2)
| c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_n_2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_nat__neq__iff) ).
fof(f236_nnf,plain,
! [V_n_2,V_m_2] :
( ( ( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n_2,V_m_2)
& ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_n_2) )
| V_m_2 != V_n_2 )
& ( c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n_2,V_m_2)
| c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_n_2)
| V_m_2 = V_n_2 ) ),
inference(nnf_transformation,[status(thm)],[f236]) ).
fof(f236_sk,plain,
! [V_m_2,V_n_2] :
( ( ( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n_2,V_m_2)
& ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_n_2) )
| V_m_2 != V_n_2 )
& ( c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n_2,V_m_2)
| c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_n_2)
| V_m_2 = V_n_2 ) ),
inference(skolemisation,[status(esa)],[f236_nnf]) ).
cnf(c363,plain,
( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0)
| X1 != X0 ),
inference(cnf_transformation,[status(esa)],[f236_sk]) ).
cnf(c364,plain,
( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,X1)
| X1 != X0 ),
inference(cnf_transformation,[status(esa)],[f236_sk]) ).
fof(f237,axiom,
! [V_n_2] :
( V_n_2 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
<=> c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),V_n_2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_neq0__conv) ).
fof(f237_nnf,plain,
! [V_n_2] :
( ( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),V_n_2)
| V_n_2 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat) )
& ( c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),V_n_2)
| V_n_2 = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ) ),
inference(nnf_transformation,[status(thm)],[f237]) ).
fof(f237_sk,plain,
! [V_n_2] :
( ( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),V_n_2)
| V_n_2 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat) )
& ( c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),V_n_2)
| V_n_2 = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ) ),
inference(skolemisation,[status(esa)],[f237_nnf]) ).
cnf(c366,plain,
( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),X0)
| X0 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ),
inference(cnf_transformation,[status(esa)],[f237_sk]) ).
fof(f238,axiom,
! [V_n] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n,V_n),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_less__not__refl) ).
fof(f238_nnf,plain,
! [V_n] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n,V_n),
inference(nnf_transformation,[status(thm)],[f238]) ).
fof(f238_sk,plain,
! [V_n] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n,V_n),
inference(skolemisation,[status(esa)],[f238_nnf]) ).
cnf(c367,plain,
~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,X0),
inference(cnf_transformation,[status(esa)],[f238_sk]) ).
fof(f239,axiom,
! [V_n] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_not__less0) ).
fof(f239_nnf,plain,
! [V_n] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(nnf_transformation,[status(thm)],[f239]) ).
fof(f239_sk,plain,
! [V_n] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(skolemisation,[status(esa)],[f239_nnf]) ).
cnf(c368,plain,
~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(cnf_transformation,[status(esa)],[f239_sk]) ).
fof(f271,axiom,
! [V_n_2,V_m_2] :
( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_n_2)
<=> c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n_2,c_Nat_OSuc(V_m_2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_not__less__eq) ).
fof(f271_nnf,plain,
! [V_n_2,V_m_2] :
( ( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n_2,c_Nat_OSuc(V_m_2))
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_n_2) )
& ( c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n_2,c_Nat_OSuc(V_m_2))
| c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_n_2) ) ),
inference(nnf_transformation,[status(thm)],[f271]) ).
fof(f271_sk,plain,
! [V_m_2,V_n_2] :
( ( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n_2,c_Nat_OSuc(V_m_2))
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_n_2) )
& ( c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n_2,c_Nat_OSuc(V_m_2))
| c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_n_2) ) ),
inference(skolemisation,[status(esa)],[f271_nnf]) ).
cnf(c413,plain,
( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,c_Nat_OSuc(X1))
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0) ),
inference(cnf_transformation,[status(esa)],[f271_sk]) ).
fof(f295,axiom,
! [V_i,V_j] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,V_j,V_i),V_i),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_not__add__less2) ).
fof(f295_nnf,plain,
! [V_i,V_j] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,V_j,V_i),V_i),
inference(nnf_transformation,[status(thm)],[f295]) ).
fof(f295_sk,plain,
! [V_j,V_i] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,V_j,V_i),V_i),
inference(skolemisation,[status(esa)],[f295_nnf]) ).
cnf(c459,plain,
~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,X0),X0),
inference(cnf_transformation,[status(esa)],[f295_sk]) ).
fof(f296,axiom,
! [V_j,V_i] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,V_i,V_j),V_i),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_not__add__less1) ).
fof(f296_nnf,plain,
! [V_j,V_i] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,V_i,V_j),V_i),
inference(nnf_transformation,[status(thm)],[f296]) ).
fof(f296_sk,plain,
! [V_i,V_j] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,V_i,V_j),V_i),
inference(skolemisation,[status(esa)],[f296_nnf]) ).
cnf(c460,plain,
~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Oplus__class_Oplus(tc_Nat_Onat,X1,X0),X1),
inference(cnf_transformation,[status(esa)],[f296_sk]) ).
fof(f325,axiom,
! [V_x,T_a] :
( class_Orderings_Opreorder(T_a)
=> ~ c_Orderings_Oord__class_Oless(T_a,V_x,V_x) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_order__less__irrefl) ).
fof(f325_nnf,plain,
! [V_x,T_a] :
( ~ c_Orderings_Oord__class_Oless(T_a,V_x,V_x)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f325]) ).
fof(f325_sk,plain,
! [T_a,V_x] :
( ~ c_Orderings_Oord__class_Oless(T_a,V_x,V_x)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f325_nnf]) ).
cnf(c494,plain,
( ~ c_Orderings_Oord__class_Oless(X1,X0,X0)
| ~ class_Orderings_Opreorder(X1) ),
inference(cnf_transformation,[status(esa)],[f325_sk]) ).
fof(f326,axiom,
! [V_y_2,V_x_2,T_a] :
( class_Orderings_Olinorder(T_a)
=> ( V_x_2 != V_y_2
<=> ( c_Orderings_Oord__class_Oless(T_a,V_y_2,V_x_2)
| c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_linorder__neq__iff) ).
fof(f326_nnf,plain,
! [V_y_2,V_x_2,T_a] :
( ( ( ( ~ c_Orderings_Oord__class_Oless(T_a,V_y_2,V_x_2)
& ~ c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2) )
| V_x_2 != V_y_2 )
& ( c_Orderings_Oord__class_Oless(T_a,V_y_2,V_x_2)
| c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2)
| V_x_2 = V_y_2 ) )
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f326]) ).
fof(f326_sk,plain,
! [T_a,V_x_2,V_y_2] :
( ( ( ( ~ c_Orderings_Oord__class_Oless(T_a,V_y_2,V_x_2)
& ~ c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2) )
| V_x_2 != V_y_2 )
& ( c_Orderings_Oord__class_Oless(T_a,V_y_2,V_x_2)
| c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2)
| V_x_2 = V_y_2 ) )
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f326_nnf]) ).
cnf(c496,plain,
( ~ c_Orderings_Oord__class_Oless(X2,X1,X0)
| X1 != X0
| ~ class_Orderings_Olinorder(X2) ),
inference(cnf_transformation,[status(esa)],[f326_sk]) ).
cnf(c497,plain,
( ~ c_Orderings_Oord__class_Oless(X2,X0,X1)
| X1 != X0
| ~ class_Orderings_Olinorder(X2) ),
inference(cnf_transformation,[status(esa)],[f326_sk]) ).
fof(f327,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)
<=> ( V_x_2 = V_y_2
| c_Orderings_Oord__class_Oless(T_a,V_y_2,V_x_2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_not__less__iff__gr__or__eq) ).
fof(f327_nnf,plain,
! [V_y_2,V_x_2,T_a] :
( ( ( ( V_x_2 != V_y_2
& ~ c_Orderings_Oord__class_Oless(T_a,V_y_2,V_x_2) )
| ~ c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2) )
& ( V_x_2 = V_y_2
| c_Orderings_Oord__class_Oless(T_a,V_y_2,V_x_2)
| c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2) ) )
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f327]) ).
fof(f327_sk,plain,
! [T_a,V_x_2,V_y_2] :
( ( ( ( V_x_2 != V_y_2
& ~ c_Orderings_Oord__class_Oless(T_a,V_y_2,V_x_2) )
| ~ c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2) )
& ( V_x_2 = V_y_2
| c_Orderings_Oord__class_Oless(T_a,V_y_2,V_x_2)
| c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2) ) )
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f327_nnf]) ).
cnf(c499,plain,
( ~ c_Orderings_Oord__class_Oless(X2,X0,X1)
| ~ c_Orderings_Oord__class_Oless(X2,X1,X0)
| ~ class_Orderings_Olinorder(X2) ),
inference(cnf_transformation,[status(esa)],[f327_sk]) ).
cnf(c500,plain,
( X1 != X0
| ~ c_Orderings_Oord__class_Oless(X2,X1,X0)
| ~ class_Orderings_Olinorder(X2) ),
inference(cnf_transformation,[status(esa)],[f327_sk]) ).
fof(f331,axiom,
! [V_y,V_x,T_a] :
( class_Orderings_Oorder(T_a)
=> ( c_Orderings_Oord__class_Oless(T_a,V_x,V_y)
=> V_x != V_y ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_less__imp__neq) ).
fof(f331_nnf,plain,
! [V_y,V_x,T_a] :
( V_x != V_y
| ~ c_Orderings_Oord__class_Oless(T_a,V_x,V_y)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f331]) ).
fof(f331_sk,plain,
! [T_a,V_x,V_y] :
( V_x != V_y
| ~ c_Orderings_Oord__class_Oless(T_a,V_x,V_y)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f331_nnf]) ).
cnf(c505,plain,
( X1 != X0
| ~ c_Orderings_Oord__class_Oless(X2,X1,X0)
| ~ class_Orderings_Oorder(X2) ),
inference(cnf_transformation,[status(esa)],[f331_sk]) ).
fof(f332,axiom,
! [V_y,V_x,T_a] :
( class_Orderings_Opreorder(T_a)
=> ( c_Orderings_Oord__class_Oless(T_a,V_x,V_y)
=> ~ c_Orderings_Oord__class_Oless(T_a,V_y,V_x) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_order__less__not__sym) ).
fof(f332_nnf,plain,
! [V_y,V_x,T_a] :
( ~ c_Orderings_Oord__class_Oless(T_a,V_y,V_x)
| ~ c_Orderings_Oord__class_Oless(T_a,V_x,V_y)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f332]) ).
fof(f332_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_Orderings_Oord__class_Oless(T_a,V_y,V_x)
| ~ c_Orderings_Oord__class_Oless(T_a,V_x,V_y)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f332_nnf]) ).
cnf(c506,plain,
( ~ c_Orderings_Oord__class_Oless(X2,X0,X1)
| ~ c_Orderings_Oord__class_Oless(X2,X1,X0)
| ~ class_Orderings_Opreorder(X2) ),
inference(cnf_transformation,[status(esa)],[f332_sk]) ).
fof(f333,axiom,
! [V_y,V_x,T_a] :
( class_Orderings_Opreorder(T_a)
=> ( c_Orderings_Oord__class_Oless(T_a,V_x,V_y)
=> ~ c_Orderings_Oord__class_Oless(T_a,V_y,V_x) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_order__less__imp__not__less) ).
fof(f333_nnf,plain,
! [V_y,V_x,T_a] :
( ~ c_Orderings_Oord__class_Oless(T_a,V_y,V_x)
| ~ c_Orderings_Oord__class_Oless(T_a,V_x,V_y)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f333]) ).
fof(f333_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_Orderings_Oord__class_Oless(T_a,V_y,V_x)
| ~ c_Orderings_Oord__class_Oless(T_a,V_x,V_y)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f333_nnf]) ).
cnf(c507,plain,
( ~ c_Orderings_Oord__class_Oless(X2,X0,X1)
| ~ c_Orderings_Oord__class_Oless(X2,X1,X0)
| ~ class_Orderings_Opreorder(X2) ),
inference(cnf_transformation,[status(esa)],[f333_sk]) ).
fof(f334,axiom,
! [V_y,V_x,T_a] :
( class_Orderings_Oorder(T_a)
=> ( c_Orderings_Oord__class_Oless(T_a,V_x,V_y)
=> V_x != V_y ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_order__less__imp__not__eq) ).
fof(f334_nnf,plain,
! [V_y,V_x,T_a] :
( V_x != V_y
| ~ c_Orderings_Oord__class_Oless(T_a,V_x,V_y)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f334]) ).
fof(f334_sk,plain,
! [T_a,V_x,V_y] :
( V_x != V_y
| ~ c_Orderings_Oord__class_Oless(T_a,V_x,V_y)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f334_nnf]) ).
cnf(c508,plain,
( X1 != X0
| ~ c_Orderings_Oord__class_Oless(X2,X1,X0)
| ~ class_Orderings_Oorder(X2) ),
inference(cnf_transformation,[status(esa)],[f334_sk]) ).
fof(f335,axiom,
! [V_y,V_x,T_a] :
( class_Orderings_Oorder(T_a)
=> ( c_Orderings_Oord__class_Oless(T_a,V_x,V_y)
=> V_y != V_x ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_order__less__imp__not__eq2) ).
fof(f335_nnf,plain,
! [V_y,V_x,T_a] :
( V_y != V_x
| ~ c_Orderings_Oord__class_Oless(T_a,V_x,V_y)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f335]) ).
fof(f335_sk,plain,
! [T_a,V_x,V_y] :
( V_y != V_x
| ~ c_Orderings_Oord__class_Oless(T_a,V_x,V_y)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f335_nnf]) ).
cnf(c509,plain,
( X0 != X1
| ~ c_Orderings_Oord__class_Oless(X2,X1,X0)
| ~ class_Orderings_Oorder(X2) ),
inference(cnf_transformation,[status(esa)],[f335_sk]) ).
fof(f336,axiom,
! [V_b,V_a,T_a] :
( class_Orderings_Opreorder(T_a)
=> ( c_Orderings_Oord__class_Oless(T_a,V_a,V_b)
=> ~ c_Orderings_Oord__class_Oless(T_a,V_b,V_a) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_order__less__asym_H) ).
fof(f336_nnf,plain,
! [V_b,V_a,T_a] :
( ~ c_Orderings_Oord__class_Oless(T_a,V_b,V_a)
| ~ c_Orderings_Oord__class_Oless(T_a,V_a,V_b)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f336]) ).
fof(f336_sk,plain,
! [T_a,V_a,V_b] :
( ~ c_Orderings_Oord__class_Oless(T_a,V_b,V_a)
| ~ c_Orderings_Oord__class_Oless(T_a,V_a,V_b)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f336_nnf]) ).
cnf(c510,plain,
( ~ c_Orderings_Oord__class_Oless(X2,X0,X1)
| ~ c_Orderings_Oord__class_Oless(X2,X1,X0)
| ~ class_Orderings_Opreorder(X2) ),
inference(cnf_transformation,[status(esa)],[f336_sk]) ).
fof(f337,axiom,
! [V_a,V_b,T_a] :
( class_Orderings_Oorder(T_a)
=> ( c_Orderings_Oord__class_Oless(T_a,V_b,V_a)
=> ~ c_Orderings_Oord__class_Oless(T_a,V_a,V_b) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_xt1_I9_J) ).
fof(f337_nnf,plain,
! [V_a,V_b,T_a] :
( ~ c_Orderings_Oord__class_Oless(T_a,V_a,V_b)
| ~ c_Orderings_Oord__class_Oless(T_a,V_b,V_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f337]) ).
fof(f337_sk,plain,
! [T_a,V_b,V_a] :
( ~ c_Orderings_Oord__class_Oless(T_a,V_a,V_b)
| ~ c_Orderings_Oord__class_Oless(T_a,V_b,V_a)
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f337_nnf]) ).
cnf(c511,plain,
( ~ c_Orderings_Oord__class_Oless(X2,X0,X1)
| ~ c_Orderings_Oord__class_Oless(X2,X1,X0)
| ~ class_Orderings_Oorder(X2) ),
inference(cnf_transformation,[status(esa)],[f337_sk]) ).
fof(f344,axiom,
! [V_y,V_x,T_a] :
( class_Orderings_Opreorder(T_a)
=> ( c_Orderings_Oord__class_Oless(T_a,V_x,V_y)
=> ~ c_Orderings_Oord__class_Oless(T_a,V_y,V_x) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_order__less__asym) ).
fof(f344_nnf,plain,
! [V_y,V_x,T_a] :
( ~ c_Orderings_Oord__class_Oless(T_a,V_y,V_x)
| ~ c_Orderings_Oord__class_Oless(T_a,V_x,V_y)
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f344]) ).
fof(f344_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_Orderings_Oord__class_Oless(T_a,V_y,V_x)
| ~ c_Orderings_Oord__class_Oless(T_a,V_x,V_y)
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f344_nnf]) ).
cnf(c518,plain,
( ~ c_Orderings_Oord__class_Oless(X2,X0,X1)
| ~ c_Orderings_Oord__class_Oless(X2,X1,X0)
| ~ class_Orderings_Opreorder(X2) ),
inference(cnf_transformation,[status(esa)],[f344_sk]) ).
fof(f348,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('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_linorder__not__less) ).
fof(f348_nnf,plain,
! [V_y_2,V_x_2,T_a] :
( ( ( ~ c_Orderings_Oord__class_Oless__eq(T_a,V_y_2,V_x_2)
| ~ 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)
| c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2) ) )
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f348]) ).
fof(f348_sk,plain,
! [T_a,V_x_2,V_y_2] :
( ( ( ~ c_Orderings_Oord__class_Oless__eq(T_a,V_y_2,V_x_2)
| ~ 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)
| c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2) ) )
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f348_nnf]) ).
cnf(c525,plain,
( ~ c_Orderings_Oord__class_Oless__eq(X2,X0,X1)
| ~ c_Orderings_Oord__class_Oless(X2,X1,X0)
| ~ class_Orderings_Olinorder(X2) ),
inference(cnf_transformation,[status(esa)],[f348_sk]) ).
fof(f349,axiom,
! [V_y_2,V_x_2,T_a] :
( class_Orderings_Olinorder(T_a)
=> ( ~ c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2)
<=> c_Orderings_Oord__class_Oless(T_a,V_y_2,V_x_2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_linorder__not__le) ).
fof(f349_nnf,plain,
! [V_y_2,V_x_2,T_a] :
( ( ( ~ c_Orderings_Oord__class_Oless(T_a,V_y_2,V_x_2)
| ~ c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2) )
& ( c_Orderings_Oord__class_Oless(T_a,V_y_2,V_x_2)
| c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2) ) )
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f349]) ).
fof(f349_sk,plain,
! [T_a,V_x_2,V_y_2] :
( ( ( ~ c_Orderings_Oord__class_Oless(T_a,V_y_2,V_x_2)
| ~ c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2) )
& ( c_Orderings_Oord__class_Oless(T_a,V_y_2,V_x_2)
| c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2) ) )
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f349_nnf]) ).
cnf(c527,plain,
( ~ c_Orderings_Oord__class_Oless(X2,X0,X1)
| ~ c_Orderings_Oord__class_Oless__eq(X2,X1,X0)
| ~ class_Orderings_Olinorder(X2) ),
inference(cnf_transformation,[status(esa)],[f349_sk]) ).
fof(f351,axiom,
! [V_y_2,V_x_2,T_a] :
( class_Orderings_Oorder(T_a)
=> ( c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2)
<=> ( V_x_2 != V_y_2
& c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_order__less__le) ).
fof(f351_nnf,plain,
! [V_y_2,V_x_2,T_a] :
( ( ( V_x_2 = V_y_2
| ~ c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2)
| c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2) )
& ( ( V_x_2 != V_y_2
& c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2) )
| ~ c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2) ) )
| ~ class_Orderings_Oorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f351]) ).
fof(f351_sk,plain,
! [T_a,V_x_2,V_y_2] :
( ( ( V_x_2 = V_y_2
| ~ c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2)
| c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2) )
& ( ( V_x_2 != V_y_2
& c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2) )
| ~ c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2) ) )
| ~ class_Orderings_Oorder(T_a) ),
inference(skolemisation,[status(esa)],[f351_nnf]) ).
cnf(c530,plain,
( X1 != X0
| ~ c_Orderings_Oord__class_Oless(X2,X1,X0)
| ~ class_Orderings_Oorder(X2) ),
inference(cnf_transformation,[status(esa)],[f351_sk]) ).
fof(f352,axiom,
! [V_y_2,V_x_2,T_a] :
( class_Orderings_Opreorder(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)
& c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_less__le__not__le) ).
fof(f352_nnf,plain,
! [V_y_2,V_x_2,T_a] :
( ( ( c_Orderings_Oord__class_Oless__eq(T_a,V_y_2,V_x_2)
| ~ c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2)
| 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)
& c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2) )
| ~ c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2) ) )
| ~ class_Orderings_Opreorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f352]) ).
fof(f352_sk,plain,
! [T_a,V_x_2,V_y_2] :
( ( ( c_Orderings_Oord__class_Oless__eq(T_a,V_y_2,V_x_2)
| ~ c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2)
| 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)
& c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2) )
| ~ c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2) ) )
| ~ class_Orderings_Opreorder(T_a) ),
inference(skolemisation,[status(esa)],[f352_nnf]) ).
cnf(c533,plain,
( ~ c_Orderings_Oord__class_Oless__eq(X2,X0,X1)
| ~ c_Orderings_Oord__class_Oless(X2,X1,X0)
| ~ class_Orderings_Opreorder(X2) ),
inference(cnf_transformation,[status(esa)],[f352_sk]) ).
fof(f359,axiom,
! [V_x,V_y,T_a] :
( class_Orderings_Olinorder(T_a)
=> ( c_Orderings_Oord__class_Oless__eq(T_a,V_y,V_x)
=> ~ c_Orderings_Oord__class_Oless(T_a,V_x,V_y) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_leD) ).
fof(f359_nnf,plain,
! [V_x,V_y,T_a] :
( ~ c_Orderings_Oord__class_Oless(T_a,V_x,V_y)
| ~ c_Orderings_Oord__class_Oless__eq(T_a,V_y,V_x)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f359]) ).
fof(f359_sk,plain,
! [T_a,V_y,V_x] :
( ~ c_Orderings_Oord__class_Oless(T_a,V_x,V_y)
| ~ c_Orderings_Oord__class_Oless__eq(T_a,V_y,V_x)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f359_nnf]) ).
cnf(c544,plain,
( ~ c_Orderings_Oord__class_Oless(X2,X0,X1)
| ~ c_Orderings_Oord__class_Oless__eq(X2,X1,X0)
| ~ class_Orderings_Olinorder(X2) ),
inference(cnf_transformation,[status(esa)],[f359_sk]) ).
fof(f361,axiom,
! [V_y_2,V_x_2,T_a] :
( class_Orderings_Olinorder(T_a)
=> ( c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2)
=> ( ~ c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2)
<=> V_x_2 = V_y_2 ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_linorder__antisym__conv2) ).
fof(f361_nnf,plain,
! [V_y_2,V_x_2,T_a] :
( ( ( V_x_2 != V_y_2
| ~ c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2) )
& ( V_x_2 = V_y_2
| c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2) ) )
| ~ c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2)
| ~ class_Orderings_Olinorder(T_a) ),
inference(nnf_transformation,[status(thm)],[f361]) ).
fof(f361_sk,plain,
! [T_a,V_x_2,V_y_2] :
( ( ( V_x_2 != V_y_2
| ~ c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2) )
& ( V_x_2 = V_y_2
| c_Orderings_Oord__class_Oless(T_a,V_x_2,V_y_2) ) )
| ~ c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,V_y_2)
| ~ class_Orderings_Olinorder(T_a) ),
inference(skolemisation,[status(esa)],[f361_nnf]) ).
cnf(c547,plain,
( X1 != X0
| ~ c_Orderings_Oord__class_Oless(X2,X1,X0)
| ~ c_Orderings_Oord__class_Oless__eq(X2,X1,X0)
| ~ class_Orderings_Olinorder(X2) ),
inference(cnf_transformation,[status(esa)],[f361_sk]) ).
fof(f379,axiom,
! [V_g_2,V_f_2,T_a,T_b] :
( class_Orderings_Oord(T_b)
=> ( c_Orderings_Oord__class_Oless(tc_fun(T_a,T_b),V_f_2,V_g_2)
<=> ( ~ c_Orderings_Oord__class_Oless__eq(tc_fun(T_a,T_b),V_g_2,V_f_2)
& c_Orderings_Oord__class_Oless__eq(tc_fun(T_a,T_b),V_f_2,V_g_2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_less__fun__def) ).
fof(f379_nnf,plain,
! [V_g_2,V_f_2,T_a,T_b] :
( ( ( c_Orderings_Oord__class_Oless__eq(tc_fun(T_a,T_b),V_g_2,V_f_2)
| ~ c_Orderings_Oord__class_Oless__eq(tc_fun(T_a,T_b),V_f_2,V_g_2)
| c_Orderings_Oord__class_Oless(tc_fun(T_a,T_b),V_f_2,V_g_2) )
& ( ( ~ c_Orderings_Oord__class_Oless__eq(tc_fun(T_a,T_b),V_g_2,V_f_2)
& c_Orderings_Oord__class_Oless__eq(tc_fun(T_a,T_b),V_f_2,V_g_2) )
| ~ c_Orderings_Oord__class_Oless(tc_fun(T_a,T_b),V_f_2,V_g_2) ) )
| ~ class_Orderings_Oord(T_b) ),
inference(nnf_transformation,[status(thm)],[f379]) ).
fof(f379_sk,plain,
! [T_b,T_a,V_f_2,V_g_2] :
( ( ( c_Orderings_Oord__class_Oless__eq(tc_fun(T_a,T_b),V_g_2,V_f_2)
| ~ c_Orderings_Oord__class_Oless__eq(tc_fun(T_a,T_b),V_f_2,V_g_2)
| c_Orderings_Oord__class_Oless(tc_fun(T_a,T_b),V_f_2,V_g_2) )
& ( ( ~ c_Orderings_Oord__class_Oless__eq(tc_fun(T_a,T_b),V_g_2,V_f_2)
& c_Orderings_Oord__class_Oless__eq(tc_fun(T_a,T_b),V_f_2,V_g_2) )
| ~ c_Orderings_Oord__class_Oless(tc_fun(T_a,T_b),V_f_2,V_g_2) ) )
| ~ class_Orderings_Oord(T_b) ),
inference(skolemisation,[status(esa)],[f379_nnf]) ).
cnf(c573,plain,
( ~ c_Orderings_Oord__class_Oless__eq(tc_fun(X2,X3),X0,X1)
| ~ c_Orderings_Oord__class_Oless(tc_fun(X2,X3),X1,X0)
| ~ class_Orderings_Oord(X3) ),
inference(cnf_transformation,[status(esa)],[f379_sk]) ).
fof(f592,axiom,
! [V_a,T_a] :
( class_Rings_Olinordered__ring(T_a)
=> ~ c_Orderings_Oord__class_Oless(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_a),V_a),c_Groups_Ozero__class_Ozero(T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_not__square__less__zero) ).
fof(f592_nnf,plain,
! [V_a,T_a] :
( ~ c_Orderings_Oord__class_Oless(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_a),V_a),c_Groups_Ozero__class_Ozero(T_a))
| ~ class_Rings_Olinordered__ring(T_a) ),
inference(nnf_transformation,[status(thm)],[f592]) ).
fof(f592_sk,plain,
! [T_a,V_a] :
( ~ c_Orderings_Oord__class_Oless(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_a),V_a),c_Groups_Ozero__class_Ozero(T_a))
| ~ class_Rings_Olinordered__ring(T_a) ),
inference(skolemisation,[status(esa)],[f592_nnf]) ).
cnf(c860,plain,
( ~ c_Orderings_Oord__class_Oless(X1,hAPP(hAPP(c_Groups_Otimes__class_Otimes(X1),X0),X0),c_Groups_Ozero__class_Ozero(X1))
| ~ class_Rings_Olinordered__ring(X1) ),
inference(cnf_transformation,[status(esa)],[f592_sk]) ).
fof(f658,axiom,
! [V_y_2,V_x_2,T_a] :
( class_Rings_Olinordered__ring__strict(T_a)
=> ( c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),c_Groups_Oplus__class_Oplus(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x_2),V_x_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_y_2),V_y_2)))
<=> ( V_y_2 != c_Groups_Ozero__class_Ozero(T_a)
| V_x_2 != c_Groups_Ozero__class_Ozero(T_a) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_sum__squares__gt__zero__iff) ).
fof(f658_nnf,plain,
! [V_y_2,V_x_2,T_a] :
( ( ( ( V_y_2 = c_Groups_Ozero__class_Ozero(T_a)
& V_x_2 = c_Groups_Ozero__class_Ozero(T_a) )
| c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),c_Groups_Oplus__class_Oplus(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x_2),V_x_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_y_2),V_y_2))) )
& ( V_y_2 != c_Groups_Ozero__class_Ozero(T_a)
| V_x_2 != c_Groups_Ozero__class_Ozero(T_a)
| ~ c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),c_Groups_Oplus__class_Oplus(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x_2),V_x_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_y_2),V_y_2))) ) )
| ~ class_Rings_Olinordered__ring__strict(T_a) ),
inference(nnf_transformation,[status(thm)],[f658]) ).
fof(f658_sk,plain,
! [T_a,V_x_2,V_y_2] :
( ( ( ( V_y_2 = c_Groups_Ozero__class_Ozero(T_a)
& V_x_2 = c_Groups_Ozero__class_Ozero(T_a) )
| c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),c_Groups_Oplus__class_Oplus(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x_2),V_x_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_y_2),V_y_2))) )
& ( V_y_2 != c_Groups_Ozero__class_Ozero(T_a)
| V_x_2 != c_Groups_Ozero__class_Ozero(T_a)
| ~ c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),c_Groups_Oplus__class_Oplus(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x_2),V_x_2),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_y_2),V_y_2))) ) )
| ~ class_Rings_Olinordered__ring__strict(T_a) ),
inference(skolemisation,[status(esa)],[f658_nnf]) ).
cnf(c970,plain,
( X0 != c_Groups_Ozero__class_Ozero(X2)
| X1 != c_Groups_Ozero__class_Ozero(X2)
| ~ c_Orderings_Oord__class_Oless(X2,c_Groups_Ozero__class_Ozero(X2),c_Groups_Oplus__class_Oplus(X2,hAPP(hAPP(c_Groups_Otimes__class_Otimes(X2),X1),X1),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X2),X0),X0)))
| ~ class_Rings_Olinordered__ring__strict(X2) ),
inference(cnf_transformation,[status(esa)],[f658_sk]) ).
fof(f659,axiom,
! [V_y,V_x,T_a] :
( class_Rings_Olinordered__ring(T_a)
=> ~ c_Orderings_Oord__class_Oless(T_a,c_Groups_Oplus__class_Oplus(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x),V_x),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_y),V_y)),c_Groups_Ozero__class_Ozero(T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_not__sum__squares__lt__zero) ).
fof(f659_nnf,plain,
! [V_y,V_x,T_a] :
( ~ c_Orderings_Oord__class_Oless(T_a,c_Groups_Oplus__class_Oplus(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x),V_x),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_y),V_y)),c_Groups_Ozero__class_Ozero(T_a))
| ~ class_Rings_Olinordered__ring(T_a) ),
inference(nnf_transformation,[status(thm)],[f659]) ).
fof(f659_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_Orderings_Oord__class_Oless(T_a,c_Groups_Oplus__class_Oplus(T_a,hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_x),V_x),hAPP(hAPP(c_Groups_Otimes__class_Otimes(T_a),V_y),V_y)),c_Groups_Ozero__class_Ozero(T_a))
| ~ class_Rings_Olinordered__ring(T_a) ),
inference(skolemisation,[status(esa)],[f659_nnf]) ).
cnf(c973,plain,
( ~ c_Orderings_Oord__class_Oless(X2,c_Groups_Oplus__class_Oplus(X2,hAPP(hAPP(c_Groups_Otimes__class_Otimes(X2),X1),X1),hAPP(hAPP(c_Groups_Otimes__class_Otimes(X2),X0),X0)),c_Groups_Ozero__class_Ozero(X2))
| ~ class_Rings_Olinordered__ring(X2) ),
inference(cnf_transformation,[status(esa)],[f659_sk]) ).
fof(f731,axiom,
! [V_x_2] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_x_2),V_x_2))
<=> V_x_2 = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_not__real__square__gt__zero) ).
fof(f731_nnf,plain,
! [V_x_2] :
( ( V_x_2 != c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_x_2),V_x_2)) )
& ( V_x_2 = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_x_2),V_x_2)) ) ),
inference(nnf_transformation,[status(thm)],[f731]) ).
fof(f731_sk,plain,
! [V_x_2] :
( ( V_x_2 != c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_x_2),V_x_2)) )
& ( V_x_2 = c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),V_x_2),V_x_2)) ) ),
inference(skolemisation,[status(esa)],[f731_nnf]) ).
cnf(c1130,plain,
( X0 != c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal)
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),hAPP(hAPP(c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal),X0),X0)) ),
inference(cnf_transformation,[status(esa)],[f731_sk]) ).
fof(f780,axiom,
! [V_n_2,V_a_2,T_a] :
( ( class_Rings_Ozero__neq__one(T_a)
& class_Rings_Ono__zero__divisors(T_a)
& class_Rings_Omult__zero(T_a)
& class_Power_Opower(T_a) )
=> ( hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_a_2),V_n_2) = c_Groups_Ozero__class_Ozero(T_a)
<=> ( V_n_2 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
& V_a_2 = c_Groups_Ozero__class_Ozero(T_a) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_power__eq__0__iff) ).
fof(f780_nnf,plain,
! [V_n_2,V_a_2,T_a] :
( ( ( V_n_2 = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| V_a_2 != c_Groups_Ozero__class_Ozero(T_a)
| hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_a_2),V_n_2) = c_Groups_Ozero__class_Ozero(T_a) )
& ( ( V_n_2 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
& V_a_2 = c_Groups_Ozero__class_Ozero(T_a) )
| hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_a_2),V_n_2) != c_Groups_Ozero__class_Ozero(T_a) ) )
| ~ class_Rings_Ozero__neq__one(T_a)
| ~ class_Rings_Ono__zero__divisors(T_a)
| ~ class_Rings_Omult__zero(T_a)
| ~ class_Power_Opower(T_a) ),
inference(nnf_transformation,[status(thm)],[f780]) ).
fof(f780_sk,plain,
! [T_a,V_a_2,V_n_2] :
( ( ( V_n_2 = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| V_a_2 != c_Groups_Ozero__class_Ozero(T_a)
| hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_a_2),V_n_2) = c_Groups_Ozero__class_Ozero(T_a) )
& ( ( V_n_2 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
& V_a_2 = c_Groups_Ozero__class_Ozero(T_a) )
| hAPP(hAPP(c_Power_Opower__class_Opower(T_a),V_a_2),V_n_2) != c_Groups_Ozero__class_Ozero(T_a) ) )
| ~ class_Rings_Ozero__neq__one(T_a)
| ~ class_Rings_Ono__zero__divisors(T_a)
| ~ class_Rings_Omult__zero(T_a)
| ~ class_Power_Opower(T_a) ),
inference(skolemisation,[status(esa)],[f780_nnf]) ).
cnf(c1198,plain,
( X0 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| hAPP(hAPP(c_Power_Opower__class_Opower(X2),X1),X0) != c_Groups_Ozero__class_Ozero(X2)
| ~ class_Rings_Ozero__neq__one(X2)
| ~ class_Rings_Ono__zero__divisors(X2)
| ~ class_Rings_Omult__zero(X2)
| ~ class_Power_Opower(X2) ),
inference(cnf_transformation,[status(esa)],[f780_sk]) ).
fof(f861,axiom,
c_Groups_Ozero__class_Ozero(tc_Int_Oint) != c_Groups_Oone__class_Oone(tc_Int_Oint),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_int__0__neq__1) ).
fof(f861_nnf,plain,
c_Groups_Ozero__class_Ozero(tc_Int_Oint) != c_Groups_Oone__class_Oone(tc_Int_Oint),
inference(nnf_transformation,[status(thm)],[f861]) ).
fof(f861_sk,plain,
c_Groups_Ozero__class_Ozero(tc_Int_Oint) != c_Groups_Oone__class_Oone(tc_Int_Oint),
inference(skolemisation,[status(esa)],[f861_nnf]) ).
cnf(c1412,plain,
c_Groups_Ozero__class_Ozero(tc_Int_Oint) != c_Groups_Oone__class_Oone(tc_Int_Oint),
inference(cnf_transformation,[status(esa)],[f861_sk]) ).
fof(f862,axiom,
! [V_z] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),V_z),V_z) != c_Groups_Ozero__class_Ozero(tc_Int_Oint),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_odd__nonzero) ).
fof(f862_nnf,plain,
! [V_z] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),V_z),V_z) != c_Groups_Ozero__class_Ozero(tc_Int_Oint),
inference(nnf_transformation,[status(thm)],[f862]) ).
fof(f862_sk,plain,
! [V_z] : c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),V_z),V_z) != c_Groups_Ozero__class_Ozero(tc_Int_Oint),
inference(skolemisation,[status(esa)],[f862_nnf]) ).
cnf(c1413,plain,
c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint),X0),X0) != c_Groups_Ozero__class_Ozero(tc_Int_Oint),
inference(cnf_transformation,[status(esa)],[f862_sk]) ).
fof(f900,axiom,
! [V_w_2,V_z_2] :
( c_Orderings_Oord__class_Oless(tc_Int_Oint,V_z_2,V_w_2)
<=> ( V_z_2 != V_w_2
& c_Orderings_Oord__class_Oless__eq(tc_Int_Oint,V_z_2,V_w_2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_zless__le) ).
fof(f900_nnf,plain,
! [V_w_2,V_z_2] :
( ( V_z_2 = V_w_2
| ~ c_Orderings_Oord__class_Oless__eq(tc_Int_Oint,V_z_2,V_w_2)
| c_Orderings_Oord__class_Oless(tc_Int_Oint,V_z_2,V_w_2) )
& ( ( V_z_2 != V_w_2
& c_Orderings_Oord__class_Oless__eq(tc_Int_Oint,V_z_2,V_w_2) )
| ~ c_Orderings_Oord__class_Oless(tc_Int_Oint,V_z_2,V_w_2) ) ),
inference(nnf_transformation,[status(thm)],[f900]) ).
fof(f900_sk,plain,
! [V_z_2,V_w_2] :
( ( V_z_2 = V_w_2
| ~ c_Orderings_Oord__class_Oless__eq(tc_Int_Oint,V_z_2,V_w_2)
| c_Orderings_Oord__class_Oless(tc_Int_Oint,V_z_2,V_w_2) )
& ( ( V_z_2 != V_w_2
& c_Orderings_Oord__class_Oless__eq(tc_Int_Oint,V_z_2,V_w_2) )
| ~ c_Orderings_Oord__class_Oless(tc_Int_Oint,V_z_2,V_w_2) ) ),
inference(skolemisation,[status(esa)],[f900_nnf]) ).
cnf(c1455,plain,
( X1 != X0
| ~ c_Orderings_Oord__class_Oless(tc_Int_Oint,X1,X0) ),
inference(cnf_transformation,[status(esa)],[f900_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c36,c39,c79,c87,c123,c204,c205,c257,c259,c305,c318,c319,c320,c321,c322,c323,c324,c325,c335,c336,c350,c351,c352,c353,c359,c361,c363,c364,c366,c367,c368,c413,c459,c460,c494,c496,c497,c499,c500,c505,c506,c507,c508,c509,c510,c511,c518,c525,c527,c530,c533,c544,c547,c573,c860,c970,c973,c1130,c1198,c1412,c1413,c1455,c1855]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t163]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWW219+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.03 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.08/0.36 % Computer : n015.cluster.edu
% 0.08/0.36 % Model : x86_64 x86_64
% 0.08/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.36 % Memory : 8046.5625MB
% 0.08/0.36 % OS : Linux 6.8.0-71-generic
% 0.08/0.36 % CPULimit : 300
% 0.08/0.36 % WCLimit : 300
% 0.08/0.36 % DateTime : Thu Sep 24 21:49:12 UTC 2026
% 0.08/0.36 % CPUTime :
% 0.08/0.36 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 99.72/14.51 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 99.72/14.51 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------