↑ Up

ZenonModulo---0.5.0.UNK-Non.f

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

% Computer : n008.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:02 EDT 2024

% Result   : Unknown 0.91s 1.11s
% Output   : None 
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.04/0.09  % Problem  : MSC016+1 : TPTP v8.2.0. Released v3.5.0.
% 0.04/0.09  % Command  : run_zenon_modulo %d %s
% 0.09/0.29  % Computer : n008.cluster.edu
% 0.09/0.29  % Model    : x86_64 x86_64
% 0.09/0.29  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.29  % Memory   : 8042.1875MB
% 0.09/0.29  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.09/0.29  % CPULimit : 300
% 0.09/0.29  % WCLimit  : 300
% 0.09/0.29  % DateTime : Sun Jun 23 00:42:23 EDT 2024
% 0.09/0.29  % CPUTime  : 
% 0.91/1.11  Zenon error: exhausted search space without finding a proof
% 0.91/1.11  (* Current branch:
% 0.91/1.11  ((g zenon_X0 (e)) != (g (e) (e)))
% 0.91/1.11  ((cow) != zenon_X78)
% 0.91/1.11  (-. (p (a) (lkg) zenon_X88))
% 0.91/1.11  (ld__ (horse) (k))
% 0.91/1.11  ((g (a) (c)) != (d))
% 0.91/1.11  ((b) != zenon_X48)
% 0.91/1.11  ((g (b) (b)) != zenon_X62)
% 0.91/1.11  (-. (p (pig) zenon_X17 (b)))
% 0.91/1.11  (-. (p (g (e) (e)) zenon_X56 (b)))
% 0.91/1.11  ((g (b) (b)) != (pig))
% 0.91/1.11  (ld__ (d) (e))
% 0.91/1.11  ((lilly) != zenon_X57)
% 0.91/1.11  ((d) != (hill))
% 0.91/1.11  ((pig) != zenon_X6)
% 0.91/1.11  ((e) != zenon_X8)
% 0.91/1.11  ((aparna) != zenon_X81)
% 0.91/1.11  ((c) != zenon_X7)
% 0.91/1.11  ((g zenon_X0 (e)) != (c))
% 0.91/1.11  ((k) != (a))
% 0.91/1.11  (-. (p (a) zenon_X80 (k)))
% 0.91/1.11  (-. (ld__ (g (e) (e)) (a)))
% 0.91/1.11  ((e) != zenon_X56)
% 0.91/1.11  ((e) != zenon_X57)
% 0.91/1.11  (ld__ (d) (a))
% 0.91/1.11  ((g (b) (b)) != zenon_X55)
% 0.91/1.11  ((aparna) != (w))
% 0.91/1.11  ((b) != zenon_X81)
% 0.91/1.11  ((cow) != (c))
% 0.91/1.11  ((g zenon_X72 zenon_X74) != (a))
% 0.91/1.11  ((g (e) zenon_X73) != (c))
% 0.91/1.11  ((horse) != (lkg))
% 0.91/1.11  (-. (p (lilly) zenon_X23 (g (b) (b))))
% 0.91/1.11  ((cow) != (lkg))
% 0.91/1.11  ((g (a) (c)) != (b))
% 0.91/1.11  (ld__ (lkg) (b))
% 0.91/1.11  ((pig) != zenon_X7)
% 0.91/1.11  (-. (p (g (e) (e)) (lilly) (c)))
% 0.91/1.11  ((aparna) != (b))
% 0.91/1.11  (ld__ (hill) (w))
% 0.91/1.11  (-. (p zenon_X6 (horse) zenon_X38))
% 0.91/1.11  ((lkg) != (a))
% 0.91/1.11  ((lilly) != zenon_X78)
% 0.91/1.11  (-. (p (d) zenon_X21 (g (b) (b))))
% 0.91/1.11  (ld__ (w) (a))
% 0.91/1.11  ((k) != zenon_X56)
% 0.91/1.11  ((h zenon_X4) != (h (d)))
% 0.91/1.11  (ld__ (aparna) (a))
% 0.91/1.11  (-. (p (g (e) (e)) (aparna) zenon_X68))
% 0.91/1.11  ((c) != zenon_X78)
% 0.91/1.11  ((g (b) (b)) != zenon_X61)
% 0.91/1.11  (-. (p (lkg) zenon_X15 (g (b) (b))))
% 0.91/1.11  (-. (p (d) zenon_X21 (k)))
% 0.91/1.11  (-. (p (g (e) (e)) (lilly) zenon_X67))
% 0.91/1.11  ((lilly) != zenon_X81)
% 0.91/1.11  (-. (p (cow) zenon_X31 (k)))
% 0.91/1.11  ((g (b) (b)) != zenon_X10)
% 0.91/1.11  (ld__ (cow) (b))
% 0.91/1.11  (-. (p (h (d)) (cow) zenon_X55))
% 0.91/1.11  (ld__ (b) (c))
% 0.91/1.11  ((b) != (hill))
% 0.91/1.11  (-. (p (g (e) (e)) (horse) (c)))
% 0.91/1.11  ((aparna) != (h (d)))
% 0.91/1.11  ((g (a) (c)) != (c))
% 0.91/1.11  ((k) != zenon_X54)
% 0.91/1.11  (-. (p (g (e) (e)) zenon_X56 (pig)))
% 0.91/1.11  ((pig) != zenon_X57)
% 0.91/1.11  ((k) != zenon_X6)
% 0.91/1.11  (ld__ (w) (b))
% 0.91/1.11  (-. (p (h (d)) (g (e) (e)) (cow)))
% 0.91/1.11  ((w) != zenon_X78)
% 0.91/1.11  ((g zenon_X0 zenon_X69) != (g (e) (e)))
% 0.91/1.11  ((cow) != zenon_X80)
% 0.91/1.11  (zenon_X1 != (e))
% 0.91/1.11  ((k) != zenon_X52)
% 0.91/1.11  ((pig) != (c))
% 0.91/1.11  (zenon_X70 != (e))
% 0.91/1.11  (-. (p (h (d)) (pig) (b)))
% 0.91/1.11  (-. (p (h (d)) (pig) (g (b) (b))))
% 0.91/1.11  (-. (p zenon_X6 zenon_X7 (horse)))
% 0.91/1.11  ((g (b) (b)) != zenon_X64)
% 0.91/1.11  ((g zenon_X0 (e)) != (d))
% 0.91/1.11  ((g zenon_X0 zenon_X69) != (h (d)))
% 0.91/1.11  (-. (p (h (d)) (lkg) zenon_X49))
% 0.91/1.11  ((b) != zenon_X62)
% 0.91/1.11  ((c) != (b))
% 0.91/1.11  (-. (p (hill) zenon_X11 (g (b) (b))))
% 0.91/1.11  ((g (e) zenon_X73) != (b))
% 0.91/1.11  (-. (p (aparna) zenon_X29 (hill)))
% 0.91/1.11  (-. (ld__ zenon_X78 (a)))
% 0.91/1.11  ((k) != (g (e) (e)))
% 0.91/1.11  ((aparna) != zenon_X8)
% 0.91/1.11  ((g (b) (b)) != zenon_X52)
% 0.91/1.11  (-. (p (w) zenon_X19 zenon_X20))
% 0.91/1.11  (-. (p (a) (pig) zenon_X85))
% 0.91/1.11  (-. (p (a) zenon_X80 (lilly)))
% 0.91/1.11  ((lilly) != (hill))
% 0.91/1.11  ((w) != (g (e) (e)))
% 0.91/1.11  (-. (p (h (d)) (cow) (k)))
% 0.91/1.11  (-. (p (h (d)) (g (e) (e)) (lilly)))
% 0.91/1.11  (-. (p (g (e) (e)) (w) zenon_X61))
% 0.91/1.11  ((g (e) zenon_X70) != (g (e) (e)))
% 0.91/1.11  ((horse) != zenon_X81)
% 0.91/1.11  (-. (p (h (d)) (hill) (k)))
% 0.91/1.11  (-. (p (h (d)) zenon_X43 (lilly)))
% 0.91/1.11  (-. (p (g (e) (e)) (lkg) zenon_X63))
% 0.91/1.11  ((aparna) != (g (e) (e)))
% 0.91/1.11  ((pig) != (a))
% 0.91/1.11  ((g (e) zenon_X75) != (h (d)))
% 0.91/1.11  ((g (b) (b)) != zenon_X50)
% 0.91/1.11  (ld__ (lilly) (c))
% 0.91/1.11  (-. (p zenon_X6 zenon_X7 (d)))
% 0.91/1.11  (ld__ (pig) (w))
% 0.91/1.11  (-. (p (h (d)) (g (e) (e)) (w)))
% 0.91/1.11  (animal (pet (aparna)))
% 0.91/1.11  ((lkg) != zenon_X57)
% 0.91/1.11  (-. (p (g (e) (e)) (cow) zenon_X65))
% 0.91/1.11  ((b) != zenon_X20)
% 0.91/1.11  ((g zenon_X0 (e)) != (lkg))
% 0.91/1.11  (ld__ (g (e) zenon_X75) (g (e) (e)))
% 0.91/1.11  ((lkg) != zenon_X81)
% 0.91/1.11  ((g zenon_X1 (e)) != (a))
% 0.91/1.11  ((b) != zenon_X32)
% 0.91/1.11  ((d) != zenon_X7)
% 0.91/1.11  (zenon_X3 != (e))
% 0.91/1.11  (-. (p (h (d)) (g (e) (e)) (hill)))
% 0.91/1.11  ((g (e) zenon_X75) != (hill))
% 0.91/1.11  (-. (p (h (d)) (k) zenon_X46))
% 0.91/1.11  (zenon_X74 != (e))
% 0.91/1.11  ((a) != zenon_X6)
% 0.91/1.11  ((w) != (b))
% 0.91/1.11  ((cow) != zenon_X43)
% 0.91/1.11  ((b) != zenon_X51)
% 0.91/1.11  ((g zenon_X0 zenon_X2) != (w))
% 0.91/1.11  (ld__ (lilly) (lkg))
% 0.91/1.11  ((lkg) != zenon_X56)
% 0.91/1.11  (-. (p (h (d)) (lilly) (g (b) (b))))
% 0.91/1.11  (ld__ (lilly) (e))
% 0.91/1.11  ((d) != (b))
% 0.91/1.11  ((g zenon_X0 (e)) != (b))
% 0.91/1.11  ((c) != zenon_X50)
% 0.91/1.11  ((g zenon_X0 (e)) != (w))
% 0.91/1.11  (ld__ (a) (b))
% 0.91/1.11  (ld__ (pig) (k))
% 0.91/1.11  (-. (ld__ zenon_X56 (a)))
% 0.91/1.11  ((d) != (lkg))
% 0.91/1.11  (ld__ (lkg) (c))
% 0.91/1.11  ((h (d)) != zenon_X6)
% 0.91/1.11  (-. (p (g (e) (e)) (w) (c)))
% 0.91/1.11  ((b) != zenon_X52)
% 0.91/1.11  (-. (p zenon_X6 zenon_X7 (w)))
% 0.91/1.11  (ld__ (g zenon_X0 zenon_X69) (g (e) zenon_X70))
% 0.91/1.11  ((c) != zenon_X53)
% 0.91/1.11  ((k) != zenon_X55)
% 0.91/1.11  ((hill) != zenon_X44)
% 0.91/1.11  ((c) != zenon_X81)
% 0.91/1.11  ((g (b) (b)) != zenon_X20)
% 0.91/1.11  (ld__ (cow) (w))
% 0.91/1.11  ((c) != zenon_X8)
% 0.91/1.11  (-. (p (a) zenon_X80 (b)))
% 0.91/1.11  (-. (p zenon_X6 (hill) zenon_X27))
% 0.91/1.11  ((w) != (h (d)))
% 0.91/1.11  (ld__ (e) (a))
% 0.91/1.11  ((g (b) (b)) != zenon_X66)
% 0.91/1.11  (ld__ (e) (b))
% 0.91/1.11  (ld__ (k) (a))
% 0.91/1.11  ((lkg) != zenon_X43)
% 0.91/1.11  ((g zenon_X72 (e)) != (g (e) (e)))
% 0.91/1.11  ((k) != zenon_X30)
% 0.91/1.11  ((g (b) (b)) != zenon_X65)
% 0.91/1.11  (ld__ (cow) (k))
% 0.91/1.11  ((lilly) != zenon_X6)
% 0.91/1.11  ((pig) != zenon_X78)
% 0.91/1.11  ((h (d)) != (a))
% 0.91/1.11  ((g zenon_X1 zenon_X3) != (a))
% 0.91/1.11  ((g (e) zenon_X73) != (e))
% 0.91/1.11  (ld__ (cow) (lkg))
% 0.91/1.11  ((horse) != (h (d)))
% 0.91/1.11  ((g (b) (b)) != zenon_X45)
% 0.91/1.11  ((hill) != (a))
% 0.91/1.11  (-. (p (e) zenon_X9 zenon_X10))
% 0.91/1.11  (-. (p (g (e) (e)) (lilly) (b)))
% 0.91/1.11  ((e) != (a))
% 0.91/1.11  ((c) != zenon_X103)
% 0.91/1.11  ((k) != zenon_X80)
% 0.91/1.11  (-. (p (h (d)) (pig) zenon_X50))
% 0.91/1.11  (-. (p (g (e) (e)) zenon_X56 (horse)))
% 0.91/1.11  ((g (b) (b)) != (lilly))
% 0.91/1.11  ((g (b) (b)) != (lkg))
% 0.91/1.11  ((k) != zenon_X24)
% 0.91/1.11  ((g (b) (b)) != zenon_X42)
% 0.91/1.11  ((h zenon_X4) != (a))
% 0.91/1.11  (animal (cow))
% 0.91/1.11  ((aparna) != (lkg))
% 0.91/1.11  ((k) != zenon_X42)
% 0.91/1.11  (ld__ (g (e) zenon_X73) (g zenon_X72 zenon_X74))
% 0.91/1.11  ((lkg) != zenon_X80)
% 0.91/1.11  (ld__ (h zenon_X4) (h (d)))
% 0.91/1.11  ((c) != zenon_X52)
% 0.91/1.11  ((c) != zenon_X45)
% 0.91/1.11  ((b) != zenon_X43)
% 0.91/1.11  (-. (p (cow) zenon_X31 (b)))
% 0.91/1.11  ((horse) != zenon_X56)
% 0.91/1.11  ((e) != zenon_X78)
% 0.91/1.11  (ld__ (d) (c))
% 0.91/1.11  ((k) != zenon_X16)
% 0.91/1.11  ((g zenon_X0 (e)) != (k))
% 0.91/1.11  ((lilly) != (b))
% 0.91/1.11  ((d) != (h (d)))
% 0.91/1.11  ((d) != zenon_X78)
% 0.91/1.11  (ld__ (k) (w))
% 0.91/1.11  (-. (ld__ (c) (c)))
% 0.91/1.11  (-. (p (d) zenon_X21 (hill)))
% 0.91/1.11  ((g (e) zenon_X70) != (a))
% 0.91/1.11  (ld__ (k) (c))
% 0.91/1.11  ((lkg) != zenon_X7)
% 0.91/1.11  ((b) != zenon_X12)
% 0.91/1.11  ((g (b) (b)) != zenon_X58)
% 0.91/1.11  (ld__ (e) (w))
% 0.91/1.11  (ld__ (lilly) (d))
% 0.91/1.11  ((hill) != zenon_X14)
% 0.91/1.11  ((w) != zenon_X43)
% 0.91/1.11  ((k) != (h (d)))
% 0.91/1.11  ((aparna) != (e))
% 0.91/1.11  ((k) != zenon_X20)
% 0.91/1.11  ((c) != zenon_X67)
% 0.91/1.11  ((g zenon_X0 zenon_X2) != (b))
% 0.91/1.11  ((pig) != (b))
% 0.91/1.11  (animal (pig))
% 0.91/1.11  ((h zenon_X4) != (k))
% 0.91/1.11  ((horse) != (w))
% 0.91/1.11  (-. (p (hill) zenon_X11 (hill)))
% 0.91/1.11  ((c) != (hill))
% 0.91/1.11  ((k) != (lkg))
% 0.91/1.11  ((hill) != zenon_X81)
% 0.91/1.11  (-. (p (a) zenon_X80 (d)))
% 0.91/1.11  ((cow) != zenon_X6)
% 0.91/1.11  ((g zenon_X0 (e)) != (e))
% 0.91/1.11  ((lilly) != (e))
% 0.91/1.11  (-. (p (g (e) (e)) zenon_X56 (aparna)))
% 0.91/1.11  ((k) != (hill))
% 0.91/1.11  ((w) != (a))
% 0.91/1.11  (ld__ (k) (e))
% 0.91/1.11  ((hill) != zenon_X32)
% 0.91/1.11  (-. (p (a) zenon_X80 (pig)))
% 0.91/1.11  ((k) != zenon_X34)
% 0.91/1.11  (ld__ (lkg) (e))
% 0.91/1.11  (ld__ (g zenon_X0 zenon_X69) (g (e) (e)))
% 0.91/1.11  ((b) != zenon_X45)
% 0.91/1.11  ((k) != zenon_X18)
% 0.91/1.11  ((c) != zenon_X80)
% 0.91/1.11  ((b) != zenon_X41)
% 0.91/1.11  (-. (p (h (d)) (e) (g (b) (b))))
% 0.91/1.11  (ld__ (aparna) (b))
% 0.91/1.11  ((b) != (lkg))
% 0.91/1.11  ((g (b) (b)) != zenon_X63)
% 0.91/1.11  (-. (p (g (e) (e)) (e) (g (b) (b))))
% 0.91/1.11  ((g zenon_X0 zenon_X69) != (b))
% 0.91/1.11  ((k) != zenon_X8)
% 0.91/1.11  ((b) != zenon_X44)
% 0.91/1.11  ((aparna) != zenon_X56)
% 0.91/1.11  (ld__ (horse) (e))
% 0.91/1.11  ((horse) != zenon_X43)
% 0.91/1.11  ((k) != zenon_X49)
% 0.91/1.11  ((g (b) (b)) != zenon_X59)
% 0.91/1.11  ((c) != (k))
% 0.91/1.11  (ld__ (lilly) (hill))
% 0.91/1.11  ((aparna) != zenon_X78)
% 0.91/1.11  ((pig) != (h (d)))
% 0.91/1.11  (ld__ (hill) (d))
% 0.91/1.11  (-. (p (h (d)) (horse) zenon_X52))
% 0.91/1.11  ((h zenon_X4) != (lkg))
% 0.91/1.11  (-. (p (a) (k) zenon_X83))
% 0.91/1.11  (p (g (e) (e)) (w) (b))
% 0.91/1.11  (-. (p (h (d)) (w) zenon_X51))
% 0.91/1.11  ((g (a) (c)) != (aparna))
% 0.91/1.11  (ld__ (aparna) (hill))
% 0.91/1.11  ((b) != zenon_X7)
% 0.91/1.11  ((hill) != (h (d)))
% 0.91/1.11  (-. (p (h (d)) (w) (g (b) (b))))
% 0.91/1.11  ((horse) != (a))
% 0.91/1.11  ((g (b) (b)) != zenon_X67)
% 0.91/1.11  ((lilly) != (c))
% 0.91/1.11  ((k) != zenon_X44)
% 0.91/1.11  (-. (p (h (d)) (lilly) zenon_X53))
% 0.91/1.11  (-. (p (h (d)) (g (e) (e)) (aparna)))
% 0.91/1.11  (-. (p (g (e) (e)) (cow) (b)))
% 0.91/1.11  (ld__ (horse) (d))
% 0.91/1.11  ((c) != zenon_X51)
% 0.91/1.11  ((c) != zenon_X44)
% 0.91/1.11  ((lilly) != zenon_X44)
% 0.91/1.11  ((b) != zenon_X8)
% 0.91/1.11  ((horse) != (g (e) (e)))
% 0.91/1.11  ((horse) != zenon_X6)
% 0.91/1.11  ((b) != zenon_X55)
% 0.91/1.11  ((aparna) != zenon_X6)
% 0.91/1.11  (ld__ (g zenon_X0 (e)) (g (e) (e)))
% 0.91/1.11  ((g (b) (b)) != (k))
% 0.91/1.11  ((aparna) != zenon_X80)
% 0.91/1.11  ((c) != zenon_X48)
% 0.91/1.11  (flower (lilly))
% 0.91/1.11  (-. (p zenon_X6 (k) zenon_X26))
% 0.91/1.11  ((w) != zenon_X80)
% 0.91/1.11  ((b) != (h (d)))
% 0.91/1.11  (-. (p (h (d)) (aparna) (c)))
% 0.91/1.11  ((pig) != (g (e) (e)))
% 0.91/1.11  ((g (e) zenon_X73) != (k))
% 0.91/1.11  ((e) != zenon_X6)
% 0.91/1.11  (-. (p (horse) zenon_X33 (k)))
% 0.91/1.11  (-. (p (h (d)) (horse) (k)))
% 0.91/1.11  (-. (p zenon_X6 (b) zenon_X94))
% 0.91/1.11  (-. (p (w) zenon_X19 (hill)))
% 0.91/1.11  ((horse) != zenon_X57)
% 0.91/1.11  (-. (p (g (e) (e)) zenon_X56 (d)))
% 0.91/1.11  ((e) != (lkg))
% 0.91/1.11  ((b) != zenon_X64)
% 0.91/1.11  ((c) != (lkg))
% 0.91/1.11  ((b) != (a))
% 0.91/1.11  ((cow) != (hill))
% 0.91/1.11  ((c) != (h (d)))
% 0.91/1.11  ((c) != zenon_X62)
% 0.91/1.11  ((g zenon_X0 (e)) != (hill))
% 0.91/1.11  (ld__ (d) (b))
% 0.91/1.11  (-. (p zenon_X6 (c) zenon_X93))
% 0.91/1.11  ((g (b) (b)) != (aparna))
% 0.91/1.11  ((k) != zenon_X45)
% 0.91/1.11  (-. (p (k) zenon_X13 zenon_X14))
% 0.91/1.11  (ld__ (a) (c))
% 0.91/1.11  ((g (a) (c)) != (w))
% 0.91/1.11  (zenon_X75 != (e))
% 0.91/1.11  ((g (a) (c)) != (cow))
% 0.91/1.11  (-. (p (a) (e) zenon_X82))
% 0.91/1.11  ((cow) != (h (d)))
% 0.91/1.11  (-. (p (h (d)) (w) (b)))
% 0.91/1.11  ((cow) != (w))
% 0.91/1.11  (-. (p (lilly) zenon_X23 (b)))
% 0.91/1.11  ((d) != zenon_X57)
% 0.91/1.11  (ld__ (lkg) (d))
% 0.91/1.11  ((aparna) != zenon_X43)
% 0.91/1.11  ((pig) != zenon_X80)
% 0.91/1.11  ((g zenon_X0 zenon_X2) != (e))
% 0.91/1.11  (-. (p zenon_X6 zenon_X7 (lkg)))
% 0.91/1.11  ((c) != zenon_X61)
% 0.91/1.11  (-. (p (pig) zenon_X17 (g (b) (b))))
% 0.91/1.11  ((c) != zenon_X55)
% 0.91/1.11  (-. (ld__ (g (e) (e)) (g (e) (e))))
% 0.91/1.11  (-. (p (e) zenon_X9 (g (b) (b))))
% 0.91/1.11  ((aparna) != zenon_X7)
% 0.91/1.11  ((horse) != zenon_X44)
% 0.91/1.11  ((aparna) != (c))
% 0.91/1.11  (-. (p (h (d)) (lkg) (g (b) (b))))
% 0.91/1.11  (-. (p (a) (horse) zenon_X91))
% 0.91/1.11  (-. (p (w) zenon_X19 (k)))
% 0.91/1.11  ((pig) != (e))
% 0.91/1.11  (-. (p (h (d)) (g (e) (e)) (b)))
% 0.91/1.11  ((g zenon_X72 (e)) != (a))
% 0.91/1.11  ((c) != (w))
% 0.91/1.11  ((k) != zenon_X78)
% 0.91/1.11  (-. (p (lkg) zenon_X15 zenon_X16))
% 0.91/1.11  (-. (ld__ zenon_X43 (a)))
% 0.91/1.11  ((horse) != (b))
% 0.91/1.11  ((aparna) != (k))
% 0.91/1.11  ((horse) != (d))
% 0.91/1.11  ((e) != (k))
% 0.91/1.11  (-. (p (h (d)) (g (e) (e)) (d)))
% 0.91/1.11  ((b) != zenon_X54)
% 0.91/1.11  ((d) != zenon_X80)
% 0.91/1.11  (-. (p zenon_X6 (cow) zenon_X37))
% 0.91/1.11  ((g (b) (b)) != (e))
% 0.91/1.11  ((h zenon_X5) != (h (d)))
% 0.91/1.11  (-. (p (g (e) (e)) zenon_X56 (lkg)))
% 0.91/1.11  ((g (b) (b)) != zenon_X24)
% 0.91/1.11  (-. (p (cow) zenon_X31 (hill)))
% 0.91/1.11  ((d) != (e))
% 0.91/1.11  ((hill) != zenon_X30)
% 0.91/1.11  (-. (p (h (d)) (d) (c)))
% 0.91/1.11  (-. (p (g (e) (e)) (c) zenon_X101))
% 0.91/1.11  (-. (p (k) zenon_X13 (k)))
% 0.91/1.11  ((cow) != (b))
% 0.91/1.11  (ld__ (d) (w))
% 0.91/1.11  (ld__ (h zenon_X4) (h zenon_X5))
% 0.91/1.11  (-. (p (pig) zenon_X17 (k)))
% 0.91/1.11  ((k) != zenon_X48)
% 0.91/1.11  ((w) != zenon_X57)
% 0.91/1.11  ((c) != (g (e) (e)))
% 0.91/1.11  (-. (p (a) zenon_X80 (hill)))
% 0.91/1.11  (p (a) (b) (c))
% 0.91/1.11  ((d) != (g (e) (e)))
% 0.91/1.11  ((e) != zenon_X7)
% 0.91/1.11  ((k) != zenon_X43)
% 0.91/1.11  ((b) != zenon_X58)
% 0.91/1.11  ((k) != zenon_X22)
% 0.91/1.11  ((g (e) zenon_X73) != (hill))
% 0.91/1.11  ((horse) != (e))
% 0.91/1.11  ((g zenon_X0 zenon_X2) != (hill))
% 0.91/1.11  (-. (p zenon_X6 zenon_X7 (aparna)))
% 0.91/1.11  (-. (ld__ (a) (a)))
% 0.91/1.11  ((g (b) (b)) != zenon_X99)
% 0.91/1.11  (-. (p (h (d)) zenon_X43 (c)))
% 0.91/1.11  (-. (p (g (e) (e)) (d) (c)))
% 0.91/1.11  ((horse) != zenon_X78)
% 0.91/1.11  ((g (b) (b)) != zenon_X30)
% 0.91/1.11  (ld__ (cow) (hill))
% 0.91/1.11  ((k) != zenon_X46)
% 0.91/1.11  ((hill) != zenon_X20)
% 0.91/1.11  (ld__ (lilly) (b))
% 0.91/1.11  (-. (p (g (e) (e)) zenon_X56 (e)))
% 0.91/1.11  ((w) != zenon_X81)
% 0.91/1.11  ((g (e) zenon_X71) != (a))
% 0.91/1.11  ((cow) != (k))
% 0.91/1.11  ((e) != (hill))
% 0.91/1.11  (-. (p (hill) zenon_X11 (k)))
% 0.91/1.11  ((g (e) zenon_X77) != (a))
% 0.91/1.11  ((c) != (d))
% 0.91/1.11  (-. (p (h (d)) (g (e) (e)) (pig)))
% 0.91/1.11  ((w) != (lkg))
% 0.91/1.11  ((h zenon_X4) != (d))
% 0.91/1.11  ((k) != zenon_X53)
% 0.91/1.11  (-. (p (g (e) (e)) (pig) (b)))
% 0.91/1.11  ((d) != (k))
% 0.91/1.11  ((c) != zenon_X54)
% 0.91/1.11  ((pig) != (lkg))
% 0.91/1.11  (-. (p (h (d)) (lkg) (k)))
% 0.91/1.11  (-. (p (cow) zenon_X31 zenon_X32))
% 0.91/1.11  ((c) != zenon_X58)
% 0.91/1.11  (-. (p (h (d)) (g (e) (e)) (c)))
% 0.91/1.11  (-. (p (h (d)) (horse) (c)))
% 0.91/1.11  (-. (p zenon_X6 (aparna) zenon_X36))
% 0.91/1.11  ((lkg) != (g (e) (e)))
% 0.91/1.11  ((b) != zenon_X68)
% 0.91/1.11  (-. (p (h (d)) (g (e) (e)) (e)))
% 0.91/1.11  (ld__ (pig) (e))
% 0.91/1.11  ((w) != zenon_X7)
% 0.91/1.11  (-. (ld__ (h (d)) (h (d))))
% 0.91/1.11  (-. (p (g (e) (e)) (e) (b)))
% 0.91/1.11  ((horse) != zenon_X80)
% 0.91/1.11  (-. (p (g (e) (e)) (aparna) (c)))
% 0.91/1.11  ((g (e) zenon_X76) != (g (e) (e)))
% 0.91/1.11  (-. (p (g (e) (e)) (horse) (b)))
% 0.91/1.11  (-. (p (h (d)) (horse) (b)))
% 0.91/1.11  ((d) != zenon_X81)
% 0.91/1.11  ((h (d)) != (g (e) (e)))
% 0.91/1.11  (-. (p (lkg) zenon_X15 (hill)))
% 0.91/1.11  (ld__ (lkg) (a))
% 0.91/1.11  ((pig) != zenon_X44)
% 0.91/1.11  (-. (ld__ (w) (w)))
% 0.91/1.11  ((k) != zenon_X81)
% 0.91/1.11  ((g zenon_X0 zenon_X69) != (k))
% 0.91/1.11  ((cow) != zenon_X7)
% 0.91/1.11  (-. (p zenon_X6 zenon_X7 (lilly)))
% 0.91/1.11  (-. (p zenon_X6 zenon_X7 (pig)))
% 0.91/1.11  ((g (b) (b)) != zenon_X18)
% 0.91/1.11  (-. (p (w) zenon_X19 (b)))
% 0.91/1.11  ((d) != zenon_X8)
% 0.91/1.11  (-. (p (g (e) (e)) (horse) (g (b) (b))))
% 0.91/1.11  (-. (p (a) (b) zenon_X103))
% 0.91/1.11  (-. (p (g (e) (e)) zenon_X56 (k)))
% 0.91/1.11  (-. (p (b) zenon_X97 zenon_X98))
% 0.91/1.11  ((lilly) != (h (d)))
% 0.91/1.11  (ld__ (pig) (c))
% 0.91/1.11  (-. (ld__ zenon_X6 (a)))
% 0.91/1.11  ((hill) != zenon_X10)
% 0.91/1.11  (-. (p zenon_X6 (pig) zenon_X40))
% 0.91/1.11  ((g (a) (c)) != (e))
% 0.91/1.11  ((g (e) (e)) != zenon_X43)
% 0.91/1.11  ((cow) != (d))
% 0.91/1.11  ((g (b) (b)) != zenon_X49)
% 0.91/1.11  (-. (p (h (d)) (c) zenon_X99))
% 0.91/1.11  (ld__ (pig) (lkg))
% 0.91/1.11  ((g (e) (e)) != zenon_X6)
% 0.91/1.11  (ld__ (g (e) zenon_X73) (g zenon_X72 (e)))
% 0.91/1.11  ((g (b) (b)) != zenon_X16)
% 0.91/1.11  ((lkg) != zenon_X44)
% 0.91/1.11  (ld__ (lilly) (k))
% 0.91/1.11  ((h zenon_X5) != (a))
% 0.91/1.11  ((pig) != (k))
% 0.91/1.11  ((c) != (e))
% 0.91/1.11  ((hill) != zenon_X43)
% 0.91/1.11  (ld__ (g zenon_X0 zenon_X2) (g zenon_X1 (e)))
% 0.91/1.11  (zenon_X76 != (e))
% 0.91/1.11  (zenon_X72 != (e))
% 0.91/1.11  (-. (p (h (d)) (aparna) (g (b) (b))))
% 0.91/1.11  (-. (p zenon_X6 (w) zenon_X41))
% 0.91/1.11  ((horse) != zenon_X7)
% 0.91/1.11  (-. (ld__ zenon_X44 (a)))
% 0.91/1.11  ((g zenon_X0 zenon_X2) != (lkg))
% 0.91/1.11  (-. (p (g (e) (e)) (hill) (g (b) (b))))
% 0.91/1.11  (p (k) (lkg) (hill))
% 0.91/1.11  (zenon_X0 != (e))
% 0.91/1.11  (zenon_X71 != (e))
% 0.91/1.11  (-. (ld__ zenon_X81 (a)))
% 0.91/1.11  ((d) != (a))
% 0.91/1.11  (-. (p (a) (d) zenon_X87))
% 0.91/1.11  ((lilly) != (lkg))
% 0.91/1.11  ((lilly) != (w))
% 0.91/1.11  (ld__ (lkg) (w))
% 0.91/1.11  ((cow) != zenon_X81)
% 0.91/1.11  ((h zenon_X4) != (w))
% 0.91/1.11  ((g zenon_X1 zenon_X3) != (g (e) (e)))
% 0.91/1.11  ((g (b) (b)) != (c))
% 0.91/1.11  ((lilly) != (k))
% 0.91/1.11  (-. (p (g (e) (e)) (d) zenon_X62))
% 0.91/1.11  (-. (p (g (e) (e)) zenon_X56 (w)))
% 0.91/1.11  ((w) != zenon_X44)
% 0.91/1.11  (-. (p zenon_X6 (d) zenon_X35))
% 0.91/1.11  (-. (p zenon_X6 zenon_X7 (cow)))
% 0.91/1.11  (-. (p (g (e) (e)) (horse) zenon_X66))
% 0.91/1.11  ((b) != zenon_X78)
% 0.91/1.11  ((cow) != (a))
% 0.91/1.11  (-. (p (h (d)) (e) zenon_X45))
% 0.91/1.11  (-. (p (aparna) zenon_X29 (g (b) (b))))
% 0.91/1.11  (ld__ (k) (b))
% 0.91/1.11  (-. (p (h (d)) zenon_X43 (pig)))
% 0.91/1.11  ((lkg) != zenon_X78)
% 0.91/1.11  (-. (p (lilly) zenon_X23 (k)))
% 0.91/1.11  (-. (p (g (e) (e)) (cow) (g (b) (b))))
% 0.91/1.11  ((g (a) (c)) != (lilly))
% 0.91/1.11  ((k) != zenon_X57)
% 0.91/1.11  ((g zenon_X0 zenon_X2) != (a))
% 0.91/1.11  ((aparna) != (d))
% 0.91/1.11  (-. (p (horse) zenon_X33 (g (b) (b))))
% 0.91/1.11  ((d) != zenon_X6)
% 0.91/1.11  (-. (p (h (d)) (b) zenon_X100))
% 0.91/1.11  ((g (e) zenon_X75) != (e))
% 0.91/1.11  (ld__ (lkg) (k))
% 0.91/1.11  ((cow) != (e))
% 0.91/1.11  (-. (p (h (d)) (c) (g (b) (b))))
% 0.91/1.11  (-. (p (g (e) (e)) (pig) zenon_X64))
% 0.91/1.11  (-. (ld__ (k) (k)))
% 0.91/1.11  ((g zenon_X0 zenon_X2) != (h (d)))
% 0.91/1.11  ((k) != zenon_X10)
% 0.91/1.11  ((w) != zenon_X8)
% 0.91/1.11  ((aparna) != zenon_X44)
% 0.91/1.11  ((g (b) (b)) != (horse))
% 0.91/1.11  ((h zenon_X4) != (g (e) (e)))
% 0.91/1.11  ((lilly) != zenon_X7)
% 0.91/1.11  (-. (p (h (d)) zenon_X43 (horse)))
% 0.91/1.11  ((b) != zenon_X30)
% 0.91/1.11  (-. (p (horse) zenon_X33 (b)))
% 0.91/1.11  ((b) != (g (e) (e)))
% 0.91/1.11  (-. (p (k) (lkg) zenon_X42))
% 0.91/1.11  (-. (p (h (d)) (b) (g (b) (b))))
% 0.91/1.11  ((g (a) (c)) != (horse))
% 0.91/1.11  (ld__ (horse) (hill))
% 0.91/1.11  ((hill) != zenon_X18)
% 0.91/1.11  ((g (b) (b)) != zenon_X51)
% 0.91/1.11  ((hill) != zenon_X7)
% 0.91/1.11  ((g (b) (b)) != (cow))
% 0.91/1.11  ((e) != (b))
% 0.91/1.11  (-. (p (k) zenon_X13 (hill)))
% 0.91/1.11  ((d) != zenon_X43)
% 0.91/1.11  (-. (p zenon_X6 (lilly) zenon_X39))
% 0.91/1.11  (-. (p (h (d)) (e) (k)))
% 0.91/1.11  (-. (p (a) (hill) zenon_X84))
% 0.91/1.11  ((c) != (a))
% 0.91/1.11  (-. (p (hill) zenon_X11 (b)))
% 0.91/1.11  ((g (b) (b)) != (w))
% 0.91/1.11  ((pig) != (d))
% 0.91/1.11  ((c) != zenon_X6)
% 0.91/1.11  (-. (p (h (d)) (d) (g (b) (b))))
% 0.91/1.11  ((g zenon_X0 zenon_X2) != (d))
% 0.91/1.11  ((g (a) (c)) != (lkg))
% 0.91/1.11  (ld__ (horse) (a))
% 0.91/1.11  (-. (p (h (d)) zenon_X43 (hill)))
% 0.91/1.11  (-. (p (w) zenon_X19 (g (b) (b))))
% 0.91/1.11  ((aparna) != zenon_X57)
% 0.91/1.11  ((b) != zenon_X42)
% 0.91/1.11  (ld__ (g zenon_X0 zenon_X2) (g zenon_X1 zenon_X3))
% 0.91/1.11  (-. (p (e) zenon_X9 (hill)))
% 0.91/1.11  (-. (p (h (d)) (d) (k)))
% 0.91/1.11  ((b) != zenon_X57)
% 0.91/1.11  ((b) != zenon_X53)
% 0.91/1.11  (ld__ (cow) (c))
% 0.91/1.11  (-. (p (lilly) zenon_X23 zenon_X24))
% 0.91/1.11  (ld__ (lilly) (a))
% 0.91/1.11  (-. (p (g (e) (e)) (lilly) (g (b) (b))))
% 0.91/1.11  ((g (a) (c)) != (hill))
% 0.91/1.11  (ld__ (aparna) (k))
% 0.91/1.11  ((b) != zenon_X65)
% 0.91/1.11  ((lilly) != zenon_X56)
% 0.91/1.11  ((k) != zenon_X32)
% 0.91/1.11  ((g (e) zenon_X76) != (a))
% 0.91/1.11  ((pig) != zenon_X81)
% 0.91/1.11  (-. (ld__ zenon_X57 (a)))
% 0.91/1.11  ((g (b) (b)) != zenon_X32)
% 0.91/1.11  ((b) != zenon_X61)
% 0.91/1.11  (ld__ (hill) (e))
% 0.91/1.11  ((aparna) != (a))
% 0.91/1.11  (ld__ (lkg) (hill))
% 0.91/1.11  ((b) != zenon_X34)
% 0.91/1.11  ((lilly) != (d))
% 0.91/1.11  ((b) != zenon_X18)
% 0.91/1.11  (-. (p (g (e) (e)) (w) (g (b) (b))))
% 0.91/1.11  ((hill) != zenon_X80)
% 0.91/1.11  (-. (p (g (e) (e)) zenon_X56 (cow)))
% 0.91/1.11  ((cow) != zenon_X44)
% 0.91/1.11  (-. (p (a) (w) zenon_X86))
% 0.91/1.11  (-. (p (h (d)) (lilly) (k)))
% 0.91/1.11  ((g (b) (b)) != (d))
% 0.91/1.11  ((lilly) != (g (e) (e)))
% 0.91/1.11  ((g (e) zenon_X75) != (k))
% 0.91/1.11  (ld__ (h (d)) (h zenon_X79))
% 0.91/1.11  ((e) != (w))
% 0.91/1.11  ((g zenon_X0 zenon_X69) != (d))
% 0.91/1.11  ((b) != zenon_X24)
% 0.91/1.11  ((lilly) != zenon_X8)
% 0.91/1.11  (ld__ (pig) (hill))
% 0.91/1.11  (-. (p (h (d)) zenon_X43 (e)))
% 0.91/1.11  ((g zenon_X0 zenon_X69) != (hill))
% 0.91/1.11  ((g zenon_X0 zenon_X2) != (c))
% 0.91/1.11  (ld__ (aparna) (d))
% 0.91/1.11  ((g zenon_X0 zenon_X69) != (e))
% 0.91/1.11  ((d) != zenon_X44)
% 0.91/1.11  (ld__ (hill) (k))
% 0.91/1.11  (-. (p (h (d)) zenon_X43 (cow)))
% 0.91/1.11  (-. (p (h (d)) (k) (k)))
% 0.91/1.11  (-. (p (a) zenon_X80 (c)))
% 0.91/1.11  ((g (b) (b)) != zenon_X22)
% 0.91/1.11  (-. (p (aparna) zenon_X29 (b)))
% 0.91/1.11  (-. (p (pig) zenon_X17 (hill)))
% 0.91/1.11  ((h zenon_X79) != (a))
% 0.91/1.11  (ld__ (lilly) (w))
% 0.91/1.11  ((c) != zenon_X43)
% 0.91/1.11  (-. (p (aparna) zenon_X29 (k)))
% 0.91/1.11  (-. (p (h (d)) (aparna) (k)))
% 0.91/1.11  (-. (p (a) zenon_X80 (lkg)))
% 0.91/1.11  (-. (p (g (e) (e)) zenon_X56 (lilly)))
% 0.91/1.11  (ld__ (e) (c))
% 0.91/1.11  ((hill) != zenon_X78)
% 0.91/1.11  (-. (p (h (d)) (horse) (g (b) (b))))
% 0.91/1.11  (-. (ld__ (h (d)) (a)))
% 0.91/1.11  (-. (p (a) zenon_X80 (horse)))
% 0.91/1.11  ((g (b) (b)) != zenon_X100)
% 0.91/1.11  (ld__ (aparna) (e))
% 0.91/1.11  (-. (p (h (d)) (g (e) (e)) (horse)))
% 0.91/1.11  ((g (b) (b)) != (b))
% 0.91/1.11  ((g zenon_X0 zenon_X69) != (a))
% 0.91/1.11  ((g (e) (e)) != (a))
% 0.91/1.11  (-. (p (h (d)) (lilly) (c)))
% 0.91/1.11  ((g (e) zenon_X75) != (g (e) (e)))
% 0.91/1.11  ((lilly) != zenon_X80)
% 0.91/1.11  (-. (p (hill) zenon_X11 zenon_X12))
% 0.91/1.11  ((g (b) (b)) != zenon_X53)
% 0.91/1.11  (-. (ld__ zenon_X8 (a)))
% 0.91/1.11  (-. (p (aparna) zenon_X29 zenon_X30))
% 0.91/1.11  (-. (p (h (d)) zenon_X43 (aparna)))
% 0.91/1.11  (-. (p (g (e) (e)) (lkg) (g (b) (b))))
% 0.91/1.11  (ld__ (k) (d))
% 0.91/1.11  ((h zenon_X4) != (hill))
% 0.91/1.11  ((c) != zenon_X56)
% 0.91/1.11  ((g (e) zenon_X73) != (h (d)))
% 0.91/1.11  ((g (a) (c)) != (k))
% 0.91/1.11  (zenon_X5 != (d))
% 0.91/1.11  ((g (e) zenon_X75) != (w))
% 0.91/1.11  ((g (b) (b)) != zenon_X34)
% 0.91/1.11  (-. (p (h (d)) (d) (b)))
% 0.91/1.11  (-. (p (h (d)) (lilly) (b)))
% 0.91/1.11  (ld__ (horse) (lkg))
% 0.91/1.11  ((cow) != zenon_X56)
% 0.91/1.11  (-. (p (h (d)) (g (e) (e)) (lkg)))
% 0.91/1.11  (-. (p (a) zenon_X80 (w)))
% 0.91/1.11  ((b) != zenon_X67)
% 0.91/1.11  ((g (a) (c)) != (pig))
% 0.91/1.11  (-. (p (h (d)) (aparna) (b)))
% 0.91/1.11  ((h zenon_X4) != (b))
% 0.91/1.11  ((g (b) (b)) != zenon_X12)
% 0.91/1.11  (-. (p (h (d)) zenon_X43 (k)))
% 0.91/1.11  ((k) != zenon_X12)
% 0.91/1.11  ((c) != zenon_X66)
% 0.91/1.11  (-. (p (g (e) (e)) (aparna) (b)))
% 0.91/1.11  (ld__ (g zenon_X0 (e)) (g (e) zenon_X71))
% 0.91/1.11  (-. (p (a) (cow) zenon_X90))
% 0.91/1.11  (-. (p (cow) zenon_X31 (g (b) (b))))
% 0.91/1.11  (ld__ (horse) (w))
% 0.91/1.11  (ld__ (horse) (c))
% 0.91/1.11  (ld__ (aparna) (c))
% 0.91/1.11  ((g (e) zenon_X73) != (a))
% 0.91/1.11  ((horse) != (c))
% 0.91/1.11  (-. (p (a) (lilly) zenon_X92))
% 0.91/1.11  ((lkg) != (h (d)))
% 0.91/1.11  ((g (e) zenon_X73) != (lkg))
% 0.91/1.11  ((g zenon_X0 (e)) != (h (d)))
% 0.91/1.11  ((e) != zenon_X80)
% 0.91/1.11  (-. (p zenon_X6 (w) (b)))
% 0.91/1.11  (-. (p (lkg) zenon_X15 (b)))
% 0.91/1.11  (-. (p (a) (c) zenon_X104))
% 0.91/1.11  ((pig) != zenon_X56)
% 0.91/1.11  ((lilly) != zenon_X43)
% 0.91/1.11  (-. (p (g (e) (e)) (pig) (c)))
% 0.91/1.11  (-. (p zenon_X6 zenon_X7 (e)))
% 0.91/1.11  (-. (p zenon_X6 zenon_X7 (b)))
% 0.91/1.11  (ld__ (cow) (e))
% 0.91/1.11  ((b) != zenon_X14)
% 0.91/1.11  (-. (p (g (e) (e)) (b) zenon_X102))
% 0.91/1.11  ((b) != (k))
% 0.91/1.11  ((b) != zenon_X10)
% 0.91/1.11  ((hill) != (g (e) (e)))
% 0.91/1.11  ((h zenon_X4) != (c))
% 0.91/1.11  ((h zenon_X79) != (h (d)))
% 0.91/1.11  (-. (p (a) zenon_X80 (e)))
% 0.91/1.11  ((pig) != (hill))
% 0.91/1.11  ((w) != zenon_X56)
% 0.91/1.11  (-. (p (k) zenon_X13 (b)))
% 0.91/1.11  (-. (p (h (d)) (cow) (c)))
% 0.91/1.11  ((g (b) (b)) != zenon_X48)
% 0.91/1.11  (-. (p (k) (lkg) (b)))
% 0.91/1.11  ((w) != zenon_X6)
% 0.91/1.11  (-. (p (pig) zenon_X17 zenon_X18))
% 0.91/1.11  (-. (p (h (d)) zenon_X43 (d)))
% 0.91/1.11  (-. (ld__ (hill) (hill)))
% 0.91/1.11  ((g (b) (b)) != zenon_X47)
% 0.91/1.11  (ld__ (aparna) (lkg))
% 0.91/1.11  ((cow) != zenon_X8)
% 0.91/1.11  (-. (p (k) (lkg) (k)))
% 0.91/1.11  (zenon_X4 != (d))
% 0.91/1.11  ((aparna) != (hill))
% 0.91/1.11  ((d) != (w))
% 0.91/1.11  (ld__ (horse) (b))
% 0.91/1.11  ((g (b) (b)) != zenon_X60)
% 0.91/1.11  ((g zenon_X0 zenon_X69) != (c))
% 0.91/1.11  (-. (ld__ (lkg) (lkg)))
% 0.91/1.11  (-. (p (a) zenon_X80 (cow)))
% 0.91/1.11  ((lkg) != (hill))
% 0.91/1.11  ((e) != (h (d)))
% 0.91/1.11  ((g (b) (b)) != zenon_X54)
% 0.91/1.11  (-. (p (k) (lkg) (g (b) (b))))
% 0.91/1.11  (-. (p (h (d)) (k) (g (b) (b))))
% 0.91/1.11  ((g (b) (b)) != zenon_X46)
% 0.91/1.11  ((g zenon_X0 zenon_X69) != (w))
% 0.91/1.11  (ld__ (cow) (a))
% 0.91/1.11  ((e) != zenon_X81)
% 0.91/1.11  (ld__ (pig) (d))
% 0.91/1.11  ((g zenon_X72 zenon_X74) != (g (e) (e)))
% 0.91/1.11  ((b) != zenon_X6)
% 0.91/1.11  (ld__ (pig) (a))
% 0.91/1.11  ((b) != zenon_X80)
% 0.91/1.11  (-. (p (g (e) (e)) zenon_X56 (hill)))
% 0.91/1.11  (-. (p (c) zenon_X95 zenon_X96))
% 0.91/1.11  ((b) != zenon_X56)
% 0.91/1.11  ((g (b) (b)) != zenon_X14)
% 0.91/1.11  (ld__ (aparna) (w))
% 0.91/1.11  ((hill) != zenon_X6)
% 0.91/1.11  (-. (p (h (d)) (cow) (g (b) (b))))
% 0.91/1.11  ((lkg) != zenon_X6)
% 0.91/1.11  ((horse) != zenon_X8)
% 0.91/1.11  (-. (p (k) zenon_X13 (g (b) (b))))
% 0.91/1.11  (-. (p (h (d)) (pig) (k)))
% 0.91/1.11  ((c) != zenon_X64)
% 0.91/1.11  (ld__ (w) (c))
% 0.91/1.11  ((b) != zenon_X16)
% 0.91/1.11  ((hill) != zenon_X22)
% 0.91/1.11  ((w) != (k))
% 0.91/1.11  ((pig) != zenon_X43)
% 0.91/1.11  (-. (p (a) zenon_X80 (aparna)))
% 0.91/1.11  (-. (p (h (d)) zenon_X43 (b)))
% 0.91/1.11  (-. (p (e) zenon_X9 (k)))
% 0.91/1.11  ((hill) != zenon_X16)
% 0.91/1.11  (-. (p (h (d)) (pig) (c)))
% 0.91/1.11  (-. (p (lkg) zenon_X15 (k)))
% 0.91/1.11  (ld__ (hill) (c))
% 0.91/1.11  ((hill) != zenon_X34)
% 0.91/1.11  ((e) != (g (e) (e)))
% 0.91/1.11  (-. (p (g (e) (e)) (cow) (c)))
% 0.91/1.11  ((c) != zenon_X68)
% 0.91/1.11  ((g (e) zenon_X75) != (a))
% 0.91/1.11  (p (h (d)) (g (e) (e)) (k))
% 0.91/1.11  (-. (p (h (d)) (e) (b)))
% 0.91/1.11  ((e) != zenon_X44)
% 0.91/1.11  (-. (p (e) zenon_X9 (b)))
% 0.91/1.11  (-. (p (g (e) (e)) (hill) zenon_X59))
% 0.91/1.11  (-. (p (h (d)) zenon_X43 (lkg)))
% 0.91/1.11  ((g (e) zenon_X77) != (g (e) (e)))
% 0.91/1.11  ((g zenon_X0 zenon_X69) != (lkg))
% 0.91/1.11  ((hill) != zenon_X12)
% 0.91/1.11  ((g (e) zenon_X75) != (d))
% 0.91/1.11  ((g (e) zenon_X75) != (c))
% 0.91/1.11  ((hill) != zenon_X56)
% 0.91/1.11  (-. (p (g (e) (e)) (k) (g (b) (b))))
% 0.91/1.11  (-. (p (horse) zenon_X33 zenon_X34))
% 0.91/1.11  ((c) != zenon_X65)
% 0.91/1.11  (-. (ld__ (b) (b)))
% 0.91/1.11  (-. (p (a) (aparna) zenon_X89))
% 0.91/1.11  ((k) != zenon_X14)
% 0.91/1.11  ((k) != zenon_X51)
% 0.91/1.11  ((g (e) zenon_X75) != (b))
% 0.91/1.11  (-. (p (h (d)) (e) (c)))
% 0.91/1.11  ((h zenon_X4) != (e))
% 0.91/1.11  ((lkg) != zenon_X13)
% 0.91/1.11  (-. (ld__ (e) (e)))
% 0.91/1.11  ((b) != zenon_X50)
% 0.91/1.11  (-. (p (h (d)) (hill) zenon_X47))
% 0.91/1.11  ((lkg) != zenon_X8)
% 0.91/1.11  ((g zenon_X0 zenon_X2) != (k))
% 0.91/1.11  (-. (p (g (e) (e)) (pig) (g (b) (b))))
% 0.91/1.11  ((g (e) zenon_X71) != (g (e) (e)))
% 0.91/1.11  ((horse) != (hill))
% 0.91/1.11  (-. (p (h (d)) (d) zenon_X48))
% 0.91/1.11  ((g zenon_X0 (e)) != (a))
% 0.91/1.11  (-. (ld__ zenon_X80 (a)))
% 0.91/1.11  ((pig) != (w))
% 0.91/1.11  ((w) != (hill))
% 0.91/1.11  (ld__ (hill) (b))
% 0.91/1.11  (ld__ (cow) (d))
% 0.91/1.11  (-. (p (g (e) (e)) (k) zenon_X60))
% 0.91/1.11  ((g (e) zenon_X75) != (lkg))
% 0.91/1.11  ((g (e) zenon_X73) != (w))
% 0.91/1.11  ((b) != zenon_X22)
% 0.91/1.11  (ld__ (pig) (b))
% 0.91/1.11  (-. (p (g (e) (e)) (e) zenon_X58))
% 0.91/1.11  ((g (b) (b)) != (hill))
% 0.91/1.11  ((g (e) zenon_X73) != (d))
% 0.91/1.11  (ld__ (hill) (a))
% 0.91/1.11  ((cow) != zenon_X57)
% 0.91/1.11  (-. (p (horse) zenon_X33 (hill)))
% 0.91/1.11  (-. (ld__ zenon_X7 (a)))
% 0.91/1.11  (-. (p (h (d)) (w) (k)))
% 0.91/1.11  (p (h (d)) (g (a) (c)) (g (b) (b)))
% 0.91/1.11  (-. (p (h (d)) (cow) (b)))
% 0.91/1.11  (p (a) (a) (a))
% 0.91/1.11  (-. (p (g (e) (e)) (d) (b)))
% 0.91/1.11  (-. (p (d) zenon_X21 zenon_X22))
% 0.91/1.11  ((c) != zenon_X57)
% 0.91/1.11  (-. (p zenon_X6 zenon_X7 (c)))
% 0.91/1.11  ((pig) != zenon_X8)
% 0.91/1.11  (-. (p (g (e) (e)) (d) (g (b) (b))))
% 0.91/1.11  ((hill) != zenon_X57)
% 0.91/1.11  (zenon_X69 != (e))
% 0.91/1.11  (-. (p (g (e) (e)) zenon_X56 (c)))
% 0.91/1.11  (-. (p (d) zenon_X21 (b)))
% 0.91/1.11  ((hill) != zenon_X8)
% 0.91/1.11  ((e) != zenon_X43)
% 0.91/1.11  ((hill) != zenon_X42)
% 0.91/1.11  (-. (p zenon_X6 (e) zenon_X28))
% 0.91/1.11  (-. (p zenon_X6 zenon_X7 (k)))
% 0.91/1.11  (animal (horse))
% 0.91/1.11  ((horse) != (k))
% 0.91/1.11  (-. (p (h (d)) (aparna) zenon_X54))
% 0.91/1.11  (-. (ld__ (d) (d)))
% 0.91/1.11  ((k) != zenon_X47)
% 0.91/1.11  (ld__ (g (e) zenon_X75) (g (e) zenon_X76))
% 0.91/1.11  (-. (p (h (d)) (hill) (g (b) (b))))
% 0.91/1.11  ((k) != zenon_X50)
% 0.91/1.11  (-. (p zenon_X6 (lkg) zenon_X25))
% 0.91/1.11  (zenon_X79 != (d))
% 0.91/1.11  (-. (p (g (e) (e)) (e) (c)))
% 0.91/1.11  ((d) != zenon_X56)
% 0.91/1.11  ((g zenon_X1 (e)) != (g (e) (e)))
% 0.91/1.11  (ld__ (g (e) (e)) (g (e) zenon_X77))
% 0.91/1.11  ((cow) != (g (e) (e)))
% 0.91/1.11  (zenon_X77 != (e))
% 0.91/1.11  (-. (p (h (d)) (w) (c)))
% 0.91/1.11  ((lilly) != (a))
% 0.91/1.11  (-. (p (h (d)) zenon_X43 (w)))
% 0.91/1.11  ((k) != zenon_X7)
% 0.91/1.11  ((hill) != zenon_X24)
% 0.91/1.11  ((b) != zenon_X66)
% 0.91/1.11  (-. (p (lilly) zenon_X23 (hill)))
% 0.91/1.11  (-. (p zenon_X6 zenon_X7 (hill)))
% 0.91/1.11  *)
% 0.91/1.11  (* NO-PROOF *)
% 0.91/1.11  % SZS status GaveUp
% 0.91/1.11  Number of rewrites on terms: 0
% 0.91/1.11  Number of rewrites on props: 1
% 0.91/1.11  nodes searched: 7462
% 0.91/1.11  max branch formulas: 1240
% 0.91/1.11  proof nodes created: 706
% 0.91/1.11  formulas created: 22038
% 0.91/1.11  
%------------------------------------------------------------------------------