↑ Up

Zenon---0.7.1.UNK-Non.f

View TPTP
Problem Process solution in
SystemOnTSTP Download .tgz 
%------------------------------------------------------------------------------
% File     : Zenon---0.7.1
% Problem  : NLP221+1 : TPTP v8.1.0. Released v2.4.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_zenon %s %d

% 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  : 600s
% DateTime : Mon Jul 18 05:56:13 EDT 2022

% Result   : Unknown 9.73s 9.88s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.11  % Problem  : NLP221+1 : TPTP v8.1.0. Released v2.4.0.
% 0.03/0.12  % Command  : run_zenon %s %d
% 0.13/0.33  % Computer : n014.cluster.edu
% 0.13/0.33  % Model    : x86_64 x86_64
% 0.13/0.33  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33  % Memory   : 8042.1875MB
% 0.13/0.33  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33  % CPULimit : 300
% 0.13/0.33  % WCLimit  : 600
% 0.13/0.33  % DateTime : Thu Jun 30 20:51:41 EDT 2022
% 0.13/0.33  % CPUTime  : 
% 9.73/9.88  Zenon error: exhausted search space without finding a proof
% 9.73/9.88  (* Current branch:
% 9.73/9.88  (present T_0 T_1)
% 9.73/9.88  (-. (be T_0 T_2 zenon_X3 T_4))
% 9.73/9.88  (-. (be T_0 zenon_X5 T_6 zenon_X7))
% 9.73/9.88  (T_0 != zenon_X8)
% 9.73/9.88  (T_4 != zenon_X9)
% 9.73/9.88  (T_2 != zenon_X10)
% 9.73/9.88  (state T_0 T_2)
% 9.73/9.88  (man T_0 T_4)
% 9.73/9.88  (T_4 != zenon_X11)
% 9.73/9.88  (T_12 != T_6)
% 9.73/9.88  (-. (be T_0 zenon_X13 T_6 zenon_X9))
% 9.73/9.88  (actual_world T_0)
% 9.73/9.88  (-. (be T_0 zenon_X14 T_6 T_4))
% 9.73/9.88  (T_4 != zenon_X15)
% 9.73/9.88  (-. (be T_0 zenon_X16 T_6 T_4))
% 9.73/9.88  (T_2 != zenon_X17)
% 9.73/9.88  (be T_0 T_2 T_6 T_4)
% 9.73/9.88  (-. (be T_0 zenon_X10 zenon_X3 T_4))
% 9.73/9.88  (T_4 != zenon_X18)
% 9.73/9.88  (-. (be T_0 zenon_X17 T_6 T_4))
% 9.73/9.88  (T_19 != zenon_X20)
% 9.73/9.88  (-. (jules_forename T_0 T_21))
% 9.73/9.88  (T_4 != zenon_X22)
% 9.73/9.88  (T_4 != zenon_X23)
% 9.73/9.88  (T_4 != zenon_X24)
% 9.73/9.88  (T_4 != zenon_X25)
% 9.73/9.88  (-. (be T_0 zenon_X26 T_6 zenon_X24))
% 9.73/9.88  (T_2 != zenon_X16)
% 9.73/9.88  (-. (be zenon_X8 zenon_X27 zenon_X28 zenon_X29))
% 9.73/9.88  (T_4 != zenon_X30)
% 9.73/9.88  (T_1 != zenon_X31)
% 9.73/9.88  (-. (be T_0 zenon_X32 T_6 zenon_X33))
% 9.73/9.88  (T_4 != zenon_X34)
% 9.73/9.88  (-. (be T_0 zenon_X35 zenon_X36 zenon_X37))
% 9.73/9.88  (of T_0 T_38 T_6)
% 9.73/9.88  (-. (accessible_world T_0 zenon_X39))
% 9.73/9.88  (-. (be T_0 zenon_X40 T_6 zenon_X15))
% 9.73/9.88  (-. (forename T_0 zenon_X41))
% 9.73/9.88  (T_1 != zenon_X42)
% 9.73/9.88  (-. (be T_0 zenon_X43 T_6 zenon_X11))
% 9.73/9.88  (T_2 != zenon_X44)
% 9.73/9.88  (-. (be T_0 zenon_X45 T_6 T_4))
% 9.73/9.88  (T_19 != zenon_X46)
% 9.73/9.88  (T_6 != zenon_X47)
% 9.73/9.88  (T_6 != zenon_X3)
% 9.73/9.88  (forename T_0 T_38)
% 9.73/9.88  (proposition T_0 T_19)
% 9.73/9.88  (event T_19 T_48)
% 9.73/9.88  (-. (be T_0 zenon_X49 T_6 zenon_X34))
% 9.73/9.88  (-. (be T_0 zenon_X44 zenon_X36 T_4))
% 9.73/9.88  (T_21 != zenon_X50)
% 9.73/9.88  (-. (think_believe_consider T_0 zenon_X51))
% 9.73/9.88  (-. (be T_0 zenon_X52 T_6 zenon_X25))
% 9.73/9.88  (T_2 != zenon_X53)
% 9.73/9.88  (T_38 != zenon_X50)
% 9.73/9.88  (T_38 != zenon_X54)
% 9.73/9.88  (agent T_19 T_48 T_6)
% 9.73/9.88  (T_4 != zenon_X55)
% 9.73/9.88  (T_4 != zenon_X33)
% 9.73/9.88  (-. (accessible_world T_0 zenon_X56))
% 9.73/9.88  (T_4 != zenon_X57)
% 9.73/9.88  (-. (be T_0 zenon_X58 T_6 T_4))
% 9.73/9.88  (T_6 != zenon_X36)
% 9.73/9.88  (-. (be T_0 zenon_X59 T_6 T_4))
% 9.73/9.88  (-. (be T_0 zenon_X60 T_6 zenon_X61))
% 9.73/9.88  (T_2 != zenon_X62)
% 9.73/9.88  (-. (be T_0 zenon_X63 T_6 T_4))
% 9.73/9.88  (-. (be T_0 zenon_X62 T_6 T_4))
% 9.73/9.88  (man T_0 T_12)
% 9.73/9.88  (-. (be T_0 zenon_X64 T_6 T_4))
% 9.73/9.88  (-. (be T_0 zenon_X65 zenon_X47 T_4))
% 9.73/9.88  (event T_19 T_66)
% 9.73/9.88  (T_4 != zenon_X7)
% 9.73/9.88  (theme T_0 T_1 T_19)
% 9.73/9.88  (agent T_0 T_1 T_12)
% 9.73/9.88  (accessible_world T_0 T_19)
% 9.73/9.88  (-. (accessible_world T_0 zenon_X20))
% 9.73/9.88  (T_38 != T_21)
% 9.73/9.88  (event T_0 T_1)
% 9.73/9.88  (T_4 != zenon_X67)
% 9.73/9.88  (T_2 != zenon_X59)
% 9.73/9.88  (-. (be T_0 zenon_X68 T_6 zenon_X55))
% 9.73/9.88  (T_48 != T_1)
% 9.73/9.88  (T_2 != zenon_X69)
% 9.73/9.88  (jules_forename T_0 T_38)
% 9.73/9.88  (-. (be T_0 zenon_X69 T_6 T_4))
% 9.73/9.88  (man T_0 T_6)
% 9.73/9.88  (T_1 != zenon_X51)
% 9.73/9.88  (-. (be T_0 zenon_X70 zenon_X3 zenon_X18))
% 9.73/9.88  (vincent_forename T_0 T_21)
% 9.73/9.88  (-. (think_believe_consider T_0 zenon_X42))
% 9.73/9.88  (-. (be T_0 T_2 zenon_X36 T_4))
% 9.73/9.88  (T_21 != zenon_X41)
% 9.73/9.88  (agent T_19 T_66 zenon_X71)
% 9.73/9.88  (T_2 != zenon_X72)
% 9.73/9.88  (-. (be T_0 zenon_X53 T_6 T_4))
% 9.73/9.88  (-. (be T_0 zenon_X73 T_6 zenon_X74))
% 9.73/9.88  (-. (think_believe_consider T_0 zenon_X31))
% 9.73/9.88  (-. (be T_0 zenon_X75 T_6 zenon_X67))
% 9.73/9.88  (smoke T_19 T_48)
% 9.73/9.88  (-. (be zenon_X8 zenon_X76 zenon_X28 T_4))
% 9.73/9.88  (-. (be T_0 T_2 zenon_X47 T_4))
% 9.73/9.88  (T_2 != zenon_X64)
% 9.73/9.88  (-. (be T_0 zenon_X77 T_6 zenon_X57))
% 9.73/9.88  (T_19 != zenon_X39)
% 9.73/9.88  (of T_0 T_21 T_12)
% 9.73/9.88  (present T_19 T_48)
% 9.73/9.88  (T_19 != zenon_X56)
% 9.73/9.88  (T_4 != zenon_X61)
% 9.73/9.88  (zenon_X71 != T_6)
% 9.73/9.88  (T_2 != zenon_X63)
% 9.73/9.88  (-. (forename T_0 zenon_X54))
% 9.73/9.88  (-. (be T_0 zenon_X78 T_6 zenon_X30))
% 9.73/9.88  (-. (accessible_world T_0 zenon_X46))
% 9.73/9.88  (T_2 != zenon_X79)
% 9.73/9.88  (T_2 != zenon_X58)
% 9.73/9.88  (-. (agent T_0 T_1 T_6))
% 9.73/9.88  (forename T_0 T_21)
% 9.73/9.88  (-. (be T_0 zenon_X72 T_6 T_4))
% 9.73/9.88  (-. (be T_0 zenon_X80 T_6 zenon_X23))
% 9.73/9.88  (-. (be T_0 zenon_X81 zenon_X47 zenon_X22))
% 9.73/9.88  (T_4 != zenon_X37)
% 9.73/9.88  (T_38 != zenon_X41)
% 9.73/9.88  (T_4 != zenon_X29)
% 9.73/9.88  (-. (think_believe_consider T_0 zenon_X82))
% 9.73/9.88  (T_21 != zenon_X54)
% 9.73/9.88  (smoke T_19 T_66)
% 9.73/9.88  (T_1 != zenon_X82)
% 9.73/9.88  (T_2 != zenon_X14)
% 9.73/9.88  (-. (forename T_0 zenon_X50))
% 9.73/9.88  (present T_19 T_66)
% 9.73/9.88  (T_2 != zenon_X45)
% 9.73/9.88  (T_4 != zenon_X74)
% 9.73/9.88  (think_believe_consider T_0 T_1)
% 9.73/9.88  (-. (be T_0 zenon_X79 T_6 T_4))
% 9.73/9.88  (T_2 != zenon_X65)
% 9.73/9.88  *)
% 9.73/9.88  (* NO-PROOF *)
% 9.73/9.88  % SZS status GaveUp
% 9.73/9.88  nodes searched: 433
% 9.73/9.88  max branch formulas: 310
% 9.73/9.88  proof nodes created: 93
% 9.73/9.88  formulas created: 4572
% 9.73/9.88  
%------------------------------------------------------------------------------