%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYO846+1 : TPTP v9.0.0. Released v7.5.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 : n029.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:38:19 PM UTC 2025
% Result : CounterSatisfiable 6.09s 2.45s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.12 % Problem : SYO846+1 : TPTP v9.0.0. Released v7.5.0.
% 0.10/0.12 % 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.12/0.33 % Computer : n029.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Wed Apr 9 10:12:34 EDT 2025
% 0.12/0.33 % CPUTime :
% 6.09/2.45
% 6.09/2.45 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.09/2.45
% 6.09/2.45 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.09/2.46 %$ asubq > ain > aex5 > aex4 > aex3 > aex2 > aal7 > aal6 > aal5 > aal4 > aal3 > aal2 > aun > asm > aint > #nlpp > asing > apow > a4 > a3 > a2 > a1 > a0 > #skF_1 > #skF_2
% 6.09/2.46
% 6.09/2.46 %Foreground sorts:
% 6.09/2.46
% 6.09/2.46
% 6.09/2.46 %Background operators:
% 6.09/2.46
% 6.09/2.46
% 6.09/2.46 %Foreground operators:
% 6.09/2.46 tff(a1, type, a1: $i).
% 6.09/2.46 tff(a3, type, a3: $i).
% 6.09/2.46 tff(aun, type, aun: ($i * $i) > $i).
% 6.09/2.46 tff(asm, type, asm: ($i * $i) > $i).
% 6.09/2.46 tff(aal2, type, aal2: $i > $o).
% 6.09/2.46 tff('#skF_1', type, '#skF_1': $i > $i).
% 6.09/2.46 tff(asubq, type, asubq: ($i * $i) > $o).
% 6.09/2.46 tff(apow, type, apow: $i > $i).
% 6.09/2.46 tff(aint, type, aint: ($i * $i) > $i).
% 6.09/2.46 tff(aex3, type, aex3: $i > $o).
% 6.09/2.46 tff(ain, type, ain: ($i * $i) > $o).
% 6.09/2.46 tff(aex5, type, aex5: $i > $o).
% 6.09/2.46 tff(a0, type, a0: $i).
% 6.09/2.46 tff(aex2, type, aex2: $i > $o).
% 6.09/2.46 tff(aal5, type, aal5: $i > $o).
% 6.09/2.46 tff(a2, type, a2: $i).
% 6.09/2.46 tff(aal4, type, aal4: $i > $o).
% 6.09/2.46 tff(aal7, type, aal7: $i > $o).
% 6.09/2.46 tff(a4, type, a4: $i).
% 6.09/2.46 tff(asing, type, asing: $i > $i).
% 6.09/2.46 tff(aal6, type, aal6: $i > $o).
% 6.09/2.46 tff(aal3, type, aal3: $i > $o).
% 6.09/2.46 tff('#skF_2', type, '#skF_2': ($i * $i) > $i).
% 6.09/2.46 tff(aex4, type, aex4: $i > $o).
% 6.09/2.46
% 6.09/2.46 %Saturated clause set:
% 6.09/2.47 tff(c_518, plain, (![X25_49]: ('#skF_2'(aun(aun(asing(a1), asing(asing(a1))), apow(asing(asing(a1)))), '#skF_2'(apow(aun(aun(asing(a1), asing(asing(a1))), apow(asing(asing(a1))))), X25_49))=asing(asing(a1)) | '#skF_2'(aun(aun(asing(a1), asing(asing(a1))), apow(asing(asing(a1)))), '#skF_2'(apow(aun(aun(asing(a1), asing(asing(a1))), apow(asing(asing(a1))))), X25_49))=asing(a1) | '#skF_2'(aun(aun(asing(a1), asing(asing(a1))), apow(asing(asing(a1)))), '#skF_2'(apow(aun(aun(asing(a1), asing(asing(a1))), apow(asing(asing(a1))))), X25_49))=a1 | '#skF_2'(aun(aun(asing(a1), asing(asing(a1))), apow(asing(asing(a1)))), '#skF_2'(apow(aun(aun(asing(a1), asing(asing(a1))), apow(asing(asing(a1))))), X25_49))=a0 | asubq(aun(aun(asing(a1), asing(asing(a1))), apow(asing(asing(a1)))), '#skF_2'(apow(aun(aun(asing(a1), asing(asing(a1))), apow(asing(asing(a1))))), X25_49)) | asubq(apow(aun(aun(asing(a1), asing(asing(a1))), apow(asing(asing(a1))))), X25_49) | ~asubq(X25_49, apow(aun(aun(asing(a1), asing(asing(a1))), apow(asing(asing(a1))))))))).
% 6.09/2.47 tff(c_526, plain, (~aal6(aun(aun(asing(a1), asing(asing(a1))), apow(asing(asing(a1))))))).
% 6.09/2.47 tff(c_491, plain, (![X25_49]: ('#skF_2'(asm(a4, apow(asing(a2))), '#skF_2'(apow(asm(a4, apow(asing(a2)))), X25_49))=a3 | '#skF_2'(asm(a4, apow(asing(a2))), '#skF_2'(apow(asm(a4, apow(asing(a2)))), X25_49))=a2 | '#skF_2'(asm(a4, apow(asing(a2))), '#skF_2'(apow(asm(a4, apow(asing(a2)))), X25_49))=a1 | asubq(asm(a4, apow(asing(a2))), '#skF_2'(apow(asm(a4, apow(asing(a2)))), X25_49)) | asubq(apow(asm(a4, apow(asing(a2)))), X25_49) | ~asubq(X25_49, apow(asm(a4, apow(asing(a2)))))))).
% 6.09/2.47 tff(c_415, plain, (![X25_14]: ('#skF_2'(aun(aun(asing(a1), asing(asing(a1))), apow(asing(asing(a1)))), X25_14)=asing(asing(a1)) | '#skF_2'(aun(aun(asing(a1), asing(asing(a1))), apow(asing(asing(a1)))), X25_14)=asing(a1) | '#skF_2'(aun(aun(asing(a1), asing(asing(a1))), apow(asing(asing(a1)))), X25_14)=a1 | '#skF_2'(aun(aun(asing(a1), asing(asing(a1))), apow(asing(asing(a1)))), X25_14)=a0 | asubq(aun(aun(asing(a1), asing(asing(a1))), apow(asing(asing(a1)))), X25_14) | ~asubq(X25_14, aun(aun(asing(a1), asing(asing(a1))), apow(asing(asing(a1)))))))).
% 6.09/2.47 tff(c_503, plain, (~aal5(asm(aint(aun(aun(asing(a1), asing(asing(a1))), aun(apow(asing(a2)), asing(a3))), aun(asing(asing(a2)), a4)), asing(a0))))).
% 6.09/2.47 tff(c_468, plain, (![X25_49]: ('#skF_2'(asm(a4, asing(a1)), '#skF_2'(apow(asm(a4, asing(a1))), X25_49))=a3 | '#skF_2'(asm(a4, asing(a1)), '#skF_2'(apow(asm(a4, asing(a1))), X25_49))=a2 | '#skF_2'(asm(a4, asing(a1)), '#skF_2'(apow(asm(a4, asing(a1))), X25_49))=a0 | asubq(asm(a4, asing(a1)), '#skF_2'(apow(asm(a4, asing(a1))), X25_49)) | asubq(apow(asm(a4, asing(a1))), X25_49) | ~asubq(X25_49, apow(asm(a4, asing(a1))))))).
% 6.09/2.47 tff(c_439, plain, (![X25_14]: (~ain('#skF_2'(aun(asing(a2), aun(apow(asing(a2)), asing(apow(a2)))), X25_14), asing(apow(a2))) | ~ain('#skF_2'(aun(asing(a2), aun(apow(asing(a2)), asing(apow(a2)))), X25_14), aun(apow(a2), asing(asing(a2)))) | asubq(aun(asing(a2), aun(apow(asing(a2)), asing(apow(a2)))), X25_14) | ~asubq(X25_14, aun(asing(a2), aun(apow(asing(a2)), asing(apow(a2)))))))).
% 6.09/2.47 tff(c_497, plain, (~aal6(asm(a4, apow(asing(a2)))))).
% 6.09/2.47 tff(c_386, plain, (![X25_49]: ('#skF_2'(apow(aun(asing(a1), asing(asing(a1)))), X25_49)=asing(a1) | ~ain(a1, '#skF_2'(apow(aun(asing(a1), asing(asing(a1)))), X25_49)) | ain(asing(a1), '#skF_2'(apow(aun(asing(a1), asing(asing(a1)))), X25_49)) | asubq(apow(aun(asing(a1), asing(asing(a1)))), X25_49) | ~asubq(X25_49, apow(aun(asing(a1), asing(asing(a1)))))))).
% 6.09/2.47 tff(c_495, plain, (~aal6(asm(a4, asing(a1))))).
% 6.09/2.47 tff(c_332, plain, (![X25_14]: ('#skF_2'(asm(a4, apow(asing(a2))), X25_14)=a3 | '#skF_2'(asm(a4, apow(asing(a2))), X25_14)=a2 | '#skF_2'(asm(a4, apow(asing(a2))), X25_14)=a1 | asubq(asm(a4, apow(asing(a2))), X25_14) | ~asubq(X25_14, asm(a4, apow(asing(a2))))))).
% 6.09/2.47 tff(c_403, plain, (![X25_49]: ('#skF_2'(a3, '#skF_2'(apow(a3), X25_49))=a2 | '#skF_2'(a3, '#skF_2'(apow(a3), X25_49))=a1 | '#skF_2'(a3, '#skF_2'(apow(a3), X25_49))=a0 | asubq(a3, '#skF_2'(apow(a3), X25_49)) | asubq(apow(a3), X25_49) | ~asubq(X25_49, apow(a3))))).
% 6.09/2.47 tff(c_472, plain, (~aal6(aun(asing(a1), asing(asing(a1)))))).
% 6.09/2.47 tff(c_311, plain, (![X25_14]: ('#skF_2'(asm(a4, asing(a1)), X25_14)=a3 | '#skF_2'(asm(a4, asing(a1)), X25_14)=a2 | '#skF_2'(asm(a4, asing(a1)), X25_14)=a0 | asubq(asm(a4, asing(a1)), X25_14) | ~asubq(X25_14, asm(a4, asing(a1)))))).
% 6.09/2.47 tff(c_176, plain, (asubq(asm(aint(aun(aun(asing(a1), asing(asing(a1))), aun(apow(asing(a2)), asing(a3))), aun(asing(asing(a2)), a4)), asing(a0)), asm(aun(asing(asing(a2)), a4), asm(apow(a2), asing(a1)))))).
% 6.09/2.47 tff(c_359, plain, (![X25_14]: (~ain('#skF_2'(aun(asing(a1), asing(asing(a1))), X25_14), asing(a2)) | asubq(aun(asing(a1), asing(asing(a1))), X25_14) | ~asubq(X25_14, aun(asing(a1), asing(asing(a1))))))).
% 6.09/2.47 tff(c_449, plain, (~aal5(aun(asing(a1), asing(a3))))).
% 6.09/2.47 tff(c_138, plain, (aint(aun(aun(asing(a2), apow(asing(a2))), asing(asm(a3, asing(a1)))), aun(asm(apow(a2), apow(asing(a2))), aun(apow(asing(a2)), asing(apow(a2)))))=aun(asing(a2), apow(asing(a2))))).
% 6.09/2.47 tff(c_444, plain, (~ain(a1, aun(asing(a1), asing(asing(a1)))))).
% 6.09/2.47 tff(c_443, plain, (~aal5(aun(asing(a1), asing(asing(a1)))))).
% 6.09/2.47 tff(c_441, plain, (~aal5(apow(a2)))).
% 6.09/2.47 tff(c_168, plain, (![X24_28]: (~aal3(asm(aint(aun(a3, asing(asm(a3, asing(a1)))), apow(asm(a3, asing(a1)))), asing(X24_28))) | ~ain(X24_28, apow(asm(a3, asing(a1)))) | ~ain(X24_28, a3)))).
% 6.09/2.47 tff(c_440, plain, (~aal5(asm(asm(apow(a2), a2), asing(asing(a1)))))).
% 6.09/2.48 tff(c_136, plain, (![X24_25]: (~ain(X24_25, asing(apow(a2))) | ~ain(X24_25, aun(asing(a2), aun(apow(asing(a2)), asing(apow(a2))))) | ~ain(X24_25, aun(apow(a2), asing(asing(a2))))))).
% 6.09/2.48 tff(c_433, plain, (~aal5(asm(asm(apow(a2), a2), asing(a2))))).
% 6.09/2.48 tff(c_338, plain, (![X24_54, X25_53]: (aal6(asm(X24_54, asing('#skF_2'(X24_54, X25_53)))) | ~aal5(X25_53) | asubq(asm(X24_54, asing('#skF_2'(X24_54, X25_53))), X25_53) | asubq(X24_54, X25_53) | ~asubq(X25_53, X24_54)))).
% 6.09/2.48 tff(c_342, plain, (![X24_55, X25_56]: (aal6(X24_55) | ~aal5('#skF_2'(apow(X24_55), X25_56)) | asubq(X24_55, '#skF_2'(apow(X24_55), X25_56)) | asubq(apow(X24_55), X25_56) | ~asubq(X25_56, apow(X24_55))))).
% 6.09/2.48 tff(c_106, plain, (![X24_22]: (asing(asing(a1))=X24_22 | asing(a1)=X24_22 | a1=X24_22 | a0=X24_22 | ~ain(X24_22, aun(aun(asing(a1), asing(asing(a1))), apow(asing(asing(a1)))))))).
% 6.09/2.48 tff(c_409, plain, (~aal6(a3))).
% 6.09/2.48 tff(c_369, plain, (![X25_63]: (~ain('#skF_2'(asm(a3, asing(a1)), X25_63), asing(a3)) | asubq(asm(a3, asing(a1)), X25_63) | ~asubq(X25_63, asm(a3, asing(a1)))))).
% 6.09/2.48 tff(c_114, plain, (~asubq(aun(asm(apow(a2), apow(asing(a2))), apow(asing(asing(a1)))), aun(asm(apow(a2), apow(asing(a1))), apow(asing(asing(a1))))))).
% 6.09/2.48 tff(c_170, plain, (~aal3(asm(aint(aun(a3, asing(asm(a3, asing(a1)))), apow(asm(a3, asing(a1)))), asing(asm(a3, asing(a1))))))).
% 6.09/2.48 tff(c_144, plain, (![X24_27]: (~aal3(asm(aun(apow(asing(a2)), asing(apow(a2))), asing(X24_27))) | ~ain(X24_27, aun(apow(asing(a2)), asing(apow(a2))))))).
% 6.09/2.48 tff(c_280, plain, (![X25_49]: ('#skF_2'(a3, X25_49)=a2 | '#skF_2'(a3, X25_49)=a1 | '#skF_2'(a3, X25_49)=a0 | asubq(a3, X25_49) | ~asubq(X25_49, a3)))).
% 6.09/2.48 tff(c_392, plain, (~ain(a1, a0))).
% 6.09/2.48 tff(c_104, plain, (![X24_21]: (asing(a1)=X24_21 | ~ain(a1, X24_21) | ain(asing(a1), X24_21) | ~asubq(X24_21, aun(asing(a1), asing(asing(a1))))))).
% 6.09/2.48 tff(c_281, plain, (![X24_9, X25_10, X25_49]: (~ain('#skF_2'(asm(X24_9, X25_10), X25_49), X25_10) | asubq(asm(X24_9, X25_10), X25_49) | ~asubq(X25_49, asm(X24_9, X25_10))))).
% 6.09/2.48 tff(c_148, plain, (aal3(asm(apow(aun(asing(a1), asing(asing(a1)))), asing(aun(asing(a1), asing(asing(a1)))))))).
% 6.09/2.48 tff(c_100, plain, (ain(a2, aun(asm(apow(a2), apow(asing(a2))), aun(apow(asing(a2)), asing(apow(a2))))))).
% 6.09/2.48 tff(c_98, plain, (ain(a1, aun(asm(apow(a2), apow(asing(a1))), aun(asing(asing(a2)), asing(apow(a2))))))).
% 6.09/2.48 tff(c_36, plain, (![X25_19, X24_18, X26_20]: (aal3(X25_19) | aal3(X24_18) | ~aal4(asm(aun(X24_18, X25_19), asing(X26_20))) | ~ain(X26_20, aun(X24_18, X25_19))))).
% 6.09/2.48 tff(c_350, plain, (![X26_11]: (~ain(X26_11, asing(a2)) | ~ain(X26_11, aun(asing(a1), asing(asing(a1))))))).
% 6.09/2.48 tff(c_128, plain, (asm(asm(apow(a2), apow(asing(a2))), asing(a2))=aun(asing(a1), asing(asing(a1))))).
% 6.09/2.48 tff(c_118, plain, (~asubq(aun(asing(asing(a1)), aun(asing(asing(a2)), a4)), aun(asing(asing(a2)), a4)))).
% 6.09/2.48 tff(c_134, plain, (aint(aun(apow(a2), asing(asing(a2))), aun(a4, asing(asm(apow(a2), a2))))=a3)).
% 6.09/2.48 tff(c_282, plain, (![X24_7, X25_49]: (asubq('#skF_2'(apow(X24_7), X25_49), X24_7) | asubq(apow(X24_7), X25_49) | ~asubq(X25_49, apow(X24_7))))).
% 6.09/2.48 tff(c_30, plain, (![X25_14, X24_13]: (asubq(X25_14, asm(X24_13, asing('#skF_2'(X24_13, X25_14)))) | asubq(X24_13, X25_14) | ~asubq(X25_14, X24_13)))).
% 6.09/2.48 tff(c_156, plain, (aal4(aun(asm(apow(a2), asing(a2)), asing(asm(apow(a2), apow(asing(a2)))))))).
% 6.09/2.48 tff(c_94, plain, (~ain(asm(apow(a2), a2), aun(asing(asing(a1)), aun(asing(asing(a2)), a4))))).
% 6.09/2.48 tff(c_334, plain, (~aal5(a1))).
% 6.09/2.48 tff(c_333, plain, (~aal5(a2))).
% 6.09/2.48 tff(c_110, plain, (![X24_24]: (a3=X24_24 | a2=X24_24 | a1=X24_24 | ~ain(X24_24, asm(a4, apow(asing(a2))))))).
% 6.09/2.48 tff(c_78, plain, (ain(a1, aun(asm(apow(a2), apow(asing(a2))), asing(asing(asing(a1))))))).
% 6.09/2.48 tff(c_130, plain, (asubq(aun(asing(a1), asing(a3)), asm(asm(a4, asing(a2)), asing(a0))))).
% 6.09/2.48 tff(c_323, plain, (~ain(a1, asm(apow(a2), asing(a1))))).
% 6.09/2.48 tff(c_88, plain, (ain(a1, asm(aun(asing(asing(a2)), a4), asm(apow(a2), asing(a1)))))).
% 6.09/2.48 tff(c_76, plain, (ain(asing(asing(a1)), aun(asm(apow(a2), a2), apow(asing(asing(a1))))))).
% 6.09/2.48 tff(c_60, plain, (~ain(asm(apow(a2), apow(asing(a2))), asm(apow(a2), asing(a1))))).
% 6.09/2.48 tff(c_116, plain, (asubq(apow(a2), aun(asing(asing(a1)), aun(a4, asing(apow(a2))))))).
% 6.09/2.48 tff(c_54, plain, (asubq(aun(asing(a1), asing(asing(a1))), asm(apow(a2), asing(a2))))).
% 6.09/2.48 tff(c_164, plain, (aex2(aint(aun(apow(a2), asing(asing(a2))), asm(a4, asing(a1)))))).
% 6.09/2.48 tff(c_108, plain, (![X24_23]: (a3=X24_23 | a2=X24_23 | a0=X24_23 | ~ain(X24_23, asm(a4, asing(a1)))))).
% 6.09/2.48 tff(c_172, plain, (aex5(aun(asm(apow(a2), apow(asing(a2))), apow(asing(asing(a1))))))).
% 6.09/2.48 tff(c_96, plain, (~ain(asm(a3, asing(a1)), aun(apow(asing(a2)), asing(apow(a2)))))).
% 6.09/2.48 tff(c_302, plain, (~aal5(a0))).
% 6.09/2.48 tff(c_56, plain, (~ain(asm(apow(a2), apow(asing(a2))), asm(apow(a2), asing(a2))))).
% 6.09/2.48 tff(c_92, plain, (ain(a2, aun(asing(asing(a1)), aun(asing(asing(a2)), a4))))).
% 6.09/2.49 tff(c_124, plain, (asubq(asm(asm(apow(a2), a2), asing(asing(a1))), asing(a2)))).
% 6.09/2.49 tff(c_102, plain, (ain(a1, aun(asing(asing(a1)), aun(a4, asing(apow(a2))))))).
% 6.09/2.49 tff(c_289, plain, (![X26_11]: (~ain(X26_11, asing(a3)) | ~ain(X26_11, asm(a3, asing(a1)))))).
% 6.09/2.49 tff(c_132, plain, (asm(asm(a4, asing(a1)), asing(a3))=asm(a3, asing(a1)))).
% 6.09/2.49 tff(c_126, plain, (asubq(asm(asm(apow(a2), a2), asing(a2)), asing(asing(a1))))).
% 6.09/2.49 tff(c_32, plain, (![X24_13, X25_14]: (ain('#skF_2'(X24_13, X25_14), X24_13) | asubq(X24_13, X25_14) | ~asubq(X25_14, X24_13)))).
% 6.09/2.49 tff(c_72, plain, (ain(asing(a1), aun(asing(asing(a1)), asing(asing(asing(a1))))))).
% 6.09/2.49 tff(c_2, plain, (![X24_1, X25_4]: (aal6(X24_1) | ~aal5(X25_4) | asubq(X24_1, X25_4) | ~asubq(X25_4, X24_1)))).
% 6.09/2.49 tff(c_243, plain, (asubq(a0, aun(asing(a1), asing(asing(a1)))))).
% 6.09/2.49 tff(c_74, plain, (ain(a0, apow(aun(asing(a1), asing(asing(a1))))))).
% 6.09/2.49 tff(c_16, plain, (![X24_6]: (a2=X24_6 | a1=X24_6 | a0=X24_6 | ~ain(X24_6, a3)))).
% 6.09/2.49 tff(c_64, plain, (ain(asing(asing(a1)), asing(asing(asing(a1)))))).
% 6.09/2.49 tff(c_90, plain, (~ain(asing(a1), aun(asing(asing(a2)), a4)))).
% 6.09/2.49 tff(c_62, plain, (asm(apow(a2), apow(asing(a2)))!=apow(a2))).
% 6.09/2.49 tff(c_112, plain, (~asubq(aun(asing(apow(asing(a1))), a4), a4))).
% 6.09/2.49 tff(c_70, plain, (~ain(asing(asing(a1)), asing(apow(asing(a1)))))).
% 6.09/2.49 tff(c_223, plain, (~ain(a2, asing(a1)))).
% 6.09/2.49 tff(c_86, plain, (~ain(a1, aun(asing(asing(a1)), asing(a3))))).
% 6.09/2.49 tff(c_26, plain, (![X26_11, X25_10, X24_9]: (~ain(X26_11, X25_10) | ~ain(X26_11, asm(X24_9, X25_10))))).
% 6.09/2.49 tff(c_142, plain, (![X24_26]: (~aal2(asm(a2, asing(X24_26))) | ~ain(X24_26, a2)))).
% 6.09/2.49 tff(c_215, plain, (asubq(a0, asing(asing(a1))))).
% 6.09/2.49 tff(c_214, plain, (asubq(a0, apow(asing(a1))))).
% 6.09/2.49 tff(c_216, plain, (![X24_12]: (asubq(X24_12, X24_12)))).
% 6.09/2.49 tff(c_24, plain, (![X25_8, X24_7]: (asubq(X25_8, X24_7) | ~ain(X25_8, apow(X24_7))))).
% 6.09/2.49 tff(c_160, plain, (aex2(aun(asing(a1), asing(asing(a1)))))).
% 6.09/2.49 tff(c_158, plain, (aal5(aun(apow(a2), asing(asing(a2)))))).
% 6.09/2.49 tff(c_200, plain, (~aal4(aun(a2, asing(apow(a2)))))).
% 6.09/2.49 tff(c_34, plain, (![X24_16, X25_17]: (~aal7(aun(X24_16, asing(X25_17))) | aal6(X24_16)))).
% 6.09/2.49 tff(c_68, plain, (ain(a0, apow(apow(asing(a1)))))).
% 6.09/2.49 tff(c_122, plain, (asubq(a2, asm(a3, asing(a2))))).
% 6.09/2.49 tff(c_80, plain, (ain(a2, asm(a4, asing(a1))))).
% 6.09/2.49 tff(c_84, plain, (~ain(asm(apow(a2), a2), a4))).
% 6.09/2.49 tff(c_166, plain, (aex3(aun(a2, asing(apow(a2)))))).
% 6.09/2.49 tff(c_66, plain, (ain(a0, apow(asing(asing(a1)))))).
% 6.09/2.49 tff(c_152, plain, (aal3(aun(a2, asing(apow(a2)))))).
% 6.09/2.49 tff(c_120, plain, (asubq(a1, asm(a2, asing(a1))))).
% 6.09/2.49 tff(c_8, plain, (![X24_1]: (asubq('#skF_1'(X24_1), X24_1) | ~aal6(X24_1)))).
% 6.09/2.49 tff(c_10, plain, (![X24_5]: (aex3(X24_5) | aal4(X24_5) | ~aal3(X24_5)))).
% 6.09/2.49 tff(c_6, plain, (![X24_1]: (~asubq(X24_1, '#skF_1'(X24_1)) | ~aal6(X24_1)))).
% 6.09/2.49 tff(c_48, plain, (~ain(asm(a3, asing(a1)), a2))).
% 6.09/2.49 tff(c_52, plain, (asing(asing(a1))!=apow(asing(a1)))).
% 6.09/2.49 tff(c_174, plain, (aex5(aun(a4, asing(apow(a2)))))).
% 6.09/2.49 tff(c_46, plain, (~ain(asing(asing(a1)), a2))).
% 6.09/2.49 tff(c_4, plain, (![X24_1]: (aal5('#skF_1'(X24_1)) | ~aal6(X24_1)))).
% 6.09/2.49 tff(c_162, plain, (aex2(asm(a3, asing(a1))))).
% 6.09/2.49 tff(c_150, plain, (aal3(asm(a4, asing(a2))))).
% 6.09/2.49 tff(c_12, plain, (![X24_5]: (~aal4(X24_5) | ~aex3(X24_5)))).
% 6.09/2.49 tff(c_14, plain, (![X24_5]: (aal3(X24_5) | ~aex3(X24_5)))).
% 6.09/2.49 tff(c_146, plain, (aal2(asm(a4, a2)))).
% 6.09/2.50 tff(c_28, plain, (![X24_12]: (ain(X24_12, apow(X24_12))))).
% 6.09/2.50 tff(c_50, plain, (apow(asing(a1))!=a2)).
% 6.09/2.50 tff(c_82, plain, (~ain(a1, asing(a3)))).
% 6.09/2.50 tff(c_22, plain, (ain(a0, a3))).
% 6.09/2.50 tff(c_178, plain, (~aex4(aint(aun(apow(a2), asing(asing(a2))), aun(asing(asing(a1)), aun(a4, asing(apow(a2)))))))).
% 6.09/2.50 tff(c_20, plain, (ain(a1, a3))).
% 6.09/2.50 tff(c_18, plain, (ain(a2, a3))).
% 6.09/2.50 tff(c_58, plain, (asing(a2)!=a2)).
% 6.09/2.50 tff(c_38, plain, (~ain(a0, a0))).
% 6.09/2.50 tff(c_40, plain, (~ain(a2, a2))).
% 6.09/2.50 tff(c_42, plain, (~asubq(a2, a0))).
% 6.09/2.50 tff(c_44, plain, (asing(a1)!=a0)).
% 6.09/2.50 tff(c_140, plain, (~aal2(asing(a3)))).
% 6.09/2.50 tff(c_154, plain, (aal4(apow(a2)))).
% 6.09/2.50 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 6.09/2.50
%------------------------------------------------------------------------------