%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP033^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 : n021.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:46 PM UTC 2025
% Result : Theorem 0.89s 1.09s
% Output : Proof 0.89s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.15 % Problem : ITP033^1 : TPTP v9.2.0. Released v7.5.0.
% 0.08/0.16 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.13/0.37 % Computer : n021.cluster.edu
% 0.13/0.37 % Model : x86_64 x86_64
% 0.13/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.37 % Memory : 8042.1875MB
% 0.13/0.37 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.37 % CPULimit : 300
% 0.13/0.37 % WCLimit : 300
% 0.13/0.37 % DateTime : Wed Oct 8 17:56:23 EDT 2025
% 0.13/0.38 % CPUTime :
% 0.89/1.09 % SZS status Theorem
% 0.89/1.09 % Mode: mode507:USE_SINE=true:SINE_TOLERANCE=3.0:SINE_GENERALITY_THRESHOLD=0:SINE_RANK_LIMIT=1.:SINE_DEPTH=1
% 0.89/1.09 % Inferences: 229
% 0.89/1.09 % SZS output start Proof
% 0.89/1.09 thf(ty_a, type, a : $tType).
% 0.89/1.09 thf(ty_binary1439146945Tree_a, type, binary1439146945Tree_a : $tType).
% 0.89/1.09 thf(ty_int, type, int : $tType).
% 0.89/1.09 thf(ty_h, type, h : (a>int)).
% 0.89/1.09 thf(ty_binary476621312_Tip_a, type, binary476621312_Tip_a : binary1439146945Tree_a).
% 0.89/1.09 thf(ty_binary1721989714Tree_a, type, binary1721989714Tree_a : ((a>int)>binary1439146945Tree_a>$o)).
% 0.89/1.09 thf(ty_t2, type, t2 : binary1439146945Tree_a).
% 0.89/1.09 thf(ty_binary717961607le_T_a, type, binary717961607le_T_a : (binary1439146945Tree_a>a>binary1439146945Tree_a>binary1439146945Tree_a)).
% 0.89/1.09 thf(ty_binary1217730267_wrm_a, type, binary1217730267_wrm_a : ((a>int)>binary1439146945Tree_a>binary1439146945Tree_a)).
% 0.89/1.09 thf(ty_t1, type, t1 : binary1439146945Tree_a).
% 0.89/1.09 thf(ty_x, type, x : a).
% 0.89/1.09 thf(sP1,plain,sP1 <=> ((binary1721989714Tree_a @ h) @ t2),introduced(definition,[new_symbols(definition,[sP1])])).
% 0.89/1.09 thf(sP2,plain,sP2 <=> (![X1:a>int]:((binary1721989714Tree_a @ X1) @ binary476621312_Tip_a)),introduced(definition,[new_symbols(definition,[sP2])])).
% 0.89/1.09 thf(sP3,plain,sP3 <=> (((binary1721989714Tree_a @ h) @ (((binary717961607le_T_a @ t1) @ x) @ t2)) => ((binary1721989714Tree_a @ h) @ t1)),introduced(definition,[new_symbols(definition,[sP3])])).
% 0.89/1.09 thf(sP4,plain,sP4 <=> ((binary1721989714Tree_a @ h) @ binary476621312_Tip_a),introduced(definition,[new_symbols(definition,[sP4])])).
% 0.89/1.09 thf(sP5,plain,sP5 <=> (![X1:binary1439146945Tree_a]:(((binary1721989714Tree_a @ h) @ (((binary717961607le_T_a @ t1) @ x) @ X1)) => ((binary1721989714Tree_a @ h) @ t1))),introduced(definition,[new_symbols(definition,[sP5])])).
% 0.89/1.09 thf(sP6,plain,sP6 <=> (![X1:a]:(![X2:binary1439146945Tree_a]:(((binary1721989714Tree_a @ h) @ (((binary717961607le_T_a @ t1) @ X1) @ X2)) => ((binary1721989714Tree_a @ h) @ t1)))),introduced(definition,[new_symbols(definition,[sP6])])).
% 0.89/1.09 thf(sP7,plain,sP7 <=> (![X1:binary1439146945Tree_a]:(![X2:a]:(![X3:binary1439146945Tree_a]:(((binary1721989714Tree_a @ h) @ (((binary717961607le_T_a @ X1) @ X2) @ X3)) => ((binary1721989714Tree_a @ h) @ X3))))),introduced(definition,[new_symbols(definition,[sP7])])).
% 0.89/1.09 thf(sP8,plain,sP8 <=> ((binary1721989714Tree_a @ h) @ t1),introduced(definition,[new_symbols(definition,[sP8])])).
% 0.89/1.09 thf(sP9,plain,sP9 <=> (![X1:a>int]:(![X2:binary1439146945Tree_a]:(![X3:a]:(![X4:binary1439146945Tree_a]:(((binary1721989714Tree_a @ X1) @ (((binary717961607le_T_a @ X2) @ X3) @ X4)) => ((binary1721989714Tree_a @ X1) @ X2)))))),introduced(definition,[new_symbols(definition,[sP9])])).
% 0.89/1.09 thf(sP10,plain,sP10 <=> (((binary1721989714Tree_a @ h) @ (((binary717961607le_T_a @ t1) @ x) @ t2)) => sP1),introduced(definition,[new_symbols(definition,[sP10])])).
% 0.89/1.09 thf(sP11,plain,sP11 <=> ((binary1721989714Tree_a @ h) @ (((binary717961607le_T_a @ t1) @ x) @ t2)),introduced(definition,[new_symbols(definition,[sP11])])).
% 0.89/1.09 thf(sP12,plain,sP12 <=> (![X1:binary1439146945Tree_a]:(((binary1721989714Tree_a @ h) @ (((binary717961607le_T_a @ t1) @ x) @ X1)) => ((binary1721989714Tree_a @ h) @ X1))),introduced(definition,[new_symbols(definition,[sP12])])).
% 0.89/1.09 thf(sP13,plain,sP13 <=> (![X1:a>int]:(![X2:binary1439146945Tree_a]:(![X3:a]:(![X4:binary1439146945Tree_a]:(((binary1721989714Tree_a @ X1) @ (((binary717961607le_T_a @ X2) @ X3) @ X4)) => ((binary1721989714Tree_a @ X1) @ X4)))))),introduced(definition,[new_symbols(definition,[sP13])])).
% 0.89/1.09 thf(sP14,plain,sP14 <=> (![X1:binary1439146945Tree_a]:(![X2:a]:(![X3:binary1439146945Tree_a]:(((binary1721989714Tree_a @ h) @ (((binary717961607le_T_a @ X1) @ X2) @ X3)) => ((binary1721989714Tree_a @ h) @ X1))))),introduced(definition,[new_symbols(definition,[sP14])])).
% 0.89/1.09 thf(sP15,plain,sP15 <=> (![X1:a]:(![X2:binary1439146945Tree_a]:(((binary1721989714Tree_a @ h) @ (((binary717961607le_T_a @ t1) @ X1) @ X2)) => ((binary1721989714Tree_a @ h) @ X2)))),introduced(definition,[new_symbols(definition,[sP15])])).
% 0.89/1.09 thf(conj_0,conjecture,sP8).
% 0.89/1.09 thf(h0,negated_conjecture,(~(sP8)),inference(assume_negation,[status(cth)],[conj_0])).
% 0.89/1.09 thf(h1,assumption,((~((binary476621312_Tip_a = binary476621312_Tip_a))) => (~(sP4))),introduced(assumption,[])).
% 0.89/1.09 thf(h2,assumption,((binary1721989714Tree_a @ h) @ ((binary1217730267_wrm_a @ h) @ binary476621312_Tip_a)),introduced(assumption,[])).
% 0.89/1.09 thf(h3,assumption,(binary476621312_Tip_a = binary476621312_Tip_a),introduced(assumption,[])).
% 0.89/1.09 thf(h4,assumption,(~(sP4)),introduced(assumption,[])).
% 0.89/1.09 thf(h5,assumption,((~((t2 = binary476621312_Tip_a))) => (~(sP1))),introduced(assumption,[])).
% 0.89/1.09 thf(h6,assumption,((binary1721989714Tree_a @ h) @ ((binary1217730267_wrm_a @ h) @ t2)),introduced(assumption,[])).
% 0.89/1.09 thf(h7,assumption,(t2 = binary476621312_Tip_a),introduced(assumption,[])).
% 0.89/1.09 thf(h8,assumption,(~(sP1)),introduced(assumption,[])).
% 0.89/1.09 thf(h9,assumption,((~((t1 = binary476621312_Tip_a))) => (~(sP8))),introduced(assumption,[])).
% 0.89/1.09 thf(h10,assumption,((binary1721989714Tree_a @ h) @ ((binary1217730267_wrm_a @ h) @ t1)),introduced(assumption,[])).
% 0.89/1.09 thf(h11,assumption,(t1 = binary476621312_Tip_a),introduced(assumption,[])).
% 0.89/1.09 thf(h12,assumption,(~(sP8)),introduced(assumption,[])).
% 0.89/1.09 thf(pax8, axiom, (p8=>(ft2)=(fbinary476621312_Tip_a)), file('<stdin>', pax8)).
% 0.89/1.09 thf(pax6, axiom, (p6=>(ft1)=(fbinary476621312_Tip_a)), file('<stdin>', pax6)).
% 0.89/1.09 thf(ax13, axiom, p8, file('<stdin>', ax13)).
% 0.89/1.09 thf(nax13, axiom, (p13<=fbinary1721989714Tree_a @ fh @ ft1), file('<stdin>', nax13)).
% 0.89/1.09 thf(ax15, axiom, p6, file('<stdin>', ax15)).
% 0.89/1.09 thf(ax8, axiom, ~(p13), file('<stdin>', ax8)).
% 0.89/1.09 thf(pax7, axiom, (p7=>![X4:a > int]:fbinary1721989714Tree_a @ X4 @ fbinary476621312_Tip_a), file('<stdin>', pax7)).
% 0.89/1.09 thf(ax14, axiom, p7, file('<stdin>', ax14)).
% 0.89/1.09 thf(c_0_8, plain, (~p8|(ft2)=(fbinary476621312_Tip_a)), inference(fof_nnf,[status(thm)],[pax8])).
% 0.89/1.09 thf(c_0_9, plain, (~p6|(ft1)=(fbinary476621312_Tip_a)), inference(fof_nnf,[status(thm)],[pax6])).
% 0.89/1.09 thf(c_0_10, plain, ((ft2)=(fbinary476621312_Tip_a)|~p8), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.89/1.09 thf(c_0_11, plain, p8, inference(split_conjunct,[status(thm)],[ax13])).
% 0.89/1.09 thf(c_0_12, plain, (~fbinary1721989714Tree_a @ fh @ ft1|p13), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax13])])).
% 0.89/1.09 thf(c_0_13, plain, ((ft1)=(fbinary476621312_Tip_a)|~p6), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.89/1.09 thf(c_0_14, plain, (fbinary476621312_Tip_a)=(ft2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_10, c_0_11])])).
% 0.89/1.09 thf(c_0_15, plain, p6, inference(split_conjunct,[status(thm)],[ax15])).
% 0.89/1.09 thf(c_0_16, plain, ~p13, inference(fof_simplification,[status(thm)],[ax8])).
% 0.89/1.09 thf(c_0_17, plain, ![X32:a > int]:(~p7|fbinary1721989714Tree_a @ X32 @ fbinary476621312_Tip_a), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax7])])])).
% 0.89/1.09 thf(c_0_18, plain, (p13|~fbinary1721989714Tree_a @ fh @ ft1), inference(split_conjunct,[status(thm)],[c_0_12])).
% 0.89/1.09 thf(c_0_19, plain, (ft1)=(ft2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_13, c_0_14]), c_0_15])])).
% 0.89/1.09 thf(c_0_20, plain, ~p13, inference(split_conjunct,[status(thm)],[c_0_16])).
% 0.89/1.09 thf(c_0_21, plain, ![X1:a > int]:(fbinary1721989714Tree_a @ X1 @ fbinary476621312_Tip_a|~p7), inference(split_conjunct,[status(thm)],[c_0_17])).
% 0.89/1.09 thf(c_0_22, plain, p7, inference(split_conjunct,[status(thm)],[ax14])).
% 0.89/1.09 thf(c_0_23, plain, ~fbinary1721989714Tree_a @ fh @ ft2, inference(sr,[status(thm)],[inference(rw,[status(thm)],[c_0_18, c_0_19]), c_0_20])).
% 0.89/1.09 thf(c_0_24, plain, ![X1:a > int]:fbinary1721989714Tree_a @ X1 @ ft2, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_21, c_0_14]), c_0_22])])).
% 0.89/1.09 thf(c_0_25, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_23, c_0_24])]), ['proof']).
% 0.89/1.09 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h11,h9,h7,h5,h3,h1,h0])],[])).
% 0.89/1.09 thf(pax3, axiom, (p3=>![X6:a > int, X7:binary1439146945Tree_a, X8:a, X9:binary1439146945Tree_a]:(fbinary1721989714Tree_a @ X6 @ (fbinary717961607le_T_a @ X7 @ X8 @ X9)=>fbinary1721989714Tree_a @ X6 @ X7)), file('<stdin>', pax3)).
% 0.89/1.09 thf(pax1, axiom, (p1=>fbinary1721989714Tree_a @ fh @ (fbinary717961607le_T_a @ ft1 @ fx @ ft2)), file('<stdin>', pax1)).
% 0.89/1.09 thf(nax13, axiom, (p13<=fbinary1721989714Tree_a @ fh @ ft1), file('<stdin>', nax13)).
% 0.89/1.09 thf(ax21, axiom, ~(p13), file('<stdin>', ax21)).
% 0.89/1.09 thf(ax24, axiom, p3, file('<stdin>', ax24)).
% 0.89/1.09 thf(ax26, axiom, p1, file('<stdin>', ax26)).
% 0.89/1.09 thf(c_0_6, plain, ![X68:a > int, X69:binary1439146945Tree_a, X70:a, X71:binary1439146945Tree_a]:(~p3|(~fbinary1721989714Tree_a @ X68 @ (fbinary717961607le_T_a @ X69 @ X70 @ X71)|fbinary1721989714Tree_a @ X68 @ X69)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax3])])])).
% 0.89/1.09 thf(c_0_7, plain, (~p1|fbinary1721989714Tree_a @ fh @ (fbinary717961607le_T_a @ ft1 @ fx @ ft2)), inference(fof_nnf,[status(thm)],[pax1])).
% 0.89/1.09 thf(c_0_8, plain, (~fbinary1721989714Tree_a @ fh @ ft1|p13), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax13])])).
% 0.89/1.09 thf(c_0_9, plain, ~p13, inference(fof_simplification,[status(thm)],[ax21])).
% 0.89/1.09 thf(c_0_10, plain, ![X1:binary1439146945Tree_a, X8:a, X3:a > int, X2:binary1439146945Tree_a]:(fbinary1721989714Tree_a @ X3 @ X1|~p3|~fbinary1721989714Tree_a @ X3 @ (fbinary717961607le_T_a @ X1 @ X8 @ X2)), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.89/1.09 thf(c_0_11, plain, p3, inference(split_conjunct,[status(thm)],[ax24])).
% 0.89/1.09 thf(c_0_12, plain, (fbinary1721989714Tree_a @ fh @ (fbinary717961607le_T_a @ ft1 @ fx @ ft2)|~p1), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.89/1.09 thf(c_0_13, plain, p1, inference(split_conjunct,[status(thm)],[ax26])).
% 0.89/1.09 thf(c_0_14, plain, (p13|~fbinary1721989714Tree_a @ fh @ ft1), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.89/1.09 thf(c_0_15, plain, ~p13, inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.89/1.09 thf(c_0_16, plain, ![X1:binary1439146945Tree_a, X8:a, X3:a > int, X2:binary1439146945Tree_a]:(fbinary1721989714Tree_a @ X3 @ X1|~fbinary1721989714Tree_a @ X3 @ (fbinary717961607le_T_a @ X1 @ X8 @ X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_10, c_0_11])])).
% 0.89/1.09 thf(c_0_17, plain, fbinary1721989714Tree_a @ fh @ (fbinary717961607le_T_a @ ft1 @ fx @ ft2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_12, c_0_13])])).
% 0.89/1.09 thf(c_0_18, plain, ~fbinary1721989714Tree_a @ fh @ ft1, inference(sr,[status(thm)],[c_0_14, c_0_15])).
% 0.89/1.09 thf(c_0_19, plain, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_16, c_0_17]), c_0_18]), ['proof']).
% 0.89/1.09 thf(2,plain,$false,inference(eprover,[status(thm),assumptions([h12,h9,h7,h5,h3,h1,h0])],[])).
% 0.89/1.09 thf(3,plain,$false,inference(tab_imp,[status(thm),assumptions([h9,h7,h5,h3,h1,h0]),tab_imp(discharge,[h11]),tab_imp(discharge,[h12])],[h9,1,2,h11,h12])).
% 0.89/1.09 thf(pax3, axiom, (p3=>![X8:a > int, X9:binary1439146945Tree_a, X10:a, X11:binary1439146945Tree_a]:(fbinary1721989714Tree_a @ X8 @ (fbinary717961607le_T_a @ X9 @ X10 @ X11)=>fbinary1721989714Tree_a @ X8 @ X9)), file('<stdin>', pax3)).
% 0.89/1.09 thf(pax1, axiom, (p1=>fbinary1721989714Tree_a @ fh @ (fbinary717961607le_T_a @ ft1 @ fx @ ft2)), file('<stdin>', pax1)).
% 0.89/1.09 thf(nax13, axiom, (p13<=fbinary1721989714Tree_a @ fh @ ft1), file('<stdin>', nax13)).
% 0.89/1.09 thf(ax26, axiom, ~(p13), file('<stdin>', ax26)).
% 0.89/1.09 thf(ax36, axiom, p3, file('<stdin>', ax36)).
% 0.89/1.09 thf(ax38, axiom, p1, file('<stdin>', ax38)).
% 0.89/1.09 thf(c_0_6, plain, ![X76:a > int, X77:binary1439146945Tree_a, X78:a, X79:binary1439146945Tree_a]:(~p3|(~fbinary1721989714Tree_a @ X76 @ (fbinary717961607le_T_a @ X77 @ X78 @ X79)|fbinary1721989714Tree_a @ X76 @ X77)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax3])])])).
% 0.89/1.09 thf(c_0_7, plain, (~p1|fbinary1721989714Tree_a @ fh @ (fbinary717961607le_T_a @ ft1 @ fx @ ft2)), inference(fof_nnf,[status(thm)],[pax1])).
% 0.89/1.09 thf(c_0_8, plain, (~fbinary1721989714Tree_a @ fh @ ft1|p13), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax13])])).
% 0.89/1.09 thf(c_0_9, plain, ~p13, inference(fof_simplification,[status(thm)],[ax26])).
% 0.89/1.09 thf(c_0_10, plain, ![X1:binary1439146945Tree_a, X2:a > int, X10:a, X3:binary1439146945Tree_a]:(fbinary1721989714Tree_a @ X2 @ X1|~p3|~fbinary1721989714Tree_a @ X2 @ (fbinary717961607le_T_a @ X1 @ X10 @ X3)), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.89/1.09 thf(c_0_11, plain, p3, inference(split_conjunct,[status(thm)],[ax36])).
% 0.89/1.09 thf(c_0_12, plain, (fbinary1721989714Tree_a @ fh @ (fbinary717961607le_T_a @ ft1 @ fx @ ft2)|~p1), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.89/1.09 thf(c_0_13, plain, p1, inference(split_conjunct,[status(thm)],[ax38])).
% 0.89/1.09 thf(c_0_14, plain, (p13|~fbinary1721989714Tree_a @ fh @ ft1), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.89/1.09 thf(c_0_15, plain, ~p13, inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.89/1.09 thf(c_0_16, plain, ![X1:binary1439146945Tree_a, X2:a > int, X10:a, X3:binary1439146945Tree_a]:(fbinary1721989714Tree_a @ X2 @ X1|~fbinary1721989714Tree_a @ X2 @ (fbinary717961607le_T_a @ X1 @ X10 @ X3)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_10, c_0_11])])).
% 0.89/1.09 thf(c_0_17, plain, fbinary1721989714Tree_a @ fh @ (fbinary717961607le_T_a @ ft1 @ fx @ ft2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_12, c_0_13])])).
% 0.89/1.09 thf(c_0_18, plain, ~fbinary1721989714Tree_a @ fh @ ft1, inference(sr,[status(thm)],[c_0_14, c_0_15])).
% 0.89/1.09 thf(c_0_19, plain, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_16, c_0_17]), c_0_18]), ['proof']).
% 0.89/1.09 thf(4,plain,$false,inference(eprover,[status(thm),assumptions([h10,h7,h5,h3,h1,h0])],[])).
% 0.89/1.09 thf(fact_7_h1,axiom,((~(((~((t1 = binary476621312_Tip_a))) => (~(sP8))))) => ((binary1721989714Tree_a @ h) @ ((binary1217730267_wrm_a @ h) @ t1)))).
% 0.89/1.09 thf(5,plain,$false,inference(tab_imp,[status(thm),assumptions([h7,h5,h3,h1,h0]),tab_imp(discharge,[h9]),tab_imp(discharge,[h10])],[fact_7_h1,3,4,h9,h10])).
% 0.89/1.09 thf(pax6, axiom, (p6=>(ft1)=(fbinary476621312_Tip_a)), file('<stdin>', pax6)).
% 0.89/1.09 thf(nax13, axiom, (p13<=fbinary1721989714Tree_a @ fh @ ft1), file('<stdin>', nax13)).
% 0.89/1.09 thf(ax32, axiom, ~(p13), file('<stdin>', ax32)).
% 0.89/1.09 thf(pax7, axiom, (p7=>![X10:a > int]:fbinary1721989714Tree_a @ X10 @ fbinary476621312_Tip_a), file('<stdin>', pax7)).
% 0.89/1.09 thf(ax39, axiom, p6, file('<stdin>', ax39)).
% 0.89/1.09 thf(ax38, axiom, p7, file('<stdin>', ax38)).
% 0.89/1.09 thf(c_0_6, plain, (~p6|(ft1)=(fbinary476621312_Tip_a)), inference(fof_nnf,[status(thm)],[pax6])).
% 0.89/1.09 thf(c_0_7, plain, (~fbinary1721989714Tree_a @ fh @ ft1|p13), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax13])])).
% 0.89/1.09 thf(c_0_8, plain, ~p13, inference(fof_simplification,[status(thm)],[ax32])).
% 0.89/1.09 thf(c_0_9, plain, ![X80:a > int]:(~p7|fbinary1721989714Tree_a @ X80 @ fbinary476621312_Tip_a), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax7])])])).
% 0.89/1.09 thf(c_0_10, plain, ((ft1)=(fbinary476621312_Tip_a)|~p6), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.89/1.09 thf(c_0_11, plain, p6, inference(split_conjunct,[status(thm)],[ax39])).
% 0.89/1.09 thf(c_0_12, plain, (p13|~fbinary1721989714Tree_a @ fh @ ft1), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.89/1.09 thf(c_0_13, plain, ~p13, inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.89/1.09 thf(c_0_14, plain, ![X4:a > int]:(fbinary1721989714Tree_a @ X4 @ fbinary476621312_Tip_a|~p7), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.89/1.09 thf(c_0_15, plain, (fbinary476621312_Tip_a)=(ft1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_10, c_0_11])])).
% 0.89/1.09 thf(c_0_16, plain, p7, inference(split_conjunct,[status(thm)],[ax38])).
% 0.89/1.09 thf(c_0_17, plain, ~fbinary1721989714Tree_a @ fh @ ft1, inference(sr,[status(thm)],[c_0_12, c_0_13])).
% 0.89/1.09 thf(c_0_18, plain, ![X4:a > int]:fbinary1721989714Tree_a @ X4 @ ft1, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_14, c_0_15]), c_0_16])])).
% 0.89/1.09 thf(c_0_19, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_17, c_0_18])]), ['proof']).
% 0.89/1.09 thf(6,plain,$false,inference(eprover,[status(thm),assumptions([h11,h9,h8,h5,h3,h1,h0])],[])).
% 0.89/1.09 thf(7,plain,(~(sP14) | sP6),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(8,plain,(~(sP6) | sP5),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(9,plain,(~(sP5) | sP3),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(10,plain,((~(sP3) | ~(sP11)) | sP8),inference(prop_rule,[status(thm)],[])).
% 0.89/1.09 thf(11,plain,(~(sP9) | sP14),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(fact_3_sortLemmaL,axiom,sP9).
% 0.89/1.09 thf(fact_1_s,axiom,sP11).
% 0.89/1.09 thf(12,plain,$false,inference(prop_unsat,[status(thm),assumptions([h12,h9,h8,h5,h3,h1,h0])],[7,8,9,10,11,h12,fact_3_sortLemmaL,fact_1_s])).
% 0.89/1.09 thf(13,plain,$false,inference(tab_imp,[status(thm),assumptions([h9,h8,h5,h3,h1,h0]),tab_imp(discharge,[h11]),tab_imp(discharge,[h12])],[h9,6,12,h11,h12])).
% 0.89/1.09 thf(pax4, axiom, (p4=>![X12:a > int, X13:binary1439146945Tree_a, X14:a, X15:binary1439146945Tree_a]:(fbinary1721989714Tree_a @ X12 @ (fbinary717961607le_T_a @ X13 @ X14 @ X15)=>fbinary1721989714Tree_a @ X12 @ X15)), file('<stdin>', pax4)).
% 0.89/1.09 thf(pax1, axiom, (p1=>fbinary1721989714Tree_a @ fh @ (fbinary717961607le_T_a @ ft1 @ fx @ ft2)), file('<stdin>', pax1)).
% 0.89/1.09 thf(nax43, axiom, (p43<=fbinary1721989714Tree_a @ fh @ ft2), file('<stdin>', nax43)).
% 0.89/1.09 thf(ax36, axiom, ~(p43), file('<stdin>', ax36)).
% 0.89/1.09 thf(ax40, axiom, p4, file('<stdin>', ax40)).
% 0.89/1.09 thf(ax43, axiom, p1, file('<stdin>', ax43)).
% 0.89/1.09 thf(c_0_6, plain, ![X100:a > int, X101:binary1439146945Tree_a, X102:a, X103:binary1439146945Tree_a]:(~p4|(~fbinary1721989714Tree_a @ X100 @ (fbinary717961607le_T_a @ X101 @ X102 @ X103)|fbinary1721989714Tree_a @ X100 @ X103)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax4])])])).
% 0.89/1.09 thf(c_0_7, plain, (~p1|fbinary1721989714Tree_a @ fh @ (fbinary717961607le_T_a @ ft1 @ fx @ ft2)), inference(fof_nnf,[status(thm)],[pax1])).
% 0.89/1.09 thf(c_0_8, plain, (~fbinary1721989714Tree_a @ fh @ ft2|p43), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax43])])).
% 0.89/1.09 thf(c_0_9, plain, ~p43, inference(fof_simplification,[status(thm)],[ax36])).
% 0.89/1.09 thf(c_0_10, plain, ![X1:a, X2:binary1439146945Tree_a, X6:a > int, X3:binary1439146945Tree_a]:(fbinary1721989714Tree_a @ X6 @ X3|~p4|~fbinary1721989714Tree_a @ X6 @ (fbinary717961607le_T_a @ X2 @ X1 @ X3)), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.89/1.09 thf(c_0_11, plain, p4, inference(split_conjunct,[status(thm)],[ax40])).
% 0.89/1.09 thf(c_0_12, plain, (fbinary1721989714Tree_a @ fh @ (fbinary717961607le_T_a @ ft1 @ fx @ ft2)|~p1), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.89/1.09 thf(c_0_13, plain, p1, inference(split_conjunct,[status(thm)],[ax43])).
% 0.89/1.09 thf(c_0_14, plain, (p43|~fbinary1721989714Tree_a @ fh @ ft2), inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.89/1.09 thf(c_0_15, plain, ~p43, inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.89/1.09 thf(c_0_16, plain, ![X1:a, X6:a > int, X3:binary1439146945Tree_a, X2:binary1439146945Tree_a]:(fbinary1721989714Tree_a @ X6 @ X2|~fbinary1721989714Tree_a @ X6 @ (fbinary717961607le_T_a @ X3 @ X1 @ X2)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_10, c_0_11])])).
% 0.89/1.09 thf(c_0_17, plain, fbinary1721989714Tree_a @ fh @ (fbinary717961607le_T_a @ ft1 @ fx @ ft2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_12, c_0_13])])).
% 0.89/1.09 thf(c_0_18, plain, ~fbinary1721989714Tree_a @ fh @ ft2, inference(sr,[status(thm)],[c_0_14, c_0_15])).
% 0.89/1.09 thf(c_0_19, plain, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_16, c_0_17]), c_0_18]), ['proof']).
% 0.89/1.09 thf(14,plain,$false,inference(eprover,[status(thm),assumptions([h10,h8,h5,h3,h1,h0])],[])).
% 0.89/1.09 thf(15,plain,$false,inference(tab_imp,[status(thm),assumptions([h8,h5,h3,h1,h0]),tab_imp(discharge,[h9]),tab_imp(discharge,[h10])],[fact_7_h1,13,14,h9,h10])).
% 0.89/1.09 thf(16,plain,$false,inference(tab_imp,[status(thm),assumptions([h5,h3,h1,h0]),tab_imp(discharge,[h7]),tab_imp(discharge,[h8])],[h5,5,15,h7,h8])).
% 0.89/1.09 thf(pax6, axiom, (p6=>(ft1)=(fbinary476621312_Tip_a)), file('<stdin>', pax6)).
% 0.89/1.09 thf(nax13, axiom, (p13<=fbinary1721989714Tree_a @ fh @ ft1), file('<stdin>', nax13)).
% 0.89/1.09 thf(ax44, axiom, ~(p13), file('<stdin>', ax44)).
% 0.89/1.09 thf(pax7, axiom, (p7=>![X14:a > int]:fbinary1721989714Tree_a @ X14 @ fbinary476621312_Tip_a), file('<stdin>', pax7)).
% 0.89/1.09 thf(ax51, axiom, p6, file('<stdin>', ax51)).
% 0.89/1.09 thf(ax50, axiom, p7, file('<stdin>', ax50)).
% 0.89/1.09 thf(c_0_6, plain, (~p6|(ft1)=(fbinary476621312_Tip_a)), inference(fof_nnf,[status(thm)],[pax6])).
% 0.89/1.09 thf(c_0_7, plain, (~fbinary1721989714Tree_a @ fh @ ft1|p13), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax13])])).
% 0.89/1.09 thf(c_0_8, plain, ~p13, inference(fof_simplification,[status(thm)],[ax44])).
% 0.89/1.09 thf(c_0_9, plain, ![X100:a > int]:(~p7|fbinary1721989714Tree_a @ X100 @ fbinary476621312_Tip_a), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax7])])])).
% 0.89/1.09 thf(c_0_10, plain, ((ft1)=(fbinary476621312_Tip_a)|~p6), inference(split_conjunct,[status(thm)],[c_0_6])).
% 0.89/1.09 thf(c_0_11, plain, p6, inference(split_conjunct,[status(thm)],[ax51])).
% 0.89/1.09 thf(c_0_12, plain, (p13|~fbinary1721989714Tree_a @ fh @ ft1), inference(split_conjunct,[status(thm)],[c_0_7])).
% 0.89/1.09 thf(c_0_13, plain, ~p13, inference(split_conjunct,[status(thm)],[c_0_8])).
% 0.89/1.09 thf(c_0_14, plain, ![X8:a > int]:(fbinary1721989714Tree_a @ X8 @ fbinary476621312_Tip_a|~p7), inference(split_conjunct,[status(thm)],[c_0_9])).
% 0.89/1.09 thf(c_0_15, plain, (fbinary476621312_Tip_a)=(ft1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_10, c_0_11])])).
% 0.89/1.09 thf(c_0_16, plain, p7, inference(split_conjunct,[status(thm)],[ax50])).
% 0.89/1.09 thf(c_0_17, plain, ~fbinary1721989714Tree_a @ fh @ ft1, inference(sr,[status(thm)],[c_0_12, c_0_13])).
% 0.89/1.09 thf(c_0_18, plain, ![X8:a > int]:fbinary1721989714Tree_a @ X8 @ ft1, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(rw,[status(thm)],[c_0_14, c_0_15]), c_0_16])])).
% 0.89/1.09 thf(c_0_19, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_17, c_0_18])]), ['proof']).
% 0.89/1.09 thf(17,plain,$false,inference(eprover,[status(thm),assumptions([h11,h9,h6,h3,h1,h0])],[])).
% 0.89/1.09 thf(18,plain,(~(sP9) | sP14),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(19,plain,(~(sP14) | sP6),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(20,plain,(~(sP6) | sP5),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(21,plain,(~(sP5) | sP3),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(22,plain,((~(sP3) | ~(sP11)) | sP8),inference(prop_rule,[status(thm)],[])).
% 0.89/1.09 thf(23,plain,$false,inference(prop_unsat,[status(thm),assumptions([h12,h9,h6,h3,h1,h0])],[18,19,20,21,22,h12,fact_3_sortLemmaL,fact_1_s])).
% 0.89/1.09 thf(24,plain,$false,inference(tab_imp,[status(thm),assumptions([h9,h6,h3,h1,h0]),tab_imp(discharge,[h11]),tab_imp(discharge,[h12])],[h9,17,23,h11,h12])).
% 0.89/1.09 thf(25,plain,(~(sP9) | sP14),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(26,plain,(~(sP14) | sP6),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(27,plain,(~(sP6) | sP5),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(28,plain,(~(sP5) | sP3),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(29,plain,((~(sP3) | ~(sP11)) | sP8),inference(prop_rule,[status(thm)],[])).
% 0.89/1.09 thf(30,plain,$false,inference(prop_unsat,[status(thm),assumptions([h10,h6,h3,h1,h0])],[25,26,27,28,29,h0,fact_3_sortLemmaL,fact_1_s])).
% 0.89/1.09 thf(31,plain,$false,inference(tab_imp,[status(thm),assumptions([h6,h3,h1,h0]),tab_imp(discharge,[h9]),tab_imp(discharge,[h10])],[fact_7_h1,24,30,h9,h10])).
% 0.89/1.09 thf(fact_11_h2,axiom,((~(((~((t2 = binary476621312_Tip_a))) => (~(sP1))))) => ((binary1721989714Tree_a @ h) @ ((binary1217730267_wrm_a @ h) @ t2)))).
% 0.89/1.09 thf(32,plain,$false,inference(tab_imp,[status(thm),assumptions([h3,h1,h0]),tab_imp(discharge,[h5]),tab_imp(discharge,[h6])],[fact_11_h2,16,31,h5,h6])).
% 0.89/1.09 thf(33,plain,(~(sP2) | sP4),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(fact_8_sortedTree_Osimps_I1_J,axiom,sP2).
% 0.89/1.09 thf(34,plain,$false,inference(prop_unsat,[status(thm),assumptions([h11,h9,h7,h5,h4,h1,h0])],[33,h4,fact_8_sortedTree_Osimps_I1_J])).
% 0.89/1.09 thf(35,plain,(~(sP2) | sP4),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(36,plain,$false,inference(prop_unsat,[status(thm),assumptions([h12,h9,h7,h5,h4,h1,h0])],[35,h4,fact_8_sortedTree_Osimps_I1_J])).
% 0.89/1.09 thf(37,plain,$false,inference(tab_imp,[status(thm),assumptions([h9,h7,h5,h4,h1,h0]),tab_imp(discharge,[h11]),tab_imp(discharge,[h12])],[h9,34,36,h11,h12])).
% 0.89/1.09 thf(38,plain,(~(sP2) | sP4),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(39,plain,$false,inference(prop_unsat,[status(thm),assumptions([h10,h7,h5,h4,h1,h0])],[38,h4,fact_8_sortedTree_Osimps_I1_J])).
% 0.89/1.09 thf(40,plain,$false,inference(tab_imp,[status(thm),assumptions([h7,h5,h4,h1,h0]),tab_imp(discharge,[h9]),tab_imp(discharge,[h10])],[fact_7_h1,37,39,h9,h10])).
% 0.89/1.09 thf(41,plain,(~(sP2) | sP4),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(42,plain,$false,inference(prop_unsat,[status(thm),assumptions([h11,h9,h8,h5,h4,h1,h0])],[41,h4,fact_8_sortedTree_Osimps_I1_J])).
% 0.89/1.09 thf(43,plain,(~(sP2) | sP4),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(44,plain,$false,inference(prop_unsat,[status(thm),assumptions([h12,h9,h8,h5,h4,h1,h0])],[43,h4,fact_8_sortedTree_Osimps_I1_J])).
% 0.89/1.09 thf(45,plain,$false,inference(tab_imp,[status(thm),assumptions([h9,h8,h5,h4,h1,h0]),tab_imp(discharge,[h11]),tab_imp(discharge,[h12])],[h9,42,44,h11,h12])).
% 0.89/1.09 thf(46,plain,(~(sP2) | sP4),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(47,plain,$false,inference(prop_unsat,[status(thm),assumptions([h10,h8,h5,h4,h1,h0])],[46,h4,fact_8_sortedTree_Osimps_I1_J])).
% 0.89/1.09 thf(48,plain,$false,inference(tab_imp,[status(thm),assumptions([h8,h5,h4,h1,h0]),tab_imp(discharge,[h9]),tab_imp(discharge,[h10])],[fact_7_h1,45,47,h9,h10])).
% 0.89/1.09 thf(49,plain,$false,inference(tab_imp,[status(thm),assumptions([h5,h4,h1,h0]),tab_imp(discharge,[h7]),tab_imp(discharge,[h8])],[h5,40,48,h7,h8])).
% 0.89/1.09 thf(50,plain,(~(sP2) | sP4),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(51,plain,$false,inference(prop_unsat,[status(thm),assumptions([h11,h9,h6,h4,h1,h0])],[50,h4,fact_8_sortedTree_Osimps_I1_J])).
% 0.89/1.09 thf(52,plain,(~(sP2) | sP4),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(53,plain,$false,inference(prop_unsat,[status(thm),assumptions([h12,h9,h6,h4,h1,h0])],[52,h4,fact_8_sortedTree_Osimps_I1_J])).
% 0.89/1.09 thf(54,plain,$false,inference(tab_imp,[status(thm),assumptions([h9,h6,h4,h1,h0]),tab_imp(discharge,[h11]),tab_imp(discharge,[h12])],[h9,51,53,h11,h12])).
% 0.89/1.09 thf(55,plain,(~(sP2) | sP4),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(56,plain,$false,inference(prop_unsat,[status(thm),assumptions([h10,h6,h4,h1,h0])],[55,h4,fact_8_sortedTree_Osimps_I1_J])).
% 0.89/1.09 thf(57,plain,$false,inference(tab_imp,[status(thm),assumptions([h6,h4,h1,h0]),tab_imp(discharge,[h9]),tab_imp(discharge,[h10])],[fact_7_h1,54,56,h9,h10])).
% 0.89/1.09 thf(58,plain,$false,inference(tab_imp,[status(thm),assumptions([h4,h1,h0]),tab_imp(discharge,[h5]),tab_imp(discharge,[h6])],[fact_11_h2,49,57,h5,h6])).
% 0.89/1.09 thf(59,plain,$false,inference(tab_imp,[status(thm),assumptions([h1,h0]),tab_imp(discharge,[h3]),tab_imp(discharge,[h4])],[h1,32,58,h3,h4])).
% 0.89/1.09 thf(60,plain,(~(sP9) | sP14),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(61,plain,(~(sP14) | sP6),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(62,plain,(~(sP6) | sP5),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(63,plain,(~(sP5) | sP3),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(64,plain,((~(sP3) | ~(sP11)) | sP8),inference(prop_rule,[status(thm)],[])).
% 0.89/1.09 thf(65,plain,$false,inference(prop_unsat,[status(thm),assumptions([h11,h9,h7,h5,h2,h0])],[60,61,62,63,64,h0,fact_3_sortLemmaL,fact_1_s])).
% 0.89/1.09 thf(66,plain,(~(sP9) | sP14),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(67,plain,(~(sP14) | sP6),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(68,plain,(~(sP6) | sP5),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(69,plain,(~(sP5) | sP3),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(70,plain,((~(sP3) | ~(sP11)) | sP8),inference(prop_rule,[status(thm)],[])).
% 0.89/1.09 thf(71,plain,$false,inference(prop_unsat,[status(thm),assumptions([h12,h9,h7,h5,h2,h0])],[66,67,68,69,70,h12,fact_3_sortLemmaL,fact_1_s])).
% 0.89/1.09 thf(72,plain,$false,inference(tab_imp,[status(thm),assumptions([h9,h7,h5,h2,h0]),tab_imp(discharge,[h11]),tab_imp(discharge,[h12])],[h9,65,71,h11,h12])).
% 0.89/1.09 thf(73,plain,(~(sP9) | sP14),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(74,plain,(~(sP14) | sP6),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(75,plain,(~(sP6) | sP5),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(76,plain,(~(sP5) | sP3),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(77,plain,((~(sP3) | ~(sP11)) | sP8),inference(prop_rule,[status(thm)],[])).
% 0.89/1.09 thf(78,plain,$false,inference(prop_unsat,[status(thm),assumptions([h10,h7,h5,h2,h0])],[73,74,75,76,77,h0,fact_3_sortLemmaL,fact_1_s])).
% 0.89/1.09 thf(79,plain,$false,inference(tab_imp,[status(thm),assumptions([h7,h5,h2,h0]),tab_imp(discharge,[h9]),tab_imp(discharge,[h10])],[fact_7_h1,72,78,h9,h10])).
% 0.89/1.09 thf(80,plain,(~(sP13) | sP7),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(81,plain,(~(sP7) | sP15),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(82,plain,(~(sP15) | sP12),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(83,plain,(~(sP12) | sP10),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(84,plain,((~(sP10) | ~(sP11)) | sP1),inference(prop_rule,[status(thm)],[])).
% 0.89/1.09 thf(fact_4_sortLemmaR,axiom,sP13).
% 0.89/1.09 thf(85,plain,$false,inference(prop_unsat,[status(thm),assumptions([h11,h9,h8,h5,h2,h0])],[80,81,82,83,84,h8,fact_4_sortLemmaR,fact_1_s])).
% 0.89/1.09 thf(86,plain,(~(sP13) | sP7),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(87,plain,(~(sP7) | sP15),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(88,plain,(~(sP15) | sP12),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(89,plain,(~(sP12) | sP10),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(90,plain,((~(sP10) | ~(sP11)) | sP1),inference(prop_rule,[status(thm)],[])).
% 0.89/1.09 thf(91,plain,$false,inference(prop_unsat,[status(thm),assumptions([h12,h9,h8,h5,h2,h0])],[86,87,88,89,90,h8,fact_4_sortLemmaR,fact_1_s])).
% 0.89/1.09 thf(92,plain,$false,inference(tab_imp,[status(thm),assumptions([h9,h8,h5,h2,h0]),tab_imp(discharge,[h11]),tab_imp(discharge,[h12])],[h9,85,91,h11,h12])).
% 0.89/1.09 thf(93,plain,(~(sP13) | sP7),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(94,plain,(~(sP7) | sP15),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(95,plain,(~(sP15) | sP12),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(96,plain,(~(sP12) | sP10),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(97,plain,((~(sP10) | ~(sP11)) | sP1),inference(prop_rule,[status(thm)],[])).
% 0.89/1.09 thf(98,plain,$false,inference(prop_unsat,[status(thm),assumptions([h10,h8,h5,h2,h0])],[93,94,95,96,97,h8,fact_4_sortLemmaR,fact_1_s])).
% 0.89/1.09 thf(99,plain,$false,inference(tab_imp,[status(thm),assumptions([h8,h5,h2,h0]),tab_imp(discharge,[h9]),tab_imp(discharge,[h10])],[fact_7_h1,92,98,h9,h10])).
% 0.89/1.09 thf(100,plain,$false,inference(tab_imp,[status(thm),assumptions([h5,h2,h0]),tab_imp(discharge,[h7]),tab_imp(discharge,[h8])],[h5,79,99,h7,h8])).
% 0.89/1.09 thf(101,plain,(~(sP9) | sP14),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(102,plain,(~(sP14) | sP6),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(103,plain,(~(sP6) | sP5),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(104,plain,(~(sP5) | sP3),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(105,plain,((~(sP3) | ~(sP11)) | sP8),inference(prop_rule,[status(thm)],[])).
% 0.89/1.09 thf(106,plain,$false,inference(prop_unsat,[status(thm),assumptions([h11,h9,h6,h2,h0])],[101,102,103,104,105,h0,fact_3_sortLemmaL,fact_1_s])).
% 0.89/1.09 thf(107,plain,(~(sP9) | sP14),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(108,plain,(~(sP14) | sP6),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(109,plain,(~(sP6) | sP5),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(110,plain,(~(sP5) | sP3),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(111,plain,((~(sP3) | ~(sP11)) | sP8),inference(prop_rule,[status(thm)],[])).
% 0.89/1.09 thf(112,plain,$false,inference(prop_unsat,[status(thm),assumptions([h12,h9,h6,h2,h0])],[107,108,109,110,111,h12,fact_3_sortLemmaL,fact_1_s])).
% 0.89/1.09 thf(113,plain,$false,inference(tab_imp,[status(thm),assumptions([h9,h6,h2,h0]),tab_imp(discharge,[h11]),tab_imp(discharge,[h12])],[h9,106,112,h11,h12])).
% 0.89/1.09 thf(114,plain,(~(sP9) | sP14),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(115,plain,(~(sP14) | sP6),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(116,plain,(~(sP6) | sP5),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(117,plain,(~(sP5) | sP3),inference(all_rule,[status(thm)],[])).
% 0.89/1.09 thf(118,plain,((~(sP3) | ~(sP11)) | sP8),inference(prop_rule,[status(thm)],[])).
% 0.89/1.09 thf(119,plain,$false,inference(prop_unsat,[status(thm),assumptions([h10,h6,h2,h0])],[114,115,116,117,118,h0,fact_3_sortLemmaL,fact_1_s])).
% 0.89/1.09 thf(120,plain,$false,inference(tab_imp,[status(thm),assumptions([h6,h2,h0]),tab_imp(discharge,[h9]),tab_imp(discharge,[h10])],[fact_7_h1,113,119,h9,h10])).
% 0.89/1.09 thf(121,plain,$false,inference(tab_imp,[status(thm),assumptions([h2,h0]),tab_imp(discharge,[h5]),tab_imp(discharge,[h6])],[fact_11_h2,100,120,h5,h6])).
% 0.89/1.09 thf(fact_13__092_060open_062Tip_A_092_060noteq_062_ATip_A_092_060and_062_AsortedTree_Ah_ATip_A_092_060longrightarrow_062_AsortedTree_Ah_A_Iwrm_Ah_ATip_J_092_060close_062,axiom,((~(((~((binary476621312_Tip_a = binary476621312_Tip_a))) => (~(sP4))))) => ((binary1721989714Tree_a @ h) @ ((binary1217730267_wrm_a @ h) @ binary476621312_Tip_a)))).
% 0.89/1.09 thf(122,plain,$false,inference(tab_imp,[status(thm),assumptions([h0]),tab_imp(discharge,[h1]),tab_imp(discharge,[h2])],[fact_13__092_060open_062Tip_A_092_060noteq_062_ATip_A_092_060and_062_AsortedTree_Ah_ATip_A_092_060longrightarrow_062_AsortedTree_Ah_A_Iwrm_Ah_ATip_J_092_060close_062,59,121,h1,h2])).
% 0.89/1.09 thf(0,theorem,sP8,inference(contra,[status(thm),contra(discharge,[h0])],[122,h0])).
% 0.89/1.09 % SZS output end Proof
%------------------------------------------------------------------------------