%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SYN015-2 : TPTP v9.0.0. Released v1.0.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 : n002.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:01:53 PM UTC 2025
% Result : Unsatisfiable 74.50s 59.77s
% Output : CNFRefutation 74.77s
% Verified :
% SZS Type : Refutation
% Derivation depth : 32
% Number of leaves : 25
% Syntax : Number of formulae : 587 ( 186 unt; 0 typ; 0 def)
% Number of atoms : 1543 ( 0 equ)
% Maximal formula atoms : 7 ( 2 avg)
% Number of connectives : 1573 ( 617 ~; 956 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 3 ( 2 usr; 1 prp; 0-2 aty)
% Number of functors : 6 ( 6 usr; 4 con; 0-1 aty)
% Number of variables : 352 ( 352 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ equalish > element > #nlpp > g > f > n > m > k > a
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(m,type,
m: $i ).
tff(a,type,
a: $i ).
tff(element,type,
element: ( $i * $i ) > $o ).
tff(k,type,
k: $i ).
tff(f,type,
f: $i > $i ).
tff(g,type,
g: $i > $i ).
tff(n,type,
n: $i ).
tff(equalish,type,
equalish: ( $i * $i ) > $o ).
tff(f_187,axiom,
~ equalish(m,a),
file(unknown,unknown) ).
tff(f_190,axiom,
equalish(m,k),
file(unknown,unknown) ).
tff(f_32,axiom,
! [X,Y] :
( ~ equalish(X,Y)
| equalish(Y,X) ),
file(unknown,unknown) ).
tff(f_40,axiom,
! [X,Y,Z] :
( ~ equalish(X,Y)
| ~ equalish(Y,Z)
| equalish(X,Z) ),
file(unknown,unknown) ).
tff(f_70,axiom,
! [A] :
( ~ equalish(A,k)
| element(A,a)
| equalish(A,a) ),
file(unknown,unknown) ).
tff(f_48,axiom,
! [A,B,C] :
( ~ equalish(A,B)
| ~ element(C,A)
| element(C,B) ),
file(unknown,unknown) ).
tff(f_178,axiom,
! [A] :
( ~ element(A,k)
| equalish(A,n)
| equalish(A,m)
| equalish(A,k) ),
file(unknown,unknown) ).
tff(f_180,axiom,
~ equalish(n,a),
file(unknown,unknown) ).
tff(f_63,axiom,
! [A] :
( ~ element(A,a)
| equalish(A,k)
| equalish(A,a) ),
file(unknown,unknown) ).
tff(f_155,axiom,
! [A,B] :
( ~ element(A,B)
| ~ element(B,A)
| equalish(A,B)
| equalish(A,n)
| ~ element(B,n)
| equalish(B,n) ),
file(unknown,unknown) ).
tff(f_182,axiom,
~ equalish(m,n),
file(unknown,unknown) ).
tff(f_185,axiom,
~ equalish(n,k),
file(unknown,unknown) ).
tff(f_27,axiom,
! [X] : equalish(X,X),
file(unknown,unknown) ).
tff(f_169,axiom,
! [A] :
( ~ equalish(A,n)
| element(A,k)
| equalish(A,k) ),
file(unknown,unknown) ).
tff(f_56,axiom,
! [A,B,C] :
( ~ element(A,B)
| ~ equalish(A,C)
| element(C,B) ),
file(unknown,unknown) ).
tff(f_189,axiom,
~ equalish(k,a),
file(unknown,unknown) ).
tff(f_93,axiom,
! [A] :
( element(A,f(A))
| ~ element(A,m)
| equalish(A,m) ),
file(unknown,unknown) ).
tff(f_100,axiom,
! [A] :
( element(f(A),A)
| ~ element(A,m)
| equalish(A,m) ),
file(unknown,unknown) ).
tff(f_86,axiom,
! [A] :
( ~ equalish(f(A),A)
| ~ element(A,m)
| equalish(A,m) ),
file(unknown,unknown) ).
tff(f_134,axiom,
! [A] :
( element(A,g(A))
| element(A,n)
| equalish(A,n) ),
file(unknown,unknown) ).
tff(f_78,axiom,
! [A] :
( ~ equalish(f(A),m)
| ~ element(A,m)
| equalish(A,m) ),
file(unknown,unknown) ).
tff(f_140,axiom,
! [A] :
( element(g(A),A)
| element(A,n)
| equalish(A,n) ),
file(unknown,unknown) ).
tff(f_121,axiom,
! [A] :
( ~ equalish(g(A),n)
| element(A,n)
| equalish(A,n) ),
file(unknown,unknown) ).
tff(f_114,axiom,
! [A,B] :
( ~ element(A,B)
| ~ element(B,A)
| equalish(A,B)
| equalish(A,m)
| element(B,m)
| equalish(B,m) ),
file(unknown,unknown) ).
tff(f_128,axiom,
! [A] :
( ~ equalish(g(A),A)
| element(A,n)
| equalish(A,n) ),
file(unknown,unknown) ).
tff(c_48,plain,
~ equalish(m,a),
inference(cnfTransformation,[status(thm)],[f_187]) ).
tff(c_52,plain,
equalish(m,k),
inference(cnfTransformation,[status(thm)],[f_190]) ).
tff(c_54,plain,
! [Y_31,X_32] :
( equalish(Y_31,X_32)
| ~ equalish(X_32,Y_31) ),
inference(cnfTransformation,[status(thm)],[f_32]) ).
tff(c_61,plain,
equalish(k,m),
inference(resolution,[status(thm)],[c_52,c_54]) ).
tff(c_66,plain,
! [X_33,Z_34,Y_35] :
( equalish(X_33,Z_34)
| ~ equalish(Y_35,Z_34)
| ~ equalish(X_33,Y_35) ),
inference(cnfTransformation,[status(thm)],[f_40]) ).
tff(c_73,plain,
! [X_33] :
( equalish(X_33,m)
| ~ equalish(X_33,k) ),
inference(resolution,[status(thm)],[c_61,c_66]) ).
tff(c_217,plain,
! [A_51] :
( equalish(A_51,a)
| element(A_51,a)
| ~ equalish(A_51,k) ),
inference(cnfTransformation,[status(thm)],[f_70]) ).
tff(c_227,plain,
( equalish(m,a)
| element(m,a) ),
inference(resolution,[status(thm)],[c_52,c_217]) ).
tff(c_234,plain,
element(m,a),
inference(negUnitSimplification,[status(thm)],[c_48,c_227]) ).
tff(c_8,plain,
! [C_9,B_8,A_7] :
( element(C_9,B_8)
| ~ element(C_9,A_7)
| ~ equalish(A_7,B_8) ),
inference(cnfTransformation,[status(thm)],[f_48]) ).
tff(c_250,plain,
! [B_53] :
( element(m,B_53)
| ~ equalish(a,B_53) ),
inference(resolution,[status(thm)],[c_234,c_8]) ).
tff(c_265,plain,
( element(m,m)
| ~ equalish(a,k) ),
inference(resolution,[status(thm)],[c_73,c_250]) ).
tff(c_286,plain,
~ equalish(a,k),
inference(splitLeft,[status(thm)],[c_265]) ).
tff(c_472681,plain,
! [A_1833] :
( equalish(A_1833,k)
| equalish(A_1833,m)
| equalish(A_1833,n)
| ~ element(A_1833,k) ),
inference(cnfTransformation,[status(thm)],[f_178]) ).
tff(c_4,plain,
! [Y_3,X_2] :
( equalish(Y_3,X_2)
| ~ equalish(X_2,Y_3) ),
inference(cnfTransformation,[status(thm)],[f_32]) ).
tff(c_474322,plain,
! [A_1850] :
( equalish(n,A_1850)
| equalish(A_1850,k)
| equalish(A_1850,m)
| ~ element(A_1850,k) ),
inference(resolution,[status(thm)],[c_472681,c_4]) ).
tff(c_42,plain,
~ equalish(n,a),
inference(cnfTransformation,[status(thm)],[f_180]) ).
tff(c_474359,plain,
( equalish(a,k)
| equalish(a,m)
| ~ element(a,k) ),
inference(resolution,[status(thm)],[c_474322,c_42]) ).
tff(c_474439,plain,
( equalish(a,m)
| ~ element(a,k) ),
inference(negUnitSimplification,[status(thm)],[c_286,c_474359]) ).
tff(c_474463,plain,
~ element(a,k),
inference(splitLeft,[status(thm)],[c_474439]) ).
tff(c_12,plain,
! [A_13] :
( equalish(A_13,a)
| equalish(A_13,k)
| ~ element(A_13,a) ),
inference(cnfTransformation,[status(thm)],[f_63]) ).
tff(c_473483,plain,
! [B_1840,A_1841] :
( equalish(B_1840,n)
| ~ element(B_1840,n)
| equalish(A_1841,n)
| equalish(A_1841,B_1840)
| ~ element(B_1840,A_1841)
| ~ element(A_1841,B_1840) ),
inference(cnfTransformation,[status(thm)],[f_155]) ).
tff(c_44,plain,
~ equalish(m,n),
inference(cnfTransformation,[status(thm)],[f_182]) ).
tff(c_476578,plain,
! [B_1879] :
( equalish(B_1879,n)
| ~ element(B_1879,n)
| equalish(m,B_1879)
| ~ element(B_1879,m)
| ~ element(m,B_1879) ),
inference(resolution,[status(thm)],[c_473483,c_44]) ).
tff(c_476682,plain,
( equalish(a,n)
| ~ element(a,n)
| ~ element(a,m)
| ~ element(m,a) ),
inference(resolution,[status(thm)],[c_476578,c_48]) ).
tff(c_476743,plain,
( equalish(a,n)
| ~ element(a,n)
| ~ element(a,m) ),
inference(demodulation,[status(thm),theory(equality)],[c_234,c_476682]) ).
tff(c_476744,plain,
~ element(a,m),
inference(splitLeft,[status(thm)],[c_476743]) ).
tff(c_184,plain,
! [A_50] :
( equalish(A_50,a)
| equalish(A_50,k)
| ~ element(A_50,a) ),
inference(cnfTransformation,[status(thm)],[f_63]) ).
tff(c_46,plain,
~ equalish(n,k),
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_203,plain,
( equalish(n,a)
| ~ element(n,a) ),
inference(resolution,[status(thm)],[c_184,c_46]) ).
tff(c_216,plain,
~ element(n,a),
inference(negUnitSimplification,[status(thm)],[c_42,c_203]) ).
tff(c_2,plain,
! [X_1] : equalish(X_1,X_1),
inference(cnfTransformation,[status(thm)],[f_27]) ).
tff(c_109,plain,
! [A_39] :
( equalish(A_39,k)
| element(A_39,k)
| ~ equalish(A_39,n) ),
inference(cnfTransformation,[status(thm)],[f_169]) ).
tff(c_113,plain,
( equalish(n,k)
| element(n,k) ),
inference(resolution,[status(thm)],[c_2,c_109]) ).
tff(c_116,plain,
element(n,k),
inference(negUnitSimplification,[status(thm)],[c_46,c_113]) ).
tff(c_117,plain,
! [C_40,B_41,A_42] :
( element(C_40,B_41)
| ~ equalish(A_42,C_40)
| ~ element(A_42,B_41) ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_127,plain,
! [B_41] :
( element(m,B_41)
| ~ element(k,B_41) ),
inference(resolution,[status(thm)],[c_61,c_117]) ).
tff(c_136,plain,
! [C_45,B_46,A_47] :
( element(C_45,B_46)
| ~ element(C_45,A_47)
| ~ equalish(A_47,B_46) ),
inference(cnfTransformation,[status(thm)],[f_48]) ).
tff(c_452,plain,
! [B_61,B_62] :
( element(m,B_61)
| ~ equalish(B_62,B_61)
| ~ element(k,B_62) ),
inference(resolution,[status(thm)],[c_127,c_136]) ).
tff(c_483,plain,
( element(m,m)
| ~ element(k,k) ),
inference(resolution,[status(thm)],[c_61,c_452]) ).
tff(c_486,plain,
~ element(k,k),
inference(splitLeft,[status(thm)],[c_483]) ).
tff(c_485,plain,
( element(m,k)
| ~ element(k,m) ),
inference(resolution,[status(thm)],[c_52,c_452]) ).
tff(c_487,plain,
~ element(k,m),
inference(splitLeft,[status(thm)],[c_485]) ).
tff(c_50,plain,
~ equalish(k,a),
inference(cnfTransformation,[status(thm)],[f_189]) ).
tff(c_224,plain,
( equalish(k,a)
| element(k,a) ),
inference(resolution,[status(thm)],[c_2,c_217]) ).
tff(c_231,plain,
element(k,a),
inference(negUnitSimplification,[status(thm)],[c_50,c_224]) ).
tff(c_1203,plain,
! [A_78] :
( equalish(A_78,k)
| equalish(A_78,m)
| equalish(A_78,n)
| ~ element(A_78,k) ),
inference(cnfTransformation,[status(thm)],[f_178]) ).
tff(c_2311,plain,
! [A_90] :
( equalish(n,A_90)
| equalish(A_90,k)
| equalish(A_90,m)
| ~ element(A_90,k) ),
inference(resolution,[status(thm)],[c_1203,c_4]) ).
tff(c_75,plain,
! [X_33] :
( equalish(X_33,k)
| ~ equalish(X_33,m) ),
inference(resolution,[status(thm)],[c_52,c_66]) ).
tff(c_2436,plain,
! [A_91] :
( equalish(n,A_91)
| equalish(A_91,k)
| ~ element(A_91,k) ),
inference(resolution,[status(thm)],[c_2311,c_75]) ).
tff(c_2654,plain,
! [A_93] :
( equalish(k,A_93)
| equalish(n,A_93)
| ~ element(A_93,k) ),
inference(resolution,[status(thm)],[c_2436,c_4]) ).
tff(c_2971,plain,
! [A_98] :
( equalish(A_98,n)
| equalish(k,A_98)
| ~ element(A_98,k) ),
inference(resolution,[status(thm)],[c_2654,c_4]) ).
tff(c_10,plain,
! [C_12,B_11,A_10] :
( element(C_12,B_11)
| ~ equalish(A_10,C_12)
| ~ element(A_10,B_11) ),
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_20236,plain,
! [A_280,B_281] :
( element(A_280,B_281)
| ~ element(k,B_281)
| equalish(A_280,n)
| ~ element(A_280,k) ),
inference(resolution,[status(thm)],[c_2971,c_10]) ).
tff(c_20271,plain,
! [A_282] :
( element(A_282,a)
| equalish(A_282,n)
| ~ element(A_282,k) ),
inference(resolution,[status(thm)],[c_231,c_20236]) ).
tff(c_20579,plain,
! [A_284] :
( equalish(n,A_284)
| element(A_284,a)
| ~ element(A_284,k) ),
inference(resolution,[status(thm)],[c_20271,c_4]) ).
tff(c_88,plain,
! [X_37] :
( equalish(X_37,m)
| ~ equalish(X_37,k) ),
inference(resolution,[status(thm)],[c_61,c_66]) ).
tff(c_6,plain,
! [X_4,Z_6,Y_5] :
( equalish(X_4,Z_6)
| ~ equalish(Y_5,Z_6)
| ~ equalish(X_4,Y_5) ),
inference(cnfTransformation,[status(thm)],[f_40]) ).
tff(c_97,plain,
! [X_4,X_37] :
( equalish(X_4,m)
| ~ equalish(X_4,X_37)
| ~ equalish(X_37,k) ),
inference(resolution,[status(thm)],[c_88,c_6]) ).
tff(c_20752,plain,
! [A_284] :
( equalish(n,m)
| ~ equalish(A_284,k)
| element(A_284,a)
| ~ element(A_284,k) ),
inference(resolution,[status(thm)],[c_20579,c_97]) ).
tff(c_52432,plain,
equalish(n,m),
inference(splitLeft,[status(thm)],[c_20752]) ).
tff(c_297,plain,
! [A_56] :
( equalish(k,A_56)
| equalish(A_56,a)
| ~ element(A_56,a) ),
inference(resolution,[status(thm)],[c_184,c_4]) ).
tff(c_369,plain,
! [A_57] :
( equalish(a,A_57)
| equalish(k,A_57)
| ~ element(A_57,a) ),
inference(resolution,[status(thm)],[c_297,c_4]) ).
tff(c_520,plain,
! [A_66] :
( equalish(A_66,k)
| equalish(a,A_66)
| ~ element(A_66,a) ),
inference(resolution,[status(thm)],[c_369,c_4]) ).
tff(c_237,plain,
! [B_8] :
( element(k,B_8)
| ~ equalish(a,B_8) ),
inference(resolution,[status(thm)],[c_231,c_8]) ).
tff(c_958,plain,
! [A_73] :
( element(k,A_73)
| equalish(A_73,k)
| ~ element(A_73,a) ),
inference(resolution,[status(thm)],[c_520,c_237]) ).
tff(c_1019,plain,
! [X_4,A_73] :
( equalish(X_4,k)
| ~ equalish(X_4,A_73)
| element(k,A_73)
| ~ element(A_73,a) ),
inference(resolution,[status(thm)],[c_958,c_6]) ).
tff(c_52513,plain,
( equalish(n,k)
| element(k,m)
| ~ element(m,a) ),
inference(resolution,[status(thm)],[c_52432,c_1019]) ).
tff(c_52648,plain,
( equalish(n,k)
| element(k,m) ),
inference(demodulation,[status(thm),theory(equality)],[c_234,c_52513]) ).
tff(c_52650,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_487,c_46,c_52648]) ).
tff(c_52652,plain,
~ equalish(n,m),
inference(splitRight,[status(thm)],[c_20752]) ).
tff(c_143,plain,
! [B_48] :
( element(n,B_48)
| ~ equalish(k,B_48) ),
inference(resolution,[status(thm)],[c_116,c_136]) ).
tff(c_147,plain,
( element(n,m)
| ~ equalish(k,k) ),
inference(resolution,[status(thm)],[c_73,c_143]) ).
tff(c_157,plain,
element(n,m),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_147]) ).
tff(c_20,plain,
! [A_17] :
( equalish(A_17,m)
| ~ element(A_17,m)
| element(A_17,f(A_17)) ),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_6303,plain,
! [B_145,A_146] :
( element(n,B_145)
| ~ element(A_146,B_145)
| equalish(A_146,k)
| equalish(A_146,m)
| ~ element(A_146,k) ),
inference(resolution,[status(thm)],[c_1203,c_10]) ).
tff(c_6351,plain,
! [A_17] :
( element(n,f(A_17))
| equalish(A_17,k)
| ~ element(A_17,k)
| equalish(A_17,m)
| ~ element(A_17,m) ),
inference(resolution,[status(thm)],[c_20,c_6303]) ).
tff(c_246,plain,
! [A_52] :
( equalish(A_52,m)
| ~ element(A_52,m)
| element(f(A_52),A_52) ),
inference(cnfTransformation,[status(thm)],[f_100]) ).
tff(c_249,plain,
! [A_52,B_8] :
( element(f(A_52),B_8)
| ~ equalish(A_52,B_8)
| equalish(A_52,m)
| ~ element(A_52,m) ),
inference(resolution,[status(thm)],[c_246,c_8]) ).
tff(c_2350,plain,
( equalish(a,k)
| equalish(a,m)
| ~ element(a,k) ),
inference(resolution,[status(thm)],[c_2311,c_42]) ).
tff(c_2418,plain,
( equalish(a,m)
| ~ element(a,k) ),
inference(negUnitSimplification,[status(thm)],[c_286,c_2350]) ).
tff(c_2435,plain,
~ element(a,k),
inference(splitLeft,[status(thm)],[c_2418]) ).
tff(c_2567,plain,
! [A_92] :
( equalish(A_92,n)
| equalish(A_92,k)
| ~ element(A_92,k) ),
inference(resolution,[status(thm)],[c_2436,c_4]) ).
tff(c_18,plain,
! [A_16] :
( equalish(A_16,m)
| ~ element(A_16,m)
| ~ equalish(f(A_16),A_16) ),
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_2579,plain,
( equalish(n,m)
| ~ element(n,m)
| equalish(f(n),k)
| ~ element(f(n),k) ),
inference(resolution,[status(thm)],[c_2567,c_18]) ).
tff(c_2630,plain,
( equalish(n,m)
| equalish(f(n),k)
| ~ element(f(n),k) ),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_2579]) ).
tff(c_5438,plain,
~ element(f(n),k),
inference(splitLeft,[status(thm)],[c_2630]) ).
tff(c_7584,plain,
! [A_163,B_164] :
( element(A_163,B_164)
| ~ element(n,B_164)
| equalish(A_163,k)
| ~ element(A_163,k) ),
inference(resolution,[status(thm)],[c_2436,c_10]) ).
tff(c_7618,plain,
! [A_165] :
( element(A_165,m)
| equalish(A_165,k)
| ~ element(A_165,k) ),
inference(resolution,[status(thm)],[c_157,c_7584]) ).
tff(c_7934,plain,
! [A_168] :
( equalish(k,A_168)
| element(A_168,m)
| ~ element(A_168,k) ),
inference(resolution,[status(thm)],[c_7618,c_4]) ).
tff(c_142,plain,
! [B_46] :
( element(n,B_46)
| ~ equalish(k,B_46) ),
inference(resolution,[status(thm)],[c_116,c_136]) ).
tff(c_8096,plain,
! [A_171] :
( element(n,A_171)
| element(A_171,m)
| ~ element(A_171,k) ),
inference(resolution,[status(thm)],[c_7934,c_142]) ).
tff(c_126,plain,
! [B_41,X_33] :
( element(m,B_41)
| ~ element(X_33,B_41)
| ~ equalish(X_33,k) ),
inference(resolution,[status(thm)],[c_73,c_117]) ).
tff(c_8187,plain,
! [A_171] :
( element(m,m)
| ~ equalish(A_171,k)
| element(n,A_171)
| ~ element(A_171,k) ),
inference(resolution,[status(thm)],[c_8096,c_126]) ).
tff(c_43628,plain,
element(m,m),
inference(splitLeft,[status(thm)],[c_8187]) ).
tff(c_1017,plain,
! [B_11,A_73] :
( element(k,B_11)
| ~ element(A_73,B_11)
| element(k,A_73)
| ~ element(A_73,a) ),
inference(resolution,[status(thm)],[c_958,c_10]) ).
tff(c_43684,plain,
( element(k,m)
| ~ element(m,a) ),
inference(resolution,[status(thm)],[c_43628,c_1017]) ).
tff(c_43786,plain,
element(k,m),
inference(demodulation,[status(thm),theory(equality)],[c_234,c_43684]) ).
tff(c_43788,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_487,c_43786]) ).
tff(c_43790,plain,
~ element(m,m),
inference(splitRight,[status(thm)],[c_8187]) ).
tff(c_98,plain,
! [X_37] :
( equalish(m,X_37)
| ~ equalish(X_37,k) ),
inference(resolution,[status(thm)],[c_88,c_4]) ).
tff(c_211,plain,
! [A_50] :
( equalish(m,A_50)
| equalish(A_50,a)
| ~ element(A_50,a) ),
inference(resolution,[status(thm)],[c_184,c_98]) ).
tff(c_1168,plain,
! [A_77] :
( equalish(A_77,n)
| element(A_77,n)
| element(A_77,g(A_77)) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_129,plain,
! [B_41] :
( element(k,B_41)
| ~ element(m,B_41) ),
inference(resolution,[status(thm)],[c_52,c_117]) ).
tff(c_1176,plain,
( element(k,g(m))
| equalish(m,n)
| element(m,n) ),
inference(resolution,[status(thm)],[c_1168,c_129]) ).
tff(c_1181,plain,
( element(k,g(m))
| element(m,n) ),
inference(negUnitSimplification,[status(thm)],[c_44,c_1176]) ).
tff(c_1182,plain,
element(m,n),
inference(splitLeft,[status(thm)],[c_1181]) ).
tff(c_1194,plain,
element(k,n),
inference(resolution,[status(thm)],[c_1182,c_129]) ).
tff(c_20426,plain,
! [A_283] :
( element(A_283,n)
| equalish(A_283,n)
| ~ element(A_283,k) ),
inference(resolution,[status(thm)],[c_1194,c_20236]) ).
tff(c_20772,plain,
! [A_285] :
( equalish(n,A_285)
| element(A_285,n)
| ~ element(A_285,k) ),
inference(resolution,[status(thm)],[c_20426,c_4]) ).
tff(c_61570,plain,
! [A_557,B_558] :
( element(A_557,B_558)
| ~ element(n,B_558)
| element(A_557,n)
| ~ element(A_557,k) ),
inference(resolution,[status(thm)],[c_20772,c_10]) ).
tff(c_61597,plain,
! [A_557] :
( element(A_557,f(n))
| element(A_557,n)
| ~ element(A_557,k)
| equalish(n,m)
| ~ element(n,m) ),
inference(resolution,[status(thm)],[c_20,c_61570]) ).
tff(c_61624,plain,
! [A_557] :
( element(A_557,f(n))
| element(A_557,n)
| ~ element(A_557,k)
| equalish(n,m) ),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_61597]) ).
tff(c_61628,plain,
! [A_559] :
( element(A_559,f(n))
| element(A_559,n)
| ~ element(A_559,k) ),
inference(negUnitSimplification,[status(thm)],[c_52652,c_61624]) ).
tff(c_20573,plain,
! [B_11,A_283] :
( element(n,B_11)
| ~ element(A_283,B_11)
| element(A_283,n)
| ~ element(A_283,k) ),
inference(resolution,[status(thm)],[c_20426,c_10]) ).
tff(c_61840,plain,
! [A_559] :
( element(n,f(n))
| element(A_559,n)
| ~ element(A_559,k) ),
inference(resolution,[status(thm)],[c_61628,c_20573]) ).
tff(c_61946,plain,
element(n,f(n)),
inference(splitLeft,[status(thm)],[c_61840]) ).
tff(c_62474,plain,
! [B_561] :
( element(n,B_561)
| ~ equalish(f(n),B_561) ),
inference(resolution,[status(thm)],[c_61946,c_8]) ).
tff(c_62762,plain,
( element(n,a)
| equalish(m,f(n))
| ~ element(f(n),a) ),
inference(resolution,[status(thm)],[c_211,c_62474]) ).
tff(c_62907,plain,
( equalish(m,f(n))
| ~ element(f(n),a) ),
inference(negUnitSimplification,[status(thm)],[c_216,c_62762]) ).
tff(c_62922,plain,
~ element(f(n),a),
inference(splitLeft,[status(thm)],[c_62907]) ).
tff(c_2009,plain,
! [B_87,A_88] :
( equalish(B_87,n)
| ~ element(B_87,n)
| equalish(A_88,n)
| equalish(A_88,B_87)
| ~ element(B_87,A_88)
| ~ element(A_88,B_87) ),
inference(cnfTransformation,[status(thm)],[f_155]) ).
tff(c_21944,plain,
! [B_295,B_296,A_297] :
( element(B_295,B_296)
| ~ element(A_297,B_296)
| equalish(B_295,n)
| ~ element(B_295,n)
| equalish(A_297,n)
| ~ element(B_295,A_297)
| ~ element(A_297,B_295) ),
inference(resolution,[status(thm)],[c_2009,c_10]) ).
tff(c_21988,plain,
! [B_295] :
( element(B_295,a)
| equalish(B_295,n)
| ~ element(B_295,n)
| equalish(m,n)
| ~ element(B_295,m)
| ~ element(m,B_295) ),
inference(resolution,[status(thm)],[c_234,c_21944]) ).
tff(c_66723,plain,
! [B_574] :
( element(B_574,a)
| equalish(B_574,n)
| ~ element(B_574,n)
| ~ element(B_574,m)
| ~ element(m,B_574) ),
inference(negUnitSimplification,[status(thm)],[c_44,c_21988]) ).
tff(c_66852,plain,
( equalish(n,m)
| ~ element(n,m)
| element(f(n),a)
| ~ element(f(n),n)
| ~ element(f(n),m)
| ~ element(m,f(n)) ),
inference(resolution,[status(thm)],[c_66723,c_18]) ).
tff(c_67023,plain,
( equalish(n,m)
| element(f(n),a)
| ~ element(f(n),n)
| ~ element(f(n),m)
| ~ element(m,f(n)) ),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_66852]) ).
tff(c_67024,plain,
( ~ element(f(n),n)
| ~ element(f(n),m)
| ~ element(m,f(n)) ),
inference(negUnitSimplification,[status(thm)],[c_62922,c_52652,c_67023]) ).
tff(c_67686,plain,
~ element(m,f(n)),
inference(splitLeft,[status(thm)],[c_67024]) ).
tff(c_67730,plain,
~ element(k,f(n)),
inference(resolution,[status(thm)],[c_127,c_67686]) ).
tff(c_292,plain,
! [A_55] :
( equalish(A_55,m)
| ~ element(A_55,m)
| ~ equalish(f(A_55),m) ),
inference(cnfTransformation,[status(thm)],[f_78]) ).
tff(c_5407,plain,
! [A_132] :
( equalish(A_132,m)
| ~ element(A_132,m)
| ~ equalish(f(A_132),k) ),
inference(resolution,[status(thm)],[c_73,c_292]) ).
tff(c_96666,plain,
! [A_701] :
( equalish(A_701,m)
| ~ element(A_701,m)
| equalish(f(A_701),a)
| ~ element(f(A_701),a) ),
inference(resolution,[status(thm)],[c_12,c_5407]) ).
tff(c_681,plain,
! [A_68] :
( equalish(A_68,m)
| ~ element(A_68,m)
| element(A_68,f(A_68)) ),
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_691,plain,
! [A_68,B_8] :
( element(A_68,B_8)
| ~ equalish(f(A_68),B_8)
| equalish(A_68,m)
| ~ element(A_68,m) ),
inference(resolution,[status(thm)],[c_681,c_8]) ).
tff(c_96960,plain,
! [A_702] :
( element(A_702,a)
| equalish(A_702,m)
| ~ element(A_702,m)
| ~ element(f(A_702),a) ),
inference(resolution,[status(thm)],[c_96666,c_691]) ).
tff(c_98350,plain,
! [A_705] :
( element(A_705,a)
| ~ equalish(A_705,a)
| equalish(A_705,m)
| ~ element(A_705,m) ),
inference(resolution,[status(thm)],[c_249,c_96960]) ).
tff(c_488,plain,
! [A_63] :
( equalish(A_63,n)
| element(A_63,n)
| element(g(A_63),A_63) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_4096,plain,
! [A_111,B_112] :
( element(g(A_111),B_112)
| ~ equalish(A_111,B_112)
| equalish(A_111,n)
| element(A_111,n) ),
inference(resolution,[status(thm)],[c_488,c_8]) ).
tff(c_69606,plain,
! [A_590,B_591,B_592] :
( element(g(A_590),B_591)
| ~ equalish(B_592,B_591)
| ~ equalish(A_590,B_592)
| equalish(A_590,n)
| element(A_590,n) ),
inference(resolution,[status(thm)],[c_4096,c_8]) ).
tff(c_70008,plain,
! [A_590] :
( element(g(A_590),k)
| ~ equalish(A_590,m)
| equalish(A_590,n)
| element(A_590,n) ),
inference(resolution,[status(thm)],[c_52,c_69606]) ).
tff(c_26,plain,
! [A_21] :
( equalish(A_21,n)
| element(A_21,n)
| ~ equalish(g(A_21),n) ),
inference(cnfTransformation,[status(thm)],[f_121]) ).
tff(c_8010,plain,
! [A_169] :
( equalish(A_169,n)
| element(A_169,n)
| equalish(g(A_169),k)
| equalish(g(A_169),m)
| ~ element(g(A_169),k) ),
inference(resolution,[status(thm)],[c_1203,c_26]) ).
tff(c_55352,plain,
! [A_524] :
( equalish(A_524,n)
| element(A_524,n)
| equalish(g(A_524),k)
| ~ element(g(A_524),k) ),
inference(resolution,[status(thm)],[c_8010,c_75]) ).
tff(c_1178,plain,
! [A_77,B_8] :
( element(A_77,B_8)
| ~ equalish(g(A_77),B_8)
| equalish(A_77,n)
| element(A_77,n) ),
inference(resolution,[status(thm)],[c_1168,c_8]) ).
tff(c_75705,plain,
! [A_630] :
( element(A_630,k)
| equalish(A_630,n)
| element(A_630,n)
| ~ element(g(A_630),k) ),
inference(resolution,[status(thm)],[c_55352,c_1178]) ).
tff(c_75722,plain,
! [A_631] :
( element(A_631,k)
| ~ equalish(A_631,m)
| equalish(A_631,n)
| element(A_631,n) ),
inference(resolution,[status(thm)],[c_70008,c_75705]) ).
tff(c_75881,plain,
( equalish(n,m)
| ~ element(n,m)
| element(f(n),k)
| ~ equalish(f(n),m)
| element(f(n),n) ),
inference(resolution,[status(thm)],[c_75722,c_18]) ).
tff(c_76066,plain,
( equalish(n,m)
| element(f(n),k)
| ~ equalish(f(n),m)
| element(f(n),n) ),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_75881]) ).
tff(c_76067,plain,
( ~ equalish(f(n),m)
| element(f(n),n) ),
inference(negUnitSimplification,[status(thm)],[c_5438,c_52652,c_76066]) ).
tff(c_76094,plain,
~ equalish(f(n),m),
inference(splitLeft,[status(thm)],[c_76067]) ).
tff(c_98389,plain,
( element(f(n),a)
| ~ equalish(f(n),a)
| ~ element(f(n),m) ),
inference(resolution,[status(thm)],[c_98350,c_76094]) ).
tff(c_98624,plain,
( ~ equalish(f(n),a)
| ~ element(f(n),m) ),
inference(negUnitSimplification,[status(thm)],[c_62922,c_98389]) ).
tff(c_98829,plain,
~ element(f(n),m),
inference(splitLeft,[status(thm)],[c_98624]) ).
tff(c_5755,plain,
! [B_140] :
( equalish(B_140,n)
| ~ element(B_140,n)
| equalish(m,B_140)
| ~ element(B_140,m)
| ~ element(m,B_140) ),
inference(resolution,[status(thm)],[c_2009,c_44]) ).
tff(c_5845,plain,
( equalish(a,n)
| ~ element(a,n)
| ~ element(a,m)
| ~ element(m,a) ),
inference(resolution,[status(thm)],[c_5755,c_48]) ).
tff(c_5899,plain,
( equalish(a,n)
| ~ element(a,n)
| ~ element(a,m) ),
inference(demodulation,[status(thm),theory(equality)],[c_234,c_5845]) ).
tff(c_5900,plain,
~ element(a,m),
inference(splitLeft,[status(thm)],[c_5899]) ).
tff(c_1656,plain,
! [B_84,A_85] :
( equalish(B_84,m)
| element(B_84,m)
| equalish(A_85,m)
| equalish(A_85,B_84)
| ~ element(B_84,A_85)
| ~ element(A_85,B_84) ),
inference(cnfTransformation,[status(thm)],[f_114]) ).
tff(c_21207,plain,
! [B_289,A_290,B_291] :
( element(m,B_289)
| ~ element(A_290,B_289)
| equalish(B_291,m)
| element(B_291,m)
| equalish(A_290,B_291)
| ~ element(B_291,A_290)
| ~ element(A_290,B_291) ),
inference(resolution,[status(thm)],[c_1656,c_10]) ).
tff(c_21277,plain,
! [B_291] :
( element(m,k)
| equalish(B_291,m)
| element(B_291,m)
| equalish(n,B_291)
| ~ element(B_291,n)
| ~ element(n,B_291) ),
inference(resolution,[status(thm)],[c_116,c_21207]) ).
tff(c_106634,plain,
element(m,k),
inference(splitLeft,[status(thm)],[c_21277]) ).
tff(c_2432,plain,
! [A_90] :
( equalish(n,A_90)
| equalish(A_90,k)
| ~ element(A_90,k) ),
inference(resolution,[status(thm)],[c_2311,c_75]) ).
tff(c_491,plain,
! [A_63,B_8] :
( element(g(A_63),B_8)
| ~ equalish(A_63,B_8)
| equalish(A_63,n)
| element(A_63,n) ),
inference(resolution,[status(thm)],[c_488,c_8]) ).
tff(c_213,plain,
! [A_50] :
( equalish(k,A_50)
| equalish(A_50,a)
| ~ element(A_50,a) ),
inference(resolution,[status(thm)],[c_184,c_4]) ).
tff(c_1022,plain,
! [A_74] :
( equalish(A_74,n)
| element(A_74,n)
| ~ equalish(g(A_74),A_74) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_1067,plain,
( equalish(a,n)
| element(a,n)
| equalish(k,g(a))
| ~ element(g(a),a) ),
inference(resolution,[status(thm)],[c_213,c_1022]) ).
tff(c_52653,plain,
~ element(g(a),a),
inference(splitLeft,[status(thm)],[c_1067]) ).
tff(c_52844,plain,
( ~ equalish(a,a)
| equalish(a,n)
| element(a,n) ),
inference(resolution,[status(thm)],[c_491,c_52653]) ).
tff(c_52850,plain,
( equalish(a,n)
| element(a,n) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_52844]) ).
tff(c_52852,plain,
element(a,n),
inference(splitLeft,[status(thm)],[c_52850]) ).
tff(c_53034,plain,
! [B_517] :
( element(a,B_517)
| ~ equalish(n,B_517) ),
inference(resolution,[status(thm)],[c_52852,c_8]) ).
tff(c_53903,plain,
! [A_519] :
( element(a,A_519)
| equalish(A_519,k)
| ~ element(A_519,k) ),
inference(resolution,[status(thm)],[c_2432,c_53034]) ).
tff(c_54232,plain,
! [B_11,A_519] :
( element(k,B_11)
| ~ element(A_519,B_11)
| element(a,A_519)
| ~ element(A_519,k) ),
inference(resolution,[status(thm)],[c_53903,c_10]) ).
tff(c_106652,plain,
( element(k,k)
| element(a,m)
| ~ element(m,k) ),
inference(resolution,[status(thm)],[c_106634,c_54232]) ).
tff(c_106792,plain,
( element(k,k)
| element(a,m) ),
inference(demodulation,[status(thm),theory(equality)],[c_106634,c_106652]) ).
tff(c_106794,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_5900,c_486,c_106792]) ).
tff(c_106818,plain,
! [B_732] :
( equalish(B_732,m)
| element(B_732,m)
| equalish(n,B_732)
| ~ element(B_732,n)
| ~ element(n,B_732) ),
inference(splitRight,[status(thm)],[c_21277]) ).
tff(c_106857,plain,
( element(f(n),m)
| equalish(n,f(n))
| ~ element(f(n),n)
| ~ element(n,f(n)) ),
inference(resolution,[status(thm)],[c_106818,c_76094]) ).
tff(c_107384,plain,
( element(f(n),m)
| equalish(n,f(n))
| ~ element(f(n),n) ),
inference(demodulation,[status(thm),theory(equality)],[c_61946,c_106857]) ).
tff(c_107385,plain,
( equalish(n,f(n))
| ~ element(f(n),n) ),
inference(negUnitSimplification,[status(thm)],[c_98829,c_107384]) ).
tff(c_107858,plain,
~ element(f(n),n),
inference(splitLeft,[status(thm)],[c_107385]) ).
tff(c_107876,plain,
( ~ equalish(n,n)
| equalish(n,m)
| ~ element(n,m) ),
inference(resolution,[status(thm)],[c_249,c_107858]) ).
tff(c_107890,plain,
equalish(n,m),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_2,c_107876]) ).
tff(c_107892,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_52652,c_107890]) ).
tff(c_107893,plain,
equalish(n,f(n)),
inference(splitRight,[status(thm)],[c_107385]) ).
tff(c_1202,plain,
! [B_8] :
( element(k,B_8)
| ~ equalish(n,B_8) ),
inference(resolution,[status(thm)],[c_1194,c_8]) ).
tff(c_108545,plain,
element(k,f(n)),
inference(resolution,[status(thm)],[c_107893,c_1202]) ).
tff(c_108677,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_67730,c_108545]) ).
tff(c_108679,plain,
element(f(n),m),
inference(splitRight,[status(thm)],[c_98624]) ).
tff(c_108946,plain,
! [B_734] :
( element(f(n),B_734)
| ~ equalish(m,B_734) ),
inference(resolution,[status(thm)],[c_108679,c_8]) ).
tff(c_1193,plain,
! [B_8] :
( element(m,B_8)
| ~ equalish(n,B_8) ),
inference(resolution,[status(thm)],[c_1182,c_8]) ).
tff(c_20748,plain,
! [A_284] :
( element(m,A_284)
| element(A_284,a)
| ~ element(A_284,k) ),
inference(resolution,[status(thm)],[c_20579,c_1193]) ).
tff(c_109066,plain,
( element(m,f(n))
| element(f(n),a)
| ~ equalish(m,k) ),
inference(resolution,[status(thm)],[c_108946,c_20748]) ).
tff(c_109212,plain,
( element(m,f(n))
| element(f(n),a) ),
inference(demodulation,[status(thm),theory(equality)],[c_52,c_109066]) ).
tff(c_109214,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_62922,c_67686,c_109212]) ).
tff(c_109216,plain,
equalish(f(n),m),
inference(splitRight,[status(thm)],[c_76067]) ).
tff(c_16,plain,
! [A_15] :
( equalish(A_15,m)
| ~ element(A_15,m)
| ~ equalish(f(A_15),m) ),
inference(cnfTransformation,[status(thm)],[f_78]) ).
tff(c_109344,plain,
( equalish(n,m)
| ~ element(n,m) ),
inference(resolution,[status(thm)],[c_109216,c_16]) ).
tff(c_109499,plain,
equalish(n,m),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_109344]) ).
tff(c_109501,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_52652,c_109499]) ).
tff(c_109503,plain,
element(m,f(n)),
inference(splitRight,[status(thm)],[c_67024]) ).
tff(c_38,plain,
! [A_28] :
( equalish(A_28,k)
| element(A_28,k)
| ~ equalish(A_28,n) ),
inference(cnfTransformation,[status(thm)],[f_169]) ).
tff(c_31148,plain,
! [A_381,B_382] :
( equalish(A_381,k)
| element(A_381,k)
| equalish(B_382,n)
| ~ element(B_382,n)
| equalish(A_381,B_382)
| ~ element(B_382,A_381)
| ~ element(A_381,B_382) ),
inference(resolution,[status(thm)],[c_2009,c_38]) ).
tff(c_31560,plain,
! [A_381] :
( equalish(A_381,k)
| element(A_381,k)
| equalish(m,n)
| ~ element(m,n)
| ~ element(m,A_381)
| ~ element(A_381,m) ),
inference(resolution,[status(thm)],[c_31148,c_75]) ).
tff(c_31860,plain,
! [A_381] :
( equalish(A_381,k)
| element(A_381,k)
| equalish(m,n)
| ~ element(m,A_381)
| ~ element(A_381,m) ),
inference(demodulation,[status(thm),theory(equality)],[c_1182,c_31560]) ).
tff(c_31864,plain,
! [A_383] :
( equalish(A_383,k)
| element(A_383,k)
| ~ element(m,A_383)
| ~ element(A_383,m) ),
inference(negUnitSimplification,[status(thm)],[c_44,c_31860]) ).
tff(c_31967,plain,
! [A_383] :
( equalish(A_383,m)
| ~ equalish(k,k)
| element(A_383,k)
| ~ element(m,A_383)
| ~ element(A_383,m) ),
inference(resolution,[status(thm)],[c_31864,c_97]) ).
tff(c_32094,plain,
! [A_383] :
( equalish(A_383,m)
| element(A_383,k)
| ~ element(m,A_383)
| ~ element(A_383,m) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_31967]) ).
tff(c_109962,plain,
! [B_735] :
( element(m,B_735)
| ~ equalish(f(n),B_735) ),
inference(resolution,[status(thm)],[c_109503,c_8]) ).
tff(c_110030,plain,
( element(m,m)
| element(f(n),k)
| ~ element(m,f(n))
| ~ element(f(n),m) ),
inference(resolution,[status(thm)],[c_32094,c_109962]) ).
tff(c_110322,plain,
( element(m,m)
| element(f(n),k)
| ~ element(f(n),m) ),
inference(demodulation,[status(thm),theory(equality)],[c_109503,c_110030]) ).
tff(c_110323,plain,
~ element(f(n),m),
inference(negUnitSimplification,[status(thm)],[c_5438,c_43790,c_110322]) ).
tff(c_175616,plain,
element(m,k),
inference(splitLeft,[status(thm)],[c_21277]) ).
tff(c_175634,plain,
( element(k,k)
| element(a,m)
| ~ element(m,k) ),
inference(resolution,[status(thm)],[c_175616,c_54232]) ).
tff(c_175776,plain,
( element(k,k)
| element(a,m) ),
inference(demodulation,[status(thm),theory(equality)],[c_175616,c_175634]) ).
tff(c_175778,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_5900,c_486,c_175776]) ).
tff(c_175790,plain,
! [B_946] :
( equalish(B_946,m)
| element(B_946,m)
| equalish(n,B_946)
| ~ element(B_946,n)
| ~ element(n,B_946) ),
inference(splitRight,[status(thm)],[c_21277]) ).
tff(c_210,plain,
! [B_11,A_50] :
( element(k,B_11)
| ~ element(A_50,B_11)
| equalish(A_50,a)
| ~ element(A_50,a) ),
inference(resolution,[status(thm)],[c_184,c_10]) ).
tff(c_109599,plain,
( element(k,f(n))
| equalish(m,a)
| ~ element(m,a) ),
inference(resolution,[status(thm)],[c_109503,c_210]) ).
tff(c_109726,plain,
( element(k,f(n))
| equalish(m,a) ),
inference(demodulation,[status(thm),theory(equality)],[c_234,c_109599]) ).
tff(c_109727,plain,
element(k,f(n)),
inference(negUnitSimplification,[status(thm)],[c_48,c_109726]) ).
tff(c_109960,plain,
! [B_8] :
( element(k,B_8)
| ~ equalish(f(n),B_8) ),
inference(resolution,[status(thm)],[c_109727,c_8]) ).
tff(c_175883,plain,
( element(k,m)
| element(f(n),m)
| equalish(n,f(n))
| ~ element(f(n),n)
| ~ element(n,f(n)) ),
inference(resolution,[status(thm)],[c_175790,c_109960]) ).
tff(c_176449,plain,
( element(k,m)
| element(f(n),m)
| equalish(n,f(n))
| ~ element(f(n),n) ),
inference(demodulation,[status(thm),theory(equality)],[c_61946,c_175883]) ).
tff(c_176450,plain,
( equalish(n,f(n))
| ~ element(f(n),n) ),
inference(negUnitSimplification,[status(thm)],[c_110323,c_487,c_176449]) ).
tff(c_176916,plain,
~ element(f(n),n),
inference(splitLeft,[status(thm)],[c_176450]) ).
tff(c_176934,plain,
( ~ equalish(n,n)
| equalish(n,m)
| ~ element(n,m) ),
inference(resolution,[status(thm)],[c_249,c_176916]) ).
tff(c_176948,plain,
equalish(n,m),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_2,c_176934]) ).
tff(c_176950,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_52652,c_176948]) ).
tff(c_176951,plain,
equalish(n,f(n)),
inference(splitRight,[status(thm)],[c_176450]) ).
tff(c_177804,plain,
equalish(f(n),n),
inference(resolution,[status(thm)],[c_176951,c_4]) ).
tff(c_178173,plain,
( equalish(n,m)
| ~ element(n,m) ),
inference(resolution,[status(thm)],[c_177804,c_18]) ).
tff(c_178361,plain,
equalish(n,m),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_178173]) ).
tff(c_178363,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_52652,c_178361]) ).
tff(c_178364,plain,
equalish(m,f(n)),
inference(splitRight,[status(thm)],[c_62907]) ).
tff(c_178554,plain,
equalish(f(n),m),
inference(resolution,[status(thm)],[c_178364,c_4]) ).
tff(c_179420,plain,
( equalish(n,m)
| ~ element(n,m) ),
inference(resolution,[status(thm)],[c_178554,c_16]) ).
tff(c_179565,plain,
equalish(n,m),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_179420]) ).
tff(c_179567,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_52652,c_179565]) ).
tff(c_179569,plain,
~ element(n,f(n)),
inference(splitRight,[status(thm)],[c_61840]) ).
tff(c_179576,plain,
( equalish(n,m)
| ~ element(n,m) ),
inference(resolution,[status(thm)],[c_20,c_179569]) ).
tff(c_179582,plain,
equalish(n,m),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_179576]) ).
tff(c_179584,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_52652,c_179582]) ).
tff(c_179586,plain,
~ element(a,n),
inference(splitRight,[status(thm)],[c_52850]) ).
tff(c_32,plain,
! [A_24] :
( equalish(A_24,n)
| element(A_24,n)
| element(g(A_24),A_24) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_52851,plain,
( equalish(a,n)
| element(a,n) ),
inference(resolution,[status(thm)],[c_32,c_52653]) ).
tff(c_179604,plain,
equalish(a,n),
inference(negUnitSimplification,[status(thm)],[c_179586,c_52851]) ).
tff(c_179717,plain,
( equalish(a,k)
| element(a,k) ),
inference(resolution,[status(thm)],[c_179604,c_38]) ).
tff(c_179867,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_2435,c_286,c_179717]) ).
tff(c_179869,plain,
element(g(a),a),
inference(splitRight,[status(thm)],[c_1067]) ).
tff(c_2566,plain,
! [A_91] :
( equalish(k,A_91)
| equalish(n,A_91)
| ~ element(A_91,k) ),
inference(resolution,[status(thm)],[c_2436,c_4]) ).
tff(c_5968,plain,
! [X_142,A_143] :
( equalish(X_142,a)
| ~ equalish(X_142,A_143)
| equalish(k,A_143)
| ~ element(A_143,a) ),
inference(resolution,[status(thm)],[c_297,c_6]) ).
tff(c_6032,plain,
! [A_91] :
( equalish(n,a)
| ~ element(A_91,a)
| equalish(k,A_91)
| ~ element(A_91,k) ),
inference(resolution,[status(thm)],[c_2566,c_5968]) ).
tff(c_6163,plain,
! [A_91] :
( ~ element(A_91,a)
| equalish(k,A_91)
| ~ element(A_91,k) ),
inference(negUnitSimplification,[status(thm)],[c_42,c_6032]) ).
tff(c_2061,plain,
! [A_88] :
( ~ element(m,n)
| equalish(A_88,n)
| equalish(A_88,m)
| ~ element(m,A_88)
| ~ element(A_88,m) ),
inference(resolution,[status(thm)],[c_2009,c_44]) ).
tff(c_6947,plain,
! [A_155] :
( equalish(A_155,n)
| equalish(A_155,m)
| ~ element(m,A_155)
| ~ element(A_155,m) ),
inference(demodulation,[status(thm),theory(equality)],[c_1182,c_2061]) ).
tff(c_8861,plain,
! [A_178] :
( equalish(n,A_178)
| equalish(A_178,m)
| ~ element(m,A_178)
| ~ element(A_178,m) ),
inference(resolution,[status(thm)],[c_6947,c_4]) ).
tff(c_212,plain,
! [X_4,A_50] :
( equalish(X_4,k)
| ~ equalish(X_4,A_50)
| equalish(A_50,a)
| ~ element(A_50,a) ),
inference(resolution,[status(thm)],[c_184,c_6]) ).
tff(c_8936,plain,
! [A_178] :
( equalish(A_178,k)
| equalish(m,a)
| ~ element(m,a)
| equalish(n,A_178)
| ~ element(m,A_178)
| ~ element(A_178,m) ),
inference(resolution,[status(thm)],[c_8861,c_212]) ).
tff(c_9030,plain,
! [A_178] :
( equalish(A_178,k)
| equalish(m,a)
| equalish(n,A_178)
| ~ element(m,A_178)
| ~ element(A_178,m) ),
inference(demodulation,[status(thm),theory(equality)],[c_234,c_8936]) ).
tff(c_9031,plain,
! [A_178] :
( equalish(A_178,k)
| equalish(n,A_178)
| ~ element(m,A_178)
| ~ element(A_178,m) ),
inference(negUnitSimplification,[status(thm)],[c_48,c_9030]) ).
tff(c_362,plain,
! [B_11,A_56] :
( element(a,B_11)
| ~ element(A_56,B_11)
| equalish(k,A_56)
| ~ element(A_56,a) ),
inference(resolution,[status(thm)],[c_297,c_10]) ).
tff(c_180131,plain,
( element(a,a)
| equalish(k,g(a))
| ~ element(g(a),a) ),
inference(resolution,[status(thm)],[c_179869,c_362]) ).
tff(c_180238,plain,
( element(a,a)
| equalish(k,g(a)) ),
inference(demodulation,[status(thm),theory(equality)],[c_179869,c_180131]) ).
tff(c_180247,plain,
equalish(k,g(a)),
inference(splitLeft,[status(thm)],[c_180238]) ).
tff(c_180443,plain,
equalish(g(a),k),
inference(resolution,[status(thm)],[c_180247,c_4]) ).
tff(c_180902,plain,
equalish(m,g(a)),
inference(resolution,[status(thm)],[c_180443,c_98]) ).
tff(c_185305,plain,
! [B_960] :
( element(g(a),B_960)
| ~ element(m,B_960) ),
inference(resolution,[status(thm)],[c_180902,c_10]) ).
tff(c_208216,plain,
! [B_1045,B_1046] :
( element(g(a),B_1045)
| ~ equalish(B_1046,B_1045)
| ~ element(m,B_1046) ),
inference(resolution,[status(thm)],[c_185305,c_8]) ).
tff(c_208758,plain,
! [X_33] :
( element(g(a),m)
| ~ element(m,X_33)
| ~ equalish(X_33,k) ),
inference(resolution,[status(thm)],[c_73,c_208216]) ).
tff(c_222360,plain,
! [X_1089] :
( ~ element(m,X_1089)
| ~ equalish(X_1089,k) ),
inference(splitLeft,[status(thm)],[c_208758]) ).
tff(c_227328,plain,
! [A_1102] :
( equalish(n,A_1102)
| ~ element(m,A_1102)
| ~ element(A_1102,m) ),
inference(resolution,[status(thm)],[c_9031,c_222360]) ).
tff(c_228182,plain,
! [A_1104] :
( equalish(A_1104,n)
| ~ element(m,A_1104)
| ~ element(A_1104,m) ),
inference(resolution,[status(thm)],[c_227328,c_4]) ).
tff(c_228324,plain,
( equalish(n,m)
| ~ element(n,m)
| ~ element(m,f(n))
| ~ element(f(n),m) ),
inference(resolution,[status(thm)],[c_228182,c_18]) ).
tff(c_228495,plain,
( equalish(n,m)
| ~ element(m,f(n))
| ~ element(f(n),m) ),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_228324]) ).
tff(c_228496,plain,
( ~ element(m,f(n))
| ~ element(f(n),m) ),
inference(negUnitSimplification,[status(thm)],[c_52652,c_228495]) ).
tff(c_228925,plain,
~ element(f(n),m),
inference(splitLeft,[status(thm)],[c_228496]) ).
tff(c_259221,plain,
! [A_1185,B_1186] :
( element(A_1185,B_1186)
| ~ element(n,B_1186)
| element(A_1185,n)
| ~ element(A_1185,k) ),
inference(resolution,[status(thm)],[c_20772,c_10]) ).
tff(c_259273,plain,
! [A_1185] :
( element(A_1185,f(n))
| element(A_1185,n)
| ~ element(A_1185,k)
| equalish(n,m)
| ~ element(n,m) ),
inference(resolution,[status(thm)],[c_20,c_259221]) ).
tff(c_259327,plain,
! [A_1185] :
( element(A_1185,f(n))
| element(A_1185,n)
| ~ element(A_1185,k)
| equalish(n,m) ),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_259273]) ).
tff(c_259772,plain,
! [A_1188] :
( element(A_1188,f(n))
| element(A_1188,n)
| ~ element(A_1188,k) ),
inference(negUnitSimplification,[status(thm)],[c_52652,c_259327]) ).
tff(c_260044,plain,
! [A_1188] :
( element(n,f(n))
| element(A_1188,n)
| ~ element(A_1188,k) ),
inference(resolution,[status(thm)],[c_259772,c_20573]) ).
tff(c_262083,plain,
element(n,f(n)),
inference(splitLeft,[status(thm)],[c_260044]) ).
tff(c_262294,plain,
! [B_1191] :
( element(n,B_1191)
| ~ equalish(f(n),B_1191) ),
inference(resolution,[status(thm)],[c_262083,c_8]) ).
tff(c_262734,plain,
( element(n,a)
| equalish(m,f(n))
| ~ element(f(n),a) ),
inference(resolution,[status(thm)],[c_211,c_262294]) ).
tff(c_262972,plain,
( equalish(m,f(n))
| ~ element(f(n),a) ),
inference(negUnitSimplification,[status(thm)],[c_216,c_262734]) ).
tff(c_262987,plain,
~ element(f(n),a),
inference(splitLeft,[status(thm)],[c_262972]) ).
tff(c_22,plain,
! [A_18] :
( equalish(A_18,m)
| ~ element(A_18,m)
| element(f(A_18),A_18) ),
inference(cnfTransformation,[status(thm)],[f_100]) ).
tff(c_13405,plain,
! [A_215,B_216] :
( equalish(m,A_215)
| equalish(B_216,m)
| element(B_216,m)
| equalish(A_215,B_216)
| ~ element(B_216,A_215)
| ~ element(A_215,B_216) ),
inference(resolution,[status(thm)],[c_1656,c_4]) ).
tff(c_314707,plain,
! [B_1385,B_1386,A_1387] :
( element(B_1385,B_1386)
| ~ element(A_1387,B_1386)
| equalish(m,A_1387)
| equalish(B_1385,m)
| element(B_1385,m)
| ~ element(B_1385,A_1387)
| ~ element(A_1387,B_1385) ),
inference(resolution,[status(thm)],[c_13405,c_10]) ).
tff(c_314833,plain,
! [B_1385] :
( equalish(m,n)
| equalish(B_1385,m)
| element(B_1385,m)
| ~ element(B_1385,n)
| ~ element(n,B_1385) ),
inference(resolution,[status(thm)],[c_157,c_314707]) ).
tff(c_314940,plain,
! [B_1388] :
( equalish(B_1388,m)
| element(B_1388,m)
| ~ element(B_1388,n)
| ~ element(n,B_1388) ),
inference(negUnitSimplification,[status(thm)],[c_44,c_314833]) ).
tff(c_315233,plain,
! [B_1388] :
( equalish(B_1388,k)
| equalish(m,a)
| ~ element(m,a)
| element(B_1388,m)
| ~ element(B_1388,n)
| ~ element(n,B_1388) ),
inference(resolution,[status(thm)],[c_314940,c_212]) ).
tff(c_315530,plain,
! [B_1388] :
( equalish(B_1388,k)
| equalish(m,a)
| element(B_1388,m)
| ~ element(B_1388,n)
| ~ element(n,B_1388) ),
inference(demodulation,[status(thm),theory(equality)],[c_234,c_315233]) ).
tff(c_315570,plain,
! [B_1389] :
( equalish(B_1389,k)
| element(B_1389,m)
| ~ element(B_1389,n)
| ~ element(n,B_1389) ),
inference(negUnitSimplification,[status(thm)],[c_48,c_315530]) ).
tff(c_183341,plain,
! [X_954] :
( equalish(X_954,g(a))
| ~ equalish(X_954,k) ),
inference(resolution,[status(thm)],[c_180247,c_6]) ).
tff(c_183677,plain,
! [X_956] :
( equalish(g(a),X_956)
| ~ equalish(X_956,k) ),
inference(resolution,[status(thm)],[c_183341,c_4]) ).
tff(c_196565,plain,
! [X_999,B_1000] :
( element(X_999,B_1000)
| ~ element(g(a),B_1000)
| ~ equalish(X_999,k) ),
inference(resolution,[status(thm)],[c_183677,c_10]) ).
tff(c_196644,plain,
! [X_999] :
( element(X_999,a)
| ~ equalish(X_999,k) ),
inference(resolution,[status(thm)],[c_179869,c_196565]) ).
tff(c_321408,plain,
! [B_1406] :
( element(B_1406,a)
| element(B_1406,m)
| ~ element(B_1406,n)
| ~ element(n,B_1406) ),
inference(resolution,[status(thm)],[c_315570,c_196644]) ).
tff(c_321489,plain,
( element(f(n),a)
| element(f(n),m)
| ~ element(n,f(n))
| equalish(n,m)
| ~ element(n,m) ),
inference(resolution,[status(thm)],[c_22,c_321408]) ).
tff(c_321572,plain,
( element(f(n),a)
| element(f(n),m)
| equalish(n,m) ),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_262083,c_321489]) ).
tff(c_321574,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_52652,c_228925,c_262987,c_321572]) ).
tff(c_321575,plain,
equalish(m,f(n)),
inference(splitRight,[status(thm)],[c_262972]) ).
tff(c_322620,plain,
equalish(f(n),m),
inference(resolution,[status(thm)],[c_321575,c_4]) ).
tff(c_322984,plain,
( equalish(n,m)
| ~ element(n,m) ),
inference(resolution,[status(thm)],[c_322620,c_16]) ).
tff(c_323153,plain,
equalish(n,m),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_322984]) ).
tff(c_323155,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_52652,c_323153]) ).
tff(c_323157,plain,
~ element(n,f(n)),
inference(splitRight,[status(thm)],[c_260044]) ).
tff(c_323163,plain,
( equalish(n,k)
| ~ element(n,k)
| equalish(n,m)
| ~ element(n,m) ),
inference(resolution,[status(thm)],[c_6351,c_323157]) ).
tff(c_323173,plain,
( equalish(n,k)
| equalish(n,m) ),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_116,c_323163]) ).
tff(c_323175,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_52652,c_46,c_323173]) ).
tff(c_323177,plain,
element(f(n),m),
inference(splitRight,[status(thm)],[c_228496]) ).
tff(c_323467,plain,
! [B_1409] :
( element(f(n),B_1409)
| ~ equalish(m,B_1409) ),
inference(resolution,[status(thm)],[c_323177,c_8]) ).
tff(c_323568,plain,
~ equalish(m,k),
inference(resolution,[status(thm)],[c_323467,c_5438]) ).
tff(c_323671,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_52,c_323568]) ).
tff(c_323673,plain,
~ equalish(k,g(a)),
inference(splitRight,[status(thm)],[c_180238]) ).
tff(c_323905,plain,
( ~ element(g(a),a)
| ~ element(g(a),k) ),
inference(resolution,[status(thm)],[c_6163,c_323673]) ).
tff(c_323933,plain,
~ element(g(a),k),
inference(demodulation,[status(thm),theory(equality)],[c_179869,c_323905]) ).
tff(c_364,plain,
! [A_56] :
( equalish(a,A_56)
| equalish(k,A_56)
| ~ element(A_56,a) ),
inference(resolution,[status(thm)],[c_297,c_4]) ).
tff(c_323923,plain,
( equalish(a,g(a))
| ~ element(g(a),a) ),
inference(resolution,[status(thm)],[c_364,c_323673]) ).
tff(c_323944,plain,
equalish(a,g(a)),
inference(demodulation,[status(thm),theory(equality)],[c_179869,c_323923]) ).
tff(c_327556,plain,
! [B_1415] :
( element(g(a),B_1415)
| ~ element(a,B_1415) ),
inference(resolution,[status(thm)],[c_323944,c_10]) ).
tff(c_349844,plain,
! [B_1483,B_1484] :
( element(g(a),B_1483)
| ~ equalish(B_1484,B_1483)
| ~ element(a,B_1484) ),
inference(resolution,[status(thm)],[c_327556,c_8]) ).
tff(c_349966,plain,
! [A_178] :
( element(g(a),k)
| ~ element(a,A_178)
| equalish(n,A_178)
| ~ element(m,A_178)
| ~ element(A_178,m) ),
inference(resolution,[status(thm)],[c_9031,c_349844]) ).
tff(c_411706,plain,
! [A_1641] :
( ~ element(a,A_1641)
| equalish(n,A_1641)
| ~ element(m,A_1641)
| ~ element(A_1641,m) ),
inference(negUnitSimplification,[status(thm)],[c_323933,c_349966]) ).
tff(c_431226,plain,
! [A_1687] :
( equalish(A_1687,n)
| ~ element(a,A_1687)
| ~ element(m,A_1687)
| ~ element(A_1687,m) ),
inference(resolution,[status(thm)],[c_411706,c_4]) ).
tff(c_431446,plain,
( equalish(n,m)
| ~ element(n,m)
| ~ element(a,f(n))
| ~ element(m,f(n))
| ~ element(f(n),m) ),
inference(resolution,[status(thm)],[c_431226,c_18]) ).
tff(c_431687,plain,
( equalish(n,m)
| ~ element(a,f(n))
| ~ element(m,f(n))
| ~ element(f(n),m) ),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_431446]) ).
tff(c_431688,plain,
( ~ element(a,f(n))
| ~ element(m,f(n))
| ~ element(f(n),m) ),
inference(negUnitSimplification,[status(thm)],[c_52652,c_431687]) ).
tff(c_453143,plain,
~ element(f(n),m),
inference(splitLeft,[status(thm)],[c_431688]) ).
tff(c_414467,plain,
! [A_1646,B_1647] :
( element(A_1646,B_1647)
| ~ element(n,B_1647)
| element(A_1646,n)
| ~ element(A_1646,k) ),
inference(resolution,[status(thm)],[c_20772,c_10]) ).
tff(c_414547,plain,
! [A_1646] :
( element(A_1646,f(n))
| element(A_1646,n)
| ~ element(A_1646,k)
| equalish(n,m)
| ~ element(n,m) ),
inference(resolution,[status(thm)],[c_20,c_414467]) ).
tff(c_414615,plain,
! [A_1646] :
( element(A_1646,f(n))
| element(A_1646,n)
| ~ element(A_1646,k)
| equalish(n,m) ),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_414547]) ).
tff(c_414619,plain,
! [A_1648] :
( element(A_1648,f(n))
| element(A_1648,n)
| ~ element(A_1648,k) ),
inference(negUnitSimplification,[status(thm)],[c_52652,c_414615]) ).
tff(c_414888,plain,
! [A_1648] :
( element(n,f(n))
| element(A_1648,n)
| ~ element(A_1648,k) ),
inference(resolution,[status(thm)],[c_414619,c_20573]) ).
tff(c_414994,plain,
element(n,f(n)),
inference(splitLeft,[status(thm)],[c_414888]) ).
tff(c_33496,plain,
! [B_392,B_393,A_394] :
( element(B_392,B_393)
| ~ element(A_394,B_393)
| equalish(B_392,m)
| element(B_392,m)
| equalish(A_394,m)
| ~ element(B_392,A_394)
| ~ element(A_394,B_392) ),
inference(resolution,[status(thm)],[c_1656,c_10]) ).
tff(c_33583,plain,
! [B_392] :
( element(B_392,k)
| equalish(B_392,m)
| element(B_392,m)
| equalish(n,m)
| ~ element(B_392,n)
| ~ element(n,B_392) ),
inference(resolution,[status(thm)],[c_116,c_33496]) ).
tff(c_416803,plain,
! [B_392] :
( element(B_392,k)
| equalish(B_392,m)
| element(B_392,m)
| ~ element(B_392,n)
| ~ element(n,B_392) ),
inference(negUnitSimplification,[status(thm)],[c_52652,c_33583]) ).
tff(c_342783,plain,
! [A_1459,B_1460,B_1461] :
( element(g(A_1459),B_1460)
| ~ equalish(B_1461,B_1460)
| ~ equalish(A_1459,B_1461)
| equalish(A_1459,n)
| element(A_1459,n) ),
inference(resolution,[status(thm)],[c_4096,c_8]) ).
tff(c_343203,plain,
! [A_1459] :
( element(g(A_1459),k)
| ~ equalish(A_1459,m)
| equalish(A_1459,n)
| element(A_1459,n) ),
inference(resolution,[status(thm)],[c_52,c_342783]) ).
tff(c_8019,plain,
! [A_169] :
( equalish(m,a)
| ~ element(m,a)
| equalish(A_169,n)
| element(A_169,n)
| equalish(g(A_169),k)
| ~ element(g(A_169),k) ),
inference(resolution,[status(thm)],[c_8010,c_212]) ).
tff(c_8046,plain,
! [A_169] :
( equalish(m,a)
| equalish(A_169,n)
| element(A_169,n)
| equalish(g(A_169),k)
| ~ element(g(A_169),k) ),
inference(demodulation,[status(thm),theory(equality)],[c_234,c_8019]) ).
tff(c_325503,plain,
! [A_1410] :
( equalish(A_1410,n)
| element(A_1410,n)
| equalish(g(A_1410),k)
| ~ element(g(A_1410),k) ),
inference(negUnitSimplification,[status(thm)],[c_48,c_8046]) ).
tff(c_468650,plain,
! [A_1808] :
( element(A_1808,k)
| equalish(A_1808,n)
| element(A_1808,n)
| ~ element(g(A_1808),k) ),
inference(resolution,[status(thm)],[c_325503,c_1178]) ).
tff(c_469062,plain,
! [A_1810] :
( element(A_1810,k)
| ~ equalish(A_1810,m)
| equalish(A_1810,n)
| element(A_1810,n) ),
inference(resolution,[status(thm)],[c_343203,c_468650]) ).
tff(c_469324,plain,
( equalish(n,m)
| ~ element(n,m)
| element(f(n),k)
| ~ equalish(f(n),m)
| element(f(n),n) ),
inference(resolution,[status(thm)],[c_469062,c_18]) ).
tff(c_469607,plain,
( equalish(n,m)
| element(f(n),k)
| ~ equalish(f(n),m)
| element(f(n),n) ),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_469324]) ).
tff(c_469608,plain,
( ~ equalish(f(n),m)
| element(f(n),n) ),
inference(negUnitSimplification,[status(thm)],[c_5438,c_52652,c_469607]) ).
tff(c_469637,plain,
~ equalish(f(n),m),
inference(splitLeft,[status(thm)],[c_469608]) ).
tff(c_469653,plain,
( element(f(n),k)
| element(f(n),m)
| ~ element(f(n),n)
| ~ element(n,f(n)) ),
inference(resolution,[status(thm)],[c_416803,c_469637]) ).
tff(c_469803,plain,
( element(f(n),k)
| element(f(n),m)
| ~ element(f(n),n) ),
inference(demodulation,[status(thm),theory(equality)],[c_414994,c_469653]) ).
tff(c_469804,plain,
~ element(f(n),n),
inference(negUnitSimplification,[status(thm)],[c_453143,c_5438,c_469803]) ).
tff(c_470090,plain,
( ~ equalish(n,n)
| equalish(n,m)
| ~ element(n,m) ),
inference(resolution,[status(thm)],[c_249,c_469804]) ).
tff(c_470102,plain,
equalish(n,m),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_2,c_470090]) ).
tff(c_470104,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_52652,c_470102]) ).
tff(c_470106,plain,
equalish(f(n),m),
inference(splitRight,[status(thm)],[c_469608]) ).
tff(c_470655,plain,
( equalish(n,m)
| ~ element(n,m) ),
inference(resolution,[status(thm)],[c_470106,c_16]) ).
tff(c_470847,plain,
equalish(n,m),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_470655]) ).
tff(c_470849,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_52652,c_470847]) ).
tff(c_470851,plain,
element(f(n),m),
inference(splitRight,[status(thm)],[c_431688]) ).
tff(c_471061,plain,
! [B_1812] :
( element(f(n),B_1812)
| ~ equalish(m,B_1812) ),
inference(resolution,[status(thm)],[c_470851,c_8]) ).
tff(c_471211,plain,
~ equalish(m,k),
inference(resolution,[status(thm)],[c_471061,c_5438]) ).
tff(c_471340,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_52,c_471211]) ).
tff(c_471342,plain,
~ element(n,f(n)),
inference(splitRight,[status(thm)],[c_414888]) ).
tff(c_471351,plain,
( equalish(n,k)
| ~ element(n,k)
| equalish(n,m)
| ~ element(n,m) ),
inference(resolution,[status(thm)],[c_6351,c_471342]) ).
tff(c_471364,plain,
( equalish(n,k)
| equalish(n,m) ),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_116,c_471351]) ).
tff(c_471366,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_52652,c_46,c_471364]) ).
tff(c_471367,plain,
( equalish(f(n),k)
| equalish(n,m) ),
inference(splitRight,[status(thm)],[c_2630]) ).
tff(c_471386,plain,
equalish(n,m),
inference(splitLeft,[status(thm)],[c_471367]) ).
tff(c_471388,plain,
( equalish(n,k)
| equalish(m,a)
| ~ element(m,a) ),
inference(resolution,[status(thm)],[c_471386,c_212]) ).
tff(c_471411,plain,
( equalish(n,k)
| equalish(m,a) ),
inference(demodulation,[status(thm),theory(equality)],[c_234,c_471388]) ).
tff(c_471413,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_48,c_46,c_471411]) ).
tff(c_471415,plain,
~ equalish(n,m),
inference(splitRight,[status(thm)],[c_471367]) ).
tff(c_471414,plain,
equalish(f(n),k),
inference(splitRight,[status(thm)],[c_471367]) ).
tff(c_296,plain,
! [A_55] :
( equalish(A_55,m)
| ~ element(A_55,m)
| ~ equalish(f(A_55),k) ),
inference(resolution,[status(thm)],[c_73,c_292]) ).
tff(c_471495,plain,
( equalish(n,m)
| ~ element(n,m) ),
inference(resolution,[status(thm)],[c_471414,c_296]) ).
tff(c_471522,plain,
equalish(n,m),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_471495]) ).
tff(c_471524,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_471415,c_471522]) ).
tff(c_471525,plain,
element(m,k),
inference(splitRight,[status(thm)],[c_485]) ).
tff(c_471531,plain,
element(k,k),
inference(resolution,[status(thm)],[c_471525,c_129]) ).
tff(c_471536,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_486,c_471531]) ).
tff(c_471537,plain,
element(m,m),
inference(splitRight,[status(thm)],[c_483]) ).
tff(c_471545,plain,
element(k,m),
inference(resolution,[status(thm)],[c_471537,c_129]) ).
tff(c_471557,plain,
element(m,k),
inference(demodulation,[status(thm),theory(equality)],[c_471545,c_485]) ).
tff(c_474364,plain,
! [A_1850] :
( equalish(m,a)
| ~ element(m,a)
| equalish(n,A_1850)
| equalish(A_1850,k)
| ~ element(A_1850,k) ),
inference(resolution,[status(thm)],[c_474322,c_212]) ).
tff(c_474445,plain,
! [A_1850] :
( equalish(m,a)
| equalish(n,A_1850)
| equalish(A_1850,k)
| ~ element(A_1850,k) ),
inference(demodulation,[status(thm),theory(equality)],[c_234,c_474364]) ).
tff(c_474464,plain,
! [A_1851] :
( equalish(n,A_1851)
| equalish(A_1851,k)
| ~ element(A_1851,k) ),
inference(negUnitSimplification,[status(thm)],[c_48,c_474445]) ).
tff(c_474725,plain,
! [A_1853] :
( equalish(k,A_1853)
| equalish(n,A_1853)
| ~ element(A_1853,k) ),
inference(resolution,[status(thm)],[c_474464,c_4]) ).
tff(c_475010,plain,
! [A_1856] :
( equalish(A_1856,n)
| equalish(k,A_1856)
| ~ element(A_1856,k) ),
inference(resolution,[status(thm)],[c_474725,c_4]) ).
tff(c_475843,plain,
! [A_1866] :
( element(n,A_1866)
| equalish(A_1866,n)
| ~ element(A_1866,k) ),
inference(resolution,[status(thm)],[c_475010,c_142]) ).
tff(c_476438,plain,
! [A_1873] :
( equalish(n,A_1873)
| element(n,A_1873)
| ~ element(A_1873,k) ),
inference(resolution,[status(thm)],[c_475843,c_4]) ).
tff(c_476486,plain,
! [A_1873] :
( equalish(n,m)
| ~ equalish(A_1873,k)
| element(n,A_1873)
| ~ element(A_1873,k) ),
inference(resolution,[status(thm)],[c_476438,c_97]) ).
tff(c_508069,plain,
equalish(n,m),
inference(splitLeft,[status(thm)],[c_476486]) ).
tff(c_474603,plain,
! [A_1851] :
( equalish(k,A_1851)
| equalish(n,A_1851)
| ~ element(A_1851,k) ),
inference(resolution,[status(thm)],[c_474464,c_4]) ).
tff(c_478778,plain,
! [X_1902,A_1903] :
( equalish(X_1902,a)
| ~ equalish(X_1902,A_1903)
| equalish(k,A_1903)
| ~ element(A_1903,a) ),
inference(resolution,[status(thm)],[c_297,c_6]) ).
tff(c_478830,plain,
! [A_1851] :
( equalish(n,a)
| ~ element(A_1851,a)
| equalish(k,A_1851)
| ~ element(A_1851,k) ),
inference(resolution,[status(thm)],[c_474603,c_478778]) ).
tff(c_479000,plain,
! [A_1904] :
( ~ element(A_1904,a)
| equalish(k,A_1904)
| ~ element(A_1904,k) ),
inference(negUnitSimplification,[status(thm)],[c_42,c_478830]) ).
tff(c_479571,plain,
! [A_1908] :
( equalish(A_1908,k)
| ~ element(A_1908,a)
| ~ element(A_1908,k) ),
inference(resolution,[status(thm)],[c_479000,c_4]) ).
tff(c_479722,plain,
! [X_4,A_1908] :
( equalish(X_4,k)
| ~ equalish(X_4,A_1908)
| ~ element(A_1908,a)
| ~ element(A_1908,k) ),
inference(resolution,[status(thm)],[c_479571,c_6]) ).
tff(c_508324,plain,
( equalish(n,k)
| ~ element(m,a)
| ~ element(m,k) ),
inference(resolution,[status(thm)],[c_508069,c_479722]) ).
tff(c_508410,plain,
equalish(n,k),
inference(demodulation,[status(thm),theory(equality)],[c_471557,c_234,c_508324]) ).
tff(c_508412,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_46,c_508410]) ).
tff(c_508414,plain,
~ equalish(n,m),
inference(splitRight,[status(thm)],[c_476486]) ).
tff(c_493188,plain,
! [A_2029,B_2030] :
( element(A_2029,B_2030)
| ~ element(k,B_2030)
| equalish(A_2029,n)
| ~ element(A_2029,k) ),
inference(resolution,[status(thm)],[c_475010,c_10]) ).
tff(c_493409,plain,
! [A_2032] :
( element(A_2032,a)
| equalish(A_2032,n)
| ~ element(A_2032,k) ),
inference(resolution,[status(thm)],[c_231,c_493188]) ).
tff(c_494118,plain,
! [A_2037] :
( equalish(n,A_2037)
| element(A_2037,a)
| ~ element(A_2037,k) ),
inference(resolution,[status(thm)],[c_493409,c_4]) ).
tff(c_512663,plain,
! [A_2180,B_2181] :
( element(A_2180,B_2181)
| ~ element(n,B_2181)
| element(A_2180,a)
| ~ element(A_2180,k) ),
inference(resolution,[status(thm)],[c_494118,c_10]) ).
tff(c_512678,plain,
! [A_2180] :
( element(A_2180,f(n))
| element(A_2180,a)
| ~ element(A_2180,k)
| equalish(n,m)
| ~ element(n,m) ),
inference(resolution,[status(thm)],[c_20,c_512663]) ).
tff(c_512694,plain,
! [A_2180] :
( element(A_2180,f(n))
| element(A_2180,a)
| ~ element(A_2180,k)
| equalish(n,m) ),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_512678]) ).
tff(c_512695,plain,
! [A_2180] :
( element(A_2180,f(n))
| element(A_2180,a)
| ~ element(A_2180,k) ),
inference(negUnitSimplification,[status(thm)],[c_508414,c_512694]) ).
tff(c_474604,plain,
! [A_1852] :
( equalish(A_1852,n)
| equalish(A_1852,k)
| ~ element(A_1852,k) ),
inference(resolution,[status(thm)],[c_474464,c_4]) ).
tff(c_474622,plain,
( equalish(n,m)
| ~ element(n,m)
| equalish(f(n),k)
| ~ element(f(n),k) ),
inference(resolution,[status(thm)],[c_474604,c_18]) ).
tff(c_474689,plain,
( equalish(n,m)
| equalish(f(n),k)
| ~ element(f(n),k) ),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_474622]) ).
tff(c_477675,plain,
~ element(f(n),k),
inference(splitLeft,[status(thm)],[c_474689]) ).
tff(c_471546,plain,
! [A_1813] :
( equalish(A_1813,n)
| element(A_1813,n)
| element(g(A_1813),A_1813) ),
inference(cnfTransformation,[status(thm)],[f_140]) ).
tff(c_471549,plain,
! [A_1813,B_8] :
( element(g(A_1813),B_8)
| ~ equalish(A_1813,B_8)
| equalish(A_1813,n)
| element(A_1813,n) ),
inference(resolution,[status(thm)],[c_471546,c_8]) ).
tff(c_482238,plain,
! [A_1933] :
( equalish(A_1933,n)
| element(A_1933,n)
| equalish(g(A_1933),k)
| equalish(g(A_1933),m)
| ~ element(g(A_1933),k) ),
inference(resolution,[status(thm)],[c_472681,c_26]) ).
tff(c_482249,plain,
! [A_1933] :
( equalish(m,a)
| ~ element(m,a)
| equalish(A_1933,n)
| element(A_1933,n)
| equalish(g(A_1933),k)
| ~ element(g(A_1933),k) ),
inference(resolution,[status(thm)],[c_482238,c_212]) ).
tff(c_482280,plain,
! [A_1933] :
( equalish(m,a)
| equalish(A_1933,n)
| element(A_1933,n)
| equalish(g(A_1933),k)
| ~ element(g(A_1933),k) ),
inference(demodulation,[status(thm),theory(equality)],[c_234,c_482249]) ).
tff(c_516291,plain,
! [A_2196] :
( equalish(A_2196,n)
| element(A_2196,n)
| equalish(g(A_2196),k)
| ~ element(g(A_2196),k) ),
inference(negUnitSimplification,[status(thm)],[c_48,c_482280]) ).
tff(c_472289,plain,
! [A_1827] :
( equalish(A_1827,n)
| element(A_1827,n)
| element(A_1827,g(A_1827)) ),
inference(cnfTransformation,[status(thm)],[f_134]) ).
tff(c_472299,plain,
! [A_1827,B_8] :
( element(A_1827,B_8)
| ~ equalish(g(A_1827),B_8)
| equalish(A_1827,n)
| element(A_1827,n) ),
inference(resolution,[status(thm)],[c_472289,c_8]) ).
tff(c_523522,plain,
! [A_2265] :
( element(A_2265,k)
| equalish(A_2265,n)
| element(A_2265,n)
| ~ element(g(A_2265),k) ),
inference(resolution,[status(thm)],[c_516291,c_472299]) ).
tff(c_523534,plain,
! [A_2266] :
( element(A_2266,k)
| ~ equalish(A_2266,k)
| equalish(A_2266,n)
| element(A_2266,n) ),
inference(resolution,[status(thm)],[c_471549,c_523522]) ).
tff(c_523650,plain,
( equalish(n,m)
| ~ element(n,m)
| element(f(n),k)
| ~ equalish(f(n),k)
| element(f(n),n) ),
inference(resolution,[status(thm)],[c_523534,c_18]) ).
tff(c_523804,plain,
( equalish(n,m)
| element(f(n),k)
| ~ equalish(f(n),k)
| element(f(n),n) ),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_523650]) ).
tff(c_523805,plain,
( ~ equalish(f(n),k)
| element(f(n),n) ),
inference(negUnitSimplification,[status(thm)],[c_477675,c_508414,c_523804]) ).
tff(c_524158,plain,
~ equalish(f(n),k),
inference(splitLeft,[status(thm)],[c_523805]) ).
tff(c_472297,plain,
( element(k,g(m))
| equalish(m,n)
| element(m,n) ),
inference(resolution,[status(thm)],[c_472289,c_129]) ).
tff(c_472302,plain,
( element(k,g(m))
| element(m,n) ),
inference(negUnitSimplification,[status(thm)],[c_44,c_472297]) ).
tff(c_472303,plain,
element(m,n),
inference(splitLeft,[status(thm)],[c_472302]) ).
tff(c_477835,plain,
! [A_1894,B_1895] :
( equalish(n,A_1894)
| equalish(B_1895,n)
| ~ element(B_1895,n)
| equalish(A_1894,B_1895)
| ~ element(B_1895,A_1894)
| ~ element(A_1894,B_1895) ),
inference(resolution,[status(thm)],[c_473483,c_4]) ).
tff(c_478042,plain,
! [A_1894] :
( equalish(A_1894,k)
| equalish(n,A_1894)
| equalish(m,n)
| ~ element(m,n)
| ~ element(m,A_1894)
| ~ element(A_1894,m) ),
inference(resolution,[status(thm)],[c_477835,c_75]) ).
tff(c_478152,plain,
! [A_1894] :
( equalish(A_1894,k)
| equalish(n,A_1894)
| equalish(m,n)
| ~ element(m,A_1894)
| ~ element(A_1894,m) ),
inference(demodulation,[status(thm),theory(equality)],[c_472303,c_478042]) ).
tff(c_480455,plain,
! [A_1915] :
( equalish(A_1915,k)
| equalish(n,A_1915)
| ~ element(m,A_1915)
| ~ element(A_1915,m) ),
inference(negUnitSimplification,[status(thm)],[c_44,c_478152]) ).
tff(c_482497,plain,
! [A_1936] :
( equalish(A_1936,n)
| equalish(A_1936,k)
| ~ element(m,A_1936)
| ~ element(A_1936,m) ),
inference(resolution,[status(thm)],[c_480455,c_4]) ).
tff(c_482649,plain,
! [A_1936] :
( element(A_1936,k)
| equalish(A_1936,k)
| ~ element(m,A_1936)
| ~ element(A_1936,m) ),
inference(resolution,[status(thm)],[c_482497,c_38]) ).
tff(c_524178,plain,
( element(f(n),k)
| ~ element(m,f(n))
| ~ element(f(n),m) ),
inference(resolution,[status(thm)],[c_482649,c_524158]) ).
tff(c_524223,plain,
( ~ element(m,f(n))
| ~ element(f(n),m) ),
inference(negUnitSimplification,[status(thm)],[c_477675,c_524178]) ).
tff(c_524235,plain,
~ element(f(n),m),
inference(splitLeft,[status(thm)],[c_524223]) ).
tff(c_512698,plain,
! [A_2182] :
( element(A_2182,f(n))
| element(A_2182,a)
| ~ element(A_2182,k) ),
inference(negUnitSimplification,[status(thm)],[c_508414,c_512694]) ).
tff(c_493586,plain,
! [B_11,A_2032] :
( element(n,B_11)
| ~ element(A_2032,B_11)
| element(A_2032,a)
| ~ element(A_2032,k) ),
inference(resolution,[status(thm)],[c_493409,c_10]) ).
tff(c_512837,plain,
! [A_2182] :
( element(n,f(n))
| element(A_2182,a)
| ~ element(A_2182,k) ),
inference(resolution,[status(thm)],[c_512698,c_493586]) ).
tff(c_512915,plain,
element(n,f(n)),
inference(splitLeft,[status(thm)],[c_512837]) ).
tff(c_473081,plain,
! [B_1836,A_1837] :
( equalish(B_1836,m)
| element(B_1836,m)
| equalish(A_1837,m)
| equalish(A_1837,B_1836)
| ~ element(B_1836,A_1837)
| ~ element(A_1837,B_1836) ),
inference(cnfTransformation,[status(thm)],[f_114]) ).
tff(c_505806,plain,
! [B_2126,B_2127,A_2128] :
( element(B_2126,B_2127)
| ~ element(A_2128,B_2127)
| equalish(B_2126,m)
| element(B_2126,m)
| equalish(A_2128,m)
| ~ element(B_2126,A_2128)
| ~ element(A_2128,B_2126) ),
inference(resolution,[status(thm)],[c_473081,c_10]) ).
tff(c_505884,plain,
! [B_2126] :
( element(B_2126,k)
| equalish(B_2126,m)
| element(B_2126,m)
| equalish(n,m)
| ~ element(B_2126,n)
| ~ element(n,B_2126) ),
inference(resolution,[status(thm)],[c_116,c_505806]) ).
tff(c_542360,plain,
! [B_2348] :
( element(B_2348,k)
| equalish(B_2348,m)
| element(B_2348,m)
| ~ element(B_2348,n)
| ~ element(n,B_2348) ),
inference(negUnitSimplification,[status(thm)],[c_508414,c_505884]) ).
tff(c_476537,plain,
! [A_1876,B_1877] :
( element(g(A_1876),B_1877)
| ~ equalish(A_1876,B_1877)
| equalish(A_1876,n)
| element(A_1876,n) ),
inference(resolution,[status(thm)],[c_471546,c_8]) ).
tff(c_526184,plain,
! [A_2277,B_2278,B_2279] :
( element(g(A_2277),B_2278)
| ~ equalish(B_2279,B_2278)
| ~ equalish(A_2277,B_2279)
| equalish(A_2277,n)
| element(A_2277,n) ),
inference(resolution,[status(thm)],[c_476537,c_8]) ).
tff(c_526678,plain,
! [A_2281] :
( element(g(A_2281),k)
| ~ equalish(A_2281,m)
| equalish(A_2281,n)
| element(A_2281,n) ),
inference(resolution,[status(thm)],[c_52,c_526184]) ).
tff(c_516475,plain,
! [A_2196] :
( element(A_2196,k)
| equalish(A_2196,n)
| element(A_2196,n)
| ~ element(g(A_2196),k) ),
inference(resolution,[status(thm)],[c_516291,c_472299]) ).
tff(c_526855,plain,
! [A_2282] :
( element(A_2282,k)
| ~ equalish(A_2282,m)
| equalish(A_2282,n)
| element(A_2282,n) ),
inference(resolution,[status(thm)],[c_526678,c_516475]) ).
tff(c_526973,plain,
( equalish(n,m)
| ~ element(n,m)
| element(f(n),k)
| ~ equalish(f(n),m)
| element(f(n),n) ),
inference(resolution,[status(thm)],[c_526855,c_18]) ).
tff(c_527128,plain,
( equalish(n,m)
| element(f(n),k)
| ~ equalish(f(n),m)
| element(f(n),n) ),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_526973]) ).
tff(c_527129,plain,
( ~ equalish(f(n),m)
| element(f(n),n) ),
inference(negUnitSimplification,[status(thm)],[c_477675,c_508414,c_527128]) ).
tff(c_527484,plain,
~ equalish(f(n),m),
inference(splitLeft,[status(thm)],[c_527129]) ).
tff(c_542390,plain,
( element(f(n),k)
| element(f(n),m)
| ~ element(f(n),n)
| ~ element(n,f(n)) ),
inference(resolution,[status(thm)],[c_542360,c_527484]) ).
tff(c_542595,plain,
( element(f(n),k)
| element(f(n),m)
| ~ element(f(n),n) ),
inference(demodulation,[status(thm),theory(equality)],[c_512915,c_542390]) ).
tff(c_542596,plain,
~ element(f(n),n),
inference(negUnitSimplification,[status(thm)],[c_524235,c_477675,c_542595]) ).
tff(c_542771,plain,
( ~ equalish(n,n)
| equalish(n,m)
| ~ element(n,m) ),
inference(resolution,[status(thm)],[c_249,c_542596]) ).
tff(c_542779,plain,
equalish(n,m),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_2,c_542771]) ).
tff(c_542781,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_508414,c_542779]) ).
tff(c_542783,plain,
equalish(f(n),m),
inference(splitRight,[status(thm)],[c_527129]) ).
tff(c_474446,plain,
! [A_1850] :
( equalish(n,A_1850)
| equalish(A_1850,k)
| ~ element(A_1850,k) ),
inference(negUnitSimplification,[status(thm)],[c_48,c_474445]) ).
tff(c_471719,plain,
! [A_1819] :
( equalish(A_1819,k)
| equalish(a,A_1819)
| ~ element(A_1819,a) ),
inference(resolution,[status(thm)],[c_369,c_4]) ).
tff(c_472467,plain,
! [A_1831] :
( equalish(m,A_1831)
| equalish(a,A_1831)
| ~ element(A_1831,a) ),
inference(resolution,[status(thm)],[c_471719,c_98]) ).
tff(c_141,plain,
! [B_46,B_41] :
( element(m,B_46)
| ~ equalish(B_41,B_46)
| ~ element(k,B_41) ),
inference(resolution,[status(thm)],[c_127,c_136]) ).
tff(c_472476,plain,
! [A_1831] :
( element(m,A_1831)
| ~ element(k,m)
| equalish(a,A_1831)
| ~ element(A_1831,a) ),
inference(resolution,[status(thm)],[c_472467,c_141]) ).
tff(c_474013,plain,
! [A_1844] :
( element(m,A_1844)
| equalish(a,A_1844)
| ~ element(A_1844,a) ),
inference(demodulation,[status(thm),theory(equality)],[c_471545,c_472476]) ).
tff(c_474016,plain,
! [A_1844] :
( ~ element(k,a)
| element(m,A_1844)
| ~ element(A_1844,a) ),
inference(resolution,[status(thm)],[c_474013,c_141]) ).
tff(c_474075,plain,
! [A_1845] :
( element(m,A_1845)
| ~ element(A_1845,a) ),
inference(demodulation,[status(thm),theory(equality)],[c_231,c_474016]) ).
tff(c_474089,plain,
( element(m,g(a))
| equalish(a,n)
| element(a,n) ),
inference(resolution,[status(thm)],[c_32,c_474075]) ).
tff(c_476745,plain,
element(a,n),
inference(splitLeft,[status(thm)],[c_474089]) ).
tff(c_476757,plain,
! [B_1880] :
( element(a,B_1880)
| ~ equalish(n,B_1880) ),
inference(resolution,[status(thm)],[c_476745,c_8]) ).
tff(c_477362,plain,
! [A_1886] :
( element(a,A_1886)
| equalish(A_1886,k)
| ~ element(A_1886,k) ),
inference(resolution,[status(thm)],[c_474446,c_476757]) ).
tff(c_477514,plain,
! [X_4,A_1886] :
( equalish(X_4,k)
| ~ equalish(X_4,A_1886)
| element(a,A_1886)
| ~ element(A_1886,k) ),
inference(resolution,[status(thm)],[c_477362,c_6]) ).
tff(c_542919,plain,
( equalish(f(n),k)
| element(a,m)
| ~ element(m,k) ),
inference(resolution,[status(thm)],[c_542783,c_477514]) ).
tff(c_543018,plain,
( equalish(f(n),k)
| element(a,m) ),
inference(demodulation,[status(thm),theory(equality)],[c_471557,c_542919]) ).
tff(c_543020,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_476744,c_524158,c_543018]) ).
tff(c_543022,plain,
element(f(n),m),
inference(splitRight,[status(thm)],[c_524223]) ).
tff(c_543437,plain,
! [B_2350] :
( element(f(n),B_2350)
| ~ equalish(m,B_2350) ),
inference(resolution,[status(thm)],[c_543022,c_8]) ).
tff(c_543562,plain,
~ equalish(m,k),
inference(resolution,[status(thm)],[c_543437,c_477675]) ).
tff(c_543676,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_52,c_543562]) ).
tff(c_543678,plain,
equalish(f(n),k),
inference(splitRight,[status(thm)],[c_523805]) ).
tff(c_544218,plain,
( equalish(n,m)
| ~ element(n,m) ),
inference(resolution,[status(thm)],[c_543678,c_296]) ).
tff(c_544350,plain,
equalish(n,m),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_544218]) ).
tff(c_544352,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_508414,c_544350]) ).
tff(c_544354,plain,
~ element(n,f(n)),
inference(splitRight,[status(thm)],[c_512837]) ).
tff(c_544357,plain,
( element(n,a)
| ~ element(n,k) ),
inference(resolution,[status(thm)],[c_512695,c_544354]) ).
tff(c_544363,plain,
element(n,a),
inference(demodulation,[status(thm),theory(equality)],[c_116,c_544357]) ).
tff(c_544365,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_216,c_544363]) ).
tff(c_544366,plain,
( equalish(f(n),k)
| equalish(n,m) ),
inference(splitRight,[status(thm)],[c_474689]) ).
tff(c_544812,plain,
equalish(n,m),
inference(splitLeft,[status(thm)],[c_544366]) ).
tff(c_476756,plain,
! [B_8] :
( element(a,B_8)
| ~ equalish(n,B_8) ),
inference(resolution,[status(thm)],[c_476745,c_8]) ).
tff(c_544817,plain,
element(a,m),
inference(resolution,[status(thm)],[c_544812,c_476756]) ).
tff(c_544846,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_476744,c_544817]) ).
tff(c_544848,plain,
~ equalish(n,m),
inference(splitRight,[status(thm)],[c_544366]) ).
tff(c_544847,plain,
equalish(f(n),k),
inference(splitRight,[status(thm)],[c_544366]) ).
tff(c_545092,plain,
( equalish(n,m)
| ~ element(n,m) ),
inference(resolution,[status(thm)],[c_544847,c_296]) ).
tff(c_545121,plain,
equalish(n,m),
inference(demodulation,[status(thm),theory(equality)],[c_157,c_545092]) ).
tff(c_545123,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_544848,c_545121]) ).
tff(c_545125,plain,
~ element(a,n),
inference(splitRight,[status(thm)],[c_474089]) ).
tff(c_472315,plain,
element(k,n),
inference(resolution,[status(thm)],[c_472303,c_129]) ).
tff(c_545713,plain,
! [A_2362,B_2363] :
( element(A_2362,B_2363)
| ~ element(k,B_2363)
| equalish(A_2362,a)
| ~ element(A_2362,a) ),
inference(resolution,[status(thm)],[c_297,c_10]) ).
tff(c_545740,plain,
! [A_2364] :
( element(A_2364,n)
| equalish(A_2364,a)
| ~ element(A_2364,a) ),
inference(resolution,[status(thm)],[c_472315,c_545713]) ).
tff(c_28,plain,
! [A_22] :
( equalish(A_22,n)
| element(A_22,n)
| ~ equalish(g(A_22),A_22) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_545772,plain,
( equalish(a,n)
| element(a,n)
| element(g(a),n)
| ~ element(g(a),a) ),
inference(resolution,[status(thm)],[c_545740,c_28]) ).
tff(c_545845,plain,
( equalish(a,n)
| element(g(a),n)
| ~ element(g(a),a) ),
inference(negUnitSimplification,[status(thm)],[c_545125,c_545772]) ).
tff(c_546818,plain,
~ element(g(a),a),
inference(splitLeft,[status(thm)],[c_545845]) ).
tff(c_546821,plain,
( ~ equalish(a,a)
| equalish(a,n)
| element(a,n) ),
inference(resolution,[status(thm)],[c_471549,c_546818]) ).
tff(c_546827,plain,
( equalish(a,n)
| element(a,n) ),
inference(demodulation,[status(thm),theory(equality)],[c_2,c_546821]) ).
tff(c_546828,plain,
equalish(a,n),
inference(negUnitSimplification,[status(thm)],[c_545125,c_546827]) ).
tff(c_546851,plain,
( equalish(a,k)
| element(a,k) ),
inference(resolution,[status(thm)],[c_546828,c_38]) ).
tff(c_546874,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_474463,c_286,c_546851]) ).
tff(c_546875,plain,
( element(g(a),n)
| equalish(a,n) ),
inference(splitRight,[status(thm)],[c_545845]) ).
tff(c_546907,plain,
equalish(a,n),
inference(splitLeft,[status(thm)],[c_546875]) ).
tff(c_547385,plain,
( equalish(a,k)
| element(a,k) ),
inference(resolution,[status(thm)],[c_546907,c_38]) ).
tff(c_547408,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_474463,c_286,c_547385]) ).
tff(c_547410,plain,
~ equalish(a,n),
inference(splitRight,[status(thm)],[c_546875]) ).
tff(c_546876,plain,
element(g(a),a),
inference(splitRight,[status(thm)],[c_545845]) ).
tff(c_547409,plain,
element(g(a),n),
inference(splitRight,[status(thm)],[c_546875]) ).
tff(c_547461,plain,
( element(a,n)
| equalish(k,g(a))
| ~ element(g(a),a) ),
inference(resolution,[status(thm)],[c_547409,c_362]) ).
tff(c_547472,plain,
( element(a,n)
| equalish(k,g(a)) ),
inference(demodulation,[status(thm),theory(equality)],[c_546876,c_547461]) ).
tff(c_547473,plain,
equalish(k,g(a)),
inference(negUnitSimplification,[status(thm)],[c_545125,c_547472]) ).
tff(c_547563,plain,
equalish(g(a),k),
inference(resolution,[status(thm)],[c_547473,c_4]) ).
tff(c_547595,plain,
( element(a,k)
| equalish(a,n)
| element(a,n) ),
inference(resolution,[status(thm)],[c_547563,c_472299]) ).
tff(c_547624,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_545125,c_547410,c_474463,c_547595]) ).
tff(c_547626,plain,
element(a,m),
inference(splitRight,[status(thm)],[c_476743]) ).
tff(c_547722,plain,
! [B_2380] :
( element(a,B_2380)
| ~ equalish(m,B_2380) ),
inference(resolution,[status(thm)],[c_547626,c_8]) ).
tff(c_547812,plain,
( element(a,k)
| equalish(m,a)
| ~ element(m,a) ),
inference(resolution,[status(thm)],[c_12,c_547722]) ).
tff(c_547886,plain,
( element(a,k)
| equalish(m,a) ),
inference(demodulation,[status(thm),theory(equality)],[c_234,c_547812]) ).
tff(c_547888,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_48,c_474463,c_547886]) ).
tff(c_547889,plain,
equalish(a,m),
inference(splitRight,[status(thm)],[c_474439]) ).
tff(c_547892,plain,
( equalish(a,k)
| equalish(m,a)
| ~ element(m,a) ),
inference(resolution,[status(thm)],[c_547889,c_212]) ).
tff(c_547915,plain,
( equalish(a,k)
| equalish(m,a) ),
inference(demodulation,[status(thm),theory(equality)],[c_234,c_547892]) ).
tff(c_547917,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_48,c_286,c_547915]) ).
tff(c_547919,plain,
~ element(m,n),
inference(splitRight,[status(thm)],[c_472302]) ).
tff(c_551137,plain,
! [A_2414,B_2415] :
( element(g(A_2414),B_2415)
| ~ equalish(A_2414,B_2415)
| equalish(A_2414,n)
| element(A_2414,n) ),
inference(resolution,[status(thm)],[c_471546,c_8]) ).
tff(c_547920,plain,
! [A_2381] :
( equalish(A_2381,n)
| element(A_2381,n)
| ~ equalish(g(A_2381),A_2381) ),
inference(cnfTransformation,[status(thm)],[f_128]) ).
tff(c_547948,plain,
( equalish(m,n)
| element(m,n)
| ~ equalish(g(m),k) ),
inference(resolution,[status(thm)],[c_73,c_547920]) ).
tff(c_547957,plain,
( element(m,n)
| ~ equalish(g(m),k) ),
inference(negUnitSimplification,[status(thm)],[c_44,c_547948]) ).
tff(c_547983,plain,
~ equalish(g(m),k),
inference(negUnitSimplification,[status(thm)],[c_547919,c_547957]) ).
tff(c_547961,plain,
~ element(k,n),
inference(resolution,[status(thm)],[c_127,c_547919]) ).
tff(c_40,plain,
! [A_29] :
( equalish(A_29,k)
| equalish(A_29,m)
| equalish(A_29,n)
| ~ element(A_29,k) ),
inference(cnfTransformation,[status(thm)],[f_178]) ).
tff(c_547918,plain,
element(k,g(m)),
inference(splitRight,[status(thm)],[c_472302]) ).
tff(c_548426,plain,
! [B_2385] :
( element(k,B_2385)
| ~ equalish(g(m),B_2385) ),
inference(resolution,[status(thm)],[c_547918,c_8]) ).
tff(c_548442,plain,
( element(k,n)
| equalish(g(m),k)
| equalish(g(m),m)
| ~ element(g(m),k) ),
inference(resolution,[status(thm)],[c_40,c_548426]) ).
tff(c_548484,plain,
( equalish(g(m),m)
| ~ element(g(m),k) ),
inference(negUnitSimplification,[status(thm)],[c_547983,c_547961,c_548442]) ).
tff(c_548936,plain,
~ element(g(m),k),
inference(splitLeft,[status(thm)],[c_548484]) ).
tff(c_551148,plain,
( ~ equalish(m,k)
| equalish(m,n)
| element(m,n) ),
inference(resolution,[status(thm)],[c_551137,c_548936]) ).
tff(c_551161,plain,
( equalish(m,n)
| element(m,n) ),
inference(demodulation,[status(thm),theory(equality)],[c_52,c_551148]) ).
tff(c_551163,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_547919,c_44,c_551161]) ).
tff(c_551164,plain,
equalish(g(m),m),
inference(splitRight,[status(thm)],[c_548484]) ).
tff(c_551174,plain,
( equalish(m,n)
| element(m,n) ),
inference(resolution,[status(thm)],[c_551164,c_28]) ).
tff(c_551196,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_547919,c_44,c_551174]) ).
tff(c_551198,plain,
equalish(a,k),
inference(splitRight,[status(thm)],[c_265]) ).
tff(c_551218,plain,
equalish(m,a),
inference(resolution,[status(thm)],[c_551198,c_98]) ).
tff(c_551231,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_48,c_551218]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.08/0.12 % Problem : SYN015-2 : TPTP v9.0.0. Released v1.0.0.
% 0.08/0.13 % 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.33 % Computer : n002.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Wed Apr 9 06:52:33 EDT 2025
% 0.13/0.33 % CPUTime :
% 74.50/59.77 % SZS status Unsatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 74.60/59.83
% 74.60/59.83 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------