%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : LAT278-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 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 : Fri Sep 25 01:58:32 PM UTC 2026
% Result : Unsatisfiable 6.31s 16.76s
% Output : CNFRefutation 6.31s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 138
% Syntax : Number of formulae : 863 ( 474 unt; 0 def)
% Number of atoms : 1303 ( 610 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 825 ( 385 ~; 440 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 42 ( 42 usr; 16 con; 0-5 aty)
% Number of variables : 1720 ( 0 sgn1720 !; 0 ?;1250 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( X0 = X5
| c_Tarski_Opotype_Opotype__ext(X0,X1,X2,X3,X4) != c_Tarski_Opotype_Opotype__ext(X5,X6,X7,X3,X4) ),
file('/export/starexec/sandbox/benchmark/Axioms/LAT006-0.ax',cls_Tarski_Opotype_Oext__inject_0) ).
fof(f2,axiom,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( X1 = X6
| c_Tarski_Opotype_Opotype__ext(X0,X1,X2,X3,X4) != c_Tarski_Opotype_Opotype__ext(X5,X6,X7,X3,X4) ),
file('/export/starexec/sandbox/benchmark/Axioms/LAT006-0.ax',cls_Tarski_Opotype_Oext__inject_1) ).
fof(f3,axiom,
! [X2,X3,X0,X1,X6,X7,X4,X5] :
( X2 = X7
| c_Tarski_Opotype_Opotype__ext(X0,X1,X2,X3,X4) != c_Tarski_Opotype_Opotype__ext(X5,X6,X7,X3,X4) ),
file('/export/starexec/sandbox/benchmark/Axioms/LAT006-0.ax',cls_Tarski_Opotype_Oext__inject_2) ).
fof(f4,axiom,
! [X2,X3,X0,X1,X4] : c_Tarski_Opotype_Opset(c_Tarski_Opotype_Opotype__ext(X0,X1,X2,X3,X4),X3,X4) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/LAT006-0.ax',cls_Tarski_Opotype_Oselect__convs__1_0) ).
fof(f5,axiom,
! [X2,X3,X0,X1,X4] : c_Tarski_Opotype_Oorder(c_Tarski_Opotype_Opotype__ext(X0,X1,X2,X3,X4),X3,X4) = X1,
file('/export/starexec/sandbox/benchmark/Axioms/LAT006-0.ax',cls_Tarski_Opotype_Oselect__convs__2_0) ).
fof(f39,axiom,
! [X2,X3,X0,X1] : c_Nat_Osize(c_Pair(X0,X1,X2,X3),tc_prod(X2,X3)) = c_0,
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Datatype_Oprod_Osize_0) ).
fof(f40,plain,
! [X2,X3,X0,X1] : c_0 = c_Nat_Osize(c_Pair(X0,X1,X2,X3),tc_prod(X2,X3)),
inference(reorient_equations,[],[f39]) ).
fof(f41,axiom,
! [X2,X0,X1] : c_Nat_Osize(c_Sum__Type_OInl(X0,X1,X2),tc_sum(X1,X2)) = c_0,
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Datatype_Osum_Osize__1_0) ).
fof(f42,plain,
! [X2,X0,X1] : c_0 = c_Nat_Osize(c_Sum__Type_OInl(X0,X1,X2),tc_sum(X1,X2)),
inference(reorient_equations,[],[f41]) ).
fof(f43,axiom,
! [X2,X0,X1] : c_Nat_Osize(c_Sum__Type_OInr(X0,X1,X2),tc_sum(X2,X1)) = c_0,
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Datatype_Osum_Osize__2_0) ).
fof(f44,plain,
! [X2,X0,X1] : c_0 = c_Nat_Osize(c_Sum__Type_OInr(X0,X1,X2),tc_sum(X2,X1)),
inference(reorient_equations,[],[f43]) ).
fof(f201,axiom,
! [X2,X3,X0,X1] :
( c_in(c_minus(X0,X2,tc_set(X3)),c_Finite__Set_OFinites,tc_set(X3))
| ~ c_in(c_minus(X0,c_insert(X1,X2,X3),tc_set(X3)),c_Finite__Set_OFinites,tc_set(X3)) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Finite__Set_Ofinite__Diff__insert_0) ).
fof(f202,axiom,
! [X2,X3,X0,X1] :
( c_in(c_minus(X0,c_insert(X3,X1,X2),tc_set(X2)),c_Finite__Set_OFinites,tc_set(X2))
| ~ c_in(c_minus(X0,X1,tc_set(X2)),c_Finite__Set_OFinites,tc_set(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Finite__Set_Ofinite__Diff__insert_1) ).
fof(f210,axiom,
! [X2,X0,X1] :
( c_in(X1,c_Finite__Set_OFinites,tc_set(X2))
| ~ c_in(c_insert(X0,X1,X2),c_Finite__Set_OFinites,tc_set(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Finite__Set_Ofinite__insert_0) ).
fof(f286,axiom,
! [X0,X1] : c_plus(X0,c_uminus(X1,tc_IntDef_Oint),tc_IntDef_Oint) = c_minus(X0,X1,tc_IntDef_Oint),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_IntArith_Oz1_A_L_A_N_Aw1_A_61_61_Az1_A_N_Aw1_0) ).
fof(f292,axiom,
! [X0,X1] :
( c_less(X0,X1,tc_IntDef_Oint)
| ~ c_lessequals(X0,c_minus(X1,c_1,tc_IntDef_Oint),tc_IntDef_Oint) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_IntArith_Ozle__diff1__eq_0) ).
fof(f293,axiom,
! [X0,X1] :
( c_lessequals(X0,c_minus(X1,c_1,tc_IntDef_Oint),tc_IntDef_Oint)
| ~ c_less(X0,X1,tc_IntDef_Oint) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_IntArith_Ozle__diff1__eq_1) ).
fof(f311,axiom,
c_0 != c_1,
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_IntDef_Oint__0__neq__1_0) ).
fof(f422,axiom,
! [X0] : c_Nat_Opower(X0,c_0,tc_IntDef_Oint) = c_1,
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_IntDiv_Opower_Osimps__1_0) ).
fof(f423,plain,
! [X0] : c_1 = c_Nat_Opower(X0,c_0,tc_IntDef_Oint),
inference(reorient_equations,[],[f422]) ).
fof(f424,axiom,
! [X0,X1] : c_Nat_Opower(X0,c_Suc(X1),tc_IntDef_Oint) = c_times(X0,c_Nat_Opower(X0,X1,tc_IntDef_Oint),tc_IntDef_Oint),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_IntDiv_Opower_Osimps__2_0) ).
fof(f481,axiom,
! [X2,X3,X0,X1,X4,X5] :
( X0 = X3
| c_in(c_Pair(X0,X3,X2,X2),X5,tc_prod(X2,X2))
| ~ c_in(c_Pair(c_List_Olist_OCons(X0,X1,X2),c_List_Olist_OCons(X3,X4,X2),tc_List_Olist(X2),tc_List_Olist(X2)),c_List_Olex(X5,X2),tc_prod(tc_List_Olist(X2),tc_List_Olist(X2))) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_List_OCons__in__lex_0) ).
fof(f482,axiom,
! [X2,X3,X0,X1,X4,X5] :
( c_in(c_Pair(X1,X4,tc_List_Olist(X2),tc_List_Olist(X2)),c_List_Olex(X5,X2),tc_prod(tc_List_Olist(X2),tc_List_Olist(X2)))
| c_in(c_Pair(X0,X3,X2,X2),X5,tc_prod(X2,X2))
| ~ c_in(c_Pair(c_List_Olist_OCons(X0,X1,X2),c_List_Olist_OCons(X3,X4,X2),tc_List_Olist(X2),tc_List_Olist(X2)),c_List_Olex(X5,X2),tc_prod(tc_List_Olist(X2),tc_List_Olist(X2))) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_List_OCons__in__lex_1) ).
fof(f483,axiom,
! [X2,X3,X0,X1,X4,X5] :
( c_Nat_Osize(X1,tc_List_Olist(X2)) = c_Nat_Osize(X4,tc_List_Olist(X2))
| X0 = X3
| ~ c_in(c_Pair(c_List_Olist_OCons(X0,X1,X2),c_List_Olist_OCons(X3,X4,X2),tc_List_Olist(X2),tc_List_Olist(X2)),c_List_Olex(X5,X2),tc_prod(tc_List_Olist(X2),tc_List_Olist(X2))) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_List_OCons__in__lex_2) ).
fof(f484,axiom,
! [X2,X3,X0,X1,X4,X5] :
( c_Nat_Osize(X1,tc_List_Olist(X2)) = c_Nat_Osize(X4,tc_List_Olist(X2))
| c_in(c_Pair(X1,X4,tc_List_Olist(X2),tc_List_Olist(X2)),c_List_Olex(X5,X2),tc_prod(tc_List_Olist(X2),tc_List_Olist(X2)))
| ~ c_in(c_Pair(c_List_Olist_OCons(X0,X1,X2),c_List_Olist_OCons(X3,X4,X2),tc_List_Olist(X2),tc_List_Olist(X2)),c_List_Olex(X5,X2),tc_prod(tc_List_Olist(X2),tc_List_Olist(X2))) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_List_OCons__in__lex_3) ).
fof(f485,axiom,
! [X2,X3,X0,X1,X4,X5] :
( c_in(c_Pair(c_List_Olist_OCons(X0,X4,X2),c_List_Olist_OCons(X1,X5,X2),tc_List_Olist(X2),tc_List_Olist(X2)),c_List_Olex(X3,X2),tc_prod(tc_List_Olist(X2),tc_List_Olist(X2)))
| c_Nat_Osize(X4,tc_List_Olist(X2)) != c_Nat_Osize(X5,tc_List_Olist(X2))
| ~ c_in(c_Pair(X0,X1,X2,X2),X3,tc_prod(X2,X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_List_OCons__in__lex_4) ).
fof(f486,axiom,
! [X2,X3,X0,X1,X4] :
( c_in(c_Pair(c_List_Olist_OCons(X4,X0,X2),c_List_Olist_OCons(X4,X1,X2),tc_List_Olist(X2),tc_List_Olist(X2)),c_List_Olex(X3,X2),tc_prod(tc_List_Olist(X2),tc_List_Olist(X2)))
| ~ c_in(c_Pair(X0,X1,tc_List_Olist(X2),tc_List_Olist(X2)),c_List_Olex(X3,X2),tc_prod(tc_List_Olist(X2),tc_List_Olist(X2))) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_List_OCons__in__lex_5) ).
fof(f487,axiom,
! [X2,X0,X1] : ~ c_in(c_Pair(X0,c_List_Olist_ONil,tc_List_Olist(X1),tc_List_Olist(X1)),c_List_Olex(X2,X1),tc_prod(tc_List_Olist(X1),tc_List_Olist(X1))),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_List_ONil2__notin__lex_0) ).
fof(f501,axiom,
! [X2,X0,X1] : ~ c_in(c_Pair(c_List_Olist_ONil,X0,tc_List_Olist(X1),tc_List_Olist(X1)),c_List_Olex(X2,X1),tc_prod(tc_List_Olist(X1),tc_List_Olist(X1))),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_List_ONil__notin__lex_0) ).
fof(f507,axiom,
! [X2,X3,X0,X1,X4] :
( X0 = X2
| c_append(X0,X3,X1) != c_append(X2,X4,X1)
| c_Nat_Osize(X0,tc_List_Olist(X1)) != c_Nat_Osize(X2,tc_List_Olist(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_List_Oappend__eq__append__conv_0) ).
fof(f508,axiom,
! [X2,X3,X0,X1,X4] :
( X3 = X4
| c_append(X0,X3,X1) != c_append(X2,X4,X1)
| c_Nat_Osize(X0,tc_List_Olist(X1)) != c_Nat_Osize(X2,tc_List_Olist(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_List_Oappend__eq__append__conv_1) ).
fof(f509,axiom,
! [X2,X3,X0,X1,X4] :
( X3 = X4
| c_append(X3,X0,X1) != c_append(X4,X2,X1)
| c_Nat_Osize(X0,tc_List_Olist(X1)) != c_Nat_Osize(X2,tc_List_Olist(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_List_Oappend__eq__append__conv_2) ).
fof(f510,axiom,
! [X2,X3,X0,X1,X4] :
( X0 = X2
| c_append(X3,X0,X1) != c_append(X4,X2,X1)
| c_Nat_Osize(X0,tc_List_Olist(X1)) != c_Nat_Osize(X2,tc_List_Olist(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_List_Oappend__eq__append__conv_3) ).
fof(f613,axiom,
! [X0,X1] :
( X0 = c_List_Olist_ONil
| c_Nat_Osize(X0,tc_List_Olist(X1)) != c_0 ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_List_Olength__0__conv_0) ).
fof(f614,plain,
! [X0,X1] :
( c_List_Olist_ONil = X0
| c_0 != c_Nat_Osize(X0,tc_List_Olist(X1)) ),
inference(reorient_equations,[],[f613]) ).
fof(f615,axiom,
! [X0] : c_Nat_Osize(c_List_Olist_ONil,tc_List_Olist(X0)) = c_0,
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_List_Olength__0__conv_1) ).
fof(f616,plain,
! [X0] : c_0 = c_Nat_Osize(c_List_Olist_ONil,tc_List_Olist(X0)),
inference(reorient_equations,[],[f615]) ).
fof(f617,axiom,
! [X2,X0,X1] : c_Nat_Osize(c_append(X0,X1,X2),tc_List_Olist(X2)) = c_plus(c_Nat_Osize(X0,tc_List_Olist(X2)),c_Nat_Osize(X1,tc_List_Olist(X2)),tc_nat),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_List_Olength__append_0) ).
fof(f621,axiom,
! [X0,X1] :
( X0 = c_List_Olist_ONil
| c_less(c_0,c_Nat_Osize(X0,tc_List_Olist(X1)),tc_nat) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_List_Olength__greater__0__conv_1) ).
fof(f622,plain,
! [X0,X1] :
( c_List_Olist_ONil = X0
| c_less(c_0,c_Nat_Osize(X0,tc_List_Olist(X1)),tc_nat) ),
inference(reorient_equations,[],[f621]) ).
fof(f656,axiom,
! [X2,X0,X1] : c_Nat_Osize(c_List_Olist_OCons(X0,X1,X2),tc_List_Olist(X2)) = c_plus(c_Nat_Osize(X1,tc_List_Olist(X2)),c_Suc(c_0),tc_nat),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_List_Olist_Osize__2_0) ).
fof(f900,axiom,
! [X2,X0,X1] :
( c_plus(c_minus(X1,X0,tc_nat),X2,tc_nat) = c_minus(c_plus(X1,X2,tc_nat),X0,tc_nat)
| ~ c_lessequals(X0,X1,tc_nat) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_NatArith_Oadd__diff__assoc2_0) ).
fof(f901,axiom,
! [X2,X0,X1] :
( c_plus(X2,c_minus(X1,X0,tc_nat),tc_nat) = c_minus(c_plus(X2,X1,tc_nat),X0,tc_nat)
| ~ c_lessequals(X0,X1,tc_nat) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_NatArith_Oadd__diff__assoc_0) ).
fof(f902,axiom,
! [X2,X0,X1] :
( c_minus(X2,c_Suc(c_minus(X1,X0,tc_nat)),tc_nat) = c_minus(c_plus(X2,X0,tc_nat),c_Suc(X1),tc_nat)
| ~ c_lessequals(X0,X1,tc_nat) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_NatArith_Odiff__Suc__diff__eq1_0) ).
fof(f903,axiom,
! [X2,X0,X1] :
( c_minus(c_Suc(c_minus(X1,X0,tc_nat)),X2,tc_nat) = c_minus(c_Suc(X1),c_plus(X0,X2,tc_nat),tc_nat)
| ~ c_lessequals(X0,X1,tc_nat) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_NatArith_Odiff__Suc__diff__eq2_0) ).
fof(f904,axiom,
! [X0,X1] :
( c_minus(X1,c_minus(X1,X0,tc_nat),tc_nat) = X0
| ~ c_lessequals(X0,X1,tc_nat) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_NatArith_Odiff__diff__cancel_0) ).
fof(f905,axiom,
! [X2,X0,X1] :
( c_minus(X2,c_minus(X1,X0,tc_nat),tc_nat) = c_minus(c_plus(X2,X0,tc_nat),X1,tc_nat)
| ~ c_lessequals(X0,X1,tc_nat) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_NatArith_Odiff__diff__right_0) ).
fof(f906,axiom,
! [X0,X1] :
( c_less(c_minus(X0,X1,tc_nat),X0,tc_nat)
| ~ c_less(c_0,X1,tc_nat)
| ~ c_less(c_0,X0,tc_nat) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_NatArith_Odiff__less_0) ).
fof(f1168,axiom,
! [X2,X0,X1] : c_minus(c_minus(c_Suc(X0),X1,tc_nat),c_Suc(X2),tc_nat) = c_minus(c_minus(X0,X1,tc_nat),X2,tc_nat),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Nat_OSuc__diff__diff_0) ).
fof(f1175,axiom,
! [X0] :
( c_Suc(c_minus(X0,c_Suc(c_0),tc_nat)) = X0
| ~ c_less(c_0,X0,tc_nat) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Nat_OSuc__pred_0) ).
fof(f1188,axiom,
! [X0] : c_minus(c_0,X0,tc_nat) = c_0,
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Nat_Odiff__0__eq__0_0) ).
fof(f1189,plain,
! [X0] : c_0 = c_minus(c_0,X0,tc_nat),
inference(reorient_equations,[],[f1188]) ).
fof(f1190,axiom,
! [X0,X1] : c_minus(c_Suc(X0),c_Suc(X1),tc_nat) = c_minus(X0,X1,tc_nat),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Nat_Odiff__Suc__Suc_0) ).
fof(f1191,plain,
! [X0,X1] : c_minus(X0,X1,tc_nat) = c_minus(c_Suc(X0),c_Suc(X1),tc_nat),
inference(reorient_equations,[],[f1190]) ).
fof(f1192,axiom,
! [X0,X1] :
( c_less(c_minus(X0,c_Suc(X1),tc_nat),X0,tc_nat)
| ~ c_less(c_0,X0,tc_nat) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Nat_Odiff__Suc__less_0) ).
fof(f1193,axiom,
! [X2,X0,X1] : c_minus(c_minus(X0,X1,tc_nat),X2,tc_nat) = c_minus(X0,c_plus(X1,X2,tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Nat_Odiff__diff__left_0) ).
fof(f1194,axiom,
! [X0,X1] :
( c_lessequals(X0,X1,tc_nat)
| c_minus(X0,X1,tc_nat) != c_0 ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Nat_Odiff__is__0__eq_0) ).
fof(f1195,plain,
! [X0,X1] :
( c_lessequals(X0,X1,tc_nat)
| c_0 != c_minus(X0,X1,tc_nat) ),
inference(reorient_equations,[],[f1194]) ).
fof(f1196,axiom,
! [X0,X1] :
( c_minus(X0,X1,tc_nat) = c_0
| ~ c_lessequals(X0,X1,tc_nat) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Nat_Odiff__is__0__eq_H_0) ).
fof(f1197,plain,
! [X0,X1] :
( c_0 = c_minus(X0,X1,tc_nat)
| ~ c_lessequals(X0,X1,tc_nat) ),
inference(reorient_equations,[],[f1196]) ).
fof(f1198,axiom,
! [X0,X1] : c_lessequals(c_minus(X0,X1,tc_nat),X0,tc_nat),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Nat_Odiff__le__self_0) ).
fof(f1199,axiom,
! [X0] : c_minus(X0,X0,tc_nat) = c_0,
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Nat_Odiff__self__eq__0_0) ).
fof(f1200,plain,
! [X0] : c_0 = c_minus(X0,X0,tc_nat),
inference(reorient_equations,[],[f1199]) ).
fof(f1201,axiom,
! [X0] :
( X0 = c_0
| ~ c_lessequals(X0,c_0,tc_nat) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Nat_Ole__0__eq_0) ).
fof(f1202,plain,
! [X0] :
( c_0 = X0
| ~ c_lessequals(X0,c_0,tc_nat) ),
inference(reorient_equations,[],[f1201]) ).
fof(f1204,axiom,
! [X0,X1] :
( c_plus(c_minus(X1,X0,tc_nat),X0,tc_nat) = X1
| ~ c_lessequals(X0,X1,tc_nat) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Nat_Ole__add__diff__inverse2_0) ).
fof(f1205,axiom,
! [X0,X1] :
( c_plus(X0,c_minus(X1,X0,tc_nat),tc_nat) = X1
| ~ c_lessequals(X0,X1,tc_nat) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Nat_Ole__add__diff__inverse_0) ).
fof(f1209,axiom,
! [X0] :
( X0 = c_0
| ~ c_less(X0,c_1,tc_nat) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Nat_Oless__one_0) ).
fof(f1210,plain,
! [X0] :
( c_0 = X0
| ~ c_less(X0,c_1,tc_nat) ),
inference(reorient_equations,[],[f1209]) ).
fof(f1211,axiom,
c_less(c_0,c_1,tc_nat),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Nat_Oless__one_1) ).
fof(f1260,axiom,
! [X0] :
( X0 = c_0
| c_less(c_0,X0,tc_nat) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Nat_Onot__gr0_0) ).
fof(f1261,plain,
! [X0] :
( c_0 = X0
| c_less(c_0,X0,tc_nat) ),
inference(reorient_equations,[],[f1260]) ).
fof(f1263,axiom,
! [X0] : ~ c_less(X0,c_0,tc_nat),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Nat_Onot__less0_0) ).
fof(f1278,axiom,
! [X0] : c_minus(X0,c_0,tc_nat) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Nat_Oop_A_N_Odiff__0_0) ).
fof(f1279,axiom,
! [X0,X1] :
( c_less(X1,X0,tc_nat)
| ~ c_less(c_0,c_minus(X0,X1,tc_nat),tc_nat) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Nat_Ozero__less__diff_0) ).
fof(f1280,axiom,
! [X0,X1] :
( c_less(c_0,c_minus(X1,X0,tc_nat),tc_nat)
| ~ c_less(X0,X1,tc_nat) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Nat_Ozero__less__diff_1) ).
fof(f1587,axiom,
! [X0,X1] :
( c_Numeral_Onumber__of(X1,tc_nat) = c_0
| c_less(c_0,X0,tc_nat)
| ~ c_less(c_0,c_Nat_Opower(X0,c_Numeral_Onumber__of(X1,tc_nat),tc_nat),tc_nat) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Parity_Ozero__less__power__nat__eq__number__of_0) ).
fof(f1588,plain,
! [X0,X1] :
( c_0 = c_Numeral_Onumber__of(X1,tc_nat)
| c_less(c_0,X0,tc_nat)
| ~ c_less(c_0,c_Nat_Opower(X0,c_Numeral_Onumber__of(X1,tc_nat),tc_nat),tc_nat) ),
inference(reorient_equations,[],[f1587]) ).
fof(f1589,axiom,
! [X0,X1] :
( c_less(c_0,c_Nat_Opower(X1,c_Numeral_Onumber__of(X0,tc_nat),tc_nat),tc_nat)
| c_Numeral_Onumber__of(X0,tc_nat) != c_0 ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Parity_Ozero__less__power__nat__eq__number__of_1) ).
fof(f1590,plain,
! [X0,X1] :
( c_less(c_0,c_Nat_Opower(X1,c_Numeral_Onumber__of(X0,tc_nat),tc_nat),tc_nat)
| c_0 != c_Numeral_Onumber__of(X0,tc_nat) ),
inference(reorient_equations,[],[f1589]) ).
fof(f1591,axiom,
! [X0,X1] :
( c_less(c_0,c_Nat_Opower(X0,c_Numeral_Onumber__of(X1,tc_nat),tc_nat),tc_nat)
| ~ c_less(c_0,X0,tc_nat) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Parity_Ozero__less__power__nat__eq__number__of_2) ).
fof(f1592,axiom,
! [X0,X1] :
( c_lessequals(c_Suc(c_0),c_Nat_Opower(X0,X1,tc_nat),tc_nat)
| ~ c_lessequals(c_1,X0,tc_nat) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Power_Onat__one__le__power_0) ).
fof(f1593,axiom,
! [X0] :
( X0 = c_0
| ~ c_less(c_0,c_Nat_Opower(c_0,X0,tc_nat),tc_nat) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Power_Onat__zero__less__power__iff_0) ).
fof(f1594,plain,
! [X0] :
( c_0 = X0
| ~ c_less(c_0,c_Nat_Opower(c_0,X0,tc_nat),tc_nat) ),
inference(reorient_equations,[],[f1593]) ).
fof(f1595,axiom,
! [X0,X1] :
( X0 = c_0
| c_less(c_0,c_Nat_Opower(X0,X1,tc_nat),tc_nat) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Power_Onat__zero__less__power__iff_1) ).
fof(f1596,plain,
! [X0,X1] :
( c_0 = X0
| c_less(c_0,c_Nat_Opower(X0,X1,tc_nat),tc_nat) ),
inference(reorient_equations,[],[f1595]) ).
fof(f1598,axiom,
! [X0] : c_Nat_Opower(X0,c_0,tc_nat) = c_1,
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Power_Opower_Osimps__1_0) ).
fof(f1599,plain,
! [X0] : c_1 = c_Nat_Opower(X0,c_0,tc_nat),
inference(reorient_equations,[],[f1598]) ).
fof(f1600,axiom,
! [X0,X1] : c_Nat_Opower(X0,c_Suc(X1),tc_nat) = c_times(X0,c_Nat_Opower(X0,X1,tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Power_Opower_Osimps__2_0) ).
fof(f1625,axiom,
! [X2,X3,X0,X1,X4,X5] :
( X0 = X4
| c_Pair(X0,X1,X2,X3) != c_Pair(X4,X5,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Product__Type_OPair__eq_0) ).
fof(f1626,axiom,
! [X2,X3,X0,X1,X4,X5] :
( X1 = X5
| c_Pair(X0,X1,X2,X3) != c_Pair(X4,X5,X2,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Product__Type_OPair__eq_1) ).
fof(f1661,axiom,
! [X0,X1] : c_Nat_Opower(X0,c_1,tc_set(tc_prod(X1,X1))) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Relation__Power_Orel__pow__1_0) ).
fof(f1937,axiom,
! [X0,X1] : c_minus(X0,X0,tc_set(X1)) = c_emptyset,
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_ODiff__cancel_0) ).
fof(f1938,plain,
! [X0,X1] : c_emptyset = c_minus(X0,X0,tc_set(X1)),
inference(reorient_equations,[],[f1937]) ).
fof(f1941,axiom,
! [X0,X1] : c_minus(X0,c_emptyset,tc_set(X1)) = X0,
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_ODiff__empty_0) ).
fof(f1942,axiom,
! [X2,X0,X1] :
( c_lessequals(X0,X1,tc_set(X2))
| c_minus(X0,X1,tc_set(X2)) != c_emptyset ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_ODiff__eq__empty__iff_0) ).
fof(f1943,plain,
! [X2,X0,X1] :
( c_lessequals(X0,X1,tc_set(X2))
| c_emptyset != c_minus(X0,X1,tc_set(X2)) ),
inference(reorient_equations,[],[f1942]) ).
fof(f1944,axiom,
! [X2,X0,X1] :
( c_minus(X0,X1,tc_set(X2)) = c_emptyset
| ~ c_lessequals(X0,X1,tc_set(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_ODiff__eq__empty__iff_1) ).
fof(f1945,plain,
! [X2,X0,X1] :
( c_emptyset = c_minus(X0,X1,tc_set(X2))
| ~ c_lessequals(X0,X1,tc_set(X2)) ),
inference(reorient_equations,[],[f1944]) ).
fof(f1946,axiom,
! [X2,X0,X1] : c_minus(c_minus(X0,X1,tc_set(X2)),X1,tc_set(X2)) = c_minus(X0,X1,tc_set(X2)),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_ODiff__idemp_0) ).
fof(f1947,plain,
! [X2,X0,X1] : c_minus(X0,X1,tc_set(X2)) = c_minus(c_minus(X0,X1,tc_set(X2)),X1,tc_set(X2)),
inference(reorient_equations,[],[f1946]) ).
fof(f1948,axiom,
! [X2,X3,X0,X1] :
( c_in(X0,X1,X3)
| ~ c_in(X0,c_minus(X1,X2,tc_set(X3)),X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_ODiff__iff_0) ).
fof(f1949,axiom,
! [X2,X3,X0,X1] :
( ~ c_in(X0,c_minus(X3,X1,tc_set(X2)),X2)
| ~ c_in(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_ODiff__iff_1) ).
fof(f1950,axiom,
! [X2,X3,X0,X1] :
( c_in(X0,c_minus(X1,X3,tc_set(X2)),X2)
| c_in(X0,X3,X2)
| ~ c_in(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_ODiff__iff_2) ).
fof(f1951,axiom,
! [X2,X3,X0,X1] :
( c_minus(X1,c_insert(X0,X3,X2),tc_set(X2)) = c_minus(X1,X3,tc_set(X2))
| c_in(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_ODiff__insert0_0) ).
fof(f1952,plain,
! [X2,X3,X0,X1] :
( c_minus(X1,X3,tc_set(X2)) = c_minus(X1,c_insert(X0,X3,X2),tc_set(X2))
| c_in(X0,X1,X2) ),
inference(reorient_equations,[],[f1951]) ).
fof(f2053,axiom,
! [X0,X1] : c_minus(c_emptyset,X0,tc_set(X1)) = c_emptyset,
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_Oempty__Diff_0) ).
fof(f2054,plain,
! [X0,X1] : c_emptyset = c_minus(c_emptyset,X0,tc_set(X1)),
inference(reorient_equations,[],[f2053]) ).
fof(f2060,axiom,
! [X0,X1] : ~ c_in(X0,c_emptyset,X1),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_Oempty__iff_0) ).
fof(f2061,axiom,
! [X2,X0,X1] : c_emptyset != c_insert(X0,X1,X2),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_Oempty__not__insert_0) ).
fof(f2062,axiom,
! [X2,X3,X0,X1] :
( c_minus(c_insert(X0,X3,X2),X1,tc_set(X2)) = c_minus(X3,X1,tc_set(X2))
| ~ c_in(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_Oinsert__Diff1_0) ).
fof(f2063,plain,
! [X2,X3,X0,X1] :
( c_minus(X3,X1,tc_set(X2)) = c_minus(c_insert(X0,X3,X2),X1,tc_set(X2))
| ~ c_in(X0,X1,X2) ),
inference(reorient_equations,[],[f2062]) ).
fof(f2064,axiom,
! [X2,X0,X1] : c_insert(X0,c_minus(X1,c_insert(X0,c_emptyset,X2),tc_set(X2)),X2) = c_insert(X0,X1,X2),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_Oinsert__Diff__single_0) ).
fof(f2065,plain,
! [X2,X0,X1] : c_insert(X0,X1,X2) = c_insert(X0,c_minus(X1,c_insert(X0,c_emptyset,X2),tc_set(X2)),X2),
inference(reorient_equations,[],[f2064]) ).
fof(f2066,axiom,
! [X2,X0,X1] : c_insert(X0,c_insert(X0,X1,X2),X2) = c_insert(X0,X1,X2),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_Oinsert__absorb2_0) ).
fof(f2067,plain,
! [X2,X0,X1] : c_insert(X0,X1,X2) = c_insert(X0,c_insert(X0,X1,X2),X2),
inference(reorient_equations,[],[f2066]) ).
fof(f2077,axiom,
! [X2,X3,X0,X1] :
( X0 = X1
| c_in(X0,X2,X3)
| ~ c_in(X0,c_insert(X1,X2,X3),X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_Oinsert__iff_0) ).
fof(f2078,axiom,
! [X2,X0,X1] : c_in(X0,c_insert(X0,X1,X2),X2),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_Oinsert__iff_1) ).
fof(f2079,axiom,
! [X2,X3,X0,X1] :
( c_in(X0,c_insert(X3,X1,X2),X2)
| ~ c_in(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_Oinsert__iff_2) ).
fof(f2083,axiom,
! [X2,X3,X0,X1] :
( c_in(X0,X3,X2)
| ~ c_lessequals(c_insert(X0,X1,X2),X3,tc_set(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_Oinsert__subset_0) ).
fof(f2084,axiom,
! [X2,X3,X0,X1] :
( c_lessequals(X1,X3,tc_set(X2))
| ~ c_lessequals(c_insert(X0,X1,X2),X3,tc_set(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_Oinsert__subset_1) ).
fof(f2085,axiom,
! [X2,X3,X0,X1] :
( c_lessequals(c_insert(X0,X3,X2),X1,tc_set(X2))
| ~ c_lessequals(X3,X1,tc_set(X2))
| ~ c_in(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_Oinsert__subset_2) ).
fof(f2086,axiom,
! [X0,X1] : ~ c_less(X0,c_emptyset,tc_set(X1)),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_Onot__psubset__empty_0) ).
fof(f2087,axiom,
! [X2,X3,X0,X1] :
( X2 = X0
| c_insert(X0,c_emptyset,X1) != c_insert(X2,X3,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_Osingleton__insert__inj__eq_0) ).
fof(f2088,plain,
! [X2,X3,X0,X1] :
( X0 = X2
| c_insert(X0,c_emptyset,X1) != c_insert(X2,X3,X1) ),
inference(reorient_equations,[],[f2087]) ).
fof(f2089,axiom,
! [X2,X3,X0,X1] :
( c_lessequals(X3,c_insert(X0,c_emptyset,X1),tc_set(X1))
| c_insert(X0,c_emptyset,X1) != c_insert(X2,X3,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_Osingleton__insert__inj__eq_1) ).
fof(f2090,axiom,
! [X2,X0,X1] :
( c_insert(X1,c_emptyset,X2) = c_insert(X1,X0,X2)
| ~ c_lessequals(X0,c_insert(X1,c_emptyset,X2),tc_set(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_Osingleton__insert__inj__eq_2) ).
fof(f2096,axiom,
! [X0,X1] :
( X0 = c_emptyset
| ~ c_lessequals(X0,c_emptyset,tc_set(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Set_Osubset__empty_0) ).
fof(f2097,plain,
! [X0,X1] :
( c_emptyset = X0
| ~ c_lessequals(X0,c_emptyset,tc_set(X1)) ),
inference(reorient_equations,[],[f2096]) ).
fof(f2099,axiom,
! [X2,X3,X0,X1] :
( X0 = X3
| c_Sum__Type_OInl(X0,X1,X2) != c_Sum__Type_OInl(X3,X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Sum__Type_OInl__eq_0) ).
fof(f2100,axiom,
! [X2,X3,X0,X1] : c_Sum__Type_OInl(X0,X1,X2) != c_Sum__Type_OInr(X3,X2,X1),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Sum__Type_OInl__not__Inr_0) ).
fof(f2101,axiom,
! [X2,X3,X0,X1] :
( X0 = X3
| c_Sum__Type_OInr(X0,X1,X2) != c_Sum__Type_OInr(X3,X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Sum__Type_OInr__eq_0) ).
fof(f2103,axiom,
! [X0,X1] : c_Sum__Type_OPlus(c_UNIV,c_UNIV,X0,X1) = c_UNIV,
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Sum__Type_OUNIV__Plus__UNIV_0) ).
fof(f2104,plain,
! [X0,X1] : c_UNIV = c_Sum__Type_OPlus(c_UNIV,c_UNIV,X0,X1),
inference(reorient_equations,[],[f2103]) ).
fof(f2111,axiom,
! [X0] : c_Transitive__Closure_Ortrancl(c_emptyset,X0) = c_Relation_OId,
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Transitive__Closure_Ortrancl__empty_0) ).
fof(f2112,plain,
! [X0] : c_Relation_OId = c_Transitive__Closure_Ortrancl(c_emptyset,X0),
inference(reorient_equations,[],[f2111]) ).
fof(f2113,axiom,
! [X0,X1] : c_Transitive__Closure_Ortrancl(c_Transitive__Closure_Ortrancl(X0,X1),X1) = c_Transitive__Closure_Ortrancl(X0,X1),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Transitive__Closure_Ortrancl__idemp_0) ).
fof(f2114,plain,
! [X0,X1] : c_Transitive__Closure_Ortrancl(X0,X1) = c_Transitive__Closure_Ortrancl(c_Transitive__Closure_Ortrancl(X0,X1),X1),
inference(reorient_equations,[],[f2113]) ).
fof(f2117,axiom,
! [X0,X1] : c_Transitive__Closure_Ortrancl(c_union(X0,c_Relation_OId,tc_prod(X1,X1)),X1) = c_Transitive__Closure_Ortrancl(X0,X1),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Transitive__Closure_Ortrancl__reflcl_0) ).
fof(f2118,plain,
! [X0,X1] : c_Transitive__Closure_Ortrancl(X0,X1) = c_Transitive__Closure_Ortrancl(c_union(X0,c_Relation_OId,tc_prod(X1,X1)),X1),
inference(reorient_equations,[],[f2117]) ).
fof(f2130,axiom,
! [X2,X3,X0,X1] :
( c_Wellfounded__Recursion_Owf(X3,X2)
| ~ c_Wellfounded__Recursion_Owf(c_insert(c_Pair(X0,X1,X2,X2),X3,tc_prod(X2,X2)),X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Wellfounded__Recursion_Owf__insert_0) ).
fof(f2131,axiom,
! [X2,X3,X0,X1] :
( ~ c_in(c_Pair(X1,X0,X2,X2),c_Transitive__Closure_Ortrancl(X3,X2),tc_prod(X2,X2))
| ~ c_Wellfounded__Recursion_Owf(c_insert(c_Pair(X0,X1,X2,X2),X3,tc_prod(X2,X2)),X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Wellfounded__Recursion_Owf__insert_1) ).
fof(f2132,axiom,
! [X2,X3,X0,X1] :
( c_in(c_Pair(X3,X2,X1,X1),c_Transitive__Closure_Ortrancl(X0,X1),tc_prod(X1,X1))
| c_Wellfounded__Recursion_Owf(c_insert(c_Pair(X2,X3,X1,X1),X0,tc_prod(X1,X1)),X1)
| ~ c_Wellfounded__Recursion_Owf(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Wellfounded__Recursion_Owf__insert_2) ).
fof(f2133,axiom,
! [X2,X0,X1] :
( ~ c_in(c_Pair(X2,X2,X1,X1),X0,tc_prod(X1,X1))
| ~ c_Wellfounded__Recursion_Owf(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Wellfounded__Recursion_Owf__not__refl_0) ).
fof(f2134,axiom,
! [X0,X1] :
( c_less(X0,X1,tc_nat)
| ~ c_in(c_Pair(X0,X1,tc_nat,tc_nat),c_Wellfounded__Relations_Oless__than,tc_prod(tc_nat,tc_nat)) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Wellfounded__Relations_Oless__than__iff_0) ).
fof(f2135,axiom,
! [X0,X1] :
( c_in(c_Pair(X0,X1,tc_nat,tc_nat),c_Wellfounded__Relations_Oless__than,tc_prod(tc_nat,tc_nat))
| ~ c_less(X0,X1,tc_nat) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-1.ax',cls_Wellfounded__Relations_Oless__than__iff_1) ).
fof(f2174,axiom,
! [X2,X0,X1] :
( c_in(c_insert(X2,X0,X1),c_Finite__Set_OFinites,tc_set(X1))
| ~ c_in(X0,c_Finite__Set_OFinites,tc_set(X1)) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',cls_Finite__Set_OFinites_OinsertI_0) ).
fof(f2213,axiom,
! [X0,X1] :
( c_Wellfounded__Recursion_Owf(c_List_Olex(X0,X1),tc_List_Olist(X1))
| ~ c_Wellfounded__Recursion_Owf(X0,X1) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',cls_List_Owf__lex_0) ).
fof(f2214,axiom,
! [X0] : c_lessequals(c_0,X0,tc_nat),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',cls_Nat_Ole0_0) ).
fof(f2216,axiom,
! [X0] : ~ c_less(X0,X0,tc_nat),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',cls_Nat_Oless__irrefl_0) ).
fof(f2255,axiom,
! [X0,X1] : c_lessequals(c_emptyset,X0,tc_set(X1)),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',cls_Set_Oempty__subsetI_0) ).
fof(f2256,axiom,
! [X2,X0,X1] :
( ~ c_lessequals(X1,X0,tc_set(X2))
| ~ c_less(X0,X1,tc_set(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',cls_Set_OpsubsetE_0) ).
fof(f2257,axiom,
! [X2,X0,X1] :
( c_lessequals(X0,X1,tc_set(X2))
| ~ c_less(X0,X1,tc_set(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',cls_Set_OpsubsetE_1) ).
fof(f2258,axiom,
! [X2,X0,X1] :
( X0 = X1
| c_less(X0,X1,tc_set(X2))
| ~ c_lessequals(X0,X1,tc_set(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',cls_Set_OpsubsetI_0) ).
fof(f2259,axiom,
! [X2,X0,X1] :
( X0 = X1
| ~ c_in(X0,c_insert(X1,c_emptyset,X2),X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',cls_Set_OsingletonD__dest_0) ).
fof(f2262,axiom,
! [X2,X3,X0,X1] :
( c_in(X0,X3,X2)
| ~ c_lessequals(X1,X3,tc_set(X2))
| ~ c_in(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',cls_Set_OsubsetD_0) ).
fof(f2265,axiom,
! [X2,X0,X1] :
( X1 = X0
| ~ c_lessequals(X1,X0,tc_set(X2))
| ~ c_lessequals(X0,X1,tc_set(X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',cls_Set_Osubset__antisym_0) ).
fof(f2266,plain,
! [X2,X0,X1] :
( X0 = X1
| ~ c_lessequals(X1,X0,tc_set(X2))
| ~ c_lessequals(X0,X1,tc_set(X2)) ),
inference(reorient_equations,[],[f2265]) ).
fof(f2267,axiom,
! [X0,X1] : c_lessequals(X0,X0,tc_set(X1)),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',cls_Set_Osubset__refl_0) ).
fof(f2268,axiom,
! [X2,X3,X0,X1,X4] :
( c_in(c_Sum__Type_OInl(X0,X2,X3),c_Sum__Type_OPlus(X1,X4,X2,X3),tc_sum(X2,X3))
| ~ c_in(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',cls_Sum__Type_OInlI_0) ).
fof(f2269,axiom,
! [X2,X3,X0,X1,X4] :
( c_in(c_Sum__Type_OInr(X0,X2,X3),c_Sum__Type_OPlus(X4,X1,X3,X2),tc_sum(X3,X2))
| ~ c_in(X0,X1,X2) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',cls_Sum__Type_OInrI_0) ).
fof(f2277,axiom,
! [X2,X0,X1] :
( c_in(X0,c_Transitive__Closure_Ortrancl(X1,X2),tc_prod(X2,X2))
| ~ c_in(X0,X1,tc_prod(X2,X2)) ),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',cls_Transitive__Closure_Or__into__rtrancl_0) ).
fof(f2278,axiom,
! [X2,X0,X1] : c_in(c_Pair(X0,X0,X1,X1),c_Transitive__Closure_Ortrancl(X2,X1),tc_prod(X1,X1)),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',cls_Transitive__Closure_Ortrancl_Ortrancl__refl_0) ).
fof(f2281,axiom,
! [X0] : c_Wellfounded__Recursion_Owf(c_emptyset,X0),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',cls_Wellfounded__Recursion_Owf__empty_0) ).
fof(f2282,axiom,
c_Relation_Otrans(c_Wellfounded__Relations_Oless__than,tc_nat),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',cls_Wellfounded__Relations_Otrans__less__than_0) ).
fof(f2284,axiom,
c_Wellfounded__Recursion_Owf(c_Wellfounded__Relations_Oless__than,tc_nat),
file('/export/starexec/sandbox/benchmark/Axioms/MSC001-0.ax',cls_Wellfounded__Relations_Owf__less__than_0) ).
fof(f3318,axiom,
v_A = c_Tarski_Opotype_Opset(v_cl,t_a,tc_Product__Type_Ounit),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Tarski_OA_A_61_61_Apset_Acl_0) ).
fof(f3319,axiom,
! [X0,X1] :
( c_Relation_Orefl(c_Tarski_Opotype_Opset(X0,X1,tc_Product__Type_Ounit),c_Tarski_Opotype_Oorder(X0,X1,tc_Product__Type_Ounit),X1)
| ~ c_in(X0,c_Tarski_OPartialOrder,tc_Tarski_Opotype_Opotype__ext__type(X1,tc_Product__Type_Ounit)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Tarski_OPartialOrder__iff_0) ).
fof(f3320,axiom,
! [X0,X1] :
( c_Relation_Oantisym(c_Tarski_Opotype_Oorder(X0,X1,tc_Product__Type_Ounit),X1)
| ~ c_in(X0,c_Tarski_OPartialOrder,tc_Tarski_Opotype_Opotype__ext__type(X1,tc_Product__Type_Ounit)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Tarski_OPartialOrder__iff_1) ).
fof(f3321,axiom,
! [X0,X1] :
( c_Relation_Otrans(c_Tarski_Opotype_Oorder(X0,X1,tc_Product__Type_Ounit),X1)
| ~ c_in(X0,c_Tarski_OPartialOrder,tc_Tarski_Opotype_Opotype__ext__type(X1,tc_Product__Type_Ounit)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Tarski_OPartialOrder__iff_2) ).
fof(f3322,axiom,
! [X0,X1] :
( c_in(X0,c_Tarski_OPartialOrder,tc_Tarski_Opotype_Opotype__ext__type(X1,tc_Product__Type_Ounit))
| ~ c_Relation_Otrans(c_Tarski_Opotype_Oorder(X0,X1,tc_Product__Type_Ounit),X1)
| ~ c_Relation_Orefl(c_Tarski_Opotype_Opset(X0,X1,tc_Product__Type_Ounit),c_Tarski_Opotype_Oorder(X0,X1,tc_Product__Type_Ounit),X1)
| ~ c_Relation_Oantisym(c_Tarski_Opotype_Oorder(X0,X1,tc_Product__Type_Ounit),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Tarski_OPartialOrder__iff_3) ).
fof(f3323,axiom,
c_in(v_cl,c_Tarski_OPartialOrder,tc_Tarski_Opotype_Opotype__ext__type(t_a,tc_Product__Type_Ounit)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Tarski_Ocl_A_58_APartialOrder_0) ).
fof(f3324,axiom,
v_r = c_Tarski_Opotype_Oorder(v_cl,t_a,tc_Product__Type_Ounit),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Tarski_Or_A_61_61_Aorder_Acl_0) ).
fof(f3325,negated_conjecture,
~ c_Relation_Orefl(v_A,v_r,t_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
tcf(c_2793,negated_conjecture,
~ c_Relation_Orefl(v_A,v_r,t_a),
inference(cnf_transformation,[],[f3325]) ).
tcf(c_2794,plain,
! [X0: $i,X1: $i] :
( c_in(X0,c_Tarski_OPartialOrder,tc_Tarski_Opotype_Opotype__ext__type(X1,tc_Product__Type_Ounit))
| ~ c_Relation_Otrans(c_Tarski_Opotype_Oorder(X0,X1,tc_Product__Type_Ounit),X1)
| ~ c_Relation_Oantisym(c_Tarski_Opotype_Oorder(X0,X1,tc_Product__Type_Ounit),X1)
| ~ c_Relation_Orefl(c_Tarski_Opotype_Opset(X0,X1,tc_Product__Type_Ounit),c_Tarski_Opotype_Oorder(X0,X1,tc_Product__Type_Ounit),X1) ),
inference(cnf_transformation,[],[f3322]) ).
tcf(c_2795,plain,
! [X0: $i,X1: $i] :
( c_Relation_Orefl(c_Tarski_Opotype_Opset(X0,X1,tc_Product__Type_Ounit),c_Tarski_Opotype_Oorder(X0,X1,tc_Product__Type_Ounit),X1)
| ~ c_in(X0,c_Tarski_OPartialOrder,tc_Tarski_Opotype_Opotype__ext__type(X1,tc_Product__Type_Ounit)) ),
inference(cnf_transformation,[],[f3319]) ).
tcf(c_2796,plain,
c_Tarski_Opotype_Opset(v_cl,t_a,tc_Product__Type_Ounit) = v_A,
inference(cnf_transformation,[],[f3318]) ).
tcf(c_2797,plain,
c_in(v_cl,c_Tarski_OPartialOrder,tc_Tarski_Opotype_Opotype__ext__type(t_a,tc_Product__Type_Ounit)),
inference(cnf_transformation,[],[f3323]) ).
tcf(c_2798,plain,
c_Tarski_Opotype_Oorder(v_cl,t_a,tc_Product__Type_Ounit) = v_r,
inference(cnf_transformation,[],[f3324]) ).
tcf(c_2799,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c_in(X3,X1,X2)
| ~ c_in(X3,X0,X2)
| ~ c_lessequals(X0,X1,tc_set(X2)) ),
inference(cnf_transformation,[],[f2262]) ).
tcf(c_2800,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : c_Tarski_Opotype_Opset(c_Tarski_Opotype_Opotype__ext(X0,X1,X2,X3,X4),X3,X4) = X0,
inference(cnf_transformation,[],[f4]) ).
tcf(c_2801,plain,
! [X0: $i,X1: $i] :
( c_Relation_Otrans(c_Tarski_Opotype_Oorder(X0,X1,tc_Product__Type_Ounit),X1)
| ~ c_in(X0,c_Tarski_OPartialOrder,tc_Tarski_Opotype_Opotype__ext__type(X1,tc_Product__Type_Ounit)) ),
inference(cnf_transformation,[],[f3321]) ).
tcf(c_2802,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : c_Tarski_Opotype_Oorder(c_Tarski_Opotype_Opotype__ext(X0,X1,X2,X3,X4),X3,X4) = X1,
inference(cnf_transformation,[],[f5]) ).
tcf(c_2804,plain,
c_Relation_Otrans(c_Wellfounded__Relations_Oless__than,tc_nat),
inference(cnf_transformation,[],[f2282]) ).
tcf(c_2805,plain,
! [X0: $i,X1: $i] :
( c_Relation_Oantisym(c_Tarski_Opotype_Oorder(X0,X1,tc_Product__Type_Ounit),X1)
| ~ c_in(X0,c_Tarski_OPartialOrder,tc_Tarski_Opotype_Opotype__ext__type(X1,tc_Product__Type_Ounit)) ),
inference(cnf_transformation,[],[f3320]) ).
tcf(c_2806,plain,
! [X0: $i] : c_lessequals(c_0,X0,tc_nat),
inference(cnf_transformation,[],[f2214]) ).
tcf(c_2808,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ~ c_lessequals(X0,c_0,tc_nat) ),
inference(cnf_transformation,[],[f1202]) ).
tcf(c_2809,plain,
! [X0: $i,X1: $i] : c_lessequals(X0,X0,tc_set(X1)),
inference(cnf_transformation,[],[f2267]) ).
tcf(c_2810,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = X1 )
| ~ c_lessequals(X1,X0,tc_set(X2))
| ~ c_lessequals(X0,X1,tc_set(X2)) ),
inference(cnf_transformation,[],[f2266]) ).
tcf(c_2811,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_less(X0,X1,tc_set(X2))
| ( X0 = X1 )
| ~ c_lessequals(X0,X1,tc_set(X2)) ),
inference(cnf_transformation,[],[f2258]) ).
tcf(c_2812,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_lessequals(X0,X1,tc_set(X2))
| ~ c_less(X0,X1,tc_set(X2)) ),
inference(cnf_transformation,[],[f2257]) ).
tcf(c_2813,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ c_less(X1,X0,tc_set(X2))
| ~ c_lessequals(X0,X1,tc_set(X2)) ),
inference(cnf_transformation,[],[f2256]) ).
tcf(c_2814,plain,
! [X0: $i,X1: $i] : c_lessequals(c_emptyset,X0,tc_set(X1)),
inference(cnf_transformation,[],[f2255]) ).
tcf(c_2816,plain,
! [X0: $i,X1: $i] :
( ( X0 = c_emptyset )
| ~ c_lessequals(X0,c_emptyset,tc_set(X1)) ),
inference(cnf_transformation,[],[f2097]) ).
tcf(c_2817,plain,
! [X0: $i,X1: $i] : ~ c_less(X0,c_emptyset,tc_set(X1)),
inference(cnf_transformation,[],[f2086]) ).
tcf(c_2818,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( ( X2 = X7 )
| ( c_Tarski_Opotype_Opotype__ext(X0,X1,X2,X3,X4) != c_Tarski_Opotype_Opotype__ext(X5,X6,X7,X3,X4) ) ),
inference(cnf_transformation,[],[f3]) ).
tcf(c_2819,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( ( X1 = X6 )
| ( c_Tarski_Opotype_Opotype__ext(X0,X1,X2,X3,X4) != c_Tarski_Opotype_Opotype__ext(X5,X6,X7,X3,X4) ) ),
inference(cnf_transformation,[],[f2]) ).
tcf(c_2820,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i] :
( ( X0 = X5 )
| ( c_Tarski_Opotype_Opotype__ext(X0,X1,X2,X3,X4) != c_Tarski_Opotype_Opotype__ext(X5,X6,X7,X3,X4) ) ),
inference(cnf_transformation,[],[f1]) ).
tcf(c_2824,plain,
! [X0: $i] : ~ c_less(X0,X0,tc_nat),
inference(cnf_transformation,[],[f2216]) ).
tcf(c_2825,plain,
! [X0: $i] : ~ c_less(X0,c_0,tc_nat),
inference(cnf_transformation,[],[f1263]) ).
tcf(c_2827,plain,
! [X0: $i] :
( c_less(c_0,X0,tc_nat)
| ( X0 = c_0 ) ),
inference(cnf_transformation,[],[f1261]) ).
tcf(c_2828,plain,
c_Wellfounded__Recursion_Owf(c_Wellfounded__Relations_Oless__than,tc_nat),
inference(cnf_transformation,[],[f2284]) ).
tcf(c_2829,plain,
! [X0: $i,X1: $i] :
( c_in(c_Pair(X0,X1,tc_nat,tc_nat),c_Wellfounded__Relations_Oless__than,tc_prod(tc_nat,tc_nat))
| ~ c_less(X0,X1,tc_nat) ),
inference(cnf_transformation,[],[f2135]) ).
tcf(c_2830,plain,
! [X0: $i,X1: $i] :
( c_less(X0,X1,tc_nat)
| ~ c_in(c_Pair(X0,X1,tc_nat,tc_nat),c_Wellfounded__Relations_Oless__than,tc_prod(tc_nat,tc_nat)) ),
inference(cnf_transformation,[],[f2134]) ).
tcf(c_2831,plain,
! [X0: $i,X1: $i] : ~ c_in(X0,c_emptyset,X1),
inference(cnf_transformation,[],[f2060]) ).
tcf(c_2832,plain,
! [X0: $i,X1: $i] : c_minus(c_emptyset,X0,tc_set(X1)) = c_emptyset,
inference(cnf_transformation,[],[f2054]) ).
tcf(c_2833,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( c_minus(X0,X1,tc_set(X2)) = c_emptyset )
| ~ c_lessequals(X0,X1,tc_set(X2)) ),
inference(cnf_transformation,[],[f1945]) ).
tcf(c_2834,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_lessequals(X0,X1,tc_set(X2))
| ( c_minus(X0,X1,tc_set(X2)) != c_emptyset ) ),
inference(cnf_transformation,[],[f1943]) ).
tcf(c_2835,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_emptyset,tc_set(X1)) = X0,
inference(cnf_transformation,[],[f1941]) ).
tcf(c_2836,plain,
! [X0: $i,X1: $i] : c_minus(X0,X0,tc_set(X1)) = c_emptyset,
inference(cnf_transformation,[],[f1938]) ).
tcf(c_2837,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( c_in(c_Sum__Type_OInr(X0,X2,X3),c_Sum__Type_OPlus(X4,X1,X3,X2),tc_sum(X3,X2))
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[],[f2269]) ).
tcf(c_2838,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( c_in(c_Sum__Type_OInl(X0,X2,X3),c_Sum__Type_OPlus(X1,X4,X2,X3),tc_sum(X2,X3))
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[],[f2268]) ).
tcf(c_2839,plain,
! [X0: $i,X1: $i,X2: $i] : c_Nat_Osize(c_Sum__Type_OInr(X0,X1,X2),tc_sum(X2,X1)) = c_0,
inference(cnf_transformation,[],[f44]) ).
tcf(c_2840,plain,
! [X0: $i,X1: $i,X2: $i] : c_Nat_Osize(c_Sum__Type_OInl(X0,X1,X2),tc_sum(X1,X2)) = c_0,
inference(cnf_transformation,[],[f42]) ).
tcf(c_2841,plain,
! [X0: $i,X1: $i] : c_Nat_Opower(X0,c_1,tc_set(tc_prod(X1,X1))) = X0,
inference(cnf_transformation,[],[f1661]) ).
tcf(c_2842,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : c_Nat_Osize(c_Pair(X0,X1,X2,X3),tc_prod(X2,X3)) = c_0,
inference(cnf_transformation,[],[f40]) ).
tcf(c_2843,plain,
! [X0: $i] : c_Wellfounded__Recursion_Owf(c_emptyset,X0),
inference(cnf_transformation,[],[f2281]) ).
tcf(c_2844,plain,
! [X0: $i,X1: $i] :
( c_Wellfounded__Recursion_Owf(c_List_Olex(X0,X1),tc_List_Olist(X1))
| ~ c_Wellfounded__Recursion_Owf(X0,X1) ),
inference(cnf_transformation,[],[f2213]) ).
tcf(c_2845,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ c_Wellfounded__Recursion_Owf(X2,X1)
| ~ c_in(c_Pair(X0,X0,X1,X1),X2,tc_prod(X1,X1)) ),
inference(cnf_transformation,[],[f2133]) ).
tcf(c_2846,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c_Wellfounded__Recursion_Owf(c_insert(c_Pair(X3,X2,X1,X1),X0,tc_prod(X1,X1)),X1)
| c_in(c_Pair(X2,X3,X1,X1),c_Transitive__Closure_Ortrancl(X0,X1),tc_prod(X1,X1))
| ~ c_Wellfounded__Recursion_Owf(X0,X1) ),
inference(cnf_transformation,[],[f2132]) ).
tcf(c_2847,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ c_Wellfounded__Recursion_Owf(c_insert(c_Pair(X1,X0,X2,X2),X3,tc_prod(X2,X2)),X2)
| ~ c_in(c_Pair(X0,X1,X2,X2),c_Transitive__Closure_Ortrancl(X3,X2),tc_prod(X2,X2)) ),
inference(cnf_transformation,[],[f2131]) ).
tcf(c_2848,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c_Wellfounded__Recursion_Owf(X3,X2)
| ~ c_Wellfounded__Recursion_Owf(c_insert(c_Pair(X0,X1,X2,X2),X3,tc_prod(X2,X2)),X2) ),
inference(cnf_transformation,[],[f2130]) ).
tcf(c_2849,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( X1 = X5 )
| ( c_Pair(X0,X1,X2,X3) != c_Pair(X4,X5,X2,X3) ) ),
inference(cnf_transformation,[],[f1626]) ).
tcf(c_2850,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( X0 = X4 )
| ( c_Pair(X0,X1,X2,X3) != c_Pair(X4,X5,X2,X3) ) ),
inference(cnf_transformation,[],[f1625]) ).
tcf(c_2851,plain,
! [X0: $i,X1: $i,X2: $i] : c_insert(X0,c_minus(X1,c_insert(X0,c_emptyset,X2),tc_set(X2)),X2) = c_insert(X0,X1,X2),
inference(cnf_transformation,[],[f2065]) ).
tcf(c_2852,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( c_minus(c_insert(X0,X3,X2),X1,tc_set(X2)) = c_minus(X3,X1,tc_set(X2)) )
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[],[f2063]) ).
tcf(c_2853,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c_in(X1,X0,X3)
| ( c_minus(X0,c_insert(X1,X2,X3),tc_set(X3)) = c_minus(X0,X2,tc_set(X3)) ) ),
inference(cnf_transformation,[],[f1952]) ).
tcf(c_2854,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c_in(X0,X3,X2)
| c_in(X0,c_minus(X1,X3,tc_set(X2)),X2)
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[],[f1950]) ).
tcf(c_2855,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ c_in(X0,X2,X3)
| ~ c_in(X0,c_minus(X1,X2,tc_set(X3)),X3) ),
inference(cnf_transformation,[],[f1949]) ).
tcf(c_2856,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c_in(X0,X1,X3)
| ~ c_in(X0,c_minus(X1,X2,tc_set(X3)),X3) ),
inference(cnf_transformation,[],[f1948]) ).
tcf(c_2857,plain,
! [X0: $i,X1: $i,X2: $i] : c_minus(c_minus(X0,X1,tc_set(X2)),X1,tc_set(X2)) = c_minus(X0,X1,tc_set(X2)),
inference(cnf_transformation,[],[f1947]) ).
tcf(c_2858,plain,
! [X0: $i,X1: $i] :
( c_less(c_0,c_minus(X1,X0,tc_nat),tc_nat)
| ~ c_less(X0,X1,tc_nat) ),
inference(cnf_transformation,[],[f1280]) ).
tcf(c_2859,plain,
! [X0: $i,X1: $i] :
( c_less(X1,X0,tc_nat)
| ~ c_less(c_0,c_minus(X0,X1,tc_nat),tc_nat) ),
inference(cnf_transformation,[],[f1279]) ).
tcf(c_2860,plain,
! [X0: $i] : c_minus(X0,c_0,tc_nat) = X0,
inference(cnf_transformation,[],[f1278]) ).
tcf(c_2861,plain,
! [X0: $i,X1: $i] :
( ( c_plus(X0,c_minus(X1,X0,tc_nat),tc_nat) = X1 )
| ~ c_lessequals(X0,X1,tc_nat) ),
inference(cnf_transformation,[],[f1205]) ).
tcf(c_2862,plain,
! [X0: $i,X1: $i] :
( ( c_plus(c_minus(X1,X0,tc_nat),X0,tc_nat) = X1 )
| ~ c_lessequals(X0,X1,tc_nat) ),
inference(cnf_transformation,[],[f1204]) ).
tcf(c_2863,plain,
! [X0: $i] : c_minus(X0,X0,tc_nat) = c_0,
inference(cnf_transformation,[],[f1200]) ).
tcf(c_2864,plain,
! [X0: $i,X1: $i] : c_lessequals(c_minus(X0,X1,tc_nat),X0,tc_nat),
inference(cnf_transformation,[],[f1198]) ).
tcf(c_2865,plain,
! [X0: $i,X1: $i] :
( ( c_minus(X0,X1,tc_nat) = c_0 )
| ~ c_lessequals(X0,X1,tc_nat) ),
inference(cnf_transformation,[],[f1197]) ).
tcf(c_2866,plain,
! [X0: $i,X1: $i] :
( c_lessequals(X0,X1,tc_nat)
| ( c_minus(X0,X1,tc_nat) != c_0 ) ),
inference(cnf_transformation,[],[f1195]) ).
tcf(c_2867,plain,
! [X0: $i,X1: $i,X2: $i] : c_minus(c_minus(X0,X1,tc_nat),X2,tc_nat) = c_minus(X0,c_plus(X1,X2,tc_nat),tc_nat),
inference(cnf_transformation,[],[f1193]) ).
tcf(c_2868,plain,
! [X0: $i,X1: $i] :
( c_less(c_minus(X0,c_Suc(X1),tc_nat),X0,tc_nat)
| ~ c_less(c_0,X0,tc_nat) ),
inference(cnf_transformation,[],[f1192]) ).
tcf(c_2869,plain,
! [X0: $i,X1: $i] : c_minus(c_Suc(X0),c_Suc(X1),tc_nat) = c_minus(X0,X1,tc_nat),
inference(cnf_transformation,[],[f1191]) ).
tcf(c_2870,plain,
! [X0: $i] : c_minus(c_0,X0,tc_nat) = c_0,
inference(cnf_transformation,[],[f1189]) ).
tcf(c_2871,plain,
! [X0: $i] :
( ( c_Suc(c_minus(X0,c_Suc(c_0),tc_nat)) = X0 )
| ~ c_less(c_0,X0,tc_nat) ),
inference(cnf_transformation,[],[f1175]) ).
tcf(c_2872,plain,
! [X0: $i,X1: $i,X2: $i] : c_minus(c_minus(c_Suc(X0),X1,tc_nat),c_Suc(X2),tc_nat) = c_minus(c_minus(X0,X1,tc_nat),X2,tc_nat),
inference(cnf_transformation,[],[f1168]) ).
tcf(c_2873,plain,
! [X0: $i,X1: $i] :
( c_less(c_minus(X0,X1,tc_nat),X0,tc_nat)
| ~ c_less(c_0,X1,tc_nat)
| ~ c_less(c_0,X0,tc_nat) ),
inference(cnf_transformation,[],[f906]) ).
tcf(c_2874,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( c_minus(c_plus(X2,X0,tc_nat),X1,tc_nat) = c_minus(X2,c_minus(X1,X0,tc_nat),tc_nat) )
| ~ c_lessequals(X0,X1,tc_nat) ),
inference(cnf_transformation,[],[f905]) ).
tcf(c_2875,plain,
! [X0: $i,X1: $i] :
( ( c_minus(X1,c_minus(X1,X0,tc_nat),tc_nat) = X0 )
| ~ c_lessequals(X0,X1,tc_nat) ),
inference(cnf_transformation,[],[f904]) ).
tcf(c_2876,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( c_minus(c_Suc(c_minus(X1,X0,tc_nat)),X2,tc_nat) = c_minus(c_Suc(X1),c_plus(X0,X2,tc_nat),tc_nat) )
| ~ c_lessequals(X0,X1,tc_nat) ),
inference(cnf_transformation,[],[f903]) ).
tcf(c_2877,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( c_minus(c_plus(X2,X0,tc_nat),c_Suc(X1),tc_nat) = c_minus(X2,c_Suc(c_minus(X1,X0,tc_nat)),tc_nat) )
| ~ c_lessequals(X0,X1,tc_nat) ),
inference(cnf_transformation,[],[f902]) ).
tcf(c_2878,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( c_plus(X2,c_minus(X1,X0,tc_nat),tc_nat) = c_minus(c_plus(X2,X1,tc_nat),X0,tc_nat) )
| ~ c_lessequals(X0,X1,tc_nat) ),
inference(cnf_transformation,[],[f901]) ).
tcf(c_2879,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( c_plus(c_minus(X1,X0,tc_nat),X2,tc_nat) = c_minus(c_plus(X1,X2,tc_nat),X0,tc_nat) )
| ~ c_lessequals(X0,X1,tc_nat) ),
inference(cnf_transformation,[],[f900]) ).
tcf(c_2880,plain,
! [X0: $i,X1: $i] :
( c_lessequals(X0,c_minus(X1,c_1,tc_IntDef_Oint),tc_IntDef_Oint)
| ~ c_less(X0,X1,tc_IntDef_Oint) ),
inference(cnf_transformation,[],[f293]) ).
tcf(c_2881,plain,
! [X0: $i,X1: $i] :
( c_less(X0,X1,tc_IntDef_Oint)
| ~ c_lessequals(X0,c_minus(X1,c_1,tc_IntDef_Oint),tc_IntDef_Oint) ),
inference(cnf_transformation,[],[f292]) ).
tcf(c_2882,plain,
! [X0: $i,X1: $i] : c_plus(X0,c_uminus(X1,tc_IntDef_Oint),tc_IntDef_Oint) = c_minus(X0,X1,tc_IntDef_Oint),
inference(cnf_transformation,[],[f286]) ).
tcf(c_2884,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X0 = X3 )
| ( c_Sum__Type_OInr(X0,X1,X2) != c_Sum__Type_OInr(X3,X1,X2) ) ),
inference(cnf_transformation,[],[f2101]) ).
tcf(c_2885,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : c_Sum__Type_OInl(X0,X1,X2) != c_Sum__Type_OInr(X3,X2,X1),
inference(cnf_transformation,[],[f2100]) ).
tcf(c_2886,plain,
! [X0: $i,X1: $i] : c_Sum__Type_OPlus(c_UNIV,c_UNIV,X0,X1) = c_UNIV,
inference(cnf_transformation,[],[f2104]) ).
tcf(c_2887,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X0 = X3 )
| ( c_Sum__Type_OInl(X0,X1,X2) != c_Sum__Type_OInl(X3,X1,X2) ) ),
inference(cnf_transformation,[],[f2099]) ).
tcf(c_2888,plain,
! [X0: $i,X1: $i,X2: $i] : c_plus(c_Nat_Osize(X0,tc_List_Olist(X1)),c_Suc(c_0),tc_nat) = c_Nat_Osize(c_List_Olist_OCons(X2,X0,X1),tc_List_Olist(X1)),
inference(cnf_transformation,[],[f656]) ).
tcf(c_2889,plain,
! [X0: $i,X1: $i] :
( c_less(c_0,c_Nat_Osize(X0,tc_List_Olist(X1)),tc_nat)
| ( X0 = c_List_Olist_ONil ) ),
inference(cnf_transformation,[],[f622]) ).
tcf(c_2891,plain,
! [X0: $i,X1: $i,X2: $i] : c_plus(c_Nat_Osize(X0,tc_List_Olist(X1)),c_Nat_Osize(X2,tc_List_Olist(X1)),tc_nat) = c_Nat_Osize(c_append(X0,X2,X1),tc_List_Olist(X1)),
inference(cnf_transformation,[],[f617]) ).
tcf(c_2892,plain,
! [X0: $i] : c_Nat_Osize(c_List_Olist_ONil,tc_List_Olist(X0)) = c_0,
inference(cnf_transformation,[],[f616]) ).
tcf(c_2893,plain,
! [X0: $i,X1: $i] :
( ( X0 = c_List_Olist_ONil )
| ( c_Nat_Osize(X0,tc_List_Olist(X1)) != c_0 ) ),
inference(cnf_transformation,[],[f614]) ).
tcf(c_2894,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( X1 = X4 )
| ( c_Nat_Osize(X1,tc_List_Olist(X2)) != c_Nat_Osize(X4,tc_List_Olist(X2)) )
| ( c_append(X0,X1,X2) != c_append(X3,X4,X2) ) ),
inference(cnf_transformation,[],[f510]) ).
tcf(c_2895,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( X0 = X3 )
| ( c_Nat_Osize(X1,tc_List_Olist(X2)) != c_Nat_Osize(X4,tc_List_Olist(X2)) )
| ( c_append(X0,X1,X2) != c_append(X3,X4,X2) ) ),
inference(cnf_transformation,[],[f509]) ).
tcf(c_2896,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( X1 = X4 )
| ( c_Nat_Osize(X0,tc_List_Olist(X2)) != c_Nat_Osize(X3,tc_List_Olist(X2)) )
| ( c_append(X0,X1,X2) != c_append(X3,X4,X2) ) ),
inference(cnf_transformation,[],[f508]) ).
tcf(c_2897,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( ( X0 = X3 )
| ( c_Nat_Osize(X0,tc_List_Olist(X2)) != c_Nat_Osize(X3,tc_List_Olist(X2)) )
| ( c_append(X0,X1,X2) != c_append(X3,X4,X2) ) ),
inference(cnf_transformation,[],[f507]) ).
tcf(c_2898,plain,
c_less(c_0,c_1,tc_nat),
inference(cnf_transformation,[],[f1211]) ).
tcf(c_2899,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ~ c_less(X0,c_1,tc_nat) ),
inference(cnf_transformation,[],[f1210]) ).
tcf(c_2900,plain,
c_0 != c_1,
inference(cnf_transformation,[],[f311]) ).
tcf(c_2901,plain,
! [X0: $i,X1: $i] : c_times(X0,c_Nat_Opower(X0,X1,tc_nat),tc_nat) = c_Nat_Opower(X0,c_Suc(X1),tc_nat),
inference(cnf_transformation,[],[f1600]) ).
tcf(c_2902,plain,
! [X0: $i] : c_Nat_Opower(X0,c_0,tc_nat) = c_1,
inference(cnf_transformation,[],[f1599]) ).
tcf(c_2904,plain,
! [X0: $i,X1: $i] :
( c_less(c_0,c_Nat_Opower(X0,X1,tc_nat),tc_nat)
| ( X0 = c_0 ) ),
inference(cnf_transformation,[],[f1596]) ).
tcf(c_2905,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ~ c_less(c_0,c_Nat_Opower(c_0,X0,tc_nat),tc_nat) ),
inference(cnf_transformation,[],[f1594]) ).
tcf(c_2906,plain,
! [X0: $i,X1: $i] :
( c_lessequals(c_Suc(c_0),c_Nat_Opower(X0,X1,tc_nat),tc_nat)
| ~ c_lessequals(c_1,X0,tc_nat) ),
inference(cnf_transformation,[],[f1592]) ).
tcf(c_2907,plain,
! [X0: $i,X1: $i] :
( c_less(c_0,c_Nat_Opower(X0,c_Numeral_Onumber__of(X1,tc_nat),tc_nat),tc_nat)
| ~ c_less(c_0,X0,tc_nat) ),
inference(cnf_transformation,[],[f1591]) ).
tcf(c_2908,plain,
! [X0: $i,X1: $i] :
( c_less(c_0,c_Nat_Opower(X1,c_Numeral_Onumber__of(X0,tc_nat),tc_nat),tc_nat)
| ( c_Numeral_Onumber__of(X0,tc_nat) != c_0 ) ),
inference(cnf_transformation,[],[f1590]) ).
tcf(c_2909,plain,
! [X0: $i,X1: $i] :
( c_less(c_0,X0,tc_nat)
| ( c_Numeral_Onumber__of(X1,tc_nat) = c_0 )
| ~ c_less(c_0,c_Nat_Opower(X0,c_Numeral_Onumber__of(X1,tc_nat),tc_nat),tc_nat) ),
inference(cnf_transformation,[],[f1588]) ).
tcf(c_2916,plain,
! [X0: $i,X1: $i] : c_times(X0,c_Nat_Opower(X0,X1,tc_IntDef_Oint),tc_IntDef_Oint) = c_Nat_Opower(X0,c_Suc(X1),tc_IntDef_Oint),
inference(cnf_transformation,[],[f424]) ).
tcf(c_2917,plain,
! [X0: $i] : c_Nat_Opower(X0,c_0,tc_IntDef_Oint) = c_1,
inference(cnf_transformation,[],[f423]) ).
tcf(c_2918,plain,
! [X0: $i,X1: $i,X2: $i] : ~ c_in(c_Pair(c_List_Olist_ONil,X0,tc_List_Olist(X1),tc_List_Olist(X1)),c_List_Olex(X2,X1),tc_prod(tc_List_Olist(X1),tc_List_Olist(X1))),
inference(cnf_transformation,[],[f501]) ).
tcf(c_2919,plain,
! [X0: $i,X1: $i,X2: $i] : ~ c_in(c_Pair(X0,c_List_Olist_ONil,tc_List_Olist(X1),tc_List_Olist(X1)),c_List_Olex(X2,X1),tc_prod(tc_List_Olist(X1),tc_List_Olist(X1))),
inference(cnf_transformation,[],[f487]) ).
tcf(c_2920,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( c_in(c_Pair(c_List_Olist_OCons(X4,X0,X2),c_List_Olist_OCons(X4,X1,X2),tc_List_Olist(X2),tc_List_Olist(X2)),c_List_Olex(X3,X2),tc_prod(tc_List_Olist(X2),tc_List_Olist(X2)))
| ~ c_in(c_Pair(X0,X1,tc_List_Olist(X2),tc_List_Olist(X2)),c_List_Olex(X3,X2),tc_prod(tc_List_Olist(X2),tc_List_Olist(X2))) ),
inference(cnf_transformation,[],[f486]) ).
tcf(c_2921,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( c_in(c_Pair(c_List_Olist_OCons(X3,X0,X1),c_List_Olist_OCons(X4,X2,X1),tc_List_Olist(X1),tc_List_Olist(X1)),c_List_Olex(X5,X1),tc_prod(tc_List_Olist(X1),tc_List_Olist(X1)))
| ~ c_in(c_Pair(X3,X4,X1,X1),X5,tc_prod(X1,X1))
| ( c_Nat_Osize(X0,tc_List_Olist(X1)) != c_Nat_Osize(X2,tc_List_Olist(X1)) ) ),
inference(cnf_transformation,[],[f485]) ).
tcf(c_2922,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( c_in(c_Pair(X1,X4,tc_List_Olist(X2),tc_List_Olist(X2)),c_List_Olex(X5,X2),tc_prod(tc_List_Olist(X2),tc_List_Olist(X2)))
| ( c_Nat_Osize(X1,tc_List_Olist(X2)) = c_Nat_Osize(X4,tc_List_Olist(X2)) )
| ~ c_in(c_Pair(c_List_Olist_OCons(X0,X1,X2),c_List_Olist_OCons(X3,X4,X2),tc_List_Olist(X2),tc_List_Olist(X2)),c_List_Olex(X5,X2),tc_prod(tc_List_Olist(X2),tc_List_Olist(X2))) ),
inference(cnf_transformation,[],[f484]) ).
tcf(c_2923,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( ( X0 = X3 )
| ( c_Nat_Osize(X1,tc_List_Olist(X2)) = c_Nat_Osize(X4,tc_List_Olist(X2)) )
| ~ c_in(c_Pair(c_List_Olist_OCons(X0,X1,X2),c_List_Olist_OCons(X3,X4,X2),tc_List_Olist(X2),tc_List_Olist(X2)),c_List_Olex(X5,X2),tc_prod(tc_List_Olist(X2),tc_List_Olist(X2))) ),
inference(cnf_transformation,[],[f483]) ).
tcf(c_2924,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( c_in(c_Pair(X0,X3,X2,X2),X5,tc_prod(X2,X2))
| c_in(c_Pair(X1,X4,tc_List_Olist(X2),tc_List_Olist(X2)),c_List_Olex(X5,X2),tc_prod(tc_List_Olist(X2),tc_List_Olist(X2)))
| ~ c_in(c_Pair(c_List_Olist_OCons(X0,X1,X2),c_List_Olist_OCons(X3,X4,X2),tc_List_Olist(X2),tc_List_Olist(X2)),c_List_Olex(X5,X2),tc_prod(tc_List_Olist(X2),tc_List_Olist(X2))) ),
inference(cnf_transformation,[],[f482]) ).
tcf(c_2925,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i] :
( c_in(c_Pair(X0,X3,X2,X2),X5,tc_prod(X2,X2))
| ( X0 = X3 )
| ~ c_in(c_Pair(c_List_Olist_OCons(X0,X1,X2),c_List_Olist_OCons(X3,X4,X2),tc_List_Olist(X2),tc_List_Olist(X2)),c_List_Olex(X5,X2),tc_prod(tc_List_Olist(X2),tc_List_Olist(X2))) ),
inference(cnf_transformation,[],[f481]) ).
tcf(c_2928,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( X0 = X1 )
| ~ c_in(X0,c_insert(X1,c_emptyset,X2),X2) ),
inference(cnf_transformation,[],[f2259]) ).
tcf(c_2929,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_in(c_insert(X2,X0,X1),c_Finite__Set_OFinites,tc_set(X1))
| ~ c_in(X0,c_Finite__Set_OFinites,tc_set(X1)) ),
inference(cnf_transformation,[],[f2174]) ).
tcf(c_2933,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( c_insert(X1,X0,X2) = c_insert(X1,c_emptyset,X2) )
| ~ c_lessequals(X0,c_insert(X1,c_emptyset,X2),tc_set(X2)) ),
inference(cnf_transformation,[],[f2090]) ).
tcf(c_2934,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c_lessequals(X1,c_insert(X3,c_emptyset,X2),tc_set(X2))
| ( c_insert(X0,X1,X2) != c_insert(X3,c_emptyset,X2) ) ),
inference(cnf_transformation,[],[f2089]) ).
tcf(c_2935,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( X0 = X3 )
| ( c_insert(X0,X1,X2) != c_insert(X3,c_emptyset,X2) ) ),
inference(cnf_transformation,[],[f2088]) ).
tcf(c_2936,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c_lessequals(c_insert(X3,X0,X2),X1,tc_set(X2))
| ~ c_in(X3,X1,X2)
| ~ c_lessequals(X0,X1,tc_set(X2)) ),
inference(cnf_transformation,[],[f2085]) ).
tcf(c_2937,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c_lessequals(X1,X3,tc_set(X2))
| ~ c_lessequals(c_insert(X0,X1,X2),X3,tc_set(X2)) ),
inference(cnf_transformation,[],[f2084]) ).
tcf(c_2938,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c_in(X0,X3,X2)
| ~ c_lessequals(c_insert(X0,X1,X2),X3,tc_set(X2)) ),
inference(cnf_transformation,[],[f2083]) ).
tcf(c_2940,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c_in(X0,c_insert(X3,X1,X2),X2)
| ~ c_in(X0,X1,X2) ),
inference(cnf_transformation,[],[f2079]) ).
tcf(c_2941,plain,
! [X0: $i,X1: $i,X2: $i] : c_in(X0,c_insert(X0,X1,X2),X2),
inference(cnf_transformation,[],[f2078]) ).
tcf(c_2942,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c_in(X0,X2,X3)
| ( X0 = X1 )
| ~ c_in(X0,c_insert(X1,X2,X3),X3) ),
inference(cnf_transformation,[],[f2077]) ).
tcf(c_2943,plain,
! [X0: $i,X1: $i,X2: $i] : c_insert(X0,c_insert(X0,X1,X2),X2) = c_insert(X0,X1,X2),
inference(cnf_transformation,[],[f2067]) ).
tcf(c_2944,plain,
! [X0: $i,X1: $i,X2: $i] : c_insert(X0,X1,X2) != c_emptyset,
inference(cnf_transformation,[],[f2061]) ).
tcf(c_2945,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_in(X1,c_Finite__Set_OFinites,tc_set(X2))
| ~ c_in(c_insert(X0,X1,X2),c_Finite__Set_OFinites,tc_set(X2)) ),
inference(cnf_transformation,[],[f210]) ).
tcf(c_2946,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c_in(c_minus(X0,c_insert(X3,X1,X2),tc_set(X2)),c_Finite__Set_OFinites,tc_set(X2))
| ~ c_in(c_minus(X0,X1,tc_set(X2)),c_Finite__Set_OFinites,tc_set(X2)) ),
inference(cnf_transformation,[],[f202]) ).
tcf(c_2947,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c_in(c_minus(X0,X2,tc_set(X3)),c_Finite__Set_OFinites,tc_set(X3))
| ~ c_in(c_minus(X0,c_insert(X1,X2,X3),tc_set(X3)),c_Finite__Set_OFinites,tc_set(X3)) ),
inference(cnf_transformation,[],[f201]) ).
tcf(c_2948,plain,
! [X0: $i,X1: $i,X2: $i] : c_in(c_Pair(X0,X0,X1,X1),c_Transitive__Closure_Ortrancl(X2,X1),tc_prod(X1,X1)),
inference(cnf_transformation,[],[f2278]) ).
tcf(c_2949,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_in(X0,c_Transitive__Closure_Ortrancl(X1,X2),tc_prod(X2,X2))
| ~ c_in(X0,X1,tc_prod(X2,X2)) ),
inference(cnf_transformation,[],[f2277]) ).
tcf(c_2950,plain,
! [X0: $i,X1: $i] : c_Transitive__Closure_Ortrancl(c_union(X0,c_Relation_OId,tc_prod(X1,X1)),X1) = c_Transitive__Closure_Ortrancl(X0,X1),
inference(cnf_transformation,[],[f2118]) ).
tcf(c_2951,plain,
! [X0: $i,X1: $i] : c_Transitive__Closure_Ortrancl(c_Transitive__Closure_Ortrancl(X0,X1),X1) = c_Transitive__Closure_Ortrancl(X0,X1),
inference(cnf_transformation,[],[f2114]) ).
tcf(c_2952,plain,
! [X0: $i] : c_Transitive__Closure_Ortrancl(c_emptyset,X0) = c_Relation_OId,
inference(cnf_transformation,[],[f2112]) ).
tcf(c_4375,plain,
! [X0: $i,X1: $i,X2: $i] : c_minus(c_minus(c_Suc(X0),X1,tc_nat),c_Suc(X2),tc_nat) = c_minus(X0,c_plus(X1,X2,tc_nat),tc_nat),
inference(light_normalisation,[status(thm)],[c_2872,c_2867]) ).
tcf(c_4376,plain,
! [X0: $i,X1: $i,X2: $i] : c_minus(c_Suc(X0),c_plus(X1,c_Suc(X2),tc_nat),tc_nat) = c_minus(X0,c_plus(X1,X2,tc_nat),tc_nat),
inference(demodulation,[status(thm)],[c_4375,c_2867]) ).
tcf(c_8488,plain,
! [X0: $i] : c_lessequals(X0,X0,tc_nat),
inference(superposition,[status(thm)],[c_2860,c_2864]) ).
tcf(c_8490,plain,
c_lessequals(c_0,c_0,tc_nat),
inference(superposition,[status(thm)],[c_2870,c_2864]) ).
tcf(c_8518,plain,
! [X0: $i] : c_Transitive__Closure_Ortrancl(c_Relation_OId,X0) = c_Relation_OId,
inference(superposition,[status(thm)],[c_2952,c_2951]) ).
tcf(c_8539,plain,
! [X0: $i,X1: $i] : ~ c_less(X0,X0,tc_set(X1)),
inference(superposition,[status(thm)],[c_2809,c_2813]) ).
tcf(c_8552,plain,
! [X0: $i,X1: $i] :
( c_less(X1,X0,tc_nat)
| ( c_minus(X0,X1,tc_nat) = c_0 ) ),
inference(superposition,[status(thm)],[c_2827,c_2859]) ).
tcf(c_8554,plain,
! [X0: $i] :
( c_less(X0,c_0,tc_nat)
| ~ c_less(c_0,c_0,tc_nat) ),
inference(superposition,[status(thm)],[c_2870,c_2859]) ).
tcf(c_8555,plain,
! [X0: $i] :
( c_less(X0,X0,tc_nat)
| ~ c_less(c_0,c_0,tc_nat) ),
inference(superposition,[status(thm)],[c_2863,c_2859]) ).
tcf(c_8564,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ( c_minus(c_1,X0,tc_nat) = c_0 ) ),
inference(superposition,[status(thm)],[c_8552,c_2899]) ).
tcf(c_8566,plain,
! [X0: $i,X1: $i] :
( c_less(X1,X0,tc_nat)
| ( c_minus(c_minus(X0,X1,tc_nat),c_0,tc_nat) = c_0 ) ),
inference(superposition,[status(thm)],[c_8552,c_2859]) ).
tcf(c_8579,plain,
! [X0: $i] :
( c_less(X0,c_1,tc_nat)
| ( X0 = c_0 )
| ~ c_less(c_0,c_0,tc_nat) ),
inference(superposition,[status(thm)],[c_8564,c_2859]) ).
tcf(c_8580,plain,
! [X0: $i] :
( c_lessequals(c_0,c_1,tc_nat)
| ( X0 = c_0 ) ),
inference(superposition,[status(thm)],[c_8564,c_2864]) ).
tcf(c_8587,plain,
! [X0: $i,X1: $i] : c_minus(c_minus(X0,X1,tc_nat),X0,tc_nat) = c_0,
inference(superposition,[status(thm)],[c_2864,c_2865]) ).
tcf(c_8590,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_plus(X1,X0,tc_nat),tc_nat) = c_0,
inference(demodulation,[status(thm)],[c_8587,c_2867]) ).
tcf(c_8591,plain,
! [X0: $i,X1: $i] :
( c_less(c_0,c_0,tc_nat)
| ~ c_less(c_plus(X0,X1,tc_nat),X1,tc_nat) ),
inference(superposition,[status(thm)],[c_8590,c_2858]) ).
tcf(c_8592,plain,
! [X0: $i,X1: $i] :
( c_less(c_plus(X0,X1,tc_nat),X1,tc_nat)
| ~ c_less(c_0,c_0,tc_nat) ),
inference(superposition,[status(thm)],[c_8590,c_2859]) ).
tcf(c_8594,plain,
! [X0: $i,X1: $i] : ~ c_less(c_plus(X0,X1,tc_nat),X1,tc_nat),
inference(forward_subsumption_resolution,[status(thm)],[c_8591,c_2825]) ).
tcf(c_8603,plain,
! [X0: $i] :
( c_lessequals(X0,c_0,tc_nat)
| ( X0 != c_0 ) ),
inference(superposition,[status(thm)],[c_2860,c_2866]) ).
tcf(c_8604,plain,
! [X0: $i] :
( c_lessequals(c_1,X0,tc_nat)
| ( X0 = c_0 ) ),
inference(superposition,[status(thm)],[c_8564,c_2866]) ).
tcf(c_8605,plain,
! [X0: $i,X1: $i] : c_lessequals(X0,c_plus(X1,X0,tc_nat),tc_nat),
inference(superposition,[status(thm)],[c_8590,c_2866]) ).
tcf(c_8620,plain,
! [X0: $i,X1: $i] :
( c_less(c_0,c_minus(X1,X0,tc_nat),tc_nat)
| ~ c_less(c_Suc(X0),c_Suc(X1),tc_nat) ),
inference(superposition,[status(thm)],[c_2869,c_2858]) ).
tcf(c_8621,plain,
! [X0: $i,X1: $i] :
( c_lessequals(c_Suc(X0),c_Suc(X1),tc_nat)
| ( c_minus(X0,X1,tc_nat) != c_0 ) ),
inference(superposition,[status(thm)],[c_2869,c_2866]) ).
tcf(c_8622,plain,
! [X0: $i,X1: $i] :
( c_less(c_Suc(X1),c_Suc(X0),tc_nat)
| ~ c_less(c_0,c_minus(X0,X1,tc_nat),tc_nat) ),
inference(superposition,[status(thm)],[c_2869,c_2859]) ).
tcf(c_8623,plain,
! [X0: $i,X1: $i] : c_lessequals(c_minus(X0,X1,tc_nat),c_Suc(X0),tc_nat),
inference(superposition,[status(thm)],[c_2869,c_2864]) ).
tcf(c_8651,plain,
! [X0: $i,X1: $i] : c_lessequals(c_minus(X0,X1,tc_nat),c_Suc(c_Suc(X0)),tc_nat),
inference(superposition,[status(thm)],[c_2869,c_8623]) ).
tcf(c_8653,plain,
! [X0: $i] : c_lessequals(X0,c_Suc(X0),tc_nat),
inference(superposition,[status(thm)],[c_2860,c_8623]) ).
tcf(c_8654,plain,
! [X0: $i] :
( c_lessequals(c_0,c_Suc(c_1),tc_nat)
| ( X0 = c_0 ) ),
inference(superposition,[status(thm)],[c_8564,c_8623]) ).
tcf(c_8655,plain,
! [X0: $i] : c_lessequals(c_0,c_Suc(X0),tc_nat),
inference(superposition,[status(thm)],[c_8590,c_8623]) ).
tcf(c_8656,plain,
! [X0: $i,X1: $i] : c_minus(c_minus(X0,X1,tc_nat),c_Suc(X0),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_8623,c_2865]) ).
tcf(c_8660,plain,
! [X0: $i] : c_minus(X0,c_Suc(X0),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_8653,c_2865]) ).
tcf(c_8663,plain,
! [X0: $i] :
( c_less(c_0,c_0,tc_nat)
| ~ c_less(c_Suc(X0),X0,tc_nat) ),
inference(superposition,[status(thm)],[c_8660,c_2858]) ).
tcf(c_8666,plain,
! [X0: $i] :
( c_less(c_Suc(X0),X0,tc_nat)
| ~ c_less(c_0,c_0,tc_nat) ),
inference(superposition,[status(thm)],[c_8660,c_2859]) ).
tcf(c_8669,plain,
! [X0: $i] : ~ c_less(c_Suc(X0),X0,tc_nat),
inference(forward_subsumption_resolution,[status(thm)],[c_8663,c_2825]) ).
tcf(c_8678,plain,
! [X0: $i,X1: $i] : c_lessequals(c_minus(X0,X1,tc_nat),c_Suc(c_Suc(c_Suc(X0))),tc_nat),
inference(superposition,[status(thm)],[c_2869,c_8651]) ).
tcf(c_8680,plain,
! [X0: $i] : c_lessequals(X0,c_Suc(c_Suc(X0)),tc_nat),
inference(superposition,[status(thm)],[c_2860,c_8651]) ).
tcf(c_8681,plain,
! [X0: $i] :
( c_lessequals(c_0,c_Suc(c_Suc(c_1)),tc_nat)
| ( X0 = c_0 ) ),
inference(superposition,[status(thm)],[c_8564,c_8651]) ).
tcf(c_8682,plain,
! [X0: $i] : c_lessequals(c_0,c_Suc(c_Suc(X0)),tc_nat),
inference(superposition,[status(thm)],[c_8590,c_8651]) ).
tcf(c_8684,plain,
! [X0: $i,X1: $i] : c_minus(c_minus(X0,X1,tc_nat),c_Suc(c_Suc(X0)),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_8651,c_2865]) ).
tcf(c_8688,plain,
! [X0: $i] : c_minus(X0,c_Suc(c_Suc(X0)),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_8680,c_2865]) ).
tcf(c_8691,plain,
! [X0: $i] :
( c_less(c_0,c_0,tc_nat)
| ~ c_less(c_Suc(c_Suc(X0)),X0,tc_nat) ),
inference(superposition,[status(thm)],[c_8688,c_2858]) ).
tcf(c_8695,plain,
! [X0: $i] :
( c_less(c_Suc(c_Suc(X0)),X0,tc_nat)
| ~ c_less(c_0,c_0,tc_nat) ),
inference(superposition,[status(thm)],[c_8688,c_2859]) ).
tcf(c_8698,plain,
! [X0: $i] : ~ c_less(c_Suc(c_Suc(X0)),X0,tc_nat),
inference(forward_subsumption_resolution,[status(thm)],[c_8691,c_2825]) ).
tcf(c_8702,plain,
! [X0: $i,X1: $i] : c_lessequals(c_minus(X0,X1,tc_nat),c_Suc(c_Suc(c_Suc(c_Suc(X0)))),tc_nat),
inference(superposition,[status(thm)],[c_2869,c_8678]) ).
tcf(c_8704,plain,
! [X0: $i] : c_lessequals(X0,c_Suc(c_Suc(c_Suc(X0))),tc_nat),
inference(superposition,[status(thm)],[c_2860,c_8678]) ).
tcf(c_8705,plain,
! [X0: $i] :
( c_lessequals(c_0,c_Suc(c_Suc(c_Suc(c_1))),tc_nat)
| ( X0 = c_0 ) ),
inference(superposition,[status(thm)],[c_8564,c_8678]) ).
tcf(c_8706,plain,
! [X0: $i] : c_lessequals(c_0,c_Suc(c_Suc(c_Suc(X0))),tc_nat),
inference(superposition,[status(thm)],[c_8590,c_8678]) ).
tcf(c_8709,plain,
! [X0: $i,X1: $i] : c_minus(c_minus(X0,X1,tc_nat),c_Suc(c_Suc(c_Suc(X0))),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_8678,c_2865]) ).
tcf(c_8713,plain,
! [X0: $i] : c_minus(X0,c_Suc(c_Suc(c_Suc(X0))),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_8704,c_2865]) ).
tcf(c_8729,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ( c_Nat_Opower(c_0,X0,tc_nat) = c_0 ) ),
inference(superposition,[status(thm)],[c_2827,c_2905]) ).
tcf(c_8730,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ( c_minus(c_Nat_Opower(c_0,X0,tc_nat),c_0,tc_nat) = c_0 ) ),
inference(superposition,[status(thm)],[c_8552,c_2905]) ).
tcf(c_8750,plain,
! [X0: $i] :
( c_less(c_0,c_0,tc_nat)
| ~ c_less(c_Suc(c_Suc(c_Suc(X0))),X0,tc_nat) ),
inference(superposition,[status(thm)],[c_8713,c_2858]) ).
tcf(c_8755,plain,
! [X0: $i] :
( c_less(c_Suc(c_Suc(c_Suc(X0))),X0,tc_nat)
| ~ c_less(c_0,c_0,tc_nat) ),
inference(superposition,[status(thm)],[c_8713,c_2859]) ).
tcf(c_8758,plain,
! [X0: $i] : ~ c_less(c_Suc(c_Suc(c_Suc(X0))),X0,tc_nat),
inference(forward_subsumption_resolution,[status(thm)],[c_8750,c_2825]) ).
tcf(c_8761,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_plus(X1,c_Suc(X0),tc_nat),tc_nat) = c_0,
inference(demodulation,[status(thm)],[c_8656,c_2867]) ).
tcf(c_8762,plain,
! [X0: $i,X1: $i] :
( c_less(c_0,c_0,tc_nat)
| ~ c_less(c_plus(X0,c_Suc(X1),tc_nat),X1,tc_nat) ),
inference(superposition,[status(thm)],[c_8761,c_2858]) ).
tcf(c_8766,plain,
! [X0: $i,X1: $i] : c_lessequals(X0,c_plus(X1,c_Suc(X0),tc_nat),tc_nat),
inference(superposition,[status(thm)],[c_8761,c_2866]) ).
tcf(c_8767,plain,
! [X0: $i,X1: $i] :
( c_less(c_plus(X0,c_Suc(X1),tc_nat),X1,tc_nat)
| ~ c_less(c_0,c_0,tc_nat) ),
inference(superposition,[status(thm)],[c_8761,c_2859]) ).
tcf(c_8769,plain,
! [X0: $i,X1: $i] : ~ c_less(c_plus(X0,c_Suc(X1),tc_nat),X1,tc_nat),
inference(forward_subsumption_resolution,[status(thm)],[c_8762,c_2825]) ).
tcf(c_8775,plain,
! [X0: $i,X1: $i] : c_lessequals(c_minus(X0,X1,tc_nat),c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))),tc_nat),
inference(superposition,[status(thm)],[c_2869,c_8702]) ).
tcf(c_8777,plain,
! [X0: $i] : c_lessequals(X0,c_Suc(c_Suc(c_Suc(c_Suc(X0)))),tc_nat),
inference(superposition,[status(thm)],[c_2860,c_8702]) ).
tcf(c_8778,plain,
! [X0: $i] :
( c_lessequals(c_0,c_Suc(c_Suc(c_Suc(c_Suc(c_1)))),tc_nat)
| ( X0 = c_0 ) ),
inference(superposition,[status(thm)],[c_8564,c_8702]) ).
tcf(c_8779,plain,
! [X0: $i] : c_lessequals(c_0,c_Suc(c_Suc(c_Suc(c_Suc(X0)))),tc_nat),
inference(superposition,[status(thm)],[c_8590,c_8702]) ).
tcf(c_8784,plain,
! [X0: $i,X1: $i] : c_minus(c_minus(X0,X1,tc_nat),c_Suc(c_Suc(c_Suc(c_Suc(X0)))),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_8702,c_2865]) ).
tcf(c_8788,plain,
! [X0: $i] : c_minus(X0,c_Suc(c_Suc(c_Suc(c_Suc(X0)))),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_8777,c_2865]) ).
tcf(c_8796,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ~ c_less(c_0,c_0,tc_nat) ),
inference(superposition,[status(thm)],[c_8729,c_2905]) ).
tcf(c_8799,plain,
! [X0: $i] :
( c_less(c_0,c_0,tc_nat)
| ~ c_less(c_Suc(c_Suc(c_Suc(c_Suc(X0)))),X0,tc_nat) ),
inference(superposition,[status(thm)],[c_8788,c_2858]) ).
tcf(c_8805,plain,
! [X0: $i] :
( c_less(c_Suc(c_Suc(c_Suc(c_Suc(X0)))),X0,tc_nat)
| ~ c_less(c_0,c_0,tc_nat) ),
inference(superposition,[status(thm)],[c_8788,c_2859]) ).
tcf(c_8808,plain,
! [X0: $i] : ~ c_less(c_Suc(c_Suc(c_Suc(c_Suc(X0)))),X0,tc_nat),
inference(forward_subsumption_resolution,[status(thm)],[c_8799,c_2825]) ).
tcf(c_8813,plain,
! [X0: $i,X1: $i] : c_in(c_Pair(X0,X0,X1,X1),c_Relation_OId,tc_prod(X1,X1)),
inference(superposition,[status(thm)],[c_8518,c_2948]) ).
tcf(c_8824,plain,
c_Relation_Otrans(c_Tarski_Opotype_Oorder(v_cl,t_a,tc_Product__Type_Ounit),t_a),
inference(superposition,[status(thm)],[c_2797,c_2801]) ).
tcf(c_8825,plain,
c_Relation_Otrans(v_r,t_a),
inference(light_normalisation,[status(thm)],[c_8824,c_2798]) ).
tcf(c_8830,plain,
c_Relation_Oantisym(c_Tarski_Opotype_Oorder(v_cl,t_a,tc_Product__Type_Ounit),t_a),
inference(superposition,[status(thm)],[c_2797,c_2805]) ).
tcf(c_8831,plain,
c_Relation_Oantisym(v_r,t_a),
inference(light_normalisation,[status(thm)],[c_8830,c_2798]) ).
tcf(c_8844,plain,
! [X0: $i,X1: $i] :
( c_less(c_minus(X0,X1,tc_nat),c_Suc(X0),tc_nat)
| ~ c_less(c_0,c_Suc(X0),tc_nat) ),
inference(superposition,[status(thm)],[c_2869,c_2868]) ).
tcf(c_8851,plain,
! [X0: $i] :
( ( c_minus(c_1,c_Suc(X0),tc_nat) = c_0 )
| ~ c_less(c_0,c_1,tc_nat) ),
inference(superposition,[status(thm)],[c_2868,c_2899]) ).
tcf(c_8852,plain,
~ c_less(c_0,c_0,tc_nat),
inference(superposition,[status(thm)],[c_2868,c_2825]) ).
tcf(c_8853,plain,
! [X0: $i] : c_minus(c_1,c_Suc(X0),tc_nat) = c_0,
inference(forward_subsumption_resolution,[status(thm)],[c_8851,c_2898]) ).
tcf(c_8858,plain,
! [X0: $i] :
( c_less(c_0,c_0,tc_nat)
| ~ c_less(c_Suc(X0),c_1,tc_nat) ),
inference(superposition,[status(thm)],[c_8853,c_2858]) ).
tcf(c_8859,plain,
c_lessequals(c_0,c_Suc(c_Suc(c_Suc(c_Suc(c_1)))),tc_nat),
inference(superposition,[status(thm)],[c_8853,c_8702]) ).
tcf(c_8860,plain,
c_lessequals(c_0,c_Suc(c_Suc(c_Suc(c_1))),tc_nat),
inference(superposition,[status(thm)],[c_8853,c_8678]) ).
tcf(c_8861,plain,
c_lessequals(c_0,c_Suc(c_Suc(c_1)),tc_nat),
inference(superposition,[status(thm)],[c_8853,c_8651]) ).
tcf(c_8862,plain,
c_lessequals(c_0,c_Suc(c_1),tc_nat),
inference(superposition,[status(thm)],[c_8853,c_8623]) ).
tcf(c_8863,plain,
! [X0: $i] : c_lessequals(c_1,c_Suc(X0),tc_nat),
inference(superposition,[status(thm)],[c_8853,c_2866]) ).
tcf(c_8864,plain,
! [X0: $i] :
( c_less(c_Suc(X0),c_1,tc_nat)
| ~ c_less(c_0,c_0,tc_nat) ),
inference(superposition,[status(thm)],[c_8853,c_2859]) ).
tcf(c_8865,plain,
c_lessequals(c_0,c_1,tc_nat),
inference(superposition,[status(thm)],[c_8853,c_2864]) ).
tcf(c_8867,plain,
! [X0: $i] : ~ c_less(c_Suc(X0),c_1,tc_nat),
inference(forward_subsumption_resolution,[status(thm)],[c_8858,c_2825]) ).
tcf(c_8872,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_plus(X1,c_Suc(c_Suc(X0)),tc_nat),tc_nat) = c_0,
inference(demodulation,[status(thm)],[c_8684,c_2867]) ).
tcf(c_8873,plain,
! [X0: $i,X1: $i] :
( c_less(c_0,c_0,tc_nat)
| ~ c_less(c_plus(X0,c_Suc(c_Suc(X1)),tc_nat),X1,tc_nat) ),
inference(superposition,[status(thm)],[c_8872,c_2858]) ).
tcf(c_8878,plain,
! [X0: $i,X1: $i] : c_lessequals(X0,c_plus(X1,c_Suc(c_Suc(X0)),tc_nat),tc_nat),
inference(superposition,[status(thm)],[c_8872,c_2866]) ).
tcf(c_8879,plain,
! [X0: $i,X1: $i] :
( c_less(c_plus(X0,c_Suc(c_Suc(X1)),tc_nat),X1,tc_nat)
| ~ c_less(c_0,c_0,tc_nat) ),
inference(superposition,[status(thm)],[c_8872,c_2859]) ).
tcf(c_8881,plain,
! [X0: $i,X1: $i] : ~ c_less(c_plus(X0,c_Suc(c_Suc(X1)),tc_nat),X1,tc_nat),
inference(forward_subsumption_resolution,[status(thm)],[c_8873,c_2825]) ).
tcf(c_8887,plain,
! [X0: $i,X1: $i] : c_lessequals(c_minus(X0,X1,tc_nat),c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0)))))),tc_nat),
inference(superposition,[status(thm)],[c_2869,c_8775]) ).
tcf(c_8889,plain,
! [X0: $i] : c_lessequals(X0,c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))),tc_nat),
inference(superposition,[status(thm)],[c_2860,c_8775]) ).
tcf(c_8890,plain,
! [X0: $i] :
( c_lessequals(c_0,c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_1))))),tc_nat)
| ( X0 = c_0 ) ),
inference(superposition,[status(thm)],[c_8564,c_8775]) ).
tcf(c_8897,plain,
c_lessequals(c_0,c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_1))))),tc_nat),
inference(superposition,[status(thm)],[c_8853,c_8775]) ).
tcf(c_8898,plain,
! [X0: $i] : c_lessequals(c_0,c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))),tc_nat),
inference(superposition,[status(thm)],[c_8872,c_8775]) ).
tcf(c_8899,plain,
! [X0: $i,X1: $i] : c_minus(c_minus(X0,X1,tc_nat),c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_8775,c_2865]) ).
tcf(c_8903,plain,
! [X0: $i] : c_minus(X0,c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_8889,c_2865]) ).
tcf(c_8906,plain,
! [X0: $i] :
( c_less(c_0,c_0,tc_nat)
| ~ c_less(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))),X0,tc_nat) ),
inference(superposition,[status(thm)],[c_8903,c_2858]) ).
tcf(c_8913,plain,
! [X0: $i] :
( c_less(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))),X0,tc_nat)
| ~ c_less(c_0,c_0,tc_nat) ),
inference(superposition,[status(thm)],[c_8903,c_2859]) ).
tcf(c_8917,plain,
! [X0: $i] : ~ c_less(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))),X0,tc_nat),
inference(forward_subsumption_resolution,[status(thm)],[c_8906,c_2825]) ).
tcf(c_8929,plain,
! [X0: $i] :
( c_lessequals(c_Suc(c_0),c_0,tc_nat)
| ( X0 = c_0 )
| ~ c_lessequals(c_1,c_0,tc_nat) ),
inference(superposition,[status(thm)],[c_8729,c_2906]) ).
tcf(c_8930,plain,
! [X0: $i] :
( c_lessequals(c_Suc(c_0),c_1,tc_nat)
| ~ c_lessequals(c_1,X0,tc_nat) ),
inference(superposition,[status(thm)],[c_2902,c_2906]) ).
tcf(c_8931,plain,
! [X0: $i,X1: $i] :
( ( c_minus(c_Suc(c_0),c_Nat_Opower(X0,X1,tc_nat),tc_nat) = c_0 )
| ~ c_lessequals(c_1,X0,tc_nat) ),
inference(superposition,[status(thm)],[c_2906,c_2865]) ).
tcf(c_8958,plain,
c_lessequals(c_Suc(c_0),c_1,tc_nat),
inference(superposition,[status(thm)],[c_8488,c_8930]) ).
tcf(c_8968,plain,
c_minus(c_Suc(c_0),c_1,tc_nat) = c_0,
inference(superposition,[status(thm)],[c_8958,c_2865]) ).
tcf(c_8969,plain,
( c_less(c_0,c_0,tc_nat)
| ~ c_less(c_1,c_Suc(c_0),tc_nat) ),
inference(superposition,[status(thm)],[c_8968,c_2858]) ).
tcf(c_8970,plain,
c_lessequals(c_0,c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_0)))))),tc_nat),
inference(superposition,[status(thm)],[c_8968,c_8775]) ).
tcf(c_8971,plain,
c_lessequals(c_0,c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_0))))),tc_nat),
inference(superposition,[status(thm)],[c_8968,c_8702]) ).
tcf(c_8972,plain,
c_lessequals(c_0,c_Suc(c_Suc(c_Suc(c_Suc(c_0)))),tc_nat),
inference(superposition,[status(thm)],[c_8968,c_8678]) ).
tcf(c_8973,plain,
c_lessequals(c_0,c_Suc(c_Suc(c_Suc(c_0))),tc_nat),
inference(superposition,[status(thm)],[c_8968,c_8651]) ).
tcf(c_8974,plain,
c_lessequals(c_0,c_Suc(c_Suc(c_0)),tc_nat),
inference(superposition,[status(thm)],[c_8968,c_8623]) ).
tcf(c_8976,plain,
( c_less(c_1,c_Suc(c_0),tc_nat)
| ~ c_less(c_0,c_0,tc_nat) ),
inference(superposition,[status(thm)],[c_8968,c_2859]) ).
tcf(c_8977,plain,
c_lessequals(c_0,c_Suc(c_0),tc_nat),
inference(superposition,[status(thm)],[c_8968,c_2864]) ).
tcf(c_8978,plain,
~ c_less(c_1,c_Suc(c_0),tc_nat),
inference(forward_subsumption_resolution,[status(thm)],[c_8969,c_2825]) ).
tcf(c_8980,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_plus(X1,c_Suc(c_Suc(c_Suc(X0))),tc_nat),tc_nat) = c_0,
inference(demodulation,[status(thm)],[c_8709,c_2867]) ).
tcf(c_8981,plain,
! [X0: $i,X1: $i] :
( c_less(c_0,c_0,tc_nat)
| ~ c_less(c_plus(X0,c_Suc(c_Suc(c_Suc(X1))),tc_nat),X1,tc_nat) ),
inference(superposition,[status(thm)],[c_8980,c_2858]) ).
tcf(c_8987,plain,
! [X0: $i,X1: $i] : c_lessequals(X0,c_plus(X1,c_Suc(c_Suc(c_Suc(X0))),tc_nat),tc_nat),
inference(superposition,[status(thm)],[c_8980,c_2866]) ).
tcf(c_8988,plain,
! [X0: $i,X1: $i] :
( c_less(c_plus(X0,c_Suc(c_Suc(c_Suc(X1))),tc_nat),X1,tc_nat)
| ~ c_less(c_0,c_0,tc_nat) ),
inference(superposition,[status(thm)],[c_8980,c_2859]) ).
tcf(c_8990,plain,
! [X0: $i,X1: $i] : ~ c_less(c_plus(X0,c_Suc(c_Suc(c_Suc(X1))),tc_nat),X1,tc_nat),
inference(forward_subsumption_resolution,[status(thm)],[c_8981,c_2825]) ).
tcf(c_8996,plain,
! [X0: $i,X1: $i] : c_lessequals(c_minus(X0,X1,tc_nat),c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))))),tc_nat),
inference(superposition,[status(thm)],[c_2869,c_8887]) ).
tcf(c_8998,plain,
! [X0: $i] : c_lessequals(X0,c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0)))))),tc_nat),
inference(superposition,[status(thm)],[c_2860,c_8887]) ).
tcf(c_8999,plain,
! [X0: $i] :
( c_lessequals(c_0,c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_1)))))),tc_nat)
| ( X0 = c_0 ) ),
inference(superposition,[status(thm)],[c_8564,c_8887]) ).
tcf(c_9006,plain,
c_lessequals(c_0,c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_1)))))),tc_nat),
inference(superposition,[status(thm)],[c_8853,c_8887]) ).
tcf(c_9009,plain,
c_lessequals(c_0,c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_0))))))),tc_nat),
inference(superposition,[status(thm)],[c_8968,c_8887]) ).
tcf(c_9010,plain,
! [X0: $i] : c_lessequals(c_0,c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0)))))),tc_nat),
inference(superposition,[status(thm)],[c_8980,c_8887]) ).
tcf(c_9011,plain,
! [X0: $i,X1: $i] : c_minus(c_minus(X0,X1,tc_nat),c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0)))))),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_8887,c_2865]) ).
tcf(c_9015,plain,
! [X0: $i] : c_minus(X0,c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0)))))),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_8998,c_2865]) ).
tcf(c_9018,plain,
! [X0: $i] :
( c_less(c_0,c_0,tc_nat)
| ~ c_less(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0)))))),X0,tc_nat) ),
inference(superposition,[status(thm)],[c_9015,c_2858]) ).
tcf(c_9026,plain,
! [X0: $i] :
( c_less(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0)))))),X0,tc_nat)
| ~ c_less(c_0,c_0,tc_nat) ),
inference(superposition,[status(thm)],[c_9015,c_2859]) ).
tcf(c_9030,plain,
! [X0: $i] : ~ c_less(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0)))))),X0,tc_nat),
inference(forward_subsumption_resolution,[status(thm)],[c_9018,c_2825]) ).
tcf(c_9049,plain,
! [X0: $i,X1: $i] :
( c_lessequals(X0,c_emptyset,tc_set(X1))
| ( X0 != c_emptyset ) ),
inference(superposition,[status(thm)],[c_2835,c_2834]) ).
tcf(c_9058,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ c_in(X0,c_emptyset,X2)
| ~ c_in(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_2836,c_2855]) ).
tcf(c_9065,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ( c_Suc(c_minus(X0,c_Suc(c_0),tc_nat)) = X0 ) ),
inference(superposition,[status(thm)],[c_2827,c_2871]) ).
tcf(c_9066,plain,
! [X0: $i,X1: $i] :
( ( X0 = c_List_Olist_ONil )
| ( c_Suc(c_minus(c_Nat_Osize(X0,tc_List_Olist(X1)),c_Suc(c_0),tc_nat)) = c_Nat_Osize(X0,tc_List_Olist(X1)) ) ),
inference(superposition,[status(thm)],[c_2889,c_2871]) ).
tcf(c_9067,plain,
c_Suc(c_minus(c_1,c_Suc(c_0),tc_nat)) = c_1,
inference(superposition,[status(thm)],[c_2898,c_2871]) ).
tcf(c_9068,plain,
! [X0: $i] :
( ( c_minus(X0,c_0,tc_nat) = c_0 )
| ( c_Suc(c_minus(X0,c_Suc(c_0),tc_nat)) = X0 ) ),
inference(superposition,[status(thm)],[c_8552,c_2871]) ).
tcf(c_9069,plain,
! [X0: $i,X1: $i] :
( ( c_Suc(c_minus(c_minus(X1,X0,tc_nat),c_Suc(c_0),tc_nat)) = c_minus(X1,X0,tc_nat) )
| ~ c_less(X0,X1,tc_nat) ),
inference(superposition,[status(thm)],[c_2858,c_2871]) ).
tcf(c_9070,plain,
! [X0: $i,X1: $i] :
( ( X0 = c_0 )
| ( c_Suc(c_minus(c_Nat_Opower(X0,X1,tc_nat),c_Suc(c_0),tc_nat)) = c_Nat_Opower(X0,X1,tc_nat) ) ),
inference(superposition,[status(thm)],[c_2904,c_2871]) ).
tcf(c_9083,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ( c_Nat_Opower(c_0,c_Suc(X0),tc_nat) = c_times(c_0,c_0,tc_nat) ) ),
inference(superposition,[status(thm)],[c_8729,c_2901]) ).
tcf(c_9084,plain,
! [X0: $i] : c_Nat_Opower(X0,c_Suc(c_0),tc_nat) = c_times(X0,c_1,tc_nat),
inference(superposition,[status(thm)],[c_2902,c_2901]) ).
tcf(c_9089,plain,
c_Suc(c_0) = c_1,
inference(demodulation,[status(thm)],[c_9067,c_8853]) ).
tcf(c_9090,plain,
! [X0: $i] :
( ( c_Suc(c_minus(X0,c_1,tc_nat)) = X0 )
| ~ c_less(c_0,X0,tc_nat) ),
inference(demodulation,[status(thm)],[c_2871,c_9089]) ).
tcf(c_9091,plain,
~ c_less(c_1,c_1,tc_nat),
inference(demodulation,[status(thm)],[c_8978,c_9089]) ).
tcf(c_9092,plain,
c_minus(c_1,c_1,tc_nat) = c_0,
inference(demodulation,[status(thm)],[c_8968,c_9089]) ).
tcf(c_9093,plain,
c_lessequals(c_1,c_1,tc_nat),
inference(demodulation,[status(thm)],[c_8958,c_9089]) ).
tcf(c_9094,plain,
! [X0: $i,X1: $i] :
( c_lessequals(c_1,c_Nat_Opower(X0,X1,tc_nat),tc_nat)
| ~ c_lessequals(c_1,X0,tc_nat) ),
inference(demodulation,[status(thm)],[c_2906,c_9089]) ).
tcf(c_9101,plain,
~ c_less(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_1))))),c_0,tc_nat),
inference(superposition,[status(thm)],[c_9089,c_9030]) ).
tcf(c_9102,plain,
c_minus(c_0,c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_1))))),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_9089,c_9015]) ).
tcf(c_9104,plain,
! [X0: $i] : c_lessequals(c_minus(c_0,X0,tc_nat),c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_1))))),tc_nat),
inference(superposition,[status(thm)],[c_9089,c_8887]) ).
tcf(c_9105,plain,
! [X0: $i] : c_lessequals(c_0,c_plus(X0,c_Suc(c_Suc(c_1)),tc_nat),tc_nat),
inference(superposition,[status(thm)],[c_9089,c_8987]) ).
tcf(c_9106,plain,
! [X0: $i] : c_minus(c_0,c_plus(X0,c_Suc(c_Suc(c_1)),tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_9089,c_8980]) ).
tcf(c_9107,plain,
~ c_less(c_Suc(c_Suc(c_Suc(c_Suc(c_1)))),c_0,tc_nat),
inference(superposition,[status(thm)],[c_9089,c_8917]) ).
tcf(c_9108,plain,
c_minus(c_0,c_Suc(c_Suc(c_Suc(c_Suc(c_1)))),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_9089,c_8903]) ).
tcf(c_9110,plain,
! [X0: $i] : c_lessequals(c_minus(c_0,X0,tc_nat),c_Suc(c_Suc(c_Suc(c_Suc(c_1)))),tc_nat),
inference(superposition,[status(thm)],[c_9089,c_8775]) ).
tcf(c_9111,plain,
! [X0: $i] : c_lessequals(c_0,c_plus(X0,c_Suc(c_1),tc_nat),tc_nat),
inference(superposition,[status(thm)],[c_9089,c_8878]) ).
tcf(c_9112,plain,
! [X0: $i] : c_minus(c_0,c_plus(X0,c_Suc(c_1),tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_9089,c_8872]) ).
tcf(c_9116,plain,
~ c_less(c_Suc(c_Suc(c_Suc(c_1))),c_0,tc_nat),
inference(superposition,[status(thm)],[c_9089,c_8808]) ).
tcf(c_9117,plain,
c_minus(c_0,c_Suc(c_Suc(c_Suc(c_1))),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_9089,c_8788]) ).
tcf(c_9119,plain,
! [X0: $i] : c_lessequals(c_minus(c_0,X0,tc_nat),c_Suc(c_Suc(c_Suc(c_1))),tc_nat),
inference(superposition,[status(thm)],[c_9089,c_8702]) ).
tcf(c_9120,plain,
! [X0: $i] : c_lessequals(c_0,c_plus(X0,c_1,tc_nat),tc_nat),
inference(superposition,[status(thm)],[c_9089,c_8766]) ).
tcf(c_9121,plain,
! [X0: $i] : c_minus(c_0,c_plus(X0,c_1,tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_9089,c_8761]) ).
tcf(c_9122,plain,
~ c_less(c_Suc(c_Suc(c_1)),c_0,tc_nat),
inference(superposition,[status(thm)],[c_9089,c_8758]) ).
tcf(c_9123,plain,
c_minus(c_0,c_Suc(c_Suc(c_1)),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_9089,c_8713]) ).
tcf(c_9125,plain,
! [X0: $i] : c_lessequals(c_minus(c_0,X0,tc_nat),c_Suc(c_Suc(c_1)),tc_nat),
inference(superposition,[status(thm)],[c_9089,c_8678]) ).
tcf(c_9126,plain,
~ c_less(c_Suc(c_1),c_0,tc_nat),
inference(superposition,[status(thm)],[c_9089,c_8698]) ).
tcf(c_9127,plain,
c_minus(c_0,c_Suc(c_1),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_9089,c_8688]) ).
tcf(c_9129,plain,
! [X0: $i] : c_lessequals(c_minus(c_0,X0,tc_nat),c_Suc(c_1),tc_nat),
inference(superposition,[status(thm)],[c_9089,c_8651]) ).
tcf(c_9130,plain,
~ c_less(c_1,c_0,tc_nat),
inference(superposition,[status(thm)],[c_9089,c_8669]) ).
tcf(c_9131,plain,
c_minus(c_0,c_1,tc_nat) = c_0,
inference(superposition,[status(thm)],[c_9089,c_8660]) ).
tcf(c_9133,plain,
! [X0: $i] : c_lessequals(c_minus(c_0,X0,tc_nat),c_1,tc_nat),
inference(superposition,[status(thm)],[c_9089,c_8623]) ).
tcf(c_9134,plain,
! [X0: $i] : c_minus(c_1,c_Suc(X0),tc_nat) = c_minus(c_0,X0,tc_nat),
inference(superposition,[status(thm)],[c_9089,c_2869]) ).
tcf(c_9135,plain,
! [X0: $i] : ~ c_less(c_plus(X0,c_Suc(c_Suc(c_1)),tc_nat),c_0,tc_nat),
inference(superposition,[status(thm)],[c_9089,c_8990]) ).
tcf(c_9136,plain,
! [X0: $i] : ~ c_less(c_plus(X0,c_Suc(c_1),tc_nat),c_0,tc_nat),
inference(superposition,[status(thm)],[c_9089,c_8881]) ).
tcf(c_9137,plain,
! [X0: $i] :
( c_less(c_minus(X0,c_1,tc_nat),X0,tc_nat)
| ~ c_less(c_0,X0,tc_nat) ),
inference(superposition,[status(thm)],[c_9089,c_2868]) ).
tcf(c_9138,plain,
! [X0: $i] : ~ c_less(c_plus(X0,c_1,tc_nat),c_0,tc_nat),
inference(superposition,[status(thm)],[c_9089,c_8769]) ).
tcf(c_9139,plain,
! [X0: $i] : c_minus(c_Suc(X0),c_1,tc_nat) = c_minus(X0,c_0,tc_nat),
inference(superposition,[status(thm)],[c_9089,c_2869]) ).
tcf(c_9144,plain,
! [X0: $i] : c_minus(c_Suc(X0),c_1,tc_nat) = X0,
inference(light_normalisation,[status(thm)],[c_9139,c_2860]) ).
tcf(c_9153,plain,
! [X0: $i] :
( c_less(c_0,X0,tc_nat)
| ~ c_less(c_1,c_Suc(X0),tc_nat) ),
inference(superposition,[status(thm)],[c_9144,c_2858]) ).
tcf(c_9154,plain,
! [X0: $i] : c_lessequals(X0,c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))))),tc_nat),
inference(superposition,[status(thm)],[c_9144,c_8887]) ).
tcf(c_9160,plain,
! [X0: $i] :
( c_lessequals(c_Suc(X0),c_1,tc_nat)
| ( X0 != c_0 ) ),
inference(superposition,[status(thm)],[c_9144,c_2866]) ).
tcf(c_9161,plain,
! [X0: $i] :
( c_less(c_1,c_Suc(X0),tc_nat)
| ~ c_less(c_0,X0,tc_nat) ),
inference(superposition,[status(thm)],[c_9144,c_2859]) ).
tcf(c_9177,plain,
! [X0: $i] : c_lessequals(c_emptyset,c_emptyset,tc_set(X0)),
inference(equality_resolution,[status(thm)],[c_9049]) ).
tcf(c_9182,plain,
! [X0: $i] :
( c_less(c_0,X0,tc_nat)
| ( c_minus(c_Suc(X0),c_1,tc_nat) = c_0 ) ),
inference(superposition,[status(thm)],[c_8552,c_9153]) ).
tcf(c_9183,plain,
( c_less(c_0,c_0,tc_nat)
| ~ c_less(c_1,c_1,tc_nat) ),
inference(superposition,[status(thm)],[c_9089,c_9153]) ).
tcf(c_9194,plain,
( c_less(c_1,c_1,tc_nat)
| ~ c_less(c_0,c_0,tc_nat) ),
inference(superposition,[status(thm)],[c_9089,c_9161]) ).
tcf(c_9196,plain,
! [X0: $i] : c_times(X0,c_1,tc_nat) = c_Nat_Opower(X0,c_1,tc_nat),
inference(light_normalisation,[status(thm)],[c_9084,c_9089]) ).
tcf(c_9198,plain,
! [X0: $i] : c_times(X0,c_times(X0,c_1,tc_nat),tc_nat) = c_Nat_Opower(X0,c_Suc(c_1),tc_nat),
inference(superposition,[status(thm)],[c_9196,c_2901]) ).
tcf(c_9199,plain,
! [X0: $i] :
( c_less(c_0,c_times(X0,c_1,tc_nat),tc_nat)
| ( X0 = c_0 ) ),
inference(superposition,[status(thm)],[c_9196,c_2904]) ).
tcf(c_9200,plain,
( ( c_0 = c_1 )
| ( c_times(c_0,c_1,tc_nat) = c_0 ) ),
inference(superposition,[status(thm)],[c_9196,c_8729]) ).
tcf(c_9201,plain,
( ( c_0 = c_1 )
| ~ c_less(c_0,c_times(c_0,c_1,tc_nat),tc_nat) ),
inference(superposition,[status(thm)],[c_9196,c_2905]) ).
tcf(c_9202,plain,
c_times(c_0,c_1,tc_nat) = c_0,
inference(forward_subsumption_resolution,[status(thm)],[c_9200,c_2900]) ).
tcf(c_9205,plain,
~ c_less(c_0,c_times(c_0,c_1,tc_nat),tc_nat),
inference(forward_subsumption_resolution,[status(thm)],[c_9201,c_2900]) ).
tcf(c_9210,plain,
! [X0: $i] : c_minus(X0,c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))))),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_9154,c_2865]) ).
tcf(c_9222,plain,
! [X0: $i] :
( c_lessequals(c_1,c_1,tc_nat)
| ~ c_lessequals(c_1,X0,tc_nat) ),
inference(superposition,[status(thm)],[c_2902,c_9094]) ).
tcf(c_9223,plain,
! [X0: $i] :
( c_lessequals(c_1,c_times(X0,c_1,tc_nat),tc_nat)
| ~ c_lessequals(c_1,X0,tc_nat) ),
inference(superposition,[status(thm)],[c_9196,c_9094]) ).
tcf(c_9224,plain,
! [X0: $i,X1: $i] :
( ( c_minus(c_1,c_Nat_Opower(X0,X1,tc_nat),tc_nat) = c_0 )
| ~ c_lessequals(c_1,X0,tc_nat) ),
inference(superposition,[status(thm)],[c_9094,c_2865]) ).
tcf(c_9231,plain,
! [X0: $i,X1: $i] : c_insert(X0,c_insert(X0,c_emptyset,X1),X1) = c_insert(X0,c_emptyset,X1),
inference(superposition,[status(thm)],[c_2836,c_2851]) ).
tcf(c_9232,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c_in(X0,c_insert(X2,X1,X3),X3)
| ~ c_in(X0,c_minus(X1,c_insert(X2,c_emptyset,X3),tc_set(X3)),X3) ),
inference(superposition,[status(thm)],[c_2851,c_2940]) ).
tcf(c_9244,plain,
! [X0: $i] :
( ( c_Numeral_Onumber__of(X0,tc_nat) = c_0 )
| ~ c_less(c_0,c_0,tc_nat) ),
inference(superposition,[status(thm)],[c_2907,c_2905]) ).
tcf(c_9245,plain,
! [X0: $i] : c_Nat_Opower(X0,c_Suc(c_0),tc_IntDef_Oint) = c_times(X0,c_1,tc_IntDef_Oint),
inference(superposition,[status(thm)],[c_2917,c_2916]) ).
tcf(c_9246,plain,
! [X0: $i] : c_times(X0,c_1,tc_IntDef_Oint) = c_Nat_Opower(X0,c_1,tc_IntDef_Oint),
inference(light_normalisation,[status(thm)],[c_9245,c_9089]) ).
tcf(c_9252,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_in(c_insert(X1,X0,X2),c_Finite__Set_OFinites,tc_set(X2))
| ~ c_in(c_minus(X0,c_insert(X1,c_emptyset,X2),tc_set(X2)),c_Finite__Set_OFinites,tc_set(X2)) ),
inference(superposition,[status(thm)],[c_2851,c_2929]) ).
tcf(c_9261,plain,
! [X0: $i,X1: $i,X2: $i] : c_lessequals(X0,c_insert(X1,X0,X2),tc_set(X2)),
inference(superposition,[status(thm)],[c_2809,c_2937]) ).
tcf(c_9262,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c_lessequals(c_minus(X1,c_insert(X0,c_emptyset,X2),tc_set(X2)),X3,tc_set(X2))
| ~ c_lessequals(c_insert(X0,X1,X2),X3,tc_set(X2)) ),
inference(superposition,[status(thm)],[c_2851,c_2937]) ).
tcf(c_9268,plain,
! [X0: $i,X1: $i,X2: $i] : c_lessequals(c_minus(X0,c_insert(X1,c_emptyset,X2),tc_set(X2)),c_insert(X1,X0,X2),tc_set(X2)),
inference(superposition,[status(thm)],[c_2851,c_9261]) ).
tcf(c_9269,plain,
! [X0: $i,X1: $i,X2: $i] : c_lessequals(c_insert(X0,X1,X2),c_insert(X0,X1,X2),tc_set(X2)),
inference(superposition,[status(thm)],[c_2943,c_9261]) ).
tcf(c_9270,plain,
! [X0: $i,X1: $i,X2: $i] : c_minus(X0,c_insert(X1,X0,X2),tc_set(X2)) = c_emptyset,
inference(superposition,[status(thm)],[c_9261,c_2833]) ).
tcf(c_9271,plain,
! [X0: $i,X1: $i,X2: $i] : ~ c_less(c_insert(X0,X1,X2),X1,tc_set(X2)),
inference(superposition,[status(thm)],[c_9261,c_2813]) ).
tcf(c_9272,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : c_lessequals(X0,c_insert(X1,c_insert(X2,X0,X3),X3),tc_set(X3)),
inference(superposition,[status(thm)],[c_9261,c_2937]) ).
tcf(c_9273,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : c_in(X0,c_insert(X1,c_insert(X0,X2,X3),X3),X3),
inference(superposition,[status(thm)],[c_9261,c_2938]) ).
tcf(c_9279,plain,
! [X0: $i,X1: $i,X2: $i] : ~ c_less(c_insert(X0,X1,X2),c_minus(X1,c_insert(X0,c_emptyset,X2),tc_set(X2)),tc_set(X2)),
inference(superposition,[status(thm)],[c_2851,c_9271]) ).
tcf(c_9280,plain,
! [X0: $i,X1: $i,X2: $i] : ~ c_less(c_insert(X0,X1,X2),c_insert(X0,X1,X2),tc_set(X2)),
inference(superposition,[status(thm)],[c_2943,c_9271]) ).
tcf(c_9282,plain,
! [X0: $i] : c_times(X0,c_times(X0,c_1,tc_IntDef_Oint),tc_IntDef_Oint) = c_Nat_Opower(X0,c_Suc(c_1),tc_IntDef_Oint),
inference(superposition,[status(thm)],[c_9246,c_2916]) ).
tcf(c_9287,plain,
! [X0: $i,X1: $i,X2: $i] : c_minus(c_minus(X0,c_insert(X1,c_emptyset,X2),tc_set(X2)),c_insert(X1,X0,X2),tc_set(X2)) = c_emptyset,
inference(superposition,[status(thm)],[c_2851,c_9270]) ).
tcf(c_9288,plain,
! [X0: $i,X1: $i,X2: $i] : c_minus(c_insert(X0,X1,X2),c_insert(X0,X1,X2),tc_set(X2)) = c_emptyset,
inference(superposition,[status(thm)],[c_2943,c_9270]) ).
tcf(c_9290,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ c_in(X0,c_emptyset,X3)
| ~ c_in(X0,c_insert(X1,X2,X3),X3) ),
inference(superposition,[status(thm)],[c_9270,c_2855]) ).
tcf(c_9294,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : c_lessequals(c_minus(X0,c_insert(X1,c_emptyset,X2),tc_set(X2)),c_insert(X3,c_insert(X1,X0,X2),X2),tc_set(X2)),
inference(superposition,[status(thm)],[c_2851,c_9272]) ).
tcf(c_9295,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : c_lessequals(c_insert(X0,X1,X2),c_insert(X3,c_insert(X0,X1,X2),X2),tc_set(X2)),
inference(superposition,[status(thm)],[c_2943,c_9272]) ).
tcf(c_9296,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : c_minus(X0,c_insert(X1,c_insert(X2,X0,X3),X3),tc_set(X3)) = c_emptyset,
inference(superposition,[status(thm)],[c_9272,c_2833]) ).
tcf(c_9297,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : ~ c_less(c_insert(X0,c_insert(X1,X2,X3),X3),X2,tc_set(X3)),
inference(superposition,[status(thm)],[c_9272,c_2813]) ).
tcf(c_9298,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : c_lessequals(X0,c_insert(X1,c_insert(X2,c_insert(X3,X0,X4),X4),X4),tc_set(X4)),
inference(superposition,[status(thm)],[c_9272,c_2937]) ).
tcf(c_9299,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : c_in(X0,c_insert(X1,c_insert(X2,c_insert(X0,X3,X4),X4),X4),X4),
inference(superposition,[status(thm)],[c_9272,c_2938]) ).
tcf(c_9312,plain,
! [X0: $i] :
( c_less(X0,c_Suc(X0),tc_nat)
| ~ c_less(c_0,c_Suc(X0),tc_nat) ),
inference(superposition,[status(thm)],[c_9144,c_9137]) ).
tcf(c_9313,plain,
( ( c_minus(c_1,c_1,tc_nat) = c_0 )
| ~ c_less(c_0,c_1,tc_nat) ),
inference(superposition,[status(thm)],[c_9137,c_2899]) ).
tcf(c_9322,plain,
! [X0: $i] :
( c_less(X0,c_Suc(X0),tc_nat)
| ( c_Suc(X0) = c_0 ) ),
inference(superposition,[status(thm)],[c_2827,c_9312]) ).
tcf(c_9323,plain,
! [X0: $i] :
( c_less(X0,c_Suc(X0),tc_nat)
| ( c_minus(c_Suc(X0),c_0,tc_nat) = c_0 ) ),
inference(superposition,[status(thm)],[c_8552,c_9312]) ).
tcf(c_9324,plain,
( c_less(c_0,c_Suc(c_0),tc_nat)
| ~ c_less(c_0,c_1,tc_nat) ),
inference(superposition,[status(thm)],[c_9089,c_9312]) ).
tcf(c_9337,plain,
( c_less(c_0,c_Suc(c_0),tc_nat)
| ( c_Suc(c_0) = c_0 ) ),
inference(superposition,[status(thm)],[c_9322,c_9312]) ).
tcf(c_9339,plain,
( c_less(c_0,c_1,tc_nat)
| ( c_0 = c_1 ) ),
inference(light_normalisation,[status(thm)],[c_9337,c_9089]) ).
tcf(c_9345,plain,
! [X0: $i] :
( ( c_minus(c_1,c_times(X0,c_1,tc_nat),tc_nat) = c_0 )
| ~ c_lessequals(c_1,X0,tc_nat) ),
inference(superposition,[status(thm)],[c_9223,c_2865]) ).
tcf(c_9350,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : ~ c_less(c_insert(X0,c_insert(X1,X2,X3),X3),c_minus(X2,c_insert(X1,c_emptyset,X3),tc_set(X3)),tc_set(X3)),
inference(superposition,[status(thm)],[c_2851,c_9297]) ).
tcf(c_9351,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : ~ c_less(c_insert(X0,c_insert(X1,X2,X3),X3),c_insert(X1,X2,X3),tc_set(X3)),
inference(superposition,[status(thm)],[c_2943,c_9297]) ).
tcf(c_9353,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ( c_Suc(c_minus(X0,c_1,tc_nat)) = X0 ) ),
inference(light_normalisation,[status(thm)],[c_9065,c_9089]) ).
tcf(c_9363,plain,
! [X0: $i] :
( c_less(c_minus(X0,c_1,tc_nat),X0,tc_nat)
| ( X0 = c_0 )
| ( c_Suc(c_minus(X0,c_1,tc_nat)) = c_0 ) ),
inference(superposition,[status(thm)],[c_9353,c_9322]) ).
tcf(c_9364,plain,
! [X0: $i] :
( c_less(c_minus(X0,c_1,tc_nat),c_Suc(c_minus(X0,c_1,tc_nat)),tc_nat)
| ( X0 = c_0 )
| ~ c_less(c_0,X0,tc_nat) ),
inference(superposition,[status(thm)],[c_9353,c_9312]) ).
tcf(c_9365,plain,
! [X0: $i] :
( c_lessequals(c_minus(X0,c_1,tc_nat),c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0)))))),tc_nat)
| ( X0 = c_0 ) ),
inference(superposition,[status(thm)],[c_9353,c_9154]) ).
tcf(c_9366,plain,
! [X0: $i] :
( c_less(c_1,X0,tc_nat)
| ( X0 = c_0 )
| ~ c_less(c_0,c_minus(X0,c_1,tc_nat),tc_nat) ),
inference(superposition,[status(thm)],[c_9353,c_9161]) ).
tcf(c_9367,plain,
! [X0: $i] :
( c_less(c_0,c_minus(X0,c_1,tc_nat),tc_nat)
| ( X0 = c_0 )
| ~ c_less(c_1,X0,tc_nat) ),
inference(superposition,[status(thm)],[c_9353,c_9153]) ).
tcf(c_9368,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ~ c_less(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))),c_minus(X0,c_1,tc_nat),tc_nat) ),
inference(superposition,[status(thm)],[c_9353,c_9030]) ).
tcf(c_9369,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ( c_minus(c_minus(X0,c_1,tc_nat),c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))),tc_nat) = c_0 ) ),
inference(superposition,[status(thm)],[c_9353,c_9015]) ).
tcf(c_9370,plain,
! [X0: $i] :
( c_lessequals(c_minus(X0,c_1,tc_nat),c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))),tc_nat)
| ( X0 = c_0 ) ),
inference(superposition,[status(thm)],[c_9353,c_8998]) ).
tcf(c_9371,plain,
! [X0: $i,X1: $i] :
( c_lessequals(c_minus(c_minus(X0,c_1,tc_nat),X1,tc_nat),c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))),tc_nat)
| ( X0 = c_0 ) ),
inference(superposition,[status(thm)],[c_9353,c_8887]) ).
tcf(c_9372,plain,
! [X0: $i,X1: $i] :
( c_lessequals(c_minus(X0,c_1,tc_nat),c_plus(X1,c_Suc(c_Suc(X0)),tc_nat),tc_nat)
| ( X0 = c_0 ) ),
inference(superposition,[status(thm)],[c_9353,c_8987]) ).
tcf(c_9373,plain,
! [X0: $i,X1: $i] :
( ( X0 = c_0 )
| ( c_minus(c_minus(X0,c_1,tc_nat),c_plus(X1,c_Suc(c_Suc(X0)),tc_nat),tc_nat) = c_0 ) ),
inference(superposition,[status(thm)],[c_9353,c_8980]) ).
tcf(c_9374,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ~ c_less(c_Suc(c_Suc(c_Suc(c_Suc(X0)))),c_minus(X0,c_1,tc_nat),tc_nat) ),
inference(superposition,[status(thm)],[c_9353,c_8917]) ).
tcf(c_9375,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ( c_minus(c_minus(X0,c_1,tc_nat),c_Suc(c_Suc(c_Suc(c_Suc(X0)))),tc_nat) = c_0 ) ),
inference(superposition,[status(thm)],[c_9353,c_8903]) ).
tcf(c_9376,plain,
! [X0: $i] :
( c_lessequals(c_minus(X0,c_1,tc_nat),c_Suc(c_Suc(c_Suc(c_Suc(X0)))),tc_nat)
| ( X0 = c_0 ) ),
inference(superposition,[status(thm)],[c_9353,c_8889]) ).
tcf(c_9377,plain,
! [X0: $i,X1: $i] :
( c_lessequals(c_minus(c_minus(X0,c_1,tc_nat),X1,tc_nat),c_Suc(c_Suc(c_Suc(c_Suc(X0)))),tc_nat)
| ( X0 = c_0 ) ),
inference(superposition,[status(thm)],[c_9353,c_8775]) ).
tcf(c_9378,plain,
! [X0: $i,X1: $i] :
( c_lessequals(c_minus(X0,c_1,tc_nat),c_plus(X1,c_Suc(X0),tc_nat),tc_nat)
| ( X0 = c_0 ) ),
inference(superposition,[status(thm)],[c_9353,c_8878]) ).
tcf(c_9379,plain,
! [X0: $i,X1: $i] :
( ( X0 = c_0 )
| ( c_minus(c_minus(X0,c_1,tc_nat),c_plus(X1,c_Suc(X0),tc_nat),tc_nat) = c_0 ) ),
inference(superposition,[status(thm)],[c_9353,c_8872]) ).
tcf(c_9383,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ~ c_less(c_Suc(c_Suc(c_Suc(X0))),c_minus(X0,c_1,tc_nat),tc_nat) ),
inference(superposition,[status(thm)],[c_9353,c_8808]) ).
tcf(c_9384,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ( c_minus(c_minus(X0,c_1,tc_nat),c_Suc(c_Suc(c_Suc(X0))),tc_nat) = c_0 ) ),
inference(superposition,[status(thm)],[c_9353,c_8788]) ).
tcf(c_9385,plain,
! [X0: $i] :
( c_lessequals(c_minus(X0,c_1,tc_nat),c_Suc(c_Suc(c_Suc(X0))),tc_nat)
| ( X0 = c_0 ) ),
inference(superposition,[status(thm)],[c_9353,c_8777]) ).
tcf(c_9386,plain,
! [X0: $i,X1: $i] :
( c_lessequals(c_minus(c_minus(X0,c_1,tc_nat),X1,tc_nat),c_Suc(c_Suc(c_Suc(X0))),tc_nat)
| ( X0 = c_0 ) ),
inference(superposition,[status(thm)],[c_9353,c_8702]) ).
tcf(c_9387,plain,
! [X0: $i,X1: $i] :
( c_lessequals(c_minus(X0,c_1,tc_nat),c_plus(X1,X0,tc_nat),tc_nat)
| ( X0 = c_0 ) ),
inference(superposition,[status(thm)],[c_9353,c_8766]) ).
tcf(c_9388,plain,
! [X0: $i,X1: $i] :
( ( X0 = c_0 )
| ( c_minus(c_minus(X0,c_1,tc_nat),c_plus(X1,X0,tc_nat),tc_nat) = c_0 ) ),
inference(superposition,[status(thm)],[c_9353,c_8761]) ).
tcf(c_9389,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ~ c_less(c_Suc(c_Suc(X0)),c_minus(X0,c_1,tc_nat),tc_nat) ),
inference(superposition,[status(thm)],[c_9353,c_8758]) ).
tcf(c_9390,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ( c_minus(c_minus(X0,c_1,tc_nat),c_Suc(c_Suc(X0)),tc_nat) = c_0 ) ),
inference(superposition,[status(thm)],[c_9353,c_8713]) ).
tcf(c_9391,plain,
! [X0: $i] :
( c_lessequals(c_minus(X0,c_1,tc_nat),c_Suc(c_Suc(X0)),tc_nat)
| ( X0 = c_0 ) ),
inference(superposition,[status(thm)],[c_9353,c_8704]) ).
tcf(c_9392,plain,
! [X0: $i,X1: $i] :
( c_lessequals(c_minus(c_minus(X0,c_1,tc_nat),X1,tc_nat),c_Suc(c_Suc(X0)),tc_nat)
| ( X0 = c_0 ) ),
inference(superposition,[status(thm)],[c_9353,c_8678]) ).
tcf(c_9393,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ~ c_less(c_Suc(X0),c_minus(X0,c_1,tc_nat),tc_nat) ),
inference(superposition,[status(thm)],[c_9353,c_8698]) ).
tcf(c_9394,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ( c_minus(c_minus(X0,c_1,tc_nat),c_Suc(X0),tc_nat) = c_0 ) ),
inference(superposition,[status(thm)],[c_9353,c_8688]) ).
tcf(c_9395,plain,
! [X0: $i] :
( c_lessequals(c_minus(X0,c_1,tc_nat),c_Suc(X0),tc_nat)
| ( X0 = c_0 ) ),
inference(superposition,[status(thm)],[c_9353,c_8680]) ).
tcf(c_9396,plain,
! [X0: $i,X1: $i] :
( c_lessequals(c_minus(c_minus(X0,c_1,tc_nat),X1,tc_nat),c_Suc(X0),tc_nat)
| ( X0 = c_0 ) ),
inference(superposition,[status(thm)],[c_9353,c_8651]) ).
tcf(c_9397,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ~ c_less(X0,c_minus(X0,c_1,tc_nat),tc_nat) ),
inference(superposition,[status(thm)],[c_9353,c_8669]) ).
tcf(c_9398,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ( c_minus(c_minus(X0,c_1,tc_nat),X0,tc_nat) = c_0 ) ),
inference(superposition,[status(thm)],[c_9353,c_8660]) ).
tcf(c_9399,plain,
! [X0: $i] :
( c_lessequals(c_minus(X0,c_1,tc_nat),X0,tc_nat)
| ( X0 = c_0 ) ),
inference(superposition,[status(thm)],[c_9353,c_8653]) ).
tcf(c_9400,plain,
! [X0: $i,X1: $i] :
( c_lessequals(c_minus(c_minus(X0,c_1,tc_nat),X1,tc_nat),X0,tc_nat)
| ( X0 = c_0 ) ),
inference(superposition,[status(thm)],[c_9353,c_8623]) ).
tcf(c_9401,plain,
! [X0: $i,X1: $i] :
( ( X0 = c_0 )
| ( c_minus(c_minus(X0,c_1,tc_nat),X1,tc_nat) = c_minus(X0,c_Suc(X1),tc_nat) ) ),
inference(superposition,[status(thm)],[c_9353,c_2869]) ).
tcf(c_9402,plain,
! [X0: $i,X1: $i] :
( ( X1 = c_0 )
| ~ c_less(c_plus(X0,c_Suc(c_Suc(X1)),tc_nat),c_minus(X1,c_1,tc_nat),tc_nat) ),
inference(superposition,[status(thm)],[c_9353,c_8990]) ).
tcf(c_9403,plain,
! [X0: $i,X1: $i] :
( ( X1 = c_0 )
| ~ c_less(c_plus(X0,c_Suc(X1),tc_nat),c_minus(X1,c_1,tc_nat),tc_nat) ),
inference(superposition,[status(thm)],[c_9353,c_8881]) ).
tcf(c_9404,plain,
! [X0: $i,X1: $i] :
( c_less(c_minus(X0,X1,tc_nat),X0,tc_nat)
| ( X1 = c_0 )
| ~ c_less(c_0,X0,tc_nat) ),
inference(superposition,[status(thm)],[c_9353,c_2868]) ).
tcf(c_9405,plain,
! [X0: $i,X1: $i] :
( ( X1 = c_0 )
| ~ c_less(c_plus(X0,X1,tc_nat),c_minus(X1,c_1,tc_nat),tc_nat) ),
inference(superposition,[status(thm)],[c_9353,c_8769]) ).
tcf(c_9406,plain,
! [X0: $i,X1: $i] :
( ( X1 = c_0 )
| ( c_minus(X0,c_minus(X1,c_1,tc_nat),tc_nat) = c_minus(c_Suc(X0),X1,tc_nat) ) ),
inference(superposition,[status(thm)],[c_9353,c_2869]) ).
tcf(c_9514,plain,
! [X0: $i,X1: $i,X2: $i] : c_minus(c_emptyset,c_insert(X0,X1,X2),tc_set(X2)) = c_emptyset,
inference(superposition,[status(thm)],[c_9270,c_2857]) ).
tcf(c_9515,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_lessequals(c_minus(X0,X1,tc_set(X2)),X1,tc_set(X2))
| ( c_minus(X0,X1,tc_set(X2)) != c_emptyset ) ),
inference(superposition,[status(thm)],[c_2857,c_2834]) ).
tcf(c_9526,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_in(c_minus(X1,c_insert(X0,c_emptyset,X2),tc_set(X2)),c_Finite__Set_OFinites,tc_set(X2))
| ~ c_in(c_insert(X0,X1,X2),c_Finite__Set_OFinites,tc_set(X2)) ),
inference(superposition,[status(thm)],[c_2851,c_2945]) ).
tcf(c_9540,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( c_in(X0,c_insert(X3,c_insert(X4,X1,X2),X2),X2)
| ~ c_in(X0,X1,X2) ),
inference(superposition,[status(thm)],[c_9272,c_2799]) ).
tcf(c_9549,plain,
! [X0: $i,X1: $i] :
( c_less(c_emptyset,X0,tc_set(X1))
| ( X0 = c_emptyset ) ),
inference(superposition,[status(thm)],[c_2814,c_2811]) ).
tcf(c_9551,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_less(X1,c_insert(X0,X1,X2),tc_set(X2))
| ( c_insert(X0,X1,X2) = X1 ) ),
inference(superposition,[status(thm)],[c_9261,c_2811]) ).
tcf(c_9552,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c_less(X2,c_insert(X0,c_insert(X1,X2,X3),X3),tc_set(X3))
| ( c_insert(X0,c_insert(X1,X2,X3),X3) = X2 ) ),
inference(superposition,[status(thm)],[c_9272,c_2811]) ).
tcf(c_9582,plain,
( ( c_0 = c_1 )
| ~ c_less(c_1,c_0,tc_nat) ),
inference(superposition,[status(thm)],[c_2863,c_9397]) ).
tcf(c_9589,plain,
( ( c_Suc(c_0) = c_0 )
| ( c_Suc(c_minus(c_Suc(c_0),c_1,tc_nat)) = c_Suc(c_0) ) ),
inference(superposition,[status(thm)],[c_9322,c_9090]) ).
tcf(c_9591,plain,
! [X0: $i,X1: $i] :
( ( X0 = c_List_Olist_ONil )
| ( c_Suc(c_minus(c_Nat_Osize(X0,tc_List_Olist(X1)),c_1,tc_nat)) = c_Nat_Osize(X0,tc_List_Olist(X1)) ) ),
inference(superposition,[status(thm)],[c_2889,c_9090]) ).
tcf(c_9592,plain,
c_Suc(c_minus(c_1,c_1,tc_nat)) = c_1,
inference(superposition,[status(thm)],[c_2898,c_9090]) ).
tcf(c_9593,plain,
! [X0: $i] :
( ( c_minus(X0,c_0,tc_nat) = c_0 )
| ( c_Suc(c_minus(X0,c_1,tc_nat)) = X0 ) ),
inference(superposition,[status(thm)],[c_8552,c_9090]) ).
tcf(c_9594,plain,
! [X0: $i,X1: $i] :
( ( c_Suc(c_minus(c_minus(X1,X0,tc_nat),c_1,tc_nat)) = c_minus(X1,X0,tc_nat) )
| ~ c_less(X0,X1,tc_nat) ),
inference(superposition,[status(thm)],[c_2858,c_9090]) ).
tcf(c_9595,plain,
! [X0: $i,X1: $i] :
( ( c_Suc(c_minus(c_Nat_Opower(X0,c_Numeral_Onumber__of(X1,tc_nat),tc_nat),c_1,tc_nat)) = c_Nat_Opower(X0,c_Numeral_Onumber__of(X1,tc_nat),tc_nat) )
| ~ c_less(c_0,X0,tc_nat) ),
inference(superposition,[status(thm)],[c_2907,c_9090]) ).
tcf(c_9596,plain,
! [X0: $i,X1: $i] :
( ( X0 = c_0 )
| ( c_Suc(c_minus(c_Nat_Opower(X0,X1,tc_nat),c_1,tc_nat)) = c_Nat_Opower(X0,X1,tc_nat) ) ),
inference(superposition,[status(thm)],[c_2904,c_9090]) ).
tcf(c_9597,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ( c_Suc(c_minus(c_times(X0,c_1,tc_nat),c_1,tc_nat)) = c_times(X0,c_1,tc_nat) ) ),
inference(superposition,[status(thm)],[c_9199,c_9090]) ).
tcf(c_9599,plain,
( ( c_0 = c_1 )
| ( c_Suc(c_minus(c_1,c_1,tc_nat)) = c_1 ) ),
inference(light_normalisation,[status(thm)],[c_9589,c_9089]) ).
tcf(c_9639,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ( c_minus(X0,c_1,tc_nat) = c_0 )
| ~ c_less(X0,c_minus(c_minus(X0,c_1,tc_nat),c_1,tc_nat),tc_nat) ),
inference(superposition,[status(thm)],[c_9353,c_9393]) ).
tcf(c_9641,plain,
( ( c_0 = c_1 )
| ~ c_less(c_Suc(c_1),c_0,tc_nat) ),
inference(superposition,[status(thm)],[c_2863,c_9393]) ).
tcf(c_9648,plain,
! [X0: $i,X1: $i] :
( c_less(X1,X0,tc_nat)
| ( c_minus(X0,c_plus(X1,c_0,tc_nat),tc_nat) = c_0 ) ),
inference(demodulation,[status(thm)],[c_8566,c_2867]) ).
tcf(c_9655,plain,
! [X0: $i] : c_minus(X0,c_plus(X0,c_0,tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_9648,c_2824]) ).
tcf(c_9656,plain,
! [X0: $i] :
( c_less(X0,c_Suc(X0),tc_nat)
| ( c_minus(c_Suc(X0),c_plus(c_0,c_0,tc_nat),tc_nat) = c_0 ) ),
inference(superposition,[status(thm)],[c_9648,c_9312]) ).
tcf(c_9657,plain,
! [X0: $i] :
( ( c_Suc(c_minus(X0,c_1,tc_nat)) = X0 )
| ( c_minus(X0,c_plus(c_0,c_0,tc_nat),tc_nat) = c_0 ) ),
inference(superposition,[status(thm)],[c_9648,c_9090]) ).
tcf(c_9658,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ( c_minus(c_1,c_plus(X0,c_0,tc_nat),tc_nat) = c_0 ) ),
inference(superposition,[status(thm)],[c_9648,c_2899]) ).
tcf(c_9659,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_plus(c_plus(X1,X0,tc_nat),c_0,tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_9648,c_8594]) ).
tcf(c_9660,plain,
! [X0: $i] : c_minus(c_0,c_plus(X0,c_0,tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_9648,c_2825]) ).
tcf(c_9661,plain,
! [X0: $i,X1: $i] :
( c_less(X1,X0,tc_nat)
| ( c_minus(c_minus(X0,X1,tc_nat),c_plus(c_0,c_0,tc_nat),tc_nat) = c_0 ) ),
inference(superposition,[status(thm)],[c_9648,c_2859]) ).
tcf(c_9662,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ( c_minus(c_Nat_Opower(c_0,X0,tc_nat),c_plus(c_0,c_0,tc_nat),tc_nat) = c_0 ) ),
inference(superposition,[status(thm)],[c_9648,c_2905]) ).
tcf(c_9663,plain,
! [X0: $i] : c_minus(X0,c_plus(c_Suc(X0),c_0,tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_9648,c_8669]) ).
tcf(c_9664,plain,
! [X0: $i] : c_minus(X0,c_plus(c_Suc(c_Suc(X0)),c_0,tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_9648,c_8698]) ).
tcf(c_9665,plain,
! [X0: $i] : c_minus(X0,c_plus(c_Suc(c_Suc(c_Suc(X0))),c_0,tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_9648,c_8758]) ).
tcf(c_9666,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_plus(c_plus(X1,c_Suc(X0),tc_nat),c_0,tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_9648,c_8769]) ).
tcf(c_9667,plain,
! [X0: $i] : c_minus(X0,c_plus(c_Suc(c_Suc(c_Suc(c_Suc(X0)))),c_0,tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_9648,c_8808]) ).
tcf(c_9668,plain,
! [X0: $i] : c_minus(c_1,c_plus(c_Suc(X0),c_0,tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_9648,c_8867]) ).
tcf(c_9669,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_plus(c_plus(X1,c_Suc(c_Suc(X0)),tc_nat),c_0,tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_9648,c_8881]) ).
tcf(c_9670,plain,
! [X0: $i] : c_minus(X0,c_plus(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))),c_0,tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_9648,c_8917]) ).
tcf(c_9671,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_plus(c_plus(X1,c_Suc(c_Suc(c_Suc(X0))),tc_nat),c_0,tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_9648,c_8990]) ).
tcf(c_9672,plain,
! [X0: $i] : c_minus(X0,c_plus(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0)))))),c_0,tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_9648,c_9030]) ).
tcf(c_9673,plain,
! [X0: $i] :
( c_less(c_0,X0,tc_nat)
| ( c_minus(c_Suc(X0),c_plus(c_1,c_0,tc_nat),tc_nat) = c_0 ) ),
inference(superposition,[status(thm)],[c_9648,c_9153]) ).
tcf(c_9674,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ( c_minus(c_minus(X0,c_1,tc_nat),c_plus(c_Suc(X0),c_0,tc_nat),tc_nat) = c_0 ) ),
inference(superposition,[status(thm)],[c_9648,c_9393]) ).
tcf(c_9675,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ( c_minus(c_minus(X0,c_1,tc_nat),c_plus(X0,c_0,tc_nat),tc_nat) = c_0 ) ),
inference(superposition,[status(thm)],[c_9648,c_9397]) ).
tcf(c_9727,plain,
! [X0: $i] :
( c_less(c_0,c_0,tc_nat)
| ~ c_less(c_plus(X0,c_0,tc_nat),X0,tc_nat) ),
inference(superposition,[status(thm)],[c_9655,c_2858]) ).
tcf(c_9734,plain,
! [X0: $i] : c_lessequals(X0,c_plus(X0,c_0,tc_nat),tc_nat),
inference(superposition,[status(thm)],[c_9655,c_2866]) ).
tcf(c_9735,plain,
! [X0: $i] :
( c_less(c_plus(X0,c_0,tc_nat),X0,tc_nat)
| ~ c_less(c_0,c_0,tc_nat) ),
inference(superposition,[status(thm)],[c_9655,c_2859]) ).
tcf(c_9737,plain,
! [X0: $i] : ~ c_less(c_plus(X0,c_0,tc_nat),X0,tc_nat),
inference(forward_subsumption_resolution,[status(thm)],[c_9727,c_2825]) ).
tcf(c_9749,plain,
! [X0: $i] : c_minus(X0,c_plus(c_plus(X0,c_0,tc_nat),c_0,tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_9648,c_9737]) ).
tcf(c_9752,plain,
c_minus(c_0,c_plus(c_1,c_0,tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_9089,c_9663]) ).
tcf(c_9754,plain,
! [X0: $i] :
( c_less(c_0,c_0,tc_nat)
| ~ c_less(c_plus(c_Suc(X0),c_0,tc_nat),X0,tc_nat) ),
inference(superposition,[status(thm)],[c_9663,c_2858]) ).
tcf(c_9761,plain,
! [X0: $i] : c_lessequals(X0,c_plus(c_Suc(X0),c_0,tc_nat),tc_nat),
inference(superposition,[status(thm)],[c_9663,c_2866]) ).
tcf(c_9762,plain,
! [X0: $i] :
( c_less(c_plus(c_Suc(X0),c_0,tc_nat),X0,tc_nat)
| ~ c_less(c_0,c_0,tc_nat) ),
inference(superposition,[status(thm)],[c_9663,c_2859]) ).
tcf(c_9764,plain,
! [X0: $i] : ~ c_less(c_plus(c_Suc(X0),c_0,tc_nat),X0,tc_nat),
inference(forward_subsumption_resolution,[status(thm)],[c_9754,c_2825]) ).
tcf(c_9782,plain,
! [X0: $i,X1: $i] : c_minus(c_0,c_plus(X0,X1,tc_nat),tc_nat) = c_minus(c_0,X1,tc_nat),
inference(superposition,[status(thm)],[c_2870,c_2867]) ).
tcf(c_9783,plain,
! [X0: $i,X1: $i,X2: $i] : c_minus(c_Suc(X0),c_plus(c_Suc(X1),X2,tc_nat),tc_nat) = c_minus(c_minus(X0,X1,tc_nat),X2,tc_nat),
inference(superposition,[status(thm)],[c_2869,c_2867]) ).
tcf(c_9784,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_plus(X0,X1,tc_nat),tc_nat) = c_minus(c_0,X1,tc_nat),
inference(superposition,[status(thm)],[c_2863,c_2867]) ).
tcf(c_9785,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_plus(c_0,X1,tc_nat),tc_nat) = c_minus(X0,X1,tc_nat),
inference(superposition,[status(thm)],[c_2860,c_2867]) ).
tcf(c_9786,plain,
! [X0: $i,X1: $i] :
( ( X0 = c_0 )
| ( c_minus(c_1,c_plus(X0,X1,tc_nat),tc_nat) = c_minus(c_0,X1,tc_nat) ) ),
inference(superposition,[status(thm)],[c_8564,c_2867]) ).
tcf(c_9787,plain,
! [X0: $i,X1: $i,X2: $i] : c_minus(X0,c_plus(c_plus(X1,X0,tc_nat),X2,tc_nat),tc_nat) = c_minus(c_0,X2,tc_nat),
inference(superposition,[status(thm)],[c_8590,c_2867]) ).
tcf(c_9788,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_plus(c_Suc(X0),X1,tc_nat),tc_nat) = c_minus(c_0,X1,tc_nat),
inference(superposition,[status(thm)],[c_8660,c_2867]) ).
tcf(c_9789,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_plus(c_Suc(c_Suc(X0)),X1,tc_nat),tc_nat) = c_minus(c_0,X1,tc_nat),
inference(superposition,[status(thm)],[c_8688,c_2867]) ).
tcf(c_9790,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_plus(c_Suc(c_Suc(c_Suc(X0))),X1,tc_nat),tc_nat) = c_minus(c_0,X1,tc_nat),
inference(superposition,[status(thm)],[c_8713,c_2867]) ).
tcf(c_9791,plain,
! [X0: $i,X1: $i,X2: $i] : c_minus(X0,c_plus(c_plus(X1,c_Suc(X0),tc_nat),X2,tc_nat),tc_nat) = c_minus(c_0,X2,tc_nat),
inference(superposition,[status(thm)],[c_8761,c_2867]) ).
tcf(c_9792,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_plus(c_Suc(c_Suc(c_Suc(c_Suc(X0)))),X1,tc_nat),tc_nat) = c_minus(c_0,X1,tc_nat),
inference(superposition,[status(thm)],[c_8788,c_2867]) ).
tcf(c_9793,plain,
! [X0: $i,X1: $i] : c_minus(c_1,c_plus(c_Suc(X0),X1,tc_nat),tc_nat) = c_minus(c_0,X1,tc_nat),
inference(superposition,[status(thm)],[c_8853,c_2867]) ).
tcf(c_9794,plain,
! [X0: $i,X1: $i,X2: $i] : c_minus(X0,c_plus(c_plus(X1,c_Suc(c_Suc(X0)),tc_nat),X2,tc_nat),tc_nat) = c_minus(c_0,X2,tc_nat),
inference(superposition,[status(thm)],[c_8872,c_2867]) ).
tcf(c_9795,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_plus(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))),X1,tc_nat),tc_nat) = c_minus(c_0,X1,tc_nat),
inference(superposition,[status(thm)],[c_8903,c_2867]) ).
tcf(c_9796,plain,
! [X0: $i,X1: $i,X2: $i] : c_minus(X0,c_plus(c_plus(X1,c_Suc(c_Suc(c_Suc(X0))),tc_nat),X2,tc_nat),tc_nat) = c_minus(c_0,X2,tc_nat),
inference(superposition,[status(thm)],[c_8980,c_2867]) ).
tcf(c_9797,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_plus(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0)))))),X1,tc_nat),tc_nat) = c_minus(c_0,X1,tc_nat),
inference(superposition,[status(thm)],[c_9015,c_2867]) ).
tcf(c_9798,plain,
! [X0: $i,X1: $i] : c_minus(c_Suc(X0),c_plus(c_1,X1,tc_nat),tc_nat) = c_minus(X0,X1,tc_nat),
inference(superposition,[status(thm)],[c_9144,c_2867]) ).
tcf(c_9799,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_plus(c_plus(X0,c_0,tc_nat),X1,tc_nat),tc_nat) = c_minus(c_0,X1,tc_nat),
inference(superposition,[status(thm)],[c_9655,c_2867]) ).
tcf(c_9800,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_plus(c_plus(c_Suc(X0),c_0,tc_nat),X1,tc_nat),tc_nat) = c_minus(c_0,X1,tc_nat),
inference(superposition,[status(thm)],[c_9663,c_2867]) ).
tcf(c_9801,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_less(c_0,c_minus(X1,c_plus(X2,X0,tc_nat),tc_nat),tc_nat)
| ~ c_less(X0,c_minus(X1,X2,tc_nat),tc_nat) ),
inference(superposition,[status(thm)],[c_2867,c_2858]) ).
tcf(c_9802,plain,
! [X0: $i,X1: $i] :
( ( c_minus(X0,X1,tc_nat) = c_0 )
| ~ c_less(c_Suc(c_minus(X0,X1,tc_nat)),c_minus(X0,c_plus(X1,c_1,tc_nat),tc_nat),tc_nat) ),
inference(superposition,[status(thm)],[c_2867,c_9393]) ).
tcf(c_9803,plain,
! [X0: $i,X1: $i] :
( ( c_minus(X0,X1,tc_nat) = c_0 )
| ~ c_less(c_minus(X0,X1,tc_nat),c_minus(X0,c_plus(X1,c_1,tc_nat),tc_nat),tc_nat) ),
inference(superposition,[status(thm)],[c_2867,c_9397]) ).
tcf(c_9804,plain,
! [X0: $i,X1: $i] :
( ( c_minus(X0,X1,tc_nat) = c_0 )
| ( c_Suc(c_minus(X0,c_plus(X1,c_1,tc_nat),tc_nat)) = c_minus(X0,X1,tc_nat) ) ),
inference(superposition,[status(thm)],[c_2867,c_9353]) ).
tcf(c_9805,plain,
! [X0: $i,X1: $i] :
( c_less(c_minus(X0,c_plus(X1,c_1,tc_nat),tc_nat),c_minus(X0,X1,tc_nat),tc_nat)
| ~ c_less(c_0,c_minus(X0,X1,tc_nat),tc_nat) ),
inference(superposition,[status(thm)],[c_2867,c_9137]) ).
tcf(c_9806,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : c_minus(c_minus(X0,c_plus(X1,X2,tc_nat),tc_nat),X3,tc_nat) = c_minus(c_minus(X0,X1,tc_nat),c_plus(X2,X3,tc_nat),tc_nat),
inference(superposition,[status(thm)],[c_2867,c_2867]) ).
tcf(c_9807,plain,
! [X0: $i,X1: $i,X2: $i] : c_lessequals(c_minus(X0,c_plus(X1,X2,tc_nat),tc_nat),c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_minus(X0,X1,tc_nat))))))),tc_nat),
inference(superposition,[status(thm)],[c_2867,c_8887]) ).
tcf(c_9808,plain,
! [X0: $i,X1: $i,X2: $i] : c_lessequals(c_minus(X0,c_plus(X1,X2,tc_nat),tc_nat),c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_minus(X0,X1,tc_nat)))))),tc_nat),
inference(superposition,[status(thm)],[c_2867,c_8775]) ).
tcf(c_9809,plain,
! [X0: $i,X1: $i,X2: $i] : c_lessequals(c_minus(X0,c_plus(X1,X2,tc_nat),tc_nat),c_Suc(c_Suc(c_Suc(c_Suc(c_minus(X0,X1,tc_nat))))),tc_nat),
inference(superposition,[status(thm)],[c_2867,c_8702]) ).
tcf(c_9810,plain,
! [X0: $i,X1: $i,X2: $i] : c_lessequals(c_minus(X0,c_plus(X1,X2,tc_nat),tc_nat),c_Suc(c_Suc(c_Suc(c_minus(X0,X1,tc_nat)))),tc_nat),
inference(superposition,[status(thm)],[c_2867,c_8678]) ).
tcf(c_9811,plain,
! [X0: $i,X1: $i,X2: $i] : c_lessequals(c_minus(X0,c_plus(X1,X2,tc_nat),tc_nat),c_Suc(c_Suc(c_minus(X0,X1,tc_nat))),tc_nat),
inference(superposition,[status(thm)],[c_2867,c_8651]) ).
tcf(c_9812,plain,
! [X0: $i,X1: $i,X2: $i] : c_lessequals(c_minus(X0,c_plus(X1,X2,tc_nat),tc_nat),c_Suc(c_minus(X0,X1,tc_nat)),tc_nat),
inference(superposition,[status(thm)],[c_2867,c_8623]) ).
tcf(c_9813,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_lessequals(c_minus(X0,X1,tc_nat),X2,tc_nat)
| ( c_minus(X0,c_plus(X1,X2,tc_nat),tc_nat) != c_0 ) ),
inference(superposition,[status(thm)],[c_2867,c_2866]) ).
tcf(c_9814,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_less(X2,c_minus(X0,X1,tc_nat),tc_nat)
| ~ c_less(c_0,c_minus(X0,c_plus(X1,X2,tc_nat),tc_nat),tc_nat) ),
inference(superposition,[status(thm)],[c_2867,c_2859]) ).
tcf(c_9815,plain,
! [X0: $i,X1: $i,X2: $i] : c_lessequals(c_minus(X0,c_plus(X1,X2,tc_nat),tc_nat),c_minus(X0,X1,tc_nat),tc_nat),
inference(superposition,[status(thm)],[c_2867,c_2864]) ).
tcf(c_9816,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_less(c_minus(X0,c_plus(X1,c_Suc(X2),tc_nat),tc_nat),c_minus(X0,X1,tc_nat),tc_nat)
| ~ c_less(c_0,c_minus(X0,X1,tc_nat),tc_nat) ),
inference(superposition,[status(thm)],[c_2867,c_2868]) ).
tcf(c_9817,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_plus(X1,c_minus(X0,X1,tc_nat),tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_2867,c_2863]) ).
tcf(c_9818,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_plus(X1,c_0,tc_nat),tc_nat) = c_minus(X0,X1,tc_nat),
inference(superposition,[status(thm)],[c_2867,c_2860]) ).
tcf(c_9819,plain,
! [X0: $i,X1: $i,X2: $i] : c_minus(X0,c_plus(X1,c_plus(X2,c_minus(X0,X1,tc_nat),tc_nat),tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_2867,c_8590]) ).
tcf(c_9820,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_plus(X1,c_Suc(c_minus(X0,X1,tc_nat)),tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_2867,c_8660]) ).
tcf(c_9821,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_plus(X1,c_Suc(c_Suc(c_minus(X0,X1,tc_nat))),tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_2867,c_8688]) ).
tcf(c_9822,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_plus(X1,c_Suc(c_Suc(c_Suc(c_minus(X0,X1,tc_nat)))),tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_2867,c_8713]) ).
tcf(c_9823,plain,
! [X0: $i,X1: $i,X2: $i] : c_minus(X0,c_plus(X1,c_plus(X2,c_Suc(c_minus(X0,X1,tc_nat)),tc_nat),tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_2867,c_8761]) ).
tcf(c_9824,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_plus(X1,c_Suc(c_Suc(c_Suc(c_Suc(c_minus(X0,X1,tc_nat))))),tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_2867,c_8788]) ).
tcf(c_9825,plain,
! [X0: $i,X1: $i,X2: $i] : c_minus(X0,c_plus(X1,c_plus(X2,c_Suc(c_Suc(c_minus(X0,X1,tc_nat))),tc_nat),tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_2867,c_8872]) ).
tcf(c_9826,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_plus(X1,c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_minus(X0,X1,tc_nat)))))),tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_2867,c_8903]) ).
tcf(c_9827,plain,
! [X0: $i,X1: $i,X2: $i] : c_minus(X0,c_plus(X1,c_plus(X2,c_Suc(c_Suc(c_Suc(c_minus(X0,X1,tc_nat)))),tc_nat),tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_2867,c_8980]) ).
tcf(c_9828,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_plus(X1,c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_minus(X0,X1,tc_nat))))))),tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_2867,c_9015]) ).
tcf(c_9829,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_plus(X1,c_plus(c_minus(X0,X1,tc_nat),c_0,tc_nat),tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_2867,c_9655]) ).
tcf(c_9830,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_plus(X1,c_plus(c_Suc(c_minus(X0,X1,tc_nat)),c_0,tc_nat),tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_2867,c_9663]) ).
tcf(c_9839,plain,
! [X0: $i,X1: $i,X2: $i] : c_minus(c_Suc(X0),c_plus(c_Suc(X1),X2,tc_nat),tc_nat) = c_minus(X0,c_plus(X1,X2,tc_nat),tc_nat),
inference(light_normalisation,[status(thm)],[c_9783,c_2867]) ).
tcf(c_9966,plain,
! [X0: $i,X1: $i] : ~ c_Wellfounded__Recursion_Owf(c_Transitive__Closure_Ortrancl(X0,X1),X1),
inference(superposition,[status(thm)],[c_2948,c_2845]) ).
tcf(c_9967,plain,
! [X0: $i] : ~ c_Wellfounded__Recursion_Owf(c_Relation_OId,X0),
inference(superposition,[status(thm)],[c_8813,c_2845]) ).
tcf(c_9968,plain,
! [X0: $i,X1: $i,X2: $i] : ~ c_Wellfounded__Recursion_Owf(c_insert(c_Pair(X0,X0,X1,X1),X2,tc_prod(X1,X1)),X1),
inference(superposition,[status(thm)],[c_2941,c_2845]) ).
tcf(c_9969,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ~ c_Wellfounded__Recursion_Owf(c_insert(X3,X2,tc_prod(X1,X1)),X1)
| ~ c_in(c_Pair(X0,X0,X1,X1),X2,tc_prod(X1,X1)) ),
inference(superposition,[status(thm)],[c_2940,c_2845]) ).
tcf(c_9971,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : ~ c_Wellfounded__Recursion_Owf(c_insert(X0,c_insert(c_Pair(X1,X1,X2,X2),X3,tc_prod(X2,X2)),tc_prod(X2,X2)),X2),
inference(superposition,[status(thm)],[c_9273,c_2845]) ).
tcf(c_9972,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] : ~ c_Wellfounded__Recursion_Owf(c_insert(X0,c_insert(X1,c_insert(c_Pair(X2,X2,X3,X3),X4,tc_prod(X3,X3)),tc_prod(X3,X3)),tc_prod(X3,X3)),X3),
inference(superposition,[status(thm)],[c_9299,c_2845]) ).
tcf(c_9997,plain,
! [X0: $i] : c_plus(c_0,c_minus(X0,c_0,tc_nat),tc_nat) = X0,
inference(superposition,[status(thm)],[c_2806,c_2861]) ).
tcf(c_9998,plain,
! [X0: $i,X1: $i] : c_plus(c_minus(X0,X1,tc_nat),c_minus(X0,c_minus(X0,X1,tc_nat),tc_nat),tc_nat) = X0,
inference(superposition,[status(thm)],[c_2864,c_2861]) ).
tcf(c_9999,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ( c_plus(c_1,c_minus(X0,c_1,tc_nat),tc_nat) = X0 ) ),
inference(superposition,[status(thm)],[c_8604,c_2861]) ).
tcf(c_10000,plain,
! [X0: $i] : c_plus(X0,c_minus(X0,X0,tc_nat),tc_nat) = X0,
inference(superposition,[status(thm)],[c_8488,c_2861]) ).
tcf(c_10001,plain,
! [X0: $i,X1: $i] : c_plus(X0,c_minus(c_plus(X1,X0,tc_nat),X0,tc_nat),tc_nat) = c_plus(X1,X0,tc_nat),
inference(superposition,[status(thm)],[c_8605,c_2861]) ).
tcf(c_10002,plain,
! [X0: $i,X1: $i] : c_plus(c_minus(X0,X1,tc_nat),c_minus(c_Suc(X0),c_minus(X0,X1,tc_nat),tc_nat),tc_nat) = c_Suc(X0),
inference(superposition,[status(thm)],[c_8623,c_2861]) ).
tcf(c_10003,plain,
! [X0: $i,X1: $i] : c_plus(c_minus(X0,X1,tc_nat),c_minus(c_Suc(c_Suc(X0)),c_minus(X0,X1,tc_nat),tc_nat),tc_nat) = c_Suc(c_Suc(X0)),
inference(superposition,[status(thm)],[c_8651,c_2861]) ).
tcf(c_10004,plain,
! [X0: $i] : c_plus(X0,c_minus(c_Suc(X0),X0,tc_nat),tc_nat) = c_Suc(X0),
inference(superposition,[status(thm)],[c_8653,c_2861]) ).
tcf(c_10005,plain,
! [X0: $i,X1: $i] : c_plus(c_minus(X0,X1,tc_nat),c_minus(c_Suc(c_Suc(c_Suc(X0))),c_minus(X0,X1,tc_nat),tc_nat),tc_nat) = c_Suc(c_Suc(c_Suc(X0))),
inference(superposition,[status(thm)],[c_8678,c_2861]) ).
tcf(c_10006,plain,
! [X0: $i] : c_plus(X0,c_minus(c_Suc(c_Suc(X0)),X0,tc_nat),tc_nat) = c_Suc(c_Suc(X0)),
inference(superposition,[status(thm)],[c_8680,c_2861]) ).
tcf(c_10007,plain,
! [X0: $i,X1: $i] : c_plus(c_minus(X0,X1,tc_nat),c_minus(c_Suc(c_Suc(c_Suc(c_Suc(X0)))),c_minus(X0,X1,tc_nat),tc_nat),tc_nat) = c_Suc(c_Suc(c_Suc(c_Suc(X0)))),
inference(superposition,[status(thm)],[c_8702,c_2861]) ).
tcf(c_10008,plain,
! [X0: $i] : c_plus(X0,c_minus(c_Suc(c_Suc(c_Suc(X0))),X0,tc_nat),tc_nat) = c_Suc(c_Suc(c_Suc(X0))),
inference(superposition,[status(thm)],[c_8704,c_2861]) ).
tcf(c_10009,plain,
! [X0: $i,X1: $i] : c_plus(X0,c_minus(c_plus(X1,c_Suc(X0),tc_nat),X0,tc_nat),tc_nat) = c_plus(X1,c_Suc(X0),tc_nat),
inference(superposition,[status(thm)],[c_8766,c_2861]) ).
tcf(c_10010,plain,
! [X0: $i,X1: $i] : c_plus(c_minus(X0,X1,tc_nat),c_minus(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))),c_minus(X0,X1,tc_nat),tc_nat),tc_nat) = c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))),
inference(superposition,[status(thm)],[c_8775,c_2861]) ).
tcf(c_10011,plain,
! [X0: $i] : c_plus(X0,c_minus(c_Suc(c_Suc(c_Suc(c_Suc(X0)))),X0,tc_nat),tc_nat) = c_Suc(c_Suc(c_Suc(c_Suc(X0)))),
inference(superposition,[status(thm)],[c_8777,c_2861]) ).
tcf(c_10012,plain,
! [X0: $i] : c_plus(c_1,c_minus(c_Suc(X0),c_1,tc_nat),tc_nat) = c_Suc(X0),
inference(superposition,[status(thm)],[c_8863,c_2861]) ).
tcf(c_10013,plain,
! [X0: $i,X1: $i] : c_plus(X0,c_minus(c_plus(X1,c_Suc(c_Suc(X0)),tc_nat),X0,tc_nat),tc_nat) = c_plus(X1,c_Suc(c_Suc(X0)),tc_nat),
inference(superposition,[status(thm)],[c_8878,c_2861]) ).
tcf(c_10014,plain,
! [X0: $i,X1: $i] : c_plus(c_minus(X0,X1,tc_nat),c_minus(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0)))))),c_minus(X0,X1,tc_nat),tc_nat),tc_nat) = c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0)))))),
inference(superposition,[status(thm)],[c_8887,c_2861]) ).
tcf(c_10015,plain,
! [X0: $i] : c_plus(X0,c_minus(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))),X0,tc_nat),tc_nat) = c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))),
inference(superposition,[status(thm)],[c_8889,c_2861]) ).
tcf(c_10016,plain,
! [X0: $i,X1: $i] : c_plus(X0,c_minus(c_plus(X1,c_Suc(c_Suc(c_Suc(X0))),tc_nat),X0,tc_nat),tc_nat) = c_plus(X1,c_Suc(c_Suc(c_Suc(X0))),tc_nat),
inference(superposition,[status(thm)],[c_8987,c_2861]) ).
tcf(c_10017,plain,
! [X0: $i] : c_plus(X0,c_minus(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0)))))),X0,tc_nat),tc_nat) = c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0)))))),
inference(superposition,[status(thm)],[c_8998,c_2861]) ).
tcf(c_10018,plain,
! [X0: $i,X1: $i] :
( ( c_plus(c_1,c_minus(c_Nat_Opower(X0,X1,tc_nat),c_1,tc_nat),tc_nat) = c_Nat_Opower(X0,X1,tc_nat) )
| ~ c_lessequals(c_1,X0,tc_nat) ),
inference(superposition,[status(thm)],[c_9094,c_2861]) ).
tcf(c_10019,plain,
! [X0: $i] : c_plus(X0,c_minus(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))))),X0,tc_nat),tc_nat) = c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))))),
inference(superposition,[status(thm)],[c_9154,c_2861]) ).
tcf(c_10020,plain,
! [X0: $i] :
( ( c_plus(c_1,c_minus(c_times(X0,c_1,tc_nat),c_1,tc_nat),tc_nat) = c_times(X0,c_1,tc_nat) )
| ~ c_lessequals(c_1,X0,tc_nat) ),
inference(superposition,[status(thm)],[c_9223,c_2861]) ).
tcf(c_10021,plain,
! [X0: $i] : c_plus(X0,c_minus(c_plus(X0,c_0,tc_nat),X0,tc_nat),tc_nat) = c_plus(X0,c_0,tc_nat),
inference(superposition,[status(thm)],[c_9734,c_2861]) ).
tcf(c_10022,plain,
! [X0: $i] : c_plus(X0,c_0,tc_nat) = X0,
inference(light_normalisation,[status(thm)],[c_10000,c_2863]) ).
tcf(c_10023,plain,
! [X0: $i] : c_plus(c_0,X0,tc_nat) = X0,
inference(light_normalisation,[status(thm)],[c_9997,c_2860]) ).
tcf(c_10024,plain,
! [X0: $i] : c_plus(c_1,X0,tc_nat) = c_Suc(X0),
inference(light_normalisation,[status(thm)],[c_10012,c_9144]) ).
tcf(c_10100,plain,
! [X0: $i] : c_plus(c_minus(X0,c_0,tc_nat),c_0,tc_nat) = X0,
inference(superposition,[status(thm)],[c_2806,c_2862]) ).
tcf(c_10101,plain,
! [X0: $i,X1: $i] : c_plus(c_minus(X0,c_minus(X0,X1,tc_nat),tc_nat),c_minus(X0,X1,tc_nat),tc_nat) = X0,
inference(superposition,[status(thm)],[c_2864,c_2862]) ).
tcf(c_10102,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ( c_plus(c_minus(X0,c_1,tc_nat),c_1,tc_nat) = X0 ) ),
inference(superposition,[status(thm)],[c_8604,c_2862]) ).
tcf(c_10103,plain,
! [X0: $i] : c_plus(c_minus(X0,X0,tc_nat),X0,tc_nat) = X0,
inference(superposition,[status(thm)],[c_8488,c_2862]) ).
tcf(c_10104,plain,
! [X0: $i,X1: $i] : c_plus(c_minus(c_plus(X0,X1,tc_nat),X1,tc_nat),X1,tc_nat) = c_plus(X0,X1,tc_nat),
inference(superposition,[status(thm)],[c_8605,c_2862]) ).
tcf(c_10105,plain,
! [X0: $i,X1: $i] : c_plus(c_minus(c_Suc(X0),c_minus(X0,X1,tc_nat),tc_nat),c_minus(X0,X1,tc_nat),tc_nat) = c_Suc(X0),
inference(superposition,[status(thm)],[c_8623,c_2862]) ).
tcf(c_10106,plain,
! [X0: $i,X1: $i] : c_plus(c_minus(c_Suc(c_Suc(X0)),c_minus(X0,X1,tc_nat),tc_nat),c_minus(X0,X1,tc_nat),tc_nat) = c_Suc(c_Suc(X0)),
inference(superposition,[status(thm)],[c_8651,c_2862]) ).
tcf(c_10107,plain,
! [X0: $i] : c_plus(c_minus(c_Suc(X0),X0,tc_nat),X0,tc_nat) = c_Suc(X0),
inference(superposition,[status(thm)],[c_8653,c_2862]) ).
tcf(c_10108,plain,
! [X0: $i,X1: $i] : c_plus(c_minus(c_Suc(c_Suc(c_Suc(X0))),c_minus(X0,X1,tc_nat),tc_nat),c_minus(X0,X1,tc_nat),tc_nat) = c_Suc(c_Suc(c_Suc(X0))),
inference(superposition,[status(thm)],[c_8678,c_2862]) ).
tcf(c_10109,plain,
! [X0: $i] : c_plus(c_minus(c_Suc(c_Suc(X0)),X0,tc_nat),X0,tc_nat) = c_Suc(c_Suc(X0)),
inference(superposition,[status(thm)],[c_8680,c_2862]) ).
tcf(c_10110,plain,
! [X0: $i,X1: $i] : c_plus(c_minus(c_Suc(c_Suc(c_Suc(c_Suc(X0)))),c_minus(X0,X1,tc_nat),tc_nat),c_minus(X0,X1,tc_nat),tc_nat) = c_Suc(c_Suc(c_Suc(c_Suc(X0)))),
inference(superposition,[status(thm)],[c_8702,c_2862]) ).
tcf(c_10111,plain,
! [X0: $i] : c_plus(c_minus(c_Suc(c_Suc(c_Suc(X0))),X0,tc_nat),X0,tc_nat) = c_Suc(c_Suc(c_Suc(X0))),
inference(superposition,[status(thm)],[c_8704,c_2862]) ).
tcf(c_10112,plain,
! [X0: $i,X1: $i] : c_plus(c_minus(c_plus(X0,c_Suc(X1),tc_nat),X1,tc_nat),X1,tc_nat) = c_plus(X0,c_Suc(X1),tc_nat),
inference(superposition,[status(thm)],[c_8766,c_2862]) ).
tcf(c_10113,plain,
! [X0: $i,X1: $i] : c_plus(c_minus(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))),c_minus(X0,X1,tc_nat),tc_nat),c_minus(X0,X1,tc_nat),tc_nat) = c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))),
inference(superposition,[status(thm)],[c_8775,c_2862]) ).
tcf(c_10114,plain,
! [X0: $i] : c_plus(c_minus(c_Suc(c_Suc(c_Suc(c_Suc(X0)))),X0,tc_nat),X0,tc_nat) = c_Suc(c_Suc(c_Suc(c_Suc(X0)))),
inference(superposition,[status(thm)],[c_8777,c_2862]) ).
tcf(c_10115,plain,
! [X0: $i] : c_plus(c_minus(c_Suc(X0),c_1,tc_nat),c_1,tc_nat) = c_Suc(X0),
inference(superposition,[status(thm)],[c_8863,c_2862]) ).
tcf(c_10116,plain,
! [X0: $i,X1: $i] : c_plus(c_minus(c_plus(X0,c_Suc(c_Suc(X1)),tc_nat),X1,tc_nat),X1,tc_nat) = c_plus(X0,c_Suc(c_Suc(X1)),tc_nat),
inference(superposition,[status(thm)],[c_8878,c_2862]) ).
tcf(c_10117,plain,
! [X0: $i,X1: $i] : c_plus(c_minus(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0)))))),c_minus(X0,X1,tc_nat),tc_nat),c_minus(X0,X1,tc_nat),tc_nat) = c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0)))))),
inference(superposition,[status(thm)],[c_8887,c_2862]) ).
tcf(c_10118,plain,
! [X0: $i] : c_plus(c_minus(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))),X0,tc_nat),X0,tc_nat) = c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))),
inference(superposition,[status(thm)],[c_8889,c_2862]) ).
tcf(c_10119,plain,
! [X0: $i,X1: $i] : c_plus(c_minus(c_plus(X0,c_Suc(c_Suc(c_Suc(X1))),tc_nat),X1,tc_nat),X1,tc_nat) = c_plus(X0,c_Suc(c_Suc(c_Suc(X1))),tc_nat),
inference(superposition,[status(thm)],[c_8987,c_2862]) ).
tcf(c_10120,plain,
! [X0: $i] : c_plus(c_minus(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0)))))),X0,tc_nat),X0,tc_nat) = c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0)))))),
inference(superposition,[status(thm)],[c_8998,c_2862]) ).
tcf(c_10121,plain,
! [X0: $i,X1: $i] :
( ( c_plus(c_minus(c_Nat_Opower(X0,X1,tc_nat),c_1,tc_nat),c_1,tc_nat) = c_Nat_Opower(X0,X1,tc_nat) )
| ~ c_lessequals(c_1,X0,tc_nat) ),
inference(superposition,[status(thm)],[c_9094,c_2862]) ).
tcf(c_10122,plain,
! [X0: $i] : c_plus(c_minus(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))))),X0,tc_nat),X0,tc_nat) = c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))))),
inference(superposition,[status(thm)],[c_9154,c_2862]) ).
tcf(c_10123,plain,
! [X0: $i] :
( ( c_plus(c_minus(c_times(X0,c_1,tc_nat),c_1,tc_nat),c_1,tc_nat) = c_times(X0,c_1,tc_nat) )
| ~ c_lessequals(c_1,X0,tc_nat) ),
inference(superposition,[status(thm)],[c_9223,c_2862]) ).
tcf(c_10126,plain,
! [X0: $i] : c_plus(X0,c_1,tc_nat) = c_Suc(X0),
inference(light_normalisation,[status(thm)],[c_10115,c_9144]) ).
tcf(c_10215,plain,
! [X0: $i] : c_plus(c_Suc(X0),c_minus(c_Suc(X0),X0,tc_nat),tc_nat) = c_Suc(c_Suc(X0)),
inference(superposition,[status(thm)],[c_2869,c_10004]) ).
tcf(c_10216,plain,
c_plus(c_0,c_Suc(c_0),tc_nat) = c_Suc(c_0),
inference(superposition,[status(thm)],[c_2860,c_10004]) ).
tcf(c_10217,plain,
c_plus(c_1,c_1,tc_nat) = c_Suc(c_1),
inference(superposition,[status(thm)],[c_9144,c_10004]) ).
tcf(c_10218,plain,
c_plus(c_0,c_minus(c_1,c_0,tc_nat),tc_nat) = c_1,
inference(superposition,[status(thm)],[c_9089,c_10004]) ).
tcf(c_10219,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ( c_plus(c_minus(X0,c_1,tc_nat),c_minus(X0,c_minus(X0,c_1,tc_nat),tc_nat),tc_nat) = X0 ) ),
inference(superposition,[status(thm)],[c_9353,c_10004]) ).
tcf(c_10220,plain,
! [X0: $i] : ~ c_less(c_Suc(X0),c_minus(c_Suc(X0),X0,tc_nat),tc_nat),
inference(superposition,[status(thm)],[c_10004,c_8594]) ).
tcf(c_10221,plain,
! [X0: $i] : c_lessequals(c_minus(c_Suc(X0),X0,tc_nat),c_Suc(X0),tc_nat),
inference(superposition,[status(thm)],[c_10004,c_8605]) ).
tcf(c_10222,plain,
! [X0: $i] : c_minus(c_minus(c_Suc(X0),X0,tc_nat),c_Suc(X0),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_10004,c_8590]) ).
tcf(c_10223,plain,
c_minus(c_Suc(c_0),c_0,tc_nat) = c_Suc(c_0),
inference(superposition,[status(thm)],[c_10004,c_10023]) ).
tcf(c_10224,plain,
c_Suc(c_minus(c_Suc(c_1),c_1,tc_nat)) = c_Suc(c_1),
inference(superposition,[status(thm)],[c_10004,c_10024]) ).
tcf(c_10225,plain,
c_minus(c_1,c_0,tc_nat) = c_1,
inference(light_normalisation,[status(thm)],[c_10223,c_9089]) ).
tcf(c_10226,plain,
c_plus(c_0,c_1,tc_nat) = c_1,
inference(light_normalisation,[status(thm)],[c_10216,c_9089]) ).
tcf(c_10252,plain,
! [X0: $i] : c_minus(X0,c_minus(X0,c_0,tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_2806,c_2875]) ).
tcf(c_10253,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_minus(X0,c_minus(X0,X1,tc_nat),tc_nat),tc_nat) = c_minus(X0,X1,tc_nat),
inference(superposition,[status(thm)],[c_2864,c_2875]) ).
tcf(c_10254,plain,
! [X0: $i] :
( ( X0 = c_0 )
| ( c_minus(X0,c_minus(X0,c_1,tc_nat),tc_nat) = c_1 ) ),
inference(superposition,[status(thm)],[c_8604,c_2875]) ).
tcf(c_10255,plain,
! [X0: $i] : c_minus(X0,c_minus(X0,X0,tc_nat),tc_nat) = X0,
inference(superposition,[status(thm)],[c_8488,c_2875]) ).
tcf(c_10256,plain,
! [X0: $i,X1: $i] : c_minus(c_plus(X0,X1,tc_nat),c_minus(c_plus(X0,X1,tc_nat),X1,tc_nat),tc_nat) = X1,
inference(superposition,[status(thm)],[c_8605,c_2875]) ).
tcf(c_10257,plain,
! [X0: $i,X1: $i] : c_minus(c_Suc(X0),c_minus(c_Suc(X0),c_minus(X0,X1,tc_nat),tc_nat),tc_nat) = c_minus(X0,X1,tc_nat),
inference(superposition,[status(thm)],[c_8623,c_2875]) ).
tcf(c_10258,plain,
! [X0: $i,X1: $i] : c_minus(c_Suc(c_Suc(X0)),c_minus(c_Suc(c_Suc(X0)),c_minus(X0,X1,tc_nat),tc_nat),tc_nat) = c_minus(X0,X1,tc_nat),
inference(superposition,[status(thm)],[c_8651,c_2875]) ).
tcf(c_10259,plain,
! [X0: $i] : c_minus(c_Suc(X0),c_minus(c_Suc(X0),X0,tc_nat),tc_nat) = X0,
inference(superposition,[status(thm)],[c_8653,c_2875]) ).
tcf(c_10260,plain,
! [X0: $i,X1: $i] : c_minus(c_Suc(c_Suc(c_Suc(X0))),c_minus(c_Suc(c_Suc(c_Suc(X0))),c_minus(X0,X1,tc_nat),tc_nat),tc_nat) = c_minus(X0,X1,tc_nat),
inference(superposition,[status(thm)],[c_8678,c_2875]) ).
tcf(c_10261,plain,
! [X0: $i] : c_minus(c_Suc(c_Suc(X0)),c_minus(c_Suc(c_Suc(X0)),X0,tc_nat),tc_nat) = X0,
inference(superposition,[status(thm)],[c_8680,c_2875]) ).
tcf(c_10262,plain,
! [X0: $i,X1: $i] : c_minus(c_Suc(c_Suc(c_Suc(c_Suc(X0)))),c_minus(c_Suc(c_Suc(c_Suc(c_Suc(X0)))),c_minus(X0,X1,tc_nat),tc_nat),tc_nat) = c_minus(X0,X1,tc_nat),
inference(superposition,[status(thm)],[c_8702,c_2875]) ).
tcf(c_10263,plain,
! [X0: $i] : c_minus(c_Suc(c_Suc(c_Suc(X0))),c_minus(c_Suc(c_Suc(c_Suc(X0))),X0,tc_nat),tc_nat) = X0,
inference(superposition,[status(thm)],[c_8704,c_2875]) ).
tcf(c_10264,plain,
! [X0: $i,X1: $i] : c_minus(c_plus(X0,c_Suc(X1),tc_nat),c_minus(c_plus(X0,c_Suc(X1),tc_nat),X1,tc_nat),tc_nat) = X1,
inference(superposition,[status(thm)],[c_8766,c_2875]) ).
tcf(c_10265,plain,
! [X0: $i,X1: $i] : c_minus(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))),c_minus(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))),c_minus(X0,X1,tc_nat),tc_nat),tc_nat) = c_minus(X0,X1,tc_nat),
inference(superposition,[status(thm)],[c_8775,c_2875]) ).
tcf(c_10266,plain,
! [X0: $i] : c_minus(c_Suc(c_Suc(c_Suc(c_Suc(X0)))),c_minus(c_Suc(c_Suc(c_Suc(c_Suc(X0)))),X0,tc_nat),tc_nat) = X0,
inference(superposition,[status(thm)],[c_8777,c_2875]) ).
tcf(c_10267,plain,
! [X0: $i] : c_minus(c_Suc(X0),c_minus(c_Suc(X0),c_1,tc_nat),tc_nat) = c_1,
inference(superposition,[status(thm)],[c_8863,c_2875]) ).
tcf(c_10268,plain,
! [X0: $i,X1: $i] : c_minus(c_plus(X0,c_Suc(c_Suc(X1)),tc_nat),c_minus(c_plus(X0,c_Suc(c_Suc(X1)),tc_nat),X1,tc_nat),tc_nat) = X1,
inference(superposition,[status(thm)],[c_8878,c_2875]) ).
tcf(c_10269,plain,
! [X0: $i,X1: $i] : c_minus(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0)))))),c_minus(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0)))))),c_minus(X0,X1,tc_nat),tc_nat),tc_nat) = c_minus(X0,X1,tc_nat),
inference(superposition,[status(thm)],[c_8887,c_2875]) ).
tcf(c_10270,plain,
! [X0: $i] : c_minus(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))),c_minus(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))),X0,tc_nat),tc_nat) = X0,
inference(superposition,[status(thm)],[c_8889,c_2875]) ).
tcf(c_10271,plain,
! [X0: $i,X1: $i] : c_minus(c_plus(X0,c_Suc(c_Suc(c_Suc(X1))),tc_nat),c_minus(c_plus(X0,c_Suc(c_Suc(c_Suc(X1))),tc_nat),X1,tc_nat),tc_nat) = X1,
inference(superposition,[status(thm)],[c_8987,c_2875]) ).
tcf(c_10272,plain,
! [X0: $i] : c_minus(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0)))))),c_minus(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0)))))),X0,tc_nat),tc_nat) = X0,
inference(superposition,[status(thm)],[c_8998,c_2875]) ).
tcf(c_10273,plain,
! [X0: $i,X1: $i] :
( ( c_minus(c_Nat_Opower(X0,X1,tc_nat),c_minus(c_Nat_Opower(X0,X1,tc_nat),c_1,tc_nat),tc_nat) = c_1 )
| ~ c_lessequals(c_1,X0,tc_nat) ),
inference(superposition,[status(thm)],[c_9094,c_2875]) ).
tcf(c_10274,plain,
! [X0: $i] : c_minus(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))))),c_minus(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))))),X0,tc_nat),tc_nat) = X0,
inference(superposition,[status(thm)],[c_9154,c_2875]) ).
tcf(c_10275,plain,
! [X0: $i] :
( ( c_minus(c_times(X0,c_1,tc_nat),c_minus(c_times(X0,c_1,tc_nat),c_1,tc_nat),tc_nat) = c_1 )
| ~ c_lessequals(c_1,X0,tc_nat) ),
inference(superposition,[status(thm)],[c_9223,c_2875]) ).
tcf(c_10278,plain,
! [X0: $i] : c_minus(c_Suc(X0),X0,tc_nat) = c_1,
inference(light_normalisation,[status(thm)],[c_10267,c_9144]) ).
tcf(c_10341,plain,
! [X0: $i,X1: $i] :
( c_in(X0,c_Relation_OId,tc_prod(X1,X1))
| ~ c_in(X0,c_emptyset,tc_prod(X1,X1)) ),
inference(superposition,[status(thm)],[c_2952,c_2949]) ).
tcf(c_10343,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_in(X0,c_Transitive__Closure_Ortrancl(X1,X2),tc_prod(X2,X2))
| ~ c_in(X0,c_union(X1,c_Relation_OId,tc_prod(X2,X2)),tc_prod(X2,X2)) ),
inference(superposition,[status(thm)],[c_2950,c_2949]) ).
tcf(c_10345,plain,
! [X0: $i,X1: $i,X2: $i] :
( ~ c_Wellfounded__Recursion_Owf(c_Transitive__Closure_Ortrancl(X2,X1),X1)
| ~ c_in(c_Pair(X0,X0,X1,X1),X2,tc_prod(X1,X1)) ),
inference(superposition,[status(thm)],[c_2949,c_2845]) ).
tcf(c_10354,plain,
( ( c_Suc(c_1) = c_0 )
| ~ c_less(c_Suc(c_Suc(c_1)),c_1,tc_nat) ),
inference(superposition,[status(thm)],[c_10278,c_9393]) ).
tcf(c_10355,plain,
( ( c_Suc(c_1) = c_0 )
| ~ c_less(c_Suc(c_1),c_1,tc_nat) ),
inference(superposition,[status(thm)],[c_10278,c_9397]) ).
tcf(c_10357,plain,
! [X0: $i,X1: $i] : c_minus(c_Suc(X0),c_plus(X0,X1,tc_nat),tc_nat) = c_minus(c_1,X1,tc_nat),
inference(superposition,[status(thm)],[c_10278,c_2867]) ).
tcf(c_10358,plain,
! [X0: $i] : c_lessequals(c_1,c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))))),tc_nat),
inference(superposition,[status(thm)],[c_10278,c_8887]) ).
tcf(c_10359,plain,
! [X0: $i] : c_lessequals(c_1,c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0)))))),tc_nat),
inference(superposition,[status(thm)],[c_10278,c_8775]) ).
tcf(c_10360,plain,
! [X0: $i] : c_lessequals(c_1,c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))),tc_nat),
inference(superposition,[status(thm)],[c_10278,c_8702]) ).
tcf(c_10361,plain,
! [X0: $i] : c_lessequals(c_1,c_Suc(c_Suc(c_Suc(c_Suc(X0)))),tc_nat),
inference(superposition,[status(thm)],[c_10278,c_8678]) ).
tcf(c_10362,plain,
! [X0: $i] : c_lessequals(c_1,c_Suc(c_Suc(c_Suc(X0))),tc_nat),
inference(superposition,[status(thm)],[c_10278,c_8651]) ).
tcf(c_10363,plain,
! [X0: $i] : c_lessequals(c_1,c_Suc(c_Suc(X0)),tc_nat),
inference(superposition,[status(thm)],[c_10278,c_8623]) ).
tcf(c_10365,plain,
! [X0: $i] :
( c_less(X0,c_Suc(X0),tc_nat)
| ~ c_less(c_0,c_1,tc_nat) ),
inference(superposition,[status(thm)],[c_10278,c_2859]) ).
tcf(c_10368,plain,
! [X0: $i] :
( c_less(c_1,c_Suc(c_Suc(X0)),tc_nat)
| ~ c_less(c_0,c_Suc(c_Suc(X0)),tc_nat) ),
inference(superposition,[status(thm)],[c_10278,c_2868]) ).
tcf(c_10370,plain,
! [X0: $i] : c_less(X0,c_Suc(X0),tc_nat),
inference(forward_subsumption_resolution,[status(thm)],[c_10365,c_2898]) ).
tcf(c_10384,plain,
! [X0: $i] :
( c_less(c_minus(X0,c_1,tc_nat),X0,tc_nat)
| ( X0 = c_0 ) ),
inference(superposition,[status(thm)],[c_9353,c_10370]) ).
tcf(c_10385,plain,
c_Suc(c_minus(c_Suc(c_0),c_1,tc_nat)) = c_Suc(c_0),
inference(superposition,[status(thm)],[c_10370,c_9090]) ).
tcf(c_10396,plain,
! [X0: $i,X1: $i] :
( c_less(c_minus(X0,c_plus(X1,c_1,tc_nat),tc_nat),c_minus(X0,X1,tc_nat),tc_nat)
| ( c_minus(X0,X1,tc_nat) = c_0 ) ),
inference(superposition,[status(thm)],[c_2867,c_10384]) ).
tcf(c_10401,plain,
( c_less(c_1,c_Suc(c_1),tc_nat)
| ( c_Suc(c_1) = c_0 ) ),
inference(superposition,[status(thm)],[c_10278,c_10384]) ).
tcf(c_10402,plain,
( ( c_0 = c_1 )
| ( c_minus(c_1,c_1,tc_nat) = c_0 ) ),
inference(superposition,[status(thm)],[c_10384,c_2899]) ).
tcf(c_10410,plain,
! [X0: $i,X1: $i,X2: $i] : c_Nat_Osize(c_List_Olist_OCons(X0,X1,X2),tc_List_Olist(X2)) = c_plus(c_Nat_Osize(X1,tc_List_Olist(X2)),c_1,tc_nat),
inference(light_normalisation,[status(thm)],[c_2888,c_9089]) ).
tcf(c_10411,plain,
! [X0: $i,X1: $i,X2: $i] : c_Nat_Osize(c_List_Olist_OCons(X0,X1,X2),tc_List_Olist(X2)) = c_Suc(c_Nat_Osize(X1,tc_List_Olist(X2))),
inference(demodulation,[status(thm)],[c_10410,c_10126]) ).
tcf(c_10412,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( c_List_Olist_OCons(X2,X0,X1) = c_List_Olist_ONil )
| ( c_Suc(c_Nat_Osize(X0,tc_List_Olist(X1))) != c_0 ) ),
inference(superposition,[status(thm)],[c_10411,c_2893]) ).
tcf(c_10413,plain,
! [X0: $i,X1: $i,X2: $i] :
( c_less(c_0,c_Suc(c_Nat_Osize(X1,tc_List_Olist(X2))),tc_nat)
| ( c_List_Olist_OCons(X0,X1,X2) = c_List_Olist_ONil ) ),
inference(superposition,[status(thm)],[c_10411,c_2889]) ).
tcf(c_10428,plain,
! [X0: $i,X1: $i,X2: $i] :
( ( c_insert(X0,X1,X2) = X1 )
| ~ c_lessequals(c_insert(X0,X1,X2),X1,tc_set(X2)) ),
inference(superposition,[status(thm)],[c_9261,c_2810]) ).
tcf(c_10429,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( ( c_insert(X0,c_insert(X1,X2,X3),X3) = X2 )
| ~ c_lessequals(c_insert(X0,c_insert(X1,X2,X3),X3),X2,tc_set(X3)) ),
inference(superposition,[status(thm)],[c_9272,c_2810]) ).
tcf(c_10440,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c_Wellfounded__Recursion_Owf(c_minus(X3,c_insert(c_Pair(X0,X1,X2,X2),c_emptyset,tc_prod(X2,X2)),tc_set(tc_prod(X2,X2))),X2)
| ~ c_Wellfounded__Recursion_Owf(c_insert(c_Pair(X0,X1,X2,X2),X3,tc_prod(X2,X2)),X2) ),
inference(superposition,[status(thm)],[c_2851,c_2848]) ).
tcf(c_10456,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c_in(X0,c_insert(X0,X2,X3),X3)
| ( X0 = X1 ) ),
inference(superposition,[status(thm)],[c_9273,c_2942]) ).
tcf(c_10457,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i] :
( c_in(X0,c_insert(X2,c_insert(X0,X3,X4),X4),X4)
| ( X0 = X1 ) ),
inference(superposition,[status(thm)],[c_9299,c_2942]) ).
tcf(c_10458,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] :
( c_in(X0,c_minus(X2,c_insert(X1,c_emptyset,X3),tc_set(X3)),X3)
| ( X0 = X1 )
| ~ c_in(X0,c_insert(X1,X2,X3),X3) ),
inference(superposition,[status(thm)],[c_2851,c_2942]) ).
tcf(c_10463,plain,
! [X0: $i,X1: $i] : c_minus(X0,c_plus(X0,X1,tc_nat),tc_nat) = c_0,
inference(demodulation,[status(thm)],[c_9784,c_2870]) ).
tcf(c_10469,plain,
! [X0: $i,X1: $i] :
( c_less(c_0,c_0,tc_nat)
| ~ c_less(c_plus(X0,X1,tc_nat),X0,tc_nat) ),
inference(superposition,[status(thm)],[c_10463,c_2858]) ).
tcf(c_10470,plain,
! [X0: $i,X1: $i,X2: $i] : c_minus(X0,c_plus(c_plus(X0,X1,tc_nat),X2,tc_nat),tc_nat) = c_minus(c_0,X2,tc_nat),
inference(superposition,[status(thm)],[c_10463,c_2867]) ).
tcf(c_10477,plain,
! [X0: $i,X1: $i] : c_lessequals(X0,c_plus(X0,X1,tc_nat),tc_nat),
inference(superposition,[status(thm)],[c_10463,c_2866]) ).
tcf(c_10478,plain,
! [X0: $i,X1: $i] :
( c_less(c_plus(X0,X1,tc_nat),X0,tc_nat)
| ~ c_less(c_0,c_0,tc_nat) ),
inference(superposition,[status(thm)],[c_10463,c_2859]) ).
tcf(c_10480,plain,
! [X0: $i,X1: $i,X2: $i] : c_minus(X0,c_plus(X1,c_plus(c_minus(X0,X1,tc_nat),X2,tc_nat),tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_10463,c_2867]) ).
tcf(c_10481,plain,
! [X0: $i,X1: $i] : ~ c_less(c_plus(X0,X1,tc_nat),X0,tc_nat),
inference(forward_subsumption_resolution,[status(thm)],[c_10469,c_2825]) ).
tcf(c_10487,plain,
! [X0: $i,X1: $i] : c_minus(c_plus(X0,X1,tc_nat),c_minus(c_plus(X0,X1,tc_nat),X0,tc_nat),tc_nat) = X0,
inference(superposition,[status(thm)],[c_10477,c_2875]) ).
tcf(c_10488,plain,
! [X0: $i,X1: $i] : c_plus(c_minus(c_plus(X0,X1,tc_nat),X0,tc_nat),X0,tc_nat) = c_plus(X0,X1,tc_nat),
inference(superposition,[status(thm)],[c_10477,c_2862]) ).
tcf(c_10489,plain,
! [X0: $i,X1: $i] : c_plus(X0,c_minus(c_plus(X0,X1,tc_nat),X0,tc_nat),tc_nat) = c_plus(X0,X1,tc_nat),
inference(superposition,[status(thm)],[c_10477,c_2861]) ).
tcf(c_10503,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : c_lessequals(c_minus(X0,c_plus(X1,c_plus(X2,X3,tc_nat),tc_nat),tc_nat),c_minus(c_minus(X0,X1,tc_nat),X2,tc_nat),tc_nat),
inference(superposition,[status(thm)],[c_2867,c_9815]) ).
tcf(c_10504,plain,
! [X0: $i] : c_lessequals(c_0,c_minus(c_0,X0,tc_nat),tc_nat),
inference(superposition,[status(thm)],[c_2870,c_9815]) ).
tcf(c_10505,plain,
! [X0: $i,X1: $i] : c_lessequals(c_0,c_minus(c_plus(X0,X1,tc_nat),X0,tc_nat),tc_nat),
inference(superposition,[status(thm)],[c_2863,c_9815]) ).
tcf(c_10506,plain,
! [X0: $i,X1: $i] :
( c_lessequals(c_0,c_minus(c_1,X0,tc_nat),tc_nat)
| ( c_plus(X0,X1,tc_nat) = c_0 ) ),
inference(superposition,[status(thm)],[c_8564,c_9815]) ).
tcf(c_10507,plain,
! [X0: $i,X1: $i] : c_lessequals(c_0,c_minus(X0,X1,tc_nat),tc_nat),
inference(superposition,[status(thm)],[c_8590,c_9815]) ).
tcf(c_10511,plain,
! [X0: $i] : c_lessequals(c_0,c_minus(X0,X0,tc_nat),tc_nat),
inference(superposition,[status(thm)],[c_10463,c_9815]) ).
tcf(c_10512,plain,
! [X0: $i,X1: $i] : c_lessequals(c_1,c_minus(c_Suc(c_plus(X0,X1,tc_nat)),X0,tc_nat),tc_nat),
inference(superposition,[status(thm)],[c_10278,c_9815]) ).
tcf(c_10513,plain,
! [X0: $i,X1: $i] : c_lessequals(c_minus(X0,X1,tc_nat),c_minus(X0,X1,tc_nat),tc_nat),
inference(superposition,[status(thm)],[c_10022,c_9815]) ).
tcf(c_10514,plain,
! [X0: $i,X1: $i] : c_lessequals(c_minus(X0,X1,tc_nat),c_minus(X0,c_0,tc_nat),tc_nat),
inference(superposition,[status(thm)],[c_10023,c_9815]) ).
tcf(c_10515,plain,
! [X0: $i,X1: $i] : c_lessequals(c_minus(X0,c_Suc(X1),tc_nat),c_minus(X0,X1,tc_nat),tc_nat),
inference(superposition,[status(thm)],[c_10126,c_9815]) ).
tcf(c_10516,plain,
! [X0: $i,X1: $i] : c_lessequals(c_minus(X0,c_Suc(X1),tc_nat),c_minus(X0,c_1,tc_nat),tc_nat),
inference(superposition,[status(thm)],[c_10024,c_9815]) ).
tcf(c_10517,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : c_lessequals(c_minus(c_minus(X0,X1,tc_nat),c_plus(X2,X3,tc_nat),tc_nat),c_minus(X0,c_plus(X1,X2,tc_nat),tc_nat),tc_nat),
inference(superposition,[status(thm)],[c_2867,c_9815]) ).
tcf(c_10518,plain,
! [X0: $i,X1: $i] : c_lessequals(c_minus(c_0,c_plus(X0,X1,tc_nat),tc_nat),c_0,tc_nat),
inference(superposition,[status(thm)],[c_2870,c_9815]) ).
tcf(c_10519,plain,
! [X0: $i,X1: $i,X2: $i] : c_lessequals(c_minus(c_Suc(X0),c_plus(c_Suc(X1),X2,tc_nat),tc_nat),c_minus(X0,X1,tc_nat),tc_nat),
inference(superposition,[status(thm)],[c_2869,c_9815]) ).
tcf(c_10520,plain,
! [X0: $i,X1: $i] : c_lessequals(c_minus(X0,c_plus(X0,X1,tc_nat),tc_nat),c_0,tc_nat),
inference(superposition,[status(thm)],[c_2863,c_9815]) ).
tcf(c_10521,plain,
! [X0: $i,X1: $i] : c_lessequals(c_minus(X0,c_plus(c_0,X1,tc_nat),tc_nat),X0,tc_nat),
inference(superposition,[status(thm)],[c_2860,c_9815]) ).
tcf(c_10522,plain,
! [X0: $i,X1: $i] :
( c_lessequals(c_minus(c_1,c_plus(X0,X1,tc_nat),tc_nat),c_0,tc_nat)
| ( X0 = c_0 ) ),
inference(superposition,[status(thm)],[c_8564,c_9815]) ).
tcf(c_10523,plain,
! [X0: $i,X1: $i,X2: $i] : c_lessequals(c_minus(X0,c_plus(c_plus(X1,X0,tc_nat),X2,tc_nat),tc_nat),c_0,tc_nat),
inference(superposition,[status(thm)],[c_8590,c_9815]) ).
tcf(c_10524,plain,
! [X0: $i,X1: $i] : c_lessequals(c_minus(X0,c_plus(c_Suc(X0),X1,tc_nat),tc_nat),c_0,tc_nat),
inference(superposition,[status(thm)],[c_8660,c_9815]) ).
tcf(c_10525,plain,
! [X0: $i,X1: $i] : c_lessequals(c_minus(X0,c_plus(c_Suc(c_Suc(X0)),X1,tc_nat),tc_nat),c_0,tc_nat),
inference(superposition,[status(thm)],[c_8688,c_9815]) ).
tcf(c_10526,plain,
! [X0: $i,X1: $i] : c_lessequals(c_minus(X0,c_plus(c_Suc(c_Suc(c_Suc(X0))),X1,tc_nat),tc_nat),c_0,tc_nat),
inference(superposition,[status(thm)],[c_8713,c_9815]) ).
tcf(c_10527,plain,
! [X0: $i,X1: $i,X2: $i] : c_lessequals(c_minus(X0,c_plus(c_plus(X1,c_Suc(X0),tc_nat),X2,tc_nat),tc_nat),c_0,tc_nat),
inference(superposition,[status(thm)],[c_8761,c_9815]) ).
tcf(c_10528,plain,
! [X0: $i,X1: $i] : c_lessequals(c_minus(X0,c_plus(c_Suc(c_Suc(c_Suc(c_Suc(X0)))),X1,tc_nat),tc_nat),c_0,tc_nat),
inference(superposition,[status(thm)],[c_8788,c_9815]) ).
tcf(c_10529,plain,
! [X0: $i,X1: $i] : c_lessequals(c_minus(c_1,c_plus(c_Suc(X0),X1,tc_nat),tc_nat),c_0,tc_nat),
inference(superposition,[status(thm)],[c_8853,c_9815]) ).
tcf(c_10530,plain,
! [X0: $i,X1: $i,X2: $i] : c_lessequals(c_minus(X0,c_plus(c_plus(X1,c_Suc(c_Suc(X0)),tc_nat),X2,tc_nat),tc_nat),c_0,tc_nat),
inference(superposition,[status(thm)],[c_8872,c_9815]) ).
tcf(c_10531,plain,
! [X0: $i,X1: $i] : c_lessequals(c_minus(X0,c_plus(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0))))),X1,tc_nat),tc_nat),c_0,tc_nat),
inference(superposition,[status(thm)],[c_8903,c_9815]) ).
tcf(c_10532,plain,
! [X0: $i,X1: $i,X2: $i] : c_lessequals(c_minus(X0,c_plus(c_plus(X1,c_Suc(c_Suc(c_Suc(X0))),tc_nat),X2,tc_nat),tc_nat),c_0,tc_nat),
inference(superposition,[status(thm)],[c_8980,c_9815]) ).
tcf(c_10533,plain,
! [X0: $i,X1: $i] : c_lessequals(c_minus(X0,c_plus(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(c_Suc(X0)))))),X1,tc_nat),tc_nat),c_0,tc_nat),
inference(superposition,[status(thm)],[c_9015,c_9815]) ).
tcf(c_10534,plain,
! [X0: $i,X1: $i] : c_lessequals(c_minus(c_Suc(X0),c_plus(c_1,X1,tc_nat),tc_nat),X0,tc_nat),
inference(superposition,[status(thm)],[c_9144,c_9815]) ).
tcf(c_10535,plain,
! [X0: $i,X1: $i,X2: $i] : c_lessequals(c_minus(X0,c_plus(c_plus(X0,X1,tc_nat),X2,tc_nat),tc_nat),c_0,tc_nat),
inference(superposition,[status(thm)],[c_10463,c_9815]) ).
tcf(c_10536,plain,
! [X0: $i,X1: $i] : c_lessequals(c_minus(c_Suc(X0),c_plus(X0,X1,tc_nat),tc_nat),c_1,tc_nat),
inference(superposition,[status(thm)],[c_10278,c_9815]) ).
tcf(c_10537,plain,
! [X0: $i,X1: $i,X2: $i] : c_minus(c_minus(X0,X1,tc_nat),c_minus(c_minus(X0,X1,tc_nat),c_minus(X0,c_plus(X1,X2,tc_nat),tc_nat),tc_nat),tc_nat) = c_minus(X0,c_plus(X1,X2,tc_nat),tc_nat),
inference(superposition,[status(thm)],[c_9815,c_2875]) ).
tcf(c_10538,plain,
! [X0: $i,X1: $i,X2: $i] : c_plus(c_minus(c_minus(X0,X1,tc_nat),c_minus(X0,c_plus(X1,X2,tc_nat),tc_nat),tc_nat),c_minus(X0,c_plus(X1,X2,tc_nat),tc_nat),tc_nat) = c_minus(X0,X1,tc_nat),
inference(superposition,[status(thm)],[c_9815,c_2862]) ).
tcf(c_10539,plain,
! [X0: $i,X1: $i,X2: $i] : c_plus(c_minus(X0,c_plus(X1,X2,tc_nat),tc_nat),c_minus(c_minus(X0,X1,tc_nat),c_minus(X0,c_plus(X1,X2,tc_nat),tc_nat),tc_nat),tc_nat) = c_minus(X0,X1,tc_nat),
inference(superposition,[status(thm)],[c_9815,c_2861]) ).
tcf(c_10540,plain,
! [X0: $i,X1: $i,X2: $i] : c_minus(c_minus(X0,c_plus(X1,X2,tc_nat),tc_nat),c_minus(X0,X1,tc_nat),tc_nat) = c_0,
inference(superposition,[status(thm)],[c_9815,c_2865]) ).
tcf(c_10545,plain,
! [X0: $i] : c_lessequals(c_minus(c_1,X0,tc_nat),c_1,tc_nat),
inference(light_normalisation,[status(thm)],[c_10536,c_10357]) ).
tcf(c_10574,plain,
! [X0: $i,X1: $i,X2: $i,X3: $i] : c_lessequals(c_minus(X0,c_plus(X1,c_plus(X2,X3,tc_nat),tc_nat),tc_nat),c_minus(X0,c_plus(X1,X2,tc_nat),tc_nat),tc_nat),
inference(light_normalisation,[status(thm)],[c_10503,c_2867]) ).
tcf(c_10592,plain,
$false,
inference(smt_impl_just,[status(thm)],[c_10574,c_10545,c_10540,c_10539,c_10538,c_10537,c_10536,c_10535,c_10534,c_10533,c_10532,c_10531,c_10530,c_10529,c_10528,c_10527,c_10526,c_10525,c_10524,c_10523,c_10522,c_10521,c_10520,c_10519,c_10518,c_10517,c_10516,c_10515,c_10514,c_10513,c_10512,c_10511,c_10507,c_10506,c_10505,c_10504,c_10503,c_10489,c_10488,c_10487,c_10481,c_10478,c_10477,c_10470,c_10469,c_10480,c_10463,c_10458,c_10457,c_10456,c_10440,c_10429,c_10428,c_10413,c_10412,c_10411,c_10410,c_10402,c_10401,c_10396,c_10385,c_10384,c_10370,c_10368,c_10365,c_10363,c_10362,c_10361,c_10360,c_10359,c_10358,c_10357,c_10355,c_10354,c_10345,c_10343,c_10341,c_10278,c_10275,c_10274,c_10273,c_10272,c_10271,c_10270,c_10269,c_10268,c_10267,c_10266,c_10265,c_10264,c_10263,c_10262,c_10261,c_10260,c_10259,c_10258,c_10257,c_10256,c_10255,c_10254,c_10253,c_10252,c_10226,c_10225,c_10222,c_10221,c_10220,c_10219,c_10218,c_10217,c_10216,c_10215,c_10224,c_10223,c_10126,c_10123,c_10122,c_10121,c_10120,c_10119,c_10118,c_10117,c_10116,c_10115,c_10114,c_10113,c_10112,c_10111,c_10110,c_10109,c_10108,c_10107,c_10106,c_10105,c_10104,c_10103,c_10102,c_10101,c_10100,c_10024,c_10023,c_10022,c_10021,c_10020,c_10019,c_10018,c_10017,c_10016,c_10015,c_10014,c_10013,c_10012,c_10011,c_10010,c_10009,c_10008,c_10007,c_10006,c_10005,c_10004,c_10003,c_10002,c_10001,c_10000,c_9999,c_9998,c_9997,c_9972,c_9971,c_9969,c_9968,c_9967,c_9966,c_9839,c_9816,c_9815,c_9814,c_9813,c_9812,c_9811,c_9810,c_9809,c_9808,c_9807,c_9805,c_9804,c_9803,c_9802,c_9801,c_9800,c_9799,c_9798,c_9797,c_9796,c_9795,c_9794,c_9793,c_9792,c_9791,c_9790,c_9789,c_9788,c_9787,c_9786,c_9785,c_9784,c_9783,c_9782,c_9806,c_9830,c_9829,c_9828,c_9827,c_9826,c_9825,c_9824,c_9823,c_9822,c_9821,c_9820,c_9819,c_9818,c_9817,c_9764,c_9762,c_9761,c_9754,c_9752,c_9749,c_9737,c_9735,c_9734,c_9727,c_9675,c_9674,c_9673,c_9672,c_9671,c_9670,c_9669,c_9668,c_9667,c_9666,c_9665,c_9664,c_9663,c_9662,c_9661,c_9660,c_9659,c_9658,c_9657,c_9656,c_9655,c_9648,c_9641,c_9639,c_9599,c_9597,c_9596,c_9595,c_9594,c_9593,c_9592,c_9591,c_9589,c_9582,c_9552,c_9551,c_9549,c_9540,c_9526,c_9515,c_9514,c_9406,c_9405,c_9404,c_9403,c_9402,c_9401,c_9400,c_9399,c_9398,c_9397,c_9396,c_9395,c_9394,c_9393,c_9392,c_9391,c_9390,c_9389,c_9388,c_9387,c_9386,c_9385,c_9384,c_9383,c_9379,c_9378,c_9377,c_9376,c_9375,c_9374,c_9373,c_9372,c_9371,c_9370,c_9369,c_9368,c_9367,c_9366,c_9365,c_9364,c_9363,c_9353,c_9351,c_9350,c_9345,c_9339,c_9337,c_9324,c_9323,c_9322,c_9313,c_9312,c_9299,c_9298,c_9297,c_9296,c_9295,c_9294,c_9290,c_9288,c_9287,c_9282,c_9280,c_9279,c_9273,c_9272,c_9271,c_9270,c_9269,c_9268,c_9262,c_9261,c_9252,c_9246,c_9245,c_9244,c_9232,c_9231,c_9224,c_9223,c_9222,c_9210,c_9205,c_9202,c_9201,c_9199,c_9198,c_9200,c_9196,c_9194,c_9183,c_9182,c_9161,c_9160,c_9154,c_9153,c_9144,c_9139,c_9138,c_9137,c_9136,c_9135,c_9134,c_9133,c_9131,c_9130,c_9129,c_9127,c_9126,c_9125,c_9123,c_9122,c_9121,c_9120,c_9119,c_9117,c_9116,c_9112,c_9111,c_9110,c_9108,c_9107,c_9106,c_9105,c_9104,c_9102,c_9101,c_9094,c_9093,c_9092,c_9091,c_9090,c_9089,c_9084,c_9083,c_9070,c_9069,c_9068,c_9067,c_9066,c_9065,c_9058,c_9049,c_9030,c_9026,c_9018,c_9015,c_9011,c_9009,c_9006,c_8999,c_8998,c_9010,c_8996,c_8990,c_8988,c_8987,c_8981,c_8980,c_8978,c_8977,c_8976,c_8974,c_8973,c_8972,c_8971,c_8970,c_8969,c_8968,c_8958,c_8931,c_8930,c_8929,c_8917,c_8913,c_8906,c_8903,c_8899,c_8897,c_8890,c_8889,c_8898,c_8887,c_8881,c_8879,c_8878,c_8873,c_8872,c_8867,c_8865,c_8864,c_8863,c_8862,c_8861,c_8860,c_8859,c_8858,c_8853,c_8851,c_8844,c_8831,c_8830,c_8825,c_8824,c_8813,c_8808,c_8805,c_8799,c_8796,c_8788,c_8784,c_8778,c_8777,c_8779,c_8775,c_8769,c_8767,c_8766,c_8762,c_8761,c_8758,c_8755,c_8750,c_8730,c_8729,c_8713,c_8709,c_8705,c_8704,c_8706,c_8702,c_8698,c_8695,c_8691,c_8688,c_8684,c_8681,c_8680,c_8682,c_8678,c_8669,c_8666,c_8663,c_8660,c_8656,c_8654,c_8653,c_8655,c_8651,c_8623,c_8622,c_8621,c_8620,c_8605,c_8604,c_8603,c_8594,c_8592,c_8591,c_8590,c_8587,c_8580,c_8579,c_8566,c_8564,c_8555,c_8554,c_8552,c_8539,c_8518,c_8488,c_4376,c_2952,c_2951,c_2950,c_2943,c_2942,c_2941,c_2940,c_2944,c_2938,c_2937,c_2936,c_2935,c_2934,c_2933,c_2887,c_2886,c_2884,c_2885,c_2857,c_2856,c_2855,c_2854,c_2853,c_2802,c_2800,c_2818,c_2819,c_2820,c_2829,c_2830,c_2845,c_2846,c_2847,c_2848,c_9177,c_2816,c_2817,c_2851,c_2852,c_2831,c_2832,c_2833,c_2834,c_2835,c_2836,c_2841,c_2849,c_2850,c_2901,c_2902,c_2904,c_2905,c_2906,c_2907,c_2908,c_2909,c_2858,c_2859,c_2860,c_2825,c_8852,c_2827,c_2898,c_2899,c_2861,c_2862,c_8490,c_2808,c_2863,c_2864,c_2865,c_2866,c_2867,c_2868,c_2869,c_2870,c_2871,c_2873,c_2874,c_2875,c_2876,c_2877,c_2878,c_2879,c_2888,c_2889,c_2891,c_2892,c_2893,c_2894,c_2895,c_2896,c_2897,c_2918,c_2919,c_2920,c_2921,c_2922,c_2923,c_2924,c_2925,c_2916,c_2917,c_2900,c_2880,c_2881,c_2882,c_2945,c_2946,c_2947,c_2839,c_2840,c_2842,c_2828,c_2804,c_2843,c_2948,c_2949,c_2837,c_2838,c_2809,c_2810,c_2799,c_2928,c_2811,c_2812,c_2813,c_2814,c_2824,c_2806,c_2844,c_2929,c_2793,c_2798,c_2797,c_2794,c_2801,c_2805,c_2795,c_2796]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : LAT278-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.12/15.39 % Computer : n016.cluster.edu
% 0.12/15.39 % Model : x86_64 x86_64
% 0.12/15.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/15.39 % Memory : 8046.5625MB
% 0.12/15.39 % OS : Linux 6.8.0-71-generic
% 0.12/15.39 % CPULimit : 300
% 0.12/15.39 % WCLimit : 300
% 0.12/15.39 % DateTime : Wed Sep 23 20:52:13 UTC 2026
% 0.12/15.40 % CPUTime :
% 0.12/15.40 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.16/15.43 Running first-order theorem proving
% 0.16/15.43 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s fof_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.16/15.45
% 0.16/15.45 % ======== iProver multi-core TPTP/SMT =========
% 0.16/15.45
% 0.16/15.45 % Detected problem language: tptp
% 0.16/15.46 % Proving...
% 6.31/16.76 % SZS status Started for theBenchmark.p
% 6.31/16.76 % SZS status Unsatisfiable for theBenchmark.p
% 6.31/16.76
% 6.31/16.76 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 6.31/16.76
% 6.31/16.76 % ------ iProver source info
% 6.31/16.76
% 6.31/16.76 % git: date: 2026-07-19 20:42:38 +0200
% 6.31/16.76 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 6.31/16.76 % git: non_committed_changes: false
% 6.31/16.76
% 6.31/16.76 % ------ Parsing...% successful
% 6.31/16.76
% 6.31/16.76
% 6.31/16.76 % ------ Clausification by vclausify_rel & Parsing by iProver...%
% 6.31/16.76
% 6.31/16.76 % ------ Preprocessing... sup_sim: 3 sf_s rm: 13 0s sf_e pe_s pe_e sup_sim: 0 sf_s rm: 3 0s sf_e pe_s pe_e %
% 6.31/16.76
% 6.31/16.76 % ------ Preprocessing... gs_s sp: 0 0s gs_e snvd_s sp: 0 0s snvd_e %
% 6.31/16.76
% 6.31/16.76 % ------ Preprocessing... sf_s rm: 1 0s sf_e sf_s rm: 0 0s sf_e
% 6.31/16.76 % ------ Proving...
% 6.31/16.76 % ------ Problem Properties
% 6.31/16.76
% 6.31/16.76 %
% 6.31/16.76 % clauses 138
% 6.31/16.76 % conjectures 1
% 6.31/16.76 % EPR 13
% 6.31/16.76 % Horn 125
% 6.31/16.76 % unary 53
% 6.31/16.76 % binary 66
% 6.31/16.76 % lits 243
% 6.31/16.76 % lits eq 100
% 6.31/16.76 % fd_pure 0
% 6.31/16.76 % fd_pseudo 0
% 6.31/16.76 % fd_cond 8
% 6.31/16.76 % fd_pseudo_cond 18
% 6.31/16.76 % AC symbols 0
% 6.31/16.76
% 6.31/16.76 % ------ Schedule dynamic 5 is on
% 6.31/16.76
% 6.31/16.76 % ------ Input Options "--resolution_flag false --inst_lit_sel_side none" Time Limit: 10.
% 6.31/16.76
% 6.31/16.76
% 6.31/16.76 % ------
% 6.31/16.76 % Current options:
% 6.31/16.76 % ------
% 6.31/16.76
% 6.31/16.76
% 6.31/16.76 %
% 6.31/16.76
% 6.31/16.76 % ------ Proving...
% 6.31/16.76 %
% 6.31/16.76
% 6.31/16.76 % SZS status Unsatisfiable for theBenchmark.p
% 6.31/16.76
% 6.31/16.76 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 6.31/16.77
% 6.31/16.77
%------------------------------------------------------------------------------