↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n007.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:10 EDT 2024

% Result   : Unknown 0.52s 0.70s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.09/0.14  % Problem  : NLP032+1 : TPTP v8.2.0. Released v2.4.0.
% 0.09/0.14  % Command  : run_zenon_modulo %d %s
% 0.13/0.35  % Computer : n007.cluster.edu
% 0.13/0.35  % Model    : x86_64 x86_64
% 0.13/0.35  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35  % Memory   : 8042.1875MB
% 0.13/0.35  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35  % CPULimit : 300
% 0.13/0.35  % WCLimit  : 300
% 0.13/0.35  % DateTime : Sat Jun 22 22:25:54 EDT 2024
% 0.13/0.35  % CPUTime  : 
% 0.52/0.69  Zenon error: exhausted search space without finding a proof
% 0.52/0.69  (* Current branch:
% 0.52/0.69  (Tau_70 != Tau_85)
% 0.52/0.69  (Tau_94 != Tau_47)
% 0.52/0.69  (Tau_96 != Tau_63)
% 0.52/0.69  (Tau_78 != Tau_101)
% 0.52/0.69  (Tau_102 != Tau_93)
% 0.52/0.69  (present Tau_0 Tau_45)
% 0.52/0.69  (Tau_82 != Tau_52)
% 0.52/0.69  (Tau_66 != Tau_93)
% 0.52/0.69  (-. (at Tau_0 Tau_53 Tau_25))
% 0.52/0.69  (-. (with Tau_0 zenon_X71 Tau_15))
% 0.52/0.69  (Tau_1 != Tau_23)
% 0.52/0.69  (Tau_110 != Tau_101)
% 0.52/0.69  (-. (at Tau_0 Tau_45 Tau_52))
% 0.52/0.69  (-. (with Tau_0 zenon_X105 Tau_15))
% 0.52/0.69  (Tau_60 != Tau_5)
% 0.52/0.69  (Tau_31 != Tau_64)
% 0.52/0.69  (present Tau_0 Tau_6)
% 0.52/0.69  (Tau_61 != zenon_X71)
% 0.52/0.69  (event Tau_0 Tau_99)
% 0.52/0.69  (zenon_X92 != Tau_3)
% 0.52/0.69  (Tau_110 != Tau_85)
% 0.52/0.69  (member Tau_0 Tau_34 Tau_3)
% 0.52/0.69  (Tau_91 != Tau_53)
% 0.52/0.69  (Tau_45 != zenon_X41)
% 0.52/0.69  (Tau_80 != Tau_85)
% 0.52/0.69  (Tau_75 != Tau_26)
% 0.52/0.69  (group Tau_0 Tau_1)
% 0.52/0.69  (zenon_X24 != Tau_21)
% 0.52/0.69  (Tau_40 != Tau_109)
% 0.52/0.69  (Tau_104 != Tau_93)
% 0.52/0.69  (zenon_X2 != Tau_15)
% 0.52/0.69  (Tau_52 != Tau_44)
% 0.52/0.69  (member Tau_0 Tau_18 zenon_X17)
% 0.52/0.69  (-. (at Tau_0 Tau_37 Tau_52))
% 0.52/0.69  (Tau_53 != zenon_X22)
% 0.52/0.69  (Tau_104 != Tau_39)
% 0.52/0.69  (zenon_X13 != Tau_23)
% 0.52/0.69  (zenon_X17 != Tau_23)
% 0.52/0.69  (Tau_60 != Tau_25)
% 0.52/0.69  (Tau_104 != Tau_18)
% 0.52/0.69  (at Tau_0 Tau_26 Tau_25)
% 0.52/0.69  (Tau_52 != Tau_5)
% 0.52/0.69  (Tau_88 != Tau_109)
% 0.52/0.69  (Tau_56 != Tau_39)
% 0.52/0.69  (Tau_88 != Tau_18)
% 0.52/0.69  (-. (at Tau_0 Tau_26 Tau_44))
% 0.52/0.69  (Tau_45 != zenon_X22)
% 0.52/0.69  (sit Tau_0 Tau_6)
% 0.52/0.69  (-. (with Tau_0 zenon_X35 Tau_15))
% 0.52/0.69  (Tau_37 != zenon_X51)
% 0.52/0.69  (-. (with Tau_0 zenon_X81 Tau_15))
% 0.52/0.69  (Tau_44 != Tau_25)
% 0.52/0.69  (Tau_106 != Tau_74)
% 0.52/0.69  (Tau_28 != Tau_85)
% 0.52/0.69  (Tau_28 != Tau_93)
% 0.52/0.69  (young Tau_0 Tau_80)
% 0.52/0.69  (member Tau_0 Tau_101 zenon_X100)
% 0.52/0.69  (Tau_75 != Tau_37)
% 0.52/0.69  (Tau_61 != zenon_X57)
% 0.52/0.69  (Tau_58 != Tau_30)
% 0.52/0.69  (Tau_75 != Tau_45)
% 0.52/0.69  (member Tau_0 Tau_77 zenon_X76)
% 0.52/0.69  (Tau_66 != Tau_63)
% 0.52/0.69  (guy Tau_0 Tau_102)
% 0.52/0.69  (Tau_70 != Tau_93)
% 0.52/0.69  (Tau_5 != zenon_X16)
% 0.52/0.69  (Tau_25 != zenon_X16)
% 0.52/0.69  (Tau_83 != Tau_53)
% 0.52/0.69  (Tau_21 != Tau_70)
% 0.52/0.69  (Tau_28 != Tau_101)
% 0.52/0.69  (member Tau_0 Tau_40 Tau_23)
% 0.52/0.69  (table Tau_0 Tau_25)
% 0.52/0.69  (Tau_80 != zenon_X7)
% 0.52/0.69  (guy Tau_0 Tau_78)
% 0.52/0.69  (Tau_45 != zenon_X87)
% 0.52/0.69  (member Tau_0 Tau_56 Tau_23)
% 0.52/0.69  (three Tau_0 Tau_23)
% 0.52/0.69  (zenon_X17 != Tau_3)
% 0.52/0.69  (Tau_64 != Tau_63)
% 0.52/0.69  (Tau_86 != Tau_109)
% 0.52/0.69  (young Tau_0 Tau_56)
% 0.52/0.69  (-. (at Tau_0 Tau_37 Tau_44))
% 0.52/0.69  (zenon_X84 != Tau_23)
% 0.52/0.69  (-. (young Tau_0 Tau_30))
% 0.52/0.69  (Tau_61 != zenon_X22)
% 0.52/0.69  (Tau_72 != Tau_69)
% 0.52/0.69  (Tau_99 != Tau_45)
% 0.52/0.69  (member zenon_X9 Tau_12 Tau_1)
% 0.52/0.69  (zenon_X68 != Tau_3)
% 0.52/0.69  (Tau_34 != Tau_47)
% 0.52/0.69  (Tau_64 != Tau_109)
% 0.52/0.69  (Tau_50 != Tau_47)
% 0.52/0.69  (Tau_98 != Tau_44)
% 0.52/0.69  (Tau_58 != Tau_109)
% 0.52/0.69  (Tau_36 != Tau_25)
% 0.52/0.69  (present Tau_0 Tau_99)
% 0.52/0.69  (Tau_88 != Tau_93)
% 0.52/0.69  (Tau_45 != zenon_X71)
% 0.52/0.69  (Tau_106 != Tau_82)
% 0.52/0.69  (Tau_70 != Tau_39)
% 0.52/0.69  (member Tau_0 Tau_96 Tau_3)
% 0.52/0.69  (Tau_37 != zenon_X97)
% 0.52/0.69  (Tau_75 != Tau_53)
% 0.52/0.69  (Tau_64 != Tau_47)
% 0.52/0.69  (Tau_34 != Tau_72)
% 0.52/0.69  (-. (with Tau_0 zenon_X43 Tau_15))
% 0.52/0.69  (Tau_42 != Tau_18)
% 0.52/0.69  (Tau_56 != Tau_101)
% 0.52/0.69  (with Tau_0 Tau_6 zenon_X2)
% 0.52/0.69  (Tau_56 != zenon_X27)
% 0.52/0.69  (Tau_48 != Tau_101)
% 0.52/0.69  (guy Tau_0 Tau_21)
% 0.52/0.69  (Tau_53 != Tau_61)
% 0.52/0.69  (Tau_80 != Tau_47)
% 0.52/0.69  (zenon_X108 != Tau_23)
% 0.52/0.69  (guy Tau_0 Tau_48)
% 0.52/0.69  (Tau_78 != Tau_85)
% 0.52/0.69  (Tau_40 != Tau_77)
% 0.52/0.69  (Tau_21 != Tau_85)
% 0.52/0.69  (Tau_88 != zenon_X7)
% 0.52/0.69  (Tau_70 != Tau_69)
% 0.52/0.69  (-. (young Tau_0 Tau_39))
% 0.52/0.69  (Tau_112 != Tau_85)
% 0.52/0.69  (Tau_45 != zenon_X35)
% 0.52/0.69  (Tau_28 != Tau_77)
% 0.52/0.69  (Tau_94 != zenon_X27)
% 0.52/0.69  (Tau_72 != Tau_93)
% 0.52/0.69  (-. (at Tau_0 Tau_61 Tau_5))
% 0.52/0.69  (member Tau_0 Tau_88 Tau_3)
% 0.52/0.69  (event Tau_0 Tau_107)
% 0.52/0.69  (Tau_106 != Tau_36)
% 0.52/0.69  (Tau_37 != zenon_X57)
% 0.52/0.69  (Tau_1 != Tau_3)
% 0.52/0.69  (guy Tau_0 Tau_66)
% 0.52/0.69  (Tau_20 != Tau_85)
% 0.52/0.69  (Tau_37 != zenon_X89)
% 0.52/0.69  (Tau_70 != Tau_30)
% 0.52/0.69  (Tau_26 != zenon_X113)
% 0.52/0.69  (Tau_34 != Tau_66)
% 0.52/0.69  (Tau_104 != Tau_30)
% 0.52/0.69  (table Tau_0 Tau_82)
% 0.52/0.69  (member Tau_0 Tau_19 Tau_1)
% 0.52/0.69  (Tau_72 != Tau_19)
% 0.52/0.69  (Tau_58 != Tau_101)
% 0.52/0.69  (Tau_64 != Tau_55)
% 0.52/0.69  (Tau_98 != Tau_82)
% 0.52/0.69  (event Tau_0 Tau_26)
% 0.52/0.69  (group Tau_0 Tau_3)
% 0.52/0.69  (table Tau_0 Tau_44)
% 0.52/0.69  (Tau_42 != Tau_58)
% 0.52/0.69  (-. (young Tau_0 Tau_77))
% 0.52/0.69  (zenon_X4 != Tau_31)
% 0.52/0.69  (Tau_112 != Tau_63)
% 0.52/0.69  (Tau_20 != Tau_39)
% 0.52/0.69  (Tau_106 != Tau_52)
% 0.52/0.69  (Tau_112 != Tau_77)
% 0.52/0.69  (Tau_61 != zenon_X97)
% 0.52/0.69  (Tau_94 != Tau_30)
% 0.52/0.69  (-. (at Tau_0 Tau_37 Tau_5))
% 0.52/0.69  (guy Tau_0 Tau_94)
% 0.52/0.69  (Tau_42 != Tau_55)
% 0.52/0.69  (-. (at Tau_0 Tau_26 Tau_90))
% 0.52/0.69  (Tau_45 != zenon_X32)
% 0.52/0.69  (member Tau_0 Tau_102 Tau_23)
% 0.52/0.69  (Tau_44 != Tau_36)
% 0.52/0.69  (Tau_102 != Tau_63)
% 0.52/0.69  (Tau_48 != Tau_63)
% 0.52/0.69  (Tau_104 != Tau_55)
% 0.52/0.69  (with Tau_0 Tau_91 zenon_X2)
% 0.52/0.69  (Tau_34 != Tau_58)
% 0.52/0.69  (Tau_6 != Tau_45)
% 0.52/0.69  (Tau_86 != Tau_39)
% 0.52/0.69  (young Tau_0 Tau_72)
% 0.52/0.69  (agent Tau_0 Tau_26 zenon_X24)
% 0.52/0.69  (-. (agent Tau_0 Tau_37 Tau_21))
% 0.52/0.69  (member Tau_0 Tau_55 zenon_X54)
% 0.52/0.69  (-. (at Tau_0 Tau_61 Tau_52))
% 0.52/0.69  (Tau_102 != Tau_47)
% 0.52/0.69  (Tau_96 != Tau_101)
% 0.52/0.69  (agent Tau_0 Tau_45 Tau_34)
% 0.52/0.69  (present Tau_0 Tau_83)
% 0.52/0.69  (-. (at Tau_0 Tau_61 Tau_25))
% 0.52/0.69  (-. (at Tau_0 Tau_61 Tau_90))
% 0.52/0.69  (Tau_110 != Tau_30)
% 0.52/0.69  (zenon_X76 != Tau_23)
% 0.52/0.69  (Tau_31 != Tau_56)
% 0.52/0.69  (Tau_91 != Tau_61)
% 0.52/0.69  (Tau_37 != zenon_X113)
% 0.52/0.69  (Tau_34 != Tau_55)
% 0.52/0.69  (Tau_66 != Tau_30)
% 0.52/0.69  (zenon_X108 != Tau_3)
% 0.52/0.69  (Tau_45 != zenon_X65)
% 0.52/0.69  (Tau_26 != zenon_X73)
% 0.52/0.69  (Tau_37 != zenon_X73)
% 0.52/0.69  (Tau_82 != Tau_5)
% 0.52/0.69  (-. (at Tau_0 Tau_45 Tau_25))
% 0.52/0.69  (Tau_6 != Tau_61)
% 0.52/0.69  (Tau_75 != Tau_61)
% 0.52/0.69  (Tau_74 != Tau_52)
% 0.52/0.69  (-. (with Tau_0 zenon_X49 Tau_15))
% 0.52/0.69  (zenon_X108 != Tau_1)
% 0.52/0.69  (Tau_90 != Tau_44)
% 0.52/0.69  (with Tau_0 Tau_26 Tau_15)
% 0.52/0.69  (-. (with Tau_0 zenon_X51 Tau_15))
% 0.52/0.69  (-. (agent Tau_0 Tau_53 Tau_72))
% 0.52/0.69  (at Tau_0 Tau_37 Tau_36)
% 0.52/0.69  (sit Tau_0 Tau_91)
% 0.52/0.69  (Tau_80 != Tau_101)
% 0.52/0.69  (Tau_48 != Tau_30)
% 0.52/0.69  (Tau_94 != Tau_77)
% 0.52/0.69  (-. (agent Tau_0 Tau_53 Tau_70))
% 0.52/0.69  (at Tau_0 Tau_99 Tau_98)
% 0.52/0.69  (Tau_94 != Tau_101)
% 0.52/0.69  (sit Tau_0 Tau_75)
% 0.52/0.69  (-. (with Tau_0 zenon_X32 Tau_15))
% 0.52/0.69  (Tau_107 != Tau_26)
% 0.52/0.69  (sit Tau_0 Tau_53)
% 0.52/0.69  (with Tau_0 Tau_83 zenon_X2)
% 0.52/0.69  (young Tau_0 Tau_42)
% 0.52/0.69  (Tau_50 != Tau_55)
% 0.52/0.69  (guy Tau_0 Tau_88)
% 0.52/0.69  (young Tau_0 Tau_40)
% 0.52/0.69  (Tau_42 != Tau_93)
% 0.52/0.69  (Tau_53 != zenon_X49)
% 0.52/0.69  (-. (with Tau_0 zenon_X103 Tau_15))
% 0.52/0.69  (Tau_98 != Tau_36)
% 0.52/0.69  (Tau_20 != Tau_93)
% 0.52/0.69  (zenon_X13 != Tau_3)
% 0.52/0.69  (zenon_X13 != Tau_1)
% 0.52/0.69  (Tau_34 != zenon_X7)
% 0.52/0.69  (-. (at Tau_0 Tau_26 Tau_36))
% 0.52/0.69  (Tau_53 != zenon_X57)
% 0.52/0.69  (-. (with Tau_0 zenon_X73 Tau_15))
% 0.52/0.69  (-. (at Tau_0 Tau_53 zenon_X16))
% 0.52/0.69  (Tau_37 != Tau_45)
% 0.52/0.69  (Tau_70 != Tau_19)
% 0.52/0.69  (zenon_X38 != Tau_23)
% 0.52/0.69  (Tau_34 != Tau_30)
% 0.52/0.69  (member Tau_0 Tau_31 Tau_23)
% 0.52/0.69  (-. (member Tau_0 zenon_X27 Tau_23))
% 0.52/0.69  (-. (at Tau_0 Tau_45 Tau_90))
% 0.52/0.69  (Tau_80 != Tau_55)
% 0.52/0.69  (Tau_86 != Tau_85)
% 0.52/0.69  (Tau_42 != Tau_30)
% 0.52/0.69  (sit Tau_0 Tau_61)
% 0.52/0.69  (Tau_52 != Tau_25)
% 0.52/0.69  (zenon_X46 != Tau_1)
% 0.52/0.69  (-. (with Tau_0 zenon_X89 Tau_15))
% 0.52/0.69  (Tau_37 != zenon_X22)
% 0.52/0.69  (at Tau_0 Tau_107 Tau_106)
% 0.52/0.69  (Tau_96 != Tau_47)
% 0.52/0.69  (zenon_X54 != Tau_23)
% 0.52/0.69  (present Tau_0 Tau_53)
% 0.52/0.69  (Tau_53 != zenon_X89)
% 0.52/0.69  (-. (at Tau_0 Tau_26 Tau_52))
% 0.52/0.69  (Tau_53 != zenon_X95)
% 0.52/0.69  (Tau_50 != Tau_77)
% 0.52/0.69  (Tau_70 != Tau_47)
% 0.52/0.69  (Tau_34 != Tau_64)
% 0.52/0.69  (Tau_45 != zenon_X57)
% 0.52/0.69  (-. (with Tau_0 zenon_X57 Tau_15))
% 0.52/0.69  (-. (at Tau_0 Tau_61 Tau_44))
% 0.52/0.69  (Tau_26 != zenon_X41)
% 0.52/0.69  (zenon_X62 != Tau_23)
% 0.52/0.69  (Tau_26 != zenon_X97)
% 0.52/0.69  (Tau_98 != zenon_X16)
% 0.52/0.69  (table Tau_0 Tau_36)
% 0.52/0.69  (young Tau_0 Tau_88)
% 0.52/0.69  (guy Tau_0 Tau_58)
% 0.52/0.69  (Tau_19 != Tau_14)
% 0.52/0.69  (-. (agent Tau_0 Tau_37 Tau_40))
% 0.52/0.69  (-. (young Tau_0 Tau_93))
% 0.52/0.69  (Tau_53 != zenon_X67)
% 0.52/0.69  (Tau_37 != zenon_X95)
% 0.52/0.69  (hamburger Tau_0 Tau_19)
% 0.52/0.69  (Tau_61 != zenon_X81)
% 0.52/0.69  (Tau_74 != Tau_60)
% 0.52/0.69  (Tau_26 != zenon_X71)
% 0.52/0.69  (Tau_21 != Tau_47)
% 0.52/0.69  (Tau_96 != zenon_X7)
% 0.52/0.69  (Tau_21 != Tau_93)
% 0.52/0.69  (three Tau_0 Tau_3)
% 0.52/0.69  (Tau_83 != Tau_45)
% 0.52/0.69  (zenon_X24 != Tau_31)
% 0.52/0.69  (Tau_86 != Tau_30)
% 0.52/0.69  (young Tau_0 Tau_86)
% 0.52/0.69  (young Tau_0 Tau_58)
% 0.52/0.69  (agent Tau_0 Tau_61 Tau_21)
% 0.52/0.69  (Tau_78 != Tau_63)
% 0.52/0.69  (Tau_61 != zenon_X32)
% 0.52/0.69  (Tau_28 != Tau_69)
% 0.52/0.69  (guy Tau_0 Tau_96)
% 0.52/0.69  (Tau_88 != Tau_63)
% 0.52/0.69  (young Tau_0 Tau_102)
% 0.52/0.69  (Tau_50 != Tau_63)
% 0.52/0.69  (Tau_42 != zenon_X7)
% 0.52/0.69  (Tau_64 != Tau_85)
% 0.52/0.69  (Tau_80 != Tau_63)
% 0.52/0.69  (Tau_21 != Tau_72)
% 0.52/0.69  (Tau_86 != Tau_55)
% 0.52/0.69  (-. (at Tau_0 Tau_45 Tau_74))
% 0.52/0.69  (Tau_53 != zenon_X87)
% 0.52/0.69  (Tau_37 != zenon_X32)
% 0.52/0.69  (member Tau_0 Tau_21 Tau_3)
% 0.52/0.69  (member Tau_0 Tau_14 zenon_X13)
% 0.52/0.69  (-. (with Tau_0 zenon_X87 Tau_15))
% 0.52/0.69  (-. (young Tau_0 Tau_101))
% 0.52/0.69  (Tau_21 != Tau_18)
% 0.52/0.69  (Tau_99 != Tau_53)
% 0.52/0.69  (Tau_86 != zenon_X27)
% 0.52/0.69  (Tau_104 != zenon_X7)
% 0.52/0.69  (event Tau_0 Tau_37)
% 0.52/0.69  (Tau_26 != zenon_X43)
% 0.52/0.69  (Tau_15 != zenon_X8)
% 0.52/0.69  (young Tau_0 Tau_66)
% 0.52/0.69  (young Tau_0 Tau_78)
% 0.52/0.69  (member Tau_0 Tau_50 Tau_3)
% 0.52/0.69  (-. (agent Tau_0 Tau_61 Tau_66))
% 0.52/0.69  (Tau_20 != Tau_47)
% 0.52/0.69  (Tau_110 != Tau_19)
% 0.52/0.69  (Tau_42 != Tau_69)
% 0.52/0.69  (Tau_72 != Tau_55)
% 0.52/0.69  (with Tau_0 Tau_37 Tau_15)
% 0.52/0.69  (-. (young Tau_0 Tau_63))
% 0.52/0.69  (sit Tau_0 Tau_99)
% 0.52/0.69  (Tau_53 != Tau_45)
% 0.52/0.69  (Tau_20 != Tau_55)
% 0.52/0.69  (Tau_28 != zenon_X27)
% 0.52/0.69  (guy Tau_0 Tau_50)
% 0.52/0.69  (Tau_21 != Tau_63)
% 0.52/0.69  (Tau_78 != Tau_77)
% 0.52/0.69  (Tau_53 != zenon_X111)
% 0.52/0.69  (zenon_X38 != Tau_3)
% 0.52/0.69  (Tau_61 != zenon_X105)
% 0.52/0.69  (-. (with Tau_0 zenon_X59 Tau_15))
% 0.52/0.69  (Tau_40 != Tau_69)
% 0.52/0.69  (Tau_37 != zenon_X43)
% 0.52/0.69  (agent Tau_0 Tau_37 Tau_31)
% 0.52/0.69  (young Tau_0 Tau_31)
% 0.52/0.69  (Tau_45 != zenon_X49)
% 0.52/0.69  (Tau_98 != Tau_60)
% 0.52/0.69  (-. (at Tau_0 Tau_45 zenon_X16))
% 0.52/0.69  (Tau_78 != Tau_69)
% 0.52/0.69  (Tau_42 != Tau_47)
% 0.52/0.69  (-. (agent Tau_0 Tau_45 Tau_56))
% 0.52/0.69  (Tau_70 != zenon_X27)
% 0.52/0.69  (Tau_37 != zenon_X71)
% 0.52/0.69  (event Tau_0 Tau_45)
% 0.52/0.69  (Tau_96 != Tau_39)
% 0.52/0.69  (zenon_X29 != Tau_1)
% 0.52/0.69  (Tau_104 != Tau_19)
% 0.52/0.69  (Tau_58 != Tau_55)
% 0.52/0.69  (Tau_42 != Tau_64)
% 0.52/0.69  (Tau_31 != Tau_69)
% 0.52/0.69  (Tau_58 != Tau_63)
% 0.52/0.69  (Tau_50 != Tau_109)
% 0.52/0.69  (Tau_50 != Tau_30)
% 0.52/0.69  (Tau_64 != Tau_30)
% 0.52/0.69  (zenon_X4 != Tau_34)
% 0.52/0.69  (zenon_X92 != Tau_23)
% 0.52/0.69  (Tau_26 != zenon_X87)
% 0.52/0.69  (agent Tau_0 Tau_75 Tau_21)
% 0.52/0.69  (Tau_42 != Tau_63)
% 0.52/0.69  (Tau_102 != Tau_109)
% 0.52/0.69  (Tau_88 != Tau_101)
% 0.52/0.69  (Tau_20 != Tau_101)
% 0.52/0.69  (Tau_99 != Tau_61)
% 0.52/0.69  (-. (at Tau_0 Tau_61 Tau_98))
% 0.52/0.69  (present Tau_0 Tau_61)
% 0.52/0.69  (Tau_66 != Tau_109)
% 0.52/0.69  (Tau_80 != Tau_39)
% 0.52/0.69  (Tau_58 != Tau_93)
% 0.52/0.69  (Tau_26 != zenon_X95)
% 0.52/0.69  (event Tau_0 Tau_61)
% 0.52/0.69  (Tau_80 != Tau_19)
% 0.52/0.69  (Tau_66 != Tau_101)
% 0.52/0.69  (present Tau_0 Tau_75)
% 0.52/0.69  (Tau_31 != Tau_70)
% 0.52/0.69  (Tau_45 != zenon_X43)
% 0.52/0.69  (event Tau_0 Tau_53)
% 0.52/0.69  (Tau_34 != Tau_40)
% 0.52/0.69  (Tau_61 != zenon_X87)
% 0.52/0.69  (Tau_72 != Tau_85)
% 0.52/0.69  (Tau_110 != Tau_77)
% 0.52/0.69  (Tau_40 != Tau_85)
% 0.52/0.69  (table Tau_0 Tau_5)
% 0.52/0.69  (Tau_96 != Tau_77)
% 0.52/0.69  (Tau_28 != Tau_55)
% 0.52/0.69  (Tau_40 != Tau_66)
% 0.52/0.69  (Tau_48 != Tau_18)
% 0.52/0.69  (Tau_31 != Tau_55)
% 0.52/0.69  (Tau_26 != zenon_X65)
% 0.52/0.69  (young Tau_0 Tau_28)
% 0.52/0.69  (zenon_X68 != Tau_23)
% 0.52/0.69  (Tau_34 != Tau_56)
% 0.52/0.69  (Tau_64 != Tau_18)
% 0.52/0.69  (Tau_40 != Tau_101)
% 0.52/0.69  (-. (at Tau_0 Tau_45 Tau_36))
% 0.52/0.69  (Tau_15 != Tau_28)
% 0.52/0.69  (member Tau_0 Tau_28 Tau_23)
% 0.52/0.69  (Tau_37 != zenon_X49)
% 0.52/0.69  (Tau_94 != Tau_18)
% 0.52/0.69  (Tau_45 != zenon_X81)
% 0.52/0.69  (Tau_80 != Tau_93)
% 0.52/0.69  (Tau_61 != Tau_37)
% 0.52/0.69  (-. (at Tau_0 Tau_45 Tau_82))
% 0.52/0.69  (Tau_56 != Tau_30)
% 0.52/0.69  (Tau_3 != Tau_23)
% 0.52/0.69  (Tau_110 != Tau_18)
% 0.52/0.69  (agent Tau_0 Tau_107 Tau_42)
% 0.52/0.69  (member Tau_0 Tau_63 zenon_X62)
% 0.52/0.69  (Tau_53 != zenon_X73)
% 0.52/0.69  (member Tau_0 Tau_80 Tau_3)
% 0.52/0.69  (Tau_112 != Tau_55)
% 0.52/0.69  (Tau_45 != zenon_X73)
% 0.52/0.69  (Tau_106 != Tau_44)
% 0.52/0.69  (at Tau_0 Tau_75 Tau_74)
% 0.52/0.69  (Tau_96 != Tau_55)
% 0.52/0.69  (Tau_98 != Tau_74)
% 0.52/0.69  (member Tau_0 Tau_93 zenon_X92)
% 0.52/0.69  (Tau_74 != Tau_25)
% 0.52/0.69  (Tau_48 != Tau_93)
% 0.52/0.69  (Tau_90 != Tau_82)
% 0.52/0.69  (Tau_82 != Tau_25)
% 0.52/0.69  (Tau_20 != zenon_X7)
% 0.52/0.69  (zenon_X29 != Tau_23)
% 0.52/0.69  (Tau_90 != Tau_60)
% 0.52/0.69  (Tau_66 != Tau_77)
% 0.52/0.69  (-. (young Tau_0 Tau_47))
% 0.52/0.69  (Tau_19 != Tau_28)
% 0.52/0.69  (Tau_42 != Tau_77)
% 0.52/0.69  (young Tau_0 Tau_34)
% 0.52/0.69  (-. (agent Tau_0 Tau_45 Tau_58))
% 0.52/0.69  (zenon_X100 != Tau_3)
% 0.52/0.69  (member Tau_0 Tau_86 Tau_23)
% 0.52/0.69  (Tau_61 != zenon_X51)
% 0.52/0.69  (young Tau_0 Tau_48)
% 0.52/0.69  (Tau_50 != Tau_39)
% 0.52/0.69  (Tau_56 != Tau_47)
% 0.52/0.69  (Tau_37 != zenon_X105)
% 0.52/0.69  (Tau_42 != Tau_56)
% 0.52/0.69  (Tau_21 != Tau_66)
% 0.52/0.69  (Tau_40 != Tau_70)
% 0.52/0.69  (-. (young Tau_0 Tau_55))
% 0.52/0.69  (young Tau_0 Tau_96)
% 0.52/0.69  (-. (at Tau_0 Tau_61 Tau_36))
% 0.52/0.69  (Tau_74 != zenon_X16)
% 0.52/0.69  (Tau_110 != Tau_63)
% 0.52/0.69  (Tau_37 != zenon_X79)
% 0.52/0.69  (Tau_15 != Tau_20)
% 0.52/0.69  (Tau_91 != Tau_45)
% 0.52/0.69  (Tau_28 != Tau_39)
% 0.52/0.69  (Tau_99 != Tau_37)
% 0.52/0.69  (Tau_26 != zenon_X81)
% 0.52/0.69  (-. (young Tau_0 Tau_109))
% 0.52/0.69  (Tau_60 != Tau_36)
% 0.52/0.69  (Tau_40 != Tau_93)
% 0.52/0.69  (young Tau_0 Tau_70)
% 0.52/0.69  (Tau_110 != Tau_39)
% 0.52/0.69  (Tau_53 != Tau_37)
% 0.52/0.69  (Tau_104 != Tau_85)
% 0.52/0.69  (table Tau_0 Tau_74)
% 0.52/0.69  (-. (at Tau_0 Tau_45 Tau_98))
% 0.52/0.69  (Tau_48 != Tau_85)
% 0.52/0.69  (Tau_64 != Tau_39)
% 0.52/0.69  (Tau_83 != Tau_61)
% 0.52/0.69  (Tau_48 != Tau_109)
% 0.52/0.69  (Tau_20 != Tau_69)
% 0.52/0.69  (-. (table Tau_0 zenon_X16))
% 0.52/0.69  (Tau_61 != zenon_X111)
% 0.52/0.69  (Tau_42 != Tau_72)
% 0.52/0.69  (Tau_102 != Tau_77)
% 0.52/0.69  (Tau_31 != zenon_X27)
% 0.52/0.69  (Tau_102 != Tau_19)
% 0.52/0.69  (Tau_37 != zenon_X81)
% 0.52/0.69  (Tau_64 != Tau_77)
% 0.52/0.69  (Tau_53 != zenon_X35)
% 0.52/0.69  (Tau_37 != zenon_X65)
% 0.52/0.69  (Tau_26 != zenon_X67)
% 0.52/0.69  (Tau_21 != Tau_58)
% 0.52/0.69  (Tau_53 != zenon_X59)
% 0.52/0.69  (-. (hamburger zenon_X9 Tau_33))
% 0.52/0.69  (table Tau_0 Tau_60)
% 0.52/0.69  (Tau_82 != Tau_60)
% 0.52/0.69  (Tau_106 != Tau_98)
% 0.52/0.69  (-. (at Tau_0 Tau_26 Tau_5))
% 0.52/0.69  (guy Tau_0 Tau_34)
% 0.52/0.69  (Tau_106 != Tau_25)
% 0.52/0.69  (Tau_94 != Tau_39)
% 0.52/0.69  (Tau_110 != Tau_69)
% 0.52/0.69  (sit Tau_0 Tau_37)
% 0.52/0.69  (Tau_53 != zenon_X79)
% 0.52/0.69  (Tau_80 != Tau_30)
% 0.52/0.69  (Tau_48 != Tau_19)
% 0.52/0.69  (-. (at Tau_0 Tau_37 Tau_82))
% 0.52/0.69  (Tau_20 != Tau_18)
% 0.52/0.69  (Tau_56 != Tau_109)
% 0.52/0.69  (-. (hamburger Tau_0 Tau_14))
% 0.52/0.69  (Tau_61 != zenon_X73)
% 0.52/0.69  (Tau_83 != Tau_26)
% 0.52/0.69  (Tau_48 != Tau_77)
% 0.52/0.69  (member zenon_X9 Tau_33 Tau_3)
% 0.52/0.69  (Tau_42 != Tau_19)
% 0.52/0.69  (Tau_31 != Tau_18)
% 0.52/0.69  (Tau_52 != zenon_X16)
% 0.52/0.69  (Tau_112 != Tau_47)
% 0.52/0.69  (agent Tau_0 Tau_91 Tau_34)
% 0.52/0.69  (Tau_45 != zenon_X111)
% 0.52/0.69  (-. (agent Tau_0 Tau_61 Tau_64))
% 0.52/0.69  (-. (young Tau_0 Tau_85))
% 0.52/0.69  (guy Tau_0 Tau_28)
% 0.52/0.69  (guy Tau_0 Tau_40)
% 0.52/0.69  (agent Tau_0 Tau_53 Tau_42)
% 0.52/0.69  (zenon_X84 != Tau_1)
% 0.52/0.69  (Tau_61 != zenon_X113)
% 0.52/0.69  (at Tau_0 Tau_91 Tau_90)
% 0.52/0.69  (Tau_61 != zenon_X35)
% 0.52/0.69  (Tau_6 != Tau_26)
% 0.52/0.69  (Tau_96 != Tau_93)
% 0.52/0.69  (Tau_34 != Tau_42)
% 0.52/0.69  (Tau_21 != Tau_42)
% 0.52/0.69  (Tau_42 != Tau_101)
% 0.52/0.69  (Tau_106 != Tau_5)
% 0.52/0.69  (Tau_72 != zenon_X7)
% 0.52/0.69  (Tau_60 != Tau_44)
% 0.52/0.69  (Tau_90 != Tau_25)
% 0.52/0.69  (Tau_94 != Tau_63)
% 0.52/0.69  (zenon_X54 != Tau_3)
% 0.52/0.69  (Tau_40 != Tau_72)
% 0.52/0.69  (-. (with Tau_0 zenon_X113 Tau_15))
% 0.52/0.69  (Tau_48 != Tau_39)
% 0.52/0.69  (member Tau_0 Tau_39 zenon_X38)
% 0.52/0.69  (Tau_40 != Tau_19)
% 0.52/0.69  (Tau_31 != Tau_21)
% 0.52/0.69  (member Tau_0 Tau_64 Tau_23)
% 0.52/0.69  (Tau_45 != zenon_X67)
% 0.52/0.69  (Tau_31 != Tau_34)
% 0.52/0.69  (Tau_72 != Tau_30)
% 0.52/0.69  (-. (hamburger zenon_X9 Tau_11))
% 0.52/0.69  (Tau_104 != Tau_69)
% 0.52/0.69  (Tau_56 != Tau_85)
% 0.52/0.69  (Tau_96 != Tau_85)
% 0.52/0.69  (Tau_88 != Tau_85)
% 0.52/0.69  (-. (with Tau_0 zenon_X79 Tau_15))
% 0.52/0.69  (Tau_31 != Tau_109)
% 0.52/0.69  (group Tau_0 Tau_23)
% 0.52/0.69  (Tau_21 != Tau_39)
% 0.52/0.69  (Tau_56 != Tau_63)
% 0.52/0.69  (Tau_91 != Tau_26)
% 0.52/0.69  (member Tau_0 Tau_69 zenon_X68)
% 0.52/0.69  (-. (hamburger zenon_X9 Tau_12))
% 0.52/0.69  (Tau_60 != zenon_X16)
% 0.52/0.69  (Tau_90 != Tau_5)
% 0.52/0.69  (Tau_26 != zenon_X22)
% 0.52/0.69  (young Tau_0 Tau_94)
% 0.52/0.69  (table Tau_0 Tau_98)
% 0.52/0.69  (Tau_53 != zenon_X65)
% 0.52/0.69  (-. (young Tau_0 Tau_69))
% 0.52/0.69  (Tau_72 != Tau_101)
% 0.52/0.69  (zenon_X4 != Tau_21)
% 0.52/0.69  (member Tau_0 Tau_104 Tau_3)
% 0.52/0.69  (Tau_40 != Tau_58)
% 0.52/0.69  (present Tau_0 Tau_26)
% 0.52/0.69  (-. (at Tau_0 Tau_53 Tau_106))
% 0.52/0.69  (Tau_56 != Tau_69)
% 0.52/0.69  (Tau_72 != Tau_63)
% 0.52/0.69  (Tau_78 != Tau_93)
% 0.52/0.69  (Tau_90 != Tau_36)
% 0.52/0.69  (Tau_34 != Tau_18)
% 0.52/0.69  (Tau_98 != Tau_25)
% 0.52/0.69  (Tau_20 != Tau_77)
% 0.52/0.69  (Tau_15 != Tau_14)
% 0.52/0.69  (Tau_61 != zenon_X79)
% 0.52/0.69  (Tau_21 != Tau_64)
% 0.52/0.69  (Tau_42 != Tau_39)
% 0.52/0.69  (Tau_104 != Tau_63)
% 0.52/0.69  (Tau_50 != zenon_X7)
% 0.52/0.69  (Tau_102 != Tau_39)
% 0.52/0.69  (Tau_34 != Tau_21)
% 0.52/0.69  (-. (at Tau_0 Tau_26 Tau_74))
% 0.52/0.69  (Tau_96 != Tau_19)
% 0.52/0.69  (Tau_112 != Tau_39)
% 0.52/0.69  (Tau_6 != Tau_53)
% 0.52/0.69  (Tau_53 != zenon_X113)
% 0.52/0.69  (Tau_21 != Tau_19)
% 0.52/0.69  (Tau_96 != Tau_18)
% 0.52/0.69  (-. (at Tau_0 Tau_53 Tau_44))
% 0.52/0.69  (Tau_45 != zenon_X51)
% 0.52/0.69  (Tau_37 != zenon_X59)
% 0.52/0.69  (Tau_37 != zenon_X67)
% 0.52/0.69  (-. (at Tau_0 Tau_61 Tau_74))
% 0.52/0.69  (Tau_58 != Tau_85)
% 0.52/0.69  (Tau_112 != zenon_X7)
% 0.52/0.69  (Tau_50 != Tau_18)
% 0.52/0.69  (zenon_X76 != Tau_3)
% 0.52/0.69  (Tau_96 != Tau_109)
% 0.52/0.69  (-. (at Tau_0 Tau_53 Tau_90))
% 0.52/0.69  (Tau_78 != Tau_39)
% 0.52/0.69  (Tau_98 != Tau_90)
% 0.52/0.69  (Tau_53 != zenon_X32)
% 0.52/0.69  (Tau_50 != Tau_101)
% 0.52/0.69  (Tau_21 != Tau_109)
% 0.52/0.69  (Tau_112 != Tau_93)
% 0.52/0.69  (young Tau_0 Tau_50)
% 0.52/0.69  (zenon_X24 != Tau_34)
% 0.52/0.69  (-. (agent Tau_0 Tau_37 Tau_42))
% 0.52/0.69  (-. (at Tau_0 Tau_53 Tau_36))
% 0.52/0.69  (Tau_106 != zenon_X16)
% 0.52/0.69  (Tau_110 != Tau_109)
% 0.52/0.69  (Tau_34 != Tau_70)
% 0.52/0.69  (at Tau_0 Tau_45 Tau_44)
% 0.52/0.69  (Tau_102 != zenon_X27)
% 0.52/0.69  (Tau_42 != Tau_70)
% 0.52/0.69  (Tau_70 != Tau_77)
% 0.52/0.69  (young Tau_0 Tau_112)
% 0.52/0.69  (Tau_34 != Tau_93)
% 0.52/0.69  (Tau_31 != Tau_39)
% 0.52/0.69  (zenon_X29 != Tau_3)
% 0.52/0.69  (Tau_64 != zenon_X27)
% 0.52/0.69  (guy Tau_0 Tau_104)
% 0.52/0.69  (Tau_96 != Tau_69)
% 0.52/0.69  (Tau_61 != zenon_X41)
% 0.52/0.69  (Tau_20 != Tau_63)
% 0.52/0.69  (-. (at Tau_0 Tau_37 Tau_74))
% 0.52/0.69  (Tau_56 != Tau_55)
% 0.52/0.69  (Tau_34 != Tau_39)
% 0.52/0.69  (sit Tau_0 Tau_26)
% 0.52/0.69  (member Tau_0 Tau_42 Tau_3)
% 0.52/0.69  (Tau_50 != Tau_93)
% 0.52/0.69  (guy Tau_0 Tau_72)
% 0.52/0.69  (-. (young Tau_0 Tau_19))
% 0.52/0.69  (member Tau_0 Tau_109 zenon_X108)
% 0.52/0.69  (Tau_83 != Tau_37)
% 0.52/0.69  (Tau_20 != Tau_109)
% 0.52/0.69  (Tau_82 != Tau_74)
% 0.52/0.69  (Tau_88 != Tau_55)
% 0.52/0.69  (Tau_34 != Tau_77)
% 0.52/0.69  (member Tau_0 Tau_48 Tau_23)
% 0.52/0.69  (member Tau_0 Tau_58 Tau_3)
% 0.52/0.69  (at Tau_0 Tau_61 Tau_60)
% 0.52/0.69  (member Tau_0 Tau_85 zenon_X84)
% 0.52/0.69  (Tau_40 != Tau_39)
% 0.52/0.69  (Tau_37 != zenon_X35)
% 0.52/0.69  (Tau_45 != zenon_X103)
% 0.52/0.69  (Tau_78 != Tau_109)
% 0.52/0.69  (-. (agent Tau_0 Tau_26 Tau_31))
% 0.52/0.69  (event Tau_0 Tau_75)
% 0.52/0.69  (Tau_21 != Tau_69)
% 0.52/0.69  (Tau_31 != Tau_66)
% 0.52/0.69  (Tau_94 != Tau_85)
% 0.52/0.69  (zenon_X46 != Tau_23)
% 0.52/0.69  (Tau_53 != zenon_X105)
% 0.52/0.69  (Tau_56 != Tau_77)
% 0.52/0.69  (Tau_26 != zenon_X49)
% 0.52/0.69  (Tau_19 != Tau_20)
% 0.52/0.69  (-. (hamburger Tau_0 Tau_28))
% 0.52/0.69  (zenon_X4 != Tau_42)
% 0.52/0.69  (Tau_37 != zenon_X87)
% 0.52/0.69  (Tau_45 != zenon_X97)
% 0.52/0.69  (with Tau_0 Tau_53 Tau_15)
% 0.52/0.69  (Tau_28 != Tau_63)
% 0.52/0.69  (agent Tau_0 Tau_83 Tau_31)
% 0.52/0.69  (Tau_37 != Tau_26)
% 0.52/0.69  (-. (at Tau_0 Tau_53 Tau_82))
% 0.52/0.69  (-. (hamburger Tau_0 Tau_20))
% 0.52/0.69  (Tau_5 != Tau_25)
% 0.52/0.69  (Tau_94 != Tau_55)
% 0.52/0.69  (Tau_26 != zenon_X51)
% 0.52/0.69  (Tau_112 != Tau_19)
% 0.52/0.69  (member Tau_0 Tau_30 zenon_X29)
% 0.52/0.69  (Tau_26 != zenon_X59)
% 0.52/0.69  (Tau_31 != Tau_101)
% 0.52/0.69  (member zenon_X9 Tau_11 zenon_X10)
% 0.52/0.69  (Tau_40 != Tau_30)
% 0.52/0.69  (present Tau_0 Tau_107)
% 0.52/0.69  (Tau_104 != Tau_77)
% 0.52/0.69  (-. (at Tau_0 Tau_37 Tau_25))
% 0.52/0.69  (sit Tau_0 Tau_45)
% 0.52/0.69  (Tau_21 != Tau_40)
% 0.52/0.69  (Tau_78 != Tau_30)
% 0.52/0.69  (member Tau_0 Tau_110 Tau_23)
% 0.52/0.69  (-. (at Tau_0 Tau_61 Tau_106))
% 0.52/0.69  (-. (agent Tau_0 Tau_26 Tau_42))
% 0.52/0.69  (Tau_48 != Tau_47)
% 0.52/0.69  (Tau_96 != Tau_30)
% 0.52/0.69  (Tau_66 != Tau_39)
% 0.52/0.69  (guy Tau_0 Tau_64)
% 0.52/0.69  (present Tau_0 Tau_91)
% 0.52/0.69  (Tau_70 != Tau_55)
% 0.52/0.69  (Tau_61 != zenon_X43)
% 0.52/0.70  (zenon_X62 != Tau_3)
% 0.52/0.70  (Tau_78 != zenon_X27)
% 0.52/0.70  (-. (at Tau_0 Tau_53 Tau_5))
% 0.52/0.70  (Tau_88 != Tau_69)
% 0.52/0.70  (Tau_53 != zenon_X51)
% 0.52/0.70  (Tau_20 != Tau_30)
% 0.52/0.70  (member Tau_0 Tau_20 Tau_3)
% 0.52/0.70  (zenon_X92 != Tau_1)
% 0.52/0.70  (Tau_45 != zenon_X113)
% 0.52/0.70  (Tau_40 != Tau_55)
% 0.52/0.70  (Tau_86 != Tau_77)
% 0.52/0.70  (Tau_88 != Tau_19)
% 0.52/0.70  (Tau_45 != zenon_X105)
% 0.52/0.70  (Tau_31 != Tau_72)
% 0.52/0.70  (guy Tau_0 Tau_56)
% 0.52/0.70  (Tau_61 != zenon_X103)
% 0.52/0.70  (Tau_110 != Tau_93)
% 0.52/0.70  (event Tau_0 Tau_6)
% 0.52/0.70  (Tau_45 != zenon_X79)
% 0.52/0.70  (Tau_40 != Tau_42)
% 0.52/0.70  (Tau_61 != zenon_X49)
% 0.52/0.70  (Tau_102 != Tau_69)
% 0.52/0.70  (Tau_31 != Tau_47)
% 0.52/0.70  (Tau_102 != Tau_30)
% 0.52/0.70  (member Tau_0 Tau_15 Tau_1)
% 0.52/0.70  (Tau_31 != Tau_77)
% 0.52/0.70  (Tau_21 != Tau_77)
% 0.52/0.70  (Tau_31 != Tau_58)
% 0.52/0.70  (Tau_72 != Tau_77)
% 0.52/0.70  (with Tau_0 Tau_61 Tau_15)
% 0.52/0.70  (-. (at Tau_0 Tau_37 Tau_60))
% 0.52/0.70  (-. (member Tau_0 zenon_X7 Tau_3))
% 0.52/0.70  (-. (at Tau_0 Tau_26 Tau_82))
% 0.52/0.70  (Tau_37 != zenon_X111)
% 0.52/0.70  (Tau_102 != Tau_85)
% 0.52/0.70  (Tau_42 != Tau_109)
% 0.52/0.70  (zenon_X76 != Tau_1)
% 0.52/0.70  (member Tau_0 Tau_78 Tau_23)
% 0.52/0.70  (Tau_31 != Tau_19)
% 0.52/0.70  (Tau_53 != zenon_X41)
% 0.52/0.70  (event Tau_0 Tau_83)
% 0.52/0.70  (Tau_66 != Tau_47)
% 0.52/0.70  (Tau_58 != Tau_69)
% 0.52/0.70  (Tau_94 != Tau_109)
% 0.52/0.70  (Tau_90 != Tau_74)
% 0.52/0.70  (zenon_X10 != Tau_1)
% 0.52/0.70  (Tau_31 != Tau_40)
% 0.52/0.70  (Tau_74 != Tau_36)
% 0.52/0.70  (Tau_74 != Tau_5)
% 0.52/0.70  (Tau_21 != Tau_101)
% 0.52/0.70  (Tau_26 != zenon_X57)
% 0.52/0.70  (Tau_45 != zenon_X59)
% 0.52/0.70  (Tau_88 != Tau_30)
% 0.52/0.70  (-. (at Tau_0 Tau_37 Tau_106))
% 0.52/0.70  (Tau_48 != Tau_69)
% 0.52/0.70  (Tau_21 != Tau_30)
% 0.52/0.70  (Tau_58 != Tau_77)
% 0.52/0.70  (member Tau_0 Tau_47 zenon_X46)
% 0.52/0.70  (Tau_107 != Tau_37)
% 0.52/0.70  (Tau_88 != Tau_39)
% 0.52/0.70  (Tau_26 != zenon_X35)
% 0.52/0.70  (Tau_34 != Tau_63)
% 0.52/0.70  (Tau_90 != Tau_52)
% 0.52/0.70  (-. (member Tau_0 zenon_X8 Tau_1))
% 0.52/0.70  (Tau_66 != zenon_X7)
% 0.52/0.70  (Tau_82 != zenon_X16)
% 0.52/0.70  (-. (at Tau_0 Tau_45 Tau_5))
% 0.52/0.70  (Tau_58 != Tau_19)
% 0.52/0.70  (Tau_107 != Tau_53)
% 0.52/0.70  (Tau_40 != Tau_47)
% 0.52/0.70  (zenon_X100 != Tau_1)
% 0.52/0.70  (Tau_58 != Tau_47)
% 0.52/0.70  (Tau_66 != Tau_18)
% 0.52/0.70  (young Tau_0 Tau_21)
% 0.52/0.70  (Tau_61 != zenon_X95)
% 0.52/0.70  (Tau_26 != zenon_X103)
% 0.52/0.70  (Tau_31 != Tau_85)
% 0.52/0.70  (Tau_112 != Tau_18)
% 0.52/0.70  (guy Tau_0 Tau_112)
% 0.52/0.70  (zenon_X17 != Tau_1)
% 0.52/0.70  (Tau_78 != Tau_18)
% 0.52/0.70  (Tau_86 != Tau_47)
% 0.52/0.70  (Tau_80 != Tau_77)
% 0.52/0.70  (Tau_106 != Tau_60)
% 0.52/0.70  (-. (at Tau_0 Tau_26 Tau_106))
% 0.52/0.70  (Tau_37 != zenon_X41)
% 0.52/0.70  (-. (with Tau_0 zenon_X67 Tau_15))
% 0.52/0.70  (-. (young Tau_0 Tau_18))
% 0.52/0.70  (Tau_45 != Tau_26)
% 0.52/0.70  (Tau_72 != Tau_109)
% 0.52/0.70  (Tau_64 != Tau_69)
% 0.52/0.70  (-. (with Tau_0 zenon_X65 Tau_15))
% 0.52/0.70  (Tau_66 != Tau_19)
% 0.52/0.70  (Tau_66 != Tau_85)
% 0.52/0.70  (-. (at Tau_0 Tau_26 Tau_98))
% 0.52/0.70  (Tau_61 != zenon_X67)
% 0.52/0.70  (Tau_26 != zenon_X105)
% 0.52/0.70  (Tau_50 != Tau_69)
% 0.52/0.70  (Tau_107 != Tau_45)
% 0.52/0.70  (Tau_53 != zenon_X43)
% 0.52/0.70  (Tau_94 != Tau_93)
% 0.52/0.70  (young Tau_0 Tau_64)
% 0.52/0.70  (Tau_102 != Tau_18)
% 0.52/0.70  (-. (at Tau_0 Tau_26 Tau_60))
% 0.52/0.70  (Tau_86 != Tau_69)
% 0.52/0.70  (zenon_X38 != Tau_1)
% 0.52/0.70  (Tau_52 != Tau_36)
% 0.52/0.70  (member Tau_0 Tau_70 Tau_23)
% 0.52/0.70  (Tau_64 != Tau_19)
% 0.52/0.70  (Tau_64 != Tau_101)
% 0.52/0.70  (Tau_28 != Tau_109)
% 0.52/0.70  (Tau_91 != Tau_37)
% 0.52/0.70  (Tau_56 != Tau_18)
% 0.52/0.70  (Tau_50 != Tau_85)
% 0.52/0.70  (Tau_94 != Tau_19)
% 0.52/0.70  (-. (at Tau_0 Tau_37 Tau_98))
% 0.52/0.70  (-. (at Tau_0 Tau_61 zenon_X16))
% 0.52/0.70  (Tau_45 != zenon_X89)
% 0.52/0.70  (Tau_40 != Tau_18)
% 0.52/0.70  (Tau_112 != Tau_101)
% 0.52/0.70  (sit Tau_0 Tau_107)
% 0.52/0.70  (guy Tau_0 Tau_110)
% 0.52/0.70  (-. (agent Tau_0 Tau_26 Tau_21))
% 0.52/0.70  (Tau_72 != Tau_18)
% 0.52/0.70  (Tau_78 != Tau_19)
% 0.52/0.70  (Tau_110 != zenon_X27)
% 0.52/0.70  (Tau_44 != zenon_X16)
% 0.52/0.70  (guy Tau_0 Tau_20)
% 0.52/0.70  (-. (agent Tau_0 Tau_26 Tau_34))
% 0.52/0.70  (-. (at Tau_0 Tau_53 Tau_74))
% 0.52/0.70  (with Tau_0 Tau_45 Tau_15)
% 0.52/0.70  (Tau_66 != Tau_69)
% 0.52/0.70  (-. (with Tau_0 zenon_X111 Tau_15))
% 0.52/0.70  (Tau_42 != Tau_66)
% 0.52/0.70  (Tau_74 != Tau_44)
% 0.52/0.70  (Tau_19 != zenon_X8)
% 0.52/0.70  (Tau_26 != zenon_X79)
% 0.52/0.70  (Tau_110 != Tau_55)
% 0.52/0.70  (-. (with Tau_0 zenon_X22 Tau_15))
% 0.52/0.70  (with Tau_0 Tau_75 zenon_X2)
% 0.52/0.70  (Tau_112 != Tau_109)
% 0.52/0.70  (hamburger Tau_0 Tau_15)
% 0.52/0.70  (Tau_102 != Tau_101)
% 0.52/0.70  (Tau_58 != zenon_X7)
% 0.52/0.70  (Tau_34 != Tau_69)
% 0.52/0.70  (Tau_99 != Tau_26)
% 0.52/0.70  (agent Tau_0 Tau_6 zenon_X4)
% 0.52/0.70  (at Tau_0 Tau_83 Tau_82)
% 0.52/0.70  (Tau_88 != Tau_47)
% 0.52/0.70  (Tau_102 != Tau_55)
% 0.52/0.70  (with Tau_0 Tau_107 zenon_X2)
% 0.52/0.70  (at Tau_0 Tau_6 Tau_5)
% 0.52/0.70  (Tau_61 != zenon_X89)
% 0.52/0.70  (-. (at Tau_0 Tau_53 Tau_98))
% 0.52/0.70  (zenon_X54 != Tau_1)
% 0.52/0.70  (Tau_44 != Tau_5)
% 0.52/0.70  (Tau_21 != zenon_X7)
% 0.52/0.70  (Tau_53 != zenon_X71)
% 0.52/0.70  (young Tau_0 Tau_104)
% 0.52/0.70  (zenon_X4 != Tau_40)
% 0.52/0.70  (Tau_86 != Tau_19)
% 0.52/0.70  (member Tau_0 Tau_72 Tau_3)
% 0.52/0.70  (-. (at Tau_0 Tau_45 Tau_106))
% 0.52/0.70  (guy Tau_0 Tau_86)
% 0.52/0.70  (zenon_X100 != Tau_23)
% 0.52/0.70  (Tau_42 != Tau_85)
% 0.52/0.70  (member Tau_0 Tau_112 Tau_3)
% 0.52/0.70  (Tau_37 != zenon_X103)
% 0.52/0.70  (table Tau_0 Tau_52)
% 0.52/0.70  (zenon_X62 != Tau_1)
% 0.52/0.70  (actual_world Tau_0)
% 0.52/0.70  (Tau_107 != Tau_61)
% 0.52/0.70  (Tau_5 != Tau_36)
% 0.52/0.70  (with Tau_0 Tau_99 zenon_X2)
% 0.52/0.70  (Tau_98 != Tau_52)
% 0.52/0.70  (Tau_28 != Tau_30)
% 0.52/0.70  (table Tau_0 Tau_106)
% 0.52/0.70  (Tau_28 != Tau_18)
% 0.52/0.70  (Tau_28 != Tau_47)
% 0.52/0.70  (-. (at Tau_0 Tau_53 Tau_60))
% 0.52/0.70  (Tau_78 != Tau_55)
% 0.52/0.70  (zenon_X84 != Tau_3)
% 0.52/0.70  (Tau_45 != Tau_61)
% 0.52/0.70  (Tau_31 != Tau_63)
% 0.52/0.70  (Tau_52 != Tau_60)
% 0.52/0.70  (Tau_112 != Tau_69)
% 0.52/0.70  (Tau_31 != Tau_42)
% 0.52/0.70  (Tau_82 != Tau_44)
% 0.52/0.70  (Tau_72 != Tau_39)
% 0.52/0.70  (guy Tau_0 Tau_70)
% 0.52/0.70  (sit Tau_0 Tau_83)
% 0.52/0.70  (Tau_53 != zenon_X97)
% 0.52/0.70  (Tau_40 != Tau_63)
% 0.52/0.70  (Tau_36 != zenon_X16)
% 0.52/0.70  (Tau_72 != Tau_47)
% 0.52/0.70  (Tau_26 != zenon_X32)
% 0.52/0.70  (member Tau_0 Tau_94 Tau_23)
% 0.52/0.70  (Tau_86 != Tau_93)
% 0.52/0.70  (Tau_40 != Tau_64)
% 0.52/0.70  (Tau_26 != zenon_X111)
% 0.52/0.70  (agent Tau_0 Tau_99 Tau_40)
% 0.52/0.70  (event Tau_0 Tau_91)
% 0.52/0.70  (Tau_70 != Tau_109)
% 0.52/0.70  (zenon_X10 != Tau_3)
% 0.52/0.70  (-. (at Tau_0 Tau_45 Tau_60))
% 0.52/0.70  (Tau_48 != Tau_55)
% 0.52/0.70  (Tau_58 != Tau_18)
% 0.52/0.70  (Tau_53 != zenon_X81)
% 0.52/0.70  (Tau_82 != Tau_36)
% 0.52/0.70  (young Tau_0 Tau_20)
% 0.52/0.70  (Tau_80 != Tau_18)
% 0.52/0.70  (Tau_61 != Tau_26)
% 0.52/0.70  (Tau_31 != Tau_30)
% 0.52/0.70  (Tau_45 != zenon_X95)
% 0.52/0.70  (table Tau_0 Tau_90)
% 0.52/0.70  (Tau_6 != Tau_37)
% 0.52/0.70  (Tau_40 != Tau_56)
% 0.52/0.70  (Tau_66 != Tau_55)
% 0.52/0.70  (Tau_80 != Tau_109)
% 0.52/0.70  (Tau_58 != Tau_39)
% 0.52/0.70  (Tau_86 != Tau_63)
% 0.52/0.70  (Tau_86 != Tau_101)
% 0.52/0.70  (Tau_64 != Tau_93)
% 0.52/0.70  (Tau_56 != Tau_19)
% 0.52/0.70  (Tau_56 != Tau_93)
% 0.52/0.70  (Tau_34 != Tau_109)
% 0.52/0.70  (Tau_106 != Tau_90)
% 0.52/0.70  (Tau_70 != Tau_101)
% 0.52/0.70  (guy Tau_0 Tau_31)
% 0.52/0.70  (Tau_40 != zenon_X27)
% 0.52/0.70  (Tau_26 != zenon_X89)
% 0.52/0.70  (zenon_X24 != Tau_42)
% 0.52/0.70  (guy Tau_0 Tau_42)
% 0.52/0.70  (Tau_31 != Tau_93)
% 0.52/0.70  (Tau_34 != Tau_101)
% 0.52/0.70  (zenon_X46 != Tau_3)
% 0.52/0.70  (Tau_53 != Tau_26)
% 0.52/0.70  (zenon_X9 != Tau_0)
% 0.52/0.70  (present Tau_0 Tau_37)
% 0.52/0.70  (Tau_70 != Tau_63)
% 0.52/0.70  (Tau_94 != Tau_69)
% 0.52/0.70  (Tau_34 != Tau_85)
% 0.52/0.70  (-. (with Tau_0 zenon_X95 Tau_15))
% 0.52/0.70  (-. (at Tau_0 Tau_37 Tau_90))
% 0.52/0.70  (Tau_21 != Tau_56)
% 0.52/0.70  (at Tau_0 Tau_53 Tau_52)
% 0.52/0.70  (young Tau_0 Tau_110)
% 0.52/0.70  (Tau_34 != Tau_19)
% 0.52/0.70  (Tau_110 != Tau_47)
% 0.52/0.70  (Tau_21 != Tau_55)
% 0.52/0.70  (Tau_98 != Tau_5)
% 0.52/0.70  (Tau_104 != Tau_101)
% 0.52/0.70  (Tau_112 != Tau_30)
% 0.52/0.70  (Tau_90 != zenon_X16)
% 0.52/0.70  (Tau_88 != Tau_77)
% 0.52/0.70  (Tau_48 != zenon_X27)
% 0.52/0.70  (zenon_X68 != Tau_1)
% 0.52/0.70  (Tau_50 != Tau_19)
% 0.52/0.70  (Tau_104 != Tau_109)
% 0.52/0.70  (Tau_61 != zenon_X65)
% 0.52/0.70  (guy Tau_0 Tau_80)
% 0.52/0.70  (-. (at Tau_0 Tau_61 Tau_82))
% 0.52/0.70  (Tau_80 != Tau_69)
% 0.52/0.70  (Tau_61 != zenon_X59)
% 0.52/0.70  (Tau_53 != zenon_X103)
% 0.52/0.70  (Tau_78 != Tau_47)
% 0.52/0.70  (-. (with Tau_0 zenon_X41 Tau_15))
% 0.52/0.70  (-. (with Tau_0 zenon_X97 Tau_15))
% 0.52/0.70  (member Tau_0 Tau_66 Tau_3)
% 0.52/0.70  (Tau_70 != Tau_18)
% 0.52/0.70  (Tau_86 != Tau_18)
% 0.52/0.70  (Tau_104 != Tau_47)
% 0.52/0.70  *)
% 0.52/0.70  (* NO-PROOF *)
% 0.52/0.70  % SZS status GaveUp
% 0.52/0.70  Number of rewrites on terms: 0
% 0.52/0.70  Number of rewrites on props: 0
% 0.52/0.70  nodes searched: 2852
% 0.52/0.70  max branch formulas: 1413
% 0.52/0.70  proof nodes created: 534
% 0.52/0.70  formulas created: 9126
% 0.52/0.70  
%------------------------------------------------------------------------------