%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : PUZ047+1 : TPTP v8.1.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n021.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 18:27:50 EDT 2022 % Result : Theorem 14.71s 14.89s % Output : Proof 14.71s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : PUZ047+1 : TPTP v8.1.0. Released v2.5.0. % 0.06/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.11/0.33 % Computer : n021.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 600 % 0.11/0.33 % DateTime : Sun May 29 01:08:12 EDT 2022 % 0.11/0.33 % CPUTime : % 14.71/14.89 % SZS status Theorem % 14.71/14.89 (* PROOF-FOUND *) % 14.71/14.89 (* BEGIN-PROOF *) % 14.71/14.89 % SZS output start Proof % 14.71/14.89 1. (p (south) (south) (south) (south) (start)) (-. (p (south) (south) (south) (south) (start))) ### Axiom % 14.71/14.89 2. (p (north) (south) (north) (south) (take_goat (start))) (-. (p (north) (south) (north) (south) (take_goat (start)))) ### Axiom % 14.71/14.89 3. (p (south) (south) (north) (south) (go_alone (take_goat (start)))) (-. (p (south) (south) (north) (south) (go_alone (take_goat (start))))) ### Axiom % 14.71/14.89 4. (p (north) (south) (north) (north) (take_cabbage (go_alone (take_goat (start))))) (-. (p (north) (south) (north) (north) (take_cabbage (go_alone (take_goat (start)))))) ### Axiom % 14.71/14.89 5. (p (south) (south) (south) (north) (take_goat (take_cabbage (go_alone (take_goat (start)))))) (-. (p (south) (south) (south) (north) (take_goat (take_cabbage (go_alone (take_goat (start))))))) ### Axiom % 14.71/14.89 6. (p (north) (north) (south) (north) (take_wolf (take_goat (take_cabbage (go_alone (take_goat (start))))))) (-. (p (north) (north) (south) (north) (take_wolf (take_goat (take_cabbage (go_alone (take_goat (start)))))))) ### Axiom % 14.71/14.89 7. (p (south) (north) (south) (north) (go_alone (take_wolf (take_goat (take_cabbage (go_alone (take_goat (start)))))))) (-. (p (south) (north) (south) (north) (go_alone (take_wolf (take_goat (take_cabbage (go_alone (take_goat (start))))))))) ### Axiom % 14.71/14.89 8. (p (north) (north) (north) (north) (take_goat (go_alone (take_wolf (take_goat (take_cabbage (go_alone (take_goat (start))))))))) (-. (p (north) (north) (north) (north) (take_goat (go_alone (take_wolf (take_goat (take_cabbage (go_alone (take_goat (start)))))))))) ### Axiom % 14.71/14.89 9. (-. (Ex Z, (p (north) (north) (north) (north) Z))) (p (north) (north) (north) (north) (take_goat (go_alone (take_wolf (take_goat (take_cabbage (go_alone (take_goat (start))))))))) ### NotExists 8 % 14.71/14.89 10. ((p (south) (north) (south) (north) (go_alone (take_wolf (take_goat (take_cabbage (go_alone (take_goat (start)))))))) => (p (north) (north) (north) (north) (take_goat (go_alone (take_wolf (take_goat (take_cabbage (go_alone (take_goat (start)))))))))) (-. (Ex Z, (p (north) (north) (north) (north) Z))) (p (south) (north) (south) (north) (go_alone (take_wolf (take_goat (take_cabbage (go_alone (take_goat (start)))))))) ### Imply 7 9 % 14.71/14.89 11. (All U, ((p (south) (north) (south) (north) U) => (p (north) (north) (north) (north) (take_goat U)))) (p (south) (north) (south) (north) (go_alone (take_wolf (take_goat (take_cabbage (go_alone (take_goat (start)))))))) (-. (Ex Z, (p (north) (north) (north) (north) Z))) ### All 10 % 14.71/14.89 12. ((p (north) (north) (south) (north) (take_wolf (take_goat (take_cabbage (go_alone (take_goat (start))))))) => (p (south) (north) (south) (north) (go_alone (take_wolf (take_goat (take_cabbage (go_alone (take_goat (start))))))))) (-. (Ex Z, (p (north) (north) (north) (north) Z))) (All U, ((p (south) (north) (south) (north) U) => (p (north) (north) (north) (north) (take_goat U)))) (p (north) (north) (south) (north) (take_wolf (take_goat (take_cabbage (go_alone (take_goat (start))))))) ### Imply 6 11 % 14.71/14.89 13. (All T1, ((p (north) (north) (south) (north) T1) => (p (south) (north) (south) (north) (go_alone T1)))) (p (north) (north) (south) (north) (take_wolf (take_goat (take_cabbage (go_alone (take_goat (start))))))) (All U, ((p (south) (north) (south) (north) U) => (p (north) (north) (north) (north) (take_goat U)))) (-. (Ex Z, (p (north) (north) (north) (north) Z))) ### All 12 % 14.71/14.89 14. ((p (south) (south) (south) (north) (take_goat (take_cabbage (go_alone (take_goat (start)))))) => (p (north) (north) (south) (north) (take_wolf (take_goat (take_cabbage (go_alone (take_goat (start)))))))) (-. (Ex Z, (p (north) (north) (north) (north) Z))) (All U, ((p (south) (north) (south) (north) U) => (p (north) (north) (north) (north) (take_goat U)))) (All T1, ((p (north) (north) (south) (north) T1) => (p (south) (north) (south) (north) (go_alone T1)))) (p (south) (south) (south) (north) (take_goat (take_cabbage (go_alone (take_goat (start)))))) ### Imply 5 13 % 14.71/14.89 15. (All T4, ((p (south) (south) (south) (north) T4) => (p (north) (north) (south) (north) (take_wolf T4)))) (p (south) (south) (south) (north) (take_goat (take_cabbage (go_alone (take_goat (start)))))) (All T1, ((p (north) (north) (south) (north) T1) => (p (south) (north) (south) (north) (go_alone T1)))) (All U, ((p (south) (north) (south) (north) U) => (p (north) (north) (north) (north) (take_goat U)))) (-. (Ex Z, (p (north) (north) (north) (north) Z))) ### All 14 % 14.71/14.89 16. ((p (north) (south) (north) (north) (take_cabbage (go_alone (take_goat (start))))) => (p (south) (south) (south) (north) (take_goat (take_cabbage (go_alone (take_goat (start))))))) (-. (Ex Z, (p (north) (north) (north) (north) Z))) (All U, ((p (south) (north) (south) (north) U) => (p (north) (north) (north) (north) (take_goat U)))) (All T1, ((p (north) (north) (south) (north) T1) => (p (south) (north) (south) (north) (go_alone T1)))) (All T4, ((p (south) (south) (south) (north) T4) => (p (north) (north) (south) (north) (take_wolf T4)))) (p (north) (south) (north) (north) (take_cabbage (go_alone (take_goat (start))))) ### Imply 4 15 % 14.71/14.89 17. (All V, ((p (north) (south) (north) (north) V) => (p (south) (south) (south) (north) (take_goat V)))) (p (north) (south) (north) (north) (take_cabbage (go_alone (take_goat (start))))) (All T4, ((p (south) (south) (south) (north) T4) => (p (north) (north) (south) (north) (take_wolf T4)))) (All T1, ((p (north) (north) (south) (north) T1) => (p (south) (north) (south) (north) (go_alone T1)))) (All U, ((p (south) (north) (south) (north) U) => (p (north) (north) (north) (north) (take_goat U)))) (-. (Ex Z, (p (north) (north) (north) (north) Z))) ### All 16 % 14.71/14.89 18. ((p (south) (south) (north) (south) (go_alone (take_goat (start)))) => (p (north) (south) (north) (north) (take_cabbage (go_alone (take_goat (start)))))) (-. (Ex Z, (p (north) (north) (north) (north) Z))) (All U, ((p (south) (north) (south) (north) U) => (p (north) (north) (north) (north) (take_goat U)))) (All T1, ((p (north) (north) (south) (north) T1) => (p (south) (north) (south) (north) (go_alone T1)))) (All T4, ((p (south) (south) (south) (north) T4) => (p (north) (north) (south) (north) (take_wolf T4)))) (All V, ((p (north) (south) (north) (north) V) => (p (south) (south) (south) (north) (take_goat V)))) (p (south) (south) (north) (south) (go_alone (take_goat (start)))) ### Imply 3 17 % 14.71/14.89 19. (All U1, ((p (south) (south) (north) (south) U1) => (p (north) (south) (north) (north) (take_cabbage U1)))) (p (south) (south) (north) (south) (go_alone (take_goat (start)))) (All V, ((p (north) (south) (north) (north) V) => (p (south) (south) (south) (north) (take_goat V)))) (All T4, ((p (south) (south) (south) (north) T4) => (p (north) (north) (south) (north) (take_wolf T4)))) (All T1, ((p (north) (north) (south) (north) T1) => (p (south) (north) (south) (north) (go_alone T1)))) (All U, ((p (south) (north) (south) (north) U) => (p (north) (north) (north) (north) (take_goat U)))) (-. (Ex Z, (p (north) (north) (north) (north) Z))) ### All 18 % 14.71/14.89 20. ((p (north) (south) (north) (south) (take_goat (start))) => (p (south) (south) (north) (south) (go_alone (take_goat (start))))) (-. (Ex Z, (p (north) (north) (north) (north) Z))) (All U, ((p (south) (north) (south) (north) U) => (p (north) (north) (north) (north) (take_goat U)))) (All T1, ((p (north) (north) (south) (north) T1) => (p (south) (north) (south) (north) (go_alone T1)))) (All T4, ((p (south) (south) (south) (north) T4) => (p (north) (north) (south) (north) (take_wolf T4)))) (All V, ((p (north) (south) (north) (north) V) => (p (south) (south) (south) (north) (take_goat V)))) (All U1, ((p (south) (south) (north) (south) U1) => (p (north) (south) (north) (north) (take_cabbage U1)))) (p (north) (south) (north) (south) (take_goat (start))) ### Imply 2 19 % 14.71/14.89 21. (All T3, ((p (north) (south) (north) (south) T3) => (p (south) (south) (north) (south) (go_alone T3)))) (p (north) (south) (north) (south) (take_goat (start))) (All U1, ((p (south) (south) (north) (south) U1) => (p (north) (south) (north) (north) (take_cabbage U1)))) (All V, ((p (north) (south) (north) (north) V) => (p (south) (south) (south) (north) (take_goat V)))) (All T4, ((p (south) (south) (south) (north) T4) => (p (north) (north) (south) (north) (take_wolf T4)))) (All T1, ((p (north) (north) (south) (north) T1) => (p (south) (north) (south) (north) (go_alone T1)))) (All U, ((p (south) (north) (south) (north) U) => (p (north) (north) (north) (north) (take_goat U)))) (-. (Ex Z, (p (north) (north) (north) (north) Z))) ### All 20 % 14.71/14.89 22. ((p (south) (south) (south) (south) (start)) => (p (north) (south) (north) (south) (take_goat (start)))) (-. (Ex Z, (p (north) (north) (north) (north) Z))) (All U, ((p (south) (north) (south) (north) U) => (p (north) (north) (north) (north) (take_goat U)))) (All T1, ((p (north) (north) (south) (north) T1) => (p (south) (north) (south) (north) (go_alone T1)))) (All T4, ((p (south) (south) (south) (north) T4) => (p (north) (north) (south) (north) (take_wolf T4)))) (All V, ((p (north) (south) (north) (north) V) => (p (south) (south) (south) (north) (take_goat V)))) (All U1, ((p (south) (south) (north) (south) U1) => (p (north) (south) (north) (north) (take_cabbage U1)))) (All T3, ((p (north) (south) (north) (south) T3) => (p (south) (south) (north) (south) (go_alone T3)))) (p (south) (south) (south) (south) (start)) ### Imply 1 21 % 14.71/14.89 23. (All U, ((p (south) (south) (south) (south) U) => (p (north) (south) (north) (south) (take_goat U)))) (p (south) (south) (south) (south) (start)) (All T3, ((p (north) (south) (north) (south) T3) => (p (south) (south) (north) (south) (go_alone T3)))) (All U1, ((p (south) (south) (north) (south) U1) => (p (north) (south) (north) (north) (take_cabbage U1)))) (All V, ((p (north) (south) (north) (north) V) => (p (south) (south) (south) (north) (take_goat V)))) (All T4, ((p (south) (south) (south) (north) T4) => (p (north) (north) (south) (north) (take_wolf T4)))) (All T1, ((p (north) (north) (south) (north) T1) => (p (south) (north) (south) (north) (go_alone T1)))) (All U, ((p (south) (north) (south) (north) U) => (p (north) (north) (north) (north) (take_goat U)))) (-. (Ex Z, (p (north) (north) (north) (north) Z))) ### All 22 % 14.71/14.89 24. (All Y, (All U, ((p (south) (south) (south) Y U) => (p (north) (south) (north) Y (take_goat U))))) (-. (Ex Z, (p (north) (north) (north) (north) Z))) (All U, ((p (south) (north) (south) (north) U) => (p (north) (north) (north) (north) (take_goat U)))) (All T1, ((p (north) (north) (south) (north) T1) => (p (south) (north) (south) (north) (go_alone T1)))) (All T4, ((p (south) (south) (south) (north) T4) => (p (north) (north) (south) (north) (take_wolf T4)))) (All V, ((p (north) (south) (north) (north) V) => (p (south) (south) (south) (north) (take_goat V)))) (All U1, ((p (south) (south) (north) (south) U1) => (p (north) (south) (north) (north) (take_cabbage U1)))) (All T3, ((p (north) (south) (north) (south) T3) => (p (south) (south) (north) (south) (go_alone T3)))) (p (south) (south) (south) (south) (start)) ### All 23 % 14.71/14.89 25. (All X, (All Y, (All U, ((p (south) X (south) Y U) => (p (north) X (north) Y (take_goat U)))))) (p (south) (south) (south) (south) (start)) (All T3, ((p (north) (south) (north) (south) T3) => (p (south) (south) (north) (south) (go_alone T3)))) (All U1, ((p (south) (south) (north) (south) U1) => (p (north) (south) (north) (north) (take_cabbage U1)))) (All V, ((p (north) (south) (north) (north) V) => (p (south) (south) (south) (north) (take_goat V)))) (All T4, ((p (south) (south) (south) (north) T4) => (p (north) (north) (south) (north) (take_wolf T4)))) (All T1, ((p (north) (north) (south) (north) T1) => (p (south) (north) (south) (north) (go_alone T1)))) (All U, ((p (south) (north) (south) (north) U) => (p (north) (north) (north) (north) (take_goat U)))) (-. (Ex Z, (p (north) (north) (north) (north) Z))) ### All 24 % 14.71/14.89 26. (All Y1, (All V, ((p (north) (south) (north) Y1 V) => (p (south) (south) (south) Y1 (take_goat V))))) (-. (Ex Z, (p (north) (north) (north) (north) Z))) (All U, ((p (south) (north) (south) (north) U) => (p (north) (north) (north) (north) (take_goat U)))) (All T1, ((p (north) (north) (south) (north) T1) => (p (south) (north) (south) (north) (go_alone T1)))) (All T4, ((p (south) (south) (south) (north) T4) => (p (north) (north) (south) (north) (take_wolf T4)))) (All U1, ((p (south) (south) (north) (south) U1) => (p (north) (south) (north) (north) (take_cabbage U1)))) (All T3, ((p (north) (south) (north) (south) T3) => (p (south) (south) (north) (south) (go_alone T3)))) (p (south) (south) (south) (south) (start)) (All X, (All Y, (All U, ((p (south) X (south) Y U) => (p (north) X (north) Y (take_goat U)))))) ### All 25 % 14.71/14.89 27. (All X1, (All Y1, (All V, ((p (north) X1 (north) Y1 V) => (p (south) X1 (south) Y1 (take_goat V)))))) (All X, (All Y, (All U, ((p (south) X (south) Y U) => (p (north) X (north) Y (take_goat U)))))) (p (south) (south) (south) (south) (start)) (All T3, ((p (north) (south) (north) (south) T3) => (p (south) (south) (north) (south) (go_alone T3)))) (All U1, ((p (south) (south) (north) (south) U1) => (p (north) (south) (north) (north) (take_cabbage U1)))) (All T4, ((p (south) (south) (south) (north) T4) => (p (north) (north) (south) (north) (take_wolf T4)))) (All T1, ((p (north) (north) (south) (north) T1) => (p (south) (north) (south) (north) (go_alone T1)))) (All U, ((p (south) (north) (south) (north) U) => (p (north) (north) (north) (north) (take_goat U)))) (-. (Ex Z, (p (north) (north) (north) (north) Z))) ### All 26 % 14.71/14.89 28. (All Y, (All U, ((p (south) (north) (south) Y U) => (p (north) (north) (north) Y (take_goat U))))) (-. (Ex Z, (p (north) (north) (north) (north) Z))) (All T1, ((p (north) (north) (south) (north) T1) => (p (south) (north) (south) (north) (go_alone T1)))) (All T4, ((p (south) (south) (south) (north) T4) => (p (north) (north) (south) (north) (take_wolf T4)))) (All U1, ((p (south) (south) (north) (south) U1) => (p (north) (south) (north) (north) (take_cabbage U1)))) (All T3, ((p (north) (south) (north) (south) T3) => (p (south) (south) (north) (south) (go_alone T3)))) (p (south) (south) (south) (south) (start)) (All X, (All Y, (All U, ((p (south) X (south) Y U) => (p (north) X (north) Y (take_goat U)))))) (All X1, (All Y1, (All V, ((p (north) X1 (north) Y1 V) => (p (south) X1 (south) Y1 (take_goat V)))))) ### All 27 % 14.71/14.89 29. (All X1, (All Y1, (All V, ((p (north) X1 (north) Y1 V) => (p (south) X1 (south) Y1 (take_goat V)))))) (All X, (All Y, (All U, ((p (south) X (south) Y U) => (p (north) X (north) Y (take_goat U)))))) (p (south) (south) (south) (south) (start)) (All T3, ((p (north) (south) (north) (south) T3) => (p (south) (south) (north) (south) (go_alone T3)))) (All U1, ((p (south) (south) (north) (south) U1) => (p (north) (south) (north) (north) (take_cabbage U1)))) (All T4, ((p (south) (south) (south) (north) T4) => (p (north) (north) (south) (north) (take_wolf T4)))) (All T1, ((p (north) (north) (south) (north) T1) => (p (south) (north) (south) (north) (go_alone T1)))) (-. (Ex Z, (p (north) (north) (north) (north) Z))) ### All 28 % 14.71/14.89 30. (-. (((p (south) (south) (south) (south) (start)) /\ ((All T, ((p (south) (north) (south) (north) T) => (p (north) (north) (south) (north) (go_alone T)))) /\ ((All T1, ((p (north) (north) (south) (north) T1) => (p (south) (north) (south) (north) (go_alone T1)))) /\ ((All T2, ((p (south) (south) (north) (south) T2) => (p (north) (south) (north) (south) (go_alone T2)))) /\ ((All T3, ((p (north) (south) (north) (south) T3) => (p (south) (south) (north) (south) (go_alone T3)))) /\ ((All T4, ((p (south) (south) (south) (north) T4) => (p (north) (north) (south) (north) (take_wolf T4)))) /\ ((All T5, ((p (north) (north) (south) (north) T5) => (p (south) (south) (south) (north) (take_wolf T5)))) /\ ((All T6, ((p (south) (south) (north) (south) T6) => (p (north) (north) (north) (south) (take_wolf T6)))) /\ ((All T7, ((p (north) (north) (north) (south) T7) => (p (south) (south) (north) (south) (take_wolf T7)))) /\ ((All X, (All Y, (All U, ((p (south) X (south) Y U) => (p (north) X (north) Y (take_goat U)))))) /\ ((All X1, (All Y1, (All V, ((p (north) X1 (north) Y1 V) => (p (south) X1 (south) Y1 (take_goat V)))))) /\ ((All T8, ((p (south) (north) (south) (south) T8) => (p (north) (north) (south) (north) (take_cabbage T8)))) /\ ((All T9, ((p (north) (north) (south) (north) T9) => (p (south) (north) (south) (south) (take_cabbage T9)))) /\ ((All U1, ((p (south) (south) (north) (south) U1) => (p (north) (south) (north) (north) (take_cabbage U1)))) /\ (All V1, ((p (north) (south) (north) (north) V1) => (p (south) (south) (north) (south) (take_cabbage V1)))))))))))))))))) => (Ex Z, (p (north) (north) (north) (north) Z)))) ### ConjTree 29 % 14.71/14.90 % SZS output end Proof % 14.71/14.90 (* END-PROOF *) %------------------------------------------------------------------------------