%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV575-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:19:00 PM UTC 2026
% Result : Unsatisfiable 49.50s 8.93s
% Output : Refutation 58.67s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 73
% Syntax : Number of formulae : 439 ( 236 unt; 20 def)
% Number of atoms : 780 ( 546 equ)
% Maximal formula atoms : 8 ( 1 avg)
% Number of connectives : 501 ( 160 ~; 332 |; 0 &)
% ( 9 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 13 ( 11 usr; 10 prp; 0-2 aty)
% Number of functors : 30 ( 30 usr; 15 con; 0-3 aty)
% Number of variables : 226 ( 0 sgn 226 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f110,axiom,
! [X0] : c_Int_Onumber__class_Onumber__of(X0,tc_Int_Oint) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_number__of__is__id_0) ).
fof(f151,axiom,
! [X0] : c_HOL_Ominus__class_Ominus(hAPP(c_Suc,X0),c_HOL_Oone__class_Oone(tc_nat),tc_nat) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_diff__Suc__1_0) ).
fof(f313,axiom,
! [X0] : hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),X0),c_HOL_Oone__class_Oone(tc_nat)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat__mult__1__right_0) ).
fof(f320,axiom,
! [X0] : hAPP(c_Suc,X0) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Suc__eq__plus1__left_0) ).
fof(f321,axiom,
! [X0] : hAPP(c_Suc,X0) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),c_HOL_Oone__class_Oone(tc_nat)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Suc__eq__plus1_0) ).
fof(f403,axiom,
! [X2,X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(X0,X1,tc_nat),X2,tc_nat) = c_HOL_Ominus__class_Ominus(X0,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X1),X2),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_diff__diff__left_0) ).
fof(f420,axiom,
! [X2,X0,X1] :
( hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),hAPP(hAPP(c_HOL_Otimes__class_Otimes(X0),X1),c_Divides_Odiv__class_Odiv(X2,X1,X0))),c_Divides_Odiv__class_Omod(X2,X1,X0)) = X2
| ~ class_Divides_Osemiring__div(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mod__div__equality2_0) ).
fof(f487,axiom,
~ c_Parity_Oeven__odd__class_Oeven(c_HOL_Oone__class_Oone(tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_odd__1__nat_0) ).
fof(f695,axiom,
! [X0,X1] : c_HOL_Ominus__class_Ominus(X0,hAPP(c_Suc,X1),tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat),X1,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_diff__Suc__eq__diff__pred_0) ).
fof(f860,axiom,
! [X0] :
( c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) != c_HOL_Oone__class_Oone(tc_nat)
| c_Parity_Oeven__odd__class_Oeven(c_Divides_Odiv__class_Odiv(c_HOL_Ominus__class_Ominus(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_nat),tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_lemma__even__mod__4__div__2_0) ).
fof(f861,plain,
! [X0] :
( c_HOL_Oone__class_Oone(tc_nat) != c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat)
| c_Parity_Oeven__odd__class_Oeven(c_Divides_Odiv__class_Odiv(c_HOL_Ominus__class_Ominus(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_nat),tc_nat) ),
inference(reorient_equations,[],[f860]) ).
fof(f899,axiom,
! [X0,X1] :
( ~ class_Divides_Osemiring__div(X0)
| c_Divides_Odiv__class_Omod(X1,X1,X0) = c_HOL_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mod__self_0) ).
fof(f900,plain,
! [X0,X1] :
( c_HOL_Ozero__class_Ozero(X0) = c_Divides_Odiv__class_Omod(X1,X1,X0)
| ~ class_Divides_Osemiring__div(X0) ),
inference(reorient_equations,[],[f899]) ).
fof(f954,axiom,
! [X0] :
( hAPP(c_Suc,hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),hAPP(c_Suc,hAPP(c_Suc,c_HOL_Ozero__class_Ozero(tc_nat)))),c_Divides_Odiv__class_Odiv(X0,hAPP(c_Suc,hAPP(c_Suc,c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat))) = X0
| c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_odd__nat__div__two__times__two__plus__one_0) ).
fof(f1164,axiom,
! [X0] : hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),X0),c_HOL_Ozero__class_Ozero(tc_nat)) = c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mult__is__0_2) ).
fof(f1165,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_nat) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),X0),c_HOL_Ozero__class_Ozero(tc_nat)),
inference(reorient_equations,[],[f1164]) ).
fof(f1166,axiom,
c_Parity_Oeven__odd__class_Oeven(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_even__zero__nat_0) ).
fof(f1186,axiom,
! [X0] : c_HOL_Ominus__class_Ominus(X0,X0,tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_diff__self__eq__0_0) ).
fof(f1187,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_nat) = c_HOL_Ominus__class_Ominus(X0,X0,tc_nat),
inference(reorient_equations,[],[f1186]) ).
fof(f1191,axiom,
! [X0,X1] : c_Divides_Odiv__class_Omod(X0,X1,tc_nat) = c_HOL_Ominus__class_Ominus(X0,hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Divides_Odiv__class_Odiv(X0,X1,tc_nat)),X1),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Divides_Omod__div__equality_H_0) ).
fof(f1202,axiom,
! [X0,X1] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X1),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat__add__commute_0) ).
fof(f1309,axiom,
! [X0] : c_HOL_Ominus__class_Ominus(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_minus__nat_Odiff__0_0) ).
fof(f1316,axiom,
! [X0] : c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_diff__0__eq__0_0) ).
fof(f1317,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat),
inference(reorient_equations,[],[f1316]) ).
fof(f1320,axiom,
! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),c_HOL_Ozero__class_Ozero(tc_nat)) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Nat_Oadd__0__right_0) ).
fof(f1321,axiom,
! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_plus__nat_Oadd__0_0) ).
fof(f1346,axiom,
! [X0,X1] : c_Divides_Odiv__class_Omod(hAPP(c_Suc,X0),X1,tc_nat) = c_Divides_Odiv__class_Omod(hAPP(c_Suc,c_Divides_Odiv__class_Omod(X0,X1,tc_nat)),X1,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mod__Suc__eq__Suc__mod_0) ).
fof(f1350,axiom,
! [X0,X1] : c_HOL_Ominus__class_Ominus(hAPP(c_Suc,X0),hAPP(c_Suc,X1),tc_nat) = c_HOL_Ominus__class_Ominus(X0,X1,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_diff__Suc__Suc_0) ).
fof(f1351,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(X0,X1,tc_nat) = c_HOL_Ominus__class_Ominus(hAPP(c_Suc,X0),hAPP(c_Suc,X1),tc_nat),
inference(reorient_equations,[],[f1350]) ).
fof(f1374,axiom,
! [X0,X1] :
( c_Divides_Odiv__class_Omod(hAPP(c_Suc,X0),X1,tc_nat) = hAPP(c_Suc,c_Divides_Odiv__class_Omod(X0,X1,tc_nat))
| hAPP(c_Suc,c_Divides_Odiv__class_Omod(X0,X1,tc_nat)) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mod__Suc_1) ).
fof(f1376,axiom,
! [X0] :
( ~ c_Parity_Oeven__odd__class_Oeven(hAPP(c_Suc,X0),tc_nat)
| ~ c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_even__Suc_0) ).
fof(f1377,axiom,
! [X0] :
( c_Parity_Oeven__odd__class_Oeven(hAPP(c_Suc,X0),tc_nat)
| c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_even__Suc_1) ).
fof(f1392,axiom,
! [X0] :
( c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),c_HOL_Oone__class_Oone(tc_nat)),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_nat) = c_Divides_Odiv__class_Odiv(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_nat)
| ~ c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_lemma__even__div2_0) ).
fof(f1472,axiom,
! [X0] : c_Int_Onat(c_Int_Onumber__class_Onumber__of(X0,tc_Int_Oint)) = c_Int_Onumber__class_Onumber__of(X0,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat__number__of_0) ).
fof(f1473,plain,
! [X0] : c_Int_Onumber__class_Onumber__of(X0,tc_nat) = c_Int_Onat(c_Int_Onumber__class_Onumber__of(X0,tc_Int_Oint)),
inference(reorient_equations,[],[f1472]) ).
fof(f1602,axiom,
c_HOL_Oone__class_Oone(tc_nat) = hAPP(c_Suc,c_HOL_Ozero__class_Ozero(tc_nat)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_One__nat__def_0) ).
fof(f1603,axiom,
hAPP(c_Suc,c_HOL_Ozero__class_Ozero(tc_nat)) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),hAPP(c_Suc,c_HOL_Ozero__class_Ozero(tc_nat))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_one__is__add_5) ).
fof(f1666,axiom,
c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat) = c_Int_Onat(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_Int_Oint)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_transfer__nat__int__numerals_I3_J_0) ).
fof(f1667,axiom,
! [X0] : c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X0),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_nat) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_add__self__div__2_0) ).
fof(f1736,axiom,
! [X0,X1] : c_Divides_Odiv__class_Omod(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),X0),X1),X0,tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mod__eq__0__iff_1) ).
fof(f1737,plain,
! [X0,X1] : c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),X0),X1),X0,tc_nat),
inference(reorient_equations,[],[f1736]) ).
fof(f1817,axiom,
! [X0] :
( c_Parity_Oeven__odd__class_Oeven(X0,tc_nat)
| ~ c_Parity_Oeven__odd__class_Oeven(c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat),tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_even__even__mod__4__iff_1) ).
fof(f1822,axiom,
! [X0] : hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),X0),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat__mult__2__right_0) ).
fof(f1823,plain,
! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X0) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),X0),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)),
inference(reorient_equations,[],[f1822]) ).
fof(f1832,axiom,
! [X0] : c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) = c_SetInterval_Oord__class_OlessThan(X0,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_atLeast0LessThan_0) ).
fof(f1833,axiom,
! [X0,X1] : c_SetInterval_Oord__class_OatLeastLessThan(X0,hAPP(c_Suc,X1),tc_nat) = c_SetInterval_Oord__class_OatLeastAtMost(X0,X1,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_atLeastLessThanSuc__atLeastAtMost_0) ).
fof(f1834,plain,
! [X0,X1] : c_SetInterval_Oord__class_OatLeastAtMost(X0,X1,tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(X0,hAPP(c_Suc,X1),tc_nat),
inference(reorient_equations,[],[f1833]) ).
fof(f1857,axiom,
! [X0] :
( c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) = c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OBit1(c_Int_OPls)),tc_nat)
| c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) = c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)
| c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) = c_HOL_Oone__class_Oone(tc_nat)
| c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mod__exhaust__less__4_0) ).
fof(f1858,plain,
! [X0] :
( c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) = c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OBit1(c_Int_OPls)),tc_nat)
| c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) = c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)
| c_HOL_Oone__class_Oone(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) ),
inference(reorient_equations,[],[f1857]) ).
fof(f1888,axiom,
! [X0] :
( hAPP(c_Suc,hAPP(c_Suc,c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat)),X0),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_nat))) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat)),X0)
| X0 = c_HOL_Ozero__class_Ozero(tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_lemma__Suc__Suc__4n__diff__2_0) ).
fof(f1889,plain,
! [X0] :
( hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat)),X0) = hAPP(c_Suc,hAPP(c_Suc,c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat)),X0),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_nat)))
| c_HOL_Ozero__class_Ozero(tc_nat) = X0 ),
inference(reorient_equations,[],[f1888]) ).
fof(f1892,axiom,
c_HOL_Oone__class_Oone(tc_nat) = c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OPls),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Numeral1__eq1__nat_0) ).
fof(f1895,axiom,
! [X0] : hAPP(c_Suc,hAPP(c_Suc,hAPP(c_Suc,X0))) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OBit1(c_Int_OPls)),tc_nat)),X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Suc3__eq__add__3_0) ).
fof(f1904,axiom,
! [X0] : c_Divides_Odiv__class_Odiv(hAPP(c_Suc,hAPP(c_Suc,X0)),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_nat) = hAPP(c_Suc,c_Divides_Odiv__class_Odiv(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_nat)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_div2__Suc__Suc_0) ).
fof(f1905,plain,
! [X0] : hAPP(c_Suc,c_Divides_Odiv__class_Odiv(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_nat)) = c_Divides_Odiv__class_Odiv(hAPP(c_Suc,hAPP(c_Suc,X0)),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_nat),
inference(reorient_equations,[],[f1904]) ).
fof(f1906,axiom,
! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)),X0) = hAPP(c_Suc,hAPP(c_Suc,X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_add__2__eq__Suc_0) ).
fof(f1907,plain,
! [X0] : hAPP(c_Suc,hAPP(c_Suc,X0)) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)),X0),
inference(reorient_equations,[],[f1906]) ).
fof(f1910,axiom,
! [X0] : c_Divides_Odiv__class_Omod(hAPP(c_Suc,hAPP(c_Suc,X0)),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_mod2__Suc__Suc_0) ).
fof(f1911,plain,
! [X0] : c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_nat) = c_Divides_Odiv__class_Omod(hAPP(c_Suc,hAPP(c_Suc,X0)),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_nat),
inference(reorient_equations,[],[f1910]) ).
fof(f1920,axiom,
c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OPls),tc_nat) = hAPP(c_Suc,c_HOL_Ozero__class_Ozero(tc_nat)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_numeral__1__eq__Suc__0_0) ).
fof(f1921,plain,
hAPP(c_Suc,c_HOL_Ozero__class_Ozero(tc_nat)) = c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OPls),tc_nat),
inference(reorient_equations,[],[f1920]) ).
fof(f1924,axiom,
c_Int_Onumber__class_Onumber__of(c_Int_OPls,tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat__number__of__Pls_0) ).
fof(f1925,plain,
c_HOL_Ozero__class_Ozero(tc_nat) = c_Int_Onumber__class_Onumber__of(c_Int_OPls,tc_nat),
inference(reorient_equations,[],[f1924]) ).
fof(f1929,axiom,
! [X0,X1] :
( hAPP(c_Suc,X0) != hAPP(c_Suc,X1)
| X0 = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat_Oinject_0) ).
fof(f1940,axiom,
c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OBit1(c_Int_OPls)),tc_nat) = hAPP(c_Suc,hAPP(c_Suc,hAPP(c_Suc,c_HOL_Ozero__class_Ozero(tc_nat)))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_numeral__3__eq__3_0) ).
fof(f1942,axiom,
! [X0] : X0 != hAPP(c_Suc,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_n__not__Suc__n_0) ).
fof(f1943,plain,
! [X0] : hAPP(c_Suc,X0) != X0,
inference(reorient_equations,[],[f1942]) ).
fof(f1947,axiom,
! [X0] : c_HOL_Ozero__class_Ozero(tc_nat) != hAPP(c_Suc,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Zero__neq__Suc_0) ).
fof(f1948,plain,
! [X0] : hAPP(c_Suc,X0) != c_HOL_Ozero__class_Ozero(tc_nat),
inference(reorient_equations,[],[f1947]) ).
fof(f1951,axiom,
hAPP(c_Suc,hAPP(c_Suc,c_HOL_Ozero__class_Ozero(tc_nat))) = c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_comp__arith_I115_J_0) ).
fof(f1955,negated_conjecture,
c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) != c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),hAPP(c_Suc,hAPP(c_Suc,hAPP(c_Suc,hAPP(c_Suc,c_HOL_Ozero__class_Ozero(tc_nat))))),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1988,axiom,
class_Divides_Osemiring__div(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_nat__Divides_Osemiring__div) ).
fof(f2057,definition,
sF0 = c_HOL_Ozero__class_Ozero(tc_nat),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f2058,plain,
c_HOL_Ozero__class_Ozero(tc_nat) = sF0,
inference(reorient_equations,[],[f2057]) ).
fof(f2059,definition,
sF1 = c_Int_OBit1(c_Int_OPls),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f2060,plain,
c_Int_OBit1(c_Int_OPls) = sF1,
inference(reorient_equations,[],[f2059]) ).
fof(f2061,definition,
sF2 = c_Int_OBit0(sF1),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f2062,plain,
c_Int_OBit0(sF1) = sF2,
inference(reorient_equations,[],[f2061]) ).
fof(f2063,definition,
sF3 = c_Int_OBit0(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f2064,plain,
c_Int_OBit0(sF2) = sF3,
inference(reorient_equations,[],[f2063]) ).
fof(f2065,definition,
sF4 = c_Int_Onumber__class_Onumber__of(sF3,tc_nat),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f2066,plain,
c_Int_Onumber__class_Onumber__of(sF3,tc_nat) = sF4,
inference(reorient_equations,[],[f2065]) ).
fof(f2067,definition,
sF5 = c_SetInterval_Oord__class_OatLeastLessThan(sF0,sF4,tc_nat),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f2068,plain,
c_SetInterval_Oord__class_OatLeastLessThan(sF0,sF4,tc_nat) = sF5,
inference(reorient_equations,[],[f2067]) ).
fof(f2069,definition,
sF6 = hAPP(c_Suc,sF0),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f2070,plain,
hAPP(c_Suc,sF0) = sF6,
inference(reorient_equations,[],[f2069]) ).
fof(f2071,definition,
sF7 = hAPP(c_Suc,sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f2072,plain,
hAPP(c_Suc,sF6) = sF7,
inference(reorient_equations,[],[f2071]) ).
fof(f2073,definition,
sF8 = hAPP(c_Suc,sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f2074,plain,
hAPP(c_Suc,sF7) = sF8,
inference(reorient_equations,[],[f2073]) ).
fof(f2075,definition,
sF9 = hAPP(c_Suc,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f2076,plain,
hAPP(c_Suc,sF8) = sF9,
inference(reorient_equations,[],[f2075]) ).
fof(f2077,definition,
sF10 = c_SetInterval_Oord__class_OatLeastLessThan(sF0,sF9,tc_nat),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f2078,plain,
c_SetInterval_Oord__class_OatLeastLessThan(sF0,sF9,tc_nat) = sF10,
inference(reorient_equations,[],[f2077]) ).
fof(f2079,plain,
sF5 != sF10,
inference(definition_folding,[],[f1955,f2078,f2076,f2074,f2072,f2070,f2058,f2058,f2068,f2066,f2064,f2062,f2060,f2058]) ).
fof(f2081,plain,
c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OBit1(c_Int_OPls)),tc_nat) = hAPP(c_Suc,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)),
inference(forward_demodulation,[],[f1940,f1951]) ).
fof(f2082,plain,
c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat) = hAPP(c_Suc,c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OPls),tc_nat)),
inference(backward_demodulation,[],[f1951,f1921]) ).
fof(f2088,plain,
! [X0] : c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X0),c_Int_Onat(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_Int_Oint)),tc_nat) = X0,
inference(backward_demodulation,[],[f1667,f1666]) ).
fof(f2096,plain,
! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X0) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),X0),c_Int_Onat(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_Int_Oint))),
inference(backward_demodulation,[],[f1823,f1666]) ).
fof(f2110,plain,
! [X0] :
( c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) = c_Int_Onat(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_Int_Oint))
| c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) = c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OBit1(c_Int_OPls)),tc_nat)
| c_HOL_Oone__class_Oone(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) ),
inference(backward_demodulation,[],[f1858,f1666]) ).
fof(f2114,plain,
! [X0] :
( hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat)),X0) = hAPP(c_Suc,hAPP(c_Suc,c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat)),X0),c_Int_Onat(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_Int_Oint)),tc_nat)))
| c_HOL_Ozero__class_Ozero(tc_nat) = X0 ),
inference(backward_demodulation,[],[f1889,f1666]) ).
fof(f2120,plain,
! [X0] : hAPP(c_Suc,c_Divides_Odiv__class_Odiv(X0,c_Int_Onat(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_Int_Oint)),tc_nat)) = c_Divides_Odiv__class_Odiv(hAPP(c_Suc,hAPP(c_Suc,X0)),c_Int_Onat(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_Int_Oint)),tc_nat),
inference(backward_demodulation,[],[f1905,f1666]) ).
fof(f2121,plain,
! [X0] : hAPP(c_Suc,hAPP(c_Suc,X0)) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Int_Onat(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_Int_Oint))),X0),
inference(backward_demodulation,[],[f1907,f1666]) ).
fof(f2123,plain,
! [X0] : c_Divides_Odiv__class_Omod(X0,c_Int_Onat(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_Int_Oint)),tc_nat) = c_Divides_Odiv__class_Omod(hAPP(c_Suc,hAPP(c_Suc,X0)),c_Int_Onat(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_Int_Oint)),tc_nat),
inference(backward_demodulation,[],[f1911,f1666]) ).
fof(f2132,plain,
c_HOL_Oone__class_Oone(tc_nat) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),c_HOL_Oone__class_Oone(tc_nat)),
inference(backward_demodulation,[],[f1603,f1602]) ).
fof(f2166,plain,
! [X0] :
( ~ c_Parity_Oeven__odd__class_Oeven(c_Divides_Odiv__class_Omod(X0,c_Int_Onat(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_Int_Oint)),tc_nat),tc_nat)
| c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(backward_demodulation,[],[f1817,f1473]) ).
fof(f2168,plain,
c_HOL_Ozero__class_Ozero(tc_nat) = c_Int_Onat(c_Int_Onumber__class_Onumber__of(c_Int_OPls,tc_Int_Oint)),
inference(backward_demodulation,[],[f1925,f1473]) ).
fof(f2170,plain,
! [X0] : hAPP(c_Suc,hAPP(c_Suc,hAPP(c_Suc,X0))) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Int_Onat(c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OBit1(c_Int_OPls)),tc_Int_Oint))),X0),
inference(backward_demodulation,[],[f1895,f1473]) ).
fof(f2171,plain,
c_HOL_Oone__class_Oone(tc_nat) = c_Int_Onat(c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OPls),tc_Int_Oint)),
inference(backward_demodulation,[],[f1892,f1473]) ).
fof(f2195,plain,
! [X0] :
( c_Divides_Odiv__class_Odiv(X0,c_Int_Onat(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_Int_Oint)),tc_nat) = c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),c_HOL_Oone__class_Oone(tc_nat)),c_Int_Onat(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_Int_Oint)),tc_nat)
| ~ c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(forward_demodulation,[],[f1392,f1473]) ).
fof(f2220,plain,
! [X0] :
( hAPP(c_Suc,hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),hAPP(c_Suc,c_HOL_Oone__class_Oone(tc_nat))),c_Divides_Odiv__class_Odiv(X0,hAPP(c_Suc,c_HOL_Oone__class_Oone(tc_nat)),tc_nat))) = X0
| c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(forward_demodulation,[],[f954,f1602]) ).
fof(f2222,plain,
! [X0] :
( c_HOL_Oone__class_Oone(tc_nat) != c_Divides_Odiv__class_Omod(X0,c_Int_Onat(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_Int_Oint)),tc_nat)
| c_Parity_Oeven__odd__class_Oeven(c_Divides_Odiv__class_Odiv(c_HOL_Ominus__class_Ominus(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f861,f1473]) ).
fof(f2239,plain,
! [X0] : c_Int_Onumber__class_Onumber__of(X0,tc_nat) = c_Int_Onat(X0),
inference(backward_demodulation,[],[f1473,f110]) ).
fof(f2289,plain,
! [X0] : sF0 = hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),X0),sF0),
inference(backward_demodulation,[],[f1165,f2058]) ).
fof(f2290,plain,
c_Parity_Oeven__odd__class_Oeven(sF0,tc_nat),
inference(backward_demodulation,[],[f1166,f2058]) ).
fof(f2299,plain,
! [X0] : c_HOL_Ominus__class_Ominus(X0,X0,tc_nat) = sF0,
inference(backward_demodulation,[],[f1187,f2058]) ).
fof(f2303,plain,
! [X0] : c_HOL_Ominus__class_Ominus(X0,sF0,tc_nat) = X0,
inference(backward_demodulation,[],[f1309,f2058]) ).
fof(f2305,plain,
! [X0] : sF0 = c_HOL_Ominus__class_Ominus(sF0,X0,tc_nat),
inference(backward_demodulation,[],[f1317,f2058]) ).
fof(f2306,plain,
! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),sF0) = X0,
inference(backward_demodulation,[],[f1320,f2058]) ).
fof(f2307,plain,
! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF0),X0) = X0,
inference(backward_demodulation,[],[f1321,f2058]) ).
fof(f2314,plain,
c_HOL_Oone__class_Oone(tc_nat) = hAPP(c_Suc,sF0),
inference(backward_demodulation,[],[f1602,f2058]) ).
fof(f2318,plain,
! [X0,X1] : c_Divides_Odiv__class_Omod(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),X0),X1),X0,tc_nat) = sF0,
inference(backward_demodulation,[],[f1737,f2058]) ).
fof(f2321,plain,
! [X0] : c_SetInterval_Oord__class_OlessThan(X0,tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(sF0,X0,tc_nat),
inference(backward_demodulation,[],[f1832,f2058]) ).
fof(f2322,plain,
! [X0] : hAPP(c_Suc,X0) != sF0,
inference(backward_demodulation,[],[f1948,f2058]) ).
fof(f2334,plain,
c_Int_Onumber__class_Onumber__of(c_Int_OBit1(sF1),tc_nat) = hAPP(c_Suc,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_nat)),
inference(forward_demodulation,[],[f2081,f2060]) ).
fof(f2335,plain,
c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_nat) = hAPP(c_Suc,c_Int_Onumber__class_Onumber__of(sF1,tc_nat)),
inference(forward_demodulation,[],[f2082,f2060]) ).
fof(f2340,plain,
! [X0] : c_Divides_Odiv__class_Omod(X0,c_Int_Onat(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat) = c_Divides_Odiv__class_Omod(hAPP(c_Suc,hAPP(c_Suc,X0)),c_Int_Onat(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),
inference(forward_demodulation,[],[f2123,f110]) ).
fof(f2342,plain,
! [X0] : hAPP(c_Suc,hAPP(c_Suc,X0)) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Int_Onat(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),X0),
inference(forward_demodulation,[],[f2121,f110]) ).
fof(f2343,plain,
! [X0] : hAPP(c_Suc,c_Divides_Odiv__class_Odiv(X0,c_Int_Onat(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat)) = c_Divides_Odiv__class_Odiv(hAPP(c_Suc,hAPP(c_Suc,X0)),c_Int_Onat(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),
inference(forward_demodulation,[],[f2120,f110]) ).
fof(f2349,plain,
! [X0] :
( hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat)),X0) = hAPP(c_Suc,hAPP(c_Suc,c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat)),X0),c_Int_Onat(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat)))
| c_HOL_Ozero__class_Ozero(tc_nat) = X0 ),
inference(forward_demodulation,[],[f2114,f110]) ).
fof(f2353,plain,
! [X0] :
( c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) = c_Int_Onat(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))
| c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) = c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OBit1(c_Int_OPls)),tc_nat)
| c_HOL_Oone__class_Oone(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f2110,f110]) ).
fof(f2367,plain,
! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X0) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),X0),c_Int_Onat(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),
inference(forward_demodulation,[],[f2096,f110]) ).
fof(f2375,plain,
! [X0] : c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X0),c_Int_Onat(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat) = X0,
inference(forward_demodulation,[],[f2088,f110]) ).
fof(f2392,plain,
c_HOL_Oone__class_Oone(tc_nat) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),c_HOL_Ozero__class_Ozero(tc_nat)),
inference(forward_demodulation,[],[f2132,f1202]) ).
fof(f2406,plain,
c_HOL_Oone__class_Oone(tc_nat) = c_Int_Onat(c_Int_OBit1(c_Int_OPls)),
inference(forward_demodulation,[],[f2171,f110]) ).
fof(f2407,plain,
! [X0] : hAPP(c_Suc,hAPP(c_Suc,hAPP(c_Suc,X0))) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Int_Onat(c_Int_OBit1(c_Int_OBit1(c_Int_OPls)))),X0),
inference(forward_demodulation,[],[f2170,f110]) ).
fof(f2409,plain,
c_HOL_Ozero__class_Ozero(tc_nat) = c_Int_Onat(c_Int_OPls),
inference(forward_demodulation,[],[f2168,f110]) ).
fof(f2411,plain,
! [X0] :
( ~ c_Parity_Oeven__odd__class_Oeven(c_Divides_Odiv__class_Omod(X0,c_Int_Onat(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),tc_nat),tc_nat)
| c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(forward_demodulation,[],[f2166,f110]) ).
fof(f2441,plain,
! [X0] :
( c_Divides_Odiv__class_Odiv(X0,c_Int_Onat(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat) = c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),c_HOL_Oone__class_Oone(tc_nat)),c_Int_Onat(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat)
| ~ c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(forward_demodulation,[],[f2195,f110]) ).
fof(f2458,plain,
! [X0] :
( c_HOL_Oone__class_Oone(tc_nat) != c_Divides_Odiv__class_Omod(X0,c_Int_Onat(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),tc_nat)
| c_Parity_Oeven__odd__class_Oeven(c_Divides_Odiv__class_Odiv(c_HOL_Ominus__class_Ominus(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f2222,f110]) ).
fof(f2467,plain,
sF4 = c_Int_Onat(sF3),
inference(backward_demodulation,[],[f2066,f2239]) ).
fof(f2471,plain,
sF5 = c_SetInterval_Oord__class_OlessThan(sF4,tc_nat),
inference(backward_demodulation,[],[f2068,f2321]) ).
fof(f2472,plain,
sF10 = c_SetInterval_Oord__class_OlessThan(sF9,tc_nat),
inference(backward_demodulation,[],[f2078,f2321]) ).
fof(f2474,plain,
c_HOL_Oone__class_Oone(tc_nat) = sF6,
inference(forward_demodulation,[],[f2314,f2070]) ).
fof(f2491,plain,
c_Int_Onumber__class_Onumber__of(c_Int_OBit1(sF1),tc_nat) = hAPP(c_Suc,c_Int_Onat(c_Int_OBit0(sF1))),
inference(forward_demodulation,[],[f2334,f2239]) ).
fof(f2492,plain,
c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF1),tc_nat) = hAPP(c_Suc,c_Int_Onat(sF1)),
inference(forward_demodulation,[],[f2335,f2239]) ).
fof(f2497,plain,
! [X0] : c_Divides_Odiv__class_Omod(X0,c_Int_Onat(c_Int_OBit0(sF1)),tc_nat) = c_Divides_Odiv__class_Omod(hAPP(c_Suc,hAPP(c_Suc,X0)),c_Int_Onat(c_Int_OBit0(sF1)),tc_nat),
inference(forward_demodulation,[],[f2340,f2060]) ).
fof(f2499,plain,
! [X0] : hAPP(c_Suc,hAPP(c_Suc,X0)) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Int_Onat(c_Int_OBit0(sF1))),X0),
inference(forward_demodulation,[],[f2342,f2060]) ).
fof(f2500,plain,
! [X0] : hAPP(c_Suc,c_Divides_Odiv__class_Odiv(X0,c_Int_Onat(c_Int_OBit0(sF1)),tc_nat)) = c_Divides_Odiv__class_Odiv(hAPP(c_Suc,hAPP(c_Suc,X0)),c_Int_Onat(c_Int_OBit0(sF1)),tc_nat),
inference(forward_demodulation,[],[f2343,f2060]) ).
fof(f2506,plain,
! [X0] :
( hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(sF1)),tc_nat)),X0) = hAPP(c_Suc,hAPP(c_Suc,c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(sF1)),tc_nat)),X0),c_Int_Onat(c_Int_OBit0(sF1)),tc_nat)))
| c_HOL_Ozero__class_Ozero(tc_nat) = X0 ),
inference(forward_demodulation,[],[f2349,f2060]) ).
fof(f2510,plain,
! [X0] :
( c_Int_Onat(c_Int_OBit0(sF1)) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(sF1)),tc_nat),tc_nat)
| c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) = c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OBit1(c_Int_OPls)),tc_nat)
| c_HOL_Oone__class_Oone(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f2353,f2060]) ).
fof(f2524,plain,
! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X0) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),X0),c_Int_Onat(c_Int_OBit0(sF1))),
inference(forward_demodulation,[],[f2367,f2060]) ).
fof(f2532,plain,
! [X0] : c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X0),c_Int_Onat(c_Int_OBit0(sF1)),tc_nat) = X0,
inference(forward_demodulation,[],[f2375,f2060]) ).
fof(f2548,plain,
c_HOL_Oone__class_Oone(tc_nat) = hAPP(c_Suc,c_HOL_Ozero__class_Ozero(tc_nat)),
inference(forward_demodulation,[],[f2392,f320]) ).
fof(f2561,plain,
c_HOL_Oone__class_Oone(tc_nat) = c_Int_Onat(sF1),
inference(forward_demodulation,[],[f2406,f2060]) ).
fof(f2562,plain,
! [X0] : hAPP(c_Suc,hAPP(c_Suc,hAPP(c_Suc,X0))) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Int_Onat(c_Int_OBit1(sF1))),X0),
inference(forward_demodulation,[],[f2407,f2060]) ).
fof(f2564,plain,
sF0 = c_Int_Onat(c_Int_OPls),
inference(backward_demodulation,[],[f2058,f2409]) ).
fof(f2566,plain,
! [X0] :
( ~ c_Parity_Oeven__odd__class_Oeven(c_Divides_Odiv__class_Omod(X0,c_Int_Onat(c_Int_OBit0(c_Int_OBit0(sF1))),tc_nat),tc_nat)
| c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(forward_demodulation,[],[f2411,f2060]) ).
fof(f2596,plain,
! [X0] :
( c_Divides_Odiv__class_Odiv(X0,c_Int_Onat(c_Int_OBit0(sF1)),tc_nat) = c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),c_HOL_Oone__class_Oone(tc_nat)),c_Int_Onat(c_Int_OBit0(sF1)),tc_nat)
| ~ c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(forward_demodulation,[],[f2441,f2060]) ).
fof(f2608,plain,
! [X0] :
( c_HOL_Oone__class_Oone(tc_nat) != c_Divides_Odiv__class_Omod(X0,c_Int_Onat(c_Int_OBit0(c_Int_OBit0(sF1))),tc_nat)
| c_Parity_Oeven__odd__class_Oeven(c_Divides_Odiv__class_Odiv(c_HOL_Ominus__class_Ominus(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f2458,f2060]) ).
fof(f2614,plain,
! [X0] : c_HOL_Ominus__class_Ominus(hAPP(c_Suc,X0),sF6,tc_nat) = X0,
inference(backward_demodulation,[],[f151,f2474]) ).
fof(f2617,plain,
! [X0] : hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),X0),sF6) = X0,
inference(backward_demodulation,[],[f313,f2474]) ).
fof(f2619,plain,
! [X0] : hAPP(c_Suc,X0) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),sF6),
inference(backward_demodulation,[],[f321,f2474]) ).
fof(f2620,plain,
~ c_Parity_Oeven__odd__class_Oeven(sF6,tc_nat),
inference(backward_demodulation,[],[f487,f2474]) ).
fof(f2621,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(X0,hAPP(c_Suc,X1),tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(X0,sF6,tc_nat),X1,tc_nat),
inference(backward_demodulation,[],[f695,f2474]) ).
fof(f2635,plain,
! [X0] :
( hAPP(c_Suc,hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),hAPP(c_Suc,sF6)),c_Divides_Odiv__class_Odiv(X0,hAPP(c_Suc,sF6),tc_nat))) = X0
| c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(backward_demodulation,[],[f2220,f2474]) ).
fof(f2652,plain,
c_Int_Onumber__class_Onumber__of(c_Int_OBit1(sF1),tc_nat) = hAPP(c_Suc,c_Int_Onat(sF2)),
inference(forward_demodulation,[],[f2491,f2062]) ).
fof(f2653,plain,
c_Int_Onat(c_Int_OBit0(sF1)) = hAPP(c_Suc,c_Int_Onat(sF1)),
inference(forward_demodulation,[],[f2492,f2239]) ).
fof(f2657,plain,
! [X0] : c_Divides_Odiv__class_Omod(X0,c_Int_Onat(sF2),tc_nat) = c_Divides_Odiv__class_Omod(hAPP(c_Suc,hAPP(c_Suc,X0)),c_Int_Onat(sF2),tc_nat),
inference(forward_demodulation,[],[f2497,f2062]) ).
fof(f2659,plain,
! [X0] : hAPP(c_Suc,hAPP(c_Suc,X0)) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Int_Onat(sF2)),X0),
inference(forward_demodulation,[],[f2499,f2062]) ).
fof(f2660,plain,
! [X0] : hAPP(c_Suc,c_Divides_Odiv__class_Odiv(X0,c_Int_Onat(sF2),tc_nat)) = c_Divides_Odiv__class_Odiv(hAPP(c_Suc,hAPP(c_Suc,X0)),c_Int_Onat(sF2),tc_nat),
inference(forward_demodulation,[],[f2500,f2062]) ).
fof(f2666,plain,
! [X0] :
( hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF2),tc_nat)),X0) = hAPP(c_Suc,hAPP(c_Suc,c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF2),tc_nat)),X0),c_Int_Onat(sF2),tc_nat)))
| c_HOL_Ozero__class_Ozero(tc_nat) = X0 ),
inference(forward_demodulation,[],[f2506,f2062]) ).
fof(f2670,plain,
! [X0] :
( c_Int_Onat(c_Int_OBit0(sF1)) = c_Divides_Odiv__class_Omod(X0,c_Int_Onat(c_Int_OBit0(c_Int_OBit0(sF1))),tc_nat)
| c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) = c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OBit1(c_Int_OPls)),tc_nat)
| c_HOL_Oone__class_Oone(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f2510,f2239]) ).
fof(f2684,plain,
! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X0) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),X0),c_Int_Onat(sF2)),
inference(forward_demodulation,[],[f2524,f2062]) ).
fof(f2692,plain,
! [X0] : c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X0),c_Int_Onat(sF2),tc_nat) = X0,
inference(forward_demodulation,[],[f2532,f2062]) ).
fof(f2708,plain,
c_HOL_Oone__class_Oone(tc_nat) = hAPP(c_Suc,c_Int_Onat(c_Int_OPls)),
inference(forward_demodulation,[],[f2548,f2409]) ).
fof(f2721,plain,
sF6 = c_Int_Onat(sF1),
inference(backward_demodulation,[],[f2474,f2561]) ).
fof(f2758,plain,
! [X0] : c_Int_Onat(c_Int_OPls) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),X0),c_Int_Onat(c_Int_OPls)),
inference(backward_demodulation,[],[f2289,f2564]) ).
fof(f2759,plain,
c_Parity_Oeven__odd__class_Oeven(c_Int_Onat(c_Int_OPls),tc_nat),
inference(backward_demodulation,[],[f2290,f2564]) ).
fof(f2764,plain,
! [X0] : c_HOL_Ominus__class_Ominus(X0,X0,tc_nat) = c_Int_Onat(c_Int_OPls),
inference(backward_demodulation,[],[f2299,f2564]) ).
fof(f2766,plain,
! [X0] : c_HOL_Ominus__class_Ominus(X0,c_Int_Onat(c_Int_OPls),tc_nat) = X0,
inference(backward_demodulation,[],[f2303,f2564]) ).
fof(f2768,plain,
! [X0] : c_Int_Onat(c_Int_OPls) = c_HOL_Ominus__class_Ominus(c_Int_Onat(c_Int_OPls),X0,tc_nat),
inference(backward_demodulation,[],[f2305,f2564]) ).
fof(f2769,plain,
! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),c_Int_Onat(c_Int_OPls)) = X0,
inference(backward_demodulation,[],[f2306,f2564]) ).
fof(f2770,plain,
! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Int_Onat(c_Int_OPls)),X0) = X0,
inference(backward_demodulation,[],[f2307,f2564]) ).
fof(f2778,plain,
! [X0,X1] : c_Divides_Odiv__class_Omod(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),X0),X1),X0,tc_nat) = c_Int_Onat(c_Int_OPls),
inference(backward_demodulation,[],[f2318,f2564]) ).
fof(f2780,plain,
! [X0] : c_SetInterval_Oord__class_OlessThan(X0,tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(c_Int_Onat(c_Int_OPls),X0,tc_nat),
inference(backward_demodulation,[],[f2321,f2564]) ).
fof(f2781,plain,
! [X0] : hAPP(c_Suc,X0) != c_Int_Onat(c_Int_OPls),
inference(backward_demodulation,[],[f2322,f2564]) ).
fof(f2794,plain,
! [X0] :
( ~ c_Parity_Oeven__odd__class_Oeven(c_Divides_Odiv__class_Omod(X0,c_Int_Onat(c_Int_OBit0(sF2)),tc_nat),tc_nat)
| c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(forward_demodulation,[],[f2566,f2062]) ).
fof(f2818,plain,
! [X0] :
( c_Divides_Odiv__class_Odiv(X0,c_Int_Onat(sF2),tc_nat) = c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),c_HOL_Oone__class_Oone(tc_nat)),c_Int_Onat(sF2),tc_nat)
| ~ c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(forward_demodulation,[],[f2596,f2062]) ).
fof(f2828,plain,
! [X0] :
( c_HOL_Oone__class_Oone(tc_nat) != c_Divides_Odiv__class_Omod(X0,c_Int_Onat(c_Int_OBit0(sF2)),tc_nat)
| c_Parity_Oeven__odd__class_Oeven(c_Divides_Odiv__class_Odiv(c_HOL_Ominus__class_Ominus(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f2608,f2062]) ).
fof(f2843,plain,
! [X0] :
( hAPP(c_Suc,hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),sF7),c_Divides_Odiv__class_Odiv(X0,sF7,tc_nat))) = X0
| c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(forward_demodulation,[],[f2635,f2072]) ).
fof(f2856,plain,
c_Int_Onat(c_Int_OBit1(sF1)) = hAPP(c_Suc,c_Int_Onat(sF2)),
inference(forward_demodulation,[],[f2652,f2239]) ).
fof(f2857,plain,
hAPP(c_Suc,c_Int_Onat(sF1)) = c_Int_Onat(sF2),
inference(forward_demodulation,[],[f2653,f2062]) ).
fof(f2862,plain,
! [X0] :
( hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onat(c_Int_OBit0(sF2))),X0) = hAPP(c_Suc,hAPP(c_Suc,c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onat(c_Int_OBit0(sF2))),X0),c_Int_Onat(sF2),tc_nat)))
| c_HOL_Ozero__class_Ozero(tc_nat) = X0 ),
inference(forward_demodulation,[],[f2666,f2239]) ).
fof(f2864,plain,
! [X0] :
( c_Int_Onat(sF2) = c_Divides_Odiv__class_Omod(X0,c_Int_Onat(c_Int_OBit0(sF2)),tc_nat)
| c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) = c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OBit1(c_Int_OPls)),tc_nat)
| c_HOL_Oone__class_Oone(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f2670,f2062]) ).
fof(f2874,plain,
c_Int_Onat(sF1) = hAPP(c_Suc,c_Int_Onat(c_Int_OPls)),
inference(forward_demodulation,[],[f2708,f2561]) ).
fof(f2882,plain,
sF7 = hAPP(c_Suc,c_Int_Onat(sF1)),
inference(backward_demodulation,[],[f2072,f2721]) ).
fof(f2883,plain,
! [X0] : c_HOL_Ominus__class_Ominus(hAPP(c_Suc,X0),c_Int_Onat(sF1),tc_nat) = X0,
inference(backward_demodulation,[],[f2614,f2721]) ).
fof(f2886,plain,
! [X0] : hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),X0),c_Int_Onat(sF1)) = X0,
inference(backward_demodulation,[],[f2617,f2721]) ).
fof(f2888,plain,
! [X0] : hAPP(c_Suc,X0) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),c_Int_Onat(sF1)),
inference(backward_demodulation,[],[f2619,f2721]) ).
fof(f2889,plain,
~ c_Parity_Oeven__odd__class_Oeven(c_Int_Onat(sF1),tc_nat),
inference(backward_demodulation,[],[f2620,f2721]) ).
fof(f2890,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(X0,hAPP(c_Suc,X1),tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(X0,c_Int_Onat(sF1),tc_nat),X1,tc_nat),
inference(backward_demodulation,[],[f2621,f2721]) ).
fof(f2911,plain,
! [X0] :
( ~ c_Parity_Oeven__odd__class_Oeven(c_Divides_Odiv__class_Omod(X0,c_Int_Onat(sF3),tc_nat),tc_nat)
| c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(forward_demodulation,[],[f2794,f2064]) ).
fof(f2914,plain,
! [X0] :
( c_Divides_Odiv__class_Odiv(X0,c_Int_Onat(sF2),tc_nat) = c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),c_Int_Onat(sF1)),c_Int_Onat(sF2),tc_nat)
| ~ c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(forward_demodulation,[],[f2818,f2561]) ).
fof(f2922,plain,
! [X0] :
( c_HOL_Oone__class_Oone(tc_nat) != c_Divides_Odiv__class_Omod(X0,c_Int_Onat(sF3),tc_nat)
| c_Parity_Oeven__odd__class_Oeven(c_Divides_Odiv__class_Odiv(c_HOL_Ominus__class_Ominus(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f2828,f2064]) ).
fof(f2944,plain,
! [X0] :
( hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onat(sF3)),X0) = hAPP(c_Suc,hAPP(c_Suc,c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onat(sF3)),X0),c_Int_Onat(sF2),tc_nat)))
| c_HOL_Ozero__class_Ozero(tc_nat) = X0 ),
inference(forward_demodulation,[],[f2862,f2064]) ).
fof(f2945,plain,
! [X0] :
( c_Int_Onat(sF2) = c_Divides_Odiv__class_Omod(X0,c_Int_Onat(sF3),tc_nat)
| c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) = c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OBit1(c_Int_OPls)),tc_nat)
| c_HOL_Oone__class_Oone(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f2864,f2064]) ).
fof(f2960,plain,
sF7 = c_Int_Onat(sF2),
inference(forward_demodulation,[],[f2882,f2857]) ).
fof(f2962,plain,
! [X0] :
( ~ c_Parity_Oeven__odd__class_Oeven(c_Divides_Odiv__class_Omod(X0,sF4,tc_nat),tc_nat)
| c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(forward_demodulation,[],[f2911,f2467]) ).
fof(f2965,plain,
! [X0] :
( c_Divides_Odiv__class_Odiv(X0,c_Int_Onat(sF2),tc_nat) = c_Divides_Odiv__class_Odiv(hAPP(c_Suc,X0),c_Int_Onat(sF2),tc_nat)
| ~ c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(forward_demodulation,[],[f2914,f2888]) ).
fof(f2967,plain,
! [X0] :
( c_HOL_Oone__class_Oone(tc_nat) != c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_Parity_Oeven__odd__class_Oeven(c_Divides_Odiv__class_Odiv(c_HOL_Ominus__class_Ominus(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f2922,f2467]) ).
fof(f2970,plain,
! [X0] :
( hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),sF4),X0) = hAPP(c_Suc,hAPP(c_Suc,c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),sF4),X0),c_Int_Onat(sF2),tc_nat)))
| c_HOL_Ozero__class_Ozero(tc_nat) = X0 ),
inference(forward_demodulation,[],[f2944,f2467]) ).
fof(f2971,plain,
! [X0] :
( c_Int_Onat(sF2) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) = c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OBit1(c_Int_OPls)),tc_nat)
| c_HOL_Oone__class_Oone(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f2945,f2467]) ).
fof(f2982,plain,
sF8 = hAPP(c_Suc,c_Int_Onat(sF2)),
inference(backward_demodulation,[],[f2074,f2960]) ).
fof(f2984,plain,
! [X0] :
( hAPP(c_Suc,hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onat(sF2)),c_Divides_Odiv__class_Odiv(X0,c_Int_Onat(sF2),tc_nat))) = X0
| c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(backward_demodulation,[],[f2843,f2960]) ).
fof(f2995,plain,
! [X0] :
( c_Int_Onat(sF1) != c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_Parity_Oeven__odd__class_Oeven(c_Divides_Odiv__class_Odiv(c_HOL_Ominus__class_Ominus(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f2967,f2561]) ).
fof(f2997,plain,
! [X0] :
( hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),sF4),X0) = hAPP(c_Suc,hAPP(c_Suc,c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),sF4),X0),c_Int_Onat(sF2),tc_nat)))
| c_Int_Onat(c_Int_OPls) = X0 ),
inference(forward_demodulation,[],[f2970,f2409]) ).
fof(f2998,plain,
! [X0] :
( c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) = c_Int_Onat(c_Int_OBit1(c_Int_OBit1(c_Int_OPls)))
| c_Int_Onat(sF2) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_HOL_Oone__class_Oone(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f2971,f2239]) ).
fof(f3003,plain,
sF8 = c_Int_Onat(c_Int_OBit1(sF1)),
inference(backward_demodulation,[],[f2856,f2982]) ).
fof(f3005,plain,
! [X0] :
( c_Parity_Oeven__odd__class_Oeven(c_Divides_Odiv__class_Odiv(c_HOL_Ominus__class_Ominus(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat),c_Int_Onat(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat)
| c_Int_Onat(sF1) != c_Divides_Odiv__class_Omod(X0,sF4,tc_nat) ),
inference(forward_demodulation,[],[f2995,f2239]) ).
fof(f3007,plain,
! [X0] :
( c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(sF1)),tc_nat),tc_nat) = c_Int_Onat(c_Int_OBit1(sF1))
| c_Int_Onat(sF2) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_HOL_Oone__class_Oone(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f2998,f2060]) ).
fof(f3012,plain,
! [X0] : hAPP(c_Suc,hAPP(c_Suc,hAPP(c_Suc,X0))) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF8),X0),
inference(backward_demodulation,[],[f2562,f3003]) ).
fof(f3013,plain,
! [X0] :
( c_Parity_Oeven__odd__class_Oeven(c_Divides_Odiv__class_Odiv(c_HOL_Ominus__class_Ominus(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat),c_Int_Onat(c_Int_OBit0(sF1)),tc_nat),tc_nat)
| c_Int_Onat(sF1) != c_Divides_Odiv__class_Omod(X0,sF4,tc_nat) ),
inference(forward_demodulation,[],[f3005,f2060]) ).
fof(f3015,plain,
! [X0] :
( sF8 = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(sF1)),tc_nat),tc_nat)
| c_Int_Onat(sF2) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_HOL_Oone__class_Oone(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f3007,f3003]) ).
fof(f3016,plain,
! [X0] :
( c_Parity_Oeven__odd__class_Oeven(c_Divides_Odiv__class_Odiv(c_HOL_Ominus__class_Ominus(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat),c_Int_Onat(sF2),tc_nat),tc_nat)
| c_Int_Onat(sF1) != c_Divides_Odiv__class_Omod(X0,sF4,tc_nat) ),
inference(forward_demodulation,[],[f3013,f2062]) ).
fof(f3018,plain,
! [X0] :
( sF8 = c_Divides_Odiv__class_Omod(X0,c_Int_Onat(c_Int_OBit0(c_Int_OBit0(sF1))),tc_nat)
| c_Int_Onat(sF2) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_HOL_Oone__class_Oone(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f3015,f2239]) ).
fof(f3019,plain,
! [X0] :
( c_Parity_Oeven__odd__class_Oeven(c_Divides_Odiv__class_Odiv(c_HOL_Ominus__class_Ominus(X0,c_Int_Onat(sF1),tc_nat),c_Int_Onat(sF2),tc_nat),tc_nat)
| c_Int_Onat(sF1) != c_Divides_Odiv__class_Omod(X0,sF4,tc_nat) ),
inference(forward_demodulation,[],[f3016,f2561]) ).
fof(f3021,plain,
! [X0] :
( sF8 = c_Divides_Odiv__class_Omod(X0,c_Int_Onat(c_Int_OBit0(sF2)),tc_nat)
| c_Int_Onat(sF2) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_HOL_Oone__class_Oone(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f3018,f2062]) ).
fof(f3023,plain,
! [X0] :
( sF8 = c_Divides_Odiv__class_Omod(X0,c_Int_Onat(sF3),tc_nat)
| c_Int_Onat(sF2) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_HOL_Oone__class_Oone(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f3021,f2064]) ).
fof(f3024,plain,
! [X0] :
( sF8 = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_Int_Onat(sF2) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_HOL_Oone__class_Oone(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f3023,f2467]) ).
fof(f3025,plain,
! [X0] :
( c_HOL_Oone__class_Oone(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onat(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),tc_nat)
| sF8 = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_Int_Onat(sF2) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f3024,f2239]) ).
fof(f3026,plain,
! [X0] :
( c_HOL_Oone__class_Oone(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onat(c_Int_OBit0(c_Int_OBit0(sF1))),tc_nat)
| sF8 = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_Int_Onat(sF2) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f3025,f2060]) ).
fof(f3027,plain,
! [X0] :
( c_HOL_Oone__class_Oone(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onat(c_Int_OBit0(sF2)),tc_nat)
| sF8 = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_Int_Onat(sF2) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f3026,f2062]) ).
fof(f3028,plain,
! [X0] :
( c_HOL_Oone__class_Oone(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onat(sF3),tc_nat)
| sF8 = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_Int_Onat(sF2) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f3027,f2064]) ).
fof(f3029,plain,
! [X0] :
( c_HOL_Oone__class_Oone(tc_nat) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| sF8 = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_Int_Onat(sF2) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f3028,f2467]) ).
fof(f3030,plain,
! [X0] :
( c_Int_Onat(sF1) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| sF8 = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_Int_Onat(sF2) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f3029,f2561]) ).
fof(f3031,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onat(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)))),tc_nat)
| c_Int_Onat(sF1) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| sF8 = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_Int_Onat(sF2) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat) ),
inference(forward_demodulation,[],[f3030,f2239]) ).
fof(f3032,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onat(c_Int_OBit0(c_Int_OBit0(sF1))),tc_nat)
| c_Int_Onat(sF1) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| sF8 = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_Int_Onat(sF2) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat) ),
inference(forward_demodulation,[],[f3031,f2060]) ).
fof(f3033,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onat(c_Int_OBit0(sF2)),tc_nat)
| c_Int_Onat(sF1) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| sF8 = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_Int_Onat(sF2) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat) ),
inference(forward_demodulation,[],[f3032,f2062]) ).
fof(f3034,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Int_Onat(sF3),tc_nat)
| c_Int_Onat(sF1) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| sF8 = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_Int_Onat(sF2) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat) ),
inference(forward_demodulation,[],[f3033,f2064]) ).
fof(f3035,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_Int_Onat(sF1) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| sF8 = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_Int_Onat(sF2) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat) ),
inference(forward_demodulation,[],[f3034,f2467]) ).
fof(f3036,plain,
! [X0] :
( c_Int_Onat(sF2) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_Int_Onat(sF1) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| sF8 = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_Int_Onat(c_Int_OPls) = c_Divides_Odiv__class_Omod(X0,sF4,tc_nat) ),
inference(forward_demodulation,[],[f3035,f2409]) ).
fof(f3041,plain,
sF8 != sF9,
inference(superposition,[],[f1943,f2076]) ).
fof(f3042,plain,
! [X0] : c_SetInterval_Oord__class_OatLeastAtMost(X0,sF8,tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(X0,sF9,tc_nat),
inference(superposition,[],[f1834,f2076]) ).
fof(f3049,plain,
sF8 != c_Int_Onat(sF2),
inference(superposition,[],[f1943,f2982]) ).
fof(f3078,plain,
c_Int_Onat(c_Int_OPls) != c_Int_Onat(sF1),
inference(superposition,[],[f1943,f2874]) ).
fof(f3082,plain,
( c_Parity_Oeven__odd__class_Oeven(c_Int_Onat(sF2),tc_nat)
| c_Parity_Oeven__odd__class_Oeven(c_Int_Onat(sF1),tc_nat) ),
inference(superposition,[],[f1377,f2857]) ).
fof(f3084,plain,
c_Parity_Oeven__odd__class_Oeven(c_Int_Onat(sF2),tc_nat),
inference(forward_subsumption_resolution,[],[f3082,f2889]) ).
fof(f3086,definition,
( spl11_1
<=> c_Parity_Oeven__odd__class_Oeven(c_Int_Onat(sF2),tc_nat) ),
introduced(definition,[new_symbols(definition,[spl11_1])],[avatar_definition]) ).
fof(f3088,plain,
( c_Parity_Oeven__odd__class_Oeven(c_Int_Onat(sF2),tc_nat)
| ~ spl11_1 ),
inference(avatar_component_clause,[],[f3086]) ).
fof(f3099,plain,
spl11_1,
inference(avatar_split_clause,[],[f3084,f3086]) ).
fof(f3165,plain,
! [X0] : c_HOL_Ominus__class_Ominus(sF8,X0,tc_nat) = c_HOL_Ominus__class_Ominus(sF9,hAPP(c_Suc,X0),tc_nat),
inference(superposition,[],[f1351,f2076]) ).
fof(f3166,plain,
! [X0] : c_HOL_Ominus__class_Ominus(c_Int_Onat(sF2),X0,tc_nat) = c_HOL_Ominus__class_Ominus(sF8,hAPP(c_Suc,X0),tc_nat),
inference(superposition,[],[f1351,f2982]) ).
fof(f3168,plain,
! [X0] : c_HOL_Ominus__class_Ominus(c_Int_Onat(c_Int_OPls),X0,tc_nat) = c_HOL_Ominus__class_Ominus(c_Int_Onat(sF1),hAPP(c_Suc,X0),tc_nat),
inference(superposition,[],[f1351,f2874]) ).
fof(f3178,plain,
! [X0] : c_Int_Onat(c_Int_OPls) = c_HOL_Ominus__class_Ominus(c_Int_Onat(sF1),hAPP(c_Suc,X0),tc_nat),
inference(forward_demodulation,[],[f3168,f2768]) ).
fof(f3180,plain,
hAPP(c_Suc,c_Divides_Odiv__class_Odiv(c_Int_Onat(sF2),c_Int_Onat(sF2),tc_nat)) = c_Divides_Odiv__class_Odiv(hAPP(c_Suc,sF8),c_Int_Onat(sF2),tc_nat),
inference(superposition,[],[f2660,f2982]) ).
fof(f3182,plain,
hAPP(c_Suc,c_Divides_Odiv__class_Odiv(c_Int_Onat(c_Int_OPls),c_Int_Onat(sF2),tc_nat)) = c_Divides_Odiv__class_Odiv(hAPP(c_Suc,c_Int_Onat(sF1)),c_Int_Onat(sF2),tc_nat),
inference(superposition,[],[f2660,f2874]) ).
fof(f3184,plain,
! [X0] :
( hAPP(c_Suc,c_Divides_Odiv__class_Odiv(c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),sF4),X0),c_Int_Onat(sF2),tc_nat),c_Int_Onat(sF2),tc_nat)) = c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),sF4),X0),c_Int_Onat(sF2),tc_nat)
| c_Int_Onat(c_Int_OPls) = X0 ),
inference(superposition,[],[f2660,f2997]) ).
fof(f3186,plain,
c_Divides_Odiv__class_Odiv(c_Int_Onat(sF2),c_Int_Onat(sF2),tc_nat) = hAPP(c_Suc,c_Divides_Odiv__class_Odiv(c_Int_Onat(c_Int_OPls),c_Int_Onat(sF2),tc_nat)),
inference(forward_demodulation,[],[f3182,f2857]) ).
fof(f3188,plain,
hAPP(c_Suc,c_Divides_Odiv__class_Odiv(c_Int_Onat(sF2),c_Int_Onat(sF2),tc_nat)) = c_Divides_Odiv__class_Odiv(sF9,c_Int_Onat(sF2),tc_nat),
inference(forward_demodulation,[],[f3180,f2076]) ).
fof(f3251,plain,
c_Divides_Odiv__class_Omod(c_Int_Onat(sF2),c_Int_Onat(sF2),tc_nat) = c_Divides_Odiv__class_Omod(hAPP(c_Suc,sF8),c_Int_Onat(sF2),tc_nat),
inference(superposition,[],[f2657,f2982]) ).
fof(f3253,plain,
c_Divides_Odiv__class_Omod(c_Int_Onat(c_Int_OPls),c_Int_Onat(sF2),tc_nat) = c_Divides_Odiv__class_Omod(hAPP(c_Suc,c_Int_Onat(sF1)),c_Int_Onat(sF2),tc_nat),
inference(superposition,[],[f2657,f2874]) ).
fof(f3260,plain,
c_Divides_Odiv__class_Omod(c_Int_Onat(sF2),c_Int_Onat(sF2),tc_nat) = c_Divides_Odiv__class_Omod(c_Int_Onat(c_Int_OPls),c_Int_Onat(sF2),tc_nat),
inference(forward_demodulation,[],[f3253,f2857]) ).
fof(f3262,plain,
c_Divides_Odiv__class_Omod(c_Int_Onat(sF2),c_Int_Onat(sF2),tc_nat) = c_Divides_Odiv__class_Omod(sF9,c_Int_Onat(sF2),tc_nat),
inference(forward_demodulation,[],[f3251,f2076]) ).
fof(f3264,plain,
c_Divides_Odiv__class_Omod(c_Int_Onat(c_Int_OPls),c_Int_Onat(sF2),tc_nat) = c_Divides_Odiv__class_Omod(sF9,c_Int_Onat(sF2),tc_nat),
inference(forward_demodulation,[],[f3262,f3260]) ).
fof(f3272,plain,
( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF4),sF4) = hAPP(c_Suc,hAPP(c_Suc,c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF4),sF4),c_Int_Onat(sF2),tc_nat)))
| c_Int_Onat(c_Int_OPls) = c_Int_Onat(sF2) ),
inference(superposition,[],[f2997,f2684]) ).
fof(f3274,definition,
( spl11_6
<=> c_Int_Onat(c_Int_OPls) = c_Int_Onat(sF2) ),
introduced(definition,[new_symbols(definition,[spl11_6])],[avatar_definition]) ).
fof(f3275,plain,
( c_Int_Onat(c_Int_OPls) != c_Int_Onat(sF2)
| spl11_6 ),
inference(avatar_component_clause,[],[f3274]) ).
fof(f3276,plain,
( c_Int_Onat(c_Int_OPls) = c_Int_Onat(sF2)
| ~ spl11_6 ),
inference(avatar_component_clause,[],[f3274]) ).
fof(f3278,definition,
( spl11_7
<=> hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF4),sF4) = hAPP(c_Suc,hAPP(c_Suc,c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF4),sF4),c_Int_Onat(sF2),tc_nat))) ),
introduced(definition,[new_symbols(definition,[spl11_7])],[avatar_definition]) ).
fof(f3280,plain,
( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF4),sF4) = hAPP(c_Suc,hAPP(c_Suc,c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF4),sF4),c_Int_Onat(sF2),tc_nat)))
| ~ spl11_7 ),
inference(avatar_component_clause,[],[f3278]) ).
fof(f3281,plain,
( spl11_6
| spl11_7 ),
inference(avatar_split_clause,[],[f3272,f3278,f3274]) ).
fof(f3348,plain,
( sF8 = hAPP(c_Suc,c_Int_Onat(c_Int_OPls))
| ~ spl11_6 ),
inference(backward_demodulation,[],[f2982,f3276]) ).
fof(f3391,plain,
( ! [X0] :
( hAPP(c_Suc,c_Divides_Odiv__class_Odiv(c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),sF4),X0),c_Int_Onat(c_Int_OPls),tc_nat),c_Int_Onat(c_Int_OPls),tc_nat)) = c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),sF4),X0),c_Int_Onat(c_Int_OPls),tc_nat)
| c_Int_Onat(c_Int_OPls) = X0 )
| ~ spl11_6 ),
inference(backward_demodulation,[],[f3184,f3276]) ).
fof(f3462,plain,
( ! [X0] :
( c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),sF4),X0),c_Int_Onat(c_Int_OPls),tc_nat) = hAPP(c_Suc,c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),sF4),X0),c_Int_Onat(c_Int_OPls),tc_nat))
| c_Int_Onat(c_Int_OPls) = X0 )
| ~ spl11_6 ),
inference(forward_demodulation,[],[f3391,f2766]) ).
fof(f3484,plain,
( sF8 = c_Int_Onat(sF1)
| ~ spl11_6 ),
inference(forward_demodulation,[],[f3348,f2874]) ).
fof(f3528,plain,
( ! [X0] : c_Int_Onat(c_Int_OPls) = X0
| ~ spl11_6 ),
inference(forward_subsumption_resolution,[],[f3462,f1943]) ).
fof(f3551,plain,
( sF9 != c_Int_Onat(sF1)
| ~ spl11_6 ),
inference(backward_demodulation,[],[f3041,f3484]) ).
fof(f3636,plain,
( sF9 != c_Int_Onat(c_Int_OPls)
| ~ spl11_6 ),
inference(forward_demodulation,[],[f3551,f3528]) ).
fof(f3666,plain,
( $false
| ~ spl11_6 ),
inference(forward_subsumption_resolution,[],[f3636,f3528]) ).
fof(f3667,plain,
~ spl11_6,
inference(avatar_contradiction_clause,[],[f3666]) ).
fof(f3947,plain,
c_HOL_Ominus__class_Ominus(sF8,c_Int_Onat(sF1),tc_nat) = c_HOL_Ominus__class_Ominus(sF9,c_Int_Onat(sF2),tc_nat),
inference(superposition,[],[f3165,f2857]) ).
fof(f4001,plain,
( c_Divides_Odiv__class_Odiv(c_Int_Onat(sF1),c_Int_Onat(sF2),tc_nat) = c_Divides_Odiv__class_Odiv(c_Int_Onat(c_Int_OPls),c_Int_Onat(sF2),tc_nat)
| ~ c_Parity_Oeven__odd__class_Oeven(c_Int_Onat(c_Int_OPls),tc_nat) ),
inference(superposition,[],[f2965,f2874]) ).
fof(f4002,plain,
( c_Divides_Odiv__class_Odiv(sF8,c_Int_Onat(sF2),tc_nat) = c_Divides_Odiv__class_Odiv(c_Int_Onat(sF2),c_Int_Onat(sF2),tc_nat)
| ~ c_Parity_Oeven__odd__class_Oeven(c_Int_Onat(sF2),tc_nat) ),
inference(superposition,[],[f2965,f2982]) ).
fof(f4018,plain,
( c_Divides_Odiv__class_Odiv(sF8,c_Int_Onat(sF2),tc_nat) = c_Divides_Odiv__class_Odiv(c_Int_Onat(sF2),c_Int_Onat(sF2),tc_nat)
| ~ spl11_1 ),
inference(forward_subsumption_resolution,[],[f4002,f3088]) ).
fof(f4019,plain,
c_Divides_Odiv__class_Odiv(c_Int_Onat(sF1),c_Int_Onat(sF2),tc_nat) = c_Divides_Odiv__class_Odiv(c_Int_Onat(c_Int_OPls),c_Int_Onat(sF2),tc_nat),
inference(forward_subsumption_resolution,[],[f4001,f2759]) ).
fof(f4091,plain,
! [X0] :
( hAPP(c_Suc,X0) != sF8
| c_Int_Onat(sF2) = X0 ),
inference(superposition,[],[f1929,f2982]) ).
fof(f4093,plain,
! [X0] :
( hAPP(c_Suc,X0) != sF9
| sF8 = X0 ),
inference(superposition,[],[f1929,f2076]) ).
fof(f4109,plain,
c_Int_Onat(sF2) = c_HOL_Ominus__class_Ominus(sF8,c_Int_Onat(sF1),tc_nat),
inference(superposition,[],[f2883,f2982]) ).
fof(f4110,plain,
c_Int_Onat(sF1) = c_HOL_Ominus__class_Ominus(c_Int_Onat(sF2),c_Int_Onat(sF1),tc_nat),
inference(superposition,[],[f2883,f2857]) ).
fof(f4116,plain,
c_Int_Onat(sF2) = c_HOL_Ominus__class_Ominus(sF9,c_Int_Onat(sF2),tc_nat),
inference(backward_demodulation,[],[f3947,f4109]) ).
fof(f4253,definition,
( spl11_23
<=> sF9 = c_Int_Onat(c_Int_OPls) ),
introduced(definition,[new_symbols(definition,[spl11_23])],[avatar_definition]) ).
fof(f4255,plain,
( sF9 != c_Int_Onat(c_Int_OPls)
| spl11_23 ),
inference(avatar_component_clause,[],[f4253]) ).
fof(f4351,plain,
c_Int_Onat(c_Int_OPls) = c_Divides_Odiv__class_Odiv(c_Int_Onat(c_Int_OPls),c_Int_Onat(sF2),tc_nat),
inference(superposition,[],[f2692,f2770]) ).
fof(f4352,plain,
c_Int_Onat(sF2) = c_Divides_Odiv__class_Odiv(hAPP(c_Suc,hAPP(c_Suc,c_Int_Onat(sF2))),c_Int_Onat(sF2),tc_nat),
inference(superposition,[],[f2692,f2659]) ).
fof(f4355,plain,
c_Int_Onat(sF2) = hAPP(c_Suc,c_Divides_Odiv__class_Odiv(c_Int_Onat(sF2),c_Int_Onat(sF2),tc_nat)),
inference(forward_demodulation,[],[f4352,f2660]) ).
fof(f4356,plain,
c_Int_Onat(c_Int_OPls) = c_Divides_Odiv__class_Odiv(c_Int_Onat(sF1),c_Int_Onat(sF2),tc_nat),
inference(backward_demodulation,[],[f4019,f4351]) ).
fof(f4357,plain,
hAPP(c_Suc,c_Int_Onat(c_Int_OPls)) = c_Divides_Odiv__class_Odiv(c_Int_Onat(sF2),c_Int_Onat(sF2),tc_nat),
inference(backward_demodulation,[],[f3186,f4351]) ).
fof(f4361,plain,
c_Int_Onat(sF2) = c_Divides_Odiv__class_Odiv(sF9,c_Int_Onat(sF2),tc_nat),
inference(backward_demodulation,[],[f3188,f4355]) ).
fof(f4362,plain,
c_Int_Onat(sF1) = c_Divides_Odiv__class_Odiv(c_Int_Onat(sF2),c_Int_Onat(sF2),tc_nat),
inference(forward_demodulation,[],[f4357,f2874]) ).
fof(f4380,plain,
( c_Int_Onat(sF1) = c_Divides_Odiv__class_Odiv(sF8,c_Int_Onat(sF2),tc_nat)
| ~ spl11_1 ),
inference(backward_demodulation,[],[f4018,f4362]) ).
fof(f4473,plain,
sF8 != c_Int_Onat(c_Int_OPls),
inference(superposition,[],[f2781,f2982]) ).
fof(f4475,plain,
sF9 != c_Int_Onat(c_Int_OPls),
inference(superposition,[],[f2781,f2076]) ).
fof(f4476,plain,
~ spl11_23,
inference(avatar_split_clause,[],[f4475,f4253]) ).
fof(f4664,plain,
! [X0] :
( c_Divides_Odiv__class_Omod(hAPP(c_Suc,X0),c_Int_Onat(sF2),tc_nat) = c_Divides_Odiv__class_Omod(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onat(sF2)),c_Divides_Odiv__class_Odiv(X0,c_Int_Onat(sF2),tc_nat)),c_Int_Onat(sF2),tc_nat)
| c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(superposition,[],[f2657,f2984]) ).
fof(f4677,plain,
! [X0] :
( c_Int_Onat(c_Int_OPls) = c_Divides_Odiv__class_Omod(hAPP(c_Suc,X0),c_Int_Onat(sF2),tc_nat)
| c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(forward_demodulation,[],[f4664,f2778]) ).
fof(f4830,definition,
( spl11_29
<=> sF8 = c_Int_Onat(sF1) ),
introduced(definition,[new_symbols(definition,[spl11_29])],[avatar_definition]) ).
fof(f4831,plain,
( sF8 != c_Int_Onat(sF1)
| spl11_29 ),
inference(avatar_component_clause,[],[f4830]) ).
fof(f4882,plain,
( sF4 = hAPP(c_Suc,hAPP(c_Suc,c_HOL_Ominus__class_Ominus(sF4,c_Int_Onat(sF2),tc_nat)))
| c_Int_Onat(c_Int_OPls) = c_Int_Onat(sF1) ),
inference(superposition,[],[f2997,f2886]) ).
fof(f4890,plain,
sF4 = hAPP(c_Suc,hAPP(c_Suc,c_HOL_Ominus__class_Ominus(sF4,c_Int_Onat(sF2),tc_nat))),
inference(forward_subsumption_resolution,[],[f4882,f3078]) ).
fof(f4931,plain,
( c_Parity_Oeven__odd__class_Oeven(c_Divides_Odiv__class_Odiv(c_Int_Onat(sF2),c_Int_Onat(sF2),tc_nat),tc_nat)
| c_Int_Onat(sF1) != c_Divides_Odiv__class_Omod(sF8,sF4,tc_nat) ),
inference(superposition,[],[f3019,f4109]) ).
fof(f4934,plain,
( c_Parity_Oeven__odd__class_Oeven(c_Int_Onat(sF1),tc_nat)
| c_Int_Onat(sF1) != c_Divides_Odiv__class_Omod(sF8,sF4,tc_nat) ),
inference(forward_demodulation,[],[f4931,f4362]) ).
fof(f4939,plain,
c_Int_Onat(sF1) != c_Divides_Odiv__class_Omod(sF8,sF4,tc_nat),
inference(forward_subsumption_resolution,[],[f4934,f2889]) ).
fof(f5058,plain,
c_SetInterval_Oord__class_OlessThan(sF9,tc_nat) = c_SetInterval_Oord__class_OatLeastAtMost(c_Int_Onat(c_Int_OPls),sF8,tc_nat),
inference(superposition,[],[f3042,f2780]) ).
fof(f5061,plain,
sF10 = c_SetInterval_Oord__class_OatLeastAtMost(c_Int_Onat(c_Int_OPls),sF8,tc_nat),
inference(forward_demodulation,[],[f5058,f2472]) ).
fof(f5507,plain,
( c_Divides_Odiv__class_Omod(sF8,c_Int_Onat(sF2),tc_nat) = c_HOL_Ominus__class_Ominus(sF8,hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onat(sF1)),c_Int_Onat(sF2)),tc_nat)
| ~ spl11_1 ),
inference(superposition,[],[f1191,f4380]) ).
fof(f5508,plain,
c_Divides_Odiv__class_Omod(sF9,c_Int_Onat(sF2),tc_nat) = c_HOL_Ominus__class_Ominus(sF9,hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onat(sF2)),c_Int_Onat(sF2)),tc_nat),
inference(superposition,[],[f1191,f4361]) ).
fof(f5532,plain,
c_Divides_Odiv__class_Omod(sF9,c_Int_Onat(sF2),tc_nat) = c_HOL_Ominus__class_Ominus(sF9,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Int_Onat(sF2)),c_Int_Onat(sF2)),tc_nat),
inference(forward_demodulation,[],[f5508,f2684]) ).
fof(f5533,plain,
( c_Divides_Odiv__class_Omod(sF8,c_Int_Onat(sF2),tc_nat) = c_HOL_Ominus__class_Ominus(sF8,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Int_Onat(sF1)),c_Int_Onat(sF1)),tc_nat)
| ~ spl11_1 ),
inference(forward_demodulation,[],[f5507,f2684]) ).
fof(f5540,plain,
c_Divides_Odiv__class_Omod(sF9,c_Int_Onat(sF2),tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(sF9,c_Int_Onat(sF2),tc_nat),c_Int_Onat(sF2),tc_nat),
inference(forward_demodulation,[],[f5532,f403]) ).
fof(f5541,plain,
( c_Divides_Odiv__class_Omod(sF8,c_Int_Onat(sF2),tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(sF8,c_Int_Onat(sF1),tc_nat),c_Int_Onat(sF1),tc_nat)
| ~ spl11_1 ),
inference(forward_demodulation,[],[f5533,f403]) ).
fof(f5545,plain,
c_HOL_Ominus__class_Ominus(c_Int_Onat(sF2),c_Int_Onat(sF2),tc_nat) = c_Divides_Odiv__class_Omod(sF9,c_Int_Onat(sF2),tc_nat),
inference(forward_demodulation,[],[f5540,f4116]) ).
fof(f5546,plain,
( c_Divides_Odiv__class_Omod(sF8,c_Int_Onat(sF2),tc_nat) = c_HOL_Ominus__class_Ominus(sF8,hAPP(c_Suc,c_Int_Onat(sF1)),tc_nat)
| ~ spl11_1 ),
inference(forward_demodulation,[],[f5541,f2890]) ).
fof(f5547,plain,
c_HOL_Ominus__class_Ominus(c_Int_Onat(sF2),c_Int_Onat(sF2),tc_nat) = c_Divides_Odiv__class_Omod(c_Int_Onat(c_Int_OPls),c_Int_Onat(sF2),tc_nat),
inference(forward_demodulation,[],[f5545,f3264]) ).
fof(f5548,plain,
( c_Divides_Odiv__class_Omod(sF8,c_Int_Onat(sF2),tc_nat) = c_HOL_Ominus__class_Ominus(c_Int_Onat(sF2),c_Int_Onat(sF1),tc_nat)
| ~ spl11_1 ),
inference(forward_demodulation,[],[f5546,f3166]) ).
fof(f5549,plain,
c_Int_Onat(c_Int_OPls) = c_Divides_Odiv__class_Omod(c_Int_Onat(c_Int_OPls),c_Int_Onat(sF2),tc_nat),
inference(forward_demodulation,[],[f5547,f2764]) ).
fof(f5550,plain,
( c_Int_Onat(sF1) = c_Divides_Odiv__class_Omod(sF8,c_Int_Onat(sF2),tc_nat)
| ~ spl11_1 ),
inference(forward_demodulation,[],[f5548,f4110]) ).
fof(f5555,plain,
c_Int_Onat(c_Int_OPls) = c_Divides_Odiv__class_Omod(sF9,c_Int_Onat(sF2),tc_nat),
inference(backward_demodulation,[],[f3264,f5549]) ).
fof(f5824,plain,
( sF8 != c_Int_Onat(sF1)
| c_Int_Onat(c_Int_OPls) = c_Int_Onat(sF2) ),
inference(superposition,[],[f4091,f2874]) ).
fof(f5827,plain,
( sF8 != c_Int_Onat(sF1)
| spl11_6 ),
inference(forward_subsumption_resolution,[],[f5824,f3275]) ).
fof(f5828,plain,
( ~ spl11_29
| spl11_6 ),
inference(avatar_split_clause,[],[f5827,f3274,f4830]) ).
fof(f9181,plain,
( sF9 != c_Int_Onat(sF2)
| sF8 = c_Int_Onat(sF1) ),
inference(superposition,[],[f4093,f2857]) ).
fof(f9182,plain,
( sF9 != c_Int_Onat(sF1)
| sF8 = c_Int_Onat(c_Int_OPls) ),
inference(superposition,[],[f4093,f2874]) ).
fof(f9183,plain,
sF9 != c_Int_Onat(sF1),
inference(forward_subsumption_resolution,[],[f9182,f4473]) ).
fof(f9184,plain,
( sF9 != c_Int_Onat(sF2)
| spl11_29 ),
inference(forward_subsumption_resolution,[],[f9181,f4831]) ).
fof(f9202,plain,
! [X0] :
( c_Divides_Odiv__class_Omod(hAPP(c_Suc,X0),X0,tc_nat) = c_Divides_Odiv__class_Omod(hAPP(c_Suc,c_HOL_Ozero__class_Ozero(tc_nat)),X0,tc_nat)
| ~ class_Divides_Osemiring__div(tc_nat) ),
inference(superposition,[],[f1346,f900]) ).
fof(f9203,plain,
! [X0] :
( hAPP(c_Suc,c_HOL_Ozero__class_Ozero(tc_nat)) = c_Divides_Odiv__class_Omod(hAPP(c_Suc,X0),X0,tc_nat)
| hAPP(c_Suc,c_HOL_Ozero__class_Ozero(tc_nat)) = X0
| ~ class_Divides_Osemiring__div(tc_nat) ),
inference(superposition,[],[f1374,f900]) ).
fof(f9208,plain,
( ~ c_Parity_Oeven__odd__class_Oeven(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat)
| c_Parity_Oeven__odd__class_Oeven(sF4,tc_nat)
| ~ class_Divides_Osemiring__div(tc_nat) ),
inference(superposition,[],[f2962,f900]) ).
fof(f9215,plain,
( ~ c_Parity_Oeven__odd__class_Oeven(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat)
| c_Parity_Oeven__odd__class_Oeven(sF4,tc_nat) ),
inference(forward_subsumption_resolution,[],[f9208,f1988]) ).
fof(f9217,plain,
! [X0] :
( hAPP(c_Suc,c_HOL_Ozero__class_Ozero(tc_nat)) = c_Divides_Odiv__class_Omod(hAPP(c_Suc,X0),X0,tc_nat)
| hAPP(c_Suc,c_HOL_Ozero__class_Ozero(tc_nat)) = X0 ),
inference(forward_subsumption_resolution,[],[f9203,f1988]) ).
fof(f9218,plain,
! [X0] : c_Divides_Odiv__class_Omod(hAPP(c_Suc,X0),X0,tc_nat) = c_Divides_Odiv__class_Omod(hAPP(c_Suc,c_HOL_Ozero__class_Ozero(tc_nat)),X0,tc_nat),
inference(forward_subsumption_resolution,[],[f9202,f1988]) ).
fof(f9223,plain,
( ~ c_Parity_Oeven__odd__class_Oeven(c_Int_Onat(c_Int_OPls),tc_nat)
| c_Parity_Oeven__odd__class_Oeven(sF4,tc_nat) ),
inference(forward_demodulation,[],[f9215,f2409]) ).
fof(f9225,plain,
! [X0] :
( hAPP(c_Suc,c_Int_Onat(c_Int_OPls)) = c_Divides_Odiv__class_Omod(hAPP(c_Suc,X0),X0,tc_nat)
| hAPP(c_Suc,c_HOL_Ozero__class_Ozero(tc_nat)) = X0 ),
inference(forward_demodulation,[],[f9217,f2409]) ).
fof(f9226,plain,
! [X0] : c_Divides_Odiv__class_Omod(hAPP(c_Suc,c_Int_Onat(c_Int_OPls)),X0,tc_nat) = c_Divides_Odiv__class_Omod(hAPP(c_Suc,X0),X0,tc_nat),
inference(forward_demodulation,[],[f9218,f2409]) ).
fof(f9228,plain,
c_Parity_Oeven__odd__class_Oeven(sF4,tc_nat),
inference(forward_subsumption_resolution,[],[f9223,f2759]) ).
fof(f9230,plain,
! [X0] :
( c_Int_Onat(sF1) = c_Divides_Odiv__class_Omod(hAPP(c_Suc,X0),X0,tc_nat)
| hAPP(c_Suc,c_HOL_Ozero__class_Ozero(tc_nat)) = X0 ),
inference(forward_demodulation,[],[f9225,f2874]) ).
fof(f9231,plain,
! [X0] : c_Divides_Odiv__class_Omod(c_Int_Onat(sF1),X0,tc_nat) = c_Divides_Odiv__class_Omod(hAPP(c_Suc,X0),X0,tc_nat),
inference(forward_demodulation,[],[f9226,f2874]) ).
fof(f9233,plain,
! [X0] :
( hAPP(c_Suc,c_Int_Onat(c_Int_OPls)) = X0
| c_Int_Onat(sF1) = c_Divides_Odiv__class_Omod(hAPP(c_Suc,X0),X0,tc_nat) ),
inference(forward_demodulation,[],[f9230,f2409]) ).
fof(f9235,plain,
! [X0] :
( c_Int_Onat(sF1) = X0
| c_Int_Onat(sF1) = c_Divides_Odiv__class_Omod(hAPP(c_Suc,X0),X0,tc_nat) ),
inference(forward_demodulation,[],[f9233,f2874]) ).
fof(f9237,plain,
! [X0] :
( c_Int_Onat(sF1) = c_Divides_Odiv__class_Omod(c_Int_Onat(sF1),X0,tc_nat)
| c_Int_Onat(sF1) = X0 ),
inference(forward_demodulation,[],[f9235,f9231]) ).
fof(f10288,plain,
c_Int_Onat(c_Int_OPls) = c_HOL_Ominus__class_Ominus(c_Int_Onat(sF1),c_Int_Onat(sF2),tc_nat),
inference(superposition,[],[f3178,f2857]) ).
fof(f10400,plain,
( hAPP(c_Suc,c_Divides_Odiv__class_Odiv(c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF4),sF4),c_Int_Onat(sF2),tc_nat),c_Int_Onat(sF2),tc_nat)) = c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF4),sF4),c_Int_Onat(sF2),tc_nat)
| ~ spl11_7 ),
inference(superposition,[],[f2660,f3280]) ).
fof(f10496,plain,
( sF4 = hAPP(c_Suc,c_Divides_Odiv__class_Odiv(c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF4),sF4),c_Int_Onat(sF2),tc_nat),c_Int_Onat(sF2),tc_nat))
| ~ spl11_7 ),
inference(forward_demodulation,[],[f10400,f2692]) ).
fof(f10536,plain,
( ~ c_Parity_Oeven__odd__class_Oeven(sF4,tc_nat)
| ~ c_Parity_Oeven__odd__class_Oeven(c_Divides_Odiv__class_Odiv(c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF4),sF4),c_Int_Onat(sF2),tc_nat),c_Int_Onat(sF2),tc_nat),tc_nat)
| ~ spl11_7 ),
inference(superposition,[],[f1376,f10496]) ).
fof(f10546,plain,
( c_Divides_Odiv__class_Odiv(c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF4),sF4),c_Int_Onat(sF2),tc_nat),c_Int_Onat(sF2),tc_nat) = c_HOL_Ominus__class_Ominus(sF4,c_Int_Onat(sF1),tc_nat)
| ~ spl11_7 ),
inference(superposition,[],[f2883,f10496]) ).
fof(f10573,definition,
( spl11_78
<=> sF4 = c_Int_Onat(sF1) ),
introduced(definition,[new_symbols(definition,[spl11_78])],[avatar_definition]) ).
fof(f10574,plain,
( sF4 != c_Int_Onat(sF1)
| spl11_78 ),
inference(avatar_component_clause,[],[f10573]) ).
fof(f10575,plain,
( sF4 = c_Int_Onat(sF1)
| ~ spl11_78 ),
inference(avatar_component_clause,[],[f10573]) ).
fof(f10583,definition,
( spl11_80
<=> sF4 = sF9 ),
introduced(definition,[new_symbols(definition,[spl11_80])],[avatar_definition]) ).
fof(f10584,plain,
( sF4 = sF9
| ~ spl11_80 ),
inference(avatar_component_clause,[],[f10583]) ).
fof(f10585,plain,
( sF4 != sF9
| spl11_80 ),
inference(avatar_component_clause,[],[f10583]) ).
fof(f10592,definition,
( spl11_82
<=> sF4 = sF8 ),
introduced(definition,[new_symbols(definition,[spl11_82])],[avatar_definition]) ).
fof(f10593,plain,
( sF4 = sF8
| ~ spl11_82 ),
inference(avatar_component_clause,[],[f10592]) ).
fof(f10594,plain,
( sF4 != sF8
| spl11_82 ),
inference(avatar_component_clause,[],[f10592]) ).
fof(f10606,plain,
( sF4 = hAPP(c_Suc,c_HOL_Ominus__class_Ominus(sF4,c_Int_Onat(sF1),tc_nat))
| ~ spl11_7 ),
inference(backward_demodulation,[],[f10496,f10546]) ).
fof(f10628,plain,
( ~ c_Parity_Oeven__odd__class_Oeven(c_Divides_Odiv__class_Odiv(c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF4),sF4),c_Int_Onat(sF2),tc_nat),c_Int_Onat(sF2),tc_nat),tc_nat)
| ~ spl11_7 ),
inference(forward_subsumption_resolution,[],[f10536,f9228]) ).
fof(f10649,plain,
( ~ c_Parity_Oeven__odd__class_Oeven(c_HOL_Ominus__class_Ominus(sF4,c_Int_Onat(sF1),tc_nat),tc_nat)
| ~ spl11_7 ),
inference(forward_demodulation,[],[f10628,f10546]) ).
fof(f10954,plain,
( c_Int_Onat(sF1) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onat(sF2)),c_Int_Onat(c_Int_OPls))),c_Divides_Odiv__class_Omod(c_Int_Onat(sF1),c_Int_Onat(sF2),tc_nat))
| ~ class_Divides_Osemiring__div(tc_nat) ),
inference(superposition,[],[f420,f4356]) ).
fof(f10955,plain,
c_Int_Onat(sF1) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onat(sF2)),c_Int_Onat(c_Int_OPls))),c_Divides_Odiv__class_Omod(c_Int_Onat(sF1),c_Int_Onat(sF2),tc_nat)),
inference(forward_subsumption_resolution,[],[f10954,f1988]) ).
fof(f10959,plain,
c_Int_Onat(sF1) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Divides_Odiv__class_Omod(c_Int_Onat(sF1),c_Int_Onat(sF2),tc_nat)),hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onat(sF2)),c_Int_Onat(c_Int_OPls))),
inference(forward_demodulation,[],[f10955,f1202]) ).
fof(f10963,plain,
c_Int_Onat(sF1) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Divides_Odiv__class_Omod(c_Int_Onat(sF1),c_Int_Onat(sF2),tc_nat)),c_Int_Onat(c_Int_OPls)),
inference(forward_demodulation,[],[f10959,f2758]) ).
fof(f10965,plain,
c_Int_Onat(sF1) = c_Divides_Odiv__class_Omod(c_Int_Onat(sF1),c_Int_Onat(sF2),tc_nat),
inference(forward_demodulation,[],[f10963,f2769]) ).
fof(f12310,plain,
hAPP(c_Suc,sF4) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF8),c_HOL_Ominus__class_Ominus(sF4,c_Int_Onat(sF2),tc_nat)),
inference(superposition,[],[f3012,f4890]) ).
fof(f12418,definition,
( spl11_99
<=> sF4 = c_Int_Onat(sF2) ),
introduced(definition,[new_symbols(definition,[spl11_99])],[avatar_definition]) ).
fof(f12419,plain,
( sF4 != c_Int_Onat(sF2)
| spl11_99 ),
inference(avatar_component_clause,[],[f12418]) ).
fof(f12420,plain,
( sF4 = c_Int_Onat(sF2)
| ~ spl11_99 ),
inference(avatar_component_clause,[],[f12418]) ).
fof(f14818,plain,
( c_Int_Onat(sF2) = hAPP(c_Suc,sF4)
| ~ spl11_78 ),
inference(backward_demodulation,[],[f2857,f10575]) ).
fof(f15155,plain,
( c_Int_Onat(c_Int_OPls) = c_HOL_Ominus__class_Ominus(sF4,c_Int_Onat(sF2),tc_nat)
| ~ spl11_78 ),
inference(backward_demodulation,[],[f10288,f10575]) ).
fof(f15418,plain,
( hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF8),c_Int_Onat(c_Int_OPls)) = hAPP(c_Suc,sF4)
| ~ spl11_78 ),
inference(backward_demodulation,[],[f12310,f15155]) ).
fof(f15666,plain,
( c_Int_Onat(sF2) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF8),c_Int_Onat(c_Int_OPls))
| ~ spl11_78 ),
inference(forward_demodulation,[],[f15418,f14818]) ).
fof(f15759,plain,
( sF8 = c_Int_Onat(sF2)
| ~ spl11_78 ),
inference(forward_demodulation,[],[f15666,f2769]) ).
fof(f15818,plain,
( $false
| ~ spl11_78 ),
inference(forward_subsumption_resolution,[],[f15759,f3049]) ).
fof(f15819,plain,
~ spl11_78,
inference(avatar_contradiction_clause,[],[f15818]) ).
fof(f20674,plain,
( c_Int_Onat(c_Int_OPls) = c_Divides_Odiv__class_Omod(sF4,c_Int_Onat(sF2),tc_nat)
| c_Parity_Oeven__odd__class_Oeven(c_HOL_Ominus__class_Ominus(sF4,c_Int_Onat(sF1),tc_nat),tc_nat)
| ~ spl11_7 ),
inference(superposition,[],[f4677,f10606]) ).
fof(f20711,plain,
( c_Int_Onat(c_Int_OPls) = c_Divides_Odiv__class_Omod(sF4,c_Int_Onat(sF2),tc_nat)
| ~ spl11_7 ),
inference(forward_subsumption_resolution,[],[f20674,f10649]) ).
fof(f27047,plain,
( c_Int_Onat(sF1) = c_Divides_Odiv__class_Omod(sF8,sF4,tc_nat)
| ~ spl11_1
| ~ spl11_99 ),
inference(backward_demodulation,[],[f5550,f12420]) ).
fof(f28352,plain,
( $false
| ~ spl11_1
| ~ spl11_99 ),
inference(forward_subsumption_resolution,[],[f27047,f4939]) ).
fof(f28353,plain,
( ~ spl11_1
| ~ spl11_99 ),
inference(avatar_contradiction_clause,[],[f28352]) ).
fof(f34253,plain,
! [X0] :
( hAPP(c_Suc,c_Int_Onat(sF1)) = c_Divides_Odiv__class_Omod(hAPP(c_Suc,c_Int_Onat(sF1)),X0,tc_nat)
| hAPP(c_Suc,c_Int_Onat(sF1)) = X0
| c_Int_Onat(sF1) = X0 ),
inference(superposition,[],[f1374,f9237]) ).
fof(f34268,plain,
! [X0] :
( c_Int_Onat(sF2) = c_Divides_Odiv__class_Omod(c_Int_Onat(sF2),X0,tc_nat)
| hAPP(c_Suc,c_Int_Onat(sF1)) = X0
| c_Int_Onat(sF1) = X0 ),
inference(forward_demodulation,[],[f34253,f2857]) ).
fof(f34271,plain,
! [X0] :
( c_Int_Onat(sF2) = c_Divides_Odiv__class_Omod(c_Int_Onat(sF2),X0,tc_nat)
| c_Int_Onat(sF2) = X0
| c_Int_Onat(sF1) = X0 ),
inference(forward_demodulation,[],[f34268,f2857]) ).
fof(f34282,plain,
! [X0] :
( hAPP(c_Suc,c_Int_Onat(sF2)) = c_Divides_Odiv__class_Omod(hAPP(c_Suc,c_Int_Onat(sF2)),X0,tc_nat)
| hAPP(c_Suc,c_Int_Onat(sF2)) = X0
| c_Int_Onat(sF2) = X0
| c_Int_Onat(sF1) = X0 ),
inference(superposition,[],[f1374,f34271]) ).
fof(f34291,plain,
! [X0] :
( sF8 = c_Divides_Odiv__class_Omod(sF8,X0,tc_nat)
| hAPP(c_Suc,c_Int_Onat(sF2)) = X0
| c_Int_Onat(sF2) = X0
| c_Int_Onat(sF1) = X0 ),
inference(forward_demodulation,[],[f34282,f2982]) ).
fof(f34294,plain,
! [X0] :
( sF8 = c_Divides_Odiv__class_Omod(sF8,X0,tc_nat)
| sF8 = X0
| c_Int_Onat(sF2) = X0
| c_Int_Onat(sF1) = X0 ),
inference(forward_demodulation,[],[f34291,f2982]) ).
fof(f34306,plain,
! [X0] :
( hAPP(c_Suc,sF8) = c_Divides_Odiv__class_Omod(hAPP(c_Suc,sF8),X0,tc_nat)
| hAPP(c_Suc,sF8) = X0
| sF8 = X0
| c_Int_Onat(sF2) = X0
| c_Int_Onat(sF1) = X0 ),
inference(superposition,[],[f1374,f34294]) ).
fof(f34315,plain,
! [X0] :
( sF9 = c_Divides_Odiv__class_Omod(sF9,X0,tc_nat)
| hAPP(c_Suc,sF8) = X0
| sF8 = X0
| c_Int_Onat(sF2) = X0
| c_Int_Onat(sF1) = X0 ),
inference(forward_demodulation,[],[f34306,f2076]) ).
fof(f34318,plain,
! [X0] :
( sF9 = c_Divides_Odiv__class_Omod(sF9,X0,tc_nat)
| sF9 = X0
| sF8 = X0
| c_Int_Onat(sF2) = X0
| c_Int_Onat(sF1) = X0 ),
inference(forward_demodulation,[],[f34315,f2076]) ).
fof(f42879,plain,
( c_Divides_Odiv__class_Omod(hAPP(c_Suc,c_Int_Onat(c_Int_OPls)),c_Int_Onat(sF2),tc_nat) = c_Divides_Odiv__class_Omod(hAPP(c_Suc,sF4),c_Int_Onat(sF2),tc_nat)
| ~ spl11_7 ),
inference(superposition,[],[f1346,f20711]) ).
fof(f42893,plain,
( c_Divides_Odiv__class_Omod(c_Int_Onat(sF1),c_Int_Onat(sF2),tc_nat) = c_Divides_Odiv__class_Omod(hAPP(c_Suc,sF4),c_Int_Onat(sF2),tc_nat)
| ~ spl11_7 ),
inference(forward_demodulation,[],[f42879,f2874]) ).
fof(f42900,plain,
( c_Int_Onat(sF1) = c_Divides_Odiv__class_Omod(hAPP(c_Suc,sF4),c_Int_Onat(sF2),tc_nat)
| ~ spl11_7 ),
inference(forward_demodulation,[],[f42893,f10965]) ).
fof(f96516,plain,
( sF9 = c_Int_Onat(sF2)
| sF9 = c_Int_Onat(sF1)
| sF8 = sF9
| sF9 = c_Int_Onat(c_Int_OPls)
| sF4 = sF9
| sF4 = sF8
| sF4 = c_Int_Onat(sF2)
| sF4 = c_Int_Onat(sF1) ),
inference(superposition,[],[f3036,f34318]) ).
fof(f96583,plain,
( sF9 = c_Int_Onat(sF1)
| sF8 = sF9
| sF9 = c_Int_Onat(c_Int_OPls)
| sF4 = sF9
| sF4 = sF8
| sF4 = c_Int_Onat(sF2)
| sF4 = c_Int_Onat(sF1)
| spl11_29 ),
inference(forward_subsumption_resolution,[],[f96516,f9184]) ).
fof(f96607,plain,
( sF8 = sF9
| sF9 = c_Int_Onat(c_Int_OPls)
| sF4 = sF9
| sF4 = sF8
| sF4 = c_Int_Onat(sF2)
| sF4 = c_Int_Onat(sF1)
| spl11_29 ),
inference(forward_subsumption_resolution,[],[f96583,f9183]) ).
fof(f96645,plain,
( sF9 = c_Int_Onat(c_Int_OPls)
| sF4 = sF9
| sF4 = sF8
| sF4 = c_Int_Onat(sF2)
| sF4 = c_Int_Onat(sF1)
| spl11_29 ),
inference(forward_subsumption_resolution,[],[f96607,f3041]) ).
fof(f96650,plain,
( sF4 = sF9
| sF4 = sF8
| sF4 = c_Int_Onat(sF2)
| sF4 = c_Int_Onat(sF1)
| spl11_23
| spl11_29 ),
inference(forward_subsumption_resolution,[],[f96645,f4255]) ).
fof(f96653,plain,
( sF4 = sF8
| sF4 = c_Int_Onat(sF2)
| sF4 = c_Int_Onat(sF1)
| spl11_23
| spl11_29
| spl11_80 ),
inference(forward_subsumption_resolution,[],[f96650,f10585]) ).
fof(f96656,plain,
( sF4 = c_Int_Onat(sF2)
| sF4 = c_Int_Onat(sF1)
| spl11_23
| spl11_29
| spl11_80
| spl11_82 ),
inference(forward_subsumption_resolution,[],[f96653,f10594]) ).
fof(f96659,plain,
( sF4 = c_Int_Onat(sF1)
| spl11_23
| spl11_29
| spl11_80
| spl11_82
| spl11_99 ),
inference(forward_subsumption_resolution,[],[f96656,f12419]) ).
fof(f96661,plain,
( $false
| spl11_23
| spl11_29
| spl11_78
| spl11_80
| spl11_82
| spl11_99 ),
inference(forward_subsumption_resolution,[],[f96659,f10574]) ).
fof(f96662,plain,
( spl11_23
| spl11_29
| spl11_78
| spl11_80
| spl11_82
| spl11_99 ),
inference(avatar_contradiction_clause,[],[f96661]) ).
fof(f96666,plain,
( sF9 = hAPP(c_Suc,sF4)
| ~ spl11_82 ),
inference(backward_demodulation,[],[f2076,f10593]) ).
fof(f97663,plain,
( c_Int_Onat(sF1) = c_Divides_Odiv__class_Omod(sF9,c_Int_Onat(sF2),tc_nat)
| ~ spl11_7
| ~ spl11_82 ),
inference(backward_demodulation,[],[f42900,f96666]) ).
fof(f97718,plain,
( c_Int_Onat(c_Int_OPls) = c_Int_Onat(sF1)
| ~ spl11_7
| ~ spl11_82 ),
inference(forward_demodulation,[],[f97663,f5555]) ).
fof(f97736,plain,
( $false
| ~ spl11_7
| ~ spl11_82 ),
inference(forward_subsumption_resolution,[],[f97718,f3078]) ).
fof(f97737,plain,
( ~ spl11_7
| ~ spl11_82 ),
inference(avatar_contradiction_clause,[],[f97736]) ).
fof(f98209,plain,
( ! [X0] : c_SetInterval_Oord__class_OatLeastAtMost(X0,sF8,tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(X0,sF4,tc_nat)
| ~ spl11_80 ),
inference(forward_demodulation,[],[f3042,f10584]) ).
fof(f98674,plain,
( sF10 = c_SetInterval_Oord__class_OatLeastLessThan(c_Int_Onat(c_Int_OPls),sF4,tc_nat)
| ~ spl11_80 ),
inference(backward_demodulation,[],[f5061,f98209]) ).
fof(f98827,plain,
( sF10 = c_SetInterval_Oord__class_OlessThan(sF4,tc_nat)
| ~ spl11_80 ),
inference(forward_demodulation,[],[f98674,f2780]) ).
fof(f98905,plain,
( sF5 = sF10
| ~ spl11_80 ),
inference(forward_demodulation,[],[f98827,f2471]) ).
fof(f98956,plain,
( $false
| ~ spl11_80 ),
inference(forward_subsumption_resolution,[],[f98905,f2079]) ).
fof(f98957,plain,
~ spl11_80,
inference(avatar_contradiction_clause,[],[f98956]) ).
cnf(s3,plain,
spl11_1,
inference(sat_conversion,[],[f3099]) ).
cnf(s5,plain,
( spl11_6
| spl11_7 ),
inference(sat_conversion,[],[f3281]) ).
cnf(s12,plain,
~ spl11_6,
inference(sat_conversion,[],[f3667]) ).
cnf(s31,plain,
~ spl11_23,
inference(sat_conversion,[],[f4476]) ).
cnf(s42,plain,
( spl11_6
| ~ spl11_29 ),
inference(sat_conversion,[],[f5828]) ).
cnf(s168,plain,
~ spl11_78,
inference(sat_conversion,[],[f15819]) ).
cnf(s393,plain,
( ~ spl11_1
| ~ spl11_99 ),
inference(sat_conversion,[],[f28353]) ).
cnf(s1715,plain,
( spl11_23
| spl11_29
| spl11_78
| spl11_80
| spl11_82
| spl11_99 ),
inference(sat_conversion,[],[f96662]) ).
cnf(s1729,plain,
( ~ spl11_7
| ~ spl11_82 ),
inference(sat_conversion,[],[f97737]) ).
cnf(s1744,plain,
~ spl11_80,
inference(sat_conversion,[],[f98957]) ).
cnf(s1746,plain,
( spl11_23
| spl11_29
| spl11_78
| spl11_82
| spl11_99 ),
inference(rat,[],[s1715,s1744]) ).
cnf(s1785,plain,
~ spl11_29,
inference(rat,[],[s42,s12]) ).
cnf(s1788,plain,
spl11_7,
inference(rat,[],[s5,s12]) ).
cnf(s1789,plain,
~ spl11_82,
inference(rat,[],[s1729,s1788]) ).
cnf(s1795,plain,
spl11_99,
inference(rat,[],[s1746,s1785,s31,s168,s1789]) ).
cnf(s1798,plain,
~ spl11_1,
inference(rat,[],[s393,s1795]) ).
cnf(s1802,plain,
$false,
inference(rat,[],[s3,s1798]) ).
fof(f98989,plain,
$false,
inference(avatar_sat_refutation,[],[s1802]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV575-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n015.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 11:58:02 UTC 2026
% 0.08/0.18 % CPUTime :
% 0.08/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.08/0.21 Running first-order theorem proving
% 0.08/0.21 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.71/2.50 % (2575433)Input is clausal, will run a generic CNF schedule.
% 12.71/2.50 % (2575438)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2649835979:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 12.71/2.50 % (2575442)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=976652125:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 12.71/2.50 % (2575444)dis-21_1_sil=8000:lcm=predicate:random_seed=203300833:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 12.71/2.50 % (2575440)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=4167476000:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 12.71/2.50 % (2575439)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=256724693:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 12.71/2.50 % (2575441)lrs+10_1_sil=8000:sp=occurrence:random_seed=4042153660:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 12.71/2.50 % (2575443)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=308057537:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 12.71/2.50 % (2575444)Instruction limit reached!
% 12.71/2.50 % (2575444)------------------------------
% 12.71/2.50 % (2575444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.71/2.50 % (2575444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.71/2.50 % (2575444)CaDiCaL version: 2.1.3
% 12.71/2.50 % (2575444)Termination reason: Instruction limit
% 12.71/2.50 % (2575444)Termination phase: Saturation
% 12.71/2.50 % (2575444)Time elapsed: 0.067 s
% 12.71/2.50 % (2575444)Peak memory usage: 90 MB
% 12.71/2.50 % (2575444)Instructions burned: 117 (million)
% 12.71/2.50 % (2575441)Instruction limit reached!
% 12.71/2.50 % (2575441)------------------------------
% 12.71/2.50 % (2575441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.71/2.50 % (2575441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.71/2.50 % (2575441)CaDiCaL version: 2.1.3
% 12.71/2.50 % (2575441)Termination reason: Instruction limit
% 12.71/2.50 % (2575441)Termination phase: Saturation
% 12.71/2.50 % (2575441)Time elapsed: 0.068 s
% 12.71/2.50 % (2575441)Peak memory usage: 90 MB
% 12.71/2.50 % (2575441)Instructions burned: 107 (million)
% 12.71/2.50 % (2575442)Instruction limit reached!
% 12.71/2.50 % (2575442)------------------------------
% 12.71/2.50 % (2575442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.71/2.50 % (2575442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.71/2.50 % (2575442)CaDiCaL version: 2.1.3
% 12.71/2.50 % (2575442)Termination reason: Instruction limit
% 12.71/2.50 % (2575442)Termination phase: Saturation
% 12.71/2.50 % (2575442)Time elapsed: 0.077 s
% 12.71/2.50 % (2575442)Peak memory usage: 90 MB
% 12.71/2.50 % (2575442)Instructions burned: 114 (million)
% 12.71/2.50 % (2575443)Instruction limit reached!
% 12.71/2.50 % (2575443)------------------------------
% 12.71/2.50 % (2575443)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.71/2.50 % (2575443)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.71/2.50 % (2575443)CaDiCaL version: 2.1.3
% 12.71/2.50 % (2575443)Termination reason: Instruction limit
% 12.71/2.50 % (2575443)Termination phase: Saturation
% 12.71/2.50 % (2575443)Time elapsed: 0.110 s
% 12.71/2.50 % (2575443)Peak memory usage: 90 MB
% 12.71/2.50 % (2575443)Instructions burned: 181 (million)
% 12.71/2.50 % (2575453)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=3953322985:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 12.71/2.50 % (2575452)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=209061059:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 12.71/2.50 % (2575452)Refutation not found, incomplete strategy
% 12.71/2.50 % (2575452)------------------------------
% 12.71/2.50 % (2575452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.71/2.50 % (2575452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.71/2.50 % (2575452)CaDiCaL version: 2.1.3
% 22.15/4.02 % (2575452)Termination reason: Refutation not found, incomplete strategy
% 22.15/4.02 % (2575452)Time elapsed: 0.016 s
% 22.15/4.02 % (2575452)Peak memory usage: 89 MB
% 22.15/4.02 % (2575452)Instructions burned: 22 (million)
% 22.15/4.02 % (2575454)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2974359079:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 22.15/4.02 % (2575455)lrs+10_64_to=lpo:sil=8000:random_seed=1185456897:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 22.15/4.02 % (2575453)Instruction limit reached!
% 22.15/4.02 % (2575453)------------------------------
% 22.15/4.02 % (2575453)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.15/4.02 % (2575453)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.15/4.02 % (2575453)CaDiCaL version: 2.1.3
% 22.15/4.02 % (2575453)Termination reason: Instruction limit
% 22.15/4.02 % (2575453)Termination phase: Saturation
% 22.15/4.02 % (2575453)Time elapsed: 0.095 s
% 22.15/4.02 % (2575453)Peak memory usage: 91 MB
% 22.15/4.02 % (2575453)Instructions burned: 190 (million)
% 22.15/4.02 % (2575454)Instruction limit reached!
% 22.15/4.02 % (2575454)------------------------------
% 22.15/4.02 % (2575454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.15/4.02 % (2575454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.15/4.02 % (2575454)CaDiCaL version: 2.1.3
% 22.15/4.02 % (2575454)Termination reason: Instruction limit
% 22.15/4.02 % (2575454)Termination phase: Saturation
% 22.15/4.02 % (2575454)Time elapsed: 0.129 s
% 22.15/4.02 % (2575454)Peak memory usage: 91 MB
% 22.15/4.02 % (2575454)Instructions burned: 221 (million)
% 22.15/4.02 % (2575455)Instruction limit reached!
% 22.15/4.02 % (2575455)------------------------------
% 22.15/4.02 % (2575455)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.15/4.02 % (2575455)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.15/4.02 % (2575455)CaDiCaL version: 2.1.3
% 22.15/4.02 % (2575455)Termination reason: Instruction limit
% 22.15/4.02 % (2575455)Termination phase: Saturation
% 22.15/4.02 % (2575455)Time elapsed: 0.081 s
% 22.15/4.02 % (2575455)Peak memory usage: 90 MB
% 22.15/4.02 % (2575455)Instructions burned: 126 (million)
% 22.15/4.02 % (2575460)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=4186924772:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 22.15/4.02 % (2575452)------------------------------
% 22.15/4.02 % (2575452)------------------------------
% 22.15/4.02 % (2575461)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=985147475:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 22.15/4.02 % (2575462)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=2463512973:i=3394:sd=4:ss=included:sgt=64_2993 on theBenchmark for (2993ds/3394Mi)
% 22.15/4.02 % (2575460)Instruction limit reached!
% 22.15/4.02 % (2575460)------------------------------
% 22.15/4.02 % (2575460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.15/4.02 % (2575460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.15/4.02 % (2575460)CaDiCaL version: 2.1.3
% 22.15/4.02 % (2575460)Termination reason: Instruction limit
% 22.15/4.02 % (2575460)Termination phase: Saturation
% 22.15/4.02 % (2575460)Time elapsed: 0.124 s
% 22.15/4.02 % (2575460)Peak memory usage: 91 MB
% 22.15/4.02 % (2575460)Instructions burned: 195 (million)
% 22.15/4.02 % (2575461)Instruction limit reached!
% 22.15/4.02 % (2575461)------------------------------
% 22.15/4.02 % (2575461)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.15/4.02 % (2575461)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.15/4.02 % (2575461)CaDiCaL version: 2.1.3
% 22.15/4.02 % (2575461)Termination reason: Instruction limit
% 22.15/4.02 % (2575461)Termination phase: Saturation
% 22.15/4.02 % (2575461)Time elapsed: 0.091 s
% 22.15/4.02 % (2575461)Peak memory usage: 91 MB
% 22.15/4.02 % (2575461)Instructions burned: 158 (million)
% 22.15/4.02 % (2575464)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=45732793:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2992 on theBenchmark for (2992ds/106Mi)
% 22.15/4.02 % (2575464)Instruction limit reached!
% 22.15/4.02 % (2575464)------------------------------
% 22.15/4.02 % (2575464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.15/4.02 % (2575464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.81/5.80 % (2575464)CaDiCaL version: 2.1.3
% 35.81/5.80 % (2575464)Termination reason: Instruction limit
% 35.81/5.80 % (2575464)Termination phase: Saturation
% 35.81/5.80 % (2575464)Time elapsed: 0.052 s
% 35.81/5.80 % (2575464)Peak memory usage: 90 MB
% 35.81/5.80 % (2575464)Instructions burned: 106 (million)
% 35.81/5.80 % (2575467)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2458920739:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 35.81/5.80 % (2575467)Refutation not found, incomplete strategy
% 35.81/5.80 % (2575467)------------------------------
% 35.81/5.80 % (2575467)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.81/5.80 % (2575467)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.81/5.80 % (2575467)CaDiCaL version: 2.1.3
% 35.81/5.80 % (2575467)Termination reason: Refutation not found, incomplete strategy
% 35.81/5.80 % (2575467)Time elapsed: 0.025 s
% 35.81/5.80 % (2575467)Peak memory usage: 90 MB
% 35.81/5.80 % (2575467)Instructions burned: 36 (million)
% 35.81/5.80 % (2575468)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3859973892:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 35.81/5.80 % (2575470)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3617814936:cond=fast:i=5208:av=off_2990 on theBenchmark for (2990ds/5208Mi)
% 35.81/5.80 % (2575468)Instruction limit reached!
% 35.81/5.80 % (2575468)------------------------------
% 35.81/5.80 % (2575468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.81/5.80 % (2575468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.81/5.80 % (2575468)CaDiCaL version: 2.1.3
% 35.81/5.80 % (2575468)Termination reason: Instruction limit
% 35.81/5.80 % (2575468)Termination phase: Saturation
% 35.81/5.80 % (2575468)Time elapsed: 0.135 s
% 35.81/5.80 % (2575468)Peak memory usage: 90 MB
% 35.81/5.80 % (2575468)Instructions burned: 242 (million)
% 35.81/5.80 % (2575467)------------------------------
% 35.81/5.80 % (2575467)------------------------------
% 35.81/5.80 % (2575474)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1169922654:i=134:sd=2:doe=on:ss=axioms:sgt=14_2988 on theBenchmark for (2988ds/134Mi)
% 35.81/5.80 % (2575474)Instruction limit reached!
% 35.81/5.80 % (2575474)------------------------------
% 35.81/5.80 % (2575474)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.81/5.80 % (2575474)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.81/5.80 % (2575474)CaDiCaL version: 2.1.3
% 35.81/5.80 % (2575474)Termination reason: Instruction limit
% 35.81/5.80 % (2575474)Termination phase: Saturation
% 35.81/5.80 % (2575474)Time elapsed: 0.085 s
% 35.81/5.80 % (2575474)Peak memory usage: 90 MB
% 35.81/5.80 % (2575474)Instructions burned: 134 (million)
% 35.81/5.80 % (2575475)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=4227720053:i=499:bd=all_2987 on theBenchmark for (2987ds/499Mi)
% 35.81/5.80 % (2575477)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=1160325120:i=191:fgj=on:bd=all_2985 on theBenchmark for (2985ds/191Mi)
% 35.81/5.80 % (2575477)Instruction limit reached!
% 35.81/5.80 % (2575477)------------------------------
% 35.81/5.80 % (2575477)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.81/5.80 % (2575477)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.81/5.80 % (2575477)CaDiCaL version: 2.1.3
% 35.81/5.80 % (2575477)Termination reason: Instruction limit
% 35.81/5.80 % (2575477)Termination phase: Saturation
% 35.81/5.80 % (2575477)Time elapsed: 0.120 s
% 35.81/5.80 % (2575477)Peak memory usage: 91 MB
% 35.81/5.80 % (2575477)Instructions burned: 191 (million)
% 35.81/5.80 % (2575475)Instruction limit reached!
% 35.81/5.80 % (2575475)------------------------------
% 35.81/5.80 % (2575475)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.81/5.80 % (2575475)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.81/5.80 % (2575475)CaDiCaL version: 2.1.3
% 35.81/5.80 % (2575475)Termination reason: Instruction limit
% 35.81/5.80 % (2575475)Termination phase: Saturation
% 35.81/5.80 % (2575475)Time elapsed: 0.293 s
% 35.81/5.80 % (2575475)Peak memory usage: 93 MB
% 35.81/5.80 % (2575475)Instructions burned: 499 (million)
% 35.81/5.80 % (2575480)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1486337689:i=264:kws=precedence:fsr=off_2983 on theBenchmark for (2983ds/264Mi)
% 49.50/8.93 % (2575481)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=4020409724:cond=on:i=156:bs=on:gtg=exists_all:er=known_2982 on theBenchmark for (2982ds/156Mi)
% 49.50/8.93 % (2575481)Instruction limit reached!
% 49.50/8.93 % (2575481)------------------------------
% 49.50/8.93 % (2575481)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.50/8.93 % (2575481)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.50/8.93 % (2575481)CaDiCaL version: 2.1.3
% 49.50/8.93 % (2575481)Termination reason: Instruction limit
% 49.50/8.93 % (2575481)Termination phase: Saturation
% 49.50/8.93 % (2575481)Time elapsed: 0.099 s
% 49.50/8.93 % (2575481)Peak memory usage: 91 MB
% 49.50/8.93 % (2575481)Instructions burned: 156 (million)
% 49.50/8.93 % (2575480)Instruction limit reached!
% 49.50/8.93 % (2575480)------------------------------
% 49.50/8.93 % (2575480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.50/8.93 % (2575480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.50/8.93 % (2575480)CaDiCaL version: 2.1.3
% 49.50/8.93 % (2575480)Termination reason: Instruction limit
% 49.50/8.93 % (2575480)Termination phase: Saturation
% 49.50/8.93 % (2575480)Time elapsed: 0.165 s
% 49.50/8.93 % (2575480)Peak memory usage: 93 MB
% 49.50/8.93 % (2575480)Instructions burned: 264 (million)
% 49.50/8.93 % (2575484)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=862167761:i=3256:kws=precedence:bd=preordered:av=off_2980 on theBenchmark for (2980ds/3256Mi)
% 49.50/8.93 % (2575485)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1529812509:i=537:av=off:ss=included_2979 on theBenchmark for (2979ds/537Mi)
% 49.50/8.93 % (2575485)Instruction limit reached!
% 49.50/8.93 % (2575485)------------------------------
% 49.50/8.93 % (2575485)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.50/8.93 % (2575485)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.50/8.93 % (2575485)CaDiCaL version: 2.1.3
% 49.50/8.93 % (2575485)Termination reason: Instruction limit
% 49.50/8.93 % (2575485)Termination phase: Saturation
% 49.50/8.93 % (2575485)Time elapsed: 0.302 s
% 49.50/8.93 % (2575485)Peak memory usage: 92 MB
% 49.50/8.93 % (2575485)Instructions burned: 537 (million)
% 49.50/8.93 % (2575488)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=290333290:i=180:bd=preordered:av=off_2975 on theBenchmark for (2975ds/180Mi)
% 49.50/8.93 % (2575488)Instruction limit reached!
% 49.50/8.93 % (2575488)------------------------------
% 49.50/8.93 % (2575488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.50/8.93 % (2575488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.50/8.93 % (2575488)CaDiCaL version: 2.1.3
% 49.50/8.93 % (2575488)Termination reason: Instruction limit
% 49.50/8.93 % (2575488)Termination phase: Saturation
% 49.50/8.93 % (2575488)Time elapsed: 0.102 s
% 49.50/8.93 % (2575488)Peak memory usage: 91 MB
% 49.50/8.93 % (2575488)Instructions burned: 181 (million)
% 49.50/8.93 % (2575490)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=2600920154:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2972 on theBenchmark for (2972ds/10307Mi)
% 49.50/8.93 % (2575462)Instruction limit reached!
% 49.50/8.93 % (2575462)------------------------------
% 49.50/8.93 % (2575462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.50/8.93 % (2575462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.50/8.93 % (2575462)CaDiCaL version: 2.1.3
% 49.50/8.93 % (2575462)Termination reason: Instruction limit
% 49.50/8.93 % (2575462)Termination phase: Saturation
% 49.50/8.93 % (2575462)Time elapsed: 2.170 s
% 49.50/8.93 % (2575462)Peak memory usage: 148 MB
% 49.50/8.93 % (2575462)Instructions burned: 3395 (million)
% 49.50/8.93 % (2575492)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=23086385:i=412:gtgl=4:gtg=exists_all_2970 on theBenchmark for (2970ds/412Mi)
% 49.50/8.93 % (2575492)Instruction limit reached!
% 49.50/8.93 % (2575492)------------------------------
% 49.50/8.93 % (2575492)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.50/8.93 % (2575492)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.50/8.93 % (2575492)CaDiCaL version: 2.1.3
% 49.50/8.93 % (2575492)Termination reason: Instruction limit
% 49.50/8.93 % (2575492)Termination phase: Saturation
% 49.50/8.93 % (2575492)Time elapsed: 0.221 s
% 49.50/8.93 % (2575492)Peak memory usage: 93 MB
% 49.50/8.93 % (2575492)Instructions burned: 413 (million)
% 49.50/8.93 % (2575494)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=3940072642:s2pl=no:i=8478:s2at=4:nm=6_2966 on theBenchmark for (2966ds/8478Mi)
% 49.50/8.93 % (2575484)Instruction limit reached!
% 49.50/8.93 % (2575484)------------------------------
% 49.50/8.93 % (2575484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.50/8.93 % (2575484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.50/8.93 % (2575484)CaDiCaL version: 2.1.3
% 49.50/8.93 % (2575484)Termination reason: Instruction limit
% 49.50/8.93 % (2575484)Termination phase: Saturation
% 49.50/8.93 % (2575484)Time elapsed: 1.965 s
% 49.50/8.93 % (2575484)Peak memory usage: 152 MB
% 49.50/8.93 % (2575484)Instructions burned: 3257 (million)
% 49.50/8.93 % (2575470)Instruction limit reached!
% 49.50/8.93 % (2575470)------------------------------
% 49.50/8.93 % (2575470)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.50/8.93 % (2575470)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.50/8.93 % (2575470)CaDiCaL version: 2.1.3
% 49.50/8.93 % (2575470)Termination reason: Instruction limit
% 49.50/8.93 % (2575470)Termination phase: Saturation
% 49.50/8.93 % (2575470)Time elapsed: 3.135 s
% 49.50/8.93 % (2575470)Peak memory usage: 162 MB
% 49.50/8.93 % (2575470)Instructions burned: 5208 (million)
% 49.50/8.93 % (2575496)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=4114534341:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2958 on theBenchmark for (2958ds/303Mi)
% 49.50/8.93 % (2575497)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2165203568:st=4:i=720:sd=3:fsr=off:ss=axioms_2957 on theBenchmark for (2957ds/720Mi)
% 49.50/8.93 % (2575496)Instruction limit reached!
% 49.50/8.93 % (2575496)------------------------------
% 49.50/8.93 % (2575496)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.50/8.93 % (2575496)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.50/8.93 % (2575496)CaDiCaL version: 2.1.3
% 49.50/8.93 % (2575496)Termination reason: Instruction limit
% 49.50/8.93 % (2575496)Termination phase: Saturation
% 49.50/8.93 % (2575496)Time elapsed: 0.176 s
% 49.50/8.93 % (2575496)Peak memory usage: 91 MB
% 49.50/8.93 % (2575496)Instructions burned: 304 (million)
% 49.50/8.93 % (2575500)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=1337831314:i=598:bs=on:bd=preordered:av=off:ss=axioms_2955 on theBenchmark for (2955ds/598Mi)
% 49.50/8.93 % (2575497)Instruction limit reached!
% 49.50/8.93 % (2575497)------------------------------
% 49.50/8.93 % (2575497)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.50/8.93 % (2575497)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.50/8.93 % (2575497)CaDiCaL version: 2.1.3
% 49.50/8.93 % (2575497)Termination reason: Instruction limit
% 49.50/8.93 % (2575497)Termination phase: Saturation
% 49.50/8.93 % (2575497)Time elapsed: 0.320 s
% 49.50/8.93 % (2575497)Peak memory usage: 91 MB
% 49.50/8.93 % (2575497)Instructions burned: 721 (million)
% 49.50/8.93 % (2575502)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=3753383142:i=2989:sd=3:ss=axioms:sgt=60_2952 on theBenchmark for (2952ds/2989Mi)
% 49.50/8.93 % (2575500)Instruction limit reached!
% 49.50/8.93 % (2575500)------------------------------
% 49.50/8.93 % (2575500)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.50/8.93 % (2575500)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.50/8.93 % (2575500)CaDiCaL version: 2.1.3
% 49.50/8.93 % (2575500)Termination reason: Instruction limit
% 49.50/8.93 % (2575500)Termination phase: Saturation
% 49.50/8.93 % (2575500)Time elapsed: 0.359 s
% 49.50/8.93 % (2575500)Peak memory usage: 94 MB
% 49.50/8.93 % (2575500)Instructions burned: 598 (million)
% 49.50/8.93 % (2575504)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=1363865778:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2950 on theBenchmark for (2950ds/1997Mi)
% 49.50/8.93 % (2575504)Instruction limit reached!
% 49.50/8.93 % (2575504)------------------------------
% 49.50/8.93 % (2575504)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.50/8.93 % (2575504)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.50/8.93 % (2575504)CaDiCaL version: 2.1.3
% 49.50/8.93 % (2575504)Termination reason: Instruction limit
% 49.50/8.93 % (2575504)Termination phase: Saturation
% 49.50/8.93 % (2575504)Time elapsed: 1.234 s
% 49.50/8.93 % (2575504)Peak memory usage: 144 MB
% 49.50/8.93 % (2575504)Instructions burned: 1997 (million)
% 49.50/8.93 % (2575506)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=2876166894:i=2088:bd=preordered:av=off_2936 on theBenchmark for (2936ds/2088Mi)
% 49.50/8.93 % (2575502)Instruction limit reached!
% 49.50/8.93 % (2575502)------------------------------
% 49.50/8.93 % (2575502)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.50/8.93 % (2575502)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.50/8.93 % (2575502)CaDiCaL version: 2.1.3
% 49.50/8.93 % (2575502)Termination reason: Instruction limit
% 49.50/8.93 % (2575502)Termination phase: Saturation
% 49.50/8.93 % (2575502)Time elapsed: 1.758 s
% 49.50/8.93 % (2575502)Peak memory usage: 145 MB
% 49.50/8.93 % (2575502)Instructions burned: 2990 (million)
% 49.50/8.93 % (2575508)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=1122635757:i=1098:nicw=on_2933 on theBenchmark for (2933ds/1098Mi)
% 49.50/8.93 % (2575508)Instruction limit reached!
% 49.50/8.93 % (2575508)------------------------------
% 49.50/8.93 % (2575508)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.50/8.93 % (2575508)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.50/8.93 % (2575508)CaDiCaL version: 2.1.3
% 49.50/8.93 % (2575508)Termination reason: Instruction limit
% 49.50/8.93 % (2575508)Termination phase: Saturation
% 49.50/8.93 % (2575508)Time elapsed: 0.679 s
% 49.50/8.93 % (2575508)Peak memory usage: 101 MB
% 49.50/8.93 % (2575508)Instructions burned: 1099 (million)
% 49.50/8.93 % (2575510)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=3253326501:i=433:bd=preordered_2925 on theBenchmark for (2925ds/433Mi)
% 49.50/8.93 % (2575510)Refutation not found, incomplete strategy
% 49.50/8.93 % (2575510)------------------------------
% 49.50/8.93 % (2575510)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.50/8.93 % (2575510)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.50/8.93 % (2575510)CaDiCaL version: 2.1.3
% 49.50/8.93 % (2575510)Termination reason: Refutation not found, incomplete strategy
% 49.50/8.93 % (2575510)Time elapsed: 0.077 s
% 49.50/8.93 % (2575510)Peak memory usage: 91 MB
% 49.50/8.93 % (2575510)Instructions burned: 128 (million)
% 49.50/8.93 % (2575506)Instruction limit reached!
% 49.50/8.93 % (2575506)------------------------------
% 49.50/8.93 % (2575506)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 49.50/8.93 % (2575506)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 49.50/8.93 % (2575506)CaDiCaL version: 2.1.3
% 49.50/8.93 % (2575506)Termination reason: Instruction limit
% 49.50/8.93 % (2575506)Termination phase: Saturation
% 49.50/8.93 % (2575506)Time elapsed: 1.300 s
% 49.50/8.93 % (2575506)Peak memory usage: 141 MB
% 49.50/8.93 % (2575506)Instructions burned: 2089 (million)
% 49.50/8.93 % (2575510)------------------------------
% 49.50/8.93 % (2575510)------------------------------
% 49.50/8.93 % (2575440)First to succeed.
% 49.50/8.93 % (2575440)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2575433"
% 49.50/8.93 % (2575512)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=191815953:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2921 on theBenchmark for (2921ds/2942Mi)
% 49.50/8.93 % (2575513)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1204391615:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2920 on theBenchmark for (2920ds/6922Mi)
% 49.50/8.93 % (2575440)Refutation found. Thanks to Tanya!
% 49.50/8.93 % SZS status Unsatisfiable for theBenchmark
% 49.50/8.93 % SZS output start Proof for theBenchmark
% See solution above
% 58.67/9.13 % (2575440)------------------------------
% 58.67/9.13 % (2575440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 58.67/9.13 % (2575440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 58.67/9.13 % (2575440)CaDiCaL version: 2.1.3
% 58.67/9.13 % (2575440)Termination reason: Refutation
% 58.67/9.13 % (2575440)Time elapsed: 7.735 s
% 58.67/9.13 % (2575440)Peak memory usage: 192 MB
% 58.67/9.13 % (2575440)Instructions burned: 11976 (million)
% 58.67/9.13 % (2575440)------------------------------
% 58.67/9.13 % (2575440)------------------------------
% 58.67/9.13 % (2575433)Success in time 8.271 s
% 58.67/9.13 % Vampire exiting
%------------------------------------------------------------------------------