%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV577-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n015.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:19:01 PM UTC 2026
% Result : Unsatisfiable 75.68s 20.05s
% Output : Refutation 139.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 20
% Number of leaves : 23
% Syntax : Number of formulae : 102 ( 87 unt; 1 def)
% Number of atoms : 120 ( 76 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 39 ( 21 ~; 18 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 10 ( 2 avg)
% Number of predicates : 6 ( 4 usr; 1 prp; 0-3 aty)
% Number of functors : 18 ( 18 usr; 5 con; 0-4 aty)
% Number of variables : 136 ( 136 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f27,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/sandbox/benchmark/theBenchmark.p',cls_insert__commute_0) ).
fof(f96,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/sandbox/benchmark/theBenchmark.p',cls_atLeastLessThan__singleton_0) ).
fof(f170,axiom,
! [X0] : c_HOL_Oord__class_Oless(X0,c_Suc(X0),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_less__Suc__eq_2) ).
fof(f176,axiom,
! [X0,X1] :
( c_SetInterval_Oord__class_OatLeastLessThan(X0,c_Suc(X1),tc_nat) = c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool))
| c_lessequals(X0,X1,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_atLeastLessThanSuc_1) ).
fof(f177,plain,
! [X0,X1] :
( c_lessequals(X0,X1,tc_nat)
| c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)) = c_SetInterval_Oord__class_OatLeastLessThan(X0,c_Suc(X1),tc_nat) ),
inference(reorient_equations,[],[f176]) ).
fof(f586,axiom,
! [X0,X1] :
( c_HOL_Oord__class_Oless(X0,c_Suc(X1),tc_nat)
| c_HOL_Oord__class_Oless(X1,X0,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_not__less__eq_0) ).
fof(f774,axiom,
! [X2,X3,X0,X1] :
( ~ c_HOL_Oord__class_Oless(X2,X3,tc_nat)
| c_Finite__Set_Osetsum(X1,c_SetInterval_Oord__class_OatLeastLessThan(X2,X3,tc_nat),tc_nat,X0) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),hAPP(X1,X2)),c_Finite__Set_Osetsum(X1,c_SetInterval_Oord__class_OatLeastLessThan(c_Suc(X2),X3,tc_nat),tc_nat,X0))
| ~ class_OrderedGroup_Ocomm__monoid__add(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_setsum__head__upt__Suc_0) ).
fof(f980,axiom,
! [X2,X0,X1] :
( ~ class_OrderedGroup_Ocomm__monoid__add(X0)
| c_Finite__Set_Osetsum(X1,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2,X0) = c_HOL_Ozero__class_Ozero(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_setsum__empty_0) ).
fof(f981,plain,
! [X2,X0,X1] :
( ~ class_OrderedGroup_Ocomm__monoid__add(X0)
| c_HOL_Ozero__class_Ozero(X0) = c_Finite__Set_Osetsum(X1,c_Orderings_Obot__class_Obot(tc_fun(X2,tc_bool)),X2,X0) ),
inference(reorient_equations,[],[f980]) ).
fof(f1014,axiom,
c_HOL_Oone__class_Oone(tc_nat) = c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_One__nat__def_0) ).
fof(f1015,plain,
c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)) = c_HOL_Oone__class_Oone(tc_nat),
inference(reorient_equations,[],[f1014]) ).
fof(f1064,axiom,
! [X0,X1] :
( ~ c_HOL_Oord__class_Oless(X0,X1,tc_nat)
| c_lessequals(X0,X1,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_nat__less__le_0) ).
fof(f1084,axiom,
! [X0,X1] :
( c_lessequals(X0,c_Suc(X1),tc_nat)
| ~ c_lessequals(X0,X1,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_le__SucI_0) ).
fof(f1089,axiom,
! [X0] : ~ c_lessequals(c_Suc(X0),X0,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Suc__n__not__le__n_0) ).
fof(f1153,axiom,
! [X0,X1] :
( ~ c_lessequals(X0,X1,tc_nat)
| 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) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_atLeastLessThanSuc_0) ).
fof(f1191,axiom,
! [X2,X3,X0,X1,X4] :
( ~ c_lessequals(X3,X4,tc_nat)
| hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),c_Finite__Set_Osetsum(X1,c_SetInterval_Oord__class_OatLeastLessThan(X2,X3,tc_nat),tc_nat,X0)),c_Finite__Set_Osetsum(X1,c_SetInterval_Oord__class_OatLeastLessThan(X3,X4,tc_nat),tc_nat,X0)) = c_Finite__Set_Osetsum(X1,c_SetInterval_Oord__class_OatLeastLessThan(X2,X4,tc_nat),tc_nat,X0)
| ~ class_OrderedGroup_Ocomm__monoid__add(X0)
| ~ c_lessequals(X2,X3,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_setsum__add__nat__ivl_0) ).
fof(f1192,axiom,
c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) = c_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/sandbox/benchmark/theBenchmark.p',cls_Ivl4_0) ).
fof(f1199,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/sandbox/benchmark/theBenchmark.p',cls_numeral__3__eq__3_0) ).
fof(f1218,axiom,
c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat) = c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_numeral__2__eq__2_0) ).
fof(f1219,plain,
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),
inference(reorient_equations,[],[f1218]) ).
fof(f1244,axiom,
! [X2,X0,X1] :
( ~ class_OrderedGroup_Ocomm__monoid__add(X0)
| hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),X1),X2) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),X2),X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_comm__monoid__add_Omult__commute_0) ).
fof(f1281,axiom,
! [X2,X3,X0,X1] :
( ~ class_OrderedGroup_Ocomm__monoid__add(X0)
| hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),X1),hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),X2),X3)) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),X2),hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),X1),X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_comm__monoid__add_Omult__left__commute_0) ).
fof(f1282,axiom,
! [X2,X3,X0,X1] :
( ~ class_OrderedGroup_Ocomm__monoid__add(X0)
| hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),X1),X2)),X3) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),X1),hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),X2),X3)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_comm__monoid__add_Omult__assoc_0) ).
fof(f1283,plain,
! [X2,X3,X0,X1] :
( ~ class_OrderedGroup_Ocomm__monoid__add(X0)
| hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),X1),hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),X2),X3)) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),X1),X2)),X3) ),
inference(reorient_equations,[],[f1282]) ).
fof(f1304,axiom,
! [X0,X1] :
( ~ class_OrderedGroup_Ocomm__monoid__add(X0)
| hAPP(hAPP(c_HOL_Oplus__class_Oplus(X0),c_HOL_Ozero__class_Ozero(X0)),X1) = X1 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_comm__monoid__add_Omult__1_0) ).
fof(f1307,negated_conjecture,
class_OrderedGroup_Ocomm__monoid__add(t_a),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',tfree_tcs) ).
fof(f1308,negated_conjecture,
c_Finite__Set_Osetsum(v_x,c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat),tc_nat,t_a) != hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_x,c_HOL_Ozero__class_Ozero(tc_nat))),hAPP(v_x,c_HOL_Oone__class_Oone(tc_nat)))),hAPP(v_x,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)))),hAPP(v_x,c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OBit1(c_Int_OPls)),tc_nat))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f1399,definition,
~ sP0(c_Finite__Set_Osetsum(v_x,c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat),tc_nat,t_a)),
introduced(definition,[new_symbols(definition,[sP0])],[inequality_splitting_name_introduction]) ).
fof(f1400,plain,
sP0(hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_x,c_HOL_Ozero__class_Ozero(tc_nat))),hAPP(v_x,c_HOL_Oone__class_Oone(tc_nat)))),hAPP(v_x,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)))),hAPP(v_x,c_Int_Onumber__class_Onumber__of(c_Int_OBit1(c_Int_OBit1(c_Int_OPls)),tc_nat)))),
inference(inequality_splitting,[],[f1308,f1399]) ).
fof(f1416,plain,
c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) = c_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_OBit1(c_Int_OBit1(c_Int_OPls)),tc_nat),c_Set_Oinsert(c_Int_Onumber__class_Onumber__of(c_Int_OBit0(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),
inference(forward_demodulation,[],[f1192,f27]) ).
fof(f1417,plain,
sP0(hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_x,c_HOL_Ozero__class_Ozero(tc_nat))),hAPP(v_x,c_HOL_Oone__class_Oone(tc_nat)))),hAPP(v_x,c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit1(c_Int_OPls)),tc_nat)))),hAPP(v_x,c_Suc(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))))))),
inference(forward_demodulation,[],[f1400,f1199]) ).
fof(f1424,plain,
c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) = c_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_OBit1(c_Int_OBit1(c_Int_OPls)),tc_nat),c_Set_Oinsert(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),tc_nat),tc_nat),
inference(forward_demodulation,[],[f1416,f1219]) ).
fof(f1425,plain,
sP0(hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_x,c_HOL_Ozero__class_Ozero(tc_nat))),hAPP(v_x,c_HOL_Oone__class_Oone(tc_nat)))),hAPP(v_x,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)))))),hAPP(v_x,c_Suc(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))))))),
inference(forward_demodulation,[],[f1417,f1219]) ).
fof(f1430,plain,
c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) = c_Set_Oinsert(c_HOL_Ozero__class_Ozero(tc_nat),c_Set_Oinsert(c_HOL_Oone__class_Oone(tc_nat),c_Set_Oinsert(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(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),
inference(forward_demodulation,[],[f1424,f27]) ).
fof(f1431,plain,
sP0(hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_x,c_HOL_Ozero__class_Ozero(tc_nat))),hAPP(v_x,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))))),hAPP(v_x,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)))))),hAPP(v_x,c_Suc(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))))))),
inference(forward_demodulation,[],[f1425,f1015]) ).
fof(f1433,plain,
c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) = c_Set_Oinsert(c_HOL_Ozero__class_Ozero(tc_nat),c_Set_Oinsert(c_Suc(c_Suc(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_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),
inference(forward_demodulation,[],[f1430,f27]) ).
fof(f1434,plain,
c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) = c_Set_Oinsert(c_HOL_Ozero__class_Ozero(tc_nat),c_Set_Oinsert(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),c_Set_Oinsert(c_HOL_Oone__class_Oone(tc_nat),c_Set_Oinsert(c_Suc(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)))),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),tc_nat),tc_nat),
inference(forward_demodulation,[],[f1433,f1199]) ).
fof(f1435,plain,
c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) = c_Set_Oinsert(c_HOL_Ozero__class_Ozero(tc_nat),c_Set_Oinsert(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),c_Set_Oinsert(c_Suc(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)))),c_Set_Oinsert(c_HOL_Oone__class_Oone(tc_nat),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),tc_nat),tc_nat),
inference(forward_demodulation,[],[f1434,f27]) ).
fof(f1436,plain,
c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) = c_Set_Oinsert(c_HOL_Ozero__class_Ozero(tc_nat),c_Set_Oinsert(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),c_Set_Oinsert(c_Suc(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)))),c_Set_Oinsert(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),tc_nat),tc_nat),
inference(forward_demodulation,[],[f1435,f1015]) ).
fof(f1437,plain,
c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) = c_Set_Oinsert(c_HOL_Ozero__class_Ozero(tc_nat),c_Set_Oinsert(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),c_Set_Oinsert(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),c_Set_Oinsert(c_Suc(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)))),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),tc_nat),tc_nat),
inference(forward_demodulation,[],[f1436,f27]) ).
fof(f1438,plain,
c_SetInterval_Oord__class_OatLeastLessThan(c_HOL_Ozero__class_Ozero(tc_nat),c_Int_Onumber__class_Onumber__of(c_Int_OBit0(c_Int_OBit0(c_Int_OBit1(c_Int_OPls))),tc_nat),tc_nat) = c_Set_Oinsert(c_HOL_Ozero__class_Ozero(tc_nat),c_Set_Oinsert(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),c_Set_Oinsert(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),c_Set_Oinsert(c_Suc(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)))),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),tc_nat),tc_nat),
inference(forward_demodulation,[],[f1437,f27]) ).
fof(f1439,plain,
~ sP0(c_Finite__Set_Osetsum(v_x,c_Set_Oinsert(c_HOL_Ozero__class_Ozero(tc_nat),c_Set_Oinsert(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)),c_Set_Oinsert(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))),c_Set_Oinsert(c_Suc(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)))),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),tc_nat),tc_nat),tc_nat,t_a)),
inference(backward_demodulation,[],[f1399,f1438]) ).
fof(f1440,plain,
! [X2,X0,X1] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X0),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X1),X2)) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X1),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X0),X2)),
inference(unit_resulting_resolution,[],[f1281,f1307]) ).
fof(f1441,plain,
! [X0,X1] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X0),X1) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X1),X0),
inference(unit_resulting_resolution,[],[f1244,f1307]) ).
fof(f1442,plain,
! [X2,X0,X1] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X0),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X1),X2)) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),X0),X1)),X2),
inference(unit_resulting_resolution,[],[f1283,f1307]) ).
fof(f1443,plain,
sP0(hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_x,c_HOL_Ozero__class_Ozero(tc_nat))),hAPP(v_x,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_x,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))))),hAPP(v_x,c_Suc(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)))))))),
inference(backward_demodulation,[],[f1431,f1442]) ).
fof(f1444,plain,
sP0(hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_x,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_x,c_HOL_Ozero__class_Ozero(tc_nat))),hAPP(v_x,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))))),hAPP(v_x,c_Suc(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)))))))),
inference(forward_demodulation,[],[f1443,f1440]) ).
fof(f1445,plain,
sP0(hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_x,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_x,c_Suc(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)))))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_x,c_HOL_Ozero__class_Ozero(tc_nat))),hAPP(v_x,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))))))),
inference(forward_demodulation,[],[f1444,f1441]) ).
fof(f1446,plain,
sP0(hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_x,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_x,c_HOL_Ozero__class_Ozero(tc_nat))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_x,c_Suc(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)))))),hAPP(v_x,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))))))),
inference(forward_demodulation,[],[f1445,f1440]) ).
fof(f1447,plain,
sP0(hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_x,c_HOL_Ozero__class_Ozero(tc_nat))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_x,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_x,c_Suc(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)))))),hAPP(v_x,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))))))),
inference(forward_demodulation,[],[f1446,f1440]) ).
fof(f1448,plain,
sP0(hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_x,c_HOL_Ozero__class_Ozero(tc_nat))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_x,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_x,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)))),hAPP(v_x,c_Suc(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))))))))),
inference(forward_demodulation,[],[f1447,f1441]) ).
fof(f1449,plain,
sP0(hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_x,c_HOL_Ozero__class_Ozero(tc_nat))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_x,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_x,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))))),hAPP(v_x,c_Suc(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))))))))),
inference(forward_demodulation,[],[f1448,f1440]) ).
fof(f1454,plain,
! [X0] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),c_HOL_Ozero__class_Ozero(t_a)),X0) = X0,
inference(unit_resulting_resolution,[],[f1304,f1307]) ).
fof(f1459,plain,
! [X0,X1] : c_HOL_Ozero__class_Ozero(t_a) = c_Finite__Set_Osetsum(X0,c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)),X1,t_a),
inference(unit_resulting_resolution,[],[f981,f1307]) ).
fof(f1464,plain,
! [X0,X1] : c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(X1,c_Suc(X1),tc_nat),tc_nat,t_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X0,X1)),c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(c_Suc(X1),c_Suc(X1),tc_nat),tc_nat,t_a)),
inference(unit_resulting_resolution,[],[f774,f1307,f170]) ).
fof(f1465,plain,
! [X0,X1] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X0,X1)),c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(c_Suc(X1),c_Suc(X1),tc_nat),tc_nat,t_a)) = c_Finite__Set_Osetsum(X0,c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat,t_a),
inference(forward_demodulation,[],[f1464,f96]) ).
fof(f1482,plain,
! [X0] : c_lessequals(X0,c_Suc(X0),tc_nat),
inference(unit_resulting_resolution,[],[f1064,f170]) ).
fof(f1489,plain,
! [X0,X1] : c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(X1,c_Suc(c_Suc(X1)),tc_nat),tc_nat,t_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(X1,c_Suc(X1),tc_nat),tc_nat,t_a)),c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(c_Suc(X1),c_Suc(c_Suc(X1)),tc_nat),tc_nat,t_a)),
inference(unit_resulting_resolution,[],[f1191,f1307,f1482,f1482]) ).
fof(f1498,plain,
! [X0,X1] : c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(X1,c_Suc(c_Suc(X1)),tc_nat),tc_nat,t_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(X1,c_Suc(X1),tc_nat),tc_nat,t_a)),c_Finite__Set_Osetsum(X0,c_Set_Oinsert(c_Suc(X1),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat,t_a)),
inference(forward_demodulation,[],[f1489,f96]) ).
fof(f1505,plain,
! [X0,X1] : c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(X1,c_Suc(c_Suc(X1)),tc_nat),tc_nat,t_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),c_Finite__Set_Osetsum(X0,c_Set_Oinsert(c_Suc(X1),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat,t_a)),c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(X1,c_Suc(X1),tc_nat),tc_nat,t_a)),
inference(forward_demodulation,[],[f1498,f1441]) ).
fof(f1511,plain,
! [X0,X1] : c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(X1,c_Suc(c_Suc(X1)),tc_nat),tc_nat,t_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),c_Finite__Set_Osetsum(X0,c_Set_Oinsert(c_Suc(X1),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat,t_a)),c_Finite__Set_Osetsum(X0,c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat,t_a)),
inference(forward_demodulation,[],[f1505,f96]) ).
fof(f1516,plain,
! [X0,X1] : c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(X1,c_Suc(c_Suc(X1)),tc_nat),tc_nat,t_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),c_Finite__Set_Osetsum(X0,c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat,t_a)),c_Finite__Set_Osetsum(X0,c_Set_Oinsert(c_Suc(X1),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat,t_a)),
inference(forward_demodulation,[],[f1511,f1441]) ).
fof(f1579,plain,
! [X0] : c_SetInterval_Oord__class_OatLeastLessThan(X0,c_Suc(c_Suc(X0)),tc_nat) = c_Set_Oinsert(c_Suc(X0),c_SetInterval_Oord__class_OatLeastLessThan(X0,c_Suc(X0),tc_nat),tc_nat),
inference(unit_resulting_resolution,[],[f1153,f1482]) ).
fof(f1585,plain,
! [X0] : c_SetInterval_Oord__class_OatLeastLessThan(X0,c_Suc(c_Suc(X0)),tc_nat) = c_Set_Oinsert(c_Suc(X0),c_Set_Oinsert(X0,c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),
inference(forward_demodulation,[],[f1579,f96]) ).
fof(f1586,plain,
! [X0] : c_SetInterval_Oord__class_OatLeastLessThan(X0,c_Suc(c_Suc(X0)),tc_nat) = c_Set_Oinsert(X0,c_Set_Oinsert(c_Suc(X0),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),
inference(forward_demodulation,[],[f1585,f27]) ).
fof(f1588,plain,
! [X0,X1] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),c_Finite__Set_Osetsum(X0,c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat,t_a)),c_Finite__Set_Osetsum(X0,c_Set_Oinsert(c_Suc(X1),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat,t_a)) = c_Finite__Set_Osetsum(X0,c_Set_Oinsert(X1,c_Set_Oinsert(c_Suc(X1),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),tc_nat,t_a),
inference(backward_demodulation,[],[f1516,f1586]) ).
fof(f1620,plain,
! [X0] : ~ c_HOL_Oord__class_Oless(c_Suc(X0),X0,tc_nat),
inference(unit_resulting_resolution,[],[f1064,f1089]) ).
fof(f1621,plain,
! [X0] : c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)) = c_SetInterval_Oord__class_OatLeastLessThan(c_Suc(X0),c_Suc(X0),tc_nat),
inference(unit_resulting_resolution,[],[f177,f1089]) ).
fof(f1627,plain,
! [X0,X1] : c_Finite__Set_Osetsum(X0,c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat,t_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X0,X1)),c_Finite__Set_Osetsum(X0,c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat,t_a)),
inference(backward_demodulation,[],[f1465,f1621]) ).
fof(f1628,plain,
! [X0,X1] : c_Finite__Set_Osetsum(X0,c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat,t_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X0,X1)),c_HOL_Ozero__class_Ozero(t_a)),
inference(forward_demodulation,[],[f1627,f1459]) ).
fof(f1632,plain,
! [X0,X1] : c_Finite__Set_Osetsum(X0,c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat,t_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),c_HOL_Ozero__class_Ozero(t_a)),hAPP(X0,X1)),
inference(forward_demodulation,[],[f1628,f1441]) ).
fof(f1636,plain,
! [X0,X1] : hAPP(X0,X1) = c_Finite__Set_Osetsum(X0,c_Set_Oinsert(X1,c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat,t_a),
inference(forward_demodulation,[],[f1632,f1454]) ).
fof(f1643,plain,
! [X0,X1] : c_Finite__Set_Osetsum(X0,c_Set_Oinsert(X1,c_Set_Oinsert(c_Suc(X1),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),tc_nat,t_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X0,X1)),c_Finite__Set_Osetsum(X0,c_Set_Oinsert(c_Suc(X1),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat,t_a)),
inference(backward_demodulation,[],[f1588,f1636]) ).
fof(f1652,plain,
! [X0,X1] : c_Finite__Set_Osetsum(X0,c_Set_Oinsert(X1,c_Set_Oinsert(c_Suc(X1),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),tc_nat,t_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X0,X1)),hAPP(X0,c_Suc(X1))),
inference(forward_demodulation,[],[f1643,f1636]) ).
fof(f1671,plain,
! [X0] : c_HOL_Oord__class_Oless(X0,c_Suc(c_Suc(X0)),tc_nat),
inference(unit_resulting_resolution,[],[f586,f1620]) ).
fof(f1688,plain,
! [X0] : c_lessequals(X0,c_Suc(c_Suc(X0)),tc_nat),
inference(unit_resulting_resolution,[],[f1064,f1671]) ).
fof(f2206,plain,
! [X0] : c_lessequals(X0,c_Suc(c_Suc(c_Suc(X0))),tc_nat),
inference(unit_resulting_resolution,[],[f1084,f1688]) ).
fof(f2222,plain,
! [X0] : c_SetInterval_Oord__class_OatLeastLessThan(X0,c_Suc(c_Suc(c_Suc(X0))),tc_nat) = c_Set_Oinsert(c_Suc(c_Suc(X0)),c_SetInterval_Oord__class_OatLeastLessThan(X0,c_Suc(c_Suc(X0)),tc_nat),tc_nat),
inference(unit_resulting_resolution,[],[f1153,f1688]) ).
fof(f2231,plain,
! [X0,X1] : c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(X1,c_Suc(c_Suc(c_Suc(c_Suc(X1)))),tc_nat),tc_nat,t_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(X1,c_Suc(c_Suc(X1)),tc_nat),tc_nat,t_a)),c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(c_Suc(c_Suc(X1)),c_Suc(c_Suc(c_Suc(c_Suc(X1)))),tc_nat),tc_nat,t_a)),
inference(unit_resulting_resolution,[],[f1191,f1307,f1688,f1688]) ).
fof(f2270,plain,
! [X0] : c_SetInterval_Oord__class_OatLeastLessThan(X0,c_Suc(c_Suc(c_Suc(X0))),tc_nat) = c_Set_Oinsert(c_Suc(c_Suc(X0)),c_Set_Oinsert(X0,c_Set_Oinsert(c_Suc(X0),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),tc_nat),
inference(forward_demodulation,[],[f2222,f1586]) ).
fof(f2279,plain,
! [X0,X1] : c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(X1,c_Suc(c_Suc(c_Suc(c_Suc(X1)))),tc_nat),tc_nat,t_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(X1,c_Suc(c_Suc(X1)),tc_nat),tc_nat,t_a)),c_Finite__Set_Osetsum(X0,c_Set_Oinsert(c_Suc(c_Suc(X1)),c_Set_Oinsert(c_Suc(c_Suc(c_Suc(X1))),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),tc_nat,t_a)),
inference(forward_demodulation,[],[f2231,f1586]) ).
fof(f2300,plain,
! [X0] : c_SetInterval_Oord__class_OatLeastLessThan(X0,c_Suc(c_Suc(c_Suc(X0))),tc_nat) = c_Set_Oinsert(X0,c_Set_Oinsert(c_Suc(c_Suc(X0)),c_Set_Oinsert(c_Suc(X0),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),tc_nat),
inference(forward_demodulation,[],[f2270,f27]) ).
fof(f2309,plain,
! [X0,X1] : c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(X1,c_Suc(c_Suc(c_Suc(c_Suc(X1)))),tc_nat),tc_nat,t_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),c_Finite__Set_Osetsum(X0,c_Set_Oinsert(c_Suc(c_Suc(X1)),c_Set_Oinsert(c_Suc(c_Suc(c_Suc(X1))),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),tc_nat,t_a)),c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(X1,c_Suc(c_Suc(X1)),tc_nat),tc_nat,t_a)),
inference(forward_demodulation,[],[f2279,f1441]) ).
fof(f2327,plain,
! [X0] : c_SetInterval_Oord__class_OatLeastLessThan(X0,c_Suc(c_Suc(c_Suc(X0))),tc_nat) = c_Set_Oinsert(X0,c_Set_Oinsert(c_Suc(X0),c_Set_Oinsert(c_Suc(c_Suc(X0)),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),tc_nat),
inference(forward_demodulation,[],[f2300,f27]) ).
fof(f2336,plain,
! [X0,X1] : c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(X1,c_Suc(c_Suc(c_Suc(c_Suc(X1)))),tc_nat),tc_nat,t_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),c_Finite__Set_Osetsum(X0,c_Set_Oinsert(c_Suc(c_Suc(X1)),c_Set_Oinsert(c_Suc(c_Suc(c_Suc(X1))),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),tc_nat,t_a)),c_Finite__Set_Osetsum(X0,c_Set_Oinsert(X1,c_Set_Oinsert(c_Suc(X1),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),tc_nat,t_a)),
inference(forward_demodulation,[],[f2309,f1586]) ).
fof(f2360,plain,
! [X0,X1] : c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(X1,c_Suc(c_Suc(c_Suc(c_Suc(X1)))),tc_nat),tc_nat,t_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),c_Finite__Set_Osetsum(X0,c_Set_Oinsert(X1,c_Set_Oinsert(c_Suc(X1),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),tc_nat,t_a)),c_Finite__Set_Osetsum(X0,c_Set_Oinsert(c_Suc(c_Suc(X1)),c_Set_Oinsert(c_Suc(c_Suc(c_Suc(X1))),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),tc_nat,t_a)),
inference(forward_demodulation,[],[f2336,f1441]) ).
fof(f2384,plain,
! [X0,X1] : c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(X1,c_Suc(c_Suc(c_Suc(c_Suc(X1)))),tc_nat),tc_nat,t_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),c_Finite__Set_Osetsum(X0,c_Set_Oinsert(X1,c_Set_Oinsert(c_Suc(X1),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),tc_nat,t_a)),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X0,c_Suc(c_Suc(X1)))),hAPP(X0,c_Suc(c_Suc(c_Suc(X1)))))),
inference(forward_demodulation,[],[f2360,f1652]) ).
fof(f2402,plain,
! [X0,X1] : c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(X1,c_Suc(c_Suc(c_Suc(c_Suc(X1)))),tc_nat),tc_nat,t_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X0,c_Suc(c_Suc(X1)))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),c_Finite__Set_Osetsum(X0,c_Set_Oinsert(X1,c_Set_Oinsert(c_Suc(X1),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),tc_nat,t_a)),hAPP(X0,c_Suc(c_Suc(c_Suc(X1)))))),
inference(forward_demodulation,[],[f2384,f1440]) ).
fof(f2416,plain,
! [X0,X1] : c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(X1,c_Suc(c_Suc(c_Suc(c_Suc(X1)))),tc_nat),tc_nat,t_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X0,c_Suc(c_Suc(X1)))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X0,c_Suc(c_Suc(c_Suc(X1))))),c_Finite__Set_Osetsum(X0,c_Set_Oinsert(X1,c_Set_Oinsert(c_Suc(X1),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),tc_nat,t_a))),
inference(forward_demodulation,[],[f2402,f1441]) ).
fof(f2428,plain,
! [X0,X1] : c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(X1,c_Suc(c_Suc(c_Suc(c_Suc(X1)))),tc_nat),tc_nat,t_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X0,c_Suc(c_Suc(X1)))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X0,c_Suc(c_Suc(c_Suc(X1))))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X0,X1)),hAPP(X0,c_Suc(X1))))),
inference(forward_demodulation,[],[f2416,f1652]) ).
fof(f2440,plain,
! [X0,X1] : c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(X1,c_Suc(c_Suc(c_Suc(c_Suc(X1)))),tc_nat),tc_nat,t_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X0,c_Suc(c_Suc(X1)))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X0,X1)),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X0,c_Suc(c_Suc(c_Suc(X1))))),hAPP(X0,c_Suc(X1))))),
inference(forward_demodulation,[],[f2428,f1440]) ).
fof(f2449,plain,
! [X0,X1] : c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(X1,c_Suc(c_Suc(c_Suc(c_Suc(X1)))),tc_nat),tc_nat,t_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X0,X1)),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X0,c_Suc(c_Suc(X1)))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X0,c_Suc(c_Suc(c_Suc(X1))))),hAPP(X0,c_Suc(X1))))),
inference(forward_demodulation,[],[f2440,f1440]) ).
fof(f2456,plain,
! [X0,X1] : c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(X1,c_Suc(c_Suc(c_Suc(c_Suc(X1)))),tc_nat),tc_nat,t_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X0,X1)),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X0,c_Suc(c_Suc(X1)))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X0,c_Suc(X1))),hAPP(X0,c_Suc(c_Suc(c_Suc(X1))))))),
inference(forward_demodulation,[],[f2449,f1441]) ).
fof(f2462,plain,
! [X0,X1] : c_Finite__Set_Osetsum(X0,c_SetInterval_Oord__class_OatLeastLessThan(X1,c_Suc(c_Suc(c_Suc(c_Suc(X1)))),tc_nat),tc_nat,t_a) = hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X0,X1)),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X0,c_Suc(X1))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X0,c_Suc(c_Suc(X1)))),hAPP(X0,c_Suc(c_Suc(c_Suc(X1))))))),
inference(forward_demodulation,[],[f2456,f1440]) ).
fof(f4436,plain,
! [X0] : c_SetInterval_Oord__class_OatLeastLessThan(X0,c_Suc(c_Suc(c_Suc(c_Suc(X0)))),tc_nat) = c_Set_Oinsert(c_Suc(c_Suc(c_Suc(X0))),c_SetInterval_Oord__class_OatLeastLessThan(X0,c_Suc(c_Suc(c_Suc(X0))),tc_nat),tc_nat),
inference(unit_resulting_resolution,[],[f1153,f2206]) ).
fof(f4548,plain,
! [X0] : c_SetInterval_Oord__class_OatLeastLessThan(X0,c_Suc(c_Suc(c_Suc(c_Suc(X0)))),tc_nat) = c_Set_Oinsert(c_Suc(c_Suc(c_Suc(X0))),c_Set_Oinsert(X0,c_Set_Oinsert(c_Suc(X0),c_Set_Oinsert(c_Suc(c_Suc(X0)),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),tc_nat),tc_nat),
inference(forward_demodulation,[],[f4436,f2327]) ).
fof(f4617,plain,
! [X0] : c_SetInterval_Oord__class_OatLeastLessThan(X0,c_Suc(c_Suc(c_Suc(c_Suc(X0)))),tc_nat) = c_Set_Oinsert(X0,c_Set_Oinsert(c_Suc(c_Suc(c_Suc(X0))),c_Set_Oinsert(c_Suc(X0),c_Set_Oinsert(c_Suc(c_Suc(X0)),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),tc_nat),tc_nat),
inference(forward_demodulation,[],[f4548,f27]) ).
fof(f4686,plain,
! [X0] : c_SetInterval_Oord__class_OatLeastLessThan(X0,c_Suc(c_Suc(c_Suc(c_Suc(X0)))),tc_nat) = c_Set_Oinsert(X0,c_Set_Oinsert(c_Suc(X0),c_Set_Oinsert(c_Suc(c_Suc(c_Suc(X0))),c_Set_Oinsert(c_Suc(c_Suc(X0)),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),tc_nat),tc_nat),
inference(forward_demodulation,[],[f4617,f27]) ).
fof(f4749,plain,
! [X0] : c_SetInterval_Oord__class_OatLeastLessThan(X0,c_Suc(c_Suc(c_Suc(c_Suc(X0)))),tc_nat) = c_Set_Oinsert(X0,c_Set_Oinsert(c_Suc(X0),c_Set_Oinsert(c_Suc(c_Suc(X0)),c_Set_Oinsert(c_Suc(c_Suc(c_Suc(X0))),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),tc_nat),tc_nat),
inference(forward_demodulation,[],[f4686,f27]) ).
fof(f4807,plain,
! [X0,X1] : hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X0,X1)),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X0,c_Suc(X1))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(X0,c_Suc(c_Suc(X1)))),hAPP(X0,c_Suc(c_Suc(c_Suc(X1))))))) = c_Finite__Set_Osetsum(X0,c_Set_Oinsert(X1,c_Set_Oinsert(c_Suc(X1),c_Set_Oinsert(c_Suc(c_Suc(X1)),c_Set_Oinsert(c_Suc(c_Suc(c_Suc(X1))),c_Orderings_Obot__class_Obot(tc_fun(tc_nat,tc_bool)),tc_nat),tc_nat),tc_nat),tc_nat),tc_nat,t_a),
inference(backward_demodulation,[],[f2462,f4749]) ).
fof(f4863,plain,
~ sP0(hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_x,c_HOL_Ozero__class_Ozero(tc_nat))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_x,c_Suc(c_HOL_Ozero__class_Ozero(tc_nat)))),hAPP(hAPP(c_HOL_Oplus__class_Oplus(t_a),hAPP(v_x,c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))))),hAPP(v_x,c_Suc(c_Suc(c_Suc(c_HOL_Ozero__class_Ozero(tc_nat))))))))),
inference(backward_demodulation,[],[f1439,f4807]) ).
fof(f4907,plain,
$false,
inference(forward_subsumption_resolution,[],[f4863,f1449]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV577-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 % Computer : n015.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 11:58:32 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.24 Running first-order theorem proving
% 0.09/0.24 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.32/2.04 % (2576331)Input is clausal, will run a generic CNF schedule.
% 11.32/2.04 % (2576341)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1613647268:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 11.32/2.04 % (2576342)dis-21_1_sil=8000:lcm=predicate:random_seed=3526549382: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)
% 11.32/2.04 % (2576339)lrs+10_1_sil=8000:sp=occurrence:random_seed=1546683492:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 11.32/2.04 % (2576340)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2695975472:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 11.32/2.04 % (2576337)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=459639811:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 11.32/2.04 % (2576336)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=563448014:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 11.32/2.04 % (2576338)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3905423658:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 11.32/2.04 % (2576341)Instruction limit reached!
% 11.32/2.04 % (2576341)------------------------------
% 11.32/2.04 % (2576341)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.32/2.04 % (2576341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.32/2.04 % (2576341)CaDiCaL version: 2.1.3
% 11.32/2.04 % (2576341)Termination reason: Instruction limit
% 11.32/2.04 % (2576341)Termination phase: Saturation
% 11.32/2.04 % (2576341)Time elapsed: 0.052 s
% 11.32/2.04 % (2576341)Peak memory usage: 89 MB
% 11.32/2.04 % (2576341)Instructions burned: 183 (million)
% 11.32/2.04 % (2576342)Instruction limit reached!
% 11.32/2.04 % (2576342)------------------------------
% 11.32/2.04 % (2576342)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.32/2.04 % (2576342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.32/2.04 % (2576342)CaDiCaL version: 2.1.3
% 11.32/2.04 % (2576342)Termination reason: Instruction limit
% 11.32/2.04 % (2576342)Termination phase: Saturation
% 11.32/2.04 % (2576342)Time elapsed: 0.061 s
% 11.32/2.04 % (2576342)Peak memory usage: 89 MB
% 11.32/2.04 % (2576342)Instructions burned: 118 (million)
% 11.32/2.04 % (2576339)Instruction limit reached!
% 11.32/2.04 % (2576339)------------------------------
% 11.32/2.04 % (2576339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.32/2.04 % (2576339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.32/2.04 % (2576339)CaDiCaL version: 2.1.3
% 11.32/2.04 % (2576339)Termination reason: Instruction limit
% 11.32/2.04 % (2576339)Termination phase: Saturation
% 11.32/2.04 % (2576339)Time elapsed: 0.069 s
% 11.32/2.04 % (2576339)Peak memory usage: 89 MB
% 11.32/2.04 % (2576339)Instructions burned: 108 (million)
% 11.32/2.04 % (2576340)Instruction limit reached!
% 11.32/2.04 % (2576340)------------------------------
% 11.32/2.04 % (2576340)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.32/2.04 % (2576340)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.32/2.04 % (2576340)CaDiCaL version: 2.1.3
% 11.32/2.04 % (2576340)Termination reason: Instruction limit
% 11.32/2.04 % (2576340)Termination phase: Saturation
% 11.32/2.04 % (2576340)Time elapsed: 0.075 s
% 11.32/2.04 % (2576340)Peak memory usage: 90 MB
% 11.32/2.04 % (2576340)Instructions burned: 114 (million)
% 11.32/2.04 % (2576350)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=2072807721:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 11.32/2.04 % (2576350)Refutation not found, incomplete strategy
% 11.32/2.04 % (2576350)------------------------------
% 11.32/2.04 % (2576350)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.32/2.04 % (2576350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.32/2.04 % (2576350)CaDiCaL version: 2.1.3
% 11.32/2.04 % (2576350)Termination reason: Refutation not found, incomplete strategy
% 11.32/2.04 % (2576350)Time elapsed: 0.010 s
% 11.32/2.04 % (2576350)Peak memory usage: 89 MB
% 11.32/2.04 % (2576350)Instructions burned: 31 (million)
% 11.32/2.04 % (2576351)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1913246438:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 18.44/3.04 % (2576352)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1595316943:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 18.44/3.04 % (2576353)lrs+10_64_to=lpo:sil=8000:random_seed=1277020283:i=126:bd=preordered_2997 on theBenchmark for (2997ds/126Mi)
% 18.44/3.04 % (2576352)Refutation not found, incomplete strategy
% 18.44/3.04 % (2576352)------------------------------
% 18.44/3.04 % (2576352)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.44/3.04 % (2576352)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.44/3.04 % (2576352)CaDiCaL version: 2.1.3
% 18.44/3.04 % (2576352)Termination reason: Refutation not found, incomplete strategy
% 18.44/3.04 % (2576352)Time elapsed: 0.025 s
% 18.44/3.04 % (2576352)Peak memory usage: 89 MB
% 18.44/3.04 % (2576352)Instructions burned: 44 (million)
% 18.44/3.04 % (2576351)Instruction limit reached!
% 18.44/3.04 % (2576351)------------------------------
% 18.44/3.04 % (2576351)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.44/3.04 % (2576351)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.44/3.04 % (2576351)CaDiCaL version: 2.1.3
% 18.44/3.04 % (2576351)Termination reason: Instruction limit
% 18.44/3.04 % (2576351)Termination phase: Saturation
% 18.44/3.04 % (2576351)Time elapsed: 0.100 s
% 18.44/3.04 % (2576351)Peak memory usage: 91 MB
% 18.44/3.04 % (2576351)Instructions burned: 189 (million)
% 18.44/3.04 % (2576353)Instruction limit reached!
% 18.44/3.04 % (2576353)------------------------------
% 18.44/3.04 % (2576353)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.44/3.04 % (2576353)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.44/3.04 % (2576353)CaDiCaL version: 2.1.3
% 18.44/3.04 % (2576353)Termination reason: Instruction limit
% 18.44/3.04 % (2576353)Termination phase: Saturation
% 18.44/3.04 % (2576353)Time elapsed: 0.077 s
% 18.44/3.04 % (2576353)Peak memory usage: 90 MB
% 18.44/3.04 % (2576353)Instructions burned: 126 (million)
% 18.44/3.04 % (2576350)------------------------------
% 18.44/3.04 % (2576350)------------------------------
% 18.44/3.04 % (2576360)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1330120609:i=3394:sd=4:ss=included:sgt=64_2995 on theBenchmark for (2995ds/3394Mi)
% 18.44/3.04 % (2576359)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2546587245:i=157:gtg=all_2995 on theBenchmark for (2995ds/157Mi)
% 18.44/3.04 % (2576358)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=835231092:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 18.44/3.04 % (2576352)------------------------------
% 18.44/3.04 % (2576352)------------------------------
% 18.44/3.04 % (2576359)Instruction limit reached!
% 18.44/3.04 % (2576359)------------------------------
% 18.44/3.04 % (2576359)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.44/3.04 % (2576359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.44/3.04 % (2576359)CaDiCaL version: 2.1.3
% 18.44/3.04 % (2576359)Termination reason: Instruction limit
% 18.44/3.04 % (2576359)Termination phase: Saturation
% 18.44/3.04 % (2576359)Time elapsed: 0.100 s
% 18.44/3.04 % (2576359)Peak memory usage: 91 MB
% 18.44/3.04 % (2576359)Instructions burned: 157 (million)
% 18.44/3.04 % (2576358)Instruction limit reached!
% 18.44/3.04 % (2576358)------------------------------
% 18.44/3.04 % (2576358)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 18.44/3.04 % (2576358)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.44/3.04 % (2576358)CaDiCaL version: 2.1.3
% 18.44/3.04 % (2576358)Termination reason: Instruction limit
% 18.44/3.04 % (2576358)Termination phase: Saturation
% 18.44/3.04 % (2576358)Time elapsed: 0.124 s
% 18.44/3.04 % (2576358)Peak memory usage: 91 MB
% 18.44/3.04 % (2576358)Instructions burned: 195 (million)
% 18.44/3.04 % (2576364)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=3394385908:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2993 on theBenchmark for (2993ds/106Mi)
% 18.44/3.04 % (2576365)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1789451897:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 29.96/4.71 % (2576364)Instruction limit reached!
% 29.96/4.71 % (2576364)------------------------------
% 29.96/4.71 % (2576364)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.96/4.71 % (2576364)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.96/4.71 % (2576364)CaDiCaL version: 2.1.3
% 29.96/4.71 % (2576364)Termination reason: Instruction limit
% 29.96/4.71 % (2576364)Termination phase: Saturation
% 29.96/4.71 % (2576364)Time elapsed: 0.052 s
% 29.96/4.71 % (2576364)Peak memory usage: 90 MB
% 29.96/4.71 % (2576364)Instructions burned: 108 (million)
% 29.96/4.71 % (2576366)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2071596535:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 29.96/4.71 % (2576365)Instruction limit reached!
% 29.96/4.71 % (2576365)------------------------------
% 29.96/4.71 % (2576365)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.96/4.71 % (2576365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.96/4.71 % (2576365)CaDiCaL version: 2.1.3
% 29.96/4.71 % (2576365)Termination reason: Instruction limit
% 29.96/4.71 % (2576365)Termination phase: Saturation
% 29.96/4.71 % (2576365)Time elapsed: 0.063 s
% 29.96/4.71 % (2576365)Peak memory usage: 90 MB
% 29.96/4.71 % (2576365)Instructions burned: 107 (million)
% 29.96/4.71 % (2576366)Instruction limit reached!
% 29.96/4.71 % (2576366)------------------------------
% 29.96/4.71 % (2576366)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.96/4.71 % (2576366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.96/4.71 % (2576366)CaDiCaL version: 2.1.3
% 29.96/4.71 % (2576366)Termination reason: Instruction limit
% 29.96/4.71 % (2576366)Termination phase: Saturation
% 29.96/4.71 % (2576366)Time elapsed: 0.138 s
% 29.96/4.71 % (2576366)Peak memory usage: 90 MB
% 29.96/4.71 % (2576366)Instructions burned: 242 (million)
% 29.96/4.71 % (2576369)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=3984773429:cond=fast:i=5208:av=off_2991 on theBenchmark for (2991ds/5208Mi)
% 29.96/4.71 % (2576371)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=742213067:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 29.96/4.71 % (2576371)Instruction limit reached!
% 29.96/4.71 % (2576371)------------------------------
% 29.96/4.71 % (2576371)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.96/4.71 % (2576371)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.96/4.71 % (2576371)CaDiCaL version: 2.1.3
% 29.96/4.71 % (2576371)Termination reason: Instruction limit
% 29.96/4.71 % (2576371)Termination phase: Saturation
% 29.96/4.71 % (2576371)Time elapsed: 0.065 s
% 29.96/4.71 % (2576371)Peak memory usage: 90 MB
% 29.96/4.71 % (2576371)Instructions burned: 136 (million)
% 29.96/4.71 % (2576373)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=3193624330:i=499:bd=all_2989 on theBenchmark for (2989ds/499Mi)
% 29.96/4.71 % (2576375)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=4049776802:i=191:fgj=on:bd=all_2988 on theBenchmark for (2988ds/191Mi)
% 29.96/4.71 % (2576375)Instruction limit reached!
% 29.96/4.71 % (2576375)------------------------------
% 29.96/4.71 % (2576375)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.96/4.71 % (2576375)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.96/4.71 % (2576375)CaDiCaL version: 2.1.3
% 29.96/4.71 % (2576375)Termination reason: Instruction limit
% 29.96/4.71 % (2576375)Termination phase: Saturation
% 29.96/4.71 % (2576375)Time elapsed: 0.120 s
% 29.96/4.71 % (2576375)Peak memory usage: 91 MB
% 29.96/4.71 % (2576375)Instructions burned: 192 (million)
% 29.96/4.71 % (2576373)Instruction limit reached!
% 29.96/4.71 % (2576373)------------------------------
% 29.96/4.71 % (2576373)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 29.96/4.71 % (2576373)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 29.96/4.71 % (2576373)CaDiCaL version: 2.1.3
% 29.96/4.71 % (2576373)Termination reason: Instruction limit
% 29.96/4.71 % (2576373)Termination phase: Saturation
% 29.96/4.71 % (2576373)Time elapsed: 0.296 s
% 29.96/4.71 % (2576373)Peak memory usage: 93 MB
% 29.96/4.71 % (2576373)Instructions burned: 499 (million)
% 29.96/4.71 % (2576378)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2433533323:i=264:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/264Mi)
% 52.23/7.83 % (2576379)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=3015617267:cond=on:i=156:bs=on:gtg=exists_all:er=known_2984 on theBenchmark for (2984ds/156Mi)
% 52.23/7.83 % (2576378)Instruction limit reached!
% 52.23/7.83 % (2576378)------------------------------
% 52.23/7.83 % (2576378)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.23/7.83 % (2576378)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.23/7.83 % (2576378)CaDiCaL version: 2.1.3
% 52.23/7.83 % (2576378)Termination reason: Instruction limit
% 52.23/7.83 % (2576378)Termination phase: Saturation
% 52.23/7.83 % (2576378)Time elapsed: 0.159 s
% 52.23/7.83 % (2576378)Peak memory usage: 93 MB
% 52.23/7.83 % (2576378)Instructions burned: 264 (million)
% 52.23/7.83 % (2576379)Instruction limit reached!
% 52.23/7.83 % (2576379)------------------------------
% 52.23/7.83 % (2576379)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.23/7.83 % (2576379)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.23/7.83 % (2576379)CaDiCaL version: 2.1.3
% 52.23/7.83 % (2576379)Termination reason: Instruction limit
% 52.23/7.83 % (2576379)Termination phase: Saturation
% 52.23/7.83 % (2576379)Time elapsed: 0.098 s
% 52.23/7.83 % (2576379)Peak memory usage: 90 MB
% 52.23/7.83 % (2576379)Instructions burned: 157 (million)
% 52.23/7.83 % (2576360)Instruction limit reached!
% 52.23/7.83 % (2576360)------------------------------
% 52.23/7.83 % (2576360)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.23/7.83 % (2576360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.23/7.83 % (2576360)CaDiCaL version: 2.1.3
% 52.23/7.83 % (2576360)Termination reason: Instruction limit
% 52.23/7.83 % (2576360)Termination phase: Saturation
% 52.23/7.83 % (2576360)Time elapsed: 1.192 s
% 52.23/7.83 % (2576360)Peak memory usage: 151 MB
% 52.23/7.83 % (2576360)Instructions burned: 3396 (million)
% 52.23/7.83 % (2576382)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=1450853543:i=3256:kws=precedence:bd=preordered:av=off_2982 on theBenchmark for (2982ds/3256Mi)
% 52.23/7.83 % (2576383)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=3519316878:i=537:av=off:ss=included_2982 on theBenchmark for (2982ds/537Mi)
% 52.23/7.83 % (2576384)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=868013309:i=180:bd=preordered:av=off_2981 on theBenchmark for (2981ds/180Mi)
% 52.23/7.83 % (2576384)Instruction limit reached!
% 52.23/7.83 % (2576384)------------------------------
% 52.23/7.83 % (2576384)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.23/7.83 % (2576384)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.23/7.83 % (2576384)CaDiCaL version: 2.1.3
% 52.23/7.83 % (2576384)Termination reason: Instruction limit
% 52.23/7.83 % (2576384)Termination phase: Saturation
% 52.23/7.83 % (2576384)Time elapsed: 0.057 s
% 52.23/7.83 % (2576384)Peak memory usage: 90 MB
% 52.23/7.83 % (2576384)Instructions burned: 181 (million)
% 52.23/7.83 % (2576388)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=2193547612:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2980 on theBenchmark for (2980ds/10307Mi)
% 52.23/7.83 % (2576383)Instruction limit reached!
% 52.23/7.83 % (2576383)------------------------------
% 52.23/7.83 % (2576383)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.23/7.83 % (2576383)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.23/7.83 % (2576383)CaDiCaL version: 2.1.3
% 52.23/7.83 % (2576383)Termination reason: Instruction limit
% 52.23/7.83 % (2576383)Termination phase: Saturation
% 52.23/7.83 % (2576383)Time elapsed: 0.295 s
% 52.23/7.83 % (2576383)Peak memory usage: 93 MB
% 52.23/7.83 % (2576383)Instructions burned: 538 (million)
% 52.23/7.83 % (2576390)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=4071394073:i=412:gtgl=4:gtg=exists_all_2977 on theBenchmark for (2977ds/412Mi)
% 52.23/7.83 % (2576390)Instruction limit reached!
% 52.23/7.83 % (2576390)------------------------------
% 52.23/7.83 % (2576390)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.23/7.83 % (2576390)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.11/10.09 % (2576390)CaDiCaL version: 2.1.3
% 68.11/10.09 % (2576390)Termination reason: Instruction limit
% 68.11/10.09 % (2576390)Termination phase: Saturation
% 68.11/10.09 % (2576390)Time elapsed: 0.213 s
% 68.11/10.09 % (2576390)Peak memory usage: 92 MB
% 68.11/10.09 % (2576390)Instructions burned: 413 (million)
% 68.11/10.09 % (2576392)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=1393705599:s2pl=no:i=8478:s2at=4:nm=6_2974 on theBenchmark for (2974ds/8478Mi)
% 68.11/10.09 % (2576382)Instruction limit reached!
% 68.11/10.09 % (2576382)------------------------------
% 68.11/10.09 % (2576382)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.11/10.09 % (2576382)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.11/10.09 % (2576382)CaDiCaL version: 2.1.3
% 68.11/10.09 % (2576382)Termination reason: Instruction limit
% 68.11/10.09 % (2576382)Termination phase: Saturation
% 68.11/10.09 % (2576382)Time elapsed: 1.278 s
% 68.11/10.09 % (2576382)Peak memory usage: 149 MB
% 68.11/10.09 % (2576382)Instructions burned: 3258 (million)
% 68.11/10.09 % (2576394)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=617758261:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2968 on theBenchmark for (2968ds/303Mi)
% 68.11/10.09 % (2576394)Instruction limit reached!
% 68.11/10.09 % (2576394)------------------------------
% 68.11/10.09 % (2576394)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.11/10.09 % (2576394)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.11/10.09 % (2576394)CaDiCaL version: 2.1.3
% 68.11/10.09 % (2576394)Termination reason: Instruction limit
% 68.11/10.09 % (2576394)Termination phase: Saturation
% 68.11/10.09 % (2576394)Time elapsed: 0.097 s
% 68.11/10.09 % (2576394)Peak memory usage: 92 MB
% 68.11/10.09 % (2576394)Instructions burned: 306 (million)
% 68.11/10.09 % (2576396)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=2124063168:st=4:i=720:sd=3:fsr=off:ss=axioms_2965 on theBenchmark for (2965ds/720Mi)
% 68.11/10.09 % (2576396)Instruction limit reached!
% 68.11/10.09 % (2576396)------------------------------
% 68.11/10.09 % (2576396)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.11/10.09 % (2576396)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.11/10.09 % (2576396)CaDiCaL version: 2.1.3
% 68.11/10.09 % (2576396)Termination reason: Instruction limit
% 68.11/10.09 % (2576396)Termination phase: Saturation
% 68.11/10.09 % (2576396)Time elapsed: 0.195 s
% 68.11/10.09 % (2576396)Peak memory usage: 95 MB
% 68.11/10.09 % (2576396)Instructions burned: 722 (million)
% 68.11/10.09 % (2576398)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3572558021:i=598:bs=on:bd=preordered:av=off:ss=axioms_2962 on theBenchmark for (2962ds/598Mi)
% 68.11/10.09 % (2576398)Instruction limit reached!
% 68.11/10.09 % (2576398)------------------------------
% 68.11/10.09 % (2576398)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.11/10.09 % (2576398)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.11/10.09 % (2576398)CaDiCaL version: 2.1.3
% 68.11/10.09 % (2576398)Termination reason: Instruction limit
% 68.11/10.09 % (2576398)Termination phase: Saturation
% 68.11/10.09 % (2576398)Time elapsed: 0.187 s
% 68.11/10.09 % (2576398)Peak memory usage: 94 MB
% 68.11/10.09 % (2576398)Instructions burned: 600 (million)
% 68.11/10.09 % (2576369)Instruction limit reached!
% 68.11/10.09 % (2576369)------------------------------
% 68.11/10.09 % (2576369)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 68.11/10.09 % (2576369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 68.11/10.09 % (2576369)CaDiCaL version: 2.1.3
% 68.11/10.09 % (2576369)Termination reason: Instruction limit
% 68.11/10.09 % (2576369)Termination phase: Saturation
% 68.11/10.09 % (2576369)Time elapsed: 3.060 s
% 68.11/10.09 % (2576369)Peak memory usage: 164 MB
% 68.11/10.09 % (2576369)Instructions burned: 5209 (million)
% 68.11/10.09 % (2576400)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1450119522:i=2989:sd=3:ss=axioms:sgt=60_2959 on theBenchmark for (2959ds/2989Mi)
% 68.11/10.09 % (2576401)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=2161868801:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2958 on theBenchmark for (2958ds/1997Mi)
% 95.15/14.02 % (2576400)Instruction limit reached!
% 95.15/14.02 % (2576400)------------------------------
% 95.15/14.02 % (2576400)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.15/14.02 % (2576400)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.15/14.02 % (2576400)CaDiCaL version: 2.1.3
% 95.15/14.02 % (2576400)Termination reason: Instruction limit
% 95.15/14.02 % (2576400)Termination phase: Saturation
% 95.15/14.02 % (2576400)Time elapsed: 0.952 s
% 95.15/14.02 % (2576400)Peak memory usage: 147 MB
% 95.15/14.02 % (2576400)Instructions burned: 2994 (million)
% 95.15/14.02 % (2576404)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=3712390376:i=2088:bd=preordered:av=off_2948 on theBenchmark for (2948ds/2088Mi)
% 95.15/14.02 % (2576401)Instruction limit reached!
% 95.15/14.02 % (2576401)------------------------------
% 95.15/14.02 % (2576401)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.15/14.02 % (2576401)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.15/14.02 % (2576401)CaDiCaL version: 2.1.3
% 95.15/14.02 % (2576401)Termination reason: Instruction limit
% 95.15/14.02 % (2576401)Termination phase: Saturation
% 95.15/14.02 % (2576401)Time elapsed: 1.239 s
% 95.15/14.02 % (2576401)Peak memory usage: 139 MB
% 95.15/14.02 % (2576401)Instructions burned: 1998 (million)
% 95.15/14.02 % (2576406)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=4053545583:i=1098:nicw=on_2944 on theBenchmark for (2944ds/1098Mi)
% 95.15/14.02 % (2576404)Instruction limit reached!
% 95.15/14.02 % (2576404)------------------------------
% 95.15/14.02 % (2576404)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.15/14.02 % (2576404)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.15/14.02 % (2576404)CaDiCaL version: 2.1.3
% 95.15/14.02 % (2576404)Termination reason: Instruction limit
% 95.15/14.02 % (2576404)Termination phase: Saturation
% 95.15/14.02 % (2576404)Time elapsed: 0.686 s
% 95.15/14.02 % (2576404)Peak memory usage: 141 MB
% 95.15/14.02 % (2576404)Instructions burned: 2091 (million)
% 95.15/14.02 % (2576408)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=582214265:i=433:bd=preordered_2940 on theBenchmark for (2940ds/433Mi)
% 95.15/14.02 % (2576408)Instruction limit reached!
% 95.15/14.02 % (2576408)------------------------------
% 95.15/14.02 % (2576408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.15/14.02 % (2576408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.15/14.02 % (2576408)CaDiCaL version: 2.1.3
% 95.15/14.02 % (2576408)Termination reason: Instruction limit
% 95.15/14.02 % (2576408)Termination phase: Saturation
% 95.15/14.02 % (2576408)Time elapsed: 0.135 s
% 95.15/14.02 % (2576408)Peak memory usage: 93 MB
% 95.15/14.02 % (2576408)Instructions burned: 440 (million)
% 95.15/14.02 % (2576406)Instruction limit reached!
% 95.15/14.02 % (2576406)------------------------------
% 95.15/14.02 % (2576406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.15/14.02 % (2576406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.15/14.02 % (2576406)CaDiCaL version: 2.1.3
% 95.15/14.02 % (2576406)Termination reason: Instruction limit
% 95.15/14.02 % (2576406)Termination phase: Saturation
% 95.15/14.02 % (2576406)Time elapsed: 0.665 s
% 95.15/14.02 % (2576406)Peak memory usage: 100 MB
% 95.15/14.02 % (2576406)Instructions burned: 1099 (million)
% 95.15/14.02 % (2576410)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=2787316837:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2937 on theBenchmark for (2937ds/2942Mi)
% 95.15/14.02 % (2576411)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=2552812795:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2936 on theBenchmark for (2936ds/6922Mi)
% 95.15/14.02 % (2576410)Instruction limit reached!
% 95.15/14.02 % (2576410)------------------------------
% 95.15/14.02 % (2576410)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 95.15/14.02 % (2576410)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 95.15/14.02 % (2576410)CaDiCaL version: 2.1.3
% 95.15/14.02 % (2576410)Termination reason: Instruction limit
% 121.87/17.71 % (2576410)Termination phase: Saturation
% 121.87/17.71 % (2576410)Time elapsed: 1.001 s
% 121.87/17.71 % (2576410)Peak memory usage: 145 MB
% 121.87/17.71 % (2576410)Instructions burned: 2944 (million)
% 121.87/17.71 % (2576414)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=1936997565:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2926 on theBenchmark for (2926ds/596Mi)
% 121.87/17.71 % (2576414)Instruction limit reached!
% 121.87/17.71 % (2576414)------------------------------
% 121.87/17.71 % (2576414)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.87/17.71 % (2576414)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.87/17.71 % (2576414)CaDiCaL version: 2.1.3
% 121.87/17.71 % (2576414)Termination reason: Instruction limit
% 121.87/17.71 % (2576414)Termination phase: Saturation
% 121.87/17.71 % (2576414)Time elapsed: 0.167 s
% 121.87/17.71 % (2576414)Peak memory usage: 93 MB
% 121.87/17.71 % (2576414)Instructions burned: 597 (million)
% 121.87/17.71 % (2576416)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=3943831923:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2923 on theBenchmark for (2923ds/4123Mi)
% 121.87/17.71 % (2576388)Instruction limit reached!
% 121.87/17.71 % (2576388)------------------------------
% 121.87/17.71 % (2576388)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.87/17.71 % (2576388)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.87/17.71 % (2576388)CaDiCaL version: 2.1.3
% 121.87/17.71 % (2576388)Termination reason: Instruction limit
% 121.87/17.71 % (2576388)Termination phase: Saturation
% 121.87/17.71 % (2576388)Time elapsed: 6.109 s
% 121.87/17.71 % (2576388)Peak memory usage: 185 MB
% 121.87/17.71 % (2576388)Instructions burned: 10307 (million)
% 121.87/17.71 % (2576392)Instruction limit reached!
% 121.87/17.71 % (2576392)------------------------------
% 121.87/17.71 % (2576392)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.87/17.71 % (2576392)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.87/17.71 % (2576392)CaDiCaL version: 2.1.3
% 121.87/17.71 % (2576392)Termination reason: Instruction limit
% 121.87/17.71 % (2576392)Termination phase: Saturation
% 121.87/17.71 % (2576392)Time elapsed: 5.509 s
% 121.87/17.71 % (2576392)Peak memory usage: 187 MB
% 121.87/17.71 % (2576392)Instructions burned: 8479 (million)
% 121.87/17.71 % (2576418)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=309520139:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2917 on theBenchmark for (2917ds/16411Mi)
% 121.87/17.71 % (2576419)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=1291622091:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2917 on theBenchmark for (2917ds/1670Mi)
% 121.87/17.71 % (2576416)Instruction limit reached!
% 121.87/17.71 % (2576416)------------------------------
% 121.87/17.71 % (2576416)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.87/17.71 % (2576416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.87/17.71 % (2576416)CaDiCaL version: 2.1.3
% 121.87/17.71 % (2576416)Termination reason: Instruction limit
% 121.87/17.71 % (2576416)Termination phase: Saturation
% 121.87/17.71 % (2576416)Time elapsed: 1.397 s
% 121.87/17.71 % (2576416)Peak memory usage: 159 MB
% 121.87/17.71 % (2576416)Instructions burned: 4124 (million)
% 121.87/17.71 % (2576422)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=4132676181:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2907 on theBenchmark for (2907ds/1722Mi)
% 121.87/17.71 % (2576419)Instruction limit reached!
% 121.87/17.71 % (2576419)------------------------------
% 121.87/17.71 % (2576419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.87/17.71 % (2576419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.87/17.71 % (2576419)CaDiCaL version: 2.1.3
% 121.87/17.71 % (2576419)Termination reason: Instruction limit
% 121.87/17.71 % (2576419)Termination phase: Saturation
% 121.87/17.71 % (2576419)Time elapsed: 1.036 s
% 121.87/17.71 % (2576419)Peak memory usage: 139 MB
% 121.87/17.71 % (2576419)Instructions burned: 1672 (million)
% 121.87/17.71 % (2576424)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=1244850185:cts=off:cond=on:i=9530:bs=on:fsd=on_2905 on theBenchmark for (2905ds/9530Mi)
% 75.68/20.05 % (2576422)Instruction limit reached!
% 75.68/20.05 % (2576422)------------------------------
% 75.68/20.05 % (2576422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.68/20.05 % (2576422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.68/20.05 % (2576422)CaDiCaL version: 2.1.3
% 75.68/20.05 % (2576422)Termination reason: Instruction limit
% 75.68/20.05 % (2576422)Termination phase: Saturation
% 75.68/20.05 % (2576422)Time elapsed: 0.614 s
% 75.68/20.05 % (2576422)Peak memory usage: 143 MB
% 75.68/20.05 % (2576422)Instructions burned: 1724 (million)
% 75.68/20.05 % (2576426)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=2380898399:st=2:i=4495:sd=10:ss=included_2900 on theBenchmark for (2900ds/4495Mi)
% 75.68/20.05 % (2576411)Instruction limit reached!
% 75.68/20.05 % (2576411)------------------------------
% 75.68/20.05 % (2576411)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.68/20.05 % (2576411)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.68/20.05 % (2576411)CaDiCaL version: 2.1.3
% 75.68/20.05 % (2576411)Termination reason: Instruction limit
% 75.68/20.05 % (2576411)Termination phase: Saturation
% 75.68/20.05 % (2576411)Time elapsed: 3.882 s
% 75.68/20.05 % (2576411)Peak memory usage: 168 MB
% 75.68/20.05 % (2576411)Instructions burned: 6922 (million)
% 75.68/20.05 % (2576428)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=1735230103:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2895 on theBenchmark for (2895ds/4920Mi)
% 75.68/20.05 % (2576428)Instruction limit reached!
% 75.68/20.05 % (2576428)------------------------------
% 75.68/20.05 % (2576428)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.68/20.05 % (2576428)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.68/20.05 % (2576428)CaDiCaL version: 2.1.3
% 75.68/20.05 % (2576428)Termination reason: Instruction limit
% 75.68/20.05 % (2576428)Termination phase: Saturation
% 75.68/20.05 % (2576428)Time elapsed: 1.632 s
% 75.68/20.05 % (2576428)Peak memory usage: 155 MB
% 75.68/20.05 % (2576428)Instructions burned: 4920 (million)
% 75.68/20.05 % (2576430)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=2455306797:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2878 on theBenchmark for (2878ds/2083Mi)
% 75.68/20.05 % (2576426)Instruction limit reached!
% 75.68/20.05 % (2576426)------------------------------
% 75.68/20.05 % (2576426)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.68/20.05 % (2576426)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.68/20.05 % (2576426)CaDiCaL version: 2.1.3
% 75.68/20.05 % (2576426)Termination reason: Instruction limit
% 75.68/20.05 % (2576426)Termination phase: Saturation
% 75.68/20.05 % (2576426)Time elapsed: 2.377 s
% 75.68/20.05 % (2576426)Peak memory usage: 159 MB
% 75.68/20.05 % (2576426)Instructions burned: 4497 (million)
% 75.68/20.05 % (2576432)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=261400037:i=4629:av=off:gsp=on_2875 on theBenchmark for (2875ds/4629Mi)
% 75.68/20.05 % (2576430)Instruction limit reached!
% 75.68/20.05 % (2576430)------------------------------
% 75.68/20.05 % (2576430)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.68/20.05 % (2576430)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.68/20.05 % (2576430)CaDiCaL version: 2.1.3
% 75.68/20.05 % (2576430)Termination reason: Instruction limit
% 75.68/20.05 % (2576430)Termination phase: Saturation
% 75.68/20.05 % (2576430)Time elapsed: 0.749 s
% 75.68/20.05 % (2576430)Peak memory usage: 139 MB
% 75.68/20.05 % (2576430)Instructions burned: 2084 (million)
% 75.68/20.05 % (2576434)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=594812038:i=1258:av=off_2869 on theBenchmark for (2869ds/1258Mi)
% 75.68/20.05 % (2576434)Instruction limit reached!
% 75.68/20.05 % (2576434)------------------------------
% 75.68/20.05 % (2576434)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.68/20.05 % (2576434)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.68/20.05 % (2576434)CaDiCaL version: 2.1.3
% 75.68/20.05 % (2576434)Termination reason: Instruction limit
% 75.68/20.05 % (2576434)Termination phase: Saturation
% 75.68/20.05 % (2576434)Time elapsed: 0.384 s
% 75.68/20.05 % (2576434)Peak memory usage: 97 MB
% 75.68/20.05 % (2576434)Instructions burned: 1260 (million)
% 75.68/20.05 % (2576436)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=319713963:i=7343:av=off:ss=included_2864 on theBenchmark for (2864ds/7343Mi)
% 75.68/20.05 % (2576432)Instruction limit reached!
% 75.68/20.05 % (2576432)------------------------------
% 75.68/20.05 % (2576432)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.68/20.05 % (2576432)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.68/20.05 % (2576432)CaDiCaL version: 2.1.3
% 75.68/20.05 % (2576432)Termination reason: Instruction limit
% 75.68/20.05 % (2576432)Termination phase: Saturation
% 75.68/20.05 % (2576432)Time elapsed: 2.632 s
% 75.68/20.05 % (2576432)Peak memory usage: 155 MB
% 75.68/20.05 % (2576432)Instructions burned: 4629 (million)
% 75.68/20.05 % (2576438)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=2806165611:i=1325:sd=2:ss=axioms:sgt=16_2847 on theBenchmark for (2847ds/1325Mi)
% 75.68/20.05 % (2576424)Instruction limit reached!
% 75.68/20.05 % (2576424)------------------------------
% 75.68/20.05 % (2576424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.68/20.05 % (2576424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.68/20.05 % (2576424)CaDiCaL version: 2.1.3
% 75.68/20.05 % (2576424)Termination reason: Instruction limit
% 75.68/20.05 % (2576424)Termination phase: Saturation
% 75.68/20.05 % (2576424)Time elapsed: 5.920 s
% 75.68/20.05 % (2576424)Peak memory usage: 179 MB
% 75.68/20.05 % (2576424)Instructions burned: 9532 (million)
% 75.68/20.05 % (2576440)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=1456071536:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2844 on theBenchmark for (2844ds/2646Mi)
% 75.68/20.05 % (2576436)Instruction limit reached!
% 75.68/20.05 % (2576436)------------------------------
% 75.68/20.05 % (2576436)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.68/20.05 % (2576436)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.68/20.05 % (2576436)CaDiCaL version: 2.1.3
% 75.68/20.05 % (2576436)Termination reason: Instruction limit
% 75.68/20.05 % (2576436)Termination phase: Saturation
% 75.68/20.05 % (2576436)Time elapsed: 2.278 s
% 75.68/20.05 % (2576436)Peak memory usage: 182 MB
% 75.68/20.05 % (2576436)Instructions burned: 7345 (million)
% 75.68/20.05 % (2576442)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=3526317655:i=1489:sd=2:ep=R:ss=axioms_2840 on theBenchmark for (2840ds/1489Mi)
% 75.68/20.05 % (2576438)Instruction limit reached!
% 75.68/20.05 % (2576438)------------------------------
% 75.68/20.05 % (2576438)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.68/20.05 % (2576438)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.68/20.05 % (2576438)CaDiCaL version: 2.1.3
% 75.68/20.05 % (2576438)Termination reason: Instruction limit
% 75.68/20.05 % (2576438)Termination phase: Saturation
% 75.68/20.05 % (2576438)Time elapsed: 0.741 s
% 75.68/20.05 % (2576438)Peak memory usage: 96 MB
% 75.68/20.05 % (2576438)Instructions burned: 1326 (million)
% 75.68/20.05 % (2576444)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=759563162:i=1503_2837 on theBenchmark for (2837ds/1503Mi)
% 75.68/20.05 % (2576442)Instruction limit reached!
% 75.68/20.05 % (2576442)------------------------------
% 75.68/20.05 % (2576442)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.68/20.05 % (2576442)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.68/20.05 % (2576442)CaDiCaL version: 2.1.3
% 75.68/20.05 % (2576442)Termination reason: Instruction limit
% 75.68/20.05 % (2576442)Termination phase: Saturation
% 75.68/20.05 % (2576442)Time elapsed: 0.497 s
% 75.68/20.05 % (2576442)Peak memory usage: 133 MB
% 75.68/20.05 % (2576442)Instructions burned: 1491 (million)
% 75.68/20.05 % (2576446)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=3196191139:i=13942:kws=frequency_2833 on theBenchmark for (2833ds/13942Mi)
% 75.68/20.05 % (2576444)Instruction limit reached!
% 75.68/20.05 % (2576444)------------------------------
% 75.68/20.05 % (2576444)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.68/20.05 % (2576444)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.68/20.05 % (2576444)CaDiCaL version: 2.1.3
% 75.68/20.05 % (2576444)Termination reason: Instruction limit
% 75.68/20.05 % (2576444)Termination phase: Saturation
% 75.68/20.05 % (2576444)Time elapsed: 0.884 s
% 75.68/20.05 % (2576444)Peak memory usage: 133 MB
% 75.68/20.05 % (2576444)Instructions burned: 1505 (million)
% 75.68/20.05 % (2576440)Instruction limit reached!
% 75.68/20.05 % (2576440)------------------------------
% 75.68/20.05 % (2576440)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.68/20.05 % (2576440)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.68/20.05 % (2576440)CaDiCaL version: 2.1.3
% 75.68/20.05 % (2576440)Termination reason: Instruction limit
% 75.68/20.05 % (2576440)Termination phase: Saturation
% 75.68/20.05 % (2576440)Time elapsed: 1.690 s
% 75.68/20.05 % (2576440)Peak memory usage: 144 MB
% 75.68/20.05 % (2576440)Instructions burned: 2647 (million)
% 75.68/20.05 % (2576448)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=unary_frequency:spb=goal:lcm=predicate:acc=on:urr=full:bce=on:bsr=unit_only:s2agt=64:sac=on:random_seed=2022942692:i=3604:fsr=off:er=filter_2827 on theBenchmark for (2827ds/3604Mi)
% 75.68/20.05 % (2576450)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=2161875886:i=1876:sd=1:ss=included:sgt=32_2825 on theBenchmark for (2825ds/1876Mi)
% 75.68/20.05 % (2576418)Instruction limit reached!
% 75.68/20.05 % (2576418)------------------------------
% 75.68/20.05 % (2576418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.68/20.05 % (2576418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.68/20.05 % (2576418)CaDiCaL version: 2.1.3
% 75.68/20.05 % (2576418)Termination reason: Instruction limit
% 75.68/20.05 % (2576418)Termination phase: Saturation
% 75.68/20.05 % (2576418)Time elapsed: 9.852 s
% 75.68/20.05 % (2576418)Peak memory usage: 187 MB
% 75.68/20.05 % (2576418)Instructions burned: 16411 (million)
% 75.68/20.05 % (2576452)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=2714566497:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2817 on theBenchmark for (2817ds/1932Mi)
% 75.68/20.05 % (2576450)Instruction limit reached!
% 75.68/20.05 % (2576450)------------------------------
% 75.68/20.05 % (2576450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.68/20.05 % (2576450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.68/20.05 % (2576450)CaDiCaL version: 2.1.3
% 75.68/20.05 % (2576450)Termination reason: Instruction limit
% 75.68/20.05 % (2576450)Termination phase: Saturation
% 75.68/20.05 % (2576450)Time elapsed: 1.146 s
% 75.68/20.05 % (2576450)Peak memory usage: 139 MB
% 75.68/20.05 % (2576450)Instructions burned: 1878 (million)
% 75.68/20.05 % (2576454)dis-1010_1_ncem=casc2026/models/loop1.pt:sil=8000:npcc=on:fde=unused:etr=on:sp=weighted_frequency:spb=goal_then_units:urr=ec_only:fd=preordered:kmz=on:random_seed=2573856341:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2812 on theBenchmark for (2812ds/1980Mi)
% 75.68/20.05 % (2576452)First to succeed.
% 75.68/20.05 % (2576452)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2576331"
% 75.68/20.05 % (2576448)Instruction limit reached!
% 75.68/20.05 % (2576448)------------------------------
% 75.68/20.05 % (2576448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 75.68/20.05 % (2576448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 75.68/20.05 % (2576448)CaDiCaL version: 2.1.3
% 75.68/20.05 % (2576448)Termination reason: Instruction limit
% 75.68/20.05 % (2576448)Termination phase: Saturation
% 75.68/20.05 % (2576448)Time elapsed: 1.978 s
% 75.68/20.05 % (2576448)Peak memory usage: 141 MB
% 75.68/20.05 % (2576448)Instructions burned: 3606 (million)
% 75.68/20.05 % (2576452)Refutation found. Thanks to Tanya!
% 75.68/20.05 % SZS status Unsatisfiable for theBenchmark
% 75.68/20.05 % SZS output start Proof for theBenchmark
% See solution above
% 139.19/20.25 % (2576452)------------------------------
% 139.19/20.25 % (2576452)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 139.19/20.25 % (2576452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 139.19/20.25 % (2576452)CaDiCaL version: 2.1.3
% 139.19/20.25 % (2576452)Termination reason: Refutation
% 139.19/20.25 % (2576452)Time elapsed: 0.876 s
% 139.19/20.25 % (2576452)Peak memory usage: 134 MB
% 139.19/20.25 % (2576452)Instructions burned: 1384 (million)
% 139.19/20.25 % (2576452)------------------------------
% 139.19/20.25 % (2576452)------------------------------
% 139.19/20.25 % (2576331)Success in time 19.61 s
% 139.19/20.25 % Vampire exiting
%------------------------------------------------------------------------------