%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : NUM301+1 : TPTP v8.1.0. Released v3.1.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n005.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 14:41:35 EDT 2022 % Result : Theorem 12.14s 12.36s % Output : Proof 12.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : NUM301+1 : TPTP v8.1.0. Released v3.1.0. % 0.06/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n005.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 : Fri Jul 8 02:18:07 EDT 2022 % 0.12/0.33 % CPUTime : % 12.14/12.36 % SZS status Theorem % 12.14/12.36 (* PROOF-FOUND *) % 12.14/12.36 (* BEGIN-PROOF *) % 12.14/12.36 % SZS output start Proof % 12.14/12.36 1. (rdn_positive_less (rdnn (n3)) (rdnn (n4))) (-. (rdn_positive_less (rdnn (n3)) (rdnn (n4)))) ### Axiom % 12.14/12.36 2. (rdn_positive_less (rdnn (n4)) (rdnn (n5))) (-. (rdn_positive_less (rdnn (n4)) (rdnn (n5)))) ### Axiom % 12.14/12.36 3. (-. (rdn_positive_less (rdnn (n3)) (rdnn (n5)))) (rdn_positive_less (rdnn (n3)) (rdnn (n5))) ### Axiom % 12.14/12.36 4. (((rdn_positive_less (rdnn (n3)) (rdnn (n4))) /\ (rdn_positive_less (rdnn (n4)) (rdnn (n5)))) => (rdn_positive_less (rdnn (n3)) (rdnn (n5)))) (-. (rdn_positive_less (rdnn (n3)) (rdnn (n5)))) (rdn_positive_less (rdnn (n4)) (rdnn (n5))) (rdn_positive_less (rdnn (n3)) (rdnn (n4))) ### DisjTree 1 2 3 % 12.14/12.36 5. (All Z, (((rdn_positive_less (rdnn (n3)) (rdnn (n4))) /\ (rdn_positive_less (rdnn (n4)) (rdnn Z))) => (rdn_positive_less (rdnn (n3)) (rdnn Z)))) (rdn_positive_less (rdnn (n3)) (rdnn (n4))) (rdn_positive_less (rdnn (n4)) (rdnn (n5))) (-. (rdn_positive_less (rdnn (n3)) (rdnn (n5)))) ### All 4 % 12.14/12.36 6. (rdn_positive_less (rdnn (n5)) (rdnn (n6))) (-. (rdn_positive_less (rdnn (n5)) (rdnn (n6)))) ### Axiom % 12.14/12.36 7. (rdn_positive_less (rdnn (n6)) (rdnn (n7))) (-. (rdn_positive_less (rdnn (n6)) (rdnn (n7)))) ### Axiom % 12.14/12.36 8. (-. (rdn_positive_less (rdnn (n5)) (rdnn (n7)))) (rdn_positive_less (rdnn (n5)) (rdnn (n7))) ### Axiom % 12.14/12.36 9. (((rdn_positive_less (rdnn (n5)) (rdnn (n6))) /\ (rdn_positive_less (rdnn (n6)) (rdnn (n7)))) => (rdn_positive_less (rdnn (n5)) (rdnn (n7)))) (-. (rdn_positive_less (rdnn (n5)) (rdnn (n7)))) (rdn_positive_less (rdnn (n6)) (rdnn (n7))) (rdn_positive_less (rdnn (n5)) (rdnn (n6))) ### DisjTree 6 7 8 % 12.14/12.36 10. (All Z, (((rdn_positive_less (rdnn (n5)) (rdnn (n6))) /\ (rdn_positive_less (rdnn (n6)) (rdnn Z))) => (rdn_positive_less (rdnn (n5)) (rdnn Z)))) (rdn_positive_less (rdnn (n5)) (rdnn (n6))) (rdn_positive_less (rdnn (n6)) (rdnn (n7))) (-. (rdn_positive_less (rdnn (n5)) (rdnn (n7)))) ### All 9 % 12.14/12.36 11. (All Y, (All Z, (((rdn_positive_less (rdnn (n5)) (rdnn Y)) /\ (rdn_positive_less (rdnn Y) (rdnn Z))) => (rdn_positive_less (rdnn (n5)) (rdnn Z))))) (-. (rdn_positive_less (rdnn (n5)) (rdnn (n7)))) (rdn_positive_less (rdnn (n6)) (rdnn (n7))) (rdn_positive_less (rdnn (n5)) (rdnn (n6))) ### All 10 % 12.14/12.36 12. (All X, (All Y, (All Z, (((rdn_positive_less (rdnn X) (rdnn Y)) /\ (rdn_positive_less (rdnn Y) (rdnn Z))) => (rdn_positive_less (rdnn X) (rdnn Z)))))) (rdn_positive_less (rdnn (n5)) (rdnn (n6))) (rdn_positive_less (rdnn (n6)) (rdnn (n7))) (-. (rdn_positive_less (rdnn (n5)) (rdnn (n7)))) ### All 11 % 12.14/12.36 13. (rdn_positive_less (rdnn (n3)) (rdnn (n7))) (-. (rdn_positive_less (rdnn (n3)) (rdnn (n7)))) ### Axiom % 12.14/12.36 14. (rdn_positive_less (rdnn (n7)) (rdnn (n8))) (-. (rdn_positive_less (rdnn (n7)) (rdnn (n8)))) ### Axiom % 12.14/12.36 15. (rdn_positive_less (rdnn (n2)) (rdnn (n3))) (-. (rdn_positive_less (rdnn (n2)) (rdnn (n3)))) ### Axiom % 12.14/12.36 16. (rdn_positive_less (rdnn (n3)) (rdnn (n8))) (-. (rdn_positive_less (rdnn (n3)) (rdnn (n8)))) ### Axiom % 12.14/12.36 17. (rdn_positive_less (rdnn (n2)) (rdnn (n8))) (-. (rdn_positive_less (rdnn (n2)) (rdnn (n8)))) ### Axiom % 12.14/12.36 18. (rdn_positive_less (rdnn (n8)) (rdnn (n9))) (-. (rdn_positive_less (rdnn (n8)) (rdnn (n9)))) ### Axiom % 12.14/12.36 19. (rdn_translate (nn9) (rdn_neg (rdnn (n9)))) (-. (rdn_translate (nn9) (rdn_neg (rdnn (n9))))) ### Axiom % 12.14/12.36 20. (rdn_translate (nn2) (rdn_neg (rdnn (n2)))) (-. (rdn_translate (nn2) (rdn_neg (rdnn (n2))))) ### Axiom % 12.14/12.36 21. (rdn_positive_less (rdnn (n2)) (rdnn (n9))) (-. (rdn_positive_less (rdnn (n2)) (rdnn (n9)))) ### Axiom % 12.14/12.36 22. (less (nn9) (nn2)) (-. (less (nn9) (nn2))) ### Axiom % 12.14/12.36 23. (-. (Ex X, (less X (nn2)))) (less (nn9) (nn2)) ### NotExists 22 % 12.14/12.36 24. (((rdn_translate (nn9) (rdn_neg (rdnn (n9)))) /\ ((rdn_translate (nn2) (rdn_neg (rdnn (n2)))) /\ (rdn_positive_less (rdnn (n2)) (rdnn (n9))))) => (less (nn9) (nn2))) (-. (Ex X, (less X (nn2)))) (rdn_positive_less (rdnn (n2)) (rdnn (n9))) (rdn_translate (nn2) (rdn_neg (rdnn (n2)))) (rdn_translate (nn9) (rdn_neg (rdnn (n9)))) ### DisjTree 19 20 21 23 % 12.14/12.36 25. (All RDN_Y, (((rdn_translate (nn9) (rdn_neg (rdnn (n9)))) /\ ((rdn_translate (nn2) (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y (rdnn (n9))))) => (less (nn9) (nn2)))) (rdn_translate (nn9) (rdn_neg (rdnn (n9)))) (rdn_translate (nn2) (rdn_neg (rdnn (n2)))) (rdn_positive_less (rdnn (n2)) (rdnn (n9))) (-. (Ex X, (less X (nn2)))) ### All 24 % 12.14/12.36 26. (((rdn_positive_less (rdnn (n2)) (rdnn (n8))) /\ (rdn_positive_less (rdnn (n8)) (rdnn (n9)))) => (rdn_positive_less (rdnn (n2)) (rdnn (n9)))) (-. (Ex X, (less X (nn2)))) (rdn_translate (nn2) (rdn_neg (rdnn (n2)))) (rdn_translate (nn9) (rdn_neg (rdnn (n9)))) (All RDN_Y, (((rdn_translate (nn9) (rdn_neg (rdnn (n9)))) /\ ((rdn_translate (nn2) (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y (rdnn (n9))))) => (less (nn9) (nn2)))) (rdn_positive_less (rdnn (n8)) (rdnn (n9))) (rdn_positive_less (rdnn (n2)) (rdnn (n8))) ### DisjTree 17 18 25 % 12.14/12.36 27. (All Z, (((rdn_positive_less (rdnn (n2)) (rdnn (n8))) /\ (rdn_positive_less (rdnn (n8)) (rdnn Z))) => (rdn_positive_less (rdnn (n2)) (rdnn Z)))) (rdn_positive_less (rdnn (n2)) (rdnn (n8))) (rdn_positive_less (rdnn (n8)) (rdnn (n9))) (All RDN_Y, (((rdn_translate (nn9) (rdn_neg (rdnn (n9)))) /\ ((rdn_translate (nn2) (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y (rdnn (n9))))) => (less (nn9) (nn2)))) (rdn_translate (nn9) (rdn_neg (rdnn (n9)))) (rdn_translate (nn2) (rdn_neg (rdnn (n2)))) (-. (Ex X, (less X (nn2)))) ### All 26 % 12.14/12.36 28. (All Y, (All Z, (((rdn_positive_less (rdnn (n2)) (rdnn Y)) /\ (rdn_positive_less (rdnn Y) (rdnn Z))) => (rdn_positive_less (rdnn (n2)) (rdnn Z))))) (-. (Ex X, (less X (nn2)))) (rdn_translate (nn2) (rdn_neg (rdnn (n2)))) (rdn_translate (nn9) (rdn_neg (rdnn (n9)))) (All RDN_Y, (((rdn_translate (nn9) (rdn_neg (rdnn (n9)))) /\ ((rdn_translate (nn2) (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y (rdnn (n9))))) => (less (nn9) (nn2)))) (rdn_positive_less (rdnn (n8)) (rdnn (n9))) (rdn_positive_less (rdnn (n2)) (rdnn (n8))) ### All 27 % 12.14/12.36 29. (((rdn_positive_less (rdnn (n2)) (rdnn (n3))) /\ (rdn_positive_less (rdnn (n3)) (rdnn (n8)))) => (rdn_positive_less (rdnn (n2)) (rdnn (n8)))) (rdn_positive_less (rdnn (n8)) (rdnn (n9))) (All RDN_Y, (((rdn_translate (nn9) (rdn_neg (rdnn (n9)))) /\ ((rdn_translate (nn2) (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y (rdnn (n9))))) => (less (nn9) (nn2)))) (rdn_translate (nn9) (rdn_neg (rdnn (n9)))) (rdn_translate (nn2) (rdn_neg (rdnn (n2)))) (-. (Ex X, (less X (nn2)))) (All Y, (All Z, (((rdn_positive_less (rdnn (n2)) (rdnn Y)) /\ (rdn_positive_less (rdnn Y) (rdnn Z))) => (rdn_positive_less (rdnn (n2)) (rdnn Z))))) (rdn_positive_less (rdnn (n3)) (rdnn (n8))) (rdn_positive_less (rdnn (n2)) (rdnn (n3))) ### DisjTree 15 16 28 % 12.14/12.36 30. (All Z, (((rdn_positive_less (rdnn (n2)) (rdnn (n3))) /\ (rdn_positive_less (rdnn (n3)) (rdnn Z))) => (rdn_positive_less (rdnn (n2)) (rdnn Z)))) (rdn_positive_less (rdnn (n2)) (rdnn (n3))) (rdn_positive_less (rdnn (n3)) (rdnn (n8))) (All Y, (All Z, (((rdn_positive_less (rdnn (n2)) (rdnn Y)) /\ (rdn_positive_less (rdnn Y) (rdnn Z))) => (rdn_positive_less (rdnn (n2)) (rdnn Z))))) (-. (Ex X, (less X (nn2)))) (rdn_translate (nn2) (rdn_neg (rdnn (n2)))) (rdn_translate (nn9) (rdn_neg (rdnn (n9)))) (All RDN_Y, (((rdn_translate (nn9) (rdn_neg (rdnn (n9)))) /\ ((rdn_translate (nn2) (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y (rdnn (n9))))) => (less (nn9) (nn2)))) (rdn_positive_less (rdnn (n8)) (rdnn (n9))) ### All 29 % 12.14/12.36 31. (rdn_positive_less (rdnn (n8)) (rdnn (n9))) (All RDN_Y, (((rdn_translate (nn9) (rdn_neg (rdnn (n9)))) /\ ((rdn_translate (nn2) (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y (rdnn (n9))))) => (less (nn9) (nn2)))) (rdn_translate (nn9) (rdn_neg (rdnn (n9)))) (rdn_translate (nn2) (rdn_neg (rdnn (n2)))) (-. (Ex X, (less X (nn2)))) (All Y, (All Z, (((rdn_positive_less (rdnn (n2)) (rdnn Y)) /\ (rdn_positive_less (rdnn Y) (rdnn Z))) => (rdn_positive_less (rdnn (n2)) (rdnn Z))))) (rdn_positive_less (rdnn (n3)) (rdnn (n8))) (rdn_positive_less (rdnn (n2)) (rdnn (n3))) ### All 30 % 12.14/12.36 32. (All X, (All Y, (All Z, (((rdn_positive_less (rdnn X) (rdnn Y)) /\ (rdn_positive_less (rdnn Y) (rdnn Z))) => (rdn_positive_less (rdnn X) (rdnn Z)))))) (rdn_positive_less (rdnn (n2)) (rdnn (n3))) (rdn_positive_less (rdnn (n3)) (rdnn (n8))) (-. (Ex X, (less X (nn2)))) (rdn_translate (nn2) (rdn_neg (rdnn (n2)))) (rdn_translate (nn9) (rdn_neg (rdnn (n9)))) (All RDN_Y, (((rdn_translate (nn9) (rdn_neg (rdnn (n9)))) /\ ((rdn_translate (nn2) (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y (rdnn (n9))))) => (less (nn9) (nn2)))) (rdn_positive_less (rdnn (n8)) (rdnn (n9))) ### All 31 % 12.14/12.36 33. (All RDN_X, (All RDN_Y, (((rdn_translate (nn9) (rdn_neg RDN_X)) /\ ((rdn_translate (nn2) (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less (nn9) (nn2))))) (rdn_positive_less (rdnn (n8)) (rdnn (n9))) (rdn_translate (nn9) (rdn_neg (rdnn (n9)))) (rdn_translate (nn2) (rdn_neg (rdnn (n2)))) (-. (Ex X, (less X (nn2)))) (rdn_positive_less (rdnn (n3)) (rdnn (n8))) (rdn_positive_less (rdnn (n2)) (rdnn (n3))) (All X, (All Y, (All Z, (((rdn_positive_less (rdnn X) (rdnn Y)) /\ (rdn_positive_less (rdnn Y) (rdnn Z))) => (rdn_positive_less (rdnn X) (rdnn Z)))))) ### All 32 % 12.14/12.36 34. (((rdn_positive_less (rdnn (n3)) (rdnn (n7))) /\ (rdn_positive_less (rdnn (n7)) (rdnn (n8)))) => (rdn_positive_less (rdnn (n3)) (rdnn (n8)))) (All X, (All Y, (All Z, (((rdn_positive_less (rdnn X) (rdnn Y)) /\ (rdn_positive_less (rdnn Y) (rdnn Z))) => (rdn_positive_less (rdnn X) (rdnn Z)))))) (rdn_positive_less (rdnn (n2)) (rdnn (n3))) (-. (Ex X, (less X (nn2)))) (rdn_translate (nn2) (rdn_neg (rdnn (n2)))) (rdn_translate (nn9) (rdn_neg (rdnn (n9)))) (rdn_positive_less (rdnn (n8)) (rdnn (n9))) (All RDN_X, (All RDN_Y, (((rdn_translate (nn9) (rdn_neg RDN_X)) /\ ((rdn_translate (nn2) (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less (nn9) (nn2))))) (rdn_positive_less (rdnn (n7)) (rdnn (n8))) (rdn_positive_less (rdnn (n3)) (rdnn (n7))) ### DisjTree 13 14 33 % 12.14/12.36 35. (All Z, (((rdn_positive_less (rdnn (n3)) (rdnn (n7))) /\ (rdn_positive_less (rdnn (n7)) (rdnn Z))) => (rdn_positive_less (rdnn (n3)) (rdnn Z)))) (rdn_positive_less (rdnn (n3)) (rdnn (n7))) (rdn_positive_less (rdnn (n7)) (rdnn (n8))) (All RDN_X, (All RDN_Y, (((rdn_translate (nn9) (rdn_neg RDN_X)) /\ ((rdn_translate (nn2) (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less (nn9) (nn2))))) (rdn_positive_less (rdnn (n8)) (rdnn (n9))) (rdn_translate (nn9) (rdn_neg (rdnn (n9)))) (rdn_translate (nn2) (rdn_neg (rdnn (n2)))) (-. (Ex X, (less X (nn2)))) (rdn_positive_less (rdnn (n2)) (rdnn (n3))) (All X, (All Y, (All Z, (((rdn_positive_less (rdnn X) (rdnn Y)) /\ (rdn_positive_less (rdnn Y) (rdnn Z))) => (rdn_positive_less (rdnn X) (rdnn Z)))))) ### All 34 % 12.14/12.36 36. (((rdn_positive_less (rdnn (n3)) (rdnn (n5))) /\ (rdn_positive_less (rdnn (n5)) (rdnn (n7)))) => (rdn_positive_less (rdnn (n3)) (rdnn (n7)))) (rdn_positive_less (rdnn (n2)) (rdnn (n3))) (-. (Ex X, (less X (nn2)))) (rdn_translate (nn2) (rdn_neg (rdnn (n2)))) (rdn_translate (nn9) (rdn_neg (rdnn (n9)))) (rdn_positive_less (rdnn (n8)) (rdnn (n9))) (All RDN_X, (All RDN_Y, (((rdn_translate (nn9) (rdn_neg RDN_X)) /\ ((rdn_translate (nn2) (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less (nn9) (nn2))))) (rdn_positive_less (rdnn (n7)) (rdnn (n8))) (All Z, (((rdn_positive_less (rdnn (n3)) (rdnn (n7))) /\ (rdn_positive_less (rdnn (n7)) (rdnn Z))) => (rdn_positive_less (rdnn (n3)) (rdnn Z)))) (rdn_positive_less (rdnn (n6)) (rdnn (n7))) (rdn_positive_less (rdnn (n5)) (rdnn (n6))) (All X, (All Y, (All Z, (((rdn_positive_less (rdnn X) (rdnn Y)) /\ (rdn_positive_less (rdnn Y) (rdnn Z))) => (rdn_positive_less (rdnn X) (rdnn Z)))))) (rdn_positive_less (rdnn (n4)) (rdnn (n5))) (rdn_positive_less (rdnn (n3)) (rdnn (n4))) (All Z, (((rdn_positive_less (rdnn (n3)) (rdnn (n4))) /\ (rdn_positive_less (rdnn (n4)) (rdnn Z))) => (rdn_positive_less (rdnn (n3)) (rdnn Z)))) ### DisjTree 5 12 35 % 12.14/12.36 37. (All Z, (((rdn_positive_less (rdnn (n3)) (rdnn (n5))) /\ (rdn_positive_less (rdnn (n5)) (rdnn Z))) => (rdn_positive_less (rdnn (n3)) (rdnn Z)))) (All Z, (((rdn_positive_less (rdnn (n3)) (rdnn (n4))) /\ (rdn_positive_less (rdnn (n4)) (rdnn Z))) => (rdn_positive_less (rdnn (n3)) (rdnn Z)))) (rdn_positive_less (rdnn (n3)) (rdnn (n4))) (rdn_positive_less (rdnn (n4)) (rdnn (n5))) (All X, (All Y, (All Z, (((rdn_positive_less (rdnn X) (rdnn Y)) /\ (rdn_positive_less (rdnn Y) (rdnn Z))) => (rdn_positive_less (rdnn X) (rdnn Z)))))) (rdn_positive_less (rdnn (n5)) (rdnn (n6))) (rdn_positive_less (rdnn (n6)) (rdnn (n7))) (All Z, (((rdn_positive_less (rdnn (n3)) (rdnn (n7))) /\ (rdn_positive_less (rdnn (n7)) (rdnn Z))) => (rdn_positive_less (rdnn (n3)) (rdnn Z)))) (rdn_positive_less (rdnn (n7)) (rdnn (n8))) (All RDN_X, (All RDN_Y, (((rdn_translate (nn9) (rdn_neg RDN_X)) /\ ((rdn_translate (nn2) (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less (nn9) (nn2))))) (rdn_positive_less (rdnn (n8)) (rdnn (n9))) (rdn_translate (nn9) (rdn_neg (rdnn (n9)))) (rdn_translate (nn2) (rdn_neg (rdnn (n2)))) (-. (Ex X, (less X (nn2)))) (rdn_positive_less (rdnn (n2)) (rdnn (n3))) ### All 36 % 12.14/12.36 38. (All Y, (All Z, (((rdn_positive_less (rdnn (n3)) (rdnn Y)) /\ (rdn_positive_less (rdnn Y) (rdnn Z))) => (rdn_positive_less (rdnn (n3)) (rdnn Z))))) (rdn_positive_less (rdnn (n2)) (rdnn (n3))) (-. (Ex X, (less X (nn2)))) (rdn_translate (nn2) (rdn_neg (rdnn (n2)))) (rdn_translate (nn9) (rdn_neg (rdnn (n9)))) (rdn_positive_less (rdnn (n8)) (rdnn (n9))) (All RDN_X, (All RDN_Y, (((rdn_translate (nn9) (rdn_neg RDN_X)) /\ ((rdn_translate (nn2) (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less (nn9) (nn2))))) (rdn_positive_less (rdnn (n7)) (rdnn (n8))) (rdn_positive_less (rdnn (n6)) (rdnn (n7))) (rdn_positive_less (rdnn (n5)) (rdnn (n6))) (All X, (All Y, (All Z, (((rdn_positive_less (rdnn X) (rdnn Y)) /\ (rdn_positive_less (rdnn Y) (rdnn Z))) => (rdn_positive_less (rdnn X) (rdnn Z)))))) (rdn_positive_less (rdnn (n4)) (rdnn (n5))) (rdn_positive_less (rdnn (n3)) (rdnn (n4))) (All Z, (((rdn_positive_less (rdnn (n3)) (rdnn (n4))) /\ (rdn_positive_less (rdnn (n4)) (rdnn Z))) => (rdn_positive_less (rdnn (n3)) (rdnn Z)))) (All Z, (((rdn_positive_less (rdnn (n3)) (rdnn (n5))) /\ (rdn_positive_less (rdnn (n5)) (rdnn Z))) => (rdn_positive_less (rdnn (n3)) (rdnn Z)))) ### All 37 % 12.14/12.36 39. (All Z, (((rdn_positive_less (rdnn (n3)) (rdnn (n5))) /\ (rdn_positive_less (rdnn (n5)) (rdnn Z))) => (rdn_positive_less (rdnn (n3)) (rdnn Z)))) (rdn_positive_less (rdnn (n3)) (rdnn (n4))) (rdn_positive_less (rdnn (n4)) (rdnn (n5))) (All X, (All Y, (All Z, (((rdn_positive_less (rdnn X) (rdnn Y)) /\ (rdn_positive_less (rdnn Y) (rdnn Z))) => (rdn_positive_less (rdnn X) (rdnn Z)))))) (rdn_positive_less (rdnn (n5)) (rdnn (n6))) (rdn_positive_less (rdnn (n6)) (rdnn (n7))) (rdn_positive_less (rdnn (n7)) (rdnn (n8))) (All RDN_X, (All RDN_Y, (((rdn_translate (nn9) (rdn_neg RDN_X)) /\ ((rdn_translate (nn2) (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less (nn9) (nn2))))) (rdn_positive_less (rdnn (n8)) (rdnn (n9))) (rdn_translate (nn9) (rdn_neg (rdnn (n9)))) (rdn_translate (nn2) (rdn_neg (rdnn (n2)))) (-. (Ex X, (less X (nn2)))) (rdn_positive_less (rdnn (n2)) (rdnn (n3))) (All Y, (All Z, (((rdn_positive_less (rdnn (n3)) (rdnn Y)) /\ (rdn_positive_less (rdnn Y) (rdnn Z))) => (rdn_positive_less (rdnn (n3)) (rdnn Z))))) ### All 38 % 12.14/12.36 40. (All Y, (All Z, (((rdn_positive_less (rdnn (n3)) (rdnn Y)) /\ (rdn_positive_less (rdnn Y) (rdnn Z))) => (rdn_positive_less (rdnn (n3)) (rdnn Z))))) (rdn_positive_less (rdnn (n2)) (rdnn (n3))) (-. (Ex X, (less X (nn2)))) (rdn_translate (nn2) (rdn_neg (rdnn (n2)))) (rdn_translate (nn9) (rdn_neg (rdnn (n9)))) (rdn_positive_less (rdnn (n8)) (rdnn (n9))) (All RDN_X, (All RDN_Y, (((rdn_translate (nn9) (rdn_neg RDN_X)) /\ ((rdn_translate (nn2) (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less (nn9) (nn2))))) (rdn_positive_less (rdnn (n7)) (rdnn (n8))) (rdn_positive_less (rdnn (n6)) (rdnn (n7))) (rdn_positive_less (rdnn (n5)) (rdnn (n6))) (All X, (All Y, (All Z, (((rdn_positive_less (rdnn X) (rdnn Y)) /\ (rdn_positive_less (rdnn Y) (rdnn Z))) => (rdn_positive_less (rdnn X) (rdnn Z)))))) (rdn_positive_less (rdnn (n4)) (rdnn (n5))) (rdn_positive_less (rdnn (n3)) (rdnn (n4))) ### All 39 % 12.14/12.36 41. (rdn_positive_less (rdnn (n3)) (rdnn (n4))) (rdn_positive_less (rdnn (n4)) (rdnn (n5))) (All X, (All Y, (All Z, (((rdn_positive_less (rdnn X) (rdnn Y)) /\ (rdn_positive_less (rdnn Y) (rdnn Z))) => (rdn_positive_less (rdnn X) (rdnn Z)))))) (rdn_positive_less (rdnn (n5)) (rdnn (n6))) (rdn_positive_less (rdnn (n6)) (rdnn (n7))) (rdn_positive_less (rdnn (n7)) (rdnn (n8))) (All RDN_X, (All RDN_Y, (((rdn_translate (nn9) (rdn_neg RDN_X)) /\ ((rdn_translate (nn2) (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less (nn9) (nn2))))) (rdn_positive_less (rdnn (n8)) (rdnn (n9))) (rdn_translate (nn9) (rdn_neg (rdnn (n9)))) (rdn_translate (nn2) (rdn_neg (rdnn (n2)))) (-. (Ex X, (less X (nn2)))) (rdn_positive_less (rdnn (n2)) (rdnn (n3))) ### All 40 % 12.20/12.37 42. (All Y, (All RDN_X, (All RDN_Y, (((rdn_translate (nn9) (rdn_neg RDN_X)) /\ ((rdn_translate Y (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less (nn9) Y))))) (rdn_positive_less (rdnn (n2)) (rdnn (n3))) (-. (Ex X, (less X (nn2)))) (rdn_translate (nn2) (rdn_neg (rdnn (n2)))) (rdn_translate (nn9) (rdn_neg (rdnn (n9)))) (rdn_positive_less (rdnn (n8)) (rdnn (n9))) (rdn_positive_less (rdnn (n7)) (rdnn (n8))) (rdn_positive_less (rdnn (n6)) (rdnn (n7))) (rdn_positive_less (rdnn (n5)) (rdnn (n6))) (All X, (All Y, (All Z, (((rdn_positive_less (rdnn X) (rdnn Y)) /\ (rdn_positive_less (rdnn Y) (rdnn Z))) => (rdn_positive_less (rdnn X) (rdnn Z)))))) (rdn_positive_less (rdnn (n4)) (rdnn (n5))) (rdn_positive_less (rdnn (n3)) (rdnn (n4))) ### All 41 % 12.20/12.37 43. (All X, (All Y, (All RDN_X, (All RDN_Y, (((rdn_translate X (rdn_neg RDN_X)) /\ ((rdn_translate Y (rdn_neg RDN_Y)) /\ (rdn_positive_less RDN_Y RDN_X))) => (less X Y)))))) (rdn_positive_less (rdnn (n3)) (rdnn (n4))) (rdn_positive_less (rdnn (n4)) (rdnn (n5))) (All X, (All Y, (All Z, (((rdn_positive_less (rdnn X) (rdnn Y)) /\ (rdn_positive_less (rdnn Y) (rdnn Z))) => (rdn_positive_less (rdnn X) (rdnn Z)))))) (rdn_positive_less (rdnn (n5)) (rdnn (n6))) (rdn_positive_less (rdnn (n6)) (rdnn (n7))) (rdn_positive_less (rdnn (n7)) (rdnn (n8))) (rdn_positive_less (rdnn (n8)) (rdnn (n9))) (rdn_translate (nn9) (rdn_neg (rdnn (n9)))) (rdn_translate (nn2) (rdn_neg (rdnn (n2)))) (-. (Ex X, (less X (nn2)))) (rdn_positive_less (rdnn (n2)) (rdnn (n3))) ### All 42 % 12.20/12.37 % SZS output end Proof % 12.20/12.37 (* END-PROOF *) %------------------------------------------------------------------------------