%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : KRS203+1 : TPTP v8.1.0. Bugfixed v5.4.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n025.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 : Sun Jul 17 03:32:11 EDT 2022 % Result : Theorem 86.48s 86.70s % Output : Proof 86.82s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : KRS203+1 : TPTP v8.1.0. Bugfixed v5.4.0. % 0.06/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n025.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 : Tue Jun 7 11:49:49 EDT 2022 % 0.12/0.33 % CPUTime : % 86.48/86.70 % SZS status Theorem % 86.48/86.70 (* PROOF-FOUND *) % 86.48/86.70 (* BEGIN-PROOF *) % 86.48/86.70 % SZS output start Proof % 86.48/86.70 1. (-. (model T_0 T_1)) (model T_0 T_1) ### Axiom % 86.48/86.70 2. (All I, (model I T_1)) (-. (model T_0 T_1)) ### All 1 % 86.48/86.70 3. (model T_0 T_2) (-. (model T_0 T_2)) ### Axiom % 86.48/86.70 4. (-. ((model T_0 T_1) /\ (model T_0 T_2))) (model T_0 T_2) (All I, (model I T_1)) ### NotAnd 2 3 % 86.48/86.70 5. (-. (Ex I1, ((model I1 T_1) /\ (model I1 T_2)))) (All I, (model I T_1)) (model T_0 T_2) ### NotExists 4 % 86.48/86.70 6. (-. (status T_1 T_2 (sat))) (status T_1 T_2 (sat)) ### Axiom % 86.48/86.70 7. ((Ex I1, ((model I1 T_1) /\ (model I1 T_2))) <=> (status T_1 T_2 (sat))) (-. (status T_1 T_2 (sat))) (model T_0 T_2) (All I, (model I T_1)) ### Equiv 5 6 % 86.48/86.70 8. (All C, ((Ex I1, ((model I1 T_1) /\ (model I1 C))) <=> (status T_1 C (sat)))) (All I, (model I T_1)) (model T_0 T_2) (-. (status T_1 T_2 (sat))) ### All 7 % 86.48/86.70 9. (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (-. (status T_1 T_2 (sat))) (model T_0 T_2) (All I, (model I T_1)) ### All 8 % 86.48/86.70 10. (-. (status T_1 T_2 (thm))) (status T_1 T_2 (thm)) ### Axiom % 86.48/86.70 11. (-. (-. (status T_1 T_2 (thm)))) (-. (status T_1 T_2 (thm))) ### NotNot 10 % 86.48/86.70 12. (-. ((status T_1 T_2 (sat)) /\ (-. (status T_1 T_2 (thm))))) (-. (status T_1 T_2 (thm))) (All I, (model I T_1)) (model T_0 T_2) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) ### NotAnd 9 11 % 86.48/86.70 13. (-. (Ex C, ((status T_1 C (sat)) /\ (-. (status T_1 C (thm)))))) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (model T_0 T_2) (All I, (model I T_1)) (-. (status T_1 T_2 (thm))) ### NotExists 12 % 86.48/86.70 14. (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) (-. (status T_1 T_2 (thm))) (All I, (model I T_1)) (model T_0 T_2) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) ### NotExists 13 % 86.48/86.70 15. (-. (model T_3 (not T_4))) (model T_3 (not T_4)) ### Axiom % 86.48/86.70 16. (-. (-. (model T_3 (not T_4)))) (-. (model T_3 (not T_4))) ### NotNot 15 % 86.48/86.70 17. (-. (model T_3 T_1)) (model T_3 T_1) ### Axiom % 86.48/86.70 18. (All I, (model I T_1)) (-. (model T_3 T_1)) ### All 17 % 86.48/86.70 19. (-. (model T_3 T_2)) (model T_3 T_2) ### Axiom % 86.48/86.70 20. ((model T_3 T_1) => (model T_3 T_2)) (-. (model T_3 T_2)) (All I, (model I T_1)) ### Imply 18 19 % 86.48/86.70 21. (All I1, ((model I1 T_1) => (model I1 T_2))) (All I, (model I T_1)) (-. (model T_3 T_2)) ### All 20 % 86.48/86.70 22. (model T_3 T_4) (-. (model T_3 T_4)) ### Axiom % 86.48/86.70 23. (-. ((model T_3 T_2) /\ (model T_3 T_4))) (model T_3 T_4) (All I, (model I T_1)) (All I1, ((model I1 T_1) => (model I1 T_2))) ### NotAnd 21 22 % 86.48/86.70 24. (-. (Ex I1, ((model I1 T_2) /\ (model I1 T_4)))) (All I1, ((model I1 T_1) => (model I1 T_2))) (All I, (model I T_1)) (model T_3 T_4) ### NotExists 23 % 86.48/86.70 25. ((model T_3 T_4) <=> (-. (model T_3 (not T_4)))) (All I, (model I T_1)) (All I1, ((model I1 T_1) => (model I1 T_2))) (-. (Ex I1, ((model I1 T_2) /\ (model I1 T_4)))) (-. (model T_3 (not T_4))) ### Equiv 16 24 % 86.48/86.70 26. (All F, ((model T_3 F) <=> (-. (model T_3 (not F))))) (-. (model T_3 (not T_4))) (-. (Ex I1, ((model I1 T_2) /\ (model I1 T_4)))) (All I1, ((model I1 T_1) => (model I1 T_2))) (All I, (model I T_1)) ### All 25 % 86.48/86.70 27. (All I, (All F, ((model I F) <=> (-. (model I (not F)))))) (All I, (model I T_1)) (All I1, ((model I1 T_1) => (model I1 T_2))) (-. (Ex I1, ((model I1 T_2) /\ (model I1 T_4)))) (-. (model T_3 (not T_4))) ### All 26 % 86.48/86.70 28. ((All I1, ((model I1 T_1) => (model I1 T_2))) <=> (status T_1 T_2 (thm))) (-. (model T_3 (not T_4))) (-. (Ex I1, ((model I1 T_2) /\ (model I1 T_4)))) (All I, (All F, ((model I F) <=> (-. (model I (not F)))))) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (model T_0 T_2) (All I, (model I T_1)) (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) ### Equiv 14 27 % 86.48/86.70 29. (All C, ((All I1, ((model I1 T_1) => (model I1 C))) <=> (status T_1 C (thm)))) (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) (All I, (model I T_1)) (model T_0 T_2) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (All I, (All F, ((model I F) <=> (-. (model I (not F)))))) (-. (Ex I1, ((model I1 T_2) /\ (model I1 T_4)))) (-. (model T_3 (not T_4))) ### All 28 % 86.48/86.70 30. (model T_5 T_4) (-. (model T_5 T_4)) ### Axiom % 86.48/86.70 31. (All I, (-. (model I T_4))) (model T_5 T_4) ### All 30 % 86.48/86.70 32. ((model T_5 T_2) /\ (model T_5 T_4)) (All I, (-. (model I T_4))) ### And 31 % 86.48/86.70 33. (Ex I1, ((model I1 T_2) /\ (model I1 T_4))) (All I, (-. (model I T_4))) ### Exists 32 % 86.48/86.70 34. ((Ex I1, ((model I1 T_2) /\ (model I1 T_4))) <=> (status T_2 T_4 (sat))) (All I, (-. (model I T_4))) (-. (model T_3 (not T_4))) (All I, (All F, ((model I F) <=> (-. (model I (not F)))))) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (model T_0 T_2) (All I, (model I T_1)) (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) (All C, ((All I1, ((model I1 T_1) => (model I1 C))) <=> (status T_1 C (thm)))) ### Equiv 29 33 % 86.48/86.70 35. (All C, ((Ex I1, ((model I1 T_2) /\ (model I1 C))) <=> (status T_2 C (sat)))) (All C, ((All I1, ((model I1 T_1) => (model I1 C))) <=> (status T_1 C (thm)))) (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) (All I, (model I T_1)) (model T_0 T_2) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (All I, (All F, ((model I F) <=> (-. (model I (not F)))))) (-. (model T_3 (not T_4))) (All I, (-. (model I T_4))) ### All 34 % 86.48/86.70 36. (All I, (-. (model I T_4))) (-. (model T_3 (not T_4))) (All I, (All F, ((model I F) <=> (-. (model I (not F)))))) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (model T_0 T_2) (All I, (model I T_1)) (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) (All C, ((All I1, ((model I1 T_1) => (model I1 C))) <=> (status T_1 C (thm)))) ### All 35 % 86.48/86.70 37. (-. (All I1, (model I1 (not T_4)))) (All C, ((All I1, ((model I1 T_1) => (model I1 C))) <=> (status T_1 C (thm)))) (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) (All I, (model I T_1)) (model T_0 T_2) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (All I, (All F, ((model I F) <=> (-. (model I (not F)))))) (All I, (-. (model I T_4))) ### NotAllEx 36 % 86.48/86.70 38. (-. ((All I1, (model I1 (not T_4))) /\ (All I1, (model I1 (not T_4))))) (All I, (-. (model I T_4))) (All I, (All F, ((model I F) <=> (-. (model I (not F)))))) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (model T_0 T_2) (All I, (model I T_1)) (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) (All C, ((All I1, ((model I1 T_1) => (model I1 C))) <=> (status T_1 C (thm)))) ### NotAnd 37 37 % 86.48/86.70 39. (-. (model T_6 T_1)) (model T_6 T_1) ### Axiom % 86.48/86.70 40. (All I, (model I T_1)) (-. (model T_6 T_1)) ### All 39 % 86.48/86.70 41. (model T_6 T_7) (-. (model T_6 T_7)) ### Axiom % 86.48/86.70 42. (-. ((model T_6 T_1) /\ (model T_6 T_7))) (model T_6 T_7) (All I, (model I T_1)) ### NotAnd 40 41 % 86.48/86.70 43. (-. (Ex I1, ((model I1 T_1) /\ (model I1 T_7)))) (All I, (model I T_1)) (model T_6 T_7) ### NotExists 42 % 86.48/86.70 44. (-. (status T_1 T_7 (sat))) (status T_1 T_7 (sat)) ### Axiom % 86.48/86.70 45. ((Ex I1, ((model I1 T_1) /\ (model I1 T_7))) <=> (status T_1 T_7 (sat))) (-. (status T_1 T_7 (sat))) (model T_6 T_7) (All I, (model I T_1)) ### Equiv 43 44 % 86.48/86.70 46. (All C, ((Ex I1, ((model I1 T_1) /\ (model I1 C))) <=> (status T_1 C (sat)))) (All I, (model I T_1)) (model T_6 T_7) (-. (status T_1 T_7 (sat))) ### All 45 % 86.48/86.70 47. (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (-. (status T_1 T_7 (sat))) (model T_6 T_7) (All I, (model I T_1)) ### All 46 % 86.48/86.70 48. (-. (status T_1 T_7 (thm))) (status T_1 T_7 (thm)) ### Axiom % 86.48/86.70 49. (-. (-. (status T_1 T_7 (thm)))) (-. (status T_1 T_7 (thm))) ### NotNot 48 % 86.48/86.70 50. (-. ((status T_1 T_7 (sat)) /\ (-. (status T_1 T_7 (thm))))) (-. (status T_1 T_7 (thm))) (All I, (model I T_1)) (model T_6 T_7) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) ### NotAnd 47 49 % 86.48/86.70 51. (-. (Ex C, ((status T_1 C (sat)) /\ (-. (status T_1 C (thm)))))) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (model T_6 T_7) (All I, (model I T_1)) (-. (status T_1 T_7 (thm))) ### NotExists 50 % 86.82/87.02 52. (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) (-. (status T_1 T_7 (thm))) (All I, (model I T_1)) (model T_6 T_7) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) ### NotExists 51 % 86.82/87.02 53. (-. (model T_8 T_1)) (model T_8 T_1) ### Axiom % 86.82/87.02 54. (All I, (model I T_1)) (-. (model T_8 T_1)) ### All 53 % 86.82/87.02 55. (-. (model T_8 T_7)) (model T_8 T_7) ### Axiom % 86.82/87.02 56. ((model T_8 T_1) => (model T_8 T_7)) (-. (model T_8 T_7)) (All I, (model I T_1)) ### Imply 54 55 % 86.82/87.02 57. (All I1, ((model I1 T_1) => (model I1 T_7))) (All I, (model I T_1)) (-. (model T_8 T_7)) ### All 56 % 86.82/87.02 58. ((All I1, ((model I1 T_1) => (model I1 T_7))) <=> (status T_1 T_7 (thm))) (-. (model T_8 T_7)) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (model T_6 T_7) (All I, (model I T_1)) (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) ### Equiv 52 57 % 86.82/87.02 59. (All C, ((All I1, ((model I1 T_1) => (model I1 C))) <=> (status T_1 C (thm)))) (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) (All I, (model I T_1)) (model T_6 T_7) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (-. (model T_8 T_7)) ### All 58 % 86.82/87.02 60. (-. (model T_8 (not T_4))) (model T_8 (not T_4)) ### Axiom % 86.82/87.02 61. (All I1, (model I1 (not T_4))) (-. (model T_8 (not T_4))) ### All 60 % 86.82/87.02 62. (-. ((model T_8 T_7) /\ (model T_8 (not T_4)))) (All I1, (model I1 (not T_4))) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (model T_6 T_7) (All I, (model I T_1)) (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) (All C, ((All I1, ((model I1 T_1) => (model I1 C))) <=> (status T_1 C (thm)))) ### NotAnd 59 61 % 86.82/87.02 63. (-. (All I1, ((model I1 T_7) /\ (model I1 (not T_4))))) (All C, ((All I1, ((model I1 T_1) => (model I1 C))) <=> (status T_1 C (thm)))) (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) (All I, (model I T_1)) (model T_6 T_7) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (All I1, (model I1 (not T_4))) ### NotAllEx 62 % 86.82/87.02 64. (-. (model T_9 T_7)) (model T_9 T_7) ### Axiom % 86.82/87.02 65. ((model T_9 T_7) /\ (model T_9 (not T_4))) (-. (model T_9 T_7)) ### And 64 % 86.82/87.02 66. (All I1, ((model I1 T_7) /\ (model I1 (not T_4)))) (-. (model T_9 T_7)) ### All 65 % 86.82/87.02 67. ((All I1, ((model I1 T_7) /\ (model I1 (not T_4)))) <=> (status T_7 (not T_4) (tau))) (-. (model T_9 T_7)) (All I1, (model I1 (not T_4))) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (model T_6 T_7) (All I, (model I T_1)) (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) (All C, ((All I1, ((model I1 T_1) => (model I1 C))) <=> (status T_1 C (thm)))) ### Equiv 63 66 % 86.82/87.02 68. (All C, ((All I1, ((model I1 T_7) /\ (model I1 C))) <=> (status T_7 C (tau)))) (All C, ((All I1, ((model I1 T_1) => (model I1 C))) <=> (status T_1 C (thm)))) (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) (All I, (model I T_1)) (model T_6 T_7) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (All I1, (model I1 (not T_4))) (-. (model T_9 T_7)) ### All 67 % 86.82/87.02 69. ((All I1, (model I1 (not T_4))) /\ (All I1, (model I1 (not T_4)))) (-. (model T_9 T_7)) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (model T_6 T_7) (All I, (model I T_1)) (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) (All C, ((All I1, ((model I1 T_1) => (model I1 C))) <=> (status T_1 C (thm)))) (All C, ((All I1, ((model I1 T_7) /\ (model I1 C))) <=> (status T_7 C (tau)))) ### And 68 % 86.82/87.02 70. (((All I1, (model I1 (not T_4))) /\ (All I1, (model I1 (not T_4)))) <=> (status (not T_4) T_4 (uns))) (All C, ((All I1, ((model I1 T_7) /\ (model I1 C))) <=> (status T_7 C (tau)))) (model T_6 T_7) (-. (model T_9 T_7)) (All C, ((All I1, ((model I1 T_1) => (model I1 C))) <=> (status T_1 C (thm)))) (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) (All I, (model I T_1)) (model T_0 T_2) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (All I, (All F, ((model I F) <=> (-. (model I (not F)))))) (All I, (-. (model I T_4))) ### Equiv 38 69 % 86.82/87.02 71. (All C, (((All I1, (model I1 (not T_4))) /\ (All I2, (model I2 (not C)))) <=> (status (not T_4) C (uns)))) (All I, (-. (model I T_4))) (All I, (All F, ((model I F) <=> (-. (model I (not F)))))) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (model T_0 T_2) (All I, (model I T_1)) (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) (All C, ((All I1, ((model I1 T_1) => (model I1 C))) <=> (status T_1 C (thm)))) (-. (model T_9 T_7)) (model T_6 T_7) (All C, ((All I1, ((model I1 T_7) /\ (model I1 C))) <=> (status T_7 C (tau)))) ### All 70 % 86.82/87.02 72. (All Ax, (All C, (((All I1, (model I1 Ax)) /\ (All I2, (model I2 (not C)))) <=> (status Ax C (uns))))) (All C, ((All I1, ((model I1 T_7) /\ (model I1 C))) <=> (status T_7 C (tau)))) (model T_6 T_7) (-. (model T_9 T_7)) (All C, ((All I1, ((model I1 T_1) => (model I1 C))) <=> (status T_1 C (thm)))) (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) (All I, (model I T_1)) (model T_0 T_2) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (All I, (All F, ((model I F) <=> (-. (model I (not F)))))) (All I, (-. (model I T_4))) ### All 71 % 86.82/87.02 73. (All Ax, (All C, ((All I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (tau))))) (All I, (-. (model I T_4))) (All I, (All F, ((model I F) <=> (-. (model I (not F)))))) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (model T_0 T_2) (All I, (model I T_1)) (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) (All C, ((All I1, ((model I1 T_1) => (model I1 C))) <=> (status T_1 C (thm)))) (-. (model T_9 T_7)) (model T_6 T_7) (All Ax, (All C, (((All I1, (model I1 Ax)) /\ (All I2, (model I2 (not C)))) <=> (status Ax C (uns))))) ### All 72 % 86.82/87.02 74. (All Ax, (All C, ((All I1, ((model I1 Ax) => (model I1 C))) <=> (status Ax C (thm))))) (All Ax, (All C, (((All I1, (model I1 Ax)) /\ (All I2, (model I2 (not C)))) <=> (status Ax C (uns))))) (model T_6 T_7) (-. (model T_9 T_7)) (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) (All I, (model I T_1)) (model T_0 T_2) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (All I, (All F, ((model I F) <=> (-. (model I (not F)))))) (All I, (-. (model I T_4))) (All Ax, (All C, ((All I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (tau))))) ### All 73 % 86.82/87.02 75. (Ex F, (All I, (model I F))) (All Ax, (All C, ((All I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (tau))))) (All I, (-. (model I T_4))) (All I, (All F, ((model I F) <=> (-. (model I (not F)))))) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (model T_0 T_2) (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) (-. (model T_9 T_7)) (model T_6 T_7) (All Ax, (All C, (((All I1, (model I1 Ax)) /\ (All I2, (model I2 (not C)))) <=> (status Ax C (uns))))) (All Ax, (All C, ((All I1, ((model I1 Ax) => (model I1 C))) <=> (status Ax C (thm))))) ### Exists 74 % 86.82/87.02 76. (Ex I2, (-. (model I2 T_7))) (All Ax, (All C, ((All I1, ((model I1 Ax) => (model I1 C))) <=> (status Ax C (thm))))) (All Ax, (All C, (((All I1, (model I1 Ax)) /\ (All I2, (model I2 (not C)))) <=> (status Ax C (uns))))) (model T_6 T_7) (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) (model T_0 T_2) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (All I, (All F, ((model I F) <=> (-. (model I (not F)))))) (All I, (-. (model I T_4))) (All Ax, (All C, ((All I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (tau))))) (Ex F, (All I, (model I F))) ### Exists 75 % 86.82/87.02 77. (Ex I1, (model I1 T_7)) (Ex F, (All I, (model I F))) (All Ax, (All C, ((All I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (tau))))) (All I, (-. (model I T_4))) (All I, (All F, ((model I F) <=> (-. (model I (not F)))))) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (model T_0 T_2) (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) (All Ax, (All C, (((All I1, (model I1 Ax)) /\ (All I2, (model I2 (not C)))) <=> (status Ax C (uns))))) (All Ax, (All C, ((All I1, ((model I1 Ax) => (model I1 C))) <=> (status Ax C (thm))))) (Ex I2, (-. (model I2 T_7))) ### Exists 76 % 86.82/87.03 78. ((Ex I1, (model I1 T_7)) /\ (Ex I2, (-. (model I2 T_7)))) (All Ax, (All C, ((All I1, ((model I1 Ax) => (model I1 C))) <=> (status Ax C (thm))))) (All Ax, (All C, (((All I1, (model I1 Ax)) /\ (All I2, (model I2 (not C)))) <=> (status Ax C (uns))))) (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) (model T_0 T_2) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (All I, (All F, ((model I F) <=> (-. (model I (not F)))))) (All I, (-. (model I T_4))) (All Ax, (All C, ((All I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (tau))))) (Ex F, (All I, (model I F))) ### And 77 % 86.82/87.03 79. (Ex F, ((Ex I1, (model I1 F)) /\ (Ex I2, (-. (model I2 F))))) (Ex F, (All I, (model I F))) (All Ax, (All C, ((All I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (tau))))) (All I, (-. (model I T_4))) (All I, (All F, ((model I F) <=> (-. (model I (not F)))))) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (model T_0 T_2) (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) (All Ax, (All C, (((All I1, (model I1 Ax)) /\ (All I2, (model I2 (not C)))) <=> (status Ax C (uns))))) (All Ax, (All C, ((All I1, ((model I1 Ax) => (model I1 C))) <=> (status Ax C (thm))))) ### Exists 78 % 86.82/87.03 80. (Ex F, (All I, (-. (model I F)))) (All Ax, (All C, ((All I1, ((model I1 Ax) => (model I1 C))) <=> (status Ax C (thm))))) (All Ax, (All C, (((All I1, (model I1 Ax)) /\ (All I2, (model I2 (not C)))) <=> (status Ax C (uns))))) (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) (model T_0 T_2) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (All I, (All F, ((model I F) <=> (-. (model I (not F)))))) (All Ax, (All C, ((All I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (tau))))) (Ex F, (All I, (model I F))) (Ex F, ((Ex I1, (model I1 F)) /\ (Ex I2, (-. (model I2 F))))) ### Exists 79 % 86.82/87.03 81. (Ex I1, (model I1 T_2)) (Ex F, ((Ex I1, (model I1 F)) /\ (Ex I2, (-. (model I2 F))))) (Ex F, (All I, (model I F))) (All Ax, (All C, ((All I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (tau))))) (All I, (All F, ((model I F) <=> (-. (model I (not F)))))) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) (All Ax, (All C, (((All I1, (model I1 Ax)) /\ (All I2, (model I2 (not C)))) <=> (status Ax C (uns))))) (All Ax, (All C, ((All I1, ((model I1 Ax) => (model I1 C))) <=> (status Ax C (thm))))) (Ex F, (All I, (-. (model I F)))) ### Exists 80 % 86.82/87.03 82. ((Ex I1, (model I1 T_2)) /\ ((All I1, ((model I1 T_2) => (model I1 T_10))) /\ ((Ex I3, ((-. (model I3 T_2)) /\ (model I3 T_10))) /\ (Ex I4, (-. (model I4 T_10)))))) (Ex F, (All I, (-. (model I F)))) (All Ax, (All C, ((All I1, ((model I1 Ax) => (model I1 C))) <=> (status Ax C (thm))))) (All Ax, (All C, (((All I1, (model I1 Ax)) /\ (All I2, (model I2 (not C)))) <=> (status Ax C (uns))))) (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (All I, (All F, ((model I F) <=> (-. (model I (not F)))))) (All Ax, (All C, ((All I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (tau))))) (Ex F, (All I, (model I F))) (Ex F, ((Ex I1, (model I1 F)) /\ (Ex I2, (-. (model I2 F))))) ### ConjTree 81 % 86.82/87.03 83. (Ex C, ((Ex I1, (model I1 T_2)) /\ ((All I1, ((model I1 T_2) => (model I1 C))) /\ ((Ex I3, ((-. (model I3 T_2)) /\ (model I3 C))) /\ (Ex I4, (-. (model I4 C))))))) (Ex F, ((Ex I1, (model I1 F)) /\ (Ex I2, (-. (model I2 F))))) (Ex F, (All I, (model I F))) (All Ax, (All C, ((All I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (tau))))) (All I, (All F, ((model I F) <=> (-. (model I (not F)))))) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) (All Ax, (All C, (((All I1, (model I1 Ax)) /\ (All I2, (model I2 (not C)))) <=> (status Ax C (uns))))) (All Ax, (All C, ((All I1, ((model I1 Ax) => (model I1 C))) <=> (status Ax C (thm))))) (Ex F, (All I, (-. (model I F)))) ### Exists 82 % 86.82/87.03 84. (Ex Ax, (Ex C, ((Ex I1, (model I1 Ax)) /\ ((All I1, ((model I1 Ax) => (model I1 C))) /\ ((Ex I3, ((-. (model I3 Ax)) /\ (model I3 C))) /\ (Ex I4, (-. (model I4 C)))))))) (Ex F, (All I, (-. (model I F)))) (All Ax, (All C, ((All I1, ((model I1 Ax) => (model I1 C))) <=> (status Ax C (thm))))) (All Ax, (All C, (((All I1, (model I1 Ax)) /\ (All I2, (model I2 (not C)))) <=> (status Ax C (uns))))) (-. (Ex Ax, (Ex C, ((status Ax C (sat)) /\ (-. (status Ax C (thm))))))) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (All I, (All F, ((model I F) <=> (-. (model I (not F)))))) (All Ax, (All C, ((All I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (tau))))) (Ex F, (All I, (model I F))) (Ex F, ((Ex I1, (model I1 F)) /\ (Ex I2, (-. (model I2 F))))) ### Exists 83 % 86.82/87.03 85. (-. (nota (sat) (thm))) (Ex F, ((Ex I1, (model I1 F)) /\ (Ex I2, (-. (model I2 F))))) (Ex F, (All I, (model I F))) (All Ax, (All C, ((All I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (tau))))) (All I, (All F, ((model I F) <=> (-. (model I (not F)))))) (All Ax, (All C, ((Ex I1, ((model I1 Ax) /\ (model I1 C))) <=> (status Ax C (sat))))) (All Ax, (All C, (((All I1, (model I1 Ax)) /\ (All I2, (model I2 (not C)))) <=> (status Ax C (uns))))) (All Ax, (All C, ((All I1, ((model I1 Ax) => (model I1 C))) <=> (status Ax C (thm))))) (Ex F, (All I, (-. (model I F)))) (Ex Ax, (Ex C, ((Ex I1, (model I1 Ax)) /\ ((All I1, ((model I1 Ax) => (model I1 C))) /\ ((Ex I3, ((-. (model I3 Ax)) /\ (model I3 C))) /\ (Ex I4, (-. (model I4 C)))))))) ### Definition-Pseudo(nota) 84 % 86.82/87.03 % SZS output end Proof % 86.82/87.03 (* END-PROOF *) %------------------------------------------------------------------------------