↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n015.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.49s 0.65s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12  % Problem  : NLP008+1 : TPTP v8.2.0. Released v2.4.0.
% 0.03/0.12  % Command  : run_zenon_modulo %d %s
% 0.12/0.33  % Computer : n015.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  : 300
% 0.12/0.33  % DateTime : Sat Jun 22 22:35:24 EDT 2024
% 0.12/0.33  % CPUTime  : 
% 0.49/0.65  Zenon error: exhausted search space without finding a proof
% 0.49/0.65  (* Current branch:
% 0.49/0.65  (man Tau_6)
% 0.49/0.65  (Tau_9 != zenon_X159)
% 0.49/0.65  (-. (in zenon_X134 Tau_0))
% 0.49/0.65  (young Tau_5)
% 0.49/0.65  (Tau_6 != zenon_X138)
% 0.49/0.65  (front Tau_7)
% 0.49/0.65  (Tau_5 != zenon_X163)
% 0.49/0.65  (car Tau_3)
% 0.49/0.65  (-. (young zenon_X57))
% 0.49/0.65  (-. (in zenon_X70 Tau_7))
% 0.49/0.65  (Tau_8 != zenon_X131)
% 0.49/0.65  (Tau_8 != zenon_X165)
% 0.49/0.65  (Tau_9 != zenon_X148)
% 0.49/0.65  (zenon_X159 != Tau_6)
% 0.49/0.65  (-. (in zenon_X187 Tau_7))
% 0.49/0.65  (Tau_8 != zenon_X138)
% 0.49/0.65  (Tau_2 != zenon_X35)
% 0.49/0.65  (zenon_X26 != Tau_6)
% 0.49/0.65  (Tau_5 != Tau_6)
% 0.49/0.65  (-. (young zenon_X60))
% 0.49/0.65  (zenon_X70 != Tau_5)
% 0.49/0.65  (in Tau_8 Tau_7)
% 0.49/0.65  (old Tau_3)
% 0.49/0.65  (zenon_X143 != Tau_6)
% 0.49/0.65  (Tau_1 != Tau_0)
% 0.49/0.65  (-. (in zenon_X47 Tau_1))
% 0.49/0.65  (Tau_6 != zenon_X160)
% 0.49/0.65  (Tau_8 != zenon_X102)
% 0.49/0.65  (Tau_9 != Tau_8)
% 0.49/0.65  (Tau_6 != zenon_X163)
% 0.49/0.65  (Tau_9 != zenon_X134)
% 0.49/0.65  (seat Tau_7)
% 0.49/0.65  (-. (city zenon_X27))
% 0.49/0.65  (-. (in zenon_X71 Tau_1))
% 0.49/0.65  (-. (in zenon_X140 Tau_0))
% 0.49/0.65  (city Tau_1)
% 0.49/0.65  (down Tau_2 Tau_4)
% 0.49/0.65  (Tau_9 != zenon_X170)
% 0.49/0.65  (-. (in zenon_X148 Tau_0))
% 0.49/0.65  (-. (in zenon_X34 Tau_1))
% 0.49/0.65  (Tau_4 != zenon_X105)
% 0.49/0.65  (Tau_6 != zenon_X144)
% 0.49/0.65  (zenon_X140 != Tau_6)
% 0.49/0.65  (-. (in zenon_X59 Tau_1))
% 0.49/0.65  (zenon_X87 != Tau_6)
% 0.49/0.65  (-. (in zenon_X130 Tau_7))
% 0.49/0.65  (Tau_5 != zenon_X144)
% 0.49/0.65  (zenon_X137 != Tau_6)
% 0.49/0.65  (Tau_8 != zenon_X53)
% 0.49/0.65  (zenon_X152 != Tau_6)
% 0.49/0.65  (-. (in zenon_X18 zenon_X10))
% 0.49/0.65  (-. (city zenon_X63))
% 0.49/0.65  (furniture Tau_7)
% 0.49/0.65  (-. (young zenon_X141))
% 0.49/0.65  (furniture Tau_0)
% 0.49/0.65  (Tau_6 = Tau_9)
% 0.49/0.65  (Tau_7 != zenon_X10)
% 0.49/0.65  (Tau_6 != zenon_X131)
% 0.49/0.65  (Tau_2 != zenon_X41)
% 0.49/0.65  (-. (in zenon_X152 Tau_0))
% 0.49/0.65  (zenon_X162 != Tau_5)
% 0.49/0.65  (Tau_9 != zenon_X119)
% 0.49/0.65  (-. (in zenon_X52 Tau_1))
% 0.49/0.65  (-. (in zenon_X56 Tau_1))
% 0.49/0.65  (-. (in zenon_X143 Tau_0))
% 0.49/0.65  (Tau_2 != zenon_X47)
% 0.49/0.65  (zenon_X147 != Tau_5)
% 0.49/0.65  (-. (event zenon_X81))
% 0.49/0.65  (in Tau_9 Tau_0)
% 0.49/0.65  (event Tau_2)
% 0.49/0.65  (-. (young zenon_X53))
% 0.49/0.65  (Tau_5 != zenon_X135)
% 0.49/0.65  (Tau_9 != zenon_X110)
% 0.49/0.65  (in Tau_2 Tau_1)
% 0.49/0.65  (Tau_6 != zenon_X60)
% 0.49/0.65  (Tau_4 != zenon_X120)
% 0.49/0.65  (Tau_9 != Tau_5)
% 0.49/0.65  (-. (in zenon_X159 Tau_0))
% 0.49/0.65  (Tau_8 != zenon_X125)
% 0.49/0.65  (zenon_X134 != Tau_6)
% 0.49/0.65  (zenon_X173 != Tau_5)
% 0.49/0.65  (-. (in zenon_X72 Tau_1))
% 0.49/0.65  (Tau_7 != Tau_1)
% 0.49/0.65  (zenon_X165 != Tau_5)
% 0.49/0.65  (-. (young zenon_X138))
% 0.49/0.65  (young Tau_6)
% 0.49/0.65  (-. (old zenon_X126))
% 0.49/0.65  (fellow Tau_5)
% 0.49/0.65  (-. (lonely zenon_X120))
% 0.49/0.65  (hollywood Tau_1)
% 0.49/0.65  (Tau_8 != zenon_X57)
% 0.49/0.65  (Tau_2 != zenon_X96)
% 0.49/0.65  (zenon_X130 != Tau_5)
% 0.49/0.65  (street Tau_4)
% 0.49/0.65  (white Tau_3)
% 0.49/0.65  (Tau_5 != zenon_X141)
% 0.49/0.65  (zenon_X170 != Tau_6)
% 0.49/0.65  (Tau_1 != zenon_X10)
% 0.49/0.65  (fellow Tau_6)
% 0.49/0.65  (Tau_3 != zenon_X126)
% 0.49/0.65  (Tau_9 != zenon_X26)
% 0.49/0.65  (Tau_9 != zenon_X137)
% 0.49/0.65  (-. (young zenon_X163))
% 0.49/0.65  (Tau_9 != zenon_X153)
% 0.49/0.65  (Tau_3 != zenon_X48)
% 0.49/0.65  (Tau_1 != zenon_X27)
% 0.49/0.65  (-. (young zenon_X160))
% 0.49/0.65  (-. (in zenon_X165 Tau_7))
% 0.49/0.65  (-. (in zenon_X147 Tau_7))
% 0.49/0.65  (zenon_X125 != Tau_5)
% 0.49/0.65  (Tau_2 != zenon_X34)
% 0.49/0.65  (-. (city zenon_X19))
% 0.49/0.65  (zenon_X174 != Tau_5)
% 0.49/0.65  (Tau_6 != zenon_X141)
% 0.49/0.65  (-. (in zenon_X87 Tau_0))
% 0.49/0.65  (Tau_5 = Tau_8)
% 0.49/0.65  (zenon_X102 != Tau_5)
% 0.49/0.65  (-. (in zenon_X26 Tau_0))
% 0.49/0.65  (-. (lonely zenon_X105))
% 0.49/0.65  (zenon_X110 != Tau_6)
% 0.49/0.65  (-. (in zenon_X170 Tau_0))
% 0.49/0.65  (Tau_9 != zenon_X149)
% 0.49/0.65  (-. (in zenon_X75 Tau_1))
% 0.49/0.65  (-. (in zenon_X76 Tau_1))
% 0.49/0.65  (Tau_5 != zenon_X60)
% 0.49/0.65  (Tau_8 != zenon_X135)
% 0.49/0.65  (Tau_8 != zenon_X60)
% 0.49/0.65  (Tau_2 != zenon_X75)
% 0.49/0.65  (Tau_2 != zenon_X72)
% 0.49/0.65  (-. (old zenon_X48))
% 0.49/0.65  (-. (young zenon_X131))
% 0.49/0.65  (-. (in zenon_X80 Tau_1))
% 0.49/0.65  (Tau_9 != zenon_X87)
% 0.49/0.65  (Tau_9 != zenon_X152)
% 0.49/0.65  (-. (old zenon_X115))
% 0.49/0.65  (Tau_5 != zenon_X131)
% 0.49/0.65  (-. (in zenon_X137 Tau_0))
% 0.49/0.65  (Tau_2 != zenon_X56)
% 0.49/0.65  (dirty Tau_3)
% 0.49/0.65  (Tau_8 != zenon_X174)
% 0.49/0.65  (Tau_8 != Tau_6)
% 0.49/0.65  (-. (young zenon_X135))
% 0.49/0.65  (Tau_6 != zenon_X53)
% 0.49/0.65  (Tau_9 != zenon_X143)
% 0.49/0.65  (Tau_9 != zenon_X140)
% 0.49/0.65  (Tau_8 != zenon_X173)
% 0.49/0.65  (zenon_X187 != Tau_5)
% 0.49/0.65  (Tau_8 != zenon_X130)
% 0.49/0.65  (chevy Tau_3)
% 0.49/0.65  (Tau_2 != zenon_X76)
% 0.49/0.65  (-. (lonely zenon_X42))
% 0.49/0.65  (Tau_6 != zenon_X57)
% 0.49/0.65  (Tau_0 != zenon_X10)
% 0.49/0.65  (Tau_8 != zenon_X187)
% 0.49/0.65  (-. (in zenon_X119 Tau_0))
% 0.49/0.65  (way Tau_4)
% 0.49/0.65  (Tau_2 != zenon_X80)
% 0.49/0.65  (-. (in zenon_X41 Tau_1))
% 0.49/0.65  (Tau_7 != Tau_0)
% 0.49/0.65  (seat Tau_0)
% 0.49/0.65  (Tau_4 != zenon_X42)
% 0.49/0.65  (Tau_2 != zenon_X62)
% 0.49/0.65  (Tau_8 != zenon_X162)
% 0.49/0.65  (Tau_2 != zenon_X52)
% 0.49/0.65  (Tau_2 != zenon_X71)
% 0.49/0.65  (-. (in zenon_X110 Tau_0))
% 0.49/0.65  (Tau_8 != zenon_X70)
% 0.49/0.65  (Tau_1 != zenon_X19)
% 0.49/0.65  (barrel Tau_2 Tau_3)
% 0.49/0.65  (Tau_2 != zenon_X59)
% 0.49/0.65  (Tau_8 != zenon_X147)
% 0.49/0.65  (Tau_3 != zenon_X115)
% 0.49/0.65  (man Tau_5)
% 0.49/0.65  (-. (front Tau_1))
% 0.49/0.65  (zenon_X148 != Tau_6)
% 0.49/0.65  (-. (event zenon_X96))
% 0.49/0.65  (zenon_X149 != Tau_6)
% 0.49/0.65  (Tau_1 != zenon_X63)
% 0.49/0.65  (Tau_5 != zenon_X160)
% 0.49/0.65  (Tau_5 != zenon_X138)
% 0.49/0.65  (-. (in zenon_X125 Tau_7))
% 0.49/0.65  (zenon_X153 != Tau_6)
% 0.49/0.65  (-. (young zenon_X144))
% 0.49/0.65  (-. (in zenon_X162 Tau_7))
% 0.49/0.65  (-. (in zenon_X102 Tau_7))
% 0.49/0.65  (-. (in zenon_X173 Tau_7))
% 0.49/0.65  (-. (event zenon_X35))
% 0.49/0.65  (lonely Tau_4)
% 0.49/0.65  (Tau_5 != zenon_X53)
% 0.49/0.65  (front Tau_0)
% 0.49/0.65  (-. (in zenon_X174 Tau_7))
% 0.49/0.65  (Tau_2 != zenon_X81)
% 0.49/0.65  (Tau_5 != zenon_X57)
% 0.49/0.65  (-. (in zenon_X62 Tau_1))
% 0.49/0.65  (-. (in zenon_X153 Tau_0))
% 0.49/0.65  (Tau_6 != zenon_X135)
% 0.49/0.65  (zenon_X119 != Tau_6)
% 0.49/0.65  (-. (in zenon_X149 Tau_0))
% 0.49/0.65  *)
% 0.49/0.65  (* NO-PROOF *)
% 0.49/0.65  % SZS status GaveUp
% 0.49/0.65  Number of rewrites on terms: 0
% 0.49/0.65  Number of rewrites on props: 0
% 0.49/0.65  nodes searched: 1960
% 0.49/0.65  max branch formulas: 537
% 0.49/0.65  proof nodes created: 292
% 0.49/0.65  formulas created: 14896
% 0.49/0.65  
%------------------------------------------------------------------------------