%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : NLP006+1 : TPTP v8.2.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon_modulo %d %s % Computer : n011.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 : 300s % DateTime : Tue Jun 25 02:03:06 EDT 2024 % Result : Unknown 0.50s 0.74s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.11 % Problem : NLP006+1 : TPTP v8.2.0. Released v2.4.0. % 0.06/0.11 % Command : run_zenon_modulo %d %s % 0.09/0.31 % Computer : n011.cluster.edu % 0.09/0.31 % Model : x86_64 x86_64 % 0.09/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.31 % Memory : 8042.1875MB % 0.09/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.31 % CPULimit : 300 % 0.09/0.31 % WCLimit : 300 % 0.09/0.31 % DateTime : Sat Jun 22 23:09:24 EDT 2024 % 0.09/0.31 % CPUTime : % 0.50/0.74 Zenon error: exhausted search space without finding a proof % 0.50/0.74 (* Current branch: % 0.50/0.74 (Tau_208 != zenon_X378) % 0.50/0.74 (Tau_204 != zenon_X325) % 0.50/0.74 (Tau_206 != Tau_199) % 0.50/0.74 (-. (in zenon_X240 Tau_200)) % 0.50/0.74 (-. (in zenon_X269 Tau_206)) % 0.50/0.74 (-. (in zenon_X374 Tau_206)) % 0.50/0.74 (-. (in zenon_X378 Tau_206)) % 0.50/0.74 (-. (in zenon_X343 Tau_199)) % 0.50/0.74 (hollywood Tau_200) % 0.50/0.74 (zenon_X309 != Tau_204) % 0.50/0.74 (-. (in zenon_X328 Tau_199)) % 0.50/0.74 (-. (old zenon_X312)) % 0.50/0.74 (furniture Tau_206) % 0.50/0.74 (in Tau_201 Tau_200) % 0.50/0.74 (-. (city zenon_X226)) % 0.50/0.74 (Tau_205 = Tau_208) % 0.50/0.74 (Tau_200 != zenon_X226) % 0.50/0.74 (-. (in zenon_X246 Tau_200)) % 0.50/0.74 (-. (lonely zenon_X320)) % 0.50/0.74 (-. (young zenon_X259)) % 0.50/0.74 (Tau_204 != zenon_X338) % 0.50/0.74 (man Tau_204) % 0.50/0.74 (-. (in zenon_X350 Tau_199)) % 0.50/0.74 (fellow Tau_204) % 0.50/0.74 (way Tau_203) % 0.50/0.74 (-. (in zenon_X271 Tau_200)) % 0.50/0.74 (Tau_201 != zenon_X274) % 0.50/0.74 (zenon_X269 != Tau_205) % 0.50/0.74 (-. (city zenon_X262)) % 0.50/0.74 (zenon_X317 != Tau_205) % 0.50/0.74 (-. (young zenon_X252)) % 0.50/0.74 (-. (in zenon_X251 Tau_200)) % 0.50/0.74 (-. (young zenon_X364)) % 0.50/0.74 (-. (in zenon_X301 Tau_206)) % 0.50/0.74 (Tau_201 != zenon_X234) % 0.50/0.74 (Tau_208 != Tau_204) % 0.50/0.74 (zenon_X369 != Tau_205) % 0.50/0.74 (Tau_208 != zenon_X377) % 0.50/0.74 (Tau_207 != zenon_X349) % 0.50/0.74 (furniture Tau_199) % 0.50/0.74 (Tau_205 != zenon_X259) % 0.50/0.74 (Tau_202 != zenon_X304) % 0.50/0.74 (-. (city zenon_X218)) % 0.50/0.74 (-. (in zenon_X349 Tau_199)) % 0.50/0.74 (Tau_204 != Tau_205) % 0.50/0.74 (-. (in zenon_X286 Tau_199)) % 0.50/0.74 (zenon_X349 != Tau_204) % 0.50/0.74 (Tau_200 != Tau_199) % 0.50/0.74 (Tau_208 != zenon_X333) % 0.50/0.74 (-. (young zenon_X341)) % 0.50/0.74 (zenon_X324 != Tau_204) % 0.50/0.74 (Tau_200 != zenon_X218) % 0.50/0.74 (-. (in zenon_X275 Tau_200)) % 0.50/0.74 (-. (young zenon_X338)) % 0.50/0.74 (Tau_201 != zenon_X261) % 0.50/0.74 (Tau_201 != zenon_X270) % 0.50/0.74 (Tau_201 != zenon_X240) % 0.50/0.74 (car Tau_202) % 0.50/0.74 (Tau_201 != zenon_X279) % 0.50/0.74 (-. (in zenon_X333 Tau_206)) % 0.50/0.74 (-. (in zenon_X278 Tau_200)) % 0.50/0.74 (-. (in zenon_X233 Tau_200)) % 0.50/0.74 (-. (in zenon_X317 Tau_206)) % 0.50/0.74 (Tau_203 != zenon_X247) % 0.50/0.74 (Tau_204 != zenon_X256) % 0.50/0.74 (-. (in zenon_X274 Tau_200)) % 0.50/0.74 (Tau_201 != zenon_X275) % 0.50/0.74 (lonely Tau_203) % 0.50/0.74 (-. (in zenon_X279 Tau_200)) % 0.50/0.74 (fellow Tau_205) % 0.50/0.74 (Tau_207 != zenon_X328) % 0.50/0.74 (zenon_X354 != Tau_204) % 0.50/0.74 (Tau_207 != zenon_X324) % 0.50/0.74 (-. (in zenon_X225 Tau_199)) % 0.50/0.74 (barrel Tau_201 Tau_202) % 0.50/0.74 (-. (event zenon_X234)) % 0.50/0.74 (zenon_X340 != Tau_204) % 0.50/0.74 (Tau_208 != zenon_X374) % 0.50/0.74 (zenon_X350 != Tau_204) % 0.50/0.74 (-. (in zenon_X258 Tau_200)) % 0.50/0.74 (zenon_X286 != Tau_204) % 0.50/0.74 (Tau_207 != zenon_X340) % 0.50/0.74 (Tau_205 != zenon_X252) % 0.50/0.74 (Tau_206 != zenon_X209) % 0.50/0.74 (Tau_207 != zenon_X225) % 0.50/0.74 (-. (event zenon_X280)) % 0.50/0.74 (-. (young zenon_X367)) % 0.50/0.74 (Tau_207 != zenon_X309) % 0.50/0.74 (-. (in zenon_X354 Tau_199)) % 0.50/0.74 (zenon_X343 != Tau_204) % 0.50/0.74 (Tau_207 != zenon_X350) % 0.50/0.74 (-. (in zenon_X324 Tau_199)) % 0.50/0.74 (man Tau_205) % 0.50/0.74 (street Tau_203) % 0.50/0.74 (-. (in zenon_X261 Tau_200)) % 0.50/0.74 (Tau_202 != zenon_X312) % 0.50/0.74 (Tau_200 != zenon_X209) % 0.50/0.74 (Tau_201 != zenon_X255) % 0.50/0.74 (-. (in zenon_X217 zenon_X209)) % 0.50/0.74 (Tau_201 != zenon_X278) % 0.50/0.74 (Tau_204 != zenon_X259) % 0.50/0.74 (Tau_205 != zenon_X364) % 0.50/0.74 (zenon_X377 != Tau_205) % 0.50/0.74 (-. (in zenon_X369 Tau_206)) % 0.50/0.74 (Tau_208 != zenon_X269) % 0.50/0.74 (Tau_203 != zenon_X329) % 0.50/0.74 (zenon_X378 != Tau_205) % 0.50/0.74 (Tau_205 != zenon_X334) % 0.50/0.74 (Tau_204 != zenon_X364) % 0.50/0.74 (zenon_X374 != Tau_205) % 0.50/0.74 (Tau_201 != zenon_X271) % 0.50/0.74 (-. (in zenon_X340 Tau_199)) % 0.50/0.74 (city Tau_200) % 0.50/0.74 (Tau_208 != zenon_X317) % 0.50/0.74 (Tau_208 != zenon_X337) % 0.50/0.74 (zenon_X337 != Tau_205) % 0.50/0.74 (Tau_205 != zenon_X256) % 0.50/0.74 (Tau_204 != zenon_X341) % 0.50/0.74 (-. (young zenon_X334)) % 0.50/0.74 (-. (lonely zenon_X329)) % 0.50/0.74 (-. (in zenon_X337 Tau_206)) % 0.50/0.74 (Tau_208 != zenon_X366) % 0.50/0.74 (Tau_207 != zenon_X286) % 0.50/0.74 (Tau_205 != zenon_X338) % 0.50/0.74 (-. (in zenon_X366 Tau_206)) % 0.50/0.74 (zenon_X333 != Tau_205) % 0.50/0.74 (in Tau_208 Tau_206) % 0.50/0.74 (Tau_207 != zenon_X252) % 0.50/0.74 (-. (event zenon_X295)) % 0.50/0.74 (-. (old zenon_X304)) % 0.50/0.74 (Tau_208 != zenon_X301) % 0.50/0.74 (Tau_204 != zenon_X367) % 0.50/0.74 (Tau_204 != zenon_X252) % 0.50/0.74 (event Tau_201) % 0.50/0.74 (Tau_201 != zenon_X233) % 0.50/0.74 (Tau_199 != zenon_X209) % 0.50/0.74 (-. (front Tau_200)) % 0.50/0.74 (old Tau_202) % 0.50/0.74 (Tau_201 != zenon_X280) % 0.50/0.74 (-. (young zenon_X256)) % 0.50/0.74 (zenon_X366 != Tau_205) % 0.50/0.74 (-. (young zenon_X325)) % 0.50/0.74 (seat Tau_199) % 0.50/0.74 (Tau_205 != zenon_X325) % 0.50/0.74 (Tau_201 != zenon_X258) % 0.50/0.74 (Tau_205 != zenon_X341) % 0.50/0.74 (young Tau_204) % 0.50/0.74 (-. (lonely zenon_X247)) % 0.50/0.74 (Tau_204 != zenon_X334) % 0.50/0.74 (zenon_X301 != Tau_205) % 0.50/0.74 (white Tau_202) % 0.50/0.74 (Tau_200 != zenon_X262) % 0.50/0.74 (-. (old zenon_X241)) % 0.50/0.74 (-. (in zenon_X309 Tau_199)) % 0.50/0.74 (Tau_201 != zenon_X246) % 0.50/0.74 (zenon_X328 != Tau_204) % 0.50/0.74 (seat Tau_206) % 0.50/0.74 (-. (in zenon_X270 Tau_200)) % 0.50/0.74 (Tau_203 != zenon_X320) % 0.50/0.74 (Tau_205 != zenon_X367) % 0.50/0.74 (Tau_207 != zenon_X343) % 0.50/0.74 (Tau_207 != zenon_X354) % 0.50/0.74 (Tau_208 != zenon_X369) % 0.50/0.74 (young Tau_205) % 0.50/0.74 (front Tau_206) % 0.50/0.74 (Tau_207 != Tau_205) % 0.50/0.74 (Tau_202 != zenon_X241) % 0.50/0.74 (dirty Tau_202) % 0.50/0.74 (Tau_201 != zenon_X251) % 0.50/0.74 (in Tau_207 Tau_199) % 0.50/0.74 (-. (in zenon_X255 Tau_200)) % 0.50/0.74 (zenon_X225 != Tau_204) % 0.50/0.74 (Tau_208 != Tau_207) % 0.50/0.74 (chevy Tau_202) % 0.50/0.74 (-. (in zenon_X377 Tau_206)) % 0.50/0.74 (Tau_206 != Tau_200) % 0.50/0.74 (down Tau_201 Tau_203) % 0.50/0.74 (front Tau_199) % 0.50/0.74 (Tau_204 = Tau_207) % 0.50/0.74 (Tau_201 != zenon_X295) % 0.50/0.74 *) % 0.50/0.74 (* NO-PROOF *) % 0.50/0.74 % SZS status GaveUp % 0.50/0.74 Number of rewrites on terms: 0 % 0.50/0.74 Number of rewrites on props: 0 % 0.50/0.74 nodes searched: 3072 % 0.50/0.74 max branch formulas: 534 % 0.50/0.74 proof nodes created: 525 % 0.50/0.74 formulas created: 30439 % 0.50/0.74 %------------------------------------------------------------------------------