%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN529+1 : TPTP v9.0.0. Released v2.1.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 : n012.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 10:03:49 PM UTC 2025 % Result : CounterSatisfiable 6.64s 2.45s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SYN529+1 : TPTP v9.0.0. Released v2.1.0. % 0.11/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.35 % Computer : n012.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Wed Apr 9 07:55:59 EDT 2025 % 0.13/0.35 % CPUTime : % 6.64/2.45 % 6.64/2.45 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.64/2.45 % 6.64/2.45 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.64/2.46 %$ c5_2 > c4_2 > c3_2 > c2_2 > c1_2 > ndr1_1 > c5_1 > c4_1 > c3_1 > c2_1 > c1_1 > #nlpp > ndr1_0 > c5_0 > c4_0 > c3_0 > c2_0 > c1_0 > a356 > a355 > a354 > a353 > a352 > a351 > a350 > a349 > a348 > a347 > a346 > a345 > a344 > a343 > a342 > a341 > a340 > a339 > a338 > a337 > a336 > a335 > a334 > a333 > a332 > a331 > a330 > a329 > a328 > a327 > a326 > a325 > a324 > a323 > a322 > a321 > a320 > a319 > a318 > a317 > a316 > a315 > a314 % 6.64/2.46 % 6.64/2.46 %Foreground sorts: % 6.64/2.46 % 6.64/2.46 % 6.64/2.46 %Background operators: % 6.64/2.46 % 6.64/2.46 % 6.64/2.46 %Foreground operators: % 6.64/2.46 tff(a323, type, a323: $i). % 6.64/2.46 tff(a316, type, a316: $i). % 6.64/2.46 tff(a347, type, a347: $i). % 6.64/2.46 tff(a322, type, a322: $i). % 6.64/2.46 tff(a336, type, a336: $i). % 6.64/2.46 tff(c4_0, type, c4_0: $o). % 6.64/2.46 tff(a335, type, a335: $i). % 6.64/2.46 tff(a326, type, a326: $i). % 6.64/2.46 tff(c3_0, type, c3_0: $o). % 6.64/2.46 tff(a338, type, a338: $i). % 6.64/2.46 tff(c1_2, type, c1_2: ($i * $i) > $o). % 6.64/2.46 tff(a334, type, a334: $i). % 6.64/2.46 tff(a337, type, a337: $i). % 6.64/2.46 tff(a320, type, a320: $i). % 6.64/2.46 tff(a354, type, a354: $i). % 6.64/2.46 tff(a348, type, a348: $i). % 6.64/2.46 tff(a341, type, a341: $i). % 6.64/2.46 tff(a342, type, a342: $i). % 6.64/2.46 tff(a355, type, a355: $i). % 6.64/2.46 tff(a330, type, a330: $i). % 6.64/2.46 tff(a314, type, a314: $i). % 6.64/2.46 tff(a321, type, a321: $i). % 6.64/2.46 tff(a318, type, a318: $i). % 6.64/2.46 tff(c5_0, type, c5_0: $o). % 6.64/2.46 tff(a329, type, a329: $i). % 6.64/2.46 tff(a353, type, a353: $i). % 6.64/2.46 tff(a343, type, a343: $i). % 6.64/2.46 tff(c1_0, type, c1_0: $o). % 6.64/2.46 tff(a331, type, a331: $i). % 6.64/2.46 tff(c2_1, type, c2_1: $i > $o). % 6.64/2.46 tff(ndr1_1, type, ndr1_1: $i > $o). % 6.64/2.46 tff(c2_0, type, c2_0: $o). % 6.64/2.46 tff(c4_1, type, c4_1: $i > $o). % 6.64/2.46 tff(a333, type, a333: $i). % 6.64/2.46 tff(a345, type, a345: $i). % 6.64/2.46 tff(a352, type, a352: $i). % 6.64/2.46 tff(a327, type, a327: $i). % 6.64/2.46 tff(ndr1_0, type, ndr1_0: $o). % 6.64/2.46 tff(a344, type, a344: $i). % 6.64/2.46 tff(a351, type, a351: $i). % 6.64/2.46 tff(a317, type, a317: $i). % 6.64/2.46 tff(a349, type, a349: $i). % 6.64/2.46 tff(a324, type, a324: $i). % 6.64/2.46 tff(c1_1, type, c1_1: $i > $o). % 6.64/2.46 tff(c5_2, type, c5_2: ($i * $i) > $o). % 6.64/2.46 tff(a340, type, a340: $i). % 6.64/2.46 tff(a315, type, a315: $i). % 6.64/2.46 tff(c4_2, type, c4_2: ($i * $i) > $o). % 6.64/2.46 tff(a319, type, a319: $i). % 6.64/2.46 tff(a328, type, a328: $i). % 6.64/2.46 tff(a332, type, a332: $i). % 6.64/2.46 tff(c5_1, type, c5_1: $i > $o). % 6.64/2.46 tff(a346, type, a346: $i). % 6.64/2.46 tff(c3_2, type, c3_2: ($i * $i) > $o). % 6.64/2.46 tff(a350, type, a350: $i). % 6.64/2.46 tff(c2_2, type, c2_2: ($i * $i) > $o). % 6.64/2.46 tff(a325, type, a325: $i). % 6.64/2.46 tff(a339, type, a339: $i). % 6.64/2.46 tff(a356, type, a356: $i). % 6.64/2.46 tff(c3_1, type, c3_1: $i > $o). % 6.64/2.46 % 6.64/2.46 %Saturated clause set: % 6.64/2.46 tff(c_1259, plain, (![X15_26, X16_28]: (~c3_2(X15_26, a350) | c5_2(X15_26, X16_28) | ~c4_2(X15_26, X16_28) | c1_2(X15_26, X16_28) | ~ndr1_1(X15_26) | ~c3_1(X15_26)))). % 6.64/2.46 tff(c_1272, plain, (~c4_1(a322))). % 6.64/2.46 tff(c_1263, plain, (![V_2, W_4]: (c5_1(V_2) | ~c4_1(V_2) | c1_2(V_2, W_4) | c3_2(V_2, W_4) | c4_2(V_2, W_4) | ~ndr1_1(V_2)))). % 6.64/2.46 tff(c_1237, plain, (![X15_26, X16_28]: (c2_2(X15_26, a350) | c5_2(X15_26, X16_28) | ~c4_2(X15_26, X16_28) | c1_2(X15_26, X16_28) | ~ndr1_1(X15_26) | ~c3_1(X15_26)))). % 6.64/2.46 tff(c_1234, plain, (~c3_1(a326))). % 6.64/2.46 tff(c_1214, plain, (![X15_26, X16_28]: (~c1_2(X15_26, a350) | c5_2(X15_26, X16_28) | ~c4_2(X15_26, X16_28) | c1_2(X15_26, X16_28) | ~ndr1_1(X15_26) | ~c3_1(X15_26)))). % 6.64/2.46 tff(c_1099, plain, (![Z_8]: (c5_1(Z_8) | c1_1(Z_8)))). % 6.64/2.47 tff(c_1096, plain, (~c1_2(a322, a323))). % 6.64/2.47 tff(c_1079, plain, (~c4_2(a322, a323))). % 6.64/2.47 tff(c_1071, plain, (c5_2(a322, a323))). % 6.64/2.47 tff(c_1058, plain, (~c3_2(a314, a315))). % 6.64/2.47 tff(c_1050, plain, (~c2_2(a314, a315))). % 6.64/2.47 tff(c_1037, plain, (c3_1(a322))). % 6.64/2.47 tff(c_1033, plain, (~c1_2(a314, a315))). % 6.64/2.47 tff(c_1029, plain, (~c5_2(a348, a349))). % 6.64/2.47 tff(c_1026, plain, (ndr1_1(a322))). % 6.64/2.47 tff(c_1020, plain, (c2_2(a348, a349))). % 6.64/2.47 tff(c_1015, plain, (c4_1(a314))). % 6.64/2.47 tff(c_1005, plain, (ndr1_1(a348))). % 6.64/2.47 tff(c_1002, plain, (ndr1_1(a314))). % 6.64/2.47 tff(c_998, plain, (~c3_1(a348))). % 6.64/2.47 tff(c_994, plain, (![X11_21, X12_23]: (~c2_1(X11_21) | c3_1(X11_21) | c2_2(X11_21, X12_23) | c3_2(X11_21, X12_23) | c4_2(X11_21, X12_23) | ~ndr1_1(X11_21)))). % 6.64/2.47 tff(c_962, plain, (c5_1(a328))). % 6.64/2.47 tff(c_936, plain, (![X10_20]: (c2_2(X10_20, a342) | c5_1(X10_20) | ~c4_1(X10_20)))). % 6.64/2.47 tff(c_932, plain, (![X10_20]: (c5_2(X10_20, a342) | c5_1(X10_20) | ~c4_1(X10_20)))). % 6.64/2.47 tff(c_928, plain, (![X10_20]: (ndr1_1(X10_20) | c5_1(X10_20) | ~c4_1(X10_20)))). % 6.64/2.47 tff(c_925, plain, (c1_0)). % 6.64/2.47 tff(c_900, plain, (c1_2(a346, a347))). % 6.64/2.47 tff(c_894, plain, (~c2_2(a329, a330))). % 6.64/2.47 tff(c_889, plain, (~c5_2(a346, a347))). % 6.64/2.47 tff(c_882, plain, (c3_2(a326, a327))). % 6.64/2.47 tff(c_866, plain, (~c5_2(a326, a327))). % 6.64/2.47 tff(c_864, plain, (~c2_2(a326, a327))). % 6.64/2.47 tff(c_852, plain, (c2_1(a326))). % 6.64/2.47 tff(c_850, plain, (ndr1_1(a346))). % 6.64/2.47 tff(c_848, plain, (c4_1(a326))). % 6.64/2.47 tff(c_843, plain, (c4_2(a335, a336))). % 6.64/2.47 tff(c_842, plain, (c3_1(a346))). % 6.64/2.47 tff(c_840, plain, (c5_2(a335, a337))). % 6.64/2.47 tff(c_839, plain, (c1_2(a335, a337))). % 6.64/2.47 tff(c_838, plain, (~c3_2(a335, a337))). % 6.64/2.47 tff(c_837, plain, (c5_2(a335, a336))). % 6.64/2.47 tff(c_836, plain, (c1_1(a329))). % 6.64/2.47 tff(c_833, plain, (c4_1(a346))). % 6.64/2.47 tff(c_831, plain, (~c2_1(a344))). % 6.64/2.47 tff(c_828, plain, (c2_2(a335, a336))). % 6.64/2.47 tff(c_826, plain, (ndr1_1(a329))). % 6.64/2.47 tff(c_824, plain, (~c2_1(a328))). % 6.64/2.47 tff(c_820, plain, (ndr1_1(a326))). % 6.64/2.47 tff(c_812, plain, (ndr1_1(a335))). % 6.64/2.47 tff(c_804, plain, (~c5_0)). % 6.64/2.47 tff(c_800, plain, (c2_0)). % 6.64/2.47 tff(c_797, plain, (ndr1_0)). % 6.64/2.47 tff(c_796, plain, (c3_0)). % 6.64/2.47 tff(c_795, plain, (~c4_0)). % 6.64/2.47 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 6.64/2.47 %------------------------------------------------------------------------------