Z3---4.15.1.THM-Prf.s

%------------------------------------------------------------------------------
% File     : Z3---4.15.1
% Problem  : SWC092+1 : TPTP v9.0.0. Released v2.4.0.
% Transfm  : none
% Format   : tptp
% Command  : run_E %s %d THM

% Computer : n007.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 : Sat Jun 21 05:30:08 AM UTC 2025

% Result   : Theorem 9.77s 9.95s
% Output   : Proof 9.85s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12  % Problem    : SWC092+1 : TPTP v9.0.0. Released v2.4.0.
% 0.03/0.12  % Command    : run_E %s %d THM
% 0.13/0.33  % Computer : n007.cluster.edu
% 0.13/0.33  % Model    : x86_64 x86_64
% 0.13/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33  % Memory   : 8042.1875MB
% 0.13/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33  % CPULimit   : 300
% 0.13/0.33  % WCLimit    : 300
% 0.13/0.33  % DateTime   : Fri Jun 20 08:19:05 EDT 2025
% 0.13/0.33  % CPUTime    : 
% 9.77/9.95  % SZS status Theorem
% 9.77/9.95  % SZS output start Proof
% 9.77/9.95  tff(segmentP_type, type, (
% 9.77/9.95     segmentP: ( $i * $i ) > $o)).
% 9.77/9.95  tff(tptp_fun_U_45_type, type, (
% 9.77/9.95     tptp_fun_U_45: $i)).
% 9.77/9.95  tff(app_type, type, (
% 9.77/9.95     app: ( $i * $i ) > $i)).
% 9.77/9.95  tff(tptp_fun_Z_47_type, type, (
% 9.77/9.95     tptp_fun_Z_47: $i)).
% 9.77/9.95  tff(tptp_fun_W_6_type, type, (
% 9.77/9.95     tptp_fun_W_6: ( $i * $i ) > $i)).
% 9.77/9.95  tff(tptp_fun_V_46_type, type, (
% 9.77/9.95     tptp_fun_V_46: $i)).
% 9.77/9.95  tff(neq_type, type, (
% 9.77/9.95     neq: ( $i * $i ) > $o)).
% 9.77/9.95  tff(nil_type, type, (
% 9.77/9.95     nil: $i)).
% 9.77/9.95  tff(ssList_type, type, (
% 9.77/9.95     ssList: $i > $o)).
% 9.77/9.95  tff(lt_type, type, (
% 9.77/9.95     lt: ( $i * $i ) > $o)).
% 9.77/9.95  tff(cons_type, type, (
% 9.77/9.95     cons: ( $i * $i ) > $i)).
% 9.77/9.95  tff(ssItem_type, type, (
% 9.77/9.95     ssItem: $i > $o)).
% 9.77/9.95  tff(strictorderedP_type, type, (
% 9.77/9.95     strictorderedP: $i > $o)).
% 9.77/9.95  tff(rearsegP_type, type, (
% 9.77/9.95     rearsegP: ( $i * $i ) > $o)).
% 9.77/9.95  tff(1,plain,
% 9.77/9.95      ((ssList(U!45) & ((~((~(nil = V!46)) & (nil = U!45))) & ssList(V!46) & strictorderedP(U!45) & (app(U!45, Z!47) = V!46) & ssList(Z!47) & ![X1: $i] : ((~ssItem(X1)) | ![X2: $i] : ((~ssList(X2)) | (~(app(cons(X1, nil), X2) = Z!47)) | ![X3: $i] : ((~ssItem(X3)) | ![X4: $i] : (~(ssList(X4) & (app(X4, cons(X3, nil)) = U!45) & lt(X3, X1)))))) & ssList(U!45) & neq(V!46, nil) & ![Y: $i] : (~(ssList(Y) & neq(Y, nil) & segmentP(V!46, Y) & segmentP(U!45, Y))))) <=> (ssList(U!45) & (~((~(nil = V!46)) & (nil = U!45))) & ssList(V!46) & strictorderedP(U!45) & (app(U!45, Z!47) = V!46) & ssList(Z!47) & ![X1: $i] : ((~ssItem(X1)) | ![X2: $i] : ((~ssList(X2)) | (~(app(cons(X1, nil), X2) = Z!47)) | ![X3: $i] : ((~ssItem(X3)) | ![X4: $i] : (~(ssList(X4) & (app(X4, cons(X3, nil)) = U!45) & lt(X3, X1)))))) & neq(V!46, nil) & ![Y: $i] : (~(ssList(Y) & neq(Y, nil) & segmentP(V!46, Y) & segmentP(U!45, Y))))),
% 9.77/9.95      inference(rewrite,[status(thm)],[])).
% 9.77/9.95  tff(2,plain,
% 9.77/9.95      (((~((~(nil = V!46)) & (nil = U!45))) & ssList(V!46) & (strictorderedP(U!45) & (app(U!45, Z!47) = V!46) & ssList(Z!47) & ![X1: $i] : ((~ssItem(X1)) | ![X2: $i] : ((~ssList(X2)) | (~(app(cons(X1, nil), X2) = Z!47)) | ![X3: $i] : ((~ssItem(X3)) | ![X4: $i] : (~(ssList(X4) & (app(X4, cons(X3, nil)) = U!45) & lt(X3, X1))))))) & ssList(U!45) & neq(V!46, nil) & ![Y: $i] : (~(ssList(Y) & neq(Y, nil) & segmentP(V!46, Y) & segmentP(U!45, Y)))) <=> ((~((~(nil = V!46)) & (nil = U!45))) & ssList(V!46) & strictorderedP(U!45) & (app(U!45, Z!47) = V!46) & ssList(Z!47) & ![X1: $i] : ((~ssItem(X1)) | ![X2: $i] : ((~ssList(X2)) | (~(app(cons(X1, nil), X2) = Z!47)) | ![X3: $i] : ((~ssItem(X3)) | ![X4: $i] : (~(ssList(X4) & (app(X4, cons(X3, nil)) = U!45) & lt(X3, X1)))))) & ssList(U!45) & neq(V!46, nil) & ![Y: $i] : (~(ssList(Y) & neq(Y, nil) & segmentP(V!46, Y) & segmentP(U!45, Y))))),
% 9.77/9.95      inference(rewrite,[status(thm)],[])).
% 9.77/9.95  tff(3,plain,
% 9.77/9.95      ((strictorderedP(U!45) & (app(U!45, Z!47) = V!46) & ssList(Z!47) & ![X1: $i] : ((~ssItem(X1)) | ![X2: $i] : ((~ssList(X2)) | (~(app(cons(X1, nil), X2) = Z!47)) | ![X3: $i] : ((~ssItem(X3)) | ![X4: $i] : (~(ssList(X4) & (app(X4, cons(X3, nil)) = U!45) & lt(X3, X1))))))) <=> (strictorderedP(U!45) & (app(U!45, Z!47) = V!46) & ssList(Z!47) & ![X1: $i] : ((~ssItem(X1)) | ![X2: $i] : ((~ssList(X2)) | (~(app(cons(X1, nil), X2) = Z!47)) | ![X3: $i] : ((~ssItem(X3)) | ![X4: $i] : (~(ssList(X4) & (app(X4, cons(X3, nil)) = U!45) & lt(X3, X1)))))))),
% 9.77/9.95      inference(rewrite,[status(thm)],[])).
% 9.77/9.95  tff(4,plain,
% 9.77/9.95      (((~((~(nil = V!46)) & (nil = U!45))) & ssList(V!46) & (strictorderedP(U!45) & (app(U!45, Z!47) = V!46) & ssList(Z!47) & ![X1: $i] : ((~ssItem(X1)) | ![X2: $i] : ((~ssList(X2)) | (~(app(cons(X1, nil), X2) = Z!47)) | ![X3: $i] : ((~ssItem(X3)) | ![X4: $i] : (~(ssList(X4) & (app(X4, cons(X3, nil)) = U!45) & lt(X3, X1))))))) & ssList(U!45) & neq(V!46, nil) & ![Y: $i] : (~(ssList(Y) & neq(Y, nil) & segmentP(V!46, Y) & segmentP(U!45, Y)))) <=> ((~((~(nil = V!46)) & (nil = U!45))) & ssList(V!46) & (strictorderedP(U!45) & (app(U!45, Z!47) = V!46) & ssList(Z!47) & ![X1: $i] : ((~ssItem(X1)) | ![X2: $i] : ((~ssList(X2)) | (~(app(cons(X1, nil), X2) = Z!47)) | ![X3: $i] : ((~ssItem(X3)) | ![X4: $i] : (~(ssList(X4) & (app(X4, cons(X3, nil)) = U!45) & lt(X3, X1))))))) & ssList(U!45) & neq(V!46, nil) & ![Y: $i] : (~(ssList(Y) & neq(Y, nil) & segmentP(V!46, Y) & segmentP(U!45, Y))))),
% 9.77/9.95      inference(monotonicity,[status(thm)],[3])).
% 9.77/9.95  tff(5,plain,
% 9.77/9.95      (((~((~(nil = V!46)) & (nil = U!45))) & ssList(V!46) & (strictorderedP(U!45) & (app(U!45, Z!47) = V!46) & ssList(Z!47) & ![X1: $i] : ((~ssItem(X1)) | ![X2: $i] : ((~ssList(X2)) | (~(app(cons(X1, nil), X2) = Z!47)) | ![X3: $i] : ((~ssItem(X3)) | ![X4: $i] : (~(ssList(X4) & (app(X4, cons(X3, nil)) = U!45) & lt(X3, X1))))))) & ssList(U!45) & neq(V!46, nil) & ![Y: $i] : (~(ssList(Y) & neq(Y, nil) & segmentP(V!46, Y) & segmentP(U!45, Y)))) <=> ((~((~(nil = V!46)) & (nil = U!45))) & ssList(V!46) & strictorderedP(U!45) & (app(U!45, Z!47) = V!46) & ssList(Z!47) & ![X1: $i] : ((~ssItem(X1)) | ![X2: $i] : ((~ssList(X2)) | (~(app(cons(X1, nil), X2) = Z!47)) | ![X3: $i] : ((~ssItem(X3)) | ![X4: $i] : (~(ssList(X4) & (app(X4, cons(X3, nil)) = U!45) & lt(X3, X1)))))) & ssList(U!45) & neq(V!46, nil) & ![Y: $i] : (~(ssList(Y) & neq(Y, nil) & segmentP(V!46, Y) & segmentP(U!45, Y))))),
% 9.77/9.95      inference(transitivity,[status(thm)],[4, 2])).
% 9.77/9.95  tff(6,plain,
% 9.77/9.95      ((ssList(U!45) & ((~((~(nil = V!46)) & (nil = U!45))) & ssList(V!46) & (strictorderedP(U!45) & (app(U!45, Z!47) = V!46) & ssList(Z!47) & ![X1: $i] : ((~ssItem(X1)) | ![X2: $i] : ((~ssList(X2)) | (~(app(cons(X1, nil), X2) = Z!47)) | ![X3: $i] : ((~ssItem(X3)) | ![X4: $i] : (~(ssList(X4) & (app(X4, cons(X3, nil)) = U!45) & lt(X3, X1))))))) & ssList(U!45) & neq(V!46, nil) & ![Y: $i] : (~(ssList(Y) & neq(Y, nil) & segmentP(V!46, Y) & segmentP(U!45, Y))))) <=> (ssList(U!45) & ((~((~(nil = V!46)) & (nil = U!45))) & ssList(V!46) & strictorderedP(U!45) & (app(U!45, Z!47) = V!46) & ssList(Z!47) & ![X1: $i] : ((~ssItem(X1)) | ![X2: $i] : ((~ssList(X2)) | (~(app(cons(X1, nil), X2) = Z!47)) | ![X3: $i] : ((~ssItem(X3)) | ![X4: $i] : (~(ssList(X4) & (app(X4, cons(X3, nil)) = U!45) & lt(X3, X1)))))) & ssList(U!45) & neq(V!46, nil) & ![Y: $i] : (~(ssList(Y) & neq(Y, nil) & segmentP(V!46, Y) & segmentP(U!45, Y)))))),
% 9.77/9.95      inference(monotonicity,[status(thm)],[5])).
% 9.77/9.95  tff(7,plain,
% 9.77/9.95      ((ssList(U!45) & ((~((~(nil = V!46)) & (nil = U!45))) & ssList(V!46) & (strictorderedP(U!45) & (app(U!45, Z!47) = V!46) & ssList(Z!47) & ![X1: $i] : ((~ssItem(X1)) | ![X2: $i] : ((~ssList(X2)) | (~(app(cons(X1, nil), X2) = Z!47)) | ![X3: $i] : ((~ssItem(X3)) | ![X4: $i] : (~(ssList(X4) & (app(X4, cons(X3, nil)) = U!45) & lt(X3, X1))))))) & ssList(U!45) & neq(V!46, nil) & ![Y: $i] : (~(ssList(Y) & neq(Y, nil) & segmentP(V!46, Y) & segmentP(U!45, Y))))) <=> (ssList(U!45) & (~((~(nil = V!46)) & (nil = U!45))) & ssList(V!46) & strictorderedP(U!45) & (app(U!45, Z!47) = V!46) & ssList(Z!47) & ![X1: $i] : ((~ssItem(X1)) | ![X2: $i] : ((~ssList(X2)) | (~(app(cons(X1, nil), X2) = Z!47)) | ![X3: $i] : ((~ssItem(X3)) | ![X4: $i] : (~(ssList(X4) & (app(X4, cons(X3, nil)) = U!45) & lt(X3, X1)))))) & neq(V!46, nil) & ![Y: $i] : (~(ssList(Y) & neq(Y, nil) & segmentP(V!46, Y) & segmentP(U!45, Y))))),
% 9.77/9.95      inference(transitivity,[status(thm)],[6, 1])).
% 9.77/9.95  tff(8,plain,
% 9.77/9.95      ((~![U: $i] : ((~ssList(U)) | ![V: $i] : (((~(nil = V)) & (nil = U)) | (~ssList(V)) | ![Z: $i] : ((~strictorderedP(U)) | (~(app(U, Z) = V)) | (~ssList(Z)) | ?[X1: $i] : (ssItem(X1) & ?[X2: $i] : (ssList(X2) & (app(cons(X1, nil), X2) = Z) & ?[X3: $i] : (ssItem(X3) & ?[X4: $i] : (ssList(X4) & (app(X4, cons(X3, nil)) = U) & lt(X3, X1)))))) | (~ssList(U)) | (~neq(V, nil)) | ?[Y: $i] : (ssList(Y) & neq(Y, nil) & segmentP(V, Y) & segmentP(U, Y))))) <=> (~![U: $i] : ((~ssList(U)) | ![V: $i] : (((~(nil = V)) & (nil = U)) | (~ssList(V)) | ![Z: $i] : ((~strictorderedP(U)) | (~(app(U, Z) = V)) | (~ssList(Z)) | ?[X1: $i] : (ssItem(X1) & ?[X2: $i] : (ssList(X2) & (app(cons(X1, nil), X2) = Z) & ?[X3: $i] : (ssItem(X3) & ?[X4: $i] : (ssList(X4) & (app(X4, cons(X3, nil)) = U) & lt(X3, X1)))))) | (~ssList(U)) | (~neq(V, nil)) | ?[Y: $i] : (ssList(Y) & neq(Y, nil) & segmentP(V, Y) & segmentP(U, Y)))))),
% 9.77/9.95      inference(rewrite,[status(thm)],[])).
% 9.77/9.95  tff(9,plain,
% 9.77/9.95      ((~![U: $i] : (ssList(U) => ![V: $i] : (ssList(V) => ![W: $i] : (ssList(W) => ![X: $i] : (ssList(X) => ((((((~(V = X)) | (~(U = W))) | (~neq(V, nil))) | ?[Y: $i] : (((ssList(Y) & neq(Y, nil)) & segmentP(V, Y)) & segmentP(U, Y))) | ![Z: $i] : (ssList(Z) => (((~(app(W, Z) = X)) | (~strictorderedP(W))) | ?[X1: $i] : (ssItem(X1) & ?[X2: $i] : ((ssList(X2) & (app(cons(X1, nil), X2) = Z)) & ?[X3: $i] : (ssItem(X3) & ?[X4: $i] : ((ssList(X4) & (app(X4, cons(X3, nil)) = W)) & lt(X3, X1)))))))) | ((~(nil = X)) & (nil = W)))))))) <=> (~![U: $i] : ((~ssList(U)) | ![V: $i] : (((~(nil = V)) & (nil = U)) | (~ssList(V)) | ![Z: $i] : ((~strictorderedP(U)) | (~(app(U, Z) = V)) | (~ssList(Z)) | ?[X1: $i] : (ssItem(X1) & ?[X2: $i] : (ssList(X2) & (app(cons(X1, nil), X2) = Z) & ?[X3: $i] : (ssItem(X3) & ?[X4: $i] : (ssList(X4) & (app(X4, cons(X3, nil)) = U) & lt(X3, X1)))))) | (~ssList(U)) | (~neq(V, nil)) | ?[Y: $i] : (ssList(Y) & neq(Y, nil) & segmentP(V, Y) & segmentP(U, Y)))))),
% 9.77/9.95      inference(rewrite,[status(thm)],[])).
% 9.77/9.95  tff(10,axiom,(~![U: $i] : (ssList(U) => ![V: $i] : (ssList(V) => ![W: $i] : (ssList(W) => ![X: $i] : (ssList(X) => ((((((~(V = X)) | (~(U = W))) | (~neq(V, nil))) | ?[Y: $i] : (((ssList(Y) & neq(Y, nil)) & segmentP(V, Y)) & segmentP(U, Y))) | ![Z: $i] : (ssList(Z) => (((~(app(W, Z) = X)) | (~strictorderedP(W))) | ?[X1: $i] : (ssItem(X1) & ?[X2: $i] : ((ssList(X2) & (app(cons(X1, nil), X2) = Z)) & ?[X3: $i] : (ssItem(X3) & ?[X4: $i] : ((ssList(X4) & (app(X4, cons(X3, nil)) = W)) & lt(X3, X1)))))))) | ((~(nil = X)) & (nil = W)))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','co1')).
% 9.77/9.95  tff(11,plain,
% 9.77/9.95      (~![U: $i] : ((~ssList(U)) | ![V: $i] : (((~(nil = V)) & (nil = U)) | (~ssList(V)) | ![Z: $i] : ((~strictorderedP(U)) | (~(app(U, Z) = V)) | (~ssList(Z)) | ?[X1: $i] : (ssItem(X1) & ?[X2: $i] : (ssList(X2) & (app(cons(X1, nil), X2) = Z) & ?[X3: $i] : (ssItem(X3) & ?[X4: $i] : (ssList(X4) & (app(X4, cons(X3, nil)) = U) & lt(X3, X1)))))) | (~ssList(U)) | (~neq(V, nil)) | ?[Y: $i] : (ssList(Y) & neq(Y, nil) & segmentP(V, Y) & segmentP(U, Y))))),
% 9.77/9.95      inference(modus_ponens,[status(thm)],[10, 9])).
% 9.77/9.95  tff(12,plain,
% 9.77/9.95      (~![U: $i] : ((~ssList(U)) | ![V: $i] : (((~(nil = V)) & (nil = U)) | (~ssList(V)) | ![Z: $i] : ((~strictorderedP(U)) | (~(app(U, Z) = V)) | (~ssList(Z)) | ?[X1: $i] : (ssItem(X1) & ?[X2: $i] : (ssList(X2) & (app(cons(X1, nil), X2) = Z) & ?[X3: $i] : (ssItem(X3) & ?[X4: $i] : (ssList(X4) & (app(X4, cons(X3, nil)) = U) & lt(X3, X1)))))) | (~ssList(U)) | (~neq(V, nil)) | ?[Y: $i] : (ssList(Y) & neq(Y, nil) & segmentP(V, Y) & segmentP(U, Y))))),
% 9.77/9.95      inference(modus_ponens,[status(thm)],[11, 8])).
% 9.77/9.95  tff(13,plain,
% 9.77/9.95      (~![U: $i] : ((~ssList(U)) | ![V: $i] : (((~(nil = V)) & (nil = U)) | (~ssList(V)) | ![Z: $i] : ((~strictorderedP(U)) | (~(app(U, Z) = V)) | (~ssList(Z)) | ?[X1: $i] : (ssItem(X1) & ?[X2: $i] : (ssList(X2) & (app(cons(X1, nil), X2) = Z) & ?[X3: $i] : (ssItem(X3) & ?[X4: $i] : (ssList(X4) & (app(X4, cons(X3, nil)) = U) & lt(X3, X1)))))) | (~ssList(U)) | (~neq(V, nil)) | ?[Y: $i] : (ssList(Y) & neq(Y, nil) & segmentP(V, Y) & segmentP(U, Y))))),
% 9.77/9.95      inference(modus_ponens,[status(thm)],[12, 8])).
% 9.77/9.95  tff(14,plain,
% 9.77/9.95      (~![U: $i] : ((~ssList(U)) | ![V: $i] : (((~(nil = V)) & (nil = U)) | (~ssList(V)) | ![Z: $i] : ((~strictorderedP(U)) | (~(app(U, Z) = V)) | (~ssList(Z)) | ?[X1: $i] : (ssItem(X1) & ?[X2: $i] : (ssList(X2) & (app(cons(X1, nil), X2) = Z) & ?[X3: $i] : (ssItem(X3) & ?[X4: $i] : (ssList(X4) & (app(X4, cons(X3, nil)) = U) & lt(X3, X1)))))) | (~ssList(U)) | (~neq(V, nil)) | ?[Y: $i] : (ssList(Y) & neq(Y, nil) & segmentP(V, Y) & segmentP(U, Y))))),
% 9.77/9.95      inference(modus_ponens,[status(thm)],[13, 8])).
% 9.77/9.95  tff(15,plain,
% 9.77/9.95      (ssList(U!45) & (~((~(nil = V!46)) & (nil = U!45))) & ssList(V!46) & strictorderedP(U!45) & (app(U!45, Z!47) = V!46) & ssList(Z!47) & ![X1: $i] : ((~ssItem(X1)) | ![X2: $i] : ((~ssList(X2)) | (~(app(cons(X1, nil), X2) = Z!47)) | ![X3: $i] : ((~ssItem(X3)) | ![X4: $i] : (~(ssList(X4) & (app(X4, cons(X3, nil)) = U!45) & lt(X3, X1)))))) & neq(V!46, nil) & ![Y: $i] : (~(ssList(Y) & neq(Y, nil) & segmentP(V!46, Y) & segmentP(U!45, Y)))),
% 9.77/9.95      inference(modus_ponens,[status(thm)],[14, 7])).
% 9.77/9.95  tff(16,plain,
% 9.77/9.95      (app(U!45, Z!47) = V!46),
% 9.77/9.95      inference(and_elim,[status(thm)],[15])).
% 9.77/9.95  tff(17,plain,
% 9.77/9.95      (ssList(U!45)),
% 9.77/9.95      inference(and_elim,[status(thm)],[15])).
% 9.77/9.95  tff(18,plain,
% 9.77/9.95      (^[U: $i] : refl(((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~rearsegP(U, V)) | (~((~ssList(tptp_fun_W_6(V, U))) | (~(app(tptp_fun_W_6(V, U), V) = U)))))) | (~(rearsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U))))))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~rearsegP(U, V)) | (~((~ssList(tptp_fun_W_6(V, U))) | (~(app(tptp_fun_W_6(V, U), V) = U)))))) | (~(rearsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U))))))))))),
% 9.77/9.95      inference(bind,[status(th)],[])).
% 9.77/9.95  tff(19,plain,
% 9.77/9.95      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~rearsegP(U, V)) | (~((~ssList(tptp_fun_W_6(V, U))) | (~(app(tptp_fun_W_6(V, U), V) = U)))))) | (~(rearsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U))))))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~rearsegP(U, V)) | (~((~ssList(tptp_fun_W_6(V, U))) | (~(app(tptp_fun_W_6(V, U), V) = U)))))) | (~(rearsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U)))))))))),
% 9.77/9.95      inference(quant_intro,[status(thm)],[18])).
% 9.77/9.95  tff(20,plain,
% 9.77/9.95      (^[U: $i] : rewrite(((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~rearsegP(U, V)) | (~((~ssList(tptp_fun_W_6(V, U))) | (~(app(tptp_fun_W_6(V, U), V) = U)))))) | (~(rearsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U))))))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~rearsegP(U, V)) | (~((~ssList(tptp_fun_W_6(V, U))) | (~(app(tptp_fun_W_6(V, U), V) = U)))))) | (~(rearsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U))))))))))),
% 9.77/9.95      inference(bind,[status(th)],[])).
% 9.77/9.95  tff(21,plain,
% 9.77/9.95      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~rearsegP(U, V)) | (~((~ssList(tptp_fun_W_6(V, U))) | (~(app(tptp_fun_W_6(V, U), V) = U)))))) | (~(rearsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U))))))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~rearsegP(U, V)) | (~((~ssList(tptp_fun_W_6(V, U))) | (~(app(tptp_fun_W_6(V, U), V) = U)))))) | (~(rearsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U)))))))))),
% 9.77/9.95      inference(quant_intro,[status(thm)],[20])).
% 9.77/9.95  tff(22,plain,
% 9.77/9.95      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~rearsegP(U, V)) | (~((~ssList(tptp_fun_W_6(V, U))) | (~(app(tptp_fun_W_6(V, U), V) = U)))))) | (~(rearsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U))))))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~rearsegP(U, V)) | (~((~ssList(tptp_fun_W_6(V, U))) | (~(app(tptp_fun_W_6(V, U), V) = U)))))) | (~(rearsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U)))))))))),
% 9.77/9.95      inference(transitivity,[status(thm)],[21, 19])).
% 9.77/9.95  tff(23,plain,
% 9.77/9.95      (^[U: $i] : rewrite(((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (((~rearsegP(U, V)) | (ssList(tptp_fun_W_6(V, U)) & (app(tptp_fun_W_6(V, U), V) = U))) & (rearsegP(U, V) | ![W: $i] : (~(ssList(W) & (app(W, V) = U))))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~rearsegP(U, V)) | (~((~ssList(tptp_fun_W_6(V, U))) | (~(app(tptp_fun_W_6(V, U), V) = U)))))) | (~(rearsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U))))))))))),
% 9.77/9.95      inference(bind,[status(th)],[])).
% 9.77/9.95  tff(24,plain,
% 9.77/9.95      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (((~rearsegP(U, V)) | (ssList(tptp_fun_W_6(V, U)) & (app(tptp_fun_W_6(V, U), V) = U))) & (rearsegP(U, V) | ![W: $i] : (~(ssList(W) & (app(W, V) = U))))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~rearsegP(U, V)) | (~((~ssList(tptp_fun_W_6(V, U))) | (~(app(tptp_fun_W_6(V, U), V) = U)))))) | (~(rearsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U)))))))))),
% 9.77/9.95      inference(quant_intro,[status(thm)],[23])).
% 9.77/9.95  tff(25,plain,
% 9.77/9.95      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (rearsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(W, V) = U))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (rearsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(W, V) = U)))))),
% 9.77/9.95      inference(rewrite,[status(thm)],[])).
% 9.77/9.95  tff(26,plain,
% 9.77/9.95      (^[U: $i] : trans(monotonicity(quant_intro(proof_bind(^[V: $i] : trans(monotonicity(rewrite((rearsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(W, V) = U))) <=> (rearsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(W, V) = U)))), ((ssList(V) => (rearsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(W, V) = U)))) <=> (ssList(V) => (rearsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(W, V) = U)))))), rewrite((ssList(V) => (rearsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(W, V) = U)))) <=> ((~ssList(V)) | (rearsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(W, V) = U))))), ((ssList(V) => (rearsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(W, V) = U)))) <=> ((~ssList(V)) | (rearsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(W, V) = U))))))), (![V: $i] : (ssList(V) => (rearsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(W, V) = U)))) <=> ![V: $i] : ((~ssList(V)) | (rearsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(W, V) = U)))))), ((ssList(U) => ![V: $i] : (ssList(V) => (rearsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(W, V) = U))))) <=> (ssList(U) => ![V: $i] : ((~ssList(V)) | (rearsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(W, V) = U))))))), rewrite((ssList(U) => ![V: $i] : ((~ssList(V)) | (rearsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(W, V) = U))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (rearsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(W, V) = U)))))), ((ssList(U) => ![V: $i] : (ssList(V) => (rearsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(W, V) = U))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (rearsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(W, V) = U)))))))),
% 9.77/9.95      inference(bind,[status(th)],[])).
% 9.77/9.95  tff(27,plain,
% 9.77/9.95      (![U: $i] : (ssList(U) => ![V: $i] : (ssList(V) => (rearsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(W, V) = U))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (rearsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(W, V) = U)))))),
% 9.77/9.95      inference(quant_intro,[status(thm)],[26])).
% 9.77/9.95  tff(28,axiom,(![U: $i] : (ssList(U) => ![V: $i] : (ssList(V) => (rearsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(W, V) = U)))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax','ax6')).
% 9.77/9.95  tff(29,plain,
% 9.77/9.95      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (rearsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(W, V) = U)))))),
% 9.77/9.95      inference(modus_ponens,[status(thm)],[28, 27])).
% 9.77/9.95  tff(30,plain,
% 9.77/9.95      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (rearsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(W, V) = U)))))),
% 9.77/9.95      inference(modus_ponens,[status(thm)],[29, 25])).
% 9.77/9.95  tff(31,plain,(
% 9.77/9.95      ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (((~rearsegP(U, V)) | (ssList(tptp_fun_W_6(V, U)) & (app(tptp_fun_W_6(V, U), V) = U))) & (rearsegP(U, V) | ![W: $i] : (~(ssList(W) & (app(W, V) = U)))))))),
% 9.77/9.95      inference(skolemize,[status(sab)],[30])).
% 9.77/9.95  tff(32,plain,
% 9.77/9.95      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~rearsegP(U, V)) | (~((~ssList(tptp_fun_W_6(V, U))) | (~(app(tptp_fun_W_6(V, U), V) = U)))))) | (~(rearsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U)))))))))),
% 9.77/9.95      inference(modus_ponens,[status(thm)],[31, 24])).
% 9.77/9.95  tff(33,plain,
% 9.77/9.95      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~rearsegP(U, V)) | (~((~ssList(tptp_fun_W_6(V, U))) | (~(app(tptp_fun_W_6(V, U), V) = U)))))) | (~(rearsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U)))))))))),
% 9.77/9.95      inference(modus_ponens,[status(thm)],[32, 22])).
% 9.77/9.95  tff(34,plain,
% 9.77/9.95      (((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~rearsegP(U, V)) | (~((~ssList(tptp_fun_W_6(V, U))) | (~(app(tptp_fun_W_6(V, U), V) = U)))))) | (~(rearsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U)))))))))) | ((~ssList(U!45)) | ![V: $i] : ((~ssList(V)) | (~((~(rearsegP(U!45, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U!45))))) | (~((~rearsegP(U!45, V)) | (~((~ssList(tptp_fun_W_6(V, U!45))) | (~(app(tptp_fun_W_6(V, U!45), V) = U!45))))))))))) <=> ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~rearsegP(U, V)) | (~((~ssList(tptp_fun_W_6(V, U))) | (~(app(tptp_fun_W_6(V, U), V) = U)))))) | (~(rearsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U)))))))))) | (~ssList(U!45)) | ![V: $i] : ((~ssList(V)) | (~((~(rearsegP(U!45, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U!45))))) | (~((~rearsegP(U!45, V)) | (~((~ssList(tptp_fun_W_6(V, U!45))) | (~(app(tptp_fun_W_6(V, U!45), V) = U!45))))))))))),
% 9.77/9.96      inference(rewrite,[status(thm)],[])).
% 9.77/9.96  tff(35,plain,
% 9.77/9.96      (((~ssList(U!45)) | ![V: $i] : ((~ssList(V)) | (~((~((~rearsegP(U!45, V)) | (~((~ssList(tptp_fun_W_6(V, U!45))) | (~(app(tptp_fun_W_6(V, U!45), V) = U!45)))))) | (~(rearsegP(U!45, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U!45))))))))) <=> ((~ssList(U!45)) | ![V: $i] : ((~ssList(V)) | (~((~(rearsegP(U!45, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U!45))))) | (~((~rearsegP(U!45, V)) | (~((~ssList(tptp_fun_W_6(V, U!45))) | (~(app(tptp_fun_W_6(V, U!45), V) = U!45))))))))))),
% 9.77/9.96      inference(rewrite,[status(thm)],[])).
% 9.77/9.96  tff(36,plain,
% 9.77/9.96      (((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~rearsegP(U, V)) | (~((~ssList(tptp_fun_W_6(V, U))) | (~(app(tptp_fun_W_6(V, U), V) = U)))))) | (~(rearsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U)))))))))) | ((~ssList(U!45)) | ![V: $i] : ((~ssList(V)) | (~((~((~rearsegP(U!45, V)) | (~((~ssList(tptp_fun_W_6(V, U!45))) | (~(app(tptp_fun_W_6(V, U!45), V) = U!45)))))) | (~(rearsegP(U!45, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U!45)))))))))) <=> ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~rearsegP(U, V)) | (~((~ssList(tptp_fun_W_6(V, U))) | (~(app(tptp_fun_W_6(V, U), V) = U)))))) | (~(rearsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U)))))))))) | ((~ssList(U!45)) | ![V: $i] : ((~ssList(V)) | (~((~(rearsegP(U!45, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U!45))))) | (~((~rearsegP(U!45, V)) | (~((~ssList(tptp_fun_W_6(V, U!45))) | (~(app(tptp_fun_W_6(V, U!45), V) = U!45)))))))))))),
% 9.77/9.96      inference(monotonicity,[status(thm)],[35])).
% 9.77/9.96  tff(37,plain,
% 9.77/9.96      (((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~rearsegP(U, V)) | (~((~ssList(tptp_fun_W_6(V, U))) | (~(app(tptp_fun_W_6(V, U), V) = U)))))) | (~(rearsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U)))))))))) | ((~ssList(U!45)) | ![V: $i] : ((~ssList(V)) | (~((~((~rearsegP(U!45, V)) | (~((~ssList(tptp_fun_W_6(V, U!45))) | (~(app(tptp_fun_W_6(V, U!45), V) = U!45)))))) | (~(rearsegP(U!45, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U!45)))))))))) <=> ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~rearsegP(U, V)) | (~((~ssList(tptp_fun_W_6(V, U))) | (~(app(tptp_fun_W_6(V, U), V) = U)))))) | (~(rearsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U)))))))))) | (~ssList(U!45)) | ![V: $i] : ((~ssList(V)) | (~((~(rearsegP(U!45, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U!45))))) | (~((~rearsegP(U!45, V)) | (~((~ssList(tptp_fun_W_6(V, U!45))) | (~(app(tptp_fun_W_6(V, U!45), V) = U!45))))))))))),
% 9.77/9.96      inference(transitivity,[status(thm)],[36, 34])).
% 9.77/9.96  tff(38,plain,
% 9.77/9.96      ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~rearsegP(U, V)) | (~((~ssList(tptp_fun_W_6(V, U))) | (~(app(tptp_fun_W_6(V, U), V) = U)))))) | (~(rearsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U)))))))))) | ((~ssList(U!45)) | ![V: $i] : ((~ssList(V)) | (~((~((~rearsegP(U!45, V)) | (~((~ssList(tptp_fun_W_6(V, U!45))) | (~(app(tptp_fun_W_6(V, U!45), V) = U!45)))))) | (~(rearsegP(U!45, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U!45)))))))))),
% 9.77/9.96      inference(quant_inst,[status(thm)],[])).
% 9.77/9.96  tff(39,plain,
% 9.77/9.96      ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~rearsegP(U, V)) | (~((~ssList(tptp_fun_W_6(V, U))) | (~(app(tptp_fun_W_6(V, U), V) = U)))))) | (~(rearsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U)))))))))) | (~ssList(U!45)) | ![V: $i] : ((~ssList(V)) | (~((~(rearsegP(U!45, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U!45))))) | (~((~rearsegP(U!45, V)) | (~((~ssList(tptp_fun_W_6(V, U!45))) | (~(app(tptp_fun_W_6(V, U!45), V) = U!45)))))))))),
% 9.77/9.96      inference(modus_ponens,[status(thm)],[38, 37])).
% 9.77/9.96  tff(40,plain,
% 9.77/9.96      (![V: $i] : ((~ssList(V)) | (~((~(rearsegP(U!45, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U!45))))) | (~((~rearsegP(U!45, V)) | (~((~ssList(tptp_fun_W_6(V, U!45))) | (~(app(tptp_fun_W_6(V, U!45), V) = U!45)))))))))),
% 9.77/9.96      inference(unit_resolution,[status(thm)],[39, 33, 17])).
% 9.77/9.96  tff(41,plain,
% 9.77/9.96      (((~![V: $i] : ((~ssList(V)) | (~((~(rearsegP(U!45, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U!45))))) | (~((~rearsegP(U!45, V)) | (~((~ssList(tptp_fun_W_6(V, U!45))) | (~(app(tptp_fun_W_6(V, U!45), V) = U!45)))))))))) | ((~ssList(U!45)) | (~((~(rearsegP(U!45, U!45) | ![W: $i] : ((~ssList(W)) | (~(app(W, U!45) = U!45))))) | (~((~rearsegP(U!45, U!45)) | (~((~ssList(tptp_fun_W_6(U!45, U!45))) | (~(app(tptp_fun_W_6(U!45, U!45), U!45) = U!45)))))))))) <=> ((~![V: $i] : ((~ssList(V)) | (~((~(rearsegP(U!45, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U!45))))) | (~((~rearsegP(U!45, V)) | (~((~ssList(tptp_fun_W_6(V, U!45))) | (~(app(tptp_fun_W_6(V, U!45), V) = U!45)))))))))) | (~ssList(U!45)) | (~((~(rearsegP(U!45, U!45) | ![W: $i] : ((~ssList(W)) | (~(app(W, U!45) = U!45))))) | (~((~rearsegP(U!45, U!45)) | (~((~ssList(tptp_fun_W_6(U!45, U!45))) | (~(app(tptp_fun_W_6(U!45, U!45), U!45) = U!45)))))))))),
% 9.77/9.96      inference(rewrite,[status(thm)],[])).
% 9.77/9.96  tff(42,plain,
% 9.77/9.96      ((~![V: $i] : ((~ssList(V)) | (~((~(rearsegP(U!45, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U!45))))) | (~((~rearsegP(U!45, V)) | (~((~ssList(tptp_fun_W_6(V, U!45))) | (~(app(tptp_fun_W_6(V, U!45), V) = U!45)))))))))) | ((~ssList(U!45)) | (~((~(rearsegP(U!45, U!45) | ![W: $i] : ((~ssList(W)) | (~(app(W, U!45) = U!45))))) | (~((~rearsegP(U!45, U!45)) | (~((~ssList(tptp_fun_W_6(U!45, U!45))) | (~(app(tptp_fun_W_6(U!45, U!45), U!45) = U!45)))))))))),
% 9.77/9.96      inference(quant_inst,[status(thm)],[])).
% 9.77/9.96  tff(43,plain,
% 9.77/9.96      ((~![V: $i] : ((~ssList(V)) | (~((~(rearsegP(U!45, V) | ![W: $i] : ((~ssList(W)) | (~(app(W, V) = U!45))))) | (~((~rearsegP(U!45, V)) | (~((~ssList(tptp_fun_W_6(V, U!45))) | (~(app(tptp_fun_W_6(V, U!45), V) = U!45)))))))))) | (~ssList(U!45)) | (~((~(rearsegP(U!45, U!45) | ![W: $i] : ((~ssList(W)) | (~(app(W, U!45) = U!45))))) | (~((~rearsegP(U!45, U!45)) | (~((~ssList(tptp_fun_W_6(U!45, U!45))) | (~(app(tptp_fun_W_6(U!45, U!45), U!45) = U!45))))))))),
% 9.77/9.96      inference(modus_ponens,[status(thm)],[42, 41])).
% 9.77/9.96  tff(44,plain,
% 9.77/9.96      (~((~(rearsegP(U!45, U!45) | ![W: $i] : ((~ssList(W)) | (~(app(W, U!45) = U!45))))) | (~((~rearsegP(U!45, U!45)) | (~((~ssList(tptp_fun_W_6(U!45, U!45))) | (~(app(tptp_fun_W_6(U!45, U!45), U!45) = U!45)))))))),
% 9.77/9.96      inference(unit_resolution,[status(thm)],[43, 17, 40])).
% 9.77/9.96  tff(45,plain,
% 9.77/9.96      (((~(rearsegP(U!45, U!45) | ![W: $i] : ((~ssList(W)) | (~(app(W, U!45) = U!45))))) | (~((~rearsegP(U!45, U!45)) | (~((~ssList(tptp_fun_W_6(U!45, U!45))) | (~(app(tptp_fun_W_6(U!45, U!45), U!45) = U!45))))))) | ((~rearsegP(U!45, U!45)) | (~((~ssList(tptp_fun_W_6(U!45, U!45))) | (~(app(tptp_fun_W_6(U!45, U!45), U!45) = U!45)))))),
% 9.77/9.96      inference(tautology,[status(thm)],[])).
% 9.77/9.96  tff(46,plain,
% 9.77/9.96      ((~rearsegP(U!45, U!45)) | (~((~ssList(tptp_fun_W_6(U!45, U!45))) | (~(app(tptp_fun_W_6(U!45, U!45), U!45) = U!45))))),
% 9.77/9.96      inference(unit_resolution,[status(thm)],[45, 44])).
% 9.77/9.96  tff(47,plain,
% 9.77/9.96      (^[U: $i] : refl(((~ssList(U)) | rearsegP(U, U)) <=> ((~ssList(U)) | rearsegP(U, U)))),
% 9.77/9.96      inference(bind,[status(th)],[])).
% 9.77/9.96  tff(48,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | rearsegP(U, U)) <=> ![U: $i] : ((~ssList(U)) | rearsegP(U, U))),
% 9.77/9.96      inference(quant_intro,[status(thm)],[47])).
% 9.77/9.96  tff(49,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | rearsegP(U, U)) <=> ![U: $i] : ((~ssList(U)) | rearsegP(U, U))),
% 9.77/9.96      inference(rewrite,[status(thm)],[])).
% 9.77/9.96  tff(50,plain,
% 9.77/9.96      (^[U: $i] : rewrite((ssList(U) => rearsegP(U, U)) <=> ((~ssList(U)) | rearsegP(U, U)))),
% 9.77/9.96      inference(bind,[status(th)],[])).
% 9.77/9.96  tff(51,plain,
% 9.77/9.96      (![U: $i] : (ssList(U) => rearsegP(U, U)) <=> ![U: $i] : ((~ssList(U)) | rearsegP(U, U))),
% 9.77/9.96      inference(quant_intro,[status(thm)],[50])).
% 9.77/9.96  tff(52,axiom,(![U: $i] : (ssList(U) => rearsegP(U, U))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax','ax49')).
% 9.77/9.96  tff(53,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | rearsegP(U, U))),
% 9.77/9.96      inference(modus_ponens,[status(thm)],[52, 51])).
% 9.77/9.96  tff(54,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | rearsegP(U, U))),
% 9.77/9.96      inference(modus_ponens,[status(thm)],[53, 49])).
% 9.77/9.96  tff(55,plain,(
% 9.77/9.96      ![U: $i] : ((~ssList(U)) | rearsegP(U, U))),
% 9.77/9.96      inference(skolemize,[status(sab)],[54])).
% 9.77/9.96  tff(56,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | rearsegP(U, U))),
% 9.77/9.96      inference(modus_ponens,[status(thm)],[55, 48])).
% 9.77/9.96  tff(57,plain,
% 9.77/9.96      (((~![U: $i] : ((~ssList(U)) | rearsegP(U, U))) | ((~ssList(U!45)) | rearsegP(U!45, U!45))) <=> ((~![U: $i] : ((~ssList(U)) | rearsegP(U, U))) | (~ssList(U!45)) | rearsegP(U!45, U!45))),
% 9.77/9.96      inference(rewrite,[status(thm)],[])).
% 9.77/9.96  tff(58,plain,
% 9.77/9.96      ((~![U: $i] : ((~ssList(U)) | rearsegP(U, U))) | ((~ssList(U!45)) | rearsegP(U!45, U!45))),
% 9.77/9.96      inference(quant_inst,[status(thm)],[])).
% 9.77/9.96  tff(59,plain,
% 9.77/9.96      ((~![U: $i] : ((~ssList(U)) | rearsegP(U, U))) | (~ssList(U!45)) | rearsegP(U!45, U!45)),
% 9.77/9.96      inference(modus_ponens,[status(thm)],[58, 57])).
% 9.77/9.96  tff(60,plain,
% 9.77/9.96      (rearsegP(U!45, U!45)),
% 9.77/9.96      inference(unit_resolution,[status(thm)],[59, 56, 17])).
% 9.77/9.96  tff(61,plain,
% 9.77/9.96      ((~((~rearsegP(U!45, U!45)) | (~((~ssList(tptp_fun_W_6(U!45, U!45))) | (~(app(tptp_fun_W_6(U!45, U!45), U!45) = U!45)))))) | (~rearsegP(U!45, U!45)) | (~((~ssList(tptp_fun_W_6(U!45, U!45))) | (~(app(tptp_fun_W_6(U!45, U!45), U!45) = U!45))))),
% 9.77/9.96      inference(tautology,[status(thm)],[])).
% 9.77/9.96  tff(62,plain,
% 9.77/9.96      ((~((~rearsegP(U!45, U!45)) | (~((~ssList(tptp_fun_W_6(U!45, U!45))) | (~(app(tptp_fun_W_6(U!45, U!45), U!45) = U!45)))))) | (~((~ssList(tptp_fun_W_6(U!45, U!45))) | (~(app(tptp_fun_W_6(U!45, U!45), U!45) = U!45))))),
% 9.77/9.96      inference(unit_resolution,[status(thm)],[61, 60])).
% 9.77/9.96  tff(63,plain,
% 9.77/9.96      (~((~ssList(tptp_fun_W_6(U!45, U!45))) | (~(app(tptp_fun_W_6(U!45, U!45), U!45) = U!45)))),
% 9.77/9.96      inference(unit_resolution,[status(thm)],[62, 46])).
% 9.77/9.96  tff(64,plain,
% 9.77/9.96      (((~ssList(tptp_fun_W_6(U!45, U!45))) | (~(app(tptp_fun_W_6(U!45, U!45), U!45) = U!45))) | (app(tptp_fun_W_6(U!45, U!45), U!45) = U!45)),
% 9.77/9.96      inference(tautology,[status(thm)],[])).
% 9.77/9.96  tff(65,plain,
% 9.77/9.96      (app(tptp_fun_W_6(U!45, U!45), U!45) = U!45),
% 9.77/9.96      inference(unit_resolution,[status(thm)],[64, 63])).
% 9.77/9.96  tff(66,plain,
% 9.77/9.96      (app(app(tptp_fun_W_6(U!45, U!45), U!45), Z!47) = app(U!45, Z!47)),
% 9.77/9.96      inference(monotonicity,[status(thm)],[65])).
% 9.77/9.96  tff(67,plain,
% 9.77/9.96      (app(app(tptp_fun_W_6(U!45, U!45), U!45), Z!47) = V!46),
% 9.77/9.96      inference(transitivity,[status(thm)],[66, 16])).
% 9.77/9.96  tff(68,plain,
% 9.77/9.96      (segmentP(app(app(tptp_fun_W_6(U!45, U!45), U!45), Z!47), U!45) <=> segmentP(V!46, U!45)),
% 9.77/9.96      inference(monotonicity,[status(thm)],[67])).
% 9.77/9.96  tff(69,plain,
% 9.77/9.96      (segmentP(V!46, U!45) <=> segmentP(app(app(tptp_fun_W_6(U!45, U!45), U!45), Z!47), U!45)),
% 9.77/9.96      inference(symmetry,[status(thm)],[68])).
% 9.77/9.96  tff(70,plain,
% 9.77/9.96      ((~segmentP(V!46, U!45)) <=> (~segmentP(app(app(tptp_fun_W_6(U!45, U!45), U!45), Z!47), U!45))),
% 9.77/9.96      inference(monotonicity,[status(thm)],[69])).
% 9.77/9.96  tff(71,plain,
% 9.77/9.96      (^[U: $i] : refl(((~ssList(U)) | segmentP(U, U)) <=> ((~ssList(U)) | segmentP(U, U)))),
% 9.77/9.96      inference(bind,[status(th)],[])).
% 9.77/9.96  tff(72,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | segmentP(U, U)) <=> ![U: $i] : ((~ssList(U)) | segmentP(U, U))),
% 9.77/9.96      inference(quant_intro,[status(thm)],[71])).
% 9.77/9.96  tff(73,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | segmentP(U, U)) <=> ![U: $i] : ((~ssList(U)) | segmentP(U, U))),
% 9.77/9.96      inference(rewrite,[status(thm)],[])).
% 9.77/9.96  tff(74,plain,
% 9.77/9.96      (^[U: $i] : rewrite((ssList(U) => segmentP(U, U)) <=> ((~ssList(U)) | segmentP(U, U)))),
% 9.77/9.96      inference(bind,[status(th)],[])).
% 9.77/9.96  tff(75,plain,
% 9.77/9.96      (![U: $i] : (ssList(U) => segmentP(U, U)) <=> ![U: $i] : ((~ssList(U)) | segmentP(U, U))),
% 9.77/9.96      inference(quant_intro,[status(thm)],[74])).
% 9.77/9.96  tff(76,axiom,(![U: $i] : (ssList(U) => segmentP(U, U))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax','ax55')).
% 9.77/9.96  tff(77,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | segmentP(U, U))),
% 9.77/9.96      inference(modus_ponens,[status(thm)],[76, 75])).
% 9.77/9.96  tff(78,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | segmentP(U, U))),
% 9.77/9.96      inference(modus_ponens,[status(thm)],[77, 73])).
% 9.77/9.96  tff(79,plain,(
% 9.77/9.96      ![U: $i] : ((~ssList(U)) | segmentP(U, U))),
% 9.77/9.96      inference(skolemize,[status(sab)],[78])).
% 9.77/9.96  tff(80,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | segmentP(U, U))),
% 9.77/9.96      inference(modus_ponens,[status(thm)],[79, 72])).
% 9.77/9.96  tff(81,plain,
% 9.77/9.96      (((~![U: $i] : ((~ssList(U)) | segmentP(U, U))) | ((~ssList(U!45)) | segmentP(U!45, U!45))) <=> ((~![U: $i] : ((~ssList(U)) | segmentP(U, U))) | (~ssList(U!45)) | segmentP(U!45, U!45))),
% 9.77/9.96      inference(rewrite,[status(thm)],[])).
% 9.77/9.96  tff(82,plain,
% 9.77/9.96      ((~![U: $i] : ((~ssList(U)) | segmentP(U, U))) | ((~ssList(U!45)) | segmentP(U!45, U!45))),
% 9.77/9.96      inference(quant_inst,[status(thm)],[])).
% 9.77/9.96  tff(83,plain,
% 9.77/9.96      ((~![U: $i] : ((~ssList(U)) | segmentP(U, U))) | (~ssList(U!45)) | segmentP(U!45, U!45)),
% 9.77/9.96      inference(modus_ponens,[status(thm)],[82, 81])).
% 9.77/9.96  tff(84,plain,
% 9.77/9.96      (segmentP(U!45, U!45)),
% 9.77/9.96      inference(unit_resolution,[status(thm)],[83, 80, 17])).
% 9.77/9.96  tff(85,plain,
% 9.77/9.96      (^[U: $i] : refl(((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V))))))),
% 9.77/9.96      inference(bind,[status(th)],[])).
% 9.77/9.96  tff(86,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V)))))),
% 9.77/9.96      inference(quant_intro,[status(thm)],[85])).
% 9.77/9.96  tff(87,plain,
% 9.77/9.96      (^[U: $i] : rewrite(((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V))))))),
% 9.77/9.96      inference(bind,[status(th)],[])).
% 9.77/9.96  tff(88,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V)))))),
% 9.77/9.96      inference(quant_intro,[status(thm)],[87])).
% 9.77/9.96  tff(89,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V)))))),
% 9.77/9.96      inference(transitivity,[status(thm)],[88, 86])).
% 9.77/9.96  tff(90,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V)))))),
% 9.77/9.96      inference(rewrite,[status(thm)],[])).
% 9.77/9.96  tff(91,plain,
% 9.77/9.96      (^[U: $i] : trans(monotonicity(quant_intro(proof_bind(^[V: $i] : trans(monotonicity(trans(rewrite((neq(U, V) <=> (~(U = V))) <=> (~((U = V) <=> neq(U, V)))), rewrite((~((U = V) <=> neq(U, V))) <=> (~((U = V) <=> neq(U, V)))), ((neq(U, V) <=> (~(U = V))) <=> (~((U = V) <=> neq(U, V))))), ((ssList(V) => (neq(U, V) <=> (~(U = V)))) <=> (ssList(V) => (~((U = V) <=> neq(U, V)))))), rewrite((ssList(V) => (~((U = V) <=> neq(U, V)))) <=> ((~ssList(V)) | (~((U = V) <=> neq(U, V))))), ((ssList(V) => (neq(U, V) <=> (~(U = V)))) <=> ((~ssList(V)) | (~((U = V) <=> neq(U, V))))))), (![V: $i] : (ssList(V) => (neq(U, V) <=> (~(U = V)))) <=> ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V)))))), ((ssList(U) => ![V: $i] : (ssList(V) => (neq(U, V) <=> (~(U = V))))) <=> (ssList(U) => ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V))))))), rewrite((ssList(U) => ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V)))))), ((ssList(U) => ![V: $i] : (ssList(V) => (neq(U, V) <=> (~(U = V))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V)))))))),
% 9.77/9.96      inference(bind,[status(th)],[])).
% 9.77/9.96  tff(92,plain,
% 9.77/9.96      (![U: $i] : (ssList(U) => ![V: $i] : (ssList(V) => (neq(U, V) <=> (~(U = V))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V)))))),
% 9.77/9.96      inference(quant_intro,[status(thm)],[91])).
% 9.77/9.96  tff(93,axiom,(![U: $i] : (ssList(U) => ![V: $i] : (ssList(V) => (neq(U, V) <=> (~(U = V)))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax','ax15')).
% 9.77/9.96  tff(94,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V)))))),
% 9.77/9.96      inference(modus_ponens,[status(thm)],[93, 92])).
% 9.77/9.96  tff(95,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V)))))),
% 9.77/9.96      inference(modus_ponens,[status(thm)],[94, 90])).
% 9.77/9.96  tff(96,plain,(
% 9.77/9.96      ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V)))))),
% 9.77/9.96      inference(skolemize,[status(sab)],[95])).
% 9.77/9.96  tff(97,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V)))))),
% 9.77/9.96      inference(modus_ponens,[status(thm)],[96, 89])).
% 9.77/9.96  tff(98,plain,
% 9.77/9.96      (((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V)))))) | ((~ssList(U!45)) | ![V: $i] : ((~ssList(V)) | (~((U!45 = V) <=> neq(U!45, V)))))) <=> ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V)))))) | (~ssList(U!45)) | ![V: $i] : ((~ssList(V)) | (~((U!45 = V) <=> neq(U!45, V)))))),
% 9.77/9.96      inference(rewrite,[status(thm)],[])).
% 9.77/9.96  tff(99,plain,
% 9.77/9.96      ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V)))))) | ((~ssList(U!45)) | ![V: $i] : ((~ssList(V)) | (~((U!45 = V) <=> neq(U!45, V)))))),
% 9.77/9.96      inference(quant_inst,[status(thm)],[])).
% 9.77/9.96  tff(100,plain,
% 9.77/9.96      ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V)))))) | (~ssList(U!45)) | ![V: $i] : ((~ssList(V)) | (~((U!45 = V) <=> neq(U!45, V))))),
% 9.77/9.96      inference(modus_ponens,[status(thm)],[99, 98])).
% 9.77/9.96  tff(101,plain,
% 9.77/9.96      (![V: $i] : ((~ssList(V)) | (~((U!45 = V) <=> neq(U!45, V))))),
% 9.77/9.96      inference(unit_resolution,[status(thm)],[100, 97, 17])).
% 9.77/9.96  tff(102,plain,
% 9.77/9.96      (ssList(nil) <=> ssList(nil)),
% 9.77/9.96      inference(rewrite,[status(thm)],[])).
% 9.77/9.96  tff(103,axiom,(ssList(nil)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax','ax17')).
% 9.77/9.96  tff(104,plain,
% 9.77/9.96      (ssList(nil)),
% 9.77/9.96      inference(modus_ponens,[status(thm)],[103, 102])).
% 9.77/9.96  tff(105,plain,
% 9.77/9.96      (((~![V: $i] : ((~ssList(V)) | (~((U!45 = V) <=> neq(U!45, V))))) | ((~ssList(nil)) | (~((U!45 = nil) <=> neq(U!45, nil))))) <=> ((~![V: $i] : ((~ssList(V)) | (~((U!45 = V) <=> neq(U!45, V))))) | (~ssList(nil)) | (~((U!45 = nil) <=> neq(U!45, nil))))),
% 9.77/9.96      inference(rewrite,[status(thm)],[])).
% 9.77/9.96  tff(106,plain,
% 9.77/9.96      ((~![V: $i] : ((~ssList(V)) | (~((U!45 = V) <=> neq(U!45, V))))) | ((~ssList(nil)) | (~((U!45 = nil) <=> neq(U!45, nil))))),
% 9.77/9.96      inference(quant_inst,[status(thm)],[])).
% 9.77/9.96  tff(107,plain,
% 9.77/9.96      ((~![V: $i] : ((~ssList(V)) | (~((U!45 = V) <=> neq(U!45, V))))) | (~ssList(nil)) | (~((U!45 = nil) <=> neq(U!45, nil)))),
% 9.77/9.96      inference(modus_ponens,[status(thm)],[106, 105])).
% 9.77/9.96  tff(108,plain,
% 9.77/9.96      (~((U!45 = nil) <=> neq(U!45, nil))),
% 9.77/9.96      inference(unit_resolution,[status(thm)],[107, 104, 101])).
% 9.77/9.96  tff(109,plain,
% 9.77/9.96      ((U!45 = nil) <=> (nil = U!45)),
% 9.77/9.96      inference(commutativity,[status(thm)],[])).
% 9.77/9.96  tff(110,plain,
% 9.77/9.96      ((nil = U!45) <=> (U!45 = nil)),
% 9.77/9.96      inference(symmetry,[status(thm)],[109])).
% 9.77/9.96  tff(111,plain,
% 9.77/9.96      ((~(nil = U!45)) <=> (~(U!45 = nil))),
% 9.77/9.96      inference(monotonicity,[status(thm)],[110])).
% 9.77/9.96  tff(112,plain,
% 9.77/9.96      (ssList(V!46)),
% 9.77/9.96      inference(and_elim,[status(thm)],[15])).
% 9.77/9.96  tff(113,plain,
% 9.77/9.96      (^[U: $i] : refl(((~ssList(U)) | (segmentP(nil, U) <=> (nil = U))) <=> ((~ssList(U)) | (segmentP(nil, U) <=> (nil = U))))),
% 9.77/9.96      inference(bind,[status(th)],[])).
% 9.77/9.96  tff(114,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | (segmentP(nil, U) <=> (nil = U))) <=> ![U: $i] : ((~ssList(U)) | (segmentP(nil, U) <=> (nil = U)))),
% 9.77/9.96      inference(quant_intro,[status(thm)],[113])).
% 9.77/9.96  tff(115,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | (segmentP(nil, U) <=> (nil = U))) <=> ![U: $i] : ((~ssList(U)) | (segmentP(nil, U) <=> (nil = U)))),
% 9.77/9.96      inference(rewrite,[status(thm)],[])).
% 9.77/9.96  tff(116,plain,
% 9.77/9.96      (^[U: $i] : rewrite((ssList(U) => (segmentP(nil, U) <=> (nil = U))) <=> ((~ssList(U)) | (segmentP(nil, U) <=> (nil = U))))),
% 9.77/9.96      inference(bind,[status(th)],[])).
% 9.77/9.96  tff(117,plain,
% 9.77/9.96      (![U: $i] : (ssList(U) => (segmentP(nil, U) <=> (nil = U))) <=> ![U: $i] : ((~ssList(U)) | (segmentP(nil, U) <=> (nil = U)))),
% 9.77/9.96      inference(quant_intro,[status(thm)],[116])).
% 9.77/9.96  tff(118,axiom,(![U: $i] : (ssList(U) => (segmentP(nil, U) <=> (nil = U)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax','ax58')).
% 9.77/9.96  tff(119,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | (segmentP(nil, U) <=> (nil = U)))),
% 9.77/9.96      inference(modus_ponens,[status(thm)],[118, 117])).
% 9.77/9.96  tff(120,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | (segmentP(nil, U) <=> (nil = U)))),
% 9.77/9.96      inference(modus_ponens,[status(thm)],[119, 115])).
% 9.77/9.96  tff(121,plain,(
% 9.77/9.96      ![U: $i] : ((~ssList(U)) | (segmentP(nil, U) <=> (nil = U)))),
% 9.77/9.96      inference(skolemize,[status(sab)],[120])).
% 9.77/9.96  tff(122,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | (segmentP(nil, U) <=> (nil = U)))),
% 9.77/9.96      inference(modus_ponens,[status(thm)],[121, 114])).
% 9.77/9.96  tff(123,plain,
% 9.77/9.96      (((~![U: $i] : ((~ssList(U)) | (segmentP(nil, U) <=> (nil = U)))) | ((~ssList(V!46)) | (segmentP(nil, V!46) <=> (nil = V!46)))) <=> ((~![U: $i] : ((~ssList(U)) | (segmentP(nil, U) <=> (nil = U)))) | (~ssList(V!46)) | (segmentP(nil, V!46) <=> (nil = V!46)))),
% 9.77/9.96      inference(rewrite,[status(thm)],[])).
% 9.77/9.96  tff(124,plain,
% 9.77/9.96      ((~![U: $i] : ((~ssList(U)) | (segmentP(nil, U) <=> (nil = U)))) | ((~ssList(V!46)) | (segmentP(nil, V!46) <=> (nil = V!46)))),
% 9.77/9.96      inference(quant_inst,[status(thm)],[])).
% 9.77/9.96  tff(125,plain,
% 9.77/9.96      ((~![U: $i] : ((~ssList(U)) | (segmentP(nil, U) <=> (nil = U)))) | (~ssList(V!46)) | (segmentP(nil, V!46) <=> (nil = V!46))),
% 9.77/9.96      inference(modus_ponens,[status(thm)],[124, 123])).
% 9.77/9.96  tff(126,plain,
% 9.77/9.96      (segmentP(nil, V!46) <=> (nil = V!46)),
% 9.77/9.96      inference(unit_resolution,[status(thm)],[125, 122, 112])).
% 9.77/9.96  tff(127,plain,
% 9.77/9.96      (((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V)))))) | ((~ssList(V!46)) | ![V: $i] : ((~ssList(V)) | (~((V!46 = V) <=> neq(V!46, V)))))) <=> ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V)))))) | (~ssList(V!46)) | ![V: $i] : ((~ssList(V)) | (~((V!46 = V) <=> neq(V!46, V)))))),
% 9.77/9.96      inference(rewrite,[status(thm)],[])).
% 9.77/9.96  tff(128,plain,
% 9.77/9.96      ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V)))))) | ((~ssList(V!46)) | ![V: $i] : ((~ssList(V)) | (~((V!46 = V) <=> neq(V!46, V)))))),
% 9.77/9.96      inference(quant_inst,[status(thm)],[])).
% 9.77/9.96  tff(129,plain,
% 9.77/9.96      ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((U = V) <=> neq(U, V)))))) | (~ssList(V!46)) | ![V: $i] : ((~ssList(V)) | (~((V!46 = V) <=> neq(V!46, V))))),
% 9.77/9.96      inference(modus_ponens,[status(thm)],[128, 127])).
% 9.77/9.96  tff(130,plain,
% 9.77/9.96      (![V: $i] : ((~ssList(V)) | (~((V!46 = V) <=> neq(V!46, V))))),
% 9.77/9.96      inference(unit_resolution,[status(thm)],[129, 97, 112])).
% 9.77/9.96  tff(131,plain,
% 9.77/9.96      (((~![V: $i] : ((~ssList(V)) | (~((V!46 = V) <=> neq(V!46, V))))) | ((~ssList(nil)) | (~((V!46 = nil) <=> neq(V!46, nil))))) <=> ((~![V: $i] : ((~ssList(V)) | (~((V!46 = V) <=> neq(V!46, V))))) | (~ssList(nil)) | (~((V!46 = nil) <=> neq(V!46, nil))))),
% 9.77/9.96      inference(rewrite,[status(thm)],[])).
% 9.77/9.96  tff(132,plain,
% 9.77/9.96      ((~![V: $i] : ((~ssList(V)) | (~((V!46 = V) <=> neq(V!46, V))))) | ((~ssList(nil)) | (~((V!46 = nil) <=> neq(V!46, nil))))),
% 9.77/9.96      inference(quant_inst,[status(thm)],[])).
% 9.77/9.96  tff(133,plain,
% 9.77/9.96      ((~![V: $i] : ((~ssList(V)) | (~((V!46 = V) <=> neq(V!46, V))))) | (~ssList(nil)) | (~((V!46 = nil) <=> neq(V!46, nil)))),
% 9.77/9.96      inference(modus_ponens,[status(thm)],[132, 131])).
% 9.77/9.96  tff(134,plain,
% 9.77/9.96      (~((V!46 = nil) <=> neq(V!46, nil))),
% 9.77/9.96      inference(unit_resolution,[status(thm)],[133, 104, 130])).
% 9.77/9.96  tff(135,plain,
% 9.77/9.96      (neq(V!46, nil)),
% 9.77/9.96      inference(and_elim,[status(thm)],[15])).
% 9.77/9.96  tff(136,plain,
% 9.77/9.96      (((V!46 = nil) <=> neq(V!46, nil)) | (~(V!46 = nil)) | (~neq(V!46, nil))),
% 9.77/9.96      inference(tautology,[status(thm)],[])).
% 9.77/9.96  tff(137,plain,
% 9.77/9.96      (((V!46 = nil) <=> neq(V!46, nil)) | (~(V!46 = nil))),
% 9.77/9.96      inference(unit_resolution,[status(thm)],[136, 135])).
% 9.77/9.96  tff(138,plain,
% 9.77/9.96      (~(V!46 = nil)),
% 9.77/9.96      inference(unit_resolution,[status(thm)],[137, 134])).
% 9.77/9.96  tff(139,plain,
% 9.77/9.96      (^[U: $i] : refl(((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~segmentP(U, V)) | (~segmentP(V, U)))) <=> ((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~segmentP(U, V)) | (~segmentP(V, U)))))),
% 9.77/9.96      inference(bind,[status(th)],[])).
% 9.77/9.96  tff(140,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~segmentP(U, V)) | (~segmentP(V, U)))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~segmentP(U, V)) | (~segmentP(V, U))))),
% 9.77/9.96      inference(quant_intro,[status(thm)],[139])).
% 9.77/9.96  tff(141,plain,
% 9.77/9.96      (^[U: $i] : rewrite(((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~segmentP(U, V)) | (~segmentP(V, U)))) <=> ((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~segmentP(U, V)) | (~segmentP(V, U)))))),
% 9.77/9.96      inference(bind,[status(th)],[])).
% 9.77/9.96  tff(142,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~segmentP(U, V)) | (~segmentP(V, U)))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~segmentP(U, V)) | (~segmentP(V, U))))),
% 9.77/9.96      inference(quant_intro,[status(thm)],[141])).
% 9.77/9.96  tff(143,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~segmentP(U, V)) | (~segmentP(V, U)))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~segmentP(U, V)) | (~segmentP(V, U))))),
% 9.77/9.96      inference(transitivity,[status(thm)],[142, 140])).
% 9.77/9.96  tff(144,plain,
% 9.77/9.96      (^[U: $i] : rewrite(((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~(segmentP(U, V) & segmentP(V, U))))) <=> ((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~segmentP(U, V)) | (~segmentP(V, U)))))),
% 9.77/9.96      inference(bind,[status(th)],[])).
% 9.77/9.96  tff(145,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~(segmentP(U, V) & segmentP(V, U))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~segmentP(U, V)) | (~segmentP(V, U))))),
% 9.77/9.96      inference(quant_intro,[status(thm)],[144])).
% 9.77/9.96  tff(146,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~(segmentP(U, V) & segmentP(V, U))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~(segmentP(U, V) & segmentP(V, U)))))),
% 9.77/9.96      inference(rewrite,[status(thm)],[])).
% 9.77/9.96  tff(147,plain,
% 9.77/9.96      (^[U: $i] : trans(monotonicity(quant_intro(proof_bind(^[V: $i] : trans(monotonicity(rewrite(((segmentP(U, V) & segmentP(V, U)) => (U = V)) <=> ((~(segmentP(U, V) & segmentP(V, U))) | (U = V))), ((ssList(V) => ((segmentP(U, V) & segmentP(V, U)) => (U = V))) <=> (ssList(V) => ((~(segmentP(U, V) & segmentP(V, U))) | (U = V))))), rewrite((ssList(V) => ((~(segmentP(U, V) & segmentP(V, U))) | (U = V))) <=> ((U = V) | (~ssList(V)) | (~(segmentP(U, V) & segmentP(V, U))))), ((ssList(V) => ((segmentP(U, V) & segmentP(V, U)) => (U = V))) <=> ((U = V) | (~ssList(V)) | (~(segmentP(U, V) & segmentP(V, U))))))), (![V: $i] : (ssList(V) => ((segmentP(U, V) & segmentP(V, U)) => (U = V))) <=> ![V: $i] : ((U = V) | (~ssList(V)) | (~(segmentP(U, V) & segmentP(V, U)))))), ((ssList(U) => ![V: $i] : (ssList(V) => ((segmentP(U, V) & segmentP(V, U)) => (U = V)))) <=> (ssList(U) => ![V: $i] : ((U = V) | (~ssList(V)) | (~(segmentP(U, V) & segmentP(V, U))))))), rewrite((ssList(U) => ![V: $i] : ((U = V) | (~ssList(V)) | (~(segmentP(U, V) & segmentP(V, U))))) <=> ((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~(segmentP(U, V) & segmentP(V, U)))))), ((ssList(U) => ![V: $i] : (ssList(V) => ((segmentP(U, V) & segmentP(V, U)) => (U = V)))) <=> ((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~(segmentP(U, V) & segmentP(V, U)))))))),
% 9.77/9.96      inference(bind,[status(th)],[])).
% 9.77/9.96  tff(148,plain,
% 9.77/9.96      (![U: $i] : (ssList(U) => ![V: $i] : (ssList(V) => ((segmentP(U, V) & segmentP(V, U)) => (U = V)))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~(segmentP(U, V) & segmentP(V, U)))))),
% 9.77/9.96      inference(quant_intro,[status(thm)],[147])).
% 9.77/9.96  tff(149,axiom,(![U: $i] : (ssList(U) => ![V: $i] : (ssList(V) => ((segmentP(U, V) & segmentP(V, U)) => (U = V))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax','ax54')).
% 9.77/9.96  tff(150,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~(segmentP(U, V) & segmentP(V, U)))))),
% 9.77/9.96      inference(modus_ponens,[status(thm)],[149, 148])).
% 9.77/9.96  tff(151,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~(segmentP(U, V) & segmentP(V, U)))))),
% 9.77/9.96      inference(modus_ponens,[status(thm)],[150, 146])).
% 9.77/9.96  tff(152,plain,(
% 9.77/9.96      ![U: $i] : ((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~(segmentP(U, V) & segmentP(V, U)))))),
% 9.77/9.96      inference(skolemize,[status(sab)],[151])).
% 9.77/9.96  tff(153,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~segmentP(U, V)) | (~segmentP(V, U))))),
% 9.77/9.96      inference(modus_ponens,[status(thm)],[152, 145])).
% 9.77/9.96  tff(154,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~segmentP(U, V)) | (~segmentP(V, U))))),
% 9.77/9.96      inference(modus_ponens,[status(thm)],[153, 143])).
% 9.77/9.96  tff(155,plain,
% 9.77/9.96      (((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~segmentP(U, V)) | (~segmentP(V, U))))) | ((~ssList(V!46)) | ![V: $i] : ((~ssList(V)) | (~segmentP(V!46, V)) | (V!46 = V) | (~segmentP(V, V!46))))) <=> ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~segmentP(U, V)) | (~segmentP(V, U))))) | (~ssList(V!46)) | ![V: $i] : ((~ssList(V)) | (~segmentP(V!46, V)) | (V!46 = V) | (~segmentP(V, V!46))))),
% 9.77/9.96      inference(rewrite,[status(thm)],[])).
% 9.77/9.96  tff(156,plain,
% 9.77/9.96      (((~ssList(V!46)) | ![V: $i] : ((V!46 = V) | (~ssList(V)) | (~segmentP(V!46, V)) | (~segmentP(V, V!46)))) <=> ((~ssList(V!46)) | ![V: $i] : ((~ssList(V)) | (~segmentP(V!46, V)) | (V!46 = V) | (~segmentP(V, V!46))))),
% 9.77/9.96      inference(rewrite,[status(thm)],[])).
% 9.77/9.96  tff(157,plain,
% 9.77/9.96      (((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~segmentP(U, V)) | (~segmentP(V, U))))) | ((~ssList(V!46)) | ![V: $i] : ((V!46 = V) | (~ssList(V)) | (~segmentP(V!46, V)) | (~segmentP(V, V!46))))) <=> ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~segmentP(U, V)) | (~segmentP(V, U))))) | ((~ssList(V!46)) | ![V: $i] : ((~ssList(V)) | (~segmentP(V!46, V)) | (V!46 = V) | (~segmentP(V, V!46)))))),
% 9.77/9.96      inference(monotonicity,[status(thm)],[156])).
% 9.77/9.96  tff(158,plain,
% 9.77/9.96      (((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~segmentP(U, V)) | (~segmentP(V, U))))) | ((~ssList(V!46)) | ![V: $i] : ((V!46 = V) | (~ssList(V)) | (~segmentP(V!46, V)) | (~segmentP(V, V!46))))) <=> ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~segmentP(U, V)) | (~segmentP(V, U))))) | (~ssList(V!46)) | ![V: $i] : ((~ssList(V)) | (~segmentP(V!46, V)) | (V!46 = V) | (~segmentP(V, V!46))))),
% 9.77/9.96      inference(transitivity,[status(thm)],[157, 155])).
% 9.77/9.96  tff(159,plain,
% 9.77/9.96      ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~segmentP(U, V)) | (~segmentP(V, U))))) | ((~ssList(V!46)) | ![V: $i] : ((V!46 = V) | (~ssList(V)) | (~segmentP(V!46, V)) | (~segmentP(V, V!46))))),
% 9.77/9.96      inference(quant_inst,[status(thm)],[])).
% 9.77/9.96  tff(160,plain,
% 9.77/9.96      ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((U = V) | (~ssList(V)) | (~segmentP(U, V)) | (~segmentP(V, U))))) | (~ssList(V!46)) | ![V: $i] : ((~ssList(V)) | (~segmentP(V!46, V)) | (V!46 = V) | (~segmentP(V, V!46)))),
% 9.77/9.96      inference(modus_ponens,[status(thm)],[159, 158])).
% 9.77/9.96  tff(161,plain,
% 9.77/9.96      (![V: $i] : ((~ssList(V)) | (~segmentP(V!46, V)) | (V!46 = V) | (~segmentP(V, V!46)))),
% 9.77/9.96      inference(unit_resolution,[status(thm)],[160, 154, 112])).
% 9.77/9.96  tff(162,plain,
% 9.77/9.96      (^[U: $i] : refl(((~ssList(U)) | segmentP(U, nil)) <=> ((~ssList(U)) | segmentP(U, nil)))),
% 9.77/9.96      inference(bind,[status(th)],[])).
% 9.77/9.96  tff(163,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | segmentP(U, nil)) <=> ![U: $i] : ((~ssList(U)) | segmentP(U, nil))),
% 9.77/9.96      inference(quant_intro,[status(thm)],[162])).
% 9.77/9.96  tff(164,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | segmentP(U, nil)) <=> ![U: $i] : ((~ssList(U)) | segmentP(U, nil))),
% 9.77/9.96      inference(rewrite,[status(thm)],[])).
% 9.77/9.96  tff(165,plain,
% 9.77/9.96      (^[U: $i] : rewrite((ssList(U) => segmentP(U, nil)) <=> ((~ssList(U)) | segmentP(U, nil)))),
% 9.77/9.96      inference(bind,[status(th)],[])).
% 9.77/9.96  tff(166,plain,
% 9.77/9.96      (![U: $i] : (ssList(U) => segmentP(U, nil)) <=> ![U: $i] : ((~ssList(U)) | segmentP(U, nil))),
% 9.77/9.96      inference(quant_intro,[status(thm)],[165])).
% 9.77/9.96  tff(167,axiom,(![U: $i] : (ssList(U) => segmentP(U, nil))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax','ax57')).
% 9.77/9.96  tff(168,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | segmentP(U, nil))),
% 9.77/9.96      inference(modus_ponens,[status(thm)],[167, 166])).
% 9.77/9.96  tff(169,plain,
% 9.77/9.96      (![U: $i] : ((~ssList(U)) | segmentP(U, nil))),
% 9.77/9.96      inference(modus_ponens,[status(thm)],[168, 164])).
% 9.77/9.96  tff(170,plain,(
% 9.77/9.96      ![U: $i] : ((~ssList(U)) | segmentP(U, nil))),
% 9.77/9.96      inference(skolemize,[status(sab)],[169])).
% 9.77/9.97  tff(171,plain,
% 9.77/9.97      (![U: $i] : ((~ssList(U)) | segmentP(U, nil))),
% 9.77/9.97      inference(modus_ponens,[status(thm)],[170, 163])).
% 9.77/9.97  tff(172,plain,
% 9.77/9.97      (((~![U: $i] : ((~ssList(U)) | segmentP(U, nil))) | ((~ssList(V!46)) | segmentP(V!46, nil))) <=> ((~![U: $i] : ((~ssList(U)) | segmentP(U, nil))) | (~ssList(V!46)) | segmentP(V!46, nil))),
% 9.77/9.97      inference(rewrite,[status(thm)],[])).
% 9.77/9.97  tff(173,plain,
% 9.77/9.97      ((~![U: $i] : ((~ssList(U)) | segmentP(U, nil))) | ((~ssList(V!46)) | segmentP(V!46, nil))),
% 9.77/9.97      inference(quant_inst,[status(thm)],[])).
% 9.77/9.97  tff(174,plain,
% 9.77/9.97      ((~![U: $i] : ((~ssList(U)) | segmentP(U, nil))) | (~ssList(V!46)) | segmentP(V!46, nil)),
% 9.77/9.97      inference(modus_ponens,[status(thm)],[173, 172])).
% 9.77/9.97  tff(175,plain,
% 9.77/9.97      (segmentP(V!46, nil)),
% 9.77/9.97      inference(unit_resolution,[status(thm)],[174, 171, 112])).
% 9.77/9.97  tff(176,plain,
% 9.77/9.97      (((~![V: $i] : ((~ssList(V)) | (~segmentP(V!46, V)) | (V!46 = V) | (~segmentP(V, V!46)))) | ((~ssList(nil)) | (~segmentP(V!46, nil)) | (~segmentP(nil, V!46)) | (V!46 = nil))) <=> ((~![V: $i] : ((~ssList(V)) | (~segmentP(V!46, V)) | (V!46 = V) | (~segmentP(V, V!46)))) | (~ssList(nil)) | (~segmentP(V!46, nil)) | (~segmentP(nil, V!46)) | (V!46 = nil))),
% 9.77/9.97      inference(rewrite,[status(thm)],[])).
% 9.77/9.97  tff(177,plain,
% 9.77/9.97      (((~ssList(nil)) | (~segmentP(V!46, nil)) | (V!46 = nil) | (~segmentP(nil, V!46))) <=> ((~ssList(nil)) | (~segmentP(V!46, nil)) | (~segmentP(nil, V!46)) | (V!46 = nil))),
% 9.77/9.97      inference(rewrite,[status(thm)],[])).
% 9.77/9.97  tff(178,plain,
% 9.77/9.97      (((~![V: $i] : ((~ssList(V)) | (~segmentP(V!46, V)) | (V!46 = V) | (~segmentP(V, V!46)))) | ((~ssList(nil)) | (~segmentP(V!46, nil)) | (V!46 = nil) | (~segmentP(nil, V!46)))) <=> ((~![V: $i] : ((~ssList(V)) | (~segmentP(V!46, V)) | (V!46 = V) | (~segmentP(V, V!46)))) | ((~ssList(nil)) | (~segmentP(V!46, nil)) | (~segmentP(nil, V!46)) | (V!46 = nil)))),
% 9.77/9.97      inference(monotonicity,[status(thm)],[177])).
% 9.77/9.97  tff(179,plain,
% 9.77/9.97      (((~![V: $i] : ((~ssList(V)) | (~segmentP(V!46, V)) | (V!46 = V) | (~segmentP(V, V!46)))) | ((~ssList(nil)) | (~segmentP(V!46, nil)) | (V!46 = nil) | (~segmentP(nil, V!46)))) <=> ((~![V: $i] : ((~ssList(V)) | (~segmentP(V!46, V)) | (V!46 = V) | (~segmentP(V, V!46)))) | (~ssList(nil)) | (~segmentP(V!46, nil)) | (~segmentP(nil, V!46)) | (V!46 = nil))),
% 9.77/9.97      inference(transitivity,[status(thm)],[178, 176])).
% 9.77/9.97  tff(180,plain,
% 9.77/9.97      ((~![V: $i] : ((~ssList(V)) | (~segmentP(V!46, V)) | (V!46 = V) | (~segmentP(V, V!46)))) | ((~ssList(nil)) | (~segmentP(V!46, nil)) | (V!46 = nil) | (~segmentP(nil, V!46)))),
% 9.77/9.97      inference(quant_inst,[status(thm)],[])).
% 9.77/9.97  tff(181,plain,
% 9.77/9.97      ((~![V: $i] : ((~ssList(V)) | (~segmentP(V!46, V)) | (V!46 = V) | (~segmentP(V, V!46)))) | (~ssList(nil)) | (~segmentP(V!46, nil)) | (~segmentP(nil, V!46)) | (V!46 = nil)),
% 9.77/9.97      inference(modus_ponens,[status(thm)],[180, 179])).
% 9.77/9.97  tff(182,plain,
% 9.77/9.97      ((~segmentP(nil, V!46)) | (V!46 = nil)),
% 9.77/9.97      inference(unit_resolution,[status(thm)],[181, 104, 175, 161])).
% 9.77/9.97  tff(183,plain,
% 9.77/9.97      (~segmentP(nil, V!46)),
% 9.77/9.97      inference(unit_resolution,[status(thm)],[182, 138])).
% 9.77/9.97  tff(184,plain,
% 9.77/9.97      ((~(segmentP(nil, V!46) <=> (nil = V!46))) | segmentP(nil, V!46) | (~(nil = V!46))),
% 9.77/9.97      inference(tautology,[status(thm)],[])).
% 9.77/9.97  tff(185,plain,
% 9.77/9.97      (~(nil = V!46)),
% 9.77/9.97      inference(unit_resolution,[status(thm)],[184, 183, 126])).
% 9.77/9.97  tff(186,plain,
% 9.77/9.97      ((~(~((nil = V!46) | (~(nil = U!45))))) <=> ((nil = V!46) | (~(nil = U!45)))),
% 9.77/9.97      inference(rewrite,[status(thm)],[])).
% 9.77/9.97  tff(187,plain,
% 9.77/9.97      (((~(nil = V!46)) & (nil = U!45)) <=> (~((nil = V!46) | (~(nil = U!45))))),
% 9.77/9.97      inference(rewrite,[status(thm)],[])).
% 9.77/9.97  tff(188,plain,
% 9.77/9.97      ((~((~(nil = V!46)) & (nil = U!45))) <=> (~(~((nil = V!46) | (~(nil = U!45)))))),
% 9.77/9.97      inference(monotonicity,[status(thm)],[187])).
% 9.77/9.97  tff(189,plain,
% 9.77/9.97      ((~((~(nil = V!46)) & (nil = U!45))) <=> ((nil = V!46) | (~(nil = U!45)))),
% 9.77/9.97      inference(transitivity,[status(thm)],[188, 186])).
% 9.77/9.97  tff(190,plain,
% 9.77/9.97      (~((~(nil = V!46)) & (nil = U!45))),
% 9.77/9.97      inference(and_elim,[status(thm)],[15])).
% 9.77/9.97  tff(191,plain,
% 9.77/9.97      ((nil = V!46) | (~(nil = U!45))),
% 9.77/9.97      inference(modus_ponens,[status(thm)],[190, 189])).
% 9.77/9.97  tff(192,plain,
% 9.77/9.97      (~(nil = U!45)),
% 9.77/9.97      inference(unit_resolution,[status(thm)],[191, 185])).
% 9.77/9.97  tff(193,plain,
% 9.77/9.97      (~(U!45 = nil)),
% 9.77/9.97      inference(modus_ponens,[status(thm)],[192, 111])).
% 9.77/9.97  tff(194,plain,
% 9.77/9.97      (((U!45 = nil) <=> neq(U!45, nil)) | (U!45 = nil) | neq(U!45, nil)),
% 9.77/9.97      inference(tautology,[status(thm)],[])).
% 9.77/9.97  tff(195,plain,
% 9.77/9.97      (neq(U!45, nil)),
% 9.77/9.97      inference(unit_resolution,[status(thm)],[194, 193, 108])).
% 9.77/9.97  tff(196,plain,
% 9.77/9.97      (^[Y: $i] : refl(((~ssList(Y)) | (~neq(Y, nil)) | (~segmentP(V!46, Y)) | (~segmentP(U!45, Y))) <=> ((~ssList(Y)) | (~neq(Y, nil)) | (~segmentP(V!46, Y)) | (~segmentP(U!45, Y))))),
% 9.77/9.97      inference(bind,[status(th)],[])).
% 9.77/9.97  tff(197,plain,
% 9.77/9.97      (![Y: $i] : ((~ssList(Y)) | (~neq(Y, nil)) | (~segmentP(V!46, Y)) | (~segmentP(U!45, Y))) <=> ![Y: $i] : ((~ssList(Y)) | (~neq(Y, nil)) | (~segmentP(V!46, Y)) | (~segmentP(U!45, Y)))),
% 9.77/9.97      inference(quant_intro,[status(thm)],[196])).
% 9.77/9.97  tff(198,plain,
% 9.77/9.97      (^[Y: $i] : trans(monotonicity(rewrite((ssList(Y) & neq(Y, nil) & segmentP(V!46, Y) & segmentP(U!45, Y)) <=> (~((~ssList(Y)) | (~neq(Y, nil)) | (~segmentP(V!46, Y)) | (~segmentP(U!45, Y))))), ((~(ssList(Y) & neq(Y, nil) & segmentP(V!46, Y) & segmentP(U!45, Y))) <=> (~(~((~ssList(Y)) | (~neq(Y, nil)) | (~segmentP(V!46, Y)) | (~segmentP(U!45, Y))))))), rewrite((~(~((~ssList(Y)) | (~neq(Y, nil)) | (~segmentP(V!46, Y)) | (~segmentP(U!45, Y))))) <=> ((~ssList(Y)) | (~neq(Y, nil)) | (~segmentP(V!46, Y)) | (~segmentP(U!45, Y)))), ((~(ssList(Y) & neq(Y, nil) & segmentP(V!46, Y) & segmentP(U!45, Y))) <=> ((~ssList(Y)) | (~neq(Y, nil)) | (~segmentP(V!46, Y)) | (~segmentP(U!45, Y)))))),
% 9.77/9.97      inference(bind,[status(th)],[])).
% 9.77/9.97  tff(199,plain,
% 9.77/9.97      (![Y: $i] : (~(ssList(Y) & neq(Y, nil) & segmentP(V!46, Y) & segmentP(U!45, Y))) <=> ![Y: $i] : ((~ssList(Y)) | (~neq(Y, nil)) | (~segmentP(V!46, Y)) | (~segmentP(U!45, Y)))),
% 9.77/9.97      inference(quant_intro,[status(thm)],[198])).
% 9.77/9.97  tff(200,plain,
% 9.77/9.97      (![Y: $i] : (~(ssList(Y) & neq(Y, nil) & segmentP(V!46, Y) & segmentP(U!45, Y)))),
% 9.77/9.97      inference(and_elim,[status(thm)],[15])).
% 9.77/9.97  tff(201,plain,
% 9.77/9.97      (![Y: $i] : ((~ssList(Y)) | (~neq(Y, nil)) | (~segmentP(V!46, Y)) | (~segmentP(U!45, Y)))),
% 9.77/9.97      inference(modus_ponens,[status(thm)],[200, 199])).
% 9.77/9.97  tff(202,plain,
% 9.77/9.97      (![Y: $i] : ((~ssList(Y)) | (~neq(Y, nil)) | (~segmentP(V!46, Y)) | (~segmentP(U!45, Y)))),
% 9.77/9.97      inference(modus_ponens,[status(thm)],[201, 197])).
% 9.77/9.97  tff(203,plain,
% 9.77/9.97      (((~![Y: $i] : ((~ssList(Y)) | (~neq(Y, nil)) | (~segmentP(V!46, Y)) | (~segmentP(U!45, Y)))) | ((~ssList(U!45)) | (~neq(U!45, nil)) | (~segmentP(V!46, U!45)) | (~segmentP(U!45, U!45)))) <=> ((~![Y: $i] : ((~ssList(Y)) | (~neq(Y, nil)) | (~segmentP(V!46, Y)) | (~segmentP(U!45, Y)))) | (~ssList(U!45)) | (~neq(U!45, nil)) | (~segmentP(V!46, U!45)) | (~segmentP(U!45, U!45)))),
% 9.77/9.97      inference(rewrite,[status(thm)],[])).
% 9.77/9.97  tff(204,plain,
% 9.77/9.97      ((~![Y: $i] : ((~ssList(Y)) | (~neq(Y, nil)) | (~segmentP(V!46, Y)) | (~segmentP(U!45, Y)))) | ((~ssList(U!45)) | (~neq(U!45, nil)) | (~segmentP(V!46, U!45)) | (~segmentP(U!45, U!45)))),
% 9.77/9.97      inference(quant_inst,[status(thm)],[])).
% 9.77/9.97  tff(205,plain,
% 9.77/9.97      ((~![Y: $i] : ((~ssList(Y)) | (~neq(Y, nil)) | (~segmentP(V!46, Y)) | (~segmentP(U!45, Y)))) | (~ssList(U!45)) | (~neq(U!45, nil)) | (~segmentP(V!46, U!45)) | (~segmentP(U!45, U!45))),
% 9.77/9.97      inference(modus_ponens,[status(thm)],[204, 203])).
% 9.77/9.97  tff(206,plain,
% 9.77/9.97      ((~neq(U!45, nil)) | (~segmentP(V!46, U!45)) | (~segmentP(U!45, U!45))),
% 9.77/9.97      inference(unit_resolution,[status(thm)],[205, 17, 202])).
% 9.77/9.97  tff(207,plain,
% 9.77/9.97      (~segmentP(V!46, U!45)),
% 9.77/9.97      inference(unit_resolution,[status(thm)],[206, 195, 84])).
% 9.77/9.97  tff(208,plain,
% 9.77/9.97      (~segmentP(app(app(tptp_fun_W_6(U!45, U!45), U!45), Z!47), U!45)),
% 9.77/9.97      inference(modus_ponens,[status(thm)],[207, 70])).
% 9.77/9.97  tff(209,plain,
% 9.77/9.97      (((~ssList(tptp_fun_W_6(U!45, U!45))) | (~(app(tptp_fun_W_6(U!45, U!45), U!45) = U!45))) | ssList(tptp_fun_W_6(U!45, U!45))),
% 9.77/9.97      inference(tautology,[status(thm)],[])).
% 9.77/9.97  tff(210,plain,
% 9.77/9.97      (ssList(tptp_fun_W_6(U!45, U!45))),
% 9.77/9.97      inference(unit_resolution,[status(thm)],[209, 63])).
% 9.77/9.97  tff(211,plain,
% 9.77/9.97      (^[U: $i] : refl(((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V)))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V)))))))),
% 9.77/9.97      inference(bind,[status(th)],[])).
% 9.77/9.97  tff(212,plain,
% 9.77/9.97      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V)))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V))))))),
% 9.77/9.97      inference(quant_intro,[status(thm)],[211])).
% 9.77/9.97  tff(213,plain,
% 9.77/9.97      (^[U: $i] : rewrite(((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V)))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V)))))))),
% 9.77/9.97      inference(bind,[status(th)],[])).
% 9.77/9.97  tff(214,plain,
% 9.77/9.97      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V)))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V))))))),
% 9.77/9.97      inference(quant_intro,[status(thm)],[213])).
% 9.77/9.97  tff(215,plain,
% 9.77/9.97      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V)))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V))))))),
% 9.77/9.97      inference(transitivity,[status(thm)],[214, 212])).
% 9.77/9.97  tff(216,plain,
% 9.77/9.97      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V)))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V))))))),
% 9.77/9.97      inference(rewrite,[status(thm)],[])).
% 9.77/9.97  tff(217,plain,
% 9.77/9.97      (^[U: $i] : trans(monotonicity(quant_intro(proof_bind(^[V: $i] : trans(monotonicity(quant_intro(proof_bind(^[W: $i] : trans(monotonicity(quant_intro(proof_bind(^[X: $i] : trans(monotonicity(rewrite((segmentP(U, V) => segmentP(app(app(W, U), X), V)) <=> ((~segmentP(U, V)) | segmentP(app(app(W, U), X), V))), ((ssList(X) => (segmentP(U, V) => segmentP(app(app(W, U), X), V))) <=> (ssList(X) => ((~segmentP(U, V)) | segmentP(app(app(W, U), X), V))))), rewrite((ssList(X) => ((~segmentP(U, V)) | segmentP(app(app(W, U), X), V))) <=> (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V)))), ((ssList(X) => (segmentP(U, V) => segmentP(app(app(W, U), X), V))) <=> (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V)))))), (![X: $i] : (ssList(X) => (segmentP(U, V) => segmentP(app(app(W, U), X), V))) <=> ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V))))), ((ssList(W) => ![X: $i] : (ssList(X) => (segmentP(U, V) => segmentP(app(app(W, U), X), V)))) <=> (ssList(W) => ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V)))))), rewrite((ssList(W) => ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V)))) <=> ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V))))), ((ssList(W) => ![X: $i] : (ssList(X) => (segmentP(U, V) => segmentP(app(app(W, U), X), V)))) <=> ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V))))))), (![W: $i] : (ssList(W) => ![X: $i] : (ssList(X) => (segmentP(U, V) => segmentP(app(app(W, U), X), V)))) <=> ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V)))))), ((ssList(V) => ![W: $i] : (ssList(W) => ![X: $i] : (ssList(X) => (segmentP(U, V) => segmentP(app(app(W, U), X), V))))) <=> (ssList(V) => ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V))))))), rewrite((ssList(V) => ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V))))) <=> ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V)))))), ((ssList(V) => ![W: $i] : (ssList(W) => ![X: $i] : (ssList(X) => (segmentP(U, V) => segmentP(app(app(W, U), X), V))))) <=> ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V)))))))), (![V: $i] : (ssList(V) => ![W: $i] : (ssList(W) => ![X: $i] : (ssList(X) => (segmentP(U, V) => segmentP(app(app(W, U), X), V))))) <=> ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V))))))), ((ssList(U) => ![V: $i] : (ssList(V) => ![W: $i] : (ssList(W) => ![X: $i] : (ssList(X) => (segmentP(U, V) => segmentP(app(app(W, U), X), V)))))) <=> (ssList(U) => ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V)))))))), rewrite((ssList(U) => ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V)))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V))))))), ((ssList(U) => ![V: $i] : (ssList(V) => ![W: $i] : (ssList(W) => ![X: $i] : (ssList(X) => (segmentP(U, V) => segmentP(app(app(W, U), X), V)))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V))))))))),
% 9.77/9.97      inference(bind,[status(th)],[])).
% 9.77/9.97  tff(218,plain,
% 9.77/9.97      (![U: $i] : (ssList(U) => ![V: $i] : (ssList(V) => ![W: $i] : (ssList(W) => ![X: $i] : (ssList(X) => (segmentP(U, V) => segmentP(app(app(W, U), X), V)))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V))))))),
% 9.77/9.97      inference(quant_intro,[status(thm)],[217])).
% 9.77/9.97  tff(219,axiom,(![U: $i] : (ssList(U) => ![V: $i] : (ssList(V) => ![W: $i] : (ssList(W) => ![X: $i] : (ssList(X) => (segmentP(U, V) => segmentP(app(app(W, U), X), V))))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax','ax56')).
% 9.77/9.97  tff(220,plain,
% 9.77/9.97      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V))))))),
% 9.77/9.97      inference(modus_ponens,[status(thm)],[219, 218])).
% 9.77/9.97  tff(221,plain,
% 9.77/9.97      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V))))))),
% 9.77/9.97      inference(modus_ponens,[status(thm)],[220, 216])).
% 9.77/9.97  tff(222,plain,(
% 9.77/9.97      ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V))))))),
% 9.77/9.97      inference(skolemize,[status(sab)],[221])).
% 9.77/9.97  tff(223,plain,
% 9.77/9.97      (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V))))))),
% 9.77/9.97      inference(modus_ponens,[status(thm)],[222, 215])).
% 9.77/9.97  tff(224,plain,
% 9.77/9.97      (((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V))))))) | ((~ssList(U!45)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | segmentP(app(app(W, U!45), X), V) | (~segmentP(U!45, V))))))) <=> ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V))))))) | (~ssList(U!45)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | segmentP(app(app(W, U!45), X), V) | (~segmentP(U!45, V))))))),
% 9.77/9.97      inference(rewrite,[status(thm)],[])).
% 9.77/9.97  tff(225,plain,
% 9.77/9.97      (((~ssList(U!45)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U!45), X), V) | (~ssList(X)) | (~segmentP(U!45, V)))))) <=> ((~ssList(U!45)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | segmentP(app(app(W, U!45), X), V) | (~segmentP(U!45, V))))))),
% 9.77/9.97      inference(rewrite,[status(thm)],[])).
% 9.77/9.97  tff(226,plain,
% 9.77/9.97      (((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V))))))) | ((~ssList(U!45)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U!45), X), V) | (~ssList(X)) | (~segmentP(U!45, V))))))) <=> ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V))))))) | ((~ssList(U!45)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | segmentP(app(app(W, U!45), X), V) | (~segmentP(U!45, V)))))))),
% 9.77/9.97      inference(monotonicity,[status(thm)],[225])).
% 9.77/9.97  tff(227,plain,
% 9.77/9.97      (((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V))))))) | ((~ssList(U!45)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U!45), X), V) | (~ssList(X)) | (~segmentP(U!45, V))))))) <=> ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V))))))) | (~ssList(U!45)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | segmentP(app(app(W, U!45), X), V) | (~segmentP(U!45, V))))))),
% 9.77/9.97      inference(transitivity,[status(thm)],[226, 224])).
% 9.77/9.97  tff(228,plain,
% 9.77/9.97      ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V))))))) | ((~ssList(U!45)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U!45), X), V) | (~ssList(X)) | (~segmentP(U!45, V))))))),
% 9.77/9.97      inference(quant_inst,[status(thm)],[])).
% 9.77/9.97  tff(229,plain,
% 9.77/9.97      ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : (segmentP(app(app(W, U), X), V) | (~ssList(X)) | (~segmentP(U, V))))))) | (~ssList(U!45)) | ![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | segmentP(app(app(W, U!45), X), V) | (~segmentP(U!45, V)))))),
% 9.77/9.97      inference(modus_ponens,[status(thm)],[228, 227])).
% 9.77/9.97  tff(230,plain,
% 9.77/9.97      (![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | segmentP(app(app(W, U!45), X), V) | (~segmentP(U!45, V)))))),
% 9.77/9.97      inference(unit_resolution,[status(thm)],[229, 223, 17])).
% 9.77/9.97  tff(231,plain,
% 9.77/9.97      (((~![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | segmentP(app(app(W, U!45), X), V) | (~segmentP(U!45, V)))))) | ((~ssList(U!45)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~segmentP(U!45, U!45)) | segmentP(app(app(W, U!45), X), U!45))))) <=> ((~![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | segmentP(app(app(W, U!45), X), V) | (~segmentP(U!45, V)))))) | (~ssList(U!45)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~segmentP(U!45, U!45)) | segmentP(app(app(W, U!45), X), U!45))))),
% 9.77/9.97      inference(rewrite,[status(thm)],[])).
% 9.77/9.97  tff(232,plain,
% 9.77/9.97      (((~ssList(U!45)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | segmentP(app(app(W, U!45), X), U!45) | (~segmentP(U!45, U!45))))) <=> ((~ssList(U!45)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~segmentP(U!45, U!45)) | segmentP(app(app(W, U!45), X), U!45))))),
% 9.77/9.97      inference(rewrite,[status(thm)],[])).
% 9.77/9.97  tff(233,plain,
% 9.77/9.97      (((~![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | segmentP(app(app(W, U!45), X), V) | (~segmentP(U!45, V)))))) | ((~ssList(U!45)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | segmentP(app(app(W, U!45), X), U!45) | (~segmentP(U!45, U!45)))))) <=> ((~![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | segmentP(app(app(W, U!45), X), V) | (~segmentP(U!45, V)))))) | ((~ssList(U!45)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~segmentP(U!45, U!45)) | segmentP(app(app(W, U!45), X), U!45)))))),
% 9.77/9.97      inference(monotonicity,[status(thm)],[232])).
% 9.77/9.97  tff(234,plain,
% 9.77/9.97      (((~![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | segmentP(app(app(W, U!45), X), V) | (~segmentP(U!45, V)))))) | ((~ssList(U!45)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | segmentP(app(app(W, U!45), X), U!45) | (~segmentP(U!45, U!45)))))) <=> ((~![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | segmentP(app(app(W, U!45), X), V) | (~segmentP(U!45, V)))))) | (~ssList(U!45)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~segmentP(U!45, U!45)) | segmentP(app(app(W, U!45), X), U!45))))),
% 9.77/9.97      inference(transitivity,[status(thm)],[233, 231])).
% 9.77/9.97  tff(235,plain,
% 9.77/9.97      ((~![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | segmentP(app(app(W, U!45), X), V) | (~segmentP(U!45, V)))))) | ((~ssList(U!45)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | segmentP(app(app(W, U!45), X), U!45) | (~segmentP(U!45, U!45)))))),
% 9.77/9.97      inference(quant_inst,[status(thm)],[])).
% 9.77/9.97  tff(236,plain,
% 9.77/9.97      ((~![V: $i] : ((~ssList(V)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | segmentP(app(app(W, U!45), X), V) | (~segmentP(U!45, V)))))) | (~ssList(U!45)) | ![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~segmentP(U!45, U!45)) | segmentP(app(app(W, U!45), X), U!45)))),
% 9.77/9.97      inference(modus_ponens,[status(thm)],[235, 234])).
% 9.77/9.97  tff(237,plain,
% 9.77/9.97      (![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~segmentP(U!45, U!45)) | segmentP(app(app(W, U!45), X), U!45)))),
% 9.77/9.97      inference(unit_resolution,[status(thm)],[236, 17, 230])).
% 9.77/9.97  tff(238,plain,
% 9.77/9.97      (((~![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~segmentP(U!45, U!45)) | segmentP(app(app(W, U!45), X), U!45)))) | ((~ssList(tptp_fun_W_6(U!45, U!45))) | ![X: $i] : ((~ssList(X)) | (~segmentP(U!45, U!45)) | segmentP(app(app(tptp_fun_W_6(U!45, U!45), U!45), X), U!45)))) <=> ((~![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~segmentP(U!45, U!45)) | segmentP(app(app(W, U!45), X), U!45)))) | (~ssList(tptp_fun_W_6(U!45, U!45))) | ![X: $i] : ((~ssList(X)) | (~segmentP(U!45, U!45)) | segmentP(app(app(tptp_fun_W_6(U!45, U!45), U!45), X), U!45)))),
% 9.77/9.97      inference(rewrite,[status(thm)],[])).
% 9.77/9.97  tff(239,plain,
% 9.77/9.97      ((~![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~segmentP(U!45, U!45)) | segmentP(app(app(W, U!45), X), U!45)))) | ((~ssList(tptp_fun_W_6(U!45, U!45))) | ![X: $i] : ((~ssList(X)) | (~segmentP(U!45, U!45)) | segmentP(app(app(tptp_fun_W_6(U!45, U!45), U!45), X), U!45)))),
% 9.77/9.97      inference(quant_inst,[status(thm)],[])).
% 9.77/9.97  tff(240,plain,
% 9.77/9.97      ((~![W: $i] : ((~ssList(W)) | ![X: $i] : ((~ssList(X)) | (~segmentP(U!45, U!45)) | segmentP(app(app(W, U!45), X), U!45)))) | (~ssList(tptp_fun_W_6(U!45, U!45))) | ![X: $i] : ((~ssList(X)) | (~segmentP(U!45, U!45)) | segmentP(app(app(tptp_fun_W_6(U!45, U!45), U!45), X), U!45))),
% 9.77/9.97      inference(modus_ponens,[status(thm)],[239, 238])).
% 9.77/9.97  tff(241,plain,
% 9.77/9.97      (![X: $i] : ((~ssList(X)) | (~segmentP(U!45, U!45)) | segmentP(app(app(tptp_fun_W_6(U!45, U!45), U!45), X), U!45))),
% 9.77/9.97      inference(unit_resolution,[status(thm)],[240, 237, 210])).
% 9.77/9.97  tff(242,plain,
% 9.77/9.97      (ssList(Z!47)),
% 9.77/9.97      inference(and_elim,[status(thm)],[15])).
% 9.77/9.97  tff(243,plain,
% 9.77/9.97      (((~![X: $i] : ((~ssList(X)) | (~segmentP(U!45, U!45)) | segmentP(app(app(tptp_fun_W_6(U!45, U!45), U!45), X), U!45))) | ((~ssList(Z!47)) | (~segmentP(U!45, U!45)) | segmentP(app(app(tptp_fun_W_6(U!45, U!45), U!45), Z!47), U!45))) <=> ((~![X: $i] : ((~ssList(X)) | (~segmentP(U!45, U!45)) | segmentP(app(app(tptp_fun_W_6(U!45, U!45), U!45), X), U!45))) | (~ssList(Z!47)) | (~segmentP(U!45, U!45)) | segmentP(app(app(tptp_fun_W_6(U!45, U!45), U!45), Z!47), U!45))),
% 9.85/10.01      inference(rewrite,[status(thm)],[])).
% 9.85/10.01  tff(244,plain,
% 9.85/10.01      ((~![X: $i] : ((~ssList(X)) | (~segmentP(U!45, U!45)) | segmentP(app(app(tptp_fun_W_6(U!45, U!45), U!45), X), U!45))) | ((~ssList(Z!47)) | (~segmentP(U!45, U!45)) | segmentP(app(app(tptp_fun_W_6(U!45, U!45), U!45), Z!47), U!45))),
% 9.85/10.01      inference(quant_inst,[status(thm)],[])).
% 9.85/10.01  tff(245,plain,
% 9.85/10.01      ((~![X: $i] : ((~ssList(X)) | (~segmentP(U!45, U!45)) | segmentP(app(app(tptp_fun_W_6(U!45, U!45), U!45), X), U!45))) | (~ssList(Z!47)) | (~segmentP(U!45, U!45)) | segmentP(app(app(tptp_fun_W_6(U!45, U!45), U!45), Z!47), U!45)),
% 9.85/10.01      inference(modus_ponens,[status(thm)],[244, 243])).
% 9.85/10.01  tff(246,plain,
% 9.85/10.01      (segmentP(app(app(tptp_fun_W_6(U!45, U!45), U!45), Z!47), U!45)),
% 9.85/10.01      inference(unit_resolution,[status(thm)],[245, 242, 84, 241])).
% 9.85/10.01  tff(247,plain,
% 9.85/10.01      ($false),
% 9.85/10.01      inference(unit_resolution,[status(thm)],[246, 208])).
% 9.85/10.01  % SZS output end Proof
% 9.85/10.01  % E exiting
%------------------------------------------------------------------------------