%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : LCL407-2 : TPTP v9.3.1. 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 : n010.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 11:11:52 AM UTC 2026 % Result : Satisfiable 6.74s 3.36s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL407-2 : TPTP v9.3.1. Released v2.5.0. % 0.00/0.04 % 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.10/0.36 % Computer : n010.cluster.edu % 0.10/0.36 % Model : x86_64 x86_64 % 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.36 % Memory : 8046.5625MB % 0.10/0.36 % OS : Linux 6.8.0-71-generic % 0.10/0.36 % CPULimit : 300 % 0.10/0.36 % WCLimit : 300 % 0.10/0.36 % DateTime : Fri Sep 4 14:26:23 UTC 2026 % 0.10/0.36 % CPUTime : % 6.74/3.35 % 6.74/3.36 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.74/3.36 % 6.74/3.36 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.74/3.37 %$ xor > and_star > #nlpp > not > truth > falsehood % 6.74/3.37 % 6.74/3.37 %Foreground sorts: % 6.74/3.37 % 6.74/3.37 % 6.74/3.37 %Background operators: % 6.74/3.37 % 6.74/3.37 % 6.74/3.37 %Foreground operators: % 6.74/3.37 tff(truth, type, truth: $i). % 6.74/3.37 tff(falsehood, type, falsehood: $i). % 6.74/3.37 tff(xor, type, xor: ($i * $i) > $i). % 6.74/3.37 tff(not, type, not: $i > $i). % 6.74/3.37 tff(and_star, type, and_star: ($i * $i) > $i). % 6.74/3.37 % 6.74/3.37 %Saturated clause set: % 6.74/3.37 tff(c_2112, plain, (![Y_48, Y_33]: (and_star(not(and_star(xor(truth, Y_48), xor(falsehood, Y_33))), xor(falsehood, Y_33))=and_star(not(and_star(xor(truth, Y_33), xor(falsehood, Y_48))), xor(falsehood, Y_48))))). % 6.74/3.37 tff(c_1944, plain, (![Y_47, Y_18]: (and_star(not(and_star(xor(falsehood, Y_47), xor(truth, Y_18))), xor(truth, Y_18))=and_star(not(and_star(xor(falsehood, Y_18), xor(truth, Y_47))), xor(truth, Y_47))))). % 6.74/3.37 tff(c_1907, plain, (![Y_33, Y_47]: (and_star(not(and_star(xor(truth, Y_33), xor(truth, Y_47))), xor(truth, Y_47))=and_star(not(and_star(xor(falsehood, Y_47), xor(falsehood, Y_33))), xor(falsehood, Y_33))))). % 6.74/3.37 tff(c_2248, plain, (![Y_26, Y_48]: (and_star(not(and_star(xor(falsehood, Y_26), xor(falsehood, Y_48))), xor(falsehood, Y_48))=and_star(not(and_star(xor(falsehood, Y_26), Y_48)), Y_48)))). % 6.74/3.37 tff(c_2083, plain, (![Y_49, Y_48]: (and_star(not(and_star(xor(truth, Y_49), xor(falsehood, Y_48))), xor(falsehood, Y_48))=and_star(not(and_star(xor(truth, Y_49), Y_48)), Y_48)))). % 6.74/3.37 tff(c_1203, plain, (![Y_37, Y_10]: (and_star(not(and_star(xor(truth, Y_37), Y_10)), Y_10)=and_star(not(and_star(xor(truth, Y_10), xor(falsehood, Y_37))), xor(falsehood, Y_37))))). % 6.74/3.37 tff(c_507, plain, (![Y_10, Y_26]: (and_star(not(and_star(xor(truth, Y_10), xor(truth, Y_26))), xor(truth, Y_26))=and_star(not(and_star(xor(falsehood, Y_26), Y_10)), Y_10)))). % 6.74/3.37 tff(c_1781, plain, (![Y_44]: (and_star(not(and_star(truth, Y_44)), xor(falsehood, Y_44))=falsehood))). % 6.74/3.37 tff(c_1774, plain, (![Y_30]: (and_star(truth, xor(falsehood, Y_30))=and_star(truth, Y_30)))). % 6.74/3.37 tff(c_904, plain, (![X_32, Y_18]: (xor(not(X_32), xor(falsehood, Y_18))=xor(X_32, xor(truth, Y_18))))). % 6.74/3.37 tff(c_1195, plain, (![Y_37]: (xor(not(xor(falsehood, Y_37)), xor(truth, Y_37))=falsehood))). % 6.74/3.37 tff(c_1368, plain, (![Y_39]: (xor(not(xor(truth, Y_39)), Y_39)=falsehood))). % 6.74/3.38 tff(c_501, plain, (![Y_26]: (xor(not(xor(truth, Y_26)), xor(falsehood, Y_26))=falsehood))). % 6.74/3.38 tff(c_1215, plain, (![Y_37]: (xor(xor(falsehood, Y_37), Y_37)=falsehood))). % 6.74/3.38 tff(c_944, plain, (![X_32, Y_33]: (xor(X_32, xor(falsehood, Y_33))=xor(X_32, Y_33)))). % 6.74/3.38 tff(c_982, plain, (xor(falsehood, truth)=truth)). % 6.74/3.38 tff(c_956, plain, (![X_32]: (xor(not(X_32), truth)=X_32))). % 6.74/3.38 tff(c_172, plain, (![X_19, Y_8]: (xor(not(X_19), xor(truth, Y_8))=xor(X_19, Y_8)))). % 6.74/3.38 tff(c_727, plain, (![Y_29]: (and_star(xor(truth, Y_29), xor(falsehood, Y_29))=falsehood))). % 6.74/3.38 tff(c_192, plain, (![Y_8]: (xor(falsehood, xor(truth, Y_8))=xor(truth, Y_8)))). % 6.74/3.38 tff(c_514, plain, (![Y_26]: (and_star(xor(falsehood, Y_26), xor(truth, Y_26))=falsehood))). % 6.74/3.38 tff(c_549, plain, (![X_7]: (xor(X_7, xor(falsehood, X_7))=falsehood))). % 6.74/3.38 tff(c_144, plain, (![Y_18]: (xor(truth, xor(truth, Y_18))=xor(falsehood, Y_18)))). % 6.74/3.38 tff(c_341, plain, (![X_22]: (and_star(not(and_star(falsehood, X_22)), X_22)=not(xor(truth, X_22))))). % 6.74/3.38 tff(c_216, plain, (![X_17]: (xor(not(X_17), xor(truth, X_17))=falsehood))). % 6.74/3.38 tff(c_343, plain, (![X_22]: (and_star(not(and_star(truth, X_22)), X_22)=falsehood))). % 6.74/3.38 tff(c_17, plain, (![Y_10, X_9]: (and_star(not(and_star(xor(truth, Y_10), X_9)), X_9)=and_star(not(and_star(xor(truth, X_9), Y_10)), Y_10)))). % 6.74/3.38 tff(c_152, plain, (![X_17]: (xor(X_17, xor(truth, not(X_17)))=falsehood))). % 6.74/3.38 tff(c_181, plain, (not(falsehood)=truth)). % 6.74/3.38 tff(c_158, plain, (![X_17]: (not(not(X_17))=X_17))). % 6.74/3.38 tff(c_18, plain, (![X_7, Y_8]: (xor(not(X_7), Y_8)=xor(X_7, xor(truth, Y_8))))). % 6.74/3.38 tff(c_75, plain, (not(truth)=falsehood)). % 6.74/3.38 tff(c_12, plain, (![X_6]: (and_star(xor(truth, X_6), X_6)=falsehood))). % 6.74/3.38 tff(c_2, plain, (![X_1]: (xor(X_1, truth)=not(X_1)))). % 6.74/3.38 tff(c_6, plain, (![X_3]: (xor(X_3, X_3)=falsehood))). % 6.74/3.38 tff(c_4, plain, (![X_2]: (xor(X_2, falsehood)=X_2))). % 6.74/3.38 tff(c_8, plain, (![X_4]: (and_star(X_4, truth)=X_4))). % 6.74/3.38 tff(c_10, plain, (![X_5]: (and_star(X_5, falsehood)=falsehood))). % 6.74/3.38 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 6.74/3.38 %------------------------------------------------------------------------------