%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SWC038+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 : n016.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:06:15 EDT 2022 % Result : Theorem 50.42s 50.58s % Output : Proof 50.49s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SWC038+1 : TPTP v8.1.0. Released v2.4.0. % 0.03/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.14/0.35 % Computer : n016.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 600 % 0.14/0.35 % DateTime : Sun Jun 12 03:58:27 EDT 2022 % 0.14/0.35 % CPUTime : % 50.42/50.58 % SZS status Theorem % 50.42/50.58 (* PROOF-FOUND *) % 50.42/50.58 (* BEGIN-PROOF *) % 50.42/50.58 % SZS output start Proof % 50.42/50.58 1. (T_0 != T_0) ### Refl(=) % 50.42/50.58 2. (T_0 != T_0) ### Refl(=) % 50.42/50.58 3. ((nil) = T_1) (T_1 != (nil)) ### Sym(=) % 50.42/50.58 4. ((nil) != T_0) (T_0 = T_1) ((nil) = T_1) ### TransEq-sym 1 2 3 % 50.42/50.58 5. (-. ((nil) != T_1)) (T_0 = T_1) ((nil) != T_0) ### NotNot 4 % 50.42/50.58 6. (-. (((nil) != T_2) \/ ((nil) != T_1))) ((nil) != T_0) (T_0 = T_1) ### NotOr 5 % 50.42/50.58 7. (T_0 != T_0) ### Refl(=) % 50.42/50.58 8. (T_0 != T_0) ### Refl(=) % 50.42/50.58 9. (ssList T_1) (-. (ssList T_1)) ### Axiom % 50.42/50.58 10. ((nil) != (nil)) ### NotEqual % 50.42/50.58 11. (ssList T_2) (-. (ssList T_2)) ### Axiom % 50.42/50.58 12. (ssList T_1) (-. (ssList T_1)) ### Axiom % 50.42/50.58 13. (ssList T_2) (-. (ssList T_2)) ### Axiom % 50.42/50.58 14. (T_3 = T_2) (T_3 != T_2) ### Axiom % 50.42/50.58 15. ((nil) != T_2) ((nil) = T_3) (T_3 = T_2) ### Trans 10 14 % 50.42/50.58 16. (ssList T_2) (-. (ssList T_2)) ### Axiom % 50.42/50.58 17. ((nil) = T_2) ((nil) != T_2) ### Axiom % 50.42/50.58 18. (ssList T_1) (-. (ssList T_1)) ### Axiom % 50.42/50.58 19. (ssList (nil)) (-. (ssList (nil))) ### Axiom % 50.42/50.58 20. (ssList T_1) (-. (ssList T_1)) ### Axiom % 50.42/50.58 21. (-. (frontsegP T_1 (nil))) (frontsegP T_1 (nil)) ### Axiom % 50.42/50.58 22. ((ssList T_1) => (frontsegP T_1 (nil))) (-. (frontsegP T_1 (nil))) (ssList T_1) ### Imply 20 21 % 50.42/50.58 23. (All U, ((ssList U) => (frontsegP U (nil)))) (ssList T_1) (-. (frontsegP T_1 (nil))) ### All 22 % 50.42/50.58 24. (ssList (nil)) (-. (ssList (nil))) ### Axiom % 50.42/50.58 25. (ssList T_2) (-. (ssList T_2)) ### Axiom % 50.42/50.58 26. (frontsegP T_1 (nil)) (-. (frontsegP T_1 (nil))) ### Axiom % 50.42/50.58 27. (frontsegP (nil) T_2) (-. (frontsegP (nil) T_2)) ### Axiom % 50.42/50.58 28. (-. (frontsegP T_1 T_2)) (frontsegP T_1 T_2) ### Axiom % 50.42/50.58 29. ((ssList T_2) => (((frontsegP T_1 (nil)) /\ (frontsegP (nil) T_2)) => (frontsegP T_1 T_2))) (-. (frontsegP T_1 T_2)) (frontsegP (nil) T_2) (frontsegP T_1 (nil)) (ssList T_2) ### DisjTree 25 26 27 28 % 50.42/50.58 30. (All W, ((ssList W) => (((frontsegP T_1 (nil)) /\ (frontsegP (nil) W)) => (frontsegP T_1 W)))) (ssList T_2) (frontsegP T_1 (nil)) (frontsegP (nil) T_2) (-. (frontsegP T_1 T_2)) ### All 29 % 50.42/50.58 31. ((ssList (nil)) => (All W, ((ssList W) => (((frontsegP T_1 (nil)) /\ (frontsegP (nil) W)) => (frontsegP T_1 W))))) (-. (frontsegP T_1 T_2)) (frontsegP (nil) T_2) (frontsegP T_1 (nil)) (ssList T_2) (ssList (nil)) ### Imply 24 30 % 50.42/50.58 32. (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP T_1 V) /\ (frontsegP V W)) => (frontsegP T_1 W)))))) (ssList (nil)) (ssList T_2) (frontsegP T_1 (nil)) (frontsegP (nil) T_2) (-. (frontsegP T_1 T_2)) ### All 31 % 50.42/50.58 33. ((frontsegP T_1 (nil)) <=> (Ex W, ((ssList W) /\ ((app (nil) W) = T_1)))) (-. (frontsegP T_1 T_2)) (frontsegP (nil) T_2) (ssList T_2) (ssList (nil)) (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP T_1 V) /\ (frontsegP V W)) => (frontsegP T_1 W)))))) (ssList T_1) (All U, ((ssList U) => (frontsegP U (nil)))) ### Equiv 23 32 % 50.42/50.58 34. ((ssList (nil)) => ((frontsegP T_1 (nil)) <=> (Ex W, ((ssList W) /\ ((app (nil) W) = T_1))))) (All U, ((ssList U) => (frontsegP U (nil)))) (ssList T_1) (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP T_1 V) /\ (frontsegP V W)) => (frontsegP T_1 W)))))) (ssList T_2) (frontsegP (nil) T_2) (-. (frontsegP T_1 T_2)) (ssList (nil)) ### Imply 19 33 % 50.42/50.58 35. (All V, ((ssList V) => ((frontsegP T_1 V) <=> (Ex W, ((ssList W) /\ ((app V W) = T_1)))))) (ssList (nil)) (-. (frontsegP T_1 T_2)) (frontsegP (nil) T_2) (ssList T_2) (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP T_1 V) /\ (frontsegP V W)) => (frontsegP T_1 W)))))) (ssList T_1) (All U, ((ssList U) => (frontsegP U (nil)))) ### All 34 % 50.42/50.58 36. ((ssList T_1) => (All V, ((ssList V) => ((frontsegP T_1 V) <=> (Ex W, ((ssList W) /\ ((app V W) = T_1))))))) (All U, ((ssList U) => (frontsegP U (nil)))) (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP T_1 V) /\ (frontsegP V W)) => (frontsegP T_1 W)))))) (ssList T_2) (frontsegP (nil) T_2) (-. (frontsegP T_1 T_2)) (ssList (nil)) (ssList T_1) ### Imply 18 35 % 50.42/50.58 37. (All U, ((ssList U) => (All V, ((ssList V) => ((frontsegP U V) <=> (Ex W, ((ssList W) /\ ((app V W) = U)))))))) (ssList T_1) (ssList (nil)) (-. (frontsegP T_1 T_2)) (frontsegP (nil) T_2) (ssList T_2) (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP T_1 V) /\ (frontsegP V W)) => (frontsegP T_1 W)))))) (All U, ((ssList U) => (frontsegP U (nil)))) ### All 36 % 50.42/50.58 38. ((frontsegP (nil) T_2) <=> ((nil) = T_2)) (All U, ((ssList U) => (frontsegP U (nil)))) (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP T_1 V) /\ (frontsegP V W)) => (frontsegP T_1 W)))))) (ssList T_2) (-. (frontsegP T_1 T_2)) (ssList (nil)) (ssList T_1) (All U, ((ssList U) => (All V, ((ssList V) => ((frontsegP U V) <=> (Ex W, ((ssList W) /\ ((app V W) = U)))))))) ((nil) = T_2) ### Equiv 17 37 % 50.42/50.58 39. ((ssList T_2) => ((frontsegP (nil) T_2) <=> ((nil) = T_2))) ((nil) = T_2) (All U, ((ssList U) => (All V, ((ssList V) => ((frontsegP U V) <=> (Ex W, ((ssList W) /\ ((app V W) = U)))))))) (ssList T_1) (ssList (nil)) (-. (frontsegP T_1 T_2)) (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP T_1 V) /\ (frontsegP V W)) => (frontsegP T_1 W)))))) (All U, ((ssList U) => (frontsegP U (nil)))) (ssList T_2) ### Imply 16 38 % 50.42/50.58 40. (All U, ((ssList U) => ((frontsegP (nil) U) <=> ((nil) = U)))) (ssList T_2) (All U, ((ssList U) => (frontsegP U (nil)))) (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP T_1 V) /\ (frontsegP V W)) => (frontsegP T_1 W)))))) (-. (frontsegP T_1 T_2)) (ssList (nil)) (ssList T_1) (All U, ((ssList U) => (All V, ((ssList V) => ((frontsegP U V) <=> (Ex W, ((ssList W) /\ ((app V W) = U)))))))) ((nil) = T_2) ### All 39 % 50.42/50.58 41. ((segmentP (nil) T_2) <=> ((nil) = T_2)) (All U, ((ssList U) => (All V, ((ssList V) => ((frontsegP U V) <=> (Ex W, ((ssList W) /\ ((app V W) = U)))))))) (ssList T_1) (ssList (nil)) (-. (frontsegP T_1 T_2)) (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP T_1 V) /\ (frontsegP V W)) => (frontsegP T_1 W)))))) (All U, ((ssList U) => (frontsegP U (nil)))) (ssList T_2) (All U, ((ssList U) => ((frontsegP (nil) U) <=> ((nil) = U)))) (T_3 = T_2) ((nil) = T_3) ### Equiv 15 40 % 50.42/50.58 42. ((ssList T_2) => ((segmentP (nil) T_2) <=> ((nil) = T_2))) ((nil) = T_3) (T_3 = T_2) (All U, ((ssList U) => ((frontsegP (nil) U) <=> ((nil) = U)))) (All U, ((ssList U) => (frontsegP U (nil)))) (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP T_1 V) /\ (frontsegP V W)) => (frontsegP T_1 W)))))) (-. (frontsegP T_1 T_2)) (ssList (nil)) (ssList T_1) (All U, ((ssList U) => (All V, ((ssList V) => ((frontsegP U V) <=> (Ex W, ((ssList W) /\ ((app V W) = U)))))))) (ssList T_2) ### Imply 13 41 % 50.42/50.58 43. (All U, ((ssList U) => ((segmentP (nil) U) <=> ((nil) = U)))) (ssList T_2) (All U, ((ssList U) => (All V, ((ssList V) => ((frontsegP U V) <=> (Ex W, ((ssList W) /\ ((app V W) = U)))))))) (ssList T_1) (ssList (nil)) (-. (frontsegP T_1 T_2)) (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP T_1 V) /\ (frontsegP V W)) => (frontsegP T_1 W)))))) (All U, ((ssList U) => (frontsegP U (nil)))) (All U, ((ssList U) => ((frontsegP (nil) U) <=> ((nil) = U)))) (T_3 = T_2) ((nil) = T_3) ### All 42 % 50.42/50.58 44. ((ssList T_1) => (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP T_1 V) /\ (frontsegP V W)) => (frontsegP T_1 W))))))) ((nil) = T_3) (T_3 = T_2) (All U, ((ssList U) => ((frontsegP (nil) U) <=> ((nil) = U)))) (All U, ((ssList U) => (frontsegP U (nil)))) (-. (frontsegP T_1 T_2)) (ssList (nil)) (All U, ((ssList U) => (All V, ((ssList V) => ((frontsegP U V) <=> (Ex W, ((ssList W) /\ ((app V W) = U)))))))) (ssList T_2) (All U, ((ssList U) => ((segmentP (nil) U) <=> ((nil) = U)))) (ssList T_1) ### Imply 12 43 % 50.42/50.58 45. (All U, ((ssList U) => (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP U V) /\ (frontsegP V W)) => (frontsegP U W)))))))) (ssList T_1) (All U, ((ssList U) => ((segmentP (nil) U) <=> ((nil) = U)))) (ssList T_2) (All U, ((ssList U) => (All V, ((ssList V) => ((frontsegP U V) <=> (Ex W, ((ssList W) /\ ((app V W) = U)))))))) (ssList (nil)) (-. (frontsegP T_1 T_2)) (All U, ((ssList U) => (frontsegP U (nil)))) (All U, ((ssList U) => ((frontsegP (nil) U) <=> ((nil) = U)))) (T_3 = T_2) ((nil) = T_3) ### All 44 % 50.42/50.58 46. (frontsegP T_2 T_1) (-. (frontsegP T_2 T_1)) ### Axiom % 50.42/50.58 47. (T_3 != T_3) ### Refl(=) % 50.42/50.58 48. (T_1 = T_2) (T_2 != T_1) ### Sym(=) % 50.49/50.67 49. (T_3 != T_1) (T_3 = T_2) (T_1 = T_2) ### Trans 47 48 % 50.49/50.67 50. ((ssList T_2) => (((frontsegP T_1 T_2) /\ (frontsegP T_2 T_1)) => (T_1 = T_2))) (T_3 != T_1) (frontsegP T_2 T_1) ((nil) = T_3) (T_3 = T_2) (All U, ((ssList U) => ((frontsegP (nil) U) <=> ((nil) = U)))) (All U, ((ssList U) => (frontsegP U (nil)))) (ssList (nil)) (All U, ((ssList U) => (All V, ((ssList V) => ((frontsegP U V) <=> (Ex W, ((ssList W) /\ ((app V W) = U)))))))) (All U, ((ssList U) => ((segmentP (nil) U) <=> ((nil) = U)))) (ssList T_1) (All U, ((ssList U) => (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP U V) /\ (frontsegP V W)) => (frontsegP U W)))))))) (ssList T_2) ### DisjTree 11 45 46 49 % 50.49/50.67 51. (All V, ((ssList V) => (((frontsegP T_1 V) /\ (frontsegP V T_1)) => (T_1 = V)))) (ssList T_2) (All U, ((ssList U) => (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP U V) /\ (frontsegP V W)) => (frontsegP U W)))))))) (ssList T_1) (All U, ((ssList U) => ((segmentP (nil) U) <=> ((nil) = U)))) (All U, ((ssList U) => (All V, ((ssList V) => ((frontsegP U V) <=> (Ex W, ((ssList W) /\ ((app V W) = U)))))))) (ssList (nil)) (All U, ((ssList U) => (frontsegP U (nil)))) (All U, ((ssList U) => ((frontsegP (nil) U) <=> ((nil) = U)))) (T_3 = T_2) ((nil) = T_3) (frontsegP T_2 T_1) (T_3 != T_1) ### All 50 % 50.49/50.67 52. (T_1 != (nil)) (frontsegP T_2 T_1) ((nil) = T_3) (T_3 = T_2) (All U, ((ssList U) => ((frontsegP (nil) U) <=> ((nil) = U)))) (All U, ((ssList U) => (frontsegP U (nil)))) (ssList (nil)) (All U, ((ssList U) => (All V, ((ssList V) => ((frontsegP U V) <=> (Ex W, ((ssList W) /\ ((app V W) = U)))))))) (All U, ((ssList U) => ((segmentP (nil) U) <=> ((nil) = U)))) (ssList T_1) (All U, ((ssList U) => (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP U V) /\ (frontsegP V W)) => (frontsegP U W)))))))) (ssList T_2) (All V, ((ssList V) => (((frontsegP T_1 V) /\ (frontsegP V T_1)) => (T_1 = V)))) ### Trans-sym 10 51 % 50.49/50.67 53. ((ssList T_1) => (All V, ((ssList V) => (((frontsegP T_1 V) /\ (frontsegP V T_1)) => (T_1 = V))))) (ssList T_2) (All U, ((ssList U) => (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP U V) /\ (frontsegP V W)) => (frontsegP U W)))))))) (All U, ((ssList U) => ((segmentP (nil) U) <=> ((nil) = U)))) (All U, ((ssList U) => (All V, ((ssList V) => ((frontsegP U V) <=> (Ex W, ((ssList W) /\ ((app V W) = U)))))))) (ssList (nil)) (All U, ((ssList U) => (frontsegP U (nil)))) (All U, ((ssList U) => ((frontsegP (nil) U) <=> ((nil) = U)))) (T_3 = T_2) ((nil) = T_3) (frontsegP T_2 T_1) (T_1 != (nil)) (ssList T_1) ### Imply 9 52 % 50.49/50.67 54. (All U, ((ssList U) => (All V, ((ssList V) => (((frontsegP U V) /\ (frontsegP V U)) => (U = V)))))) (ssList T_1) (T_1 != (nil)) (frontsegP T_2 T_1) ((nil) = T_3) (T_3 = T_2) (All U, ((ssList U) => ((frontsegP (nil) U) <=> ((nil) = U)))) (All U, ((ssList U) => (frontsegP U (nil)))) (ssList (nil)) (All U, ((ssList U) => (All V, ((ssList V) => ((frontsegP U V) <=> (Ex W, ((ssList W) /\ ((app V W) = U)))))))) (All U, ((ssList U) => ((segmentP (nil) U) <=> ((nil) = U)))) (All U, ((ssList U) => (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP U V) /\ (frontsegP V W)) => (frontsegP U W)))))))) (ssList T_2) ### All 53 % 50.49/50.67 55. ((nil) != T_0) (T_0 = T_1) (ssList T_2) (All U, ((ssList U) => (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP U V) /\ (frontsegP V W)) => (frontsegP U W)))))))) (All U, ((ssList U) => ((segmentP (nil) U) <=> ((nil) = U)))) (All U, ((ssList U) => (All V, ((ssList V) => ((frontsegP U V) <=> (Ex W, ((ssList W) /\ ((app V W) = U)))))))) (ssList (nil)) (All U, ((ssList U) => (frontsegP U (nil)))) (All U, ((ssList U) => ((frontsegP (nil) U) <=> ((nil) = U)))) (T_3 = T_2) ((nil) = T_3) (frontsegP T_2 T_1) (ssList T_1) (All U, ((ssList U) => (All V, ((ssList V) => (((frontsegP U V) /\ (frontsegP V U)) => (U = V)))))) ### TransEq-sym 7 8 54 % 50.49/50.67 56. (-. (-. (frontsegP T_2 T_1))) (All U, ((ssList U) => (All V, ((ssList V) => (((frontsegP U V) /\ (frontsegP V U)) => (U = V)))))) (ssList T_1) ((nil) = T_3) (T_3 = T_2) (All U, ((ssList U) => ((frontsegP (nil) U) <=> ((nil) = U)))) (All U, ((ssList U) => (frontsegP U (nil)))) (ssList (nil)) (All U, ((ssList U) => (All V, ((ssList V) => ((frontsegP U V) <=> (Ex W, ((ssList W) /\ ((app V W) = U)))))))) (All U, ((ssList U) => ((segmentP (nil) U) <=> ((nil) = U)))) (All U, ((ssList U) => (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP U V) /\ (frontsegP V W)) => (frontsegP U W)))))))) (ssList T_2) (T_0 = T_1) ((nil) != T_0) ### NotNot 55 % 50.49/50.67 57. (-. ((-. (neq T_1 (nil))) \/ (-. (frontsegP T_2 T_1)))) ((nil) != T_0) (T_0 = T_1) (ssList T_2) (All U, ((ssList U) => (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP U V) /\ (frontsegP V W)) => (frontsegP U W)))))))) (All U, ((ssList U) => ((segmentP (nil) U) <=> ((nil) = U)))) (All U, ((ssList U) => (All V, ((ssList V) => ((frontsegP U V) <=> (Ex W, ((ssList W) /\ ((app V W) = U)))))))) (ssList (nil)) (All U, ((ssList U) => (frontsegP U (nil)))) (All U, ((ssList U) => ((frontsegP (nil) U) <=> ((nil) = U)))) (T_3 = T_2) ((nil) = T_3) (ssList T_1) (All U, ((ssList U) => (All V, ((ssList V) => (((frontsegP U V) /\ (frontsegP V U)) => (U = V)))))) ### NotOr 56 % 50.49/50.67 58. (-. ((((nil) != T_2) \/ ((nil) != T_1)) /\ ((-. (neq T_1 (nil))) \/ (-. (frontsegP T_2 T_1))))) (All U, ((ssList U) => (All V, ((ssList V) => (((frontsegP U V) /\ (frontsegP V U)) => (U = V)))))) (ssList T_1) ((nil) = T_3) (T_3 = T_2) (All U, ((ssList U) => ((frontsegP (nil) U) <=> ((nil) = U)))) (All U, ((ssList U) => (frontsegP U (nil)))) (ssList (nil)) (All U, ((ssList U) => (All V, ((ssList V) => ((frontsegP U V) <=> (Ex W, ((ssList W) /\ ((app V W) = U)))))))) (All U, ((ssList U) => ((segmentP (nil) U) <=> ((nil) = U)))) (All U, ((ssList U) => (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP U V) /\ (frontsegP V W)) => (frontsegP U W)))))))) (ssList T_2) (T_0 = T_1) ((nil) != T_0) ### NotAnd 6 57 % 50.49/50.67 59. (-. ((ssList T_2) => (((nil) != T_3) \/ ((T_3 != T_2) \/ ((T_0 != T_1) \/ (((nil) = T_0) \/ ((((nil) != T_2) \/ ((nil) != T_1)) /\ ((-. (neq T_1 (nil))) \/ (-. (frontsegP T_2 T_1)))))))))) (All U, ((ssList U) => (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP U V) /\ (frontsegP V W)) => (frontsegP U W)))))))) (All U, ((ssList U) => ((segmentP (nil) U) <=> ((nil) = U)))) (All U, ((ssList U) => (All V, ((ssList V) => ((frontsegP U V) <=> (Ex W, ((ssList W) /\ ((app V W) = U)))))))) (ssList (nil)) (All U, ((ssList U) => (frontsegP U (nil)))) (All U, ((ssList U) => ((frontsegP (nil) U) <=> ((nil) = U)))) (ssList T_1) (All U, ((ssList U) => (All V, ((ssList V) => (((frontsegP U V) /\ (frontsegP V U)) => (U = V)))))) ### ConjTree 58 % 50.49/50.67 60. (-. (All X, ((ssList X) => (((nil) != T_3) \/ ((T_3 != X) \/ ((T_0 != T_1) \/ (((nil) = T_0) \/ ((((nil) != X) \/ ((nil) != T_1)) /\ ((-. (neq T_1 (nil))) \/ (-. (frontsegP X T_1))))))))))) (All U, ((ssList U) => (All V, ((ssList V) => (((frontsegP U V) /\ (frontsegP V U)) => (U = V)))))) (ssList T_1) (All U, ((ssList U) => ((frontsegP (nil) U) <=> ((nil) = U)))) (All U, ((ssList U) => (frontsegP U (nil)))) (ssList (nil)) (All U, ((ssList U) => (All V, ((ssList V) => ((frontsegP U V) <=> (Ex W, ((ssList W) /\ ((app V W) = U)))))))) (All U, ((ssList U) => ((segmentP (nil) U) <=> ((nil) = U)))) (All U, ((ssList U) => (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP U V) /\ (frontsegP V W)) => (frontsegP U W)))))))) ### NotAllEx 59 % 50.49/50.67 61. (-. ((ssList T_1) => (All X, ((ssList X) => (((nil) != T_3) \/ ((T_3 != X) \/ ((T_0 != T_1) \/ (((nil) = T_0) \/ ((((nil) != X) \/ ((nil) != T_1)) /\ ((-. (neq T_1 (nil))) \/ (-. (frontsegP X T_1)))))))))))) (All U, ((ssList U) => (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP U V) /\ (frontsegP V W)) => (frontsegP U W)))))))) (All U, ((ssList U) => ((segmentP (nil) U) <=> ((nil) = U)))) (All U, ((ssList U) => (All V, ((ssList V) => ((frontsegP U V) <=> (Ex W, ((ssList W) /\ ((app V W) = U)))))))) (ssList (nil)) (All U, ((ssList U) => (frontsegP U (nil)))) (All U, ((ssList U) => ((frontsegP (nil) U) <=> ((nil) = U)))) (All U, ((ssList U) => (All V, ((ssList V) => (((frontsegP U V) /\ (frontsegP V U)) => (U = V)))))) ### NotImply 60 % 50.49/50.68 62. (-. (All W, ((ssList W) => (All X, ((ssList X) => (((nil) != T_3) \/ ((T_3 != X) \/ ((T_0 != W) \/ (((nil) = T_0) \/ ((((nil) != X) \/ ((nil) != W)) /\ ((-. (neq W (nil))) \/ (-. (frontsegP X W))))))))))))) (All U, ((ssList U) => (All V, ((ssList V) => (((frontsegP U V) /\ (frontsegP V U)) => (U = V)))))) (All U, ((ssList U) => ((frontsegP (nil) U) <=> ((nil) = U)))) (All U, ((ssList U) => (frontsegP U (nil)))) (ssList (nil)) (All U, ((ssList U) => (All V, ((ssList V) => ((frontsegP U V) <=> (Ex W, ((ssList W) /\ ((app V W) = U)))))))) (All U, ((ssList U) => ((segmentP (nil) U) <=> ((nil) = U)))) (All U, ((ssList U) => (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP U V) /\ (frontsegP V W)) => (frontsegP U W)))))))) ### NotAllEx 61 % 50.49/50.68 63. (-. ((ssList T_3) => (All W, ((ssList W) => (All X, ((ssList X) => (((nil) != T_3) \/ ((T_3 != X) \/ ((T_0 != W) \/ (((nil) = T_0) \/ ((((nil) != X) \/ ((nil) != W)) /\ ((-. (neq W (nil))) \/ (-. (frontsegP X W)))))))))))))) (All U, ((ssList U) => (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP U V) /\ (frontsegP V W)) => (frontsegP U W)))))))) (All U, ((ssList U) => ((segmentP (nil) U) <=> ((nil) = U)))) (All U, ((ssList U) => (All V, ((ssList V) => ((frontsegP U V) <=> (Ex W, ((ssList W) /\ ((app V W) = U)))))))) (ssList (nil)) (All U, ((ssList U) => (frontsegP U (nil)))) (All U, ((ssList U) => ((frontsegP (nil) U) <=> ((nil) = U)))) (All U, ((ssList U) => (All V, ((ssList V) => (((frontsegP U V) /\ (frontsegP V U)) => (U = V)))))) ### NotImply 62 % 50.49/50.68 64. (-. (All V, ((ssList V) => (All W, ((ssList W) => (All X, ((ssList X) => (((nil) != V) \/ ((V != X) \/ ((T_0 != W) \/ (((nil) = T_0) \/ ((((nil) != X) \/ ((nil) != W)) /\ ((-. (neq W (nil))) \/ (-. (frontsegP X W))))))))))))))) (All U, ((ssList U) => (All V, ((ssList V) => (((frontsegP U V) /\ (frontsegP V U)) => (U = V)))))) (All U, ((ssList U) => ((frontsegP (nil) U) <=> ((nil) = U)))) (All U, ((ssList U) => (frontsegP U (nil)))) (ssList (nil)) (All U, ((ssList U) => (All V, ((ssList V) => ((frontsegP U V) <=> (Ex W, ((ssList W) /\ ((app V W) = U)))))))) (All U, ((ssList U) => ((segmentP (nil) U) <=> ((nil) = U)))) (All U, ((ssList U) => (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP U V) /\ (frontsegP V W)) => (frontsegP U W)))))))) ### NotAllEx 63 % 50.49/50.68 65. (-. ((ssList T_0) => (All V, ((ssList V) => (All W, ((ssList W) => (All X, ((ssList X) => (((nil) != V) \/ ((V != X) \/ ((T_0 != W) \/ (((nil) = T_0) \/ ((((nil) != X) \/ ((nil) != W)) /\ ((-. (neq W (nil))) \/ (-. (frontsegP X W)))))))))))))))) (All U, ((ssList U) => (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP U V) /\ (frontsegP V W)) => (frontsegP U W)))))))) (All U, ((ssList U) => ((segmentP (nil) U) <=> ((nil) = U)))) (All U, ((ssList U) => (All V, ((ssList V) => ((frontsegP U V) <=> (Ex W, ((ssList W) /\ ((app V W) = U)))))))) (ssList (nil)) (All U, ((ssList U) => (frontsegP U (nil)))) (All U, ((ssList U) => ((frontsegP (nil) U) <=> ((nil) = U)))) (All U, ((ssList U) => (All V, ((ssList V) => (((frontsegP U V) /\ (frontsegP V U)) => (U = V)))))) ### NotImply 64 % 50.49/50.68 66. (-. (All U, ((ssList U) => (All V, ((ssList V) => (All W, ((ssList W) => (All X, ((ssList X) => (((nil) != V) \/ ((V != X) \/ ((U != W) \/ (((nil) = U) \/ ((((nil) != X) \/ ((nil) != W)) /\ ((-. (neq W (nil))) \/ (-. (frontsegP X W))))))))))))))))) (All U, ((ssList U) => (All V, ((ssList V) => (((frontsegP U V) /\ (frontsegP V U)) => (U = V)))))) (All U, ((ssList U) => ((frontsegP (nil) U) <=> ((nil) = U)))) (All U, ((ssList U) => (frontsegP U (nil)))) (ssList (nil)) (All U, ((ssList U) => (All V, ((ssList V) => ((frontsegP U V) <=> (Ex W, ((ssList W) /\ ((app V W) = U)))))))) (All U, ((ssList U) => ((segmentP (nil) U) <=> ((nil) = U)))) (All U, ((ssList U) => (All V, ((ssList V) => (All W, ((ssList W) => (((frontsegP U V) /\ (frontsegP V W)) => (frontsegP U W)))))))) ### NotAllEx 65 % 50.49/50.68 % SZS output end Proof % 50.49/50.68 (* END-PROOF *) %------------------------------------------------------------------------------