%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN743-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 : n003.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:04:20 PM UTC 2025 % Result : Satisfiable 5.54s 2.31s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : SYN743-1 : TPTP v9.0.0. Released v2.5.0. % 0.04/0.13 % 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.13/0.34 % Computer : n003.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Apr 9 08:14:03 EDT 2025 % 0.13/0.34 % CPUTime : % 5.54/2.31 % 5.54/2.31 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.54/2.31 % 5.54/2.31 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.54/2.32 %$ ssRr > ssPv8 > ssPv7 > ssPv6 > ssPv5 > ssPv4 > ssPv3 > ssPv2 > ssPv1 > #nlpp > skf1 % 5.54/2.32 % 5.54/2.32 %Foreground sorts: % 5.54/2.32 % 5.54/2.32 % 5.54/2.32 %Background operators: % 5.54/2.32 % 5.54/2.32 % 5.54/2.32 %Foreground operators: % 5.54/2.32 tff(skf1, type, skf1: $i > $i). % 5.54/2.32 tff(ssPv1, type, ssPv1: $i > $o). % 5.54/2.32 tff(ssPv3, type, ssPv3: $i > $o). % 5.54/2.32 tff(ssPv7, type, ssPv7: $i > $o). % 5.54/2.32 tff(ssPv6, type, ssPv6: $i > $o). % 5.54/2.32 tff(ssPv5, type, ssPv5: $i > $o). % 5.54/2.32 tff(ssRr, type, ssRr: ($i * $i) > $o). % 5.54/2.32 tff(ssPv4, type, ssPv4: $i > $o). % 5.54/2.32 tff(ssPv2, type, ssPv2: $i > $o). % 5.54/2.32 tff(ssPv8, type, ssPv8: $i > $o). % 5.54/2.32 % 5.54/2.32 %Saturated clause set: % 5.54/2.32 tff(c_951, plain, (![U_1, V_343]: (~ssPv5(skf1(U_1)) | ~ssPv8(V_343) | ~ssRr(U_1, V_343) | ssPv6(U_1) | ssPv2(U_1) | ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv3(skf1(U_1)) | ssPv4(U_1) | ssPv3(U_1)))). % 5.54/2.32 tff(c_777, plain, (![W_212, U_320, V_213]: (~ssPv5(W_212) | ~ssRr(U_320, W_212) | ~ssPv8(V_213) | ~ssRr(U_320, V_213) | ssPv6(U_320) | ssPv2(U_320) | ssPv1(skf1(U_320)) | ssPv2(skf1(U_320)) | ~ssPv3(skf1(U_320)) | ssPv4(U_320) | ssPv3(U_320)))). % 5.54/2.32 tff(c_944, plain, (![U_1]: (~ssPv5(U_1) | ssPv6(U_1) | ssPv2(U_1) | ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv3(skf1(U_1)) | ssPv4(U_1) | ssPv3(U_1)))). % 5.54/2.32 tff(c_919, plain, (![U_190]: (ssPv1(skf1(U_190)) | ~ssPv3(skf1(U_190)) | ssPv2(U_190) | ~ssPv7(U_190) | ssPv3(U_190) | ~ssPv8(U_190) | ssPv5(U_190) | ssPv2(skf1(U_190)) | ~ssPv4(U_190)))). % 5.54/2.32 tff(c_874, plain, (![U_1]: (ssPv6(U_1) | ssPv3(U_1) | ~ssPv2(skf1(U_1)) | ssPv7(U_1) | ssPv3(skf1(U_1)) | ~ssPv4(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv7(skf1(U_1)) | ~ssPv2(U_1)))). % 5.54/2.32 tff(c_863, plain, (![U_1]: (ssPv6(U_1) | ~ssPv8(skf1(U_1)) | ssPv3(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv7(U_1) | ssPv3(skf1(U_1)) | ~ssPv4(skf1(U_1))))). % 5.54/2.32 tff(c_679, plain, (![U_1, V_306]: (ssPv6(U_1) | ~ssPv8(V_306) | ~ssRr(U_1, V_306) | ssPv3(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv7(U_1) | ssPv3(skf1(U_1)) | ~ssPv4(skf1(U_1))))). % 5.54/2.32 tff(c_819, plain, (![U_1]: (ssPv6(U_1) | ~ssPv2(skf1(U_1)) | ssPv3(U_1) | ssPv3(skf1(U_1)) | ~ssPv5(U_1) | ssPv1(skf1(U_1)) | ssPv7(skf1(U_1)) | ~ssPv2(U_1)))). % 5.54/2.32 tff(c_399, plain, (![U_239]: (ssPv3(U_239) | ~ssPv8(U_239) | ssPv5(U_239) | ~ssPv4(U_239) | ~ssPv6(skf1(U_239)) | ssPv1(skf1(U_239)) | ssPv2(skf1(U_239)) | ~ssPv3(skf1(U_239))))). % 5.54/2.32 tff(c_808, plain, (![U_1]: (ssPv6(U_1) | ~ssPv8(skf1(U_1)) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv3(U_1) | ssPv3(skf1(U_1)) | ~ssPv5(U_1)))). % 5.54/2.32 tff(c_681, plain, (![U_1, V_306]: (ssPv6(U_1) | ~ssPv8(V_306) | ~ssRr(U_1, V_306) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv3(U_1) | ssPv3(skf1(U_1)) | ~ssPv5(U_1)))). % 5.54/2.32 tff(c_801, plain, (![U_1]: (~ssPv7(U_1) | ssPv6(U_1) | ssPv2(U_1) | ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv3(skf1(U_1)) | ssPv4(U_1) | ssPv3(U_1)))). % 5.54/2.32 tff(c_664, plain, (![U_1]: (ssPv6(U_1) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv3(skf1(U_1)) | ssPv2(U_1) | ~ssPv7(U_1) | ~ssPv4(skf1(U_1))))). % 5.54/2.32 tff(c_260, plain, (![U_184]: (ssPv5(skf1(U_184)) | ~ssPv8(U_184) | ~ssPv4(U_184) | ~ssPv4(skf1(U_184)) | ssPv2(skf1(U_184)) | ssPv1(skf1(U_184)) | ~ssPv3(skf1(U_184)) | ssPv6(skf1(U_184))))). % 5.54/2.32 tff(c_663, plain, (![U_1]: (ssPv6(U_1) | ssPv2(U_1) | ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv3(skf1(U_1)) | ssPv4(U_1) | ssPv3(U_1) | ssPv4(skf1(U_1))))). % 5.54/2.32 tff(c_745, plain, (![U_1]: (ssPv6(U_1) | ssPv3(U_1) | ~ssPv8(U_1) | ssPv5(U_1) | ssPv2(skf1(U_1)) | ~ssPv4(U_1)))). % 5.54/2.32 tff(c_701, plain, (![U_1]: (ssPv6(U_1) | ssPv3(U_1) | ssPv4(U_1) | ~ssPv5(U_1) | ~ssPv2(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv7(skf1(U_1)) | ~ssPv2(U_1)))). % 5.54/2.32 tff(c_690, plain, (![U_1]: (ssPv6(U_1) | ~ssPv8(skf1(U_1)) | ssPv3(U_1) | ssPv1(skf1(U_1)) | ssPv4(U_1) | ~ssPv5(U_1) | ~ssPv2(skf1(U_1))))). % 5.54/2.32 tff(c_682, plain, (![U_1, V_306]: (ssPv6(U_1) | ~ssPv8(V_306) | ~ssRr(U_1, V_306) | ssPv3(U_1) | ssPv1(skf1(U_1)) | ssPv4(U_1) | ~ssPv5(U_1) | ~ssPv2(skf1(U_1))))). % 5.54/2.33 tff(c_669, plain, (![U_1, V_304]: (ssPv6(U_1) | ~ssPv5(skf1(U_1)) | ~ssPv8(V_304) | ~ssRr(U_1, V_304) | ssPv3(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1))))). % 5.54/2.33 tff(c_428, plain, (![U_249, W_212, V_213]: (ssPv6(U_249) | ~ssPv5(W_212) | ~ssRr(U_249, W_212) | ~ssPv8(V_213) | ~ssRr(U_249, V_213) | ssPv3(U_249) | ssPv1(skf1(U_249)) | ~ssPv2(skf1(U_249))))). % 5.54/2.33 tff(c_661, plain, (![U_206]: (ssPv1(skf1(U_206)) | ssPv2(skf1(U_206)) | ~ssPv3(skf1(U_206)) | ssPv6(U_206) | ssPv4(U_206) | ssPv2(U_206) | ~ssPv3(U_206)))). % 5.54/2.33 tff(c_318, plain, (![U_1]: (ssPv6(U_1) | ssPv4(U_1) | ssPv2(U_1) | ~ssPv6(skf1(U_1)) | ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv3(skf1(U_1))))). % 5.54/2.33 tff(c_640, plain, (![U_206]: (ssPv1(skf1(U_206)) | ssPv2(skf1(U_206)) | ~ssPv3(skf1(U_206)) | ssPv1(U_206) | ssPv2(U_206) | ~ssPv3(U_206)))). % 5.54/2.33 tff(c_616, plain, (![U_296]: (ssPv1(skf1(U_296)) | ssPv7(U_296) | ssPv6(U_296) | ~ssPv1(U_296) | ssPv3(U_296) | ~ssPv8(U_296) | ssPv5(U_296) | ~ssPv4(U_296)))). % 5.54/2.33 tff(c_595, plain, (![U_1]: (ssPv2(U_1) | ~ssPv5(U_1) | ~ssPv8(skf1(U_1)) | ssPv3(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1))))). % 5.54/2.33 tff(c_430, plain, (![U_249, V_193]: (ssPv2(U_249) | ~ssPv5(U_249) | ~ssPv8(V_193) | ~ssRr(U_249, V_193) | ssPv3(U_249) | ssPv1(skf1(U_249)) | ~ssPv2(skf1(U_249))))). % 5.54/2.33 tff(c_580, plain, (![U_190]: (ssPv3(U_190) | ~ssPv2(U_190) | ~ssPv8(U_190) | ssPv5(U_190) | ssPv2(skf1(U_190)) | ~ssPv4(U_190)))). % 5.54/2.33 tff(c_483, plain, (![U_266]: (ssPv8(U_266) | ssPv5(U_266) | ssPv3(U_266) | ssPv2(U_266) | ssPv7(U_266) | ssPv3(skf1(U_266)) | ~ssPv4(skf1(U_266))))). % 5.54/2.33 tff(c_466, plain, (![U_190]: (ssPv1(skf1(U_190)) | ~ssPv6(U_190) | ssPv3(U_190) | ~ssPv8(U_190) | ssPv5(U_190) | ssPv2(skf1(U_190)) | ~ssPv4(U_190)))). % 5.54/2.33 tff(c_542, plain, (![U_1]: (ssPv6(U_1) | ssPv6(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ~ssPv5(skf1(U_1))))). % 5.54/2.33 tff(c_538, plain, (![U_1, V_285]: (ssPv6(U_1) | ssPv6(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ~ssPv5(V_285) | ~ssRr(U_1, V_285)))). % 5.54/2.33 tff(c_534, plain, (![U_1, W_281, V_282]: (ssPv6(U_1) | ssPv6(skf1(U_1)) | ~ssPv2(W_281) | ~ssRr(U_1, W_281) | ~ssPv5(V_282) | ~ssRr(U_1, V_282)))). % 5.54/2.33 tff(c_54, plain, (![U_72, X_75, W_74, V_73]: (ssPv6(U_72) | ssPv6(X_75) | ~ssRr(U_72, X_75) | ~ssPv2(W_74) | ~ssRr(U_72, W_74) | ~ssPv5(V_73) | ~ssRr(U_72, V_73)))). % 5.54/2.33 tff(c_504, plain, (![U_276]: (ssPv3(U_276) | ssPv4(skf1(U_276)) | ~ssPv8(U_276) | ssPv1(skf1(U_276)) | ssPv7(skf1(U_276)) | ~ssPv2(U_276)))). % 5.54/2.33 tff(c_503, plain, (![U_276]: (ssPv5(skf1(U_276)) | ~ssPv8(U_276) | ~ssPv4(U_276) | ssPv1(skf1(U_276)) | ssPv7(skf1(U_276)) | ~ssPv2(U_276)))). % 5.54/2.33 tff(c_495, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv7(skf1(U_1)) | ssPv8(skf1(U_1)) | ~ssPv2(U_1)))). % 5.54/2.33 tff(c_491, plain, (![U_1, V_273]: (ssPv1(skf1(U_1)) | ssPv7(skf1(U_1)) | ssPv8(V_273) | ~ssPv2(U_1) | ~ssRr(U_1, V_273)))). % 5.54/2.33 tff(c_487, plain, (![U_1, W_268, V_269]: (ssPv1(skf1(U_1)) | ssPv7(W_268) | ssPv8(V_269) | ~ssPv2(U_1) | ~ssRr(U_1, W_268) | ~ssRr(U_1, V_269)))). % 5.54/2.33 tff(c_48, plain, (![X_63, W_62, V_61, U_60]: (ssPv1(X_63) | ssPv7(W_62) | ssPv8(V_61) | ~ssPv2(U_60) | ~ssRr(U_60, X_63) | ~ssRr(U_60, W_62) | ~ssRr(U_60, V_61)))). % 5.54/2.33 tff(c_478, plain, (![U_1]: (ssPv7(U_1) | ssPv3(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv4(skf1(U_1))))). % 5.54/2.33 tff(c_474, plain, (![U_1, V_263]: (ssPv7(U_1) | ssPv3(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv4(V_263) | ~ssRr(U_1, V_263)))). % 5.54/2.33 tff(c_470, plain, (![U_1, W_259, V_260]: (ssPv7(U_1) | ssPv3(skf1(U_1)) | ssPv5(W_259) | ~ssRr(U_1, W_259) | ~ssPv4(V_260) | ~ssRr(U_1, V_260)))). % 5.54/2.33 tff(c_50, plain, (![U_64, X_67, W_66, V_65]: (ssPv7(U_64) | ssPv3(X_67) | ssPv5(W_66) | ~ssRr(U_64, X_67) | ~ssRr(U_64, W_66) | ~ssPv4(V_65) | ~ssRr(U_64, V_65)))). % 5.54/2.33 tff(c_457, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv6(U_1) | ~ssPv4(skf1(U_1))))). % 5.54/2.33 tff(c_453, plain, (![U_1, V_253]: (ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv6(U_1) | ~ssPv4(V_253) | ~ssRr(U_1, V_253)))). % 5.54/2.33 tff(c_414, plain, (![U_1, W_246, V_248]: (ssPv1(skf1(U_1)) | ssPv2(W_246) | ~ssPv6(U_1) | ~ssRr(U_1, W_246) | ~ssPv4(V_248) | ~ssRr(U_1, V_248)))). % 5.54/2.33 tff(c_432, plain, (![U_249]: (ssPv7(U_249) | ssPv6(U_249) | ~ssPv1(U_249) | ssPv3(U_249) | ssPv1(skf1(U_249)) | ~ssPv2(skf1(U_249))))). % 5.54/2.33 tff(c_410, plain, (![U_1]: (ssPv3(U_1) | ssPv1(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv2(skf1(U_1))))). % 5.54/2.33 tff(c_56, plain, (![X_79, W_78, U_76, V_77]: (ssPv1(X_79) | ssPv2(W_78) | ~ssPv6(U_76) | ~ssRr(U_76, X_79) | ~ssRr(U_76, W_78) | ~ssPv4(V_77) | ~ssRr(U_76, V_77)))). % 5.54/2.33 tff(c_406, plain, (![U_1, V_242]: (ssPv3(U_1) | ssPv1(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv2(V_242) | ~ssRr(U_1, V_242)))). % 5.54/2.33 tff(c_385, plain, (![U_1, W_237, V_238]: (ssPv3(U_1) | ssPv1(skf1(U_1)) | ssPv4(W_237) | ~ssRr(U_1, W_237) | ~ssPv2(V_238) | ~ssRr(U_1, V_238)))). % 5.54/2.33 tff(c_381, plain, (![U_1]: (~ssPv7(skf1(U_1)) | ssPv3(U_1) | ~ssPv8(U_1) | ssPv5(U_1) | ssPv2(skf1(U_1)) | ~ssPv4(U_1)))). % 5.54/2.33 tff(c_52, plain, (![U_68, X_71, W_70, V_69]: (ssPv3(U_68) | ssPv1(X_71) | ssPv4(W_70) | ~ssRr(U_68, X_71) | ~ssRr(U_68, W_70) | ~ssPv2(V_69) | ~ssRr(U_68, V_69)))). % 5.54/2.33 tff(c_347, plain, (![V_219, U_190]: (~ssPv7(V_219) | ~ssRr(U_190, V_219) | ssPv3(U_190) | ~ssPv8(U_190) | ssPv5(U_190) | ssPv2(skf1(U_190)) | ~ssPv4(U_190)))). % 5.54/2.33 tff(c_364, plain, (![U_1]: (ssPv8(U_1) | ssPv5(U_1) | ~ssPv5(skf1(U_1)) | ssPv7(U_1) | ssPv3(U_1) | ssPv2(U_1)))). % 5.54/2.33 tff(c_141, plain, (![U_1, V_128]: (ssPv8(U_1) | ssPv5(U_1) | ~ssPv5(V_128) | ~ssRr(U_1, V_128) | ssPv7(U_1) | ssPv3(U_1) | ssPv2(U_1)))). % 5.54/2.33 tff(c_351, plain, (![U_1, W_222, V_223]: (ssPv1(skf1(U_1)) | ~ssPv6(U_1) | ~ssPv1(W_222) | ~ssRr(U_1, W_222) | ~ssPv5(V_223) | ~ssRr(U_1, V_223)))). % 5.54/2.33 tff(c_327, plain, (![U_1, W_212, V_213]: (ssPv6(U_1) | ~ssPv4(skf1(U_1)) | ~ssPv5(W_212) | ~ssRr(U_1, W_212) | ~ssPv8(V_213) | ~ssRr(U_1, V_213)))). % 5.54/2.33 tff(c_60, plain, (![X_87, U_84, W_86, V_85]: (ssPv1(X_87) | ~ssPv6(U_84) | ~ssRr(U_84, X_87) | ~ssPv1(W_86) | ~ssRr(U_84, W_86) | ~ssPv5(V_85) | ~ssRr(U_84, V_85)))). % 5.54/2.33 tff(c_343, plain, (![U_1, V_217]: (ssPv2(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv4(skf1(U_1)) | ~ssPv7(V_217) | ~ssRr(U_1, V_217)))). % 5.54/2.33 tff(c_291, plain, (![U_1, W_202, V_203]: (ssPv2(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv4(W_202) | ~ssRr(U_1, W_202) | ~ssPv7(V_203) | ~ssRr(U_1, V_203)))). % 5.54/2.33 tff(c_277, plain, (![U_190]: (ssPv3(U_190) | ssPv4(skf1(U_190)) | ~ssPv8(U_190) | ssPv5(U_190) | ssPv2(skf1(U_190)) | ~ssPv4(U_190)))). % 5.54/2.33 tff(c_58, plain, (![U_80, X_83, W_82, V_81]: (ssPv6(U_80) | ~ssPv4(X_83) | ~ssRr(U_80, X_83) | ~ssPv5(W_82) | ~ssRr(U_80, W_82) | ~ssPv8(V_81) | ~ssRr(U_80, V_81)))). % 5.54/2.33 tff(c_304, plain, (![U_206]: (ssPv6(U_206) | ssPv4(U_206) | ssPv2(U_206) | ssPv6(skf1(U_206)) | ~ssPv3(U_206)))). % 5.54/2.33 tff(c_309, plain, (![U_207]: (ssPv7(U_207) | ~ssPv6(U_207) | ssPv1(U_207) | ssPv2(U_207) | ~ssPv3(U_207)))). % 5.54/2.33 tff(c_303, plain, (![U_206]: (ssPv1(U_206) | ssPv2(U_206) | ssPv6(skf1(U_206)) | ~ssPv3(U_206)))). % 5.54/2.34 tff(c_295, plain, (![U_1]: (ssPv2(U_1) | ssPv6(skf1(U_1)) | ssPv7(skf1(U_1)) | ~ssPv3(U_1)))). % 5.54/2.34 tff(c_287, plain, (![U_1, V_199]: (ssPv2(U_1) | ssPv6(skf1(U_1)) | ssPv7(V_199) | ~ssPv3(U_1) | ~ssRr(U_1, V_199)))). % 5.54/2.34 tff(c_62, plain, (![X_91, U_88, W_90, V_89]: (ssPv2(X_91) | ~ssPv4(U_88) | ~ssRr(U_88, X_91) | ~ssPv4(W_90) | ~ssRr(U_88, W_90) | ~ssPv7(V_89) | ~ssRr(U_88, V_89)))). % 5.54/2.34 tff(c_30, plain, (![U_33, W_35, V_34]: (ssPv2(U_33) | ssPv6(W_35) | ssPv7(V_34) | ~ssPv3(U_33) | ~ssRr(U_33, W_35) | ~ssRr(U_33, V_34)))). % 5.54/2.34 tff(c_276, plain, (![U_190]: (ssPv5(skf1(U_190)) | ~ssPv8(U_190) | ssPv5(U_190) | ssPv2(skf1(U_190)) | ~ssPv4(U_190)))). % 5.54/2.34 tff(c_281, plain, (![U_1, V_193]: (ssPv2(U_1) | ~ssPv5(U_1) | ~ssPv4(skf1(U_1)) | ~ssPv8(V_193) | ~ssRr(U_1, V_193)))). % 5.54/2.34 tff(c_46, plain, (![U_57, W_59, V_58]: (ssPv2(U_57) | ~ssPv5(U_57) | ~ssPv4(W_59) | ~ssRr(U_57, W_59) | ~ssPv8(V_58) | ~ssRr(U_57, V_58)))). % 5.54/2.34 tff(c_268, plain, (![U_1]: (ssPv5(U_1) | ssPv2(skf1(U_1)) | ssPv8(skf1(U_1)) | ~ssPv4(U_1)))). % 5.54/2.34 tff(c_264, plain, (![U_1, V_187]: (ssPv5(U_1) | ssPv2(skf1(U_1)) | ssPv8(V_187) | ~ssPv4(U_1) | ~ssRr(U_1, V_187)))). % 5.54/2.34 tff(c_26, plain, (![U_27, W_29, V_28]: (ssPv5(U_27) | ssPv2(W_29) | ssPv8(V_28) | ~ssPv4(U_27) | ~ssRr(U_27, W_29) | ~ssRr(U_27, V_28)))). % 5.54/2.34 tff(c_255, plain, (![U_1]: (ssPv5(skf1(U_1)) | ~ssPv8(U_1) | ~ssPv4(U_1) | ~ssPv8(skf1(U_1))))). % 5.54/2.34 tff(c_251, plain, (![U_1, V_181]: (ssPv5(skf1(U_1)) | ~ssPv8(U_1) | ~ssPv4(U_1) | ~ssPv8(V_181) | ~ssRr(U_1, V_181)))). % 5.54/2.34 tff(c_44, plain, (![W_56, U_54, V_55]: (ssPv5(W_56) | ~ssPv8(U_54) | ~ssPv4(U_54) | ~ssRr(U_54, W_56) | ~ssPv8(V_55) | ~ssRr(U_54, V_55)))). % 5.54/2.34 tff(c_246, plain, (![U_1]: (ssPv3(U_1) | ssPv3(skf1(U_1)) | ssPv5(skf1(U_1)) | ~ssPv5(U_1)))). % 5.54/2.34 tff(c_237, plain, (![U_1, V_174]: (ssPv3(U_1) | ssPv3(skf1(U_1)) | ssPv5(V_174) | ~ssPv5(U_1) | ~ssRr(U_1, V_174)))). % 5.54/2.34 tff(c_233, plain, (![U_1]: (ssPv8(U_1) | ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv6(U_1)))). % 5.54/2.34 tff(c_28, plain, (![U_30, W_32, V_31]: (ssPv3(U_30) | ssPv3(W_32) | ssPv5(V_31) | ~ssPv5(U_30) | ~ssRr(U_30, W_32) | ~ssRr(U_30, V_31)))). % 5.54/2.34 tff(c_229, plain, (![U_1, V_169]: (ssPv8(U_1) | ssPv1(skf1(U_1)) | ssPv2(V_169) | ~ssPv6(U_1) | ~ssRr(U_1, V_169)))). % 5.54/2.34 tff(c_24, plain, (![U_24, W_26, V_25]: (ssPv8(U_24) | ssPv1(W_26) | ssPv2(V_25) | ~ssPv6(U_24) | ~ssRr(U_24, W_26) | ~ssRr(U_24, V_25)))). % 5.54/2.34 tff(c_220, plain, (![U_1]: (ssPv3(U_1) | ssPv4(skf1(U_1)) | ~ssPv8(U_1) | ~ssPv8(skf1(U_1))))). % 5.54/2.34 tff(c_211, plain, (![U_1, V_162]: (ssPv3(U_1) | ssPv4(skf1(U_1)) | ~ssPv8(U_1) | ~ssPv8(V_162) | ~ssRr(U_1, V_162)))). % 5.54/2.34 tff(c_207, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv6(U_1) | ~ssPv5(U_1)))). % 5.54/2.34 tff(c_38, plain, (![U_45, W_47, V_46]: (ssPv3(U_45) | ssPv4(W_47) | ~ssPv8(U_45) | ~ssRr(U_45, W_47) | ~ssPv8(V_46) | ~ssRr(U_45, V_46)))). % 5.54/2.34 tff(c_198, plain, (![U_1, V_153]: (ssPv1(skf1(U_1)) | ssPv2(V_153) | ~ssPv6(U_1) | ~ssPv5(U_1) | ~ssRr(U_1, V_153)))). % 5.54/2.34 tff(c_202, plain, (![U_1]: (ssPv4(U_1) | ssPv5(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv2(skf1(U_1))))). % 5.54/2.34 tff(c_194, plain, (![U_1, V_151]: (ssPv4(U_1) | ssPv5(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv2(V_151) | ~ssRr(U_1, V_151)))). % 5.54/2.34 tff(c_32, plain, (![W_38, V_37, U_36]: (ssPv1(W_38) | ssPv2(V_37) | ~ssPv6(U_36) | ~ssPv5(U_36) | ~ssRr(U_36, W_38) | ~ssRr(U_36, V_37)))). % 5.54/2.34 tff(c_36, plain, (![U_42, W_44, V_43]: (ssPv4(U_42) | ssPv5(W_44) | ~ssPv5(U_42) | ~ssRr(U_42, W_44) | ~ssPv2(V_43) | ~ssRr(U_42, V_43)))). % 5.54/2.34 tff(c_185, plain, (![U_1]: (ssPv4(U_1) | ssPv3(U_1) | ssPv4(skf1(U_1)) | ssPv6(skf1(U_1))))). % 5.54/2.34 tff(c_172, plain, (![U_1, V_142]: (ssPv4(U_1) | ssPv3(U_1) | ssPv4(skf1(U_1)) | ssPv6(V_142) | ~ssRr(U_1, V_142)))). % 5.54/2.34 tff(c_176, plain, (![U_1]: (ssPv2(U_1) | ssPv6(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(skf1(U_1))))). % 5.54/2.34 tff(c_168, plain, (![U_1, V_139]: (ssPv2(U_1) | ssPv6(skf1(U_1)) | ~ssPv7(U_1) | ~ssPv4(V_139) | ~ssRr(U_1, V_139)))). % 5.54/2.34 tff(c_22, plain, (![U_21, W_23, V_22]: (ssPv4(U_21) | ssPv3(U_21) | ssPv4(W_23) | ssPv6(V_22) | ~ssRr(U_21, W_23) | ~ssRr(U_21, V_22)))). % 5.54/2.34 tff(c_42, plain, (![U_51, W_53, V_52]: (ssPv2(U_51) | ssPv6(W_53) | ~ssPv7(U_51) | ~ssRr(U_51, W_53) | ~ssPv4(V_52) | ~ssRr(U_51, V_52)))). % 5.54/2.34 tff(c_155, plain, (![U_1]: (ssPv3(U_1) | ssPv7(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv5(skf1(U_1))))). % 5.54/2.34 tff(c_151, plain, (![U_1, V_133]: (ssPv3(U_1) | ssPv7(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv5(V_133) | ~ssRr(U_1, V_133)))). % 5.54/2.34 tff(c_40, plain, (![U_48, W_50, V_49]: (ssPv3(U_48) | ssPv7(W_50) | ~ssPv2(U_48) | ~ssRr(U_48, W_50) | ~ssPv5(V_49) | ~ssRr(U_48, V_49)))). % 5.54/2.34 tff(c_146, plain, (![U_129]: (~ssPv4(U_129) | ssPv2(U_129) | ssPv1(U_129) | ~ssPv3(U_129) | ssPv8(U_129) | ssPv6(U_129)))). % 5.54/2.34 tff(c_131, plain, (![U_125]: (ssPv2(U_125) | ssPv1(U_125) | ~ssPv3(U_125) | ssPv8(U_125) | ssPv6(U_125) | ssPv2(skf1(U_125))))). % 5.54/2.34 tff(c_123, plain, (![U_1, V_124]: (ssPv8(U_1) | ssPv5(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv5(V_124) | ~ssRr(U_1, V_124)))). % 5.54/2.34 tff(c_132, plain, (![U_125]: (ssPv4(U_125) | ssPv2(U_125) | ssPv8(U_125) | ssPv6(U_125) | ssPv2(skf1(U_125))))). % 5.54/2.34 tff(c_119, plain, (![U_1]: (ssPv8(U_1) | ssPv6(U_1) | ssPv2(skf1(U_1)) | ssPv7(skf1(U_1))))). % 5.54/2.34 tff(c_34, plain, (![U_39, W_41, V_40]: (ssPv8(U_39) | ssPv5(U_39) | ~ssPv1(W_41) | ~ssRr(U_39, W_41) | ~ssPv5(V_40) | ~ssRr(U_39, V_40)))). % 5.54/2.34 tff(c_115, plain, (![U_1, V_119]: (ssPv8(U_1) | ssPv6(U_1) | ssPv2(skf1(U_1)) | ssPv7(V_119) | ~ssRr(U_1, V_119)))). % 5.54/2.34 tff(c_20, plain, (![U_18, W_20, V_19]: (ssPv8(U_18) | ssPv6(U_18) | ssPv2(W_20) | ssPv7(V_19) | ~ssRr(U_18, W_20) | ~ssRr(U_18, V_19)))). % 5.54/2.34 tff(c_110, plain, (![U_1]: (ssPv8(U_1) | ssPv6(U_1) | ~ssPv2(U_1) | ~ssPv3(skf1(U_1))))). % 5.54/2.34 tff(c_10, plain, (![U_8, V_9]: (ssPv8(U_8) | ssPv6(U_8) | ~ssPv2(U_8) | ~ssPv3(V_9) | ~ssRr(U_8, V_9)))). % 5.54/2.34 tff(c_104, plain, (![U_1]: (ssPv5(U_1) | ~ssPv8(U_1) | ~ssPv3(U_1) | ~ssPv4(skf1(U_1))))). % 5.54/2.34 tff(c_18, plain, (![U_16, V_17]: (ssPv5(U_16) | ~ssPv8(U_16) | ~ssPv3(U_16) | ~ssPv4(V_17) | ~ssRr(U_16, V_17)))). % 5.54/2.34 tff(c_98, plain, (![U_1]: (ssPv2(U_1) | ssPv1(U_1) | ~ssPv3(U_1) | ~ssPv7(skf1(U_1))))). % 5.54/2.34 tff(c_14, plain, (![U_12, V_13]: (ssPv2(U_12) | ssPv1(U_12) | ~ssPv3(U_12) | ~ssPv7(V_13) | ~ssRr(U_12, V_13)))). % 5.54/2.34 tff(c_92, plain, (![U_1]: (ssPv7(U_1) | ssPv6(U_1) | ~ssPv1(U_1) | ~ssPv4(skf1(U_1))))). % 5.54/2.34 tff(c_12, plain, (![U_10, V_11]: (ssPv7(U_10) | ssPv6(U_10) | ~ssPv1(U_10) | ~ssPv4(V_11) | ~ssRr(U_10, V_11)))). % 5.54/2.34 tff(c_86, plain, (![U_1]: (ssPv7(U_1) | ~ssPv6(U_1) | ~ssPv3(U_1) | ~ssPv6(skf1(U_1))))). % 5.54/2.34 tff(c_16, plain, (![U_14, V_15]: (ssPv7(U_14) | ~ssPv6(U_14) | ~ssPv3(U_14) | ~ssPv6(V_15) | ~ssRr(U_14, V_15)))). % 5.54/2.34 tff(c_80, plain, (![U_1]: (ssPv6(U_1) | ssPv4(U_1) | ssPv2(U_1) | ~ssPv7(skf1(U_1))))). % 5.54/2.34 tff(c_6, plain, (![U_4, V_5]: (ssPv6(U_4) | ssPv4(U_4) | ssPv2(U_4) | ~ssPv7(V_5) | ~ssRr(U_4, V_5)))). % 5.54/2.34 tff(c_74, plain, (![U_1]: (ssPv8(U_1) | ssPv6(U_1) | ~ssPv4(U_1) | ~ssPv2(skf1(U_1))))). % 5.54/2.34 tff(c_8, plain, (![U_6, V_7]: (ssPv8(U_6) | ssPv6(U_6) | ~ssPv4(U_6) | ~ssPv2(V_7) | ~ssRr(U_6, V_7)))). % 5.54/2.34 tff(c_68, plain, (![U_1]: (ssPv7(U_1) | ssPv3(U_1) | ssPv2(U_1) | ssPv1(skf1(U_1))))). % 5.54/2.34 tff(c_4, plain, (![U_2, V_3]: (ssPv7(U_2) | ssPv3(U_2) | ssPv2(U_2) | ssPv1(V_3) | ~ssRr(U_2, V_3)))). % 5.54/2.34 tff(c_2, plain, (![U_1]: (ssRr(U_1, skf1(U_1))))). % 5.54/2.34 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.54/2.34 %------------------------------------------------------------------------------