%------------------------------------------------------------------------------
% File : Z3---4.15.1
% Problem : SWC002+1 : TPTP v9.0.0. Released v2.4.0.
% Transfm : none
% Format : tptp
% Command : run_E %s %d THM
% Computer : n010.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:29:53 AM UTC 2025
% Result : Theorem 22.08s 22.26s
% Output : Proof 22.16s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : SWC002+1 : TPTP v9.0.0. Released v2.4.0.
% 0.12/0.12 % Command : run_E %s %d THM
% 0.12/0.33 % Computer : n010.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:00:42 EDT 2025
% 0.12/0.34 % CPUTime :
% 22.08/22.26 % SZS status Theorem
% 22.08/22.26 % SZS output start Proof
% 22.08/22.26 tff(memberP_type, type, (
% 22.08/22.26 memberP: ( $i * $i ) > $o)).
% 22.08/22.26 tff(tptp_fun_X2_50_type, type, (
% 22.08/22.26 tptp_fun_X2_50: $i > $i)).
% 22.08/22.26 tff(tptp_fun_X3_47_type, type, (
% 22.08/22.26 tptp_fun_X3_47: $i)).
% 22.08/22.26 tff(tptp_fun_V_46_type, type, (
% 22.08/22.26 tptp_fun_V_46: $i)).
% 22.08/22.26 tff(geq_type, type, (
% 22.08/22.26 geq: ( $i * $i ) > $o)).
% 22.08/22.26 tff(ssItem_type, type, (
% 22.08/22.26 ssItem: $i > $o)).
% 22.08/22.26 tff(app_type, type, (
% 22.08/22.26 app: ( $i * $i ) > $i)).
% 22.08/22.26 tff(cons_type, type, (
% 22.08/22.26 cons: ( $i * $i ) > $i)).
% 22.08/22.26 tff(nil_type, type, (
% 22.08/22.26 nil: $i)).
% 22.08/22.26 tff(tptp_fun_X4_48_type, type, (
% 22.08/22.26 tptp_fun_X4_48: $i)).
% 22.08/22.26 tff(tptp_fun_U_45_type, type, (
% 22.08/22.26 tptp_fun_U_45: $i)).
% 22.08/22.26 tff(ssList_type, type, (
% 22.08/22.26 ssList: $i > $o)).
% 22.08/22.26 tff(neq_type, type, (
% 22.08/22.26 neq: ( $i * $i ) > $o)).
% 22.08/22.26 tff(tptp_fun_X5_49_type, type, (
% 22.08/22.26 tptp_fun_X5_49: $i)).
% 22.08/22.26 tff(1,plain,
% 22.08/22.26 (^[Y: $i] : refl(((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y)))))))) <=> ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y)))))))))),
% 22.08/22.26 inference(bind,[status(th)],[])).
% 22.08/22.26 tff(2,plain,
% 22.08/22.26 (![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y)))))))) <=> ![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y))))))))),
% 22.08/22.26 inference(quant_intro,[status(thm)],[1])).
% 22.08/22.26 tff(3,plain,
% 22.08/22.26 (^[Y: $i] : rewrite(((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y)))))))) <=> ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y)))))))))),
% 22.08/22.26 inference(bind,[status(th)],[])).
% 22.08/22.26 tff(4,plain,
% 22.08/22.26 (![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y)))))))) <=> ![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y))))))))),
% 22.08/22.26 inference(quant_intro,[status(thm)],[3])).
% 22.08/22.26 tff(5,plain,
% 22.08/22.26 (![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y)))))))) <=> ![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y))))))))),
% 22.08/22.26 inference(transitivity,[status(thm)],[4, 2])).
% 22.08/22.26 tff(6,plain,
% 22.08/22.26 ((ssList(U!45) & (ssList(V!46) & ssList(U!45) & ssItem(X3!47) & ssList(X4!48) & (app(X4!48, X5!49) = U!45) & (app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46) & ssList(X5!49) & ![X6: $i] : (~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47))) & ![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y)))))))) & neq(V!46, nil))) <=> (ssList(U!45) & ssList(V!46) & ssItem(X3!47) & ssList(X4!48) & (app(X4!48, X5!49) = U!45) & (app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46) & ssList(X5!49) & ![X6: $i] : (~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47))) & ![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y)))))))) & neq(V!46, nil))),
% 22.08/22.26 inference(rewrite,[status(thm)],[])).
% 22.08/22.26 tff(7,plain,
% 22.08/22.26 ((ssList(V!46) & ssList(U!45) & (ssItem(X3!47) & ssList(X4!48) & (app(X4!48, X5!49) = U!45) & (app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46) & ssList(X5!49) & ![X6: $i] : (~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47)))) & ![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y)))))))) & neq(V!46, nil)) <=> (ssList(V!46) & ssList(U!45) & ssItem(X3!47) & ssList(X4!48) & (app(X4!48, X5!49) = U!45) & (app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46) & ssList(X5!49) & ![X6: $i] : (~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47))) & ![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y)))))))) & neq(V!46, nil))),
% 22.08/22.26 inference(rewrite,[status(thm)],[])).
% 22.08/22.26 tff(8,plain,
% 22.08/22.26 (^[Y: $i] : rewrite(((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~(app(Z, X1) = U!45)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y)))))))) <=> ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y)))))))))),
% 22.08/22.26 inference(bind,[status(th)],[])).
% 22.08/22.26 tff(9,plain,
% 22.08/22.26 (![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~(app(Z, X1) = U!45)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y)))))))) <=> ![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y))))))))),
% 22.08/22.26 inference(quant_intro,[status(thm)],[8])).
% 22.08/22.26 tff(10,plain,
% 22.08/22.26 ((ssItem(X3!47) & (ssList(X4!48) & (app(X4!48, X5!49) = U!45) & (app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46) & ssList(X5!49) & ![X6: $i] : (~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47))))) <=> (ssItem(X3!47) & ssList(X4!48) & (app(X4!48, X5!49) = U!45) & (app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46) & ssList(X5!49) & ![X6: $i] : (~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47))))),
% 22.08/22.26 inference(rewrite,[status(thm)],[])).
% 22.08/22.26 tff(11,plain,
% 22.08/22.26 ((ssList(X4!48) & ((app(X4!48, X5!49) = U!45) & (app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46) & ssList(X5!49) & ![X6: $i] : (~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47))))) <=> (ssList(X4!48) & (app(X4!48, X5!49) = U!45) & (app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46) & ssList(X5!49) & ![X6: $i] : (~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47))))),
% 22.08/22.26 inference(rewrite,[status(thm)],[])).
% 22.08/22.26 tff(12,plain,
% 22.08/22.26 (((app(X4!48, X5!49) = U!45) & (app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46) & ssList(X5!49) & ![X6: $i] : (~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47)))) <=> ((app(X4!48, X5!49) = U!45) & (app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46) & ssList(X5!49) & ![X6: $i] : (~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47))))),
% 22.08/22.26 inference(rewrite,[status(thm)],[])).
% 22.08/22.26 tff(13,plain,
% 22.08/22.26 ((ssList(X4!48) & ((app(X4!48, X5!49) = U!45) & (app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46) & ssList(X5!49) & ![X6: $i] : (~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47))))) <=> (ssList(X4!48) & ((app(X4!48, X5!49) = U!45) & (app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46) & ssList(X5!49) & ![X6: $i] : (~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47)))))),
% 22.08/22.26 inference(monotonicity,[status(thm)],[12])).
% 22.08/22.26 tff(14,plain,
% 22.08/22.26 ((ssList(X4!48) & ((app(X4!48, X5!49) = U!45) & (app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46) & ssList(X5!49) & ![X6: $i] : (~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47))))) <=> (ssList(X4!48) & (app(X4!48, X5!49) = U!45) & (app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46) & ssList(X5!49) & ![X6: $i] : (~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47))))),
% 22.08/22.26 inference(transitivity,[status(thm)],[13, 11])).
% 22.08/22.26 tff(15,plain,
% 22.08/22.26 ((ssItem(X3!47) & (ssList(X4!48) & ((app(X4!48, X5!49) = U!45) & (app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46) & ssList(X5!49) & ![X6: $i] : (~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47)))))) <=> (ssItem(X3!47) & (ssList(X4!48) & (app(X4!48, X5!49) = U!45) & (app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46) & ssList(X5!49) & ![X6: $i] : (~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47)))))),
% 22.08/22.26 inference(monotonicity,[status(thm)],[14])).
% 22.08/22.26 tff(16,plain,
% 22.08/22.26 ((ssItem(X3!47) & (ssList(X4!48) & ((app(X4!48, X5!49) = U!45) & (app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46) & ssList(X5!49) & ![X6: $i] : (~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47)))))) <=> (ssItem(X3!47) & ssList(X4!48) & (app(X4!48, X5!49) = U!45) & (app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46) & ssList(X5!49) & ![X6: $i] : (~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47))))),
% 22.08/22.26 inference(transitivity,[status(thm)],[15, 10])).
% 22.08/22.26 tff(17,plain,
% 22.08/22.26 ((ssList(V!46) & ssList(U!45) & (ssItem(X3!47) & (ssList(X4!48) & ((app(X4!48, X5!49) = U!45) & (app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46) & ssList(X5!49) & ![X6: $i] : (~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47)))))) & ![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~(app(Z, X1) = U!45)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y)))))))) & neq(V!46, nil)) <=> (ssList(V!46) & ssList(U!45) & (ssItem(X3!47) & ssList(X4!48) & (app(X4!48, X5!49) = U!45) & (app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46) & ssList(X5!49) & ![X6: $i] : (~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47)))) & ![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y)))))))) & neq(V!46, nil))),
% 22.08/22.26 inference(monotonicity,[status(thm)],[16, 9])).
% 22.08/22.26 tff(18,plain,
% 22.08/22.26 ((ssList(V!46) & ssList(U!45) & (ssItem(X3!47) & (ssList(X4!48) & ((app(X4!48, X5!49) = U!45) & (app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46) & ssList(X5!49) & ![X6: $i] : (~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47)))))) & ![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~(app(Z, X1) = U!45)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y)))))))) & neq(V!46, nil)) <=> (ssList(V!46) & ssList(U!45) & ssItem(X3!47) & ssList(X4!48) & (app(X4!48, X5!49) = U!45) & (app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46) & ssList(X5!49) & ![X6: $i] : (~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47))) & ![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y)))))))) & neq(V!46, nil))),
% 22.08/22.26 inference(transitivity,[status(thm)],[17, 7])).
% 22.08/22.26 tff(19,plain,
% 22.08/22.26 ((ssList(U!45) & (ssList(V!46) & ssList(U!45) & (ssItem(X3!47) & (ssList(X4!48) & ((app(X4!48, X5!49) = U!45) & (app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46) & ssList(X5!49) & ![X6: $i] : (~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47)))))) & ![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~(app(Z, X1) = U!45)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y)))))))) & neq(V!46, nil))) <=> (ssList(U!45) & (ssList(V!46) & ssList(U!45) & ssItem(X3!47) & ssList(X4!48) & (app(X4!48, X5!49) = U!45) & (app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46) & ssList(X5!49) & ![X6: $i] : (~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47))) & ![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y)))))))) & neq(V!46, nil)))),
% 22.08/22.26 inference(monotonicity,[status(thm)],[18])).
% 22.08/22.26 tff(20,plain,
% 22.08/22.26 ((ssList(U!45) & (ssList(V!46) & ssList(U!45) & (ssItem(X3!47) & (ssList(X4!48) & ((app(X4!48, X5!49) = U!45) & (app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46) & ssList(X5!49) & ![X6: $i] : (~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47)))))) & ![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~(app(Z, X1) = U!45)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y)))))))) & neq(V!46, nil))) <=> (ssList(U!45) & ssList(V!46) & ssItem(X3!47) & ssList(X4!48) & (app(X4!48, X5!49) = U!45) & (app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46) & ssList(X5!49) & ![X6: $i] : (~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47))) & ![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y)))))))) & neq(V!46, nil))),
% 22.08/22.26 inference(transitivity,[status(thm)],[19, 6])).
% 22.08/22.26 tff(21,plain,
% 22.08/22.26 ((~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~ssList(U)) | ![X3: $i] : ((~ssItem(X3)) | ![X4: $i] : ((~ssList(X4)) | ![X5: $i] : ((~(app(X4, X5) = U)) | (~(app(app(X4, cons(X3, nil)), X5) = V)) | (~ssList(X5)) | ?[X6: $i] : (ssItem(X6) & (~(X3 = X6)) & memberP(V, X6) & geq(X6, X3))))) | ?[Y: $i] : (ssItem(Y) & ?[Z: $i] : (ssList(Z) & ?[X1: $i] : (ssList(X1) & (app(app(Z, cons(Y, nil)), X1) = V) & (app(Z, X1) = U) & ![X2: $i] : ((~ssItem(X2)) | (Y = X2) | (~geq(X2, Y)) | (~memberP(V, X2)))))) | (~neq(V, nil))))) <=> (~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~ssList(U)) | ![X3: $i] : ((~ssItem(X3)) | ![X4: $i] : ((~ssList(X4)) | ![X5: $i] : ((~(app(X4, X5) = U)) | (~(app(app(X4, cons(X3, nil)), X5) = V)) | (~ssList(X5)) | ?[X6: $i] : (ssItem(X6) & (~(X3 = X6)) & memberP(V, X6) & geq(X6, X3))))) | ?[Y: $i] : (ssItem(Y) & ?[Z: $i] : (ssList(Z) & ?[X1: $i] : (ssList(X1) & (app(app(Z, cons(Y, nil)), X1) = V) & (app(Z, X1) = U) & ![X2: $i] : ((~ssItem(X2)) | (Y = X2) | (~geq(X2, Y)) | (~memberP(V, X2)))))) | (~neq(V, nil)))))),
% 22.08/22.26 inference(rewrite,[status(thm)],[])).
% 22.08/22.26 tff(22,plain,
% 22.08/22.26 ((~![U: $i] : (ssList(U) => ![V: $i] : (ssList(V) => ![W: $i] : (ssList(W) => ![X: $i] : (ssList(X) => (((~(V = X)) | (~(U = W))) | ((((~neq(V, nil)) | ?[Y: $i] : (ssItem(Y) & ?[Z: $i] : (ssList(Z) & ?[X1: $i] : (((ssList(X1) & (app(app(Z, cons(Y, nil)), X1) = V)) & (app(Z, X1) = U)) & ![X2: $i] : (ssItem(X2) => (((~memberP(V, X2)) | (~geq(X2, Y))) | (Y = X2))))))) | ![X3: $i] : (ssItem(X3) => ![X4: $i] : (ssList(X4) => ![X5: $i] : (ssList(X5) => (((~(app(app(X4, cons(X3, nil)), X5) = X)) | (~(app(X4, X5) = W))) | ?[X6: $i] : (((ssItem(X6) & (~(X3 = X6))) & memberP(X, X6)) & geq(X6, X3))))))) & ((~neq(V, nil)) | neq(X, nil))))))))) <=> (~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~ssList(U)) | ![X3: $i] : ((~ssItem(X3)) | ![X4: $i] : ((~ssList(X4)) | ![X5: $i] : ((~(app(X4, X5) = U)) | (~(app(app(X4, cons(X3, nil)), X5) = V)) | (~ssList(X5)) | ?[X6: $i] : (ssItem(X6) & (~(X3 = X6)) & memberP(V, X6) & geq(X6, X3))))) | ?[Y: $i] : (ssItem(Y) & ?[Z: $i] : (ssList(Z) & ?[X1: $i] : (ssList(X1) & (app(app(Z, cons(Y, nil)), X1) = V) & (app(Z, X1) = U) & ![X2: $i] : ((~ssItem(X2)) | (Y = X2) | (~geq(X2, Y)) | (~memberP(V, X2)))))) | (~neq(V, nil)))))),
% 22.08/22.26 inference(rewrite,[status(thm)],[])).
% 22.08/22.26 tff(23,axiom,(~![U: $i] : (ssList(U) => ![V: $i] : (ssList(V) => ![W: $i] : (ssList(W) => ![X: $i] : (ssList(X) => (((~(V = X)) | (~(U = W))) | ((((~neq(V, nil)) | ?[Y: $i] : (ssItem(Y) & ?[Z: $i] : (ssList(Z) & ?[X1: $i] : (((ssList(X1) & (app(app(Z, cons(Y, nil)), X1) = V)) & (app(Z, X1) = U)) & ![X2: $i] : (ssItem(X2) => (((~memberP(V, X2)) | (~geq(X2, Y))) | (Y = X2))))))) | ![X3: $i] : (ssItem(X3) => ![X4: $i] : (ssList(X4) => ![X5: $i] : (ssList(X5) => (((~(app(app(X4, cons(X3, nil)), X5) = X)) | (~(app(X4, X5) = W))) | ?[X6: $i] : (((ssItem(X6) & (~(X3 = X6))) & memberP(X, X6)) & geq(X6, X3))))))) & ((~neq(V, nil)) | neq(X, nil))))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p','co1')).
% 22.08/22.26 tff(24,plain,
% 22.08/22.26 (~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~ssList(U)) | ![X3: $i] : ((~ssItem(X3)) | ![X4: $i] : ((~ssList(X4)) | ![X5: $i] : ((~(app(X4, X5) = U)) | (~(app(app(X4, cons(X3, nil)), X5) = V)) | (~ssList(X5)) | ?[X6: $i] : (ssItem(X6) & (~(X3 = X6)) & memberP(V, X6) & geq(X6, X3))))) | ?[Y: $i] : (ssItem(Y) & ?[Z: $i] : (ssList(Z) & ?[X1: $i] : (ssList(X1) & (app(app(Z, cons(Y, nil)), X1) = V) & (app(Z, X1) = U) & ![X2: $i] : ((~ssItem(X2)) | (Y = X2) | (~geq(X2, Y)) | (~memberP(V, X2)))))) | (~neq(V, nil))))),
% 22.08/22.26 inference(modus_ponens,[status(thm)],[23, 22])).
% 22.08/22.26 tff(25,plain,
% 22.08/22.26 (~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~ssList(U)) | ![X3: $i] : ((~ssItem(X3)) | ![X4: $i] : ((~ssList(X4)) | ![X5: $i] : ((~(app(X4, X5) = U)) | (~(app(app(X4, cons(X3, nil)), X5) = V)) | (~ssList(X5)) | ?[X6: $i] : (ssItem(X6) & (~(X3 = X6)) & memberP(V, X6) & geq(X6, X3))))) | ?[Y: $i] : (ssItem(Y) & ?[Z: $i] : (ssList(Z) & ?[X1: $i] : (ssList(X1) & (app(app(Z, cons(Y, nil)), X1) = V) & (app(Z, X1) = U) & ![X2: $i] : ((~ssItem(X2)) | (Y = X2) | (~geq(X2, Y)) | (~memberP(V, X2)))))) | (~neq(V, nil))))),
% 22.08/22.26 inference(modus_ponens,[status(thm)],[24, 21])).
% 22.08/22.26 tff(26,plain,
% 22.08/22.26 (~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~ssList(U)) | ![X3: $i] : ((~ssItem(X3)) | ![X4: $i] : ((~ssList(X4)) | ![X5: $i] : ((~(app(X4, X5) = U)) | (~(app(app(X4, cons(X3, nil)), X5) = V)) | (~ssList(X5)) | ?[X6: $i] : (ssItem(X6) & (~(X3 = X6)) & memberP(V, X6) & geq(X6, X3))))) | ?[Y: $i] : (ssItem(Y) & ?[Z: $i] : (ssList(Z) & ?[X1: $i] : (ssList(X1) & (app(app(Z, cons(Y, nil)), X1) = V) & (app(Z, X1) = U) & ![X2: $i] : ((~ssItem(X2)) | (Y = X2) | (~geq(X2, Y)) | (~memberP(V, X2)))))) | (~neq(V, nil))))),
% 22.08/22.26 inference(modus_ponens,[status(thm)],[25, 21])).
% 22.08/22.26 tff(27,plain,
% 22.08/22.26 (~![U: $i] : ((~ssList(U)) | ![V: $i] : ((~ssList(V)) | (~ssList(U)) | ![X3: $i] : ((~ssItem(X3)) | ![X4: $i] : ((~ssList(X4)) | ![X5: $i] : ((~(app(X4, X5) = U)) | (~(app(app(X4, cons(X3, nil)), X5) = V)) | (~ssList(X5)) | ?[X6: $i] : (ssItem(X6) & (~(X3 = X6)) & memberP(V, X6) & geq(X6, X3))))) | ?[Y: $i] : (ssItem(Y) & ?[Z: $i] : (ssList(Z) & ?[X1: $i] : (ssList(X1) & (app(app(Z, cons(Y, nil)), X1) = V) & (app(Z, X1) = U) & ![X2: $i] : ((~ssItem(X2)) | (Y = X2) | (~geq(X2, Y)) | (~memberP(V, X2)))))) | (~neq(V, nil))))),
% 22.08/22.26 inference(modus_ponens,[status(thm)],[26, 21])).
% 22.08/22.26 tff(28,plain,
% 22.08/22.26 (ssList(U!45) & ssList(V!46) & ssItem(X3!47) & ssList(X4!48) & (app(X4!48, X5!49) = U!45) & (app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46) & ssList(X5!49) & ![X6: $i] : (~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47))) & ![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y)))))))) & neq(V!46, nil)),
% 22.08/22.26 inference(modus_ponens,[status(thm)],[27, 20])).
% 22.08/22.26 tff(29,plain,
% 22.08/22.26 (![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y))))))))),
% 22.08/22.26 inference(and_elim,[status(thm)],[28])).
% 22.08/22.26 tff(30,plain,
% 22.08/22.26 (![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y))))))))),
% 22.08/22.26 inference(modus_ponens,[status(thm)],[29, 5])).
% 22.08/22.26 tff(31,plain,
% 22.08/22.26 (ssItem(X3!47)),
% 22.08/22.26 inference(and_elim,[status(thm)],[28])).
% 22.08/22.26 tff(32,plain,
% 22.08/22.26 (((~![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y))))))))) | ((~ssItem(X3!47)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(X3!47, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47))))))))) <=> ((~![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y))))))))) | (~ssItem(X3!47)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(X3!47, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47))))))))),
% 22.08/22.26 inference(rewrite,[status(thm)],[])).
% 22.08/22.26 tff(33,plain,
% 22.08/22.26 ((~![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y))))))))) | ((~ssItem(X3!47)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(X3!47, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47))))))))),
% 22.08/22.26 inference(quant_inst,[status(thm)],[])).
% 22.08/22.26 tff(34,plain,
% 22.08/22.26 ((~![Y: $i] : ((~ssItem(Y)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(Y, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(Y))) | (Y = tptp_fun_X2_50(Y)) | (~geq(tptp_fun_X2_50(Y), Y)) | (~memberP(V!46, tptp_fun_X2_50(Y))))))))) | (~ssItem(X3!47)) | ![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(X3!47, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47)))))))),
% 22.08/22.27 inference(modus_ponens,[status(thm)],[33, 32])).
% 22.08/22.27 tff(35,plain,
% 22.08/22.27 (![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(X3!47, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47)))))))),
% 22.08/22.27 inference(unit_resolution,[status(thm)],[34, 31, 30])).
% 22.08/22.27 tff(36,plain,
% 22.08/22.27 (ssList(X4!48)),
% 22.08/22.27 inference(and_elim,[status(thm)],[28])).
% 22.08/22.27 tff(37,plain,
% 22.08/22.27 (((~![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(X3!47, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47)))))))) | ((~ssList(X4!48)) | ![X1: $i] : ((~ssList(X1)) | (~(app(X4!48, X1) = U!45)) | (~(app(app(X4!48, cons(X3!47, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47)))))))) <=> ((~![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(X3!47, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47)))))))) | (~ssList(X4!48)) | ![X1: $i] : ((~ssList(X1)) | (~(app(X4!48, X1) = U!45)) | (~(app(app(X4!48, cons(X3!47, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47)))))))),
% 22.08/22.27 inference(rewrite,[status(thm)],[])).
% 22.08/22.27 tff(38,plain,
% 22.08/22.27 ((~![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(X3!47, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47)))))))) | ((~ssList(X4!48)) | ![X1: $i] : ((~ssList(X1)) | (~(app(X4!48, X1) = U!45)) | (~(app(app(X4!48, cons(X3!47, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47)))))))),
% 22.08/22.27 inference(quant_inst,[status(thm)],[])).
% 22.08/22.27 tff(39,plain,
% 22.08/22.27 ((~![Z: $i] : ((~ssList(Z)) | ![X1: $i] : ((~ssList(X1)) | (~(app(Z, X1) = U!45)) | (~(app(app(Z, cons(X3!47, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47)))))))) | (~ssList(X4!48)) | ![X1: $i] : ((~ssList(X1)) | (~(app(X4!48, X1) = U!45)) | (~(app(app(X4!48, cons(X3!47, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47))))))),
% 22.08/22.27 inference(modus_ponens,[status(thm)],[38, 37])).
% 22.08/22.27 tff(40,plain,
% 22.08/22.27 (![X1: $i] : ((~ssList(X1)) | (~(app(X4!48, X1) = U!45)) | (~(app(app(X4!48, cons(X3!47, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47))))))),
% 22.08/22.27 inference(unit_resolution,[status(thm)],[39, 36, 35])).
% 22.08/22.27 tff(41,plain,
% 22.08/22.27 (ssList(X5!49)),
% 22.08/22.27 inference(and_elim,[status(thm)],[28])).
% 22.08/22.27 tff(42,plain,
% 22.08/22.27 (app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46),
% 22.08/22.27 inference(and_elim,[status(thm)],[28])).
% 22.08/22.27 tff(43,plain,
% 22.08/22.27 (app(X4!48, X5!49) = U!45),
% 22.08/22.27 inference(and_elim,[status(thm)],[28])).
% 22.08/22.27 tff(44,plain,
% 22.08/22.27 (((~![X1: $i] : ((~ssList(X1)) | (~(app(X4!48, X1) = U!45)) | (~(app(app(X4!48, cons(X3!47, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47))))))) | ((~ssList(X5!49)) | (~(app(X4!48, X5!49) = U!45)) | (~(app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46)) | (~((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47))))))) <=> ((~![X1: $i] : ((~ssList(X1)) | (~(app(X4!48, X1) = U!45)) | (~(app(app(X4!48, cons(X3!47, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47))))))) | (~ssList(X5!49)) | (~(app(X4!48, X5!49) = U!45)) | (~(app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46)) | (~((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47))))))),
% 22.08/22.27 inference(rewrite,[status(thm)],[])).
% 22.08/22.27 tff(45,plain,
% 22.08/22.27 ((~![X1: $i] : ((~ssList(X1)) | (~(app(X4!48, X1) = U!45)) | (~(app(app(X4!48, cons(X3!47, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47))))))) | ((~ssList(X5!49)) | (~(app(X4!48, X5!49) = U!45)) | (~(app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46)) | (~((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47))))))),
% 22.08/22.27 inference(quant_inst,[status(thm)],[])).
% 22.08/22.27 tff(46,plain,
% 22.08/22.27 ((~![X1: $i] : ((~ssList(X1)) | (~(app(X4!48, X1) = U!45)) | (~(app(app(X4!48, cons(X3!47, nil)), X1) = V!46)) | (~((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47))))))) | (~ssList(X5!49)) | (~(app(X4!48, X5!49) = U!45)) | (~(app(app(X4!48, cons(X3!47, nil)), X5!49) = V!46)) | (~((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47)))))),
% 22.08/22.27 inference(modus_ponens,[status(thm)],[45, 44])).
% 22.08/22.27 tff(47,plain,
% 22.08/22.27 (~((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47))))),
% 22.08/22.27 inference(unit_resolution,[status(thm)],[46, 43, 42, 41, 40])).
% 22.08/22.27 tff(48,plain,
% 22.08/22.27 (((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47)))) | memberP(V!46, tptp_fun_X2_50(X3!47))),
% 22.08/22.27 inference(tautology,[status(thm)],[])).
% 22.08/22.27 tff(49,plain,
% 22.08/22.27 (memberP(V!46, tptp_fun_X2_50(X3!47))),
% 22.08/22.27 inference(unit_resolution,[status(thm)],[48, 47])).
% 22.08/22.27 tff(50,plain,
% 22.08/22.27 (((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47)))) | geq(tptp_fun_X2_50(X3!47), X3!47)),
% 22.08/22.27 inference(tautology,[status(thm)],[])).
% 22.08/22.27 tff(51,plain,
% 22.08/22.27 (geq(tptp_fun_X2_50(X3!47), X3!47)),
% 22.08/22.27 inference(unit_resolution,[status(thm)],[50, 47])).
% 22.08/22.27 tff(52,plain,
% 22.08/22.27 (((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47)))) | (~(X3!47 = tptp_fun_X2_50(X3!47)))),
% 22.08/22.27 inference(tautology,[status(thm)],[])).
% 22.08/22.27 tff(53,plain,
% 22.08/22.27 (~(X3!47 = tptp_fun_X2_50(X3!47))),
% 22.08/22.27 inference(unit_resolution,[status(thm)],[52, 47])).
% 22.08/22.27 tff(54,plain,
% 22.08/22.27 (((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47)))) | ssItem(tptp_fun_X2_50(X3!47))),
% 22.08/22.27 inference(tautology,[status(thm)],[])).
% 22.08/22.27 tff(55,plain,
% 22.08/22.27 (ssItem(tptp_fun_X2_50(X3!47))),
% 22.08/22.27 inference(unit_resolution,[status(thm)],[54, 47])).
% 22.08/22.27 tff(56,plain,
% 22.08/22.27 (^[X6: $i] : refl(((~ssItem(X6)) | (~memberP(V!46, X6)) | (X3!47 = X6) | (~geq(X6, X3!47))) <=> ((~ssItem(X6)) | (~memberP(V!46, X6)) | (X3!47 = X6) | (~geq(X6, X3!47))))),
% 22.08/22.27 inference(bind,[status(th)],[])).
% 22.08/22.27 tff(57,plain,
% 22.08/22.27 (![X6: $i] : ((~ssItem(X6)) | (~memberP(V!46, X6)) | (X3!47 = X6) | (~geq(X6, X3!47))) <=> ![X6: $i] : ((~ssItem(X6)) | (~memberP(V!46, X6)) | (X3!47 = X6) | (~geq(X6, X3!47)))),
% 22.08/22.27 inference(quant_intro,[status(thm)],[56])).
% 22.08/22.27 tff(58,plain,
% 22.08/22.27 (^[X6: $i] : trans(monotonicity(rewrite((ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47)) <=> (~((~ssItem(X6)) | (~memberP(V!46, X6)) | (X3!47 = X6) | (~geq(X6, X3!47))))), ((~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47))) <=> (~(~((~ssItem(X6)) | (~memberP(V!46, X6)) | (X3!47 = X6) | (~geq(X6, X3!47))))))), rewrite((~(~((~ssItem(X6)) | (~memberP(V!46, X6)) | (X3!47 = X6) | (~geq(X6, X3!47))))) <=> ((~ssItem(X6)) | (~memberP(V!46, X6)) | (X3!47 = X6) | (~geq(X6, X3!47)))), ((~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47))) <=> ((~ssItem(X6)) | (~memberP(V!46, X6)) | (X3!47 = X6) | (~geq(X6, X3!47)))))),
% 22.08/22.27 inference(bind,[status(th)],[])).
% 22.08/22.27 tff(59,plain,
% 22.08/22.27 (![X6: $i] : (~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47))) <=> ![X6: $i] : ((~ssItem(X6)) | (~memberP(V!46, X6)) | (X3!47 = X6) | (~geq(X6, X3!47)))),
% 22.08/22.27 inference(quant_intro,[status(thm)],[58])).
% 22.08/22.27 tff(60,plain,
% 22.08/22.27 (![X6: $i] : (~(ssItem(X6) & (~(X3!47 = X6)) & memberP(V!46, X6) & geq(X6, X3!47)))),
% 22.08/22.27 inference(and_elim,[status(thm)],[28])).
% 22.08/22.27 tff(61,plain,
% 22.08/22.27 (![X6: $i] : ((~ssItem(X6)) | (~memberP(V!46, X6)) | (X3!47 = X6) | (~geq(X6, X3!47)))),
% 22.08/22.27 inference(modus_ponens,[status(thm)],[60, 59])).
% 22.08/22.27 tff(62,plain,
% 22.08/22.27 (![X6: $i] : ((~ssItem(X6)) | (~memberP(V!46, X6)) | (X3!47 = X6) | (~geq(X6, X3!47)))),
% 22.08/22.27 inference(modus_ponens,[status(thm)],[61, 57])).
% 22.08/22.27 tff(63,plain,
% 22.08/22.27 (((~![X6: $i] : ((~ssItem(X6)) | (~memberP(V!46, X6)) | (X3!47 = X6) | (~geq(X6, X3!47)))) | ((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47))))) <=> ((~![X6: $i] : ((~ssItem(X6)) | (~memberP(V!46, X6)) | (X3!47 = X6) | (~geq(X6, X3!47)))) | (~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47))))),
% 22.08/22.27 inference(rewrite,[status(thm)],[])).
% 22.08/22.27 tff(64,plain,
% 22.08/22.27 (((~ssItem(tptp_fun_X2_50(X3!47))) | (~memberP(V!46, tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47))) <=> ((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47))))),
% 22.08/22.27 inference(rewrite,[status(thm)],[])).
% 22.08/22.27 tff(65,plain,
% 22.08/22.27 (((~![X6: $i] : ((~ssItem(X6)) | (~memberP(V!46, X6)) | (X3!47 = X6) | (~geq(X6, X3!47)))) | ((~ssItem(tptp_fun_X2_50(X3!47))) | (~memberP(V!46, tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)))) <=> ((~![X6: $i] : ((~ssItem(X6)) | (~memberP(V!46, X6)) | (X3!47 = X6) | (~geq(X6, X3!47)))) | ((~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47)))))),
% 22.08/22.27 inference(monotonicity,[status(thm)],[64])).
% 22.08/22.27 tff(66,plain,
% 22.08/22.27 (((~![X6: $i] : ((~ssItem(X6)) | (~memberP(V!46, X6)) | (X3!47 = X6) | (~geq(X6, X3!47)))) | ((~ssItem(tptp_fun_X2_50(X3!47))) | (~memberP(V!46, tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)))) <=> ((~![X6: $i] : ((~ssItem(X6)) | (~memberP(V!46, X6)) | (X3!47 = X6) | (~geq(X6, X3!47)))) | (~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47))))),
% 22.08/22.27 inference(transitivity,[status(thm)],[65, 63])).
% 22.08/22.27 tff(67,plain,
% 22.08/22.27 ((~![X6: $i] : ((~ssItem(X6)) | (~memberP(V!46, X6)) | (X3!47 = X6) | (~geq(X6, X3!47)))) | ((~ssItem(tptp_fun_X2_50(X3!47))) | (~memberP(V!46, tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)))),
% 22.16/22.33 inference(quant_inst,[status(thm)],[])).
% 22.16/22.33 tff(68,plain,
% 22.16/22.33 ((~![X6: $i] : ((~ssItem(X6)) | (~memberP(V!46, X6)) | (X3!47 = X6) | (~geq(X6, X3!47)))) | (~ssItem(tptp_fun_X2_50(X3!47))) | (X3!47 = tptp_fun_X2_50(X3!47)) | (~geq(tptp_fun_X2_50(X3!47), X3!47)) | (~memberP(V!46, tptp_fun_X2_50(X3!47)))),
% 22.16/22.33 inference(modus_ponens,[status(thm)],[67, 66])).
% 22.16/22.33 tff(69,plain,
% 22.16/22.33 ($false),
% 22.16/22.33 inference(unit_resolution,[status(thm)],[68, 62, 55, 53, 51, 49])).
% 22.16/22.33 % SZS output end Proof
% 22.16/22.34 % E exiting
%------------------------------------------------------------------------------