%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN736-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 : 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:04:20 PM UTC 2025 % Result : Satisfiable 6.16s 2.41s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SYN736-1 : TPTP v9.0.0. Released v2.5.0. % 0.06/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.12/0.34 % Computer : n012.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Wed Apr 9 08:13:29 EDT 2025 % 0.12/0.34 % CPUTime : % 6.16/2.41 % 6.16/2.41 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.16/2.41 % 6.16/2.41 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.16/2.42 %$ ssRr > ssPv4 > ssPv3 > ssPv2 > ssPv1 > #nlpp > skf1 % 6.16/2.42 % 6.16/2.42 %Foreground sorts: % 6.16/2.42 % 6.16/2.42 % 6.16/2.42 %Background operators: % 6.16/2.42 % 6.16/2.42 % 6.16/2.42 %Foreground operators: % 6.16/2.42 tff(skf1, type, skf1: $i > $i). % 6.16/2.42 tff(ssPv1, type, ssPv1: $i > $o). % 6.16/2.42 tff(ssPv3, type, ssPv3: $i > $o). % 6.16/2.42 tff(ssRr, type, ssRr: ($i * $i) > $o). % 6.16/2.42 tff(ssPv4, type, ssPv4: $i > $o). % 6.16/2.42 tff(ssPv2, type, ssPv2: $i > $o). % 6.16/2.42 % 6.16/2.42 %Saturated clause set: % 6.16/2.42 tff(c_751, plain, (![U_535, U_537, V_538]: (~ssPv4(skf1(skf1(U_535))) | ~ssPv1(skf1(skf1(skf1(skf1(U_535))))) | ~ssRr(skf1(skf1(U_535)), U_537) | ~ssPv4(V_538) | ~ssRr(U_537, V_538) | ssPv2(skf1(U_535)) | ssPv1(skf1(U_535)) | ssPv3(skf1(U_535)) | ssPv3(U_535) | ssPv2(skf1(skf1(U_535))) | ~ssPv3(skf1(skf1(U_535)))))). % 6.16/2.42 tff(c_746, plain, (![U_534, Y_533, U_530, V_531]: (~ssPv4(skf1(skf1(U_534))) | ~ssPv1(Y_533) | ~ssRr(skf1(skf1(skf1(U_534))), Y_533) | ~ssRr(skf1(skf1(U_534)), U_530) | ~ssPv4(V_531) | ~ssRr(U_530, V_531) | ssPv2(skf1(U_534)) | ssPv1(skf1(U_534)) | ssPv3(skf1(U_534)) | ssPv3(U_534) | ssPv2(skf1(skf1(U_534))) | ~ssPv3(skf1(skf1(U_534)))))). % 6.25/2.42 tff(c_610, plain, (![X_275, V_276, U_274, Y_273, U_498]: (~ssPv4(skf1(skf1(U_498))) | ~ssRr(skf1(skf1(U_498)), X_275) | ~ssPv1(Y_273) | ~ssRr(X_275, Y_273) | ~ssRr(skf1(skf1(U_498)), U_274) | ~ssPv4(V_276) | ~ssRr(U_274, V_276) | ssPv2(skf1(U_498)) | ssPv1(skf1(U_498)) | ssPv3(skf1(U_498)) | ssPv3(U_498) | ssPv2(skf1(skf1(U_498))) | ~ssPv3(skf1(skf1(U_498)))))). % 6.25/2.42 tff(c_728, plain, (![U_523, U_525, V_526]: (~ssPv4(skf1(skf1(U_523))) | ~ssPv1(skf1(skf1(skf1(skf1(U_523))))) | ~ssRr(skf1(skf1(U_523)), U_525) | ~ssPv4(V_526) | ~ssRr(U_525, V_526) | ssPv2(skf1(U_523)) | ssPv1(skf1(U_523)) | ssPv3(skf1(U_523)) | ssPv1(U_523) | ~ssPv3(U_523) | ~ssPv3(skf1(skf1(U_523)))))). % 6.25/2.42 tff(c_723, plain, (![U_522, Y_521, U_518, V_519]: (~ssPv4(skf1(skf1(U_522))) | ~ssPv1(Y_521) | ~ssRr(skf1(skf1(skf1(U_522))), Y_521) | ~ssRr(skf1(skf1(U_522)), U_518) | ~ssPv4(V_519) | ~ssRr(U_518, V_519) | ssPv2(skf1(U_522)) | ssPv1(skf1(U_522)) | ssPv3(skf1(U_522)) | ssPv1(U_522) | ~ssPv3(U_522) | ~ssPv3(skf1(skf1(U_522)))))). % 6.25/2.42 tff(c_525, plain, (![X_275, V_276, U_274, Y_273, U_469]: (~ssPv4(skf1(skf1(U_469))) | ~ssRr(skf1(skf1(U_469)), X_275) | ~ssPv1(Y_273) | ~ssRr(X_275, Y_273) | ~ssRr(skf1(skf1(U_469)), U_274) | ~ssPv4(V_276) | ~ssRr(U_274, V_276) | ssPv2(skf1(U_469)) | ssPv1(skf1(U_469)) | ssPv3(skf1(U_469)) | ssPv1(U_469) | ~ssPv3(U_469) | ~ssPv3(skf1(skf1(U_469)))))). % 6.25/2.43 tff(c_697, plain, (![U_515]: (ssPv4(skf1(U_515)) | ~ssPv3(skf1(skf1(skf1(U_515)))) | ~ssPv4(U_515) | ssPv2(skf1(U_515)) | ssPv1(skf1(U_515)) | ssPv3(skf1(U_515)) | ssPv3(U_515) | ssPv2(skf1(skf1(U_515))) | ~ssPv3(skf1(skf1(U_515)))))). % 6.25/2.43 tff(c_691, plain, (![U_512, V_514]: (ssPv4(skf1(U_512)) | ~ssPv3(V_514) | ~ssRr(skf1(skf1(U_512)), V_514) | ~ssPv4(U_512) | ssPv2(skf1(U_512)) | ssPv1(skf1(U_512)) | ssPv3(skf1(U_512)) | ssPv3(U_512) | ssPv2(skf1(skf1(U_512))) | ~ssPv3(skf1(skf1(U_512)))))). % 6.25/2.43 tff(c_605, plain, (![U_498, U_478, V_479]: (ssPv4(skf1(U_498)) | ~ssRr(skf1(U_498), U_478) | ~ssPv3(V_479) | ~ssRr(U_478, V_479) | ~ssPv4(U_498) | ssPv2(skf1(U_498)) | ssPv1(skf1(U_498)) | ssPv3(skf1(U_498)) | ssPv3(U_498) | ssPv2(skf1(skf1(U_498))) | ~ssPv3(skf1(skf1(U_498)))))). % 6.25/2.43 tff(c_665, plain, (![U_509]: (ssPv4(skf1(U_509)) | ~ssPv3(skf1(skf1(skf1(U_509)))) | ssPv2(U_509) | ssPv2(skf1(U_509)) | ssPv1(skf1(U_509)) | ssPv3(skf1(U_509)) | ssPv1(U_509) | ~ssPv3(U_509) | ~ssPv3(skf1(skf1(U_509)))))). % 6.25/2.43 tff(c_659, plain, (![U_506, V_508]: (ssPv4(skf1(U_506)) | ~ssPv3(V_508) | ~ssRr(skf1(skf1(U_506)), V_508) | ssPv2(U_506) | ssPv2(skf1(U_506)) | ssPv1(skf1(U_506)) | ssPv3(skf1(U_506)) | ssPv1(U_506) | ~ssPv3(U_506) | ~ssPv3(skf1(skf1(U_506)))))). % 6.25/2.43 tff(c_522, plain, (![U_469, U_437, V_438]: (ssPv4(skf1(U_469)) | ~ssRr(skf1(U_469), U_437) | ~ssPv3(V_438) | ~ssRr(U_437, V_438) | ssPv2(U_469) | ssPv2(skf1(U_469)) | ssPv1(skf1(U_469)) | ssPv3(skf1(U_469)) | ssPv1(U_469) | ~ssPv3(U_469) | ~ssPv3(skf1(skf1(U_469)))))). % 6.25/2.43 tff(c_633, plain, (![U_503]: (ssPv4(skf1(U_503)) | ~ssPv3(skf1(skf1(skf1(U_503)))) | ~ssPv4(U_503) | ssPv2(skf1(U_503)) | ssPv1(skf1(U_503)) | ssPv3(skf1(U_503)) | ssPv1(U_503) | ~ssPv3(U_503) | ~ssPv3(skf1(skf1(U_503)))))). % 6.25/2.43 tff(c_627, plain, (![U_500, V_502]: (ssPv4(skf1(U_500)) | ~ssPv3(V_502) | ~ssRr(skf1(skf1(U_500)), V_502) | ~ssPv4(U_500) | ssPv2(skf1(U_500)) | ssPv1(skf1(U_500)) | ssPv3(skf1(U_500)) | ssPv1(U_500) | ~ssPv3(U_500) | ~ssPv3(skf1(skf1(U_500)))))). % 6.25/2.43 tff(c_554, plain, (![U_468, U_481, V_482]: (ssPv4(skf1(U_468)) | ~ssRr(skf1(U_468), U_481) | ~ssPv3(V_482) | ~ssRr(U_481, V_482) | ~ssPv4(U_468) | ssPv2(skf1(U_468)) | ssPv1(skf1(U_468)) | ssPv3(skf1(U_468)) | ssPv1(U_468) | ~ssPv3(U_468) | ~ssPv3(skf1(skf1(U_468)))))). % 6.25/2.43 tff(c_588, plain, (![U_497]: (ssPv3(skf1(skf1(skf1(U_497)))) | ~ssPv2(skf1(U_497)) | ssPv3(skf1(U_497)) | ssPv1(skf1(skf1(skf1(U_497)))) | ssPv3(U_497) | ssPv2(skf1(skf1(U_497))) | ~ssPv3(skf1(skf1(U_497)))))). % 6.25/2.43 tff(c_590, plain, (![U_497]: (ssPv2(skf1(U_497)) | ssPv1(skf1(U_497)) | ssPv3(skf1(U_497)) | ssPv1(skf1(skf1(skf1(U_497)))) | ssPv3(U_497) | ssPv2(skf1(skf1(U_497))) | ~ssPv3(skf1(skf1(U_497)))))). % 6.25/2.43 tff(c_575, plain, (![U_495]: (ssPv3(skf1(U_495)) | ssPv1(skf1(skf1(skf1(U_495)))) | ssPv4(skf1(skf1(skf1(U_495)))) | ssPv3(U_495) | ssPv2(skf1(skf1(U_495))) | ~ssPv3(skf1(skf1(U_495)))))). % 6.25/2.43 tff(c_570, plain, (![U_492, V_493]: (ssPv3(skf1(U_492)) | ssPv1(skf1(skf1(skf1(U_492)))) | ssPv4(V_493) | ~ssRr(skf1(skf1(U_492)), V_493) | ssPv3(U_492) | ssPv2(skf1(skf1(U_492))) | ~ssPv3(skf1(skf1(U_492)))))). % 6.25/2.43 tff(c_565, plain, (![U_488, V_490, U_491]: (ssPv3(skf1(U_488)) | ssPv1(skf1(skf1(skf1(U_488)))) | ssPv4(V_490) | ~ssRr(skf1(U_488), U_491) | ~ssRr(U_491, V_490) | ssPv3(U_488) | ssPv2(skf1(skf1(U_488))) | ~ssPv3(skf1(skf1(U_488)))))). % 6.25/2.43 tff(c_560, plain, (![U_487, Y_486, V_485, U_483]: (ssPv3(skf1(U_487)) | ssPv1(Y_486) | ssPv4(V_485) | ~ssRr(skf1(skf1(U_487)), Y_486) | ~ssRr(skf1(U_487), U_483) | ~ssRr(U_483, V_485) | ssPv3(U_487) | ssPv2(skf1(skf1(U_487))) | ~ssPv3(skf1(skf1(U_487)))))). % 6.25/2.43 tff(c_368, plain, (![U_414, U_303, Y_304, X_306, V_305]: (ssPv3(skf1(U_414)) | ssPv1(Y_304) | ssPv4(V_305) | ~ssRr(skf1(U_414), X_306) | ~ssRr(X_306, Y_304) | ~ssRr(skf1(U_414), U_303) | ~ssRr(U_303, V_305) | ssPv3(U_414) | ssPv2(skf1(skf1(U_414))) | ~ssPv3(skf1(skf1(U_414)))))). % 6.25/2.43 tff(c_547, plain, (![U_476, U_478, V_479]: (ssPv4(skf1(U_476)) | ~ssPv1(skf1(skf1(skf1(U_476)))) | ~ssRr(skf1(U_476), U_478) | ~ssPv3(V_479) | ~ssRr(U_478, V_479) | ssPv2(skf1(U_476)) | ssPv3(skf1(U_476)) | ~ssPv4(U_476)))). % 6.25/2.43 tff(c_542, plain, (![U_471, Y_474, U_473, V_472]: (ssPv4(skf1(U_471)) | ~ssPv1(Y_474) | ~ssRr(skf1(skf1(U_471)), Y_474) | ~ssRr(skf1(U_471), U_473) | ~ssPv3(V_472) | ~ssRr(U_473, V_472) | ssPv2(skf1(U_471)) | ssPv3(skf1(U_471)) | ~ssPv4(U_471)))). % 6.25/2.43 tff(c_215, plain, (![U_174, X_240, V_242, Y_241, U_238]: (ssPv4(skf1(U_174)) | ~ssRr(skf1(U_174), X_240) | ~ssPv1(Y_241) | ~ssRr(X_240, Y_241) | ~ssRr(skf1(U_174), U_238) | ~ssPv3(V_242) | ~ssRr(U_238, V_242) | ssPv2(skf1(U_174)) | ssPv3(skf1(U_174)) | ~ssPv4(U_174)))). % 6.25/2.43 tff(c_506, plain, (![U_468]: (ssPv3(skf1(skf1(skf1(U_468)))) | ~ssPv2(skf1(U_468)) | ssPv3(skf1(U_468)) | ssPv1(skf1(skf1(skf1(U_468)))) | ssPv1(U_468) | ~ssPv3(U_468) | ~ssPv3(skf1(skf1(U_468)))))). % 6.25/2.43 tff(c_508, plain, (![U_468]: (ssPv2(skf1(U_468)) | ssPv1(skf1(U_468)) | ssPv3(skf1(U_468)) | ssPv1(skf1(skf1(skf1(U_468)))) | ssPv1(U_468) | ~ssPv3(U_468) | ~ssPv3(skf1(skf1(U_468)))))). % 6.25/2.43 tff(c_493, plain, (![U_466]: (ssPv3(skf1(U_466)) | ssPv1(skf1(skf1(skf1(U_466)))) | ssPv4(skf1(skf1(skf1(U_466)))) | ssPv1(U_466) | ~ssPv3(U_466) | ~ssPv3(skf1(skf1(U_466)))))). % 6.25/2.43 tff(c_488, plain, (![U_463, V_464]: (ssPv3(skf1(U_463)) | ssPv1(skf1(skf1(skf1(U_463)))) | ssPv4(V_464) | ~ssRr(skf1(skf1(U_463)), V_464) | ssPv1(U_463) | ~ssPv3(U_463) | ~ssPv3(skf1(skf1(U_463)))))). % 6.25/2.43 tff(c_483, plain, (![U_459, V_461, U_462]: (ssPv3(skf1(U_459)) | ssPv1(skf1(skf1(skf1(U_459)))) | ssPv4(V_461) | ~ssRr(skf1(U_459), U_462) | ~ssRr(U_462, V_461) | ssPv1(U_459) | ~ssPv3(U_459) | ~ssPv3(skf1(skf1(U_459)))))). % 6.25/2.43 tff(c_478, plain, (![U_456, Y_455, V_458, U_457]: (ssPv3(skf1(U_456)) | ssPv1(Y_455) | ssPv4(V_458) | ~ssRr(skf1(skf1(U_456)), Y_455) | ~ssRr(skf1(U_456), U_457) | ~ssRr(U_457, V_458) | ssPv1(U_456) | ~ssPv3(U_456) | ~ssPv3(skf1(skf1(U_456)))))). % 6.25/2.43 tff(c_270, plain, (![U_198, U_308, V_311, X_310, Y_312]: (ssPv3(skf1(U_198)) | ssPv1(Y_312) | ssPv4(V_311) | ~ssRr(skf1(U_198), X_310) | ~ssRr(X_310, Y_312) | ~ssRr(skf1(U_198), U_308) | ~ssRr(U_308, V_311) | ssPv1(U_198) | ~ssPv3(U_198) | ~ssPv3(skf1(skf1(U_198)))))). % 6.25/2.43 tff(c_468, plain, (![U_447, U_449, V_450]: (~ssPv4(skf1(U_447)) | ~ssPv1(skf1(skf1(skf1(U_447)))) | ~ssRr(skf1(U_447), U_449) | ~ssPv4(V_450) | ~ssRr(U_449, V_450) | ssPv4(U_447) | ssPv3(skf1(U_447)) | ~ssPv1(U_447)))). % 6.25/2.43 tff(c_463, plain, (![U_442, Y_443, U_444, V_446]: (~ssPv4(skf1(U_442)) | ~ssPv1(Y_443) | ~ssRr(skf1(skf1(U_442)), Y_443) | ~ssRr(skf1(U_442), U_444) | ~ssPv4(V_446) | ~ssRr(U_444, V_446) | ssPv4(U_442) | ssPv3(skf1(U_442)) | ~ssPv1(U_442)))). % 6.25/2.43 tff(c_248, plain, (![U_142, V_281, Y_283, X_282, U_280]: (~ssPv4(skf1(U_142)) | ~ssRr(skf1(U_142), X_282) | ~ssPv1(Y_283) | ~ssRr(X_282, Y_283) | ~ssRr(skf1(U_142), U_280) | ~ssPv4(V_281) | ~ssRr(U_280, V_281) | ssPv4(U_142) | ssPv3(skf1(U_142)) | ~ssPv1(U_142)))). % 6.25/2.43 tff(c_453, plain, (![U_435, U_437, V_438]: (ssPv4(skf1(U_435)) | ~ssPv1(skf1(skf1(skf1(U_435)))) | ~ssRr(skf1(U_435), U_437) | ~ssPv3(V_438) | ~ssRr(U_437, V_438) | ssPv2(U_435) | ssPv1(U_435) | ssPv3(skf1(U_435))))). % 6.25/2.43 tff(c_421, plain, (![U_427, Y_429, U_428, V_426]: (ssPv4(skf1(U_427)) | ~ssPv1(Y_429) | ~ssRr(skf1(skf1(U_427)), Y_429) | ~ssRr(skf1(U_427), U_428) | ~ssPv3(V_426) | ~ssRr(U_428, V_426) | ssPv2(U_427) | ssPv1(U_427) | ssPv3(skf1(U_427))))). % 6.25/2.43 tff(c_435, plain, (![U_174]: (ssPv3(U_174) | ssPv2(U_174) | ssPv1(U_174) | ssPv2(skf1(U_174)) | ssPv3(skf1(U_174)) | ~ssPv4(U_174)))). % 6.25/2.44 tff(c_216, plain, (![X_240, V_242, U_129, Y_241, U_238]: (ssPv4(skf1(U_129)) | ~ssRr(skf1(U_129), X_240) | ~ssPv1(Y_241) | ~ssRr(X_240, Y_241) | ~ssRr(skf1(U_129), U_238) | ~ssPv3(V_242) | ~ssRr(U_238, V_242) | ssPv2(U_129) | ssPv1(U_129) | ssPv3(skf1(U_129))))). % 6.25/2.44 tff(c_407, plain, (![U_420]: (ssPv2(skf1(U_420)) | ~ssPv1(skf1(skf1(skf1(U_420)))) | ssPv3(U_420) | ssPv2(U_420) | ssPv1(U_420) | ssPv3(skf1(U_420))))). % 6.25/2.44 tff(c_401, plain, (![U_417, V_419]: (ssPv2(skf1(U_417)) | ~ssPv1(V_419) | ~ssRr(skf1(skf1(U_417)), V_419) | ssPv3(U_417) | ssPv2(U_417) | ssPv1(U_417) | ssPv3(skf1(U_417))))). % 6.25/2.44 tff(c_396, plain, (![U_416, U_124, V_125]: (ssPv2(skf1(U_416)) | ~ssRr(skf1(U_416), U_124) | ~ssPv1(V_125) | ~ssRr(U_124, V_125) | ssPv3(U_416) | ssPv2(U_416) | ssPv1(U_416) | ssPv3(skf1(U_416))))). % 6.25/2.44 tff(c_380, plain, (![U_129]: (ssPv3(U_129) | ssPv2(skf1(skf1(U_129))) | ssPv2(U_129) | ssPv1(U_129) | ssPv3(skf1(U_129))))). % 6.25/2.44 tff(c_371, plain, (![U_414]: (ssPv2(U_414) | ssPv1(U_414) | ssPv3(U_414) | ssPv2(skf1(skf1(U_414))) | ~ssPv3(skf1(skf1(U_414)))))). % 6.25/2.44 tff(c_356, plain, (![U_412]: (ssPv3(U_412) | ssPv2(skf1(skf1(U_412))) | ssPv4(skf1(skf1(U_412))) | ~ssPv3(skf1(skf1(U_412)))))). % 6.25/2.44 tff(c_351, plain, (![U_1, V_411]: (ssPv3(U_1) | ssPv2(skf1(skf1(U_1))) | ssPv4(skf1(skf1(U_1))) | ~ssPv3(V_411) | ~ssRr(skf1(U_1), V_411)))). % 6.25/2.44 tff(c_347, plain, (![U_405, U_407, V_408]: (ssPv3(U_405) | ssPv2(skf1(skf1(U_405))) | ssPv4(skf1(skf1(U_405))) | ~ssRr(U_405, U_407) | ~ssPv3(V_408) | ~ssRr(U_407, V_408)))). % 6.25/2.44 tff(c_342, plain, (![U_1, Y_403, U_402, V_400]: (ssPv3(U_1) | ssPv2(skf1(skf1(U_1))) | ssPv4(Y_403) | ~ssRr(skf1(U_1), Y_403) | ~ssRr(U_1, U_402) | ~ssPv3(V_400) | ~ssRr(U_402, V_400)))). % 6.25/2.44 tff(c_338, plain, (![U_398, Y_397, X_396, V_399, U_395]: (ssPv3(U_395) | ssPv2(skf1(skf1(U_395))) | ssPv4(Y_397) | ~ssRr(U_395, X_396) | ~ssRr(X_396, Y_397) | ~ssRr(U_395, U_398) | ~ssPv3(V_399) | ~ssRr(U_398, V_399)))). % 6.25/2.44 tff(c_327, plain, (![Y_381, X_383, X1_382, U_380, V_384, U_1]: (ssPv3(U_1) | ssPv2(X1_382) | ssPv4(Y_381) | ~ssRr(skf1(U_1), X1_382) | ~ssRr(U_1, X_383) | ~ssRr(X_383, Y_381) | ~ssRr(U_1, U_380) | ~ssPv3(V_384) | ~ssRr(U_380, V_384)))). % 6.25/2.44 tff(c_332, plain, (![U_387, U_389, V_390]: (ssPv2(U_387) | ~ssPv2(skf1(skf1(U_387))) | ~ssRr(U_387, U_389) | ~ssPv4(V_390) | ~ssRr(U_389, V_390) | ssPv4(U_387) | ssPv3(skf1(U_387)) | ~ssPv1(U_387)))). % 6.25/2.44 tff(c_323, plain, (![U_1, Y_378, U_377, V_376]: (ssPv2(U_1) | ~ssPv2(Y_378) | ~ssRr(skf1(U_1), Y_378) | ~ssRr(U_1, U_377) | ~ssPv4(V_376) | ~ssRr(U_377, V_376) | ssPv4(U_1) | ssPv3(skf1(U_1)) | ~ssPv1(U_1)))). % 6.25/2.44 tff(c_36, plain, (![W_83, X1_86, Y_88, V_89, U_84, X_87, Z_85]: (ssPv3(W_83) | ssPv2(X1_86) | ssPv4(Y_88) | ~ssRr(W_83, Z_85) | ~ssRr(Z_85, X1_86) | ~ssRr(W_83, X_87) | ~ssRr(X_87, Y_88) | ~ssRr(W_83, U_84) | ~ssPv3(V_89) | ~ssRr(U_84, V_89)))). % 6.25/2.44 tff(c_319, plain, (![Y_373, U_142, X_372, U_371, V_370]: (ssPv2(U_142) | ~ssRr(U_142, X_372) | ~ssPv2(Y_373) | ~ssRr(X_372, Y_373) | ~ssRr(U_142, U_371) | ~ssPv4(V_370) | ~ssRr(U_371, V_370) | ssPv4(U_142) | ssPv3(skf1(U_142)) | ~ssPv1(U_142)))). % 6.25/2.44 tff(c_315, plain, (![X_366, Y_369, U_365, V_364, U_367]: (ssPv2(U_365) | ~ssPv1(skf1(skf1(U_365))) | ~ssRr(U_365, X_366) | ~ssPv2(Y_369) | ~ssRr(X_366, Y_369) | ~ssRr(U_365, U_367) | ~ssPv4(V_364) | ~ssRr(U_367, V_364)))). % 6.25/2.44 tff(c_310, plain, (![V_362, U_358, X_363, X1_359, Y_360, U_1]: (ssPv2(U_1) | ~ssPv1(X1_359) | ~ssRr(skf1(U_1), X1_359) | ~ssRr(U_1, X_363) | ~ssPv2(Y_360) | ~ssRr(X_363, Y_360) | ~ssRr(U_1, U_358) | ~ssPv4(V_362) | ~ssRr(U_358, V_362)))). % 6.25/2.44 tff(c_40, plain, (![V_103, X1_100, W_97, Y_102, U_98, Z_99, X_101]: (ssPv2(W_97) | ~ssRr(W_97, Z_99) | ~ssPv1(X1_100) | ~ssRr(Z_99, X1_100) | ~ssRr(W_97, X_101) | ~ssPv2(Y_102) | ~ssRr(X_101, Y_102) | ~ssRr(W_97, U_98) | ~ssPv4(V_103) | ~ssRr(U_98, V_103)))). % 6.25/2.44 tff(c_301, plain, (![U_1, Y_349, U_348, V_351]: (ssPv4(U_1) | ssPv2(skf1(skf1(U_1))) | ~ssPv2(Y_349) | ~ssRr(skf1(U_1), Y_349) | ~ssRr(U_1, U_348) | ~ssPv4(V_351) | ~ssRr(U_348, V_351)))). % 6.25/2.44 tff(c_297, plain, (![U_347, Y_342, X_346, U_343, V_345]: (ssPv4(U_343) | ssPv2(skf1(skf1(U_343))) | ~ssRr(U_343, X_346) | ~ssPv2(Y_342) | ~ssRr(X_346, Y_342) | ~ssRr(U_343, U_347) | ~ssPv4(V_345) | ~ssRr(U_347, V_345)))). % 6.25/2.44 tff(c_283, plain, (![U_327, V_329, X1_328, X_326, Y_330, U_1]: (ssPv4(U_1) | ssPv2(X1_328) | ~ssRr(skf1(U_1), X1_328) | ~ssRr(U_1, X_326) | ~ssPv2(Y_330) | ~ssRr(X_326, Y_330) | ~ssRr(U_1, U_327) | ~ssPv4(V_329) | ~ssRr(U_327, V_329)))). % 6.25/2.44 tff(c_287, plain, (![U_1, Y_333, U_336, V_335]: (ssPv3(skf1(skf1(U_1))) | ~ssPv2(U_1) | ~ssPv3(Y_333) | ~ssRr(skf1(U_1), Y_333) | ~ssRr(U_1, U_336) | ~ssPv4(V_335) | ~ssRr(U_336, V_335)))). % 6.25/2.44 tff(c_279, plain, (![U_323, V_325, X_320, Y_322, U_324]: (ssPv3(skf1(skf1(U_323))) | ~ssPv2(U_323) | ~ssRr(U_323, X_320) | ~ssPv3(Y_322) | ~ssRr(X_320, Y_322) | ~ssRr(U_323, U_324) | ~ssPv4(V_325) | ~ssRr(U_324, V_325)))). % 6.25/2.44 tff(c_38, plain, (![Z_92, X_94, Y_95, X1_93, U_91, W_90, V_96]: (ssPv4(W_90) | ssPv2(X1_93) | ~ssRr(W_90, Z_92) | ~ssRr(Z_92, X1_93) | ~ssRr(W_90, X_94) | ~ssPv2(Y_95) | ~ssRr(X_94, Y_95) | ~ssRr(W_90, U_91) | ~ssPv4(V_96) | ~ssRr(U_91, V_96)))). % 6.25/2.44 tff(c_274, plain, (![X1_315, Y_314, U_319, X_317, V_316, U_1]: (ssPv3(X1_315) | ~ssPv2(U_1) | ~ssRr(skf1(U_1), X1_315) | ~ssRr(U_1, X_317) | ~ssPv3(Y_314) | ~ssRr(X_317, Y_314) | ~ssRr(U_1, U_319) | ~ssPv4(V_316) | ~ssRr(U_319, V_316)))). % 6.25/2.44 tff(c_42, plain, (![X_108, W_104, U_105, Y_109, X1_107, V_110, Z_106]: (ssPv3(X1_107) | ~ssPv2(W_104) | ~ssRr(W_104, Z_106) | ~ssRr(Z_106, X1_107) | ~ssRr(W_104, X_108) | ~ssPv3(Y_109) | ~ssRr(X_108, Y_109) | ~ssRr(W_104, U_105) | ~ssPv4(V_110) | ~ssRr(U_105, V_110)))). % 6.25/2.44 tff(c_266, plain, (![U_303, Y_304, X_306, V_305, U_1]: (ssPv3(U_1) | ssPv1(Y_304) | ssPv4(V_305) | ~ssPv4(skf1(U_1)) | ~ssRr(U_1, X_306) | ~ssRr(X_306, Y_304) | ~ssRr(U_1, U_303) | ~ssRr(U_303, V_305)))). % 6.25/2.44 tff(c_24, plain, (![V_52, W_47, U_48, Y_51, X_50, Z_49]: (ssPv3(W_47) | ssPv1(Y_51) | ssPv4(V_52) | ~ssPv4(Z_49) | ~ssRr(W_47, Z_49) | ~ssRr(W_47, X_50) | ~ssRr(X_50, Y_51) | ~ssRr(W_47, U_48) | ~ssRr(U_48, V_52)))). % 6.25/2.44 tff(c_261, plain, (![U_295, U_297, V_298]: (ssPv2(skf1(U_295)) | ~ssPv4(U_295) | ~ssPv2(skf1(skf1(U_295))) | ~ssRr(U_295, U_297) | ~ssPv3(V_298) | ~ssRr(U_297, V_298)))). % 6.25/2.44 tff(c_256, plain, (![U_1, Y_294, U_290, V_293]: (ssPv2(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv2(Y_294) | ~ssRr(skf1(U_1), Y_294) | ~ssRr(U_1, U_290) | ~ssPv3(V_293) | ~ssRr(U_290, V_293)))). % 6.25/2.44 tff(c_252, plain, (![Y_286, V_287, U_285, X_284, U_1]: (ssPv2(skf1(U_1)) | ~ssPv4(U_1) | ~ssRr(U_1, X_284) | ~ssPv2(Y_286) | ~ssRr(X_284, Y_286) | ~ssRr(U_1, U_285) | ~ssPv3(V_287) | ~ssRr(U_285, V_287)))). % 6.25/2.44 tff(c_32, plain, (![Z_73, U_72, V_76, W_71, X_74, Y_75]: (ssPv2(Z_73) | ~ssPv4(W_71) | ~ssRr(W_71, Z_73) | ~ssRr(W_71, X_74) | ~ssPv2(Y_75) | ~ssRr(X_74, Y_75) | ~ssRr(W_71, U_72) | ~ssPv3(V_76) | ~ssRr(U_72, V_76)))). % 6.25/2.44 tff(c_244, plain, (![X_275, V_276, U_274, Y_273, U_1]: (~ssPv4(U_1) | ~ssPv1(skf1(U_1)) | ~ssRr(U_1, X_275) | ~ssPv1(Y_273) | ~ssRr(X_275, Y_273) | ~ssRr(U_1, U_274) | ~ssPv4(V_276) | ~ssRr(U_274, V_276)))). % 6.25/2.44 tff(c_34, plain, (![V_82, X_80, Z_79, Y_81, U_78, W_77]: (~ssPv4(W_77) | ~ssPv1(Z_79) | ~ssRr(W_77, Z_79) | ~ssRr(W_77, X_80) | ~ssPv1(Y_81) | ~ssRr(X_80, Y_81) | ~ssRr(W_77, U_78) | ~ssPv4(V_82) | ~ssRr(U_78, V_82)))). % 6.25/2.44 tff(c_239, plain, (![U_266, U_268, V_269]: (ssPv3(U_266) | ssPv3(skf1(U_266)) | ~ssPv2(skf1(skf1(U_266))) | ~ssRr(U_266, U_268) | ~ssPv4(V_269) | ~ssRr(U_268, V_269)))). % 6.25/2.44 tff(c_234, plain, (![U_1, Y_261, U_265, V_264]: (ssPv3(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(Y_261) | ~ssRr(skf1(U_1), Y_261) | ~ssRr(U_1, U_265) | ~ssPv4(V_264) | ~ssRr(U_265, V_264)))). % 6.25/2.44 tff(c_230, plain, (![Y_259, V_260, X_256, U_255, U_1]: (ssPv3(U_1) | ssPv3(skf1(U_1)) | ~ssRr(U_1, X_256) | ~ssPv2(Y_259) | ~ssRr(X_256, Y_259) | ~ssRr(U_1, U_255) | ~ssPv4(V_260) | ~ssRr(U_255, V_260)))). % 6.25/2.44 tff(c_26, plain, (![W_53, Y_57, U_54, X_56, V_58, Z_55]: (ssPv3(W_53) | ssPv3(Z_55) | ~ssRr(W_53, Z_55) | ~ssRr(W_53, X_56) | ~ssPv2(Y_57) | ~ssRr(X_56, Y_57) | ~ssRr(W_53, U_54) | ~ssPv4(V_58) | ~ssRr(U_54, V_58)))). % 6.25/2.44 tff(c_225, plain, (![U_248, U_250, V_251]: (ssPv1(skf1(U_248)) | ~ssPv3(U_248) | ~ssPv2(skf1(skf1(U_248))) | ~ssRr(U_248, U_250) | ~ssPv4(V_251) | ~ssRr(U_250, V_251)))). % 6.25/2.44 tff(c_220, plain, (![U_1, Y_246, U_244, V_245]: (ssPv1(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv2(Y_246) | ~ssRr(skf1(U_1), Y_246) | ~ssRr(U_1, U_244) | ~ssPv4(V_245) | ~ssRr(U_244, V_245)))). % 6.25/2.44 tff(c_204, plain, (![X_232, Y_235, U_231, V_236, U_1]: (ssPv1(skf1(U_1)) | ~ssPv3(U_1) | ~ssRr(U_1, X_232) | ~ssPv2(Y_235) | ~ssRr(X_232, Y_235) | ~ssRr(U_1, U_231) | ~ssPv4(V_236) | ~ssRr(U_231, V_236)))). % 6.25/2.44 tff(c_186, plain, (![X_217, V_220, Y_221, U_216, U_1]: (ssPv4(U_1) | ~ssPv3(skf1(U_1)) | ~ssRr(U_1, X_217) | ~ssPv1(Y_221) | ~ssRr(X_217, Y_221) | ~ssRr(U_1, U_216) | ~ssPv3(V_220) | ~ssRr(U_216, V_220)))). % 6.25/2.44 tff(c_200, plain, (![U_229]: (ssPv3(U_229) | ssPv3(skf1(skf1(U_229))) | ~ssPv2(U_229) | ~ssPv4(skf1(skf1(U_229)))))). % 6.25/2.44 tff(c_30, plain, (![Y_69, X_68, V_70, W_65, Z_67, U_66]: (ssPv1(Z_67) | ~ssPv3(W_65) | ~ssRr(W_65, Z_67) | ~ssRr(W_65, X_68) | ~ssPv2(Y_69) | ~ssRr(X_68, Y_69) | ~ssRr(W_65, U_66) | ~ssPv4(V_70) | ~ssRr(U_66, V_70)))). % 6.25/2.44 tff(c_195, plain, (![U_1, V_228]: (ssPv3(U_1) | ssPv3(skf1(skf1(U_1))) | ~ssPv2(U_1) | ~ssPv4(V_228) | ~ssRr(skf1(U_1), V_228)))). % 6.25/2.44 tff(c_191, plain, (![U_222, U_224, V_225]: (ssPv3(U_222) | ssPv3(skf1(skf1(U_222))) | ~ssPv2(U_222) | ~ssRr(U_222, U_224) | ~ssPv4(V_225) | ~ssRr(U_224, V_225)))). % 6.25/2.44 tff(c_151, plain, (![U_1, Y_201, U_204, V_200]: (ssPv3(U_1) | ssPv3(Y_201) | ~ssPv2(U_1) | ~ssRr(skf1(U_1), Y_201) | ~ssRr(U_1, U_204) | ~ssPv4(V_200) | ~ssRr(U_204, V_200)))). % 6.25/2.44 tff(c_28, plain, (![V_64, Z_61, U_60, X_62, W_59, Y_63]: (ssPv4(W_59) | ~ssPv3(Z_61) | ~ssRr(W_59, Z_61) | ~ssRr(W_59, X_62) | ~ssPv1(Y_63) | ~ssRr(X_62, Y_63) | ~ssRr(W_59, U_60) | ~ssPv3(V_64) | ~ssRr(U_60, V_64)))). % 6.25/2.44 tff(c_173, plain, (![U_213]: (ssPv3(skf1(U_213)) | ~ssPv1(U_213) | ~ssPv2(skf1(U_213)) | ~ssPv3(skf1(skf1(U_213)))))). % 6.25/2.44 tff(c_167, plain, (![U_1, V_212]: (ssPv3(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv3(V_212) | ~ssRr(skf1(U_1), V_212)))). % 6.25/2.44 tff(c_163, plain, (![U_1, U_208, V_209]: (ssPv3(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv2(skf1(U_1)) | ~ssRr(U_1, U_208) | ~ssPv3(V_209) | ~ssRr(U_208, V_209)))). % 6.25/2.44 tff(c_133, plain, (![U_1, X_190, U_187, V_189]: (ssPv3(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv2(X_190) | ~ssRr(U_1, X_190) | ~ssRr(U_1, U_187) | ~ssPv3(V_189) | ~ssRr(U_187, V_189)))). % 6.25/2.44 tff(c_147, plain, (![U_198]: (ssPv1(U_198) | ssPv4(skf1(skf1(U_198))) | ~ssPv3(U_198) | ~ssPv3(skf1(skf1(U_198)))))). % 6.25/2.44 tff(c_20, plain, (![V_41, Y_40, X_39, W_37, U_38]: (ssPv3(W_37) | ssPv3(Y_40) | ~ssPv2(W_37) | ~ssRr(W_37, X_39) | ~ssRr(X_39, Y_40) | ~ssRr(W_37, U_38) | ~ssPv4(V_41) | ~ssRr(U_38, V_41)))). % 6.25/2.44 tff(c_142, plain, (![U_1, V_197]: (ssPv1(U_1) | ssPv4(skf1(skf1(U_1))) | ~ssPv3(U_1) | ~ssPv3(V_197) | ~ssRr(skf1(U_1), V_197)))). % 6.25/2.44 tff(c_138, plain, (![U_191, U_193, V_194]: (ssPv1(U_191) | ssPv4(skf1(skf1(U_191))) | ~ssPv3(U_191) | ~ssRr(U_191, U_193) | ~ssPv3(V_194) | ~ssRr(U_193, V_194)))). % 6.25/2.44 tff(c_129, plain, (![U_1, Y_184, U_181, V_182]: (ssPv1(U_1) | ssPv4(Y_184) | ~ssPv3(U_1) | ~ssRr(skf1(U_1), Y_184) | ~ssRr(U_1, U_181) | ~ssPv3(V_182) | ~ssRr(U_181, V_182)))). % 6.25/2.44 tff(c_22, plain, (![V_46, X_44, W_42, U_43, Y_45]: (ssPv3(Y_45) | ~ssPv1(W_42) | ~ssRr(W_42, Y_45) | ~ssPv2(X_44) | ~ssRr(W_42, X_44) | ~ssRr(W_42, U_43) | ~ssPv3(V_46) | ~ssRr(U_43, V_46)))). % 6.25/2.44 tff(c_18, plain, (![W_32, V_36, X_34, U_33, Y_35]: (ssPv1(W_32) | ssPv4(Y_35) | ~ssPv3(W_32) | ~ssRr(W_32, X_34) | ~ssRr(X_34, Y_35) | ~ssRr(W_32, U_33) | ~ssPv3(V_36) | ~ssRr(U_33, V_36)))). % 6.25/2.44 tff(c_110, plain, (![U_1, V_169, X_167, U_166]: (ssPv4(skf1(U_1)) | ssPv4(V_169) | ~ssPv3(U_1) | ~ssPv4(X_167) | ~ssRr(U_1, X_167) | ~ssRr(U_1, U_166) | ~ssRr(U_166, V_169)))). % 6.25/2.44 tff(c_120, plain, (![U_174]: (ssPv2(skf1(U_174)) | ssPv3(skf1(U_174)) | ssPv3(skf1(skf1(U_174))) | ~ssPv4(U_174)))). % 6.25/2.44 tff(c_114, plain, (![U_1, V_172]: (ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv3(V_172) | ~ssPv4(U_1) | ~ssRr(skf1(U_1), V_172)))). % 6.25/2.44 tff(c_106, plain, (![U_1, V_164, U_165]: (ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ssPv3(V_164) | ~ssPv4(U_1) | ~ssRr(U_1, U_165) | ~ssRr(U_165, V_164)))). % 6.25/2.44 tff(c_16, plain, (![W_27, U_28, X_29, V_31, Y_30]: (ssPv4(Y_30) | ssPv4(V_31) | ~ssPv3(W_27) | ~ssRr(W_27, Y_30) | ~ssPv4(X_29) | ~ssRr(W_27, X_29) | ~ssRr(W_27, U_28) | ~ssRr(U_28, V_31)))). % 6.25/2.45 tff(c_97, plain, (![U_1, X_152, V_150, U_151]: (ssPv2(skf1(U_1)) | ssPv3(X_152) | ssPv3(V_150) | ~ssPv4(U_1) | ~ssRr(U_1, X_152) | ~ssRr(U_1, U_151) | ~ssRr(U_151, V_150)))). % 6.25/2.45 tff(c_101, plain, (![U_1, V_156, U_158]: (ssPv4(U_1) | ssPv3(skf1(U_1)) | ssPv2(V_156) | ~ssPv4(skf1(U_1)) | ~ssRr(U_1, U_158) | ~ssRr(U_158, V_156)))). % 6.25/2.45 tff(c_93, plain, (![U_1, V_146, X_145, U_147]: (ssPv4(U_1) | ssPv3(skf1(U_1)) | ssPv2(V_146) | ~ssPv4(X_145) | ~ssRr(U_1, X_145) | ~ssRr(U_1, U_147) | ~ssRr(U_147, V_146)))). % 6.25/2.45 tff(c_14, plain, (![Y_25, V_26, U_23, W_22, X_24]: (ssPv2(Y_25) | ssPv3(X_24) | ssPv3(V_26) | ~ssPv4(W_22) | ~ssRr(W_22, Y_25) | ~ssRr(W_22, X_24) | ~ssRr(W_22, U_23) | ~ssRr(U_23, V_26)))). % 6.25/2.45 tff(c_12, plain, (![V_21, X_19, W_17, U_18, Y_20]: (ssPv4(W_17) | ssPv3(Y_20) | ssPv2(V_21) | ~ssRr(W_17, Y_20) | ~ssPv4(X_19) | ~ssRr(W_17, X_19) | ~ssRr(W_17, U_18) | ~ssRr(U_18, V_21)))). % 6.25/2.45 tff(c_88, plain, (![U_142]: (ssPv4(U_142) | ssPv3(skf1(U_142)) | ssPv1(skf1(skf1(U_142))) | ~ssPv1(U_142)))). % 6.25/2.45 tff(c_82, plain, (![U_1, V_140]: (ssPv4(U_1) | ssPv3(skf1(U_1)) | ssPv1(V_140) | ~ssPv1(U_1) | ~ssRr(skf1(U_1), V_140)))). % 6.25/2.45 tff(c_77, plain, (![U_1, V_134, U_135]: (ssPv4(U_1) | ssPv3(skf1(U_1)) | ssPv1(V_134) | ~ssPv1(U_1) | ~ssRr(U_1, U_135) | ~ssRr(U_135, V_134)))). % 6.25/2.45 tff(c_62, plain, (![U_1, U_124, V_125]: (ssPv3(U_1) | ssPv2(U_1) | ~ssPv2(skf1(U_1)) | ~ssRr(U_1, U_124) | ~ssPv1(V_125) | ~ssRr(U_124, V_125)))). % 6.25/2.45 tff(c_8, plain, (![W_11, X_12, V_10, U_9]: (ssPv4(W_11) | ssPv3(X_12) | ssPv1(V_10) | ~ssPv1(W_11) | ~ssRr(W_11, X_12) | ~ssRr(W_11, U_9) | ~ssRr(U_9, V_10)))). % 6.25/2.45 tff(c_72, plain, (![U_129]: (ssPv2(U_129) | ssPv1(U_129) | ssPv3(skf1(U_129)) | ssPv3(skf1(skf1(U_129)))))). % 6.25/2.45 tff(c_66, plain, (![U_1, V_127]: (ssPv2(U_1) | ssPv1(U_1) | ssPv3(skf1(U_1)) | ssPv3(V_127) | ~ssRr(skf1(U_1), V_127)))). % 6.25/2.45 tff(c_58, plain, (![U_1, V_120, U_121]: (ssPv2(U_1) | ssPv1(U_1) | ssPv3(skf1(U_1)) | ssPv3(V_120) | ~ssRr(U_1, U_121) | ~ssRr(U_121, V_120)))). % 6.25/2.45 tff(c_10, plain, (![W_15, X_16, U_13, V_14]: (ssPv3(W_15) | ssPv2(W_15) | ~ssPv2(X_16) | ~ssRr(W_15, X_16) | ~ssRr(W_15, U_13) | ~ssPv1(V_14) | ~ssRr(U_13, V_14)))). % 6.25/2.45 tff(c_6, plain, (![W_7, X_8, V_6, U_5]: (ssPv2(W_7) | ssPv1(W_7) | ssPv3(X_8) | ssPv3(V_6) | ~ssRr(W_7, X_8) | ~ssRr(W_7, U_5) | ~ssRr(U_5, V_6)))). % 6.25/2.45 tff(c_53, plain, (![U_115]: (ssPv3(U_115) | ssPv2(U_115) | ssPv1(U_115) | ~ssPv4(skf1(skf1(U_115)))))). % 6.25/2.45 tff(c_47, plain, (![U_1, V_114]: (ssPv3(U_1) | ssPv2(U_1) | ssPv1(U_1) | ~ssPv4(V_114) | ~ssRr(skf1(U_1), V_114)))). % 6.25/2.45 tff(c_4, plain, (![W_4, U_2, V_3]: (ssPv3(W_4) | ssPv2(W_4) | ssPv1(W_4) | ~ssRr(W_4, U_2) | ~ssPv4(V_3) | ~ssRr(U_2, V_3)))). % 6.25/2.45 tff(c_2, plain, (![U_1]: (ssRr(U_1, skf1(U_1))))). % 6.25/2.45 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.25/2.45 %------------------------------------------------------------------------------