%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN870-1 : TPTP v9.0.0. Released v2.5.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 : n023.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:05:58 PM UTC 2025 % Result : Satisfiable 10.46s 3.45s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.08 % Problem : SYN870-1 : TPTP v9.0.0. Released v2.5.0. % 0.00/0.09 % 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.09/0.28 % Computer : n023.cluster.edu % 0.09/0.28 % Model : x86_64 x86_64 % 0.09/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.28 % Memory : 8042.1875MB % 0.09/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.28 % CPULimit : 300 % 0.09/0.28 % WCLimit : 300 % 0.09/0.28 % DateTime : Wed Apr 9 08:34:09 EDT 2025 % 0.13/0.28 % CPUTime : % 10.46/3.45 % 10.46/3.45 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 10.46/3.45 % 10.46/3.45 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 10.46/3.46 %$ ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1 > ssPv10_11r1r1r1r1r1r1r1r1r1r1r1 > ssNder1_11r1r1r1r1r1r1r1r1r1r1r1 > ssPv11_10r1r1r1r1r1r1r1r1r1r1 > ssNder1_10r1r1r1r1r1r1r1r1r1r1 > ssPv12_9r1r1r1r1r1r1r1r1r1 > ssNder1_9r1r1r1r1r1r1r1r1r1 > ssPv13_8r1r1r1r1r1r1r1r1 > ssNder1_8r1r1r1r1r1r1r1r1 > ssPv14_7r1r1r1r1r1r1r1 > ssNder1_7r1r1r1r1r1r1r1 > ssPv15_6r1r1r1r1r1r1 > ssNder1_6r1r1r1r1r1r1 > ssPv16_5r1r1r1r1r1 > ssNder1_5r1r1r1r1r1 > ssPv17_4r1r1r1r1 > ssNder1_4r1r1r1r1 > ssPv18_3r1r1r1 > ssNder1_3r1r1r1 > ssPv19_2r1r1 > ssNder1_2r1r1 > ssPv20_1r1 > ssNder1_1r1 > #nlpp > ssNder1_0 > skc31 > skc30 > skc29 > skc28 > skc27 > skc26 > skc25 > skc24 > skc23 > skc22 > skc21 > skc20 > skc19 > skc18 > skc17 > skc16 % 10.46/3.46 % 10.46/3.46 %Foreground sorts: % 10.46/3.46 % 10.46/3.46 % 10.46/3.46 %Background operators: % 10.46/3.46 % 10.46/3.46 % 10.46/3.46 %Foreground operators: % 10.46/3.46 tff(skc16, type, skc16: $i). % 10.46/3.46 tff(ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(ssPv17_4r1r1r1r1, type, ssPv17_4r1r1r1r1: ($i * $i * $i * $i) > $o). % 10.46/3.46 tff(ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(ssNder1_7r1r1r1r1r1r1r1, type, ssNder1_7r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(ssPv16_5r1r1r1r1r1, type, ssPv16_5r1r1r1r1r1: ($i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(skc18, type, skc18: $i). % 10.46/3.46 tff(skc29, type, skc29: $i). % 10.46/3.46 tff(skc25, type, skc25: $i). % 10.46/3.46 tff(ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(ssNder1_10r1r1r1r1r1r1r1r1r1r1, type, ssNder1_10r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(skc17, type, skc17: $i). % 10.46/3.46 tff(skc26, type, skc26: $i). % 10.46/3.46 tff(skc24, type, skc24: $i). % 10.46/3.46 tff(ssNder1_2r1r1, type, ssNder1_2r1r1: ($i * $i) > $o). % 10.46/3.46 tff(ssPv15_6r1r1r1r1r1r1, type, ssPv15_6r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(ssPv18_3r1r1r1, type, ssPv18_3r1r1r1: ($i * $i * $i) > $o). % 10.46/3.46 tff(ssPv11_10r1r1r1r1r1r1r1r1r1r1, type, ssPv11_10r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(ssPv12_9r1r1r1r1r1r1r1r1r1, type, ssPv12_9r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(skc20, type, skc20: $i). % 10.46/3.46 tff(ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(skc23, type, skc23: $i). % 10.46/3.46 tff(ssPv14_7r1r1r1r1r1r1r1, type, ssPv14_7r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(ssNder1_0, type, ssNder1_0: $o). % 10.46/3.46 tff(skc21, type, skc21: $i). % 10.46/3.46 tff(ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(skc22, type, skc22: $i). % 10.46/3.46 tff(ssNder1_11r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_11r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(skc27, type, skc27: $i). % 10.46/3.46 tff(ssNder1_8r1r1r1r1r1r1r1r1, type, ssNder1_8r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(ssNder1_5r1r1r1r1r1, type, ssNder1_5r1r1r1r1r1: ($i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(ssPv19_2r1r1, type, ssPv19_2r1r1: ($i * $i) > $o). % 10.46/3.46 tff(ssNder1_9r1r1r1r1r1r1r1r1r1, type, ssNder1_9r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(ssNder1_3r1r1r1, type, ssNder1_3r1r1r1: ($i * $i * $i) > $o). % 10.46/3.46 tff(skc31, type, skc31: $i). % 10.46/3.46 tff(ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(ssNder1_6r1r1r1r1r1r1, type, ssNder1_6r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(ssNder1_4r1r1r1r1, type, ssNder1_4r1r1r1r1: ($i * $i * $i * $i) > $o). % 10.46/3.46 tff(ssPv20_1r1, type, ssPv20_1r1: $i > $o). % 10.46/3.46 tff(skc30, type, skc30: $i). % 10.46/3.46 tff(ssPv13_8r1r1r1r1r1r1r1r1, type, ssPv13_8r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(ssPv10_11r1r1r1r1r1r1r1r1r1r1r1, type, ssPv10_11r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(skc19, type, skc19: $i). % 10.46/3.46 tff(ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1, type, ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1: ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $o). % 10.46/3.46 tff(ssNder1_1r1, type, ssNder1_1r1: $i > $o). % 10.46/3.46 tff(skc28, type, skc28: $i). % 10.46/3.46 % 10.46/3.46 %Saturated clause set: % 10.46/3.47 tff(c_1199, plain, (![X3_463, X10_476, Z_466, X7_467, X_471, X2_470, W_462, X1_468, X6_461, V_473, Y_472, X9_465, X4_475, X11_469, X5_460, U_464, X8_474]: (ssPv14_7r1r1r1r1r1r1r1(U_464, V_473, W_462, X_471, Y_472, Z_466, X1_468) | ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_464, V_473, W_462, X_471, Y_472, Z_466, X1_468, X2_470, X3_463, X4_475, X5_460, X6_461, X7_467, X8_474, X9_465, X10_476) | ~ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_464, V_473, W_462, X_471, Y_472, Z_466, X1_468, X2_470, X3_463, X4_475, X5_460, X6_461, X7_467, X8_474, X9_465, X10_476, X11_469)))). % 10.46/3.47 tff(c_1203, plain, (![X6_478, X8_492, X_489, X9_482, X12_483, X10_494, X3_480, W_479, U_481, V_491, Z_484, X1_486, Y_490, X2_488, X7_485, X11_487, X4_493, X5_477]: (ssPv14_7r1r1r1r1r1r1r1(U_481, V_491, W_479, X_489, Y_490, Z_484, X1_486) | ssPv13_8r1r1r1r1r1r1r1r1(U_481, V_491, W_479, X_489, Y_490, Z_484, X1_486, X2_488) | ~ssPv3_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_481, V_491, W_479, X_489, Y_490, Z_484, X1_486, X2_488, X3_480, X4_493, X5_477, X6_478, X7_485, X8_492, X9_482, X10_494, X11_487, X12_483)))). % 10.46/3.47 tff(c_1213, plain, (![X1_200, U_198, X2_201, X3_197, W_196, Y_203, X6_195, X4_205, X_202, X5_194, Z_199, V_204]: (ssPv14_7r1r1r1r1r1r1r1(U_198, V_204, W_196, X_202, Y_203, Z_199, X1_200) | ~ssPv16_5r1r1r1r1r1(U_198, V_204, W_196, X_202, Y_203) | ~ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(U_198, V_204, W_196, X_202, Y_203, Z_199, X1_200, X2_201, X3_197, X4_205, X5_194, X6_195)))). % 10.46/3.47 tff(c_1211, plain, (![X4_180, X_177, Y_178, X1_175, W_170, U_172, X3_171, Z_173, V_179, X2_176]: (ssPv13_8r1r1r1r1r1r1r1r1(U_172, V_179, W_170, X_177, Y_178, Z_173, X1_175, X2_176) | ssPv11_10r1r1r1r1r1r1r1r1r1r1(U_172, V_179, W_170, X_177, Y_178, Z_173, X1_175, X2_176, X3_171, X4_180)))). % 10.46/3.47 tff(c_1212, plain, (![X4_180, X_177, Y_178, X1_175, W_170, U_172, X3_171, Z_173, V_179, X2_176]: (ssPv11_10r1r1r1r1r1r1r1r1r1r1(U_172, V_179, W_170, X_177, Y_178, Z_173, X1_175, X2_176, X3_171, X4_180) | ~ssPv14_7r1r1r1r1r1r1r1(U_172, V_179, W_170, X_177, Y_178, Z_173, X1_175)))). % 10.46/3.47 tff(c_1209, plain, (![Z_1247, X5_1252, X1_1243, U_1242, X3_1251, W_1249, X4_1240, Y_1245, X2_1250, X_1244, V_1241]: (~ssPv10_11r1r1r1r1r1r1r1r1r1r1r1(U_1242, V_1241, W_1249, X_1244, Y_1245, Z_1247, X1_1243, X2_1250, X3_1251, X4_1240, X5_1252)))). % 10.46/3.47 tff(c_1205, plain, (![U_25, V_28]: (~ssPv19_2r1r1(U_25, V_28)))). % 10.46/3.47 tff(c_1194, plain, (![U_11]: (ssPv20_1r1(U_11)))). % 10.46/3.48 tff(c_936, plain, (![X12_651, X9_650, X4_662, X11_655, X3_648, V_660, X2_656, X10_664, X1_654, X5_645, X_658, X7_653, U_649, X6_646, X8_661, W_647, X14_663, Y_659, X13_657, Z_652]: (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_649, V_660, W_647, X_658, Y_659, Z_652, X1_654, X2_656, X3_648, X4_662, X5_645, X6_646, X7_653, X8_661) | ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_649, V_660, W_647, X_658, Y_659, Z_652, X1_654, X2_656, X3_648, X4_662, X5_645, X6_646, X7_653, X8_661, X9_650) | ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_649, V_660, W_647, X_658, Y_659, Z_652, X1_654, X2_656, X3_648, X4_662, X5_645, X6_646, X7_653, X8_661, X9_650, X10_664, X11_655, X12_651, X13_657) | ~ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_649, V_660, W_647, X_658, Y_659, Z_652, X1_654, X2_656, X3_648, X4_662, X5_645, X6_646, X7_653, X8_661, X9_650, X10_664, X11_655, X12_651, X13_657, X14_663)))). % 10.46/3.48 tff(c_910, plain, (![Y_544, U_536, X1_540, X_543, V_545, Z_538, X5_532, X11_541, X2_542, W_534, X7_539, X4_547, X3_535, X6_533, X9_537, X8_546, X10_548]: (ssPv12_9r1r1r1r1r1r1r1r1r1(U_536, V_545, W_534, X_543, Y_544, Z_538, X1_540, X2_542, X3_535) | ~ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_536, V_545, W_534, X_543, Y_544, Z_538, X1_540, X2_542, X3_535, X4_547, X5_532, X6_533, X7_539, X8_546, X9_537) | ~ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_536, V_545, W_534, X_543, Y_544, Z_538, X1_540, X2_542, X3_535, X4_547, X5_532, X6_533, X7_539, X8_546, X9_537, X10_548, X11_541) | ~ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_536, V_545, W_534, X_543, Y_544, Z_538, X1_540, X2_542, X3_535, X4_547, X5_532, X6_533, X7_539, X8_546, X9_537, X10_548)))). % 10.46/3.48 tff(c_940, plain, (![X6_626, X9_630, X5_625, X11_635, Y_639, V_640, X4_642, U_629, X7_633, W_627, X8_641, Z_632, X13_637, X2_636, X12_631, X14_643, X1_634, X10_644, X_638, X3_628]: (ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_629, V_640, W_627, X_638, Y_639, Z_632, X1_634, X2_636, X3_628, X4_642, X5_625, X6_626, X7_633, X8_641, X9_630, X10_644, X11_635, X12_631, X13_637, X14_643) | ~ssPv16_5r1r1r1r1r1(U_629, V_640, W_627, X_638, Y_639) | ~ssPv14_7r1r1r1r1r1r1r1(U_629, V_640, W_627, X_638, Y_639, Z_632, X1_634) | ~ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_629, V_640, W_627, X_638, Y_639, Z_632, X1_634, X2_636, X3_628, X4_642, X5_625, X6_626, X7_633, X8_641, X9_630, X10_644, X11_635, X12_631, X13_637)))). % 10.46/3.48 tff(c_948, plain, (![W_569, X2_578, X7_575, X_580, V_582, X1_576, X4_584, X13_579, X11_577, Z_574, X5_567, X12_573, X8_583, Y_581, X6_568, X9_572, X10_585, X3_570, U_571]: (ssPv14_7r1r1r1r1r1r1r1(U_571, V_582, W_569, X_580, Y_581, Z_574, X1_576) | ssPv4_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_571, V_582, W_569, X_580, Y_581, Z_574, X1_576, X2_578, X3_570, X4_584, X5_567, X6_568, X7_575, X8_583, X9_572, X10_585, X11_577) | ssPv2_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_571, V_582, W_569, X_580, Y_581, Z_574, X1_576, X2_578, X3_570, X4_584, X5_567, X6_568, X7_575, X8_583, X9_572, X10_585, X11_577, X12_573, X13_579) | ~ssPv15_6r1r1r1r1r1r1(U_571, V_582, W_569, X_580, Y_581, Z_574)))). % 10.46/3.48 tff(c_1126, plain, (![U_25, V_28, W_24]: (~ssPv18_3r1r1r1(U_25, V_28, W_24)))). % 10.46/3.48 tff(c_1122, plain, (![U_41, V_45, W_40, X_43]: (ssPv17_4r1r1r1r1(U_41, V_45, W_40, X_43)))). % 10.46/3.48 tff(c_934, plain, (![X5_495, Z_502, U_499, X8_511, X7_503, X4_512, V_510, X9_500, X3_498, X6_496, X10_513, W_497, X13_507, X1_504, X2_506, X11_505, Y_509, X_508, X12_501]: (ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_499, V_510, W_497, X_508, Y_509, Z_502, X1_504, X2_506, X3_498, X4_512, X5_495, X6_496, X7_503, X8_511, X9_500, X10_513, X11_505, X12_501, X13_507)))). % 10.46/3.48 tff(c_930, plain, (![Z_449, U_446, X12_448, X7_450, X8_457, X10_459, V_456, X2_453, X11_452, Y_455, X3_445, X1_451, X6_443, X4_458, X_454, W_444, X5_442, X9_447]: (ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_446, V_456, W_444, X_454, Y_455, Z_449, X1_451, X2_453, X3_445, X4_458, X5_442, X6_443, X7_450, X8_457, X9_447, X10_459, X11_452, X12_448)))). % 10.46/3.48 tff(c_902, plain, (![X_404, Z_399, X10_409, X6_394, X11_402, X4_408, X9_398, X5_393, U_397, X3_396, Y_405, X2_403, X8_407, W_395, X1_401, X7_400, V_406]: (ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_397, V_406, W_395, X_404, Y_405, Z_399, X1_401, X2_403, X3_396, X4_408, X5_393, X6_394, X7_400, X8_407, X9_398, X10_409, X11_402)))). % 10.46/3.48 tff(c_854, plain, (![X2_314, X4_319, V_317, X9_310, X1_313, X5_305, W_307, X8_318, Y_316, X3_308, U_309, X7_312, X_315, X6_306, Z_311]: (~ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_309, V_317, W_307, X_315, Y_316, Z_311, X1_313, X2_314, X3_308, X4_319, X5_305, X6_306, X7_312, X8_318, X9_310, skc17)))). % 10.46/3.48 tff(c_864, plain, (![V_302, X9_295, X_300, W_292, X8_303, X3_293, U_294, X5_290, Z_296, X1_298, Y_301, X7_297, X6_291, X2_299, X4_304]: (ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_294, V_302, W_292, X_300, Y_301, Z_296, X1_298, X2_299, X3_293, X4_304, X5_290, X6_291, X7_297, X8_303, X9_295, skc16)))). % 10.46/3.48 tff(c_870, plain, (![Y_373, X4_376, Z_368, U_366, X5_362, W_364, X2_371, X_372, X9_367, X8_375, X3_365, V_374, X7_369, X10_377, X1_370, X6_363]: (ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_366, V_374, W_364, X_372, Y_373, Z_368, X1_370, X2_371, X3_365, X4_376, X5_362, X6_363, X7_369, X8_375, X9_367, X10_377)))). % 10.46/3.48 tff(c_774, plain, (![X_243, X5_234, X8_246, X1_241, X6_235, X7_240, X4_247, Z_239, W_236, X3_237, U_238, Y_244, V_245, X2_242]: (~ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_238, V_245, W_236, X_243, Y_244, Z_239, X1_241, X2_242, X3_237, X4_247, X5_234, X6_235, X7_240, X8_246, skc19)))). % 10.46/3.48 tff(c_780, plain, (![U_224, X8_232, V_231, W_222, X5_220, X4_233, X2_228, Y_230, X7_226, X6_221, Z_225, X1_227, X_229, X3_223]: (ssPv6_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_224, V_231, W_222, X_229, Y_230, Z_225, X1_227, X2_228, X3_223, X4_233, X5_220, X6_221, X7_226, X8_232, skc18)))). % 10.46/3.48 tff(c_868, plain, (![W_277, X6_276, U_279, X9_280, X_285, X4_289, X5_275, Y_286, V_287, X2_284, X3_278, X7_282, X1_283, Z_281, X8_288]: (ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_279, V_287, W_277, X_285, Y_286, Z_281, X1_283, X2_284, X3_278, X4_289, X5_275, X6_276, X7_282, X8_288, X9_280)))). % 10.46/3.48 tff(c_754, plain, (![V_192, W_183, X3_184, X2_189, Z_186, X7_187, X_190, X4_193, Y_191, U_185, X6_182, X1_188, X5_181]: (~ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_185, V_192, W_183, X_190, Y_191, Z_186, X1_188, X2_189, X3_184, X4_193, X5_181, X6_182, X7_187, skc21)))). % 10.46/3.48 tff(c_776, plain, (![X5_206, X3_209, Y_216, X8_218, X4_219, V_217, X_215, X2_214, Z_211, X1_213, X6_207, W_208, U_210, X7_212]: (ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_210, V_217, W_208, X_215, Y_216, Z_211, X1_213, X2_214, X3_209, X4_219, X5_206, X6_207, X7_212, X8_218)))). % 10.46/3.48 tff(c_784, plain, (![X6_169, X4_180, X_177, Y_178, X1_175, W_170, X5_168, U_172, X3_171, Z_173, X7_174, V_179, X2_176]: (ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(U_172, V_179, W_170, X_177, Y_178, Z_173, X1_175, X2_176, X3_171, X4_180, X5_168, X6_169, X7_174, skc20)))). % 10.46/3.48 tff(c_750, plain, (![X1_137, V_141, X6_132, X5_131, U_135, X_139, X2_138, X3_134, Z_136, Y_140, X4_142, W_133]: (ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U_135, V_141, W_133, X_139, Y_140, Z_136, X1_137, X2_138, X3_134, X4_142, X5_131, X6_132, skc22)))). % 10.46/3.48 tff(c_770, plain, (![X3_158, X5_155, X1_162, X4_167, X7_161, X2_163, Z_160, X6_156, W_157, U_159, V_166, X_164, Y_165]: (ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U_159, V_166, W_157, X_164, Y_165, Z_160, X1_162, X2_163, X3_158, X4_167, X5_155, X6_156, X7_161)))). % 10.46/3.48 tff(c_766, plain, (![Y_152, X_151, X3_146, X6_144, V_153, U_147, X1_149, Z_148, X5_143, X4_154, W_145, X2_150]: (~ssPv8_13r1r1r1r1r1r1r1r1r1r1r1r1r1(U_147, V_153, W_145, X_151, Y_152, Z_148, X1_149, X2_150, X3_146, X4_154, X5_143, X6_144, skc23)))). % 10.46/3.48 tff(c_752, plain, (![X4_130, W_121, X1_125, U_123, Y_128, X2_126, X5_119, V_129, X_127, X3_122, Z_124, X6_120]: (ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(U_123, V_129, W_121, X_127, Y_128, Z_124, X1_125, X2_126, X3_122, X4_130, X5_119, X6_120)))). % 10.46/3.48 tff(c_694, plain, (![X3_110, W_109, X_115, Z_112, X4_118, V_117, Y_116, X5_108, U_111, X1_113, X2_114]: (ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(U_111, V_117, W_109, X_115, Y_116, Z_112, X1_113, X2_114, X3_110, X4_118, X5_108)))). % 10.46/3.48 tff(c_624, plain, (![Z_101, X_104, X4_107, V_106, U_100, W_98, X3_99, Y_105, X1_102, X2_103]: (ssNder1_10r1r1r1r1r1r1r1r1r1r1(U_100, V_106, W_98, X_104, Y_105, Z_101, X1_102, X2_103, X3_99, X4_107)))). % 10.46/3.48 tff(c_602, plain, (![Z_84, U_83, X3_82, Y_88, V_89, X_87, X1_85, X2_86, W_81]: (ssNder1_9r1r1r1r1r1r1r1r1r1(U_83, V_89, W_81, X_87, Y_88, Z_84, X1_85, X2_86, X3_82)))). % 10.46/3.48 tff(c_470, plain, (![Y_64, V_65, Z_61, U_60, X1_62, W_59, X_63]: (ssPv13_8r1r1r1r1r1r1r1r1(U_60, V_65, W_59, X_63, Y_64, Z_61, X1_62, skc24)))). % 10.46/3.48 tff(c_452, plain, (![V_80, X2_77, Z_75, W_73, Y_79, X1_76, U_74, X_78]: (ssNder1_8r1r1r1r1r1r1r1r1(U_74, V_80, W_73, X_78, Y_79, Z_75, X1_76, X2_77)))). % 10.46/3.48 tff(c_382, plain, (![X_70, U_67, X1_69, Y_71, Z_68, V_72, W_66]: (~ssPv13_8r1r1r1r1r1r1r1r1(U_67, V_72, W_66, X_70, Y_71, Z_68, X1_69, skc25)))). % 10.46/3.48 tff(c_444, plain, (![Y_57, Z_54, U_53, X_56, V_58, X1_55, W_52]: (ssNder1_7r1r1r1r1r1r1r1(U_53, V_58, W_52, X_56, Y_57, Z_54, X1_55)))). % 10.46/3.49 tff(c_438, plain, (![V_45, X_43, Y_44, Z_42, W_40, U_41]: (ssPv14_7r1r1r1r1r1r1r1(U_41, V_45, W_40, X_43, Y_44, Z_42, skc26)))). % 10.46/3.49 tff(c_430, plain, (![W_46, U_47, Y_50, Z_48, V_51, X_49]: (~ssPv14_7r1r1r1r1r1r1r1(U_47, V_51, W_46, X_49, Y_50, Z_48, skc27)))). % 10.46/3.49 tff(c_372, plain, (![V_39, Z_36, U_35, X_37, Y_38, W_34]: (ssNder1_6r1r1r1r1r1r1(U_35, V_39, W_34, X_37, Y_38, Z_36)))). % 10.46/3.49 tff(c_288, plain, (![V_28, W_24, X_26, Y_27, U_25]: (ssPv15_6r1r1r1r1r1r1(U_25, V_28, W_24, X_26, Y_27, skc28)))). % 10.46/3.49 tff(c_254, plain, (![W_29, Y_32, X_31, V_33, U_30]: (~ssPv15_6r1r1r1r1r1r1(U_30, V_33, W_29, X_31, Y_32, skc29)))). % 10.46/3.49 tff(c_370, plain, (![U_11, V_12, W_13, X_14]: (ssPv16_5r1r1r1r1r1(U_11, V_12, W_13, X_14, skc30)))). % 10.46/3.49 tff(c_290, plain, (![U_20, X_21, Y_22, W_19, V_23]: (ssNder1_5r1r1r1r1r1(U_20, V_23, W_19, X_21, Y_22)))). % 10.46/3.49 tff(c_314, plain, (![U_15, V_16, W_17, X_18]: (~ssPv16_5r1r1r1r1r1(U_15, V_16, W_17, X_18, skc31)))). % 10.46/3.49 tff(c_252, plain, (![U_7, V_8, W_9, X_10]: (ssNder1_4r1r1r1r1(U_7, V_8, W_9, X_10)))). % 10.46/3.49 tff(c_234, plain, (![U_4, V_5, W_6]: (ssNder1_3r1r1r1(U_4, V_5, W_6)))). % 10.46/3.49 tff(c_226, plain, (![U_2, V_3]: (ssNder1_2r1r1(U_2, V_3)))). % 10.46/3.49 tff(c_114, plain, (![U_1]: (ssNder1_1r1(U_1)))). % 10.46/3.49 tff(c_2, plain, (ssNder1_0)). % 10.46/3.49 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 10.46/3.49 %------------------------------------------------------------------------------