%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SEU284+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 : n016.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 : Tue Jul 19 14:49:55 EDT 2022 % Result : Theorem 0.22s 0.44s % Output : Proof 0.22s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.14 % Problem : SEU284+1 : TPTP v8.1.0. Released v3.3.0. % 0.08/0.15 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.15/0.37 % Computer : n016.cluster.edu % 0.15/0.37 % Model : x86_64 x86_64 % 0.15/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.15/0.37 % Memory : 8042.1875MB % 0.15/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.15/0.37 % CPULimit : 300 % 0.15/0.37 % WCLimit : 600 % 0.15/0.37 % DateTime : Mon Jun 20 02:54:24 EDT 2022 % 0.15/0.37 % CPUTime : % 0.22/0.44 % SZS status Theorem % 0.22/0.44 (* PROOF-FOUND *) % 0.22/0.44 (* BEGIN-PROOF *) % 0.22/0.44 % SZS output start Proof % 0.22/0.44 1. (T_0 != T_0) ### Refl(=) % 0.22/0.44 2. (T_0 != T_0) ### Refl(=) % 0.22/0.44 3. (T_1 = (singleton T_2)) ((singleton T_2) != T_1) ### Sym(=) % 0.22/0.44 4. (T_1 != T_0) (T_0 = (singleton T_2)) (T_1 = (singleton T_2)) ### TransEq-sym 1 2 3 % 0.22/0.44 5. (-. (((in T_2 T_3) /\ ((T_1 = (singleton T_2)) /\ (T_0 = (singleton T_2)))) => (T_1 = T_0))) ### ConjTree 4 % 0.22/0.44 6. (-. (All D, (((in T_2 T_3) /\ ((T_1 = (singleton T_2)) /\ (D = (singleton T_2)))) => (T_1 = D)))) ### NotAllEx 5 % 0.22/0.44 7. (-. (All C, (All D, (((in T_2 T_3) /\ ((C = (singleton T_2)) /\ (D = (singleton T_2)))) => (C = D))))) ### NotAllEx 6 % 0.22/0.44 8. (-. (All B, (All C, (All D, (((in B T_3) /\ ((C = (singleton B)) /\ (D = (singleton B)))) => (C = D)))))) ### NotAllEx 7 % 0.22/0.44 9. ((singleton T_4) != (singleton T_4)) ### Refl(=) % 0.22/0.44 10. (All C, (C != (singleton T_4))) ### All 9 % 0.22/0.44 11. ((in T_4 T_3) /\ (All C, (C != (singleton T_4)))) ### And 10 % 0.22/0.44 12. (-. (-. ((in T_4 T_3) /\ (All C, (C != (singleton T_4)))))) ### NotNot 11 % 0.22/0.44 13. (-. (All B, (-. ((in B T_3) /\ (All C, (C != (singleton B))))))) ### NotAllEx 12 % 0.22/0.44 14. (-. (Ex B, ((relation B) /\ ((function B) /\ (((relation_dom B) = T_3) /\ (All C, ((in C T_3) => ((apply B C) = (singleton C))))))))) (Ex B, ((relation B) /\ ((function B) /\ (((relation_dom B) = T_3) /\ (All C, ((in C T_3) => ((apply B C) = (singleton C)))))))) ### Axiom % 0.22/0.44 15. (((All B, (All C, (All D, (((in B T_3) /\ ((C = (singleton B)) /\ (D = (singleton B)))) => (C = D))))) /\ (All B, (-. ((in B T_3) /\ (All C, (C != (singleton B))))))) => (Ex B, ((relation B) /\ ((function B) /\ (((relation_dom B) = T_3) /\ (All C, ((in C T_3) => ((apply B C) = (singleton C))))))))) (-. (Ex B, ((relation B) /\ ((function B) /\ (((relation_dom B) = T_3) /\ (All C, ((in C T_3) => ((apply B C) = (singleton C))))))))) ### DisjTree 8 13 14 % 0.22/0.44 16. (All A, (((All B, (All C, (All D, (((in B A) /\ ((C = (singleton B)) /\ (D = (singleton B)))) => (C = D))))) /\ (All B, (-. ((in B A) /\ (All C, (C != (singleton B))))))) => (Ex B, ((relation B) /\ ((function B) /\ (((relation_dom B) = A) /\ (All C, ((in C A) => ((apply B C) = (singleton C)))))))))) (-. (Ex B, ((relation B) /\ ((function B) /\ (((relation_dom B) = T_3) /\ (All C, ((in C T_3) => ((apply B C) = (singleton C))))))))) ### All 15 % 0.22/0.44 17. (-. (All A, (Ex B, ((relation B) /\ ((function B) /\ (((relation_dom B) = A) /\ (All C, ((in C A) => ((apply B C) = (singleton C)))))))))) (All A, (((All B, (All C, (All D, (((in B A) /\ ((C = (singleton B)) /\ (D = (singleton B)))) => (C = D))))) /\ (All B, (-. ((in B A) /\ (All C, (C != (singleton B))))))) => (Ex B, ((relation B) /\ ((function B) /\ (((relation_dom B) = A) /\ (All C, ((in C A) => ((apply B C) = (singleton C)))))))))) ### NotAllEx 16 % 0.22/0.44 % SZS output end Proof % 0.22/0.44 (* END-PROOF *) %------------------------------------------------------------------------------