%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : PLA030-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 : 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 08:23:05 PM UTC 2025 % Result : Satisfiable 3.76s 2.02s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : PLA030-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.14/0.34 % Computer : n006.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Tue Apr 8 16:35:23 EDT 2025 % 0.14/0.35 % CPUTime : % 3.76/2.02 % 3.76/2.02 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.76/2.02 % 3.76/2.02 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.76/2.03 %$ holds > differ > putdown > on > do > and > #nlpp > pickup > holding > clear > table > s0 > empty > d > c > b > a % 3.76/2.03 % 3.76/2.03 %Foreground sorts: % 3.76/2.03 % 3.76/2.03 % 3.76/2.03 %Background operators: % 3.76/2.03 % 3.76/2.03 % 3.76/2.03 %Foreground operators: % 3.76/2.03 tff(s0, type, s0: $i). % 3.76/2.03 tff(a, type, a: $i). % 3.76/2.03 tff(putdown, type, putdown: ($i * $i) > $i). % 3.76/2.03 tff(pickup, type, pickup: $i > $i). % 3.76/2.03 tff(b, type, b: $i). % 3.76/2.03 tff(on, type, on: ($i * $i) > $i). % 3.76/2.03 tff(holding, type, holding: $i > $i). % 3.76/2.03 tff(holds, type, holds: ($i * $i) > $o). % 3.76/2.03 tff(clear, type, clear: $i > $i). % 3.76/2.03 tff(d, type, d: $i). % 3.76/2.03 tff(table, type, table: $i). % 3.76/2.03 tff(and, type, and: ($i * $i) > $i). % 3.76/2.03 tff(differ, type, differ: ($i * $i) > $o). % 3.76/2.03 tff(empty, type, empty: $i). % 3.76/2.03 tff(do, type, do: ($i * $i) > $i). % 3.76/2.03 tff(c, type, c: $i). % 3.76/2.03 % 3.76/2.03 %Saturated clause set: % 3.76/2.03 tff(c_6, plain, (![State_8, X_7, Y_6]: (~holds(empty, State_8) | ~holds(clear(X_7), State_8) | ~holds(on(X_7, Y_6), State_8) | holds(clear(Y_6), do(pickup(X_7), State_8))))). % 3.76/2.03 tff(c_4, plain, (![X_4, State_5]: (~differ(X_4, table) | ~holds(clear(X_4), State_5) | ~holds(empty, State_5) | holds(holding(X_4), do(pickup(X_4), State_5))))). % 3.76/2.03 tff(c_14, plain, (![Y_20, State_21, X_19]: (~holds(clear(Y_20), State_21) | ~holds(holding(X_19), State_21) | holds(on(X_19, Y_20), do(putdown(X_19, Y_20), State_21))))). % 3.76/2.03 tff(c_16, plain, (![Y_23, State_24, X_22]: (~holds(clear(Y_23), State_24) | ~holds(holding(X_22), State_24) | holds(clear(X_22), do(putdown(X_22, Y_23), State_24))))). % 3.76/2.03 tff(c_8, plain, (![X_9, Z_11, Y_10, State_12]: (~differ(X_9, Z_11) | ~holds(on(X_9, Y_10), State_12) | holds(on(X_9, Y_10), do(pickup(Z_11), State_12))))). % 3.76/2.03 tff(c_12, plain, (![Y_17, State_18, X_16]: (~holds(clear(Y_17), State_18) | ~holds(holding(X_16), State_18) | holds(empty, do(putdown(X_16, Y_17), State_18))))). % 3.76/2.03 tff(c_20, plain, (![Z_30, Y_32, State_33, X_31]: (~differ(Z_30, Y_32) | ~holds(clear(Z_30), State_33) | holds(clear(Z_30), do(putdown(X_31, Y_32), State_33))))). % 3.76/2.03 tff(c_18, plain, (![W_25, State_29, Z_26, Y_28, X_27]: (~holds(on(X_27, Y_28), State_29) | holds(on(X_27, Y_28), do(putdown(Z_26, W_25), State_29))))). % 3.76/2.03 tff(c_87, plain, (differ(c, b))). % 3.76/2.03 tff(c_84, plain, (differ(d, c))). % 3.76/2.03 tff(c_10, plain, (![X_13, Z_14, State_15]: (~differ(X_13, Z_14) | ~holds(clear(X_13), State_15) | holds(clear(X_13), do(pickup(Z_14), State_15))))). % 3.76/2.03 tff(c_85, plain, (differ(table, b))). % 3.76/2.03 tff(c_86, plain, (differ(d, b))). % 3.76/2.03 tff(c_92, plain, (differ(table, d))). % 3.76/2.04 tff(c_2, plain, (![Y_2, State_3, X_1]: (~holds(Y_2, State_3) | ~holds(X_1, State_3) | holds(and(X_1, Y_2), State_3)))). % 3.76/2.04 tff(c_91, plain, (differ(table, a))). % 3.76/2.04 tff(c_90, plain, (differ(d, a))). % 3.76/2.04 tff(c_89, plain, (differ(c, a))). % 3.76/2.04 tff(c_88, plain, (differ(b, a))). % 3.76/2.04 tff(c_83, plain, (differ(table, c))). % 3.76/2.04 tff(c_22, plain, (![Y_35, X_34]: (~differ(Y_35, X_34) | differ(X_34, Y_35)))). % 3.76/2.04 tff(c_48, plain, (holds(on(c, d), s0))). % 3.76/2.04 tff(c_50, plain, (holds(on(d, table), s0))). % 3.76/2.04 tff(c_46, plain, (holds(on(b, table), s0))). % 3.76/2.04 tff(c_44, plain, (holds(on(a, table), s0))). % 3.76/2.04 tff(c_56, plain, (holds(clear(c), s0))). % 3.76/2.04 tff(c_60, plain, (![State_36]: (holds(clear(table), State_36)))). % 3.76/2.04 tff(c_52, plain, (holds(clear(a), s0))). % 3.76/2.04 tff(c_54, plain, (holds(clear(b), s0))). % 3.76/2.04 tff(c_40, plain, (differ(c, table))). % 3.76/2.04 tff(c_38, plain, (differ(c, d))). % 3.76/2.04 tff(c_36, plain, (differ(b, table))). % 3.76/2.04 tff(c_34, plain, (differ(b, d))). % 3.76/2.04 tff(c_32, plain, (differ(b, c))). % 3.76/2.04 tff(c_24, plain, (differ(a, b))). % 3.76/2.04 tff(c_26, plain, (differ(a, c))). % 3.76/2.04 tff(c_28, plain, (differ(a, d))). % 3.76/2.04 tff(c_30, plain, (differ(a, table))). % 3.76/2.04 tff(c_42, plain, (differ(d, table))). % 3.76/2.04 tff(c_58, plain, (holds(empty, s0))). % 3.76/2.04 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.76/2.04 %------------------------------------------------------------------------------