%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SWC046+1 : TPTP v9.0.0. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n006.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:01 AM UTC 2025
% Result : Theorem 2.47s 2.70s
% Output : Proof 2.56s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWC046+1 : TPTP v9.0.0. Released v2.4.0.
% 0.07/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n006.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Fri Jun 20 08:06:05 EDT 2025
% 0.12/0.33 % CPUTime :
% 2.47/2.70 % SZS status Theorem
% 2.47/2.70 % SZS output start Proof
% 2.47/2.70 tff(memberP_type, type, (
% 2.47/2.70 memberP: ( $i * $i ) > $o)).
% 2.47/2.70 tff(hd_type, type, (
% 2.47/2.70 hd: $i > $i)).
% 2.47/2.70 tff(tptp_fun_U_45_type, type, (
% 2.47/2.70 tptp_fun_U_45: $i)).
% 2.47/2.70 tff(cons_type, type, (
% 2.47/2.70 cons: ( $i * $i ) > $i)).
% 2.47/2.70 tff(tptp_fun_V_43_type, type, (
% 2.47/2.70 tptp_fun_V_43: $i > $i)).
% 2.47/2.70 tff(tptp_fun_W_44_type, type, (
% 2.47/2.70 tptp_fun_W_44: $i > $i)).
% 2.47/2.70 tff(ssItem_type, type, (
% 2.47/2.70 ssItem: $i > $o)).
% 2.47/2.70 tff(ssList_type, type, (
% 2.47/2.70 ssList: $i > $o)).
% 2.47/2.70 tff(segmentP_type, type, (
% 2.47/2.70 segmentP: ( $i * $i ) > $o)).
% 2.47/2.70 tff(app_type, type, (
% 2.47/2.70 app: ( $i * $i ) > $i)).
% 2.47/2.70 tff(nil_type, type, (
% 2.47/2.70 nil: $i)).
% 2.47/2.70 tff(tptp_fun_Z_46_type, type, (
% 2.47/2.70 tptp_fun_Z_46: $i > $i)).
% 2.47/2.70 tff(1,plain,
% 2.47/2.70 (((~(nil = U!45)) & ssList(U!45) & ssList(nil) & ![Y: $i] : ((~ssItem(Y)) | (((~memberP(U!45, Y)) | (memberP(nil, Y) & ![Z: $i] : (~(ssList(Z) & segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil))))))) & (memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil)))))) | (~memberP(nil, Y)))))) <=> ((~(nil = U!45)) & ssList(U!45) & ssList(nil) & ![Y: $i] : ((~ssItem(Y)) | (((~memberP(U!45, Y)) | (memberP(nil, Y) & ![Z: $i] : (~(ssList(Z) & segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil))))))) & ((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil))))))))))),
% 2.47/2.70 inference(rewrite,[status(thm)],[])).
% 2.47/2.70 tff(2,plain,
% 2.47/2.70 ((~![U: $i] : ((nil = U) | (~ssList(U)) | (~ssList(nil)) | ?[Y: $i] : (ssItem(Y) & ((memberP(U, Y) & ((~memberP(nil, Y)) | ?[Z: $i] : (ssList(Z) & segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))) | ((~memberP(U, Y)) & ![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil))))) & memberP(nil, Y)))))) <=> (~![U: $i] : ((nil = U) | (~ssList(U)) | (~ssList(nil)) | ?[Y: $i] : (ssItem(Y) & ((memberP(U, Y) & ((~memberP(nil, Y)) | ?[Z: $i] : (ssList(Z) & segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))) | ((~memberP(U, Y)) & ![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil))))) & memberP(nil, Y))))))),
% 2.47/2.70 inference(rewrite,[status(thm)],[])).
% 2.47/2.70 tff(3,plain,
% 2.47/2.70 ((~![U: $i] : (ssList(U) => ![V: $i] : (ssList(V) => ![W: $i] : (ssList(W) => ![X: $i] : (ssList(X) => (((((~(nil = V)) | (~(V = X))) | (~(U = W))) | (nil = U)) | ?[Y: $i] : (ssItem(Y) & ((((~memberP(W, Y)) & ![Z: $i] : (ssList(Z) => (~segmentP(X, app(app(cons(Y, nil), Z), cons(Y, nil)))))) & memberP(X, Y)) | (memberP(W, Y) & ((~memberP(X, Y)) | ?[Z: $i] : (ssList(Z) & segmentP(X, app(app(cons(Y, nil), Z), cons(Y, nil)))))))))))))) <=> (~![U: $i] : ((nil = U) | (~ssList(U)) | (~ssList(nil)) | ?[Y: $i] : (ssItem(Y) & ((memberP(U, Y) & ((~memberP(nil, Y)) | ?[Z: $i] : (ssList(Z) & segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))) | ((~memberP(U, Y)) & ![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil))))) & memberP(nil, Y))))))),
% 2.47/2.70 inference(rewrite,[status(thm)],[])).
% 2.47/2.70 tff(4,axiom,(~![U: $i] : (ssList(U) => ![V: $i] : (ssList(V) => ![W: $i] : (ssList(W) => ![X: $i] : (ssList(X) => (((((~(nil = V)) | (~(V = X))) | (~(U = W))) | (nil = U)) | ?[Y: $i] : (ssItem(Y) & ((((~memberP(W, Y)) & ![Z: $i] : (ssList(Z) => (~segmentP(X, app(app(cons(Y, nil), Z), cons(Y, nil)))))) & memberP(X, Y)) | (memberP(W, Y) & ((~memberP(X, Y)) | ?[Z: $i] : (ssList(Z) & segmentP(X, app(app(cons(Y, nil), Z), cons(Y, nil)))))))))))))), file('/export/starexec/sandbox/benchmark/theBenchmark.p','co1')).
% 2.47/2.70 tff(5,plain,
% 2.47/2.70 (~![U: $i] : ((nil = U) | (~ssList(U)) | (~ssList(nil)) | ?[Y: $i] : (ssItem(Y) & ((memberP(U, Y) & ((~memberP(nil, Y)) | ?[Z: $i] : (ssList(Z) & segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))) | ((~memberP(U, Y)) & ![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil))))) & memberP(nil, Y)))))),
% 2.47/2.70 inference(modus_ponens,[status(thm)],[4, 3])).
% 2.47/2.70 tff(6,plain,
% 2.47/2.70 (~![U: $i] : ((nil = U) | (~ssList(U)) | (~ssList(nil)) | ?[Y: $i] : (ssItem(Y) & ((memberP(U, Y) & ((~memberP(nil, Y)) | ?[Z: $i] : (ssList(Z) & segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))) | ((~memberP(U, Y)) & ![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil))))) & memberP(nil, Y)))))),
% 2.47/2.70 inference(modus_ponens,[status(thm)],[5, 2])).
% 2.47/2.70 tff(7,plain,
% 2.47/2.70 (~![U: $i] : ((nil = U) | (~ssList(U)) | (~ssList(nil)) | ?[Y: $i] : (ssItem(Y) & ((memberP(U, Y) & ((~memberP(nil, Y)) | ?[Z: $i] : (ssList(Z) & segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))) | ((~memberP(U, Y)) & ![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil))))) & memberP(nil, Y)))))),
% 2.47/2.70 inference(modus_ponens,[status(thm)],[6, 2])).
% 2.47/2.70 tff(8,plain,
% 2.47/2.70 (~![U: $i] : ((nil = U) | (~ssList(U)) | (~ssList(nil)) | ?[Y: $i] : (ssItem(Y) & ((memberP(U, Y) & ((~memberP(nil, Y)) | ?[Z: $i] : (ssList(Z) & segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))) | ((~memberP(U, Y)) & ![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil))))) & memberP(nil, Y)))))),
% 2.47/2.70 inference(modus_ponens,[status(thm)],[7, 2])).
% 2.47/2.70 tff(9,plain,
% 2.47/2.70 ((~(nil = U!45)) & ssList(U!45) & ssList(nil) & ![Y: $i] : ((~ssItem(Y)) | (((~memberP(U!45, Y)) | (memberP(nil, Y) & ![Z: $i] : (~(ssList(Z) & segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil))))))) & ((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil)))))))))),
% 2.47/2.70 inference(modus_ponens,[status(thm)],[8, 1])).
% 2.47/2.70 tff(10,plain,
% 2.47/2.70 (ssList(U!45)),
% 2.47/2.70 inference(and_elim,[status(thm)],[9])).
% 2.47/2.70 tff(11,plain,
% 2.47/2.70 (~(nil = U!45)),
% 2.47/2.70 inference(and_elim,[status(thm)],[9])).
% 2.47/2.70 tff(12,plain,
% 2.47/2.70 (^[U: $i] : refl(((nil = U) | (~ssList(U)) | (~((~ssList(tptp_fun_V_43(U))) | (~ssItem(tptp_fun_W_44(U))) | (~(cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U))))) <=> ((nil = U) | (~ssList(U)) | (~((~ssList(tptp_fun_V_43(U))) | (~ssItem(tptp_fun_W_44(U))) | (~(cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U))))))),
% 2.47/2.70 inference(bind,[status(th)],[])).
% 2.47/2.70 tff(13,plain,
% 2.47/2.70 (![U: $i] : ((nil = U) | (~ssList(U)) | (~((~ssList(tptp_fun_V_43(U))) | (~ssItem(tptp_fun_W_44(U))) | (~(cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U))))) <=> ![U: $i] : ((nil = U) | (~ssList(U)) | (~((~ssList(tptp_fun_V_43(U))) | (~ssItem(tptp_fun_W_44(U))) | (~(cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U)))))),
% 2.47/2.70 inference(quant_intro,[status(thm)],[12])).
% 2.47/2.70 tff(14,plain,
% 2.47/2.70 (^[U: $i] : trans(monotonicity(rewrite((ssList(tptp_fun_V_43(U)) & ssItem(tptp_fun_W_44(U)) & (cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U)) <=> (~((~ssList(tptp_fun_V_43(U))) | (~ssItem(tptp_fun_W_44(U))) | (~(cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U))))), (((nil = U) | (~ssList(U)) | (ssList(tptp_fun_V_43(U)) & ssItem(tptp_fun_W_44(U)) & (cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U))) <=> ((nil = U) | (~ssList(U)) | (~((~ssList(tptp_fun_V_43(U))) | (~ssItem(tptp_fun_W_44(U))) | (~(cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U))))))), rewrite(((nil = U) | (~ssList(U)) | (~((~ssList(tptp_fun_V_43(U))) | (~ssItem(tptp_fun_W_44(U))) | (~(cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U))))) <=> ((nil = U) | (~ssList(U)) | (~((~ssList(tptp_fun_V_43(U))) | (~ssItem(tptp_fun_W_44(U))) | (~(cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U)))))), (((nil = U) | (~ssList(U)) | (ssList(tptp_fun_V_43(U)) & ssItem(tptp_fun_W_44(U)) & (cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U))) <=> ((nil = U) | (~ssList(U)) | (~((~ssList(tptp_fun_V_43(U))) | (~ssItem(tptp_fun_W_44(U))) | (~(cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U)))))))),
% 2.47/2.70 inference(bind,[status(th)],[])).
% 2.47/2.70 tff(15,plain,
% 2.47/2.70 (![U: $i] : ((nil = U) | (~ssList(U)) | (ssList(tptp_fun_V_43(U)) & ssItem(tptp_fun_W_44(U)) & (cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U))) <=> ![U: $i] : ((nil = U) | (~ssList(U)) | (~((~ssList(tptp_fun_V_43(U))) | (~ssItem(tptp_fun_W_44(U))) | (~(cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U)))))),
% 2.47/2.70 inference(quant_intro,[status(thm)],[14])).
% 2.47/2.70 tff(16,plain,
% 2.47/2.70 (^[U: $i] : trans(monotonicity(rewrite((ssList(tptp_fun_V_43(U)) & (ssItem(tptp_fun_W_44(U)) & (cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U))) <=> (ssList(tptp_fun_V_43(U)) & ssItem(tptp_fun_W_44(U)) & (cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U))), (((ssList(tptp_fun_V_43(U)) & (ssItem(tptp_fun_W_44(U)) & (cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U))) | (nil = U) | (~ssList(U))) <=> ((ssList(tptp_fun_V_43(U)) & ssItem(tptp_fun_W_44(U)) & (cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U)) | (nil = U) | (~ssList(U))))), rewrite(((ssList(tptp_fun_V_43(U)) & ssItem(tptp_fun_W_44(U)) & (cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U)) | (nil = U) | (~ssList(U))) <=> ((nil = U) | (~ssList(U)) | (ssList(tptp_fun_V_43(U)) & ssItem(tptp_fun_W_44(U)) & (cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U)))), (((ssList(tptp_fun_V_43(U)) & (ssItem(tptp_fun_W_44(U)) & (cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U))) | (nil = U) | (~ssList(U))) <=> ((nil = U) | (~ssList(U)) | (ssList(tptp_fun_V_43(U)) & ssItem(tptp_fun_W_44(U)) & (cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U)))))),
% 2.47/2.70 inference(bind,[status(th)],[])).
% 2.47/2.70 tff(17,plain,
% 2.47/2.70 (![U: $i] : ((ssList(tptp_fun_V_43(U)) & (ssItem(tptp_fun_W_44(U)) & (cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U))) | (nil = U) | (~ssList(U))) <=> ![U: $i] : ((nil = U) | (~ssList(U)) | (ssList(tptp_fun_V_43(U)) & ssItem(tptp_fun_W_44(U)) & (cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U)))),
% 2.47/2.70 inference(quant_intro,[status(thm)],[16])).
% 2.47/2.70 tff(18,plain,
% 2.47/2.70 (![U: $i] : (?[V: $i] : (ssList(V) & ?[W: $i] : (ssItem(W) & (cons(W, V) = U))) | (nil = U) | (~ssList(U))) <=> ![U: $i] : (?[V: $i] : (ssList(V) & ?[W: $i] : (ssItem(W) & (cons(W, V) = U))) | (nil = U) | (~ssList(U)))),
% 2.47/2.70 inference(rewrite,[status(thm)],[])).
% 2.47/2.70 tff(19,plain,
% 2.47/2.70 (^[U: $i] : trans(monotonicity(rewrite(((nil = U) | ?[V: $i] : (ssList(V) & ?[W: $i] : (ssItem(W) & (cons(W, V) = U)))) <=> ((nil = U) | ?[V: $i] : (ssList(V) & ?[W: $i] : (ssItem(W) & (cons(W, V) = U))))), ((ssList(U) => ((nil = U) | ?[V: $i] : (ssList(V) & ?[W: $i] : (ssItem(W) & (cons(W, V) = U))))) <=> (ssList(U) => ((nil = U) | ?[V: $i] : (ssList(V) & ?[W: $i] : (ssItem(W) & (cons(W, V) = U))))))), rewrite((ssList(U) => ((nil = U) | ?[V: $i] : (ssList(V) & ?[W: $i] : (ssItem(W) & (cons(W, V) = U))))) <=> (?[V: $i] : (ssList(V) & ?[W: $i] : (ssItem(W) & (cons(W, V) = U))) | (nil = U) | (~ssList(U)))), ((ssList(U) => ((nil = U) | ?[V: $i] : (ssList(V) & ?[W: $i] : (ssItem(W) & (cons(W, V) = U))))) <=> (?[V: $i] : (ssList(V) & ?[W: $i] : (ssItem(W) & (cons(W, V) = U))) | (nil = U) | (~ssList(U)))))),
% 2.47/2.70 inference(bind,[status(th)],[])).
% 2.47/2.70 tff(20,plain,
% 2.47/2.70 (![U: $i] : (ssList(U) => ((nil = U) | ?[V: $i] : (ssList(V) & ?[W: $i] : (ssItem(W) & (cons(W, V) = U))))) <=> ![U: $i] : (?[V: $i] : (ssList(V) & ?[W: $i] : (ssItem(W) & (cons(W, V) = U))) | (nil = U) | (~ssList(U)))),
% 2.47/2.70 inference(quant_intro,[status(thm)],[19])).
% 2.47/2.70 tff(21,axiom,(![U: $i] : (ssList(U) => ((nil = U) | ?[V: $i] : (ssList(V) & ?[W: $i] : (ssItem(W) & (cons(W, V) = U)))))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax','ax20')).
% 2.47/2.70 tff(22,plain,
% 2.47/2.70 (![U: $i] : (?[V: $i] : (ssList(V) & ?[W: $i] : (ssItem(W) & (cons(W, V) = U))) | (nil = U) | (~ssList(U)))),
% 2.47/2.70 inference(modus_ponens,[status(thm)],[21, 20])).
% 2.47/2.70 tff(23,plain,
% 2.47/2.70 (![U: $i] : (?[V: $i] : (ssList(V) & ?[W: $i] : (ssItem(W) & (cons(W, V) = U))) | (nil = U) | (~ssList(U)))),
% 2.47/2.70 inference(modus_ponens,[status(thm)],[22, 18])).
% 2.47/2.70 tff(24,plain,(
% 2.47/2.70 ![U: $i] : ((ssList(tptp_fun_V_43(U)) & (ssItem(tptp_fun_W_44(U)) & (cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U))) | (nil = U) | (~ssList(U)))),
% 2.47/2.70 inference(skolemize,[status(sab)],[23])).
% 2.47/2.70 tff(25,plain,
% 2.47/2.70 (![U: $i] : ((nil = U) | (~ssList(U)) | (ssList(tptp_fun_V_43(U)) & ssItem(tptp_fun_W_44(U)) & (cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U)))),
% 2.47/2.70 inference(modus_ponens,[status(thm)],[24, 17])).
% 2.47/2.70 tff(26,plain,
% 2.47/2.70 (![U: $i] : ((nil = U) | (~ssList(U)) | (~((~ssList(tptp_fun_V_43(U))) | (~ssItem(tptp_fun_W_44(U))) | (~(cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U)))))),
% 2.47/2.70 inference(modus_ponens,[status(thm)],[25, 15])).
% 2.47/2.70 tff(27,plain,
% 2.47/2.70 (![U: $i] : ((nil = U) | (~ssList(U)) | (~((~ssList(tptp_fun_V_43(U))) | (~ssItem(tptp_fun_W_44(U))) | (~(cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U)))))),
% 2.47/2.70 inference(modus_ponens,[status(thm)],[26, 13])).
% 2.47/2.70 tff(28,plain,
% 2.47/2.70 (((~![U: $i] : ((nil = U) | (~ssList(U)) | (~((~ssList(tptp_fun_V_43(U))) | (~ssItem(tptp_fun_W_44(U))) | (~(cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U)))))) | ((~ssList(U!45)) | (nil = U!45) | (~((~ssList(tptp_fun_V_43(U!45))) | (~ssItem(tptp_fun_W_44(U!45))) | (~(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)) = U!45)))))) <=> ((~![U: $i] : ((nil = U) | (~ssList(U)) | (~((~ssList(tptp_fun_V_43(U))) | (~ssItem(tptp_fun_W_44(U))) | (~(cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U)))))) | (~ssList(U!45)) | (nil = U!45) | (~((~ssList(tptp_fun_V_43(U!45))) | (~ssItem(tptp_fun_W_44(U!45))) | (~(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)) = U!45)))))),
% 2.47/2.70 inference(rewrite,[status(thm)],[])).
% 2.47/2.70 tff(29,plain,
% 2.47/2.70 (((nil = U!45) | (~ssList(U!45)) | (~((~ssList(tptp_fun_V_43(U!45))) | (~ssItem(tptp_fun_W_44(U!45))) | (~(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)) = U!45))))) <=> ((~ssList(U!45)) | (nil = U!45) | (~((~ssList(tptp_fun_V_43(U!45))) | (~ssItem(tptp_fun_W_44(U!45))) | (~(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)) = U!45)))))),
% 2.47/2.70 inference(rewrite,[status(thm)],[])).
% 2.47/2.70 tff(30,plain,
% 2.47/2.70 ((~((~ssList(tptp_fun_V_43(U!45))) | (~ssItem(tptp_fun_W_44(U!45))) | (~(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)) = U!45)))) <=> (~((~ssList(tptp_fun_V_43(U!45))) | (~ssItem(tptp_fun_W_44(U!45))) | (~(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)) = U!45))))),
% 2.47/2.70 inference(rewrite,[status(thm)],[])).
% 2.47/2.70 tff(31,plain,
% 2.47/2.70 (((nil = U!45) | (~ssList(U!45)) | (~((~ssList(tptp_fun_V_43(U!45))) | (~ssItem(tptp_fun_W_44(U!45))) | (~(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)) = U!45))))) <=> ((nil = U!45) | (~ssList(U!45)) | (~((~ssList(tptp_fun_V_43(U!45))) | (~ssItem(tptp_fun_W_44(U!45))) | (~(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)) = U!45)))))),
% 2.47/2.70 inference(monotonicity,[status(thm)],[30])).
% 2.47/2.70 tff(32,plain,
% 2.47/2.70 (((nil = U!45) | (~ssList(U!45)) | (~((~ssList(tptp_fun_V_43(U!45))) | (~ssItem(tptp_fun_W_44(U!45))) | (~(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)) = U!45))))) <=> ((~ssList(U!45)) | (nil = U!45) | (~((~ssList(tptp_fun_V_43(U!45))) | (~ssItem(tptp_fun_W_44(U!45))) | (~(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)) = U!45)))))),
% 2.47/2.70 inference(transitivity,[status(thm)],[31, 29])).
% 2.47/2.70 tff(33,plain,
% 2.47/2.70 (((~![U: $i] : ((nil = U) | (~ssList(U)) | (~((~ssList(tptp_fun_V_43(U))) | (~ssItem(tptp_fun_W_44(U))) | (~(cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U)))))) | ((nil = U!45) | (~ssList(U!45)) | (~((~ssList(tptp_fun_V_43(U!45))) | (~ssItem(tptp_fun_W_44(U!45))) | (~(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)) = U!45)))))) <=> ((~![U: $i] : ((nil = U) | (~ssList(U)) | (~((~ssList(tptp_fun_V_43(U))) | (~ssItem(tptp_fun_W_44(U))) | (~(cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U)))))) | ((~ssList(U!45)) | (nil = U!45) | (~((~ssList(tptp_fun_V_43(U!45))) | (~ssItem(tptp_fun_W_44(U!45))) | (~(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)) = U!45))))))),
% 2.47/2.70 inference(monotonicity,[status(thm)],[32])).
% 2.47/2.70 tff(34,plain,
% 2.47/2.70 (((~![U: $i] : ((nil = U) | (~ssList(U)) | (~((~ssList(tptp_fun_V_43(U))) | (~ssItem(tptp_fun_W_44(U))) | (~(cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U)))))) | ((nil = U!45) | (~ssList(U!45)) | (~((~ssList(tptp_fun_V_43(U!45))) | (~ssItem(tptp_fun_W_44(U!45))) | (~(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)) = U!45)))))) <=> ((~![U: $i] : ((nil = U) | (~ssList(U)) | (~((~ssList(tptp_fun_V_43(U))) | (~ssItem(tptp_fun_W_44(U))) | (~(cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U)))))) | (~ssList(U!45)) | (nil = U!45) | (~((~ssList(tptp_fun_V_43(U!45))) | (~ssItem(tptp_fun_W_44(U!45))) | (~(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)) = U!45)))))),
% 2.47/2.70 inference(transitivity,[status(thm)],[33, 28])).
% 2.47/2.70 tff(35,plain,
% 2.47/2.70 ((~![U: $i] : ((nil = U) | (~ssList(U)) | (~((~ssList(tptp_fun_V_43(U))) | (~ssItem(tptp_fun_W_44(U))) | (~(cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U)))))) | ((nil = U!45) | (~ssList(U!45)) | (~((~ssList(tptp_fun_V_43(U!45))) | (~ssItem(tptp_fun_W_44(U!45))) | (~(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)) = U!45)))))),
% 2.47/2.70 inference(quant_inst,[status(thm)],[])).
% 2.47/2.70 tff(36,plain,
% 2.47/2.70 ((~![U: $i] : ((nil = U) | (~ssList(U)) | (~((~ssList(tptp_fun_V_43(U))) | (~ssItem(tptp_fun_W_44(U))) | (~(cons(tptp_fun_W_44(U), tptp_fun_V_43(U)) = U)))))) | (~ssList(U!45)) | (nil = U!45) | (~((~ssList(tptp_fun_V_43(U!45))) | (~ssItem(tptp_fun_W_44(U!45))) | (~(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)) = U!45))))),
% 2.47/2.70 inference(modus_ponens,[status(thm)],[35, 34])).
% 2.47/2.70 tff(37,plain,
% 2.47/2.70 (~((~ssList(tptp_fun_V_43(U!45))) | (~ssItem(tptp_fun_W_44(U!45))) | (~(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)) = U!45)))),
% 2.47/2.70 inference(unit_resolution,[status(thm)],[36, 27, 11, 10])).
% 2.47/2.70 tff(38,plain,
% 2.47/2.70 (((~ssList(tptp_fun_V_43(U!45))) | (~ssItem(tptp_fun_W_44(U!45))) | (~(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)) = U!45))) | (cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)) = U!45)),
% 2.47/2.70 inference(tautology,[status(thm)],[])).
% 2.47/2.70 tff(39,plain,
% 2.47/2.70 (cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)) = U!45),
% 2.47/2.70 inference(unit_resolution,[status(thm)],[38, 37])).
% 2.47/2.70 tff(40,plain,
% 2.47/2.70 (memberP(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)), hd(U!45)) <=> memberP(U!45, hd(U!45))),
% 2.47/2.70 inference(monotonicity,[status(thm)],[39])).
% 2.47/2.70 tff(41,plain,
% 2.47/2.70 (memberP(U!45, hd(U!45)) <=> memberP(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)), hd(U!45))),
% 2.47/2.70 inference(symmetry,[status(thm)],[40])).
% 2.47/2.70 tff(42,plain,
% 2.47/2.70 ((~memberP(U!45, hd(U!45))) <=> (~memberP(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)), hd(U!45)))),
% 2.47/2.70 inference(monotonicity,[status(thm)],[41])).
% 2.47/2.70 tff(43,plain,
% 2.47/2.70 (^[U: $i] : refl(((nil = U) | ssItem(hd(U)) | (~ssList(U))) <=> ((nil = U) | ssItem(hd(U)) | (~ssList(U))))),
% 2.47/2.70 inference(bind,[status(th)],[])).
% 2.47/2.70 tff(44,plain,
% 2.47/2.70 (![U: $i] : ((nil = U) | ssItem(hd(U)) | (~ssList(U))) <=> ![U: $i] : ((nil = U) | ssItem(hd(U)) | (~ssList(U)))),
% 2.47/2.70 inference(quant_intro,[status(thm)],[43])).
% 2.47/2.70 tff(45,plain,
% 2.47/2.70 (![U: $i] : ((nil = U) | ssItem(hd(U)) | (~ssList(U))) <=> ![U: $i] : ((nil = U) | ssItem(hd(U)) | (~ssList(U)))),
% 2.47/2.70 inference(rewrite,[status(thm)],[])).
% 2.47/2.70 tff(46,plain,
% 2.47/2.70 (^[U: $i] : trans(monotonicity(rewrite(((~(nil = U)) => ssItem(hd(U))) <=> ((nil = U) | ssItem(hd(U)))), ((ssList(U) => ((~(nil = U)) => ssItem(hd(U)))) <=> (ssList(U) => ((nil = U) | ssItem(hd(U)))))), rewrite((ssList(U) => ((nil = U) | ssItem(hd(U)))) <=> ((nil = U) | ssItem(hd(U)) | (~ssList(U)))), ((ssList(U) => ((~(nil = U)) => ssItem(hd(U)))) <=> ((nil = U) | ssItem(hd(U)) | (~ssList(U)))))),
% 2.47/2.70 inference(bind,[status(th)],[])).
% 2.47/2.70 tff(47,plain,
% 2.47/2.70 (![U: $i] : (ssList(U) => ((~(nil = U)) => ssItem(hd(U)))) <=> ![U: $i] : ((nil = U) | ssItem(hd(U)) | (~ssList(U)))),
% 2.47/2.70 inference(quant_intro,[status(thm)],[46])).
% 2.47/2.70 tff(48,axiom,(![U: $i] : (ssList(U) => ((~(nil = U)) => ssItem(hd(U))))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax','ax22')).
% 2.47/2.70 tff(49,plain,
% 2.47/2.70 (![U: $i] : ((nil = U) | ssItem(hd(U)) | (~ssList(U)))),
% 2.47/2.70 inference(modus_ponens,[status(thm)],[48, 47])).
% 2.47/2.70 tff(50,plain,
% 2.47/2.70 (![U: $i] : ((nil = U) | ssItem(hd(U)) | (~ssList(U)))),
% 2.47/2.70 inference(modus_ponens,[status(thm)],[49, 45])).
% 2.47/2.70 tff(51,plain,(
% 2.47/2.70 ![U: $i] : ((nil = U) | ssItem(hd(U)) | (~ssList(U)))),
% 2.47/2.70 inference(skolemize,[status(sab)],[50])).
% 2.47/2.70 tff(52,plain,
% 2.47/2.70 (![U: $i] : ((nil = U) | ssItem(hd(U)) | (~ssList(U)))),
% 2.47/2.70 inference(modus_ponens,[status(thm)],[51, 44])).
% 2.47/2.70 tff(53,plain,
% 2.47/2.70 (((~![U: $i] : ((nil = U) | ssItem(hd(U)) | (~ssList(U)))) | ((~ssList(U!45)) | (nil = U!45) | ssItem(hd(U!45)))) <=> ((~![U: $i] : ((nil = U) | ssItem(hd(U)) | (~ssList(U)))) | (~ssList(U!45)) | (nil = U!45) | ssItem(hd(U!45)))),
% 2.47/2.70 inference(rewrite,[status(thm)],[])).
% 2.47/2.70 tff(54,plain,
% 2.47/2.70 (((nil = U!45) | ssItem(hd(U!45)) | (~ssList(U!45))) <=> ((~ssList(U!45)) | (nil = U!45) | ssItem(hd(U!45)))),
% 2.47/2.70 inference(rewrite,[status(thm)],[])).
% 2.47/2.70 tff(55,plain,
% 2.47/2.70 (((~![U: $i] : ((nil = U) | ssItem(hd(U)) | (~ssList(U)))) | ((nil = U!45) | ssItem(hd(U!45)) | (~ssList(U!45)))) <=> ((~![U: $i] : ((nil = U) | ssItem(hd(U)) | (~ssList(U)))) | ((~ssList(U!45)) | (nil = U!45) | ssItem(hd(U!45))))),
% 2.47/2.70 inference(monotonicity,[status(thm)],[54])).
% 2.47/2.70 tff(56,plain,
% 2.47/2.70 (((~![U: $i] : ((nil = U) | ssItem(hd(U)) | (~ssList(U)))) | ((nil = U!45) | ssItem(hd(U!45)) | (~ssList(U!45)))) <=> ((~![U: $i] : ((nil = U) | ssItem(hd(U)) | (~ssList(U)))) | (~ssList(U!45)) | (nil = U!45) | ssItem(hd(U!45)))),
% 2.47/2.70 inference(transitivity,[status(thm)],[55, 53])).
% 2.47/2.70 tff(57,plain,
% 2.47/2.70 ((~![U: $i] : ((nil = U) | ssItem(hd(U)) | (~ssList(U)))) | ((nil = U!45) | ssItem(hd(U!45)) | (~ssList(U!45)))),
% 2.47/2.70 inference(quant_inst,[status(thm)],[])).
% 2.47/2.70 tff(58,plain,
% 2.47/2.70 ((~![U: $i] : ((nil = U) | ssItem(hd(U)) | (~ssList(U)))) | (~ssList(U!45)) | (nil = U!45) | ssItem(hd(U!45))),
% 2.47/2.70 inference(modus_ponens,[status(thm)],[57, 56])).
% 2.47/2.70 tff(59,plain,
% 2.47/2.70 (ssItem(hd(U!45))),
% 2.47/2.70 inference(unit_resolution,[status(thm)],[58, 52, 11, 10])).
% 2.47/2.70 tff(60,plain,
% 2.47/2.70 (^[Y: $i] : rewrite(((~ssItem(Y)) | (~((~((~memberP(U!45, Y)) | (~((~memberP(nil, Y)) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))))))) | (~((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil))))))))))) <=> ((~ssItem(Y)) | (~((~((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil)))))))) | (~((~memberP(U!45, Y)) | (~((~memberP(nil, Y)) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil))))))))))))))),
% 2.47/2.70 inference(bind,[status(th)],[])).
% 2.47/2.70 tff(61,plain,
% 2.47/2.70 (![Y: $i] : ((~ssItem(Y)) | (~((~((~memberP(U!45, Y)) | (~((~memberP(nil, Y)) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))))))) | (~((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil))))))))))) <=> ![Y: $i] : ((~ssItem(Y)) | (~((~((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil)))))))) | (~((~memberP(U!45, Y)) | (~((~memberP(nil, Y)) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))))))))))),
% 2.47/2.70 inference(quant_intro,[status(thm)],[60])).
% 2.47/2.70 tff(62,plain,
% 2.47/2.70 (^[Y: $i] : refl(((~ssItem(Y)) | (~((~((~memberP(U!45, Y)) | (~((~memberP(nil, Y)) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))))))) | (~((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil))))))))))) <=> ((~ssItem(Y)) | (~((~((~memberP(U!45, Y)) | (~((~memberP(nil, Y)) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))))))) | (~((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil))))))))))))),
% 2.47/2.70 inference(bind,[status(th)],[])).
% 2.47/2.70 tff(63,plain,
% 2.47/2.70 (![Y: $i] : ((~ssItem(Y)) | (~((~((~memberP(U!45, Y)) | (~((~memberP(nil, Y)) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))))))) | (~((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil))))))))))) <=> ![Y: $i] : ((~ssItem(Y)) | (~((~((~memberP(U!45, Y)) | (~((~memberP(nil, Y)) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))))))) | (~((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil)))))))))))),
% 2.47/2.70 inference(quant_intro,[status(thm)],[62])).
% 2.47/2.70 tff(64,plain,
% 2.47/2.70 (^[Y: $i] : rewrite(((~ssItem(Y)) | (~((~((~memberP(U!45, Y)) | (~((~memberP(nil, Y)) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))))))) | (~((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil))))))))))) <=> ((~ssItem(Y)) | (~((~((~memberP(U!45, Y)) | (~((~memberP(nil, Y)) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))))))) | (~((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil))))))))))))),
% 2.47/2.71 inference(bind,[status(th)],[])).
% 2.47/2.71 tff(65,plain,
% 2.47/2.71 (![Y: $i] : ((~ssItem(Y)) | (~((~((~memberP(U!45, Y)) | (~((~memberP(nil, Y)) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))))))) | (~((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil))))))))))) <=> ![Y: $i] : ((~ssItem(Y)) | (~((~((~memberP(U!45, Y)) | (~((~memberP(nil, Y)) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))))))) | (~((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil)))))))))))),
% 2.47/2.71 inference(quant_intro,[status(thm)],[64])).
% 2.47/2.71 tff(66,plain,
% 2.47/2.71 (![Y: $i] : ((~ssItem(Y)) | (~((~((~memberP(U!45, Y)) | (~((~memberP(nil, Y)) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))))))) | (~((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil))))))))))) <=> ![Y: $i] : ((~ssItem(Y)) | (~((~((~memberP(U!45, Y)) | (~((~memberP(nil, Y)) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))))))) | (~((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil)))))))))))),
% 2.47/2.71 inference(transitivity,[status(thm)],[65, 63])).
% 2.47/2.71 tff(67,plain,
% 2.47/2.71 (^[Y: $i] : rewrite(((~ssItem(Y)) | (((~memberP(U!45, Y)) | (memberP(nil, Y) & ![Z: $i] : (~(ssList(Z) & segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil))))))) & ((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil))))))))) <=> ((~ssItem(Y)) | (~((~((~memberP(U!45, Y)) | (~((~memberP(nil, Y)) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))))))) | (~((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil))))))))))))),
% 2.47/2.71 inference(bind,[status(th)],[])).
% 2.47/2.71 tff(68,plain,
% 2.47/2.71 (![Y: $i] : ((~ssItem(Y)) | (((~memberP(U!45, Y)) | (memberP(nil, Y) & ![Z: $i] : (~(ssList(Z) & segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil))))))) & ((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil))))))))) <=> ![Y: $i] : ((~ssItem(Y)) | (~((~((~memberP(U!45, Y)) | (~((~memberP(nil, Y)) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))))))) | (~((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil)))))))))))),
% 2.47/2.71 inference(quant_intro,[status(thm)],[67])).
% 2.47/2.71 tff(69,plain,
% 2.47/2.71 (![Y: $i] : ((~ssItem(Y)) | (((~memberP(U!45, Y)) | (memberP(nil, Y) & ![Z: $i] : (~(ssList(Z) & segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil))))))) & ((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil)))))))))),
% 2.47/2.71 inference(and_elim,[status(thm)],[9])).
% 2.47/2.71 tff(70,plain,
% 2.47/2.71 (![Y: $i] : ((~ssItem(Y)) | (~((~((~memberP(U!45, Y)) | (~((~memberP(nil, Y)) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))))))) | (~((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil)))))))))))),
% 2.47/2.71 inference(modus_ponens,[status(thm)],[69, 68])).
% 2.47/2.71 tff(71,plain,
% 2.47/2.71 (![Y: $i] : ((~ssItem(Y)) | (~((~((~memberP(U!45, Y)) | (~((~memberP(nil, Y)) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))))))) | (~((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil)))))))))))),
% 2.47/2.71 inference(modus_ponens,[status(thm)],[70, 66])).
% 2.47/2.71 tff(72,plain,
% 2.47/2.71 (![Y: $i] : ((~ssItem(Y)) | (~((~((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil)))))))) | (~((~memberP(U!45, Y)) | (~((~memberP(nil, Y)) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))))))))))),
% 2.47/2.71 inference(modus_ponens,[status(thm)],[71, 61])).
% 2.47/2.71 tff(73,plain,
% 2.47/2.71 (((~![Y: $i] : ((~ssItem(Y)) | (~((~((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil)))))))) | (~((~memberP(U!45, Y)) | (~((~memberP(nil, Y)) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))))))))))) | ((~ssItem(hd(U!45))) | (~((~(memberP(U!45, hd(U!45)) | (~memberP(nil, hd(U!45))) | (~((~ssList(tptp_fun_Z_46(hd(U!45)))) | (~segmentP(nil, app(app(cons(hd(U!45), nil), tptp_fun_Z_46(hd(U!45))), cons(hd(U!45), nil)))))))) | (~((~memberP(U!45, hd(U!45))) | (~((~memberP(nil, hd(U!45))) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(hd(U!45), nil), Z), cons(hd(U!45), nil)))))))))))))) <=> ((~![Y: $i] : ((~ssItem(Y)) | (~((~((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil)))))))) | (~((~memberP(U!45, Y)) | (~((~memberP(nil, Y)) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))))))))))) | (~ssItem(hd(U!45))) | (~((~(memberP(U!45, hd(U!45)) | (~memberP(nil, hd(U!45))) | (~((~ssList(tptp_fun_Z_46(hd(U!45)))) | (~segmentP(nil, app(app(cons(hd(U!45), nil), tptp_fun_Z_46(hd(U!45))), cons(hd(U!45), nil)))))))) | (~((~memberP(U!45, hd(U!45))) | (~((~memberP(nil, hd(U!45))) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(hd(U!45), nil), Z), cons(hd(U!45), nil)))))))))))))),
% 2.47/2.71 inference(rewrite,[status(thm)],[])).
% 2.47/2.71 tff(74,plain,
% 2.47/2.71 (((~ssItem(hd(U!45))) | (~((~((~memberP(nil, hd(U!45))) | memberP(U!45, hd(U!45)) | (~((~ssList(tptp_fun_Z_46(hd(U!45)))) | (~segmentP(nil, app(app(cons(hd(U!45), nil), tptp_fun_Z_46(hd(U!45))), cons(hd(U!45), nil)))))))) | (~((~memberP(U!45, hd(U!45))) | (~((~memberP(nil, hd(U!45))) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(hd(U!45), nil), Z), cons(hd(U!45), nil))))))))))))) <=> ((~ssItem(hd(U!45))) | (~((~(memberP(U!45, hd(U!45)) | (~memberP(nil, hd(U!45))) | (~((~ssList(tptp_fun_Z_46(hd(U!45)))) | (~segmentP(nil, app(app(cons(hd(U!45), nil), tptp_fun_Z_46(hd(U!45))), cons(hd(U!45), nil)))))))) | (~((~memberP(U!45, hd(U!45))) | (~((~memberP(nil, hd(U!45))) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(hd(U!45), nil), Z), cons(hd(U!45), nil)))))))))))))),
% 2.47/2.71 inference(rewrite,[status(thm)],[])).
% 2.47/2.71 tff(75,plain,
% 2.47/2.71 (((~![Y: $i] : ((~ssItem(Y)) | (~((~((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil)))))))) | (~((~memberP(U!45, Y)) | (~((~memberP(nil, Y)) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))))))))))) | ((~ssItem(hd(U!45))) | (~((~((~memberP(nil, hd(U!45))) | memberP(U!45, hd(U!45)) | (~((~ssList(tptp_fun_Z_46(hd(U!45)))) | (~segmentP(nil, app(app(cons(hd(U!45), nil), tptp_fun_Z_46(hd(U!45))), cons(hd(U!45), nil)))))))) | (~((~memberP(U!45, hd(U!45))) | (~((~memberP(nil, hd(U!45))) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(hd(U!45), nil), Z), cons(hd(U!45), nil)))))))))))))) <=> ((~![Y: $i] : ((~ssItem(Y)) | (~((~((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil)))))))) | (~((~memberP(U!45, Y)) | (~((~memberP(nil, Y)) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))))))))))) | ((~ssItem(hd(U!45))) | (~((~(memberP(U!45, hd(U!45)) | (~memberP(nil, hd(U!45))) | (~((~ssList(tptp_fun_Z_46(hd(U!45)))) | (~segmentP(nil, app(app(cons(hd(U!45), nil), tptp_fun_Z_46(hd(U!45))), cons(hd(U!45), nil)))))))) | (~((~memberP(U!45, hd(U!45))) | (~((~memberP(nil, hd(U!45))) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(hd(U!45), nil), Z), cons(hd(U!45), nil))))))))))))))),
% 2.47/2.71 inference(monotonicity,[status(thm)],[74])).
% 2.47/2.71 tff(76,plain,
% 2.47/2.71 (((~![Y: $i] : ((~ssItem(Y)) | (~((~((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil)))))))) | (~((~memberP(U!45, Y)) | (~((~memberP(nil, Y)) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))))))))))) | ((~ssItem(hd(U!45))) | (~((~((~memberP(nil, hd(U!45))) | memberP(U!45, hd(U!45)) | (~((~ssList(tptp_fun_Z_46(hd(U!45)))) | (~segmentP(nil, app(app(cons(hd(U!45), nil), tptp_fun_Z_46(hd(U!45))), cons(hd(U!45), nil)))))))) | (~((~memberP(U!45, hd(U!45))) | (~((~memberP(nil, hd(U!45))) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(hd(U!45), nil), Z), cons(hd(U!45), nil)))))))))))))) <=> ((~![Y: $i] : ((~ssItem(Y)) | (~((~((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil)))))))) | (~((~memberP(U!45, Y)) | (~((~memberP(nil, Y)) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))))))))))) | (~ssItem(hd(U!45))) | (~((~(memberP(U!45, hd(U!45)) | (~memberP(nil, hd(U!45))) | (~((~ssList(tptp_fun_Z_46(hd(U!45)))) | (~segmentP(nil, app(app(cons(hd(U!45), nil), tptp_fun_Z_46(hd(U!45))), cons(hd(U!45), nil)))))))) | (~((~memberP(U!45, hd(U!45))) | (~((~memberP(nil, hd(U!45))) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(hd(U!45), nil), Z), cons(hd(U!45), nil)))))))))))))),
% 2.47/2.71 inference(transitivity,[status(thm)],[75, 73])).
% 2.47/2.71 tff(77,plain,
% 2.47/2.71 ((~![Y: $i] : ((~ssItem(Y)) | (~((~((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil)))))))) | (~((~memberP(U!45, Y)) | (~((~memberP(nil, Y)) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))))))))))) | ((~ssItem(hd(U!45))) | (~((~((~memberP(nil, hd(U!45))) | memberP(U!45, hd(U!45)) | (~((~ssList(tptp_fun_Z_46(hd(U!45)))) | (~segmentP(nil, app(app(cons(hd(U!45), nil), tptp_fun_Z_46(hd(U!45))), cons(hd(U!45), nil)))))))) | (~((~memberP(U!45, hd(U!45))) | (~((~memberP(nil, hd(U!45))) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(hd(U!45), nil), Z), cons(hd(U!45), nil)))))))))))))),
% 2.47/2.71 inference(quant_inst,[status(thm)],[])).
% 2.47/2.71 tff(78,plain,
% 2.47/2.71 ((~![Y: $i] : ((~ssItem(Y)) | (~((~((~memberP(nil, Y)) | memberP(U!45, Y) | (~((~ssList(tptp_fun_Z_46(Y))) | (~segmentP(nil, app(app(cons(Y, nil), tptp_fun_Z_46(Y)), cons(Y, nil)))))))) | (~((~memberP(U!45, Y)) | (~((~memberP(nil, Y)) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(Y, nil), Z), cons(Y, nil)))))))))))))) | (~ssItem(hd(U!45))) | (~((~(memberP(U!45, hd(U!45)) | (~memberP(nil, hd(U!45))) | (~((~ssList(tptp_fun_Z_46(hd(U!45)))) | (~segmentP(nil, app(app(cons(hd(U!45), nil), tptp_fun_Z_46(hd(U!45))), cons(hd(U!45), nil)))))))) | (~((~memberP(U!45, hd(U!45))) | (~((~memberP(nil, hd(U!45))) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(hd(U!45), nil), Z), cons(hd(U!45), nil))))))))))))),
% 2.47/2.71 inference(modus_ponens,[status(thm)],[77, 76])).
% 2.47/2.71 tff(79,plain,
% 2.47/2.71 (~((~(memberP(U!45, hd(U!45)) | (~memberP(nil, hd(U!45))) | (~((~ssList(tptp_fun_Z_46(hd(U!45)))) | (~segmentP(nil, app(app(cons(hd(U!45), nil), tptp_fun_Z_46(hd(U!45))), cons(hd(U!45), nil)))))))) | (~((~memberP(U!45, hd(U!45))) | (~((~memberP(nil, hd(U!45))) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(hd(U!45), nil), Z), cons(hd(U!45), nil)))))))))))),
% 2.47/2.71 inference(unit_resolution,[status(thm)],[78, 72, 59])).
% 2.47/2.71 tff(80,plain,
% 2.47/2.71 (((~(memberP(U!45, hd(U!45)) | (~memberP(nil, hd(U!45))) | (~((~ssList(tptp_fun_Z_46(hd(U!45)))) | (~segmentP(nil, app(app(cons(hd(U!45), nil), tptp_fun_Z_46(hd(U!45))), cons(hd(U!45), nil)))))))) | (~((~memberP(U!45, hd(U!45))) | (~((~memberP(nil, hd(U!45))) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(hd(U!45), nil), Z), cons(hd(U!45), nil))))))))))) | ((~memberP(U!45, hd(U!45))) | (~((~memberP(nil, hd(U!45))) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(hd(U!45), nil), Z), cons(hd(U!45), nil)))))))))),
% 2.47/2.71 inference(tautology,[status(thm)],[])).
% 2.47/2.71 tff(81,plain,
% 2.47/2.71 ((~memberP(U!45, hd(U!45))) | (~((~memberP(nil, hd(U!45))) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(hd(U!45), nil), Z), cons(hd(U!45), nil))))))))),
% 2.47/2.71 inference(unit_resolution,[status(thm)],[80, 79])).
% 2.47/2.71 tff(82,plain,
% 2.47/2.71 (^[U: $i] : refl(((~ssItem(U)) | (~memberP(nil, U))) <=> ((~ssItem(U)) | (~memberP(nil, U))))),
% 2.47/2.71 inference(bind,[status(th)],[])).
% 2.47/2.71 tff(83,plain,
% 2.47/2.71 (![U: $i] : ((~ssItem(U)) | (~memberP(nil, U))) <=> ![U: $i] : ((~ssItem(U)) | (~memberP(nil, U)))),
% 2.47/2.71 inference(quant_intro,[status(thm)],[82])).
% 2.47/2.71 tff(84,plain,
% 2.47/2.71 (![U: $i] : ((~ssItem(U)) | (~memberP(nil, U))) <=> ![U: $i] : ((~ssItem(U)) | (~memberP(nil, U)))),
% 2.47/2.71 inference(rewrite,[status(thm)],[])).
% 2.47/2.71 tff(85,plain,
% 2.47/2.71 (^[U: $i] : rewrite((ssItem(U) => (~memberP(nil, U))) <=> ((~ssItem(U)) | (~memberP(nil, U))))),
% 2.47/2.71 inference(bind,[status(th)],[])).
% 2.47/2.71 tff(86,plain,
% 2.47/2.71 (![U: $i] : (ssItem(U) => (~memberP(nil, U))) <=> ![U: $i] : ((~ssItem(U)) | (~memberP(nil, U)))),
% 2.47/2.71 inference(quant_intro,[status(thm)],[85])).
% 2.47/2.71 tff(87,axiom,(![U: $i] : (ssItem(U) => (~memberP(nil, U)))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax','ax38')).
% 2.47/2.71 tff(88,plain,
% 2.47/2.71 (![U: $i] : ((~ssItem(U)) | (~memberP(nil, U)))),
% 2.47/2.71 inference(modus_ponens,[status(thm)],[87, 86])).
% 2.47/2.71 tff(89,plain,
% 2.47/2.71 (![U: $i] : ((~ssItem(U)) | (~memberP(nil, U)))),
% 2.47/2.71 inference(modus_ponens,[status(thm)],[88, 84])).
% 2.47/2.71 tff(90,plain,(
% 2.47/2.71 ![U: $i] : ((~ssItem(U)) | (~memberP(nil, U)))),
% 2.47/2.71 inference(skolemize,[status(sab)],[89])).
% 2.47/2.71 tff(91,plain,
% 2.47/2.71 (![U: $i] : ((~ssItem(U)) | (~memberP(nil, U)))),
% 2.47/2.71 inference(modus_ponens,[status(thm)],[90, 83])).
% 2.47/2.71 tff(92,plain,
% 2.47/2.71 (((~![U: $i] : ((~ssItem(U)) | (~memberP(nil, U)))) | ((~ssItem(hd(U!45))) | (~memberP(nil, hd(U!45))))) <=> ((~![U: $i] : ((~ssItem(U)) | (~memberP(nil, U)))) | (~ssItem(hd(U!45))) | (~memberP(nil, hd(U!45))))),
% 2.47/2.71 inference(rewrite,[status(thm)],[])).
% 2.47/2.71 tff(93,plain,
% 2.47/2.71 ((~![U: $i] : ((~ssItem(U)) | (~memberP(nil, U)))) | ((~ssItem(hd(U!45))) | (~memberP(nil, hd(U!45))))),
% 2.47/2.71 inference(quant_inst,[status(thm)],[])).
% 2.47/2.71 tff(94,plain,
% 2.47/2.71 ((~![U: $i] : ((~ssItem(U)) | (~memberP(nil, U)))) | (~ssItem(hd(U!45))) | (~memberP(nil, hd(U!45)))),
% 2.47/2.71 inference(modus_ponens,[status(thm)],[93, 92])).
% 2.47/2.71 tff(95,plain,
% 2.47/2.71 (~memberP(nil, hd(U!45))),
% 2.47/2.71 inference(unit_resolution,[status(thm)],[94, 91, 59])).
% 2.47/2.71 tff(96,plain,
% 2.47/2.71 (((~memberP(nil, hd(U!45))) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(hd(U!45), nil), Z), cons(hd(U!45), nil))))))) | memberP(nil, hd(U!45))),
% 2.47/2.71 inference(tautology,[status(thm)],[])).
% 2.47/2.71 tff(97,plain,
% 2.47/2.71 ((~memberP(nil, hd(U!45))) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(hd(U!45), nil), Z), cons(hd(U!45), nil))))))),
% 2.47/2.71 inference(unit_resolution,[status(thm)],[96, 95])).
% 2.47/2.71 tff(98,plain,
% 2.47/2.71 ((~((~memberP(U!45, hd(U!45))) | (~((~memberP(nil, hd(U!45))) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(hd(U!45), nil), Z), cons(hd(U!45), nil)))))))))) | (~memberP(U!45, hd(U!45))) | (~((~memberP(nil, hd(U!45))) | (~![Z: $i] : ((~ssList(Z)) | (~segmentP(nil, app(app(cons(hd(U!45), nil), Z), cons(hd(U!45), nil))))))))),
% 2.47/2.71 inference(tautology,[status(thm)],[])).
% 2.47/2.71 tff(99,plain,
% 2.47/2.71 (~memberP(U!45, hd(U!45))),
% 2.47/2.71 inference(unit_resolution,[status(thm)],[98, 97, 81])).
% 2.47/2.71 tff(100,plain,
% 2.47/2.71 (~memberP(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)), hd(U!45))),
% 2.47/2.71 inference(modus_ponens,[status(thm)],[99, 42])).
% 2.47/2.71 tff(101,plain,
% 2.47/2.71 (^[U: $i] : refl(((~ssItem(U)) | ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U)))))) <=> ((~ssItem(U)) | ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U)))))))),
% 2.47/2.71 inference(bind,[status(th)],[])).
% 2.47/2.71 tff(102,plain,
% 2.47/2.71 (![U: $i] : ((~ssItem(U)) | ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U)))))) <=> ![U: $i] : ((~ssItem(U)) | ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U))))))),
% 2.47/2.71 inference(quant_intro,[status(thm)],[101])).
% 2.47/2.71 tff(103,plain,
% 2.47/2.71 (^[U: $i] : rewrite(((~ssItem(U)) | ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U)))))) <=> ((~ssItem(U)) | ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U)))))))),
% 2.47/2.71 inference(bind,[status(th)],[])).
% 2.47/2.71 tff(104,plain,
% 2.47/2.71 (![U: $i] : ((~ssItem(U)) | ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U)))))) <=> ![U: $i] : ((~ssItem(U)) | ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U))))))),
% 2.47/2.71 inference(quant_intro,[status(thm)],[103])).
% 2.47/2.71 tff(105,plain,
% 2.47/2.71 (![U: $i] : ((~ssItem(U)) | ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U)))))) <=> ![U: $i] : ((~ssItem(U)) | ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U))))))),
% 2.47/2.71 inference(transitivity,[status(thm)],[104, 102])).
% 2.47/2.71 tff(106,plain,
% 2.47/2.71 (![U: $i] : ((~ssItem(U)) | ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U)))))) <=> ![U: $i] : ((~ssItem(U)) | ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U))))))),
% 2.47/2.71 inference(rewrite,[status(thm)],[])).
% 2.47/2.71 tff(107,plain,
% 2.47/2.71 (^[U: $i] : trans(monotonicity(quant_intro(proof_bind(^[V: $i] : trans(monotonicity(quant_intro(proof_bind(^[W: $i] : rewrite((ssList(W) => (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U)))) <=> ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U)))))), (![W: $i] : (ssList(W) => (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U)))) <=> ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U)))))), ((ssItem(V) => ![W: $i] : (ssList(W) => (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U))))) <=> (ssItem(V) => ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U))))))), rewrite((ssItem(V) => ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U))))) <=> ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U)))))), ((ssItem(V) => ![W: $i] : (ssList(W) => (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U))))) <=> ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U)))))))), (![V: $i] : (ssItem(V) => ![W: $i] : (ssList(W) => (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U))))) <=> ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U))))))), ((ssItem(U) => ![V: $i] : (ssItem(V) => ![W: $i] : (ssList(W) => (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U)))))) <=> (ssItem(U) => ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U)))))))), rewrite((ssItem(U) => ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U)))))) <=> ((~ssItem(U)) | ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U))))))), ((ssItem(U) => ![V: $i] : (ssItem(V) => ![W: $i] : (ssList(W) => (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U)))))) <=> ((~ssItem(U)) | ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U))))))))),
% 2.47/2.71 inference(bind,[status(th)],[])).
% 2.47/2.71 tff(108,plain,
% 2.47/2.71 (![U: $i] : (ssItem(U) => ![V: $i] : (ssItem(V) => ![W: $i] : (ssList(W) => (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U)))))) <=> ![U: $i] : ((~ssItem(U)) | ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U))))))),
% 2.47/2.71 inference(quant_intro,[status(thm)],[107])).
% 2.47/2.71 tff(109,axiom,(![U: $i] : (ssItem(U) => ![V: $i] : (ssItem(V) => ![W: $i] : (ssList(W) => (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U))))))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax','ax37')).
% 2.47/2.71 tff(110,plain,
% 2.47/2.71 (![U: $i] : ((~ssItem(U)) | ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U))))))),
% 2.47/2.71 inference(modus_ponens,[status(thm)],[109, 108])).
% 2.47/2.71 tff(111,plain,
% 2.47/2.71 (![U: $i] : ((~ssItem(U)) | ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U))))))),
% 2.47/2.71 inference(modus_ponens,[status(thm)],[110, 106])).
% 2.47/2.71 tff(112,plain,(
% 2.47/2.71 ![U: $i] : ((~ssItem(U)) | ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U))))))),
% 2.47/2.71 inference(skolemize,[status(sab)],[111])).
% 2.47/2.71 tff(113,plain,
% 2.47/2.71 (![U: $i] : ((~ssItem(U)) | ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U))))))),
% 2.47/2.71 inference(modus_ponens,[status(thm)],[112, 105])).
% 2.47/2.71 tff(114,plain,
% 2.47/2.71 (((~![U: $i] : ((~ssItem(U)) | ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U))))))) | ((~ssItem(hd(U!45))) | ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), hd(U!45)) <=> ((hd(U!45) = V) | memberP(W, hd(U!45)))))))) <=> ((~![U: $i] : ((~ssItem(U)) | ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U))))))) | (~ssItem(hd(U!45))) | ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), hd(U!45)) <=> ((hd(U!45) = V) | memberP(W, hd(U!45)))))))),
% 2.47/2.71 inference(rewrite,[status(thm)],[])).
% 2.47/2.71 tff(115,plain,
% 2.47/2.71 ((~![U: $i] : ((~ssItem(U)) | ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U))))))) | ((~ssItem(hd(U!45))) | ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), hd(U!45)) <=> ((hd(U!45) = V) | memberP(W, hd(U!45)))))))),
% 2.47/2.71 inference(quant_inst,[status(thm)],[])).
% 2.47/2.71 tff(116,plain,
% 2.47/2.71 ((~![U: $i] : ((~ssItem(U)) | ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), U) <=> ((U = V) | memberP(W, U))))))) | (~ssItem(hd(U!45))) | ![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), hd(U!45)) <=> ((hd(U!45) = V) | memberP(W, hd(U!45))))))),
% 2.47/2.71 inference(modus_ponens,[status(thm)],[115, 114])).
% 2.47/2.71 tff(117,plain,
% 2.47/2.71 (![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), hd(U!45)) <=> ((hd(U!45) = V) | memberP(W, hd(U!45))))))),
% 2.47/2.71 inference(unit_resolution,[status(thm)],[116, 113, 59])).
% 2.47/2.71 tff(118,plain,
% 2.47/2.71 (((~ssList(tptp_fun_V_43(U!45))) | (~ssItem(tptp_fun_W_44(U!45))) | (~(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)) = U!45))) | ssItem(tptp_fun_W_44(U!45))),
% 2.47/2.71 inference(tautology,[status(thm)],[])).
% 2.47/2.71 tff(119,plain,
% 2.47/2.71 (ssItem(tptp_fun_W_44(U!45))),
% 2.47/2.71 inference(unit_resolution,[status(thm)],[118, 37])).
% 2.47/2.71 tff(120,plain,
% 2.47/2.71 (((~![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), hd(U!45)) <=> ((hd(U!45) = V) | memberP(W, hd(U!45))))))) | ((~ssItem(tptp_fun_W_44(U!45))) | ![W: $i] : ((~ssList(W)) | (memberP(cons(tptp_fun_W_44(U!45), W), hd(U!45)) <=> ((hd(U!45) = tptp_fun_W_44(U!45)) | memberP(W, hd(U!45))))))) <=> ((~![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), hd(U!45)) <=> ((hd(U!45) = V) | memberP(W, hd(U!45))))))) | (~ssItem(tptp_fun_W_44(U!45))) | ![W: $i] : ((~ssList(W)) | (memberP(cons(tptp_fun_W_44(U!45), W), hd(U!45)) <=> ((hd(U!45) = tptp_fun_W_44(U!45)) | memberP(W, hd(U!45))))))),
% 2.47/2.71 inference(rewrite,[status(thm)],[])).
% 2.47/2.71 tff(121,plain,
% 2.47/2.71 ((~![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), hd(U!45)) <=> ((hd(U!45) = V) | memberP(W, hd(U!45))))))) | ((~ssItem(tptp_fun_W_44(U!45))) | ![W: $i] : ((~ssList(W)) | (memberP(cons(tptp_fun_W_44(U!45), W), hd(U!45)) <=> ((hd(U!45) = tptp_fun_W_44(U!45)) | memberP(W, hd(U!45))))))),
% 2.47/2.71 inference(quant_inst,[status(thm)],[])).
% 2.47/2.71 tff(122,plain,
% 2.47/2.71 ((~![V: $i] : ((~ssItem(V)) | ![W: $i] : ((~ssList(W)) | (memberP(cons(V, W), hd(U!45)) <=> ((hd(U!45) = V) | memberP(W, hd(U!45))))))) | (~ssItem(tptp_fun_W_44(U!45))) | ![W: $i] : ((~ssList(W)) | (memberP(cons(tptp_fun_W_44(U!45), W), hd(U!45)) <=> ((hd(U!45) = tptp_fun_W_44(U!45)) | memberP(W, hd(U!45)))))),
% 2.47/2.71 inference(modus_ponens,[status(thm)],[121, 120])).
% 2.47/2.71 tff(123,plain,
% 2.47/2.71 (![W: $i] : ((~ssList(W)) | (memberP(cons(tptp_fun_W_44(U!45), W), hd(U!45)) <=> ((hd(U!45) = tptp_fun_W_44(U!45)) | memberP(W, hd(U!45)))))),
% 2.47/2.71 inference(unit_resolution,[status(thm)],[122, 119, 117])).
% 2.47/2.71 tff(124,plain,
% 2.47/2.71 (((~ssList(tptp_fun_V_43(U!45))) | (~ssItem(tptp_fun_W_44(U!45))) | (~(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)) = U!45))) | ssList(tptp_fun_V_43(U!45))),
% 2.47/2.71 inference(tautology,[status(thm)],[])).
% 2.47/2.71 tff(125,plain,
% 2.47/2.71 (ssList(tptp_fun_V_43(U!45))),
% 2.47/2.71 inference(unit_resolution,[status(thm)],[124, 37])).
% 2.47/2.71 tff(126,plain,
% 2.47/2.71 (((~![W: $i] : ((~ssList(W)) | (memberP(cons(tptp_fun_W_44(U!45), W), hd(U!45)) <=> ((hd(U!45) = tptp_fun_W_44(U!45)) | memberP(W, hd(U!45)))))) | ((~ssList(tptp_fun_V_43(U!45))) | (memberP(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)), hd(U!45)) <=> ((hd(U!45) = tptp_fun_W_44(U!45)) | memberP(tptp_fun_V_43(U!45), hd(U!45)))))) <=> ((~![W: $i] : ((~ssList(W)) | (memberP(cons(tptp_fun_W_44(U!45), W), hd(U!45)) <=> ((hd(U!45) = tptp_fun_W_44(U!45)) | memberP(W, hd(U!45)))))) | (~ssList(tptp_fun_V_43(U!45))) | (memberP(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)), hd(U!45)) <=> ((hd(U!45) = tptp_fun_W_44(U!45)) | memberP(tptp_fun_V_43(U!45), hd(U!45)))))),
% 2.47/2.71 inference(rewrite,[status(thm)],[])).
% 2.47/2.71 tff(127,plain,
% 2.47/2.71 ((~![W: $i] : ((~ssList(W)) | (memberP(cons(tptp_fun_W_44(U!45), W), hd(U!45)) <=> ((hd(U!45) = tptp_fun_W_44(U!45)) | memberP(W, hd(U!45)))))) | ((~ssList(tptp_fun_V_43(U!45))) | (memberP(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)), hd(U!45)) <=> ((hd(U!45) = tptp_fun_W_44(U!45)) | memberP(tptp_fun_V_43(U!45), hd(U!45)))))),
% 2.47/2.71 inference(quant_inst,[status(thm)],[])).
% 2.47/2.71 tff(128,plain,
% 2.47/2.71 ((~![W: $i] : ((~ssList(W)) | (memberP(cons(tptp_fun_W_44(U!45), W), hd(U!45)) <=> ((hd(U!45) = tptp_fun_W_44(U!45)) | memberP(W, hd(U!45)))))) | (~ssList(tptp_fun_V_43(U!45))) | (memberP(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)), hd(U!45)) <=> ((hd(U!45) = tptp_fun_W_44(U!45)) | memberP(tptp_fun_V_43(U!45), hd(U!45))))),
% 2.47/2.71 inference(modus_ponens,[status(thm)],[127, 126])).
% 2.47/2.71 tff(129,plain,
% 2.47/2.71 (memberP(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)), hd(U!45)) <=> ((hd(U!45) = tptp_fun_W_44(U!45)) | memberP(tptp_fun_V_43(U!45), hd(U!45)))),
% 2.47/2.71 inference(unit_resolution,[status(thm)],[128, 125, 123])).
% 2.47/2.71 tff(130,plain,
% 2.47/2.71 ((hd(U!45) = tptp_fun_W_44(U!45)) <=> (tptp_fun_W_44(U!45) = hd(U!45))),
% 2.47/2.71 inference(commutativity,[status(thm)],[])).
% 2.47/2.71 tff(131,plain,
% 2.47/2.71 ((tptp_fun_W_44(U!45) = hd(U!45)) <=> (hd(U!45) = tptp_fun_W_44(U!45))),
% 2.47/2.71 inference(symmetry,[status(thm)],[130])).
% 2.47/2.71 tff(132,plain,
% 2.47/2.71 (hd(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45))) = hd(U!45)),
% 2.47/2.71 inference(monotonicity,[status(thm)],[39])).
% 2.47/2.71 tff(133,plain,
% 2.47/2.71 (^[U: $i] : refl(((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (hd(cons(V, U)) = V))) <=> ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (hd(cons(V, U)) = V))))),
% 2.47/2.71 inference(bind,[status(th)],[])).
% 2.47/2.71 tff(134,plain,
% 2.47/2.71 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (hd(cons(V, U)) = V))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (hd(cons(V, U)) = V)))),
% 2.47/2.71 inference(quant_intro,[status(thm)],[133])).
% 2.47/2.72 tff(135,plain,
% 2.47/2.72 (^[U: $i] : rewrite(((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (hd(cons(V, U)) = V))) <=> ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (hd(cons(V, U)) = V))))),
% 2.47/2.72 inference(bind,[status(th)],[])).
% 2.47/2.72 tff(136,plain,
% 2.47/2.72 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (hd(cons(V, U)) = V))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (hd(cons(V, U)) = V)))),
% 2.47/2.72 inference(quant_intro,[status(thm)],[135])).
% 2.47/2.72 tff(137,plain,
% 2.47/2.72 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (hd(cons(V, U)) = V))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (hd(cons(V, U)) = V)))),
% 2.47/2.72 inference(transitivity,[status(thm)],[136, 134])).
% 2.47/2.72 tff(138,plain,
% 2.47/2.72 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (hd(cons(V, U)) = V))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (hd(cons(V, U)) = V)))),
% 2.47/2.72 inference(rewrite,[status(thm)],[])).
% 2.47/2.72 tff(139,plain,
% 2.47/2.72 (^[U: $i] : trans(monotonicity(quant_intro(proof_bind(^[V: $i] : rewrite((ssItem(V) => (hd(cons(V, U)) = V)) <=> ((~ssItem(V)) | (hd(cons(V, U)) = V)))), (![V: $i] : (ssItem(V) => (hd(cons(V, U)) = V)) <=> ![V: $i] : ((~ssItem(V)) | (hd(cons(V, U)) = V)))), ((ssList(U) => ![V: $i] : (ssItem(V) => (hd(cons(V, U)) = V))) <=> (ssList(U) => ![V: $i] : ((~ssItem(V)) | (hd(cons(V, U)) = V))))), rewrite((ssList(U) => ![V: $i] : ((~ssItem(V)) | (hd(cons(V, U)) = V))) <=> ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (hd(cons(V, U)) = V)))), ((ssList(U) => ![V: $i] : (ssItem(V) => (hd(cons(V, U)) = V))) <=> ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (hd(cons(V, U)) = V)))))),
% 2.47/2.72 inference(bind,[status(th)],[])).
% 2.47/2.72 tff(140,plain,
% 2.47/2.72 (![U: $i] : (ssList(U) => ![V: $i] : (ssItem(V) => (hd(cons(V, U)) = V))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (hd(cons(V, U)) = V)))),
% 2.47/2.72 inference(quant_intro,[status(thm)],[139])).
% 2.47/2.72 tff(141,axiom,(![U: $i] : (ssList(U) => ![V: $i] : (ssItem(V) => (hd(cons(V, U)) = V)))), file('/export/starexec/sandbox/benchmark/Axioms/SWC001+0.ax','ax23')).
% 2.47/2.72 tff(142,plain,
% 2.47/2.72 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (hd(cons(V, U)) = V)))),
% 2.47/2.72 inference(modus_ponens,[status(thm)],[141, 140])).
% 2.47/2.72 tff(143,plain,
% 2.47/2.72 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (hd(cons(V, U)) = V)))),
% 2.47/2.72 inference(modus_ponens,[status(thm)],[142, 138])).
% 2.47/2.72 tff(144,plain,(
% 2.47/2.72 ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (hd(cons(V, U)) = V)))),
% 2.47/2.72 inference(skolemize,[status(sab)],[143])).
% 2.47/2.72 tff(145,plain,
% 2.47/2.72 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (hd(cons(V, U)) = V)))),
% 2.47/2.72 inference(modus_ponens,[status(thm)],[144, 137])).
% 2.47/2.72 tff(146,plain,
% 2.47/2.72 (((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (hd(cons(V, U)) = V)))) | ((~ssList(tptp_fun_V_43(U!45))) | ![V: $i] : ((~ssItem(V)) | (hd(cons(V, tptp_fun_V_43(U!45))) = V)))) <=> ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (hd(cons(V, U)) = V)))) | (~ssList(tptp_fun_V_43(U!45))) | ![V: $i] : ((~ssItem(V)) | (hd(cons(V, tptp_fun_V_43(U!45))) = V)))),
% 2.47/2.72 inference(rewrite,[status(thm)],[])).
% 2.47/2.72 tff(147,plain,
% 2.47/2.72 ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (hd(cons(V, U)) = V)))) | ((~ssList(tptp_fun_V_43(U!45))) | ![V: $i] : ((~ssItem(V)) | (hd(cons(V, tptp_fun_V_43(U!45))) = V)))),
% 2.47/2.72 inference(quant_inst,[status(thm)],[])).
% 2.47/2.72 tff(148,plain,
% 2.47/2.72 ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssItem(V)) | (hd(cons(V, U)) = V)))) | (~ssList(tptp_fun_V_43(U!45))) | ![V: $i] : ((~ssItem(V)) | (hd(cons(V, tptp_fun_V_43(U!45))) = V))),
% 2.47/2.72 inference(modus_ponens,[status(thm)],[147, 146])).
% 2.47/2.72 tff(149,plain,
% 2.47/2.72 (![V: $i] : ((~ssItem(V)) | (hd(cons(V, tptp_fun_V_43(U!45))) = V))),
% 2.47/2.72 inference(unit_resolution,[status(thm)],[148, 145, 125])).
% 2.47/2.72 tff(150,plain,
% 2.47/2.72 (((~![V: $i] : ((~ssItem(V)) | (hd(cons(V, tptp_fun_V_43(U!45))) = V))) | ((~ssItem(tptp_fun_W_44(U!45))) | (hd(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45))) = tptp_fun_W_44(U!45)))) <=> ((~![V: $i] : ((~ssItem(V)) | (hd(cons(V, tptp_fun_V_43(U!45))) = V))) | (~ssItem(tptp_fun_W_44(U!45))) | (hd(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45))) = tptp_fun_W_44(U!45)))),
% 2.56/2.73 inference(rewrite,[status(thm)],[])).
% 2.56/2.73 tff(151,plain,
% 2.56/2.73 ((~![V: $i] : ((~ssItem(V)) | (hd(cons(V, tptp_fun_V_43(U!45))) = V))) | ((~ssItem(tptp_fun_W_44(U!45))) | (hd(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45))) = tptp_fun_W_44(U!45)))),
% 2.56/2.73 inference(quant_inst,[status(thm)],[])).
% 2.56/2.73 tff(152,plain,
% 2.56/2.73 ((~![V: $i] : ((~ssItem(V)) | (hd(cons(V, tptp_fun_V_43(U!45))) = V))) | (~ssItem(tptp_fun_W_44(U!45))) | (hd(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45))) = tptp_fun_W_44(U!45))),
% 2.56/2.73 inference(modus_ponens,[status(thm)],[151, 150])).
% 2.56/2.73 tff(153,plain,
% 2.56/2.73 (hd(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45))) = tptp_fun_W_44(U!45)),
% 2.56/2.73 inference(unit_resolution,[status(thm)],[152, 119, 149])).
% 2.56/2.73 tff(154,plain,
% 2.56/2.73 (tptp_fun_W_44(U!45) = hd(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)))),
% 2.56/2.73 inference(symmetry,[status(thm)],[153])).
% 2.56/2.73 tff(155,plain,
% 2.56/2.73 (tptp_fun_W_44(U!45) = hd(U!45)),
% 2.56/2.73 inference(transitivity,[status(thm)],[154, 132])).
% 2.56/2.73 tff(156,plain,
% 2.56/2.73 (hd(U!45) = tptp_fun_W_44(U!45)),
% 2.56/2.73 inference(modus_ponens,[status(thm)],[155, 131])).
% 2.56/2.73 tff(157,plain,
% 2.56/2.73 (((hd(U!45) = tptp_fun_W_44(U!45)) | memberP(tptp_fun_V_43(U!45), hd(U!45))) | (~(hd(U!45) = tptp_fun_W_44(U!45)))),
% 2.56/2.73 inference(tautology,[status(thm)],[])).
% 2.56/2.73 tff(158,plain,
% 2.56/2.73 ((hd(U!45) = tptp_fun_W_44(U!45)) | memberP(tptp_fun_V_43(U!45), hd(U!45))),
% 2.56/2.73 inference(unit_resolution,[status(thm)],[157, 156])).
% 2.56/2.73 tff(159,plain,
% 2.56/2.73 ((~(memberP(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)), hd(U!45)) <=> ((hd(U!45) = tptp_fun_W_44(U!45)) | memberP(tptp_fun_V_43(U!45), hd(U!45))))) | memberP(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)), hd(U!45)) | (~((hd(U!45) = tptp_fun_W_44(U!45)) | memberP(tptp_fun_V_43(U!45), hd(U!45))))),
% 2.56/2.73 inference(tautology,[status(thm)],[])).
% 2.56/2.73 tff(160,plain,
% 2.56/2.73 ((~(memberP(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)), hd(U!45)) <=> ((hd(U!45) = tptp_fun_W_44(U!45)) | memberP(tptp_fun_V_43(U!45), hd(U!45))))) | memberP(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)), hd(U!45))),
% 2.56/2.73 inference(unit_resolution,[status(thm)],[159, 158])).
% 2.56/2.73 tff(161,plain,
% 2.56/2.73 (memberP(cons(tptp_fun_W_44(U!45), tptp_fun_V_43(U!45)), hd(U!45))),
% 2.56/2.73 inference(unit_resolution,[status(thm)],[160, 129])).
% 2.56/2.73 tff(162,plain,
% 2.56/2.73 ($false),
% 2.56/2.73 inference(unit_resolution,[status(thm)],[161, 100])).
% 2.56/2.73 % SZS output end Proof
% 2.56/2.73 % E exiting
%------------------------------------------------------------------------------