%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : GRA013+1 : TPTP v9.0.0. Released v3.2.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 : n026.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 06:23:20 PM UTC 2025 % Result : CounterSatisfiable 6.13s 2.57s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : GRA013+1 : TPTP v9.0.0. Released v3.2.0. % 0.03/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 : n026.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 : Mon Apr 7 20:51:38 EDT 2025 % 0.12/0.34 % CPUTime : % 6.13/2.56 % 6.13/2.57 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.13/2.57 % 6.13/2.57 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.13/2.57 %$ red > less_than > green > #nlpp > n5 > n4 > n3 > n2 > n1 > goal % 6.13/2.57 % 6.13/2.57 %Foreground sorts: % 6.13/2.57 % 6.13/2.57 % 6.13/2.57 %Background operators: % 6.13/2.57 % 6.13/2.57 % 6.13/2.57 %Foreground operators: % 6.13/2.57 tff(green, type, green: ($i * $i) > $o). % 6.13/2.57 tff(n3, type, n3: $i). % 6.13/2.57 tff(goal, type, goal: $o). % 6.13/2.57 tff(n1, type, n1: $i). % 6.13/2.57 tff(red, type, red: ($i * $i) > $o). % 6.13/2.57 tff(less_than, type, less_than: ($i * $i) > $o). % 6.13/2.57 tff(n4, type, n4: $i). % 6.13/2.57 tff(n2, type, n2: $i). % 6.13/2.57 tff(n5, type, n5: $i). % 6.13/2.57 % 6.13/2.57 %Saturated clause set: % 6.13/2.58 tff(c_2760, plain, (![A_136, A_7]: (green(A_136, n4) | green(A_7, n4) | green(A_136, A_7) | ~less_than(A_136, A_7) | ~less_than(A_136, n2) | ~less_than(A_7, n2)))). % 6.13/2.58 tff(c_2766, plain, (![A_136, A_20]: (green(A_136, n4) | green(A_20, n4) | green(A_136, A_20) | ~less_than(A_136, A_20) | ~less_than(A_136, n2) | ~less_than(A_20, n3)))). % 6.13/2.58 tff(c_2761, plain, (![A_136, A_20]: (green(A_136, n4) | green(A_20, n4) | green(A_136, A_20) | ~less_than(A_136, A_20) | ~less_than(A_136, n2) | ~less_than(A_20, n1)))). % 6.13/2.58 tff(c_1920, plain, (![A_108, A_20]: (green(A_108, n5) | green(A_20, n5) | green(A_108, A_20) | ~less_than(A_108, A_20) | ~less_than(A_108, n2) | ~less_than(A_20, n1)))). % 6.13/2.58 tff(c_1441, plain, (![A_85, A_20]: (green(A_85, n4) | green(A_20, n4) | green(A_85, A_20) | ~less_than(A_85, A_20) | ~less_than(A_85, n3) | ~less_than(A_20, n1)))). % 6.13/2.58 tff(c_2170, plain, (![A_118, A_20]: (green(A_118, n5) | green(A_20, n5) | green(A_118, A_20) | ~less_than(A_118, A_20) | ~less_than(A_118, n4) | ~less_than(A_20, n4)))). % 6.13/2.58 tff(c_1511, plain, (![A_91, A_7]: (green(A_91, n4) | green(A_7, n4) | green(A_91, A_7) | ~less_than(A_91, A_7) | ~less_than(A_91, n1) | ~less_than(A_7, n2)))). % 6.13/2.58 tff(c_1927, plain, (![A_108, A_20]: (green(A_108, n5) | green(A_20, n5) | green(A_108, A_20) | ~less_than(A_108, A_20) | ~less_than(A_108, n2) | ~less_than(A_20, n4)))). % 6.13/2.58 tff(c_1512, plain, (![A_91, A_20]: (green(A_91, n4) | green(A_20, n4) | green(A_91, A_20) | ~less_than(A_91, A_20) | ~less_than(A_91, n1) | ~less_than(A_20, n1)))). % 6.13/2.58 tff(c_1518, plain, (![A_91, A_20]: (green(A_91, n4) | green(A_20, n4) | green(A_91, A_20) | ~less_than(A_91, A_20) | ~less_than(A_91, n1) | ~less_than(A_20, n3)))). % 6.13/2.58 tff(c_1921, plain, (![A_108, A_20]: (green(A_108, n5) | green(A_20, n5) | green(A_108, A_20) | ~less_than(A_108, A_20) | ~less_than(A_108, n2) | ~less_than(A_20, n2)))). % 6.13/2.58 tff(c_1831, plain, (![A_103, A_20]: (green(A_103, n3) | green(A_20, n3) | green(A_103, A_20) | ~less_than(A_103, A_20) | ~less_than(A_103, n2) | ~less_than(A_20, n2)))). % 6.13/2.58 tff(c_2164, plain, (![A_118, A_20]: (green(A_118, n5) | green(A_20, n5) | green(A_118, A_20) | ~less_than(A_118, A_20) | ~less_than(A_118, n4) | ~less_than(A_20, n1)))). % 6.13/2.58 tff(c_2165, plain, (![A_118, A_20]: (green(A_118, n5) | green(A_20, n5) | green(A_118, A_20) | ~less_than(A_118, A_20) | ~less_than(A_118, n4) | ~less_than(A_20, n2)))). % 6.13/2.58 tff(c_415, plain, (![A_48, B_11]: (green(A_48, n4) | green(B_11, n4) | ~less_than(B_11, n4) | green(A_48, B_11) | ~less_than(A_48, B_11) | ~less_than(A_48, n2)))). % 6.13/2.58 tff(c_2071, plain, (![A_115, A_20]: (green(A_115, n2) | green(A_20, n2) | green(A_115, A_20) | ~less_than(A_115, A_20) | ~less_than(A_115, n1) | ~less_than(A_20, n1)))). % 6.13/2.58 tff(c_1440, plain, (![A_85, A_7]: (green(A_85, n4) | green(A_7, n4) | green(A_85, A_7) | ~less_than(A_85, A_7) | ~less_than(A_85, n3) | ~less_than(A_7, n2)))). % 6.13/2.58 tff(c_1655, plain, (![A_96, A_20]: (green(A_96, n5) | green(A_20, n5) | green(A_96, A_20) | ~less_than(A_96, A_20) | ~less_than(A_96, n1) | ~less_than(A_20, n4)))). % 6.13/2.58 tff(c_1647, plain, (![A_96, A_20]: (green(A_96, n5) | green(A_20, n5) | green(A_96, A_20) | ~less_than(A_96, A_20) | ~less_than(A_96, n1) | ~less_than(A_20, n1)))). % 6.13/2.58 tff(c_1648, plain, (![A_96, A_20]: (green(A_96, n5) | green(A_20, n5) | green(A_96, A_20) | ~less_than(A_96, A_20) | ~less_than(A_96, n1) | ~less_than(A_20, n2)))). % 6.13/2.58 tff(c_1447, plain, (![A_85, A_20]: (green(A_85, n4) | green(A_20, n4) | green(A_85, A_20) | ~less_than(A_85, A_20) | ~less_than(A_85, n3) | ~less_than(A_20, n3)))). % 6.13/2.58 tff(c_883, plain, (![A_20]: (green(A_20, n5) | green(n2, A_20) | ~less_than(n2, A_20) | ~less_than(A_20, n4)))). % 6.13/2.58 tff(c_2267, plain, (~green(n3, n3))). % 6.13/2.58 tff(c_2260, plain, (~green(n4, n3))). % 6.13/2.59 tff(c_2261, plain, (![B_5]: (~green(B_5, n5) | ~green(n3, B_5)))). % 6.13/2.59 tff(c_2254, plain, (green(n3, n5))). % 6.13/2.59 tff(c_2255, plain, (~green(n1, n3))). % 6.13/2.59 tff(c_259, plain, (![A_20, B_41]: (green(A_20, n5) | green(B_41, n5) | ~less_than(B_41, n5) | green(A_20, B_41) | ~less_than(A_20, B_41) | ~less_than(A_20, n4)))). % 6.13/2.59 tff(c_2138, plain, (~less_than(n5, n4))). % 6.13/2.59 tff(c_1048, plain, (![A_20]: (green(A_20, n5) | green(n1, A_20) | ~less_than(n1, A_20) | ~less_than(A_20, n4)))). % 6.13/2.59 tff(c_258, plain, (![A_20, B_41]: (green(A_20, n2) | green(B_41, n2) | ~less_than(B_41, n2) | green(A_20, B_41) | ~less_than(A_20, B_41) | ~less_than(A_20, n1)))). % 6.13/2.59 tff(c_1487, plain, (![A_7]: (green(A_7, n4) | green(n2, A_7) | ~less_than(n2, A_7) | ~less_than(A_7, n2)))). % 6.13/2.59 tff(c_1403, plain, (![A_20]: (green(A_20, n4) | green(n3, A_20) | ~less_than(n3, A_20) | ~less_than(A_20, n3)))). % 6.13/2.59 tff(c_1948, plain, (![A_20]: (green(A_20, n4) | green(A_20, n2) | ~less_than(A_20, n2)))). % 6.13/2.59 tff(c_1926, plain, (![A_108]: (green(A_108, n5) | green(A_108, n2) | ~less_than(A_108, n2)))). % 6.13/2.59 tff(c_280, plain, (![A_42, B_11]: (green(A_42, n5) | green(B_11, n5) | ~less_than(B_11, n5) | green(A_42, B_11) | ~less_than(A_42, B_11) | ~less_than(A_42, n2)))). % 6.13/2.59 tff(c_1902, plain, (![A_20]: (green(A_20, n5) | green(A_20, n2) | ~less_than(A_20, n1)))). % 6.13/2.59 tff(c_1039, plain, (![A_20]: (green(A_20, n5) | green(n1, A_20) | ~less_than(n1, A_20) | ~less_than(A_20, n1)))). % 6.13/2.59 tff(c_257, plain, (![A_20, B_41]: (green(A_20, n3) | green(B_41, n3) | ~less_than(B_41, n3) | green(A_20, B_41) | ~less_than(A_20, B_41) | ~less_than(A_20, n2)))). % 6.13/2.59 tff(c_1493, plain, (![A_20]: (green(A_20, n4) | green(n2, A_20) | ~less_than(n2, A_20) | ~less_than(A_20, n3)))). % 6.13/2.59 tff(c_1398, plain, (![A_7]: (green(A_7, n4) | green(n3, A_7) | ~less_than(n3, A_7) | ~less_than(A_7, n2)))). % 6.13/2.59 tff(c_1040, plain, (![A_20]: (green(A_20, n5) | green(n1, A_20) | ~less_than(n1, A_20) | ~less_than(A_20, n2)))). % 6.13/2.59 tff(c_1631, plain, (![A_20]: (green(A_20, n4) | green(A_20, n2) | ~less_than(A_20, n1)))). % 6.13/2.59 tff(c_1651, plain, (![A_96]: (green(A_96, n5) | green(A_96, n1) | ~less_than(A_96, n1)))). % 6.13/2.59 tff(c_388, plain, (![A_46, B_11]: (green(A_46, n5) | green(B_11, n5) | ~less_than(B_11, n5) | green(A_46, B_11) | ~less_than(A_46, B_11) | ~less_than(A_46, n1)))). % 6.13/2.59 tff(c_1399, plain, (![A_20]: (green(A_20, n4) | green(n3, A_20) | ~less_than(n3, A_20) | ~less_than(A_20, n1)))). % 6.13/2.59 tff(c_1488, plain, (![A_20]: (green(A_20, n4) | green(n2, A_20) | ~less_than(n2, A_20) | ~less_than(A_20, n1)))). % 6.13/2.59 tff(c_352, plain, (![A_45, B_11]: (green(A_45, n4) | green(B_11, n4) | ~less_than(B_11, n4) | green(A_45, B_11) | ~less_than(A_45, B_11) | ~less_than(A_45, n1)))). % 6.13/2.59 tff(c_1421, plain, (![B_41]: (green(B_41, n4) | ~less_than(B_41, n4) | green(n2, B_41) | ~less_than(n2, B_41)))). % 6.13/2.59 tff(c_1470, plain, (![A_20]: (green(A_20, n4) | green(A_20, n3) | ~less_than(A_20, n1)))). % 6.13/2.59 tff(c_1459, plain, (![A_20]: (green(A_20, n4) | green(A_20, n3) | ~less_than(A_20, n2)))). % 6.13/2.59 tff(c_1450, plain, (![A_85]: (green(A_85, n4) | green(A_85, n3) | ~less_than(A_85, n3)))). % 6.13/2.59 tff(c_260, plain, (![A_20, B_41]: (green(A_20, n4) | green(B_41, n4) | ~less_than(B_41, n4) | green(A_20, B_41) | ~less_than(A_20, B_41) | ~less_than(A_20, n3)))). % 6.13/2.59 tff(c_1411, plain, (~less_than(n3, n2))). % 6.13/2.59 tff(c_1422, plain, (~green(n2, n4))). % 6.13/2.59 tff(c_1407, plain, (~less_than(n3, n3))). % 6.13/2.59 tff(c_1383, plain, (![B_41]: (green(B_41, n4) | ~less_than(B_41, n4) | green(n3, B_41) | ~less_than(n3, B_41)))). % 6.13/2.59 tff(c_1043, plain, (~less_than(n1, n1))). % 6.13/2.59 tff(c_1384, plain, (~green(n3, n4))). % 6.13/2.59 tff(c_1024, plain, (![B_41]: (green(B_41, n5) | ~less_than(B_41, n5) | green(n1, B_41) | ~less_than(n1, B_41)))). % 6.13/2.59 tff(c_1025, plain, (~green(n1, n5))). % 6.13/2.59 tff(c_879, plain, (![A_20]: (green(A_20, n5) | green(n2, A_20) | ~less_than(n2, A_20) | ~less_than(A_20, n2)))). % 6.13/2.59 tff(c_946, plain, (![B_5]: (~green(B_5, n4) | ~green(n1, B_5)))). % 6.13/2.59 tff(c_943, plain, (green(n1, n4))). % 6.13/2.59 tff(c_878, plain, (![A_20]: (green(A_20, n5) | green(n2, A_20) | ~less_than(n2, A_20) | ~less_than(A_20, n1)))). % 6.13/2.59 tff(c_863, plain, (![B_41]: (green(B_41, n5) | ~less_than(B_41, n5) | green(n2, B_41) | ~less_than(n2, B_41)))). % 6.13/2.59 tff(c_864, plain, (~green(n2, n5))). % 6.13/2.59 tff(c_420, plain, (![A_7, A_48]: (less_than(A_7, n4) | ~less_than(A_7, A_48) | ~less_than(A_48, n2)))). % 6.13/2.59 tff(c_357, plain, (![A_7, A_45]: (less_than(A_7, n4) | ~less_than(A_7, A_45) | ~less_than(A_45, n1)))). % 6.13/2.59 tff(c_550, plain, (~green(n1, n1))). % 6.13/2.59 tff(c_546, plain, (![B_5]: (~green(B_5, n2) | ~green(n1, B_5)))). % 6.13/2.59 tff(c_543, plain, (green(n1, n2))). % 6.13/2.60 tff(c_392, plain, (![A_7, A_46]: (less_than(A_7, n5) | ~less_than(A_7, A_46) | ~less_than(A_46, n1)))). % 6.13/2.60 tff(c_284, plain, (![A_7, A_42]: (less_than(A_7, n5) | ~less_than(A_7, A_42) | ~less_than(A_42, n2)))). % 6.13/2.60 tff(c_430, plain, (~green(n2, n2))). % 6.13/2.60 tff(c_426, plain, (![B_5]: (~green(B_5, n3) | ~green(n2, B_5)))). % 6.13/2.60 tff(c_423, plain, (green(n2, n3))). % 6.13/2.60 tff(c_160, plain, (![A_7]: (less_than(A_7, n4) | ~less_than(A_7, n2)))). % 6.13/2.60 tff(c_397, plain, (~green(n4, n4))). % 6.13/2.60 tff(c_366, plain, (![B_5]: (~green(B_5, n5) | ~green(n4, B_5)))). % 6.13/2.60 tff(c_373, plain, (![A_20]: (less_than(A_20, n5) | ~less_than(A_20, n1)))). % 6.13/2.60 tff(c_367, plain, (~less_than(n5, n3))). % 6.13/2.60 tff(c_363, plain, (~less_than(n2, n1))). % 6.13/2.60 tff(c_359, plain, (green(n4, n5))). % 6.13/2.60 tff(c_358, plain, (~less_than(n2, n2))). % 6.13/2.60 tff(c_194, plain, (![A_20]: (less_than(A_20, n4) | ~less_than(A_20, n1)))). % 6.13/2.60 tff(c_327, plain, (~less_than(n5, n2))). % 6.13/2.60 tff(c_59, plain, (![A_7, A_29]: (less_than(A_7, n3) | ~less_than(A_7, A_29) | ~less_than(A_29, n2)))). % 6.13/2.60 tff(c_285, plain, (~less_than(n3, n1))). % 6.13/2.60 tff(c_105, plain, (![A_20]: (less_than(A_20, n5) | ~less_than(A_20, n2)))). % 6.13/2.60 tff(c_268, plain, (~less_than(n4, n1))). % 6.13/2.60 tff(c_227, plain, (~less_than(n4, n2))). % 6.13/2.60 tff(c_139, plain, (![A_10, B_36, B_11]: (green(A_10, B_36) | ~less_than(A_10, B_36) | green(B_11, B_36) | ~less_than(B_11, B_36) | green(A_10, B_11) | ~less_than(A_10, B_11)))). % 6.13/2.60 tff(c_223, plain, (~less_than(n4, n3))). % 6.13/2.60 tff(c_162, plain, (~less_than(n4, n4))). % 6.13/2.60 tff(c_204, plain, (less_than(n1, n4))). % 6.13/2.60 tff(c_47, plain, (![A_7, A_26]: (less_than(A_7, n4) | ~less_than(A_7, A_26) | ~less_than(A_26, n3)))). % 6.13/2.60 tff(c_161, plain, (~less_than(n5, n1))). % 6.13/2.60 tff(c_135, plain, (less_than(n2, n4))). % 6.13/2.60 tff(c_134, plain, (less_than(n1, n5))). % 6.13/2.60 tff(c_43, plain, (![A_25, A_10, B_11]: (~red(A_25, A_10) | green(A_25, B_11) | ~less_than(A_25, B_11) | green(A_10, B_11) | ~less_than(A_10, B_11)))). % 6.13/2.60 tff(c_114, plain, (less_than(n2, n5))). % 6.13/2.60 tff(c_51, plain, (![A_7, A_27]: (less_than(A_7, n5) | ~less_than(A_7, A_27) | ~less_than(A_27, n4)))). % 6.13/2.60 tff(c_55, plain, (![A_7, A_28]: (less_than(A_7, n2) | ~less_than(A_7, A_28) | ~less_than(A_28, n1)))). % 6.13/2.60 tff(c_38, plain, (![A_20]: (less_than(A_20, n3) | ~less_than(A_20, n2)))). % 6.13/2.60 tff(c_39, plain, (![A_20]: (less_than(A_20, n2) | ~less_than(A_20, n1)))). % 6.13/2.60 tff(c_37, plain, (![A_20]: (less_than(A_20, n5) | ~less_than(A_20, n4)))). % 6.13/2.60 tff(c_36, plain, (![A_20]: (less_than(A_20, n4) | ~less_than(A_20, n3)))). % 6.13/2.60 tff(c_26, plain, (![B_2, B_19, A_18]: (~red(B_2, B_19) | ~red(A_18, B_2) | green(A_18, B_19) | ~less_than(A_18, B_19)))). % 6.13/2.60 tff(c_14, plain, (![A_7, C_9, B_8]: (less_than(A_7, C_9) | ~less_than(B_8, C_9) | ~less_than(A_7, B_8)))). % 6.13/2.60 tff(c_16, plain, (![A_10, B_11]: (green(A_10, B_11) | red(A_10, B_11) | ~less_than(A_10, B_11)))). % 6.43/2.60 tff(c_19, plain, (![A_4, C_6, B_5]: (~green(A_4, C_6) | ~green(B_5, C_6) | ~green(A_4, B_5)))). % 6.43/2.60 tff(c_20, plain, (![A_1, C_3, B_2]: (~red(A_1, C_3) | ~red(B_2, C_3) | ~red(A_1, B_2)))). % 6.43/2.60 tff(c_8, plain, (less_than(n3, n4))). % 6.43/2.60 tff(c_6, plain, (less_than(n4, n5))). % 6.43/2.60 tff(c_10, plain, (less_than(n2, n3))). % 6.43/2.60 tff(c_12, plain, (less_than(n1, n2))). % 6.43/2.60 tff(c_18, plain, (~goal)). % 6.43/2.60 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.43/2.60 %------------------------------------------------------------------------------