%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN524-1 : TPTP v9.0.0. Released v2.1.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 : n009.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:03:48 PM UTC 2025 % Result : Satisfiable 5.10s 2.06s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SYN524-1 : TPTP v9.0.0. Released v2.1.0. % 0.12/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.12/0.34 % Computer : n009.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Wed Apr 9 07:55:11 EDT 2025 % 0.12/0.34 % CPUTime : % 5.10/2.06 % 5.10/2.06 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.10/2.07 % 5.10/2.07 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.10/2.07 %$ c5_2 > c4_2 > c3_2 > c2_2 > c1_2 > ssSkP1 > ssSkP0 > ndr1_1 > c5_1 > c4_1 > c3_1 > c2_1 > c1_1 > #nlpp > ssSkC4 > ssSkC3 > ssSkC2 > ssSkC1 > ssSkC0 > ndr1_0 > c5_0 > c4_0 > c3_0 > c2_0 > c1_0 > a187 > a186 > a185 > a184 > a183 > a182 > a181 > a180 > a179 > a178 > a177 > a176 > a175 > a174 > a173 > a172 > a171 > a170 > a169 > a168 > a167 > a166 > a165 > a164 > a163 > a162 > a161 > a160 > a159 > a158 > a157 % 5.10/2.07 % 5.10/2.07 %Foreground sorts: % 5.10/2.07 % 5.10/2.07 % 5.10/2.07 %Background operators: % 5.10/2.07 % 5.10/2.07 % 5.10/2.07 %Foreground operators: % 5.10/2.07 tff(a178, type, a178: $i). % 5.10/2.07 tff(a169, type, a169: $i). % 5.10/2.07 tff(c4_0, type, c4_0: $o). % 5.10/2.07 tff(ssSkP0, type, ssSkP0: $i > $o). % 5.10/2.07 tff(a167, type, a167: $i). % 5.10/2.07 tff(c3_0, type, c3_0: $o). % 5.10/2.07 tff(c1_2, type, c1_2: ($i * $i) > $o). % 5.10/2.07 tff(ssSkC3, type, ssSkC3: $o). % 5.10/2.07 tff(a157, type, a157: $i). % 5.10/2.07 tff(a185, type, a185: $i). % 5.10/2.07 tff(a171, type, a171: $i). % 5.10/2.07 tff(a161, type, a161: $i). % 5.10/2.07 tff(a184, type, a184: $i). % 5.10/2.07 tff(a174, type, a174: $i). % 5.10/2.07 tff(a166, type, a166: $i). % 5.10/2.07 tff(a176, type, a176: $i). % 5.10/2.07 tff(a183, type, a183: $i). % 5.10/2.07 tff(a165, type, a165: $i). % 5.10/2.07 tff(ssSkC4, type, ssSkC4: $o). % 5.10/2.07 tff(a179, type, a179: $i). % 5.10/2.07 tff(c5_0, type, c5_0: $o). % 5.10/2.07 tff(a180, type, a180: $i). % 5.10/2.07 tff(a173, type, a173: $i). % 5.10/2.07 tff(a163, type, a163: $i). % 5.10/2.07 tff(a187, type, a187: $i). % 5.10/2.07 tff(a160, type, a160: $i). % 5.10/2.07 tff(c1_0, type, c1_0: $o). % 5.10/2.07 tff(a172, type, a172: $i). % 5.10/2.07 tff(c2_1, type, c2_1: $i > $o). % 5.10/2.07 tff(ndr1_1, type, ndr1_1: $i > $o). % 5.10/2.07 tff(c2_0, type, c2_0: $o). % 5.10/2.07 tff(c4_1, type, c4_1: $i > $o). % 5.10/2.07 tff(a159, type, a159: $i). % 5.10/2.07 tff(a186, type, a186: $i). % 5.10/2.07 tff(a158, type, a158: $i). % 5.10/2.07 tff(a175, type, a175: $i). % 5.10/2.07 tff(ndr1_0, type, ndr1_0: $o). % 5.10/2.07 tff(a177, type, a177: $i). % 5.10/2.07 tff(a182, type, a182: $i). % 5.10/2.07 tff(c1_1, type, c1_1: $i > $o). % 5.10/2.07 tff(a170, type, a170: $i). % 5.10/2.07 tff(ssSkC2, type, ssSkC2: $o). % 5.10/2.07 tff(c5_2, type, c5_2: ($i * $i) > $o). % 5.10/2.07 tff(c4_2, type, c4_2: ($i * $i) > $o). % 5.10/2.07 tff(ssSkC1, type, ssSkC1: $o). % 5.10/2.07 tff(ssSkC0, type, ssSkC0: $o). % 5.10/2.07 tff(ssSkP1, type, ssSkP1: $i > $o). % 5.10/2.07 tff(a164, type, a164: $i). % 5.10/2.07 tff(c5_1, type, c5_1: $i > $o). % 5.10/2.07 tff(c3_2, type, c3_2: ($i * $i) > $o). % 5.10/2.07 tff(c2_2, type, c2_2: ($i * $i) > $o). % 5.10/2.07 tff(a181, type, a181: $i). % 5.10/2.07 tff(a162, type, a162: $i). % 5.10/2.07 tff(a168, type, a168: $i). % 5.10/2.07 tff(c3_1, type, c3_1: $i > $o). % 5.10/2.07 % 5.10/2.07 %Saturated clause set: % 5.10/2.07 tff(c_414, plain, (![U_79, V_80]: (~c4_1(U_79) | ~c1_1(U_79) | ~ndr1_1(U_79) | ~c1_2(U_79, V_80) | ~c3_2(U_79, V_80) | ~c4_2(U_79, V_80)))). % 5.10/2.07 tff(c_382, plain, (~ssSkC1)). % 5.10/2.08 tff(c_364, plain, (![U_42, V_43]: (c5_2(U_42, V_43) | c1_2(U_42, V_43) | ~c5_1(U_42) | ~c3_2(U_42, a157) | ~ndr1_1(U_42)))). % 5.10/2.08 tff(c_354, plain, (![U_34, V_35]: (c2_2(U_34, a157) | c5_2(U_34, V_35) | c1_2(U_34, V_35) | ~c5_1(U_34) | ~ndr1_1(U_34)))). % 5.10/2.08 tff(c_347, plain, (![V_33]: (c4_1(V_33) | ~c2_1(V_33) | ~c5_1(V_33)))). % 5.10/2.08 tff(c_326, plain, (~c3_1(a181))). % 5.10/2.08 tff(c_322, plain, (~ndr1_1(a181))). % 5.10/2.08 tff(c_318, plain, (![U_21]: (c5_2(a169, U_21) | c3_2(a169, U_21) | c2_2(a169, U_21)))). % 5.10/2.08 tff(c_319, plain, (ndr1_1(a169))). % 5.10/2.08 tff(c_302, plain, (ssSkP1(a183))). % 5.10/2.08 tff(c_298, plain, (c2_2(a183, a185))). % 5.10/2.08 tff(c_297, plain, (~c2_0)). % 5.10/2.08 tff(c_288, plain, (![U_13]: (c2_2(a183, U_13) | c3_2(a183, U_13)))). % 5.10/2.08 tff(c_278, plain, (![U_10]: (c4_2(U_10, a186) | ~c3_1(U_10) | ~ssSkP1(U_10)))). % 5.10/2.08 tff(c_274, plain, (![U_14]: (~c3_1(U_14) | ~c1_2(U_14, a186) | ~ssSkP1(U_14)))). % 5.10/2.08 tff(c_271, plain, (ssSkC4)). % 5.10/2.08 tff(c_262, plain, (![U_1]: (~c3_1(U_1) | ndr1_1(U_1)))). % 5.10/2.08 tff(c_248, plain, (~c1_0)). % 5.10/2.08 tff(c_244, plain, (~c5_2(a183, a184))). % 5.10/2.08 tff(c_88, plain, (![U_6]: (ssSkP0(U_6) | ~c4_2(U_6, a176)))). % 5.10/2.08 tff(c_84, plain, (![U_4]: (ssSkP1(U_4) | ~c2_2(U_4, a185)))). % 5.10/2.08 tff(c_54, plain, (![U_3]: (ssSkP0(U_3) | c2_2(U_3, a176)))). % 5.10/2.08 tff(c_86, plain, (![U_5]: (ssSkP1(U_5) | ~c3_2(U_5, a185)))). % 5.10/2.08 tff(c_238, plain, (c1_2(a183, a184))). % 5.10/2.08 tff(c_236, plain, (c2_1(a183))). % 5.10/2.08 tff(c_234, plain, (c5_2(a161, a162))). % 5.10/2.08 tff(c_233, plain, (~ssSkC2)). % 5.10/2.08 tff(c_22, plain, (![U_2]: (ssSkP0(U_2) | ndr1_1(U_2)))). % 5.10/2.08 tff(c_231, plain, (c3_2(a161, a162))). % 5.10/2.08 tff(c_230, plain, (ndr1_1(a183))). % 5.10/2.08 tff(c_228, plain, (c1_1(a181))). % 5.53/2.08 tff(c_226, plain, (c1_2(a161, a162))). % 5.53/2.08 tff(c_225, plain, (~ssSkC0)). % 5.53/2.08 tff(c_20, plain, (![U_1]: (ssSkP1(U_1) | ndr1_1(U_1)))). % 5.53/2.08 tff(c_223, plain, (~c4_1(a181))). % 5.53/2.08 tff(c_221, plain, (~c3_1(a170))). % 5.53/2.08 tff(c_220, plain, (ndr1_1(a161))). % 5.53/2.08 tff(c_218, plain, (~c4_0)). % 5.53/2.08 tff(c_216, plain, (c3_1(a169))). % 5.53/2.08 tff(c_215, plain, (c4_1(a161))). % 5.53/2.08 tff(c_212, plain, (~c1_1(a170))). % 5.53/2.08 tff(c_211, plain, (~c3_1(a161))). % 5.53/2.08 tff(c_205, plain, (ndr1_0)). % 5.53/2.08 tff(c_204, plain, (~c3_0)). % 5.53/2.08 tff(c_203, plain, (~c5_0)). % 5.53/2.08 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 5.53/2.08 %------------------------------------------------------------------------------