%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : KRS032+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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n025.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 6.74s 2.58s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : KRS032+1 : TPTP v9.0.0. Released v3.1.0.
% 0.11/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.33 % Computer : n025.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.34 % DateTime : Tue Apr 8 02:54:35 EDT 2025
% 0.13/0.34 % CPUTime :
% 6.74/2.58
% 6.74/2.58 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.74/2.58
% 6.74/2.58 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.74/2.59 %$ rr > xsd_string > xsd_integer > cp5 > cp4 > cp3 > cp2 > cp1 > cp > cowlThing > cowlNothing > cSatisfiable > #nlpp > i2003_11_14_17_15_33836 > #skF_9 > #skF_7 > #skF_5 > #skF_2 > #skF_4 > #skF_1 > #skF_8 > #skF_10 > #skF_3 > #skF_6
% 6.74/2.59
% 6.74/2.59 %Foreground sorts:
% 6.74/2.59
% 6.74/2.59
% 6.74/2.59 %Background operators:
% 6.74/2.59
% 6.74/2.59
% 6.74/2.59 %Foreground operators:
% 6.74/2.59 tff('#skF_9', type, '#skF_9': $i > $i).
% 6.74/2.59 tff('#skF_7', type, '#skF_7': $i > $i).
% 6.74/2.59 tff('#skF_5', type, '#skF_5': $i > $i).
% 6.74/2.59 tff(cp5, type, cp5: $i > $o).
% 6.74/2.59 tff(rr, type, rr: ($i * $i) > $o).
% 6.74/2.59 tff('#skF_2', type, '#skF_2': $i > $i).
% 6.74/2.59 tff('#skF_4', type, '#skF_4': $i > $i).
% 6.74/2.59 tff(cowlThing, type, cowlThing: $i > $o).
% 6.74/2.59 tff('#skF_1', type, '#skF_1': $i > $i).
% 6.74/2.59 tff('#skF_8', type, '#skF_8': $i > $i).
% 6.74/2.59 tff(cp4, type, cp4: $i > $o).
% 6.74/2.59 tff(i2003_11_14_17_15_33836, type, i2003_11_14_17_15_33836: $i).
% 6.74/2.59 tff(xsd_integer, type, xsd_integer: $i > $o).
% 6.74/2.59 tff('#skF_10', type, '#skF_10': $i > $i).
% 6.74/2.59 tff(cSatisfiable, type, cSatisfiable: $i > $o).
% 6.74/2.59 tff(cp3, type, cp3: $i > $o).
% 6.74/2.59 tff(xsd_string, type, xsd_string: $i > $o).
% 6.74/2.59 tff('#skF_3', type, '#skF_3': $i > $i).
% 6.74/2.59 tff(cp, type, cp: $i > $o).
% 6.74/2.59 tff(cp2, type, cp2: $i > $o).
% 6.74/2.59 tff('#skF_6', type, '#skF_6': $i > $i).
% 6.74/2.59 tff(cowlNothing, type, cowlNothing: $i > $o).
% 6.74/2.59 tff(cp1, type, cp1: $i > $o).
% 6.74/2.59
% 6.74/2.59 %Saturated clause set:
% 6.74/2.59 tff(c_950, plain, (![X_31]: ('#skF_7'(X_31)='#skF_8'(X_31) | '#skF_5'(X_31)='#skF_8'(X_31) | '#skF_7'(X_31)='#skF_5'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | '#skF_5'(X_31)='#skF_6'(X_31) | ~cSatisfiable(X_31)))).
% 6.74/2.59 tff(c_880, plain, (![X_31]: ('#skF_5'(X_31)='#skF_10'(X_31) | '#skF_5'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_5'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | ~cSatisfiable(X_31)))).
% 6.74/2.59 tff(c_2736, plain, (![Y2_60, Y1_59, Y0_58]: (Y2_60='#skF_6'(i2003_11_14_17_15_33836) | Y1_59='#skF_6'(i2003_11_14_17_15_33836) | Y2_60=Y1_59 | Y0_58='#skF_6'(i2003_11_14_17_15_33836) | Y2_60=Y0_58 | Y1_59=Y0_58 | ~rr(i2003_11_14_17_15_33836, Y2_60) | ~rr(i2003_11_14_17_15_33836, Y1_59) | ~rr(i2003_11_14_17_15_33836, Y0_58)))).
% 6.74/2.59 tff(c_2361, plain, (![Y2_60, Y1_59, Y0_58]: (Y2_60='#skF_10'(i2003_11_14_17_15_33836) | Y1_59='#skF_10'(i2003_11_14_17_15_33836) | Y2_60=Y1_59 | Y0_58='#skF_10'(i2003_11_14_17_15_33836) | Y2_60=Y0_58 | Y1_59=Y0_58 | ~rr(i2003_11_14_17_15_33836, Y2_60) | ~rr(i2003_11_14_17_15_33836, Y1_59) | ~rr(i2003_11_14_17_15_33836, Y0_58)))).
% 6.74/2.59 tff(c_1998, plain, (![Y2_60, Y1_59, Y0_58]: (Y2_60='#skF_8'(i2003_11_14_17_15_33836) | Y1_59='#skF_8'(i2003_11_14_17_15_33836) | Y2_60=Y1_59 | Y0_58='#skF_8'(i2003_11_14_17_15_33836) | Y2_60=Y0_58 | Y1_59=Y0_58 | ~rr(i2003_11_14_17_15_33836, Y2_60) | ~rr(i2003_11_14_17_15_33836, Y1_59) | ~rr(i2003_11_14_17_15_33836, Y0_58)))).
% 6.74/2.59 tff(c_1372, plain, (![X_31]: ('#skF_9'(X_31)='#skF_8'(X_31) | '#skF_9'(X_31)='#skF_5'(X_31) | '#skF_5'(X_31)='#skF_8'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_5'(X_31)='#skF_10'(X_31) | ~cSatisfiable(X_31)))).
% 6.74/2.59 tff(c_2994, plain, (![Y1_103, Y0_105]: (Y1_103='#skF_6'(i2003_11_14_17_15_33836) | Y1_103='#skF_10'(i2003_11_14_17_15_33836) | Y0_105='#skF_6'(i2003_11_14_17_15_33836) | Y0_105='#skF_10'(i2003_11_14_17_15_33836) | Y1_103=Y0_105 | ~rr(i2003_11_14_17_15_33836, Y1_103) | ~rr(i2003_11_14_17_15_33836, Y0_105)))).
% 6.74/2.59 tff(c_852, plain, (![X_31]: ('#skF_10'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | ~cSatisfiable(X_31)))).
% 6.74/2.59 tff(c_2922, plain, (![Y1_103, Y0_105]: (Y1_103='#skF_6'(i2003_11_14_17_15_33836) | Y1_103='#skF_8'(i2003_11_14_17_15_33836) | Y0_105='#skF_6'(i2003_11_14_17_15_33836) | Y0_105='#skF_8'(i2003_11_14_17_15_33836) | Y1_103=Y0_105 | ~rr(i2003_11_14_17_15_33836, Y1_103) | ~rr(i2003_11_14_17_15_33836, Y0_105)))).
% 6.74/2.59 tff(c_2860, plain, (![Y1_103, Y0_105]: (Y1_103='#skF_10'(i2003_11_14_17_15_33836) | Y1_103='#skF_8'(i2003_11_14_17_15_33836) | Y0_105='#skF_10'(i2003_11_14_17_15_33836) | Y0_105='#skF_8'(i2003_11_14_17_15_33836) | Y1_103=Y0_105 | ~rr(i2003_11_14_17_15_33836, Y1_103) | ~rr(i2003_11_14_17_15_33836, Y0_105)))).
% 6.74/2.59 tff(c_844, plain, (![X_31]: ('#skF_10'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_5'(X_31)='#skF_10'(X_31) | '#skF_5'(X_31)='#skF_6'(X_31) | '#skF_5'(X_31)='#skF_8'(X_31) | ~cSatisfiable(X_31)))).
% 6.74/2.59 tff(c_1258, plain, (![X_31]: ('#skF_9'(X_31)='#skF_8'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | '#skF_9'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | ~cSatisfiable(X_31)))).
% 6.74/2.59 tff(c_2754, plain, (![Y0_109]: (Y0_109='#skF_6'(i2003_11_14_17_15_33836) | Y0_109='#skF_10'(i2003_11_14_17_15_33836) | Y0_109='#skF_8'(i2003_11_14_17_15_33836) | ~rr(i2003_11_14_17_15_33836, Y0_109)))).
% 6.74/2.59 tff(c_922, plain, (![X_31]: ('#skF_8'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_6'(X_31) | ~cSatisfiable(X_31)))).
% 6.74/2.59 tff(c_2390, plain, (rr(i2003_11_14_17_15_33836, '#skF_6'(i2003_11_14_17_15_33836)))).
% 6.74/2.59 tff(c_817, plain, (![X_31]: ('#skF_10'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | ~cSatisfiable(X_31)))).
% 6.74/2.59 tff(c_2373, plain, ('#skF_8'(i2003_11_14_17_15_33836)!='#skF_6'(i2003_11_14_17_15_33836))).
% 6.74/2.59 tff(c_2396, plain, (cp3('#skF_6'(i2003_11_14_17_15_33836)))).
% 6.74/2.59 tff(c_2394, plain, (~cp1('#skF_6'(i2003_11_14_17_15_33836)))).
% 6.74/2.60 tff(c_2392, plain, (~cp2('#skF_6'(i2003_11_14_17_15_33836)))).
% 6.74/2.60 tff(c_2364, plain, ('#skF_5'(i2003_11_14_17_15_33836)='#skF_6'(i2003_11_14_17_15_33836))).
% 6.74/2.60 tff(c_1175, plain, (![X_31]: ('#skF_9'(X_31)='#skF_7'(X_31) | '#skF_7'(X_31)='#skF_5'(X_31) | '#skF_9'(X_31)='#skF_5'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_6'(X_31) | '#skF_5'(X_31)='#skF_6'(X_31) | ~cSatisfiable(X_31)))).
% 6.74/2.60 tff(c_2022, plain, (rr(i2003_11_14_17_15_33836, '#skF_10'(i2003_11_14_17_15_33836)))).
% 6.74/2.60 tff(c_2008, plain, ('#skF_10'(i2003_11_14_17_15_33836)!='#skF_6'(i2003_11_14_17_15_33836))).
% 6.74/2.60 tff(c_2026, plain, (cp('#skF_10'(i2003_11_14_17_15_33836)))).
% 6.74/2.60 tff(c_2024, plain, (cp1('#skF_10'(i2003_11_14_17_15_33836)))).
% 6.74/2.60 tff(c_2006, plain, ('#skF_9'(i2003_11_14_17_15_33836)='#skF_10'(i2003_11_14_17_15_33836))).
% 6.74/2.60 tff(c_1347, plain, (![X_31]: ('#skF_5'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_5'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_5'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | ~cSatisfiable(X_31)))).
% 6.74/2.60 tff(c_1664, plain, (rr(i2003_11_14_17_15_33836, '#skF_8'(i2003_11_14_17_15_33836)))).
% 6.74/2.60 tff(c_1229, plain, (![X_31]: ('#skF_8'(X_31)='#skF_6'(X_31) | '#skF_5'(X_31)='#skF_8'(X_31) | '#skF_5'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | '#skF_9'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_5'(X_31) | ~cSatisfiable(X_31)))).
% 6.74/2.60 tff(c_1666, plain, (cp2('#skF_8'(i2003_11_14_17_15_33836)))).
% 6.74/2.60 tff(c_1662, plain, (~cp1('#skF_8'(i2003_11_14_17_15_33836)))).
% 6.74/2.60 tff(c_1644, plain, ('#skF_7'(i2003_11_14_17_15_33836)='#skF_8'(i2003_11_14_17_15_33836))).
% 6.74/2.60 tff(c_1255, plain, (![X_31]: ('#skF_9'(X_31)='#skF_8'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | '#skF_9'(X_31)='#skF_5'(X_31) | '#skF_5'(X_31)='#skF_8'(X_31) | '#skF_7'(X_31)='#skF_5'(X_31) | ~cSatisfiable(X_31)))).
% 7.16/2.60 tff(c_874, plain, (![X_31]: ('#skF_5'(X_31)='#skF_10'(X_31) | '#skF_5'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_5'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_6'(X_31) | ~cSatisfiable(X_31)))).
% 7.16/2.60 tff(c_1456, plain, ('#skF_8'(i2003_11_14_17_15_33836)!='#skF_10'(i2003_11_14_17_15_33836))).
% 7.16/2.60 tff(c_927, plain, (![X_31]: ('#skF_8'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | ~cSatisfiable(X_31)))).
% 7.16/2.60 tff(c_1059, plain, (![X_31]: ('#skF_8'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | '#skF_5'(X_31)='#skF_10'(X_31) | '#skF_5'(X_31)='#skF_8'(X_31) | '#skF_7'(X_31)='#skF_5'(X_31) | ~cSatisfiable(X_31)))).
% 7.16/2.60 tff(c_444, plain, (![X_31, Y0_162]: ('#skF_9'(X_31)='#skF_8'(X_31) | '#skF_9'(X_31)='#skF_5'(X_31) | '#skF_5'(X_31)='#skF_8'(X_31) | Y0_162='#skF_9'(X_31) | Y0_162='#skF_8'(X_31) | Y0_162='#skF_5'(X_31) | ~rr(X_31, Y0_162) | ~cSatisfiable(X_31)))).
% 7.16/2.60 tff(c_631, plain, (![X_31, Y0_197]: ('#skF_5'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_5'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | Y0_197='#skF_5'(X_31) | Y0_197='#skF_10'(X_31) | Y0_197='#skF_9'(X_31) | ~rr(X_31, Y0_197) | ~cSatisfiable(X_31)))).
% 7.16/2.60 tff(c_344, plain, (![X_31, Y0_139]: ('#skF_7'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | Y0_139='#skF_10'(X_31) | Y0_139='#skF_7'(X_31) | Y0_139='#skF_9'(X_31) | ~rr(X_31, Y0_139) | ~cSatisfiable(X_31)))).
% 7.16/2.60 tff(c_790, plain, (![X_31, Y0_237]: ('#skF_10'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_6'(X_31) | Y0_237='#skF_10'(X_31) | Y0_237='#skF_6'(X_31) | Y0_237='#skF_9'(X_31) | ~rr(X_31, Y0_237) | ~cSatisfiable(X_31)))).
% 7.16/2.60 tff(c_451, plain, (![X_31, Y0_162]: ('#skF_9'(X_31)='#skF_8'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | Y0_162='#skF_9'(X_31) | Y0_162='#skF_8'(X_31) | Y0_162='#skF_7'(X_31) | ~rr(X_31, Y0_162) | ~cSatisfiable(X_31)))).
% 7.16/2.60 tff(c_711, plain, (![X_31, Y0_213]: ('#skF_8'(X_31)='#skF_6'(X_31) | '#skF_5'(X_31)='#skF_8'(X_31) | '#skF_5'(X_31)='#skF_6'(X_31) | Y0_213='#skF_8'(X_31) | Y0_213='#skF_6'(X_31) | Y0_213='#skF_5'(X_31) | ~rr(X_31, Y0_213) | ~cSatisfiable(X_31)))).
% 7.16/2.60 tff(c_672, plain, (![X_31, Y0_203]: ('#skF_7'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_7'(X_31) | '#skF_9'(X_31)='#skF_6'(X_31) | Y0_203='#skF_7'(X_31) | Y0_203='#skF_6'(X_31) | Y0_203='#skF_9'(X_31) | ~rr(X_31, Y0_203) | ~cSatisfiable(X_31)))).
% 7.16/2.60 tff(c_547, plain, (![X_31, Y0_181]: ('#skF_9'(X_31)='#skF_7'(X_31) | '#skF_7'(X_31)='#skF_5'(X_31) | '#skF_9'(X_31)='#skF_5'(X_31) | Y0_181='#skF_7'(X_31) | Y0_181='#skF_9'(X_31) | Y0_181='#skF_5'(X_31) | ~rr(X_31, Y0_181) | ~cSatisfiable(X_31)))).
% 7.16/2.60 tff(c_343, plain, (![X_31, Y0_139]: ('#skF_7'(X_31)='#skF_10'(X_31) | '#skF_5'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_5'(X_31) | Y0_139='#skF_10'(X_31) | Y0_139='#skF_7'(X_31) | Y0_139='#skF_5'(X_31) | ~rr(X_31, Y0_139) | ~cSatisfiable(X_31)))).
% 7.16/2.60 tff(c_568, plain, (![X_31, Y0_184]: ('#skF_9'(X_31)='#skF_6'(X_31) | '#skF_5'(X_31)='#skF_6'(X_31) | '#skF_9'(X_31)='#skF_5'(X_31) | Y0_184='#skF_6'(X_31) | Y0_184='#skF_9'(X_31) | Y0_184='#skF_5'(X_31) | ~rr(X_31, Y0_184) | ~cSatisfiable(X_31)))).
% 7.16/2.60 tff(c_447, plain, (![X_31, Y0_162]: ('#skF_9'(X_31)='#skF_8'(X_31) | '#skF_9'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | Y0_162='#skF_9'(X_31) | Y0_162='#skF_8'(X_31) | Y0_162='#skF_6'(X_31) | ~rr(X_31, Y0_162) | ~cSatisfiable(X_31)))).
% 7.16/2.60 tff(c_472, plain, (![X_31, Y0_165]: ('#skF_8'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | Y0_165='#skF_10'(X_31) | Y0_165='#skF_8'(X_31) | Y0_165='#skF_7'(X_31) | ~rr(X_31, Y0_165) | ~cSatisfiable(X_31)))).
% 7.16/2.60 tff(c_676, plain, (![X_31, Y0_203]: ('#skF_7'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | Y0_203='#skF_7'(X_31) | Y0_203='#skF_6'(X_31) | Y0_203='#skF_8'(X_31) | ~rr(X_31, Y0_203) | ~cSatisfiable(X_31)))).
% 7.16/2.60 tff(c_386, plain, (![X_31, Y0_149]: ('#skF_7'(X_31)='#skF_5'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | '#skF_5'(X_31)='#skF_6'(X_31) | Y0_149='#skF_7'(X_31) | Y0_149='#skF_5'(X_31) | Y0_149='#skF_6'(X_31) | ~rr(X_31, Y0_149) | ~cSatisfiable(X_31)))).
% 7.16/2.60 tff(c_635, plain, (![X_31, Y0_197]: ('#skF_5'(X_31)='#skF_10'(X_31) | '#skF_5'(X_31)='#skF_8'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | Y0_197='#skF_5'(X_31) | Y0_197='#skF_10'(X_31) | Y0_197='#skF_8'(X_31) | ~rr(X_31, Y0_197) | ~cSatisfiable(X_31)))).
% 7.16/2.60 tff(c_507, plain, (![X_31, Y0_171]: ('#skF_7'(X_31)='#skF_8'(X_31) | '#skF_5'(X_31)='#skF_8'(X_31) | '#skF_7'(X_31)='#skF_5'(X_31) | Y0_171='#skF_8'(X_31) | Y0_171='#skF_7'(X_31) | Y0_171='#skF_5'(X_31) | ~rr(X_31, Y0_171) | ~cSatisfiable(X_31)))).
% 7.16/2.60 tff(c_466, plain, (![X_31, Y0_165]: ('#skF_8'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_10'(X_31) | '#skF_9'(X_31)='#skF_8'(X_31) | Y0_165='#skF_10'(X_31) | Y0_165='#skF_8'(X_31) | Y0_165='#skF_9'(X_31) | ~rr(X_31, Y0_165) | ~cSatisfiable(X_31)))).
% 7.16/2.60 tff(c_76, plain, (![Y_57, Y_53, Y_54, Y_55, X_31, Y_56, Y_52]: ('#skF_1'(X_31)!='#skF_3'(X_31) | cSatisfiable(X_31) | ~cp1(Y_57) | ~rr(X_31, Y_57) | ~cp1(Y_56) | ~cp(Y_56) | ~rr(X_31, Y_56) | ~cp(Y_55) | ~cp2(Y_55) | ~rr(X_31, Y_55) | ~cp2(Y_54) | ~rr(X_31, Y_54) | ~cp(Y_53) | ~cp3(Y_53) | ~rr(X_31, Y_53) | ~cp3(Y_52) | ~rr(X_31, Y_52)))).
% 7.16/2.60 tff(c_632, plain, (![X_31, Y0_197]: ('#skF_5'(X_31)='#skF_10'(X_31) | '#skF_5'(X_31)='#skF_6'(X_31) | '#skF_10'(X_31)='#skF_6'(X_31) | Y0_197='#skF_5'(X_31) | Y0_197='#skF_10'(X_31) | Y0_197='#skF_6'(X_31) | ~rr(X_31, Y0_197) | ~cSatisfiable(X_31)))).
% 7.16/2.60 tff(c_795, plain, (![X_31, Y0_237]: ('#skF_10'(X_31)='#skF_6'(X_31) | '#skF_8'(X_31)='#skF_10'(X_31) | '#skF_8'(X_31)='#skF_6'(X_31) | Y0_237='#skF_10'(X_31) | Y0_237='#skF_6'(X_31) | Y0_237='#skF_8'(X_31) | ~rr(X_31, Y0_237) | ~cSatisfiable(X_31)))).
% 7.16/2.60 tff(c_796, plain, (![X_31, Y0_237]: ('#skF_10'(X_31)='#skF_6'(X_31) | '#skF_7'(X_31)='#skF_10'(X_31) | '#skF_7'(X_31)='#skF_6'(X_31) | Y0_237='#skF_10'(X_31) | Y0_237='#skF_6'(X_31) | Y0_237='#skF_7'(X_31) | ~rr(X_31, Y0_237) | ~cSatisfiable(X_31)))).
% 7.16/2.60 tff(c_305, plain, (![X_31, Y1_131, Y0_132]: ('#skF_10'(X_31)='#skF_6'(X_31) | Y1_131='#skF_10'(X_31) | Y1_131='#skF_6'(X_31) | Y0_132='#skF_10'(X_31) | Y0_132='#skF_6'(X_31) | Y1_131=Y0_132 | ~rr(X_31, Y1_131) | ~rr(X_31, Y0_132) | ~cSatisfiable(X_31)))).
% 7.16/2.60 tff(c_80, plain, (![Y_57, Y_53, Y_54, Y_55, X_31, Y_56, Y_52]: (rr(X_31, '#skF_4'(X_31)) | cSatisfiable(X_31) | ~cp1(Y_57) | ~rr(X_31, Y_57) | ~cp1(Y_56) | ~cp(Y_56) | ~rr(X_31, Y_56) | ~cp(Y_55) | ~cp2(Y_55) | ~rr(X_31, Y_55) | ~cp2(Y_54) | ~rr(X_31, Y_54) | ~cp(Y_53) | ~cp3(Y_53) | ~rr(X_31, Y_53) | ~cp3(Y_52) | ~rr(X_31, Y_52)))).
% 7.16/2.60 tff(c_68, plain, (![Y_57, Y_53, Y_54, Y_55, X_31, Y_56, Y_52]: ('#skF_4'(X_31)!='#skF_3'(X_31) | cSatisfiable(X_31) | ~cp1(Y_57) | ~rr(X_31, Y_57) | ~cp1(Y_56) | ~cp(Y_56) | ~rr(X_31, Y_56) | ~cp(Y_55) | ~cp2(Y_55) | ~rr(X_31, Y_55) | ~cp2(Y_54) | ~rr(X_31, Y_54) | ~cp(Y_53) | ~cp3(Y_53) | ~rr(X_31, Y_53) | ~cp3(Y_52) | ~rr(X_31, Y_52)))).
% 7.16/2.60 tff(c_72, plain, (![Y_57, Y_53, Y_54, Y_55, X_31, Y_56, Y_52]: ('#skF_2'(X_31)!='#skF_3'(X_31) | cSatisfiable(X_31) | ~cp1(Y_57) | ~rr(X_31, Y_57) | ~cp1(Y_56) | ~cp(Y_56) | ~rr(X_31, Y_56) | ~cp(Y_55) | ~cp2(Y_55) | ~rr(X_31, Y_55) | ~cp2(Y_54) | ~rr(X_31, Y_54) | ~cp(Y_53) | ~cp3(Y_53) | ~rr(X_31, Y_53) | ~cp3(Y_52) | ~rr(X_31, Y_52)))).
% 7.16/2.60 tff(c_285, plain, (![X_31, Y1_127, Y0_128]: ('#skF_8'(X_31)='#skF_6'(X_31) | Y1_127='#skF_8'(X_31) | Y1_127='#skF_6'(X_31) | Y0_128='#skF_8'(X_31) | Y0_128='#skF_6'(X_31) | Y1_127=Y0_128 | ~rr(X_31, Y1_127) | ~rr(X_31, Y0_128) | ~cSatisfiable(X_31)))).
% 7.16/2.60 tff(c_78, plain, (![Y_57, Y_53, Y_54, Y_55, X_31, Y_56, Y_52]: ('#skF_2'(X_31)!='#skF_1'(X_31) | cSatisfiable(X_31) | ~cp1(Y_57) | ~rr(X_31, Y_57) | ~cp1(Y_56) | ~cp(Y_56) | ~rr(X_31, Y_56) | ~cp(Y_55) | ~cp2(Y_55) | ~rr(X_31, Y_55) | ~cp2(Y_54) | ~rr(X_31, Y_54) | ~cp(Y_53) | ~cp3(Y_53) | ~rr(X_31, Y_53) | ~cp3(Y_52) | ~rr(X_31, Y_52)))).
% 7.16/2.60 tff(c_226, plain, (![X_31, Y1_112, Y0_113]: ('#skF_7'(X_31)='#skF_6'(X_31) | Y1_112='#skF_7'(X_31) | Y1_112='#skF_6'(X_31) | Y0_113='#skF_7'(X_31) | Y0_113='#skF_6'(X_31) | Y1_112=Y0_113 | ~rr(X_31, Y1_112) | ~rr(X_31, Y0_113) | ~cSatisfiable(X_31)))).
% 7.16/2.60 tff(c_304, plain, (![X_31, Y1_131, Y0_132]: ('#skF_9'(X_31)='#skF_10'(X_31) | Y1_131='#skF_10'(X_31) | Y1_131='#skF_9'(X_31) | Y0_132='#skF_10'(X_31) | Y0_132='#skF_9'(X_31) | Y1_131=Y0_132 | ~rr(X_31, Y1_131) | ~rr(X_31, Y0_132) | ~cSatisfiable(X_31)))).
% 7.16/2.60 tff(c_208, plain, (![X_31, Y1_108, Y0_109]: ('#skF_5'(X_31)='#skF_10'(X_31) | Y1_108='#skF_5'(X_31) | Y1_108='#skF_10'(X_31) | Y0_109='#skF_5'(X_31) | Y0_109='#skF_10'(X_31) | Y1_108=Y0_109 | ~rr(X_31, Y1_108) | ~rr(X_31, Y0_109) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_209, plain, (![X_31, Y1_108, Y0_109]: ('#skF_5'(X_31)='#skF_8'(X_31) | Y1_108='#skF_5'(X_31) | Y1_108='#skF_8'(X_31) | Y0_109='#skF_5'(X_31) | Y0_109='#skF_8'(X_31) | Y1_108=Y0_109 | ~rr(X_31, Y1_108) | ~rr(X_31, Y0_109) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_70, plain, (![Y_57, Y_53, Y_54, Y_55, X_31, Y_56, Y_52]: ('#skF_2'(X_31)!='#skF_4'(X_31) | cSatisfiable(X_31) | ~cp1(Y_57) | ~rr(X_31, Y_57) | ~cp1(Y_56) | ~cp(Y_56) | ~rr(X_31, Y_56) | ~cp(Y_55) | ~cp2(Y_55) | ~rr(X_31, Y_55) | ~cp2(Y_54) | ~rr(X_31, Y_54) | ~cp(Y_53) | ~cp3(Y_53) | ~rr(X_31, Y_53) | ~cp3(Y_52) | ~rr(X_31, Y_52)))).
% 7.16/2.61 tff(c_324, plain, (![X_31, Y1_135, Y0_136]: ('#skF_9'(X_31)='#skF_6'(X_31) | Y1_135='#skF_6'(X_31) | Y1_135='#skF_9'(X_31) | Y0_136='#skF_6'(X_31) | Y0_136='#skF_9'(X_31) | Y1_135=Y0_136 | ~rr(X_31, Y1_135) | ~rr(X_31, Y0_136) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_225, plain, (![X_31, Y1_112, Y0_113]: ('#skF_9'(X_31)='#skF_7'(X_31) | Y1_112='#skF_7'(X_31) | Y1_112='#skF_9'(X_31) | Y0_113='#skF_7'(X_31) | Y0_113='#skF_9'(X_31) | Y1_112=Y0_113 | ~rr(X_31, Y1_112) | ~rr(X_31, Y0_113) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_84, plain, (![Y_57, Y_53, Y_54, Y_55, X_31, Y_56, Y_52]: (rr(X_31, '#skF_2'(X_31)) | cSatisfiable(X_31) | ~cp1(Y_57) | ~rr(X_31, Y_57) | ~cp1(Y_56) | ~cp(Y_56) | ~rr(X_31, Y_56) | ~cp(Y_55) | ~cp2(Y_55) | ~rr(X_31, Y_55) | ~cp2(Y_54) | ~rr(X_31, Y_54) | ~cp(Y_53) | ~cp3(Y_53) | ~rr(X_31, Y_53) | ~cp3(Y_52) | ~rr(X_31, Y_52)))).
% 7.16/2.61 tff(c_289, plain, (![X_31, Y1_127, Y0_128]: ('#skF_7'(X_31)='#skF_8'(X_31) | Y1_127='#skF_8'(X_31) | Y1_127='#skF_7'(X_31) | Y0_128='#skF_8'(X_31) | Y0_128='#skF_7'(X_31) | Y1_127=Y0_128 | ~rr(X_31, Y1_127) | ~rr(X_31, Y0_128) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_263, plain, (![X_31, Y1_123, Y0_124]: ('#skF_9'(X_31)='#skF_5'(X_31) | Y1_123='#skF_9'(X_31) | Y1_123='#skF_5'(X_31) | Y0_124='#skF_9'(X_31) | Y0_124='#skF_5'(X_31) | Y1_123=Y0_124 | ~rr(X_31, Y1_123) | ~rr(X_31, Y0_124) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_308, plain, (![X_31, Y1_131, Y0_132]: ('#skF_8'(X_31)='#skF_10'(X_31) | Y1_131='#skF_10'(X_31) | Y1_131='#skF_8'(X_31) | Y0_132='#skF_10'(X_31) | Y0_132='#skF_8'(X_31) | Y1_131=Y0_132 | ~rr(X_31, Y1_131) | ~rr(X_31, Y0_132) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_268, plain, (![X_31, Y1_123, Y0_124]: ('#skF_9'(X_31)='#skF_8'(X_31) | Y1_123='#skF_9'(X_31) | Y1_123='#skF_8'(X_31) | Y0_124='#skF_9'(X_31) | Y0_124='#skF_8'(X_31) | Y1_123=Y0_124 | ~rr(X_31, Y1_123) | ~rr(X_31, Y0_124) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_82, plain, (![Y_57, Y_53, Y_54, Y_55, X_31, Y_56, Y_52]: (rr(X_31, '#skF_3'(X_31)) | cSatisfiable(X_31) | ~cp1(Y_57) | ~rr(X_31, Y_57) | ~cp1(Y_56) | ~cp(Y_56) | ~rr(X_31, Y_56) | ~cp(Y_55) | ~cp2(Y_55) | ~rr(X_31, Y_55) | ~cp2(Y_54) | ~rr(X_31, Y_54) | ~cp(Y_53) | ~cp3(Y_53) | ~rr(X_31, Y_53) | ~cp3(Y_52) | ~rr(X_31, Y_52)))).
% 7.16/2.61 tff(c_207, plain, (![X_31, Y1_108, Y0_109]: ('#skF_5'(X_31)='#skF_6'(X_31) | Y1_108='#skF_5'(X_31) | Y1_108='#skF_6'(X_31) | Y0_109='#skF_5'(X_31) | Y0_109='#skF_6'(X_31) | Y1_108=Y0_109 | ~rr(X_31, Y1_108) | ~rr(X_31, Y0_109) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_224, plain, (![X_31, Y1_112, Y0_113]: ('#skF_7'(X_31)='#skF_5'(X_31) | Y1_112='#skF_7'(X_31) | Y1_112='#skF_5'(X_31) | Y0_113='#skF_7'(X_31) | Y0_113='#skF_5'(X_31) | Y1_112=Y0_113 | ~rr(X_31, Y1_112) | ~rr(X_31, Y0_113) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_74, plain, (![Y_57, Y_53, Y_54, Y_55, X_31, Y_56, Y_52]: ('#skF_4'(X_31)!='#skF_1'(X_31) | cSatisfiable(X_31) | ~cp1(Y_57) | ~rr(X_31, Y_57) | ~cp1(Y_56) | ~cp(Y_56) | ~rr(X_31, Y_56) | ~cp(Y_55) | ~cp2(Y_55) | ~rr(X_31, Y_55) | ~cp2(Y_54) | ~rr(X_31, Y_54) | ~cp(Y_53) | ~cp3(Y_53) | ~rr(X_31, Y_53) | ~cp3(Y_52) | ~rr(X_31, Y_52)))).
% 7.16/2.61 tff(c_309, plain, (![X_31, Y1_131, Y0_132]: ('#skF_7'(X_31)='#skF_10'(X_31) | Y1_131='#skF_10'(X_31) | Y1_131='#skF_7'(X_31) | Y0_132='#skF_10'(X_31) | Y0_132='#skF_7'(X_31) | Y1_131=Y0_132 | ~rr(X_31, Y1_131) | ~rr(X_31, Y0_132) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_187, plain, (![Y2_101, X_31, Y1_103, Y0_105]: (Y2_101='#skF_6'(X_31) | Y1_103='#skF_6'(X_31) | Y2_101=Y1_103 | Y0_105='#skF_6'(X_31) | Y2_101=Y0_105 | Y1_103=Y0_105 | ~rr(X_31, Y2_101) | ~rr(X_31, Y1_103) | ~rr(X_31, Y0_105) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_188, plain, (![Y2_101, X_31, Y1_103, Y0_105]: (Y2_101='#skF_10'(X_31) | Y1_103='#skF_10'(X_31) | Y2_101=Y1_103 | Y0_105='#skF_10'(X_31) | Y2_101=Y0_105 | Y1_103=Y0_105 | ~rr(X_31, Y2_101) | ~rr(X_31, Y1_103) | ~rr(X_31, Y0_105) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_189, plain, (![Y2_101, X_31, Y1_103, Y0_105]: (Y2_101='#skF_8'(X_31) | Y1_103='#skF_8'(X_31) | Y2_101=Y1_103 | Y0_105='#skF_8'(X_31) | Y2_101=Y0_105 | Y1_103=Y0_105 | ~rr(X_31, Y2_101) | ~rr(X_31, Y1_103) | ~rr(X_31, Y0_105) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_186, plain, (![Y2_101, X_31, Y1_103, Y0_105]: (Y2_101='#skF_9'(X_31) | Y1_103='#skF_9'(X_31) | Y2_101=Y1_103 | Y0_105='#skF_9'(X_31) | Y2_101=Y0_105 | Y1_103=Y0_105 | ~rr(X_31, Y2_101) | ~rr(X_31, Y1_103) | ~rr(X_31, Y0_105) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_86, plain, (![Y_57, Y_53, Y_54, Y_55, X_31, Y_56, Y_52]: (rr(X_31, '#skF_1'(X_31)) | cSatisfiable(X_31) | ~cp1(Y_57) | ~rr(X_31, Y_57) | ~cp1(Y_56) | ~cp(Y_56) | ~rr(X_31, Y_56) | ~cp(Y_55) | ~cp2(Y_55) | ~rr(X_31, Y_55) | ~cp2(Y_54) | ~rr(X_31, Y_54) | ~cp(Y_53) | ~cp3(Y_53) | ~rr(X_31, Y_53) | ~cp3(Y_52) | ~rr(X_31, Y_52)))).
% 7.16/2.61 tff(c_190, plain, (![Y2_101, X_31, Y1_103, Y0_105]: (Y2_101='#skF_7'(X_31) | Y1_103='#skF_7'(X_31) | Y2_101=Y1_103 | Y0_105='#skF_7'(X_31) | Y2_101=Y0_105 | Y1_103=Y0_105 | ~rr(X_31, Y2_101) | ~rr(X_31, Y1_103) | ~rr(X_31, Y0_105) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_185, plain, (![Y2_101, X_31, Y1_103, Y0_105]: (Y2_101='#skF_5'(X_31) | Y1_103='#skF_5'(X_31) | Y2_101=Y1_103 | Y0_105='#skF_5'(X_31) | Y2_101=Y0_105 | Y1_103=Y0_105 | ~rr(X_31, Y2_101) | ~rr(X_31, Y1_103) | ~rr(X_31, Y0_105) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_62, plain, (![Y2_60, Y3_61, Y0_58, X_31, Y1_59]: (Y3_61=Y2_60 | Y3_61=Y1_59 | Y2_60=Y1_59 | Y3_61=Y0_58 | Y2_60=Y0_58 | Y1_59=Y0_58 | ~rr(X_31, Y3_61) | ~rr(X_31, Y2_60) | ~rr(X_31, Y1_59) | ~rr(X_31, Y0_58) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_66, plain, (![X_31]: (rr(X_31, '#skF_5'(X_31)) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_44, plain, (![X_31]: (rr(X_31, '#skF_9'(X_31)) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_60, plain, (![X_31]: (rr(X_31, '#skF_6'(X_31)) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_38, plain, (![X_31]: (rr(X_31, '#skF_10'(X_31)) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_158, plain, (![X_88]: (~cp2('#skF_5'(X_88)) | ~cSatisfiable(X_88)))).
% 7.16/2.61 tff(c_159, plain, (![X_88]: (~cp1('#skF_5'(X_88)) | ~cSatisfiable(X_88)))).
% 7.16/2.61 tff(c_50, plain, (![X_31]: (rr(X_31, '#skF_8'(X_31)) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_146, plain, (![X_84]: (~cp2('#skF_6'(X_84)) | ~cSatisfiable(X_84)))).
% 7.16/2.61 tff(c_147, plain, (![X_84]: (~cp1('#skF_6'(X_84)) | ~cSatisfiable(X_84)))).
% 7.16/2.61 tff(c_137, plain, (![X_82]: (~cp1('#skF_7'(X_82)) | ~cSatisfiable(X_82)))).
% 7.16/2.61 tff(c_54, plain, (![X_31]: (rr(X_31, '#skF_7'(X_31)) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_132, plain, (![X_81]: (~cp1('#skF_8'(X_81)) | ~cSatisfiable(X_81)))).
% 7.16/2.61 tff(c_64, plain, (![X_31]: (cp3('#skF_5'(X_31)) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_36, plain, (![X_31]: (cp1('#skF_10'(X_31)) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_40, plain, (![X_31]: (cp1('#skF_9'(X_31)) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_42, plain, (![X_31]: (cp('#skF_9'(X_31)) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_58, plain, (![X_31]: (cp3('#skF_6'(X_31)) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_56, plain, (![X_31]: (cp('#skF_6'(X_31)) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_52, plain, (![X_31]: (cp2('#skF_7'(X_31)) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_48, plain, (![X_31]: (cp2('#skF_8'(X_31)) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_46, plain, (![X_31]: (cp('#skF_8'(X_31)) | ~cSatisfiable(X_31)))).
% 7.16/2.61 tff(c_100, plain, (![X_63]: (~cp4(X_63) | ~cp2(X_63)))).
% 7.16/2.61 tff(c_98, plain, (![X_63]: (~cp3(X_63) | ~cp2(X_63)))).
% 7.16/2.61 tff(c_104, plain, (![X_64]: (~cp4(X_64) | ~cp3(X_64)))).
% 7.16/2.61 tff(c_96, plain, (![X_63]: (~cp5(X_63) | ~cp2(X_63)))).
% 7.16/2.61 tff(c_88, plain, (![X_62]: (~cp2(X_62) | ~cp1(X_62)))).
% 7.16/2.61 tff(c_92, plain, (![X_62]: (~cp3(X_62) | ~cp1(X_62)))).
% 7.16/2.61 tff(c_34, plain, (![X_30]: (xsd_string(X_30) | xsd_integer(X_30)))).
% 7.16/2.61 tff(c_90, plain, (![X_62]: (~cp5(X_62) | ~cp1(X_62)))).
% 7.16/2.61 tff(c_106, plain, (![X_65]: (~cp5(X_65) | ~cp4(X_65)))).
% 7.16/2.61 tff(c_94, plain, (![X_62]: (~cp4(X_62) | ~cp1(X_62)))).
% 7.16/2.61 tff(c_102, plain, (![X_64]: (~cp5(X_64) | ~cp3(X_64)))).
% 7.16/2.61 tff(c_32, plain, (![X_30]: (~xsd_integer(X_30) | ~xsd_string(X_30)))).
% 7.16/2.61 tff(c_28, plain, (![X_29]: (cowlThing(X_29)))).
% 7.16/2.61 tff(c_30, plain, (![X_29]: (~cowlNothing(X_29)))).
% 7.16/2.61 tff(c_108, plain, (cSatisfiable(i2003_11_14_17_15_33836))).
% 7.16/2.61 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 7.16/2.61
%------------------------------------------------------------------------------