%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : RNG061+2 : TPTP v8.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % Computer : n019.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 : Mon Jul 18 20:41:54 EDT 2022 % Result : Theorem 2.92s 3.14s % Output : Proof 2.92s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : RNG061+2 : TPTP v8.1.0. Released v4.0.0. % 0.07/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.13/0.35 % Computer : n019.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 600 % 0.13/0.35 % DateTime : Mon May 30 16:38:25 EDT 2022 % 0.13/0.35 % CPUTime : % 2.92/3.14 % SZS status Theorem % 2.92/3.14 (* PROOF-FOUND *) % 2.92/3.14 (* BEGIN-PROOF *) % 2.92/3.14 % SZS output start Proof % 2.92/3.14 1. ((sdtasdt0 (sdtpldt0 (xR) (smndt0 (xS))) (sdtpldt0 (xR) (smndt0 (xS)))) != (sdtasdt0 (sdtpldt0 (xR) (smndt0 (xS))) (sdtpldt0 (xR) (smndt0 (xS))))) ### Refl(=) % 2.92/3.14 2. ((sdtasdt0 (sdtpldt0 (xR) (smndt0 (xS))) (sdtpldt0 (xR) (smndt0 (xS)))) != (sdtasdt0 (sdtpldt0 (xR) (smndt0 (xS))) (sdtpldt0 (xR) (smndt0 (xS))))) ### Refl(=) % 2.92/3.14 3. ((sdtpldt0 (sdtasdt0 (xR) (xR)) (smndt0 (xN))) != (sdtpldt0 (sdtasdt0 (xR) (xR)) (smndt0 (xN)))) ### Refl(=) % 2.92/3.14 4. (aScalar0 (xN)) (-. (aScalar0 (xN))) ### Axiom % 2.92/3.14 5. (-. (aScalar0 (smndt0 (xN)))) (aScalar0 (xN)) ### Extension/test/mNegScctrp 4 % 2.92/3.14 6. (aScalar0 (xS)) (-. (aScalar0 (xS))) ### Axiom % 2.92/3.14 7. (aScalar0 (xS)) (-. (aScalar0 (xS))) ### Axiom % 2.92/3.14 8. (-. (aScalar0 (sdtasdt0 (xS) (xS)))) (aScalar0 (xS)) ### Extension/test/mMulScctrp 6 7 % 2.92/3.14 9. (aScalar0 (sz0z00)) (-. (aScalar0 (sz0z00))) ### Axiom % 2.92/3.14 10. ((sdtpldt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS))) != (sdtpldt0 (sdtasdt0 (xS) (xS)) (smndt0 (xN)))) ((sdtpldt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS))) = (sdtpldt0 (sdtasdt0 (xS) (xS)) (smndt0 (xN)))) ### Axiom % 2.92/3.14 11. (((sdtpldt0 (sdtpldt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS))) (sz0z00)) = (sdtpldt0 (smndt0 (xN)) (sdtpldt0 (sdtasdt0 (xS) (xS)) (sz0z00)))) /\ (((sdtpldt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS))) = (sdtpldt0 (sdtasdt0 (xS) (xS)) (smndt0 (xN)))) /\ (((sdtasdt0 (sdtasdt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS))) (sz0z00)) = (sdtasdt0 (smndt0 (xN)) (sdtasdt0 (sdtasdt0 (xS) (xS)) (sz0z00)))) /\ ((sdtasdt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS))) = (sdtasdt0 (sdtasdt0 (xS) (xS)) (smndt0 (xN))))))) ((sdtpldt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS))) != (sdtpldt0 (sdtasdt0 (xS) (xS)) (smndt0 (xN)))) ### ConjTree 10 % 2.92/3.14 12. (((aScalar0 (smndt0 (xN))) /\ ((aScalar0 (sdtasdt0 (xS) (xS))) /\ (aScalar0 (sz0z00)))) => (((sdtpldt0 (sdtpldt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS))) (sz0z00)) = (sdtpldt0 (smndt0 (xN)) (sdtpldt0 (sdtasdt0 (xS) (xS)) (sz0z00)))) /\ (((sdtpldt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS))) = (sdtpldt0 (sdtasdt0 (xS) (xS)) (smndt0 (xN)))) /\ (((sdtasdt0 (sdtasdt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS))) (sz0z00)) = (sdtasdt0 (smndt0 (xN)) (sdtasdt0 (sdtasdt0 (xS) (xS)) (sz0z00)))) /\ ((sdtasdt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS))) = (sdtasdt0 (sdtasdt0 (xS) (xS)) (smndt0 (xN)))))))) ((sdtpldt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS))) != (sdtpldt0 (sdtasdt0 (xS) (xS)) (smndt0 (xN)))) (aScalar0 (sz0z00)) (aScalar0 (xS)) (aScalar0 (xN)) ### DisjTree 5 8 9 11 % 2.92/3.14 13. (All W2, (((aScalar0 (smndt0 (xN))) /\ ((aScalar0 (sdtasdt0 (xS) (xS))) /\ (aScalar0 W2))) => (((sdtpldt0 (sdtpldt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS))) W2) = (sdtpldt0 (smndt0 (xN)) (sdtpldt0 (sdtasdt0 (xS) (xS)) W2))) /\ (((sdtpldt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS))) = (sdtpldt0 (sdtasdt0 (xS) (xS)) (smndt0 (xN)))) /\ (((sdtasdt0 (sdtasdt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS))) W2) = (sdtasdt0 (smndt0 (xN)) (sdtasdt0 (sdtasdt0 (xS) (xS)) W2))) /\ ((sdtasdt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS))) = (sdtasdt0 (sdtasdt0 (xS) (xS)) (smndt0 (xN))))))))) (aScalar0 (xN)) (aScalar0 (xS)) (aScalar0 (sz0z00)) ((sdtpldt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS))) != (sdtpldt0 (sdtasdt0 (xS) (xS)) (smndt0 (xN)))) ### All 12 % 2.92/3.14 14. (All W1, (All W2, (((aScalar0 (smndt0 (xN))) /\ ((aScalar0 W1) /\ (aScalar0 W2))) => (((sdtpldt0 (sdtpldt0 (smndt0 (xN)) W1) W2) = (sdtpldt0 (smndt0 (xN)) (sdtpldt0 W1 W2))) /\ (((sdtpldt0 (smndt0 (xN)) W1) = (sdtpldt0 W1 (smndt0 (xN)))) /\ (((sdtasdt0 (sdtasdt0 (smndt0 (xN)) W1) W2) = (sdtasdt0 (smndt0 (xN)) (sdtasdt0 W1 W2))) /\ ((sdtasdt0 (smndt0 (xN)) W1) = (sdtasdt0 W1 (smndt0 (xN)))))))))) ((sdtpldt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS))) != (sdtpldt0 (sdtasdt0 (xS) (xS)) (smndt0 (xN)))) (aScalar0 (sz0z00)) (aScalar0 (xS)) (aScalar0 (xN)) ### All 13 % 2.92/3.14 15. (All W0, (All W1, (All W2, (((aScalar0 W0) /\ ((aScalar0 W1) /\ (aScalar0 W2))) => (((sdtpldt0 (sdtpldt0 W0 W1) W2) = (sdtpldt0 W0 (sdtpldt0 W1 W2))) /\ (((sdtpldt0 W0 W1) = (sdtpldt0 W1 W0)) /\ (((sdtasdt0 (sdtasdt0 W0 W1) W2) = (sdtasdt0 W0 (sdtasdt0 W1 W2))) /\ ((sdtasdt0 W0 W1) = (sdtasdt0 W1 W0))))))))) (aScalar0 (xN)) (aScalar0 (xS)) (aScalar0 (sz0z00)) ((sdtpldt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS))) != (sdtpldt0 (sdtasdt0 (xS) (xS)) (smndt0 (xN)))) ### All 14 % 2.92/3.14 16. ((sdtpldt0 (sdtpldt0 (sdtasdt0 (xR) (xR)) (smndt0 (xN))) (sdtpldt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS)))) != (sdtpldt0 (sdtpldt0 (sdtasdt0 (xR) (xR)) (smndt0 (xN))) (sdtpldt0 (sdtasdt0 (xS) (xS)) (smndt0 (xN))))) (aScalar0 (sz0z00)) (aScalar0 (xS)) (aScalar0 (xN)) (All W0, (All W1, (All W2, (((aScalar0 W0) /\ ((aScalar0 W1) /\ (aScalar0 W2))) => (((sdtpldt0 (sdtpldt0 W0 W1) W2) = (sdtpldt0 W0 (sdtpldt0 W1 W2))) /\ (((sdtpldt0 W0 W1) = (sdtpldt0 W1 W0)) /\ (((sdtasdt0 (sdtasdt0 W0 W1) W2) = (sdtasdt0 W0 (sdtasdt0 W1 W2))) /\ ((sdtasdt0 W0 W1) = (sdtasdt0 W1 W0))))))))) ### NotEqual 3 15 % 2.92/3.14 17. ((sdtasdt0 (sdtpldt0 (xR) (smndt0 (xS))) (sdtpldt0 (xR) (smndt0 (xS)))) != (sdtpldt0 (sdtpldt0 (sdtasdt0 (xR) (xR)) (smndt0 (xN))) (sdtpldt0 (sdtasdt0 (xS) (xS)) (smndt0 (xN))))) ((sdtasdt0 (sdtpldt0 (xR) (smndt0 (xS))) (sdtpldt0 (xR) (smndt0 (xS)))) = (sdtpldt0 (sdtpldt0 (sdtasdt0 (xR) (xR)) (smndt0 (xN))) (sdtpldt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS))))) (All W0, (All W1, (All W2, (((aScalar0 W0) /\ ((aScalar0 W1) /\ (aScalar0 W2))) => (((sdtpldt0 (sdtpldt0 W0 W1) W2) = (sdtpldt0 W0 (sdtpldt0 W1 W2))) /\ (((sdtpldt0 W0 W1) = (sdtpldt0 W1 W0)) /\ (((sdtasdt0 (sdtasdt0 W0 W1) W2) = (sdtasdt0 W0 (sdtasdt0 W1 W2))) /\ ((sdtasdt0 W0 W1) = (sdtasdt0 W1 W0))))))))) (aScalar0 (xN)) (aScalar0 (xS)) (aScalar0 (sz0z00)) ### TransEq 1 2 16 % 2.92/3.14 18. ((aScalar0 (xN)) /\ ((xN) = (sdtasdt0 (xR) (xS)))) (aScalar0 (sz0z00)) (aScalar0 (xS)) (All W0, (All W1, (All W2, (((aScalar0 W0) /\ ((aScalar0 W1) /\ (aScalar0 W2))) => (((sdtpldt0 (sdtpldt0 W0 W1) W2) = (sdtpldt0 W0 (sdtpldt0 W1 W2))) /\ (((sdtpldt0 W0 W1) = (sdtpldt0 W1 W0)) /\ (((sdtasdt0 (sdtasdt0 W0 W1) W2) = (sdtasdt0 W0 (sdtasdt0 W1 W2))) /\ ((sdtasdt0 W0 W1) = (sdtasdt0 W1 W0))))))))) ((sdtasdt0 (sdtpldt0 (xR) (smndt0 (xS))) (sdtpldt0 (xR) (smndt0 (xS)))) = (sdtpldt0 (sdtpldt0 (sdtasdt0 (xR) (xR)) (smndt0 (xN))) (sdtpldt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS))))) ((sdtasdt0 (sdtpldt0 (xR) (smndt0 (xS))) (sdtpldt0 (xR) (smndt0 (xS)))) != (sdtpldt0 (sdtpldt0 (sdtasdt0 (xR) (xR)) (smndt0 (xN))) (sdtpldt0 (sdtasdt0 (xS) (xS)) (smndt0 (xN))))) ### And 17 % 2.92/3.14 19. ((aScalar0 (xS)) /\ ((xS) = (sdtasdt0 (xF) (xD)))) ((sdtasdt0 (sdtpldt0 (xR) (smndt0 (xS))) (sdtpldt0 (xR) (smndt0 (xS)))) != (sdtpldt0 (sdtpldt0 (sdtasdt0 (xR) (xR)) (smndt0 (xN))) (sdtpldt0 (sdtasdt0 (xS) (xS)) (smndt0 (xN))))) ((sdtasdt0 (sdtpldt0 (xR) (smndt0 (xS))) (sdtpldt0 (xR) (smndt0 (xS)))) = (sdtpldt0 (sdtpldt0 (sdtasdt0 (xR) (xR)) (smndt0 (xN))) (sdtpldt0 (smndt0 (xN)) (sdtasdt0 (xS) (xS))))) (All W0, (All W1, (All W2, (((aScalar0 W0) /\ ((aScalar0 W1) /\ (aScalar0 W2))) => (((sdtpldt0 (sdtpldt0 W0 W1) W2) = (sdtpldt0 W0 (sdtpldt0 W1 W2))) /\ (((sdtpldt0 W0 W1) = (sdtpldt0 W1 W0)) /\ (((sdtasdt0 (sdtasdt0 W0 W1) W2) = (sdtasdt0 W0 (sdtasdt0 W1 W2))) /\ ((sdtasdt0 W0 W1) = (sdtasdt0 W1 W0))))))))) (aScalar0 (sz0z00)) ((aScalar0 (xN)) /\ ((xN) = (sdtasdt0 (xR) (xS)))) ### And 18 % 2.92/3.14 % SZS output end Proof % 2.92/3.14 (* END-PROOF *) %------------------------------------------------------------------------------