%------------------------------------------------------------------------------ % File : SuperZenon---0.0.1 % Problem : COM146+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 : n015.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:17 EDT 2022 % Result : Theorem 68.90s 69.11s % Output : Proof 68.90s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : COM146+1 : TPTP v8.1.0. Released v6.4.0. % 0.04/0.12 % Command : run_super_zenon -p0 -itptp -om -max-time %d %s % 0.12/0.34 % Computer : n015.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 600 % 0.12/0.34 % DateTime : Thu Jun 16 18:54:26 EDT 2022 % 0.12/0.34 % CPUTime : % 68.90/69.11 % SZS status Theorem % 68.90/69.11 (* PROOF-FOUND *) % 68.90/69.11 (* BEGIN-PROOF *) % 68.90/69.11 % SZS output start Proof % 68.90/69.11 1. ((vvar T_0) != (vvar T_0)) ### Refl(=) % 68.90/69.11 2. ((vreduce (vvar T_0)) = (vsomeExp T_1)) ((vsomeExp T_1) != (vreduce (vvar T_0))) ### Sym(=) % 68.90/69.11 3. ((vnoExp) != (vsomeExp T_1)) ((vsomeExp T_1) = (vnoExp)) ### Sym(=) % 68.90/69.11 4. (((vvar T_0) = (vvar T_0)) => (((vsomeExp T_1) = (vreduce (vvar T_0))) => ((vsomeExp T_1) = (vnoExp)))) ((vnoExp) != (vsomeExp T_1)) ((vreduce (vvar T_0)) = (vsomeExp T_1)) ### DisjTree 1 2 3 % 68.90/69.11 5. (All RESULT, (((vvar T_0) = (vvar T_0)) => ((RESULT = (vreduce (vvar T_0))) => (RESULT = (vnoExp))))) ((vreduce (vvar T_0)) = (vsomeExp T_1)) ((vnoExp) != (vsomeExp T_1)) ### All 4 % 68.90/69.11 6. (All VExp0, (All RESULT, ((VExp0 = (vvar T_0)) => ((RESULT = (vreduce VExp0)) => (RESULT = (vnoExp)))))) ((vnoExp) != (vsomeExp T_1)) ((vreduce (vvar T_0)) = (vsomeExp T_1)) ### All 5 % 68.90/69.11 7. (All Vx, (All VExp0, (All RESULT, ((VExp0 = (vvar Vx)) => ((RESULT = (vreduce VExp0)) => (RESULT = (vnoExp))))))) ((vreduce (vvar T_0)) = (vsomeExp T_1)) ((vnoExp) != (vsomeExp T_1)) ### All 6 % 68.90/69.11 8. (All VExp0, ((vnoExp) != (vsomeExp VExp0))) ((vreduce (vvar T_0)) = (vsomeExp T_1)) (All Vx, (All VExp0, (All RESULT, ((VExp0 = (vvar Vx)) => ((RESULT = (vreduce VExp0)) => (RESULT = (vnoExp))))))) ### All 7 % 68.90/69.11 9. (-. ((((vreduce (vvar T_0)) = (vsomeExp T_1)) /\ (vtcheck T_2 (vvar T_0) T_3)) => (vtcheck T_2 T_1 T_3))) (All Vx, (All VExp0, (All RESULT, ((VExp0 = (vvar Vx)) => ((RESULT = (vreduce VExp0)) => (RESULT = (vnoExp))))))) (All VExp0, ((vnoExp) != (vsomeExp VExp0))) ### ConjTree 8 % 68.90/69.11 10. (-. (All VT, ((((vreduce (vvar T_0)) = (vsomeExp T_1)) /\ (vtcheck T_2 (vvar T_0) VT)) => (vtcheck T_2 T_1 VT)))) (All VExp0, ((vnoExp) != (vsomeExp VExp0))) (All Vx, (All VExp0, (All RESULT, ((VExp0 = (vvar Vx)) => ((RESULT = (vreduce VExp0)) => (RESULT = (vnoExp))))))) ### NotAllEx 9 % 68.90/69.11 11. (-. (All Veout, (All VT, ((((vreduce (vvar T_0)) = (vsomeExp Veout)) /\ (vtcheck T_2 (vvar T_0) VT)) => (vtcheck T_2 Veout VT))))) (All Vx, (All VExp0, (All RESULT, ((VExp0 = (vvar Vx)) => ((RESULT = (vreduce VExp0)) => (RESULT = (vnoExp))))))) (All VExp0, ((vnoExp) != (vsomeExp VExp0))) ### NotAllEx 10 % 68.90/69.11 12. (-. (All VC, (All Veout, (All VT, ((((vreduce (vvar T_0)) = (vsomeExp Veout)) /\ (vtcheck VC (vvar T_0) VT)) => (vtcheck VC Veout VT)))))) (All VExp0, ((vnoExp) != (vsomeExp VExp0))) (All Vx, (All VExp0, (All RESULT, ((VExp0 = (vvar Vx)) => ((RESULT = (vreduce VExp0)) => (RESULT = (vnoExp))))))) ### NotAllEx 11 % 68.90/69.11 13. (-. (All Vx, (All VC, (All Veout, (All VT, ((((vreduce (vvar Vx)) = (vsomeExp Veout)) /\ (vtcheck VC (vvar Vx) VT)) => (vtcheck VC Veout VT))))))) (All Vx, (All VExp0, (All RESULT, ((VExp0 = (vvar Vx)) => ((RESULT = (vreduce VExp0)) => (RESULT = (vnoExp))))))) (All VExp0, ((vnoExp) != (vsomeExp VExp0))) ### NotAllEx 12 % 68.90/69.11 % SZS output end Proof % 68.90/69.11 (* END-PROOF *) %------------------------------------------------------------------------------