%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SWV883-1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 01:19:43 PM UTC 2026
% Result : Unsatisfiable 6.10s 1.69s
% Output : Refutation 7.70s
% Verified :
% SZS Type : Refutation
% Derivation depth : 25
% Number of leaves : 49
% Syntax : Number of formulae : 187 ( 84 unt; 25 def)
% Number of atoms : 346 ( 107 equ)
% Maximal formula atoms : 5 ( 1 avg)
% Number of connectives : 299 ( 140 ~; 151 |; 0 &)
% ( 8 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 6 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 9 prp; 0-3 aty)
% Number of functors : 42 ( 42 usr; 24 con; 0-4 aty)
% Number of variables : 91 ( 0 sgn 91 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f23,axiom,
! [X0] : c_Suc(X0) = c_HOL_Oplus__class_Oplus(X0,c_HOL_Oone__class_Oone(tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_Suc__eq__plus1_0) ).
fof(f454,axiom,
! [X2,X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(X0,X1,tc_nat),X2,tc_nat) = c_HOL_Ominus__class_Ominus(X0,c_HOL_Oplus__class_Oplus(X1,X2,tc_nat),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_diff__diff__left_0) ).
fof(f462,axiom,
! [X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Oplus__class_Oplus(X0,X1,tc_nat),X0,tc_nat) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_diff__add__inverse_0) ).
fof(f470,axiom,
! [X0,X1] :
( ~ c_lessequals(X0,X1,tc_nat)
| c_HOL_Oplus__class_Oplus(X0,c_HOL_Ominus__class_Ominus(X1,X0,tc_nat),tc_nat) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_le__add__diff__inverse_0) ).
fof(f485,axiom,
! [X0] :
( v_wt(c_Option_Othe(c_Com_Obody(X0),tc_Com_Ocom))
| ~ c_in(X0,v_U,tc_Com_Opname) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_assms_I4_J_0) ).
fof(f519,axiom,
! [X0,X1] :
( c_Finite__Set_Ocard(X0,X1) != c_HOL_Ozero__class_Ozero(tc_nat)
| ~ c_Finite__Set_Ofinite(X0,X1)
| X0 = c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_card__eq__0__iff_0) ).
fof(f520,plain,
! [X0,X1] :
( c_HOL_Ozero__class_Ozero(tc_nat) != c_Finite__Set_Ocard(X0,X1)
| ~ c_Finite__Set_Ofinite(X0,X1)
| c_Orderings_Obot__class_Obot(tc_fun(X1,tc_bool)) = X0 ),
inference(reorient_equations,[],[f519]) ).
fof(f528,axiom,
! [X0,X1] :
( ~ hBOOL(hAPP(hAPP(v_P,c_Set_Oinsert(hAPP(v_mgt__call,X1),X0,t_a)),c_Set_Oinsert(v_mgt(c_Option_Othe(c_Com_Obody(X1),tc_Com_Ocom)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a)))
| hBOOL(hAPP(hAPP(v_P,X0),c_Set_Oinsert(hAPP(v_mgt__call,X1),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_assms_I2_J_0) ).
fof(f538,axiom,
! [X2,X0,X1] :
( c_in(X0,X1,X2)
| c_Finite__Set_Ocard(c_Set_Oinsert(X0,X1,X2),X2) = c_Suc(c_Finite__Set_Ocard(X1,X2))
| c_Finite__Set_Ocard(X1,X2) = c_HOL_Ozero__class_Ozero(tc_nat) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_card__Suc__eq_4) ).
fof(f539,plain,
! [X2,X0,X1] :
( c_in(X0,X1,X2)
| c_Finite__Set_Ocard(c_Set_Oinsert(X0,X1,X2),X2) = c_Suc(c_Finite__Set_Ocard(X1,X2))
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Finite__Set_Ocard(X1,X2) ),
inference(reorient_equations,[],[f538]) ).
fof(f566,axiom,
! [X2,X0,X1] :
( ~ c_lessequals(X0,X2,tc_fun(X1,tc_bool))
| c_Finite__Set_Ofinite(X0,X1)
| ~ c_Finite__Set_Ofinite(X2,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_rev__finite__subset_0) ).
fof(f588,axiom,
! [X2,X3,X0,X1] :
( c_lessequals(c_Set_Oinsert(X0,X1,X2),X3,tc_fun(X2,tc_bool))
| ~ c_lessequals(X1,X3,tc_fun(X2,tc_bool))
| ~ c_in(X0,X3,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_insert__subset_2) ).
fof(f608,axiom,
! [X2,X3,X0,X1] :
( c_Finite__Set_Ofinite(c_Set_Oimage(X0,X1,X2,X3),X3)
| ~ c_Finite__Set_Ofinite(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_finite__imageI_0) ).
fof(f650,axiom,
! [X2,X0,X1] :
( c_Finite__Set_Ocard(c_Set_Oinsert(X0,X1,X2),X2) = c_Suc(c_Finite__Set_Ocard(X1,X2))
| c_in(X0,X1,X2)
| ~ c_Finite__Set_Ofinite(X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_card__insert__if_1) ).
fof(f663,axiom,
! [X0,X1] : c_lessequals(c_HOL_Ominus__class_Ominus(X0,X1,tc_nat),X0,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_diff__le__self_0) ).
fof(f668,axiom,
! [X2,X0,X1] : c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(X0,X1,tc_nat),X2,tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(X0,X2,tc_nat),X1,tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_diff__commute_0) ).
fof(f691,axiom,
! [X0,X1] :
( ~ c_lessequals(X1,X0,tc_nat)
| c_HOL_Ominus__class_Ominus(X0,c_HOL_Ominus__class_Ominus(X0,X1,tc_nat),tc_nat) = X1 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_diff__diff__cancel_0) ).
fof(f697,axiom,
! [X2,X3,X0,X1,X4] :
( c_in(hAPP(X0,X1),c_Set_Oimage(X0,X2,X3,X4),X4)
| ~ c_in(X1,X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_imageI_0) ).
fof(f699,negated_conjecture,
c_Finite__Set_Ofinite(v_U,tc_Com_Opname),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_0) ).
fof(f700,negated_conjecture,
c_lessequals(v_G,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_1) ).
fof(f701,negated_conjecture,
c_lessequals(c_Suc(v_na),c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_2) ).
fof(f702,negated_conjecture,
c_Finite__Set_Ocard(v_G,t_a) = c_HOL_Ominus__class_Ominus(c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),c_Suc(v_na),tc_nat),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_3) ).
fof(f703,negated_conjecture,
c_in(v_pn,v_U,tc_Com_Opname),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_4) ).
fof(f704,negated_conjecture,
~ c_in(hAPP(v_mgt__call,v_pn),v_G,t_a),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_5) ).
fof(f705,negated_conjecture,
~ hBOOL(hAPP(hAPP(v_P,v_G),c_Set_Oinsert(hAPP(v_mgt__call,v_pn),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_6) ).
fof(f706,negated_conjecture,
! [X0,X1] :
( c_Finite__Set_Ocard(X0,t_a) != c_HOL_Ominus__class_Ominus(c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),v_na,tc_nat)
| ~ c_lessequals(X0,c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),tc_fun(t_a,tc_bool))
| hBOOL(hAPP(hAPP(v_P,X0),c_Set_Oinsert(v_mgt(X1),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a)))
| ~ v_wt(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cls_conjecture_7) ).
fof(f803,plain,
! [X2,X0,X1] :
( c_in(X0,X1,X2)
| c_Finite__Set_Ocard(c_Set_Oinsert(X0,X1,X2),X2) = c_HOL_Oplus__class_Oplus(c_Finite__Set_Ocard(X1,X2),c_HOL_Oone__class_Oone(tc_nat),tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Finite__Set_Ocard(X1,X2) ),
inference(definition_unfolding,[],[f539,f23]) ).
fof(f817,plain,
! [X2,X0,X1] :
( c_in(X0,X1,X2)
| c_Finite__Set_Ocard(c_Set_Oinsert(X0,X1,X2),X2) = c_HOL_Oplus__class_Oplus(c_Finite__Set_Ocard(X1,X2),c_HOL_Oone__class_Oone(tc_nat),tc_nat)
| ~ c_Finite__Set_Ofinite(X1,X2) ),
inference(definition_unfolding,[],[f650,f23]) ).
fof(f824,plain,
c_lessequals(c_HOL_Oplus__class_Oplus(v_na,c_HOL_Oone__class_Oone(tc_nat),tc_nat),c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),tc_nat),
inference(definition_unfolding,[],[f701,f23]) ).
fof(f825,plain,
c_Finite__Set_Ocard(v_G,t_a) = c_HOL_Ominus__class_Ominus(c_Finite__Set_Ocard(c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),t_a),c_HOL_Oplus__class_Oplus(v_na,c_HOL_Oone__class_Oone(tc_nat),tc_nat),tc_nat),
inference(definition_unfolding,[],[f702,f23]) ).
fof(f826,definition,
sF0 = c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f827,plain,
c_Set_Oimage(v_mgt__call,v_U,tc_Com_Opname,t_a) = sF0,
inference(reorient_equations,[],[f826]) ).
fof(f828,definition,
sF1 = tc_fun(t_a,tc_bool),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f829,plain,
tc_fun(t_a,tc_bool) = sF1,
inference(reorient_equations,[],[f828]) ).
fof(f830,plain,
c_lessequals(v_G,sF0,sF1),
inference(definition_folding,[],[f700,f829,f827]) ).
fof(f831,definition,
sF2 = c_HOL_Oone__class_Oone(tc_nat),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f832,plain,
c_HOL_Oone__class_Oone(tc_nat) = sF2,
inference(reorient_equations,[],[f831]) ).
fof(f833,definition,
sF3 = c_HOL_Oplus__class_Oplus(v_na,sF2,tc_nat),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f834,plain,
c_HOL_Oplus__class_Oplus(v_na,sF2,tc_nat) = sF3,
inference(reorient_equations,[],[f833]) ).
fof(f835,definition,
sF4 = c_Finite__Set_Ocard(sF0,t_a),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f836,plain,
c_Finite__Set_Ocard(sF0,t_a) = sF4,
inference(reorient_equations,[],[f835]) ).
fof(f837,plain,
c_lessequals(sF3,sF4,tc_nat),
inference(definition_folding,[],[f824,f836,f827,f834,f832]) ).
fof(f838,definition,
sF5 = c_Finite__Set_Ocard(v_G,t_a),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f839,plain,
c_Finite__Set_Ocard(v_G,t_a) = sF5,
inference(reorient_equations,[],[f838]) ).
fof(f840,definition,
sF6 = c_HOL_Ominus__class_Ominus(sF4,sF3,tc_nat),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f841,plain,
c_HOL_Ominus__class_Ominus(sF4,sF3,tc_nat) = sF6,
inference(reorient_equations,[],[f840]) ).
fof(f842,plain,
sF5 = sF6,
inference(definition_folding,[],[f825,f841,f834,f832,f836,f827,f839]) ).
fof(f843,definition,
sF7 = hAPP(v_mgt__call,v_pn),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f844,plain,
hAPP(v_mgt__call,v_pn) = sF7,
inference(reorient_equations,[],[f843]) ).
fof(f845,plain,
~ c_in(sF7,v_G,t_a),
inference(definition_folding,[],[f704,f844]) ).
fof(f846,definition,
sF8 = hAPP(v_P,v_G),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f847,plain,
hAPP(v_P,v_G) = sF8,
inference(reorient_equations,[],[f846]) ).
fof(f848,definition,
sF9 = c_Orderings_Obot__class_Obot(sF1),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f849,plain,
c_Orderings_Obot__class_Obot(sF1) = sF9,
inference(reorient_equations,[],[f848]) ).
fof(f850,definition,
sF10 = c_Set_Oinsert(sF7,sF9,t_a),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
fof(f851,plain,
c_Set_Oinsert(sF7,sF9,t_a) = sF10,
inference(reorient_equations,[],[f850]) ).
fof(f852,definition,
sF11 = hAPP(sF8,sF10),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
fof(f853,plain,
hAPP(sF8,sF10) = sF11,
inference(reorient_equations,[],[f852]) ).
fof(f854,plain,
~ hBOOL(sF11),
inference(definition_folding,[],[f705,f853,f851,f849,f829,f844,f847]) ).
fof(f855,definition,
! [X0] : sF12(X0) = c_Finite__Set_Ocard(X0,t_a),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f856,plain,
! [X0] : c_Finite__Set_Ocard(X0,t_a) = sF12(X0),
inference(reorient_equations,[],[f855]) ).
fof(f857,definition,
sF13 = c_HOL_Ominus__class_Ominus(sF4,v_na,tc_nat),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f858,plain,
c_HOL_Ominus__class_Ominus(sF4,v_na,tc_nat) = sF13,
inference(reorient_equations,[],[f857]) ).
fof(f859,definition,
! [X0] : sF14(X0) = hAPP(v_P,X0),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f860,plain,
! [X0] : hAPP(v_P,X0) = sF14(X0),
inference(reorient_equations,[],[f859]) ).
fof(f861,definition,
! [X1] : sF15(X1) = c_Set_Oinsert(v_mgt(X1),sF9,t_a),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f862,plain,
! [X1] : c_Set_Oinsert(v_mgt(X1),sF9,t_a) = sF15(X1),
inference(reorient_equations,[],[f861]) ).
fof(f863,definition,
! [X0,X1] : sF16(X0,X1) = hAPP(sF14(X0),sF15(X1)),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f864,plain,
! [X0,X1] : hAPP(sF14(X0),sF15(X1)) = sF16(X0,X1),
inference(reorient_equations,[],[f863]) ).
fof(f865,plain,
! [X0,X1] :
( sF12(X0) != sF13
| ~ c_lessequals(X0,sF0,sF1)
| hBOOL(sF16(X0,X1))
| ~ v_wt(X1) ),
inference(definition_folding,[],[f706,f864,f862,f849,f829,f860,f829,f827,f858,f836,f827,f856]) ).
fof(f883,plain,
sF5 = c_HOL_Ominus__class_Ominus(sF4,sF3,tc_nat),
inference(forward_demodulation,[],[f841,f842]) ).
fof(f915,plain,
! [X2,X0,X1] :
( c_lessequals(c_Set_Oinsert(X0,X1,t_a),X2,sF1)
| ~ c_lessequals(X1,X2,sF1)
| ~ c_in(X0,X2,t_a) ),
inference(superposition,[],[f588,f829]) ).
fof(f918,plain,
! [X2,X0,X1] :
( c_in(sF7,c_Set_Oimage(v_mgt__call,X0,X1,X2),X2)
| ~ c_in(v_pn,X0,X1) ),
inference(superposition,[],[f697,f844]) ).
fof(f922,plain,
( c_in(sF7,sF0,t_a)
| ~ c_in(v_pn,v_U,tc_Com_Opname) ),
inference(superposition,[],[f918,f827]) ).
fof(f923,plain,
c_in(sF7,sF0,t_a),
inference(forward_subsumption_resolution,[],[f922,f703]) ).
fof(f944,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(v_P,c_Set_Oinsert(sF7,X0,t_a)),c_Set_Oinsert(v_mgt(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom)),c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a)))
| hBOOL(hAPP(hAPP(v_P,X0),c_Set_Oinsert(sF7,c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a))) ),
inference(superposition,[],[f528,f844]) ).
fof(f947,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(v_P,c_Set_Oinsert(sF7,X0,t_a)),c_Set_Oinsert(v_mgt(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom)),c_Orderings_Obot__class_Obot(sF1),t_a)))
| hBOOL(hAPP(hAPP(v_P,X0),c_Set_Oinsert(sF7,c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a))) ),
inference(forward_demodulation,[],[f944,f829]) ).
fof(f949,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(v_P,c_Set_Oinsert(sF7,X0,t_a)),c_Set_Oinsert(v_mgt(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom)),sF9,t_a)))
| hBOOL(hAPP(hAPP(v_P,X0),c_Set_Oinsert(sF7,c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a))) ),
inference(forward_demodulation,[],[f947,f849]) ).
fof(f951,plain,
! [X0] :
( ~ hBOOL(hAPP(hAPP(v_P,c_Set_Oinsert(sF7,X0,t_a)),sF15(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom))))
| hBOOL(hAPP(hAPP(v_P,X0),c_Set_Oinsert(sF7,c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a))) ),
inference(forward_demodulation,[],[f949,f862]) ).
fof(f953,plain,
! [X0] :
( ~ hBOOL(hAPP(sF14(c_Set_Oinsert(sF7,X0,t_a)),sF15(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom))))
| hBOOL(hAPP(hAPP(v_P,X0),c_Set_Oinsert(sF7,c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a))) ),
inference(forward_demodulation,[],[f951,f860]) ).
fof(f955,plain,
! [X0] :
( ~ hBOOL(sF16(c_Set_Oinsert(sF7,X0,t_a),c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom)))
| hBOOL(hAPP(hAPP(v_P,X0),c_Set_Oinsert(sF7,c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)),t_a))) ),
inference(forward_demodulation,[],[f953,f864]) ).
fof(f957,plain,
! [X0] :
( hBOOL(hAPP(hAPP(v_P,X0),c_Set_Oinsert(sF7,c_Orderings_Obot__class_Obot(sF1),t_a)))
| ~ hBOOL(sF16(c_Set_Oinsert(sF7,X0,t_a),c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom))) ),
inference(forward_demodulation,[],[f955,f829]) ).
fof(f958,plain,
! [X0] :
( hBOOL(hAPP(hAPP(v_P,X0),c_Set_Oinsert(sF7,sF9,t_a)))
| ~ hBOOL(sF16(c_Set_Oinsert(sF7,X0,t_a),c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom))) ),
inference(forward_demodulation,[],[f957,f849]) ).
fof(f959,plain,
! [X0] :
( hBOOL(hAPP(hAPP(v_P,X0),sF10))
| ~ hBOOL(sF16(c_Set_Oinsert(sF7,X0,t_a),c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom))) ),
inference(forward_demodulation,[],[f958,f851]) ).
fof(f960,plain,
! [X0] :
( ~ hBOOL(sF16(c_Set_Oinsert(sF7,X0,t_a),c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom)))
| hBOOL(hAPP(sF14(X0),sF10)) ),
inference(forward_demodulation,[],[f959,f860]) ).
fof(f962,plain,
sF8 = sF14(v_G),
inference(superposition,[],[f847,f860]) ).
fof(f1023,definition,
( spl17_3
<=> c_Finite__Set_Ofinite(v_G,t_a) ),
introduced(definition,[new_symbols(definition,[spl17_3])],[avatar_definition]) ).
fof(f1024,plain,
( c_Finite__Set_Ofinite(v_G,t_a)
| ~ spl17_3 ),
inference(avatar_component_clause,[],[f1023]) ).
fof(f1025,plain,
( ~ c_Finite__Set_Ofinite(v_G,t_a)
| spl17_3 ),
inference(avatar_component_clause,[],[f1023]) ).
fof(f1031,definition,
( spl17_5
<=> c_Finite__Set_Ofinite(sF0,t_a) ),
introduced(definition,[new_symbols(definition,[spl17_5])],[avatar_definition]) ).
fof(f1032,plain,
( c_Finite__Set_Ofinite(sF0,t_a)
| ~ spl17_5 ),
inference(avatar_component_clause,[],[f1031]) ).
fof(f1033,plain,
( ~ c_Finite__Set_Ofinite(sF0,t_a)
| spl17_5 ),
inference(avatar_component_clause,[],[f1031]) ).
fof(f1041,plain,
sF2 = c_HOL_Ominus__class_Ominus(sF3,v_na,tc_nat),
inference(superposition,[],[f462,f834]) ).
fof(f1085,plain,
sF3 = c_HOL_Ominus__class_Ominus(sF4,c_HOL_Ominus__class_Ominus(sF4,sF3,tc_nat),tc_nat),
inference(resolution,[],[f837,f691]) ).
fof(f1086,plain,
sF3 = c_HOL_Ominus__class_Ominus(sF4,sF5,tc_nat),
inference(forward_demodulation,[],[f1085,f883]) ).
fof(f1155,plain,
( c_Finite__Set_Ofinite(sF0,t_a)
| ~ c_Finite__Set_Ofinite(v_U,tc_Com_Opname) ),
inference(superposition,[],[f608,f827]) ).
fof(f1156,plain,
( ~ c_Finite__Set_Ofinite(v_U,tc_Com_Opname)
| spl17_5 ),
inference(forward_subsumption_resolution,[],[f1155,f1033]) ).
fof(f1157,plain,
( $false
| spl17_5 ),
inference(forward_subsumption_resolution,[],[f1156,f699]) ).
fof(f1158,plain,
spl17_5,
inference(avatar_contradiction_clause,[],[f1157]) ).
fof(f1192,plain,
( c_HOL_Ozero__class_Ozero(tc_nat) != sF5
| ~ c_Finite__Set_Ofinite(v_G,t_a)
| c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)) = v_G ),
inference(superposition,[],[f520,f839]) ).
fof(f1271,plain,
! [X0] : c_HOL_Ominus__class_Ominus(sF4,c_HOL_Oplus__class_Oplus(v_na,X0,tc_nat),tc_nat) = c_HOL_Ominus__class_Ominus(sF13,X0,tc_nat),
inference(superposition,[],[f454,f858]) ).
fof(f1288,plain,
c_HOL_Ominus__class_Ominus(sF4,sF3,tc_nat) = c_HOL_Ominus__class_Ominus(sF13,sF2,tc_nat),
inference(superposition,[],[f1271,f834]) ).
fof(f1294,plain,
sF5 = c_HOL_Ominus__class_Ominus(sF13,sF2,tc_nat),
inference(forward_demodulation,[],[f1288,f883]) ).
fof(f1297,plain,
c_lessequals(sF5,sF13,tc_nat),
inference(superposition,[],[f663,f1294]) ).
fof(f1313,plain,
( c_Finite__Set_Ocard(c_Set_Oinsert(sF7,v_G,t_a),t_a) = c_HOL_Oplus__class_Oplus(c_Finite__Set_Ocard(v_G,t_a),c_HOL_Oone__class_Oone(tc_nat),tc_nat)
| ~ c_Finite__Set_Ofinite(v_G,t_a) ),
inference(resolution,[],[f817,f845]) ).
fof(f1631,plain,
! [X0] : c_HOL_Ominus__class_Ominus(sF3,X0,tc_nat) = c_HOL_Ominus__class_Ominus(c_HOL_Ominus__class_Ominus(sF4,X0,tc_nat),sF5,tc_nat),
inference(superposition,[],[f668,f1086]) ).
fof(f1648,plain,
! [X0] : c_HOL_Ominus__class_Ominus(sF3,X0,tc_nat) = c_HOL_Ominus__class_Ominus(sF4,c_HOL_Oplus__class_Oplus(X0,sF5,tc_nat),tc_nat),
inference(forward_demodulation,[],[f1631,f454]) ).
fof(f2653,definition,
( spl17_51
<=> v_wt(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom)) ),
introduced(definition,[new_symbols(definition,[spl17_51])],[avatar_definition]) ).
fof(f2654,plain,
( v_wt(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom))
| ~ spl17_51 ),
inference(avatar_component_clause,[],[f2653]) ).
fof(f2655,plain,
( ~ v_wt(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom))
| spl17_51 ),
inference(avatar_component_clause,[],[f2653]) ).
fof(f2670,plain,
( ~ c_in(v_pn,v_U,tc_Com_Opname)
| spl17_51 ),
inference(resolution,[],[f2655,f485]) ).
fof(f2671,plain,
( $false
| spl17_51 ),
inference(forward_subsumption_resolution,[],[f2670,f703]) ).
fof(f2672,plain,
spl17_51,
inference(avatar_contradiction_clause,[],[f2671]) ).
fof(f2936,plain,
sF13 = c_HOL_Oplus__class_Oplus(sF5,c_HOL_Ominus__class_Ominus(sF13,sF5,tc_nat),tc_nat),
inference(resolution,[],[f1297,f470]) ).
fof(f3184,plain,
( c_Finite__Set_Ocard(c_Set_Oinsert(sF7,v_G,t_a),t_a) = c_HOL_Oplus__class_Oplus(c_Finite__Set_Ocard(v_G,t_a),c_HOL_Oone__class_Oone(tc_nat),tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Finite__Set_Ocard(v_G,t_a) ),
inference(resolution,[],[f803,f845]) ).
fof(f3187,plain,
( c_Finite__Set_Ocard(c_Set_Oinsert(sF7,v_G,t_a),t_a) = c_HOL_Oplus__class_Oplus(c_Finite__Set_Ocard(v_G,t_a),sF2,tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Finite__Set_Ocard(v_G,t_a) ),
inference(forward_demodulation,[],[f3184,f832]) ).
fof(f3202,plain,
( c_Finite__Set_Ocard(c_Set_Oinsert(sF7,v_G,t_a),t_a) = c_HOL_Oplus__class_Oplus(sF5,sF2,tc_nat)
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Finite__Set_Ocard(v_G,t_a) ),
inference(forward_demodulation,[],[f3187,f839]) ).
fof(f3212,plain,
( c_HOL_Oplus__class_Oplus(sF5,sF2,tc_nat) = sF12(c_Set_Oinsert(sF7,v_G,t_a))
| c_HOL_Ozero__class_Ozero(tc_nat) = c_Finite__Set_Ocard(v_G,t_a) ),
inference(forward_demodulation,[],[f3202,f856]) ).
fof(f3221,plain,
( c_HOL_Ozero__class_Ozero(tc_nat) = sF5
| c_HOL_Oplus__class_Oplus(sF5,sF2,tc_nat) = sF12(c_Set_Oinsert(sF7,v_G,t_a)) ),
inference(forward_demodulation,[],[f3212,f839]) ).
fof(f3230,definition,
( spl17_61
<=> c_HOL_Oplus__class_Oplus(sF5,sF2,tc_nat) = sF12(c_Set_Oinsert(sF7,v_G,t_a)) ),
introduced(definition,[new_symbols(definition,[spl17_61])],[avatar_definition]) ).
fof(f3231,plain,
( c_HOL_Oplus__class_Oplus(sF5,sF2,tc_nat) != sF12(c_Set_Oinsert(sF7,v_G,t_a))
| spl17_61 ),
inference(avatar_component_clause,[],[f3230]) ).
fof(f3232,plain,
( c_HOL_Oplus__class_Oplus(sF5,sF2,tc_nat) = sF12(c_Set_Oinsert(sF7,v_G,t_a))
| ~ spl17_61 ),
inference(avatar_component_clause,[],[f3230]) ).
fof(f3234,definition,
( spl17_62
<=> c_HOL_Ozero__class_Ozero(tc_nat) = sF5 ),
introduced(definition,[new_symbols(definition,[spl17_62])],[avatar_definition]) ).
fof(f3236,plain,
( c_HOL_Ozero__class_Ozero(tc_nat) = sF5
| ~ spl17_62 ),
inference(avatar_component_clause,[],[f3234]) ).
fof(f3237,plain,
( spl17_61
| spl17_62 ),
inference(avatar_split_clause,[],[f3221,f3234,f3230]) ).
fof(f3246,plain,
( ! [X0] :
( sF13 != c_HOL_Oplus__class_Oplus(sF5,sF2,tc_nat)
| ~ c_lessequals(c_Set_Oinsert(sF7,v_G,t_a),sF0,sF1)
| hBOOL(sF16(c_Set_Oinsert(sF7,v_G,t_a),X0))
| ~ v_wt(X0) )
| ~ spl17_61 ),
inference(superposition,[],[f865,f3232]) ).
fof(f3268,definition,
( spl17_68
<=> c_lessequals(c_Set_Oinsert(sF7,v_G,t_a),sF0,sF1) ),
introduced(definition,[new_symbols(definition,[spl17_68])],[avatar_definition]) ).
fof(f3270,plain,
( ~ c_lessequals(c_Set_Oinsert(sF7,v_G,t_a),sF0,sF1)
| spl17_68 ),
inference(avatar_component_clause,[],[f3268]) ).
fof(f3290,definition,
( spl17_73
<=> ! [X0] :
( hBOOL(sF16(c_Set_Oinsert(sF7,v_G,t_a),X0))
| ~ v_wt(X0) ) ),
introduced(definition,[new_symbols(definition,[spl17_73])],[avatar_definition]) ).
fof(f3291,plain,
( ! [X0] :
( hBOOL(sF16(c_Set_Oinsert(sF7,v_G,t_a),X0))
| ~ v_wt(X0) )
| ~ spl17_73 ),
inference(avatar_component_clause,[],[f3290]) ).
fof(f3293,definition,
( spl17_74
<=> sF13 = c_HOL_Oplus__class_Oplus(sF5,sF2,tc_nat) ),
introduced(definition,[new_symbols(definition,[spl17_74])],[avatar_definition]) ).
fof(f3294,plain,
( sF13 = c_HOL_Oplus__class_Oplus(sF5,sF2,tc_nat)
| ~ spl17_74 ),
inference(avatar_component_clause,[],[f3293]) ).
fof(f3295,plain,
( sF13 != c_HOL_Oplus__class_Oplus(sF5,sF2,tc_nat)
| spl17_74 ),
inference(avatar_component_clause,[],[f3293]) ).
fof(f3296,plain,
( spl17_73
| ~ spl17_68
| ~ spl17_74
| ~ spl17_61 ),
inference(avatar_split_clause,[],[f3246,f3230,f3293,f3268,f3290]) ).
fof(f3297,plain,
( ~ c_lessequals(v_G,sF0,sF1)
| ~ c_in(sF7,sF0,t_a)
| spl17_68 ),
inference(resolution,[],[f3270,f915]) ).
fof(f3299,plain,
( ~ c_in(sF7,sF0,t_a)
| spl17_68 ),
inference(forward_subsumption_resolution,[],[f3297,f830]) ).
fof(f3300,plain,
( $false
| spl17_68 ),
inference(forward_subsumption_resolution,[],[f3299,f923]) ).
fof(f3301,plain,
spl17_68,
inference(avatar_contradiction_clause,[],[f3300]) ).
fof(f3376,plain,
( ~ v_wt(c_Option_Othe(c_Com_Obody(v_pn),tc_Com_Ocom))
| hBOOL(hAPP(sF14(v_G),sF10))
| ~ spl17_73 ),
inference(resolution,[],[f3291,f960]) ).
fof(f3378,plain,
( hBOOL(hAPP(sF14(v_G),sF10))
| ~ spl17_51
| ~ spl17_73 ),
inference(forward_subsumption_resolution,[],[f3376,f2654]) ).
fof(f3379,plain,
( hBOOL(hAPP(sF8,sF10))
| ~ spl17_51
| ~ spl17_73 ),
inference(forward_demodulation,[],[f3378,f962]) ).
fof(f3380,plain,
( hBOOL(sF11)
| ~ spl17_51
| ~ spl17_73 ),
inference(forward_demodulation,[],[f3379,f853]) ).
fof(f3381,plain,
( $false
| ~ spl17_51
| ~ spl17_73 ),
inference(forward_subsumption_resolution,[],[f3380,f854]) ).
fof(f3382,plain,
( ~ spl17_51
| ~ spl17_73 ),
inference(avatar_contradiction_clause,[],[f3381]) ).
fof(f4632,plain,
c_HOL_Ominus__class_Ominus(sF3,v_na,tc_nat) = c_HOL_Ominus__class_Ominus(sF13,sF5,tc_nat),
inference(superposition,[],[f1271,f1648]) ).
fof(f4779,plain,
sF2 = c_HOL_Ominus__class_Ominus(sF13,sF5,tc_nat),
inference(forward_demodulation,[],[f4632,f1041]) ).
fof(f4781,plain,
sF13 = c_HOL_Oplus__class_Oplus(sF5,sF2,tc_nat),
inference(superposition,[],[f2936,f4779]) ).
fof(f4792,plain,
( $false
| spl17_74 ),
inference(forward_subsumption_resolution,[],[f4781,f3295]) ).
fof(f4793,plain,
spl17_74,
inference(avatar_contradiction_clause,[],[f4792]) ).
fof(f5299,plain,
! [X0,X1] :
( ~ c_lessequals(X0,X1,sF1)
| c_Finite__Set_Ofinite(X0,t_a)
| ~ c_Finite__Set_Ofinite(X1,t_a) ),
inference(superposition,[],[f566,f829]) ).
fof(f5311,plain,
( c_Finite__Set_Ofinite(v_G,t_a)
| ~ c_Finite__Set_Ofinite(sF0,t_a) ),
inference(resolution,[],[f5299,f830]) ).
fof(f5323,plain,
( ~ c_Finite__Set_Ofinite(sF0,t_a)
| spl17_3 ),
inference(forward_subsumption_resolution,[],[f5311,f1025]) ).
fof(f5326,plain,
( $false
| spl17_3
| ~ spl17_5 ),
inference(forward_subsumption_resolution,[],[f5323,f1032]) ).
fof(f5327,plain,
( spl17_3
| ~ spl17_5 ),
inference(avatar_contradiction_clause,[],[f5326]) ).
fof(f5328,plain,
( ~ c_Finite__Set_Ofinite(v_G,t_a)
| c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)) = v_G
| ~ spl17_62 ),
inference(forward_subsumption_resolution,[],[f1192,f3236]) ).
fof(f5329,plain,
( c_Finite__Set_Ocard(c_Set_Oinsert(sF7,v_G,t_a),t_a) = c_HOL_Oplus__class_Oplus(c_Finite__Set_Ocard(v_G,t_a),c_HOL_Oone__class_Oone(tc_nat),tc_nat)
| ~ spl17_3 ),
inference(forward_subsumption_resolution,[],[f1313,f1024]) ).
fof(f5331,plain,
( c_Orderings_Obot__class_Obot(tc_fun(t_a,tc_bool)) = v_G
| ~ spl17_3
| ~ spl17_62 ),
inference(forward_subsumption_resolution,[],[f5328,f1024]) ).
fof(f5332,plain,
( c_Finite__Set_Ocard(c_Set_Oinsert(sF7,v_G,t_a),t_a) = c_HOL_Oplus__class_Oplus(c_Finite__Set_Ocard(v_G,t_a),sF2,tc_nat)
| ~ spl17_3 ),
inference(forward_demodulation,[],[f5329,f832]) ).
fof(f5334,plain,
( v_G = c_Orderings_Obot__class_Obot(sF1)
| ~ spl17_3
| ~ spl17_62 ),
inference(forward_demodulation,[],[f5331,f829]) ).
fof(f5335,plain,
( c_Finite__Set_Ocard(c_Set_Oinsert(sF7,v_G,t_a),t_a) = c_HOL_Oplus__class_Oplus(sF5,sF2,tc_nat)
| ~ spl17_3 ),
inference(forward_demodulation,[],[f5332,f839]) ).
fof(f5337,plain,
( v_G = sF9
| ~ spl17_3
| ~ spl17_62 ),
inference(forward_demodulation,[],[f5334,f849]) ).
fof(f5338,plain,
( sF13 = c_Finite__Set_Ocard(c_Set_Oinsert(sF7,v_G,t_a),t_a)
| ~ spl17_3
| ~ spl17_74 ),
inference(forward_demodulation,[],[f5335,f3294]) ).
fof(f5340,plain,
( sF13 = sF12(c_Set_Oinsert(sF7,v_G,t_a))
| ~ spl17_3
| ~ spl17_74 ),
inference(forward_demodulation,[],[f5338,f856]) ).
fof(f5342,plain,
( sF13 = sF12(c_Set_Oinsert(sF7,sF9,t_a))
| ~ spl17_3
| ~ spl17_62
| ~ spl17_74 ),
inference(forward_demodulation,[],[f5340,f5337]) ).
fof(f5382,plain,
( c_HOL_Oplus__class_Oplus(sF5,sF2,tc_nat) != sF12(c_Set_Oinsert(sF7,sF9,t_a))
| ~ spl17_3
| spl17_61
| ~ spl17_62 ),
inference(superposition,[],[f3231,f5337]) ).
fof(f5428,plain,
( sF13 = sF12(sF10)
| ~ spl17_3
| ~ spl17_62
| ~ spl17_74 ),
inference(forward_demodulation,[],[f5342,f851]) ).
fof(f5429,plain,
( sF12(sF10) != c_HOL_Oplus__class_Oplus(sF5,sF2,tc_nat)
| ~ spl17_3
| spl17_61
| ~ spl17_62 ),
inference(forward_demodulation,[],[f5382,f851]) ).
fof(f5431,plain,
( sF13 != sF12(sF10)
| ~ spl17_3
| spl17_61
| ~ spl17_62
| ~ spl17_74 ),
inference(forward_demodulation,[],[f5429,f3294]) ).
fof(f5435,plain,
( $false
| ~ spl17_3
| spl17_61
| ~ spl17_62
| ~ spl17_74 ),
inference(forward_subsumption_resolution,[],[f5431,f5428]) ).
fof(f5436,plain,
( ~ spl17_3
| spl17_61
| ~ spl17_62
| ~ spl17_74 ),
inference(avatar_contradiction_clause,[],[f5435]) ).
cnf(s4,plain,
spl17_5,
inference(sat_conversion,[],[f1158]) ).
cnf(s36,plain,
spl17_51,
inference(sat_conversion,[],[f2672]) ).
cnf(s47,plain,
( spl17_61
| spl17_62 ),
inference(sat_conversion,[],[f3237]) ).
cnf(s52,plain,
( ~ spl17_61
| ~ spl17_68
| spl17_73
| ~ spl17_74 ),
inference(sat_conversion,[],[f3296]) ).
cnf(s53,plain,
spl17_68,
inference(sat_conversion,[],[f3301]) ).
cnf(s59,plain,
( ~ spl17_51
| ~ spl17_73 ),
inference(sat_conversion,[],[f3382]) ).
cnf(s103,plain,
spl17_74,
inference(sat_conversion,[],[f4793]) ).
cnf(s117,plain,
( spl17_3
| ~ spl17_5 ),
inference(sat_conversion,[],[f5327]) ).
cnf(s121,plain,
( ~ spl17_3
| spl17_61
| ~ spl17_62
| ~ spl17_74 ),
inference(sat_conversion,[],[f5436]) ).
cnf(s125,plain,
( ~ spl17_61
| spl17_73 ),
inference(rat,[],[s52,s103,s53]) ).
cnf(s129,plain,
~ spl17_73,
inference(rat,[],[s59,s36]) ).
cnf(s130,plain,
~ spl17_61,
inference(rat,[],[s125,s129]) ).
cnf(s131,plain,
spl17_62,
inference(rat,[],[s47,s130]) ).
cnf(s132,plain,
~ spl17_3,
inference(rat,[],[s121,s103,s130,s131]) ).
cnf(s133,plain,
~ spl17_5,
inference(rat,[],[s117,s132]) ).
cnf(s136,plain,
$false,
inference(rat,[],[s4,s133]) ).
fof(f5437,plain,
$false,
inference(avatar_sat_refutation,[],[s136]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWV883-1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.19 % Computer : n019.cluster.edu
% 0.07/0.19 % Model : x86_64 x86_64
% 0.07/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.19 % Memory : 8046.5625MB
% 0.07/0.19 % OS : Linux 6.8.0-71-generic
% 0.07/0.19 % CPULimit : 300
% 0.07/0.19 % WCLimit : 300
% 0.07/0.19 % DateTime : Mon Sep 28 12:48:33 UTC 2026
% 0.07/0.19 % CPUTime :
% 0.07/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.07/0.22 Running first-order theorem proving
% 0.07/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 6.10/1.69 % (3977643)Input is clausal, will run a generic CNF schedule.
% 6.10/1.69 % (3977648)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=1895312520:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 6.10/1.69 % (3977653)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2410833651:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 6.10/1.69 % (3977649)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=2161566665:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 6.10/1.69 % (3977654)dis-21_1_sil=8000:lcm=predicate:random_seed=1340733678: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)
% 6.10/1.69 % (3977652)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=1837531997:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 6.10/1.69 % (3977651)lrs+10_1_sil=8000:sp=occurrence:random_seed=2378325357:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 6.10/1.69 % (3977650)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1138692692:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 6.10/1.69 % (3977654)Instruction limit reached!
% 6.10/1.69 % (3977654)------------------------------
% 6.10/1.69 % (3977654)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.10/1.69 % (3977654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.10/1.69 % (3977654)CaDiCaL version: 2.1.3
% 6.10/1.69 % (3977654)Termination reason: Instruction limit
% 6.10/1.69 % (3977654)Termination phase: Saturation
% 6.10/1.69 % (3977654)Time elapsed: 0.066 s
% 6.10/1.69 % (3977654)Peak memory usage: 89 MB
% 6.10/1.69 % (3977654)Instructions burned: 117 (million)
% 6.10/1.69 % (3977651)Instruction limit reached!
% 6.10/1.69 % (3977651)------------------------------
% 6.10/1.69 % (3977651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.10/1.69 % (3977651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.10/1.69 % (3977651)CaDiCaL version: 2.1.3
% 6.10/1.69 % (3977651)Termination reason: Instruction limit
% 6.10/1.69 % (3977651)Termination phase: Saturation
% 6.10/1.69 % (3977651)Time elapsed: 0.072 s
% 6.10/1.69 % (3977651)Peak memory usage: 89 MB
% 6.10/1.69 % (3977651)Instructions burned: 108 (million)
% 6.10/1.69 % (3977652)Instruction limit reached!
% 6.10/1.69 % (3977652)------------------------------
% 6.10/1.69 % (3977652)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.10/1.69 % (3977652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.10/1.69 % (3977652)CaDiCaL version: 2.1.3
% 6.10/1.69 % (3977652)Termination reason: Instruction limit
% 6.10/1.69 % (3977652)Termination phase: Saturation
% 6.10/1.69 % (3977652)Time elapsed: 0.077 s
% 6.10/1.69 % (3977652)Peak memory usage: 89 MB
% 6.10/1.69 % (3977652)Instructions burned: 115 (million)
% 6.10/1.69 % (3977653)Instruction limit reached!
% 6.10/1.69 % (3977653)------------------------------
% 6.10/1.69 % (3977653)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.10/1.69 % (3977653)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.10/1.69 % (3977653)CaDiCaL version: 2.1.3
% 6.10/1.69 % (3977653)Termination reason: Instruction limit
% 6.10/1.69 % (3977653)Termination phase: Saturation
% 6.10/1.69 % (3977653)Time elapsed: 0.121 s
% 6.10/1.69 % (3977653)Peak memory usage: 90 MB
% 6.10/1.69 % (3977653)Instructions burned: 180 (million)
% 6.10/1.69 % (3977662)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=1126583738:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 6.10/1.69 % (3977663)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=1712695380: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)
% 6.10/1.69 % (3977664)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3322055549:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 6.10/1.69 % (3977665)lrs+10_64_to=lpo:sil=8000:random_seed=2159749709:i=126:bd=preordered_2996 on theBenchmark for (2996ds/126Mi)
% 6.10/1.69 % (3977662)Instruction limit reached!
% 6.10/1.69 % (3977662)------------------------------
% 6.10/1.69 % (3977662)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.10/1.69 % (3977662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.10/1.69 % (3977662)CaDiCaL version: 2.1.3
% 6.10/1.69 % (3977662)Termination reason: Instruction limit
% 6.10/1.69 % (3977662)Termination phase: Saturation
% 6.10/1.69 % (3977662)Time elapsed: 0.086 s
% 6.10/1.69 % (3977662)Peak memory usage: 89 MB
% 6.10/1.69 % (3977662)Instructions burned: 144 (million)
% 6.10/1.69 % (3977663)Instruction limit reached!
% 6.10/1.69 % (3977663)------------------------------
% 6.10/1.69 % (3977663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.10/1.69 % (3977663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.10/1.69 % (3977663)CaDiCaL version: 2.1.3
% 6.10/1.69 % (3977663)Termination reason: Instruction limit
% 6.10/1.69 % (3977663)Termination phase: Saturation
% 6.10/1.69 % (3977663)Time elapsed: 0.106 s
% 6.10/1.69 % (3977663)Peak memory usage: 90 MB
% 6.10/1.69 % (3977663)Instructions burned: 190 (million)
% 6.10/1.69 % (3977664)Instruction limit reached!
% 6.10/1.69 % (3977664)------------------------------
% 6.10/1.69 % (3977664)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.10/1.69 % (3977664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.10/1.69 % (3977664)CaDiCaL version: 2.1.3
% 6.10/1.69 % (3977664)Termination reason: Instruction limit
% 6.10/1.69 % (3977664)Termination phase: Saturation
% 6.10/1.69 % (3977664)Time elapsed: 0.130 s
% 6.10/1.69 % (3977664)Peak memory usage: 90 MB
% 6.10/1.69 % (3977664)Instructions burned: 219 (million)
% 6.10/1.69 % (3977665)Instruction limit reached!
% 6.10/1.69 % (3977665)------------------------------
% 6.10/1.69 % (3977665)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.10/1.69 % (3977665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.10/1.69 % (3977665)CaDiCaL version: 2.1.3
% 6.10/1.69 % (3977665)Termination reason: Instruction limit
% 6.10/1.69 % (3977665)Termination phase: Saturation
% 6.10/1.69 % (3977665)Time elapsed: 0.083 s
% 6.10/1.69 % (3977665)Peak memory usage: 90 MB
% 6.10/1.69 % (3977665)Instructions burned: 126 (million)
% 6.10/1.69 % (3977670)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=2426411947:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 6.10/1.69 % (3977671)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=694539018:i=157:gtg=all_2994 on theBenchmark for (2994ds/157Mi)
% 6.10/1.69 % (3977672)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3872439103:i=3394:sd=4:ss=included:sgt=64_2994 on theBenchmark for (2994ds/3394Mi)
% 6.10/1.69 % (3977673)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=2681530357:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2994 on theBenchmark for (2994ds/106Mi)
% 6.10/1.69 % (3977671)Instruction limit reached!
% 6.10/1.69 % (3977671)------------------------------
% 6.10/1.69 % (3977671)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.10/1.69 % (3977671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.10/1.69 % (3977671)CaDiCaL version: 2.1.3
% 6.10/1.69 % (3977671)Termination reason: Instruction limit
% 6.10/1.69 % (3977671)Termination phase: Saturation
% 6.10/1.69 % (3977671)Time elapsed: 0.103 s
% 6.10/1.69 % (3977671)Peak memory usage: 90 MB
% 6.10/1.69 % (3977671)Instructions burned: 157 (million)
% 6.10/1.69 % (3977673)Instruction limit reached!
% 6.10/1.69 % (3977673)------------------------------
% 6.10/1.69 % (3977673)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.10/1.69 % (3977673)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.10/1.69 % (3977673)CaDiCaL version: 2.1.3
% 6.10/1.69 % (3977673)Termination reason: Instruction limit
% 6.10/1.69 % (3977673)Termination phase: Saturation
% 6.10/1.69 % (3977673)Time elapsed: 0.055 s
% 6.10/1.69 % (3977673)Peak memory usage: 89 MB
% 6.10/1.69 % (3977673)Instructions burned: 107 (million)
% 6.10/1.69 % (3977670)Instruction limit reached!
% 6.10/1.69 % (3977670)------------------------------
% 6.10/1.69 % (3977670)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.10/1.69 % (3977670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.10/1.69 % (3977670)CaDiCaL version: 2.1.3
% 6.10/1.69 % (3977670)Termination reason: Instruction limit
% 6.10/1.69 % (3977670)Termination phase: Saturation
% 6.10/1.69 % (3977670)Time elapsed: 0.131 s
% 6.10/1.69 % (3977670)Peak memory usage: 90 MB
% 6.10/1.69 % (3977670)Instructions burned: 195 (million)
% 6.10/1.69 % (3977648)First to succeed.
% 6.10/1.69 % (3977648)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3977643"
% 6.10/1.69 % (3977678)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=4098194096:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 6.10/1.69 % (3977679)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=861329363:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2992 on theBenchmark for (2992ds/242Mi)
% 6.10/1.69 % (3977680)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2221820501:cond=fast:i=5208:av=off_2992 on theBenchmark for (2992ds/5208Mi)
% 6.10/1.69 % (3977678)Instruction limit reached!
% 6.10/1.69 % (3977678)------------------------------
% 6.10/1.69 % (3977678)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.10/1.69 % (3977678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.10/1.69 % (3977678)CaDiCaL version: 2.1.3
% 6.10/1.69 % (3977678)Termination reason: Instruction limit
% 6.10/1.69 % (3977678)Termination phase: Saturation
% 6.10/1.69 % (3977678)Time elapsed: 0.070 s
% 6.10/1.69 % (3977678)Peak memory usage: 90 MB
% 6.10/1.69 % (3977678)Instructions burned: 109 (million)
% 6.10/1.69 % (3977648)Refutation found. Thanks to Tanya!
% 6.10/1.69 % SZS status Unsatisfiable for theBenchmark
% 6.10/1.69 % SZS output start Proof for theBenchmark
% See solution above
% 7.70/1.89 % (3977648)------------------------------
% 7.70/1.89 % (3977648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.70/1.89 % (3977648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.70/1.89 % (3977648)CaDiCaL version: 2.1.3
% 7.70/1.89 % (3977648)Termination reason: Refutation
% 7.70/1.89 % (3977648)Time elapsed: 0.716 s
% 7.70/1.89 % (3977648)Peak memory usage: 139 MB
% 7.70/1.89 % (3977648)Instructions burned: 1918 (million)
% 7.70/1.89 % (3977648)------------------------------
% 7.70/1.89 % (3977648)------------------------------
% 7.70/1.89 % (3977643)Success in time 1.025 s
% 7.70/1.89 % Vampire exiting
%------------------------------------------------------------------------------