%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : HWV036-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 : n013.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:46:52 PM UTC 2025 % Result : Satisfiable 4.69s 2.13s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : HWV036-1 : TPTP v9.0.0. Released v2.5.0. % 0.08/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.13/0.34 % Computer : n013.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 : Mon Apr 7 22:58:47 EDT 2025 % 0.13/0.34 % CPUTime : % 4.69/2.12 % 4.69/2.13 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.69/2.13 % 4.69/2.13 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.69/2.13 %$ value > type > mode > equal_value > connection > out > in > #nlpp > or1 > not1 > h2 > h1 > and2 > and1 > s > or > ok > not > n2 > n1 > n0 > halfadder > fulladder > c > and > abnormal % 4.69/2.13 % 4.69/2.13 %Foreground sorts: % 4.69/2.13 % 4.69/2.13 % 4.69/2.13 %Background operators: % 4.69/2.13 % 4.69/2.13 % 4.69/2.13 %Foreground operators: % 4.69/2.13 tff(or, type, or: $i). % 4.69/2.13 tff(and, type, and: $i). % 4.69/2.13 tff(not, type, not: $i). % 4.69/2.13 tff(or1, type, or1: $i > $i). % 4.69/2.13 tff(in, type, in: ($i * $i) > $i). % 4.69/2.13 tff(connection, type, connection: ($i * $i) > $o). % 4.69/2.13 tff(s, type, s: $i). % 4.69/2.13 tff(halfadder, type, halfadder: $i). % 4.69/2.13 tff(h2, type, h2: $i > $i). % 4.69/2.13 tff(and2, type, and2: $i > $i). % 4.69/2.13 tff(equal_value, type, equal_value: ($i * $i) > $o). % 4.69/2.13 tff(n1, type, n1: $i). % 4.69/2.13 tff(h1, type, h1: $i > $i). % 4.69/2.13 tff(n0, type, n0: $i). % 4.69/2.13 tff(type, type, type: ($i * $i) > $o). % 4.69/2.13 tff(fulladder, type, fulladder: $i). % 4.69/2.13 tff(value, type, value: ($i * $i) > $o). % 4.69/2.13 tff(not1, type, not1: $i > $i). % 4.69/2.13 tff(and1, type, and1: $i > $i). % 4.69/2.13 tff(abnormal, type, abnormal: $i). % 4.69/2.13 tff(n2, type, n2: $i). % 4.69/2.13 tff(out, type, out: ($i * $i) > $i). % 4.69/2.13 tff(mode, type, mode: ($i * $i) > $o). % 4.69/2.13 tff(ok, type, ok: $i). % 4.69/2.13 tff(c, type, c: $i). % 4.69/2.13 % 4.69/2.13 %Saturated clause set: % 4.69/2.14 tff(c_387, plain, (![X_39]: (value(in(n1, and1(X_39)), n1) | ~value(in(n2, or1(X_39)), n1) | ~value(in(n1, or1(X_39)), n1) | ~type(or1(X_39), and) | ~mode(or1(X_39), ok) | ~type(X_39, halfadder)))). % 4.69/2.14 tff(c_397, plain, (![X_39]: (value(in(n1, and1(X_39)), n0) | ~value(in(n2, or1(X_39)), n0) | ~value(in(n1, or1(X_39)), n0) | ~type(or1(X_39), or) | ~mode(or1(X_39), ok) | ~type(X_39, halfadder)))). % 4.69/2.14 tff(c_395, plain, (![X_40]: (value(in(n1, not1(X_40)), n0) | ~value(in(n2, and2(X_40)), n0) | ~value(in(n1, and2(X_40)), n0) | ~type(and2(X_40), or) | ~mode(and2(X_40), ok) | ~type(X_40, halfadder)))). % 4.69/2.14 tff(c_385, plain, (![X_40]: (value(in(n1, not1(X_40)), n1) | ~value(in(n2, and2(X_40)), n1) | ~value(in(n1, and2(X_40)), n1) | ~type(and2(X_40), and) | ~mode(and2(X_40), ok) | ~type(X_40, halfadder)))). % 4.69/2.14 tff(c_357, plain, (![K_21]: (~value(in(n2, K_21), n1) | ~value(in(n1, K_21), n1) | ~type(K_21, and) | ~value(in(n2, K_21), n0) | ~value(in(n1, K_21), n0) | ~type(K_21, or) | ~mode(K_21, ok)))). % 4.69/2.14 tff(c_396, plain, (![X_41]: (value(in(n2, and1(X_41)), n0) | ~value(in(n2, not1(X_41)), n0) | ~value(in(n1, not1(X_41)), n0) | ~type(not1(X_41), or) | ~mode(not1(X_41), ok) | ~type(X_41, halfadder)))). % 4.69/2.14 tff(c_386, plain, (![X_41]: (value(in(n2, and1(X_41)), n1) | ~value(in(n2, not1(X_41)), n1) | ~value(in(n1, not1(X_41)), n1) | ~type(not1(X_41), and) | ~mode(not1(X_41), ok) | ~type(X_41, halfadder)))). % 4.69/2.14 tff(c_365, plain, (![X_38]: (value(out(c, X_38), n0) | ~value(in(n2, and2(X_38)), n0) | ~value(in(n1, and2(X_38)), n0) | ~type(and2(X_38), or) | ~mode(and2(X_38), ok) | ~type(X_38, halfadder)))). % 4.69/2.14 tff(c_377, plain, (![X_52]: (value(out(c, X_52), n1) | ~value(in(n2, or1(X_52)), n1) | ~value(in(n1, or1(X_52)), n1) | ~type(or1(X_52), and) | ~mode(or1(X_52), ok) | ~type(X_52, fulladder)))). % 4.69/2.14 tff(c_366, plain, (![X_37]: (value(out(s, X_37), n0) | ~value(in(n2, and1(X_37)), n0) | ~value(in(n1, and1(X_37)), n0) | ~type(and1(X_37), or) | ~mode(and1(X_37), ok) | ~type(X_37, halfadder)))). % 4.69/2.14 tff(c_376, plain, (![X_37]: (value(out(s, X_37), n1) | ~value(in(n2, and1(X_37)), n1) | ~value(in(n1, and1(X_37)), n1) | ~type(and1(X_37), and) | ~mode(and1(X_37), ok) | ~type(X_37, halfadder)))). % 4.69/2.14 tff(c_367, plain, (![X_52]: (value(out(c, X_52), n0) | ~value(in(n2, or1(X_52)), n0) | ~value(in(n1, or1(X_52)), n0) | ~type(or1(X_52), or) | ~mode(or1(X_52), ok) | ~type(X_52, fulladder)))). % 4.69/2.14 tff(c_375, plain, (![X_38]: (value(out(c, X_38), n1) | ~value(in(n2, and2(X_38)), n1) | ~value(in(n1, and2(X_38)), n1) | ~type(and2(X_38), and) | ~mode(and2(X_38), ok) | ~type(X_38, halfadder)))). % 4.69/2.14 tff(c_297, plain, (![V1_8, K_116]: (equal_value(V1_8, n0) | ~value(out(n1, K_116), V1_8) | ~value(in(n2, K_116), n0) | ~value(in(n1, K_116), n0) | ~type(K_116, or) | ~mode(K_116, ok)))). % 4.69/2.14 tff(c_298, plain, (![P2_2, K_116]: (value(P2_2, n0) | ~connection(out(n1, K_116), P2_2) | ~value(in(n2, K_116), n0) | ~value(in(n1, K_116), n0) | ~type(K_116, or) | ~mode(K_116, ok)))). % 4.69/2.14 tff(c_339, plain, (![P2_2, K_119]: (value(P2_2, n1) | ~connection(out(n1, K_119), P2_2) | ~value(in(n2, K_119), n1) | ~value(in(n1, K_119), n1) | ~type(K_119, and) | ~mode(K_119, ok)))). % 4.69/2.14 tff(c_337, plain, (![P1_4, K_119]: (value(P1_4, n1) | ~connection(P1_4, out(n1, K_119)) | ~value(in(n2, K_119), n1) | ~value(in(n1, K_119), n1) | ~type(K_119, and) | ~mode(K_119, ok)))). % 4.69/2.14 tff(c_296, plain, (![P1_4, K_116]: (value(P1_4, n0) | ~connection(P1_4, out(n1, K_116)) | ~value(in(n2, K_116), n0) | ~value(in(n1, K_116), n0) | ~type(K_116, or) | ~mode(K_116, ok)))). % 4.69/2.14 tff(c_338, plain, (![V1_8, K_119]: (equal_value(V1_8, n1) | ~value(out(n1, K_119), V1_8) | ~value(in(n2, K_119), n1) | ~value(in(n1, K_119), n1) | ~type(K_119, and) | ~mode(K_119, ok)))). % 4.69/2.14 tff(c_20, plain, (![K_16]: (value(in(n2, K_16), n0) | value(in(n1, K_16), n0) | ~value(out(n1, K_16), n0) | ~type(K_16, and) | ~mode(K_16, ok)))). % 4.69/2.14 tff(c_340, plain, (![K_26]: (~value(in(n1, K_26), n1) | ~type(K_26, not) | ~mode(K_26, ok)))). % 4.69/2.14 tff(c_18, plain, (![K_15]: (value(out(n1, K_15), n1) | ~value(in(n2, K_15), n1) | ~value(in(n1, K_15), n1) | ~type(K_15, and) | ~mode(K_15, ok)))). % 4.69/2.14 tff(c_28, plain, (![K_21]: (value(out(n1, K_21), n0) | ~value(in(n2, K_21), n0) | ~value(in(n1, K_21), n0) | ~type(K_21, or) | ~mode(K_21, ok)))). % 4.69/2.14 tff(c_275, plain, (![K_25]: (~value(in(n1, K_25), n0) | ~type(K_25, not) | ~mode(K_25, ok)))). % 4.69/2.14 tff(c_30, plain, (![K_22]: (value(in(n2, K_22), n1) | value(in(n1, K_22), n1) | ~value(out(n1, K_22), n1) | ~type(K_22, or) | ~mode(K_22, ok)))). % 4.69/2.15 tff(c_26, plain, (![K_19, Any_20]: (value(out(n1, K_19), n1) | ~value(in(Any_20, K_19), n1) | ~type(K_19, or) | ~mode(K_19, ok)))). % 4.69/2.15 tff(c_34, plain, (![K_24]: (value(in(n2, K_24), n0) | ~value(out(n1, K_24), n0) | ~type(K_24, or) | ~mode(K_24, ok)))). % 4.69/2.15 tff(c_42, plain, (![K_28]: (value(in(n1, K_28), n0) | ~value(out(n1, K_28), n1) | ~type(K_28, not) | ~mode(K_28, ok)))). % 4.69/2.15 tff(c_16, plain, (![K_13, Any_14]: (value(out(n1, K_13), n0) | ~value(in(Any_14, K_13), n0) | ~type(K_13, and) | ~mode(K_13, ok)))). % 4.69/2.15 tff(c_32, plain, (![K_23]: (value(in(n1, K_23), n0) | ~value(out(n1, K_23), n0) | ~type(K_23, or) | ~mode(K_23, ok)))). % 4.69/2.15 tff(c_24, plain, (![K_18]: (value(in(n2, K_18), n1) | ~value(out(n1, K_18), n1) | ~type(K_18, and) | ~mode(K_18, ok)))). % 4.69/2.15 tff(c_22, plain, (![K_17]: (value(in(n1, K_17), n1) | ~value(out(n1, K_17), n1) | ~type(K_17, and) | ~mode(K_17, ok)))). % 4.69/2.15 tff(c_40, plain, (![K_27]: (value(in(n1, K_27), n1) | ~value(out(n1, K_27), n0) | ~type(K_27, not) | ~mode(K_27, ok)))). % 4.69/2.15 tff(c_76, plain, (![X_45]: (connection(out(s, h1(X_45)), in(n2, h2(X_45))) | ~type(X_45, fulladder)))). % 4.69/2.15 tff(c_66, plain, (![X_40]: (connection(out(n1, and2(X_40)), in(n1, not1(X_40))) | ~type(X_40, halfadder)))). % 4.69/2.15 tff(c_68, plain, (![X_41]: (connection(out(n1, not1(X_41)), in(n2, and1(X_41))) | ~type(X_41, halfadder)))). % 4.69/2.15 tff(c_78, plain, (![X_46]: (connection(out(c, h1(X_46)), in(n2, or1(X_46))) | ~type(X_46, fulladder)))). % 4.69/2.15 tff(c_124, plain, (![X_29]: (mode(and1(X_29), abnormal) | mode(and1(X_29), ok) | ~type(X_29, halfadder)))). % 4.69/2.15 tff(c_123, plain, (![X_30]: (mode(and2(X_30), abnormal) | mode(and2(X_30), ok) | ~type(X_30, halfadder)))). % 4.69/2.15 tff(c_125, plain, (![X_32]: (mode(or1(X_32), abnormal) | mode(or1(X_32), ok) | ~type(X_32, halfadder)))). % 4.69/2.15 tff(c_126, plain, (![X_42]: (mode(h1(X_42), abnormal) | mode(h1(X_42), ok) | ~type(X_42, fulladder)))). % 4.69/2.15 tff(c_80, plain, (![X_47]: (connection(out(c, h2(X_47)), in(n1, or1(X_47))) | ~type(X_47, fulladder)))). % 4.69/2.15 tff(c_127, plain, (![X_44]: (mode(or1(X_44), abnormal) | mode(or1(X_44), ok) | ~type(X_44, fulladder)))). % 4.69/2.15 tff(c_121, plain, (![X_43]: (mode(h2(X_43), abnormal) | mode(h2(X_43), ok) | ~type(X_43, fulladder)))). % 4.69/2.15 tff(c_122, plain, (![X_31]: (mode(not1(X_31), abnormal) | mode(not1(X_31), ok) | ~type(X_31, halfadder)))). % 4.69/2.15 tff(c_64, plain, (![X_39]: (connection(out(n1, or1(X_39)), in(n1, and1(X_39))) | ~type(X_39, halfadder)))). % 4.69/2.15 tff(c_62, plain, (![X_38]: (connection(out(c, X_38), out(n1, and2(X_38))) | ~type(X_38, halfadder)))). % 4.69/2.15 tff(c_60, plain, (![X_37]: (connection(out(s, X_37), out(n1, and1(X_37))) | ~type(X_37, halfadder)))). % 4.69/2.15 tff(c_86, plain, (![X_50]: (connection(in(c, X_50), in(n2, h1(X_50))) | ~type(X_50, fulladder)))). % 4.69/2.15 tff(c_90, plain, (![X_52]: (connection(out(c, X_52), out(n1, or1(X_52))) | ~type(X_52, fulladder)))). % 4.69/2.15 tff(c_56, plain, (![X_35]: (connection(in(n1, X_35), in(n1, and2(X_35))) | ~type(X_35, halfadder)))). % 4.69/2.15 tff(c_84, plain, (![X_49]: (connection(in(n2, X_49), in(n1, h1(X_49))) | ~type(X_49, fulladder)))). % 4.69/2.15 tff(c_82, plain, (![X_48]: (connection(in(n1, X_48), in(n1, h2(X_48))) | ~type(X_48, fulladder)))). % 4.69/2.15 tff(c_54, plain, (![X_34]: (connection(in(n2, X_34), in(n2, or1(X_34))) | ~type(X_34, halfadder)))). % 4.69/2.15 tff(c_52, plain, (![X_33]: (connection(in(n1, X_33), in(n1, or1(X_33))) | ~type(X_33, halfadder)))). % 4.69/2.15 tff(c_88, plain, (![X_51]: (connection(out(s, X_51), out(s, h2(X_51))) | ~type(X_51, fulladder)))). % 4.69/2.15 tff(c_58, plain, (![X_36]: (connection(in(n2, X_36), in(n2, and2(X_36))) | ~type(X_36, halfadder)))). % 4.69/2.15 tff(c_4, plain, (![P1_4, V_6, P2_5]: (value(P1_4, V_6) | ~value(P2_5, V_6) | ~connection(P1_4, P2_5)))). % 4.69/2.15 tff(c_6, plain, (![V1_8, V2_9, P_7]: (equal_value(V1_8, V2_9) | ~value(P_7, V2_9) | ~value(P_7, V1_8)))). % 4.69/2.15 tff(c_2, plain, (![P2_2, V_3, P1_1]: (value(P2_2, V_3) | ~value(P1_1, V_3) | ~connection(P1_1, P2_2)))). % 4.69/2.15 tff(c_14, plain, (![K_11, Any_12]: (mode(K_11, abnormal) | mode(K_11, ok) | ~type(K_11, Any_12)))). % 4.69/2.15 tff(c_72, plain, (![X_43]: (type(h2(X_43), halfadder) | ~type(X_43, fulladder)))). % 4.69/2.15 tff(c_48, plain, (![X_31]: (type(not1(X_31), not) | ~type(X_31, halfadder)))). % 4.69/2.15 tff(c_46, plain, (![X_30]: (type(and2(X_30), and) | ~type(X_30, halfadder)))). % 4.69/2.15 tff(c_44, plain, (![X_29]: (type(and1(X_29), and) | ~type(X_29, halfadder)))). % 4.69/2.15 tff(c_50, plain, (![X_32]: (type(or1(X_32), or) | ~type(X_32, halfadder)))). % 4.69/2.15 tff(c_70, plain, (![X_42]: (type(h1(X_42), halfadder) | ~type(X_42, fulladder)))). % 4.69/2.15 tff(c_74, plain, (![X_44]: (type(or1(X_44), or) | ~type(X_44, fulladder)))). % 4.69/2.15 tff(c_12, plain, (![K_10]: (~mode(K_10, abnormal) | ~mode(K_10, ok)))). % 4.69/2.15 tff(c_8, plain, (~equal_value(n0, n1))). % 4.69/2.15 tff(c_10, plain, (~equal_value(n1, n0))). % 4.69/2.15 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 4.69/2.15 %------------------------------------------------------------------------------