%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN739-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/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 : n004.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.03s 2.16s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SYN739-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/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.14/0.34 % Computer : n004.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Wed Apr 9 08:13:37 EDT 2025 % 0.14/0.34 % CPUTime : % 5.03/2.15 % 5.03/2.16 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.03/2.16 % 5.03/2.16 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.26/2.16 %$ ssRr > ssPv8 > ssPv7 > ssPv6 > ssPv5 > ssPv4 > ssPv3 > ssPv2 > ssPv1 > #nlpp > skf1 % 5.26/2.16 % 5.26/2.16 %Foreground sorts: % 5.26/2.16 % 5.26/2.16 % 5.26/2.16 %Background operators: % 5.26/2.16 % 5.26/2.16 % 5.26/2.16 %Foreground operators: % 5.26/2.16 tff(skf1, type, skf1: $i > $i). % 5.26/2.16 tff(ssPv1, type, ssPv1: $i > $o). % 5.26/2.16 tff(ssPv3, type, ssPv3: $i > $o). % 5.26/2.16 tff(ssPv7, type, ssPv7: $i > $o). % 5.26/2.16 tff(ssPv6, type, ssPv6: $i > $o). % 5.26/2.16 tff(ssPv5, type, ssPv5: $i > $o). % 5.26/2.16 tff(ssRr, type, ssRr: ($i * $i) > $o). % 5.26/2.16 tff(ssPv4, type, ssPv4: $i > $o). % 5.26/2.16 tff(ssPv2, type, ssPv2: $i > $o). % 5.26/2.16 tff(ssPv8, type, ssPv8: $i > $o). % 5.26/2.16 % 5.26/2.16 %Saturated clause set: % 5.26/2.17 tff(c_580, plain, (![U_446]: (~ssPv8(skf1(skf1(U_446))) | ~ssPv5(skf1(skf1(skf1(skf1(U_446))))) | ~ssPv6(skf1(U_446)) | ~ssPv3(skf1(U_446)) | ~ssPv1(skf1(skf1(U_446))) | ~ssPv7(skf1(U_446)) | ~ssPv5(skf1(U_446)) | ssPv7(U_446) | ssPv6(U_446) | ssPv3(U_446) | ssPv1(skf1(U_446)) | ssPv2(skf1(U_446)) | ssPv7(skf1(skf1(U_446))) | ssPv6(skf1(skf1(U_446))) | ssPv3(skf1(skf1(U_446)))))). % 5.26/2.17 tff(c_574, plain, (![U_443, V_445]: (~ssPv8(skf1(skf1(U_443))) | ~ssPv5(V_445) | ~ssRr(skf1(skf1(skf1(U_443))), V_445) | ~ssPv6(skf1(U_443)) | ~ssPv3(skf1(U_443)) | ~ssPv1(skf1(skf1(U_443))) | ~ssPv7(skf1(U_443)) | ~ssPv5(skf1(U_443)) | ssPv7(U_443) | ssPv6(U_443) | ssPv3(U_443) | ssPv1(skf1(U_443)) | ssPv2(skf1(U_443)) | ssPv7(skf1(skf1(U_443))) | ssPv6(skf1(skf1(U_443))) | ssPv3(skf1(skf1(U_443)))))). % 5.26/2.17 tff(c_547, plain, (![U_430, U_148, V_149]: (~ssPv8(skf1(skf1(U_430))) | ~ssRr(skf1(skf1(U_430)), U_148) | ~ssPv5(V_149) | ~ssRr(U_148, V_149) | ~ssPv6(skf1(U_430)) | ~ssPv3(skf1(U_430)) | ~ssPv1(skf1(skf1(U_430))) | ~ssPv7(skf1(U_430)) | ~ssPv5(skf1(U_430)) | ssPv7(U_430) | ssPv6(U_430) | ssPv3(U_430) | ssPv1(skf1(U_430)) | ssPv2(skf1(U_430)) | ssPv7(skf1(skf1(U_430))) | ssPv6(skf1(skf1(U_430))) | ssPv3(skf1(skf1(U_430)))))). % 5.26/2.17 tff(c_568, plain, (![U_440]: (ssPv4(skf1(U_440)) | ~ssPv3(skf1(skf1(skf1(U_440)))) | ~ssPv1(skf1(skf1(U_440))) | ~ssPv7(skf1(U_440)) | ~ssPv5(skf1(U_440)) | ssPv7(U_440) | ssPv6(U_440) | ssPv3(U_440) | ssPv1(skf1(U_440)) | ssPv2(skf1(U_440)) | ssPv7(skf1(skf1(U_440))) | ssPv6(skf1(skf1(U_440))) | ssPv3(skf1(skf1(U_440))) | ssPv1(skf1(skf1(skf1(U_440))))))). % 5.26/2.17 tff(c_563, plain, (![U_437, V_439]: (ssPv4(skf1(U_437)) | ~ssPv3(V_439) | ~ssRr(skf1(skf1(U_437)), V_439) | ~ssPv1(skf1(skf1(U_437))) | ~ssPv7(skf1(U_437)) | ~ssPv5(skf1(U_437)) | ssPv7(U_437) | ssPv6(U_437) | ssPv3(U_437) | ssPv1(skf1(U_437)) | ssPv2(skf1(U_437)) | ssPv7(skf1(skf1(U_437))) | ssPv6(skf1(skf1(U_437))) | ssPv3(skf1(skf1(U_437))) | ssPv1(skf1(skf1(skf1(U_437))))))). % 5.26/2.17 tff(c_538, plain, (![U_429, U_415, V_416]: (ssPv4(skf1(U_429)) | ~ssRr(skf1(U_429), U_415) | ~ssPv3(V_416) | ~ssRr(U_415, V_416) | ~ssPv1(skf1(skf1(U_429))) | ~ssPv7(skf1(U_429)) | ~ssPv5(skf1(U_429)) | ssPv7(U_429) | ssPv6(U_429) | ssPv3(U_429) | ssPv1(skf1(U_429)) | ssPv2(skf1(U_429)) | ssPv7(skf1(skf1(U_429))) | ssPv6(skf1(skf1(U_429))) | ssPv3(skf1(skf1(U_429))) | ssPv1(skf1(skf1(skf1(U_429))))))). % 5.26/2.17 tff(c_557, plain, (![U_434]: (ssPv4(skf1(U_434)) | ~ssPv3(skf1(skf1(skf1(U_434)))) | ~ssPv1(skf1(skf1(U_434))) | ~ssPv7(skf1(U_434)) | ~ssPv5(skf1(U_434)) | ssPv6(skf1(U_434)) | ~ssPv7(U_434) | ~ssPv1(U_434) | ssPv7(skf1(skf1(U_434))) | ssPv6(skf1(skf1(U_434))) | ssPv3(skf1(skf1(U_434))) | ssPv1(skf1(skf1(skf1(U_434))))))). % 5.26/2.17 tff(c_552, plain, (![U_431, V_433]: (ssPv4(skf1(U_431)) | ~ssPv3(V_433) | ~ssRr(skf1(skf1(U_431)), V_433) | ~ssPv1(skf1(skf1(U_431))) | ~ssPv7(skf1(U_431)) | ~ssPv5(skf1(U_431)) | ssPv6(skf1(U_431)) | ~ssPv7(U_431) | ~ssPv1(U_431) | ssPv7(skf1(skf1(U_431))) | ssPv6(skf1(skf1(U_431))) | ssPv3(skf1(skf1(U_431))) | ssPv1(skf1(skf1(skf1(U_431))))))). % 5.26/2.17 tff(c_514, plain, (![U_427, U_385, V_386]: (ssPv4(skf1(U_427)) | ~ssRr(skf1(U_427), U_385) | ~ssPv3(V_386) | ~ssRr(U_385, V_386) | ~ssPv1(skf1(skf1(U_427))) | ~ssPv7(skf1(U_427)) | ~ssPv5(skf1(U_427)) | ssPv6(skf1(U_427)) | ~ssPv7(U_427) | ~ssPv1(U_427) | ssPv7(skf1(skf1(U_427))) | ssPv6(skf1(skf1(U_427))) | ssPv3(skf1(skf1(U_427))) | ssPv1(skf1(skf1(skf1(U_427))))))). % 5.26/2.17 tff(c_543, plain, (![U_429]: (~ssPv6(skf1(U_429)) | ~ssPv3(skf1(U_429)) | ~ssPv1(skf1(skf1(U_429))) | ~ssPv7(skf1(U_429)) | ~ssPv5(skf1(U_429)) | ssPv7(U_429) | ssPv6(U_429) | ssPv3(U_429) | ssPv1(skf1(U_429)) | ssPv2(skf1(U_429)) | ssPv7(skf1(skf1(U_429))) | ssPv6(skf1(skf1(U_429))) | ssPv3(skf1(skf1(U_429))) | ssPv1(skf1(skf1(skf1(U_429))))))). % 5.26/2.17 tff(c_491, plain, (![U_426]: (~ssPv1(skf1(skf1(U_426))) | ~ssPv7(skf1(U_426)) | ~ssPv5(skf1(U_426)) | ssPv7(U_426) | ssPv6(U_426) | ssPv3(U_426) | ssPv1(skf1(U_426)) | ssPv2(skf1(U_426)) | ssPv7(skf1(skf1(U_426))) | ssPv6(skf1(skf1(U_426))) | ssPv3(skf1(skf1(U_426))) | ssPv1(skf1(skf1(skf1(U_426)))) | ssPv2(skf1(skf1(skf1(U_426))))))). % 5.26/2.17 tff(c_492, plain, (![U_426]: (ssPv6(skf1(skf1(U_426))) | ~ssPv7(skf1(U_426)) | ~ssPv5(skf1(U_426)) | ssPv7(U_426) | ssPv6(U_426) | ssPv3(U_426) | ssPv1(skf1(U_426)) | ssPv2(skf1(U_426)) | ssPv6(skf1(skf1(skf1(U_426)))) | ~ssPv7(skf1(skf1(U_426))) | ~ssPv1(skf1(skf1(U_426)))))). % 5.26/2.17 tff(c_456, plain, (![U_412]: (~ssPv1(skf1(skf1(U_412))) | ~ssPv7(skf1(U_412)) | ~ssPv5(skf1(U_412)) | ssPv6(skf1(U_412)) | ~ssPv7(U_412) | ~ssPv1(U_412) | ssPv7(skf1(skf1(U_412))) | ssPv6(skf1(skf1(U_412))) | ssPv3(skf1(skf1(U_412))) | ssPv1(skf1(skf1(skf1(U_412)))) | ssPv2(skf1(skf1(skf1(U_412))))))). % 5.26/2.17 tff(c_483, plain, (![U_424]: (ssPv6(skf1(skf1(U_424))) | ~ssPv1(skf1(skf1(U_424))) | ~ssPv2(skf1(skf1(skf1(skf1(U_424))))) | ~ssPv7(skf1(U_424)) | ~ssPv5(skf1(U_424)) | ssPv7(U_424) | ssPv6(U_424) | ssPv3(U_424) | ssPv1(skf1(U_424)) | ssPv2(skf1(U_424))))). % 5.26/2.17 tff(c_477, plain, (![U_421, V_423]: (ssPv6(skf1(skf1(U_421))) | ~ssPv1(skf1(skf1(U_421))) | ~ssPv2(V_423) | ~ssRr(skf1(skf1(skf1(U_421))), V_423) | ~ssPv7(skf1(U_421)) | ~ssPv5(skf1(U_421)) | ssPv7(U_421) | ssPv6(U_421) | ssPv3(U_421) | ssPv1(skf1(U_421)) | ssPv2(skf1(U_421))))). % 5.26/2.17 tff(c_420, plain, (![U_395, U_113, V_114]: (ssPv6(skf1(skf1(U_395))) | ~ssPv1(skf1(skf1(U_395))) | ~ssRr(skf1(skf1(U_395)), U_113) | ~ssPv2(V_114) | ~ssRr(U_113, V_114) | ~ssPv7(skf1(U_395)) | ~ssPv5(skf1(U_395)) | ssPv7(U_395) | ssPv6(U_395) | ssPv3(U_395) | ssPv1(skf1(U_395)) | ssPv2(skf1(U_395))))). % 5.26/2.17 tff(c_457, plain, (![U_412]: (ssPv6(skf1(skf1(U_412))) | ~ssPv7(skf1(U_412)) | ~ssPv5(skf1(U_412)) | ssPv6(skf1(U_412)) | ~ssPv7(U_412) | ~ssPv1(U_412) | ssPv6(skf1(skf1(skf1(U_412)))) | ~ssPv7(skf1(skf1(U_412))) | ~ssPv1(skf1(skf1(U_412)))))). % 5.26/2.17 tff(c_462, plain, (![U_413, U_415, V_416]: (ssPv4(skf1(U_413)) | ~ssPv2(skf1(skf1(skf1(U_413)))) | ~ssRr(skf1(U_413), U_415) | ~ssPv3(V_416) | ~ssRr(U_415, V_416) | ssPv7(U_413) | ssPv6(U_413) | ssPv3(U_413) | ssPv1(skf1(U_413)) | ssPv2(skf1(U_413))))). % 5.26/2.18 tff(c_437, plain, (![U_402, Y_404, U_405, V_403]: (ssPv4(skf1(U_402)) | ~ssPv2(Y_404) | ~ssRr(skf1(skf1(U_402)), Y_404) | ~ssRr(skf1(U_402), U_405) | ~ssPv3(V_403) | ~ssRr(U_405, V_403) | ssPv7(U_402) | ssPv6(U_402) | ssPv3(U_402) | ssPv1(skf1(U_402)) | ssPv2(skf1(U_402))))). % 5.26/2.18 tff(c_448, plain, (![U_410]: (ssPv6(skf1(skf1(U_410))) | ~ssPv1(skf1(skf1(U_410))) | ~ssPv2(skf1(skf1(skf1(skf1(U_410))))) | ~ssPv7(skf1(U_410)) | ~ssPv5(skf1(U_410)) | ssPv6(skf1(U_410)) | ~ssPv7(U_410) | ~ssPv1(U_410)))). % 5.26/2.18 tff(c_442, plain, (![U_407, V_409]: (ssPv6(skf1(skf1(U_407))) | ~ssPv1(skf1(skf1(U_407))) | ~ssPv2(V_409) | ~ssRr(skf1(skf1(skf1(U_407))), V_409) | ~ssPv7(skf1(U_407)) | ~ssPv5(skf1(U_407)) | ssPv6(skf1(U_407)) | ~ssPv7(U_407) | ~ssPv1(U_407)))). % 5.26/2.18 tff(c_358, plain, (![U_356, U_113, V_114]: (ssPv6(skf1(skf1(U_356))) | ~ssPv1(skf1(skf1(U_356))) | ~ssRr(skf1(skf1(U_356)), U_113) | ~ssPv2(V_114) | ~ssRr(U_113, V_114) | ~ssPv7(skf1(U_356)) | ~ssPv5(skf1(U_356)) | ssPv6(skf1(U_356)) | ~ssPv7(U_356) | ~ssPv1(U_356)))). % 5.26/2.18 tff(c_315, plain, (![Y_328, X_327, V_326, U_324, U_210]: (ssPv4(skf1(U_210)) | ~ssRr(skf1(U_210), X_327) | ~ssPv2(Y_328) | ~ssRr(X_327, Y_328) | ~ssRr(skf1(U_210), U_324) | ~ssPv3(V_326) | ~ssRr(U_324, V_326) | ssPv7(U_210) | ssPv6(U_210) | ssPv3(U_210) | ssPv1(skf1(U_210)) | ssPv2(skf1(U_210))))). % 5.26/2.18 tff(c_431, plain, (![U_399]: (ssPv4(skf1(U_399)) | ~ssPv3(skf1(skf1(skf1(U_399)))) | ssPv6(skf1(U_399)) | ~ssPv7(U_399) | ~ssPv1(U_399) | ssPv6(skf1(skf1(U_399))) | ~ssPv7(skf1(U_399)) | ~ssPv1(skf1(U_399))))). % 5.26/2.18 tff(c_425, plain, (![U_396, V_398]: (ssPv4(skf1(U_396)) | ~ssPv3(V_398) | ~ssRr(skf1(skf1(U_396)), V_398) | ssPv6(skf1(U_396)) | ~ssPv7(U_396) | ~ssPv1(U_396) | ssPv6(skf1(skf1(U_396))) | ~ssPv7(skf1(U_396)) | ~ssPv1(skf1(U_396))))). % 5.26/2.18 tff(c_401, plain, (![U_387, U_388, V_389]: (ssPv4(skf1(U_387)) | ~ssRr(skf1(U_387), U_388) | ~ssPv3(V_389) | ~ssRr(U_388, V_389) | ssPv6(skf1(U_387)) | ~ssPv7(U_387) | ~ssPv1(U_387) | ssPv6(skf1(skf1(U_387))) | ~ssPv7(skf1(U_387)) | ~ssPv1(skf1(U_387))))). % 5.26/2.18 tff(c_412, plain, (![U_394]: (ssPv4(skf1(skf1(skf1(U_394)))) | ~ssPv7(skf1(U_394)) | ~ssPv5(skf1(U_394)) | ssPv7(U_394) | ssPv6(U_394) | ssPv3(U_394) | ssPv1(skf1(U_394)) | ssPv2(skf1(U_394))))). % 5.26/2.18 tff(c_406, plain, (![V_390, U_391]: (ssPv4(V_390) | ~ssPv7(skf1(U_391)) | ~ssPv5(skf1(U_391)) | ~ssRr(skf1(skf1(U_391)), V_390) | ssPv7(U_391) | ssPv6(U_391) | ssPv3(U_391) | ssPv1(skf1(U_391)) | ssPv2(skf1(U_391))))). % 5.26/2.18 tff(c_230, plain, (![V_136, U_243, U_139]: (ssPv4(V_136) | ~ssPv7(skf1(U_243)) | ~ssPv5(skf1(U_243)) | ~ssRr(skf1(U_243), U_139) | ~ssRr(U_139, V_136) | ssPv7(U_243) | ssPv6(U_243) | ssPv3(U_243) | ssPv1(skf1(U_243)) | ssPv2(skf1(U_243))))). % 5.26/2.18 tff(c_392, plain, (![U_383, U_385, V_386]: (ssPv4(skf1(U_383)) | ~ssPv2(skf1(skf1(skf1(U_383)))) | ~ssRr(skf1(U_383), U_385) | ~ssPv3(V_386) | ~ssRr(U_385, V_386) | ssPv6(skf1(U_383)) | ~ssPv7(U_383) | ~ssPv1(U_383)))). % 5.26/2.18 tff(c_386, plain, (![U_380, Y_378, U_379, V_377]: (ssPv4(skf1(U_380)) | ~ssPv2(Y_378) | ~ssRr(skf1(skf1(U_380)), Y_378) | ~ssRr(skf1(U_380), U_379) | ~ssPv3(V_377) | ~ssRr(U_379, V_377) | ssPv6(skf1(U_380)) | ~ssPv7(U_380) | ~ssPv1(U_380)))). % 5.26/2.18 tff(c_381, plain, (![U_375]: (ssPv2(U_375) | ssPv2(skf1(skf1(U_375))) | ssPv6(skf1(skf1(U_375))) | ~ssPv3(skf1(skf1(U_375)))))). % 5.26/2.18 tff(c_316, plain, (![Y_328, U_128, X_327, V_326, U_324]: (ssPv4(skf1(U_128)) | ~ssRr(skf1(U_128), X_327) | ~ssPv2(Y_328) | ~ssRr(X_327, Y_328) | ~ssRr(skf1(U_128), U_324) | ~ssPv3(V_326) | ~ssRr(U_324, V_326) | ssPv6(skf1(U_128)) | ~ssPv7(U_128) | ~ssPv1(U_128)))). % 5.26/2.18 tff(c_376, plain, (![U_1, V_374]: (ssPv2(U_1) | ssPv2(skf1(skf1(U_1))) | ssPv6(skf1(skf1(U_1))) | ~ssPv3(V_374) | ~ssRr(skf1(U_1), V_374)))). % 5.26/2.18 tff(c_372, plain, (![U_368, U_370, V_371]: (ssPv2(U_368) | ssPv2(skf1(skf1(U_368))) | ssPv6(skf1(skf1(U_368))) | ~ssRr(U_368, U_370) | ~ssPv3(V_371) | ~ssRr(U_370, V_371)))). % 5.26/2.18 tff(c_367, plain, (![U_1, Y_364, U_365, V_363]: (ssPv2(U_1) | ssPv2(skf1(skf1(U_1))) | ssPv6(Y_364) | ~ssRr(skf1(U_1), Y_364) | ~ssRr(U_1, U_365) | ~ssPv3(V_363) | ~ssRr(U_365, V_363)))). % 5.26/2.18 tff(c_363, plain, (![V_362, U_358, U_360, Y_357, X_359]: (ssPv2(U_358) | ssPv2(skf1(skf1(U_358))) | ssPv6(Y_357) | ~ssRr(U_358, X_359) | ~ssRr(X_359, Y_357) | ~ssRr(U_358, U_360) | ~ssPv3(V_362) | ~ssRr(U_360, V_362)))). % 5.26/2.18 tff(c_338, plain, (![V_344, Y_348, U_345, X_343, X1_347, U_1]: (ssPv2(U_1) | ssPv2(X1_347) | ssPv6(Y_348) | ~ssRr(skf1(U_1), X1_347) | ~ssRr(U_1, X_343) | ~ssRr(X_343, Y_348) | ~ssRr(U_1, U_345) | ~ssPv3(V_344) | ~ssRr(U_345, V_344)))). % 5.26/2.18 tff(c_350, plain, (![U_355]: (ssPv4(skf1(skf1(skf1(U_355)))) | ~ssPv7(skf1(U_355)) | ~ssPv5(skf1(U_355)) | ssPv6(skf1(U_355)) | ~ssPv7(U_355) | ~ssPv1(U_355)))). % 5.26/2.18 tff(c_344, plain, (![V_351, U_352]: (ssPv4(V_351) | ~ssPv7(skf1(U_352)) | ~ssPv5(skf1(U_352)) | ~ssRr(skf1(skf1(U_352)), V_351) | ssPv6(skf1(U_352)) | ~ssPv7(U_352) | ~ssPv1(U_352)))). % 5.26/2.18 tff(c_117, plain, (![V_150, U_128, U_152]: (ssPv4(V_150) | ~ssPv7(skf1(U_128)) | ~ssPv5(skf1(U_128)) | ~ssRr(skf1(U_128), U_152) | ~ssRr(U_152, V_150) | ssPv6(skf1(U_128)) | ~ssPv7(U_128) | ~ssPv1(U_128)))). % 5.26/2.18 tff(c_334, plain, (![U_341]: (ssPv8(U_341) | ssPv2(skf1(U_341)) | ssPv2(skf1(skf1(U_341))) | ssPv8(skf1(skf1(U_341)))))). % 5.26/2.18 tff(c_42, plain, (![X1_97, V_100, Y_99, U_95, X_98, W_94, Z_96]: (ssPv2(W_94) | ssPv2(X1_97) | ssPv6(Y_99) | ~ssRr(W_94, Z_96) | ~ssRr(Z_96, X1_97) | ~ssRr(W_94, X_98) | ~ssRr(X_98, Y_99) | ~ssRr(W_94, U_95) | ~ssPv3(V_100) | ~ssRr(U_95, V_100)))). % 5.26/2.18 tff(c_329, plain, (![U_1, V_339]: (ssPv8(U_1) | ssPv2(skf1(U_1)) | ssPv2(skf1(skf1(U_1))) | ssPv8(V_339) | ~ssRr(skf1(U_1), V_339)))). % 5.26/2.18 tff(c_325, plain, (![U_334, V_336, U_337]: (ssPv8(U_334) | ssPv2(skf1(U_334)) | ssPv2(skf1(skf1(U_334))) | ssPv8(V_336) | ~ssRr(U_334, U_337) | ~ssRr(U_337, V_336)))). % 5.26/2.18 tff(c_320, plain, (![U_1, Y_332, V_330, U_331]: (ssPv8(U_1) | ssPv2(skf1(U_1)) | ssPv2(Y_332) | ssPv8(V_330) | ~ssRr(skf1(U_1), Y_332) | ~ssRr(U_1, U_331) | ~ssRr(U_331, V_330)))). % 5.26/2.18 tff(c_309, plain, (![X_319, V_323, U_318, Y_322, U_1]: (ssPv8(U_1) | ssPv2(skf1(U_1)) | ssPv2(Y_322) | ssPv8(V_323) | ~ssRr(U_1, X_319) | ~ssRr(X_319, Y_322) | ~ssRr(U_1, U_318) | ~ssRr(U_318, V_323)))). % 5.26/2.18 tff(c_295, plain, (![Y_306, V_310, U_311, X_309, U_1]: (ssPv4(U_1) | ~ssPv2(skf1(U_1)) | ~ssRr(U_1, X_309) | ~ssPv2(Y_306) | ~ssRr(X_309, Y_306) | ~ssRr(U_1, U_311) | ~ssPv3(V_310) | ~ssRr(U_311, V_310)))). % 5.26/2.18 tff(c_28, plain, (![W_53, Y_57, U_54, X_56, V_58, Z_55]: (ssPv8(W_53) | ssPv2(Z_55) | ssPv2(Y_57) | ssPv8(V_58) | ~ssRr(W_53, Z_55) | ~ssRr(W_53, X_56) | ~ssRr(X_56, Y_57) | ~ssRr(W_53, U_54) | ~ssRr(U_54, V_58)))). % 5.26/2.18 tff(c_304, plain, (![U_315]: (ssPv4(U_315) | ssPv1(skf1(U_315)) | ssPv8(skf1(skf1(U_315))) | ~ssPv6(skf1(skf1(U_315)))))). % 5.26/2.18 tff(c_299, plain, (![U_1, V_314]: (ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv8(skf1(skf1(U_1))) | ~ssPv6(V_314) | ~ssRr(skf1(U_1), V_314)))). % 5.26/2.18 tff(c_291, plain, (![U_302, U_304, V_305]: (ssPv4(U_302) | ssPv1(skf1(U_302)) | ssPv8(skf1(skf1(U_302))) | ~ssRr(U_302, U_304) | ~ssPv6(V_305) | ~ssRr(U_304, V_305)))). % 5.26/2.18 tff(c_38, plain, (![Z_84, U_83, V_87, X_85, W_82, Y_86]: (ssPv4(W_82) | ~ssPv2(Z_84) | ~ssRr(W_82, Z_84) | ~ssRr(W_82, X_85) | ~ssPv2(Y_86) | ~ssRr(X_85, Y_86) | ~ssRr(W_82, U_83) | ~ssPv3(V_87) | ~ssRr(U_83, V_87)))). % 5.26/2.19 tff(c_286, plain, (![U_1, Y_300, U_299, V_298]: (ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv8(Y_300) | ~ssRr(skf1(U_1), Y_300) | ~ssRr(U_1, U_299) | ~ssPv6(V_298) | ~ssRr(U_299, V_298)))). % 5.26/2.19 tff(c_272, plain, (![V_285, X_290, Y_288, U_289, U_1]: (ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv8(Y_288) | ~ssRr(U_1, X_290) | ~ssRr(X_290, Y_288) | ~ssRr(U_1, U_289) | ~ssPv6(V_285) | ~ssRr(U_289, V_285)))). % 5.26/2.19 tff(c_281, plain, (![U_294]: (ssPv7(skf1(U_294)) | ssPv5(skf1(skf1(U_294))) | ~ssPv4(U_294) | ~ssPv2(skf1(skf1(U_294)))))). % 5.26/2.19 tff(c_276, plain, (![U_1, V_293]: (ssPv7(skf1(U_1)) | ssPv5(skf1(skf1(U_1))) | ~ssPv4(U_1) | ~ssPv2(V_293) | ~ssRr(skf1(U_1), V_293)))). % 5.26/2.19 tff(c_268, plain, (![U_281, U_283, V_284]: (ssPv7(skf1(U_281)) | ssPv5(skf1(skf1(U_281))) | ~ssPv4(U_281) | ~ssRr(U_281, U_283) | ~ssPv2(V_284) | ~ssRr(U_283, V_284)))). % 5.26/2.19 tff(c_32, plain, (![W_64, U_65, V_69, Z_66, Y_68, X_67]: (ssPv4(W_64) | ssPv1(Z_66) | ssPv8(Y_68) | ~ssRr(W_64, Z_66) | ~ssRr(W_64, X_67) | ~ssRr(X_67, Y_68) | ~ssRr(W_64, U_65) | ~ssPv6(V_69) | ~ssRr(U_65, V_69)))). % 5.26/2.19 tff(c_263, plain, (![U_1, Y_279, U_280, V_278]: (ssPv7(skf1(U_1)) | ssPv5(Y_279) | ~ssPv4(U_1) | ~ssRr(skf1(U_1), Y_279) | ~ssRr(U_1, U_280) | ~ssPv2(V_278) | ~ssRr(U_280, V_278)))). % 5.26/2.19 tff(c_258, plain, (![U_269, V_272, X_273, Y_271, U_1]: (ssPv7(skf1(U_1)) | ssPv5(Y_271) | ~ssPv4(U_1) | ~ssRr(U_1, X_273) | ~ssRr(X_273, Y_271) | ~ssRr(U_1, U_269) | ~ssPv2(V_272) | ~ssRr(U_269, V_272)))). % 5.26/2.19 tff(c_254, plain, (![U_267]: (ssPv3(skf1(U_267)) | ssPv6(skf1(skf1(U_267))) | ~ssPv1(U_267) | ~ssPv3(skf1(skf1(U_267)))))). % 5.26/2.19 tff(c_34, plain, (![V_75, W_70, X_73, U_71, Y_74, Z_72]: (ssPv7(Z_72) | ssPv5(Y_74) | ~ssPv4(W_70) | ~ssRr(W_70, Z_72) | ~ssRr(W_70, X_73) | ~ssRr(X_73, Y_74) | ~ssRr(W_70, U_71) | ~ssPv2(V_75) | ~ssRr(U_71, V_75)))). % 5.26/2.19 tff(c_249, plain, (![U_1, V_266]: (ssPv3(skf1(U_1)) | ssPv6(skf1(skf1(U_1))) | ~ssPv1(U_1) | ~ssPv3(V_266) | ~ssRr(skf1(U_1), V_266)))). % 5.26/2.19 tff(c_245, plain, (![U_260, U_262, V_263]: (ssPv3(skf1(U_260)) | ssPv6(skf1(skf1(U_260))) | ~ssPv1(U_260) | ~ssRr(U_260, U_262) | ~ssPv3(V_263) | ~ssRr(U_262, V_263)))). % 5.26/2.19 tff(c_240, plain, (![U_1, Y_257, U_259, V_255]: (ssPv3(skf1(U_1)) | ssPv6(Y_257) | ~ssPv1(U_1) | ~ssRr(skf1(U_1), Y_257) | ~ssRr(U_1, U_259) | ~ssPv3(V_255) | ~ssRr(U_259, V_255)))). % 5.26/2.19 tff(c_235, plain, (![Y_246, U_247, X_249, V_245, U_1]: (ssPv3(skf1(U_1)) | ssPv6(Y_246) | ~ssPv1(U_1) | ~ssRr(U_1, X_249) | ~ssRr(X_249, Y_246) | ~ssRr(U_1, U_247) | ~ssPv3(V_245) | ~ssRr(U_247, V_245)))). % 5.26/2.19 tff(c_213, plain, (![V_235, X_239, Y_236, U_234, U_1]: (ssPv2(Y_236) | ~ssPv5(U_1) | ~ssPv7(skf1(U_1)) | ~ssRr(U_1, X_239) | ~ssRr(X_239, Y_236) | ~ssRr(U_1, U_234) | ~ssPv7(V_235) | ~ssRr(U_234, V_235)))). % 5.26/2.19 tff(c_36, plain, (![X_79, W_76, Z_78, U_77, Y_80, V_81]: (ssPv3(Z_78) | ssPv6(Y_80) | ~ssPv1(W_76) | ~ssRr(W_76, Z_78) | ~ssRr(W_76, X_79) | ~ssRr(X_79, Y_80) | ~ssRr(W_76, U_77) | ~ssPv3(V_81) | ~ssRr(U_77, V_81)))). % 5.26/2.19 tff(c_223, plain, (![U_210]: (ssPv7(U_210) | ssPv6(U_210) | ssPv2(skf1(skf1(U_210))) | ssPv3(U_210) | ssPv1(skf1(U_210)) | ssPv2(skf1(U_210))))). % 5.26/2.19 tff(c_218, plain, (![U_240]: (ssPv7(U_240) | ssPv6(U_240) | ssPv2(skf1(skf1(U_240))) | ~ssPv4(skf1(skf1(U_240)))))). % 5.26/2.19 tff(c_209, plain, (![U_1, V_233]: (ssPv7(U_1) | ssPv6(U_1) | ssPv2(skf1(skf1(U_1))) | ~ssPv4(V_233) | ~ssRr(skf1(U_1), V_233)))). % 5.26/2.19 tff(c_40, plain, (![V_93, U_89, Y_92, X_91, W_88, Z_90]: (ssPv2(Y_92) | ~ssPv5(W_88) | ~ssPv7(Z_90) | ~ssRr(W_88, Z_90) | ~ssRr(W_88, X_91) | ~ssRr(X_91, Y_92) | ~ssRr(W_88, U_89) | ~ssPv7(V_93) | ~ssRr(U_89, V_93)))). % 5.26/2.19 tff(c_205, plain, (![U_227, U_229, V_230]: (ssPv7(U_227) | ssPv6(U_227) | ssPv2(skf1(skf1(U_227))) | ~ssRr(U_227, U_229) | ~ssPv4(V_230) | ~ssRr(U_229, V_230)))). % 5.26/2.19 tff(c_200, plain, (![U_1, Y_225, U_223, V_226]: (ssPv7(U_1) | ssPv6(U_1) | ssPv2(Y_225) | ~ssRr(skf1(U_1), Y_225) | ~ssRr(U_1, U_223) | ~ssPv4(V_226) | ~ssRr(U_223, V_226)))). % 5.26/2.19 tff(c_20, plain, (![U_34, Y_36, V_37, W_33, X_35]: (ssPv7(W_33) | ssPv6(W_33) | ssPv2(Y_36) | ~ssRr(W_33, X_35) | ~ssRr(X_35, Y_36) | ~ssRr(W_33, U_34) | ~ssPv4(V_37) | ~ssRr(U_34, V_37)))). % 5.26/2.19 tff(c_188, plain, (![U_1, V_212, X_213, U_214]: (ssPv7(U_1) | ssPv2(skf1(U_1)) | ssPv6(V_212) | ~ssPv2(X_213) | ~ssRr(U_1, X_213) | ~ssRr(U_1, U_214) | ~ssRr(U_214, V_212)))). % 5.26/2.19 tff(c_184, plain, (![U_210]: (ssPv3(U_210) | ssPv1(skf1(U_210)) | ssPv2(skf1(U_210)) | ssPv4(skf1(skf1(U_210)))))). % 5.26/2.19 tff(c_22, plain, (![U_39, X_40, V_42, W_38, Y_41]: (ssPv7(W_38) | ssPv2(Y_41) | ssPv6(V_42) | ~ssRr(W_38, Y_41) | ~ssPv2(X_40) | ~ssRr(W_38, X_40) | ~ssRr(W_38, U_39) | ~ssRr(U_39, V_42)))). % 5.26/2.19 tff(c_178, plain, (![U_1, V_208]: (ssPv3(U_1) | ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ssPv4(V_208) | ~ssRr(skf1(U_1), V_208)))). % 5.26/2.19 tff(c_174, plain, (![U_1, V_205, U_206]: (ssPv3(U_1) | ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ssPv4(V_205) | ~ssRr(U_1, U_206) | ~ssRr(U_206, V_205)))). % 5.26/2.19 tff(c_170, plain, (![U_1, X_200, V_201, U_198]: (ssPv3(U_1) | ssPv1(skf1(U_1)) | ssPv2(X_200) | ssPv4(V_201) | ~ssRr(U_1, X_200) | ~ssRr(U_1, U_198) | ~ssRr(U_198, V_201)))). % 5.26/2.19 tff(c_18, plain, (![V_32, Y_31, W_28, U_29, X_30]: (ssPv3(W_28) | ssPv1(Y_31) | ssPv2(X_30) | ssPv4(V_32) | ~ssRr(W_28, Y_31) | ~ssRr(W_28, X_30) | ~ssRr(W_28, U_29) | ~ssRr(U_29, V_32)))). % 5.26/2.19 tff(c_165, plain, (![U_191, U_193, V_194]: (~ssPv8(U_191) | ~ssPv2(U_191) | ~ssPv3(skf1(skf1(U_191))) | ~ssRr(U_191, U_193) | ~ssPv5(V_194) | ~ssRr(U_193, V_194)))). % 5.26/2.19 tff(c_150, plain, (![U_1, Y_182, U_180, V_181]: (~ssPv8(U_1) | ~ssPv2(U_1) | ~ssPv3(Y_182) | ~ssRr(skf1(U_1), Y_182) | ~ssRr(U_1, U_180) | ~ssPv5(V_181) | ~ssRr(U_180, V_181)))). % 5.26/2.19 tff(c_159, plain, (![U_188]: (ssPv8(U_188) | ssPv6(skf1(skf1(U_188))) | ~ssPv6(U_188) | ~ssPv7(skf1(skf1(U_188)))))). % 5.26/2.19 tff(c_154, plain, (![U_1, V_187]: (ssPv8(U_1) | ssPv6(skf1(skf1(U_1))) | ~ssPv6(U_1) | ~ssPv7(V_187) | ~ssRr(skf1(U_1), V_187)))). % 5.26/2.19 tff(c_146, plain, (![U_176, U_178, V_179]: (ssPv8(U_176) | ssPv6(skf1(skf1(U_176))) | ~ssPv6(U_176) | ~ssRr(U_176, U_178) | ~ssPv7(V_179) | ~ssRr(U_178, V_179)))). % 5.26/2.19 tff(c_30, plain, (![V_63, X_61, U_60, Y_62, W_59]: (~ssPv8(W_59) | ~ssPv2(W_59) | ~ssRr(W_59, X_61) | ~ssPv3(Y_62) | ~ssRr(X_61, Y_62) | ~ssRr(W_59, U_60) | ~ssPv5(V_63) | ~ssRr(U_60, V_63)))). % 5.26/2.19 tff(c_135, plain, (![U_1, Y_169, U_172, V_170]: (ssPv8(U_1) | ssPv6(Y_169) | ~ssPv6(U_1) | ~ssRr(skf1(U_1), Y_169) | ~ssRr(U_1, U_172) | ~ssPv7(V_170) | ~ssRr(U_172, V_170)))). % 5.26/2.19 tff(c_140, plain, (![U_173]: (ssPv5(U_173) | ssPv2(U_173) | ssPv8(skf1(skf1(U_173))) | ~ssPv5(skf1(skf1(U_173)))))). % 5.26/2.19 tff(c_131, plain, (![U_1, V_167]: (ssPv5(U_1) | ssPv2(U_1) | ssPv8(skf1(skf1(U_1))) | ~ssPv5(V_167) | ~ssRr(skf1(U_1), V_167)))). % 5.26/2.19 tff(c_26, plain, (![V_52, W_48, Y_51, X_50, U_49]: (ssPv8(W_48) | ssPv6(Y_51) | ~ssPv6(W_48) | ~ssRr(W_48, X_50) | ~ssRr(X_50, Y_51) | ~ssRr(W_48, U_49) | ~ssPv7(V_52) | ~ssRr(U_49, V_52)))). % 5.26/2.19 tff(c_127, plain, (![U_161, U_163, V_164]: (ssPv5(U_161) | ssPv2(U_161) | ssPv8(skf1(skf1(U_161))) | ~ssRr(U_161, U_163) | ~ssPv5(V_164) | ~ssRr(U_163, V_164)))). % 5.26/2.19 tff(c_122, plain, (![U_1, Y_156, U_157, V_160]: (ssPv5(U_1) | ssPv2(U_1) | ssPv8(Y_156) | ~ssRr(skf1(U_1), Y_156) | ~ssRr(U_1, U_157) | ~ssPv5(V_160) | ~ssRr(U_157, V_160)))). % 5.26/2.19 tff(c_24, plain, (![W_43, V_47, X_45, U_44, Y_46]: (ssPv5(W_43) | ssPv2(W_43) | ssPv8(Y_46) | ~ssRr(W_43, X_45) | ~ssRr(X_45, Y_46) | ~ssRr(W_43, U_44) | ~ssPv5(V_47) | ~ssRr(U_44, V_47)))). % 5.26/2.19 tff(c_113, plain, (![U_1, U_148, V_149]: (ssPv6(U_1) | ~ssPv8(U_1) | ~ssPv1(skf1(U_1)) | ~ssRr(U_1, U_148) | ~ssPv5(V_149) | ~ssRr(U_148, V_149)))). % 5.26/2.19 tff(c_98, plain, (![V_136, U_1, U_139]: (ssPv4(V_136) | ~ssPv7(U_1) | ~ssPv5(U_1) | ~ssPv2(skf1(U_1)) | ~ssRr(U_1, U_139) | ~ssRr(U_139, V_136)))). % 5.26/2.19 tff(c_14, plain, (![W_22, X_23, U_20, V_21]: (ssPv6(W_22) | ~ssPv8(W_22) | ~ssPv1(X_23) | ~ssRr(W_22, X_23) | ~ssRr(W_22, U_20) | ~ssPv5(V_21) | ~ssRr(U_20, V_21)))). % 5.26/2.19 tff(c_108, plain, (![U_143]: (ssPv2(skf1(U_143)) | ssPv8(skf1(skf1(U_143))) | ~ssPv6(U_143) | ~ssPv4(U_143)))). % 5.26/2.19 tff(c_102, plain, (![U_1, V_141]: (ssPv2(skf1(U_1)) | ssPv8(V_141) | ~ssPv6(U_1) | ~ssPv4(U_1) | ~ssRr(skf1(U_1), V_141)))). % 5.26/2.19 tff(c_94, plain, (![U_1, V_133, U_135]: (ssPv2(skf1(U_1)) | ssPv8(V_133) | ~ssPv6(U_1) | ~ssPv4(U_1) | ~ssRr(U_1, U_135) | ~ssRr(U_135, V_133)))). % 5.26/2.19 tff(c_12, plain, (![V_17, W_18, X_19, U_16]: (ssPv4(V_17) | ~ssPv7(W_18) | ~ssPv5(W_18) | ~ssPv2(X_19) | ~ssRr(W_18, X_19) | ~ssRr(W_18, U_16) | ~ssRr(U_16, V_17)))). % 5.26/2.19 tff(c_8, plain, (![X_11, V_9, W_10, U_8]: (ssPv2(X_11) | ssPv8(V_9) | ~ssPv6(W_10) | ~ssPv4(W_10) | ~ssRr(W_10, X_11) | ~ssRr(W_10, U_8) | ~ssRr(U_8, V_9)))). % 5.26/2.19 tff(c_89, plain, (![U_130]: (~ssPv6(U_130) | ~ssPv3(U_130) | ssPv6(skf1(U_130)) | ~ssPv7(U_130) | ~ssPv1(U_130)))). % 5.26/2.19 tff(c_84, plain, (![U_128]: (ssPv6(skf1(U_128)) | ssPv2(skf1(skf1(U_128))) | ~ssPv7(U_128) | ~ssPv1(U_128)))). % 5.26/2.19 tff(c_78, plain, (![U_1, V_126]: (ssPv6(skf1(U_1)) | ssPv2(V_126) | ~ssPv7(U_1) | ~ssPv1(U_1) | ~ssRr(skf1(U_1), V_126)))). % 5.26/2.19 tff(c_74, plain, (![U_1, V_122, U_124]: (ssPv6(skf1(U_1)) | ssPv2(V_122) | ~ssPv7(U_1) | ~ssPv1(U_1) | ~ssRr(U_1, U_124) | ~ssRr(U_124, V_122)))). % 5.26/2.19 tff(c_10, plain, (![X_15, V_13, W_14, U_12]: (ssPv6(X_15) | ssPv2(V_13) | ~ssPv7(W_14) | ~ssPv1(W_14) | ~ssRr(W_14, X_15) | ~ssRr(W_14, U_12) | ~ssRr(U_12, V_13)))). % 5.26/2.19 tff(c_62, plain, (![U_1, U_113, V_114]: (ssPv6(U_1) | ~ssPv1(U_1) | ~ssPv4(skf1(U_1)) | ~ssRr(U_1, U_113) | ~ssPv2(V_114) | ~ssRr(U_113, V_114)))). % 5.26/2.19 tff(c_68, plain, (![U_115]: (ssPv3(U_115) | ssPv8(skf1(skf1(U_115))) | ~ssPv2(U_115) | ~ssPv1(U_115)))). % 5.26/2.19 tff(c_58, plain, (![U_1, V_109]: (ssPv3(U_1) | ssPv8(V_109) | ~ssPv2(U_1) | ~ssPv1(U_1) | ~ssRr(skf1(U_1), V_109)))). % 5.26/2.19 tff(c_16, plain, (![W_26, X_27, U_24, V_25]: (ssPv6(W_26) | ~ssPv1(W_26) | ~ssPv4(X_27) | ~ssRr(W_26, X_27) | ~ssRr(W_26, U_24) | ~ssPv2(V_25) | ~ssRr(U_24, V_25)))). % 5.26/2.19 tff(c_4, plain, (![W_4, V_3, U_2]: (ssPv3(W_4) | ssPv8(V_3) | ~ssPv2(W_4) | ~ssPv1(W_4) | ~ssRr(W_4, U_2) | ~ssRr(U_2, V_3)))). % 5.26/2.20 tff(c_53, plain, (![U_105]: (~ssPv7(U_105) | ~ssPv6(U_105) | ~ssPv3(U_105) | ~ssPv2(skf1(skf1(U_105)))))). % 5.26/2.20 tff(c_47, plain, (![U_1, V_104]: (~ssPv7(U_1) | ~ssPv6(U_1) | ~ssPv3(U_1) | ~ssPv2(V_104) | ~ssRr(skf1(U_1), V_104)))). % 5.26/2.20 tff(c_6, plain, (![W_7, U_5, V_6]: (~ssPv7(W_7) | ~ssPv6(W_7) | ~ssPv3(W_7) | ~ssRr(W_7, U_5) | ~ssPv2(V_6) | ~ssRr(U_5, V_6)))). % 5.26/2.20 tff(c_2, plain, (![U_1]: (ssRr(U_1, skf1(U_1))))). % 5.26/2.20 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.26/2.20 %------------------------------------------------------------------------------