%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : COM147+1 : TPTP v8.1.0. Released v6.4.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 : Fri Jul 15 01:46:18 EDT 2022 % Result : Theorem 19.43s 19.67s % Output : Proof 19.43s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : COM147+1 : TPTP v8.1.0. Released v6.4.0. % 0.07/0.13 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.14/0.34 % Computer : n009.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 600 % 0.14/0.34 % DateTime : Thu Jun 16 19:06:07 EDT 2022 % 0.14/0.35 % CPUTime : % 19.43/19.67 % SZS status Theorem % 19.43/19.67 (* PROOF-FOUND *) % 19.43/19.67 (* BEGIN-PROOF *) % 19.43/19.67 % SZS output start Proof % 19.43/19.67 1. ((vabs T_0 T_1 (ve1)) != (vabs T_0 T_1 (ve1))) ### Refl(=) % 19.43/19.67 2. (-. (visValue (vabs T_0 T_1 (ve1)))) (visValue (vabs T_0 T_1 (ve1))) ### Axiom % 19.43/19.67 3. (((vabs T_0 T_1 (ve1)) = (vabs T_0 T_1 (ve1))) => (visValue (vabs T_0 T_1 (ve1)))) (-. (visValue (vabs T_0 T_1 (ve1)))) ### Imply 1 2 % 19.43/19.67 4. (All VExp0, ((VExp0 = (vabs T_0 T_1 (ve1))) => (visValue VExp0))) (-. (visValue (vabs T_0 T_1 (ve1)))) ### All 3 % 19.43/19.67 5. (All Ve, (All VExp0, ((VExp0 = (vabs T_0 T_1 Ve)) => (visValue VExp0)))) (-. (visValue (vabs T_0 T_1 (ve1)))) ### All 4 % 19.43/19.67 6. (All VS, (All Ve, (All VExp0, ((VExp0 = (vabs T_0 VS Ve)) => (visValue VExp0))))) (-. (visValue (vabs T_0 T_1 (ve1)))) ### All 5 % 19.43/19.67 7. (All Vx, (All VS, (All Ve, (All VExp0, ((VExp0 = (vabs Vx VS Ve)) => (visValue VExp0)))))) (-. (visValue (vabs T_0 T_1 (ve1)))) ### All 6 % 19.43/19.67 8. (-. (((vtcheck (vempty) (vabs T_0 T_1 (ve1)) T_2) /\ (-. (visValue (vabs T_0 T_1 (ve1))))) => (Ex Veout, ((vreduce (vabs T_0 T_1 (ve1))) = (vsomeExp Veout))))) (All Vx, (All VS, (All Ve, (All VExp0, ((VExp0 = (vabs Vx VS Ve)) => (visValue VExp0)))))) ### ConjTree 7 % 19.43/19.67 9. (-. (All VS, (((vtcheck (vempty) (vabs T_0 VS (ve1)) T_2) /\ (-. (visValue (vabs T_0 VS (ve1))))) => (Ex Veout, ((vreduce (vabs T_0 VS (ve1))) = (vsomeExp Veout)))))) (All Vx, (All VS, (All Ve, (All VExp0, ((VExp0 = (vabs Vx VS Ve)) => (visValue VExp0)))))) ### NotAllEx 8 % 19.43/19.67 10. (-. (All Vx, (All VS, (((vtcheck (vempty) (vabs Vx VS (ve1)) T_2) /\ (-. (visValue (vabs Vx VS (ve1))))) => (Ex Veout, ((vreduce (vabs Vx VS (ve1))) = (vsomeExp Veout))))))) (All Vx, (All VS, (All Ve, (All VExp0, ((VExp0 = (vabs Vx VS Ve)) => (visValue VExp0)))))) ### NotAllEx 9 % 19.43/19.67 11. (-. (All VTin, (All Vx, (All VS, (((vtcheck (vempty) (vabs Vx VS (ve1)) VTin) /\ (-. (visValue (vabs Vx VS (ve1))))) => (Ex Veout, ((vreduce (vabs Vx VS (ve1))) = (vsomeExp Veout)))))))) (All Vx, (All VS, (All Ve, (All VExp0, ((VExp0 = (vabs Vx VS Ve)) => (visValue VExp0)))))) ### NotAllEx 10 % 19.43/19.67 % SZS output end Proof % 19.43/19.67 (* END-PROOF *) %------------------------------------------------------------------------------