%------------------------------------------------------------------------------
% File : Satallax---3.5
% Problem : ITP168^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 : n016.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:47:10 PM UTC 2025
% Result : Theorem 165.27s 165.15s
% Output : Proof 165.27s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : ITP168^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 : n016.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:25:38 EDT 2025
% 0.12/0.35 % CPUTime :
% 165.27/165.15 % SZS status Theorem
% 165.27/165.15 % Mode: mode500:USE_SINE=true:SINE_TOLERANCE=1.0:SINE_GENERALITY_THRESHOLD=16:SINE_RANK_LIMIT=2.:SINE_DEPTH=0
% 165.27/165.15 % Inferences: 9
% 165.27/165.15 % SZS output start Proof
% 165.27/165.15 thf(conj_0,conjecture,((((move @ ts3) @ ts_a) @ v) = (((move @ ts3) @ ts) @ v))).
% 165.27/165.15 thf(h0,negated_conjecture,(~(((((move @ ts3) @ ts_a) @ v) = (((move @ ts3) @ ts) @ v)))),inference(assume_negation,[status(cth)],[conj_0])).
% 165.27/165.15 thf(pax57, axiom, (p57=>![X4:traffic, X5:cars, X6:traffic, X7:view_e774982825t_unit]:(fcreate_reservation @ X4 @ X5 @ X6=>(fmove @ X4 @ X6 @ X7)=(X7))), file('<stdin>', pax57)).
% 165.27/165.15 thf(nax64, axiom, (p64<=![X3:cars]:~(fcreate_reservation @ fts_a @ X3 @ fts)), file('<stdin>', nax64)).
% 165.27/165.15 thf(ax6, axiom, ~(p64), file('<stdin>', ax6)).
% 165.27/165.15 thf(ax13, axiom, p57, file('<stdin>', ax13)).
% 165.27/165.15 thf(pax55, axiom, (p55=>![X4:traffic, X8:traffic, X6:traffic, X7:view_e774982825t_unit]:(~((fabstract @ X4 @ X8=>~(fabstract @ X8 @ X6)))=>(fmove @ X8 @ X6 @ (fmove @ X4 @ X8 @ X7))=(fmove @ X4 @ X6 @ X7))), file('<stdin>', pax55)).
% 165.27/165.15 thf(nax1, axiom, (p1<=(fmove @ fts3 @ fts_a @ fv)=(fmove @ fts3 @ fts @ fv)), file('<stdin>', nax1)).
% 165.27/165.15 thf(ax69, axiom, ~(p1), file('<stdin>', ax69)).
% 165.27/165.15 thf(ax15, axiom, p55, file('<stdin>', ax15)).
% 165.27/165.15 thf(pax65, axiom, (p65=>fabstract @ fts3 @ fts_a), file('<stdin>', pax65)).
% 165.27/165.15 thf(pax44, axiom, (p44=>![X21:traffic, X22:traffic, X23:traffic]:(fabstract @ X21 @ X22=>(~(![X20:cars]:~(fcreate_reservation @ X22 @ X20 @ X23))=>fabstract @ X21 @ X23))), file('<stdin>', pax44)).
% 165.27/165.15 thf(ax5, axiom, p65, file('<stdin>', ax5)).
% 165.27/165.15 thf(ax26, axiom, p44, file('<stdin>', ax26)).
% 165.27/165.15 thf(pax41, axiom, (p41=>![X29:traffic]:fabstract @ X29 @ X29), file('<stdin>', pax41)).
% 165.27/165.15 thf(ax29, axiom, p41, file('<stdin>', ax29)).
% 165.27/165.15 thf(c_0_14, plain, ![X94:traffic, X95:cars, X96:traffic, X97:view_e774982825t_unit]:(~p57|(~fcreate_reservation @ X94 @ X95 @ X96|(fmove @ X94 @ X96 @ X97)=(X97))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax57])])])).
% 165.27/165.15 thf(c_0_15, plain, (fcreate_reservation @ fts_a @ esk5_0 @ fts|p64), inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax64])])])])).
% 165.27/165.15 thf(c_0_16, plain, ~p64, inference(fof_simplification,[status(thm)],[ax6])).
% 165.27/165.15 thf(c_0_17, plain, ![X1:view_e774982825t_unit, X3:cars, X4:traffic, X6:traffic]:((fmove @ X4 @ X6 @ X1)=(X1)|~p57|~fcreate_reservation @ X4 @ X3 @ X6), inference(split_conjunct,[status(thm)],[c_0_14])).
% 165.27/165.15 thf(c_0_18, plain, p57, inference(split_conjunct,[status(thm)],[ax13])).
% 165.27/165.15 thf(c_0_19, plain, (fcreate_reservation @ fts_a @ esk5_0 @ fts|p64), inference(split_conjunct,[status(thm)],[c_0_15])).
% 165.27/165.15 thf(c_0_20, plain, ~p64, inference(split_conjunct,[status(thm)],[c_0_16])).
% 165.27/165.15 thf(c_0_21, plain, ![X102:traffic, X103:traffic, X104:traffic, X105:view_e774982825t_unit]:(~p55|(~fabstract @ X102 @ X103|~fabstract @ X103 @ X104|(fmove @ X103 @ X104 @ (fmove @ X102 @ X103 @ X105))=(fmove @ X102 @ X104 @ X105))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax55])])])])).
% 165.27/165.15 thf(c_0_22, plain, ((fmove @ fts3 @ fts_a @ fv)!=(fmove @ fts3 @ fts @ fv)|p1), inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[nax1])])).
% 165.27/165.15 thf(c_0_23, plain, ~p1, inference(fof_simplification,[status(thm)],[ax69])).
% 165.27/165.15 thf(c_0_24, plain, ![X1:view_e774982825t_unit, X3:cars, X4:traffic, X6:traffic]:((fmove @ X4 @ X6 @ X1)=(X1)|~fcreate_reservation @ X4 @ X3 @ X6), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_17, c_0_18])])).
% 165.27/165.15 thf(c_0_25, plain, fcreate_reservation @ fts_a @ esk5_0 @ fts, inference(sr,[status(thm)],[c_0_19, c_0_20])).
% 165.27/165.15 thf(c_0_26, plain, ![X1:view_e774982825t_unit, X4:traffic, X6:traffic, X8:traffic]:((fmove @ X6 @ X8 @ (fmove @ X4 @ X6 @ X1))=(fmove @ X4 @ X8 @ X1)|~p55|~fabstract @ X4 @ X6|~fabstract @ X6 @ X8), inference(split_conjunct,[status(thm)],[c_0_21])).
% 165.27/165.15 thf(c_0_27, plain, p55, inference(split_conjunct,[status(thm)],[ax15])).
% 165.27/165.15 thf(c_0_28, plain, (~p65|fabstract @ fts3 @ fts_a), inference(fof_nnf,[status(thm)],[pax65])).
% 165.27/165.15 thf(c_0_29, plain, ![X174:traffic, X175:traffic, X176:traffic, X177:cars]:(~p44|(~fabstract @ X174 @ X175|(~fcreate_reservation @ X175 @ X177 @ X176|fabstract @ X174 @ X176))), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[inference(fof_simplification,[status(thm)],[pax44])])])])).
% 165.27/165.15 thf(c_0_30, plain, (p1|(fmove @ fts3 @ fts_a @ fv)!=(fmove @ fts3 @ fts @ fv)), inference(split_conjunct,[status(thm)],[c_0_22])).
% 165.27/165.15 thf(c_0_31, plain, ~p1, inference(split_conjunct,[status(thm)],[c_0_23])).
% 165.27/165.15 thf(c_0_32, plain, ![X1:view_e774982825t_unit]:(fmove @ fts_a @ fts @ X1)=(X1), inference(spm,[status(thm)],[c_0_24, c_0_25])).
% 165.27/165.15 thf(c_0_33, plain, ![X1:view_e774982825t_unit, X8:traffic, X6:traffic, X4:traffic]:((fmove @ X4 @ X6 @ (fmove @ X8 @ X4 @ X1))=(fmove @ X8 @ X6 @ X1)|~fabstract @ X4 @ X6|~fabstract @ X8 @ X4), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_26, c_0_27])])).
% 165.27/165.15 thf(c_0_34, plain, (fabstract @ fts3 @ fts_a|~p65), inference(split_conjunct,[status(thm)],[c_0_28])).
% 165.27/165.15 thf(c_0_35, plain, p65, inference(split_conjunct,[status(thm)],[ax5])).
% 165.27/165.15 thf(c_0_36, plain, ![X3:cars, X6:traffic, X4:traffic, X8:traffic]:(fabstract @ X4 @ X8|~p44|~fabstract @ X4 @ X6|~fcreate_reservation @ X6 @ X3 @ X8), inference(split_conjunct,[status(thm)],[c_0_29])).
% 165.27/165.15 thf(c_0_37, plain, p44, inference(split_conjunct,[status(thm)],[ax26])).
% 165.27/165.15 thf(c_0_38, plain, ![X198:traffic]:(~p41|fabstract @ X198 @ X198), inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[pax41])])])).
% 165.27/165.15 thf(c_0_39, plain, (fmove @ fts3 @ fts @ fv)!=(fmove @ fts3 @ fts_a @ fv), inference(sr,[status(thm)],[c_0_30, c_0_31])).
% 165.27/165.15 thf(c_0_40, plain, ![X1:view_e774982825t_unit, X4:traffic]:((fmove @ X4 @ fts @ X1)=(fmove @ X4 @ fts_a @ X1)|~fabstract @ fts_a @ fts|~fabstract @ X4 @ fts_a), inference(spm,[status(thm)],[c_0_32, c_0_33])).
% 165.27/165.15 thf(c_0_41, plain, fabstract @ fts3 @ fts_a, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_34, c_0_35])])).
% 165.27/165.15 thf(c_0_42, plain, ![X3:cars, X4:traffic, X6:traffic, X8:traffic]:(fabstract @ X4 @ X6|~fcreate_reservation @ X8 @ X3 @ X6|~fabstract @ X4 @ X8), inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_36, c_0_37])])).
% 165.27/165.15 thf(c_0_43, plain, ![X4:traffic]:(fabstract @ X4 @ X4|~p41), inference(split_conjunct,[status(thm)],[c_0_38])).
% 165.27/165.15 thf(c_0_44, plain, p41, inference(split_conjunct,[status(thm)],[ax29])).
% 165.27/165.15 thf(c_0_45, plain, ~fabstract @ fts_a @ fts, inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_39, c_0_40]), c_0_41])])).
% 165.27/165.15 thf(c_0_46, plain, ![X4:traffic]:(fabstract @ X4 @ fts|~fabstract @ X4 @ fts_a), inference(spm,[status(thm)],[c_0_42, c_0_25])).
% 165.27/165.15 thf(c_0_47, plain, ![X4:traffic]:fabstract @ X4 @ X4, inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_43, c_0_44])])).
% 165.27/165.15 thf(c_0_48, plain, ($false), inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_45, c_0_46]), c_0_47])]), ['proof']).
% 165.27/165.15 thf(1,plain,$false,inference(eprover,[status(thm),assumptions([h0])],[])).
% 165.27/165.15 thf(0,theorem,((((move @ ts3) @ ts_a) @ v) = (((move @ ts3) @ ts) @ v)),inference(contra,[status(thm),contra(discharge,[h0])],[1,h0])).
% 165.27/165.15 % SZS output end Proof
%------------------------------------------------------------------------------