%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SWV406+1 : TPTP v8.1.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n009.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:51:15 EDT 2022 % Result : Theorem 12.14s 12.32s % Output : Proof 12.34s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.11 % Problem : SWV406+1 : TPTP v8.1.0. Released v3.3.0. % 0.11/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n009.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Wed Jun 15 09:38:23 EDT 2022 % 0.18/0.33 % CPUTime : % 12.14/12.32 % SZS status Theorem % 12.14/12.32 (* PROOF-FOUND *) % 12.14/12.32 (* BEGIN-PROOF *) % 12.14/12.32 % SZS output start Proof % 12.14/12.32 1. (pair_in_list T_0 T_1 T_2) (-. (pair_in_list T_0 T_1 T_2)) ### Axiom % 12.14/12.32 2. (pair_in_list T_0 T_1 T_2) (-. (pair_in_list T_0 T_1 T_2)) ### Axiom % 12.14/12.32 3. (-. (pair_in_list (insert_slb T_0 (pair T_3 T_4)) T_1 T_2)) (pair_in_list T_0 T_1 T_2) ### Extension/test/not_ax23 1 2 % 12.14/12.32 4. (-. (less_than T_2 T_1)) (less_than T_2 T_1) ### Axiom % 12.14/12.32 5. ((pair_in_list (insert_slb T_0 (pair T_3 T_4)) T_1 T_2) => (less_than T_2 T_1)) (-. (less_than T_2 T_1)) (pair_in_list T_0 T_1 T_2) ### Imply 3 4 % 12.14/12.32 6. (All X5, ((pair_in_list (insert_slb T_0 (pair T_3 T_4)) T_1 X5) => (less_than X5 T_1))) (pair_in_list T_0 T_1 T_2) (-. (less_than T_2 T_1)) ### All 5 % 12.14/12.32 7. (All X4, (All X5, ((pair_in_list (insert_slb T_0 (pair T_3 T_4)) X4 X5) => (less_than X5 X4)))) (-. (less_than T_2 T_1)) (pair_in_list T_0 T_1 T_2) ### All 6 % 12.14/12.32 8. (-. ((pair_in_list T_0 T_1 T_2) => (less_than T_2 T_1))) (All X4, (All X5, ((pair_in_list (insert_slb T_0 (pair T_3 T_4)) X4 X5) => (less_than X5 X4)))) ### NotImply 7 % 12.14/12.32 9. (-. (All Y, ((pair_in_list T_0 T_1 Y) => (less_than Y T_1)))) (All X4, (All X5, ((pair_in_list (insert_slb T_0 (pair T_3 T_4)) X4 X5) => (less_than X5 X4)))) ### NotAllEx 8 % 12.14/12.32 10. (-. (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))) (All X4, (All X5, ((pair_in_list (insert_slb T_0 (pair T_3 T_4)) X4 X5) => (less_than X5 X4)))) ### NotAllEx 9 % 12.14/12.32 11. (less_than (bottom) T_3) (-. (less_than (bottom) T_3)) ### Axiom % 12.14/12.32 12. (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (-. (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))) ### Axiom % 12.14/12.32 13. (-. (check_cpq (triple T_5 T_0 T_6))) (check_cpq (triple T_5 T_0 T_6)) ### Axiom % 12.14/12.32 14. ((check_cpq (triple T_5 T_0 T_6)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))) (-. (check_cpq (triple T_5 T_0 T_6))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) ### Equiv 12 13 % 12.14/12.32 15. (All W, ((check_cpq (triple T_5 T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (-. (check_cpq (triple T_5 T_0 T_6))) ### All 14 % 12.14/12.32 16. (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (-. (check_cpq (triple T_5 T_0 T_6))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) ### All 15 % 12.14/12.32 17. (T_3 != T_3) ### Refl(=) % 12.14/12.32 18. (T_4 != T_4) ### Refl(=) % 12.14/12.32 19. (-. (pair_in_list (insert_slb T_0 (pair T_3 T_4)) T_3 T_4)) ### Extension/test/not_ax23 17 18 % 12.14/12.32 20. (-. (less_than T_4 T_3)) (less_than T_4 T_3) ### Axiom % 12.14/12.32 21. ((pair_in_list (insert_slb T_0 (pair T_3 T_4)) T_3 T_4) => (less_than T_4 T_3)) (-. (less_than T_4 T_3)) ### Imply 19 20 % 12.14/12.32 22. (All X5, ((pair_in_list (insert_slb T_0 (pair T_3 T_4)) T_3 X5) => (less_than X5 T_3))) (-. (less_than T_4 T_3)) ### All 21 % 12.14/12.32 23. (check_cpq (triple T_5 T_0 T_6)) (-. (check_cpq (triple T_5 T_0 T_6))) ### Axiom % 12.14/12.32 24. (-. (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) ### Axiom % 12.14/12.32 25. ((check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) <=> (check_cpq (triple T_5 T_0 T_6))) (-. (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6))) (check_cpq (triple T_5 T_0 T_6)) ### Equiv 23 24 % 12.14/12.32 26. ((less_than T_4 T_3) => ((check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) <=> (check_cpq (triple T_5 T_0 T_6)))) (check_cpq (triple T_5 T_0 T_6)) (-. (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6))) (All X5, ((pair_in_list (insert_slb T_0 (pair T_3 T_4)) T_3 X5) => (less_than X5 T_3))) ### Imply 22 25 % 12.14/12.32 27. (All Y, ((less_than Y T_3) => ((check_cpq (triple T_5 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> (check_cpq (triple T_5 T_0 T_6))))) (All X5, ((pair_in_list (insert_slb T_0 (pair T_3 T_4)) T_3 X5) => (less_than X5 T_3))) (-. (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6))) (check_cpq (triple T_5 T_0 T_6)) ### All 26 % 12.14/12.32 28. (All X, (All Y, ((less_than Y X) => ((check_cpq (triple T_5 (insert_slb T_0 (pair X Y)) T_6)) <=> (check_cpq (triple T_5 T_0 T_6)))))) (check_cpq (triple T_5 T_0 T_6)) (-. (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6))) (All X5, ((pair_in_list (insert_slb T_0 (pair T_3 T_4)) T_3 X5) => (less_than X5 T_3))) ### All 27 % 12.14/12.32 29. ((check_cpq (triple T_5 (insert_slb T_0 (pair T_3 (bottom))) T_6)) <=> (check_cpq (triple T_5 T_0 T_6))) (All X5, ((pair_in_list (insert_slb T_0 (pair T_3 T_4)) T_3 X5) => (less_than X5 T_3))) (-. (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6))) (All X, (All Y, ((less_than Y X) => ((check_cpq (triple T_5 (insert_slb T_0 (pair X Y)) T_6)) <=> (check_cpq (triple T_5 T_0 T_6)))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) ### Equiv 16 28 % 12.14/12.32 30. ((less_than (bottom) T_3) => ((check_cpq (triple T_5 (insert_slb T_0 (pair T_3 (bottom))) T_6)) <=> (check_cpq (triple T_5 T_0 T_6)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All X, (All Y, ((less_than Y X) => ((check_cpq (triple T_5 (insert_slb T_0 (pair X Y)) T_6)) <=> (check_cpq (triple T_5 T_0 T_6)))))) (-. (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6))) (All X5, ((pair_in_list (insert_slb T_0 (pair T_3 T_4)) T_3 X5) => (less_than X5 T_3))) (less_than (bottom) T_3) ### Imply 11 29 % 12.14/12.32 31. (All Y, ((less_than Y T_3) => ((check_cpq (triple T_5 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> (check_cpq (triple T_5 T_0 T_6))))) (less_than (bottom) T_3) (All X5, ((pair_in_list (insert_slb T_0 (pair T_3 T_4)) T_3 X5) => (less_than X5 T_3))) (-. (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6))) (All X, (All Y, ((less_than Y X) => ((check_cpq (triple T_5 (insert_slb T_0 (pair X Y)) T_6)) <=> (check_cpq (triple T_5 T_0 T_6)))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) ### All 30 % 12.14/12.32 32. (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All X, (All Y, ((less_than Y X) => ((check_cpq (triple T_5 (insert_slb T_0 (pair X Y)) T_6)) <=> (check_cpq (triple T_5 T_0 T_6)))))) (-. (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6))) (All X5, ((pair_in_list (insert_slb T_0 (pair T_3 T_4)) T_3 X5) => (less_than X5 T_3))) (less_than (bottom) T_3) ### All 31 % 12.14/12.32 33. (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple T_5 (insert_slb T_0 (pair X Y)) W)) <=> (check_cpq (triple T_5 T_0 W))))))) (less_than (bottom) T_3) (All X5, ((pair_in_list (insert_slb T_0 (pair T_3 T_4)) T_3 X5) => (less_than X5 T_3))) (-. (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) ### All 32 % 12.14/12.32 34. (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple T_5 (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple T_5 V W)))))))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (-. (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6))) (All X5, ((pair_in_list (insert_slb T_0 (pair T_3 T_4)) T_3 X5) => (less_than X5 T_3))) (less_than (bottom) T_3) ### All 33 % 12.14/12.32 35. (All U, (less_than (bottom) U)) (All X5, ((pair_in_list (insert_slb T_0 (pair T_3 T_4)) T_3 X5) => (less_than X5 T_3))) (-. (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple T_5 (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple T_5 V W)))))))) ### All 34 % 12.14/12.35 36. (All X4, (All X5, ((pair_in_list (insert_slb T_0 (pair T_3 T_4)) X4 X5) => (less_than X5 X4)))) (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple T_5 (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple T_5 V W)))))))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (-. (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6))) (All U, (less_than (bottom) U)) ### All 35 % 12.14/12.35 37. (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (All U, (less_than (bottom) U)) (-. (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X4, (All X5, ((pair_in_list (insert_slb T_0 (pair T_3 T_4)) X4 X5) => (less_than X5 X4)))) ### All 36 % 12.14/12.35 38. ((check_cpq (triple zenon_X7 T_0 zenon_X8)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (-. (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6))) (All U, (less_than (bottom) U)) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (All X4, (All X5, ((pair_in_list (insert_slb T_0 (pair T_3 T_4)) X4 X5) => (less_than X5 X4)))) ### Equiv 10 37 % 12.14/12.35 39. (All W, ((check_cpq (triple zenon_X7 T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))))) (All X4, (All X5, ((pair_in_list (insert_slb T_0 (pair T_3 T_4)) X4 X5) => (less_than X5 X4)))) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (All U, (less_than (bottom) U)) (-. (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) ### All 38 % 12.14/12.35 40. (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (-. (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6))) (All U, (less_than (bottom) U)) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (All X4, (All X5, ((pair_in_list (insert_slb T_0 (pair T_3 T_4)) X4 X5) => (less_than X5 X4)))) ### All 39 % 12.14/12.35 41. (-. (less_than T_4 T_3)) (less_than T_4 T_3) ### Axiom % 12.14/12.35 42. (-. (less_than T_3 T_4)) (less_than T_3 T_4) ### Axiom % 12.14/12.35 43. ((less_than T_4 T_3) \/ (less_than T_3 T_4)) (-. (less_than T_3 T_4)) (-. (less_than T_4 T_3)) ### Or 41 42 % 12.14/12.35 44. (All V, ((less_than T_4 V) \/ (less_than V T_4))) (-. (less_than T_4 T_3)) (-. (less_than T_3 T_4)) ### All 43 % 12.14/12.35 45. (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (-. (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6))) ### Axiom % 12.14/12.35 46. (-. (check_cpq (triple T_5 T_0 T_6))) (check_cpq (triple T_5 T_0 T_6)) ### Axiom % 12.14/12.35 47. ((check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) <=> (check_cpq (triple T_5 T_0 T_6))) (-. (check_cpq (triple T_5 T_0 T_6))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) ### Equiv 45 46 % 12.14/12.35 48. ((less_than T_4 T_3) => ((check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) <=> (check_cpq (triple T_5 T_0 T_6)))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (-. (check_cpq (triple T_5 T_0 T_6))) (-. (less_than T_3 T_4)) (All V, ((less_than T_4 V) \/ (less_than V T_4))) ### Imply 44 47 % 12.14/12.35 49. (All Y, ((less_than Y T_3) => ((check_cpq (triple T_5 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> (check_cpq (triple T_5 T_0 T_6))))) (All V, ((less_than T_4 V) \/ (less_than V T_4))) (-. (less_than T_3 T_4)) (-. (check_cpq (triple T_5 T_0 T_6))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) ### All 48 % 12.14/12.35 50. (less_than T_4 T_3) (-. (less_than T_4 T_3)) ### Axiom % 12.14/12.35 51. ((less_than T_4 T_3) => ((check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) <=> (check_cpq (triple T_5 T_0 T_6)))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (-. (check_cpq (triple T_5 T_0 T_6))) (less_than T_4 T_3) ### Imply 50 47 % 12.14/12.35 52. (All Y, ((less_than Y T_3) => ((check_cpq (triple T_5 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> (check_cpq (triple T_5 T_0 T_6))))) (less_than T_4 T_3) (-. (check_cpq (triple T_5 T_0 T_6))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) ### All 51 % 12.14/12.35 53. (-. (strictly_less_than T_3 T_4)) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (-. (check_cpq (triple T_5 T_0 T_6))) (All V, ((less_than T_4 V) \/ (less_than V T_4))) (All Y, ((less_than Y T_3) => ((check_cpq (triple T_5 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> (check_cpq (triple T_5 T_0 T_6))))) ### Extension/test/not_stricly_smaller_definition 49 52 % 12.14/12.35 54. (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (-. (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6))) ### Axiom % 12.14/12.35 55. False ### False % 12.14/12.35 56. ((check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) <=> False) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) ### Equiv 54 55 % 12.14/12.35 57. ((strictly_less_than T_3 T_4) => ((check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) <=> False)) (All Y, ((less_than Y T_3) => ((check_cpq (triple T_5 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> (check_cpq (triple T_5 T_0 T_6))))) (All V, ((less_than T_4 V) \/ (less_than V T_4))) (-. (check_cpq (triple T_5 T_0 T_6))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) ### Imply 53 56 % 12.14/12.35 58. (All Y, ((strictly_less_than T_3 Y) => ((check_cpq (triple T_5 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> False))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (-. (check_cpq (triple T_5 T_0 T_6))) (All V, ((less_than T_4 V) \/ (less_than V T_4))) (All Y, ((less_than Y T_3) => ((check_cpq (triple T_5 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> (check_cpq (triple T_5 T_0 T_6))))) ### All 57 % 12.14/12.35 59. (All X, (All Y, ((less_than Y X) => ((check_cpq (triple T_5 (insert_slb T_0 (pair X Y)) T_6)) <=> (check_cpq (triple T_5 T_0 T_6)))))) (All V, ((less_than T_4 V) \/ (less_than V T_4))) (-. (check_cpq (triple T_5 T_0 T_6))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All Y, ((strictly_less_than T_3 Y) => ((check_cpq (triple T_5 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> False))) ### All 58 % 12.14/12.35 60. (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple T_5 (insert_slb T_0 (pair X Y)) T_6)) <=> False)))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (-. (check_cpq (triple T_5 T_0 T_6))) (All V, ((less_than T_4 V) \/ (less_than V T_4))) (All X, (All Y, ((less_than Y X) => ((check_cpq (triple T_5 (insert_slb T_0 (pair X Y)) T_6)) <=> (check_cpq (triple T_5 T_0 T_6)))))) ### All 59 % 12.14/12.35 61. (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple T_5 (insert_slb T_0 (pair X Y)) W)) <=> (check_cpq (triple T_5 T_0 W))))))) (All V, ((less_than T_4 V) \/ (less_than V T_4))) (-. (check_cpq (triple T_5 T_0 T_6))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple T_5 (insert_slb T_0 (pair X Y)) T_6)) <=> False)))) ### All 60 % 12.14/12.35 62. (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple T_5 (insert_slb T_0 (pair X Y)) W)) <=> False))))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (-. (check_cpq (triple T_5 T_0 T_6))) (All V, ((less_than T_4 V) \/ (less_than V T_4))) (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple T_5 (insert_slb T_0 (pair X Y)) W)) <=> (check_cpq (triple T_5 T_0 W))))))) ### All 61 % 12.14/12.35 63. (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple T_5 (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple T_5 V W)))))))) (All V, ((less_than T_4 V) \/ (less_than V T_4))) (-. (check_cpq (triple T_5 T_0 T_6))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple T_5 (insert_slb T_0 (pair X Y)) W)) <=> False))))) ### All 62 % 12.14/12.36 64. (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple T_5 (insert_slb V (pair X Y)) W)) <=> False)))))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (-. (check_cpq (triple T_5 T_0 T_6))) (All V, ((less_than T_4 V) \/ (less_than V T_4))) (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple T_5 (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple T_5 V W)))))))) ### All 63 % 12.14/12.36 65. (-. (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) ### Axiom % 12.14/12.36 66. ((check_cpq (triple T_5 T_0 T_6)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))) (-. (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))) (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple T_5 (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple T_5 V W)))))))) (All V, ((less_than T_4 V) \/ (less_than V T_4))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple T_5 (insert_slb V (pair X Y)) W)) <=> False)))))) ### Equiv 64 65 % 12.14/12.36 67. (All W, ((check_cpq (triple T_5 T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))))) (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple T_5 (insert_slb V (pair X Y)) W)) <=> False)))))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All V, ((less_than T_4 V) \/ (less_than V T_4))) (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple T_5 (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple T_5 V W)))))))) (-. (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))) ### All 66 % 12.14/12.36 68. (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (-. (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))) (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple T_5 (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple T_5 V W)))))))) (All V, ((less_than T_4 V) \/ (less_than V T_4))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple T_5 (insert_slb V (pair X Y)) W)) <=> False)))))) ### All 67 % 12.14/12.36 69. (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple T_5 (insert_slb V (pair X Y)) W)) <=> False)))))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All V, ((less_than T_4 V) \/ (less_than V T_4))) (-. (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) ### All 68 % 12.14/12.36 70. (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (-. (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))) (All V, ((less_than T_4 V) \/ (less_than V T_4))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) ### All 69 % 12.14/12.36 71. (All U, (All V, ((less_than U V) \/ (less_than V U)))) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (-. (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) ### All 70 % 12.14/12.36 72. (pair_in_list T_0 T_9 T_10) (-. (pair_in_list T_0 T_9 T_10)) ### Axiom % 12.14/12.36 73. (-. (less_than T_10 T_9)) (less_than T_10 T_9) ### Axiom % 12.14/12.36 74. ((pair_in_list T_0 T_9 T_10) => (less_than T_10 T_9)) (-. (less_than T_10 T_9)) (pair_in_list T_0 T_9 T_10) ### Imply 72 73 % 12.14/12.36 75. (All Y, ((pair_in_list T_0 T_9 Y) => (less_than Y T_9))) (pair_in_list T_0 T_9 T_10) (-. (less_than T_10 T_9)) ### All 74 % 12.14/12.36 76. (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (-. (less_than T_10 T_9)) (pair_in_list T_0 T_9 T_10) ### All 75 % 12.14/12.36 77. ((check_cpq (triple zenon_X7 T_0 zenon_X8)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))) (pair_in_list T_0 T_9 T_10) (-. (less_than T_10 T_9)) (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (All U, (All V, ((less_than U V) \/ (less_than V U)))) ### Equiv 71 76 % 12.14/12.36 78. (All W, ((check_cpq (triple zenon_X7 T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))))) (All U, (All V, ((less_than U V) \/ (less_than V U)))) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) (-. (less_than T_10 T_9)) (pair_in_list T_0 T_9 T_10) ### All 77 % 12.14/12.36 79. (pair_in_list T_0 T_9 T_10) (-. (less_than T_10 T_9)) (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (All U, (All V, ((less_than U V) \/ (less_than V U)))) ### All 78 % 12.14/12.36 80. (-. (less_than T_10 T_3)) (less_than T_10 T_3) ### Axiom % 12.14/12.36 81. (-. (less_than T_3 T_10)) (less_than T_3 T_10) ### Axiom % 12.14/12.36 82. ((less_than T_10 T_3) \/ (less_than T_3 T_10)) (-. (less_than T_3 T_10)) (-. (less_than T_10 T_3)) ### Or 80 81 % 12.14/12.36 83. (All V, ((less_than T_10 V) \/ (less_than V T_10))) (-. (less_than T_10 T_3)) (-. (less_than T_3 T_10)) ### All 82 % 12.14/12.36 84. (-. (less_than T_10 T_10)) ### Extension/test/reflexivity % 12.14/12.36 85. (less_than T_9 T_10) (-. (less_than T_9 T_10)) ### Axiom % 12.14/12.36 86. (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (-. (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))) ### Axiom % 12.14/12.36 87. (-. (check_cpq (triple zenon_X11 T_0 T_6))) (check_cpq (triple zenon_X11 T_0 T_6)) ### Axiom % 12.14/12.36 88. ((check_cpq (triple zenon_X11 T_0 T_6)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))) (-. (check_cpq (triple zenon_X11 T_0 T_6))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) ### Equiv 86 87 % 12.14/12.36 89. (All W, ((check_cpq (triple zenon_X11 T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (-. (check_cpq (triple zenon_X11 T_0 T_6))) ### All 88 % 12.14/12.36 90. (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (-. (check_cpq (triple zenon_X11 T_0 T_6))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) ### All 89 % 12.22/12.39 91. (less_than T_3 T_10) (-. (less_than T_3 T_10)) ### Axiom % 12.22/12.39 92. (-. (less_than T_10 T_3)) (less_than T_10 T_3) ### Axiom % 12.22/12.39 93. (-. (strictly_less_than T_3 T_10)) (-. (less_than T_10 T_3)) (less_than T_3 T_10) ### Extension/test/not_stricly_smaller_definition 91 92 % 12.22/12.39 94. (less_than T_4 T_3) (-. (less_than T_4 T_3)) ### Axiom % 12.22/12.39 95. (check_cpq (triple zenon_X11 T_0 T_6)) (-. (check_cpq (triple zenon_X11 T_0 T_6))) ### Axiom % 12.22/12.39 96. (zenon_X11 != zenon_X11) ### Refl(=) % 12.22/12.39 97. (T_0 != T_0) ### Refl(=) % 12.22/12.39 98. (T_3 != T_3) ### Refl(=) % 12.22/12.39 99. (T_4 = T_10) (T_4 != T_10) ### Axiom % 12.22/12.39 100. ((pair T_3 T_4) != (pair T_3 T_10)) (T_4 = T_10) ### NotEqual 98 99 % 12.22/12.39 101. ((insert_slb T_0 (pair T_3 T_4)) != (insert_slb T_0 (pair T_3 T_10))) (T_4 = T_10) ### NotEqual 97 100 % 12.22/12.39 102. (T_6 != T_6) ### Refl(=) % 12.22/12.39 103. ((triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6) != (triple zenon_X11 (insert_slb T_0 (pair T_3 T_10)) T_6)) (T_4 = T_10) ### NotEqual 96 101 102 % 12.22/12.39 104. (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_10)) T_6))) (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6)) (T_4 = T_10) ### P-NotP 103 % 12.22/12.39 105. ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6))) (T_4 = T_10) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_10)) T_6))) (check_cpq (triple zenon_X11 T_0 T_6)) ### Equiv 95 104 % 12.22/12.39 106. ((less_than T_4 T_3) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6)))) (check_cpq (triple zenon_X11 T_0 T_6)) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_10)) T_6))) (T_4 = T_10) (less_than T_4 T_3) ### Imply 94 105 % 12.22/12.39 107. (All Y, ((less_than Y T_3) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6))))) (less_than T_4 T_3) (T_4 = T_10) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_10)) T_6))) (check_cpq (triple zenon_X11 T_0 T_6)) ### All 106 % 12.22/12.39 108. (All X, (All Y, ((less_than Y X) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6)))))) (check_cpq (triple zenon_X11 T_0 T_6)) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_10)) T_6))) (T_4 = T_10) (less_than T_4 T_3) ### All 107 % 12.22/12.39 109. False ### False % 12.22/12.39 110. ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_10)) T_6)) <=> False) (less_than T_4 T_3) (T_4 = T_10) (check_cpq (triple zenon_X11 T_0 T_6)) (All X, (All Y, ((less_than Y X) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6)))))) ### Equiv 108 109 % 12.22/12.39 111. ((strictly_less_than T_3 T_10) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_10)) T_6)) <=> False)) (All X, (All Y, ((less_than Y X) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6)))))) (check_cpq (triple zenon_X11 T_0 T_6)) (T_4 = T_10) (less_than T_4 T_3) (less_than T_3 T_10) (-. (less_than T_10 T_3)) ### Imply 93 110 % 12.22/12.39 112. (All Y, ((strictly_less_than T_3 Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> False))) (-. (less_than T_10 T_3)) (less_than T_3 T_10) (less_than T_4 T_3) (T_4 = T_10) (check_cpq (triple zenon_X11 T_0 T_6)) (All X, (All Y, ((less_than Y X) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6)))))) ### All 111 % 12.22/12.39 113. ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_10 T_9)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6))) (All X, (All Y, ((less_than Y X) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6)))))) (T_4 = T_10) (less_than T_4 T_3) (less_than T_3 T_10) (-. (less_than T_10 T_3)) (All Y, ((strictly_less_than T_3 Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> False))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) ### Equiv 90 112 % 12.22/12.39 114. ((less_than T_9 T_10) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_10 T_9)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All Y, ((strictly_less_than T_3 Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> False))) (-. (less_than T_10 T_3)) (less_than T_3 T_10) (less_than T_4 T_3) (T_4 = T_10) (All X, (All Y, ((less_than Y X) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6)))))) (less_than T_9 T_10) ### Imply 85 113 % 12.22/12.39 115. (All Y, ((less_than Y T_10) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_10 Y)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6))))) (less_than T_9 T_10) (All X, (All Y, ((less_than Y X) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6)))))) (T_4 = T_10) (less_than T_4 T_3) (less_than T_3 T_10) (-. (less_than T_10 T_3)) (All Y, ((strictly_less_than T_3 Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> False))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) ### All 114 % 12.22/12.39 116. (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All Y, ((strictly_less_than T_3 Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> False))) (-. (less_than T_10 T_3)) (less_than T_3 T_10) (less_than T_4 T_3) (T_4 = T_10) (All X, (All Y, ((less_than Y X) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6)))))) (less_than T_9 T_10) ### All 115 % 12.22/12.39 117. (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) W)) <=> (check_cpq (triple zenon_X11 T_0 W))))))) (less_than T_9 T_10) (T_4 = T_10) (less_than T_4 T_3) (less_than T_3 T_10) (-. (less_than T_10 T_3)) (All Y, ((strictly_less_than T_3 Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> False))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) ### All 116 % 12.22/12.39 118. (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple zenon_X11 (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple zenon_X11 V W)))))))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All Y, ((strictly_less_than T_3 Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> False))) (-. (less_than T_10 T_3)) (less_than T_3 T_10) (less_than T_4 T_3) (T_4 = T_10) (less_than T_9 T_10) ### All 117 % 12.22/12.39 119. (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (less_than T_9 T_10) (T_4 = T_10) (less_than T_4 T_3) (less_than T_3 T_10) (-. (less_than T_10 T_3)) (All Y, ((strictly_less_than T_3 Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> False))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) ### All 118 % 12.22/12.39 120. (-. (less_than T_3 T_3)) ### Extension/test/reflexivity % 12.22/12.39 121. (less_than T_9 T_10) (-. (less_than T_9 T_10)) ### Axiom % 12.22/12.39 122. (-. (less_than T_10 T_9)) (less_than T_10 T_9) ### Axiom % 12.22/12.42 123. (-. (strictly_less_than T_9 T_10)) (-. (less_than T_10 T_9)) (less_than T_9 T_10) ### Extension/test/not_stricly_smaller_definition 121 122 % 12.22/12.42 124. (less_than (bottom) T_9) (-. (less_than (bottom) T_9)) ### Axiom % 12.22/12.42 125. (less_than T_10 T_3) (-. (less_than T_10 T_3)) ### Axiom % 12.22/12.42 126. (check_cpq (triple zenon_X11 T_0 T_6)) (-. (check_cpq (triple zenon_X11 T_0 T_6))) ### Axiom % 12.22/12.42 127. (zenon_X11 != zenon_X11) ### Refl(=) % 12.22/12.42 128. (T_0 != T_0) ### Refl(=) % 12.22/12.42 129. (T_3 = T_9) (T_3 != T_9) ### Axiom % 12.22/12.42 130. (T_10 != T_10) ### Refl(=) % 12.22/12.42 131. ((pair T_3 T_10) != (pair T_9 T_10)) (T_3 = T_9) ### NotEqual 129 130 % 12.22/12.42 132. ((insert_slb T_0 (pair T_3 T_10)) != (insert_slb T_0 (pair T_9 T_10))) (T_3 = T_9) ### NotEqual 128 131 % 12.22/12.42 133. (T_6 != T_6) ### Refl(=) % 12.22/12.42 134. ((triple zenon_X11 (insert_slb T_0 (pair T_3 T_10)) T_6) != (triple zenon_X11 (insert_slb T_0 (pair T_9 T_10)) T_6)) (T_3 = T_9) ### NotEqual 127 132 133 % 12.22/12.42 135. (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_9 T_10)) T_6))) (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_10)) T_6)) (T_3 = T_9) ### P-NotP 134 % 12.22/12.42 136. ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_10)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6))) (T_3 = T_9) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_9 T_10)) T_6))) (check_cpq (triple zenon_X11 T_0 T_6)) ### Equiv 126 135 % 12.22/12.42 137. ((less_than T_10 T_3) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_10)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6)))) (check_cpq (triple zenon_X11 T_0 T_6)) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_9 T_10)) T_6))) (T_3 = T_9) (less_than T_10 T_3) ### Imply 125 136 % 12.22/12.42 138. (All Y, ((less_than Y T_3) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6))))) (less_than T_10 T_3) (T_3 = T_9) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_9 T_10)) T_6))) (check_cpq (triple zenon_X11 T_0 T_6)) ### All 137 % 12.22/12.42 139. ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_9 (bottom))) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6))) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_9 T_10)) T_6))) (T_3 = T_9) (less_than T_10 T_3) (All Y, ((less_than Y T_3) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) ### Equiv 90 138 % 12.22/12.42 140. ((less_than (bottom) T_9) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_9 (bottom))) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All Y, ((less_than Y T_3) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6))))) (less_than T_10 T_3) (T_3 = T_9) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_9 T_10)) T_6))) (less_than (bottom) T_9) ### Imply 124 139 % 12.22/12.42 141. (All Y, ((less_than Y T_9) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_9 Y)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6))))) (less_than (bottom) T_9) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_9 T_10)) T_6))) (T_3 = T_9) (less_than T_10 T_3) (All Y, ((less_than Y T_3) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) ### All 140 % 12.22/12.42 142. (All X, (All Y, ((less_than Y X) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6)))))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (less_than T_10 T_3) (T_3 = T_9) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_9 T_10)) T_6))) (less_than (bottom) T_9) (All Y, ((less_than Y T_9) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_9 Y)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6))))) ### All 141 % 12.22/12.42 143. (less_than (bottom) T_9) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_9 T_10)) T_6))) (T_3 = T_9) (less_than T_10 T_3) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((less_than Y X) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6)))))) ### All 142 % 12.22/12.42 144. (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) W)) <=> (check_cpq (triple zenon_X11 T_0 W))))))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (less_than T_10 T_3) (T_3 = T_9) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_9 T_10)) T_6))) (less_than (bottom) T_9) ### All 143 % 12.22/12.42 145. False ### False % 12.22/12.42 146. ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_9 T_10)) T_6)) <=> False) (less_than (bottom) T_9) (T_3 = T_9) (less_than T_10 T_3) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) W)) <=> (check_cpq (triple zenon_X11 T_0 W))))))) ### Equiv 144 145 % 12.22/12.42 147. ((strictly_less_than T_9 T_10) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_9 T_10)) T_6)) <=> False)) (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) W)) <=> (check_cpq (triple zenon_X11 T_0 W))))))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (less_than T_10 T_3) (T_3 = T_9) (less_than (bottom) T_9) (less_than T_9 T_10) (-. (less_than T_10 T_9)) ### Imply 123 146 % 12.22/12.42 148. (All Y, ((strictly_less_than T_9 Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_9 Y)) T_6)) <=> False))) (-. (less_than T_10 T_9)) (less_than T_9 T_10) (less_than (bottom) T_9) (T_3 = T_9) (less_than T_10 T_3) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) W)) <=> (check_cpq (triple zenon_X11 T_0 W))))))) ### All 147 % 12.22/12.42 149. (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple zenon_X11 (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple zenon_X11 V W)))))))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (less_than T_10 T_3) (T_3 = T_9) (less_than (bottom) T_9) (less_than T_9 T_10) (-. (less_than T_10 T_9)) (All Y, ((strictly_less_than T_9 Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_9 Y)) T_6)) <=> False))) ### All 148 % 12.22/12.42 150. (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> False)))) (-. (less_than T_10 T_9)) (less_than T_9 T_10) (less_than (bottom) T_9) (T_3 = T_9) (less_than T_10 T_3) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple zenon_X11 (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple zenon_X11 V W)))))))) ### All 149 % 12.22/12.42 151. (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (less_than T_10 T_3) (T_3 = T_9) (less_than (bottom) T_9) (less_than T_9 T_10) (-. (less_than T_10 T_9)) (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> False)))) ### All 150 % 12.22/12.44 152. (((less_than T_10 T_3) /\ (less_than T_3 T_3)) => (less_than T_10 T_3)) (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> False)))) (-. (less_than T_10 T_9)) (less_than (bottom) T_9) (T_3 = T_9) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All Y, ((strictly_less_than T_3 Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> False))) (less_than T_3 T_10) (less_than T_4 T_3) (T_4 = T_10) (less_than T_9 T_10) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) ### DisjTree 119 120 151 % 12.22/12.44 153. (((less_than T_3 T_10) /\ (less_than T_10 T_10)) => (less_than T_3 T_10)) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (less_than T_9 T_10) (T_4 = T_10) (less_than T_4 T_3) (All Y, ((strictly_less_than T_3 Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> False))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (T_3 = T_9) (less_than (bottom) T_9) (-. (less_than T_10 T_9)) (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> False)))) (((less_than T_10 T_3) /\ (less_than T_3 T_3)) => (less_than T_10 T_3)) (-. (less_than T_10 T_3)) (All V, ((less_than T_10 V) \/ (less_than V T_10))) ### DisjTree 83 84 152 % 12.22/12.44 154. (All W, (((less_than T_3 T_10) /\ (less_than T_10 W)) => (less_than T_3 W))) (All V, ((less_than T_10 V) \/ (less_than V T_10))) (-. (less_than T_10 T_3)) (((less_than T_10 T_3) /\ (less_than T_3 T_3)) => (less_than T_10 T_3)) (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> False)))) (-. (less_than T_10 T_9)) (less_than (bottom) T_9) (T_3 = T_9) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All Y, ((strictly_less_than T_3 Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> False))) (less_than T_4 T_3) (T_4 = T_10) (less_than T_9 T_10) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) ### All 153 % 12.22/12.44 155. (All V, (All W, (((less_than T_3 V) /\ (less_than V W)) => (less_than T_3 W)))) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (less_than T_9 T_10) (T_4 = T_10) (less_than T_4 T_3) (All Y, ((strictly_less_than T_3 Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> False))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (T_3 = T_9) (less_than (bottom) T_9) (-. (less_than T_10 T_9)) (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> False)))) (((less_than T_10 T_3) /\ (less_than T_3 T_3)) => (less_than T_10 T_3)) (-. (less_than T_10 T_3)) (All V, ((less_than T_10 V) \/ (less_than V T_10))) ### All 154 % 12.22/12.44 156. (All V, ((less_than T_10 V) \/ (less_than V T_10))) (((less_than T_10 T_3) /\ (less_than T_3 T_3)) => (less_than T_10 T_3)) (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> False)))) (-. (less_than T_10 T_9)) (less_than (bottom) T_9) (T_3 = T_9) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All Y, ((strictly_less_than T_3 Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> False))) (less_than T_4 T_3) (T_4 = T_10) (less_than T_9 T_10) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (All V, (All W, (((less_than T_3 V) /\ (less_than V W)) => (less_than T_3 W)))) ### DisjTree 155 120 151 % 12.22/12.44 157. (All W, (((less_than T_10 T_3) /\ (less_than T_3 W)) => (less_than T_10 W))) (All V, (All W, (((less_than T_3 V) /\ (less_than V W)) => (less_than T_3 W)))) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (less_than T_9 T_10) (T_4 = T_10) (less_than T_4 T_3) (All Y, ((strictly_less_than T_3 Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> False))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (T_3 = T_9) (less_than (bottom) T_9) (-. (less_than T_10 T_9)) (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> False)))) (All V, ((less_than T_10 V) \/ (less_than V T_10))) ### All 156 % 12.22/12.44 158. (All V, (All W, (((less_than T_10 V) /\ (less_than V W)) => (less_than T_10 W)))) (All V, ((less_than T_10 V) \/ (less_than V T_10))) (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> False)))) (-. (less_than T_10 T_9)) (less_than (bottom) T_9) (T_3 = T_9) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All Y, ((strictly_less_than T_3 Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> False))) (less_than T_4 T_3) (T_4 = T_10) (less_than T_9 T_10) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (All V, (All W, (((less_than T_3 V) /\ (less_than V W)) => (less_than T_3 W)))) ### All 157 % 12.22/12.44 159. (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (less_than T_9 T_10) (T_4 = T_10) (less_than T_4 T_3) (All Y, ((strictly_less_than T_3 Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> False))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (T_3 = T_9) (less_than (bottom) T_9) (-. (less_than T_10 T_9)) (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> False)))) (All V, ((less_than T_10 V) \/ (less_than V T_10))) (All V, (All W, (((less_than T_10 V) /\ (less_than V W)) => (less_than T_10 W)))) ### All 158 % 12.22/12.44 160. (All V, ((less_than T_10 V) \/ (less_than V T_10))) (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> False)))) (-. (less_than T_10 T_9)) (less_than (bottom) T_9) (T_3 = T_9) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All Y, ((strictly_less_than T_3 Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> False))) (less_than T_4 T_3) (T_4 = T_10) (less_than T_9 T_10) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) ### All 159 % 12.22/12.47 161. (-. (less_than T_3 T_4)) (less_than T_3 T_4) ### Axiom % 12.22/12.47 162. ((less_than T_4 T_3) \/ (less_than T_3 T_4)) (-. (less_than T_3 T_4)) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (less_than T_9 T_10) (T_4 = T_10) (All Y, ((strictly_less_than T_3 Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> False))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (T_3 = T_9) (less_than (bottom) T_9) (-. (less_than T_10 T_9)) (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> False)))) (All V, ((less_than T_10 V) \/ (less_than V T_10))) ### Or 160 161 % 12.22/12.47 163. (All V, ((less_than T_4 V) \/ (less_than V T_4))) (All V, ((less_than T_10 V) \/ (less_than V T_10))) (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> False)))) (-. (less_than T_10 T_9)) (less_than (bottom) T_9) (T_3 = T_9) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All Y, ((strictly_less_than T_3 Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> False))) (T_4 = T_10) (less_than T_9 T_10) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) (-. (less_than T_3 T_4)) ### All 162 % 12.22/12.47 164. (All U, (All V, ((less_than U V) \/ (less_than V U)))) (-. (less_than T_3 T_4)) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (less_than T_9 T_10) (T_4 = T_10) (All Y, ((strictly_less_than T_3 Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> False))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (T_3 = T_9) (less_than (bottom) T_9) (-. (less_than T_10 T_9)) (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> False)))) (All V, ((less_than T_10 V) \/ (less_than V T_10))) ### All 163 % 12.22/12.47 165. (-. (strictly_less_than T_3 T_4)) (All V, ((less_than T_10 V) \/ (less_than V T_10))) (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> False)))) (-. (less_than T_10 T_9)) (less_than (bottom) T_9) (T_3 = T_9) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All Y, ((strictly_less_than T_3 Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> False))) (T_4 = T_10) (less_than T_9 T_10) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) (All U, (All V, ((less_than U V) \/ (less_than V U)))) ### Extension/test/not_stricly_smaller_definition 164 160 % 12.22/12.47 166. (less_than T_9 T_10) (-. (less_than T_9 T_10)) ### Axiom % 12.22/12.47 167. (less_than T_4 T_3) (-. (less_than T_4 T_3)) ### Axiom % 12.22/12.47 168. (check_cpq (triple zenon_X11 T_0 T_6)) (-. (check_cpq (triple zenon_X11 T_0 T_6))) ### Axiom % 12.22/12.47 169. (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6))) (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6)) ### Axiom % 12.22/12.47 170. ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6))) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6))) (check_cpq (triple zenon_X11 T_0 T_6)) ### Equiv 168 169 % 12.22/12.47 171. ((less_than T_4 T_3) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6)))) (check_cpq (triple zenon_X11 T_0 T_6)) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6))) (less_than T_4 T_3) ### Imply 167 170 % 12.22/12.47 172. (All Y, ((less_than Y T_3) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6))))) (less_than T_4 T_3) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6))) (check_cpq (triple zenon_X11 T_0 T_6)) ### All 171 % 12.22/12.47 173. (All X, (All Y, ((less_than Y X) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6)))))) (check_cpq (triple zenon_X11 T_0 T_6)) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6))) (less_than T_4 T_3) ### All 172 % 12.22/12.47 174. ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_10 T_9)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6))) (less_than T_4 T_3) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6))) (All X, (All Y, ((less_than Y X) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6)))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) ### Equiv 90 173 % 12.22/12.47 175. ((less_than T_9 T_10) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_10 T_9)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All X, (All Y, ((less_than Y X) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6)))))) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6))) (less_than T_4 T_3) (less_than T_9 T_10) ### Imply 166 174 % 12.22/12.47 176. (All Y, ((less_than Y T_10) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_10 Y)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6))))) (less_than T_9 T_10) (less_than T_4 T_3) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6))) (All X, (All Y, ((less_than Y X) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6)))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) ### All 175 % 12.22/12.47 177. (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All X, (All Y, ((less_than Y X) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> (check_cpq (triple zenon_X11 T_0 T_6)))))) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6))) (less_than T_4 T_3) (less_than T_9 T_10) ### All 176 % 12.22/12.47 178. (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) W)) <=> (check_cpq (triple zenon_X11 T_0 W))))))) (less_than T_9 T_10) (less_than T_4 T_3) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) ### All 177 % 12.30/12.48 179. (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple zenon_X11 (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple zenon_X11 V W)))))))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6))) (less_than T_4 T_3) (less_than T_9 T_10) ### All 178 % 12.30/12.48 180. (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (less_than T_9 T_10) (less_than T_4 T_3) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) ### All 179 % 12.30/12.48 181. False ### False % 12.30/12.48 182. ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6)) <=> False) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (less_than T_4 T_3) (less_than T_9 T_10) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) ### Equiv 180 181 % 12.30/12.48 183. (-. (less_than T_3 T_4)) (less_than T_3 T_4) ### Axiom % 12.30/12.48 184. ((less_than T_4 T_3) \/ (less_than T_3 T_4)) (-. (less_than T_3 T_4)) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (less_than T_9 T_10) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6)) <=> False) ### Or 182 183 % 12.30/12.48 185. (All V, ((less_than T_4 V) \/ (less_than V T_4))) ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6)) <=> False) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (less_than T_9 T_10) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (-. (less_than T_3 T_4)) ### All 184 % 12.30/12.48 186. (-. (strictly_less_than T_3 T_4)) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6))) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (less_than T_9 T_10) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6)) <=> False) (All V, ((less_than T_4 V) \/ (less_than V T_4))) ### Extension/test/not_stricly_smaller_definition 185 180 % 12.30/12.48 187. ((strictly_less_than T_3 T_4) => ((check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) <=> False)) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All V, ((less_than T_4 V) \/ (less_than V T_4))) ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6)) <=> False) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (less_than T_9 T_10) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6))) ### Imply 186 56 % 12.30/12.48 188. (All Y, ((strictly_less_than T_3 Y) => ((check_cpq (triple T_5 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> False))) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6))) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (less_than T_9 T_10) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6)) <=> False) (All V, ((less_than T_4 V) \/ (less_than V T_4))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) ### All 187 % 12.30/12.48 189. (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple T_5 (insert_slb T_0 (pair X Y)) T_6)) <=> False)))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All V, ((less_than T_4 V) \/ (less_than V T_4))) ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6)) <=> False) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (less_than T_9 T_10) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6))) ### All 188 % 12.30/12.48 190. (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple T_5 (insert_slb T_0 (pair X Y)) W)) <=> False))))) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6))) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (less_than T_9 T_10) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6)) <=> False) (All V, ((less_than T_4 V) \/ (less_than V T_4))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) ### All 189 % 12.30/12.48 191. (All U, (All V, ((less_than U V) \/ (less_than V U)))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6)) <=> False) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (less_than T_9 T_10) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6))) (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple T_5 (insert_slb T_0 (pair X Y)) W)) <=> False))))) ### All 190 % 12.30/12.48 192. (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple T_5 (insert_slb V (pair X Y)) W)) <=> False)))))) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6))) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (less_than T_9 T_10) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6)) <=> False) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All U, (All V, ((less_than U V) \/ (less_than V U)))) ### All 191 % 12.30/12.48 193. (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) (All U, (All V, ((less_than U V) \/ (less_than V U)))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6)) <=> False) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (less_than T_9 T_10) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (-. (check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6))) ### All 192 % 12.32/12.50 194. False ### False % 12.32/12.50 195. (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (less_than T_9 T_10) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6)) <=> False) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All U, (All V, ((less_than U V) \/ (less_than V U)))) (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) ### Equiv 193 194 % 12.32/12.50 196. ((strictly_less_than T_3 T_4) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 T_4)) T_6)) <=> False)) (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All U, (All V, ((less_than U V) \/ (less_than V U)))) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (less_than T_9 T_10) (T_4 = T_10) (All Y, ((strictly_less_than T_3 Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> False))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (T_3 = T_9) (less_than (bottom) T_9) (-. (less_than T_10 T_9)) (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> False)))) (All V, ((less_than T_10 V) \/ (less_than V T_10))) ### Imply 165 195 % 12.32/12.50 197. (All V, ((less_than T_10 V) \/ (less_than V T_10))) (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> False)))) (-. (less_than T_10 T_9)) (less_than (bottom) T_9) (T_3 = T_9) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All Y, ((strictly_less_than T_3 Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair T_3 Y)) T_6)) <=> False))) (T_4 = T_10) (less_than T_9 T_10) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) (All U, (All V, ((less_than U V) \/ (less_than V U)))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) ### All 196 % 12.32/12.50 198. (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All U, (All V, ((less_than U V) \/ (less_than V U)))) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (less_than T_9 T_10) (T_4 = T_10) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (T_3 = T_9) (less_than (bottom) T_9) (-. (less_than T_10 T_9)) (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) T_6)) <=> False)))) (All V, ((less_than T_10 V) \/ (less_than V T_10))) ### All 197 % 12.32/12.50 199. (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple zenon_X11 (insert_slb T_0 (pair X Y)) W)) <=> False))))) (All V, ((less_than T_10 V) \/ (less_than V T_10))) (-. (less_than T_10 T_9)) (less_than (bottom) T_9) (T_3 = T_9) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (T_4 = T_10) (less_than T_9 T_10) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) (All U, (All V, ((less_than U V) \/ (less_than V U)))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) ### All 198 % 12.32/12.50 200. (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple zenon_X11 (insert_slb V (pair X Y)) W)) <=> False)))))) (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All U, (All V, ((less_than U V) \/ (less_than V U)))) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (less_than T_9 T_10) (T_4 = T_10) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (T_3 = T_9) (less_than (bottom) T_9) (-. (less_than T_10 T_9)) (All V, ((less_than T_10 V) \/ (less_than V T_10))) ### All 199 % 12.32/12.50 201. (-. (less_than T_10 T_9)) (less_than (bottom) T_9) (T_3 = T_9) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (T_4 = T_10) (less_than T_9 T_10) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) (All U, (All V, ((less_than U V) \/ (less_than V U)))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple zenon_X11 (insert_slb V (pair X Y)) W)) <=> False)))))) ### All 200 % 12.32/12.50 202. (All U, (less_than (bottom) U)) (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple zenon_X11 (insert_slb V (pair X Y)) W)) <=> False)))))) (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All U, (All V, ((less_than U V) \/ (less_than V U)))) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (less_than T_9 T_10) (T_4 = T_10) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (T_3 = T_9) (-. (less_than T_10 T_9)) ### All 201 % 12.32/12.50 203. (-. (less_than T_10 T_9)) (less_than T_10 T_9) ### Axiom % 12.32/12.51 204. ((less_than T_9 T_10) \/ (less_than T_10 T_9)) (-. (less_than T_10 T_9)) (T_3 = T_9) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (T_4 = T_10) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) (All U, (All V, ((less_than U V) \/ (less_than V U)))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple zenon_X11 (insert_slb V (pair X Y)) W)) <=> False)))))) (All U, (less_than (bottom) U)) ### Or 202 203 % 12.32/12.51 205. (All V, ((less_than T_9 V) \/ (less_than V T_9))) (All U, (less_than (bottom) U)) (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple zenon_X11 (insert_slb V (pair X Y)) W)) <=> False)))))) (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All U, (All V, ((less_than U V) \/ (less_than V U)))) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (T_4 = T_10) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (T_3 = T_9) (-. (less_than T_10 T_9)) ### All 204 % 12.32/12.51 206. (-. (less_than T_10 T_9)) (T_3 = T_9) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (T_4 = T_10) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) (All U, (All V, ((less_than U V) \/ (less_than V U)))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple zenon_X11 (insert_slb V (pair X Y)) W)) <=> False)))))) (All U, (less_than (bottom) U)) ### All 205 % 12.32/12.51 207. (All U, (less_than (bottom) U)) (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All U, (All V, ((less_than U V) \/ (less_than V U)))) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (T_4 = T_10) (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (T_3 = T_9) (-. (less_than T_10 T_9)) ### All 206 % 12.32/12.51 208. ((check_cpq (triple zenon_X7 T_0 zenon_X8)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))) (-. (less_than T_10 T_9)) (T_3 = T_9) (T_4 = T_10) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) (All U, (less_than (bottom) U)) (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (All U, (All V, ((less_than U V) \/ (less_than V U)))) ### Equiv 71 207 % 12.32/12.51 209. (All W, ((check_cpq (triple zenon_X7 T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X)))))) (All U, (All V, ((less_than U V) \/ (less_than V U)))) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) (All U, (less_than (bottom) U)) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) (T_4 = T_10) (T_3 = T_9) (-. (less_than T_10 T_9)) ### All 208 % 12.32/12.51 210. (-. (less_than T_10 T_9)) (T_3 = T_9) (T_4 = T_10) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) (All U, (less_than (bottom) U)) (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (All U, (All V, ((less_than U V) \/ (less_than V U)))) ### All 209 % 12.32/12.51 211. (pair_in_list (insert_slb T_0 (pair T_3 T_4)) T_9 T_10) (All U, (less_than (bottom) U)) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) (All U, (All V, ((less_than U V) \/ (less_than V U)))) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) (-. (less_than T_10 T_9)) ### Extension/test/ax23 79 210 % 12.32/12.51 212. (-. ((pair_in_list (insert_slb T_0 (pair T_3 T_4)) T_9 T_10) => (less_than T_10 T_9))) (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (All U, (All V, ((less_than U V) \/ (less_than V U)))) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) (All U, (less_than (bottom) U)) ### NotImply 211 % 12.32/12.51 213. (-. (All X5, ((pair_in_list (insert_slb T_0 (pair T_3 T_4)) T_9 X5) => (less_than X5 T_9)))) (All U, (less_than (bottom) U)) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) (All U, (All V, ((less_than U V) \/ (less_than V U)))) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) ### NotAllEx 212 % 12.34/12.51 214. (-. (All X4, (All X5, ((pair_in_list (insert_slb T_0 (pair T_3 T_4)) X4 X5) => (less_than X5 X4))))) (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (All U, (All V, ((less_than U V) \/ (less_than V U)))) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) (All U, (less_than (bottom) U)) ### NotAllEx 213 % 12.34/12.51 215. (-. ((check_cpq (triple T_5 (insert_slb T_0 (pair T_3 T_4)) T_6)) <=> (All X4, (All X5, ((pair_in_list (insert_slb T_0 (pair T_3 T_4)) X4 X5) => (less_than X5 X4)))))) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) (All U, (All V, ((less_than U V) \/ (less_than V U)))) (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (All U, (less_than (bottom) U)) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) ### NotEquiv 40 214 % 12.34/12.51 216. (-. (All X3, ((check_cpq (triple T_5 (insert_slb T_0 (pair T_3 X3)) T_6)) <=> (All X4, (All X5, ((pair_in_list (insert_slb T_0 (pair T_3 X3)) X4 X5) => (less_than X5 X4))))))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All U, (less_than (bottom) U)) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) (All U, (All V, ((less_than U V) \/ (less_than V U)))) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) ### NotAllEx 215 % 12.34/12.51 217. (-. (All X2, (All X3, ((check_cpq (triple T_5 (insert_slb T_0 (pair X2 X3)) T_6)) <=> (All X4, (All X5, ((pair_in_list (insert_slb T_0 (pair X2 X3)) X4 X5) => (less_than X5 X4)))))))) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) (All U, (All V, ((less_than U V) \/ (less_than V U)))) (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (All U, (less_than (bottom) U)) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) ### NotAllEx 216 % 12.34/12.51 218. (-. (All X1, (All X2, (All X3, ((check_cpq (triple T_5 (insert_slb T_0 (pair X2 X3)) X1)) <=> (All X4, (All X5, ((pair_in_list (insert_slb T_0 (pair X2 X3)) X4 X5) => (less_than X5 X4))))))))) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) (All U, (less_than (bottom) U)) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) (All U, (All V, ((less_than U V) \/ (less_than V U)))) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) ### NotAllEx 217 % 12.34/12.51 219. (-. (All Z, (All X1, (All X2, (All X3, ((check_cpq (triple Z (insert_slb T_0 (pair X2 X3)) X1)) <=> (All X4, (All X5, ((pair_in_list (insert_slb T_0 (pair X2 X3)) X4 X5) => (less_than X5 X4)))))))))) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) (All U, (All V, ((less_than U V) \/ (less_than V U)))) (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (All U, (less_than (bottom) U)) (All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) ### NotAllEx 218 % 12.34/12.51 220. (-. ((All V, (All W, ((check_cpq (triple V T_0 W)) <=> (All X, (All Y, ((pair_in_list T_0 X Y) => (less_than Y X))))))) => (All Z, (All X1, (All X2, (All X3, ((check_cpq (triple Z (insert_slb T_0 (pair X2 X3)) X1)) <=> (All X4, (All X5, ((pair_in_list (insert_slb T_0 (pair X2 X3)) X4 X5) => (less_than X5 X4))))))))))) (All U, (less_than (bottom) U)) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) (All U, (All V, ((less_than U V) \/ (less_than V U)))) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) ### NotImply 219 % 12.34/12.51 221. (-. (All U, ((All V, (All W, ((check_cpq (triple V U W)) <=> (All X, (All Y, ((pair_in_list U X Y) => (less_than Y X))))))) => (All Z, (All X1, (All X2, (All X3, ((check_cpq (triple Z (insert_slb U (pair X2 X3)) X1)) <=> (All X4, (All X5, ((pair_in_list (insert_slb U (pair X2 X3)) X4 X5) => (less_than X5 X4)))))))))))) (All U, (All V, (All W, (((less_than U V) /\ (less_than V W)) => (less_than U W))))) (All U, (All V, ((less_than U V) \/ (less_than V U)))) (All U, (All V, (All W, (All X, (All Y, ((strictly_less_than X Y) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> False))))))) (All U, (All V, (All W, (All X, (All Y, ((less_than Y X) => ((check_cpq (triple U (insert_slb V (pair X Y)) W)) <=> (check_cpq (triple U V W))))))))) (All U, (less_than (bottom) U)) ### NotAllEx 220 % 12.34/12.51 % SZS output end Proof % 12.34/12.51 (* END-PROOF *) %------------------------------------------------------------------------------