%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : ITP214^1 : TPTP v9.3.1. Bugfixed v9.2.1.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% Computer : n011.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 : Wed Sep 30 08:07:13 AM UTC 2026
% Result : Theorem 15.76s 5.29s
% Output : Refutation 16.65s
% Verified :
% SZS Type : Refutation
% Derivation depth : 3
% Number of leaves : 70
% Syntax : Number of formulae : 142 ( 68 unt; 0 typ; 0 def)
% Number of atoms : 342 ( 48 equ; 0 cnn)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 1096 ( 16 ~; 6 |; 10 &; 932 @)
% ( 0 <=>; 132 =>; 0 <=; 0 <~>)
% Maximal formula depth : 17 ( 7 avg)
% Number of types : 192 ( 191 usr)
% Number of type conns : 58 ( 58 >; 0 *; 0 +; 0 <<)
% Number of symbols : 34 ( 32 usr; 12 con; 0-5 aty)
% Number of variables : 398 ( 14 ^; 366 !; 18 ?; 398 :)
% Comments :
%------------------------------------------------------------------------------
thf(produc7766336532480398636_nat_o_type,type,
produc7766336532480398636_nat_o: $tType ).
thf(produc6999243976208994655_nat_o_type,type,
produc6999243976208994655_nat_o: $tType ).
thf(set_Pr3444600963470892981et_nat_type,type,
set_Pr3444600963470892981et_nat: $tType ).
thf(produc5657529347773406293et_nat_type,type,
produc5657529347773406293et_nat: $tType ).
thf(produc50402934264563236_nat_o_type,type,
produc50402934264563236_nat_o: $tType ).
thf(produc8628075524815789655_nat_o_type,type,
produc8628075524815789655_nat_o: $tType ).
thf(set_Pr7928877670098842301et_nat_type,type,
set_Pr7928877670098842301et_nat: $tType ).
thf(produc6830853553727218525et_nat_type,type,
produc6830853553727218525et_nat: $tType ).
thf(option2860828798490689354et_nat_type,type,
option2860828798490689354et_nat: $tType ).
thf(list_P362550909693114634et_nat_type,type,
list_P362550909693114634et_nat: $tType ).
thf(set_Pr8536935166611901872et_nat_type,type,
set_Pr8536935166611901872et_nat: $tType ).
thf(produc2732055786443039994et_nat_type,type,
produc2732055786443039994et_nat: $tType ).
thf(produc1319942482725812455at_nat_type,type,
produc1319942482725812455at_nat: $tType ).
thf(produc1399344845416535567atural_type,type,
produc1399344845416535567atural: $tType ).
thf(produc7538756082594784606_nat_b_type,type,
produc7538756082594784606_nat_b: $tType ).
thf(produc7140141985219958623_nat_a_type,type,
produc7140141985219958623_nat_a: $tType ).
thf(produc7250841696378415494atural_type,type,
produc7250841696378415494atural: $tType ).
thf(set_Pr5508209795250834101it_nat_type,type,
set_Pr5508209795250834101it_nat: $tType ).
thf(set_Pr2819221443900773171it_nat_type,type,
set_Pr2819221443900773171it_nat: $tType ).
thf(set_Pr2161125870931222855_nat_o_type,type,
set_Pr2161125870931222855_nat_o: $tType ).
thf(produc1273031398460193109it_nat_type,type,
produc1273031398460193109it_nat: $tType ).
thf(produc9011797661310329043it_nat_type,type,
produc9011797661310329043it_nat: $tType ).
thf(option5190343406534369742et_nat_type,type,
option5190343406534369742et_nat: $tType ).
thf(produc8449588929630179473_nat_b_type,type,
produc8449588929630179473_nat_b: $tType ).
thf(produc2763251018811306770_nat_a_type,type,
produc2763251018811306770_nat_a: $tType ).
thf(list_P2321686559999237006et_nat_type,type,
list_P2321686559999237006et_nat: $tType ).
thf(set_Pr3286484037609594932et_nat_type,type,
set_Pr3286484037609594932et_nat: $tType ).
thf(produc4928098042776334183_nat_o_type,type,
produc4928098042776334183_nat_o: $tType ).
thf(set_Pr719794911490849221et_nat_type,type,
set_Pr719794911490849221et_nat: $tType ).
thf(produc3925858234332021118et_nat_type,type,
produc3925858234332021118et_nat: $tType ).
thf(produc8111630337999740517et_nat_type,type,
produc8111630337999740517et_nat: $tType ).
thf(set_Pr4389693562480114009it_nat_type,type,
set_Pr4389693562480114009it_nat: $tType ).
thf(produc5966032636589952099nteger_type,type,
produc5966032636589952099nteger: $tType ).
thf(produc8961450480463052793it_nat_type,type,
produc8961450480463052793it_nat: $tType ).
thf(option2498585697089621389at_nat_type,type,
option2498585697089621389at_nat: $tType ).
thf(produc3911288613690379145it_nat_type,type,
produc3911288613690379145it_nat: $tType ).
thf(option1583680563626158861at_nat_type,type,
option1583680563626158861at_nat: $tType ).
thf(set_Pr8551490117392284871at_nat_type,type,
set_Pr8551490117392284871at_nat: $tType ).
thf(option7428179582072448501nteger_type,type,
option7428179582072448501nteger: $tType ).
thf(produc6756470014200349799atural_type,type,
produc6756470014200349799atural: $tType ).
thf(produc2207270350733924475it_nat_type,type,
produc2207270350733924475it_nat: $tType ).
thf(produc4453839368661128058it_nat_type,type,
produc4453839368661128058it_nat: $tType ).
thf(produc3500511559948749619nt_int_type,type,
produc3500511559948749619nt_int: $tType ).
thf(produc4166570645942440679at_nat_type,type,
produc4166570645942440679at_nat: $tType ).
thf(set_Pr4329608150637261639at_nat_type,type,
set_Pr4329608150637261639at_nat: $tType ).
thf(produc4471711990508489141at_nat_type,type,
produc4471711990508489141at_nat: $tType ).
thf(option4277301481530639448it_nat_type,type,
option4277301481530639448it_nat: $tType ).
thf(option2555668343544256180it_nat_type,type,
option2555668343544256180it_nat: $tType ).
thf(option8956607266484857688it_nat_type,type,
option8956607266484857688it_nat: $tType ).
thf(option1013472963438093988it_nat_type,type,
option1013472963438093988it_nat: $tType ).
thf(list_P626663023886443800it_nat_type,type,
list_P626663023886443800it_nat: $tType ).
thf(produc3843707927480180839at_nat_type,type,
produc3843707927480180839at_nat: $tType ).
thf(produc6751673265320737416it_nat_type,type,
produc6751673265320737416it_nat: $tType ).
thf(produc7196121022310644452it_nat_type,type,
produc7196121022310644452it_nat: $tType ).
thf(option4065278094766928714it_nat_type,type,
option4065278094766928714it_nat: $tType ).
thf(option3562590408128118217it_nat_type,type,
option3562590408128118217it_nat: $tType ).
thf(set_Pr8693737435421807431at_nat_type,type,
set_Pr8693737435421807431at_nat: $tType ).
thf(set_Pr2560585780119916871nt_int_type,type,
set_Pr2560585780119916871nt_int: $tType ).
thf(produc8664842809031399944it_nat_type,type,
produc8664842809031399944it_nat: $tType ).
thf(list_P7438302566501821706it_nat_type,type,
list_P7438302566501821706it_nat: $tType ).
thf(list_P6935614879863011209it_nat_type,type,
list_P6935614879863011209it_nat: $tType ).
thf(produc8032495849646651230it_nat_type,type,
produc8032495849646651230it_nat: $tType ).
thf(set_Pr7600907837789447088it_nat_type,type,
set_Pr7600907837789447088it_nat: $tType ).
thf(set_Pr7098220151150636591it_nat_type,type,
set_Pr7098220151150636591it_nat: $tType ).
thf(produc6197004810343482825et_nat_type,type,
produc6197004810343482825et_nat: $tType ).
thf(list_P7985473006766602707_nat_o_type,type,
list_P7985473006766602707_nat_o: $tType ).
thf(produc5835291356934675326atural_type,type,
produc5835291356934675326atural: $tType ).
thf(produc5728234346263159722nt_int_type,type,
produc5728234346263159722nt_int: $tType ).
thf(produc859450856879609959at_nat_type,type,
produc859450856879609959at_nat: $tType ).
thf(produc1219242969750017639nt_int_type,type,
produc1219242969750017639nt_int: $tType ).
thf(option936205604648967762et_nat_type,type,
option936205604648967762et_nat: $tType ).
thf(produc7388388658123137530it_nat_type,type,
produc7388388658123137530it_nat: $tType ).
thf(produc3260487557148687353it_nat_type,type,
produc3260487557148687353it_nat: $tType ).
thf(set_Pr7577011563204128103nteger_type,type,
set_Pr7577011563204128103nteger: $tType ).
thf(list_P9062070895058802706et_nat_type,type,
list_P9062070895058802706et_nat: $tType ).
thf(option233860712434008220it_nat_type,type,
option233860712434008220it_nat: $tType ).
thf(produc6491284506569428743nteger_type,type,
produc6491284506569428743nteger: $tType ).
thf(produc1730305018825802663t_unit_type,type,
produc1730305018825802663t_unit: $tType ).
thf(produc3407818250607552075t_unit_type,type,
produc3407818250607552075t_unit: $tType ).
thf(list_P131111800688179804it_nat_type,type,
list_P131111800688179804it_nat: $tType ).
thf(produc3658429121746597890et_nat_type,type,
produc3658429121746597890et_nat: $tType ).
thf(produc5011041761010125393t_unit_type,type,
produc5011041761010125393t_unit: $tType ).
thf(set_Pr5488025237498180813et_nat_type,type,
set_Pr5488025237498180813et_nat: $tType ).
thf(set_Pr2522554150109002629et_int_type,type,
set_Pr2522554150109002629et_int: $tType ).
thf(produc6653097349344004940it_nat_type,type,
produc6653097349344004940it_nat: $tType ).
thf(produc7248412053542808358at_nat_type,type,
produc7248412053542808358at_nat: $tType ).
thf(option8963830502488799655at_nat_type,type,
option8963830502488799655at_nat: $tType ).
thf(option1893999432384633940_int_o_type,type,
option1893999432384633940_int_o: $tType ).
thf(option8057788054806935849nteger_type,type,
option8057788054806935849nteger: $tType ).
thf(set_se7855581050983116737at_nat_type,type,
set_se7855581050983116737at_nat: $tType ).
thf(set_se6260736226359567993nt_int_type,type,
set_se6260736226359567993nt_int: $tType ).
thf(produc7819656566062154093et_nat_type,type,
produc7819656566062154093et_nat: $tType ).
thf(produc2115011035271226405et_int_type,type,
produc2115011035271226405et_int: $tType ).
thf(produc7822875418678951345atural_type,type,
produc7822875418678951345atural: $tType ).
thf(produc8923325533196201883nteger_type,type,
produc8923325533196201883nteger: $tType ).
thf(multis2468970476368604999at_nat_type,type,
multis2468970476368604999at_nat: $tType ).
thf(option4624381673175914239nt_int_type,type,
option4624381673175914239nt_int: $tType ).
thf(filter1242075044329608583at_nat_type,type,
filter1242075044329608583at_nat: $tType ).
thf(set_He475150555083384525t_unit_type,type,
set_He475150555083384525t_unit: $tType ).
thf(list_P6011104703257516679at_nat_type,type,
list_P6011104703257516679at_nat: $tType ).
thf(list_P3521021558325789923at_int_type,type,
list_P3521021558325789923at_int: $tType ).
thf(list_P8198026277950538467nt_nat_type,type,
list_P8198026277950538467nt_nat: $tType ).
thf(list_P5707943133018811711nt_int_type,type,
list_P5707943133018811711nt_int: $tType ).
thf(set_Pr1261947904930325089at_nat_type,type,
set_Pr1261947904930325089at_nat: $tType ).
thf(set_Pr958786334691620121nt_int_type,type,
set_Pr958786334691620121nt_int: $tType ).
thf(heap_T3836121109492952855ay_nat_type,type,
heap_T3836121109492952855ay_nat: $tType ).
thf(heap_T1346037964561226099ay_int_type,type,
heap_T1346037964561226099ay_int: $tType ).
thf(list_P7333126701944960589_nat_o_type,type,
list_P7333126701944960589_nat_o: $tType ).
thf(list_P5087981734274514673_int_o_type,type,
list_P5087981734274514673_int_o: $tType ).
thf(list_P6285523579766656935_o_nat_type,type,
list_P6285523579766656935_o_nat: $tType ).
thf(list_P3795440434834930179_o_int_type,type,
list_P3795440434834930179_o_int: $tType ).
thf(set_set_list_nat_type,type,
set_set_list_nat: $tType ).
thf(produc6271795597528267376eger_o_type,type,
produc6271795597528267376eger_o: $tType ).
thf(set_set_set_nat_type,type,
set_set_set_nat: $tType ).
thf(set_set_Code_integer_type,type,
set_set_Code_integer: $tType ).
thf(heap_T5738788834812785303t_unit_type,type,
heap_T5738788834812785303t_unit: $tType ).
thf(set_Product_prod_b_b_type,type,
set_Product_prod_b_b: $tType ).
thf(set_Product_prod_a_a_type,type,
set_Product_prod_a_a: $tType ).
thf(heap_T5660665574680485309rray_o_type,type,
heap_T5660665574680485309rray_o: $tType ).
thf(heap_e7401611519738050253t_unit_type,type,
heap_e7401611519738050253t_unit: $tType ).
thf(product_prod_num_num_type,type,
product_prod_num_num: $tType ).
thf(product_prod_nat_num_type,type,
product_prod_nat_num: $tType ).
thf(product_prod_nat_nat_type,type,
product_prod_nat_nat: $tType ).
thf(product_prod_nat_int_type,type,
product_prod_nat_int: $tType ).
thf(product_prod_int_nat_type,type,
product_prod_int_nat: $tType ).
thf(product_prod_int_int_type,type,
product_prod_int_int: $tType ).
thf(list_P4002435161011370285od_o_o_type,type,
list_P4002435161011370285od_o_o: $tType ).
thf(set_Product_prod_o_o_type,type,
set_Product_prod_o_o: $tType ).
thf(list_option_num_type,type,
list_option_num: $tType ).
thf(option_set_nat_type,type,
option_set_nat: $tType ).
thf(option_set_int_type,type,
option_set_int: $tType ).
thf(option_Code_integer_type,type,
option_Code_integer: $tType ).
thf(filter_set_nat_type,type,
filter_set_nat: $tType ).
thf(heap_Time_Heap_nat_type,type,
heap_Time_Heap_nat: $tType ).
thf(heap_Time_Heap_int_type,type,
heap_Time_Heap_int: $tType ).
thf(set_list_nat_type,type,
set_list_nat: $tType ).
thf(set_list_int_type,type,
set_list_int: $tType ).
thf(product_prod_nat_o_type,type,
product_prod_nat_o: $tType ).
thf(product_prod_int_o_type,type,
product_prod_int_o: $tType ).
thf(product_prod_o_nat_type,type,
product_prod_o_nat: $tType ).
thf(product_prod_o_int_type,type,
product_prod_o_int: $tType ).
thf(set_set_nat_type,type,
set_set_nat: $tType ).
thf(set_set_int_type,type,
set_set_int: $tType ).
thf(set_Code_integer_type,type,
set_Code_integer: $tType ).
thf(array_Product_unit_type,type,
array_Product_unit: $tType ).
thf(list_Product_unit_type,type,
list_Product_unit: $tType ).
thf(option_assn_type,type,
option_assn: $tType ).
thf(ref_Product_unit_type,type,
ref_Product_unit: $tType ).
thf(set_Product_unit_type,type,
set_Product_unit: $tType ).
thf(product_prod_b_b_type,type,
product_prod_b_b: $tType ).
thf(product_prod_a_a_type,type,
product_prod_a_a: $tType ).
thf(option_set_o_type,type,
option_set_o: $tType ).
thf(heap_Time_Heap_b_type,type,
heap_Time_Heap_b: $tType ).
thf(heap_Time_Heap_a_type,type,
heap_Time_Heap_a: $tType ).
thf(heap_Time_Heap_o_type,type,
heap_Time_Heap_o: $tType ).
thf(set_list_o_type,type,
set_list_o: $tType ).
thf(product_prod_o_o_type,type,
product_prod_o_o: $tType ).
thf(set_assn_type,type,
set_assn: $tType ).
thf(option_rat_type,type,
option_rat: $tType ).
thf(option_num_type,type,
option_num: $tType ).
thf(option_nat_type,type,
option_nat: $tType ).
thf(option_int_type,type,
option_int: $tType ).
thf(list_char_type,type,
list_char: $tType ).
thf(filter_nat_type,type,
filter_nat: $tType ).
thf(array_nat_type,type,
array_nat: $tType ).
thf(array_int_type,type,
array_int: $tType ).
thf(list_rat_type,type,
list_rat: $tType ).
thf(list_num_type,type,
list_num: $tType ).
thf(list_nat_type,type,
list_nat: $tType ).
thf(list_int_type,type,
list_int: $tType ).
thf(set_rat_type,type,
set_rat: $tType ).
thf(set_num_type,type,
set_num: $tType ).
thf(set_nat_type,type,
set_nat: $tType ).
thf(set_int_type,type,
set_int: $tType ).
thf(code_natural_type,type,
code_natural: $tType ).
thf(code_integer_type,type,
code_integer: $tType ).
thf(product_unit_type,type,
product_unit: $tType ).
thf(option_o_type,type,
option_o: $tType ).
thf(list_b_type,type,
list_b: $tType ).
thf(list_a_type,type,
list_a: $tType ).
thf(array_o_type,type,
array_o: $tType ).
thf(list_o_type,type,
list_o: $tType ).
thf(assn_type,type,
assn: $tType ).
thf(set_o_type,type,
set_o: $tType ).
thf(char_type,type,
char: $tType ).
thf(rat_type,type,
rat: $tType ).
thf(num_type,type,
num: $tType ).
thf(nat_type,type,
nat: $tType ).
thf(int_type,type,
int: $tType ).
thf(b_type,type,
b: $tType ).
thf(a_type,type,
a: $tType ).
thf(abs_assn_decl,type,
abs_assn: ( produc3658429121746597890et_nat > $o ) > assn ).
thf(rep_assn_decl,type,
rep_assn: assn > produc3658429121746597890et_nat > $o ).
thf(entails_decl,type,
entails: assn > assn > $o ).
thf(in_range_decl,type,
in_range: produc3658429121746597890et_nat > $o ).
thf(relH_decl,type,
relH: set_nat > heap_e7401611519738050253t_unit > heap_e7401611519738050253t_unit > $o ).
thf(uminus_uminus_assn_decl,type,
uminus_uminus_assn: assn > assn ).
thf(heap_T6553295506729943825t_unit_decl,type,
heap_T6553295506729943825t_unit: heap_T5738788834812785303t_unit > heap_e7401611519738050253t_unit > heap_e7401611519738050253t_unit > product_unit > nat > $o ).
thf(heap_Time_effect_a_decl,type,
heap_Time_effect_a: heap_Time_Heap_a > heap_e7401611519738050253t_unit > heap_e7401611519738050253t_unit > a > nat > $o ).
thf(heap_Time_effect_b_decl,type,
heap_Time_effect_b: heap_Time_Heap_b > heap_e7401611519738050253t_unit > heap_e7401611519738050253t_unit > b > nat > $o ).
thf(heap_T584514906347983379t_unit_decl,type,
heap_T584514906347983379t_unit: heap_T5738788834812785303t_unit > heap_e7401611519738050253t_unit > $o ).
thf(heap_Time_success_a_decl,type,
heap_Time_success_a: heap_Time_Heap_a > heap_e7401611519738050253t_unit > $o ).
thf(heap_Time_success_b_decl,type,
heap_Time_success_b: heap_Time_Heap_b > heap_e7401611519738050253t_unit > $o ).
thf(hoare_8945653483474564448t_unit_decl,type,
hoare_8945653483474564448t_unit: assn > heap_T5738788834812785303t_unit > ( product_unit > assn ) > $o ).
thf(hoare_hoare_triple_a_decl,type,
hoare_hoare_triple_a: assn > heap_Time_Heap_a > ( a > assn ) > $o ).
thf(hoare_hoare_triple_b_decl,type,
hoare_hoare_triple_b: assn > heap_Time_Heap_b > ( b > assn ) > $o ).
thf(hoare_new_addrs_decl,type,
hoare_new_addrs: heap_e7401611519738050253t_unit > set_nat > heap_e7401611519738050253t_unit > set_nat ).
thf(sup_sup_assn_decl,type,
sup_sup_assn: assn > assn > assn ).
thf(bot_bot_assn_decl,type,
bot_bot_assn: assn ).
thf(bot_bot_set_nat_decl,type,
bot_bot_set_nat: set_nat ).
thf(top_top_assn_decl,type,
top_top_assn: assn ).
thf(produc7507926704131184380et_nat_decl,type,
produc7507926704131184380et_nat: heap_e7401611519738050253t_unit > set_nat > produc3658429121746597890et_nat ).
thf(p_decl,type,
p: assn ).
thf(q_decl,type,
q: b > assn ).
thf(r_decl,type,
r: a > assn ).
thf(as_decl,type,
as: set_nat ).
thf(f_decl,type,
f: heap_Time_Heap_a ).
thf(g_decl,type,
g: a > heap_Time_Heap_b ).
thf(h_decl,type,
h: heap_e7401611519738050253t_unit ).
thf(h2_decl,type,
h2: heap_e7401611519738050253t_unit ).
thf(h3_decl,type,
h3: heap_e7401611519738050253t_unit ).
thf(rf_decl,type,
rf: a ).
thf(rg_decl,type,
rg: b ).
thf(70,axiom,
! [A: assn,B: heap_T5738788834812785303t_unit,C: product_unit > assn] :
( ! [D: produc3658429121746597890et_nat] :
( ( rep_assn @ A @ D )
=> ( hoare_8945653483474564448t_unit @ A @ B @ C ) )
=> ( hoare_8945653483474564448t_unit @ A @ B @ C ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_103_hoare__triple__preI) ).
thf(257,plain,
! [A: assn,B: heap_T5738788834812785303t_unit,C: product_unit > assn] :
( ! [D: produc3658429121746597890et_nat] :
( ( rep_assn @ A @ D )
=> ( hoare_8945653483474564448t_unit @ A @ B @ C ) )
=> ( hoare_8945653483474564448t_unit @ A @ B @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[70]) ).
thf(30,axiom,
( sup_sup_assn
= ( ^ [A: assn,B: assn] :
( abs_assn
@ ^ [C: produc3658429121746597890et_nat] :
( ( rep_assn @ A @ C )
| ( rep_assn @ B @ C ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3887_sup__assn__def) ).
thf(141,plain,
( sup_sup_assn
= ( ^ [A: assn,B: assn] :
( abs_assn
@ ^ [C: produc3658429121746597890et_nat] :
( ( rep_assn @ A @ C )
| ( rep_assn @ B @ C ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(43,axiom,
! [A: set_nat,B: heap_e7401611519738050253t_unit,C: heap_e7401611519738050253t_unit,D: assn] :
( ( relH @ A @ B @ C )
=> ( ( rep_assn @ D @ ( produc7507926704131184380et_nat @ B @ A ) )
= ( rep_assn @ D @ ( produc7507926704131184380et_nat @ C @ A ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_548_mod__relH) ).
thf(173,plain,
! [A: set_nat,B: heap_e7401611519738050253t_unit,C: heap_e7401611519738050253t_unit,D: assn] :
( ( relH @ A @ B @ C )
=> ( ( rep_assn @ D @ ( produc7507926704131184380et_nat @ B @ A ) )
= ( rep_assn @ D @ ( produc7507926704131184380et_nat @ C @ A ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[43]) ).
thf(20,axiom,
! [A: assn,B: heap_Time_Heap_b,C: b > assn,D: b > assn] :
( ( hoare_hoare_triple_b @ A @ B @ C )
=> ( ! [E: b] : ( entails @ ( C @ E ) @ ( D @ E ) )
=> ( hoare_hoare_triple_b @ A @ B @ D ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2518_cons__post__rule) ).
thf(118,plain,
! [A: assn,B: heap_Time_Heap_b,C: b > assn,D: b > assn] :
( ( hoare_hoare_triple_b @ A @ B @ C )
=> ( ! [E: b] : ( entails @ ( C @ E ) @ ( D @ E ) )
=> ( hoare_hoare_triple_b @ A @ B @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(11,axiom,
! [A: heap_Time_Heap_b,B: b > assn] : ( hoare_hoare_triple_b @ bot_bot_assn @ A @ B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1995_false__rule) ).
thf(95,plain,
! [A: heap_Time_Heap_b,B: b > assn] : ( hoare_hoare_triple_b @ bot_bot_assn @ A @ B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(44,axiom,
! [A: assn,B: assn] :
( ! [C: produc3658429121746597890et_nat] :
( ( rep_assn @ A @ C )
=> ( rep_assn @ B @ C ) )
=> ( entails @ A @ B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2500_entailsI) ).
thf(177,plain,
! [A: assn,B: assn] :
( ! [C: produc3658429121746597890et_nat] :
( ( rep_assn @ A @ C )
=> ( rep_assn @ B @ C ) )
=> ( entails @ A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(29,axiom,
! [A: a] : ( hoare_hoare_triple_b @ ( r @ A ) @ ( g @ A ) @ q ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_54_T2) ).
thf(139,plain,
! [A: a] : ( hoare_hoare_triple_b @ ( r @ A ) @ ( g @ A ) @ q ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(56,axiom,
rep_assn @ ( q @ rg ) @ ( produc7507926704131184380et_nat @ h @ ( hoare_new_addrs @ h2 @ ( hoare_new_addrs @ h3 @ as @ h2 ) @ h ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3_POST__G) ).
thf(214,plain,
rep_assn @ ( q @ rg ) @ ( produc7507926704131184380et_nat @ h @ ( hoare_new_addrs @ h2 @ ( hoare_new_addrs @ h3 @ as @ h2 ) @ h ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[56]) ).
thf(25,axiom,
hoare_hoare_triple_a @ p @ f @ r,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_53_T1) ).
thf(131,plain,
hoare_hoare_triple_a @ p @ f @ r,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(14,axiom,
! [A: assn] : ( entails @ bot_bot_assn @ A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2533_ent__false) ).
thf(101,plain,
! [A: assn] : ( entails @ bot_bot_assn @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(67,axiom,
! [A: assn,B: heap_e7401611519738050253t_unit,C: heap_e7401611519738050253t_unit] :
( ( rep_assn @ A @ ( produc7507926704131184380et_nat @ B @ bot_bot_set_nat ) )
= ( rep_assn @ A @ ( produc7507926704131184380et_nat @ C @ bot_bot_set_nat ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1965_mod__h__bot__indep) ).
thf(249,plain,
! [A: assn,B: heap_e7401611519738050253t_unit,C: heap_e7401611519738050253t_unit] :
( ( rep_assn @ A @ ( produc7507926704131184380et_nat @ B @ bot_bot_set_nat ) )
= ( rep_assn @ A @ ( produc7507926704131184380et_nat @ C @ bot_bot_set_nat ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[67]) ).
thf(42,axiom,
! [A: assn,B: assn,C: heap_Time_Heap_a,D: a > assn] :
( ( entails @ A @ B )
=> ( ( hoare_hoare_triple_a @ B @ C @ D )
=> ( hoare_hoare_triple_a @ A @ C @ D ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2566_cons__pre__rule) ).
thf(170,plain,
! [A: assn,B: assn,C: heap_Time_Heap_a,D: a > assn] :
( ( entails @ A @ B )
=> ( ( hoare_hoare_triple_a @ B @ C @ D )
=> ( hoare_hoare_triple_a @ A @ C @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(19,axiom,
! [A: assn,B: assn,C: assn] :
( ( entails @ A @ B )
=> ( ( entails @ B @ C )
=> ( entails @ A @ C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2311_ent__trans) ).
thf(115,plain,
! [A: assn,B: assn,C: assn] :
( ( entails @ A @ B )
=> ( ( entails @ B @ C )
=> ( entails @ A @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(46,axiom,
! [A: produc3658429121746597890et_nat > $o,B: assn] :
( ! [C: produc3658429121746597890et_nat] :
( ( A @ C )
= ( rep_assn @ B @ C ) )
=> ( ( abs_assn @ A )
= B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3810_Abs__assn__eqI_I1_J) ).
thf(184,plain,
! [A: produc3658429121746597890et_nat > $o,B: assn] :
( ! [C: produc3658429121746597890et_nat] :
( ( A @ C )
= ( rep_assn @ B @ C ) )
=> ( ( abs_assn @ A )
= B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(51,axiom,
! [A: heap_e7401611519738050253t_unit] : ( rep_assn @ top_top_assn @ ( produc7507926704131184380et_nat @ A @ bot_bot_set_nat ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_9965_mod__h__bot__iff_I2_J) ).
thf(196,plain,
! [A: heap_e7401611519738050253t_unit] : ( rep_assn @ top_top_assn @ ( produc7507926704131184380et_nat @ A @ bot_bot_set_nat ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[51]) ).
thf(36,axiom,
! [A: heap_Time_Heap_a,B: a > assn] : ( hoare_hoare_triple_a @ bot_bot_assn @ A @ B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1994_false__rule) ).
thf(157,plain,
! [A: heap_Time_Heap_a,B: a > assn] : ( hoare_hoare_triple_a @ bot_bot_assn @ A @ B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(48,axiom,
rep_assn @ ( r @ rf ) @ ( produc7507926704131184380et_nat @ h2 @ ( hoare_new_addrs @ h3 @ as @ h2 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_4_POST__F) ).
thf(189,plain,
rep_assn @ ( r @ rf ) @ ( produc7507926704131184380et_nat @ h2 @ ( hoare_new_addrs @ h3 @ as @ h2 ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[48]) ).
thf(5,axiom,
! [A: set_nat,B: heap_e7401611519738050253t_unit,C: heap_e7401611519738050253t_unit] :
( ( relH @ A @ B @ C )
=> ( in_range @ ( produc7507926704131184380et_nat @ B @ A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3655_relH__in__rangeI_I1_J) ).
thf(78,plain,
! [A: set_nat,B: heap_e7401611519738050253t_unit,C: heap_e7401611519738050253t_unit] :
( ( relH @ A @ B @ C )
=> ( in_range @ ( produc7507926704131184380et_nat @ B @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(39,axiom,
! [A: assn] : ( entails @ A @ top_top_assn ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_9960_ent__true) ).
thf(164,plain,
! [A: assn] : ( entails @ A @ top_top_assn ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).
thf(16,axiom,
! [A: assn,B: assn] :
( ( entails @ A @ B )
=> ( ( entails @ B @ A )
=> ( A = B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2309_ent__iffI) ).
thf(106,plain,
! [A: assn,B: assn] :
( ( entails @ A @ B )
=> ( ( entails @ B @ A )
=> ( A = B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(21,axiom,
! [A: assn,B: assn,C: assn] :
( ( entails @ A @ B )
=> ( entails @ A @ ( sup_sup_assn @ B @ C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2526_ent__disjI1_H) ).
thf(121,plain,
! [A: assn,B: assn,C: assn] :
( ( entails @ A @ B )
=> ( entails @ A @ ( sup_sup_assn @ B @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(7,axiom,
( uminus_uminus_assn
= ( ^ [A: assn] :
( abs_assn
@ ^ [B: produc3658429121746597890et_nat] :
( ( in_range @ B )
& ~ ( rep_assn @ A @ B ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_4882_uminus__assn__def) ).
thf(84,plain,
( uminus_uminus_assn
= ( ^ [A: assn] :
( abs_assn
@ ^ [B: produc3658429121746597890et_nat] :
( ( in_range @ B )
& ~ ( rep_assn @ A @ B ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(26,axiom,
! [A: heap_e7401611519738050253t_unit,B: set_nat] :
( ( in_range @ ( produc7507926704131184380et_nat @ A @ B ) )
=> ( relH @ B @ A @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3656_relH__refl) ).
thf(132,plain,
! [A: heap_e7401611519738050253t_unit,B: set_nat] :
( ( in_range @ ( produc7507926704131184380et_nat @ A @ B ) )
=> ( relH @ B @ A @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(9,axiom,
! [A: assn,B: assn,C: heap_e7401611519738050253t_unit] :
( ( rep_assn @ ( sup_sup_assn @ A @ B ) @ ( produc7507926704131184380et_nat @ C @ bot_bot_set_nat ) )
= ( ( rep_assn @ A @ ( produc7507926704131184380et_nat @ C @ bot_bot_set_nat ) )
| ( rep_assn @ B @ ( produc7507926704131184380et_nat @ C @ bot_bot_set_nat ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1740_mod__h__bot__iff_I7_J) ).
thf(89,plain,
! [A: assn,B: assn,C: heap_e7401611519738050253t_unit] :
( ( rep_assn @ ( sup_sup_assn @ A @ B ) @ ( produc7507926704131184380et_nat @ C @ bot_bot_set_nat ) )
= ( ( rep_assn @ A @ ( produc7507926704131184380et_nat @ C @ bot_bot_set_nat ) )
| ( rep_assn @ B @ ( produc7507926704131184380et_nat @ C @ bot_bot_set_nat ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(54,axiom,
! [A: assn,B: assn,C: produc3658429121746597890et_nat] :
( ( rep_assn @ ( sup_sup_assn @ A @ B ) @ C )
= ( ( rep_assn @ A @ C )
| ( rep_assn @ B @ C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1127_mod__or__dist) ).
thf(206,plain,
! [A: assn,B: assn,C: produc3658429121746597890et_nat] :
( ( rep_assn @ ( sup_sup_assn @ A @ B ) @ C )
= ( ( rep_assn @ A @ C )
| ( rep_assn @ B @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[54]) ).
thf(66,axiom,
rep_assn @ p @ ( produc7507926704131184380et_nat @ h3 @ as ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1__092_060open_062_Ih_M_Aas_J_A_092_060Turnstile_062_AP_092_060close_062) ).
thf(248,plain,
rep_assn @ p @ ( produc7507926704131184380et_nat @ h3 @ as ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[66]) ).
thf(53,axiom,
! [A: assn,B: heap_Time_Heap_b,C: b > assn] :
( ! [D: produc3658429121746597890et_nat] :
( ( rep_assn @ A @ D )
=> ( hoare_hoare_triple_b @ A @ B @ C ) )
=> ( hoare_hoare_triple_b @ A @ B @ C ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_102_hoare__triple__preI) ).
thf(201,plain,
! [A: assn,B: heap_Time_Heap_b,C: b > assn] :
( ! [D: produc3658429121746597890et_nat] :
( ( rep_assn @ A @ D )
=> ( hoare_hoare_triple_b @ A @ B @ C ) )
=> ( hoare_hoare_triple_b @ A @ B @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[53]) ).
thf(58,axiom,
! [A: heap_e7401611519738050253t_unit,B: set_nat] :
( ( hoare_new_addrs @ A @ B @ A )
= B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2_new__addr__refl) ).
thf(220,plain,
! [A: heap_e7401611519738050253t_unit,B: set_nat] :
( ( hoare_new_addrs @ A @ B @ A )
= B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[58]) ).
thf(10,axiom,
! [A: assn,B: assn,C: heap_Time_Heap_b,D: b > assn] :
( ( entails @ A @ B )
=> ( ( hoare_hoare_triple_b @ B @ C @ D )
=> ( hoare_hoare_triple_b @ A @ C @ D ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2567_cons__pre__rule) ).
thf(92,plain,
! [A: assn,B: assn,C: heap_Time_Heap_b,D: b > assn] :
( ( entails @ A @ B )
=> ( ( hoare_hoare_triple_b @ B @ C @ D )
=> ( hoare_hoare_triple_b @ A @ C @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(61,axiom,
( entails
= ( ^ [A: assn,B: assn] :
! [C: produc3658429121746597890et_nat] :
( ( rep_assn @ A @ C )
=> ( rep_assn @ B @ C ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2501_entails__def) ).
thf(229,plain,
( entails
= ( ^ [A: assn,B: assn] :
! [C: produc3658429121746597890et_nat] :
( ( rep_assn @ A @ C )
=> ( rep_assn @ B @ C ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[61]) ).
thf(68,axiom,
! [A: assn,B: produc3658429121746597890et_nat] :
( ( rep_assn @ A @ B )
=> ( in_range @ B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3653_models__in__range) ).
thf(252,plain,
! [A: assn,B: produc3658429121746597890et_nat] :
( ( rep_assn @ A @ B )
=> ( in_range @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[68]) ).
thf(12,axiom,
! [A: assn] : ( entails @ A @ A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2310_ent__refl) ).
thf(97,plain,
! [A: assn] : ( entails @ A @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(17,axiom,
! [A: assn,B: assn,C: product_unit > assn,D: product_unit > assn,E: heap_T5738788834812785303t_unit] :
( ( entails @ A @ B )
=> ( ! [F: product_unit] : ( entails @ ( C @ F ) @ ( D @ F ) )
=> ( ( hoare_8945653483474564448t_unit @ B @ E @ C )
=> ( hoare_8945653483474564448t_unit @ A @ E @ D ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2522_cons__rule) ).
thf(109,plain,
! [A: assn,B: assn,C: product_unit > assn,D: product_unit > assn,E: heap_T5738788834812785303t_unit] :
( ( entails @ A @ B )
=> ( ! [F: product_unit] : ( entails @ ( C @ F ) @ ( D @ F ) )
=> ( ( hoare_8945653483474564448t_unit @ B @ E @ C )
=> ( hoare_8945653483474564448t_unit @ A @ E @ D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(22,axiom,
( top_top_assn
= ( abs_assn @ in_range ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_9964_top__assn__def) ).
thf(124,plain,
( top_top_assn
= ( abs_assn @ in_range ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(50,axiom,
! [A: assn] :
( ( abs_assn @ ( rep_assn @ A ) )
= A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3701_Rep__assn__inverse) ).
thf(193,plain,
! [A: assn] :
( ( abs_assn @ ( rep_assn @ A ) )
= A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[50]) ).
thf(27,axiom,
! [A: heap_e7401611519738050253t_unit] : ( in_range @ ( produc7507926704131184380et_nat @ A @ bot_bot_set_nat ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3646_in__range__empty) ).
thf(134,plain,
! [A: heap_e7401611519738050253t_unit] : ( in_range @ ( produc7507926704131184380et_nat @ A @ bot_bot_set_nat ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(3,axiom,
! [A: assn,B: produc3658429121746597890et_nat] :
( ( rep_assn @ ( uminus_uminus_assn @ A ) @ B )
= ( ( in_range @ B )
& ~ ( rep_assn @ A @ B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_4753_mod__not__dist) ).
thf(73,plain,
! [A: assn,B: produc3658429121746597890et_nat] :
( ( rep_assn @ ( uminus_uminus_assn @ A ) @ B )
= ( ( in_range @ B )
& ~ ( rep_assn @ A @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(24,axiom,
! [A: assn,B: assn,C: assn] :
( ( entails @ A @ B )
=> ( entails @ A @ ( sup_sup_assn @ C @ B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2527_ent__disjI2_H) ).
thf(128,plain,
! [A: assn,B: assn,C: assn] :
( ( entails @ A @ B )
=> ( entails @ A @ ( sup_sup_assn @ C @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(65,axiom,
! [A: produc3658429121746597890et_nat] :
~ ! [B: heap_e7401611519738050253t_unit,C: set_nat] :
( A
!= ( produc7507926704131184380et_nat @ B @ C ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_16_one__assn__raw_Ocases) ).
thf(244,plain,
! [A: produc3658429121746597890et_nat] :
~ ! [B: heap_e7401611519738050253t_unit,C: set_nat] :
( A
!= ( produc7507926704131184380et_nat @ B @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[65]) ).
thf(40,axiom,
! [A: assn,B: assn,C: assn] :
( ( entails @ ( sup_sup_assn @ A @ B ) @ C )
=> ( entails @ A @ C ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2524_ent__disjI1) ).
thf(166,plain,
! [A: assn,B: assn,C: assn] :
( ( entails @ ( sup_sup_assn @ A @ B ) @ C )
=> ( entails @ A @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).
thf(33,axiom,
! [A: assn,B: heap_T5738788834812785303t_unit,C: product_unit > assn,D: product_unit > assn] :
( ( hoare_8945653483474564448t_unit @ A @ B @ C )
=> ( ! [E: product_unit] : ( entails @ ( C @ E ) @ ( D @ E ) )
=> ( hoare_8945653483474564448t_unit @ A @ B @ D ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2519_cons__post__rule) ).
thf(148,plain,
! [A: assn,B: heap_T5738788834812785303t_unit,C: product_unit > assn,D: product_unit > assn] :
( ( hoare_8945653483474564448t_unit @ A @ B @ C )
=> ( ! [E: product_unit] : ( entails @ ( C @ E ) @ ( D @ E ) )
=> ( hoare_8945653483474564448t_unit @ A @ B @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(38,axiom,
! [A: set_nat,B: heap_e7401611519738050253t_unit,C: heap_e7401611519738050253t_unit,D: heap_e7401611519738050253t_unit] :
( ( relH @ A @ B @ C )
=> ( ( relH @ A @ C @ D )
=> ( relH @ A @ B @ D ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_331_relH__trans) ).
thf(161,plain,
! [A: set_nat,B: heap_e7401611519738050253t_unit,C: heap_e7401611519738050253t_unit,D: heap_e7401611519738050253t_unit] :
( ( relH @ A @ B @ C )
=> ( ( relH @ A @ C @ D )
=> ( relH @ A @ B @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(63,axiom,
! [A: assn,B: heap_Time_Heap_b,C: b > assn,D: heap_e7401611519738050253t_unit,E: set_nat] :
( ( hoare_hoare_triple_b @ A @ B @ C )
=> ( ( rep_assn @ A @ ( produc7507926704131184380et_nat @ D @ E ) )
=> ? [F: heap_e7401611519738050253t_unit,G: b,H: nat] :
( ( heap_Time_effect_b @ B @ D @ F @ G @ H )
& ( rep_assn @ ( C @ G ) @ ( produc7507926704131184380et_nat @ F @ ( hoare_new_addrs @ D @ E @ F ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_140_hoare__triple__effect) ).
thf(236,plain,
! [A: assn,B: heap_Time_Heap_b,C: b > assn,D: heap_e7401611519738050253t_unit,E: set_nat] :
( ( hoare_hoare_triple_b @ A @ B @ C )
=> ( ( rep_assn @ A @ ( produc7507926704131184380et_nat @ D @ E ) )
=> ? [F: heap_e7401611519738050253t_unit,G: b,H: nat] :
( ( heap_Time_effect_b @ B @ D @ F @ G @ H )
& ( rep_assn @ ( C @ G ) @ ( produc7507926704131184380et_nat @ F @ ( hoare_new_addrs @ D @ E @ F ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[63]) ).
thf(45,axiom,
! [A: assn,B: assn] :
( ( ( rep_assn @ A )
= ( rep_assn @ B ) )
= ( A = B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_5_Rep__assn__inject) ).
thf(181,plain,
! [A: assn,B: assn] :
( ( ( rep_assn @ A )
= ( rep_assn @ B ) )
= ( A = B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).
thf(8,axiom,
! [A: assn,B: assn,C: b > assn,D: b > assn,E: heap_Time_Heap_b] :
( ( entails @ A @ B )
=> ( ! [F: b] : ( entails @ ( C @ F ) @ ( D @ F ) )
=> ( ( hoare_hoare_triple_b @ B @ E @ C )
=> ( hoare_hoare_triple_b @ A @ E @ D ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2521_cons__rule) ).
thf(86,plain,
! [A: assn,B: assn,C: b > assn,D: b > assn,E: heap_Time_Heap_b] :
( ( entails @ A @ B )
=> ( ! [F: b] : ( entails @ ( C @ F ) @ ( D @ F ) )
=> ( ( hoare_hoare_triple_b @ B @ E @ C )
=> ( hoare_hoare_triple_b @ A @ E @ D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(37,axiom,
! [A: set_nat,B: heap_e7401611519738050253t_unit,C: heap_e7401611519738050253t_unit] :
( ( relH @ A @ B @ C )
=> ( relH @ A @ C @ B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_332_relH__sym) ).
thf(159,plain,
! [A: set_nat,B: heap_e7401611519738050253t_unit,C: heap_e7401611519738050253t_unit] :
( ( relH @ A @ B @ C )
=> ( relH @ A @ C @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(47,axiom,
( ( hoare_new_addrs @ h2 @ ( hoare_new_addrs @ h3 @ as @ h2 ) @ h )
= ( hoare_new_addrs @ h3 @ as @ h ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_0__092_060open_062new__addrs_Ah_H_A_Inew__addrs_Ah_Aas_Ah_H_J_Ah_H_H_A_061_Anew__addrs_Ah_Aas_Ah_H_H_092_060close_062) ).
thf(187,plain,
( ( hoare_new_addrs @ h2 @ ( hoare_new_addrs @ h3 @ as @ h2 ) @ h )
= ( hoare_new_addrs @ h3 @ as @ h ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).
thf(6,axiom,
! [A: assn,B: assn,C: assn] :
( ( entails @ A @ B )
=> ( ( entails @ C @ B )
=> ( entails @ ( sup_sup_assn @ A @ C ) @ B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2523_ent__disjE) ).
thf(81,plain,
! [A: assn,B: assn,C: assn] :
( ( entails @ A @ B )
=> ( ( entails @ C @ B )
=> ( entails @ ( sup_sup_assn @ A @ C ) @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(4,axiom,
! [A: assn,B: assn,C: assn] :
( ( entails @ ( sup_sup_assn @ A @ B ) @ C )
=> ( entails @ B @ C ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2525_ent__disjI2) ).
thf(76,plain,
! [A: assn,B: assn,C: assn] :
( ( entails @ ( sup_sup_assn @ A @ B ) @ C )
=> ( entails @ B @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(15,axiom,
! [A: assn,B: heap_Time_Heap_a,C: a > assn,D: a > assn] :
( ( hoare_hoare_triple_a @ A @ B @ C )
=> ( ! [E: a] : ( entails @ ( C @ E ) @ ( D @ E ) )
=> ( hoare_hoare_triple_a @ A @ B @ D ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2517_cons__post__rule) ).
thf(103,plain,
! [A: assn,B: heap_Time_Heap_a,C: a > assn,D: a > assn] :
( ( hoare_hoare_triple_a @ A @ B @ C )
=> ( ! [E: a] : ( entails @ ( C @ E ) @ ( D @ E ) )
=> ( hoare_hoare_triple_a @ A @ B @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(52,axiom,
! [A: assn,B: produc3658429121746597890et_nat,C: assn] :
( ( rep_assn @ A @ B )
=> ( ( entails @ A @ C )
=> ( rep_assn @ C @ B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2498_ent__fwd) ).
thf(198,plain,
! [A: assn,B: produc3658429121746597890et_nat,C: assn] :
( ( rep_assn @ A @ B )
=> ( ( entails @ A @ C )
=> ( rep_assn @ C @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[52]) ).
thf(59,axiom,
! [A: produc3658429121746597890et_nat] :
~ ( rep_assn @ bot_bot_assn @ A ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2018_mod__false) ).
thf(223,plain,
! [A: produc3658429121746597890et_nat] :
~ ( rep_assn @ bot_bot_assn @ A ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[59]) ).
thf(60,axiom,
! [A: assn,B: heap_Time_Heap_a,C: a > assn,D: heap_e7401611519738050253t_unit,E: set_nat] :
( ( hoare_hoare_triple_a @ A @ B @ C )
=> ( ( rep_assn @ A @ ( produc7507926704131184380et_nat @ D @ E ) )
=> ( heap_Time_success_a @ B @ D ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_142_hoare__triple__success) ).
thf(226,plain,
! [A: assn,B: heap_Time_Heap_a,C: a > assn,D: heap_e7401611519738050253t_unit,E: set_nat] :
( ( hoare_hoare_triple_a @ A @ B @ C )
=> ( ( rep_assn @ A @ ( produc7507926704131184380et_nat @ D @ E ) )
=> ( heap_Time_success_a @ B @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[60]) ).
thf(64,axiom,
! [A: assn,B: heap_Time_Heap_b,C: b > assn,D: heap_e7401611519738050253t_unit,E: set_nat] :
( ( hoare_hoare_triple_b @ A @ B @ C )
=> ( ( rep_assn @ A @ ( produc7507926704131184380et_nat @ D @ E ) )
=> ( heap_Time_success_b @ B @ D ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_143_hoare__triple__success) ).
thf(241,plain,
! [A: assn,B: heap_Time_Heap_b,C: b > assn,D: heap_e7401611519738050253t_unit,E: set_nat] :
( ( hoare_hoare_triple_b @ A @ B @ C )
=> ( ( rep_assn @ A @ ( produc7507926704131184380et_nat @ D @ E ) )
=> ( heap_Time_success_b @ B @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[64]) ).
thf(55,axiom,
! [A: assn,B: heap_Time_Heap_a,C: a > assn] :
( ! [D: produc3658429121746597890et_nat] :
( ( rep_assn @ A @ D )
=> ( hoare_hoare_triple_a @ A @ B @ C ) )
=> ( hoare_hoare_triple_a @ A @ B @ C ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_101_hoare__triple__preI) ).
thf(209,plain,
! [A: assn,B: heap_Time_Heap_a,C: a > assn] :
( ! [D: produc3658429121746597890et_nat] :
( ( rep_assn @ A @ D )
=> ( hoare_hoare_triple_a @ A @ B @ C ) )
=> ( hoare_hoare_triple_a @ A @ B @ C ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[55]) ).
thf(18,axiom,
! [A: assn] :
( ( entails @ A @ bot_bot_assn )
= ( ! [B: produc3658429121746597890et_nat] :
~ ( rep_assn @ A @ B ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2239_ent__false__iff) ).
thf(112,plain,
! [A: assn] :
( ( entails @ A @ bot_bot_assn )
= ( ! [B: produc3658429121746597890et_nat] :
~ ( rep_assn @ A @ B ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(32,axiom,
! [A: assn,B: assn,C: a > assn,D: a > assn,E: heap_Time_Heap_a] :
( ( entails @ A @ B )
=> ( ! [F: a] : ( entails @ ( C @ F ) @ ( D @ F ) )
=> ( ( hoare_hoare_triple_a @ B @ E @ C )
=> ( hoare_hoare_triple_a @ A @ E @ D ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2520_cons__rule) ).
thf(145,plain,
! [A: assn,B: assn,C: a > assn,D: a > assn,E: heap_Time_Heap_a] :
( ( entails @ A @ B )
=> ( ! [F: a] : ( entails @ ( C @ F ) @ ( D @ F ) )
=> ( ( hoare_hoare_triple_a @ B @ E @ C )
=> ( hoare_hoare_triple_a @ A @ E @ D ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(35,axiom,
! [A: produc3658429121746597890et_nat] :
( ( rep_assn @ top_top_assn @ A )
= ( in_range @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_9958_mod__true) ).
thf(154,plain,
! [A: produc3658429121746597890et_nat] :
( ( rep_assn @ top_top_assn @ A )
= ( in_range @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(1,conjecture,
rep_assn @ ( q @ rg ) @ ( produc7507926704131184380et_nat @ h @ ( hoare_new_addrs @ h3 @ as @ h ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',conj_0) ).
thf(2,negated_conjecture,
~ ( rep_assn @ ( q @ rg ) @ ( produc7507926704131184380et_nat @ h @ ( hoare_new_addrs @ h3 @ as @ h ) ) ),
inference(neg_conjecture,[status(cth)],[1]) ).
thf(72,plain,
~ ( rep_assn @ ( q @ rg ) @ ( produc7507926704131184380et_nat @ h @ ( hoare_new_addrs @ h3 @ as @ h ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(31,axiom,
! [A: assn,B: assn] : ( entails @ A @ ( sup_sup_assn @ A @ B ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2528_ent__disjI1__direct) ).
thf(143,plain,
! [A: assn,B: assn] : ( entails @ A @ ( sup_sup_assn @ A @ B ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(62,axiom,
! [A: assn,B: heap_T5738788834812785303t_unit,C: product_unit > assn,D: heap_e7401611519738050253t_unit,E: set_nat] :
( ( hoare_8945653483474564448t_unit @ A @ B @ C )
=> ( ( rep_assn @ A @ ( produc7507926704131184380et_nat @ D @ E ) )
=> ? [F: heap_e7401611519738050253t_unit,G: product_unit,H: nat] :
( ( heap_T6553295506729943825t_unit @ B @ D @ F @ G @ H )
& ( rep_assn @ ( C @ G ) @ ( produc7507926704131184380et_nat @ F @ ( hoare_new_addrs @ D @ E @ F ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_141_hoare__triple__effect) ).
thf(231,plain,
! [A: assn,B: heap_T5738788834812785303t_unit,C: product_unit > assn,D: heap_e7401611519738050253t_unit,E: set_nat] :
( ( hoare_8945653483474564448t_unit @ A @ B @ C )
=> ( ( rep_assn @ A @ ( produc7507926704131184380et_nat @ D @ E ) )
=> ? [F: heap_e7401611519738050253t_unit,G: product_unit,H: nat] :
( ( heap_T6553295506729943825t_unit @ B @ D @ F @ G @ H )
& ( rep_assn @ ( C @ G ) @ ( produc7507926704131184380et_nat @ F @ ( hoare_new_addrs @ D @ E @ F ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[62]) ).
thf(13,axiom,
! [A: assn,B: assn] : ( entails @ A @ ( sup_sup_assn @ B @ A ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2529_ent__disjI2__direct) ).
thf(99,plain,
! [A: assn,B: assn] : ( entails @ A @ ( sup_sup_assn @ B @ A ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(34,axiom,
! [A: assn,B: assn,C: heap_T5738788834812785303t_unit,D: product_unit > assn] :
( ( entails @ A @ B )
=> ( ( hoare_8945653483474564448t_unit @ B @ C @ D )
=> ( hoare_8945653483474564448t_unit @ A @ C @ D ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2568_cons__pre__rule) ).
thf(151,plain,
! [A: assn,B: assn,C: heap_T5738788834812785303t_unit,D: product_unit > assn] :
( ( entails @ A @ B )
=> ( ( hoare_8945653483474564448t_unit @ B @ C @ D )
=> ( hoare_8945653483474564448t_unit @ A @ C @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(49,axiom,
! [A: assn,B: assn,C: produc3658429121746597890et_nat] :
( ( entails @ A @ B )
=> ( ( rep_assn @ A @ C )
=> ( rep_assn @ B @ C ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_2499_entailsD) ).
thf(190,plain,
! [A: assn,B: assn,C: produc3658429121746597890et_nat] :
( ( entails @ A @ B )
=> ( ( rep_assn @ A @ C )
=> ( rep_assn @ B @ C ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[49]) ).
thf(41,axiom,
! [A: heap_T5738788834812785303t_unit,B: product_unit > assn] : ( hoare_8945653483474564448t_unit @ bot_bot_assn @ A @ B ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_1996_false__rule) ).
thf(168,plain,
! [A: heap_T5738788834812785303t_unit,B: product_unit > assn] : ( hoare_8945653483474564448t_unit @ bot_bot_assn @ A @ B ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(71,axiom,
! [A: produc3658429121746597890et_nat > $o,B: assn] :
( ! [C: produc3658429121746597890et_nat] :
( ( A @ C )
= ( rep_assn @ B @ C ) )
=> ( B
= ( abs_assn @ A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3811_Abs__assn__eqI_I2_J) ).
thf(262,plain,
! [A: produc3658429121746597890et_nat > $o,B: assn] :
( ! [C: produc3658429121746597890et_nat] :
( ( A @ C )
= ( rep_assn @ B @ C ) )
=> ( B
= ( abs_assn @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[71]) ).
thf(23,axiom,
! [A: set_nat,B: heap_e7401611519738050253t_unit,C: heap_e7401611519738050253t_unit] :
( ( relH @ A @ B @ C )
=> ( in_range @ ( produc7507926704131184380et_nat @ C @ A ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_3654_relH__in__rangeI_I2_J) ).
thf(126,plain,
! [A: set_nat,B: heap_e7401611519738050253t_unit,C: heap_e7401611519738050253t_unit] :
( ( relH @ A @ B @ C )
=> ( in_range @ ( produc7507926704131184380et_nat @ C @ A ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(28,axiom,
top_top_assn != bot_bot_assn,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_9957_assn__basic__inequalities_I5_J) ).
thf(136,plain,
top_top_assn != bot_bot_assn,
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(69,axiom,
! [A: assn,B: heap_T5738788834812785303t_unit,C: product_unit > assn,D: heap_e7401611519738050253t_unit,E: set_nat] :
( ( hoare_8945653483474564448t_unit @ A @ B @ C )
=> ( ( rep_assn @ A @ ( produc7507926704131184380et_nat @ D @ E ) )
=> ( heap_T584514906347983379t_unit @ B @ D ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_144_hoare__triple__success) ).
thf(254,plain,
! [A: assn,B: heap_T5738788834812785303t_unit,C: product_unit > assn,D: heap_e7401611519738050253t_unit,E: set_nat] :
( ( hoare_8945653483474564448t_unit @ A @ B @ C )
=> ( ( rep_assn @ A @ ( produc7507926704131184380et_nat @ D @ E ) )
=> ( heap_T584514906347983379t_unit @ B @ D ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[69]) ).
thf(57,axiom,
! [A: assn,B: heap_Time_Heap_a,C: a > assn,D: heap_e7401611519738050253t_unit,E: set_nat] :
( ( hoare_hoare_triple_a @ A @ B @ C )
=> ( ( rep_assn @ A @ ( produc7507926704131184380et_nat @ D @ E ) )
=> ? [F: heap_e7401611519738050253t_unit,G: a,H: nat] :
( ( heap_Time_effect_a @ B @ D @ F @ G @ H )
& ( rep_assn @ ( C @ G ) @ ( produc7507926704131184380et_nat @ F @ ( hoare_new_addrs @ D @ E @ F ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fact_139_hoare__triple__effect) ).
thf(215,plain,
! [A: assn,B: heap_Time_Heap_a,C: a > assn,D: heap_e7401611519738050253t_unit,E: set_nat] :
( ( hoare_hoare_triple_a @ A @ B @ C )
=> ( ( rep_assn @ A @ ( produc7507926704131184380et_nat @ D @ E ) )
=> ? [F: heap_e7401611519738050253t_unit,G: a,H: nat] :
( ( heap_Time_effect_a @ B @ D @ F @ G @ H )
& ( rep_assn @ ( C @ G ) @ ( produc7507926704131184380et_nat @ F @ ( hoare_new_addrs @ D @ E @ F ) ) ) ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).
thf(267,plain,
$false,
inference(e,[status(thm)],[257,141,173,118,95,177,139,214,131,101,249,170,115,184,196,157,189,78,164,106,121,84,132,89,206,248,201,220,92,229,252,97,109,124,193,134,73,128,244,166,148,161,236,181,86,159,187,81,76,103,198,223,226,241,209,112,145,154,72,143,231,99,151,190,168,262,126,136,254,215]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : ITP214^1 : TPTP v9.3.1. Bugfixed v9.2.1.
% 0.00/0.08 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 0.10/0.23 % Computer : n011.cluster.edu
% 0.10/0.23 % Model : x86_64 x86_64
% 0.10/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.23 % Memory : 8046.5625MB
% 0.10/0.23 % OS : Linux 6.8.0-71-generic
% 0.10/0.24 % CPULimit : 300
% 0.10/0.24 % WCLimit : 300
% 0.10/0.24 % DateTime : Tue Sep 29 20:15:47 UTC 2026
% 0.10/0.24 % CPUTime :
% 0.10/0.24 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox2/solver/bin/leo3.jar /export/starexec/sandbox2/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox2/solver/bin/externals/eprover --instantiate 39
% 1.01/0.82 % [INFO] Parsing problem /export/starexec/sandbox2/benchmark/theBenchmark.p ...
% 6.53/2.45 % [INFO] Parsing done (1626ms).
% 6.53/2.47 % [INFO] Running in sequential loop mode.
% 7.57/2.90 % [INFO] eprover registered as external prover.
% 7.57/2.91 % [INFO] Scanning for conjecture ...
% 9.43/3.48 % [INFO] Found a conjecture (or negated_conjecture) and 10266 axioms. Running axiom selection ...
% 10.22/3.66 % [INFO] Axiom selection finished. Selected 69 axioms (removed 10197 axioms).
% 11.00/3.83 % [INFO] Problem is higher-order (TPTP THF).
% 11.00/3.85 % [INFO] Type checking passed.
% 11.00/3.86 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 15.76/5.29 % External prover 'e' found a proof!
% 15.76/5.29 % [INFO] Killing All external provers ...
% 15.76/5.29 % Time passed: 4917ms (effective reasoning time: 2817ms)
% 15.76/5.29 % Solved by strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>
% 15.76/5.29 % Axioms used in derivation (69): fact_9965_mod__h__bot__iff_I2_J, fact_102_hoare__triple__preI, fact_1995_false__rule, fact_2517_cons__post__rule, fact_3701_Rep__assn__inverse, fact_140_hoare__triple__effect, fact_0__092_060open_062new__addrs_Ah_H_A_Inew__addrs_Ah_Aas_Ah_H_J_Ah_H_H_A_061_Anew__addrs_Ah_Aas_Ah_H_H_092_060close_062, fact_9957_assn__basic__inequalities_I5_J, fact_2527_ent__disjI2_H, fact_2_new__addr__refl, fact_1996_false__rule, fact_16_one__assn__raw_Ocases, fact_3654_relH__in__rangeI_I2_J, fact_2498_ent__fwd, fact_141_hoare__triple__effect, fact_139_hoare__triple__effect, fact_2499_entailsD, fact_101_hoare__triple__preI, fact_2524_ent__disjI1, fact_2518_cons__post__rule, fact_1127_mod__or__dist, fact_3646_in__range__empty, fact_2239_ent__false__iff, fact_2568_cons__pre__rule, fact_332_relH__sym, fact_2522_cons__rule, fact_54_T2, fact_3_POST__G, fact_2310_ent__refl, fact_548_mod__relH, fact_9964_top__assn__def, fact_4882_uminus__assn__def, fact_3810_Abs__assn__eqI_I1_J, fact_144_hoare__triple__success, fact_3655_relH__in__rangeI_I1_J, fact_9958_mod__true, fact_2523_ent__disjE, fact_1__092_060open_062_Ih_M_Aas_J_A_092_060Turnstile_062_AP_092_060close_062, fact_2528_ent__disjI1__direct, fact_331_relH__trans, fact_53_T1, fact_3811_Abs__assn__eqI_I2_J, fact_3887_sup__assn__def, fact_1740_mod__h__bot__iff_I7_J, fact_2566_cons__pre__rule, fact_2501_entails__def, fact_4753_mod__not__dist, fact_1994_false__rule, fact_4_POST__F, fact_2567_cons__pre__rule, fact_2521_cons__rule, fact_9960_ent__true, fact_2529_ent__disjI2__direct, fact_2519_cons__post__rule, fact_2309_ent__iffI, fact_2311_ent__trans, fact_5_Rep__assn__inject, fact_103_hoare__triple__preI, fact_142_hoare__triple__success, fact_1965_mod__h__bot__indep, fact_2500_entailsI, fact_2526_ent__disjI1_H, fact_2018_mod__false, fact_3653_models__in__range, fact_3656_relH__refl, fact_2520_cons__rule, fact_2525_ent__disjI2, fact_143_hoare__triple__success, fact_2533_ent__false
% 15.76/5.29 % No. of inferences in proof: 142
% 15.76/5.29 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : 4917 ms resp. 2817 ms w/o parsing
% 16.65/5.42 % SZS output start Refutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
% 16.65/5.42 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------