%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : SYO579+1 : TPTP v8.2.0. Released v5.5.0. % Transfm : none % Format : tptp:raw % Command : run_zenon_modulo %d %s % Computer : n005.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:20:11 EDT 2024 % Result : Unknown 3.62s 3.87s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.14 % Problem : SYO579+1 : TPTP v8.2.0. Released v5.5.0. % 0.07/0.14 % Command : run_zenon_modulo %d %s % 0.13/0.35 % Computer : n005.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 : Sun Jun 23 17:46:38 EDT 2024 % 0.13/0.35 % CPUTime : % 3.62/3.86 Zenon error: exhausted search space without finding a proof % 3.62/3.86 (* Current branch: % 3.62/3.86 (zenon_X26 != zenon_X52) % 3.62/3.86 (zenon_X28 != zenon_X23) % 3.62/3.86 (zenon_X91 != Tau_19) % 3.62/3.86 (zenon_X59 != zenon_X74) % 3.62/3.86 (-. (b48_buttercup10110 Tau_0)) % 3.62/3.86 (zenon_X79 != zenon_X69) % 3.62/3.86 (zenon_X66 != zenon_X83) % 3.62/3.86 (Tau_14 != zenon_X27) % 3.62/3.86 (Tau_9 != zenon_X69) % 3.62/3.86 (zenon_X84 != zenon_X53) % 3.62/3.86 (zenon_X54 != zenon_X71) % 3.62/3.86 (-. (b48_buttercup10107 zenon_X52)) % 3.62/3.86 (zenon_X89 != zenon_X73) % 3.62/3.86 (zenon_X32 != zenon_X91) % 3.62/3.86 (Tau_20 != zenon_X75) % 3.62/3.86 (zenon_X48 != zenon_X62) % 3.62/3.86 (zenon_X28 != zenon_X64) % 3.62/3.86 (Tau_8 != zenon_X55) % 3.62/3.86 (zenon_X78 != Tau_20) % 3.62/3.86 (-. (b48_buttercup10102 Tau_9)) % 3.62/3.86 (Tau_13 != zenon_X83) % 3.62/3.86 (zenon_X78 != zenon_X52) % 3.62/3.86 (-. (b48_buttercup10107 zenon_X66)) % 3.62/3.86 (zenon_X79 != zenon_X56) % 3.62/3.86 (zenon_X35 != zenon_X37) % 3.62/3.86 (Tau_0 != Tau_18) % 3.62/3.86 (zenon_X60 != Tau_2) % 3.62/3.86 (zenon_X89 != zenon_X76) % 3.62/3.86 (Tau_19 != zenon_X57) % 3.62/3.86 (-. (b48_buttercup10107 Tau_8)) % 3.62/3.86 (zenon_X54 != Tau_19) % 3.62/3.86 (Tau_13 != Tau_20) % 3.62/3.86 (zenon_X54 != Tau_8) % 3.62/3.86 (Tau_4 != Tau_1) % 3.62/3.86 (Tau_16 != zenon_X75) % 3.62/3.86 (zenon_X46 != Tau_2) % 3.62/3.86 (b48_buttercup10109 Tau_19) % 3.62/3.86 (zenon_X24 != Tau_2) % 3.62/3.86 (zenon_X66 != zenon_X79) % 3.62/3.86 (zenon_X83 != zenon_X51) % 3.62/3.86 (zenon_X54 != Tau_4) % 3.62/3.86 (zenon_X81 != zenon_X49) % 3.62/3.86 (zenon_X36 != Tau_17) % 3.62/3.86 (zenon_X59 != zenon_X75) % 3.62/3.86 (zenon_X91 != Tau_16) % 3.62/3.86 (zenon_X58 != zenon_X49) % 3.62/3.86 (zenon_X57 != zenon_X75) % 3.62/3.86 (Tau_13 != zenon_X64) % 3.62/3.86 (zenon_X59 != zenon_X51) % 3.62/3.86 (Tau_3 != zenon_X76) % 3.62/3.86 (Tau_5 != zenon_X74) % 3.62/3.86 (Tau_2 != zenon_X22) % 3.62/3.86 (-. (b48_buttercup10110 zenon_X65)) % 3.62/3.86 (Tau_7 != zenon_X89) % 3.62/3.86 (Tau_19 != zenon_X49) % 3.62/3.86 (zenon_X69 != zenon_X55) % 3.62/3.86 (Tau_3 != zenon_X68) % 3.62/3.86 (Tau_7 != zenon_X82) % 3.62/3.86 (Tau_5 != zenon_X79) % 3.62/3.86 (zenon_X84 != zenon_X85) % 3.62/3.86 (Tau_13 != zenon_X62) % 3.62/3.86 (-. (b48_buttercup10110 zenon_X92)) % 3.62/3.86 (-. (b48_buttercup10109 zenon_X57)) % 3.62/3.86 (Tau_4 != zenon_X56) % 3.62/3.86 (-. (b48_buttercup10111 zenon_X59)) % 3.62/3.86 (zenon_X31 != Tau_20) % 3.62/3.86 (Tau_7 != zenon_X59) % 3.62/3.86 (zenon_X31 != zenon_X24) % 3.62/3.86 (Tau_11 != Tau_10) % 3.62/3.86 (Tau_4 != zenon_X55) % 3.62/3.86 (-. (b48_buttercup10110 zenon_X63)) % 3.62/3.86 (zenon_X66 != zenon_X63) % 3.62/3.86 (Tau_9 != zenon_X64) % 3.62/3.86 (zenon_X77 != zenon_X21) % 3.62/3.86 (zenon_X65 != zenon_X45) % 3.62/3.86 (zenon_X36 != zenon_X74) % 3.62/3.86 (Tau_4 != zenon_X75) % 3.62/3.86 (Tau_5 != zenon_X58) % 3.62/3.86 (zenon_X71 != Tau_16) % 3.62/3.86 (zenon_X72 != zenon_X79) % 3.62/3.86 (b48_buttercup10111 Tau_13) % 3.62/3.86 (zenon_X28 != zenon_X62) % 3.62/3.86 (zenon_X27 != zenon_X68) % 3.62/3.86 (-. (b48_buttercup10108 zenon_X82)) % 3.62/3.86 (Tau_11 != zenon_X52) % 3.62/3.86 (-. (b48_buttercup10102 zenon_X55)) % 3.62/3.86 (Tau_19 != Tau_6) % 3.62/3.86 (k04_buttercup10622 zenon_X59) % 3.62/3.86 (zenon_X65 != Tau_16) % 3.62/3.86 (zenon_X84 != zenon_X69) % 3.62/3.86 (zenon_X91 != Tau_10) % 3.62/3.86 (Tau_20 != zenon_X81) % 3.62/3.86 (Tau_13 != zenon_X26) % 3.62/3.86 (Tau_2 != zenon_X47) % 3.62/3.86 (zenon_X84 != zenon_X73) % 3.62/3.86 (zenon_X37 != zenon_X64) % 3.62/3.86 (zenon_X24 != zenon_X80) % 3.62/3.86 (zenon_X76 != zenon_X74) % 3.62/3.86 (zenon_X63 != Tau_15) % 3.62/3.86 (Tau_20 != zenon_X55) % 3.62/3.86 (Tau_6 != zenon_X63) % 3.62/3.86 (zenon_X36 != zenon_X92) % 3.62/3.86 (zenon_X88 != zenon_X55) % 3.62/3.86 (-. (b48_buttercup10109 zenon_X36)) % 3.62/3.86 (Tau_11 != zenon_X27) % 3.62/3.86 (zenon_X33 != zenon_X21) % 3.62/3.86 (zenon_X61 != Tau_13) % 3.62/3.86 (zenon_X65 != Tau_8) % 3.62/3.86 (zenon_X53 != Tau_16) % 3.62/3.86 (Tau_14 != zenon_X53) % 3.62/3.86 (zenon_X33 != zenon_X37) % 3.62/3.86 (zenon_X92 != zenon_X30) % 3.62/3.86 (b48_buttercup10108 zenon_X25) % 3.62/3.86 (zenon_X86 != zenon_X45) % 3.62/3.86 (zenon_X76 != Tau_20) % 3.62/3.86 (Tau_7 != zenon_X63) % 3.62/3.86 (Tau_5 != zenon_X61) % 3.62/3.86 (zenon_X76 != Tau_8) % 3.62/3.86 (zenon_X23 != zenon_X87) % 3.62/3.86 (zenon_X90 != zenon_X81) % 3.62/3.86 (-. (b48_buttercup10109 zenon_X69)) % 3.62/3.86 (k04_buttercup10100 Tau_13) % 3.62/3.86 (zenon_X76 != zenon_X62) % 3.62/3.86 (zenon_X88 != zenon_X56) % 3.62/3.86 (Tau_9 != zenon_X87) % 3.62/3.86 (zenon_X21 != Tau_11) % 3.62/3.86 (zenon_X64 != zenon_X45) % 3.62/3.86 (zenon_X26 != zenon_X59) % 3.62/3.86 (zenon_X24 != zenon_X92) % 3.62/3.86 (-. (b48_buttercup10102 zenon_X52)) % 3.62/3.86 (zenon_X66 != Tau_16) % 3.62/3.86 (zenon_X72 != zenon_X82) % 3.62/3.86 (-. (b48_buttercup10104 zenon_X61)) % 3.62/3.86 (-. (b48_buttercup10104 zenon_X86)) % 3.62/3.86 (-. (b48_buttercup10111 zenon_X89)) % 3.62/3.86 (Tau_5 != zenon_X75) % 3.62/3.86 (-. (b48_buttercup10109 Tau_11)) % 3.62/3.86 (zenon_X81 != Tau_6) % 3.62/3.86 (Tau_3 != zenon_X59) % 3.62/3.86 (Tau_18 != zenon_X61) % 3.62/3.86 (Tau_20 != zenon_X52) % 3.62/3.86 (zenon_X63 != zenon_X22) % 3.62/3.86 (zenon_X33 != zenon_X50) % 3.62/3.86 (Tau_15 != zenon_X55) % 3.62/3.86 (zenon_X90 != zenon_X32) % 3.62/3.86 (zenon_X53 != zenon_X50) % 3.62/3.86 (Tau_10 != zenon_X56) % 3.62/3.86 (Tau_15 != zenon_X67) % 3.62/3.86 (zenon_X90 != zenon_X58) % 3.62/3.86 (Tau_16 != zenon_X45) % 3.62/3.86 (-. (b48_buttercup10102 Tau_6)) % 3.62/3.86 (zenon_X58 != zenon_X82) % 3.62/3.86 (-. (b48_buttercup10110 zenon_X59)) % 3.62/3.86 (zenon_X48 != zenon_X56) % 3.62/3.86 (zenon_X86 != zenon_X71) % 3.62/3.86 (zenon_X26 != zenon_X50) % 3.62/3.86 (zenon_X26 != Tau_0) % 3.62/3.86 (-. (b48_buttercup10107 Tau_6)) % 3.62/3.86 (zenon_X87 != zenon_X80) % 3.62/3.86 (zenon_X51 != Tau_17) % 3.62/3.86 (zenon_X28 != zenon_X50) % 3.62/3.86 (zenon_X83 != Tau_10) % 3.62/3.86 (zenon_X83 != zenon_X73) % 3.62/3.86 (zenon_X32 != Tau_1) % 3.62/3.86 (zenon_X28 != zenon_X74) % 3.62/3.86 (zenon_X66 != zenon_X86) % 3.62/3.86 (zenon_X37 != zenon_X88) % 3.62/3.86 (Tau_1 != zenon_X80) % 3.62/3.86 (zenon_X51 != zenon_X80) % 3.62/3.86 (zenon_X36 != zenon_X55) % 3.62/3.86 (zenon_X45 != zenon_X56) % 3.62/3.86 (zenon_X58 != zenon_X79) % 3.62/3.86 (-. (k04_buttercup10619 Tau_19)) % 3.62/3.86 (zenon_X47 != Tau_13) % 3.62/3.86 (zenon_X61 != Tau_20) % 3.62/3.86 (zenon_X83 != zenon_X67) % 3.62/3.86 (-. (k04_buttercup10622 zenon_X71)) % 3.62/3.86 (-. (b48_buttercup10111 Tau_14)) % 3.62/3.86 (zenon_X36 != zenon_X64) % 3.62/3.86 (zenon_X59 != zenon_X55) % 3.62/3.86 (Tau_17 != zenon_X22) % 3.62/3.86 (zenon_X53 != zenon_X71) % 3.62/3.86 (Tau_14 != zenon_X49) % 3.62/3.86 (-. (b48_buttercup10104 Tau_3)) % 3.62/3.86 (zenon_X51 != zenon_X50) % 3.62/3.86 (-. (b48_buttercup10102 Tau_17)) % 3.62/3.86 (Tau_5 != zenon_X87) % 3.62/3.86 (zenon_X60 != zenon_X65) % 3.62/3.86 (zenon_X54 != zenon_X58) % 3.62/3.86 (Tau_11 != zenon_X73) % 3.62/3.86 (-. (b48_buttercup10111 Tau_16)) % 3.62/3.86 (-. (b48_buttercup10108 zenon_X62)) % 3.62/3.86 (-. (b48_buttercup10111 zenon_X84)) % 3.62/3.86 (zenon_X57 != zenon_X47) % 3.62/3.86 (zenon_X92 != zenon_X66) % 3.62/3.86 (-. (k04_buttercup10619 Tau_2)) % 3.62/3.86 (zenon_X51 != Tau_19) % 3.62/3.86 (-. (k04_buttercup10100 zenon_X73)) % 3.62/3.86 (Tau_10 != zenon_X81) % 3.62/3.86 (zenon_X26 != zenon_X86) % 3.62/3.86 (Tau_1 != zenon_X75) % 3.62/3.86 (zenon_X53 != zenon_X79) % 3.62/3.86 (Tau_6 != zenon_X50) % 3.62/3.86 (Tau_4 != zenon_X87) % 3.62/3.86 (-. (b48_buttercup10111 zenon_X36)) % 3.62/3.86 (-. (k04_buttercup10100 zenon_X24)) % 3.62/3.86 (zenon_X25 != zenon_X87) % 3.62/3.86 (zenon_X30 != Tau_15) % 3.62/3.86 (Tau_16 != Tau_15) % 3.62/3.86 (zenon_X65 != zenon_X27) % 3.62/3.86 (zenon_X58 != zenon_X80) % 3.62/3.86 (Tau_14 != zenon_X90) % 3.62/3.86 (zenon_X72 != zenon_X75) % 3.62/3.86 (Tau_3 != Tau_19) % 3.62/3.86 (Tau_1 != zenon_X74) % 3.62/3.86 (zenon_X66 != Tau_0) % 3.62/3.86 (zenon_X90 != zenon_X25) % 3.62/3.86 (Tau_9 != Tau_19) % 3.62/3.86 (zenon_X69 != zenon_X75) % 3.62/3.86 (zenon_X83 != zenon_X33) % 3.62/3.86 (zenon_X84 != zenon_X70) % 3.62/3.86 (zenon_X57 != zenon_X62) % 3.62/3.86 (zenon_X89 != zenon_X61) % 3.62/3.86 (Tau_1 != Tau_0) % 3.62/3.86 (zenon_X26 != zenon_X45) % 3.62/3.86 (zenon_X24 != zenon_X33) % 3.62/3.86 (-. (b48_buttercup10102 zenon_X31)) % 3.62/3.86 (zenon_X53 != zenon_X73) % 3.62/3.86 (k04_buttercup10619 zenon_X24) % 3.62/3.86 (zenon_X58 != Tau_13) % 3.62/3.86 (zenon_X77 != zenon_X74) % 3.62/3.86 (zenon_X91 != zenon_X45) % 3.62/3.86 (zenon_X56 != zenon_X80) % 3.62/3.86 (Tau_6 != zenon_X69) % 3.62/3.86 (zenon_X85 != Tau_2) % 3.62/3.86 (zenon_X30 != zenon_X74) % 3.62/3.86 (zenon_X85 != zenon_X90) % 3.62/3.86 (zenon_X25 != zenon_X74) % 3.62/3.86 (zenon_X57 != zenon_X50) % 3.62/3.86 (-. (b48_buttercup10107 Tau_16)) % 3.62/3.86 (zenon_X23 != zenon_X21) % 3.62/3.86 (-. (k04_buttercup10100 zenon_X89)) % 3.62/3.86 (zenon_X81 != zenon_X78) % 3.62/3.86 (Tau_8 != Tau_16) % 3.62/3.86 (Tau_11 != zenon_X50) % 3.62/3.86 (zenon_X85 != Tau_20) % 3.62/3.86 (Tau_3 != Tau_0) % 3.62/3.86 (zenon_X81 != Tau_11) % 3.62/3.86 (-. (b48_buttercup10111 zenon_X88)) % 3.62/3.86 (-. (b48_buttercup10108 zenon_X73)) % 3.62/3.86 (-. (k04_buttercup10100 Tau_16)) % 3.62/3.86 (zenon_X71 != zenon_X67) % 3.62/3.86 (b48_buttercup10108 zenon_X23) % 3.62/3.86 (zenon_X82 != Tau_13) % 3.62/3.86 (Tau_13 != Tau_6) % 3.62/3.86 (zenon_X84 != Tau_20) % 3.62/3.86 (zenon_X37 != zenon_X79) % 3.62/3.86 (zenon_X61 != zenon_X33) % 3.62/3.86 (zenon_X46 != zenon_X47) % 3.62/3.86 (zenon_X52 != zenon_X81) % 3.62/3.86 (zenon_X53 != zenon_X74) % 3.62/3.86 (zenon_X30 != zenon_X53) % 3.62/3.86 (zenon_X31 != zenon_X80) % 3.62/3.86 (zenon_X28 != zenon_X82) % 3.62/3.86 (Tau_18 != zenon_X74) % 3.62/3.86 (zenon_X30 != Tau_10) % 3.62/3.86 (zenon_X53 != zenon_X61) % 3.62/3.86 (-. (b48_buttercup10102 zenon_X82)) % 3.62/3.86 (Tau_0 != Tau_15) % 3.62/3.86 (Tau_14 != zenon_X87) % 3.62/3.86 (zenon_X24 != zenon_X74) % 3.62/3.86 (-. (k04_buttercup10100 zenon_X25)) % 3.62/3.86 (zenon_X52 != zenon_X49) % 3.62/3.86 (zenon_X49 != zenon_X33) % 3.62/3.86 (k04_buttercup10619 Tau_15) % 3.62/3.86 (b48_buttercup10102 zenon_X74) % 3.62/3.86 (zenon_X62 != Tau_10) % 3.62/3.86 (zenon_X63 != zenon_X90) % 3.62/3.86 (k04_buttercup10100 zenon_X75) % 3.62/3.86 (zenon_X31 != zenon_X61) % 3.62/3.86 (-. (k04_buttercup10100 zenon_X55)) % 3.62/3.86 (zenon_X54 != zenon_X35) % 3.62/3.86 (zenon_X82 != Tau_17) % 3.62/3.86 (zenon_X55 != Tau_13) % 3.62/3.86 (zenon_X25 != zenon_X67) % 3.62/3.86 (zenon_X27 != zenon_X73) % 3.62/3.86 (zenon_X58 != zenon_X46) % 3.62/3.86 (zenon_X52 != zenon_X92) % 3.62/3.86 (zenon_X79 != Tau_20) % 3.62/3.86 (zenon_X62 != zenon_X46) % 3.62/3.86 (zenon_X32 != zenon_X22) % 3.62/3.86 (Tau_17 != zenon_X81) % 3.62/3.86 (zenon_X92 != Tau_1) % 3.62/3.86 (zenon_X72 != zenon_X64) % 3.62/3.86 (-. (b48_buttercup10107 zenon_X69)) % 3.62/3.86 (k04_buttercup10619 zenon_X88) % 3.62/3.86 (Tau_6 != zenon_X57) % 3.62/3.86 (-. (b48_buttercup10109 zenon_X76)) % 3.62/3.86 (zenon_X82 != Tau_15) % 3.62/3.86 (zenon_X79 != Tau_2) % 3.62/3.86 (zenon_X81 != zenon_X69) % 3.62/3.86 (-. (b48_buttercup10102 zenon_X35)) % 3.62/3.86 (zenon_X62 != zenon_X73) % 3.62/3.86 (Tau_8 != zenon_X53) % 3.62/3.86 (zenon_X28 != zenon_X47) % 3.62/3.86 (zenon_X71 != zenon_X75) % 3.62/3.86 (Tau_8 != zenon_X49) % 3.62/3.86 (Tau_14 != zenon_X77) % 3.62/3.86 (-. (k04_buttercup10100 zenon_X60)) % 3.62/3.86 (zenon_X31 != zenon_X23) % 3.62/3.86 (Tau_0 != zenon_X74) % 3.62/3.86 (zenon_X81 != zenon_X54) % 3.62/3.86 (zenon_X88 != Tau_17) % 3.62/3.86 (zenon_X48 != Tau_16) % 3.62/3.86 (k04_buttercup10622 zenon_X74) % 3.62/3.86 (zenon_X85 != zenon_X35) % 3.62/3.86 (zenon_X76 != zenon_X35) % 3.62/3.86 (zenon_X53 != zenon_X57) % 3.62/3.86 (Tau_6 != zenon_X36) % 3.62/3.86 (zenon_X23 != zenon_X64) % 3.62/3.86 (zenon_X88 != zenon_X81) % 3.62/3.86 (zenon_X66 != zenon_X64) % 3.62/3.86 (zenon_X78 != zenon_X85) % 3.62/3.86 (zenon_X57 != zenon_X81) % 3.62/3.86 (zenon_X72 != Tau_17) % 3.62/3.86 (zenon_X59 != zenon_X73) % 3.62/3.86 (Tau_19 != zenon_X62) % 3.62/3.86 (-. (b48_buttercup10110 zenon_X64)) % 3.62/3.86 (-. (b48_buttercup10107 Tau_13)) % 3.62/3.86 (-. (b48_buttercup10110 zenon_X62)) % 3.62/3.86 (Tau_9 != Tau_1) % 3.62/3.86 (Tau_20 != zenon_X70) % 3.62/3.86 (zenon_X77 != zenon_X64) % 3.62/3.86 (zenon_X54 != Tau_20) % 3.62/3.86 (b48_buttercup10108 zenon_X77) % 3.62/3.86 (Tau_19 != zenon_X64) % 3.62/3.86 (Tau_17 != zenon_X45) % 3.62/3.86 (zenon_X66 != zenon_X87) % 3.62/3.86 (zenon_X73 != zenon_X55) % 3.62/3.86 (Tau_11 != Tau_4) % 3.62/3.86 (Tau_10 != Tau_13) % 3.62/3.86 (Tau_7 != zenon_X50) % 3.62/3.86 (Tau_3 != zenon_X75) % 3.62/3.86 (zenon_X58 != zenon_X51) % 3.62/3.86 (zenon_X78 != zenon_X45) % 3.62/3.86 (zenon_X72 != zenon_X88) % 3.62/3.86 (zenon_X85 != Tau_8) % 3.62/3.86 (-. (b48_buttercup10109 zenon_X64)) % 3.62/3.86 (b48_buttercup10110 zenon_X55) % 3.62/3.86 (zenon_X32 != zenon_X27) % 3.62/3.86 (-. (b48_buttercup10111 zenon_X74)) % 3.62/3.86 (zenon_X32 != zenon_X85) % 3.62/3.86 (-. (b48_buttercup10109 zenon_X49)) % 3.62/3.86 (zenon_X23 != zenon_X63) % 3.62/3.86 (Tau_17 != zenon_X50) % 3.62/3.86 (zenon_X48 != zenon_X64) % 3.62/3.86 (Tau_19 != zenon_X48) % 3.62/3.86 (k04_buttercup10622 zenon_X78) % 3.62/3.86 (-. (b48_buttercup10102 zenon_X70)) % 3.62/3.86 (Tau_18 != Tau_5) % 3.62/3.86 (zenon_X51 != zenon_X57) % 3.62/3.86 (zenon_X53 != zenon_X22) % 3.62/3.86 (Tau_7 != zenon_X70) % 3.62/3.86 (-. (k04_buttercup10100 zenon_X82)) % 3.62/3.86 (-. (b48_buttercup10104 zenon_X83)) % 3.62/3.86 (zenon_X52 != zenon_X85) % 3.62/3.86 (Tau_3 != Tau_10) % 3.62/3.86 (zenon_X58 != zenon_X57) % 3.62/3.86 (zenon_X60 != zenon_X63) % 3.62/3.86 (zenon_X50 != zenon_X86) % 3.62/3.86 (zenon_X35 != zenon_X36) % 3.62/3.86 (zenon_X77 != zenon_X81) % 3.62/3.86 (Tau_5 != zenon_X67) % 3.62/3.86 (zenon_X60 != zenon_X46) % 3.62/3.86 (zenon_X36 != zenon_X57) % 3.62/3.86 (zenon_X79 != Tau_0) % 3.62/3.86 (zenon_X65 != zenon_X64) % 3.62/3.86 (-. (b48_buttercup10109 Tau_5)) % 3.62/3.86 (zenon_X35 != Tau_18) % 3.62/3.86 (Tau_8 != zenon_X64) % 3.62/3.86 (zenon_X88 != Tau_19) % 3.62/3.86 (zenon_X23 != zenon_X76) % 3.62/3.86 (zenon_X27 != zenon_X85) % 3.62/3.86 (zenon_X77 != Tau_1) % 3.62/3.86 (zenon_X71 != zenon_X49) % 3.62/3.86 (zenon_X91 != zenon_X22) % 3.62/3.86 (zenon_X76 != zenon_X49) % 3.62/3.86 (zenon_X23 != zenon_X80) % 3.62/3.86 (zenon_X76 != zenon_X68) % 3.62/3.86 (zenon_X21 != Tau_7) % 3.62/3.86 (zenon_X72 != zenon_X70) % 3.62/3.86 (b48_buttercup10104 zenon_X82) % 3.62/3.86 (zenon_X77 != zenon_X67) % 3.62/3.86 (-. (b48_buttercup10110 Tau_16)) % 3.62/3.86 (zenon_X77 != Tau_19) % 3.62/3.86 (zenon_X28 != zenon_X77) % 3.62/3.86 (k04_buttercup10622 Tau_16) % 3.62/3.86 (zenon_X59 != Tau_0) % 3.62/3.86 (zenon_X66 != Tau_2) % 3.62/3.86 (zenon_X72 != zenon_X83) % 3.62/3.86 (zenon_X33 != zenon_X53) % 3.62/3.86 (zenon_X88 != zenon_X68) % 3.62/3.86 (zenon_X50 != zenon_X74) % 3.62/3.86 (zenon_X78 != zenon_X82) % 3.62/3.86 (b48_buttercup10104 zenon_X63) % 3.62/3.86 (zenon_X25 != zenon_X63) % 3.62/3.86 (zenon_X30 != zenon_X62) % 3.62/3.86 (Tau_16 != zenon_X47) % 3.62/3.86 (zenon_X21 != Tau_6) % 3.62/3.86 (-. (k04_buttercup10100 zenon_X85)) % 3.62/3.86 (-. (b48_buttercup10108 zenon_X84)) % 3.62/3.86 (zenon_X71 != Tau_17) % 3.62/3.86 (Tau_11 != zenon_X70) % 3.62/3.86 (zenon_X84 != zenon_X75) % 3.62/3.86 (zenon_X65 != zenon_X86) % 3.62/3.86 (zenon_X49 != Tau_13) % 3.62/3.86 (Tau_19 != zenon_X50) % 3.62/3.86 (zenon_X79 != Tau_19) % 3.62/3.86 (-. (b48_buttercup10110 Tau_17)) % 3.62/3.86 (zenon_X91 != zenon_X75) % 3.62/3.86 (Tau_7 != zenon_X83) % 3.62/3.86 (zenon_X86 != Tau_0) % 3.62/3.86 (Tau_16 != zenon_X73) % 3.62/3.86 (zenon_X60 != zenon_X70) % 3.62/3.86 (zenon_X31 != zenon_X77) % 3.62/3.86 (Tau_4 != zenon_X76) % 3.62/3.86 (Tau_5 != zenon_X77) % 3.62/3.86 (zenon_X32 != Tau_17) % 3.62/3.86 (zenon_X83 != zenon_X22) % 3.62/3.86 (zenon_X70 != zenon_X46) % 3.62/3.86 (zenon_X31 != zenon_X88) % 3.62/3.86 (b48_buttercup10111 zenon_X92) % 3.62/3.86 (zenon_X37 != zenon_X80) % 3.62/3.86 (zenon_X63 != zenon_X67) % 3.62/3.86 (zenon_X21 != zenon_X49) % 3.62/3.86 (zenon_X59 != Tau_8) % 3.62/3.86 (Tau_6 != zenon_X83) % 3.62/3.86 (-. (b48_buttercup10109 Tau_10)) % 3.62/3.86 (zenon_X87 != Tau_15) % 3.62/3.86 (zenon_X61 != zenon_X22) % 3.62/3.86 (-. (b48_buttercup10102 Tau_11)) % 3.62/3.86 (zenon_X25 != zenon_X69) % 3.62/3.86 (Tau_13 != zenon_X53) % 3.62/3.86 (zenon_X30 != zenon_X82) % 3.62/3.86 (Tau_14 != Tau_19) % 3.62/3.86 (zenon_X61 != Tau_2) % 3.62/3.86 (Tau_3 != zenon_X53) % 3.62/3.86 (Tau_4 != zenon_X49) % 3.62/3.86 (Tau_4 != zenon_X81) % 3.62/3.86 (zenon_X53 != zenon_X64) % 3.62/3.86 (zenon_X81 != zenon_X66) % 3.62/3.86 (b48_buttercup10104 zenon_X76) % 3.62/3.86 (zenon_X28 != zenon_X25) % 3.62/3.86 (zenon_X87 != zenon_X86) % 3.62/3.86 (zenon_X26 != zenon_X74) % 3.62/3.86 (zenon_X76 != zenon_X69) % 3.62/3.86 (-. (b48_buttercup10102 zenon_X64)) % 3.62/3.86 (-. (b48_buttercup10109 Tau_18)) % 3.62/3.86 (zenon_X52 != zenon_X67) % 3.62/3.86 (-. (b48_buttercup10108 Tau_0)) % 3.62/3.86 (zenon_X30 != Tau_16) % 3.62/3.86 (zenon_X24 != zenon_X86) % 3.62/3.86 (zenon_X55 != zenon_X68) % 3.62/3.86 (Tau_6 != zenon_X79) % 3.62/3.86 (zenon_X65 != Tau_15) % 3.62/3.86 (Tau_16 != zenon_X79) % 3.62/3.86 (zenon_X52 != zenon_X79) % 3.62/3.86 (zenon_X65 != zenon_X21) % 3.62/3.86 (k04_buttercup10100 zenon_X22) % 3.62/3.86 (k04_buttercup10622 zenon_X51) % 3.62/3.86 (zenon_X26 != zenon_X67) % 3.62/3.86 (zenon_X86 != zenon_X90) % 3.62/3.86 (-. (b48_buttercup10104 zenon_X30)) % 3.62/3.86 (Tau_19 != Tau_0) % 3.62/3.86 (zenon_X31 != zenon_X52) % 3.62/3.86 (Tau_13 != zenon_X70) % 3.62/3.86 (zenon_X30 != Tau_13) % 3.62/3.86 (k04_buttercup10622 zenon_X48) % 3.62/3.86 (zenon_X69 != Tau_13) % 3.62/3.86 (zenon_X31 != zenon_X50) % 3.62/3.86 (zenon_X64 != zenon_X50) % 3.62/3.86 (k04_buttercup10619 zenon_X49) % 3.62/3.86 (k04_buttercup10622 zenon_X25) % 3.62/3.86 (-. (b48_buttercup10111 Tau_4)) % 3.62/3.86 (Tau_20 != zenon_X22) % 3.62/3.86 (zenon_X31 != zenon_X47) % 3.62/3.86 (Tau_15 != zenon_X61) % 3.62/3.86 (zenon_X53 != zenon_X81) % 3.62/3.86 (zenon_X53 != Tau_1) % 3.62/3.86 (k04_buttercup10622 zenon_X54) % 3.62/3.86 (-. (b48_buttercup10109 Tau_4)) % 3.62/3.86 (Tau_3 != zenon_X62) % 3.62/3.86 (zenon_X61 != zenon_X35) % 3.62/3.86 (zenon_X51 != zenon_X63) % 3.62/3.86 (-. (k04_buttercup10100 Tau_7)) % 3.62/3.86 (-. (k04_buttercup10622 Tau_20)) % 3.62/3.86 (zenon_X66 != zenon_X24) % 3.62/3.86 (k04_buttercup10622 zenon_X72) % 3.62/3.86 (zenon_X37 != Tau_2) % 3.62/3.86 (-. (b48_buttercup10104 zenon_X66)) % 3.62/3.86 (Tau_11 != zenon_X85) % 3.62/3.86 (zenon_X37 != zenon_X73) % 3.62/3.86 (zenon_X73 != zenon_X21) % 3.62/3.86 (-. (b48_buttercup10111 zenon_X47)) % 3.62/3.86 (Tau_5 != zenon_X45) % 3.62/3.86 (zenon_X54 != zenon_X56) % 3.62/3.86 (Tau_20 != zenon_X27) % 3.62/3.86 (zenon_X60 != Tau_16) % 3.62/3.86 (zenon_X32 != Tau_0) % 3.62/3.86 (-. (b48_buttercup10111 zenon_X60)) % 3.62/3.86 (Tau_1 != zenon_X81) % 3.62/3.86 (zenon_X36 != zenon_X87) % 3.62/3.86 (-. (b48_buttercup10107 zenon_X64)) % 3.62/3.86 (zenon_X24 != Tau_17) % 3.62/3.86 (-. (b48_buttercup10108 Tau_20)) % 3.62/3.86 (zenon_X62 != zenon_X68) % 3.62/3.86 (-. (k04_buttercup10622 zenon_X87)) % 3.62/3.86 (-. (b48_buttercup10102 zenon_X91)) % 3.62/3.86 (zenon_X25 != zenon_X50) % 3.62/3.86 (zenon_X35 != Tau_11) % 3.62/3.86 (zenon_X60 != zenon_X88) % 3.62/3.86 (-. (b48_buttercup10107 zenon_X76)) % 3.62/3.86 (zenon_X52 != zenon_X62) % 3.62/3.86 (Tau_11 != Tau_20) % 3.62/3.86 (zenon_X36 != Tau_2) % 3.62/3.86 (zenon_X21 != zenon_X28) % 3.62/3.86 (Tau_6 != zenon_X85) % 3.62/3.86 (zenon_X83 != zenon_X46) % 3.62/3.86 (zenon_X30 != zenon_X88) % 3.62/3.86 (k04_buttercup10622 zenon_X28) % 3.62/3.86 (Tau_1 != zenon_X22) % 3.62/3.86 (b48_buttercup10110 Tau_9) % 3.62/3.86 (zenon_X63 != Tau_13) % 3.62/3.86 (-. (b48_buttercup10102 zenon_X78)) % 3.62/3.86 (zenon_X26 != zenon_X65) % 3.62/3.86 (Tau_1 != zenon_X21) % 3.62/3.86 (Tau_18 != Tau_1) % 3.62/3.86 (zenon_X66 != zenon_X27) % 3.62/3.86 (zenon_X85 != zenon_X47) % 3.62/3.86 (k04_buttercup10619 zenon_X69) % 3.62/3.86 (zenon_X64 != zenon_X86) % 3.62/3.86 (Tau_9 != Tau_17) % 3.62/3.86 (zenon_X65 != Tau_17) % 3.62/3.86 (Tau_7 != zenon_X79) % 3.62/3.86 (zenon_X21 != Tau_9) % 3.62/3.86 (zenon_X71 != zenon_X70) % 3.62/3.86 (Tau_9 != Tau_18) % 3.62/3.86 (zenon_X53 != Tau_15) % 3.62/3.86 (-. (k04_buttercup10100 Tau_15)) % 3.62/3.86 (Tau_11 != zenon_X22) % 3.62/3.86 (zenon_X53 != zenon_X69) % 3.62/3.86 (zenon_X72 != zenon_X33) % 3.62/3.86 (Tau_2 != zenon_X80) % 3.62/3.86 (zenon_X80 != zenon_X79) % 3.62/3.86 (zenon_X54 != Tau_1) % 3.62/3.86 (zenon_X25 != zenon_X49) % 3.62/3.86 (zenon_X35 != zenon_X80) % 3.62/3.86 (b48_buttercup10102 zenon_X47) % 3.62/3.86 (zenon_X91 != zenon_X49) % 3.62/3.86 (zenon_X77 != zenon_X52) % 3.62/3.86 (-. (b48_buttercup10102 zenon_X63)) % 3.62/3.86 (zenon_X46 != zenon_X75) % 3.62/3.86 (zenon_X79 != zenon_X92) % 3.62/3.86 (-. (b48_buttercup10111 zenon_X71)) % 3.62/3.86 (zenon_X63 != zenon_X35) % 3.62/3.86 (Tau_15 != Tau_13) % 3.62/3.86 (zenon_X21 != Tau_5) % 3.62/3.86 (zenon_X31 != Tau_8) % 3.62/3.86 (zenon_X28 != zenon_X68) % 3.62/3.86 (-. (b48_buttercup10107 zenon_X27)) % 3.62/3.86 (zenon_X82 != zenon_X47) % 3.62/3.86 (Tau_17 != zenon_X87) % 3.62/3.86 (Tau_7 != zenon_X88) % 3.62/3.86 (Tau_5 != zenon_X85) % 3.62/3.86 (zenon_X72 != zenon_X52) % 3.62/3.86 (zenon_X79 != zenon_X71) % 3.62/3.86 (zenon_X33 != zenon_X32) % 3.62/3.86 (zenon_X24 != zenon_X56) % 3.62/3.86 (zenon_X60 != zenon_X69) % 3.62/3.86 (zenon_X45 != zenon_X74) % 3.62/3.86 (zenon_X78 != Tau_8) % 3.62/3.86 (-. (b48_buttercup10107 zenon_X23)) % 3.62/3.86 (zenon_X28 != zenon_X79) % 3.62/3.86 (zenon_X89 != zenon_X50) % 3.62/3.86 (b48_buttercup10108 zenon_X83) % 3.62/3.86 (zenon_X88 != zenon_X33) % 3.62/3.86 (Tau_2 != Tau_14) % 3.62/3.86 (zenon_X32 != zenon_X74) % 3.62/3.86 (Tau_6 != Tau_10) % 3.62/3.86 (Tau_9 != zenon_X22) % 3.62/3.86 (zenon_X31 != zenon_X82) % 3.62/3.86 (zenon_X35 != zenon_X49) % 3.62/3.86 (Tau_14 != zenon_X47) % 3.62/3.86 (zenon_X60 != zenon_X50) % 3.62/3.86 (b48_buttercup10109 Tau_8) % 3.62/3.86 (Tau_2 != Tau_10) % 3.62/3.86 (zenon_X68 != Tau_0) % 3.62/3.86 (zenon_X31 != Tau_0) % 3.62/3.86 (Tau_4 != Tau_20) % 3.62/3.86 (-. (b48_buttercup10102 zenon_X89)) % 3.62/3.86 (zenon_X50 != Tau_15) % 3.62/3.86 (zenon_X51 != zenon_X47) % 3.62/3.86 (Tau_13 != zenon_X48) % 3.62/3.86 (zenon_X24 != zenon_X22) % 3.62/3.86 (zenon_X64 != zenon_X74) % 3.62/3.86 (zenon_X30 != zenon_X89) % 3.62/3.86 (-. (b48_buttercup10107 zenon_X48)) % 3.62/3.86 (zenon_X26 != zenon_X82) % 3.62/3.86 (zenon_X21 != Tau_3) % 3.62/3.86 (-. (b48_buttercup10107 zenon_X72)) % 3.62/3.86 (zenon_X48 != zenon_X79) % 3.62/3.86 (zenon_X71 != zenon_X47) % 3.62/3.86 (zenon_X26 != zenon_X56) % 3.62/3.86 (Tau_11 != zenon_X88) % 3.62/3.86 (zenon_X86 != Tau_13) % 3.62/3.86 (zenon_X84 != Tau_17) % 3.62/3.86 (zenon_X77 != zenon_X56) % 3.62/3.86 (zenon_X61 != zenon_X67) % 3.62/3.86 (zenon_X57 != zenon_X61) % 3.62/3.86 (-. (b48_buttercup10108 zenon_X67)) % 3.62/3.86 (Tau_7 != zenon_X46) % 3.62/3.86 (-. (b48_buttercup10110 zenon_X21)) % 3.62/3.86 (Tau_10 != zenon_X22) % 3.62/3.86 (Tau_6 != zenon_X53) % 3.62/3.86 (b48_buttercup10110 zenon_X54) % 3.62/3.86 (zenon_X63 != zenon_X75) % 3.62/3.86 (zenon_X86 != Tau_19) % 3.62/3.86 (-. (b48_buttercup10102 zenon_X22)) % 3.62/3.86 (Tau_6 != zenon_X70) % 3.62/3.86 (Tau_5 != zenon_X52) % 3.62/3.86 (zenon_X65 != zenon_X80) % 3.62/3.86 (zenon_X24 != zenon_X69) % 3.62/3.86 (zenon_X54 != zenon_X36) % 3.62/3.86 (zenon_X58 != zenon_X63) % 3.62/3.86 (zenon_X79 != zenon_X90) % 3.62/3.86 (Tau_6 != zenon_X75) % 3.62/3.86 (zenon_X65 != zenon_X74) % 3.62/3.86 (zenon_X51 != Tau_16) % 3.62/3.86 (zenon_X86 != zenon_X22) % 3.62/3.86 (zenon_X36 != zenon_X75) % 3.62/3.86 (zenon_X80 != zenon_X92) % 3.62/3.86 (zenon_X58 != zenon_X21) % 3.62/3.86 (-. (b48_buttercup10102 zenon_X50)) % 3.62/3.86 (b48_buttercup10108 Tau_18) % 3.62/3.86 (zenon_X26 != Tau_15) % 3.62/3.86 (zenon_X76 != Tau_13) % 3.62/3.86 (zenon_X92 != Tau_3) % 3.62/3.86 (Tau_7 != zenon_X68) % 3.62/3.86 (Tau_3 != zenon_X67) % 3.62/3.86 (Tau_7 != Tau_13) % 3.62/3.86 (b48_buttercup10108 zenon_X70) % 3.62/3.86 (zenon_X63 != Tau_19) % 3.62/3.86 (zenon_X78 != Tau_16) % 3.62/3.86 (-. (b48_buttercup10107 zenon_X37)) % 3.62/3.86 (-. (b48_buttercup10102 zenon_X36)) % 3.62/3.86 (zenon_X35 != zenon_X87) % 3.62/3.86 (zenon_X21 != zenon_X30) % 3.62/3.86 (Tau_1 != zenon_X52) % 3.62/3.86 (zenon_X60 != zenon_X25) % 3.62/3.86 (zenon_X30 != zenon_X56) % 3.62/3.86 (zenon_X71 != zenon_X87) % 3.62/3.86 (zenon_X27 != zenon_X75) % 3.62/3.86 (zenon_X80 != zenon_X75) % 3.62/3.86 (zenon_X69 != zenon_X87) % 3.62/3.86 (-. (k04_buttercup10100 zenon_X78)) % 3.62/3.86 (zenon_X36 != Tau_20) % 3.62/3.86 (zenon_X86 != Tau_8) % 3.62/3.86 (zenon_X66 != zenon_X80) % 3.62/3.86 (b48_buttercup10110 Tau_11) % 3.62/3.86 (-. (b48_buttercup10104 zenon_X81)) % 3.62/3.86 (zenon_X33 != zenon_X69) % 3.62/3.86 (zenon_X66 != zenon_X22) % 3.62/3.86 (Tau_11 != Tau_2) % 3.62/3.86 (-. (b48_buttercup10107 Tau_19)) % 3.62/3.86 (zenon_X91 != zenon_X74) % 3.62/3.86 (zenon_X83 != zenon_X69) % 3.62/3.86 (Tau_3 != zenon_X64) % 3.62/3.86 (zenon_X25 != zenon_X86) % 3.62/3.86 (zenon_X21 != zenon_X69) % 3.62/3.86 (zenon_X77 != zenon_X33) % 3.62/3.86 (zenon_X35 != Tau_5) % 3.62/3.86 (zenon_X79 != zenon_X33) % 3.62/3.86 (Tau_15 != zenon_X22) % 3.62/3.86 (k04_buttercup10100 zenon_X50) % 3.62/3.86 (zenon_X71 != Tau_10) % 3.62/3.86 (-. (k04_buttercup10100 zenon_X76)) % 3.62/3.86 (Tau_10 != zenon_X45) % 3.62/3.86 (zenon_X90 != zenon_X50) % 3.62/3.86 (zenon_X25 != zenon_X46) % 3.62/3.86 (zenon_X82 != Tau_8) % 3.62/3.86 (-. (b48_buttercup10111 zenon_X25)) % 3.62/3.86 (Tau_18 != zenon_X73) % 3.62/3.86 (zenon_X63 != zenon_X47) % 3.62/3.86 (Tau_9 != Tau_4) % 3.62/3.86 (zenon_X26 != zenon_X47) % 3.62/3.86 (Tau_8 != Tau_17) % 3.62/3.86 (Tau_2 != zenon_X56) % 3.62/3.86 (zenon_X78 != zenon_X22) % 3.62/3.86 (-. (b48_buttercup10107 Tau_9)) % 3.62/3.86 (zenon_X36 != zenon_X27) % 3.62/3.86 (Tau_2 != zenon_X74) % 3.62/3.86 (zenon_X30 != Tau_1) % 3.62/3.86 (zenon_X91 != zenon_X80) % 3.62/3.86 (-. (b48_buttercup10104 zenon_X89)) % 3.62/3.86 (-. (b48_buttercup10104 zenon_X56)) % 3.62/3.86 (Tau_14 != zenon_X69) % 3.62/3.86 (Tau_3 != zenon_X74) % 3.62/3.86 (Tau_5 != zenon_X91) % 3.62/3.86 (zenon_X79 != zenon_X75) % 3.62/3.86 (Tau_18 != zenon_X86) % 3.62/3.86 (k04_buttercup10100 Tau_0) % 3.62/3.86 (zenon_X90 != Tau_16) % 3.62/3.86 (Tau_17 != Tau_20) % 3.62/3.86 (zenon_X90 != Tau_10) % 3.62/3.86 (Tau_13 != zenon_X89) % 3.62/3.86 (zenon_X66 != zenon_X70) % 3.62/3.86 (zenon_X78 != Tau_4) % 3.62/3.86 (Tau_10 != Tau_14) % 3.62/3.86 (-. (b48_buttercup10111 zenon_X65)) % 3.62/3.86 (zenon_X81 != zenon_X60) % 3.62/3.86 (zenon_X31 != Tau_4) % 3.62/3.86 (zenon_X31 != zenon_X22) % 3.62/3.86 (zenon_X74 != zenon_X85) % 3.62/3.86 (zenon_X31 != zenon_X70) % 3.62/3.86 (zenon_X91 != Tau_8) % 3.62/3.86 (zenon_X78 != Tau_17) % 3.62/3.86 (-. (b48_buttercup10104 zenon_X78)) % 3.62/3.86 (zenon_X36 != Tau_0) % 3.62/3.86 (-. (b48_buttercup10111 Tau_20)) % 3.62/3.86 (zenon_X82 != zenon_X74) % 3.62/3.86 (zenon_X51 != zenon_X68) % 3.62/3.86 (zenon_X92 != Tau_19) % 3.62/3.86 (zenon_X86 != zenon_X75) % 3.62/3.86 (zenon_X90 != zenon_X48) % 3.62/3.86 (-. (b48_buttercup10108 zenon_X69)) % 3.62/3.86 (zenon_X32 != Tau_13) % 3.62/3.86 (zenon_X54 != zenon_X90) % 3.62/3.86 (zenon_X71 != zenon_X74) % 3.62/3.86 (-. (b48_buttercup10108 zenon_X54)) % 3.62/3.86 (-. (b48_buttercup10109 zenon_X21)) % 3.62/3.86 (zenon_X27 != Tau_10) % 3.62/3.86 (k04_buttercup10622 zenon_X63) % 3.62/3.86 (zenon_X66 != zenon_X67) % 3.62/3.86 (zenon_X72 != Tau_19) % 3.62/3.86 (Tau_7 != zenon_X62) % 3.62/3.86 (Tau_3 != zenon_X61) % 3.62/3.86 (Tau_3 != Tau_8) % 3.62/3.86 (zenon_X45 != zenon_X80) % 3.62/3.86 (-. (k04_buttercup10100 Tau_3)) % 3.62/3.86 (zenon_X30 != zenon_X49) % 3.62/3.86 (-. (b48_buttercup10111 zenon_X24)) % 3.62/3.86 (Tau_6 != zenon_X91) % 3.62/3.86 (Tau_6 != zenon_X68) % 3.62/3.86 (-. (b48_buttercup10107 zenon_X47)) % 3.62/3.86 (zenon_X91 != zenon_X55) % 3.62/3.86 (Tau_18 != zenon_X64) % 3.62/3.86 (zenon_X26 != zenon_X68) % 3.62/3.86 (zenon_X26 != Tau_8) % 3.62/3.86 (-. (b48_buttercup10109 zenon_X23)) % 3.62/3.86 (zenon_X89 != Tau_0) % 3.62/3.86 (b48_buttercup10102 zenon_X49) % 3.62/3.86 (zenon_X25 != zenon_X55) % 3.62/3.86 (zenon_X33 != zenon_X30) % 3.62/3.86 (-. (k04_buttercup10100 zenon_X68)) % 3.62/3.86 (zenon_X92 != zenon_X72) % 3.62/3.86 (zenon_X59 != Tau_1) % 3.62/3.86 (zenon_X82 != zenon_X90) % 3.62/3.86 (zenon_X23 != zenon_X33) % 3.62/3.86 (Tau_2 != Tau_17) % 3.62/3.86 (zenon_X66 != Tau_18) % 3.62/3.86 (zenon_X91 != zenon_X61) % 3.62/3.86 (-. (k04_buttercup10622 zenon_X35)) % 3.62/3.86 (zenon_X54 != zenon_X25) % 3.62/3.86 (zenon_X32 != zenon_X70) % 3.62/3.86 (-. (b48_buttercup10107 zenon_X86)) % 3.62/3.86 (Tau_5 != zenon_X56) % 3.62/3.86 (zenon_X57 != zenon_X55) % 3.62/3.86 (Tau_2 != Tau_15) % 3.62/3.86 (-. (b48_buttercup10102 zenon_X23)) % 3.62/3.86 (zenon_X48 != Tau_17) % 3.62/3.86 (zenon_X65 != zenon_X82) % 3.62/3.86 (Tau_14 != zenon_X85) % 3.62/3.86 (zenon_X48 != zenon_X49) % 3.62/3.86 (zenon_X28 != zenon_X83) % 3.62/3.86 (zenon_X70 != zenon_X55) % 3.62/3.86 (zenon_X30 != zenon_X87) % 3.62/3.86 (-. (b48_buttercup10108 Tau_9)) % 3.62/3.86 (zenon_X24 != zenon_X75) % 3.62/3.86 (zenon_X31 != zenon_X56) % 3.62/3.86 (Tau_5 != Tau_8) % 3.62/3.86 (zenon_X65 != zenon_X49) % 3.62/3.86 (Tau_5 != zenon_X83) % 3.62/3.86 (zenon_X25 != zenon_X79) % 3.62/3.86 (zenon_X90 != zenon_X67) % 3.62/3.86 (Tau_11 != zenon_X87) % 3.62/3.86 (Tau_1 != zenon_X57) % 3.62/3.86 (zenon_X35 != Tau_17) % 3.62/3.86 (-. (b48_buttercup10111 zenon_X82)) % 3.62/3.86 (-. (b48_buttercup10109 zenon_X62)) % 3.62/3.86 (zenon_X28 != zenon_X67) % 3.62/3.86 (-. (b48_buttercup10107 zenon_X75)) % 3.62/3.86 (zenon_X59 != zenon_X69) % 3.62/3.86 (zenon_X76 != Tau_19) % 3.62/3.86 (zenon_X74 != zenon_X46) % 3.62/3.86 (-. (b48_buttercup10108 zenon_X64)) % 3.62/3.86 (zenon_X89 != zenon_X27) % 3.62/3.86 (-. (b48_buttercup10107 zenon_X32)) % 3.62/3.86 (b48_buttercup10102 zenon_X69) % 3.62/3.86 (-. (b48_buttercup10109 zenon_X50)) % 3.62/3.86 (-. (b48_buttercup10111 Tau_3)) % 3.62/3.86 (zenon_X48 != zenon_X59) % 3.62/3.86 (b48_buttercup10110 Tau_6) % 3.62/3.86 (zenon_X35 != zenon_X66) % 3.62/3.86 (-. (b48_buttercup10107 zenon_X59)) % 3.62/3.86 (zenon_X78 != zenon_X57) % 3.62/3.86 (Tau_9 != zenon_X70) % 3.62/3.86 (-. (b48_buttercup10104 zenon_X68)) % 3.62/3.86 (Tau_17 != zenon_X56) % 3.62/3.86 (zenon_X28 != Tau_0) % 3.62/3.86 (zenon_X58 != zenon_X33) % 3.62/3.86 (-. (k04_buttercup10100 zenon_X69)) % 3.62/3.86 (-. (b48_buttercup10102 zenon_X73)) % 3.62/3.86 (zenon_X78 != zenon_X36) % 3.62/3.86 (Tau_14 != zenon_X88) % 3.62/3.86 (-. (b48_buttercup10108 zenon_X72)) % 3.62/3.86 (zenon_X35 != zenon_X70) % 3.62/3.86 (zenon_X82 != zenon_X21) % 3.62/3.86 (zenon_X32 != Tau_4) % 3.62/3.86 (Tau_9 != zenon_X76) % 3.62/3.86 (-. (b48_buttercup10107 zenon_X28)) % 3.62/3.86 (zenon_X32 != Tau_15) % 3.62/3.86 (zenon_X64 != zenon_X22) % 3.62/3.86 (b48_buttercup10098 zenon_X34) % 3.62/3.86 (Tau_17 != zenon_X69) % 3.62/3.86 (Tau_0 != Tau_17) % 3.62/3.86 (zenon_X89 != zenon_X55) % 3.62/3.86 (zenon_X58 != Tau_10) % 3.62/3.86 (k04_buttercup10622 zenon_X77) % 3.62/3.86 (-. (b48_buttercup10111 zenon_X27)) % 3.62/3.86 (zenon_X88 != zenon_X75) % 3.62/3.86 (zenon_X89 != zenon_X80) % 3.62/3.86 (zenon_X37 != zenon_X27) % 3.62/3.86 (zenon_X62 != zenon_X85) % 3.62/3.86 (Tau_20 != zenon_X89) % 3.62/3.86 (zenon_X37 != Tau_18) % 3.62/3.86 (zenon_X45 != zenon_X47) % 3.62/3.86 (zenon_X26 != zenon_X58) % 3.62/3.86 (Tau_18 != zenon_X85) % 3.62/3.86 (zenon_X90 != zenon_X56) % 3.62/3.86 (zenon_X36 != zenon_X67) % 3.62/3.86 (k04_buttercup10622 zenon_X32) % 3.62/3.86 (zenon_X65 != zenon_X46) % 3.62/3.86 (zenon_X92 != zenon_X84) % 3.62/3.86 (Tau_20 != zenon_X53) % 3.62/3.86 (Tau_7 != zenon_X67) % 3.62/3.86 (-. (k04_buttercup10622 Tau_10)) % 3.62/3.86 (-. (b48_buttercup10109 zenon_X52)) % 3.62/3.86 (zenon_X36 != zenon_X46) % 3.62/3.86 (-. (b48_buttercup10111 zenon_X32)) % 3.62/3.86 (-. (k04_buttercup10619 zenon_X56)) % 3.62/3.86 (zenon_X30 != Tau_0) % 3.62/3.86 (zenon_X51 != zenon_X45) % 3.62/3.86 (zenon_X56 != zenon_X27) % 3.62/3.86 (zenon_X37 != Tau_10) % 3.62/3.86 (Tau_3 != zenon_X47) % 3.62/3.86 (zenon_X26 != zenon_X75) % 3.62/3.86 (zenon_X58 != zenon_X69) % 3.62/3.86 (zenon_X33 != zenon_X84) % 3.62/3.86 (k04_buttercup10619 zenon_X58) % 3.62/3.86 (zenon_X35 != zenon_X67) % 3.62/3.86 (zenon_X90 != zenon_X69) % 3.62/3.86 (Tau_3 != Tau_20) % 3.62/3.86 (-. (b48_buttercup10104 zenon_X21)) % 3.62/3.86 (Tau_18 != zenon_X49) % 3.62/3.86 (-. (b48_buttercup10102 Tau_10)) % 3.62/3.86 (-. (b48_buttercup10109 zenon_X86)) % 3.62/3.86 (-. (b48_buttercup10108 zenon_X28)) % 3.62/3.86 (-. (b48_buttercup10107 zenon_X55)) % 3.62/3.86 (-. (b48_buttercup10111 zenon_X51)) % 3.62/3.86 (zenon_X48 != zenon_X74) % 3.62/3.86 (-. (k04_buttercup10100 zenon_X27)) % 3.62/3.86 (zenon_X30 != zenon_X68) % 3.62/3.86 (zenon_X32 != zenon_X76) % 3.62/3.86 (-. (b48_buttercup10109 Tau_15)) % 3.62/3.86 (zenon_X91 != zenon_X57) % 3.62/3.86 (zenon_X81 != zenon_X48) % 3.62/3.86 (zenon_X48 != Tau_15) % 3.62/3.86 (zenon_X23 != zenon_X45) % 3.62/3.86 (zenon_X54 != zenon_X89) % 3.62/3.86 (-. (b48_buttercup10108 zenon_X81)) % 3.62/3.86 (zenon_X60 != Tau_1) % 3.62/3.86 (Tau_18 != zenon_X57) % 3.62/3.86 (zenon_X30 != zenon_X91) % 3.62/3.86 (zenon_X23 != zenon_X22) % 3.62/3.86 (zenon_X83 != zenon_X87) % 3.62/3.86 (Tau_8 != zenon_X70) % 3.62/3.86 (zenon_X86 != Tau_20) % 3.62/3.86 (Tau_1 != zenon_X64) % 3.62/3.86 (zenon_X55 != Tau_17) % 3.62/3.86 (Tau_1 != zenon_X70) % 3.62/3.86 (-. (b48_buttercup10111 Tau_1)) % 3.62/3.86 (zenon_X77 != zenon_X51) % 3.62/3.86 (zenon_X35 != zenon_X30) % 3.62/3.86 (zenon_X78 != zenon_X74) % 3.62/3.86 (zenon_X70 != zenon_X21) % 3.62/3.86 (zenon_X68 != Tau_20) % 3.62/3.86 (-. (b48_buttercup10109 zenon_X87)) % 3.62/3.86 (zenon_X65 != zenon_X87) % 3.62/3.86 (zenon_X50 != zenon_X49) % 3.62/3.86 (-. (k04_buttercup10622 Tau_8)) % 3.62/3.86 (-. (k04_buttercup10622 zenon_X45)) % 3.62/3.86 (zenon_X72 != zenon_X47) % 3.62/3.86 (zenon_X21 != zenon_X26) % 3.62/3.86 (-. (b48_buttercup10102 Tau_2)) % 3.62/3.86 (Tau_7 != zenon_X56) % 3.62/3.86 (Tau_13 != zenon_X66) % 3.62/3.86 (-. (b48_buttercup10111 zenon_X48)) % 3.62/3.86 (zenon_X37 != zenon_X68) % 3.62/3.86 (zenon_X81 != Tau_3) % 3.62/3.86 (zenon_X60 != zenon_X57) % 3.62/3.86 (zenon_X64 != zenon_X49) % 3.62/3.86 (zenon_X33 != zenon_X91) % 3.62/3.86 (-. (b48_buttercup10109 zenon_X66)) % 3.62/3.86 (Tau_13 != zenon_X33) % 3.62/3.86 (zenon_X64 != zenon_X67) % 3.62/3.86 (zenon_X63 != zenon_X50) % 3.62/3.86 (zenon_X78 != zenon_X53) % 3.62/3.86 (zenon_X35 != zenon_X22) % 3.62/3.86 (zenon_X81 != zenon_X86) % 3.62/3.86 (b48_buttercup10104 zenon_X88) % 3.62/3.86 (zenon_X65 != zenon_X79) % 3.62/3.86 (zenon_X54 != zenon_X80) % 3.62/3.86 (Tau_17 != Tau_16) % 3.62/3.86 (k04_buttercup10619 zenon_X89) % 3.62/3.86 (Tau_18 != zenon_X21) % 3.62/3.86 (Tau_16 != Tau_20) % 3.62/3.86 (Tau_2 != zenon_X21) % 3.62/3.86 (zenon_X48 != zenon_X57) % 3.62/3.86 (-. (b48_buttercup10107 zenon_X80)) % 3.62/3.86 (k04_buttercup10619 zenon_X61) % 3.62/3.86 (-. (b48_buttercup10110 Tau_8)) % 3.62/3.86 (zenon_X56 != zenon_X86) % 3.62/3.86 (zenon_X52 != zenon_X50) % 3.62/3.86 (-. (b48_buttercup10111 Tau_17)) % 3.62/3.86 (zenon_X72 != Tau_8) % 3.62/3.86 (Tau_9 != zenon_X79) % 3.62/3.86 (-. (b48_buttercup10109 zenon_X56)) % 3.62/3.86 (-. (b48_buttercup10111 zenon_X23)) % 3.62/3.86 (zenon_X47 != zenon_X22) % 3.62/3.86 (-. (b48_buttercup10108 zenon_X47)) % 3.62/3.86 (zenon_X64 != zenon_X79) % 3.62/3.86 (zenon_X66 != zenon_X47) % 3.62/3.86 (zenon_X88 != zenon_X49) % 3.62/3.86 (zenon_X66 != zenon_X46) % 3.62/3.86 (zenon_X46 != Tau_13) % 3.62/3.86 (k04_buttercup10622 zenon_X60) % 3.62/3.86 (k04_buttercup10622 Tau_15) % 3.62/3.86 (Tau_14 != zenon_X73) % 3.62/3.86 (zenon_X65 != zenon_X33) % 3.62/3.86 (zenon_X82 != zenon_X69) % 3.62/3.86 (-. (b48_buttercup10102 zenon_X48)) % 3.62/3.86 (zenon_X77 != zenon_X45) % 3.62/3.86 (zenon_X76 != zenon_X73) % 3.62/3.86 (zenon_X26 != zenon_X46) % 3.62/3.86 (k04_buttercup10619 zenon_X53) % 3.62/3.86 (zenon_X61 != zenon_X47) % 3.62/3.86 (zenon_X52 != Tau_10) % 3.62/3.86 (-. (b48_buttercup10107 zenon_X77)) % 3.62/3.86 (k04_buttercup10622 zenon_X53) % 3.62/3.86 (Tau_5 != zenon_X76) % 3.62/3.86 (zenon_X23 != Tau_16) % 3.62/3.86 (Tau_5 != zenon_X46) % 3.62/3.86 (Tau_14 != zenon_X65) % 3.62/3.86 (zenon_X51 != zenon_X49) % 3.62/3.86 (zenon_X37 != zenon_X89) % 3.62/3.86 (Tau_9 != zenon_X67) % 3.62/3.86 (b48_buttercup10110 zenon_X37) % 3.62/3.86 (zenon_X37 != zenon_X82) % 3.62/3.86 (zenon_X83 != zenon_X68) % 3.62/3.86 (zenon_X48 != zenon_X91) % 3.62/3.86 (zenon_X90 != zenon_X22) % 3.62/3.86 (zenon_X84 != zenon_X82) % 3.62/3.86 (zenon_X59 != zenon_X61) % 3.62/3.86 (zenon_X35 != zenon_X25) % 3.62/3.86 (zenon_X63 != Tau_1) % 3.62/3.86 (-. (b48_buttercup10102 zenon_X32)) % 3.62/3.86 (k04_buttercup10622 zenon_X64) % 3.62/3.86 (-. (b48_buttercup10108 zenon_X48)) % 3.62/3.86 (Tau_15 != zenon_X73) % 3.62/3.86 (b48_buttercup10098 Tau_12) % 3.62/3.86 (Tau_11 != zenon_X62) % 3.62/3.86 (Tau_3 != zenon_X58) % 3.62/3.86 (zenon_X64 != zenon_X47) % 3.62/3.86 (-. (b48_buttercup10107 Tau_4)) % 3.62/3.86 (zenon_X92 != zenon_X53) % 3.62/3.86 (zenon_X87 != zenon_X62) % 3.62/3.86 (zenon_X74 != zenon_X61) % 3.62/3.86 (-. (k04_buttercup10619 zenon_X92)) % 3.62/3.86 (-. (b48_buttercup10107 zenon_X91)) % 3.62/3.86 (-. (b48_buttercup10108 zenon_X61)) % 3.62/3.86 (-. (b48_buttercup10102 Tau_4)) % 3.62/3.86 (b48_buttercup10108 zenon_X58) % 3.62/3.86 (zenon_X92 != zenon_X77) % 3.62/3.86 (zenon_X59 != Tau_10) % 3.62/3.86 (zenon_X78 != zenon_X47) % 3.62/3.86 (-. (b48_buttercup10110 zenon_X57)) % 3.62/3.86 (zenon_X32 != zenon_X62) % 3.62/3.86 (-. (b48_buttercup10104 Tau_18)) % 3.62/3.86 (zenon_X84 != zenon_X58) % 3.62/3.86 (zenon_X28 != zenon_X46) % 3.62/3.86 (zenon_X31 != zenon_X89) % 3.62/3.86 (zenon_X84 != zenon_X57) % 3.62/3.86 (zenon_X36 != Tau_13) % 3.62/3.86 (zenon_X66 != Tau_4) % 3.62/3.86 (zenon_X54 != zenon_X57) % 3.62/3.86 (zenon_X64 != zenon_X80) % 3.62/3.86 (zenon_X71 != zenon_X32) % 3.62/3.86 (zenon_X65 != zenon_X55) % 3.62/3.86 (Tau_2 != zenon_X70) % 3.62/3.86 (zenon_X88 != Tau_1) % 3.62/3.86 (-. (b48_buttercup10107 zenon_X81)) % 3.62/3.86 (zenon_X60 != zenon_X36) % 3.62/3.86 (zenon_X72 != Tau_18) % 3.62/3.86 (-. (b48_buttercup10102 zenon_X66)) % 3.62/3.86 (Tau_5 != zenon_X47) % 3.62/3.86 (zenon_X89 != zenon_X67) % 3.62/3.86 (Tau_13 != zenon_X23) % 3.62/3.86 (-. (b48_buttercup10104 zenon_X37)) % 3.62/3.86 (zenon_X30 != zenon_X86) % 3.62/3.86 (zenon_X54 != zenon_X23) % 3.62/3.86 (zenon_X83 != zenon_X82) % 3.62/3.86 (-. (b48_buttercup10102 Tau_0)) % 3.62/3.86 (zenon_X89 != zenon_X24) % 3.62/3.86 (zenon_X28 != zenon_X56) % 3.62/3.86 (zenon_X85 != zenon_X45) % 3.62/3.86 (Tau_0 != zenon_X80) % 3.62/3.86 (k04_buttercup10619 zenon_X70) % 3.62/3.86 (-. (k04_buttercup10622 zenon_X56)) % 3.62/3.86 (-. (b48_buttercup10102 zenon_X75)) % 3.62/3.86 (zenon_X64 != zenon_X56) % 3.62/3.86 (Tau_17 != Tau_14) % 3.62/3.86 (-. (b48_buttercup10102 zenon_X54)) % 3.62/3.86 (k04_buttercup10100 zenon_X81) % 3.62/3.86 (zenon_X28 != zenon_X57) % 3.62/3.86 (zenon_X26 != Tau_1) % 3.62/3.86 (zenon_X70 != zenon_X87) % 3.62/3.86 (zenon_X50 != zenon_X27) % 3.62/3.86 (zenon_X78 != zenon_X46) % 3.62/3.86 (Tau_8 != zenon_X52) % 3.62/3.86 (Tau_8 != zenon_X89) % 3.62/3.86 (-. (b48_buttercup10109 zenon_X65)) % 3.62/3.86 (Tau_4 != Tau_5) % 3.62/3.86 (-. (b48_buttercup10109 zenon_X78)) % 3.62/3.86 (zenon_X72 != zenon_X87) % 3.62/3.86 (Tau_3 != zenon_X90) % 3.62/3.86 (Tau_4 != zenon_X86) % 3.62/3.86 (Tau_2 != zenon_X87) % 3.62/3.86 (zenon_X45 != zenon_X21) % 3.62/3.86 (zenon_X28 != Tau_15) % 3.62/3.86 (-. (b48_buttercup10111 Tau_19)) % 3.62/3.86 (k04_buttercup10619 zenon_X47) % 3.62/3.86 (Tau_11 != zenon_X56) % 3.62/3.86 (Tau_13 != zenon_X57) % 3.62/3.86 (Tau_7 != zenon_X22) % 3.62/3.86 (Tau_13 != zenon_X72) % 3.62/3.86 (zenon_X26 != Tau_4) % 3.62/3.86 (-. (b48_buttercup10108 Tau_5)) % 3.62/3.86 (-. (b48_buttercup10107 zenon_X31)) % 3.62/3.86 (zenon_X55 != Tau_10) % 3.62/3.86 (b48_buttercup10110 Tau_7) % 3.62/3.86 (zenon_X27 != zenon_X61) % 3.62/3.86 (-. (b48_buttercup10102 zenon_X37)) % 3.62/3.86 (Tau_3 != zenon_X25) % 3.62/3.86 (-. (b48_buttercup10104 zenon_X62)) % 3.62/3.86 (zenon_X23 != Tau_1) % 3.62/3.86 (zenon_X84 != zenon_X24) % 3.62/3.86 (zenon_X37 != zenon_X24) % 3.62/3.86 (zenon_X53 != zenon_X49) % 3.62/3.86 (zenon_X30 != zenon_X24) % 3.62/3.86 (Tau_4 != zenon_X50) % 3.62/3.86 (Tau_16 != zenon_X68) % 3.62/3.86 (zenon_X65 != zenon_X67) % 3.62/3.86 (zenon_X26 != zenon_X57) % 3.62/3.86 (k04_buttercup10622 Tau_7) % 3.62/3.86 (zenon_X70 != zenon_X56) % 3.62/3.86 (Tau_8 != zenon_X25) % 3.62/3.86 (zenon_X54 != zenon_X83) % 3.62/3.86 (zenon_X24 != Tau_19) % 3.62/3.86 (-. (b48_buttercup10104 Tau_0)) % 3.62/3.86 (-. (b48_buttercup10109 zenon_X30)) % 3.62/3.86 (zenon_X26 != Tau_20) % 3.62/3.86 (zenon_X26 != zenon_X49) % 3.62/3.86 (zenon_X71 != zenon_X57) % 3.62/3.86 (zenon_X24 != zenon_X55) % 3.62/3.86 (zenon_X92 != zenon_X45) % 3.62/3.86 (zenon_X48 != zenon_X73) % 3.62/3.86 (Tau_18 != zenon_X68) % 3.62/3.86 (zenon_X84 != Tau_10) % 3.62/3.86 (Tau_9 != zenon_X86) % 3.62/3.86 (zenon_X37 != zenon_X23) % 3.62/3.86 (zenon_X35 != zenon_X89) % 3.62/3.86 (b48_buttercup10107 Tau_10) % 3.62/3.86 (zenon_X91 != Tau_17) % 3.62/3.86 (zenon_X73 != zenon_X75) % 3.62/3.86 (zenon_X21 != Tau_15) % 3.62/3.86 (zenon_X63 != zenon_X45) % 3.62/3.86 (zenon_X26 != zenon_X90) % 3.62/3.86 (zenon_X24 != zenon_X85) % 3.62/3.86 (zenon_X37 != zenon_X85) % 3.62/3.86 (zenon_X85 != zenon_X75) % 3.62/3.86 (zenon_X24 != Tau_1) % 3.62/3.86 (Tau_17 != Tau_1) % 3.62/3.86 (zenon_X80 != zenon_X67) % 3.62/3.86 (zenon_X54 != Tau_17) % 3.62/3.86 (-. (b48_buttercup10104 zenon_X23)) % 3.62/3.86 (zenon_X80 != zenon_X55) % 3.62/3.86 (zenon_X31 != zenon_X49) % 3.62/3.87 (k04_buttercup10619 Tau_17) % 3.62/3.87 (zenon_X55 != zenon_X56) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X74)) % 3.62/3.87 (k04_buttercup10622 zenon_X24) % 3.62/3.87 (zenon_X30 != Tau_4) % 3.62/3.87 (Tau_18 != Tau_19) % 3.62/3.87 (zenon_X36 != zenon_X51) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X49)) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X79)) % 3.62/3.87 (zenon_X35 != zenon_X53) % 3.62/3.87 (zenon_X72 != zenon_X22) % 3.62/3.87 (zenon_X82 != zenon_X79) % 3.62/3.87 (zenon_X68 != zenon_X71) % 3.62/3.87 (zenon_X92 != zenon_X89) % 3.62/3.87 (zenon_X56 != zenon_X62) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X65)) % 3.62/3.87 (-. (k04_buttercup10622 zenon_X92)) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X30)) % 3.62/3.87 (zenon_X36 != Tau_8) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X35)) % 3.62/3.87 (zenon_X55 != zenon_X79) % 3.62/3.87 (Tau_18 != zenon_X76) % 3.62/3.87 (zenon_X51 != zenon_X88) % 3.62/3.87 (zenon_X88 != zenon_X85) % 3.62/3.87 (zenon_X33 != Tau_7) % 3.62/3.87 (zenon_X78 != zenon_X89) % 3.62/3.87 (zenon_X52 != Tau_0) % 3.62/3.87 (Tau_13 != zenon_X77) % 3.62/3.87 (zenon_X26 != zenon_X53) % 3.62/3.87 (Tau_3 != zenon_X63) % 3.62/3.87 (Tau_5 != zenon_X62) % 3.62/3.87 (zenon_X92 != zenon_X83) % 3.62/3.87 (zenon_X24 != Tau_8) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X65)) % 3.62/3.87 (k04_buttercup10622 zenon_X49) % 3.62/3.87 (zenon_X28 != Tau_17) % 3.62/3.87 (Tau_14 != zenon_X89) % 3.62/3.87 (zenon_X24 != zenon_X79) % 3.62/3.87 (Tau_14 != zenon_X83) % 3.62/3.87 (zenon_X37 != zenon_X49) % 3.62/3.87 (zenon_X85 != zenon_X87) % 3.62/3.87 (b48_buttercup10098 Tau_6) % 3.62/3.87 (b48_buttercup10107 zenon_X61) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X70)) % 3.62/3.87 (Tau_1 != zenon_X62) % 3.62/3.87 (zenon_X84 != Tau_19) % 3.62/3.87 (zenon_X52 != zenon_X87) % 3.62/3.87 (zenon_X74 != zenon_X79) % 3.62/3.87 (Tau_6 != Tau_15) % 3.62/3.87 (zenon_X57 != Tau_10) % 3.62/3.87 (zenon_X78 != Tau_2) % 3.62/3.87 (zenon_X59 != zenon_X46) % 3.62/3.87 (Tau_9 != Tau_15) % 3.62/3.87 (zenon_X23 != zenon_X27) % 3.62/3.87 (zenon_X82 != zenon_X81) % 3.62/3.87 (zenon_X26 != zenon_X62) % 3.62/3.87 (Tau_7 != zenon_X64) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X70)) % 3.62/3.87 (zenon_X79 != zenon_X87) % 3.62/3.87 (zenon_X58 != Tau_0) % 3.62/3.87 (Tau_14 != zenon_X63) % 3.62/3.87 (zenon_X66 != zenon_X52) % 3.62/3.87 (zenon_X27 != zenon_X79) % 3.62/3.87 (zenon_X72 != Tau_16) % 3.62/3.87 (zenon_X37 != zenon_X25) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X90)) % 3.62/3.87 (zenon_X36 != zenon_X80) % 3.62/3.87 (zenon_X82 != zenon_X50) % 3.62/3.87 (zenon_X52 != Tau_17) % 3.62/3.87 (zenon_X30 != Tau_19) % 3.62/3.87 (zenon_X64 != zenon_X62) % 3.62/3.87 (zenon_X35 != zenon_X81) % 3.62/3.87 (zenon_X92 != zenon_X48) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X33)) % 3.62/3.87 (Tau_11 != zenon_X77) % 3.62/3.87 (-. (b48_buttercup10104 Tau_8)) % 3.62/3.87 (Tau_14 != zenon_X76) % 3.62/3.87 (zenon_X54 != zenon_X52) % 3.62/3.87 (zenon_X52 != zenon_X61) % 3.62/3.87 (zenon_X57 != zenon_X22) % 3.62/3.87 (Tau_9 != zenon_X89) % 3.62/3.87 (zenon_X90 != zenon_X30) % 3.62/3.87 (Tau_7 != zenon_X73) % 3.62/3.87 (zenon_X72 != zenon_X56) % 3.62/3.87 (Tau_14 != zenon_X70) % 3.62/3.87 (zenon_X83 != zenon_X52) % 3.62/3.87 (zenon_X88 != zenon_X21) % 3.62/3.87 (Tau_11 != zenon_X71) % 3.62/3.87 (zenon_X30 != Tau_8) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X59)) % 3.62/3.87 (zenon_X31 != zenon_X83) % 3.62/3.87 (zenon_X66 != zenon_X49) % 3.62/3.87 (zenon_X68 != zenon_X64) % 3.62/3.87 (zenon_X78 != zenon_X91) % 3.62/3.87 (zenon_X58 != zenon_X87) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X77)) % 3.62/3.87 (zenon_X33 != zenon_X26) % 3.62/3.87 (zenon_X89 != zenon_X82) % 3.62/3.87 (zenon_X70 != zenon_X51) % 3.62/3.87 (zenon_X31 != zenon_X75) % 3.62/3.87 (Tau_7 != zenon_X76) % 3.62/3.87 (Tau_5 != zenon_X73) % 3.62/3.87 (zenon_X89 != zenon_X33) % 3.62/3.87 (Tau_6 != zenon_X76) % 3.62/3.87 (zenon_X78 != zenon_X80) % 3.62/3.87 (Tau_7 != zenon_X74) % 3.62/3.87 (Tau_3 != zenon_X73) % 3.62/3.87 (b48_buttercup10104 zenon_X24) % 3.62/3.87 (zenon_X88 != zenon_X69) % 3.62/3.87 (zenon_X88 != Tau_20) % 3.62/3.87 (Tau_9 != zenon_X47) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X84)) % 3.62/3.87 (zenon_X71 != zenon_X89) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X85)) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X63)) % 3.62/3.87 (Tau_19 != zenon_X80) % 3.62/3.87 (zenon_X90 != zenon_X57) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X63)) % 3.62/3.87 (-. (k04_buttercup10619 zenon_X75)) % 3.62/3.87 (Tau_16 != zenon_X87) % 3.62/3.87 (Tau_18 != zenon_X82) % 3.62/3.87 (-. (b48_buttercup10108 Tau_11)) % 3.62/3.87 (zenon_X78 != zenon_X75) % 3.62/3.87 (zenon_X51 != zenon_X73) % 3.62/3.87 (zenon_X70 != zenon_X27) % 3.62/3.87 (zenon_X92 != Tau_4) % 3.62/3.87 (zenon_X51 != zenon_X75) % 3.62/3.87 (Tau_17 != zenon_X47) % 3.62/3.87 (zenon_X85 != zenon_X56) % 3.62/3.87 (b48_buttercup10098 Tau_1) % 3.62/3.87 (zenon_X53 != Tau_19) % 3.62/3.87 (zenon_X76 != zenon_X45) % 3.62/3.87 (zenon_X91 != zenon_X47) % 3.62/3.87 (-. (b48_buttercup10111 Tau_18)) % 3.62/3.87 (zenon_X23 != zenon_X69) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X90)) % 3.62/3.87 (zenon_X32 != zenon_X58) % 3.62/3.87 (Tau_6 != zenon_X52) % 3.62/3.87 (Tau_9 != zenon_X59) % 3.62/3.87 (zenon_X28 != zenon_X70) % 3.62/3.87 (zenon_X59 != zenon_X52) % 3.62/3.87 (Tau_4 != zenon_X82) % 3.62/3.87 (Tau_8 != Tau_18) % 3.62/3.87 (zenon_X30 != Tau_20) % 3.62/3.87 (zenon_X64 != Tau_0) % 3.62/3.87 (k04_buttercup10100 zenon_X67) % 3.62/3.87 (zenon_X66 != zenon_X71) % 3.62/3.87 (zenon_X91 != zenon_X64) % 3.62/3.87 (zenon_X48 != zenon_X76) % 3.62/3.87 (Tau_10 != zenon_X87) % 3.62/3.87 (Tau_5 != Tau_1) % 3.62/3.87 (zenon_X91 != Tau_13) % 3.62/3.87 (Tau_19 != zenon_X27) % 3.62/3.87 (zenon_X76 != zenon_X47) % 3.62/3.87 (Tau_13 != zenon_X80) % 3.62/3.87 (zenon_X70 != zenon_X22) % 3.62/3.87 (zenon_X58 != zenon_X52) % 3.62/3.87 (Tau_7 != Tau_18) % 3.62/3.87 (zenon_X63 != zenon_X81) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X37)) % 3.62/3.87 (zenon_X72 != zenon_X69) % 3.62/3.87 (zenon_X49 != zenon_X55) % 3.62/3.87 (zenon_X65 != zenon_X47) % 3.62/3.87 (zenon_X59 != zenon_X86) % 3.62/3.87 (zenon_X31 != zenon_X65) % 3.62/3.87 (Tau_9 != zenon_X80) % 3.62/3.87 (zenon_X84 != zenon_X64) % 3.62/3.87 (Tau_11 != zenon_X86) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X71)) % 3.62/3.87 (zenon_X54 != zenon_X67) % 3.62/3.87 (zenon_X25 != zenon_X76) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X74)) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X24)) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X31)) % 3.62/3.87 (zenon_X84 != zenon_X91) % 3.62/3.87 (zenon_X75 != zenon_X55) % 3.62/3.87 (zenon_X66 != Tau_8) % 3.62/3.87 (zenon_X48 != zenon_X69) % 3.62/3.87 (zenon_X32 != zenon_X88) % 3.62/3.87 (zenon_X63 != zenon_X79) % 3.62/3.87 (zenon_X31 != zenon_X79) % 3.62/3.87 (zenon_X49 != zenon_X75) % 3.62/3.87 (-. (b48_buttercup10110 Tau_20)) % 3.62/3.87 (zenon_X77 != zenon_X80) % 3.62/3.87 (Tau_11 != Tau_19) % 3.62/3.87 (zenon_X87 != zenon_X74) % 3.62/3.87 (zenon_X54 != zenon_X69) % 3.62/3.87 (zenon_X48 != zenon_X63) % 3.62/3.87 (zenon_X70 != zenon_X68) % 3.62/3.87 (zenon_X89 != zenon_X69) % 3.62/3.87 (zenon_X33 != zenon_X47) % 3.62/3.87 (zenon_X60 != zenon_X22) % 3.62/3.87 (zenon_X72 != Tau_2) % 3.62/3.87 (zenon_X30 != Tau_2) % 3.62/3.87 (zenon_X54 != zenon_X53) % 3.62/3.87 (zenon_X83 != zenon_X75) % 3.62/3.87 (zenon_X71 != zenon_X36) % 3.62/3.87 (zenon_X23 != zenon_X49) % 3.62/3.87 (k04_buttercup10100 zenon_X33) % 3.62/3.87 (-. (b48_buttercup10104 Tau_10)) % 3.62/3.87 (b48_buttercup10104 zenon_X52) % 3.62/3.87 (-. (b48_buttercup10109 Tau_16)) % 3.62/3.87 (b48_buttercup10102 Tau_15) % 3.62/3.87 (zenon_X63 != zenon_X71) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X59)) % 3.62/3.87 (zenon_X56 != zenon_X69) % 3.62/3.87 (zenon_X72 != zenon_X62) % 3.62/3.87 (zenon_X79 != Tau_13) % 3.62/3.87 (Tau_18 != zenon_X55) % 3.62/3.87 (zenon_X28 != zenon_X91) % 3.62/3.87 (Tau_3 != zenon_X23) % 3.62/3.87 (Tau_4 != zenon_X27) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X89)) % 3.62/3.87 (zenon_X48 != zenon_X68) % 3.62/3.87 (Tau_7 != zenon_X86) % 3.62/3.87 (Tau_3 != zenon_X85) % 3.62/3.87 (zenon_X48 != zenon_X36) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X26)) % 3.62/3.87 (zenon_X21 != zenon_X80) % 3.62/3.87 (zenon_X60 != Tau_10) % 3.62/3.87 (zenon_X81 != Tau_5) % 3.62/3.87 (zenon_X72 != zenon_X73) % 3.62/3.87 (k04_buttercup10622 zenon_X88) % 3.62/3.87 (Tau_19 != zenon_X21) % 3.62/3.87 (Tau_8 != Tau_9) % 3.62/3.87 (zenon_X46 != Tau_16) % 3.62/3.87 (zenon_X91 != zenon_X76) % 3.62/3.87 (Tau_1 != zenon_X47) % 3.62/3.87 (zenon_X88 != zenon_X45) % 3.62/3.87 (zenon_X51 != zenon_X27) % 3.62/3.87 (zenon_X33 != zenon_X74) % 3.62/3.87 (zenon_X59 != zenon_X47) % 3.62/3.87 (zenon_X33 != Tau_14) % 3.62/3.87 (-. (b48_buttercup10108 Tau_17)) % 3.62/3.87 (zenon_X23 != Tau_15) % 3.62/3.87 (zenon_X32 != zenon_X75) % 3.62/3.87 (zenon_X46 != zenon_X84) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X50)) % 3.62/3.87 (zenon_X85 != Tau_1) % 3.62/3.87 (zenon_X85 != Tau_13) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X46)) % 3.62/3.87 (zenon_X35 != zenon_X84) % 3.62/3.87 (-. (b48_buttercup10108 Tau_16)) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X92)) % 3.62/3.87 (zenon_X56 != zenon_X47) % 3.62/3.87 (zenon_X37 != zenon_X56) % 3.62/3.87 (Tau_11 != zenon_X79) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X58)) % 3.62/3.87 (zenon_X33 != zenon_X80) % 3.62/3.87 (zenon_X48 != zenon_X70) % 3.62/3.87 (zenon_X36 != zenon_X63) % 3.62/3.87 (zenon_X48 != zenon_X27) % 3.62/3.87 (Tau_14 != zenon_X58) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X80)) % 3.62/3.87 (zenon_X78 != Tau_10) % 3.62/3.87 (Tau_20 != zenon_X25) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X36)) % 3.62/3.87 (Tau_6 != zenon_X89) % 3.62/3.87 (zenon_X37 != zenon_X91) % 3.62/3.87 (Tau_5 != Tau_19) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X80)) % 3.62/3.87 (Tau_9 != zenon_X82) % 3.62/3.87 (zenon_X83 != zenon_X50) % 3.62/3.87 (b48_buttercup10108 zenon_X89) % 3.62/3.87 (k04_buttercup10619 zenon_X36) % 3.62/3.87 (zenon_X57 != zenon_X80) % 3.62/3.87 (Tau_19 != zenon_X25) % 3.62/3.87 (zenon_X48 != zenon_X50) % 3.62/3.87 (Tau_9 != zenon_X68) % 3.62/3.87 (zenon_X37 != Tau_15) % 3.62/3.87 (Tau_11 != zenon_X74) % 3.62/3.87 (-. (b48_buttercup10111 Tau_10)) % 3.62/3.87 (Tau_16 != zenon_X27) % 3.62/3.87 (Tau_11 != Tau_15) % 3.62/3.87 (zenon_X63 != zenon_X87) % 3.62/3.87 (zenon_X37 != zenon_X52) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X79)) % 3.62/3.87 (zenon_X71 != zenon_X62) % 3.62/3.87 (zenon_X69 != zenon_X92) % 3.62/3.87 (-. (b48_buttercup10108 Tau_14)) % 3.62/3.87 (zenon_X79 != zenon_X50) % 3.62/3.87 (zenon_X84 != Tau_2) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X36)) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X55)) % 3.62/3.87 (zenon_X91 != zenon_X69) % 3.62/3.87 (zenon_X54 != zenon_X73) % 3.62/3.87 (zenon_X82 != Tau_10) % 3.62/3.87 (Tau_1 != zenon_X69) % 3.62/3.87 (zenon_X21 != zenon_X54) % 3.62/3.87 (-. (k04_buttercup10622 zenon_X85)) % 3.62/3.87 (zenon_X82 != zenon_X45) % 3.62/3.87 (zenon_X58 != zenon_X27) % 3.62/3.87 (zenon_X28 != Tau_16) % 3.62/3.87 (Tau_20 != zenon_X58) % 3.62/3.87 (zenon_X77 != zenon_X82) % 3.62/3.87 (zenon_X31 != zenon_X90) % 3.62/3.87 (Tau_9 != Tau_10) % 3.62/3.87 (zenon_X85 != zenon_X71) % 3.62/3.87 (zenon_X61 != zenon_X75) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X53)) % 3.62/3.87 (-. (b48_buttercup10109 Tau_3)) % 3.62/3.87 (zenon_X24 != zenon_X81) % 3.62/3.87 (Tau_20 != zenon_X73) % 3.62/3.87 (zenon_X89 != zenon_X64) % 3.62/3.87 (zenon_X91 != zenon_X62) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X60)) % 3.62/3.87 (zenon_X83 != zenon_X79) % 3.62/3.87 (-. (b48_buttercup10104 Tau_11)) % 3.62/3.87 (zenon_X22 != zenon_X55) % 3.62/3.87 (Tau_10 != zenon_X75) % 3.62/3.87 (zenon_X48 != zenon_X52) % 3.62/3.87 (zenon_X87 != zenon_X64) % 3.62/3.87 (zenon_X46 != Tau_14) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X91)) % 3.62/3.87 (zenon_X32 != zenon_X59) % 3.62/3.87 (zenon_X77 != Tau_17) % 3.62/3.87 (zenon_X82 != zenon_X80) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X32)) % 3.62/3.87 (k04_buttercup10622 zenon_X47) % 3.62/3.87 (zenon_X37 != zenon_X62) % 3.62/3.87 (Tau_15 != Tau_1) % 3.62/3.87 (zenon_X33 != zenon_X48) % 3.62/3.87 (-. (k04_buttercup10100 Tau_5)) % 3.62/3.87 (Tau_9 != zenon_X50) % 3.62/3.87 (zenon_X68 != Tau_15) % 3.62/3.87 (zenon_X66 != zenon_X65) % 3.62/3.87 (zenon_X46 != zenon_X21) % 3.62/3.87 (zenon_X86 != Tau_2) % 3.62/3.87 (zenon_X91 != zenon_X27) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X57)) % 3.62/3.87 (zenon_X84 != zenon_X47) % 3.62/3.87 (zenon_X66 != zenon_X25) % 3.62/3.87 (zenon_X46 != zenon_X69) % 3.62/3.87 (zenon_X70 != zenon_X80) % 3.62/3.87 (-. (k04_buttercup10622 Tau_19)) % 3.62/3.87 (-. (k04_buttercup10619 zenon_X67)) % 3.62/3.87 (zenon_X61 != Tau_0) % 3.62/3.87 (zenon_X51 != zenon_X79) % 3.62/3.87 (zenon_X31 != zenon_X74) % 3.62/3.87 (zenon_X25 != zenon_X75) % 3.62/3.87 (zenon_X76 != zenon_X79) % 3.62/3.87 (zenon_X76 != zenon_X55) % 3.62/3.87 (Tau_18 != zenon_X27) % 3.62/3.87 (zenon_X30 != Tau_18) % 3.62/3.87 (zenon_X24 != Tau_10) % 3.62/3.87 (zenon_X25 != zenon_X62) % 3.62/3.87 (Tau_0 != Tau_14) % 3.62/3.87 (k04_buttercup10622 Tau_9) % 3.62/3.87 (zenon_X80 != zenon_X61) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X90)) % 3.62/3.87 (zenon_X80 != zenon_X68) % 3.62/3.87 (b48_buttercup10109 Tau_20) % 3.62/3.87 (zenon_X78 != zenon_X25) % 3.62/3.87 (zenon_X83 != zenon_X88) % 3.62/3.87 (zenon_X32 != zenon_X50) % 3.62/3.87 (zenon_X28 != zenon_X88) % 3.62/3.87 (b48_buttercup10098 zenon_X42) % 3.62/3.87 (zenon_X31 != zenon_X57) % 3.62/3.87 (Tau_10 != Tau_19) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X22)) % 3.62/3.87 (zenon_X82 != Tau_20) % 3.62/3.87 (Tau_8 != zenon_X69) % 3.62/3.87 (zenon_X48 != zenon_X77) % 3.62/3.87 (b48_buttercup10107 zenon_X68) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X80)) % 3.62/3.87 (zenon_X76 != Tau_1) % 3.62/3.87 (zenon_X65 != zenon_X57) % 3.62/3.87 (-. (b48_buttercup10108 Tau_13)) % 3.62/3.87 (b48_buttercup10107 zenon_X46) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X77)) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X77)) % 3.62/3.87 (zenon_X59 != Tau_17) % 3.62/3.87 (zenon_X26 != zenon_X87) % 3.62/3.87 (zenon_X80 != Tau_10) % 3.62/3.87 (zenon_X76 != zenon_X75) % 3.62/3.87 (Tau_4 != zenon_X46) % 3.62/3.87 (zenon_X51 != zenon_X61) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X50)) % 3.62/3.87 (zenon_X71 != Tau_15) % 3.62/3.87 (zenon_X60 != Tau_15) % 3.62/3.87 (zenon_X70 != zenon_X45) % 3.62/3.87 (-. (k04_buttercup10619 zenon_X71)) % 3.62/3.87 (zenon_X78 != zenon_X65) % 3.62/3.87 (zenon_X88 != zenon_X87) % 3.62/3.87 (zenon_X57 != zenon_X74) % 3.62/3.87 (Tau_3 != zenon_X87) % 3.62/3.87 (zenon_X46 != Tau_9) % 3.62/3.87 (zenon_X92 != Tau_9) % 3.62/3.87 (Tau_6 != zenon_X25) % 3.62/3.87 (zenon_X76 != zenon_X71) % 3.62/3.87 (Tau_3 != zenon_X91) % 3.62/3.87 (zenon_X78 != zenon_X24) % 3.62/3.87 (zenon_X25 != zenon_X56) % 3.62/3.87 (Tau_5 != zenon_X64) % 3.62/3.87 (zenon_X61 != zenon_X90) % 3.62/3.87 (Tau_15 != zenon_X45) % 3.62/3.87 (zenon_X82 != zenon_X33) % 3.62/3.87 (zenon_X54 != zenon_X77) % 3.62/3.87 (Tau_11 != zenon_X36) % 3.62/3.87 (zenon_X70 != zenon_X82) % 3.62/3.87 (Tau_11 != zenon_X91) % 3.62/3.87 (zenon_X25 != zenon_X61) % 3.62/3.87 (Tau_5 != zenon_X68) % 3.62/3.87 (Tau_8 != Tau_15) % 3.62/3.87 (zenon_X35 != zenon_X47) % 3.62/3.87 (zenon_X85 != zenon_X67) % 3.62/3.87 (zenon_X76 != zenon_X27) % 3.62/3.87 (Tau_6 != zenon_X86) % 3.62/3.87 (zenon_X26 != zenon_X88) % 3.62/3.87 (zenon_X79 != zenon_X21) % 3.62/3.87 (Tau_8 != zenon_X22) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X58)) % 3.62/3.87 (zenon_X90 != zenon_X49) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X88)) % 3.62/3.87 (zenon_X89 != zenon_X56) % 3.62/3.87 (Tau_14 != zenon_X59) % 3.62/3.87 (zenon_X51 != zenon_X24) % 3.62/3.87 (zenon_X83 != zenon_X57) % 3.62/3.87 (zenon_X57 != zenon_X87) % 3.62/3.87 (zenon_X36 != zenon_X56) % 3.62/3.87 (zenon_X89 != Tau_15) % 3.62/3.87 (zenon_X36 != zenon_X62) % 3.62/3.87 (zenon_X35 != zenon_X46) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X84)) % 3.62/3.87 (zenon_X72 != zenon_X24) % 3.62/3.87 (Tau_16 != zenon_X50) % 3.62/3.87 (zenon_X70 != zenon_X24) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X70)) % 3.62/3.87 (zenon_X54 != zenon_X46) % 3.62/3.87 (zenon_X35 != Tau_16) % 3.62/3.87 (Tau_15 != Tau_20) % 3.62/3.87 (Tau_9 != zenon_X63) % 3.62/3.87 (zenon_X55 != zenon_X46) % 3.62/3.87 (zenon_X89 != zenon_X68) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X86)) % 3.62/3.87 (zenon_X77 != zenon_X57) % 3.62/3.87 (-. (b48_buttercup10102 Tau_8)) % 3.62/3.87 (Tau_7 != zenon_X61) % 3.62/3.87 (Tau_5 != Tau_2) % 3.62/3.87 (Tau_16 != zenon_X22) % 3.62/3.87 (zenon_X35 != zenon_X60) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X49)) % 3.62/3.87 (Tau_3 != zenon_X69) % 3.62/3.87 (zenon_X63 != zenon_X80) % 3.62/3.87 (zenon_X53 != zenon_X46) % 3.62/3.87 (zenon_X54 != zenon_X85) % 3.62/3.87 (zenon_X90 != zenon_X28) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X37)) % 3.62/3.87 (k04_buttercup10622 Tau_4) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X25)) % 3.62/3.87 (zenon_X58 != Tau_16) % 3.62/3.87 (Tau_1 != zenon_X50) % 3.62/3.87 (zenon_X68 != zenon_X75) % 3.62/3.87 (zenon_X57 != zenon_X67) % 3.62/3.87 (zenon_X69 != zenon_X67) % 3.62/3.87 (zenon_X51 != zenon_X85) % 3.62/3.87 (zenon_X63 != zenon_X62) % 3.62/3.87 (zenon_X24 != zenon_X35) % 3.62/3.87 (Tau_13 != zenon_X78) % 3.62/3.87 (zenon_X24 != zenon_X87) % 3.62/3.87 (zenon_X35 != Tau_9) % 3.62/3.87 (Tau_5 != zenon_X89) % 3.62/3.87 (b48_buttercup10104 zenon_X64) % 3.62/3.87 (zenon_X37 != zenon_X67) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X68)) % 3.62/3.87 (zenon_X78 != zenon_X64) % 3.62/3.87 (zenon_X83 != Tau_0) % 3.62/3.87 (zenon_X57 != Tau_17) % 3.62/3.87 (zenon_X81 != Tau_9) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X26)) % 3.62/3.87 (zenon_X37 != zenon_X65) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X87)) % 3.62/3.87 (-. (k04_buttercup10622 zenon_X67)) % 3.62/3.87 (zenon_X49 != zenon_X67) % 3.62/3.87 (Tau_11 != Tau_1) % 3.62/3.87 (b48_buttercup10098 zenon_X38) % 3.62/3.87 (Tau_11 != zenon_X89) % 3.62/3.87 (zenon_X25 != Tau_0) % 3.62/3.87 (zenon_X82 != zenon_X71) % 3.62/3.87 (-. (b48_buttercup10104 Tau_2)) % 3.62/3.87 (zenon_X92 != zenon_X71) % 3.62/3.87 (-. (b48_buttercup10109 Tau_14)) % 3.62/3.87 (Tau_14 != zenon_X82) % 3.62/3.87 (zenon_X78 != zenon_X50) % 3.62/3.87 (zenon_X90 != zenon_X27) % 3.62/3.87 (Tau_20 != Tau_6) % 3.62/3.87 (Tau_6 != zenon_X82) % 3.62/3.87 (zenon_X50 != zenon_X47) % 3.62/3.87 (-. (k04_buttercup10100 Tau_10)) % 3.62/3.87 (zenon_X70 != zenon_X75) % 3.62/3.87 (zenon_X54 != zenon_X33) % 3.62/3.87 (zenon_X63 != zenon_X69) % 3.62/3.87 (Tau_1 != zenon_X58) % 3.62/3.87 (Tau_11 != zenon_X57) % 3.62/3.87 (zenon_X33 != Tau_4) % 3.62/3.87 (zenon_X49 != Tau_0) % 3.62/3.87 (-. (b48_buttercup10108 Tau_6)) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X72)) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X81)) % 3.62/3.87 (zenon_X66 != zenon_X50) % 3.62/3.87 (zenon_X92 != Tau_16) % 3.62/3.87 (zenon_X60 != zenon_X89) % 3.62/3.87 (b48_buttercup10102 zenon_X27) % 3.62/3.87 (zenon_X56 != Tau_15) % 3.62/3.87 (Tau_1 != zenon_X48) % 3.62/3.87 (zenon_X84 != zenon_X65) % 3.62/3.87 (zenon_X61 != zenon_X45) % 3.62/3.87 (zenon_X25 != zenon_X92) % 3.62/3.87 (zenon_X83 != zenon_X24) % 3.62/3.87 (zenon_X30 != zenon_X83) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X33)) % 3.62/3.87 (b48_buttercup10098 zenon_X29) % 3.62/3.87 (Tau_9 != zenon_X25) % 3.62/3.87 (zenon_X89 != zenon_X22) % 3.62/3.87 (Tau_7 != zenon_X87) % 3.62/3.87 (zenon_X84 != zenon_X61) % 3.62/3.87 (zenon_X60 != Tau_0) % 3.62/3.87 (Tau_13 != zenon_X59) % 3.62/3.87 (Tau_20 != zenon_X87) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X53)) % 3.62/3.87 (zenon_X72 != Tau_1) % 3.62/3.87 (zenon_X33 != Tau_9) % 3.62/3.87 (zenon_X80 != zenon_X22) % 3.62/3.87 (k04_buttercup10619 zenon_X27) % 3.62/3.87 (Tau_7 != zenon_X23) % 3.62/3.87 (zenon_X54 != Tau_15) % 3.62/3.87 (zenon_X68 != Tau_1) % 3.62/3.87 (Tau_4 != zenon_X22) % 3.62/3.87 (zenon_X70 != zenon_X62) % 3.62/3.87 (zenon_X70 != zenon_X74) % 3.62/3.87 (zenon_X59 != zenon_X81) % 3.62/3.87 (zenon_X81 != zenon_X62) % 3.62/3.87 (zenon_X46 != zenon_X45) % 3.62/3.87 (b48_buttercup10110 Tau_5) % 3.62/3.87 (zenon_X45 != zenon_X69) % 3.62/3.87 (zenon_X90 != zenon_X37) % 3.62/3.87 (zenon_X91 != zenon_X51) % 3.62/3.87 (Tau_7 != Tau_17) % 3.62/3.87 (zenon_X37 != zenon_X77) % 3.62/3.87 (zenon_X26 != zenon_X91) % 3.62/3.87 (zenon_X37 != zenon_X22) % 3.62/3.87 (zenon_X92 != Tau_20) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X80)) % 3.62/3.87 (zenon_X28 != zenon_X36) % 3.62/3.87 (zenon_X35 != Tau_4) % 3.62/3.87 (zenon_X58 != zenon_X55) % 3.62/3.87 (-. (b48_buttercup10110 Tau_1)) % 3.62/3.87 (zenon_X76 != zenon_X21) % 3.62/3.87 (Tau_11 != zenon_X75) % 3.62/3.87 (Tau_4 != Tau_15) % 3.62/3.87 (zenon_X33 != Tau_10) % 3.62/3.87 (zenon_X50 != zenon_X80) % 3.62/3.87 (zenon_X79 != zenon_X47) % 3.62/3.87 (zenon_X53 != zenon_X52) % 3.62/3.87 (-. (b48_buttercup10104 Tau_5)) % 3.62/3.87 (zenon_X66 != zenon_X76) % 3.62/3.87 (zenon_X60 != zenon_X56) % 3.62/3.87 (zenon_X53 != zenon_X82) % 3.62/3.87 (zenon_X83 != zenon_X74) % 3.62/3.87 (zenon_X24 != zenon_X47) % 3.62/3.87 (zenon_X54 != Tau_10) % 3.62/3.87 (zenon_X30 != zenon_X70) % 3.62/3.87 (Tau_20 != zenon_X57) % 3.62/3.87 (b48_buttercup10104 zenon_X57) % 3.62/3.87 (Tau_5 != zenon_X88) % 3.62/3.87 (Tau_11 != zenon_X83) % 3.62/3.87 (zenon_X85 != Tau_19) % 3.62/3.87 (zenon_X71 != zenon_X37) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X33)) % 3.62/3.87 (zenon_X91 != Tau_2) % 3.62/3.87 (Tau_7 != zenon_X36) % 3.62/3.87 (zenon_X31 != zenon_X67) % 3.62/3.87 (Tau_19 != zenon_X73) % 3.62/3.87 (Tau_6 != zenon_X65) % 3.62/3.87 (Tau_2 != zenon_X67) % 3.62/3.87 (Tau_16 != zenon_X67) % 3.62/3.87 (zenon_X74 != zenon_X73) % 3.62/3.87 (zenon_X54 != zenon_X27) % 3.62/3.87 (Tau_16 != Tau_19) % 3.62/3.87 (zenon_X86 != zenon_X55) % 3.62/3.87 (Tau_18 != zenon_X88) % 3.62/3.87 (zenon_X77 != zenon_X69) % 3.62/3.87 (zenon_X32 != zenon_X83) % 3.62/3.87 (zenon_X66 != zenon_X90) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X79)) % 3.62/3.87 (zenon_X65 != Tau_19) % 3.62/3.87 (zenon_X72 != zenon_X91) % 3.62/3.87 (Tau_7 != Tau_1) % 3.62/3.87 (zenon_X52 != zenon_X55) % 3.62/3.87 (zenon_X30 != zenon_X77) % 3.62/3.87 (k04_buttercup10100 zenon_X87) % 3.62/3.87 (zenon_X68 != zenon_X81) % 3.62/3.87 (-. (b48_buttercup10107 Tau_5)) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X32)) % 3.62/3.87 (Tau_13 != zenon_X35) % 3.62/3.87 (zenon_X59 != Tau_20) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X60)) % 3.62/3.87 (zenon_X36 != zenon_X47) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X49)) % 3.62/3.87 (zenon_X81 != zenon_X30) % 3.62/3.87 (zenon_X26 != zenon_X70) % 3.62/3.87 (-. (k04_buttercup10619 Tau_1)) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X37)) % 3.62/3.87 (zenon_X24 != Tau_20) % 3.62/3.87 (Tau_7 != Tau_0) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X45)) % 3.62/3.87 (zenon_X84 != zenon_X62) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X62)) % 3.62/3.87 (zenon_X59 != zenon_X90) % 3.62/3.87 (-. (b48_buttercup10104 Tau_9)) % 3.62/3.87 (Tau_14 != zenon_X45) % 3.62/3.87 (Tau_7 != zenon_X85) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X88)) % 3.62/3.87 (zenon_X58 != zenon_X92) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X64)) % 3.62/3.87 (zenon_X27 != zenon_X46) % 3.62/3.87 (-. (b48_buttercup10108 Tau_15)) % 3.62/3.87 (zenon_X86 != zenon_X61) % 3.62/3.87 (Tau_10 != zenon_X47) % 3.62/3.87 (zenon_X72 != zenon_X36) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X79)) % 3.62/3.87 (k04_buttercup10622 zenon_X86) % 3.62/3.87 (zenon_X63 != zenon_X49) % 3.62/3.87 (zenon_X84 != zenon_X45) % 3.62/3.87 (Tau_6 != zenon_X24) % 3.62/3.87 (Tau_3 != zenon_X52) % 3.62/3.87 (zenon_X60 != zenon_X67) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X23)) % 3.62/3.87 (zenon_X72 != zenon_X53) % 3.62/3.87 (zenon_X84 != zenon_X87) % 3.62/3.87 (zenon_X76 != zenon_X80) % 3.62/3.87 (zenon_X71 != zenon_X21) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X87)) % 3.62/3.87 (Tau_7 != zenon_X91) % 3.62/3.87 (zenon_X33 != zenon_X87) % 3.62/3.87 (zenon_X84 != zenon_X36) % 3.62/3.87 (Tau_4 != zenon_X51) % 3.62/3.87 (Tau_5 != zenon_X53) % 3.62/3.87 (zenon_X54 != zenon_X91) % 3.62/3.87 (zenon_X32 != Tau_18) % 3.62/3.87 (Tau_3 != zenon_X71) % 3.62/3.87 (Tau_4 != zenon_X68) % 3.62/3.87 (-. (b48_buttercup10108 Tau_3)) % 3.62/3.87 (zenon_X21 != zenon_X60) % 3.62/3.87 (Tau_6 != zenon_X49) % 3.62/3.87 (zenon_X66 != zenon_X69) % 3.62/3.87 (zenon_X25 != zenon_X68) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X45)) % 3.62/3.87 (zenon_X84 != zenon_X77) % 3.62/3.87 (zenon_X32 != zenon_X36) % 3.62/3.87 (Tau_3 != zenon_X88) % 3.62/3.87 (Tau_5 != zenon_X86) % 3.62/3.87 (Tau_6 != zenon_X67) % 3.62/3.87 (zenon_X54 != zenon_X88) % 3.62/3.87 (zenon_X91 != zenon_X88) % 3.62/3.87 (zenon_X35 != Tau_6) % 3.62/3.87 (zenon_X62 != zenon_X33) % 3.62/3.87 (zenon_X24 != zenon_X46) % 3.62/3.87 (Tau_8 != zenon_X83) % 3.62/3.87 (-. (k04_buttercup10622 zenon_X68)) % 3.62/3.87 (-. (b48_buttercup10107 Tau_14)) % 3.62/3.87 (zenon_X33 != Tau_5) % 3.62/3.87 (zenon_X23 != zenon_X62) % 3.62/3.87 (zenon_X90 != Tau_17) % 3.62/3.87 (zenon_X81 != zenon_X32) % 3.62/3.87 (zenon_X72 != zenon_X61) % 3.62/3.87 (zenon_X86 != Tau_17) % 3.62/3.87 (zenon_X51 != Tau_8) % 3.62/3.87 (zenon_X33 != zenon_X60) % 3.62/3.87 (Tau_2 != zenon_X73) % 3.62/3.87 (Tau_6 != zenon_X59) % 3.62/3.87 (zenon_X90 != zenon_X47) % 3.62/3.87 (zenon_X65 != zenon_X75) % 3.62/3.87 (zenon_X84 != zenon_X56) % 3.62/3.87 (Tau_14 != zenon_X25) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X46)) % 3.62/3.87 (zenon_X77 != zenon_X73) % 3.62/3.87 (zenon_X54 != Tau_18) % 3.62/3.87 (k04_buttercup10622 Tau_5) % 3.62/3.87 (zenon_X78 != Tau_19) % 3.62/3.87 (zenon_X59 != zenon_X35) % 3.62/3.87 (zenon_X72 != Tau_10) % 3.62/3.87 (-. (k04_buttercup10619 Tau_20)) % 3.62/3.87 (zenon_X58 != Tau_15) % 3.62/3.87 (zenon_X28 != zenon_X89) % 3.62/3.87 (zenon_X91 != zenon_X21) % 3.62/3.87 (zenon_X23 != Tau_17) % 3.62/3.87 (zenon_X68 != zenon_X33) % 3.62/3.87 (zenon_X92 != zenon_X23) % 3.62/3.87 (Tau_9 != zenon_X53) % 3.62/3.87 (zenon_X48 != zenon_X82) % 3.62/3.87 (zenon_X82 != Tau_1) % 3.62/3.87 (zenon_X35 != Tau_15) % 3.62/3.87 (Tau_9 != zenon_X71) % 3.62/3.87 (zenon_X91 != zenon_X67) % 3.62/3.87 (Tau_3 != Tau_13) % 3.62/3.87 (Tau_20 != zenon_X56) % 3.62/3.87 (zenon_X81 != Tau_15) % 3.62/3.87 (zenon_X24 != zenon_X61) % 3.62/3.87 (Tau_13 != Tau_18) % 3.62/3.87 (k04_buttercup10622 Tau_3) % 3.62/3.87 (Tau_18 != Tau_10) % 3.62/3.87 (Tau_15 != Tau_7) % 3.62/3.87 (zenon_X72 != zenon_X35) % 3.62/3.87 (Tau_3 != zenon_X46) % 3.62/3.87 (zenon_X63 != zenon_X33) % 3.62/3.87 (zenon_X92 != zenon_X62) % 3.62/3.87 (-. (b48_buttercup10110 Tau_2)) % 3.62/3.87 (zenon_X68 != zenon_X22) % 3.62/3.87 (zenon_X65 != zenon_X71) % 3.62/3.87 (zenon_X77 != zenon_X87) % 3.62/3.87 (zenon_X45 != zenon_X67) % 3.62/3.87 (zenon_X61 != zenon_X81) % 3.62/3.87 (zenon_X46 != zenon_X50) % 3.62/3.87 (Tau_4 != Tau_19) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X46)) % 3.62/3.87 (Tau_9 != zenon_X49) % 3.62/3.87 (zenon_X79 != zenon_X67) % 3.62/3.87 (zenon_X25 != zenon_X47) % 3.62/3.87 (zenon_X78 != zenon_X73) % 3.62/3.87 (k04_buttercup10619 zenon_X85) % 3.62/3.87 (zenon_X33 != zenon_X56) % 3.62/3.87 (zenon_X86 != zenon_X79) % 3.62/3.87 (zenon_X82 != zenon_X73) % 3.62/3.87 (zenon_X92 != Tau_7) % 3.62/3.87 (zenon_X37 != Tau_20) % 3.62/3.87 (zenon_X76 != zenon_X87) % 3.62/3.87 (zenon_X35 != Tau_10) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X72)) % 3.62/3.87 (zenon_X72 != zenon_X86) % 3.62/3.87 (zenon_X59 != zenon_X85) % 3.62/3.87 (zenon_X91 != zenon_X82) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X65)) % 3.62/3.87 (zenon_X77 != zenon_X27) % 3.62/3.87 (zenon_X66 != zenon_X53) % 3.62/3.87 (zenon_X92 != zenon_X57) % 3.62/3.87 (zenon_X52 != zenon_X74) % 3.62/3.87 (zenon_X31 != zenon_X68) % 3.62/3.87 (Tau_3 != zenon_X36) % 3.62/3.87 (zenon_X33 != Tau_18) % 3.62/3.87 (zenon_X58 != zenon_X74) % 3.62/3.87 (zenon_X71 != zenon_X64) % 3.62/3.87 (zenon_X37 != Tau_0) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X83)) % 3.62/3.87 (zenon_X59 != zenon_X88) % 3.62/3.87 (zenon_X64 != zenon_X55) % 3.62/3.87 (zenon_X58 != zenon_X61) % 3.62/3.87 (zenon_X57 != zenon_X73) % 3.62/3.87 (zenon_X51 != zenon_X52) % 3.62/3.87 (zenon_X46 != Tau_18) % 3.62/3.87 (-. (b48_buttercup10111 Tau_5)) % 3.62/3.87 (Tau_6 != zenon_X23) % 3.62/3.87 (zenon_X32 != zenon_X45) % 3.62/3.87 (Tau_11 != zenon_X69) % 3.62/3.87 (zenon_X33 != zenon_X28) % 3.62/3.87 (zenon_X23 != zenon_X79) % 3.62/3.87 (-. (k04_buttercup10619 zenon_X45)) % 3.62/3.87 (zenon_X66 != zenon_X75) % 3.62/3.87 (zenon_X25 != zenon_X73) % 3.62/3.87 (Tau_3 != zenon_X45) % 3.62/3.87 (zenon_X31 != zenon_X45) % 3.62/3.87 (zenon_X37 != zenon_X92) % 3.62/3.87 (zenon_X88 != zenon_X67) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X26)) % 3.62/3.87 (Tau_2 != zenon_X75) % 3.62/3.87 (zenon_X76 != zenon_X56) % 3.62/3.87 (Tau_18 != zenon_X80) % 3.62/3.87 (-. (k04_buttercup10100 Tau_6)) % 3.62/3.87 (Tau_4 != Tau_17) % 3.62/3.87 (b48_buttercup10110 zenon_X78) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X26)) % 3.62/3.87 (zenon_X86 != Tau_1) % 3.62/3.87 (zenon_X71 != zenon_X28) % 3.62/3.87 (zenon_X60 != zenon_X91) % 3.62/3.87 (Tau_9 != zenon_X77) % 3.62/3.87 (Tau_7 != Tau_16) % 3.62/3.87 (Tau_14 != zenon_X50) % 3.62/3.87 (Tau_0 != Tau_16) % 3.62/3.87 (zenon_X31 != Tau_18) % 3.62/3.87 (zenon_X51 != Tau_1) % 3.62/3.87 (zenon_X78 != zenon_X87) % 3.62/3.87 (zenon_X47 != zenon_X75) % 3.62/3.87 (k04_buttercup10619 zenon_X59) % 3.62/3.87 (zenon_X49 != Tau_17) % 3.62/3.87 (zenon_X65 != zenon_X85) % 3.62/3.87 (zenon_X72 != zenon_X25) % 3.62/3.87 (zenon_X82 != zenon_X49) % 3.62/3.87 (zenon_X28 != Tau_2) % 3.62/3.87 (zenon_X23 != zenon_X67) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X25)) % 3.62/3.87 (zenon_X23 != zenon_X81) % 3.62/3.87 (zenon_X28 != Tau_19) % 3.62/3.87 (zenon_X26 != zenon_X71) % 3.62/3.87 (zenon_X77 != zenon_X49) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X47)) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X68)) % 3.62/3.87 (zenon_X76 != Tau_15) % 3.62/3.87 (Tau_3 != zenon_X77) % 3.62/3.87 (Tau_4 != zenon_X74) % 3.62/3.87 (Tau_11 != zenon_X76) % 3.62/3.87 (zenon_X65 != zenon_X63) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X28)) % 3.62/3.87 (Tau_13 != zenon_X45) % 3.62/3.87 (zenon_X74 != zenon_X22) % 3.62/3.87 (-. (k04_buttercup10622 Tau_0)) % 3.62/3.87 (Tau_7 != zenon_X49) % 3.62/3.87 (zenon_X70 != zenon_X61) % 3.62/3.87 (zenon_X60 != zenon_X23) % 3.62/3.87 (zenon_X73 != zenon_X50) % 3.62/3.87 (zenon_X28 != Tau_20) % 3.62/3.87 (zenon_X49 != zenon_X73) % 3.62/3.87 (zenon_X32 != zenon_X80) % 3.62/3.87 (-. (k04_buttercup10622 zenon_X90)) % 3.62/3.87 (Tau_19 != zenon_X74) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X79)) % 3.62/3.87 (b48_buttercup10108 zenon_X65) % 3.62/3.87 (Tau_5 != zenon_X50) % 3.62/3.87 (zenon_X24 != Tau_13) % 3.62/3.87 (zenon_X63 != Tau_8) % 3.62/3.87 (zenon_X25 != zenon_X33) % 3.62/3.87 (zenon_X53 != zenon_X80) % 3.62/3.87 (zenon_X92 != Tau_8) % 3.62/3.87 (zenon_X25 != zenon_X52) % 3.62/3.87 (zenon_X91 != zenon_X85) % 3.62/3.87 (b48_buttercup10098 zenon_X40) % 3.62/3.87 (zenon_X47 != zenon_X55) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X91)) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X67)) % 3.62/3.87 (Tau_3 != zenon_X83) % 3.62/3.87 (Tau_14 != zenon_X74) % 3.62/3.87 (zenon_X68 != zenon_X21) % 3.62/3.87 (zenon_X31 != Tau_2) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X31)) % 3.62/3.87 (zenon_X62 != zenon_X75) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X84)) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X82)) % 3.62/3.87 (zenon_X52 != zenon_X27) % 3.62/3.87 (k04_buttercup10619 Tau_9) % 3.62/3.87 (Tau_4 != zenon_X24) % 3.62/3.87 (Tau_5 != zenon_X23) % 3.62/3.87 (Tau_2 != zenon_X52) % 3.62/3.87 (zenon_X71 != zenon_X22) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X74)) % 3.62/3.87 (zenon_X60 != zenon_X24) % 3.62/3.87 (k04_buttercup10619 zenon_X25) % 3.62/3.87 (zenon_X80 != zenon_X85) % 3.62/3.87 (Tau_7 != zenon_X69) % 3.62/3.87 (zenon_X36 != zenon_X86) % 3.62/3.87 (zenon_X62 != zenon_X61) % 3.62/3.87 (zenon_X31 != zenon_X63) % 3.62/3.87 (Tau_7 != zenon_X77) % 3.62/3.87 (Tau_4 != zenon_X73) % 3.62/3.87 (-. (b48_buttercup10102 Tau_7)) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X84)) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X88)) % 3.62/3.87 (zenon_X35 != zenon_X32) % 3.62/3.87 (zenon_X26 != zenon_X63) % 3.62/3.87 (zenon_X25 != zenon_X64) % 3.62/3.87 (Tau_18 != zenon_X62) % 3.62/3.87 (zenon_X21 != zenon_X48) % 3.62/3.87 (zenon_X73 != zenon_X81) % 3.62/3.87 (zenon_X79 != zenon_X81) % 3.62/3.87 (zenon_X71 != zenon_X69) % 3.62/3.87 (zenon_X84 != zenon_X49) % 3.62/3.87 (zenon_X59 != zenon_X45) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X63)) % 3.62/3.87 (b48_buttercup10109 zenon_X45) % 3.62/3.87 (zenon_X30 != zenon_X63) % 3.62/3.87 (zenon_X70 != zenon_X49) % 3.62/3.87 (Tau_15 != Tau_19) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X46)) % 3.62/3.87 (zenon_X85 != zenon_X50) % 3.62/3.87 (zenon_X84 != Tau_18) % 3.62/3.87 (zenon_X68 != zenon_X90) % 3.62/3.87 (zenon_X48 != Tau_10) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X56)) % 3.62/3.87 (zenon_X71 != Tau_0) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X74)) % 3.62/3.87 (-. (k04_buttercup10622 zenon_X50)) % 3.62/3.87 (Tau_18 != zenon_X79) % 3.62/3.87 (Tau_7 != zenon_X71) % 3.62/3.87 (Tau_4 != zenon_X67) % 3.62/3.87 (zenon_X70 != zenon_X76) % 3.62/3.87 (Tau_7 != zenon_X90) % 3.62/3.87 (Tau_4 != zenon_X85) % 3.62/3.87 (k04_buttercup10622 zenon_X80) % 3.62/3.87 (zenon_X23 != zenon_X85) % 3.62/3.87 (zenon_X78 != Tau_15) % 3.62/3.87 (zenon_X86 != zenon_X85) % 3.62/3.87 (zenon_X37 != zenon_X50) % 3.62/3.87 (zenon_X47 != zenon_X92) % 3.62/3.87 (zenon_X46 != zenon_X67) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X27)) % 3.62/3.87 (zenon_X70 != zenon_X50) % 3.62/3.87 (zenon_X86 != zenon_X73) % 3.62/3.87 (b48_buttercup10102 zenon_X86) % 3.62/3.87 (Tau_7 != Tau_10) % 3.62/3.87 (zenon_X60 != zenon_X59) % 3.62/3.87 (Tau_5 != Tau_15) % 3.62/3.87 (Tau_13 != Tau_2) % 3.62/3.87 (zenon_X72 != zenon_X76) % 3.62/3.87 (zenon_X87 != zenon_X49) % 3.62/3.87 (zenon_X56 != zenon_X49) % 3.62/3.87 (zenon_X21 != Tau_14) % 3.62/3.87 (zenon_X27 != zenon_X67) % 3.62/3.87 (Tau_18 != zenon_X56) % 3.62/3.87 (zenon_X77 != zenon_X61) % 3.62/3.87 (zenon_X51 != zenon_X87) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X31)) % 3.62/3.87 (Tau_20 != zenon_X64) % 3.62/3.87 (Tau_2 != Tau_6) % 3.62/3.87 (Tau_2 != zenon_X58) % 3.62/3.87 (b48_buttercup10108 zenon_X91) % 3.62/3.87 (Tau_18 != zenon_X69) % 3.62/3.87 (zenon_X30 != zenon_X65) % 3.62/3.87 (-. (b48_buttercup10104 Tau_15)) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X30)) % 3.62/3.87 (zenon_X81 != zenon_X26) % 3.62/3.87 (zenon_X51 != zenon_X35) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X33)) % 3.62/3.87 (zenon_X83 != zenon_X56) % 3.62/3.87 (zenon_X48 != zenon_X80) % 3.62/3.87 (Tau_2 != Tau_16) % 3.62/3.87 (zenon_X70 != zenon_X33) % 3.62/3.87 (zenon_X60 != zenon_X62) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X57)) % 3.62/3.87 (Tau_0 != Tau_6) % 3.62/3.87 (Tau_2 != zenon_X27) % 3.62/3.87 (zenon_X58 != zenon_X50) % 3.62/3.87 (zenon_X35 != zenon_X27) % 3.62/3.87 (Tau_8 != zenon_X73) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X48)) % 3.62/3.87 (zenon_X52 != zenon_X56) % 3.62/3.87 (zenon_X25 != zenon_X21) % 3.62/3.87 (zenon_X84 != zenon_X80) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X83)) % 3.62/3.87 (zenon_X52 != zenon_X86) % 3.62/3.87 (zenon_X45 != zenon_X73) % 3.62/3.87 (zenon_X32 != zenon_X69) % 3.62/3.87 (Tau_4 != zenon_X63) % 3.62/3.87 (Tau_5 != zenon_X65) % 3.62/3.87 (zenon_X91 != Tau_15) % 3.62/3.87 (zenon_X66 != Tau_17) % 3.62/3.87 (zenon_X21 != zenon_X31) % 3.62/3.87 (zenon_X91 != zenon_X81) % 3.62/3.87 (zenon_X84 != zenon_X23) % 3.62/3.87 (zenon_X89 != zenon_X45) % 3.62/3.87 (b48_buttercup10107 zenon_X79) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X45)) % 3.62/3.87 (zenon_X54 != zenon_X87) % 3.62/3.87 (zenon_X30 != zenon_X73) % 3.62/3.87 (zenon_X65 != zenon_X52) % 3.62/3.87 (Tau_16 != Tau_1) % 3.62/3.87 (zenon_X89 != Tau_10) % 3.62/3.87 (Tau_19 != zenon_X56) % 3.62/3.87 (zenon_X51 != zenon_X92) % 3.62/3.87 (Tau_2 != Tau_9) % 3.62/3.87 (zenon_X37 != zenon_X45) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X58)) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X61)) % 3.62/3.87 (Tau_8 != Tau_6) % 3.62/3.87 (zenon_X28 != zenon_X76) % 3.62/3.87 (zenon_X27 != zenon_X55) % 3.62/3.87 (Tau_18 != zenon_X47) % 3.62/3.87 (zenon_X70 != Tau_15) % 3.62/3.87 (Tau_14 != zenon_X56) % 3.62/3.87 (zenon_X31 != zenon_X69) % 3.62/3.87 (zenon_X72 != zenon_X71) % 3.62/3.87 (zenon_X61 != zenon_X50) % 3.62/3.87 (k04_buttercup10619 zenon_X86) % 3.62/3.87 (zenon_X64 != zenon_X85) % 3.62/3.87 (k04_buttercup10622 zenon_X83) % 3.62/3.87 (zenon_X88 != zenon_X80) % 3.62/3.87 (zenon_X28 != zenon_X61) % 3.62/3.87 (zenon_X71 != zenon_X25) % 3.62/3.87 (Tau_16 != zenon_X69) % 3.62/3.87 (zenon_X31 != zenon_X85) % 3.62/3.87 (zenon_X24 != zenon_X73) % 3.62/3.87 (Tau_4 != zenon_X79) % 3.62/3.87 (zenon_X88 != zenon_X73) % 3.62/3.87 (zenon_X72 != zenon_X90) % 3.62/3.87 (zenon_X90 != zenon_X52) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X26)) % 3.62/3.87 (Tau_4 != zenon_X64) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X85)) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X74)) % 3.62/3.87 (zenon_X23 != zenon_X74) % 3.62/3.87 (zenon_X90 != zenon_X89) % 3.62/3.87 (zenon_X78 != zenon_X62) % 3.62/3.87 (zenon_X55 != zenon_X50) % 3.62/3.87 (zenon_X79 != zenon_X35) % 3.62/3.87 (b48_buttercup10110 zenon_X28) % 3.62/3.87 (k04_buttercup10622 Tau_11) % 3.62/3.87 (-. (k04_buttercup10622 zenon_X33)) % 3.62/3.87 (zenon_X31 != zenon_X58) % 3.62/3.87 (zenon_X59 != zenon_X21) % 3.62/3.87 (zenon_X60 != zenon_X85) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X73)) % 3.62/3.87 (Tau_8 != zenon_X27) % 3.62/3.87 (Tau_20 != zenon_X50) % 3.62/3.87 (-. (b48_buttercup10104 Tau_14)) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X60)) % 3.62/3.87 (zenon_X88 != Tau_2) % 3.62/3.87 (zenon_X54 != zenon_X64) % 3.62/3.87 (k04_buttercup10100 Tau_20) % 3.62/3.87 (Tau_13 != zenon_X60) % 3.62/3.87 (zenon_X84 != zenon_X59) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X68)) % 3.62/3.87 (Tau_14 != Tau_4) % 3.62/3.87 (zenon_X37 != Tau_1) % 3.62/3.87 (zenon_X88 != zenon_X90) % 3.62/3.87 (zenon_X31 != Tau_15) % 3.62/3.87 (zenon_X63 != zenon_X27) % 3.62/3.87 (Tau_6 != zenon_X90) % 3.62/3.87 (-. (b48_buttercup10102 Tau_16)) % 3.62/3.87 (zenon_X58 != zenon_X64) % 3.62/3.87 (Tau_6 != zenon_X77) % 3.62/3.87 (zenon_X77 != Tau_0) % 3.62/3.87 (zenon_X72 != zenon_X89) % 3.62/3.87 (zenon_X32 != zenon_X52) % 3.62/3.87 (zenon_X48 != Tau_18) % 3.62/3.87 (Tau_2 != zenon_X83) % 3.62/3.87 (zenon_X23 != zenon_X52) % 3.62/3.87 (Tau_3 != zenon_X27) % 3.62/3.87 (zenon_X68 != zenon_X69) % 3.62/3.87 (b48_buttercup10110 zenon_X48) % 3.62/3.87 (zenon_X48 != zenon_X25) % 3.62/3.87 (Tau_6 != zenon_X64) % 3.62/3.87 (Tau_5 != zenon_X57) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X62)) % 3.62/3.87 (zenon_X21 != zenon_X47) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X71)) % 3.62/3.87 (b48_buttercup10098 zenon_X41) % 3.62/3.87 (b48_buttercup10110 zenon_X31) % 3.62/3.87 (-. (b48_buttercup10102 Tau_5)) % 3.62/3.87 (zenon_X45 != zenon_X62) % 3.62/3.87 (zenon_X92 != zenon_X33) % 3.62/3.87 (k04_buttercup10622 zenon_X65) % 3.62/3.87 (b48_buttercup10110 zenon_X51) % 3.62/3.87 (zenon_X61 != Tau_1) % 3.62/3.87 (Tau_9 != zenon_X36) % 3.62/3.87 (zenon_X53 != zenon_X63) % 3.62/3.87 (b48_buttercup10110 zenon_X26) % 3.62/3.87 (zenon_X37 != Tau_8) % 3.62/3.87 (zenon_X32 != zenon_X87) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X47)) % 3.62/3.87 (zenon_X53 != zenon_X87) % 3.62/3.87 (zenon_X26 != Tau_19) % 3.62/3.87 (k04_buttercup10619 zenon_X63) % 3.62/3.87 (b48_buttercup10110 zenon_X66) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X27)) % 3.62/3.87 (k04_buttercup10622 zenon_X37) % 3.62/3.87 (Tau_3 != zenon_X89) % 3.62/3.87 (zenon_X60 != zenon_X75) % 3.62/3.87 (Tau_8 != zenon_X21) % 3.62/3.87 (zenon_X36 != zenon_X73) % 3.62/3.87 (zenon_X65 != Tau_10) % 3.62/3.87 (zenon_X32 != zenon_X89) % 3.62/3.87 (k04_buttercup10100 zenon_X21) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X54)) % 3.62/3.87 (Tau_10 != zenon_X67) % 3.62/3.87 (zenon_X65 != zenon_X81) % 3.62/3.87 (zenon_X89 != Tau_17) % 3.62/3.87 (Tau_8 != zenon_X87) % 3.62/3.87 (zenon_X81 != zenon_X27) % 3.62/3.87 (-. (b48_buttercup10111 Tau_11)) % 3.62/3.87 (zenon_X51 != zenon_X33) % 3.62/3.87 (Tau_1 != zenon_X56) % 3.62/3.87 (zenon_X59 != Tau_16) % 3.62/3.87 (k04_buttercup10622 zenon_X27) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X46)) % 3.62/3.87 (zenon_X62 != zenon_X55) % 3.62/3.87 (Tau_19 != zenon_X69) % 3.62/3.87 (-. (k04_buttercup10619 zenon_X21)) % 3.62/3.87 (zenon_X32 != Tau_16) % 3.62/3.87 (zenon_X70 != zenon_X73) % 3.62/3.87 (zenon_X37 != zenon_X58) % 3.62/3.87 (zenon_X88 != zenon_X61) % 3.62/3.87 (zenon_X92 != Tau_6) % 3.62/3.87 (zenon_X21 != zenon_X78) % 3.62/3.87 (zenon_X48 != zenon_X83) % 3.62/3.87 (zenon_X25 != zenon_X51) % 3.62/3.87 (zenon_X78 != zenon_X90) % 3.62/3.87 (zenon_X64 != zenon_X81) % 3.62/3.87 (zenon_X65 != zenon_X24) % 3.62/3.87 (zenon_X88 != Tau_13) % 3.62/3.87 (zenon_X88 != zenon_X79) % 3.62/3.87 (Tau_11 != Tau_13) % 3.62/3.87 (Tau_18 != zenon_X24) % 3.62/3.87 (Tau_9 != zenon_X74) % 3.62/3.87 (zenon_X32 != Tau_2) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X66)) % 3.62/3.87 (b48_buttercup10108 zenon_X36) % 3.62/3.87 (zenon_X31 != zenon_X59) % 3.62/3.87 (zenon_X23 != Tau_19) % 3.62/3.87 (zenon_X74 != zenon_X67) % 3.62/3.87 (zenon_X24 != zenon_X71) % 3.62/3.87 (zenon_X81 != zenon_X72) % 3.62/3.87 (zenon_X54 != zenon_X63) % 3.62/3.87 (zenon_X59 != zenon_X64) % 3.62/3.87 (zenon_X77 != zenon_X63) % 3.62/3.87 (zenon_X33 != zenon_X46) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X35)) % 3.62/3.87 (zenon_X59 != zenon_X57) % 3.62/3.87 (-. (k04_buttercup10619 zenon_X87)) % 3.62/3.87 (-. (k04_buttercup10622 zenon_X73)) % 3.62/3.87 (zenon_X70 != Tau_0) % 3.62/3.87 (Tau_18 != zenon_X52) % 3.62/3.87 (zenon_X24 != zenon_X67) % 3.62/3.87 (Tau_5 != Tau_16) % 3.62/3.87 (k04_buttercup10619 zenon_X82) % 3.62/3.87 (zenon_X82 != zenon_X56) % 3.62/3.87 (zenon_X21 != zenon_X37) % 3.62/3.87 (zenon_X65 != zenon_X90) % 3.62/3.87 (zenon_X60 != zenon_X53) % 3.62/3.87 (zenon_X53 != zenon_X27) % 3.62/3.87 (Tau_13 != Tau_8) % 3.62/3.87 (zenon_X59 != Tau_15) % 3.62/3.87 (zenon_X24 != zenon_X27) % 3.62/3.87 (zenon_X37 != zenon_X69) % 3.62/3.87 (zenon_X91 != Tau_0) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X26)) % 3.62/3.87 (zenon_X60 != zenon_X76) % 3.62/3.87 (zenon_X51 != zenon_X56) % 3.62/3.87 (zenon_X91 != zenon_X73) % 3.62/3.87 (Tau_11 != zenon_X46) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X49)) % 3.62/3.87 (zenon_X89 != zenon_X86) % 3.62/3.87 (zenon_X23 != zenon_X75) % 3.62/3.87 (zenon_X60 != zenon_X73) % 3.62/3.87 (Tau_7 != Tau_4) % 3.62/3.87 (zenon_X88 != zenon_X46) % 3.62/3.87 (zenon_X76 != zenon_X50) % 3.62/3.87 (Tau_4 != Tau_2) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X61)) % 3.62/3.87 (zenon_X45 != zenon_X50) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X52)) % 3.62/3.87 (-. (b48_buttercup10108 Tau_2)) % 3.62/3.87 (zenon_X25 != zenon_X45) % 3.62/3.87 (zenon_X61 != zenon_X69) % 3.62/3.87 (Tau_0 != Tau_10) % 3.62/3.87 (zenon_X54 != zenon_X82) % 3.62/3.87 (zenon_X60 != Tau_8) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X28)) % 3.62/3.87 (Tau_7 != zenon_X25) % 3.62/3.87 (Tau_16 != zenon_X85) % 3.62/3.87 (zenon_X36 != zenon_X82) % 3.62/3.87 (zenon_X68 != zenon_X86) % 3.62/3.87 (Tau_5 != Tau_20) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X24)) % 3.62/3.87 (zenon_X83 != zenon_X45) % 3.62/3.87 (zenon_X35 != zenon_X57) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X75)) % 3.62/3.87 (zenon_X83 != zenon_X55) % 3.62/3.87 (zenon_X54 != zenon_X24) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X47)) % 3.62/3.87 (zenon_X66 != zenon_X68) % 3.62/3.87 (zenon_X57 != Tau_15) % 3.62/3.87 (-. (k04_buttercup10100 Tau_11)) % 3.62/3.87 (zenon_X54 != zenon_X62) % 3.62/3.87 (Tau_20 != zenon_X69) % 3.62/3.87 (zenon_X83 != zenon_X61) % 3.62/3.87 (zenon_X64 != Tau_17) % 3.62/3.87 (zenon_X51 != zenon_X64) % 3.62/3.87 (zenon_X31 != zenon_X62) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X54)) % 3.62/3.87 (zenon_X53 != zenon_X51) % 3.62/3.87 (Tau_1 != zenon_X87) % 3.62/3.87 (zenon_X26 != Tau_17) % 3.62/3.87 (zenon_X33 != Tau_17) % 3.62/3.87 (zenon_X37 != zenon_X36) % 3.62/3.87 (zenon_X66 != zenon_X61) % 3.62/3.87 (zenon_X76 != zenon_X22) % 3.62/3.87 (zenon_X68 != Tau_2) % 3.62/3.87 (zenon_X68 != zenon_X92) % 3.62/3.87 (zenon_X82 != Tau_2) % 3.62/3.87 (zenon_X23 != zenon_X47) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X49)) % 3.62/3.87 (zenon_X48 != zenon_X53) % 3.62/3.87 (Tau_9 != zenon_X62) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X36)) % 3.62/3.87 (zenon_X52 != zenon_X22) % 3.62/3.87 (Tau_3 != Tau_15) % 3.62/3.87 (zenon_X60 != zenon_X27) % 3.62/3.87 (zenon_X77 != Tau_8) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X74)) % 3.62/3.87 (Tau_8 != zenon_X56) % 3.62/3.87 (Tau_18 != zenon_X87) % 3.62/3.87 (zenon_X45 != zenon_X22) % 3.62/3.87 (zenon_X77 != zenon_X68) % 3.62/3.87 (Tau_20 != zenon_X74) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X68)) % 3.62/3.87 (Tau_13 != zenon_X65) % 3.62/3.87 (Tau_7 != zenon_X58) % 3.62/3.87 (zenon_X78 != zenon_X67) % 3.62/3.87 (zenon_X65 != Tau_1) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X67)) % 3.62/3.87 (zenon_X68 != zenon_X56) % 3.62/3.87 (zenon_X58 != zenon_X67) % 3.62/3.87 (zenon_X82 != zenon_X67) % 3.62/3.87 (zenon_X78 != zenon_X49) % 3.62/3.87 (zenon_X92 != zenon_X70) % 3.62/3.87 (Tau_19 != zenon_X75) % 3.62/3.87 (zenon_X28 != zenon_X53) % 3.62/3.87 (zenon_X49 != zenon_X22) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X83)) % 3.62/3.87 (zenon_X26 != zenon_X76) % 3.62/3.87 (Tau_6 != Tau_18) % 3.62/3.87 (zenon_X35 != zenon_X31) % 3.62/3.87 (Tau_16 != zenon_X61) % 3.62/3.87 (zenon_X91 != zenon_X24) % 3.62/3.87 (zenon_X78 != Tau_0) % 3.62/3.87 (zenon_X33 != Tau_3) % 3.62/3.87 (zenon_X83 != zenon_X62) % 3.62/3.87 (zenon_X30 != zenon_X61) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X82)) % 3.62/3.87 (zenon_X32 != zenon_X61) % 3.62/3.87 (zenon_X91 != zenon_X46) % 3.62/3.87 (-. (b48_buttercup10110 Tau_13)) % 3.62/3.87 (zenon_X28 != Tau_1) % 3.62/3.87 (zenon_X66 != Tau_1) % 3.62/3.87 (zenon_X31 != zenon_X86) % 3.62/3.87 (zenon_X54 != zenon_X47) % 3.62/3.87 (zenon_X48 != zenon_X87) % 3.62/3.87 (zenon_X37 != Tau_19) % 3.62/3.87 (zenon_X63 != Tau_0) % 3.62/3.87 (zenon_X30 != zenon_X46) % 3.62/3.87 (zenon_X31 != zenon_X91) % 3.62/3.87 (zenon_X23 != zenon_X82) % 3.62/3.87 (Tau_9 != zenon_X85) % 3.62/3.87 (Tau_16 != zenon_X86) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X56)) % 3.62/3.87 (zenon_X27 != Tau_17) % 3.62/3.87 (Tau_18 != zenon_X81) % 3.62/3.87 (zenon_X90 != zenon_X91) % 3.62/3.87 (zenon_X48 != zenon_X89) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X51)) % 3.62/3.87 (zenon_X76 != zenon_X86) % 3.62/3.87 (zenon_X78 != zenon_X68) % 3.62/3.87 (zenon_X51 != zenon_X23) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X92)) % 3.62/3.87 (zenon_X37 != Tau_16) % 3.62/3.87 (zenon_X28 != zenon_X73) % 3.62/3.87 (zenon_X83 != zenon_X63) % 3.62/3.87 (zenon_X84 != zenon_X68) % 3.62/3.87 (zenon_X81 != zenon_X28) % 3.62/3.87 (Tau_19 != zenon_X52) % 3.62/3.87 (zenon_X59 != zenon_X67) % 3.62/3.87 (Tau_11 != zenon_X59) % 3.62/3.87 (zenon_X28 != zenon_X65) % 3.62/3.87 (zenon_X45 != zenon_X27) % 3.62/3.87 (zenon_X26 != zenon_X77) % 3.62/3.87 (zenon_X54 != zenon_X76) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X66)) % 3.62/3.87 (Tau_7 != zenon_X65) % 3.62/3.87 (Tau_4 != zenon_X61) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X25)) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X87)) % 3.62/3.87 (zenon_X35 != zenon_X62) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X69)) % 3.62/3.87 (zenon_X70 != zenon_X57) % 3.62/3.87 (Tau_9 != zenon_X90) % 3.62/3.87 (Tau_11 != zenon_X49) % 3.62/3.87 (zenon_X59 != zenon_X63) % 3.62/3.87 (zenon_X90 != zenon_X75) % 3.62/3.87 (zenon_X63 != Tau_10) % 3.62/3.87 (Tau_19 != zenon_X89) % 3.62/3.87 (zenon_X45 != zenon_X49) % 3.62/3.87 (zenon_X71 != zenon_X58) % 3.62/3.87 (zenon_X49 != zenon_X61) % 3.62/3.87 (Tau_3 != Tau_17) % 3.62/3.87 (zenon_X53 != zenon_X47) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X58)) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X22)) % 3.62/3.87 (Tau_9 != zenon_X23) % 3.62/3.87 (Tau_3 != zenon_X65) % 3.62/3.87 (Tau_4 != zenon_X62) % 3.62/3.87 (k04_buttercup10100 Tau_8) % 3.62/3.87 (zenon_X72 != zenon_X85) % 3.62/3.87 (zenon_X59 != zenon_X22) % 3.62/3.87 (zenon_X36 != zenon_X68) % 3.62/3.87 (zenon_X92 != zenon_X90) % 3.62/3.87 (zenon_X76 != zenon_X46) % 3.62/3.87 (Tau_14 != zenon_X71) % 3.62/3.87 (-. (b48_buttercup10111 Tau_9)) % 3.62/3.87 (zenon_X64 != zenon_X21) % 3.62/3.87 (Tau_19 != zenon_X58) % 3.62/3.87 (zenon_X89 != Tau_16) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X47)) % 3.62/3.87 (b48_buttercup10110 zenon_X30) % 3.62/3.87 (zenon_X68 != Tau_8) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X52)) % 3.62/3.87 (zenon_X27 != zenon_X33) % 3.62/3.87 (zenon_X65 != zenon_X62) % 3.62/3.87 (Tau_20 != zenon_X48) % 3.62/3.87 (zenon_X72 != Tau_0) % 3.62/3.87 (Tau_20 != zenon_X49) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X32)) % 3.62/3.87 (zenon_X84 != Tau_1) % 3.62/3.87 (zenon_X37 != zenon_X70) % 3.62/3.87 (zenon_X81 != zenon_X51) % 3.62/3.87 (zenon_X78 != zenon_X70) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X46)) % 3.62/3.87 (zenon_X57 != zenon_X79) % 3.62/3.87 (zenon_X88 != zenon_X92) % 3.62/3.87 (zenon_X61 != zenon_X87) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X28)) % 3.62/3.87 (zenon_X54 != Tau_2) % 3.62/3.87 (zenon_X59 != zenon_X76) % 3.62/3.87 (zenon_X55 != zenon_X61) % 3.62/3.87 (Tau_14 != zenon_X36) % 3.62/3.87 (zenon_X27 != zenon_X22) % 3.62/3.87 (zenon_X76 != zenon_X81) % 3.62/3.87 (zenon_X65 != zenon_X61) % 3.62/3.87 (zenon_X58 != zenon_X62) % 3.62/3.87 (zenon_X61 != zenon_X71) % 3.62/3.87 (-. (b48_buttercup10102 Tau_3)) % 3.62/3.87 (Tau_11 != zenon_X67) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X52)) % 3.62/3.87 (zenon_X89 != zenon_X57) % 3.62/3.87 (zenon_X88 != zenon_X27) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X92)) % 3.62/3.87 (zenon_X77 != zenon_X76) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X81)) % 3.62/3.87 (zenon_X36 != Tau_16) % 3.62/3.87 (zenon_X49 != Tau_10) % 3.62/3.87 (zenon_X81 != Tau_14) % 3.62/3.87 (zenon_X84 != zenon_X25) % 3.62/3.87 (-. (b48_buttercup10102 Tau_1)) % 3.62/3.87 (zenon_X33 != zenon_X31) % 3.62/3.87 (Tau_20 != zenon_X21) % 3.62/3.87 (Tau_0 != zenon_X48) % 3.62/3.87 (zenon_X51 != zenon_X46) % 3.62/3.87 (zenon_X60 != zenon_X45) % 3.62/3.87 (Tau_16 != zenon_X55) % 3.62/3.87 (zenon_X36 != zenon_X81) % 3.62/3.87 (Tau_8 != zenon_X48) % 3.62/3.87 (k04_buttercup10619 zenon_X74) % 3.62/3.87 (zenon_X48 != zenon_X45) % 3.62/3.87 (zenon_X60 != zenon_X52) % 3.62/3.87 (Tau_4 != Tau_16) % 3.62/3.87 (zenon_X91 != Tau_1) % 3.62/3.87 (zenon_X28 != Tau_18) % 3.62/3.87 (zenon_X88 != Tau_15) % 3.62/3.87 (zenon_X83 != zenon_X49) % 3.62/3.87 (zenon_X71 != zenon_X56) % 3.62/3.87 (zenon_X74 != Tau_17) % 3.62/3.87 (Tau_11 != Tau_0) % 3.62/3.87 (zenon_X65 != zenon_X73) % 3.62/3.87 (Tau_10 != Tau_16) % 3.62/3.87 (zenon_X28 != zenon_X63) % 3.62/3.87 (zenon_X28 != zenon_X49) % 3.62/3.87 (zenon_X92 != zenon_X59) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X78)) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X31)) % 3.62/3.87 (zenon_X65 != zenon_X69) % 3.62/3.87 (Tau_9 != Tau_13) % 3.62/3.87 (Tau_1 != zenon_X25) % 3.62/3.87 (Tau_18 != zenon_X51) % 3.62/3.87 (-. (b48_buttercup10107 Tau_15)) % 3.62/3.87 (zenon_X27 != Tau_0) % 3.62/3.87 (b48_buttercup10108 zenon_X53) % 3.62/3.87 (zenon_X70 != Tau_10) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X90)) % 3.62/3.87 (zenon_X69 != Tau_0) % 3.62/3.87 (zenon_X23 != zenon_X35) % 3.62/3.87 (Tau_3 != zenon_X56) % 3.62/3.87 (zenon_X58 != zenon_X75) % 3.62/3.87 (Tau_6 != Tau_17) % 3.62/3.87 (zenon_X92 != Tau_2) % 3.62/3.87 (zenon_X57 != zenon_X56) % 3.62/3.87 (zenon_X77 != zenon_X47) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X88)) % 3.62/3.87 (zenon_X46 != zenon_X81) % 3.62/3.87 (zenon_X53 != Tau_17) % 3.62/3.87 (Tau_2 != Tau_0) % 3.62/3.87 (zenon_X60 != zenon_X87) % 3.62/3.87 (zenon_X25 != Tau_13) % 3.62/3.87 (Tau_9 != zenon_X24) % 3.62/3.87 (zenon_X51 != zenon_X86) % 3.62/3.87 (zenon_X30 != zenon_X22) % 3.62/3.87 (Tau_7 != Tau_19) % 3.62/3.87 (zenon_X31 != Tau_1) % 3.62/3.87 (zenon_X21 != zenon_X62) % 3.62/3.87 (zenon_X82 != zenon_X86) % 3.62/3.87 (zenon_X47 != Tau_0) % 3.62/3.87 (zenon_X56 != zenon_X74) % 3.62/3.87 (zenon_X32 != Tau_19) % 3.62/3.87 (Tau_9 != zenon_X61) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X57)) % 3.62/3.87 (zenon_X28 != zenon_X59) % 3.62/3.87 (zenon_X83 != zenon_X80) % 3.62/3.87 (zenon_X25 != Tau_15) % 3.62/3.87 (Tau_7 != zenon_X52) % 3.62/3.87 (Tau_5 != Tau_0) % 3.62/3.87 (zenon_X23 != zenon_X24) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X65)) % 3.62/3.87 (zenon_X23 != zenon_X71) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X84)) % 3.62/3.87 (zenon_X51 != zenon_X82) % 3.62/3.87 (zenon_X89 != zenon_X63) % 3.62/3.87 (zenon_X77 != zenon_X22) % 3.62/3.87 (-. (b48_buttercup10104 Tau_1)) % 3.62/3.87 (zenon_X24 != zenon_X90) % 3.62/3.87 (zenon_X53 != zenon_X76) % 3.62/3.87 (b48_buttercup10109 zenon_X33) % 3.62/3.87 (zenon_X28 != zenon_X45) % 3.62/3.87 (zenon_X88 != zenon_X74) % 3.62/3.87 (zenon_X30 != zenon_X76) % 3.62/3.87 (zenon_X78 != zenon_X61) % 3.62/3.87 (zenon_X35 != zenon_X64) % 3.62/3.87 (Tau_5 != zenon_X25) % 3.62/3.87 (zenon_X51 != zenon_X69) % 3.62/3.87 (zenon_X76 != zenon_X61) % 3.62/3.87 (zenon_X88 != zenon_X71) % 3.62/3.87 (zenon_X66 != zenon_X45) % 3.62/3.87 (Tau_3 != zenon_X86) % 3.62/3.87 (Tau_11 != zenon_X58) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X70)) % 3.62/3.87 (-. (b48_buttercup10104 Tau_6)) % 3.62/3.87 (Tau_11 != zenon_X82) % 3.62/3.87 (Tau_14 != zenon_X23) % 3.62/3.87 (Tau_6 != zenon_X62) % 3.62/3.87 (k04_buttercup10619 zenon_X64) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X32)) % 3.62/3.87 (zenon_X50 != zenon_X69) % 3.62/3.87 (zenon_X85 != zenon_X92) % 3.62/3.87 (zenon_X48 != zenon_X75) % 3.62/3.87 (-. (b48_buttercup10111 Tau_6)) % 3.62/3.87 (zenon_X25 != zenon_X22) % 3.62/3.87 (zenon_X32 != zenon_X49) % 3.62/3.87 (zenon_X55 != zenon_X92) % 3.62/3.87 (zenon_X68 != zenon_X45) % 3.62/3.87 (-. (k04_buttercup10619 Tau_13)) % 3.62/3.87 (zenon_X66 != zenon_X58) % 3.62/3.87 (Tau_9 != zenon_X57) % 3.62/3.87 (zenon_X61 != zenon_X92) % 3.62/3.87 (zenon_X91 != zenon_X50) % 3.62/3.87 (zenon_X76 != Tau_17) % 3.62/3.87 (zenon_X51 != zenon_X62) % 3.62/3.87 (zenon_X48 != zenon_X85) % 3.62/3.87 (Tau_7 != zenon_X45) % 3.62/3.87 (zenon_X49 != zenon_X79) % 3.62/3.87 (Tau_1 != zenon_X49) % 3.62/3.87 (b48_buttercup10109 zenon_X71) % 3.62/3.87 (zenon_X47 != zenon_X87) % 3.62/3.87 (zenon_X82 != zenon_X46) % 3.62/3.87 (zenon_X64 != zenon_X33) % 3.62/3.87 (zenon_X72 != Tau_15) % 3.62/3.87 (zenon_X73 != zenon_X67) % 3.62/3.87 (Tau_3 != Tau_1) % 3.62/3.87 (zenon_X36 != zenon_X76) % 3.62/3.87 (zenon_X57 != Tau_0) % 3.62/3.87 (Tau_9 != zenon_X58) % 3.62/3.87 (Tau_5 != zenon_X49) % 3.62/3.87 (Tau_1 != zenon_X67) % 3.62/3.87 (zenon_X36 != zenon_X21) % 3.62/3.87 (zenon_X21 != zenon_X51) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X71)) % 3.62/3.87 (zenon_X46 != zenon_X22) % 3.62/3.87 (zenon_X90 != zenon_X55) % 3.62/3.87 (-. (k04_buttercup10100 Tau_14)) % 3.62/3.87 (zenon_X35 != zenon_X48) % 3.62/3.87 (k04_buttercup10619 zenon_X62) % 3.62/3.87 (zenon_X37 != zenon_X46) % 3.62/3.87 (zenon_X36 != zenon_X88) % 3.62/3.87 (zenon_X21 != zenon_X32) % 3.62/3.87 (Tau_9 != zenon_X75) % 3.62/3.87 (-. (b48_buttercup10104 Tau_4)) % 3.62/3.87 (zenon_X70 != zenon_X67) % 3.62/3.87 (zenon_X60 != zenon_X58) % 3.62/3.87 (zenon_X72 != zenon_X77) % 3.62/3.87 (zenon_X60 != Tau_17) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X78)) % 3.62/3.87 (Tau_14 != Tau_20) % 3.62/3.87 (Tau_15 != zenon_X79) % 3.62/3.87 (Tau_16 != Tau_14) % 3.62/3.87 (zenon_X91 != zenon_X92) % 3.62/3.87 (zenon_X63 != zenon_X21) % 3.62/3.87 (zenon_X82 != zenon_X87) % 3.62/3.87 (k04_buttercup10622 zenon_X84) % 3.62/3.87 (zenon_X24 != zenon_X62) % 3.62/3.87 (Tau_11 != Tau_18) % 3.62/3.87 (zenon_X35 != zenon_X75) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X53)) % 3.62/3.87 (k04_buttercup10619 Tau_4) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X91)) % 3.62/3.87 (zenon_X52 != zenon_X45) % 3.62/3.87 (Tau_14 != zenon_X80) % 3.62/3.87 (zenon_X58 != zenon_X88) % 3.62/3.87 (zenon_X73 != Tau_13) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X72)) % 3.62/3.87 (-. (b48_buttercup10104 Tau_7)) % 3.62/3.87 (zenon_X53 != zenon_X62) % 3.62/3.87 (zenon_X66 != zenon_X59) % 3.62/3.87 (Tau_7 != zenon_X57) % 3.62/3.87 (zenon_X32 != zenon_X46) % 3.62/3.87 (zenon_X76 != zenon_X92) % 3.62/3.87 (zenon_X28 != Tau_4) % 3.62/3.87 (zenon_X54 != zenon_X22) % 3.62/3.87 (zenon_X70 != zenon_X69) % 3.62/3.87 (zenon_X70 != zenon_X63) % 3.62/3.87 (Tau_20 != zenon_X67) % 3.62/3.87 (k04_buttercup10622 zenon_X91) % 3.62/3.87 (-. (k04_buttercup10100 Tau_4)) % 3.62/3.87 (zenon_X83 != zenon_X47) % 3.62/3.87 (zenon_X71 != zenon_X48) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X71)) % 3.62/3.87 (zenon_X37 != Tau_13) % 3.62/3.87 (zenon_X32 != zenon_X82) % 3.62/3.87 (b48_buttercup10107 zenon_X73) % 3.62/3.87 (zenon_X48 != Tau_4) % 3.62/3.87 (-. (b48_buttercup10102 Tau_13)) % 3.62/3.87 (zenon_X80 != zenon_X46) % 3.62/3.87 (zenon_X32 != zenon_X73) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X57)) % 3.62/3.87 (b48_buttercup10107 Tau_17) % 3.62/3.87 (zenon_X31 != zenon_X46) % 3.62/3.87 (zenon_X62 != Tau_0) % 3.62/3.87 (zenon_X35 != Tau_7) % 3.62/3.87 (zenon_X88 != zenon_X50) % 3.62/3.87 (zenon_X53 != zenon_X24) % 3.62/3.87 (zenon_X51 != Tau_10) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X50)) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X21)) % 3.62/3.87 (Tau_10 != Tau_20) % 3.62/3.87 (Tau_2 != zenon_X69) % 3.62/3.87 (zenon_X23 != Tau_2) % 3.62/3.87 (zenon_X65 != zenon_X50) % 3.62/3.87 (zenon_X71 != zenon_X80) % 3.62/3.87 (zenon_X26 != zenon_X24) % 3.62/3.87 (zenon_X70 != zenon_X47) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X67)) % 3.62/3.87 (Tau_9 != zenon_X88) % 3.62/3.87 (zenon_X77 != zenon_X86) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X76)) % 3.62/3.87 (zenon_X30 != zenon_X47) % 3.62/3.87 (Tau_18 != zenon_X50) % 3.62/3.87 (zenon_X86 != zenon_X67) % 3.62/3.87 (zenon_X31 != zenon_X76) % 3.62/3.87 (zenon_X89 != zenon_X52) % 3.62/3.87 (Tau_6 != zenon_X80) % 3.62/3.87 (-. (b48_buttercup10111 Tau_2)) % 3.62/3.87 (Tau_8 != zenon_X47) % 3.62/3.87 (zenon_X79 != zenon_X45) % 3.62/3.87 (Tau_18 != zenon_X63) % 3.62/3.87 (zenon_X72 != zenon_X49) % 3.62/3.87 (zenon_X37 != zenon_X59) % 3.62/3.87 (Tau_10 != zenon_X50) % 3.62/3.87 (zenon_X30 != zenon_X58) % 3.62/3.87 (-. (b48_buttercup10109 Tau_6)) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X89)) % 3.62/3.87 (zenon_X74 != zenon_X55) % 3.62/3.87 (Tau_3 != zenon_X80) % 3.62/3.87 (zenon_X36 != zenon_X52) % 3.62/3.87 (Tau_6 != Tau_1) % 3.62/3.87 (zenon_X78 != Tau_1) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X61)) % 3.62/3.87 (zenon_X77 != zenon_X24) % 3.62/3.87 (zenon_X48 != zenon_X58) % 3.62/3.87 (zenon_X35 != zenon_X52) % 3.62/3.87 (-. (k04_buttercup10622 zenon_X21)) % 3.62/3.87 (zenon_X85 != zenon_X33) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X85)) % 3.62/3.87 (zenon_X90 != zenon_X70) % 3.62/3.87 (zenon_X77 != zenon_X71) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X27)) % 3.62/3.87 (-. (b48_buttercup10107 Tau_3)) % 3.62/3.87 (zenon_X45 != zenon_X55) % 3.62/3.87 (Tau_13 != Tau_19) % 3.62/3.87 (zenon_X36 != zenon_X45) % 3.62/3.87 (zenon_X36 != zenon_X24) % 3.62/3.87 (-. (b48_buttercup10111 Tau_15)) % 3.62/3.87 (Tau_7 != zenon_X27) % 3.62/3.87 (Tau_3 != zenon_X22) % 3.62/3.87 (zenon_X51 != Tau_20) % 3.62/3.87 (-. (k04_buttercup10622 zenon_X22)) % 3.62/3.87 (zenon_X63 != zenon_X61) % 3.62/3.87 (Tau_7 != Tau_2) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X55)) % 3.62/3.87 (k04_buttercup10619 Tau_18) % 3.62/3.87 (zenon_X91 != zenon_X63) % 3.62/3.87 (zenon_X52 != zenon_X21) % 3.62/3.87 (zenon_X54 != zenon_X79) % 3.62/3.87 (zenon_X28 != zenon_X27) % 3.62/3.87 (zenon_X91 != zenon_X87) % 3.62/3.87 (zenon_X89 != zenon_X88) % 3.62/3.87 (zenon_X54 != Tau_16) % 3.62/3.87 (Tau_3 != zenon_X49) % 3.62/3.87 (zenon_X78 != zenon_X59) % 3.62/3.87 (zenon_X71 != zenon_X83) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X49)) % 3.62/3.87 (zenon_X73 != zenon_X47) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X22)) % 3.62/3.87 (Tau_18 != zenon_X75) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X45)) % 3.62/3.87 (zenon_X86 != Tau_10) % 3.62/3.87 (zenon_X55 != zenon_X87) % 3.62/3.87 (zenon_X23 != zenon_X68) % 3.62/3.87 (zenon_X91 != zenon_X79) % 3.62/3.87 (zenon_X32 != zenon_X67) % 3.62/3.87 (k04_buttercup10619 zenon_X76) % 3.62/3.87 (zenon_X33 != zenon_X22) % 3.62/3.87 (zenon_X32 != zenon_X57) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X73)) % 3.62/3.87 (zenon_X76 != zenon_X90) % 3.62/3.87 (Tau_7 != Tau_20) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X21)) % 3.62/3.87 (zenon_X35 != Tau_0) % 3.62/3.87 (-. (b48_buttercup10107 Tau_11)) % 3.62/3.87 (-. (k04_buttercup10619 zenon_X35)) % 3.62/3.87 (b48_buttercup10098 Tau_20) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X35)) % 3.62/3.87 (Tau_11 != Tau_16) % 3.62/3.87 (zenon_X68 != zenon_X67) % 3.62/3.87 (zenon_X31 != zenon_X25) % 3.62/3.87 (zenon_X72 != zenon_X63) % 3.62/3.87 (-. (b48_buttercup10111 Tau_8)) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X66)) % 3.62/3.87 (zenon_X57 != zenon_X86) % 3.62/3.87 (Tau_16 != zenon_X81) % 3.62/3.87 (zenon_X32 != zenon_X77) % 3.62/3.87 (Tau_11 != zenon_X23) % 3.62/3.87 (Tau_9 != zenon_X65) % 3.62/3.87 (Tau_19 != zenon_X87) % 3.62/3.87 (zenon_X70 != zenon_X79) % 3.62/3.87 (Tau_14 != zenon_X86) % 3.62/3.87 (zenon_X77 != zenon_X75) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X51)) % 3.62/3.87 (Tau_0 != Tau_9) % 3.62/3.87 (zenon_X28 != zenon_X22) % 3.62/3.87 (zenon_X33 != zenon_X67) % 3.62/3.87 (zenon_X58 != zenon_X45) % 3.62/3.87 (Tau_17 != Tau_11) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X77)) % 3.62/3.87 (zenon_X31 != zenon_X73) % 3.62/3.87 (-. (b48_buttercup10104 Tau_17)) % 3.62/3.87 (zenon_X59 != Tau_19) % 3.62/3.87 (Tau_16 != Tau_13) % 3.62/3.87 (Tau_2 != zenon_X62) % 3.62/3.87 (-. (b48_buttercup10104 Tau_20)) % 3.62/3.87 (zenon_X84 != Tau_16) % 3.62/3.87 (zenon_X25 != zenon_X82) % 3.62/3.87 (Tau_8 != zenon_X67) % 3.62/3.87 (b48_buttercup10098 zenon_X44) % 3.62/3.87 (zenon_X71 != zenon_X91) % 3.62/3.87 (zenon_X21 != zenon_X72) % 3.62/3.87 (zenon_X62 != Tau_17) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X87)) % 3.62/3.87 (zenon_X36 != zenon_X61) % 3.62/3.87 (zenon_X36 != zenon_X79) % 3.62/3.87 (zenon_X32 != zenon_X24) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X22)) % 3.62/3.87 (zenon_X48 != zenon_X23) % 3.62/3.87 (zenon_X83 != zenon_X27) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X52)) % 3.62/3.87 (zenon_X30 != zenon_X27) % 3.62/3.87 (k04_buttercup10622 zenon_X82) % 3.62/3.87 (zenon_X78 != Tau_18) % 3.62/3.87 (Tau_8 != Tau_0) % 3.62/3.87 (Tau_11 != zenon_X61) % 3.62/3.87 (Tau_3 != zenon_X70) % 3.62/3.87 (Tau_2 != zenon_X50) % 3.62/3.87 (zenon_X26 != zenon_X79) % 3.62/3.87 (zenon_X71 != zenon_X81) % 3.62/3.87 (zenon_X21 != zenon_X66) % 3.62/3.87 (zenon_X54 != zenon_X68) % 3.62/3.87 (Tau_9 != Tau_20) % 3.62/3.87 (Tau_2 != zenon_X57) % 3.62/3.87 (zenon_X86 != zenon_X46) % 3.62/3.87 (zenon_X23 != zenon_X86) % 3.62/3.87 (b48_buttercup10109 Tau_2) % 3.62/3.87 (k04_buttercup10622 zenon_X70) % 3.62/3.87 (zenon_X78 != zenon_X76) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X73)) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X24)) % 3.62/3.87 (zenon_X30 != zenon_X45) % 3.62/3.87 (zenon_X49 != zenon_X92) % 3.62/3.87 (Tau_14 != zenon_X61) % 3.62/3.87 (zenon_X32 != Tau_20) % 3.62/3.87 (zenon_X71 != zenon_X55) % 3.62/3.87 (zenon_X68 != zenon_X63) % 3.62/3.87 (zenon_X92 != zenon_X54) % 3.62/3.87 (zenon_X71 != zenon_X27) % 3.62/3.87 (zenon_X33 != Tau_11) % 3.62/3.87 (zenon_X32 != zenon_X23) % 3.62/3.87 (Tau_4 != Tau_10) % 3.62/3.87 (Tau_9 != zenon_X91) % 3.62/3.87 (k04_buttercup10622 zenon_X57) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X78)) % 3.62/3.87 (zenon_X51 != zenon_X74) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X51)) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X37)) % 3.62/3.87 (zenon_X51 != zenon_X90) % 3.62/3.87 (Tau_6 != zenon_X87) % 3.62/3.87 (zenon_X71 != Tau_4) % 3.62/3.87 (zenon_X77 != zenon_X35) % 3.62/3.87 (Tau_13 != zenon_X74) % 3.62/3.87 (zenon_X64 != zenon_X73) % 3.62/3.87 (zenon_X88 != zenon_X22) % 3.62/3.87 (zenon_X78 != zenon_X88) % 3.62/3.87 (Tau_14 != zenon_X22) % 3.62/3.87 (zenon_X35 != zenon_X55) % 3.62/3.87 (zenon_X61 != zenon_X21) % 3.62/3.87 (Tau_4 != zenon_X88) % 3.62/3.87 (Tau_5 != zenon_X90) % 3.62/3.87 (-. (b48_buttercup10107 Tau_7)) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X30)) % 3.62/3.87 (zenon_X88 != Tau_10) % 3.62/3.87 (-. (b48_buttercup10109 Tau_0)) % 3.62/3.87 (Tau_19 != zenon_X22) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X91)) % 3.62/3.87 (zenon_X91 != zenon_X68) % 3.62/3.87 (zenon_X66 != zenon_X56) % 3.62/3.87 (zenon_X27 != zenon_X92) % 3.62/3.87 (zenon_X31 != zenon_X53) % 3.62/3.87 (zenon_X60 != zenon_X68) % 3.62/3.87 (Tau_5 != zenon_X36) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X83)) % 3.62/3.87 (zenon_X77 != zenon_X85) % 3.62/3.87 (zenon_X30 != zenon_X80) % 3.62/3.87 (zenon_X37 != zenon_X53) % 3.62/3.87 (zenon_X35 != zenon_X74) % 3.62/3.87 (zenon_X73 != zenon_X56) % 3.62/3.87 (zenon_X57 != zenon_X33) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X64)) % 3.62/3.87 (zenon_X55 != zenon_X81) % 3.62/3.87 (Tau_16 != zenon_X56) % 3.62/3.87 (Tau_15 != Tau_18) % 3.62/3.87 (Tau_11 != zenon_X53) % 3.62/3.87 (Tau_9 != zenon_X45) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X75)) % 3.62/3.87 (zenon_X28 != zenon_X86) % 3.62/3.87 (zenon_X66 != zenon_X74) % 3.62/3.87 (zenon_X77 != Tau_20) % 3.62/3.87 (-. (b48_buttercup10108 Tau_19)) % 3.62/3.87 (zenon_X26 != zenon_X80) % 3.62/3.87 (zenon_X30 != zenon_X52) % 3.62/3.87 (zenon_X30 != zenon_X57) % 3.62/3.87 (zenon_X36 != Tau_1) % 3.62/3.87 (k04_buttercup10622 zenon_X66) % 3.62/3.87 (zenon_X26 != zenon_X22) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X56)) % 3.62/3.87 (Tau_10 != Tau_1) % 3.62/3.87 (zenon_X90 != zenon_X36) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X53)) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X61)) % 3.62/3.87 (-. (b48_buttercup10109 Tau_17)) % 3.62/3.87 (zenon_X89 != zenon_X49) % 3.62/3.87 (zenon_X84 != zenon_X22) % 3.62/3.87 (Tau_8 != Tau_14) % 3.62/3.87 (zenon_X77 != Tau_10) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X55)) % 3.62/3.87 (k04_buttercup10619 zenon_X91) % 3.62/3.87 (zenon_X77 != Tau_15) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X28)) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X60)) % 3.62/3.87 (zenon_X70 != zenon_X52) % 3.62/3.87 (zenon_X54 != zenon_X70) % 3.62/3.87 (zenon_X89 != zenon_X74) % 3.62/3.87 (zenon_X46 != Tau_8) % 3.62/3.87 (zenon_X91 != zenon_X56) % 3.62/3.87 (zenon_X31 != zenon_X64) % 3.62/3.87 (zenon_X58 != zenon_X22) % 3.62/3.87 (zenon_X92 != Tau_10) % 3.62/3.87 (zenon_X85 != zenon_X22) % 3.62/3.87 (zenon_X77 != zenon_X88) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X70)) % 3.62/3.87 (zenon_X92 != zenon_X65) % 3.62/3.87 (Tau_2 != zenon_X53) % 3.62/3.87 (zenon_X68 != zenon_X35) % 3.62/3.87 (zenon_X92 != Tau_18) % 3.62/3.87 (zenon_X90 != zenon_X62) % 3.62/3.87 (zenon_X91 != zenon_X52) % 3.62/3.87 (zenon_X58 != Tau_17) % 3.62/3.87 (zenon_X61 != Tau_8) % 3.62/3.87 (zenon_X70 != Tau_16) % 3.62/3.87 (zenon_X63 != zenon_X86) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X60)) % 3.62/3.87 (zenon_X90 != zenon_X64) % 3.62/3.87 (zenon_X48 != zenon_X86) % 3.62/3.87 (zenon_X78 != zenon_X35) % 3.62/3.87 (zenon_X82 != zenon_X55) % 3.62/3.87 (Tau_14 != zenon_X91) % 3.62/3.87 (zenon_X77 != zenon_X62) % 3.62/3.87 (zenon_X59 != zenon_X50) % 3.62/3.87 (zenon_X60 != zenon_X83) % 3.62/3.87 (k04_buttercup10619 zenon_X79) % 3.62/3.87 (zenon_X49 != zenon_X85) % 3.62/3.87 (zenon_X23 != Tau_8) % 3.62/3.87 (zenon_X89 != zenon_X46) % 3.62/3.87 (zenon_X78 != zenon_X69) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X31)) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X35)) % 3.62/3.87 (Tau_4 != zenon_X80) % 3.62/3.87 (zenon_X21 != zenon_X86) % 3.62/3.87 (k04_buttercup10619 zenon_X73) % 3.62/3.87 (Tau_14 != zenon_X68) % 3.62/3.87 (zenon_X24 != Tau_15) % 3.62/3.87 (Tau_5 != Tau_17) % 3.62/3.87 (-. (k04_buttercup10622 zenon_X46)) % 3.62/3.87 (zenon_X26 != zenon_X83) % 3.62/3.87 (Tau_3 != zenon_X24) % 3.62/3.87 (Tau_5 != zenon_X27) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X85)) % 3.62/3.87 (Tau_1 != zenon_X55) % 3.62/3.87 (k04_buttercup10622 zenon_X76) % 3.62/3.87 (Tau_7 != zenon_X80) % 3.62/3.87 (Tau_3 != zenon_X79) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X26)) % 3.62/3.87 (Tau_14 != zenon_X62) % 3.62/3.87 (zenon_X78 != zenon_X79) % 3.62/3.87 (zenon_X60 != zenon_X90) % 3.62/3.87 (Tau_8 != zenon_X80) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X67)) % 3.62/3.87 (zenon_X82 != zenon_X62) % 3.62/3.87 (zenon_X59 != zenon_X27) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X33)) % 3.62/3.87 (zenon_X36 != zenon_X50) % 3.62/3.87 (zenon_X71 != zenon_X50) % 3.62/3.87 (zenon_X60 != Tau_19) % 3.62/3.87 (Tau_5 != Tau_13) % 3.62/3.87 (zenon_X81 != zenon_X80) % 3.62/3.87 (b48_buttercup10110 Tau_3) % 3.62/3.87 (b48_buttercup10102 zenon_X80) % 3.62/3.87 (zenon_X70 != zenon_X85) % 3.62/3.87 (Tau_17 != zenon_X21) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X85)) % 3.62/3.87 (zenon_X58 != zenon_X85) % 3.62/3.87 (zenon_X30 != zenon_X85) % 3.62/3.87 (zenon_X82 != Tau_0) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X58)) % 3.62/3.87 (zenon_X72 != zenon_X23) % 3.62/3.87 (zenon_X60 != Tau_18) % 3.62/3.87 (zenon_X83 != zenon_X76) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X62)) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X63)) % 3.62/3.87 (Tau_16 != zenon_X62) % 3.62/3.87 (Tau_6 != zenon_X74) % 3.62/3.87 (zenon_X35 != zenon_X58) % 3.62/3.87 (Tau_20 != Tau_0) % 3.62/3.87 (Tau_6 != zenon_X58) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X57)) % 3.62/3.87 (zenon_X24 != zenon_X68) % 3.62/3.87 (zenon_X66 != zenon_X36) % 3.62/3.87 (Tau_6 != zenon_X88) % 3.62/3.87 (zenon_X51 != Tau_15) % 3.62/3.87 (Tau_19 != zenon_X83) % 3.62/3.87 (-. (b48_buttercup10102 Tau_20)) % 3.62/3.87 (zenon_X66 != Tau_10) % 3.62/3.87 (zenon_X82 != zenon_X27) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X28)) % 3.62/3.87 (zenon_X21 != zenon_X84) % 3.62/3.87 (zenon_X68 != Tau_19) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X79)) % 3.62/3.87 (zenon_X36 != Tau_15) % 3.62/3.87 (zenon_X82 != zenon_X22) % 3.62/3.87 (Tau_19 != zenon_X81) % 3.62/3.87 (Tau_3 != Tau_18) % 3.62/3.87 (zenon_X26 != zenon_X27) % 3.62/3.87 (Tau_13 != Tau_1) % 3.62/3.87 (zenon_X51 != zenon_X71) % 3.62/3.87 (b48_buttercup10108 zenon_X59) % 3.62/3.87 (Tau_16 != zenon_X80) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X90)) % 3.62/3.87 (zenon_X58 != zenon_X47) % 3.62/3.87 (zenon_X25 != Tau_16) % 3.62/3.87 (k04_buttercup10619 zenon_X68) % 3.62/3.87 (k04_buttercup10619 zenon_X57) % 3.62/3.87 (zenon_X51 != Tau_0) % 3.62/3.87 (zenon_X57 != zenon_X49) % 3.62/3.87 (Tau_18 != Tau_20) % 3.62/3.87 (-. (k04_buttercup10619 zenon_X90)) % 3.62/3.87 (zenon_X64 != zenon_X75) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X22)) % 3.62/3.87 (zenon_X31 != zenon_X71) % 3.62/3.87 (zenon_X85 != Tau_0) % 3.62/3.87 (Tau_19 != zenon_X67) % 3.62/3.87 (zenon_X23 != zenon_X46) % 3.62/3.87 (zenon_X37 != zenon_X63) % 3.62/3.87 (k04_buttercup10622 zenon_X31) % 3.62/3.87 (zenon_X28 != zenon_X75) % 3.62/3.87 (zenon_X72 != zenon_X50) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X24)) % 3.62/3.87 (zenon_X32 != zenon_X65) % 3.62/3.87 (k04_buttercup10622 Tau_6) % 3.62/3.87 (Tau_11 != zenon_X24) % 3.62/3.87 (zenon_X73 != zenon_X22) % 3.62/3.87 (b48_buttercup10109 Tau_1) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X25)) % 3.62/3.87 (zenon_X64 != zenon_X69) % 3.62/3.87 (zenon_X48 != zenon_X88) % 3.62/3.87 (zenon_X90 != Tau_0) % 3.62/3.87 (zenon_X77 != Tau_2) % 3.62/3.87 (zenon_X33 != Tau_15) % 3.62/3.87 (zenon_X88 != zenon_X35) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X70)) % 3.62/3.87 (zenon_X33 != Tau_0) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X81)) % 3.62/3.87 (Tau_4 != Tau_13) % 3.62/3.87 (zenon_X80 != Tau_17) % 3.62/3.87 (Tau_1 != zenon_X73) % 3.62/3.87 (zenon_X83 != Tau_17) % 3.62/3.87 (Tau_8 != zenon_X50) % 3.62/3.87 (Tau_6 != Tau_16) % 3.62/3.87 (zenon_X30 != zenon_X79) % 3.62/3.87 (zenon_X65 != zenon_X22) % 3.62/3.87 (zenon_X60 != zenon_X77) % 3.62/3.87 (zenon_X72 != Tau_4) % 3.62/3.87 (zenon_X54 != zenon_X59) % 3.62/3.87 (Tau_19 != zenon_X70) % 3.62/3.87 (Tau_11 != zenon_X65) % 3.62/3.87 (zenon_X35 != zenon_X28) % 3.62/3.87 (zenon_X60 != zenon_X82) % 3.62/3.87 (zenon_X63 != zenon_X92) % 3.62/3.87 (zenon_X54 != zenon_X65) % 3.62/3.87 (zenon_X37 != zenon_X76) % 3.62/3.87 (zenon_X48 != zenon_X22) % 3.62/3.87 (zenon_X37 != zenon_X61) % 3.62/3.87 (zenon_X84 != zenon_X50) % 3.62/3.87 (zenon_X52 != zenon_X68) % 3.62/3.87 (zenon_X85 != zenon_X81) % 3.62/3.87 (zenon_X88 != zenon_X86) % 3.62/3.87 (zenon_X25 != zenon_X80) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X69)) % 3.62/3.87 (zenon_X76 != Tau_0) % 3.62/3.87 (zenon_X86 != zenon_X35) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X80)) % 3.62/3.87 (Tau_11 != zenon_X64) % 3.62/3.87 (zenon_X36 != zenon_X49) % 3.62/3.87 (zenon_X53 != Tau_10) % 3.62/3.87 (Tau_20 != zenon_X47) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X75)) % 3.62/3.87 (zenon_X59 != zenon_X71) % 3.62/3.87 (zenon_X35 != zenon_X56) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X82)) % 3.62/3.87 (b48_buttercup10110 zenon_X32) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X75)) % 3.62/3.87 (Tau_14 != Tau_1) % 3.62/3.87 (zenon_X31 != Tau_19) % 3.62/3.87 (zenon_X31 != Tau_17) % 3.62/3.87 (zenon_X33 != zenon_X66) % 3.62/3.87 (zenon_X73 != zenon_X69) % 3.62/3.87 (k04_buttercup10622 Tau_18) % 3.62/3.87 (zenon_X26 != zenon_X61) % 3.62/3.87 (zenon_X28 != zenon_X85) % 3.62/3.87 (zenon_X33 != Tau_16) % 3.62/3.87 (-. (b48_buttercup10109 Tau_7)) % 3.62/3.87 (zenon_X82 != zenon_X92) % 3.62/3.87 (zenon_X80 != zenon_X73) % 3.62/3.87 (Tau_6 != zenon_X73) % 3.62/3.87 (zenon_X70 != zenon_X64) % 3.62/3.87 (zenon_X23 != zenon_X73) % 3.62/3.87 (zenon_X63 != zenon_X46) % 3.62/3.87 (Tau_11 != Tau_8) % 3.62/3.87 (Tau_2 != zenon_X55) % 3.62/3.87 (zenon_X57 != zenon_X68) % 3.62/3.87 (zenon_X62 != zenon_X79) % 3.62/3.87 (zenon_X77 != zenon_X50) % 3.62/3.87 (zenon_X26 != Tau_10) % 3.62/3.87 (Tau_2 != zenon_X81) % 3.62/3.87 (zenon_X31 != zenon_X87) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X71)) % 3.62/3.87 (zenon_X53 != zenon_X68) % 3.62/3.87 (zenon_X33 != zenon_X81) % 3.62/3.87 (zenon_X89 != zenon_X75) % 3.62/3.87 (zenon_X74 != zenon_X68) % 3.62/3.87 (zenon_X84 != zenon_X79) % 3.62/3.87 (Tau_7 != zenon_X47) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X51)) % 3.62/3.87 (zenon_X66 != zenon_X91) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X86)) % 3.62/3.87 (zenon_X83 != Tau_15) % 3.62/3.87 (zenon_X31 != Tau_13) % 3.62/3.87 (zenon_X21 != zenon_X74) % 3.62/3.87 (zenon_X72 != zenon_X45) % 3.62/3.87 (zenon_X90 != zenon_X83) % 3.62/3.87 (Tau_1 != zenon_X83) % 3.62/3.87 (Tau_17 != zenon_X75) % 3.62/3.87 (Tau_11 != zenon_X45) % 3.62/3.87 (zenon_X86 != zenon_X92) % 3.62/3.87 (b48_buttercup10098 zenon_X43) % 3.62/3.87 (Tau_4 != zenon_X45) % 3.62/3.87 (k04_buttercup10622 zenon_X30) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X89)) % 3.62/3.87 (zenon_X89 != zenon_X87) % 3.62/3.87 (zenon_X59 != zenon_X82) % 3.62/3.87 (-. (b48_buttercup10110 Tau_4)) % 3.62/3.87 (zenon_X57 != zenon_X27) % 3.62/3.87 (Tau_5 != zenon_X82) % 3.62/3.87 (zenon_X84 != zenon_X83) % 3.62/3.87 (zenon_X78 != zenon_X56) % 3.62/3.87 (zenon_X65 != zenon_X76) % 3.62/3.87 (zenon_X89 != zenon_X85) % 3.62/3.87 (zenon_X32 != zenon_X64) % 3.62/3.87 (zenon_X23 != zenon_X90) % 3.62/3.87 (zenon_X63 != zenon_X85) % 3.62/3.87 (-. (b48_buttercup10107 Tau_20)) % 3.62/3.87 (Tau_17 != Tau_13) % 3.62/3.87 (zenon_X35 != zenon_X83) % 3.62/3.87 (zenon_X84 != Tau_8) % 3.62/3.87 (zenon_X65 != zenon_X88) % 3.62/3.87 (zenon_X58 != zenon_X56) % 3.62/3.87 (zenon_X30 != zenon_X50) % 3.62/3.87 (k04_buttercup10100 Tau_2) % 3.62/3.87 (zenon_X24 != zenon_X49) % 3.62/3.87 (zenon_X76 != Tau_10) % 3.62/3.87 (zenon_X66 != Tau_20) % 3.62/3.87 (zenon_X57 != zenon_X21) % 3.62/3.87 (-. (b48_buttercup10102 Tau_14)) % 3.62/3.87 (zenon_X58 != zenon_X76) % 3.62/3.87 (Tau_11 != zenon_X47) % 3.62/3.87 (zenon_X65 != zenon_X56) % 3.62/3.87 (-. (b48_buttercup10107 Tau_2)) % 3.62/3.87 (zenon_X71 != zenon_X30) % 3.62/3.87 (zenon_X92 != zenon_X35) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X92)) % 3.62/3.87 (b48_buttercup10109 zenon_X90) % 3.62/3.87 (Tau_16 != zenon_X74) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X48)) % 3.62/3.87 (zenon_X81 != zenon_X37) % 3.62/3.87 (-. (k04_buttercup10622 Tau_2)) % 3.62/3.87 (zenon_X66 != zenon_X82) % 3.62/3.87 (zenon_X53 != zenon_X45) % 3.62/3.87 (zenon_X79 != Tau_1) % 3.62/3.87 (zenon_X26 != zenon_X23) % 3.62/3.87 (b48_buttercup10108 Tau_4) % 3.62/3.87 (Tau_6 != zenon_X27) % 3.62/3.87 (Tau_15 != Tau_17) % 3.62/3.87 (zenon_X51 != Tau_13) % 3.62/3.87 (k04_buttercup10619 zenon_X65) % 3.62/3.87 (zenon_X90 != Tau_4) % 3.62/3.87 (Tau_7 != zenon_X75) % 3.62/3.87 (zenon_X37 != zenon_X57) % 3.62/3.87 (zenon_X28 != zenon_X24) % 3.62/3.87 (zenon_X85 != zenon_X69) % 3.62/3.87 (zenon_X92 != Tau_15) % 3.62/3.87 (zenon_X82 != zenon_X61) % 3.62/3.87 (zenon_X45 != zenon_X81) % 3.62/3.87 (-. (b48_buttercup10107 Tau_0)) % 3.62/3.87 (zenon_X90 != zenon_X74) % 3.62/3.87 (k04_buttercup10622 zenon_X69) % 3.62/3.87 (zenon_X66 != Tau_19) % 3.62/3.87 (zenon_X72 != zenon_X65) % 3.62/3.87 (zenon_X45 != Tau_0) % 3.62/3.87 (Tau_20 != zenon_X80) % 3.62/3.87 (zenon_X48 != zenon_X67) % 3.62/3.87 (Tau_8 != zenon_X57) % 3.62/3.87 (b48_buttercup10110 zenon_X60) % 3.62/3.87 (Tau_5 != zenon_X70) % 3.62/3.87 (zenon_X88 != zenon_X47) % 3.62/3.87 (zenon_X46 != Tau_20) % 3.62/3.87 (zenon_X91 != zenon_X35) % 3.62/3.87 (zenon_X48 != zenon_X65) % 3.62/3.87 (zenon_X60 != zenon_X64) % 3.62/3.87 (-. (b48_buttercup10102 Tau_18)) % 3.62/3.87 (zenon_X55 != Tau_0) % 3.62/3.87 (zenon_X84 != zenon_X89) % 3.62/3.87 (zenon_X26 != Tau_18) % 3.62/3.87 (zenon_X49 != zenon_X46) % 3.62/3.87 (zenon_X83 != zenon_X86) % 3.62/3.87 (Tau_1 != zenon_X89) % 3.62/3.87 (Tau_19 != zenon_X47) % 3.62/3.87 (zenon_X92 != Tau_14) % 3.62/3.87 (zenon_X23 != Tau_20) % 3.62/3.87 (zenon_X90 != zenon_X21) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X23)) % 3.62/3.87 (zenon_X91 != Tau_20) % 3.62/3.87 (zenon_X30 != zenon_X67) % 3.62/3.87 (Tau_11 != zenon_X80) % 3.62/3.87 (-. (k04_buttercup10622 Tau_17)) % 3.62/3.87 (zenon_X84 != zenon_X27) % 3.62/3.87 (zenon_X84 != Tau_4) % 3.62/3.87 (k04_buttercup10622 Tau_14) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X77)) % 3.62/3.87 (zenon_X53 != zenon_X85) % 3.62/3.87 (-. (b48_buttercup10110 Tau_15)) % 3.62/3.87 (zenon_X77 != zenon_X79) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X92)) % 3.62/3.87 (zenon_X78 != zenon_X58) % 3.62/3.87 (zenon_X77 != Tau_16) % 3.62/3.87 (zenon_X84 != zenon_X52) % 3.62/3.87 (k04_buttercup10619 zenon_X51) % 3.62/3.87 (Tau_10 != zenon_X21) % 3.62/3.87 (zenon_X65 != Tau_0) % 3.62/3.87 (zenon_X59 != zenon_X62) % 3.62/3.87 (Tau_4 != Tau_8) % 3.62/3.87 (zenon_X28 != Tau_8) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X36)) % 3.62/3.87 (zenon_X24 != zenon_X50) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X79)) % 3.62/3.87 (zenon_X68 != zenon_X47) % 3.62/3.87 (Tau_13 != Tau_14) % 3.62/3.87 (zenon_X84 != zenon_X76) % 3.62/3.87 (Tau_3 != Tau_2) % 3.62/3.87 (-. (k04_buttercup10619 zenon_X22)) % 3.62/3.87 (zenon_X84 != zenon_X90) % 3.62/3.87 (Tau_8 != zenon_X74) % 3.62/3.87 (zenon_X83 != zenon_X64) % 3.62/3.87 (Tau_4 != zenon_X69) % 3.62/3.87 (zenon_X37 != zenon_X87) % 3.62/3.87 (zenon_X70 != zenon_X88) % 3.62/3.87 (zenon_X67 != zenon_X55) % 3.62/3.87 (zenon_X23 != zenon_X88) % 3.62/3.87 (zenon_X51 != Tau_2) % 3.62/3.87 (zenon_X81 != zenon_X84) % 3.62/3.87 (Tau_18 != zenon_X22) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X83)) % 3.62/3.87 (zenon_X65 != Tau_20) % 3.62/3.87 (zenon_X60 != zenon_X80) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X88)) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X51)) % 3.62/3.87 (zenon_X60 != Tau_20) % 3.62/3.87 (zenon_X53 != zenon_X55) % 3.62/3.87 (zenon_X26 != Tau_2) % 3.62/3.87 (k04_buttercup10100 zenon_X92) % 3.62/3.87 (zenon_X81 != Tau_7) % 3.62/3.87 (zenon_X31 != zenon_X27) % 3.62/3.87 (zenon_X46 != Tau_0) % 3.62/3.87 (zenon_X71 != zenon_X46) % 3.62/3.87 (zenon_X92 != Tau_17) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X83)) % 3.62/3.87 (b48_buttercup10110 Tau_14) % 3.62/3.87 (-. (k04_buttercup10100 Tau_9)) % 3.62/3.87 (Tau_8 != zenon_X62) % 3.62/3.87 (zenon_X90 != zenon_X80) % 3.62/3.87 (Tau_7 != zenon_X53) % 3.62/3.87 (zenon_X63 != zenon_X73) % 3.62/3.87 (zenon_X25 != zenon_X81) % 3.62/3.87 (zenon_X65 != zenon_X68) % 3.62/3.87 (zenon_X58 != zenon_X86) % 3.62/3.87 (k04_buttercup10622 zenon_X23) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X86)) % 3.62/3.87 (zenon_X23 != zenon_X50) % 3.62/3.87 (zenon_X37 != zenon_X74) % 3.62/3.87 (-. (b48_buttercup10104 Tau_13)) % 3.62/3.87 (zenon_X88 != zenon_X62) % 3.62/3.87 (zenon_X53 != zenon_X86) % 3.62/3.87 (zenon_X71 != zenon_X52) % 3.62/3.87 (zenon_X28 != Tau_10) % 3.62/3.87 (Tau_6 != zenon_X71) % 3.62/3.87 (zenon_X62 != zenon_X22) % 3.62/3.87 (zenon_X57 != zenon_X85) % 3.62/3.87 (zenon_X25 != zenon_X27) % 3.62/3.87 (zenon_X84 != zenon_X86) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X77)) % 3.62/3.87 (k04_buttercup10622 zenon_X62) % 3.62/3.87 (zenon_X72 != zenon_X57) % 3.62/3.87 (zenon_X68 != zenon_X50) % 3.62/3.87 (zenon_X35 != zenon_X73) % 3.62/3.87 (zenon_X89 != zenon_X81) % 3.62/3.87 (zenon_X35 != Tau_3) % 3.62/3.87 (-. (k04_buttercup10622 Tau_13)) % 3.62/3.87 (zenon_X32 != zenon_X79) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X61)) % 3.62/3.87 (Tau_14 != zenon_X64) % 3.62/3.87 (-. (b48_buttercup10107 Tau_1)) % 3.62/3.87 (zenon_X60 != zenon_X79) % 3.62/3.87 (zenon_X21 != zenon_X55) % 3.62/3.87 (zenon_X90 != Tau_18) % 3.62/3.87 (zenon_X72 != Tau_20) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X76)) % 3.62/3.87 (-. (b48_buttercup10104 Tau_19)) % 3.62/3.87 (zenon_X92 != zenon_X64) % 3.62/3.87 (zenon_X78 != zenon_X83) % 3.62/3.87 (k04_buttercup10619 zenon_X77) % 3.62/3.87 (zenon_X74 != zenon_X75) % 3.62/3.87 (zenon_X46 != zenon_X87) % 3.62/3.87 (zenon_X92 != Tau_11) % 3.62/3.87 (zenon_X60 != zenon_X49) % 3.62/3.87 (zenon_X24 != Tau_0) % 3.62/3.87 (k04_buttercup10619 Tau_16) % 3.62/3.87 (Tau_11 != zenon_X25) % 3.62/3.87 (zenon_X32 != zenon_X25) % 3.62/3.87 (zenon_X59 != zenon_X49) % 3.62/3.87 (zenon_X46 != Tau_15) % 3.62/3.87 (Tau_6 != zenon_X47) % 3.62/3.87 (zenon_X71 != Tau_18) % 3.62/3.87 (zenon_X28 != zenon_X52) % 3.62/3.87 (zenon_X37 != Tau_4) % 3.62/3.87 (Tau_3 != zenon_X82) % 3.62/3.87 (Tau_5 != zenon_X80) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X72)) % 3.62/3.87 (zenon_X61 != zenon_X56) % 3.62/3.87 (Tau_6 != zenon_X45) % 3.62/3.87 (zenon_X30 != zenon_X36) % 3.62/3.87 (k04_buttercup10619 zenon_X80) % 3.62/3.87 (zenon_X26 != zenon_X36) % 3.62/3.87 (zenon_X32 != zenon_X53) % 3.62/3.87 (Tau_14 != zenon_X57) % 3.62/3.87 (Tau_18 != zenon_X45) % 3.62/3.87 (zenon_X48 != zenon_X47) % 3.62/3.87 (zenon_X89 != zenon_X62) % 3.62/3.87 (zenon_X28 != zenon_X87) % 3.62/3.87 (zenon_X77 != zenon_X46) % 3.62/3.87 (Tau_8 != zenon_X75) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X76)) % 3.62/3.87 (Tau_14 != zenon_X52) % 3.62/3.87 (zenon_X33 != zenon_X75) % 3.62/3.87 (zenon_X66 != zenon_X85) % 3.62/3.87 (zenon_X59 != zenon_X56) % 3.62/3.87 (Tau_6 != zenon_X22) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X67)) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X24)) % 3.62/3.87 (zenon_X66 != zenon_X73) % 3.62/3.87 (-. (k04_buttercup10622 zenon_X61)) % 3.62/3.87 (-. (k04_buttercup10100 Tau_17)) % 3.62/3.87 (k04_buttercup10622 zenon_X89) % 3.62/3.87 (zenon_X88 != Tau_8) % 3.62/3.87 (zenon_X72 != zenon_X59) % 3.62/3.87 (Tau_9 != zenon_X83) % 3.62/3.87 (Tau_9 != zenon_X52) % 3.62/3.87 (Tau_15 != Tau_10) % 3.62/3.87 (zenon_X84 != zenon_X67) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X54)) % 3.62/3.87 (b48_buttercup10104 Tau_16) % 3.62/3.87 (Tau_7 != zenon_X24) % 3.62/3.87 (Tau_5 != zenon_X22) % 3.62/3.87 (k04_buttercup10619 zenon_X83) % 3.62/3.87 (zenon_X76 != Tau_2) % 3.62/3.87 (zenon_X76 != zenon_X33) % 3.62/3.87 (zenon_X88 != Tau_0) % 3.62/3.87 (zenon_X58 != zenon_X68) % 3.62/3.87 (zenon_X74 != Tau_10) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X80)) % 3.62/3.87 (zenon_X64 != zenon_X46) % 3.62/3.87 (zenon_X65 != zenon_X51) % 3.62/3.87 (zenon_X82 != Tau_19) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X56)) % 3.62/3.87 (zenon_X31 != Tau_16) % 3.62/3.87 (zenon_X81 != zenon_X47) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X54)) % 3.62/3.87 (Tau_13 != zenon_X84) % 3.62/3.87 (Tau_2 != zenon_X64) % 3.62/3.87 (Tau_1 != zenon_X27) % 3.62/3.87 (zenon_X58 != zenon_X73) % 3.62/3.87 (Tau_14 != zenon_X75) % 3.62/3.87 (zenon_X85 != zenon_X55) % 3.62/3.87 (zenon_X73 != Tau_0) % 3.62/3.87 (zenon_X37 != zenon_X47) % 3.62/3.87 (Tau_19 != zenon_X55) % 3.62/3.87 (zenon_X54 != zenon_X50) % 3.62/3.87 (zenon_X83 != Tau_16) % 3.62/3.87 (k04_buttercup10619 zenon_X23) % 3.62/3.87 (zenon_X83 != zenon_X85) % 3.62/3.87 (-. (k04_buttercup10619 zenon_X50)) % 3.62/3.87 (Tau_9 != zenon_X56) % 3.62/3.87 (zenon_X24 != zenon_X45) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X53)) % 3.62/3.87 (zenon_X32 != zenon_X86) % 3.62/3.87 (zenon_X60 != zenon_X47) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X51)) % 3.62/3.87 (k04_buttercup10619 zenon_X37) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X63)) % 3.62/3.87 (zenon_X59 != zenon_X33) % 3.62/3.87 (zenon_X59 != zenon_X68) % 3.62/3.87 (Tau_8 != zenon_X81) % 3.62/3.87 (zenon_X25 != zenon_X57) % 3.62/3.87 (zenon_X30 != zenon_X25) % 3.62/3.87 (zenon_X92 != zenon_X32) % 3.62/3.87 (zenon_X33 != zenon_X73) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X58)) % 3.62/3.87 (zenon_X90 != zenon_X46) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X30)) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X91)) % 3.62/3.87 (Tau_3 != zenon_X57) % 3.62/3.87 (zenon_X85 != zenon_X21) % 3.62/3.87 (zenon_X30 != Tau_17) % 3.62/3.87 (zenon_X46 != Tau_6) % 3.62/3.87 (zenon_X92 != zenon_X74) % 3.62/3.87 (zenon_X82 != zenon_X75) % 3.62/3.87 (Tau_13 != zenon_X71) % 3.62/3.87 (zenon_X37 != zenon_X75) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X33)) % 3.62/3.87 (zenon_X86 != zenon_X33) % 3.62/3.87 (zenon_X66 != zenon_X23) % 3.62/3.87 (zenon_X90 != zenon_X73) % 3.62/3.87 (Tau_5 != Tau_10) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X50)) % 3.62/3.87 (zenon_X83 != zenon_X21) % 3.62/3.87 (zenon_X73 != zenon_X87) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X45)) % 3.62/3.87 (zenon_X66 != Tau_15) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X53)) % 3.62/3.87 (zenon_X78 != zenon_X23) % 3.62/3.87 (zenon_X72 != zenon_X46) % 3.62/3.87 (zenon_X48 != zenon_X24) % 3.62/3.87 (zenon_X54 != Tau_0) % 3.62/3.87 (Tau_6 != zenon_X61) % 3.62/3.87 (zenon_X78 != zenon_X77) % 3.62/3.87 (zenon_X69 != zenon_X22) % 3.62/3.87 (Tau_14 != zenon_X79) % 3.62/3.87 (Tau_14 != zenon_X24) % 3.62/3.87 (zenon_X72 != zenon_X68) % 3.62/3.87 (b48_buttercup10109 zenon_X35) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X88)) % 3.62/3.87 (zenon_X83 != zenon_X81) % 3.62/3.87 (zenon_X37 != Tau_17) % 3.62/3.87 (zenon_X68 != zenon_X87) % 3.62/3.87 (Tau_5 != zenon_X24) % 3.62/3.87 (Tau_17 != Tau_19) % 3.62/3.87 (zenon_X35 != Tau_14) % 3.62/3.87 (Tau_2 != zenon_X89) % 3.62/3.87 (-. (k04_buttercup10619 zenon_X81)) % 3.62/3.87 (-. (b48_buttercup10108 Tau_8)) % 3.62/3.87 (zenon_X59 != zenon_X79) % 3.62/3.87 (zenon_X65 != zenon_X35) % 3.62/3.87 (zenon_X70 != Tau_17) % 3.62/3.87 (Tau_15 != Tau_14) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X35)) % 3.62/3.87 (Tau_9 != zenon_X73) % 3.62/3.87 (zenon_X53 != zenon_X21) % 3.62/3.87 (-. (k04_buttercup10622 Tau_1)) % 3.62/3.87 (Tau_6 != Tau_4) % 3.62/3.87 (-. (k04_buttercup10622 zenon_X81)) % 3.62/3.87 (b48_buttercup10102 zenon_X62) % 3.62/3.87 (Tau_7 != Tau_8) % 3.62/3.87 (zenon_X25 != zenon_X88) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X53)) % 3.62/3.87 (zenon_X57 != zenon_X69) % 3.62/3.87 (zenon_X54 != zenon_X49) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X72)) % 3.62/3.87 (zenon_X65 != Tau_2) % 3.62/3.87 (zenon_X82 != zenon_X35) % 3.62/3.87 (Tau_2 != zenon_X49) % 3.62/3.87 (zenon_X92 != zenon_X78) % 3.62/3.87 (zenon_X36 != Tau_19) % 3.62/3.87 (Tau_17 != zenon_X67) % 3.62/3.87 (Tau_8 != Tau_10) % 3.62/3.87 (zenon_X63 != zenon_X74) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X46)) % 3.62/3.87 (k04_buttercup10622 zenon_X55) % 3.62/3.87 (zenon_X89 != zenon_X21) % 3.62/3.87 (zenon_X54 != zenon_X75) % 3.62/3.87 (Tau_5 != zenon_X69) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X59)) % 3.62/3.87 (-. (b48_buttercup10110 Tau_10)) % 3.62/3.87 (Tau_13 != zenon_X54) % 3.62/3.87 (k04_buttercup10100 zenon_X56) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X21)) % 3.62/3.87 (zenon_X92 != zenon_X28) % 3.62/3.87 (zenon_X57 != zenon_X46) % 3.62/3.87 (zenon_X89 != zenon_X79) % 3.62/3.87 (Tau_2 != Tau_18) % 3.62/3.87 (zenon_X26 != zenon_X73) % 3.62/3.87 (b48_buttercup10110 zenon_X72) % 3.62/3.87 (zenon_X52 != zenon_X80) % 3.62/3.87 (zenon_X87 != zenon_X27) % 3.62/3.87 (-. (b48_buttercup10108 Tau_10)) % 3.62/3.87 (k04_buttercup10619 Tau_10) % 3.62/3.87 (zenon_X51 != zenon_X76) % 3.62/3.87 (zenon_X48 != zenon_X46) % 3.62/3.87 (zenon_X63 != zenon_X56) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X73)) % 3.62/3.87 (zenon_X53 != zenon_X67) % 3.62/3.87 (zenon_X78 != zenon_X27) % 3.62/3.87 (zenon_X36 != zenon_X69) % 3.62/3.87 (zenon_X64 != Tau_15) % 3.62/3.87 (zenon_X26 != zenon_X89) % 3.62/3.87 (zenon_X23 != Tau_0) % 3.62/3.87 (zenon_X66 != zenon_X88) % 3.62/3.87 (zenon_X21 != zenon_X27) % 3.62/3.87 (Tau_5 != zenon_X63) % 3.62/3.87 (zenon_X33 != zenon_X36) % 3.62/3.87 (zenon_X59 != Tau_2) % 3.62/3.87 (zenon_X72 != zenon_X67) % 3.62/3.87 (Tau_13 != zenon_X90) % 3.62/3.87 (zenon_X52 != zenon_X69) % 3.62/3.87 (zenon_X30 != zenon_X69) % 3.62/3.87 (zenon_X78 != zenon_X86) % 3.62/3.87 (zenon_X25 != Tau_10) % 3.62/3.87 (Tau_4 != zenon_X57) % 3.62/3.87 (Tau_5 != zenon_X59) % 3.62/3.87 (zenon_X66 != zenon_X62) % 3.62/3.87 (zenon_X57 != zenon_X45) % 3.62/3.87 (zenon_X26 != zenon_X25) % 3.62/3.87 (Tau_4 != zenon_X21) % 3.62/3.87 (Tau_6 != zenon_X56) % 3.62/3.87 (zenon_X26 != Tau_16) % 3.62/3.87 (Tau_0 != zenon_X53) % 3.62/3.87 (k04_buttercup10622 zenon_X36) % 3.62/3.87 (zenon_X26 != zenon_X85) % 3.62/3.87 (zenon_X30 != zenon_X75) % 3.62/3.87 (-. (b48_buttercup10108 Tau_7)) % 3.62/3.87 (zenon_X58 != zenon_X81) % 3.62/3.87 (-. (b48_buttercup10102 Tau_19)) % 3.62/3.87 (zenon_X35 != zenon_X69) % 3.62/3.87 (zenon_X33 != zenon_X55) % 3.62/3.87 (zenon_X62 != zenon_X67) % 3.62/3.87 (zenon_X31 != zenon_X92) % 3.62/3.87 (-. (k04_buttercup10619 Tau_0)) % 3.62/3.87 (-. (k04_buttercup10622 zenon_X79)) % 3.62/3.87 (zenon_X60 != zenon_X71) % 3.62/3.87 (zenon_X25 != Tau_17) % 3.62/3.87 (zenon_X53 != zenon_X88) % 3.62/3.87 (Tau_20 != zenon_X83) % 3.62/3.87 (-. (b48_buttercup10111 Tau_7)) % 3.62/3.87 (zenon_X60 != zenon_X86) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X25)) % 3.62/3.87 (Tau_4 != Tau_0) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X69)) % 3.62/3.87 (zenon_X32 != zenon_X63) % 3.62/3.87 (b48_buttercup10107 zenon_X85) % 3.62/3.87 (Tau_11 != zenon_X63) % 3.62/3.87 (zenon_X53 != zenon_X90) % 3.62/3.87 (zenon_X84 != zenon_X88) % 3.62/3.87 (zenon_X81 != zenon_X31) % 3.62/3.87 (zenon_X79 != Tau_8) % 3.62/3.87 (zenon_X54 != zenon_X61) % 3.62/3.87 (Tau_10 != zenon_X69) % 3.62/3.87 (k04_buttercup10619 zenon_X46) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X59)) % 3.62/3.87 (zenon_X32 != zenon_X68) % 3.62/3.87 (zenon_X54 != zenon_X45) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X58)) % 3.62/3.87 (zenon_X90 != zenon_X87) % 3.62/3.87 (zenon_X31 != Tau_10) % 3.62/3.87 (zenon_X77 != zenon_X90) % 3.62/3.87 (zenon_X52 != zenon_X33) % 3.62/3.87 (-. (b48_buttercup10109 Tau_9)) % 3.62/3.87 (Tau_18 != Tau_16) % 3.62/3.87 (zenon_X78 != zenon_X71) % 3.62/3.87 (zenon_X52 != zenon_X46) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X86)) % 3.62/3.87 (zenon_X59 != zenon_X87) % 3.62/3.87 (Tau_2 != zenon_X48) % 3.62/3.87 (zenon_X58 != zenon_X24) % 3.62/3.87 (-. (b48_buttercup10109 Tau_13)) % 3.62/3.87 (zenon_X46 != Tau_1) % 3.62/3.87 (zenon_X71 != zenon_X73) % 3.62/3.87 (k04_buttercup10622 zenon_X26) % 3.62/3.87 (Tau_16 != Tau_3) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X27)) % 3.62/3.87 (-. (b48_buttercup10110 zenon_X76)) % 3.62/3.87 (zenon_X32 != Tau_8) % 3.62/3.87 (zenon_X53 != zenon_X56) % 3.62/3.87 (Tau_8 != zenon_X58) % 3.62/3.87 (k04_buttercup10100 zenon_X35) % 3.62/3.87 (zenon_X63 != Tau_2) % 3.62/3.87 (Tau_9 != Tau_16) % 3.62/3.87 (zenon_X32 != Tau_10) % 3.62/3.87 (zenon_X70 != zenon_X81) % 3.62/3.87 (zenon_X23 != zenon_X55) % 3.62/3.87 (zenon_X27 != Tau_13) % 3.62/3.87 (zenon_X90 != Tau_15) % 3.62/3.87 (-. (b48_buttercup10110 Tau_19)) % 3.62/3.87 (zenon_X63 != Tau_17) % 3.62/3.87 (-. (b48_buttercup10104 zenon_X87)) % 3.62/3.87 (zenon_X30 != zenon_X64) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X54)) % 3.62/3.87 (Tau_14 != Tau_18) % 3.62/3.87 (zenon_X78 != zenon_X33) % 3.62/3.87 (zenon_X68 != Tau_13) % 3.62/3.87 (zenon_X47 != zenon_X67) % 3.62/3.87 (zenon_X79 != zenon_X22) % 3.62/3.87 (zenon_X30 != zenon_X23) % 3.62/3.87 (zenon_X33 != Tau_6) % 3.62/3.87 (zenon_X72 != zenon_X27) % 3.62/3.87 (zenon_X35 != zenon_X26) % 3.62/3.87 (zenon_X84 != zenon_X63) % 3.62/3.87 (zenon_X45 != zenon_X87) % 3.62/3.87 (zenon_X23 != Tau_10) % 3.62/3.87 (zenon_X26 != zenon_X69) % 3.62/3.87 (-. (b48_buttercup10108 Tau_1)) % 3.62/3.87 (zenon_X23 != zenon_X56) % 3.62/3.87 (zenon_X30 != zenon_X59) % 3.62/3.87 (k04_buttercup10622 zenon_X52) % 3.62/3.87 (zenon_X37 != zenon_X86) % 3.62/3.87 (Tau_3 != zenon_X50) % 3.62/3.87 (-. (k04_buttercup10100 Tau_18)) % 3.62/3.87 (zenon_X92 != zenon_X60) % 3.62/3.87 (Tau_15 != zenon_X75) % 3.62/3.87 (zenon_X78 != zenon_X63) % 3.62/3.87 (Tau_18 != zenon_X67) % 3.62/3.87 (zenon_X51 != zenon_X67) % 3.62/3.87 (zenon_X84 != zenon_X74) % 3.62/3.87 (-. (k04_buttercup10100 zenon_X48)) % 3.62/3.87 (zenon_X77 != zenon_X55) % 3.62/3.87 (zenon_X52 != zenon_X75) % 3.62/3.87 (zenon_X28 != zenon_X58) % 3.62/3.87 (zenon_X64 != zenon_X27) % 3.62/3.87 (zenon_X35 != zenon_X50) % 3.62/3.87 (zenon_X82 != zenon_X68) % 3.62/3.87 (zenon_X45 != zenon_X75) % 3.62/3.87 (zenon_X66 != zenon_X89) % 3.62/3.87 (-. (k04_buttercup10622 zenon_X75)) % 3.62/3.87 (zenon_X84 != Tau_15) % 3.62/3.87 (zenon_X84 != Tau_0) % 3.62/3.87 (Tau_9 != zenon_X27) % 3.62/3.87 (zenon_X23 != zenon_X57) % 3.62/3.87 (zenon_X32 != zenon_X56) % 3.62/3.87 (Tau_11 != zenon_X90) % 3.62/3.87 (zenon_X31 != zenon_X36) % 3.62/3.87 (zenon_X66 != zenon_X57) % 3.62/3.87 (-. (b48_buttercup10109 zenon_X85)) % 3.62/3.87 (zenon_X23 != zenon_X61) % 3.62/3.87 (zenon_X54 != zenon_X74) % 3.62/3.87 (zenon_X50 != zenon_X62) % 3.62/3.87 (zenon_X37 != zenon_X83) % 3.62/3.87 (zenon_X54 != zenon_X86) % 3.62/3.87 (zenon_X48 != zenon_X61) % 3.62/3.87 (-. (k04_buttercup10619 zenon_X33)) % 3.62/3.87 (Tau_3 != Tau_4) % 3.62/3.87 (Tau_15 != zenon_X85) % 3.62/3.87 (zenon_X66 != zenon_X77) % 3.62/3.87 (zenon_X92 != zenon_X46) % 3.62/3.87 (zenon_X84 != zenon_X71) % 3.62/3.87 (b48_buttercup10110 zenon_X84) % 3.62/3.87 (zenon_X46 != Tau_19) % 3.62/3.87 (zenon_X60 != Tau_4) % 3.62/3.87 (zenon_X60 != zenon_X74) % 3.62/3.87 (Tau_20 != zenon_X62) % 3.62/3.87 (zenon_X76 != zenon_X85) % 3.62/3.87 (zenon_X76 != zenon_X67) % 3.62/3.87 (-. (b48_buttercup10110 Tau_18)) % 3.62/3.87 (b48_buttercup10098 zenon_X39) % 3.62/3.87 (k04_buttercup10619 zenon_X52) % 3.62/3.87 (Tau_4 != zenon_X47) % 3.62/3.87 (zenon_X26 != zenon_X64) % 3.62/3.87 (zenon_X51 != zenon_X89) % 3.62/3.87 (zenon_X82 != zenon_X85) % 3.62/3.87 (zenon_X63 != zenon_X55) % 3.62/3.87 (zenon_X92 != Tau_5) % 3.62/3.87 (zenon_X72 != zenon_X74) % 3.62/3.87 (zenon_X64 != Tau_10) % 3.62/3.87 (zenon_X25 != zenon_X85) % 3.62/3.87 (zenon_X52 != zenon_X73) % 3.62/3.87 (-. (b48_buttercup10108 zenon_X30)) % 3.62/3.87 (zenon_X52 != Tau_13) % 3.62/3.87 (zenon_X92 != zenon_X26) % 3.62/3.87 (Tau_2 != zenon_X25) % 3.62/3.87 (zenon_X49 != zenon_X68) % 3.62/3.87 (-. (b48_buttercup10107 Tau_18)) % 3.62/3.87 (zenon_X36 != Tau_10) % 3.62/3.87 (-. (b48_buttercup10107 zenon_X90)) % 3.62/3.87 (zenon_X59 != zenon_X24) % 3.62/3.87 (zenon_X72 != zenon_X58) % 3.62/3.87 (zenon_X72 != zenon_X80) % 3.62/3.87 (zenon_X70 != zenon_X86) % 3.62/3.87 (zenon_X52 != Tau_15) % 3.62/3.87 (zenon_X36 != zenon_X22) % 3.62/3.87 (zenon_X81 != zenon_X74) % 3.62/3.87 (zenon_X53 != zenon_X75) % 3.62/3.87 (zenon_X89 != zenon_X47) % 3.62/3.87 (zenon_X25 != zenon_X24) % 3.62/3.87 (Tau_16 != zenon_X21) % 3.62/3.87 (zenon_X61 != Tau_19) % 3.62/3.87 (zenon_X51 != zenon_X22) % 3.62/3.87 (zenon_X63 != Tau_20) % 3.62/3.87 (zenon_X28 != zenon_X69) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X45)) % 3.62/3.87 (zenon_X52 != zenon_X47) % 3.62/3.87 (zenon_X59 != zenon_X80) % 3.62/3.87 (zenon_X28 != zenon_X80) % 3.62/3.87 (Tau_16 != zenon_X49) % 3.62/3.87 (zenon_X35 != zenon_X21) % 3.62/3.87 (zenon_X36 != zenon_X85) % 3.62/3.87 (zenon_X73 != zenon_X92) % 3.62/3.87 (zenon_X60 != zenon_X61) % 3.62/3.87 (Tau_11 != zenon_X68) % 3.62/3.87 (zenon_X64 != zenon_X61) % 3.62/3.87 (Tau_14 != zenon_X67) % 3.62/3.87 (Tau_5 != zenon_X71) % 3.62/3.87 (zenon_X46 != zenon_X56) % 3.62/3.87 (Tau_18 != Tau_17) % 3.62/3.87 (-. (k04_buttercup10619 Tau_8)) % 3.62/3.87 (zenon_X32 != zenon_X47) % 3.62/3.87 (k04_buttercup10622 zenon_X58) % 3.62/3.87 (Tau_4 != zenon_X52) % 3.62/3.87 (zenon_X28 != Tau_13) % 3.62/3.87 (-. (b48_buttercup10111 zenon_X55)) % 3.62/3.87 (zenon_X24 != zenon_X21) % 3.62/3.87 (-. (b48_buttercup10102 zenon_X68)) % 3.62/3.87 (zenon_X91 != zenon_X86) % 3.62/3.87 *) % 3.62/3.87 (* NO-PROOF *) % 3.62/3.87 % SZS status GaveUp % 3.62/3.87 Number of rewrites on terms: 0 % 3.62/3.87 Number of rewrites on props: 1927 % 3.62/3.87 nodes searched: 134040 % 3.62/3.87 max branch formulas: 8481 % 3.62/3.87 proof nodes created: 2974 % 3.62/3.87 formulas created: 126132 % 3.62/3.87 %------------------------------------------------------------------------------