%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : HWV034-2 : TPTP v9.0.0. Bugfixed v2.7.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 : n032.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:51 PM UTC 2025 % Result : Satisfiable 3.47s 1.84s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.09 % Problem : HWV034-2 : TPTP v9.0.0. Bugfixed v2.7.0. % 0.02/0.09 % 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.08/0.28 % Computer : n032.cluster.edu % 0.08/0.28 % Model : x86_64 x86_64 % 0.08/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.28 % Memory : 8042.1875MB % 0.08/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.08/0.28 % CPULimit : 300 % 0.08/0.28 % WCLimit : 300 % 0.08/0.28 % DateTime : Mon Apr 7 22:58:16 EDT 2025 % 0.08/0.28 % CPUTime : % 3.47/1.84 % 3.47/1.84 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.47/1.84 % 3.47/1.84 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.47/1.85 %$ connection > zero > or_ok > one > not_ok > logic_or > logic_not > logic_and > and_ok > abnormal > #nlpp > out1 > in2 > in1 % 3.47/1.85 % 3.47/1.85 %Foreground sorts: % 3.47/1.85 % 3.47/1.85 % 3.47/1.85 %Background operators: % 3.47/1.85 % 3.47/1.85 % 3.47/1.85 %Foreground operators: % 3.47/1.85 tff(not_ok, type, not_ok: $i > $o). % 3.47/1.85 tff(connection, type, connection: ($i * $i) > $o). % 3.47/1.85 tff(or_ok, type, or_ok: $i > $o). % 3.47/1.85 tff(in1, type, in1: $i > $i). % 3.47/1.85 tff(in2, type, in2: $i > $i). % 3.47/1.85 tff(logic_and, type, logic_and: $i > $o). % 3.47/1.85 tff(out1, type, out1: $i > $i). % 3.47/1.85 tff(logic_not, type, logic_not: $i > $o). % 3.47/1.85 tff(and_ok, type, and_ok: $i > $o). % 3.47/1.85 tff(abnormal, type, abnormal: $i > $o). % 3.47/1.85 tff(one, type, one: $i > $o). % 3.47/1.85 tff(zero, type, zero: $i > $o). % 3.47/1.85 tff(logic_or, type, logic_or: $i > $o). % 3.47/1.85 % 3.47/1.85 %Saturated clause set: % 3.47/1.85 tff(c_225, plain, (![K_27]: (zero(in2(K_27)) | zero(in1(K_27)) | ~and_ok(K_27) | ~one(in1(K_27)) | ~not_ok(K_27)))). % 3.47/1.85 tff(c_260, plain, (![K_72]: (one(in1(K_72)) | ~not_ok(K_72) | ~zero(in2(K_72)) | ~zero(in1(K_72)) | ~or_ok(K_72)))). % 3.47/1.85 tff(c_263, plain, (![K_72]: (~one(out1(K_72)) | ~zero(in2(K_72)) | ~zero(in1(K_72)) | ~or_ok(K_72)))). % 3.47/1.85 tff(c_281, plain, (![K_74]: (~one(in2(K_74)) | ~or_ok(K_74) | ~zero(in1(K_74)) | ~and_ok(K_74)))). % 3.47/1.85 tff(c_178, plain, (![K_61]: (~not_ok(K_61) | ~one(in2(K_61)) | ~one(in1(K_61)) | ~and_ok(K_61)))). % 3.47/1.85 tff(c_133, plain, (![K_56]: (zero(in2(K_56)) | ~or_ok(K_56) | ~zero(in1(K_56)) | ~and_ok(K_56)))). % 3.47/1.85 tff(c_84, plain, (![K_50]: (zero(in1(K_50)) | ~or_ok(K_50) | ~zero(in2(K_50)) | ~and_ok(K_50)))). % 3.47/1.85 tff(c_32, plain, (![K_20]: (zero(out1(K_20)) | ~zero(in2(K_20)) | ~zero(in1(K_20)) | ~or_ok(K_20)))). % 3.47/1.85 tff(c_98, plain, (![K_52]: (one(in2(K_52)) | ~and_ok(K_52) | ~one(in1(K_52)) | ~or_ok(K_52)))). % 3.47/1.85 tff(c_132, plain, (![K_56]: (one(in1(K_56)) | ~not_ok(K_56) | ~zero(in1(K_56)) | ~and_ok(K_56)))). % 3.47/1.85 tff(c_118, plain, (![K_11]: (one(in1(K_11)) | ~not_ok(K_11) | ~zero(in2(K_11)) | ~and_ok(K_11)))). % 3.47/1.85 tff(c_18, plain, (![K_13]: (zero(in2(K_13)) | zero(in1(K_13)) | ~zero(out1(K_13)) | ~and_ok(K_13)))). % 3.47/1.85 tff(c_108, plain, (![K_53]: (one(in1(K_53)) | ~and_ok(K_53) | ~one(in2(K_53)) | ~or_ok(K_53)))). % 3.47/1.86 tff(c_211, plain, (![K_19]: (~and_ok(K_19) | ~not_ok(K_19) | ~one(in2(K_19)) | ~or_ok(K_19)))). % 3.47/1.86 tff(c_186, plain, (![K_29]: (~and_ok(K_29) | ~one(out1(K_29)) | ~not_ok(K_29)))). % 3.47/1.86 tff(c_34, plain, (![K_21]: (one(in2(K_21)) | one(in1(K_21)) | ~one(out1(K_21)) | ~or_ok(K_21)))). % 3.47/1.86 tff(c_135, plain, (![K_56]: (~one(out1(K_56)) | ~zero(in1(K_56)) | ~and_ok(K_56)))). % 3.47/1.86 tff(c_167, plain, (![K_18]: (~not_ok(K_18) | ~one(in1(K_18)) | ~or_ok(K_18)))). % 3.47/1.86 tff(c_16, plain, (![K_12]: (one(out1(K_12)) | ~one(in2(K_12)) | ~one(in1(K_12)) | ~and_ok(K_12)))). % 3.47/1.86 tff(c_90, plain, (![K_51]: (~one(in1(K_51)) | ~one(out1(K_51)) | ~not_ok(K_51)))). % 3.47/1.86 tff(c_85, plain, (![K_50]: (~one(out1(K_50)) | ~zero(in2(K_50)) | ~and_ok(K_50)))). % 3.47/1.86 tff(c_44, plain, (![K_26]: (one(out1(K_26)) | ~zero(in1(K_26)) | ~not_ok(K_26)))). % 3.47/1.86 tff(c_46, plain, (![K_27]: (zero(out1(K_27)) | ~one(in1(K_27)) | ~not_ok(K_27)))). % 3.47/1.86 tff(c_12, plain, (![K_10]: (zero(out1(K_10)) | ~zero(in1(K_10)) | ~and_ok(K_10)))). % 3.47/1.86 tff(c_48, plain, (![K_28]: (one(in1(K_28)) | ~zero(out1(K_28)) | ~not_ok(K_28)))). % 3.47/1.86 tff(c_38, plain, (![K_23]: (zero(in2(K_23)) | ~zero(out1(K_23)) | ~or_ok(K_23)))). % 3.47/1.86 tff(c_30, plain, (![K_19]: (one(out1(K_19)) | ~one(in2(K_19)) | ~or_ok(K_19)))). % 3.47/1.86 tff(c_28, plain, (![K_18]: (one(out1(K_18)) | ~one(in1(K_18)) | ~or_ok(K_18)))). % 3.47/1.86 tff(c_50, plain, (![K_29]: (zero(in1(K_29)) | ~one(out1(K_29)) | ~not_ok(K_29)))). % 3.47/1.86 tff(c_14, plain, (![K_11]: (zero(out1(K_11)) | ~zero(in2(K_11)) | ~and_ok(K_11)))). % 3.47/1.86 tff(c_22, plain, (![K_15]: (one(in2(K_15)) | ~one(out1(K_15)) | ~and_ok(K_15)))). % 3.47/1.86 tff(c_20, plain, (![K_14]: (one(in1(K_14)) | ~one(out1(K_14)) | ~and_ok(K_14)))). % 3.47/1.86 tff(c_36, plain, (![K_22]: (zero(in1(K_22)) | ~zero(out1(K_22)) | ~or_ok(K_22)))). % 3.47/1.86 tff(c_2, plain, (![P2_2, P1_1]: (zero(P2_2) | ~zero(P1_1) | ~connection(P1_1, P2_2)))). % 3.47/1.86 tff(c_8, plain, (![P1_7, P2_8]: (one(P1_7) | ~one(P2_8) | ~connection(P1_7, P2_8)))). % 3.47/1.86 tff(c_6, plain, (![P1_5, P2_6]: (zero(P1_5) | ~zero(P2_6) | ~connection(P1_5, P2_6)))). % 3.47/1.86 tff(c_4, plain, (![P2_4, P1_3]: (one(P2_4) | ~one(P1_3) | ~connection(P1_3, P2_4)))). % 3.47/1.86 tff(c_26, plain, (![K_17]: (abnormal(K_17) | and_ok(K_17) | ~logic_and(K_17)))). % 3.47/1.86 tff(c_42, plain, (![K_25]: (abnormal(K_25) | or_ok(K_25) | ~logic_or(K_25)))). % 3.47/1.86 tff(c_54, plain, (![K_31]: (abnormal(K_31) | not_ok(K_31) | ~logic_not(K_31)))). % 3.47/1.86 tff(c_10, plain, (![P_9]: (~one(P_9) | ~zero(P_9)))). % 3.47/1.86 tff(c_24, plain, (![K_16]: (~abnormal(K_16) | ~and_ok(K_16)))). % 3.47/1.86 tff(c_40, plain, (![K_24]: (~abnormal(K_24) | ~or_ok(K_24)))). % 3.47/1.86 tff(c_52, plain, (![K_30]: (~abnormal(K_30) | ~not_ok(K_30)))). % 3.47/1.86 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 3.47/1.86 %------------------------------------------------------------------------------