%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN744-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 : n002.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.06s 2.18s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN744-1 : TPTP v9.0.0. Released v2.5.0. % 0.07/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.13/0.34 % Computer : n002.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Apr 9 08:14:33 EDT 2025 % 0.13/0.34 % CPUTime : % 5.06/2.18 % 5.06/2.18 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.06/2.19 % 5.06/2.19 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.06/2.19 %$ ssRr > ssPv8 > ssPv7 > ssPv6 > ssPv5 > ssPv4 > ssPv3 > ssPv2 > ssPv1 > #nlpp > skf1 % 5.06/2.19 % 5.06/2.19 %Foreground sorts: % 5.06/2.19 % 5.06/2.19 % 5.06/2.19 %Background operators: % 5.06/2.19 % 5.06/2.19 % 5.06/2.19 %Foreground operators: % 5.06/2.19 tff(skf1, type, skf1: $i > $i). % 5.06/2.19 tff(ssPv1, type, ssPv1: $i > $o). % 5.06/2.19 tff(ssPv3, type, ssPv3: $i > $o). % 5.06/2.19 tff(ssPv7, type, ssPv7: $i > $o). % 5.06/2.19 tff(ssPv6, type, ssPv6: $i > $o). % 5.06/2.19 tff(ssPv5, type, ssPv5: $i > $o). % 5.06/2.19 tff(ssRr, type, ssRr: ($i * $i) > $o). % 5.06/2.19 tff(ssPv4, type, ssPv4: $i > $o). % 5.06/2.19 tff(ssPv2, type, ssPv2: $i > $o). % 5.06/2.19 tff(ssPv8, type, ssPv8: $i > $o). % 5.06/2.19 % 5.06/2.19 %Saturated clause set: % 5.06/2.19 tff(c_672, plain, (![U_1]: (~ssPv5(U_1) | ssPv2(skf1(U_1)) | ~ssPv1(U_1) | ssPv4(U_1) | ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv7(U_1)))). % 5.06/2.19 tff(c_483, plain, (![U_298]: (ssPv1(U_298) | ssPv2(skf1(U_298)) | ~ssPv1(skf1(U_298)) | ssPv4(U_298) | ~ssPv5(U_298) | ssPv6(U_298) | ssPv3(skf1(U_298)) | ~ssPv7(U_298)))). % 5.06/2.19 tff(c_605, plain, (![U_326]: (~ssPv6(U_326) | ~ssPv2(U_326) | ssPv2(skf1(U_326)) | ~ssPv1(U_326) | ssPv4(U_326) | ssPv3(skf1(U_326)) | ssPv4(skf1(U_326)) | ~ssPv7(U_326)))). % 5.06/2.19 tff(c_631, plain, (![U_1]: (ssPv6(U_1) | ~ssPv6(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv8(U_1) | ssPv1(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv1(U_1)))). % 5.06/2.20 tff(c_357, plain, (![U_255, V_171]: (ssPv6(U_255) | ~ssPv6(V_171) | ~ssRr(U_255, V_171) | ssPv2(skf1(U_255)) | ~ssPv8(U_255) | ssPv1(skf1(U_255)) | ~ssPv4(U_255) | ~ssPv1(U_255)))). % 5.06/2.20 tff(c_517, plain, (![U_310]: (ssPv3(U_310) | ssPv1(skf1(U_310)) | ~ssPv4(U_310) | ssPv5(U_310) | ssPv2(skf1(U_310)) | ~ssPv6(U_310) | ssPv3(skf1(U_310)) | ~ssPv7(U_310)))). % 5.06/2.20 tff(c_610, plain, (![U_1]: (ssPv6(U_1) | ~ssPv4(U_1) | ~ssPv6(skf1(U_1)) | ssPv2(skf1(U_1)) | ~ssPv8(U_1) | ssPv3(skf1(U_1)) | ~ssPv7(U_1)))). % 5.06/2.20 tff(c_472, plain, (![U_297, V_171]: (ssPv6(U_297) | ~ssPv4(U_297) | ~ssPv6(V_171) | ~ssRr(U_297, V_171) | ssPv2(skf1(U_297)) | ~ssPv8(U_297) | ssPv3(skf1(U_297)) | ~ssPv7(U_297)))). % 5.06/2.20 tff(c_534, plain, (![U_312]: (ssPv2(skf1(U_312)) | ~ssPv1(U_312) | ssPv4(U_312) | ssPv6(skf1(U_312)) | ssPv3(skf1(U_312)) | ssPv4(skf1(U_312)) | ~ssPv7(U_312)))). % 5.06/2.20 tff(c_585, plain, (![U_1]: (ssPv6(U_1) | ~ssPv4(U_1) | ~ssPv6(skf1(U_1)) | ssPv2(U_1) | ~ssPv8(U_1) | ssPv3(skf1(U_1)) | ~ssPv7(U_1)))). % 5.06/2.20 tff(c_460, plain, (![U_296, V_171]: (ssPv6(U_296) | ~ssPv4(U_296) | ~ssPv6(V_171) | ~ssRr(U_296, V_171) | ssPv2(U_296) | ~ssPv8(U_296) | ssPv3(skf1(U_296)) | ~ssPv7(U_296)))). % 5.06/2.20 tff(c_580, plain, (![U_1]: (~ssPv3(U_1) | ssPv5(U_1) | ~ssPv6(U_1) | ssPv2(U_1) | ~ssPv8(U_1) | ssPv1(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv1(U_1)))). % 5.06/2.20 tff(c_559, plain, (![U_1]: (~ssPv3(U_1) | ~ssPv3(skf1(U_1)) | ssPv5(U_1) | ~ssPv6(U_1) | ssPv1(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv1(U_1)))). % 5.06/2.20 tff(c_505, plain, (![U_1, V_309]: (~ssPv3(U_1) | ~ssPv3(V_309) | ~ssRr(U_1, V_309) | ssPv5(U_1) | ~ssPv6(U_1) | ssPv1(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv1(U_1)))). % 5.06/2.20 tff(c_550, plain, (![U_1]: (ssPv3(U_1) | ~ssPv5(skf1(U_1)) | ssPv5(U_1) | ~ssPv6(U_1) | ssPv1(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv1(U_1)))). % 5.06/2.20 tff(c_233, plain, (![U_184, V_143]: (ssPv3(U_184) | ~ssPv5(V_143) | ~ssRr(U_184, V_143) | ssPv5(U_184) | ~ssPv6(U_184) | ssPv1(skf1(U_184)) | ~ssPv4(U_184) | ~ssPv1(U_184)))). % 5.06/2.20 tff(c_473, plain, (![U_297]: (ssPv3(U_297) | ssPv1(skf1(U_297)) | ~ssPv4(U_297) | ssPv2(skf1(U_297)) | ~ssPv8(U_297) | ssPv3(skf1(U_297)) | ~ssPv7(U_297)))). % 5.06/2.20 tff(c_515, plain, (![U_310]: (ssPv1(U_310) | ~ssPv1(skf1(U_310)) | ssPv5(U_310) | ssPv2(skf1(U_310)) | ~ssPv6(U_310) | ssPv3(skf1(U_310)) | ~ssPv7(U_310)))). % 5.06/2.20 tff(c_461, plain, (![U_296]: (ssPv3(U_296) | ssPv1(skf1(U_296)) | ~ssPv4(U_296) | ssPv2(U_296) | ~ssPv8(U_296) | ssPv3(skf1(U_296)) | ~ssPv7(U_296)))). % 5.06/2.20 tff(c_443, plain, (![U_291]: (ssPv4(U_291) | ssPv6(skf1(U_291)) | ssPv7(skf1(U_291)) | ssPv3(skf1(U_291)) | ssPv4(skf1(U_291)) | ~ssPv7(U_291)))). % 5.06/2.20 tff(c_471, plain, (![U_297]: (ssPv1(U_297) | ~ssPv1(skf1(U_297)) | ssPv2(skf1(U_297)) | ~ssPv8(U_297) | ssPv3(skf1(U_297)) | ~ssPv7(U_297)))). % 5.06/2.20 tff(c_445, plain, (![U_291]: (ssPv5(U_291) | ssPv2(skf1(U_291)) | ~ssPv6(U_291) | ssPv3(skf1(U_291)) | ssPv4(skf1(U_291)) | ~ssPv7(U_291)))). % 5.06/2.20 tff(c_497, plain, (![U_1, V_306]: (ssPv1(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv3(V_306) | ~ssRr(U_1, V_306)))). % 5.06/2.20 tff(c_493, plain, (![U_1]: (ssPv2(skf1(U_1)) | ~ssPv8(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv7(skf1(U_1))))). % 5.06/2.20 tff(c_416, plain, (![U_1, W_284, V_285]: (ssPv1(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv2(W_284) | ~ssRr(U_1, W_284) | ~ssPv3(V_285) | ~ssRr(U_1, V_285)))). % 5.06/2.20 tff(c_489, plain, (![U_1, V_301]: (ssPv2(skf1(U_1)) | ~ssPv8(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv7(V_301) | ~ssRr(U_1, V_301)))). % 5.06/2.20 tff(c_449, plain, (![U_1, W_294, V_295]: (ssPv2(skf1(U_1)) | ~ssPv8(U_1) | ~ssPv1(W_294) | ~ssRr(U_1, W_294) | ~ssPv7(V_295) | ~ssRr(U_1, V_295)))). % 5.06/2.20 tff(c_442, plain, (![U_291]: (ssPv4(U_291) | ~ssPv5(U_291) | ssPv6(U_291) | ssPv3(skf1(U_291)) | ssPv4(skf1(U_291)) | ~ssPv7(U_291)))). % 5.06/2.20 tff(c_441, plain, (![U_291]: (ssPv2(skf1(U_291)) | ~ssPv8(U_291) | ssPv3(skf1(U_291)) | ssPv4(skf1(U_291)) | ~ssPv7(U_291)))). % 5.06/2.20 tff(c_444, plain, (![U_291]: (ssPv2(U_291) | ~ssPv8(U_291) | ssPv3(skf1(U_291)) | ssPv4(skf1(U_291)) | ~ssPv7(U_291)))). % 5.06/2.20 tff(c_60, plain, (![X_93, U_90, W_92, V_91]: (ssPv2(X_93) | ~ssPv8(U_90) | ~ssRr(U_90, X_93) | ~ssPv1(W_92) | ~ssRr(U_90, W_92) | ~ssPv7(V_91) | ~ssRr(U_90, V_91)))). % 5.06/2.20 tff(c_424, plain, (![U_1]: (ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv8(skf1(U_1)) | ~ssPv7(U_1)))). % 5.06/2.20 tff(c_420, plain, (![U_1, V_288]: (ssPv3(skf1(U_1)) | ssPv4(skf1(U_1)) | ssPv8(V_288) | ~ssPv7(U_1) | ~ssRr(U_1, V_288)))). % 5.06/2.20 tff(c_412, plain, (![U_1, W_279, V_280]: (ssPv3(skf1(U_1)) | ssPv4(W_279) | ssPv8(V_280) | ~ssPv7(U_1) | ~ssRr(U_1, W_279) | ~ssRr(U_1, V_280)))). % 5.06/2.20 tff(c_62, plain, (![X_97, U_94, W_96, V_95]: (ssPv1(X_97) | ~ssPv3(U_94) | ~ssRr(U_94, X_97) | ~ssPv2(W_96) | ~ssRr(U_94, W_96) | ~ssPv3(V_95) | ~ssRr(U_94, V_95)))). % 5.06/2.20 tff(c_40, plain, (![X_53, W_52, V_51, U_50]: (ssPv3(X_53) | ssPv4(W_52) | ssPv8(V_51) | ~ssPv7(U_50) | ~ssRr(U_50, X_53) | ~ssRr(U_50, W_52) | ~ssRr(U_50, V_51)))). % 5.06/2.20 tff(c_403, plain, (![U_1]: (~ssPv5(skf1(U_1)) | ssPv3(U_1) | ~ssPv8(U_1) | ssPv1(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv1(U_1)))). % 5.06/2.20 tff(c_374, plain, (![V_143, U_256]: (~ssPv5(V_143) | ~ssRr(U_256, V_143) | ssPv3(U_256) | ~ssPv8(U_256) | ssPv1(skf1(U_256)) | ~ssPv4(U_256) | ~ssPv1(U_256)))). % 5.06/2.20 tff(c_377, plain, (![U_256]: (ssPv2(U_256) | ~ssPv7(U_256) | ssPv3(U_256) | ~ssPv8(U_256) | ssPv1(skf1(U_256)) | ~ssPv4(U_256) | ~ssPv1(U_256)))). % 5.06/2.20 tff(c_394, plain, (![U_1, W_269, V_270]: (ssPv1(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv1(W_269) | ~ssRr(U_1, W_269) | ~ssPv5(V_270) | ~ssRr(U_1, V_270)))). % 5.06/2.20 tff(c_58, plain, (![X_89, U_86, W_88, V_87]: (ssPv1(X_89) | ~ssPv4(U_86) | ~ssRr(U_86, X_89) | ~ssPv1(W_88) | ~ssRr(U_86, W_88) | ~ssPv5(V_87) | ~ssRr(U_86, V_87)))). % 5.06/2.20 tff(c_389, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv7(skf1(U_1))))). % 5.06/2.20 tff(c_385, plain, (![U_1, V_263]: (ssPv1(skf1(U_1)) | ssPv3(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv7(V_263) | ~ssRr(U_1, V_263)))). % 5.06/2.20 tff(c_381, plain, (![U_1, W_258, V_260]: (ssPv1(skf1(U_1)) | ssPv3(W_258) | ~ssPv4(U_1) | ~ssRr(U_1, W_258) | ~ssPv7(V_260) | ~ssRr(U_1, V_260)))). % 5.06/2.21 tff(c_44, plain, (![X_61, W_60, U_58, V_59]: (ssPv1(X_61) | ssPv3(W_60) | ~ssPv4(U_58) | ~ssRr(U_58, X_61) | ~ssRr(U_58, W_60) | ~ssPv7(V_59) | ~ssRr(U_58, V_59)))). % 5.06/2.21 tff(c_358, plain, (![U_255]: (ssPv3(U_255) | ssPv2(skf1(U_255)) | ~ssPv8(U_255) | ssPv1(skf1(U_255)) | ~ssPv4(U_255) | ~ssPv1(U_255)))). % 5.06/2.21 tff(c_321, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv8(U_1) | ssPv1(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv1(U_1)))). % 5.06/2.21 tff(c_341, plain, (![U_1]: (ssPv1(U_1) | ssPv2(skf1(U_1)) | ~ssPv1(skf1(U_1)) | ~ssPv4(skf1(U_1))))). % 5.06/2.21 tff(c_337, plain, (![U_1, V_251]: (ssPv1(U_1) | ssPv2(skf1(U_1)) | ~ssPv1(skf1(U_1)) | ~ssPv4(V_251) | ~ssRr(U_1, V_251)))). % 5.06/2.21 tff(c_333, plain, (![U_1, W_247, V_248]: (ssPv1(U_1) | ssPv2(skf1(U_1)) | ~ssPv1(W_247) | ~ssRr(U_1, W_247) | ~ssPv4(V_248) | ~ssRr(U_1, V_248)))). % 5.06/2.21 tff(c_52, plain, (![U_74, X_77, W_76, V_75]: (ssPv1(U_74) | ssPv2(X_77) | ~ssRr(U_74, X_77) | ~ssPv1(W_76) | ~ssRr(U_74, W_76) | ~ssPv4(V_75) | ~ssRr(U_74, V_75)))). % 5.06/2.21 tff(c_325, plain, (![U_1, V_242]: (ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(skf1(U_1)) | ~ssPv4(V_242) | ~ssRr(U_1, V_242)))). % 5.06/2.21 tff(c_316, plain, (![U_1, W_237, V_238]: (ssPv4(U_1) | ssPv1(skf1(U_1)) | ~ssPv2(W_237) | ~ssRr(U_1, W_237) | ~ssPv4(V_238) | ~ssRr(U_1, V_238)))). % 5.06/2.21 tff(c_312, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv8(U_1) | ~ssPv8(skf1(U_1))))). % 5.06/2.21 tff(c_50, plain, (![U_70, X_73, W_72, V_71]: (ssPv4(U_70) | ssPv1(X_73) | ~ssRr(U_70, X_73) | ~ssPv2(W_72) | ~ssRr(U_70, W_72) | ~ssPv4(V_71) | ~ssRr(U_70, V_71)))). % 5.06/2.21 tff(c_308, plain, (![U_1, V_232]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv8(U_1) | ~ssPv8(V_232) | ~ssRr(U_1, V_232)))). % 5.06/2.21 tff(c_295, plain, (![U_1, W_221, V_223]: (ssPv2(skf1(U_1)) | ssPv4(W_221) | ~ssPv8(U_1) | ~ssRr(U_1, W_221) | ~ssPv8(V_223) | ~ssRr(U_1, V_223)))). % 5.06/2.21 tff(c_303, plain, (![U_1]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv7(skf1(U_1))))). % 5.06/2.21 tff(c_299, plain, (![U_1, V_226]: (ssPv2(skf1(U_1)) | ssPv4(skf1(U_1)) | ~ssPv1(U_1) | ~ssPv7(V_226) | ~ssRr(U_1, V_226)))). % 5.06/2.21 tff(c_291, plain, (![U_1, W_217, V_219]: (ssPv2(skf1(U_1)) | ssPv4(W_217) | ~ssPv1(U_1) | ~ssRr(U_1, W_217) | ~ssPv7(V_219) | ~ssRr(U_1, V_219)))). % 5.06/2.21 tff(c_48, plain, (![X_69, W_68, U_66, V_67]: (ssPv2(X_69) | ssPv4(W_68) | ~ssPv8(U_66) | ~ssRr(U_66, X_69) | ~ssRr(U_66, W_68) | ~ssPv8(V_67) | ~ssRr(U_66, V_67)))). % 5.06/2.21 tff(c_46, plain, (![X_65, W_64, U_62, V_63]: (ssPv2(X_65) | ssPv4(W_64) | ~ssPv1(U_62) | ~ssRr(U_62, X_65) | ~ssRr(U_62, W_64) | ~ssPv7(V_63) | ~ssRr(U_62, V_63)))). % 5.06/2.21 tff(c_283, plain, (![U_1, V_213]: (ssPv5(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv1(skf1(U_1)) | ~ssPv5(V_213) | ~ssRr(U_1, V_213)))). % 5.06/2.21 tff(c_279, plain, (![U_1, W_209, V_210]: (ssPv5(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv1(W_209) | ~ssRr(U_1, W_209) | ~ssPv5(V_210) | ~ssRr(U_1, V_210)))). % 5.06/2.21 tff(c_56, plain, (![X_85, U_82, W_84, V_83]: (ssPv5(X_85) | ~ssPv5(U_82) | ~ssRr(U_82, X_85) | ~ssPv1(W_84) | ~ssRr(U_82, W_84) | ~ssPv5(V_83) | ~ssRr(U_82, V_83)))). % 5.06/2.21 tff(c_270, plain, (![U_1]: (ssPv4(U_1) | ~ssPv5(U_1) | ~ssPv8(skf1(U_1)) | ssPv6(U_1) | ssPv4(skf1(U_1)) | ~ssPv7(U_1)))). % 5.06/2.21 tff(c_220, plain, (![U_1, V_183]: (ssPv4(U_1) | ~ssPv5(U_1) | ~ssPv8(V_183) | ~ssRr(U_1, V_183) | ssPv6(U_1) | ssPv4(skf1(U_1)) | ~ssPv7(U_1)))). % 5.06/2.21 tff(c_261, plain, (![U_1]: (ssPv4(U_1) | ssPv6(skf1(U_1)) | ssPv7(skf1(U_1)) | ~ssPv8(skf1(U_1))))). % 5.06/2.21 tff(c_257, plain, (![U_1, V_200]: (ssPv4(U_1) | ssPv6(skf1(U_1)) | ssPv7(skf1(U_1)) | ~ssPv8(V_200) | ~ssRr(U_1, V_200)))). % 5.06/2.21 tff(c_253, plain, (![U_1, W_196, V_197]: (ssPv4(U_1) | ssPv6(skf1(U_1)) | ssPv7(W_196) | ~ssRr(U_1, W_196) | ~ssPv8(V_197) | ~ssRr(U_1, V_197)))). % 5.06/2.21 tff(c_42, plain, (![U_54, X_57, W_56, V_55]: (ssPv4(U_54) | ssPv6(X_57) | ssPv7(W_56) | ~ssRr(U_54, X_57) | ~ssRr(U_54, W_56) | ~ssPv8(V_55) | ~ssRr(U_54, V_55)))). % 5.06/2.21 tff(c_236, plain, (![U_184]: (ssPv2(U_184) | ~ssPv7(U_184) | ssPv5(U_184) | ~ssPv6(U_184) | ssPv1(skf1(U_184)) | ~ssPv4(U_184) | ~ssPv1(U_184)))). % 5.06/2.21 tff(c_240, plain, (![U_1, W_187, V_188]: (ssPv1(skf1(U_1)) | ~ssPv3(U_1) | ~ssPv1(W_187) | ~ssRr(U_1, W_187) | ~ssPv5(V_188) | ~ssRr(U_1, V_188)))). % 5.06/2.21 tff(c_196, plain, (![U_1]: (ssPv2(U_1) | ssPv3(skf1(U_1)) | ~ssPv8(U_1) | ssPv1(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv1(U_1)))). % 5.06/2.21 tff(c_54, plain, (![X_81, U_78, W_80, V_79]: (ssPv1(X_81) | ~ssPv3(U_78) | ~ssRr(U_78, X_81) | ~ssPv1(W_80) | ~ssRr(U_78, W_80) | ~ssPv5(V_79) | ~ssRr(U_78, V_79)))). % 5.06/2.21 tff(c_183, plain, (![U_1]: (ssPv5(U_1) | ssPv2(skf1(U_1)) | ~ssPv6(U_1) | ssPv1(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv1(U_1)))). % 5.06/2.21 tff(c_216, plain, (![U_1, V_181]: (ssPv4(U_1) | ~ssPv5(U_1) | ~ssPv6(skf1(U_1)) | ~ssPv8(V_181) | ~ssRr(U_1, V_181)))). % 5.06/2.21 tff(c_36, plain, (![U_44, W_46, V_45]: (ssPv4(U_44) | ~ssPv5(U_44) | ~ssPv6(W_46) | ~ssRr(U_44, W_46) | ~ssPv8(V_45) | ~ssRr(U_44, V_45)))). % 5.06/2.21 tff(c_204, plain, (![U_1, V_174]: (ssPv5(skf1(U_1)) | ~ssPv5(U_1) | ~ssPv1(U_1) | ~ssPv5(V_174) | ~ssRr(U_1, V_174)))). % 5.06/2.21 tff(c_200, plain, (![U_1, V_171]: (ssPv6(U_1) | ~ssPv4(U_1) | ~ssPv4(skf1(U_1)) | ~ssPv6(V_171) | ~ssRr(U_1, V_171)))). % 5.06/2.21 tff(c_32, plain, (![W_40, U_38, V_39]: (ssPv5(W_40) | ~ssPv5(U_38) | ~ssPv1(U_38) | ~ssRr(U_38, W_40) | ~ssPv5(V_39) | ~ssRr(U_38, V_39)))). % 5.06/2.21 tff(c_34, plain, (![U_41, W_43, V_42]: (ssPv6(U_41) | ~ssPv4(U_41) | ~ssPv4(W_43) | ~ssRr(U_41, W_43) | ~ssPv6(V_42) | ~ssRr(U_41, V_42)))). % 5.06/2.21 tff(c_191, plain, (![U_1]: (ssPv2(U_1) | ssPv3(skf1(U_1)) | ~ssPv8(U_1) | ~ssPv8(skf1(U_1))))). % 5.06/2.21 tff(c_187, plain, (![U_1, V_165]: (ssPv2(U_1) | ssPv3(skf1(U_1)) | ~ssPv8(U_1) | ~ssPv8(V_165) | ~ssRr(U_1, V_165)))). % 5.06/2.21 tff(c_28, plain, (![U_32, W_34, V_33]: (ssPv2(U_32) | ssPv3(W_34) | ~ssPv8(U_32) | ~ssRr(U_32, W_34) | ~ssPv8(V_33) | ~ssRr(U_32, V_33)))). % 5.06/2.21 tff(c_178, plain, (![U_1]: (ssPv5(U_1) | ssPv2(skf1(U_1)) | ~ssPv6(U_1) | ~ssPv8(skf1(U_1))))). % 5.06/2.21 tff(c_174, plain, (![U_1, V_159]: (ssPv5(U_1) | ssPv2(skf1(U_1)) | ~ssPv6(U_1) | ~ssPv8(V_159) | ~ssRr(U_1, V_159)))). % 5.06/2.21 tff(c_22, plain, (![U_23, W_25, V_24]: (ssPv5(U_23) | ssPv2(W_25) | ~ssPv6(U_23) | ~ssRr(U_23, W_25) | ~ssPv8(V_24) | ~ssRr(U_23, V_24)))). % 5.06/2.21 tff(c_164, plain, (![U_1, V_153]: (ssPv8(U_1) | ssPv4(U_1) | ~ssPv3(skf1(U_1)) | ~ssPv4(V_153) | ~ssRr(U_1, V_153)))). % 5.06/2.21 tff(c_160, plain, (![U_1]: (ssPv3(U_1) | ssPv1(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv4(skf1(U_1))))). % 5.06/2.21 tff(c_24, plain, (![U_26, W_28, V_27]: (ssPv8(U_26) | ssPv4(U_26) | ~ssPv3(W_28) | ~ssRr(U_26, W_28) | ~ssPv4(V_27) | ~ssRr(U_26, V_27)))). % 5.06/2.21 tff(c_156, plain, (![U_1, V_148]: (ssPv3(U_1) | ssPv1(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv4(V_148) | ~ssRr(U_1, V_148)))). % 5.06/2.21 tff(c_26, plain, (![U_29, W_31, V_30]: (ssPv3(U_29) | ssPv1(W_31) | ~ssPv4(U_29) | ~ssRr(U_29, W_31) | ~ssPv4(V_30) | ~ssRr(U_29, V_30)))). % 5.06/2.21 tff(c_151, plain, (![U_1, V_143]: (ssPv3(U_1) | ~ssPv4(U_1) | ~ssPv2(skf1(U_1)) | ~ssPv5(V_143) | ~ssRr(U_1, V_143)))). % 5.06/2.21 tff(c_38, plain, (![U_47, W_49, V_48]: (ssPv3(U_47) | ~ssPv4(U_47) | ~ssPv2(W_49) | ~ssRr(U_47, W_49) | ~ssPv5(V_48) | ~ssRr(U_47, V_48)))). % 5.06/2.21 tff(c_142, plain, (![U_1]: (ssPv2(skf1(U_1)) | ~ssPv6(U_1) | ~ssPv2(U_1) | ~ssPv6(skf1(U_1))))). % 5.06/2.21 tff(c_138, plain, (![U_1, V_137]: (ssPv2(skf1(U_1)) | ~ssPv6(U_1) | ~ssPv2(U_1) | ~ssPv6(V_137) | ~ssRr(U_1, V_137)))). % 5.06/2.21 tff(c_30, plain, (![W_37, U_35, V_36]: (ssPv2(W_37) | ~ssPv6(U_35) | ~ssPv2(U_35) | ~ssRr(U_35, W_37) | ~ssPv6(V_36) | ~ssRr(U_35, V_36)))). % 5.06/2.21 tff(c_133, plain, (![U_1]: (ssPv1(skf1(U_1)) | ssPv8(skf1(U_1)) | ~ssPv4(U_1) | ~ssPv1(U_1)))). % 5.06/2.21 tff(c_129, plain, (![U_1, V_130]: (ssPv1(skf1(U_1)) | ssPv8(V_130) | ~ssPv4(U_1) | ~ssPv1(U_1) | ~ssRr(U_1, V_130)))). % 5.06/2.21 tff(c_20, plain, (![W_22, V_21, U_20]: (ssPv1(W_22) | ssPv8(V_21) | ~ssPv4(U_20) | ~ssPv1(U_20) | ~ssRr(U_20, W_22) | ~ssRr(U_20, V_21)))). % 5.06/2.21 tff(c_124, plain, (![U_1]: (ssPv6(U_1) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv4(skf1(U_1))))). % 5.06/2.21 tff(c_115, plain, (![U_1, V_124]: (ssPv6(U_1) | ssPv4(U_1) | ssPv1(skf1(U_1)) | ssPv4(V_124) | ~ssRr(U_1, V_124)))). % 5.06/2.21 tff(c_111, plain, (![U_1]: (ssPv6(U_1) | ssPv4(skf1(U_1)) | ssPv6(skf1(U_1)) | ~ssPv7(U_1)))). % 5.06/2.21 tff(c_16, plain, (![U_14, W_16, V_15]: (ssPv6(U_14) | ssPv4(U_14) | ssPv1(W_16) | ssPv4(V_15) | ~ssRr(U_14, W_16) | ~ssRr(U_14, V_15)))). % 5.06/2.21 tff(c_107, plain, (![U_1, V_119]: (ssPv6(U_1) | ssPv4(skf1(U_1)) | ssPv6(V_119) | ~ssPv7(U_1) | ~ssRr(U_1, V_119)))). % 5.06/2.21 tff(c_18, plain, (![U_17, W_19, V_18]: (ssPv6(U_17) | ssPv4(W_19) | ssPv6(V_18) | ~ssPv7(U_17) | ~ssRr(U_17, W_19) | ~ssRr(U_17, V_18)))). % 5.06/2.21 tff(c_102, plain, (![U_1]: (ssPv7(U_1) | ssPv6(U_1) | ~ssPv3(U_1) | ~ssPv6(skf1(U_1))))). % 5.06/2.21 tff(c_6, plain, (![U_4, V_5]: (ssPv7(U_4) | ssPv6(U_4) | ~ssPv3(U_4) | ~ssPv6(V_5) | ~ssRr(U_4, V_5)))). % 5.06/2.21 tff(c_96, plain, (![U_1]: (ssPv8(U_1) | ssPv1(U_1) | ~ssPv4(U_1) | ~ssPv2(skf1(U_1))))). % 5.06/2.21 tff(c_10, plain, (![U_8, V_9]: (ssPv8(U_8) | ssPv1(U_8) | ~ssPv4(U_8) | ~ssPv2(V_9) | ~ssRr(U_8, V_9)))). % 5.06/2.21 tff(c_90, plain, (![U_1]: (ssPv7(U_1) | ssPv1(U_1) | ~ssPv5(U_1) | ~ssPv2(skf1(U_1))))). % 5.06/2.21 tff(c_12, plain, (![U_10, V_11]: (ssPv7(U_10) | ssPv1(U_10) | ~ssPv5(U_10) | ~ssPv2(V_11) | ~ssRr(U_10, V_11)))). % 5.06/2.21 tff(c_84, plain, (![U_1]: (ssPv2(U_1) | ~ssPv7(U_1) | ~ssPv4(U_1) | ~ssPv2(skf1(U_1))))). % 5.06/2.21 tff(c_14, plain, (![U_12, V_13]: (ssPv2(U_12) | ~ssPv7(U_12) | ~ssPv4(U_12) | ~ssPv2(V_13) | ~ssRr(U_12, V_13)))). % 5.06/2.21 tff(c_74, plain, (![U_1]: (ssPv4(U_1) | ssPv5(skf1(U_1)) | ~ssPv8(U_1) | ~ssPv6(U_1)))). % 5.06/2.22 tff(c_8, plain, (![U_6, V_7]: (ssPv4(U_6) | ssPv5(V_7) | ~ssPv8(U_6) | ~ssPv6(U_6) | ~ssRr(U_6, V_7)))). % 5.06/2.22 tff(c_68, plain, (![U_1]: (ssPv8(U_1) | ssPv7(U_1) | ~ssPv3(U_1) | ~ssPv5(skf1(U_1))))). % 5.06/2.22 tff(c_4, plain, (![U_2, V_3]: (ssPv8(U_2) | ssPv7(U_2) | ~ssPv3(U_2) | ~ssPv5(V_3) | ~ssRr(U_2, V_3)))). % 5.39/2.22 tff(c_2, plain, (![U_1]: (ssRr(U_1, skf1(U_1))))). % 5.39/2.22 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.39/2.22 %------------------------------------------------------------------------------