↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n007.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.21s 0.60s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13  % Problem  : NLP165+1 : TPTP v8.2.0. Released v2.4.0.
% 0.07/0.13  % Command  : run_zenon_modulo %d %s
% 0.12/0.34  % Computer : n007.cluster.edu
% 0.12/0.34  % Model    : x86_64 x86_64
% 0.12/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34  % Memory   : 8042.1875MB
% 0.12/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34  % CPULimit : 300
% 0.12/0.34  % WCLimit  : 300
% 0.12/0.34  % DateTime : Sat Jun 22 23:57:54 EDT 2024
% 0.12/0.34  % CPUTime  : 
% 0.21/0.60  Zenon error: exhausted search space without finding a proof
% 0.21/0.60  (* Current branch:
% 0.21/0.60  (zenon_X221 != Tau_132)
% 0.21/0.60  (-. (cheap Tau_123 Tau_243))
% 0.21/0.60  (zenon_X245 != Tau_132)
% 0.21/0.60  (member Tau_123 Tau_186 zenon_X185)
% 0.21/0.60  (-. (cheap zenon_X141 Tau_150))
% 0.21/0.60  (zenon_X232 != Tau_132)
% 0.21/0.60  (-. (cheap Tau_123 Tau_270))
% 0.21/0.60  (Tau_130 != zenon_X223)
% 0.21/0.60  (member Tau_123 Tau_260 zenon_X259)
% 0.21/0.60  (zenon_X242 != Tau_132)
% 0.21/0.60  (member Tau_123 Tau_251 zenon_X250)
% 0.21/0.60  (nonreflexive Tau_123 Tau_139)
% 0.21/0.60  (-. (cheap Tau_123 Tau_200))
% 0.21/0.60  (-. (old Tau_123 zenon_X201))
% 0.21/0.60  (zenon_X232 != Tau_131)
% 0.21/0.60  (Tau_130 != zenon_X255)
% 0.21/0.60  (actual_world Tau_123)
% 0.21/0.60  (-. (placename Tau_123 zenon_X194))
% 0.21/0.60  (-. (group Tau_123 zenon_X244))
% 0.21/0.60  (zenon_X269 != Tau_132)
% 0.21/0.60  (member Tau_123 Tau_254 zenon_X253)
% 0.21/0.60  (Tau_127 != zenon_X187)
% 0.21/0.60  (zenon_X263 != Tau_132)
% 0.21/0.60  (Tau_162 != zenon_X136)
% 0.21/0.60  (zenon_X261 != Tau_131)
% 0.21/0.60  (group Tau_123 Tau_124)
% 0.21/0.60  (fellow Tau_123 Tau_162)
% 0.21/0.60  (-. (cheap Tau_123 Tau_237))
% 0.21/0.60  (in Tau_123 Tau_130 Tau_126)
% 0.21/0.60  (-. (city Tau_123 zenon_X179))
% 0.21/0.60  (-. (placename Tau_123 zenon_X227))
% 0.21/0.60  (-. (cheap Tau_123 Tau_178))
% 0.21/0.60  (Tau_132 != zenon_X152)
% 0.21/0.60  (zenon_X257 != Tau_132)
% 0.21/0.60  (-. (cheap Tau_123 Tau_206))
% 0.21/0.60  (-. (cheap Tau_123 Tau_160))
% 0.21/0.60  (agent Tau_123 Tau_139 zenon_X138)
% 0.21/0.60  (zenon_X185 != Tau_132)
% 0.21/0.60  (-. (cheap Tau_123 Tau_170))
% 0.21/0.60  (-. (cheap Tau_123 Tau_162))
% 0.21/0.60  (zenon_X265 != Tau_131)
% 0.21/0.60  (street Tau_123 Tau_129)
% 0.21/0.60  (young Tau_123 Tau_162)
% 0.21/0.60  (zenon_X211 != Tau_132)
% 0.21/0.60  (Tau_128 != zenon_X238)
% 0.21/0.60  (Tau_131 != zenon_X252)
% 0.21/0.60  (-. (cheap Tau_123 Tau_186))
% 0.21/0.60  (Tau_125 != Tau_129)
% 0.21/0.60  (event Tau_123 Tau_139)
% 0.21/0.60  (-. (member Tau_123 zenon_X140 Tau_132))
% 0.21/0.60  (member Tau_123 Tau_246 zenon_X245)
% 0.21/0.60  (-. (cheap Tau_123 Tau_226))
% 0.21/0.60  (Tau_128 != zenon_X207)
% 0.21/0.60  (zenon_X159 != Tau_132)
% 0.21/0.60  (-. (cheap Tau_123 Tau_260))
% 0.21/0.60  (member Tau_123 Tau_217 zenon_X216)
% 0.21/0.60  (zenon_X250 != Tau_131)
% 0.21/0.60  (member Tau_123 Tau_178 zenon_X177)
% 0.21/0.60  (in Tau_123 Tau_135 Tau_125)
% 0.21/0.60  (zenon_X205 != Tau_132)
% 0.21/0.60  (Tau_124 != zenon_X252)
% 0.21/0.60  (zenon_X225 != Tau_132)
% 0.21/0.60  (dirty Tau_123 Tau_128)
% 0.21/0.60  (zenon_X259 != Tau_131)
% 0.21/0.60  (Tau_132 != zenon_X252)
% 0.21/0.60  (member Tau_123 Tau_266 zenon_X265)
% 0.21/0.60  (Tau_129 != zenon_X247)
% 0.21/0.60  (zenon_X225 != Tau_131)
% 0.21/0.60  (member zenon_X141 Tau_161 Tau_132)
% 0.21/0.60  (-. (barrel Tau_123 zenon_X255))
% 0.21/0.60  (Tau_130 != zenon_X234)
% 0.21/0.60  (zenon_X267 != Tau_132)
% 0.21/0.60  (-. (old Tau_123 zenon_X207))
% 0.21/0.60  (zenon_X177 != Tau_132)
% 0.21/0.60  (zenon_X149 != Tau_131)
% 0.21/0.60  (zenon_X265 != Tau_132)
% 0.21/0.60  (zenon_X159 != Tau_131)
% 0.21/0.60  (placename Tau_123 Tau_127)
% 0.21/0.60  (member zenon_X141 Tau_150 zenon_X149)
% 0.21/0.60  (member Tau_123 Tau_237 zenon_X236)
% 0.21/0.60  (group Tau_123 Tau_131)
% 0.21/0.60  (-. (cheap zenon_X141 Tau_151))
% 0.21/0.60  (zenon_X259 != Tau_132)
% 0.21/0.60  (member Tau_123 Tau_200 zenon_X199)
% 0.21/0.60  (member Tau_123 Tau_226 zenon_X225)
% 0.21/0.60  (wear Tau_123 Tau_139)
% 0.21/0.60  (zenon_X253 != Tau_132)
% 0.21/0.60  (zenon_X149 != Tau_132)
% 0.21/0.60  (-. (cheap Tau_123 Tau_222))
% 0.21/0.60  (member Tau_123 Tau_258 zenon_X257)
% 0.21/0.60  (zenon_X261 != Tau_132)
% 0.21/0.60  (zenon_X253 != Tau_131)
% 0.21/0.60  (two Tau_123 Tau_131)
% 0.21/0.60  (zenon_X216 != Tau_132)
% 0.21/0.60  (member Tau_123 Tau_160 zenon_X159)
% 0.21/0.60  (member Tau_123 Tau_268 zenon_X267)
% 0.21/0.60  (-. (cheap Tau_123 Tau_193))
% 0.21/0.60  (Tau_126 != zenon_X179)
% 0.21/0.60  (present Tau_123 Tau_139)
% 0.21/0.60  (-. (cheap Tau_123 Tau_264))
% 0.21/0.60  (member Tau_123 Tau_206 zenon_X205)
% 0.21/0.60  (zenon_X242 != Tau_131)
% 0.21/0.60  (-. (city Tau_123 zenon_X171))
% 0.21/0.60  (Tau_126 != zenon_X163)
% 0.21/0.60  (zenon_X267 != Tau_131)
% 0.21/0.60  (zenon_X257 != Tau_131)
% 0.21/0.60  (-. (cheap Tau_123 Tau_251))
% 0.21/0.60  (zenon_X269 != Tau_131)
% 0.21/0.60  (zenon_X141 != Tau_123)
% 0.21/0.60  (zenon_X192 != Tau_131)
% 0.21/0.60  (of Tau_123 Tau_127 Tau_126)
% 0.21/0.60  (zenon_X169 != Tau_131)
% 0.21/0.60  (member Tau_123 Tau_262 zenon_X261)
% 0.21/0.60  (zenon_X211 != Tau_131)
% 0.21/0.60  (zenon_X216 != Tau_131)
% 0.21/0.60  (event Tau_123 Tau_130)
% 0.21/0.60  (member Tau_123 Tau_212 zenon_X211)
% 0.21/0.60  (Tau_127 != zenon_X194)
% 0.21/0.60  (-. (barrel Tau_123 zenon_X223))
% 0.21/0.60  (zenon_X199 != Tau_132)
% 0.21/0.60  (-. (barrel Tau_123 zenon_X234))
% 0.21/0.60  (-. (group Tau_123 zenon_X152))
% 0.21/0.60  (-. (cheap Tau_123 Tau_266))
% 0.21/0.60  (-. (cheap Tau_123 Tau_233))
% 0.21/0.60  (-. (lonely Tau_123 zenon_X247))
% 0.21/0.60  (Tau_124 != zenon_X244)
% 0.21/0.60  (-. (lonely Tau_123 zenon_X218))
% 0.21/0.60  (zenon_X192 != Tau_132)
% 0.21/0.60  (Tau_131 != Tau_132)
% 0.21/0.60  (Tau_131 != zenon_X244)
% 0.21/0.60  (member Tau_123 Tau_222 zenon_X221)
% 0.21/0.60  (-. (old Tau_123 zenon_X238))
% 0.21/0.60  (zenon_X263 != Tau_131)
% 0.21/0.60  (-. (cheap Tau_123 Tau_212))
% 0.21/0.60  (state Tau_123 Tau_134)
% 0.21/0.60  (white Tau_123 Tau_128)
% 0.21/0.60  (member Tau_123 Tau_193 zenon_X192)
% 0.21/0.60  (zenon_X236 != Tau_132)
% 0.21/0.60  (zenon_X177 != Tau_131)
% 0.21/0.60  (Tau_124 != zenon_X152)
% 0.21/0.60  (agent Tau_123 Tau_130 Tau_128)
% 0.21/0.60  (zenon_X205 != Tau_131)
% 0.21/0.60  (member Tau_123 Tau_233 zenon_X232)
% 0.21/0.60  (zenon_X199 != Tau_131)
% 0.21/0.60  (Tau_131 != Tau_124)
% 0.21/0.60  (-. (cheap Tau_123 Tau_268))
% 0.21/0.60  (Tau_128 != zenon_X201)
% 0.21/0.60  (-. (lonely Tau_123 zenon_X213))
% 0.21/0.60  (barrel Tau_123 Tau_130)
% 0.21/0.60  (-. (member Tau_123 zenon_X136 Tau_131))
% 0.21/0.60  (-. (group Tau_123 zenon_X252))
% 0.21/0.60  (zenon_X169 != Tau_132)
% 0.21/0.60  (member zenon_X141 Tau_151 Tau_131)
% 0.21/0.60  (-. (city Tau_123 zenon_X163))
% 0.21/0.60  (-. (placename Tau_123 zenon_X187))
% 0.21/0.60  (zenon_X185 != Tau_131)
% 0.21/0.60  (Tau_127 != zenon_X227)
% 0.21/0.60  (zenon_X250 != Tau_132)
% 0.21/0.60  (old Tau_123 Tau_128)
% 0.21/0.60  (chevy Tau_123 Tau_128)
% 0.21/0.60  (present Tau_123 Tau_130)
% 0.21/0.60  (Tau_129 != zenon_X213)
% 0.21/0.60  (group Tau_123 Tau_132)
% 0.21/0.60  (member Tau_123 Tau_264 zenon_X263)
% 0.21/0.60  (-. (cheap Tau_123 Tau_254))
% 0.21/0.60  (zenon_X236 != Tau_131)
% 0.21/0.60  (zenon_X245 != Tau_131)
% 0.21/0.60  (member Tau_123 Tau_162 Tau_131)
% 0.21/0.60  (-. (cheap zenon_X141 Tau_161))
% 0.21/0.60  (be Tau_123 Tau_134 zenon_X133 Tau_135)
% 0.21/0.60  (member Tau_123 Tau_270 zenon_X269)
% 0.21/0.60  (patient Tau_123 Tau_139 zenon_X137)
% 0.21/0.60  (-. (cheap Tau_123 Tau_246))
% 0.21/0.60  (Tau_129 != zenon_X218)
% 0.21/0.60  (Tau_132 != zenon_X244)
% 0.21/0.60  (Tau_126 != zenon_X171)
% 0.21/0.60  (city Tau_123 Tau_126)
% 0.21/0.60  (-. (two Tau_123 Tau_124))
% 0.21/0.60  (-. (cheap Tau_123 Tau_217))
% 0.21/0.60  (member Tau_123 Tau_170 zenon_X169)
% 0.21/0.60  (-. (frontseat Tau_123 Tau_129))
% 0.21/0.60  (lonely Tau_123 Tau_129)
% 0.21/0.60  (member Tau_123 Tau_243 zenon_X242)
% 0.21/0.60  (-. (cheap Tau_123 Tau_258))
% 0.21/0.60  (frontseat Tau_123 Tau_125)
% 0.21/0.60  (down Tau_123 Tau_130 Tau_129)
% 0.21/0.60  (Tau_131 != zenon_X152)
% 0.21/0.60  (zenon_X221 != Tau_131)
% 0.21/0.60  (-. (cheap Tau_123 Tau_262))
% 0.21/0.60  (hollywood_placename Tau_123 Tau_127)
% 0.21/0.60  *)
% 0.21/0.60  (* NO-PROOF *)
% 0.21/0.60  % SZS status GaveUp
% 0.21/0.60  Number of rewrites on terms: 0
% 0.21/0.60  Number of rewrites on props: 0
% 0.21/0.60  nodes searched: 873
% 0.21/0.60  max branch formulas: 488
% 0.21/0.60  proof nodes created: 71
% 0.21/0.60  formulas created: 13321
% 0.21/0.60  
%------------------------------------------------------------------------------