%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : NLP135+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n018.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 05:54:36 EDT 2022 % Result : Unknown 0.51s 0.69s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.11 % Problem : NLP135+1 : TPTP v8.1.0. Released v2.4.0. % 0.03/0.12 % Command : run_zenon %s %d % 0.11/0.33 % Computer : n018.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 600 % 0.11/0.33 % DateTime : Thu Jun 30 19:54:01 EDT 2022 % 0.11/0.33 % CPUTime : % 0.51/0.69 Zenon error: exhausted search space without finding a proof % 0.51/0.69 (* Current branch: % 0.51/0.69 (in T_0 T_1 T_2) % 0.51/0.69 (state T_0 T_3) % 0.51/0.69 (-. (young zenon_X4 T_5)) % 0.51/0.69 (member T_0 T_6 T_7) % 0.51/0.69 (-. (young T_0 T_8)) % 0.51/0.69 (placename T_0 T_9) % 0.51/0.69 (in T_0 T_10 T_2) % 0.51/0.69 (T_11 != zenon_X12) % 0.51/0.69 (old T_0 T_2) % 0.51/0.69 (be T_0 T_13 zenon_X14 T_15) % 0.51/0.69 (fellow T_0 T_6) % 0.51/0.69 (T_16 != zenon_X17) % 0.51/0.69 (-. (young T_0 T_18)) % 0.51/0.69 (zenon_X4 != T_0) % 0.51/0.69 (of T_0 T_9 T_2) % 0.51/0.69 (street T_0 T_11) % 0.51/0.69 (zenon_X19 != T_7) % 0.51/0.69 (be T_0 T_20 T_16 T_21) % 0.51/0.69 (T_2 != zenon_X14) % 0.51/0.69 (-. (in T_0 T_15 T_15)) % 0.51/0.69 (white T_0 T_2) % 0.51/0.69 (-. (young T_0 T_22)) % 0.51/0.69 (chevy T_0 T_2) % 0.51/0.69 (member T_0 T_23 zenon_X24) % 0.51/0.69 (-. (lonely T_0 zenon_X12)) % 0.51/0.69 (state T_0 T_25) % 0.51/0.69 (state T_0 T_13) % 0.51/0.69 (be T_0 T_3 zenon_X17 T_16) % 0.51/0.69 (T_21 != T_16) % 0.51/0.69 (-. (placename T_0 zenon_X26)) % 0.51/0.69 (zenon_X24 != T_7) % 0.51/0.69 (-. (in T_0 zenon_X14 zenon_X14)) % 0.51/0.69 (zenon_X27 != T_7) % 0.51/0.69 (-. (in T_0 zenon_X17 zenon_X17)) % 0.51/0.69 (state T_0 T_20) % 0.51/0.69 (member T_0 T_18 zenon_X19) % 0.51/0.69 (T_10 != T_2) % 0.51/0.69 (T_2 != zenon_X17) % 0.51/0.69 (zenon_X17 != zenon_X14) % 0.51/0.69 (T_1 != T_2) % 0.51/0.69 (member zenon_X4 T_28 T_7) % 0.51/0.69 (two T_0 T_7) % 0.51/0.69 (in T_0 T_16 zenon_X17) % 0.51/0.69 (-. (young T_0 T_29)) % 0.51/0.69 (member T_0 T_8 zenon_X30) % 0.51/0.69 (T_16 != T_2) % 0.51/0.69 (T_16 != T_15) % 0.51/0.69 (T_9 != zenon_X26) % 0.51/0.69 (agent T_0 T_10 T_2) % 0.51/0.69 (T_10 != zenon_X31) % 0.51/0.69 (T_6 != T_23) % 0.51/0.69 (T_6 != T_18) % 0.51/0.69 (zenon_X32 != T_7) % 0.51/0.69 (-. (member T_0 zenon_X33 T_7)) % 0.51/0.69 (-. (young T_0 T_23)) % 0.51/0.69 (zenon_X30 != T_7) % 0.51/0.69 (down T_0 T_10 T_11) % 0.51/0.69 (T_6 != zenon_X33) % 0.51/0.69 (-. (in T_0 T_2 T_2)) % 0.51/0.69 (actual_world T_0) % 0.51/0.69 (dirty T_0 T_2) % 0.51/0.69 (T_6 != T_8) % 0.51/0.69 (member T_0 T_22 zenon_X32) % 0.51/0.69 (T_16 != zenon_X14) % 0.51/0.69 (T_2 != T_15) % 0.51/0.69 (T_6 != T_29) % 0.51/0.69 (group T_0 T_7) % 0.51/0.69 (member zenon_X4 T_5 zenon_X34) % 0.51/0.69 (T_6 != T_22) % 0.51/0.69 (city T_0 T_2) % 0.51/0.69 (barrel T_0 T_10) % 0.51/0.69 (in T_0 T_15 zenon_X14) % 0.51/0.69 (lonely T_0 T_11) % 0.51/0.69 (T_2 != zenon_X35) % 0.51/0.69 (-. (old T_0 zenon_X35)) % 0.51/0.69 (event T_0 T_10) % 0.51/0.69 (T_15 != zenon_X14) % 0.51/0.69 (-. (barrel T_0 zenon_X31)) % 0.51/0.69 (be T_0 T_25 T_2 T_1) % 0.51/0.69 (in T_0 T_21 T_16) % 0.51/0.69 (member T_0 T_29 zenon_X27) % 0.51/0.69 (young T_0 T_6) % 0.51/0.69 (present T_0 T_10) % 0.51/0.69 (zenon_X34 != T_7) % 0.51/0.69 (-. (in T_0 T_16 T_16)) % 0.51/0.69 (hollywood_placename T_0 T_9) % 0.51/0.69 (-. (young zenon_X4 T_28)) % 0.51/0.69 *) % 0.51/0.69 (* NO-PROOF *) % 0.51/0.69 % SZS status GaveUp % 0.51/0.69 nodes searched: 236 % 0.51/0.69 max branch formulas: 192 % 0.51/0.69 proof nodes created: 33 % 0.51/0.69 formulas created: 2106 % 0.51/0.69 %------------------------------------------------------------------------------