%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : ITP206_1 : TPTP v9.0.0. Released v8.0.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n007.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sat Jun 21 05:11:57 AM UTC 2025
% Result : Theorem 6.02s 6.24s
% Output : Proof 6.44s
% Verified :
% SZS Type : Refutation
% Derivation depth : 13
% Number of leaves : 33
% Syntax : Number of formulae : 81 ( 29 unt; 0 typ; 0 def)
% Number of atoms : 374 ( 147 equ)
% Maximal formula atoms : 12 ( 4 avg)
% Number of connectives : 448 ( 180 ~; 176 |; 0 &)
% ( 48 <=>; 44 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 6 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of FOOLs : 25 ( 25 fml; 0 var)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 20 ( 18 usr; 14 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 7 con; 0-2 aty)
% Number of variables : 324 ( 293 !; 0 ?; 324 :)
% Comments :
%------------------------------------------------------------------------------
tff(thesis_type,type,
thesis: $o ).
tff(aa_Pro7711270743135521984_ref_a_type,type,
aa_Pro7711270743135521984_ref_a: ( fun_Pr1332931745038653183_ref_a * produc7812382424243267045t_unit ) > ref_a ).
tff(aa_hea1409956391221964662t_unit_type,type,
aa_hea1409956391221964662t_unit: ( fun_he3288789352778960325t_unit * heap_e7401611519738050253t_unit ) > produc7812382424243267045t_unit ).
tff(h_type,type,
h: heap_e7401611519738050253t_unit ).
tff(alloc_a_type,type,
alloc_a: a > fun_he3288789352778960325t_unit ).
tff(x_type,type,
x: a ).
tff(produc473321116828791851t_unit_type,type,
produc473321116828791851t_unit: fun_Pr1332931745038653183_ref_a ).
tff(r_type,type,
r: ref_a ).
tff(pp_type,type,
pp: bool > $o ).
tff(aa_ref_a_bool_type,type,
aa_ref_a_bool: ( fun_ref_a_bool * ref_a ) > bool ).
tff(aa_hea8135729668157506370a_bool_type,type,
aa_hea8135729668157506370a_bool: ( fun_he1716177789110362441a_bool * heap_e7401611519738050253t_unit ) > fun_ref_a_bool ).
tff(aa_Pro8575920914306358506t_unit_type,type,
aa_Pro8575920914306358506t_unit: ( fun_Pr7082408943852936193t_unit * produc7812382424243267045t_unit ) > heap_e7401611519738050253t_unit ).
tff(produc1126150082675451753t_unit_type,type,
produc1126150082675451753t_unit: fun_Pr7082408943852936193t_unit ).
tff(heap_effect_ref_a_type,type,
heap_effect_ref_a: ( heap_Heap_ref_a * heap_e7401611519738050253t_unit ) > fun_he1716177789110362441a_bool ).
tff(heap_heap_ref_a_type,type,
heap_heap_ref_a: fun_he3288789352778960325t_unit > heap_Heap_ref_a ).
tff(h2_type,type,
h2: heap_e7401611519738050253t_unit ).
tff(aa_a_Heap_Heap_ref_a_type,type,
aa_a_Heap_Heap_ref_a: ( fun_a_7797985579152759073_ref_a * a ) > heap_Heap_ref_a ).
tff(ref_a2_type,type,
ref_a2: fun_a_7797985579152759073_ref_a ).
tff(1,plain,
( ~ thesis
<=> ~ thesis ),
inference(rewrite,[status(thm)],[]) ).
tff(2,axiom,
~ thesis,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',conj_1) ).
tff(3,plain,
~ thesis,
inference(modus_ponens,[status(thm)],[2,1]) ).
tff(4,plain,
^ [F: fun_he3288789352778960325t_unit,H: heap_e7401611519738050253t_unit] :
refl(( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(F,H))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H))))
<=> pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(F,H))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H)))) )),
inference(bind,[status(th)],[]) ).
tff(5,plain,
( ! [F: fun_he3288789352778960325t_unit,H: heap_e7401611519738050253t_unit] : pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(F,H))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H))))
<=> ! [F: fun_he3288789352778960325t_unit,H: heap_e7401611519738050253t_unit] : pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(F,H))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H)))) ),
inference(quant_intro,[status(thm)],[4]) ).
tff(6,plain,
( ! [F: fun_he3288789352778960325t_unit,H: heap_e7401611519738050253t_unit] : pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(F,H))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H))))
<=> ! [F: fun_he3288789352778960325t_unit,H: heap_e7401611519738050253t_unit] : pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(F,H))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H)))) ),
inference(rewrite,[status(thm)],[]) ).
tff(7,plain,
( ! [H2: heap_e7401611519738050253t_unit,F: fun_he3288789352778960325t_unit,H: heap_e7401611519738050253t_unit,R: ref_a] : pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(F,H))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H))))
<=> ! [F: fun_he3288789352778960325t_unit,H: heap_e7401611519738050253t_unit] : pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(F,H))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H)))) ),
inference(elim_unused_vars,[status(thm)],[]) ).
tff(8,plain,
( ! [H2: heap_e7401611519738050253t_unit,F: fun_he3288789352778960325t_unit,H: heap_e7401611519738050253t_unit,R: ref_a] :
( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),H2),R))
| ( R != aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H)) )
| ( H2 != aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(F,H)) ) )
<=> ! [H2: heap_e7401611519738050253t_unit,F: fun_he3288789352778960325t_unit,H: heap_e7401611519738050253t_unit,R: ref_a] : pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(F,H))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H)))) ),
inference(destructive_equality_resolution,[status(thm)],[]) ).
tff(9,plain,
( ! [H2: heap_e7401611519738050253t_unit,F: fun_he3288789352778960325t_unit,H: heap_e7401611519738050253t_unit,R: ref_a] :
( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),H2),R))
| ( R != aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H)) )
| ( H2 != aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(F,H)) ) )
<=> ! [F: fun_he3288789352778960325t_unit,H: heap_e7401611519738050253t_unit] : pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(F,H))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H)))) ),
inference(transitivity,[status(thm)],[8,7]) ).
tff(10,plain,
^ [H2: heap_e7401611519738050253t_unit,F: fun_he3288789352778960325t_unit,H: heap_e7401611519738050253t_unit,R: ref_a] :
trans(monotonicity(rewrite(( ( ( R = aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H)) )
=> pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),H2),R)) )
<=> ( ( R != aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H)) )
| pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),H2),R)) ) )),
( ( ( H2 = aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(F,H)) )
=> ( ( R = aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H)) )
=> pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),H2),R)) ) )
<=> ( ( H2 = aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(F,H)) )
=> ( ( R != aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H)) )
| pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),H2),R)) ) ) )),
rewrite(( ( ( H2 = aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(F,H)) )
=> ( ( R != aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H)) )
| pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),H2),R)) ) )
<=> ( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),H2),R))
| ( R != aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H)) )
| ( H2 != aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(F,H)) ) ) )),
( ( ( H2 = aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(F,H)) )
=> ( ( R = aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H)) )
=> pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),H2),R)) ) )
<=> ( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),H2),R))
| ( R != aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H)) )
| ( H2 != aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(F,H)) ) ) )),
inference(bind,[status(th)],[]) ).
tff(11,plain,
( ! [H2: heap_e7401611519738050253t_unit,F: fun_he3288789352778960325t_unit,H: heap_e7401611519738050253t_unit,R: ref_a] :
( ( H2 = aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(F,H)) )
=> ( ( R = aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H)) )
=> pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),H2),R)) ) )
<=> ! [H2: heap_e7401611519738050253t_unit,F: fun_he3288789352778960325t_unit,H: heap_e7401611519738050253t_unit,R: ref_a] :
( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),H2),R))
| ( R != aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H)) )
| ( H2 != aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(F,H)) ) ) ),
inference(quant_intro,[status(thm)],[10]) ).
tff(12,plain,
( ! [H2: heap_e7401611519738050253t_unit,F: fun_he3288789352778960325t_unit,H: heap_e7401611519738050253t_unit,R: ref_a] :
( ( H2 = aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(F,H)) )
=> ( ( R = aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H)) )
=> pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),H2),R)) ) )
<=> ! [F: fun_he3288789352778960325t_unit,H: heap_e7401611519738050253t_unit] : pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(F,H))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H)))) ),
inference(transitivity,[status(thm)],[11,9]) ).
tff(13,axiom,
! [H2: heap_e7401611519738050253t_unit,F: fun_he3288789352778960325t_unit,H: heap_e7401611519738050253t_unit,R: ref_a] :
( ( H2 = aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(F,H)) )
=> ( ( R = aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H)) )
=> pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),H2),R)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_149_effect__heapI) ).
tff(14,plain,
! [F: fun_he3288789352778960325t_unit,H: heap_e7401611519738050253t_unit] : pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(F,H))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H)))),
inference(modus_ponens,[status(thm)],[13,12]) ).
tff(15,plain,
! [F: fun_he3288789352778960325t_unit,H: heap_e7401611519738050253t_unit] : pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(F,H))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H)))),
inference(modus_ponens,[status(thm)],[14,6]) ).
tff(16,plain,
! [F: fun_he3288789352778960325t_unit,H: heap_e7401611519738050253t_unit] : pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(F,H))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H)))),
inference(skolemize,[status(sab)],[15]) ).
tff(17,plain,
! [F: fun_he3288789352778960325t_unit,H: heap_e7401611519738050253t_unit] : pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(F,H))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H)))),
inference(modus_ponens,[status(thm)],[16,5]) ).
tff(18,plain,
( ~ ! [F: fun_he3288789352778960325t_unit,H: heap_e7401611519738050253t_unit] : pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(F),H),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(F,H))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(F,H))))
| pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)))) ),
inference(quant_inst,[status(thm)],[]) ).
tff(19,plain,
pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)))),
inference(unit_resolution,[status(thm)],[18,17]) ).
tff(20,plain,
^ [V: a] :
refl(( ( aa_a_Heap_Heap_ref_a(ref_a2,V) = heap_heap_ref_a(alloc_a(V)) )
<=> ( aa_a_Heap_Heap_ref_a(ref_a2,V) = heap_heap_ref_a(alloc_a(V)) ) )),
inference(bind,[status(th)],[]) ).
tff(21,plain,
( ! [V: a] : ( aa_a_Heap_Heap_ref_a(ref_a2,V) = heap_heap_ref_a(alloc_a(V)) )
<=> ! [V: a] : ( aa_a_Heap_Heap_ref_a(ref_a2,V) = heap_heap_ref_a(alloc_a(V)) ) ),
inference(quant_intro,[status(thm)],[20]) ).
tff(22,plain,
( ! [V: a] : ( aa_a_Heap_Heap_ref_a(ref_a2,V) = heap_heap_ref_a(alloc_a(V)) )
<=> ! [V: a] : ( aa_a_Heap_Heap_ref_a(ref_a2,V) = heap_heap_ref_a(alloc_a(V)) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(23,axiom,
! [V: a] : ( aa_a_Heap_Heap_ref_a(ref_a2,V) = heap_heap_ref_a(alloc_a(V)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_23_ref__def) ).
tff(24,plain,
! [V: a] : ( aa_a_Heap_Heap_ref_a(ref_a2,V) = heap_heap_ref_a(alloc_a(V)) ),
inference(modus_ponens,[status(thm)],[23,22]) ).
tff(25,plain,
! [V: a] : ( aa_a_Heap_Heap_ref_a(ref_a2,V) = heap_heap_ref_a(alloc_a(V)) ),
inference(skolemize,[status(sab)],[24]) ).
tff(26,plain,
! [V: a] : ( aa_a_Heap_Heap_ref_a(ref_a2,V) = heap_heap_ref_a(alloc_a(V)) ),
inference(modus_ponens,[status(thm)],[25,21]) ).
tff(27,plain,
( ~ ! [V: a] : ( aa_a_Heap_Heap_ref_a(ref_a2,V) = heap_heap_ref_a(alloc_a(V)) )
| ( aa_a_Heap_Heap_ref_a(ref_a2,x) = heap_heap_ref_a(alloc_a(x)) ) ),
inference(quant_inst,[status(thm)],[]) ).
tff(28,plain,
aa_a_Heap_Heap_ref_a(ref_a2,x) = heap_heap_ref_a(alloc_a(x)),
inference(unit_resolution,[status(thm)],[27,26]) ).
tff(29,plain,
heap_heap_ref_a(alloc_a(x)) = aa_a_Heap_Heap_ref_a(ref_a2,x),
inference(symmetry,[status(thm)],[28]) ).
tff(30,plain,
heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h) = heap_effect_ref_a(aa_a_Heap_Heap_ref_a(ref_a2,x),h),
inference(monotonicity,[status(thm)],[29]) ).
tff(31,plain,
aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),h2) = aa_hea8135729668157506370a_bool(heap_effect_ref_a(aa_a_Heap_Heap_ref_a(ref_a2,x),h),h2),
inference(monotonicity,[status(thm)],[30]) ).
tff(32,plain,
aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),h2),r) = aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(aa_a_Heap_Heap_ref_a(ref_a2,x),h),h2),r),
inference(monotonicity,[status(thm)],[31]) ).
tff(33,plain,
( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),h2),r))
<=> pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(aa_a_Heap_Heap_ref_a(ref_a2,x),h),h2),r)) ),
inference(monotonicity,[status(thm)],[32]) ).
tff(34,plain,
( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(aa_a_Heap_Heap_ref_a(ref_a2,x),h),h2),r))
<=> pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),h2),r)) ),
inference(symmetry,[status(thm)],[33]) ).
tff(35,plain,
( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(aa_a_Heap_Heap_ref_a(ref_a2,x),h),h2),r))
<=> pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(aa_a_Heap_Heap_ref_a(ref_a2,x),h),h2),r)) ),
inference(rewrite,[status(thm)],[]) ).
tff(36,axiom,
pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(aa_a_Heap_Heap_ref_a(ref_a2,x),h),h2),r)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_1_assms) ).
tff(37,plain,
pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(aa_a_Heap_Heap_ref_a(ref_a2,x),h),h2),r)),
inference(modus_ponens,[status(thm)],[36,35]) ).
tff(38,plain,
pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),h2),r)),
inference(modus_ponens,[status(thm)],[37,34]) ).
tff(39,plain,
^ [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
refl(( ( ( A = B )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) )
<=> ( ( A = B )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) ) )),
inference(bind,[status(th)],[]) ).
tff(40,plain,
( ! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( A = B )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) )
<=> ! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( A = B )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) ) ),
inference(quant_intro,[status(thm)],[39]) ).
tff(41,plain,
( ! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( A = B )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) )
<=> ! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( A = B )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(42,plain,
^ [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
trans(monotonicity(rewrite(( ( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
=> ( A = B ) )
<=> ( ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ( A = B ) ) )),
( ( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A))
=> ( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
=> ( A = B ) ) )
<=> ( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A))
=> ( ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ( A = B ) ) ) )),
rewrite(( ( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A))
=> ( ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ( A = B ) ) )
<=> ( ( A = B )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) ) )),
( ( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A))
=> ( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
=> ( A = B ) ) )
<=> ( ( A = B )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) ) )),
inference(bind,[status(th)],[]) ).
tff(43,plain,
( ! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A))
=> ( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
=> ( A = B ) ) )
<=> ! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( A = B )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) ) ),
inference(quant_intro,[status(thm)],[42]) ).
tff(44,axiom,
! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A))
=> ( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
=> ( A = B ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_184_effect__deterministic_I1_J) ).
tff(45,plain,
! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( A = B )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) ),
inference(modus_ponens,[status(thm)],[44,43]) ).
tff(46,plain,
! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( A = B )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) ),
inference(modus_ponens,[status(thm)],[45,41]) ).
tff(47,plain,
! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( A = B )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) ),
inference(skolemize,[status(sab)],[46]) ).
tff(48,plain,
! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( A = B )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) ),
inference(modus_ponens,[status(thm)],[47,40]) ).
tff(49,plain,
( ( ~ ! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( A = B )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) )
| ( r = aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),h2),r))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)))) )
<=> ( ~ ! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( A = B )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) )
| ( r = aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),h2),r))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)))) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(50,plain,
( ( ( r = aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),h2),r)) )
<=> ( ( r = aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),h2),r))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)))) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(51,plain,
( ( ~ ! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( A = B )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) )
| ( r = aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),h2),r)) )
<=> ( ~ ! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( A = B )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) )
| ( r = aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),h2),r))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)))) ) ),
inference(monotonicity,[status(thm)],[50]) ).
tff(52,plain,
( ( ~ ! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( A = B )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) )
| ( r = aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),h2),r)) )
<=> ( ~ ! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( A = B )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) )
| ( r = aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),h2),r))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)))) ) ),
inference(transitivity,[status(thm)],[51,49]) ).
tff(53,plain,
( ~ ! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( A = B )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) )
| ( r = aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),h2),r)) ),
inference(quant_inst,[status(thm)],[]) ).
tff(54,plain,
( ~ ! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( A = B )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) )
| ( r = aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),h2),r))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)))) ),
inference(modus_ponens,[status(thm)],[53,52]) ).
tff(55,plain,
r = aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)),
inference(unit_resolution,[status(thm)],[54,48,38,19]) ).
tff(56,plain,
^ [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
refl(( ( ( H2 = H3 )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) )
<=> ( ( H2 = H3 )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) ) )),
inference(bind,[status(th)],[]) ).
tff(57,plain,
( ! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( H2 = H3 )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) )
<=> ! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( H2 = H3 )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) ) ),
inference(quant_intro,[status(thm)],[56]) ).
tff(58,plain,
( ! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( H2 = H3 )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) )
<=> ! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( H2 = H3 )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(59,plain,
^ [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
trans(monotonicity(rewrite(( ( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
=> ( H2 = H3 ) )
<=> ( ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ( H2 = H3 ) ) )),
( ( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A))
=> ( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
=> ( H2 = H3 ) ) )
<=> ( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A))
=> ( ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ( H2 = H3 ) ) ) )),
rewrite(( ( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A))
=> ( ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ( H2 = H3 ) ) )
<=> ( ( H2 = H3 )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) ) )),
( ( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A))
=> ( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
=> ( H2 = H3 ) ) )
<=> ( ( H2 = H3 )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) ) )),
inference(bind,[status(th)],[]) ).
tff(60,plain,
( ! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A))
=> ( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
=> ( H2 = H3 ) ) )
<=> ! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( H2 = H3 )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) ) ),
inference(quant_intro,[status(thm)],[59]) ).
tff(61,axiom,
! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A))
=> ( pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
=> ( H2 = H3 ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_183_effect__deterministic_I2_J) ).
tff(62,plain,
! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( H2 = H3 )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) ),
inference(modus_ponens,[status(thm)],[61,60]) ).
tff(63,plain,
! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( H2 = H3 )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) ),
inference(modus_ponens,[status(thm)],[62,58]) ).
tff(64,plain,
! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( H2 = H3 )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) ),
inference(skolemize,[status(sab)],[63]) ).
tff(65,plain,
! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( H2 = H3 )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) ),
inference(modus_ponens,[status(thm)],[64,57]) ).
tff(66,plain,
( ( ~ ! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( H2 = H3 )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) )
| ( h2 = aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),h2),r))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)))) )
<=> ( ~ ! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( H2 = H3 )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) )
| ( h2 = aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),h2),r))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)))) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(67,plain,
( ( ( h2 = aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),h2),r)) )
<=> ( ( h2 = aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),h2),r))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)))) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(68,plain,
( ( ~ ! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( H2 = H3 )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) )
| ( h2 = aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),h2),r)) )
<=> ( ~ ! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( H2 = H3 )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) )
| ( h2 = aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),h2),r))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)))) ) ),
inference(monotonicity,[status(thm)],[67]) ).
tff(69,plain,
( ( ~ ! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( H2 = H3 )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) )
| ( h2 = aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),h2),r)) )
<=> ( ~ ! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( H2 = H3 )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) )
| ( h2 = aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),h2),r))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)))) ) ),
inference(transitivity,[status(thm)],[68,66]) ).
tff(70,plain,
( ~ ! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( H2 = H3 )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) )
| ( h2 = aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),h2),r)) ),
inference(quant_inst,[status(thm)],[]) ).
tff(71,plain,
( ~ ! [F: heap_Heap_ref_a,H: heap_e7401611519738050253t_unit,H2: heap_e7401611519738050253t_unit,A: ref_a,H3: heap_e7401611519738050253t_unit,B: ref_a] :
( ( H2 = H3 )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H3),B))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(F,H),H2),A)) )
| ( h2 = aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),h2),r))
| ~ pp(aa_ref_a_bool(aa_hea8135729668157506370a_bool(heap_effect_ref_a(heap_heap_ref_a(alloc_a(x)),h),aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h))),aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)))) ),
inference(modus_ponens,[status(thm)],[70,69]) ).
tff(72,plain,
h2 = aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)),
inference(unit_resolution,[status(thm)],[71,65,38,19]) ).
tff(73,plain,
( ( thesis
| ( h2 != aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
| ( r != aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) ) )
<=> ( thesis
| ( h2 != aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
| ( r != aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) ) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(74,plain,
( ( ( r = aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
=> ( thesis
| ( h2 != aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) ) ) )
<=> ( thesis
| ( h2 != aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
| ( r != aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) ) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(75,plain,
( ( ( h2 = aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
=> thesis )
<=> ( thesis
| ( h2 != aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) ) ) ),
inference(rewrite,[status(thm)],[]) ).
tff(76,plain,
( ( ( r = aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
=> ( ( h2 = aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
=> thesis ) )
<=> ( ( r = aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
=> ( thesis
| ( h2 != aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) ) ) ) ),
inference(monotonicity,[status(thm)],[75]) ).
tff(77,plain,
( ( ( r = aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
=> ( ( h2 = aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
=> thesis ) )
<=> ( thesis
| ( h2 != aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
| ( r != aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) ) ) ),
inference(transitivity,[status(thm)],[76,74]) ).
tff(78,axiom,
( ( r = aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
=> ( ( h2 = aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
=> thesis ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fact_0_that) ).
tff(79,plain,
( thesis
| ( h2 != aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
| ( r != aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) ) ),
inference(modus_ponens,[status(thm)],[78,77]) ).
tff(80,plain,
( thesis
| ( h2 != aa_Pro8575920914306358506t_unit(produc1126150082675451753t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) )
| ( r != aa_Pro7711270743135521984_ref_a(produc473321116828791851t_unit,aa_hea1409956391221964662t_unit(alloc_a(x),h)) ) ),
inference(modus_ponens,[status(thm)],[79,73]) ).
tff(81,plain,
$false,
inference(unit_resolution,[status(thm)],[80,72,55,3]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.12 % Problem : ITP206_1 : TPTP v9.0.0. Released v8.0.0.
% 0.04/0.12 % Command : run_E %s %d THM
% 0.11/0.32 % Computer : n007.cluster.edu
% 0.11/0.32 % Model : x86_64 x86_64
% 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.32 % Memory : 8042.1875MB
% 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.32 % CPULimit : 300
% 0.11/0.32 % WCLimit : 300
% 0.11/0.32 % DateTime : Thu Jun 19 18:31:50 EDT 2025
% 0.11/0.33 % CPUTime :
% 6.02/6.24 % SZS status Theorem
% 6.02/6.24 % SZS output start Proof
% See solution above
% 6.44/6.65 % E exiting
%------------------------------------------------------------------------------