%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SYN435-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/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 : n008.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:34 PM UTC 2025 % Result : Satisfiable 57.71s 44.23s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.13 % Problem : SYN435-1 : TPTP v9.0.0. Released v2.1.0. % 0.13/0.14 % 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.35 % Computer : n008.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:26:47 EDT 2025 % 0.13/0.36 % CPUTime : % 57.71/44.22 % 57.71/44.23 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 57.71/44.23 % 57.71/44.23 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 57.71/44.24 %$ c3_1 > c2_1 > c1_1 > c0_1 > #nlpp > ndr1_0 > hskp9 > hskp8 > hskp7 > hskp6 > hskp52 > hskp51 > hskp50 > hskp5 > hskp49 > hskp48 > hskp47 > hskp46 > hskp45 > hskp44 > hskp43 > hskp42 > hskp41 > hskp40 > hskp4 > hskp39 > hskp38 > hskp37 > hskp36 > hskp35 > hskp34 > hskp33 > hskp32 > hskp31 > hskp30 > hskp3 > hskp29 > hskp28 > hskp27 > hskp26 > hskp25 > hskp24 > hskp23 > hskp22 > hskp21 > hskp20 > hskp2 > hskp19 > hskp18 > hskp17 > hskp16 > hskp15 > hskp14 > hskp13 > hskp12 > hskp11 > hskp10 > hskp1 > hskp0 > a347 > a345 > a344 > a343 > a342 > a340 > a337 > a336 > a335 > a334 > a333 > a331 > a330 > a327 > a326 > a325 > a324 > a322 > a319 > a318 > a317 > a316 > a315 > a313 > a312 > a311 > a310 > a309 > a307 > a306 > a305 > a304 > a303 > a302 > a301 > a300 > a299 > a298 > a297 > a296 > a294 > a293 > a292 > a291 > a290 > a289 > a288 > a287 > a286 > a285 > a284 > a283 > a282 % 57.71/44.24 % 57.71/44.24 %Foreground sorts: % 57.71/44.24 % 57.71/44.24 % 57.71/44.24 %Background operators: % 57.71/44.24 % 57.71/44.24 % 57.71/44.24 %Foreground operators: % 57.71/44.24 tff(hskp50, type, hskp50: $o). % 57.71/44.24 tff(hskp31, type, hskp31: $o). % 57.71/44.24 tff(a316, type, a316: $i). % 57.71/44.24 tff(a347, type, a347: $i). % 57.71/44.24 tff(hskp17, type, hskp17: $o). % 57.71/44.24 tff(a322, type, a322: $i). % 57.71/44.24 tff(a313, type, a313: $i). % 57.71/44.24 tff(a292, type, a292: $i). % 57.71/44.24 tff(hskp19, type, hskp19: $o). % 57.71/44.24 tff(a336, type, a336: $i). % 57.71/44.24 tff(hskp42, type, hskp42: $o). % 57.71/44.24 tff(a335, type, a335: $i). % 57.71/44.24 tff(a326, type, a326: $i). % 57.71/44.24 tff(a297, type, a297: $i). % 57.71/44.24 tff(a290, type, a290: $i). % 57.71/44.24 tff(hskp37, type, hskp37: $o). % 57.71/44.24 tff(hskp44, type, hskp44: $o). % 57.71/44.24 tff(hskp47, type, hskp47: $o). % 57.71/44.24 tff(a334, type, a334: $i). % 57.71/44.24 tff(hskp46, type, hskp46: $o). % 57.71/44.24 tff(a309, type, a309: $i). % 57.71/44.24 tff(a302, type, a302: $i). % 57.71/44.24 tff(hskp6, type, hskp6: $o). % 57.71/44.24 tff(a337, type, a337: $i). % 57.71/44.24 tff(a306, type, a306: $i). % 57.71/44.24 tff(hskp43, type, hskp43: $o). % 57.71/44.24 tff(a301, type, a301: $i). % 57.71/44.24 tff(a284, type, a284: $i). % 57.71/44.24 tff(hskp10, type, hskp10: $o). % 57.71/44.24 tff(a310, type, a310: $i). % 57.71/44.24 tff(a285, type, a285: $i). % 57.71/44.24 tff(hskp23, type, hskp23: $o). % 57.71/44.24 tff(hskp13, type, hskp13: $o). % 57.71/44.24 tff(hskp52, type, hskp52: $o). % 57.71/44.24 tff(a342, type, a342: $i). % 57.71/44.24 tff(hskp32, type, hskp32: $o). % 57.71/44.24 tff(hskp14, type, hskp14: $o). % 57.71/44.24 tff(a311, type, a311: $i). % 57.71/44.24 tff(a286, type, a286: $i). % 57.71/44.24 tff(a330, type, a330: $i). % 57.71/44.24 tff(hskp45, type, hskp45: $o). % 57.71/44.24 tff(a291, type, a291: $i). % 57.71/44.24 tff(hskp18, type, hskp18: $o). % 57.71/44.24 tff(hskp5, type, hskp5: $o). % 57.71/44.24 tff(a283, type, a283: $i). % 57.71/44.24 tff(a293, type, a293: $i). % 57.71/44.24 tff(hskp12, type, hskp12: $o). % 57.71/44.24 tff(a294, type, a294: $i). % 57.71/44.24 tff(a318, type, a318: $i). % 57.71/44.24 tff(hskp29, type, hskp29: $o). % 57.71/44.24 tff(hskp2, type, hskp2: $o). % 57.71/44.24 tff(hskp28, type, hskp28: $o). % 57.71/44.24 tff(hskp1, type, hskp1: $o). % 57.71/44.24 tff(a298, type, a298: $i). % 57.71/44.24 tff(hskp27, type, hskp27: $o). % 57.71/44.24 tff(hskp41, type, hskp41: $o). % 57.71/44.24 tff(a304, type, a304: $i). % 57.71/44.24 tff(a343, type, a343: $i). % 57.71/44.24 tff(hskp33, type, hskp33: $o). % 57.71/44.24 tff(a282, type, a282: $i). % 57.71/44.24 tff(a331, type, a331: $i). % 57.71/44.24 tff(hskp3, type, hskp3: $o). % 57.71/44.24 tff(c2_1, type, c2_1: $i > $o). % 57.71/44.24 tff(hskp4, type, hskp4: $o). % 57.71/44.24 tff(c0_1, type, c0_1: $i > $o). % 57.71/44.24 tff(hskp20, type, hskp20: $o). % 57.71/44.24 tff(a333, type, a333: $i). % 57.71/44.24 tff(hskp36, type, hskp36: $o). % 57.71/44.24 tff(a345, type, a345: $i). % 57.71/44.24 tff(hskp16, type, hskp16: $o). % 57.71/44.24 tff(hskp11, type, hskp11: $o). % 57.71/44.24 tff(a327, type, a327: $i). % 57.71/44.24 tff(hskp30, type, hskp30: $o). % 57.71/44.24 tff(hskp48, type, hskp48: $o). % 57.71/44.24 tff(hskp24, type, hskp24: $o). % 57.71/44.24 tff(hskp51, type, hskp51: $o). % 57.71/44.24 tff(hskp49, type, hskp49: $o). % 57.71/44.24 tff(hskp26, type, hskp26: $o). % 57.71/44.24 tff(a289, type, a289: $i). % 57.71/44.24 tff(ndr1_0, type, ndr1_0: $o). % 57.71/44.24 tff(a288, type, a288: $i). % 57.71/44.24 tff(hskp25, type, hskp25: $o). % 57.71/44.24 tff(a300, type, a300: $i). % 57.71/44.24 tff(a287, type, a287: $i). % 57.71/44.24 tff(a344, type, a344: $i). % 57.71/44.24 tff(hskp22, type, hskp22: $o). % 57.71/44.24 tff(a317, type, a317: $i). % 57.71/44.24 tff(hskp9, type, hskp9: $o). % 57.71/44.24 tff(a324, type, a324: $i). % 57.71/44.24 tff(c1_1, type, c1_1: $i > $o). % 57.71/44.24 tff(a340, type, a340: $i). % 57.71/44.24 tff(a299, type, a299: $i). % 57.71/44.24 tff(hskp39, type, hskp39: $o). % 57.71/44.24 tff(a315, type, a315: $i). % 57.71/44.24 tff(hskp38, type, hskp38: $o). % 57.71/44.24 tff(a319, type, a319: $i). % 57.71/44.24 tff(a296, type, a296: $i). % 57.71/44.24 tff(hskp34, type, hskp34: $o). % 57.71/44.24 tff(a325, type, a325: $i). % 57.71/44.24 tff(hskp8, type, hskp8: $o). % 57.71/44.24 tff(hskp15, type, hskp15: $o). % 57.71/44.24 tff(a305, type, a305: $i). % 57.71/44.24 tff(hskp35, type, hskp35: $o). % 57.71/44.24 tff(a312, type, a312: $i). % 57.71/44.24 tff(hskp0, type, hskp0: $o). % 57.71/44.24 tff(a307, type, a307: $i). % 57.71/44.24 tff(a303, type, a303: $i). % 57.71/44.24 tff(hskp7, type, hskp7: $o). % 57.71/44.24 tff(hskp21, type, hskp21: $o). % 57.71/44.24 tff(c3_1, type, c3_1: $i > $o). % 57.71/44.24 tff(hskp40, type, hskp40: $o). % 57.71/44.24 % 57.71/44.24 %Saturated clause set: % 57.71/44.24 tff(c_364523, plain, (![U_50]: (c0_1(U_50) | ~c3_1(U_50) | ~c2_1(U_50)))). % 57.71/44.24 tff(c_364452, plain, (hskp25)). % 57.71/44.24 tff(c_364433, plain, (~c2_1(a343))). % 57.71/44.24 tff(c_364403, plain, (![U_39]: (~c3_1(U_39) | ~c1_1(U_39) | ~c2_1(U_39)))). % 57.71/44.24 tff(c_364378, plain, (~c0_1(a310))). % 57.71/44.24 tff(c_364387, plain, (~c0_1(a316))). % 57.71/44.24 tff(c_364375, plain, (~c0_1(a306))). % 57.71/44.24 tff(c_364331, plain, (![U_21]: (c3_1(U_21) | c2_1(U_21) | ~c0_1(U_21)))). % 57.71/44.24 tff(c_364327, plain, (~c2_1(a316))). % 57.71/44.24 tff(c_364312, plain, (~c2_1(a292))). % 57.71/44.24 tff(c_364270, plain, (![V_42]: (c3_1(V_42) | c1_1(V_42) | ~c2_1(V_42)))). % 57.71/44.24 tff(c_364231, plain, (hskp26)). % 57.71/44.24 tff(c_364215, plain, (c1_1(a334))). % 57.71/44.24 tff(c_364187, plain, (![U_6]: (c1_1(U_6) | c0_1(U_6) | ~c2_1(U_6)))). % 57.71/44.24 tff(c_364170, plain, (~c0_1(a296))). % 57.71/44.24 tff(c_364173, plain, (~c1_1(a289))). % 57.71/44.24 tff(c_364160, plain, (~c1_1(a287))). % 57.71/44.24 tff(c_364138, plain, (![U_16]: (~c2_1(U_16) | ~c1_1(U_16) | ~c0_1(U_16)))). % 57.71/44.24 tff(c_364132, plain, (hskp10)). % 57.71/44.24 tff(c_364120, plain, (hskp4)). % 57.71/44.25 tff(c_364115, plain, (c0_1(a325))). % 57.71/44.25 tff(c_364081, plain, (~c1_1(a347))). % 57.71/44.25 tff(c_364084, plain, (![U_7]: (c0_1(U_7) | ~c3_1(U_7) | ~c1_1(U_7)))). % 57.71/44.25 tff(c_364080, plain, (c1_1(a343))). % 57.71/44.25 tff(c_364078, plain, (c1_1(a304))). % 57.71/44.25 tff(c_364076, plain, (~hskp24)). % 57.71/44.25 tff(c_364075, plain, (~c2_1(a319))). % 57.71/44.25 tff(c_364073, plain, (~c3_1(a312))). % 57.71/44.25 tff(c_364072, plain, (~c1_1(a322))). % 57.71/44.25 tff(c_364070, plain, (~c2_1(a337))). % 57.71/44.25 tff(c_364069, plain, (~c0_1(a334))). % 57.71/44.25 tff(c_364067, plain, (~c2_1(a347))). % 57.71/44.25 tff(c_364066, plain, (~hskp31)). % 57.71/44.25 tff(c_364065, plain, (c0_1(a289))). % 57.71/44.25 tff(c_364063, plain, (c2_1(a287))). % 57.71/44.25 tff(c_364061, plain, (~c0_1(a312))). % 57.71/44.25 tff(c_364060, plain, (~c0_1(a347))). % 57.71/44.25 tff(c_364059, plain, (~c2_1(a306))). % 57.71/44.25 tff(c_364058, plain, (~hskp3)). % 57.71/44.25 tff(c_364057, plain, (c1_1(a319))). % 57.71/44.25 tff(c_364055, plain, (~hskp39)). % 57.71/44.25 tff(c_364054, plain, (~c1_1(a310))). % 57.71/44.25 tff(c_364053, plain, (c2_1(a297))). % 57.71/44.25 tff(c_364051, plain, (~c2_1(a325))). % 57.71/44.25 tff(c_364049, plain, (~c0_1(a324))). % 57.71/44.25 tff(c_364048, plain, (c2_1(a334))). % 57.71/44.25 tff(c_364045, plain, (c0_1(a304))). % 57.71/44.25 tff(c_364046, plain, (hskp38)). % 57.71/44.25 tff(c_363843, plain, (c2_1(a284))). % 57.71/44.25 tff(c_363841, plain, (c0_1(a343))). % 57.71/44.25 tff(c_363839, plain, (~c2_1(a305))). % 57.71/44.25 tff(c_363838, plain, (~c2_1(a324))). % 57.71/44.25 tff(c_363837, plain, (~c2_1(a312))). % 57.71/44.25 tff(c_363835, plain, (~c0_1(a292))). % 57.71/44.25 tff(c_363834, plain, (~c3_1(a334))). % 57.71/44.25 tff(c_363832, plain, (~c2_1(a318))). % 57.71/44.25 tff(c_363831, plain, (~c3_1(a292))). % 57.71/44.25 tff(c_363830, plain, (~hskp7)). % 57.71/44.25 tff(c_363829, plain, (c0_1(a287))). % 57.71/44.25 tff(c_363827, plain, (~c2_1(a288))). % 57.71/44.25 tff(c_363826, plain, (~hskp15)). % 57.71/44.25 tff(c_363825, plain, (c3_1(a343))). % 57.71/44.25 tff(c_363823, plain, (c0_1(a311))). % 57.71/44.25 tff(c_363821, plain, (~c0_1(a284))). % 57.71/44.25 tff(c_363819, plain, (c3_1(a289))). % 57.71/44.25 tff(c_363814, plain, (c3_1(a287))). % 57.71/44.25 tff(c_363815, plain, (hskp30)). % 57.71/44.25 tff(c_363609, plain, (~c3_1(a306))). % 57.71/44.25 tff(c_363608, plain, (c2_1(a296))). % 57.71/44.25 tff(c_363606, plain, (~hskp29)). % 57.71/44.25 tff(c_363605, plain, (~hskp22)). % 57.71/44.25 tff(c_363604, plain, (~c2_1(a322))). % 57.71/44.25 tff(c_363601, plain, (c0_1(a297))). % 57.71/44.25 tff(c_363602, plain, (hskp6)). % 57.71/44.25 tff(c_360335, plain, (~c1_1(a336))). % 57.71/44.25 tff(c_360334, plain, (~c1_1(a288))). % 57.71/44.25 tff(c_360333, plain, (~c0_1(a318))). % 57.71/44.25 tff(c_360332, plain, (~c1_1(a311))). % 57.71/44.25 tff(c_360329, plain, (c2_1(a289))). % 57.71/44.25 tff(c_360330, plain, (hskp32)). % 57.71/44.25 tff(c_360189, plain, (hskp18)). % 57.71/44.25 tff(c_360188, plain, (~c1_1(a292))). % 57.71/44.25 tff(c_360187, plain, (~hskp9)). % 57.71/44.25 tff(c_360186, plain, (~c2_1(a310))). % 57.71/44.25 tff(c_360185, plain, (~c0_1(a301))). % 57.71/44.25 tff(c_360184, plain, (~hskp21)). % 57.71/44.25 tff(c_360183, plain, (~hskp23)). % 57.71/44.25 tff(c_360182, plain, (~c3_1(a310))). % 57.71/44.25 tff(c_360179, plain, (~c1_1(a297))). % 57.71/44.25 tff(c_360178, plain, (~hskp40)). % 57.71/44.25 tff(c_360177, plain, (~c3_1(a324))). % 57.71/44.25 tff(c_360176, plain, (~hskp8)). % 57.71/44.25 tff(c_360175, plain, (c1_1(a325))). % 57.71/44.25 tff(c_360173, plain, (~c2_1(a326))). % 57.71/44.25 tff(c_360171, plain, (c3_1(a311))). % 57.71/44.25 tff(c_360172, plain, (hskp13)). % 57.71/44.25 tff(c_357667, plain, (~c2_1(a304))). % 57.71/44.25 tff(c_357666, plain, (~c0_1(a327))). % 57.71/44.25 tff(c_357665, plain, (~hskp28)). % 57.71/44.25 tff(c_357664, plain, (~hskp42)). % 57.71/44.26 tff(c_357663, plain, (~hskp37)). % 57.71/44.26 tff(c_357660, plain, (~c3_1(a318))). % 57.71/44.26 tff(c_357662, plain, (~c3_1(a296))). % 57.71/44.26 tff(c_357659, plain, (~c0_1(a337))). % 57.71/44.26 tff(c_357657, plain, (c1_1(a284))). % 57.71/44.26 tff(c_357658, plain, (hskp27)). % 57.71/44.26 tff(c_357158, plain, (~c3_1(a316))). % 57.71/44.26 tff(c_357157, plain, (~hskp52)). % 57.71/44.26 tff(c_357156, plain, (~hskp45)). % 57.71/44.26 tff(c_357155, plain, (~hskp11)). % 57.71/44.26 tff(c_357154, plain, (~hskp36)). % 57.71/44.26 tff(c_357153, plain, (~c1_1(a306))). % 57.71/44.26 tff(c_357152, plain, (~c0_1(a319))). % 57.71/44.26 tff(c_357150, plain, (c1_1(a296))). % 57.71/44.26 tff(c_357151, plain, (hskp34)). % 57.71/44.26 tff(c_340943, plain, (c3_1(a325))). % 57.71/44.26 tff(c_340941, plain, (~c1_1(a326))). % 57.71/44.26 tff(c_340940, plain, (~c2_1(a291))). % 57.71/44.26 tff(c_340939, plain, (hskp46)). % 57.71/44.26 tff(c_340937, plain, (~hskp16)). % 57.71/44.26 tff(c_340935, plain, (c3_1(a322))). % 57.71/44.26 tff(c_340936, plain, (hskp19)). % 57.71/44.26 tff(c_566, plain, (~hskp33)). % 57.71/44.26 tff(c_565, plain, (~c2_1(a309))). % 57.71/44.26 tff(c_564, plain, (~c3_1(a337))). % 57.71/44.26 tff(c_563, plain, (~hskp48)). % 57.71/44.26 tff(c_562, plain, (~c1_1(a305))). % 57.71/44.26 tff(c_561, plain, (~hskp35)). % 57.71/44.26 tff(c_560, plain, (hskp43)). % 57.71/44.26 tff(c_516, plain, (ndr1_0)). % 57.71/44.26 tff(c_514, plain, (~hskp44)). % 57.71/44.26 tff(c_513, plain, (~hskp2)). % 57.71/44.26 tff(c_512, plain, (~hskp47)). % 57.71/44.26 tff(c_511, plain, (~hskp5)). % 57.71/44.26 tff(c_510, plain, (~hskp41)). % 57.71/44.26 tff(c_509, plain, (~hskp49)). % 57.71/44.26 tff(c_508, plain, (hskp50)). % 57.71/44.26 tff(c_507, plain, (~hskp51)). % 57.71/44.26 tff(c_506, plain, (~hskp1)). % 57.71/44.26 tff(c_505, plain, (~hskp0)). % 57.71/44.26 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 57.71/44.26 %------------------------------------------------------------------------------