%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV282-1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:08:39 PM UTC 2026
% Result : Unsatisfiable 22.08s 3.97s
% Output : Refutation 23.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 23
% Number of leaves : 33
% Syntax : Number of formulae : 184 ( 50 unt; 18 def)
% Number of atoms : 447 ( 153 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 435 ( 172 ~; 248 |; 0 &)
% ( 15 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 21 ( 19 usr; 16 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 9 con; 0-3 aty)
% Number of variables : 163 ( 0 sgn 163 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f79,axiom,
! [X0] : c_less(X0,c_Suc(X0),tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Nat_OlessI_0) ).
fof(f82,axiom,
! [X0,X1] :
( c_lessequals(X1,X1,X0)
| ~ class_Orderings_Oorder(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Orderings_Oorder__class_Oaxioms__1_0) ).
fof(f243,axiom,
class_Orderings_Oorder(tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clsarity_nat_3) ).
fof(f2350,axiom,
! [X0] : c_plus(X0,c_0,tc_nat) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',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/sandbox/benchmark/theBenchmark.p',cls_Nat_Oadd__Suc__right_0) ).
fof(f2431,axiom,
! [X0,X1] : ~ c_less(c_plus(X0,X1,tc_nat),X0,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Nat_Onot__add__less1_0) ).
fof(f2432,axiom,
! [X0,X1] : ~ c_less(c_plus(X0,X1,tc_nat),X1,tc_nat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Nat_Onot__add__less2_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/sandbox/benchmark/theBenchmark.p',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(f3054,axiom,
! [X0] : c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat) = c_Suc(X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',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(f3558,axiom,
! [X0,X1] : c_lessequals(X0,c_plus(X0,X1,tc_nat),tc_nat),
file('/export/starexec/sandbox/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/sandbox/benchmark/theBenchmark.p',cls_Nat_Ole__add2_0) ).
fof(f3560,axiom,
! [X0,X1] :
( ~ c_less(X0,c_Suc(X1),tc_nat)
| c_lessequals(X0,X1,tc_nat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',cls_Nat_Oless__Suc__eq__le_0) ).
fof(f3561,axiom,
! [X0,X1] :
( ~ c_lessequals(X0,X1,tc_nat)
| c_less(X0,c_Suc(X1),tc_nat) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f3564,plain,
! [X2,X0,X1] :
( X0 = X1
| X1 = X2
| 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) ),
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(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(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(f3818,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,[],[f3560,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(f3820,definition,
sF0 = c_Event_Oused(v_evs_H_H),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f3821,plain,
c_Event_Oused(v_evs_H_H) = sF0,
inference(reorient_equations,[],[f3820]) ).
fof(f3822,definition,
sF1 = c_Event_Oused(v_evs_H),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f3823,plain,
c_Event_Oused(v_evs_H) = sF1,
inference(reorient_equations,[],[f3822]) ).
fof(f3824,definition,
sF2 = c_Event_Oused(v_evs),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f3825,plain,
c_Event_Oused(v_evs) = sF2,
inference(reorient_equations,[],[f3824]) ).
fof(f3826,plain,
! [X2,X0,X1] :
( c_in(c_Message_Omsg_ONonce(X2),sF1,tc_Message_Omsg)
| c_in(c_Message_Omsg_ONonce(X1),sF0,tc_Message_Omsg)
| c_in(c_Message_Omsg_ONonce(X0),sF2,tc_Message_Omsg)
| X0 = X2
| X1 = X2
| X0 = X1 ),
inference(definition_folding,[],[f3564,f3825,f3823,f3821]) ).
fof(f3853,plain,
! [X0,X1] : c_plus(X0,c_Finite__Set_Ocard(c_SetInterval_OatMost(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(forward_demodulation,[],[f3692,f3710]) ).
fof(f3972,plain,
! [X0] :
( ~ c_lessequals(v_sko__urX(v_evs_H),X0,tc_nat)
| ~ c_in(c_Message_Omsg_ONonce(X0),sF1,tc_Message_Omsg) ),
inference(superposition,[],[f3562,f3823]) ).
fof(f3973,plain,
! [X0] :
( ~ c_lessequals(v_sko__urX(v_evs),X0,tc_nat)
| ~ c_in(c_Message_Omsg_ONonce(X0),sF2,tc_Message_Omsg) ),
inference(superposition,[],[f3562,f3825]) ).
fof(f3974,plain,
! [X0] :
( ~ c_lessequals(v_sko__urX(v_evs_H_H),X0,tc_nat)
| ~ c_in(c_Message_Omsg_ONonce(X0),sF0,tc_Message_Omsg) ),
inference(superposition,[],[f3562,f3821]) ).
fof(f3975,plain,
! [X0] : ~ c_in(c_Message_Omsg_ONonce(c_plus(X0,v_sko__urX(v_evs_H_H),tc_nat)),sF0,tc_Message_Omsg),
inference(resolution,[],[f3559,f3974]) ).
fof(f3977,plain,
! [X0] : ~ c_in(c_Message_Omsg_ONonce(c_plus(X0,v_sko__urX(v_evs_H),tc_nat)),sF1,tc_Message_Omsg),
inference(resolution,[],[f3559,f3972]) ).
fof(f3978,plain,
! [X0] : ~ c_in(c_Message_Omsg_ONonce(c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat)),sF0,tc_Message_Omsg),
inference(resolution,[],[f3558,f3974]) ).
fof(f3979,plain,
! [X0] : ~ c_in(c_Message_Omsg_ONonce(c_plus(v_sko__urX(v_evs),X0,tc_nat)),sF2,tc_Message_Omsg),
inference(resolution,[],[f3558,f3973]) ).
fof(f3980,plain,
! [X0] : ~ c_in(c_Message_Omsg_ONonce(c_plus(v_sko__urX(v_evs_H),X0,tc_nat)),sF1,tc_Message_Omsg),
inference(resolution,[],[f3558,f3972]) ).
fof(f4000,plain,
! [X2,X0,X1] :
( c_in(c_Message_Omsg_ONonce(X2),sF2,tc_Message_Omsg)
| c_in(c_Message_Omsg_ONonce(X1),sF0,tc_Message_Omsg)
| c_plus(v_sko__urX(v_evs_H),X0,tc_nat) = X2
| c_plus(v_sko__urX(v_evs_H),X0,tc_nat) = X1
| X1 = X2 ),
inference(resolution,[],[f3826,f3980]) ).
fof(f4002,plain,
! [X2,X0,X1] :
( c_in(c_Message_Omsg_ONonce(X2),sF2,tc_Message_Omsg)
| c_in(c_Message_Omsg_ONonce(X1),sF1,tc_Message_Omsg)
| X1 = X2
| c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat) = X1
| c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat) = X2 ),
inference(resolution,[],[f3826,f3978]) ).
fof(f4004,plain,
! [X2,X0,X1] :
( c_in(c_Message_Omsg_ONonce(X2),sF0,tc_Message_Omsg)
| c_in(c_Message_Omsg_ONonce(X1),sF1,tc_Message_Omsg)
| c_plus(v_sko__urX(v_evs),X0,tc_nat) = X1
| X1 = X2
| c_plus(v_sko__urX(v_evs),X0,tc_nat) = X2 ),
inference(resolution,[],[f3826,f3979]) ).
fof(f4006,plain,
! [X2,X0,X1] :
( c_in(c_Message_Omsg_ONonce(X1),sF1,tc_Message_Omsg)
| c_plus(v_sko__urX(v_evs),X0,tc_nat) = X1
| c_plus(v_sko__urX(v_evs_H_H),X2,tc_nat) = X1
| c_plus(v_sko__urX(v_evs),X0,tc_nat) = c_plus(v_sko__urX(v_evs_H_H),X2,tc_nat) ),
inference(resolution,[],[f4002,f3979]) ).
fof(f4010,plain,
! [X2,X0,X1] :
( c_in(c_Message_Omsg_ONonce(X1),sF0,tc_Message_Omsg)
| c_plus(v_sko__urX(v_evs),X0,tc_nat) = c_plus(v_sko__urX(v_evs_H),X2,tc_nat)
| c_plus(v_sko__urX(v_evs_H),X2,tc_nat) = X1
| c_plus(v_sko__urX(v_evs),X0,tc_nat) = X1 ),
inference(resolution,[],[f4000,f3979]) ).
fof(f4013,plain,
! [X2,X0,X1] :
( c_in(c_Message_Omsg_ONonce(X1),sF1,tc_Message_Omsg)
| c_plus(v_sko__urX(v_evs),X2,tc_nat) = X1
| c_plus(X0,v_sko__urX(v_evs_H_H),tc_nat) = X1
| c_plus(X0,v_sko__urX(v_evs_H_H),tc_nat) = c_plus(v_sko__urX(v_evs),X2,tc_nat) ),
inference(resolution,[],[f4004,f3975]) ).
fof(f4033,plain,
! [X2,X0,X1] :
( c_plus(v_sko__urX(v_evs),X0,tc_nat) = c_plus(v_sko__urX(v_evs_H),X1,tc_nat)
| c_plus(X2,v_sko__urX(v_evs_H_H),tc_nat) = c_plus(v_sko__urX(v_evs_H),X1,tc_nat)
| c_plus(v_sko__urX(v_evs),X0,tc_nat) = c_plus(X2,v_sko__urX(v_evs_H_H),tc_nat) ),
inference(resolution,[],[f4010,f3975]) ).
fof(f4036,plain,
! [X0,X1] : ~ c_lessequals(c_plus(c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat),X1,tc_nat),X0,tc_nat),
inference(resolution,[],[f3819,f2431]) ).
fof(f4039,plain,
! [X0,X1] : ~ c_lessequals(c_plus(X0,c_Finite__Set_Ocard(c_SetInterval_OatMost(X1,tc_nat),tc_nat),tc_nat),X0,tc_nat),
inference(forward_demodulation,[],[f4036,f3853]) ).
fof(f4060,plain,
( ~ class_Orderings_Oorder(tc_nat)
| ~ c_in(c_Message_Omsg_ONonce(v_sko__urX(v_evs_H_H)),sF0,tc_Message_Omsg) ),
inference(resolution,[],[f82,f3974]) ).
fof(f4062,plain,
( ~ class_Orderings_Oorder(tc_nat)
| ~ c_in(c_Message_Omsg_ONonce(v_sko__urX(v_evs_H)),sF1,tc_Message_Omsg) ),
inference(resolution,[],[f82,f3972]) ).
fof(f4066,plain,
~ c_in(c_Message_Omsg_ONonce(v_sko__urX(v_evs_H)),sF1,tc_Message_Omsg),
inference(forward_subsumption_resolution,[],[f4062,f243]) ).
fof(f4068,plain,
~ c_in(c_Message_Omsg_ONonce(v_sko__urX(v_evs_H_H)),sF0,tc_Message_Omsg),
inference(forward_subsumption_resolution,[],[f4060,f243]) ).
fof(f4083,plain,
! [X0,X1] :
( c_plus(v_sko__urX(v_evs),X0,tc_nat) = c_plus(v_sko__urX(v_evs_H_H),X1,tc_nat)
| v_sko__urX(v_evs_H) = c_plus(v_sko__urX(v_evs_H_H),X1,tc_nat)
| v_sko__urX(v_evs_H) = c_plus(v_sko__urX(v_evs),X0,tc_nat) ),
inference(resolution,[],[f4066,f4006]) ).
fof(f4084,plain,
! [X0,X1] :
( c_plus(v_sko__urX(v_evs),X0,tc_nat) = c_plus(X1,v_sko__urX(v_evs_H_H),tc_nat)
| v_sko__urX(v_evs_H) = c_plus(X1,v_sko__urX(v_evs_H_H),tc_nat)
| v_sko__urX(v_evs_H) = c_plus(v_sko__urX(v_evs),X0,tc_nat) ),
inference(resolution,[],[f4066,f4013]) ).
fof(f4085,plain,
! [X0,X1] :
( c_in(c_Message_Omsg_ONonce(X1),sF2,tc_Message_Omsg)
| c_in(c_Message_Omsg_ONonce(X0),sF1,tc_Message_Omsg)
| X0 = X1
| v_sko__urX(v_evs_H_H) = X0
| v_sko__urX(v_evs_H_H) = X1 ),
inference(resolution,[],[f4068,f3826]) ).
fof(f4091,plain,
! [X0,X1] :
( c_plus(v_sko__urX(v_evs),X0,tc_nat) = c_plus(v_sko__urX(v_evs_H),X1,tc_nat)
| v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs_H),X1,tc_nat)
| v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs),X0,tc_nat) ),
inference(resolution,[],[f4068,f4010]) ).
fof(f4098,plain,
! [X0] :
( c_in(c_Message_Omsg_ONonce(X0),sF2,tc_Message_Omsg)
| v_sko__urX(v_evs_H) = X0
| v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H)
| v_sko__urX(v_evs_H_H) = X0 ),
inference(resolution,[],[f4085,f4066]) ).
fof(f4100,definition,
( spl3_3
<=> v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H) ),
introduced(definition,[new_symbols(definition,[spl3_3])],[avatar_definition]) ).
fof(f4101,plain,
( v_sko__urX(v_evs_H) != v_sko__urX(v_evs_H_H)
| spl3_3 ),
inference(avatar_component_clause,[],[f4100]) ).
fof(f4102,plain,
( v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H)
| ~ spl3_3 ),
inference(avatar_component_clause,[],[f4100]) ).
fof(f4104,definition,
( spl3_4
<=> ! [X0] :
( c_in(c_Message_Omsg_ONonce(X0),sF2,tc_Message_Omsg)
| v_sko__urX(v_evs_H_H) = X0
| v_sko__urX(v_evs_H) = X0 ) ),
introduced(definition,[new_symbols(definition,[spl3_4])],[avatar_definition]) ).
fof(f4105,plain,
( ! [X0] :
( c_in(c_Message_Omsg_ONonce(X0),sF2,tc_Message_Omsg)
| v_sko__urX(v_evs_H_H) = X0
| v_sko__urX(v_evs_H) = X0 )
| ~ spl3_4 ),
inference(avatar_component_clause,[],[f4104]) ).
fof(f4106,plain,
( spl3_3
| spl3_4 ),
inference(avatar_split_clause,[],[f4098,f4104,f4100]) ).
fof(f4108,definition,
( spl3_5
<=> v_sko__urX(v_evs) = v_sko__urX(v_evs_H_H) ),
introduced(definition,[new_symbols(definition,[spl3_5])],[avatar_definition]) ).
fof(f4109,plain,
( v_sko__urX(v_evs) != v_sko__urX(v_evs_H_H)
| spl3_5 ),
inference(avatar_component_clause,[],[f4108]) ).
fof(f4110,plain,
( v_sko__urX(v_evs) = v_sko__urX(v_evs_H_H)
| ~ spl3_5 ),
inference(avatar_component_clause,[],[f4108]) ).
fof(f4117,plain,
( ! [X0] : ~ c_in(c_Message_Omsg_ONonce(c_plus(X0,v_sko__urX(v_evs_H_H),tc_nat)),sF1,tc_Message_Omsg)
| ~ spl3_3 ),
inference(superposition,[],[f3977,f4102]) ).
fof(f4512,plain,
! [X0] : c_lessequals(X0,X0,tc_nat),
inference(resolution,[],[f3818,f3569]) ).
fof(f6101,plain,
! [X2,X0,X1] :
( ~ c_less(c_plus(v_sko__urX(v_evs),X0,tc_nat),X1,tc_nat)
| c_plus(v_sko__urX(v_evs),X0,tc_nat) = c_plus(v_sko__urX(v_evs_H),X2,tc_nat)
| c_plus(v_sko__urX(v_evs_H),X2,tc_nat) = c_plus(X1,v_sko__urX(v_evs_H_H),tc_nat) ),
inference(superposition,[],[f2431,f4033]) ).
fof(f6716,plain,
! [X0,X1] :
( ~ c_in(c_Message_Omsg_ONonce(c_plus(v_sko__urX(v_evs_H),X0,tc_nat)),sF2,tc_Message_Omsg)
| v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs_H),X0,tc_nat)
| v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs),X1,tc_nat) ),
inference(superposition,[],[f3979,f4091]) ).
fof(f7583,plain,
! [X0] :
( v_sko__urX(v_evs) = c_plus(X0,v_sko__urX(v_evs_H_H),tc_nat)
| v_sko__urX(v_evs_H) = c_plus(X0,v_sko__urX(v_evs_H_H),tc_nat)
| v_sko__urX(v_evs_H) = c_plus(v_sko__urX(v_evs),c_0,tc_nat) ),
inference(superposition,[],[f2350,f4084]) ).
fof(f7586,plain,
( ! [X0,X1] :
( ~ c_in(c_Message_Omsg_ONonce(c_plus(v_sko__urX(v_evs),X0,tc_nat)),sF1,tc_Message_Omsg)
| v_sko__urX(v_evs_H) = c_plus(X1,v_sko__urX(v_evs_H_H),tc_nat)
| v_sko__urX(v_evs_H) = c_plus(v_sko__urX(v_evs),X0,tc_nat) )
| ~ spl3_3 ),
inference(superposition,[],[f4117,f4084]) ).
fof(f9152,plain,
! [X0,X1] :
( ~ c_lessequals(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) = c_plus(v_sko__urX(v_evs_H_H),c_Finite__Set_Ocard(c_SetInterval_OatMost(X1,tc_nat),tc_nat),tc_nat)
| v_sko__urX(v_evs_H) = c_plus(v_sko__urX(v_evs),X0,tc_nat) ),
inference(superposition,[],[f4039,f4083]) ).
fof(f9703,definition,
( spl3_15
<=> ! [X1] : v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs),X1,tc_nat) ),
introduced(definition,[new_symbols(definition,[spl3_15])],[avatar_definition]) ).
fof(f9704,plain,
( ! [X1] : v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs),X1,tc_nat)
| ~ spl3_15 ),
inference(avatar_component_clause,[],[f9703]) ).
fof(f9856,plain,
( ! [X0,X1] :
( v_sko__urX(v_evs_H_H) = c_plus(X1,v_sko__urX(v_evs_H_H),tc_nat)
| ~ c_in(c_Message_Omsg_ONonce(c_plus(v_sko__urX(v_evs),X0,tc_nat)),sF1,tc_Message_Omsg)
| v_sko__urX(v_evs_H) = c_plus(v_sko__urX(v_evs),X0,tc_nat) )
| ~ spl3_3 ),
inference(forward_demodulation,[],[f7586,f4102]) ).
fof(f10311,definition,
( spl3_20
<=> ! [X0] :
( ~ c_in(c_Message_Omsg_ONonce(c_plus(v_sko__urX(v_evs),X0,tc_nat)),sF1,tc_Message_Omsg)
| v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs),X0,tc_nat) ) ),
introduced(definition,[new_symbols(definition,[spl3_20])],[avatar_definition]) ).
fof(f10312,plain,
( ! [X0] :
( ~ c_in(c_Message_Omsg_ONonce(c_plus(v_sko__urX(v_evs),X0,tc_nat)),sF1,tc_Message_Omsg)
| v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs),X0,tc_nat) )
| ~ spl3_20 ),
inference(avatar_component_clause,[],[f10311]) ).
fof(f10334,definition,
( spl3_25
<=> ! [X2] : v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs_H_H),X2,tc_nat) ),
introduced(definition,[new_symbols(definition,[spl3_25])],[avatar_definition]) ).
fof(f10335,plain,
( ! [X2] : v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs_H_H),X2,tc_nat)
| ~ spl3_25 ),
inference(avatar_component_clause,[],[f10334]) ).
fof(f10497,plain,
( ! [X0,X1] :
( v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs),X0,tc_nat)
| v_sko__urX(v_evs_H_H) = c_plus(X1,v_sko__urX(v_evs_H_H),tc_nat)
| ~ c_in(c_Message_Omsg_ONonce(c_plus(v_sko__urX(v_evs),X0,tc_nat)),sF1,tc_Message_Omsg) )
| ~ spl3_3 ),
inference(forward_demodulation,[],[f9856,f4102]) ).
fof(f10836,definition,
( spl3_51
<=> ! [X1] : v_sko__urX(v_evs_H_H) = c_plus(X1,v_sko__urX(v_evs_H_H),tc_nat) ),
introduced(definition,[new_symbols(definition,[spl3_51])],[avatar_definition]) ).
fof(f10837,plain,
( ! [X1] : v_sko__urX(v_evs_H_H) = c_plus(X1,v_sko__urX(v_evs_H_H),tc_nat)
| ~ spl3_51 ),
inference(avatar_component_clause,[],[f10836]) ).
fof(f10843,plain,
( spl3_51
| spl3_20
| ~ spl3_3 ),
inference(avatar_split_clause,[],[f10497,f4100,f10311,f10836]) ).
fof(f10951,definition,
( spl3_61
<=> ! [X1] : v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs),c_Finite__Set_Ocard(c_SetInterval_OatMost(X1,tc_nat),tc_nat),tc_nat) ),
introduced(definition,[new_symbols(definition,[spl3_61])],[avatar_definition]) ).
fof(f10952,plain,
( ! [X1] : v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs),c_Finite__Set_Ocard(c_SetInterval_OatMost(X1,tc_nat),tc_nat),tc_nat)
| ~ spl3_61 ),
inference(avatar_component_clause,[],[f10951]) ).
fof(f11057,definition,
( spl3_71
<=> ! [X0] :
( ~ c_in(c_Message_Omsg_ONonce(c_plus(v_sko__urX(v_evs_H),X0,tc_nat)),sF2,tc_Message_Omsg)
| v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs_H),X0,tc_nat) ) ),
introduced(definition,[new_symbols(definition,[spl3_71])],[avatar_definition]) ).
fof(f11058,plain,
( ! [X0] :
( ~ c_in(c_Message_Omsg_ONonce(c_plus(v_sko__urX(v_evs_H),X0,tc_nat)),sF2,tc_Message_Omsg)
| v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs_H),X0,tc_nat) )
| ~ spl3_71 ),
inference(avatar_component_clause,[],[f11057]) ).
fof(f11081,plain,
( spl3_15
| spl3_71 ),
inference(avatar_split_clause,[],[f6716,f11057,f9703]) ).
fof(f11301,definition,
( spl3_126
<=> v_sko__urX(v_evs_H) = v_sko__urX(v_evs) ),
introduced(definition,[new_symbols(definition,[spl3_126])],[avatar_definition]) ).
fof(f11303,plain,
( v_sko__urX(v_evs_H) = v_sko__urX(v_evs)
| ~ spl3_126 ),
inference(avatar_component_clause,[],[f11301]) ).
fof(f11387,definition,
( spl3_142
<=> ! [X0] :
( v_sko__urX(v_evs_H) = c_plus(X0,v_sko__urX(v_evs_H_H),tc_nat)
| v_sko__urX(v_evs) = c_plus(X0,v_sko__urX(v_evs_H_H),tc_nat) ) ),
introduced(definition,[new_symbols(definition,[spl3_142])],[avatar_definition]) ).
fof(f11388,plain,
( ! [X0] :
( v_sko__urX(v_evs) = c_plus(X0,v_sko__urX(v_evs_H_H),tc_nat)
| v_sko__urX(v_evs_H) = c_plus(X0,v_sko__urX(v_evs_H_H),tc_nat) )
| ~ spl3_142 ),
inference(avatar_component_clause,[],[f11387]) ).
fof(f11412,definition,
( spl3_145
<=> ! [X1] : v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs_H),c_Finite__Set_Ocard(c_SetInterval_OatMost(X1,tc_nat),tc_nat),tc_nat) ),
introduced(definition,[new_symbols(definition,[spl3_145])],[avatar_definition]) ).
fof(f11413,plain,
( ! [X1] : v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs_H),c_Finite__Set_Ocard(c_SetInterval_OatMost(X1,tc_nat),tc_nat),tc_nat)
| ~ spl3_145 ),
inference(avatar_component_clause,[],[f11412]) ).
fof(f11566,plain,
! [X0] :
( v_sko__urX(v_evs_H) = v_sko__urX(v_evs)
| v_sko__urX(v_evs) = c_plus(X0,v_sko__urX(v_evs_H_H),tc_nat)
| v_sko__urX(v_evs_H) = c_plus(X0,v_sko__urX(v_evs_H_H),tc_nat) ),
inference(forward_demodulation,[],[f7583,f2350]) ).
fof(f11709,definition,
( spl3_198
<=> ! [X1] : v_sko__urX(v_evs_H) = c_plus(v_sko__urX(v_evs_H_H),c_Finite__Set_Ocard(c_SetInterval_OatMost(X1,tc_nat),tc_nat),tc_nat) ),
introduced(definition,[new_symbols(definition,[spl3_198])],[avatar_definition]) ).
fof(f11710,plain,
( ! [X1] : v_sko__urX(v_evs_H) = c_plus(v_sko__urX(v_evs_H_H),c_Finite__Set_Ocard(c_SetInterval_OatMost(X1,tc_nat),tc_nat),tc_nat)
| ~ spl3_198 ),
inference(avatar_component_clause,[],[f11709]) ).
fof(f11712,definition,
( spl3_199
<=> ! [X0] :
( ~ c_lessequals(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) = c_plus(v_sko__urX(v_evs),X0,tc_nat) ) ),
introduced(definition,[new_symbols(definition,[spl3_199])],[avatar_definition]) ).
fof(f11713,plain,
( ! [X0] :
( ~ c_lessequals(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) = c_plus(v_sko__urX(v_evs),X0,tc_nat) )
| ~ spl3_199 ),
inference(avatar_component_clause,[],[f11712]) ).
fof(f11714,plain,
( spl3_198
| spl3_199 ),
inference(avatar_split_clause,[],[f9152,f11712,f11709]) ).
fof(f11733,plain,
( spl3_142
| spl3_126 ),
inference(avatar_split_clause,[],[f11566,f11301,f11387]) ).
fof(f12250,plain,
( ~ c_lessequals(v_sko__urX(v_evs_H_H),v_sko__urX(v_evs_H_H),tc_nat)
| ~ spl3_25 ),
inference(superposition,[],[f4039,f10335]) ).
fof(f12728,plain,
( $false
| ~ spl3_25 ),
inference(forward_subsumption_resolution,[],[f12250,f4512]) ).
fof(f12729,plain,
~ spl3_25,
inference(avatar_contradiction_clause,[],[f12728]) ).
fof(f14162,plain,
( ! [X0] : ~ c_less(v_sko__urX(v_evs_H_H),X0,tc_nat)
| ~ spl3_51 ),
inference(superposition,[],[f2431,f10837]) ).
fof(f14270,plain,
( $false
| ~ spl3_51 ),
inference(resolution,[],[f14162,f3569]) ).
fof(f14272,plain,
~ spl3_51,
inference(avatar_contradiction_clause,[],[f14270]) ).
fof(f14516,plain,
( ! [X0] :
( v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs_H),X0,tc_nat)
| v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs_H),X0,tc_nat)
| v_sko__urX(v_evs_H) = c_plus(v_sko__urX(v_evs_H),X0,tc_nat) )
| ~ spl3_4
| ~ spl3_71 ),
inference(resolution,[],[f11058,f4105]) ).
fof(f14537,plain,
( ! [X0] :
( v_sko__urX(v_evs_H) = c_plus(v_sko__urX(v_evs_H),X0,tc_nat)
| v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs_H),X0,tc_nat) )
| ~ spl3_4
| ~ spl3_71 ),
inference(duplicate_literal_removal,[],[f14516]) ).
fof(f14826,plain,
( ! [X0] : ~ c_less(v_sko__urX(v_evs_H_H),c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat),tc_nat)
| ~ spl3_145 ),
inference(superposition,[],[f2432,f11413]) ).
fof(f14962,plain,
( ! [X0] : ~ c_less(v_sko__urX(v_evs_H),c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat),tc_nat)
| ~ spl3_198 ),
inference(superposition,[],[f2432,f11710]) ).
fof(f15204,plain,
( $false
| ~ spl3_198 ),
inference(resolution,[],[f14962,f3569]) ).
fof(f15208,plain,
~ spl3_198,
inference(avatar_contradiction_clause,[],[f15204]) ).
fof(f16743,plain,
( ! [X0] :
( ~ c_lessequals(v_sko__urX(v_evs_H),v_sko__urX(v_evs_H),tc_nat)
| v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs_H),c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat),tc_nat) )
| ~ spl3_4
| ~ spl3_71 ),
inference(superposition,[],[f4039,f14537]) ).
fof(f16763,plain,
( ! [X0] : v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs_H),c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat),tc_nat)
| ~ spl3_4
| ~ spl3_71 ),
inference(forward_subsumption_resolution,[],[f16743,f4512]) ).
fof(f16779,plain,
( spl3_145
| ~ spl3_4
| ~ spl3_71 ),
inference(avatar_split_clause,[],[f16763,f11057,f4104,f11412]) ).
fof(f17110,plain,
( $false
| ~ spl3_145 ),
inference(resolution,[],[f14826,f3569]) ).
fof(f17114,plain,
~ spl3_145,
inference(avatar_contradiction_clause,[],[f17110]) ).
fof(f17185,definition,
( spl3_209
<=> c_in(c_Message_Omsg_ONonce(v_sko__urX(v_evs)),sF1,tc_Message_Omsg) ),
introduced(definition,[new_symbols(definition,[spl3_209])],[avatar_definition]) ).
fof(f17186,plain,
( c_in(c_Message_Omsg_ONonce(v_sko__urX(v_evs)),sF1,tc_Message_Omsg)
| ~ spl3_209 ),
inference(avatar_component_clause,[],[f17185]) ).
fof(f17187,plain,
( ~ c_in(c_Message_Omsg_ONonce(v_sko__urX(v_evs)),sF1,tc_Message_Omsg)
| spl3_209 ),
inference(avatar_component_clause,[],[f17185]) ).
fof(f17208,plain,
( ! [X0] :
( ~ c_lessequals(v_sko__urX(v_evs_H_H),v_sko__urX(v_evs_H_H),tc_nat)
| v_sko__urX(v_evs_H) = c_plus(v_sko__urX(v_evs),X0,tc_nat) )
| ~ spl3_15
| ~ spl3_199 ),
inference(forward_demodulation,[],[f11713,f9704]) ).
fof(f17370,plain,
( ! [X0] : v_sko__urX(v_evs_H) = c_plus(v_sko__urX(v_evs),X0,tc_nat)
| ~ spl3_15
| ~ spl3_199 ),
inference(forward_subsumption_resolution,[],[f17208,f4512]) ).
fof(f17438,plain,
( v_sko__urX(v_evs_H) = v_sko__urX(v_evs_H_H)
| ~ spl3_15
| ~ spl3_199 ),
inference(forward_demodulation,[],[f17370,f9704]) ).
fof(f17490,plain,
( $false
| spl3_3
| ~ spl3_15
| ~ spl3_199 ),
inference(forward_subsumption_resolution,[],[f17438,f4101]) ).
fof(f17491,plain,
( spl3_3
| ~ spl3_15
| ~ spl3_199 ),
inference(avatar_contradiction_clause,[],[f17490]) ).
fof(f17535,plain,
( v_sko__urX(v_evs) = v_sko__urX(v_evs_H_H)
| ~ spl3_3
| ~ spl3_126 ),
inference(forward_demodulation,[],[f11303,f4102]) ).
fof(f17725,plain,
( $false
| ~ spl3_3
| spl3_5
| ~ spl3_126 ),
inference(forward_subsumption_resolution,[],[f17535,f4109]) ).
fof(f17726,plain,
( ~ spl3_3
| spl3_5
| ~ spl3_126 ),
inference(avatar_contradiction_clause,[],[f17725]) ).
fof(f18312,plain,
( ! [X0] :
( c_in(c_Message_Omsg_ONonce(X0),sF2,tc_Message_Omsg)
| v_sko__urX(v_evs) = X0
| v_sko__urX(v_evs) = v_sko__urX(v_evs_H_H)
| v_sko__urX(v_evs_H_H) = X0 )
| spl3_209 ),
inference(resolution,[],[f17187,f4085]) ).
fof(f18320,plain,
( ! [X0] :
( c_in(c_Message_Omsg_ONonce(X0),sF2,tc_Message_Omsg)
| v_sko__urX(v_evs) = X0
| v_sko__urX(v_evs_H_H) = X0 )
| spl3_5
| spl3_209 ),
inference(forward_subsumption_resolution,[],[f18312,f4109]) ).
fof(f18323,plain,
( ! [X0] :
( v_sko__urX(v_evs) = 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) )
| spl3_5
| spl3_209 ),
inference(resolution,[],[f18320,f3979]) ).
fof(f18810,plain,
( ~ c_in(c_Message_Omsg_ONonce(v_sko__urX(v_evs)),sF1,tc_Message_Omsg)
| v_sko__urX(v_evs) = v_sko__urX(v_evs_H_H)
| ~ spl3_20 ),
inference(superposition,[],[f10312,f2350]) ).
fof(f19109,plain,
( ! [X0] :
( c_lessequals(v_sko__urX(v_evs_H_H),v_sko__urX(v_evs),tc_nat)
| v_sko__urX(v_evs_H) = c_plus(X0,v_sko__urX(v_evs_H_H),tc_nat) )
| ~ spl3_142 ),
inference(superposition,[],[f3559,f11388]) ).
fof(f19888,plain,
( ~ c_lessequals(v_sko__urX(v_evs_H_H),v_sko__urX(v_evs),tc_nat)
| ~ spl3_61 ),
inference(superposition,[],[f4039,f10952]) ).
fof(f19987,plain,
( ! [X0] :
( v_sko__urX(v_evs_H_H) = c_plus(X0,v_sko__urX(v_evs_H_H),tc_nat)
| c_lessequals(v_sko__urX(v_evs_H_H),v_sko__urX(v_evs),tc_nat) )
| ~ spl3_3
| ~ spl3_142 ),
inference(forward_demodulation,[],[f19109,f4102]) ).
fof(f20007,plain,
( ! [X0] : v_sko__urX(v_evs_H_H) = c_plus(X0,v_sko__urX(v_evs_H_H),tc_nat)
| ~ spl3_3
| ~ spl3_61
| ~ spl3_142 ),
inference(forward_subsumption_resolution,[],[f19987,f19888]) ).
fof(f20017,plain,
( spl3_51
| ~ spl3_3
| ~ spl3_61
| ~ spl3_142 ),
inference(avatar_split_clause,[],[f20007,f11387,f10951,f4100,f10836]) ).
fof(f20238,plain,
( ! [X0] :
( ~ c_lessequals(v_sko__urX(v_evs),v_sko__urX(v_evs),tc_nat)
| v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs),c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat),tc_nat) )
| spl3_5
| spl3_209 ),
inference(superposition,[],[f4039,f18323]) ).
fof(f20260,plain,
( ! [X0] : v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs),c_Finite__Set_Ocard(c_SetInterval_OatMost(X0,tc_nat),tc_nat),tc_nat)
| spl3_5
| spl3_209 ),
inference(forward_subsumption_resolution,[],[f20238,f4512]) ).
fof(f20264,plain,
( spl3_61
| spl3_5
| spl3_209 ),
inference(avatar_split_clause,[],[f20260,f17185,f4108,f10951]) ).
fof(f20265,plain,
( v_sko__urX(v_evs) = v_sko__urX(v_evs_H_H)
| ~ spl3_20
| ~ spl3_209 ),
inference(forward_subsumption_resolution,[],[f18810,f17186]) ).
fof(f20310,plain,
( $false
| spl3_5
| ~ spl3_20
| ~ spl3_209 ),
inference(forward_subsumption_resolution,[],[f20265,f4109]) ).
fof(f20311,plain,
( spl3_5
| ~ spl3_20
| ~ spl3_209 ),
inference(avatar_contradiction_clause,[],[f20310]) ).
fof(f22520,plain,
! [X0,X1] :
( c_plus(v_sko__urX(v_evs),X0,tc_nat) = c_plus(v_sko__urX(v_evs_H),X1,tc_nat)
| c_plus(v_sko__urX(v_evs_H),X1,tc_nat) = c_plus(c_Finite__Set_Ocard(c_SetInterval_OatMost(c_plus(v_sko__urX(v_evs),X0,tc_nat),tc_nat),tc_nat),v_sko__urX(v_evs_H_H),tc_nat) ),
inference(resolution,[],[f6101,f3569]) ).
fof(f22560,plain,
( ! [X0,X1] :
( c_plus(v_sko__urX(v_evs),X0,tc_nat) = c_plus(v_sko__urX(v_evs_H_H),X1,tc_nat)
| c_plus(v_sko__urX(v_evs_H),X1,tc_nat) = c_plus(c_Finite__Set_Ocard(c_SetInterval_OatMost(c_plus(v_sko__urX(v_evs),X0,tc_nat),tc_nat),tc_nat),v_sko__urX(v_evs_H_H),tc_nat) )
| ~ spl3_3 ),
inference(forward_demodulation,[],[f22520,f4102]) ).
fof(f22579,plain,
( ! [X0,X1] :
( c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat) = c_plus(v_sko__urX(v_evs_H_H),X1,tc_nat)
| c_plus(v_sko__urX(v_evs_H),X1,tc_nat) = c_plus(c_Finite__Set_Ocard(c_SetInterval_OatMost(c_plus(v_sko__urX(v_evs),X0,tc_nat),tc_nat),tc_nat),v_sko__urX(v_evs_H_H),tc_nat) )
| ~ spl3_3
| ~ spl3_5 ),
inference(forward_demodulation,[],[f22560,f4110]) ).
fof(f22597,plain,
( ! [X0,X1] :
( c_plus(v_sko__urX(v_evs_H),X1,tc_nat) = c_plus(c_plus(v_sko__urX(v_evs),X0,tc_nat),c_Finite__Set_Ocard(c_SetInterval_OatMost(v_sko__urX(v_evs_H_H),tc_nat),tc_nat),tc_nat)
| c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat) = c_plus(v_sko__urX(v_evs_H_H),X1,tc_nat) )
| ~ spl3_3
| ~ spl3_5 ),
inference(forward_demodulation,[],[f22579,f3853]) ).
fof(f22605,plain,
( ! [X0,X1] :
( c_plus(v_sko__urX(v_evs_H),X1,tc_nat) = c_plus(c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat),c_Finite__Set_Ocard(c_SetInterval_OatMost(v_sko__urX(v_evs_H_H),tc_nat),tc_nat),tc_nat)
| c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat) = c_plus(v_sko__urX(v_evs_H_H),X1,tc_nat) )
| ~ spl3_3
| ~ spl3_5 ),
inference(forward_demodulation,[],[f22597,f4110]) ).
fof(f22607,plain,
( ! [X0,X1] :
( c_plus(v_sko__urX(v_evs_H_H),X1,tc_nat) = c_plus(c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat),c_Finite__Set_Ocard(c_SetInterval_OatMost(v_sko__urX(v_evs_H_H),tc_nat),tc_nat),tc_nat)
| c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat) = c_plus(v_sko__urX(v_evs_H_H),X1,tc_nat) )
| ~ spl3_3
| ~ spl3_5 ),
inference(forward_demodulation,[],[f22605,f4102]) ).
fof(f28791,plain,
( ! [X0,X1] :
( ~ c_lessequals(c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat),c_plus(v_sko__urX(v_evs_H_H),X1,tc_nat),tc_nat)
| c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat) = c_plus(v_sko__urX(v_evs_H_H),X1,tc_nat) )
| ~ spl3_3
| ~ spl3_5 ),
inference(superposition,[],[f4039,f22607]) ).
fof(f28794,plain,
( ! [X0,X1] :
( c_lessequals(c_plus(v_sko__urX(v_evs_H_H),X1,tc_nat),c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat),tc_nat)
| c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat) = c_plus(v_sko__urX(v_evs_H_H),X1,tc_nat) )
| ~ spl3_3
| ~ spl3_5 ),
inference(superposition,[],[f3558,f22607]) ).
fof(f28805,plain,
( ! [X0,X1] : c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat) = c_plus(v_sko__urX(v_evs_H_H),X1,tc_nat)
| ~ spl3_3
| ~ spl3_5 ),
inference(forward_subsumption_resolution,[],[f28791,f28794]) ).
fof(f29115,plain,
( ! [X0] : v_sko__urX(v_evs_H_H) = c_plus(v_sko__urX(v_evs_H_H),X0,tc_nat)
| ~ spl3_3
| ~ spl3_5 ),
inference(superposition,[],[f2350,f28805]) ).
fof(f29159,plain,
( spl3_25
| ~ spl3_3
| ~ spl3_5 ),
inference(avatar_split_clause,[],[f29115,f4108,f4100,f10334]) ).
cnf(s4,plain,
( spl3_3
| spl3_4 ),
inference(sat_conversion,[],[f4106]) ).
cnf(s117,plain,
( ~ spl3_3
| spl3_20
| spl3_51 ),
inference(sat_conversion,[],[f10843]) ).
cnf(s184,plain,
( spl3_15
| spl3_71 ),
inference(sat_conversion,[],[f11081]) ).
cnf(s408,plain,
( spl3_198
| spl3_199 ),
inference(sat_conversion,[],[f11714]) ).
cnf(s415,plain,
( spl3_126
| spl3_142 ),
inference(sat_conversion,[],[f11733]) ).
cnf(s451,plain,
~ spl3_25,
inference(sat_conversion,[],[f12729]) ).
cnf(s516,plain,
~ spl3_51,
inference(sat_conversion,[],[f14272]) ).
cnf(s528,plain,
~ spl3_198,
inference(sat_conversion,[],[f15208]) ).
cnf(s539,plain,
( ~ spl3_4
| ~ spl3_71
| spl3_145 ),
inference(sat_conversion,[],[f16779]) ).
cnf(s551,plain,
~ spl3_145,
inference(sat_conversion,[],[f17114]) ).
cnf(s575,plain,
( spl3_3
| ~ spl3_15
| ~ spl3_199 ),
inference(sat_conversion,[],[f17491]) ).
cnf(s586,plain,
( ~ spl3_3
| spl3_5
| ~ spl3_126 ),
inference(sat_conversion,[],[f17726]) ).
cnf(s622,plain,
( ~ spl3_3
| spl3_51
| ~ spl3_61
| ~ spl3_142 ),
inference(sat_conversion,[],[f20017]) ).
cnf(s626,plain,
( spl3_5
| spl3_61
| spl3_209 ),
inference(sat_conversion,[],[f20264]) ).
cnf(s629,plain,
( spl3_5
| ~ spl3_20
| ~ spl3_209 ),
inference(sat_conversion,[],[f20311]) ).
cnf(s675,plain,
( ~ spl3_3
| ~ spl3_5
| spl3_25 ),
inference(sat_conversion,[],[f29159]) ).
cnf(s683,plain,
( ~ spl3_4
| ~ spl3_71 ),
inference(rat,[],[s539,s551]) ).
cnf(s693,plain,
spl3_199,
inference(rat,[],[s408,s528]) ).
cnf(s709,plain,
( ~ spl3_3
| spl3_20 ),
inference(rat,[],[s117,s516]) ).
cnf(s734,plain,
spl3_3,
inference(rat,[],[s683,s184,s4,s575,s693]) ).
cnf(s735,plain,
~ spl3_5,
inference(rat,[],[s675,s451,s734]) ).
cnf(s746,plain,
spl3_20,
inference(rat,[],[s709,s734]) ).
cnf(s752,plain,
~ spl3_126,
inference(rat,[],[s586,s735,s734]) ).
cnf(s754,plain,
~ spl3_209,
inference(rat,[],[s629,s735,s746]) ).
cnf(s756,plain,
spl3_142,
inference(rat,[],[s415,s752]) ).
cnf(s760,plain,
spl3_61,
inference(rat,[],[s626,s735,s754]) ).
cnf(s766,plain,
$false,
inference(rat,[],[s622,s734,s516,s756,s760]) ).
fof(f29208,plain,
$false,
inference(avatar_sat_refutation,[],[s766]) ).
%------------------------------------------------------------------------------
%----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/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n008.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 10:25:25 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.22 Running first-order theorem proving
% 0.09/0.22 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
% 10.78/2.21 % (2158532)Input is clausal, will run a generic CNF schedule.
% 10.78/2.21 % (2158538)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=777923524:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.78/2.21 % (2158537)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=1865071869:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.78/2.21 % (2158542)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3238949531:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.78/2.21 % (2158540)lrs+10_1_sil=8000:sp=occurrence:random_seed=316640559:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.78/2.21 % (2158541)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1130692000:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.78/2.21 % (2158539)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=2547997860:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.78/2.21 % (2158543)dis-21_1_sil=8000:lcm=predicate:random_seed=1953310292: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)
% 10.78/2.21 % (2158541)Instruction limit reached!
% 10.78/2.21 % (2158541)------------------------------
% 10.78/2.21 % (2158541)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.78/2.21 % (2158541)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.78/2.21 % (2158541)CaDiCaL version: 2.1.3
% 10.78/2.21 % (2158541)Termination reason: Instruction limit
% 10.78/2.21 % (2158541)Termination phase: Saturation
% 10.78/2.21 % (2158541)Time elapsed: 0.071 s
% 10.78/2.21 % (2158541)Peak memory usage: 91 MB
% 10.78/2.21 % (2158541)Instructions burned: 114 (million)
% 10.78/2.21 % (2158540)Instruction limit reached!
% 10.78/2.21 % (2158540)------------------------------
% 10.78/2.21 % (2158540)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.78/2.21 % (2158540)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.78/2.21 % (2158540)CaDiCaL version: 2.1.3
% 10.78/2.21 % (2158540)Termination reason: Instruction limit
% 10.78/2.21 % (2158540)Termination phase: Saturation
% 10.78/2.21 % (2158540)Time elapsed: 0.073 s
% 10.78/2.21 % (2158540)Peak memory usage: 91 MB
% 10.78/2.21 % (2158540)Instructions burned: 107 (million)
% 10.78/2.21 % (2158543)Instruction limit reached!
% 10.78/2.21 % (2158543)------------------------------
% 10.78/2.21 % (2158543)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.78/2.21 % (2158543)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.78/2.21 % (2158543)CaDiCaL version: 2.1.3
% 10.78/2.21 % (2158543)Termination reason: Instruction limit
% 10.78/2.21 % (2158543)Termination phase: Saturation
% 10.78/2.21 % (2158543)Time elapsed: 0.062 s
% 10.78/2.21 % (2158543)Peak memory usage: 91 MB
% 10.78/2.21 % (2158543)Instructions burned: 118 (million)
% 10.78/2.21 % (2158542)Instruction limit reached!
% 10.78/2.21 % (2158542)------------------------------
% 10.78/2.21 % (2158542)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.78/2.21 % (2158542)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.78/2.21 % (2158542)CaDiCaL version: 2.1.3
% 10.78/2.21 % (2158542)Termination reason: Instruction limit
% 10.78/2.21 % (2158542)Termination phase: Saturation
% 10.78/2.21 % (2158542)Time elapsed: 0.107 s
% 10.78/2.21 % (2158542)Peak memory usage: 91 MB
% 10.78/2.21 % (2158542)Instructions burned: 182 (million)
% 10.78/2.21 % (2158552)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1599785443: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)
% 10.78/2.21 % (2158553)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=1372137124:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 10.78/2.21 % (2158551)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=488464190:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 10.78/2.21 % (2158551)Refutation not found, incomplete strategy
% 10.78/2.21 % (2158551)------------------------------
% 10.78/2.21 % (2158551)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.23/3.88 % (2158551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.23/3.88 % (2158551)CaDiCaL version: 2.1.3
% 21.23/3.88 % (2158551)Termination reason: Refutation not found, incomplete strategy
% 21.23/3.88 % (2158551)Time elapsed: 0.012 s
% 21.23/3.88 % (2158551)Peak memory usage: 90 MB
% 21.23/3.88 % (2158551)Instructions burned: 17 (million)
% 21.23/3.88 % (2158552)Refutation not found, incomplete strategy
% 21.23/3.88 % (2158552)------------------------------
% 21.23/3.88 % (2158552)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.23/3.88 % (2158552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.23/3.88 % (2158552)CaDiCaL version: 2.1.3
% 21.23/3.88 % (2158552)Termination reason: Refutation not found, incomplete strategy
% 21.23/3.88 % (2158552)Time elapsed: 0.032 s
% 21.23/3.88 % (2158552)Peak memory usage: 91 MB
% 21.23/3.88 % (2158552)Instructions burned: 53 (million)
% 21.23/3.88 % (2158553)Refutation not found, incomplete strategy
% 21.23/3.88 % (2158553)------------------------------
% 21.23/3.88 % (2158553)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.23/3.88 % (2158553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.23/3.88 % (2158553)CaDiCaL version: 2.1.3
% 21.23/3.88 % (2158553)Termination reason: Refutation not found, incomplete strategy
% 21.23/3.88 % (2158553)Time elapsed: 0.036 s
% 21.23/3.88 % (2158553)Peak memory usage: 90 MB
% 21.23/3.88 % (2158553)Instructions burned: 58 (million)
% 21.23/3.88 % (2158554)lrs+10_64_to=lpo:sil=8000:random_seed=4009731817:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 21.23/3.88 % (2158554)Instruction limit reached!
% 21.23/3.88 % (2158554)------------------------------
% 21.23/3.88 % (2158554)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.23/3.88 % (2158554)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.23/3.88 % (2158554)CaDiCaL version: 2.1.3
% 21.23/3.88 % (2158554)Termination reason: Instruction limit
% 21.23/3.88 % (2158554)Termination phase: Saturation
% 21.23/3.88 % (2158554)Time elapsed: 0.076 s
% 21.23/3.88 % (2158554)Peak memory usage: 91 MB
% 21.23/3.88 % (2158554)Instructions burned: 129 (million)
% 21.23/3.88 % (2158559)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2065454989:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 21.23/3.88 % (2158551)------------------------------
% 21.23/3.88 % (2158551)------------------------------
% 21.23/3.88 % (2158552)------------------------------
% 21.23/3.88 % (2158552)------------------------------
% 21.23/3.88 % (2158553)------------------------------
% 21.23/3.88 % (2158553)------------------------------
% 21.23/3.88 % (2158559)Instruction limit reached!
% 21.23/3.88 % (2158559)------------------------------
% 21.23/3.88 % (2158559)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.23/3.88 % (2158559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.23/3.88 % (2158559)CaDiCaL version: 2.1.3
% 21.23/3.88 % (2158559)Termination reason: Instruction limit
% 21.23/3.88 % (2158559)Termination phase: Saturation
% 21.23/3.88 % (2158559)Time elapsed: 0.113 s
% 21.23/3.88 % (2158559)Peak memory usage: 92 MB
% 21.23/3.88 % (2158559)Instructions burned: 194 (million)
% 21.23/3.88 % (2158561)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=4044322420:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 21.23/3.88 % (2158562)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=4076931290:i=3394:sd=4:ss=included:sgt=64_2992 on theBenchmark for (2992ds/3394Mi)
% 21.23/3.88 % (2158563)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=1005908850:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2992 on theBenchmark for (2992ds/106Mi)
% 21.23/3.88 % (2158563)Instruction limit reached!
% 21.23/3.88 % (2158563)------------------------------
% 21.23/3.88 % (2158563)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 21.23/3.88 % (2158563)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 21.23/3.88 % (2158563)CaDiCaL version: 2.1.3
% 21.23/3.88 % (2158563)Termination reason: Instruction limit
% 21.23/3.88 % (2158563)Termination phase: Saturation
% 21.23/3.88 % (2158563)Time elapsed: 0.061 s
% 21.23/3.88 % (2158563)Peak memory usage: 90 MB
% 21.23/3.88 % (2158563)Instructions burned: 106 (million)
% 21.23/3.88 % (2158561)Instruction limit reached!
% 21.23/3.88 % (2158561)------------------------------
% 22.08/3.97 % (2158561)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.08/3.97 % (2158561)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.08/3.97 % (2158561)CaDiCaL version: 2.1.3
% 22.08/3.97 % (2158561)Termination reason: Instruction limit
% 22.08/3.97 % (2158561)Termination phase: Saturation
% 22.08/3.97 % (2158561)Time elapsed: 0.083 s
% 22.08/3.97 % (2158561)Peak memory usage: 92 MB
% 22.08/3.97 % (2158561)Instructions burned: 157 (million)
% 22.08/3.97 % (2158564)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1249070371:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 22.08/3.97 % (2158564)Instruction limit reached!
% 22.08/3.97 % (2158564)------------------------------
% 22.08/3.97 % (2158564)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.08/3.97 % (2158564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.08/3.97 % (2158564)CaDiCaL version: 2.1.3
% 22.08/3.97 % (2158564)Termination reason: Instruction limit
% 22.08/3.97 % (2158564)Termination phase: Saturation
% 22.08/3.97 % (2158564)Time elapsed: 0.061 s
% 22.08/3.97 % (2158564)Peak memory usage: 92 MB
% 22.08/3.97 % (2158564)Instructions burned: 109 (million)
% 22.08/3.97 % (2158568)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=811021861:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2990 on theBenchmark for (2990ds/242Mi)
% 22.08/3.97 % (2158569)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1109395339:cond=fast:i=5208:av=off_2990 on theBenchmark for (2990ds/5208Mi)
% 22.08/3.97 % (2158571)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=1250264902:i=134:sd=2:doe=on:ss=axioms:sgt=14_2990 on theBenchmark for (2990ds/134Mi)
% 22.08/3.97 % (2158568)Instruction limit reached!
% 22.08/3.97 % (2158568)------------------------------
% 22.08/3.97 % (2158568)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.08/3.97 % (2158568)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.08/3.97 % (2158568)CaDiCaL version: 2.1.3
% 22.08/3.97 % (2158568)Termination reason: Instruction limit
% 22.08/3.97 % (2158568)Termination phase: Saturation
% 22.08/3.97 % (2158568)Time elapsed: 0.129 s
% 22.08/3.97 % (2158568)Peak memory usage: 91 MB
% 22.08/3.97 % (2158568)Instructions burned: 243 (million)
% 22.08/3.97 % (2158571)Instruction limit reached!
% 22.08/3.97 % (2158571)------------------------------
% 22.08/3.97 % (2158571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.08/3.97 % (2158571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.08/3.97 % (2158571)CaDiCaL version: 2.1.3
% 22.08/3.97 % (2158571)Termination reason: Instruction limit
% 22.08/3.97 % (2158571)Termination phase: Saturation
% 22.08/3.97 % (2158571)Time elapsed: 0.087 s
% 22.08/3.97 % (2158571)Peak memory usage: 92 MB
% 22.08/3.97 % (2158571)Instructions burned: 135 (million)
% 22.08/3.97 % (2158575)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=1402457881:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 22.08/3.97 % (2158576)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=3910108087:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 22.08/3.97 % (2158576)Instruction limit reached!
% 22.08/3.97 % (2158576)------------------------------
% 22.08/3.97 % (2158576)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.08/3.97 % (2158576)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.08/3.97 % (2158576)CaDiCaL version: 2.1.3
% 22.08/3.97 % (2158576)Termination reason: Instruction limit
% 22.08/3.97 % (2158576)Termination phase: Saturation
% 22.08/3.97 % (2158576)Time elapsed: 0.115 s
% 22.08/3.97 % (2158576)Peak memory usage: 92 MB
% 22.08/3.97 % (2158576)Instructions burned: 191 (million)
% 22.08/3.97 % (2158575)Instruction limit reached!
% 22.08/3.97 % (2158575)------------------------------
% 22.08/3.97 % (2158575)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.08/3.97 % (2158575)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.08/3.97 % (2158575)CaDiCaL version: 2.1.3
% 22.08/3.97 % (2158575)Termination reason: Instruction limit
% 22.08/3.97 % (2158575)Termination phase: Saturation
% 22.08/3.97 % (2158575)Time elapsed: 0.266 s
% 22.08/3.97 % (2158575)Peak memory usage: 100 MB
% 22.08/3.97 % (2158575)Instructions burned: 500 (million)
% 22.08/3.97 % (2158579)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2934836229:i=264:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/264Mi)
% 22.08/3.97 % (2158580)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=1921652571:cond=on:i=156:bs=on:gtg=exists_all:er=known_2984 on theBenchmark for (2984ds/156Mi)
% 22.08/3.97 % (2158579)Instruction limit reached!
% 22.08/3.97 % (2158579)------------------------------
% 22.08/3.97 % (2158579)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.08/3.97 % (2158579)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.08/3.97 % (2158579)CaDiCaL version: 2.1.3
% 22.08/3.97 % (2158579)Termination reason: Instruction limit
% 22.08/3.97 % (2158579)Termination phase: Saturation
% 22.08/3.97 % (2158579)Time elapsed: 0.124 s
% 22.08/3.97 % (2158579)Peak memory usage: 94 MB
% 22.08/3.97 % (2158579)Instructions burned: 267 (million)
% 22.08/3.97 % (2158580)Instruction limit reached!
% 22.08/3.97 % (2158580)------------------------------
% 22.08/3.97 % (2158580)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.08/3.97 % (2158580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.08/3.97 % (2158580)CaDiCaL version: 2.1.3
% 22.08/3.97 % (2158580)Termination reason: Instruction limit
% 22.08/3.97 % (2158580)Termination phase: Saturation
% 22.08/3.97 % (2158580)Time elapsed: 0.086 s
% 22.08/3.97 % (2158580)Peak memory usage: 91 MB
% 22.08/3.97 % (2158580)Instructions burned: 156 (million)
% 22.08/3.97 % (2158583)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=3738334812:i=3256:kws=precedence:bd=preordered:av=off_2982 on theBenchmark for (2982ds/3256Mi)
% 22.08/3.97 % (2158584)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=185658070:i=537:av=off:ss=included_2982 on theBenchmark for (2982ds/537Mi)
% 22.08/3.97 % (2158584)Instruction limit reached!
% 22.08/3.97 % (2158584)------------------------------
% 22.08/3.97 % (2158584)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.08/3.97 % (2158584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.08/3.97 % (2158584)CaDiCaL version: 2.1.3
% 22.08/3.97 % (2158584)Termination reason: Instruction limit
% 22.08/3.97 % (2158584)Termination phase: Saturation
% 22.08/3.97 % (2158584)Time elapsed: 0.284 s
% 22.08/3.97 % (2158584)Peak memory usage: 93 MB
% 22.08/3.97 % (2158584)Instructions burned: 540 (million)
% 22.08/3.97 % (2158587)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=1867010432:i=180:bd=preordered:av=off_2978 on theBenchmark for (2978ds/180Mi)
% 22.08/3.97 % (2158587)Instruction limit reached!
% 22.08/3.97 % (2158587)------------------------------
% 22.08/3.97 % (2158587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.08/3.97 % (2158587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.08/3.97 % (2158587)CaDiCaL version: 2.1.3
% 22.08/3.97 % (2158587)Termination reason: Instruction limit
% 22.08/3.97 % (2158587)Termination phase: Saturation
% 22.08/3.97 % (2158587)Time elapsed: 0.103 s
% 22.08/3.97 % (2158587)Peak memory usage: 92 MB
% 22.08/3.97 % (2158587)Instructions burned: 181 (million)
% 22.08/3.97 % (2158589)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=112106867:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2975 on theBenchmark for (2975ds/10307Mi)
% 22.08/3.97 % (2158562)Instruction limit reached!
% 22.08/3.97 % (2158562)------------------------------
% 22.08/3.97 % (2158562)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.08/3.97 % (2158562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.08/3.97 % (2158562)CaDiCaL version: 2.1.3
% 22.08/3.97 % (2158562)Termination reason: Instruction limit
% 22.08/3.97 % (2158562)Termination phase: Saturation
% 22.08/3.97 % (2158562)Time elapsed: 2.005 s
% 22.08/3.97 % (2158562)Peak memory usage: 148 MB
% 22.08/3.97 % (2158562)Instructions burned: 3394 (million)
% 22.08/3.97 % (2158591)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=1125850662:i=412:gtgl=4:gtg=exists_all_2971 on theBenchmark for (2971ds/412Mi)
% 22.08/3.97 % (2158537)First to succeed.
% 22.08/3.97 % (2158537)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2158532"
% 22.08/3.97 % (2158591)Instruction limit reached!
% 22.08/3.97 % (2158591)------------------------------
% 22.08/3.97 % (2158591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.08/3.97 % (2158591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.08/3.97 % (2158591)CaDiCaL version: 2.1.3
% 22.08/3.97 % (2158591)Termination reason: Instruction limit
% 22.08/3.97 % (2158591)Termination phase: Saturation
% 22.08/3.97 % (2158591)Time elapsed: 0.229 s
% 22.08/3.97 % (2158591)Peak memory usage: 95 MB
% 22.08/3.97 % (2158591)Instructions burned: 412 (million)
% 22.08/3.97 % (2158537)Refutation found. Thanks to Tanya!
% 22.08/3.97 % SZS status Unsatisfiable for theBenchmark
% 22.08/3.97 % SZS output start Proof for theBenchmark
% See solution above
% 23.62/4.17 % (2158537)------------------------------
% 23.62/4.17 % (2158537)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 23.62/4.17 % (2158537)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 23.62/4.17 % (2158537)CaDiCaL version: 2.1.3
% 23.62/4.17 % (2158537)Termination reason: Refutation
% 23.62/4.17 % (2158537)Time elapsed: 2.835 s
% 23.62/4.17 % (2158537)Peak memory usage: 156 MB
% 23.62/4.17 % (2158537)Instructions burned: 5095 (million)
% 23.62/4.17 % (2158537)------------------------------
% 23.62/4.17 % (2158537)------------------------------
% 23.62/4.17 % (2158532)Success in time 3.317 s
% 23.62/4.17 % Vampire exiting
%------------------------------------------------------------------------------