%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : HWV035-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 : n014.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.42s 2.07s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : HWV035-1 : TPTP v9.0.0. Released v2.5.0. % 0.10/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 : n014.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:19 EDT 2025 % 0.13/0.34 % CPUTime : % 4.42/2.07 % 4.42/2.07 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.42/2.07 % 4.42/2.07 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.42/2.08 %$ value > type > mode > equal_value > connection > out > in > #nlpp > or1 > not1 > and2 > and1 > s > or > ok > not > n2 > n1 > n0 > halfadder > c > and > abnormal % 4.42/2.08 % 4.42/2.08 %Foreground sorts: % 4.42/2.08 % 4.42/2.08 % 4.42/2.08 %Background operators: % 4.42/2.08 % 4.42/2.08 % 4.42/2.08 %Foreground operators: % 4.42/2.08 tff(or, type, or: $i). % 4.42/2.08 tff(and, type, and: $i). % 4.42/2.08 tff(not, type, not: $i). % 4.42/2.08 tff(or1, type, or1: $i > $i). % 4.42/2.08 tff(in, type, in: ($i * $i) > $i). % 4.42/2.08 tff(connection, type, connection: ($i * $i) > $o). % 4.42/2.08 tff(s, type, s: $i). % 4.42/2.08 tff(halfadder, type, halfadder: $i). % 4.42/2.08 tff(and2, type, and2: $i > $i). % 4.42/2.08 tff(equal_value, type, equal_value: ($i * $i) > $o). % 4.42/2.08 tff(n1, type, n1: $i). % 4.42/2.08 tff(n0, type, n0: $i). % 4.42/2.08 tff(type, type, type: ($i * $i) > $o). % 4.42/2.08 tff(value, type, value: ($i * $i) > $o). % 4.42/2.08 tff(not1, type, not1: $i > $i). % 4.42/2.08 tff(and1, type, and1: $i > $i). % 4.42/2.08 tff(abnormal, type, abnormal: $i). % 4.42/2.08 tff(n2, type, n2: $i). % 4.42/2.08 tff(out, type, out: ($i * $i) > $i). % 4.42/2.08 tff(mode, type, mode: ($i * $i) > $o). % 4.42/2.08 tff(ok, type, ok: $i). % 4.42/2.08 tff(c, type, c: $i). % 4.42/2.08 % 4.42/2.08 %Saturated clause set: % 4.50/2.08 tff(c_361, 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.50/2.08 tff(c_323, 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.50/2.08 tff(c_352, 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.50/2.08 tff(c_322, 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.50/2.08 tff(c_362, 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.50/2.08 tff(c_324, 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.50/2.08 tff(c_363, 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.50/2.08 tff(c_369, 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.50/2.09 tff(c_370, 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.50/2.09 tff(c_330, 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.50/2.09 tff(c_331, 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.50/2.09 tff(c_270, plain, (![P1_4, K_95]: (value(P1_4, n1) | ~connection(P1_4, out(n1, K_95)) | ~value(in(n2, K_95), n1) | ~value(in(n1, K_95), n1) | ~type(K_95, and) | ~mode(K_95, ok)))). % 4.50/2.09 tff(c_271, plain, (![P2_2, K_95]: (value(P2_2, n1) | ~connection(out(n1, K_95), P2_2) | ~value(in(n2, K_95), n1) | ~value(in(n1, K_95), n1) | ~type(K_95, and) | ~mode(K_95, ok)))). % 4.50/2.09 tff(c_269, plain, (![V1_8, K_95]: (equal_value(V1_8, n1) | ~value(out(n1, K_95), V1_8) | ~value(in(n2, K_95), n1) | ~value(in(n1, K_95), n1) | ~type(K_95, and) | ~mode(K_95, ok)))). % 4.50/2.09 tff(c_311, plain, (![V1_8, K_98]: (equal_value(V1_8, n0) | ~value(out(n1, K_98), V1_8) | ~value(in(n2, K_98), n0) | ~value(in(n1, K_98), n0) | ~type(K_98, or) | ~mode(K_98, ok)))). % 4.50/2.09 tff(c_312, plain, (![P1_4, K_98]: (value(P1_4, n0) | ~connection(P1_4, out(n1, K_98)) | ~value(in(n2, K_98), n0) | ~value(in(n1, K_98), n0) | ~type(K_98, or) | ~mode(K_98, ok)))). % 4.50/2.09 tff(c_313, plain, (![P2_2, K_98]: (value(P2_2, n0) | ~connection(out(n1, K_98), P2_2) | ~value(in(n2, K_98), n0) | ~value(in(n1, K_98), n0) | ~type(K_98, or) | ~mode(K_98, ok)))). % 4.50/2.09 tff(c_283, plain, (![K_26]: (~value(in(n1, K_26), n1) | ~type(K_26, not) | ~mode(K_26, ok)))). % 4.50/2.09 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.50/2.09 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.50/2.09 tff(c_244, plain, (![K_25]: (~value(in(n1, K_25), n0) | ~type(K_25, not) | ~mode(K_25, ok)))). % 4.50/2.09 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.50/2.09 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.50/2.09 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.50/2.09 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.50/2.09 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.50/2.09 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.50/2.09 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.50/2.09 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.50/2.09 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.50/2.09 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.50/2.09 tff(c_66, plain, (![X_40]: (connection(out(n1, and2(X_40)), in(n1, not1(X_40))) | ~type(X_40, halfadder)))). % 4.50/2.09 tff(c_68, plain, (![X_41]: (connection(out(n1, not1(X_41)), in(n2, and1(X_41))) | ~type(X_41, halfadder)))). % 4.50/2.09 tff(c_90, plain, (![X_31]: (mode(not1(X_31), abnormal) | mode(not1(X_31), ok) | ~type(X_31, halfadder)))). % 4.50/2.09 tff(c_89, plain, (![X_29]: (mode(and1(X_29), abnormal) | mode(and1(X_29), ok) | ~type(X_29, halfadder)))). % 4.50/2.09 tff(c_64, plain, (![X_39]: (connection(out(n1, or1(X_39)), in(n1, and1(X_39))) | ~type(X_39, halfadder)))). % 4.50/2.09 tff(c_88, plain, (![X_32]: (mode(or1(X_32), abnormal) | mode(or1(X_32), ok) | ~type(X_32, halfadder)))). % 4.50/2.09 tff(c_87, plain, (![X_30]: (mode(and2(X_30), abnormal) | mode(and2(X_30), ok) | ~type(X_30, halfadder)))). % 4.50/2.09 tff(c_58, plain, (![X_36]: (connection(in(n2, X_36), in(n2, and2(X_36))) | ~type(X_36, halfadder)))). % 4.50/2.09 tff(c_60, plain, (![X_37]: (connection(out(s, X_37), out(n1, and1(X_37))) | ~type(X_37, halfadder)))). % 4.50/2.09 tff(c_62, plain, (![X_38]: (connection(out(c, X_38), out(n1, and2(X_38))) | ~type(X_38, halfadder)))). % 4.50/2.09 tff(c_52, plain, (![X_33]: (connection(in(n1, X_33), in(n1, or1(X_33))) | ~type(X_33, halfadder)))). % 4.50/2.09 tff(c_56, plain, (![X_35]: (connection(in(n1, X_35), in(n1, and2(X_35))) | ~type(X_35, halfadder)))). % 4.50/2.09 tff(c_54, plain, (![X_34]: (connection(in(n2, X_34), in(n2, or1(X_34))) | ~type(X_34, halfadder)))). % 4.50/2.10 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.50/2.10 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.50/2.10 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.50/2.10 tff(c_14, plain, (![K_11, Any_12]: (mode(K_11, abnormal) | mode(K_11, ok) | ~type(K_11, Any_12)))). % 4.50/2.10 tff(c_46, plain, (![X_30]: (type(and2(X_30), and) | ~type(X_30, halfadder)))). % 4.50/2.10 tff(c_50, plain, (![X_32]: (type(or1(X_32), or) | ~type(X_32, halfadder)))). % 4.50/2.10 tff(c_44, plain, (![X_29]: (type(and1(X_29), and) | ~type(X_29, halfadder)))). % 4.50/2.10 tff(c_48, plain, (![X_31]: (type(not1(X_31), not) | ~type(X_31, halfadder)))). % 4.50/2.10 tff(c_12, plain, (![K_10]: (~mode(K_10, abnormal) | ~mode(K_10, ok)))). % 4.50/2.10 tff(c_8, plain, (~equal_value(n0, n1))). % 4.50/2.10 tff(c_10, plain, (~equal_value(n1, n0))). % 4.50/2.10 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 4.50/2.10 %------------------------------------------------------------------------------