%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP099^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 : n022.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:58 PM UTC 2025
% Result : Theorem 10.31s 10.52s
% Output : Proof 10.31s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : ITP099^1 : TPTP v9.2.0. Released v7.5.0.
% 0.07/0.14 % Command : satallax -E eprover-ho -P picomus -M modes -p tstp -t %d %s
% 0.14/0.35 % Computer : n022.cluster.edu
% 0.14/0.35 % Model : x86_64 x86_64
% 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35 % Memory : 8042.1875MB
% 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35 % CPULimit : 300
% 0.14/0.35 % WCLimit : 300
% 0.14/0.35 % DateTime : Wed Oct 8 18:43:53 EDT 2025
% 0.14/0.35 % CPUTime :
% 10.31/10.52 % SZS status Theorem
% 10.31/10.52 % Mode: mode507:USE_SINE=true:SINE_TOLERANCE=3.0:SINE_GENERALITY_THRESHOLD=0:SINE_RANK_LIMIT=1.:SINE_DEPTH=1
% 10.31/10.52 % Inferences: 25
% 10.31/10.52 % SZS output start Proof
% 10.31/10.52 thf(ty_a, type, a : $tType).
% 10.31/10.52 thf(ty_nat, type, nat : $tType).
% 10.31/10.52 thf(ty_list_a, type, list_a : $tType).
% 10.31/10.52 thf(ty_eigen__1, type, eigen__1 : nat).
% 10.31/10.52 thf(ty_n, type, n : nat).
% 10.31/10.52 thf(ty_eigen__0, type, eigen__0 : nat).
% 10.31/10.52 thf(ty_minus_minus_nat, type, minus_minus_nat : (nat>nat>nat)).
% 10.31/10.52 thf(ty_ord_less_nat, type, ord_less_nat : (nat>nat>$o)).
% 10.31/10.52 thf(ty_xs, type, xs : list_a).
% 10.31/10.52 thf(ty_size_size_list_a, type, size_size_list_a : (list_a>nat)).
% 10.31/10.52 thf(ty_drop_a, type, drop_a : (nat>list_a>list_a)).
% 10.31/10.52 thf(ty_f, type, f : (nat>a)).
% 10.31/10.52 thf(ty_listIn1312259492pend_a, type, listIn1312259492pend_a : (list_a>(nat>a)>nat>a)).
% 10.31/10.52 thf(ty_listIn1417627087drop_a, type, listIn1417627087drop_a : (nat>(nat>a)>nat>a)).
% 10.31/10.52 thf(conj_0,conjecture,(~(((((ord_less_nat @ n) @ (size_size_list_a @ xs)) => (((listIn1417627087drop_a @ n) @ ((listIn1312259492pend_a @ xs) @ f)) = ((listIn1312259492pend_a @ ((drop_a @ n) @ xs)) @ f))) => (~(((~(((ord_less_nat @ n) @ (size_size_list_a @ xs)))) => (((listIn1417627087drop_a @ n) @ ((listIn1312259492pend_a @ xs) @ f)) = ((listIn1417627087drop_a @ ((minus_minus_nat @ n) @ (size_size_list_a @ xs))) @ f))))))))).
% 10.31/10.52 thf(h0,negated_conjecture,((((ord_less_nat @ n) @ (size_size_list_a @ xs)) => (((listIn1417627087drop_a @ n) @ ((listIn1312259492pend_a @ xs) @ f)) = ((listIn1312259492pend_a @ ((drop_a @ n) @ xs)) @ f))) => (~(((~(((ord_less_nat @ n) @ (size_size_list_a @ xs)))) => (((listIn1417627087drop_a @ n) @ ((listIn1312259492pend_a @ xs) @ f)) = ((listIn1417627087drop_a @ ((minus_minus_nat @ n) @ (size_size_list_a @ xs))) @ f)))))),inference(assume_negation,[status(cth)],[conj_0])).
% 10.31/10.52 thf(h1,assumption,(~((((ord_less_nat @ n) @ (size_size_list_a @ xs)) => (((listIn1417627087drop_a @ n) @ ((listIn1312259492pend_a @ xs) @ f)) = ((listIn1312259492pend_a @ ((drop_a @ n) @ xs)) @ f))))),introduced(assumption,[])).
% 10.31/10.52 thf(h2,assumption,(~(((~(((ord_less_nat @ n) @ (size_size_list_a @ xs)))) => (((listIn1417627087drop_a @ n) @ ((listIn1312259492pend_a @ xs) @ f)) = ((listIn1417627087drop_a @ ((minus_minus_nat @ n) @ (size_size_list_a @ xs))) @ f))))),introduced(assumption,[])).
% 10.31/10.52 thf(h3,assumption,((ord_less_nat @ n) @ (size_size_list_a @ xs)),introduced(assumption,[])).
% 10.31/10.52 thf(h4,assumption,(~((((listIn1417627087drop_a @ n) @ ((listIn1312259492pend_a @ xs) @ f)) = ((listIn1312259492pend_a @ ((drop_a @ n) @ xs)) @ f)))),introduced(assumption,[])).
% 10.31/10.52 thf(h5,assumption,(~((![X1:nat]:((((listIn1417627087drop_a @ n) @ ((listIn1312259492pend_a @ xs) @ f)) @ X1) = (((listIn1312259492pend_a @ ((drop_a @ n) @ xs)) @ f) @ X1))))),introduced(assumption,[])).
% 10.31/10.52 thf(h6,assumption,(~(((((listIn1417627087drop_a @ n) @ ((listIn1312259492pend_a @ xs) @ f)) @ eigen__0) = (((listIn1312259492pend_a @ ((drop_a @ n) @ xs)) @ f) @ eigen__0)))),introduced(assumption,[])).
% 10.31/10.52 thf(nax143, axiom, (p143<=(flistIn1417627087drop_a @ fn @ (flistIn1312259492pend_a @ fxs @ ff) @ f__0)=(flistIn1312259492pend_a @ (fdrop_a @ fn @ fxs) @ ff @ f__0)), file('<stdin>', nax143)).
% 10.31/10.52 thf(ax471, axiom, ~(p143), file('<stdin>', ax471)).
% 10.31/10.52 thf(pax26, axiom, (p26=>![X96:nat, X97:list_a, X95:nat > a]:(ford_less_eq_nat @ X96 @ (fsize_size_list_a @ X97)=>(flistIn1417627087drop_a @ X96 @ (flistIn1312259492pend_a @ X97 @ X95))=(flistIn1312259492pend_a @ (fdrop_a @ X96 @ X97) @ X95))), file('<stdin>', pax26)).
% 10.31/10.52 thf(ax588, axiom, p26, file('<stdin>', ax588)).
% 10.31/10.52 thf(pax44, axiom, (p44=>![X68:nat, X63:nat]:(ford_less_nat @ X68 @ X63=>ford_less_eq_nat @ X68 @ X63)), file('<stdin>', pax44)).
% 10.31/10.52 thf(pax144, axiom, (p144=>ford_less_nat @ fn @ (fsize_size_list_a @ fxs)), file('<stdin>', pax144)).
% 10.31/10.52 thf(ax570, axiom, p44, file('<stdin>', ax570)).
% 10.31/10.52 thf(ax470, axiom, p144, file('<stdin>', ax470)).
% 10.31/10.52 thf(c_0_8, plain, ((flistIn1417627087drop_a @ fn @ (flistIn1312259492pend_a @ fxs @ ff) @ f__0)!=(flistIn1312259492pend_a @ (fdrop_a @ fn @ fxs) @ ff @ f__0)|p143), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax143])])).
% 10.31/10.52 thf(c_0_9, plain, ~p143, inference(fof_simplification,[status(thm)],[ax471])).
% 10.31/10.52 thf(c_0_10, plain, ![X769:nat, X770:list_a, X771:nat > a]:(~p26|(~ford_less_eq_nat @ X769 @ (fsize_size_list_a @ X770)|(flistIn1417627087drop_a @ X769 @ (flistIn1312259492pend_a @ X770 @ X771))=(flistIn1312259492pend_a @ (fdrop_a @ X769 @ X770) @ X771))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax26])])])).
% 10.31/10.52 thf(c_0_11, plain, (p143|(flistIn1417627087drop_a @ fn @ (flistIn1312259492pend_a @ fxs @ ff) @ f__0)!=(flistIn1312259492pend_a @ (fdrop_a @ fn @ fxs) @ ff @ f__0)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 10.31/10.52 thf(c_0_12, plain, ~p143, inference(split_conjunct,[status(thm)],[c_0_9])).
% 10.31/10.52 thf(c_0_13, plain, ![X1:nat, X3:nat > a, X4:list_a]:((flistIn1417627087drop_a @ X1 @ (flistIn1312259492pend_a @ X4 @ X3))=(flistIn1312259492pend_a @ (fdrop_a @ X1 @ X4) @ X3)|~p26|~ford_less_eq_nat @ X1 @ (fsize_size_list_a @ X4)), inference(split_conjunct,[status(thm)],[c_0_10])).
% 10.31/10.52 thf(c_0_14, plain, p26, inference(split_conjunct,[status(thm)],[ax588])).
% 10.31/10.52 thf(c_0_15, plain, ![X705:nat, X706:nat]:(~p44|(~ford_less_nat @ X705 @ X706|ford_less_eq_nat @ X705 @ X706)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax44])])])).
% 10.31/10.52 thf(c_0_16, plain, (~p144|ford_less_nat @ fn @ (fsize_size_list_a @ fxs)), inference(fof_nnf,[status(thm)],[pax144])).
% 10.31/10.52 thf(c_0_17, plain, (flistIn1417627087drop_a @ fn @ (flistIn1312259492pend_a @ fxs @ ff) @ f__0)!=(flistIn1312259492pend_a @ (fdrop_a @ fn @ fxs) @ ff @ f__0), inference(sr,[status(thm)],[c_0_11, c_0_12])).
% 10.31/10.52 thf(c_0_18, plain, ![X1:nat, X3:nat > a, X4:list_a]:((flistIn1417627087drop_a @ X1 @ (flistIn1312259492pend_a @ X4 @ X3))=(flistIn1312259492pend_a @ (fdrop_a @ X1 @ X4) @ X3)|~ford_less_eq_nat @ X1 @ (fsize_size_list_a @ X4)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_13, c_0_14])])).
% 10.31/10.52 thf(c_0_19, plain, ![X1:nat, X2:nat]:(ford_less_eq_nat @ X1 @ X2|~p44|~ford_less_nat @ X1 @ X2), inference(split_conjunct,[status(thm)],[c_0_15])).
% 10.31/10.52 thf(c_0_20, plain, p44, inference(split_conjunct,[status(thm)],[ax570])).
% 10.31/10.52 thf(c_0_21, plain, (ford_less_nat @ fn @ (fsize_size_list_a @ fxs)|~p144), inference(split_conjunct,[status(thm)],[c_0_16])).
% 10.31/10.52 thf(c_0_22, plain, p144, inference(split_conjunct,[status(thm)],[ax470])).
% 10.31/10.52 thf(c_0_23, plain, ~ford_less_eq_nat @ fn @ (fsize_size_list_a @ fxs), inference(spm,[status(thm)],[c_0_17, c_0_18])).
% 10.31/10.52 thf(c_0_24, plain, ![X1:nat, X2:nat]:(ford_less_eq_nat @ X1 @ X2|~ford_less_nat @ X1 @ X2), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_19, c_0_20])])).
% 10.31/10.52 thf(c_0_25, plain, ford_less_nat @ fn @ (fsize_size_list_a @ fxs), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_21, c_0_22])])).
% 10.31/10.52 thf(c_0_26, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_23, c_0_24]), c_0_25])]), ['proof']).
% 10.31/10.52 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h6,h5,h3,h4,h1,h0])],[])).
% 10.31/10.52 thf(2,plain,$false,inference(tab_negall,[status(thm),assumptions([h5,h3,h4,h1,h0]),tab_negall(discharge,[h6]),tab_negall(eigenvar,eigen__0)],[h5,1,h6])).
% 10.31/10.52 thf(3,plain,$false,inference(tab_fe,[status(thm),assumptions([h3,h4,h1,h0]),tab_fe(discharge,[h5])],[h4,2,h5])).
% 10.31/10.52 thf(4,plain,$false,inference(tab_negimp,[status(thm),assumptions([h1,h0]),tab_negimp(discharge,[h3,h4])],[h1,3,h3,h4])).
% 10.31/10.52 thf(h7,assumption,(~(((ord_less_nat @ n) @ (size_size_list_a @ xs)))),introduced(assumption,[])).
% 10.31/10.52 thf(h8,assumption,(~((((listIn1417627087drop_a @ n) @ ((listIn1312259492pend_a @ xs) @ f)) = ((listIn1417627087drop_a @ ((minus_minus_nat @ n) @ (size_size_list_a @ xs))) @ f)))),introduced(assumption,[])).
% 10.31/10.52 thf(h9,assumption,(~((![X1:nat]:((((listIn1417627087drop_a @ n) @ ((listIn1312259492pend_a @ xs) @ f)) @ X1) = (((listIn1417627087drop_a @ ((minus_minus_nat @ n) @ (size_size_list_a @ xs))) @ f) @ X1))))),introduced(assumption,[])).
% 10.31/10.52 thf(h10,assumption,(~(((((listIn1417627087drop_a @ n) @ ((listIn1312259492pend_a @ xs) @ f)) @ eigen__1) = (((listIn1417627087drop_a @ ((minus_minus_nat @ n) @ (size_size_list_a @ xs))) @ f) @ eigen__1)))),introduced(assumption,[])).
% 10.31/10.52 thf(nax615, axiom, (p615<=(flistIn1417627087drop_a @ fn @ (flistIn1312259492pend_a @ fxs @ ff) @ f__1)=(flistIn1417627087drop_a @ (fminus_minus_nat @ fn @ (fsize_size_list_a @ fxs)) @ ff @ f__1)), file('<stdin>', nax615)).
% 10.31/10.52 thf(ax10, axiom, ~(p615), file('<stdin>', ax10)).
% 10.31/10.52 thf(pax27, axiom, (p27=>![X96:list_a, X97:nat, X98:nat > a]:(ford_less_eq_nat @ (fsize_size_list_a @ X96) @ X97=>(flistIn1417627087drop_a @ X97 @ (flistIn1312259492pend_a @ X96 @ X98))=(flistIn1417627087drop_a @ (fminus_minus_nat @ X97 @ (fsize_size_list_a @ X96)) @ X98))), file('<stdin>', pax27)).
% 10.31/10.52 thf(ax126, axiom, p27, file('<stdin>', ax126)).
% 10.31/10.52 thf(pax107, axiom, (p107=>![X21:nat, X31:nat]:(~(ford_less_eq_nat @ X21 @ X31)=>ford_less_nat @ X31 @ X21)), file('<stdin>', pax107)).
% 10.31/10.52 thf(nax144, axiom, (p144<=ford_less_nat @ fn @ (fsize_size_list_a @ fxs)), file('<stdin>', nax144)).
% 10.31/10.52 thf(ax9, axiom, ~(p144), file('<stdin>', ax9)).
% 10.31/10.52 thf(ax46, axiom, p107, file('<stdin>', ax46)).
% 10.31/10.52 thf(c_0_8, plain, ((flistIn1417627087drop_a @ fn @ (flistIn1312259492pend_a @ fxs @ ff) @ f__1)!=(flistIn1417627087drop_a @ (fminus_minus_nat @ fn @ (fsize_size_list_a @ fxs)) @ ff @ f__1)|p615), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax615])])).
% 10.31/10.52 thf(c_0_9, plain, ~p615, inference(fof_simplification,[status(thm)],[ax10])).
% 10.31/10.52 thf(c_0_10, plain, ![X774:list_a, X775:nat, X776:nat > a]:(~p27|(~ford_less_eq_nat @ (fsize_size_list_a @ X774) @ X775|(flistIn1417627087drop_a @ X775 @ (flistIn1312259492pend_a @ X774 @ X776))=(flistIn1417627087drop_a @ (fminus_minus_nat @ X775 @ (fsize_size_list_a @ X774)) @ X776))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax27])])])).
% 10.31/10.52 thf(c_0_11, plain, (p615|(flistIn1417627087drop_a @ fn @ (flistIn1312259492pend_a @ fxs @ ff) @ f__1)!=(flistIn1417627087drop_a @ (fminus_minus_nat @ fn @ (fsize_size_list_a @ fxs)) @ ff @ f__1)), inference(split_conjunct,[status(thm)],[c_0_8])).
% 10.31/10.52 thf(c_0_12, plain, ~p615, inference(split_conjunct,[status(thm)],[c_0_9])).
% 10.31/10.52 thf(c_0_13, plain, ![X6:nat > a, X2:list_a, X1:nat]:((flistIn1417627087drop_a @ X1 @ (flistIn1312259492pend_a @ X2 @ X6))=(flistIn1417627087drop_a @ (fminus_minus_nat @ X1 @ (fsize_size_list_a @ X2)) @ X6)|~p27|~ford_less_eq_nat @ (fsize_size_list_a @ X2) @ X1), inference(split_conjunct,[status(thm)],[c_0_10])).
% 10.31/10.52 thf(c_0_14, plain, p27, inference(split_conjunct,[status(thm)],[ax126])).
% 10.31/10.52 thf(c_0_15, plain, ![X440:nat, X441:nat]:(~p107|(ford_less_eq_nat @ X440 @ X441|ford_less_nat @ X441 @ X440)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax107])])])])).
% 10.31/10.52 thf(c_0_16, plain, (~ford_less_nat @ fn @ (fsize_size_list_a @ fxs)|p144), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax144])])).
% 10.31/10.52 thf(c_0_17, plain, ~p144, inference(fof_simplification,[status(thm)],[ax9])).
% 10.31/10.52 thf(c_0_18, plain, (flistIn1417627087drop_a @ fn @ (flistIn1312259492pend_a @ fxs @ ff) @ f__1)!=(flistIn1417627087drop_a @ (fminus_minus_nat @ fn @ (fsize_size_list_a @ fxs)) @ ff @ f__1), inference(sr,[status(thm)],[c_0_11, c_0_12])).
% 10.31/10.52 thf(c_0_19, plain, ![X6:nat > a, X2:list_a, X1:nat]:((flistIn1417627087drop_a @ X1 @ (flistIn1312259492pend_a @ X2 @ X6))=(flistIn1417627087drop_a @ (fminus_minus_nat @ X1 @ (fsize_size_list_a @ X2)) @ X6)|~ford_less_eq_nat @ (fsize_size_list_a @ X2) @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_13, c_0_14])])).
% 10.31/10.52 thf(c_0_20, plain, ![X4:nat, X1:nat]:(ford_less_eq_nat @ X1 @ X4|ford_less_nat @ X4 @ X1|~p107), inference(split_conjunct,[status(thm)],[c_0_15])).
% 10.31/10.52 thf(c_0_21, plain, p107, inference(split_conjunct,[status(thm)],[ax46])).
% 10.31/10.52 thf(c_0_22, plain, (p144|~ford_less_nat @ fn @ (fsize_size_list_a @ fxs)), inference(split_conjunct,[status(thm)],[c_0_16])).
% 10.31/10.52 thf(c_0_23, plain, ~p144, inference(split_conjunct,[status(thm)],[c_0_17])).
% 10.31/10.52 thf(c_0_24, plain, ~ford_less_eq_nat @ (fsize_size_list_a @ fxs) @ fn, inference(spm,[status(thm)],[c_0_18, c_0_19])).
% 10.31/10.52 thf(c_0_25, plain, ![X4:nat, X1:nat]:(ford_less_eq_nat @ X1 @ X4|ford_less_nat @ X4 @ X1), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_20, c_0_21])])).
% 10.31/10.52 thf(c_0_26, plain, ~ford_less_nat @ fn @ (fsize_size_list_a @ fxs), inference(sr,[status(thm)],[c_0_22, c_0_23])).
% 10.31/10.52 thf(c_0_27, plain, ($false), inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_24, c_0_25]), c_0_26]), ['proof']).
% 10.31/10.52 thf(5,plain,$false,inference(eprover,[status(thm),assumptions([h10,h9,h7,h8,h2,h0])],[])).
% 10.31/10.52 thf(6,plain,$false,inference(tab_negall,[status(thm),assumptions([h9,h7,h8,h2,h0]),tab_negall(discharge,[h10]),tab_negall(eigenvar,eigen__1)],[h9,5,h10])).
% 10.31/10.52 thf(7,plain,$false,inference(tab_fe,[status(thm),assumptions([h7,h8,h2,h0]),tab_fe(discharge,[h9])],[h8,6,h9])).
% 10.31/10.52 thf(8,plain,$false,inference(tab_negimp,[status(thm),assumptions([h2,h0]),tab_negimp(discharge,[h7,h8])],[h2,7,h7,h8])).
% 10.31/10.52 thf(9,plain,$false,inference(tab_imp,[status(thm),assumptions([h0]),tab_imp(discharge,[h1]),tab_imp(discharge,[h2])],[h0,4,8,h1,h2])).
% 10.31/10.52 thf(0,theorem,(~(((((ord_less_nat @ n) @ (size_size_list_a @ xs)) => (((listIn1417627087drop_a @ n) @ ((listIn1312259492pend_a @ xs) @ f)) = ((listIn1312259492pend_a @ ((drop_a @ n) @ xs)) @ f))) => (~(((~(((ord_less_nat @ n) @ (size_size_list_a @ xs)))) => (((listIn1417627087drop_a @ n) @ ((listIn1312259492pend_a @ xs) @ f)) = ((listIn1417627087drop_a @ ((minus_minus_nat @ n) @ (size_size_list_a @ xs))) @ f)))))))),inference(contra,[status(thm),contra(discharge,[h0])],[9,h0])).
% 10.31/10.52 % SZS output end Proof
%------------------------------------------------------------------------------