%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW470+2 : TPTP v9.3.1. Released v5.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n020.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:40:05 PM UTC 2026
% Result : Theorem 10.43s 1.97s
% Output : Refutation 10.43s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 23
% Syntax : Number of formulae : 106 ( 35 unt; 6 def)
% Number of atoms : 214 ( 48 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 194 ( 86 ~; 93 |; 1 &)
% ( 8 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 10 ( 3 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of predicates : 10 ( 8 usr; 7 prp; 0-2 aty)
% Number of functors : 47 ( 47 usr; 22 con; 0-4 aty)
% Number of variables : 83 ( 0 sgn 81 !; 2 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f5,axiom,
! [X0] : is_bool(finite419198954a_bool(X0)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gsy_c_Finite__Set_Ocomp__fun__idem_000tc__Hoare____Mirabelle____ddpglwnxwg__Otri) ).
fof(f17,axiom,
is_bool(bot_bot_bool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gsy_c_Orderings_Obot__class_Obot_000tc__HOL__Obool) ).
fof(f18,axiom,
is_bool(fFalse),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gsy_c_fFalse) ).
fof(f25,axiom,
! [X0,X1] : is_bool(hAPP_f540970102l_bool(X0,X1)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',gsy_c_hAPP_000tc__fun_Itc__Hoare____Mirabelle____ddpglwnxwg__Otriple_It__a_J_Mtc) ).
fof(f29,axiom,
! [X0] : hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(X0),bot_bo1181479936a_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_empty) ).
fof(f33,axiom,
! [X0,X1,X2] :
( hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(X1),X2))
=> ( hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(X0),X1))
=> hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(X0),X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_4_cut) ).
fof(f39,axiom,
! [X0,X1,X2,X3] :
( ! [X4,X5] :
( hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(X3,X4),X5))
=> hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(X0),hAPP_f1591852335a_bool(hAPP_H1641355846a_bool(insert873085594iple_a,hoare_1760757500iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_s1806633685e_bool(hAPP_f817621513e_bool(cOMBC_2027030106e_bool,fequal_state),X5)),X1,hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_a2036067514e_bool(X2,X4)))),bot_bo1181479936a_bool))) )
=> hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(X0),hAPP_f1591852335a_bool(hAPP_H1641355846a_bool(insert873085594iple_a,hoare_1760757500iple_a(X3,X1,X2)),bot_bo1181479936a_bool))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_10_escape) ).
fof(f56,axiom,
! [X0] : collec268032053iple_a(hAPP_H1190454433a_bool(fequal879838495iple_a,X0)) = hAPP_f1591852335a_bool(hAPP_H1641355846a_bool(insert873085594iple_a,X0),bot_bo1181479936a_bool),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_27_singleton__conv2) ).
fof(f76,axiom,
! [X0] :
( collec268032053iple_a(X0) = bot_bo1181479936a_bool
<=> ! [X1] : ~ hBOOL(hAPP_H1421470952a_bool(X0,X1)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_47_Collect__empty__eq) ).
fof(f153,axiom,
! [X0] :
( hBOOL(hAPP_H1421470952a_bool(bot_bo1181479936a_bool,X0))
<=> hBOOL(bot_bot_bool) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_124_bot__apply) ).
fof(f261,axiom,
! [X0] : collec268032053iple_a(X0) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_232_Collect__def) ).
fof(f442,axiom,
hBOOL(finite419198954a_bool(insert873085594iple_a)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_413_comp__fun__idem__insert) ).
fof(f737,axiom,
~ hBOOL(fFalse),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fFalse_1_1_U) ).
fof(f738,axiom,
! [X0] :
( is_bool(X0)
=> ( X0 = fTrue
| X0 = fFalse ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fFalse_1_1_T) ).
fof(f749,axiom,
! [X0,X1] :
( is_bool(X0)
=> hAPP_state_bool(hAPP_b2019457360e_bool(cOMBK_bool_state,X0),X1) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Com__Ostate_U) ).
fof(f755,axiom,
! [X0,X1] : hAPP_a2036067514e_bool(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,X0),X1) = X0,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBK_1_1_COMBK_000tc__fun_Itc__Com__Ostate_Mtc__HOL__Obool_J_000t__a_U) ).
fof(f830,conjecture,
hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(g),hAPP_f1591852335a_bool(hAPP_H1641355846a_bool(insert873085594iple_a,hoare_1760757500iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)))),bot_bo1181479936a_bool))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
fof(f831,negated_conjecture,
~ hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(g),hAPP_f1591852335a_bool(hAPP_H1641355846a_bool(insert873085594iple_a,hoare_1760757500iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)))),bot_bo1181479936a_bool))),
inference(negated_conjecture,[status(cth)],[f830]) ).
fof(f835,plain,
~ hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(g),hAPP_f1591852335a_bool(hAPP_H1641355846a_bool(insert873085594iple_a,hoare_1760757500iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)))),bot_bo1181479936a_bool))),
inference(flattening,[],[f831]) ).
fof(f839,plain,
! [X0,X1,X2] :
( hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(X0),X2))
| ~ hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(X0),X1))
| ~ hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(X1),X2)) ),
inference(ennf_transformation,[],[f33]) ).
fof(f840,plain,
! [X0,X1,X2] :
( hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(X0),X2))
| ~ hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(X0),X1))
| ~ hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(X1),X2)) ),
inference(flattening,[],[f839]) ).
fof(f849,plain,
! [X0,X1,X2,X3] :
( hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(X0),hAPP_f1591852335a_bool(hAPP_H1641355846a_bool(insert873085594iple_a,hoare_1760757500iple_a(X3,X1,X2)),bot_bo1181479936a_bool)))
| ? [X4,X5] :
( ~ hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(X0),hAPP_f1591852335a_bool(hAPP_H1641355846a_bool(insert873085594iple_a,hoare_1760757500iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_s1806633685e_bool(hAPP_f817621513e_bool(cOMBC_2027030106e_bool,fequal_state),X5)),X1,hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_a2036067514e_bool(X2,X4)))),bot_bo1181479936a_bool)))
& hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(X3,X4),X5)) ) ),
inference(ennf_transformation,[],[f39]) ).
fof(f1383,plain,
! [X0] :
( X0 = fTrue
| X0 = fFalse
| ~ is_bool(X0) ),
inference(ennf_transformation,[],[f738]) ).
fof(f1384,plain,
! [X0] :
( X0 = fTrue
| X0 = fFalse
| ~ is_bool(X0) ),
inference(flattening,[],[f1383]) ).
fof(f1386,plain,
! [X0,X1] :
( hAPP_state_bool(hAPP_b2019457360e_bool(cOMBK_bool_state,X0),X1) = X0
| ~ is_bool(X0) ),
inference(ennf_transformation,[],[f749]) ).
fof(f1394,plain,
! [X0] : is_bool(finite419198954a_bool(X0)),
inference(cnf_transformation,[],[f5]) ).
fof(f1406,plain,
is_bool(bot_bot_bool),
inference(cnf_transformation,[],[f17]) ).
fof(f1407,plain,
is_bool(fFalse),
inference(cnf_transformation,[],[f18]) ).
fof(f1414,plain,
! [X0,X1] : is_bool(hAPP_f540970102l_bool(X0,X1)),
inference(cnf_transformation,[],[f25]) ).
fof(f1418,plain,
! [X0] : hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(X0),bot_bo1181479936a_bool)),
inference(cnf_transformation,[],[f29]) ).
fof(f1428,plain,
! [X2,X0,X1] :
( hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(X0),X2))
| ~ hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(X0),X1))
| ~ hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(X1),X2)) ),
inference(cnf_transformation,[],[f840]) ).
fof(f1436,plain,
! [X2,X3,X0,X1] :
( hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(X3,sK0(X0,X1,X2,X3)),sK1(X0,X1,X2,X3)))
| hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(X0),hAPP_f1591852335a_bool(hAPP_H1641355846a_bool(insert873085594iple_a,hoare_1760757500iple_a(X3,X1,X2)),bot_bo1181479936a_bool))) ),
inference(cnf_transformation,[],[f849]) ).
fof(f1466,plain,
! [X0] : collec268032053iple_a(hAPP_H1190454433a_bool(fequal879838495iple_a,X0)) = hAPP_f1591852335a_bool(hAPP_H1641355846a_bool(insert873085594iple_a,X0),bot_bo1181479936a_bool),
inference(cnf_transformation,[],[f56]) ).
fof(f1496,plain,
! [X0,X1] :
( ~ hBOOL(hAPP_H1421470952a_bool(X0,X1))
| bot_bo1181479936a_bool != collec268032053iple_a(X0) ),
inference(cnf_transformation,[],[f76]) ).
fof(f1618,plain,
! [X0] :
( ~ hBOOL(bot_bot_bool)
| hBOOL(hAPP_H1421470952a_bool(bot_bo1181479936a_bool,X0)) ),
inference(cnf_transformation,[],[f153]) ).
fof(f1786,plain,
! [X0] : collec268032053iple_a(X0) = X0,
inference(cnf_transformation,[],[f261]) ).
fof(f2090,plain,
hBOOL(finite419198954a_bool(insert873085594iple_a)),
inference(cnf_transformation,[],[f442]) ).
fof(f2512,plain,
~ hBOOL(fFalse),
inference(cnf_transformation,[],[f737]) ).
fof(f2513,plain,
! [X0] :
( ~ is_bool(X0)
| fFalse = X0
| fTrue = X0 ),
inference(cnf_transformation,[],[f1384]) ).
fof(f2524,plain,
! [X0,X1] :
( ~ is_bool(X0)
| hAPP_state_bool(hAPP_b2019457360e_bool(cOMBK_bool_state,X0),X1) = X0 ),
inference(cnf_transformation,[],[f1386]) ).
fof(f2530,plain,
! [X0,X1] : hAPP_a2036067514e_bool(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,X0),X1) = X0,
inference(cnf_transformation,[],[f755]) ).
fof(f2605,plain,
~ hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(g),hAPP_f1591852335a_bool(hAPP_H1641355846a_bool(insert873085594iple_a,hoare_1760757500iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)))),bot_bo1181479936a_bool))),
inference(cnf_transformation,[],[f835]) ).
fof(f2776,definition,
( spl172_1
<=> ! [X0] : hBOOL(hAPP_H1421470952a_bool(bot_bo1181479936a_bool,X0)) ),
introduced(definition,[new_symbols(definition,[spl172_1])],[avatar_definition]) ).
fof(f2777,plain,
( ! [X0] : hBOOL(hAPP_H1421470952a_bool(bot_bo1181479936a_bool,X0))
| ~ spl172_1 ),
inference(avatar_component_clause,[],[f2776]) ).
fof(f2779,definition,
( spl172_2
<=> hBOOL(bot_bot_bool) ),
introduced(definition,[new_symbols(definition,[spl172_2])],[avatar_definition]) ).
fof(f2781,plain,
( ~ hBOOL(bot_bot_bool)
| spl172_2 ),
inference(avatar_component_clause,[],[f2779]) ).
fof(f2782,plain,
( spl172_1
| ~ spl172_2 ),
inference(avatar_split_clause,[],[f1618,f2779,f2776]) ).
fof(f2791,plain,
! [X0,X1] :
( ~ hBOOL(hAPP_H1421470952a_bool(X0,X1))
| bot_bo1181479936a_bool != X0 ),
inference(forward_demodulation,[],[f1496,f1786]) ).
fof(f2808,plain,
! [X0] :
( finite419198954a_bool(X0) = fFalse
| finite419198954a_bool(X0) = fTrue ),
inference(resolution,[],[f2513,f1394]) ).
fof(f2818,plain,
( bot_bot_bool = fFalse
| bot_bot_bool = fTrue ),
inference(resolution,[],[f2513,f1406]) ).
fof(f2826,plain,
! [X0,X1] :
( fFalse = hAPP_f540970102l_bool(X0,X1)
| fTrue = hAPP_f540970102l_bool(X0,X1) ),
inference(resolution,[],[f2513,f1414]) ).
fof(f2831,definition,
( spl172_3
<=> bot_bot_bool = fTrue ),
introduced(definition,[new_symbols(definition,[spl172_3])],[avatar_definition]) ).
fof(f2833,plain,
( bot_bot_bool = fTrue
| ~ spl172_3 ),
inference(avatar_component_clause,[],[f2831]) ).
fof(f2835,definition,
( spl172_4
<=> bot_bot_bool = fFalse ),
introduced(definition,[new_symbols(definition,[spl172_4])],[avatar_definition]) ).
fof(f2837,plain,
( bot_bot_bool = fFalse
| ~ spl172_4 ),
inference(avatar_component_clause,[],[f2835]) ).
fof(f2838,plain,
( spl172_3
| spl172_4 ),
inference(avatar_split_clause,[],[f2818,f2835,f2831]) ).
fof(f2865,plain,
( ! [X0] :
( finite419198954a_bool(X0) = fFalse
| finite419198954a_bool(X0) = bot_bot_bool )
| ~ spl172_3 ),
inference(forward_demodulation,[],[f2808,f2833]) ).
fof(f2883,plain,
( hBOOL(fFalse)
| bot_bot_bool = finite419198954a_bool(insert873085594iple_a)
| ~ spl172_3 ),
inference(superposition,[],[f2090,f2865]) ).
fof(f2885,plain,
( bot_bot_bool = finite419198954a_bool(insert873085594iple_a)
| ~ spl172_3 ),
inference(forward_subsumption_resolution,[],[f2883,f2512]) ).
fof(f2887,plain,
( hBOOL(bot_bot_bool)
| ~ spl172_3 ),
inference(superposition,[],[f2090,f2885]) ).
fof(f2889,plain,
( $false
| spl172_2
| ~ spl172_3 ),
inference(forward_subsumption_resolution,[],[f2887,f2781]) ).
fof(f2890,plain,
( spl172_2
| ~ spl172_3 ),
inference(avatar_contradiction_clause,[],[f2889]) ).
fof(f2891,plain,
( bot_bo1181479936a_bool != bot_bo1181479936a_bool
| ~ spl172_1 ),
inference(resolution,[],[f2777,f2791]) ).
fof(f2892,plain,
( $false
| ~ spl172_1 ),
inference(trivial_inequality_removal,[],[f2891]) ).
fof(f2893,plain,
~ spl172_1,
inference(avatar_contradiction_clause,[],[f2892]) ).
fof(f2933,plain,
( ! [X0] :
( finite419198954a_bool(X0) = fTrue
| finite419198954a_bool(X0) = bot_bot_bool )
| ~ spl172_4 ),
inference(forward_demodulation,[],[f2808,f2837]) ).
fof(f2941,plain,
( hBOOL(fTrue)
| bot_bot_bool = finite419198954a_bool(insert873085594iple_a)
| ~ spl172_4 ),
inference(superposition,[],[f2090,f2933]) ).
fof(f2944,definition,
( spl172_6
<=> bot_bot_bool = finite419198954a_bool(insert873085594iple_a) ),
introduced(definition,[new_symbols(definition,[spl172_6])],[avatar_definition]) ).
fof(f2946,plain,
( bot_bot_bool = finite419198954a_bool(insert873085594iple_a)
| ~ spl172_6 ),
inference(avatar_component_clause,[],[f2944]) ).
fof(f2948,definition,
( spl172_7
<=> hBOOL(fTrue) ),
introduced(definition,[new_symbols(definition,[spl172_7])],[avatar_definition]) ).
fof(f2950,plain,
( hBOOL(fTrue)
| ~ spl172_7 ),
inference(avatar_component_clause,[],[f2948]) ).
fof(f2951,plain,
( spl172_6
| spl172_7
| ~ spl172_4 ),
inference(avatar_split_clause,[],[f2941,f2835,f2948,f2944]) ).
fof(f2953,plain,
( hBOOL(bot_bot_bool)
| ~ spl172_6 ),
inference(superposition,[],[f2090,f2946]) ).
fof(f2955,plain,
( $false
| spl172_2
| ~ spl172_6 ),
inference(forward_subsumption_resolution,[],[f2953,f2781]) ).
fof(f2956,plain,
( spl172_2
| ~ spl172_6 ),
inference(avatar_contradiction_clause,[],[f2955]) ).
fof(f3014,plain,
! [X0] : fFalse = hAPP_state_bool(hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse),X0),
inference(resolution,[],[f2524,f1407]) ).
fof(f3025,plain,
( ! [X0] : bot_bot_bool = hAPP_state_bool(hAPP_b2019457360e_bool(cOMBK_bool_state,bot_bot_bool),X0)
| ~ spl172_4 ),
inference(forward_demodulation,[],[f3014,f2837]) ).
fof(f3136,plain,
! [X0] : hAPP_H1190454433a_bool(fequal879838495iple_a,X0) = hAPP_f1591852335a_bool(hAPP_H1641355846a_bool(insert873085594iple_a,X0),bot_bo1181479936a_bool),
inference(forward_demodulation,[],[f1466,f1786]) ).
fof(f3916,plain,
( ! [X0,X1] :
( fTrue = hAPP_f540970102l_bool(X0,X1)
| bot_bot_bool = hAPP_f540970102l_bool(X0,X1) )
| ~ spl172_4 ),
inference(forward_demodulation,[],[f2826,f2837]) ).
fof(f4635,plain,
! [X0] :
( ~ hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(g),X0))
| ~ hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(X0),hAPP_f1591852335a_bool(hAPP_H1641355846a_bool(insert873085594iple_a,hoare_1760757500iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)))),bot_bo1181479936a_bool))) ),
inference(resolution,[],[f1428,f2605]) ).
fof(f4642,plain,
! [X0] :
( ~ hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(X0),hAPP_H1190454433a_bool(fequal879838495iple_a,hoare_1760757500iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b))))))
| ~ hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(g),X0)) ),
inference(forward_demodulation,[],[f4635,f3136]) ).
fof(f4643,plain,
( ! [X0] :
( ~ hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(X0),hAPP_H1190454433a_bool(fequal879838495iple_a,hoare_1760757500iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,bot_bot_bool)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b))))))
| ~ hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(g),X0)) )
| ~ spl172_4 ),
inference(forward_demodulation,[],[f4642,f2837]) ).
fof(f4647,plain,
( ! [X0] :
( ~ hBOOL(fTrue)
| ~ hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(g),X0))
| bot_bot_bool = hAPP_f540970102l_bool(hoare_606018542rivs_a(X0),hAPP_H1190454433a_bool(fequal879838495iple_a,hoare_1760757500iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,bot_bot_bool)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b))))) )
| ~ spl172_4 ),
inference(superposition,[],[f4643,f3916]) ).
fof(f4648,plain,
( ! [X0] :
( ~ hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(g),X0))
| bot_bot_bool = hAPP_f540970102l_bool(hoare_606018542rivs_a(X0),hAPP_H1190454433a_bool(fequal879838495iple_a,hoare_1760757500iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,bot_bot_bool)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b))))) )
| ~ spl172_4
| ~ spl172_7 ),
inference(forward_subsumption_resolution,[],[f4647,f2950]) ).
fof(f4764,plain,
( bot_bot_bool = hAPP_f540970102l_bool(hoare_606018542rivs_a(bot_bo1181479936a_bool),hAPP_H1190454433a_bool(fequal879838495iple_a,hoare_1760757500iple_a(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,bot_bot_bool)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)))))
| ~ spl172_4
| ~ spl172_7 ),
inference(resolution,[],[f4648,f1418]) ).
fof(f22583,plain,
! [X2,X3,X0,X1] :
( hBOOL(hAPP_f540970102l_bool(hoare_606018542rivs_a(X0),hAPP_H1190454433a_bool(fequal879838495iple_a,hoare_1760757500iple_a(X3,X1,X2))))
| hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(X3,sK0(X0,X1,X2,X3)),sK1(X0,X1,X2,X3))) ),
inference(forward_demodulation,[],[f1436,f3136]) ).
fof(f22706,plain,
( hBOOL(bot_bot_bool)
| hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,bot_bot_bool)),sK0(bot_bo1181479936a_bool,c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)),hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,bot_bot_bool)))),sK1(bot_bo1181479936a_bool,c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)),hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,bot_bot_bool)))))
| ~ spl172_4
| ~ spl172_7 ),
inference(superposition,[],[f22583,f4764]) ).
fof(f22720,plain,
( hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,bot_bot_bool)),sK0(bot_bo1181479936a_bool,c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)),hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,bot_bot_bool)))),sK1(bot_bo1181479936a_bool,c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)),hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,bot_bot_bool)))))
| spl172_2
| ~ spl172_4
| ~ spl172_7 ),
inference(forward_subsumption_resolution,[],[f22706,f2781]) ).
fof(f22769,plain,
( hBOOL(hAPP_state_bool(hAPP_b2019457360e_bool(cOMBK_bool_state,bot_bot_bool),sK1(bot_bo1181479936a_bool,c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(hAPP_f375255701e_bool(cOMBB_145932198bool_a,cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(hAPP_f1178339559l_bool(cOMBB_1355796797bool_a,hAPP_f1561913689l_bool(cOMBB_188601460_state,fconj)),p))),hAPP_f1759915619e_bool(hAPP_f2073279419e_bool(cOMBB_160679318_state,fNot),b)),hAPP_f762886889e_bool(cOMBK_1458035955bool_a,hAPP_b2019457360e_bool(cOMBK_bool_state,bot_bot_bool)))))
| spl172_2
| ~ spl172_4
| ~ spl172_7 ),
inference(forward_demodulation,[],[f22720,f2530]) ).
fof(f22810,plain,
( hBOOL(bot_bot_bool)
| spl172_2
| ~ spl172_4
| ~ spl172_7 ),
inference(forward_demodulation,[],[f22769,f3025]) ).
fof(f22854,plain,
( $false
| spl172_2
| ~ spl172_4
| ~ spl172_7 ),
inference(forward_subsumption_resolution,[],[f22810,f2781]) ).
fof(f22855,plain,
( spl172_2
| ~ spl172_4
| ~ spl172_7 ),
inference(avatar_contradiction_clause,[],[f22854]) ).
cnf(s1,plain,
( spl172_1
| ~ spl172_2 ),
inference(sat_conversion,[],[f2782]) ).
cnf(s2,plain,
( spl172_3
| spl172_4 ),
inference(sat_conversion,[],[f2838]) ).
cnf(s4,plain,
( spl172_2
| ~ spl172_3 ),
inference(sat_conversion,[],[f2890]) ).
cnf(s5,plain,
~ spl172_1,
inference(sat_conversion,[],[f2893]) ).
cnf(s6,plain,
( ~ spl172_4
| spl172_6
| spl172_7 ),
inference(sat_conversion,[],[f2951]) ).
cnf(s7,plain,
( spl172_2
| ~ spl172_6 ),
inference(sat_conversion,[],[f2956]) ).
cnf(s21,plain,
( spl172_2
| ~ spl172_4
| ~ spl172_7 ),
inference(sat_conversion,[],[f22855]) ).
cnf(s26,plain,
~ spl172_2,
inference(rat,[],[s1,s5]) ).
cnf(s27,plain,
~ spl172_6,
inference(rat,[],[s7,s26]) ).
cnf(s28,plain,
~ spl172_3,
inference(rat,[],[s4,s26]) ).
cnf(s29,plain,
spl172_4,
inference(rat,[],[s2,s28]) ).
cnf(s31,plain,
~ spl172_7,
inference(rat,[],[s21,s26,s29]) ).
cnf(s32,plain,
$false,
inference(rat,[],[s6,s27,s31,s29]) ).
fof(f22866,plain,
$false,
inference(avatar_sat_refutation,[],[s32]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW470+2 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.20 % Computer : n020.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Mon Sep 28 14:03:23 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.09/0.23 Running first-order model finding
% 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.16/1.79 % (178537)Will run a generic schedule for satisfiability detection.
% 9.16/1.79 % (178547)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2901918299:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 9.16/1.79 % (178543)% WARNING: option uhcvi not known.
% 9.16/1.79 % (178542)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3253376771_2999 on theBenchmark for (2999ds/0Mi)
% 9.16/1.79 % (178544)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1280218375:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 9.16/1.79 % (178545)dis+10_1_sil=32000:sp=arity:random_seed=2711518285:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 9.16/1.79 % (178548)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1144436187:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 9.16/1.79 % (178543)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3174211685:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 9.16/1.79 % (178546)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=699711852:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 9.16/1.79 % (178547)Instruction limit reached!
% 9.16/1.79 % (178547)------------------------------
% 9.16/1.79 % (178547)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.16/1.79 % (178547)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.16/1.79 % (178547)CaDiCaL version: 2.1.3
% 9.16/1.79 % (178547)Termination reason: Instruction limit
% 9.16/1.79 % (178547)Termination phase: Saturation
% 9.16/1.79 % (178547)Time elapsed: 0.036 s
% 9.16/1.79 % (178547)Peak memory usage: 14 MB
% 9.16/1.79 % (178547)Instructions burned: 132 (million)
% 9.16/1.79 % (178556)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2235625125:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 9.16/1.79 % (178545)Instruction limit reached!
% 9.16/1.79 % (178545)------------------------------
% 9.16/1.79 % (178545)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.16/1.79 % (178545)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.16/1.79 % (178545)CaDiCaL version: 2.1.3
% 9.16/1.79 % (178545)Termination reason: Instruction limit
% 9.16/1.79 % (178545)Termination phase: Saturation
% 9.16/1.79 % (178545)Time elapsed: 0.053 s
% 9.16/1.79 % (178545)Peak memory usage: 14 MB
% 9.16/1.79 % (178545)Instructions burned: 104 (million)
% 9.16/1.79 % (178546)Instruction limit reached!
% 9.16/1.79 % (178546)------------------------------
% 9.16/1.79 % (178546)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.16/1.79 % (178546)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.16/1.79 % (178546)CaDiCaL version: 2.1.3
% 9.16/1.79 % (178546)Termination reason: Instruction limit
% 9.16/1.79 % (178546)Termination phase: Saturation
% 9.16/1.79 % (178546)Time elapsed: 0.054 s
% 9.16/1.79 % (178546)Peak memory usage: 14 MB
% 9.16/1.79 % (178546)Instructions burned: 117 (million)
% 9.16/1.79 % (178558)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=138323768:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 9.16/1.79 % (178559)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=881353188:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 9.16/1.79 % (178548)Instruction limit reached!
% 9.16/1.79 % (178548)------------------------------
% 9.16/1.79 % (178548)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.16/1.79 % (178548)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.16/1.79 % (178548)CaDiCaL version: 2.1.3
% 9.16/1.79 % (178548)Termination reason: Instruction limit
% 9.16/1.79 % (178548)Termination phase: Saturation
% 9.16/1.79 % (178548)Time elapsed: 0.089 s
% 9.16/1.79 % (178548)Peak memory usage: 14 MB
% 9.16/1.79 % (178548)Instructions burned: 160 (million)
% 9.16/1.79 % (178562)ott-21_1_sil=16000:fs=off:random_seed=3132214718:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 9.16/1.79 % (178558)Instruction limit reached!
% 9.16/1.79 % (178558)------------------------------
% 9.16/1.79 % (178558)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 9.16/1.79 % (178558)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.16/1.79 % (178558)CaDiCaL version: 2.1.3
% 9.16/1.79 % (178558)Termination reason: Instruction limit
% 10.43/1.97 % (178558)Termination phase: Saturation
% 10.43/1.97 % (178558)Time elapsed: 0.064 s
% 10.43/1.97 % (178558)Peak memory usage: 14 MB
% 10.43/1.97 % (178558)Instructions burned: 132 (million)
% 10.43/1.97 % (178564)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1344802572:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 10.43/1.97 % (178562)Instruction limit reached!
% 10.43/1.97 % (178562)------------------------------
% 10.43/1.97 % (178562)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.43/1.97 % (178562)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.43/1.97 % (178562)CaDiCaL version: 2.1.3
% 10.43/1.97 % (178562)Termination reason: Instruction limit
% 10.43/1.97 % (178562)Termination phase: Saturation
% 10.43/1.97 % (178562)Time elapsed: 0.094 s
% 10.43/1.97 % (178562)Peak memory usage: 15 MB
% 10.43/1.97 % (178562)Instructions burned: 181 (million)
% 10.43/1.97 % (178556)Instruction limit reached!
% 10.43/1.97 % (178556)------------------------------
% 10.43/1.97 % (178556)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.43/1.97 % (178556)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.43/1.97 % (178556)CaDiCaL version: 2.1.3
% 10.43/1.97 % (178556)Termination reason: Instruction limit
% 10.43/1.97 % (178556)Termination phase: Finite model building preprocessing
% 10.43/1.97 % (178556)Time elapsed: 0.177 s
% 10.43/1.97 % (178556)Peak memory usage: 23 MB
% 10.43/1.97 % (178556)Instructions burned: 714 (million)
% 10.43/1.97 % (178566)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=661000425:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 10.43/1.97 % (178567)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1293749250:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 10.43/1.97 % TRYING [1]
% 10.43/1.97 % TRYING [2]
% 10.43/1.97 % (178564)Instruction limit reached!
% 10.43/1.97 % (178564)------------------------------
% 10.43/1.97 % (178564)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.43/1.97 % (178564)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.43/1.97 % (178564)CaDiCaL version: 2.1.3
% 10.43/1.97 % (178564)Termination reason: Instruction limit
% 10.43/1.97 % (178564)Termination phase: Saturation
% 10.43/1.97 % (178564)Time elapsed: 0.266 s
% 10.43/1.97 % (178564)Peak memory usage: 15 MB
% 10.43/1.97 % (178564)Instructions burned: 478 (million)
% 10.43/1.97 % (178570)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=4013061033:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 10.43/1.97 % (178559)Instruction limit reached!
% 10.43/1.97 % (178559)------------------------------
% 10.43/1.97 % (178559)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.43/1.97 % (178559)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.43/1.97 % (178559)CaDiCaL version: 2.1.3
% 10.43/1.97 % (178559)Termination reason: Instruction limit
% 10.43/1.97 % (178559)Termination phase: Saturation
% 10.43/1.97 % (178559)Time elapsed: 0.420 s
% 10.43/1.97 % (178559)Peak memory usage: 20 MB
% 10.43/1.97 % (178559)Instructions burned: 685 (million)
% 10.43/1.97 % (178572)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2602800704:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 10.43/1.97 % TRYING [3]
% 10.43/1.97 % (178567)Instruction limit reached!
% 10.43/1.97 % (178567)------------------------------
% 10.43/1.97 % (178567)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.43/1.97 % (178567)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.43/1.97 % (178567)CaDiCaL version: 2.1.3
% 10.43/1.97 % (178567)Termination reason: Instruction limit
% 10.43/1.97 % (178567)Termination phase: Saturation
% 10.43/1.97 % (178567)Time elapsed: 0.347 s
% 10.43/1.97 % (178567)Peak memory usage: 26 MB
% 10.43/1.97 % (178567)Instructions burned: 1182 (million)
% 10.43/1.97 % (178574)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3608117738:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 10.43/1.97 % TRYING [1]
% 10.43/1.97 % (178566)Instruction limit reached!
% 10.43/1.97 % (178566)------------------------------
% 10.43/1.97 % (178566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.43/1.97 % (178566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.43/1.97 % (178566)CaDiCaL version: 2.1.3
% 10.43/1.97 % (178566)Termination reason: Instruction limit
% 10.43/1.97 % (178566)Termination phase: Finite model building constraint generation
% 10.43/1.97 % (178566)Time elapsed: 0.405 s
% 10.43/1.97 % (178566)Peak memory usage: 27 MB
% 10.43/1.97 % (178566)Instructions burned: 867 (million)
% 10.43/1.97 % (178576)fmb+10_1_sil=64000:random_seed=1012147823:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 10.43/1.97 % (178574)Instruction limit reached!
% 10.43/1.97 % (178574)------------------------------
% 10.43/1.97 % (178574)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.43/1.97 % (178574)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.43/1.97 % (178574)CaDiCaL version: 2.1.3
% 10.43/1.97 % (178574)Termination reason: Instruction limit
% 10.43/1.97 % (178574)Termination phase: Saturation
% 10.43/1.97 % (178574)Time elapsed: 0.236 s
% 10.43/1.97 % (178574)Peak memory usage: 21 MB
% 10.43/1.97 % (178574)Instructions burned: 883 (million)
% 10.43/1.97 % (178578)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2699588985:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 10.43/1.97 % (178570)Instruction limit reached!
% 10.43/1.97 % (178570)------------------------------
% 10.43/1.97 % (178570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.43/1.97 % (178570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.43/1.97 % (178570)CaDiCaL version: 2.1.3
% 10.43/1.97 % (178570)Termination reason: Instruction limit
% 10.43/1.97 % (178570)Termination phase: Finite model building constraint generation
% 10.43/1.97 % (178570)Time elapsed: 0.422 s
% 10.43/1.97 % (178570)Peak memory usage: 42 MB
% 10.43/1.97 % (178570)Instructions burned: 889 (million)
% 10.43/1.97 % (178580)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1997041692:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 10.43/1.97 % (178572)Instruction limit reached!
% 10.43/1.97 % (178572)------------------------------
% 10.43/1.97 % (178572)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.43/1.97 % (178572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.43/1.97 % (178572)CaDiCaL version: 2.1.3
% 10.43/1.97 % (178572)Termination reason: Instruction limit
% 10.43/1.97 % (178572)Termination phase: Saturation
% 10.43/1.97 % (178572)Time elapsed: 0.379 s
% 10.43/1.97 % (178572)Peak memory usage: 21 MB
% 10.43/1.97 % (178572)Instructions burned: 692 (million)
% 10.43/1.97 % (178582)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=1561382548:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 10.43/1.97 % TRYING [1]
% 10.43/1.97 % (178578)Cannot represent all propositional literals internally
% 10.43/1.97 % (178578)Refutation not found, incomplete strategy
% 10.43/1.97 % (178578)------------------------------
% 10.43/1.97 % (178578)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.43/1.97 % (178578)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.43/1.97 % (178578)CaDiCaL version: 2.1.3
% 10.43/1.97 % (178578)Termination reason: Refutation not found, incomplete strategy
% 10.43/1.97 % (178578)Time elapsed: 0.190 s
% 10.43/1.97 % (178578)Peak memory usage: 25 MB
% 10.43/1.97 % (178578)Instructions burned: 751 (million)
% 10.43/1.97 % (178578)------------------------------
% 10.43/1.97 % (178578)------------------------------
% 10.43/1.97 % TRYING [2]
% 10.43/1.97 % (178584)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=353383644:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi)
% 10.43/1.97 % TRYING [4]
% 10.43/1.97 % TRYING [8]
% 10.43/1.97 % (178580)Instruction limit reached!
% 10.43/1.97 % (178580)------------------------------
% 10.43/1.97 % (178580)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.43/1.97 % (178580)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.43/1.97 % (178580)CaDiCaL version: 2.1.3
% 10.43/1.97 % (178580)Termination reason: Instruction limit
% 10.43/1.97 % (178580)Termination phase: Finite model building constraint generation
% 10.43/1.97 % (178580)Time elapsed: 0.422 s
% 10.43/1.97 % (178580)Peak memory usage: 35 MB
% 10.43/1.97 % (178580)Instructions burned: 923 (million)
% 10.43/1.97 % (178586)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3880624003:i=6324_2986 on theBenchmark for (2986ds/6324Mi)
% 10.43/1.97 % (178584)Instruction limit reached!
% 10.43/1.97 % (178584)------------------------------
% 10.43/1.97 % (178584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.43/1.97 % (178584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.43/1.97 % (178584)CaDiCaL version: 2.1.3
% 10.43/1.97 % (178584)Termination reason: Instruction limit
% 10.43/1.97 % (178584)Termination phase: Saturation
% 10.43/1.97 % (178584)Time elapsed: 0.431 s
% 10.43/1.97 % (178584)Peak memory usage: 26 MB
% 10.43/1.97 % (178584)Instructions burned: 1475 (million)
% 10.43/1.97 % (178588)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3839197265:fmbsr=2.30978:i=2174_2984 on theBenchmark for (2984ds/2174Mi)
% 10.43/1.97 % TRYING [3]
% 10.43/1.97 % (178582) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-178537-178582"...
% 10.43/1.97 % (178582)...printing done.
% 10.43/1.97 % (178582)Refutation found. Thanks to Tanya!
% 10.43/1.97 % SZS status Theorem for theBenchmark
% 10.43/1.97 % SZS output start Proof for theBenchmark
% See solution above
% 10.43/1.97 % (178582)------------------------------
% 10.43/1.97 % (178582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 10.43/1.97 % (178582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.43/1.97 % (178582)CaDiCaL version: 2.1.3
% 10.43/1.97 % (178582)Termination reason: Refutation
% 10.43/1.97 % (178582)Time elapsed: 0.710 s
% 10.43/1.97 % (178582)Peak memory usage: 23 MB
% 10.43/1.97 % (178582)Instructions burned: 1233 (million)
% 10.43/1.97 % (178537)Success in time 1.727 s
% 10.43/1.97 % Vampire exiting
%------------------------------------------------------------------------------