%------------------------------------------------------------------------------ % File : Zenon---0.7.1 % Problem : NLP124+1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon %s %d % Computer : n020.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:29 EDT 2022 % Result : Unknown 0.54s 0.77s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : NLP124+1 : TPTP v8.1.0. Released v2.4.0. % 0.10/0.12 % Command : run_zenon %s %d % 0.12/0.33 % Computer : n020.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Fri Jul 1 07:18:45 EDT 2022 % 0.12/0.33 % CPUTime : % 0.54/0.77 Zenon error: exhausted search space without finding a proof % 0.54/0.77 (* Current branch: % 0.54/0.77 (singleton zenon_X0 T_1) % 0.54/0.77 (zenon_X2 != zenon_X3) % 0.54/0.77 (-. (relation zenon_X0 zenon_X4)) % 0.54/0.77 (T_5 != zenon_X6) % 0.54/0.77 (T_7 != zenon_X8) % 0.54/0.77 (T_5 != zenon_X9) % 0.54/0.77 (T_5 != zenon_X10) % 0.54/0.77 (T_5 != zenon_X11) % 0.54/0.77 (T_7 != zenon_X12) % 0.54/0.77 (T_1 != zenon_X9) % 0.54/0.77 (-. (nonexistent zenon_X13 T_1)) % 0.54/0.77 (-. (placename zenon_X14 zenon_X15)) % 0.54/0.77 (-. (placename T_16 zenon_X17)) % 0.54/0.77 (-. (general zenon_X18 zenon_X2)) % 0.54/0.77 (general zenon_X19 T_5) % 0.54/0.77 (T_7 != zenon_X20) % 0.54/0.77 (T_5 != zenon_X21) % 0.54/0.77 (zenon_X22 != zenon_X23) % 0.54/0.77 (zenon_X2 != zenon_X24) % 0.54/0.77 (zenon_X25 != zenon_X13) % 0.54/0.77 (abstraction T_16 T_5) % 0.54/0.77 (zenon_X23 != zenon_X26) % 0.54/0.77 (T_5 != zenon_X27) % 0.54/0.77 (-. (general T_16 zenon_X28)) % 0.54/0.77 (-. (barrel zenon_X29 zenon_X30)) % 0.54/0.77 (T_1 != zenon_X2) % 0.54/0.77 (singleton zenon_X0 T_31) % 0.54/0.77 (T_32 != zenon_X20) % 0.54/0.77 (-. (placename T_16 zenon_X9)) % 0.54/0.77 (singleton zenon_X22 T_5) % 0.54/0.77 (relation zenon_X33 zenon_X2) % 0.54/0.77 (T_5 != zenon_X34) % 0.54/0.77 (-. (placename T_16 zenon_X35)) % 0.54/0.77 (T_32 != zenon_X8) % 0.54/0.77 (T_7 != T_1) % 0.54/0.77 (-. (relname zenon_X33 zenon_X11)) % 0.54/0.77 (-. (thing zenon_X0 zenon_X36)) % 0.54/0.77 (zenon_X2 != zenon_X37) % 0.54/0.77 (zenon_X2 != zenon_X38) % 0.54/0.77 (T_5 != zenon_X39) % 0.54/0.77 (thing zenon_X40 T_32) % 0.54/0.77 (-. (placename T_16 T_31)) % 0.54/0.77 (T_32 != zenon_X41) % 0.54/0.77 (T_32 != T_1) % 0.54/0.77 (singleton zenon_X14 zenon_X2) % 0.54/0.77 (T_1 != zenon_X42) % 0.54/0.77 (T_5 != zenon_X43) % 0.54/0.77 (zenon_X2 != zenon_X44) % 0.54/0.77 (T_7 != zenon_X44) % 0.54/0.77 (T_5 != zenon_X24) % 0.54/0.77 (zenon_X2 != zenon_X45) % 0.54/0.77 (general zenon_X0 zenon_X2) % 0.54/0.77 (-. (specific zenon_X33 zenon_X2)) % 0.54/0.77 (actual_world T_16) % 0.54/0.77 (-. (relname zenon_X22 zenon_X2)) % 0.54/0.77 (-. (relation zenon_X23 zenon_X2)) % 0.54/0.77 (T_32 != T_5) % 0.54/0.77 (-. (placename T_16 zenon_X24)) % 0.54/0.77 (-. (placename zenon_X26 zenon_X46)) % 0.54/0.77 (zenon_X2 != zenon_X43) % 0.54/0.77 (-. (placename zenon_X47 zenon_X48)) % 0.54/0.77 (-. (placename T_16 zenon_X49)) % 0.54/0.77 (singleton zenon_X33 zenon_X2) % 0.54/0.77 (T_5 != zenon_X50) % 0.54/0.77 (zenon_X2 != zenon_X50) % 0.54/0.77 (T_31 != zenon_X51) % 0.54/0.77 (zenon_X14 != zenon_X23) % 0.54/0.77 (T_7 != zenon_X52) % 0.54/0.77 (-. (placename T_16 zenon_X53)) % 0.54/0.77 (T_5 != zenon_X3) % 0.54/0.77 (-. (placename T_16 zenon_X54)) % 0.54/0.77 (-. (placename T_16 zenon_X38)) % 0.54/0.77 (placename T_16 zenon_X2) % 0.54/0.77 (T_1 != zenon_X55) % 0.54/0.77 (singleton zenon_X33 T_7) % 0.54/0.77 (-. (placename T_16 zenon_X21)) % 0.54/0.77 (zenon_X2 != zenon_X17) % 0.54/0.77 (-. (specific zenon_X0 zenon_X2)) % 0.54/0.77 (T_7 != T_5) % 0.54/0.77 (nonhuman zenon_X33 zenon_X2) % 0.54/0.77 (zenon_X2 != zenon_X56) % 0.54/0.77 (T_7 != zenon_X9) % 0.54/0.77 (zenon_X2 != zenon_X49) % 0.54/0.77 (zenon_X2 != zenon_X57) % 0.54/0.77 (existent zenon_X58 T_32) % 0.54/0.77 (-. (placename T_16 T_7)) % 0.54/0.77 (T_32 != zenon_X2) % 0.54/0.77 (T_5 != zenon_X59) % 0.54/0.77 (-. (event zenon_X60 zenon_X61)) % 0.54/0.77 (T_32 != zenon_X62) % 0.54/0.77 (singleton zenon_X23 T_31) % 0.54/0.77 (zenon_X0 != zenon_X63) % 0.54/0.77 (zenon_X2 != zenon_X64) % 0.54/0.77 (zenon_X14 != zenon_X26) % 0.54/0.77 (white T_16 T_32) % 0.54/0.77 (singleton zenon_X0 T_7) % 0.54/0.77 (-. (relname zenon_X14 zenon_X65)) % 0.54/0.77 (-. (hollywood_placename zenon_X22 zenon_X66)) % 0.54/0.77 (-. (abstraction T_16 zenon_X54)) % 0.54/0.77 (location zenon_X67 T_7) % 0.54/0.77 (T_5 != zenon_X38) % 0.54/0.77 (T_32 != zenon_X68) % 0.54/0.77 (T_31 != zenon_X69) % 0.54/0.77 (thing zenon_X23 T_5) % 0.54/0.77 (-. (of T_16 zenon_X70 zenon_X71)) % 0.54/0.77 (singleton zenon_X14 T_1) % 0.54/0.77 (zenon_X2 != zenon_X72) % 0.54/0.77 (way zenon_X73 T_31) % 0.54/0.77 (T_5 != zenon_X74) % 0.54/0.77 (T_16 != zenon_X75) % 0.54/0.77 (T_32 != zenon_X76) % 0.54/0.77 (T_5 != zenon_X77) % 0.54/0.77 (-. (placename zenon_X0 zenon_X2)) % 0.54/0.77 (T_5 != zenon_X44) % 0.54/0.77 (-. (abstraction zenon_X33 zenon_X74)) % 0.54/0.77 (zenon_X2 != zenon_X34) % 0.54/0.77 (-. (abstraction zenon_X0 zenon_X56)) % 0.54/0.77 (T_5 != zenon_X78) % 0.54/0.77 (-. (placename T_16 zenon_X39)) % 0.54/0.77 (T_31 != zenon_X20) % 0.54/0.77 (relation zenon_X22 T_5) % 0.54/0.77 (-. (way zenon_X79 zenon_X80)) % 0.54/0.77 (thing T_16 T_5) % 0.54/0.77 (-. (placename T_16 zenon_X81)) % 0.54/0.77 (singleton zenon_X22 T_32) % 0.54/0.77 (T_5 != zenon_X45) % 0.54/0.77 (T_1 != zenon_X12) % 0.54/0.77 (singleton zenon_X33 T_1) % 0.54/0.77 (zenon_X2 != zenon_X11) % 0.54/0.77 (zenon_X2 != zenon_X78) % 0.54/0.77 (T_16 != zenon_X0) % 0.54/0.77 (zenon_X22 != zenon_X26) % 0.54/0.77 (-. (hollywood_placename zenon_X18 zenon_X82)) % 0.54/0.77 (zenon_X2 != zenon_X12) % 0.54/0.77 (T_5 != zenon_X4) % 0.54/0.77 (T_5 != zenon_X81) % 0.54/0.77 (-. (general zenon_X14 zenon_X83)) % 0.54/0.77 (zenon_X14 != zenon_X19) % 0.54/0.77 (T_32 != zenon_X36) % 0.54/0.77 (-. (general zenon_X0 zenon_X84)) % 0.54/0.77 (T_16 != zenon_X23) % 0.54/0.77 (-. (placename T_16 zenon_X85)) % 0.54/0.77 (-. (placename T_16 zenon_X42)) % 0.54/0.77 (-. (placename T_16 zenon_X43)) % 0.54/0.77 (-. (relation zenon_X19 zenon_X21)) % 0.54/0.77 (unisex zenon_X0 zenon_X2) % 0.54/0.77 (-. (relation zenon_X14 zenon_X86)) % 0.54/0.77 (unisex zenon_X33 T_5) % 0.54/0.77 (-. (general zenon_X19 zenon_X87)) % 0.54/0.77 (-. (placename T_16 zenon_X88)) % 0.54/0.77 (-. (entity zenon_X58 zenon_X89)) % 0.54/0.77 (-. (specific zenon_X33 T_5)) % 0.54/0.77 (zenon_X2 != zenon_X54) % 0.54/0.77 (unisex zenon_X90 T_32) % 0.54/0.77 (zenon_X2 != zenon_X36) % 0.54/0.77 (T_7 != zenon_X91) % 0.54/0.77 (T_16 != zenon_X22) % 0.54/0.77 (-. (placename T_16 zenon_X59)) % 0.54/0.77 (T_5 != zenon_X68) % 0.54/0.77 (-. (placename T_16 T_1)) % 0.54/0.77 (T_1 != zenon_X92) % 0.54/0.77 (T_5 != zenon_X57) % 0.54/0.77 (-. (existent T_16 T_1)) % 0.54/0.77 (-. (placename T_16 zenon_X45)) % 0.54/0.77 (-. (placename T_16 zenon_X11)) % 0.54/0.77 (thing zenon_X40 T_31) % 0.54/0.77 (zenon_X2 != zenon_X93) % 0.54/0.77 (T_31 != zenon_X68) % 0.54/0.77 (-. (hollywood_placename zenon_X26 zenon_X94)) % 0.54/0.77 (T_5 != zenon_X95) % 0.54/0.77 (-. (relation zenon_X63 T_5)) % 0.54/0.77 (-. (relname zenon_X23 zenon_X2)) % 0.54/0.77 (object zenon_X96 T_31) % 0.54/0.77 (T_16 != zenon_X33) % 0.54/0.77 (relation T_16 T_5) % 0.54/0.77 (zenon_X33 != zenon_X47) % 0.54/0.77 (entity zenon_X97 T_32) % 0.54/0.77 (vehicle zenon_X98 T_32) % 0.54/0.77 (-. (placename T_16 zenon_X6)) % 0.54/0.77 (zenon_X2 != zenon_X85) % 0.54/0.77 (zenon_X2 != zenon_X99) % 0.54/0.77 (relname zenon_X0 T_5) % 0.54/0.77 (-. (specific zenon_X22 T_5)) % 0.54/0.77 (-. (placename T_16 zenon_X12)) % 0.54/0.77 (-. (eventuality zenon_X25 zenon_X100)) % 0.54/0.77 (T_31 != zenon_X101) % 0.54/0.77 (T_16 != zenon_X26) % 0.54/0.77 (T_31 != zenon_X36) % 0.54/0.77 (T_5 != zenon_X102) % 0.54/0.77 (thing zenon_X22 zenon_X2) % 0.54/0.77 (T_5 != zenon_X103) % 0.54/0.77 (T_32 != zenon_X77) % 0.54/0.77 (T_5 != zenon_X104) % 0.54/0.77 (zenon_X2 != zenon_X105) % 0.54/0.77 (general zenon_X33 T_5) % 0.54/0.77 (chevy T_16 T_32) % 0.54/0.77 (T_1 != zenon_X106) % 0.54/0.77 (-. (relation zenon_X18 zenon_X6)) % 0.54/0.77 (zenon_X0 != zenon_X26) % 0.54/0.77 (-. (abstraction zenon_X22 zenon_X107)) % 0.54/0.77 (T_5 = zenon_X2) % 0.54/0.77 (-. (relation zenon_X14 zenon_X2)) % 0.54/0.77 (T_32 != zenon_X108) % 0.54/0.77 (unisex T_16 zenon_X2) % 0.54/0.77 (T_16 != zenon_X13) % 0.54/0.77 (-. (abstraction T_16 zenon_X95)) % 0.54/0.77 (singleton zenon_X14 T_32) % 0.54/0.77 (T_1 != zenon_X30) % 0.54/0.77 (T_5 != zenon_X49) % 0.54/0.77 (T_7 != zenon_X89) % 0.54/0.77 (T_31 != zenon_X9) % 0.54/0.77 (-. (placename T_16 zenon_X56)) % 0.54/0.77 (T_7 != zenon_X69) % 0.54/0.77 (specific zenon_X109 T_32) % 0.54/0.77 (T_1 != zenon_X110) % 0.54/0.77 (nonhuman zenon_X22 T_5) % 0.54/0.77 (-. (thing zenon_X26 zenon_X44)) % 0.54/0.77 (T_1 != zenon_X111) % 0.54/0.77 (-. (barrel zenon_X13 zenon_X112)) % 0.54/0.77 (T_1 != zenon_X100) % 0.54/0.77 (-. (relname zenon_X18 zenon_X113)) % 0.54/0.77 (nonexistent zenon_X25 T_1) % 0.54/0.77 (T_5 != zenon_X114) % 0.54/0.77 (zenon_X2 != zenon_X115) % 0.54/0.77 (singleton zenon_X26 T_1) % 0.54/0.77 (-. (hollywood_placename zenon_X19 zenon_X116)) % 0.54/0.77 (-. (hollywood_placename zenon_X47 zenon_X117)) % 0.54/0.77 (singleton zenon_X23 T_32) % 0.54/0.77 (-. (relname zenon_X0 zenon_X99)) % 0.54/0.77 (of T_16 T_5 T_7) % 0.54/0.77 (T_5 != zenon_X86) % 0.54/0.77 (zenon_X22 != zenon_X47) % 0.54/0.77 (-. (location zenon_X118 zenon_X52)) % 0.54/0.77 (-. (relname zenon_X23 zenon_X3)) % 0.54/0.77 (-. (specific zenon_X14 T_5)) % 0.54/0.77 (T_5 != zenon_X88) % 0.54/0.77 (-. (placename zenon_X23 zenon_X119)) % 0.54/0.77 (-. (hollywood_placename zenon_X23 zenon_X120)) % 0.54/0.77 (T_32 != zenon_X42) % 0.54/0.77 (T_31 != zenon_X41) % 0.54/0.77 (zenon_X2 != zenon_X59) % 0.54/0.77 (T_7 != zenon_X51) % 0.54/0.77 (T_5 != zenon_X121) % 0.54/0.77 (T_5 != zenon_X64) % 0.54/0.77 (zenon_X2 != zenon_X35) % 0.54/0.77 (singleton zenon_X23 T_5) % 0.54/0.77 (object zenon_X96 T_32) % 0.54/0.77 (-. (event zenon_X13 zenon_X122)) % 0.54/0.77 (present T_16 T_1) % 0.54/0.77 (specific zenon_X109 T_31) % 0.54/0.77 (-. (placename T_16 zenon_X123)) % 0.54/0.77 (singleton T_16 T_7) % 0.54/0.77 (zenon_X33 != zenon_X63) % 0.54/0.77 (-. (placename T_16 zenon_X115)) % 0.54/0.77 (-. (placename T_16 zenon_X124)) % 0.54/0.77 (-. (abstraction zenon_X18 zenon_X125)) % 0.54/0.77 (T_31 != zenon_X2) % 0.54/0.77 (T_5 != zenon_X37) % 0.54/0.77 (specific zenon_X109 T_7) % 0.54/0.77 (entity zenon_X97 T_7) % 0.54/0.77 (zenon_X0 != zenon_X22) % 0.54/0.77 (zenon_X0 != zenon_X14) % 0.54/0.77 (-. (nonexistent zenon_X25 zenon_X92)) % 0.54/0.77 (zenon_X2 != zenon_X42) % 0.54/0.77 (zenon_X33 != zenon_X14) % 0.54/0.77 (zenon_X2 != zenon_X126) % 0.54/0.77 (T_32 != zenon_X101) % 0.54/0.77 (-. (placename T_16 zenon_X3)) % 0.54/0.77 (zenon_X2 != zenon_X74) % 0.54/0.77 (-. (placename zenon_X63 zenon_X127)) % 0.54/0.77 (zenon_X22 != zenon_X14) % 0.54/0.77 (-. (placename T_16 zenon_X126)) % 0.54/0.77 (T_7 != zenon_X36) % 0.54/0.77 (-. (placename T_16 zenon_X107)) % 0.54/0.77 (relation zenon_X33 T_5) % 0.54/0.77 (T_5 != zenon_X36) % 0.54/0.77 (general T_16 T_5) % 0.54/0.77 (abstraction zenon_X22 T_5) % 0.54/0.77 (T_1 != zenon_X77) % 0.54/0.77 (-. (placename T_16 zenon_X128)) % 0.54/0.77 (T_5 != zenon_X42) % 0.54/0.77 (zenon_X2 != zenon_X84) % 0.54/0.77 (abstraction zenon_X0 zenon_X2) % 0.54/0.77 (-. (specific zenon_X22 zenon_X2)) % 0.54/0.77 (barrel T_16 T_1) % 0.54/0.77 (-. (placename zenon_X0 zenon_X129)) % 0.54/0.77 (nonhuman zenon_X14 T_5) % 0.54/0.77 (zenon_X2 != zenon_X39) % 0.54/0.77 (-. (relname T_16 zenon_X121)) % 0.54/0.77 (-. (relation zenon_X19 zenon_X2)) % 0.54/0.77 (agent T_16 T_1 T_32) % 0.54/0.77 (relname zenon_X33 T_5) % 0.54/0.77 (unisex T_16 T_5) % 0.54/0.77 (-. (placename T_16 zenon_X105)) % 0.54/0.77 (-. (street zenon_X73 zenon_X130)) % 0.54/0.77 (zenon_X22 != zenon_X19) % 0.54/0.77 (nonliving zenon_X131 T_7) % 0.54/0.77 (-. (general zenon_X18 zenon_X45)) % 0.54/0.77 (lonely T_16 T_31) % 0.54/0.77 (-. (specific T_16 zenon_X2)) % 0.54/0.77 (-. (abstraction zenon_X23 zenon_X2)) % 0.54/0.77 (nonhuman zenon_X47 T_5) % 0.54/0.77 (-. (city zenon_X67 zenon_X132)) % 0.54/0.77 (-. (relname zenon_X19 zenon_X2)) % 0.54/0.77 (T_31 != zenon_X133) % 0.54/0.77 (T_7 != zenon_X77) % 0.54/0.77 (-. (existent zenon_X25 T_1)) % 0.54/0.77 (abstraction zenon_X22 zenon_X2) % 0.54/0.77 (-. (placename T_16 zenon_X103)) % 0.54/0.77 (zenon_X0 != zenon_X18) % 0.54/0.77 (T_32 != zenon_X9) % 0.54/0.77 (T_5 != zenon_X93) % 0.54/0.77 (T_1 != zenon_X122) % 0.54/0.77 (-. (abstraction T_16 zenon_X35)) % 0.54/0.77 (T_1 != zenon_X134) % 0.54/0.77 (-. (abstraction zenon_X14 zenon_X105)) % 0.54/0.77 (T_5 != zenon_X107) % 0.54/0.77 (thing zenon_X22 T_5) % 0.54/0.77 (zenon_X2 != zenon_X103) % 0.54/0.77 (-. (instrumentality zenon_X135 zenon_X62)) % 0.54/0.77 (-. (abstraction zenon_X0 zenon_X34)) % 0.54/0.77 (-. (object zenon_X97 zenon_X20)) % 0.54/0.77 (nonliving zenon_X131 T_31) % 0.54/0.77 (T_32 != zenon_X133) % 0.54/0.77 (zenon_X2 != zenon_X77) % 0.54/0.77 (thing zenon_X0 T_5) % 0.54/0.77 (transport zenon_X136 T_32) % 0.54/0.77 (T_16 != zenon_X19) % 0.54/0.77 (zenon_X60 != zenon_X13) % 0.54/0.77 (T_7 != zenon_X41) % 0.54/0.77 (thing zenon_X137 T_1) % 0.54/0.77 (zenon_X2 != zenon_X128) % 0.54/0.77 (-. (placename T_16 zenon_X74)) % 0.54/0.77 (zenon_X2 != zenon_X102) % 0.54/0.77 (thing zenon_X33 T_5) % 0.54/0.77 (object zenon_X118 T_7) % 0.54/0.77 (-. (abstraction zenon_X14 zenon_X126)) % 0.54/0.77 (-. (placename T_16 zenon_X68)) % 0.54/0.77 (T_16 != zenon_X18) % 0.54/0.77 (unisex zenon_X22 zenon_X2) % 0.54/0.77 (-. (chevy zenon_X138 zenon_X139)) % 0.54/0.77 (zenon_X2 != zenon_X123) % 0.54/0.77 (-. (existent zenon_X29 T_1)) % 0.54/0.77 (-. (thing zenon_X14 zenon_X68)) % 0.54/0.77 (zenon_X2 != zenon_X121) % 0.54/0.77 (T_5 != zenon_X17) % 0.54/0.77 (T_31 != zenon_X130) % 0.54/0.77 (-. (relation zenon_X23 zenon_X140)) % 0.54/0.77 (-. (nonexistent zenon_X29 zenon_X141)) % 0.54/0.77 (T_5 != zenon_X72) % 0.54/0.77 (zenon_X2 != zenon_X81) % 0.54/0.77 (-. (placename T_16 zenon_X102)) % 0.54/0.77 (T_7 != zenon_X2) % 0.54/0.77 (-. (relation zenon_X26 zenon_X2)) % 0.54/0.77 (singleton zenon_X33 T_32) % 0.54/0.77 (abstraction zenon_X14 T_5) % 0.54/0.77 (zenon_X22 != zenon_X63) % 0.54/0.77 (-. (placename T_16 T_32)) % 0.54/0.77 (general zenon_X14 zenon_X2) % 0.54/0.77 (-. (abstraction zenon_X47 zenon_X88)) % 0.54/0.77 (zenon_X2 != zenon_X95) % 0.54/0.77 (zenon_X2 != zenon_X10) % 0.54/0.77 (unisex zenon_X22 T_5) % 0.54/0.77 (T_1 != zenon_X141) % 0.54/0.77 (-. (abstraction zenon_X0 zenon_X64)) % 0.54/0.77 (-. (placename T_16 zenon_X142)) % 0.54/0.77 (T_5 != zenon_X128) % 0.54/0.77 (unisex zenon_X90 T_31) % 0.54/0.77 (-. (thing zenon_X23 zenon_X77)) % 0.54/0.77 (zenon_X33 != zenon_X22) % 0.54/0.77 (relation T_16 zenon_X2) % 0.54/0.77 (-. (car zenon_X98 zenon_X143)) % 0.54/0.77 (artifact zenon_X135 T_32) % 0.54/0.77 (-. (relation zenon_X63 zenon_X115)) % 0.54/0.77 (general T_16 zenon_X2) % 0.54/0.77 (T_1 != zenon_X144) % 0.54/0.77 (-. (hollywood_placename zenon_X14 zenon_X145)) % 0.54/0.77 (zenon_X0 != zenon_X19) % 0.54/0.77 (-. (object zenon_X90 zenon_X69)) % 0.54/0.77 (-. (placename T_16 zenon_X99)) % 0.54/0.77 (T_5 != zenon_X105) % 0.54/0.77 (-. (placename T_16 zenon_X86)) % 0.54/0.77 (zenon_X0 != zenon_X47) % 0.54/0.77 (thing zenon_X40 T_7) % 0.54/0.77 (T_5 != zenon_X12) % 0.54/0.77 (zenon_X2 != zenon_X129) % 0.54/0.77 (-. (placename T_16 zenon_X28)) % 0.54/0.77 (-. (hollywood_placename zenon_X33 zenon_X128)) % 0.54/0.77 (placename zenon_X33 T_5) % 0.54/0.77 (singleton zenon_X22 T_31) % 0.54/0.77 (relname T_16 zenon_X2) % 0.54/0.77 (-. (relation zenon_X26 T_5)) % 0.54/0.77 (-. (placename zenon_X22 zenon_X146)) % 0.54/0.77 (T_16 != zenon_X47) % 0.54/0.77 (T_5 != zenon_X124) % 0.54/0.77 (-. (placename zenon_X19 zenon_X147)) % 0.54/0.77 (-. (relation zenon_X23 T_5)) % 0.54/0.77 (-. (relation zenon_X22 zenon_X72)) % 0.54/0.77 (T_1 != zenon_X36) % 0.54/0.77 (T_5 != zenon_X54) % 0.54/0.77 (-. (artifact zenon_X96 zenon_X101)) % 0.54/0.77 (-. (placename T_16 zenon_X78)) % 0.54/0.77 (-. (nonexistent zenon_X60 zenon_X134)) % 0.54/0.77 (T_31 != T_5) % 0.54/0.77 (-. (abstraction zenon_X22 zenon_X78)) % 0.54/0.77 (relname zenon_X33 zenon_X2) % 0.54/0.77 (-. (placename T_16 zenon_X140)) % 0.54/0.77 (-. (abstraction T_16 zenon_X49)) % 0.54/0.77 (-. (placename T_16 zenon_X34)) % 0.54/0.77 (-. (placename T_16 zenon_X4)) % 0.54/0.77 (T_16 != zenon_X14) % 0.54/0.77 (-. (specific zenon_X14 zenon_X2)) % 0.54/0.77 (nonhuman zenon_X33 T_5) % 0.54/0.77 (T_1 != T_5) % 0.54/0.77 (singleton zenon_X23 zenon_X2) % 0.54/0.77 (T_7 != zenon_X71) % 0.54/0.77 (nonliving zenon_X131 T_32) % 0.54/0.77 (T_5 != zenon_X148) % 0.54/0.77 (-. (relname zenon_X23 T_5)) % 0.54/0.77 (-. (thing zenon_X22 zenon_X42)) % 0.54/0.77 (-. (entity zenon_X40 zenon_X133)) % 0.54/0.77 (T_5 != zenon_X84) % 0.54/0.77 (nonhuman zenon_X22 zenon_X2) % 0.54/0.77 (singleton zenon_X0 T_32) % 0.54/0.77 (instrumentality zenon_X149 T_32) % 0.54/0.77 (-. (placename T_16 zenon_X83)) % 0.54/0.77 (impartial zenon_X150 T_7) % 0.54/0.77 (relation zenon_X0 T_5) % 0.54/0.77 (T_31 != zenon_X80) % 0.54/0.77 (-. (eventuality zenon_X13 T_1)) % 0.54/0.77 (singleton T_16 T_1) % 0.54/0.77 (-. (abstraction zenon_X33 zenon_X124)) % 0.54/0.77 (-. (placename zenon_X33 zenon_X85)) % 0.54/0.77 (zenon_X33 != zenon_X23) % 0.54/0.77 (singleton zenon_X0 zenon_X2) % 0.54/0.77 (singleton zenon_X26 T_31) % 0.54/0.77 (T_32 != zenon_X89) % 0.54/0.77 (abstraction zenon_X33 zenon_X2) % 0.54/0.77 (T_1 != zenon_X61) % 0.54/0.77 (unisex zenon_X14 T_5) % 0.54/0.77 (-. (placename T_16 zenon_X129)) % 0.54/0.77 (singleton zenon_X22 zenon_X2) % 0.54/0.77 (-. (placename T_16 zenon_X121)) % 0.54/0.77 (zenon_X14 != zenon_X18) % 0.54/0.77 (city T_16 T_7) % 0.54/0.77 (nonhuman T_16 T_5) % 0.54/0.77 (zenon_X2 != zenon_X4) % 0.54/0.77 (-. (abstraction zenon_X63 zenon_X43)) % 0.54/0.77 (singleton zenon_X22 T_7) % 0.54/0.77 (-. (placename T_16 zenon_X57)) % 0.54/0.77 (placename T_16 T_5) % 0.54/0.77 (existent zenon_X58 T_7) % 0.54/0.77 (-. (abstraction zenon_X63 zenon_X2)) % 0.54/0.77 (-. (general zenon_X22 zenon_X93)) % 0.54/0.77 (unisex zenon_X33 zenon_X2) % 0.54/0.77 (-. (placename T_16 zenon_X50)) % 0.54/0.77 (-. (placename T_16 zenon_X37)) % 0.54/0.77 (T_1 != zenon_X68) % 0.54/0.77 (unisex zenon_X151 T_1) % 0.54/0.77 (-. (relname zenon_X19 T_5)) % 0.54/0.77 (zenon_X2 != zenon_X125) % 0.54/0.77 (-. (of zenon_X75 zenon_X152 T_7)) % 0.54/0.77 (zenon_X2 != zenon_X124) % 0.54/0.77 (zenon_X2 != zenon_X140) % 0.54/0.77 (impartial zenon_X150 T_32) % 0.54/0.77 (nonhuman zenon_X0 T_5) % 0.54/0.77 (singleton T_16 zenon_X2) % 0.54/0.77 (singleton zenon_X26 T_7) % 0.54/0.77 (zenon_X2 != zenon_X86) % 0.54/0.77 (zenon_X2 != zenon_X88) % 0.54/0.77 (specific zenon_X153 T_1) % 0.54/0.77 (-. (relation zenon_X63 zenon_X2)) % 0.54/0.77 (T_5 != zenon_X129) % 0.54/0.77 (impartial zenon_X150 T_31) % 0.54/0.77 (-. (placename T_16 zenon_X72)) % 0.54/0.77 (-. (abstraction zenon_X14 zenon_X57)) % 0.54/0.77 (-. (relname zenon_X47 T_5)) % 0.54/0.77 (-. (of zenon_X75 zenon_X154 zenon_X91)) % 0.54/0.77 (general zenon_X14 T_5) % 0.54/0.77 (T_5 != zenon_X123) % 0.54/0.77 (zenon_X2 != zenon_X27) % 0.54/0.77 (zenon_X2 != zenon_X6) % 0.54/0.77 (-. (placename T_16 zenon_X77)) % 0.54/0.77 (T_32 != zenon_X12) % 0.54/0.77 (-. (abstraction zenon_X26 zenon_X155)) % 0.54/0.77 (zenon_X14 != zenon_X63) % 0.54/0.77 (singleton T_16 T_32) % 0.54/0.77 (singleton zenon_X14 T_31) % 0.54/0.77 (-. (object zenon_X131 zenon_X41)) % 0.54/0.77 (T_5 != zenon_X85) % 0.54/0.77 (-. (hollywood_placename zenon_X0 zenon_X156)) % 0.54/0.77 (-. (hollywood_placename zenon_X33 zenon_X2)) % 0.54/0.77 (T_5 != zenon_X28) % 0.54/0.77 (-. (relation T_16 zenon_X27)) % 0.54/0.77 (T_31 != zenon_X8) % 0.54/0.77 (-. (relation zenon_X26 zenon_X38)) % 0.54/0.77 (T_5 != zenon_X99) % 0.54/0.77 (singleton zenon_X26 T_32) % 0.54/0.77 (-. (entity zenon_X109 zenon_X8)) % 0.54/0.77 (-. (placename T_16 zenon_X10)) % 0.54/0.77 (artifact zenon_X79 T_31) % 0.54/0.77 (-. (specific zenon_X19 zenon_X2)) % 0.54/0.77 (-. (abstraction zenon_X0 zenon_X17)) % 0.54/0.77 (-. (abstraction zenon_X22 zenon_X59)) % 0.54/0.77 (T_32 != zenon_X139) % 0.54/0.77 (T_7 != zenon_X133) % 0.54/0.77 (-. (eventuality zenon_X153 zenon_X111)) % 0.54/0.77 (entity zenon_X97 T_31) % 0.54/0.77 (-. (abstraction zenon_X18 T_5)) % 0.54/0.77 (relation zenon_X0 zenon_X2) % 0.54/0.77 (zenon_X2 != zenon_X28) % 0.54/0.77 (-. (abstraction zenon_X23 zenon_X103)) % 0.54/0.77 (singleton zenon_X22 T_1) % 0.54/0.77 (zenon_X33 != zenon_X26) % 0.54/0.77 (-. (specific zenon_X19 T_5)) % 0.54/0.77 (-. (general zenon_X18 T_5)) % 0.54/0.77 (abstraction zenon_X0 T_5) % 0.54/0.77 (abstraction T_16 zenon_X2) % 0.54/0.77 (zenon_X33 != zenon_X18) % 0.54/0.77 (-. (relname zenon_X47 zenon_X24)) % 0.54/0.77 (zenon_X33 != zenon_X19) % 0.54/0.77 (-. (existent zenon_X60 T_1)) % 0.54/0.77 (T_5 != zenon_X126) % 0.54/0.77 (singleton zenon_X23 T_1) % 0.54/0.77 (zenon_X29 != zenon_X13) % 0.54/0.77 (-. (specific zenon_X0 T_5)) % 0.54/0.77 (-. (relname zenon_X63 zenon_X157)) % 0.54/0.77 (-. (specific T_16 T_5)) % 0.54/0.77 (singleton zenon_X26 T_5) % 0.54/0.77 (-. (placename zenon_X18 zenon_X158)) % 0.54/0.77 (T_5 != zenon_X87) % 0.54/0.77 (-. (abstraction zenon_X33 zenon_X142)) % 0.54/0.77 (-. (relname zenon_X26 zenon_X159)) % 0.54/0.77 (hollywood_placename T_16 T_5) % 0.54/0.77 (-. (abstraction zenon_X19 zenon_X2)) % 0.54/0.77 (singleton zenon_X23 T_7) % 0.54/0.77 (zenon_X14 != zenon_X47) % 0.54/0.77 (-. (vehicle zenon_X136 zenon_X76)) % 0.54/0.77 (-. (nonexistent T_16 zenon_X160)) % 0.54/0.77 (zenon_X2 != zenon_X87) % 0.54/0.77 (-. (abstraction zenon_X22 zenon_X102)) % 0.54/0.77 (general zenon_X33 zenon_X2) % 0.54/0.77 (thing zenon_X33 zenon_X2) % 0.54/0.77 (-. (thing T_16 zenon_X9)) % 0.54/0.77 (nonhuman T_16 zenon_X2) % 0.54/0.77 (event zenon_X29 T_1) % 0.54/0.77 (relname T_16 T_5) % 0.54/0.77 (singleton zenon_X14 T_5) % 0.54/0.77 (-. (thing zenon_X33 zenon_X12)) % 0.54/0.77 (T_7 != zenon_X68) % 0.54/0.77 (zenon_X2 != zenon_X68) % 0.54/0.77 (-. (nonexistent zenon_X13 zenon_X106)) % 0.54/0.77 (singleton T_16 T_5) % 0.54/0.77 (singleton zenon_X14 T_7) % 0.54/0.77 (unisex zenon_X0 T_5) % 0.54/0.77 (general zenon_X22 T_5) % 0.54/0.77 (zenon_X2 != zenon_X142) % 0.54/0.77 (-. (of T_16 zenon_X114 T_7)) % 0.54/0.77 (-. (object zenon_X150 zenon_X51)) % 0.54/0.77 (-. (placename T_16 zenon_X87)) % 0.54/0.77 (singleton zenon_X33 T_5) % 0.54/0.77 (general zenon_X22 zenon_X2) % 0.54/0.77 (T_5 != zenon_X56) % 0.54/0.77 (T_5 != zenon_X125) % 0.54/0.77 (T_1 != zenon_X44) % 0.54/0.77 (T_32 != zenon_X69) % 0.54/0.77 (street T_16 T_31) % 0.54/0.77 (zenon_X2 != zenon_X104) % 0.54/0.77 (zenon_X22 != zenon_X18) % 0.54/0.77 (abstraction zenon_X33 T_5) % 0.54/0.77 (T_7 != zenon_X132) % 0.54/0.77 (-. (placename T_16 zenon_X148)) % 0.54/0.77 (-. (relation zenon_X19 T_5)) % 0.54/0.77 (T_7 != zenon_X42) % 0.54/0.77 (T_1 != zenon_X160) % 0.54/0.77 (zenon_X0 != zenon_X23) % 0.54/0.77 (-. (abstraction zenon_X19 zenon_X39)) % 0.54/0.77 (T_5 != zenon_X53) % 0.54/0.77 (-. (abstraction zenon_X33 zenon_X37)) % 0.54/0.77 (thing T_16 zenon_X2) % 0.54/0.77 (dirty T_16 T_32) % 0.54/0.77 (-. (relation zenon_X18 zenon_X2)) % 0.54/0.77 (unisex zenon_X63 T_5) % 0.54/0.77 (thing zenon_X14 zenon_X2) % 0.54/0.77 (zenon_X2 != zenon_X148) % 0.54/0.77 (T_32 != zenon_X51) % 0.54/0.77 (car zenon_X138 T_32) % 0.54/0.77 (event T_16 T_1) % 0.54/0.77 (T_5 != zenon_X142) % 0.54/0.77 (old T_16 T_32) % 0.54/0.77 (-. (placename T_16 zenon_X44)) % 0.54/0.77 (T_5 != zenon_X35) % 0.54/0.77 (-. (relname zenon_X47 zenon_X2)) % 0.54/0.77 (-. (relation zenon_X18 T_5)) % 0.54/0.77 (zenon_X19 != zenon_X18) % 0.54/0.77 (zenon_X2 != zenon_X114) % 0.54/0.77 (T_5 != zenon_X140) % 0.54/0.77 (nonhuman zenon_X0 zenon_X2) % 0.54/0.77 (zenon_X2 != zenon_X107) % 0.54/0.77 (-. (hollywood_placename T_16 zenon_X148)) % 0.54/0.77 (T_31 != zenon_X12) % 0.54/0.77 (unisex zenon_X90 T_7) % 0.54/0.77 (-. (abstraction zenon_X18 zenon_X2)) % 0.54/0.77 (unisex zenon_X14 zenon_X2) % 0.54/0.77 (-. (placename T_16 zenon_X27)) % 0.54/0.77 (T_5 != zenon_X115) % 0.54/0.77 (thing zenon_X0 zenon_X2) % 0.54/0.77 (T_16 != zenon_X63) % 0.54/0.77 (-. (hollywood_placename zenon_X63 zenon_X161)) % 0.54/0.77 (existent zenon_X58 T_31) % 0.54/0.77 (down T_16 T_1 T_31) % 0.54/0.77 (T_31 != zenon_X89) % 0.54/0.77 (T_31 != zenon_X77) % 0.54/0.77 (singleton zenon_X33 T_31) % 0.54/0.77 (-. (eventuality zenon_X137 zenon_X55)) % 0.54/0.77 (-. (placename T_16 zenon_X84)) % 0.54/0.77 (T_32 != zenon_X143) % 0.54/0.77 (-. (general zenon_X33 zenon_X81)) % 0.54/0.77 (-. (placename T_16 zenon_X95)) % 0.54/0.77 (eventuality zenon_X60 T_1) % 0.54/0.77 (-. (relation zenon_X47 zenon_X162)) % 0.54/0.77 (zenon_X33 != zenon_X0) % 0.54/0.77 (T_31 != zenon_X42) % 0.54/0.77 (T_5 != zenon_X83) % 0.54/0.77 (-. (placename T_16 zenon_X36)) % 0.54/0.77 (-. (transport zenon_X149 zenon_X108)) % 0.54/0.77 (-. (abstraction zenon_X47 zenon_X2)) % 0.54/0.77 (T_31 != zenon_X44) % 0.54/0.77 (-. (placename T_16 zenon_X93)) % 0.54/0.77 (singleton zenon_X0 T_5) % 0.54/0.77 (T_31 != T_1) % 0.54/0.77 (-. (relname zenon_X22 zenon_X123)) % 0.54/0.77 (-. (placename T_16 zenon_X104)) % 0.54/0.77 (-. (thing zenon_X26 zenon_X2)) % 0.54/0.77 (-. (placename T_16 zenon_X64)) % 0.54/0.77 (-. (relation zenon_X33 zenon_X104)) % 0.54/0.77 (zenon_X2 != zenon_X21) % 0.54/0.77 (-. (relname zenon_X19 zenon_X10)) % 0.54/0.77 (singleton T_16 T_31) % 0.54/0.77 (-. (abstraction zenon_X14 zenon_X50)) % 0.54/0.77 (thing zenon_X14 T_5) % 0.54/0.77 (nonhuman zenon_X14 zenon_X2) % 0.54/0.77 (T_32 != zenon_X44) % 0.54/0.77 (zenon_X2 != zenon_X53) % 0.54/0.77 (-. (placename T_16 zenon_X125)) % 0.54/0.77 (-. (eventuality zenon_X151 zenon_X144)) % 0.54/0.77 (-. (event zenon_X13 T_1)) % 0.54/0.77 (general zenon_X0 T_5) % 0.54/0.77 (-. (eventuality zenon_X13 zenon_X110)) % 0.54/0.77 (in T_16 T_1 T_7) % 0.54/0.77 (zenon_X2 != zenon_X9) % 0.54/0.77 (zenon_X2 != zenon_X83) % 0.54/0.77 *) % 0.54/0.77 (* NO-PROOF *) % 0.54/0.77 % SZS status GaveUp % 0.54/0.77 nodes searched: 5198 % 0.54/0.77 max branch formulas: 1224 % 0.54/0.77 proof nodes created: 713 % 0.54/0.77 formulas created: 18333 % 0.54/0.77 %------------------------------------------------------------------------------