%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN757-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 : n017.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.16s 2.59s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : SYN757-1 : TPTP v9.0.0. Released v2.5.0. % 0.08/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.35 % Computer : n017.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Wed Apr 9 08:15:25 EDT 2025 % 0.13/0.35 % CPUTime : % 7.16/2.59 % 7.16/2.59 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.16/2.59 % 7.16/2.59 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.16/2.60 %$ ssRr > ssPv4 > ssPv3 > ssPv2 > ssPv1 > #nlpp > skf1 % 7.16/2.60 % 7.16/2.60 %Foreground sorts: % 7.16/2.60 % 7.16/2.60 % 7.16/2.60 %Background operators: % 7.16/2.60 % 7.16/2.60 % 7.16/2.60 %Foreground operators: % 7.16/2.60 tff(skf1, type, skf1: $i > $i). % 7.16/2.60 tff(ssPv1, type, ssPv1: $i > $o). % 7.16/2.60 tff(ssPv3, type, ssPv3: $i > $o). % 7.16/2.60 tff(ssRr, type, ssRr: ($i * $i) > $o). % 7.16/2.60 tff(ssPv4, type, ssPv4: $i > $o). % 7.16/2.60 tff(ssPv2, type, ssPv2: $i > $o). % 7.16/2.60 % 7.16/2.60 %Saturated clause set: % 7.16/2.60 tff(c_2077, plain, (![U_542]: (ssPv3(U_542) | ssPv1(U_542) | ~ssPv4(U_542) | ssPv2(skf1(U_542)) | ssPv1(skf1(U_542))))). % 7.16/2.60 tff(c_1996, plain, (![U_1]: (ssPv3(U_1) | ~ssPv4(U_1) | ~ssPv4(skf1(U_1)) | ssPv2(skf1(U_1)) | ssPv2(U_1) | ~ssPv1(skf1(U_1))))). % 7.16/2.60 tff(c_1144, plain, (![U_428, V_215]: (ssPv3(U_428) | ~ssPv4(U_428) | ~ssPv4(V_215) | ~ssRr(U_428, V_215) | ssPv2(skf1(U_428)) | ssPv2(U_428) | ~ssPv1(skf1(U_428))))). % 7.16/2.60 tff(c_1972, plain, (![U_535]: (ssPv3(U_535) | ~ssPv4(U_535) | ssPv2(U_535) | ssPv2(skf1(U_535)) | ssPv1(skf1(U_535))))). % 7.16/2.60 tff(c_1891, plain, (![U_1]: (ssPv3(U_1) | ~ssPv4(U_1) | ~ssPv4(skf1(U_1)) | ssPv2(U_1) | ssPv2(skf1(U_1)) | ~ssPv1(U_1)))). % 7.16/2.60 tff(c_758, plain, (![U_323, V_215]: (ssPv3(U_323) | ~ssPv4(U_323) | ~ssPv4(V_215) | ~ssRr(U_323, V_215) | ssPv2(U_323) | ssPv2(skf1(U_323)) | ~ssPv1(U_323)))). % 7.16/2.60 tff(c_1846, plain, (![U_1]: (ssPv3(U_1) | ~ssPv4(U_1) | ~ssPv4(skf1(U_1)) | ssPv2(U_1) | ~ssPv1(U_1) | ~ssPv1(skf1(U_1))))). % 7.16/2.60 tff(c_667, plain, (![U_299, V_215]: (ssPv3(U_299) | ~ssPv4(U_299) | ~ssPv4(V_215) | ~ssRr(U_299, V_215) | ssPv2(U_299) | ~ssPv1(U_299) | ~ssPv1(skf1(U_299))))). % 7.16/2.60 tff(c_1801, plain, (![U_1]: (ssPv3(U_1) | ~ssPv4(skf1(U_1)) | ssPv1(U_1) | ~ssPv4(U_1) | ~ssPv1(skf1(U_1))))). % 7.16/2.60 tff(c_1697, plain, (![U_513, V_215]: (ssPv3(U_513) | ~ssPv4(V_215) | ~ssRr(U_513, V_215) | ssPv1(U_513) | ~ssPv4(U_513) | ~ssPv1(skf1(U_513))))). % 7.16/2.60 tff(c_1757, plain, (![U_1]: (ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv1(U_1)))). % 7.16/2.60 tff(c_1756, plain, (![U_520]: (ssPv4(U_520) | ssPv3(skf1(U_520)) | ssPv2(skf1(U_520)) | ssPv1(skf1(U_520))))). % 7.16/2.61 tff(c_1760, plain, (![U_1]: (ssPv3(skf1(U_1)) | ssPv4(U_1) | ssPv2(U_1) | ssPv1(skf1(U_1))))). % 7.16/2.61 tff(c_1720, plain, (![U_1]: (ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv4(skf1(U_1))))). % 7.16/2.61 tff(c_1716, plain, (![U_1, V_517]: (ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv4(V_517) | ~ssRr(U_1, V_517)))). % 7.16/2.61 tff(c_1316, plain, (![U_1, W_470, V_471]: (ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv3(W_470) | ~ssRr(U_1, W_470) | ~ssPv4(V_471) | ~ssRr(U_1, V_471)))). % 7.16/2.61 tff(c_1696, plain, (![U_513]: (ssPv2(skf1(U_513)) | ~ssPv3(U_513) | ssPv1(U_513) | ~ssPv4(U_513) | ~ssPv1(skf1(U_513))))). % 7.16/2.61 tff(c_1682, plain, (![U_512]: (ssPv1(U_512) | ssPv3(skf1(U_512)) | ~ssPv4(U_512) | ~ssPv1(skf1(U_512))))). % 7.16/2.61 tff(c_1660, plain, (![U_1]: (ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv1(skf1(U_1))))). % 7.16/2.61 tff(c_1656, plain, (![U_1, V_509]: (ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv1(V_509) | ~ssRr(U_1, V_509)))). % 7.16/2.61 tff(c_1344, plain, (![U_1, W_475, V_477]: (ssPv3(skf1(U_1)) | ssPv4(W_475) | ~ssPv4(U_1) | ~ssRr(U_1, W_475) | ~ssPv1(V_477) | ~ssRr(U_1, V_477)))). % 7.16/2.61 tff(c_1188, plain, (![U_1, W_456, V_457]: (ssPv4(U_1) | ssPv2(skf1(U_1)) | ~ssPv2(W_456) | ~ssRr(U_1, W_456) | ~ssPv4(V_457) | ~ssRr(U_1, V_457)))). % 7.16/2.61 tff(c_1434, plain, (![U_495]: (ssPv3(U_495) | ssPv2(U_495) | ssPv1(U_495) | ssPv1(skf1(U_495)) | ~ssPv4(U_495) | ~ssPv3(skf1(U_495))))). % 7.16/2.61 tff(c_1535, plain, (![U_1, V_499]: (ssPv4(U_1) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv3(V_499) | ~ssRr(U_1, V_499)))). % 7.16/2.61 tff(c_1515, plain, (![U_1]: (ssPv3(U_1) | ssPv1(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv1(U_1)))). % 7.16/2.61 tff(c_1397, plain, (![U_1, W_488, V_489]: (ssPv4(U_1) | ssPv3(skf1(U_1)) | ssPv4(W_488) | ~ssRr(U_1, W_488) | ~ssPv3(V_489) | ~ssRr(U_1, V_489)))). % 7.16/2.61 tff(c_1405, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv3(skf1(U_1))))). % 7.16/2.61 tff(c_1401, plain, (![U_1, V_492]: (ssPv1(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv3(V_492) | ~ssRr(U_1, V_492)))). % 7.16/2.61 tff(c_1348, plain, (![U_1, W_479, V_481]: (ssPv1(skf1(U_1)) | ssPv4(W_479) | ~ssPv4(U_1) | ~ssRr(U_1, W_479) | ~ssPv3(V_481) | ~ssRr(U_1, V_481)))). % 7.16/2.61 tff(c_90, plain, (![U_129, X_132, W_131, V_130]: (ssPv4(U_129) | ssPv3(X_132) | ssPv4(W_131) | ~ssRr(U_129, X_132) | ~ssRr(U_129, W_131) | ~ssPv3(V_130) | ~ssRr(U_129, V_130)))). % 7.16/2.61 tff(c_1381, plain, (![U_1]: (~ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv1(U_1)))). % 7.16/2.61 tff(c_1352, plain, (![U_1]: (~ssPv4(skf1(U_1)) | ~ssPv1(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv1(U_1)))). % 7.16/2.61 tff(c_1309, plain, (![V_311, U_467]: (~ssPv4(V_311) | ~ssRr(U_467, V_311) | ~ssPv1(skf1(U_467)) | ~ssPv3(U_467) | ~ssPv1(U_467)))). % 7.16/2.61 tff(c_96, plain, (![X_144, W_143, U_141, V_142]: (ssPv1(X_144) | ssPv4(W_143) | ~ssPv4(U_141) | ~ssRr(U_141, X_144) | ~ssRr(U_141, W_143) | ~ssPv3(V_142) | ~ssRr(U_141, V_142)))). % 7.16/2.61 tff(c_98, plain, (![X_148, W_147, U_145, V_146]: (ssPv3(X_148) | ssPv4(W_147) | ~ssPv4(U_145) | ~ssRr(U_145, X_148) | ~ssRr(U_145, W_147) | ~ssPv1(V_146) | ~ssRr(U_145, V_146)))). % 7.16/2.61 tff(c_1312, plain, (![U_467]: (ssPv4(U_467) | ssPv2(U_467) | ~ssPv1(skf1(U_467)) | ~ssPv3(U_467) | ~ssPv1(U_467)))). % 7.16/2.61 tff(c_1276, plain, (![U_427]: (~ssPv3(U_427) | ssPv2(skf1(U_427)) | ssPv2(U_427) | ~ssPv1(skf1(U_427))))). % 7.16/2.61 tff(c_82, plain, (![U_113, X_116, W_115, V_114]: (ssPv4(U_113) | ssPv1(X_116) | ssPv3(W_115) | ~ssRr(U_113, X_116) | ~ssRr(U_113, W_115) | ~ssPv4(V_114) | ~ssRr(U_113, V_114)))). % 7.16/2.61 tff(c_1288, plain, (![U_1]: (~ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv1(U_1)))). % 7.16/2.61 tff(c_1200, plain, (![U_1]: (ssPv2(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv3(skf1(U_1))))). % 7.16/2.61 tff(c_1196, plain, (![U_1, V_463]: (ssPv2(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv3(V_463) | ~ssRr(U_1, V_463)))). % 7.16/2.61 tff(c_1172, plain, (![U_1, W_445, V_446]: (ssPv2(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv1(W_445) | ~ssRr(U_1, W_445) | ~ssPv3(V_446) | ~ssRr(U_1, V_446)))). % 7.16/2.61 tff(c_919, plain, (![U_1, W_382, V_383]: (ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(W_382) | ~ssRr(U_1, W_382) | ~ssPv4(V_383) | ~ssRr(U_1, V_383)))). % 7.16/2.61 tff(c_100, plain, (![U_149, X_152, W_151, V_150]: (ssPv4(U_149) | ssPv2(X_152) | ~ssRr(U_149, X_152) | ~ssPv2(W_151) | ~ssRr(U_149, W_151) | ~ssPv4(V_150) | ~ssRr(U_149, V_150)))). % 7.16/2.61 tff(c_1180, plain, (![U_1, V_451]: (ssPv2(U_1) | ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ssPv4(V_451) | ~ssRr(U_1, V_451)))). % 7.16/2.61 tff(c_1148, plain, (![U_1, W_431, V_432]: (ssPv2(U_1) | ssPv1(skf1(U_1)) | ssPv2(W_431) | ssPv4(V_432) | ~ssRr(U_1, W_431) | ~ssRr(U_1, V_432)))). % 7.16/2.61 tff(c_1168, plain, (![U_1, V_442]: (ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv1(V_442) | ~ssRr(U_1, V_442)))). % 7.16/2.61 tff(c_102, plain, (![X_156, U_153, W_155, V_154]: (ssPv2(X_156) | ~ssPv3(U_153) | ~ssRr(U_153, X_156) | ~ssPv1(W_155) | ~ssRr(U_153, W_155) | ~ssPv3(V_154) | ~ssRr(U_153, V_154)))). % 7.16/2.61 tff(c_1107, plain, (![U_1, W_423, V_424]: (ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv4(W_423) | ~ssRr(U_1, W_423) | ~ssPv1(V_424) | ~ssRr(U_1, V_424)))). % 7.16/2.61 tff(c_1160, plain, (![U_1, V_437]: (ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv1(V_437) | ~ssRr(U_1, V_437)))). % 7.16/2.61 tff(c_1058, plain, (![U_1, W_409, V_410]: (ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv3(W_409) | ~ssRr(U_1, W_409) | ~ssPv1(V_410) | ~ssRr(U_1, V_410)))). % 7.16/2.61 tff(c_1140, plain, (![U_427]: (ssPv3(U_427) | ssPv1(U_427) | ssPv2(U_427) | ssPv3(skf1(U_427)) | ~ssPv1(skf1(U_427))))). % 7.16/2.61 tff(c_78, plain, (![U_105, X_108, W_107, V_106]: (ssPv2(U_105) | ssPv1(X_108) | ssPv2(W_107) | ssPv4(V_106) | ~ssRr(U_105, X_108) | ~ssRr(U_105, W_107) | ~ssRr(U_105, V_106)))). % 7.16/2.61 tff(c_1134, plain, (![U_427]: (ssPv2(skf1(U_427)) | ssPv2(U_427) | ssPv3(skf1(U_427)) | ~ssPv1(skf1(U_427))))). % 7.16/2.61 tff(c_1111, plain, (![U_1]: (ssPv2(U_1) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv1(skf1(U_1))))). % 7.16/2.62 tff(c_1103, plain, (![U_1, V_420]: (ssPv2(U_1) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv1(V_420) | ~ssRr(U_1, V_420)))). % 7.16/2.62 tff(c_92, plain, (![U_133, X_136, W_135, V_134]: (ssPv4(U_133) | ssPv1(X_136) | ssPv4(W_135) | ~ssRr(U_133, X_136) | ~ssRr(U_133, W_135) | ~ssPv1(V_134) | ~ssRr(U_133, V_134)))). % 7.16/2.62 tff(c_870, plain, (![U_1, W_371, V_372]: (ssPv2(U_1) | ssPv3(skf1(U_1)) | ssPv4(W_371) | ~ssRr(U_1, W_371) | ~ssPv1(V_372) | ~ssRr(U_1, V_372)))). % 7.16/2.62 tff(c_1093, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv2(U_1) | ssPv3(skf1(U_1)) | ~ssPv3(U_1)))). % 7.16/2.62 tff(c_1066, plain, (![U_1]: (ssPv2(U_1) | ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv4(skf1(U_1))))). % 7.16/2.62 tff(c_1062, plain, (![U_1, V_413]: (ssPv2(U_1) | ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv4(V_413) | ~ssRr(U_1, V_413)))). % 7.16/2.62 tff(c_1042, plain, (![U_1, W_399, V_400]: (ssPv2(U_1) | ssPv2(skf1(U_1)) | ssPv3(W_399) | ~ssRr(U_1, W_399) | ~ssPv4(V_400) | ~ssRr(U_1, V_400)))). % 7.16/2.62 tff(c_84, plain, (![U_117, X_120, W_119, V_118]: (ssPv4(U_117) | ssPv1(X_120) | ssPv3(W_119) | ~ssRr(U_117, X_120) | ~ssRr(U_117, W_119) | ~ssPv1(V_118) | ~ssRr(U_117, V_118)))). % 7.16/2.62 tff(c_1050, plain, (![U_1]: (ssPv2(U_1) | ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ssPv3(skf1(U_1))))). % 7.16/2.62 tff(c_1046, plain, (![U_1, V_403]: (ssPv2(U_1) | ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ssPv3(V_403) | ~ssRr(U_1, V_403)))). % 7.16/2.62 tff(c_971, plain, (![U_1, W_389, V_390]: (ssPv2(U_1) | ssPv1(skf1(U_1)) | ssPv2(W_389) | ssPv3(V_390) | ~ssRr(U_1, W_389) | ~ssRr(U_1, V_390)))). % 7.16/2.62 tff(c_88, plain, (![U_125, X_128, W_127, V_126]: (ssPv2(U_125) | ssPv2(X_128) | ssPv3(W_127) | ~ssRr(U_125, X_128) | ~ssRr(U_125, W_127) | ~ssPv4(V_126) | ~ssRr(U_125, V_126)))). % 7.16/2.62 tff(c_1026, plain, (![U_1]: (~ssPv3(U_1) | ssPv4(U_1) | ~ssPv2(U_1) | ~ssPv1(U_1) | ~ssPv1(skf1(U_1))))). % 7.16/2.62 tff(c_1004, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv3(U_1) | ~ssPv4(U_1) | ~ssPv2(U_1)))). % 7.16/2.62 tff(c_80, plain, (![U_109, X_112, W_111, V_110]: (ssPv2(U_109) | ssPv1(X_112) | ssPv2(W_111) | ssPv3(V_110) | ~ssRr(U_109, X_112) | ~ssRr(U_109, W_111) | ~ssRr(U_109, V_110)))). % 7.16/2.62 tff(c_94, plain, (![U_137, X_140, W_139, V_138]: (ssPv4(U_137) | ssPv1(X_140) | ~ssRr(U_137, X_140) | ~ssPv1(W_139) | ~ssRr(U_137, W_139) | ~ssPv4(V_138) | ~ssRr(U_137, V_138)))). % 7.16/2.62 tff(c_866, plain, (![U_1]: (ssPv3(U_1) | ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv2(U_1)))). % 7.16/2.62 tff(c_86, plain, (![U_121, X_124, W_123, V_122]: (ssPv2(U_121) | ssPv3(X_124) | ssPv4(W_123) | ~ssRr(U_121, X_124) | ~ssRr(U_121, W_123) | ~ssPv1(V_122) | ~ssRr(U_121, V_122)))). % 7.16/2.62 tff(c_843, plain, (![U_1, V_363]: (ssPv3(U_1) | ssPv1(skf1(U_1)) | ssPv3(V_363) | ~ssPv2(U_1) | ~ssRr(U_1, V_363)))). % 7.16/2.62 tff(c_847, plain, (![U_1]: (ssPv2(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv1(U_1) | ~ssPv1(skf1(U_1))))). % 7.16/2.62 tff(c_839, plain, (![U_1, V_360]: (ssPv2(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv1(U_1) | ~ssPv1(V_360) | ~ssRr(U_1, V_360)))). % 7.16/2.62 tff(c_26, plain, (![U_27, W_29, V_28]: (ssPv3(U_27) | ssPv1(W_29) | ssPv3(V_28) | ~ssPv2(U_27) | ~ssRr(U_27, W_29) | ~ssRr(U_27, V_28)))). % 7.16/2.62 tff(c_70, plain, (![W_95, U_93, V_94]: (ssPv2(W_95) | ~ssPv2(U_93) | ~ssPv1(U_93) | ~ssRr(U_93, W_95) | ~ssPv1(V_94) | ~ssRr(U_93, V_94)))). % 7.16/2.62 tff(c_831, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv1(U_1)))). % 7.16/2.62 tff(c_819, plain, (![U_1, V_350]: (ssPv1(skf1(U_1)) | ssPv3(V_350) | ~ssPv4(U_1) | ~ssPv1(U_1) | ~ssRr(U_1, V_350)))). % 7.16/2.62 tff(c_823, plain, (![U_1]: (ssPv4(U_1) | ssPv3(U_1) | ssPv2(skf1(U_1)) | ssPv3(skf1(U_1))))). % 7.16/2.62 tff(c_815, plain, (![U_1, V_348]: (ssPv4(U_1) | ssPv3(U_1) | ssPv2(skf1(U_1)) | ssPv3(V_348) | ~ssRr(U_1, V_348)))). % 7.16/2.62 tff(c_46, plain, (![W_59, V_58, U_57]: (ssPv1(W_59) | ssPv3(V_58) | ~ssPv4(U_57) | ~ssPv1(U_57) | ~ssRr(U_57, W_59) | ~ssRr(U_57, V_58)))). % 7.16/2.62 tff(c_20, plain, (![U_18, W_20, V_19]: (ssPv4(U_18) | ssPv3(U_18) | ssPv2(W_20) | ssPv3(V_19) | ~ssRr(U_18, W_20) | ~ssRr(U_18, V_19)))). % 7.16/2.62 tff(c_807, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv2(U_1)))). % 7.16/2.62 tff(c_803, plain, (![U_1, V_341]: (ssPv1(skf1(U_1)) | ssPv3(V_341) | ~ssPv3(U_1) | ~ssPv2(U_1) | ~ssRr(U_1, V_341)))). % 7.16/2.62 tff(c_44, plain, (![W_56, V_55, U_54]: (ssPv1(W_56) | ssPv3(V_55) | ~ssPv3(U_54) | ~ssPv2(U_54) | ~ssRr(U_54, W_56) | ~ssRr(U_54, V_55)))). % 7.16/2.62 tff(c_782, plain, (![U_1]: (ssPv4(U_1) | ssPv2(U_1) | ssPv4(skf1(U_1)) | ~ssPv1(skf1(U_1))))). % 7.16/2.62 tff(c_778, plain, (![U_1, V_336]: (ssPv4(U_1) | ssPv2(U_1) | ssPv4(skf1(U_1)) | ~ssPv1(V_336) | ~ssRr(U_1, V_336)))). % 7.16/2.62 tff(c_34, plain, (![U_39, W_41, V_40]: (ssPv4(U_39) | ssPv2(U_39) | ssPv4(W_41) | ~ssRr(U_39, W_41) | ~ssPv1(V_40) | ~ssRr(U_39, V_40)))). % 7.16/2.62 tff(c_766, plain, (![U_1, V_329]: (ssPv4(U_1) | ssPv2(U_1) | ssPv1(skf1(U_1)) | ~ssPv1(V_329) | ~ssRr(U_1, V_329)))). % 7.16/2.62 tff(c_762, plain, (![U_1, V_326]: (~ssPv3(U_1) | ~ssPv1(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv3(V_326) | ~ssRr(U_1, V_326)))). % 7.16/2.62 tff(c_38, plain, (![U_45, W_47, V_46]: (ssPv4(U_45) | ssPv2(U_45) | ssPv1(W_47) | ~ssRr(U_45, W_47) | ~ssPv1(V_46) | ~ssRr(U_45, V_46)))). % 7.16/2.62 tff(c_76, plain, (![U_102, W_104, V_103]: (~ssPv3(U_102) | ~ssPv1(U_102) | ~ssPv1(W_104) | ~ssRr(U_102, W_104) | ~ssPv3(V_103) | ~ssRr(U_102, V_103)))). % 7.16/2.62 tff(c_754, plain, (![U_1]: (ssPv2(U_1) | ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv1(U_1)))). % 7.16/2.62 tff(c_750, plain, (![U_1, V_320]: (ssPv2(U_1) | ssPv2(skf1(U_1)) | ssPv3(V_320) | ~ssPv1(U_1) | ~ssRr(U_1, V_320)))). % 7.16/2.62 tff(c_32, plain, (![U_36, W_38, V_37]: (ssPv2(U_36) | ssPv2(W_38) | ssPv3(V_37) | ~ssPv1(U_36) | ~ssRr(U_36, W_38) | ~ssRr(U_36, V_37)))). % 7.16/2.62 tff(c_691, plain, (![U_1, V_311]: (~ssPv3(U_1) | ~ssPv1(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv4(V_311) | ~ssRr(U_1, V_311)))). % 7.16/2.62 tff(c_720, plain, (![U_1]: (ssPv2(U_1) | ssPv1(U_1) | ssPv2(skf1(U_1))))). % 7.16/2.62 tff(c_74, plain, (![U_99, W_101, V_100]: (~ssPv3(U_99) | ~ssPv1(U_99) | ~ssPv2(W_101) | ~ssRr(U_99, W_101) | ~ssPv4(V_100) | ~ssRr(U_99, V_100)))). % 7.16/2.62 tff(c_40, plain, (![U_48, W_50, V_49]: (ssPv2(U_48) | ssPv1(U_48) | ssPv2(W_50) | ~ssRr(U_48, W_50) | ~ssPv4(V_49) | ~ssRr(U_48, V_49)))). % 7.16/2.62 tff(c_679, plain, (![U_1, V_303]: (ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv1(V_303) | ~ssRr(U_1, V_303)))). % 7.16/2.62 tff(c_52, plain, (![U_66, W_68, V_67]: (ssPv4(U_66) | ssPv1(W_68) | ~ssPv3(U_66) | ~ssRr(U_66, W_68) | ~ssPv1(V_67) | ~ssRr(U_66, V_67)))). % 7.16/2.62 tff(c_542, plain, (![U_273]: (ssPv1(U_273) | ~ssPv4(U_273) | ssPv1(skf1(U_273)) | ssPv3(skf1(U_273)) | ssPv2(skf1(U_273))))). % 7.16/2.62 tff(c_659, plain, (![U_1]: (ssPv2(U_1) | ssPv3(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv1(skf1(U_1))))). % 7.16/2.62 tff(c_629, plain, (![U_1, V_294]: (ssPv2(U_1) | ssPv3(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv1(V_294) | ~ssRr(U_1, V_294)))). % 7.16/2.62 tff(c_638, plain, (![U_1]: (ssPv4(U_1) | ssPv2(U_1) | ssPv1(U_1)))). % 7.16/2.62 tff(c_56, plain, (![U_72, W_74, V_73]: (ssPv2(U_72) | ssPv3(W_74) | ~ssPv1(U_72) | ~ssRr(U_72, W_74) | ~ssPv1(V_73) | ~ssRr(U_72, V_73)))). % 7.16/2.62 tff(c_613, plain, (![U_1]: (ssPv4(U_1) | ssPv2(U_1) | ssPv3(skf1(U_1)) | ~ssPv1(skf1(U_1))))). % 7.16/2.62 tff(c_597, plain, (![U_1, V_287]: (ssPv4(U_1) | ssPv2(U_1) | ssPv3(skf1(U_1)) | ~ssPv1(V_287) | ~ssRr(U_1, V_287)))). % 7.16/2.62 tff(c_36, plain, (![U_42, W_44, V_43]: (ssPv4(U_42) | ssPv2(U_42) | ssPv3(W_44) | ~ssRr(U_42, W_44) | ~ssPv1(V_43) | ~ssRr(U_42, V_43)))). % 7.16/2.62 tff(c_569, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv1(U_1)))). % 7.16/2.62 tff(c_552, plain, (![U_1, V_277]: (ssPv2(skf1(U_1)) | ssPv3(V_277) | ~ssPv3(U_1) | ~ssPv1(U_1) | ~ssRr(U_1, V_277)))). % 7.16/2.62 tff(c_562, plain, (![U_279]: (ssPv1(U_279) | ssPv4(U_279) | ssPv3(U_279) | ssPv1(skf1(U_279)) | ~ssPv2(U_279)))). % 7.16/2.62 tff(c_548, plain, (![U_1]: (ssPv3(U_1) | ssPv1(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv2(U_1)))). % 7.16/2.62 tff(c_50, plain, (![W_65, V_64, U_63]: (ssPv2(W_65) | ssPv3(V_64) | ~ssPv3(U_63) | ~ssPv1(U_63) | ~ssRr(U_63, W_65) | ~ssRr(U_63, V_64)))). % 7.16/2.62 tff(c_507, plain, (![U_1, V_270]: (ssPv3(U_1) | ssPv1(skf1(U_1)) | ssPv2(V_270) | ~ssPv2(U_1) | ~ssRr(U_1, V_270)))). % 7.16/2.62 tff(c_511, plain, (![U_1]: (ssPv1(U_1) | ssPv3(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv4(skf1(U_1))))). % 7.16/2.62 tff(c_503, plain, (![U_1, V_267]: (ssPv1(U_1) | ssPv3(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv4(V_267) | ~ssRr(U_1, V_267)))). % 7.16/2.62 tff(c_28, plain, (![U_30, W_32, V_31]: (ssPv3(U_30) | ssPv1(W_32) | ssPv2(V_31) | ~ssPv2(U_30) | ~ssRr(U_30, W_32) | ~ssRr(U_30, V_31)))). % 7.16/2.62 tff(c_60, plain, (![U_78, W_80, V_79]: (ssPv1(U_78) | ssPv3(W_80) | ~ssPv4(U_78) | ~ssRr(U_78, W_80) | ~ssPv4(V_79) | ~ssRr(U_78, V_79)))). % 7.16/2.62 tff(c_486, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv2(U_1) | ssPv1(U_1) | ~ssPv3(U_1)))). % 7.16/2.62 tff(c_42, plain, (![U_51, W_53, V_52]: (ssPv2(U_51) | ssPv1(U_51) | ssPv2(W_53) | ~ssRr(U_51, W_53) | ~ssPv3(V_52) | ~ssRr(U_51, V_52)))). % 7.16/2.62 tff(c_426, plain, (![U_1, V_252]: (ssPv2(U_1) | ssPv2(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv2(V_252) | ~ssRr(U_1, V_252)))). % 7.16/2.62 tff(c_430, plain, (![U_1]: (ssPv3(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv3(U_1) | ~ssPv2(skf1(U_1))))). % 7.16/2.62 tff(c_422, plain, (![U_1, V_249]: (ssPv3(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv3(U_1) | ~ssPv2(V_249) | ~ssRr(U_1, V_249)))). % 7.16/2.62 tff(c_58, plain, (![U_75, W_77, V_76]: (ssPv2(U_75) | ssPv2(W_77) | ~ssPv1(U_75) | ~ssRr(U_75, W_77) | ~ssPv2(V_76) | ~ssRr(U_75, V_76)))). % 7.16/2.63 tff(c_66, plain, (![W_89, U_87, V_88]: (ssPv3(W_89) | ~ssPv4(U_87) | ~ssPv3(U_87) | ~ssRr(U_87, W_89) | ~ssPv2(V_88) | ~ssRr(U_87, V_88)))). % 7.16/2.63 tff(c_384, plain, (![U_238]: (ssPv1(skf1(U_238)) | ~ssPv2(skf1(U_238)) | ssPv3(skf1(U_238)) | ~ssPv3(U_238) | ~ssPv1(U_238)))). % 7.16/2.63 tff(c_329, plain, (![U_227]: (ssPv1(skf1(U_227)) | ssPv3(skf1(U_227)) | ssPv4(U_227) | ~ssPv2(U_227) | ~ssPv2(skf1(U_227))))). % 7.16/2.63 tff(c_394, plain, (![U_1]: (ssPv3(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv2(U_1) | ~ssPv2(skf1(U_1))))). % 7.16/2.63 tff(c_390, plain, (![U_1, V_241]: (ssPv3(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv2(U_1) | ~ssPv2(V_241) | ~ssRr(U_1, V_241)))). % 7.16/2.63 tff(c_68, plain, (![W_92, U_90, V_91]: (ssPv3(W_92) | ~ssPv3(U_90) | ~ssPv2(U_90) | ~ssRr(U_90, W_92) | ~ssPv2(V_91) | ~ssRr(U_90, V_91)))). % 7.16/2.63 tff(c_373, plain, (![U_1]: (ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv1(U_1)))). % 7.16/2.63 tff(c_357, plain, (![U_1, V_233]: (ssPv3(skf1(U_1)) | ssPv4(V_233) | ~ssPv3(U_1) | ~ssPv1(U_1) | ~ssRr(U_1, V_233)))). % 7.16/2.63 tff(c_48, plain, (![W_62, V_61, U_60]: (ssPv3(W_62) | ssPv4(V_61) | ~ssPv3(U_60) | ~ssPv1(U_60) | ~ssRr(U_60, W_62) | ~ssRr(U_60, V_61)))). % 7.16/2.63 tff(c_330, plain, (![U_227]: (ssPv3(U_227) | ssPv1(U_227) | ssPv4(U_227) | ~ssPv2(U_227) | ~ssPv2(skf1(U_227))))). % 7.16/2.63 tff(c_318, plain, (![U_1]: (ssPv4(U_1) | ssPv4(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv2(skf1(U_1))))). % 7.16/2.63 tff(c_310, plain, (![U_1, V_221]: (ssPv4(U_1) | ssPv4(skf1(U_1)) | ~ssPv2(U_1) | ~ssPv2(V_221) | ~ssRr(U_1, V_221)))). % 7.16/2.63 tff(c_24, plain, (![U_24, W_26, V_25]: (ssPv2(U_24) | ssPv1(U_24) | ssPv2(W_26) | ssPv4(V_25) | ~ssRr(U_24, W_26) | ~ssRr(U_24, V_25)))). % 7.16/2.63 tff(c_54, plain, (![U_69, W_71, V_70]: (ssPv4(U_69) | ssPv4(W_71) | ~ssPv2(U_69) | ~ssRr(U_69, W_71) | ~ssPv2(V_70) | ~ssRr(U_69, V_70)))). % 7.16/2.63 tff(c_268, plain, (![U_209]: (ssPv1(skf1(U_209)) | ~ssPv2(skf1(U_209)) | ssPv2(U_209) | ssPv3(skf1(U_209)) | ~ssPv3(U_209)))). % 7.16/2.63 tff(c_285, plain, (![U_1, V_215]: (ssPv3(U_1) | ~ssPv4(U_1) | ~ssPv3(skf1(U_1)) | ~ssPv4(V_215) | ~ssRr(U_1, V_215)))). % 7.16/2.63 tff(c_72, plain, (![U_96, W_98, V_97]: (ssPv3(U_96) | ~ssPv4(U_96) | ~ssPv3(W_98) | ~ssRr(U_96, W_98) | ~ssPv4(V_97) | ~ssRr(U_96, V_97)))). % 7.16/2.63 tff(c_257, plain, (![U_1]: (ssPv2(U_1) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv3(U_1)))). % 7.16/2.63 tff(c_253, plain, (![U_1, V_206]: (ssPv2(U_1) | ssPv3(skf1(U_1)) | ssPv4(V_206) | ~ssPv3(U_1) | ~ssRr(U_1, V_206)))). % 7.16/2.63 tff(c_30, plain, (![U_33, W_35, V_34]: (ssPv2(U_33) | ssPv3(W_35) | ssPv4(V_34) | ~ssPv3(U_33) | ~ssRr(U_33, W_35) | ~ssRr(U_33, V_34)))). % 7.16/2.63 tff(c_236, plain, (![U_1]: (ssPv4(U_1) | ssPv2(U_1) | ssPv1(skf1(U_1)) | ssPv4(skf1(U_1))))). % 7.16/2.63 tff(c_228, plain, (![U_1, V_198]: (ssPv4(U_1) | ssPv2(U_1) | ssPv1(skf1(U_1)) | ssPv4(V_198) | ~ssRr(U_1, V_198)))). % 7.16/2.63 tff(c_176, plain, (![U_1, V_188]: (ssPv1(U_1) | ssPv1(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv1(V_188) | ~ssRr(U_1, V_188)))). % 7.16/2.63 tff(c_22, plain, (![U_21, W_23, V_22]: (ssPv4(U_21) | ssPv2(U_21) | ssPv1(W_23) | ssPv4(V_22) | ~ssRr(U_21, W_23) | ~ssRr(U_21, V_22)))). % 7.16/2.63 tff(c_172, plain, (![U_1, V_185]: (ssPv4(U_1) | ssPv1(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv3(V_185) | ~ssRr(U_1, V_185)))). % 7.16/2.63 tff(c_62, plain, (![U_81, W_83, V_82]: (ssPv1(U_81) | ssPv1(W_83) | ~ssPv3(U_81) | ~ssRr(U_81, W_83) | ~ssPv1(V_82) | ~ssRr(U_81, V_82)))). % 7.16/2.63 tff(c_64, plain, (![U_84, W_86, V_85]: (ssPv4(U_84) | ssPv1(U_84) | ~ssPv2(W_86) | ~ssRr(U_84, W_86) | ~ssPv3(V_85) | ~ssRr(U_84, V_85)))). % 7.16/2.63 tff(c_162, plain, (![U_1]: (ssPv2(U_1) | ssPv3(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv3(U_1)))). % 7.16/2.63 tff(c_156, plain, (![U_178]: (ssPv1(U_178) | ssPv3(U_178) | ~ssPv4(U_178) | ~ssPv2(U_178)))). % 7.16/2.63 tff(c_14, plain, (![U_12, V_13]: (ssPv2(U_12) | ssPv3(V_13) | ~ssPv4(U_12) | ~ssPv3(U_12) | ~ssRr(U_12, V_13)))). % 7.16/2.63 tff(c_148, plain, (![U_1]: (ssPv3(U_1) | ssPv4(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv2(U_1)))). % 7.16/2.63 tff(c_12, plain, (![U_10, V_11]: (ssPv3(U_10) | ssPv4(V_11) | ~ssPv4(U_10) | ~ssPv2(U_10) | ~ssRr(U_10, V_11)))). % 7.16/2.63 tff(c_132, plain, (![U_1]: (ssPv3(U_1) | ssPv1(U_1) | ~ssPv2(U_1) | ~ssPv4(skf1(U_1))))). % 7.16/2.63 tff(c_18, plain, (![U_16, V_17]: (ssPv3(U_16) | ssPv1(U_16) | ~ssPv2(U_16) | ~ssPv4(V_17) | ~ssRr(U_16, V_17)))). % 7.16/2.63 tff(c_126, plain, (![U_1]: (ssPv2(U_1) | ssPv1(U_1) | ssPv3(skf1(U_1)) | ~ssPv3(U_1)))). % 7.16/2.63 tff(c_8, plain, (![U_6, V_7]: (ssPv2(U_6) | ssPv1(U_6) | ssPv3(V_7) | ~ssPv3(U_6) | ~ssRr(U_6, V_7)))). % 7.16/2.63 tff(c_120, plain, (![U_1]: (ssPv3(U_1) | ssPv2(U_1) | ssPv1(U_1) | ~ssPv4(skf1(U_1))))). % 7.16/2.63 tff(c_10, plain, (![U_8, V_9]: (ssPv3(U_8) | ssPv2(U_8) | ssPv1(U_8) | ~ssPv4(V_9) | ~ssRr(U_8, V_9)))). % 7.16/2.63 tff(c_114, plain, (![U_1]: (ssPv4(U_1) | ssPv3(U_1) | ssPv2(U_1) | ssPv3(skf1(U_1))))). % 7.16/2.63 tff(c_4, plain, (![U_2, V_3]: (ssPv4(U_2) | ssPv3(U_2) | ssPv2(U_2) | ssPv3(V_3) | ~ssRr(U_2, V_3)))). % 7.16/2.63 tff(c_108, plain, (![U_1]: (ssPv4(U_1) | ssPv2(U_1) | ~ssPv1(U_1) | ~ssPv2(skf1(U_1))))). % 7.16/2.63 tff(c_16, plain, (![U_14, V_15]: (ssPv4(U_14) | ssPv2(U_14) | ~ssPv1(U_14) | ~ssPv2(V_15) | ~ssRr(U_14, V_15)))). % 7.16/2.63 tff(c_2, plain, (![U_1]: (ssRr(U_1, skf1(U_1))))). % 7.16/2.63 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 7.16/2.63 %------------------------------------------------------------------------------