%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : LCL415-1 : 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 : n006.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:53 AM UTC 2026 % Result : Satisfiable 2.92s 2.15s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL415-1 : TPTP v9.3.1. Released v2.5.0. % 0.00/0.05 % 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.11/0.36 % Computer : n006.cluster.edu % 0.11/0.36 % Model : x86_64 x86_64 % 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.36 % Memory : 8046.5625MB % 0.11/0.36 % OS : Linux 6.8.0-71-generic % 0.11/0.37 % CPULimit : 300 % 0.11/0.37 % WCLimit : 300 % 0.11/0.37 % DateTime : Sun Sep 6 00:16:31 UTC 2026 % 0.11/0.37 % CPUTime : % 2.92/2.15 % 2.92/2.15 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.92/2.15 % 2.92/2.15 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.92/2.17 %$ is_a_theorem > implies > #nlpp > b > a % 2.92/2.17 % 2.92/2.17 %Foreground sorts: % 2.92/2.17 % 2.92/2.17 % 2.92/2.17 %Background operators: % 2.92/2.17 % 2.92/2.17 % 2.92/2.17 %Foreground operators: % 2.92/2.17 tff(a, type, a: $i). % 2.92/2.17 tff(is_a_theorem, type, is_a_theorem: $i > $o). % 2.92/2.17 tff(b, type, b: $i). % 2.92/2.17 tff(implies, type, implies: ($i * $i) > $i). % 2.92/2.17 % 2.92/2.17 %Saturated clause set: % 2.92/2.18 tff(c_89, plain, (![A_15, C_52, C_14]: (is_a_theorem(implies(A_15, implies(implies(C_52, implies(C_14, A_15)), implies(C_14, A_15)))) | ~is_a_theorem(implies(A_15, implies(implies(implies(C_52, implies(C_14, A_15)), implies(C_14, A_15)), implies(implies(C_52, implies(C_14, A_15)), implies(C_14, A_15))))) | ~is_a_theorem(implies(implies(C_52, implies(C_14, A_15)), implies(C_14, A_15))) | ~is_a_theorem(implies(implies(implies(C_52, implies(C_14, A_15)), implies(C_14, A_15)), implies(implies(C_14, A_15), implies(implies(C_52, implies(C_14, A_15)), implies(C_14, A_15)))))))). % 2.92/2.18 tff(c_75, plain, (![A_15, D_48, C_46, C_14]: (is_a_theorem(implies(A_15, D_48)) | ~is_a_theorem(implies(A_15, implies(implies(implies(C_46, implies(C_14, A_15)), D_48), implies(implies(C_46, implies(C_14, A_15)), D_48)))) | ~is_a_theorem(implies(implies(C_46, implies(C_14, A_15)), D_48)) | ~is_a_theorem(implies(implies(implies(C_46, implies(C_14, A_15)), D_48), implies(implies(C_14, A_15), implies(implies(C_46, implies(C_14, A_15)), D_48))))))). % 2.92/2.18 tff(c_74, plain, (![C_46, A_47]: (is_a_theorem(implies(implies(implies(implies(C_46, A_47), A_47), implies(implies(C_46, A_47), A_47)), implies(A_47, implies(implies(C_46, A_47), A_47)))) | ~is_a_theorem(implies(implies(C_46, A_47), A_47)) | ~is_a_theorem(implies(implies(implies(C_46, A_47), A_47), implies(A_47, implies(implies(C_46, A_47), A_47))))))). % 2.92/2.18 tff(c_76, plain, (![A_47, D_48, C_46]: (is_a_theorem(implies(A_47, D_48)) | ~is_a_theorem(implies(implies(implies(C_46, A_47), D_48), implies(implies(C_46, A_47), D_48))) | ~is_a_theorem(implies(implies(C_46, A_47), D_48)) | ~is_a_theorem(implies(implies(implies(C_46, A_47), D_48), implies(A_47, implies(implies(C_46, A_47), D_48))))))). % 2.92/2.18 tff(c_61, plain, (![C_38, A_39, D_40]: (is_a_theorem(implies(implies(implies(implies(C_38, A_39), D_40), implies(implies(C_38, A_39), D_40)), implies(A_39, D_40))) | ~is_a_theorem(implies(implies(C_38, A_39), D_40)) | ~is_a_theorem(implies(implies(implies(C_38, A_39), D_40), implies(A_39, implies(implies(C_38, A_39), D_40))))))). % 2.92/2.18 tff(c_45, plain, (![A_15, C_30, D_33, C_32, C_14]: (is_a_theorem(implies(A_15, implies(implies(C_32, implies(C_14, A_15)), D_33))) | ~is_a_theorem(implies(A_15, implies(implies(C_30, implies(C_14, A_15)), implies(implies(C_32, implies(C_14, A_15)), D_33)))) | ~is_a_theorem(implies(implies(C_14, A_15), implies(C_30, implies(C_14, A_15))))))). % 2.92/2.19 tff(c_52, plain, (![C_5, A_3, D_6]: (is_a_theorem(implies(implies(implies(C_5, A_3), D_6), implies(implies(implies(implies(C_5, A_3), D_6), implies(implies(C_5, A_3), D_6)), implies(A_3, D_6)))) | ~is_a_theorem(implies(implies(implies(C_5, A_3), D_6), implies(A_3, implies(implies(C_5, A_3), D_6))))))). % 2.92/2.19 tff(c_46, plain, (![A_31, C_32, D_33, C_30]: (is_a_theorem(implies(A_31, implies(implies(C_32, A_31), D_33))) | ~is_a_theorem(implies(implies(C_30, A_31), implies(implies(C_32, A_31), D_33))) | ~is_a_theorem(implies(A_31, implies(C_30, A_31)))))). % 2.92/2.19 tff(c_32, plain, (![C_21, A_9, C_11, D_12]: (is_a_theorem(implies(implies(implies(C_21, A_9), implies(implies(C_11, A_9), D_12)), implies(A_9, implies(implies(C_11, A_9), D_12)))) | ~is_a_theorem(implies(A_9, implies(C_21, A_9)))))). % 2.92/2.19 tff(c_26, plain, (![C_11, B_10, A_17, D_12, C_20]: (is_a_theorem(implies(A_17, D_12)) | ~is_a_theorem(implies(A_17, implies(B_10, implies(implies(C_11, implies(C_20, A_17)), D_12)))) | ~is_a_theorem(implies(implies(C_20, A_17), B_10))))). % 2.92/2.19 tff(c_27, plain, (![C_5, A_3, D_6, B_4]: (is_a_theorem(implies(implies(implies(C_5, A_3), D_6), implies(A_3, D_6))) | ~is_a_theorem(implies(implies(implies(C_5, A_3), D_6), implies(A_3, B_4)))))). % 2.92/2.19 tff(c_17, plain, (![A_15, D_16, B_13, C_14]: (is_a_theorem(implies(A_15, D_16)) | ~is_a_theorem(implies(B_13, implies(implies(C_14, A_15), D_16))) | ~is_a_theorem(implies(A_15, B_13))))). % 2.92/2.19 tff(c_12, plain, (![B_10, C_11, A_9, D_12]: (is_a_theorem(implies(implies(B_10, implies(implies(C_11, A_9), D_12)), implies(A_9, D_12))) | ~is_a_theorem(implies(A_9, B_10))))). % 2.92/2.19 tff(c_4, plain, (![A_3, B_4, C_5, D_6]: (is_a_theorem(implies(implies(A_3, B_4), implies(implies(B_4, implies(implies(C_5, A_3), D_6)), implies(A_3, D_6))))))). % 2.92/2.19 tff(c_2, plain, (![B_2, A_1]: (is_a_theorem(B_2) | ~is_a_theorem(A_1) | ~is_a_theorem(implies(A_1, B_2))))). % 2.92/2.19 tff(c_6, plain, (~is_a_theorem(implies(a, implies(b, a))))). % 2.92/2.19 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 2.92/2.19 %------------------------------------------------------------------------------