%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : KRS033+1 : TPTP v9.0.0. Released v3.1.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n008.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 07:07:11 PM UTC 2025
% Result : Satisfiable 15.28s 4.57s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.13 % Problem : KRS033+1 : TPTP v9.0.0. Released v3.1.0.
% 0.07/0.14 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.14/0.36 % Computer : n008.cluster.edu
% 0.14/0.36 % Model : x86_64 x86_64
% 0.14/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.36 % Memory : 8042.1875MB
% 0.14/0.36 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.36 % CPULimit : 300
% 0.14/0.36 % WCLimit : 300
% 0.14/0.36 % DateTime : Tue Apr 8 02:55:02 EDT 2025
% 0.14/0.36 % CPUTime :
% 14.99/4.57
% 15.28/4.57 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.28/4.57
% 15.28/4.57 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.28/4.58 %$ rr > xsd_string > xsd_integer > cp5 > cp4 > cp3 > cp2 > cp1 > cp > cowlThing > cowlNothing > cSatisfiable > #nlpp > i2003_11_14_17_15_37698 > #skF_9 > #skF_7 > #skF_5 > #skF_2 > #skF_4 > #skF_1 > #skF_8 > #skF_10 > #skF_13 > #skF_3 > #skF_11 > #skF_12 > #skF_6
% 15.28/4.58
% 15.28/4.58 %Foreground sorts:
% 15.28/4.58
% 15.28/4.58
% 15.28/4.58 %Background operators:
% 15.28/4.58
% 15.28/4.58
% 15.28/4.58 %Foreground operators:
% 15.28/4.58 tff('#skF_9', type, '#skF_9': $i > $i).
% 15.28/4.58 tff('#skF_7', type, '#skF_7': $i > $i).
% 15.28/4.58 tff('#skF_5', type, '#skF_5': $i > $i).
% 15.28/4.58 tff(cp5, type, cp5: $i > $o).
% 15.28/4.58 tff(rr, type, rr: ($i * $i) > $o).
% 15.28/4.58 tff('#skF_2', type, '#skF_2': $i > $i).
% 15.28/4.58 tff('#skF_4', type, '#skF_4': $i > $i).
% 15.28/4.58 tff(cowlThing, type, cowlThing: $i > $o).
% 15.28/4.58 tff('#skF_1', type, '#skF_1': $i > $i).
% 15.28/4.58 tff('#skF_8', type, '#skF_8': $i > $i).
% 15.28/4.58 tff(cp4, type, cp4: $i > $o).
% 15.28/4.58 tff(xsd_integer, type, xsd_integer: $i > $o).
% 15.28/4.58 tff('#skF_10', type, '#skF_10': $i > $i).
% 15.28/4.58 tff(cSatisfiable, type, cSatisfiable: $i > $o).
% 15.28/4.58 tff(cp3, type, cp3: $i > $o).
% 15.28/4.58 tff('#skF_13', type, '#skF_13': $i > $i).
% 15.28/4.58 tff(xsd_string, type, xsd_string: $i > $o).
% 15.28/4.58 tff('#skF_3', type, '#skF_3': $i > $i).
% 15.28/4.58 tff('#skF_11', type, '#skF_11': $i > $i).
% 15.28/4.58 tff(i2003_11_14_17_15_37698, type, i2003_11_14_17_15_37698: $i).
% 15.28/4.58 tff(cp, type, cp: $i > $o).
% 15.28/4.58 tff('#skF_12', type, '#skF_12': $i > $i).
% 15.28/4.58 tff(cp2, type, cp2: $i > $o).
% 15.28/4.58 tff('#skF_6', type, '#skF_6': $i > $i).
% 15.28/4.58 tff(cowlNothing, type, cowlNothing: $i > $o).
% 15.28/4.58 tff(cp1, type, cp1: $i > $o).
% 15.28/4.58
% 15.28/4.58 %Saturated clause set:
% 15.28/4.58 tff(c_3445, plain, (![X_31]: ('#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.58 tff(c_3489, plain, (![X_31]: ('#skF_9'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.58 tff(c_5078, plain, (![X_31]: ('#skF_11'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.58 tff(c_3818, plain, (![X_31]: ('#skF_8'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.58 tff(c_5526, plain, (![X_31]: ('#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.58 tff(c_3707, plain, (![X_31]: ('#skF_7'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.58 tff(c_5447, plain, (![X_31]: ('#skF_8'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.58 tff(c_3410, plain, (![X_31]: ('#skF_10'(X_31)='#skF_13'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.58 tff(c_5592, plain, (![X_31]: ('#skF_9'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.58 tff(c_4446, plain, (![X_31]: ('#skF_10'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.58 tff(c_4746, plain, (![X_31]: ('#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.59 tff(c_5367, plain, (![X_31]: ('#skF_7'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_6'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.59 tff(c_5591, plain, (![X_31]: ('#skF_9'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.59 tff(c_3665, plain, (![X_31]: ('#skF_7'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_6'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.59 tff(c_5222, plain, (![X_31]: ('#skF_8'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.59 tff(c_5631, plain, (![X_31]: ('#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.59 tff(c_5637, plain, (![X_31]: ('#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.59 tff(c_4747, plain, (![X_31]: ('#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.59 tff(c_3891, plain, (![X_31]: ('#skF_8'(X_31)='#skF_13'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.59 tff(c_4080, plain, (![X_31]: ('#skF_13'(X_31)='#skF_12'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.59 tff(c_5519, plain, (![X_31]: ('#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.59 tff(c_3302, plain, (![X_31]: ('#skF_10'(X_31)='#skF_11'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.59 tff(c_5486, plain, (![X_31]: ('#skF_10'(X_31)='#skF_13'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.59 tff(c_9733, plain, (![Y3_69, Y2_68, Y1_67, Y0_66]: (Y3_69='#skF_11'(i2003_11_14_17_15_37698) | Y2_68='#skF_11'(i2003_11_14_17_15_37698) | Y3_69=Y2_68 | Y1_67='#skF_11'(i2003_11_14_17_15_37698) | Y3_69=Y1_67 | Y2_68=Y1_67 | Y0_66='#skF_11'(i2003_11_14_17_15_37698) | Y3_69=Y0_66 | Y2_68=Y0_66 | Y1_67=Y0_66 | ~rr(i2003_11_14_17_15_37698, Y3_69) | ~rr(i2003_11_14_17_15_37698, Y2_68) | ~rr(i2003_11_14_17_15_37698, Y1_67) | ~rr(i2003_11_14_17_15_37698, Y0_66)))).
% 15.28/4.59 tff(c_8443, plain, (![Y3_69, Y2_68, Y1_67, Y0_66]: (Y3_69='#skF_13'(i2003_11_14_17_15_37698) | Y2_68='#skF_13'(i2003_11_14_17_15_37698) | Y3_69=Y2_68 | Y1_67='#skF_13'(i2003_11_14_17_15_37698) | Y3_69=Y1_67 | Y2_68=Y1_67 | Y0_66='#skF_13'(i2003_11_14_17_15_37698) | Y3_69=Y0_66 | Y2_68=Y0_66 | Y1_67=Y0_66 | ~rr(i2003_11_14_17_15_37698, Y3_69) | ~rr(i2003_11_14_17_15_37698, Y2_68) | ~rr(i2003_11_14_17_15_37698, Y1_67) | ~rr(i2003_11_14_17_15_37698, Y0_66)))).
% 15.28/4.59 tff(c_11013, plain, (![Y3_69, Y2_68, Y1_67, Y0_66]: (Y3_69='#skF_6'(i2003_11_14_17_15_37698) | Y2_68='#skF_6'(i2003_11_14_17_15_37698) | Y3_69=Y2_68 | Y1_67='#skF_6'(i2003_11_14_17_15_37698) | Y3_69=Y1_67 | Y2_68=Y1_67 | Y0_66='#skF_6'(i2003_11_14_17_15_37698) | Y3_69=Y0_66 | Y2_68=Y0_66 | Y1_67=Y0_66 | ~rr(i2003_11_14_17_15_37698, Y3_69) | ~rr(i2003_11_14_17_15_37698, Y2_68) | ~rr(i2003_11_14_17_15_37698, Y1_67) | ~rr(i2003_11_14_17_15_37698, Y0_66)))).
% 15.28/4.59 tff(c_7031, plain, (![Y3_69, Y2_68, Y1_67, Y0_66]: (Y3_69='#skF_12'(i2003_11_14_17_15_37698) | Y2_68='#skF_12'(i2003_11_14_17_15_37698) | Y3_69=Y2_68 | Y1_67='#skF_12'(i2003_11_14_17_15_37698) | Y3_69=Y1_67 | Y2_68=Y1_67 | Y0_66='#skF_12'(i2003_11_14_17_15_37698) | Y3_69=Y0_66 | Y2_68=Y0_66 | Y1_67=Y0_66 | ~rr(i2003_11_14_17_15_37698, Y3_69) | ~rr(i2003_11_14_17_15_37698, Y2_68) | ~rr(i2003_11_14_17_15_37698, Y1_67) | ~rr(i2003_11_14_17_15_37698, Y0_66)))).
% 15.28/4.59 tff(c_4558, plain, (![X_31]: ('#skF_9'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.59 tff(c_4592, plain, (![X_31]: ('#skF_8'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.59 tff(c_5072, plain, (![X_31]: ('#skF_11'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.59 tff(c_4225, plain, (![X_31]: ('#skF_8'(X_31)='#skF_12'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.59 tff(c_3675, plain, (![X_31]: ('#skF_7'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.59 tff(c_4897, plain, (![X_31]: ('#skF_9'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.59 tff(c_9700, plain, (![Y2_126, Y1_123, Y0_122]: (Y2_126='#skF_12'(i2003_11_14_17_15_37698) | Y2_126='#skF_11'(i2003_11_14_17_15_37698) | Y1_123='#skF_12'(i2003_11_14_17_15_37698) | Y1_123='#skF_11'(i2003_11_14_17_15_37698) | Y2_126=Y1_123 | Y0_122='#skF_12'(i2003_11_14_17_15_37698) | Y0_122='#skF_11'(i2003_11_14_17_15_37698) | Y2_126=Y0_122 | Y1_123=Y0_122 | ~rr(i2003_11_14_17_15_37698, Y2_126) | ~rr(i2003_11_14_17_15_37698, Y1_123) | ~rr(i2003_11_14_17_15_37698, Y0_122)))).
% 15.28/4.59 tff(c_3888, plain, (![X_31]: ('#skF_8'(X_31)='#skF_13'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.59 tff(c_8427, plain, (![Y2_126, Y1_123, Y0_122]: (Y2_126='#skF_6'(i2003_11_14_17_15_37698) | Y2_126='#skF_13'(i2003_11_14_17_15_37698) | Y1_123='#skF_6'(i2003_11_14_17_15_37698) | Y1_123='#skF_13'(i2003_11_14_17_15_37698) | Y2_126=Y1_123 | Y0_122='#skF_6'(i2003_11_14_17_15_37698) | Y0_122='#skF_13'(i2003_11_14_17_15_37698) | Y2_126=Y0_122 | Y1_123=Y0_122 | ~rr(i2003_11_14_17_15_37698, Y2_126) | ~rr(i2003_11_14_17_15_37698, Y1_123) | ~rr(i2003_11_14_17_15_37698, Y0_122)))).
% 15.28/4.59 tff(c_8423, plain, (![Y2_126, Y1_123, Y0_122]: (Y2_126='#skF_11'(i2003_11_14_17_15_37698) | Y2_126='#skF_13'(i2003_11_14_17_15_37698) | Y1_123='#skF_11'(i2003_11_14_17_15_37698) | Y1_123='#skF_13'(i2003_11_14_17_15_37698) | Y2_126=Y1_123 | Y0_122='#skF_11'(i2003_11_14_17_15_37698) | Y0_122='#skF_13'(i2003_11_14_17_15_37698) | Y2_126=Y0_122 | Y1_123=Y0_122 | ~rr(i2003_11_14_17_15_37698, Y2_126) | ~rr(i2003_11_14_17_15_37698, Y1_123) | ~rr(i2003_11_14_17_15_37698, Y0_122)))).
% 15.28/4.59 tff(c_5376, plain, (![X_31]: ('#skF_7'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.59 tff(c_10993, plain, (![Y2_126, Y1_123, Y0_122]: (Y2_126='#skF_11'(i2003_11_14_17_15_37698) | Y2_126='#skF_6'(i2003_11_14_17_15_37698) | Y1_123='#skF_11'(i2003_11_14_17_15_37698) | Y1_123='#skF_6'(i2003_11_14_17_15_37698) | Y2_126=Y1_123 | Y0_122='#skF_11'(i2003_11_14_17_15_37698) | Y0_122='#skF_6'(i2003_11_14_17_15_37698) | Y2_126=Y0_122 | Y1_123=Y0_122 | ~rr(i2003_11_14_17_15_37698, Y2_126) | ~rr(i2003_11_14_17_15_37698, Y1_123) | ~rr(i2003_11_14_17_15_37698, Y0_122)))).
% 15.28/4.59 tff(c_7010, plain, (![Y2_126, Y1_123, Y0_122]: (Y2_126='#skF_13'(i2003_11_14_17_15_37698) | Y2_126='#skF_12'(i2003_11_14_17_15_37698) | Y1_123='#skF_13'(i2003_11_14_17_15_37698) | Y1_123='#skF_12'(i2003_11_14_17_15_37698) | Y2_126=Y1_123 | Y0_122='#skF_13'(i2003_11_14_17_15_37698) | Y0_122='#skF_12'(i2003_11_14_17_15_37698) | Y2_126=Y0_122 | Y1_123=Y0_122 | ~rr(i2003_11_14_17_15_37698, Y2_126) | ~rr(i2003_11_14_17_15_37698, Y1_123) | ~rr(i2003_11_14_17_15_37698, Y0_122)))).
% 15.28/4.59 tff(c_7017, plain, (![Y2_126, Y1_123, Y0_122]: (Y2_126='#skF_6'(i2003_11_14_17_15_37698) | Y2_126='#skF_12'(i2003_11_14_17_15_37698) | Y1_123='#skF_6'(i2003_11_14_17_15_37698) | Y1_123='#skF_12'(i2003_11_14_17_15_37698) | Y2_126=Y1_123 | Y0_122='#skF_6'(i2003_11_14_17_15_37698) | Y0_122='#skF_12'(i2003_11_14_17_15_37698) | Y2_126=Y0_122 | Y1_123=Y0_122 | ~rr(i2003_11_14_17_15_37698, Y2_126) | ~rr(i2003_11_14_17_15_37698, Y1_123) | ~rr(i2003_11_14_17_15_37698, Y0_122)))).
% 15.28/4.59 tff(c_4148, plain, (![X_31]: ('#skF_9'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.59 tff(c_4037, plain, (![X_31]: ('#skF_9'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.59 tff(c_3446, plain, (![X_31]: ('#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.59 tff(c_3601, plain, (![X_31]: ('#skF_11'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.59 tff(c_5302, plain, (![X_31]: ('#skF_11'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.59 tff(c_5225, plain, (![X_31]: ('#skF_8'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.59 tff(c_5007, plain, (![X_31]: ('#skF_7'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_9'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_3713, plain, (![X_31]: ('#skF_7'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_3595, plain, (![X_31]: ('#skF_11'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_4073, plain, (![X_31]: ('#skF_13'(X_31)='#skF_12'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_3629, plain, (![X_31]: ('#skF_10'(X_31)='#skF_12'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_3306, plain, (![X_31]: ('#skF_10'(X_31)='#skF_11'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_9579, plain, (![Y1_129, Y0_128]: (Y1_129='#skF_12'(i2003_11_14_17_15_37698) | Y1_129='#skF_6'(i2003_11_14_17_15_37698) | Y1_129='#skF_11'(i2003_11_14_17_15_37698) | Y0_128='#skF_12'(i2003_11_14_17_15_37698) | Y0_128='#skF_6'(i2003_11_14_17_15_37698) | Y0_128='#skF_11'(i2003_11_14_17_15_37698) | Y1_129=Y0_128 | ~rr(i2003_11_14_17_15_37698, Y1_129) | ~rr(i2003_11_14_17_15_37698, Y0_128)))).
% 15.28/4.60 tff(c_10961, plain, (![Y1_129, Y0_128]: (Y1_129='#skF_12'(i2003_11_14_17_15_37698) | Y1_129='#skF_13'(i2003_11_14_17_15_37698) | Y1_129='#skF_6'(i2003_11_14_17_15_37698) | Y0_128='#skF_12'(i2003_11_14_17_15_37698) | Y0_128='#skF_13'(i2003_11_14_17_15_37698) | Y0_128='#skF_6'(i2003_11_14_17_15_37698) | Y1_129=Y0_128 | ~rr(i2003_11_14_17_15_37698, Y1_129) | ~rr(i2003_11_14_17_15_37698, Y0_128)))).
% 15.28/4.60 tff(c_9682, plain, (![Y1_129, Y0_128]: (Y1_129='#skF_12'(i2003_11_14_17_15_37698) | Y1_129='#skF_13'(i2003_11_14_17_15_37698) | Y1_129='#skF_11'(i2003_11_14_17_15_37698) | Y0_128='#skF_12'(i2003_11_14_17_15_37698) | Y0_128='#skF_13'(i2003_11_14_17_15_37698) | Y0_128='#skF_11'(i2003_11_14_17_15_37698) | Y1_129=Y0_128 | ~rr(i2003_11_14_17_15_37698, Y1_129) | ~rr(i2003_11_14_17_15_37698, Y0_128)))).
% 15.28/4.60 tff(c_5258, plain, (![X_31]: ('#skF_10'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_8307, plain, (![Y1_158, Y0_157]: (Y1_158='#skF_11'(i2003_11_14_17_15_37698) | Y1_158='#skF_6'(i2003_11_14_17_15_37698) | Y1_158='#skF_13'(i2003_11_14_17_15_37698) | Y0_157='#skF_11'(i2003_11_14_17_15_37698) | Y0_157='#skF_6'(i2003_11_14_17_15_37698) | Y0_157='#skF_13'(i2003_11_14_17_15_37698) | Y1_158=Y0_157 | ~rr(i2003_11_14_17_15_37698, Y1_158) | ~rr(i2003_11_14_17_15_37698, Y0_157)))).
% 15.28/4.60 tff(c_4633, plain, (![X_31]: ('#skF_10'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_4775, plain, (![X_31]: ('#skF_13'(X_31)='#skF_11'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_9818, plain, (rr(i2003_11_14_17_15_37698, '#skF_6'(i2003_11_14_17_15_37698)))).
% 15.28/4.60 tff(c_9822, plain, (cp3('#skF_6'(i2003_11_14_17_15_37698)))).
% 15.28/4.60 tff(c_4635, plain, (![X_31]: ('#skF_10'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_9820, plain, (~cp2('#skF_6'(i2003_11_14_17_15_37698)))).
% 15.28/4.60 tff(c_9816, plain, (~cp1('#skF_6'(i2003_11_14_17_15_37698)))).
% 15.28/4.60 tff(c_9790, plain, ('#skF_10'(i2003_11_14_17_15_37698)='#skF_6'(i2003_11_14_17_15_37698))).
% 15.28/4.60 tff(c_4115, plain, (![X_31]: ('#skF_9'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_8550, plain, (rr(i2003_11_14_17_15_37698, '#skF_11'(i2003_11_14_17_15_37698)))).
% 15.28/4.60 tff(c_3746, plain, (![X_31]: ('#skF_9'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_8554, plain, (cp1('#skF_11'(i2003_11_14_17_15_37698)))).
% 15.28/4.60 tff(c_8552, plain, (cp('#skF_11'(i2003_11_14_17_15_37698)))).
% 15.28/4.60 tff(c_8532, plain, ('#skF_8'(i2003_11_14_17_15_37698)='#skF_11'(i2003_11_14_17_15_37698))).
% 15.28/4.60 tff(c_7247, plain, (rr(i2003_11_14_17_15_37698, '#skF_13'(i2003_11_14_17_15_37698)))).
% 15.28/4.60 tff(c_7253, plain, (cp('#skF_13'(i2003_11_14_17_15_37698)))).
% 15.28/4.60 tff(c_7251, plain, (cp2('#skF_13'(i2003_11_14_17_15_37698)))).
% 15.28/4.60 tff(c_3933, plain, (![X_31]: ('#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_7249, plain, (~cp1('#skF_13'(i2003_11_14_17_15_37698)))).
% 15.28/4.60 tff(c_7229, plain, ('#skF_7'(i2003_11_14_17_15_37698)='#skF_13'(i2003_11_14_17_15_37698))).
% 15.28/4.60 tff(c_7119, plain, (![Y0_301]: (Y0_301='#skF_13'(i2003_11_14_17_15_37698) | Y0_301='#skF_11'(i2003_11_14_17_15_37698) | Y0_301='#skF_6'(i2003_11_14_17_15_37698) | Y0_301='#skF_12'(i2003_11_14_17_15_37698) | ~rr(i2003_11_14_17_15_37698, Y0_301)))).
% 15.28/4.60 tff(c_7120, plain, ('#skF_11'(i2003_11_14_17_15_37698)!='#skF_6'(i2003_11_14_17_15_37698))).
% 15.28/4.60 tff(c_5636, plain, (![X_31]: ('#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_7094, plain, ('#skF_13'(i2003_11_14_17_15_37698)!='#skF_6'(i2003_11_14_17_15_37698))).
% 15.28/4.60 tff(c_4117, plain, (![X_31]: ('#skF_9'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_7050, plain, ('#skF_11'(i2003_11_14_17_15_37698)!='#skF_12'(i2003_11_14_17_15_37698))).
% 15.28/4.60 tff(c_5888, plain, (rr(i2003_11_14_17_15_37698, '#skF_12'(i2003_11_14_17_15_37698)))).
% 15.28/4.60 tff(c_5868, plain, ('#skF_12'(i2003_11_14_17_15_37698)!='#skF_6'(i2003_11_14_17_15_37698))).
% 15.28/4.60 tff(c_5894, plain, (~cp1('#skF_12'(i2003_11_14_17_15_37698)))).
% 15.28/4.60 tff(c_5896, plain, (cp4('#skF_12'(i2003_11_14_17_15_37698)))).
% 15.28/4.60 tff(c_5892, plain, (~cp3('#skF_12'(i2003_11_14_17_15_37698)))).
% 15.28/4.60 tff(c_3303, plain, (![X_31]: ('#skF_10'(X_31)='#skF_11'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_5890, plain, (~cp2('#skF_12'(i2003_11_14_17_15_37698)))).
% 15.28/4.60 tff(c_5867, plain, ('#skF_9'(i2003_11_14_17_15_37698)='#skF_12'(i2003_11_14_17_15_37698))).
% 15.28/4.60 tff(c_5866, plain, ('#skF_13'(i2003_11_14_17_15_37698)!='#skF_12'(i2003_11_14_17_15_37698))).
% 15.28/4.60 tff(c_3784, plain, (![X_31]: ('#skF_9'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_6'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_5782, plain, ('#skF_13'(i2003_11_14_17_15_37698)!='#skF_11'(i2003_11_14_17_15_37698))).
% 15.28/4.60 tff(c_3602, plain, (![X_31]: ('#skF_11'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_4741, plain, (![X_31]: ('#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_2116, plain, (![X_31, Y0_470]: ('#skF_13'(X_31)='#skF_12'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | Y0_470='#skF_13'(X_31) | Y0_470='#skF_12'(X_31) | Y0_470='#skF_10'(X_31) | Y0_470='#skF_11'(X_31) | ~rr(X_31, Y0_470) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_2058, plain, (![X_31, Y0_464]: ('#skF_9'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | Y0_464='#skF_8'(X_31) | Y0_464='#skF_9'(X_31) | Y0_464='#skF_12'(X_31) | Y0_464='#skF_7'(X_31) | ~rr(X_31, Y0_464) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_2504, plain, (![X_31, Y0_512]: ('#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_6'(X_31) | Y0_512='#skF_7'(X_31) | Y0_512='#skF_10'(X_31) | Y0_512='#skF_6'(X_31) | Y0_512='#skF_9'(X_31) | ~rr(X_31, Y0_512) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_2759, plain, (![X_31, Y0_539]: ('#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | Y0_539='#skF_9'(X_31) | Y0_539='#skF_6'(X_31) | Y0_539='#skF_8'(X_31) | Y0_539='#skF_13'(X_31) | ~rr(X_31, Y0_539) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_2064, plain, (![X_31, Y0_464]: ('#skF_9'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | Y0_464='#skF_8'(X_31) | Y0_464='#skF_9'(X_31) | Y0_464='#skF_12'(X_31) | Y0_464='#skF_10'(X_31) | ~rr(X_31, Y0_464) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_2233, plain, (![X_31, Y0_482]: ('#skF_8'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | Y0_482='#skF_8'(X_31) | Y0_482='#skF_6'(X_31) | Y0_482='#skF_11'(X_31) | Y0_482='#skF_10'(X_31) | ~rr(X_31, Y0_482) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_2758, plain, (![X_31, Y0_539]: ('#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | Y0_539='#skF_9'(X_31) | Y0_539='#skF_6'(X_31) | Y0_539='#skF_8'(X_31) | Y0_539='#skF_7'(X_31) | ~rr(X_31, Y0_539) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_2141, plain, (![X_31, Y0_473]: ('#skF_10'(X_31)='#skF_13'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | Y0_473='#skF_10'(X_31) | Y0_473='#skF_13'(X_31) | Y0_473='#skF_6'(X_31) | Y0_473='#skF_7'(X_31) | ~rr(X_31, Y0_473) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_1806, plain, (![X_31, Y0_437]: ('#skF_8'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | Y0_437='#skF_10'(X_31) | Y0_437='#skF_8'(X_31) | Y0_437='#skF_11'(X_31) | Y0_437='#skF_13'(X_31) | ~rr(X_31, Y0_437) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_2007, plain, (![X_31, Y0_458]: ('#skF_11'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | Y0_458='#skF_11'(X_31) | Y0_458='#skF_12'(X_31) | Y0_458='#skF_9'(X_31) | Y0_458='#skF_8'(X_31) | ~rr(X_31, Y0_458) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_1726, plain, (![X_31, Y0_428]: ('#skF_7'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | Y0_428='#skF_7'(X_31) | Y0_428='#skF_13'(X_31) | Y0_428='#skF_12'(X_31) | Y0_428='#skF_6'(X_31) | ~rr(X_31, Y0_428) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_3124, plain, (![X_31, Y0_578]: ('#skF_7'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | Y0_578='#skF_7'(X_31) | Y0_578='#skF_6'(X_31) | Y0_578='#skF_12'(X_31) | Y0_578='#skF_11'(X_31) | ~rr(X_31, Y0_578) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_2672, plain, (![X_31, Y0_530]: ('#skF_11'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | Y0_530='#skF_11'(X_31) | Y0_530='#skF_12'(X_31) | Y0_530='#skF_7'(X_31) | Y0_530='#skF_9'(X_31) | ~rr(X_31, Y0_530) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_2874, plain, (![X_31, Y0_551]: ('#skF_10'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | Y0_551='#skF_12'(X_31) | Y0_551='#skF_10'(X_31) | Y0_551='#skF_6'(X_31) | Y0_551='#skF_8'(X_31) | ~rr(X_31, Y0_551) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_2396, plain, (![X_31, Y0_500]: ('#skF_8'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | Y0_500='#skF_12'(X_31) | Y0_500='#skF_8'(X_31) | Y0_500='#skF_7'(X_31) | Y0_500='#skF_11'(X_31) | ~rr(X_31, Y0_500) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_2481, plain, (![X_31, Y0_509]: ('#skF_7'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | Y0_509='#skF_7'(X_31) | Y0_509='#skF_6'(X_31) | Y0_509='#skF_13'(X_31) | Y0_509='#skF_11'(X_31) | ~rr(X_31, Y0_509) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_3102, plain, (![X_31, Y0_575]: ('#skF_13'(X_31)='#skF_11'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | Y0_575='#skF_13'(X_31) | Y0_575='#skF_11'(X_31) | Y0_575='#skF_8'(X_31) | Y0_575='#skF_12'(X_31) | ~rr(X_31, Y0_575) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_3156, plain, (![X_31, Y0_581]: ('#skF_7'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | Y0_581='#skF_7'(X_31) | Y0_581='#skF_13'(X_31) | Y0_581='#skF_9'(X_31) | Y0_581='#skF_8'(X_31) | ~rr(X_31, Y0_581) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_2794, plain, (![X_31, Y0_542]: ('#skF_11'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | Y0_542='#skF_11'(X_31) | Y0_542='#skF_6'(X_31) | Y0_542='#skF_10'(X_31) | Y0_542='#skF_12'(X_31) | ~rr(X_31, Y0_542) | ~cSatisfiable(X_31)))).
% 15.28/4.60 tff(c_2564, plain, (![X_31, Y0_518]: ('#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | Y0_518='#skF_7'(X_31) | Y0_518='#skF_10'(X_31) | Y0_518='#skF_12'(X_31) | Y0_518='#skF_11'(X_31) | ~rr(X_31, Y0_518) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2984, plain, (![X_31, Y0_563]: ('#skF_7'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_9'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | Y0_563='#skF_7'(X_31) | Y0_563='#skF_6'(X_31) | Y0_563='#skF_9'(X_31) | Y0_563='#skF_13'(X_31) | ~rr(X_31, Y0_563) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2819, plain, (![X_31, Y0_545]: ('#skF_9'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_6'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | Y0_545='#skF_9'(X_31) | Y0_545='#skF_13'(X_31) | Y0_545='#skF_11'(X_31) | Y0_545='#skF_6'(X_31) | ~rr(X_31, Y0_545) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2962, plain, (![X_31, Y0_560]: ('#skF_7'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | Y0_560='#skF_7'(X_31) | Y0_560='#skF_11'(X_31) | Y0_560='#skF_13'(X_31) | Y0_560='#skF_12'(X_31) | ~rr(X_31, Y0_560) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_1896, plain, (![X_31, Y0_446]: ('#skF_9'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | Y0_446='#skF_9'(X_31) | Y0_446='#skF_11'(X_31) | Y0_446='#skF_7'(X_31) | Y0_446='#skF_8'(X_31) | ~rr(X_31, Y0_446) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2732, plain, (![X_31, Y0_536]: ('#skF_8'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | Y0_536='#skF_8'(X_31) | Y0_536='#skF_6'(X_31) | Y0_536='#skF_13'(X_31) | Y0_536='#skF_11'(X_31) | ~rr(X_31, Y0_536) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_1867, plain, (![X_31, Y0_443]: ('#skF_10'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | Y0_443='#skF_11'(X_31) | Y0_443='#skF_10'(X_31) | Y0_443='#skF_7'(X_31) | Y0_443='#skF_8'(X_31) | ~rr(X_31, Y0_443) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_1617, plain, (![X_31, Y0_416]: ('#skF_13'(X_31)='#skF_11'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | Y0_416='#skF_13'(X_31) | Y0_416='#skF_11'(X_31) | Y0_416='#skF_6'(X_31) | Y0_416='#skF_10'(X_31) | ~rr(X_31, Y0_416) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2900, plain, (![X_31, Y0_554]: ('#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | Y0_554='#skF_9'(X_31) | Y0_554='#skF_6'(X_31) | Y0_554='#skF_12'(X_31) | Y0_554='#skF_11'(X_31) | ~rr(X_31, Y0_554) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2112, plain, (![X_31, Y0_470]: ('#skF_13'(X_31)='#skF_12'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | Y0_470='#skF_13'(X_31) | Y0_470='#skF_12'(X_31) | Y0_470='#skF_10'(X_31) | Y0_470='#skF_9'(X_31) | ~rr(X_31, Y0_470) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2738, plain, (![X_31, Y0_536]: ('#skF_8'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | Y0_536='#skF_8'(X_31) | Y0_536='#skF_6'(X_31) | Y0_536='#skF_13'(X_31) | Y0_536='#skF_12'(X_31) | ~rr(X_31, Y0_536) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_1834, plain, (![X_31, Y0_440]: ('#skF_10'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | Y0_440='#skF_10'(X_31) | Y0_440='#skF_13'(X_31) | Y0_440='#skF_9'(X_31) | Y0_440='#skF_7'(X_31) | ~rr(X_31, Y0_440) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_1947, plain, (![X_31, Y0_452]: ('#skF_8'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | Y0_452='#skF_8'(X_31) | Y0_452='#skF_11'(X_31) | Y0_452='#skF_9'(X_31) | Y0_452='#skF_13'(X_31) | ~rr(X_31, Y0_452) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2059, plain, (![X_31, Y0_464]: ('#skF_9'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | Y0_464='#skF_8'(X_31) | Y0_464='#skF_9'(X_31) | Y0_464='#skF_12'(X_31) | Y0_464='#skF_13'(X_31) | ~rr(X_31, Y0_464) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2934, plain, (![X_31, Y0_557]: ('#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | Y0_557='#skF_7'(X_31) | Y0_557='#skF_10'(X_31) | Y0_557='#skF_13'(X_31) | Y0_557='#skF_12'(X_31) | ~rr(X_31, Y0_557) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_1866, plain, (![X_31, Y0_443]: ('#skF_10'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | Y0_443='#skF_11'(X_31) | Y0_443='#skF_10'(X_31) | Y0_443='#skF_7'(X_31) | Y0_443='#skF_6'(X_31) | ~rr(X_31, Y0_443) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2618, plain, (![X_31, Y0_524]: ('#skF_10'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | Y0_524='#skF_12'(X_31) | Y0_524='#skF_10'(X_31) | Y0_524='#skF_9'(X_31) | Y0_524='#skF_7'(X_31) | ~rr(X_31, Y0_524) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2140, plain, (![X_31, Y0_473]: ('#skF_10'(X_31)='#skF_13'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_6'(X_31) | Y0_473='#skF_10'(X_31) | Y0_473='#skF_13'(X_31) | Y0_473='#skF_6'(X_31) | Y0_473='#skF_9'(X_31) | ~rr(X_31, Y0_473) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2535, plain, (![X_31, Y0_515]: ('#skF_8'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | Y0_515='#skF_8'(X_31) | Y0_515='#skF_6'(X_31) | Y0_515='#skF_12'(X_31) | Y0_515='#skF_11'(X_31) | ~rr(X_31, Y0_515) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2647, plain, (![X_31, Y0_527]: ('#skF_7'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | Y0_527='#skF_8'(X_31) | Y0_527='#skF_7'(X_31) | Y0_527='#skF_11'(X_31) | Y0_527='#skF_13'(X_31) | ~rr(X_31, Y0_527) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_3073, plain, (![X_31, Y0_572]: ('#skF_7'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | Y0_572='#skF_8'(X_31) | Y0_572='#skF_7'(X_31) | Y0_572='#skF_6'(X_31) | Y0_572='#skF_10'(X_31) | ~rr(X_31, Y0_572) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_3120, plain, (![X_31, Y0_578]: ('#skF_7'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | Y0_578='#skF_7'(X_31) | Y0_578='#skF_6'(X_31) | Y0_578='#skF_12'(X_31) | Y0_578='#skF_9'(X_31) | ~rr(X_31, Y0_578) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_1917, plain, (![X_31, Y0_449]: ('#skF_8'(X_31)='#skF_12'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | Y0_449='#skF_12'(X_31) | Y0_449='#skF_8'(X_31) | Y0_449='#skF_10'(X_31) | Y0_449='#skF_7'(X_31) | ~rr(X_31, Y0_449) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2198, plain, (![X_31, Y0_479]: ('#skF_8'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | Y0_479='#skF_8'(X_31) | Y0_479='#skF_6'(X_31) | Y0_479='#skF_10'(X_31) | Y0_479='#skF_13'(X_31) | ~rr(X_31, Y0_479) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2091, plain, (![X_31, Y0_467]: ('#skF_9'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | Y0_467='#skF_10'(X_31) | Y0_467='#skF_9'(X_31) | Y0_467='#skF_11'(X_31) | Y0_467='#skF_8'(X_31) | ~rr(X_31, Y0_467) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2842, plain, (![X_31, Y0_548]: ('#skF_9'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | Y0_548='#skF_9'(X_31) | Y0_548='#skF_12'(X_31) | Y0_548='#skF_13'(X_31) | Y0_548='#skF_7'(X_31) | ~rr(X_31, Y0_548) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_1696, plain, (![X_31, Y0_425]: ('#skF_13'(X_31)='#skF_12'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | Y0_425='#skF_13'(X_31) | Y0_425='#skF_12'(X_31) | Y0_425='#skF_6'(X_31) | Y0_425='#skF_11'(X_31) | ~rr(X_31, Y0_425) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2285, plain, (![X_31, Y0_488]: ('#skF_9'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | Y0_488='#skF_8'(X_31) | Y0_488='#skF_9'(X_31) | Y0_488='#skF_10'(X_31) | Y0_488='#skF_6'(X_31) | ~rr(X_31, Y0_488) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_1748, plain, (![X_31, Y0_431]: ('#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | Y0_431='#skF_7'(X_31) | Y0_431='#skF_10'(X_31) | Y0_431='#skF_8'(X_31) | Y0_431='#skF_9'(X_31) | ~rr(X_31, Y0_431) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_3017, plain, (![X_31, Y0_566]: ('#skF_8'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | Y0_566='#skF_13'(X_31) | Y0_566='#skF_8'(X_31) | Y0_566='#skF_7'(X_31) | Y0_566='#skF_10'(X_31) | ~rr(X_31, Y0_566) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2766, plain, (![X_31, Y0_539]: ('#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | Y0_539='#skF_9'(X_31) | Y0_539='#skF_6'(X_31) | Y0_539='#skF_8'(X_31) | Y0_539='#skF_12'(X_31) | ~rr(X_31, Y0_539) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2598, plain, (![X_31, Y0_521]: ('#skF_8'(X_31)='#skF_13'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | Y0_521='#skF_13'(X_31) | Y0_521='#skF_8'(X_31) | Y0_521='#skF_10'(X_31) | Y0_521='#skF_12'(X_31) | ~rr(X_31, Y0_521) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2821, plain, (![X_31, Y0_545]: ('#skF_9'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | Y0_545='#skF_9'(X_31) | Y0_545='#skF_13'(X_31) | Y0_545='#skF_11'(X_31) | Y0_545='#skF_10'(X_31) | ~rr(X_31, Y0_545) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2345, plain, (![X_31, Y0_494]: ('#skF_8'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | Y0_494='#skF_13'(X_31) | Y0_494='#skF_8'(X_31) | Y0_494='#skF_9'(X_31) | Y0_494='#skF_10'(X_31) | ~rr(X_31, Y0_494) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2090, plain, (![X_31, Y0_467]: ('#skF_9'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_6'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | Y0_467='#skF_10'(X_31) | Y0_467='#skF_9'(X_31) | Y0_467='#skF_11'(X_31) | Y0_467='#skF_6'(X_31) | ~rr(X_31, Y0_467) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2094, plain, (![X_31, Y0_467]: ('#skF_9'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | Y0_467='#skF_10'(X_31) | Y0_467='#skF_9'(X_31) | Y0_467='#skF_11'(X_31) | Y0_467='#skF_12'(X_31) | ~rr(X_31, Y0_467) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2484, plain, (![X_31, Y0_509]: ('#skF_7'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | Y0_509='#skF_7'(X_31) | Y0_509='#skF_6'(X_31) | Y0_509='#skF_13'(X_31) | Y0_509='#skF_8'(X_31) | ~rr(X_31, Y0_509) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2650, plain, (![X_31, Y0_527]: ('#skF_7'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | Y0_527='#skF_8'(X_31) | Y0_527='#skF_7'(X_31) | Y0_527='#skF_11'(X_31) | Y0_527='#skF_6'(X_31) | ~rr(X_31, Y0_527) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_1782, plain, (![X_31, Y0_434]: ('#skF_10'(X_31)='#skF_12'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | Y0_434='#skF_12'(X_31) | Y0_434='#skF_10'(X_31) | Y0_434='#skF_11'(X_31) | Y0_434='#skF_8'(X_31) | ~rr(X_31, Y0_434) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2168, plain, (![X_31, Y0_476]: ('#skF_11'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | Y0_476='#skF_11'(X_31) | Y0_476='#skF_6'(X_31) | Y0_476='#skF_7'(X_31) | Y0_476='#skF_9'(X_31) | ~rr(X_31, Y0_476) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2456, plain, (![X_31, Y0_506]: ('#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | Y0_506='#skF_9'(X_31) | Y0_506='#skF_6'(X_31) | Y0_506='#skF_11'(X_31) | Y0_506='#skF_8'(X_31) | ~rr(X_31, Y0_506) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2533, plain, (![X_31, Y0_515]: ('#skF_8'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | Y0_515='#skF_8'(X_31) | Y0_515='#skF_6'(X_31) | Y0_515='#skF_12'(X_31) | Y0_515='#skF_7'(X_31) | ~rr(X_31, Y0_515) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2845, plain, (![X_31, Y0_548]: ('#skF_9'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | Y0_548='#skF_9'(X_31) | Y0_548='#skF_12'(X_31) | Y0_548='#skF_13'(X_31) | Y0_548='#skF_11'(X_31) | ~rr(X_31, Y0_548) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2710, plain, (![X_31, Y0_533]: ('#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | Y0_533='#skF_9'(X_31) | Y0_533='#skF_6'(X_31) | Y0_533='#skF_10'(X_31) | Y0_533='#skF_12'(X_31) | ~rr(X_31, Y0_533) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2150, plain, (![X_31, Y0_473]: ('#skF_10'(X_31)='#skF_13'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | Y0_473='#skF_10'(X_31) | Y0_473='#skF_13'(X_31) | Y0_473='#skF_6'(X_31) | Y0_473='#skF_12'(X_31) | ~rr(X_31, Y0_473) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2869, plain, (![X_31, Y0_551]: ('#skF_10'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | Y0_551='#skF_12'(X_31) | Y0_551='#skF_10'(X_31) | Y0_551='#skF_6'(X_31) | Y0_551='#skF_7'(X_31) | ~rr(X_31, Y0_551) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_3154, plain, (![X_31, Y0_581]: ('#skF_7'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | Y0_581='#skF_7'(X_31) | Y0_581='#skF_13'(X_31) | Y0_581='#skF_9'(X_31) | Y0_581='#skF_11'(X_31) | ~rr(X_31, Y0_581) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_1665, plain, (![X_31, Y0_422]: ('#skF_10'(X_31)='#skF_11'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | Y0_422='#skF_11'(X_31) | Y0_422='#skF_10'(X_31) | Y0_422='#skF_13'(X_31) | Y0_422='#skF_7'(X_31) | ~rr(X_31, Y0_422) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2086, plain, (![X_31, Y0_467]: ('#skF_9'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | Y0_467='#skF_10'(X_31) | Y0_467='#skF_9'(X_31) | Y0_467='#skF_11'(X_31) | Y0_467='#skF_7'(X_31) | ~rr(X_31, Y0_467) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2899, plain, (![X_31, Y0_554]: ('#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | Y0_554='#skF_9'(X_31) | Y0_554='#skF_6'(X_31) | Y0_554='#skF_12'(X_31) | Y0_554='#skF_13'(X_31) | ~rr(X_31, Y0_554) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_2395, plain, (![X_31, Y0_500]: ('#skF_8'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | Y0_500='#skF_12'(X_31) | Y0_500='#skF_8'(X_31) | Y0_500='#skF_7'(X_31) | Y0_500='#skF_13'(X_31) | ~rr(X_31, Y0_500) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_978, plain, (![X_31, Y1_275, Y0_276]: ('#skF_7'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | Y1_275='#skF_7'(X_31) | Y1_275='#skF_13'(X_31) | Y1_275='#skF_9'(X_31) | Y0_276='#skF_7'(X_31) | Y0_276='#skF_13'(X_31) | Y0_276='#skF_9'(X_31) | Y1_275=Y0_276 | ~rr(X_31, Y1_275) | ~rr(X_31, Y0_276) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_854, plain, (![X_31, Y1_250, Y0_251]: ('#skF_7'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | Y1_250='#skF_7'(X_31) | Y1_250='#skF_6'(X_31) | Y1_250='#skF_12'(X_31) | Y0_251='#skF_7'(X_31) | Y0_251='#skF_6'(X_31) | Y0_251='#skF_12'(X_31) | Y1_250=Y0_251 | ~rr(X_31, Y1_250) | ~rr(X_31, Y0_251) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_1118, plain, (![X_31, Y1_300, Y0_301]: ('#skF_13'(X_31)='#skF_11'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | Y1_300='#skF_13'(X_31) | Y1_300='#skF_11'(X_31) | Y1_300='#skF_8'(X_31) | Y0_301='#skF_13'(X_31) | Y0_301='#skF_11'(X_31) | Y0_301='#skF_8'(X_31) | Y1_300=Y0_301 | ~rr(X_31, Y1_300) | ~rr(X_31, Y0_301) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_1062, plain, (![X_31, Y1_292, Y0_293]: ('#skF_7'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | Y1_292='#skF_8'(X_31) | Y1_292='#skF_7'(X_31) | Y1_292='#skF_6'(X_31) | Y0_293='#skF_8'(X_31) | Y0_293='#skF_7'(X_31) | Y0_293='#skF_6'(X_31) | Y1_292=Y0_293 | ~rr(X_31, Y1_292) | ~rr(X_31, Y0_293) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_1539, plain, (![X_31, Y1_394, Y0_395]: ('#skF_9'(X_31)='#skF_7'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | Y1_394='#skF_7'(X_31) | Y1_394='#skF_9'(X_31) | Y1_394='#skF_10'(X_31) | Y0_395='#skF_7'(X_31) | Y0_395='#skF_9'(X_31) | Y0_395='#skF_10'(X_31) | Y1_394=Y0_395 | ~rr(X_31, Y1_394) | ~rr(X_31, Y0_395) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_767, plain, (![X_31, Y1_233, Y0_234]: ('#skF_8'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | Y1_233='#skF_13'(X_31) | Y1_233='#skF_8'(X_31) | Y1_233='#skF_7'(X_31) | Y0_234='#skF_13'(X_31) | Y0_234='#skF_8'(X_31) | Y0_234='#skF_7'(X_31) | Y1_233=Y0_234 | ~rr(X_31, Y1_233) | ~rr(X_31, Y0_234) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_845, plain, (![X_31, Y1_250, Y0_251]: ('#skF_7'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_9'(X_31)='#skF_6'(X_31) | Y1_250='#skF_7'(X_31) | Y1_250='#skF_6'(X_31) | Y1_250='#skF_9'(X_31) | Y0_251='#skF_7'(X_31) | Y0_251='#skF_6'(X_31) | Y0_251='#skF_9'(X_31) | Y1_250=Y0_251 | ~rr(X_31, Y1_250) | ~rr(X_31, Y0_251) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_875, plain, (![X_31, Y1_254, Y0_255]: ('#skF_7'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | Y1_254='#skF_7'(X_31) | Y1_254='#skF_11'(X_31) | Y1_254='#skF_13'(X_31) | Y0_255='#skF_7'(X_31) | Y0_255='#skF_11'(X_31) | Y0_255='#skF_13'(X_31) | Y1_254=Y0_255 | ~rr(X_31, Y1_254) | ~rr(X_31, Y0_255) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_1008, plain, (![X_31, Y1_279, Y0_280]: ('#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | Y1_279='#skF_7'(X_31) | Y1_279='#skF_10'(X_31) | Y1_279='#skF_13'(X_31) | Y0_280='#skF_7'(X_31) | Y0_280='#skF_10'(X_31) | Y0_280='#skF_13'(X_31) | Y1_279=Y0_280 | ~rr(X_31, Y1_279) | ~rr(X_31, Y0_280) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_1409, plain, (![X_31, Y1_364, Y0_365]: ('#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | Y1_364='#skF_9'(X_31) | Y1_364='#skF_6'(X_31) | Y1_364='#skF_12'(X_31) | Y0_365='#skF_9'(X_31) | Y0_365='#skF_6'(X_31) | Y0_365='#skF_12'(X_31) | Y1_364=Y0_365 | ~rr(X_31, Y1_364) | ~rr(X_31, Y0_365) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_1194, plain, (![X_31, Y1_317, Y0_318]: ('#skF_10'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | Y1_317='#skF_12'(X_31) | Y1_317='#skF_10'(X_31) | Y1_317='#skF_6'(X_31) | Y0_318='#skF_12'(X_31) | Y0_318='#skF_10'(X_31) | Y0_318='#skF_6'(X_31) | Y1_317=Y0_318 | ~rr(X_31, Y1_317) | ~rr(X_31, Y0_318) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_821, plain, (![X_31, Y1_246, Y0_247]: ('#skF_9'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | Y1_246='#skF_9'(X_31) | Y1_246='#skF_12'(X_31) | Y1_246='#skF_13'(X_31) | Y0_247='#skF_9'(X_31) | Y0_247='#skF_12'(X_31) | Y0_247='#skF_13'(X_31) | Y1_246=Y0_247 | ~rr(X_31, Y1_246) | ~rr(X_31, Y0_247) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_638, plain, (![X_31, Y1_208, Y0_209]: ('#skF_9'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | Y1_208='#skF_9'(X_31) | Y1_208='#skF_13'(X_31) | Y1_208='#skF_11'(X_31) | Y0_209='#skF_9'(X_31) | Y0_209='#skF_13'(X_31) | Y0_209='#skF_11'(X_31) | Y1_208=Y0_209 | ~rr(X_31, Y1_208) | ~rr(X_31, Y0_209) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_1225, plain, (![X_31, Y1_321, Y0_322]: ('#skF_11'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | Y1_321='#skF_11'(X_31) | Y1_321='#skF_6'(X_31) | Y1_321='#skF_10'(X_31) | Y0_322='#skF_11'(X_31) | Y0_322='#skF_6'(X_31) | Y0_322='#skF_10'(X_31) | Y1_321=Y0_322 | ~rr(X_31, Y1_321) | ~rr(X_31, Y0_322) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_1407, plain, (![X_31, Y1_364, Y0_365]: ('#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | Y1_364='#skF_9'(X_31) | Y1_364='#skF_6'(X_31) | Y1_364='#skF_8'(X_31) | Y0_365='#skF_9'(X_31) | Y0_365='#skF_6'(X_31) | Y0_365='#skF_8'(X_31) | Y1_364=Y0_365 | ~rr(X_31, Y1_364) | ~rr(X_31, Y0_365) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_901, plain, (![X_31, Y1_258, Y0_259]: ('#skF_8'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | Y1_258='#skF_8'(X_31) | Y1_258='#skF_6'(X_31) | Y1_258='#skF_13'(X_31) | Y0_259='#skF_8'(X_31) | Y0_259='#skF_6'(X_31) | Y0_259='#skF_13'(X_31) | Y1_258=Y0_259 | ~rr(X_31, Y1_258) | ~rr(X_31, Y0_259) | ~cSatisfiable(X_31)))).
% 15.28/4.61 tff(c_1408, plain, (![X_31, Y1_364, Y0_365]: ('#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | Y1_364='#skF_9'(X_31) | Y1_364='#skF_6'(X_31) | Y1_364='#skF_10'(X_31) | Y0_365='#skF_9'(X_31) | Y0_365='#skF_6'(X_31) | Y0_365='#skF_10'(X_31) | Y1_364=Y0_365 | ~rr(X_31, Y1_364) | ~rr(X_31, Y0_365) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_952, plain, (![X_31, Y1_271, Y0_272]: ('#skF_11'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | Y1_271='#skF_11'(X_31) | Y1_271='#skF_12'(X_31) | Y1_271='#skF_7'(X_31) | Y0_272='#skF_11'(X_31) | Y0_272='#skF_12'(X_31) | Y0_272='#skF_7'(X_31) | Y1_271=Y0_272 | ~rr(X_31, Y1_271) | ~rr(X_31, Y0_272) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_1061, plain, (![X_31, Y1_292, Y0_293]: ('#skF_7'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | Y1_292='#skF_8'(X_31) | Y1_292='#skF_7'(X_31) | Y1_292='#skF_11'(X_31) | Y0_293='#skF_8'(X_31) | Y0_293='#skF_7'(X_31) | Y0_293='#skF_11'(X_31) | Y1_292=Y0_293 | ~rr(X_31, Y1_292) | ~rr(X_31, Y0_293) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_1190, plain, (![X_31, Y1_317, Y0_318]: ('#skF_10'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | Y1_317='#skF_12'(X_31) | Y1_317='#skF_10'(X_31) | Y1_317='#skF_9'(X_31) | Y0_318='#skF_12'(X_31) | Y0_318='#skF_10'(X_31) | Y0_318='#skF_9'(X_31) | Y1_317=Y0_318 | ~rr(X_31, Y1_317) | ~rr(X_31, Y0_318) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_774, plain, (![X_31, Y1_233, Y0_234]: ('#skF_8'(X_31)='#skF_13'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | Y1_233='#skF_13'(X_31) | Y1_233='#skF_8'(X_31) | Y1_233='#skF_10'(X_31) | Y0_234='#skF_13'(X_31) | Y0_234='#skF_8'(X_31) | Y0_234='#skF_10'(X_31) | Y1_233=Y0_234 | ~rr(X_31, Y1_233) | ~rr(X_31, Y0_234) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_1014, plain, (![X_31, Y1_279, Y0_280]: ('#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | Y1_279='#skF_7'(X_31) | Y1_279='#skF_10'(X_31) | Y1_279='#skF_12'(X_31) | Y0_280='#skF_7'(X_31) | Y0_280='#skF_10'(X_31) | Y0_280='#skF_12'(X_31) | Y1_279=Y0_280 | ~rr(X_31, Y1_279) | ~rr(X_31, Y0_280) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_908, plain, (![X_31, Y1_258, Y0_259]: ('#skF_8'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | Y1_258='#skF_8'(X_31) | Y1_258='#skF_6'(X_31) | Y1_258='#skF_12'(X_31) | Y0_259='#skF_8'(X_31) | Y0_259='#skF_6'(X_31) | Y0_259='#skF_12'(X_31) | Y1_258=Y0_259 | ~rr(X_31, Y1_258) | ~rr(X_31, Y0_259) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_1010, plain, (![X_31, Y1_279, Y0_280]: ('#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | Y1_279='#skF_7'(X_31) | Y1_279='#skF_10'(X_31) | Y1_279='#skF_6'(X_31) | Y0_280='#skF_7'(X_31) | Y0_280='#skF_10'(X_31) | Y0_280='#skF_6'(X_31) | Y1_279=Y0_280 | ~rr(X_31, Y1_279) | ~rr(X_31, Y0_280) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_848, plain, (![X_31, Y1_250, Y0_251]: ('#skF_7'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_13'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | Y1_250='#skF_7'(X_31) | Y1_250='#skF_6'(X_31) | Y1_250='#skF_13'(X_31) | Y0_251='#skF_7'(X_31) | Y0_251='#skF_6'(X_31) | Y0_251='#skF_13'(X_31) | Y1_250=Y0_251 | ~rr(X_31, Y1_250) | ~rr(X_31, Y0_251) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_1404, plain, (![X_31, Y1_364, Y0_365]: ('#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | Y1_364='#skF_9'(X_31) | Y1_364='#skF_6'(X_31) | Y1_364='#skF_11'(X_31) | Y0_365='#skF_9'(X_31) | Y0_365='#skF_6'(X_31) | Y0_365='#skF_11'(X_31) | Y1_364=Y0_365 | ~rr(X_31, Y1_364) | ~rr(X_31, Y0_365) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_957, plain, (![X_31, Y1_271, Y0_272]: ('#skF_11'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | Y1_271='#skF_11'(X_31) | Y1_271='#skF_12'(X_31) | Y1_271='#skF_8'(X_31) | Y0_272='#skF_11'(X_31) | Y0_272='#skF_12'(X_31) | Y0_272='#skF_8'(X_31) | Y1_271=Y0_272 | ~rr(X_31, Y1_271) | ~rr(X_31, Y0_272) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_607, plain, (![X_31, Y1_204, Y0_205]: ('#skF_8'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | Y1_204='#skF_12'(X_31) | Y1_204='#skF_8'(X_31) | Y1_204='#skF_7'(X_31) | Y0_205='#skF_12'(X_31) | Y0_205='#skF_8'(X_31) | Y0_205='#skF_7'(X_31) | Y1_204=Y0_205 | ~rr(X_31, Y1_204) | ~rr(X_31, Y0_205) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_956, plain, (![X_31, Y1_271, Y0_272]: ('#skF_11'(X_31)='#skF_12'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | Y1_271='#skF_11'(X_31) | Y1_271='#skF_12'(X_31) | Y1_271='#skF_6'(X_31) | Y0_272='#skF_11'(X_31) | Y0_272='#skF_12'(X_31) | Y0_272='#skF_6'(X_31) | Y1_271=Y0_272 | ~rr(X_31, Y1_271) | ~rr(X_31, Y0_272) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_766, plain, (![X_31, Y1_233, Y0_234]: ('#skF_8'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | Y1_233='#skF_13'(X_31) | Y1_233='#skF_8'(X_31) | Y1_233='#skF_9'(X_31) | Y0_234='#skF_13'(X_31) | Y0_234='#skF_8'(X_31) | Y0_234='#skF_9'(X_31) | Y1_233=Y0_234 | ~rr(X_31, Y1_233) | ~rr(X_31, Y0_234) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_1120, plain, (![X_31, Y1_300, Y0_301]: ('#skF_13'(X_31)='#skF_11'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | Y1_300='#skF_13'(X_31) | Y1_300='#skF_11'(X_31) | Y1_300='#skF_12'(X_31) | Y0_301='#skF_13'(X_31) | Y0_301='#skF_11'(X_31) | Y0_301='#skF_12'(X_31) | Y1_300=Y0_301 | ~rr(X_31, Y1_300) | ~rr(X_31, Y0_301) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_587, plain, (![X_31, Y1_200, Y0_201]: ('#skF_9'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | Y1_200='#skF_8'(X_31) | Y1_200='#skF_9'(X_31) | Y1_200='#skF_10'(X_31) | Y0_201='#skF_8'(X_31) | Y0_201='#skF_9'(X_31) | Y0_201='#skF_10'(X_31) | Y1_200=Y0_201 | ~rr(X_31, Y1_200) | ~rr(X_31, Y0_201) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_527, plain, (![X_31, Y1_187, Y0_188]: ('#skF_7'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | Y1_187='#skF_7'(X_31) | Y1_187='#skF_12'(X_31) | Y1_187='#skF_9'(X_31) | Y0_188='#skF_7'(X_31) | Y0_188='#skF_12'(X_31) | Y0_188='#skF_9'(X_31) | Y1_187=Y0_188 | ~rr(X_31, Y1_187) | ~rr(X_31, Y0_188) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_902, plain, (![X_31, Y1_258, Y0_259]: ('#skF_8'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | Y1_258='#skF_8'(X_31) | Y1_258='#skF_6'(X_31) | Y1_258='#skF_11'(X_31) | Y0_259='#skF_8'(X_31) | Y0_259='#skF_6'(X_31) | Y0_259='#skF_11'(X_31) | Y1_258=Y0_259 | ~rr(X_31, Y1_258) | ~rr(X_31, Y0_259) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_907, plain, (![X_31, Y1_258, Y0_259]: ('#skF_8'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | Y1_258='#skF_8'(X_31) | Y1_258='#skF_6'(X_31) | Y1_258='#skF_10'(X_31) | Y0_259='#skF_8'(X_31) | Y0_259='#skF_6'(X_31) | Y0_259='#skF_10'(X_31) | Y1_258=Y0_259 | ~rr(X_31, Y1_258) | ~rr(X_31, Y0_259) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_1218, plain, (![X_31, Y1_321, Y0_322]: ('#skF_11'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | Y1_321='#skF_11'(X_31) | Y1_321='#skF_6'(X_31) | Y1_321='#skF_7'(X_31) | Y0_322='#skF_11'(X_31) | Y0_322='#skF_6'(X_31) | Y0_322='#skF_7'(X_31) | Y1_321=Y0_322 | ~rr(X_31, Y1_321) | ~rr(X_31, Y0_322) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_1326, plain, (![X_31, Y1_347, Y0_348]: ('#skF_10'(X_31)='#skF_13'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | Y1_347='#skF_10'(X_31) | Y1_347='#skF_13'(X_31) | Y1_347='#skF_6'(X_31) | Y0_348='#skF_10'(X_31) | Y0_348='#skF_13'(X_31) | Y0_348='#skF_6'(X_31) | Y1_347=Y0_348 | ~rr(X_31, Y1_347) | ~rr(X_31, Y0_348) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_1276, plain, (![X_31, Y1_334, Y0_335]: ('#skF_13'(X_31)='#skF_12'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | Y1_334='#skF_13'(X_31) | Y1_334='#skF_12'(X_31) | Y1_334='#skF_10'(X_31) | Y0_335='#skF_13'(X_31) | Y0_335='#skF_12'(X_31) | Y0_335='#skF_10'(X_31) | Y1_334=Y0_335 | ~rr(X_31, Y1_334) | ~rr(X_31, Y0_335) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_691, plain, (![X_31, Y1_216, Y0_217]: ('#skF_9'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | Y1_216='#skF_10'(X_31) | Y1_216='#skF_9'(X_31) | Y1_216='#skF_11'(X_31) | Y0_217='#skF_10'(X_31) | Y0_217='#skF_9'(X_31) | Y0_217='#skF_11'(X_31) | Y1_216=Y0_217 | ~rr(X_31, Y1_216) | ~rr(X_31, Y0_217) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_588, plain, (![X_31, Y1_200, Y0_201]: ('#skF_9'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | Y1_200='#skF_8'(X_31) | Y1_200='#skF_9'(X_31) | Y1_200='#skF_12'(X_31) | Y0_201='#skF_8'(X_31) | Y0_201='#skF_9'(X_31) | Y0_201='#skF_12'(X_31) | Y1_200=Y0_201 | ~rr(X_31, Y1_200) | ~rr(X_31, Y0_201) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_739, plain, (![X_31, Y1_229, Y0_230]: ('#skF_13'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_6'(X_31) | Y1_229='#skF_13'(X_31) | Y1_229='#skF_6'(X_31) | Y1_229='#skF_9'(X_31) | Y0_230='#skF_13'(X_31) | Y0_230='#skF_6'(X_31) | Y0_230='#skF_9'(X_31) | Y1_229=Y0_230 | ~rr(X_31, Y1_229) | ~rr(X_31, Y0_230) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_951, plain, (![X_31, Y1_271, Y0_272]: ('#skF_11'(X_31)='#skF_12'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_12'(X_31) | Y1_271='#skF_11'(X_31) | Y1_271='#skF_12'(X_31) | Y1_271='#skF_9'(X_31) | Y0_272='#skF_11'(X_31) | Y0_272='#skF_12'(X_31) | Y0_272='#skF_9'(X_31) | Y1_271=Y0_272 | ~rr(X_31, Y1_271) | ~rr(X_31, Y0_272) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_1275, plain, (![X_31, Y1_334, Y0_335]: ('#skF_13'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_13'(X_31) | '#skF_8'(X_31)='#skF_12'(X_31) | Y1_334='#skF_13'(X_31) | Y1_334='#skF_12'(X_31) | Y1_334='#skF_8'(X_31) | Y0_335='#skF_13'(X_31) | Y0_335='#skF_12'(X_31) | Y0_335='#skF_8'(X_31) | Y1_334=Y0_335 | ~rr(X_31, Y1_334) | ~rr(X_31, Y0_335) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_1084, plain, (![X_31, Y1_296, Y0_297]: ('#skF_8'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | '#skF_9'(X_31)='#skF_11'(X_31) | Y1_296='#skF_8'(X_31) | Y1_296='#skF_11'(X_31) | Y1_296='#skF_9'(X_31) | Y0_297='#skF_8'(X_31) | Y0_297='#skF_11'(X_31) | Y0_297='#skF_9'(X_31) | Y1_296=Y0_297 | ~rr(X_31, Y1_296) | ~rr(X_31, Y0_297) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_613, plain, (![X_31, Y1_204, Y0_205]: ('#skF_8'(X_31)='#skF_12'(X_31) | '#skF_10'(X_31)='#skF_12'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | Y1_204='#skF_12'(X_31) | Y1_204='#skF_8'(X_31) | Y1_204='#skF_10'(X_31) | Y0_205='#skF_12'(X_31) | Y0_205='#skF_8'(X_31) | Y0_205='#skF_10'(X_31) | Y1_204=Y0_205 | ~rr(X_31, Y1_204) | ~rr(X_31, Y0_205) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_1506, plain, (![X_31, Y1_390, Y0_391]: ('#skF_9'(X_31)='#skF_11'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | Y1_390='#skF_9'(X_31) | Y1_390='#skF_11'(X_31) | Y1_390='#skF_7'(X_31) | Y0_391='#skF_9'(X_31) | Y0_391='#skF_11'(X_31) | Y0_391='#skF_7'(X_31) | Y1_390=Y0_391 | ~rr(X_31, Y1_390) | ~rr(X_31, Y0_391) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_661, plain, (![X_31, Y1_212, Y0_213]: ('#skF_10'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_11'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | Y1_212='#skF_11'(X_31) | Y1_212='#skF_10'(X_31) | Y1_212='#skF_7'(X_31) | Y0_213='#skF_11'(X_31) | Y0_213='#skF_10'(X_31) | Y0_213='#skF_7'(X_31) | Y1_212=Y0_213 | ~rr(X_31, Y1_212) | ~rr(X_31, Y0_213) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_1321, plain, (![X_31, Y1_347, Y0_348]: ('#skF_10'(X_31)='#skF_13'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_13'(X_31) | Y1_347='#skF_10'(X_31) | Y1_347='#skF_13'(X_31) | Y1_347='#skF_9'(X_31) | Y0_348='#skF_10'(X_31) | Y0_348='#skF_13'(X_31) | Y0_348='#skF_9'(X_31) | Y1_347=Y0_348 | ~rr(X_31, Y1_347) | ~rr(X_31, Y0_348) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_1166, plain, (![X_31, Y1_313, Y0_314]: ('#skF_8'(X_31)='#skF_10'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | '#skF_8'(X_31)='#skF_11'(X_31) | Y1_313='#skF_10'(X_31) | Y1_313='#skF_8'(X_31) | Y1_313='#skF_11'(X_31) | Y0_314='#skF_10'(X_31) | Y0_314='#skF_8'(X_31) | Y0_314='#skF_11'(X_31) | Y1_313=Y0_314 | ~rr(X_31, Y1_313) | ~rr(X_31, Y0_314) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_1193, plain, (![X_31, Y1_317, Y0_318]: ('#skF_10'(X_31)='#skF_12'(X_31) | '#skF_11'(X_31)='#skF_12'(X_31) | '#skF_10'(X_31)='#skF_11'(X_31) | Y1_317='#skF_12'(X_31) | Y1_317='#skF_10'(X_31) | Y1_317='#skF_11'(X_31) | Y0_318='#skF_12'(X_31) | Y0_318='#skF_10'(X_31) | Y0_318='#skF_11'(X_31) | Y1_317=Y0_318 | ~rr(X_31, Y1_317) | ~rr(X_31, Y0_318) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_1011, plain, (![X_31, Y1_279, Y0_280]: ('#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | Y1_279='#skF_7'(X_31) | Y1_279='#skF_10'(X_31) | Y1_279='#skF_8'(X_31) | Y0_280='#skF_7'(X_31) | Y0_280='#skF_10'(X_31) | Y0_280='#skF_8'(X_31) | Y1_279=Y0_280 | ~rr(X_31, Y1_279) | ~rr(X_31, Y0_280) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_987, plain, (![X_31, Y1_275, Y0_276]: ('#skF_7'(X_31)='#skF_13'(X_31) | '#skF_7'(X_31)='#skF_12'(X_31) | '#skF_13'(X_31)='#skF_12'(X_31) | Y1_275='#skF_7'(X_31) | Y1_275='#skF_13'(X_31) | Y1_275='#skF_12'(X_31) | Y0_276='#skF_7'(X_31) | Y0_276='#skF_13'(X_31) | Y0_276='#skF_12'(X_31) | Y1_275=Y0_276 | ~rr(X_31, Y1_275) | ~rr(X_31, Y0_276) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_1274, plain, (![X_31, Y1_334, Y0_335]: ('#skF_13'(X_31)='#skF_12'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_12'(X_31)='#skF_6'(X_31) | Y1_334='#skF_13'(X_31) | Y1_334='#skF_12'(X_31) | Y1_334='#skF_6'(X_31) | Y0_335='#skF_13'(X_31) | Y0_335='#skF_12'(X_31) | Y0_335='#skF_6'(X_31) | Y1_334=Y0_335 | ~rr(X_31, Y1_334) | ~rr(X_31, Y0_335) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_662, plain, (![X_31, Y1_212, Y0_213]: ('#skF_10'(X_31)='#skF_11'(X_31) | '#skF_13'(X_31)='#skF_11'(X_31) | '#skF_10'(X_31)='#skF_13'(X_31) | Y1_212='#skF_11'(X_31) | Y1_212='#skF_10'(X_31) | Y1_212='#skF_13'(X_31) | Y0_213='#skF_11'(X_31) | Y0_213='#skF_10'(X_31) | Y0_213='#skF_13'(X_31) | Y1_212=Y0_213 | ~rr(X_31, Y1_212) | ~rr(X_31, Y0_213) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_1538, plain, (![X_31, Y1_394, Y0_395]: ('#skF_9'(X_31)='#skF_7'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | Y1_394='#skF_7'(X_31) | Y1_394='#skF_9'(X_31) | Y1_394='#skF_8'(X_31) | Y0_395='#skF_7'(X_31) | Y0_395='#skF_9'(X_31) | Y0_395='#skF_8'(X_31) | Y1_394=Y0_395 | ~rr(X_31, Y1_394) | ~rr(X_31, Y0_395) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_1117, plain, (![X_31, Y1_300, Y0_301]: ('#skF_13'(X_31)='#skF_11'(X_31) | '#skF_13'(X_31)='#skF_6'(X_31) | '#skF_11'(X_31)='#skF_6'(X_31) | Y1_300='#skF_13'(X_31) | Y1_300='#skF_11'(X_31) | Y1_300='#skF_6'(X_31) | Y0_301='#skF_13'(X_31) | Y0_301='#skF_11'(X_31) | Y0_301='#skF_6'(X_31) | Y1_300=Y0_301 | ~rr(X_31, Y1_300) | ~rr(X_31, Y0_301) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_90, plain, (![Y_58, Y_64, Y_60, Y_65, Y_61, X_31, Y_62, Y_59, Y_63]: ('#skF_5'(X_31)!='#skF_1'(X_31) | cSatisfiable(X_31) | ~cp2(Y_65) | ~rr(X_31, Y_65) | ~cp(Y_64) | ~cp4(Y_64) | ~rr(X_31, Y_64) | ~cp1(Y_63) | ~rr(X_31, Y_63) | ~cp3(Y_62) | ~rr(X_31, Y_62) | ~cp4(Y_61) | ~rr(X_31, Y_61) | ~cp1(Y_60) | ~cp(Y_60) | ~rr(X_31, Y_60) | ~cp(Y_59) | ~cp2(Y_59) | ~rr(X_31, Y_59) | ~cp(Y_58) | ~cp3(Y_58) | ~rr(X_31, Y_58)))).
% 15.28/4.62 tff(c_104, plain, (![Y_58, Y_64, Y_60, Y_65, Y_61, X_31, Y_62, Y_59, Y_63]: (rr(X_31, '#skF_2'(X_31)) | cSatisfiable(X_31) | ~cp2(Y_65) | ~rr(X_31, Y_65) | ~cp(Y_64) | ~cp4(Y_64) | ~rr(X_31, Y_64) | ~cp1(Y_63) | ~rr(X_31, Y_63) | ~cp3(Y_62) | ~rr(X_31, Y_62) | ~cp4(Y_61) | ~rr(X_31, Y_61) | ~cp1(Y_60) | ~cp(Y_60) | ~rr(X_31, Y_60) | ~cp(Y_59) | ~cp2(Y_59) | ~rr(X_31, Y_59) | ~cp(Y_58) | ~cp3(Y_58) | ~rr(X_31, Y_58)))).
% 15.28/4.62 tff(c_475, plain, (![X_31, Y2_179, Y1_177, Y0_176]: ('#skF_9'(X_31)='#skF_7'(X_31) | Y2_179='#skF_7'(X_31) | Y2_179='#skF_9'(X_31) | Y1_177='#skF_7'(X_31) | Y1_177='#skF_9'(X_31) | Y2_179=Y1_177 | Y0_176='#skF_7'(X_31) | Y0_176='#skF_9'(X_31) | Y2_179=Y0_176 | Y1_177=Y0_176 | ~rr(X_31, Y2_179) | ~rr(X_31, Y1_177) | ~rr(X_31, Y0_176) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_273, plain, (![X_31, Y2_131, Y1_129, Y0_128]: ('#skF_9'(X_31)='#skF_11'(X_31) | Y2_131='#skF_9'(X_31) | Y2_131='#skF_11'(X_31) | Y1_129='#skF_9'(X_31) | Y1_129='#skF_11'(X_31) | Y2_131=Y1_129 | Y0_128='#skF_9'(X_31) | Y0_128='#skF_11'(X_31) | Y2_131=Y0_128 | Y1_129=Y0_128 | ~rr(X_31, Y2_131) | ~rr(X_31, Y1_129) | ~rr(X_31, Y0_128) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_78, plain, (![Y_58, Y_64, Y_60, Y_65, Y_61, X_31, Y_62, Y_59, Y_63]: ('#skF_5'(X_31)!='#skF_4'(X_31) | cSatisfiable(X_31) | ~cp2(Y_65) | ~rr(X_31, Y_65) | ~cp(Y_64) | ~cp4(Y_64) | ~rr(X_31, Y_64) | ~cp1(Y_63) | ~rr(X_31, Y_63) | ~cp3(Y_62) | ~rr(X_31, Y_62) | ~cp4(Y_61) | ~rr(X_31, Y_61) | ~cp1(Y_60) | ~cp(Y_60) | ~rr(X_31, Y_60) | ~cp(Y_59) | ~cp2(Y_59) | ~rr(X_31, Y_59) | ~cp(Y_58) | ~cp3(Y_58) | ~rr(X_31, Y_58)))).
% 15.28/4.62 tff(c_324, plain, (![X_31, Y2_145, Y1_143, Y0_142]: ('#skF_10'(X_31)='#skF_6'(X_31) | Y2_145='#skF_10'(X_31) | Y2_145='#skF_6'(X_31) | Y1_143='#skF_10'(X_31) | Y1_143='#skF_6'(X_31) | Y2_145=Y1_143 | Y0_142='#skF_10'(X_31) | Y0_142='#skF_6'(X_31) | Y2_145=Y0_142 | Y1_143=Y0_142 | ~rr(X_31, Y2_145) | ~rr(X_31, Y1_143) | ~rr(X_31, Y0_142) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_96, plain, (![Y_58, Y_64, Y_60, Y_65, Y_61, X_31, Y_62, Y_59, Y_63]: ('#skF_2'(X_31)!='#skF_1'(X_31) | cSatisfiable(X_31) | ~cp2(Y_65) | ~rr(X_31, Y_65) | ~cp(Y_64) | ~cp4(Y_64) | ~rr(X_31, Y_64) | ~cp1(Y_63) | ~rr(X_31, Y_63) | ~cp3(Y_62) | ~rr(X_31, Y_62) | ~cp4(Y_61) | ~rr(X_31, Y_61) | ~cp1(Y_60) | ~cp(Y_60) | ~rr(X_31, Y_60) | ~cp(Y_59) | ~cp2(Y_59) | ~rr(X_31, Y_59) | ~cp(Y_58) | ~cp3(Y_58) | ~rr(X_31, Y_58)))).
% 15.28/4.62 tff(c_274, plain, (![X_31, Y2_131, Y1_129, Y0_128]: ('#skF_9'(X_31)='#skF_6'(X_31) | Y2_131='#skF_9'(X_31) | Y2_131='#skF_6'(X_31) | Y1_129='#skF_9'(X_31) | Y1_129='#skF_6'(X_31) | Y2_131=Y1_129 | Y0_128='#skF_9'(X_31) | Y0_128='#skF_6'(X_31) | Y2_131=Y0_128 | Y1_129=Y0_128 | ~rr(X_31, Y2_131) | ~rr(X_31, Y1_129) | ~rr(X_31, Y0_128) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_380, plain, (![X_31, Y2_155, Y1_153, Y0_152]: ('#skF_12'(X_31)='#skF_6'(X_31) | Y2_155='#skF_6'(X_31) | Y2_155='#skF_12'(X_31) | Y1_153='#skF_6'(X_31) | Y1_153='#skF_12'(X_31) | Y2_155=Y1_153 | Y0_152='#skF_6'(X_31) | Y0_152='#skF_12'(X_31) | Y2_155=Y0_152 | Y1_153=Y0_152 | ~rr(X_31, Y2_155) | ~rr(X_31, Y1_153) | ~rr(X_31, Y0_152) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_100, plain, (![Y_58, Y_64, Y_60, Y_65, Y_61, X_31, Y_62, Y_59, Y_63]: (rr(X_31, '#skF_4'(X_31)) | cSatisfiable(X_31) | ~cp2(Y_65) | ~rr(X_31, Y_65) | ~cp(Y_64) | ~cp4(Y_64) | ~rr(X_31, Y_64) | ~cp1(Y_63) | ~rr(X_31, Y_63) | ~cp3(Y_62) | ~rr(X_31, Y_62) | ~cp4(Y_61) | ~rr(X_31, Y_61) | ~cp1(Y_60) | ~cp(Y_60) | ~rr(X_31, Y_60) | ~cp(Y_59) | ~cp2(Y_59) | ~rr(X_31, Y_59) | ~cp(Y_58) | ~cp3(Y_58) | ~rr(X_31, Y_58)))).
% 15.28/4.62 tff(c_322, plain, (![X_31, Y2_145, Y1_143, Y0_142]: ('#skF_10'(X_31)='#skF_13'(X_31) | Y2_145='#skF_10'(X_31) | Y2_145='#skF_13'(X_31) | Y1_143='#skF_10'(X_31) | Y1_143='#skF_13'(X_31) | Y2_145=Y1_143 | Y0_142='#skF_10'(X_31) | Y0_142='#skF_13'(X_31) | Y2_145=Y0_142 | Y1_143=Y0_142 | ~rr(X_31, Y2_145) | ~rr(X_31, Y1_143) | ~rr(X_31, Y0_142) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_86, plain, (![Y_58, Y_64, Y_60, Y_65, Y_61, X_31, Y_62, Y_59, Y_63]: ('#skF_2'(X_31)!='#skF_4'(X_31) | cSatisfiable(X_31) | ~cp2(Y_65) | ~rr(X_31, Y_65) | ~cp(Y_64) | ~cp4(Y_64) | ~rr(X_31, Y_64) | ~cp1(Y_63) | ~rr(X_31, Y_63) | ~cp3(Y_62) | ~rr(X_31, Y_62) | ~cp4(Y_61) | ~rr(X_31, Y_61) | ~cp1(Y_60) | ~cp(Y_60) | ~rr(X_31, Y_60) | ~cp(Y_59) | ~cp2(Y_59) | ~rr(X_31, Y_59) | ~cp(Y_58) | ~cp3(Y_58) | ~rr(X_31, Y_58)))).
% 15.28/4.62 tff(c_432, plain, (![X_31, Y2_165, Y1_163, Y0_162]: ('#skF_13'(X_31)='#skF_12'(X_31) | Y2_165='#skF_13'(X_31) | Y2_165='#skF_12'(X_31) | Y1_163='#skF_13'(X_31) | Y1_163='#skF_12'(X_31) | Y2_165=Y1_163 | Y0_162='#skF_13'(X_31) | Y0_162='#skF_12'(X_31) | Y2_165=Y0_162 | Y1_163=Y0_162 | ~rr(X_31, Y2_165) | ~rr(X_31, Y1_163) | ~rr(X_31, Y0_162) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_80, plain, (![Y_58, Y_64, Y_60, Y_65, Y_61, X_31, Y_62, Y_59, Y_63]: ('#skF_5'(X_31)!='#skF_3'(X_31) | cSatisfiable(X_31) | ~cp2(Y_65) | ~rr(X_31, Y_65) | ~cp(Y_64) | ~cp4(Y_64) | ~rr(X_31, Y_64) | ~cp1(Y_63) | ~rr(X_31, Y_63) | ~cp3(Y_62) | ~rr(X_31, Y_62) | ~cp4(Y_61) | ~rr(X_31, Y_61) | ~cp1(Y_60) | ~cp(Y_60) | ~rr(X_31, Y_60) | ~cp(Y_59) | ~cp2(Y_59) | ~rr(X_31, Y_59) | ~cp(Y_58) | ~cp3(Y_58) | ~rr(X_31, Y_58)))).
% 15.28/4.62 tff(c_403, plain, (![X_31, Y2_160, Y1_158, Y0_157]: ('#skF_11'(X_31)='#skF_6'(X_31) | Y2_160='#skF_11'(X_31) | Y2_160='#skF_6'(X_31) | Y1_158='#skF_11'(X_31) | Y1_158='#skF_6'(X_31) | Y2_160=Y1_158 | Y0_157='#skF_11'(X_31) | Y0_157='#skF_6'(X_31) | Y2_160=Y0_157 | Y1_158=Y0_157 | ~rr(X_31, Y2_160) | ~rr(X_31, Y1_158) | ~rr(X_31, Y0_157) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_507, plain, (![X_31, Y2_184, Y1_182, Y0_181]: ('#skF_10'(X_31)='#skF_12'(X_31) | Y2_184='#skF_12'(X_31) | Y2_184='#skF_10'(X_31) | Y1_182='#skF_12'(X_31) | Y1_182='#skF_10'(X_31) | Y2_184=Y1_182 | Y0_181='#skF_12'(X_31) | Y0_181='#skF_10'(X_31) | Y2_184=Y0_181 | Y1_182=Y0_181 | ~rr(X_31, Y2_184) | ~rr(X_31, Y1_182) | ~rr(X_31, Y0_181) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_325, plain, (![X_31, Y2_145, Y1_143, Y0_142]: ('#skF_8'(X_31)='#skF_10'(X_31) | Y2_145='#skF_10'(X_31) | Y2_145='#skF_8'(X_31) | Y1_143='#skF_10'(X_31) | Y1_143='#skF_8'(X_31) | Y2_145=Y1_143 | Y0_142='#skF_10'(X_31) | Y0_142='#skF_8'(X_31) | Y2_145=Y0_142 | Y1_143=Y0_142 | ~rr(X_31, Y2_145) | ~rr(X_31, Y1_143) | ~rr(X_31, Y0_142) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_82, plain, (![Y_58, Y_64, Y_60, Y_65, Y_61, X_31, Y_62, Y_59, Y_63]: ('#skF_4'(X_31)!='#skF_3'(X_31) | cSatisfiable(X_31) | ~cp2(Y_65) | ~rr(X_31, Y_65) | ~cp(Y_64) | ~cp4(Y_64) | ~rr(X_31, Y_64) | ~cp1(Y_63) | ~rr(X_31, Y_63) | ~cp3(Y_62) | ~rr(X_31, Y_62) | ~cp4(Y_61) | ~rr(X_31, Y_61) | ~cp1(Y_60) | ~cp(Y_60) | ~rr(X_31, Y_60) | ~cp(Y_59) | ~cp2(Y_59) | ~rr(X_31, Y_59) | ~cp(Y_58) | ~cp3(Y_58) | ~rr(X_31, Y_58)))).
% 15.28/4.62 tff(c_428, plain, (![X_31, Y2_165, Y1_163, Y0_162]: ('#skF_13'(X_31)='#skF_11'(X_31) | Y2_165='#skF_13'(X_31) | Y2_165='#skF_11'(X_31) | Y1_163='#skF_13'(X_31) | Y1_163='#skF_11'(X_31) | Y2_165=Y1_163 | Y0_162='#skF_13'(X_31) | Y0_162='#skF_11'(X_31) | Y2_165=Y0_162 | Y1_163=Y0_162 | ~rr(X_31, Y2_165) | ~rr(X_31, Y1_163) | ~rr(X_31, Y0_162) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_349, plain, (![X_31, Y2_150, Y1_148, Y0_147]: ('#skF_8'(X_31)='#skF_11'(X_31) | Y2_150='#skF_8'(X_31) | Y2_150='#skF_11'(X_31) | Y1_148='#skF_8'(X_31) | Y1_148='#skF_11'(X_31) | Y2_150=Y1_148 | Y0_147='#skF_8'(X_31) | Y0_147='#skF_11'(X_31) | Y2_150=Y0_147 | Y1_148=Y0_147 | ~rr(X_31, Y2_150) | ~rr(X_31, Y1_148) | ~rr(X_31, Y0_147) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_347, plain, (![X_31, Y2_150, Y1_148, Y0_147]: ('#skF_7'(X_31)='#skF_8'(X_31) | Y2_150='#skF_8'(X_31) | Y2_150='#skF_7'(X_31) | Y1_148='#skF_8'(X_31) | Y1_148='#skF_7'(X_31) | Y2_150=Y1_148 | Y0_147='#skF_8'(X_31) | Y0_147='#skF_7'(X_31) | Y2_150=Y0_147 | Y1_148=Y0_147 | ~rr(X_31, Y2_150) | ~rr(X_31, Y1_148) | ~rr(X_31, Y0_147) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_98, plain, (![Y_58, Y_64, Y_60, Y_65, Y_61, X_31, Y_62, Y_59, Y_63]: (rr(X_31, '#skF_5'(X_31)) | cSatisfiable(X_31) | ~cp2(Y_65) | ~rr(X_31, Y_65) | ~cp(Y_64) | ~cp4(Y_64) | ~rr(X_31, Y_64) | ~cp1(Y_63) | ~rr(X_31, Y_63) | ~cp3(Y_62) | ~rr(X_31, Y_62) | ~cp4(Y_61) | ~rr(X_31, Y_61) | ~cp1(Y_60) | ~cp(Y_60) | ~rr(X_31, Y_60) | ~cp(Y_59) | ~cp2(Y_59) | ~rr(X_31, Y_59) | ~cp(Y_58) | ~cp3(Y_58) | ~rr(X_31, Y_58)))).
% 15.28/4.62 tff(c_482, plain, (![X_31, Y2_179, Y1_177, Y0_176]: ('#skF_7'(X_31)='#skF_10'(X_31) | Y2_179='#skF_7'(X_31) | Y2_179='#skF_10'(X_31) | Y1_177='#skF_7'(X_31) | Y1_177='#skF_10'(X_31) | Y2_179=Y1_177 | Y0_176='#skF_7'(X_31) | Y0_176='#skF_10'(X_31) | Y2_179=Y0_176 | Y1_177=Y0_176 | ~rr(X_31, Y2_179) | ~rr(X_31, Y1_177) | ~rr(X_31, Y0_176) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_478, plain, (![X_31, Y2_179, Y1_177, Y0_176]: ('#skF_7'(X_31)='#skF_13'(X_31) | Y2_179='#skF_7'(X_31) | Y2_179='#skF_13'(X_31) | Y1_177='#skF_7'(X_31) | Y1_177='#skF_13'(X_31) | Y2_179=Y1_177 | Y0_176='#skF_7'(X_31) | Y0_176='#skF_13'(X_31) | Y2_179=Y0_176 | Y1_177=Y0_176 | ~rr(X_31, Y2_179) | ~rr(X_31, Y1_177) | ~rr(X_31, Y0_176) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_406, plain, (![X_31, Y2_160, Y1_158, Y0_157]: ('#skF_11'(X_31)='#skF_12'(X_31) | Y2_160='#skF_11'(X_31) | Y2_160='#skF_12'(X_31) | Y1_158='#skF_11'(X_31) | Y1_158='#skF_12'(X_31) | Y2_160=Y1_158 | Y0_157='#skF_11'(X_31) | Y0_157='#skF_12'(X_31) | Y2_160=Y0_157 | Y1_158=Y0_157 | ~rr(X_31, Y2_160) | ~rr(X_31, Y1_158) | ~rr(X_31, Y0_157) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_88, plain, (![Y_58, Y_64, Y_60, Y_65, Y_61, X_31, Y_62, Y_59, Y_63]: ('#skF_2'(X_31)!='#skF_3'(X_31) | cSatisfiable(X_31) | ~cp2(Y_65) | ~rr(X_31, Y_65) | ~cp(Y_64) | ~cp4(Y_64) | ~rr(X_31, Y_64) | ~cp1(Y_63) | ~rr(X_31, Y_63) | ~cp3(Y_62) | ~rr(X_31, Y_62) | ~cp4(Y_61) | ~rr(X_31, Y_61) | ~cp1(Y_60) | ~cp(Y_60) | ~rr(X_31, Y_60) | ~cp(Y_59) | ~cp2(Y_59) | ~rr(X_31, Y_59) | ~cp(Y_58) | ~cp3(Y_58) | ~rr(X_31, Y_58)))).
% 15.28/4.62 tff(c_350, plain, (![X_31, Y2_150, Y1_148, Y0_147]: ('#skF_8'(X_31)='#skF_6'(X_31) | Y2_150='#skF_8'(X_31) | Y2_150='#skF_6'(X_31) | Y1_148='#skF_8'(X_31) | Y1_148='#skF_6'(X_31) | Y2_150=Y1_148 | Y0_147='#skF_8'(X_31) | Y0_147='#skF_6'(X_31) | Y2_150=Y0_147 | Y1_148=Y0_147 | ~rr(X_31, Y2_150) | ~rr(X_31, Y1_148) | ~rr(X_31, Y0_147) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_479, plain, (![X_31, Y2_179, Y1_177, Y0_176]: ('#skF_7'(X_31)='#skF_11'(X_31) | Y2_179='#skF_7'(X_31) | Y2_179='#skF_11'(X_31) | Y1_177='#skF_7'(X_31) | Y1_177='#skF_11'(X_31) | Y2_179=Y1_177 | Y0_176='#skF_7'(X_31) | Y0_176='#skF_11'(X_31) | Y2_179=Y0_176 | Y1_177=Y0_176 | ~rr(X_31, Y2_179) | ~rr(X_31, Y1_177) | ~rr(X_31, Y0_176) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_480, plain, (![X_31, Y2_179, Y1_177, Y0_176]: ('#skF_7'(X_31)='#skF_6'(X_31) | Y2_179='#skF_7'(X_31) | Y2_179='#skF_6'(X_31) | Y1_177='#skF_7'(X_31) | Y1_177='#skF_6'(X_31) | Y2_179=Y1_177 | Y0_176='#skF_7'(X_31) | Y0_176='#skF_6'(X_31) | Y2_179=Y0_176 | Y1_177=Y0_176 | ~rr(X_31, Y2_179) | ~rr(X_31, Y1_177) | ~rr(X_31, Y0_176) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_277, plain, (![X_31, Y2_131, Y1_129, Y0_128]: ('#skF_9'(X_31)='#skF_12'(X_31) | Y2_131='#skF_9'(X_31) | Y2_131='#skF_12'(X_31) | Y1_129='#skF_9'(X_31) | Y1_129='#skF_12'(X_31) | Y2_131=Y1_129 | Y0_128='#skF_9'(X_31) | Y0_128='#skF_12'(X_31) | Y2_131=Y0_128 | Y1_129=Y0_128 | ~rr(X_31, Y2_131) | ~rr(X_31, Y1_129) | ~rr(X_31, Y0_128) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_106, plain, (![Y_58, Y_64, Y_60, Y_65, Y_61, X_31, Y_62, Y_59, Y_63]: (rr(X_31, '#skF_1'(X_31)) | cSatisfiable(X_31) | ~cp2(Y_65) | ~rr(X_31, Y_65) | ~cp(Y_64) | ~cp4(Y_64) | ~rr(X_31, Y_64) | ~cp1(Y_63) | ~rr(X_31, Y_63) | ~cp3(Y_62) | ~rr(X_31, Y_62) | ~cp4(Y_61) | ~rr(X_31, Y_61) | ~cp1(Y_60) | ~cp(Y_60) | ~rr(X_31, Y_60) | ~cp(Y_59) | ~cp2(Y_59) | ~rr(X_31, Y_59) | ~cp(Y_58) | ~cp3(Y_58) | ~rr(X_31, Y_58)))).
% 15.28/4.62 tff(c_430, plain, (![X_31, Y2_165, Y1_163, Y0_162]: ('#skF_8'(X_31)='#skF_13'(X_31) | Y2_165='#skF_13'(X_31) | Y2_165='#skF_8'(X_31) | Y1_163='#skF_13'(X_31) | Y1_163='#skF_8'(X_31) | Y2_165=Y1_163 | Y0_162='#skF_13'(X_31) | Y0_162='#skF_8'(X_31) | Y2_165=Y0_162 | Y1_163=Y0_162 | ~rr(X_31, Y2_165) | ~rr(X_31, Y1_163) | ~rr(X_31, Y0_162) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_429, plain, (![X_31, Y2_165, Y1_163, Y0_162]: ('#skF_13'(X_31)='#skF_6'(X_31) | Y2_165='#skF_13'(X_31) | Y2_165='#skF_6'(X_31) | Y1_163='#skF_13'(X_31) | Y1_163='#skF_6'(X_31) | Y2_165=Y1_163 | Y0_162='#skF_13'(X_31) | Y0_162='#skF_6'(X_31) | Y2_165=Y0_162 | Y1_163=Y0_162 | ~rr(X_31, Y2_165) | ~rr(X_31, Y1_163) | ~rr(X_31, Y0_162) | ~cSatisfiable(X_31)))).
% 15.28/4.62 tff(c_92, plain, (![Y_58, Y_64, Y_60, Y_65, Y_61, X_31, Y_62, Y_59, Y_63]: ('#skF_4'(X_31)!='#skF_1'(X_31) | cSatisfiable(X_31) | ~cp2(Y_65) | ~rr(X_31, Y_65) | ~cp(Y_64) | ~cp4(Y_64) | ~rr(X_31, Y_64) | ~cp1(Y_63) | ~rr(X_31, Y_63) | ~cp3(Y_62) | ~rr(X_31, Y_62) | ~cp4(Y_61) | ~rr(X_31, Y_61) | ~cp1(Y_60) | ~cp(Y_60) | ~rr(X_31, Y_60) | ~cp(Y_59) | ~cp2(Y_59) | ~rr(X_31, Y_59) | ~cp(Y_58) | ~cp3(Y_58) | ~rr(X_31, Y_58)))).
% 15.28/4.63 tff(c_320, plain, (![X_31, Y2_145, Y1_143, Y0_142]: ('#skF_9'(X_31)='#skF_10'(X_31) | Y2_145='#skF_10'(X_31) | Y2_145='#skF_9'(X_31) | Y1_143='#skF_10'(X_31) | Y1_143='#skF_9'(X_31) | Y2_145=Y1_143 | Y0_142='#skF_10'(X_31) | Y0_142='#skF_9'(X_31) | Y2_145=Y0_142 | Y1_143=Y0_142 | ~rr(X_31, Y2_145) | ~rr(X_31, Y1_143) | ~rr(X_31, Y0_142) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_405, plain, (![X_31, Y2_160, Y1_158, Y0_157]: ('#skF_10'(X_31)='#skF_11'(X_31) | Y2_160='#skF_11'(X_31) | Y2_160='#skF_10'(X_31) | Y1_158='#skF_11'(X_31) | Y1_158='#skF_10'(X_31) | Y2_160=Y1_158 | Y0_157='#skF_11'(X_31) | Y0_157='#skF_10'(X_31) | Y2_160=Y0_157 | Y1_158=Y0_157 | ~rr(X_31, Y2_160) | ~rr(X_31, Y1_158) | ~rr(X_31, Y0_157) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_272, plain, (![X_31, Y2_131, Y1_129, Y0_128]: ('#skF_9'(X_31)='#skF_13'(X_31) | Y2_131='#skF_9'(X_31) | Y2_131='#skF_13'(X_31) | Y1_129='#skF_9'(X_31) | Y1_129='#skF_13'(X_31) | Y2_131=Y1_129 | Y0_128='#skF_9'(X_31) | Y0_128='#skF_13'(X_31) | Y2_131=Y0_128 | Y1_129=Y0_128 | ~rr(X_31, Y2_131) | ~rr(X_31, Y1_129) | ~rr(X_31, Y0_128) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_506, plain, (![X_31, Y2_184, Y1_182, Y0_181]: ('#skF_8'(X_31)='#skF_12'(X_31) | Y2_184='#skF_12'(X_31) | Y2_184='#skF_8'(X_31) | Y1_182='#skF_12'(X_31) | Y1_182='#skF_8'(X_31) | Y2_184=Y1_182 | Y0_181='#skF_12'(X_31) | Y0_181='#skF_8'(X_31) | Y2_184=Y0_181 | Y1_182=Y0_181 | ~rr(X_31, Y2_184) | ~rr(X_31, Y1_182) | ~rr(X_31, Y0_181) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_346, plain, (![X_31, Y2_150, Y1_148, Y0_147]: ('#skF_9'(X_31)='#skF_8'(X_31) | Y2_150='#skF_8'(X_31) | Y2_150='#skF_9'(X_31) | Y1_148='#skF_8'(X_31) | Y1_148='#skF_9'(X_31) | Y2_150=Y1_148 | Y0_147='#skF_8'(X_31) | Y0_147='#skF_9'(X_31) | Y2_150=Y0_147 | Y1_148=Y0_147 | ~rr(X_31, Y2_150) | ~rr(X_31, Y1_148) | ~rr(X_31, Y0_147) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_94, plain, (![Y_58, Y_64, Y_60, Y_65, Y_61, X_31, Y_62, Y_59, Y_63]: ('#skF_1'(X_31)!='#skF_3'(X_31) | cSatisfiable(X_31) | ~cp2(Y_65) | ~rr(X_31, Y_65) | ~cp(Y_64) | ~cp4(Y_64) | ~rr(X_31, Y_64) | ~cp1(Y_63) | ~rr(X_31, Y_63) | ~cp3(Y_62) | ~rr(X_31, Y_62) | ~cp4(Y_61) | ~rr(X_31, Y_61) | ~cp1(Y_60) | ~cp(Y_60) | ~rr(X_31, Y_60) | ~cp(Y_59) | ~cp2(Y_59) | ~rr(X_31, Y_59) | ~cp(Y_58) | ~cp3(Y_58) | ~rr(X_31, Y_58)))).
% 15.28/4.63 tff(c_483, plain, (![X_31, Y2_179, Y1_177, Y0_176]: ('#skF_7'(X_31)='#skF_12'(X_31) | Y2_179='#skF_7'(X_31) | Y2_179='#skF_12'(X_31) | Y1_177='#skF_7'(X_31) | Y1_177='#skF_12'(X_31) | Y2_179=Y1_177 | Y0_176='#skF_7'(X_31) | Y0_176='#skF_12'(X_31) | Y2_179=Y0_176 | Y1_177=Y0_176 | ~rr(X_31, Y2_179) | ~rr(X_31, Y1_177) | ~rr(X_31, Y0_176) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_251, plain, (![Y3_121, Y0_122, Y2_126, X_31, Y1_123]: (Y3_121='#skF_12'(X_31) | Y2_126='#skF_12'(X_31) | Y3_121=Y2_126 | Y1_123='#skF_12'(X_31) | Y3_121=Y1_123 | Y2_126=Y1_123 | Y0_122='#skF_12'(X_31) | Y3_121=Y0_122 | Y2_126=Y0_122 | Y1_123=Y0_122 | ~rr(X_31, Y3_121) | ~rr(X_31, Y2_126) | ~rr(X_31, Y1_123) | ~rr(X_31, Y0_122) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_245, plain, (![Y3_121, Y0_122, Y2_126, X_31, Y1_123]: (Y3_121='#skF_7'(X_31) | Y2_126='#skF_7'(X_31) | Y3_121=Y2_126 | Y1_123='#skF_7'(X_31) | Y3_121=Y1_123 | Y2_126=Y1_123 | Y0_122='#skF_7'(X_31) | Y3_121=Y0_122 | Y2_126=Y0_122 | Y1_123=Y0_122 | ~rr(X_31, Y3_121) | ~rr(X_31, Y2_126) | ~rr(X_31, Y1_123) | ~rr(X_31, Y0_122) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_102, plain, (![Y_58, Y_64, Y_60, Y_65, Y_61, X_31, Y_62, Y_59, Y_63]: (rr(X_31, '#skF_3'(X_31)) | cSatisfiable(X_31) | ~cp2(Y_65) | ~rr(X_31, Y_65) | ~cp(Y_64) | ~cp4(Y_64) | ~rr(X_31, Y_64) | ~cp1(Y_63) | ~rr(X_31, Y_63) | ~cp3(Y_62) | ~rr(X_31, Y_62) | ~cp4(Y_61) | ~rr(X_31, Y_61) | ~cp1(Y_60) | ~cp(Y_60) | ~rr(X_31, Y_60) | ~cp(Y_59) | ~cp2(Y_59) | ~rr(X_31, Y_59) | ~cp(Y_58) | ~cp3(Y_58) | ~rr(X_31, Y_58)))).
% 15.28/4.63 tff(c_246, plain, (![Y3_121, Y0_122, Y2_126, X_31, Y1_123]: (Y3_121='#skF_13'(X_31) | Y2_126='#skF_13'(X_31) | Y3_121=Y2_126 | Y1_123='#skF_13'(X_31) | Y3_121=Y1_123 | Y2_126=Y1_123 | Y0_122='#skF_13'(X_31) | Y3_121=Y0_122 | Y2_126=Y0_122 | Y1_123=Y0_122 | ~rr(X_31, Y3_121) | ~rr(X_31, Y2_126) | ~rr(X_31, Y1_123) | ~rr(X_31, Y0_122) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_247, plain, (![Y3_121, Y0_122, Y2_126, X_31, Y1_123]: (Y3_121='#skF_11'(X_31) | Y2_126='#skF_11'(X_31) | Y3_121=Y2_126 | Y1_123='#skF_11'(X_31) | Y3_121=Y1_123 | Y2_126=Y1_123 | Y0_122='#skF_11'(X_31) | Y3_121=Y0_122 | Y2_126=Y0_122 | Y1_123=Y0_122 | ~rr(X_31, Y3_121) | ~rr(X_31, Y2_126) | ~rr(X_31, Y1_123) | ~rr(X_31, Y0_122) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_248, plain, (![Y3_121, Y0_122, Y2_126, X_31, Y1_123]: (Y3_121='#skF_6'(X_31) | Y2_126='#skF_6'(X_31) | Y3_121=Y2_126 | Y1_123='#skF_6'(X_31) | Y3_121=Y1_123 | Y2_126=Y1_123 | Y0_122='#skF_6'(X_31) | Y3_121=Y0_122 | Y2_126=Y0_122 | Y1_123=Y0_122 | ~rr(X_31, Y3_121) | ~rr(X_31, Y2_126) | ~rr(X_31, Y1_123) | ~rr(X_31, Y0_122) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_249, plain, (![Y3_121, Y0_122, Y2_126, X_31, Y1_123]: (Y3_121='#skF_8'(X_31) | Y2_126='#skF_8'(X_31) | Y3_121=Y2_126 | Y1_123='#skF_8'(X_31) | Y3_121=Y1_123 | Y2_126=Y1_123 | Y0_122='#skF_8'(X_31) | Y3_121=Y0_122 | Y2_126=Y0_122 | Y1_123=Y0_122 | ~rr(X_31, Y3_121) | ~rr(X_31, Y2_126) | ~rr(X_31, Y1_123) | ~rr(X_31, Y0_122) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_250, plain, (![Y3_121, Y0_122, Y2_126, X_31, Y1_123]: (Y3_121='#skF_10'(X_31) | Y2_126='#skF_10'(X_31) | Y3_121=Y2_126 | Y1_123='#skF_10'(X_31) | Y3_121=Y1_123 | Y2_126=Y1_123 | Y0_122='#skF_10'(X_31) | Y3_121=Y0_122 | Y2_126=Y0_122 | Y1_123=Y0_122 | ~rr(X_31, Y3_121) | ~rr(X_31, Y2_126) | ~rr(X_31, Y1_123) | ~rr(X_31, Y0_122) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_84, plain, (![Y_58, Y_64, Y_60, Y_65, Y_61, X_31, Y_62, Y_59, Y_63]: ('#skF_5'(X_31)!='#skF_2'(X_31) | cSatisfiable(X_31) | ~cp2(Y_65) | ~rr(X_31, Y_65) | ~cp(Y_64) | ~cp4(Y_64) | ~rr(X_31, Y_64) | ~cp1(Y_63) | ~rr(X_31, Y_63) | ~cp3(Y_62) | ~rr(X_31, Y_62) | ~cp4(Y_61) | ~rr(X_31, Y_61) | ~cp1(Y_60) | ~cp(Y_60) | ~rr(X_31, Y_60) | ~cp(Y_59) | ~cp2(Y_59) | ~rr(X_31, Y_59) | ~cp(Y_58) | ~cp3(Y_58) | ~rr(X_31, Y_58)))).
% 15.28/4.63 tff(c_244, plain, (![Y3_121, Y0_122, Y2_126, X_31, Y1_123]: (Y3_121='#skF_9'(X_31) | Y2_126='#skF_9'(X_31) | Y3_121=Y2_126 | Y1_123='#skF_9'(X_31) | Y3_121=Y1_123 | Y2_126=Y1_123 | Y0_122='#skF_9'(X_31) | Y3_121=Y0_122 | Y2_126=Y0_122 | Y1_123=Y0_122 | ~rr(X_31, Y3_121) | ~rr(X_31, Y2_126) | ~rr(X_31, Y1_123) | ~rr(X_31, Y0_122) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_58, plain, (![Y3_69, Y4_70, Y0_66, Y1_67, X_31, Y2_68]: (Y4_70=Y3_69 | Y4_70=Y2_68 | Y3_69=Y2_68 | Y4_70=Y1_67 | Y3_69=Y1_67 | Y2_68=Y1_67 | Y4_70=Y0_66 | Y3_69=Y0_66 | Y2_68=Y0_66 | Y1_67=Y0_66 | ~rr(X_31, Y4_70) | ~rr(X_31, Y3_69) | ~rr(X_31, Y2_68) | ~rr(X_31, Y1_67) | ~rr(X_31, Y0_66) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_56, plain, (![X_31]: (rr(X_31, '#skF_9'(X_31)) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_70, plain, (![X_31]: (rr(X_31, '#skF_7'(X_31)) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_38, plain, (![X_31]: (rr(X_31, '#skF_13'(X_31)) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_48, plain, (![X_31]: (rr(X_31, '#skF_11'(X_31)) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_76, plain, (![X_31]: (rr(X_31, '#skF_6'(X_31)) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_167, plain, (![X_91]: (~cp2('#skF_9'(X_91)) | ~cSatisfiable(X_91)))).
% 15.28/4.63 tff(c_197, plain, (![X_96]: (~cp1('#skF_6'(X_96)) | ~cSatisfiable(X_96)))).
% 15.28/4.63 tff(c_64, plain, (![X_31]: (rr(X_31, '#skF_8'(X_31)) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_184, plain, (![X_94]: (~cp1('#skF_12'(X_94)) | ~cSatisfiable(X_94)))).
% 15.28/4.63 tff(c_155, plain, (![X_90]: (~cp1('#skF_10'(X_90)) | ~cSatisfiable(X_90)))).
% 15.28/4.63 tff(c_168, plain, (![X_91]: (~cp3('#skF_9'(X_91)) | ~cSatisfiable(X_91)))).
% 15.28/4.63 tff(c_52, plain, (![X_31]: (rr(X_31, '#skF_10'(X_31)) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_169, plain, (![X_91]: (~cp1('#skF_9'(X_91)) | ~cSatisfiable(X_91)))).
% 15.28/4.63 tff(c_156, plain, (![X_90]: (~cp2('#skF_10'(X_90)) | ~cSatisfiable(X_90)))).
% 15.28/4.63 tff(c_189, plain, (![X_95]: (~cp1('#skF_13'(X_95)) | ~cSatisfiable(X_95)))).
% 15.28/4.63 tff(c_198, plain, (![X_96]: (~cp2('#skF_6'(X_96)) | ~cSatisfiable(X_96)))).
% 15.28/4.63 tff(c_206, plain, (![X_100]: (~cp1('#skF_7'(X_100)) | ~cSatisfiable(X_100)))).
% 15.28/4.63 tff(c_44, plain, (![X_31]: (rr(X_31, '#skF_12'(X_31)) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_182, plain, (![X_94]: (~cp2('#skF_12'(X_94)) | ~cSatisfiable(X_94)))).
% 15.28/4.63 tff(c_183, plain, (![X_94]: (~cp3('#skF_12'(X_94)) | ~cSatisfiable(X_94)))).
% 15.28/4.63 tff(c_68, plain, (![X_31]: (cp2('#skF_7'(X_31)) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_40, plain, (![X_31]: (cp('#skF_12'(X_31)) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_46, plain, (![X_31]: (cp1('#skF_11'(X_31)) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_72, plain, (![X_31]: (cp('#skF_6'(X_31)) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_74, plain, (![X_31]: (cp3('#skF_6'(X_31)) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_36, plain, (![X_31]: (cp2('#skF_13'(X_31)) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_42, plain, (![X_31]: (cp4('#skF_12'(X_31)) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_62, plain, (![X_31]: (cp('#skF_8'(X_31)) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_60, plain, (![X_31]: (cp1('#skF_8'(X_31)) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_54, plain, (![X_31]: (cp4('#skF_9'(X_31)) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_50, plain, (![X_31]: (cp3('#skF_10'(X_31)) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_66, plain, (![X_31]: (cp('#skF_7'(X_31)) | ~cSatisfiable(X_31)))).
% 15.28/4.63 tff(c_34, plain, (![X_30]: (xsd_string(X_30) | xsd_integer(X_30)))).
% 15.28/4.63 tff(c_108, plain, (![X_71]: (~cp5(X_71) | ~cp1(X_71)))).
% 15.28/4.63 tff(c_110, plain, (![X_71]: (~cp2(X_71) | ~cp1(X_71)))).
% 15.28/4.63 tff(c_120, plain, (![X_72]: (~cp4(X_72) | ~cp2(X_72)))).
% 15.28/4.63 tff(c_112, plain, (![X_71]: (~cp3(X_71) | ~cp1(X_71)))).
% 15.28/4.63 tff(c_124, plain, (![X_73]: (~cp4(X_73) | ~cp3(X_73)))).
% 15.28/4.63 tff(c_32, plain, (![X_30]: (~xsd_integer(X_30) | ~xsd_string(X_30)))).
% 15.28/4.63 tff(c_118, plain, (![X_72]: (~cp3(X_72) | ~cp2(X_72)))).
% 15.28/4.63 tff(c_116, plain, (![X_72]: (~cp5(X_72) | ~cp2(X_72)))).
% 15.28/4.63 tff(c_114, plain, (![X_71]: (~cp4(X_71) | ~cp1(X_71)))).
% 15.28/4.63 tff(c_122, plain, (![X_73]: (~cp5(X_73) | ~cp3(X_73)))).
% 15.28/4.63 tff(c_126, plain, (![X_74]: (~cp5(X_74) | ~cp4(X_74)))).
% 15.28/4.63 tff(c_28, plain, (![X_29]: (cowlThing(X_29)))).
% 15.28/4.63 tff(c_30, plain, (![X_29]: (~cowlNothing(X_29)))).
% 15.28/4.63 tff(c_128, plain, (cSatisfiable(i2003_11_14_17_15_37698))).
% 15.28/4.63 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.28/4.63
%------------------------------------------------------------------------------