%------------------------------------------------------------------------------
% File : FindProof---0.1
% Problem : SWW196+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:48 PM UTC 2026
% Result : Theorem 66.08s 11.61s
% Output : Proof 66.08s
% Verified :
% SZS Type : Refutation
% Derivation depth : 9
% Number of leaves : 85
% Syntax : Number of formulae : 353 ( 176 unt; 0 def)
% Number of atoms : 815 ( 299 equ)
% Maximal formula atoms : 13 ( 2 avg)
% Number of connectives : 1029 ( 567 ~; 293 |; 112 &)
% ( 26 <=>; 31 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 21 ( 19 usr; 2 prp; 0-3 aty)
% Number of functors : 25 ( 25 usr; 10 con; 0-4 aty)
% Number of variables : 466 ( 36 sgn 338 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1170,hypothesis,
( ? [B_m] : v_na____ = c_Groups_Otimes__class_Otimes(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),B_m)
=> v_thesis____ ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
fof(f1170_nnf,plain,
( v_thesis____
| ! [B_m] : v_na____ != c_Groups_Otimes__class_Otimes(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),B_m) ),
inference(nnf_transformation,[status(thm)],[f1170]) ).
fof(f1170_sk,plain,
! [B_m] :
( v_thesis____
| v_na____ != c_Groups_Otimes__class_Otimes(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),B_m) ),
inference(skolemisation,[status(esa)],[f1170_nnf]) ).
cnf(c1692,plain,
( v_thesis____
| v_na____ != c_Groups_Otimes__class_Otimes(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),X0) ),
inference(cnf_transformation,[status(esa)],[f1170_sk]) ).
cnf(hi1572,axiom,
ifeq(v_na____,c_Groups_Otimes__class_Otimes(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),X0),v_thesis____,true) = true,
inference(equality_encoding,[status(esa)],[c1692]) ).
fof(f0,axiom,
? [B_m] : v_na____ = c_Groups_Otimes__class_Otimes(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),B_m),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact__096EX_Am_O_An_A_061_A2_A_K_Am_096) ).
fof(f0_nnf,plain,
? [B_m] : v_na____ = c_Groups_Otimes__class_Otimes(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),B_m),
inference(nnf_transformation,[status(thm)],[f0]) ).
fof(f0_sk,plain,
v_na____ = c_Groups_Otimes__class_Otimes(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),sk0),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk0])],[f0_nnf]) ).
cnf(c0,plain,
v_na____ = c_Groups_Otimes__class_Otimes(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),sk0),
inference(cnf_transformation,[status(esa)],[f0_sk]) ).
cnf(hi0,axiom,
v_na____ = c_Groups_Otimes__class_Otimes(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),sk0),
inference(equality_encoding,[status(esa)],[c0]) ).
fof(f700,axiom,
! [V_k] : c_Int_OBit1(V_k) = 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_k),V_k),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Bit1__def) ).
fof(f700_nnf,plain,
! [V_k] : c_Int_OBit1(V_k) = 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_k),V_k),
inference(nnf_transformation,[status(thm)],[f700]) ).
fof(f700_sk,plain,
! [V_k] : c_Int_OBit1(V_k) = 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_k),V_k),
inference(skolemisation,[status(esa)],[f700_nnf]) ).
cnf(c1066,plain,
c_Int_OBit1(X0) = 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),
inference(cnf_transformation,[status(esa)],[f700_sk]) ).
cnf(hi1,axiom,
c_Int_OBit1(X0) = 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),
inference(equality_encoding,[status(esa)],[c1066]) ).
fof(f303,axiom,
! [V_k] : c_Int_OBit0(V_k) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,V_k,V_k),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Bit0__def) ).
fof(f303_nnf,plain,
! [V_k] : c_Int_OBit0(V_k) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,V_k,V_k),
inference(nnf_transformation,[status(thm)],[f303]) ).
fof(f303_sk,plain,
! [V_k] : c_Int_OBit0(V_k) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,V_k,V_k),
inference(skolemisation,[status(esa)],[f303_nnf]) ).
cnf(c466,plain,
c_Int_OBit0(X0) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,X0),
inference(cnf_transformation,[status(esa)],[f303_sk]) ).
cnf(hi2,axiom,
c_Int_OBit0(X0) = c_Groups_Oplus__class_Oplus(tc_Int_Oint,X0,X0),
inference(equality_encoding,[status(esa)],[c466]) ).
cnf(h24,plain,
v_thesis____ = true,
inference(hyper_resolution,[status(thm)],[hi1572,hi0,hi1,hi2]) ).
fof(f1171,conjecture,
v_thesis____,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_1) ).
fof(f1171_neg,negated_conjecture,
~ v_thesis____,
inference(negated_conjecture,[status(cth)],[f1171]) ).
fof(f1171_nnf,plain,
~ v_thesis____,
inference(nnf_transformation,[status(thm)],[f1171_neg]) ).
fof(f1171_sk,plain,
~ v_thesis____,
inference(skolemisation,[status(esa)],[f1171_nnf]) ).
cnf(c1693,plain,
~ v_thesis____,
inference(cnf_transformation,[status(esa)],[f1171_sk]) ).
cnf(hi1654,negated_conjecture,
ifeq(v_thesis____,true,false,true) = true,
inference(equality_encoding,[status(esa)],[c1693]) ).
cnf(t0,plain,
true = false,
inference(hyper_resolution,[status(thm)],[hi1654,h24]) ).
cnf(t164,plain,
false = true,
inference(orient,[status(thm)],[t0]) ).
fof(f1,axiom,
v_na____ != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_n) ).
fof(f1_nnf,plain,
v_na____ != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(nnf_transformation,[status(thm)],[f1]) ).
fof(f1_sk,plain,
v_na____ != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(skolemisation,[status(esa)],[f1_nnf]) ).
cnf(c1,plain,
v_na____ != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(cnf_transformation,[status(esa)],[f1_sk]) ).
fof(f3,axiom,
v_n != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_assms_I2_J) ).
fof(f3_nnf,plain,
v_n != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(nnf_transformation,[status(thm)],[f3]) ).
fof(f3_sk,plain,
v_n != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(skolemisation,[status(esa)],[f3_nnf]) ).
cnf(c3,plain,
v_n != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(cnf_transformation,[status(esa)],[f3_sk]) ).
fof(f9,axiom,
! [V_l,V_k] : c_Int_OBit0(V_k) != c_Int_OBit1(V_l),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_rel__simps_I49_J) ).
fof(f9_nnf,plain,
! [V_l,V_k] : c_Int_OBit0(V_k) != c_Int_OBit1(V_l),
inference(nnf_transformation,[status(thm)],[f9]) ).
fof(f9_sk,plain,
! [V_k,V_l] : c_Int_OBit0(V_k) != c_Int_OBit1(V_l),
inference(skolemisation,[status(esa)],[f9_nnf]) ).
cnf(c11,plain,
c_Int_OBit0(X1) != c_Int_OBit1(X0),
inference(cnf_transformation,[status(esa)],[f9_sk]) ).
fof(f10,axiom,
! [V_l,V_k] : c_Int_OBit1(V_k) != c_Int_OBit0(V_l),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_rel__simps_I50_J) ).
fof(f10_nnf,plain,
! [V_l,V_k] : c_Int_OBit1(V_k) != c_Int_OBit0(V_l),
inference(nnf_transformation,[status(thm)],[f10]) ).
fof(f10_sk,plain,
! [V_k,V_l] : c_Int_OBit1(V_k) != c_Int_OBit0(V_l),
inference(skolemisation,[status(esa)],[f10_nnf]) ).
cnf(c12,plain,
c_Int_OBit1(X1) != c_Int_OBit0(X0),
inference(cnf_transformation,[status(esa)],[f10_sk]) ).
fof(f11,axiom,
! [V_l] : c_Int_OPls != c_Int_OBit1(V_l),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_rel__simps_I39_J) ).
fof(f11_nnf,plain,
! [V_l] : c_Int_OPls != c_Int_OBit1(V_l),
inference(nnf_transformation,[status(thm)],[f11]) ).
fof(f11_sk,plain,
! [V_l] : c_Int_OPls != c_Int_OBit1(V_l),
inference(skolemisation,[status(esa)],[f11_nnf]) ).
cnf(c13,plain,
c_Int_OPls != c_Int_OBit1(X0),
inference(cnf_transformation,[status(esa)],[f11_sk]) ).
fof(f12,axiom,
! [V_k] : c_Int_OBit1(V_k) != c_Int_OPls,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_rel__simps_I46_J) ).
fof(f12_nnf,plain,
! [V_k] : c_Int_OBit1(V_k) != c_Int_OPls,
inference(nnf_transformation,[status(thm)],[f12]) ).
fof(f12_sk,plain,
! [V_k] : c_Int_OBit1(V_k) != c_Int_OPls,
inference(skolemisation,[status(esa)],[f12_nnf]) ).
cnf(c14,plain,
c_Int_OBit1(X0) != c_Int_OPls,
inference(cnf_transformation,[status(esa)],[f12_sk]) ).
fof(f62,axiom,
! [V_nb_2] :
( ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_nb_2)
<=> ? [B_m] : V_nb_2 = c_Nat_OSuc(c_Groups_Otimes__class_Otimes(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),B_m)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_odd__Suc__mult__two__ex) ).
fof(f62_nnf,plain,
! [V_nb_2] :
( ( ! [B_m] : V_nb_2 != c_Nat_OSuc(c_Groups_Otimes__class_Otimes(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),B_m))
| ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_nb_2) )
& ( ? [B_m] : V_nb_2 = c_Nat_OSuc(c_Groups_Otimes__class_Otimes(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),B_m))
| c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_nb_2) ) ),
inference(nnf_transformation,[status(thm)],[f62]) ).
fof(f62_sk,plain,
! [V_nb_2,B_m] :
( ( V_nb_2 != c_Nat_OSuc(c_Groups_Otimes__class_Otimes(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),B_m))
| ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_nb_2) )
& ( V_nb_2 = c_Nat_OSuc(c_Groups_Otimes__class_Otimes(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),sk2(V_nb_2)))
| c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_nb_2) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk2])],[f62_nnf]) ).
cnf(c82,plain,
( X0 != c_Nat_OSuc(c_Groups_Otimes__class_Otimes(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),X1))
| ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,X0) ),
inference(cnf_transformation,[status(esa)],[f62_sk]) ).
fof(f70,axiom,
! [T_a] :
( class_Int_Onumber__ring(T_a)
=> ~ c_Int_Oiszero(T_a,c_Int_Onumber__class_Onumber__of(T_a,c_Int_OBit1(c_Int_OPls))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_not__iszero__Numeral1) ).
fof(f70_nnf,plain,
! [T_a] :
( ~ c_Int_Oiszero(T_a,c_Int_Onumber__class_Onumber__of(T_a,c_Int_OBit1(c_Int_OPls)))
| ~ class_Int_Onumber__ring(T_a) ),
inference(nnf_transformation,[status(thm)],[f70]) ).
fof(f70_sk,plain,
! [T_a] :
( ~ c_Int_Oiszero(T_a,c_Int_Onumber__class_Onumber__of(T_a,c_Int_OBit1(c_Int_OPls)))
| ~ class_Int_Onumber__ring(T_a) ),
inference(skolemisation,[status(esa)],[f70_nnf]) ).
cnf(c93,plain,
( ~ c_Int_Oiszero(X0,c_Int_Onumber__class_Onumber__of(X0,c_Int_OBit1(c_Int_OPls)))
| ~ class_Int_Onumber__ring(X0) ),
inference(cnf_transformation,[status(esa)],[f70_sk]) ).
fof(f92,axiom,
! [V_n] : V_n != c_Nat_OSuc(V_n),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_n__not__Suc__n) ).
fof(f92_nnf,plain,
! [V_n] : V_n != c_Nat_OSuc(V_n),
inference(nnf_transformation,[status(thm)],[f92]) ).
fof(f92_sk,plain,
! [V_n] : V_n != c_Nat_OSuc(V_n),
inference(skolemisation,[status(esa)],[f92_nnf]) ).
cnf(c117,plain,
X0 != c_Nat_OSuc(X0),
inference(cnf_transformation,[status(esa)],[f92_sk]) ).
fof(f93,axiom,
! [V_n] : c_Nat_OSuc(V_n) != V_n,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_Suc__n__not__n) ).
fof(f93_nnf,plain,
! [V_n] : c_Nat_OSuc(V_n) != V_n,
inference(nnf_transformation,[status(thm)],[f93]) ).
fof(f93_sk,plain,
! [V_n] : c_Nat_OSuc(V_n) != V_n,
inference(skolemisation,[status(esa)],[f93_nnf]) ).
cnf(c118,plain,
c_Nat_OSuc(X0) != X0,
inference(cnf_transformation,[status(esa)],[f93_sk]) ).
fof(f143,axiom,
! [V_nb_2,V_x_2] :
( c_Parity_Oeven__odd__class_Oeven(tc_Int_Oint,c_Power_Opower__class_Opower(tc_Int_Oint,V_x_2,V_nb_2))
<=> ( V_nb_2 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
& c_Parity_Oeven__odd__class_Oeven(tc_Int_Oint,V_x_2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_even__power) ).
fof(f143_nnf,plain,
! [V_nb_2,V_x_2] :
( ( V_nb_2 = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| ~ c_Parity_Oeven__odd__class_Oeven(tc_Int_Oint,V_x_2)
| c_Parity_Oeven__odd__class_Oeven(tc_Int_Oint,c_Power_Opower__class_Opower(tc_Int_Oint,V_x_2,V_nb_2)) )
& ( ( V_nb_2 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
& c_Parity_Oeven__odd__class_Oeven(tc_Int_Oint,V_x_2) )
| ~ c_Parity_Oeven__odd__class_Oeven(tc_Int_Oint,c_Power_Opower__class_Opower(tc_Int_Oint,V_x_2,V_nb_2)) ) ),
inference(nnf_transformation,[status(thm)],[f143]) ).
fof(f143_sk,plain,
! [V_x_2,V_nb_2] :
( ( V_nb_2 = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| ~ c_Parity_Oeven__odd__class_Oeven(tc_Int_Oint,V_x_2)
| c_Parity_Oeven__odd__class_Oeven(tc_Int_Oint,c_Power_Opower__class_Opower(tc_Int_Oint,V_x_2,V_nb_2)) )
& ( ( V_nb_2 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
& c_Parity_Oeven__odd__class_Oeven(tc_Int_Oint,V_x_2) )
| ~ c_Parity_Oeven__odd__class_Oeven(tc_Int_Oint,c_Power_Opower__class_Opower(tc_Int_Oint,V_x_2,V_nb_2)) ) ),
inference(skolemisation,[status(esa)],[f143_nnf]) ).
cnf(c202,plain,
( X0 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| ~ c_Parity_Oeven__odd__class_Oeven(tc_Int_Oint,c_Power_Opower__class_Opower(tc_Int_Oint,X1,X0)) ),
inference(cnf_transformation,[status(esa)],[f143_sk]) ).
fof(f144,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,c_Groups_Otimes__class_Otimes(T_a,V_x_2,V_x_2),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(f144_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,c_Groups_Otimes__class_Otimes(T_a,V_x_2,V_x_2),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,c_Groups_Otimes__class_Otimes(T_a,V_x_2,V_x_2),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)],[f144]) ).
fof(f144_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,c_Groups_Otimes__class_Otimes(T_a,V_x_2,V_x_2),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,c_Groups_Otimes__class_Otimes(T_a,V_x_2,V_x_2),c_Groups_Otimes__class_Otimes(T_a,V_y_2,V_y_2))) ) )
| ~ class_Rings_Olinordered__ring__strict(T_a) ),
inference(skolemisation,[status(esa)],[f144_nnf]) ).
cnf(c204,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,c_Groups_Otimes__class_Otimes(X2,X1,X1),c_Groups_Otimes__class_Otimes(X2,X0,X0)))
| ~ class_Rings_Olinordered__ring__strict(X2) ),
inference(cnf_transformation,[status(esa)],[f144_sk]) ).
fof(f145,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,c_Groups_Otimes__class_Otimes(T_a,V_x,V_x),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(f145_nnf,plain,
! [V_y,V_x,T_a] :
( ~ c_Orderings_Oord__class_Oless(T_a,c_Groups_Oplus__class_Oplus(T_a,c_Groups_Otimes__class_Otimes(T_a,V_x,V_x),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)],[f145]) ).
fof(f145_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_Orderings_Oord__class_Oless(T_a,c_Groups_Oplus__class_Oplus(T_a,c_Groups_Otimes__class_Otimes(T_a,V_x,V_x),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)],[f145_nnf]) ).
cnf(c207,plain,
( ~ c_Orderings_Oord__class_Oless(X2,c_Groups_Oplus__class_Oplus(X2,c_Groups_Otimes__class_Otimes(X2,X1,X1),c_Groups_Otimes__class_Otimes(X2,X0,X0)),c_Groups_Ozero__class_Ozero(X2))
| ~ class_Rings_Olinordered__ring(X2) ),
inference(cnf_transformation,[status(esa)],[f145_sk]) ).
fof(f146,axiom,
! [V_nb_2,V_x_2,T_a] :
( class_Rings_Olinordered__idom(T_a)
=> ( c_Orderings_Oord__class_Oless(T_a,c_Power_Opower__class_Opower(T_a,V_x_2,V_nb_2),c_Groups_Ozero__class_Ozero(T_a))
<=> ( c_Orderings_Oord__class_Oless(T_a,V_x_2,c_Groups_Ozero__class_Ozero(T_a))
& ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_nb_2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_power__less__zero__eq) ).
fof(f146_nnf,plain,
! [V_nb_2,V_x_2,T_a] :
( ( ( ~ c_Orderings_Oord__class_Oless(T_a,V_x_2,c_Groups_Ozero__class_Ozero(T_a))
| c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_nb_2)
| c_Orderings_Oord__class_Oless(T_a,c_Power_Opower__class_Opower(T_a,V_x_2,V_nb_2),c_Groups_Ozero__class_Ozero(T_a)) )
& ( ( c_Orderings_Oord__class_Oless(T_a,V_x_2,c_Groups_Ozero__class_Ozero(T_a))
& ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_nb_2) )
| ~ c_Orderings_Oord__class_Oless(T_a,c_Power_Opower__class_Opower(T_a,V_x_2,V_nb_2),c_Groups_Ozero__class_Ozero(T_a)) ) )
| ~ class_Rings_Olinordered__idom(T_a) ),
inference(nnf_transformation,[status(thm)],[f146]) ).
fof(f146_sk,plain,
! [T_a,V_x_2,V_nb_2] :
( ( ( ~ c_Orderings_Oord__class_Oless(T_a,V_x_2,c_Groups_Ozero__class_Ozero(T_a))
| c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_nb_2)
| c_Orderings_Oord__class_Oless(T_a,c_Power_Opower__class_Opower(T_a,V_x_2,V_nb_2),c_Groups_Ozero__class_Ozero(T_a)) )
& ( ( c_Orderings_Oord__class_Oless(T_a,V_x_2,c_Groups_Ozero__class_Ozero(T_a))
& ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_nb_2) )
| ~ c_Orderings_Oord__class_Oless(T_a,c_Power_Opower__class_Opower(T_a,V_x_2,V_nb_2),c_Groups_Ozero__class_Ozero(T_a)) ) )
| ~ class_Rings_Olinordered__idom(T_a) ),
inference(skolemisation,[status(esa)],[f146_nnf]) ).
cnf(c208,plain,
( ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,X0)
| ~ c_Orderings_Oord__class_Oless(X2,c_Power_Opower__class_Opower(X2,X1,X0),c_Groups_Ozero__class_Ozero(X2))
| ~ class_Rings_Olinordered__idom(X2) ),
inference(cnf_transformation,[status(esa)],[f146_sk]) ).
fof(f172,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(f172_nnf,plain,
! [V_m] : c_Nat_OSuc(V_m) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(nnf_transformation,[status(thm)],[f172]) ).
fof(f172_sk,plain,
! [V_m] : c_Nat_OSuc(V_m) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(skolemisation,[status(esa)],[f172_nnf]) ).
cnf(c242,plain,
c_Nat_OSuc(X0) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(cnf_transformation,[status(esa)],[f172_sk]) ).
fof(f173,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(f173_nnf,plain,
! [V_m] : c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != c_Nat_OSuc(V_m),
inference(nnf_transformation,[status(thm)],[f173]) ).
fof(f173_sk,plain,
! [V_m] : c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != c_Nat_OSuc(V_m),
inference(skolemisation,[status(esa)],[f173_nnf]) ).
cnf(c243,plain,
c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != c_Nat_OSuc(X0),
inference(cnf_transformation,[status(esa)],[f173_sk]) ).
fof(f174,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(f174_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)],[f174]) ).
fof(f174_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)],[f174_nnf]) ).
cnf(c244,plain,
c_Nat_OSuc(X0) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(cnf_transformation,[status(esa)],[f174_sk]) ).
fof(f175,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(f175_nnf,plain,
! [V_m] : c_Nat_OSuc(V_m) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(nnf_transformation,[status(thm)],[f175]) ).
fof(f175_sk,plain,
! [V_m] : c_Nat_OSuc(V_m) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(skolemisation,[status(esa)],[f175_nnf]) ).
cnf(c245,plain,
c_Nat_OSuc(X0) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat),
inference(cnf_transformation,[status(esa)],[f175_sk]) ).
fof(f176,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(f176_nnf,plain,
! [V_nat_H] : c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != c_Nat_OSuc(V_nat_H),
inference(nnf_transformation,[status(thm)],[f176]) ).
fof(f176_sk,plain,
! [V_nat_H] : c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != c_Nat_OSuc(V_nat_H),
inference(skolemisation,[status(esa)],[f176_nnf]) ).
cnf(c246,plain,
c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != c_Nat_OSuc(X0),
inference(cnf_transformation,[status(esa)],[f176_sk]) ).
fof(f177,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(f177_nnf,plain,
! [V_m] : c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != c_Nat_OSuc(V_m),
inference(nnf_transformation,[status(thm)],[f177]) ).
fof(f177_sk,plain,
! [V_m] : c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != c_Nat_OSuc(V_m),
inference(skolemisation,[status(esa)],[f177_nnf]) ).
cnf(c247,plain,
c_Groups_Ozero__class_Ozero(tc_Nat_Onat) != c_Nat_OSuc(X0),
inference(cnf_transformation,[status(esa)],[f177_sk]) ).
fof(f186,axiom,
~ c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Int_OPls,c_Int_OPls),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_rel__simps_I2_J) ).
fof(f186_nnf,plain,
~ c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Int_OPls,c_Int_OPls),
inference(nnf_transformation,[status(thm)],[f186]) ).
fof(f186_sk,plain,
~ c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Int_OPls,c_Int_OPls),
inference(skolemisation,[status(esa)],[f186_nnf]) ).
cnf(c260,plain,
~ c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Int_OPls,c_Int_OPls),
inference(cnf_transformation,[status(esa)],[f186_sk]) ).
fof(f194,axiom,
! [V_x_2] :
( c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Nat_OSuc(V_x_2))
<=> ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_x_2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_even__Suc) ).
fof(f194_nnf,plain,
! [V_x_2] :
( ( c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_x_2)
| c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Nat_OSuc(V_x_2)) )
& ( ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_x_2)
| ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Nat_OSuc(V_x_2)) ) ),
inference(nnf_transformation,[status(thm)],[f194]) ).
fof(f194_sk,plain,
! [V_x_2] :
( ( c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_x_2)
| c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Nat_OSuc(V_x_2)) )
& ( ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_x_2)
| ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Nat_OSuc(V_x_2)) ) ),
inference(skolemisation,[status(esa)],[f194_nnf]) ).
cnf(c272,plain,
( ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,X0)
| ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Nat_OSuc(X0)) ),
inference(cnf_transformation,[status(esa)],[f194_sk]) ).
fof(f206,axiom,
! [V_w_2,V_x_2,T_a] :
( class_Rings_Olinordered__idom(T_a)
=> ( c_Orderings_Oord__class_Oless(T_a,c_Power_Opower__class_Opower(T_a,V_x_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2)),c_Groups_Ozero__class_Ozero(T_a))
<=> ( c_Orderings_Oord__class_Oless(T_a,V_x_2,c_Groups_Ozero__class_Ozero(T_a))
& ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_power__less__zero__eq__number__of) ).
fof(f206_nnf,plain,
! [V_w_2,V_x_2,T_a] :
( ( ( ~ c_Orderings_Oord__class_Oless(T_a,V_x_2,c_Groups_Ozero__class_Ozero(T_a))
| c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2))
| c_Orderings_Oord__class_Oless(T_a,c_Power_Opower__class_Opower(T_a,V_x_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2)),c_Groups_Ozero__class_Ozero(T_a)) )
& ( ( c_Orderings_Oord__class_Oless(T_a,V_x_2,c_Groups_Ozero__class_Ozero(T_a))
& ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2)) )
| ~ c_Orderings_Oord__class_Oless(T_a,c_Power_Opower__class_Opower(T_a,V_x_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2)),c_Groups_Ozero__class_Ozero(T_a)) ) )
| ~ class_Rings_Olinordered__idom(T_a) ),
inference(nnf_transformation,[status(thm)],[f206]) ).
fof(f206_sk,plain,
! [T_a,V_x_2,V_w_2] :
( ( ( ~ c_Orderings_Oord__class_Oless(T_a,V_x_2,c_Groups_Ozero__class_Ozero(T_a))
| c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2))
| c_Orderings_Oord__class_Oless(T_a,c_Power_Opower__class_Opower(T_a,V_x_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2)),c_Groups_Ozero__class_Ozero(T_a)) )
& ( ( c_Orderings_Oord__class_Oless(T_a,V_x_2,c_Groups_Ozero__class_Ozero(T_a))
& ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2)) )
| ~ c_Orderings_Oord__class_Oless(T_a,c_Power_Opower__class_Opower(T_a,V_x_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2)),c_Groups_Ozero__class_Ozero(T_a)) ) )
| ~ class_Rings_Olinordered__idom(T_a) ),
inference(skolemisation,[status(esa)],[f206_nnf]) ).
cnf(c310,plain,
( ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,X0))
| ~ c_Orderings_Oord__class_Oless(X2,c_Power_Opower__class_Opower(X2,X1,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,X0)),c_Groups_Ozero__class_Ozero(X2))
| ~ class_Rings_Olinordered__idom(X2) ),
inference(cnf_transformation,[status(esa)],[f206_sk]) ).
fof(f208,axiom,
! [V_y,V_x,T_a] :
( class_Rings_Olinordered__idom(T_a)
=> ~ c_Orderings_Oord__class_Oless(T_a,c_Groups_Oplus__class_Oplus(T_a,c_Power_Opower__class_Opower(T_a,V_x,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(T_a,V_y,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),c_Groups_Ozero__class_Ozero(T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_not__sum__power2__lt__zero) ).
fof(f208_nnf,plain,
! [V_y,V_x,T_a] :
( ~ c_Orderings_Oord__class_Oless(T_a,c_Groups_Oplus__class_Oplus(T_a,c_Power_Opower__class_Opower(T_a,V_x,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(T_a,V_y,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),c_Groups_Ozero__class_Ozero(T_a))
| ~ class_Rings_Olinordered__idom(T_a) ),
inference(nnf_transformation,[status(thm)],[f208]) ).
fof(f208_sk,plain,
! [T_a,V_x,V_y] :
( ~ c_Orderings_Oord__class_Oless(T_a,c_Groups_Oplus__class_Oplus(T_a,c_Power_Opower__class_Opower(T_a,V_x,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(T_a,V_y,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),c_Groups_Ozero__class_Ozero(T_a))
| ~ class_Rings_Olinordered__idom(T_a) ),
inference(skolemisation,[status(esa)],[f208_nnf]) ).
cnf(c314,plain,
( ~ c_Orderings_Oord__class_Oless(X2,c_Groups_Oplus__class_Oplus(X2,c_Power_Opower__class_Opower(X2,X1,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(X2,X0,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))),c_Groups_Ozero__class_Ozero(X2))
| ~ class_Rings_Olinordered__idom(X2) ),
inference(cnf_transformation,[status(esa)],[f208_sk]) ).
fof(f209,axiom,
! [V_y_2,V_x_2,T_a] :
( class_Rings_Olinordered__idom(T_a)
=> ( c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),c_Groups_Oplus__class_Oplus(T_a,c_Power_Opower__class_Opower(T_a,V_x_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(T_a,V_y_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))))
<=> ( 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__power2__gt__zero__iff) ).
fof(f209_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,c_Power_Opower__class_Opower(T_a,V_x_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(T_a,V_y_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))) )
& ( 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,c_Power_Opower__class_Opower(T_a,V_x_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(T_a,V_y_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))) ) )
| ~ class_Rings_Olinordered__idom(T_a) ),
inference(nnf_transformation,[status(thm)],[f209]) ).
fof(f209_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,c_Power_Opower__class_Opower(T_a,V_x_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(T_a,V_y_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))) )
& ( 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,c_Power_Opower__class_Opower(T_a,V_x_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(T_a,V_y_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))) ) )
| ~ class_Rings_Olinordered__idom(T_a) ),
inference(skolemisation,[status(esa)],[f209_nnf]) ).
cnf(c315,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,c_Power_Opower__class_Opower(X2,X1,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Power_Opower__class_Opower(X2,X0,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))))
| ~ class_Rings_Olinordered__idom(X2) ),
inference(cnf_transformation,[status(esa)],[f209_sk]) ).
fof(f238,axiom,
! [V_a,T_a] :
( class_Rings_Olinordered__ring(T_a)
=> ~ c_Orderings_Oord__class_Oless(T_a,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(f238_nnf,plain,
! [V_a,T_a] :
( ~ c_Orderings_Oord__class_Oless(T_a,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)],[f238]) ).
fof(f238_sk,plain,
! [T_a,V_a] :
( ~ c_Orderings_Oord__class_Oless(T_a,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)],[f238_nnf]) ).
cnf(c371,plain,
( ~ c_Orderings_Oord__class_Oless(X1,c_Groups_Otimes__class_Otimes(X1,X0,X0),c_Groups_Ozero__class_Ozero(X1))
| ~ class_Rings_Olinordered__ring(X1) ),
inference(cnf_transformation,[status(esa)],[f238_sk]) ).
fof(f245,axiom,
~ c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Int_OPls,c_Groups_Ozero__class_Ozero(tc_Int_Oint)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_bin__less__0__simps_I1_J) ).
fof(f245_nnf,plain,
~ c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Int_OPls,c_Groups_Ozero__class_Ozero(tc_Int_Oint)),
inference(nnf_transformation,[status(thm)],[f245]) ).
fof(f245_sk,plain,
~ c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Int_OPls,c_Groups_Ozero__class_Ozero(tc_Int_Oint)),
inference(skolemisation,[status(esa)],[f245_nnf]) ).
cnf(c384,plain,
~ c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Int_OPls,c_Groups_Ozero__class_Ozero(tc_Int_Oint)),
inference(cnf_transformation,[status(esa)],[f245_sk]) ).
fof(f253,axiom,
! [V_a,T_a] :
( class_Rings_Olinordered__idom(T_a)
=> ~ c_Orderings_Oord__class_Oless(T_a,c_Power_Opower__class_Opower(T_a,V_a,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Groups_Ozero__class_Ozero(T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_power2__less__0) ).
fof(f253_nnf,plain,
! [V_a,T_a] :
( ~ c_Orderings_Oord__class_Oless(T_a,c_Power_Opower__class_Opower(T_a,V_a,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Groups_Ozero__class_Ozero(T_a))
| ~ class_Rings_Olinordered__idom(T_a) ),
inference(nnf_transformation,[status(thm)],[f253]) ).
fof(f253_sk,plain,
! [T_a,V_a] :
( ~ c_Orderings_Oord__class_Oless(T_a,c_Power_Opower__class_Opower(T_a,V_a,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Groups_Ozero__class_Ozero(T_a))
| ~ class_Rings_Olinordered__idom(T_a) ),
inference(skolemisation,[status(esa)],[f253_nnf]) ).
cnf(c399,plain,
( ~ c_Orderings_Oord__class_Oless(X1,c_Power_Opower__class_Opower(X1,X0,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),c_Groups_Ozero__class_Ozero(X1))
| ~ class_Rings_Olinordered__idom(X1) ),
inference(cnf_transformation,[status(esa)],[f253_sk]) ).
fof(f254,axiom,
! [V_a_2,T_a] :
( class_Rings_Olinordered__idom(T_a)
=> ( c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),c_Power_Opower__class_Opower(T_a,V_a_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))
<=> V_a_2 != c_Groups_Ozero__class_Ozero(T_a) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_zero__less__power2) ).
fof(f254_nnf,plain,
! [V_a_2,T_a] :
( ( ( V_a_2 = c_Groups_Ozero__class_Ozero(T_a)
| c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),c_Power_Opower__class_Opower(T_a,V_a_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) )
& ( V_a_2 != c_Groups_Ozero__class_Ozero(T_a)
| ~ c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),c_Power_Opower__class_Opower(T_a,V_a_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) ) )
| ~ class_Rings_Olinordered__idom(T_a) ),
inference(nnf_transformation,[status(thm)],[f254]) ).
fof(f254_sk,plain,
! [T_a,V_a_2] :
( ( ( V_a_2 = c_Groups_Ozero__class_Ozero(T_a)
| c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),c_Power_Opower__class_Opower(T_a,V_a_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) )
& ( V_a_2 != c_Groups_Ozero__class_Ozero(T_a)
| ~ c_Orderings_Oord__class_Oless(T_a,c_Groups_Ozero__class_Ozero(T_a),c_Power_Opower__class_Opower(T_a,V_a_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))))) ) )
| ~ class_Rings_Olinordered__idom(T_a) ),
inference(skolemisation,[status(esa)],[f254_nnf]) ).
cnf(c400,plain,
( X0 != c_Groups_Ozero__class_Ozero(X1)
| ~ c_Orderings_Oord__class_Oless(X1,c_Groups_Ozero__class_Ozero(X1),c_Power_Opower__class_Opower(X1,X0,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))))
| ~ class_Rings_Olinordered__idom(X1) ),
inference(cnf_transformation,[status(esa)],[f254_sk]) ).
fof(f258,axiom,
! [V_w_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) )
=> ( c_Power_Opower__class_Opower(T_a,V_a_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2)) = c_Groups_Ozero__class_Ozero(T_a)
<=> ( c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_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__number__of) ).
fof(f258_nnf,plain,
! [V_w_2,V_a_2,T_a] :
( ( ( c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| V_a_2 != c_Groups_Ozero__class_Ozero(T_a)
| c_Power_Opower__class_Opower(T_a,V_a_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2)) = c_Groups_Ozero__class_Ozero(T_a) )
& ( ( c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
& V_a_2 = c_Groups_Ozero__class_Ozero(T_a) )
| c_Power_Opower__class_Opower(T_a,V_a_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_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)],[f258]) ).
fof(f258_sk,plain,
! [T_a,V_a_2,V_w_2] :
( ( ( c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| V_a_2 != c_Groups_Ozero__class_Ozero(T_a)
| c_Power_Opower__class_Opower(T_a,V_a_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2)) = c_Groups_Ozero__class_Ozero(T_a) )
& ( ( c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
& V_a_2 = c_Groups_Ozero__class_Ozero(T_a) )
| c_Power_Opower__class_Opower(T_a,V_a_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_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)],[f258_nnf]) ).
cnf(c406,plain,
( c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,X0) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| c_Power_Opower__class_Opower(X2,X1,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,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)],[f258_sk]) ).
fof(f260,axiom,
! [V_x_2] :
( ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_x_2)
<=> ? [B_y] : V_x_2 = c_Nat_OSuc(c_Groups_Otimes__class_Otimes(tc_Nat_Onat,c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),B_y)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_odd__nat__equiv__def2) ).
fof(f260_nnf,plain,
! [V_x_2] :
( ( ! [B_y] : V_x_2 != c_Nat_OSuc(c_Groups_Otimes__class_Otimes(tc_Nat_Onat,c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),B_y))
| ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_x_2) )
& ( ? [B_y] : V_x_2 = c_Nat_OSuc(c_Groups_Otimes__class_Otimes(tc_Nat_Onat,c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),B_y))
| c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_x_2) ) ),
inference(nnf_transformation,[status(thm)],[f260]) ).
fof(f260_sk,plain,
! [V_x_2,B_y] :
( ( V_x_2 != c_Nat_OSuc(c_Groups_Otimes__class_Otimes(tc_Nat_Onat,c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),B_y))
| ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_x_2) )
& ( V_x_2 = c_Nat_OSuc(c_Groups_Otimes__class_Otimes(tc_Nat_Onat,c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),sk4(V_x_2)))
| c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_x_2) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk4])],[f260_nnf]) ).
cnf(c410,plain,
( X0 != c_Nat_OSuc(c_Groups_Otimes__class_Otimes(tc_Nat_Onat,c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))),X1))
| ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,X0) ),
inference(cnf_transformation,[status(esa)],[f260_sk]) ).
fof(f262,axiom,
! [V_w,T_a] :
( ( class_Int_Oring__char__0(T_a)
& class_Int_Onumber__ring(T_a) )
=> ~ c_Int_Oiszero(T_a,c_Int_Onumber__class_Onumber__of(T_a,c_Int_OBit1(V_w))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_iszero__number__of__Bit1) ).
fof(f262_nnf,plain,
! [V_w,T_a] :
( ~ c_Int_Oiszero(T_a,c_Int_Onumber__class_Onumber__of(T_a,c_Int_OBit1(V_w)))
| ~ class_Int_Oring__char__0(T_a)
| ~ class_Int_Onumber__ring(T_a) ),
inference(nnf_transformation,[status(thm)],[f262]) ).
fof(f262_sk,plain,
! [T_a,V_w] :
( ~ c_Int_Oiszero(T_a,c_Int_Onumber__class_Onumber__of(T_a,c_Int_OBit1(V_w)))
| ~ class_Int_Oring__char__0(T_a)
| ~ class_Int_Onumber__ring(T_a) ),
inference(skolemisation,[status(esa)],[f262_nnf]) ).
cnf(c413,plain,
( ~ c_Int_Oiszero(X1,c_Int_Onumber__class_Onumber__of(X1,c_Int_OBit1(X0)))
| ~ class_Int_Oring__char__0(X1)
| ~ class_Int_Onumber__ring(X1) ),
inference(cnf_transformation,[status(esa)],[f262_sk]) ).
fof(f283,axiom,
! [V_nb_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) )
=> ( c_Power_Opower__class_Opower(T_a,V_a_2,V_nb_2) = c_Groups_Ozero__class_Ozero(T_a)
<=> ( V_nb_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(f283_nnf,plain,
! [V_nb_2,V_a_2,T_a] :
( ( ( V_nb_2 = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| V_a_2 != c_Groups_Ozero__class_Ozero(T_a)
| c_Power_Opower__class_Opower(T_a,V_a_2,V_nb_2) = c_Groups_Ozero__class_Ozero(T_a) )
& ( ( V_nb_2 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
& V_a_2 = c_Groups_Ozero__class_Ozero(T_a) )
| c_Power_Opower__class_Opower(T_a,V_a_2,V_nb_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)],[f283]) ).
fof(f283_sk,plain,
! [T_a,V_a_2,V_nb_2] :
( ( ( V_nb_2 = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| V_a_2 != c_Groups_Ozero__class_Ozero(T_a)
| c_Power_Opower__class_Opower(T_a,V_a_2,V_nb_2) = c_Groups_Ozero__class_Ozero(T_a) )
& ( ( V_nb_2 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
& V_a_2 = c_Groups_Ozero__class_Ozero(T_a) )
| c_Power_Opower__class_Opower(T_a,V_a_2,V_nb_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)],[f283_nnf]) ).
cnf(c439,plain,
( X0 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| 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)],[f283_sk]) ).
fof(f286,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(f286_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)],[f286]) ).
fof(f286_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)],[f286_nnf]) ).
cnf(c444,plain,
~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(cnf_transformation,[status(esa)],[f286_sk]) ).
fof(f290,axiom,
! [V_x_2] :
( ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal),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(f290_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),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),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,V_x_2,V_x_2)) ) ),
inference(nnf_transformation,[status(thm)],[f290]) ).
fof(f290_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),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),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,V_x_2,V_x_2)) ) ),
inference(skolemisation,[status(esa)],[f290_nnf]) ).
cnf(c449,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),c_Groups_Otimes__class_Otimes(tc_RealDef_Oreal,X0,X0)) ),
inference(cnf_transformation,[status(esa)],[f290_sk]) ).
fof(f304,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(f304_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)],[f304]) ).
fof(f304_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)],[f304_nnf]) ).
cnf(c467,plain,
~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(cnf_transformation,[status(esa)],[f304_sk]) ).
fof(f305,axiom,
! [V_nb_2] :
( V_nb_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_nb_2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_neq0__conv) ).
fof(f305_nnf,plain,
! [V_nb_2] :
( ( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),V_nb_2)
| V_nb_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_nb_2)
| V_nb_2 = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ) ),
inference(nnf_transformation,[status(thm)],[f305]) ).
fof(f305_sk,plain,
! [V_nb_2] :
( ( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),V_nb_2)
| V_nb_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_nb_2)
| V_nb_2 = c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ) ),
inference(skolemisation,[status(esa)],[f305_nnf]) ).
cnf(c469,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)],[f305_sk]) ).
fof(f306,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(f306_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)],[f306]) ).
fof(f306_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)],[f306_nnf]) ).
cnf(c470,plain,
~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,c_Groups_Ozero__class_Ozero(tc_Nat_Onat)),
inference(cnf_transformation,[status(esa)],[f306_sk]) ).
fof(f307,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(f307_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)],[f307]) ).
fof(f307_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)],[f307_nnf]) ).
cnf(c471,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)],[f307_sk]) ).
fof(f321,axiom,
! [V_nb_2,V_m_2] :
( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_nb_2)
<=> c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_nb_2,c_Nat_OSuc(V_m_2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_not__less__eq) ).
fof(f321_nnf,plain,
! [V_nb_2,V_m_2] :
( ( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_nb_2,c_Nat_OSuc(V_m_2))
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_nb_2) )
& ( c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_nb_2,c_Nat_OSuc(V_m_2))
| c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_nb_2) ) ),
inference(nnf_transformation,[status(thm)],[f321]) ).
fof(f321_sk,plain,
! [V_m_2,V_nb_2] :
( ( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_nb_2,c_Nat_OSuc(V_m_2))
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_nb_2) )
& ( c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_nb_2,c_Nat_OSuc(V_m_2))
| c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_nb_2) ) ),
inference(skolemisation,[status(esa)],[f321_nnf]) ).
cnf(c492,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)],[f321_sk]) ).
fof(f330,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(f330_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)],[f330]) ).
fof(f330_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)],[f330_nnf]) ).
cnf(c502,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)],[f330_sk]) ).
fof(f331,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(f331_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)],[f331]) ).
fof(f331_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)],[f331_nnf]) ).
cnf(c503,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)],[f331_sk]) ).
fof(f340,axiom,
! [V_n,V_m] :
( c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Groups_Ozero__class_Ozero(tc_Int_Oint),V_m)
=> ( c_Orderings_Oord__class_Oless(tc_Int_Oint,V_m,V_n)
=> ~ c_Rings_Odvd__class_Odvd(tc_Int_Oint,V_n,V_m) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_zdvd__not__zless) ).
fof(f340_nnf,plain,
! [V_n,V_m] :
( ~ c_Rings_Odvd__class_Odvd(tc_Int_Oint,V_n,V_m)
| ~ c_Orderings_Oord__class_Oless(tc_Int_Oint,V_m,V_n)
| ~ c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Groups_Ozero__class_Ozero(tc_Int_Oint),V_m) ),
inference(nnf_transformation,[status(thm)],[f340]) ).
fof(f340_sk,plain,
! [V_m,V_n] :
( ~ c_Rings_Odvd__class_Odvd(tc_Int_Oint,V_n,V_m)
| ~ c_Orderings_Oord__class_Oless(tc_Int_Oint,V_m,V_n)
| ~ c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Groups_Ozero__class_Ozero(tc_Int_Oint),V_m) ),
inference(skolemisation,[status(esa)],[f340_nnf]) ).
cnf(c518,plain,
( ~ c_Rings_Odvd__class_Odvd(tc_Int_Oint,X0,X1)
| ~ c_Orderings_Oord__class_Oless(tc_Int_Oint,X1,X0)
| ~ c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Groups_Ozero__class_Ozero(tc_Int_Oint),X1) ),
inference(cnf_transformation,[status(esa)],[f340_sk]) ).
fof(f348,axiom,
! [V_n,V_m] :
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),V_m)
=> ( c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m,V_n)
=> ~ c_Rings_Odvd__class_Odvd(tc_Nat_Onat,V_n,V_m) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_nat__dvd__not__less) ).
fof(f348_nnf,plain,
! [V_n,V_m] :
( ~ c_Rings_Odvd__class_Odvd(tc_Nat_Onat,V_n,V_m)
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m,V_n)
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),V_m) ),
inference(nnf_transformation,[status(thm)],[f348]) ).
fof(f348_sk,plain,
! [V_m,V_n] :
( ~ c_Rings_Odvd__class_Odvd(tc_Nat_Onat,V_n,V_m)
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m,V_n)
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),V_m) ),
inference(skolemisation,[status(esa)],[f348_nnf]) ).
cnf(c531,plain,
( ~ c_Rings_Odvd__class_Odvd(tc_Nat_Onat,X0,X1)
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0)
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),X1) ),
inference(cnf_transformation,[status(esa)],[f348_sk]) ).
fof(f411,axiom,
! [V_x_2] :
( ~ c_Parity_Oeven__odd__class_Oeven(tc_Int_Oint,V_x_2)
<=> ? [B_y] : V_x_2 = c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Otimes__class_Otimes(tc_Int_Oint,c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),B_y),c_Groups_Oone__class_Oone(tc_Int_Oint)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_odd__equiv__def) ).
fof(f411_nnf,plain,
! [V_x_2] :
( ( ! [B_y] : V_x_2 != c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Otimes__class_Otimes(tc_Int_Oint,c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),B_y),c_Groups_Oone__class_Oone(tc_Int_Oint))
| ~ c_Parity_Oeven__odd__class_Oeven(tc_Int_Oint,V_x_2) )
& ( ? [B_y] : V_x_2 = c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Otimes__class_Otimes(tc_Int_Oint,c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),B_y),c_Groups_Oone__class_Oone(tc_Int_Oint))
| c_Parity_Oeven__odd__class_Oeven(tc_Int_Oint,V_x_2) ) ),
inference(nnf_transformation,[status(thm)],[f411]) ).
fof(f411_sk,plain,
! [V_x_2,B_y] :
( ( V_x_2 != c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Otimes__class_Otimes(tc_Int_Oint,c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),B_y),c_Groups_Oone__class_Oone(tc_Int_Oint))
| ~ c_Parity_Oeven__odd__class_Oeven(tc_Int_Oint,V_x_2) )
& ( V_x_2 = c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Otimes__class_Otimes(tc_Int_Oint,c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),sk11(V_x_2)),c_Groups_Oone__class_Oone(tc_Int_Oint))
| c_Parity_Oeven__odd__class_Oeven(tc_Int_Oint,V_x_2) ) ),
inference(skolemisation,[status(esa),new_symbols(skolem,[sk11])],[f411_nnf]) ).
cnf(c630,plain,
( X0 != c_Groups_Oplus__class_Oplus(tc_Int_Oint,c_Groups_Otimes__class_Otimes(tc_Int_Oint,c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),X1),c_Groups_Oone__class_Oone(tc_Int_Oint))
| ~ c_Parity_Oeven__odd__class_Oeven(tc_Int_Oint,X0) ),
inference(cnf_transformation,[status(esa)],[f411_sk]) ).
fof(f424,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(f424_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)],[f424]) ).
fof(f424_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)],[f424_nnf]) ).
cnf(c650,plain,
( X1 != X0
| ~ c_Orderings_Oord__class_Oless(tc_RealDef_Oreal,X1,X0) ),
inference(cnf_transformation,[status(esa)],[f424_sk]) ).
fof(f425,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(f425_nnf,plain,
! [V_n] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n,V_n),
inference(nnf_transformation,[status(thm)],[f425]) ).
fof(f425_sk,plain,
! [V_n] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n,V_n),
inference(skolemisation,[status(esa)],[f425_nnf]) ).
cnf(c652,plain,
~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,X0),
inference(cnf_transformation,[status(esa)],[f425_sk]) ).
fof(f426,axiom,
! [V_nb_2,V_m_2] :
( V_m_2 != V_nb_2
<=> ( c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_nb_2,V_m_2)
| c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_nb_2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_nat__neq__iff) ).
fof(f426_nnf,plain,
! [V_nb_2,V_m_2] :
( ( ( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_nb_2,V_m_2)
& ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_nb_2) )
| V_m_2 != V_nb_2 )
& ( c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_nb_2,V_m_2)
| c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_nb_2)
| V_m_2 = V_nb_2 ) ),
inference(nnf_transformation,[status(thm)],[f426]) ).
fof(f426_sk,plain,
! [V_m_2,V_nb_2] :
( ( ( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_nb_2,V_m_2)
& ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_nb_2) )
| V_m_2 != V_nb_2 )
& ( c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_nb_2,V_m_2)
| c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_nb_2)
| V_m_2 = V_nb_2 ) ),
inference(skolemisation,[status(esa)],[f426_nnf]) ).
cnf(c654,plain,
( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0)
| X1 != X0 ),
inference(cnf_transformation,[status(esa)],[f426_sk]) ).
cnf(c655,plain,
( ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,X1)
| X1 != X0 ),
inference(cnf_transformation,[status(esa)],[f426_sk]) ).
fof(f427,axiom,
! [V_nb_2,V_m_2] :
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_nb_2)
<=> ( V_m_2 != V_nb_2
& c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_m_2,V_nb_2) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_nat__less__le) ).
fof(f427_nnf,plain,
! [V_nb_2,V_m_2] :
( ( V_m_2 = V_nb_2
| ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_m_2,V_nb_2)
| c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_nb_2) )
& ( ( V_m_2 != V_nb_2
& c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_m_2,V_nb_2) )
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_nb_2) ) ),
inference(nnf_transformation,[status(thm)],[f427]) ).
fof(f427_sk,plain,
! [V_m_2,V_nb_2] :
( ( V_m_2 = V_nb_2
| ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_m_2,V_nb_2)
| c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_nb_2) )
& ( ( V_m_2 != V_nb_2
& c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_m_2,V_nb_2) )
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_m_2,V_nb_2) ) ),
inference(skolemisation,[status(esa)],[f427_nnf]) ).
cnf(c657,plain,
( X1 != X0
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0) ),
inference(cnf_transformation,[status(esa)],[f427_sk]) ).
fof(f430,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(f430_nnf,plain,
! [V_n] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n,V_n),
inference(nnf_transformation,[status(thm)],[f430]) ).
fof(f430_sk,plain,
! [V_n] : ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,V_n,V_n),
inference(skolemisation,[status(esa)],[f430_nnf]) ).
cnf(c663,plain,
~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X0,X0),
inference(cnf_transformation,[status(esa)],[f430_sk]) ).
fof(f431,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(f431_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)],[f431]) ).
fof(f431_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)],[f431_nnf]) ).
cnf(c664,plain,
( X0 != X1
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0) ),
inference(cnf_transformation,[status(esa)],[f431_sk]) ).
fof(f432,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(f432_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)],[f432]) ).
fof(f432_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)],[f432_nnf]) ).
cnf(c665,plain,
( X1 != X0
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,X1,X0) ),
inference(cnf_transformation,[status(esa)],[f432_sk]) ).
fof(f469,axiom,
~ c_Orderings_Oord__class_Oless__eq(tc_Int_Oint,c_Int_OPls,c_Int_OMin),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_rel__simps_I20_J) ).
fof(f469_nnf,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_Int_Oint,c_Int_OPls,c_Int_OMin),
inference(nnf_transformation,[status(thm)],[f469]) ).
fof(f469_sk,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_Int_Oint,c_Int_OPls,c_Int_OMin),
inference(skolemisation,[status(esa)],[f469_nnf]) ).
cnf(c725,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_Int_Oint,c_Int_OPls,c_Int_OMin),
inference(cnf_transformation,[status(esa)],[f469_sk]) ).
fof(f474,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(f474_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)],[f474]) ).
fof(f474_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)],[f474_nnf]) ).
cnf(c733,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)],[f474_sk]) ).
fof(f514,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(f514_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)],[f514]) ).
fof(f514_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)],[f514_nnf]) ).
cnf(c794,plain,
( c_Groups_Ozero__class_Ozero(X0) != c_Groups_Oone__class_Oone(X0)
| ~ class_Rings_Ozero__neq__one(X0) ),
inference(cnf_transformation,[status(esa)],[f514_sk]) ).
fof(f515,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(f515_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)],[f515]) ).
fof(f515_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)],[f515_nnf]) ).
cnf(c795,plain,
( c_Groups_Oone__class_Oone(X0) != c_Groups_Ozero__class_Ozero(X0)
| ~ class_Rings_Ozero__neq__one(X0) ),
inference(cnf_transformation,[status(esa)],[f515_sk]) ).
fof(f527,axiom,
c_Int_OMin != c_Int_OPls,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_rel__simps_I40_J) ).
fof(f527_nnf,plain,
c_Int_OMin != c_Int_OPls,
inference(nnf_transformation,[status(thm)],[f527]) ).
fof(f527_sk,plain,
c_Int_OMin != c_Int_OPls,
inference(skolemisation,[status(esa)],[f527_nnf]) ).
cnf(c810,plain,
c_Int_OMin != c_Int_OPls,
inference(cnf_transformation,[status(esa)],[f527_sk]) ).
fof(f528,axiom,
c_Int_OPls != c_Int_OMin,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_rel__simps_I37_J) ).
fof(f528_nnf,plain,
c_Int_OPls != c_Int_OMin,
inference(nnf_transformation,[status(thm)],[f528]) ).
fof(f528_sk,plain,
c_Int_OPls != c_Int_OMin,
inference(skolemisation,[status(esa)],[f528_nnf]) ).
cnf(c811,plain,
c_Int_OPls != c_Int_OMin,
inference(cnf_transformation,[status(esa)],[f528_sk]) ).
fof(f535,axiom,
! [V_l] : c_Int_OMin != c_Int_OBit0(V_l),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_rel__simps_I42_J) ).
fof(f535_nnf,plain,
! [V_l] : c_Int_OMin != c_Int_OBit0(V_l),
inference(nnf_transformation,[status(thm)],[f535]) ).
fof(f535_sk,plain,
! [V_l] : c_Int_OMin != c_Int_OBit0(V_l),
inference(skolemisation,[status(esa)],[f535_nnf]) ).
cnf(c818,plain,
c_Int_OMin != c_Int_OBit0(X0),
inference(cnf_transformation,[status(esa)],[f535_sk]) ).
fof(f536,axiom,
! [V_k] : c_Int_OBit0(V_k) != c_Int_OMin,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_rel__simps_I45_J) ).
fof(f536_nnf,plain,
! [V_k] : c_Int_OBit0(V_k) != c_Int_OMin,
inference(nnf_transformation,[status(thm)],[f536]) ).
fof(f536_sk,plain,
! [V_k] : c_Int_OBit0(V_k) != c_Int_OMin,
inference(skolemisation,[status(esa)],[f536_nnf]) ).
cnf(c819,plain,
c_Int_OBit0(X0) != c_Int_OMin,
inference(cnf_transformation,[status(esa)],[f536_sk]) ).
fof(f555,axiom,
~ c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Int_OMin,c_Int_OMin),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_rel__simps_I7_J) ).
fof(f555_nnf,plain,
~ c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Int_OMin,c_Int_OMin),
inference(nnf_transformation,[status(thm)],[f555]) ).
fof(f555_sk,plain,
~ c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Int_OMin,c_Int_OMin),
inference(skolemisation,[status(esa)],[f555_nnf]) ).
cnf(c841,plain,
~ c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Int_OMin,c_Int_OMin),
inference(cnf_transformation,[status(esa)],[f555_sk]) ).
fof(f567,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(f567_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)],[f567]) ).
fof(f567_sk,plain,
! [V_n] : ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_OSuc(V_n),V_n),
inference(skolemisation,[status(esa)],[f567_nnf]) ).
cnf(c856,plain,
~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_OSuc(X0),X0),
inference(cnf_transformation,[status(esa)],[f567_sk]) ).
fof(f568,axiom,
! [V_nb_2,V_m_2] :
( ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_m_2,V_nb_2)
<=> c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_OSuc(V_nb_2),V_m_2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_not__less__eq__eq) ).
fof(f568_nnf,plain,
! [V_nb_2,V_m_2] :
( ( ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_OSuc(V_nb_2),V_m_2)
| ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_m_2,V_nb_2) )
& ( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_OSuc(V_nb_2),V_m_2)
| c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_m_2,V_nb_2) ) ),
inference(nnf_transformation,[status(thm)],[f568]) ).
fof(f568_sk,plain,
! [V_m_2,V_nb_2] :
( ( ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_OSuc(V_nb_2),V_m_2)
| ~ c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_m_2,V_nb_2) )
& ( c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,c_Nat_OSuc(V_nb_2),V_m_2)
| c_Orderings_Oord__class_Oless__eq(tc_Nat_Onat,V_m_2,V_nb_2) ) ),
inference(skolemisation,[status(esa)],[f568_nnf]) ).
cnf(c858,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)],[f568_sk]) ).
fof(f595,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(f595_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)],[f595]) ).
fof(f595_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)],[f595_nnf]) ).
cnf(c898,plain,
( X1 != X0
| ~ c_Orderings_Oord__class_Oless(tc_Int_Oint,X1,X0) ),
inference(cnf_transformation,[status(esa)],[f595_sk]) ).
fof(f596,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(f596_nnf,plain,
c_Groups_Ozero__class_Ozero(tc_Int_Oint) != c_Groups_Oone__class_Oone(tc_Int_Oint),
inference(nnf_transformation,[status(thm)],[f596]) ).
fof(f596_sk,plain,
c_Groups_Ozero__class_Ozero(tc_Int_Oint) != c_Groups_Oone__class_Oone(tc_Int_Oint),
inference(skolemisation,[status(esa)],[f596_nnf]) ).
cnf(c900,plain,
c_Groups_Ozero__class_Ozero(tc_Int_Oint) != c_Groups_Oone__class_Oone(tc_Int_Oint),
inference(cnf_transformation,[status(esa)],[f596_sk]) ).
fof(f609,axiom,
~ c_Parity_Oeven__odd__class_Oeven(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_odd__one__int) ).
fof(f609_nnf,plain,
~ c_Parity_Oeven__odd__class_Oeven(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint)),
inference(nnf_transformation,[status(thm)],[f609]) ).
fof(f609_sk,plain,
~ c_Parity_Oeven__odd__class_Oeven(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint)),
inference(skolemisation,[status(esa)],[f609_nnf]) ).
cnf(c925,plain,
~ c_Parity_Oeven__odd__class_Oeven(tc_Int_Oint,c_Groups_Oone__class_Oone(tc_Int_Oint)),
inference(cnf_transformation,[status(esa)],[f609_sk]) ).
fof(f613,axiom,
! [T_a] :
( class_Rings_Osemiring__1(T_a)
=> ~ c_Int_Oiszero(T_a,c_Groups_Oone__class_Oone(T_a)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_not__iszero__1) ).
fof(f613_nnf,plain,
! [T_a] :
( ~ c_Int_Oiszero(T_a,c_Groups_Oone__class_Oone(T_a))
| ~ class_Rings_Osemiring__1(T_a) ),
inference(nnf_transformation,[status(thm)],[f613]) ).
fof(f613_sk,plain,
! [T_a] :
( ~ c_Int_Oiszero(T_a,c_Groups_Oone__class_Oone(T_a))
| ~ class_Rings_Osemiring__1(T_a) ),
inference(skolemisation,[status(esa)],[f613_nnf]) ).
cnf(c931,plain,
( ~ c_Int_Oiszero(X0,c_Groups_Oone__class_Oone(X0))
| ~ class_Rings_Osemiring__1(X0) ),
inference(cnf_transformation,[status(esa)],[f613_sk]) ).
fof(f625,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(f625_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)],[f625]) ).
fof(f625_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)],[f625_nnf]) ).
cnf(c947,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)],[f625_sk]) ).
fof(f656,axiom,
! [V_w_2,V_v_2,T_a] :
( ( class_Orderings_Olinorder(T_a)
& class_Int_Onumber(T_a) )
=> ( c_Orderings_Oord__class_Oless__eq(T_a,c_Int_Onumber__class_Onumber__of(T_a,V_v_2),c_Int_Onumber__class_Onumber__of(T_a,V_w_2))
<=> ~ c_Orderings_Oord__class_Oless(T_a,c_Int_Onumber__class_Onumber__of(T_a,V_w_2),c_Int_Onumber__class_Onumber__of(T_a,V_v_2)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_le__number__of__eq__not__less) ).
fof(f656_nnf,plain,
! [V_w_2,V_v_2,T_a] :
( ( ( c_Orderings_Oord__class_Oless(T_a,c_Int_Onumber__class_Onumber__of(T_a,V_w_2),c_Int_Onumber__class_Onumber__of(T_a,V_v_2))
| c_Orderings_Oord__class_Oless__eq(T_a,c_Int_Onumber__class_Onumber__of(T_a,V_v_2),c_Int_Onumber__class_Onumber__of(T_a,V_w_2)) )
& ( ~ c_Orderings_Oord__class_Oless(T_a,c_Int_Onumber__class_Onumber__of(T_a,V_w_2),c_Int_Onumber__class_Onumber__of(T_a,V_v_2))
| ~ c_Orderings_Oord__class_Oless__eq(T_a,c_Int_Onumber__class_Onumber__of(T_a,V_v_2),c_Int_Onumber__class_Onumber__of(T_a,V_w_2)) ) )
| ~ class_Orderings_Olinorder(T_a)
| ~ class_Int_Onumber(T_a) ),
inference(nnf_transformation,[status(thm)],[f656]) ).
fof(f656_sk,plain,
! [T_a,V_v_2,V_w_2] :
( ( ( c_Orderings_Oord__class_Oless(T_a,c_Int_Onumber__class_Onumber__of(T_a,V_w_2),c_Int_Onumber__class_Onumber__of(T_a,V_v_2))
| c_Orderings_Oord__class_Oless__eq(T_a,c_Int_Onumber__class_Onumber__of(T_a,V_v_2),c_Int_Onumber__class_Onumber__of(T_a,V_w_2)) )
& ( ~ c_Orderings_Oord__class_Oless(T_a,c_Int_Onumber__class_Onumber__of(T_a,V_w_2),c_Int_Onumber__class_Onumber__of(T_a,V_v_2))
| ~ c_Orderings_Oord__class_Oless__eq(T_a,c_Int_Onumber__class_Onumber__of(T_a,V_v_2),c_Int_Onumber__class_Onumber__of(T_a,V_w_2)) ) )
| ~ class_Orderings_Olinorder(T_a)
| ~ class_Int_Onumber(T_a) ),
inference(skolemisation,[status(esa)],[f656_nnf]) ).
cnf(c994,plain,
( ~ c_Orderings_Oord__class_Oless(X2,c_Int_Onumber__class_Onumber__of(X2,X0),c_Int_Onumber__class_Onumber__of(X2,X1))
| ~ c_Orderings_Oord__class_Oless__eq(X2,c_Int_Onumber__class_Onumber__of(X2,X1),c_Int_Onumber__class_Onumber__of(X2,X0))
| ~ class_Orderings_Olinorder(X2)
| ~ class_Int_Onumber(X2) ),
inference(cnf_transformation,[status(esa)],[f656_sk]) ).
fof(f676,axiom,
~ c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Int_OPls,c_Int_OMin),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_rel__simps_I3_J) ).
fof(f676_nnf,plain,
~ c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Int_OPls,c_Int_OMin),
inference(nnf_transformation,[status(thm)],[f676]) ).
fof(f676_sk,plain,
~ c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Int_OPls,c_Int_OMin),
inference(skolemisation,[status(esa)],[f676_nnf]) ).
cnf(c1030,plain,
~ c_Orderings_Oord__class_Oless(tc_Int_Oint,c_Int_OPls,c_Int_OMin),
inference(cnf_transformation,[status(esa)],[f676_sk]) ).
fof(f679,axiom,
c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OPls) != c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OMin),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_eq__number__of__Pls__Min) ).
fof(f679_nnf,plain,
c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OPls) != c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OMin),
inference(nnf_transformation,[status(thm)],[f679]) ).
fof(f679_sk,plain,
c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OPls) != c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OMin),
inference(skolemisation,[status(esa)],[f679_nnf]) ).
cnf(c1034,plain,
c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OPls) != c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OMin),
inference(cnf_transformation,[status(esa)],[f679_sk]) ).
fof(f701,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(f701_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)],[f701]) ).
fof(f701_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)],[f701_nnf]) ).
cnf(c1067,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)],[f701_sk]) ).
fof(f703,axiom,
! [T_a] :
( class_Int_Onumber__ring(T_a)
=> ~ c_Int_Oiszero(T_a,c_Int_Onumber__class_Onumber__of(T_a,c_Int_OMin)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_nonzero__number__of__Min) ).
fof(f703_nnf,plain,
! [T_a] :
( ~ c_Int_Oiszero(T_a,c_Int_Onumber__class_Onumber__of(T_a,c_Int_OMin))
| ~ class_Int_Onumber__ring(T_a) ),
inference(nnf_transformation,[status(thm)],[f703]) ).
fof(f703_sk,plain,
! [T_a] :
( ~ c_Int_Oiszero(T_a,c_Int_Onumber__class_Onumber__of(T_a,c_Int_OMin))
| ~ class_Int_Onumber__ring(T_a) ),
inference(skolemisation,[status(esa)],[f703_nnf]) ).
cnf(c1071,plain,
( ~ c_Int_Oiszero(X0,c_Int_Onumber__class_Onumber__of(X0,c_Int_OMin))
| ~ class_Int_Onumber__ring(X0) ),
inference(cnf_transformation,[status(esa)],[f703_sk]) ).
fof(f780,axiom,
! [V_nb_2,V_x_2,T_a] :
( class_Rings_Olinordered__idom(T_a)
=> ( c_Orderings_Oord__class_Oless__eq(T_a,c_Power_Opower__class_Opower(T_a,V_x_2,V_nb_2),c_Groups_Ozero__class_Ozero(T_a))
<=> ( ( ( V_x_2 = c_Groups_Ozero__class_Ozero(T_a)
& c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_nb_2) )
| ( c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,c_Groups_Ozero__class_Ozero(T_a))
& ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_nb_2) ) )
& V_nb_2 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_power__le__zero__eq) ).
fof(f780_nnf,plain,
! [V_nb_2,V_x_2,T_a] :
( ( ( ( ( V_x_2 != c_Groups_Ozero__class_Ozero(T_a)
| ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_nb_2) )
& ( ~ c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,c_Groups_Ozero__class_Ozero(T_a))
| c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_nb_2) ) )
| V_nb_2 = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| c_Orderings_Oord__class_Oless__eq(T_a,c_Power_Opower__class_Opower(T_a,V_x_2,V_nb_2),c_Groups_Ozero__class_Ozero(T_a)) )
& ( ( ( ( V_x_2 = c_Groups_Ozero__class_Ozero(T_a)
& c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_nb_2) )
| ( c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,c_Groups_Ozero__class_Ozero(T_a))
& ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_nb_2) ) )
& V_nb_2 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat) )
| ~ c_Orderings_Oord__class_Oless__eq(T_a,c_Power_Opower__class_Opower(T_a,V_x_2,V_nb_2),c_Groups_Ozero__class_Ozero(T_a)) ) )
| ~ class_Rings_Olinordered__idom(T_a) ),
inference(nnf_transformation,[status(thm)],[f780]) ).
fof(f780_sk,plain,
! [T_a,V_x_2,V_nb_2] :
( ( ( ( ( V_x_2 != c_Groups_Ozero__class_Ozero(T_a)
| ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_nb_2) )
& ( ~ c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,c_Groups_Ozero__class_Ozero(T_a))
| c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_nb_2) ) )
| V_nb_2 = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| c_Orderings_Oord__class_Oless__eq(T_a,c_Power_Opower__class_Opower(T_a,V_x_2,V_nb_2),c_Groups_Ozero__class_Ozero(T_a)) )
& ( ( ( ( V_x_2 = c_Groups_Ozero__class_Ozero(T_a)
& c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_nb_2) )
| ( c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,c_Groups_Ozero__class_Ozero(T_a))
& ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_nb_2) ) )
& V_nb_2 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat) )
| ~ c_Orderings_Oord__class_Oless__eq(T_a,c_Power_Opower__class_Opower(T_a,V_x_2,V_nb_2),c_Groups_Ozero__class_Ozero(T_a)) ) )
| ~ class_Rings_Olinordered__idom(T_a) ),
inference(skolemisation,[status(esa)],[f780_nnf]) ).
cnf(c1183,plain,
( X0 != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| ~ c_Orderings_Oord__class_Oless__eq(X2,c_Power_Opower__class_Opower(X2,X1,X0),c_Groups_Ozero__class_Ozero(X2))
| ~ class_Rings_Olinordered__idom(X2) ),
inference(cnf_transformation,[status(esa)],[f780_sk]) ).
fof(f789,axiom,
! [V_w_2,V_x_2,T_a] :
( class_Rings_Olinordered__idom(T_a)
=> ( c_Orderings_Oord__class_Oless__eq(T_a,c_Power_Opower__class_Opower(T_a,V_x_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2)),c_Groups_Ozero__class_Ozero(T_a))
<=> ( ( ( V_x_2 = c_Groups_Ozero__class_Ozero(T_a)
& c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2)) )
| ( c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,c_Groups_Ozero__class_Ozero(T_a))
& ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2)) ) )
& c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_power__le__zero__eq__number__of) ).
fof(f789_nnf,plain,
! [V_w_2,V_x_2,T_a] :
( ( ( ( ( V_x_2 != c_Groups_Ozero__class_Ozero(T_a)
| ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2)) )
& ( ~ c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,c_Groups_Ozero__class_Ozero(T_a))
| c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2)) ) )
| c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| c_Orderings_Oord__class_Oless__eq(T_a,c_Power_Opower__class_Opower(T_a,V_x_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2)),c_Groups_Ozero__class_Ozero(T_a)) )
& ( ( ( ( V_x_2 = c_Groups_Ozero__class_Ozero(T_a)
& c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2)) )
| ( c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,c_Groups_Ozero__class_Ozero(T_a))
& ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2)) ) )
& c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat) )
| ~ c_Orderings_Oord__class_Oless__eq(T_a,c_Power_Opower__class_Opower(T_a,V_x_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2)),c_Groups_Ozero__class_Ozero(T_a)) ) )
| ~ class_Rings_Olinordered__idom(T_a) ),
inference(nnf_transformation,[status(thm)],[f789]) ).
fof(f789_sk,plain,
! [T_a,V_x_2,V_w_2] :
( ( ( ( ( V_x_2 != c_Groups_Ozero__class_Ozero(T_a)
| ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2)) )
& ( ~ c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,c_Groups_Ozero__class_Ozero(T_a))
| c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2)) ) )
| c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2) = c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| c_Orderings_Oord__class_Oless__eq(T_a,c_Power_Opower__class_Opower(T_a,V_x_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2)),c_Groups_Ozero__class_Ozero(T_a)) )
& ( ( ( ( V_x_2 = c_Groups_Ozero__class_Ozero(T_a)
& c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2)) )
| ( c_Orderings_Oord__class_Oless__eq(T_a,V_x_2,c_Groups_Ozero__class_Ozero(T_a))
& ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2)) ) )
& c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat) )
| ~ c_Orderings_Oord__class_Oless__eq(T_a,c_Power_Opower__class_Opower(T_a,V_x_2,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,V_w_2)),c_Groups_Ozero__class_Ozero(T_a)) ) )
| ~ class_Rings_Olinordered__idom(T_a) ),
inference(skolemisation,[status(esa)],[f789_nnf]) ).
cnf(c1204,plain,
( c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,X0) != c_Groups_Ozero__class_Ozero(tc_Nat_Onat)
| ~ c_Orderings_Oord__class_Oless__eq(X2,c_Power_Opower__class_Opower(X2,X1,c_Int_Onumber__class_Onumber__of(tc_Nat_Onat,X0)),c_Groups_Ozero__class_Ozero(X2))
| ~ class_Rings_Olinordered__idom(X2) ),
inference(cnf_transformation,[status(esa)],[f789_sk]) ).
fof(f806,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(f806_nnf,plain,
c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) != c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
inference(nnf_transformation,[status(thm)],[f806]) ).
fof(f806_sk,plain,
c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) != c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
inference(skolemisation,[status(esa)],[f806_nnf]) ).
cnf(c1229,plain,
c_Groups_Ozero__class_Ozero(tc_RealDef_Oreal) != c_Groups_Oone__class_Oone(tc_RealDef_Oreal),
inference(cnf_transformation,[status(esa)],[f806_sk]) ).
fof(f835,axiom,
~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_odd__1__nat) ).
fof(f835_nnf,plain,
~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat)),
inference(nnf_transformation,[status(thm)],[f835]) ).
fof(f835_sk,plain,
~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat)),
inference(skolemisation,[status(esa)],[f835_nnf]) ).
cnf(c1265,plain,
~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Groups_Oone__class_Oone(tc_Nat_Onat)),
inference(cnf_transformation,[status(esa)],[f835_sk]) ).
fof(f846,axiom,
! [V_nb_2] :
( c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),V_nb_2)
=> ( c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_nb_2)
<=> ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,V_nb_2,c_Groups_Oone__class_Oone(tc_Nat_Onat))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_even__num__iff) ).
fof(f846_nnf,plain,
! [V_nb_2] :
( ( ( c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,V_nb_2,c_Groups_Oone__class_Oone(tc_Nat_Onat)))
| c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_nb_2) )
& ( ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,V_nb_2,c_Groups_Oone__class_Oone(tc_Nat_Onat)))
| ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_nb_2) ) )
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),V_nb_2) ),
inference(nnf_transformation,[status(thm)],[f846]) ).
fof(f846_sk,plain,
! [V_nb_2] :
( ( ( c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,V_nb_2,c_Groups_Oone__class_Oone(tc_Nat_Onat)))
| c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_nb_2) )
& ( ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,V_nb_2,c_Groups_Oone__class_Oone(tc_Nat_Onat)))
| ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_nb_2) ) )
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),V_nb_2) ),
inference(skolemisation,[status(esa)],[f846_nnf]) ).
cnf(c1278,plain,
( ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,c_Groups_Ominus__class_Ominus(tc_Nat_Onat,X0,c_Groups_Oone__class_Oone(tc_Nat_Onat)))
| ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,X0)
| ~ c_Orderings_Oord__class_Oless(tc_Nat_Onat,c_Groups_Ozero__class_Ozero(tc_Nat_Onat),X0) ),
inference(cnf_transformation,[status(esa)],[f846_sk]) ).
fof(f942,axiom,
! [V_x_2] :
( c_Divides_Odiv__class_Omod(tc_Int_Oint,V_x_2,c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) != c_Groups_Ozero__class_Ozero(tc_Int_Oint)
<=> c_Divides_Odiv__class_Omod(tc_Int_Oint,V_x_2,c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = c_Groups_Oone__class_Oone(tc_Int_Oint) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_neq__one__mod__two) ).
fof(f942_nnf,plain,
! [V_x_2] :
( ( c_Divides_Odiv__class_Omod(tc_Int_Oint,V_x_2,c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) != c_Groups_Oone__class_Oone(tc_Int_Oint)
| c_Divides_Odiv__class_Omod(tc_Int_Oint,V_x_2,c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) != c_Groups_Ozero__class_Ozero(tc_Int_Oint) )
& ( c_Divides_Odiv__class_Omod(tc_Int_Oint,V_x_2,c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = c_Groups_Oone__class_Oone(tc_Int_Oint)
| c_Divides_Odiv__class_Omod(tc_Int_Oint,V_x_2,c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = c_Groups_Ozero__class_Ozero(tc_Int_Oint) ) ),
inference(nnf_transformation,[status(thm)],[f942]) ).
fof(f942_sk,plain,
! [V_x_2] :
( ( c_Divides_Odiv__class_Omod(tc_Int_Oint,V_x_2,c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) != c_Groups_Oone__class_Oone(tc_Int_Oint)
| c_Divides_Odiv__class_Omod(tc_Int_Oint,V_x_2,c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) != c_Groups_Ozero__class_Ozero(tc_Int_Oint) )
& ( c_Divides_Odiv__class_Omod(tc_Int_Oint,V_x_2,c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = c_Groups_Oone__class_Oone(tc_Int_Oint)
| c_Divides_Odiv__class_Omod(tc_Int_Oint,V_x_2,c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) = c_Groups_Ozero__class_Ozero(tc_Int_Oint) ) ),
inference(skolemisation,[status(esa)],[f942_nnf]) ).
cnf(c1446,plain,
( c_Divides_Odiv__class_Omod(tc_Int_Oint,X0,c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) != c_Groups_Oone__class_Oone(tc_Int_Oint)
| c_Divides_Odiv__class_Omod(tc_Int_Oint,X0,c_Int_Onumber__class_Onumber__of(tc_Int_Oint,c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))) != c_Groups_Ozero__class_Ozero(tc_Int_Oint) ),
inference(cnf_transformation,[status(esa)],[f942_sk]) ).
fof(f969,axiom,
! [V_x_2] :
( ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_x_2)
<=> c_Divides_Odiv__class_Omod(tc_Nat_Onat,V_x_2,c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))) = c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_odd__nat__equiv__def) ).
fof(f969_nnf,plain,
! [V_x_2] :
( ( c_Divides_Odiv__class_Omod(tc_Nat_Onat,V_x_2,c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))) != c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))
| ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_x_2) )
& ( c_Divides_Odiv__class_Omod(tc_Nat_Onat,V_x_2,c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))) = c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))
| c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_x_2) ) ),
inference(nnf_transformation,[status(thm)],[f969]) ).
fof(f969_sk,plain,
! [V_x_2] :
( ( c_Divides_Odiv__class_Omod(tc_Nat_Onat,V_x_2,c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))) != c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))
| ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_x_2) )
& ( c_Divides_Odiv__class_Omod(tc_Nat_Onat,V_x_2,c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))) = c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))
| c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,V_x_2) ) ),
inference(skolemisation,[status(esa)],[f969_nnf]) ).
cnf(c1479,plain,
( c_Divides_Odiv__class_Omod(tc_Nat_Onat,X0,c_Nat_OSuc(c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat)))) != c_Nat_OSuc(c_Groups_Ozero__class_Ozero(tc_Nat_Onat))
| ~ c_Parity_Oeven__odd__class_Oeven(tc_Nat_Onat,X0) ),
inference(cnf_transformation,[status(esa)],[f969_sk]) ).
cnf(goal_0,negated_conjecture,
true != false,
inference(equality_encoding,[status(esa)],[c1,c3,c11,c12,c13,c14,c82,c93,c117,c118,c202,c204,c207,c208,c242,c243,c244,c245,c246,c247,c260,c272,c310,c314,c315,c371,c384,c399,c400,c406,c410,c413,c439,c444,c449,c467,c469,c470,c471,c492,c502,c503,c518,c531,c630,c650,c652,c654,c655,c657,c663,c664,c665,c725,c733,c794,c795,c810,c811,c818,c819,c841,c856,c858,c898,c900,c925,c931,c947,c994,c1030,c1034,c1067,c1071,c1183,c1204,c1229,c1265,c1278,c1446,c1479,c1693]) ).
cnf(g0_0,plain,
true != true,
inference(rw,[status(thm)],[goal_0,t164]) ).
cnf(contradiction_0,plain,
$false,
inference(trivial_inequality_removal,[status(thm)],[g0_0]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW196+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.04 % Command : run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 0.11/0.37 % Computer : n015.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Thu Sep 24 21:45:56 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_findproof /export/starexec/sandbox2/benchmark/theBenchmark.p 300
% 66.08/11.61 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 66.08/11.61 % SZS output start Proof for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------