%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN756-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 : n032.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:22 PM UTC 2025 % Result : Satisfiable 7.20s 2.52s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.10 % Problem : SYN756-1 : TPTP v9.0.0. Released v2.5.0. % 0.10/0.11 % 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.11/0.30 % Computer : n032.cluster.edu % 0.11/0.30 % Model : x86_64 x86_64 % 0.11/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.30 % Memory : 8042.1875MB % 0.11/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.30 % CPULimit : 300 % 0.11/0.30 % WCLimit : 300 % 0.11/0.30 % DateTime : Wed Apr 9 08:15:45 EDT 2025 % 0.11/0.30 % CPUTime : % 7.20/2.52 % 7.20/2.52 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 7.20/2.52 % 7.20/2.52 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 7.20/2.52 %$ ssRr > ssPv4 > ssPv3 > ssPv2 > ssPv1 > #nlpp > skf1 % 7.20/2.52 % 7.20/2.52 %Foreground sorts: % 7.20/2.52 % 7.20/2.52 % 7.20/2.52 %Background operators: % 7.20/2.52 % 7.20/2.52 % 7.20/2.52 %Foreground operators: % 7.20/2.52 tff(skf1, type, skf1: $i > $i). % 7.20/2.52 tff(ssPv1, type, ssPv1: $i > $o). % 7.20/2.52 tff(ssPv3, type, ssPv3: $i > $o). % 7.20/2.52 tff(ssRr, type, ssRr: ($i * $i) > $o). % 7.20/2.52 tff(ssPv4, type, ssPv4: $i > $o). % 7.20/2.52 tff(ssPv2, type, ssPv2: $i > $o). % 7.20/2.52 % 7.20/2.52 %Saturated clause set: % 7.20/2.53 tff(c_2202, plain, (![U_536]: (~ssPv1(U_536) | ~ssPv4(U_536) | ~ssPv2(U_536)))). % 7.20/2.53 tff(c_1312, plain, (![U_1, W_419, V_420]: (ssPv1(U_1) | ~ssPv2(W_419) | ~ssRr(U_1, W_419) | ~ssPv4(V_420) | ~ssRr(U_1, V_420) | ~ssPv4(U_1) | ~ssPv3(U_1)))). % 7.20/2.53 tff(c_2077, plain, (![U_412]: (ssPv2(U_412) | ssPv4(U_412) | ~ssPv1(skf1(U_412)) | ~ssPv3(U_412) | ~ssPv1(U_412)))). % 7.20/2.53 tff(c_2007, plain, (![U_1]: (~ssPv4(skf1(U_1)) | ssPv4(U_1) | ssPv1(U_1) | ~ssPv1(skf1(U_1)) | ssPv3(U_1) | ~ssPv2(U_1)))). % 7.20/2.53 tff(c_1879, plain, (![V_511, U_1]: (~ssPv4(V_511) | ~ssRr(U_1, V_511) | ssPv4(U_1) | ssPv1(U_1) | ~ssPv1(skf1(U_1)) | ssPv3(U_1) | ~ssPv2(U_1)))). % 7.20/2.53 tff(c_1978, plain, (![U_1]: (ssPv1(U_1) | ssPv2(skf1(U_1)) | ~ssPv4(skf1(U_1)) | ssPv3(U_1) | ssPv2(U_1) | ~ssPv4(U_1)))). % 7.20/2.53 tff(c_1338, plain, (![U_1, V_425]: (ssPv1(U_1) | ssPv2(skf1(U_1)) | ~ssPv4(V_425) | ~ssRr(U_1, V_425) | ssPv3(U_1) | ssPv2(U_1) | ~ssPv4(U_1)))). % 7.20/2.53 tff(c_1815, plain, (![U_504, V_298]: (ssPv1(U_504) | ~ssPv4(V_298) | ~ssRr(U_504, V_298) | ~ssPv1(skf1(U_504)) | ~ssPv3(U_504) | ~ssPv2(skf1(U_504))))). % 7.20/2.53 tff(c_1869, plain, (![U_1, V_509]: (~ssPv2(skf1(U_1)) | ~ssPv4(V_509) | ~ssRr(U_1, V_509) | ssPv4(U_1) | ssPv1(U_1) | ~ssPv2(U_1)))). % 7.20/2.53 tff(c_1315, plain, (![W_419, U_1, V_420]: (~ssPv2(W_419) | ~ssRr(U_1, W_419) | ~ssPv4(V_420) | ~ssRr(U_1, V_420) | ssPv4(U_1) | ssPv1(U_1) | ~ssPv2(U_1)))). % 7.20/2.53 tff(c_1848, plain, (![U_505]: (ssPv1(skf1(U_505)) | ~ssPv3(U_505) | ~ssPv2(skf1(U_505))))). % 7.20/2.53 tff(c_1789, plain, (![U_503]: (~ssPv1(skf1(U_503)) | ssPv3(skf1(U_503)) | ~ssPv3(U_503) | ~ssPv2(skf1(U_503))))). % 7.20/2.53 tff(c_1737, plain, (![U_1]: (ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv2(skf1(U_1))))). % 7.20/2.53 tff(c_1733, plain, (![U_1, V_500]: (ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv2(V_500) | ~ssRr(U_1, V_500)))). % 7.20/2.53 tff(c_1618, plain, (![U_1, W_468, V_470]: (ssPv3(skf1(U_1)) | ssPv4(W_468) | ~ssPv3(U_1) | ~ssRr(U_1, W_468) | ~ssPv2(V_470) | ~ssRr(U_1, V_470)))). % 7.20/2.53 tff(c_1721, plain, (![U_1, V_493]: (ssPv3(U_1) | ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv2(V_493) | ~ssRr(U_1, V_493)))). % 7.20/2.53 tff(c_1717, plain, (![U_1, V_490]: (ssPv1(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ~ssPv3(V_490) | ~ssRr(U_1, V_490)))). % 7.20/2.53 tff(c_1346, plain, (![U_1, W_431, V_432]: (ssPv3(U_1) | ssPv1(skf1(U_1)) | ssPv2(W_431) | ~ssRr(U_1, W_431) | ~ssPv2(V_432) | ~ssRr(U_1, V_432)))). % 7.20/2.53 tff(c_1437, plain, (![U_1, W_454, V_455]: (ssPv1(U_1) | ssPv3(skf1(U_1)) | ~ssPv2(W_454) | ~ssRr(U_1, W_454) | ~ssPv3(V_455) | ~ssRr(U_1, V_455)))). % 7.20/2.53 tff(c_1684, plain, (![U_1]: (ssPv3(U_1) | ssPv3(skf1(U_1)) | ~ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1))))). % 7.20/2.53 tff(c_1680, plain, (![U_1, V_484]: (ssPv3(U_1) | ssPv3(skf1(U_1)) | ~ssPv1(skf1(U_1)) | ~ssPv2(V_484) | ~ssRr(U_1, V_484)))). % 7.20/2.53 tff(c_1672, plain, (![U_1, W_478, V_479]: (ssPv3(U_1) | ssPv3(skf1(U_1)) | ~ssPv1(W_478) | ~ssRr(U_1, W_478) | ~ssPv2(V_479) | ~ssRr(U_1, V_479)))). % 7.20/2.53 tff(c_1668, plain, (![U_1, V_475]: (ssPv1(U_1) | ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv3(V_475) | ~ssRr(U_1, V_475)))). % 7.20/2.53 tff(c_84, plain, (![U_114, X_117, W_116, V_115]: (ssPv3(U_114) | ssPv3(X_117) | ~ssRr(U_114, X_117) | ~ssPv1(W_116) | ~ssRr(U_114, W_116) | ~ssPv2(V_115) | ~ssRr(U_114, V_115)))). % 7.20/2.53 tff(c_1522, plain, (![U_1, W_461, V_462]: (ssPv1(U_1) | ssPv2(skf1(U_1)) | ssPv3(W_461) | ~ssRr(U_1, W_461) | ~ssPv3(V_462) | ~ssRr(U_1, V_462)))). % 7.20/2.53 tff(c_96, plain, (![X_141, W_140, U_138, V_139]: (ssPv3(X_141) | ssPv4(W_140) | ~ssPv3(U_138) | ~ssRr(U_138, X_141) | ~ssRr(U_138, W_140) | ~ssPv2(V_139) | ~ssRr(U_138, V_139)))). % 7.20/2.53 tff(c_1597, plain, (![U_465]: (~ssPv2(skf1(U_465)) | ssPv1(skf1(U_465)) | ~ssPv4(U_465) | ~ssPv2(U_465)))). % 7.20/2.53 tff(c_82, plain, (![U_110, X_113, W_112, V_111]: (ssPv1(U_110) | ssPv2(X_113) | ssPv3(W_112) | ~ssRr(U_110, X_113) | ~ssRr(U_110, W_112) | ~ssPv3(V_111) | ~ssRr(U_110, V_111)))). % 7.20/2.53 tff(c_1496, plain, (![U_310]: (ssPv1(U_310) | ssPv3(U_310) | ~ssPv4(U_310) | ~ssPv2(U_310)))). % 7.20/2.53 tff(c_1432, plain, (![U_1]: (ssPv1(U_1) | ~ssPv1(skf1(U_1)) | ssPv3(U_1) | ssPv2(skf1(U_1)) | ~ssPv2(U_1)))). % 7.20/2.53 tff(c_88, plain, (![U_122, X_125, W_124, V_123]: (ssPv1(U_122) | ssPv3(X_125) | ~ssRr(U_122, X_125) | ~ssPv2(W_124) | ~ssRr(U_122, W_124) | ~ssPv3(V_123) | ~ssRr(U_122, V_123)))). % 7.20/2.53 tff(c_1412, plain, (![U_1]: (ssPv1(U_1) | ssPv2(skf1(U_1)) | ~ssPv1(skf1(U_1)) | ~ssPv4(skf1(U_1))))). % 7.20/2.54 tff(c_1408, plain, (![U_1, V_448]: (ssPv1(U_1) | ssPv2(skf1(U_1)) | ~ssPv1(skf1(U_1)) | ~ssPv4(V_448) | ~ssRr(U_1, V_448)))). % 7.20/2.54 tff(c_1396, plain, (![U_1, W_439, V_440]: (ssPv1(U_1) | ssPv2(skf1(U_1)) | ~ssPv1(W_439) | ~ssRr(U_1, W_439) | ~ssPv4(V_440) | ~ssRr(U_1, V_440)))). % 7.20/2.54 tff(c_1400, plain, (![U_1, V_443]: (ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv2(V_443) | ~ssRr(U_1, V_443)))). % 7.20/2.54 tff(c_1173, plain, (![U_1, W_407, V_409]: (ssPv2(skf1(U_1)) | ssPv3(W_407) | ~ssPv2(U_1) | ~ssRr(U_1, W_407) | ~ssPv2(V_409) | ~ssRr(U_1, V_409)))). % 7.20/2.54 tff(c_94, plain, (![U_134, X_137, W_136, V_135]: (ssPv1(U_134) | ssPv2(X_137) | ~ssRr(U_134, X_137) | ~ssPv1(W_136) | ~ssRr(U_134, W_136) | ~ssPv4(V_135) | ~ssRr(U_134, V_135)))). % 7.20/2.54 tff(c_1379, plain, (![U_435]: (ssPv4(U_435) | ssPv1(skf1(U_435)) | ~ssPv2(skf1(U_435))))). % 7.20/2.54 tff(c_1342, plain, (![U_1, V_428]: (ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv2(V_428) | ~ssRr(U_1, V_428)))). % 7.20/2.54 tff(c_80, plain, (![U_106, X_109, W_108, V_107]: (ssPv3(U_106) | ssPv1(X_109) | ssPv2(W_108) | ~ssRr(U_106, X_109) | ~ssRr(U_106, W_108) | ~ssPv2(V_107) | ~ssRr(U_106, V_107)))). % 7.20/2.54 tff(c_1039, plain, (![U_1, W_373, V_374]: (ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv3(W_373) | ~ssRr(U_1, W_373) | ~ssPv2(V_374) | ~ssRr(U_1, V_374)))). % 7.20/2.54 tff(c_1319, plain, (![U_1, V_423]: (ssPv1(U_1) | ssPv2(skf1(U_1)) | ~ssPv3(skf1(U_1)) | ~ssPv4(V_423) | ~ssRr(U_1, V_423)))). % 7.20/2.54 tff(c_1263, plain, (![U_1, W_415, V_416]: (ssPv1(U_1) | ssPv2(skf1(U_1)) | ~ssPv3(W_415) | ~ssRr(U_1, W_415) | ~ssPv4(V_416) | ~ssRr(U_1, V_416)))). % 7.20/2.54 tff(c_959, plain, (![U_1, W_362, V_363]: (ssPv1(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv2(W_362) | ~ssRr(U_1, W_362) | ~ssPv4(V_363) | ~ssRr(U_1, V_363)))). % 7.20/2.54 tff(c_1256, plain, (![U_412]: (ssPv4(U_412) | ssPv2(skf1(U_412)) | ~ssPv1(skf1(U_412)) | ~ssPv3(U_412) | ~ssPv1(U_412)))). % 7.20/2.54 tff(c_92, plain, (![U_130, X_133, W_132, V_131]: (ssPv1(U_130) | ssPv2(X_133) | ~ssRr(U_130, X_133) | ~ssPv3(W_132) | ~ssRr(U_130, W_132) | ~ssPv4(V_131) | ~ssRr(U_130, V_131)))). % 7.20/2.54 tff(c_1190, plain, (![U_1]: (ssPv2(skf1(U_1)) | ~ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv1(U_1)))). % 7.20/2.54 tff(c_1169, plain, (![U_1]: (ssPv2(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv4(skf1(U_1))))). % 7.20/2.54 tff(c_86, plain, (![X_121, W_120, U_118, V_119]: (ssPv2(X_121) | ssPv3(W_120) | ~ssPv2(U_118) | ~ssRr(U_118, X_121) | ~ssRr(U_118, W_120) | ~ssPv2(V_119) | ~ssRr(U_118, V_119)))). % 7.20/2.54 tff(c_1165, plain, (![U_1, V_403]: (ssPv2(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv4(V_403) | ~ssRr(U_1, V_403)))). % 7.20/2.54 tff(c_1132, plain, (![U_1, W_393, V_394]: (ssPv2(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv1(W_393) | ~ssRr(U_1, W_393) | ~ssPv4(V_394) | ~ssRr(U_1, V_394)))). % 7.20/2.54 tff(c_1140, plain, (![U_1]: (ssPv1(U_1) | ssPv3(skf1(U_1)) | ~ssPv1(skf1(U_1)) | ~ssPv4(skf1(U_1))))). % 7.20/2.54 tff(c_1136, plain, (![U_1, V_397]: (ssPv1(U_1) | ssPv3(skf1(U_1)) | ~ssPv1(skf1(U_1)) | ~ssPv4(V_397) | ~ssRr(U_1, V_397)))). % 7.20/2.54 tff(c_1108, plain, (![U_1, W_384, V_385]: (ssPv1(U_1) | ssPv3(skf1(U_1)) | ~ssPv1(W_384) | ~ssRr(U_1, W_384) | ~ssPv4(V_385) | ~ssRr(U_1, V_385)))). % 7.20/2.54 tff(c_100, plain, (![X_149, U_146, W_148, V_147]: (ssPv2(X_149) | ~ssPv1(U_146) | ~ssRr(U_146, X_149) | ~ssPv1(W_148) | ~ssRr(U_146, W_148) | ~ssPv4(V_147) | ~ssRr(U_146, V_147)))). % 7.20/2.54 tff(c_1112, plain, (![U_1, V_388]: (ssPv2(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv3(skf1(U_1)) | ~ssPv4(V_388) | ~ssRr(U_1, V_388)))). % 7.20/2.54 tff(c_1064, plain, (![U_1, W_378, V_379]: (ssPv2(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv3(W_378) | ~ssRr(U_1, W_378) | ~ssPv4(V_379) | ~ssRr(U_1, V_379)))). % 7.20/2.54 tff(c_90, plain, (![U_126, X_129, W_128, V_127]: (ssPv1(U_126) | ssPv3(X_129) | ~ssRr(U_126, X_129) | ~ssPv1(W_128) | ~ssRr(U_126, W_128) | ~ssPv4(V_127) | ~ssRr(U_126, V_127)))). % 7.20/2.54 tff(c_102, plain, (![X_153, U_150, W_152, V_151]: (ssPv2(X_153) | ~ssPv2(U_150) | ~ssRr(U_150, X_153) | ~ssPv3(W_152) | ~ssRr(U_150, W_152) | ~ssPv4(V_151) | ~ssRr(U_150, V_151)))). % 7.20/2.54 tff(c_1034, plain, (![U_370]: (~ssPv2(U_370) | ~ssPv4(U_370) | ~ssPv3(U_370)))). % 7.20/2.54 tff(c_78, plain, (![U_102, X_105, W_104, V_103]: (ssPv4(U_102) | ssPv1(X_105) | ssPv3(W_104) | ~ssRr(U_102, X_105) | ~ssRr(U_102, W_104) | ~ssPv2(V_103) | ~ssRr(U_102, V_103)))). % 7.20/2.54 tff(c_1015, plain, (![U_1]: (ssPv1(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv3(U_1)))). % 7.20/2.54 tff(c_933, plain, (![U_1, V_356]: (ssPv3(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv2(U_1) | ~ssPv3(V_356) | ~ssRr(U_1, V_356)))). % 7.20/2.54 tff(c_955, plain, (![U_1]: (ssPv2(U_1) | ssPv3(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv4(skf1(U_1))))). % 7.20/2.54 tff(c_98, plain, (![U_142, X_145, W_144, V_143]: (ssPv1(U_142) | ~ssPv1(X_145) | ~ssRr(U_142, X_145) | ~ssPv2(W_144) | ~ssRr(U_142, W_144) | ~ssPv4(V_143) | ~ssRr(U_142, V_143)))). % 7.20/2.54 tff(c_830, plain, (![U_1, V_347]: (ssPv2(U_1) | ssPv3(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv4(V_347) | ~ssRr(U_1, V_347)))). % 7.20/2.54 tff(c_64, plain, (![W_83, U_81, V_82]: (ssPv3(W_83) | ~ssPv3(U_81) | ~ssPv2(U_81) | ~ssRr(U_81, W_83) | ~ssPv3(V_82) | ~ssRr(U_81, V_82)))). % 7.20/2.54 tff(c_879, plain, (![U_1]: (~ssPv4(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv3(U_1) | ~ssPv1(U_1)))). % 7.20/2.54 tff(c_872, plain, (![V_198, U_349]: (~ssPv4(V_198) | ~ssRr(U_349, V_198) | ~ssPv4(U_349) | ~ssPv3(U_349) | ~ssPv1(U_349)))). % 7.20/2.54 tff(c_852, plain, (![U_348]: (~ssPv4(U_348) | ssPv3(skf1(U_348)) | ~ssPv3(U_348) | ~ssPv1(U_348)))). % 7.20/2.54 tff(c_826, plain, (![U_1]: (ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv1(U_1)))). % 7.20/2.54 tff(c_52, plain, (![U_63, W_65, V_64]: (ssPv2(U_63) | ssPv3(W_65) | ~ssPv4(U_63) | ~ssRr(U_63, W_65) | ~ssPv4(V_64) | ~ssRr(U_63, V_64)))). % 7.20/2.54 tff(c_817, plain, (![U_1, V_340]: (ssPv3(skf1(U_1)) | ssPv4(V_340) | ~ssPv3(U_1) | ~ssPv1(U_1) | ~ssRr(U_1, V_340)))). % 7.20/2.54 tff(c_809, plain, (![U_1]: (~ssPv4(U_1) | ~ssPv3(U_1) | ~ssPv2(skf1(U_1))))). % 7.20/2.54 tff(c_40, plain, (![W_47, V_46, U_45]: (ssPv3(W_47) | ssPv4(V_46) | ~ssPv3(U_45) | ~ssPv1(U_45) | ~ssRr(U_45, W_47) | ~ssRr(U_45, V_46)))). % 7.20/2.54 tff(c_759, plain, (![U_1]: (~ssPv4(skf1(U_1)) | ssPv3(U_1) | ~ssPv2(U_1) | ~ssPv1(U_1)))). % 7.20/2.54 tff(c_752, plain, (![V_332, U_1]: (~ssPv4(V_332) | ~ssRr(U_1, V_332) | ssPv3(U_1) | ~ssPv2(U_1) | ~ssPv1(U_1)))). % 7.20/2.54 tff(c_744, plain, (![U_1, V_330]: (~ssPv2(U_1) | ~ssPv1(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv4(V_330) | ~ssRr(U_1, V_330)))). % 7.20/2.54 tff(c_76, plain, (![U_99, W_101, V_100]: (~ssPv2(U_99) | ~ssPv1(U_99) | ~ssPv1(W_101) | ~ssRr(U_99, W_101) | ~ssPv4(V_100) | ~ssRr(U_99, V_100)))). % 7.20/2.54 tff(c_721, plain, (![U_1, V_324]: (ssPv2(U_1) | ~ssPv3(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv3(V_324) | ~ssRr(U_1, V_324)))). % 7.20/2.54 tff(c_717, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv3(U_1) | ~ssPv2(U_1) | ~ssPv1(U_1)))). % 7.20/2.54 tff(c_68, plain, (![U_87, W_89, V_88]: (ssPv2(U_87) | ~ssPv3(U_87) | ~ssPv2(W_89) | ~ssRr(U_87, W_89) | ~ssPv3(V_88) | ~ssRr(U_87, V_88)))). % 7.20/2.54 tff(c_712, plain, (![U_320]: (~ssPv2(skf1(U_320)) | ssPv3(U_320) | ssPv1(skf1(U_320)) | ~ssPv1(U_320)))). % 7.20/2.54 tff(c_693, plain, (![U_1]: (ssPv3(U_1) | ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv1(U_1)))). % 7.20/2.54 tff(c_679, plain, (![U_1, V_314]: (ssPv3(U_1) | ssPv1(skf1(U_1)) | ssPv3(V_314) | ~ssPv1(U_1) | ~ssRr(U_1, V_314)))). % 7.20/2.54 tff(c_684, plain, (![U_1]: (~ssPv2(skf1(U_1)) | ssPv3(U_1) | ~ssPv4(U_1) | ~ssPv2(U_1)))). % 7.20/2.54 tff(c_672, plain, (![V_275, U_311]: (~ssPv2(V_275) | ~ssRr(U_311, V_275) | ssPv3(U_311) | ~ssPv4(U_311) | ~ssPv2(U_311)))). % 7.20/2.54 tff(c_28, plain, (![U_27, W_29, V_28]: (ssPv3(U_27) | ssPv1(W_29) | ssPv3(V_28) | ~ssPv1(U_27) | ~ssRr(U_27, W_29) | ~ssRr(U_27, V_28)))). % 7.20/2.54 tff(c_658, plain, (![U_310]: (ssPv3(U_310) | ssPv1(skf1(U_310)) | ~ssPv4(U_310) | ~ssPv2(U_310)))). % 7.20/2.54 tff(c_639, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv2(U_1)))). % 7.20/2.54 tff(c_635, plain, (![U_1, V_306]: (ssPv1(skf1(U_1)) | ssPv4(V_306) | ~ssPv4(U_1) | ~ssPv2(U_1) | ~ssRr(U_1, V_306)))). % 7.20/2.54 tff(c_36, plain, (![W_41, V_40, U_39]: (ssPv1(W_41) | ssPv4(V_40) | ~ssPv4(U_39) | ~ssPv2(U_39) | ~ssRr(U_39, W_41) | ~ssRr(U_39, V_40)))). % 7.20/2.54 tff(c_574, plain, (![U_1, V_298]: (ssPv1(U_1) | ~ssPv3(U_1) | ~ssPv3(skf1(U_1)) | ~ssPv4(V_298) | ~ssRr(U_1, V_298)))). % 7.20/2.54 tff(c_594, plain, (![U_1]: (ssPv3(U_1) | ssPv2(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv4(skf1(U_1))))). % 7.20/2.54 tff(c_529, plain, (![U_1, V_292]: (ssPv3(U_1) | ssPv2(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv4(V_292) | ~ssRr(U_1, V_292)))). % 7.20/2.54 tff(c_70, plain, (![U_90, W_92, V_91]: (ssPv1(U_90) | ~ssPv3(U_90) | ~ssPv3(W_92) | ~ssRr(U_90, W_92) | ~ssPv4(V_91) | ~ssRr(U_90, V_91)))). % 7.20/2.54 tff(c_50, plain, (![U_60, W_62, V_61]: (ssPv3(U_60) | ssPv2(W_62) | ~ssPv1(U_60) | ~ssRr(U_60, W_62) | ~ssPv4(V_61) | ~ssRr(U_60, V_61)))). % 7.20/2.54 tff(c_504, plain, (![U_1]: (ssPv3(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv3(U_1) | ~ssPv4(skf1(U_1))))). % 7.20/2.54 tff(c_500, plain, (![U_1, V_286]: (ssPv3(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv3(U_1) | ~ssPv4(V_286) | ~ssRr(U_1, V_286)))). % 7.20/2.55 tff(c_62, plain, (![W_80, U_78, V_79]: (ssPv3(W_80) | ~ssPv4(U_78) | ~ssPv3(U_78) | ~ssRr(U_78, W_80) | ~ssPv4(V_79) | ~ssRr(U_78, V_79)))). % 7.20/2.55 tff(c_487, plain, (![U_1]: (ssPv3(U_1) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1))))). % 7.20/2.55 tff(c_483, plain, (![U_1, V_280]: (ssPv3(U_1) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(V_280) | ~ssRr(U_1, V_280)))). % 7.20/2.55 tff(c_32, plain, (![U_33, W_35, V_34]: (ssPv3(U_33) | ssPv1(U_33) | ssPv1(W_35) | ~ssRr(U_33, W_35) | ~ssPv2(V_34) | ~ssRr(U_33, V_34)))). % 7.20/2.55 tff(c_472, plain, (![U_1, V_275]: (ssPv3(U_1) | ~ssPv4(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv2(V_275) | ~ssRr(U_1, V_275)))). % 7.20/2.55 tff(c_66, plain, (![U_84, W_86, V_85]: (ssPv3(U_84) | ~ssPv4(U_84) | ~ssPv1(W_86) | ~ssRr(U_84, W_86) | ~ssPv2(V_85) | ~ssRr(U_84, V_85)))). % 7.20/2.55 tff(c_464, plain, (![U_1, V_270]: (ssPv2(U_1) | ssPv3(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv3(V_270) | ~ssRr(U_1, V_270)))). % 7.20/2.55 tff(c_56, plain, (![U_69, W_71, V_70]: (ssPv2(U_69) | ssPv3(W_71) | ~ssPv1(U_69) | ~ssRr(U_69, W_71) | ~ssPv3(V_70) | ~ssRr(U_69, V_70)))). % 7.20/2.55 tff(c_395, plain, (![U_1, V_261]: (ssPv4(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv3(U_1) | ~ssPv2(V_261) | ~ssRr(U_1, V_261)))). % 7.20/2.55 tff(c_60, plain, (![W_77, U_75, V_76]: (ssPv4(W_77) | ~ssPv4(U_75) | ~ssPv3(U_75) | ~ssRr(U_75, W_77) | ~ssPv2(V_76) | ~ssRr(U_75, V_76)))). % 7.20/2.55 tff(c_366, plain, (![U_1, V_253]: (ssPv3(U_1) | ssPv2(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv2(V_253) | ~ssRr(U_1, V_253)))). % 7.20/2.55 tff(c_370, plain, (![U_1]: (ssPv3(U_1) | ssPv1(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv4(skf1(U_1))))). % 7.20/2.55 tff(c_362, plain, (![U_1, V_250]: (ssPv3(U_1) | ssPv1(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv4(V_250) | ~ssRr(U_1, V_250)))). % 7.20/2.55 tff(c_48, plain, (![U_57, W_59, V_58]: (ssPv3(U_57) | ssPv2(W_59) | ~ssPv2(U_57) | ~ssRr(U_57, W_59) | ~ssPv2(V_58) | ~ssRr(U_57, V_58)))). % 7.20/2.55 tff(c_44, plain, (![U_51, W_53, V_52]: (ssPv3(U_51) | ssPv1(W_53) | ~ssPv4(U_51) | ~ssRr(U_51, W_53) | ~ssPv4(V_52) | ~ssRr(U_51, V_52)))). % 7.20/2.55 tff(c_353, plain, (![U_246]: (~ssPv2(skf1(U_246)) | ssPv1(skf1(U_246)) | ~ssPv4(U_246) | ~ssPv1(U_246)))). % 7.20/2.55 tff(c_337, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv1(U_1)))). % 7.20/2.55 tff(c_329, plain, (![U_1, V_240]: (ssPv1(skf1(U_1)) | ssPv3(V_240) | ~ssPv4(U_1) | ~ssPv1(U_1) | ~ssRr(U_1, V_240)))). % 7.20/2.55 tff(c_325, plain, (![U_1, V_238]: (ssPv2(U_1) | ssPv2(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv2(V_238) | ~ssRr(U_1, V_238)))). % 7.20/2.55 tff(c_38, plain, (![W_44, V_43, U_42]: (ssPv1(W_44) | ssPv3(V_43) | ~ssPv4(U_42) | ~ssPv1(U_42) | ~ssRr(U_42, W_44) | ~ssRr(U_42, V_43)))). % 7.20/2.55 tff(c_54, plain, (![U_66, W_68, V_67]: (ssPv2(U_66) | ssPv2(W_68) | ~ssPv3(U_66) | ~ssRr(U_66, W_68) | ~ssPv2(V_67) | ~ssRr(U_66, V_67)))). % 7.20/2.55 tff(c_312, plain, (![U_1]: (ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv3(U_1)))). % 7.20/2.55 tff(c_308, plain, (![U_1, V_232]: (ssPv1(U_1) | ssPv1(skf1(U_1)) | ssPv4(V_232) | ~ssPv3(U_1) | ~ssRr(U_1, V_232)))). % 7.20/2.55 tff(c_30, plain, (![U_30, W_32, V_31]: (ssPv1(U_30) | ssPv1(W_32) | ssPv4(V_31) | ~ssPv3(U_30) | ~ssRr(U_30, W_32) | ~ssRr(U_30, V_31)))). % 7.20/2.55 tff(c_300, plain, (![U_1, V_227]: (ssPv2(U_1) | ssPv1(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv4(V_227) | ~ssRr(U_1, V_227)))). % 7.20/2.55 tff(c_58, plain, (![U_72, W_74, V_73]: (ssPv2(U_72) | ssPv1(U_72) | ~ssPv2(W_74) | ~ssRr(U_72, W_74) | ~ssPv4(V_73) | ~ssRr(U_72, V_73)))). % 7.20/2.55 tff(c_275, plain, (![U_1, V_216]: (~ssPv3(U_1) | ~ssPv1(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv4(V_216) | ~ssRr(U_1, V_216)))). % 7.20/2.55 tff(c_34, plain, (![W_38, V_37, U_36]: (ssPv1(W_38) | ssPv4(V_37) | ~ssPv4(U_36) | ~ssPv3(U_36) | ~ssRr(U_36, W_38) | ~ssRr(U_36, V_37)))). % 7.20/2.55 tff(c_74, plain, (![U_96, W_98, V_97]: (~ssPv3(U_96) | ~ssPv1(U_96) | ~ssPv1(W_98) | ~ssRr(U_96, W_98) | ~ssPv4(V_97) | ~ssRr(U_96, V_97)))). % 7.20/2.55 tff(c_262, plain, (![U_1]: (ssPv3(U_1) | ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv2(U_1)))). % 7.20/2.55 tff(c_258, plain, (![U_1, V_210]: (ssPv3(U_1) | ssPv2(skf1(U_1)) | ssPv4(V_210) | ~ssPv2(U_1) | ~ssRr(U_1, V_210)))). % 7.20/2.55 tff(c_26, plain, (![U_24, W_26, V_25]: (ssPv3(U_24) | ssPv2(W_26) | ssPv4(V_25) | ~ssPv2(U_24) | ~ssRr(U_24, W_26) | ~ssRr(U_24, V_25)))). % 7.20/2.55 tff(c_249, plain, (![U_1]: (ssPv4(U_1) | ssPv2(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv3(skf1(U_1))))). % 7.20/2.55 tff(c_245, plain, (![U_1, V_204]: (ssPv4(U_1) | ssPv2(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv3(V_204) | ~ssRr(U_1, V_204)))). % 7.20/2.55 tff(c_42, plain, (![U_48, W_50, V_49]: (ssPv4(U_48) | ssPv2(W_50) | ~ssPv3(U_48) | ~ssRr(U_48, W_50) | ~ssPv3(V_49) | ~ssRr(U_48, V_49)))). % 7.20/2.55 tff(c_215, plain, (![U_1]: (ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ssPv3(U_1) | ssPv2(U_1) | ~ssPv4(U_1)))). % 7.20/2.55 tff(c_232, plain, (![U_1, V_198]: (~ssPv4(U_1) | ~ssPv3(U_1) | ~ssPv3(skf1(U_1)) | ~ssPv4(V_198) | ~ssRr(U_1, V_198)))). % 7.20/2.55 tff(c_72, plain, (![U_93, W_95, V_94]: (~ssPv4(U_93) | ~ssPv3(U_93) | ~ssPv3(W_95) | ~ssRr(U_93, W_95) | ~ssPv4(V_94) | ~ssRr(U_93, V_94)))). % 7.20/2.55 tff(c_223, plain, (![U_1]: (ssPv3(U_1) | ssPv2(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv3(skf1(U_1))))). % 7.20/2.55 tff(c_219, plain, (![U_1, V_192]: (ssPv3(U_1) | ssPv2(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv3(V_192) | ~ssRr(U_1, V_192)))). % 7.20/2.55 tff(c_46, plain, (![U_54, W_56, V_55]: (ssPv3(U_54) | ssPv2(W_56) | ~ssPv2(U_54) | ~ssRr(U_54, W_56) | ~ssPv3(V_55) | ~ssRr(U_54, V_55)))). % 7.20/2.55 tff(c_210, plain, (![U_188]: (ssPv1(U_188) | ~ssPv3(U_188) | ~ssPv2(U_188)))). % 7.20/2.55 tff(c_174, plain, (![U_1]: (ssPv3(U_1) | ssPv2(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv1(U_1)))). % 7.20/2.55 tff(c_10, plain, (![U_8, V_9]: (ssPv3(U_8) | ssPv2(V_9) | ~ssPv2(U_8) | ~ssPv1(U_8) | ~ssRr(U_8, V_9)))). % 7.20/2.55 tff(c_158, plain, (![U_1]: (ssPv1(U_1) | ~ssPv4(U_1) | ~ssPv2(U_1) | ~ssPv2(skf1(U_1))))). % 7.20/2.55 tff(c_20, plain, (![U_18, V_19]: (ssPv1(U_18) | ~ssPv4(U_18) | ~ssPv2(U_18) | ~ssPv2(V_19) | ~ssRr(U_18, V_19)))). % 7.20/2.55 tff(c_148, plain, (![U_1]: (ssPv3(U_1) | ~ssPv4(U_1) | ~ssPv1(U_1) | ~ssPv4(skf1(U_1))))). % 7.20/2.55 tff(c_18, plain, (![U_16, V_17]: (ssPv3(U_16) | ~ssPv4(U_16) | ~ssPv1(U_16) | ~ssPv4(V_17) | ~ssRr(U_16, V_17)))). % 7.20/2.55 tff(c_138, plain, (![U_1]: (ssPv4(U_1) | ssPv1(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(U_1)))). % 7.20/2.55 tff(c_6, plain, (![U_4, V_5]: (ssPv4(U_4) | ssPv1(U_4) | ssPv1(V_5) | ~ssPv2(U_4) | ~ssRr(U_4, V_5)))). % 7.20/2.55 tff(c_132, plain, (![U_1]: (ssPv3(U_1) | ssPv2(U_1) | ~ssPv1(U_1) | ~ssPv2(skf1(U_1))))). % 7.20/2.55 tff(c_12, plain, (![U_10, V_11]: (ssPv3(U_10) | ssPv2(U_10) | ~ssPv1(U_10) | ~ssPv2(V_11) | ~ssRr(U_10, V_11)))). % 7.20/2.55 tff(c_126, plain, (![U_1]: (ssPv3(U_1) | ssPv2(U_1) | ssPv1(U_1) | ~ssPv1(skf1(U_1))))). % 7.20/2.55 tff(c_8, plain, (![U_6, V_7]: (ssPv3(U_6) | ssPv2(U_6) | ssPv1(U_6) | ~ssPv1(V_7) | ~ssRr(U_6, V_7)))). % 7.20/2.55 tff(c_114, plain, (![U_1]: (ssPv3(U_1) | ssPv2(U_1) | ssPv3(skf1(U_1)) | ~ssPv4(U_1)))). % 7.20/2.55 tff(c_4, plain, (![U_2, V_3]: (ssPv3(U_2) | ssPv2(U_2) | ssPv3(V_3) | ~ssPv4(U_2) | ~ssRr(U_2, V_3)))). % 7.20/2.55 tff(c_2, plain, (![U_1]: (ssRr(U_1, skf1(U_1))))). % 7.20/2.55 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 7.20/2.55 %------------------------------------------------------------------------------