%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SWC039+1 : TPTP v9.0.0. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n004.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:00 AM UTC 2025
% Result : Theorem 11.80s 12.01s
% Output : Proof 11.88s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.13 % Problem : SWC039+1 : TPTP v9.0.0. Released v2.4.0.
% 0.04/0.13 % Command : run_E %s %d THM
% 0.13/0.34 % Computer : n004.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Fri Jun 20 08:05:38 EDT 2025
% 0.13/0.34 % CPUTime :
% 11.80/12.01 % SZS status Theorem
% 11.80/12.01 % SZS output start Proof
% 11.80/12.01 tff(nil_type, type, (
% 11.80/12.01 nil: $i)).
% 11.80/12.01 tff(app_type, type, (
% 11.80/12.01 app: ( $i * $i ) > $i)).
% 11.80/12.01 tff(tptp_fun_U_45_type, type, (
% 11.80/12.01 tptp_fun_U_45: $i)).
% 11.80/12.01 tff(tptp_fun_Z_47_type, type, (
% 11.80/12.01 tptp_fun_Z_47: $i)).
% 11.80/12.01 tff(ssList_type, type, (
% 11.80/12.01 ssList: $i > $o)).
% 11.80/12.01 tff(frontsegP_type, type, (
% 11.80/12.01 frontsegP: ( $i * $i ) > $o)).
% 11.80/12.01 tff(tptp_fun_W_5_type, type, (
% 11.80/12.01 tptp_fun_W_5: ( $i * $i ) > $i)).
% 11.80/12.01 tff(lt_type, type, (
% 11.80/12.01 lt: ( $i * $i ) > $o)).
% 11.80/12.01 tff(tptp_fun_Y_46_type, type, (
% 11.80/12.01 tptp_fun_Y_46: $i)).
% 11.80/12.01 tff(memberP_type, type, (
% 11.80/12.01 memberP: ( $i * $i ) > $o)).
% 11.80/12.01 tff(tptp_fun_X1_48_type, type, (
% 11.80/12.01 tptp_fun_X1_48: $i)).
% 11.80/12.01 tff(ssItem_type, type, (
% 11.80/12.01 ssItem: $i > $o)).
% 11.80/12.01 tff(cons_type, type, (
% 11.80/12.01 cons: ( $i * $i ) > $i)).
% 11.80/12.01 tff(1,plain,
% 11.80/12.01 (((~(nil = U!45)) & ssList(U!45) & ssList(nil) & ((ssItem(Y!46) & (ssList(Z!47) & (ssList(X1!48) & ![X2: $i] : (~(ssItem(X2) & memberP(Z!47, X2) & lt(Y!46, X2))) & ![X3: $i] : (~(ssItem(X3) & memberP(X1!48, X3) & lt(X3, Y!46))) & (cons(Y!46, nil) = U!45) & (app(app(Z!47, U!45), X1!48) = nil)))) | (nil = U!45))) <=> ((~(nil = U!45)) & ssList(U!45) & ssList(nil) & ((nil = U!45) | (ssItem(Y!46) & ssList(Z!47) & ssList(X1!48) & ![X2: $i] : (~(ssItem(X2) & memberP(Z!47, X2) & lt(Y!46, X2))) & ![X3: $i] : (~(ssItem(X3) & memberP(X1!48, X3) & lt(X3, Y!46))) & (cons(Y!46, nil) = U!45) & (app(app(Z!47, U!45), X1!48) = nil))))),
% 11.80/12.01 inference(rewrite,[status(thm)],[])).
% 11.80/12.01 tff(2,plain,
% 11.80/12.01 ((~![U: $i] : ((nil = U) | (~ssList(U)) | (~ssList(nil)) | (![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | ?[X2: $i] : (ssItem(X2) & memberP(Z, X2) & lt(Y, X2)) | ?[X3: $i] : (ssItem(X3) & memberP(X1, X3) & lt(X3, Y)) | (~(cons(Y, nil) = U)) | (~(app(app(Z, U), X1) = nil))))) & (~(nil = U))))) <=> (~![U: $i] : ((nil = U) | (~ssList(U)) | (~ssList(nil)) | (![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | ?[X2: $i] : (ssItem(X2) & memberP(Z, X2) & lt(Y, X2)) | ?[X3: $i] : (ssItem(X3) & memberP(X1, X3) & lt(X3, Y)) | (~(cons(Y, nil) = U)) | (~(app(app(Z, U), X1) = nil))))) & (~(nil = U)))))),
% 11.80/12.01 inference(rewrite,[status(thm)],[])).
% 11.80/12.01 tff(3,plain,
% 11.80/12.01 ((~![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) => ![Z: $i] : (ssList(Z) => ![X1: $i] : (ssList(X1) => ((((~(cons(Y, nil) = W)) | (~(app(app(Z, W), X1) = X))) | ?[X2: $i] : ((ssItem(X2) & memberP(Z, X2)) & lt(Y, X2))) | ?[X3: $i] : ((ssItem(X3) & memberP(X1, X3)) & lt(X3, Y)))))) & ((~(nil = X)) | (~(nil = W)))))))))) <=> (~![U: $i] : ((nil = U) | (~ssList(U)) | (~ssList(nil)) | (![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | ?[X2: $i] : (ssItem(X2) & memberP(Z, X2) & lt(Y, X2)) | ?[X3: $i] : (ssItem(X3) & memberP(X1, X3) & lt(X3, Y)) | (~(cons(Y, nil) = U)) | (~(app(app(Z, U), X1) = nil))))) & (~(nil = U)))))),
% 11.80/12.01 inference(rewrite,[status(thm)],[])).
% 11.80/12.01 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) => ![Z: $i] : (ssList(Z) => ![X1: $i] : (ssList(X1) => ((((~(cons(Y, nil) = W)) | (~(app(app(Z, W), X1) = X))) | ?[X2: $i] : ((ssItem(X2) & memberP(Z, X2)) & lt(Y, X2))) | ?[X3: $i] : ((ssItem(X3) & memberP(X1, X3)) & lt(X3, Y)))))) & ((~(nil = X)) | (~(nil = W)))))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','co1')).
% 11.80/12.01 tff(5,plain,
% 11.80/12.01 (~![U: $i] : ((nil = U) | (~ssList(U)) | (~ssList(nil)) | (![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | ?[X2: $i] : (ssItem(X2) & memberP(Z, X2) & lt(Y, X2)) | ?[X3: $i] : (ssItem(X3) & memberP(X1, X3) & lt(X3, Y)) | (~(cons(Y, nil) = U)) | (~(app(app(Z, U), X1) = nil))))) & (~(nil = U))))),
% 11.80/12.01 inference(modus_ponens,[status(thm)],[4, 3])).
% 11.80/12.01 tff(6,plain,
% 11.80/12.01 (~![U: $i] : ((nil = U) | (~ssList(U)) | (~ssList(nil)) | (![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | ?[X2: $i] : (ssItem(X2) & memberP(Z, X2) & lt(Y, X2)) | ?[X3: $i] : (ssItem(X3) & memberP(X1, X3) & lt(X3, Y)) | (~(cons(Y, nil) = U)) | (~(app(app(Z, U), X1) = nil))))) & (~(nil = U))))),
% 11.80/12.01 inference(modus_ponens,[status(thm)],[5, 2])).
% 11.80/12.01 tff(7,plain,
% 11.80/12.01 (~![U: $i] : ((nil = U) | (~ssList(U)) | (~ssList(nil)) | (![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | ?[X2: $i] : (ssItem(X2) & memberP(Z, X2) & lt(Y, X2)) | ?[X3: $i] : (ssItem(X3) & memberP(X1, X3) & lt(X3, Y)) | (~(cons(Y, nil) = U)) | (~(app(app(Z, U), X1) = nil))))) & (~(nil = U))))),
% 11.80/12.01 inference(modus_ponens,[status(thm)],[6, 2])).
% 11.80/12.01 tff(8,plain,
% 11.80/12.01 (~![U: $i] : ((nil = U) | (~ssList(U)) | (~ssList(nil)) | (![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | ?[X2: $i] : (ssItem(X2) & memberP(Z, X2) & lt(Y, X2)) | ?[X3: $i] : (ssItem(X3) & memberP(X1, X3) & lt(X3, Y)) | (~(cons(Y, nil) = U)) | (~(app(app(Z, U), X1) = nil))))) & (~(nil = U))))),
% 11.80/12.01 inference(modus_ponens,[status(thm)],[7, 2])).
% 11.80/12.01 tff(9,plain,
% 11.80/12.01 ((~(nil = U!45)) & ssList(U!45) & ssList(nil) & ((nil = U!45) | (ssItem(Y!46) & ssList(Z!47) & ssList(X1!48) & ![X2: $i] : (~(ssItem(X2) & memberP(Z!47, X2) & lt(Y!46, X2))) & ![X3: $i] : (~(ssItem(X3) & memberP(X1!48, X3) & lt(X3, Y!46))) & (cons(Y!46, nil) = U!45) & (app(app(Z!47, U!45), X1!48) = nil)))),
% 11.80/12.01 inference(modus_ponens,[status(thm)],[8, 1])).
% 11.80/12.01 tff(10,plain,
% 11.80/12.01 (~(nil = U!45)),
% 11.80/12.01 inference(and_elim,[status(thm)],[9])).
% 11.80/12.01 tff(11,plain,
% 11.80/12.01 (((nil = U!45) | (~((~(cons(Y!46, nil) = U!45)) | (~ssItem(Y!46)) | (~ssList(Z!47)) | (~(app(app(Z!47, U!45), X1!48) = nil)) | (~ssList(X1!48)) | (~![X2: $i] : ((~ssItem(X2)) | (~memberP(Z!47, X2)) | (~lt(Y!46, X2)))) | (~![X3: $i] : ((~ssItem(X3)) | (~memberP(X1!48, X3)) | (~lt(X3, Y!46))))))) <=> ((nil = U!45) | (~((~(cons(Y!46, nil) = U!45)) | (~ssItem(Y!46)) | (~ssList(Z!47)) | (~(app(app(Z!47, U!45), X1!48) = nil)) | (~ssList(X1!48)) | (~![X2: $i] : ((~ssItem(X2)) | (~memberP(Z!47, X2)) | (~lt(Y!46, X2)))) | (~![X3: $i] : ((~ssItem(X3)) | (~memberP(X1!48, X3)) | (~lt(X3, Y!46)))))))),
% 11.80/12.01 inference(rewrite,[status(thm)],[])).
% 11.80/12.01 tff(12,plain,
% 11.80/12.01 (((nil = U!45) | (~((~(cons(Y!46, nil) = U!45)) | (~ssItem(Y!46)) | (~ssList(Z!47)) | (~(app(app(Z!47, U!45), X1!48) = nil)) | (~ssList(X1!48)) | (~![X2: $i] : ((~ssItem(X2)) | (~memberP(Z!47, X2)) | (~lt(Y!46, X2)))) | (~![X3: $i] : ((~ssItem(X3)) | (~memberP(X1!48, X3)) | (~lt(X3, Y!46))))))) <=> ((nil = U!45) | (~((~(cons(Y!46, nil) = U!45)) | (~ssItem(Y!46)) | (~ssList(Z!47)) | (~(app(app(Z!47, U!45), X1!48) = nil)) | (~ssList(X1!48)) | (~![X2: $i] : ((~ssItem(X2)) | (~memberP(Z!47, X2)) | (~lt(Y!46, X2)))) | (~![X3: $i] : ((~ssItem(X3)) | (~memberP(X1!48, X3)) | (~lt(X3, Y!46)))))))),
% 11.80/12.01 inference(rewrite,[status(thm)],[])).
% 11.80/12.01 tff(13,plain,
% 11.80/12.01 ((ssItem(Y!46) & ssList(Z!47) & ssList(X1!48) & ![X2: $i] : ((~ssItem(X2)) | (~memberP(Z!47, X2)) | (~lt(Y!46, X2))) & ![X3: $i] : ((~ssItem(X3)) | (~memberP(X1!48, X3)) | (~lt(X3, Y!46))) & (cons(Y!46, nil) = U!45) & (app(app(Z!47, U!45), X1!48) = nil)) <=> (~((~(cons(Y!46, nil) = U!45)) | (~ssItem(Y!46)) | (~ssList(Z!47)) | (~(app(app(Z!47, U!45), X1!48) = nil)) | (~ssList(X1!48)) | (~![X2: $i] : ((~ssItem(X2)) | (~memberP(Z!47, X2)) | (~lt(Y!46, X2)))) | (~![X3: $i] : ((~ssItem(X3)) | (~memberP(X1!48, X3)) | (~lt(X3, Y!46))))))),
% 11.80/12.01 inference(rewrite,[status(thm)],[])).
% 11.80/12.01 tff(14,plain,
% 11.80/12.01 (^[X3: $i] : trans(monotonicity(rewrite((ssItem(X3) & memberP(X1!48, X3) & lt(X3, Y!46)) <=> (~((~ssItem(X3)) | (~memberP(X1!48, X3)) | (~lt(X3, Y!46))))), ((~(ssItem(X3) & memberP(X1!48, X3) & lt(X3, Y!46))) <=> (~(~((~ssItem(X3)) | (~memberP(X1!48, X3)) | (~lt(X3, Y!46))))))), rewrite((~(~((~ssItem(X3)) | (~memberP(X1!48, X3)) | (~lt(X3, Y!46))))) <=> ((~ssItem(X3)) | (~memberP(X1!48, X3)) | (~lt(X3, Y!46)))), ((~(ssItem(X3) & memberP(X1!48, X3) & lt(X3, Y!46))) <=> ((~ssItem(X3)) | (~memberP(X1!48, X3)) | (~lt(X3, Y!46)))))),
% 11.80/12.01 inference(bind,[status(th)],[])).
% 11.80/12.01 tff(15,plain,
% 11.80/12.01 (![X3: $i] : (~(ssItem(X3) & memberP(X1!48, X3) & lt(X3, Y!46))) <=> ![X3: $i] : ((~ssItem(X3)) | (~memberP(X1!48, X3)) | (~lt(X3, Y!46)))),
% 11.80/12.01 inference(quant_intro,[status(thm)],[14])).
% 11.80/12.01 tff(16,plain,
% 11.80/12.01 (^[X2: $i] : trans(monotonicity(rewrite((ssItem(X2) & memberP(Z!47, X2) & lt(Y!46, X2)) <=> (~((~ssItem(X2)) | (~memberP(Z!47, X2)) | (~lt(Y!46, X2))))), ((~(ssItem(X2) & memberP(Z!47, X2) & lt(Y!46, X2))) <=> (~(~((~ssItem(X2)) | (~memberP(Z!47, X2)) | (~lt(Y!46, X2))))))), rewrite((~(~((~ssItem(X2)) | (~memberP(Z!47, X2)) | (~lt(Y!46, X2))))) <=> ((~ssItem(X2)) | (~memberP(Z!47, X2)) | (~lt(Y!46, X2)))), ((~(ssItem(X2) & memberP(Z!47, X2) & lt(Y!46, X2))) <=> ((~ssItem(X2)) | (~memberP(Z!47, X2)) | (~lt(Y!46, X2)))))),
% 11.80/12.01 inference(bind,[status(th)],[])).
% 11.80/12.01 tff(17,plain,
% 11.80/12.01 (![X2: $i] : (~(ssItem(X2) & memberP(Z!47, X2) & lt(Y!46, X2))) <=> ![X2: $i] : ((~ssItem(X2)) | (~memberP(Z!47, X2)) | (~lt(Y!46, X2)))),
% 11.80/12.01 inference(quant_intro,[status(thm)],[16])).
% 11.80/12.01 tff(18,plain,
% 11.80/12.01 ((ssItem(Y!46) & ssList(Z!47) & ssList(X1!48) & ![X2: $i] : (~(ssItem(X2) & memberP(Z!47, X2) & lt(Y!46, X2))) & ![X3: $i] : (~(ssItem(X3) & memberP(X1!48, X3) & lt(X3, Y!46))) & (cons(Y!46, nil) = U!45) & (app(app(Z!47, U!45), X1!48) = nil)) <=> (ssItem(Y!46) & ssList(Z!47) & ssList(X1!48) & ![X2: $i] : ((~ssItem(X2)) | (~memberP(Z!47, X2)) | (~lt(Y!46, X2))) & ![X3: $i] : ((~ssItem(X3)) | (~memberP(X1!48, X3)) | (~lt(X3, Y!46))) & (cons(Y!46, nil) = U!45) & (app(app(Z!47, U!45), X1!48) = nil))),
% 11.80/12.01 inference(monotonicity,[status(thm)],[17, 15])).
% 11.80/12.01 tff(19,plain,
% 11.80/12.01 ((ssItem(Y!46) & ssList(Z!47) & ssList(X1!48) & ![X2: $i] : (~(ssItem(X2) & memberP(Z!47, X2) & lt(Y!46, X2))) & ![X3: $i] : (~(ssItem(X3) & memberP(X1!48, X3) & lt(X3, Y!46))) & (cons(Y!46, nil) = U!45) & (app(app(Z!47, U!45), X1!48) = nil)) <=> (~((~(cons(Y!46, nil) = U!45)) | (~ssItem(Y!46)) | (~ssList(Z!47)) | (~(app(app(Z!47, U!45), X1!48) = nil)) | (~ssList(X1!48)) | (~![X2: $i] : ((~ssItem(X2)) | (~memberP(Z!47, X2)) | (~lt(Y!46, X2)))) | (~![X3: $i] : ((~ssItem(X3)) | (~memberP(X1!48, X3)) | (~lt(X3, Y!46))))))),
% 11.80/12.01 inference(transitivity,[status(thm)],[18, 13])).
% 11.80/12.01 tff(20,plain,
% 11.80/12.01 (((nil = U!45) | (ssItem(Y!46) & ssList(Z!47) & ssList(X1!48) & ![X2: $i] : (~(ssItem(X2) & memberP(Z!47, X2) & lt(Y!46, X2))) & ![X3: $i] : (~(ssItem(X3) & memberP(X1!48, X3) & lt(X3, Y!46))) & (cons(Y!46, nil) = U!45) & (app(app(Z!47, U!45), X1!48) = nil))) <=> ((nil = U!45) | (~((~(cons(Y!46, nil) = U!45)) | (~ssItem(Y!46)) | (~ssList(Z!47)) | (~(app(app(Z!47, U!45), X1!48) = nil)) | (~ssList(X1!48)) | (~![X2: $i] : ((~ssItem(X2)) | (~memberP(Z!47, X2)) | (~lt(Y!46, X2)))) | (~![X3: $i] : ((~ssItem(X3)) | (~memberP(X1!48, X3)) | (~lt(X3, Y!46)))))))),
% 11.80/12.01 inference(monotonicity,[status(thm)],[19])).
% 11.80/12.01 tff(21,plain,
% 11.80/12.01 (((nil = U!45) | (ssItem(Y!46) & ssList(Z!47) & ssList(X1!48) & ![X2: $i] : (~(ssItem(X2) & memberP(Z!47, X2) & lt(Y!46, X2))) & ![X3: $i] : (~(ssItem(X3) & memberP(X1!48, X3) & lt(X3, Y!46))) & (cons(Y!46, nil) = U!45) & (app(app(Z!47, U!45), X1!48) = nil))) <=> ((nil = U!45) | (~((~(cons(Y!46, nil) = U!45)) | (~ssItem(Y!46)) | (~ssList(Z!47)) | (~(app(app(Z!47, U!45), X1!48) = nil)) | (~ssList(X1!48)) | (~![X2: $i] : ((~ssItem(X2)) | (~memberP(Z!47, X2)) | (~lt(Y!46, X2)))) | (~![X3: $i] : ((~ssItem(X3)) | (~memberP(X1!48, X3)) | (~lt(X3, Y!46)))))))),
% 11.80/12.01 inference(transitivity,[status(thm)],[20, 12])).
% 11.80/12.01 tff(22,plain,
% 11.80/12.01 ((nil = U!45) | (ssItem(Y!46) & ssList(Z!47) & ssList(X1!48) & ![X2: $i] : (~(ssItem(X2) & memberP(Z!47, X2) & lt(Y!46, X2))) & ![X3: $i] : (~(ssItem(X3) & memberP(X1!48, X3) & lt(X3, Y!46))) & (cons(Y!46, nil) = U!45) & (app(app(Z!47, U!45), X1!48) = nil))),
% 11.80/12.01 inference(and_elim,[status(thm)],[9])).
% 11.80/12.01 tff(23,plain,
% 11.80/12.01 ((nil = U!45) | (~((~(cons(Y!46, nil) = U!45)) | (~ssItem(Y!46)) | (~ssList(Z!47)) | (~(app(app(Z!47, U!45), X1!48) = nil)) | (~ssList(X1!48)) | (~![X2: $i] : ((~ssItem(X2)) | (~memberP(Z!47, X2)) | (~lt(Y!46, X2)))) | (~![X3: $i] : ((~ssItem(X3)) | (~memberP(X1!48, X3)) | (~lt(X3, Y!46))))))),
% 11.80/12.01 inference(modus_ponens,[status(thm)],[22, 21])).
% 11.80/12.01 tff(24,plain,
% 11.80/12.01 ((nil = U!45) | (~((~(cons(Y!46, nil) = U!45)) | (~ssItem(Y!46)) | (~ssList(Z!47)) | (~(app(app(Z!47, U!45), X1!48) = nil)) | (~ssList(X1!48)) | (~![X2: $i] : ((~ssItem(X2)) | (~memberP(Z!47, X2)) | (~lt(Y!46, X2)))) | (~![X3: $i] : ((~ssItem(X3)) | (~memberP(X1!48, X3)) | (~lt(X3, Y!46))))))),
% 11.80/12.01 inference(modus_ponens,[status(thm)],[23, 11])).
% 11.80/12.01 tff(25,plain,
% 11.80/12.01 (~((~(cons(Y!46, nil) = U!45)) | (~ssItem(Y!46)) | (~ssList(Z!47)) | (~(app(app(Z!47, U!45), X1!48) = nil)) | (~ssList(X1!48)) | (~![X2: $i] : ((~ssItem(X2)) | (~memberP(Z!47, X2)) | (~lt(Y!46, X2)))) | (~![X3: $i] : ((~ssItem(X3)) | (~memberP(X1!48, X3)) | (~lt(X3, Y!46)))))),
% 11.80/12.01 inference(unit_resolution,[status(thm)],[24, 10])).
% 11.80/12.01 tff(26,plain,
% 11.80/12.01 (((~(cons(Y!46, nil) = U!45)) | (~ssItem(Y!46)) | (~ssList(Z!47)) | (~(app(app(Z!47, U!45), X1!48) = nil)) | (~ssList(X1!48)) | (~![X2: $i] : ((~ssItem(X2)) | (~memberP(Z!47, X2)) | (~lt(Y!46, X2)))) | (~![X3: $i] : ((~ssItem(X3)) | (~memberP(X1!48, X3)) | (~lt(X3, Y!46))))) | ssList(Z!47)),
% 11.80/12.01 inference(tautology,[status(thm)],[])).
% 11.80/12.01 tff(27,plain,
% 11.80/12.01 (ssList(Z!47)),
% 11.80/12.01 inference(unit_resolution,[status(thm)],[26, 25])).
% 11.80/12.01 tff(28,plain,
% 11.80/12.01 (^[U: $i] : refl(((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ssList(app(U, V)))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ssList(app(U, V)))))),
% 11.80/12.01 inference(bind,[status(th)],[])).
% 11.80/12.01 tff(29,plain,
% 11.80/12.01 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ssList(app(U, V)))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ssList(app(U, V))))),
% 11.80/12.01 inference(quant_intro,[status(thm)],[28])).
% 11.80/12.01 tff(30,plain,
% 11.80/12.01 (^[U: $i] : rewrite(((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ssList(app(U, V)))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ssList(app(U, V)))))),
% 11.80/12.01 inference(bind,[status(th)],[])).
% 11.80/12.01 tff(31,plain,
% 11.80/12.01 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ssList(app(U, V)))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ssList(app(U, V))))),
% 11.80/12.01 inference(quant_intro,[status(thm)],[30])).
% 11.80/12.01 tff(32,plain,
% 11.80/12.01 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ssList(app(U, V)))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ssList(app(U, V))))),
% 11.80/12.01 inference(transitivity,[status(thm)],[31, 29])).
% 11.80/12.01 tff(33,plain,
% 11.80/12.01 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ssList(app(U, V)))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ssList(app(U, V))))),
% 11.80/12.01 inference(rewrite,[status(thm)],[])).
% 11.80/12.01 tff(34,plain,
% 11.80/12.01 (^[U: $i] : trans(monotonicity(quant_intro(proof_bind(^[V: $i] : rewrite((ssList(V) => ssList(app(U, V))) <=> ((~ssList(V)) | ssList(app(U, V))))), (![V: $i] : (ssList(V) => ssList(app(U, V))) <=> ![V: $i] : ((~ssList(V)) | ssList(app(U, V))))), ((ssList(U) => ![V: $i] : (ssList(V) => ssList(app(U, V)))) <=> (ssList(U) => ![V: $i] : ((~ssList(V)) | ssList(app(U, V)))))), rewrite((ssList(U) => ![V: $i] : ((~ssList(V)) | ssList(app(U, V)))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ssList(app(U, V))))), ((ssList(U) => ![V: $i] : (ssList(V) => ssList(app(U, V)))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ssList(app(U, V))))))),
% 11.80/12.01 inference(bind,[status(th)],[])).
% 11.80/12.01 tff(35,plain,
% 11.80/12.01 (![U: $i] : (ssList(U) => ![V: $i] : (ssList(V) => ssList(app(U, V)))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ssList(app(U, V))))),
% 11.80/12.01 inference(quant_intro,[status(thm)],[34])).
% 11.80/12.01 tff(36,axiom,(![U: $i] : (ssList(U) => ![V: $i] : (ssList(V) => ssList(app(U, V))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax','ax26')).
% 11.80/12.01 tff(37,plain,
% 11.80/12.01 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ssList(app(U, V))))),
% 11.80/12.01 inference(modus_ponens,[status(thm)],[36, 35])).
% 11.80/12.01 tff(38,plain,
% 11.80/12.01 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ssList(app(U, V))))),
% 11.80/12.01 inference(modus_ponens,[status(thm)],[37, 33])).
% 11.80/12.01 tff(39,plain,(
% 11.80/12.01 ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ssList(app(U, V))))),
% 11.80/12.01 inference(skolemize,[status(sab)],[38])).
% 11.80/12.01 tff(40,plain,
% 11.80/12.01 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ssList(app(U, V))))),
% 11.80/12.01 inference(modus_ponens,[status(thm)],[39, 32])).
% 11.80/12.01 tff(41,plain,
% 11.80/12.01 (((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ssList(app(U, V))))) | ((~ssList(Z!47)) | ![V: $i] : ((~ssList(V)) | ssList(app(Z!47, V))))) <=> ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ssList(app(U, V))))) | (~ssList(Z!47)) | ![V: $i] : ((~ssList(V)) | ssList(app(Z!47, V))))),
% 11.80/12.01 inference(rewrite,[status(thm)],[])).
% 11.80/12.01 tff(42,plain,
% 11.80/12.01 ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ssList(app(U, V))))) | ((~ssList(Z!47)) | ![V: $i] : ((~ssList(V)) | ssList(app(Z!47, V))))),
% 11.80/12.01 inference(quant_inst,[status(thm)],[])).
% 11.80/12.01 tff(43,plain,
% 11.80/12.01 ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ssList(app(U, V))))) | (~ssList(Z!47)) | ![V: $i] : ((~ssList(V)) | ssList(app(Z!47, V)))),
% 11.80/12.01 inference(modus_ponens,[status(thm)],[42, 41])).
% 11.80/12.01 tff(44,plain,
% 11.80/12.01 (![V: $i] : ((~ssList(V)) | ssList(app(Z!47, V)))),
% 11.80/12.01 inference(unit_resolution,[status(thm)],[43, 40, 27])).
% 11.80/12.01 tff(45,plain,
% 11.80/12.01 (ssList(U!45)),
% 11.80/12.01 inference(and_elim,[status(thm)],[9])).
% 11.80/12.01 tff(46,plain,
% 11.80/12.01 (((~![V: $i] : ((~ssList(V)) | ssList(app(Z!47, V)))) | ((~ssList(U!45)) | ssList(app(Z!47, U!45)))) <=> ((~![V: $i] : ((~ssList(V)) | ssList(app(Z!47, V)))) | (~ssList(U!45)) | ssList(app(Z!47, U!45)))),
% 11.80/12.01 inference(rewrite,[status(thm)],[])).
% 11.80/12.01 tff(47,plain,
% 11.80/12.01 ((~![V: $i] : ((~ssList(V)) | ssList(app(Z!47, V)))) | ((~ssList(U!45)) | ssList(app(Z!47, U!45)))),
% 11.80/12.01 inference(quant_inst,[status(thm)],[])).
% 11.80/12.01 tff(48,plain,
% 11.80/12.01 ((~![V: $i] : ((~ssList(V)) | ssList(app(Z!47, V)))) | (~ssList(U!45)) | ssList(app(Z!47, U!45))),
% 11.80/12.01 inference(modus_ponens,[status(thm)],[47, 46])).
% 11.80/12.01 tff(49,plain,
% 11.80/12.01 (ssList(app(Z!47, U!45))),
% 11.80/12.01 inference(unit_resolution,[status(thm)],[48, 45, 44])).
% 11.80/12.01 tff(50,plain,
% 11.80/12.01 (ssList(nil) <=> ssList(nil)),
% 11.80/12.01 inference(rewrite,[status(thm)],[])).
% 11.80/12.01 tff(51,axiom,(ssList(nil)), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax','ax17')).
% 11.80/12.01 tff(52,plain,
% 11.80/12.01 (ssList(nil)),
% 11.80/12.01 inference(modus_ponens,[status(thm)],[51, 50])).
% 11.80/12.01 tff(53,plain,
% 11.80/12.01 (^[U: $i] : refl(((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U))))))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U))))))))))),
% 11.80/12.01 inference(bind,[status(th)],[])).
% 11.80/12.01 tff(54,plain,
% 11.80/12.01 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U))))))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U)))))))))),
% 11.80/12.01 inference(quant_intro,[status(thm)],[53])).
% 11.80/12.01 tff(55,plain,
% 11.80/12.01 (^[U: $i] : rewrite(((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U))))))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U))))))))))),
% 11.80/12.01 inference(bind,[status(th)],[])).
% 11.80/12.01 tff(56,plain,
% 11.80/12.01 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U))))))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U)))))))))),
% 11.80/12.01 inference(quant_intro,[status(thm)],[55])).
% 11.80/12.01 tff(57,plain,
% 11.80/12.01 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U))))))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U)))))))))),
% 11.80/12.01 inference(transitivity,[status(thm)],[56, 54])).
% 11.80/12.01 tff(58,plain,
% 11.80/12.01 (^[U: $i] : rewrite(((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (((~frontsegP(U, V)) | (ssList(tptp_fun_W_5(V, U)) & (app(V, tptp_fun_W_5(V, U)) = U))) & (frontsegP(U, V) | ![W: $i] : (~(ssList(W) & (app(V, W) = U))))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U))))))))))),
% 11.80/12.01 inference(bind,[status(th)],[])).
% 11.80/12.01 tff(59,plain,
% 11.80/12.01 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (((~frontsegP(U, V)) | (ssList(tptp_fun_W_5(V, U)) & (app(V, tptp_fun_W_5(V, U)) = U))) & (frontsegP(U, V) | ![W: $i] : (~(ssList(W) & (app(V, W) = U))))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U)))))))))),
% 11.80/12.01 inference(quant_intro,[status(thm)],[58])).
% 11.80/12.01 tff(60,plain,
% 11.80/12.01 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U)))))),
% 11.80/12.01 inference(rewrite,[status(thm)],[])).
% 11.80/12.01 tff(61,plain,
% 11.80/12.01 (^[U: $i] : trans(monotonicity(quant_intro(proof_bind(^[V: $i] : trans(monotonicity(rewrite((frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U))) <=> (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U)))), ((ssList(V) => (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U)))) <=> (ssList(V) => (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U)))))), rewrite((ssList(V) => (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U)))) <=> ((~ssList(V)) | (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U))))), ((ssList(V) => (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U)))) <=> ((~ssList(V)) | (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U))))))), (![V: $i] : (ssList(V) => (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U)))) <=> ![V: $i] : ((~ssList(V)) | (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U)))))), ((ssList(U) => ![V: $i] : (ssList(V) => (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U))))) <=> (ssList(U) => ![V: $i] : ((~ssList(V)) | (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U))))))), rewrite((ssList(U) => ![V: $i] : ((~ssList(V)) | (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U)))))), ((ssList(U) => ![V: $i] : (ssList(V) => (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U)))))))),
% 11.80/12.01 inference(bind,[status(th)],[])).
% 11.80/12.01 tff(62,plain,
% 11.80/12.01 (![U: $i] : (ssList(U) => ![V: $i] : (ssList(V) => (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U)))))),
% 11.80/12.01 inference(quant_intro,[status(thm)],[61])).
% 11.80/12.01 tff(63,axiom,(![U: $i] : (ssList(U) => ![V: $i] : (ssList(V) => (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U)))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax','ax5')).
% 11.80/12.01 tff(64,plain,
% 11.80/12.01 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U)))))),
% 11.80/12.01 inference(modus_ponens,[status(thm)],[63, 62])).
% 11.80/12.01 tff(65,plain,
% 11.80/12.01 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (frontsegP(U, V) <=> ?[W: $i] : (ssList(W) & (app(V, W) = U)))))),
% 11.80/12.01 inference(modus_ponens,[status(thm)],[64, 60])).
% 11.80/12.01 tff(66,plain,(
% 11.80/12.01 ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (((~frontsegP(U, V)) | (ssList(tptp_fun_W_5(V, U)) & (app(V, tptp_fun_W_5(V, U)) = U))) & (frontsegP(U, V) | ![W: $i] : (~(ssList(W) & (app(V, W) = U)))))))),
% 11.80/12.01 inference(skolemize,[status(sab)],[65])).
% 11.80/12.01 tff(67,plain,
% 11.80/12.01 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U)))))))))),
% 11.80/12.01 inference(modus_ponens,[status(thm)],[66, 59])).
% 11.80/12.01 tff(68,plain,
% 11.80/12.01 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U)))))))))),
% 11.80/12.01 inference(modus_ponens,[status(thm)],[67, 57])).
% 11.80/12.01 tff(69,plain,
% 11.80/12.01 (((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U)))))))))) | ((~ssList(nil)) | ![V: $i] : ((~ssList(V)) | (~((~(frontsegP(nil, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = nil))))) | (~((~frontsegP(nil, V)) | (~((~ssList(tptp_fun_W_5(V, nil))) | (~(app(V, tptp_fun_W_5(V, nil)) = nil))))))))))) <=> ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U)))))))))) | (~ssList(nil)) | ![V: $i] : ((~ssList(V)) | (~((~(frontsegP(nil, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = nil))))) | (~((~frontsegP(nil, V)) | (~((~ssList(tptp_fun_W_5(V, nil))) | (~(app(V, tptp_fun_W_5(V, nil)) = nil))))))))))),
% 11.80/12.01 inference(rewrite,[status(thm)],[])).
% 11.80/12.01 tff(70,plain,
% 11.80/12.01 (((~ssList(nil)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(nil, V)) | (~((~ssList(tptp_fun_W_5(V, nil))) | (~(app(V, tptp_fun_W_5(V, nil)) = nil)))))) | (~(frontsegP(nil, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = nil))))))))) <=> ((~ssList(nil)) | ![V: $i] : ((~ssList(V)) | (~((~(frontsegP(nil, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = nil))))) | (~((~frontsegP(nil, V)) | (~((~ssList(tptp_fun_W_5(V, nil))) | (~(app(V, tptp_fun_W_5(V, nil)) = nil))))))))))),
% 11.80/12.01 inference(rewrite,[status(thm)],[])).
% 11.80/12.01 tff(71,plain,
% 11.80/12.01 (((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U)))))))))) | ((~ssList(nil)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(nil, V)) | (~((~ssList(tptp_fun_W_5(V, nil))) | (~(app(V, tptp_fun_W_5(V, nil)) = nil)))))) | (~(frontsegP(nil, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = nil)))))))))) <=> ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U)))))))))) | ((~ssList(nil)) | ![V: $i] : ((~ssList(V)) | (~((~(frontsegP(nil, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = nil))))) | (~((~frontsegP(nil, V)) | (~((~ssList(tptp_fun_W_5(V, nil))) | (~(app(V, tptp_fun_W_5(V, nil)) = nil)))))))))))),
% 11.80/12.01 inference(monotonicity,[status(thm)],[70])).
% 11.80/12.01 tff(72,plain,
% 11.80/12.01 (((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U)))))))))) | ((~ssList(nil)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(nil, V)) | (~((~ssList(tptp_fun_W_5(V, nil))) | (~(app(V, tptp_fun_W_5(V, nil)) = nil)))))) | (~(frontsegP(nil, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = nil)))))))))) <=> ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U)))))))))) | (~ssList(nil)) | ![V: $i] : ((~ssList(V)) | (~((~(frontsegP(nil, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = nil))))) | (~((~frontsegP(nil, V)) | (~((~ssList(tptp_fun_W_5(V, nil))) | (~(app(V, tptp_fun_W_5(V, nil)) = nil))))))))))),
% 11.80/12.02 inference(transitivity,[status(thm)],[71, 69])).
% 11.80/12.02 tff(73,plain,
% 11.80/12.02 ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U)))))))))) | ((~ssList(nil)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(nil, V)) | (~((~ssList(tptp_fun_W_5(V, nil))) | (~(app(V, tptp_fun_W_5(V, nil)) = nil)))))) | (~(frontsegP(nil, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = nil)))))))))),
% 11.80/12.02 inference(quant_inst,[status(thm)],[])).
% 11.80/12.02 tff(74,plain,
% 11.80/12.02 ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~((~((~frontsegP(U, V)) | (~((~ssList(tptp_fun_W_5(V, U))) | (~(app(V, tptp_fun_W_5(V, U)) = U)))))) | (~(frontsegP(U, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = U)))))))))) | (~ssList(nil)) | ![V: $i] : ((~ssList(V)) | (~((~(frontsegP(nil, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = nil))))) | (~((~frontsegP(nil, V)) | (~((~ssList(tptp_fun_W_5(V, nil))) | (~(app(V, tptp_fun_W_5(V, nil)) = nil)))))))))),
% 11.80/12.02 inference(modus_ponens,[status(thm)],[73, 72])).
% 11.80/12.02 tff(75,plain,
% 11.80/12.02 (![V: $i] : ((~ssList(V)) | (~((~(frontsegP(nil, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = nil))))) | (~((~frontsegP(nil, V)) | (~((~ssList(tptp_fun_W_5(V, nil))) | (~(app(V, tptp_fun_W_5(V, nil)) = nil)))))))))),
% 11.80/12.02 inference(unit_resolution,[status(thm)],[74, 68, 52])).
% 11.80/12.02 tff(76,plain,
% 11.80/12.02 (((~![V: $i] : ((~ssList(V)) | (~((~(frontsegP(nil, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = nil))))) | (~((~frontsegP(nil, V)) | (~((~ssList(tptp_fun_W_5(V, nil))) | (~(app(V, tptp_fun_W_5(V, nil)) = nil)))))))))) | ((~ssList(app(Z!47, U!45))) | (~((~(frontsegP(nil, app(Z!47, U!45)) | ![W: $i] : ((~ssList(W)) | (~(app(app(Z!47, U!45), W) = nil))))) | (~((~frontsegP(nil, app(Z!47, U!45))) | (~((~ssList(tptp_fun_W_5(app(Z!47, U!45), nil))) | (~(app(app(Z!47, U!45), tptp_fun_W_5(app(Z!47, U!45), nil)) = nil)))))))))) <=> ((~![V: $i] : ((~ssList(V)) | (~((~(frontsegP(nil, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = nil))))) | (~((~frontsegP(nil, V)) | (~((~ssList(tptp_fun_W_5(V, nil))) | (~(app(V, tptp_fun_W_5(V, nil)) = nil)))))))))) | (~ssList(app(Z!47, U!45))) | (~((~(frontsegP(nil, app(Z!47, U!45)) | ![W: $i] : ((~ssList(W)) | (~(app(app(Z!47, U!45), W) = nil))))) | (~((~frontsegP(nil, app(Z!47, U!45))) | (~((~ssList(tptp_fun_W_5(app(Z!47, U!45), nil))) | (~(app(app(Z!47, U!45), tptp_fun_W_5(app(Z!47, U!45), nil)) = nil)))))))))),
% 11.80/12.02 inference(rewrite,[status(thm)],[])).
% 11.80/12.02 tff(77,plain,
% 11.80/12.02 ((~![V: $i] : ((~ssList(V)) | (~((~(frontsegP(nil, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = nil))))) | (~((~frontsegP(nil, V)) | (~((~ssList(tptp_fun_W_5(V, nil))) | (~(app(V, tptp_fun_W_5(V, nil)) = nil)))))))))) | ((~ssList(app(Z!47, U!45))) | (~((~(frontsegP(nil, app(Z!47, U!45)) | ![W: $i] : ((~ssList(W)) | (~(app(app(Z!47, U!45), W) = nil))))) | (~((~frontsegP(nil, app(Z!47, U!45))) | (~((~ssList(tptp_fun_W_5(app(Z!47, U!45), nil))) | (~(app(app(Z!47, U!45), tptp_fun_W_5(app(Z!47, U!45), nil)) = nil)))))))))),
% 11.80/12.02 inference(quant_inst,[status(thm)],[])).
% 11.80/12.02 tff(78,plain,
% 11.80/12.02 ((~![V: $i] : ((~ssList(V)) | (~((~(frontsegP(nil, V) | ![W: $i] : ((~ssList(W)) | (~(app(V, W) = nil))))) | (~((~frontsegP(nil, V)) | (~((~ssList(tptp_fun_W_5(V, nil))) | (~(app(V, tptp_fun_W_5(V, nil)) = nil)))))))))) | (~ssList(app(Z!47, U!45))) | (~((~(frontsegP(nil, app(Z!47, U!45)) | ![W: $i] : ((~ssList(W)) | (~(app(app(Z!47, U!45), W) = nil))))) | (~((~frontsegP(nil, app(Z!47, U!45))) | (~((~ssList(tptp_fun_W_5(app(Z!47, U!45), nil))) | (~(app(app(Z!47, U!45), tptp_fun_W_5(app(Z!47, U!45), nil)) = nil))))))))),
% 11.80/12.02 inference(modus_ponens,[status(thm)],[77, 76])).
% 11.80/12.02 tff(79,plain,
% 11.80/12.02 (~((~(frontsegP(nil, app(Z!47, U!45)) | ![W: $i] : ((~ssList(W)) | (~(app(app(Z!47, U!45), W) = nil))))) | (~((~frontsegP(nil, app(Z!47, U!45))) | (~((~ssList(tptp_fun_W_5(app(Z!47, U!45), nil))) | (~(app(app(Z!47, U!45), tptp_fun_W_5(app(Z!47, U!45), nil)) = nil)))))))),
% 11.80/12.02 inference(unit_resolution,[status(thm)],[78, 75, 49])).
% 11.80/12.02 tff(80,plain,
% 11.80/12.02 (((~(frontsegP(nil, app(Z!47, U!45)) | ![W: $i] : ((~ssList(W)) | (~(app(app(Z!47, U!45), W) = nil))))) | (~((~frontsegP(nil, app(Z!47, U!45))) | (~((~ssList(tptp_fun_W_5(app(Z!47, U!45), nil))) | (~(app(app(Z!47, U!45), tptp_fun_W_5(app(Z!47, U!45), nil)) = nil))))))) | (frontsegP(nil, app(Z!47, U!45)) | ![W: $i] : ((~ssList(W)) | (~(app(app(Z!47, U!45), W) = nil))))),
% 11.80/12.02 inference(tautology,[status(thm)],[])).
% 11.80/12.02 tff(81,plain,
% 11.80/12.02 (frontsegP(nil, app(Z!47, U!45)) | ![W: $i] : ((~ssList(W)) | (~(app(app(Z!47, U!45), W) = nil)))),
% 11.80/12.02 inference(unit_resolution,[status(thm)],[80, 79])).
% 11.80/12.02 tff(82,plain,
% 11.80/12.02 (^[U: $i] : refl(((~ssList(U)) | (frontsegP(nil, U) <=> (nil = U))) <=> ((~ssList(U)) | (frontsegP(nil, U) <=> (nil = U))))),
% 11.80/12.02 inference(bind,[status(th)],[])).
% 11.80/12.02 tff(83,plain,
% 11.80/12.02 (![U: $i] : ((~ssList(U)) | (frontsegP(nil, U) <=> (nil = U))) <=> ![U: $i] : ((~ssList(U)) | (frontsegP(nil, U) <=> (nil = U)))),
% 11.80/12.02 inference(quant_intro,[status(thm)],[82])).
% 11.80/12.02 tff(84,plain,
% 11.80/12.02 (![U: $i] : ((~ssList(U)) | (frontsegP(nil, U) <=> (nil = U))) <=> ![U: $i] : ((~ssList(U)) | (frontsegP(nil, U) <=> (nil = U)))),
% 11.80/12.02 inference(rewrite,[status(thm)],[])).
% 11.80/12.02 tff(85,plain,
% 11.80/12.02 (^[U: $i] : rewrite((ssList(U) => (frontsegP(nil, U) <=> (nil = U))) <=> ((~ssList(U)) | (frontsegP(nil, U) <=> (nil = U))))),
% 11.80/12.02 inference(bind,[status(th)],[])).
% 11.80/12.02 tff(86,plain,
% 11.80/12.02 (![U: $i] : (ssList(U) => (frontsegP(nil, U) <=> (nil = U))) <=> ![U: $i] : ((~ssList(U)) | (frontsegP(nil, U) <=> (nil = U)))),
% 11.80/12.02 inference(quant_intro,[status(thm)],[85])).
% 11.80/12.02 tff(87,axiom,(![U: $i] : (ssList(U) => (frontsegP(nil, U) <=> (nil = U)))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax','ax46')).
% 11.80/12.02 tff(88,plain,
% 11.80/12.02 (![U: $i] : ((~ssList(U)) | (frontsegP(nil, U) <=> (nil = U)))),
% 11.80/12.02 inference(modus_ponens,[status(thm)],[87, 86])).
% 11.80/12.02 tff(89,plain,
% 11.80/12.02 (![U: $i] : ((~ssList(U)) | (frontsegP(nil, U) <=> (nil = U)))),
% 11.80/12.02 inference(modus_ponens,[status(thm)],[88, 84])).
% 11.80/12.02 tff(90,plain,(
% 11.80/12.02 ![U: $i] : ((~ssList(U)) | (frontsegP(nil, U) <=> (nil = U)))),
% 11.80/12.02 inference(skolemize,[status(sab)],[89])).
% 11.80/12.02 tff(91,plain,
% 11.80/12.02 (![U: $i] : ((~ssList(U)) | (frontsegP(nil, U) <=> (nil = U)))),
% 11.80/12.02 inference(modus_ponens,[status(thm)],[90, 83])).
% 11.80/12.02 tff(92,plain,
% 11.80/12.02 (((~![U: $i] : ((~ssList(U)) | (frontsegP(nil, U) <=> (nil = U)))) | ((~ssList(app(Z!47, U!45))) | (frontsegP(nil, app(Z!47, U!45)) <=> (nil = app(Z!47, U!45))))) <=> ((~![U: $i] : ((~ssList(U)) | (frontsegP(nil, U) <=> (nil = U)))) | (~ssList(app(Z!47, U!45))) | (frontsegP(nil, app(Z!47, U!45)) <=> (nil = app(Z!47, U!45))))),
% 11.80/12.02 inference(rewrite,[status(thm)],[])).
% 11.80/12.02 tff(93,plain,
% 11.80/12.02 ((~![U: $i] : ((~ssList(U)) | (frontsegP(nil, U) <=> (nil = U)))) | ((~ssList(app(Z!47, U!45))) | (frontsegP(nil, app(Z!47, U!45)) <=> (nil = app(Z!47, U!45))))),
% 11.80/12.02 inference(quant_inst,[status(thm)],[])).
% 11.80/12.02 tff(94,plain,
% 11.80/12.02 ((~![U: $i] : ((~ssList(U)) | (frontsegP(nil, U) <=> (nil = U)))) | (~ssList(app(Z!47, U!45))) | (frontsegP(nil, app(Z!47, U!45)) <=> (nil = app(Z!47, U!45)))),
% 11.80/12.02 inference(modus_ponens,[status(thm)],[93, 92])).
% 11.80/12.02 tff(95,plain,
% 11.80/12.02 (frontsegP(nil, app(Z!47, U!45)) <=> (nil = app(Z!47, U!45))),
% 11.80/12.02 inference(unit_resolution,[status(thm)],[94, 91, 49])).
% 11.80/12.02 tff(96,plain,
% 11.80/12.02 (^[U: $i] : refl(((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~(((~(nil = V)) | (~(nil = U))) <=> (nil = app(U, V)))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~(((~(nil = V)) | (~(nil = U))) <=> (nil = app(U, V)))))))),
% 11.80/12.02 inference(bind,[status(th)],[])).
% 11.80/12.02 tff(97,plain,
% 11.80/12.02 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~(((~(nil = V)) | (~(nil = U))) <=> (nil = app(U, V)))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~(((~(nil = V)) | (~(nil = U))) <=> (nil = app(U, V))))))),
% 11.80/12.02 inference(quant_intro,[status(thm)],[96])).
% 11.80/12.02 tff(98,plain,
% 11.80/12.02 (^[U: $i] : rewrite(((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~(((~(nil = V)) | (~(nil = U))) <=> (nil = app(U, V)))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~(((~(nil = V)) | (~(nil = U))) <=> (nil = app(U, V)))))))),
% 11.80/12.02 inference(bind,[status(th)],[])).
% 11.80/12.02 tff(99,plain,
% 11.80/12.02 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~(((~(nil = V)) | (~(nil = U))) <=> (nil = app(U, V)))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~(((~(nil = V)) | (~(nil = U))) <=> (nil = app(U, V))))))),
% 11.80/12.02 inference(quant_intro,[status(thm)],[98])).
% 11.80/12.02 tff(100,plain,
% 11.80/12.02 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~(((~(nil = V)) | (~(nil = U))) <=> (nil = app(U, V)))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~(((~(nil = V)) | (~(nil = U))) <=> (nil = app(U, V))))))),
% 11.80/12.02 inference(transitivity,[status(thm)],[99, 97])).
% 11.80/12.02 tff(101,plain,
% 11.80/12.02 (^[U: $i] : rewrite(((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ((nil = app(U, V)) <=> ((nil = V) & (nil = U))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~(((~(nil = V)) | (~(nil = U))) <=> (nil = app(U, V)))))))),
% 11.80/12.02 inference(bind,[status(th)],[])).
% 11.80/12.02 tff(102,plain,
% 11.80/12.02 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ((nil = app(U, V)) <=> ((nil = V) & (nil = U))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~(((~(nil = V)) | (~(nil = U))) <=> (nil = app(U, V))))))),
% 11.80/12.02 inference(quant_intro,[status(thm)],[101])).
% 11.80/12.02 tff(103,plain,
% 11.80/12.02 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ((nil = app(U, V)) <=> ((nil = V) & (nil = U))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ((nil = app(U, V)) <=> ((nil = V) & (nil = U)))))),
% 11.80/12.02 inference(rewrite,[status(thm)],[])).
% 11.80/12.02 tff(104,plain,
% 11.80/12.02 (^[U: $i] : trans(monotonicity(quant_intro(proof_bind(^[V: $i] : rewrite((ssList(V) => ((nil = app(U, V)) <=> ((nil = V) & (nil = U)))) <=> ((~ssList(V)) | ((nil = app(U, V)) <=> ((nil = V) & (nil = U)))))), (![V: $i] : (ssList(V) => ((nil = app(U, V)) <=> ((nil = V) & (nil = U)))) <=> ![V: $i] : ((~ssList(V)) | ((nil = app(U, V)) <=> ((nil = V) & (nil = U)))))), ((ssList(U) => ![V: $i] : (ssList(V) => ((nil = app(U, V)) <=> ((nil = V) & (nil = U))))) <=> (ssList(U) => ![V: $i] : ((~ssList(V)) | ((nil = app(U, V)) <=> ((nil = V) & (nil = U))))))), rewrite((ssList(U) => ![V: $i] : ((~ssList(V)) | ((nil = app(U, V)) <=> ((nil = V) & (nil = U))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ((nil = app(U, V)) <=> ((nil = V) & (nil = U)))))), ((ssList(U) => ![V: $i] : (ssList(V) => ((nil = app(U, V)) <=> ((nil = V) & (nil = U))))) <=> ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ((nil = app(U, V)) <=> ((nil = V) & (nil = U)))))))),
% 11.80/12.02 inference(bind,[status(th)],[])).
% 11.80/12.02 tff(105,plain,
% 11.80/12.02 (![U: $i] : (ssList(U) => ![V: $i] : (ssList(V) => ((nil = app(U, V)) <=> ((nil = V) & (nil = U))))) <=> ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ((nil = app(U, V)) <=> ((nil = V) & (nil = U)))))),
% 11.80/12.02 inference(quant_intro,[status(thm)],[104])).
% 11.80/12.02 tff(106,axiom,(![U: $i] : (ssList(U) => ![V: $i] : (ssList(V) => ((nil = app(U, V)) <=> ((nil = V) & (nil = U)))))), file('/export/starexec/sandbox2/benchmark/Axioms/SWC001+0.ax','ax83')).
% 11.80/12.02 tff(107,plain,
% 11.80/12.02 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ((nil = app(U, V)) <=> ((nil = V) & (nil = U)))))),
% 11.80/12.02 inference(modus_ponens,[status(thm)],[106, 105])).
% 11.80/12.02 tff(108,plain,
% 11.80/12.02 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ((nil = app(U, V)) <=> ((nil = V) & (nil = U)))))),
% 11.80/12.02 inference(modus_ponens,[status(thm)],[107, 103])).
% 11.80/12.02 tff(109,plain,(
% 11.80/12.02 ![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | ((nil = app(U, V)) <=> ((nil = V) & (nil = U)))))),
% 11.80/12.02 inference(skolemize,[status(sab)],[108])).
% 11.80/12.02 tff(110,plain,
% 11.80/12.02 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~(((~(nil = V)) | (~(nil = U))) <=> (nil = app(U, V))))))),
% 11.80/12.02 inference(modus_ponens,[status(thm)],[109, 102])).
% 11.80/12.02 tff(111,plain,
% 11.80/12.02 (![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~(((~(nil = V)) | (~(nil = U))) <=> (nil = app(U, V))))))),
% 11.80/12.02 inference(modus_ponens,[status(thm)],[110, 100])).
% 11.80/12.02 tff(112,plain,
% 11.80/12.02 (((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~(((~(nil = V)) | (~(nil = U))) <=> (nil = app(U, V))))))) | ((~ssList(Z!47)) | ![V: $i] : ((~ssList(V)) | (~(((~(nil = V)) | (~(nil = Z!47))) <=> (nil = app(Z!47, V))))))) <=> ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~(((~(nil = V)) | (~(nil = U))) <=> (nil = app(U, V))))))) | (~ssList(Z!47)) | ![V: $i] : ((~ssList(V)) | (~(((~(nil = V)) | (~(nil = Z!47))) <=> (nil = app(Z!47, V))))))),
% 11.80/12.02 inference(rewrite,[status(thm)],[])).
% 11.80/12.02 tff(113,plain,
% 11.80/12.02 ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~(((~(nil = V)) | (~(nil = U))) <=> (nil = app(U, V))))))) | ((~ssList(Z!47)) | ![V: $i] : ((~ssList(V)) | (~(((~(nil = V)) | (~(nil = Z!47))) <=> (nil = app(Z!47, V))))))),
% 11.80/12.02 inference(quant_inst,[status(thm)],[])).
% 11.80/12.02 tff(114,plain,
% 11.80/12.02 ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~(((~(nil = V)) | (~(nil = U))) <=> (nil = app(U, V))))))) | (~ssList(Z!47)) | ![V: $i] : ((~ssList(V)) | (~(((~(nil = V)) | (~(nil = Z!47))) <=> (nil = app(Z!47, V)))))),
% 11.80/12.02 inference(modus_ponens,[status(thm)],[113, 112])).
% 11.80/12.02 tff(115,plain,
% 11.80/12.02 (![V: $i] : ((~ssList(V)) | (~(((~(nil = V)) | (~(nil = Z!47))) <=> (nil = app(Z!47, V)))))),
% 11.80/12.02 inference(unit_resolution,[status(thm)],[114, 111, 27])).
% 11.80/12.02 tff(116,plain,
% 11.80/12.02 (((~![V: $i] : ((~ssList(V)) | (~(((~(nil = V)) | (~(nil = Z!47))) <=> (nil = app(Z!47, V)))))) | ((~ssList(U!45)) | (~(((~(nil = U!45)) | (~(nil = Z!47))) <=> (nil = app(Z!47, U!45)))))) <=> ((~![V: $i] : ((~ssList(V)) | (~(((~(nil = V)) | (~(nil = Z!47))) <=> (nil = app(Z!47, V)))))) | (~ssList(U!45)) | (~(((~(nil = U!45)) | (~(nil = Z!47))) <=> (nil = app(Z!47, U!45)))))),
% 11.80/12.02 inference(rewrite,[status(thm)],[])).
% 11.80/12.02 tff(117,plain,
% 11.80/12.02 ((~![V: $i] : ((~ssList(V)) | (~(((~(nil = V)) | (~(nil = Z!47))) <=> (nil = app(Z!47, V)))))) | ((~ssList(U!45)) | (~(((~(nil = U!45)) | (~(nil = Z!47))) <=> (nil = app(Z!47, U!45)))))),
% 11.80/12.02 inference(quant_inst,[status(thm)],[])).
% 11.80/12.02 tff(118,plain,
% 11.80/12.02 ((~![V: $i] : ((~ssList(V)) | (~(((~(nil = V)) | (~(nil = Z!47))) <=> (nil = app(Z!47, V)))))) | (~ssList(U!45)) | (~(((~(nil = U!45)) | (~(nil = Z!47))) <=> (nil = app(Z!47, U!45))))),
% 11.80/12.02 inference(modus_ponens,[status(thm)],[117, 116])).
% 11.80/12.02 tff(119,plain,
% 11.80/12.02 (~(((~(nil = U!45)) | (~(nil = Z!47))) <=> (nil = app(Z!47, U!45)))),
% 11.80/12.02 inference(unit_resolution,[status(thm)],[118, 45, 115])).
% 11.80/12.02 tff(120,plain,
% 11.80/12.02 (((~(nil = U!45)) | (~(nil = Z!47))) | (nil = U!45)),
% 11.80/12.02 inference(tautology,[status(thm)],[])).
% 11.80/12.02 tff(121,plain,
% 11.80/12.02 ((~(nil = U!45)) | (~(nil = Z!47))),
% 11.80/12.02 inference(unit_resolution,[status(thm)],[120, 10])).
% 11.80/12.02 tff(122,plain,
% 11.80/12.02 ((((~(nil = U!45)) | (~(nil = Z!47))) <=> (nil = app(Z!47, U!45))) | (~((~(nil = U!45)) | (~(nil = Z!47)))) | (~(nil = app(Z!47, U!45)))),
% 11.80/12.02 inference(tautology,[status(thm)],[])).
% 11.80/12.02 tff(123,plain,
% 11.80/12.02 ((((~(nil = U!45)) | (~(nil = Z!47))) <=> (nil = app(Z!47, U!45))) | (~(nil = app(Z!47, U!45)))),
% 11.80/12.02 inference(unit_resolution,[status(thm)],[122, 121])).
% 11.80/12.02 tff(124,plain,
% 11.80/12.02 (~(nil = app(Z!47, U!45))),
% 11.80/12.02 inference(unit_resolution,[status(thm)],[123, 119])).
% 11.80/12.02 tff(125,plain,
% 11.80/12.02 ((~(frontsegP(nil, app(Z!47, U!45)) <=> (nil = app(Z!47, U!45)))) | (~frontsegP(nil, app(Z!47, U!45))) | (nil = app(Z!47, U!45))),
% 11.80/12.02 inference(tautology,[status(thm)],[])).
% 11.80/12.02 tff(126,plain,
% 11.80/12.02 ((~(frontsegP(nil, app(Z!47, U!45)) <=> (nil = app(Z!47, U!45)))) | (~frontsegP(nil, app(Z!47, U!45)))),
% 11.80/12.02 inference(unit_resolution,[status(thm)],[125, 124])).
% 11.80/12.02 tff(127,plain,
% 11.80/12.02 (~frontsegP(nil, app(Z!47, U!45))),
% 11.80/12.02 inference(unit_resolution,[status(thm)],[126, 95])).
% 11.80/12.02 tff(128,plain,
% 11.80/12.02 ((~(frontsegP(nil, app(Z!47, U!45)) | ![W: $i] : ((~ssList(W)) | (~(app(app(Z!47, U!45), W) = nil))))) | frontsegP(nil, app(Z!47, U!45)) | ![W: $i] : ((~ssList(W)) | (~(app(app(Z!47, U!45), W) = nil)))),
% 11.88/12.05 inference(tautology,[status(thm)],[])).
% 11.88/12.05 tff(129,plain,
% 11.88/12.05 (![W: $i] : ((~ssList(W)) | (~(app(app(Z!47, U!45), W) = nil)))),
% 11.88/12.05 inference(unit_resolution,[status(thm)],[128, 127, 81])).
% 11.88/12.05 tff(130,plain,
% 11.88/12.05 (((~(cons(Y!46, nil) = U!45)) | (~ssItem(Y!46)) | (~ssList(Z!47)) | (~(app(app(Z!47, U!45), X1!48) = nil)) | (~ssList(X1!48)) | (~![X2: $i] : ((~ssItem(X2)) | (~memberP(Z!47, X2)) | (~lt(Y!46, X2)))) | (~![X3: $i] : ((~ssItem(X3)) | (~memberP(X1!48, X3)) | (~lt(X3, Y!46))))) | ssList(X1!48)),
% 11.88/12.05 inference(tautology,[status(thm)],[])).
% 11.88/12.05 tff(131,plain,
% 11.88/12.05 (ssList(X1!48)),
% 11.88/12.05 inference(unit_resolution,[status(thm)],[130, 25])).
% 11.88/12.05 tff(132,plain,
% 11.88/12.05 (((~(cons(Y!46, nil) = U!45)) | (~ssItem(Y!46)) | (~ssList(Z!47)) | (~(app(app(Z!47, U!45), X1!48) = nil)) | (~ssList(X1!48)) | (~![X2: $i] : ((~ssItem(X2)) | (~memberP(Z!47, X2)) | (~lt(Y!46, X2)))) | (~![X3: $i] : ((~ssItem(X3)) | (~memberP(X1!48, X3)) | (~lt(X3, Y!46))))) | (app(app(Z!47, U!45), X1!48) = nil)),
% 11.88/12.05 inference(tautology,[status(thm)],[])).
% 11.88/12.05 tff(133,plain,
% 11.88/12.05 (app(app(Z!47, U!45), X1!48) = nil),
% 11.88/12.05 inference(unit_resolution,[status(thm)],[132, 25])).
% 11.88/12.05 tff(134,plain,
% 11.88/12.05 (((~![W: $i] : ((~ssList(W)) | (~(app(app(Z!47, U!45), W) = nil)))) | ((~ssList(X1!48)) | (~(app(app(Z!47, U!45), X1!48) = nil)))) <=> ((~![W: $i] : ((~ssList(W)) | (~(app(app(Z!47, U!45), W) = nil)))) | (~ssList(X1!48)) | (~(app(app(Z!47, U!45), X1!48) = nil)))),
% 11.88/12.05 inference(rewrite,[status(thm)],[])).
% 11.88/12.05 tff(135,plain,
% 11.88/12.05 ((~![W: $i] : ((~ssList(W)) | (~(app(app(Z!47, U!45), W) = nil)))) | ((~ssList(X1!48)) | (~(app(app(Z!47, U!45), X1!48) = nil)))),
% 11.88/12.05 inference(quant_inst,[status(thm)],[])).
% 11.88/12.05 tff(136,plain,
% 11.88/12.05 ((~![W: $i] : ((~ssList(W)) | (~(app(app(Z!47, U!45), W) = nil)))) | (~ssList(X1!48)) | (~(app(app(Z!47, U!45), X1!48) = nil))),
% 11.88/12.05 inference(modus_ponens,[status(thm)],[135, 134])).
% 11.88/12.05 tff(137,plain,
% 11.88/12.05 ($false),
% 11.88/12.05 inference(unit_resolution,[status(thm)],[136, 133, 131, 129])).
% 11.88/12.05 % SZS output end Proof
% 11.88/12.06 % E exiting
%------------------------------------------------------------------------------