%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : MSC013-10 : TPTP v9.0.0. Released v7.3.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 : n026.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 07:45:08 PM UTC 2025 % Result : Satisfiable 47.61s 36.09s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.09 % Problem : MSC013-10 : TPTP v9.0.0. Released v7.3.0. % 0.02/0.10 % 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.10/0.30 % Computer : n026.cluster.edu % 0.10/0.30 % Model : x86_64 x86_64 % 0.10/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.30 % Memory : 8042.1875MB % 0.10/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.30 % CPULimit : 300 % 0.10/0.30 % WCLimit : 300 % 0.10/0.30 % DateTime : Tue Apr 8 07:57:53 EDT 2025 % 0.10/0.30 % CPUTime : % 47.61/36.08 % 47.61/36.09 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 47.61/36.09 % 47.61/36.09 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 47.61/36.09 %$ f > sK1_relation_exists_F > ifeq > equalish > #nlpp > true > n1 > n0 > goal % 47.61/36.09 % 47.61/36.09 %Foreground sorts: % 47.61/36.09 % 47.61/36.09 % 47.61/36.09 %Background operators: % 47.61/36.09 % 47.61/36.09 % 47.61/36.09 %Foreground operators: % 47.61/36.09 tff(sK1_relation_exists_F, type, sK1_relation_exists_F: ($i * $i * $i * $i * $i) > $i). % 47.61/36.09 tff(n1, type, n1: $i). % 47.61/36.09 tff(goal, type, goal: $i). % 47.61/36.09 tff(equalish, type, equalish: ($i * $i) > $i). % 47.61/36.09 tff(n0, type, n0: $i). % 47.61/36.09 tff(true, type, true: $i). % 47.61/36.09 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 47.61/36.09 tff(f, type, f: ($i * $i * $i * $i * $i * $i) > $i). % 47.61/36.09 % 47.61/36.09 %Saturated clause set: % 47.61/36.09 tff(c_93493, plain, (![B_4408, A_4409]: (ifeq(equalish(B_4408, B_4408), true, ifeq(equalish(A_4409, A_4409), true, f(A_4409, B_4408, n1, n1, n0, sK1_relation_exists_F(A_4409, B_4408, n1, n1, n0)), true), true)=true))). % 47.61/36.10 tff(c_77990, plain, (![B_3352, A_3353]: (ifeq(equalish(B_3352, B_3352), true, ifeq(equalish(A_3353, A_3353), true, f(A_3353, B_3352, n0, n1, n0, sK1_relation_exists_F(A_3353, B_3352, n0, n1, n0)), true), true)=true))). % 47.61/36.10 tff(c_81789, plain, (![B_3592, A_3593]: (ifeq(equalish(B_3592, B_3592), true, ifeq(equalish(A_3593, A_3593), true, f(A_3593, B_3592, n0, n0, n0, sK1_relation_exists_F(A_3593, B_3592, n0, n0, n0)), true), true)=true))). % 47.61/36.10 tff(c_82705, plain, (![B_3654, A_3655]: (ifeq(equalish(B_3654, B_3654), true, ifeq(equalish(A_3655, A_3655), true, f(A_3655, B_3654, n1, n1, n1, sK1_relation_exists_F(A_3655, B_3654, n1, n1, n1)), true), true)=true))). % 47.61/36.10 tff(c_77730, plain, (![B_3350, A_3351]: (ifeq(equalish(B_3350, B_3350), true, ifeq(equalish(A_3351, A_3351), true, f(A_3351, B_3350, n0, n1, n1, sK1_relation_exists_F(A_3351, B_3350, n0, n1, n1)), true), true)=true))). % 47.61/36.10 tff(c_88289, plain, (![B_4046, A_4047]: (ifeq(equalish(B_4046, B_4046), true, ifeq(equalish(A_4047, A_4047), true, f(A_4047, B_4046, n0, n0, n1, sK1_relation_exists_F(A_4047, B_4046, n0, n0, n1)), true), true)=true))). % 47.61/36.10 tff(c_78597, plain, (![B_3358, A_3359]: (ifeq(equalish(B_3358, B_3358), true, ifeq(equalish(A_3359, A_3359), true, f(A_3359, B_3358, n1, n0, n0, sK1_relation_exists_F(A_3359, B_3358, n1, n0, n0)), true), true)=true))). % 47.61/36.10 tff(c_78785, plain, (![B_3360, A_3361]: (ifeq(equalish(B_3360, B_3360), true, ifeq(equalish(A_3361, A_3361), true, f(A_3361, B_3360, n1, n0, n1, sK1_relation_exists_F(A_3361, B_3360, n1, n0, n1)), true), true)=true))). % 47.61/36.10 tff(c_94858, plain, (![A_4513, D_4514, B_4512, C_4511, E_4510]: (ifeq(f(A_4513, B_4512, C_4511, D_4514, E_4510, sK1_relation_exists_F(n0, n0, n0, n1, n0)), true, equalish(E_4510, n0), true)=true))). % 47.61/36.10 tff(c_94723, plain, (![C_4501, E_4500, B_4502, A_4503, D_4504]: (ifeq(f(A_4503, B_4502, C_4501, D_4504, E_4500, sK1_relation_exists_F(n0, n0, n0, n1, n1)), true, equalish(E_4500, n1), true)=true))). % 47.71/36.10 tff(c_94575, plain, (![E_4493, A_4491, C_4494, D_4492, B_4490]: (ifeq(f(A_4491, B_4490, C_4494, D_4492, E_4493, sK1_relation_exists_F(n0, n0, n0, n1, n1)), true, equalish(A_4491, n0), true)=true))). % 47.71/36.10 tff(c_94428, plain, (![C_4482, A_4480, B_4481, D_4484, E_4483]: (ifeq(f(A_4480, B_4481, C_4482, D_4484, E_4483, sK1_relation_exists_F(n0, n0, n0, n1, n0)), true, equalish(C_4482, n0), true)=true))). % 47.71/36.10 tff(c_94293, plain, (![B_4471, D_4473, C_4474, A_4472, E_4470]: (ifeq(f(A_4472, B_4471, C_4474, D_4473, E_4470, sK1_relation_exists_F(n0, n0, n0, n1, n1)), true, equalish(B_4471, n0), true)=true))). % 47.71/36.10 tff(c_94157, plain, (![E_4460, C_4464, D_4463, B_4461, A_4462]: (ifeq(f(A_4462, B_4461, C_4464, D_4463, E_4460, sK1_relation_exists_F(n0, n0, n0, n1, n0)), true, equalish(B_4461, n0), true)=true))). % 47.71/36.10 tff(c_94034, plain, (![C_4452, A_4450, B_4451, E_4453, D_4454]: (ifeq(f(A_4450, B_4451, C_4452, D_4454, E_4453, sK1_relation_exists_F(n0, n0, n0, n1, n1)), true, equalish(C_4452, n0), true)=true))). % 47.71/36.10 tff(c_93911, plain, (![E_4443, A_4441, C_4444, D_4442, B_4440]: (ifeq(f(A_4441, B_4440, C_4444, D_4442, E_4443, sK1_relation_exists_F(n0, n0, n0, n1, n0)), true, equalish(A_4441, n0), true)=true))). % 47.71/36.10 tff(c_93787, plain, (![D_4433, A_4430, B_4432, C_4431, E_4434]: (ifeq(f(A_4430, B_4432, C_4431, D_4433, E_4434, sK1_relation_exists_F(n0, n0, n0, n1, n1)), true, equalish(D_4433, n1), true)=true))). % 47.71/36.10 tff(c_93664, plain, (![A_4420, D_4423, B_4422, C_4421, E_4424]: (ifeq(f(A_4420, B_4422, C_4421, D_4423, E_4424, sK1_relation_exists_F(n0, n0, n0, n1, n0)), true, equalish(D_4423, n1), true)=true))). % 47.71/36.10 tff(c_93541, plain, (![C_4411, E_4414, B_4412, D_4413, A_4410]: (ifeq(f(A_4410, B_4412, C_4411, D_4413, E_4414, sK1_relation_exists_F(n1, n1, n1, n0, n1)), true, equalish(D_4413, n0), true)=true))). % 47.71/36.10 tff(c_93277, plain, (![C_4399, A_4401, E_4398, D_4402, B_4400]: (ifeq(f(A_4401, B_4400, C_4399, D_4402, E_4398, sK1_relation_exists_F(n1, n1, n0, n1, n0)), true, equalish(E_4398, n0), true)=true))). % 47.71/36.10 tff(c_93130, plain, (![D_4392, A_4388, E_4391, C_4390, B_4389]: (ifeq(f(A_4388, B_4389, C_4390, D_4392, E_4391, sK1_relation_exists_F(n0, n1, n1, n0, n1)), true, equalish(C_4390, n1), true)=true))). % 47.71/36.10 tff(c_92983, plain, (![B_4378, D_4380, E_4381, C_4382, A_4379]: (ifeq(f(A_4379, B_4378, C_4382, D_4380, E_4381, sK1_relation_exists_F(n1, n1, n0, n1, n0)), true, equalish(A_4379, n1), true)=true))). % 47.71/36.10 tff(c_92835, plain, (![B_4369, C_4372, D_4371, A_4370, E_4368]: (ifeq(f(A_4370, B_4369, C_4372, D_4371, E_4368, sK1_relation_exists_F(n0, n1, n1, n1, n0)), true, equalish(B_4369, n1), true)=true))). % 47.71/36.10 tff(c_92688, plain, (![B_4359, D_4361, E_4358, A_4360, C_4362]: (ifeq(f(A_4360, B_4359, C_4362, D_4361, E_4358, sK1_relation_exists_F(n0, n0, n1, n0, n1)), true, equalish(B_4359, n0), true)=true))). % 47.71/36.10 tff(c_92553, plain, (![E_4351, C_4350, B_4349, D_4352, A_4348]: (ifeq(f(A_4348, B_4349, C_4350, D_4352, E_4351, sK1_relation_exists_F(n0, n0, n1, n0, n1)), true, equalish(C_4350, n1), true)=true))). % 47.71/36.10 tff(c_92393, plain, (![B_4339, A_4340, E_4338, D_4341, C_4342]: (ifeq(f(A_4340, B_4339, C_4342, D_4341, E_4338, sK1_relation_exists_F(n0, n1, n1, n1, n1)), true, equalish(B_4339, n1), true)=true))). % 47.71/36.10 tff(c_92258, plain, (![B_4330, E_4328, A_4331, C_4329, D_4332]: (ifeq(f(A_4331, B_4330, C_4329, D_4332, E_4328, sK1_relation_exists_F(n1, n1, n1, n0, n0)), true, equalish(E_4328, n0), true)=true))). % 47.71/36.10 tff(c_92111, plain, (![E_4321, D_4322, A_4318, C_4320, B_4319]: (ifeq(f(A_4318, B_4319, C_4320, D_4322, E_4321, sK1_relation_exists_F(n0, n1, n1, n1, n1)), true, equalish(C_4320, n1), true)=true))). % 47.71/36.10 tff(c_91975, plain, (![E_4308, C_4312, B_4309, D_4311, A_4310]: (ifeq(f(A_4310, B_4309, C_4312, D_4311, E_4308, sK1_relation_exists_F(n0, n0, n1, n1, n1)), true, equalish(B_4309, n0), true)=true))). % 47.71/36.10 tff(c_91840, plain, (![D_4302, B_4299, E_4301, C_4300, A_4298]: (ifeq(f(A_4298, B_4299, C_4300, D_4302, E_4301, sK1_relation_exists_F(n0, n1, n1, n0, n0)), true, equalish(C_4300, n1), true)=true))). % 47.71/36.10 tff(c_91705, plain, (![A_4291, B_4290, C_4289, D_4292, E_4288]: (ifeq(f(A_4291, B_4290, C_4289, D_4292, E_4288, sK1_relation_exists_F(n0, n1, n1, n0, n1)), true, equalish(E_4288, n1), true)=true))). % 47.71/36.10 tff(c_91569, plain, (![A_4279, D_4280, E_4281, B_4278, C_4282]: (ifeq(f(A_4279, B_4278, C_4282, D_4280, E_4281, sK1_relation_exists_F(n0, n1, n1, n0, n1)), true, equalish(A_4279, n0), true)=true))). % 47.71/36.10 tff(c_91422, plain, (![E_4268, C_4269, D_4272, A_4271, B_4270]: (ifeq(f(A_4271, B_4270, C_4269, D_4272, E_4268, sK1_relation_exists_F(n0, n0, n1, n1, n1)), true, equalish(E_4268, n1), true)=true))). % 47.71/36.10 tff(c_91299, plain, (![E_4258, A_4261, C_4259, B_4260, D_4262]: (ifeq(f(A_4261, B_4260, C_4259, D_4262, E_4258, sK1_relation_exists_F(n1, n1, n1, n1, n0)), true, equalish(E_4258, n0), true)=true))). % 47.71/36.10 tff(c_91127, plain, (![B_4249, D_4252, C_4250, A_4248, E_4251]: (ifeq(f(A_4248, B_4249, C_4250, D_4252, E_4251, sK1_relation_exists_F(n1, n1, n1, n1, n1)), true, equalish(C_4250, n1), true)=true))). % 47.71/36.10 tff(c_90968, plain, (![B_4239, D_4241, A_4240, E_4238, C_4242]: (ifeq(f(A_4240, B_4239, C_4242, D_4241, E_4238, sK1_relation_exists_F(n0, n0, n1, n0, n0)), true, equalish(B_4239, n0), true)=true))). % 47.71/36.10 tff(c_90845, plain, (![B_4229, D_4231, A_4230, C_4232, E_4228]: (ifeq(f(A_4230, B_4229, C_4232, D_4231, E_4228, sK1_relation_exists_F(n0, n1, n1, n0, n1)), true, equalish(B_4229, n1), true)=true))). % 47.71/36.11 tff(c_90697, plain, (![E_4218, A_4221, C_4219, B_4220, D_4222]: (ifeq(f(A_4221, B_4220, C_4219, D_4222, E_4218, sK1_relation_exists_F(n0, n0, n1, n0, n0)), true, equalish(E_4218, n0), true)=true))). % 47.71/36.11 tff(c_90550, plain, (![E_4211, A_4209, C_4212, B_4208, D_4210]: (ifeq(f(A_4209, B_4208, C_4212, D_4210, E_4211, sK1_relation_exists_F(n1, n1, n1, n0, n0)), true, equalish(A_4209, n1), true)=true))). % 47.71/36.11 tff(c_90415, plain, (![E_4201, B_4199, C_4200, A_4198, D_4202]: (ifeq(f(A_4198, B_4199, C_4200, D_4202, E_4201, sK1_relation_exists_F(n1, n0, n0, n1, n1)), true, equalish(C_4200, n0), true)=true))). % 47.71/36.11 tff(c_90255, plain, (![A_4189, E_4191, B_4188, D_4190, C_4192]: (ifeq(f(A_4189, B_4188, C_4192, D_4190, E_4191, sK1_relation_exists_F(n1, n0, n1, n1, n1)), true, equalish(A_4189, n1), true)=true))). % 47.71/36.11 tff(c_90120, plain, (![E_4178, A_4180, B_4179, C_4182, D_4181]: (ifeq(f(A_4180, B_4179, C_4182, D_4181, E_4178, sK1_relation_exists_F(n1, n1, n1, n0, n0)), true, equalish(B_4179, n1), true)=true))). % 47.71/36.11 tff(c_89961, plain, (![C_4169, D_4171, E_4172, B_4170, A_4168]: (ifeq(f(A_4168, B_4170, C_4169, D_4171, E_4172, sK1_relation_exists_F(n0, n0, n0, n0, n1)), true, equalish(D_4171, n0), true)=true))). % 47.71/36.11 tff(c_89813, plain, (![A_4158, B_4160, C_4159, D_4161, E_4162]: (ifeq(f(A_4158, B_4160, C_4159, D_4161, E_4162, sK1_relation_exists_F(n1, n0, n0, n1, n1)), true, equalish(D_4161, n1), true)=true))). % 47.71/36.11 tff(c_89678, plain, (![B_4150, D_4151, A_4148, E_4152, C_4149]: (ifeq(f(A_4148, B_4150, C_4149, D_4151, E_4152, sK1_relation_exists_F(n1, n1, n0, n1, n0)), true, equalish(D_4151, n1), true)=true))). % 47.71/36.11 tff(c_89543, plain, (![C_4139, A_4141, B_4140, E_4138, D_4142]: (ifeq(f(A_4141, B_4140, C_4139, D_4142, E_4138, sK1_relation_exists_F(n1, n0, n1, n1, n0)), true, equalish(E_4138, n0), true)=true))). % 47.71/36.11 tff(c_89407, plain, (![C_4132, E_4128, B_4129, A_4130, D_4131]: (ifeq(f(A_4130, B_4129, C_4132, D_4131, E_4128, sK1_relation_exists_F(n0, n1, n0, n1, n0)), true, equalish(B_4129, n1), true)=true))). % 47.71/36.11 tff(c_89284, plain, (![A_4118, B_4120, C_4119, D_4121, E_4122]: (ifeq(f(A_4118, B_4120, C_4119, D_4121, E_4122, sK1_relation_exists_F(n0, n1, n1, n0, n1)), true, equalish(D_4121, n0), true)=true))). % 47.71/36.11 tff(c_89161, plain, (![D_4112, E_4108, C_4109, A_4111, B_4110]: (ifeq(f(A_4111, B_4110, C_4109, D_4112, E_4108, sK1_relation_exists_F(n0, n0, n0, n0, n1)), true, equalish(E_4108, n1), true)=true))). % 47.71/36.11 tff(c_89013, plain, (![C_4099, B_4100, D_4102, A_4101, E_4098]: (ifeq(f(A_4101, B_4100, C_4099, D_4102, E_4098, sK1_relation_exists_F(n1, n0, n1, n1, n1)), true, equalish(E_4098, n1), true)=true))). % 47.71/36.11 tff(c_88890, plain, (![A_4090, E_4088, B_4089, C_4092, D_4091]: (ifeq(f(A_4090, B_4089, C_4092, D_4091, E_4088, sK1_relation_exists_F(n1, n0, n0, n1, n1)), true, equalish(B_4089, n0), true)=true))). % 47.71/36.11 tff(c_88743, plain, (![C_4079, E_4078, A_4081, B_4080, D_4082]: (ifeq(f(A_4081, B_4080, C_4079, D_4082, E_4078, sK1_relation_exists_F(n0, n1, n1, n0, n0)), true, equalish(E_4078, n0), true)=true))). % 47.71/36.11 tff(c_88619, plain, (![A_4068, B_4070, E_4072, D_4071, C_4069]: (ifeq(f(A_4068, B_4070, C_4069, D_4071, E_4072, sK1_relation_exists_F(n0, n1, n0, n1, n0)), true, equalish(D_4071, n1), true)=true))). % 47.71/36.11 tff(c_88472, plain, (![C_4062, D_4060, B_4058, A_4059, E_4061]: (ifeq(f(A_4059, B_4058, C_4062, D_4060, E_4061, sK1_relation_exists_F(n0, n0, n0, n0, n1)), true, equalish(A_4059, n0), true)=true))). % 47.71/36.11 tff(c_88337, plain, (![C_4049, D_4051, E_4052, A_4048, B_4050]: (ifeq(f(A_4048, B_4050, C_4049, D_4051, E_4052, sK1_relation_exists_F(n0, n1, n1, n0, n0)), true, equalish(D_4051, n0), true)=true))). % 47.71/36.11 tff(c_88073, plain, (![B_4038, E_4040, A_4036, D_4039, C_4037]: (ifeq(f(A_4036, B_4038, C_4037, D_4039, E_4040, sK1_relation_exists_F(n1, n0, n1, n1, n1)), true, equalish(D_4039, n1), true)=true))). % 47.71/36.11 tff(c_87926, plain, (![C_4027, A_4029, B_4028, D_4030, E_4026]: (ifeq(f(A_4029, B_4028, C_4027, D_4030, E_4026, sK1_relation_exists_F(n0, n1, n0, n1, n1)), true, equalish(E_4026, n1), true)=true))). % 47.71/36.11 tff(c_87791, plain, (![B_4017, C_4018, D_4020, E_4019, A_4016]: (ifeq(f(A_4016, B_4017, C_4018, D_4020, E_4019, sK1_relation_exists_F(n0, n0, n1, n1, n0)), true, equalish(C_4018, n1), true)=true))). % 47.71/36.11 tff(c_87631, plain, (![B_4008, D_4010, E_4006, C_4007, A_4009]: (ifeq(f(A_4009, B_4008, C_4007, D_4010, E_4006, sK1_relation_exists_F(n1, n1, n1, n1, n1)), true, equalish(E_4006, n1), true)=true))). % 47.71/36.11 tff(c_87496, plain, (![B_3996, D_3998, E_3999, C_4000, A_3997]: (ifeq(f(A_3997, B_3996, C_4000, D_3998, E_3999, sK1_relation_exists_F(n0, n0, n1, n0, n0)), true, equalish(A_3997, n0), true)=true))). % 47.71/36.11 tff(c_87361, plain, (![D_3990, E_3989, B_3987, A_3986, C_3988]: (ifeq(f(A_3986, B_3987, C_3988, D_3990, E_3989, sK1_relation_exists_F(n0, n1, n1, n1, n0)), true, equalish(C_3988, n1), true)=true))). % 47.71/36.11 tff(c_87237, plain, (![C_3980, E_3976, D_3979, B_3977, A_3978]: (ifeq(f(A_3978, B_3977, C_3980, D_3979, E_3976, sK1_relation_exists_F(n1, n1, n0, n1, n0)), true, equalish(B_3977, n1), true)=true))). % 47.71/36.11 tff(c_87090, plain, (![C_3967, B_3968, E_3966, A_3969, D_3970]: (ifeq(f(A_3969, B_3968, C_3967, D_3970, E_3966, sK1_relation_exists_F(n0, n1, n0, n1, n0)), true, equalish(E_3966, n0), true)=true))). % 47.71/36.11 tff(c_86943, plain, (![E_3956, C_3957, B_3958, A_3959, D_3960]: (ifeq(f(A_3959, B_3958, C_3957, D_3960, E_3956, sK1_relation_exists_F(n1, n0, n0, n1, n0)), true, equalish(E_3956, n0), true)=true))). % 47.71/36.11 tff(c_86819, plain, (![D_3950, E_3946, C_3947, B_3948, A_3949]: (ifeq(f(A_3949, B_3948, C_3947, D_3950, E_3946, sK1_relation_exists_F(n0, n0, n1, n0, n1)), true, equalish(E_3946, n1), true)=true))). % 47.71/36.11 tff(c_86684, plain, (![E_3940, B_3938, A_3936, D_3939, C_3937]: (ifeq(f(A_3936, B_3938, C_3937, D_3939, E_3940, sK1_relation_exists_F(n0, n0, n1, n1, n1)), true, equalish(D_3939, n1), true)=true))). % 47.71/36.11 tff(c_86549, plain, (![C_3927, E_3926, B_3928, D_3930, A_3929]: (ifeq(f(A_3929, B_3928, C_3927, D_3930, E_3926, sK1_relation_exists_F(n0, n1, n1, n1, n1)), true, equalish(E_3926, n1), true)=true))). % 47.71/36.11 tff(c_86413, plain, (![B_3918, A_3916, C_3917, E_3920, D_3919]: (ifeq(f(A_3916, B_3918, C_3917, D_3919, E_3920, sK1_relation_exists_F(n1, n0, n0, n1, n0)), true, equalish(D_3919, n1), true)=true))). % 47.71/36.11 tff(c_86290, plain, (![C_3908, B_3907, A_3906, D_3910, E_3909]: (ifeq(f(A_3906, B_3907, C_3908, D_3910, E_3909, sK1_relation_exists_F(n0, n0, n1, n0, n0)), true, equalish(C_3908, n1), true)=true))). % 47.71/36.11 tff(c_86167, plain, (![A_3896, E_3900, D_3899, B_3898, C_3897]: (ifeq(f(A_3896, B_3898, C_3897, D_3899, E_3900, sK1_relation_exists_F(n0, n0, n1, n0, n0)), true, equalish(D_3899, n0), true)=true))). % 47.71/36.11 tff(c_86031, plain, (![C_3890, E_3886, A_3888, B_3887, D_3889]: (ifeq(f(A_3888, B_3887, C_3890, D_3889, E_3886, sK1_relation_exists_F(n0, n1, n0, n1, n1)), true, equalish(B_3887, n1), true)=true))). % 47.71/36.11 tff(c_85884, plain, (![C_3880, B_3876, D_3878, A_3877, E_3879]: (ifeq(f(A_3877, B_3876, C_3880, D_3878, E_3879, sK1_relation_exists_F(n1, n1, n1, n1, n1)), true, equalish(A_3877, n1), true)=true))). % 47.71/36.11 tff(c_85749, plain, (![E_3869, A_3867, D_3868, C_3870, B_3866]: (ifeq(f(A_3867, B_3866, C_3870, D_3868, E_3869, sK1_relation_exists_F(n0, n0, n1, n0, n1)), true, equalish(A_3867, n0), true)=true))). % 47.71/36.11 tff(c_85625, plain, (![B_3856, A_3857, E_3859, C_3860, D_3858]: (ifeq(f(A_3857, B_3856, C_3860, D_3858, E_3859, sK1_relation_exists_F(n0, n1, n1, n1, n1)), true, equalish(A_3857, n0), true)=true))). % 47.71/36.11 tff(c_85466, plain, (![E_3849, C_3850, B_3846, D_3848, A_3847]: (ifeq(f(A_3847, B_3846, C_3850, D_3848, E_3849, sK1_relation_exists_F(n1, n1, n0, n1, n1)), true, equalish(A_3847, n1), true)=true))). % 47.71/36.11 tff(c_85331, plain, (![B_3838, C_3837, E_3836, D_3840, A_3839]: (ifeq(f(A_3839, B_3838, C_3837, D_3840, E_3836, sK1_relation_exists_F(n1, n0, n0, n1, n1)), true, equalish(E_3836, n1), true)=true))). % 47.71/36.11 tff(c_85195, plain, (![C_3830, D_3828, E_3829, B_3826, A_3827]: (ifeq(f(A_3827, B_3826, C_3830, D_3828, E_3829, sK1_relation_exists_F(n0, n1, n0, n1, n1)), true, equalish(A_3827, n0), true)=true))). % 47.71/36.11 tff(c_85072, plain, (![D_3820, B_3817, C_3818, A_3816, E_3819]: (ifeq(f(A_3816, B_3817, C_3818, D_3820, E_3819, sK1_relation_exists_F(n0, n1, n0, n1, n1)), true, equalish(C_3818, n0), true)=true))). % 47.71/36.11 tff(c_84901, plain, (![D_3810, E_3806, C_3807, B_3808, A_3809]: (ifeq(f(A_3809, B_3808, C_3807, D_3810, E_3806, sK1_relation_exists_F(n0, n0, n0, n0, n0)), true, equalish(E_3806, n0), true)=true))). % 47.71/36.11 tff(c_84765, plain, (![E_3799, B_3797, C_3798, D_3800, A_3796]: (ifeq(f(A_3796, B_3797, C_3798, D_3800, E_3799, sK1_relation_exists_F(n0, n1, n0, n1, n0)), true, equalish(C_3798, n0), true)=true))). % 47.71/36.11 tff(c_84606, plain, (![E_3789, C_3788, A_3786, D_3790, B_3787]: (ifeq(f(A_3786, B_3787, C_3788, D_3790, E_3789, sK1_relation_exists_F(n1, n1, n1, n1, n0)), true, equalish(C_3788, n1), true)=true))). % 47.71/36.11 tff(c_84459, plain, (![B_3777, D_3779, A_3778, E_3776, C_3780]: (ifeq(f(A_3778, B_3777, C_3780, D_3779, E_3776, sK1_relation_exists_F(n1, n1, n0, n1, n1)), true, equalish(B_3777, n1), true)=true))). % 47.71/36.11 tff(c_84299, plain, (![B_3766, D_3768, A_3767, C_3770, E_3769]: (ifeq(f(A_3767, B_3766, C_3770, D_3768, E_3769, sK1_relation_exists_F(n0, n0, n0, n0, n0)), true, equalish(A_3767, n0), true)=true))). % 47.71/36.11 tff(c_84176, plain, (![B_3758, E_3760, A_3756, C_3757, D_3759]: (ifeq(f(A_3756, B_3758, C_3757, D_3759, E_3760, sK1_relation_exists_F(n0, n1, n1, n1, n0)), true, equalish(D_3759, n1), true)=true))). % 47.71/36.11 tff(c_84017, plain, (![C_3747, A_3749, B_3748, D_3750, E_3746]: (ifeq(f(A_3749, B_3748, C_3747, D_3750, E_3746, sK1_relation_exists_F(n1, n1, n1, n0, n1)), true, equalish(E_3746, n1), true)=true))). % 47.71/36.11 tff(c_83893, plain, (![B_3736, A_3737, E_3739, D_3738, C_3740]: (ifeq(f(A_3737, B_3736, C_3740, D_3738, E_3739, sK1_relation_exists_F(n1, n0, n0, n1, n1)), true, equalish(A_3737, n1), true)=true))). % 47.71/36.11 tff(c_83770, plain, (![A_3727, B_3726, D_3728, C_3730, E_3729]: (ifeq(f(A_3727, B_3726, C_3730, D_3728, E_3729, sK1_relation_exists_F(n1, n0, n0, n1, n0)), true, equalish(A_3727, n1), true)=true))). % 47.71/36.11 tff(c_83647, plain, (![D_3719, E_3720, B_3718, A_3716, C_3717]: (ifeq(f(A_3716, B_3718, C_3717, D_3719, E_3720, sK1_relation_exists_F(n0, n1, n1, n1, n1)), true, equalish(D_3719, n1), true)=true))). % 47.71/36.11 tff(c_83511, plain, (![C_3710, A_3708, D_3709, E_3706, B_3707]: (ifeq(f(A_3708, B_3707, C_3710, D_3709, E_3706, sK1_relation_exists_F(n0, n0, n0, n0, n1)), true, equalish(B_3707, n0), true)=true))). % 47.71/36.11 tff(c_83376, plain, (![A_3698, D_3699, B_3697, E_3696, C_3700]: (ifeq(f(A_3698, B_3697, C_3700, D_3699, E_3696, sK1_relation_exists_F(n1, n1, n1, n1, n1)), true, equalish(B_3697, n1), true)=true))). % 47.71/36.11 tff(c_83229, plain, (![A_3686, C_3688, E_3689, D_3690, B_3687]: (ifeq(f(A_3686, B_3687, C_3688, D_3690, E_3689, sK1_relation_exists_F(n0, n0, n0, n0, n0)), true, equalish(C_3688, n0), true)=true))). % 47.71/36.11 tff(c_83105, plain, (![B_3677, C_3678, A_3676, E_3679, D_3680]: (ifeq(f(A_3676, B_3677, C_3678, D_3680, E_3679, sK1_relation_exists_F(n1, n1, n0, n1, n1)), true, equalish(C_3678, n0), true)=true))). % 47.71/36.11 tff(c_82982, plain, (![B_3668, C_3667, E_3670, A_3666, D_3669]: (ifeq(f(A_3666, B_3668, C_3667, D_3669, E_3670, sK1_relation_exists_F(n0, n1, n0, n1, n1)), true, equalish(D_3669, n1), true)=true))). % 47.71/36.11 tff(c_82835, plain, (![A_3656, B_3658, C_3657, D_3659, E_3660]: (ifeq(f(A_3656, B_3658, C_3657, D_3659, E_3660, sK1_relation_exists_F(n1, n0, n1, n1, n0)), true, equalish(D_3659, n1), true)=true))). % 47.71/36.11 tff(c_82583, plain, (![E_3644, C_3648, B_3645, A_3646, D_3647]: (ifeq(f(A_3646, B_3645, C_3648, D_3647, E_3644, sK1_relation_exists_F(n1, n0, n1, n1, n1)), true, equalish(B_3645, n0), true)=true))). % 47.71/36.11 tff(c_82436, plain, (![D_3637, B_3636, A_3634, E_3638, C_3635]: (ifeq(f(A_3634, B_3636, C_3635, D_3637, E_3638, sK1_relation_exists_F(n1, n1, n1, n1, n0)), true, equalish(D_3637, n1), true)=true))). % 47.71/36.11 tff(c_82301, plain, (![D_3628, E_3627, B_3625, C_3626, A_3624]: (ifeq(f(A_3624, B_3625, C_3626, D_3628, E_3627, sK1_relation_exists_F(n1, n0, n0, n1, n0)), true, equalish(C_3626, n0), true)=true))). % 47.71/36.12 tff(c_82177, plain, (![A_3614, E_3618, C_3615, B_3616, D_3617]: (ifeq(f(A_3614, B_3616, C_3615, D_3617, E_3618, sK1_relation_exists_F(n1, n1, n1, n1, n1)), true, equalish(D_3617, n1), true)=true))). % 47.71/36.12 tff(c_82054, plain, (![E_3607, C_3608, A_3605, B_3604, D_3606]: (ifeq(f(A_3605, B_3604, C_3608, D_3606, E_3607, sK1_relation_exists_F(n0, n1, n1, n0, n0)), true, equalish(A_3605, n0), true)=true))). % 47.71/36.12 tff(c_81919, plain, (![A_3595, B_3594, C_3598, E_3597, D_3596]: (ifeq(f(A_3595, B_3594, C_3598, D_3596, E_3597, sK1_relation_exists_F(n1, n0, n1, n1, n0)), true, equalish(A_3595, n1), true)=true))). % 47.71/36.12 tff(c_81667, plain, (![C_3583, E_3586, B_3584, A_3582, D_3585]: (ifeq(f(A_3582, B_3584, C_3583, D_3585, E_3586, sK1_relation_exists_F(n1, n1, n1, n0, n0)), true, equalish(D_3585, n0), true)=true))). % 47.71/36.12 tff(c_81544, plain, (![C_3576, A_3574, D_3575, B_3573, E_3572]: (ifeq(f(A_3574, B_3573, C_3576, D_3575, E_3572, sK1_relation_exists_F(n0, n1, n1, n0, n0)), true, equalish(B_3573, n1), true)=true))). % 47.71/36.12 tff(c_81409, plain, (![E_3566, D_3565, C_3563, B_3564, A_3562]: (ifeq(f(A_3562, B_3564, C_3563, D_3565, E_3566, sK1_relation_exists_F(n0, n0, n0, n0, n0)), true, equalish(D_3565, n0), true)=true))). % 47.71/36.12 tff(c_81285, plain, (![C_3556, E_3552, D_3555, B_3553, A_3554]: (ifeq(f(A_3554, B_3553, C_3556, D_3555, E_3552, sK1_relation_exists_F(n0, n0, n0, n0, n0)), true, equalish(B_3553, n0), true)=true))). % 47.71/36.12 tff(c_81150, plain, (![D_3546, B_3544, C_3543, E_3542, A_3545]: (ifeq(f(A_3545, B_3544, C_3543, D_3546, E_3542, sK1_relation_exists_F(n1, n1, n0, n1, n1)), true, equalish(E_3542, n1), true)=true))). % 47.71/36.12 tff(c_81027, plain, (![D_3535, C_3533, A_3532, E_3536, B_3534]: (ifeq(f(A_3532, B_3534, C_3533, D_3535, E_3536, sK1_relation_exists_F(n1, n1, n0, n1, n1)), true, equalish(D_3535, n1), true)=true))). % 47.71/36.12 tff(c_80903, plain, (![A_3524, D_3525, B_3523, C_3526, E_3522]: (ifeq(f(A_3524, B_3523, C_3526, D_3525, E_3522, sK1_relation_exists_F(n1, n0, n0, n1, n0)), true, equalish(B_3523, n0), true)=true))). % 47.71/36.12 tff(c_80768, plain, (![A_3513, E_3515, D_3514, B_3512, C_3516]: (ifeq(f(A_3513, B_3512, C_3516, D_3514, E_3515, sK1_relation_exists_F(n1, n1, n1, n1, n0)), true, equalish(A_3513, n1), true)=true))). % 47.71/36.12 tff(c_80645, plain, (![A_3502, E_3506, C_3503, D_3505, B_3504]: (ifeq(f(A_3502, B_3504, C_3503, D_3505, E_3506, sK1_relation_exists_F(n0, n0, n1, n0, n1)), true, equalish(D_3505, n0), true)=true))). % 47.71/36.12 tff(c_80521, plain, (![C_3496, D_3494, E_3495, B_3492, A_3493]: (ifeq(f(A_3493, B_3492, C_3496, D_3494, E_3495, sK1_relation_exists_F(n0, n1, n0, n1, n0)), true, equalish(A_3493, n0), true)=true))). % 47.71/36.12 tff(c_80398, plain, (![B_3483, C_3484, E_3485, D_3486, A_3482]: (ifeq(f(A_3482, B_3483, C_3484, D_3486, E_3485, sK1_relation_exists_F(n1, n1, n0, n1, n0)), true, equalish(C_3484, n0), true)=true))). % 47.71/36.12 tff(c_80251, plain, (![D_3474, A_3473, C_3476, B_3472, E_3475]: (ifeq(f(A_3473, B_3472, C_3476, D_3474, E_3475, sK1_relation_exists_F(n0, n0, n1, n1, n0)), true, equalish(A_3473, n0), true)=true))). % 47.71/36.12 tff(c_80127, plain, (![E_3462, C_3466, D_3465, B_3463, A_3464]: (ifeq(f(A_3464, B_3463, C_3466, D_3465, E_3462, sK1_relation_exists_F(n1, n0, n1, n1, n0)), true, equalish(B_3463, n0), true)=true))). % 47.71/36.12 tff(c_79992, plain, (![D_3456, C_3453, B_3454, A_3455, E_3452]: (ifeq(f(A_3455, B_3454, C_3453, D_3456, E_3452, sK1_relation_exists_F(n0, n1, n1, n1, n0)), true, equalish(E_3452, n0), true)=true))). % 47.71/36.12 tff(c_79869, plain, (![D_3446, B_3443, A_3442, E_3445, C_3444]: (ifeq(f(A_3442, B_3443, C_3444, D_3446, E_3445, sK1_relation_exists_F(n1, n1, n1, n0, n0)), true, equalish(C_3444, n1), true)=true))). % 47.71/36.12 tff(c_79721, plain, (![D_3434, A_3433, B_3432, C_3436, E_3435]: (ifeq(f(A_3433, B_3432, C_3436, D_3434, E_3435, sK1_relation_exists_F(n1, n1, n1, n0, n1)), true, equalish(A_3433, n1), true)=true))). % 47.71/36.12 tff(c_79598, plain, (![E_3425, C_3424, D_3426, A_3422, B_3423]: (ifeq(f(A_3422, B_3423, C_3424, D_3426, E_3425, sK1_relation_exists_F(n0, n0, n0, n0, n1)), true, equalish(C_3424, n0), true)=true))). % 47.71/36.12 tff(c_79463, plain, (![B_3413, D_3415, E_3412, C_3416, A_3414]: (ifeq(f(A_3414, B_3413, C_3416, D_3415, E_3412, sK1_relation_exists_F(n1, n1, n1, n0, n1)), true, equalish(B_3413, n1), true)=true))). % 47.71/36.12 tff(c_79339, plain, (![C_3406, B_3402, D_3404, A_3403, E_3405]: (ifeq(f(A_3403, B_3402, C_3406, D_3404, E_3405, sK1_relation_exists_F(n0, n1, n1, n1, n0)), true, equalish(A_3403, n0), true)=true))). % 47.71/36.12 tff(c_79216, plain, (![A_3394, C_3396, B_3393, E_3392, D_3395]: (ifeq(f(A_3394, B_3393, C_3396, D_3395, E_3392, sK1_relation_exists_F(n1, n1, n1, n1, n0)), true, equalish(B_3393, n1), true)=true))). % 47.71/36.12 tff(c_79093, plain, (![D_3386, C_3384, A_3382, B_3383, E_3385]: (ifeq(f(A_3382, B_3383, C_3384, D_3386, E_3385, sK1_relation_exists_F(n1, n0, n1, n1, n0)), true, equalish(C_3384, n1), true)=true))). % 47.71/36.12 tff(c_78969, plain, (![B_3373, D_3376, E_3375, A_3372, C_3374]: (ifeq(f(A_3372, B_3373, C_3374, D_3376, E_3375, sK1_relation_exists_F(n1, n0, n1, n1, n1)), true, equalish(C_3374, n1), true)=true))). % 47.71/36.12 tff(c_78846, plain, (![B_3363, C_3364, E_3365, D_3366, A_3362]: (ifeq(f(A_3362, B_3363, C_3364, D_3366, E_3365, sK1_relation_exists_F(n1, n1, n1, n0, n1)), true, equalish(C_3364, n1), true)=true))). % 47.71/36.12 tff(c_78288, plain, (![A_3356]: (ifeq(equalish(A_3356, A_3356), true, f(A_3356, n0, n0, n0, n1, sK1_relation_exists_F(A_3356, n0, n0, n0, n1)), true)=true))). % 47.71/36.12 tff(c_78040, plain, (![B_3354]: (ifeq(equalish(B_3354, B_3354), true, f(n1, B_3354, n1, n1, n0, sK1_relation_exists_F(n1, B_3354, n1, n1, n0)), true)=true))). % 47.71/36.12 tff(c_22033, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n0, n0, n0, n1, n0)), true, equalish(n0, H_31), true)=true))). % 47.71/36.12 tff(c_22039, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n0, n0, n0, n1, n0)), true, equalish(n1, I_23), true)=true))). % 47.71/36.12 tff(c_22195, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n0, n0, n0, n1, n1)), true, equalish(n0, G_47), true)=true))). % 47.71/36.12 tff(c_22193, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n0, n0, n0, n1, n1)), true, equalish(n0, H_31), true)=true))). % 47.71/36.12 tff(c_22037, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n0, n0, n0, n1, n0)), true, equalish(n0, J_11), true)=true))). % 47.71/36.12 tff(c_22191, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n0, n0, n0, n1, n1)), true, equalish(n0, F_57), true)=true))). % 47.71/36.12 tff(c_22197, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n0, n0, n0, n1, n1)), true, equalish(n1, J_11), true)=true))). % 47.71/36.12 tff(c_77151, plain, (![B_3313]: (ifeq(equalish(B_3313, B_3313), true, f(n0, B_3313, n1, n0, n1, sK1_relation_exists_F(n0, B_3313, n1, n0, n1)), true)=true))). % 47.71/36.12 tff(c_22031, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n0, n0, n0, n1, n0)), true, equalish(n0, F_57), true)=true))). % 47.71/36.12 tff(c_76994, plain, (![J_55, H_53, G_3302, I_56, G_58]: (ifeq(f(G_3302, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n0, n0, n0, n1, n0)), true, true, true)=true))). % 47.71/36.12 tff(c_22035, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n0, n0, n0, n1, n0)), true, equalish(n0, G_47), true)=true))). % 47.71/36.12 tff(c_76885, plain, (![J_55, H_53, I_56, G_58, I_3288]: (ifeq(f(I_3288, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n0, n0, n0, n1, n1)), true, true, true)=true))). % 47.71/36.12 tff(c_22199, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n0, n0, n0, n1, n1)), true, equalish(n1, I_23), true)=true))). % 47.71/36.12 tff(c_22363, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n0, n0, n1, n1, n1)), true, equalish(n0, F_57), true)=true))). % 47.71/36.12 tff(c_41283, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n0, n0, n1, n0, n1)), true, equalish(n0, I_23), true)=true))). % 47.71/36.12 tff(c_32337, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n0, n1, n1, n1, n0)), true, equalish(n1, H_31), true)=true))). % 47.71/36.12 tff(c_36339, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n1, n0, n1, n1, n1)), true, equalish(n1, F_57), true)=true))). % 47.71/36.12 tff(c_23751, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n0, n0, n1, n1, n0)), true, equalish(n0, G_47), true)=true))). % 47.71/36.12 tff(c_32343, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n0, n1, n1, n1, n0)), true, equalish(n1, I_23), true)=true))). % 47.71/36.12 tff(c_36347, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n1, n0, n1, n1, n1)), true, equalish(n1, I_23), true)=true))). % 47.71/36.12 tff(c_23755, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n0, n0, n1, n1, n0)), true, equalish(n1, I_23), true)=true))). % 47.71/36.12 tff(c_46176, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n1, n1, n1, n1, n0)), true, equalish(n1, I_23), true)=true))). % 47.71/36.12 tff(c_14756, plain, (![C_943, B_944]: (ifeq(equalish(C_943, C_943), true, ifeq(equalish(B_944, B_944), true, f(n0, B_944, C_943, n0, n1, sK1_relation_exists_F(n0, B_944, C_943, n0, n1)), true), true)=true))). % 47.71/36.12 tff(c_23753, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n0, n0, n1, n1, n0)), true, equalish(n0, J_11), true)=true))). % 47.71/36.12 tff(c_29100, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n0, n1, n0, n1, n0)), true, equalish(n0, F_57), true)=true))). % 47.71/36.12 tff(c_41275, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n0, n0, n1, n0, n1)), true, equalish(n0, F_57), true)=true))). % 47.71/36.12 tff(c_75714, plain, (![A_3224]: (ifeq(equalish(A_3224, A_3224), true, f(A_3224, n0, n1, n0, n0, sK1_relation_exists_F(A_3224, n0, n1, n0, n0)), true)=true))). % 47.71/36.12 tff(c_27343, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n1, n1, n0, n1, n1)), true, equalish(n1, I_23), true)=true))). % 47.71/36.12 tff(c_27335, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n1, n1, n0, n1, n1)), true, equalish(n1, F_57), true)=true))). % 47.71/36.12 tff(c_29250, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n1, n1, n0, n1, n0)), true, equalish(n1, G_47), true)=true))). % 47.71/36.12 tff(c_57140, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n1, n0, n0, n1, n0)), true, equalish(n0, J_11), true)=true))). % 47.71/36.12 tff(c_36345, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n1, n0, n1, n1, n1)), true, equalish(n1, J_11), true)=true))). % 47.71/36.12 tff(c_41277, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n0, n0, n1, n0, n1)), true, equalish(n1, H_31), true)=true))). % 47.71/36.12 tff(c_27189, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n0, n1, n0, n1, n1)), true, equalish(n0, F_57), true)=true))). % 47.71/36.12 tff(c_37996, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n0, n1, n1, n0, n1)), true, equalish(n0, I_23), true)=true))). % 47.71/36.12 tff(c_34968, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n1, n0, n1, n1, n0)), true, equalish(n0, G_47), true)=true))). % 47.71/36.12 tff(c_22367, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n0, n0, n1, n1, n1)), true, equalish(n0, G_47), true)=true))). % 47.71/36.12 tff(c_41279, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n0, n0, n1, n0, n1)), true, equalish(n0, G_47), true)=true))). % 47.71/36.12 tff(c_27193, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n0, n1, n0, n1, n1)), true, equalish(n1, G_47), true)=true))). % 47.71/36.12 tff(c_43385, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n0, n0, n1, n0, n0)), true, equalish(n0, I_23), true)=true))). % 47.71/36.12 tff(c_46174, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n1, n1, n1, n1, n0)), true, equalish(n0, J_11), true)=true))). % 47.71/36.12 tff(c_41133, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n0, n0, n0, n0, n1)), true, equalish(n0, I_23), true)=true))). % 47.71/36.12 tff(c_43223, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n0, n0, n0, n0, n0)), true, equalish(n0, G_47), true)=true))). % 47.71/36.12 tff(c_36343, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n1, n0, n1, n1, n1)), true, equalish(n0, G_47), true)=true))). % 47.71/36.12 tff(c_37988, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n0, n1, n1, n0, n1)), true, equalish(n0, F_57), true)=true))). % 47.71/36.12 tff(c_34970, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n1, n0, n1, n1, n0)), true, equalish(n0, J_11), true)=true))). % 47.71/36.12 tff(c_47558, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n1, n1, n1, n0, n0)), true, equalish(n1, G_47), true)=true))). % 47.71/36.12 tff(c_43221, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n0, n0, n0, n0, n0)), true, equalish(n0, H_31), true)=true))). % 47.71/36.12 tff(c_46168, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n1, n1, n1, n1, n0)), true, equalish(n1, F_57), true)=true))). % 47.71/36.13 tff(c_74344, plain, (![B_3112]: (ifeq(equalish(B_3112, B_3112), true, f(n0, B_3112, n0, n0, n1, sK1_relation_exists_F(n0, B_3112, n0, n0, n1)), true)=true))). % 47.71/36.13 tff(c_32335, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n0, n1, n1, n1, n0)), true, equalish(n0, F_57), true)=true))). % 47.71/36.13 tff(c_49161, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n1, n1, n1, n0, n1)), true, equalish(n1, H_31), true)=true))). % 47.71/36.13 tff(c_59945, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n0, n1, n1, n1, n1)), true, equalish(n1, H_31), true)=true))). % 47.71/36.13 tff(c_59947, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n0, n1, n1, n1, n1)), true, equalish(n1, G_47), true)=true))). % 47.71/36.13 tff(c_29102, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n0, n1, n0, n1, n0)), true, equalish(n0, H_31), true)=true))). % 47.71/36.13 tff(c_41131, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n0, n0, n0, n0, n1)), true, equalish(n1, J_11), true)=true))). % 47.71/36.13 tff(c_23747, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n0, n0, n1, n1, n0)), true, equalish(n0, F_57), true)=true))). % 47.71/36.13 tff(c_51899, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n1, n1, n1, n1, n1)), true, equalish(n1, G_47), true)=true))). % 47.71/36.13 tff(c_57138, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n1, n0, n0, n1, n0)), true, equalish(n0, G_47), true)=true))). % 47.71/36.13 tff(c_34966, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n1, n0, n1, n1, n0)), true, equalish(n1, H_31), true)=true))). % 47.71/36.13 tff(c_27339, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n1, n1, n0, n1, n1)), true, equalish(n1, G_47), true)=true))). % 47.71/36.13 tff(c_46172, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n1, n1, n1, n1, n0)), true, equalish(n1, G_47), true)=true))). % 47.71/36.13 tff(c_49159, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n1, n1, n1, n0, n1)), true, equalish(n1, F_57), true)=true))). % 47.71/36.13 tff(c_43219, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n0, n0, n0, n0, n0)), true, equalish(n0, F_57), true)=true))). % 47.71/36.13 tff(c_32341, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n0, n1, n1, n1, n0)), true, equalish(n0, J_11), true)=true))). % 47.71/36.13 tff(c_37992, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n0, n1, n1, n0, n1)), true, equalish(n1, G_47), true)=true))). % 47.71/36.13 tff(c_51897, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n1, n1, n1, n1, n1)), true, equalish(n1, H_31), true)=true))). % 47.71/36.13 tff(c_31090, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n1, n0, n0, n1, n1)), true, equalish(n1, J_11), true)=true))). % 47.71/36.13 tff(c_27197, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n0, n1, n0, n1, n1)), true, equalish(n1, I_23), true)=true))). % 47.71/36.13 tff(c_29104, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n0, n1, n0, n1, n0)), true, equalish(n1, G_47), true)=true))). % 47.71/36.13 tff(c_41127, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n0, n0, n0, n0, n1)), true, equalish(n0, H_31), true)=true))). % 47.71/36.13 tff(c_34972, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n1, n0, n1, n1, n0)), true, equalish(n1, I_23), true)=true))). % 47.71/36.13 tff(c_47556, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n1, n1, n1, n0, n0)), true, equalish(n1, H_31), true)=true))). % 47.71/36.13 tff(c_72999, plain, (![J_55, H_53, J_2990, I_56, G_58]: (ifeq(f(J_2990, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n0, n0, n1, n0, n1)), true, true, true)=true))). % 47.71/36.13 tff(c_41281, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n0, n0, n1, n0, n1)), true, equalish(n1, J_11), true)=true))). % 47.71/36.13 tff(c_31086, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n1, n0, n0, n1, n1)), true, equalish(n0, H_31), true)=true))). % 47.71/36.13 tff(c_59949, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n0, n1, n1, n1, n1)), true, equalish(n1, J_11), true)=true))). % 47.71/36.13 tff(c_51895, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n1, n1, n1, n1, n1)), true, equalish(n1, F_57), true)=true))). % 47.71/36.13 tff(c_59951, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n0, n1, n1, n1, n1)), true, equalish(n1, I_23), true)=true))). % 47.71/36.13 tff(c_72697, plain, (![J_55, H_2958, H_53, I_56, G_58]: (ifeq(f(H_2958, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n1, n1, n1, n1, n0)), true, true, true)=true))). % 47.71/36.13 tff(c_46170, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n1, n1, n1, n1, n0)), true, equalish(n1, H_31), true)=true))). % 47.71/36.13 tff(c_31092, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n1, n0, n0, n1, n1)), true, equalish(n1, I_23), true)=true))). % 47.71/36.13 tff(c_51903, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n1, n1, n1, n1, n1)), true, equalish(n1, I_23), true)=true))). % 47.71/36.13 tff(c_47554, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n1, n1, n1, n0, n0)), true, equalish(n1, F_57), true)=true))). % 47.71/36.13 tff(c_43383, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n0, n0, n1, n0, n0)), true, equalish(n0, J_11), true)=true))). % 47.71/36.13 tff(c_57136, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n1, n0, n0, n1, n0)), true, equalish(n0, H_31), true)=true))). % 47.71/36.13 tff(c_72353, plain, (![J_55, H_53, I_56, G_58, H_2923]: (ifeq(f(H_2923, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n1, n0, n1, n1, n1)), true, true, true)=true))). % 47.71/36.13 tff(c_36341, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n1, n0, n1, n1, n1)), true, equalish(n1, H_31), true)=true))). % 47.71/36.13 tff(c_27191, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n0, n1, n0, n1, n1)), true, equalish(n0, H_31), true)=true))). % 47.71/36.13 tff(c_72098, plain, (![A_2915]: (ifeq(equalish(A_2915, A_2915), true, f(A_2915, n0, n0, n1, n1, sK1_relation_exists_F(A_2915, n0, n0, n1, n1)), true)=true))). % 47.71/36.13 tff(c_31084, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n1, n0, n0, n1, n1)), true, equalish(n1, F_57), true)=true))). % 47.71/36.13 tff(c_37990, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n0, n1, n1, n0, n1)), true, equalish(n1, H_31), true)=true))). % 47.71/36.13 tff(c_49165, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n1, n1, n1, n0, n1)), true, equalish(n1, J_11), true)=true))). % 47.71/36.13 tff(c_61957, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n0, n1, n1, n0, n0)), true, equalish(n0, I_23), true)=true))). % 47.71/36.13 tff(c_57142, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n1, n0, n0, n1, n0)), true, equalish(n1, I_23), true)=true))). % 47.71/36.13 tff(c_71749, plain, (![G_2884, J_55, H_53, I_56, G_58]: (ifeq(f(G_2884, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n0, n1, n1, n1, n0)), true, true, true)=true))). % 47.71/36.13 tff(c_32339, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n0, n1, n1, n1, n0)), true, equalish(n1, G_47), true)=true))). % 47.71/36.13 tff(c_4560, plain, (![E_408, A_410]: (ifeq(equalish(E_408, E_408), true, ifeq(equalish(A_410, A_410), true, f(A_410, n0, n1, n0, E_408, sK1_relation_exists_F(A_410, n0, n1, n0, E_408)), true), true)=true))). % 47.71/36.13 tff(c_71427, plain, (![J_55, J_2871, H_53, I_56, G_58]: (ifeq(f(J_2871, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n1, n1, n1, n1, n1)), true, true, true)=true))). % 47.71/36.13 tff(c_51901, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n1, n1, n1, n1, n1)), true, equalish(n1, J_11), true)=true))). % 47.71/36.13 tff(c_71205, plain, (![B_2866]: (ifeq(equalish(B_2866, B_2866), true, f(n1, B_2866, n0, n1, n0, sK1_relation_exists_F(n1, B_2866, n0, n1, n0)), true)=true))). % 47.71/36.13 tff(c_71081, plain, (![J_55, H_53, I_56, G_58, H_2857]: (ifeq(f(H_2857, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n0, n0, n1, n1, n0)), true, true, true)=true))). % 47.71/36.13 tff(c_23749, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n0, n0, n1, n1, n0)), true, equalish(n1, H_31), true)=true))). % 47.71/36.13 tff(c_22371, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n0, n0, n1, n1, n1)), true, equalish(n1, I_23), true)=true))). % 47.71/36.13 tff(c_29106, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n0, n1, n0, n1, n0)), true, equalish(n0, J_11), true)=true))). % 47.71/36.13 tff(c_61953, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n0, n1, n1, n0, n0)), true, equalish(n1, G_47), true)=true))). % 47.71/36.13 tff(c_70802, plain, (![J_55, H_53, I_56, G_58, G_2835]: (ifeq(f(G_2835, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n1, n0, n0, n1, n1)), true, true, true)=true))). % 47.71/36.13 tff(c_31088, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n1, n0, n0, n1, n1)), true, equalish(n0, G_47), true)=true))). % 47.71/36.13 tff(c_29254, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n1, n1, n0, n1, n0)), true, equalish(n1, I_23), true)=true))). % 47.71/36.13 tff(c_41129, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n0, n0, n0, n0, n1)), true, equalish(n0, G_47), true)=true))). % 47.71/36.13 tff(c_70491, plain, (![A_2819]: (ifeq(equalish(A_2819, A_2819), true, f(A_2819, n1, n1, n0, n0, sK1_relation_exists_F(A_2819, n1, n1, n0, n0)), true)=true))). % 47.71/36.13 tff(c_27341, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n1, n1, n0, n1, n1)), true, equalish(n1, J_11), true)=true))). % 47.71/36.13 tff(c_47560, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n1, n1, n1, n0, n0)), true, equalish(n0, J_11), true)=true))). % 47.71/36.13 tff(c_70294, plain, (![J_55, H_53, I_56, G_58, I_2799]: (ifeq(f(I_2799, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n1, n1, n1, n0, n0)), true, true, true)=true))). % 47.71/36.13 tff(c_47562, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n1, n1, n1, n0, n0)), true, equalish(n0, I_23), true)=true))). % 47.71/36.13 tff(c_49163, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n1, n1, n1, n0, n1)), true, equalish(n1, G_47), true)=true))). % 47.71/36.13 tff(c_61951, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n0, n1, n1, n0, n0)), true, equalish(n1, H_31), true)=true))). % 47.71/36.13 tff(c_29246, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n1, n1, n0, n1, n0)), true, equalish(n1, F_57), true)=true))). % 47.71/36.13 tff(c_43225, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n0, n0, n0, n0, n0)), true, equalish(n0, J_11), true)=true))). % 47.71/36.13 tff(c_70019, plain, (![F_2772, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, F_2772, I_34, J_33, sK1_relation_exists_F(n0, n1, n1, n1, n1)), true, true, true)=true))). % 47.71/36.13 tff(c_59943, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n0, n1, n1, n1, n1)), true, equalish(n0, F_57), true)=true))). % 47.71/36.13 tff(c_69908, plain, (![J_33, F_2762, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, F_2762, I_34, J_33, sK1_relation_exists_F(n1, n0, n1, n1, n0)), true, true, true)=true))). % 47.71/36.13 tff(c_34964, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n1, n0, n1, n1, n0)), true, equalish(n1, F_57), true)=true))). % 47.71/36.13 tff(c_43377, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n0, n0, n1, n0, n0)), true, equalish(n0, F_57), true)=true))). % 47.71/36.13 tff(c_29252, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n1, n1, n0, n1, n0)), true, equalish(n0, J_11), true)=true))). % 47.71/36.13 tff(c_22369, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n0, n0, n1, n1, n1)), true, equalish(n1, J_11), true)=true))). % 47.71/36.13 tff(c_69633, plain, (![J_55, H_53, I_2734, I_56, G_58]: (ifeq(f(I_2734, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n0, n0, n0, n0, n0)), true, true, true)=true))). % 47.71/36.13 tff(c_43227, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n0, n0, n0, n0, n0)), true, equalish(n0, I_23), true)=true))). % 47.71/36.13 tff(c_43381, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n0, n0, n1, n0, n0)), true, equalish(n0, G_47), true)=true))). % 47.71/36.13 tff(c_69484, plain, (![J_55, J_2722, H_53, I_56, G_58]: (ifeq(f(J_2722, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n0, n1, n0, n1, n1)), true, true, true)=true))). % 47.71/36.13 tff(c_27195, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n0, n1, n0, n1, n1)), true, equalish(n1, J_11), true)=true))). % 47.71/36.13 tff(c_69374, plain, (![J_55, H_53, I_56, G_58, H_2710]: (ifeq(f(H_2710, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n1, n1, n0, n1, n1)), true, true, true)=true))). % 47.71/36.13 tff(c_27337, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n1, n1, n0, n1, n1)), true, equalish(n0, H_31), true)=true))). % 47.71/36.13 tff(c_69269, plain, (![J_33, F_2702, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, F_2702, I_34, J_33, sK1_relation_exists_F(n0, n0, n0, n0, n1)), true, true, true)=true))). % 47.71/36.13 tff(c_41125, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n0, n0, n0, n0, n1)), true, equalish(n0, F_57), true)=true))). % 47.71/36.13 tff(c_69155, plain, (![H_2690, J_55, H_53, I_56, G_58]: (ifeq(f(H_2690, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n1, n1, n0, n1, n0)), true, true, true)=true))). % 47.71/36.13 tff(c_29248, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n1, n1, n0, n1, n0)), true, equalish(n0, H_31), true)=true))). % 47.71/36.14 tff(c_69044, plain, (![J_55, H_53, I_56, G_58, J_2682]: (ifeq(f(J_2682, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n0, n1, n1, n0, n1)), true, true, true)=true))). % 47.71/36.14 tff(c_37994, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n0, n1, n1, n0, n1)), true, equalish(n1, J_11), true)=true))). % 47.71/36.14 tff(c_68935, plain, (![J_55, H_53, I_56, H_2670, G_58]: (ifeq(f(H_2670, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n0, n0, n1, n0, n0)), true, true, true)=true))). % 47.71/36.14 tff(c_43379, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n0, n0, n1, n0, n0)), true, equalish(n1, H_31), true)=true))). % 47.71/36.14 tff(c_61955, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n0, n1, n1, n0, n0)), true, equalish(n0, J_11), true)=true))). % 47.71/36.14 tff(c_68777, plain, (![J_55, H_53, I_56, G_58, I_2654]: (ifeq(f(I_2654, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n0, n1, n0, n1, n0)), true, true, true)=true))). % 47.71/36.14 tff(c_29108, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n0, n1, n0, n1, n0)), true, equalish(n1, I_23), true)=true))). % 47.71/36.14 tff(c_68658, plain, (![J_55, H_53, I_56, H_2645, G_58]: (ifeq(f(H_2645, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n0, n0, n1, n1, n1)), true, true, true)=true))). % 47.71/36.14 tff(c_22365, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n0, n0, n1, n1, n1)), true, equalish(n1, H_31), true)=true))). % 47.71/36.14 tff(c_68542, plain, (![J_55, H_53, I_56, I_2634, G_58]: (ifeq(f(I_2634, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n1, n1, n1, n0, n1)), true, true, true)=true))). % 47.71/36.14 tff(c_49167, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n1, n1, n1, n0, n1)), true, equalish(n0, I_23), true)=true))). % 47.71/36.14 tff(c_68435, plain, (![J_33, F_2627, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, F_2627, I_34, J_33, sK1_relation_exists_F(n1, n0, n0, n1, n0)), true, true, true)=true))). % 47.71/36.14 tff(c_57134, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n1, n0, n0, n1, n0)), true, equalish(n1, F_57), true)=true))). % 47.71/36.14 tff(c_68326, plain, (![J_33, F_2617, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, F_2617, I_34, J_33, sK1_relation_exists_F(n0, n1, n1, n0, n0)), true, true, true)=true))). % 47.71/36.14 tff(c_61949, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n0, n1, n1, n0, n0)), true, equalish(n0, F_57), true)=true))). % 47.71/36.14 tff(c_68107, plain, (![B_2612]: (ifeq(equalish(B_2612, B_2612), true, f(n1, B_2612, n1, n0, n1, sK1_relation_exists_F(n1, B_2612, n1, n0, n1)), true)=true))). % 47.71/36.14 tff(c_58268, plain, (![D_2468]: (ifeq(equalish(D_2468, D_2468), true, f(n0, n1, n1, D_2468, n0, sK1_relation_exists_F(n0, n1, n1, D_2468, n0)), true)=true))). % 47.71/36.14 tff(c_67509, plain, (![B_2608]: (ifeq(equalish(B_2608, B_2608), true, f(n0, B_2608, n1, n1, n1, sK1_relation_exists_F(n0, B_2608, n1, n1, n1)), true)=true))). % 47.71/36.14 tff(c_37559, plain, (![D_1932]: (ifeq(equalish(D_1932, D_1932), true, f(n1, n0, n1, D_1932, n1, sK1_relation_exists_F(n1, n0, n1, D_1932, n1)), true)=true))). % 47.71/36.14 tff(c_53754, plain, (![E_2392]: (ifeq(equalish(E_2392, E_2392), true, f(n0, n0, n1, n1, E_2392, sK1_relation_exists_F(n0, n0, n1, n1, E_2392)), true)=true))). % 47.71/36.14 tff(c_55067, plain, (![E_2406]: (ifeq(equalish(E_2406, E_2406), true, f(n1, n1, n0, n1, E_2406, sK1_relation_exists_F(n1, n1, n0, n1, E_2406)), true)=true))). % 47.71/36.14 tff(c_20558, plain, (![C_1277, A_1279]: (ifeq(equalish(C_1277, C_1277), true, ifeq(equalish(A_1279, A_1279), true, f(A_1279, n0, C_1277, n1, n0, sK1_relation_exists_F(A_1279, n0, C_1277, n1, n0)), true), true)=true))). % 47.71/36.14 tff(c_61532, plain, (![D_2530]: (ifeq(equalish(D_2530, D_2530), true, f(n0, n1, n1, D_2530, n1, sK1_relation_exists_F(n0, n1, n1, D_2530, n1)), true)=true))). % 47.71/36.14 tff(c_40421, plain, (![D_2005]: (ifeq(equalish(D_2005, D_2005), true, f(n1, n1, n0, D_2005, n1, sK1_relation_exists_F(n1, n1, n0, D_2005, n1)), true)=true))). % 47.71/36.14 tff(c_65839, plain, (![A_2597]: (ifeq(equalish(A_2597, A_2597), true, f(A_2597, n1, n1, n1, n0, sK1_relation_exists_F(A_2597, n1, n1, n1, n0)), true)=true))). % 47.71/36.14 tff(c_49582, plain, (![D_2295]: (ifeq(equalish(D_2295, D_2295), true, f(n1, n1, n1, D_2295, n0, sK1_relation_exists_F(n1, n1, n1, D_2295, n0)), true)=true))). % 47.71/36.14 tff(c_36751, plain, (![E_1905]: (ifeq(equalish(E_1905, E_1905), true, f(n1, n0, n0, n1, E_1905, sK1_relation_exists_F(n1, n0, n0, n1, E_1905)), true)=true))). % 47.71/36.14 tff(c_44397, plain, (![E_2134]: (ifeq(equalish(E_2134, E_2134), true, f(n1, n0, n1, n1, E_2134, sK1_relation_exists_F(n1, n0, n1, n1, E_2134)), true)=true))). % 47.71/36.14 tff(c_44749, plain, (![E_2144]: (ifeq(equalish(E_2144, E_2144), true, f(n0, n1, n1, n1, E_2144, sK1_relation_exists_F(n0, n1, n1, n1, E_2144)), true)=true))). % 47.71/36.14 tff(c_6399, plain, (![D_497, A_499]: (ifeq(equalish(D_497, D_497), true, ifeq(equalish(A_499, A_499), true, f(A_499, n0, n0, D_497, n1, sK1_relation_exists_F(A_499, n0, n0, D_497, n1)), true), true)=true))). % 47.71/36.14 tff(c_28316, plain, (![E_1624]: (ifeq(equalish(E_1624, E_1624), true, f(n1, n1, n1, n1, E_1624, sK1_relation_exists_F(n1, n1, n1, n1, E_1624)), true)=true))). % 47.71/36.14 tff(c_50718, plain, (![D_2325]: (ifeq(equalish(D_2325, D_2325), true, f(n1, n0, n0, D_2325, n0, sK1_relation_exists_F(n1, n0, n0, D_2325, n0)), true)=true))). % 47.71/36.14 tff(c_58876, plain, (![E_2474]: (ifeq(equalish(E_2474, E_2474), true, f(n0, n1, n1, n0, E_2474, sK1_relation_exists_F(n0, n1, n1, n0, E_2474)), true)=true))). % 47.71/36.14 tff(c_45180, plain, (![E_2155]: (ifeq(equalish(E_2155, E_2155), true, f(n0, n0, n0, n0, E_2155, sK1_relation_exists_F(n0, n0, n0, n0, E_2155)), true)=true))). % 47.71/36.14 tff(c_56755, plain, (![C_2423]: (ifeq(equalish(C_2423, C_2423), true, f(n0, n1, C_2423, n0, n0, sK1_relation_exists_F(n0, n1, C_2423, n0, n0)), true)=true))). % 47.71/36.14 tff(c_61531, plain, (![D_2530]: (ifeq(equalish(D_2530, D_2530), true, f(n0, n0, n1, D_2530, n1, sK1_relation_exists_F(n0, n0, n1, D_2530, n1)), true)=true))). % 47.71/36.14 tff(c_20559, plain, (![C_1277, B_1278]: (ifeq(equalish(C_1277, C_1277), true, ifeq(equalish(B_1278, B_1278), true, f(n0, B_1278, C_1277, n1, n0, sK1_relation_exists_F(n0, B_1278, C_1277, n1, n0)), true), true)=true))). % 47.71/36.14 tff(c_63135, plain, (![E_2576]: (ifeq(equalish(E_2576, E_2576), true, f(n1, n1, n1, n0, E_2576, sK1_relation_exists_F(n1, n1, n1, n0, E_2576)), true)=true))). % 47.71/36.14 tff(c_51700, plain, (![E_2340]: (ifeq(equalish(E_2340, E_2340), true, f(n0, n1, n0, n1, E_2340, sK1_relation_exists_F(n0, n1, n0, n1, E_2340)), true)=true))). % 47.71/36.14 tff(c_54122, plain, (![E_2396]: (ifeq(equalish(E_2396, E_2396), true, f(n0, n0, n1, n0, E_2396, sK1_relation_exists_F(n0, n0, n1, n0, E_2396)), true)=true))). % 47.71/36.14 tff(c_53190, plain, (![D_2386]: (ifeq(equalish(D_2386, D_2386), true, f(n1, n1, n1, D_2386, n1, sK1_relation_exists_F(n1, n1, n1, D_2386, n1)), true)=true))). % 47.71/36.14 tff(c_63386, plain, (![A_2580]: (ifeq(equalish(A_2580, A_2580), true, f(A_2580, n0, n1, n0, n1, sK1_relation_exists_F(A_2580, n0, n1, n0, n1)), true)=true))). % 47.71/36.14 tff(c_63161, plain, (![D_2578]: (ifeq(equalish(D_2578, D_2578), true, f(n0, n0, n1, D_2578, n0, sK1_relation_exists_F(n0, n0, n1, D_2578, n0)), true)=true))). % 47.71/36.14 tff(c_710, plain, (![E_221, C_222]: (ifeq(equalish(E_221, E_221), true, ifeq(equalish(C_222, C_222), true, f(n1, n1, C_222, n0, E_221, sK1_relation_exists_F(n1, n1, C_222, n0, E_221)), true), true)=true))). % 47.71/36.14 tff(c_61769, plain, (![B_2534]: (ifeq(equalish(B_2534, B_2534), true, f(n0, B_2534, n1, n0, n0, sK1_relation_exists_F(n0, B_2534, n1, n0, n0)), true)=true))). % 47.71/36.14 tff(c_61780, plain, (f(n0, n1, n1, n0, n0, sK1_relation_exists_F(n0, n1, n1, n0, n0))=true)). % 47.71/36.14 tff(c_61575, plain, (![A_2532]: (ifeq(equalish(A_2532, A_2532), true, f(A_2532, n1, n1, n0, n1, sK1_relation_exists_F(A_2532, n1, n1, n0, n1)), true)=true))). % 47.71/36.14 tff(c_5397, plain, (![D_447, B_449]: (ifeq(equalish(D_447, D_447), true, ifeq(equalish(B_449, B_449), true, f(n0, B_449, n1, D_447, n1, sK1_relation_exists_F(n0, B_449, n1, D_447, n1)), true), true)=true))). % 47.71/36.14 tff(c_61160, plain, (![C_2528]: (ifeq(equalish(C_2528, C_2528), true, f(n0, n1, C_2528, n1, n1, sK1_relation_exists_F(n0, n1, C_2528, n1, n1)), true)=true))). % 47.71/36.14 tff(c_18975, plain, (![D_1154, A_1156]: (ifeq(equalish(D_1154, D_1154), true, ifeq(equalish(A_1156, A_1156), true, f(A_1156, n1, n0, D_1154, n1, sK1_relation_exists_F(A_1156, n1, n0, D_1154, n1)), true), true)=true))). % 47.71/36.14 tff(c_59751, plain, (![A_2484]: (ifeq(equalish(A_2484, A_2484), true, f(A_2484, n1, n1, n1, n1, sK1_relation_exists_F(A_2484, n1, n1, n1, n1)), true)=true))). % 47.71/36.14 tff(c_59777, plain, (f(n0, n1, n1, n1, n1, sK1_relation_exists_F(n0, n1, n1, n1, n1))=true)). % 47.71/36.14 tff(c_59528, plain, (![C_2482]: (ifeq(equalish(C_2482, C_2482), true, f(n1, n0, C_2482, n1, n0, sK1_relation_exists_F(n1, n0, C_2482, n1, n0)), true)=true))). % 47.71/36.14 tff(c_17176, plain, (![C_1051, A_1053]: (ifeq(equalish(C_1051, C_1051), true, ifeq(equalish(A_1053, A_1053), true, f(A_1053, n0, C_1051, n0, n0, sK1_relation_exists_F(A_1053, n0, C_1051, n0, n0)), true), true)=true))). % 47.71/36.14 tff(c_59110, plain, (![B_2478]: (ifeq(equalish(B_2478, B_2478), true, f(n1, B_2478, n0, n0, n0, sK1_relation_exists_F(n1, B_2478, n0, n0, n0)), true)=true))). % 47.71/36.14 tff(c_4391, plain, (![C_396, A_398]: (ifeq(equalish(C_396, C_396), true, ifeq(equalish(A_398, A_398), true, f(A_398, n0, C_396, n1, n1, sK1_relation_exists_F(A_398, n0, C_396, n1, n1)), true), true)=true))). % 47.71/36.14 tff(c_8281, plain, (![E_609, D_610]: (ifeq(equalish(E_609, E_609), true, ifeq(equalish(D_610, D_610), true, f(n0, n1, n1, D_610, E_609, sK1_relation_exists_F(n0, n1, n1, D_610, E_609)), true), true)=true))). % 47.71/36.14 tff(c_58505, plain, (![D_2472]: (ifeq(equalish(D_2472, D_2472), true, f(n0, n1, n0, D_2472, n0, sK1_relation_exists_F(n0, n1, n0, D_2472, n0)), true)=true))). % 47.71/36.14 tff(c_20560, plain, (![C_1277, A_1279]: (ifeq(equalish(C_1277, C_1277), true, ifeq(equalish(A_1279, A_1279), true, f(A_1279, n1, C_1277, n1, n0, sK1_relation_exists_F(A_1279, n1, C_1277, n1, n0)), true), true)=true))). % 47.71/36.14 tff(c_9456, plain, (![D_688, A_690]: (ifeq(equalish(D_688, D_688), true, ifeq(equalish(A_690, A_690), true, f(A_690, n1, n1, D_688, n0, sK1_relation_exists_F(A_690, n1, n1, D_688, n0)), true), true)=true))). % 47.71/36.14 tff(c_56938, plain, (![A_2426]: (ifeq(equalish(A_2426, A_2426), true, f(A_2426, n0, n0, n1, n0, sK1_relation_exists_F(A_2426, n0, n0, n1, n0)), true)=true))). % 47.71/36.14 tff(c_56969, plain, (f(n1, n0, n0, n1, n0, sK1_relation_exists_F(n1, n0, n0, n1, n0))=true)). % 47.71/36.14 tff(c_56550, plain, (![D_2422]: (ifeq(equalish(D_2422, D_2422), true, f(n0, n0, n0, D_2422, n1, sK1_relation_exists_F(n0, n0, n0, D_2422, n1)), true)=true))). % 47.71/36.14 tff(c_17177, plain, (![C_1051, B_1052]: (ifeq(equalish(C_1051, C_1051), true, ifeq(equalish(B_1052, B_1052), true, f(n0, B_1052, C_1051, n0, n0, sK1_relation_exists_F(n0, B_1052, C_1051, n0, n0)), true), true)=true))). % 47.71/36.14 tff(c_6951, plain, (![D_524, C_525]: (ifeq(equalish(D_524, D_524), true, ifeq(equalish(C_525, C_525), true, f(n0, n0, C_525, D_524, n1, sK1_relation_exists_F(n0, n0, C_525, D_524, n1)), true), true)=true))). % 47.71/36.14 tff(c_18449, plain, (![E_1121, C_1123]: (ifeq(equalish(E_1121, E_1121), true, ifeq(equalish(C_1123, C_1123), true, f(n1, n1, C_1123, n1, E_1121, sK1_relation_exists_F(n1, n1, C_1123, n1, E_1121)), true), true)=true))). % 47.71/36.14 tff(c_55957, plain, (![B_2416]: (ifeq(equalish(B_2416, B_2416), true, f(n0, B_2416, n1, n1, n0, sK1_relation_exists_F(n0, B_2416, n1, n1, n0)), true)=true))). % 47.71/36.14 tff(c_55734, plain, (![C_2414]: (ifeq(equalish(C_2414, C_2414), true, f(n1, n0, C_2414, n1, n1, sK1_relation_exists_F(n1, n0, C_2414, n1, n1)), true)=true))). % 47.71/36.14 tff(c_4392, plain, (![C_396, B_397]: (ifeq(equalish(C_396, C_396), true, ifeq(equalish(B_397, B_397), true, f(n0, B_397, C_396, n1, n1, sK1_relation_exists_F(n0, B_397, C_396, n1, n1)), true), true)=true))). % 47.71/36.14 tff(c_55306, plain, (![D_2410]: (ifeq(equalish(D_2410, D_2410), true, f(n0, n0, n0, D_2410, n0, sK1_relation_exists_F(n0, n0, n0, D_2410, n0)), true)=true))). % 47.71/36.14 tff(c_12671, plain, (![E_865, B_867]: (ifeq(equalish(E_865, E_865), true, ifeq(equalish(B_867, B_867), true, f(n1, B_867, n0, n0, E_865, sK1_relation_exists_F(n1, B_867, n0, n0, E_865)), true), true)=true))). % 47.71/36.14 tff(c_9118, plain, (![E_670, B_672]: (ifeq(equalish(E_670, E_670), true, ifeq(equalish(B_672, B_672), true, f(n1, B_672, n0, n1, E_670, sK1_relation_exists_F(n1, B_672, n0, n1, E_670)), true), true)=true))). % 47.71/36.14 tff(c_54701, plain, (![B_2404]: (ifeq(equalish(B_2404, B_2404), true, f(n0, B_2404, n0, n1, n1, sK1_relation_exists_F(n0, B_2404, n0, n1, n1)), true)=true))). % 47.71/36.14 tff(c_9454, plain, (![D_688, A_690]: (ifeq(equalish(D_688, D_688), true, ifeq(equalish(A_690, A_690), true, f(A_690, n1, n0, D_688, n0, sK1_relation_exists_F(A_690, n1, n0, D_688, n0)), true), true)=true))). % 47.71/36.14 tff(c_54149, plain, (![A_2398]: (ifeq(equalish(A_2398, A_2398), true, f(A_2398, n0, n0, n0, n0, sK1_relation_exists_F(A_2398, n0, n0, n0, n0)), true)=true))). % 47.71/36.14 tff(c_14755, plain, (![C_943, A_945]: (ifeq(equalish(C_943, C_943), true, ifeq(equalish(A_945, A_945), true, f(A_945, n0, C_943, n0, n1, sK1_relation_exists_F(A_945, n0, C_943, n0, n1)), true), true)=true))). % 47.71/36.14 tff(c_5051, plain, (![E_432, B_433]: (ifeq(equalish(E_432, E_432), true, ifeq(equalish(B_433, B_433), true, f(n0, B_433, n1, n0, E_432, sK1_relation_exists_F(n0, B_433, n1, n0, E_432)), true), true)=true))). % 47.71/36.14 tff(c_53777, plain, (![C_2394]: (ifeq(equalish(C_2394, C_2394), true, f(n1, n1, C_2394, n1, n1, sK1_relation_exists_F(n1, n1, C_2394, n1, n1)), true)=true))). % 47.71/36.14 tff(c_16369, plain, (![E_1020, D_1021]: (ifeq(equalish(E_1020, E_1020), true, ifeq(equalish(D_1021, D_1021), true, f(n0, n0, n1, D_1021, E_1020, sK1_relation_exists_F(n0, n0, n1, D_1021, E_1020)), true), true)=true))). % 47.71/36.14 tff(c_53226, plain, (![D_2388]: (ifeq(equalish(D_2388, D_2388), true, f(n0, n1, n0, D_2388, n1, sK1_relation_exists_F(n0, n1, n0, D_2388, n1)), true)=true))). % 47.71/36.14 tff(c_17406, plain, (![D_1064, A_1066]: (ifeq(equalish(D_1064, D_1064), true, ifeq(equalish(A_1066, A_1066), true, f(A_1066, n0, n0, D_1064, n0, sK1_relation_exists_F(A_1066, n0, n0, D_1064, n0)), true), true)=true))). % 47.71/36.14 tff(c_18977, plain, (![D_1154, A_1156]: (ifeq(equalish(D_1154, D_1154), true, ifeq(equalish(A_1156, A_1156), true, f(A_1156, n1, n1, D_1154, n1, sK1_relation_exists_F(A_1156, n1, n1, D_1154, n1)), true), true)=true))). % 47.71/36.14 tff(c_51727, plain, (![B_2342]: (ifeq(equalish(B_2342, B_2342), true, f(n1, B_2342, n1, n1, n1, sK1_relation_exists_F(n1, B_2342, n1, n1, n1)), true)=true))). % 47.71/36.14 tff(c_4393, plain, (![C_396, A_398]: (ifeq(equalish(C_396, C_396), true, ifeq(equalish(A_398, A_398), true, f(A_398, n1, C_396, n1, n1, sK1_relation_exists_F(A_398, n1, C_396, n1, n1)), true), true)=true))). % 47.71/36.14 tff(c_51738, plain, (f(n1, n1, n1, n1, n1, sK1_relation_exists_F(n1, n1, n1, n1, n1))=true)). % 47.71/36.14 tff(c_17869, plain, (![E_1088, D_1089]: (ifeq(equalish(E_1088, E_1088), true, ifeq(equalish(D_1089, D_1089), true, f(n0, n1, n0, D_1089, E_1088, sK1_relation_exists_F(n0, n1, n0, D_1089, E_1088)), true), true)=true))). % 47.71/36.14 tff(c_51047, plain, (![B_2332]: (ifeq(equalish(B_2332, B_2332), true, f(n1, B_2332, n1, n0, n0, sK1_relation_exists_F(n1, B_2332, n1, n0, n0)), true)=true))). % 47.88/36.14 tff(c_7603, plain, (![D_561, C_562]: (ifeq(equalish(D_561, D_561), true, ifeq(equalish(C_562, C_562), true, f(n0, n1, C_562, D_561, n0, sK1_relation_exists_F(n0, n1, C_562, D_561, n0)), true), true)=true))). % 47.88/36.14 tff(c_50490, plain, (![B_2324]: (ifeq(equalish(B_2324, B_2324), true, f(n1, B_2324, n0, n0, n1, sK1_relation_exists_F(n1, B_2324, n0, n0, n1)), true)=true))). % 47.88/36.14 tff(c_6675, plain, (![D_513, B_515]: (ifeq(equalish(D_513, D_513), true, ifeq(equalish(B_515, B_515), true, f(n1, B_515, n0, D_513, n0, sK1_relation_exists_F(n1, B_515, n0, D_513, n0)), true), true)=true))). % 47.88/36.14 tff(c_14758, plain, (![C_943, B_944]: (ifeq(equalish(C_943, C_943), true, ifeq(equalish(B_944, B_944), true, f(n1, B_944, C_943, n0, n1, sK1_relation_exists_F(n1, B_944, C_943, n0, n1)), true), true)=true))). % 47.88/36.14 tff(c_48991, plain, (![C_2278]: (ifeq(equalish(C_2278, C_2278), true, f(n1, n1, C_2278, n0, n1, sK1_relation_exists_F(n1, n1, C_2278, n0, n1)), true)=true))). % 47.88/36.14 tff(c_17031, plain, (![D_1048, B_1049]: (ifeq(equalish(D_1048, D_1048), true, ifeq(equalish(B_1049, B_1049), true, f(n1, B_1049, n1, D_1048, n0, sK1_relation_exists_F(n1, B_1049, n1, D_1048, n0)), true), true)=true))). % 47.88/36.14 tff(c_49002, plain, (f(n1, n1, n1, n0, n1, sK1_relation_exists_F(n1, n1, n1, n0, n1))=true)). % 47.88/36.14 tff(c_15056, plain, (![D_960, B_962]: (ifeq(equalish(D_960, D_960), true, ifeq(equalish(B_962, B_962), true, f(n1, B_962, n0, D_960, n1, sK1_relation_exists_F(n1, B_962, n0, D_960, n1)), true), true)=true))). % 47.88/36.14 tff(c_47388, plain, (![C_2228]: (ifeq(equalish(C_2228, C_2228), true, f(n1, n1, C_2228, n0, n0, sK1_relation_exists_F(n1, n1, C_2228, n0, n0)), true)=true))). % 47.88/36.14 tff(c_8283, plain, (![E_609, D_610]: (ifeq(equalish(E_609, E_609), true, ifeq(equalish(D_610, D_610), true, f(n1, n1, n1, D_610, E_609, sK1_relation_exists_F(n1, n1, n1, D_610, E_609)), true), true)=true))). % 47.88/36.14 tff(c_47401, plain, (f(n1, n1, n1, n0, n0, sK1_relation_exists_F(n1, n1, n1, n0, n0))=true)). % 47.88/36.14 tff(c_11441, plain, (![E_817, B_819]: (ifeq(equalish(E_817, E_817), true, ifeq(equalish(B_819, B_819), true, f(n1, B_819, n1, n0, E_817, sK1_relation_exists_F(n1, B_819, n1, n0, E_817)), true), true)=true))). % 47.88/36.14 tff(c_46000, plain, (![C_2180]: (ifeq(equalish(C_2180, C_2180), true, f(n1, n1, C_2180, n1, n0, sK1_relation_exists_F(n1, n1, C_2180, n1, n0)), true)=true))). % 47.88/36.15 tff(c_46019, plain, (f(n1, n1, n1, n1, n0, sK1_relation_exists_F(n1, n1, n1, n1, n0))=true)). % 47.88/36.15 tff(c_17179, plain, (![C_1051, B_1052]: (ifeq(equalish(C_1051, C_1051), true, ifeq(equalish(B_1052, B_1052), true, f(n1, B_1052, C_1051, n0, n0, sK1_relation_exists_F(n1, B_1052, C_1051, n0, n0)), true), true)=true))). % 47.88/36.15 tff(c_44991, plain, (![B_2154]: (ifeq(equalish(B_2154, B_2154), true, f(n0, B_2154, n0, n0, n0, sK1_relation_exists_F(n0, B_2154, n0, n0, n0)), true)=true))). % 47.88/36.15 tff(c_15154, plain, (![E_963, D_964]: (ifeq(equalish(E_963, E_963), true, ifeq(equalish(D_964, D_964), true, f(n0, n0, n0, D_964, E_963, sK1_relation_exists_F(n0, n0, n0, D_964, E_963)), true), true)=true))). % 47.88/36.15 tff(c_6301, plain, (![E_494, B_496]: (ifeq(equalish(E_494, E_494), true, ifeq(equalish(B_496, B_496), true, f(n0, B_496, n1, n1, E_494, sK1_relation_exists_F(n0, B_496, n1, n1, E_494)), true), true)=true))). % 47.88/36.15 tff(c_4562, plain, (![E_408, A_410]: (ifeq(equalish(E_408, E_408), true, ifeq(equalish(A_410, A_410), true, f(A_410, n0, n1, n1, E_408, sK1_relation_exists_F(A_410, n0, n1, n1, E_408)), true), true)=true))). % 47.88/36.15 tff(c_43051, plain, (![C_2088]: (ifeq(equalish(C_2088, C_2088), true, f(n0, n0, C_2088, n0, n0, sK1_relation_exists_F(n0, n0, C_2088, n0, n0)), true)=true))). % 47.88/36.15 tff(c_43066, plain, (f(n0, n0, n1, n0, n0, sK1_relation_exists_F(n0, n0, n1, n0, n0))=true)). % 47.88/36.15 tff(c_43065, plain, (f(n0, n0, n0, n0, n0, sK1_relation_exists_F(n0, n0, n0, n0, n0))=true)). % 47.88/36.15 tff(c_17407, plain, (![D_1064, C_1065]: (ifeq(equalish(D_1064, D_1064), true, ifeq(equalish(C_1065, C_1065), true, f(n0, n0, C_1065, D_1064, n0, sK1_relation_exists_F(n0, n0, C_1065, D_1064, n0)), true), true)=true))). % 47.88/36.15 tff(c_6034, plain, (![E_478, C_480]: (ifeq(equalish(E_478, E_478), true, ifeq(equalish(C_480, C_480), true, f(n1, n0, C_480, n1, E_478, sK1_relation_exists_F(n1, n0, C_480, n1, E_478)), true), true)=true))). % 47.88/36.15 tff(c_40966, plain, (![C_2016]: (ifeq(equalish(C_2016, C_2016), true, f(n0, n0, C_2016, n0, n1, sK1_relation_exists_F(n0, n0, C_2016, n0, n1)), true)=true))). % 47.88/36.15 tff(c_17029, plain, (![D_1048, B_1049]: (ifeq(equalish(D_1048, D_1048), true, ifeq(equalish(B_1049, B_1049), true, f(n0, B_1049, n1, D_1048, n0, sK1_relation_exists_F(n0, B_1049, n1, D_1048, n0)), true), true)=true))). % 47.88/36.15 tff(c_40976, plain, (f(n0, n0, n1, n0, n1, sK1_relation_exists_F(n0, n0, n1, n0, n1))=true)). % 47.88/36.15 tff(c_40975, plain, (f(n0, n0, n0, n0, n1, sK1_relation_exists_F(n0, n0, n0, n0, n1))=true)). % 47.88/36.15 tff(c_16835, plain, (![E_1040, B_1042]: (ifeq(equalish(E_1040, E_1040), true, ifeq(equalish(B_1042, B_1042), true, f(n0, B_1042, n0, n0, E_1040, sK1_relation_exists_F(n0, B_1042, n0, n0, E_1040)), true), true)=true))). % 47.88/36.15 tff(c_5052, plain, (![E_432, A_434]: (ifeq(equalish(E_432, E_432), true, ifeq(equalish(A_434, A_434), true, f(A_434, n1, n1, n0, E_432, sK1_relation_exists_F(A_434, n1, n1, n0, E_432)), true), true)=true))). % 47.88/36.15 tff(c_40263, plain, (![D_2004]: (ifeq(equalish(D_2004, D_2004), true, f(n1, n1, n0, D_2004, n0, sK1_relation_exists_F(n1, n1, n0, D_2004, n0)), true)=true))). % 47.88/36.15 tff(c_15059, plain, (![D_960, C_961]: (ifeq(equalish(D_960, D_960), true, ifeq(equalish(C_961, C_961), true, f(n1, n1, C_961, D_960, n1, sK1_relation_exists_F(n1, n1, C_961, D_960, n1)), true), true)=true))). % 47.88/36.15 tff(c_6678, plain, (![D_513, C_514]: (ifeq(equalish(D_513, D_513), true, ifeq(equalish(C_514, C_514), true, f(n1, n1, C_514, D_513, n0, sK1_relation_exists_F(n1, n1, C_514, D_513, n0)), true), true)=true))). % 47.88/36.15 tff(c_16366, plain, (![E_1020, C_1022]: (ifeq(equalish(E_1020, E_1020), true, ifeq(equalish(C_1022, C_1022), true, f(n0, n0, C_1022, n0, E_1020, sK1_relation_exists_F(n0, n0, C_1022, n0, E_1020)), true), true)=true))). % 47.88/36.15 tff(c_39571, plain, (![D_1992]: (ifeq(equalish(D_1992, D_1992), true, f(n1, n0, n1, D_1992, n0, sK1_relation_exists_F(n1, n0, n1, D_1992, n0)), true)=true))). % 47.88/36.15 tff(c_7600, plain, (![D_561, B_563]: (ifeq(equalish(D_561, D_561), true, ifeq(equalish(B_563, B_563), true, f(n0, B_563, n0, D_561, n0, sK1_relation_exists_F(n0, B_563, n0, D_561, n0)), true), true)=true))). % 47.88/36.15 tff(c_39118, plain, (![B_1984]: (ifeq(equalish(B_1984, B_1984), true, f(n0, B_1984, n0, n1, n0, sK1_relation_exists_F(n0, B_1984, n0, n1, n0)), true)=true))). % 47.88/36.15 tff(c_12674, plain, (![E_865, D_866]: (ifeq(equalish(E_865, E_865), true, ifeq(equalish(D_866, D_866), true, f(n1, n1, n0, D_866, E_865, sK1_relation_exists_F(n1, n1, n0, D_866, E_865)), true), true)=true))). % 47.88/36.15 tff(c_18976, plain, (![D_1154, C_1155]: (ifeq(equalish(D_1154, D_1154), true, ifeq(equalish(C_1155, C_1155), true, f(n0, n1, C_1155, D_1154, n1, sK1_relation_exists_F(n0, n1, C_1155, D_1154, n1)), true), true)=true))). % 47.88/36.15 tff(c_37824, plain, (![C_1940]: (ifeq(equalish(C_1940, C_1940), true, f(n0, n1, C_1940, n0, n1, sK1_relation_exists_F(n0, n1, C_1940, n0, n1)), true)=true))). % 47.88/36.15 tff(c_37847, plain, (f(n0, n1, n1, n0, n1, sK1_relation_exists_F(n0, n1, n1, n0, n1))=true)). % 47.88/36.15 tff(c_17178, plain, (![C_1051, A_1053]: (ifeq(equalish(C_1051, C_1051), true, ifeq(equalish(A_1053, A_1053), true, f(A_1053, n1, C_1051, n0, n0, sK1_relation_exists_F(A_1053, n1, C_1051, n0, n0)), true), true)=true))). % 47.88/36.15 tff(c_15058, plain, (![D_960, B_962]: (ifeq(equalish(D_960, D_960), true, ifeq(equalish(B_962, B_962), true, f(n1, B_962, n1, D_960, n1, sK1_relation_exists_F(n1, B_962, n1, D_960, n1)), true), true)=true))). % 47.88/36.15 tff(c_36167, plain, (![A_1888]: (ifeq(equalish(A_1888, A_1888), true, f(A_1888, n0, n1, n1, n1, sK1_relation_exists_F(A_1888, n0, n1, n1, n1)), true)=true))). % 47.88/36.15 tff(c_7330, plain, (![E_543, A_545]: (ifeq(equalish(E_543, E_543), true, ifeq(equalish(A_545, A_545), true, f(A_545, n0, n0, n1, E_543, sK1_relation_exists_F(A_545, n0, n0, n1, E_543)), true), true)=true))). % 47.88/36.15 tff(c_36186, plain, (f(n1, n0, n1, n1, n1, sK1_relation_exists_F(n1, n0, n1, n1, n1))=true)). % 47.88/36.15 tff(c_6952, plain, (![D_524, A_526]: (ifeq(equalish(D_524, D_524), true, ifeq(equalish(A_526, A_526), true, f(A_526, n0, n1, D_524, n1, sK1_relation_exists_F(A_526, n0, n1, D_524, n1)), true), true)=true))). % 47.88/36.15 tff(c_34796, plain, (![A_1842]: (ifeq(equalish(A_1842, A_1842), true, f(A_1842, n0, n1, n1, n0, sK1_relation_exists_F(A_1842, n0, n1, n1, n0)), true)=true))). % 47.88/36.15 tff(c_4563, plain, (![E_408, D_409]: (ifeq(equalish(E_408, E_408), true, ifeq(equalish(D_409, D_409), true, f(n1, n0, n1, D_409, E_408, sK1_relation_exists_F(n1, n0, n1, D_409, E_408)), true), true)=true))). % 47.88/36.15 tff(c_34815, plain, (f(n1, n0, n1, n1, n0, sK1_relation_exists_F(n1, n0, n1, n1, n0))=true)). % 47.88/36.15 tff(c_17408, plain, (![D_1064, A_1066]: (ifeq(equalish(D_1064, D_1064), true, ifeq(equalish(A_1066, A_1066), true, f(A_1066, n0, n1, D_1064, n0, sK1_relation_exists_F(A_1066, n0, n1, D_1064, n0)), true), true)=true))). % 47.88/36.15 tff(c_15057, plain, (![D_960, C_961]: (ifeq(equalish(D_960, D_960), true, ifeq(equalish(C_961, C_961), true, f(n1, n0, C_961, D_960, n1, sK1_relation_exists_F(n1, n0, C_961, D_960, n1)), true), true)=true))). % 47.88/36.15 tff(c_33874, plain, (![B_1818]: (ifeq(equalish(B_1818, B_1818), true, f(n1, B_1818, n0, n1, n1, sK1_relation_exists_F(n1, B_1818, n0, n1, n1)), true)=true))). % 47.88/36.15 tff(c_20561, plain, (![C_1277, B_1278]: (ifeq(equalish(C_1277, C_1277), true, ifeq(equalish(B_1278, B_1278), true, f(n1, B_1278, C_1277, n1, n0, sK1_relation_exists_F(n1, B_1278, C_1277, n1, n0)), true), true)=true))). % 47.88/36.15 tff(c_15153, plain, (![E_963, A_965]: (ifeq(equalish(E_963, E_963), true, ifeq(equalish(A_965, A_965), true, f(A_965, n0, n0, n0, E_963, sK1_relation_exists_F(A_965, n0, n0, n0, E_963)), true), true)=true))). % 47.88/36.15 tff(c_5597, plain, (![E_459, B_460]: (ifeq(equalish(E_459, E_459), true, ifeq(equalish(B_460, B_460), true, f(n0, B_460, n0, n1, E_459, sK1_relation_exists_F(n0, B_460, n0, n1, E_459)), true), true)=true))). % 47.88/36.15 tff(c_32182, plain, (![C_1762]: (ifeq(equalish(C_1762, C_1762), true, f(n0, n1, C_1762, n1, n0, sK1_relation_exists_F(n0, n1, C_1762, n1, n0)), true)=true))). % 47.88/36.15 tff(c_14757, plain, (![C_943, A_945]: (ifeq(equalish(C_943, C_943), true, ifeq(equalish(A_945, A_945), true, f(A_945, n1, C_943, n0, n1, sK1_relation_exists_F(A_945, n1, C_943, n0, n1)), true), true)=true))). % 47.88/36.15 tff(c_32194, plain, (f(n0, n1, n1, n1, n0, sK1_relation_exists_F(n0, n1, n1, n1, n0))=true)). % 47.88/36.15 tff(c_8684, plain, (![E_632, C_633]: (ifeq(equalish(E_632, E_632), true, ifeq(equalish(C_633, C_633), true, f(n0, n1, C_633, n1, E_632, sK1_relation_exists_F(n0, n1, C_633, n1, E_632)), true), true)=true))). % 47.88/36.15 tff(c_30920, plain, (![D_1720]: (ifeq(equalish(D_1720, D_1720), true, f(n1, n0, n0, D_1720, n1, sK1_relation_exists_F(n1, n0, n0, D_1720, n1)), true)=true))). % 47.88/36.15 tff(c_4321, plain, (![E_393, B_394]: (ifeq(equalish(E_393, E_393), true, ifeq(equalish(B_394, B_394), true, f(n1, B_394, n1, n1, E_393, sK1_relation_exists_F(n1, B_394, n1, n1, E_393)), true), true)=true))). % 47.88/36.15 tff(c_30943, plain, (f(n1, n0, n0, n1, n1, sK1_relation_exists_F(n1, n0, n0, n1, n1))=true)). % 47.88/36.15 tff(c_6400, plain, (![D_497, B_498]: (ifeq(equalish(D_497, D_497), true, ifeq(equalish(B_498, B_498), true, f(n0, B_498, n0, D_497, n1, sK1_relation_exists_F(n0, B_498, n0, D_497, n1)), true), true)=true))). % 47.88/36.15 tff(c_4394, plain, (![C_396, B_397]: (ifeq(equalish(C_396, C_396), true, ifeq(equalish(B_397, B_397), true, f(n1, B_397, C_396, n1, n1, sK1_relation_exists_F(n1, B_397, C_396, n1, n1)), true), true)=true))). % 47.88/36.15 tff(c_28953, plain, (![A_1648]: (ifeq(equalish(A_1648, A_1648), true, f(A_1648, n1, n0, n1, n0, sK1_relation_exists_F(A_1648, n1, n0, n1, n0)), true)=true))). % 47.88/36.15 tff(c_708, plain, (![E_221, C_222]: (ifeq(equalish(E_221, E_221), true, ifeq(equalish(C_222, C_222), true, f(n0, n1, C_222, n0, E_221, sK1_relation_exists_F(n0, n1, C_222, n0, E_221)), true), true)=true))). % 47.88/36.15 tff(c_28963, plain, (f(n1, n1, n0, n1, n0, sK1_relation_exists_F(n1, n1, n0, n1, n0))=true)). % 47.88/36.15 tff(c_28962, plain, (f(n0, n1, n0, n1, n0, sK1_relation_exists_F(n0, n1, n0, n1, n0))=true)). % 47.88/36.15 tff(c_6676, plain, (![D_513, C_514]: (ifeq(equalish(D_513, D_513), true, ifeq(equalish(C_514, C_514), true, f(n1, n0, C_514, D_513, n0, sK1_relation_exists_F(n1, n0, C_514, D_513, n0)), true), true)=true))). % 47.88/36.15 tff(c_5950, plain, (![E_475, A_477]: (ifeq(equalish(E_475, E_475), true, ifeq(equalish(A_477, A_477), true, f(A_477, n1, n1, n1, E_475, sK1_relation_exists_F(A_477, n1, n1, n1, E_475)), true), true)=true))). % 47.88/36.15 tff(c_27042, plain, (![A_1580]: (ifeq(equalish(A_1580, A_1580), true, f(A_1580, n1, n0, n1, n1, sK1_relation_exists_F(A_1580, n1, n0, n1, n1)), true)=true))). % 47.88/36.15 tff(c_6033, plain, (![E_478, D_479]: (ifeq(equalish(E_478, E_478), true, ifeq(equalish(D_479, D_479), true, f(n1, n0, n0, D_479, E_478, sK1_relation_exists_F(n1, n0, n0, D_479, E_478)), true), true)=true))). % 47.88/36.15 tff(c_27052, plain, (f(n1, n1, n0, n1, n1, sK1_relation_exists_F(n1, n1, n0, n1, n1))=true)). % 47.88/36.15 tff(c_27051, plain, (f(n0, n1, n0, n1, n1, sK1_relation_exists_F(n0, n1, n0, n1, n1))=true)). % 47.88/36.15 tff(c_5598, plain, (![E_459, A_461]: (ifeq(equalish(E_459, E_459), true, ifeq(equalish(A_461, A_461), true, f(A_461, n1, n0, n1, E_459, sK1_relation_exists_F(A_461, n1, n0, n1, E_459)), true), true)=true))). % 47.88/36.15 tff(c_26846, plain, (![A_1570, D_1571, C_1572, E_1568, B_1569]: (ifeq(f(A_1570, B_1569, C_1572, D_1571, E_1568, sK1_relation_exists_F(n0, n0, n1, n1, n0)), true, equalish(B_1569, n0), true)=true))). % 47.88/36.15 tff(c_4170, plain, (![D_384, C_385, B_386, A_387]: (ifeq(equalish(D_384, D_384), true, ifeq(equalish(C_385, C_385), true, ifeq(equalish(B_386, B_386), true, ifeq(equalish(A_387, A_387), true, f(A_387, B_386, C_385, D_384, n1, sK1_relation_exists_F(A_387, B_386, C_385, D_384, n1)), true), true), true), true)=true))). % 47.88/36.15 tff(c_4029, plain, (![D_375, C_376, B_377, A_378]: (ifeq(equalish(D_375, D_375), true, ifeq(equalish(C_376, C_376), true, ifeq(equalish(B_377, B_377), true, ifeq(equalish(A_378, A_378), true, f(A_378, B_377, C_376, D_375, n0, sK1_relation_exists_F(A_378, B_377, C_376, D_375, n0)), true), true), true), true)=true))). % 47.88/36.15 tff(c_26175, plain, (![C_1547, B_1548, A_1549, E_1546, D_1550]: (ifeq(f(A_1549, B_1548, C_1547, D_1550, E_1546, sK1_relation_exists_F(n0, n0, n1, n1, n0)), true, equalish(E_1546, n0), true)=true))). % 47.88/36.15 tff(c_25789, plain, (![E_1527, D_1528, A_1524, B_1525, C_1526]: (ifeq(f(A_1524, B_1525, C_1526, D_1528, E_1527, sK1_relation_exists_F(n0, n0, n1, n1, n1)), true, equalish(C_1526, n1), true)=true))). % 47.88/36.15 tff(c_25060, plain, (![A_1486, B_1488, D_1489, E_1490, C_1487]: (ifeq(f(A_1486, B_1488, C_1487, D_1489, E_1490, sK1_relation_exists_F(n0, n0, n1, n1, n0)), true, equalish(D_1489, n1), true)=true))). % 47.88/36.15 tff(c_24762, plain, (![D_1466, B_1464, C_1468, E_1467, A_1465]: (ifeq(f(A_1465, B_1464, C_1468, D_1466, E_1467, sK1_relation_exists_F(n0, n0, n1, n1, n1)), true, equalish(A_1465, n0), true)=true))). % 47.88/36.15 tff(c_23587, plain, (![C_1418]: (ifeq(equalish(C_1418, C_1418), true, f(n0, n0, C_1418, n1, n0, sK1_relation_exists_F(n0, n0, C_1418, n1, n0)), true)=true))). % 47.88/36.15 tff(c_23610, plain, (f(n0, n0, n1, n1, n0, sK1_relation_exists_F(n0, n0, n1, n1, n0))=true)). % 47.88/36.15 tff(c_22215, plain, (![C_1356]: (ifeq(equalish(C_1356, C_1356), true, f(n0, n0, C_1356, n1, n1, sK1_relation_exists_F(n0, n0, C_1356, n1, n1)), true)=true))). % 47.88/36.15 tff(c_22226, plain, (f(n0, n0, n1, n1, n1, sK1_relation_exists_F(n0, n0, n1, n1, n1))=true)). % 47.88/36.15 tff(c_22046, plain, (f(n0, n0, n0, n1, n1, sK1_relation_exists_F(n0, n0, n0, n1, n1))=true)). % 47.88/36.15 tff(c_21886, plain, (f(n0, n0, n0, n1, n0, sK1_relation_exists_F(n0, n0, n0, n1, n0))=true)). % 47.88/36.15 tff(c_21783, plain, (![E_1353]: (ifeq(equalish(E_1353, E_1353), true, f(n0, n0, n0, n1, E_1353, sK1_relation_exists_F(n0, n0, n0, n1, E_1353)), true)=true))). % 47.88/36.15 tff(c_16368, plain, (![E_1020, C_1022]: (ifeq(equalish(E_1020, E_1020), true, ifeq(equalish(C_1022, C_1022), true, f(n0, n0, C_1022, n1, E_1020, sK1_relation_exists_F(n0, n0, C_1022, n1, E_1020)), true), true)=true))). % 47.88/36.15 tff(c_21542, plain, (![B_1344, C_1347, A_1345, E_1343, D_1346]: (ifeq(f(A_1345, B_1344, C_1347, D_1346, E_1343, sK1_relation_exists_F(n1, n0, n0, n0, n1)), true, equalish(B_1344, n0), true)=true))). % 47.88/36.15 tff(c_4095, plain, (![D_375, B_377, A_378]: (ifeq(equalish(D_375, D_375), true, ifeq(equalish(B_377, B_377), true, ifeq(equalish(A_378, A_378), true, f(A_378, B_377, n0, D_375, n0, sK1_relation_exists_F(A_378, B_377, n0, D_375, n0)), true), true), true)=true))). % 47.88/36.15 tff(c_21268, plain, (![D_1332, B_1330, A_1331, E_1333, C_1334]: (ifeq(f(A_1331, B_1330, C_1334, D_1332, E_1333, sK1_relation_exists_F(n1, n0, n0, n0, n0)), true, equalish(A_1331, n1), true)=true))). % 47.88/36.15 tff(c_21133, plain, (![D_1324, C_1322, A_1320, E_1323, B_1321]: (ifeq(f(A_1320, B_1321, C_1322, D_1324, E_1323, sK1_relation_exists_F(n1, n0, n0, n0, n1)), true, equalish(C_1322, n0), true)=true))). % 47.88/36.15 tff(c_21010, plain, (![E_1314, B_1312, D_1313, C_1311, A_1310]: (ifeq(f(A_1310, B_1312, C_1311, D_1313, E_1314, sK1_relation_exists_F(n1, n0, n0, n0, n1)), true, equalish(D_1313, n0), true)=true))). % 47.88/36.15 tff(c_20850, plain, (![B_1301, D_1303, E_1300, C_1304, A_1302]: (ifeq(f(A_1302, B_1301, C_1304, D_1303, E_1300, sK1_relation_exists_F(n1, n0, n0, n0, n0)), true, equalish(B_1301, n0), true)=true))). % 47.88/36.15 tff(c_20715, plain, (![C_1294, A_1291, E_1293, D_1292, B_1290]: (ifeq(f(A_1291, B_1290, C_1294, D_1292, E_1293, sK1_relation_exists_F(n1, n0, n0, n0, n1)), true, equalish(A_1291, n1), true)=true))). % 47.88/36.15 tff(c_20568, plain, (![D_1284, E_1280, A_1283, B_1282, C_1281]: (ifeq(f(A_1283, B_1282, C_1281, D_1284, E_1280, sK1_relation_exists_F(n1, n0, n0, n0, n0)), true, equalish(E_1280, n0), true)=true))). % 47.88/36.15 tff(c_4098, plain, (![C_376, B_377, A_378]: (ifeq(equalish(C_376, C_376), true, ifeq(equalish(B_377, B_377), true, ifeq(equalish(A_378, A_378), true, f(A_378, B_377, C_376, n1, n0, sK1_relation_exists_F(A_378, B_377, C_376, n1, n0)), true), true), true)=true))). % 47.88/36.15 tff(c_20305, plain, (![C_1269, B_1268, A_1267, E_1270, D_1271]: (ifeq(f(A_1267, B_1268, C_1269, D_1271, E_1270, sK1_relation_exists_F(n1, n0, n0, n0, n0)), true, equalish(C_1269, n0), true)=true))). % 47.88/36.15 tff(c_20182, plain, (![C_1258, B_1259, A_1257, D_1260, E_1261]: (ifeq(f(A_1257, B_1259, C_1258, D_1260, E_1261, sK1_relation_exists_F(n1, n0, n0, n0, n0)), true, equalish(D_1260, n0), true)=true))). % 47.88/36.15 tff(c_20059, plain, (![B_1249, E_1247, D_1251, C_1248, A_1250]: (ifeq(f(A_1250, B_1249, C_1248, D_1251, E_1247, sK1_relation_exists_F(n1, n0, n0, n0, n1)), true, equalish(E_1247, n1), true)=true))). % 47.88/36.15 tff(c_19919, plain, (![B_1238, A_1239, E_1237, D_1240, C_1241]: (ifeq(f(A_1239, B_1238, C_1241, D_1240, E_1237, sK1_relation_exists_F(n1, n0, n1, n0, n1)), true, equalish(B_1238, n0), true)=true))). % 47.88/36.15 tff(c_19765, plain, (![D_1231, C_1228, A_1230, B_1229, E_1227]: (ifeq(f(A_1230, B_1229, C_1228, D_1231, E_1227, sK1_relation_exists_F(n1, n0, n1, n0, n1)), true, equalish(E_1227, n1), true)=true))). % 47.88/36.15 tff(c_19635, plain, (![A_1217, B_1219, E_1221, D_1220, C_1218]: (ifeq(f(A_1217, B_1219, C_1218, D_1220, E_1221, sK1_relation_exists_F(n1, n0, n1, n0, n1)), true, equalish(D_1220, n0), true)=true))). % 47.88/36.15 tff(c_19391, plain, (![E_1200, B_1197, A_1198, C_1201, D_1199]: (ifeq(f(A_1198, B_1197, C_1201, D_1199, E_1200, sK1_relation_exists_F(n1, n0, n1, n0, n0)), true, equalish(A_1198, n1), true)=true))). % 47.88/36.15 tff(c_11706, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n1, n0, n0, n0, n1)), true, equalish(n0, I_23), true)=true))). % 47.88/36.15 tff(c_11704, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n1, n0, n0, n0, n1)), true, equalish(n1, J_11), true)=true))). % 47.88/36.15 tff(c_11567, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n1, n0, n0, n0, n0)), true, equalish(n0, I_23), true)=true))). % 47.88/36.15 tff(c_11561, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n1, n0, n0, n0, n0)), true, equalish(n0, H_31), true)=true))). % 47.88/36.15 tff(c_11559, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n1, n0, n0, n0, n0)), true, equalish(n1, F_57), true)=true))). % 47.88/36.15 tff(c_11563, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n1, n0, n0, n0, n0)), true, equalish(n0, G_47), true)=true))). % 47.88/36.15 tff(c_11702, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n1, n0, n0, n0, n1)), true, equalish(n0, G_47), true)=true))). % 47.88/36.15 tff(c_11698, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n1, n0, n0, n0, n1)), true, equalish(n1, F_57), true)=true))). % 47.88/36.15 tff(c_18986, plain, (![J_55, H_1158, H_53, I_56, G_58]: (ifeq(f(H_1158, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n1, n0, n0, n0, n1)), true, true, true)=true))). % 47.88/36.15 tff(c_11700, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n1, n0, n0, n0, n1)), true, equalish(n0, H_31), true)=true))). % 47.88/36.15 tff(c_4212, plain, (![D_384, C_385, A_387]: (ifeq(equalish(D_384, D_384), true, ifeq(equalish(C_385, C_385), true, ifeq(equalish(A_387, A_387), true, f(A_387, n1, C_385, D_384, n1, sK1_relation_exists_F(A_387, n1, C_385, D_384, n1)), true), true), true)=true))). % 47.88/36.15 tff(c_18730, plain, (![J_55, H_53, I_56, G_58, J_1147]: (ifeq(f(J_1147, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n1, n0, n0, n0, n0)), true, true, true)=true))). % 47.88/36.15 tff(c_11565, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n1, n0, n0, n0, n0)), true, equalish(n0, J_11), true)=true))). % 47.88/36.15 tff(c_13667, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n1, n0, n1, n0, n1)), true, equalish(n1, H_31), true)=true))). % 47.88/36.16 tff(c_13673, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n1, n0, n1, n0, n1)), true, equalish(n0, I_23), true)=true))). % 47.88/36.16 tff(c_13669, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n1, n0, n1, n0, n1)), true, equalish(n0, G_47), true)=true))). % 47.88/36.16 tff(c_12266, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n1, n0, n1, n0, n0)), true, equalish(n1, F_57), true)=true))). % 47.88/36.16 tff(c_2826, plain, (![E_321, D_322, C_323]: (ifeq(equalish(E_321, E_321), true, ifeq(equalish(D_322, D_322), true, ifeq(equalish(C_323, C_323), true, f(n1, n1, C_323, D_322, E_321, sK1_relation_exists_F(n1, n1, C_323, D_322, E_321)), true), true), true)=true))). % 47.88/36.16 tff(c_12270, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n1, n0, n1, n0, n0)), true, equalish(n0, G_47), true)=true))). % 47.88/36.16 tff(c_12274, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n1, n0, n1, n0, n0)), true, equalish(n0, I_23), true)=true))). % 47.88/36.16 tff(c_12272, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n1, n0, n1, n0, n0)), true, equalish(n0, J_11), true)=true))). % 47.88/36.16 tff(c_17952, plain, (![J_55, H_53, I_56, G_58, H_1097]: (ifeq(f(H_1097, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n1, n0, n1, n0, n0)), true, true, true)=true))). % 47.88/36.16 tff(c_12268, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n1, n0, n1, n0, n0)), true, equalish(n1, H_31), true)=true))). % 47.88/36.16 tff(c_13671, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n1, n0, n1, n0, n1)), true, equalish(n1, J_11), true)=true))). % 47.88/36.16 tff(c_1200, plain, (![E_239, D_240, B_242]: (ifeq(equalish(E_239, E_239), true, ifeq(equalish(D_240, D_240), true, ifeq(equalish(B_242, B_242), true, f(n0, B_242, n0, D_240, E_239, sK1_relation_exists_F(n0, B_242, n0, D_240, E_239)), true), true), true)=true))). % 47.88/36.16 tff(c_17625, plain, (![J_33, F_1081, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, F_1081, I_34, J_33, sK1_relation_exists_F(n1, n0, n1, n0, n1)), true, true, true)=true))). % 47.88/36.16 tff(c_13665, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n1, n0, n1, n0, n1)), true, equalish(n1, F_57), true)=true))). % 47.88/36.16 tff(c_17436, plain, (![C_1069, D_1071, B_1068, A_1067, E_1070]: (ifeq(f(A_1067, B_1068, C_1069, D_1071, E_1070, sK1_relation_exists_F(n1, n0, n1, n0, n0)), true, equalish(C_1069, n1), true)=true))). % 47.88/36.16 tff(c_11249, plain, (![E_814]: (ifeq(equalish(E_814, E_814), true, f(n1, n0, n1, n0, E_814, sK1_relation_exists_F(n1, n0, n1, n0, E_814)), true)=true))). % 47.88/36.16 tff(c_4096, plain, (![D_375, C_376, A_378]: (ifeq(equalish(D_375, D_375), true, ifeq(equalish(C_376, C_376), true, ifeq(equalish(A_378, A_378), true, f(A_378, n0, C_376, D_375, n0, sK1_relation_exists_F(A_378, n0, C_376, D_375, n0)), true), true), true)=true))). % 47.88/36.16 tff(c_17202, plain, (![C_1058, A_1056, E_1054, D_1057, B_1055]: (ifeq(f(A_1056, B_1055, C_1058, D_1057, E_1054, sK1_relation_exists_F(n1, n0, n1, n0, n0)), true, equalish(B_1055, n0), true)=true))). % 47.88/36.16 tff(c_4094, plain, (![C_376, B_377, A_378]: (ifeq(equalish(C_376, C_376), true, ifeq(equalish(B_377, B_377), true, ifeq(equalish(A_378, A_378), true, f(A_378, B_377, C_376, n0, n0, sK1_relation_exists_F(A_378, B_377, C_376, n0, n0)), true), true), true)=true))). % 47.88/36.16 tff(c_4099, plain, (![D_375, B_377, A_378]: (ifeq(equalish(D_375, D_375), true, ifeq(equalish(B_377, B_377), true, ifeq(equalish(A_378, A_378), true, f(A_378, B_377, n1, D_375, n0, sK1_relation_exists_F(A_378, B_377, n1, D_375, n0)), true), true), true)=true))). % 47.88/36.16 tff(c_16702, plain, (![D_1039, A_1035, E_1038, C_1037, B_1036]: (ifeq(f(A_1035, B_1036, C_1037, D_1039, E_1038, sK1_relation_exists_F(n1, n0, n1, n0, n1)), true, equalish(C_1037, n1), true)=true))). % 47.88/36.16 tff(c_3897, plain, (![E_367, C_368, B_369]: (ifeq(equalish(E_367, E_367), true, ifeq(equalish(C_368, C_368), true, ifeq(equalish(B_369, B_369), true, f(n0, B_369, C_368, n0, E_367, sK1_relation_exists_F(n0, B_369, C_368, n0, E_367)), true), true), true)=true))). % 47.88/36.16 tff(c_3895, plain, (![E_367, B_369, A_370]: (ifeq(equalish(E_367, E_367), true, ifeq(equalish(B_369, B_369), true, ifeq(equalish(A_370, A_370), true, f(A_370, B_369, n0, n0, E_367, sK1_relation_exists_F(A_370, B_369, n0, n0, E_367)), true), true), true)=true))). % 47.88/36.16 tff(c_16072, plain, (![C_1008, E_1007, A_1010, D_1011, B_1009]: (ifeq(f(A_1010, B_1009, C_1008, D_1011, E_1007, sK1_relation_exists_F(n1, n0, n1, n0, n0)), true, equalish(E_1007, n0), true)=true))). % 47.88/36.16 tff(c_1201, plain, (![E_239, D_240, C_241]: (ifeq(equalish(E_239, E_239), true, ifeq(equalish(D_240, D_240), true, ifeq(equalish(C_241, C_241), true, f(n0, n0, C_241, D_240, E_239, sK1_relation_exists_F(n0, n0, C_241, D_240, E_239)), true), true), true)=true))). % 47.88/36.16 tff(c_3281, plain, (![E_342, D_343, A_345]: (ifeq(equalish(E_342, E_342), true, ifeq(equalish(D_343, D_343), true, ifeq(equalish(A_345, A_345), true, f(A_345, n1, n0, D_343, E_342, sK1_relation_exists_F(A_345, n1, n0, D_343, E_342)), true), true), true)=true))). % 47.88/36.16 tff(c_15173, plain, (![C_967, E_970, A_966, D_969, B_968]: (ifeq(f(A_966, B_968, C_967, D_969, E_970, sK1_relation_exists_F(n1, n0, n1, n0, n0)), true, equalish(D_969, n0), true)=true))). % 47.88/36.16 tff(c_3278, plain, (![E_342, D_343, A_345]: (ifeq(equalish(E_342, E_342), true, ifeq(equalish(D_343, D_343), true, ifeq(equalish(A_345, A_345), true, f(A_345, n0, n0, D_343, E_342, sK1_relation_exists_F(A_345, n0, n0, D_343, E_342)), true), true), true)=true))). % 47.88/36.16 tff(c_4213, plain, (![D_384, C_385, B_386]: (ifeq(equalish(D_384, D_384), true, ifeq(equalish(C_385, C_385), true, ifeq(equalish(B_386, B_386), true, f(n1, B_386, C_385, D_384, n1, sK1_relation_exists_F(n1, B_386, C_385, D_384, n1)), true), true), true)=true))). % 47.88/36.16 tff(c_14767, plain, (![A_947, E_949, B_946, C_950, D_948]: (ifeq(f(A_947, B_946, C_950, D_948, E_949, sK1_relation_exists_F(n1, n0, n1, n0, n1)), true, equalish(A_947, n1), true)=true))). % 47.88/36.16 tff(c_4206, plain, (![C_385, B_386, A_387]: (ifeq(equalish(C_385, C_385), true, ifeq(equalish(B_386, B_386), true, ifeq(equalish(A_387, A_387), true, f(A_387, B_386, C_385, n0, n1, sK1_relation_exists_F(A_387, B_386, C_385, n0, n1)), true), true), true)=true))). % 47.88/36.16 tff(c_13525, plain, (![C_901]: (ifeq(equalish(C_901, C_901), true, f(n1, n0, C_901, n0, n1, sK1_relation_exists_F(n1, n0, C_901, n0, n1)), true)=true))). % 47.88/36.16 tff(c_13536, plain, (f(n1, n0, n1, n0, n1, sK1_relation_exists_F(n1, n0, n1, n0, n1))=true)). % 47.88/36.16 tff(c_12129, plain, (![C_848]: (ifeq(equalish(C_848, C_848), true, f(n1, n0, C_848, n0, n0, sK1_relation_exists_F(n1, n0, C_848, n0, n0)), true)=true))). % 47.88/36.16 tff(c_3282, plain, (![E_342, D_343, B_344]: (ifeq(equalish(E_342, E_342), true, ifeq(equalish(D_343, D_343), true, ifeq(equalish(B_344, B_344), true, f(n1, B_344, n0, D_343, E_342, sK1_relation_exists_F(n1, B_344, n0, D_343, E_342)), true), true), true)=true))). % 47.88/36.16 tff(c_12141, plain, (f(n1, n0, n1, n0, n0, sK1_relation_exists_F(n1, n0, n1, n0, n0))=true)). % 47.88/36.16 tff(c_11573, plain, (f(n1, n0, n0, n0, n1, sK1_relation_exists_F(n1, n0, n0, n0, n1))=true)). % 47.88/36.16 tff(c_11331, plain, (f(n1, n0, n0, n0, n0, sK1_relation_exists_F(n1, n0, n0, n0, n0))=true)). % 47.88/36.16 tff(c_801, plain, (![E_226, D_227, B_228]: (ifeq(equalish(E_226, E_226), true, ifeq(equalish(D_227, D_227), true, ifeq(equalish(B_228, B_228), true, f(n1, B_228, n1, D_227, E_226, sK1_relation_exists_F(n1, B_228, n1, D_227, E_226)), true), true), true)=true))). % 47.88/36.16 tff(c_11248, plain, (![E_814]: (ifeq(equalish(E_814, E_814), true, f(n1, n0, n0, n0, E_814, sK1_relation_exists_F(n1, n0, n0, n0, E_814)), true)=true))). % 47.88/36.16 tff(c_10881, plain, (![E_791, C_792]: (ifeq(equalish(E_791, E_791), true, ifeq(equalish(C_792, C_792), true, f(n1, n0, C_792, n0, E_791, sK1_relation_exists_F(n1, n0, C_792, n0, E_791)), true), true)=true))). % 47.88/36.16 tff(c_11046, plain, (![A_806, E_804, D_807, B_805, C_808]: (ifeq(f(A_806, B_805, C_808, D_807, E_804, sK1_relation_exists_F(n0, n1, n0, n0, n0)), true, equalish(B_805, n1), true)=true))). % 47.88/36.16 tff(c_10887, plain, (![D_798, A_794, C_796, B_795, E_797]: (ifeq(f(A_794, B_795, C_796, D_798, E_797, sK1_relation_exists_F(n0, n1, n0, n0, n0)), true, equalish(C_796, n0), true)=true))). % 47.88/36.16 tff(c_3896, plain, (![E_367, C_368, A_370]: (ifeq(equalish(E_367, E_367), true, ifeq(equalish(C_368, C_368), true, ifeq(equalish(A_370, A_370), true, f(A_370, n0, C_368, n0, E_367, sK1_relation_exists_F(A_370, n0, C_368, n0, E_367)), true), true), true)=true))). % 47.88/36.16 tff(c_10673, plain, (![B_783, C_782, D_785, E_781, A_784]: (ifeq(f(A_784, B_783, C_782, D_785, E_781, sK1_relation_exists_F(n0, n1, n0, n0, n0)), true, equalish(E_781, n0), true)=true))). % 47.88/36.16 tff(c_10538, plain, (![A_771, D_774, E_775, B_773, C_772]: (ifeq(f(A_771, B_773, C_772, D_774, E_775, sK1_relation_exists_F(n0, n1, n0, n0, n0)), true, equalish(D_774, n0), true)=true))). % 47.88/36.16 tff(c_10391, plain, (![C_763, E_764, B_762, A_761, D_765]: (ifeq(f(A_761, B_762, C_763, D_765, E_764, sK1_relation_exists_F(n0, n1, n0, n0, n1)), true, equalish(C_763, n0), true)=true))). % 47.88/36.16 tff(c_10255, plain, (![E_755, C_752, A_751, D_754, B_753]: (ifeq(f(A_751, B_753, C_752, D_754, E_755, sK1_relation_exists_F(n0, n1, n0, n0, n1)), true, equalish(D_754, n0), true)=true))). % 47.88/36.16 tff(c_10132, plain, (![C_745, E_744, B_741, A_742, D_743]: (ifeq(f(A_742, B_741, C_745, D_743, E_744, sK1_relation_exists_F(n0, n1, n0, n0, n1)), true, equalish(A_742, n0), true)=true))). % 47.88/36.16 tff(c_10009, plain, (![C_735, E_734, D_733, A_732, B_731]: (ifeq(f(A_732, B_731, C_735, D_733, E_734, sK1_relation_exists_F(n0, n1, n0, n0, n0)), true, equalish(A_732, n0), true)=true))). % 47.88/36.16 tff(c_9873, plain, (![B_723, C_722, A_724, E_721, D_725]: (ifeq(f(A_724, B_723, C_722, D_725, E_721, sK1_relation_exists_F(n0, n1, n0, n0, n1)), true, equalish(E_721, n1), true)=true))). % 47.88/36.16 tff(c_9750, plain, (![B_712, C_715, D_714, A_713, E_711]: (ifeq(f(A_713, B_712, C_715, D_714, E_711, sK1_relation_exists_F(n0, n1, n0, n0, n1)), true, equalish(B_712, n1), true)=true))). % 47.88/36.16 tff(c_9608, plain, (![C_705, E_701, D_704, B_702, A_703]: (ifeq(f(A_703, B_702, C_705, D_704, E_701, sK1_relation_exists_F(n1, n1, n0, n0, n0)), true, equalish(B_702, n1), true)=true))). % 47.88/36.16 tff(c_9466, plain, (![A_691, D_695, B_692, E_694, C_693]: (ifeq(f(A_691, B_692, C_693, D_695, E_694, sK1_relation_exists_F(n1, n1, n0, n0, n1)), true, equalish(C_693, n0), true)=true))). % 47.88/36.16 tff(c_4100, plain, (![D_375, C_376, A_378]: (ifeq(equalish(D_375, D_375), true, ifeq(equalish(C_376, C_376), true, ifeq(equalish(A_378, A_378), true, f(A_378, n1, C_376, D_375, n0, sK1_relation_exists_F(A_378, n1, C_376, D_375, n0)), true), true), true)=true))). % 47.88/36.16 tff(c_9193, plain, (![A_680, E_678, D_681, C_682, B_679]: (ifeq(f(A_680, B_679, C_682, D_681, E_678, sK1_relation_exists_F(n1, n1, n0, n0, n1)), true, equalish(B_679, n1), true)=true))). % 47.88/36.16 tff(c_931, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n0, n1, n0, n0, n0)), true, equalish(n0, F_57), true)=true))). % 47.88/36.16 tff(c_2824, plain, (![E_321, C_323, B_324]: (ifeq(equalish(E_321, E_321), true, ifeq(equalish(C_323, C_323), true, ifeq(equalish(B_324, B_324), true, f(n1, B_324, C_323, n1, E_321, sK1_relation_exists_F(n1, B_324, C_323, n1, E_321)), true), true), true)=true))). % 47.88/36.16 tff(c_1044, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n0, n1, n0, n0, n1)), true, equalish(n1, J_11), true)=true))). % 47.88/36.16 tff(c_937, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n0, n1, n0, n0, n0)), true, equalish(n0, J_11), true)=true))). % 47.88/36.16 tff(c_935, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n0, n1, n0, n0, n0)), true, equalish(n1, G_47), true)=true))). % 47.88/36.16 tff(c_1038, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n0, n1, n0, n0, n1)), true, equalish(n0, F_57), true)=true))). % 47.88/36.16 tff(c_933, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n0, n1, n0, n0, n0)), true, equalish(n0, H_31), true)=true))). % 47.88/36.16 tff(c_1046, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n0, n1, n0, n0, n1)), true, equalish(n0, I_23), true)=true))). % 47.88/36.16 tff(c_1040, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n0, n1, n0, n0, n1)), true, equalish(n0, H_31), true)=true))). % 47.88/36.16 tff(c_2276, plain, (![E_293, C_294, B_295]: (ifeq(equalish(E_293, E_293), true, ifeq(equalish(C_294, C_294), true, ifeq(equalish(B_295, B_295), true, f(n0, B_295, C_294, n1, E_293, sK1_relation_exists_F(n0, B_295, C_294, n1, E_293)), true), true), true)=true))). % 47.88/36.16 tff(c_8460, plain, (![J_55, H_53, I_56, G_58, I_622]: (ifeq(f(I_622, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n0, n1, n0, n0, n0)), true, true, true)=true))). % 47.88/36.16 tff(c_939, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n0, n1, n0, n0, n0)), true, equalish(n0, I_23), true)=true))). % 47.88/36.16 tff(c_7851, plain, (![E_583, D_582, C_580, A_579, B_581]: (ifeq(f(A_579, B_581, C_580, D_582, E_583, sK1_relation_exists_F(n1, n1, n0, n0, n0)), true, equalish(D_582, n0), true)=true))). % 47.88/36.16 tff(c_8163, plain, (![J_55, H_53, I_56, G_58, G_608]: (ifeq(f(G_608, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n0, n1, n0, n0, n1)), true, true, true)=true))). % 47.88/36.16 tff(c_670, plain, (![E_217, D_218, A_220]: (ifeq(equalish(E_217, E_217), true, ifeq(equalish(D_218, D_218), true, ifeq(equalish(A_220, A_220), true, f(A_220, n1, n1, D_218, E_217, sK1_relation_exists_F(A_220, n1, n1, D_218, E_217)), true), true), true)=true))). % 47.88/36.16 tff(c_1042, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n0, n1, n0, n0, n1)), true, equalish(n1, G_47), true)=true))). % 47.88/36.16 tff(c_1541, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n1, n1, n0, n0, n1)), true, equalish(n0, I_23), true)=true))). % 47.88/36.16 tff(c_2951, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n1, n1, n0, n0, n0)), true, equalish(n1, G_47), true)=true))). % 47.88/36.16 tff(c_1535, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n1, n1, n0, n0, n1)), true, equalish(n0, H_31), true)=true))). % 47.88/36.16 tff(c_1533, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n1, n1, n0, n0, n1)), true, equalish(n1, F_57), true)=true))). % 47.88/36.16 tff(c_2955, plain, (![H_20, J_22, F_24, I_23, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, sK1_relation_exists_F(n1, n1, n0, n0, n0)), true, equalish(n0, I_23), true)=true))). % 47.88/36.16 tff(c_2947, plain, (![F_57, J_55, H_53, I_56, G_58]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n1, n1, n0, n0, n0)), true, equalish(n1, F_57), true)=true))). % 47.88/36.16 tff(c_2949, plain, (![H_31, J_33, G_36, F_35, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, sK1_relation_exists_F(n1, n1, n0, n0, n0)), true, equalish(n0, H_31), true)=true))). % 47.88/36.16 tff(c_4097, plain, (![D_375, C_376, B_377]: (ifeq(equalish(D_375, D_375), true, ifeq(equalish(C_376, C_376), true, ifeq(equalish(B_377, B_377), true, f(n0, B_377, C_376, D_375, n0, sK1_relation_exists_F(n0, B_377, C_376, D_375, n0)), true), true), true)=true))). % 47.88/36.16 tff(c_7424, plain, (![J_554, J_55, H_53, I_56, G_58]: (ifeq(f(J_554, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n1, n1, n0, n0, n0)), true, true, true)=true))). % 47.88/36.16 tff(c_2953, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n1, n1, n0, n0, n0)), true, equalish(n0, J_11), true)=true))). % 47.88/36.16 tff(c_1539, plain, (![J_11, H_9, F_13, I_12, G_14]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, sK1_relation_exists_F(n1, n1, n0, n0, n1)), true, equalish(n1, J_11), true)=true))). % 47.88/36.16 tff(c_2275, plain, (![E_293, C_294, A_296]: (ifeq(equalish(E_293, E_293), true, ifeq(equalish(C_294, C_294), true, ifeq(equalish(A_296, A_296), true, f(A_296, n0, C_294, n1, E_293, sK1_relation_exists_F(A_296, n0, C_294, n1, E_293)), true), true), true)=true))). % 47.88/36.16 tff(c_7103, plain, (![G_537, J_55, H_53, I_56, G_58]: (ifeq(f(G_537, G_58, H_53, I_56, J_55, sK1_relation_exists_F(n1, n1, n0, n0, n1)), true, true, true)=true))). % 47.88/36.16 tff(c_1537, plain, (![F_46, J_44, H_42, G_47, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, sK1_relation_exists_F(n1, n1, n0, n0, n1)), true, equalish(n1, G_47), true)=true))). % 47.88/36.16 tff(c_746, plain, (![E_224]: (ifeq(equalish(E_224, E_224), true, f(n1, n1, n0, n0, E_224, sK1_relation_exists_F(n1, n1, n0, n0, E_224)), true)=true))). % 47.88/36.16 tff(c_6823, plain, (![C_521, E_522, A_519, B_520, D_523]: (ifeq(f(A_519, B_520, C_521, D_523, E_522, sK1_relation_exists_F(n1, n1, n0, n0, n0)), true, equalish(C_521, n0), true)=true))). % 47.88/36.16 tff(c_4208, plain, (![D_384, C_385, A_387]: (ifeq(equalish(D_384, D_384), true, ifeq(equalish(C_385, C_385), true, ifeq(equalish(A_387, A_387), true, f(A_387, n0, C_385, D_384, n1, sK1_relation_exists_F(A_387, n0, C_385, D_384, n1)), true), true), true)=true))). % 47.88/36.16 tff(c_668, plain, (![E_217, D_218, C_219]: (ifeq(equalish(E_217, E_217), true, ifeq(equalish(D_218, D_218), true, ifeq(equalish(C_219, C_219), true, f(n0, n1, C_219, D_218, E_217, sK1_relation_exists_F(n0, n1, C_219, D_218, E_217)), true), true), true)=true))). % 47.88/36.16 tff(c_4101, plain, (![D_375, C_376, B_377]: (ifeq(equalish(D_375, D_375), true, ifeq(equalish(C_376, C_376), true, ifeq(equalish(B_377, B_377), true, f(n1, B_377, C_376, D_375, n0, sK1_relation_exists_F(n1, B_377, C_376, D_375, n0)), true), true), true)=true))). % 47.88/36.16 tff(c_6422, plain, (![C_501, D_504, A_503, E_500, B_502]: (ifeq(f(A_503, B_502, C_501, D_504, E_500, sK1_relation_exists_F(n1, n1, n0, n0, n1)), true, equalish(E_500, n1), true)=true))). % 47.88/36.16 tff(c_4211, plain, (![D_384, B_386, A_387]: (ifeq(equalish(D_384, D_384), true, ifeq(equalish(B_386, B_386), true, ifeq(equalish(A_387, A_387), true, f(A_387, B_386, n1, D_384, n1, sK1_relation_exists_F(A_387, B_386, n1, D_384, n1)), true), true), true)=true))). % 47.88/36.16 tff(c_4207, plain, (![D_384, B_386, A_387]: (ifeq(equalish(D_384, D_384), true, ifeq(equalish(B_386, B_386), true, ifeq(equalish(A_387, A_387), true, f(A_387, B_386, n0, D_384, n1, sK1_relation_exists_F(A_387, B_386, n0, D_384, n1)), true), true), true)=true))). % 47.88/36.16 tff(c_1203, plain, (![E_239, D_240, B_242]: (ifeq(equalish(E_239, E_239), true, ifeq(equalish(D_240, D_240), true, ifeq(equalish(B_242, B_242), true, f(n0, B_242, n1, D_240, E_239, sK1_relation_exists_F(n0, B_242, n1, D_240, E_239)), true), true), true)=true))). % 47.88/36.16 tff(c_6052, plain, (![A_481, C_482, B_483, D_484, E_485]: (ifeq(f(A_481, B_483, C_482, D_484, E_485, sK1_relation_exists_F(n1, n1, n0, n0, n1)), true, equalish(D_484, n0), true)=true))). % 47.88/36.16 tff(c_3900, plain, (![E_367, C_368, B_369]: (ifeq(equalish(E_367, E_367), true, ifeq(equalish(C_368, C_368), true, ifeq(equalish(B_369, B_369), true, f(n1, B_369, C_368, n0, E_367, sK1_relation_exists_F(n1, B_369, C_368, n0, E_367)), true), true), true)=true))). % 47.88/36.16 tff(c_1830, plain, (![E_272, D_273, C_274]: (ifeq(equalish(E_272, E_272), true, ifeq(equalish(D_273, D_273), true, ifeq(equalish(C_274, C_274), true, f(n1, n0, C_274, D_273, E_272, sK1_relation_exists_F(n1, n0, C_274, D_273, E_272)), true), true), true)=true))). % 47.88/36.16 tff(c_669, plain, (![E_217, C_219, A_220]: (ifeq(equalish(E_217, E_217), true, ifeq(equalish(C_219, C_219), true, ifeq(equalish(A_220, A_220), true, f(A_220, n1, C_219, n1, E_217, sK1_relation_exists_F(A_220, n1, C_219, n1, E_217)), true), true), true)=true))). % 47.88/36.16 tff(c_5415, plain, (![C_454, D_452, B_450, E_453, A_451]: (ifeq(f(A_451, B_450, C_454, D_452, E_453, sK1_relation_exists_F(n1, n1, n0, n0, n1)), true, equalish(A_451, n1), true)=true))). % 47.88/36.16 tff(c_3280, plain, (![E_342, B_344, A_345]: (ifeq(equalish(E_342, E_342), true, ifeq(equalish(B_344, B_344), true, ifeq(equalish(A_345, A_345), true, f(A_345, B_344, n0, n1, E_342, sK1_relation_exists_F(A_345, B_344, n0, n1, E_342)), true), true), true)=true))). % 47.88/36.16 tff(c_4209, plain, (![D_384, C_385, B_386]: (ifeq(equalish(D_384, D_384), true, ifeq(equalish(C_385, C_385), true, ifeq(equalish(B_386, B_386), true, f(n0, B_386, C_385, D_384, n1, sK1_relation_exists_F(n0, B_386, C_385, D_384, n1)), true), true), true)=true))). % 47.88/36.16 tff(c_3898, plain, (![E_367, B_369, A_370]: (ifeq(equalish(E_367, E_367), true, ifeq(equalish(B_369, B_369), true, ifeq(equalish(A_370, A_370), true, f(A_370, B_369, n1, n0, E_367, sK1_relation_exists_F(A_370, B_369, n1, n0, E_367)), true), true), true)=true))). % 47.88/36.16 tff(c_4403, plain, (![C_400, D_403, E_399, A_402, B_401]: (ifeq(f(A_402, B_401, C_400, D_403, E_399, sK1_relation_exists_F(n1, n1, n0, n0, n0)), true, equalish(E_399, n0), true)=true))). % 47.88/36.16 tff(c_1829, plain, (![E_272, D_273, A_275]: (ifeq(equalish(E_272, E_272), true, ifeq(equalish(D_273, D_273), true, ifeq(equalish(A_275, A_275), true, f(A_275, n0, n1, D_273, E_272, sK1_relation_exists_F(A_275, n0, n1, D_273, E_272)), true), true), true)=true))). % 47.88/36.16 tff(c_4210, plain, (![C_385, B_386, A_387]: (ifeq(equalish(C_385, C_385), true, ifeq(equalish(B_386, B_386), true, ifeq(equalish(A_387, A_387), true, f(A_387, B_386, C_385, n1, n1, sK1_relation_exists_F(A_387, B_386, C_385, n1, n1)), true), true), true)=true))). % 47.88/36.16 tff(c_2277, plain, (![E_293, B_295, A_296]: (ifeq(equalish(E_293, E_293), true, ifeq(equalish(B_295, B_295), true, ifeq(equalish(A_296, A_296), true, f(A_296, B_295, n1, n1, E_293, sK1_relation_exists_F(A_296, B_295, n1, n1, E_293)), true), true), true)=true))). % 47.88/36.16 tff(c_4110, plain, (![A_380, B_379, E_382, C_383, D_381]: (ifeq(f(A_380, B_379, C_383, D_381, E_382, sK1_relation_exists_F(n1, n1, n0, n0, n0)), true, equalish(A_380, n1), true)=true))). % 47.88/36.16 tff(c_480, plain, (![E_195, C_197, B_196, A_198]: (ifeq(equalish(E_195, E_195), true, ifeq(equalish(C_197, C_197), true, ifeq(equalish(B_196, B_196), true, ifeq(equalish(A_198, A_198), true, f(A_198, B_196, C_197, n0, E_195, sK1_relation_exists_F(A_198, B_196, C_197, n0, E_195)), true), true), true), true)=true))). % 47.88/36.16 tff(c_2835, plain, (![A_325]: (ifeq(equalish(A_325, A_325), true, f(A_325, n1, n0, n0, n0, sK1_relation_exists_F(A_325, n1, n0, n0, n0)), true)=true))). % 47.88/36.16 tff(c_481, plain, (![E_195, D_194, B_196, A_198]: (ifeq(equalish(E_195, E_195), true, ifeq(equalish(D_194, D_194), true, ifeq(equalish(B_196, B_196), true, ifeq(equalish(A_198, A_198), true, f(A_198, B_196, n0, D_194, E_195, sK1_relation_exists_F(A_198, B_196, n0, D_194, E_195)), true), true), true), true)=true))). % 47.88/36.16 tff(c_2858, plain, (f(n1, n1, n0, n0, n0, sK1_relation_exists_F(n1, n1, n0, n0, n0))=true)). % 47.88/36.16 tff(c_487, plain, (![E_195, D_194, C_197, B_196]: (ifeq(equalish(E_195, E_195), true, ifeq(equalish(D_194, D_194), true, ifeq(equalish(C_197, C_197), true, ifeq(equalish(B_196, B_196), true, f(n1, B_196, C_197, D_194, E_195, sK1_relation_exists_F(n1, B_196, C_197, D_194, E_195)), true), true), true), true)=true))). % 47.88/36.16 tff(c_484, plain, (![E_195, C_197, B_196, A_198]: (ifeq(equalish(E_195, E_195), true, ifeq(equalish(C_197, C_197), true, ifeq(equalish(B_196, B_196), true, ifeq(equalish(A_198, A_198), true, f(A_198, B_196, C_197, n1, E_195, sK1_relation_exists_F(A_198, B_196, C_197, n1, E_195)), true), true), true), true)=true))). % 47.88/36.17 tff(c_1437, plain, (![A_255]: (ifeq(equalish(A_255, A_255), true, f(A_255, n1, n0, n0, n1, sK1_relation_exists_F(A_255, n1, n0, n0, n1)), true)=true))). % 47.88/36.17 tff(c_482, plain, (![E_195, D_194, C_197, A_198]: (ifeq(equalish(E_195, E_195), true, ifeq(equalish(D_194, D_194), true, ifeq(equalish(C_197, C_197), true, ifeq(equalish(A_198, A_198), true, f(A_198, n0, C_197, D_194, E_195, sK1_relation_exists_F(A_198, n0, C_197, D_194, E_195)), true), true), true), true)=true))). % 47.88/36.17 tff(c_1448, plain, (f(n1, n1, n0, n0, n1, sK1_relation_exists_F(n1, n1, n0, n0, n1))=true)). % 47.88/36.17 tff(c_483, plain, (![E_195, D_194, C_197, B_196]: (ifeq(equalish(E_195, E_195), true, ifeq(equalish(D_194, D_194), true, ifeq(equalish(C_197, C_197), true, ifeq(equalish(B_196, B_196), true, f(n0, B_196, C_197, D_194, E_195, sK1_relation_exists_F(n0, B_196, C_197, D_194, E_195)), true), true), true), true)=true))). % 47.88/36.17 tff(c_945, plain, (f(n0, n1, n0, n0, n1, sK1_relation_exists_F(n0, n1, n0, n0, n1))=true)). % 47.88/36.17 tff(c_838, plain, (f(n0, n1, n0, n0, n0, sK1_relation_exists_F(n0, n1, n0, n0, n0))=true)). % 47.88/36.17 tff(c_745, plain, (![E_224]: (ifeq(equalish(E_224, E_224), true, f(n0, n1, n0, n0, E_224, sK1_relation_exists_F(n0, n1, n0, n0, E_224)), true)=true))). % 47.88/36.17 tff(c_485, plain, (![E_195, D_194, B_196, A_198]: (ifeq(equalish(E_195, E_195), true, ifeq(equalish(D_194, D_194), true, ifeq(equalish(B_196, B_196), true, ifeq(equalish(A_198, A_198), true, f(A_198, B_196, n1, D_194, E_195, sK1_relation_exists_F(A_198, B_196, n1, D_194, E_195)), true), true), true), true)=true))). % 47.88/36.17 tff(c_707, plain, (![E_221, A_223]: (ifeq(equalish(E_221, E_221), true, ifeq(equalish(A_223, A_223), true, f(A_223, n1, n0, n0, E_221, sK1_relation_exists_F(A_223, n1, n0, n0, E_221)), true), true)=true))). % 47.88/36.17 tff(c_666, plain, (![E_217, C_219, A_220]: (ifeq(equalish(E_217, E_217), true, ifeq(equalish(C_219, C_219), true, ifeq(equalish(A_220, A_220), true, f(A_220, n1, C_219, n0, E_217, sK1_relation_exists_F(A_220, n1, C_219, n0, E_217)), true), true), true)=true))). % 47.88/36.17 tff(c_486, plain, (![E_195, D_194, C_197, A_198]: (ifeq(equalish(E_195, E_195), true, ifeq(equalish(D_194, D_194), true, ifeq(equalish(C_197, C_197), true, ifeq(equalish(A_198, A_198), true, f(A_198, n1, C_197, D_194, E_195, sK1_relation_exists_F(A_198, n1, C_197, D_194, E_195)), true), true), true), true)=true))). % 47.88/36.17 tff(c_432, plain, (![I_192, B_183, H_187, C_193, K_185, J_184, E_190, G_188, D_189]: (ifeq(f(n1, G_188, H_187, I_192, J_184, K_185), true, ifeq(f(n1, B_183, C_193, D_189, E_190, K_185), true, true, true), true)=true))). % 47.88/36.17 tff(c_429, plain, (![I_192, B_183, H_187, C_193, K_185, J_184, E_190, G_188, D_189]: (ifeq(f(n0, G_188, H_187, I_192, J_184, K_185), true, ifeq(f(n0, B_183, C_193, D_189, E_190, K_185), true, true, true), true)=true))). % 47.88/36.17 tff(c_12, plain, (![B_5, D_8, A_4, C_6, E_7]: (ifeq(equalish(E_7, E_7), true, ifeq(equalish(D_8, D_8), true, ifeq(equalish(C_6, C_6), true, ifeq(equalish(B_5, B_5), true, ifeq(equalish(A_4, A_4), true, f(A_4, B_5, C_6, D_8, E_7, sK1_relation_exists_F(A_4, B_5, C_6, D_8, E_7)), true), true), true), true), true)=true))). % 47.88/36.17 tff(c_22, plain, (![D_63, B_59, F_57, J_55, E_62, H_53, K_61, I_56, G_58, C_60, A_54]: (ifeq(f(F_57, G_58, H_53, I_56, J_55, K_61), true, ifeq(f(A_54, B_59, C_60, D_63, E_62, K_61), true, equalish(A_54, F_57), true), true)=true))). % 47.88/36.17 tff(c_279, plain, (![D_162, F_158, B_159, J_154, I_156, A_157, G_163, K_164, E_161]: (ifeq(f(F_158, G_163, n1, I_156, J_154, K_164), true, ifeq(f(A_157, B_159, n1, D_162, E_161, K_164), true, true, true), true)=true))). % 47.88/36.17 tff(c_276, plain, (![D_162, F_158, B_159, J_154, I_156, A_157, G_163, K_164, E_161]: (ifeq(f(F_158, G_163, n0, I_156, J_154, K_164), true, ifeq(f(A_157, B_159, n0, D_162, E_161, K_164), true, true, true), true)=true))). % 47.88/36.17 tff(c_18, plain, (![D_41, H_31, J_33, E_40, C_38, G_36, A_32, F_35, K_39, B_37, I_34]: (ifeq(f(F_35, G_36, H_31, I_34, J_33, K_39), true, ifeq(f(A_32, B_37, C_38, D_41, E_40, K_39), true, equalish(C_38, H_31), true), true)=true))). % 47.88/36.17 tff(c_166, plain, (![I_128, A_130, J_126, F_131, K_133, D_134, E_125, H_127, C_135]: (ifeq(f(F_131, n1, H_127, I_128, J_126, K_133), true, ifeq(f(A_130, n1, C_135, D_134, E_125, K_133), true, true, true), true)=true))). % 47.88/36.17 tff(c_163, plain, (![I_128, A_130, J_126, F_131, K_133, D_134, E_125, H_127, C_135]: (ifeq(f(F_131, n0, H_127, I_128, J_126, K_133), true, ifeq(f(A_130, n0, C_135, D_134, E_125, K_133), true, true, true), true)=true))). % 47.88/36.17 tff(c_20, plain, (![F_46, J_44, D_52, H_42, E_51, K_50, G_47, A_43, C_49, B_48, I_45]: (ifeq(f(F_46, G_47, H_42, I_45, J_44, K_50), true, ifeq(f(A_43, B_48, C_49, D_52, E_51, K_50), true, equalish(B_48, G_47), true), true)=true))). % 47.88/36.17 tff(c_93, plain, (![D_104, I_98, F_96, H_99, B_102, C_101, G_105, A_103, K_106]: (ifeq(f(F_96, G_105, H_99, I_98, n1, K_106), true, ifeq(f(A_103, B_102, C_101, D_104, n1, K_106), true, true, true), true)=true))). % 47.88/36.17 tff(c_90, plain, (![D_104, I_98, F_96, H_99, B_102, C_101, G_105, A_103, K_106]: (ifeq(f(F_96, G_105, H_99, I_98, n0, K_106), true, ifeq(f(A_103, B_102, C_101, D_104, n0, K_106), true, true, true), true)=true))). % 47.88/36.17 tff(c_14, plain, (![A_10, J_11, E_18, D_19, C_16, K_17, H_9, F_13, I_12, G_14, B_15]: (ifeq(f(F_13, G_14, H_9, I_12, J_11, K_17), true, ifeq(f(A_10, B_15, C_16, D_19, E_18, K_17), true, equalish(E_18, J_11), true), true)=true))). % 47.88/36.17 tff(c_60, plain, (![F_74, B_73, G_72, E_77, J_70, A_67, K_71, C_69, H_76]: (ifeq(f(F_74, G_72, H_76, n1, J_70, K_71), true, ifeq(f(A_67, B_73, C_69, n1, E_77, K_71), true, true, true), true)=true))). % 47.88/36.17 tff(c_57, plain, (![F_74, B_73, G_72, E_77, J_70, A_67, K_71, C_69, H_76]: (ifeq(f(F_74, G_72, H_76, n0, J_70, K_71), true, ifeq(f(A_67, B_73, C_69, n0, E_77, K_71), true, true, true), true)=true))). % 47.88/36.17 tff(c_16, plain, (![A_21, D_30, H_20, J_22, E_29, K_28, C_27, F_24, I_23, B_26, G_25]: (ifeq(f(F_24, G_25, H_20, I_23, J_22, K_28), true, ifeq(f(A_21, B_26, C_27, D_30, E_29, K_28), true, equalish(D_30, I_23), true), true)=true))). % 47.88/36.17 tff(c_10, plain, (ifeq(equalish(n1, n0), true, goal, true)=true)). % 47.88/36.17 tff(c_8, plain, (ifeq(equalish(n0, n1), true, goal, true)=true)). % 47.88/36.17 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq(A_1, A_1, B_2, C_3)=B_2))). % 47.88/36.17 tff(c_4, plain, (equalish(n0, n0)=true)). % 47.88/36.17 tff(c_6, plain, (equalish(n1, n1)=true)). % 47.88/36.17 tff(c_24, plain, (true!=goal)). % 47.88/36.17 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 47.88/36.17 %------------------------------------------------------------------------------