%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : NLP167+1 : TPTP v8.2.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : run_zenon_modulo %d %s % Computer : n014.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:30 EDT 2024 % Result : Unknown 0.39s 0.57s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : NLP167+1 : TPTP v8.2.0. Released v2.4.0. % 0.06/0.12 % Command : run_zenon_modulo %d %s % 0.11/0.33 % Computer : n014.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 : 300 % 0.11/0.33 % DateTime : Sat Jun 22 22:35:54 EDT 2024 % 0.11/0.34 % CPUTime : % 0.39/0.56 Zenon error: exhausted search space without finding a proof % 0.39/0.56 (* Current branch: % 0.39/0.56 (-. (cheap Tau_0 Tau_63)) % 0.39/0.56 (-. (two Tau_0 Tau_1)) % 0.39/0.56 (-. (barrel Tau_0 zenon_X80)) % 0.39/0.56 (zenon_X86 != Tau_8) % 0.39/0.56 (-. (group Tau_0 zenon_X88)) % 0.39/0.56 (member Tau_0 Tau_110 zenon_X109) % 0.39/0.56 (actual_world Tau_0) % 0.39/0.56 (zenon_X82 != Tau_7) % 0.39/0.56 (-. (cheap Tau_0 Tau_110)) % 0.39/0.56 (zenon_X49 != Tau_7) % 0.39/0.56 (chevy Tau_0 Tau_4) % 0.39/0.56 (Tau_3 != zenon_X37) % 0.39/0.56 (Tau_2 != Tau_4) % 0.39/0.56 (member Tau_0 Tau_96 zenon_X95) % 0.39/0.56 (young Tau_0 Tau_36) % 0.39/0.56 (-. (lonely Tau_0 zenon_X75)) % 0.39/0.56 (zenon_X49 != Tau_8) % 0.39/0.56 (zenon_X78 != Tau_8) % 0.39/0.56 (Tau_4 != zenon_X91) % 0.39/0.56 (zenon_X97 != Tau_7) % 0.39/0.56 (city Tau_0 Tau_2) % 0.39/0.56 (member Tau_0 Tau_113 zenon_X112) % 0.39/0.56 (state Tau_0 Tau_10) % 0.39/0.56 (group Tau_0 Tau_1) % 0.39/0.56 (present Tau_0 Tau_6) % 0.39/0.56 (-. (lonely Tau_0 zenon_X99)) % 0.39/0.56 (zenon_X89 != Tau_7) % 0.39/0.56 (zenon_X68 != Tau_8) % 0.39/0.56 (zenon_X95 != Tau_8) % 0.39/0.56 (zenon_X109 != Tau_8) % 0.39/0.56 (-. (cheap Tau_0 Tau_105)) % 0.39/0.56 (member Tau_0 Tau_83 zenon_X82) % 0.39/0.56 (zenon_X119 != Tau_8) % 0.39/0.56 (-. (cheap Tau_0 Tau_43)) % 0.39/0.56 (-. (cheap Tau_0 Tau_90)) % 0.39/0.56 (Tau_8 != zenon_X106) % 0.39/0.56 (zenon_X24 != Tau_7) % 0.39/0.56 (Tau_5 != zenon_X75) % 0.39/0.56 (-. (group Tau_0 zenon_X106)) % 0.39/0.56 (zenon_X86 != Tau_7) % 0.39/0.56 (member Tau_0 Tau_34 zenon_X33) % 0.39/0.56 (-. (cheap Tau_0 Tau_74)) % 0.39/0.56 (of Tau_0 Tau_3 Tau_2) % 0.39/0.56 (zenon_X102 != Tau_8) % 0.39/0.56 (Tau_4 != zenon_X64) % 0.39/0.56 (zenon_X68 != Tau_7) % 0.39/0.56 (in Tau_0 Tau_6 Tau_2) % 0.39/0.56 (-. (group Tau_0 zenon_X27)) % 0.39/0.56 (zenon_X42 != Tau_8) % 0.39/0.56 (in Tau_0 Tau_11 Tau_4) % 0.39/0.56 (group Tau_0 Tau_8) % 0.39/0.56 (member Tau_0 Tau_105 zenon_X104) % 0.39/0.56 (zenon_X62 != Tau_8) % 0.39/0.56 (Tau_8 != zenon_X88) % 0.39/0.56 (zenon_X89 != Tau_8) % 0.39/0.56 (down Tau_0 Tau_6 Tau_5) % 0.39/0.56 (Tau_8 != zenon_X27) % 0.39/0.56 (zenon_X73 != Tau_7) % 0.39/0.56 (-. (city Tau_0 Tau_4)) % 0.39/0.56 (-. (old Tau_0 zenon_X64)) % 0.39/0.56 (-. (member Tau_0 zenon_X16 Tau_8)) % 0.39/0.56 (member Tau_0 Tau_98 zenon_X97) % 0.39/0.56 (fellow Tau_0 Tau_36) % 0.39/0.56 (-. (cheap zenon_X17 Tau_35)) % 0.39/0.56 (Tau_6 != zenon_X80) % 0.39/0.56 (barrel Tau_0 Tau_6) % 0.39/0.56 (-. (cheap Tau_0 Tau_98)) % 0.39/0.56 (-. (barrel Tau_0 zenon_X114)) % 0.39/0.56 (-. (cheap Tau_0 Tau_87)) % 0.39/0.56 (zenon_X56 != Tau_8) % 0.39/0.56 (event Tau_0 Tau_6) % 0.39/0.56 (member Tau_0 Tau_120 zenon_X119) % 0.39/0.56 (member Tau_0 Tau_69 zenon_X68) % 0.39/0.56 (-. (cheap Tau_0 Tau_83)) % 0.39/0.56 (-. (cheap Tau_0 Tau_79)) % 0.39/0.56 (member Tau_0 Tau_74 zenon_X73) % 0.39/0.56 (Tau_7 != zenon_X106) % 0.39/0.56 (zenon_X107 != Tau_8) % 0.39/0.56 (zenon_X109 != Tau_7) % 0.39/0.56 (zenon_X24 != Tau_8) % 0.39/0.56 (Tau_7 != zenon_X27) % 0.39/0.56 (-. (cheap Tau_0 Tau_108)) % 0.39/0.56 (zenon_X82 != Tau_8) % 0.39/0.56 (patient Tau_0 Tau_15 zenon_X13) % 0.39/0.56 (Tau_3 != zenon_X44) % 0.39/0.56 (zenon_X33 != Tau_7) % 0.39/0.56 (Tau_6 != zenon_X84) % 0.39/0.56 (-. (old Tau_0 zenon_X58)) % 0.39/0.56 (zenon_X95 != Tau_7) % 0.39/0.56 (-. (cheap zenon_X17 Tau_25)) % 0.39/0.56 (Tau_3 != zenon_X51) % 0.39/0.56 (-. (cheap Tau_0 Tau_57)) % 0.39/0.56 (zenon_X97 != Tau_8) % 0.39/0.56 (-. (cheap Tau_0 Tau_103)) % 0.39/0.56 (-. (cheap Tau_0 Tau_34)) % 0.39/0.56 (member zenon_X17 Tau_26 Tau_7) % 0.39/0.56 (zenon_X42 != Tau_7) % 0.39/0.56 (member Tau_0 Tau_43 zenon_X42) % 0.39/0.56 (Tau_1 != zenon_X88) % 0.39/0.56 (-. (cheap Tau_0 Tau_50)) % 0.39/0.56 (hollywood_placename Tau_0 Tau_3) % 0.39/0.56 (zenon_X17 != Tau_0) % 0.39/0.56 (member Tau_0 Tau_90 zenon_X89) % 0.39/0.56 (dirty Tau_0 Tau_4) % 0.39/0.56 (-. (cheap zenon_X17 Tau_26)) % 0.39/0.56 (zenon_X102 != Tau_7) % 0.39/0.56 (event Tau_0 Tau_15) % 0.39/0.56 (Tau_5 != zenon_X99) % 0.39/0.56 (zenon_X62 != Tau_7) % 0.39/0.56 (Tau_36 != zenon_X12) % 0.39/0.56 (-. (cheap Tau_0 Tau_36)) % 0.39/0.56 (member Tau_0 Tau_57 zenon_X56) % 0.39/0.56 (-. (two Tau_0 Tau_8)) % 0.39/0.56 (Tau_7 != Tau_1) % 0.39/0.56 (member Tau_0 Tau_50 zenon_X49) % 0.39/0.56 (zenon_X78 != Tau_7) % 0.39/0.56 (-. (cheap Tau_0 Tau_69)) % 0.39/0.56 (member Tau_0 Tau_117 zenon_X116) % 0.39/0.56 (member Tau_0 Tau_36 Tau_7) % 0.39/0.56 (Tau_5 != zenon_X70) % 0.39/0.56 (-. (placename Tau_0 zenon_X44)) % 0.39/0.56 (-. (placename Tau_0 zenon_X37)) % 0.39/0.56 (street Tau_0 Tau_5) % 0.39/0.56 (Tau_4 != zenon_X58) % 0.39/0.56 (-. (placename Tau_0 zenon_X51)) % 0.39/0.56 (zenon_X56 != Tau_7) % 0.39/0.56 (zenon_X107 != Tau_7) % 0.39/0.56 (-. (cheap Tau_0 Tau_113)) % 0.39/0.56 (member Tau_0 Tau_103 zenon_X102) % 0.39/0.56 (-. (barrel Tau_0 zenon_X84)) % 0.39/0.56 (frontseat Tau_0 Tau_4) % 0.39/0.56 (zenon_X104 != Tau_7) % 0.39/0.56 (-. (cheap Tau_0 Tau_96)) % 0.39/0.56 (group Tau_0 Tau_7) % 0.39/0.56 (member zenon_X17 Tau_35 Tau_8) % 0.39/0.56 (zenon_X33 != Tau_8) % 0.39/0.56 (zenon_X112 != Tau_8) % 0.39/0.56 (zenon_X112 != Tau_7) % 0.39/0.56 (Tau_7 != zenon_X88) % 0.39/0.56 (placename Tau_0 Tau_3) % 0.39/0.56 (Tau_7 != Tau_8) % 0.39/0.56 (agent Tau_0 Tau_6 Tau_4) % 0.39/0.56 (-. (cheap Tau_0 Tau_120)) % 0.39/0.56 (zenon_X104 != Tau_8) % 0.39/0.56 (zenon_X116 != Tau_7) % 0.39/0.56 (Tau_1 != zenon_X106) % 0.39/0.56 (member zenon_X17 Tau_25 zenon_X24) % 0.39/0.56 (member Tau_0 Tau_63 zenon_X62) % 0.39/0.56 (zenon_X73 != Tau_8) % 0.39/0.56 (white Tau_0 Tau_4) % 0.39/0.56 (present Tau_0 Tau_15) % 0.39/0.56 (agent Tau_0 Tau_15 zenon_X14) % 0.39/0.56 (-. (lonely Tau_0 zenon_X70)) % 0.39/0.56 (be Tau_0 Tau_10 zenon_X9 Tau_11) % 0.39/0.56 (Tau_1 != zenon_X27) % 0.39/0.56 (-. (cheap Tau_0 Tau_117)) % 0.39/0.56 (Tau_6 != zenon_X114) % 0.39/0.56 (wear Tau_0 Tau_15) % 0.39/0.56 (member Tau_0 Tau_79 zenon_X78) % 0.39/0.56 (old Tau_0 Tau_4) % 0.39/0.56 (lonely Tau_0 Tau_5) % 0.39/0.56 (zenon_X116 != Tau_8) % 0.39/0.56 (zenon_X119 != Tau_7) % 0.39/0.57 (member Tau_0 Tau_108 zenon_X107) % 0.39/0.57 (nonreflexive Tau_0 Tau_15) % 0.39/0.57 (-. (old Tau_0 zenon_X91)) % 0.39/0.57 (two Tau_0 Tau_7) % 0.39/0.57 (-. (member Tau_0 zenon_X12 Tau_7)) % 0.39/0.57 (member Tau_0 Tau_87 zenon_X86) % 0.39/0.57 *) % 0.39/0.57 (* NO-PROOF *) % 0.39/0.57 % SZS status GaveUp % 0.39/0.57 Number of rewrites on terms: 0 % 0.39/0.57 Number of rewrites on props: 0 % 0.39/0.57 nodes searched: 493 % 0.39/0.57 max branch formulas: 420 % 0.39/0.57 proof nodes created: 39 % 0.39/0.57 formulas created: 6879 % 0.39/0.57 %------------------------------------------------------------------------------