%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SWC381+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n025.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 : 600s % DateTime : Tue Jul 19 22:07:59 EDT 2022 % Result : Theorem 53.69s 53.95s % Output : Proof 53.83s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWC381+1 : TPTP v8.1.0. Released v2.4.0. % 0.12/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.34 % Computer : n025.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Sat Jun 11 22:57:07 EDT 2022 % 0.12/0.34 % CPUTime : % 53.69/53.95 % SZS status Theorem % 53.69/53.95 (* PROOF-FOUND *) % 53.69/53.95 (* BEGIN-PROOF *) % 53.69/53.95 % SZS output start Proof % 53.69/53.95 1. (ssItem T_0) (-. (ssItem T_0)) ### Axiom % 53.69/53.95 2. (ssItem T_0) (-. (ssItem T_0)) ### Axiom % 53.69/53.95 3. (ssItem T_0) (-. (ssItem T_0)) ### Axiom % 53.69/53.95 4. ((cons T_0 (nil)) != (cons T_0 (nil))) ### Refl(=) % 53.69/53.95 5. (T_1 = T_2) (T_2 != T_1) ### Sym(=) % 53.69/53.95 6. ((cons T_0 (nil)) != T_1) ((cons T_0 (nil)) = T_2) (T_1 = T_2) ### Trans 4 5 % 53.69/53.95 7. (ssItem T_0) (-. (ssItem T_0)) ### Axiom % 53.69/53.95 8. (ssItem T_0) (-. (ssItem T_0)) ### Axiom % 53.69/53.95 9. (ssItem T_0) (-. (ssItem T_0)) ### Axiom % 53.69/53.95 10. (ssList T_3) (-. (ssList T_3)) ### Axiom % 53.69/53.95 11. (ssList T_3) (-. (ssList T_3)) ### Axiom % 53.69/53.95 12. (ssList T_4) (-. (ssList T_4)) ### Axiom % 53.69/53.95 13. (ssList T_3) (-. (ssList T_3)) ### Axiom % 53.69/53.95 14. (memberP T_4 T_0) (-. (memberP T_4 T_0)) ### Axiom % 53.69/53.95 15. (-. ((memberP T_4 T_0) \/ (memberP T_3 T_0))) (memberP T_4 T_0) ### NotOr 14 % 53.69/53.95 16. (T_3 = T_4) (T_4 != T_3) ### Sym(=) % 53.69/53.95 17. (T_3 != T_3) ### Refl(=) % 53.69/53.95 18. ((app T_4 T_3) != (app T_3 T_3)) (T_3 = T_4) ### NotEqual 16 17 % 53.69/53.95 19. (-. (T_0 != T_0)) (T_0 != T_0) ### Axiom % 53.69/53.95 20. (-. (memberP (app T_3 T_3) T_0)) (memberP (app T_4 T_3) T_0) (-. (T_0 != T_0)) (T_3 = T_4) ### P-NotP 18 19 % 53.69/53.95 21. ((memberP (app T_4 T_3) T_0) <=> ((memberP T_4 T_0) \/ (memberP T_3 T_0))) (T_3 = T_4) (-. (T_0 != T_0)) (-. (memberP (app T_3 T_3) T_0)) (memberP T_4 T_0) ### Equiv 15 20 % 53.69/53.95 22. ((ssList T_3) => ((memberP (app T_4 T_3) T_0) <=> ((memberP T_4 T_0) \/ (memberP T_3 T_0)))) (memberP T_4 T_0) (-. (memberP (app T_3 T_3) T_0)) (-. (T_0 != T_0)) (T_3 = T_4) (ssList T_3) ### Imply 13 21 % 53.69/53.95 23. (All W, ((ssList W) => ((memberP (app T_4 W) T_0) <=> ((memberP T_4 T_0) \/ (memberP W T_0))))) (ssList T_3) (T_3 = T_4) (-. (T_0 != T_0)) (-. (memberP (app T_3 T_3) T_0)) (memberP T_4 T_0) ### All 22 % 53.69/53.95 24. ((ssList T_4) => (All W, ((ssList W) => ((memberP (app T_4 W) T_0) <=> ((memberP T_4 T_0) \/ (memberP W T_0)))))) (memberP T_4 T_0) (-. (memberP (app T_3 T_3) T_0)) (-. (T_0 != T_0)) (T_3 = T_4) (ssList T_3) (ssList T_4) ### Imply 12 23 % 53.69/53.95 25. (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) T_0) <=> ((memberP V T_0) \/ (memberP W T_0))))))) (ssList T_4) (ssList T_3) (T_3 = T_4) (-. (T_0 != T_0)) (-. (memberP (app T_3 T_3) T_0)) (memberP T_4 T_0) ### All 24 % 53.69/53.95 26. (-. (memberP T_3 T_0)) (memberP T_3 T_0) ### Axiom % 53.69/53.95 27. (-. (memberP T_3 T_0)) (memberP T_3 T_0) ### Axiom % 53.69/53.95 28. ((memberP T_3 T_0) \/ (memberP T_3 T_0)) (-. (memberP T_3 T_0)) ### Or 26 27 % 53.69/53.95 29. ((memberP (app T_3 T_3) T_0) <=> ((memberP T_3 T_0) \/ (memberP T_3 T_0))) (-. (memberP T_3 T_0)) (memberP T_4 T_0) (-. (T_0 != T_0)) (T_3 = T_4) (ssList T_3) (ssList T_4) (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) T_0) <=> ((memberP V T_0) \/ (memberP W T_0))))))) ### Equiv 25 28 % 53.69/53.95 30. ((ssList T_3) => ((memberP (app T_3 T_3) T_0) <=> ((memberP T_3 T_0) \/ (memberP T_3 T_0)))) (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) T_0) <=> ((memberP V T_0) \/ (memberP W T_0))))))) (ssList T_4) (T_3 = T_4) (-. (T_0 != T_0)) (memberP T_4 T_0) (-. (memberP T_3 T_0)) (ssList T_3) ### Imply 11 29 % 53.69/53.95 31. (All W, ((ssList W) => ((memberP (app T_3 W) T_0) <=> ((memberP T_3 T_0) \/ (memberP W T_0))))) (ssList T_3) (-. (memberP T_3 T_0)) (memberP T_4 T_0) (-. (T_0 != T_0)) (T_3 = T_4) (ssList T_4) (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) T_0) <=> ((memberP V T_0) \/ (memberP W T_0))))))) ### All 30 % 53.69/53.95 32. ((ssList T_3) => (All W, ((ssList W) => ((memberP (app T_3 W) T_0) <=> ((memberP T_3 T_0) \/ (memberP W T_0)))))) (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) T_0) <=> ((memberP V T_0) \/ (memberP W T_0))))))) (ssList T_4) (T_3 = T_4) (-. (T_0 != T_0)) (memberP T_4 T_0) (-. (memberP T_3 T_0)) (ssList T_3) ### Imply 10 31 % 53.69/53.95 33. (ssList T_3) (-. (memberP T_3 T_0)) (memberP T_4 T_0) (-. (T_0 != T_0)) (T_3 = T_4) (ssList T_4) (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) T_0) <=> ((memberP V T_0) \/ (memberP W T_0))))))) ### All 32 % 53.69/53.95 34. (leq T_0 T_0) (-. (leq T_0 T_0)) ### Axiom % 53.69/53.95 35. (-. ((T_0 != T_0) /\ (leq T_0 T_0))) (leq T_0 T_0) (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) T_0) <=> ((memberP V T_0) \/ (memberP W T_0))))))) (ssList T_4) (T_3 = T_4) (memberP T_4 T_0) (-. (memberP T_3 T_0)) (ssList T_3) ### NotAnd 33 34 % 53.69/53.95 36. (-. (lt T_0 T_0)) (lt T_0 T_0) ### Axiom % 53.69/53.95 37. ((lt T_0 T_0) <=> ((T_0 != T_0) /\ (leq T_0 T_0))) (-. (lt T_0 T_0)) (ssList T_3) (-. (memberP T_3 T_0)) (memberP T_4 T_0) (T_3 = T_4) (ssList T_4) (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) T_0) <=> ((memberP V T_0) \/ (memberP W T_0))))))) (leq T_0 T_0) ### Equiv 35 36 % 53.69/53.95 38. ((ssItem T_0) => ((lt T_0 T_0) <=> ((T_0 != T_0) /\ (leq T_0 T_0)))) (leq T_0 T_0) (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) T_0) <=> ((memberP V T_0) \/ (memberP W T_0))))))) (ssList T_4) (T_3 = T_4) (memberP T_4 T_0) (-. (memberP T_3 T_0)) (ssList T_3) (-. (lt T_0 T_0)) (ssItem T_0) ### Imply 9 37 % 53.69/53.95 39. (All V, ((ssItem V) => ((lt T_0 V) <=> ((T_0 != V) /\ (leq T_0 V))))) (ssItem T_0) (-. (lt T_0 T_0)) (ssList T_3) (-. (memberP T_3 T_0)) (memberP T_4 T_0) (T_3 = T_4) (ssList T_4) (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) T_0) <=> ((memberP V T_0) \/ (memberP W T_0))))))) (leq T_0 T_0) ### All 38 % 53.69/53.95 40. ((ssItem T_0) => (-. (lt T_0 T_0))) (leq T_0 T_0) (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) T_0) <=> ((memberP V T_0) \/ (memberP W T_0))))))) (ssList T_4) (T_3 = T_4) (memberP T_4 T_0) (-. (memberP T_3 T_0)) (ssList T_3) (All V, ((ssItem V) => ((lt T_0 V) <=> ((T_0 != V) /\ (leq T_0 V))))) (ssItem T_0) ### Imply 8 39 % 53.69/53.95 41. (All U, ((ssItem U) => (-. (lt U U)))) (ssItem T_0) (All V, ((ssItem V) => ((lt T_0 V) <=> ((T_0 != V) /\ (leq T_0 V))))) (ssList T_3) (-. (memberP T_3 T_0)) (memberP T_4 T_0) (T_3 = T_4) (ssList T_4) (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) T_0) <=> ((memberP V T_0) \/ (memberP W T_0))))))) (leq T_0 T_0) ### All 40 % 53.69/53.95 42. ((ssItem T_0) => (All V, ((ssItem V) => ((lt T_0 V) <=> ((T_0 != V) /\ (leq T_0 V)))))) (leq T_0 T_0) (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) T_0) <=> ((memberP V T_0) \/ (memberP W T_0))))))) (ssList T_4) (T_3 = T_4) (memberP T_4 T_0) (-. (memberP T_3 T_0)) (ssList T_3) (All U, ((ssItem U) => (-. (lt U U)))) (ssItem T_0) ### Imply 7 41 % 53.69/53.95 43. (All U, ((ssItem U) => (All V, ((ssItem V) => ((lt U V) <=> ((U != V) /\ (leq U V))))))) (ssItem T_0) (All U, ((ssItem U) => (-. (lt U U)))) (ssList T_3) (-. (memberP T_3 T_0)) (memberP T_4 T_0) (T_3 = T_4) (ssList T_4) (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) T_0) <=> ((memberP V T_0) \/ (memberP W T_0))))))) (leq T_0 T_0) ### All 42 % 53.69/53.95 44. (-. ((ssItem T_0) /\ (((cons T_0 (nil)) = T_1) /\ (memberP T_3 T_0)))) (leq T_0 T_0) (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) T_0) <=> ((memberP V T_0) \/ (memberP W T_0))))))) (ssList T_4) (T_3 = T_4) (memberP T_4 T_0) (ssList T_3) (All U, ((ssItem U) => (-. (lt U U)))) (All U, ((ssItem U) => (All V, ((ssItem V) => ((lt U V) <=> ((U != V) /\ (leq U V))))))) (T_1 = T_2) ((cons T_0 (nil)) = T_2) (ssItem T_0) ### DisjTree 3 6 43 % 53.69/53.95 45. (-. (Ex Y, ((ssItem Y) /\ (((cons Y (nil)) = T_1) /\ (memberP T_3 Y))))) (ssItem T_0) ((cons T_0 (nil)) = T_2) (T_1 = T_2) (All U, ((ssItem U) => (All V, ((ssItem V) => ((lt U V) <=> ((U != V) /\ (leq U V))))))) (All U, ((ssItem U) => (-. (lt U U)))) (ssList T_3) (memberP T_4 T_0) (T_3 = T_4) (ssList T_4) (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) T_0) <=> ((memberP V T_0) \/ (memberP W T_0))))))) (leq T_0 T_0) ### NotExists 44 % 53.69/53.95 46. ((ssItem T_0) => (leq T_0 T_0)) (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) T_0) <=> ((memberP V T_0) \/ (memberP W T_0))))))) (ssList T_4) (T_3 = T_4) (memberP T_4 T_0) (ssList T_3) (All U, ((ssItem U) => (-. (lt U U)))) (All U, ((ssItem U) => (All V, ((ssItem V) => ((lt U V) <=> ((U != V) /\ (leq U V))))))) (T_1 = T_2) ((cons T_0 (nil)) = T_2) (-. (Ex Y, ((ssItem Y) /\ (((cons Y (nil)) = T_1) /\ (memberP T_3 Y))))) (ssItem T_0) ### Imply 2 45 % 53.69/53.95 47. (All U, ((ssItem U) => (leq U U))) (ssItem T_0) (-. (Ex Y, ((ssItem Y) /\ (((cons Y (nil)) = T_1) /\ (memberP T_3 Y))))) ((cons T_0 (nil)) = T_2) (T_1 = T_2) (All U, ((ssItem U) => (All V, ((ssItem V) => ((lt U V) <=> ((U != V) /\ (leq U V))))))) (All U, ((ssItem U) => (-. (lt U U)))) (ssList T_3) (memberP T_4 T_0) (T_3 = T_4) (ssList T_4) (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) T_0) <=> ((memberP V T_0) \/ (memberP W T_0))))))) ### All 46 % 53.80/54.03 48. ((ssItem T_0) => (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) T_0) <=> ((memberP V T_0) \/ (memberP W T_0)))))))) (ssList T_4) (T_3 = T_4) (memberP T_4 T_0) (ssList T_3) (All U, ((ssItem U) => (-. (lt U U)))) (All U, ((ssItem U) => (All V, ((ssItem V) => ((lt U V) <=> ((U != V) /\ (leq U V))))))) (T_1 = T_2) ((cons T_0 (nil)) = T_2) (-. (Ex Y, ((ssItem Y) /\ (((cons Y (nil)) = T_1) /\ (memberP T_3 Y))))) (All U, ((ssItem U) => (leq U U))) (ssItem T_0) ### Imply 1 47 % 53.80/54.03 49. (All U, ((ssItem U) => (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) U) <=> ((memberP V U) \/ (memberP W U))))))))) (ssItem T_0) (All U, ((ssItem U) => (leq U U))) (-. (Ex Y, ((ssItem Y) /\ (((cons Y (nil)) = T_1) /\ (memberP T_3 Y))))) ((cons T_0 (nil)) = T_2) (T_1 = T_2) (All U, ((ssItem U) => (All V, ((ssItem V) => ((lt U V) <=> ((U != V) /\ (leq U V))))))) (All U, ((ssItem U) => (-. (lt U U)))) (ssList T_3) (memberP T_4 T_0) (T_3 = T_4) (ssList T_4) ### All 48 % 53.80/54.03 50. (-. ((ssItem T_0) => (((cons T_0 (nil)) != T_2) \/ (-. (memberP T_4 T_0))))) (ssList T_4) (T_3 = T_4) (ssList T_3) (All U, ((ssItem U) => (-. (lt U U)))) (All U, ((ssItem U) => (All V, ((ssItem V) => ((lt U V) <=> ((U != V) /\ (leq U V))))))) (T_1 = T_2) (-. (Ex Y, ((ssItem Y) /\ (((cons Y (nil)) = T_1) /\ (memberP T_3 Y))))) (All U, ((ssItem U) => (leq U U))) (All U, ((ssItem U) => (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) U) <=> ((memberP V U) \/ (memberP W U))))))))) ### ConjTree 49 % 53.80/54.03 51. (-. (All Z, ((ssItem Z) => (((cons Z (nil)) != T_2) \/ (-. (memberP T_4 Z)))))) (All U, ((ssItem U) => (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) U) <=> ((memberP V U) \/ (memberP W U))))))))) (All U, ((ssItem U) => (leq U U))) (-. (Ex Y, ((ssItem Y) /\ (((cons Y (nil)) = T_1) /\ (memberP T_3 Y))))) (T_1 = T_2) (All U, ((ssItem U) => (All V, ((ssItem V) => ((lt U V) <=> ((U != V) /\ (leq U V))))))) (All U, ((ssItem U) => (-. (lt U U)))) (ssList T_3) (T_3 = T_4) (ssList T_4) ### NotAllEx 50 % 53.80/54.03 52. (-. ((-. (neq T_3 (nil))) \/ ((Ex Y, ((ssItem Y) /\ (((cons Y (nil)) = T_1) /\ (memberP T_3 Y)))) \/ (All Z, ((ssItem Z) => (((cons Z (nil)) != T_2) \/ (-. (memberP T_4 Z)))))))) (ssList T_4) (T_3 = T_4) (ssList T_3) (All U, ((ssItem U) => (-. (lt U U)))) (All U, ((ssItem U) => (All V, ((ssItem V) => ((lt U V) <=> ((U != V) /\ (leq U V))))))) (T_1 = T_2) (All U, ((ssItem U) => (leq U U))) (All U, ((ssItem U) => (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) U) <=> ((memberP V U) \/ (memberP W U))))))))) ### ConjTree 51 % 53.80/54.03 53. (T_3 = T_4) (T_3 != T_4) ### Axiom % 53.80/54.03 54. ((nil) != (nil)) ### NotEqual % 53.80/54.03 55. (-. (neq T_4 (nil))) (neq T_3 (nil)) (T_3 = T_4) ### P-NotP 53 54 % 53.80/54.03 56. (-. (-. (neq T_3 (nil)))) (T_3 = T_4) (-. (neq T_4 (nil))) ### NotNot 55 % 53.80/54.03 57. (-. ((-. (neq T_3 (nil))) \/ (neq T_4 (nil)))) (T_3 = T_4) ### NotOr 56 % 53.80/54.03 58. (-. (((-. (neq T_3 (nil))) \/ ((Ex Y, ((ssItem Y) /\ (((cons Y (nil)) = T_1) /\ (memberP T_3 Y)))) \/ (All Z, ((ssItem Z) => (((cons Z (nil)) != T_2) \/ (-. (memberP T_4 Z))))))) /\ ((-. (neq T_3 (nil))) \/ (neq T_4 (nil))))) (All U, ((ssItem U) => (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) U) <=> ((memberP V U) \/ (memberP W U))))))))) (All U, ((ssItem U) => (leq U U))) (T_1 = T_2) (All U, ((ssItem U) => (All V, ((ssItem V) => ((lt U V) <=> ((U != V) /\ (leq U V))))))) (All U, ((ssItem U) => (-. (lt U U)))) (ssList T_3) (T_3 = T_4) (ssList T_4) ### NotAnd 52 57 % 53.80/54.03 59. (-. ((ssList T_4) => ((T_3 != T_4) \/ ((T_1 != T_2) \/ (((-. (neq T_3 (nil))) \/ ((Ex Y, ((ssItem Y) /\ (((cons Y (nil)) = T_1) /\ (memberP T_3 Y)))) \/ (All Z, ((ssItem Z) => (((cons Z (nil)) != T_2) \/ (-. (memberP T_4 Z))))))) /\ ((-. (neq T_3 (nil))) \/ (neq T_4 (nil)))))))) (ssList T_3) (All U, ((ssItem U) => (-. (lt U U)))) (All U, ((ssItem U) => (All V, ((ssItem V) => ((lt U V) <=> ((U != V) /\ (leq U V))))))) (All U, ((ssItem U) => (leq U U))) (All U, ((ssItem U) => (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) U) <=> ((memberP V U) \/ (memberP W U))))))))) ### ConjTree 58 % 53.80/54.03 60. (-. (All X, ((ssList X) => ((T_3 != X) \/ ((T_1 != T_2) \/ (((-. (neq T_3 (nil))) \/ ((Ex Y, ((ssItem Y) /\ (((cons Y (nil)) = T_1) /\ (memberP T_3 Y)))) \/ (All Z, ((ssItem Z) => (((cons Z (nil)) != T_2) \/ (-. (memberP X Z))))))) /\ ((-. (neq T_3 (nil))) \/ (neq X (nil))))))))) (All U, ((ssItem U) => (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) U) <=> ((memberP V U) \/ (memberP W U))))))))) (All U, ((ssItem U) => (leq U U))) (All U, ((ssItem U) => (All V, ((ssItem V) => ((lt U V) <=> ((U != V) /\ (leq U V))))))) (All U, ((ssItem U) => (-. (lt U U)))) (ssList T_3) ### NotAllEx 59 % 53.80/54.03 61. (-. ((ssList T_2) => (All X, ((ssList X) => ((T_3 != X) \/ ((T_1 != T_2) \/ (((-. (neq T_3 (nil))) \/ ((Ex Y, ((ssItem Y) /\ (((cons Y (nil)) = T_1) /\ (memberP T_3 Y)))) \/ (All Z, ((ssItem Z) => (((cons Z (nil)) != T_2) \/ (-. (memberP X Z))))))) /\ ((-. (neq T_3 (nil))) \/ (neq X (nil)))))))))) (ssList T_3) (All U, ((ssItem U) => (-. (lt U U)))) (All U, ((ssItem U) => (All V, ((ssItem V) => ((lt U V) <=> ((U != V) /\ (leq U V))))))) (All U, ((ssItem U) => (leq U U))) (All U, ((ssItem U) => (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) U) <=> ((memberP V U) \/ (memberP W U))))))))) ### NotImply 60 % 53.80/54.03 62. (-. (All W, ((ssList W) => (All X, ((ssList X) => ((T_3 != X) \/ ((T_1 != W) \/ (((-. (neq T_3 (nil))) \/ ((Ex Y, ((ssItem Y) /\ (((cons Y (nil)) = T_1) /\ (memberP T_3 Y)))) \/ (All Z, ((ssItem Z) => (((cons Z (nil)) != W) \/ (-. (memberP X Z))))))) /\ ((-. (neq T_3 (nil))) \/ (neq X (nil))))))))))) (All U, ((ssItem U) => (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) U) <=> ((memberP V U) \/ (memberP W U))))))))) (All U, ((ssItem U) => (leq U U))) (All U, ((ssItem U) => (All V, ((ssItem V) => ((lt U V) <=> ((U != V) /\ (leq U V))))))) (All U, ((ssItem U) => (-. (lt U U)))) (ssList T_3) ### NotAllEx 61 % 53.80/54.03 63. (-. ((ssList T_3) => (All W, ((ssList W) => (All X, ((ssList X) => ((T_3 != X) \/ ((T_1 != W) \/ (((-. (neq T_3 (nil))) \/ ((Ex Y, ((ssItem Y) /\ (((cons Y (nil)) = T_1) /\ (memberP T_3 Y)))) \/ (All Z, ((ssItem Z) => (((cons Z (nil)) != W) \/ (-. (memberP X Z))))))) /\ ((-. (neq T_3 (nil))) \/ (neq X (nil)))))))))))) (All U, ((ssItem U) => (-. (lt U U)))) (All U, ((ssItem U) => (All V, ((ssItem V) => ((lt U V) <=> ((U != V) /\ (leq U V))))))) (All U, ((ssItem U) => (leq U U))) (All U, ((ssItem U) => (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) U) <=> ((memberP V U) \/ (memberP W U))))))))) ### NotImply 62 % 53.80/54.03 64. (-. (All V, ((ssList V) => (All W, ((ssList W) => (All X, ((ssList X) => ((V != X) \/ ((T_1 != W) \/ (((-. (neq V (nil))) \/ ((Ex Y, ((ssItem Y) /\ (((cons Y (nil)) = T_1) /\ (memberP V Y)))) \/ (All Z, ((ssItem Z) => (((cons Z (nil)) != W) \/ (-. (memberP X Z))))))) /\ ((-. (neq V (nil))) \/ (neq X (nil))))))))))))) (All U, ((ssItem U) => (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) U) <=> ((memberP V U) \/ (memberP W U))))))))) (All U, ((ssItem U) => (leq U U))) (All U, ((ssItem U) => (All V, ((ssItem V) => ((lt U V) <=> ((U != V) /\ (leq U V))))))) (All U, ((ssItem U) => (-. (lt U U)))) ### NotAllEx 63 % 53.80/54.03 65. (-. ((ssList T_1) => (All V, ((ssList V) => (All W, ((ssList W) => (All X, ((ssList X) => ((V != X) \/ ((T_1 != W) \/ (((-. (neq V (nil))) \/ ((Ex Y, ((ssItem Y) /\ (((cons Y (nil)) = T_1) /\ (memberP V Y)))) \/ (All Z, ((ssItem Z) => (((cons Z (nil)) != W) \/ (-. (memberP X Z))))))) /\ ((-. (neq V (nil))) \/ (neq X (nil)))))))))))))) (All U, ((ssItem U) => (-. (lt U U)))) (All U, ((ssItem U) => (All V, ((ssItem V) => ((lt U V) <=> ((U != V) /\ (leq U V))))))) (All U, ((ssItem U) => (leq U U))) (All U, ((ssItem U) => (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) U) <=> ((memberP V U) \/ (memberP W U))))))))) ### NotImply 64 % 53.83/54.04 66. (-. (All U, ((ssList U) => (All V, ((ssList V) => (All W, ((ssList W) => (All X, ((ssList X) => ((V != X) \/ ((U != W) \/ (((-. (neq V (nil))) \/ ((Ex Y, ((ssItem Y) /\ (((cons Y (nil)) = U) /\ (memberP V Y)))) \/ (All Z, ((ssItem Z) => (((cons Z (nil)) != W) \/ (-. (memberP X Z))))))) /\ ((-. (neq V (nil))) \/ (neq X (nil))))))))))))))) (All U, ((ssItem U) => (All V, ((ssList V) => (All W, ((ssList W) => ((memberP (app V W) U) <=> ((memberP V U) \/ (memberP W U))))))))) (All U, ((ssItem U) => (leq U U))) (All U, ((ssItem U) => (All V, ((ssItem V) => ((lt U V) <=> ((U != V) /\ (leq U V))))))) (All U, ((ssItem U) => (-. (lt U U)))) ### NotAllEx 65 % 53.83/54.04 % SZS output end Proof % 53.83/54.04 (* END-PROOF *) %------------------------------------------------------------------------------