↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n005.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:06 EDT 2024

% Result   : Unknown 0.50s 0.65s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.13/0.14  % Problem  : NLP005+1 : TPTP v8.2.0. Released v2.4.0.
% 0.13/0.14  % Command  : run_zenon_modulo %d %s
% 0.14/0.35  % Computer : n005.cluster.edu
% 0.14/0.35  % Model    : x86_64 x86_64
% 0.14/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.35  % Memory   : 8042.1875MB
% 0.14/0.35  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.14/0.35  % CPULimit : 300
% 0.14/0.35  % WCLimit  : 300
% 0.14/0.35  % DateTime : Sat Jun 22 22:16:39 EDT 2024
% 0.14/0.35  % CPUTime  : 
% 0.50/0.65  Zenon error: exhausted search space without finding a proof
% 0.50/0.65  (* Current branch:
% 0.50/0.65  (-. (young zenon_X137))
% 0.50/0.65  (Tau_0 != zenon_X10)
% 0.50/0.65  (barrel Tau_3 Tau_5)
% 0.50/0.65  (zenon_X148 != Tau_7)
% 0.50/0.65  (zenon_X76 != Tau_6)
% 0.50/0.65  (Tau_2 != zenon_X10)
% 0.50/0.65  (zenon_X93 != Tau_7)
% 0.50/0.65  (Tau_6 != zenon_X125)
% 0.50/0.65  (Tau_2 != Tau_0)
% 0.50/0.65  (zenon_X144 != Tau_6)
% 0.50/0.65  (Tau_7 != zenon_X145)
% 0.50/0.65  (Tau_9 != zenon_X189)
% 0.50/0.65  (-. (in zenon_X93 Tau_1))
% 0.50/0.65  (-. (in zenon_X64 Tau_2))
% 0.50/0.65  (-. (in zenon_X116 Tau_2))
% 0.50/0.65  (Tau_2 != zenon_X27)
% 0.50/0.65  (in Tau_3 Tau_2)
% 0.50/0.65  (-. (event zenon_X87))
% 0.50/0.65  (fellow Tau_6)
% 0.50/0.65  (Tau_4 != zenon_X129)
% 0.50/0.65  (Tau_6 != zenon_X65)
% 0.50/0.65  (-. (in zenon_X76 Tau_0))
% 0.50/0.65  (Tau_3 != zenon_X116)
% 0.50/0.65  (-. (lonely zenon_X129))
% 0.50/0.65  (-. (city zenon_X27))
% 0.50/0.65  (Tau_8 != zenon_X61)
% 0.50/0.65  (Tau_8 != zenon_X161)
% 0.50/0.65  (-. (in zenon_X139 Tau_0))
% 0.50/0.65  (-. (in zenon_X159 Tau_0))
% 0.50/0.65  (zenon_X133 != Tau_7)
% 0.50/0.65  (-. (in zenon_X143 Tau_0))
% 0.50/0.65  (Tau_3 != zenon_X99)
% 0.50/0.65  (front Tau_1)
% 0.50/0.65  (-. (in zenon_X144 Tau_0))
% 0.50/0.65  (-. (young zenon_X145))
% 0.50/0.65  (zenon_X106 != Tau_6)
% 0.50/0.65  (white Tau_5)
% 0.50/0.65  (Tau_9 != zenon_X93)
% 0.50/0.65  (hollywood Tau_2)
% 0.50/0.65  (-. (city zenon_X35))
% 0.50/0.65  (Tau_6 != Tau_7)
% 0.50/0.65  (-. (in zenon_X142 Tau_0))
% 0.50/0.65  (Tau_8 != zenon_X159)
% 0.50/0.65  (-. (old zenon_X50))
% 0.50/0.65  (zenon_X122 != Tau_7)
% 0.50/0.65  (-. (young zenon_X125))
% 0.50/0.65  (Tau_6 != zenon_X164)
% 0.50/0.65  (young Tau_6)
% 0.50/0.65  (Tau_8 != zenon_X158)
% 0.50/0.65  (Tau_7 != zenon_X134)
% 0.50/0.65  (-. (in zenon_X67 Tau_2))
% 0.50/0.65  (zenon_X182 != Tau_7)
% 0.50/0.65  (Tau_3 != zenon_X70)
% 0.50/0.65  (zenon_X159 != Tau_6)
% 0.50/0.65  (young Tau_7)
% 0.50/0.65  (-. (in zenon_X55 Tau_2))
% 0.50/0.65  (man Tau_6)
% 0.50/0.65  (Tau_5 != zenon_X50)
% 0.50/0.65  (Tau_8 != zenon_X142)
% 0.50/0.65  (old Tau_5)
% 0.50/0.65  (Tau_8 != zenon_X76)
% 0.50/0.65  (Tau_7 != zenon_X61)
% 0.50/0.65  (Tau_1 != zenon_X10)
% 0.50/0.65  (-. (in zenon_X42 Tau_2))
% 0.50/0.65  (Tau_7 != zenon_X164)
% 0.50/0.65  (-. (in zenon_X136 Tau_0))
% 0.50/0.65  (Tau_9 != Tau_8)
% 0.50/0.65  (Tau_3 != zenon_X64)
% 0.50/0.65  (-. (young zenon_X65))
% 0.50/0.65  (-. (young zenon_X114))
% 0.50/0.65  (Tau_3 != zenon_X42)
% 0.50/0.65  (Tau_9 != zenon_X133)
% 0.50/0.65  (-. (in zenon_X106 Tau_0))
% 0.50/0.65  (-. (in zenon_X166 Tau_1))
% 0.50/0.65  (-. (young zenon_X169))
% 0.50/0.65  (Tau_4 != zenon_X109)
% 0.50/0.65  (seat Tau_0)
% 0.50/0.65  (-. (in zenon_X189 Tau_1))
% 0.50/0.65  (-. (front Tau_2))
% 0.50/0.65  (Tau_9 != zenon_X171)
% 0.50/0.65  (zenon_X142 != Tau_6)
% 0.50/0.65  (zenon_X157 != Tau_6)
% 0.50/0.65  (event Tau_3)
% 0.50/0.65  (-. (in zenon_X113 Tau_0))
% 0.50/0.65  (Tau_7 != zenon_X137)
% 0.50/0.65  (zenon_X136 != Tau_6)
% 0.50/0.65  (-. (in zenon_X60 Tau_2))
% 0.50/0.65  (Tau_8 != zenon_X113)
% 0.50/0.65  (furniture Tau_1)
% 0.50/0.65  (Tau_8 != zenon_X106)
% 0.50/0.65  (Tau_0 != Tau_1)
% 0.50/0.65  (-. (in zenon_X182 Tau_1))
% 0.50/0.65  (city Tau_2)
% 0.50/0.65  (Tau_8 != zenon_X139)
% 0.50/0.65  (lonely Tau_4)
% 0.50/0.65  (Tau_9 != zenon_X26)
% 0.50/0.65  (-. (young zenon_X61))
% 0.50/0.65  (zenon_X34 != Tau_6)
% 0.50/0.65  (zenon_X188 != Tau_7)
% 0.50/0.65  (-. (in zenon_X202 Tau_2))
% 0.50/0.65  (Tau_9 != Tau_6)
% 0.50/0.65  (Tau_5 != zenon_X101)
% 0.50/0.65  (Tau_6 = Tau_8)
% 0.50/0.65  (Tau_2 != zenon_X19)
% 0.50/0.65  (zenon_X26 != Tau_7)
% 0.50/0.65  (Tau_8 != zenon_X65)
% 0.50/0.65  (-. (in zenon_X161 Tau_0))
% 0.50/0.65  (-. (city zenon_X19))
% 0.50/0.65  (Tau_9 != zenon_X148)
% 0.50/0.65  (-. (in zenon_X18 zenon_X10))
% 0.50/0.65  (-. (young zenon_X140))
% 0.50/0.65  (Tau_8 != zenon_X144)
% 0.50/0.65  (Tau_8 != zenon_X143)
% 0.50/0.65  (Tau_8 != zenon_X134)
% 0.50/0.65  (Tau_7 != zenon_X125)
% 0.50/0.65  (Tau_8 != zenon_X34)
% 0.50/0.65  (Tau_6 != zenon_X169)
% 0.50/0.65  (-. (young zenon_X164))
% 0.50/0.65  (-. (in zenon_X148 Tau_1))
% 0.50/0.65  (Tau_3 != zenon_X202)
% 0.50/0.65  (Tau_3 != zenon_X67)
% 0.50/0.65  (dirty Tau_5)
% 0.50/0.65  (Tau_6 != zenon_X134)
% 0.50/0.65  (Tau_9 != zenon_X188)
% 0.50/0.65  (street Tau_4)
% 0.50/0.65  (zenon_X139 != Tau_6)
% 0.50/0.65  (zenon_X158 != Tau_6)
% 0.50/0.65  (Tau_7 != zenon_X114)
% 0.50/0.65  (-. (young zenon_X134))
% 0.50/0.65  (Tau_8 != zenon_X137)
% 0.50/0.65  (Tau_8 != zenon_X136)
% 0.50/0.65  (Tau_4 != zenon_X56)
% 0.50/0.65  (-. (in zenon_X158 Tau_0))
% 0.50/0.65  (-. (in zenon_X100 Tau_2))
% 0.50/0.65  (-. (in zenon_X122 Tau_1))
% 0.50/0.65  (way Tau_4)
% 0.50/0.65  (zenon_X161 != Tau_6)
% 0.50/0.65  (-. (lonely zenon_X109))
% 0.50/0.65  (Tau_3 != zenon_X100)
% 0.50/0.65  (-. (in zenon_X188 Tau_1))
% 0.50/0.65  (-. (in zenon_X157 Tau_0))
% 0.50/0.65  (Tau_8 != zenon_X114)
% 0.50/0.65  (Tau_7 != zenon_X140)
% 0.50/0.65  (in Tau_8 Tau_0)
% 0.50/0.65  (Tau_9 != zenon_X122)
% 0.50/0.65  (furniture Tau_0)
% 0.50/0.65  (Tau_5 != zenon_X117)
% 0.50/0.65  (man Tau_7)
% 0.50/0.65  (-. (old zenon_X101))
% 0.50/0.65  (-. (in zenon_X99 Tau_2))
% 0.50/0.65  (-. (in zenon_X49 Tau_2))
% 0.50/0.65  (car Tau_5)
% 0.50/0.65  (-. (event zenon_X70))
% 0.50/0.65  (zenon_X171 != Tau_7)
% 0.50/0.65  (Tau_6 != zenon_X114)
% 0.50/0.65  (down Tau_3 Tau_4)
% 0.50/0.65  (-. (in zenon_X171 Tau_1))
% 0.50/0.65  (fellow Tau_7)
% 0.50/0.65  (zenon_X113 != Tau_6)
% 0.50/0.65  (-. (lonely zenon_X56))
% 0.50/0.65  (Tau_2 != zenon_X35)
% 0.50/0.65  (Tau_9 != zenon_X182)
% 0.50/0.65  (Tau_6 != zenon_X61)
% 0.50/0.65  (Tau_8 != zenon_X128)
% 0.50/0.65  (-. (in zenon_X133 Tau_1))
% 0.50/0.65  (Tau_6 != zenon_X145)
% 0.50/0.65  (-. (in zenon_X26 Tau_1))
% 0.50/0.65  (Tau_3 != zenon_X49)
% 0.50/0.65  (Tau_6 != zenon_X140)
% 0.50/0.65  (front Tau_0)
% 0.50/0.65  (seat Tau_1)
% 0.50/0.65  (zenon_X128 != Tau_6)
% 0.50/0.65  (Tau_9 != zenon_X166)
% 0.50/0.65  (in Tau_9 Tau_1)
% 0.50/0.65  (Tau_3 != zenon_X55)
% 0.50/0.65  (Tau_8 != zenon_X157)
% 0.50/0.65  (Tau_3 != zenon_X87)
% 0.50/0.65  (-. (event zenon_X43))
% 0.50/0.65  (Tau_7 != zenon_X65)
% 0.50/0.65  (Tau_6 != zenon_X137)
% 0.50/0.65  (-. (in zenon_X128 Tau_0))
% 0.50/0.65  (zenon_X143 != Tau_6)
% 0.50/0.65  (-. (in zenon_X34 Tau_0))
% 0.50/0.65  (Tau_7 != zenon_X169)
% 0.50/0.65  (Tau_8 != Tau_7)
% 0.50/0.65  (Tau_8 != zenon_X125)
% 0.50/0.65  (Tau_3 != zenon_X60)
% 0.50/0.65  (zenon_X189 != Tau_7)
% 0.50/0.65  (Tau_7 = Tau_9)
% 0.50/0.65  (Tau_8 != zenon_X140)
% 0.50/0.65  (-. (old zenon_X117))
% 0.50/0.65  (chevy Tau_5)
% 0.50/0.65  (Tau_2 != Tau_1)
% 0.50/0.65  (zenon_X166 != Tau_7)
% 0.50/0.65  (Tau_3 != zenon_X43)
% 0.50/0.65  *)
% 0.50/0.65  (* NO-PROOF *)
% 0.50/0.65  % SZS status GaveUp
% 0.50/0.65  Number of rewrites on terms: 0
% 0.50/0.65  Number of rewrites on props: 0
% 0.50/0.65  nodes searched: 1677
% 0.50/0.65  max branch formulas: 541
% 0.50/0.65  proof nodes created: 226
% 0.50/0.65  formulas created: 14686
% 0.50/0.65  
%------------------------------------------------------------------------------