%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWV282-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:20:43 PM UTC 2026
% Result : Unsatisfiable 41.82s 12.24s
% Output : Refutation 41.82s
% Verified :
% SZS Type : Refutation
% Derivation depth : 64
% Number of leaves : 60
% Syntax : Number of formulae : 276 ( 103 unt; 0 def)
% Number of atoms : 538 ( 385 equ)
% Maximal formula atoms : 6 ( 1 avg)
% Number of connectives : 355 ( 93 ~; 262 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 9 ( 7 usr; 1 prp; 0-3 aty)
% Number of functors : 27 ( 27 usr; 9 con; 0-3 aty)
% Number of variables : 300 ( 300 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f79,axiom,
! [X0] : c_less(X0,c_Suc(X0),tc_nat),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-0.ax',cls_Nat_OlessI_0) ).
fof(f81,axiom,
! [X0] : c_less(c_0,c_Suc(X0),tc_nat),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-0.ax',cls_Nat_Ozero__less__Suc_0) ).
fof(f82,axiom,
! [X0,X1] :
( ~ class_Orderings_Oorder(X0)
| c_lessequals(X1,X1,X0) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-0.ax',cls_Orderings_Oorder__class_Oaxioms__1_0) ).
fof(f155,axiom,
class_OrderedGroup_Ocomm__monoid__add(tc_IntDef_Oint),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-0.ax',clsarity_IntDef__Oint_12) ).
fof(f176,axiom,
class_Orderings_Oorder(tc_IntDef_Oint),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-0.ax',clsarity_IntDef__Oint_31) ).
fof(f236,axiom,
class_OrderedGroup_Omonoid__mult(tc_nat),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-0.ax',clsarity_nat_23) ).
fof(f243,axiom,
class_Orderings_Oorder(tc_nat),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-0.ax',clsarity_nat_3) ).
fof(f1264,axiom,
! [X0] : c_div(X0,c_Suc(c_0),tc_nat) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_Divides_Odiv__1_0) ).
fof(f1265,axiom,
! [X0,X1] : c_lessequals(c_div(X0,X1,tc_nat),X0,tc_nat),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_Divides_Odiv__le__dividend_0) ).
fof(f1272,axiom,
! [X2,X0,X1] :
( ~ c_less(c_0,X0,tc_nat)
| c_div(c_plus(X1,c_times(X2,X0,tc_nat),tc_nat),X0,tc_nat) = c_plus(X2,c_div(X1,X0,tc_nat),tc_nat) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_Divides_Odiv__mult__self1_0) ).
fof(f1273,axiom,
! [X0,X1] :
( ~ c_less(c_0,X0,tc_nat)
| c_div(c_times(X0,X1,tc_nat),X0,tc_nat) = X1 ),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_Divides_Odiv__mult__self1__is__m_0) ).
fof(f1277,axiom,
! [X0] :
( ~ c_less(c_0,X0,tc_nat)
| c_div(X0,X0,tc_nat) = c_1 ),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_Divides_Odiv__self_0) ).
fof(f1278,plain,
! [X0] :
( ~ c_less(c_0,X0,tc_nat)
| c_1 = c_div(X0,X0,tc_nat) ),
inference(reorient_equations,[],[f1277]) ).
fof(f1462,axiom,
! [X0] :
( ~ c_less(c_HOL_Oabs(X0,tc_IntDef_Oint),c_1,tc_IntDef_Oint)
| X0 = c_0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_IntArith_Ozabs__less__one__iff_0) ).
fof(f1463,plain,
! [X0] :
( ~ c_less(c_HOL_Oabs(X0,tc_IntDef_Oint),c_1,tc_IntDef_Oint)
| c_0 = X0 ),
inference(reorient_equations,[],[f1462]) ).
fof(f1482,axiom,
! [X0] : c_HOL_Oabs(c_IntDef_Oint(X0),tc_IntDef_Oint) = c_IntDef_Oint(X0),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_IntDef_Oabs__int__eq_0) ).
fof(f1483,plain,
! [X0] : c_IntDef_Oint(X0) = c_HOL_Oabs(c_IntDef_Oint(X0),tc_IntDef_Oint),
inference(reorient_equations,[],[f1482]) ).
fof(f1487,axiom,
c_IntDef_Oint(c_1) = c_1,
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_IntDef_Oint__1_0) ).
fof(f1488,plain,
c_1 = c_IntDef_Oint(c_1),
inference(reorient_equations,[],[f1487]) ).
fof(f1489,axiom,
! [X0] : c_IntDef_Oint(c_Suc(X0)) = c_plus(c_1,c_IntDef_Oint(X0),tc_IntDef_Oint),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_IntDef_Oint__Suc_0) ).
fof(f1492,axiom,
c_IntDef_Oint(c_0) = c_0,
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_IntDef_Oint__eq__0__conv_1) ).
fof(f1493,plain,
c_0 = c_IntDef_Oint(c_0),
inference(reorient_equations,[],[f1492]) ).
fof(f1505,axiom,
! [X0] : c_IntDef_Onat(c_IntDef_Oint(X0)) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_IntDef_Onat__int_0) ).
fof(f1556,axiom,
! [X0,X1] :
( ~ c_lessequals(c_IntDef_Oint(X0),c_IntDef_Oint(X1),tc_IntDef_Oint)
| c_lessequals(X0,X1,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_IntDef_Ozle__int_0) ).
fof(f1559,axiom,
! [X0,X1] :
( c_less(c_IntDef_Oint(X0),c_IntDef_Oint(X1),tc_IntDef_Oint)
| ~ c_less(X0,X1,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_IntDef_Ozless__int_1) ).
fof(f1745,axiom,
! [X0,X1] : c_List_Odrop(X0,c_List_Olist_ONil,X1) = c_List_Olist_ONil,
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_List_Odrop_Odrop__Nil_0) ).
fof(f1746,plain,
! [X0,X1] : c_List_Olist_ONil = c_List_Odrop(X0,c_List_Olist_ONil,X1),
inference(reorient_equations,[],[f1745]) ).
fof(f1760,axiom,
! [X2,X0,X1] : c_List_Odrop(X0,c_List_Oupt(X1,X2),tc_nat) = c_List_Oupt(c_plus(X1,X0,tc_nat),X2),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_List_Odrop__upt_0) ).
fof(f1790,axiom,
! [X0] : c_Nat_Osize(c_List_Olist_ONil,tc_List_Olist(X0)) = c_0,
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_List_Olength__0__conv_1) ).
fof(f1791,plain,
! [X0] : c_0 = c_Nat_Osize(c_List_Olist_ONil,tc_List_Olist(X0)),
inference(reorient_equations,[],[f1790]) ).
fof(f1811,axiom,
! [X0,X1] : c_Nat_Osize(c_List_Oupt(X0,X1),tc_List_Olist(tc_nat)) = c_minus(X1,X0,tc_nat),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_List_Olength__upt_0) ).
fof(f1812,plain,
! [X0,X1] : c_minus(X1,X0,tc_nat) = c_Nat_Osize(c_List_Oupt(X0,X1),tc_List_Olist(tc_nat)),
inference(reorient_equations,[],[f1811]) ).
fof(f2059,axiom,
! [X0,X1] :
( ~ c_lessequals(X0,X1,tc_nat)
| c_List_Oupt(X1,X0) = c_List_Olist_ONil ),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_List_Oupt__eq__Nil__conv_2) ).
fof(f2060,plain,
! [X0,X1] :
( ~ c_lessequals(X0,X1,tc_nat)
| c_List_Olist_ONil = c_List_Oupt(X1,X0) ),
inference(reorient_equations,[],[f2059]) ).
fof(f2073,axiom,
! [X2,X0,X1] :
( ~ c_lessequals(X0,X1,tc_nat)
| c_plus(c_minus(X1,X0,tc_nat),X2,tc_nat) = c_minus(c_plus(X1,X2,tc_nat),X0,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_NatArith_Oadd__diff__assoc2_0) ).
fof(f2074,axiom,
! [X2,X0,X1] :
( ~ c_lessequals(X0,X1,tc_nat)
| c_plus(X2,c_minus(X1,X0,tc_nat),tc_nat) = c_minus(c_plus(X2,X1,tc_nat),X0,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_NatArith_Oadd__diff__assoc_0) ).
fof(f2079,axiom,
! [X0,X1] :
( ~ c_less(c_0,X1,tc_nat)
| ~ c_less(c_0,X0,tc_nat)
| c_less(c_minus(X0,X1,tc_nat),X0,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_NatArith_Odiff__less_0) ).
fof(f2144,axiom,
! [X0,X1] : c_IntDef_Oint(c_plus(X0,X1,tc_nat)) = c_plus(c_IntDef_Oint(X0),c_IntDef_Oint(X1),tc_IntDef_Oint),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_NatBin_Oint_A_Im2_A_L_An2_J_A_61_61_Aint_Am2_A_L_Aint_An2_0) ).
fof(f2349,axiom,
! [X0] : c_0 != c_Suc(X0),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_Nat_OZero__not__Suc_0) ).
fof(f2350,axiom,
! [X0] : c_plus(X0,c_0,tc_nat) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_Nat_Oadd__0__right_0) ).
fof(f2351,axiom,
! [X0,X1] : c_plus(X0,c_Suc(X1),tc_nat) = c_Suc(c_plus(X0,X1,tc_nat)),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_Nat_Oadd__Suc__right_0) ).
fof(f2361,axiom,
! [X0] : c_minus(c_0,X0,tc_nat) = c_0,
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_Nat_Odiff__0__eq__0_0) ).
fof(f2362,plain,
! [X0] : c_0 = c_minus(c_0,X0,tc_nat),
inference(reorient_equations,[],[f2361]) ).
fof(f2363,axiom,
! [X0,X1] : c_minus(c_Suc(X0),c_Suc(X1),tc_nat) = c_minus(X0,X1,tc_nat),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_Nat_Odiff__Suc__Suc_0) ).
fof(f2364,plain,
! [X0,X1] : c_minus(X0,X1,tc_nat) = c_minus(c_Suc(X0),c_Suc(X1),tc_nat),
inference(reorient_equations,[],[f2363]) ).
fof(f2366,axiom,
! [X2,X0,X1] : c_minus(c_minus(X0,X1,tc_nat),X2,tc_nat) = c_minus(X0,c_plus(X1,X2,tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_Nat_Odiff__diff__left_0) ).
fof(f2367,axiom,
! [X0,X1] :
( c_minus(X0,X1,tc_nat) != c_0
| c_lessequals(X0,X1,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_Nat_Odiff__is__0__eq_0) ).
fof(f2368,plain,
! [X0,X1] :
( c_0 != c_minus(X0,X1,tc_nat)
| c_lessequals(X0,X1,tc_nat) ),
inference(reorient_equations,[],[f2367]) ).
fof(f2369,axiom,
! [X0,X1] :
( ~ c_lessequals(X0,X1,tc_nat)
| c_minus(X0,X1,tc_nat) = c_0 ),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_Nat_Odiff__is__0__eq_H_0) ).
fof(f2370,plain,
! [X0,X1] :
( ~ c_lessequals(X0,X1,tc_nat)
| c_0 = c_minus(X0,X1,tc_nat) ),
inference(reorient_equations,[],[f2369]) ).
fof(f2372,axiom,
! [X0] : c_minus(X0,X0,tc_nat) = c_0,
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_Nat_Odiff__self__eq__0_0) ).
fof(f2373,plain,
! [X0] : c_0 = c_minus(X0,X0,tc_nat),
inference(reorient_equations,[],[f2372]) ).
fof(f2378,axiom,
! [X0,X1] :
( ~ c_lessequals(X0,X1,tc_nat)
| c_plus(X0,c_minus(X1,X0,tc_nat),tc_nat) = X1 ),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_Nat_Ole__add__diff__inverse_0) ).
fof(f2384,axiom,
c_less(c_0,c_1,tc_nat),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_Nat_Oless__one_1) ).
fof(f2425,axiom,
! [X2,X0,X1] :
( c_plus(X0,X1,tc_nat) != c_plus(X0,X2,tc_nat)
| X1 = X2 ),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_Nat_Onat__add__left__cancel_0) ).
fof(f2430,axiom,
! [X2,X0,X1] :
( c_plus(X0,X1,tc_nat) != c_plus(X2,X1,tc_nat)
| X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_Nat_Onat__add__right__cancel_0) ).
fof(f2432,axiom,
! [X0,X1] : ~ c_less(c_plus(X0,X1,tc_nat),X1,tc_nat),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_Nat_Onot__add__less2_0) ).
fof(f2436,axiom,
! [X0] : ~ c_less(X0,c_0,tc_nat),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_Nat_Onot__less0_0) ).
fof(f2441,axiom,
c_Suc(c_0) = c_times(c_1,c_1,tc_nat),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_Nat_Oone__eq__mult__iff_2) ).
fof(f2448,axiom,
! [X0] : c_plus(c_0,X0,tc_nat) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_Nat_Oop_A_L_Oadd__0_0) ).
fof(f2449,axiom,
! [X0,X1] : c_plus(c_Suc(X0),X1,tc_nat) = c_Suc(c_plus(X0,X1,tc_nat)),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_Nat_Oop_A_L_Oadd__Suc_0) ).
fof(f2450,plain,
! [X0,X1] : c_Suc(c_plus(X0,X1,tc_nat)) = c_plus(c_Suc(X0),X1,tc_nat),
inference(reorient_equations,[],[f2449]) ).
fof(f2451,axiom,
! [X0] : c_minus(X0,c_0,tc_nat) = X0,
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_Nat_Oop_A_N_Odiff__0_0) ).
fof(f2453,axiom,
! [X0,X1] :
( c_less(c_0,c_minus(X1,X0,tc_nat),tc_nat)
| ~ c_less(X0,X1,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_Nat_Ozero__less__diff_1) ).
fof(f2566,axiom,
! [X0,X1] :
( ~ class_OrderedGroup_Ocomm__monoid__add(X0)
| c_plus(X1,c_0,X0) = X1 ),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_OrderedGroup_Oadd__0__right_0) ).
fof(f2608,axiom,
! [X0,X1] :
( ~ class_OrderedGroup_Omonoid__mult(X0)
| c_times(X1,c_1,X0) = X1 ),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_OrderedGroup_Omonoid__mult__class_Oaxioms__2_0) ).
fof(f2680,axiom,
! [X0] :
( ~ c_Parity_Oeven(X0,tc_nat)
| ~ c_Parity_Oeven(c_Suc(X0),tc_nat) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_Parity_Oeven__nat__Suc_0) ).
fof(f2681,axiom,
! [X0] :
( c_Parity_Oeven(X0,tc_nat)
| c_Parity_Oeven(c_Suc(X0),tc_nat) ),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_Parity_Oeven__nat__Suc_1) ).
fof(f3054,axiom,
! [X0] : c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat) = c_Suc(X0),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_SetInterval_Ocard__atMost_0) ).
fof(f3055,plain,
! [X0] : c_Suc(X0) = c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat),
inference(reorient_equations,[],[f3054]) ).
fof(f3060,axiom,
! [X0,X1] : c_Finite__Set_Ocard(c_SetInterval_OgreaterThanLessThan(X0,X1,tc_nat),tc_nat) = c_minus(X1,c_Suc(X0),tc_nat),
file('/export/starexec/sandbox2/benchmark/Axioms/MSC001-1.ax',cls_SetInterval_Ocard__greaterThanLessThan_0) ).
fof(f3558,axiom,
! [X0,X1] : c_lessequals(X0,c_plus(X0,X1,tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Nat_Ole__add1_0) ).
fof(f3559,axiom,
! [X0,X1] : c_lessequals(X0,c_plus(X1,X0,tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Nat_Ole__add2_0) ).
fof(f3561,axiom,
! [X0,X1] :
( ~ c_lessequals(X0,X1,tc_nat)
| c_less(X0,c_Suc(X1),tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Nat_Oless__Suc__eq__le_1) ).
fof(f3562,axiom,
! [X0,X1] :
( ~ c_in(c_Message_Omsg_ONonce(X0),c_Event_Oused(X1),tc_Message_Omsg)
| ~ c_lessequals(v_sko__urX(X1),X0,tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Public_ONonce__supply__lemma_0) ).
fof(f3563,negated_conjecture,
! [X2,X0,X1] :
( X0 = X1
| X2 = X1
| X0 = X2
| c_in(c_Message_Omsg_ONonce(X1),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)
| c_in(c_Message_Omsg_ONonce(X2),c_Event_Oused(v_evs_H),tc_Message_Omsg)
| c_in(c_Message_Omsg_ONonce(X0),c_Event_Oused(v_evs),tc_Message_Omsg) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f3564,plain,
! [X2,X0,X1] :
( c_in(c_Message_Omsg_ONonce(X2),c_Event_Oused(v_evs_H),tc_Message_Omsg)
| c_in(c_Message_Omsg_ONonce(X1),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)
| c_in(c_Message_Omsg_ONonce(X0),c_Event_Oused(v_evs),tc_Message_Omsg)
| X0 = X2
| X1 = X2
| X0 = X1 ),
inference(reorient_equations,[],[f3563]) ).
fof(f3569,plain,
! [X0] : c_less(X0,c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat),tc_nat),
inference(definition_unfolding,[],[f79,f3055]) ).
fof(f3570,plain,
! [X0] : c_less(c_0,c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat),tc_nat),
inference(definition_unfolding,[],[f81,f3055]) ).
fof(f3586,plain,
! [X0] : c_div(X0,c_Finite__Set_Ocard(c_SetInterval_OatMost(c_0,tc_nat),tc_nat),tc_nat) = X0,
inference(definition_unfolding,[],[f1264,f3055]) ).
fof(f3622,plain,
! [X0] : c_plus(c_1,c_IntDef_Oint(X0),tc_IntDef_Oint) = c_IntDef_Oint(c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat)),
inference(definition_unfolding,[],[f1489,f3055]) ).
fof(f3691,plain,
! [X0] : c_0 != c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat),
inference(definition_unfolding,[],[f2349,f3055]) ).
fof(f3692,plain,
! [X0,X1] : c_plus(X0,c_Finite__Set_Ocard(c_SetInterval_OatMost(X1,tc_nat),tc_nat),tc_nat) = c_Finite__Set_Ocard(c_SetInterval_OatMost(c_plus(X0,X1,tc_nat),tc_nat),tc_nat),
inference(definition_unfolding,[],[f2351,f3055,f3055]) ).
fof(f3693,plain,
! [X0,X1] : c_minus(X0,X1,tc_nat) = c_minus(c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat),c_Finite__Set_Ocard(c_SetInterval_OatMost(X1,tc_nat),tc_nat),tc_nat),
inference(definition_unfolding,[],[f2364,f3055,f3055]) ).
fof(f3705,plain,
c_times(c_1,c_1,tc_nat) = c_Finite__Set_Ocard(c_SetInterval_OatMost(c_0,tc_nat),tc_nat),
inference(definition_unfolding,[],[f2441,f3055]) ).
fof(f3710,plain,
! [X0,X1] : c_Finite__Set_Ocard(c_SetInterval_OatMost(c_plus(X0,X1,tc_nat),tc_nat),tc_nat) = c_plus(c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat),X1,tc_nat),
inference(definition_unfolding,[],[f2450,f3055,f3055]) ).
fof(f3730,plain,
! [X0] :
( ~ c_Parity_Oeven(c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat),tc_nat)
| ~ c_Parity_Oeven(X0,tc_nat) ),
inference(definition_unfolding,[],[f2680,f3055]) ).
fof(f3731,plain,
! [X0] :
( c_Parity_Oeven(c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat),tc_nat)
| c_Parity_Oeven(X0,tc_nat) ),
inference(definition_unfolding,[],[f2681,f3055]) ).
fof(f3738,plain,
! [X0,X1] : c_Finite__Set_Ocard(c_SetInterval_OgreaterThanLessThan(X0,X1,tc_nat),tc_nat) = c_minus(X1,c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat),tc_nat),
inference(definition_unfolding,[],[f3060,f3055]) ).
fof(f3819,plain,
! [X0,X1] :
( c_less(X0,c_Finite__Set_Ocard(c_SetInterval_OatMost(X1,tc_nat),tc_nat),tc_nat)
| ~ c_lessequals(X0,X1,tc_nat) ),
inference(definition_unfolding,[],[f3561,f3055]) ).
fof(f3842,plain,
! [X0,X1] : c_minus(X0,X1,tc_nat) = c_Finite__Set_Ocard(c_SetInterval_OgreaterThanLessThan(X1,c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat),tc_nat),tc_nat),
inference(forward_demodulation,[],[f3693,f3738]) ).
fof(f3917,plain,
! [X0] : c_div(X0,c_times(c_1,c_1,tc_nat),tc_nat) = X0,
inference(forward_demodulation,[],[f3586,f3705]) ).
fof(f4718,plain,
! [X0] : c_lessequals(X0,X0,tc_IntDef_Oint),
inference(resolution,[],[f82,f176]) ).
fof(f4719,plain,
! [X0] : c_lessequals(X0,X0,tc_nat),
inference(resolution,[],[f82,f243]) ).
fof(f4901,plain,
! [X0] : c_plus(X0,c_0,tc_IntDef_Oint) = X0,
inference(resolution,[],[f2566,f155]) ).
fof(f4913,plain,
! [X0] : c_times(X0,c_1,tc_nat) = X0,
inference(resolution,[],[f2608,f236]) ).
fof(f5016,plain,
! [X0] :
( ~ c_less(c_IntDef_Oint(X0),c_1,tc_IntDef_Oint)
| c_0 = c_IntDef_Oint(X0) ),
inference(superposition,[],[f1463,f1483]) ).
fof(f5143,plain,
! [X0,X1] : c_List_Olist_ONil = c_List_Oupt(c_plus(X0,X1,tc_nat),X0),
inference(resolution,[],[f2060,f3558]) ).
fof(f5144,plain,
! [X0,X1] : c_List_Olist_ONil = c_List_Oupt(c_plus(X0,X1,tc_nat),X1),
inference(resolution,[],[f2060,f3559]) ).
fof(f5300,plain,
! [X0] : c_div(X0,c_1,tc_nat) = X0,
inference(superposition,[],[f3917,f4913]) ).
fof(f5431,plain,
! [X0] :
( ~ c_lessequals(c_IntDef_Oint(X0),c_0,tc_IntDef_Oint)
| c_lessequals(X0,c_0,tc_nat) ),
inference(superposition,[],[f1556,f1493]) ).
fof(f5452,plain,
! [X0] :
( c_less(c_IntDef_Oint(X0),c_1,tc_IntDef_Oint)
| ~ c_less(X0,c_1,tc_nat) ),
inference(superposition,[],[f1559,f1488]) ).
fof(f5622,plain,
! [X0,X1] : c_0 = c_minus(X0,c_plus(X1,X0,tc_nat),tc_nat),
inference(resolution,[],[f2370,f3559]) ).
fof(f5628,plain,
! [X0,X1] : c_0 = c_minus(c_div(X0,X1,tc_nat),X0,tc_nat),
inference(resolution,[],[f2370,f1265]) ).
fof(f5692,plain,
! [X0] :
( ~ c_less(X0,c_1,tc_nat)
| c_0 = c_IntDef_Oint(X0) ),
inference(resolution,[],[f5452,f5016]) ).
fof(f6418,plain,
! [X0,X1] :
( c_less(c_0,c_0,tc_nat)
| ~ c_less(X0,c_div(X0,X1,tc_nat),tc_nat) ),
inference(superposition,[],[f2453,f5628]) ).
fof(f6422,plain,
! [X0,X1] : ~ c_less(X0,c_div(X0,X1,tc_nat),tc_nat),
inference(forward_subsumption_resolution,[],[f6418,f2436]) ).
fof(f6799,plain,
! [X2,X0,X1] :
( ~ c_lessequals(v_sko__urX(v_evs_H),X0,tc_nat)
| c_in(c_Message_Omsg_ONonce(X1),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)
| c_in(c_Message_Omsg_ONonce(X2),c_Event_Oused(v_evs),tc_Message_Omsg)
| X0 = X2
| X0 = X1
| X1 = X2 ),
inference(resolution,[],[f3562,f3564]) ).
fof(f6803,plain,
! [X0,X1] :
( c_in(c_Message_Omsg_ONonce(X1),c_Event_Oused(v_evs),tc_Message_Omsg)
| c_in(c_Message_Omsg_ONonce(X0),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)
| v_sko__urX(v_evs_H) = X1
| v_sko__urX(v_evs_H) = X0
| X0 = X1 ),
inference(resolution,[],[f6799,f4719]) ).
fof(f6814,plain,
! [X0,X1] :
( ~ c_lessequals(v_sko__urX(v_evs),X0,tc_nat)
| v_sko__urX(v_evs_H) = X0
| v_sko__urX(v_evs_H) = X1
| X0 = X1
| c_in(c_Message_Omsg_ONonce(X1),c_Event_Oused(v_evs_H_H),tc_Message_Omsg) ),
inference(resolution,[],[f6803,f3562]) ).
fof(f6815,plain,
! [X0,X1] :
( ~ c_lessequals(v_sko__urX(v_evs_H_H),X0,tc_nat)
| v_sko__urX(v_evs_H) = X1
| v_sko__urX(v_evs_H) = X0
| X0 = X1
| c_in(c_Message_Omsg_ONonce(X1),c_Event_Oused(v_evs),tc_Message_Omsg) ),
inference(resolution,[],[f6803,f3562]) ).
fof(f6819,plain,
! [X0] :
( c_in(c_Message_Omsg_ONonce(X0),c_Event_Oused(v_evs_H_H),tc_Message_Omsg)
| v_sko__urX(v_evs_H) = X0
| v_sko__urX(v_evs) = X0
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(resolution,[],[f6814,f4719]) ).
fof(f6830,plain,
! [X0] :
( ~ c_lessequals(v_sko__urX(v_evs_H_H),X0,tc_nat)
| v_sko__urX(v_evs) = X0
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs)
| v_sko__urX(v_evs_H) = X0 ),
inference(resolution,[],[f6819,f3562]) ).
fof(f6845,plain,
! [X0] :
( v_sko__urX(v_evs) = c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs)
| v_sko__urX(v_evs_H) = c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat) ),
inference(resolution,[],[f6830,f3558]) ).
fof(f6895,plain,
! [X0] :
( ~ c_less(v_sko__urX(v_evs),X0,tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs)
| v_sko__urX(v_evs_H) = c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat) ),
inference(superposition,[],[f2432,f6845]) ).
fof(f6898,plain,
! [X0] :
( v_sko__urX(v_evs_H) = c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs)
| c_List_Olist_ONil = c_List_Oupt(v_sko__urX(v_evs),v_sko__urX(v_evs_H_H)) ),
inference(superposition,[],[f5143,f6845]) ).
fof(f6899,plain,
! [X0] :
( v_sko__urX(v_evs_H) = c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs)
| c_List_Olist_ONil = c_List_Oupt(v_sko__urX(v_evs),X0) ),
inference(superposition,[],[f5144,f6845]) ).
fof(f6907,plain,
( v_sko__urX(v_evs_H) = v_sko__urX(v_evs)
| v_sko__urX(v_evs_H) = c_plus(v_sko__urX(v_evs_H_H),c_Finite__Set_Ocard(c_SetInterval_OatMost(v_sko__urX(v_evs),tc_nat),tc_nat),tc_nat) ),
inference(resolution,[],[f6895,f3569]) ).
fof(f6908,plain,
( v_sko__urX(v_evs_H) = c_Finite__Set_Ocard(c_SetInterval_OatMost(c_plus(v_sko__urX(v_evs_H_H),v_sko__urX(v_evs),tc_nat),tc_nat),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(forward_demodulation,[],[f6907,f3692]) ).
fof(f6921,plain,
( c_less(c_plus(v_sko__urX(v_evs_H_H),v_sko__urX(v_evs),tc_nat),v_sko__urX(v_evs_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(superposition,[],[f3569,f6908]) ).
fof(f6922,plain,
( c_less(c_0,v_sko__urX(v_evs_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(superposition,[],[f3570,f6908]) ).
fof(f6927,plain,
( ~ c_Parity_Oeven(c_plus(v_sko__urX(v_evs_H_H),v_sko__urX(v_evs),tc_nat),tc_nat)
| ~ c_Parity_Oeven(v_sko__urX(v_evs_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(superposition,[],[f3730,f6908]) ).
fof(f6928,plain,
( c_Parity_Oeven(c_plus(v_sko__urX(v_evs_H_H),v_sko__urX(v_evs),tc_nat),tc_nat)
| c_Parity_Oeven(v_sko__urX(v_evs_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(superposition,[],[f3731,f6908]) ).
fof(f6943,plain,
( c_1 = c_div(v_sko__urX(v_evs_H),v_sko__urX(v_evs_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(resolution,[],[f6922,f1278]) ).
fof(f6980,plain,
( c_0 = c_minus(c_1,v_sko__urX(v_evs_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(superposition,[],[f5628,f6943]) ).
fof(f7089,plain,
( c_less(v_sko__urX(v_evs),v_sko__urX(v_evs_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs)
| v_sko__urX(v_evs_H) = c_plus(v_sko__urX(v_evs_H_H),v_sko__urX(v_evs),tc_nat) ),
inference(superposition,[],[f6921,f6845]) ).
fof(f7090,plain,
( c_less(v_sko__urX(v_evs),v_sko__urX(v_evs_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs)
| v_sko__urX(v_evs_H) = c_plus(v_sko__urX(v_evs_H_H),v_sko__urX(v_evs),tc_nat) ),
inference(duplicate_literal_removal,[],[f7089]) ).
fof(f7340,plain,
! [X0] :
( c_List_Olist_ONil = c_List_Oupt(v_sko__urX(v_evs_H),v_sko__urX(v_evs_H_H))
| c_List_Olist_ONil = c_List_Oupt(v_sko__urX(v_evs),X0)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(superposition,[],[f5143,f6899]) ).
fof(f7451,plain,
! [X0] :
( c_Nat_Osize(c_List_Olist_ONil,tc_List_Olist(tc_nat)) = c_minus(X0,v_sko__urX(v_evs),tc_nat)
| c_List_Olist_ONil = c_List_Oupt(v_sko__urX(v_evs_H),v_sko__urX(v_evs_H_H))
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(superposition,[],[f1812,f7340]) ).
fof(f7455,plain,
! [X0] :
( c_0 = c_minus(X0,v_sko__urX(v_evs),tc_nat)
| c_List_Olist_ONil = c_List_Oupt(v_sko__urX(v_evs_H),v_sko__urX(v_evs_H_H))
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(forward_demodulation,[],[f7451,f1791]) ).
fof(f7457,plain,
! [X0] : c_plus(c_1,c_IntDef_Oint(X0),tc_IntDef_Oint) = c_IntDef_Oint(c_plus(c_1,X0,tc_nat)),
inference(superposition,[],[f2144,f1488]) ).
fof(f7485,plain,
! [X0,X1] :
( c_plus(X0,X1,tc_nat) != X0
| c_0 = X1 ),
inference(superposition,[],[f2425,f2350]) ).
fof(f7506,plain,
! [X0,X1] :
( c_plus(X1,X0,tc_nat) != X0
| c_0 = X1 ),
inference(superposition,[],[f2430,f2448]) ).
fof(f7582,plain,
! [X0] :
( c_less(c_0,c_0,tc_nat)
| ~ c_less(v_sko__urX(v_evs),X0,tc_nat)
| c_List_Olist_ONil = c_List_Oupt(v_sko__urX(v_evs_H),v_sko__urX(v_evs_H_H))
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(superposition,[],[f2453,f7455]) ).
fof(f7590,plain,
! [X0] :
( ~ c_less(v_sko__urX(v_evs),X0,tc_nat)
| c_List_Olist_ONil = c_List_Oupt(v_sko__urX(v_evs_H),v_sko__urX(v_evs_H_H))
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(forward_subsumption_resolution,[],[f7582,f2436]) ).
fof(f7600,plain,
( c_List_Olist_ONil = c_List_Oupt(v_sko__urX(v_evs_H),v_sko__urX(v_evs_H_H))
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(resolution,[],[f7590,f3569]) ).
fof(f7605,plain,
( c_Nat_Osize(c_List_Olist_ONil,tc_List_Olist(tc_nat)) = c_minus(v_sko__urX(v_evs_H_H),v_sko__urX(v_evs_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(superposition,[],[f1812,f7600]) ).
fof(f7608,plain,
( c_0 = c_minus(v_sko__urX(v_evs_H_H),v_sko__urX(v_evs_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(forward_demodulation,[],[f7605,f1791]) ).
fof(f7615,plain,
( c_0 != c_0
| c_lessequals(v_sko__urX(v_evs_H_H),v_sko__urX(v_evs_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(superposition,[],[f2368,f7608]) ).
fof(f7620,plain,
( c_lessequals(v_sko__urX(v_evs_H_H),v_sko__urX(v_evs_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(trivial_inequality_removal,[],[f7615]) ).
fof(f7727,plain,
( c_less(v_sko__urX(v_evs_H),v_sko__urX(v_evs_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs)
| c_List_Olist_ONil = c_List_Oupt(v_sko__urX(v_evs),v_sko__urX(v_evs_H_H)) ),
inference(superposition,[],[f6921,f6898]) ).
fof(f7741,plain,
! [X0] :
( ~ c_less(v_sko__urX(v_evs_H),X0,tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs)
| c_List_Olist_ONil = c_List_Oupt(v_sko__urX(v_evs),v_sko__urX(v_evs_H_H)) ),
inference(superposition,[],[f2432,f6898]) ).
fof(f7753,plain,
( c_less(v_sko__urX(v_evs_H),v_sko__urX(v_evs_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs)
| c_List_Olist_ONil = c_List_Oupt(v_sko__urX(v_evs),v_sko__urX(v_evs_H_H)) ),
inference(duplicate_literal_removal,[],[f7727]) ).
fof(f7760,plain,
( c_List_Olist_ONil = c_List_Oupt(v_sko__urX(v_evs),v_sko__urX(v_evs_H_H))
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(forward_subsumption_resolution,[],[f7753,f7741]) ).
fof(f7774,plain,
( c_Nat_Osize(c_List_Olist_ONil,tc_List_Olist(tc_nat)) = c_minus(v_sko__urX(v_evs_H_H),v_sko__urX(v_evs),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(superposition,[],[f1812,f7760]) ).
fof(f7777,plain,
( c_0 = c_minus(v_sko__urX(v_evs_H_H),v_sko__urX(v_evs),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(forward_demodulation,[],[f7774,f1791]) ).
fof(f7782,plain,
( c_0 != c_0
| c_lessequals(v_sko__urX(v_evs_H_H),v_sko__urX(v_evs),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(superposition,[],[f2368,f7777]) ).
fof(f7787,plain,
( c_lessequals(v_sko__urX(v_evs_H_H),v_sko__urX(v_evs),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(trivial_inequality_removal,[],[f7782]) ).
fof(f15212,plain,
! [X0] :
( c_in(c_Message_Omsg_ONonce(X0),c_Event_Oused(v_evs),tc_Message_Omsg)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H)
| v_sko__urX(v_evs_H_H) = X0
| v_sko__urX(v_evs_H) = X0 ),
inference(resolution,[],[f6815,f4719]) ).
fof(f15274,plain,
! [X0] :
( ~ c_lessequals(v_sko__urX(v_evs),X0,tc_nat)
| v_sko__urX(v_evs_H_H) = X0
| v_sko__urX(v_evs_H) = X0
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(resolution,[],[f15212,f3562]) ).
fof(f15307,plain,
! [X0] :
( v_sko__urX(v_evs_H) = c_plus(v_sko__urX(v_evs),X0,tc_nat)
| v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs),X0,tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(resolution,[],[f15274,f3558]) ).
fof(f15455,plain,
! [X0] :
( ~ c_less(v_sko__urX(v_evs_H),X0,tc_nat)
| v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs),X0,tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(superposition,[],[f2432,f15307]) ).
fof(f15463,plain,
! [X0] :
( v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs),X0,tc_nat)
| c_List_Olist_ONil = c_List_Oupt(v_sko__urX(v_evs_H),X0)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(superposition,[],[f5144,f15307]) ).
fof(f15489,plain,
( v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs),c_Finite__Set_Ocard(c_SetInterval_OatMost(v_sko__urX(v_evs_H),tc_nat),tc_nat),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(resolution,[],[f15455,f3569]) ).
fof(f15496,plain,
( v_sko__urX(v_evs_H_H) = c_Finite__Set_Ocard(c_SetInterval_OatMost(c_plus(v_sko__urX(v_evs),v_sko__urX(v_evs_H),tc_nat),tc_nat),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(forward_demodulation,[],[f15489,f3692]) ).
fof(f15556,plain,
( c_less(c_plus(v_sko__urX(v_evs),v_sko__urX(v_evs_H),tc_nat),v_sko__urX(v_evs_H_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(superposition,[],[f3569,f15496]) ).
fof(f15557,plain,
( c_less(c_0,v_sko__urX(v_evs_H_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(superposition,[],[f3570,f15496]) ).
fof(f15683,plain,
! [X0] : c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat) = c_IntDef_Onat(c_plus(c_1,c_IntDef_Oint(X0),tc_IntDef_Oint)),
inference(superposition,[],[f1505,f3622]) ).
fof(f15786,plain,
! [X0] : c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat) = c_IntDef_Onat(c_IntDef_Oint(c_plus(c_1,X0,tc_nat))),
inference(forward_demodulation,[],[f15683,f7457]) ).
fof(f15808,plain,
! [X0] : c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat) = c_plus(c_1,X0,tc_nat),
inference(forward_demodulation,[],[f15786,f1505]) ).
fof(f16002,plain,
! [X0] :
( ~ c_lessequals(X0,c_plus(v_sko__urX(v_evs),v_sko__urX(v_evs_H),tc_nat),tc_nat)
| c_less(X0,v_sko__urX(v_evs_H_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(superposition,[],[f3819,f15496]) ).
fof(f16402,plain,
! [X0] :
( c_div(c_times(v_sko__urX(v_evs_H_H),X0,tc_nat),v_sko__urX(v_evs_H_H),tc_nat) = X0
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(resolution,[],[f1273,f15557]) ).
fof(f16741,plain,
! [X0] :
( ~ c_less(c_times(v_sko__urX(v_evs_H_H),X0,tc_nat),X0,tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(superposition,[],[f6422,f16402]) ).
fof(f16765,plain,
! [X0] :
( v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H)
| ~ c_lessequals(c_times(v_sko__urX(v_evs_H_H),c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat),tc_nat),X0,tc_nat) ),
inference(resolution,[],[f16741,f3819]) ).
fof(f16778,plain,
! [X0] :
( ~ c_lessequals(c_times(v_sko__urX(v_evs_H_H),c_plus(c_1,X0,tc_nat),tc_nat),X0,tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(forward_demodulation,[],[f16765,f15808]) ).
fof(f16926,plain,
! [X0] :
( c_List_Odrop(X0,c_List_Olist_ONil,tc_nat) = c_List_Oupt(c_plus(v_sko__urX(v_evs),X0,tc_nat),v_sko__urX(v_evs_H_H))
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(superposition,[],[f1760,f7760]) ).
fof(f16942,plain,
! [X0] :
( c_List_Olist_ONil = c_List_Oupt(c_plus(v_sko__urX(v_evs),X0,tc_nat),v_sko__urX(v_evs_H_H))
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(forward_demodulation,[],[f16926,f1746]) ).
fof(f17139,plain,
! [X0] :
( c_Nat_Osize(c_List_Olist_ONil,tc_List_Olist(tc_nat)) = c_minus(v_sko__urX(v_evs_H_H),c_plus(v_sko__urX(v_evs),X0,tc_nat),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(superposition,[],[f1812,f16942]) ).
fof(f17154,plain,
! [X0] :
( c_0 = c_minus(v_sko__urX(v_evs_H_H),c_plus(v_sko__urX(v_evs),X0,tc_nat),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(forward_demodulation,[],[f17139,f1791]) ).
fof(f17564,plain,
( v_sko__urX(v_evs) = c_plus(v_sko__urX(v_evs_H_H),c_minus(v_sko__urX(v_evs),v_sko__urX(v_evs_H_H),tc_nat),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(resolution,[],[f2378,f7787]) ).
fof(f17567,plain,
( v_sko__urX(v_evs_H) = c_plus(v_sko__urX(v_evs_H_H),c_minus(v_sko__urX(v_evs_H),v_sko__urX(v_evs_H_H),tc_nat),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(resolution,[],[f2378,f7620]) ).
fof(f17981,plain,
( ~ c_lessequals(c_times(v_sko__urX(v_evs_H_H),c_1,tc_nat),c_0,tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(superposition,[],[f16778,f2350]) ).
fof(f17991,plain,
( ~ c_lessequals(v_sko__urX(v_evs_H_H),c_0,tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(forward_demodulation,[],[f17981,f4913]) ).
fof(f18026,plain,
! [X0] :
( c_less(c_0,c_0,tc_nat)
| ~ c_less(c_plus(v_sko__urX(v_evs),X0,tc_nat),v_sko__urX(v_evs_H_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(superposition,[],[f2453,f17154]) ).
fof(f18046,plain,
! [X0] :
( ~ c_less(c_plus(v_sko__urX(v_evs),X0,tc_nat),v_sko__urX(v_evs_H_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(forward_subsumption_resolution,[],[f18026,f2436]) ).
fof(f18085,plain,
( v_sko__urX(v_evs_H) = v_sko__urX(v_evs)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(resolution,[],[f18046,f15556]) ).
fof(f25584,plain,
! [X0] :
( ~ c_less(c_0,X0,tc_nat)
| c_less(c_minus(X0,v_sko__urX(v_evs_H),tc_nat),X0,tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(resolution,[],[f2079,f6922]) ).
fof(f25585,plain,
! [X0] :
( ~ c_less(c_0,X0,tc_nat)
| c_less(c_minus(X0,v_sko__urX(v_evs_H_H),tc_nat),X0,tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(resolution,[],[f2079,f15557]) ).
fof(f25599,plain,
( c_less(c_minus(c_1,v_sko__urX(v_evs_H),tc_nat),c_1,tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(resolution,[],[f25584,f2384]) ).
fof(f25644,plain,
( c_0 = c_IntDef_Oint(c_minus(c_1,v_sko__urX(v_evs_H),tc_nat))
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(resolution,[],[f25599,f5692]) ).
fof(f25741,plain,
! [X0] :
( c_plus(c_IntDef_Oint(X0),c_0,tc_IntDef_Oint) = c_IntDef_Oint(c_plus(X0,c_minus(c_1,v_sko__urX(v_evs_H),tc_nat),tc_nat))
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(superposition,[],[f2144,f25644]) ).
fof(f25798,plain,
! [X0] :
( c_IntDef_Oint(X0) = c_IntDef_Oint(c_plus(X0,c_minus(c_1,v_sko__urX(v_evs_H),tc_nat),tc_nat))
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(forward_demodulation,[],[f25741,f4901]) ).
fof(f27432,plain,
( c_less(c_minus(c_1,v_sko__urX(v_evs_H_H),tc_nat),c_1,tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(resolution,[],[f25585,f2384]) ).
fof(f27521,plain,
( c_0 = c_IntDef_Oint(c_minus(c_1,v_sko__urX(v_evs_H_H),tc_nat))
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(resolution,[],[f27432,f5692]) ).
fof(f27646,plain,
! [X0] :
( c_plus(c_IntDef_Oint(X0),c_0,tc_IntDef_Oint) = c_IntDef_Oint(c_plus(X0,c_minus(c_1,v_sko__urX(v_evs_H_H),tc_nat),tc_nat))
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(superposition,[],[f2144,f27521]) ).
fof(f27664,plain,
( ~ c_lessequals(c_0,c_0,tc_IntDef_Oint)
| c_lessequals(c_minus(c_1,v_sko__urX(v_evs_H_H),tc_nat),c_0,tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(superposition,[],[f5431,f27521]) ).
fof(f27688,plain,
( c_lessequals(c_minus(c_1,v_sko__urX(v_evs_H_H),tc_nat),c_0,tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(forward_subsumption_resolution,[],[f27664,f4718]) ).
fof(f27696,plain,
! [X0] :
( c_IntDef_Oint(X0) = c_IntDef_Oint(c_plus(X0,c_minus(c_1,v_sko__urX(v_evs_H_H),tc_nat),tc_nat))
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(forward_demodulation,[],[f27646,f4901]) ).
fof(f28346,plain,
! [X2,X0,X1] : c_Finite__Set_Ocard(c_SetInterval_OgreaterThanLessThan(X0,c_minus(X1,X2,tc_nat),tc_nat),tc_nat) = c_minus(X1,c_plus(X2,c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat),tc_nat),tc_nat),
inference(superposition,[],[f2366,f3738]) ).
fof(f28349,plain,
! [X2,X0,X1] : c_Finite__Set_Ocard(c_SetInterval_OgreaterThanLessThan(X0,c_minus(X1,X2,tc_nat),tc_nat),tc_nat) = c_minus(X1,c_Finite__Set_Ocard(c_SetInterval_OatMost(c_plus(X2,X0,tc_nat),tc_nat),tc_nat),tc_nat),
inference(forward_demodulation,[],[f28346,f3692]) ).
fof(f28366,plain,
! [X2,X0,X1] : c_Finite__Set_Ocard(c_SetInterval_OgreaterThanLessThan(X0,c_minus(X1,X2,tc_nat),tc_nat),tc_nat) = c_Finite__Set_Ocard(c_SetInterval_OgreaterThanLessThan(c_plus(X2,X0,tc_nat),X1,tc_nat),tc_nat),
inference(forward_demodulation,[],[f28349,f3738]) ).
fof(f28724,plain,
! [X0] :
( c_IntDef_Onat(c_IntDef_Oint(X0)) = c_plus(X0,c_minus(c_1,v_sko__urX(v_evs_H),tc_nat),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(superposition,[],[f1505,f25798]) ).
fof(f28805,plain,
! [X0] :
( c_plus(X0,c_minus(c_1,v_sko__urX(v_evs_H),tc_nat),tc_nat) = X0
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(forward_demodulation,[],[f28724,f1505]) ).
fof(f28841,plain,
! [X0,X1] :
( c_plus(X0,X1,tc_nat) != X0
| c_minus(c_1,v_sko__urX(v_evs_H),tc_nat) = X1
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(superposition,[],[f2425,f28805]) ).
fof(f29712,plain,
! [X0] :
( c_IntDef_Onat(c_IntDef_Oint(X0)) = c_plus(X0,c_minus(c_1,v_sko__urX(v_evs_H_H),tc_nat),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(superposition,[],[f1505,f27696]) ).
fof(f29778,plain,
! [X0] :
( c_plus(X0,c_minus(c_1,v_sko__urX(v_evs_H_H),tc_nat),tc_nat) = X0
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(forward_demodulation,[],[f29712,f1505]) ).
fof(f29859,plain,
! [X0,X1] :
( c_plus(X0,X1,tc_nat) != X0
| c_minus(c_1,v_sko__urX(v_evs_H_H),tc_nat) = X1
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(superposition,[],[f2425,f29778]) ).
fof(f38311,plain,
! [X0,X1] : c_lessequals(X0,c_Finite__Set_Ocard(c_SetInterval_OatMost(c_plus(X0,X1,tc_nat),tc_nat),tc_nat),tc_nat),
inference(superposition,[],[f3558,f3692]) ).
fof(f38570,plain,
! [X0,X1] : c_lessequals(X0,c_plus(c_1,c_plus(X0,X1,tc_nat),tc_nat),tc_nat),
inference(forward_demodulation,[],[f38311,f15808]) ).
fof(f38806,plain,
! [X0,X1] : c_lessequals(X1,c_Finite__Set_Ocard(c_SetInterval_OatMost(c_plus(X0,X1,tc_nat),tc_nat),tc_nat),tc_nat),
inference(superposition,[],[f3559,f3710]) ).
fof(f38847,plain,
! [X0,X1] : c_lessequals(X1,c_plus(c_1,c_plus(X0,X1,tc_nat),tc_nat),tc_nat),
inference(forward_demodulation,[],[f38806,f15808]) ).
fof(f44397,plain,
! [X0] :
( c_plus(c_minus(c_0,c_minus(c_1,v_sko__urX(v_evs_H_H),tc_nat),tc_nat),X0,tc_nat) = c_minus(c_plus(c_0,X0,tc_nat),c_minus(c_1,v_sko__urX(v_evs_H_H),tc_nat),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(resolution,[],[f2073,f27688]) ).
fof(f44427,plain,
! [X0] :
( c_minus(X0,c_minus(c_1,v_sko__urX(v_evs_H_H),tc_nat),tc_nat) = c_plus(c_minus(c_0,c_minus(c_1,v_sko__urX(v_evs_H_H),tc_nat),tc_nat),X0,tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(forward_demodulation,[],[f44397,f2448]) ).
fof(f44447,plain,
! [X0] :
( c_plus(c_0,X0,tc_nat) = c_minus(X0,c_minus(c_1,v_sko__urX(v_evs_H_H),tc_nat),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(forward_demodulation,[],[f44427,f2362]) ).
fof(f44460,plain,
! [X0] :
( c_minus(X0,c_minus(c_1,v_sko__urX(v_evs_H_H),tc_nat),tc_nat) = X0
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(forward_demodulation,[],[f44447,f2448]) ).
fof(f44496,plain,
! [X0,X1] : c_minus(c_plus(X0,X1,tc_nat),X1,tc_nat) = c_plus(X0,c_minus(X1,X1,tc_nat),tc_nat),
inference(resolution,[],[f2074,f4719]) ).
fof(f44621,plain,
! [X0,X1] : c_plus(X0,c_0,tc_nat) = c_minus(c_plus(X0,X1,tc_nat),X1,tc_nat),
inference(forward_demodulation,[],[f44496,f2373]) ).
fof(f44634,plain,
! [X0,X1] : c_minus(c_plus(X0,X1,tc_nat),X1,tc_nat) = X0,
inference(forward_demodulation,[],[f44621,f2350]) ).
fof(f47193,plain,
( v_sko__urX(v_evs_H) != v_sko__urX(v_evs_H_H)
| c_minus(c_1,v_sko__urX(v_evs_H),tc_nat) = c_minus(v_sko__urX(v_evs_H),v_sko__urX(v_evs_H_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(superposition,[],[f28841,f17567]) ).
fof(f47198,plain,
( v_sko__urX(v_evs_H) != v_sko__urX(v_evs_H_H)
| c_minus(c_1,v_sko__urX(v_evs_H),tc_nat) = c_minus(v_sko__urX(v_evs_H),v_sko__urX(v_evs_H_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(duplicate_literal_removal,[],[f47193]) ).
fof(f47217,plain,
( c_minus(c_1,v_sko__urX(v_evs_H),tc_nat) = c_minus(v_sko__urX(v_evs_H),v_sko__urX(v_evs_H_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(forward_subsumption_resolution,[],[f47198,f18085]) ).
fof(f47307,plain,
( c_0 != c_minus(c_1,v_sko__urX(v_evs_H),tc_nat)
| c_lessequals(v_sko__urX(v_evs_H),v_sko__urX(v_evs_H_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(superposition,[],[f2368,f47217]) ).
fof(f47326,plain,
( c_lessequals(v_sko__urX(v_evs_H),v_sko__urX(v_evs_H_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(forward_subsumption_resolution,[],[f47307,f6980]) ).
fof(f47430,plain,
( c_List_Olist_ONil = c_List_Oupt(v_sko__urX(v_evs_H_H),v_sko__urX(v_evs_H))
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(resolution,[],[f47326,f2060]) ).
fof(f47506,plain,
! [X0] :
( c_List_Odrop(X0,c_List_Olist_ONil,tc_nat) = c_List_Oupt(c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat),v_sko__urX(v_evs_H))
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(superposition,[],[f1760,f47430]) ).
fof(f47518,plain,
! [X0] :
( c_List_Olist_ONil = c_List_Oupt(c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat),v_sko__urX(v_evs_H))
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(forward_demodulation,[],[f47506,f1746]) ).
fof(f47704,plain,
( c_List_Olist_ONil = c_List_Oupt(v_sko__urX(v_evs),v_sko__urX(v_evs_H))
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(superposition,[],[f47518,f17564]) ).
fof(f47735,plain,
( c_List_Olist_ONil = c_List_Oupt(v_sko__urX(v_evs),v_sko__urX(v_evs_H))
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(duplicate_literal_removal,[],[f47704]) ).
fof(f47796,plain,
( c_Nat_Osize(c_List_Olist_ONil,tc_List_Olist(tc_nat)) = c_minus(v_sko__urX(v_evs_H),v_sko__urX(v_evs),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(superposition,[],[f1812,f47735]) ).
fof(f47801,plain,
( c_0 = c_minus(v_sko__urX(v_evs_H),v_sko__urX(v_evs),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(forward_demodulation,[],[f47796,f1791]) ).
fof(f47852,plain,
( c_less(c_0,c_0,tc_nat)
| ~ c_less(v_sko__urX(v_evs),v_sko__urX(v_evs_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(superposition,[],[f2453,f47801]) ).
fof(f47862,plain,
( ~ c_less(v_sko__urX(v_evs),v_sko__urX(v_evs_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(forward_subsumption_resolution,[],[f47852,f2436]) ).
fof(f47878,plain,
( v_sko__urX(v_evs_H) = v_sko__urX(v_evs)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs)
| v_sko__urX(v_evs_H) = c_plus(v_sko__urX(v_evs_H_H),v_sko__urX(v_evs),tc_nat) ),
inference(resolution,[],[f47862,f7090]) ).
fof(f47891,plain,
( v_sko__urX(v_evs_H) = c_plus(v_sko__urX(v_evs_H_H),v_sko__urX(v_evs),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(duplicate_literal_removal,[],[f47878]) ).
fof(f47972,plain,
( ~ c_Parity_Oeven(v_sko__urX(v_evs_H),tc_nat)
| ~ c_Parity_Oeven(v_sko__urX(v_evs_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(superposition,[],[f6927,f47891]) ).
fof(f47973,plain,
( c_Parity_Oeven(v_sko__urX(v_evs_H),tc_nat)
| c_Parity_Oeven(v_sko__urX(v_evs_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(superposition,[],[f6928,f47891]) ).
fof(f48047,plain,
( c_Parity_Oeven(v_sko__urX(v_evs_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(duplicate_literal_removal,[],[f47973]) ).
fof(f48048,plain,
( ~ c_Parity_Oeven(v_sko__urX(v_evs_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
inference(duplicate_literal_removal,[],[f47972]) ).
fof(f48072,plain,
v_sko__urX(v_evs_H) = v_sko__urX(v_evs),
inference(forward_subsumption_resolution,[],[f48048,f48047]) ).
fof(f51704,plain,
! [X0,X1] : c_div(c_plus(X0,c_times(X1,c_1,tc_nat),tc_nat),c_1,tc_nat) = c_plus(X1,c_div(X0,c_1,tc_nat),tc_nat),
inference(resolution,[],[f1272,f2384]) ).
fof(f51732,plain,
! [X0,X1] : c_plus(X1,X0,tc_nat) = c_div(c_plus(X0,c_times(X1,c_1,tc_nat),tc_nat),c_1,tc_nat),
inference(forward_demodulation,[],[f51704,f5300]) ).
fof(f51738,plain,
! [X0,X1] : c_plus(X1,X0,tc_nat) = c_plus(X0,c_times(X1,c_1,tc_nat),tc_nat),
inference(forward_demodulation,[],[f51732,f5300]) ).
fof(f51743,plain,
! [X0,X1] : c_plus(X0,X1,tc_nat) = c_plus(X1,X0,tc_nat),
inference(forward_demodulation,[],[f51738,f4913]) ).
fof(f60334,plain,
! [X0] :
( ~ c_less(v_sko__urX(v_evs_H_H),X0,tc_nat)
| c_List_Olist_ONil = c_List_Oupt(v_sko__urX(v_evs_H),X0)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(superposition,[],[f2432,f15463]) ).
fof(f60533,plain,
( c_List_Olist_ONil = c_List_Oupt(v_sko__urX(v_evs_H),c_Finite__Set_Ocard(c_SetInterval_OatMost(v_sko__urX(v_evs_H_H),tc_nat),tc_nat))
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(resolution,[],[f60334,f3569]) ).
fof(f60542,plain,
( c_List_Olist_ONil = c_List_Oupt(v_sko__urX(v_evs_H),c_plus(c_1,v_sko__urX(v_evs_H_H),tc_nat))
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(forward_demodulation,[],[f60533,f15808]) ).
fof(f60621,plain,
( c_Nat_Osize(c_List_Olist_ONil,tc_List_Olist(tc_nat)) = c_minus(c_plus(c_1,v_sko__urX(v_evs_H_H),tc_nat),v_sko__urX(v_evs_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(superposition,[],[f1812,f60542]) ).
fof(f60624,plain,
( c_0 = c_minus(c_plus(c_1,v_sko__urX(v_evs_H_H),tc_nat),v_sko__urX(v_evs_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(forward_demodulation,[],[f60621,f1791]) ).
fof(f63123,plain,
( c_less(v_sko__urX(v_evs_H),v_sko__urX(v_evs_H_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(resolution,[],[f16002,f3559]) ).
fof(f63208,plain,
( v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H)
| v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs),v_sko__urX(v_evs_H_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(resolution,[],[f63123,f15455]) ).
fof(f63228,plain,
( v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H)
| v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs),v_sko__urX(v_evs_H_H),tc_nat) ),
inference(duplicate_literal_removal,[],[f63208]) ).
fof(f63230,plain,
( v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs_H_H),v_sko__urX(v_evs),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(forward_demodulation,[],[f63228,f51743]) ).
fof(f63231,plain,
( v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs_H_H),v_sko__urX(v_evs_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(forward_demodulation,[],[f63230,f48072]) ).
fof(f64118,plain,
( v_sko__urX(v_evs_H_H) != v_sko__urX(v_evs_H_H)
| v_sko__urX(v_evs_H) = c_minus(c_1,v_sko__urX(v_evs_H_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(superposition,[],[f29859,f63231]) ).
fof(f64125,plain,
( v_sko__urX(v_evs_H_H) != v_sko__urX(v_evs_H_H)
| v_sko__urX(v_evs_H) = c_minus(c_1,v_sko__urX(v_evs_H_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(duplicate_literal_removal,[],[f64118]) ).
fof(f64126,plain,
( v_sko__urX(v_evs_H) = c_minus(c_1,v_sko__urX(v_evs_H_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(trivial_inequality_removal,[],[f64125]) ).
fof(f66149,plain,
! [X0] :
( c_minus(X0,v_sko__urX(v_evs_H),tc_nat) = X0
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(superposition,[],[f44460,f64126]) ).
fof(f66216,plain,
! [X0] :
( c_minus(X0,v_sko__urX(v_evs_H),tc_nat) = X0
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(duplicate_literal_removal,[],[f66149]) ).
fof(f66726,plain,
( c_0 = c_plus(c_1,v_sko__urX(v_evs_H_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(superposition,[],[f60624,f66216]) ).
fof(f66772,plain,
( c_0 = c_plus(c_1,v_sko__urX(v_evs_H_H),tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(duplicate_literal_removal,[],[f66726]) ).
fof(f68735,plain,
( c_lessequals(v_sko__urX(v_evs_H_H),c_0,tc_nat)
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
inference(superposition,[],[f3559,f66772]) ).
fof(f68806,plain,
v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H),
inference(forward_subsumption_resolution,[],[f68735,f17991]) ).
fof(f86200,plain,
! [X0,X1] :
( c_Finite__Set_Ocard(c_SetInterval_OatMost(c_plus(X0,X1,tc_nat),tc_nat),tc_nat) != X0
| c_0 = c_Finite__Set_Ocard(c_SetInterval_OatMost(X1,tc_nat),tc_nat) ),
inference(superposition,[],[f7485,f3692]) ).
fof(f86264,plain,
! [X0,X1] : c_Finite__Set_Ocard(c_SetInterval_OatMost(c_plus(X0,X1,tc_nat),tc_nat),tc_nat) != X0,
inference(forward_subsumption_resolution,[],[f86200,f3691]) ).
fof(f86270,plain,
! [X0,X1] : c_plus(c_1,c_plus(X0,X1,tc_nat),tc_nat) != X0,
inference(forward_demodulation,[],[f86264,f15808]) ).
fof(f86529,plain,
! [X0,X1] :
( c_Finite__Set_Ocard(c_SetInterval_OatMost(c_plus(X0,X1,tc_nat),tc_nat),tc_nat) != X1
| c_0 = c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat) ),
inference(superposition,[],[f7506,f3710]) ).
fof(f86562,plain,
! [X0,X1] : c_Finite__Set_Ocard(c_SetInterval_OatMost(c_plus(X0,X1,tc_nat),tc_nat),tc_nat) != X1,
inference(forward_subsumption_resolution,[],[f86529,f3691]) ).
fof(f86570,plain,
! [X0,X1] : c_plus(c_1,c_plus(X0,X1,tc_nat),tc_nat) != X1,
inference(forward_demodulation,[],[f86562,f15808]) ).
fof(f99421,plain,
! [X0,X1] : c_Finite__Set_Ocard(c_SetInterval_OgreaterThanLessThan(X0,X1,tc_nat),tc_nat) = c_minus(X1,c_plus(c_1,X0,tc_nat),tc_nat),
inference(superposition,[],[f3738,f15808]) ).
fof(f105309,plain,
! [X0,X1] :
( v_sko__urX(v_evs_H) = X0
| v_sko__urX(v_evs_H) = c_plus(c_1,c_plus(v_sko__urX(v_evs_H_H),X1,tc_nat),tc_nat)
| c_plus(c_1,c_plus(v_sko__urX(v_evs_H_H),X1,tc_nat),tc_nat) = X0
| c_in(c_Message_Omsg_ONonce(X0),c_Event_Oused(v_evs),tc_Message_Omsg) ),
inference(resolution,[],[f38570,f6815]) ).
fof(f105419,plain,
! [X0,X1] :
( v_sko__urX(v_evs_H_H) = X0
| v_sko__urX(v_evs_H) = c_plus(c_1,c_plus(v_sko__urX(v_evs_H_H),X1,tc_nat),tc_nat)
| c_plus(c_1,c_plus(v_sko__urX(v_evs_H_H),X1,tc_nat),tc_nat) = X0
| c_in(c_Message_Omsg_ONonce(X0),c_Event_Oused(v_evs),tc_Message_Omsg) ),
inference(forward_demodulation,[],[f105309,f68806]) ).
fof(f105434,plain,
! [X0,X1] :
( v_sko__urX(v_evs_H_H) = c_plus(c_1,c_plus(v_sko__urX(v_evs_H_H),X1,tc_nat),tc_nat)
| v_sko__urX(v_evs_H_H) = X0
| c_plus(c_1,c_plus(v_sko__urX(v_evs_H_H),X1,tc_nat),tc_nat) = X0
| c_in(c_Message_Omsg_ONonce(X0),c_Event_Oused(v_evs),tc_Message_Omsg) ),
inference(forward_demodulation,[],[f105419,f68806]) ).
fof(f105444,plain,
! [X0,X1] :
( c_in(c_Message_Omsg_ONonce(X0),c_Event_Oused(v_evs),tc_Message_Omsg)
| c_plus(c_1,c_plus(v_sko__urX(v_evs_H_H),X1,tc_nat),tc_nat) = X0
| v_sko__urX(v_evs_H_H) = X0 ),
inference(forward_subsumption_resolution,[],[f105434,f86270]) ).
fof(f116911,plain,
! [X0,X1] :
( c_plus(c_1,c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat),tc_nat) = X1
| v_sko__urX(v_evs_H_H) = X1
| ~ c_lessequals(v_sko__urX(v_evs),X1,tc_nat) ),
inference(resolution,[],[f105444,f3562]) ).
fof(f116922,plain,
! [X0,X1] :
( ~ c_lessequals(v_sko__urX(v_evs_H),X1,tc_nat)
| c_plus(c_1,c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat),tc_nat) = X1
| v_sko__urX(v_evs_H_H) = X1 ),
inference(forward_demodulation,[],[f116911,f48072]) ).
fof(f116923,plain,
! [X0,X1] :
( ~ c_lessequals(v_sko__urX(v_evs_H_H),X1,tc_nat)
| c_plus(c_1,c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat),tc_nat) = X1
| v_sko__urX(v_evs_H_H) = X1 ),
inference(forward_demodulation,[],[f116922,f68806]) ).
fof(f117153,plain,
! [X0,X1] :
( c_plus(c_1,c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat),tc_nat) = c_plus(c_1,c_plus(X1,v_sko__urX(v_evs_H_H),tc_nat),tc_nat)
| v_sko__urX(v_evs_H_H) = c_plus(c_1,c_plus(X1,v_sko__urX(v_evs_H_H),tc_nat),tc_nat) ),
inference(resolution,[],[f116923,f38847]) ).
fof(f117189,plain,
! [X0,X1] : c_plus(c_1,c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat),tc_nat) = c_plus(c_1,c_plus(X1,v_sko__urX(v_evs_H_H),tc_nat),tc_nat),
inference(forward_subsumption_resolution,[],[f117153,f86570]) ).
fof(f117777,plain,
! [X0,X1] : c_0 = c_minus(c_plus(X1,v_sko__urX(v_evs_H_H),tc_nat),c_plus(c_1,c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat),tc_nat),tc_nat),
inference(superposition,[],[f5622,f117189]) ).
fof(f117805,plain,
! [X0,X1] : c_0 = c_Finite__Set_Ocard(c_SetInterval_OgreaterThanLessThan(c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat),c_plus(X1,v_sko__urX(v_evs_H_H),tc_nat),tc_nat),tc_nat),
inference(forward_demodulation,[],[f117777,f99421]) ).
fof(f117830,plain,
! [X0,X1] : c_0 = c_Finite__Set_Ocard(c_SetInterval_OgreaterThanLessThan(X0,c_minus(c_plus(X1,v_sko__urX(v_evs_H_H),tc_nat),v_sko__urX(v_evs_H_H),tc_nat),tc_nat),tc_nat),
inference(forward_demodulation,[],[f117805,f28366]) ).
fof(f117845,plain,
! [X0,X1] : c_0 = c_Finite__Set_Ocard(c_SetInterval_OgreaterThanLessThan(X0,X1,tc_nat),tc_nat),
inference(forward_demodulation,[],[f117830,f44634]) ).
fof(f117888,plain,
! [X0,X1] : c_0 = c_minus(X0,X1,tc_nat),
inference(superposition,[],[f3842,f117845]) ).
fof(f118035,plain,
! [X0] : c_0 = X0,
inference(superposition,[],[f2451,f117888]) ).
fof(f125599,plain,
c_0 != c_0,
inference(superposition,[],[f3691,f118035]) ).
fof(f131236,plain,
$false,
inference(trivial_inequality_removal,[],[f125599]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWV282-1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.18 % Computer : n016.cluster.edu
% 0.08/0.18 % Model : x86_64 x86_64
% 0.08/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.18 % Memory : 8046.5625MB
% 0.08/0.18 % OS : Linux 6.8.0-71-generic
% 0.08/0.18 % CPULimit : 300
% 0.08/0.18 % WCLimit : 300
% 0.08/0.18 % DateTime : Mon Sep 28 10:29:33 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.53/1.59 % (3535266)Will run a generic schedule for satisfiability detection.
% 7.53/1.59 % (3535276)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=943480706:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 7.53/1.59 % (3535272)% WARNING: option uhcvi not known.
% 7.53/1.59 % (3535271)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3764182660_2999 on theBenchmark for (2999ds/0Mi)
% 7.53/1.59 % (3535272)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1543615459:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 7.53/1.59 % (3535274)dis+10_1_sil=32000:sp=arity:random_seed=3599129896:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 7.53/1.59 % (3535275)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=421708924:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 7.53/1.59 % (3535277)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3244228327:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 7.53/1.59 % (3535273)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4097424952:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 7.53/1.59 % (3535276)Instruction limit reached!
% 7.53/1.59 % (3535276)------------------------------
% 7.53/1.59 % (3535276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.53/1.59 % (3535276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.53/1.59 % (3535276)CaDiCaL version: 2.1.3
% 7.53/1.59 % (3535276)Termination reason: Instruction limit
% 7.53/1.59 % (3535276)Termination phase: Saturation
% 7.53/1.59 % (3535276)Time elapsed: 0.042 s
% 7.53/1.59 % (3535276)Peak memory usage: 16 MB
% 7.53/1.59 % (3535276)Instructions burned: 131 (million)
% 7.53/1.59 % (3535285)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=807366507:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 7.53/1.59 % (3535274)Instruction limit reached!
% 7.53/1.59 % (3535274)------------------------------
% 7.53/1.59 % (3535274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.53/1.59 % (3535274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.53/1.59 % (3535274)CaDiCaL version: 2.1.3
% 7.53/1.59 % (3535274)Termination reason: Instruction limit
% 7.53/1.59 % (3535274)Termination phase: Saturation
% 7.53/1.59 % (3535274)Time elapsed: 0.062 s
% 7.53/1.59 % (3535274)Peak memory usage: 15 MB
% 7.53/1.59 % (3535274)Instructions burned: 103 (million)
% 7.53/1.59 % (3535275)Instruction limit reached!
% 7.53/1.59 % (3535275)------------------------------
% 7.53/1.59 % (3535275)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.53/1.59 % (3535275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.53/1.59 % (3535275)CaDiCaL version: 2.1.3
% 7.53/1.59 % (3535275)Termination reason: Instruction limit
% 7.53/1.59 % (3535275)Termination phase: Saturation
% 7.53/1.59 % (3535275)Time elapsed: 0.065 s
% 7.53/1.59 % (3535275)Peak memory usage: 16 MB
% 7.53/1.59 % (3535275)Instructions burned: 118 (million)
% 7.53/1.59 % (3535287)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3602208733:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 7.53/1.59 % (3535288)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1757955983:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 7.53/1.59 % (3535277)Instruction limit reached!
% 7.53/1.59 % (3535277)------------------------------
% 7.53/1.59 % (3535277)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.53/1.59 % (3535277)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.53/1.59 % (3535277)CaDiCaL version: 2.1.3
% 7.53/1.59 % (3535277)Termination reason: Instruction limit
% 7.53/1.59 % (3535277)Termination phase: Saturation
% 7.53/1.59 % (3535277)Time elapsed: 0.099 s
% 7.53/1.59 % (3535277)Peak memory usage: 17 MB
% 7.53/1.59 % (3535277)Instructions burned: 160 (million)
% 7.53/1.59 % (3535291)ott-21_1_sil=16000:fs=off:random_seed=2191591887:i=180:av=off:fsr=off_2997 on theBenchmark for (2997ds/180Mi)
% 7.53/1.59 % (3535287)Instruction limit reached!
% 7.53/1.59 % (3535287)------------------------------
% 7.53/1.59 % (3535287)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 7.53/1.59 % (3535287)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.53/1.59 % (3535287)CaDiCaL version: 2.1.3
% 34.81/5.24 % (3535287)Termination reason: Instruction limit
% 34.81/5.24 % (3535287)Termination phase: Saturation
% 34.81/5.24 % (3535287)Time elapsed: 0.077 s
% 34.81/5.24 % (3535287)Peak memory usage: 16 MB
% 34.81/5.24 % (3535287)Instructions burned: 131 (million)
% 34.81/5.24 % (3535293)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=801331890:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 34.81/5.24 % TRYING [1]
% 34.81/5.24 % (3535291)Instruction limit reached!
% 34.81/5.24 % (3535291)------------------------------
% 34.81/5.24 % (3535291)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.81/5.24 % (3535291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.81/5.24 % (3535291)CaDiCaL version: 2.1.3
% 34.81/5.24 % (3535291)Termination reason: Instruction limit
% 34.81/5.24 % (3535291)Termination phase: Saturation
% 34.81/5.24 % (3535291)Time elapsed: 0.097 s
% 34.81/5.24 % (3535291)Peak memory usage: 16 MB
% 34.81/5.24 % (3535291)Instructions burned: 180 (million)
% 34.81/5.24 % TRYING [2]
% 34.81/5.24 % (3535285)Instruction limit reached!
% 34.81/5.24 % (3535285)------------------------------
% 34.81/5.24 % (3535285)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.81/5.24 % (3535285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.81/5.24 % (3535285)CaDiCaL version: 2.1.3
% 34.81/5.24 % (3535285)Termination reason: Instruction limit
% 34.81/5.24 % (3535285)Termination phase: Finite model building constraint generation
% 34.81/5.24 % (3535285)Time elapsed: 0.184 s
% 34.81/5.24 % (3535285)Peak memory usage: 27 MB
% 34.81/5.24 % (3535285)Instructions burned: 716 (million)
% 34.81/5.24 % (3535295)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1376073523:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 34.81/5.24 % (3535296)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3863282011:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 34.81/5.24 % TRYING [1]
% 34.81/5.24 % TRYING [2]
% 34.81/5.24 % (3535288)Instruction limit reached!
% 34.81/5.24 % (3535288)------------------------------
% 34.81/5.24 % (3535288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.81/5.24 % (3535288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.81/5.24 % (3535288)CaDiCaL version: 2.1.3
% 34.81/5.24 % (3535288)Termination reason: Instruction limit
% 34.81/5.24 % (3535288)Termination phase: Saturation
% 34.81/5.24 % (3535288)Time elapsed: 0.344 s
% 34.81/5.24 % (3535288)Peak memory usage: 19 MB
% 34.81/5.24 % (3535288)Instructions burned: 685 (million)
% 34.81/5.24 % (3535299)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3307400640:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 34.81/5.24 % (3535293)Instruction limit reached!
% 34.81/5.24 % (3535293)------------------------------
% 34.81/5.24 % (3535293)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.81/5.24 % (3535293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.81/5.24 % (3535293)CaDiCaL version: 2.1.3
% 34.81/5.24 % (3535293)Termination reason: Instruction limit
% 34.81/5.24 % (3535293)Termination phase: Saturation
% 34.81/5.24 % (3535293)Time elapsed: 0.295 s
% 34.81/5.24 % (3535293)Peak memory usage: 17 MB
% 34.81/5.24 % (3535293)Instructions burned: 477 (million)
% 34.81/5.24 % (3535301)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1021167716:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 34.81/5.24 % TRYING [1]
% 34.81/5.24 % (3535296)Instruction limit reached!
% 34.81/5.24 % (3535296)------------------------------
% 34.81/5.24 % (3535296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.81/5.24 % (3535296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.81/5.24 % (3535296)CaDiCaL version: 2.1.3
% 34.81/5.24 % (3535296)Termination reason: Instruction limit
% 34.81/5.24 % (3535296)Termination phase: Saturation
% 34.81/5.24 % (3535296)Time elapsed: 0.411 s
% 34.81/5.24 % (3535296)Peak memory usage: 28 MB
% 34.81/5.24 % (3535296)Instructions burned: 1180 (million)
% 34.81/5.24 % (3535303)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=1394872241:i=879:kws=inv_precedence:fsr=off_2992 on theBenchmark for (2992ds/879Mi)
% 34.81/5.24 % (3535295)Instruction limit reached!
% 34.81/5.24 % (3535295)------------------------------
% 34.81/5.24 % (3535295)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 34.81/5.24 % (3535295)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.03/9.09 % (3535295)CaDiCaL version: 2.1.3
% 62.03/9.09 % (3535295)Termination reason: Instruction limit
% 62.03/9.09 % (3535295)Termination phase: Finite model building constraint generation
% 62.03/9.09 % (3535295)Time elapsed: 0.430 s
% 62.03/9.09 % (3535295)Peak memory usage: 43 MB
% 62.03/9.09 % (3535295)Instructions burned: 868 (million)
% 62.03/9.09 % (3535305)fmb+10_1_sil=64000:random_seed=3934182312:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 62.03/9.09 % (3535299)Cannot represent all propositional literals internally
% 62.03/9.09 % (3535299)Refutation not found, incomplete strategy
% 62.03/9.09 % (3535299)------------------------------
% 62.03/9.09 % (3535299)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.03/9.09 % (3535299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.03/9.09 % (3535299)CaDiCaL version: 2.1.3
% 62.03/9.09 % (3535299)Termination reason: Refutation not found, incomplete strategy
% 62.03/9.09 % (3535299)Time elapsed: 0.314 s
% 62.03/9.09 % (3535299)Peak memory usage: 25 MB
% 62.03/9.09 % (3535299)Instructions burned: 627 (million)
% 62.03/9.09 % (3535299)------------------------------
% 62.03/9.09 % (3535299)------------------------------
% 62.03/9.09 % (3535307)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4091109931:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 62.03/9.09 % (3535301)Instruction limit reached!
% 62.03/9.09 % (3535301)------------------------------
% 62.03/9.09 % (3535301)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.03/9.09 % (3535301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.03/9.09 % (3535301)CaDiCaL version: 2.1.3
% 62.03/9.09 % (3535301)Termination reason: Instruction limit
% 62.03/9.09 % (3535301)Termination phase: Saturation
% 62.03/9.09 % (3535301)Time elapsed: 0.396 s
% 62.03/9.09 % (3535301)Peak memory usage: 26 MB
% 62.03/9.09 % (3535301)Instructions burned: 692 (million)
% 62.03/9.09 % (3535303)Instruction limit reached!
% 62.03/9.09 % (3535303)------------------------------
% 62.03/9.09 % (3535303)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.03/9.09 % (3535303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.03/9.09 % (3535303)CaDiCaL version: 2.1.3
% 62.03/9.09 % (3535303)Termination reason: Instruction limit
% 62.03/9.09 % (3535303)Termination phase: Saturation
% 62.03/9.09 % (3535303)Time elapsed: 0.232 s
% 62.03/9.09 % (3535303)Peak memory usage: 21 MB
% 62.03/9.09 % (3535303)Instructions burned: 883 (million)
% 62.03/9.09 % (3535310)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2860433522:i=5131_2989 on theBenchmark for (2989ds/5131Mi)
% 62.03/9.09 % (3535309)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=85485731:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 62.03/9.09 % TRYING [1]
% 62.03/9.09 % (3535307)Cannot represent all propositional literals internally
% 62.03/9.09 % (3535307)Refutation not found, incomplete strategy
% 62.03/9.09 % (3535307)------------------------------
% 62.03/9.09 % (3535307)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.03/9.09 % (3535307)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.03/9.09 % (3535307)CaDiCaL version: 2.1.3
% 62.03/9.09 % (3535307)Termination reason: Refutation not found, incomplete strategy
% 62.03/9.09 % (3535307)Time elapsed: 0.311 s
% 62.03/9.09 % (3535307)Peak memory usage: 24 MB
% 62.03/9.09 % (3535307)Instructions burned: 624 (million)
% 62.03/9.09 % (3535307)------------------------------
% 62.03/9.09 % (3535307)------------------------------
% 62.03/9.09 % (3535313)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1617517093:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 62.03/9.09 % (3535309)Cannot represent all propositional literals internally
% 62.03/9.09 % (3535309)Refutation not found, incomplete strategy
% 62.03/9.09 % (3535309)------------------------------
% 62.03/9.09 % (3535309)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 62.03/9.09 % (3535309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 62.03/9.09 % (3535309)CaDiCaL version: 2.1.3
% 62.03/9.09 % (3535309)Termination reason: Refutation not found, incomplete strategy
% 62.03/9.09 % (3535309)Time elapsed: 0.311 s
% 62.03/9.09 % (3535309)Peak memory usage: 24 MB
% 62.03/9.09 % (3535309)Instructions burned: 624 (million)
% 62.03/9.09 % (3535309)------------------------------
% 62.03/9.09 % (3535309)------------------------------
% 62.03/9.09 % (3535315)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1568757489:i=6324_2986 on theBenchmark for (2986ds/6324Mi)
% 67.56/9.90 % TRYING [2]
% 67.56/9.90 % (3535315)Cannot represent all propositional literals internally
% 67.56/9.90 % (3535315)Refutation not found, incomplete strategy
% 67.56/9.90 % (3535315)------------------------------
% 67.56/9.90 % (3535315)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.56/9.90 % (3535315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.56/9.90 % (3535315)CaDiCaL version: 2.1.3
% 67.56/9.90 % (3535315)Termination reason: Refutation not found, incomplete strategy
% 67.56/9.90 % (3535315)Time elapsed: 0.322 s
% 67.56/9.90 % (3535315)Peak memory usage: 25 MB
% 67.56/9.90 % (3535315)Instructions burned: 644 (million)
% 67.56/9.90 % (3535315)------------------------------
% 67.56/9.90 % (3535315)------------------------------
% 67.56/9.90 % (3535317)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4130083669:fmbsr=2.30978:i=2174_2983 on theBenchmark for (2983ds/2174Mi)
% 67.56/9.90 % (3535313)Instruction limit reached!
% 67.56/9.90 % (3535313)------------------------------
% 67.56/9.90 % (3535313)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.56/9.90 % (3535313)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.56/9.90 % (3535313)CaDiCaL version: 2.1.3
% 67.56/9.90 % (3535313)Termination reason: Instruction limit
% 67.56/9.90 % (3535313)Termination phase: Saturation
% 67.56/9.90 % (3535313)Time elapsed: 0.880 s
% 67.56/9.90 % (3535313)Peak memory usage: 35 MB
% 67.56/9.90 % (3535313)Instructions burned: 1473 (million)
% 67.56/9.90 % (3535319)ott-2_1_sil=16000:newcnf=on:random_seed=689922204:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2978 on theBenchmark for (2978ds/869Mi)
% 67.56/9.90 % (3535319)Instruction limit reached!
% 67.56/9.90 % (3535319)------------------------------
% 67.56/9.90 % (3535319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.56/9.90 % (3535319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.56/9.90 % (3535319)CaDiCaL version: 2.1.3
% 67.56/9.90 % (3535319)Termination reason: Instruction limit
% 67.56/9.90 % (3535319)Termination phase: Saturation
% 67.56/9.90 % (3535319)Time elapsed: 0.441 s
% 67.56/9.90 % (3535319)Peak memory usage: 18 MB
% 67.56/9.90 % (3535319)Instructions burned: 870 (million)
% 67.56/9.90 % (3535321)ott+10_1_sil=32000:tgt=ground:random_seed=3700602588:i=5114:av=off_2974 on theBenchmark for (2974ds/5114Mi)
% 67.56/9.90 % (3535310)Instruction limit reached!
% 67.56/9.90 % (3535310)------------------------------
% 67.56/9.90 % (3535310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.56/9.90 % (3535310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.56/9.90 % (3535310)CaDiCaL version: 2.1.3
% 67.56/9.90 % (3535310)Termination reason: Instruction limit
% 67.56/9.90 % (3535310)Termination phase: Saturation
% 67.56/9.90 % (3535310)Time elapsed: 1.678 s
% 67.56/9.90 % (3535310)Peak memory usage: 52 MB
% 67.56/9.90 % (3535310)Instructions burned: 5134 (million)
% 67.56/9.90 % (3535323)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=198939330:i=54282_2973 on theBenchmark for (2973ds/54282Mi)
% 67.56/9.90 % (3535317)Instruction limit reached!
% 67.56/9.90 % (3535317)------------------------------
% 67.56/9.90 % (3535317)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.56/9.90 % (3535317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.56/9.90 % (3535317)CaDiCaL version: 2.1.3
% 67.56/9.90 % (3535317)Termination reason: Instruction limit
% 67.56/9.90 % (3535317)Termination phase: Finite model building preprocessing
% 67.56/9.90 % (3535317)Time elapsed: 1.090 s
% 67.56/9.90 % (3535317)Peak memory usage: 39 MB
% 67.56/9.90 % (3535317)Instructions burned: 2176 (million)
% 67.56/9.90 % (3535325)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2058950214:i=3512:aac=none_2971 on theBenchmark for (2971ds/3512Mi)
% 67.56/9.90 % TRYING [1]
% 67.56/9.90 % TRYING [2]
% 67.56/9.90 % (3535325)Instruction limit reached!
% 67.56/9.90 % (3535325)------------------------------
% 67.56/9.90 % (3535325)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 67.56/9.90 % (3535325)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.56/9.90 % (3535325)CaDiCaL version: 2.1.3
% 67.56/9.90 % (3535325)Termination reason: Instruction limit
% 67.56/9.90 % (3535325)Termination phase: Saturation
% 67.56/9.90 % (3535325)Time elapsed: 2.191 s
% 67.56/9.90 % (3535325)Peak memory usage: 44 MB
% 67.56/9.90 % (3535325)Instructions burned: 3513 (million)
% 41.82/12.24 % (3535327)dis+21_1_sil=32000:sas=cadical:random_seed=2714699741:i=3773:amm=off_2949 on theBenchmark for (2949ds/3773Mi)
% 41.82/12.24 % (3535321)Instruction limit reached!
% 41.82/12.24 % (3535321)------------------------------
% 41.82/12.24 % (3535321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.82/12.24 % (3535321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.82/12.24 % (3535321)CaDiCaL version: 2.1.3
% 41.82/12.24 % (3535321)Termination reason: Instruction limit
% 41.82/12.24 % (3535321)Termination phase: Saturation
% 41.82/12.24 % (3535321)Time elapsed: 2.765 s
% 41.82/12.24 % (3535321)Peak memory usage: 39 MB
% 41.82/12.24 % (3535321)Instructions burned: 5115 (million)
% 41.82/12.24 % (3535329)ott+11_1_sil=16000:gs=on:random_seed=2166905524:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2946 on theBenchmark for (2946ds/2251Mi)
% 41.82/12.24 % (3535329)Instruction limit reached!
% 41.82/12.24 % (3535329)------------------------------
% 41.82/12.24 % (3535329)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.82/12.24 % (3535329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.82/12.24 % (3535329)CaDiCaL version: 2.1.3
% 41.82/12.24 % (3535329)Termination reason: Instruction limit
% 41.82/12.24 % (3535329)Termination phase: Saturation
% 41.82/12.24 % (3535329)Time elapsed: 1.119 s
% 41.82/12.24 % (3535329)Peak memory usage: 24 MB
% 41.82/12.24 % (3535329)Instructions burned: 2251 (million)
% 41.82/12.24 % (3535331)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=350725020:fmbsr=1.6:i=67534_2934 on theBenchmark for (2934ds/67534Mi)
% 41.82/12.24 % (3535331)Cannot represent all propositional literals internally
% 41.82/12.24 % (3535331)Refutation not found, incomplete strategy
% 41.82/12.24 % (3535331)------------------------------
% 41.82/12.24 % (3535331)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.82/12.24 % (3535331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.82/12.24 % (3535331)CaDiCaL version: 2.1.3
% 41.82/12.24 % (3535331)Termination reason: Refutation not found, incomplete strategy
% 41.82/12.24 % (3535331)Time elapsed: 0.319 s
% 41.82/12.24 % (3535331)Peak memory usage: 23 MB
% 41.82/12.24 % (3535331)Instructions burned: 651 (million)
% 41.82/12.24 % (3535331)------------------------------
% 41.82/12.24 % (3535331)------------------------------
% 41.82/12.24 % (3535333)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3078317801:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2931 on theBenchmark for (2931ds/4591Mi)
% 41.82/12.24 % (3535327)Instruction limit reached!
% 41.82/12.24 % (3535327)------------------------------
% 41.82/12.24 % (3535327)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.82/12.24 % (3535327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.82/12.24 % (3535327)CaDiCaL version: 2.1.3
% 41.82/12.24 % (3535327)Termination reason: Instruction limit
% 41.82/12.24 % (3535327)Termination phase: Saturation
% 41.82/12.24 % (3535327)Time elapsed: 2.290 s
% 41.82/12.24 % (3535327)Peak memory usage: 44 MB
% 41.82/12.24 % (3535327)Instructions burned: 3774 (million)
% 41.82/12.24 % (3535335)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=1035917633:i=29340_2926 on theBenchmark for (2926ds/29340Mi)
% 41.82/12.24 % (3535323)Cannot represent all propositional literals internally
% 41.82/12.24 % (3535271)Cannot represent all propositional literals internally
% 41.82/12.24 % (3535323)Refutation not found, incomplete strategy
% 41.82/12.24 % (3535323)------------------------------
% 41.82/12.24 % (3535323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.82/12.24 % (3535323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.82/12.24 % (3535323)CaDiCaL version: 2.1.3
% 41.82/12.24 % (3535323)Termination reason: Refutation not found, incomplete strategy
% 41.82/12.24 % (3535323)Time elapsed: 5.460 s
% 41.82/12.24 % (3535323)Peak memory usage: 981 MB
% 41.82/12.24 % (3535323)Instructions burned: 14777 (million)
% 41.82/12.24 % (3535323)------------------------------
% 41.82/12.24 % (3535323)------------------------------
% 41.82/12.24 % (3535337)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2690809447:i=5211_2917 on theBenchmark for (2917ds/5211Mi)
% 41.82/12.24 % (3535271)Refutation not found, incomplete strategy
% 41.82/12.24 % (3535271)------------------------------
% 41.82/12.24 % (3535271)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.82/12.24 % (3535271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.82/12.24 % (3535271)CaDiCaL version: 2.1.3
% 41.82/12.24 % (3535271)Termination reason: Refutation not found, incomplete strategy
% 41.82/12.24 % (3535271)Time elapsed: 8.759 s
% 41.82/12.24 % (3535271)Peak memory usage: 981 MB
% 41.82/12.24 % (3535271)Instructions burned: 14777 (million)
% 41.82/12.24 % (3535271)------------------------------
% 41.82/12.24 % (3535271)------------------------------
% 41.82/12.24 % (3535339)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3830453865:i=5497:nm=2_2910 on theBenchmark for (2910ds/5497Mi)
% 41.82/12.24 % (3535333)Instruction limit reached!
% 41.82/12.24 % (3535333)------------------------------
% 41.82/12.24 % (3535333)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.82/12.24 % (3535333)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.82/12.24 % (3535333)CaDiCaL version: 2.1.3
% 41.82/12.24 % (3535333)Termination reason: Instruction limit
% 41.82/12.24 % (3535333)Termination phase: Saturation
% 41.82/12.24 % (3535333)Time elapsed: 2.154 s
% 41.82/12.24 % (3535333)Peak memory usage: 42 MB
% 41.82/12.24 % (3535333)Instructions burned: 4592 (million)
% 41.82/12.24 % (3535341)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3571323188:fmbsr=2:i=46332_2909 on theBenchmark for (2909ds/46332Mi)
% 41.82/12.24 % (3535339)Cannot represent all propositional literals internally
% 41.82/12.24 % (3535339)Refutation not found, incomplete strategy
% 41.82/12.24 % (3535339)------------------------------
% 41.82/12.24 % (3535339)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.82/12.24 % (3535339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.82/12.24 % (3535339)CaDiCaL version: 2.1.3
% 41.82/12.24 % (3535339)Termination reason: Refutation not found, incomplete strategy
% 41.82/12.24 % (3535339)Time elapsed: 0.326 s
% 41.82/12.24 % (3535339)Peak memory usage: 25 MB
% 41.82/12.24 % (3535339)Instructions burned: 644 (million)
% 41.82/12.24 % (3535339)------------------------------
% 41.82/12.24 % (3535339)------------------------------
% 41.82/12.24 % (3535343)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3284093009:i=14071_2906 on theBenchmark for (2906ds/14071Mi)
% 41.82/12.24 % (3535341)Cannot represent all propositional literals internally
% 41.82/12.24 % (3535341)Refutation not found, incomplete strategy
% 41.82/12.24 % (3535341)------------------------------
% 41.82/12.24 % (3535341)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.82/12.24 % (3535341)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.82/12.24 % (3535341)CaDiCaL version: 2.1.3
% 41.82/12.24 % (3535341)Termination reason: Refutation not found, incomplete strategy
% 41.82/12.24 % (3535341)Time elapsed: 0.319 s
% 41.82/12.24 % (3535341)Peak memory usage: 23 MB
% 41.82/12.24 % (3535341)Instructions burned: 653 (million)
% 41.82/12.24 % (3535341)------------------------------
% 41.82/12.24 % (3535341)------------------------------
% 41.82/12.24 % (3535345)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3277669971:i=22565:add=on:rawr=on_2906 on theBenchmark for (2906ds/22565Mi)
% 41.82/12.24 % (3535337)Instruction limit reached!
% 41.82/12.24 % (3535337)------------------------------
% 41.82/12.24 % (3535337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.82/12.24 % (3535337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.82/12.24 % (3535337)CaDiCaL version: 2.1.3
% 41.82/12.24 % (3535337)Termination reason: Instruction limit
% 41.82/12.24 % (3535337)Termination phase: Saturation
% 41.82/12.24 % (3535337)Time elapsed: 1.413 s
% 41.82/12.24 % (3535337)Peak memory usage: 44 MB
% 41.82/12.24 % (3535337)Instructions burned: 5211 (million)
% 41.82/12.24 % (3535343)Cannot represent all propositional literals internally
% 41.82/12.24 % (3535343)Refutation not found, incomplete strategy
% 41.82/12.24 % (3535343)------------------------------
% 41.82/12.24 % (3535343)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.82/12.24 % (3535343)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.82/12.24 % (3535343)CaDiCaL version: 2.1.3
% 41.82/12.24 % (3535343)Termination reason: Refutation not found, incomplete strategy
% 41.82/12.24 % (3535343)Time elapsed: 0.315 s
% 41.82/12.24 % (3535343)Peak memory usage: 25 MB
% 41.82/12.24 % (3535343)Instructions burned: 626 (million)
% 41.82/12.24 % (3535343)------------------------------
% 41.82/12.24 % (3535343)------------------------------
% 41.82/12.24 % (3535347)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=871710316:i=8173:av=off_2903 on theBenchmark for (2903ds/8173Mi)
% 41.82/12.24 % (3535348)dis+10_16:1_sil=16000:random_seed=3832446574:i=9155:fsr=off_2903 on theBenchmark for (2903ds/9155Mi)
% 41.82/12.24 % (3535347) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3535266-3535347"...
% 41.82/12.24 % (3535347)...printing done.
% 41.82/12.24 % (3535347)Refutation found. Thanks to Tanya!
% 41.82/12.24 % SZS status Unsatisfiable for theBenchmark
% 41.82/12.24 % SZS output start Proof for theBenchmark
% See solution above
% 41.82/12.25 % (3535347)------------------------------
% 41.82/12.25 % (3535347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 41.82/12.25 % (3535347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 41.82/12.25 % (3535347)CaDiCaL version: 2.1.3
% 41.82/12.25 % (3535347)Termination reason: Refutation
% 41.82/12.25 % (3535347)Time elapsed: 2.265 s
% 41.82/12.25 % (3535347)Peak memory usage: 51 MB
% 41.82/12.25 % (3535347)Instructions burned: 7680 (million)
% 41.82/12.25 % (3535266)Success in time 12.014 s
% 41.82/12.25 % Vampire exiting
%------------------------------------------------------------------------------