↑ Up

Zenon---0.7.1.UNK-Non.f

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

% Computer : n019.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:53:37 EDT 2022

% Result   : Unknown 0.19s 0.61s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12  % Problem  : NLP032+1 : TPTP v8.1.0. Released v2.4.0.
% 0.06/0.13  % Command  : run_zenon %s %d
% 0.12/0.34  % Computer : n019.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 20:48:38 EDT 2022
% 0.12/0.34  % CPUTime  : 
% 0.19/0.61  Zenon error: exhausted search space without finding a proof
% 0.19/0.61  (* Current branch:
% 0.19/0.61  (T_0 != zenon_X1)
% 0.19/0.61  (T_2 != T_3)
% 0.19/0.61  (T_4 != T_5)
% 0.19/0.61  (T_6 != T_7)
% 0.19/0.61  (at T_8 T_9 T_3)
% 0.19/0.61  (-. (with T_8 zenon_X10 T_11))
% 0.19/0.61  (T_4 != T_12)
% 0.19/0.61  (T_0 != zenon_X13)
% 0.19/0.61  (T_14 != zenon_X15)
% 0.19/0.61  (T_16 != T_12)
% 0.19/0.61  (guy T_8 T_17)
% 0.19/0.61  (zenon_X18 != T_19)
% 0.19/0.61  (T_20 != T_21)
% 0.19/0.61  (T_22 != T_5)
% 0.19/0.61  (zenon_X23 != T_24)
% 0.19/0.61  (T_25 != T_26)
% 0.19/0.61  (T_20 != zenon_X27)
% 0.19/0.61  (T_28 != T_5)
% 0.19/0.61  (T_29 != T_30)
% 0.19/0.61  (T_17 != T_21)
% 0.19/0.61  (T_29 != T_31)
% 0.19/0.61  (T_32 != T_30)
% 0.19/0.61  (T_20 != T_33)
% 0.19/0.61  (T_34 != T_33)
% 0.19/0.61  (T_35 != T_2)
% 0.19/0.61  (T_36 != T_37)
% 0.19/0.61  (T_26 != zenon_X38)
% 0.19/0.61  (T_39 != T_40)
% 0.19/0.61  (T_41 != T_14)
% 0.19/0.61  (member T_8 T_29 T_24)
% 0.19/0.61  (T_42 != T_43)
% 0.19/0.61  (T_6 != T_37)
% 0.19/0.61  (T_44 != T_45)
% 0.19/0.61  (T_46 != T_47)
% 0.19/0.61  (-. (at T_8 T_14 T_48))
% 0.19/0.61  (T_20 != T_49)
% 0.19/0.61  (T_50 != T_31)
% 0.19/0.61  (table T_8 T_51)
% 0.19/0.61  (T_52 != T_31)
% 0.19/0.61  (T_53 != T_54)
% 0.19/0.61  (T_55 != T_56)
% 0.19/0.61  (T_34 != zenon_X27)
% 0.19/0.61  (at T_8 T_45 T_43)
% 0.19/0.61  (-. (at T_8 T_0 T_3))
% 0.19/0.61  (T_57 != T_9)
% 0.19/0.61  (T_16 != T_58)
% 0.19/0.61  (T_26 != zenon_X59)
% 0.19/0.61  (-. (with T_8 zenon_X13 T_11))
% 0.19/0.61  (T_45 != zenon_X15)
% 0.19/0.61  (T_60 != T_61)
% 0.19/0.61  (T_60 != T_58)
% 0.19/0.61  (T_60 != T_53)
% 0.19/0.61  (-. (at T_8 T_0 T_51))
% 0.19/0.61  (T_62 != T_33)
% 0.19/0.61  (T_60 != zenon_X63)
% 0.19/0.61  (T_45 != zenon_X64)
% 0.19/0.61  (T_35 != T_51)
% 0.19/0.61  (T_50 != T_54)
% 0.19/0.61  (T_14 != zenon_X65)
% 0.19/0.61  (-. (table T_8 zenon_X66))
% 0.19/0.61  (present T_8 T_0)
% 0.19/0.61  (table T_8 T_67)
% 0.19/0.61  (member T_8 T_22 T_19)
% 0.19/0.61  (member T_8 T_12 zenon_X68)
% 0.19/0.61  (agent T_8 T_45 T_60)
% 0.19/0.61  (T_36 != T_12)
% 0.19/0.61  (T_16 != T_54)
% 0.19/0.61  (T_61 != zenon_X27)
% 0.19/0.61  (T_69 != T_48)
% 0.19/0.61  (T_34 != T_7)
% 0.19/0.61  (T_29 != zenon_X63)
% 0.19/0.61  (-. (with T_8 zenon_X70 T_11))
% 0.19/0.61  (T_39 != T_34)
% 0.19/0.61  (-. (at T_8 T_0 T_67))
% 0.19/0.61  (sit T_8 T_9)
% 0.19/0.61  (-. (at T_8 T_26 T_2))
% 0.19/0.61  (member T_8 T_4 T_24)
% 0.19/0.61  (zenon_X71 != T_72)
% 0.19/0.61  (zenon_X73 != T_17)
% 0.19/0.61  (T_52 != T_21)
% 0.19/0.61  (T_40 != T_47)
% 0.19/0.61  (T_26 != zenon_X74)
% 0.19/0.61  (member T_8 T_39 T_19)
% 0.19/0.61  (T_45 != zenon_X75)
% 0.19/0.61  (-. (young T_8 T_47))
% 0.19/0.61  (T_76 != T_12)
% 0.19/0.61  (zenon_X77 != T_72)
% 0.19/0.61  (-. (at T_8 T_45 T_35))
% 0.19/0.61  (T_36 != T_47)
% 0.19/0.61  (T_55 != T_30)
% 0.19/0.61  (T_14 != zenon_X78)
% 0.19/0.61  (guy T_8 T_40)
% 0.19/0.61  (T_17 != T_12)
% 0.19/0.61  (member zenon_X79 T_80 T_72)
% 0.19/0.61  (T_14 != zenon_X81)
% 0.19/0.61  (T_29 != T_56)
% 0.19/0.61  (T_0 != zenon_X59)
% 0.19/0.61  (T_82 != zenon_X66)
% 0.19/0.61  (T_22 != T_58)
% 0.19/0.61  (T_83 != T_58)
% 0.19/0.61  (T_50 != T_56)
% 0.19/0.61  (T_35 != T_67)
% 0.19/0.61  (at T_8 T_57 T_48)
% 0.19/0.61  (T_17 != T_30)
% 0.19/0.61  (young T_8 T_6)
% 0.19/0.61  (T_41 != T_9)
% 0.19/0.61  (T_40 != T_58)
% 0.19/0.61  (young T_8 T_60)
% 0.19/0.61  (zenon_X68 != T_72)
% 0.19/0.61  (present T_8 T_26)
% 0.19/0.61  (T_67 != T_3)
% 0.19/0.61  (T_4 != T_30)
% 0.19/0.61  (-. (member T_8 zenon_X27 T_19))
% 0.19/0.61  (T_72 != T_19)
% 0.19/0.61  (T_17 != T_20)
% 0.19/0.61  (member T_8 T_33 zenon_X84)
% 0.19/0.61  (T_53 != T_56)
% 0.19/0.61  (guy T_8 T_22)
% 0.19/0.61  (T_52 != T_30)
% 0.19/0.61  (T_4 != T_33)
% 0.19/0.61  (T_60 != T_30)
% 0.19/0.61  (T_45 != zenon_X65)
% 0.19/0.61  (T_17 != T_32)
% 0.19/0.61  (T_60 != T_56)
% 0.19/0.61  (-. (at T_8 T_9 zenon_X66))
% 0.19/0.61  (T_76 != T_30)
% 0.19/0.61  (T_60 != T_12)
% 0.19/0.61  (T_53 != T_37)
% 0.19/0.61  (T_46 != zenon_X63)
% 0.19/0.61  (table T_8 T_48)
% 0.19/0.61  (with T_8 T_9 T_11)
% 0.19/0.61  (guy T_8 T_53)
% 0.19/0.61  (T_85 != T_22)
% 0.19/0.61  (T_61 != T_12)
% 0.19/0.61  (-. (agent T_8 T_45 T_20))
% 0.19/0.61  (member T_8 T_32 T_24)
% 0.19/0.61  (T_40 != T_34)
% 0.19/0.61  (-. (at T_8 T_45 T_86))
% 0.19/0.61  (guy T_8 T_62)
% 0.19/0.61  (-. (with T_8 zenon_X87 T_11))
% 0.19/0.61  (T_29 != T_54)
% 0.19/0.61  (T_32 != T_54)
% 0.19/0.61  (table T_8 T_69)
% 0.19/0.61  (-. (agent T_8 T_26 T_39))
% 0.19/0.61  (T_6 != T_33)
% 0.19/0.61  (T_16 != T_5)
% 0.19/0.61  (T_49 != T_37)
% 0.19/0.61  (T_26 != zenon_X88)
% 0.19/0.61  (T_69 != T_43)
% 0.19/0.61  (T_26 != zenon_X81)
% 0.19/0.61  (-. (hamburger T_8 T_89))
% 0.19/0.61  (T_9 != zenon_X59)
% 0.19/0.61  (zenon_X90 != T_72)
% 0.19/0.61  (at T_8 T_41 T_42)
% 0.19/0.61  (T_83 != T_56)
% 0.19/0.61  (T_16 != T_47)
% 0.19/0.61  (member T_8 T_76 T_24)
% 0.19/0.61  (at T_8 T_91 T_67)
% 0.19/0.61  (T_62 != T_58)
% 0.19/0.61  (zenon_X73 != T_39)
% 0.19/0.61  (T_52 != T_37)
% 0.19/0.61  (-. (with T_8 zenon_X92 T_11))
% 0.19/0.61  (-. (young T_8 T_21))
% 0.19/0.61  (-. (agent T_8 T_0 T_32))
% 0.19/0.61  (T_0 != zenon_X93)
% 0.19/0.61  (T_34 != T_31)
% 0.19/0.61  (T_4 != T_56)
% 0.19/0.61  (T_0 != zenon_X94)
% 0.19/0.61  (T_17 != T_58)
% 0.19/0.61  (zenon_X95 != T_39)
% 0.19/0.61  (-. (with T_8 zenon_X78 T_11))
% 0.19/0.61  (-. (at T_8 T_0 T_43))
% 0.19/0.61  (group T_8 T_24)
% 0.19/0.61  (T_52 != T_58)
% 0.19/0.61  (T_32 != T_37)
% 0.19/0.61  (-. (with T_8 zenon_X15 T_11))
% 0.19/0.61  (T_20 != T_32)
% 0.19/0.61  (T_52 != T_12)
% 0.19/0.61  (T_39 != T_20)
% 0.19/0.61  (T_46 != T_7)
% 0.19/0.61  (-. (young T_8 T_37))
% 0.19/0.61  (T_48 != T_43)
% 0.19/0.61  (T_16 != T_56)
% 0.19/0.61  (group T_8 T_72)
% 0.19/0.61  (T_4 != T_58)
% 0.19/0.61  (T_46 != T_37)
% 0.19/0.61  (T_16 != T_30)
% 0.19/0.61  (T_40 != T_33)
% 0.19/0.61  (T_76 != T_58)
% 0.19/0.61  (T_2 != T_43)
% 0.19/0.61  (T_39 != T_54)
% 0.19/0.61  (T_9 != zenon_X64)
% 0.19/0.61  (T_22 != T_33)
% 0.19/0.61  (T_96 != T_37)
% 0.19/0.61  (-. (at T_8 T_45 T_48))
% 0.19/0.61  (T_55 != T_31)
% 0.19/0.61  (T_40 != T_32)
% 0.19/0.61  (T_62 != T_21)
% 0.19/0.61  (T_6 != T_21)
% 0.19/0.61  (T_96 != T_58)
% 0.19/0.61  (-. (agent T_8 T_14 T_34))
% 0.19/0.61  (-. (with T_8 zenon_X75 T_11))
% 0.19/0.61  (-. (at T_8 T_9 T_42))
% 0.19/0.61  (actual_world T_8)
% 0.19/0.61  (T_17 != zenon_X63)
% 0.19/0.61  (table T_8 T_86)
% 0.19/0.61  (T_14 != zenon_X13)
% 0.19/0.61  (T_69 != T_82)
% 0.19/0.61  (-. (at T_8 T_45 T_3))
% 0.19/0.61  (T_35 != T_3)
% 0.19/0.61  (member T_8 T_60 T_24)
% 0.19/0.61  (T_83 != zenon_X63)
% 0.19/0.61  (T_28 != zenon_X27)
% 0.19/0.61  (zenon_X97 != T_19)
% 0.19/0.61  (T_55 != T_85)
% 0.19/0.61  (T_48 != T_3)
% 0.19/0.61  (T_39 != T_83)
% 0.19/0.61  (T_41 != T_45)
% 0.19/0.61  (T_36 != T_56)
% 0.19/0.61  (T_42 != zenon_X66)
% 0.19/0.61  (T_55 != T_12)
% 0.19/0.61  (young T_8 T_16)
% 0.19/0.61  (young T_8 T_32)
% 0.19/0.61  (-. (young T_8 T_5))
% 0.19/0.61  (T_96 != T_33)
% 0.19/0.61  (T_53 != T_30)
% 0.19/0.61  (event T_8 T_98)
% 0.19/0.61  (T_9 != zenon_X87)
% 0.19/0.61  (T_53 != T_58)
% 0.19/0.61  (present T_8 T_98)
% 0.19/0.61  (T_48 != T_2)
% 0.19/0.61  (-. (with T_8 zenon_X99 T_11))
% 0.19/0.61  (T_86 != T_82)
% 0.19/0.61  (T_60 != T_49)
% 0.19/0.61  (-. (with T_8 zenon_X59 T_11))
% 0.19/0.61  (member zenon_X79 T_100 T_19)
% 0.19/0.61  (T_0 != zenon_X78)
% 0.19/0.61  (T_22 != T_7)
% 0.19/0.61  (T_69 != T_86)
% 0.19/0.61  (T_22 != T_47)
% 0.19/0.61  (T_9 != zenon_X81)
% 0.19/0.61  (T_62 != T_12)
% 0.19/0.61  (T_42 != T_67)
% 0.19/0.61  (event T_8 T_44)
% 0.19/0.61  (T_62 != T_30)
% 0.19/0.61  (-. (at T_8 T_45 T_67))
% 0.19/0.61  (T_45 != zenon_X13)
% 0.19/0.61  (T_57 != T_14)
% 0.19/0.61  (T_96 != T_21)
% 0.19/0.61  (T_29 != T_85)
% 0.19/0.61  (T_0 != zenon_X70)
% 0.19/0.61  (T_34 != T_30)
% 0.19/0.61  (event T_8 T_25)
% 0.19/0.61  (T_26 != zenon_X99)
% 0.19/0.61  (T_45 != zenon_X101)
% 0.19/0.61  (-. (at T_8 T_26 T_35))
% 0.19/0.61  (T_4 != T_54)
% 0.19/0.61  (T_57 != T_26)
% 0.19/0.61  (T_39 != T_32)
% 0.19/0.61  (T_28 != T_54)
% 0.19/0.61  (T_53 != T_7)
% 0.19/0.61  (-. (at T_8 T_9 T_2))
% 0.19/0.61  (T_9 != zenon_X99)
% 0.19/0.61  (T_60 != T_83)
% 0.19/0.61  (member T_8 T_53 T_19)
% 0.19/0.61  (T_35 != T_82)
% 0.19/0.61  (T_45 != zenon_X94)
% 0.19/0.61  (zenon_X71 != T_19)
% 0.19/0.61  (three T_8 T_24)
% 0.19/0.61  (T_45 != zenon_X59)
% 0.19/0.61  (T_96 != T_31)
% 0.19/0.61  (-. (agent T_8 T_26 T_20))
% 0.19/0.61  (T_40 != T_54)
% 0.19/0.61  (T_35 != T_86)
% 0.19/0.61  (T_9 != zenon_X78)
% 0.19/0.61  (-. (at T_8 T_26 T_3))
% 0.19/0.61  (T_14 != zenon_X38)
% 0.19/0.61  (T_85 != T_89)
% 0.19/0.61  (T_25 != T_14)
% 0.19/0.61  (T_60 != T_33)
% 0.19/0.61  (T_45 != zenon_X38)
% 0.19/0.61  (T_49 != T_54)
% 0.19/0.61  (T_20 != T_56)
% 0.19/0.61  (sit T_8 T_14)
% 0.19/0.61  (T_28 != T_7)
% 0.19/0.61  (T_6 != T_30)
% 0.19/0.61  (young T_8 T_61)
% 0.19/0.61  (T_14 != zenon_X94)
% 0.19/0.61  (member T_8 T_37 zenon_X71)
% 0.19/0.61  (T_61 != T_21)
% 0.19/0.61  (T_76 != T_21)
% 0.19/0.61  (T_36 != T_21)
% 0.19/0.61  (T_29 != T_5)
% 0.19/0.61  (table T_8 T_42)
% 0.19/0.61  (T_17 != T_33)
% 0.19/0.61  (T_11 != zenon_X102)
% 0.19/0.61  (T_60 != T_85)
% 0.19/0.61  (with T_8 T_57 zenon_X103)
% 0.19/0.61  (T_69 != T_42)
% 0.19/0.61  (T_50 != T_85)
% 0.19/0.61  (-. (at T_8 T_9 T_51))
% 0.19/0.61  (T_20 != T_85)
% 0.19/0.61  (T_40 != T_37)
% 0.19/0.61  (zenon_X90 != T_24)
% 0.19/0.61  (T_52 != T_47)
% 0.19/0.61  (T_16 != T_31)
% 0.19/0.61  (T_20 != T_7)
% 0.19/0.61  (T_32 != T_21)
% 0.19/0.61  (-. (with T_8 zenon_X65 T_11))
% 0.19/0.61  (-. (agent T_8 T_26 T_60))
% 0.19/0.61  (T_48 != T_35)
% 0.19/0.61  (T_0 != zenon_X92)
% 0.19/0.61  (-. (at T_8 T_0 T_35))
% 0.19/0.61  (T_53 != T_47)
% 0.19/0.61  (T_55 != T_33)
% 0.19/0.61  (member T_8 T_58 zenon_X90)
% 0.19/0.61  (T_26 != zenon_X87)
% 0.19/0.61  (T_34 != T_85)
% 0.19/0.61  (T_62 != T_56)
% 0.19/0.61  (T_45 != T_9)
% 0.19/0.61  (T_20 != T_53)
% 0.19/0.61  (T_4 != T_31)
% 0.19/0.61  (T_69 != T_51)
% 0.19/0.61  (T_29 != T_12)
% 0.19/0.61  (-. (agent T_8 T_45 T_40))
% 0.19/0.61  (T_40 != T_61)
% 0.19/0.61  (T_91 != T_14)
% 0.19/0.61  (T_46 != T_56)
% 0.19/0.61  (-. (hamburger T_8 T_22))
% 0.19/0.61  (T_45 != zenon_X81)
% 0.19/0.61  (T_83 != T_47)
% 0.19/0.61  (T_96 != T_5)
% 0.19/0.61  (zenon_X95 != T_40)
% 0.19/0.61  (guy T_8 T_6)
% 0.19/0.61  (T_49 != T_47)
% 0.19/0.61  (zenon_X84 != T_24)
% 0.19/0.61  (T_46 != T_21)
% 0.19/0.61  (member T_8 T_36 T_19)
% 0.19/0.61  (T_50 != T_58)
% 0.19/0.61  (T_26 != zenon_X65)
% 0.19/0.61  (young T_8 T_36)
% 0.19/0.61  (T_14 != zenon_X104)
% 0.19/0.61  (T_55 != T_58)
% 0.19/0.61  (T_91 != T_45)
% 0.19/0.61  (T_60 != T_47)
% 0.19/0.61  (agent T_8 T_0 T_40)
% 0.19/0.61  (with T_8 T_26 T_11)
% 0.19/0.61  (zenon_X105 != T_24)
% 0.19/0.61  (young T_8 T_40)
% 0.19/0.61  (T_3 != zenon_X66)
% 0.19/0.61  (zenon_X18 != T_24)
% 0.19/0.61  (agent T_8 T_98 T_60)
% 0.19/0.61  (with T_8 T_41 zenon_X103)
% 0.19/0.61  (T_76 != T_37)
% 0.19/0.61  (T_2 != zenon_X66)
% 0.19/0.61  (T_20 != T_58)
% 0.19/0.61  (T_46 != T_54)
% 0.19/0.61  (T_53 != T_21)
% 0.19/0.61  (T_50 != T_30)
% 0.19/0.61  (T_39 != T_17)
% 0.19/0.61  (-. (at T_8 T_26 T_43))
% 0.19/0.61  (guy T_8 T_52)
% 0.19/0.61  (T_20 != T_47)
% 0.19/0.61  (three T_8 T_19)
% 0.19/0.61  (guy T_8 T_32)
% 0.19/0.61  (T_52 != T_56)
% 0.19/0.61  (T_61 != T_31)
% 0.19/0.61  (T_52 != T_85)
% 0.19/0.61  (zenon_X68 != T_24)
% 0.19/0.61  (T_49 != T_33)
% 0.19/0.61  (T_14 != zenon_X88)
% 0.19/0.61  (with T_8 T_44 zenon_X103)
% 0.19/0.61  (T_53 != T_33)
% 0.19/0.61  (T_32 != T_47)
% 0.19/0.61  (T_55 != T_7)
% 0.19/0.61  (T_45 != zenon_X99)
% 0.19/0.61  (T_22 != T_31)
% 0.19/0.61  (zenon_X106 != T_19)
% 0.19/0.61  (T_14 != T_26)
% 0.19/0.61  (T_41 != T_26)
% 0.19/0.61  (T_60 != T_39)
% 0.19/0.61  (T_32 != T_5)
% 0.19/0.61  (zenon_X107 != T_72)
% 0.19/0.61  (guy T_8 T_20)
% 0.19/0.61  (at T_8 T_98 T_35)
% 0.19/0.61  (T_29 != T_7)
% 0.19/0.61  (T_40 != T_56)
% 0.19/0.61  (member T_8 T_7 zenon_X108)
% 0.19/0.61  (zenon_X109 != T_72)
% 0.19/0.61  (T_36 != zenon_X27)
% 0.19/0.61  (T_60 != T_21)
% 0.19/0.61  (T_46 != T_12)
% 0.19/0.61  (T_29 != T_37)
% 0.19/0.61  (zenon_X18 != T_72)
% 0.19/0.61  (T_45 != zenon_X78)
% 0.19/0.61  (guy T_8 T_36)
% 0.19/0.61  (T_40 != T_53)
% 0.19/0.61  (sit T_8 T_0)
% 0.19/0.61  (T_20 != T_31)
% 0.19/0.61  (zenon_X23 != T_19)
% 0.19/0.61  (T_9 != zenon_X13)
% 0.19/0.61  (T_60 != T_31)
% 0.19/0.61  (agent T_8 T_9 T_39)
% 0.19/0.61  (zenon_X68 != T_19)
% 0.19/0.61  (member T_8 T_55 T_24)
% 0.19/0.61  (-. (agent T_8 T_9 T_49))
% 0.19/0.61  (table T_8 T_43)
% 0.19/0.61  (T_60 != T_54)
% 0.19/0.61  (T_46 != T_58)
% 0.19/0.61  (T_9 != zenon_X38)
% 0.19/0.61  (-. (at T_8 T_0 zenon_X66))
% 0.19/0.61  (-. (at T_8 T_0 T_69))
% 0.19/0.61  (young T_8 T_34)
% 0.19/0.61  (T_2 != T_82)
% 0.19/0.61  (T_44 != T_14)
% 0.19/0.61  (-. (agent T_8 T_45 T_17))
% 0.19/0.61  (T_0 != zenon_X110)
% 0.19/0.61  (T_49 != T_5)
% 0.19/0.61  (T_17 != T_83)
% 0.19/0.61  (-. (hamburger zenon_X79 T_80))
% 0.19/0.61  (T_98 != T_9)
% 0.19/0.61  (T_44 != T_9)
% 0.19/0.61  (zenon_X108 != T_24)
% 0.19/0.61  (T_17 != T_47)
% 0.19/0.61  (T_32 != zenon_X63)
% 0.19/0.61  (-. (with T_8 zenon_X104 T_11))
% 0.19/0.61  (T_20 != T_12)
% 0.19/0.61  (young T_8 T_22)
% 0.19/0.61  (T_76 != T_33)
% 0.19/0.61  (-. (at T_8 T_14 T_35))
% 0.19/0.61  (-. (at T_8 T_26 T_42))
% 0.19/0.61  (-. (with T_8 zenon_X88 T_11))
% 0.19/0.61  (-. (at T_8 T_45 T_82))
% 0.19/0.61  (T_26 != zenon_X75)
% 0.19/0.61  (T_83 != T_7)
% 0.19/0.61  (T_32 != T_12)
% 0.19/0.61  (T_53 != T_5)
% 0.19/0.61  (zenon_X108 != T_72)
% 0.19/0.61  (T_0 != zenon_X38)
% 0.19/0.61  (T_42 != T_51)
% 0.19/0.61  (T_0 != zenon_X64)
% 0.19/0.61  (T_50 != T_21)
% 0.19/0.61  (T_17 != T_34)
% 0.19/0.61  (-. (young T_8 T_30))
% 0.19/0.61  (T_60 != T_7)
% 0.19/0.61  (-. (at T_8 T_0 T_2))
% 0.19/0.61  (T_26 != zenon_X104)
% 0.19/0.61  (member T_8 T_47 zenon_X97)
% 0.19/0.61  (-. (at T_8 T_26 T_67))
% 0.19/0.61  (T_50 != zenon_X27)
% 0.19/0.61  (young T_8 T_46)
% 0.19/0.61  (-. (at T_8 T_14 T_42))
% 0.19/0.61  (T_0 != zenon_X10)
% 0.19/0.61  (-. (at T_8 T_14 T_82))
% 0.19/0.61  (T_40 != T_17)
% 0.19/0.61  (T_34 != T_56)
% 0.19/0.61  (T_17 != T_37)
% 0.19/0.61  (-. (hamburger zenon_X79 T_100))
% 0.19/0.61  (T_39 != T_31)
% 0.19/0.61  (T_40 != T_20)
% 0.19/0.61  (T_26 != zenon_X10)
% 0.19/0.61  (young T_8 T_4)
% 0.19/0.61  (member T_8 T_30 zenon_X106)
% 0.19/0.61  (T_67 != T_51)
% 0.19/0.61  (T_16 != T_21)
% 0.19/0.61  (T_22 != zenon_X27)
% 0.19/0.61  (zenon_X106 != T_24)
% 0.19/0.61  (T_67 != T_43)
% 0.19/0.61  (T_46 != T_5)
% 0.19/0.61  (T_26 != zenon_X110)
% 0.19/0.61  (zenon_X109 != T_24)
% 0.19/0.61  (T_14 != zenon_X111)
% 0.19/0.61  (agent T_8 T_57 T_39)
% 0.19/0.61  (T_6 != T_31)
% 0.19/0.61  (-. (at T_8 T_9 T_43))
% 0.19/0.61  (T_25 != T_9)
% 0.19/0.61  (T_0 != zenon_X75)
% 0.19/0.61  (agent T_8 T_25 zenon_X73)
% 0.19/0.61  (at T_8 T_26 T_51)
% 0.19/0.61  (T_34 != T_37)
% 0.19/0.61  (T_20 != T_37)
% 0.19/0.61  (T_0 != zenon_X87)
% 0.19/0.61  (T_83 != T_30)
% 0.19/0.61  (T_19 != T_24)
% 0.19/0.61  (agent T_8 T_44 T_20)
% 0.19/0.61  (T_32 != T_56)
% 0.19/0.61  (T_49 != T_56)
% 0.19/0.61  (T_0 != zenon_X88)
% 0.19/0.61  (T_6 != T_85)
% 0.19/0.61  (sit T_8 T_44)
% 0.19/0.61  (with T_8 T_14 T_11)
% 0.19/0.61  (T_40 != zenon_X27)
% 0.19/0.61  (T_45 != zenon_X87)
% 0.19/0.61  (T_98 != T_14)
% 0.19/0.61  (zenon_X106 != T_72)
% 0.19/0.61  (T_60 != T_17)
% 0.19/0.61  (T_28 != T_31)
% 0.19/0.61  (-. (at T_8 T_0 T_48))
% 0.19/0.61  (T_48 != T_67)
% 0.19/0.61  (member T_8 T_40 T_19)
% 0.19/0.61  (T_96 != T_47)
% 0.19/0.61  (T_40 != T_5)
% 0.19/0.61  (T_50 != T_12)
% 0.19/0.61  (member T_8 T_5 zenon_X112)
% 0.19/0.61  (T_9 != zenon_X110)
% 0.19/0.61  (T_50 != T_37)
% 0.19/0.61  (-. (at T_8 T_14 T_3))
% 0.19/0.61  (T_9 != zenon_X65)
% 0.19/0.61  (event T_8 T_14)
% 0.19/0.61  (T_14 != zenon_X74)
% 0.19/0.61  (T_9 != zenon_X101)
% 0.19/0.61  (T_9 != zenon_X104)
% 0.19/0.61  (T_4 != T_21)
% 0.19/0.61  (T_62 != T_31)
% 0.19/0.61  (guy T_8 T_34)
% 0.19/0.61  (T_42 != T_82)
% 0.19/0.61  (T_57 != T_0)
% 0.19/0.61  (T_45 != zenon_X10)
% 0.19/0.61  (T_76 != T_7)
% 0.19/0.61  (agent T_8 T_14 T_20)
% 0.19/0.61  (T_22 != T_12)
% 0.19/0.61  (zenon_X95 != T_20)
% 0.19/0.61  (T_55 != T_37)
% 0.19/0.61  (-. (at T_8 T_14 T_43))
% 0.19/0.61  (T_6 != T_56)
% 0.19/0.61  (-. (young T_8 T_7))
% 0.19/0.61  (member T_8 T_21 zenon_X23)
% 0.19/0.61  (T_17 != T_31)
% 0.19/0.61  (T_28 != T_21)
% 0.19/0.61  (T_61 != T_54)
% 0.19/0.61  (zenon_X77 != T_24)
% 0.19/0.61  (T_60 != T_32)
% 0.19/0.61  (T_17 != T_7)
% 0.19/0.61  (T_36 != T_33)
% 0.19/0.61  (T_49 != T_31)
% 0.19/0.61  (T_45 != zenon_X92)
% 0.19/0.61  (T_61 != T_33)
% 0.19/0.61  (T_0 != zenon_X65)
% 0.19/0.61  (young T_8 T_17)
% 0.19/0.61  (-. (young T_8 T_12))
% 0.19/0.61  (T_86 != zenon_X66)
% 0.19/0.61  (T_14 != T_0)
% 0.19/0.61  (T_39 != zenon_X27)
% 0.19/0.61  (zenon_X112 != T_24)
% 0.19/0.61  (T_40 != T_31)
% 0.19/0.61  (T_28 != T_30)
% 0.19/0.61  (-. (with T_8 zenon_X1 T_11))
% 0.19/0.61  (guy T_8 T_46)
% 0.19/0.61  (T_50 != T_5)
% 0.19/0.61  (T_0 != T_26)
% 0.19/0.61  (T_39 != T_58)
% 0.19/0.61  (T_45 != zenon_X110)
% 0.19/0.61  (T_67 != zenon_X66)
% 0.19/0.61  (T_32 != T_33)
% 0.19/0.61  (zenon_X103 != T_11)
% 0.19/0.61  (member T_8 T_6 T_19)
% 0.19/0.61  (T_20 != T_83)
% 0.19/0.61  (T_17 != T_61)
% 0.19/0.61  (T_28 != T_12)
% 0.19/0.61  (T_36 != T_7)
% 0.19/0.61  (T_60 != T_40)
% 0.19/0.61  (guy T_8 T_60)
% 0.19/0.61  (event T_8 T_57)
% 0.19/0.61  (T_46 != T_33)
% 0.19/0.61  (member T_8 T_17 T_24)
% 0.19/0.61  (T_61 != T_85)
% 0.19/0.61  (with T_8 T_98 zenon_X103)
% 0.19/0.61  (member T_8 T_83 T_24)
% 0.19/0.61  (member T_8 T_85 T_72)
% 0.19/0.61  (T_45 != zenon_X104)
% 0.19/0.61  (T_17 != T_53)
% 0.19/0.61  (T_40 != T_30)
% 0.19/0.61  (T_36 != T_30)
% 0.19/0.61  (T_41 != T_0)
% 0.19/0.61  (T_55 != T_47)
% 0.19/0.61  (T_39 != T_49)
% 0.19/0.61  (member zenon_X79 T_113 zenon_X107)
% 0.19/0.61  (T_20 != T_61)
% 0.19/0.61  (T_45 != zenon_X74)
% 0.19/0.61  (T_48 != T_51)
% 0.19/0.61  (zenon_X97 != T_72)
% 0.19/0.61  (-. (young T_8 T_56))
% 0.19/0.61  (-. (hamburger T_8 T_46))
% 0.19/0.61  (T_53 != T_12)
% 0.19/0.61  (at T_8 T_25 T_82)
% 0.19/0.61  (-. (at T_8 T_9 T_86))
% 0.19/0.61  (sit T_8 T_91)
% 0.19/0.61  (T_35 != zenon_X66)
% 0.19/0.61  (T_9 != zenon_X111)
% 0.19/0.61  (zenon_X112 != T_72)
% 0.19/0.61  (T_28 != T_56)
% 0.19/0.61  (T_9 != zenon_X93)
% 0.19/0.61  (T_52 != T_54)
% 0.19/0.61  (T_85 != T_46)
% 0.19/0.61  (T_53 != zenon_X27)
% 0.19/0.61  (event T_8 T_45)
% 0.19/0.61  (T_11 != T_22)
% 0.19/0.61  (young T_8 T_96)
% 0.19/0.61  (T_17 != T_54)
% 0.19/0.61  (zenon_X71 != T_24)
% 0.19/0.61  (event T_8 T_26)
% 0.19/0.61  (at T_8 T_0 T_86)
% 0.19/0.61  (T_25 != T_45)
% 0.19/0.61  (T_16 != T_33)
% 0.19/0.61  (T_0 != zenon_X99)
% 0.19/0.61  (young T_8 T_53)
% 0.19/0.61  (at T_8 T_44 T_69)
% 0.19/0.61  (T_17 != T_56)
% 0.19/0.61  (T_3 != T_43)
% 0.19/0.61  (member T_8 T_54 zenon_X18)
% 0.19/0.61  (T_72 != T_24)
% 0.19/0.61  (member T_8 T_16 T_24)
% 0.19/0.61  (-. (at T_8 T_0 T_82))
% 0.19/0.61  (zenon_X84 != T_19)
% 0.19/0.61  (T_14 != zenon_X99)
% 0.19/0.61  (-. (at T_8 T_14 T_69))
% 0.19/0.61  (T_22 != T_30)
% 0.19/0.61  (with T_8 T_25 zenon_X103)
% 0.19/0.61  (member T_8 T_46 T_24)
% 0.19/0.61  (-. (at T_8 T_26 T_82))
% 0.19/0.61  (T_76 != T_31)
% 0.19/0.61  (T_44 != T_0)
% 0.19/0.61  (T_86 != T_43)
% 0.19/0.61  (guy T_8 T_61)
% 0.19/0.61  (T_26 != zenon_X94)
% 0.19/0.61  (guy T_8 T_76)
% 0.19/0.61  (agent T_8 T_91 T_40)
% 0.19/0.61  (T_20 != T_34)
% 0.19/0.61  (T_14 != zenon_X93)
% 0.19/0.61  (T_4 != T_85)
% 0.19/0.61  (-. (with T_8 zenon_X94 T_11))
% 0.19/0.61  (agent T_8 T_26 zenon_X95)
% 0.19/0.61  (T_43 != zenon_X66)
% 0.19/0.61  (T_61 != T_56)
% 0.19/0.61  (zenon_X107 != T_19)
% 0.19/0.61  (zenon_X77 != T_19)
% 0.19/0.61  (member T_8 T_52 T_19)
% 0.19/0.61  (-. (at T_8 T_14 T_67))
% 0.19/0.61  (T_6 != T_58)
% 0.19/0.61  (-. (at T_8 T_9 T_35))
% 0.19/0.61  (T_96 != T_12)
% 0.19/0.61  (T_85 != zenon_X102)
% 0.19/0.61  (present T_8 T_45)
% 0.19/0.61  (T_36 != T_31)
% 0.19/0.61  (T_83 != T_5)
% 0.19/0.61  (-. (at T_8 T_14 T_86))
% 0.19/0.61  (event T_8 T_41)
% 0.19/0.61  (T_39 != T_53)
% 0.19/0.61  (T_16 != T_7)
% 0.19/0.61  (T_26 != zenon_X92)
% 0.19/0.61  (table T_8 T_35)
% 0.19/0.61  (T_20 != T_30)
% 0.19/0.61  (T_29 != T_21)
% 0.19/0.61  (-. (at T_8 T_26 T_86))
% 0.19/0.61  (T_86 != T_3)
% 0.19/0.61  (T_50 != T_33)
% 0.19/0.61  (T_29 != T_33)
% 0.19/0.61  (T_32 != T_7)
% 0.19/0.61  (T_83 != T_12)
% 0.19/0.61  (T_26 != zenon_X15)
% 0.19/0.61  (zenon_X73 != T_20)
% 0.19/0.61  (T_42 != T_2)
% 0.19/0.61  (-. (at T_8 T_26 T_48))
% 0.19/0.61  (T_69 != T_2)
% 0.19/0.61  (T_91 != T_26)
% 0.19/0.61  (T_42 != T_35)
% 0.19/0.61  (T_9 != zenon_X74)
% 0.19/0.61  (-. (with T_8 zenon_X110 T_11))
% 0.19/0.61  (T_50 != T_7)
% 0.19/0.61  (T_26 != zenon_X1)
% 0.19/0.61  (zenon_X112 != T_19)
% 0.19/0.61  (T_20 != T_5)
% 0.19/0.61  (T_14 != zenon_X70)
% 0.19/0.61  (T_48 != zenon_X66)
% 0.19/0.61  (event T_8 T_0)
% 0.19/0.61  (T_42 != T_3)
% 0.19/0.61  (T_40 != T_83)
% 0.19/0.61  (T_39 != T_85)
% 0.19/0.61  (T_61 != T_5)
% 0.19/0.61  (-. (with T_8 zenon_X101 T_11))
% 0.19/0.61  (T_96 != T_85)
% 0.19/0.61  (guy T_8 T_16)
% 0.19/0.61  (T_32 != T_85)
% 0.19/0.61  (T_39 != T_12)
% 0.19/0.61  (T_2 != T_51)
% 0.19/0.61  (T_53 != T_85)
% 0.19/0.61  (T_46 != T_30)
% 0.19/0.61  (young T_8 T_83)
% 0.19/0.61  (present T_8 T_91)
% 0.19/0.61  (T_9 != zenon_X10)
% 0.19/0.61  (T_62 != T_37)
% 0.19/0.61  (young T_8 T_39)
% 0.19/0.61  (young T_8 T_49)
% 0.19/0.61  (T_34 != T_47)
% 0.19/0.61  (T_16 != T_37)
% 0.19/0.61  (young T_8 T_29)
% 0.19/0.61  (-. (at T_8 T_45 T_42))
% 0.19/0.61  (T_36 != T_5)
% 0.19/0.61  (-. (with T_8 zenon_X93 T_11))
% 0.19/0.61  (T_67 != T_82)
% 0.19/0.61  (T_34 != T_58)
% 0.19/0.61  (T_26 != zenon_X78)
% 0.19/0.61  (zenon_X73 != T_60)
% 0.19/0.61  (sit T_8 T_98)
% 0.19/0.61  (T_83 != T_33)
% 0.19/0.61  (T_40 != T_49)
% 0.19/0.61  (-. (with T_8 zenon_X74 T_11))
% 0.19/0.61  (T_49 != T_85)
% 0.19/0.61  (T_61 != T_58)
% 0.19/0.61  (T_96 != T_30)
% 0.19/0.61  (T_14 != zenon_X1)
% 0.19/0.61  (T_36 != T_58)
% 0.19/0.61  (-. (with T_8 zenon_X81 T_11))
% 0.19/0.61  (T_39 != T_37)
% 0.19/0.61  (zenon_X23 != T_72)
% 0.19/0.61  (T_25 != T_0)
% 0.19/0.61  (T_44 != T_26)
% 0.19/0.61  (-. (at T_8 T_9 T_67))
% 0.19/0.61  (T_83 != T_54)
% 0.19/0.61  (present T_8 T_57)
% 0.19/0.61  (T_26 != zenon_X13)
% 0.19/0.61  (T_9 != zenon_X15)
% 0.19/0.61  (T_3 != T_51)
% 0.19/0.61  (-. (with T_8 zenon_X111 T_11))
% 0.19/0.61  (-. (young T_8 T_31))
% 0.19/0.61  (T_11 != T_46)
% 0.19/0.61  (T_40 != T_12)
% 0.19/0.61  (T_29 != T_58)
% 0.19/0.61  (-. (at T_8 T_26 T_69))
% 0.19/0.61  (T_55 != T_21)
% 0.19/0.61  (T_45 != zenon_X93)
% 0.19/0.61  (T_83 != T_31)
% 0.19/0.61  (T_34 != T_5)
% 0.19/0.61  (sit T_8 T_57)
% 0.19/0.61  (agent T_8 T_41 T_17)
% 0.19/0.61  (T_76 != T_56)
% 0.19/0.61  (T_55 != T_54)
% 0.19/0.61  (T_62 != T_7)
% 0.19/0.61  (T_61 != T_37)
% 0.19/0.61  (T_22 != T_54)
% 0.19/0.61  (member T_8 T_11 T_72)
% 0.19/0.61  (T_45 != zenon_X1)
% 0.19/0.61  (guy T_8 T_50)
% 0.19/0.61  (T_86 != T_51)
% 0.19/0.61  (T_76 != T_47)
% 0.19/0.61  (guy T_8 T_96)
% 0.19/0.61  (sit T_8 T_45)
% 0.19/0.61  (young T_8 T_20)
% 0.19/0.61  (T_16 != zenon_X63)
% 0.19/0.61  (T_2 != T_86)
% 0.19/0.61  (T_9 != zenon_X1)
% 0.19/0.61  (T_6 != T_54)
% 0.19/0.61  (-. (agent T_8 T_9 T_53))
% 0.19/0.61  (member T_8 T_20 T_19)
% 0.19/0.61  (guy T_8 T_49)
% 0.19/0.61  (T_26 != zenon_X101)
% 0.19/0.61  (guy T_8 T_4)
% 0.19/0.61  (T_4 != T_7)
% 0.19/0.61  (T_57 != T_45)
% 0.19/0.61  (member T_8 T_34 T_19)
% 0.19/0.61  (T_52 != T_7)
% 0.19/0.61  (-. (at T_8 T_14 T_51))
% 0.19/0.61  (T_60 != T_20)
% 0.19/0.61  (-. (hamburger zenon_X79 T_113))
% 0.19/0.61  (-. (with T_8 zenon_X64 T_11))
% 0.19/0.61  (T_32 != T_58)
% 0.19/0.61  (T_9 != zenon_X88)
% 0.19/0.61  (T_28 != T_47)
% 0.19/0.61  (T_76 != T_5)
% 0.19/0.61  (zenon_X108 != T_19)
% 0.19/0.61  (young T_8 T_76)
% 0.19/0.61  (young T_8 T_55)
% 0.19/0.61  (with T_8 T_91 zenon_X103)
% 0.19/0.61  (T_96 != T_54)
% 0.19/0.61  (T_61 != T_47)
% 0.19/0.61  (-. (member T_8 zenon_X102 T_72))
% 0.19/0.61  (member T_8 T_56 zenon_X109)
% 0.19/0.61  (-. (at T_8 T_9 T_69))
% 0.19/0.61  (zenon_X79 != T_8)
% 0.19/0.61  (guy T_8 T_29)
% 0.19/0.61  (T_69 != T_35)
% 0.19/0.61  (T_4 != T_37)
% 0.19/0.61  (T_96 != zenon_X63)
% 0.19/0.61  (T_14 != T_45)
% 0.19/0.61  (T_9 != zenon_X92)
% 0.19/0.61  (T_96 != T_7)
% 0.19/0.61  (T_91 != T_9)
% 0.19/0.61  (-. (at T_8 T_9 T_48))
% 0.19/0.61  (T_96 != T_56)
% 0.19/0.61  (T_9 != T_26)
% 0.19/0.61  (member T_8 T_50 T_19)
% 0.19/0.61  (present T_8 T_9)
% 0.19/0.61  (T_60 != T_5)
% 0.19/0.61  (group T_8 T_19)
% 0.19/0.61  (T_45 != zenon_X88)
% 0.19/0.61  (T_46 != T_31)
% 0.19/0.61  (T_36 != T_54)
% 0.19/0.61  (T_4 != T_47)
% 0.19/0.61  (zenon_X95 != T_60)
% 0.19/0.61  (at T_8 T_14 T_2)
% 0.19/0.61  (-. (agent T_8 T_14 T_83))
% 0.19/0.61  (T_40 != T_21)
% 0.19/0.61  (T_62 != T_47)
% 0.19/0.61  (T_45 != T_26)
% 0.19/0.61  (T_42 != T_86)
% 0.19/0.61  (T_39 != T_33)
% 0.19/0.61  (T_35 != T_43)
% 0.19/0.61  (T_22 != T_56)
% 0.19/0.61  (T_52 != T_33)
% 0.19/0.61  (table T_8 T_82)
% 0.19/0.61  (T_49 != T_7)
% 0.19/0.61  (member T_8 T_31 zenon_X105)
% 0.19/0.61  (T_98 != T_45)
% 0.19/0.61  (T_67 != T_86)
% 0.19/0.61  (T_14 != zenon_X64)
% 0.19/0.61  (guy T_8 T_83)
% 0.19/0.61  (T_83 != T_21)
% 0.19/0.61  (T_98 != T_0)
% 0.19/0.61  (T_9 != zenon_X94)
% 0.19/0.61  (T_17 != T_5)
% 0.19/0.61  (T_17 != T_49)
% 0.19/0.61  (T_14 != zenon_X10)
% 0.19/0.61  (T_14 != zenon_X101)
% 0.19/0.61  (T_22 != T_37)
% 0.19/0.61  (T_62 != T_5)
% 0.19/0.61  (T_6 != T_5)
% 0.19/0.61  (T_39 != T_61)
% 0.19/0.61  (T_16 != T_85)
% 0.19/0.61  (-. (at T_8 T_9 T_82))
% 0.19/0.61  (with T_8 T_0 T_11)
% 0.19/0.61  (T_4 != zenon_X63)
% 0.19/0.61  (T_39 != T_7)
% 0.19/0.61  (T_76 != T_85)
% 0.19/0.61  (T_14 != zenon_X87)
% 0.19/0.61  (guy T_8 T_28)
% 0.19/0.61  (T_62 != T_54)
% 0.19/0.61  (-. (at T_8 T_0 T_42))
% 0.19/0.61  (present T_8 T_41)
% 0.19/0.61  (zenon_X84 != T_72)
% 0.19/0.61  (T_48 != T_82)
% 0.19/0.61  (T_26 != zenon_X64)
% 0.19/0.61  (-. (at T_8 T_45 T_2))
% 0.19/0.61  (T_49 != T_30)
% 0.19/0.61  (T_26 != zenon_X93)
% 0.19/0.61  (T_76 != zenon_X63)
% 0.19/0.61  (T_0 != T_45)
% 0.19/0.61  (T_45 != zenon_X70)
% 0.19/0.61  (T_32 != T_31)
% 0.19/0.61  (-. (agent T_8 T_0 T_61))
% 0.19/0.61  (T_0 != zenon_X111)
% 0.19/0.61  (T_69 != T_3)
% 0.19/0.61  (-. (young T_8 T_58))
% 0.19/0.61  (-. (at T_8 T_14 zenon_X66))
% 0.19/0.61  (T_55 != zenon_X63)
% 0.19/0.61  (T_51 != zenon_X66)
% 0.19/0.61  (T_34 != T_12)
% 0.19/0.61  (member T_8 T_62 T_19)
% 0.19/0.61  (T_0 != zenon_X74)
% 0.19/0.61  (T_42 != T_48)
% 0.19/0.61  (T_14 != T_9)
% 0.19/0.61  (T_17 != T_85)
% 0.19/0.61  (T_82 != T_43)
% 0.19/0.61  (young T_8 T_62)
% 0.19/0.61  (-. (with T_8 zenon_X38 T_11))
% 0.19/0.61  (T_53 != T_31)
% 0.19/0.61  (T_39 != T_5)
% 0.19/0.61  (T_34 != T_21)
% 0.19/0.61  (T_55 != T_5)
% 0.19/0.61  (-. (member T_8 zenon_X63 T_24))
% 0.19/0.61  (member T_8 T_49 T_24)
% 0.19/0.61  (-. (young T_8 T_54))
% 0.19/0.61  (-. (at T_8 T_45 T_69))
% 0.19/0.61  (T_82 != T_51)
% 0.19/0.61  (T_3 != T_82)
% 0.19/0.61  (-. (at T_8 T_45 T_51))
% 0.19/0.61  (zenon_X90 != T_19)
% 0.19/0.61  (T_61 != T_7)
% 0.19/0.61  (T_48 != T_86)
% 0.19/0.61  (T_83 != T_85)
% 0.19/0.61  (T_39 != T_21)
% 0.19/0.61  (-. (agent T_8 T_26 T_40))
% 0.19/0.61  (T_43 != T_51)
% 0.19/0.61  (zenon_X97 != T_24)
% 0.19/0.61  (present T_8 T_14)
% 0.19/0.61  (event T_8 T_91)
% 0.19/0.61  (T_76 != T_54)
% 0.19/0.61  (T_14 != zenon_X92)
% 0.19/0.61  (member T_8 T_61 T_19)
% 0.19/0.61  (T_36 != T_85)
% 0.19/0.61  (T_6 != T_47)
% 0.19/0.61  (sit T_8 T_26)
% 0.19/0.61  (T_28 != T_85)
% 0.19/0.61  (hamburger T_8 T_11)
% 0.19/0.61  (member T_8 T_96 T_24)
% 0.19/0.61  (T_49 != T_21)
% 0.19/0.61  (T_91 != T_0)
% 0.19/0.61  (T_62 != T_85)
% 0.19/0.61  (T_45 != zenon_X111)
% 0.19/0.61  (table T_8 T_2)
% 0.19/0.61  (T_0 != zenon_X104)
% 0.19/0.61  (T_39 != T_56)
% 0.19/0.61  (guy T_8 T_55)
% 0.19/0.61  (T_98 != T_26)
% 0.19/0.61  (T_6 != T_12)
% 0.19/0.61  (young T_8 T_52)
% 0.19/0.61  (T_28 != T_33)
% 0.19/0.61  (table T_8 T_3)
% 0.19/0.61  (T_49 != zenon_X63)
% 0.19/0.61  (guy T_8 T_39)
% 0.19/0.61  (T_52 != zenon_X27)
% 0.19/0.61  (T_62 != zenon_X27)
% 0.19/0.61  (present T_8 T_25)
% 0.19/0.61  (hamburger T_8 T_85)
% 0.19/0.61  (T_26 != zenon_X111)
% 0.19/0.61  (young T_8 T_28)
% 0.19/0.61  (T_49 != T_12)
% 0.19/0.61  (T_52 != T_5)
% 0.19/0.61  (T_69 != zenon_X66)
% 0.19/0.61  (T_39 != T_30)
% 0.19/0.61  (T_20 != T_54)
% 0.19/0.61  (T_22 != T_21)
% 0.19/0.61  (zenon_X105 != T_72)
% 0.19/0.61  (T_60 != T_34)
% 0.19/0.61  (T_60 != T_37)
% 0.19/0.61  (T_0 != zenon_X101)
% 0.19/0.61  (sit T_8 T_25)
% 0.19/0.61  (zenon_X109 != T_19)
% 0.19/0.61  (member T_8 T_89 zenon_X77)
% 0.19/0.61  (event T_8 T_9)
% 0.19/0.61  (T_34 != T_54)
% 0.19/0.61  (T_11 != T_89)
% 0.19/0.61  (-. (young T_8 T_85))
% 0.19/0.61  (with T_8 T_45 T_11)
% 0.19/0.61  (T_39 != T_47)
% 0.19/0.61  (T_0 != zenon_X81)
% 0.19/0.61  (T_26 != zenon_X70)
% 0.19/0.61  (T_83 != T_37)
% 0.19/0.61  (T_40 != T_85)
% 0.19/0.61  (young T_8 T_50)
% 0.19/0.61  (T_28 != T_58)
% 0.19/0.61  (T_50 != T_47)
% 0.19/0.61  (-. (young T_8 T_33))
% 0.19/0.61  (T_61 != T_30)
% 0.19/0.61  (T_49 != T_58)
% 0.19/0.61  (sit T_8 T_41)
% 0.19/0.61  (T_40 != T_7)
% 0.19/0.61  (T_69 != T_67)
% 0.19/0.61  (T_9 != T_0)
% 0.19/0.61  (present T_8 T_44)
% 0.19/0.61  (T_14 != zenon_X59)
% 0.19/0.61  (T_9 != zenon_X75)
% 0.19/0.61  (T_28 != T_37)
% 0.19/0.61  (T_14 != zenon_X75)
% 0.19/0.61  (zenon_X105 != T_19)
% 0.19/0.61  (T_9 != zenon_X70)
% 0.19/0.61  (T_14 != zenon_X110)
% 0.19/0.61  (T_6 != zenon_X27)
% 0.19/0.61  (T_67 != T_2)
% 0.19/0.61  (T_29 != T_47)
% 0.19/0.61  (member T_8 T_28 T_19)
% 0.19/0.61  (zenon_X73 != T_40)
% 0.19/0.61  (T_0 != zenon_X15)
% 0.19/0.61  *)
% 0.19/0.61  (* NO-PROOF *)
% 0.19/0.61  % SZS status GaveUp
% 0.19/0.61  nodes searched: 2970
% 0.19/0.61  max branch formulas: 1456
% 0.19/0.61  proof nodes created: 534
% 0.19/0.61  formulas created: 9127
% 0.19/0.61  
%------------------------------------------------------------------------------