%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP070^1 : TPTP v9.2.0. Released v7.5.0.
% Transfm : none
% Format : tptp:raw
% Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% Computer : n005.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 : Thu Oct 9 01:46:52 PM UTC 2025
% Result : Theorem 1.08s 1.29s
% Output : Proof 1.08s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : ITP070^1 : TPTP v9.2.0. Released v7.5.0.
% 0.07/0.13 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.12/0.34 % Computer : n005.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Oct 8 18:35:08 EDT 2025
% 0.12/0.35 % CPUTime :
% 1.08/1.29 % SZS status Theorem
% 1.08/1.29 % Mode: mode507:USE_SINE=true:SINE_TOLERANCE=3.0:SINE_GENERALITY_THRESHOLD=0:SINE_RANK_LIMIT=1.:SINE_DEPTH=1
% 1.08/1.29 % Inferences: 39
% 1.08/1.29 % SZS output start Proof
% 1.08/1.29 thf(ty_a, type, a : $tType).
% 1.08/1.29 thf(ty_multiset_a, type, multiset_a : $tType).
% 1.08/1.29 thf(ty_tree_a, type, tree_a : $tType).
% 1.08/1.29 thf(ty_l2, type, l2 : tree_a).
% 1.08/1.29 thf(ty_t_a, type, t_a : (a>tree_a>tree_a>tree_a)).
% 1.08/1.29 thf(ty_v, type, v : a).
% 1.08/1.29 thf(ty_multiset_a2, type, multiset_a2 : (tree_a>multiset_a)).
% 1.08/1.29 thf(ty_v2, type, v2 : a).
% 1.08/1.29 thf(ty_heapIm1091024090Down_a, type, heapIm1091024090Down_a : (tree_a>tree_a)).
% 1.08/1.29 thf(ty_r1, type, r1 : tree_a).
% 1.08/1.29 thf(ty_val_a, type, val_a : (tree_a>a)).
% 1.08/1.29 thf(ty_ord_less_eq_a, type, ord_less_eq_a : (a>a>$o)).
% 1.08/1.29 thf(ty_r2, type, r2 : tree_a).
% 1.08/1.29 thf(ty_v1, type, v1 : a).
% 1.08/1.29 thf(ty_l1, type, l1 : tree_a).
% 1.08/1.29 thf(ty_heapIm1140443833left_a, type, heapIm1140443833left_a : (tree_a>tree_a)).
% 1.08/1.29 thf(ty_heapIm1257206334ight_a, type, heapIm1257206334ight_a : (tree_a>tree_a)).
% 1.08/1.29 thf(sP1,plain,sP1 <=> ((ord_less_eq_a @ (val_a @ (((t_a @ v2) @ l2) @ r2))) @ (val_a @ (((t_a @ v1) @ l1) @ r1))),introduced(definition,[new_symbols(definition,[sP1])])).
% 1.08/1.29 thf(conj_0,conjecture,((multiset_a2 @ (heapIm1091024090Down_a @ (((t_a @ v) @ (((t_a @ v1) @ l1) @ r1)) @ (((t_a @ v2) @ l2) @ r2)))) = (multiset_a2 @ (((t_a @ v) @ (((t_a @ v1) @ l1) @ r1)) @ (((t_a @ v2) @ l2) @ r2))))).
% 1.08/1.29 thf(h0,negated_conjecture,(~(((multiset_a2 @ (heapIm1091024090Down_a @ (((t_a @ v) @ (((t_a @ v1) @ l1) @ r1)) @ (((t_a @ v2) @ l2) @ r2)))) = (multiset_a2 @ (((t_a @ v) @ (((t_a @ v1) @ l1) @ r1)) @ (((t_a @ v2) @ l2) @ r2)))))),inference(assume_negation,[status(cth)],[conj_0])).
% 1.08/1.29 thf(h1,assumption,(~(sP1)),introduced(assumption,[])).
% 1.08/1.29 thf(h2,assumption,((~(((ord_less_eq_a @ (val_a @ (((t_a @ v1) @ l1) @ r1))) @ v))) => ((multiset_a2 @ (heapIm1091024090Down_a @ (((t_a @ v) @ (heapIm1140443833left_a @ (((t_a @ v1) @ l1) @ r1))) @ (heapIm1257206334ight_a @ (((t_a @ v1) @ l1) @ r1))))) = (multiset_a2 @ (((t_a @ v) @ (heapIm1140443833left_a @ (((t_a @ v1) @ l1) @ r1))) @ (heapIm1257206334ight_a @ (((t_a @ v1) @ l1) @ r1)))))),introduced(assumption,[])).
% 1.08/1.29 thf(h3,assumption,sP1,introduced(assumption,[])).
% 1.08/1.29 thf(h4,assumption,((~(((ord_less_eq_a @ (val_a @ (((t_a @ v2) @ l2) @ r2))) @ v))) => ((multiset_a2 @ (heapIm1091024090Down_a @ (((t_a @ v) @ (heapIm1140443833left_a @ (((t_a @ v2) @ l2) @ r2))) @ (heapIm1257206334ight_a @ (((t_a @ v2) @ l2) @ r2))))) = (multiset_a2 @ (((t_a @ v) @ (heapIm1140443833left_a @ (((t_a @ v2) @ l2) @ r2))) @ (heapIm1257206334ight_a @ (((t_a @ v2) @ l2) @ r2)))))),introduced(assumption,[])).
% 1.08/1.29 thf(1,plain,$false,inference(tab_conflict,[status(thm),assumptions([h3,h1,h0])],[h3,h1])).
% 1.08/1.29 thf(h5,assumption,((ord_less_eq_a @ (val_a @ (((t_a @ v2) @ l2) @ r2))) @ v),introduced(assumption,[])).
% 1.08/1.29 thf(h6,assumption,((multiset_a2 @ (heapIm1091024090Down_a @ (((t_a @ v) @ (heapIm1140443833left_a @ (((t_a @ v2) @ l2) @ r2))) @ (heapIm1257206334ight_a @ (((t_a @ v2) @ l2) @ r2))))) = (multiset_a2 @ (((t_a @ v) @ (heapIm1140443833left_a @ (((t_a @ v2) @ l2) @ r2))) @ (heapIm1257206334ight_a @ (((t_a @ v2) @ l2) @ r2))))),introduced(assumption,[])).
% 1.08/1.29 thf(pax22, axiom, (p22=>![X14:a, X15:tree_a, X16:tree_a]:(fval_a @ (ft_a @ X14 @ X15 @ X16))=(X14)), file('<stdin>', pax22)).
% 1.08/1.29 thf(pax1, axiom, (p1=>ford_less_eq_a @ fv2 @ fv1), file('<stdin>', pax1)).
% 1.08/1.29 thf(nax3, axiom, (p3<=ford_less_eq_a @ (fval_a @ (ft_a @ fv2 @ fl2 @ fr2)) @ (fval_a @ (ft_a @ fv1 @ fl1 @ fr1))), file('<stdin>', nax3)).
% 1.08/1.29 thf(ax8, axiom, p22, file('<stdin>', ax8)).
% 1.08/1.29 thf(ax29, axiom, p1, file('<stdin>', ax29)).
% 1.08/1.29 thf(ax26, axiom, ~(p3), file('<stdin>', ax26)).
% 1.08/1.29 thf(c_0_6, plain, ![X127:a, X128:tree_a, X129:tree_a]:(~p22|(fval_a @ (ft_a @ X127 @ X128 @ X129))=(X127)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax22])])])).
% 1.08/1.29 thf(c_0_7, plain, (~p1|ford_less_eq_a @ fv2 @ fv1), inference(fof_nnf,[status(thm)],[pax1])).
% 1.08/1.29 thf(c_0_8, plain, (~ford_less_eq_a @ (fval_a @ (ft_a @ fv2 @ fl2 @ fr2)) @ (fval_a @ (ft_a @ fv1 @ fl1 @ fr1))|p3), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax3])])).
% 1.08/1.29 thf(c_0_9, plain, ![X3:tree_a, X2:tree_a, X1:a]:((fval_a @ (ft_a @ X1 @ X2 @ X3))=(X1)|~p22), inference(split_conjunct,[status(thm)],[c_0_6])).
% 1.08/1.29 thf(c_0_10, plain, p22, inference(split_conjunct,[status(thm)],[ax8])).
% 1.08/1.29 thf(c_0_11, plain, (ford_less_eq_a @ fv2 @ fv1|~p1), inference(split_conjunct,[status(thm)],[c_0_7])).
% 1.08/1.29 thf(c_0_12, plain, p1, inference(split_conjunct,[status(thm)],[ax29])).
% 1.08/1.29 thf(c_0_13, plain, ~p3, inference(fof_simplification,[status(thm)],[ax26])).
% 1.08/1.29 thf(c_0_14, plain, (p3|~ford_less_eq_a @ (fval_a @ (ft_a @ fv2 @ fl2 @ fr2)) @ (fval_a @ (ft_a @ fv1 @ fl1 @ fr1))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 1.08/1.29 thf(c_0_15, plain, ![X3:tree_a, X2:tree_a, X1:a]:(fval_a @ (ft_a @ X1 @ X2 @ X3))=(X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_9, c_0_10])])).
% 1.08/1.29 thf(c_0_16, plain, ford_less_eq_a @ fv2 @ fv1, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_11, c_0_12])])).
% 1.08/1.29 thf(c_0_17, plain, ~p3, inference(split_conjunct,[status(thm)],[c_0_13])).
% 1.08/1.29 thf(c_0_18, plain, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_14, c_0_15]), c_0_15]), c_0_16])]), c_0_17]), ['proof']).
% 1.08/1.29 thf(2,plain,$false,inference(eprover,[status(thm),assumptions([h5,h4,h1,h0])],[])).
% 1.08/1.29 thf(pax22, axiom, (p22=>![X18:a, X19:tree_a, X20:tree_a]:(fval_a @ (ft_a @ X18 @ X19 @ X20))=(X18)), file('<stdin>', pax22)).
% 1.08/1.29 thf(pax1, axiom, (p1=>ford_less_eq_a @ fv2 @ fv1), file('<stdin>', pax1)).
% 1.08/1.29 thf(nax3, axiom, (p3<=ford_less_eq_a @ (fval_a @ (ft_a @ fv2 @ fl2 @ fr2)) @ (fval_a @ (ft_a @ fv1 @ fl1 @ fr1))), file('<stdin>', nax3)).
% 1.08/1.29 thf(ax18, axiom, p22, file('<stdin>', ax18)).
% 1.08/1.29 thf(ax39, axiom, p1, file('<stdin>', ax39)).
% 1.08/1.29 thf(ax36, axiom, ~(p3), file('<stdin>', ax36)).
% 1.08/1.29 thf(c_0_6, plain, ![X143:a, X144:tree_a, X145:tree_a]:(~p22|(fval_a @ (ft_a @ X143 @ X144 @ X145))=(X143)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax22])])])).
% 1.08/1.29 thf(c_0_7, plain, (~p1|ford_less_eq_a @ fv2 @ fv1), inference(fof_nnf,[status(thm)],[pax1])).
% 1.08/1.29 thf(c_0_8, plain, (~ford_less_eq_a @ (fval_a @ (ft_a @ fv2 @ fl2 @ fr2)) @ (fval_a @ (ft_a @ fv1 @ fl1 @ fr1))|p3), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax3])])).
% 1.08/1.29 thf(c_0_9, plain, ![X1:tree_a, X2:tree_a, X5:a]:((fval_a @ (ft_a @ X5 @ X1 @ X2))=(X5)|~p22), inference(split_conjunct,[status(thm)],[c_0_6])).
% 1.08/1.29 thf(c_0_10, plain, p22, inference(split_conjunct,[status(thm)],[ax18])).
% 1.08/1.29 thf(c_0_11, plain, (ford_less_eq_a @ fv2 @ fv1|~p1), inference(split_conjunct,[status(thm)],[c_0_7])).
% 1.08/1.29 thf(c_0_12, plain, p1, inference(split_conjunct,[status(thm)],[ax39])).
% 1.08/1.29 thf(c_0_13, plain, ~p3, inference(fof_simplification,[status(thm)],[ax36])).
% 1.08/1.29 thf(c_0_14, plain, (p3|~ford_less_eq_a @ (fval_a @ (ft_a @ fv2 @ fl2 @ fr2)) @ (fval_a @ (ft_a @ fv1 @ fl1 @ fr1))), inference(split_conjunct,[status(thm)],[c_0_8])).
% 1.08/1.29 thf(c_0_15, plain, ![X1:tree_a, X2:tree_a, X5:a]:(fval_a @ (ft_a @ X5 @ X1 @ X2))=(X5), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_9, c_0_10])])).
% 1.08/1.29 thf(c_0_16, plain, ford_less_eq_a @ fv2 @ fv1, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_11, c_0_12])])).
% 1.08/1.29 thf(c_0_17, plain, ~p3, inference(split_conjunct,[status(thm)],[c_0_13])).
% 1.08/1.29 thf(c_0_18, plain, ($false), inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_14, c_0_15]), c_0_15]), c_0_16])]), c_0_17]), ['proof']).
% 1.08/1.29 thf(3,plain,$false,inference(eprover,[status(thm),assumptions([h6,h4,h1,h0])],[])).
% 1.08/1.29 thf(4,plain,$false,inference(tab_imp,[status(thm),assumptions([h4,h1,h0]),tab_imp(discharge,[h5]),tab_imp(discharge,[h6])],[h4,2,3,h5,h6])).
% 1.08/1.29 thf(fact_2__C5__2_Ohyps_C_I2_J,axiom,((~(sP1)) => ((~(((ord_less_eq_a @ (val_a @ (((t_a @ v2) @ l2) @ r2))) @ v))) => ((multiset_a2 @ (heapIm1091024090Down_a @ (((t_a @ v) @ (heapIm1140443833left_a @ (((t_a @ v2) @ l2) @ r2))) @ (heapIm1257206334ight_a @ (((t_a @ v2) @ l2) @ r2))))) = (multiset_a2 @ (((t_a @ v) @ (heapIm1140443833left_a @ (((t_a @ v2) @ l2) @ r2))) @ (heapIm1257206334ight_a @ (((t_a @ v2) @ l2) @ r2)))))))).
% 1.08/1.29 thf(5,plain,$false,inference(tab_imp,[status(thm),assumptions([h1,h0]),tab_imp(discharge,[h3]),tab_imp(discharge,[h4])],[fact_2__C5__2_Ohyps_C_I2_J,1,4,h3,h4])).
% 1.08/1.29 thf(h7,assumption,((ord_less_eq_a @ (val_a @ (((t_a @ v1) @ l1) @ r1))) @ v),introduced(assumption,[])).
% 1.08/1.29 thf(h8,assumption,((multiset_a2 @ (heapIm1091024090Down_a @ (((t_a @ v) @ (heapIm1140443833left_a @ (((t_a @ v1) @ l1) @ r1))) @ (heapIm1257206334ight_a @ (((t_a @ v1) @ l1) @ r1))))) = (multiset_a2 @ (((t_a @ v) @ (heapIm1140443833left_a @ (((t_a @ v1) @ l1) @ r1))) @ (heapIm1257206334ight_a @ (((t_a @ v1) @ l1) @ r1))))),introduced(assumption,[])).
% 1.08/1.29 thf(pax23, axiom, (p23=>![X19:a, X20:tree_a, X21:tree_a, X22:a, X15:tree_a, X23:tree_a, X24:a]:~(((ford_less_eq_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ (fval_a @ (ft_a @ X22 @ X15 @ X23))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X22 @ X15 @ X23)) @ X24=>(fheapIm1091024090Down_a @ (ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=(ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X22 @ X15 @ X23)) @ X24)=>(fheapIm1091024090Down_a @ (ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=(ft_a @ (fval_a @ (ft_a @ X22 @ X15 @ X23)) @ (fheapIm1091024090Down_a @ (ft_a @ X24 @ (fheapIm1140443833left_a @ (ft_a @ X22 @ X15 @ X23)) @ (fheapIm1257206334ight_a @ (ft_a @ X22 @ X15 @ X23)))) @ (ft_a @ X19 @ X20 @ X21)))))))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ (fval_a @ (ft_a @ X22 @ X15 @ X23)))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ X24=>(fheapIm1091024090Down_a @ (ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=(ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ X24)=>(fheapIm1091024090Down_a @ (ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=(ft_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ (ft_a @ X22 @ X15 @ X23) @ (fheapIm1091024090Down_a @ (ft_a @ X24 @ (fheapIm1140443833left_a @ (ft_a @ X19 @ X20 @ X21)) @ (fheapIm1257206334ight_a @ (ft_a @ X19 @ X20 @ X21)))))))))))))), file('<stdin>', pax23)).
% 1.08/1.29 thf(ax8, axiom, (p33|~(p40)), file('<stdin>', ax8)).
% 1.08/1.29 thf(ax16, axiom, ~(p33), file('<stdin>', ax16)).
% 1.08/1.29 thf(pax22, axiom, (p22=>![X19:a, X20:tree_a, X21:tree_a]:(fval_a @ (ft_a @ X19 @ X20 @ X21))=(X19)), file('<stdin>', pax22)).
% 1.08/1.29 thf(nax40, axiom, (p40<=(fheapIm1091024090Down_a @ (ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)))=(ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2))), file('<stdin>', nax40)).
% 1.08/1.29 thf(ax25, axiom, p23, file('<stdin>', ax25)).
% 1.08/1.29 thf(ax26, axiom, p22, file('<stdin>', ax26)).
% 1.08/1.29 thf(pax2, axiom, (p2=>ford_less_eq_a @ fv1 @ fv), file('<stdin>', pax2)).
% 1.08/1.29 thf(pax1, axiom, (p1=>ford_less_eq_a @ fv2 @ fv1), file('<stdin>', pax1)).
% 1.08/1.29 thf(ax46, axiom, p2, file('<stdin>', ax46)).
% 1.08/1.29 thf(ax47, axiom, p1, file('<stdin>', ax47)).
% 1.08/1.29 thf(c_0_11, plain, (epred1_0<=>![X19:a, X20:tree_a, X21:tree_a, X22:a, X15:tree_a, X23:tree_a, X24:a]:~(((ford_less_eq_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ (fval_a @ (ft_a @ X22 @ X15 @ X23))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X22 @ X15 @ X23)) @ X24=>(fheapIm1091024090Down_a @ (ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=(ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X22 @ X15 @ X23)) @ X24)=>(fheapIm1091024090Down_a @ (ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=(ft_a @ (fval_a @ (ft_a @ X22 @ X15 @ X23)) @ (fheapIm1091024090Down_a @ (ft_a @ X24 @ (fheapIm1140443833left_a @ (ft_a @ X22 @ X15 @ X23)) @ (fheapIm1257206334ight_a @ (ft_a @ X22 @ X15 @ X23)))) @ (ft_a @ X19 @ X20 @ X21)))))))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ (fval_a @ (ft_a @ X22 @ X15 @ X23)))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ X24=>(fheapIm1091024090Down_a @ (ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=(ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ X24)=>(fheapIm1091024090Down_a @ (ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=(ft_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ (ft_a @ X22 @ X15 @ X23) @ (fheapIm1091024090Down_a @ (ft_a @ X24 @ (fheapIm1140443833left_a @ (ft_a @ X19 @ X20 @ X21)) @ (fheapIm1257206334ight_a @ (ft_a @ X19 @ X20 @ X21)))))))))))))), introduced(definition)).
% 1.08/1.29 thf(c_0_12, axiom, (p23=>epred1_0), inference(apply_def,[status(thm)],[pax23, c_0_11])).
% 1.08/1.29 thf(c_0_13, plain, (p33|~p40), inference(fof_simplification,[status(thm)],[ax8])).
% 1.08/1.29 thf(c_0_14, plain, ~p33, inference(fof_simplification,[status(thm)],[ax16])).
% 1.08/1.29 thf(c_0_15, plain, (epred1_0=>![X19:a, X20:tree_a, X21:tree_a, X22:a, X15:tree_a, X23:tree_a, X24:a]:~(((ford_less_eq_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ (fval_a @ (ft_a @ X22 @ X15 @ X23))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X22 @ X15 @ X23)) @ X24=>(fheapIm1091024090Down_a @ (ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=(ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X22 @ X15 @ X23)) @ X24)=>(fheapIm1091024090Down_a @ (ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=(ft_a @ (fval_a @ (ft_a @ X22 @ X15 @ X23)) @ (fheapIm1091024090Down_a @ (ft_a @ X24 @ (fheapIm1140443833left_a @ (ft_a @ X22 @ X15 @ X23)) @ (fheapIm1257206334ight_a @ (ft_a @ X22 @ X15 @ X23)))) @ (ft_a @ X19 @ X20 @ X21)))))))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ (fval_a @ (ft_a @ X22 @ X15 @ X23)))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ X24=>(fheapIm1091024090Down_a @ (ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=(ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ X24)=>(fheapIm1091024090Down_a @ (ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=(ft_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ (ft_a @ X22 @ X15 @ X23) @ (fheapIm1091024090Down_a @ (ft_a @ X24 @ (fheapIm1140443833left_a @ (ft_a @ X19 @ X20 @ X21)) @ (fheapIm1257206334ight_a @ (ft_a @ X19 @ X20 @ X21)))))))))))))), inference(split_equiv,[status(thm)],[c_0_11])).
% 1.08/1.29 thf(c_0_16, plain, (~p23|epred1_0), inference(fof_nnf,[status(thm)],[c_0_12])).
% 1.08/1.29 thf(c_0_17, plain, ![X164:a, X165:tree_a, X166:tree_a]:(~p22|(fval_a @ (ft_a @ X164 @ X165 @ X166))=(X164)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax22])])])).
% 1.08/1.29 thf(c_0_18, plain, ((fheapIm1091024090Down_a @ (ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)))!=(ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2))|p40), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax40])])).
% 1.08/1.29 thf(c_0_19, plain, (p33|~p40), inference(split_conjunct,[status(thm)],[c_0_13])).
% 1.08/1.29 thf(c_0_20, plain, ~p33, inference(split_conjunct,[status(thm)],[c_0_14])).
% 1.08/1.29 thf(c_0_21, plain, ![X262:a, X263:tree_a, X264:tree_a, X265:a, X266:tree_a, X267:tree_a, X268:a]:(((~ford_less_eq_a @ (fval_a @ (ft_a @ X265 @ X266 @ X267)) @ X268|(fheapIm1091024090Down_a @ (ft_a @ X268 @ (ft_a @ X265 @ X266 @ X267) @ (ft_a @ X262 @ X263 @ X264)))=(ft_a @ X268 @ (ft_a @ X265 @ X266 @ X267) @ (ft_a @ X262 @ X263 @ X264))|~ford_less_eq_a @ (fval_a @ (ft_a @ X262 @ X263 @ X264)) @ (fval_a @ (ft_a @ X265 @ X266 @ X267))|~epred1_0)&(ford_less_eq_a @ (fval_a @ (ft_a @ X265 @ X266 @ X267)) @ X268|(fheapIm1091024090Down_a @ (ft_a @ X268 @ (ft_a @ X265 @ X266 @ X267) @ (ft_a @ X262 @ X263 @ X264)))=(ft_a @ (fval_a @ (ft_a @ X265 @ X266 @ X267)) @ (fheapIm1091024090Down_a @ (ft_a @ X268 @ (fheapIm1140443833left_a @ (ft_a @ X265 @ X266 @ X267)) @ (fheapIm1257206334ight_a @ (ft_a @ X265 @ X266 @ X267)))) @ (ft_a @ X262 @ X263 @ X264))|~ford_less_eq_a @ (fval_a @ (ft_a @ X262 @ X263 @ X264)) @ (fval_a @ (ft_a @ X265 @ X266 @ X267))|~epred1_0))&((~ford_less_eq_a @ (fval_a @ (ft_a @ X262 @ X263 @ X264)) @ X268|(fheapIm1091024090Down_a @ (ft_a @ X268 @ (ft_a @ X265 @ X266 @ X267) @ (ft_a @ X262 @ X263 @ X264)))=(ft_a @ X268 @ (ft_a @ X265 @ X266 @ X267) @ (ft_a @ X262 @ X263 @ X264))|ford_less_eq_a @ (fval_a @ (ft_a @ X262 @ X263 @ X264)) @ (fval_a @ (ft_a @ X265 @ X266 @ X267))|~epred1_0)&(ford_less_eq_a @ (fval_a @ (ft_a @ X262 @ X263 @ X264)) @ X268|(fheapIm1091024090Down_a @ (ft_a @ X268 @ (ft_a @ X265 @ X266 @ X267) @ (ft_a @ X262 @ X263 @ X264)))=(ft_a @ (fval_a @ (ft_a @ X262 @ X263 @ X264)) @ (ft_a @ X265 @ X266 @ X267) @ (fheapIm1091024090Down_a @ (ft_a @ X268 @ (fheapIm1140443833left_a @ (ft_a @ X262 @ X263 @ X264)) @ (fheapIm1257206334ight_a @ (ft_a @ X262 @ X263 @ X264)))))|ford_less_eq_a @ (fval_a @ (ft_a @ X262 @ X263 @ X264)) @ (fval_a @ (ft_a @ X265 @ X266 @ X267))|~epred1_0))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_15])])])])])).
% 1.08/1.29 thf(c_0_22, plain, (epred1_0|~p23), inference(split_conjunct,[status(thm)],[c_0_16])).
% 1.08/1.29 thf(c_0_23, plain, p23, inference(split_conjunct,[status(thm)],[ax25])).
% 1.08/1.29 thf(c_0_24, plain, ![X2:tree_a, X3:tree_a, X6:a]:((fval_a @ (ft_a @ X6 @ X2 @ X3))=(X6)|~p22), inference(split_conjunct,[status(thm)],[c_0_17])).
% 1.08/1.29 thf(c_0_25, plain, p22, inference(split_conjunct,[status(thm)],[ax26])).
% 1.08/1.29 thf(c_0_26, plain, (~p2|ford_less_eq_a @ fv1 @ fv), inference(fof_nnf,[status(thm)],[pax2])).
% 1.08/1.29 thf(c_0_27, plain, (~p1|ford_less_eq_a @ fv2 @ fv1), inference(fof_nnf,[status(thm)],[pax1])).
% 1.08/1.29 thf(c_0_28, plain, (p40|(fheapIm1091024090Down_a @ (ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)))!=(ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2))), inference(split_conjunct,[status(thm)],[c_0_18])).
% 1.08/1.29 thf(c_0_29, plain, ~p40, inference(sr,[status(thm)],[c_0_19, c_0_20])).
% 1.08/1.29 thf(c_0_30, plain, ![X2:tree_a, X12:a, X10:a, X8:tree_a, X7:tree_a, X6:a, X3:tree_a]:((fheapIm1091024090Down_a @ (ft_a @ X10 @ (ft_a @ X6 @ X2 @ X3) @ (ft_a @ X12 @ X7 @ X8)))=(ft_a @ X10 @ (ft_a @ X6 @ X2 @ X3) @ (ft_a @ X12 @ X7 @ X8))|~ford_less_eq_a @ (fval_a @ (ft_a @ X6 @ X2 @ X3)) @ X10|~ford_less_eq_a @ (fval_a @ (ft_a @ X12 @ X7 @ X8)) @ (fval_a @ (ft_a @ X6 @ X2 @ X3))|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_21])).
% 1.08/1.29 thf(c_0_31, plain, epred1_0, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_22, c_0_23])])).
% 1.08/1.29 thf(c_0_32, plain, ![X2:tree_a, X3:tree_a, X6:a]:(fval_a @ (ft_a @ X6 @ X2 @ X3))=(X6), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_24, c_0_25])])).
% 1.08/1.29 thf(c_0_33, plain, (ford_less_eq_a @ fv1 @ fv|~p2), inference(split_conjunct,[status(thm)],[c_0_26])).
% 1.08/1.29 thf(c_0_34, plain, p2, inference(split_conjunct,[status(thm)],[ax46])).
% 1.08/1.29 thf(c_0_35, plain, (ford_less_eq_a @ fv2 @ fv1|~p1), inference(split_conjunct,[status(thm)],[c_0_27])).
% 1.08/1.29 thf(c_0_36, plain, p1, inference(split_conjunct,[status(thm)],[ax47])).
% 1.08/1.29 thf(c_0_37, plain, (fheapIm1091024090Down_a @ (ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)))!=(ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)), inference(sr,[status(thm)],[c_0_28, c_0_29])).
% 1.08/1.29 thf(c_0_38, plain, ![X2:tree_a, X3:tree_a, X7:tree_a, X6:a, X8:tree_a, X12:a, X10:a]:((fheapIm1091024090Down_a @ (ft_a @ X6 @ (ft_a @ X10 @ X2 @ X3) @ (ft_a @ X12 @ X7 @ X8)))=(ft_a @ X6 @ (ft_a @ X10 @ X2 @ X3) @ (ft_a @ X12 @ X7 @ X8))|~ford_less_eq_a @ X10 @ X6|~ford_less_eq_a @ X12 @ X10), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_30, c_0_31]), c_0_32]), c_0_32]), c_0_32])])).
% 1.08/1.29 thf(c_0_39, plain, ford_less_eq_a @ fv1 @ fv, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_33, c_0_34])])).
% 1.08/1.29 thf(c_0_40, plain, ford_less_eq_a @ fv2 @ fv1, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_35, c_0_36])])).
% 1.08/1.29 thf(c_0_41, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_38]), c_0_39]), c_0_40])]), ['proof']).
% 1.08/1.29 thf(6,plain,$false,inference(eprover,[status(thm),assumptions([h3,h7,h2,h0])],[])).
% 1.08/1.29 thf(pax23, axiom, (p23=>![X19:a, X20:tree_a, X21:tree_a, X22:a, X15:tree_a, X23:tree_a, X24:a]:~(((ford_less_eq_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ (fval_a @ (ft_a @ X22 @ X15 @ X23))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X22 @ X15 @ X23)) @ X24=>(fheapIm1091024090Down_a @ (ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=(ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X22 @ X15 @ X23)) @ X24)=>(fheapIm1091024090Down_a @ (ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=(ft_a @ (fval_a @ (ft_a @ X22 @ X15 @ X23)) @ (fheapIm1091024090Down_a @ (ft_a @ X24 @ (fheapIm1140443833left_a @ (ft_a @ X22 @ X15 @ X23)) @ (fheapIm1257206334ight_a @ (ft_a @ X22 @ X15 @ X23)))) @ (ft_a @ X19 @ X20 @ X21)))))))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ (fval_a @ (ft_a @ X22 @ X15 @ X23)))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ X24=>(fheapIm1091024090Down_a @ (ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=(ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ X24)=>(fheapIm1091024090Down_a @ (ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=(ft_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ (ft_a @ X22 @ X15 @ X23) @ (fheapIm1091024090Down_a @ (ft_a @ X24 @ (fheapIm1140443833left_a @ (ft_a @ X19 @ X20 @ X21)) @ (fheapIm1257206334ight_a @ (ft_a @ X19 @ X20 @ X21)))))))))))))), file('<stdin>', pax23)).
% 1.08/1.29 thf(ax21, axiom, (p33|~(p40)), file('<stdin>', ax21)).
% 1.08/1.29 thf(ax29, axiom, ~(p33), file('<stdin>', ax29)).
% 1.08/1.29 thf(pax22, axiom, (p22=>![X19:a, X20:tree_a, X21:tree_a]:(fval_a @ (ft_a @ X19 @ X20 @ X21))=(X19)), file('<stdin>', pax22)).
% 1.08/1.29 thf(nax40, axiom, (p40<=(fheapIm1091024090Down_a @ (ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)))=(ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2))), file('<stdin>', nax40)).
% 1.08/1.29 thf(ax38, axiom, p23, file('<stdin>', ax38)).
% 1.08/1.29 thf(ax39, axiom, p22, file('<stdin>', ax39)).
% 1.08/1.29 thf(pax2, axiom, (p2=>ford_less_eq_a @ fv1 @ fv), file('<stdin>', pax2)).
% 1.08/1.29 thf(pax1, axiom, (p1=>ford_less_eq_a @ fv2 @ fv1), file('<stdin>', pax1)).
% 1.08/1.29 thf(ax59, axiom, p2, file('<stdin>', ax59)).
% 1.08/1.29 thf(ax60, axiom, p1, file('<stdin>', ax60)).
% 1.08/1.29 thf(c_0_11, plain, (epred1_0<=>![X19:a, X20:tree_a, X21:tree_a, X22:a, X15:tree_a, X23:tree_a, X24:a]:~(((ford_less_eq_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ (fval_a @ (ft_a @ X22 @ X15 @ X23))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X22 @ X15 @ X23)) @ X24=>(fheapIm1091024090Down_a @ (ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=(ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X22 @ X15 @ X23)) @ X24)=>(fheapIm1091024090Down_a @ (ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=(ft_a @ (fval_a @ (ft_a @ X22 @ X15 @ X23)) @ (fheapIm1091024090Down_a @ (ft_a @ X24 @ (fheapIm1140443833left_a @ (ft_a @ X22 @ X15 @ X23)) @ (fheapIm1257206334ight_a @ (ft_a @ X22 @ X15 @ X23)))) @ (ft_a @ X19 @ X20 @ X21)))))))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ (fval_a @ (ft_a @ X22 @ X15 @ X23)))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ X24=>(fheapIm1091024090Down_a @ (ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=(ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ X24)=>(fheapIm1091024090Down_a @ (ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=(ft_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ (ft_a @ X22 @ X15 @ X23) @ (fheapIm1091024090Down_a @ (ft_a @ X24 @ (fheapIm1140443833left_a @ (ft_a @ X19 @ X20 @ X21)) @ (fheapIm1257206334ight_a @ (ft_a @ X19 @ X20 @ X21)))))))))))))), introduced(definition)).
% 1.08/1.29 thf(c_0_12, axiom, (p23=>epred1_0), inference(apply_def,[status(thm)],[pax23, c_0_11])).
% 1.08/1.29 thf(c_0_13, plain, (p33|~p40), inference(fof_simplification,[status(thm)],[ax21])).
% 1.08/1.29 thf(c_0_14, plain, ~p33, inference(fof_simplification,[status(thm)],[ax29])).
% 1.08/1.29 thf(c_0_15, plain, (epred1_0=>![X19:a, X20:tree_a, X21:tree_a, X22:a, X15:tree_a, X23:tree_a, X24:a]:~(((ford_less_eq_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ (fval_a @ (ft_a @ X22 @ X15 @ X23))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X22 @ X15 @ X23)) @ X24=>(fheapIm1091024090Down_a @ (ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=(ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X22 @ X15 @ X23)) @ X24)=>(fheapIm1091024090Down_a @ (ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=(ft_a @ (fval_a @ (ft_a @ X22 @ X15 @ X23)) @ (fheapIm1091024090Down_a @ (ft_a @ X24 @ (fheapIm1140443833left_a @ (ft_a @ X22 @ X15 @ X23)) @ (fheapIm1257206334ight_a @ (ft_a @ X22 @ X15 @ X23)))) @ (ft_a @ X19 @ X20 @ X21)))))))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ (fval_a @ (ft_a @ X22 @ X15 @ X23)))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ X24=>(fheapIm1091024090Down_a @ (ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=(ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ X24)=>(fheapIm1091024090Down_a @ (ft_a @ X24 @ (ft_a @ X22 @ X15 @ X23) @ (ft_a @ X19 @ X20 @ X21)))=(ft_a @ (fval_a @ (ft_a @ X19 @ X20 @ X21)) @ (ft_a @ X22 @ X15 @ X23) @ (fheapIm1091024090Down_a @ (ft_a @ X24 @ (fheapIm1140443833left_a @ (ft_a @ X19 @ X20 @ X21)) @ (fheapIm1257206334ight_a @ (ft_a @ X19 @ X20 @ X21)))))))))))))), inference(split_equiv,[status(thm)],[c_0_11])).
% 1.08/1.29 thf(c_0_16, plain, (~p23|epred1_0), inference(fof_nnf,[status(thm)],[c_0_12])).
% 1.08/1.29 thf(c_0_17, plain, ![X164:a, X165:tree_a, X166:tree_a]:(~p22|(fval_a @ (ft_a @ X164 @ X165 @ X166))=(X164)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax22])])])).
% 1.08/1.29 thf(c_0_18, plain, ((fheapIm1091024090Down_a @ (ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)))!=(ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2))|p40), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax40])])).
% 1.08/1.29 thf(c_0_19, plain, (p33|~p40), inference(split_conjunct,[status(thm)],[c_0_13])).
% 1.08/1.29 thf(c_0_20, plain, ~p33, inference(split_conjunct,[status(thm)],[c_0_14])).
% 1.08/1.29 thf(c_0_21, plain, ![X262:a, X263:tree_a, X264:tree_a, X265:a, X266:tree_a, X267:tree_a, X268:a]:(((~ford_less_eq_a @ (fval_a @ (ft_a @ X265 @ X266 @ X267)) @ X268|(fheapIm1091024090Down_a @ (ft_a @ X268 @ (ft_a @ X265 @ X266 @ X267) @ (ft_a @ X262 @ X263 @ X264)))=(ft_a @ X268 @ (ft_a @ X265 @ X266 @ X267) @ (ft_a @ X262 @ X263 @ X264))|~ford_less_eq_a @ (fval_a @ (ft_a @ X262 @ X263 @ X264)) @ (fval_a @ (ft_a @ X265 @ X266 @ X267))|~epred1_0)&(ford_less_eq_a @ (fval_a @ (ft_a @ X265 @ X266 @ X267)) @ X268|(fheapIm1091024090Down_a @ (ft_a @ X268 @ (ft_a @ X265 @ X266 @ X267) @ (ft_a @ X262 @ X263 @ X264)))=(ft_a @ (fval_a @ (ft_a @ X265 @ X266 @ X267)) @ (fheapIm1091024090Down_a @ (ft_a @ X268 @ (fheapIm1140443833left_a @ (ft_a @ X265 @ X266 @ X267)) @ (fheapIm1257206334ight_a @ (ft_a @ X265 @ X266 @ X267)))) @ (ft_a @ X262 @ X263 @ X264))|~ford_less_eq_a @ (fval_a @ (ft_a @ X262 @ X263 @ X264)) @ (fval_a @ (ft_a @ X265 @ X266 @ X267))|~epred1_0))&((~ford_less_eq_a @ (fval_a @ (ft_a @ X262 @ X263 @ X264)) @ X268|(fheapIm1091024090Down_a @ (ft_a @ X268 @ (ft_a @ X265 @ X266 @ X267) @ (ft_a @ X262 @ X263 @ X264)))=(ft_a @ X268 @ (ft_a @ X265 @ X266 @ X267) @ (ft_a @ X262 @ X263 @ X264))|ford_less_eq_a @ (fval_a @ (ft_a @ X262 @ X263 @ X264)) @ (fval_a @ (ft_a @ X265 @ X266 @ X267))|~epred1_0)&(ford_less_eq_a @ (fval_a @ (ft_a @ X262 @ X263 @ X264)) @ X268|(fheapIm1091024090Down_a @ (ft_a @ X268 @ (ft_a @ X265 @ X266 @ X267) @ (ft_a @ X262 @ X263 @ X264)))=(ft_a @ (fval_a @ (ft_a @ X262 @ X263 @ X264)) @ (ft_a @ X265 @ X266 @ X267) @ (fheapIm1091024090Down_a @ (ft_a @ X268 @ (fheapIm1140443833left_a @ (ft_a @ X262 @ X263 @ X264)) @ (fheapIm1257206334ight_a @ (ft_a @ X262 @ X263 @ X264)))))|ford_less_eq_a @ (fval_a @ (ft_a @ X262 @ X263 @ X264)) @ (fval_a @ (ft_a @ X265 @ X266 @ X267))|~epred1_0))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_15])])])])])).
% 1.08/1.29 thf(c_0_22, plain, (epred1_0|~p23), inference(split_conjunct,[status(thm)],[c_0_16])).
% 1.08/1.29 thf(c_0_23, plain, p23, inference(split_conjunct,[status(thm)],[ax38])).
% 1.08/1.29 thf(c_0_24, plain, ![X2:tree_a, X3:tree_a, X6:a]:((fval_a @ (ft_a @ X6 @ X2 @ X3))=(X6)|~p22), inference(split_conjunct,[status(thm)],[c_0_17])).
% 1.08/1.29 thf(c_0_25, plain, p22, inference(split_conjunct,[status(thm)],[ax39])).
% 1.08/1.29 thf(c_0_26, plain, (~p2|ford_less_eq_a @ fv1 @ fv), inference(fof_nnf,[status(thm)],[pax2])).
% 1.08/1.29 thf(c_0_27, plain, (~p1|ford_less_eq_a @ fv2 @ fv1), inference(fof_nnf,[status(thm)],[pax1])).
% 1.08/1.29 thf(c_0_28, plain, (p40|(fheapIm1091024090Down_a @ (ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)))!=(ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2))), inference(split_conjunct,[status(thm)],[c_0_18])).
% 1.08/1.29 thf(c_0_29, plain, ~p40, inference(sr,[status(thm)],[c_0_19, c_0_20])).
% 1.08/1.29 thf(c_0_30, plain, ![X2:tree_a, X12:a, X10:a, X8:tree_a, X7:tree_a, X6:a, X3:tree_a]:((fheapIm1091024090Down_a @ (ft_a @ X10 @ (ft_a @ X6 @ X2 @ X3) @ (ft_a @ X12 @ X7 @ X8)))=(ft_a @ X10 @ (ft_a @ X6 @ X2 @ X3) @ (ft_a @ X12 @ X7 @ X8))|~ford_less_eq_a @ (fval_a @ (ft_a @ X6 @ X2 @ X3)) @ X10|~ford_less_eq_a @ (fval_a @ (ft_a @ X12 @ X7 @ X8)) @ (fval_a @ (ft_a @ X6 @ X2 @ X3))|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_21])).
% 1.08/1.29 thf(c_0_31, plain, epred1_0, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_22, c_0_23])])).
% 1.08/1.29 thf(c_0_32, plain, ![X2:tree_a, X3:tree_a, X6:a]:(fval_a @ (ft_a @ X6 @ X2 @ X3))=(X6), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_24, c_0_25])])).
% 1.08/1.29 thf(c_0_33, plain, (ford_less_eq_a @ fv1 @ fv|~p2), inference(split_conjunct,[status(thm)],[c_0_26])).
% 1.08/1.29 thf(c_0_34, plain, p2, inference(split_conjunct,[status(thm)],[ax59])).
% 1.08/1.29 thf(c_0_35, plain, (ford_less_eq_a @ fv2 @ fv1|~p1), inference(split_conjunct,[status(thm)],[c_0_27])).
% 1.08/1.29 thf(c_0_36, plain, p1, inference(split_conjunct,[status(thm)],[ax60])).
% 1.08/1.29 thf(c_0_37, plain, (fheapIm1091024090Down_a @ (ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)))!=(ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)), inference(sr,[status(thm)],[c_0_28, c_0_29])).
% 1.08/1.29 thf(c_0_38, plain, ![X2:tree_a, X3:tree_a, X7:tree_a, X6:a, X8:tree_a, X12:a, X10:a]:((fheapIm1091024090Down_a @ (ft_a @ X6 @ (ft_a @ X10 @ X2 @ X3) @ (ft_a @ X12 @ X7 @ X8)))=(ft_a @ X6 @ (ft_a @ X10 @ X2 @ X3) @ (ft_a @ X12 @ X7 @ X8))|~ford_less_eq_a @ X10 @ X6|~ford_less_eq_a @ X12 @ X10), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_30, c_0_31]), c_0_32]), c_0_32]), c_0_32])])).
% 1.08/1.29 thf(c_0_39, plain, ford_less_eq_a @ fv1 @ fv, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_33, c_0_34])])).
% 1.08/1.29 thf(c_0_40, plain, ford_less_eq_a @ fv2 @ fv1, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_35, c_0_36])])).
% 1.08/1.29 thf(c_0_41, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_38]), c_0_39]), c_0_40])]), ['proof']).
% 1.08/1.29 thf(7,plain,$false,inference(eprover,[status(thm),assumptions([h5,h4,h7,h2,h0])],[])).
% 1.08/1.29 thf(pax23, axiom, (p23=>![X24:a, X25:tree_a, X26:tree_a, X27:a, X21:tree_a, X28:tree_a, X29:a]:~(((ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (fval_a @ (ft_a @ X27 @ X21 @ X28))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ X29=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ X29)=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ (fheapIm1091024090Down_a @ (ft_a @ X29 @ (fheapIm1140443833left_a @ (ft_a @ X27 @ X21 @ X28)) @ (fheapIm1257206334ight_a @ (ft_a @ X27 @ X21 @ X28)))) @ (ft_a @ X24 @ X25 @ X26)))))))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (fval_a @ (ft_a @ X27 @ X21 @ X28)))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ X29=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ X29)=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (ft_a @ X27 @ X21 @ X28) @ (fheapIm1091024090Down_a @ (ft_a @ X29 @ (fheapIm1140443833left_a @ (ft_a @ X24 @ X25 @ X26)) @ (fheapIm1257206334ight_a @ (ft_a @ X24 @ X25 @ X26)))))))))))))), file('<stdin>', pax23)).
% 1.08/1.29 thf(ax31, axiom, (p33|~(p40)), file('<stdin>', ax31)).
% 1.08/1.29 thf(ax39, axiom, ~(p33), file('<stdin>', ax39)).
% 1.08/1.29 thf(pax22, axiom, (p22=>![X24:a, X25:tree_a, X26:tree_a]:(fval_a @ (ft_a @ X24 @ X25 @ X26))=(X24)), file('<stdin>', pax22)).
% 1.08/1.29 thf(nax40, axiom, (p40<=(fheapIm1091024090Down_a @ (ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)))=(ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2))), file('<stdin>', nax40)).
% 1.08/1.29 thf(ax48, axiom, p23, file('<stdin>', ax48)).
% 1.08/1.29 thf(ax49, axiom, p22, file('<stdin>', ax49)).
% 1.08/1.29 thf(pax2, axiom, (p2=>ford_less_eq_a @ fv1 @ fv), file('<stdin>', pax2)).
% 1.08/1.29 thf(pax1, axiom, (p1=>ford_less_eq_a @ fv2 @ fv1), file('<stdin>', pax1)).
% 1.08/1.29 thf(ax69, axiom, p2, file('<stdin>', ax69)).
% 1.08/1.29 thf(ax70, axiom, p1, file('<stdin>', ax70)).
% 1.08/1.29 thf(c_0_11, plain, (epred1_0<=>![X24:a, X25:tree_a, X26:tree_a, X27:a, X21:tree_a, X28:tree_a, X29:a]:~(((ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (fval_a @ (ft_a @ X27 @ X21 @ X28))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ X29=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ X29)=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ (fheapIm1091024090Down_a @ (ft_a @ X29 @ (fheapIm1140443833left_a @ (ft_a @ X27 @ X21 @ X28)) @ (fheapIm1257206334ight_a @ (ft_a @ X27 @ X21 @ X28)))) @ (ft_a @ X24 @ X25 @ X26)))))))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (fval_a @ (ft_a @ X27 @ X21 @ X28)))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ X29=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ X29)=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (ft_a @ X27 @ X21 @ X28) @ (fheapIm1091024090Down_a @ (ft_a @ X29 @ (fheapIm1140443833left_a @ (ft_a @ X24 @ X25 @ X26)) @ (fheapIm1257206334ight_a @ (ft_a @ X24 @ X25 @ X26)))))))))))))), introduced(definition)).
% 1.08/1.29 thf(c_0_12, axiom, (p23=>epred1_0), inference(apply_def,[status(thm)],[pax23, c_0_11])).
% 1.08/1.29 thf(c_0_13, plain, (p33|~p40), inference(fof_simplification,[status(thm)],[ax31])).
% 1.08/1.29 thf(c_0_14, plain, ~p33, inference(fof_simplification,[status(thm)],[ax39])).
% 1.08/1.29 thf(c_0_15, plain, (epred1_0=>![X24:a, X25:tree_a, X26:tree_a, X27:a, X21:tree_a, X28:tree_a, X29:a]:~(((ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (fval_a @ (ft_a @ X27 @ X21 @ X28))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ X29=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ X29)=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ (fheapIm1091024090Down_a @ (ft_a @ X29 @ (fheapIm1140443833left_a @ (ft_a @ X27 @ X21 @ X28)) @ (fheapIm1257206334ight_a @ (ft_a @ X27 @ X21 @ X28)))) @ (ft_a @ X24 @ X25 @ X26)))))))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (fval_a @ (ft_a @ X27 @ X21 @ X28)))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ X29=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ X29)=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (ft_a @ X27 @ X21 @ X28) @ (fheapIm1091024090Down_a @ (ft_a @ X29 @ (fheapIm1140443833left_a @ (ft_a @ X24 @ X25 @ X26)) @ (fheapIm1257206334ight_a @ (ft_a @ X24 @ X25 @ X26)))))))))))))), inference(split_equiv,[status(thm)],[c_0_11])).
% 1.08/1.29 thf(c_0_16, plain, (~p23|epred1_0), inference(fof_nnf,[status(thm)],[c_0_12])).
% 1.08/1.29 thf(c_0_17, plain, ![X211:a, X212:tree_a, X213:tree_a]:(~p22|(fval_a @ (ft_a @ X211 @ X212 @ X213))=(X211)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax22])])])).
% 1.08/1.29 thf(c_0_18, plain, ((fheapIm1091024090Down_a @ (ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)))!=(ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2))|p40), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax40])])).
% 1.08/1.29 thf(c_0_19, plain, (p33|~p40), inference(split_conjunct,[status(thm)],[c_0_13])).
% 1.08/1.29 thf(c_0_20, plain, ~p33, inference(split_conjunct,[status(thm)],[c_0_14])).
% 1.08/1.29 thf(c_0_21, plain, ![X309:a, X310:tree_a, X311:tree_a, X312:a, X313:tree_a, X314:tree_a, X315:a]:(((~ford_less_eq_a @ (fval_a @ (ft_a @ X312 @ X313 @ X314)) @ X315|(fheapIm1091024090Down_a @ (ft_a @ X315 @ (ft_a @ X312 @ X313 @ X314) @ (ft_a @ X309 @ X310 @ X311)))=(ft_a @ X315 @ (ft_a @ X312 @ X313 @ X314) @ (ft_a @ X309 @ X310 @ X311))|~ford_less_eq_a @ (fval_a @ (ft_a @ X309 @ X310 @ X311)) @ (fval_a @ (ft_a @ X312 @ X313 @ X314))|~epred1_0)&(ford_less_eq_a @ (fval_a @ (ft_a @ X312 @ X313 @ X314)) @ X315|(fheapIm1091024090Down_a @ (ft_a @ X315 @ (ft_a @ X312 @ X313 @ X314) @ (ft_a @ X309 @ X310 @ X311)))=(ft_a @ (fval_a @ (ft_a @ X312 @ X313 @ X314)) @ (fheapIm1091024090Down_a @ (ft_a @ X315 @ (fheapIm1140443833left_a @ (ft_a @ X312 @ X313 @ X314)) @ (fheapIm1257206334ight_a @ (ft_a @ X312 @ X313 @ X314)))) @ (ft_a @ X309 @ X310 @ X311))|~ford_less_eq_a @ (fval_a @ (ft_a @ X309 @ X310 @ X311)) @ (fval_a @ (ft_a @ X312 @ X313 @ X314))|~epred1_0))&((~ford_less_eq_a @ (fval_a @ (ft_a @ X309 @ X310 @ X311)) @ X315|(fheapIm1091024090Down_a @ (ft_a @ X315 @ (ft_a @ X312 @ X313 @ X314) @ (ft_a @ X309 @ X310 @ X311)))=(ft_a @ X315 @ (ft_a @ X312 @ X313 @ X314) @ (ft_a @ X309 @ X310 @ X311))|ford_less_eq_a @ (fval_a @ (ft_a @ X309 @ X310 @ X311)) @ (fval_a @ (ft_a @ X312 @ X313 @ X314))|~epred1_0)&(ford_less_eq_a @ (fval_a @ (ft_a @ X309 @ X310 @ X311)) @ X315|(fheapIm1091024090Down_a @ (ft_a @ X315 @ (ft_a @ X312 @ X313 @ X314) @ (ft_a @ X309 @ X310 @ X311)))=(ft_a @ (fval_a @ (ft_a @ X309 @ X310 @ X311)) @ (ft_a @ X312 @ X313 @ X314) @ (fheapIm1091024090Down_a @ (ft_a @ X315 @ (fheapIm1140443833left_a @ (ft_a @ X309 @ X310 @ X311)) @ (fheapIm1257206334ight_a @ (ft_a @ X309 @ X310 @ X311)))))|ford_less_eq_a @ (fval_a @ (ft_a @ X309 @ X310 @ X311)) @ (fval_a @ (ft_a @ X312 @ X313 @ X314))|~epred1_0))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_15])])])])])).
% 1.08/1.29 thf(c_0_22, plain, (epred1_0|~p23), inference(split_conjunct,[status(thm)],[c_0_16])).
% 1.08/1.29 thf(c_0_23, plain, p23, inference(split_conjunct,[status(thm)],[ax48])).
% 1.08/1.29 thf(c_0_24, plain, ![X4:tree_a, X3:tree_a, X1:a]:((fval_a @ (ft_a @ X1 @ X3 @ X4))=(X1)|~p22), inference(split_conjunct,[status(thm)],[c_0_17])).
% 1.08/1.29 thf(c_0_25, plain, p22, inference(split_conjunct,[status(thm)],[ax49])).
% 1.08/1.29 thf(c_0_26, plain, (~p2|ford_less_eq_a @ fv1 @ fv), inference(fof_nnf,[status(thm)],[pax2])).
% 1.08/1.29 thf(c_0_27, plain, (~p1|ford_less_eq_a @ fv2 @ fv1), inference(fof_nnf,[status(thm)],[pax1])).
% 1.08/1.29 thf(c_0_28, plain, (p40|(fheapIm1091024090Down_a @ (ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)))!=(ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2))), inference(split_conjunct,[status(thm)],[c_0_18])).
% 1.08/1.29 thf(c_0_29, plain, ~p40, inference(sr,[status(thm)],[c_0_19, c_0_20])).
% 1.08/1.29 thf(c_0_30, plain, ![X2:a, X1:a, X3:tree_a, X7:tree_a, X6:tree_a, X5:a, X4:tree_a]:((fheapIm1091024090Down_a @ (ft_a @ X2 @ (ft_a @ X1 @ X3 @ X4) @ (ft_a @ X5 @ X6 @ X7)))=(ft_a @ X2 @ (ft_a @ X1 @ X3 @ X4) @ (ft_a @ X5 @ X6 @ X7))|~ford_less_eq_a @ (fval_a @ (ft_a @ X1 @ X3 @ X4)) @ X2|~ford_less_eq_a @ (fval_a @ (ft_a @ X5 @ X6 @ X7)) @ (fval_a @ (ft_a @ X1 @ X3 @ X4))|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_21])).
% 1.08/1.29 thf(c_0_31, plain, epred1_0, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_22, c_0_23])])).
% 1.08/1.29 thf(c_0_32, plain, ![X4:tree_a, X3:tree_a, X1:a]:(fval_a @ (ft_a @ X1 @ X3 @ X4))=(X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_24, c_0_25])])).
% 1.08/1.29 thf(c_0_33, plain, (ford_less_eq_a @ fv1 @ fv|~p2), inference(split_conjunct,[status(thm)],[c_0_26])).
% 1.08/1.29 thf(c_0_34, plain, p2, inference(split_conjunct,[status(thm)],[ax69])).
% 1.08/1.29 thf(c_0_35, plain, (ford_less_eq_a @ fv2 @ fv1|~p1), inference(split_conjunct,[status(thm)],[c_0_27])).
% 1.08/1.29 thf(c_0_36, plain, p1, inference(split_conjunct,[status(thm)],[ax70])).
% 1.08/1.29 thf(c_0_37, plain, (fheapIm1091024090Down_a @ (ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)))!=(ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)), inference(sr,[status(thm)],[c_0_28, c_0_29])).
% 1.08/1.29 thf(c_0_38, plain, ![X1:a, X3:tree_a, X4:tree_a, X7:tree_a, X6:tree_a, X5:a, X2:a]:((fheapIm1091024090Down_a @ (ft_a @ X1 @ (ft_a @ X2 @ X3 @ X4) @ (ft_a @ X5 @ X6 @ X7)))=(ft_a @ X1 @ (ft_a @ X2 @ X3 @ X4) @ (ft_a @ X5 @ X6 @ X7))|~ford_less_eq_a @ X2 @ X1|~ford_less_eq_a @ X5 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_30, c_0_31]), c_0_32]), c_0_32]), c_0_32])])).
% 1.08/1.29 thf(c_0_39, plain, ford_less_eq_a @ fv1 @ fv, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_33, c_0_34])])).
% 1.08/1.29 thf(c_0_40, plain, ford_less_eq_a @ fv2 @ fv1, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_35, c_0_36])])).
% 1.08/1.29 thf(c_0_41, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_38]), c_0_39]), c_0_40])]), ['proof']).
% 1.08/1.29 thf(8,plain,$false,inference(eprover,[status(thm),assumptions([h6,h4,h7,h2,h0])],[])).
% 1.08/1.29 thf(9,plain,$false,inference(tab_imp,[status(thm),assumptions([h4,h7,h2,h0]),tab_imp(discharge,[h5]),tab_imp(discharge,[h6])],[h4,7,8,h5,h6])).
% 1.08/1.29 thf(10,plain,$false,inference(tab_imp,[status(thm),assumptions([h7,h2,h0]),tab_imp(discharge,[h3]),tab_imp(discharge,[h4])],[fact_2__C5__2_Ohyps_C_I2_J,6,9,h3,h4])).
% 1.08/1.29 thf(pax23, axiom, (p23=>![X24:a, X25:tree_a, X26:tree_a, X27:a, X21:tree_a, X28:tree_a, X29:a]:~(((ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (fval_a @ (ft_a @ X27 @ X21 @ X28))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ X29=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ X29)=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ (fheapIm1091024090Down_a @ (ft_a @ X29 @ (fheapIm1140443833left_a @ (ft_a @ X27 @ X21 @ X28)) @ (fheapIm1257206334ight_a @ (ft_a @ X27 @ X21 @ X28)))) @ (ft_a @ X24 @ X25 @ X26)))))))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (fval_a @ (ft_a @ X27 @ X21 @ X28)))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ X29=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ X29)=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (ft_a @ X27 @ X21 @ X28) @ (fheapIm1091024090Down_a @ (ft_a @ X29 @ (fheapIm1140443833left_a @ (ft_a @ X24 @ X25 @ X26)) @ (fheapIm1257206334ight_a @ (ft_a @ X24 @ X25 @ X26)))))))))))))), file('<stdin>', pax23)).
% 1.08/1.29 thf(ax39, axiom, (p33|~(p40)), file('<stdin>', ax39)).
% 1.08/1.29 thf(ax47, axiom, ~(p33), file('<stdin>', ax47)).
% 1.08/1.29 thf(pax22, axiom, (p22=>![X24:a, X25:tree_a, X26:tree_a]:(fval_a @ (ft_a @ X24 @ X25 @ X26))=(X24)), file('<stdin>', pax22)).
% 1.08/1.29 thf(nax40, axiom, (p40<=(fheapIm1091024090Down_a @ (ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)))=(ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2))), file('<stdin>', nax40)).
% 1.08/1.29 thf(ax56, axiom, p23, file('<stdin>', ax56)).
% 1.08/1.29 thf(ax57, axiom, p22, file('<stdin>', ax57)).
% 1.08/1.29 thf(pax2, axiom, (p2=>ford_less_eq_a @ fv1 @ fv), file('<stdin>', pax2)).
% 1.08/1.29 thf(pax1, axiom, (p1=>ford_less_eq_a @ fv2 @ fv1), file('<stdin>', pax1)).
% 1.08/1.29 thf(ax77, axiom, p2, file('<stdin>', ax77)).
% 1.08/1.29 thf(ax78, axiom, p1, file('<stdin>', ax78)).
% 1.08/1.29 thf(c_0_11, plain, (epred1_0<=>![X24:a, X25:tree_a, X26:tree_a, X27:a, X21:tree_a, X28:tree_a, X29:a]:~(((ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (fval_a @ (ft_a @ X27 @ X21 @ X28))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ X29=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ X29)=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ (fheapIm1091024090Down_a @ (ft_a @ X29 @ (fheapIm1140443833left_a @ (ft_a @ X27 @ X21 @ X28)) @ (fheapIm1257206334ight_a @ (ft_a @ X27 @ X21 @ X28)))) @ (ft_a @ X24 @ X25 @ X26)))))))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (fval_a @ (ft_a @ X27 @ X21 @ X28)))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ X29=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ X29)=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (ft_a @ X27 @ X21 @ X28) @ (fheapIm1091024090Down_a @ (ft_a @ X29 @ (fheapIm1140443833left_a @ (ft_a @ X24 @ X25 @ X26)) @ (fheapIm1257206334ight_a @ (ft_a @ X24 @ X25 @ X26)))))))))))))), introduced(definition)).
% 1.08/1.29 thf(c_0_12, axiom, (p23=>epred1_0), inference(apply_def,[status(thm)],[pax23, c_0_11])).
% 1.08/1.29 thf(c_0_13, plain, (p33|~p40), inference(fof_simplification,[status(thm)],[ax39])).
% 1.08/1.29 thf(c_0_14, plain, ~p33, inference(fof_simplification,[status(thm)],[ax47])).
% 1.08/1.29 thf(c_0_15, plain, (epred1_0=>![X24:a, X25:tree_a, X26:tree_a, X27:a, X21:tree_a, X28:tree_a, X29:a]:~(((ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (fval_a @ (ft_a @ X27 @ X21 @ X28))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ X29=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ X29)=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ (fheapIm1091024090Down_a @ (ft_a @ X29 @ (fheapIm1140443833left_a @ (ft_a @ X27 @ X21 @ X28)) @ (fheapIm1257206334ight_a @ (ft_a @ X27 @ X21 @ X28)))) @ (ft_a @ X24 @ X25 @ X26)))))))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (fval_a @ (ft_a @ X27 @ X21 @ X28)))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ X29=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ X29)=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (ft_a @ X27 @ X21 @ X28) @ (fheapIm1091024090Down_a @ (ft_a @ X29 @ (fheapIm1140443833left_a @ (ft_a @ X24 @ X25 @ X26)) @ (fheapIm1257206334ight_a @ (ft_a @ X24 @ X25 @ X26)))))))))))))), inference(split_equiv,[status(thm)],[c_0_11])).
% 1.08/1.29 thf(c_0_16, plain, (~p23|epred1_0), inference(fof_nnf,[status(thm)],[c_0_12])).
% 1.08/1.29 thf(c_0_17, plain, ![X371:a, X372:tree_a, X373:tree_a]:(~p22|(fval_a @ (ft_a @ X371 @ X372 @ X373))=(X371)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax22])])])).
% 1.08/1.29 thf(c_0_18, plain, ((fheapIm1091024090Down_a @ (ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)))!=(ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2))|p40), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax40])])).
% 1.08/1.29 thf(c_0_19, plain, (p33|~p40), inference(split_conjunct,[status(thm)],[c_0_13])).
% 1.08/1.29 thf(c_0_20, plain, ~p33, inference(split_conjunct,[status(thm)],[c_0_14])).
% 1.08/1.29 thf(c_0_21, plain, ![X469:a, X470:tree_a, X471:tree_a, X472:a, X473:tree_a, X474:tree_a, X475:a]:(((~ford_less_eq_a @ (fval_a @ (ft_a @ X472 @ X473 @ X474)) @ X475|(fheapIm1091024090Down_a @ (ft_a @ X475 @ (ft_a @ X472 @ X473 @ X474) @ (ft_a @ X469 @ X470 @ X471)))=(ft_a @ X475 @ (ft_a @ X472 @ X473 @ X474) @ (ft_a @ X469 @ X470 @ X471))|~ford_less_eq_a @ (fval_a @ (ft_a @ X469 @ X470 @ X471)) @ (fval_a @ (ft_a @ X472 @ X473 @ X474))|~epred1_0)&(ford_less_eq_a @ (fval_a @ (ft_a @ X472 @ X473 @ X474)) @ X475|(fheapIm1091024090Down_a @ (ft_a @ X475 @ (ft_a @ X472 @ X473 @ X474) @ (ft_a @ X469 @ X470 @ X471)))=(ft_a @ (fval_a @ (ft_a @ X472 @ X473 @ X474)) @ (fheapIm1091024090Down_a @ (ft_a @ X475 @ (fheapIm1140443833left_a @ (ft_a @ X472 @ X473 @ X474)) @ (fheapIm1257206334ight_a @ (ft_a @ X472 @ X473 @ X474)))) @ (ft_a @ X469 @ X470 @ X471))|~ford_less_eq_a @ (fval_a @ (ft_a @ X469 @ X470 @ X471)) @ (fval_a @ (ft_a @ X472 @ X473 @ X474))|~epred1_0))&((~ford_less_eq_a @ (fval_a @ (ft_a @ X469 @ X470 @ X471)) @ X475|(fheapIm1091024090Down_a @ (ft_a @ X475 @ (ft_a @ X472 @ X473 @ X474) @ (ft_a @ X469 @ X470 @ X471)))=(ft_a @ X475 @ (ft_a @ X472 @ X473 @ X474) @ (ft_a @ X469 @ X470 @ X471))|ford_less_eq_a @ (fval_a @ (ft_a @ X469 @ X470 @ X471)) @ (fval_a @ (ft_a @ X472 @ X473 @ X474))|~epred1_0)&(ford_less_eq_a @ (fval_a @ (ft_a @ X469 @ X470 @ X471)) @ X475|(fheapIm1091024090Down_a @ (ft_a @ X475 @ (ft_a @ X472 @ X473 @ X474) @ (ft_a @ X469 @ X470 @ X471)))=(ft_a @ (fval_a @ (ft_a @ X469 @ X470 @ X471)) @ (ft_a @ X472 @ X473 @ X474) @ (fheapIm1091024090Down_a @ (ft_a @ X475 @ (fheapIm1140443833left_a @ (ft_a @ X469 @ X470 @ X471)) @ (fheapIm1257206334ight_a @ (ft_a @ X469 @ X470 @ X471)))))|ford_less_eq_a @ (fval_a @ (ft_a @ X469 @ X470 @ X471)) @ (fval_a @ (ft_a @ X472 @ X473 @ X474))|~epred1_0))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_15])])])])])).
% 1.08/1.29 thf(c_0_22, plain, (epred1_0|~p23), inference(split_conjunct,[status(thm)],[c_0_16])).
% 1.08/1.29 thf(c_0_23, plain, p23, inference(split_conjunct,[status(thm)],[ax56])).
% 1.08/1.29 thf(c_0_24, plain, ![X4:tree_a, X3:tree_a, X1:a]:((fval_a @ (ft_a @ X1 @ X3 @ X4))=(X1)|~p22), inference(split_conjunct,[status(thm)],[c_0_17])).
% 1.08/1.29 thf(c_0_25, plain, p22, inference(split_conjunct,[status(thm)],[ax57])).
% 1.08/1.29 thf(c_0_26, plain, (~p2|ford_less_eq_a @ fv1 @ fv), inference(fof_nnf,[status(thm)],[pax2])).
% 1.08/1.29 thf(c_0_27, plain, (~p1|ford_less_eq_a @ fv2 @ fv1), inference(fof_nnf,[status(thm)],[pax1])).
% 1.08/1.29 thf(c_0_28, plain, (p40|(fheapIm1091024090Down_a @ (ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)))!=(ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2))), inference(split_conjunct,[status(thm)],[c_0_18])).
% 1.08/1.29 thf(c_0_29, plain, ~p40, inference(sr,[status(thm)],[c_0_19, c_0_20])).
% 1.08/1.29 thf(c_0_30, plain, ![X2:a, X1:a, X3:tree_a, X7:tree_a, X6:tree_a, X5:a, X4:tree_a]:((fheapIm1091024090Down_a @ (ft_a @ X2 @ (ft_a @ X1 @ X3 @ X4) @ (ft_a @ X5 @ X6 @ X7)))=(ft_a @ X2 @ (ft_a @ X1 @ X3 @ X4) @ (ft_a @ X5 @ X6 @ X7))|~ford_less_eq_a @ (fval_a @ (ft_a @ X1 @ X3 @ X4)) @ X2|~ford_less_eq_a @ (fval_a @ (ft_a @ X5 @ X6 @ X7)) @ (fval_a @ (ft_a @ X1 @ X3 @ X4))|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_21])).
% 1.08/1.29 thf(c_0_31, plain, epred1_0, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_22, c_0_23])])).
% 1.08/1.29 thf(c_0_32, plain, ![X4:tree_a, X3:tree_a, X1:a]:(fval_a @ (ft_a @ X1 @ X3 @ X4))=(X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_24, c_0_25])])).
% 1.08/1.29 thf(c_0_33, plain, (ford_less_eq_a @ fv1 @ fv|~p2), inference(split_conjunct,[status(thm)],[c_0_26])).
% 1.08/1.29 thf(c_0_34, plain, p2, inference(split_conjunct,[status(thm)],[ax77])).
% 1.08/1.29 thf(c_0_35, plain, (ford_less_eq_a @ fv2 @ fv1|~p1), inference(split_conjunct,[status(thm)],[c_0_27])).
% 1.08/1.29 thf(c_0_36, plain, p1, inference(split_conjunct,[status(thm)],[ax78])).
% 1.08/1.29 thf(c_0_37, plain, (fheapIm1091024090Down_a @ (ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)))!=(ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)), inference(sr,[status(thm)],[c_0_28, c_0_29])).
% 1.08/1.29 thf(c_0_38, plain, ![X1:a, X3:tree_a, X4:tree_a, X7:tree_a, X6:tree_a, X5:a, X2:a]:((fheapIm1091024090Down_a @ (ft_a @ X1 @ (ft_a @ X2 @ X3 @ X4) @ (ft_a @ X5 @ X6 @ X7)))=(ft_a @ X1 @ (ft_a @ X2 @ X3 @ X4) @ (ft_a @ X5 @ X6 @ X7))|~ford_less_eq_a @ X2 @ X1|~ford_less_eq_a @ X5 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_30, c_0_31]), c_0_32]), c_0_32]), c_0_32])])).
% 1.08/1.29 thf(c_0_39, plain, ford_less_eq_a @ fv1 @ fv, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_33, c_0_34])])).
% 1.08/1.29 thf(c_0_40, plain, ford_less_eq_a @ fv2 @ fv1, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_35, c_0_36])])).
% 1.08/1.29 thf(c_0_41, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_38]), c_0_39]), c_0_40])]), ['proof']).
% 1.08/1.29 thf(11,plain,$false,inference(eprover,[status(thm),assumptions([h3,h8,h2,h0])],[])).
% 1.08/1.29 thf(pax23, axiom, (p23=>![X24:a, X25:tree_a, X26:tree_a, X27:a, X21:tree_a, X28:tree_a, X29:a]:~(((ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (fval_a @ (ft_a @ X27 @ X21 @ X28))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ X29=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ X29)=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ (fheapIm1091024090Down_a @ (ft_a @ X29 @ (fheapIm1140443833left_a @ (ft_a @ X27 @ X21 @ X28)) @ (fheapIm1257206334ight_a @ (ft_a @ X27 @ X21 @ X28)))) @ (ft_a @ X24 @ X25 @ X26)))))))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (fval_a @ (ft_a @ X27 @ X21 @ X28)))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ X29=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ X29)=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (ft_a @ X27 @ X21 @ X28) @ (fheapIm1091024090Down_a @ (ft_a @ X29 @ (fheapIm1140443833left_a @ (ft_a @ X24 @ X25 @ X26)) @ (fheapIm1257206334ight_a @ (ft_a @ X24 @ X25 @ X26)))))))))))))), file('<stdin>', pax23)).
% 1.08/1.29 thf(ax50, axiom, (p33|~(p40)), file('<stdin>', ax50)).
% 1.08/1.29 thf(ax58, axiom, ~(p33), file('<stdin>', ax58)).
% 1.08/1.29 thf(pax22, axiom, (p22=>![X24:a, X25:tree_a, X26:tree_a]:(fval_a @ (ft_a @ X24 @ X25 @ X26))=(X24)), file('<stdin>', pax22)).
% 1.08/1.29 thf(nax40, axiom, (p40<=(fheapIm1091024090Down_a @ (ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)))=(ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2))), file('<stdin>', nax40)).
% 1.08/1.29 thf(ax67, axiom, p23, file('<stdin>', ax67)).
% 1.08/1.29 thf(ax68, axiom, p22, file('<stdin>', ax68)).
% 1.08/1.29 thf(pax2, axiom, (p2=>ford_less_eq_a @ fv1 @ fv), file('<stdin>', pax2)).
% 1.08/1.29 thf(pax1, axiom, (p1=>ford_less_eq_a @ fv2 @ fv1), file('<stdin>', pax1)).
% 1.08/1.29 thf(ax88, axiom, p2, file('<stdin>', ax88)).
% 1.08/1.29 thf(ax89, axiom, p1, file('<stdin>', ax89)).
% 1.08/1.29 thf(c_0_11, plain, (epred1_0<=>![X24:a, X25:tree_a, X26:tree_a, X27:a, X21:tree_a, X28:tree_a, X29:a]:~(((ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (fval_a @ (ft_a @ X27 @ X21 @ X28))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ X29=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ X29)=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ (fheapIm1091024090Down_a @ (ft_a @ X29 @ (fheapIm1140443833left_a @ (ft_a @ X27 @ X21 @ X28)) @ (fheapIm1257206334ight_a @ (ft_a @ X27 @ X21 @ X28)))) @ (ft_a @ X24 @ X25 @ X26)))))))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (fval_a @ (ft_a @ X27 @ X21 @ X28)))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ X29=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ X29)=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (ft_a @ X27 @ X21 @ X28) @ (fheapIm1091024090Down_a @ (ft_a @ X29 @ (fheapIm1140443833left_a @ (ft_a @ X24 @ X25 @ X26)) @ (fheapIm1257206334ight_a @ (ft_a @ X24 @ X25 @ X26)))))))))))))), introduced(definition)).
% 1.08/1.29 thf(c_0_12, axiom, (p23=>epred1_0), inference(apply_def,[status(thm)],[pax23, c_0_11])).
% 1.08/1.29 thf(c_0_13, plain, (p33|~p40), inference(fof_simplification,[status(thm)],[ax50])).
% 1.08/1.29 thf(c_0_14, plain, ~p33, inference(fof_simplification,[status(thm)],[ax58])).
% 1.08/1.29 thf(c_0_15, plain, (epred1_0=>![X24:a, X25:tree_a, X26:tree_a, X27:a, X21:tree_a, X28:tree_a, X29:a]:~(((ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (fval_a @ (ft_a @ X27 @ X21 @ X28))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ X29=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ X29)=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ (fheapIm1091024090Down_a @ (ft_a @ X29 @ (fheapIm1140443833left_a @ (ft_a @ X27 @ X21 @ X28)) @ (fheapIm1257206334ight_a @ (ft_a @ X27 @ X21 @ X28)))) @ (ft_a @ X24 @ X25 @ X26)))))))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (fval_a @ (ft_a @ X27 @ X21 @ X28)))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ X29=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ X29)=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (ft_a @ X27 @ X21 @ X28) @ (fheapIm1091024090Down_a @ (ft_a @ X29 @ (fheapIm1140443833left_a @ (ft_a @ X24 @ X25 @ X26)) @ (fheapIm1257206334ight_a @ (ft_a @ X24 @ X25 @ X26)))))))))))))), inference(split_equiv,[status(thm)],[c_0_11])).
% 1.08/1.29 thf(c_0_16, plain, (~p23|epred1_0), inference(fof_nnf,[status(thm)],[c_0_12])).
% 1.08/1.29 thf(c_0_17, plain, ![X691:a, X692:tree_a, X693:tree_a]:(~p22|(fval_a @ (ft_a @ X691 @ X692 @ X693))=(X691)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax22])])])).
% 1.08/1.29 thf(c_0_18, plain, ((fheapIm1091024090Down_a @ (ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)))!=(ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2))|p40), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax40])])).
% 1.08/1.29 thf(c_0_19, plain, (p33|~p40), inference(split_conjunct,[status(thm)],[c_0_13])).
% 1.08/1.29 thf(c_0_20, plain, ~p33, inference(split_conjunct,[status(thm)],[c_0_14])).
% 1.08/1.29 thf(c_0_21, plain, ![X789:a, X790:tree_a, X791:tree_a, X792:a, X793:tree_a, X794:tree_a, X795:a]:(((~ford_less_eq_a @ (fval_a @ (ft_a @ X792 @ X793 @ X794)) @ X795|(fheapIm1091024090Down_a @ (ft_a @ X795 @ (ft_a @ X792 @ X793 @ X794) @ (ft_a @ X789 @ X790 @ X791)))=(ft_a @ X795 @ (ft_a @ X792 @ X793 @ X794) @ (ft_a @ X789 @ X790 @ X791))|~ford_less_eq_a @ (fval_a @ (ft_a @ X789 @ X790 @ X791)) @ (fval_a @ (ft_a @ X792 @ X793 @ X794))|~epred1_0)&(ford_less_eq_a @ (fval_a @ (ft_a @ X792 @ X793 @ X794)) @ X795|(fheapIm1091024090Down_a @ (ft_a @ X795 @ (ft_a @ X792 @ X793 @ X794) @ (ft_a @ X789 @ X790 @ X791)))=(ft_a @ (fval_a @ (ft_a @ X792 @ X793 @ X794)) @ (fheapIm1091024090Down_a @ (ft_a @ X795 @ (fheapIm1140443833left_a @ (ft_a @ X792 @ X793 @ X794)) @ (fheapIm1257206334ight_a @ (ft_a @ X792 @ X793 @ X794)))) @ (ft_a @ X789 @ X790 @ X791))|~ford_less_eq_a @ (fval_a @ (ft_a @ X789 @ X790 @ X791)) @ (fval_a @ (ft_a @ X792 @ X793 @ X794))|~epred1_0))&((~ford_less_eq_a @ (fval_a @ (ft_a @ X789 @ X790 @ X791)) @ X795|(fheapIm1091024090Down_a @ (ft_a @ X795 @ (ft_a @ X792 @ X793 @ X794) @ (ft_a @ X789 @ X790 @ X791)))=(ft_a @ X795 @ (ft_a @ X792 @ X793 @ X794) @ (ft_a @ X789 @ X790 @ X791))|ford_less_eq_a @ (fval_a @ (ft_a @ X789 @ X790 @ X791)) @ (fval_a @ (ft_a @ X792 @ X793 @ X794))|~epred1_0)&(ford_less_eq_a @ (fval_a @ (ft_a @ X789 @ X790 @ X791)) @ X795|(fheapIm1091024090Down_a @ (ft_a @ X795 @ (ft_a @ X792 @ X793 @ X794) @ (ft_a @ X789 @ X790 @ X791)))=(ft_a @ (fval_a @ (ft_a @ X789 @ X790 @ X791)) @ (ft_a @ X792 @ X793 @ X794) @ (fheapIm1091024090Down_a @ (ft_a @ X795 @ (fheapIm1140443833left_a @ (ft_a @ X789 @ X790 @ X791)) @ (fheapIm1257206334ight_a @ (ft_a @ X789 @ X790 @ X791)))))|ford_less_eq_a @ (fval_a @ (ft_a @ X789 @ X790 @ X791)) @ (fval_a @ (ft_a @ X792 @ X793 @ X794))|~epred1_0))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_15])])])])])).
% 1.08/1.29 thf(c_0_22, plain, (epred1_0|~p23), inference(split_conjunct,[status(thm)],[c_0_16])).
% 1.08/1.29 thf(c_0_23, plain, p23, inference(split_conjunct,[status(thm)],[ax67])).
% 1.08/1.29 thf(c_0_24, plain, ![X4:tree_a, X3:tree_a, X1:a]:((fval_a @ (ft_a @ X1 @ X3 @ X4))=(X1)|~p22), inference(split_conjunct,[status(thm)],[c_0_17])).
% 1.08/1.29 thf(c_0_25, plain, p22, inference(split_conjunct,[status(thm)],[ax68])).
% 1.08/1.29 thf(c_0_26, plain, (~p2|ford_less_eq_a @ fv1 @ fv), inference(fof_nnf,[status(thm)],[pax2])).
% 1.08/1.29 thf(c_0_27, plain, (~p1|ford_less_eq_a @ fv2 @ fv1), inference(fof_nnf,[status(thm)],[pax1])).
% 1.08/1.29 thf(c_0_28, plain, (p40|(fheapIm1091024090Down_a @ (ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)))!=(ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2))), inference(split_conjunct,[status(thm)],[c_0_18])).
% 1.08/1.29 thf(c_0_29, plain, ~p40, inference(sr,[status(thm)],[c_0_19, c_0_20])).
% 1.08/1.29 thf(c_0_30, plain, ![X2:a, X1:a, X3:tree_a, X7:tree_a, X6:tree_a, X5:a, X4:tree_a]:((fheapIm1091024090Down_a @ (ft_a @ X2 @ (ft_a @ X1 @ X3 @ X4) @ (ft_a @ X5 @ X6 @ X7)))=(ft_a @ X2 @ (ft_a @ X1 @ X3 @ X4) @ (ft_a @ X5 @ X6 @ X7))|~ford_less_eq_a @ (fval_a @ (ft_a @ X1 @ X3 @ X4)) @ X2|~ford_less_eq_a @ (fval_a @ (ft_a @ X5 @ X6 @ X7)) @ (fval_a @ (ft_a @ X1 @ X3 @ X4))|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_21])).
% 1.08/1.29 thf(c_0_31, plain, epred1_0, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_22, c_0_23])])).
% 1.08/1.29 thf(c_0_32, plain, ![X4:tree_a, X3:tree_a, X1:a]:(fval_a @ (ft_a @ X1 @ X3 @ X4))=(X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_24, c_0_25])])).
% 1.08/1.29 thf(c_0_33, plain, (ford_less_eq_a @ fv1 @ fv|~p2), inference(split_conjunct,[status(thm)],[c_0_26])).
% 1.08/1.29 thf(c_0_34, plain, p2, inference(split_conjunct,[status(thm)],[ax88])).
% 1.08/1.29 thf(c_0_35, plain, (ford_less_eq_a @ fv2 @ fv1|~p1), inference(split_conjunct,[status(thm)],[c_0_27])).
% 1.08/1.29 thf(c_0_36, plain, p1, inference(split_conjunct,[status(thm)],[ax89])).
% 1.08/1.29 thf(c_0_37, plain, (fheapIm1091024090Down_a @ (ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)))!=(ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)), inference(sr,[status(thm)],[c_0_28, c_0_29])).
% 1.08/1.29 thf(c_0_38, plain, ![X1:a, X3:tree_a, X4:tree_a, X7:tree_a, X6:tree_a, X5:a, X2:a]:((fheapIm1091024090Down_a @ (ft_a @ X1 @ (ft_a @ X2 @ X3 @ X4) @ (ft_a @ X5 @ X6 @ X7)))=(ft_a @ X1 @ (ft_a @ X2 @ X3 @ X4) @ (ft_a @ X5 @ X6 @ X7))|~ford_less_eq_a @ X2 @ X1|~ford_less_eq_a @ X5 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_30, c_0_31]), c_0_32]), c_0_32]), c_0_32])])).
% 1.08/1.29 thf(c_0_39, plain, ford_less_eq_a @ fv1 @ fv, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_33, c_0_34])])).
% 1.08/1.29 thf(c_0_40, plain, ford_less_eq_a @ fv2 @ fv1, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_35, c_0_36])])).
% 1.08/1.29 thf(c_0_41, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_38]), c_0_39]), c_0_40])]), ['proof']).
% 1.08/1.29 thf(12,plain,$false,inference(eprover,[status(thm),assumptions([h5,h4,h8,h2,h0])],[])).
% 1.08/1.29 thf(pax23, axiom, (p23=>![X24:a, X25:tree_a, X26:tree_a, X27:a, X21:tree_a, X28:tree_a, X29:a]:~(((ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (fval_a @ (ft_a @ X27 @ X21 @ X28))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ X29=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ X29)=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ (fheapIm1091024090Down_a @ (ft_a @ X29 @ (fheapIm1140443833left_a @ (ft_a @ X27 @ X21 @ X28)) @ (fheapIm1257206334ight_a @ (ft_a @ X27 @ X21 @ X28)))) @ (ft_a @ X24 @ X25 @ X26)))))))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (fval_a @ (ft_a @ X27 @ X21 @ X28)))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ X29=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ X29)=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (ft_a @ X27 @ X21 @ X28) @ (fheapIm1091024090Down_a @ (ft_a @ X29 @ (fheapIm1140443833left_a @ (ft_a @ X24 @ X25 @ X26)) @ (fheapIm1257206334ight_a @ (ft_a @ X24 @ X25 @ X26)))))))))))))), file('<stdin>', pax23)).
% 1.08/1.29 thf(ax60, axiom, (p33|~(p40)), file('<stdin>', ax60)).
% 1.08/1.29 thf(ax68, axiom, ~(p33), file('<stdin>', ax68)).
% 1.08/1.29 thf(pax22, axiom, (p22=>![X24:a, X25:tree_a, X26:tree_a]:(fval_a @ (ft_a @ X24 @ X25 @ X26))=(X24)), file('<stdin>', pax22)).
% 1.08/1.29 thf(nax40, axiom, (p40<=(fheapIm1091024090Down_a @ (ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)))=(ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2))), file('<stdin>', nax40)).
% 1.08/1.29 thf(ax77, axiom, p23, file('<stdin>', ax77)).
% 1.08/1.29 thf(ax78, axiom, p22, file('<stdin>', ax78)).
% 1.08/1.29 thf(pax2, axiom, (p2=>ford_less_eq_a @ fv1 @ fv), file('<stdin>', pax2)).
% 1.08/1.29 thf(pax1, axiom, (p1=>ford_less_eq_a @ fv2 @ fv1), file('<stdin>', pax1)).
% 1.08/1.29 thf(ax98, axiom, p2, file('<stdin>', ax98)).
% 1.08/1.29 thf(ax99, axiom, p1, file('<stdin>', ax99)).
% 1.08/1.29 thf(c_0_11, plain, (epred1_0<=>![X24:a, X25:tree_a, X26:tree_a, X27:a, X21:tree_a, X28:tree_a, X29:a]:~(((ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (fval_a @ (ft_a @ X27 @ X21 @ X28))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ X29=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ X29)=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ (fheapIm1091024090Down_a @ (ft_a @ X29 @ (fheapIm1140443833left_a @ (ft_a @ X27 @ X21 @ X28)) @ (fheapIm1257206334ight_a @ (ft_a @ X27 @ X21 @ X28)))) @ (ft_a @ X24 @ X25 @ X26)))))))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (fval_a @ (ft_a @ X27 @ X21 @ X28)))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ X29=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ X29)=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (ft_a @ X27 @ X21 @ X28) @ (fheapIm1091024090Down_a @ (ft_a @ X29 @ (fheapIm1140443833left_a @ (ft_a @ X24 @ X25 @ X26)) @ (fheapIm1257206334ight_a @ (ft_a @ X24 @ X25 @ X26)))))))))))))), introduced(definition)).
% 1.08/1.29 thf(c_0_12, axiom, (p23=>epred1_0), inference(apply_def,[status(thm)],[pax23, c_0_11])).
% 1.08/1.29 thf(c_0_13, plain, (p33|~p40), inference(fof_simplification,[status(thm)],[ax60])).
% 1.08/1.29 thf(c_0_14, plain, ~p33, inference(fof_simplification,[status(thm)],[ax68])).
% 1.08/1.29 thf(c_0_15, plain, (epred1_0=>![X24:a, X25:tree_a, X26:tree_a, X27:a, X21:tree_a, X28:tree_a, X29:a]:~(((ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (fval_a @ (ft_a @ X27 @ X21 @ X28))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ X29=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ X29)=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ (fval_a @ (ft_a @ X27 @ X21 @ X28)) @ (fheapIm1091024090Down_a @ (ft_a @ X29 @ (fheapIm1140443833left_a @ (ft_a @ X27 @ X21 @ X28)) @ (fheapIm1257206334ight_a @ (ft_a @ X27 @ X21 @ X28)))) @ (ft_a @ X24 @ X25 @ X26)))))))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (fval_a @ (ft_a @ X27 @ X21 @ X28)))=>~(((ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ X29=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=>~((~(ford_less_eq_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ X29)=>(fheapIm1091024090Down_a @ (ft_a @ X29 @ (ft_a @ X27 @ X21 @ X28) @ (ft_a @ X24 @ X25 @ X26)))=(ft_a @ (fval_a @ (ft_a @ X24 @ X25 @ X26)) @ (ft_a @ X27 @ X21 @ X28) @ (fheapIm1091024090Down_a @ (ft_a @ X29 @ (fheapIm1140443833left_a @ (ft_a @ X24 @ X25 @ X26)) @ (fheapIm1257206334ight_a @ (ft_a @ X24 @ X25 @ X26)))))))))))))), inference(split_equiv,[status(thm)],[c_0_11])).
% 1.08/1.29 thf(c_0_16, plain, (~p23|epred1_0), inference(fof_nnf,[status(thm)],[c_0_12])).
% 1.08/1.29 thf(c_0_17, plain, ![X1123:a, X1124:tree_a, X1125:tree_a]:(~p22|(fval_a @ (ft_a @ X1123 @ X1124 @ X1125))=(X1123)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax22])])])).
% 1.08/1.29 thf(c_0_18, plain, ((fheapIm1091024090Down_a @ (ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)))!=(ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2))|p40), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax40])])).
% 1.08/1.29 thf(c_0_19, plain, (p33|~p40), inference(split_conjunct,[status(thm)],[c_0_13])).
% 1.08/1.29 thf(c_0_20, plain, ~p33, inference(split_conjunct,[status(thm)],[c_0_14])).
% 1.08/1.29 thf(c_0_21, plain, ![X1221:a, X1222:tree_a, X1223:tree_a, X1224:a, X1225:tree_a, X1226:tree_a, X1227:a]:(((~ford_less_eq_a @ (fval_a @ (ft_a @ X1224 @ X1225 @ X1226)) @ X1227|(fheapIm1091024090Down_a @ (ft_a @ X1227 @ (ft_a @ X1224 @ X1225 @ X1226) @ (ft_a @ X1221 @ X1222 @ X1223)))=(ft_a @ X1227 @ (ft_a @ X1224 @ X1225 @ X1226) @ (ft_a @ X1221 @ X1222 @ X1223))|~ford_less_eq_a @ (fval_a @ (ft_a @ X1221 @ X1222 @ X1223)) @ (fval_a @ (ft_a @ X1224 @ X1225 @ X1226))|~epred1_0)&(ford_less_eq_a @ (fval_a @ (ft_a @ X1224 @ X1225 @ X1226)) @ X1227|(fheapIm1091024090Down_a @ (ft_a @ X1227 @ (ft_a @ X1224 @ X1225 @ X1226) @ (ft_a @ X1221 @ X1222 @ X1223)))=(ft_a @ (fval_a @ (ft_a @ X1224 @ X1225 @ X1226)) @ (fheapIm1091024090Down_a @ (ft_a @ X1227 @ (fheapIm1140443833left_a @ (ft_a @ X1224 @ X1225 @ X1226)) @ (fheapIm1257206334ight_a @ (ft_a @ X1224 @ X1225 @ X1226)))) @ (ft_a @ X1221 @ X1222 @ X1223))|~ford_less_eq_a @ (fval_a @ (ft_a @ X1221 @ X1222 @ X1223)) @ (fval_a @ (ft_a @ X1224 @ X1225 @ X1226))|~epred1_0))&((~ford_less_eq_a @ (fval_a @ (ft_a @ X1221 @ X1222 @ X1223)) @ X1227|(fheapIm1091024090Down_a @ (ft_a @ X1227 @ (ft_a @ X1224 @ X1225 @ X1226) @ (ft_a @ X1221 @ X1222 @ X1223)))=(ft_a @ X1227 @ (ft_a @ X1224 @ X1225 @ X1226) @ (ft_a @ X1221 @ X1222 @ X1223))|ford_less_eq_a @ (fval_a @ (ft_a @ X1221 @ X1222 @ X1223)) @ (fval_a @ (ft_a @ X1224 @ X1225 @ X1226))|~epred1_0)&(ford_less_eq_a @ (fval_a @ (ft_a @ X1221 @ X1222 @ X1223)) @ X1227|(fheapIm1091024090Down_a @ (ft_a @ X1227 @ (ft_a @ X1224 @ X1225 @ X1226) @ (ft_a @ X1221 @ X1222 @ X1223)))=(ft_a @ (fval_a @ (ft_a @ X1221 @ X1222 @ X1223)) @ (ft_a @ X1224 @ X1225 @ X1226) @ (fheapIm1091024090Down_a @ (ft_a @ X1227 @ (fheapIm1140443833left_a @ (ft_a @ X1221 @ X1222 @ X1223)) @ (fheapIm1257206334ight_a @ (ft_a @ X1221 @ X1222 @ X1223)))))|ford_less_eq_a @ (fval_a @ (ft_a @ X1221 @ X1222 @ X1223)) @ (fval_a @ (ft_a @ X1224 @ X1225 @ X1226))|~epred1_0))), inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[c_0_15])])])])])).
% 1.08/1.29 thf(c_0_22, plain, (epred1_0|~p23), inference(split_conjunct,[status(thm)],[c_0_16])).
% 1.08/1.29 thf(c_0_23, plain, p23, inference(split_conjunct,[status(thm)],[ax77])).
% 1.08/1.29 thf(c_0_24, plain, ![X4:tree_a, X3:tree_a, X1:a]:((fval_a @ (ft_a @ X1 @ X3 @ X4))=(X1)|~p22), inference(split_conjunct,[status(thm)],[c_0_17])).
% 1.08/1.29 thf(c_0_25, plain, p22, inference(split_conjunct,[status(thm)],[ax78])).
% 1.08/1.29 thf(c_0_26, plain, (~p2|ford_less_eq_a @ fv1 @ fv), inference(fof_nnf,[status(thm)],[pax2])).
% 1.08/1.29 thf(c_0_27, plain, (~p1|ford_less_eq_a @ fv2 @ fv1), inference(fof_nnf,[status(thm)],[pax1])).
% 1.08/1.29 thf(c_0_28, plain, (p40|(fheapIm1091024090Down_a @ (ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)))!=(ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2))), inference(split_conjunct,[status(thm)],[c_0_18])).
% 1.08/1.29 thf(c_0_29, plain, ~p40, inference(sr,[status(thm)],[c_0_19, c_0_20])).
% 1.08/1.29 thf(c_0_30, plain, ![X2:a, X1:a, X3:tree_a, X7:tree_a, X6:tree_a, X5:a, X4:tree_a]:((fheapIm1091024090Down_a @ (ft_a @ X2 @ (ft_a @ X1 @ X3 @ X4) @ (ft_a @ X5 @ X6 @ X7)))=(ft_a @ X2 @ (ft_a @ X1 @ X3 @ X4) @ (ft_a @ X5 @ X6 @ X7))|~ford_less_eq_a @ (fval_a @ (ft_a @ X1 @ X3 @ X4)) @ X2|~ford_less_eq_a @ (fval_a @ (ft_a @ X5 @ X6 @ X7)) @ (fval_a @ (ft_a @ X1 @ X3 @ X4))|~epred1_0), inference(split_conjunct,[status(thm)],[c_0_21])).
% 1.08/1.29 thf(c_0_31, plain, epred1_0, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_22, c_0_23])])).
% 1.08/1.29 thf(c_0_32, plain, ![X4:tree_a, X3:tree_a, X1:a]:(fval_a @ (ft_a @ X1 @ X3 @ X4))=(X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_24, c_0_25])])).
% 1.08/1.29 thf(c_0_33, plain, (ford_less_eq_a @ fv1 @ fv|~p2), inference(split_conjunct,[status(thm)],[c_0_26])).
% 1.08/1.29 thf(c_0_34, plain, p2, inference(split_conjunct,[status(thm)],[ax98])).
% 1.08/1.29 thf(c_0_35, plain, (ford_less_eq_a @ fv2 @ fv1|~p1), inference(split_conjunct,[status(thm)],[c_0_27])).
% 1.08/1.29 thf(c_0_36, plain, p1, inference(split_conjunct,[status(thm)],[ax99])).
% 1.08/1.29 thf(c_0_37, plain, (fheapIm1091024090Down_a @ (ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)))!=(ft_a @ fv @ (ft_a @ fv1 @ fl1 @ fr1) @ (ft_a @ fv2 @ fl2 @ fr2)), inference(sr,[status(thm)],[c_0_28, c_0_29])).
% 1.08/1.29 thf(c_0_38, plain, ![X1:a, X3:tree_a, X4:tree_a, X7:tree_a, X6:tree_a, X5:a, X2:a]:((fheapIm1091024090Down_a @ (ft_a @ X1 @ (ft_a @ X2 @ X3 @ X4) @ (ft_a @ X5 @ X6 @ X7)))=(ft_a @ X1 @ (ft_a @ X2 @ X3 @ X4) @ (ft_a @ X5 @ X6 @ X7))|~ford_less_eq_a @ X2 @ X1|~ford_less_eq_a @ X5 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_30, c_0_31]), c_0_32]), c_0_32]), c_0_32])])).
% 1.08/1.29 thf(c_0_39, plain, ford_less_eq_a @ fv1 @ fv, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_33, c_0_34])])).
% 1.08/1.29 thf(c_0_40, plain, ford_less_eq_a @ fv2 @ fv1, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_35, c_0_36])])).
% 1.08/1.29 thf(c_0_41, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_38]), c_0_39]), c_0_40])]), ['proof']).
% 1.08/1.29 thf(13,plain,$false,inference(eprover,[status(thm),assumptions([h6,h4,h8,h2,h0])],[])).
% 1.08/1.29 thf(14,plain,$false,inference(tab_imp,[status(thm),assumptions([h4,h8,h2,h0]),tab_imp(discharge,[h5]),tab_imp(discharge,[h6])],[h4,12,13,h5,h6])).
% 1.08/1.29 thf(15,plain,$false,inference(tab_imp,[status(thm),assumptions([h8,h2,h0]),tab_imp(discharge,[h3]),tab_imp(discharge,[h4])],[fact_2__C5__2_Ohyps_C_I2_J,11,14,h3,h4])).
% 1.08/1.29 thf(16,plain,$false,inference(tab_imp,[status(thm),assumptions([h2,h0]),tab_imp(discharge,[h7]),tab_imp(discharge,[h8])],[h2,10,15,h7,h8])).
% 1.08/1.29 thf(fact_3__C5__2_Ohyps_C_I1_J,axiom,(sP1 => ((~(((ord_less_eq_a @ (val_a @ (((t_a @ v1) @ l1) @ r1))) @ v))) => ((multiset_a2 @ (heapIm1091024090Down_a @ (((t_a @ v) @ (heapIm1140443833left_a @ (((t_a @ v1) @ l1) @ r1))) @ (heapIm1257206334ight_a @ (((t_a @ v1) @ l1) @ r1))))) = (multiset_a2 @ (((t_a @ v) @ (heapIm1140443833left_a @ (((t_a @ v1) @ l1) @ r1))) @ (heapIm1257206334ight_a @ (((t_a @ v1) @ l1) @ r1)))))))).
% 1.08/1.29 thf(17,plain,$false,inference(tab_imp,[status(thm),assumptions([h0]),tab_imp(discharge,[h1]),tab_imp(discharge,[h2])],[fact_3__C5__2_Ohyps_C_I1_J,5,16,h1,h2])).
% 1.08/1.29 thf(0,theorem,((multiset_a2 @ (heapIm1091024090Down_a @ (((t_a @ v) @ (((t_a @ v1) @ l1) @ r1)) @ (((t_a @ v2) @ l2) @ r2)))) = (multiset_a2 @ (((t_a @ v) @ (((t_a @ v1) @ l1) @ r1)) @ (((t_a @ v2) @ l2) @ r2)))),inference(contra,[status(thm),contra(discharge,[h0])],[17,h0])).
% 1.08/1.29 % SZS output end Proof
%------------------------------------------------------------------------------