%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : PLA029-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/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 : n010.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 2.96s 1.63s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.11 % Problem : PLA029-1 : TPTP v9.0.0. Released v2.5.0. % 0.12/0.12 % 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.33 % Computer : n010.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Tue Apr 8 16:36:33 EDT 2025 % 0.13/0.33 % CPUTime : % 2.96/1.63 % 2.96/1.63 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.96/1.64 % 2.96/1.64 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.96/1.64 %$ holds > differ > putdown > on > do > and > #nlpp > pickup > holding > clear > table > empty % 2.96/1.64 % 2.96/1.64 %Foreground sorts: % 2.96/1.64 % 2.96/1.64 % 2.96/1.64 %Background operators: % 2.96/1.64 % 2.96/1.64 % 2.96/1.64 %Foreground operators: % 2.96/1.64 tff(putdown, type, putdown: ($i * $i) > $i). % 2.96/1.64 tff(pickup, type, pickup: $i > $i). % 2.96/1.64 tff(on, type, on: ($i * $i) > $i). % 2.96/1.64 tff(holding, type, holding: $i > $i). % 2.96/1.64 tff(holds, type, holds: ($i * $i) > $o). % 2.96/1.64 tff(clear, type, clear: $i > $i). % 2.96/1.64 tff(table, type, table: $i). % 2.96/1.64 tff(and, type, and: ($i * $i) > $i). % 2.96/1.64 tff(differ, type, differ: ($i * $i) > $o). % 2.96/1.64 tff(empty, type, empty: $i). % 2.96/1.64 tff(do, type, do: ($i * $i) > $i). % 2.96/1.64 % 2.96/1.64 %Saturated clause set: % 2.96/1.65 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))))). % 2.96/1.65 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))))). % 2.96/1.65 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))))). % 2.96/1.65 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))))). % 2.96/1.65 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))))). % 2.96/1.65 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))))). % 2.96/1.65 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))))). % 2.96/1.65 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))))). % 2.96/1.65 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))))). % 2.96/1.65 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)))). % 2.96/1.65 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.96/1.65 %------------------------------------------------------------------------------