%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : PRO009+2 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n026.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 : Mon Jul 18 17:54:13 EDT 2022 % Result : Theorem 215.07s 215.32s % Output : Proof 215.07s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : PRO009+2 : TPTP v8.1.0. Released v4.0.0. % 0.06/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n026.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 : 600 % 0.12/0.33 % DateTime : Mon Jun 13 03:33:05 EDT 2022 % 0.12/0.33 % CPUTime : % 215.07/215.32 % SZS status Theorem % 215.07/215.32 (* PROOF-FOUND *) % 215.07/215.32 (* BEGIN-PROOF *) % 215.07/215.32 % SZS output start Proof % 215.07/215.32 1. (occurrence_of T_0 (tptp0)) (-. (occurrence_of T_0 (tptp0))) ### Axiom % 215.07/215.32 2. (occurrence_of T_1 (tptp3)) (-. (occurrence_of T_1 (tptp3))) ### Axiom % 215.07/215.32 3. (Ex X34, ((occurrence_of T_0 X34) /\ ((subactivity_occurrence T_1 T_0) /\ (root T_1 X34)))) (-. (Ex X34, ((occurrence_of T_0 X34) /\ ((subactivity_occurrence T_1 T_0) /\ (root T_1 X34))))) ### Axiom % 215.07/215.32 4. (-. (root_occ T_1 T_0)) (Ex X34, ((occurrence_of T_0 X34) /\ ((subactivity_occurrence T_1 T_0) /\ (root T_1 X34)))) ### Definition-Pseudo(root_occ) 3 % 215.07/215.32 5. (occurrence_of T_2 (tptp2)) (-. (occurrence_of T_2 (tptp2))) ### Axiom % 215.07/215.32 6. (-. ((occurrence_of T_2 (tptp2)) \/ (occurrence_of T_2 (tptp1)))) (occurrence_of T_2 (tptp2)) ### NotOr 5 % 215.07/215.32 7. (min_precedes T_1 T_3 (tptp0)) (-. (min_precedes T_1 T_3 (tptp0))) ### Axiom % 215.07/215.32 8. (min_precedes T_3 T_2 (tptp0)) (-. (min_precedes T_3 T_2 (tptp0))) ### Axiom % 215.07/215.32 9. (-. (min_precedes T_1 T_2 (tptp0))) (min_precedes T_1 T_2 (tptp0)) ### Axiom % 215.07/215.32 10. (((min_precedes T_1 T_3 (tptp0)) /\ (min_precedes T_3 T_2 (tptp0))) => (min_precedes T_1 T_2 (tptp0))) (-. (min_precedes T_1 T_2 (tptp0))) (min_precedes T_3 T_2 (tptp0)) (min_precedes T_1 T_3 (tptp0)) ### DisjTree 7 8 9 % 215.07/215.32 11. (All X3, (((min_precedes T_1 T_3 X3) /\ (min_precedes T_3 T_2 X3)) => (min_precedes T_1 T_2 X3))) (min_precedes T_1 T_3 (tptp0)) (min_precedes T_3 T_2 (tptp0)) (-. (min_precedes T_1 T_2 (tptp0))) ### All 10 % 215.07/215.32 12. (All X2, (All X3, (((min_precedes T_1 T_3 X3) /\ (min_precedes T_3 X2 X3)) => (min_precedes T_1 X2 X3)))) (-. (min_precedes T_1 T_2 (tptp0))) (min_precedes T_3 T_2 (tptp0)) (min_precedes T_1 T_3 (tptp0)) ### All 11 % 215.07/215.32 13. (All X1, (All X2, (All X3, (((min_precedes T_1 X1 X3) /\ (min_precedes X1 X2 X3)) => (min_precedes T_1 X2 X3))))) (min_precedes T_1 T_3 (tptp0)) (min_precedes T_3 T_2 (tptp0)) (-. (min_precedes T_1 T_2 (tptp0))) ### All 12 % 215.07/215.32 14. (All X0, (All X1, (All X2, (All X3, (((min_precedes X0 X1 X3) /\ (min_precedes X1 X2 X3)) => (min_precedes X0 X2 X3)))))) (-. (min_precedes T_1 T_2 (tptp0))) (min_precedes T_3 T_2 (tptp0)) (min_precedes T_1 T_3 (tptp0)) ### All 13 % 215.07/215.32 15. (Ex X37, ((occurrence_of T_0 X37) /\ ((subactivity_occurrence T_2 T_0) /\ (leaf T_2 X37)))) (-. (Ex X37, ((occurrence_of T_0 X37) /\ ((subactivity_occurrence T_2 T_0) /\ (leaf T_2 X37))))) ### Axiom % 215.07/215.32 16. (-. (leaf_occ T_2 T_0)) (Ex X37, ((occurrence_of T_0 X37) /\ ((subactivity_occurrence T_2 T_0) /\ (leaf T_2 X37)))) ### Definition-Pseudo(leaf_occ) 15 % 215.07/215.32 17. (-. ((occurrence_of T_1 (tptp3)) /\ ((root_occ T_1 T_0) /\ (((occurrence_of T_2 (tptp2)) \/ (occurrence_of T_2 (tptp1))) /\ ((min_precedes T_1 T_2 (tptp0)) /\ (leaf_occ T_2 T_0)))))) (Ex X37, ((occurrence_of T_0 X37) /\ ((subactivity_occurrence T_2 T_0) /\ (leaf T_2 X37)))) (min_precedes T_1 T_3 (tptp0)) (min_precedes T_3 T_2 (tptp0)) (All X0, (All X1, (All X2, (All X3, (((min_precedes X0 X1 X3) /\ (min_precedes X1 X2 X3)) => (min_precedes X0 X2 X3)))))) (occurrence_of T_2 (tptp2)) (Ex X34, ((occurrence_of T_0 X34) /\ ((subactivity_occurrence T_1 T_0) /\ (root T_1 X34)))) (occurrence_of T_1 (tptp3)) ### DisjTree 2 4 6 14 16 % 215.07/215.32 18. (-. (Ex X101, ((occurrence_of T_1 (tptp3)) /\ ((root_occ T_1 T_0) /\ (((occurrence_of X101 (tptp2)) \/ (occurrence_of X101 (tptp1))) /\ ((min_precedes T_1 X101 (tptp0)) /\ (leaf_occ X101 T_0))))))) (occurrence_of T_1 (tptp3)) (Ex X34, ((occurrence_of T_0 X34) /\ ((subactivity_occurrence T_1 T_0) /\ (root T_1 X34)))) (occurrence_of T_2 (tptp2)) (All X0, (All X1, (All X2, (All X3, (((min_precedes X0 X1 X3) /\ (min_precedes X1 X2 X3)) => (min_precedes X0 X2 X3)))))) (min_precedes T_3 T_2 (tptp0)) (min_precedes T_1 T_3 (tptp0)) (Ex X37, ((occurrence_of T_0 X37) /\ ((subactivity_occurrence T_2 T_0) /\ (leaf T_2 X37)))) ### NotExists 17 % 215.07/215.32 19. (-. (Ex X100, (Ex X101, ((occurrence_of X100 (tptp3)) /\ ((root_occ X100 T_0) /\ (((occurrence_of X101 (tptp2)) \/ (occurrence_of X101 (tptp1))) /\ ((min_precedes X100 X101 (tptp0)) /\ (leaf_occ X101 T_0)))))))) (Ex X37, ((occurrence_of T_0 X37) /\ ((subactivity_occurrence T_2 T_0) /\ (leaf T_2 X37)))) (min_precedes T_1 T_3 (tptp0)) (min_precedes T_3 T_2 (tptp0)) (All X0, (All X1, (All X2, (All X3, (((min_precedes X0 X1 X3) /\ (min_precedes X1 X2 X3)) => (min_precedes X0 X2 X3)))))) (occurrence_of T_2 (tptp2)) (Ex X34, ((occurrence_of T_0 X34) /\ ((subactivity_occurrence T_1 T_0) /\ (root T_1 X34)))) (occurrence_of T_1 (tptp3)) ### NotExists 18 % 215.07/215.32 20. (occurrence_of T_1 (tptp3)) (-. (occurrence_of T_1 (tptp3))) ### Axiom % 215.07/215.32 21. (occurrence_of T_2 (tptp1)) (-. (occurrence_of T_2 (tptp1))) ### Axiom % 215.07/215.32 22. (-. ((occurrence_of T_2 (tptp2)) \/ (occurrence_of T_2 (tptp1)))) (occurrence_of T_2 (tptp1)) ### NotOr 21 % 215.07/215.32 23. (-. ((occurrence_of T_1 (tptp3)) /\ ((root_occ T_1 T_0) /\ (((occurrence_of T_2 (tptp2)) \/ (occurrence_of T_2 (tptp1))) /\ ((min_precedes T_1 T_2 (tptp0)) /\ (leaf_occ T_2 T_0)))))) (Ex X37, ((occurrence_of T_0 X37) /\ ((subactivity_occurrence T_2 T_0) /\ (leaf T_2 X37)))) (min_precedes T_1 T_3 (tptp0)) (min_precedes T_3 T_2 (tptp0)) (All X0, (All X1, (All X2, (All X3, (((min_precedes X0 X1 X3) /\ (min_precedes X1 X2 X3)) => (min_precedes X0 X2 X3)))))) (occurrence_of T_2 (tptp1)) (Ex X34, ((occurrence_of T_0 X34) /\ ((subactivity_occurrence T_1 T_0) /\ (root T_1 X34)))) (occurrence_of T_1 (tptp3)) ### DisjTree 20 4 22 14 16 % 215.07/215.32 24. (-. (Ex X101, ((occurrence_of T_1 (tptp3)) /\ ((root_occ T_1 T_0) /\ (((occurrence_of X101 (tptp2)) \/ (occurrence_of X101 (tptp1))) /\ ((min_precedes T_1 X101 (tptp0)) /\ (leaf_occ X101 T_0))))))) (occurrence_of T_1 (tptp3)) (Ex X34, ((occurrence_of T_0 X34) /\ ((subactivity_occurrence T_1 T_0) /\ (root T_1 X34)))) (occurrence_of T_2 (tptp1)) (All X0, (All X1, (All X2, (All X3, (((min_precedes X0 X1 X3) /\ (min_precedes X1 X2 X3)) => (min_precedes X0 X2 X3)))))) (min_precedes T_3 T_2 (tptp0)) (min_precedes T_1 T_3 (tptp0)) (Ex X37, ((occurrence_of T_0 X37) /\ ((subactivity_occurrence T_2 T_0) /\ (leaf T_2 X37)))) ### NotExists 23 % 215.07/215.32 25. (-. (Ex X100, (Ex X101, ((occurrence_of X100 (tptp3)) /\ ((root_occ X100 T_0) /\ (((occurrence_of X101 (tptp2)) \/ (occurrence_of X101 (tptp1))) /\ ((min_precedes X100 X101 (tptp0)) /\ (leaf_occ X101 T_0)))))))) (Ex X37, ((occurrence_of T_0 X37) /\ ((subactivity_occurrence T_2 T_0) /\ (leaf T_2 X37)))) (min_precedes T_1 T_3 (tptp0)) (min_precedes T_3 T_2 (tptp0)) (All X0, (All X1, (All X2, (All X3, (((min_precedes X0 X1 X3) /\ (min_precedes X1 X2 X3)) => (min_precedes X0 X2 X3)))))) (occurrence_of T_2 (tptp1)) (Ex X34, ((occurrence_of T_0 X34) /\ ((subactivity_occurrence T_1 T_0) /\ (root T_1 X34)))) (occurrence_of T_1 (tptp3)) ### NotExists 24 % 215.07/215.32 26. ((occurrence_of T_2 (tptp2)) \/ (occurrence_of T_2 (tptp1))) (occurrence_of T_1 (tptp3)) (Ex X34, ((occurrence_of T_0 X34) /\ ((subactivity_occurrence T_1 T_0) /\ (root T_1 X34)))) (All X0, (All X1, (All X2, (All X3, (((min_precedes X0 X1 X3) /\ (min_precedes X1 X2 X3)) => (min_precedes X0 X2 X3)))))) (min_precedes T_3 T_2 (tptp0)) (min_precedes T_1 T_3 (tptp0)) (Ex X37, ((occurrence_of T_0 X37) /\ ((subactivity_occurrence T_2 T_0) /\ (leaf T_2 X37)))) (-. (Ex X100, (Ex X101, ((occurrence_of X100 (tptp3)) /\ ((root_occ X100 T_0) /\ (((occurrence_of X101 (tptp2)) \/ (occurrence_of X101 (tptp1))) /\ ((min_precedes X100 X101 (tptp0)) /\ (leaf_occ X101 T_0)))))))) ### Or 19 25 % 215.07/215.32 27. (leaf_occ T_2 T_0) (-. (Ex X100, (Ex X101, ((occurrence_of X100 (tptp3)) /\ ((root_occ X100 T_0) /\ (((occurrence_of X101 (tptp2)) \/ (occurrence_of X101 (tptp1))) /\ ((min_precedes X100 X101 (tptp0)) /\ (leaf_occ X101 T_0)))))))) (min_precedes T_1 T_3 (tptp0)) (min_precedes T_3 T_2 (tptp0)) (All X0, (All X1, (All X2, (All X3, (((min_precedes X0 X1 X3) /\ (min_precedes X1 X2 X3)) => (min_precedes X0 X2 X3)))))) (Ex X34, ((occurrence_of T_0 X34) /\ ((subactivity_occurrence T_1 T_0) /\ (root T_1 X34)))) (occurrence_of T_1 (tptp3)) ((occurrence_of T_2 (tptp2)) \/ (occurrence_of T_2 (tptp1))) ### Definition-Pseudo(leaf_occ) 26 % 215.07/215.32 28. ((min_precedes T_3 T_2 (tptp0)) /\ (-. (Ex X18, ((min_precedes T_3 X18 (tptp0)) /\ (min_precedes X18 T_2 (tptp0)))))) ((occurrence_of T_2 (tptp2)) \/ (occurrence_of T_2 (tptp1))) (occurrence_of T_1 (tptp3)) (Ex X34, ((occurrence_of T_0 X34) /\ ((subactivity_occurrence T_1 T_0) /\ (root T_1 X34)))) (All X0, (All X1, (All X2, (All X3, (((min_precedes X0 X1 X3) /\ (min_precedes X1 X2 X3)) => (min_precedes X0 X2 X3)))))) (min_precedes T_1 T_3 (tptp0)) (-. (Ex X100, (Ex X101, ((occurrence_of X100 (tptp3)) /\ ((root_occ X100 T_0) /\ (((occurrence_of X101 (tptp2)) \/ (occurrence_of X101 (tptp1))) /\ ((min_precedes X100 X101 (tptp0)) /\ (leaf_occ X101 T_0)))))))) (leaf_occ T_2 T_0) ### And 27 % 215.07/215.34 29. (next_subocc T_3 T_2 (tptp0)) (leaf_occ T_2 T_0) (-. (Ex X100, (Ex X101, ((occurrence_of X100 (tptp3)) /\ ((root_occ X100 T_0) /\ (((occurrence_of X101 (tptp2)) \/ (occurrence_of X101 (tptp1))) /\ ((min_precedes X100 X101 (tptp0)) /\ (leaf_occ X101 T_0)))))))) (min_precedes T_1 T_3 (tptp0)) (All X0, (All X1, (All X2, (All X3, (((min_precedes X0 X1 X3) /\ (min_precedes X1 X2 X3)) => (min_precedes X0 X2 X3)))))) (Ex X34, ((occurrence_of T_0 X34) /\ ((subactivity_occurrence T_1 T_0) /\ (root T_1 X34)))) (occurrence_of T_1 (tptp3)) ((occurrence_of T_2 (tptp2)) \/ (occurrence_of T_2 (tptp1))) ### Definition-Pseudo(next_subocc) 28 % 215.07/215.34 30. ((min_precedes T_1 T_3 (tptp0)) /\ (-. (Ex X18, ((min_precedes T_1 X18 (tptp0)) /\ (min_precedes X18 T_3 (tptp0)))))) ((occurrence_of T_2 (tptp2)) \/ (occurrence_of T_2 (tptp1))) (occurrence_of T_1 (tptp3)) (Ex X34, ((occurrence_of T_0 X34) /\ ((subactivity_occurrence T_1 T_0) /\ (root T_1 X34)))) (All X0, (All X1, (All X2, (All X3, (((min_precedes X0 X1 X3) /\ (min_precedes X1 X2 X3)) => (min_precedes X0 X2 X3)))))) (-. (Ex X100, (Ex X101, ((occurrence_of X100 (tptp3)) /\ ((root_occ X100 T_0) /\ (((occurrence_of X101 (tptp2)) \/ (occurrence_of X101 (tptp1))) /\ ((min_precedes X100 X101 (tptp0)) /\ (leaf_occ X101 T_0)))))))) (leaf_occ T_2 T_0) (next_subocc T_3 T_2 (tptp0)) ### And 29 % 215.07/215.34 31. (next_subocc T_1 T_3 (tptp0)) (next_subocc T_3 T_2 (tptp0)) (leaf_occ T_2 T_0) (-. (Ex X100, (Ex X101, ((occurrence_of X100 (tptp3)) /\ ((root_occ X100 T_0) /\ (((occurrence_of X101 (tptp2)) \/ (occurrence_of X101 (tptp1))) /\ ((min_precedes X100 X101 (tptp0)) /\ (leaf_occ X101 T_0)))))))) (All X0, (All X1, (All X2, (All X3, (((min_precedes X0 X1 X3) /\ (min_precedes X1 X2 X3)) => (min_precedes X0 X2 X3)))))) (Ex X34, ((occurrence_of T_0 X34) /\ ((subactivity_occurrence T_1 T_0) /\ (root T_1 X34)))) (occurrence_of T_1 (tptp3)) ((occurrence_of T_2 (tptp2)) \/ (occurrence_of T_2 (tptp1))) ### Definition-Pseudo(next_subocc) 30 % 215.07/215.34 32. (root_occ T_1 T_0) ((occurrence_of T_2 (tptp2)) \/ (occurrence_of T_2 (tptp1))) (occurrence_of T_1 (tptp3)) (All X0, (All X1, (All X2, (All X3, (((min_precedes X0 X1 X3) /\ (min_precedes X1 X2 X3)) => (min_precedes X0 X2 X3)))))) (-. (Ex X100, (Ex X101, ((occurrence_of X100 (tptp3)) /\ ((root_occ X100 T_0) /\ (((occurrence_of X101 (tptp2)) \/ (occurrence_of X101 (tptp1))) /\ ((min_precedes X100 X101 (tptp0)) /\ (leaf_occ X101 T_0)))))))) (leaf_occ T_2 T_0) (next_subocc T_3 T_2 (tptp0)) (next_subocc T_1 T_3 (tptp0)) ### Definition-Pseudo(root_occ) 31 % 215.07/215.34 33. ((occurrence_of T_1 (tptp3)) /\ ((root_occ T_1 T_0) /\ ((occurrence_of T_3 (tptp4)) /\ ((next_subocc T_1 T_3 (tptp0)) /\ (((occurrence_of T_2 (tptp2)) \/ (occurrence_of T_2 (tptp1))) /\ ((next_subocc T_3 T_2 (tptp0)) /\ (leaf_occ T_2 T_0))))))) (-. (Ex X100, (Ex X101, ((occurrence_of X100 (tptp3)) /\ ((root_occ X100 T_0) /\ (((occurrence_of X101 (tptp2)) \/ (occurrence_of X101 (tptp1))) /\ ((min_precedes X100 X101 (tptp0)) /\ (leaf_occ X101 T_0)))))))) (All X0, (All X1, (All X2, (All X3, (((min_precedes X0 X1 X3) /\ (min_precedes X1 X2 X3)) => (min_precedes X0 X2 X3)))))) ### ConjTree 32 % 215.07/215.34 34. (Ex X98, ((occurrence_of T_1 (tptp3)) /\ ((root_occ T_1 T_0) /\ ((occurrence_of T_3 (tptp4)) /\ ((next_subocc T_1 T_3 (tptp0)) /\ (((occurrence_of X98 (tptp2)) \/ (occurrence_of X98 (tptp1))) /\ ((next_subocc T_3 X98 (tptp0)) /\ (leaf_occ X98 T_0)))))))) (All X0, (All X1, (All X2, (All X3, (((min_precedes X0 X1 X3) /\ (min_precedes X1 X2 X3)) => (min_precedes X0 X2 X3)))))) (-. (Ex X100, (Ex X101, ((occurrence_of X100 (tptp3)) /\ ((root_occ X100 T_0) /\ (((occurrence_of X101 (tptp2)) \/ (occurrence_of X101 (tptp1))) /\ ((min_precedes X100 X101 (tptp0)) /\ (leaf_occ X101 T_0)))))))) ### Exists 33 % 215.07/215.34 35. (Ex X97, (Ex X98, ((occurrence_of T_1 (tptp3)) /\ ((root_occ T_1 T_0) /\ ((occurrence_of X97 (tptp4)) /\ ((next_subocc T_1 X97 (tptp0)) /\ (((occurrence_of X98 (tptp2)) \/ (occurrence_of X98 (tptp1))) /\ ((next_subocc X97 X98 (tptp0)) /\ (leaf_occ X98 T_0))))))))) (-. (Ex X100, (Ex X101, ((occurrence_of X100 (tptp3)) /\ ((root_occ X100 T_0) /\ (((occurrence_of X101 (tptp2)) \/ (occurrence_of X101 (tptp1))) /\ ((min_precedes X100 X101 (tptp0)) /\ (leaf_occ X101 T_0)))))))) (All X0, (All X1, (All X2, (All X3, (((min_precedes X0 X1 X3) /\ (min_precedes X1 X2 X3)) => (min_precedes X0 X2 X3)))))) ### Exists 34 % 215.07/215.34 36. (Ex X96, (Ex X97, (Ex X98, ((occurrence_of X96 (tptp3)) /\ ((root_occ X96 T_0) /\ ((occurrence_of X97 (tptp4)) /\ ((next_subocc X96 X97 (tptp0)) /\ (((occurrence_of X98 (tptp2)) \/ (occurrence_of X98 (tptp1))) /\ ((next_subocc X97 X98 (tptp0)) /\ (leaf_occ X98 T_0)))))))))) (All X0, (All X1, (All X2, (All X3, (((min_precedes X0 X1 X3) /\ (min_precedes X1 X2 X3)) => (min_precedes X0 X2 X3)))))) (-. (Ex X100, (Ex X101, ((occurrence_of X100 (tptp3)) /\ ((root_occ X100 T_0) /\ (((occurrence_of X101 (tptp2)) \/ (occurrence_of X101 (tptp1))) /\ ((min_precedes X100 X101 (tptp0)) /\ (leaf_occ X101 T_0)))))))) ### Exists 35 % 215.07/215.34 37. ((occurrence_of T_0 (tptp0)) => (Ex X96, (Ex X97, (Ex X98, ((occurrence_of X96 (tptp3)) /\ ((root_occ X96 T_0) /\ ((occurrence_of X97 (tptp4)) /\ ((next_subocc X96 X97 (tptp0)) /\ (((occurrence_of X98 (tptp2)) \/ (occurrence_of X98 (tptp1))) /\ ((next_subocc X97 X98 (tptp0)) /\ (leaf_occ X98 T_0))))))))))) (-. (Ex X100, (Ex X101, ((occurrence_of X100 (tptp3)) /\ ((root_occ X100 T_0) /\ (((occurrence_of X101 (tptp2)) \/ (occurrence_of X101 (tptp1))) /\ ((min_precedes X100 X101 (tptp0)) /\ (leaf_occ X101 T_0)))))))) (All X0, (All X1, (All X2, (All X3, (((min_precedes X0 X1 X3) /\ (min_precedes X1 X2 X3)) => (min_precedes X0 X2 X3)))))) (occurrence_of T_0 (tptp0)) ### Imply 1 36 % 215.07/215.34 38. (All X95, ((occurrence_of X95 (tptp0)) => (Ex X96, (Ex X97, (Ex X98, ((occurrence_of X96 (tptp3)) /\ ((root_occ X96 X95) /\ ((occurrence_of X97 (tptp4)) /\ ((next_subocc X96 X97 (tptp0)) /\ (((occurrence_of X98 (tptp2)) \/ (occurrence_of X98 (tptp1))) /\ ((next_subocc X97 X98 (tptp0)) /\ (leaf_occ X98 X95)))))))))))) (occurrence_of T_0 (tptp0)) (All X0, (All X1, (All X2, (All X3, (((min_precedes X0 X1 X3) /\ (min_precedes X1 X2 X3)) => (min_precedes X0 X2 X3)))))) (-. (Ex X100, (Ex X101, ((occurrence_of X100 (tptp3)) /\ ((root_occ X100 T_0) /\ (((occurrence_of X101 (tptp2)) \/ (occurrence_of X101 (tptp1))) /\ ((min_precedes X100 X101 (tptp0)) /\ (leaf_occ X101 T_0)))))))) ### All 37 % 215.07/215.34 39. (-. ((occurrence_of T_0 (tptp0)) => (Ex X100, (Ex X101, ((occurrence_of X100 (tptp3)) /\ ((root_occ X100 T_0) /\ (((occurrence_of X101 (tptp2)) \/ (occurrence_of X101 (tptp1))) /\ ((min_precedes X100 X101 (tptp0)) /\ (leaf_occ X101 T_0))))))))) (All X0, (All X1, (All X2, (All X3, (((min_precedes X0 X1 X3) /\ (min_precedes X1 X2 X3)) => (min_precedes X0 X2 X3)))))) (All X95, ((occurrence_of X95 (tptp0)) => (Ex X96, (Ex X97, (Ex X98, ((occurrence_of X96 (tptp3)) /\ ((root_occ X96 X95) /\ ((occurrence_of X97 (tptp4)) /\ ((next_subocc X96 X97 (tptp0)) /\ (((occurrence_of X98 (tptp2)) \/ (occurrence_of X98 (tptp1))) /\ ((next_subocc X97 X98 (tptp0)) /\ (leaf_occ X98 X95)))))))))))) ### NotImply 38 % 215.07/215.34 40. (-. (All X99, ((occurrence_of X99 (tptp0)) => (Ex X100, (Ex X101, ((occurrence_of X100 (tptp3)) /\ ((root_occ X100 X99) /\ (((occurrence_of X101 (tptp2)) \/ (occurrence_of X101 (tptp1))) /\ ((min_precedes X100 X101 (tptp0)) /\ (leaf_occ X101 X99)))))))))) (All X95, ((occurrence_of X95 (tptp0)) => (Ex X96, (Ex X97, (Ex X98, ((occurrence_of X96 (tptp3)) /\ ((root_occ X96 X95) /\ ((occurrence_of X97 (tptp4)) /\ ((next_subocc X96 X97 (tptp0)) /\ (((occurrence_of X98 (tptp2)) \/ (occurrence_of X98 (tptp1))) /\ ((next_subocc X97 X98 (tptp0)) /\ (leaf_occ X98 X95)))))))))))) (All X0, (All X1, (All X2, (All X3, (((min_precedes X0 X1 X3) /\ (min_precedes X1 X2 X3)) => (min_precedes X0 X2 X3)))))) ### NotAllEx 39 % 215.07/215.34 % SZS output end Proof % 215.07/215.34 (* END-PROOF *) %------------------------------------------------------------------------------