%------------------------------------------------------------------------------
% File : Drodi---4.1.1
% Problem : SWV822-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n016.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 : Thu Sep 24 02:49:37 PM UTC 2026
% Result : Unsatisfiable 70.31s 9.38s
% Output : CNFRefutation 70.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 103
% Syntax : Number of formulae : 326 ( 45 unt; 55 def)
% Number of atoms : 833 ( 161 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 903 ( 396 ~; 452 |; 0 &)
% ( 55 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 64 ( 62 usr; 56 prp; 0-4 aty)
% Number of functors : 21 ( 21 usr; 9 con; 0-4 aty)
% Number of variables : 452 ( 452 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [V_m,V_n] :
( ~ c_lessequals(V_n,V_m,tc_nat)
| c_HOL_Ominus__class_Ominus(c_Suc(V_m),V_n,tc_nat) = c_Suc(c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f33,axiom,
! [V_n,V_m] :
( ~ c_HOL_Oord__class_Oless(V_n,V_m,tc_nat)
| c_lessequals(c_Suc(V_n),V_m,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f36,axiom,
! [T_a,V_b,V_a,V_c] :
( ~ c_lessequals(c_HOL_Ozero__class_Ozero(T_a),V_c,T_a)
| ~ c_lessequals(V_b,V_a,T_a)
| c_lessequals(V_b,c_HOL_Oplus__class_Oplus(V_a,V_c,T_a),T_a)
| ~ class_OrderedGroup_Ocomm__monoid__add(T_a)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f37,axiom,
! [T_a,V_b,V_a,V_c] :
( ~ c_lessequals(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a)
| ~ c_lessequals(V_b,V_c,T_a)
| c_lessequals(V_b,c_HOL_Oplus__class_Oplus(V_a,V_c,T_a),T_a)
| ~ class_OrderedGroup_Ocomm__monoid__add(T_a)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f68,axiom,
! [V_m,V_n] :
( c_lessequals(V_m,V_n,tc_nat)
| c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat) != c_HOL_Ozero__class_Ozero(tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f72,axiom,
! [T_a,V_b,V_a,V_c] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a)
| ~ c_lessequals(V_b,V_c,T_a)
| c_HOL_Oord__class_Oless(V_b,c_HOL_Oplus__class_Oplus(V_a,V_c,T_a),T_a)
| ~ class_OrderedGroup_Ocomm__monoid__add(T_a)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f73,axiom,
c_HOL_Oplus__class_Oplus(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f81,axiom,
! [V_n] :
( ~ c_HOL_Oord__class_Oless(V_n,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat)
| V_n = c_HOL_Ozero__class_Ozero(tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f84,axiom,
! [T_a,V_x,V_y] :
( c_Orderings_Oord__class_Omin(V_x,c_Orderings_Oord__class_Omin(V_x,V_y,T_a),T_a) = c_Orderings_Oord__class_Omin(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f85,axiom,
! [V_i,V_u,V_m,V_j,V_n] :
( ~ c_lessequals(V_i,V_j,tc_nat)
| c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_i,V_u,tc_nat),V_m,tc_nat),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_j,V_u,tc_nat),V_n,tc_nat),tc_nat) = c_HOL_Ominus__class_Ominus(V_m,c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(V_j,V_i,tc_nat),V_u,tc_nat),V_n,tc_nat),tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f93,axiom,
! [V_m,V_n] :
( ~ c_HOL_Oord__class_Oless(V_m,c_Suc(V_n),tc_nat)
| c_lessequals(V_m,V_n,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f133,axiom,
! [V_k,V_m,V_n] :
( V_m = V_n
| V_k = c_HOL_Ozero__class_Ozero(tc_nat)
| c_HOL_Otimes__class_Otimes(V_k,V_m,tc_nat) != c_HOL_Otimes__class_Otimes(V_k,V_n,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f134,axiom,
! [V_m,V_k,V_n] :
( V_m = V_n
| V_k = c_HOL_Ozero__class_Ozero(tc_nat)
| c_HOL_Otimes__class_Otimes(V_m,V_k,tc_nat) != c_HOL_Otimes__class_Otimes(V_n,V_k,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f143,axiom,
! [V_n] : c_Orderings_Oord__class_Omin(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f173,axiom,
! [V_m,V_n] :
( V_n = c_HOL_Ozero__class_Ozero(tc_nat)
| V_m = c_HOL_Ozero__class_Ozero(tc_nat)
| c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) != c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f209,axiom,
c_HOL_Otimes__class_Otimes(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f240,axiom,
! [V_m,V_n] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat)
| c_HOL_Oord__class_Oless(c_Divides_Odiv__class_Omod(V_m,V_n,tc_nat),V_n,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f288,axiom,
! [V_n] : c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(V_n),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f470,axiom,
! [V_m,V_n,V_k] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_k,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_k,V_m,tc_nat),c_HOL_Otimes__class_Otimes(V_k,V_n,tc_nat),tc_nat)
| c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f471,axiom,
! [V_k,V_m,V_n] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_k,tc_nat)
| ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat)
| c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_k,V_m,tc_nat),c_HOL_Otimes__class_Otimes(V_k,V_n,tc_nat),tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f487,axiom,
! [V_m] : c_lessequals(V_m,c_HOL_Otimes__class_Otimes(V_m,c_HOL_Otimes__class_Otimes(V_m,V_m,tc_nat),tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f500,axiom,
! [V_m] : c_HOL_Oplus__class_Oplus(V_m,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = V_m,
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f571,axiom,
! [V_m,V_n] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_m,tc_nat)
| c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat),V_m,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f581,axiom,
! [V_m,V_n] :
( V_m = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))
| V_n = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))
| c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat) != c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f620,axiom,
! [V_n,V_m] :
( c_lessequals(V_m,V_n,tc_nat)
| c_lessequals(V_n,V_m,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f630,axiom,
! [V_m,V_n] :
( ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat)
| c_HOL_Oord__class_Oless(V_m,c_Suc(V_n),tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f633,axiom,
! [V_c,V_s,V_m,V_t,V_n] :
( ~ c_Natural_Oevaln(V_c,V_s,V_n,V_t)
| ~ c_lessequals(V_n,V_m,tc_nat)
| c_Natural_Oevaln(V_c,V_s,V_m,V_t) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f639,axiom,
! [V_n] : ~ c_lessequals(c_Suc(V_n),V_n,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f641,axiom,
! [V_m,V_n] :
( ~ c_lessequals(c_Suc(V_m),V_n,tc_nat)
| c_lessequals(V_m,V_n,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f642,axiom,
! [V_i,V_k,V_j] :
( ~ c_HOL_Oord__class_Oless(V_i,V_j,tc_nat)
| ~ c_HOL_Oord__class_Oless(V_j,V_k,tc_nat)
| c_HOL_Oord__class_Oless(c_Suc(V_i),V_k,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f646,axiom,
! [V_nat_H] : c_Suc(V_nat_H) != c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f650,axiom,
! [V_m,V_n] :
( c_HOL_Oord__class_Oless(V_n,V_m,tc_nat)
| ~ c_HOL_Oord__class_Oless(V_n,c_Suc(V_m),tc_nat)
| V_m = V_n ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f652,axiom,
! [V_m,V_n] : c_HOL_Ominus__class_Ominus(c_Suc(V_m),c_Suc(V_n),tc_nat) = c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f655,axiom,
! [V_x,V_y] :
( V_x = V_y
| c_Suc(V_x) != c_Suc(V_y) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f656,axiom,
! [V_P,V_s,V_n,V_s1] :
( ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(V_P),V_s,V_n,V_s1)
| c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(V_P),tc_Com_Ocom),V_s,c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(V_P,V_n,V_s,V_s1),V_s1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f669,axiom,
! [V_m,V_n] : c_HOL_Oplus__class_Oplus(c_Suc(V_m),V_n,tc_nat) = c_HOL_Oplus__class_Oplus(V_m,c_Suc(V_n),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f670,axiom,
! [V_m,V_n] :
( ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat)
| c_Suc(V_m) = V_n
| c_HOL_Oord__class_Oless(c_Suc(V_m),V_n,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f672,axiom,
! [V_n,V_m] :
( c_lessequals(V_m,V_n,tc_nat)
| c_lessequals(c_Suc(V_n),V_m,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f673,axiom,
! [V_pn,V_s0,V_n,V_s1] :
( ~ c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(V_pn),tc_Com_Ocom),V_s0,V_n,V_s1)
| c_Natural_Oevaln(c_Com_Ocom_OBODY(V_pn),V_s0,c_Suc(V_n),V_s1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f678,axiom,
! [V_m,V_n] : c_Orderings_Oord__class_Omin(c_Suc(V_m),c_Suc(V_n),tc_nat) = c_Suc(c_Orderings_Oord__class_Omin(V_m,V_n,tc_nat)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f679,axiom,
! [V_n,V_P,V_s,V_s1] :
( ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(V_P),V_s,V_n,V_s1)
| V_n = c_Suc(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(V_P,V_n,V_s,V_s1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f691,negated_conjecture,
( hBOOL(hAPP(hAPP(v_P,v_x),v_xa))
| hBOOL(hAPP(hAPP(v_P,v_x),v_xa)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f695,negated_conjecture,
( c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),v_xa,v_n,v_xb)
| c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),v_xa,c_Suc(v_n),v_xb) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f699,negated_conjecture,
( ~ hBOOL(hAPP(hAPP(v_Q,v_x),v_xb))
| ~ hBOOL(hAPP(hAPP(v_Q,v_x),v_xb)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f700,negated_conjecture,
! [V_Za,V_s_Ha,V_sa,V_Z,V_s_H,V_s] :
( ~ hBOOL(hAPP(hAPP(v_P,V_Z),V_s))
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),V_s,c_Suc(v_n),V_s_H)
| hBOOL(hAPP(hAPP(v_Q,V_Z),V_s_H))
| ~ hBOOL(hAPP(hAPP(v_P,V_Za),V_sa))
| ~ c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),V_sa,v_n,V_s_Ha)
| hBOOL(hAPP(hAPP(v_Q,V_Za),V_s_Ha)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f702,axiom,
class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f718,axiom,
class_OrderedGroup_Ocomm__monoid__add(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f726,axiom,
class_Orderings_Olinorder(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p') ).
fof(f729,plain,
! [X0,X1] :
( ~ c_lessequals(X1,X0,tc_nat)
| c_HOL_Ominus__class_Ominus(c_Suc(X0),X1,tc_nat) = c_Suc(c_HOL_Ominus__class_Ominus(X0,X1,tc_nat)) ),
inference(cnf_transformation,[status(thm)],[f2]) ).
fof(f781,plain,
! [X0,X1] :
( c_lessequals(c_Suc(X0),X1,tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_nat) ),
inference(cnf_transformation,[status(thm)],[f33]) ).
fof(f784,plain,
! [T_a,V_c] :
( ~ c_lessequals(c_HOL_Ozero__class_Ozero(T_a),V_c,T_a)
| ! [V_b,V_a] :
( ~ c_lessequals(V_b,V_a,T_a)
| c_lessequals(V_b,c_HOL_Oplus__class_Oplus(V_a,V_c,T_a),T_a)
| ~ class_OrderedGroup_Ocomm__monoid__add(T_a)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) ) ),
inference(miniscoping,[status(thm)],[f36]) ).
fof(f785,plain,
! [X0,X1,X2,X3] :
( ~ class_OrderedGroup_Ocomm__monoid__add(X2)
| c_lessequals(X0,c_HOL_Oplus__class_Oplus(X1,X3,X2),X2)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(X2),X3,X2)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(X2)
| ~ c_lessequals(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f784]) ).
fof(f786,plain,
! [T_a,V_a] :
( ~ c_lessequals(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a)
| ! [V_b,V_c] :
( ~ c_lessequals(V_b,V_c,T_a)
| c_lessequals(V_b,c_HOL_Oplus__class_Oplus(V_a,V_c,T_a),T_a)
| ~ class_OrderedGroup_Ocomm__monoid__add(T_a)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) ) ),
inference(miniscoping,[status(thm)],[f37]) ).
fof(f787,plain,
! [X0,X1,X2,X3] :
( ~ class_OrderedGroup_Ocomm__monoid__add(X0)
| c_lessequals(X2,c_HOL_Oplus__class_Oplus(X1,X3,X0),X0)
| ~ c_lessequals(X2,X3,X0)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(X0),X1,X0)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(X0) ),
inference(cnf_transformation,[status(thm)],[f786]) ).
fof(f842,plain,
! [X0,X1] :
( c_HOL_Ozero__class_Ozero(tc_nat) != c_HOL_Ominus__class_Ominus(X0,X1,tc_nat)
| c_lessequals(X0,X1,tc_nat) ),
inference(cnf_transformation,[status(thm)],[f68]) ).
fof(f849,plain,
! [T_a,V_a] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(T_a),V_a,T_a)
| ! [V_b,V_c] :
( ~ c_lessequals(V_b,V_c,T_a)
| c_HOL_Oord__class_Oless(V_b,c_HOL_Oplus__class_Oplus(V_a,V_c,T_a),T_a)
| ~ class_OrderedGroup_Ocomm__monoid__add(T_a)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(T_a) ) ),
inference(miniscoping,[status(thm)],[f72]) ).
fof(f850,plain,
! [X0,X1,X2,X3] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(X0),X2,X0)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(X0)
| ~ c_lessequals(X1,X3,X0)
| c_HOL_Oord__class_Oless(X1,c_HOL_Oplus__class_Oplus(X2,X3,X0),X0)
| ~ class_OrderedGroup_Ocomm__monoid__add(X0) ),
inference(cnf_transformation,[status(thm)],[f849]) ).
fof(f851,plain,
c_HOL_Oplus__class_Oplus(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),
inference(cnf_transformation,[status(thm)],[f73]) ).
fof(f864,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(X0,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = X0 ),
inference(cnf_transformation,[status(thm)],[f81]) ).
fof(f867,plain,
! [T_a] :
( ! [V_x,V_y] : c_Orderings_Oord__class_Omin(V_x,c_Orderings_Oord__class_Omin(V_x,V_y,T_a),T_a) = c_Orderings_Oord__class_Omin(V_x,V_y,T_a)
| ~ class_Orderings_Olinorder(T_a) ),
inference(miniscoping,[status(thm)],[f84]) ).
fof(f868,plain,
! [X0,X1,X2] :
( ~ class_Orderings_Olinorder(X2)
| c_Orderings_Oord__class_Omin(X0,c_Orderings_Oord__class_Omin(X0,X1,X2),X2) = c_Orderings_Oord__class_Omin(X0,X1,X2) ),
inference(cnf_transformation,[status(thm)],[f867]) ).
fof(f869,plain,
! [V_i,V_j] :
( ~ c_lessequals(V_i,V_j,tc_nat)
| ! [V_u,V_m,V_n] : c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_i,V_u,tc_nat),V_m,tc_nat),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(V_j,V_u,tc_nat),V_n,tc_nat),tc_nat) = c_HOL_Ominus__class_Ominus(V_m,c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(V_j,V_i,tc_nat),V_u,tc_nat),V_n,tc_nat),tc_nat) ),
inference(miniscoping,[status(thm)],[f85]) ).
fof(f870,plain,
! [X0,X1,X2,X3,X4] :
( c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X0,X2,tc_nat),X3,tc_nat),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X1,X2,tc_nat),X4,tc_nat),tc_nat) = c_HOL_Ominus__class_Ominus(X3,c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(X1,X0,tc_nat),X2,tc_nat),X4,tc_nat),tc_nat)
| ~ c_lessequals(X0,X1,tc_nat) ),
inference(cnf_transformation,[status(thm)],[f869]) ).
fof(f884,plain,
! [X0,X1] :
( c_lessequals(X0,X1,tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,c_Suc(X1),tc_nat) ),
inference(cnf_transformation,[status(thm)],[f93]) ).
fof(f946,plain,
! [V_m,V_n] :
( V_m = V_n
| ! [V_k] :
( V_k = c_HOL_Ozero__class_Ozero(tc_nat)
| c_HOL_Otimes__class_Otimes(V_k,V_m,tc_nat) != c_HOL_Otimes__class_Otimes(V_k,V_n,tc_nat) ) ),
inference(miniscoping,[status(thm)],[f133]) ).
fof(f947,plain,
! [X0,X1,X2] :
( c_HOL_Otimes__class_Otimes(X0,X2,tc_nat) != c_HOL_Otimes__class_Otimes(X0,X1,tc_nat)
| X1 = X2
| X0 = c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(cnf_transformation,[status(thm)],[f946]) ).
fof(f948,plain,
! [V_m,V_n] :
( V_m = V_n
| ! [V_k] :
( V_k = c_HOL_Ozero__class_Ozero(tc_nat)
| c_HOL_Otimes__class_Otimes(V_m,V_k,tc_nat) != c_HOL_Otimes__class_Otimes(V_n,V_k,tc_nat) ) ),
inference(miniscoping,[status(thm)],[f134]) ).
fof(f949,plain,
! [X0,X1,X2] :
( c_HOL_Ozero__class_Ozero(tc_nat) = X2
| c_HOL_Otimes__class_Otimes(X1,X2,tc_nat) != c_HOL_Otimes__class_Otimes(X0,X2,tc_nat)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f948]) ).
fof(f966,plain,
! [X0] : c_Orderings_Oord__class_Omin(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat),
inference(cnf_transformation,[status(thm)],[f143]) ).
fof(f1007,plain,
! [V_n] :
( V_n = c_HOL_Ozero__class_Ozero(tc_nat)
| ! [V_m] :
( V_m = c_HOL_Ozero__class_Ozero(tc_nat)
| c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) != c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat) ) ),
inference(miniscoping,[status(thm)],[f173]) ).
fof(f1008,plain,
! [X0,X1] :
( c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) != c_HOL_Oplus__class_Oplus(X0,X1,tc_nat)
| X1 = c_HOL_Ozero__class_Ozero(tc_nat)
| X0 = c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(cnf_transformation,[status(thm)],[f1007]) ).
fof(f1068,plain,
c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = c_HOL_Otimes__class_Otimes(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat),
inference(cnf_transformation,[status(thm)],[f209]) ).
fof(f1121,plain,
! [V_n] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat)
| ! [V_m] : c_HOL_Oord__class_Oless(c_Divides_Odiv__class_Omod(V_m,V_n,tc_nat),V_n,tc_nat) ),
inference(miniscoping,[status(thm)],[f240]) ).
fof(f1122,plain,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X1,tc_nat)
| c_HOL_Oord__class_Oless(c_Divides_Odiv__class_Omod(X0,X1,tc_nat),X1,tc_nat) ),
inference(cnf_transformation,[status(thm)],[f1121]) ).
fof(f1196,plain,
! [X0] : c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(X0),tc_nat),
inference(cnf_transformation,[status(thm)],[f288]) ).
fof(f1498,plain,
! [V_k] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_k,tc_nat)
| ! [V_m,V_n] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_k,V_m,tc_nat),c_HOL_Otimes__class_Otimes(V_k,V_n,tc_nat),tc_nat)
| c_HOL_Oord__class_Oless(V_m,V_n,tc_nat) ) ),
inference(miniscoping,[status(thm)],[f470]) ).
fof(f1499,plain,
! [X0,X1,X2] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X2,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(X2,X0,tc_nat),c_HOL_Otimes__class_Otimes(X2,X1,tc_nat),tc_nat)
| c_HOL_Oord__class_Oless(X0,X1,tc_nat) ),
inference(cnf_transformation,[status(thm)],[f1498]) ).
fof(f1500,plain,
! [V_k] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_k,tc_nat)
| ! [V_m,V_n] :
( ~ c_HOL_Oord__class_Oless(V_m,V_n,tc_nat)
| c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(V_k,V_m,tc_nat),c_HOL_Otimes__class_Otimes(V_k,V_n,tc_nat),tc_nat) ) ),
inference(miniscoping,[status(thm)],[f471]) ).
fof(f1501,plain,
! [X0,X1,X2] :
( ~ c_HOL_Oord__class_Oless(X1,X2,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)
| c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(X0,X1,tc_nat),c_HOL_Otimes__class_Otimes(X0,X2,tc_nat),tc_nat) ),
inference(cnf_transformation,[status(thm)],[f1500]) ).
fof(f1532,plain,
! [X0] : c_lessequals(X0,c_HOL_Otimes__class_Otimes(X0,c_HOL_Otimes__class_Otimes(X0,X0,tc_nat),tc_nat),tc_nat),
inference(cnf_transformation,[status(thm)],[f487]) ).
fof(f1554,plain,
! [X0] : c_HOL_Oplus__class_Oplus(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = X0,
inference(cnf_transformation,[status(thm)],[f500]) ).
fof(f1669,plain,
! [V_n] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_n,tc_nat)
| ! [V_m] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),V_m,tc_nat)
| c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(V_m,V_n,tc_nat),V_m,tc_nat) ) ),
inference(miniscoping,[status(thm)],[f571]) ).
fof(f1670,plain,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X1,tc_nat)
| c_HOL_Oord__class_Oless(c_HOL_Ominus__class_Ominus(X1,X0,tc_nat),X1,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) ),
inference(cnf_transformation,[status(thm)],[f1669]) ).
fof(f1688,plain,
! [V_m] :
( V_m = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))
| ! [V_n] :
( V_n = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))
| c_HOL_Oplus__class_Oplus(V_m,V_n,tc_nat) != c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ) ),
inference(miniscoping,[status(thm)],[f581]) ).
fof(f1689,plain,
! [X0,X1] :
( c_HOL_Oplus__class_Oplus(X1,X0,tc_nat) != c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))
| c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = X1
| c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = X0 ),
inference(cnf_transformation,[status(thm)],[f1688]) ).
fof(f1751,plain,
! [X0,X1] :
( c_lessequals(X1,X0,tc_nat)
| c_lessequals(X0,X1,tc_nat) ),
inference(cnf_transformation,[status(thm)],[f620]) ).
fof(f1762,plain,
! [X0,X1] :
( c_HOL_Oord__class_Oless(X0,c_Suc(X1),tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_nat) ),
inference(cnf_transformation,[status(thm)],[f630]) ).
fof(f1765,plain,
! [V_c,V_s,V_t,V_n] :
( ~ c_Natural_Oevaln(V_c,V_s,V_n,V_t)
| ! [V_m] :
( ~ c_lessequals(V_n,V_m,tc_nat)
| c_Natural_Oevaln(V_c,V_s,V_m,V_t) ) ),
inference(miniscoping,[status(thm)],[f633]) ).
fof(f1766,plain,
! [X0,X1,X2,X3,X4] :
( ~ c_Natural_Oevaln(X2,X3,X0,X4)
| c_Natural_Oevaln(X2,X3,X1,X4)
| ~ c_lessequals(X0,X1,tc_nat) ),
inference(cnf_transformation,[status(thm)],[f1765]) ).
fof(f1772,plain,
! [X0] : ~ c_lessequals(c_Suc(X0),X0,tc_nat),
inference(cnf_transformation,[status(thm)],[f639]) ).
fof(f1774,plain,
! [X0,X1] :
( ~ c_lessequals(c_Suc(X0),X1,tc_nat)
| c_lessequals(X0,X1,tc_nat) ),
inference(cnf_transformation,[status(thm)],[f641]) ).
fof(f1775,plain,
! [V_i,V_j] :
( ~ c_HOL_Oord__class_Oless(V_i,V_j,tc_nat)
| ! [V_k] :
( ~ c_HOL_Oord__class_Oless(V_j,V_k,tc_nat)
| c_HOL_Oord__class_Oless(c_Suc(V_i),V_k,tc_nat) ) ),
inference(miniscoping,[status(thm)],[f642]) ).
fof(f1776,plain,
! [X0,X1,X2] :
( ~ c_HOL_Oord__class_Oless(X2,X1,tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,X2,tc_nat)
| c_HOL_Oord__class_Oless(c_Suc(X0),X1,tc_nat) ),
inference(cnf_transformation,[status(thm)],[f1775]) ).
fof(f1780,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_nat) != c_Suc(X0),
inference(cnf_transformation,[status(thm)],[f646]) ).
fof(f1784,plain,
! [X0,X1] :
( c_HOL_Oord__class_Oless(X0,X1,tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,c_Suc(X1),tc_nat)
| X0 = X1 ),
inference(cnf_transformation,[status(thm)],[f650]) ).
fof(f1786,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(c_Suc(X0),c_Suc(X1),tc_nat) = c_HOL_Ominus__class_Ominus(X0,X1,tc_nat),
inference(cnf_transformation,[status(thm)],[f652]) ).
fof(f1789,plain,
! [X0,X1] :
( X0 = X1
| c_Suc(X0) != c_Suc(X1) ),
inference(cnf_transformation,[status(thm)],[f655]) ).
fof(f1790,plain,
! [X0,X1,X2,X3] :
( c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(X0),tc_Com_Ocom),X1,c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(X0,X2,X1,X3),X3)
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(X0),X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f656]) ).
fof(f1806,plain,
! [X0,X1] : c_HOL_Oplus__class_Oplus(c_Suc(X0),X1,tc_nat) = c_HOL_Oplus__class_Oplus(X0,c_Suc(X1),tc_nat),
inference(cnf_transformation,[status(thm)],[f669]) ).
fof(f1807,plain,
! [X0,X1] :
( X1 = c_Suc(X0)
| ~ c_HOL_Oord__class_Oless(X0,X1,tc_nat)
| c_HOL_Oord__class_Oless(c_Suc(X0),X1,tc_nat) ),
inference(cnf_transformation,[status(thm)],[f670]) ).
fof(f1809,plain,
! [X0,X1] :
( c_lessequals(X1,X0,tc_nat)
| c_lessequals(c_Suc(X0),X1,tc_nat) ),
inference(cnf_transformation,[status(thm)],[f672]) ).
fof(f1810,plain,
! [X0,X1,X2,X3] :
( ~ c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(X0),tc_Com_Ocom),X1,X2,X3)
| c_Natural_Oevaln(c_Com_Ocom_OBODY(X0),X1,c_Suc(X2),X3) ),
inference(cnf_transformation,[status(thm)],[f673]) ).
fof(f1815,plain,
! [X0,X1] : c_Suc(c_Orderings_Oord__class_Omin(X0,X1,tc_nat)) = c_Orderings_Oord__class_Omin(c_Suc(X0),c_Suc(X1),tc_nat),
inference(cnf_transformation,[status(thm)],[f678]) ).
fof(f1816,plain,
! [X0,X1,X2,X3] :
( c_Suc(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(X0,X2,X1,X3)) = X2
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(X0),X1,X2,X3) ),
inference(cnf_transformation,[status(thm)],[f679]) ).
fof(f1831,plain,
( hBOOL(hAPP(hAPP(v_P,v_x),v_xa))
| hBOOL(hAPP(hAPP(v_P,v_x),v_xa)) ),
inference(cnf_transformation,[status(thm)],[f691]) ).
fof(f1835,plain,
( c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),v_xa,v_n,v_xb)
| c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),v_xa,c_Suc(v_n),v_xb) ),
inference(cnf_transformation,[status(thm)],[f695]) ).
fof(f1839,plain,
( ~ hBOOL(hAPP(hAPP(v_Q,v_x),v_xb))
| ~ hBOOL(hAPP(hAPP(v_Q,v_x),v_xb)) ),
inference(cnf_transformation,[status(thm)],[f699]) ).
fof(f1840,plain,
! [V_Z,V_s] :
( ~ hBOOL(hAPP(hAPP(v_P,V_Z),V_s))
| ! [V_s_H] :
( ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),V_s,c_Suc(v_n),V_s_H)
| hBOOL(hAPP(hAPP(v_Q,V_Z),V_s_H))
| ! [V_Za,V_sa] :
( ~ hBOOL(hAPP(hAPP(v_P,V_Za),V_sa))
| ! [V_s_Ha] :
( ~ c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),V_sa,v_n,V_s_Ha)
| hBOOL(hAPP(hAPP(v_Q,V_Za),V_s_Ha)) ) ) ) ),
inference(miniscoping,[status(thm)],[f700]) ).
fof(f1841,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ hBOOL(hAPP(hAPP(v_P,X3),X5))
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X5,c_Suc(v_n),X4)
| hBOOL(hAPP(hAPP(v_Q,X3),X4))
| ~ hBOOL(hAPP(hAPP(v_P,X0),X2))
| ~ c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),X2,v_n,X1)
| hBOOL(hAPP(hAPP(v_Q,X0),X1)) ),
inference(cnf_transformation,[status(thm)],[f1840]) ).
fof(f1843,plain,
class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat),
inference(cnf_transformation,[status(thm)],[f702]) ).
fof(f1859,plain,
class_OrderedGroup_Ocomm__monoid__add(tc_nat),
inference(cnf_transformation,[status(thm)],[f718]) ).
fof(f1867,plain,
class_Orderings_Olinorder(tc_nat),
inference(cnf_transformation,[status(thm)],[f726]) ).
fof(f1869,definition,
( sQ0_spl
<=> hBOOL(hAPP(hAPP(v_P,v_x),v_xa)) ),
introduced(definition,[new_symbols(definition,[sQ0_spl])],[split_symbol_definition]) ).
fof(f1870,plain,
( ~ sQ0_spl
| hBOOL(hAPP(hAPP(v_P,v_x),v_xa)) ),
inference(component_clause,[status(thm)],[f1869]) ).
fof(f1872,plain,
sQ0_spl,
inference(split_clause,[status(thm)],[f1831,f1869]) ).
fof(f1873,definition,
( sQ1_spl
<=> c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),v_xa,c_Suc(v_n),v_xb) ),
introduced(definition,[new_symbols(definition,[sQ1_spl])],[split_symbol_definition]) ).
fof(f1874,plain,
( ~ sQ1_spl
| c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),v_xa,c_Suc(v_n),v_xb) ),
inference(component_clause,[status(thm)],[f1873]) ).
fof(f1877,definition,
( sQ2_spl
<=> hBOOL(hAPP(hAPP(v_Q,v_x),v_xb)) ),
introduced(definition,[new_symbols(definition,[sQ2_spl])],[split_symbol_definition]) ).
fof(f1879,plain,
( sQ2_spl
| ~ hBOOL(hAPP(hAPP(v_Q,v_x),v_xb)) ),
inference(component_clause,[status(thm)],[f1877]) ).
fof(f1881,definition,
( sQ3_spl
<=> c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),v_xa,v_n,v_xb) ),
introduced(definition,[new_symbols(definition,[sQ3_spl])],[split_symbol_definition]) ).
fof(f1882,plain,
( ~ sQ3_spl
| c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),v_xa,v_n,v_xb) ),
inference(component_clause,[status(thm)],[f1881]) ).
fof(f1883,plain,
( sQ3_spl
| ~ c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),v_xa,v_n,v_xb) ),
inference(component_clause,[status(thm)],[f1881]) ).
fof(f1885,plain,
( sQ3_spl
| sQ1_spl ),
inference(split_clause,[status(thm)],[f1835,f1873,f1881]) ).
fof(f1889,plain,
~ sQ2_spl,
inference(split_clause,[status(thm)],[f1839,f1877]) ).
fof(f1890,definition,
! [X0,X1,X2] :
( sQ4_spl
<=> ( ~ hBOOL(hAPP(hAPP(v_P,X0),X2))
| ~ c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),X2,v_n,X1)
| hBOOL(hAPP(hAPP(v_Q,X0),X1)) ) ),
introduced(definition,[new_symbols(definition,[sQ4_spl])],[split_symbol_definition]) ).
fof(f1891,plain,
! [X0,X1,X2] :
( ~ sQ4_spl
| ~ hBOOL(hAPP(hAPP(v_P,X0),X2))
| ~ c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),X2,v_n,X1)
| hBOOL(hAPP(hAPP(v_Q,X0),X1)) ),
inference(component_clause,[status(thm)],[f1890]) ).
fof(f1893,definition,
! [X3,X4,X5] :
( sQ5_spl
<=> ( ~ hBOOL(hAPP(hAPP(v_P,X3),X5))
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X5,c_Suc(v_n),X4)
| hBOOL(hAPP(hAPP(v_Q,X3),X4)) ) ),
introduced(definition,[new_symbols(definition,[sQ5_spl])],[split_symbol_definition]) ).
fof(f1894,plain,
! [X0,X1,X2] :
( ~ sQ5_spl
| ~ hBOOL(hAPP(hAPP(v_P,X0),X2))
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X2,c_Suc(v_n),X1)
| hBOOL(hAPP(hAPP(v_Q,X0),X1)) ),
inference(component_clause,[status(thm)],[f1893]) ).
fof(f1896,plain,
( sQ5_spl
| sQ4_spl ),
inference(split_clause,[status(thm)],[f1841,f1890,f1893]) ).
fof(f1955,plain,
! [X0] : c_lessequals(X0,X0,tc_nat),
inference(resolution,[status(thm)],[f1809,f1772]) ).
fof(f1960,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(X0,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat)
| c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = c_Suc(X0)
| c_Suc(X0) = c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(resolution,[status(thm)],[f864,f1807]) ).
fof(f1961,plain,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(X0,X1,tc_nat)
| ~ c_HOL_Oord__class_Oless(X1,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat)
| c_Suc(X0) = c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(resolution,[status(thm)],[f864,f1776]) ).
fof(f1965,plain,
! [X0] :
( X0 = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))
| X0 = c_HOL_Ozero__class_Ozero(tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat) ),
inference(resolution,[status(thm)],[f864,f1784]) ).
fof(f1966,plain,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(X1,X0,tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) ),
inference(forward_subsumption_resolution,[status(thm)],[f1961,f1780]) ).
fof(f1968,plain,
! [X0] :
( c_Suc(X0) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))
| ~ c_HOL_Oord__class_Oless(X0,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) ),
inference(forward_subsumption_resolution,[status(thm)],[f1960,f1780]) ).
fof(f1969,plain,
! [X0,X1,X2] :
( ~ class_OrderedGroup_Ocomm__monoid__add(tc_nat)
| c_lessequals(X1,c_HOL_Oplus__class_Oplus(X0,X2,tc_nat),tc_nat)
| ~ c_lessequals(X1,X2,tc_nat)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat)
| c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ),
inference(resolution,[status(thm)],[f1751,f787]) ).
fof(f1970,plain,
! [X0,X1] :
( c_lessequals(X1,X0,tc_nat)
| c_lessequals(X0,c_Suc(X1),tc_nat) ),
inference(resolution,[status(thm)],[f1751,f1774]) ).
fof(f1971,plain,
! [X0] : c_lessequals(X0,c_Suc(X0),tc_nat),
inference(resolution,[status(thm)],[f1751,f1772]) ).
fof(f1974,definition,
! [X0,X1,X2] :
( sQ6_spl
<=> ( c_lessequals(X1,c_HOL_Oplus__class_Oplus(X0,X2,tc_nat),tc_nat)
| ~ c_lessequals(X1,X2,tc_nat)
| c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ) ),
introduced(definition,[new_symbols(definition,[sQ6_spl])],[split_symbol_definition]) ).
fof(f1977,definition,
( sQ7_spl
<=> class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ7_spl])],[split_symbol_definition]) ).
fof(f1979,plain,
( sQ7_spl
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat) ),
inference(component_clause,[status(thm)],[f1977]) ).
fof(f1980,definition,
( sQ8_spl
<=> class_OrderedGroup_Ocomm__monoid__add(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ8_spl])],[split_symbol_definition]) ).
fof(f1982,plain,
( sQ8_spl
| ~ class_OrderedGroup_Ocomm__monoid__add(tc_nat) ),
inference(component_clause,[status(thm)],[f1980]) ).
fof(f1983,plain,
( ~ sQ8_spl
| ~ sQ7_spl
| sQ6_spl ),
inference(split_clause,[status(thm)],[f1969,f1974,f1977,f1980]) ).
fof(f1984,plain,
( sQ8_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1982,f1859]) ).
fof(f1985,plain,
sQ8_spl,
inference(contradiction_clause,[status(thm)],[f1984]) ).
fof(f1999,plain,
! [X0] :
( c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = X0
| c_Suc(X0) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))
| ~ c_HOL_Oord__class_Oless(X0,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat) ),
inference(resolution,[status(thm)],[f1968,f1784]) ).
fof(f2001,plain,
c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat),
inference(forward_demodulation,[status(thm)],[f1806,f851]) ).
fof(f2002,plain,
( c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = c_HOL_Ozero__class_Ozero(tc_nat)
| c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ),
inference(resolution,[status(thm)],[f2001,f1689]) ).
fof(f2005,definition,
( sQ9_spl
<=> c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ),
introduced(definition,[new_symbols(definition,[sQ9_spl])],[split_symbol_definition]) ).
fof(f2008,definition,
( sQ10_spl
<=> c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = c_HOL_Ozero__class_Ozero(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ10_spl])],[split_symbol_definition]) ).
fof(f2009,plain,
( ~ sQ10_spl
| c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(component_clause,[status(thm)],[f2008]) ).
fof(f2012,plain,
( sQ10_spl
| sQ9_spl ),
inference(split_clause,[status(thm)],[f2002,f2005,f2008]) ).
fof(f2013,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat)
| c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = c_Suc(X0) ),
inference(resolution,[status(thm)],[f1762,f1968]) ).
fof(f2016,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Suc(X0)
| c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = c_Suc(c_Suc(X0)) ),
inference(resolution,[status(thm)],[f2013,f1807]) ).
fof(f2021,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Suc(X0) ),
inference(forward_subsumption_resolution,[status(thm)],[f2016,f1789]) ).
fof(f2022,plain,
! [X0] : ~ c_HOL_Oord__class_Oless(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(forward_subsumption_resolution,[status(thm)],[f2021,f1780]) ).
fof(f2029,plain,
! [X0,X1,X2] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X1,tc_nat)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat)
| ~ c_lessequals(X0,X2,tc_nat)
| c_HOL_Oord__class_Oless(X0,c_HOL_Oplus__class_Oplus(X1,X2,tc_nat),tc_nat) ),
inference(resolution,[status(thm)],[f850,f1859]) ).
fof(f2030,definition,
! [X0,X1,X2] :
( sQ11_spl
<=> ( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X1,tc_nat)
| ~ c_lessequals(X0,X2,tc_nat)
| c_HOL_Oord__class_Oless(X0,c_HOL_Oplus__class_Oplus(X1,X2,tc_nat),tc_nat) ) ),
introduced(definition,[new_symbols(definition,[sQ11_spl])],[split_symbol_definition]) ).
fof(f2033,plain,
( ~ sQ7_spl
| sQ11_spl ),
inference(split_clause,[status(thm)],[f2029,f2030,f1977]) ).
fof(f2034,plain,
( sQ7_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f1979,f1843]) ).
fof(f2035,plain,
sQ7_spl,
inference(contradiction_clause,[status(thm)],[f2034]) ).
fof(f2044,plain,
! [X0,X1] :
( ~ class_OrderedGroup_Ocomm__monoid__add(tc_nat)
| c_lessequals(X0,c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_nat),X1,tc_nat),tc_nat)
| ~ c_lessequals(X0,X1,tc_nat)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat) ),
inference(resolution,[status(thm)],[f1955,f787]) ).
fof(f2051,definition,
! [X0,X1] :
( sQ12_spl
<=> ( c_lessequals(X0,c_HOL_Oplus__class_Oplus(c_HOL_Ozero__class_Ozero(tc_nat),X1,tc_nat),tc_nat)
| ~ c_lessequals(X0,X1,tc_nat) ) ),
introduced(definition,[new_symbols(definition,[sQ12_spl])],[split_symbol_definition]) ).
fof(f2054,plain,
( ~ sQ8_spl
| sQ12_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f2044,f1977,f2051,f1980]) ).
fof(f2055,plain,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(X0,X1,tc_nat)
| c_lessequals(X0,X1,tc_nat) ),
inference(resolution,[status(thm)],[f781,f1774]) ).
fof(f2056,plain,
! [X0] : ~ c_HOL_Oord__class_Oless(X0,X0,tc_nat),
inference(resolution,[status(thm)],[f781,f1772]) ).
fof(f2079,plain,
! [X0,X1,X2,X3] :
( ~ sQ4_spl
| hBOOL(hAPP(hAPP(v_Q,X3),X2))
| ~ c_lessequals(X1,v_n,tc_nat)
| ~ hBOOL(hAPP(hAPP(v_P,X3),X0))
| ~ c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),X0,X1,X2) ),
inference(resolution,[status(thm)],[f1766,f1891]) ).
fof(f2081,plain,
! [X0,X1,X2,X3,X4] :
( c_HOL_Ominus__class_Ominus(X2,c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(X0,c_Suc(X1),tc_nat),X3,tc_nat),X4,tc_nat),tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Suc(X1),X3,tc_nat),X2,tc_nat),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(X0,X3,tc_nat),X4,tc_nat),tc_nat)
| c_lessequals(X0,X1,tc_nat) ),
inference(resolution,[status(thm)],[f870,f1809]) ).
fof(f2095,plain,
! [X0,X1] :
( sQ2_spl
| ~ sQ4_spl
| ~ c_lessequals(X1,v_n,tc_nat)
| ~ c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),X0,X1,v_xb)
| ~ hBOOL(hAPP(hAPP(v_P,v_x),X0)) ),
inference(resolution,[status(thm)],[f2079,f1879]) ).
fof(f2112,plain,
! [X0] :
( ~ sQ0_spl
| sQ2_spl
| ~ sQ4_spl
| ~ c_lessequals(X0,v_n,tc_nat)
| ~ c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),v_xa,X0,v_xb) ),
inference(resolution,[status(thm)],[f2095,f1870]) ).
fof(f2113,plain,
! [X0,X1] :
( ~ class_OrderedGroup_Ocomm__monoid__add(tc_nat)
| c_lessequals(X0,c_HOL_Oplus__class_Oplus(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X1,tc_nat),tc_nat)
| ~ c_lessequals(X0,X1,tc_nat)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat) ),
inference(resolution,[status(thm)],[f1971,f787]) ).
fof(f2114,plain,
! [X0] : c_lessequals(X0,c_Suc(c_Suc(X0)),tc_nat),
inference(resolution,[status(thm)],[f1971,f1774]) ).
fof(f2124,definition,
! [X0,X1] :
( sQ13_spl
<=> ( c_lessequals(X0,c_HOL_Oplus__class_Oplus(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X1,tc_nat),tc_nat)
| ~ c_lessequals(X0,X1,tc_nat) ) ),
introduced(definition,[new_symbols(definition,[sQ13_spl])],[split_symbol_definition]) ).
fof(f2127,plain,
( ~ sQ8_spl
| sQ13_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f2113,f1977,f2124,f1980]) ).
fof(f2133,plain,
! [X0,X1] :
( c_lessequals(X0,X1,tc_nat)
| c_HOL_Ominus__class_Ominus(c_Suc(X0),c_Suc(X1),tc_nat) = c_Suc(c_HOL_Ominus__class_Ominus(X0,c_Suc(X1),tc_nat)) ),
inference(resolution,[status(thm)],[f729,f1809]) ).
fof(f2136,plain,
! [X0,X1] :
( c_lessequals(X0,X1,tc_nat)
| c_Suc(c_HOL_Ominus__class_Ominus(X0,X1,tc_nat)) = c_HOL_Ominus__class_Ominus(c_Suc(X0),X1,tc_nat) ),
inference(resolution,[status(thm)],[f729,f1751]) ).
fof(f2137,plain,
! [X0,X1] :
( c_lessequals(X0,X1,tc_nat)
| c_HOL_Ominus__class_Ominus(X0,X1,tc_nat) = c_Suc(c_HOL_Ominus__class_Ominus(X0,c_Suc(X1),tc_nat)) ),
inference(forward_demodulation,[status(thm)],[f1786,f2133]) ).
fof(f2172,plain,
( c_HOL_Ozero__class_Ozero(tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ),
inference(resolution,[status(thm)],[f1008,f2001]) ).
fof(f2178,definition,
( sQ14_spl
<=> c_HOL_Ozero__class_Ozero(tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ14_spl])],[split_symbol_definition]) ).
fof(f2182,plain,
( sQ14_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f2172,f2008,f2178]) ).
fof(f2184,plain,
( ~ sQ10_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2009,f1780]) ).
fof(f2185,plain,
~ sQ10_spl,
inference(contradiction_clause,[status(thm)],[f2184]) ).
fof(f2244,plain,
! [X0,X1,X2] :
( c_lessequals(X0,c_HOL_Oplus__class_Oplus(X1,X2,tc_nat),tc_nat)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_nat),X2,tc_nat)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat)
| ~ c_lessequals(X0,X1,tc_nat) ),
inference(resolution,[status(thm)],[f785,f1859]) ).
fof(f2245,definition,
! [X0,X1,X2] :
( sQ15_spl
<=> ( c_lessequals(X0,c_HOL_Oplus__class_Oplus(X1,X2,tc_nat),tc_nat)
| ~ c_lessequals(c_HOL_Ozero__class_Ozero(tc_nat),X2,tc_nat)
| ~ c_lessequals(X0,X1,tc_nat) ) ),
introduced(definition,[new_symbols(definition,[sQ15_spl])],[split_symbol_definition]) ).
fof(f2248,plain,
( ~ sQ7_spl
| sQ15_spl ),
inference(split_clause,[status(thm)],[f2244,f2245,f1977]) ).
fof(f2255,plain,
! [X0,X1] :
( X1 = X1
| c_HOL_Ozero__class_Ozero(tc_nat) = X0 ),
inference(equality_resolution,[status(thm)],[f947]) ).
fof(f2256,definition,
! [X0] :
( sQ16_spl
<=> c_HOL_Ozero__class_Ozero(tc_nat) = X0 ),
introduced(definition,[new_symbols(definition,[sQ16_spl])],[split_symbol_definition]) ).
fof(f2257,plain,
! [X0] :
( ~ sQ16_spl
| X0 = c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(component_clause,[status(thm)],[f2256]) ).
fof(f2259,definition,
! [X1] :
( sQ17_spl
<=> X1 = X1 ),
introduced(definition,[new_symbols(definition,[sQ17_spl])],[split_symbol_definition]) ).
fof(f2262,plain,
( sQ17_spl
| sQ16_spl ),
inference(split_clause,[status(thm)],[f2255,f2256,f2259]) ).
fof(f2283,plain,
! [X0] :
( X0 = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))
| c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) != c_HOL_Otimes__class_Otimes(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X0,tc_nat) ),
inference(paramodulation,[status(thm)],[f1068,f947]) ).
fof(f2290,definition,
! [X0] :
( sQ18_spl
<=> ( X0 = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))
| c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) != c_HOL_Otimes__class_Otimes(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X0,tc_nat) ) ),
introduced(definition,[new_symbols(definition,[sQ18_spl])],[split_symbol_definition]) ).
fof(f2293,plain,
( sQ10_spl
| sQ18_spl ),
inference(split_clause,[status(thm)],[f2283,f2290,f2008]) ).
fof(f2348,plain,
! [X0,X1] :
( ~ class_OrderedGroup_Ocomm__monoid__add(tc_nat)
| c_lessequals(X0,c_HOL_Oplus__class_Oplus(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),X1,tc_nat),tc_nat)
| ~ c_lessequals(X0,X1,tc_nat)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat) ),
inference(resolution,[status(thm)],[f2114,f787]) ).
fof(f2365,definition,
! [X0,X1] :
( sQ21_spl
<=> ( c_lessequals(X0,c_HOL_Oplus__class_Oplus(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),X1,tc_nat),tc_nat)
| ~ c_lessequals(X0,X1,tc_nat) ) ),
introduced(definition,[new_symbols(definition,[sQ21_spl])],[split_symbol_definition]) ).
fof(f2368,plain,
( ~ sQ8_spl
| sQ21_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f2348,f1977,f2365,f1980]) ).
fof(f2443,plain,
! [X0] : c_lessequals(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat),
inference(resolution,[status(thm)],[f1196,f884]) ).
fof(f2447,plain,
! [X0,X1,X2] :
( ~ class_OrderedGroup_Ocomm__monoid__add(tc_nat)
| c_lessequals(X0,c_HOL_Oplus__class_Oplus(X2,X1,tc_nat),tc_nat)
| ~ c_lessequals(X0,X1,tc_nat)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat) ),
inference(resolution,[status(thm)],[f2443,f787]) ).
fof(f2458,definition,
! [X0,X1,X2] :
( sQ22_spl
<=> ( c_lessequals(X0,c_HOL_Oplus__class_Oplus(X2,X1,tc_nat),tc_nat)
| ~ c_lessequals(X0,X1,tc_nat) ) ),
introduced(definition,[new_symbols(definition,[sQ22_spl])],[split_symbol_definition]) ).
fof(f2461,plain,
( ~ sQ8_spl
| sQ22_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f2447,f1977,f2458,f1980]) ).
fof(f2659,plain,
! [X0,X1,X2] :
( ~ class_OrderedGroup_Ocomm__monoid__add(tc_nat)
| c_lessequals(X1,c_HOL_Oplus__class_Oplus(X0,X2,tc_nat),tc_nat)
| ~ c_lessequals(X1,X2,tc_nat)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat)
| c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) != c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(resolution,[status(thm)],[f842,f787]) ).
fof(f2680,definition,
! [X0,X1,X2] :
( sQ24_spl
<=> ( c_lessequals(X1,c_HOL_Oplus__class_Oplus(X0,X2,tc_nat),tc_nat)
| ~ c_lessequals(X1,X2,tc_nat)
| c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) != c_HOL_Ozero__class_Ozero(tc_nat) ) ),
introduced(definition,[new_symbols(definition,[sQ24_spl])],[split_symbol_definition]) ).
fof(f2683,plain,
( ~ sQ8_spl
| ~ sQ7_spl
| sQ24_spl ),
inference(split_clause,[status(thm)],[f2659,f2680,f1977,f1980]) ).
fof(f2725,plain,
( ~ sQ16_spl
| $false ),
inference(backward_subsumption_resolution,[status(thm)],[f1780,f2257]) ).
fof(f2744,plain,
~ sQ16_spl,
inference(contradiction_clause,[status(thm)],[f2725]) ).
fof(f2799,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(tc_nat) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))
| c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) != c_HOL_Otimes__class_Otimes(X0,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat)
| X0 = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ),
inference(paramodulation,[status(thm)],[f1068,f949]) ).
fof(f2807,definition,
! [X0] :
( sQ30_spl
<=> ( c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) != c_HOL_Otimes__class_Otimes(X0,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat)
| X0 = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ) ),
introduced(definition,[new_symbols(definition,[sQ30_spl])],[split_symbol_definition]) ).
fof(f2810,plain,
( sQ10_spl
| sQ30_spl ),
inference(split_clause,[status(thm)],[f2799,f2807,f2008]) ).
fof(f2938,plain,
! [X0] :
( ~ class_Orderings_Olinorder(tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Orderings_Oord__class_Omin(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) ),
inference(paramodulation,[status(thm)],[f966,f868]) ).
fof(f2939,plain,
! [X0] :
( ~ class_Orderings_Olinorder(tc_nat)
| c_Orderings_Oord__class_Omin(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = c_Orderings_Oord__class_Omin(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) ),
inference(paramodulation,[status(thm)],[f966,f868]) ).
fof(f2940,definition,
! [X0] :
( sQ36_spl
<=> c_HOL_Ozero__class_Ozero(tc_nat) = c_Orderings_Oord__class_Omin(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ36_spl])],[split_symbol_definition]) ).
fof(f2943,definition,
( sQ37_spl
<=> class_Orderings_Olinorder(tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ37_spl])],[split_symbol_definition]) ).
fof(f2945,plain,
( sQ37_spl
| ~ class_Orderings_Olinorder(tc_nat) ),
inference(component_clause,[status(thm)],[f2943]) ).
fof(f2946,plain,
( ~ sQ37_spl
| sQ36_spl ),
inference(split_clause,[status(thm)],[f2938,f2940,f2943]) ).
fof(f2947,definition,
! [X0] :
( sQ38_spl
<=> c_Orderings_Oord__class_Omin(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = c_Orderings_Oord__class_Omin(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ38_spl])],[split_symbol_definition]) ).
fof(f2950,plain,
( ~ sQ37_spl
| sQ38_spl ),
inference(split_clause,[status(thm)],[f2939,f2947,f2943]) ).
fof(f2951,plain,
( sQ37_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f2945,f1867]) ).
fof(f2952,plain,
sQ37_spl,
inference(contradiction_clause,[status(thm)],[f2951]) ).
fof(f2978,definition,
( sQ39_spl
<=> c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(v_pn,c_Suc(v_n),v_xa,v_xb) = v_n ),
introduced(definition,[new_symbols(definition,[sQ39_spl])],[split_symbol_definition]) ).
fof(f2979,plain,
( ~ sQ39_spl
| c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(v_pn,c_Suc(v_n),v_xa,v_xb) = v_n ),
inference(component_clause,[status(thm)],[f2978]) ).
fof(f3019,plain,
( ~ sQ0_spl
| sQ2_spl
| ~ sQ4_spl
| ~ sQ3_spl
| ~ c_lessequals(v_n,v_n,tc_nat) ),
inference(resolution,[status(thm)],[f1882,f2112]) ).
fof(f3022,plain,
( ~ sQ0_spl
| sQ2_spl
| ~ sQ4_spl
| ~ sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3019,f1955]) ).
fof(f3023,plain,
( ~ sQ0_spl
| sQ2_spl
| ~ sQ4_spl
| ~ sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f3022]) ).
fof(f3025,plain,
( ~ sQ1_spl
| c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),v_xa,c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(v_pn,c_Suc(v_n),v_xa,v_xb),v_xb) ),
inference(resolution,[status(thm)],[f1874,f1790]) ).
fof(f3027,plain,
! [X0] :
( sQ2_spl
| ~ sQ5_spl
| ~ hBOOL(hAPP(hAPP(v_P,v_x),X0))
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),X0,c_Suc(v_n),v_xb) ),
inference(resolution,[status(thm)],[f1894,f1879]) ).
fof(f3108,plain,
( ~ sQ3_spl
| c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),v_xa,c_Suc(v_n),v_xb) ),
inference(resolution,[status(thm)],[f1810,f1882]) ).
fof(f3109,plain,
! [X0] :
( ~ sQ5_spl
| ~ sQ3_spl
| hBOOL(hAPP(hAPP(v_Q,X0),v_xb))
| ~ hBOOL(hAPP(hAPP(v_P,X0),v_xa)) ),
inference(resolution,[status(thm)],[f3108,f1894]) ).
fof(f3202,plain,
( sQ2_spl
| ~ sQ5_spl
| ~ sQ3_spl
| ~ hBOOL(hAPP(hAPP(v_P,v_x),v_xa)) ),
inference(resolution,[status(thm)],[f3109,f1879]) ).
fof(f3203,plain,
( sQ2_spl
| ~ sQ5_spl
| ~ sQ3_spl
| ~ sQ0_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3202,f1870]) ).
fof(f3204,plain,
( sQ2_spl
| ~ sQ5_spl
| ~ sQ3_spl
| ~ sQ0_spl ),
inference(contradiction_clause,[status(thm)],[f3203]) ).
fof(f3241,plain,
( ~ sQ0_spl
| sQ2_spl
| ~ sQ5_spl
| ~ c_Natural_Oevaln(c_Com_Ocom_OBODY(v_pn),v_xa,c_Suc(v_n),v_xb) ),
inference(resolution,[status(thm)],[f3027,f1870]) ).
fof(f3242,plain,
( ~ sQ0_spl
| sQ2_spl
| ~ sQ5_spl
| ~ sQ1_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3241,f1874]) ).
fof(f3243,plain,
( ~ sQ0_spl
| sQ2_spl
| ~ sQ5_spl
| ~ sQ1_spl ),
inference(contradiction_clause,[status(thm)],[f3242]) ).
fof(f3620,plain,
( ~ sQ1_spl
| ~ sQ39_spl
| c_Natural_Oevaln(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom),v_xa,v_n,v_xb) ),
inference(forward_demodulation,[status(thm)],[f2979,f3025]) ).
fof(f3621,plain,
( ~ sQ1_spl
| ~ sQ39_spl
| sQ3_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f3620,f1883]) ).
fof(f3622,plain,
( ~ sQ1_spl
| ~ sQ39_spl
| sQ3_spl ),
inference(contradiction_clause,[status(thm)],[f3621]) ).
fof(f4306,plain,
! [X0,X1] :
( ~ class_Orderings_Olinorder(tc_nat)
| c_Orderings_Oord__class_Omin(c_Suc(X0),c_Suc(c_Orderings_Oord__class_Omin(X0,X1,tc_nat)),tc_nat) = c_Orderings_Oord__class_Omin(c_Suc(X0),c_Suc(X1),tc_nat) ),
inference(paramodulation,[status(thm)],[f1815,f868]) ).
fof(f4307,definition,
! [X0,X1] :
( sQ47_spl
<=> c_Orderings_Oord__class_Omin(c_Suc(X0),c_Suc(c_Orderings_Oord__class_Omin(X0,X1,tc_nat)),tc_nat) = c_Orderings_Oord__class_Omin(c_Suc(X0),c_Suc(X1),tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ47_spl])],[split_symbol_definition]) ).
fof(f4310,plain,
( ~ sQ37_spl
| sQ47_spl ),
inference(split_clause,[status(thm)],[f4306,f4307,f2943]) ).
fof(f4815,plain,
! [X0,X1,X2] :
( ~ class_OrderedGroup_Ocomm__monoid__add(tc_nat)
| c_lessequals(X1,c_HOL_Oplus__class_Oplus(c_Suc(X0),X2,tc_nat),tc_nat)
| ~ c_lessequals(X1,X2,tc_nat)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat)
| c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ),
inference(resolution,[status(thm)],[f1970,f787]) ).
fof(f4844,definition,
! [X0,X1,X2] :
( sQ49_spl
<=> ( c_lessequals(X1,c_HOL_Oplus__class_Oplus(c_Suc(X0),X2,tc_nat),tc_nat)
| ~ c_lessequals(X1,X2,tc_nat)
| c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ) ),
introduced(definition,[new_symbols(definition,[sQ49_spl])],[split_symbol_definition]) ).
fof(f4847,plain,
( ~ sQ8_spl
| ~ sQ7_spl
| sQ49_spl ),
inference(split_clause,[status(thm)],[f4815,f4844,f1977,f1980]) ).
fof(f4928,definition,
( sQ50_spl
<=> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ50_spl])],[split_symbol_definition]) ).
fof(f4930,plain,
( sQ50_spl
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) ),
inference(component_clause,[status(thm)],[f4928]) ).
fof(f5157,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ),
inference(resolution,[status(thm)],[f1670,f2022]) ).
fof(f5158,plain,
! [X0] :
( c_HOL_Ominus__class_Ominus(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),X0,tc_nat) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))
| c_HOL_Ominus__class_Ominus(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),X0,tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat) ),
inference(resolution,[status(thm)],[f1670,f1965]) ).
fof(f5159,plain,
! [X0] :
( c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = c_HOL_Ominus__class_Ominus(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),X0,tc_nat)
| c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = c_Suc(c_HOL_Ominus__class_Ominus(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),X0,tc_nat))
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat) ),
inference(resolution,[status(thm)],[f1670,f1999]) ).
fof(f5160,plain,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(X1,c_HOL_Ominus__class_Ominus(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X0,tc_nat),tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) ),
inference(resolution,[status(thm)],[f1670,f1966]) ).
fof(f5161,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(tc_nat) = c_HOL_Ominus__class_Ominus(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X0,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) ),
inference(resolution,[status(thm)],[f1670,f864]) ).
fof(f5162,plain,
! [X0] :
( c_Suc(c_HOL_Ominus__class_Ominus(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X0,tc_nat)) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) ),
inference(resolution,[status(thm)],[f1670,f1968]) ).
fof(f5172,definition,
! [X0,X1] :
( sQ54_spl
<=> ( ~ c_HOL_Oord__class_Oless(X1,c_HOL_Ominus__class_Ominus(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X0,tc_nat),tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) ) ),
introduced(definition,[new_symbols(definition,[sQ54_spl])],[split_symbol_definition]) ).
fof(f5175,plain,
( sQ54_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f5160,f4928,f5172]) ).
fof(f5176,definition,
! [X0] :
( sQ55_spl
<=> ( c_HOL_Ozero__class_Ozero(tc_nat) = c_HOL_Ominus__class_Ominus(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X0,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) ) ),
introduced(definition,[new_symbols(definition,[sQ55_spl])],[split_symbol_definition]) ).
fof(f5179,plain,
( sQ55_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f5161,f4928,f5176]) ).
fof(f5180,definition,
( sQ56_spl
<=> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ56_spl])],[split_symbol_definition]) ).
fof(f5183,definition,
! [X0] :
( sQ57_spl
<=> ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ57_spl])],[split_symbol_definition]) ).
fof(f5187,definition,
( sQ58_spl
<=> c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ58_spl])],[split_symbol_definition]) ).
fof(f5189,plain,
( sQ58_spl
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat) ),
inference(component_clause,[status(thm)],[f5187]) ).
fof(f5190,definition,
! [X0] :
( sQ59_spl
<=> ( c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = c_HOL_Ominus__class_Ominus(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),X0,tc_nat)
| c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = c_Suc(c_HOL_Ominus__class_Ominus(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),X0,tc_nat))
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) ) ),
introduced(definition,[new_symbols(definition,[sQ59_spl])],[split_symbol_definition]) ).
fof(f5193,plain,
( sQ59_spl
| ~ sQ58_spl ),
inference(split_clause,[status(thm)],[f5159,f5187,f5190]) ).
fof(f5200,plain,
( sQ57_spl
| ~ sQ56_spl ),
inference(split_clause,[status(thm)],[f5157,f5180,f5183]) ).
fof(f5201,definition,
! [X0] :
( sQ61_spl
<=> ( c_Suc(c_HOL_Ominus__class_Ominus(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X0,tc_nat)) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) ) ),
introduced(definition,[new_symbols(definition,[sQ61_spl])],[split_symbol_definition]) ).
fof(f5204,plain,
( sQ61_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f5162,f4928,f5201]) ).
fof(f5205,definition,
! [X0] :
( sQ62_spl
<=> ( c_HOL_Ominus__class_Ominus(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),X0,tc_nat) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))
| c_HOL_Ominus__class_Ominus(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),X0,tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) ) ),
introduced(definition,[new_symbols(definition,[sQ62_spl])],[split_symbol_definition]) ).
fof(f5208,plain,
( sQ62_spl
| ~ sQ58_spl ),
inference(split_clause,[status(thm)],[f5158,f5187,f5205]) ).
fof(f5209,plain,
( sQ50_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f4930,f1196]) ).
fof(f5210,plain,
sQ50_spl,
inference(contradiction_clause,[status(thm)],[f5209]) ).
fof(f5211,plain,
( sQ58_spl
| $false ),
inference(forward_subsumption_resolution,[status(thm)],[f5189,f1196]) ).
fof(f5212,plain,
sQ58_spl,
inference(contradiction_clause,[status(thm)],[f5211]) ).
fof(f5854,plain,
! [X0] :
( X0 != c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))
| c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = X0
| c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = c_HOL_Ozero__class_Ozero(tc_nat) ),
inference(paramodulation,[status(thm)],[f1554,f1689]) ).
fof(f5856,definition,
! [X0] :
( sQ73_spl
<=> ( X0 != c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))
| c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = X0 ) ),
introduced(definition,[new_symbols(definition,[sQ73_spl])],[split_symbol_definition]) ).
fof(f5859,plain,
( sQ73_spl
| sQ10_spl ),
inference(split_clause,[status(thm)],[f5854,f2008,f5856]) ).
fof(f5989,plain,
! [X0,X1,X2] :
( ~ class_OrderedGroup_Ocomm__monoid__add(tc_nat)
| c_lessequals(X1,c_HOL_Oplus__class_Oplus(X0,X2,tc_nat),tc_nat)
| ~ c_lessequals(X1,X2,tc_nat)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) ),
inference(resolution,[status(thm)],[f2055,f787]) ).
fof(f6023,definition,
! [X0,X1,X2] :
( sQ76_spl
<=> ( c_lessequals(X1,c_HOL_Oplus__class_Oplus(X0,X2,tc_nat),tc_nat)
| ~ c_lessequals(X1,X2,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) ) ),
introduced(definition,[new_symbols(definition,[sQ76_spl])],[split_symbol_definition]) ).
fof(f6026,plain,
( ~ sQ8_spl
| ~ sQ7_spl
| sQ76_spl ),
inference(split_clause,[status(thm)],[f5989,f6023,f1977,f1980]) ).
fof(f6292,plain,
! [X0,X1] :
( ~ class_OrderedGroup_Ocomm__monoid__add(tc_nat)
| c_lessequals(X0,c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),tc_nat),X1,tc_nat),tc_nat)
| ~ c_lessequals(X0,X1,tc_nat)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat) ),
inference(resolution,[status(thm)],[f1532,f787]) ).
fof(f6341,definition,
! [X0,X1] :
( sQ77_spl
<=> ( c_lessequals(X0,c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),tc_nat),X1,tc_nat),tc_nat)
| ~ c_lessequals(X0,X1,tc_nat) ) ),
introduced(definition,[new_symbols(definition,[sQ77_spl])],[split_symbol_definition]) ).
fof(f6344,plain,
( ~ sQ8_spl
| sQ77_spl
| ~ sQ7_spl ),
inference(split_clause,[status(thm)],[f6292,f1977,f6341,f1980]) ).
fof(f6758,plain,
! [X0,X1,X2,X3,X4,X5] :
( ~ class_OrderedGroup_Ocomm__monoid__add(tc_nat)
| c_lessequals(X4,c_HOL_Oplus__class_Oplus(X1,X5,tc_nat),tc_nat)
| ~ c_lessequals(X4,X5,tc_nat)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat)
| c_HOL_Ominus__class_Ominus(X0,c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(X1),tc_nat),X2,tc_nat),X3,tc_nat),tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Suc(X1),X2,tc_nat),X0,tc_nat),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_nat),X2,tc_nat),X3,tc_nat),tc_nat) ),
inference(resolution,[status(thm)],[f2081,f787]) ).
fof(f6793,definition,
! [X0,X1,X2,X3,X4,X5] :
( sQ78_spl
<=> ( c_lessequals(X4,c_HOL_Oplus__class_Oplus(X1,X5,tc_nat),tc_nat)
| ~ c_lessequals(X4,X5,tc_nat)
| c_HOL_Ominus__class_Ominus(X0,c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(X1),tc_nat),X2,tc_nat),X3,tc_nat),tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_Suc(X1),X2,tc_nat),X0,tc_nat),c_HOL_Oplus__class_Oplus(c_HOL_Otimes__class_Otimes(c_HOL_Ozero__class_Ozero(tc_nat),X2,tc_nat),X3,tc_nat),tc_nat) ) ),
introduced(definition,[new_symbols(definition,[sQ78_spl])],[split_symbol_definition]) ).
fof(f6796,plain,
( ~ sQ8_spl
| ~ sQ7_spl
| sQ78_spl ),
inference(split_clause,[status(thm)],[f6758,f6793,f1977,f1980]) ).
fof(f7517,plain,
! [X0] :
( c_Divides_Odiv__class_Omod(X0,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))
| c_Divides_Odiv__class_Omod(X0,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat) ),
inference(resolution,[status(thm)],[f1122,f1965]) ).
fof(f7518,plain,
! [X0] :
( c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = c_Divides_Odiv__class_Omod(X0,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat)
| c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = c_Suc(c_Divides_Odiv__class_Omod(X0,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat))
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat) ),
inference(resolution,[status(thm)],[f1122,f1999]) ).
fof(f7521,plain,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(X0,c_Divides_Odiv__class_Omod(X1,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat),tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) ),
inference(resolution,[status(thm)],[f1122,f1966]) ).
fof(f7522,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) ),
inference(resolution,[status(thm)],[f1122,f864]) ).
fof(f7523,plain,
! [X0] :
( c_Suc(c_Divides_Odiv__class_Omod(X0,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat)) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) ),
inference(resolution,[status(thm)],[f1122,f1968]) ).
fof(f7532,definition,
! [X0] :
( sQ82_spl
<=> ( c_Divides_Odiv__class_Omod(X0,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))
| c_Divides_Odiv__class_Omod(X0,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat) ) ),
introduced(definition,[new_symbols(definition,[sQ82_spl])],[split_symbol_definition]) ).
fof(f7535,plain,
( sQ82_spl
| ~ sQ58_spl ),
inference(split_clause,[status(thm)],[f7517,f5187,f7532]) ).
fof(f7538,definition,
! [X0] :
( sQ83_spl
<=> ( c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = c_Divides_Odiv__class_Omod(X0,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat)
| c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = c_Suc(c_Divides_Odiv__class_Omod(X0,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat)) ) ),
introduced(definition,[new_symbols(definition,[sQ83_spl])],[split_symbol_definition]) ).
fof(f7541,plain,
( sQ83_spl
| ~ sQ58_spl ),
inference(split_clause,[status(thm)],[f7518,f5187,f7538]) ).
fof(f7542,definition,
! [X0,X1] :
( sQ84_spl
<=> ~ c_HOL_Oord__class_Oless(X0,c_Divides_Odiv__class_Omod(X1,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat),tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ84_spl])],[split_symbol_definition]) ).
fof(f7543,plain,
! [X0,X1] :
( ~ sQ84_spl
| ~ c_HOL_Oord__class_Oless(X0,c_Divides_Odiv__class_Omod(X1,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat),tc_nat) ),
inference(component_clause,[status(thm)],[f7542]) ).
fof(f7545,plain,
( sQ84_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f7521,f4928,f7542]) ).
fof(f7546,definition,
! [X0] :
( sQ85_spl
<=> c_Suc(c_Divides_Odiv__class_Omod(X0,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat)) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) ),
introduced(definition,[new_symbols(definition,[sQ85_spl])],[split_symbol_definition]) ).
fof(f7549,plain,
( sQ85_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f7523,f4928,f7546]) ).
fof(f7550,definition,
! [X0] :
( sQ86_spl
<=> c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ86_spl])],[split_symbol_definition]) ).
fof(f7553,plain,
( sQ86_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f7522,f4928,f7550]) ).
fof(f7611,plain,
! [X0,X1] :
( ~ sQ84_spl
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X1,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Divides_Odiv__class_Omod(X0,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat),tc_nat) ),
inference(resolution,[status(thm)],[f7543,f1670]) ).
fof(f7623,definition,
! [X0] :
( sQ87_spl
<=> ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Divides_Odiv__class_Omod(X0,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat),tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ87_spl])],[split_symbol_definition]) ).
fof(f7626,plain,
( ~ sQ84_spl
| sQ57_spl
| sQ87_spl ),
inference(split_clause,[status(thm)],[f7611,f7623,f5183,f7542]) ).
fof(f7675,plain,
! [X0,X1,X2] :
( ~ class_OrderedGroup_Ocomm__monoid__add(tc_nat)
| c_lessequals(X1,c_HOL_Oplus__class_Oplus(X0,X2,tc_nat),tc_nat)
| ~ c_lessequals(X1,X2,tc_nat)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat)
| c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) = c_Suc(c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(X0),tc_nat)) ),
inference(resolution,[status(thm)],[f2137,f787]) ).
fof(f7733,definition,
! [X0,X1,X2] :
( sQ90_spl
<=> ( c_lessequals(X1,c_HOL_Oplus__class_Oplus(X0,X2,tc_nat),tc_nat)
| ~ c_lessequals(X1,X2,tc_nat)
| c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) = c_Suc(c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(X0),tc_nat)) ) ),
introduced(definition,[new_symbols(definition,[sQ90_spl])],[split_symbol_definition]) ).
fof(f7736,plain,
( ~ sQ8_spl
| ~ sQ7_spl
| sQ90_spl ),
inference(split_clause,[status(thm)],[f7675,f7733,f1977,f1980]) ).
fof(f7747,plain,
! [X0,X1,X2] :
( ~ class_OrderedGroup_Ocomm__monoid__add(tc_nat)
| c_lessequals(X1,c_HOL_Oplus__class_Oplus(X0,X2,tc_nat),tc_nat)
| ~ c_lessequals(X1,X2,tc_nat)
| ~ class_OrderedGroup_Opordered__ab__semigroup__add__imp__le(tc_nat)
| c_Suc(c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)) = c_HOL_Ominus__class_Ominus(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X0,tc_nat) ),
inference(resolution,[status(thm)],[f2136,f787]) ).
fof(f7793,definition,
! [X0,X1,X2] :
( sQ91_spl
<=> ( c_lessequals(X1,c_HOL_Oplus__class_Oplus(X0,X2,tc_nat),tc_nat)
| ~ c_lessequals(X1,X2,tc_nat)
| c_Suc(c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat)) = c_HOL_Ominus__class_Ominus(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X0,tc_nat) ) ),
introduced(definition,[new_symbols(definition,[sQ91_spl])],[split_symbol_definition]) ).
fof(f7796,plain,
( ~ sQ8_spl
| ~ sQ7_spl
| sQ91_spl ),
inference(split_clause,[status(thm)],[f7747,f7793,f1977,f1980]) ).
fof(f7988,plain,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(X1,X1,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) ),
inference(resolution,[status(thm)],[f1501,f2056]) ).
fof(f7990,plain,
! [X0] :
( c_HOL_Oord__class_Oless(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Otimes__class_Otimes(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X0,tc_nat),tc_nat)
| ~ c_HOL_Oord__class_Oless(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X0,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) ),
inference(paramodulation,[status(thm)],[f1068,f1501]) ).
fof(f7994,plain,
! [X0] :
( c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X0,tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) ),
inference(paramodulation,[status(thm)],[f1068,f1501]) ).
fof(f7997,definition,
! [X0] :
( sQ95_spl
<=> ( c_HOL_Oord__class_Oless(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Otimes__class_Otimes(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X0,tc_nat),tc_nat)
| ~ c_HOL_Oord__class_Oless(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X0,tc_nat) ) ),
introduced(definition,[new_symbols(definition,[sQ95_spl])],[split_symbol_definition]) ).
fof(f8000,plain,
( sQ95_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f7990,f4928,f7997]) ).
fof(f8001,definition,
! [X1] :
( sQ96_spl
<=> ~ c_HOL_Oord__class_Oless(X1,X1,tc_nat) ),
introduced(definition,[new_symbols(definition,[sQ96_spl])],[split_symbol_definition]) ).
fof(f8004,plain,
( sQ96_spl
| sQ57_spl ),
inference(split_clause,[status(thm)],[f7988,f5183,f8001]) ).
fof(f8008,definition,
! [X0] :
( sQ97_spl
<=> ( c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X0,tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat)
| ~ c_HOL_Oord__class_Oless(X0,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) ) ),
introduced(definition,[new_symbols(definition,[sQ97_spl])],[split_symbol_definition]) ).
fof(f8011,plain,
( sQ97_spl
| ~ sQ50_spl ),
inference(split_clause,[status(thm)],[f7994,f4928,f8008]) ).
fof(f8162,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat)
| ~ c_HOL_Oord__class_Oless(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Otimes__class_Otimes(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X0,tc_nat),tc_nat)
| c_HOL_Oord__class_Oless(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X0,tc_nat) ),
inference(paramodulation,[status(thm)],[f1068,f1499]) ).
fof(f8166,plain,
! [X0] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat)
| ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X0,tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat)
| c_HOL_Oord__class_Oless(X0,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) ),
inference(paramodulation,[status(thm)],[f1068,f1499]) ).
fof(f8179,definition,
! [X0] :
( sQ101_spl
<=> ( ~ c_HOL_Oord__class_Oless(c_HOL_Otimes__class_Otimes(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X0,tc_nat),c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat)
| c_HOL_Oord__class_Oless(X0,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) ) ),
introduced(definition,[new_symbols(definition,[sQ101_spl])],[split_symbol_definition]) ).
fof(f8182,plain,
( ~ sQ50_spl
| sQ101_spl ),
inference(split_clause,[status(thm)],[f8166,f8179,f4928]) ).
fof(f8187,definition,
! [X0] :
( sQ103_spl
<=> ( ~ c_HOL_Oord__class_Oless(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Otimes__class_Otimes(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X0,tc_nat),tc_nat)
| c_HOL_Oord__class_Oless(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X0,tc_nat) ) ),
introduced(definition,[new_symbols(definition,[sQ103_spl])],[split_symbol_definition]) ).
fof(f8190,plain,
( ~ sQ50_spl
| sQ103_spl ),
inference(split_clause,[status(thm)],[f8162,f8187,f4928]) ).
fof(f8520,plain,
( ~ sQ1_spl
| c_Suc(v_n) = c_Suc(c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(v_pn,c_Suc(v_n),v_xa,v_xb)) ),
inference(resolution,[status(thm)],[f1816,f1874]) ).
fof(f8545,plain,
( ~ sQ1_spl
| c_Natural_Osko__Natural__Xevaln__elim__cases__6__1(v_pn,c_Suc(v_n),v_xa,v_xb) = v_n ),
inference(resolution,[status(thm)],[f8520,f1789]) ).
fof(f8617,plain,
( ~ sQ1_spl
| sQ39_spl ),
inference(split_clause,[status(thm)],[f8545,f2978,f1873]) ).
fof(f8662,plain,
$false,
inference(sat_refutation,[status(thm)],[f1872,f1885,f1889,f1896,f1983,f1985,f2012,f2033,f2035,f2054,f2127,f2182,f2185,f2248,f2262,f2293,f2368,f2461,f2683,f2744,f2810,f2946,f2950,f2952,f3023,f3204,f3243,f3622,f4310,f4847,f5175,f5179,f5193,f5200,f5204,f5208,f5210,f5212,f5859,f6026,f6344,f6796,f7535,f7541,f7545,f7549,f7553,f7626,f7736,f7796,f8000,f8004,f8011,f8182,f8190,f8617]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV822-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.03 % Command : drodi -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n016.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 09:31:38 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.09/0.41 % Drodi V4.1.1
% 70.31/9.38 % Refutation found
% 70.31/9.38 % SZS status Unsatisfiable for theBenchmark: Theory is unsatisfiable
% 70.31/9.38 % SZS output start CNFRefutation for theBenchmark
% See solution above
% 15.89/10.61 % Elapsed time: 10.023485 seconds
% 15.89/10.61 % CPU time: 67.022084 seconds
% 15.89/10.61 % Total memory used: 458.165 MB
% 15.89/10.61 % Net memory used: 417.965 MB
%------------------------------------------------------------------------------