%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYO579+1 : TPTP v9.0.0. Released v5.5.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 : n012.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 10:37:52 PM UTC 2025
% Result : CounterSatisfiable 8.77s 3.07s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.11 % Problem : SYO579+1 : TPTP v9.0.0. Released v5.5.0.
% 0.11/0.12 % 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.12/0.33 % Computer : n012.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed Apr 9 09:21:59 EDT 2025
% 0.12/0.33 % CPUTime :
% 8.77/3.07
% 8.77/3.07 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.77/3.07
% 8.77/3.07 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 8.77/3.08 %$ k04_buttercup10622 > k04_buttercup10620 > k04_buttercup10619 > k04_buttercup10100 > b48_buttercup10111 > b48_buttercup10110 > b48_buttercup10109 > b48_buttercup10108 > b48_buttercup10107 > b48_buttercup10104 > b48_buttercup10102 > b48_buttercup10098 > #nlpp > #skF_33 > #skF_41 > #skF_52 > #skF_49 > #skF_20 > #skF_18 > #skF_17 > #skF_11 > #skF_31 > #skF_15 > #skF_25 > #skF_55 > #skF_38 > #skF_36 > #skF_56 > #skF_54 > #skF_43 > #skF_19 > #skF_40 > #skF_48 > #skF_7 > #skF_37 > #skF_10 > #skF_16 > #skF_47 > #skF_26 > #skF_53 > #skF_14 > #skF_51 > #skF_5 > #skF_45 > #skF_46 > #skF_39 > #skF_6 > #skF_13 > #skF_2 > #skF_3 > #skF_1 > #skF_21 > #skF_9 > #skF_32 > #skF_50 > #skF_8 > #skF_30 > #skF_42 > #skF_4 > #skF_22 > #skF_29 > #skF_28 > #skF_35 > #skF_24 > #skF_27 > #skF_23 > #skF_44 > #skF_12 > #skF_34
% 8.77/3.08
% 8.77/3.08 %Foreground sorts:
% 8.77/3.08
% 8.77/3.08
% 8.77/3.08 %Background operators:
% 8.77/3.08
% 8.77/3.08
% 8.77/3.08 %Foreground operators:
% 8.77/3.08 tff(b48_buttercup10110, type, b48_buttercup10110: $i > $o).
% 8.77/3.08 tff('#skF_33', type, '#skF_33': $i).
% 8.77/3.08 tff('#skF_41', type, '#skF_41': $i).
% 8.77/3.08 tff('#skF_52', type, '#skF_52': $i).
% 8.77/3.08 tff(k04_buttercup10622, type, k04_buttercup10622: $i > $o).
% 8.77/3.08 tff('#skF_49', type, '#skF_49': $i).
% 8.77/3.08 tff('#skF_20', type, '#skF_20': $i).
% 8.77/3.08 tff('#skF_18', type, '#skF_18': $i).
% 8.77/3.08 tff('#skF_17', type, '#skF_17': $i).
% 8.77/3.08 tff('#skF_11', type, '#skF_11': $i).
% 8.77/3.08 tff('#skF_31', type, '#skF_31': $i).
% 8.77/3.08 tff('#skF_15', type, '#skF_15': $i).
% 8.77/3.08 tff('#skF_25', type, '#skF_25': $i).
% 8.77/3.08 tff(b48_buttercup10102, type, b48_buttercup10102: $i > $o).
% 8.77/3.08 tff('#skF_55', type, '#skF_55': $i).
% 8.77/3.08 tff(k04_buttercup10100, type, k04_buttercup10100: $i > $o).
% 8.77/3.08 tff('#skF_38', type, '#skF_38': $i).
% 8.77/3.08 tff('#skF_36', type, '#skF_36': $i).
% 8.77/3.08 tff('#skF_56', type, '#skF_56': $i).
% 8.77/3.08 tff('#skF_54', type, '#skF_54': $i).
% 8.77/3.08 tff('#skF_43', type, '#skF_43': $i).
% 8.77/3.08 tff('#skF_19', type, '#skF_19': $i).
% 8.77/3.08 tff('#skF_40', type, '#skF_40': $i).
% 8.77/3.08 tff(b48_buttercup10108, type, b48_buttercup10108: $i > $o).
% 8.77/3.08 tff('#skF_48', type, '#skF_48': $i).
% 8.77/3.08 tff('#skF_7', type, '#skF_7': $i).
% 8.77/3.08 tff('#skF_37', type, '#skF_37': $i).
% 8.77/3.08 tff('#skF_10', type, '#skF_10': $i).
% 8.77/3.08 tff('#skF_16', type, '#skF_16': $i).
% 8.77/3.08 tff('#skF_47', type, '#skF_47': $i).
% 8.77/3.08 tff(k04_buttercup10619, type, k04_buttercup10619: $i > $o).
% 8.77/3.08 tff('#skF_26', type, '#skF_26': $i).
% 8.77/3.08 tff(b48_buttercup10107, type, b48_buttercup10107: $i > $o).
% 8.77/3.08 tff('#skF_53', type, '#skF_53': $i).
% 8.77/3.08 tff('#skF_14', type, '#skF_14': $i).
% 8.77/3.08 tff('#skF_51', type, '#skF_51': $i).
% 8.77/3.08 tff('#skF_5', type, '#skF_5': $i).
% 8.77/3.08 tff('#skF_45', type, '#skF_45': $i).
% 8.77/3.08 tff('#skF_46', type, '#skF_46': $i).
% 8.77/3.08 tff('#skF_39', type, '#skF_39': $i).
% 8.77/3.08 tff(b48_buttercup10104, type, b48_buttercup10104: $i > $o).
% 8.77/3.08 tff(b48_buttercup10111, type, b48_buttercup10111: $i > $o).
% 8.77/3.08 tff('#skF_6', type, '#skF_6': $i).
% 8.77/3.08 tff('#skF_13', type, '#skF_13': $i).
% 8.77/3.08 tff('#skF_2', type, '#skF_2': $i).
% 8.77/3.08 tff('#skF_3', type, '#skF_3': $i).
% 8.77/3.08 tff('#skF_1', type, '#skF_1': $i).
% 8.77/3.08 tff(b48_buttercup10098, type, b48_buttercup10098: $i > $o).
% 8.77/3.08 tff(b48_buttercup10109, type, b48_buttercup10109: $i > $o).
% 8.77/3.08 tff('#skF_21', type, '#skF_21': $i).
% 8.77/3.08 tff('#skF_9', type, '#skF_9': $i).
% 8.77/3.08 tff('#skF_32', type, '#skF_32': $i).
% 8.77/3.08 tff('#skF_50', type, '#skF_50': $i).
% 8.77/3.08 tff('#skF_8', type, '#skF_8': $i).
% 8.77/3.08 tff('#skF_30', type, '#skF_30': $i).
% 8.77/3.08 tff('#skF_42', type, '#skF_42': $i).
% 8.77/3.08 tff('#skF_4', type, '#skF_4': $i).
% 8.77/3.08 tff('#skF_22', type, '#skF_22': $i).
% 8.77/3.08 tff('#skF_29', type, '#skF_29': $i).
% 8.77/3.08 tff('#skF_28', type, '#skF_28': $i).
% 8.77/3.08 tff('#skF_35', type, '#skF_35': $i).
% 8.77/3.08 tff('#skF_24', type, '#skF_24': $i).
% 8.77/3.08 tff('#skF_27', type, '#skF_27': $i).
% 8.77/3.08 tff('#skF_23', type, '#skF_23': $i).
% 8.77/3.08 tff('#skF_44', type, '#skF_44': $i).
% 8.77/3.08 tff(k04_buttercup10620, type, k04_buttercup10620: $i > $o).
% 8.77/3.08 tff('#skF_12', type, '#skF_12': $i).
% 8.77/3.08 tff('#skF_34', type, '#skF_34': $i).
% 8.77/3.08
% 8.77/3.08 %Saturated clause set:
% 8.77/3.08 tff(c_1895, plain, (b48_buttercup10102('#skF_45'))).
% 8.77/3.08 tff(c_1889, plain, (b48_buttercup10102('#skF_32'))).
% 8.77/3.08 tff(c_1882, plain, (b48_buttercup10102('#skF_47'))).
% 8.77/3.08 tff(c_1883, plain, (~b48_buttercup10098('#skF_10'))).
% 8.77/3.08 tff(c_1875, plain, (b48_buttercup10102('#skF_31'))).
% 8.77/3.08 tff(c_1876, plain, (~b48_buttercup10098('#skF_8'))).
% 8.77/3.09 tff(c_1869, plain, (b48_buttercup10102('#skF_30'))).
% 8.77/3.09 tff(c_1854, plain, (b48_buttercup10102('#skF_29'))).
% 8.77/3.09 tff(c_1853, plain, (b48_buttercup10104('#skF_38'))).
% 8.77/3.09 tff(c_1831, plain, (b48_buttercup10109('#skF_18'))).
% 8.77/3.09 tff(c_946, plain, (![X141_87]: (b48_buttercup10111(X141_87) | b48_buttercup10110(X141_87) | b48_buttercup10109(X141_87) | b48_buttercup10108(X141_87) | b48_buttercup10107(X141_87) | b48_buttercup10104(X141_87) | b48_buttercup10102(X141_87) | ~b48_buttercup10098(X141_87)))).
% 8.77/3.09 tff(c_1682, plain, (![X26_16]: (~b48_buttercup10111(X26_16) | ~k04_buttercup10619(X26_16)))).
% 8.77/3.09 tff(c_1681, plain, (~b48_buttercup10111('#skF_8'))).
% 8.77/3.09 tff(c_1680, plain, (~b48_buttercup10111('#skF_10'))).
% 8.77/3.09 tff(c_1630, plain, (![X36_20]: (~b48_buttercup10109(X36_20) | ~k04_buttercup10619(X36_20)))).
% 8.77/3.09 tff(c_1629, plain, (~b48_buttercup10107('#skF_56'))).
% 8.77/3.09 tff(c_1628, plain, (~b48_buttercup10107('#skF_18'))).
% 8.77/3.09 tff(c_1627, plain, (~b48_buttercup10107('#skF_6'))).
% 8.77/3.09 tff(c_1626, plain, (~b48_buttercup10107('#skF_44'))).
% 8.77/3.09 tff(c_1391, plain, (![X73_131]: (~k04_buttercup10100(X73_131) | ~b48_buttercup10107(X73_131)))).
% 8.77/3.09 tff(c_1603, plain, (~b48_buttercup10108('#skF_56'))).
% 9.20/3.09 tff(c_1602, plain, (~b48_buttercup10108('#skF_18'))).
% 9.20/3.09 tff(c_1604, plain, (~b48_buttercup10107('#skF_40'))).
% 9.20/3.09 tff(c_1601, plain, (~b48_buttercup10108('#skF_6'))).
% 9.20/3.09 tff(c_1600, plain, (~b48_buttercup10108('#skF_44'))).
% 9.20/3.09 tff(c_1466, plain, (![X59_136]: (~k04_buttercup10100(X59_136) | ~b48_buttercup10108(X59_136)))).
% 9.20/3.09 tff(c_1577, plain, (~b48_buttercup10110('#skF_18'))).
% 9.20/3.09 tff(c_1576, plain, (~b48_buttercup10110('#skF_6'))).
% 9.20/3.09 tff(c_1578, plain, (~b48_buttercup10110('#skF_56'))).
% 9.20/3.09 tff(c_1575, plain, (~b48_buttercup10110('#skF_44'))).
% 9.20/3.09 tff(c_1423, plain, (![X57_133]: (~k04_buttercup10100(X57_133) | ~b48_buttercup10110(X57_133)))).
% 9.20/3.09 tff(c_1553, plain, (~b48_buttercup10104('#skF_56'))).
% 9.20/3.09 tff(c_1552, plain, (~b48_buttercup10104('#skF_18'))).
% 9.20/3.09 tff(c_1551, plain, (~b48_buttercup10104('#skF_6'))).
% 9.20/3.09 tff(c_1550, plain, (~b48_buttercup10104('#skF_44'))).
% 9.20/3.09 tff(c_1449, plain, (![X55_135]: (~k04_buttercup10100(X55_135) | ~b48_buttercup10104(X55_135)))).
% 9.20/3.09 tff(c_1526, plain, (~b48_buttercup10102('#skF_6'))).
% 9.20/3.09 tff(c_1527, plain, (~b48_buttercup10102('#skF_18'))).
% 9.20/3.09 tff(c_1528, plain, (~b48_buttercup10102('#skF_56'))).
% 9.20/3.09 tff(c_1525, plain, (~b48_buttercup10102('#skF_44'))).
% 9.20/3.09 tff(c_1493, plain, (![X71_138]: (~k04_buttercup10100(X71_138) | ~b48_buttercup10102(X71_138)))).
% 9.20/3.09 tff(c_1503, plain, (~b48_buttercup10108('#skF_46'))).
% 9.20/3.09 tff(c_1097, plain, (![X59_30]: (~k04_buttercup10620(X59_30) | ~b48_buttercup10108(X59_30)))).
% 9.20/3.09 tff(c_1491, plain, (~b48_buttercup10102('#skF_11'))).
% 9.20/3.09 tff(c_1494, plain, (~b48_buttercup10102('#skF_12'))).
% 9.20/3.09 tff(c_1285, plain, (![X71_124]: (k04_buttercup10619(X71_124) | ~b48_buttercup10102(X71_124)))).
% 9.20/3.09 tff(c_1476, plain, (~b48_buttercup10110('#skF_46'))).
% 9.20/3.09 tff(c_1477, plain, (~b48_buttercup10104('#skF_4'))).
% 9.20/3.09 tff(c_1261, plain, (![X57_121]: (~k04_buttercup10620(X57_121) | ~b48_buttercup10110(X57_121)))).
% 9.20/3.09 tff(c_1464, plain, (~b48_buttercup10108('#skF_11'))).
% 9.20/3.09 tff(c_1467, plain, (~b48_buttercup10108('#skF_12'))).
% 9.20/3.09 tff(c_1077, plain, (![X59_105]: (k04_buttercup10619(X59_105) | ~b48_buttercup10108(X59_105)))).
% 9.20/3.09 tff(c_1447, plain, (~b48_buttercup10104('#skF_11'))).
% 9.20/3.09 tff(c_1450, plain, (~b48_buttercup10104('#skF_12'))).
% 9.20/3.09 tff(c_1271, plain, (![X55_122]: (k04_buttercup10619(X55_122) | ~b48_buttercup10104(X55_122)))).
% 9.20/3.09 tff(c_1284, plain, (![X71_124]: (~k04_buttercup10620(X71_124) | ~b48_buttercup10102(X71_124)))).
% 9.20/3.09 tff(c_1421, plain, (~b48_buttercup10110('#skF_11'))).
% 9.20/3.09 tff(c_1424, plain, (~b48_buttercup10110('#skF_12'))).
% 9.20/3.09 tff(c_1262, plain, (![X57_121]: (k04_buttercup10619(X57_121) | ~b48_buttercup10110(X57_121)))).
% 9.20/3.09 tff(c_1270, plain, (![X55_122]: (~k04_buttercup10620(X55_122) | ~b48_buttercup10104(X55_122)))).
% 9.20/3.09 tff(c_1398, plain, (~b48_buttercup10110('#skF_27'))).
% 9.20/3.09 tff(c_1397, plain, (~b48_buttercup10107('#skF_11'))).
% 9.20/3.09 tff(c_1393, plain, (~k04_buttercup10619('#skF_11'))).
% 9.20/3.09 tff(c_1392, plain, (~b48_buttercup10107('#skF_12'))).
% 9.20/3.09 tff(c_1360, plain, (![X73_127]: (k04_buttercup10619(X73_127) | ~b48_buttercup10107(X73_127)))).
% 9.20/3.09 tff(c_1326, plain, (~b48_buttercup10109('#skF_31'))).
% 9.20/3.09 tff(c_1324, plain, (~b48_buttercup10109('#skF_29'))).
% 9.20/3.09 tff(c_1327, plain, (~b48_buttercup10109('#skF_47'))).
% 9.20/3.09 tff(c_944, plain, (![X140_86]: (k04_buttercup10622(X140_86) | k04_buttercup10620(X140_86) | ~k04_buttercup10619(X140_86)))).
% 9.20/3.09 tff(c_1328, plain, (~b48_buttercup10109('#skF_38'))).
% 9.20/3.09 tff(c_1323, plain, (~b48_buttercup10109('#skF_46'))).
% 9.20/3.09 tff(c_1370, plain, (~b48_buttercup10107('#skF_54'))).
% 9.20/3.09 tff(c_900, plain, (![X118_64]: (~b48_buttercup10107(X118_64) | ~b48_buttercup10108(X118_64)))).
% 9.20/3.09 tff(c_1325, plain, (~b48_buttercup10109('#skF_30'))).
% 9.20/3.10 tff(c_1357, plain, (~b48_buttercup10107('#skF_30'))).
% 9.20/3.10 tff(c_1358, plain, (~b48_buttercup10107('#skF_29'))).
% 9.20/3.10 tff(c_1356, plain, (~b48_buttercup10107('#skF_31'))).
% 9.20/3.10 tff(c_1365, plain, (b48_buttercup10098('#skF_50'))).
% 9.20/3.10 tff(c_16, plain, (![X7_8]: (b48_buttercup10098(X7_8) | ~b48_buttercup10110(X7_8)))).
% 9.20/3.10 tff(c_1355, plain, (~b48_buttercup10107('#skF_47'))).
% 9.20/3.10 tff(c_1354, plain, (~b48_buttercup10107('#skF_38'))).
% 9.20/3.10 tff(c_1329, plain, (~b48_buttercup10109('#skF_45'))).
% 9.20/3.10 tff(c_718, plain, (![X73_36]: (k04_buttercup10620(X73_36) | ~b48_buttercup10107(X73_36)))).
% 9.20/3.10 tff(c_1331, plain, (~b48_buttercup10109('#skF_32'))).
% 9.20/3.10 tff(c_132, plain, (![X17_13]: (k04_buttercup10100(X17_13) | ~b48_buttercup10109(X17_13)))).
% 9.20/3.10 tff(c_1293, plain, (~b48_buttercup10104('#skF_46'))).
% 9.20/3.10 tff(c_1294, plain, (~b48_buttercup10104('#skF_53'))).
% 9.24/3.10 tff(c_886, plain, (![X111_57]: (~b48_buttercup10104(X111_57) | ~b48_buttercup10107(X111_57)))).
% 9.24/3.10 tff(c_714, plain, (![X71_35]: (k04_buttercup10622(X71_35) | ~b48_buttercup10102(X71_35)))).
% 9.24/3.10 tff(c_1276, plain, (~b48_buttercup10102('#skF_54'))).
% 9.24/3.10 tff(c_896, plain, (![X116_62]: (~b48_buttercup10102(X116_62) | ~b48_buttercup10108(X116_62)))).
% 9.24/3.10 tff(c_582, plain, (![X55_28]: (k04_buttercup10622(X55_28) | ~b48_buttercup10104(X55_28)))).
% 9.24/3.10 tff(c_588, plain, (![X57_29]: (k04_buttercup10622(X57_29) | ~b48_buttercup10110(X57_29)))).
% 9.24/3.10 tff(c_1253, plain, (b48_buttercup10098('#skF_49'))).
% 9.24/3.10 tff(c_18, plain, (![X8_9]: (b48_buttercup10098(X8_9) | ~b48_buttercup10111(X8_9)))).
% 9.24/3.10 tff(c_1248, plain, (~b48_buttercup10110('#skF_49'))).
% 9.24/3.10 tff(c_942, plain, (![X139_85]: (~b48_buttercup10110(X139_85) | ~b48_buttercup10111(X139_85)))).
% 9.24/3.10 tff(c_1243, plain, (~b48_buttercup10108('#skF_55'))).
% 9.24/3.10 tff(c_914, plain, (![X125_71]: (~b48_buttercup10108(X125_71) | ~b48_buttercup10109(X125_71)))).
% 9.24/3.10 tff(c_1238, plain, (b48_buttercup10098('#skF_54'))).
% 9.24/3.10 tff(c_12, plain, (![X5_6]: (b48_buttercup10098(X5_6) | ~b48_buttercup10108(X5_6)))).
% 9.24/3.10 tff(c_1233, plain, (~b48_buttercup10102('#skF_52'))).
% 9.24/3.10 tff(c_872, plain, (![X104_50]: (~b48_buttercup10102(X104_50) | ~b48_buttercup10104(X104_50)))).
% 9.24/3.10 tff(c_1228, plain, (~b48_buttercup10109('#skF_49'))).
% 9.24/3.10 tff(c_940, plain, (![X138_84]: (~b48_buttercup10109(X138_84) | ~b48_buttercup10111(X138_84)))).
% 9.24/3.10 tff(c_1195, plain, (~b48_buttercup10111('#skF_29'))).
% 9.24/3.10 tff(c_1152, plain, (~b48_buttercup10111('#skF_31'))).
% 9.24/3.10 tff(c_1223, plain, (~b48_buttercup10109('#skF_50'))).
% 9.24/3.10 tff(c_928, plain, (![X132_78]: (~b48_buttercup10109(X132_78) | ~b48_buttercup10110(X132_78)))).
% 9.24/3.10 tff(c_1144, plain, (~b48_buttercup10111('#skF_38'))).
% 9.24/3.10 tff(c_1217, plain, (~b48_buttercup10102('#skF_46'))).
% 9.24/3.10 tff(c_1218, plain, (~b48_buttercup10102('#skF_53'))).
% 9.24/3.10 tff(c_884, plain, (![X110_56]: (~b48_buttercup10102(X110_56) | ~b48_buttercup10107(X110_56)))).
% 9.24/3.10 tff(c_1148, plain, (~b48_buttercup10111('#skF_47'))).
% 9.24/3.10 tff(c_1161, plain, (~b48_buttercup10111('#skF_30'))).
% 9.24/3.10 tff(c_1199, plain, (~b48_buttercup10111('#skF_46'))).
% 9.24/3.10 tff(c_1187, plain, (b48_buttercup10098('#skF_30'))).
% 9.24/3.10 tff(c_1209, plain, (~b48_buttercup10107('#skF_50'))).
% 9.24/3.10 tff(c_924, plain, (![X130_76]: (~b48_buttercup10107(X130_76) | ~b48_buttercup10110(X130_76)))).
% 9.24/3.10 tff(c_1188, plain, (b48_buttercup10098('#skF_29'))).
% 9.24/3.10 tff(c_1186, plain, (b48_buttercup10098('#skF_31'))).
% 9.24/3.10 tff(c_1204, plain, (b48_buttercup10098('#skF_55'))).
% 9.24/3.10 tff(c_14, plain, (![X6_7]: (b48_buttercup10098(X6_7) | ~b48_buttercup10109(X6_7)))).
% 9.24/3.10 tff(c_1185, plain, (b48_buttercup10098('#skF_47'))).
% 9.24/3.10 tff(c_1184, plain, (b48_buttercup10098('#skF_38'))).
% 9.24/3.10 tff(c_1135, plain, (~k04_buttercup10100('#skF_46'))).
% 9.24/3.10 tff(c_1134, plain, (~k04_buttercup10100('#skF_29'))).
% 9.24/3.10 tff(c_1191, plain, (b48_buttercup10098('#skF_45'))).
% 9.24/3.10 tff(c_246, plain, (![X27_17]: (b48_buttercup10098(X27_17) | ~k04_buttercup10619(X27_17)))).
% 9.24/3.10 tff(c_1140, plain, (~b48_buttercup10111('#skF_45'))).
% 9.24/3.10 tff(c_1133, plain, (~k04_buttercup10100('#skF_30'))).
% 9.24/3.10 tff(c_1157, plain, (~b48_buttercup10108('#skF_50'))).
% 9.24/3.10 tff(c_926, plain, (![X131_77]: (~b48_buttercup10108(X131_77) | ~b48_buttercup10110(X131_77)))).
% 9.24/3.10 tff(c_1132, plain, (~k04_buttercup10100('#skF_31'))).
% 9.24/3.10 tff(c_1131, plain, (~k04_buttercup10100('#skF_47'))).
% 9.24/3.10 tff(c_1130, plain, (~k04_buttercup10100('#skF_38'))).
% 9.24/3.10 tff(c_1136, plain, (~k04_buttercup10100('#skF_45'))).
% 9.24/3.10 tff(c_1107, plain, (~b48_buttercup10102('#skF_49'))).
% 9.24/3.10 tff(c_858, plain, (![X97_43]: (~k04_buttercup10100(X97_43) | ~k04_buttercup10619(X97_43)))).
% 9.24/3.10 tff(c_1101, plain, (~k04_buttercup10620('#skF_38'))).
% 9.24/3.10 tff(c_1102, plain, (~k04_buttercup10620('#skF_47'))).
% 9.24/3.10 tff(c_1100, plain, (~k04_buttercup10620('#skF_31'))).
% 9.24/3.10 tff(c_932, plain, (![X134_80]: (~b48_buttercup10102(X134_80) | ~b48_buttercup10111(X134_80)))).
% 9.24/3.10 tff(c_1099, plain, (~k04_buttercup10620('#skF_30'))).
% 9.24/3.10 tff(c_1098, plain, (~k04_buttercup10620('#skF_29'))).
% 9.24/3.10 tff(c_856, plain, (![X96_42]: (~k04_buttercup10620(X96_42) | ~k04_buttercup10622(X96_42)))).
% 9.24/3.10 tff(c_594, plain, (![X59_30]: (k04_buttercup10622(X59_30) | ~b48_buttercup10108(X59_30)))).
% 9.27/3.10 tff(c_1072, plain, (~b48_buttercup10104('#skF_54'))).
% 9.27/3.10 tff(c_898, plain, (![X117_63]: (~b48_buttercup10104(X117_63) | ~b48_buttercup10108(X117_63)))).
% 9.27/3.10 tff(c_1067, plain, (b48_buttercup10098('#skF_46'))).
% 9.27/3.10 tff(c_1063, plain, (b48_buttercup10107('#skF_46'))).
% 9.27/3.10 tff(c_1058, plain, (~b48_buttercup10102('#skF_55'))).
% 9.27/3.10 tff(c_716, plain, (![X73_36]: (b48_buttercup10107(X73_36) | ~k04_buttercup10620(X73_36)))).
% 9.27/3.10 tff(c_908, plain, (![X122_68]: (~b48_buttercup10102(X122_68) | ~b48_buttercup10109(X122_68)))).
% 9.27/3.10 tff(c_1051, plain, (b48_buttercup10098('#skF_18'))).
% 9.27/3.10 tff(c_1050, plain, (b48_buttercup10098('#skF_6'))).
% 9.27/3.11 tff(c_1049, plain, (b48_buttercup10098('#skF_44'))).
% 9.27/3.11 tff(c_1031, plain, (~b48_buttercup10107('#skF_55'))).
% 9.27/3.11 tff(c_600, plain, (![X61_31]: (b48_buttercup10098(X61_31) | ~k04_buttercup10100(X61_31)))).
% 9.27/3.11 tff(c_912, plain, (![X124_70]: (~b48_buttercup10107(X124_70) | ~b48_buttercup10109(X124_70)))).
% 9.27/3.11 tff(c_1026, plain, (~b48_buttercup10104('#skF_49'))).
% 9.27/3.11 tff(c_1021, plain, (b48_buttercup10098('#skF_53'))).
% 9.27/3.11 tff(c_934, plain, (![X135_81]: (~b48_buttercup10104(X135_81) | ~b48_buttercup10111(X135_81)))).
% 9.27/3.11 tff(c_10, plain, (![X4_5]: (b48_buttercup10098(X4_5) | ~b48_buttercup10107(X4_5)))).
% 9.27/3.11 tff(c_1016, plain, (b48_buttercup10098('#skF_51'))).
% 9.27/3.11 tff(c_6, plain, (![X2_3]: (b48_buttercup10098(X2_3) | ~b48_buttercup10102(X2_3)))).
% 9.27/3.11 tff(c_1011, plain, (~b48_buttercup10111('#skF_32'))).
% 9.27/3.11 tff(c_1006, plain, (~b48_buttercup10104('#skF_55'))).
% 9.27/3.11 tff(c_360, plain, (![X37_21]: (k04_buttercup10100(X37_21) | ~b48_buttercup10111(X37_21)))).
% 9.27/3.11 tff(c_1000, plain, (k04_buttercup10619('#skF_38'))).
% 9.27/3.11 tff(c_1001, plain, (k04_buttercup10619('#skF_47'))).
% 9.27/3.11 tff(c_999, plain, (k04_buttercup10619('#skF_31'))).
% 9.27/3.11 tff(c_910, plain, (![X123_69]: (~b48_buttercup10104(X123_69) | ~b48_buttercup10109(X123_69)))).
% 9.27/3.11 tff(c_998, plain, (k04_buttercup10619('#skF_30'))).
% 9.27/3.11 tff(c_997, plain, (k04_buttercup10619('#skF_29'))).
% 9.27/3.11 tff(c_4, plain, (![X1_2]: (k04_buttercup10619(X1_2) | ~k04_buttercup10622(X1_2)))).
% 9.27/3.11 tff(c_980, plain, (~b48_buttercup10104('#skF_50'))).
% 9.27/3.11 tff(c_975, plain, (k04_buttercup10619('#skF_46'))).
% 9.27/3.11 tff(c_922, plain, (![X129_75]: (~b48_buttercup10104(X129_75) | ~b48_buttercup10110(X129_75)))).
% 9.27/3.11 tff(c_2, plain, (![X0_1]: (k04_buttercup10619(X0_1) | ~k04_buttercup10620(X0_1)))).
% 9.27/3.11 tff(c_970, plain, (b48_buttercup10098('#skF_52'))).
% 9.27/3.11 tff(c_965, plain, (~b48_buttercup10108('#skF_49'))).
% 9.27/3.11 tff(c_8, plain, (![X3_4]: (b48_buttercup10098(X3_4) | ~b48_buttercup10104(X3_4)))).
% 9.27/3.11 tff(c_938, plain, (![X137_83]: (~b48_buttercup10108(X137_83) | ~b48_buttercup10111(X137_83)))).
% 9.27/3.11 tff(c_960, plain, (~b48_buttercup10102('#skF_50'))).
% 9.27/3.11 tff(c_920, plain, (![X128_74]: (~b48_buttercup10102(X128_74) | ~b48_buttercup10110(X128_74)))).
% 9.27/3.11 tff(c_955, plain, (~b48_buttercup10107('#skF_49'))).
% 9.27/3.11 tff(c_936, plain, (![X136_82]: (~b48_buttercup10107(X136_82) | ~b48_buttercup10111(X136_82)))).
% 9.27/3.11 tff(c_578, plain, (~b48_buttercup10104('#skF_29'))).
% 9.27/3.11 tff(c_244, plain, (b48_buttercup10098('#skF_12'))).
% 9.27/3.11 tff(c_242, plain, (~k04_buttercup10619('#skF_12'))).
% 9.27/3.11 tff(c_850, plain, (b48_buttercup10109('#skF_55'))).
% 9.27/3.11 tff(c_580, plain, (k04_buttercup10622('#skF_29'))).
% 9.27/3.11 tff(c_584, plain, (~b48_buttercup10110('#skF_30'))).
% 9.27/3.11 tff(c_586, plain, (k04_buttercup10622('#skF_30'))).
% 9.27/3.11 tff(c_590, plain, (~b48_buttercup10108('#skF_31'))).
% 9.27/3.11 tff(c_592, plain, (k04_buttercup10622('#skF_31'))).
% 9.27/3.11 tff(c_596, plain, (~k04_buttercup10100('#skF_32'))).
% 9.27/3.11 tff(c_828, plain, (k04_buttercup10100('#skF_44'))).
% 9.27/3.11 tff(c_710, plain, (~b48_buttercup10102('#skF_38'))).
% 9.27/3.11 tff(c_130, plain, (k04_buttercup10100('#skF_6'))).
% 9.27/3.11 tff(c_832, plain, (k04_buttercup10620('#skF_46'))).
% 9.27/3.11 tff(c_598, plain, (b48_buttercup10098('#skF_32'))).
% 9.27/3.11 tff(c_712, plain, (k04_buttercup10622('#skF_38'))).
% 9.27/3.11 tff(c_830, plain, (k04_buttercup10619('#skF_45'))).
% 9.27/3.11 tff(c_834, plain, (k04_buttercup10622('#skF_47'))).
% 9.27/3.11 tff(c_836, plain, (b48_buttercup10098('#skF_48'))).
% 9.27/3.11 tff(c_356, plain, (~b48_buttercup10111('#skF_18'))).
% 9.27/3.11 tff(c_128, plain, (~b48_buttercup10109('#skF_6'))).
% 9.27/3.11 tff(c_848, plain, (b48_buttercup10108('#skF_54'))).
% 9.27/3.11 tff(c_846, plain, (b48_buttercup10107('#skF_53'))).
% 9.27/3.11 tff(c_844, plain, (b48_buttercup10104('#skF_52'))).
% 9.27/3.11 tff(c_358, plain, (k04_buttercup10100('#skF_18'))).
% 9.27/3.11 tff(c_838, plain, (b48_buttercup10111('#skF_49'))).
% 9.27/3.11 tff(c_840, plain, (b48_buttercup10110('#skF_50'))).
% 9.27/3.11 tff(c_842, plain, (b48_buttercup10102('#skF_51'))).
% 9.27/3.11 tff(c_948, plain, (b48_buttercup10098('#skF_56'))).
% 9.27/3.11 tff(c_950, plain, (k04_buttercup10100('#skF_56'))).
% 9.27/3.11 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.27/3.11
%------------------------------------------------------------------------------