↑ Up

ZenonModulo---0.5.0.UNK-Non.f

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : ZenonModulo---0.5.0
% Problem  : NLP163+1 : TPTP v8.2.0. Released v2.4.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_zenon_modulo %d %s

% Computer : n016.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:29 EDT 2024

% Result   : Unknown 0.38s 0.62s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.13  % Problem  : NLP163+1 : TPTP v8.2.0. Released v2.4.0.
% 0.08/0.13  % Command  : run_zenon_modulo %d %s
% 0.13/0.34  % Computer : n016.cluster.edu
% 0.13/0.34  % Model    : x86_64 x86_64
% 0.13/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34  % Memory   : 8042.1875MB
% 0.13/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34  % CPULimit : 300
% 0.13/0.34  % WCLimit  : 300
% 0.13/0.34  % DateTime : Sun Jun 23 00:17:54 EDT 2024
% 0.13/0.35  % CPUTime  : 
% 0.38/0.62  Zenon error: exhausted search space without finding a proof
% 0.38/0.62  (* Current branch:
% 0.38/0.62  (member Tau_84 Tau_212 zenon_X211)
% 0.38/0.62  (-. (cheap Tau_84 Tau_212))
% 0.38/0.62  (Tau_89 != zenon_X199)
% 0.38/0.62  (-. (cheap Tau_84 Tau_225))
% 0.38/0.62  (Tau_90 != zenon_X174)
% 0.38/0.62  (Tau_86 != Tau_87)
% 0.38/0.62  (zenon_X214 != Tau_92)
% 0.38/0.62  (-. (cheap Tau_84 Tau_198))
% 0.38/0.62  (-. (old Tau_84 zenon_X199))
% 0.38/0.62  (nonreflexive Tau_84 Tau_100)
% 0.38/0.62  (zenon_X224 != Tau_93)
% 0.38/0.62  (actual_world Tau_84)
% 0.38/0.62  (Tau_89 != zenon_X168)
% 0.38/0.62  (-. (cheap Tau_84 Tau_227))
% 0.38/0.62  (zenon_X172 != Tau_92)
% 0.38/0.62  (Tau_123 != zenon_X97)
% 0.38/0.62  (-. (cheap Tau_84 Tau_187))
% 0.38/0.62  (group Tau_84 Tau_85)
% 0.38/0.62  (zenon_X228 != Tau_92)
% 0.38/0.62  (fellow Tau_84 Tau_123)
% 0.38/0.62  (zenon_X218 != Tau_93)
% 0.38/0.62  (Tau_92 != zenon_X205)
% 0.38/0.62  (-. (cheap Tau_84 Tau_221))
% 0.38/0.62  (in Tau_84 Tau_91 Tau_87)
% 0.38/0.62  (-. (old Tau_84 zenon_X168))
% 0.38/0.62  (-. (city Tau_84 zenon_X140))
% 0.38/0.62  (-. (cheap Tau_84 Tau_183))
% 0.38/0.62  (Tau_93 != zenon_X113)
% 0.38/0.62  (-. (barrel Tau_84 zenon_X184))
% 0.38/0.62  (zenon_X203 != Tau_93)
% 0.38/0.62  (agent Tau_84 Tau_100 zenon_X99)
% 0.38/0.62  (-. (cheap Tau_84 Tau_123))
% 0.38/0.62  (-. (cheap Tau_84 Tau_167))
% 0.38/0.62  (street Tau_84 Tau_90)
% 0.38/0.62  (Tau_90 != zenon_X179)
% 0.38/0.62  (zenon_X193 != Tau_92)
% 0.38/0.62  (zenon_X172 != Tau_93)
% 0.38/0.62  (young Tau_84 Tau_123)
% 0.38/0.62  (member Tau_84 Tau_131 zenon_X130)
% 0.38/0.62  (-. (cheap Tau_84 Tau_219))
% 0.38/0.62  (member Tau_84 Tau_194 zenon_X193)
% 0.38/0.62  (zenon_X182 != Tau_93)
% 0.38/0.62  (zenon_X211 != Tau_92)
% 0.38/0.62  (event Tau_84 Tau_100)
% 0.38/0.62  (-. (member Tau_84 zenon_X101 Tau_93))
% 0.38/0.62  (zenon_X110 != Tau_93)
% 0.38/0.62  (-. (cheap Tau_84 Tau_161))
% 0.38/0.62  (-. (group Tau_84 zenon_X205))
% 0.38/0.62  (Tau_92 != zenon_X213)
% 0.38/0.62  (in Tau_84 Tau_96 Tau_86)
% 0.38/0.62  (-. (cheap Tau_84 Tau_223))
% 0.38/0.62  (dirty Tau_84 Tau_89)
% 0.38/0.62  (zenon_X160 != Tau_93)
% 0.38/0.62  (member Tau_84 Tau_161 zenon_X160)
% 0.38/0.62  (-. (cheap Tau_84 Tau_173))
% 0.38/0.62  (-. (placename Tau_84 zenon_X155))
% 0.38/0.62  (member Tau_84 Tau_198 zenon_X197)
% 0.38/0.62  (member zenon_X102 Tau_122 Tau_93)
% 0.38/0.62  (zenon_X230 != Tau_92)
% 0.38/0.62  (zenon_X203 != Tau_92)
% 0.38/0.62  (zenon_X206 != Tau_93)
% 0.38/0.62  (zenon_X186 != Tau_93)
% 0.38/0.62  (zenon_X218 != Tau_92)
% 0.38/0.62  (member Tau_84 Tau_147 zenon_X146)
% 0.38/0.62  (Tau_93 != zenon_X213)
% 0.38/0.62  (-. (cheap Tau_84 Tau_131))
% 0.38/0.62  (zenon_X222 != Tau_92)
% 0.38/0.62  (zenon_X146 != Tau_93)
% 0.38/0.62  (placename Tau_84 Tau_88)
% 0.38/0.62  (zenon_X110 != Tau_92)
% 0.38/0.62  (group Tau_84 Tau_92)
% 0.38/0.62  (-. (cheap zenon_X102 Tau_112))
% 0.38/0.62  (Tau_85 != zenon_X205)
% 0.38/0.62  (-. (cheap Tau_84 Tau_139))
% 0.38/0.62  (-. (cheap Tau_84 Tau_154))
% 0.38/0.62  (-. (cheap Tau_84 Tau_229))
% 0.38/0.62  (wear Tau_84 Tau_100)
% 0.38/0.62  (zenon_X146 != Tau_92)
% 0.38/0.62  (Tau_91 != zenon_X184)
% 0.38/0.62  (member Tau_84 Tau_121 zenon_X120)
% 0.38/0.62  (zenon_X153 != Tau_93)
% 0.38/0.62  (Tau_91 != zenon_X195)
% 0.38/0.62  (member Tau_84 Tau_187 zenon_X186)
% 0.38/0.62  (member Tau_84 Tau_154 zenon_X153)
% 0.38/0.62  (two Tau_84 Tau_92)
% 0.38/0.62  (Tau_85 != zenon_X213)
% 0.38/0.62  (zenon_X182 != Tau_92)
% 0.38/0.62  (member Tau_84 Tau_229 zenon_X228)
% 0.38/0.62  (Tau_87 != zenon_X140)
% 0.38/0.62  (zenon_X226 != Tau_93)
% 0.38/0.62  (zenon_X177 != Tau_92)
% 0.38/0.62  (-. (lonely Tau_84 zenon_X179))
% 0.38/0.62  (present Tau_84 Tau_100)
% 0.38/0.62  (member zenon_X102 Tau_111 zenon_X110)
% 0.38/0.62  (-. (city Tau_84 zenon_X132))
% 0.38/0.62  (member Tau_84 Tau_167 zenon_X166)
% 0.38/0.62  (zenon_X222 != Tau_93)
% 0.38/0.62  (Tau_87 != zenon_X124)
% 0.38/0.62  (-. (cheap Tau_84 Tau_147))
% 0.38/0.62  (-. (barrel Tau_84 zenon_X216))
% 0.38/0.62  (zenon_X102 != Tau_84)
% 0.38/0.62  (of Tau_84 Tau_88 Tau_87)
% 0.38/0.62  (zenon_X197 != Tau_92)
% 0.38/0.62  (member Tau_84 Tau_231 zenon_X230)
% 0.38/0.62  (event Tau_84 Tau_91)
% 0.38/0.62  (Tau_88 != zenon_X188)
% 0.38/0.62  (-. (cheap Tau_84 Tau_178))
% 0.38/0.62  (member Tau_84 Tau_215 zenon_X214)
% 0.38/0.62  (-. (cheap Tau_84 Tau_194))
% 0.38/0.62  (zenon_X138 != Tau_92)
% 0.38/0.62  (Tau_89 != zenon_X162)
% 0.38/0.62  (Tau_88 != zenon_X148)
% 0.38/0.62  (-. (cheap Tau_84 Tau_121))
% 0.38/0.62  (Tau_90 != zenon_X208)
% 0.38/0.62  (-. (frontseat Tau_84 Tau_87))
% 0.38/0.62  (-. (group Tau_84 zenon_X213))
% 0.38/0.62  (zenon_X130 != Tau_93)
% 0.38/0.62  (Tau_88 != zenon_X155)
% 0.38/0.62  (-. (group Tau_84 zenon_X113))
% 0.38/0.62  (zenon_X166 != Tau_92)
% 0.38/0.62  (member Tau_84 Tau_227 zenon_X226)
% 0.38/0.62  (-. (cheap Tau_84 Tau_207))
% 0.38/0.62  (-. (cheap Tau_84 Tau_204))
% 0.38/0.62  (Tau_91 != zenon_X216)
% 0.38/0.62  (Tau_92 != Tau_93)
% 0.38/0.62  (zenon_X130 != Tau_92)
% 0.38/0.62  (zenon_X160 != Tau_92)
% 0.38/0.62  (member Tau_84 Tau_183 zenon_X182)
% 0.38/0.62  (zenon_X206 != Tau_92)
% 0.38/0.62  (zenon_X193 != Tau_93)
% 0.38/0.62  (state Tau_84 Tau_95)
% 0.38/0.62  (zenon_X138 != Tau_93)
% 0.38/0.62  (zenon_X220 != Tau_93)
% 0.38/0.62  (white Tau_84 Tau_89)
% 0.38/0.62  (zenon_X120 != Tau_93)
% 0.38/0.62  (-. (lonely Tau_84 zenon_X208))
% 0.38/0.62  (member Tau_84 Tau_204 zenon_X203)
% 0.38/0.62  (Tau_85 != zenon_X113)
% 0.38/0.62  (agent Tau_84 Tau_91 Tau_89)
% 0.38/0.62  (-. (placename Tau_84 zenon_X148))
% 0.38/0.62  (zenon_X166 != Tau_93)
% 0.38/0.62  (member Tau_84 Tau_173 zenon_X172)
% 0.38/0.62  (Tau_92 != Tau_85)
% 0.38/0.62  (zenon_X220 != Tau_92)
% 0.38/0.62  (zenon_X153 != Tau_92)
% 0.38/0.62  (-. (lonely Tau_84 zenon_X174))
% 0.38/0.62  (member Tau_84 Tau_139 zenon_X138)
% 0.38/0.62  (member Tau_84 Tau_219 zenon_X218)
% 0.38/0.62  (zenon_X226 != Tau_92)
% 0.38/0.62  (barrel Tau_84 Tau_91)
% 0.38/0.62  (-. (member Tau_84 zenon_X97 Tau_92))
% 0.38/0.62  (zenon_X120 != Tau_92)
% 0.38/0.62  (member zenon_X102 Tau_112 Tau_92)
% 0.38/0.62  (-. (city Tau_84 zenon_X124))
% 0.38/0.62  (Tau_93 != zenon_X205)
% 0.38/0.62  (zenon_X224 != Tau_92)
% 0.38/0.62  (old Tau_84 Tau_89)
% 0.38/0.62  (chevy Tau_84 Tau_89)
% 0.38/0.62  (member Tau_84 Tau_178 zenon_X177)
% 0.38/0.62  (present Tau_84 Tau_91)
% 0.38/0.62  (group Tau_84 Tau_93)
% 0.38/0.62  (zenon_X228 != Tau_93)
% 0.38/0.62  (member Tau_84 Tau_207 zenon_X206)
% 0.38/0.62  (member Tau_84 Tau_123 Tau_92)
% 0.38/0.62  (-. (cheap zenon_X102 Tau_122))
% 0.38/0.62  (zenon_X230 != Tau_93)
% 0.38/0.62  (be Tau_84 Tau_95 zenon_X94 Tau_96)
% 0.38/0.62  (patient Tau_84 Tau_100 zenon_X98)
% 0.38/0.62  (-. (cheap Tau_84 Tau_215))
% 0.38/0.62  (zenon_X186 != Tau_92)
% 0.38/0.62  (zenon_X214 != Tau_93)
% 0.38/0.62  (zenon_X177 != Tau_93)
% 0.38/0.62  (-. (barrel Tau_84 zenon_X195))
% 0.38/0.62  (zenon_X211 != Tau_93)
% 0.38/0.62  (Tau_87 != zenon_X132)
% 0.38/0.62  (city Tau_84 Tau_87)
% 0.38/0.62  (-. (two Tau_84 Tau_85))
% 0.38/0.62  (-. (cheap Tau_84 Tau_231))
% 0.38/0.62  (member Tau_84 Tau_225 zenon_X224)
% 0.38/0.62  (lonely Tau_84 Tau_90)
% 0.38/0.62  (frontseat Tau_84 Tau_86)
% 0.38/0.62  (down Tau_84 Tau_91 Tau_90)
% 0.38/0.62  (Tau_92 != zenon_X113)
% 0.38/0.62  (member Tau_84 Tau_221 zenon_X220)
% 0.38/0.62  (zenon_X197 != Tau_93)
% 0.38/0.62  (member Tau_84 Tau_223 zenon_X222)
% 0.38/0.62  (-. (cheap zenon_X102 Tau_111))
% 0.38/0.62  (-. (placename Tau_84 zenon_X188))
% 0.38/0.62  (hollywood_placename Tau_84 Tau_88)
% 0.38/0.62  (-. (old Tau_84 zenon_X162))
% 0.38/0.62  *)
% 0.38/0.62  (* NO-PROOF *)
% 0.38/0.62  % SZS status GaveUp
% 0.38/0.62  Number of rewrites on terms: 0
% 0.38/0.62  Number of rewrites on props: 0
% 0.38/0.62  nodes searched: 758
% 0.38/0.62  max branch formulas: 488
% 0.38/0.62  proof nodes created: 59
% 0.38/0.62  formulas created: 11437
% 0.38/0.62  
%------------------------------------------------------------------------------