%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SEU101+1 : TPTP v8.1.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n017.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 14:48:19 EDT 2022 % Result : Theorem 3.16s 3.35s % Output : Proof 3.16s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SEU101+1 : TPTP v8.1.0. Released v3.2.0. % 0.07/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.34 % Computer : n017.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 : 600 % 0.13/0.34 % DateTime : Sun Jun 19 22:08:28 EDT 2022 % 0.13/0.34 % CPUTime : % 3.16/3.35 % SZS status Theorem % 3.16/3.35 (* PROOF-FOUND *) % 3.16/3.35 (* BEGIN-PROOF *) % 3.16/3.35 % SZS output start Proof % 3.16/3.35 1. (in T_0 T_1) (-. (in T_0 T_1)) ### Axiom % 3.16/3.35 2. (in T_2 T_1) (-. (in T_2 T_1)) ### Axiom % 3.16/3.35 3. (-. (in (set_union2 T_0 T_2) T_1)) (in (set_union2 T_0 T_2) T_1) ### Axiom % 3.16/3.35 4. ((in (set_union2 T_0 T_2) T_1) /\ (in (set_difference T_0 T_2) T_1)) (-. (in (set_union2 T_0 T_2) T_1)) ### And 3 % 3.16/3.35 5. (((in T_0 T_1) /\ (in T_2 T_1)) => ((in (set_union2 T_0 T_2) T_1) /\ (in (set_difference T_0 T_2) T_1))) (-. (in (set_union2 T_0 T_2) T_1)) (in T_2 T_1) (in T_0 T_1) ### DisjTree 1 2 4 % 3.16/3.35 6. (All C, (((in T_0 T_1) /\ (in C T_1)) => ((in (set_union2 T_0 C) T_1) /\ (in (set_difference T_0 C) T_1)))) (in T_0 T_1) (in T_2 T_1) (-. (in (set_union2 T_0 T_2) T_1)) ### All 5 % 3.16/3.35 7. (All B, (All C, (((in B T_1) /\ (in C T_1)) => ((in (set_union2 B C) T_1) /\ (in (set_difference B C) T_1))))) (-. (in (set_union2 T_0 T_2) T_1)) (in T_2 T_1) (in T_0 T_1) ### All 6 % 3.16/3.35 8. (-. (((in T_0 T_1) /\ (in T_2 T_1)) => (in (set_union2 T_0 T_2) T_1))) (All B, (All C, (((in B T_1) /\ (in C T_1)) => ((in (set_union2 B C) T_1) /\ (in (set_difference B C) T_1))))) ### ConjTree 7 % 3.16/3.35 9. (-. (All C, (((in T_0 T_1) /\ (in C T_1)) => (in (set_union2 T_0 C) T_1)))) (All B, (All C, (((in B T_1) /\ (in C T_1)) => ((in (set_union2 B C) T_1) /\ (in (set_difference B C) T_1))))) ### NotAllEx 8 % 3.16/3.35 10. (-. (All B, (All C, (((in B T_1) /\ (in C T_1)) => (in (set_union2 B C) T_1))))) (All B, (All C, (((in B T_1) /\ (in C T_1)) => ((in (set_union2 B C) T_1) /\ (in (set_difference B C) T_1))))) ### NotAllEx 9 % 3.16/3.35 11. (-. (cup_closed T_1)) (All B, (All C, (((in B T_1) /\ (in C T_1)) => ((in (set_union2 B C) T_1) /\ (in (set_difference B C) T_1))))) ### Definition-Pseudo(cup_closed) 10 % 3.16/3.35 12. (in T_3 T_1) (-. (in T_3 T_1)) ### Axiom % 3.16/3.35 13. (in T_4 T_1) (-. (in T_4 T_1)) ### Axiom % 3.16/3.35 14. (-. (in (set_difference T_3 T_4) T_1)) (in (set_difference T_3 T_4) T_1) ### Axiom % 3.16/3.35 15. ((in (set_union2 T_3 T_4) T_1) /\ (in (set_difference T_3 T_4) T_1)) (-. (in (set_difference T_3 T_4) T_1)) ### And 14 % 3.16/3.35 16. (((in T_3 T_1) /\ (in T_4 T_1)) => ((in (set_union2 T_3 T_4) T_1) /\ (in (set_difference T_3 T_4) T_1))) (-. (in (set_difference T_3 T_4) T_1)) (in T_4 T_1) (in T_3 T_1) ### DisjTree 12 13 15 % 3.16/3.35 17. (All C, (((in T_3 T_1) /\ (in C T_1)) => ((in (set_union2 T_3 C) T_1) /\ (in (set_difference T_3 C) T_1)))) (in T_3 T_1) (in T_4 T_1) (-. (in (set_difference T_3 T_4) T_1)) ### All 16 % 3.16/3.35 18. (All B, (All C, (((in B T_1) /\ (in C T_1)) => ((in (set_union2 B C) T_1) /\ (in (set_difference B C) T_1))))) (-. (in (set_difference T_3 T_4) T_1)) (in T_4 T_1) (in T_3 T_1) ### All 17 % 3.16/3.35 19. (-. (((in T_3 T_1) /\ (in T_4 T_1)) => (in (set_difference T_3 T_4) T_1))) (All B, (All C, (((in B T_1) /\ (in C T_1)) => ((in (set_union2 B C) T_1) /\ (in (set_difference B C) T_1))))) ### ConjTree 18 % 3.16/3.35 20. (-. (All C, (((in T_3 T_1) /\ (in C T_1)) => (in (set_difference T_3 C) T_1)))) (All B, (All C, (((in B T_1) /\ (in C T_1)) => ((in (set_union2 B C) T_1) /\ (in (set_difference B C) T_1))))) ### NotAllEx 19 % 3.16/3.35 21. (-. (All B, (All C, (((in B T_1) /\ (in C T_1)) => (in (set_difference B C) T_1))))) (All B, (All C, (((in B T_1) /\ (in C T_1)) => ((in (set_union2 B C) T_1) /\ (in (set_difference B C) T_1))))) ### NotAllEx 20 % 3.16/3.35 22. (-. (diff_closed T_1)) (All B, (All C, (((in B T_1) /\ (in C T_1)) => ((in (set_union2 B C) T_1) /\ (in (set_difference B C) T_1))))) ### Definition-Pseudo(diff_closed) 21 % 3.16/3.35 23. (-. ((cup_closed T_1) /\ (diff_closed T_1))) (All B, (All C, (((in B T_1) /\ (in C T_1)) => ((in (set_union2 B C) T_1) /\ (in (set_difference B C) T_1))))) ### NotAnd 11 22 % 3.16/3.35 24. (-. (preboolean T_1)) (All B, (All C, (((in B T_1) /\ (in C T_1)) => ((in (set_union2 B C) T_1) /\ (in (set_difference B C) T_1))))) ### Definition-Pseudo(preboolean) 23 % 3.16/3.35 25. (in T_5 T_1) (-. (in T_5 T_1)) ### Axiom % 3.16/3.35 26. (in T_6 T_1) (-. (in T_6 T_1)) ### Axiom % 3.16/3.35 27. (-. (in (set_union2 T_5 T_6) T_1)) (in (set_union2 T_5 T_6) T_1) ### Axiom % 3.16/3.35 28. (((in T_5 T_1) /\ (in T_6 T_1)) => (in (set_union2 T_5 T_6) T_1)) (-. (in (set_union2 T_5 T_6) T_1)) (in T_6 T_1) (in T_5 T_1) ### DisjTree 25 26 27 % 3.16/3.35 29. (All C, (((in T_5 T_1) /\ (in C T_1)) => (in (set_union2 T_5 C) T_1))) (in T_5 T_1) (in T_6 T_1) (-. (in (set_union2 T_5 T_6) T_1)) ### All 28 % 3.16/3.35 30. (All B, (All C, (((in B T_1) /\ (in C T_1)) => (in (set_union2 B C) T_1)))) (-. (in (set_union2 T_5 T_6) T_1)) (in T_6 T_1) (in T_5 T_1) ### All 29 % 3.16/3.35 31. (in T_5 T_1) (-. (in T_5 T_1)) ### Axiom % 3.16/3.35 32. (in T_6 T_1) (-. (in T_6 T_1)) ### Axiom % 3.16/3.35 33. (-. (in (set_difference T_5 T_6) T_1)) (in (set_difference T_5 T_6) T_1) ### Axiom % 3.16/3.35 34. (((in T_5 T_1) /\ (in T_6 T_1)) => (in (set_difference T_5 T_6) T_1)) (-. (in (set_difference T_5 T_6) T_1)) (in T_6 T_1) (in T_5 T_1) ### DisjTree 31 32 33 % 3.16/3.35 35. (All C, (((in T_5 T_1) /\ (in C T_1)) => (in (set_difference T_5 C) T_1))) (in T_5 T_1) (in T_6 T_1) (-. (in (set_difference T_5 T_6) T_1)) ### All 34 % 3.16/3.35 36. (All B, (All C, (((in B T_1) /\ (in C T_1)) => (in (set_difference B C) T_1)))) (-. (in (set_difference T_5 T_6) T_1)) (in T_6 T_1) (in T_5 T_1) ### All 35 % 3.16/3.35 37. (-. ((in (set_union2 T_5 T_6) T_1) /\ (in (set_difference T_5 T_6) T_1))) (All B, (All C, (((in B T_1) /\ (in C T_1)) => (in (set_difference B C) T_1)))) (in T_5 T_1) (in T_6 T_1) (All B, (All C, (((in B T_1) /\ (in C T_1)) => (in (set_union2 B C) T_1)))) ### NotAnd 30 36 % 3.16/3.35 38. (-. (((in T_5 T_1) /\ (in T_6 T_1)) => ((in (set_union2 T_5 T_6) T_1) /\ (in (set_difference T_5 T_6) T_1)))) (All B, (All C, (((in B T_1) /\ (in C T_1)) => (in (set_union2 B C) T_1)))) (All B, (All C, (((in B T_1) /\ (in C T_1)) => (in (set_difference B C) T_1)))) ### ConjTree 37 % 3.16/3.35 39. (-. (All C, (((in T_5 T_1) /\ (in C T_1)) => ((in (set_union2 T_5 C) T_1) /\ (in (set_difference T_5 C) T_1))))) (All B, (All C, (((in B T_1) /\ (in C T_1)) => (in (set_difference B C) T_1)))) (All B, (All C, (((in B T_1) /\ (in C T_1)) => (in (set_union2 B C) T_1)))) ### NotAllEx 38 % 3.16/3.35 40. (-. (All B, (All C, (((in B T_1) /\ (in C T_1)) => ((in (set_union2 B C) T_1) /\ (in (set_difference B C) T_1)))))) (All B, (All C, (((in B T_1) /\ (in C T_1)) => (in (set_union2 B C) T_1)))) (All B, (All C, (((in B T_1) /\ (in C T_1)) => (in (set_difference B C) T_1)))) ### NotAllEx 39 % 3.16/3.35 41. (diff_closed T_1) (All B, (All C, (((in B T_1) /\ (in C T_1)) => (in (set_union2 B C) T_1)))) (-. (All B, (All C, (((in B T_1) /\ (in C T_1)) => ((in (set_union2 B C) T_1) /\ (in (set_difference B C) T_1)))))) ### Definition-Pseudo(diff_closed) 40 % 3.16/3.35 42. (cup_closed T_1) (-. (All B, (All C, (((in B T_1) /\ (in C T_1)) => ((in (set_union2 B C) T_1) /\ (in (set_difference B C) T_1)))))) (diff_closed T_1) ### Definition-Pseudo(cup_closed) 41 % 3.16/3.35 43. ((cup_closed T_1) /\ (diff_closed T_1)) (-. (All B, (All C, (((in B T_1) /\ (in C T_1)) => ((in (set_union2 B C) T_1) /\ (in (set_difference B C) T_1)))))) ### And 42 % 3.16/3.35 44. (preboolean T_1) (-. (All B, (All C, (((in B T_1) /\ (in C T_1)) => ((in (set_union2 B C) T_1) /\ (in (set_difference B C) T_1)))))) ### Definition-Pseudo(preboolean) 43 % 3.16/3.35 45. (-. ((preboolean T_1) <=> (All B, (All C, (((in B T_1) /\ (in C T_1)) => ((in (set_union2 B C) T_1) /\ (in (set_difference B C) T_1))))))) ### NotEquiv 24 44 % 3.16/3.35 46. (-. (All A, ((preboolean A) <=> (All B, (All C, (((in B A) /\ (in C A)) => ((in (set_union2 B C) A) /\ (in (set_difference B C) A)))))))) ### NotAllEx 45 % 3.16/3.35 % SZS output end Proof % 3.16/3.35 (* END-PROOF *) %------------------------------------------------------------------------------