↑ Up

Zenon---0.7.1.UNK-Non.f

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

% Computer : n021.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:55:44 EDT 2022

% Result   : Unknown 72.36s 72.57s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.01/0.12  % Problem  : NLP166+1 : TPTP v8.1.0. Released v2.4.0.
% 0.01/0.13  % Command  : run_zenon %s %d
% 0.12/0.34  % Computer : n021.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  : 600
% 0.12/0.34  % DateTime : Thu Jun 30 17:58:58 EDT 2022
% 0.12/0.34  % CPUTime  : 
% 72.36/72.57  Zenon error: exhausted search space without finding a proof
% 72.36/72.57  (* Current branch:
% 72.36/72.57  (-. (cheap T_0 T_1))
% 72.36/72.57  (-. (cheap T_0 T_2))
% 72.36/72.57  (-. (cheap T_0 T_3))
% 72.36/72.57  (T_4 != zenon_X5)
% 72.36/72.57  (zenon_X6 != T_7)
% 72.36/72.57  (-. (old T_0 zenon_X8))
% 72.36/72.57  (-. (lonely T_0 zenon_X5))
% 72.36/72.57  (member T_0 T_9 zenon_X10)
% 72.36/72.57  (member T_0 T_2 zenon_X11)
% 72.36/72.57  (zenon_X10 != T_7)
% 72.36/72.57  (dirty T_0 T_12)
% 72.36/72.57  (two T_0 T_7)
% 72.36/72.57  (member T_0 T_13 zenon_X14)
% 72.36/72.57  (be T_0 T_15 zenon_X16 T_17)
% 72.36/72.57  (-. (cheap zenon_X18 T_19))
% 72.36/72.57  (-. (cheap T_0 T_20))
% 72.36/72.57  (zenon_X21 != T_22)
% 72.36/72.57  (-. (cheap T_0 T_23))
% 72.36/72.57  (-. (two T_0 T_24))
% 72.36/72.57  (T_25 != zenon_X26)
% 72.36/72.57  (group T_0 T_22)
% 72.36/72.57  (zenon_X27 != T_22)
% 72.36/72.57  (member T_0 T_3 zenon_X6)
% 72.36/72.57  (hollywood_placename T_0 T_28)
% 72.36/72.57  (barrel T_0 T_25)
% 72.36/72.57  (placename T_0 T_28)
% 72.36/72.57  (in T_0 T_17 T_29)
% 72.36/72.57  (young T_0 T_30)
% 72.36/72.57  (member zenon_X18 T_31 T_7)
% 72.36/72.57  (zenon_X32 != T_22)
% 72.36/72.57  (T_22 != zenon_X33)
% 72.36/72.57  (down T_0 T_25 T_4)
% 72.36/72.57  (zenon_X34 != T_7)
% 72.36/72.57  (-. (two T_0 T_22))
% 72.36/72.57  (-. (barrel T_0 zenon_X35))
% 72.36/72.57  (zenon_X18 != T_0)
% 72.36/72.57  (-. (lonely T_0 zenon_X36))
% 72.36/72.57  (zenon_X37 != T_7)
% 72.36/72.57  (member T_0 T_38 zenon_X21)
% 72.36/72.57  (T_12 != zenon_X8)
% 72.36/72.57  (zenon_X39 != T_22)
% 72.36/72.57  (old T_0 T_12)
% 72.36/72.57  (T_12 != zenon_X40)
% 72.36/72.57  (zenon_X41 != T_7)
% 72.36/72.57  (-. (placename T_0 zenon_X42))
% 72.36/72.57  (zenon_X37 != T_22)
% 72.36/72.57  (T_7 != zenon_X33)
% 72.36/72.57  (zenon_X43 != T_7)
% 72.36/72.57  (member zenon_X18 T_19 zenon_X27)
% 72.36/72.57  (zenon_X39 != T_7)
% 72.36/72.57  (zenon_X44 != T_22)
% 72.36/72.57  (member T_0 T_45 zenon_X46)
% 72.36/72.57  (T_22 != zenon_X47)
% 72.36/72.57  (-. (old T_0 zenon_X48))
% 72.36/72.57  (-. (member T_0 zenon_X49 T_7))
% 72.36/72.57  (lonely T_0 T_4)
% 72.36/72.57  (-. (placename T_0 zenon_X50))
% 72.36/72.57  (-. (cheap T_0 T_51))
% 72.36/72.57  (member T_0 T_20 zenon_X52)
% 72.36/72.57  (zenon_X53 != T_22)
% 72.36/72.57  (T_24 != zenon_X47)
% 72.36/72.57  (T_28 != zenon_X50)
% 72.36/72.57  (zenon_X11 != T_7)
% 72.36/72.57  (zenon_X44 != T_7)
% 72.36/72.57  (actual_world T_0)
% 72.36/72.57  (-. (cheap T_0 T_30))
% 72.36/72.57  (member T_0 T_51 zenon_X32)
% 72.36/72.57  (-. (placename T_0 zenon_X54))
% 72.36/72.57  (member T_0 T_30 T_7)
% 72.36/72.57  (-. (cheap T_0 T_38))
% 72.36/72.57  (zenon_X46 != T_7)
% 72.36/72.57  (member zenon_X18 T_55 T_22)
% 72.36/72.57  (zenon_X21 != T_7)
% 72.36/72.57  (group T_0 T_24)
% 72.36/72.57  (-. (cheap T_0 T_9))
% 72.36/72.57  (-. (city T_0 T_12))
% 72.36/72.57  (zenon_X32 != T_7)
% 72.36/72.57  (wear T_0 T_56)
% 72.36/72.57  (fellow T_0 T_30)
% 72.36/72.57  (member T_0 T_57 zenon_X58)
% 72.36/72.57  (T_12 != zenon_X48)
% 72.36/72.57  (-. (cheap T_0 T_59))
% 72.36/72.57  (-. (cheap T_0 T_45))
% 72.36/72.57  (zenon_X41 != T_22)
% 72.36/72.57  (present T_0 T_25)
% 72.36/72.57  (event T_0 T_25)
% 72.36/72.57  (-. (cheap T_0 T_60))
% 72.36/72.57  (zenon_X14 != T_7)
% 72.36/72.57  (zenon_X58 != T_22)
% 72.36/72.57  (T_24 != zenon_X61)
% 72.36/72.57  (-. (barrel T_0 zenon_X62))
% 72.36/72.57  (-. (cheap T_0 T_13))
% 72.36/72.57  (-. (old T_0 zenon_X40))
% 72.36/72.57  (-. (group T_0 zenon_X33))
% 72.36/72.57  (-. (cheap T_0 T_63))
% 72.36/72.57  (zenon_X58 != T_7)
% 72.36/72.57  (member T_0 T_60 zenon_X34)
% 72.36/72.57  (zenon_X27 != T_7)
% 72.36/72.57  (member T_0 T_23 zenon_X43)
% 72.36/72.57  (of T_0 T_28 T_29)
% 72.36/72.57  (chevy T_0 T_12)
% 72.36/72.57  (T_29 != T_12)
% 72.36/72.57  (-. (cheap T_0 T_64))
% 72.36/72.57  (street T_0 T_4)
% 72.36/72.57  (member T_0 T_65 zenon_X66)
% 72.36/72.57  (white T_0 T_12)
% 72.36/72.57  (T_4 != zenon_X36)
% 72.36/72.57  (zenon_X67 != T_22)
% 72.36/72.57  (zenon_X46 != T_22)
% 72.36/72.57  (member T_0 T_68 zenon_X39)
% 72.36/72.57  (T_28 != zenon_X42)
% 72.36/72.57  (zenon_X67 != T_7)
% 72.36/72.57  (-. (cheap zenon_X18 T_55))
% 72.36/72.57  (T_7 != T_22)
% 72.36/72.57  (zenon_X10 != T_22)
% 72.36/72.57  (zenon_X66 != T_7)
% 72.36/72.57  (member T_0 T_63 zenon_X44)
% 72.36/72.57  (frontseat T_0 T_29)
% 72.36/72.57  (member T_0 T_59 zenon_X41)
% 72.36/72.57  (event T_0 T_56)
% 72.36/72.57  (city T_0 T_29)
% 72.36/72.57  (-. (cheap T_0 T_68))
% 72.36/72.57  (member T_0 T_64 zenon_X69)
% 72.36/72.57  (patient T_0 T_56 zenon_X70)
% 72.36/72.57  (in T_0 T_25 T_29)
% 72.36/72.57  (zenon_X34 != T_22)
% 72.36/72.57  (-. (cheap T_0 T_71))
% 72.36/72.57  (-. (cheap T_0 T_72))
% 72.36/72.57  (-. (group T_0 zenon_X61))
% 72.36/72.57  (zenon_X53 != T_7)
% 72.36/72.57  (zenon_X73 != T_7)
% 72.36/72.57  (T_22 != zenon_X61)
% 72.36/72.57  (-. (cheap zenon_X18 T_31))
% 72.36/72.57  (T_25 != zenon_X62)
% 72.36/72.57  (zenon_X14 != T_22)
% 72.36/72.57  (-. (member T_0 zenon_X74 T_22))
% 72.36/72.57  (member T_0 T_75 zenon_X53)
% 72.36/72.57  (agent T_0 T_25 T_12)
% 72.36/72.57  (T_7 != zenon_X61)
% 72.36/72.57  (zenon_X69 != T_22)
% 72.36/72.57  (zenon_X66 != T_22)
% 72.36/72.57  (-. (cheap T_0 T_75))
% 72.36/72.57  (-. (group T_0 zenon_X47))
% 72.36/72.57  (T_30 != zenon_X49)
% 72.36/72.57  (T_24 != zenon_X33)
% 72.36/72.57  (zenon_X73 != T_22)
% 72.36/72.57  (zenon_X69 != T_7)
% 72.36/72.57  (agent T_0 T_56 zenon_X76)
% 72.36/72.57  (zenon_X52 != T_22)
% 72.36/72.57  (T_25 != zenon_X35)
% 72.36/72.57  (T_28 != zenon_X54)
% 72.36/72.57  (present T_0 T_56)
% 72.36/72.57  (zenon_X43 != T_22)
% 72.36/72.57  (-. (lonely T_0 zenon_X77))
% 72.36/72.57  (state T_0 T_15)
% 72.36/72.57  (zenon_X52 != T_7)
% 72.36/72.57  (-. (cheap T_0 T_57))
% 72.36/72.57  (zenon_X6 != T_22)
% 72.36/72.57  (-. (cheap T_0 T_65))
% 72.36/72.57  (T_4 != zenon_X77)
% 72.36/72.57  (nonreflexive T_0 T_56)
% 72.36/72.57  (T_7 != T_24)
% 72.36/72.57  (member T_0 T_71 zenon_X67)
% 72.36/72.57  (zenon_X11 != T_22)
% 72.36/72.57  (-. (barrel T_0 zenon_X26))
% 72.36/72.57  (T_7 != zenon_X47)
% 72.36/72.57  (member T_0 T_72 zenon_X73)
% 72.36/72.57  (group T_0 T_7)
% 72.36/72.57  (member T_0 T_1 zenon_X37)
% 72.36/72.57  *)
% 72.36/72.57  (* NO-PROOF *)
% 72.36/72.57  % SZS status GaveUp
% 72.36/72.57  nodes searched: 571
% 72.36/72.57  max branch formulas: 444
% 72.36/72.57  proof nodes created: 39
% 72.36/72.57  formulas created: 7044
% 72.36/72.57  
%------------------------------------------------------------------------------