%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SWW470_1 : 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 : n002.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 0.17s 0.34s
% Output : Refutation 0.17s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 23
% Syntax : Number of formulae : 115 ( 42 unt; 0 typ; 7 def)
% Number of atoms : 246 ( 33 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 237 ( 106 ~; 105 |; 7 &)
% ( 8 <=>; 11 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 4 avg)
% Maximal term depth : 11 ( 2 avg)
% Number of types : 46 ( 45 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 10 ( 8 usr; 8 prp; 0-2 aty)
% Number of functors : 137 ( 137 usr; 30 con; 0-6 aty)
% Number of variables : 106 ( 0 sgn 100 !; 6 ?; 106 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
x_a: $tType ).
tff(type_def_6,type,
com: $tType ).
tff(type_def_7,type,
state: $tType ).
tff(type_def_8,type,
bool: $tType ).
tff(type_def_9,type,
hoare_1927711152iple_a: $tType ).
tff(type_def_10,type,
fun_a_fun_state_bool: $tType ).
tff(type_def_11,type,
fun_a_1632297036l_bool: $tType ).
tff(type_def_12,type,
fun_a_998512028e_bool: $tType ).
tff(type_def_13,type,
fun_a_2117018159e_bool: $tType ).
tff(type_def_14,type,
fun_state_bool: $tType ).
tff(type_def_15,type,
fun_st1506752259e_bool: $tType ).
tff(type_def_16,type,
fun_st2063251938l_bool: $tType ).
tff(type_def_17,type,
fun_bool_bool: $tType ).
tff(type_def_18,type,
fun_bo675861616e_bool: $tType ).
tff(type_def_19,type,
fun_bo1936561970e_bool: $tType ).
tff(type_def_20,type,
fun_bo1549164019l_bool: $tType ).
tff(type_def_21,type,
fun_Ho1877127206a_bool: $tType ).
tff(type_def_22,type,
fun_Ho843200573iple_a: $tType ).
tff(type_def_23,type,
fun_Ho957066028l_bool: $tType ).
tff(type_def_24,type,
fun_Ho440810351a_bool: $tType ).
tff(type_def_25,type,
fun_Ho333840202iple_a: $tType ).
tff(type_def_26,type,
fun_Ho525994229l_bool: $tType ).
tff(type_def_27,type,
fun_Ho1630563774a_bool: $tType ).
tff(type_def_28,type,
fun_fu2118559873l_bool: $tType ).
tff(type_def_29,type,
fun_fu1591723597e_bool: $tType ).
tff(type_def_30,type,
fun_fu2008829792e_bool: $tType ).
tff(type_def_31,type,
fun_fu222103665e_bool: $tType ).
tff(type_def_32,type,
fun_fu734682033e_bool: $tType ).
tff(type_def_33,type,
fun_fu281355805e_bool: $tType ).
tff(type_def_34,type,
fun_fu373216837e_bool: $tType ).
tff(type_def_35,type,
fun_fu1658206819l_bool: $tType ).
tff(type_def_36,type,
fun_fu402792811e_bool: $tType ).
tff(type_def_37,type,
fun_fu1219323149e_bool: $tType ).
tff(type_def_38,type,
fun_fu1047394976e_bool: $tType ).
tff(type_def_39,type,
fun_fu832487784l_bool: $tType ).
tff(type_def_40,type,
fun_fu1033095803iple_a: $tType ).
tff(type_def_41,type,
fun_fu1585556401a_bool: $tType ).
tff(type_def_42,type,
fun_fu269925879l_bool: $tType ).
tff(type_def_43,type,
fun_fu276214394a_bool: $tType ).
tff(type_def_44,type,
fun_fu1644852787l_bool: $tType ).
tff(type_def_45,type,
fun_fu1249172034a_bool: $tType ).
tff(type_def_46,type,
fun_fu1563903738a_bool: $tType ).
tff(type_def_47,type,
fun_fu893561155a_bool: $tType ).
tff(type_def_48,type,
fun_fu1192765369a_bool: $tType ).
tff(type_def_49,type,
fun_fu1905604217a_bool: $tType ).
tff(func_def_0,type,
cOMBB_160679318_state: fun_bool_bool > fun_fu373216837e_bool ).
tff(func_def_1,type,
cOMBB_213049548iple_a: fun_bool_bool > fun_fu1585556401a_bool ).
tff(func_def_2,type,
cOMBB_188601460_state: fun_bo1549164019l_bool > fun_fu1658206819l_bool ).
tff(func_def_3,type,
cOMBB_196465322iple_a: fun_bo1549164019l_bool > fun_fu269925879l_bool ).
tff(func_def_4,type,
cOMBB_1355796797bool_a: fun_fu1658206819l_bool > fun_fu2118559873l_bool ).
tff(func_def_5,type,
cOMBB_1348041619bool_a: fun_fu1219323149e_bool > fun_fu1591723597e_bool ).
tff(func_def_6,type,
cOMBB_145932198bool_a: fun_fu1047394976e_bool > fun_fu2008829792e_bool ).
tff(func_def_7,type,
cOMBB_1083611331iple_a: fun_fu832487784l_bool > fun_fu1563903738a_bool ).
tff(func_def_8,type,
cOMBC_41962815e_bool: fun_fu222103665e_bool ).
tff(func_def_9,type,
cOMBC_892787026e_bool: fun_fu734682033e_bool ).
tff(func_def_10,type,
cOMBC_2027030106e_bool: fun_fu402792811e_bool ).
tff(func_def_11,type,
cOMBC_231445413l_bool: fun_fu1219323149e_bool ).
tff(func_def_12,type,
cOMBC_671859290a_bool: fun_fu893561155a_bool ).
tff(func_def_13,type,
cOMBC_862840740l_bool: fun_fu1192765369a_bool ).
tff(func_def_14,type,
cOMBC_825881325a_bool: fun_fu1905604217a_bool ).
tff(func_def_15,type,
cOMBK_bool_state: bool > fun_state_bool ).
tff(func_def_16,type,
cOMBK_712844119iple_a: bool > fun_Ho1877127206a_bool ).
tff(func_def_17,type,
cOMBK_1458035955bool_a: fun_state_bool > fun_a_fun_state_bool ).
tff(func_def_18,type,
cOMBS_1378840469l_bool: fun_fu1047394976e_bool ).
tff(func_def_19,type,
cOMBS_2061548107l_bool: fun_fu1249172034a_bool ).
tff(func_def_20,type,
skip: com ).
tff(func_def_21,type,
semi: ( com * com ) > com ).
tff(func_def_22,type,
finite68738179iple_a: fun_fu832487784l_bool ).
tff(func_def_23,type,
finite2098837632iple_a: ( fun_Ho333840202iple_a * fun_Ho1877127206a_bool ) > fun_Ho1877127206a_bool ).
tff(func_def_24,type,
finite1943414032iple_a: fun_Ho333840202iple_a > fun_fu1033095803iple_a ).
tff(func_def_25,type,
finite148164294iple_a: ( fun_Ho333840202iple_a * hoare_1927711152iple_a * fun_Ho1877127206a_bool ) > fun_Ho1877127206a_bool ).
tff(func_def_26,type,
finite83514413iple_a: ( fun_Ho333840202iple_a * fun_fu1033095803iple_a ) > bool ).
tff(func_def_27,type,
finite1511031594iple_a: ( fun_Ho333840202iple_a * fun_fu1033095803iple_a ) > bool ).
tff(func_def_28,type,
the_Ho1307659873iple_a: fun_fu1033095803iple_a ).
tff(func_def_29,type,
hoare_1617968510rivs_a: fun_Ho1877127206a_bool > fun_fu832487784l_bool ).
tff(func_def_30,type,
hoare_1652181356iple_a: ( fun_a_fun_state_bool * com * fun_a_fun_state_bool ) > hoare_1927711152iple_a ).
tff(func_def_31,type,
bot_bot_bool: bool ).
tff(func_def_32,type,
bot_bo1208640912a_bool: fun_Ho1877127206a_bool ).
tff(func_def_33,type,
collec829051333iple_a: fun_Ho1877127206a_bool > fun_Ho1877127206a_bool ).
tff(func_def_34,type,
insert1434104874iple_a: fun_Ho1630563774a_bool ).
tff(func_def_35,type,
the_el1997360207iple_a: fun_fu1033095803iple_a ).
tff(func_def_36,type,
fFalse: bool ).
tff(func_def_37,type,
fNot: fun_bool_bool ).
tff(func_def_38,type,
fTrue: bool ).
tff(func_def_39,type,
fconj: fun_bo1549164019l_bool ).
tff(func_def_40,type,
fdisj: fun_bo1549164019l_bool ).
tff(func_def_41,type,
fequal_state: fun_st1506752259e_bool ).
tff(func_def_42,type,
fequal1440857775iple_a: fun_Ho440810351a_bool ).
tff(func_def_43,type,
fequal1285825639a_bool: fun_fu1644852787l_bool ).
tff(func_def_44,type,
fimplies: fun_bo1549164019l_bool ).
tff(func_def_45,type,
hAPP_a2036067514e_bool: ( fun_a_fun_state_bool * x_a ) > fun_state_bool ).
tff(func_def_46,type,
hAPP_a849909144l_bool: ( fun_a_1632297036l_bool * x_a ) > fun_st2063251938l_bool ).
tff(func_def_47,type,
hAPP_a723219176e_bool: ( fun_a_998512028e_bool * x_a ) > fun_bo1936561970e_bool ).
tff(func_def_48,type,
hAPP_a1200519163e_bool: ( fun_a_2117018159e_bool * x_a ) > fun_fu373216837e_bool ).
tff(func_def_49,type,
hAPP_state_bool: ( fun_state_bool * state ) > bool ).
tff(func_def_50,type,
hAPP_s1806633685e_bool: ( fun_st1506752259e_bool * state ) > fun_state_bool ).
tff(func_def_51,type,
hAPP_s58564346l_bool: ( fun_st2063251938l_bool * state ) > fun_bool_bool ).
tff(func_def_52,type,
hAPP_bool_bool: ( fun_bool_bool * bool ) > bool ).
tff(func_def_53,type,
hAPP_b540892988e_bool: ( fun_bo675861616e_bool * bool ) > fun_a_fun_state_bool ).
tff(func_def_54,type,
hAPP_b2019457360e_bool: ( fun_bo1936561970e_bool * bool ) > fun_state_bool ).
tff(func_def_55,type,
hAPP_b589554111l_bool: ( fun_bo1549164019l_bool * bool ) > fun_bool_bool ).
tff(func_def_56,type,
hAPP_H1448631928a_bool: ( fun_Ho1877127206a_bool * hoare_1927711152iple_a ) > bool ).
tff(func_def_57,type,
hAPP_H963118037iple_a: ( fun_Ho843200573iple_a * hoare_1927711152iple_a ) > hoare_1927711152iple_a ).
tff(func_def_58,type,
hAPP_H1487873860l_bool: ( fun_Ho957066028l_bool * hoare_1927711152iple_a ) > fun_bool_bool ).
tff(func_def_59,type,
hAPP_H1027145665a_bool: ( fun_Ho440810351a_bool * hoare_1927711152iple_a ) > fun_Ho1877127206a_bool ).
tff(func_def_60,type,
hAPP_H1700437986iple_a: ( fun_Ho333840202iple_a * hoare_1927711152iple_a ) > fun_Ho843200573iple_a ).
tff(func_def_61,type,
hAPP_H694056973l_bool: ( fun_Ho525994229l_bool * hoare_1927711152iple_a ) > fun_fu832487784l_bool ).
tff(func_def_62,type,
hAPP_H1975128022a_bool: ( fun_Ho1630563774a_bool * hoare_1927711152iple_a ) > fun_fu1585556401a_bool ).
tff(func_def_63,type,
hAPP_f1509969235l_bool: ( fun_fu2118559873l_bool * fun_a_fun_state_bool ) > fun_a_1632297036l_bool ).
tff(func_def_64,type,
hAPP_f340725611e_bool: ( fun_fu1591723597e_bool * fun_a_1632297036l_bool ) > fun_a_998512028e_bool ).
tff(func_def_65,type,
hAPP_f963367678e_bool: ( fun_fu2008829792e_bool * fun_a_1632297036l_bool ) > fun_a_2117018159e_bool ).
tff(func_def_66,type,
hAPP_f1824947087e_bool: ( fun_fu222103665e_bool * fun_a_998512028e_bool ) > fun_bo675861616e_bool ).
tff(func_def_67,type,
hAPP_f1261923407e_bool: ( fun_fu734682033e_bool * fun_a_2117018159e_bool ) > fun_fu281355805e_bool ).
tff(func_def_68,type,
hAPP_f762886889e_bool: ( fun_fu281355805e_bool * fun_state_bool ) > fun_a_fun_state_bool ).
tff(func_def_69,type,
hAPP_f1759915619e_bool: ( fun_fu373216837e_bool * fun_state_bool ) > fun_state_bool ).
tff(func_def_70,type,
hAPP_f1259673775l_bool: ( fun_fu1658206819l_bool * fun_state_bool ) > fun_st2063251938l_bool ).
tff(func_def_71,type,
hAPP_f817621513e_bool: ( fun_fu402792811e_bool * fun_st1506752259e_bool ) > fun_st1506752259e_bool ).
tff(func_def_72,type,
hAPP_f167292325e_bool: ( fun_fu1219323149e_bool * fun_st2063251938l_bool ) > fun_bo1936561970e_bool ).
tff(func_def_73,type,
hAPP_f644196280e_bool: ( fun_fu1047394976e_bool * fun_st2063251938l_bool ) > fun_fu373216837e_bool ).
tff(func_def_74,type,
hAPP_f1454306822l_bool: ( fun_fu832487784l_bool * fun_Ho1877127206a_bool ) > bool ).
tff(func_def_75,type,
hAPP_f490779847iple_a: ( fun_fu1033095803iple_a * fun_Ho1877127206a_bool ) > hoare_1927711152iple_a ).
tff(func_def_76,type,
hAPP_f16502863a_bool: ( fun_fu1585556401a_bool * fun_Ho1877127206a_bool ) > fun_Ho1877127206a_bool ).
tff(func_def_77,type,
hAPP_f749678531l_bool: ( fun_fu269925879l_bool * fun_Ho1877127206a_bool ) > fun_Ho957066028l_bool ).
tff(func_def_78,type,
hAPP_f993216280a_bool: ( fun_fu276214394a_bool * fun_Ho1877127206a_bool ) > fun_Ho440810351a_bool ).
tff(func_def_79,type,
hAPP_f625100287l_bool: ( fun_fu1644852787l_bool * fun_Ho1877127206a_bool ) > fun_fu832487784l_bool ).
tff(func_def_80,type,
hAPP_f2112551770a_bool: ( fun_fu1249172034a_bool * fun_Ho957066028l_bool ) > fun_fu1585556401a_bool ).
tff(func_def_81,type,
hAPP_f909473944a_bool: ( fun_fu1563903738a_bool * fun_Ho440810351a_bool ) > fun_Ho1877127206a_bool ).
tff(func_def_82,type,
hAPP_f1216137953a_bool: ( fun_fu893561155a_bool * fun_Ho440810351a_bool ) > fun_Ho440810351a_bool ).
tff(func_def_83,type,
hAPP_f684479953a_bool: ( fun_fu1192765369a_bool * fun_Ho525994229l_bool ) > fun_fu1585556401a_bool ).
tff(func_def_84,type,
hAPP_f1022403729a_bool: ( fun_fu1905604217a_bool * fun_Ho1630563774a_bool ) > fun_fu276214394a_bool ).
tff(func_def_85,type,
member127332739iple_a: fun_Ho525994229l_bool ).
tff(func_def_86,type,
g: fun_Ho1877127206a_bool ).
tff(func_def_87,type,
p: fun_a_fun_state_bool ).
tff(func_def_88,type,
b: fun_state_bool ).
tff(func_def_89,type,
c: com ).
tff(func_def_90,type,
sK0: ( fun_Ho1877127206a_bool * com * fun_a_fun_state_bool * fun_a_fun_state_bool ) > x_a ).
tff(func_def_91,type,
sK1: ( fun_Ho1877127206a_bool * com * fun_a_fun_state_bool * fun_a_fun_state_bool ) > state ).
tff(func_def_92,type,
sK2: ( fun_a_fun_state_bool * fun_a_fun_state_bool ) > x_a ).
tff(func_def_93,type,
sK3: ( fun_a_fun_state_bool * fun_a_fun_state_bool ) > state ).
tff(func_def_94,type,
sK4: ( fun_a_fun_state_bool * fun_a_fun_state_bool ) > x_a ).
tff(func_def_95,type,
sK5: ( fun_a_fun_state_bool * fun_a_fun_state_bool ) > state ).
tff(func_def_96,type,
sK6: ( fun_a_fun_state_bool * fun_a_fun_state_bool * fun_a_fun_state_bool * fun_a_fun_state_bool ) > x_a ).
tff(func_def_97,type,
sK7: ( fun_a_fun_state_bool * fun_a_fun_state_bool * fun_a_fun_state_bool * fun_a_fun_state_bool ) > state ).
tff(func_def_98,type,
sK8: ( fun_a_fun_state_bool * fun_a_fun_state_bool * fun_a_fun_state_bool * fun_a_fun_state_bool ) > state ).
tff(func_def_99,type,
sK9: fun_Ho1877127206a_bool > hoare_1927711152iple_a ).
tff(func_def_100,type,
sK10: fun_Ho1877127206a_bool > hoare_1927711152iple_a ).
tff(func_def_101,type,
sK11: fun_Ho1877127206a_bool > hoare_1927711152iple_a ).
tff(func_def_102,type,
sK12: fun_Ho1877127206a_bool > hoare_1927711152iple_a ).
tff(func_def_103,type,
sK13: hoare_1927711152iple_a > fun_a_fun_state_bool ).
tff(func_def_104,type,
sK14: hoare_1927711152iple_a > com ).
tff(func_def_105,type,
sK15: hoare_1927711152iple_a > fun_a_fun_state_bool ).
tff(func_def_106,type,
sK16: ( hoare_1927711152iple_a * fun_Ho1877127206a_bool ) > fun_Ho1877127206a_bool ).
tff(func_def_107,type,
sK17: ( hoare_1927711152iple_a * fun_Ho1877127206a_bool ) > fun_Ho1877127206a_bool ).
tff(func_def_108,type,
sK18: fun_Ho1877127206a_bool > hoare_1927711152iple_a ).
tff(func_def_109,type,
sK19: ( fun_Ho1877127206a_bool * hoare_1927711152iple_a ) > hoare_1927711152iple_a ).
tff(func_def_110,type,
sK20: ( fun_Ho1877127206a_bool * hoare_1927711152iple_a ) > hoare_1927711152iple_a ).
tff(func_def_111,type,
sK21: ( fun_Ho1877127206a_bool * hoare_1927711152iple_a ) > hoare_1927711152iple_a ).
tff(func_def_112,type,
sK22: ( fun_Ho1877127206a_bool * hoare_1927711152iple_a ) > hoare_1927711152iple_a ).
tff(func_def_113,type,
sK23: ( fun_a_fun_state_bool * fun_Ho1877127206a_bool * com * fun_a_fun_state_bool ) > x_a ).
tff(func_def_114,type,
sK24: ( fun_a_fun_state_bool * fun_Ho1877127206a_bool * com * fun_a_fun_state_bool ) > state ).
tff(func_def_115,type,
sK25: ( fun_a_fun_state_bool * fun_Ho1877127206a_bool * com * fun_a_fun_state_bool * fun_a_fun_state_bool * fun_a_fun_state_bool ) > state ).
tff(func_def_116,type,
sK26: fun_Ho1877127206a_bool > hoare_1927711152iple_a ).
tff(func_def_117,type,
sK27: fun_Ho1877127206a_bool > fun_Ho1877127206a_bool ).
tff(func_def_118,type,
sK28: fun_Ho333840202iple_a > hoare_1927711152iple_a ).
tff(func_def_119,type,
sK29: fun_Ho333840202iple_a > hoare_1927711152iple_a ).
tff(func_def_120,type,
sK30: ( fun_Ho333840202iple_a * hoare_1927711152iple_a * fun_Ho1877127206a_bool * hoare_1927711152iple_a ) > hoare_1927711152iple_a ).
tff(func_def_121,type,
sK31: ( fun_Ho333840202iple_a * hoare_1927711152iple_a * fun_Ho1877127206a_bool * hoare_1927711152iple_a ) > fun_Ho1877127206a_bool ).
tff(func_def_122,type,
sK32: ( fun_Ho333840202iple_a * fun_Ho1877127206a_bool ) > hoare_1927711152iple_a ).
tff(func_def_123,type,
sK33: fun_fu832487784l_bool > hoare_1927711152iple_a ).
tff(func_def_124,type,
sK34: fun_fu832487784l_bool > fun_Ho1877127206a_bool ).
tff(func_def_125,type,
sK35: fun_Ho1877127206a_bool > fun_Ho1877127206a_bool ).
tff(func_def_126,type,
sK36: fun_Ho1877127206a_bool > hoare_1927711152iple_a ).
tff(func_def_127,type,
sK37: ( fun_Ho333840202iple_a * hoare_1927711152iple_a * fun_Ho1877127206a_bool ) > hoare_1927711152iple_a ).
tff(func_def_128,type,
sK38: ( fun_Ho333840202iple_a * fun_Ho1877127206a_bool * hoare_1927711152iple_a ) > hoare_1927711152iple_a ).
tff(func_def_129,type,
sK39: ( fun_Ho333840202iple_a * fun_Ho1877127206a_bool * hoare_1927711152iple_a ) > fun_Ho1877127206a_bool ).
tff(func_def_130,type,
sK40: ( fun_Ho333840202iple_a * fun_Ho1877127206a_bool * hoare_1927711152iple_a ) > hoare_1927711152iple_a ).
tff(func_def_131,type,
sK41: ( fun_Ho333840202iple_a * hoare_1927711152iple_a * fun_Ho1877127206a_bool * hoare_1927711152iple_a ) > hoare_1927711152iple_a ).
tff(func_def_132,type,
sK42: ( fun_Ho333840202iple_a * hoare_1927711152iple_a * fun_Ho1877127206a_bool * hoare_1927711152iple_a ) > fun_Ho1877127206a_bool ).
tff(func_def_133,type,
sK43: ( fun_Ho333840202iple_a * hoare_1927711152iple_a * fun_Ho1877127206a_bool * hoare_1927711152iple_a ) > hoare_1927711152iple_a ).
tff(func_def_134,type,
sK44: fun_fu832487784l_bool > hoare_1927711152iple_a ).
tff(func_def_135,type,
sK45: fun_fu832487784l_bool > hoare_1927711152iple_a ).
tff(func_def_136,type,
sK46: fun_fu832487784l_bool > fun_Ho1877127206a_bool ).
tff(pred_def_1,type,
hBOOL: bool > $o ).
tff(f1,axiom,
! [X0: fun_Ho1877127206a_bool] : hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X0),bot_bo1208640912a_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_empty) ).
tff(f3,axiom,
! [X0: fun_Ho1877127206a_bool,X1: fun_Ho1877127206a_bool,X2: fun_Ho1877127206a_bool] :
( hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X1),X2))
=> ( hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X0),X1))
=> hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X0),X2)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_2_cut) ).
tff(f6,axiom,
! [X0: fun_Ho1877127206a_bool,X1: com,X2: fun_a_fun_state_bool,X3: fun_a_fun_state_bool] :
( ! [X4: x_a,X5: state] :
( hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(X3,X4),X5))
=> hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X0),hAPP_f16502863a_bool(hAPP_H1975128022a_bool(insert1434104874iple_a,hoare_1652181356iple_a(cOMBK_1458035955bool_a(hAPP_s1806633685e_bool(hAPP_f817621513e_bool(cOMBC_2027030106e_bool,fequal_state),X5)),X1,cOMBK_1458035955bool_a(hAPP_a2036067514e_bool(X2,X4)))),bot_bo1208640912a_bool))) )
=> hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X0),hAPP_f16502863a_bool(hAPP_H1975128022a_bool(insert1434104874iple_a,hoare_1652181356iple_a(X3,X1,X2)),bot_bo1208640912a_bool))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_5_escape) ).
tff(f13,axiom,
! [X0: hoare_1927711152iple_a] : ( collec829051333iple_a(hAPP_H1027145665a_bool(fequal1440857775iple_a,X0)) = hAPP_f16502863a_bool(hAPP_H1975128022a_bool(insert1434104874iple_a,X0),bot_bo1208640912a_bool) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_12_singleton__conv2) ).
tff(f23,axiom,
bot_bo1208640912a_bool = collec829051333iple_a(cOMBK_712844119iple_a(fFalse)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_22_empty__def) ).
tff(f42,axiom,
! [X0: hoare_1927711152iple_a] :
( hBOOL(hAPP_H1448631928a_bool(bot_bo1208640912a_bool,X0))
<=> hBOOL(bot_bot_bool) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_41_bot__apply) ).
tff(f72,axiom,
hBOOL(hAPP_f1454306822l_bool(finite68738179iple_a,bot_bo1208640912a_bool)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_71_finite_OemptyI) ).
tff(f73,axiom,
! [X0: hoare_1927711152iple_a,X1: fun_Ho1877127206a_bool] :
( hBOOL(hAPP_f1454306822l_bool(finite68738179iple_a,X1))
=> hBOOL(hAPP_f1454306822l_bool(finite68738179iple_a,hAPP_f16502863a_bool(hAPP_H1975128022a_bool(insert1434104874iple_a,X0),X1))) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_72_finite_OinsertI) ).
tff(f75,axiom,
! [X0: fun_Ho1877127206a_bool] : ( collec829051333iple_a(X0) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_74_Collect__def) ).
tff(f87,axiom,
! [X0: fun_fu832487784l_bool,X1: fun_Ho1877127206a_bool] :
( hBOOL(hAPP_f1454306822l_bool(finite68738179iple_a,X1))
=> ( hBOOL(hAPP_f1454306822l_bool(X0,bot_bo1208640912a_bool))
=> ( ! [X2: hoare_1927711152iple_a,X3: fun_Ho1877127206a_bool] :
( hBOOL(hAPP_f1454306822l_bool(finite68738179iple_a,X3))
=> ( ~ hBOOL(hAPP_f1454306822l_bool(hAPP_H694056973l_bool(member127332739iple_a,X2),X3))
=> ( hBOOL(hAPP_f1454306822l_bool(X0,X3))
=> hBOOL(hAPP_f1454306822l_bool(X0,hAPP_f16502863a_bool(hAPP_H1975128022a_bool(insert1434104874iple_a,X2),X3))) ) ) )
=> hBOOL(hAPP_f1454306822l_bool(X0,X1)) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_86_finite__induct) ).
tff(f104,axiom,
~ hBOOL(fFalse),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fFalse_1_1_U) ).
tff(f105,axiom,
! [X0: bool] :
( ( X0 = fTrue )
| ( X0 = fFalse ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_fFalse_1_1_T) ).
tff(f111,axiom,
! [X0: bool,X1: state] : ( hAPP_state_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) ).
tff(f112,axiom,
! [X0: fun_state_bool,X1: x_a] : ( hAPP_a2036067514e_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) ).
tff(f120,axiom,
! [X0: bool,X1: hoare_1927711152iple_a] : ( hAPP_H1448631928a_bool(cOMBK_712844119iple_a(X0),X1) = X0 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',help_COMBK_1_1_COMBK_000tc__HOL__Obool_000tc__Hoare____Mirabelle____yiemogtkbg__) ).
tff(f135,conjecture,
hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(g),hAPP_f16502863a_bool(hAPP_H1975128022a_bool(insert1434104874iple_a,hoare_1652181356iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b)))),bot_bo1208640912a_bool))),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_0) ).
tff(f136,negated_conjecture,
~ hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(g),hAPP_f16502863a_bool(hAPP_H1975128022a_bool(insert1434104874iple_a,hoare_1652181356iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b)))),bot_bo1208640912a_bool))),
inference(negated_conjecture,[status(cth)],[f135]) ).
tff(f138,plain,
~ hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(g),hAPP_f16502863a_bool(hAPP_H1975128022a_bool(insert1434104874iple_a,hoare_1652181356iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b)))),bot_bo1208640912a_bool))),
inference(flattening,[],[f136]) ).
tff(f139,plain,
! [X0: fun_Ho1877127206a_bool,X1: fun_Ho1877127206a_bool,X2: fun_Ho1877127206a_bool] :
( hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X0),X2))
| ~ hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X0),X1))
| ~ hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X1),X2)) ),
inference(ennf_transformation,[],[f3]) ).
tff(f140,plain,
! [X0: fun_Ho1877127206a_bool,X1: fun_Ho1877127206a_bool,X2: fun_Ho1877127206a_bool] :
( hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X0),X2))
| ~ hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X0),X1))
| ~ hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X1),X2)) ),
inference(flattening,[],[f139]) ).
tff(f144,plain,
! [X0: fun_Ho1877127206a_bool,X1: com,X2: fun_a_fun_state_bool,X3: fun_a_fun_state_bool] :
( hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X0),hAPP_f16502863a_bool(hAPP_H1975128022a_bool(insert1434104874iple_a,hoare_1652181356iple_a(X3,X1,X2)),bot_bo1208640912a_bool)))
| ? [X4: x_a,X5: state] :
( ~ hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X0),hAPP_f16502863a_bool(hAPP_H1975128022a_bool(insert1434104874iple_a,hoare_1652181356iple_a(cOMBK_1458035955bool_a(hAPP_s1806633685e_bool(hAPP_f817621513e_bool(cOMBC_2027030106e_bool,fequal_state),X5)),X1,cOMBK_1458035955bool_a(hAPP_a2036067514e_bool(X2,X4)))),bot_bo1208640912a_bool)))
& hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(X3,X4),X5)) ) ),
inference(ennf_transformation,[],[f6]) ).
tff(f185,plain,
! [X0: hoare_1927711152iple_a,X1: fun_Ho1877127206a_bool] :
( hBOOL(hAPP_f1454306822l_bool(finite68738179iple_a,hAPP_f16502863a_bool(hAPP_H1975128022a_bool(insert1434104874iple_a,X0),X1)))
| ~ hBOOL(hAPP_f1454306822l_bool(finite68738179iple_a,X1)) ),
inference(ennf_transformation,[],[f73]) ).
tff(f198,plain,
! [X0: fun_fu832487784l_bool,X1: fun_Ho1877127206a_bool] :
( hBOOL(hAPP_f1454306822l_bool(X0,X1))
| ? [X2: hoare_1927711152iple_a,X3: fun_Ho1877127206a_bool] :
( ~ hBOOL(hAPP_f1454306822l_bool(X0,hAPP_f16502863a_bool(hAPP_H1975128022a_bool(insert1434104874iple_a,X2),X3)))
& hBOOL(hAPP_f1454306822l_bool(X0,X3))
& ~ hBOOL(hAPP_f1454306822l_bool(hAPP_H694056973l_bool(member127332739iple_a,X2),X3))
& hBOOL(hAPP_f1454306822l_bool(finite68738179iple_a,X3)) )
| ~ hBOOL(hAPP_f1454306822l_bool(X0,bot_bo1208640912a_bool))
| ~ hBOOL(hAPP_f1454306822l_bool(finite68738179iple_a,X1)) ),
inference(ennf_transformation,[],[f87]) ).
tff(f199,plain,
! [X0: fun_fu832487784l_bool,X1: fun_Ho1877127206a_bool] :
( hBOOL(hAPP_f1454306822l_bool(X0,X1))
| ? [X2: hoare_1927711152iple_a,X3: fun_Ho1877127206a_bool] :
( ~ hBOOL(hAPP_f1454306822l_bool(X0,hAPP_f16502863a_bool(hAPP_H1975128022a_bool(insert1434104874iple_a,X2),X3)))
& hBOOL(hAPP_f1454306822l_bool(X0,X3))
& ~ hBOOL(hAPP_f1454306822l_bool(hAPP_H694056973l_bool(member127332739iple_a,X2),X3))
& hBOOL(hAPP_f1454306822l_bool(finite68738179iple_a,X3)) )
| ~ hBOOL(hAPP_f1454306822l_bool(X0,bot_bo1208640912a_bool))
| ~ hBOOL(hAPP_f1454306822l_bool(finite68738179iple_a,X1)) ),
inference(flattening,[],[f198]) ).
tff(f208,plain,
! [X0: fun_Ho1877127206a_bool] : hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X0),bot_bo1208640912a_bool)),
inference(cnf_transformation,[],[f1]) ).
tff(f213,plain,
! [X2: fun_Ho1877127206a_bool,X0: fun_Ho1877127206a_bool,X1: fun_Ho1877127206a_bool] :
( ~ hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X1),X2))
| ~ hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X0),X1))
| hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X0),X2)) ),
inference(cnf_transformation,[],[f140]) ).
tff(f217,plain,
! [X2: fun_a_fun_state_bool,X3: fun_a_fun_state_bool,X0: fun_Ho1877127206a_bool,X1: com] :
( hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(X3,sK0(X0,X1,X2,X3)),sK1(X0,X1,X2,X3)))
| hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X0),hAPP_f16502863a_bool(hAPP_H1975128022a_bool(insert1434104874iple_a,hoare_1652181356iple_a(X3,X1,X2)),bot_bo1208640912a_bool))) ),
inference(cnf_transformation,[],[f144]) ).
tff(f230,plain,
! [X0: hoare_1927711152iple_a] : ( collec829051333iple_a(hAPP_H1027145665a_bool(fequal1440857775iple_a,X0)) = hAPP_f16502863a_bool(hAPP_H1975128022a_bool(insert1434104874iple_a,X0),bot_bo1208640912a_bool) ),
inference(cnf_transformation,[],[f13]) ).
tff(f246,plain,
bot_bo1208640912a_bool = collec829051333iple_a(cOMBK_712844119iple_a(fFalse)),
inference(cnf_transformation,[],[f23]) ).
tff(f276,plain,
! [X0: hoare_1927711152iple_a] :
( ~ hBOOL(bot_bot_bool)
| hBOOL(hAPP_H1448631928a_bool(bot_bo1208640912a_bool,X0)) ),
inference(cnf_transformation,[],[f42]) ).
tff(f324,plain,
hBOOL(hAPP_f1454306822l_bool(finite68738179iple_a,bot_bo1208640912a_bool)),
inference(cnf_transformation,[],[f72]) ).
tff(f325,plain,
! [X0: hoare_1927711152iple_a,X1: fun_Ho1877127206a_bool] :
( ~ hBOOL(hAPP_f1454306822l_bool(finite68738179iple_a,X1))
| hBOOL(hAPP_f1454306822l_bool(finite68738179iple_a,hAPP_f16502863a_bool(hAPP_H1975128022a_bool(insert1434104874iple_a,X0),X1))) ),
inference(cnf_transformation,[],[f185]) ).
tff(f328,plain,
! [X0: fun_Ho1877127206a_bool] : ( collec829051333iple_a(X0) = X0 ),
inference(cnf_transformation,[],[f75]) ).
tff(f347,plain,
! [X0: fun_fu832487784l_bool,X1: fun_Ho1877127206a_bool] :
( ~ hBOOL(hAPP_f1454306822l_bool(finite68738179iple_a,X1))
| ~ hBOOL(hAPP_f1454306822l_bool(X0,bot_bo1208640912a_bool))
| hBOOL(hAPP_f1454306822l_bool(X0,sK34(X0)))
| hBOOL(hAPP_f1454306822l_bool(X0,X1)) ),
inference(cnf_transformation,[],[f199]) ).
tff(f385,plain,
~ hBOOL(fFalse),
inference(cnf_transformation,[],[f104]) ).
tff(f386,plain,
! [X0: bool] :
( ( fTrue = X0 )
| ( fFalse = X0 ) ),
inference(cnf_transformation,[],[f105]) ).
tff(f392,plain,
! [X0: bool,X1: state] : ( hAPP_state_bool(cOMBK_bool_state(X0),X1) = X0 ),
inference(cnf_transformation,[],[f111]) ).
tff(f393,plain,
! [X0: fun_state_bool,X1: x_a] : ( hAPP_a2036067514e_bool(cOMBK_1458035955bool_a(X0),X1) = X0 ),
inference(cnf_transformation,[],[f112]) ).
tff(f401,plain,
! [X0: bool,X1: hoare_1927711152iple_a] : ( hAPP_H1448631928a_bool(cOMBK_712844119iple_a(X0),X1) = X0 ),
inference(cnf_transformation,[],[f120]) ).
tff(f416,plain,
~ hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(g),hAPP_f16502863a_bool(hAPP_H1975128022a_bool(insert1434104874iple_a,hoare_1652181356iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b)))),bot_bo1208640912a_bool))),
inference(cnf_transformation,[],[f138]) ).
tff(f449,plain,
! [X0: fun_Ho1877127206a_bool] : ~ hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X0),bot_bo1208640912a_bool)),
inference(consistent_polarity_flipping,[],[f208]) ).
tff(f450,plain,
! [X2: fun_Ho1877127206a_bool,X0: fun_Ho1877127206a_bool,X1: fun_Ho1877127206a_bool] :
( ~ hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X0),X2))
| hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X0),X1))
| hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X1),X2)) ),
inference(consistent_polarity_flipping,[],[f213]) ).
tff(f455,plain,
! [X2: fun_a_fun_state_bool,X3: fun_a_fun_state_bool,X0: fun_Ho1877127206a_bool,X1: com] :
( ~ hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(X3,sK0(X0,X1,X2,X3)),sK1(X0,X1,X2,X3)))
| ~ hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X0),hAPP_f16502863a_bool(hAPP_H1975128022a_bool(insert1434104874iple_a,hoare_1652181356iple_a(X3,X1,X2)),bot_bo1208640912a_bool))) ),
inference(consistent_polarity_flipping,[],[f217]) ).
tff(f496,plain,
! [X0: hoare_1927711152iple_a] :
( hBOOL(bot_bot_bool)
| ~ hBOOL(hAPP_H1448631928a_bool(bot_bo1208640912a_bool,X0)) ),
inference(consistent_polarity_flipping,[],[f276]) ).
tff(f532,plain,
~ hBOOL(hAPP_f1454306822l_bool(finite68738179iple_a,bot_bo1208640912a_bool)),
inference(consistent_polarity_flipping,[],[f324]) ).
tff(f533,plain,
! [X0: hoare_1927711152iple_a,X1: fun_Ho1877127206a_bool] :
( ~ hBOOL(hAPP_f1454306822l_bool(finite68738179iple_a,hAPP_f16502863a_bool(hAPP_H1975128022a_bool(insert1434104874iple_a,X0),X1)))
| hBOOL(hAPP_f1454306822l_bool(finite68738179iple_a,X1)) ),
inference(consistent_polarity_flipping,[],[f325]) ).
tff(f551,plain,
! [X0: fun_fu832487784l_bool,X1: fun_Ho1877127206a_bool] :
( ~ hBOOL(hAPP_f1454306822l_bool(X0,sK34(X0)))
| hBOOL(hAPP_f1454306822l_bool(X0,bot_bo1208640912a_bool))
| hBOOL(hAPP_f1454306822l_bool(finite68738179iple_a,X1))
| ~ hBOOL(hAPP_f1454306822l_bool(X0,X1)) ),
inference(consistent_polarity_flipping,[],[f347]) ).
tff(f590,plain,
hBOOL(fFalse),
inference(consistent_polarity_flipping,[],[f385]) ).
tff(f600,plain,
hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(g),hAPP_f16502863a_bool(hAPP_H1975128022a_bool(insert1434104874iple_a,hoare_1652181356iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b)))),bot_bo1208640912a_bool))),
inference(consistent_polarity_flipping,[],[f416]) ).
tff(f603,definition,
( spl47_1
<=> ! [X0: hoare_1927711152iple_a] : ~ hBOOL(hAPP_H1448631928a_bool(bot_bo1208640912a_bool,X0)) ),
introduced(definition,[new_symbols(definition,[spl47_1])],[avatar_definition]) ).
tff(f604,plain,
( ! [X0: hoare_1927711152iple_a] : ~ hBOOL(hAPP_H1448631928a_bool(bot_bo1208640912a_bool,X0))
| ~ spl47_1 ),
inference(avatar_component_clause,[],[f603]) ).
tff(f606,definition,
( spl47_2
<=> hBOOL(bot_bot_bool) ),
introduced(definition,[new_symbols(definition,[spl47_2])],[avatar_definition]) ).
tff(f608,plain,
( hBOOL(bot_bot_bool)
| ~ spl47_2 ),
inference(avatar_component_clause,[],[f606]) ).
tff(f614,plain,
( spl47_1
| spl47_2 ),
inference(avatar_split_clause,[],[f496,f606,f603]) ).
tff(f616,plain,
bot_bo1208640912a_bool = cOMBK_712844119iple_a(fFalse),
inference(superposition,[],[f246,f328]) ).
tff(f622,plain,
( ~ hBOOL(fTrue)
| ( fFalse = hAPP_f1454306822l_bool(finite68738179iple_a,bot_bo1208640912a_bool) ) ),
inference(superposition,[],[f532,f386]) ).
tff(f633,definition,
( spl47_6
<=> ( fFalse = hAPP_f1454306822l_bool(finite68738179iple_a,bot_bo1208640912a_bool) ) ),
introduced(definition,[new_symbols(definition,[spl47_6])],[avatar_definition]) ).
tff(f635,plain,
( ( fFalse = hAPP_f1454306822l_bool(finite68738179iple_a,bot_bo1208640912a_bool) )
| ~ spl47_6 ),
inference(avatar_component_clause,[],[f633]) ).
tff(f637,definition,
( spl47_7
<=> hBOOL(fTrue) ),
introduced(definition,[new_symbols(definition,[spl47_7])],[avatar_definition]) ).
tff(f639,plain,
( ~ hBOOL(fTrue)
| spl47_7 ),
inference(avatar_component_clause,[],[f637]) ).
tff(f640,plain,
( spl47_6
| ~ spl47_7 ),
inference(avatar_split_clause,[],[f622,f637,f633]) ).
tff(f651,definition,
( spl47_10
<=> ! [X0: hoare_1927711152iple_a] : ( fFalse = hAPP_H1448631928a_bool(bot_bo1208640912a_bool,X0) ) ),
introduced(definition,[new_symbols(definition,[spl47_10])],[avatar_definition]) ).
tff(f652,plain,
( ! [X0: hoare_1927711152iple_a] : ( fFalse = hAPP_H1448631928a_bool(bot_bo1208640912a_bool,X0) )
| ~ spl47_10 ),
inference(avatar_component_clause,[],[f651]) ).
tff(f660,plain,
! [X0: hoare_1927711152iple_a] : ( fFalse = hAPP_H1448631928a_bool(bot_bo1208640912a_bool,X0) ),
inference(superposition,[],[f401,f616]) ).
tff(f661,plain,
spl47_10,
inference(avatar_split_clause,[],[f660,f651]) ).
tff(f665,plain,
( ~ hBOOL(fFalse)
| ~ spl47_6 ),
inference(superposition,[],[f532,f635]) ).
tff(f666,plain,
( $false
| ~ spl47_6 ),
inference(forward_subsumption_resolution,[],[f665,f590]) ).
tff(f667,plain,
~ spl47_6,
inference(avatar_contradiction_clause,[],[f666]) ).
tff(f691,plain,
( ! [X0: bool] :
( ~ hBOOL(X0)
| ( fFalse = X0 ) )
| spl47_7 ),
inference(superposition,[],[f639,f386]) ).
tff(f699,plain,
( ( fFalse = bot_bot_bool )
| ~ spl47_2
| spl47_7 ),
inference(resolution,[],[f691,f608]) ).
tff(f767,plain,
! [X0: hoare_1927711152iple_a] : ( hAPP_H1027145665a_bool(fequal1440857775iple_a,X0) = hAPP_f16502863a_bool(hAPP_H1975128022a_bool(insert1434104874iple_a,X0),bot_bo1208640912a_bool) ),
inference(forward_demodulation,[],[f230,f328]) ).
tff(f912,plain,
! [X0: hoare_1927711152iple_a] :
( ~ hBOOL(hAPP_f1454306822l_bool(finite68738179iple_a,hAPP_H1027145665a_bool(fequal1440857775iple_a,X0)))
| hBOOL(hAPP_f1454306822l_bool(finite68738179iple_a,bot_bo1208640912a_bool)) ),
inference(superposition,[],[f533,f767]) ).
tff(f915,plain,
! [X0: hoare_1927711152iple_a] : ~ hBOOL(hAPP_f1454306822l_bool(finite68738179iple_a,hAPP_H1027145665a_bool(fequal1440857775iple_a,X0))),
inference(forward_subsumption_resolution,[],[f912,f532]) ).
tff(f1117,plain,
! [X0: fun_Ho1877127206a_bool] :
( hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(g),X0))
| hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X0),hAPP_f16502863a_bool(hAPP_H1975128022a_bool(insert1434104874iple_a,hoare_1652181356iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b)))),bot_bo1208640912a_bool))) ),
inference(resolution,[],[f450,f600]) ).
tff(f1129,plain,
! [X0: fun_Ho1877127206a_bool] :
( hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X0),hAPP_H1027145665a_bool(fequal1440857775iple_a,hoare_1652181356iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b))))))
| hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(g),X0)) ),
inference(forward_demodulation,[],[f1117,f767]) ).
tff(f1132,plain,
( ! [X0: fun_Ho1877127206a_bool] :
( hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X0),hAPP_H1027145665a_bool(fequal1440857775iple_a,hoare_1652181356iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(bot_bot_bool)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b))))))
| hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(g),X0)) )
| ~ spl47_2
| spl47_7 ),
inference(forward_demodulation,[],[f1129,f699]) ).
tff(f1156,plain,
( ! [X0: fun_Ho1877127206a_bool] :
( hBOOL(fTrue)
| hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(g),X0))
| ( fFalse = hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X0),hAPP_H1027145665a_bool(fequal1440857775iple_a,hoare_1652181356iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(bot_bot_bool)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b))))) ) )
| ~ spl47_2
| spl47_7 ),
inference(superposition,[],[f1132,f386]) ).
tff(f1157,plain,
( ! [X0: fun_Ho1877127206a_bool] :
( hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(g),X0))
| ( fFalse = hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X0),hAPP_H1027145665a_bool(fequal1440857775iple_a,hoare_1652181356iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(bot_bot_bool)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b))))) ) )
| ~ spl47_2
| spl47_7 ),
inference(forward_subsumption_resolution,[],[f1156,f639]) ).
tff(f1159,plain,
( ! [X0: fun_Ho1877127206a_bool] :
( hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(g),X0))
| ( bot_bot_bool = hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X0),hAPP_H1027145665a_bool(fequal1440857775iple_a,hoare_1652181356iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(bot_bot_bool)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b))))) ) )
| ~ spl47_2
| spl47_7 ),
inference(forward_demodulation,[],[f1157,f699]) ).
tff(f1428,plain,
( ! [X0: fun_Ho1877127206a_bool] :
( hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(g),bot_bo1208640912a_bool))
| hBOOL(hAPP_f1454306822l_bool(finite68738179iple_a,X0))
| ~ hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(g),X0))
| ( bot_bot_bool = hAPP_f1454306822l_bool(hoare_1617968510rivs_a(sK34(hoare_1617968510rivs_a(g))),hAPP_H1027145665a_bool(fequal1440857775iple_a,hoare_1652181356iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(bot_bot_bool)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b))))) ) )
| ~ spl47_2
| spl47_7 ),
inference(resolution,[],[f551,f1159]) ).
tff(f1438,plain,
( ! [X0: fun_Ho1877127206a_bool] :
( hBOOL(hAPP_f1454306822l_bool(finite68738179iple_a,X0))
| ~ hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(g),X0))
| ( bot_bot_bool = hAPP_f1454306822l_bool(hoare_1617968510rivs_a(sK34(hoare_1617968510rivs_a(g))),hAPP_H1027145665a_bool(fequal1440857775iple_a,hoare_1652181356iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(bot_bot_bool)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b))))) ) )
| ~ spl47_2
| spl47_7 ),
inference(forward_subsumption_resolution,[],[f1428,f449]) ).
tff(f1449,definition,
( spl47_18
<=> ( bot_bot_bool = hAPP_f1454306822l_bool(hoare_1617968510rivs_a(sK34(hoare_1617968510rivs_a(g))),hAPP_H1027145665a_bool(fequal1440857775iple_a,hoare_1652181356iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(bot_bot_bool)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b))))) ) ),
introduced(definition,[new_symbols(definition,[spl47_18])],[avatar_definition]) ).
tff(f1451,plain,
( ( bot_bot_bool = hAPP_f1454306822l_bool(hoare_1617968510rivs_a(sK34(hoare_1617968510rivs_a(g))),hAPP_H1027145665a_bool(fequal1440857775iple_a,hoare_1652181356iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(bot_bot_bool)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b))))) )
| ~ spl47_18 ),
inference(avatar_component_clause,[],[f1449]) ).
tff(f1453,definition,
( spl47_19
<=> ! [X0: fun_Ho1877127206a_bool] :
( hBOOL(hAPP_f1454306822l_bool(finite68738179iple_a,X0))
| ~ hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(g),X0)) ) ),
introduced(definition,[new_symbols(definition,[spl47_19])],[avatar_definition]) ).
tff(f1454,plain,
( ! [X0: fun_Ho1877127206a_bool] :
( ~ hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(g),X0))
| hBOOL(hAPP_f1454306822l_bool(finite68738179iple_a,X0)) )
| ~ spl47_19 ),
inference(avatar_component_clause,[],[f1453]) ).
tff(f1455,plain,
( spl47_18
| spl47_19
| ~ spl47_2
| spl47_7 ),
inference(avatar_split_clause,[],[f1438,f637,f606,f1453,f1449]) ).
tff(f1465,plain,
( hBOOL(hAPP_f1454306822l_bool(finite68738179iple_a,hAPP_f16502863a_bool(hAPP_H1975128022a_bool(insert1434104874iple_a,hoare_1652181356iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b)))),bot_bo1208640912a_bool)))
| ~ spl47_19 ),
inference(resolution,[],[f1454,f600]) ).
tff(f1487,plain,
( hBOOL(hAPP_f1454306822l_bool(finite68738179iple_a,hAPP_H1027145665a_bool(fequal1440857775iple_a,hoare_1652181356iple_a(cOMBK_1458035955bool_a(cOMBK_bool_state(fFalse)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b))))))
| ~ spl47_19 ),
inference(forward_demodulation,[],[f1465,f767]) ).
tff(f1495,plain,
( $false
| ~ spl47_19 ),
inference(forward_subsumption_resolution,[],[f1487,f915]) ).
tff(f1496,plain,
~ spl47_19,
inference(avatar_contradiction_clause,[],[f1495]) ).
tff(f1833,plain,
( ~ hBOOL(fFalse)
| ~ spl47_1
| ~ spl47_10 ),
inference(forward_demodulation,[],[f604,f652]) ).
tff(f1839,plain,
( $false
| ~ spl47_1
| ~ spl47_10 ),
inference(forward_subsumption_resolution,[],[f1833,f590]) ).
tff(f1840,plain,
( ~ spl47_1
| ~ spl47_10 ),
inference(avatar_contradiction_clause,[],[f1839]) ).
tff(f2333,plain,
! [X2: fun_a_fun_state_bool,X3: fun_a_fun_state_bool,X0: fun_Ho1877127206a_bool,X1: com] :
( ~ hBOOL(hAPP_f1454306822l_bool(hoare_1617968510rivs_a(X0),hAPP_H1027145665a_bool(fequal1440857775iple_a,hoare_1652181356iple_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,[],[f455,f767]) ).
tff(f2335,plain,
( ~ hBOOL(bot_bot_bool)
| ~ hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(cOMBK_1458035955bool_a(cOMBK_bool_state(bot_bot_bool)),sK0(sK34(hoare_1617968510rivs_a(g)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b)),cOMBK_1458035955bool_a(cOMBK_bool_state(bot_bot_bool)))),sK1(sK34(hoare_1617968510rivs_a(g)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b)),cOMBK_1458035955bool_a(cOMBK_bool_state(bot_bot_bool)))))
| ~ spl47_18 ),
inference(superposition,[],[f2333,f1451]) ).
tff(f2337,plain,
( ~ hBOOL(hAPP_state_bool(hAPP_a2036067514e_bool(cOMBK_1458035955bool_a(cOMBK_bool_state(bot_bot_bool)),sK0(sK34(hoare_1617968510rivs_a(g)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b)),cOMBK_1458035955bool_a(cOMBK_bool_state(bot_bot_bool)))),sK1(sK34(hoare_1617968510rivs_a(g)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b)),cOMBK_1458035955bool_a(cOMBK_bool_state(bot_bot_bool)))))
| ~ spl47_2
| ~ spl47_18 ),
inference(forward_subsumption_resolution,[],[f2335,f608]) ).
tff(f2338,plain,
( ~ hBOOL(hAPP_state_bool(cOMBK_bool_state(bot_bot_bool),sK1(sK34(hoare_1617968510rivs_a(g)),c,hAPP_f762886889e_bool(hAPP_f1261923407e_bool(cOMBC_892787026e_bool,hAPP_f963367678e_bool(cOMBB_145932198bool_a(cOMBS_1378840469l_bool),hAPP_f1509969235l_bool(cOMBB_1355796797bool_a(cOMBB_188601460_state(fconj)),p))),hAPP_f1759915619e_bool(cOMBB_160679318_state(fNot),b)),cOMBK_1458035955bool_a(cOMBK_bool_state(bot_bot_bool)))))
| ~ spl47_2
| ~ spl47_18 ),
inference(forward_demodulation,[],[f2337,f393]) ).
tff(f2339,plain,
( ~ hBOOL(bot_bot_bool)
| ~ spl47_2
| ~ spl47_18 ),
inference(forward_demodulation,[],[f2338,f392]) ).
tff(f2340,plain,
( $false
| ~ spl47_2
| ~ spl47_18 ),
inference(forward_subsumption_resolution,[],[f2339,f608]) ).
tff(f2341,plain,
( ~ spl47_2
| ~ spl47_18 ),
inference(avatar_contradiction_clause,[],[f2340]) ).
cnf(s3,plain,
( spl47_1
| spl47_2 ),
inference(sat_conversion,[],[f614]) ).
cnf(s6,plain,
( spl47_6
| ~ spl47_7 ),
inference(sat_conversion,[],[f640]) ).
cnf(s10,plain,
spl47_10,
inference(sat_conversion,[],[f661]) ).
cnf(s11,plain,
~ spl47_6,
inference(sat_conversion,[],[f667]) ).
cnf(s22,plain,
( ~ spl47_2
| spl47_7
| spl47_18
| spl47_19 ),
inference(sat_conversion,[],[f1455]) ).
cnf(s27,plain,
~ spl47_19,
inference(sat_conversion,[],[f1496]) ).
cnf(s46,plain,
( ~ spl47_1
| ~ spl47_10 ),
inference(sat_conversion,[],[f1840]) ).
cnf(s64,plain,
( ~ spl47_2
| ~ spl47_18 ),
inference(sat_conversion,[],[f2341]) ).
cnf(s66,plain,
( ~ spl47_2
| spl47_7
| spl47_18 ),
inference(rat,[],[s22,s27]) ).
cnf(s67,plain,
~ spl47_1,
inference(rat,[],[s46,s10]) ).
cnf(s68,plain,
~ spl47_7,
inference(rat,[],[s6,s11]) ).
cnf(s73,plain,
spl47_2,
inference(rat,[],[s3,s67]) ).
cnf(s74,plain,
~ spl47_18,
inference(rat,[],[s64,s73]) ).
cnf(s78,plain,
$false,
inference(rat,[],[s66,s68,s74,s73]) ).
tff(f2342,plain,
$false,
inference(avatar_sat_refutation,[],[s78]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SWW470_1 : TPTP v9.3.1. Released v5.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.18 % Computer : n002.cluster.edu
% 0.07/0.18 % Model : x86_64 x86_64
% 0.07/0.18 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.07/0.18 % Memory : 8046.5625MB
% 0.07/0.18 % OS : Linux 6.8.0-71-generic
% 0.07/0.18 % CPULimit : 300
% 0.07/0.18 % WCLimit : 300
% 0.07/0.18 % DateTime : Mon Sep 28 14:05:10 UTC 2026
% 0.07/0.18 % CPUTime :
% 0.07/0.18 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.07/0.21 Running first-order model finding
% 0.07/0.21 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
% 0.17/0.34 % (362972)Will run a generic schedule for satisfiability detection.
% 0.17/0.34 % (362983)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2659820081:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.17/0.34 % (362978)% WARNING: option uhcvi not known.
% 0.17/0.34 % (362977)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=815579861_2999 on theBenchmark for (2999ds/0Mi)
% 0.17/0.34 % (362978)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2514551892:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.17/0.34 % (362980)dis+10_1_sil=32000:sp=arity:random_seed=3595772322:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.17/0.34 % (362981)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1117265683:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.17/0.34 % (362979)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1156571221:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.17/0.34 % (362982)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=115661342:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.17/0.34 % (362983)Instruction limit reached!
% 0.17/0.34 % (362983)------------------------------
% 0.17/0.34 % (362983)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.17/0.34 % (362983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/0.34 % (362983)CaDiCaL version: 2.1.3
% 0.17/0.34 % (362983)Termination reason: Instruction limit
% 0.17/0.34 % (362983)Termination phase: Saturation
% 0.17/0.34 % (362983)Time elapsed: 0.049 s
% 0.17/0.34 % (362983)Peak memory usage: 13 MB
% 0.17/0.34 % (362983)Instructions burned: 160 (million)
% 0.17/0.34 % (362991)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=4055352564:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 0.17/0.34 % (362980)Instruction limit reached!
% 0.17/0.34 % (362980)------------------------------
% 0.17/0.34 % (362980)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.17/0.34 % (362980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/0.34 % (362980)CaDiCaL version: 2.1.3
% 0.17/0.34 % (362980)Termination reason: Instruction limit
% 0.17/0.34 % (362980)Termination phase: Saturation
% 0.17/0.34 % (362980)Time elapsed: 0.060 s
% 0.17/0.34 % (362980)Peak memory usage: 13 MB
% 0.17/0.34 % (362980)Instructions burned: 103 (million)
% 0.17/0.34 % (362981)Instruction limit reached!
% 0.17/0.34 % (362981)------------------------------
% 0.17/0.34 % (362981)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.17/0.34 % (362981)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/0.34 % (362981)CaDiCaL version: 2.1.3
% 0.17/0.34 % (362981)Termination reason: Instruction limit
% 0.17/0.34 % (362981)Termination phase: Saturation
% 0.17/0.34 % (362981)Time elapsed: 0.063 s
% 0.17/0.34 % (362981)Peak memory usage: 13 MB
% 0.17/0.34 % (362981)Instructions burned: 117 (million)
% 0.17/0.34 % (362978) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-362972-362978"...
% 0.17/0.34 % (362982)Instruction limit reached!
% 0.17/0.34 % (362982)------------------------------
% 0.17/0.34 % (362982)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.17/0.34 % (362982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/0.34 % (362982)CaDiCaL version: 2.1.3
% 0.17/0.34 % (362982)Termination reason: Instruction limit
% 0.17/0.34 % (362982)Termination phase: Saturation
% 0.17/0.34 % (362982)Time elapsed: 0.076 s
% 0.17/0.34 % (362982)Peak memory usage: 13 MB
% 0.17/0.34 % (362982)Instructions burned: 138 (million)
% 0.17/0.34 % (362978)...printing done.
% 0.17/0.34 % (362978)Refutation found. Thanks to Tanya!
% 0.17/0.34 % SZS status Theorem for theBenchmark
% 0.17/0.34 % SZS output start Proof for theBenchmark
% See solution above
% 0.17/0.34 % (362978)------------------------------
% 0.17/0.34 % (362978)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.17/0.34 % (362978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.17/0.34 % (362978)CaDiCaL version: 2.1.3
% 0.17/0.34 % (362978)Termination reason: Refutation
% 0.17/0.34 % (362978)Time elapsed: 0.077 s
% 0.17/0.34 % (362978)Peak memory usage: 14 MB
% 0.17/0.34 % (362978)Instructions burned: 124 (million)
% 0.17/0.34 % (362972)Success in time 0.121 s
% 0.17/0.34 % Vampire exiting
%------------------------------------------------------------------------------