%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : SWW469+5 : TPTP v8.1.0. Released v5.3.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n017.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 : Thu Jul 21 01:31:46 EDT 2022 % Result : Theorem 2.00s 2.20s % Output : Proof 2.00s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.11 % Problem : SWW469+5 : TPTP v8.1.0. Released v5.3.0. % 0.08/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.33 % Computer : n017.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 : Sat Jun 4 20:26:45 EDT 2022 % 0.12/0.33 % CPUTime : % 2.00/2.20 % SZS status Theorem % 2.00/2.20 (* PROOF-FOUND *) % 2.00/2.20 (* BEGIN-PROOF *) % 2.00/2.20 % SZS output start Proof % 2.00/2.20 1. ((ti (state) zenon_X0) != (ti (state) zenon_X0)) ### Refl(=) % 2.00/2.20 2. ((ti (state) T_1) = (ti (state) T_2)) ((ti (state) T_2) != (ti (state) T_1)) ### Sym(=) % 2.00/2.20 3. ((ti (state) T_1) != (ti (state) zenon_X0)) ((ti (state) zenon_X0) = (ti (state) T_2)) ((ti (state) T_1) = (ti (state) T_2)) ### Trans-sym 1 2 % 2.00/2.20 4. (All S, ((ti (state) S) = (ti (state) T_2))) ((ti (state) zenon_X0) = (ti (state) T_2)) ((ti (state) T_1) != (ti (state) zenon_X0)) ### All 3 % 2.00/2.20 5. ((ti (state) T_2) != (ti (state) T_3)) ((ti (state) T_3) = (ti (state) T_2)) ### Sym(=) % 2.00/2.20 6. (All S, ((ti (state) S) = (ti (state) T_2))) ((ti (state) T_2) != (ti (state) T_3)) ### All 5 % 2.00/2.20 7. ((ti (state) T_1) != (ti (state) T_3)) ((ti (state) zenon_X0) = (ti (state) T_2)) (All S, ((ti (state) S) = (ti (state) T_2))) ### TransEq 4 6 6 % 2.00/2.20 8. (All S, ((ti (state) S) = (ti (state) T_2))) ((ti (state) T_1) != (ti (state) T_3)) ### All 7 % 2.00/2.20 9. (-. (-. (All S, ((ti (state) S) = (ti (state) T_2))))) ((ti (state) T_1) != (ti (state) T_3)) ### NotNot 8 % 2.00/2.20 10. (-. (All T, (-. (All S, ((ti (state) S) = (ti (state) T)))))) ((ti (state) T_1) != (ti (state) T_3)) ### NotAllEx 9 % 2.00/2.20 11. (hBOOL (hoare_1883395792gleton)) (-. (All T, (-. (All S, ((ti (state) S) = (ti (state) T)))))) ### Extension/test/fact_0_state__not__singleton__def 10 % 2.00/2.20 % SZS output end Proof % 2.00/2.20 (* END-PROOF *) %------------------------------------------------------------------------------