%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP102^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 : n026.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 3.20s 3.43s
% Output : Proof 3.20s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.14 % Problem : ITP102^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.13/0.35 % Computer : n026.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Wed Oct 8 18:06:23 EDT 2025
% 0.13/0.35 % CPUTime :
% 3.20/3.43 % SZS status Theorem
% 3.20/3.43 % Mode: mode507:USE_SINE=true:SINE_TOLERANCE=3.0:SINE_GENERALITY_THRESHOLD=0:SINE_RANK_LIMIT=1.:SINE_DEPTH=1
% 3.20/3.43 % Inferences: 2
% 3.20/3.43 % SZS output start Proof
% 3.20/3.43 thf(ty_a, type, a : $tType).
% 3.20/3.43 thf(ty_nat, type, nat : $tType).
% 3.20/3.43 thf(ty_list_a, type, list_a : $tType).
% 3.20/3.43 thf(ty_eigen__0, type, eigen__0 : nat).
% 3.20/3.43 thf(ty_nth_a, type, nth_a : (list_a>nat>a)).
% 3.20/3.43 thf(ty_ord_less_nat, type, ord_less_nat : (nat>nat>$o)).
% 3.20/3.43 thf(ty_xs, type, xs : list_a).
% 3.20/3.43 thf(ty_size_size_list_a, type, size_size_list_a : (list_a>nat)).
% 3.20/3.43 thf(ty_ys, type, ys : list_a).
% 3.20/3.43 thf(conj_2,conjecture,(![X1:nat]:(((ord_less_nat @ X1) @ (size_size_list_a @ xs)) => (((nth_a @ xs) @ X1) = ((nth_a @ ys) @ X1))))).
% 3.20/3.43 thf(h0,negated_conjecture,(~((![X1:nat]:(((ord_less_nat @ X1) @ (size_size_list_a @ xs)) => (((nth_a @ xs) @ X1) = ((nth_a @ ys) @ X1)))))),inference(assume_negation,[status(cth)],[conj_2])).
% 3.20/3.43 thf(h1,assumption,(~((((ord_less_nat @ eigen__0) @ (size_size_list_a @ xs)) => (((nth_a @ xs) @ eigen__0) = ((nth_a @ ys) @ eigen__0))))),introduced(assumption,[])).
% 3.20/3.43 thf(h2,assumption,((ord_less_nat @ eigen__0) @ (size_size_list_a @ xs)),introduced(assumption,[])).
% 3.20/3.43 thf(h3,assumption,(~((((nth_a @ xs) @ eigen__0) = ((nth_a @ ys) @ eigen__0)))),introduced(assumption,[])).
% 3.20/3.43 thf(pax45, axiom, (p45=>![X17:nat, X25:nat, X27:nat]:(ford_less_eq_nat @ X17 @ X25=>(ford_less_nat @ X27 @ X17=>ford_less_nat @ X27 @ X25))), file('<stdin>', pax45)).
% 3.20/3.43 thf(pax122, axiom, (p122=>ford_less_eq_nat @ (fsize_size_list_a @ fxs) @ (fsize_size_list_a @ fys)), file('<stdin>', pax122)).
% 3.20/3.43 thf(ax83, axiom, p45, file('<stdin>', ax83)).
% 3.20/3.43 thf(ax6, axiom, p122, file('<stdin>', ax6)).
% 3.20/3.43 thf(pax124, axiom, (p124=>ford_less_nat @ f__0 @ (fsize_size_list_a @ fxs)), file('<stdin>', pax124)).
% 3.20/3.43 thf(pax2, axiom, (p2=>![X43:nat, X42:list_a, X44:nat > a]:(ford_less_nat @ X43 @ (fsize_size_list_a @ X42)=>(flistIn1312259492pend_a @ X42 @ X44 @ X43)=(fnth_a @ X42 @ X43))), file('<stdin>', pax2)).
% 3.20/3.43 thf(ax4, axiom, p124, file('<stdin>', ax4)).
% 3.20/3.43 thf(pax121, axiom, (p121=>![X3:nat]:(flistIn1312259492pend_a @ fxs @ ff @ X3)=(flistIn1312259492pend_a @ fys @ fg @ X3)), file('<stdin>', pax121)).
% 3.20/3.43 thf(ax126, axiom, p2, file('<stdin>', ax126)).
% 3.20/3.43 thf(nax123, axiom, (p123<=(fnth_a @ fxs @ f__0)=(fnth_a @ fys @ f__0)), file('<stdin>', nax123)).
% 3.20/3.43 thf(ax5, axiom, ~(p123), file('<stdin>', ax5)).
% 3.20/3.43 thf(ax7, axiom, p121, file('<stdin>', ax7)).
% 3.20/3.43 thf(c_0_12, plain, ![X305:nat, X306:nat, X307:nat]:(~p45|(~ford_less_eq_nat @ X305 @ X306|(~ford_less_nat @ X307 @ X305|ford_less_nat @ X307 @ X306))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax45])])])).
% 3.20/3.43 thf(c_0_13, plain, (~p122|ford_less_eq_nat @ (fsize_size_list_a @ fxs) @ (fsize_size_list_a @ fys)), inference(fof_nnf,[status(thm)],[pax122])).
% 3.20/3.43 thf(c_0_14, plain, ![X5:nat, X4:nat, X3:nat]:(ford_less_nat @ X5 @ X4|~p45|~ford_less_eq_nat @ X3 @ X4|~ford_less_nat @ X5 @ X3), inference(split_conjunct,[status(thm)],[c_0_12])).
% 3.20/3.43 thf(c_0_15, plain, p45, inference(split_conjunct,[status(thm)],[ax83])).
% 3.20/3.43 thf(c_0_16, plain, (ford_less_eq_nat @ (fsize_size_list_a @ fxs) @ (fsize_size_list_a @ fys)|~p122), inference(split_conjunct,[status(thm)],[c_0_13])).
% 3.20/3.43 thf(c_0_17, plain, p122, inference(split_conjunct,[status(thm)],[ax6])).
% 3.20/3.43 thf(c_0_18, plain, (~p124|ford_less_nat @ f__0 @ (fsize_size_list_a @ fxs)), inference(fof_nnf,[status(thm)],[pax124])).
% 3.20/3.43 thf(c_0_19, plain, ![X459:nat, X460:list_a, X461:nat > a]:(~p2|(~ford_less_nat @ X459 @ (fsize_size_list_a @ X460)|(flistIn1312259492pend_a @ X460 @ X461 @ X459)=(fnth_a @ X460 @ X459))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax2])])])).
% 3.20/3.43 thf(c_0_20, plain, ![X3:nat, X5:nat, X4:nat]:(ford_less_nat @ X3 @ X4|~ford_less_nat @ X3 @ X5|~ford_less_eq_nat @ X5 @ X4), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_14, c_0_15])])).
% 3.20/3.43 thf(c_0_21, plain, ford_less_eq_nat @ (fsize_size_list_a @ fxs) @ (fsize_size_list_a @ fys), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_16, c_0_17])])).
% 3.20/3.43 thf(c_0_22, plain, (ford_less_nat @ f__0 @ (fsize_size_list_a @ fxs)|~p124), inference(split_conjunct,[status(thm)],[c_0_18])).
% 3.20/3.43 thf(c_0_23, plain, p124, inference(split_conjunct,[status(thm)],[ax4])).
% 3.20/3.43 thf(c_0_24, plain, ![X53:nat]:(~p121|(flistIn1312259492pend_a @ fxs @ ff @ X53)=(flistIn1312259492pend_a @ fys @ fg @ X53)), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax121])])])).
% 3.20/3.43 thf(c_0_25, plain, ![X3:nat, X7:nat > a, X6:list_a]:((flistIn1312259492pend_a @ X6 @ X7 @ X3)=(fnth_a @ X6 @ X3)|~p2|~ford_less_nat @ X3 @ (fsize_size_list_a @ X6)), inference(split_conjunct,[status(thm)],[c_0_19])).
% 3.20/3.43 thf(c_0_26, plain, p2, inference(split_conjunct,[status(thm)],[ax126])).
% 3.20/3.43 thf(c_0_27, plain, ![X3:nat]:(ford_less_nat @ X3 @ (fsize_size_list_a @ fys)|~ford_less_nat @ X3 @ (fsize_size_list_a @ fxs)), inference(spm,[status(thm)],[c_0_20, c_0_21])).
% 3.20/3.43 thf(c_0_28, plain, ford_less_nat @ f__0 @ (fsize_size_list_a @ fxs), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_22, c_0_23])])).
% 3.20/3.43 thf(c_0_29, plain, ((fnth_a @ fxs @ f__0)!=(fnth_a @ fys @ f__0)|p123), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax123])])).
% 3.20/3.43 thf(c_0_30, plain, ~p123, inference(fof_simplification,[status(thm)],[ax5])).
% 3.20/3.43 thf(c_0_31, plain, ![X3:nat]:((flistIn1312259492pend_a @ fxs @ ff @ X3)=(flistIn1312259492pend_a @ fys @ fg @ X3)|~p121), inference(split_conjunct,[status(thm)],[c_0_24])).
% 3.20/3.43 thf(c_0_32, plain, p121, inference(split_conjunct,[status(thm)],[ax7])).
% 3.20/3.43 thf(c_0_33, plain, ![X3:nat, X7:nat > a, X6:list_a]:((flistIn1312259492pend_a @ X6 @ X7 @ X3)=(fnth_a @ X6 @ X3)|~ford_less_nat @ X3 @ (fsize_size_list_a @ X6)), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_25, c_0_26])])).
% 3.20/3.43 thf(c_0_34, plain, ford_less_nat @ f__0 @ (fsize_size_list_a @ fys), inference(spm,[status(thm)],[c_0_27, c_0_28])).
% 3.20/3.43 thf(c_0_35, plain, (p123|(fnth_a @ fxs @ f__0)!=(fnth_a @ fys @ f__0)), inference(split_conjunct,[status(thm)],[c_0_29])).
% 3.20/3.43 thf(c_0_36, plain, ~p123, inference(split_conjunct,[status(thm)],[c_0_30])).
% 3.20/3.43 thf(c_0_37, plain, ![X3:nat]:(flistIn1312259492pend_a @ fys @ fg @ X3)=(flistIn1312259492pend_a @ fxs @ ff @ X3), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_31, c_0_32])])).
% 3.20/3.43 thf(c_0_38, plain, ![X7:nat > a]:(flistIn1312259492pend_a @ fys @ X7 @ f__0)=(fnth_a @ fys @ f__0), inference(spm,[status(thm)],[c_0_33, c_0_34])).
% 3.20/3.43 thf(c_0_39, plain, ![X7:nat > a]:(flistIn1312259492pend_a @ fxs @ X7 @ f__0)=(fnth_a @ fxs @ f__0), inference(spm,[status(thm)],[c_0_33, c_0_28])).
% 3.20/3.43 thf(c_0_40, plain, (fnth_a @ fys @ f__0)!=(fnth_a @ fxs @ f__0), inference(sr,[status(thm)],[c_0_35, c_0_36])).
% 3.20/3.43 thf(c_0_41, plain, ($false), inference(sr,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_37, c_0_38]), c_0_39]), c_0_40]), ['proof']).
% 3.20/3.43 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h2,h3,h1,h0])],[])).
% 3.20/3.43 thf(2,plain,$false,inference(tab_negimp,[status(thm),assumptions([h1,h0]),tab_negimp(discharge,[h2,h3])],[h1,1,h2,h3])).
% 3.20/3.43 thf(3,plain,$false,inference(tab_negall,[status(thm),assumptions([h0]),tab_negall(discharge,[h1]),tab_negall(eigenvar,eigen__0)],[h0,2,h1])).
% 3.20/3.43 thf(0,theorem,(![X1:nat]:(((ord_less_nat @ X1) @ (size_size_list_a @ xs)) => (((nth_a @ xs) @ X1) = ((nth_a @ ys) @ X1)))),inference(contra,[status(thm),contra(discharge,[h0])],[3,h0])).
% 3.20/3.43 % SZS output end Proof
%------------------------------------------------------------------------------