%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN535-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/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 : n006.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:50 PM UTC 2025 % Result : Satisfiable 5.27s 2.13s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SYN535-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/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.34 % Computer : n006.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 07:57:07 EDT 2025 % 0.13/0.35 % CPUTime : % 5.27/2.13 % 5.27/2.13 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.27/2.13 % 5.27/2.13 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.27/2.14 %$ c5_2 > c4_2 > c3_2 > c2_2 > c1_2 > ndr1_1 > c5_1 > c4_1 > c3_1 > c2_1 > c1_1 > #nlpp > ssSkC8 > ssSkC7 > ssSkC6 > ssSkC5 > ssSkC4 > ssSkC3 > ssSkC2 > ssSkC1 > ssSkC0 > ndr1_0 > c5_0 > c4_0 > c3_0 > c2_0 > c1_0 > a519 > a518 > a517 > a516 > a515 > a514 > a513 > a512 > a511 > a510 > a509 > a508 > a507 > a506 > a505 > a504 > a503 > a502 > a501 > a500 > a499 > a498 > a497 > a496 > a495 > a494 > a493 > a492 % 5.27/2.14 % 5.27/2.14 %Foreground sorts: % 5.27/2.14 % 5.27/2.14 % 5.27/2.14 %Background operators: % 5.27/2.14 % 5.27/2.14 % 5.27/2.14 %Foreground operators: % 5.27/2.14 tff(a492, type, a492: $i). % 5.27/2.14 tff(ssSkC8, type, ssSkC8: $o). % 5.27/2.14 tff(ssSkC7, type, ssSkC7: $o). % 5.27/2.14 tff(a506, type, a506: $i). % 5.27/2.14 tff(c4_0, type, c4_0: $o). % 5.27/2.14 tff(ssSkC6, type, ssSkC6: $o). % 5.27/2.14 tff(c3_0, type, c3_0: $o). % 5.27/2.14 tff(c1_2, type, c1_2: ($i * $i) > $o). % 5.27/2.14 tff(ssSkC3, type, ssSkC3: $o). % 5.27/2.14 tff(a503, type, a503: $i). % 5.27/2.14 tff(a495, type, a495: $i). % 5.27/2.14 tff(a502, type, a502: $i). % 5.27/2.14 tff(a493, type, a493: $i). % 5.27/2.14 tff(a511, type, a511: $i). % 5.27/2.14 tff(a508, type, a508: $i). % 5.27/2.14 tff(a510, type, a510: $i). % 5.27/2.14 tff(a498, type, a498: $i). % 5.27/2.14 tff(ssSkC4, type, ssSkC4: $o). % 5.27/2.14 tff(a505, type, a505: $i). % 5.27/2.14 tff(a504, type, a504: $i). % 5.27/2.14 tff(c5_0, type, c5_0: $o). % 5.27/2.14 tff(a518, type, a518: $i). % 5.27/2.14 tff(a499, type, a499: $i). % 5.27/2.14 tff(a500, type, a500: $i). % 5.27/2.14 tff(a516, type, a516: $i). % 5.27/2.14 tff(a509, type, a509: $i). % 5.27/2.14 tff(c1_0, type, c1_0: $o). % 5.27/2.14 tff(c2_1, type, c2_1: $i > $o). % 5.27/2.14 tff(ndr1_1, type, ndr1_1: $i > $o). % 5.27/2.14 tff(c2_0, type, c2_0: $o). % 5.27/2.14 tff(c4_1, type, c4_1: $i > $o). % 5.27/2.14 tff(a494, type, a494: $i). % 5.27/2.14 tff(a507, type, a507: $i). % 5.27/2.14 tff(ndr1_0, type, ndr1_0: $o). % 5.27/2.14 tff(a501, type, a501: $i). % 5.27/2.14 tff(c1_1, type, c1_1: $i > $o). % 5.27/2.14 tff(a497, type, a497: $i). % 5.27/2.14 tff(ssSkC2, type, ssSkC2: $o). % 5.27/2.14 tff(c5_2, type, c5_2: ($i * $i) > $o). % 5.27/2.14 tff(a496, type, a496: $i). % 5.27/2.14 tff(a519, type, a519: $i). % 5.27/2.14 tff(c4_2, type, c4_2: ($i * $i) > $o). % 5.27/2.14 tff(a517, type, a517: $i). % 5.27/2.14 tff(ssSkC1, type, ssSkC1: $o). % 5.27/2.14 tff(ssSkC0, type, ssSkC0: $o). % 5.27/2.14 tff(a515, type, a515: $i). % 5.27/2.14 tff(ssSkC5, type, ssSkC5: $o). % 5.27/2.14 tff(c5_1, type, c5_1: $i > $o). % 5.27/2.14 tff(c3_2, type, c3_2: ($i * $i) > $o). % 5.27/2.14 tff(a514, type, a514: $i). % 5.27/2.14 tff(c2_2, type, c2_2: ($i * $i) > $o). % 5.27/2.14 tff(a513, type, a513: $i). % 5.27/2.14 tff(a512, type, a512: $i). % 5.27/2.14 tff(c3_1, type, c3_1: $i > $o). % 5.27/2.14 % 5.27/2.14 %Saturated clause set: % 5.27/2.14 tff(c_450, plain, (~c1_1(a507))). % 5.27/2.14 tff(c_449, plain, (~c1_1(a500))). % 5.27/2.14 tff(c_446, plain, (c2_1(a513))). % 5.27/2.14 tff(c_427, plain, (![U_47]: (c2_1(U_47) | ~c1_1(U_47) | ~c3_1(U_47)))). % 5.27/2.14 tff(c_421, plain, (~ssSkC5)). % 5.27/2.14 tff(c_416, plain, (c3_1(a495))). % 5.27/2.14 tff(c_409, plain, (~c3_2(a495, a497))). % 5.27/2.14 tff(c_396, plain, (![U_20, V_21]: (c3_1(U_20) | c5_2(U_20, a497) | c1_2(U_20, V_21) | c2_2(U_20, V_21) | ~ndr1_1(U_20)))). % 5.27/2.14 tff(c_393, plain, (c1_2(a503, a504))). % 5.27/2.14 tff(c_392, plain, (c1_2(a492, a493))). % 5.27/2.14 tff(c_383, plain, (c1_2(a503, a505))). % 5.27/2.14 tff(c_386, plain, (![U_24, V_25]: (c3_1(U_24) | c3_2(U_24, a497) | c1_2(U_24, V_25) | c2_2(U_24, V_25) | ~ndr1_1(U_24)))). % 5.27/2.14 tff(c_357, plain, (![U_22, V_23]: (c3_1(U_22) | c1_2(U_22, a497) | c1_2(U_22, V_23) | c2_2(U_22, V_23) | ~ndr1_1(U_22)))). % 5.27/2.14 tff(c_352, plain, (~c5_1(a511))). % 5.27/2.14 tff(c_351, plain, (~c5_1(a509))). % 5.27/2.14 tff(c_346, plain, (~ndr1_1(a511))). % 5.27/2.14 tff(c_340, plain, (~ndr1_1(a509))). % 5.27/2.14 tff(c_339, plain, (~c5_1(a507))). % 5.27/2.14 tff(c_333, plain, (~ndr1_1(a507))). % 5.27/2.14 tff(c_332, plain, (~c2_2(a503, a505))). % 5.27/2.14 tff(c_328, plain, (~c2_2(a503, a504))). % 5.27/2.14 tff(c_324, plain, (~c5_2(a503, a505))). % 5.27/2.14 tff(c_320, plain, (~c5_2(a503, a504))). % 5.27/2.14 tff(c_316, plain, (~c3_2(a503, a505))). % 5.27/2.14 tff(c_312, plain, (c4_2(a503, a504))). % 5.27/2.14 tff(c_308, plain, (ndr1_1(a503))). % 5.27/2.14 tff(c_297, plain, (![U_4]: (c4_1(U_4) | c5_2(U_4, a506) | ~c5_1(U_4)))). % 5.27/2.14 tff(c_293, plain, (![U_7]: (c4_1(U_7) | ~c5_1(U_7) | ~c3_2(U_7, a506)))). % 5.27/2.14 tff(c_289, plain, (![U_6]: (~c3_2(a495, U_6) | ~c5_2(a495, U_6)))). % 5.27/2.14 tff(c_285, plain, (![U_3]: (c4_1(U_3) | c4_2(U_3, a506) | ~c5_1(U_3)))). % 5.27/2.14 tff(c_281, plain, (![U_2]: (c4_1(U_2) | ndr1_1(U_2) | ~c5_1(U_2)))). % 5.27/2.14 tff(c_278, plain, (~c3_0)). % 5.27/2.14 tff(c_269, plain, (~c3_2(a500, a501))). % 5.27/2.14 tff(c_267, plain, (~ssSkC1)). % 5.27/2.14 tff(c_266, plain, (~c4_2(a517, a518))). % 5.27/2.14 tff(c_262, plain, (~ssSkC6)). % 5.27/2.14 tff(c_259, plain, (~c5_2(a495, a496))). % 5.27/2.14 tff(c_258, plain, (c4_2(a495, a496))). % 5.27/2.14 tff(c_257, plain, (c5_2(a517, a518))). % 5.27/2.14 tff(c_256, plain, (c3_2(a517, a518))). % 5.27/2.14 tff(c_255, plain, (~ssSkC3)). % 5.27/2.14 tff(c_254, plain, (~ssSkC7)). % 5.27/2.14 tff(c_252, plain, (~c5_2(a492, a493))). % 5.27/2.14 tff(c_251, plain, (~ssSkC0)). % 5.27/2.14 tff(c_249, plain, (~c2_2(a492, a493))). % 5.27/2.15 tff(c_248, plain, (c1_2(a500, a501))). % 5.27/2.15 tff(c_247, plain, (~c2_2(a500, a501))). % 5.27/2.15 tff(c_246, plain, (c2_2(a495, a496))). % 5.27/2.15 tff(c_245, plain, (~c3_2(a492, a493))). % 5.27/2.15 tff(c_244, plain, (~c2_1(a509))). % 5.27/2.15 tff(c_243, plain, (~c4_1(a513))). % 5.27/2.15 tff(c_242, plain, (~c3_1(a511))). % 5.27/2.15 tff(c_241, plain, (~c2_1(a517))). % 5.27/2.15 tff(c_240, plain, (c3_1(a507))). % 5.27/2.15 tff(c_237, plain, (ndr1_1(a492))). % 5.27/2.15 tff(c_236, plain, (c2_1(a495))). % 5.27/2.15 tff(c_235, plain, (ndr1_1(a500))). % 5.27/2.15 tff(c_232, plain, (c1_1(a513))). % 5.27/2.15 tff(c_231, plain, (ndr1_1(a517))). % 5.27/2.15 tff(c_230, plain, (c3_1(a513))). % 5.27/2.15 tff(c_229, plain, (c4_1(a517))). % 5.27/2.15 tff(c_225, plain, (~c1_0)). % 5.27/2.15 tff(c_224, plain, (~c4_1(a507))). % 5.27/2.15 tff(c_223, plain, (~c4_1(a499))). % 5.27/2.15 tff(c_222, plain, (c5_1(a492))). % 5.27/2.15 tff(c_219, plain, (~c2_1(a500))). % 5.27/2.15 tff(c_218, plain, (~c2_1(a492))). % 5.27/2.15 tff(c_217, plain, (ndr1_1(a495))). % 5.27/2.15 tff(c_216, plain, (c3_1(a500))). % 5.27/2.15 tff(c_215, plain, (~c1_1(a516))). % 5.27/2.15 tff(c_214, plain, (~c2_1(a511))). % 5.27/2.15 tff(c_213, plain, (~c5_0)). % 5.27/2.15 tff(c_206, plain, (c4_0)). % 5.27/2.15 tff(c_202, plain, (ndr1_0)). % 5.27/2.15 tff(c_201, plain, (~c2_0)). % 5.27/2.15 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 5.27/2.15 %------------------------------------------------------------------------------