%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SWV036+1 : TPTP v8.1.0. Bugfixed v3.3.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n006.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 : Wed Jul 20 21:49:47 EDT 2022 % Result : Theorem 33.35s 33.52s % Output : Proof 33.35s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWV036+1 : TPTP v8.1.0. Bugfixed v3.3.0. % 0.07/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.34 % Computer : n006.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 : Wed Jun 15 16:22:56 EDT 2022 % 0.13/0.34 % CPUTime : % 33.35/33.52 % SZS status Theorem % 33.35/33.52 (* PROOF-FOUND *) % 33.35/33.52 (* BEGIN-PROOF *) % 33.35/33.52 % SZS output start Proof % 33.35/33.52 1. ((init) != (init)) ### NotEqual % 33.35/33.52 2. ((s_best7_init) = (init)) ((s_best7_init) != (init)) ### Axiom % 33.35/33.52 3. (gt (succ (s_best7)) (n0)) (-. (gt (succ (s_best7)) (n0))) ### Axiom % 33.35/33.52 4. (-. (leq (n0) (s_best7))) (gt (succ (s_best7)) (n0)) ### Definition-Pseudo(leq) 3 % 33.35/33.52 5. (gt (succ (n3)) (s_best7)) (-. (gt (succ (n3)) (s_best7))) ### Axiom % 33.35/33.52 6. (-. (leq (s_best7) (n3))) (gt (succ (n3)) (s_best7)) ### Definition-Pseudo(leq) 5 % 33.35/33.52 7. ((a_select2 (s_values7_init) (s_best7)) != (init)) ((a_select2 (s_values7_init) (s_best7)) = (init)) ### Axiom % 33.35/33.52 8. (((leq (n0) (s_best7)) /\ (leq (s_best7) (n3))) => ((a_select2 (s_values7_init) (s_best7)) = (init))) ((a_select2 (s_values7_init) (s_best7)) != (init)) (gt (succ (n3)) (s_best7)) (gt (succ (s_best7)) (n0)) ### DisjTree 4 6 7 % 33.35/33.52 9. (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (gt (succ (s_best7)) (n0)) (gt (succ (n3)) (s_best7)) ((a_select2 (s_values7_init) (s_best7)) != (init)) ### All 8 % 33.35/33.52 10. (gt (succ (pv1388)) (n2)) (-. (gt (succ (pv1388)) (n2))) ### Axiom % 33.35/33.52 11. ((n1) != (n1)) ### NotEqual % 33.35/33.52 12. (-. (gt (succ (pv1388)) (n1))) (gt (n2) (n1)) (gt (succ (pv1388)) (n2)) ### Trans 10 11 % 33.35/33.52 13. ((n0) != (n0)) ### NotEqual % 33.35/33.52 14. (-. (gt (succ (pv1388)) (n0))) (gt (n1) (n0)) (gt (succ (pv1388)) (n2)) (gt (n2) (n1)) ### Trans 12 13 % 33.35/33.52 15. (-. (leq (n0) (pv1388))) (gt (n2) (n1)) (gt (succ (pv1388)) (n2)) (gt (n1) (n0)) ### Definition-Pseudo(leq) 14 % 33.35/33.52 16. (gt (succ (n3)) (pv1388)) (-. (gt (succ (n3)) (pv1388))) ### Axiom % 33.35/33.52 17. (-. (leq (pv1388) (n3))) (gt (succ (n3)) (pv1388)) ### Definition-Pseudo(leq) 16 % 33.35/33.52 18. ((a_select2 (s_values7_init) (pv1388)) != (init)) ((a_select2 (s_values7_init) (pv1388)) = (init)) ### Axiom % 33.35/33.52 19. (((leq (n0) (pv1388)) /\ (leq (pv1388) (n3))) => ((a_select2 (s_values7_init) (pv1388)) = (init))) ((a_select2 (s_values7_init) (pv1388)) != (init)) (gt (succ (n3)) (pv1388)) (gt (n1) (n0)) (gt (succ (pv1388)) (n2)) (gt (n2) (n1)) ### DisjTree 15 17 18 % 33.35/33.52 20. (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (gt (n2) (n1)) (gt (succ (pv1388)) (n2)) (gt (n1) (n0)) (gt (succ (n3)) (pv1388)) ((a_select2 (s_values7_init) (pv1388)) != (init)) ### All 19 % 33.35/33.52 21. ((s_worst7_init) = (init)) ((s_worst7_init) != (init)) ### Axiom % 33.35/33.52 22. (gt (succ (s_worst7)) (n0)) (-. (gt (succ (s_worst7)) (n0))) ### Axiom % 33.35/33.52 23. (-. (leq (n0) (s_worst7))) (gt (succ (s_worst7)) (n0)) ### Definition-Pseudo(leq) 22 % 33.35/33.52 24. (gt (succ (n3)) (s_worst7)) (-. (gt (succ (n3)) (s_worst7))) ### Axiom % 33.35/33.52 25. (-. (leq (s_worst7) (n3))) (gt (succ (n3)) (s_worst7)) ### Definition-Pseudo(leq) 24 % 33.35/33.52 26. ((a_select2 (s_values7_init) (s_worst7)) != (init)) ((a_select2 (s_values7_init) (s_worst7)) = (init)) ### Axiom % 33.35/33.52 27. (((leq (n0) (s_worst7)) /\ (leq (s_worst7) (n3))) => ((a_select2 (s_values7_init) (s_worst7)) = (init))) ((a_select2 (s_values7_init) (s_worst7)) != (init)) (gt (succ (n3)) (s_worst7)) (gt (succ (s_worst7)) (n0)) ### DisjTree 23 25 26 % 33.35/33.52 28. (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (gt (succ (s_worst7)) (n0)) (gt (succ (n3)) (s_worst7)) ((a_select2 (s_values7_init) (s_worst7)) != (init)) ### All 27 % 33.35/33.52 29. ((s_sworst7_init) = (init)) ((s_sworst7_init) != (init)) ### Axiom % 33.35/33.52 30. (gt (succ (s_sworst7)) (n0)) (-. (gt (succ (s_sworst7)) (n0))) ### Axiom % 33.35/33.52 31. (-. (leq (n0) (s_sworst7))) (gt (succ (s_sworst7)) (n0)) ### Definition-Pseudo(leq) 30 % 33.35/33.52 32. (gt (succ (n3)) (s_sworst7)) (-. (gt (succ (n3)) (s_sworst7))) ### Axiom % 33.35/33.52 33. (-. (leq (s_sworst7) (n3))) (gt (succ (n3)) (s_sworst7)) ### Definition-Pseudo(leq) 32 % 33.35/33.52 34. ((a_select2 (s_values7_init) (s_sworst7)) != (init)) ((a_select2 (s_values7_init) (s_sworst7)) = (init)) ### Axiom % 33.35/33.52 35. (((leq (n0) (s_sworst7)) /\ (leq (s_sworst7) (n3))) => ((a_select2 (s_values7_init) (s_sworst7)) = (init))) ((a_select2 (s_values7_init) (s_sworst7)) != (init)) (gt (succ (n3)) (s_sworst7)) (gt (succ (s_sworst7)) (n0)) ### DisjTree 31 33 34 % 33.35/33.52 36. (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (gt (succ (s_sworst7)) (n0)) (gt (succ (n3)) (s_sworst7)) ((a_select2 (s_values7_init) (s_sworst7)) != (init)) ### All 35 % 33.35/33.52 37. ((s_best7_init) = (init)) ((s_best7_init) != (init)) ### Axiom % 33.35/33.52 38. ((s_sworst7_init) = (init)) ((s_sworst7_init) != (init)) ### Axiom % 33.35/33.52 39. ((s_worst7_init) = (init)) ((s_worst7_init) != (init)) ### Axiom % 33.35/33.52 40. (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (-. (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init))))))) ### Axiom % 33.35/33.52 41. (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (-. (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init))))) ### Axiom % 33.35/33.52 42. (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (-. (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init))))) ### Axiom % 33.35/33.52 43. (-. (gt (loopcounter) (n1))) (gt (loopcounter) (n1)) ### Axiom % 33.35/33.52 44. (-. ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))) (-. (gt (loopcounter) (n1))) ### NotImply 43 % 33.35/33.52 45. (-. (((s_best7_init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))) (-. (gt (loopcounter) (n1))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (gt (succ (n3)) (s_worst7)) (gt (succ (n3)) (s_sworst7)) (gt (succ (n3)) (s_best7)) (gt (succ (s_worst7)) (n0)) (gt (succ (s_sworst7)) (n0)) (gt (succ (s_best7)) (n0)) ((s_worst7_init) = (init)) ((s_sworst7_init) = (init)) ((s_best7_init) = (init)) ### DisjTree 37 38 39 4 31 23 6 33 25 40 41 42 44 % 33.35/33.52 46. (-. ((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7)))) => (((s_best7_init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init))))))))))))))))))) ((s_best7_init) = (init)) ((s_sworst7_init) = (init)) ((s_worst7_init) = (init)) (gt (succ (s_best7)) (n0)) (gt (succ (s_sworst7)) (n0)) (gt (succ (s_worst7)) (n0)) (gt (succ (n3)) (s_best7)) (gt (succ (n3)) (s_sworst7)) (gt (succ (n3)) (s_worst7)) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (-. (gt (loopcounter) (n1))) ### NotImply 45 % 33.35/33.52 47. ((s_best7_init) = (init)) ((s_best7_init) != (init)) ### Axiom % 33.35/33.52 48. ((s_worst7_init) = (init)) ((s_worst7_init) != (init)) ### Axiom % 33.35/33.52 49. (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (-. (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init))))))) ### Axiom % 33.35/33.52 50. (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (-. (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init))))) ### Axiom % 33.35/33.52 51. (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (-. (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init))))) ### Axiom % 33.35/33.52 52. (-. (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))) (-. (gt (loopcounter) (n1))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (gt (succ (n3)) (pv1388)) (gt (succ (n3)) (s_worst7)) (gt (succ (n3)) (s_best7)) (gt (n1) (n0)) (gt (succ (pv1388)) (n2)) (gt (n2) (n1)) (gt (succ (s_worst7)) (n0)) (gt (succ (s_best7)) (n0)) ((s_worst7_init) = (init)) ((s_best7_init) = (init)) ### DisjTree 1 47 48 4 23 15 6 25 17 49 50 51 44 % 33.35/33.52 53. (-. ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init))))))))))))))))))) ((s_best7_init) = (init)) ((s_worst7_init) = (init)) (gt (succ (s_best7)) (n0)) (gt (succ (s_worst7)) (n0)) (gt (n2) (n1)) (gt (succ (pv1388)) (n2)) (gt (n1) (n0)) (gt (succ (n3)) (s_best7)) (gt (succ (n3)) (s_worst7)) (gt (succ (n3)) (pv1388)) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (-. (gt (loopcounter) (n1))) ### NotImply 52 % 33.35/33.52 54. (-. (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_sworst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7)))) => (((s_best7_init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) (-. (gt (loopcounter) (n1))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (gt (succ (n3)) (s_worst7)) (gt (succ (n3)) (s_best7)) (gt (succ (s_worst7)) (n0)) (gt (succ (s_best7)) (n0)) ((s_worst7_init) = (init)) ((s_best7_init) = (init)) (gt (succ (n3)) (pv1388)) (gt (n1) (n0)) (gt (succ (pv1388)) (n2)) (gt (n2) (n1)) (gt (succ (n3)) (s_sworst7)) (gt (succ (s_sworst7)) (n0)) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) ((s_sworst7_init) = (init)) ### DisjTree 1 29 36 20 46 53 % 33.35/33.52 55. (-. ((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7)))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_sworst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7)))) => (((s_best7_init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init))))))))))))))))))))))))) ((s_sworst7_init) = (init)) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (gt (succ (s_sworst7)) (n0)) (gt (succ (n3)) (s_sworst7)) (gt (n2) (n1)) (gt (succ (pv1388)) (n2)) (gt (n1) (n0)) (gt (succ (n3)) (pv1388)) ((s_best7_init) = (init)) ((s_worst7_init) = (init)) (gt (succ (s_best7)) (n0)) (gt (succ (s_worst7)) (n0)) (gt (succ (n3)) (s_best7)) (gt (succ (n3)) (s_worst7)) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (-. (gt (loopcounter) (n1))) ### NotImply 54 % 33.35/33.52 56. (-. ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init))))))))))))))))))) ((s_best7_init) = (init)) ((s_worst7_init) = (init)) (gt (succ (s_best7)) (n0)) (gt (succ (s_worst7)) (n0)) (gt (n2) (n1)) (gt (succ (pv1388)) (n2)) (gt (n1) (n0)) (gt (succ (n3)) (s_best7)) (gt (succ (n3)) (s_worst7)) (gt (succ (n3)) (pv1388)) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (-. (gt (loopcounter) (n1))) ### NotImply 52 % 33.35/33.52 57. (-. (((init) = (init)) /\ (((s_worst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_worst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7)))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_sworst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7)))) => (((s_best7_init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) (-. (gt (loopcounter) (n1))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (gt (succ (n3)) (s_best7)) (gt (succ (s_best7)) (n0)) ((s_best7_init) = (init)) (gt (succ (n3)) (s_sworst7)) (gt (succ (s_sworst7)) (n0)) ((s_sworst7_init) = (init)) (gt (succ (n3)) (pv1388)) (gt (n1) (n0)) (gt (succ (pv1388)) (n2)) (gt (n2) (n1)) (gt (succ (n3)) (s_worst7)) (gt (succ (s_worst7)) (n0)) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) ((s_worst7_init) = (init)) ### DisjTree 1 21 28 20 55 56 % 33.35/33.52 58. (-. ((-. (gt (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_best7)))) => (((init) = (init)) /\ (((s_worst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_worst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7)))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_sworst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7)))) => (((s_best7_init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init))))))))))))))))))))))))) ((s_worst7_init) = (init)) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (gt (succ (s_worst7)) (n0)) (gt (succ (n3)) (s_worst7)) (gt (n2) (n1)) (gt (succ (pv1388)) (n2)) (gt (n1) (n0)) (gt (succ (n3)) (pv1388)) ((s_sworst7_init) = (init)) (gt (succ (s_sworst7)) (n0)) (gt (succ (n3)) (s_sworst7)) ((s_best7_init) = (init)) (gt (succ (s_best7)) (n0)) (gt (succ (n3)) (s_best7)) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (-. (gt (loopcounter) (n1))) ### NotImply 57 % 33.35/33.52 59. ((s_sworst7_init) = (init)) ((s_sworst7_init) != (init)) ### Axiom % 33.35/33.52 60. ((s_worst7_init) = (init)) ((s_worst7_init) != (init)) ### Axiom % 33.35/33.52 61. (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (-. (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init))))))) ### Axiom % 33.35/33.52 62. (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (-. (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init))))) ### Axiom % 33.35/33.52 63. (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (-. (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init))))) ### Axiom % 33.35/33.52 64. (-. (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))) (-. (gt (loopcounter) (n1))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (gt (succ (n3)) (pv1388)) (gt (succ (n3)) (s_worst7)) (gt (succ (n3)) (s_sworst7)) (gt (n1) (n0)) (gt (succ (pv1388)) (n2)) (gt (n2) (n1)) (gt (succ (s_worst7)) (n0)) (gt (succ (s_sworst7)) (n0)) ((s_worst7_init) = (init)) ((s_sworst7_init) = (init)) ### DisjTree 1 59 60 31 23 15 33 25 17 61 62 63 44 % 33.35/33.52 65. (-. ((gt (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_best7))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init))))))))))))))))))) ((s_sworst7_init) = (init)) ((s_worst7_init) = (init)) (gt (succ (s_sworst7)) (n0)) (gt (succ (s_worst7)) (n0)) (gt (n2) (n1)) (gt (succ (pv1388)) (n2)) (gt (n1) (n0)) (gt (succ (n3)) (s_sworst7)) (gt (succ (n3)) (s_worst7)) (gt (succ (n3)) (pv1388)) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (-. (gt (loopcounter) (n1))) ### NotImply 64 % 33.35/33.52 66. (-. (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_best7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (gt (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_best7)))) => (((init) = (init)) /\ (((s_worst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_worst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7)))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_sworst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7)))) => (((s_best7_init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) /\ ((gt (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_best7))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) (-. (gt (loopcounter) (n1))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (gt (succ (n3)) (s_sworst7)) (gt (succ (s_sworst7)) (n0)) ((s_sworst7_init) = (init)) (gt (succ (n3)) (s_worst7)) (gt (succ (s_worst7)) (n0)) ((s_worst7_init) = (init)) (gt (succ (n3)) (pv1388)) (gt (n1) (n0)) (gt (succ (pv1388)) (n2)) (gt (n2) (n1)) (gt (succ (n3)) (s_best7)) (gt (succ (s_best7)) (n0)) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) ((s_best7_init) = (init)) ### DisjTree 1 2 9 20 58 65 % 33.35/33.52 67. ((s_best7_init) = (init)) ((s_best7_init) != (init)) ### Axiom % 33.35/33.52 68. ((s_worst7_init) = (init)) ((s_worst7_init) != (init)) ### Axiom % 33.35/33.52 69. ((s_sworst7_init) = (init)) ((s_sworst7_init) != (init)) ### Axiom % 33.35/33.52 70. ((s_best7_init) = (init)) ((s_best7_init) != (init)) ### Axiom % 33.35/33.52 71. ((s_sworst7_init) = (init)) ((s_sworst7_init) != (init)) ### Axiom % 33.35/33.52 72. ((s_worst7_init) = (init)) ((s_worst7_init) != (init)) ### Axiom % 33.35/33.52 73. (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (-. (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init))))))) ### Axiom % 33.35/33.52 74. (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (-. (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init))))) ### Axiom % 33.35/33.52 75. (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (-. (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init))))) ### Axiom % 33.35/33.52 76. (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))) (-. (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init))))) ### Axiom % 33.35/33.52 77. (-. ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))) (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))) ### NotImply 76 % 33.35/33.52 78. (-. (((s_best7_init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))) (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (gt (succ (n3)) (s_worst7)) (gt (succ (n3)) (s_sworst7)) (gt (succ (n3)) (s_best7)) (gt (succ (s_worst7)) (n0)) (gt (succ (s_sworst7)) (n0)) (gt (succ (s_best7)) (n0)) ((s_worst7_init) = (init)) ((s_sworst7_init) = (init)) ((s_best7_init) = (init)) ### DisjTree 70 71 72 4 31 23 6 33 25 73 74 75 77 % 33.35/33.52 79. (-. ((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7)))) => (((s_best7_init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init))))))))))))))))))) ((s_best7_init) = (init)) ((s_sworst7_init) = (init)) ((s_worst7_init) = (init)) (gt (succ (s_best7)) (n0)) (gt (succ (s_sworst7)) (n0)) (gt (succ (s_worst7)) (n0)) (gt (succ (n3)) (s_best7)) (gt (succ (n3)) (s_sworst7)) (gt (succ (n3)) (s_worst7)) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))) ### NotImply 78 % 33.35/33.52 80. ((s_best7_init) = (init)) ((s_best7_init) != (init)) ### Axiom % 33.35/33.52 81. ((s_worst7_init) = (init)) ((s_worst7_init) != (init)) ### Axiom % 33.35/33.52 82. (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (-. (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init))))))) ### Axiom % 33.35/33.52 83. (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (-. (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init))))) ### Axiom % 33.35/33.52 84. (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (-. (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init))))) ### Axiom % 33.35/33.52 85. (-. (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))) (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (gt (succ (n3)) (pv1388)) (gt (succ (n3)) (s_worst7)) (gt (succ (n3)) (s_best7)) (gt (n1) (n0)) (gt (succ (pv1388)) (n2)) (gt (n2) (n1)) (gt (succ (s_worst7)) (n0)) (gt (succ (s_best7)) (n0)) ((s_worst7_init) = (init)) ((s_best7_init) = (init)) ### DisjTree 1 80 81 4 23 15 6 25 17 82 83 84 77 % 33.35/33.52 86. (-. ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init))))))))))))))))))) ((s_best7_init) = (init)) ((s_worst7_init) = (init)) (gt (succ (s_best7)) (n0)) (gt (succ (s_worst7)) (n0)) (gt (n2) (n1)) (gt (succ (pv1388)) (n2)) (gt (n1) (n0)) (gt (succ (n3)) (s_best7)) (gt (succ (n3)) (s_worst7)) (gt (succ (n3)) (pv1388)) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))) ### NotImply 85 % 33.35/33.52 87. (-. (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_sworst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7)))) => (((s_best7_init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (gt (succ (n3)) (s_worst7)) (gt (succ (n3)) (s_best7)) (gt (succ (s_worst7)) (n0)) (gt (succ (s_best7)) (n0)) ((s_worst7_init) = (init)) ((s_best7_init) = (init)) (gt (succ (n3)) (pv1388)) (gt (n1) (n0)) (gt (succ (pv1388)) (n2)) (gt (n2) (n1)) (gt (succ (n3)) (s_sworst7)) (gt (succ (s_sworst7)) (n0)) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) ((s_sworst7_init) = (init)) ### DisjTree 1 69 36 20 79 86 % 33.35/33.52 88. (-. ((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7)))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_sworst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7)))) => (((s_best7_init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init))))))))))))))))))))))))) ((s_sworst7_init) = (init)) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (gt (succ (s_sworst7)) (n0)) (gt (succ (n3)) (s_sworst7)) (gt (n2) (n1)) (gt (succ (pv1388)) (n2)) (gt (n1) (n0)) (gt (succ (n3)) (pv1388)) ((s_best7_init) = (init)) ((s_worst7_init) = (init)) (gt (succ (s_best7)) (n0)) (gt (succ (s_worst7)) (n0)) (gt (succ (n3)) (s_best7)) (gt (succ (n3)) (s_worst7)) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))) ### NotImply 87 % 33.35/33.52 89. (-. ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init))))))))))))))))))) ((s_best7_init) = (init)) ((s_worst7_init) = (init)) (gt (succ (s_best7)) (n0)) (gt (succ (s_worst7)) (n0)) (gt (n2) (n1)) (gt (succ (pv1388)) (n2)) (gt (n1) (n0)) (gt (succ (n3)) (s_best7)) (gt (succ (n3)) (s_worst7)) (gt (succ (n3)) (pv1388)) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))) ### NotImply 85 % 33.35/33.52 90. (-. (((init) = (init)) /\ (((s_worst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_worst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7)))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_sworst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7)))) => (((s_best7_init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (gt (succ (n3)) (s_best7)) (gt (succ (s_best7)) (n0)) ((s_best7_init) = (init)) (gt (succ (n3)) (s_sworst7)) (gt (succ (s_sworst7)) (n0)) ((s_sworst7_init) = (init)) (gt (succ (n3)) (pv1388)) (gt (n1) (n0)) (gt (succ (pv1388)) (n2)) (gt (n2) (n1)) (gt (succ (n3)) (s_worst7)) (gt (succ (s_worst7)) (n0)) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) ((s_worst7_init) = (init)) ### DisjTree 1 68 28 20 88 89 % 33.35/33.52 91. (-. ((-. (gt (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_best7)))) => (((init) = (init)) /\ (((s_worst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_worst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7)))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_sworst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7)))) => (((s_best7_init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init))))))))))))))))))))))))) ((s_worst7_init) = (init)) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (gt (succ (s_worst7)) (n0)) (gt (succ (n3)) (s_worst7)) (gt (n2) (n1)) (gt (succ (pv1388)) (n2)) (gt (n1) (n0)) (gt (succ (n3)) (pv1388)) ((s_sworst7_init) = (init)) (gt (succ (s_sworst7)) (n0)) (gt (succ (n3)) (s_sworst7)) ((s_best7_init) = (init)) (gt (succ (s_best7)) (n0)) (gt (succ (n3)) (s_best7)) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))) ### NotImply 90 % 33.35/33.52 92. ((s_sworst7_init) = (init)) ((s_sworst7_init) != (init)) ### Axiom % 33.35/33.52 93. ((s_worst7_init) = (init)) ((s_worst7_init) != (init)) ### Axiom % 33.35/33.52 94. (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (-. (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init))))))) ### Axiom % 33.35/33.52 95. (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (-. (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init))))) ### Axiom % 33.35/33.52 96. (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (-. (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init))))) ### Axiom % 33.35/33.52 97. (-. (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))) (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (gt (succ (n3)) (pv1388)) (gt (succ (n3)) (s_worst7)) (gt (succ (n3)) (s_sworst7)) (gt (n1) (n0)) (gt (succ (pv1388)) (n2)) (gt (n2) (n1)) (gt (succ (s_worst7)) (n0)) (gt (succ (s_sworst7)) (n0)) ((s_worst7_init) = (init)) ((s_sworst7_init) = (init)) ### DisjTree 1 92 93 31 23 15 33 25 17 94 95 96 77 % 33.35/33.52 98. (-. ((gt (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_best7))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init))))))))))))))))))) ((s_sworst7_init) = (init)) ((s_worst7_init) = (init)) (gt (succ (s_sworst7)) (n0)) (gt (succ (s_worst7)) (n0)) (gt (n2) (n1)) (gt (succ (pv1388)) (n2)) (gt (n1) (n0)) (gt (succ (n3)) (s_sworst7)) (gt (succ (n3)) (s_worst7)) (gt (succ (n3)) (pv1388)) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))) ### NotImply 97 % 33.35/33.52 99. (-. (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_best7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (gt (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_best7)))) => (((init) = (init)) /\ (((s_worst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_worst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7)))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_sworst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7)))) => (((s_best7_init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) /\ ((gt (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_best7))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (gt (succ (n3)) (s_sworst7)) (gt (succ (s_sworst7)) (n0)) ((s_sworst7_init) = (init)) (gt (succ (n3)) (s_worst7)) (gt (succ (s_worst7)) (n0)) ((s_worst7_init) = (init)) (gt (succ (n3)) (pv1388)) (gt (n1) (n0)) (gt (succ (pv1388)) (n2)) (gt (n2) (n1)) (gt (succ (n3)) (s_best7)) (gt (succ (s_best7)) (n0)) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) ((s_best7_init) = (init)) ### DisjTree 1 67 9 20 91 98 % 33.35/33.52 100. ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init))))) ((s_best7_init) = (init)) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (gt (succ (s_best7)) (n0)) (gt (succ (n3)) (s_best7)) (gt (n2) (n1)) (gt (succ (pv1388)) (n2)) (gt (n1) (n0)) (gt (succ (n3)) (pv1388)) ((s_worst7_init) = (init)) (gt (succ (s_worst7)) (n0)) (gt (succ (n3)) (s_worst7)) ((s_sworst7_init) = (init)) (gt (succ (s_sworst7)) (n0)) (gt (succ (n3)) (s_sworst7)) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (-. (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_best7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (gt (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_best7)))) => (((init) = (init)) /\ (((s_worst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_worst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7)))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_sworst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7)))) => (((s_best7_init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) /\ ((gt (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_best7))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) ### Imply 66 99 % 33.35/33.52 101. (leq (pv1388) (n3)) (-. (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_best7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (gt (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_best7)))) => (((init) = (init)) /\ (((s_worst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_worst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7)))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_sworst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7)))) => (((s_best7_init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) /\ ((gt (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_best7))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (gt (succ (n3)) (s_sworst7)) (gt (succ (s_sworst7)) (n0)) ((s_sworst7_init) = (init)) (gt (succ (n3)) (s_worst7)) (gt (succ (s_worst7)) (n0)) ((s_worst7_init) = (init)) (gt (n1) (n0)) (gt (succ (pv1388)) (n2)) (gt (n2) (n1)) (gt (succ (n3)) (s_best7)) (gt (succ (s_best7)) (n0)) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) ((s_best7_init) = (init)) ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init))))) ### Definition-Pseudo(leq) 100 % 33.35/33.52 102. (leq (s_worst7) (n3)) ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init))))) ((s_best7_init) = (init)) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (gt (succ (s_best7)) (n0)) (gt (succ (n3)) (s_best7)) (gt (n2) (n1)) (gt (succ (pv1388)) (n2)) (gt (n1) (n0)) ((s_worst7_init) = (init)) (gt (succ (s_worst7)) (n0)) ((s_sworst7_init) = (init)) (gt (succ (s_sworst7)) (n0)) (gt (succ (n3)) (s_sworst7)) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (-. (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_best7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (gt (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_best7)))) => (((init) = (init)) /\ (((s_worst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_worst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7)))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_sworst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7)))) => (((s_best7_init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) /\ ((gt (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_best7))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) (leq (pv1388) (n3)) ### Definition-Pseudo(leq) 101 % 33.35/33.52 103. (leq (s_sworst7) (n3)) (leq (pv1388) (n3)) (-. (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_best7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (gt (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_best7)))) => (((init) = (init)) /\ (((s_worst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_worst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7)))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_sworst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7)))) => (((s_best7_init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) /\ ((gt (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_best7))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (gt (succ (s_sworst7)) (n0)) ((s_sworst7_init) = (init)) (gt (succ (s_worst7)) (n0)) ((s_worst7_init) = (init)) (gt (n1) (n0)) (gt (succ (pv1388)) (n2)) (gt (n2) (n1)) (gt (succ (n3)) (s_best7)) (gt (succ (s_best7)) (n0)) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) ((s_best7_init) = (init)) ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init))))) (leq (s_worst7) (n3)) ### Definition-Pseudo(leq) 102 % 33.35/33.52 104. (leq (s_best7) (n3)) (leq (s_worst7) (n3)) ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init))))) ((s_best7_init) = (init)) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (gt (succ (s_best7)) (n0)) (gt (n2) (n1)) (gt (succ (pv1388)) (n2)) (gt (n1) (n0)) ((s_worst7_init) = (init)) (gt (succ (s_worst7)) (n0)) ((s_sworst7_init) = (init)) (gt (succ (s_sworst7)) (n0)) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (-. (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_best7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (gt (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_best7)))) => (((init) = (init)) /\ (((s_worst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_worst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7)))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_sworst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7)))) => (((s_best7_init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) /\ ((gt (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_best7))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) (leq (pv1388) (n3)) (leq (s_sworst7) (n3)) ### Definition-Pseudo(leq) 103 % 33.35/33.52 105. (leq (n2) (pv1388)) (leq (s_sworst7) (n3)) (leq (pv1388) (n3)) (-. (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_best7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (gt (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_best7)))) => (((init) = (init)) /\ (((s_worst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_worst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7)))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_sworst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7)))) => (((s_best7_init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) /\ ((gt (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_best7))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (gt (succ (s_sworst7)) (n0)) ((s_sworst7_init) = (init)) (gt (succ (s_worst7)) (n0)) ((s_worst7_init) = (init)) (gt (n1) (n0)) (gt (n2) (n1)) (gt (succ (s_best7)) (n0)) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) ((s_best7_init) = (init)) ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init))))) (leq (s_worst7) (n3)) (leq (s_best7) (n3)) ### Definition-Pseudo(leq) 104 % 33.35/33.52 106. (leq (n0) (s_worst7)) (leq (s_best7) (n3)) (leq (s_worst7) (n3)) ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init))))) ((s_best7_init) = (init)) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (gt (succ (s_best7)) (n0)) (gt (n2) (n1)) (gt (n1) (n0)) ((s_worst7_init) = (init)) ((s_sworst7_init) = (init)) (gt (succ (s_sworst7)) (n0)) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (-. (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_best7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (gt (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_best7)))) => (((init) = (init)) /\ (((s_worst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_worst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7)))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_sworst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7)))) => (((s_best7_init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) /\ ((gt (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_best7))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) (leq (pv1388) (n3)) (leq (s_sworst7) (n3)) (leq (n2) (pv1388)) ### Definition-Pseudo(leq) 105 % 33.35/33.52 107. (leq (n0) (s_sworst7)) (leq (n2) (pv1388)) (leq (s_sworst7) (n3)) (leq (pv1388) (n3)) (-. (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_best7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (gt (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_best7)))) => (((init) = (init)) /\ (((s_worst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_worst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7)))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_sworst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7)))) => (((s_best7_init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) /\ ((gt (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_best7))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) ((s_sworst7_init) = (init)) ((s_worst7_init) = (init)) (gt (n1) (n0)) (gt (n2) (n1)) (gt (succ (s_best7)) (n0)) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) ((s_best7_init) = (init)) ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init))))) (leq (s_worst7) (n3)) (leq (s_best7) (n3)) (leq (n0) (s_worst7)) ### Definition-Pseudo(leq) 106 % 33.35/33.52 108. (leq (n0) (s_best7)) (leq (n0) (s_worst7)) (leq (s_best7) (n3)) (leq (s_worst7) (n3)) ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init))))) ((s_best7_init) = (init)) (All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) (gt (n2) (n1)) (gt (n1) (n0)) ((s_worst7_init) = (init)) ((s_sworst7_init) = (init)) (All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) (All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) (-. (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_best7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (gt (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_best7)))) => (((init) = (init)) /\ (((s_worst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_worst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7)))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_sworst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7)))) => (((s_best7_init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) /\ ((gt (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_best7))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) (leq (pv1388) (n3)) (leq (s_sworst7) (n3)) (leq (n2) (pv1388)) (leq (n0) (s_sworst7)) ### Definition-Pseudo(leq) 107 % 33.35/33.52 109. (-. ((((s_best7_init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n2) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init))))))))))))))))))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_best7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (gt (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_best7)))) => (((init) = (init)) /\ (((s_worst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_worst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7)))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((a_select2 (s_values7_init) (s_sworst7)) = (init)) /\ (((a_select2 (s_values7_init) (pv1388)) = (init)) /\ (((-. (leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7)))) => (((s_best7_init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_sworst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) /\ ((leq (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_worst7))) => (((init) = (init)) /\ (((s_best7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_best7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_best7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init)))))))))))))))))))))))) /\ ((gt (a_select2 (s_values7) (pv1388)) (a_select2 (s_values7) (s_best7))) => (((init) = (init)) /\ (((s_sworst7_init) = (init)) /\ (((s_worst7_init) = (init)) /\ ((leq (n0) (s_sworst7)) /\ ((leq (n0) (s_worst7)) /\ ((leq (n0) (pv1388)) /\ ((leq (s_sworst7) (n3)) /\ ((leq (s_worst7) (n3)) /\ ((leq (pv1388) (n3)) /\ ((All A, (((leq (n0) A) /\ (leq A (n2))) => (All B, (((leq (n0) B) /\ (leq B (n3))) => ((a_select3 (simplex7_init) B A) = (init)))))) /\ ((All C, (((leq (n0) C) /\ (leq C (n3))) => ((a_select2 (s_values7_init) C) = (init)))) /\ ((All D, (((leq (n0) D) /\ (leq D (n2))) => ((a_select2 (s_center7_init) D) = (init)))) /\ ((gt (loopcounter) (n1)) => (((pvar1400_init) = (init)) /\ (((pvar1401_init) = (init)) /\ ((pvar1402_init) = (init))))))))))))))))))))))))) (gt (n1) (n0)) (gt (n2) (n1)) ### ConjTree 108 % 33.35/33.53 % SZS output end Proof % 33.35/33.53 (* END-PROOF *) %------------------------------------------------------------------------------