%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV576-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n008.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:01 PM UTC 2026
% Result : Unsatisfiable 21.69s 3.83s
% Output : Refutation 0.20s
% Verified :
% SZS Type : Refutation
% Derivation depth : 48
% Number of leaves : 64
% Syntax : Number of formulae : 336 ( 290 unt; 20 def)
% Number of atoms : 385 ( 321 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 100 ( 51 ~; 49 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 2 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 40 ( 40 usr; 23 con; 0-3 aty)
% Number of variables : 251 ( 251 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f2,axiom,
! [X0,X1] : c_HOL_Oord__class_Oless(X0,c_Suc(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X1),X0)),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_less__add__Suc2_0) ).
fof(f71,axiom,
! [X0] :
( hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)))),c_Divides_Odiv__class_Odiv(X0,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat)) = X0
| ~ c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_even__nat__div__two__times__two_0) ).
fof(f115,axiom,
! [X0,X1] : hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),X0),X1) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),X1),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat__mult__commute_0) ).
fof(f546,axiom,
! [X0,X1] : c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1),X1,tc_nat) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_diff__add__inverse2_0) ).
fof(f701,axiom,
! [X2,X0,X1] : c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X1),X2,tc_nat) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Divides_Odiv__class_Odiv(X0,X2,tc_nat)),c_Divides_Odiv__class_Odiv(X1,X2,tc_nat))),c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Divides_Odiv__class_Omod(X0,X2,tc_nat)),c_Divides_Odiv__class_Omod(X1,X2,tc_nat)),X2,tc_nat)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_div__add1__eq_0) ).
fof(f890,axiom,
! [X0] : c_HOL_Ominus__class_Ominus(X0,X0,tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_diff__self__eq__0_0) ).
fof(f891,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_nat) = c_HOL_Ominus__class_Ominus(X0,X0,tc_nat),
inference(reorient_equations,[],[f890]) ).
fof(f892,axiom,
! [X0] : c_HOL_Ominus__class_Ominus(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_minus__nat_Odiff__0_0) ).
fof(f899,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/sandbox2/benchmark/theBenchmark.p',cls_diff__0__eq__0_0) ).
fof(f900,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,[],[f899]) ).
fof(f901,axiom,
! [X0] : c_lessequals(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_le0_0) ).
fof(f904,axiom,
! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),c_HOL_Ozero__class_Ozero(tc_nat)) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Nat_Oadd__0__right_0) ).
fof(f905,axiom,
! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Ozero__class_Ozero(tc_nat)),X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_plus__nat_Oadd__0_0) ).
fof(f924,axiom,
! [X0] :
( c_Divides_Odiv__class_Omod(X0,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat) != c_HOL_Ozero__class_Ozero(tc_nat)
| c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_even__nat__equiv__def_1) ).
fof(f925,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(tc_nat) != c_Divides_Odiv__class_Omod(X0,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),tc_nat)
| c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(reorient_equations,[],[f924]) ).
fof(f993,axiom,
! [X0,X1] : c_Divides_Odiv__class_Odiv(c_Suc(X0),X1,tc_nat) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Divides_Odiv__class_Odiv(X0,X1,tc_nat)),c_Divides_Odiv__class_Odiv(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X1,tc_nat))),c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Divides_Odiv__class_Omod(X0,X1,tc_nat)),c_Divides_Odiv__class_Omod(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),X1,tc_nat)),X1,tc_nat)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_div__Suc_0) ).
fof(f1029,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/sandbox2/benchmark/theBenchmark.p',cls_Divides_Omod__div__equality_H_0) ).
fof(f1040,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/sandbox2/benchmark/theBenchmark.p',cls_nat__add__commute_0) ).
fof(f1107,axiom,
! [X0] : hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat__mult__1_0) ).
fof(f1262,axiom,
! [X0,X1] : c_lessequals(X0,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X1),X0),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_le__add2_0) ).
fof(f1332,axiom,
! [X0] : c_Divides_Odiv__class_Omod(X0,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_mod__1_0) ).
fof(f1333,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat),
inference(reorient_equations,[],[f1332]) ).
fof(f1346,axiom,
! [X0] : c_Divides_Odiv__class_Odiv(X0,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_div__1_0) ).
fof(f1385,axiom,
! [X0,X1] :
( c_HOL_Ominus__class_Ominus(c_Suc(X0),X1,tc_nat) = c_HOL_Ominus__class_Ominus(X0,c_HOL_Ominus__class_Ominus(X1,c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OPls),tc_nat),tc_nat),tc_nat)
| ~ c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(c_Int_OPls,tc_nat),X1,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__diff__eq__diff__pred_0) ).
fof(f1402,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/sandbox2/benchmark/theBenchmark.p',cls_nat__mult__2__right_0) ).
fof(f1403,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,[],[f1402]) ).
fof(f1404,axiom,
! [X0] : hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)),X0) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat__mult__2_0) ).
fof(f1405,plain,
! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X0) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)),X0),
inference(reorient_equations,[],[f1404]) ).
fof(f1413,axiom,
! [X0,X1] : c_HOL_Ominus__class_Ominus(X0,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/sandbox2/benchmark/theBenchmark.p',cls_diff__Suc__eq__diff__pred_0) ).
fof(f1415,axiom,
! [X0] : c_Suc(X0) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__eq__plus1__left_0) ).
fof(f1416,axiom,
! [X0] : c_Suc(X0) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),c_HOL_Oone__class_Oone(tc_nat)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__eq__plus1_0) ).
fof(f1420,axiom,
! [X2,X0,X1] :
( ~ class_Orderings_Oorder(X0)
| c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool)) = c_SetInterval_Oord__class_OatLeastLessThan(X1,X2,X0)
| c_HOL_Oord__class_Oless(X1,X2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_atLeastLessThan__empty__iff2_1) ).
fof(f1421,plain,
! [X2,X0,X1] :
( c_SetInterval_Oord__class_OatLeastLessThan(X1,X2,X0) = c_Orderings_Obot__class_Obot(tc_fun(X0,tc_bool))
| ~ class_Orderings_Oorder(X0)
| c_HOL_Oord__class_Oless(X1,X2,X0) ),
inference(reorient_equations,[],[f1420]) ).
fof(f1424,axiom,
! [X0] : c_SetInterval_Oord__class_OatMost(c_Suc(X0),tc_nat) = c_Set_Oinsert(c_Suc(X0),c_SetInterval_Oord__class_OatMost(X0,tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_atMost__Suc_0) ).
fof(f1489,axiom,
! [X0] : c_lessequals(X0,X0,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_le__refl_0) ).
fof(f1596,axiom,
! [X0,X1] :
( c_SetInterval_Oord__class_OatLeastLessThan(X0,c_Suc(X1),tc_nat) = c_Set_Oinsert(X1,c_SetInterval_Oord__class_OatLeastLessThan(X0,X1,tc_nat),tc_nat)
| ~ c_lessequals(X0,X1,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_atLeastLessThanSuc_0) ).
fof(f1597,axiom,
c_SetInterval_Oord__class_OatMost(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = c_Set_Oinsert(c_HOL_Ozero__class_Ozero(tc_nat),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_atMost__0_0) ).
fof(f1616,axiom,
! [X0] : c_Divides_Odiv__class_Odiv(c_Suc(c_Suc(X0)),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_nat) = 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/sandbox2/benchmark/theBenchmark.p',cls_div2__Suc__Suc_0) ).
fof(f1617,plain,
! [X0] : 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(c_Suc(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,[],[f1616]) ).
fof(f1620,axiom,
! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)) = c_Suc(c_Suc(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_add__2__eq__Suc_H_0) ).
fof(f1621,plain,
! [X0] : c_Suc(c_Suc(X0)) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)),
inference(reorient_equations,[],[f1620]) ).
fof(f1624,axiom,
hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),c_HOL_Oone__class_Oone(tc_nat)) = c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat__1__add__1_0) ).
fof(f1625,plain,
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),c_HOL_Oone__class_Oone(tc_nat)),c_HOL_Oone__class_Oone(tc_nat)),
inference(reorient_equations,[],[f1624]) ).
fof(f1635,axiom,
! [X0] : c_SetInterval_Oord__class_OatLeastLessThan(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_atLeastLessThan0_0) ).
fof(f1636,plain,
! [X0] : c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)) = c_SetInterval_Oord__class_OatLeastLessThan(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),
inference(reorient_equations,[],[f1635]) ).
fof(f1644,axiom,
c_Int_Onumber__class_Onumber__of(c_Int_OPls,tc_nat) = c_HOL_Ozero__class_Ozero(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_nat__number__of__Pls_0) ).
fof(f1645,plain,
c_HOL_Ozero__class_Ozero(tc_nat) = c_Int_Onumber__class_Onumber__of(c_Int_OPls,tc_nat),
inference(reorient_equations,[],[f1644]) ).
fof(f1648,axiom,
c_HOL_Oone__class_Oone(tc_nat) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_One__nat__def_0) ).
fof(f1649,plain,
c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = c_HOL_Oone__class_Oone(tc_nat),
inference(reorient_equations,[],[f1648]) ).
fof(f1672,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/sandbox2/benchmark/theBenchmark.p',cls_Numeral1__eq1__nat_0) ).
fof(f1673,axiom,
c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OBit1(c_Int_OPls)),tc_nat) = c_Suc(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_numeral__3__eq__3_0) ).
fof(f1684,axiom,
! [X0] : c_SetInterval_Oord__class_OatLeastLessThan(X0,c_Suc(X0),tc_nat) = c_Set_Oinsert(X0,c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_atLeastLessThan__singleton_0) ).
fof(f1685,axiom,
! [X2,X0,X1] : c_Set_Oinsert(X0,X1,X2) != c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_insert__not__empty_0) ).
fof(f1686,plain,
! [X2,X0,X1] : c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)) != c_Set_Oinsert(X0,X1,X2),
inference(reorient_equations,[],[f1685]) ).
fof(f1693,axiom,
! [X2,X3,X0,X1] : c_Set_Oinsert(X0,c_Set_Oinsert(X1,X2,X3),X3) = c_Set_Oinsert(X1,c_Set_Oinsert(X0,X2,X3),X3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_insert__commute_0) ).
fof(f1694,axiom,
c_Suc(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/sandbox2/benchmark/theBenchmark.p',cls_comp__arith_I115_J_0) ).
fof(f1700,negated_conjecture,
c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),c_Suc(c_Suc(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))))),tc_nat) != c_Set_Oinsert(c_HOL_Ozero__class_Ozero(tc_nat),c_Set_Oinsert(c_HOL_Oone__class_Oone(tc_nat),c_Set_Oinsert(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),c_Set_Oinsert(c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OBit1(c_Int_OPls)),tc_nat),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1735,axiom,
class_Orderings_Oorder(tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',clsarity_nat__Orderings_Oorder) ).
fof(f1793,plain,
! [X0,X1] : c_HOL_Oord__class_Oless(X0,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X1),X0)),tc_nat),
inference(definition_unfolding,[],[f2,f1415]) ).
fof(f1804,plain,
! [X0] :
( hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),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)))),c_Divides_Odiv__class_Odiv(X0,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),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))),tc_nat)) = X0
| ~ c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(definition_unfolding,[],[f71,f1415,f1415,f1415,f1415]) ).
fof(f1837,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(tc_nat) != c_Divides_Odiv__class_Omod(X0,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),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))),tc_nat)
| c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(definition_unfolding,[],[f925,f1415,f1415]) ).
fof(f1855,plain,
! [X0,X1] : c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X0),X1,tc_nat) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Divides_Odiv__class_Odiv(X0,X1,tc_nat)),c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),c_HOL_Ozero__class_Ozero(tc_nat)),X1,tc_nat))),c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Divides_Odiv__class_Omod(X0,X1,tc_nat)),c_Divides_Odiv__class_Omod(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),c_HOL_Ozero__class_Ozero(tc_nat)),X1,tc_nat)),X1,tc_nat)),
inference(definition_unfolding,[],[f993,f1415,f1415,f1415]) ).
fof(f1897,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat),
inference(definition_unfolding,[],[f1333,f1415]) ).
fof(f1905,plain,
! [X0] : c_Divides_Odiv__class_Odiv(X0,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),c_HOL_Ozero__class_Ozero(tc_nat)),tc_nat) = X0,
inference(definition_unfolding,[],[f1346,f1415]) ).
fof(f1920,plain,
! [X0,X1] :
( c_HOL_Ominus__class_Ominus(X0,c_HOL_Ominus__class_Ominus(X1,c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OPls),tc_nat),tc_nat),tc_nat) = c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X0),X1,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(c_Int_OPls,tc_nat),X1,tc_nat) ),
inference(definition_unfolding,[],[f1385,f1415]) ).
fof(f1929,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat),X1,tc_nat) = c_HOL_Ominus__class_Ominus(X0,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X1),tc_nat),
inference(definition_unfolding,[],[f1413,f1415]) ).
fof(f1931,plain,
! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),c_HOL_Oone__class_Oone(tc_nat)) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X0),
inference(definition_unfolding,[],[f1416,f1415]) ).
fof(f1932,plain,
! [X0] : c_SetInterval_Oord__class_OatMost(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X0),tc_nat) = c_Set_Oinsert(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X0),c_SetInterval_Oord__class_OatMost(X0,tc_nat),tc_nat),
inference(definition_unfolding,[],[f1424,f1415,f1415]) ).
fof(f1942,plain,
! [X0,X1] :
( c_Set_Oinsert(X1,c_SetInterval_Oord__class_OatLeastLessThan(X0,X1,tc_nat),tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(X0,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X1),tc_nat)
| ~ c_lessequals(X0,X1,tc_nat) ),
inference(definition_unfolding,[],[f1596,f1415]) ).
fof(f1946,plain,
! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(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_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X0)),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_nat),
inference(definition_unfolding,[],[f1617,f1415,f1415,f1415]) ).
fof(f1948,plain,
! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(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),c_HOL_Oone__class_Oone(tc_nat)),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X0)),
inference(definition_unfolding,[],[f1621,f1415,f1415]) ).
fof(f1955,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(definition_unfolding,[],[f1649,f1415]) ).
fof(f1959,plain,
c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OBit1(c_Int_OPls)),tc_nat) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),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(definition_unfolding,[],[f1673,f1415,f1415,f1415]) ).
fof(f1962,plain,
! [X0] : c_Set_Oinsert(X0,c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(X0,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X0),tc_nat),
inference(definition_unfolding,[],[f1684,f1415]) ).
fof(f1965,plain,
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),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(definition_unfolding,[],[f1694,f1415,f1415]) ).
fof(f1966,plain,
c_Set_Oinsert(c_HOL_Ozero__class_Ozero(tc_nat),c_Set_Oinsert(c_HOL_Oone__class_Oone(tc_nat),c_Set_Oinsert(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),c_Set_Oinsert(c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OBit1(c_Int_OPls)),tc_nat),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),tc_nat),tc_nat) != c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),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))))),tc_nat),
inference(definition_unfolding,[],[f1700,f1415,f1415,f1415,f1415]) ).
fof(f1967,definition,
sF0 = c_HOL_Ozero__class_Ozero(tc_nat),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f1968,plain,
c_HOL_Ozero__class_Ozero(tc_nat) = sF0,
inference(reorient_equations,[],[f1967]) ).
fof(f1969,definition,
sF1 = c_HOL_Oone__class_Oone(tc_nat),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f1970,plain,
c_HOL_Oone__class_Oone(tc_nat) = sF1,
inference(reorient_equations,[],[f1969]) ).
fof(f1971,definition,
sF2 = c_Int_OBit1(c_Int_OPls),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f1972,plain,
c_Int_OBit1(c_Int_OPls) = sF2,
inference(reorient_equations,[],[f1971]) ).
fof(f1973,definition,
sF3 = c_Int_OBit0(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f1974,plain,
c_Int_OBit0(sF2) = sF3,
inference(reorient_equations,[],[f1973]) ).
fof(f1975,definition,
sF4 = c_Int_Onumber__class_Onumber__of(sF3,tc_nat),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f1976,plain,
c_Int_Onumber__class_Onumber__of(sF3,tc_nat) = sF4,
inference(reorient_equations,[],[f1975]) ).
fof(f1977,definition,
sF5 = c_Int_OBit1(sF2),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f1978,plain,
c_Int_OBit1(sF2) = sF5,
inference(reorient_equations,[],[f1977]) ).
fof(f1979,definition,
sF6 = c_Int_Onumber__class_Onumber__of(sF5,tc_nat),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f1980,plain,
c_Int_Onumber__class_Onumber__of(sF5,tc_nat) = sF6,
inference(reorient_equations,[],[f1979]) ).
fof(f1981,definition,
sF7 = tc_fun(tc_nat,tc_bool),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f1982,plain,
tc_fun(tc_nat,tc_bool) = sF7,
inference(reorient_equations,[],[f1981]) ).
fof(f1983,definition,
sF8 = c_Orderings_Obot__class_Obot(sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f1984,plain,
c_Orderings_Obot__class_Obot(sF7) = sF8,
inference(reorient_equations,[],[f1983]) ).
fof(f1985,definition,
sF9 = c_Set_Oinsert(sF6,sF8,tc_nat),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f1986,plain,
c_Set_Oinsert(sF6,sF8,tc_nat) = sF9,
inference(reorient_equations,[],[f1985]) ).
fof(f1987,definition,
sF10 = c_Set_Oinsert(sF4,sF9,tc_nat),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f1988,plain,
c_Set_Oinsert(sF4,sF9,tc_nat) = sF10,
inference(reorient_equations,[],[f1987]) ).
fof(f1989,definition,
sF11 = c_Set_Oinsert(sF1,sF10,tc_nat),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f1990,plain,
c_Set_Oinsert(sF1,sF10,tc_nat) = sF11,
inference(reorient_equations,[],[f1989]) ).
fof(f1991,definition,
sF12 = c_Set_Oinsert(sF0,sF11,tc_nat),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f1992,plain,
c_Set_Oinsert(sF0,sF11,tc_nat) = sF12,
inference(reorient_equations,[],[f1991]) ).
fof(f1993,definition,
sF13 = c_HOL_Oplus__class_Oplus(tc_nat),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f1994,plain,
c_HOL_Oplus__class_Oplus(tc_nat) = sF13,
inference(reorient_equations,[],[f1993]) ).
fof(f1995,definition,
sF14 = hAPP(sF13,sF1),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f1996,plain,
hAPP(sF13,sF1) = sF14,
inference(reorient_equations,[],[f1995]) ).
fof(f1997,definition,
sF15 = hAPP(sF14,sF0),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f1998,plain,
hAPP(sF14,sF0) = sF15,
inference(reorient_equations,[],[f1997]) ).
fof(f1999,definition,
sF16 = hAPP(sF14,sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f2000,plain,
hAPP(sF14,sF15) = sF16,
inference(reorient_equations,[],[f1999]) ).
fof(f2001,definition,
sF17 = hAPP(sF14,sF16),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f2002,plain,
hAPP(sF14,sF16) = sF17,
inference(reorient_equations,[],[f2001]) ).
fof(f2003,definition,
sF18 = hAPP(sF14,sF17),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f2004,plain,
hAPP(sF14,sF17) = sF18,
inference(reorient_equations,[],[f2003]) ).
fof(f2005,definition,
sF19 = c_SetInterval_Oord__class_OatLeastLessThan(sF0,sF18,tc_nat),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f2006,plain,
c_SetInterval_Oord__class_OatLeastLessThan(sF0,sF18,tc_nat) = sF19,
inference(reorient_equations,[],[f2005]) ).
fof(f2007,plain,
sF12 != sF19,
inference(definition_folding,[],[f1966,f2006,f2004,f2002,f2000,f1998,f1968,f1996,f1970,f1994,f1996,f1970,f1994,f1996,f1970,f1994,f1996,f1970,f1994,f1968,f1992,f1990,f1988,f1986,f1984,f1982,f1980,f1978,f1972,f1976,f1974,f1972,f1970,f1968]) ).
fof(f2009,plain,
c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OBit1(c_Int_OPls)),tc_nat) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)),
inference(forward_demodulation,[],[f1959,f1965]) ).
fof(f2013,plain,
! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(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_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_nat),
inference(forward_demodulation,[],[f1946,f1948]) ).
fof(f2025,plain,
! [X0,X1] :
( c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X0),X1,tc_nat) = c_HOL_Ominus__class_Ominus(X0,c_HOL_Ominus__class_Ominus(X1,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_nat)
| ~ c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(c_Int_OPls,tc_nat),X1,tc_nat) ),
inference(forward_demodulation,[],[f1920,f1672]) ).
fof(f2035,plain,
! [X0] : c_Divides_Odiv__class_Odiv(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat) = X0,
inference(forward_demodulation,[],[f1905,f1955]) ).
fof(f2042,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat),
inference(forward_demodulation,[],[f1897,f1955]) ).
fof(f2047,plain,
! [X0,X1] : c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X0),X1,tc_nat) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Divides_Odiv__class_Odiv(X0,X1,tc_nat)),c_Divides_Odiv__class_Odiv(c_HOL_Oone__class_Oone(tc_nat),X1,tc_nat))),c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_Divides_Odiv__class_Omod(X0,X1,tc_nat)),c_Divides_Odiv__class_Omod(c_HOL_Oone__class_Oone(tc_nat),X1,tc_nat)),X1,tc_nat)),
inference(forward_demodulation,[],[f1855,f1955]) ).
fof(f2051,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(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)
| c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(forward_demodulation,[],[f1837,f1965]) ).
fof(f2074,plain,
! [X0] :
( hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),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)) = X0
| ~ c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(forward_demodulation,[],[f1804,f1965]) ).
fof(f2076,plain,
c_Int_Onumber__class_Onumber__of(c_Int_OBit1(sF2),tc_nat) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF2),tc_nat)),
inference(forward_demodulation,[],[f2009,f1972]) ).
fof(f2079,plain,
! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),c_Divides_Odiv__class_Odiv(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF2),tc_nat),tc_nat)) = c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF2),tc_nat)),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF2),tc_nat),tc_nat),
inference(forward_demodulation,[],[f2013,f1972]) ).
fof(f2090,plain,
! [X0,X1] :
( c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF1),X0),X1,tc_nat) = c_HOL_Ominus__class_Ominus(X0,c_HOL_Ominus__class_Ominus(X1,sF1,tc_nat),tc_nat)
| ~ c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(c_Int_OPls,tc_nat),X1,tc_nat) ),
inference(forward_demodulation,[],[f2025,f1970]) ).
fof(f2099,plain,
! [X0] : c_Divides_Odiv__class_Odiv(X0,sF1,tc_nat) = X0,
inference(forward_demodulation,[],[f2035,f1970]) ).
fof(f2104,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_nat) = c_Divides_Odiv__class_Omod(X0,sF1,tc_nat),
inference(forward_demodulation,[],[f2042,f1970]) ).
fof(f2106,plain,
! [X0,X1] : c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X0),X1,tc_nat) = c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),c_HOL_Oone__class_Oone(tc_nat)),X1,tc_nat),
inference(forward_demodulation,[],[f2047,f701]) ).
fof(f2108,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(tc_nat) != c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF2),tc_nat),tc_nat)
| c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(forward_demodulation,[],[f2051,f1972]) ).
fof(f2130,plain,
! [X0] :
( hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF2),tc_nat)),c_Divides_Odiv__class_Odiv(X0,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF2),tc_nat),tc_nat)) = X0
| ~ c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(forward_demodulation,[],[f2074,f1972]) ).
fof(f2132,plain,
c_Int_Onumber__class_Onumber__of(c_Int_OBit1(sF2),tc_nat) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),c_Int_Onumber__class_Onumber__of(sF3,tc_nat)),
inference(forward_demodulation,[],[f2076,f1974]) ).
fof(f2135,plain,
! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),c_Divides_Odiv__class_Odiv(X0,c_Int_Onumber__class_Onumber__of(sF3,tc_nat),tc_nat)) = c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),c_Int_Onumber__class_Onumber__of(sF3,tc_nat)),c_Int_Onumber__class_Onumber__of(sF3,tc_nat),tc_nat),
inference(forward_demodulation,[],[f2079,f1974]) ).
fof(f2146,plain,
! [X0,X1] :
( c_HOL_Ominus__class_Ominus(X0,c_HOL_Ominus__class_Ominus(X1,sF1,tc_nat),tc_nat) = c_HOL_Ominus__class_Ominus(hAPP(hAPP(sF13,sF1),X0),X1,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(c_Int_OPls,tc_nat),X1,tc_nat) ),
inference(forward_demodulation,[],[f2090,f1994]) ).
fof(f2159,plain,
! [X0] : sF0 = c_Divides_Odiv__class_Omod(X0,sF1,tc_nat),
inference(forward_demodulation,[],[f2104,f1968]) ).
fof(f2161,plain,
! [X0,X1] : c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF1),X0),X1,tc_nat) = c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),sF1),X1,tc_nat),
inference(forward_demodulation,[],[f2106,f1970]) ).
fof(f2163,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(tc_nat) != c_Divides_Odiv__class_Omod(X0,c_Int_Onumber__class_Onumber__of(sF3,tc_nat),tc_nat)
| c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(forward_demodulation,[],[f2108,f1974]) ).
fof(f2178,plain,
! [X0] :
( hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onumber__class_Onumber__of(sF3,tc_nat)),c_Divides_Odiv__class_Odiv(X0,c_Int_Onumber__class_Onumber__of(sF3,tc_nat),tc_nat)) = X0
| ~ c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(forward_demodulation,[],[f2130,f1974]) ).
fof(f2179,plain,
c_Int_Onumber__class_Onumber__of(c_Int_OBit1(sF2),tc_nat) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),sF4),
inference(forward_demodulation,[],[f2132,f1976]) ).
fof(f2182,plain,
! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),c_Divides_Odiv__class_Odiv(X0,sF4,tc_nat)) = c_Divides_Odiv__class_Odiv(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),sF4),sF4,tc_nat),
inference(forward_demodulation,[],[f2135,f1976]) ).
fof(f2193,plain,
! [X0,X1] :
( c_HOL_Ominus__class_Ominus(X0,c_HOL_Ominus__class_Ominus(X1,sF1,tc_nat),tc_nat) = c_HOL_Ominus__class_Ominus(hAPP(sF14,X0),X1,tc_nat)
| ~ c_HOL_Oord__class_Oless(c_Int_Onumber__class_Onumber__of(c_Int_OPls,tc_nat),X1,tc_nat) ),
inference(forward_demodulation,[],[f2146,f1996]) ).
fof(f2206,plain,
! [X0,X1] : c_Divides_Odiv__class_Odiv(hAPP(hAPP(sF13,sF1),X0),X1,tc_nat) = c_Divides_Odiv__class_Odiv(hAPP(hAPP(sF13,X0),sF1),X1,tc_nat),
inference(forward_demodulation,[],[f2161,f1994]) ).
fof(f2208,plain,
! [X0] :
( c_HOL_Ozero__class_Ozero(tc_nat) != c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(forward_demodulation,[],[f2163,f1976]) ).
fof(f2222,plain,
! [X0] :
( hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),sF4),c_Divides_Odiv__class_Odiv(X0,sF4,tc_nat)) = X0
| ~ c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(forward_demodulation,[],[f2178,f1976]) ).
fof(f2223,plain,
c_Int_Onumber__class_Onumber__of(c_Int_OBit1(sF2),tc_nat) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF4),c_HOL_Oone__class_Oone(tc_nat)),
inference(forward_demodulation,[],[f2179,f1931]) ).
fof(f2226,plain,
! [X0] : hAPP(hAPP(sF13,c_HOL_Oone__class_Oone(tc_nat)),c_Divides_Odiv__class_Odiv(X0,sF4,tc_nat)) = c_Divides_Odiv__class_Odiv(hAPP(hAPP(sF13,X0),sF4),sF4,tc_nat),
inference(forward_demodulation,[],[f2182,f1994]) ).
fof(f2236,plain,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(c_HOL_Ozero__class_Ozero(tc_nat),X1,tc_nat)
| c_HOL_Ominus__class_Ominus(X0,c_HOL_Ominus__class_Ominus(X1,sF1,tc_nat),tc_nat) = c_HOL_Ominus__class_Ominus(hAPP(sF14,X0),X1,tc_nat) ),
inference(forward_demodulation,[],[f2193,f1645]) ).
fof(f2246,plain,
! [X0,X1] : c_Divides_Odiv__class_Odiv(hAPP(hAPP(sF13,X0),sF1),X1,tc_nat) = c_Divides_Odiv__class_Odiv(hAPP(sF14,X0),X1,tc_nat),
inference(forward_demodulation,[],[f2206,f1996]) ).
fof(f2248,plain,
! [X0] :
( sF0 != c_Divides_Odiv__class_Omod(X0,sF4,tc_nat)
| c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(forward_demodulation,[],[f2208,f1968]) ).
fof(f2256,plain,
c_Int_Onumber__class_Onumber__of(c_Int_OBit1(sF2),tc_nat) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF4),sF1),
inference(forward_demodulation,[],[f2223,f1970]) ).
fof(f2259,plain,
! [X0] : c_Divides_Odiv__class_Odiv(hAPP(hAPP(sF13,X0),sF4),sF4,tc_nat) = hAPP(hAPP(sF13,sF1),c_Divides_Odiv__class_Odiv(X0,sF4,tc_nat)),
inference(forward_demodulation,[],[f2226,f1970]) ).
fof(f2269,plain,
! [X0,X1] :
( c_HOL_Ominus__class_Ominus(X0,c_HOL_Ominus__class_Ominus(X1,sF1,tc_nat),tc_nat) = c_HOL_Ominus__class_Ominus(hAPP(sF14,X0),X1,tc_nat)
| ~ c_HOL_Oord__class_Oless(sF0,X1,tc_nat) ),
inference(forward_demodulation,[],[f2236,f1968]) ).
fof(f2284,plain,
c_Int_Onumber__class_Onumber__of(c_Int_OBit1(sF2),tc_nat) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF1),sF4),
inference(forward_demodulation,[],[f2256,f1040]) ).
fof(f2286,plain,
! [X0] : c_Divides_Odiv__class_Odiv(hAPP(hAPP(sF13,X0),sF4),sF4,tc_nat) = hAPP(sF14,c_Divides_Odiv__class_Odiv(X0,sF4,tc_nat)),
inference(forward_demodulation,[],[f2259,f1996]) ).
fof(f2302,plain,
c_Int_Onumber__class_Onumber__of(c_Int_OBit1(sF2),tc_nat) = hAPP(hAPP(sF13,sF1),sF4),
inference(forward_demodulation,[],[f2284,f1994]) ).
fof(f2310,plain,
c_Int_Onumber__class_Onumber__of(c_Int_OBit1(sF2),tc_nat) = hAPP(sF14,sF4),
inference(forward_demodulation,[],[f2302,f1996]) ).
fof(f2318,plain,
c_Int_Onumber__class_Onumber__of(sF5,tc_nat) = hAPP(sF14,sF4),
inference(forward_demodulation,[],[f2310,f1978]) ).
fof(f2326,plain,
sF6 = hAPP(sF14,sF4),
inference(forward_demodulation,[],[f2318,f1980]) ).
fof(f2348,plain,
! [X0] : hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),sF1),X0) = X0,
inference(superposition,[],[f1107,f1970]) ).
fof(f2353,plain,
! [X0] : hAPP(hAPP(sF13,c_HOL_Ozero__class_Ozero(tc_nat)),X0) = X0,
inference(superposition,[],[f905,f1994]) ).
fof(f2356,plain,
! [X0] : hAPP(hAPP(sF13,sF0),X0) = X0,
inference(forward_demodulation,[],[f2353,f1968]) ).
fof(f2386,plain,
hAPP(sF14,c_Divides_Odiv__class_Odiv(sF0,sF4,tc_nat)) = c_Divides_Odiv__class_Odiv(sF4,sF4,tc_nat),
inference(superposition,[],[f2286,f2356]) ).
fof(f2397,plain,
! [X0,X1] : hAPP(hAPP(sF13,X0),X1) = hAPP(hAPP(sF13,X1),X0),
inference(superposition,[],[f1040,f1994]) ).
fof(f2403,plain,
! [X0] : c_Set_Oinsert(X0,c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(X0,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),c_HOL_Oone__class_Oone(tc_nat)),tc_nat),
inference(superposition,[],[f1962,f1040]) ).
fof(f2406,plain,
! [X0] : c_Set_Oinsert(X0,c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(X0,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),sF1),tc_nat),
inference(forward_demodulation,[],[f2403,f1970]) ).
fof(f2410,plain,
! [X0] : c_Set_Oinsert(X0,c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(X0,hAPP(hAPP(sF13,X0),sF1),tc_nat),
inference(forward_demodulation,[],[f2406,f1994]) ).
fof(f2413,plain,
! [X0] : c_Set_Oinsert(X0,c_Orderings_Obot__class_Obot(sF7),tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(X0,hAPP(hAPP(sF13,X0),sF1),tc_nat),
inference(forward_demodulation,[],[f2410,f1982]) ).
fof(f2415,plain,
! [X0] : c_Set_Oinsert(X0,sF8,tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(X0,hAPP(hAPP(sF13,X0),sF1),tc_nat),
inference(forward_demodulation,[],[f2413,f1984]) ).
fof(f2418,plain,
c_Set_Oinsert(sF0,sF8,tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(sF0,sF1,tc_nat),
inference(superposition,[],[f2415,f2356]) ).
fof(f2421,plain,
! [X0] : hAPP(sF14,X0) = hAPP(hAPP(sF13,X0),sF1),
inference(superposition,[],[f2397,f1996]) ).
fof(f2426,plain,
! [X0] : hAPP(hAPP(sF13,X0),sF0) = X0,
inference(superposition,[],[f2356,f2397]) ).
fof(f2435,plain,
sF1 = hAPP(sF14,sF0),
inference(superposition,[],[f2356,f2421]) ).
fof(f2454,plain,
! [X0] : c_Set_Oinsert(X0,sF9,tc_nat) = c_Set_Oinsert(sF6,c_Set_Oinsert(X0,sF8,tc_nat),tc_nat),
inference(superposition,[],[f1693,f1986]) ).
fof(f2502,plain,
! [X0] : hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),X0),sF1) = X0,
inference(superposition,[],[f2348,f115]) ).
fof(f2520,plain,
( c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)) = c_Set_Oinsert(sF0,sF8,tc_nat)
| ~ class_Orderings_Oorder(tc_nat)
| c_HOL_Oord__class_Oless(sF0,sF1,tc_nat) ),
inference(superposition,[],[f2418,f1421]) ).
fof(f2533,plain,
( ~ class_Orderings_Oorder(tc_nat)
| c_HOL_Oord__class_Oless(sF0,sF1,tc_nat) ),
inference(forward_subsumption_resolution,[],[f2520,f1686]) ).
fof(f2553,plain,
c_HOL_Oord__class_Oless(sF0,sF1,tc_nat),
inference(forward_subsumption_resolution,[],[f2533,f1735]) ).
fof(f2579,plain,
! [X0] : c_Divides_Odiv__class_Odiv(hAPP(sF14,sF0),X0,tc_nat) = c_Divides_Odiv__class_Odiv(sF1,X0,tc_nat),
inference(superposition,[],[f2246,f2356]) ).
fof(f2586,plain,
! [X0] : c_Divides_Odiv__class_Odiv(sF1,X0,tc_nat) = c_Divides_Odiv__class_Odiv(sF15,X0,tc_nat),
inference(forward_demodulation,[],[f2579,f1998]) ).
fof(f2588,plain,
sF15 = c_Divides_Odiv__class_Odiv(sF1,sF1,tc_nat),
inference(superposition,[],[f2099,f2586]) ).
fof(f2589,plain,
sF1 = sF15,
inference(forward_demodulation,[],[f2588,f2099]) ).
fof(f2593,plain,
sF16 = hAPP(sF14,sF1),
inference(superposition,[],[f2000,f2589]) ).
fof(f2611,plain,
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),sF1),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF1),c_HOL_Ozero__class_Ozero(tc_nat))),
inference(superposition,[],[f1965,f1970]) ).
fof(f2622,plain,
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),sF1),sF1),
inference(forward_demodulation,[],[f2611,f904]) ).
fof(f2629,plain,
c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat) = hAPP(hAPP(sF13,sF1),sF1),
inference(forward_demodulation,[],[f2622,f1994]) ).
fof(f2634,plain,
c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat) = hAPP(sF14,sF1),
inference(forward_demodulation,[],[f2629,f2421]) ).
fof(f2639,plain,
c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat) = sF16,
inference(forward_demodulation,[],[f2634,f2593]) ).
fof(f2644,plain,
sF16 = c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF2),tc_nat),
inference(forward_demodulation,[],[f2639,f1972]) ).
fof(f2647,plain,
c_Int_Onumber__class_Onumber__of(sF3,tc_nat) = sF16,
inference(forward_demodulation,[],[f2644,f1974]) ).
fof(f2650,plain,
sF4 = sF16,
inference(forward_demodulation,[],[f2647,f1976]) ).
fof(f2659,plain,
sF17 = hAPP(sF14,sF4),
inference(superposition,[],[f2002,f2650]) ).
fof(f2660,plain,
sF6 = sF17,
inference(forward_demodulation,[],[f2659,f2326]) ).
fof(f2664,plain,
sF18 = hAPP(sF14,sF6),
inference(superposition,[],[f2004,f2660]) ).
fof(f2720,plain,
! [X0] : c_SetInterval_Oord__class_OatMost(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF1),X0),tc_nat) = c_Set_Oinsert(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF1),X0),c_SetInterval_Oord__class_OatMost(X0,tc_nat),tc_nat),
inference(superposition,[],[f1932,f1970]) ).
fof(f2724,plain,
c_SetInterval_Oord__class_OatMost(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_nat) = c_Set_Oinsert(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),c_SetInterval_Oord__class_OatMost(c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_nat),
inference(superposition,[],[f1932,f1625]) ).
fof(f2728,plain,
! [X0,X1] : c_Set_Oinsert(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X0),c_Set_Oinsert(X1,c_SetInterval_Oord__class_OatMost(X0,tc_nat),tc_nat),tc_nat) = c_Set_Oinsert(X1,c_SetInterval_Oord__class_OatMost(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X0),tc_nat),tc_nat),
inference(superposition,[],[f1693,f1932]) ).
fof(f2729,plain,
! [X0,X1] : c_Set_Oinsert(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF1),X0),c_Set_Oinsert(X1,c_SetInterval_Oord__class_OatMost(X0,tc_nat),tc_nat),tc_nat) = c_Set_Oinsert(X1,c_SetInterval_Oord__class_OatMost(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF1),X0),tc_nat),tc_nat),
inference(forward_demodulation,[],[f2728,f1970]) ).
fof(f2733,plain,
c_SetInterval_Oord__class_OatMost(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),tc_nat) = c_Set_Oinsert(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat),c_SetInterval_Oord__class_OatMost(sF1,tc_nat),tc_nat),
inference(forward_demodulation,[],[f2724,f1970]) ).
fof(f2737,plain,
! [X0] : c_SetInterval_Oord__class_OatMost(hAPP(hAPP(sF13,sF1),X0),tc_nat) = c_Set_Oinsert(hAPP(hAPP(sF13,sF1),X0),c_SetInterval_Oord__class_OatMost(X0,tc_nat),tc_nat),
inference(forward_demodulation,[],[f2720,f1994]) ).
fof(f2739,plain,
! [X0,X1] : c_Set_Oinsert(hAPP(hAPP(sF13,sF1),X0),c_Set_Oinsert(X1,c_SetInterval_Oord__class_OatMost(X0,tc_nat),tc_nat),tc_nat) = c_Set_Oinsert(X1,c_SetInterval_Oord__class_OatMost(hAPP(hAPP(sF13,sF1),X0),tc_nat),tc_nat),
inference(forward_demodulation,[],[f2729,f1994]) ).
fof(f2743,plain,
c_SetInterval_Oord__class_OatMost(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF2),tc_nat),tc_nat) = c_Set_Oinsert(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF2),tc_nat),c_SetInterval_Oord__class_OatMost(sF1,tc_nat),tc_nat),
inference(forward_demodulation,[],[f2733,f1972]) ).
fof(f2747,plain,
! [X0] : c_SetInterval_Oord__class_OatMost(hAPP(sF14,X0),tc_nat) = c_Set_Oinsert(hAPP(sF14,X0),c_SetInterval_Oord__class_OatMost(X0,tc_nat),tc_nat),
inference(forward_demodulation,[],[f2737,f1996]) ).
fof(f2749,plain,
! [X0,X1] : c_Set_Oinsert(hAPP(sF14,X0),c_Set_Oinsert(X1,c_SetInterval_Oord__class_OatMost(X0,tc_nat),tc_nat),tc_nat) = c_Set_Oinsert(X1,c_SetInterval_Oord__class_OatMost(hAPP(sF14,X0),tc_nat),tc_nat),
inference(forward_demodulation,[],[f2739,f1996]) ).
fof(f2753,plain,
c_SetInterval_Oord__class_OatMost(c_Int_Onumber__class_Onumber__of(sF3,tc_nat),tc_nat) = c_Set_Oinsert(c_Int_Onumber__class_Onumber__of(sF3,tc_nat),c_SetInterval_Oord__class_OatMost(sF1,tc_nat),tc_nat),
inference(forward_demodulation,[],[f2743,f1974]) ).
fof(f2757,plain,
c_SetInterval_Oord__class_OatMost(sF4,tc_nat) = c_Set_Oinsert(sF4,c_SetInterval_Oord__class_OatMost(sF1,tc_nat),tc_nat),
inference(forward_demodulation,[],[f2753,f1976]) ).
fof(f2761,plain,
c_SetInterval_Oord__class_OatMost(c_Divides_Odiv__class_Odiv(sF4,sF4,tc_nat),tc_nat) = c_Set_Oinsert(c_Divides_Odiv__class_Odiv(sF4,sF4,tc_nat),c_SetInterval_Oord__class_OatMost(c_Divides_Odiv__class_Odiv(sF0,sF4,tc_nat),tc_nat),tc_nat),
inference(superposition,[],[f2747,f2386]) ).
fof(f2763,plain,
c_SetInterval_Oord__class_OatMost(sF6,tc_nat) = c_Set_Oinsert(sF6,c_SetInterval_Oord__class_OatMost(sF4,tc_nat),tc_nat),
inference(superposition,[],[f2747,f2326]) ).
fof(f2784,plain,
! [X0] : c_Set_Oinsert(sF15,c_Set_Oinsert(X0,c_SetInterval_Oord__class_OatMost(sF0,tc_nat),tc_nat),tc_nat) = c_Set_Oinsert(X0,c_SetInterval_Oord__class_OatMost(sF15,tc_nat),tc_nat),
inference(superposition,[],[f2749,f1998]) ).
fof(f2808,plain,
! [X0] : c_Set_Oinsert(sF1,c_Set_Oinsert(X0,c_SetInterval_Oord__class_OatMost(sF0,tc_nat),tc_nat),tc_nat) = c_Set_Oinsert(X0,c_SetInterval_Oord__class_OatMost(sF1,tc_nat),tc_nat),
inference(forward_demodulation,[],[f2784,f2589]) ).
fof(f3238,plain,
! [X0] :
( c_SetInterval_Oord__class_OatLeastLessThan(X0,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X0)),tc_nat) = c_Set_Oinsert(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X0),c_Set_Oinsert(X0,c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat)
| ~ c_lessequals(X0,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X0),tc_nat) ),
inference(superposition,[],[f1942,f1962]) ).
fof(f3245,plain,
! [X0,X1] :
( c_Set_Oinsert(X0,c_SetInterval_Oord__class_OatLeastLessThan(X1,X0,tc_nat),tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(X1,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF1),X0),tc_nat)
| ~ c_lessequals(X1,X0,tc_nat) ),
inference(superposition,[],[f1942,f1970]) ).
fof(f3270,plain,
! [X0,X1] :
( c_Set_Oinsert(X0,c_SetInterval_Oord__class_OatLeastLessThan(X1,X0,tc_nat),tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(X1,hAPP(hAPP(sF13,sF1),X0),tc_nat)
| ~ c_lessequals(X1,X0,tc_nat) ),
inference(forward_demodulation,[],[f3245,f1994]) ).
fof(f3277,plain,
! [X0] : c_SetInterval_Oord__class_OatLeastLessThan(X0,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X0)),tc_nat) = c_Set_Oinsert(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X0),c_Set_Oinsert(X0,c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),
inference(forward_subsumption_resolution,[],[f3238,f1262]) ).
fof(f3289,plain,
! [X0,X1] :
( c_Set_Oinsert(X0,c_SetInterval_Oord__class_OatLeastLessThan(X1,X0,tc_nat),tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(X1,hAPP(sF14,X0),tc_nat)
| ~ c_lessequals(X1,X0,tc_nat) ),
inference(forward_demodulation,[],[f3270,f1996]) ).
fof(f3296,plain,
! [X0] : c_SetInterval_Oord__class_OatLeastLessThan(X0,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X0)),tc_nat) = c_Set_Oinsert(X0,c_Set_Oinsert(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X0),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),
inference(forward_demodulation,[],[f3277,f1693]) ).
fof(f3313,plain,
! [X0] : c_SetInterval_Oord__class_OatLeastLessThan(X0,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X0)),tc_nat) = c_Set_Oinsert(X0,c_Set_Oinsert(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X0),c_Orderings_Obot__class_Obot(sF7),tc_nat),tc_nat),
inference(forward_demodulation,[],[f3296,f1982]) ).
fof(f3321,plain,
! [X0] : c_SetInterval_Oord__class_OatLeastLessThan(X0,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X0)),tc_nat) = c_Set_Oinsert(X0,c_Set_Oinsert(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),c_HOL_Oone__class_Oone(tc_nat)),X0),sF8,tc_nat),tc_nat),
inference(forward_demodulation,[],[f3313,f1984]) ).
fof(f3328,plain,
! [X0] : c_SetInterval_Oord__class_OatLeastLessThan(X0,hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF1),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF1),X0)),tc_nat) = c_Set_Oinsert(X0,c_Set_Oinsert(hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF1),X0),sF8,tc_nat),tc_nat),
inference(forward_demodulation,[],[f3321,f1970]) ).
fof(f3331,plain,
! [X0] : c_SetInterval_Oord__class_OatLeastLessThan(X0,hAPP(hAPP(sF13,sF1),hAPP(hAPP(sF13,sF1),X0)),tc_nat) = c_Set_Oinsert(X0,c_Set_Oinsert(hAPP(hAPP(sF13,sF1),X0),sF8,tc_nat),tc_nat),
inference(forward_demodulation,[],[f3328,f1994]) ).
fof(f3332,plain,
! [X0] : c_Set_Oinsert(X0,c_Set_Oinsert(hAPP(sF14,X0),sF8,tc_nat),tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(X0,hAPP(sF14,hAPP(sF14,X0)),tc_nat),
inference(forward_demodulation,[],[f3331,f1996]) ).
fof(f3371,plain,
c_Set_Oinsert(c_Divides_Odiv__class_Odiv(sF0,sF4,tc_nat),c_Set_Oinsert(c_Divides_Odiv__class_Odiv(sF4,sF4,tc_nat),sF8,tc_nat),tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(c_Divides_Odiv__class_Odiv(sF0,sF4,tc_nat),hAPP(sF14,c_Divides_Odiv__class_Odiv(sF4,sF4,tc_nat)),tc_nat),
inference(superposition,[],[f3332,f2386]) ).
fof(f3373,plain,
c_Set_Oinsert(sF1,c_Set_Oinsert(sF16,sF8,tc_nat),tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(sF1,hAPP(sF14,sF16),tc_nat),
inference(superposition,[],[f3332,f2593]) ).
fof(f3395,plain,
c_Set_Oinsert(sF1,c_Set_Oinsert(sF16,sF8,tc_nat),tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(sF1,sF17,tc_nat),
inference(forward_demodulation,[],[f3373,f2002]) ).
fof(f3402,plain,
c_Set_Oinsert(sF1,c_Set_Oinsert(sF16,sF8,tc_nat),tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(sF1,sF6,tc_nat),
inference(forward_demodulation,[],[f3395,f2660]) ).
fof(f3407,plain,
c_SetInterval_Oord__class_OatLeastLessThan(sF1,sF6,tc_nat) = c_Set_Oinsert(sF1,c_Set_Oinsert(sF4,sF8,tc_nat),tc_nat),
inference(forward_demodulation,[],[f3402,f2650]) ).
fof(f3566,plain,
! [X0] : c_Set_Oinsert(sF1,c_Set_Oinsert(X0,c_Set_Oinsert(sF4,sF8,tc_nat),tc_nat),tc_nat) = c_Set_Oinsert(X0,c_SetInterval_Oord__class_OatLeastLessThan(sF1,sF6,tc_nat),tc_nat),
inference(superposition,[],[f1693,f3407]) ).
fof(f3614,plain,
c_Set_Oinsert(sF6,c_SetInterval_Oord__class_OatLeastLessThan(sF1,sF6,tc_nat),tc_nat) = c_Set_Oinsert(sF1,c_Set_Oinsert(sF4,sF9,tc_nat),tc_nat),
inference(superposition,[],[f3566,f2454]) ).
fof(f3629,plain,
c_Set_Oinsert(sF1,sF10,tc_nat) = c_Set_Oinsert(sF6,c_SetInterval_Oord__class_OatLeastLessThan(sF1,sF6,tc_nat),tc_nat),
inference(forward_demodulation,[],[f3614,f1988]) ).
fof(f3631,plain,
sF11 = c_Set_Oinsert(sF6,c_SetInterval_Oord__class_OatLeastLessThan(sF1,sF6,tc_nat),tc_nat),
inference(forward_demodulation,[],[f3629,f1990]) ).
fof(f3640,plain,
! [X0] : c_Set_Oinsert(X0,sF11,tc_nat) = c_Set_Oinsert(sF6,c_Set_Oinsert(X0,c_SetInterval_Oord__class_OatLeastLessThan(sF1,sF6,tc_nat),tc_nat),tc_nat),
inference(superposition,[],[f1693,f3631]) ).
fof(f5011,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(sF2),tc_nat)),
inference(superposition,[],[f1403,f1972]) ).
fof(f5024,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(sF3,tc_nat)),
inference(forward_demodulation,[],[f5011,f1974]) ).
fof(f5029,plain,
! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),X0),X0) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),X0),sF4),
inference(forward_demodulation,[],[f5024,f1976]) ).
fof(f5034,plain,
! [X0] : hAPP(hAPP(sF13,X0),X0) = hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),X0),sF4),
inference(forward_demodulation,[],[f5029,f1994]) ).
fof(f5050,plain,
sF4 = hAPP(hAPP(sF13,sF1),sF1),
inference(superposition,[],[f2348,f5034]) ).
fof(f5053,plain,
sF4 = hAPP(sF14,sF1),
inference(forward_demodulation,[],[f5050,f2421]) ).
fof(f6418,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat),X1,tc_nat) = c_HOL_Ominus__class_Ominus(X0,hAPP(hAPP(sF13,c_HOL_Oone__class_Oone(tc_nat)),X1),tc_nat),
inference(superposition,[],[f1929,f1994]) ).
fof(f6444,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(X0,sF1,tc_nat),X1,tc_nat) = c_HOL_Ominus__class_Ominus(X0,hAPP(hAPP(sF13,sF1),X1),tc_nat),
inference(forward_demodulation,[],[f6418,f1970]) ).
fof(f6455,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(X0,sF1,tc_nat),X1,tc_nat) = c_HOL_Ominus__class_Ominus(X0,hAPP(sF14,X1),tc_nat),
inference(forward_demodulation,[],[f6444,f1996]) ).
fof(f6482,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(X0,sF1,tc_nat),hAPP(sF14,X1),tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(X0,hAPP(sF14,sF1),tc_nat),X1,tc_nat),
inference(superposition,[],[f6455,f6455]) ).
fof(f6499,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(X0,sF1,tc_nat),hAPP(sF14,X1),tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(X0,sF16,tc_nat),X1,tc_nat),
inference(forward_demodulation,[],[f6482,f2593]) ).
fof(f6507,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(X0,sF1,tc_nat),hAPP(sF14,X1),tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(X0,sF4,tc_nat),X1,tc_nat),
inference(forward_demodulation,[],[f6499,f2650]) ).
fof(f6512,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(X0,sF4,tc_nat),X1,tc_nat) = c_HOL_Ominus__class_Ominus(X0,hAPP(sF14,hAPP(sF14,X1)),tc_nat),
inference(forward_demodulation,[],[f6507,f6455]) ).
fof(f6534,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(X0,hAPP(sF14,hAPP(sF14,hAPP(sF14,X1))),tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(X0,sF1,tc_nat),sF4,tc_nat),X1,tc_nat),
inference(superposition,[],[f6455,f6512]) ).
fof(f6537,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(X0,hAPP(sF14,hAPP(sF14,hAPP(sF14,X1))),tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(X0,hAPP(sF14,sF4),tc_nat),X1,tc_nat),
inference(forward_demodulation,[],[f6534,f6455]) ).
fof(f6550,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(X0,hAPP(sF14,hAPP(sF14,hAPP(sF14,X1))),tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(X0,sF6,tc_nat),X1,tc_nat),
inference(forward_demodulation,[],[f6537,f2326]) ).
fof(f6561,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(X0,sF6,tc_nat),X1,tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(X0,sF4,tc_nat),hAPP(sF14,X1),tc_nat),
inference(forward_demodulation,[],[f6550,f6512]) ).
fof(f6637,plain,
! [X0] :
( c_SetInterval_Oord__class_OatLeastLessThan(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat) = c_Set_Oinsert(c_HOL_Ozero__class_Ozero(tc_nat),c_SetInterval_Oord__class_OatLeastLessThan(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat),tc_nat)
| ~ c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ),
inference(superposition,[],[f1942,f1955]) ).
fof(f6648,plain,
! [X0] :
( c_Set_Oinsert(c_HOL_Ozero__class_Ozero(tc_nat),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat)
| ~ c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f6637,f1636]) ).
fof(f6656,plain,
! [X0] :
( c_Set_Oinsert(c_HOL_Ozero__class_Ozero(tc_nat),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(X0,sF1,tc_nat)
| ~ c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f6648,f1970]) ).
fof(f6663,plain,
! [X0] :
( c_SetInterval_Oord__class_OatMost(c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(X0,sF1,tc_nat)
| ~ c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f6656,f1597]) ).
fof(f6669,plain,
! [X0] :
( c_SetInterval_Oord__class_OatMost(sF0,tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(X0,sF1,tc_nat)
| ~ c_lessequals(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) ),
inference(forward_demodulation,[],[f6663,f1968]) ).
fof(f6673,plain,
! [X0] :
( c_SetInterval_Oord__class_OatMost(sF0,tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(X0,sF1,tc_nat)
| ~ c_lessequals(X0,sF0,tc_nat) ),
inference(forward_demodulation,[],[f6669,f1968]) ).
fof(f6688,plain,
( c_Set_Oinsert(sF0,sF8,tc_nat) = c_SetInterval_Oord__class_OatMost(sF0,tc_nat)
| ~ c_lessequals(sF0,sF0,tc_nat) ),
inference(superposition,[],[f2418,f6673]) ).
fof(f6693,plain,
c_Set_Oinsert(sF0,sF8,tc_nat) = c_SetInterval_Oord__class_OatMost(sF0,tc_nat),
inference(forward_subsumption_resolution,[],[f6688,f1489]) ).
fof(f6716,plain,
! [X0] : c_Set_Oinsert(X0,c_SetInterval_Oord__class_OatMost(sF0,tc_nat),tc_nat) = c_Set_Oinsert(sF0,c_Set_Oinsert(X0,sF8,tc_nat),tc_nat),
inference(superposition,[],[f1693,f6693]) ).
fof(f6729,plain,
c_Set_Oinsert(sF0,c_SetInterval_Oord__class_OatLeastLessThan(sF1,sF6,tc_nat),tc_nat) = c_Set_Oinsert(sF1,c_Set_Oinsert(sF4,c_SetInterval_Oord__class_OatMost(sF0,tc_nat),tc_nat),tc_nat),
inference(superposition,[],[f3566,f6716]) ).
fof(f6744,plain,
c_Set_Oinsert(sF4,c_SetInterval_Oord__class_OatMost(sF1,tc_nat),tc_nat) = c_Set_Oinsert(sF0,c_SetInterval_Oord__class_OatLeastLessThan(sF1,sF6,tc_nat),tc_nat),
inference(forward_demodulation,[],[f6729,f2808]) ).
fof(f6751,plain,
c_SetInterval_Oord__class_OatMost(sF4,tc_nat) = c_Set_Oinsert(sF0,c_SetInterval_Oord__class_OatLeastLessThan(sF1,sF6,tc_nat),tc_nat),
inference(forward_demodulation,[],[f6744,f2757]) ).
fof(f7217,plain,
! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(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),sF1),hAPP(hAPP(c_HOL_Oplus__class_Oplus(tc_nat),sF1),X0)),
inference(superposition,[],[f1948,f1970]) ).
fof(f7253,plain,
! [X0] : hAPP(hAPP(sF13,sF1),hAPP(hAPP(sF13,sF1),X0)) = hAPP(hAPP(sF13,X0),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)),
inference(forward_demodulation,[],[f7217,f1994]) ).
fof(f7270,plain,
! [X0] : hAPP(hAPP(sF13,sF1),hAPP(hAPP(sF13,sF1),X0)) = hAPP(hAPP(sF13,X0),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(sF2),tc_nat)),
inference(forward_demodulation,[],[f7253,f1972]) ).
fof(f7287,plain,
! [X0] : hAPP(hAPP(sF13,sF1),hAPP(hAPP(sF13,sF1),X0)) = hAPP(hAPP(sF13,X0),c_Int_Onumber__class_Onumber__of(sF3,tc_nat)),
inference(forward_demodulation,[],[f7270,f1974]) ).
fof(f7304,plain,
! [X0] : hAPP(hAPP(sF13,X0),sF4) = hAPP(hAPP(sF13,sF1),hAPP(hAPP(sF13,sF1),X0)),
inference(forward_demodulation,[],[f7287,f1976]) ).
fof(f7320,plain,
! [X0] : hAPP(hAPP(sF13,X0),sF4) = hAPP(sF14,hAPP(sF14,X0)),
inference(forward_demodulation,[],[f7304,f1996]) ).
fof(f7368,plain,
! [X0] : hAPP(sF14,c_Divides_Odiv__class_Odiv(X0,sF4,tc_nat)) = c_Divides_Odiv__class_Odiv(hAPP(sF14,hAPP(sF14,X0)),sF4,tc_nat),
inference(superposition,[],[f2286,f7320]) ).
fof(f7446,plain,
hAPP(sF14,c_Divides_Odiv__class_Odiv(sF4,sF4,tc_nat)) = c_Divides_Odiv__class_Odiv(hAPP(sF14,sF6),sF4,tc_nat),
inference(superposition,[],[f7368,f2326]) ).
fof(f7460,plain,
hAPP(sF14,c_Divides_Odiv__class_Odiv(sF4,sF4,tc_nat)) = c_Divides_Odiv__class_Odiv(sF18,sF4,tc_nat),
inference(forward_demodulation,[],[f7446,f2664]) ).
fof(f8284,plain,
! [X0,X1] : c_HOL_Oord__class_Oless(X0,hAPP(hAPP(sF13,c_HOL_Oone__class_Oone(tc_nat)),hAPP(hAPP(sF13,X1),X0)),tc_nat),
inference(superposition,[],[f1793,f1994]) ).
fof(f8308,plain,
! [X0,X1] : c_HOL_Oord__class_Oless(X0,hAPP(hAPP(sF13,sF1),hAPP(hAPP(sF13,X1),X0)),tc_nat),
inference(forward_demodulation,[],[f8284,f1970]) ).
fof(f8316,plain,
! [X0,X1] : c_HOL_Oord__class_Oless(X0,hAPP(sF14,hAPP(hAPP(sF13,X1),X0)),tc_nat),
inference(forward_demodulation,[],[f8308,f1996]) ).
fof(f8360,plain,
! [X0] : c_HOL_Oord__class_Oless(sF0,hAPP(sF14,X0),tc_nat),
inference(superposition,[],[f8316,f2426]) ).
fof(f8720,plain,
c_Set_Oinsert(sF0,sF11,tc_nat) = c_Set_Oinsert(sF6,c_SetInterval_Oord__class_OatMost(sF4,tc_nat),tc_nat),
inference(superposition,[],[f3640,f6751]) ).
fof(f8732,plain,
c_Set_Oinsert(sF0,sF11,tc_nat) = c_SetInterval_Oord__class_OatMost(sF6,tc_nat),
inference(forward_demodulation,[],[f8720,f2763]) ).
fof(f8735,plain,
sF12 = c_SetInterval_Oord__class_OatMost(sF6,tc_nat),
inference(forward_demodulation,[],[f8732,f1992]) ).
fof(f10452,plain,
! [X0] : c_lessequals(sF0,X0,tc_nat),
inference(superposition,[],[f901,f1968]) ).
fof(f10784,plain,
! [X0] : c_Divides_Odiv__class_Omod(X0,sF1,tc_nat) = c_HOL_Ominus__class_Ominus(X0,c_Divides_Odiv__class_Odiv(X0,sF1,tc_nat),tc_nat),
inference(superposition,[],[f1029,f2502]) ).
fof(f10802,plain,
! [X0] : c_HOL_Ominus__class_Ominus(X0,X0,tc_nat) = c_Divides_Odiv__class_Omod(X0,sF1,tc_nat),
inference(forward_demodulation,[],[f10784,f2099]) ).
fof(f10825,plain,
! [X0] : c_HOL_Ominus__class_Ominus(X0,X0,tc_nat) = sF0,
inference(forward_demodulation,[],[f10802,f2159]) ).
fof(f10860,plain,
! [X0] : c_HOL_Ominus__class_Ominus(sF1,hAPP(sF14,X0),tc_nat) = c_HOL_Ominus__class_Ominus(sF0,X0,tc_nat),
inference(superposition,[],[f6455,f10825]) ).
fof(f10861,plain,
! [X0] :
( c_HOL_Ominus__class_Ominus(hAPP(sF14,X0),sF1,tc_nat) = c_HOL_Ominus__class_Ominus(X0,sF0,tc_nat)
| ~ c_HOL_Oord__class_Oless(sF0,sF1,tc_nat) ),
inference(superposition,[],[f2269,f10825]) ).
fof(f10874,plain,
! [X0] : c_HOL_Ominus__class_Ominus(hAPP(sF14,X0),sF1,tc_nat) = c_HOL_Ominus__class_Ominus(X0,sF0,tc_nat),
inference(forward_subsumption_resolution,[],[f10861,f2553]) ).
fof(f10950,plain,
c_HOL_Ominus__class_Ominus(sF4,sF1,tc_nat) = c_HOL_Ominus__class_Ominus(sF1,sF0,tc_nat),
inference(superposition,[],[f10874,f5053]) ).
fof(f10952,plain,
c_HOL_Ominus__class_Ominus(sF6,sF1,tc_nat) = c_HOL_Ominus__class_Ominus(sF4,sF0,tc_nat),
inference(superposition,[],[f10874,f2326]) ).
fof(f10960,plain,
! [X0,X1] :
( c_HOL_Ominus__class_Ominus(hAPP(sF14,X1),hAPP(sF14,X0),tc_nat) = c_HOL_Ominus__class_Ominus(X1,c_HOL_Ominus__class_Ominus(X0,sF0,tc_nat),tc_nat)
| ~ c_HOL_Oord__class_Oless(sF0,hAPP(sF14,X0),tc_nat) ),
inference(superposition,[],[f2269,f10874]) ).
fof(f10972,plain,
! [X0,X1] : c_HOL_Ominus__class_Ominus(hAPP(sF14,X1),hAPP(sF14,X0),tc_nat) = c_HOL_Ominus__class_Ominus(X1,c_HOL_Ominus__class_Ominus(X0,sF0,tc_nat),tc_nat),
inference(forward_subsumption_resolution,[],[f10960,f8360]) ).
fof(f11285,plain,
! [X0] : c_HOL_Ominus__class_Ominus(hAPP(sF14,X0),sF1,tc_nat) = c_HOL_Ominus__class_Ominus(X0,c_HOL_Ominus__class_Ominus(sF0,sF0,tc_nat),tc_nat),
inference(superposition,[],[f10972,f2435]) ).
fof(f11316,plain,
! [X0] : c_HOL_Ominus__class_Ominus(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = c_HOL_Ominus__class_Ominus(hAPP(sF14,X0),sF1,tc_nat),
inference(forward_demodulation,[],[f11285,f891]) ).
fof(f11340,plain,
! [X0] : c_HOL_Ominus__class_Ominus(X0,c_HOL_Ozero__class_Ozero(tc_nat),tc_nat) = c_HOL_Ominus__class_Ominus(X0,sF0,tc_nat),
inference(forward_demodulation,[],[f11316,f10874]) ).
fof(f11352,plain,
! [X0] : c_HOL_Ominus__class_Ominus(X0,sF0,tc_nat) = X0,
inference(forward_demodulation,[],[f11340,f892]) ).
fof(f11763,plain,
! [X0] : c_HOL_Ominus__class_Ominus(sF6,hAPP(sF14,X0),tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(sF4,sF0,tc_nat),X0,tc_nat),
inference(superposition,[],[f6455,f10952]) ).
fof(f11776,plain,
! [X0] : c_HOL_Ominus__class_Ominus(sF4,X0,tc_nat) = c_HOL_Ominus__class_Ominus(sF6,hAPP(sF14,X0),tc_nat),
inference(forward_demodulation,[],[f11763,f11352]) ).
fof(f11804,plain,
c_HOL_Ominus__class_Ominus(sF4,sF1,tc_nat) = c_HOL_Ominus__class_Ominus(sF6,sF4,tc_nat),
inference(superposition,[],[f11776,f5053]) ).
fof(f11832,plain,
c_HOL_Ominus__class_Ominus(sF1,sF0,tc_nat) = c_HOL_Ominus__class_Ominus(sF6,sF4,tc_nat),
inference(forward_demodulation,[],[f11804,f10950]) ).
fof(f11844,plain,
sF1 = c_HOL_Ominus__class_Ominus(sF6,sF4,tc_nat),
inference(forward_demodulation,[],[f11832,f11352]) ).
fof(f11856,plain,
! [X0] : c_HOL_Ominus__class_Ominus(sF1,hAPP(sF14,X0),tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(sF6,sF6,tc_nat),X0,tc_nat),
inference(superposition,[],[f6561,f11844]) ).
fof(f11868,plain,
! [X0] : c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) = c_HOL_Ominus__class_Ominus(sF1,hAPP(sF14,X0),tc_nat),
inference(forward_demodulation,[],[f11856,f891]) ).
fof(f11873,plain,
! [X0] : c_HOL_Ominus__class_Ominus(c_HOL_Ozero__class_Ozero(tc_nat),X0,tc_nat) = c_HOL_Ominus__class_Ominus(sF0,X0,tc_nat),
inference(forward_demodulation,[],[f11868,f10860]) ).
fof(f11876,plain,
! [X0] : c_HOL_Ozero__class_Ozero(tc_nat) = c_HOL_Ominus__class_Ominus(sF0,X0,tc_nat),
inference(forward_demodulation,[],[f11873,f900]) ).
fof(f11879,plain,
! [X0] : sF0 = c_HOL_Ominus__class_Ominus(sF0,X0,tc_nat),
inference(forward_demodulation,[],[f11876,f1968]) ).
fof(f11896,plain,
! [X0] : sF0 = c_Divides_Odiv__class_Omod(sF0,X0,tc_nat),
inference(superposition,[],[f1029,f11879]) ).
fof(f11949,plain,
( sF0 != sF0
| c_Parity_Oeven__odd__class_Oeven(sF0,tc_nat) ),
inference(superposition,[],[f2248,f11896]) ).
fof(f11953,plain,
c_Parity_Oeven__odd__class_Oeven(sF0,tc_nat),
inference(trivial_inequality_removal,[],[f11949]) ).
fof(f12590,plain,
! [X0] : 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_OBit1(c_Int_OPls)),tc_nat)),X0),X0,tc_nat) = X0,
inference(superposition,[],[f546,f1405]) ).
fof(f12684,plain,
! [X0] : 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),X0,tc_nat) = X0,
inference(forward_demodulation,[],[f12590,f1972]) ).
fof(f12709,plain,
! [X0] : c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),c_Int_Onumber__class_Onumber__of(sF3,tc_nat)),X0),X0,tc_nat) = X0,
inference(forward_demodulation,[],[f12684,f1974]) ).
fof(f12722,plain,
! [X0] : c_HOL_Ominus__class_Ominus(hAPP(hAPP(c_HOL_Otimes__class_Otimes(tc_nat),sF4),X0),X0,tc_nat) = X0,
inference(forward_demodulation,[],[f12709,f1976]) ).
fof(f12846,plain,
! [X0] :
( c_Divides_Odiv__class_Odiv(X0,sF4,tc_nat) = c_HOL_Ominus__class_Ominus(X0,c_Divides_Odiv__class_Odiv(X0,sF4,tc_nat),tc_nat)
| ~ c_Parity_Oeven__odd__class_Oeven(X0,tc_nat) ),
inference(superposition,[],[f12722,f2222]) ).
fof(f14141,plain,
( sF0 = c_Divides_Odiv__class_Odiv(sF0,sF4,tc_nat)
| ~ c_Parity_Oeven__odd__class_Oeven(sF0,tc_nat) ),
inference(superposition,[],[f11879,f12846]) ).
fof(f14146,plain,
sF0 = c_Divides_Odiv__class_Odiv(sF0,sF4,tc_nat),
inference(forward_subsumption_resolution,[],[f14141,f11953]) ).
fof(f14217,plain,
c_Set_Oinsert(sF0,c_Set_Oinsert(c_Divides_Odiv__class_Odiv(sF4,sF4,tc_nat),sF8,tc_nat),tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(sF0,hAPP(sF14,c_Divides_Odiv__class_Odiv(sF4,sF4,tc_nat)),tc_nat),
inference(superposition,[],[f3371,f14146]) ).
fof(f14218,plain,
c_SetInterval_Oord__class_OatMost(c_Divides_Odiv__class_Odiv(sF4,sF4,tc_nat),tc_nat) = c_Set_Oinsert(c_Divides_Odiv__class_Odiv(sF4,sF4,tc_nat),c_SetInterval_Oord__class_OatMost(sF0,tc_nat),tc_nat),
inference(superposition,[],[f2761,f14146]) ).
fof(f14220,plain,
hAPP(sF14,sF0) = c_Divides_Odiv__class_Odiv(sF4,sF4,tc_nat),
inference(superposition,[],[f2386,f14146]) ).
fof(f14229,plain,
sF15 = c_Divides_Odiv__class_Odiv(sF4,sF4,tc_nat),
inference(forward_demodulation,[],[f14220,f1998]) ).
fof(f14231,plain,
c_Set_Oinsert(sF0,c_Set_Oinsert(c_Divides_Odiv__class_Odiv(sF4,sF4,tc_nat),sF8,tc_nat),tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(sF0,c_Divides_Odiv__class_Odiv(sF18,sF4,tc_nat),tc_nat),
inference(forward_demodulation,[],[f14217,f7460]) ).
fof(f14233,plain,
sF1 = c_Divides_Odiv__class_Odiv(sF4,sF4,tc_nat),
inference(forward_demodulation,[],[f14229,f2589]) ).
fof(f14234,plain,
c_Set_Oinsert(c_Divides_Odiv__class_Odiv(sF4,sF4,tc_nat),c_SetInterval_Oord__class_OatMost(sF0,tc_nat),tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(sF0,c_Divides_Odiv__class_Odiv(sF18,sF4,tc_nat),tc_nat),
inference(forward_demodulation,[],[f14231,f6716]) ).
fof(f14236,plain,
c_SetInterval_Oord__class_OatMost(c_Divides_Odiv__class_Odiv(sF4,sF4,tc_nat),tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(sF0,c_Divides_Odiv__class_Odiv(sF18,sF4,tc_nat),tc_nat),
inference(forward_demodulation,[],[f14234,f14218]) ).
fof(f14238,plain,
c_SetInterval_Oord__class_OatMost(sF1,tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(sF0,c_Divides_Odiv__class_Odiv(sF18,sF4,tc_nat),tc_nat),
inference(forward_demodulation,[],[f14236,f14233]) ).
fof(f14254,plain,
hAPP(sF14,sF1) = c_Divides_Odiv__class_Odiv(sF18,sF4,tc_nat),
inference(superposition,[],[f7460,f14233]) ).
fof(f14277,plain,
sF16 = c_Divides_Odiv__class_Odiv(sF18,sF4,tc_nat),
inference(forward_demodulation,[],[f14254,f2593]) ).
fof(f14286,plain,
sF4 = c_Divides_Odiv__class_Odiv(sF18,sF4,tc_nat),
inference(forward_demodulation,[],[f14277,f2650]) ).
fof(f14624,plain,
( c_Set_Oinsert(c_Divides_Odiv__class_Odiv(sF18,sF4,tc_nat),c_SetInterval_Oord__class_OatMost(sF1,tc_nat),tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(sF0,hAPP(sF14,c_Divides_Odiv__class_Odiv(sF18,sF4,tc_nat)),tc_nat)
| ~ c_lessequals(sF0,c_Divides_Odiv__class_Odiv(sF18,sF4,tc_nat),tc_nat) ),
inference(superposition,[],[f3289,f14238]) ).
fof(f14629,plain,
c_Set_Oinsert(c_Divides_Odiv__class_Odiv(sF18,sF4,tc_nat),c_SetInterval_Oord__class_OatMost(sF1,tc_nat),tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(sF0,hAPP(sF14,c_Divides_Odiv__class_Odiv(sF18,sF4,tc_nat)),tc_nat),
inference(forward_subsumption_resolution,[],[f14624,f10452]) ).
fof(f14637,plain,
c_Set_Oinsert(sF4,c_SetInterval_Oord__class_OatMost(sF1,tc_nat),tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(sF0,hAPP(sF14,sF4),tc_nat),
inference(forward_demodulation,[],[f14629,f14286]) ).
fof(f14645,plain,
c_Set_Oinsert(sF4,c_SetInterval_Oord__class_OatMost(sF1,tc_nat),tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(sF0,sF6,tc_nat),
inference(forward_demodulation,[],[f14637,f2326]) ).
fof(f14653,plain,
c_SetInterval_Oord__class_OatMost(sF4,tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(sF0,sF6,tc_nat),
inference(forward_demodulation,[],[f14645,f2757]) ).
fof(f14673,plain,
( c_Set_Oinsert(sF6,c_SetInterval_Oord__class_OatMost(sF4,tc_nat),tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(sF0,hAPP(sF14,sF6),tc_nat)
| ~ c_lessequals(sF0,sF6,tc_nat) ),
inference(superposition,[],[f3289,f14653]) ).
fof(f14678,plain,
c_Set_Oinsert(sF6,c_SetInterval_Oord__class_OatMost(sF4,tc_nat),tc_nat) = c_SetInterval_Oord__class_OatLeastLessThan(sF0,hAPP(sF14,sF6),tc_nat),
inference(forward_subsumption_resolution,[],[f14673,f10452]) ).
fof(f14686,plain,
c_SetInterval_Oord__class_OatLeastLessThan(sF0,sF18,tc_nat) = c_Set_Oinsert(sF6,c_SetInterval_Oord__class_OatMost(sF4,tc_nat),tc_nat),
inference(forward_demodulation,[],[f14678,f2664]) ).
fof(f14694,plain,
c_SetInterval_Oord__class_OatLeastLessThan(sF0,sF18,tc_nat) = c_SetInterval_Oord__class_OatMost(sF6,tc_nat),
inference(forward_demodulation,[],[f14686,f2763]) ).
fof(f14702,plain,
sF12 = c_SetInterval_Oord__class_OatLeastLessThan(sF0,sF18,tc_nat),
inference(forward_demodulation,[],[f14694,f8735]) ).
fof(f14713,plain,
sF12 = sF19,
inference(superposition,[],[f2006,f14702]) ).
fof(f14728,plain,
$false,
inference(forward_subsumption_resolution,[],[f14713,f2007]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV576-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.18 % Computer : n008.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.19 % DateTime : Mon Sep 28 11:55:24 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.22 Running first-order theorem proving
% 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.24/2.42 % (2197404)Input is clausal, will run a generic CNF schedule.
% 12.24/2.42 % (2197410)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1077911787:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 12.24/2.42 % (2197413)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1342449838:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 12.24/2.42 % (2197412)lrs+10_1_sil=8000:sp=occurrence:random_seed=2667891234:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 12.24/2.42 % (2197409)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=3740317912:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 12.24/2.42 % (2197414)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3571036986:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 12.24/2.42 % (2197411)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=730508151:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 12.24/2.42 % (2197415)dis-21_1_sil=8000:lcm=predicate:random_seed=804322368: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.24/2.42 % (2197415)Instruction limit reached!
% 12.24/2.42 % (2197415)------------------------------
% 12.24/2.42 % (2197415)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.24/2.42 % (2197415)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.24/2.42 % (2197415)CaDiCaL version: 2.1.3
% 12.24/2.42 % (2197415)Termination reason: Instruction limit
% 12.24/2.42 % (2197415)Termination phase: Saturation
% 12.24/2.42 % (2197415)Time elapsed: 0.060 s
% 12.24/2.42 % (2197415)Peak memory usage: 90 MB
% 12.24/2.42 % (2197415)Instructions burned: 117 (million)
% 12.24/2.42 % (2197412)Instruction limit reached!
% 12.24/2.42 % (2197412)------------------------------
% 12.24/2.42 % (2197412)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.24/2.42 % (2197412)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.24/2.42 % (2197412)CaDiCaL version: 2.1.3
% 12.24/2.42 % (2197412)Termination reason: Instruction limit
% 12.24/2.42 % (2197412)Termination phase: Saturation
% 12.24/2.42 % (2197412)Time elapsed: 0.068 s
% 12.24/2.42 % (2197412)Peak memory usage: 90 MB
% 12.24/2.42 % (2197412)Instructions burned: 108 (million)
% 12.24/2.42 % (2197413)Instruction limit reached!
% 12.24/2.42 % (2197413)------------------------------
% 12.24/2.42 % (2197413)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.24/2.42 % (2197413)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.24/2.42 % (2197413)CaDiCaL version: 2.1.3
% 12.24/2.42 % (2197413)Termination reason: Instruction limit
% 12.24/2.42 % (2197413)Termination phase: Saturation
% 12.24/2.42 % (2197413)Time elapsed: 0.073 s
% 12.24/2.42 % (2197413)Peak memory usage: 89 MB
% 12.24/2.42 % (2197413)Instructions burned: 115 (million)
% 12.24/2.42 % (2197414)Instruction limit reached!
% 12.24/2.42 % (2197414)------------------------------
% 12.24/2.42 % (2197414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.24/2.42 % (2197414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.24/2.42 % (2197414)CaDiCaL version: 2.1.3
% 12.24/2.42 % (2197414)Termination reason: Instruction limit
% 12.24/2.42 % (2197414)Termination phase: Saturation
% 12.24/2.42 % (2197414)Time elapsed: 0.109 s
% 12.24/2.42 % (2197414)Peak memory usage: 90 MB
% 12.24/2.42 % (2197414)Instructions burned: 181 (million)
% 12.24/2.42 % (2197423)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=1862360636:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 12.24/2.42 % (2197424)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2691299713: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.24/2.42 % (2197425)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=2593679996:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 12.24/2.42 % (2197423)Refutation not found, incomplete strategy
% 12.24/2.42 % (2197423)------------------------------
% 12.24/2.42 % (2197423)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.69/3.83 % (2197423)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.69/3.83 % (2197423)CaDiCaL version: 2.1.3
% 21.69/3.83 % (2197423)Termination reason: Refutation not found, incomplete strategy
% 21.69/3.83 % (2197423)Time elapsed: 0.017 s
% 21.69/3.83 % (2197423)Peak memory usage: 89 MB
% 21.69/3.83 % (2197423)Instructions burned: 26 (million)
% 21.69/3.83 % (2197425)Refutation not found, incomplete strategy
% 21.69/3.83 % (2197425)------------------------------
% 21.69/3.83 % (2197425)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.69/3.83 % (2197425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.69/3.83 % (2197425)CaDiCaL version: 2.1.3
% 21.69/3.83 % (2197425)Termination reason: Refutation not found, incomplete strategy
% 21.69/3.83 % (2197425)Time elapsed: 0.035 s
% 21.69/3.83 % (2197425)Peak memory usage: 90 MB
% 21.69/3.83 % (2197425)Instructions burned: 62 (million)
% 21.69/3.83 % (2197426)lrs+10_64_to=lpo:sil=8000:random_seed=2634790600:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 21.69/3.83 % (2197424)Instruction limit reached!
% 21.69/3.83 % (2197424)------------------------------
% 21.69/3.83 % (2197424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.69/3.83 % (2197424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.69/3.83 % (2197424)CaDiCaL version: 2.1.3
% 21.69/3.83 % (2197424)Termination reason: Instruction limit
% 21.69/3.83 % (2197424)Termination phase: Saturation
% 21.69/3.83 % (2197424)Time elapsed: 0.097 s
% 21.69/3.83 % (2197424)Peak memory usage: 91 MB
% 21.69/3.83 % (2197424)Instructions burned: 191 (million)
% 21.69/3.83 % (2197426)Instruction limit reached!
% 21.69/3.83 % (2197426)------------------------------
% 21.69/3.83 % (2197426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.69/3.83 % (2197426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.69/3.83 % (2197426)CaDiCaL version: 2.1.3
% 21.69/3.83 % (2197426)Termination reason: Instruction limit
% 21.69/3.83 % (2197426)Termination phase: Saturation
% 21.69/3.83 % (2197426)Time elapsed: 0.076 s
% 21.69/3.83 % (2197426)Peak memory usage: 90 MB
% 21.69/3.83 % (2197426)Instructions burned: 127 (million)
% 21.69/3.83 % (2197423)------------------------------
% 21.69/3.83 % (2197423)------------------------------
% 21.69/3.83 % (2197431)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=3431862044:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 21.69/3.83 % (2197425)------------------------------
% 21.69/3.83 % (2197425)------------------------------
% 21.69/3.83 % (2197432)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=831434811:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 21.69/3.83 % (2197431)Instruction limit reached!
% 21.69/3.83 % (2197431)------------------------------
% 21.69/3.83 % (2197431)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.69/3.83 % (2197431)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.69/3.83 % (2197431)CaDiCaL version: 2.1.3
% 21.69/3.83 % (2197431)Termination reason: Instruction limit
% 21.69/3.83 % (2197431)Termination phase: Saturation
% 21.69/3.83 % (2197431)Time elapsed: 0.116 s
% 21.69/3.83 % (2197431)Peak memory usage: 91 MB
% 21.69/3.83 % (2197431)Instructions burned: 194 (million)
% 21.69/3.83 % (2197432)Instruction limit reached!
% 21.69/3.83 % (2197432)------------------------------
% 21.69/3.83 % (2197432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.69/3.83 % (2197432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.69/3.83 % (2197432)CaDiCaL version: 2.1.3
% 21.69/3.83 % (2197432)Termination reason: Instruction limit
% 21.69/3.83 % (2197432)Termination phase: Saturation
% 21.69/3.83 % (2197432)Time elapsed: 0.094 s
% 21.69/3.83 % (2197432)Peak memory usage: 91 MB
% 21.69/3.83 % (2197432)Instructions burned: 158 (million)
% 21.69/3.83 % (2197434)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3794651184:i=3394:sd=4:ss=included:sgt=64_2992 on theBenchmark for (2992ds/3394Mi)
% 21.69/3.83 % (2197435)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=1683048205:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2992 on theBenchmark for (2992ds/106Mi)
% 21.69/3.83 % (2197435)Instruction limit reached!
% 21.69/3.83 % (2197435)------------------------------
% 21.69/3.83 % (2197435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.69/3.83 % (2197435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.69/3.83 % (2197435)CaDiCaL version: 2.1.3
% 21.69/3.83 % (2197435)Termination reason: Instruction limit
% 21.69/3.83 % (2197435)Termination phase: Saturation
% 21.69/3.83 % (2197435)Time elapsed: 0.051 s
% 21.69/3.83 % (2197435)Peak memory usage: 89 MB
% 21.69/3.83 % (2197435)Instructions burned: 107 (million)
% 21.69/3.83 % (2197438)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=317450111:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 21.69/3.83 % (2197437)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2317510455:i=107_2991 on theBenchmark for (2991ds/107Mi)
% 21.69/3.83 % (2197437)Refutation not found, incomplete strategy
% 21.69/3.83 % (2197437)------------------------------
% 21.69/3.83 % (2197437)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.69/3.83 % (2197437)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.69/3.83 % (2197437)CaDiCaL version: 2.1.3
% 21.69/3.83 % (2197437)Termination reason: Refutation not found, incomplete strategy
% 21.69/3.83 % (2197437)Time elapsed: 0.032 s
% 21.69/3.83 % (2197437)Peak memory usage: 90 MB
% 21.69/3.83 % (2197437)Instructions burned: 58 (million)
% 21.69/3.83 % (2197441)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2637629316:cond=fast:i=5208:av=off_2990 on theBenchmark for (2990ds/5208Mi)
% 21.69/3.83 % (2197438)Instruction limit reached!
% 21.69/3.83 % (2197438)------------------------------
% 21.69/3.83 % (2197438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.69/3.83 % (2197438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.69/3.83 % (2197438)CaDiCaL version: 2.1.3
% 21.69/3.83 % (2197438)Termination reason: Instruction limit
% 21.69/3.83 % (2197438)Termination phase: Saturation
% 21.69/3.83 % (2197438)Time elapsed: 0.132 s
% 21.69/3.83 % (2197438)Peak memory usage: 90 MB
% 21.69/3.83 % (2197438)Instructions burned: 242 (million)
% 21.69/3.83 % (2197437)------------------------------
% 21.69/3.83 % (2197437)------------------------------
% 21.69/3.83 % (2197445)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1543249654:i=134:sd=2:doe=on:ss=axioms:sgt=14_2988 on theBenchmark for (2988ds/134Mi)
% 21.69/3.83 % (2197445)Instruction limit reached!
% 21.69/3.83 % (2197445)------------------------------
% 21.69/3.83 % (2197445)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.69/3.83 % (2197445)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.69/3.83 % (2197445)CaDiCaL version: 2.1.3
% 21.69/3.83 % (2197445)Termination reason: Instruction limit
% 21.69/3.83 % (2197445)Termination phase: Saturation
% 21.69/3.83 % (2197445)Time elapsed: 0.087 s
% 21.69/3.83 % (2197445)Peak memory usage: 90 MB
% 21.69/3.83 % (2197445)Instructions burned: 135 (million)
% 21.69/3.83 % (2197446)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=429923117:i=499:bd=all_2987 on theBenchmark for (2987ds/499Mi)
% 21.69/3.83 % (2197448)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3117369457:i=191:fgj=on:bd=all_2986 on theBenchmark for (2986ds/191Mi)
% 21.69/3.83 % (2197448)Instruction limit reached!
% 21.69/3.83 % (2197448)------------------------------
% 21.69/3.83 % (2197448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.69/3.83 % (2197448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.69/3.83 % (2197448)CaDiCaL version: 2.1.3
% 21.69/3.83 % (2197448)Termination reason: Instruction limit
% 21.69/3.83 % (2197448)Termination phase: Saturation
% 21.69/3.83 % (2197448)Time elapsed: 0.113 s
% 21.69/3.83 % (2197448)Peak memory usage: 90 MB
% 21.69/3.83 % (2197448)Instructions burned: 192 (million)
% 21.69/3.83 % (2197446)Instruction limit reached!
% 21.69/3.83 % (2197446)------------------------------
% 21.69/3.83 % (2197446)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.69/3.83 % (2197446)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.69/3.83 % (2197446)CaDiCaL version: 2.1.3
% 21.69/3.83 % (2197446)Termination reason: Instruction limit
% 21.69/3.83 % (2197446)Termination phase: Saturation
% 21.69/3.83 % (2197446)Time elapsed: 0.317 s
% 21.69/3.83 % (2197446)Peak memory usage: 94 MB
% 21.69/3.83 % (2197446)Instructions burned: 500 (million)
% 21.69/3.83 % (2197451)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=1349634316:i=264:kws=precedence:fsr=off_2983 on theBenchmark for (2983ds/264Mi)
% 21.69/3.83 % (2197452)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3610233151:cond=on:i=156:bs=on:gtg=exists_all:er=known_2982 on theBenchmark for (2982ds/156Mi)
% 21.69/3.83 % (2197451)Instruction limit reached!
% 21.69/3.83 % (2197451)------------------------------
% 21.69/3.83 % (2197451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.69/3.83 % (2197451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.69/3.83 % (2197451)CaDiCaL version: 2.1.3
% 21.69/3.83 % (2197451)Termination reason: Instruction limit
% 21.69/3.83 % (2197451)Termination phase: Saturation
% 21.69/3.83 % (2197451)Time elapsed: 0.154 s
% 21.69/3.83 % (2197451)Peak memory usage: 93 MB
% 21.69/3.83 % (2197451)Instructions burned: 265 (million)
% 21.69/3.83 % (2197452)Instruction limit reached!
% 21.69/3.83 % (2197452)------------------------------
% 21.69/3.83 % (2197452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.69/3.83 % (2197452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.69/3.83 % (2197452)CaDiCaL version: 2.1.3
% 21.69/3.83 % (2197452)Termination reason: Instruction limit
% 21.69/3.83 % (2197452)Termination phase: Saturation
% 21.69/3.83 % (2197452)Time elapsed: 0.091 s
% 21.69/3.83 % (2197452)Peak memory usage: 90 MB
% 21.69/3.83 % (2197452)Instructions burned: 156 (million)
% 21.69/3.83 % (2197455)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=2823097757:i=3256:kws=precedence:bd=preordered:av=off_2980 on theBenchmark for (2980ds/3256Mi)
% 21.69/3.83 % (2197456)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=2089503184:i=537:av=off:ss=included_2979 on theBenchmark for (2979ds/537Mi)
% 21.69/3.83 % (2197456)Instruction limit reached!
% 21.69/3.83 % (2197456)------------------------------
% 21.69/3.83 % (2197456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.69/3.83 % (2197456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.69/3.83 % (2197456)CaDiCaL version: 2.1.3
% 21.69/3.83 % (2197456)Termination reason: Instruction limit
% 21.69/3.83 % (2197456)Termination phase: Saturation
% 21.69/3.83 % (2197456)Time elapsed: 0.309 s
% 21.69/3.83 % (2197456)Peak memory usage: 92 MB
% 21.69/3.83 % (2197456)Instructions burned: 537 (million)
% 21.69/3.83 % (2197459)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3958671856:i=180:bd=preordered:av=off_2975 on theBenchmark for (2975ds/180Mi)
% 21.69/3.83 % (2197459)Instruction limit reached!
% 21.69/3.83 % (2197459)------------------------------
% 21.69/3.83 % (2197459)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.69/3.83 % (2197459)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.69/3.83 % (2197459)CaDiCaL version: 2.1.3
% 21.69/3.83 % (2197459)Termination reason: Instruction limit
% 21.69/3.83 % (2197459)Termination phase: Saturation
% 21.69/3.83 % (2197459)Time elapsed: 0.104 s
% 21.69/3.83 % (2197459)Peak memory usage: 90 MB
% 21.69/3.83 % (2197459)Instructions burned: 181 (million)
% 21.69/3.83 % (2197441)First to succeed.
% 21.69/3.83 % (2197441)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2197404"
% 21.69/3.83 % (2197461)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=1199682088:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2972 on theBenchmark for (2972ds/10307Mi)
% 21.69/3.83 % (2197434)Instruction limit reached!
% 21.69/3.83 % (2197434)------------------------------
% 21.69/3.83 % (2197434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.69/3.83 % (2197434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.69/3.83 % (2197434)CaDiCaL version: 2.1.3
% 21.69/3.83 % (2197434)Termination reason: Instruction limit
% 21.69/3.83 % (2197434)Termination phase: Saturation
% 21.69/3.83 % (2197434)Time elapsed: 2.124 s
% 21.69/3.83 % (2197434)Peak memory usage: 146 MB
% 21.69/3.83 % (2197434)Instructions burned: 3395 (million)
% 21.69/3.83 % (2197441)Refutation found. Thanks to Tanya!
% 21.69/3.83 % SZS status Unsatisfiable for theBenchmark
% 21.69/3.83 % SZS output start Proof for theBenchmark
% See solution above
% 0.20/4.03 % (2197441)------------------------------
% 0.20/4.03 % (2197441)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.20/4.03 % (2197441)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.20/4.03 % (2197441)CaDiCaL version: 2.1.3
% 0.20/4.03 % (2197441)Termination reason: Refutation
% 0.20/4.03 % (2197441)Time elapsed: 1.765 s
% 0.20/4.03 % (2197441)Peak memory usage: 146 MB
% 0.20/4.03 % (2197441)Instructions burned: 2818 (million)
% 0.20/4.03 % (2197441)------------------------------
% 0.20/4.03 % (2197441)------------------------------
% 0.20/4.03 % (2197404)Success in time 3.167 s
% 0.20/4.03 % Vampire exiting
%------------------------------------------------------------------------------