%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWV527-1.030 : TPTP v9.0.0. Released v4.0.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 : n015.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 09:31:00 PM UTC 2025
% Result : Unsatisfiable 60.11s 36.62s
% Output : CNFRefutation 61.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 65
% Number of leaves : 307
% Syntax : Number of formulae : 1567 (1159 unt; 0 typ; 0 def)
% Number of atoms : 1975 (1944 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 954 ( 546 ~; 408 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 2 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 127 ( 127 usr; 124 con; 0-3 aty)
% Number of variables : 87 ( 87 !; 0 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ store > sk > select > #nlpp > i_1129 > i9 > i8 > i7 > i6 > i5 > i4 > i30 > i3 > i29 > i28 > i27 > i26 > i25 > i24 > i23 > i22 > i21 > i20 > i2 > i19 > i18 > i17 > i16 > i15 > i14 > i13 > i12 > i11 > i10 > i1 > e_1131 > e_1130 > e9 > e8 > e7 > e6 > e5 > e4 > e30 > e3 > e29 > e28 > e27 > e26 > e25 > e24 > e23 > e22 > e21 > e20 > e2 > e19 > e18 > e17 > e16 > e15 > e14 > e13 > e12 > e11 > e10 > e1 > a_1128 > a_1127 > a_1126 > a_1125 > a_1124 > a_1123 > a_1122 > a_1121 > a_1120 > a_1119 > a_1118 > a_1117 > a_1116 > a_1115 > a_1114 > a_1113 > a_1112 > a_1111 > a_1110 > a_1109 > a_1108 > a_1107 > a_1106 > a_1105 > a_1104 > a_1103 > a_1102 > a_1101 > a_1100 > a_1099 > a_1098 > a_1097 > a_1096 > a_1095 > a_1094 > a_1093 > a_1092 > a_1091 > a_1090 > a_1089 > a_1088 > a_1087 > a_1086 > a_1085 > a_1084 > a_1083 > a_1082 > a_1081 > a_1080 > a_1079 > a_1078 > a_1077 > a_1076 > a_1075 > a_1074 > a_1073 > a_1072 > a_1071 > a_1070 > a_1069 > a1
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(e29,type,
e29: $i ).
tff(a_1096,type,
a_1096: $i ).
tff(a1,type,
a1: $i ).
tff(e1,type,
e1: $i ).
tff(a_1092,type,
a_1092: $i ).
tff(e8,type,
e8: $i ).
tff(e_1130,type,
e_1130: $i ).
tff(a_1094,type,
a_1094: $i ).
tff(a_1089,type,
a_1089: $i ).
tff(a_1116,type,
a_1116: $i ).
tff(e21,type,
e21: $i ).
tff(a_1107,type,
a_1107: $i ).
tff(i16,type,
i16: $i ).
tff(a_1109,type,
a_1109: $i ).
tff(a_1100,type,
a_1100: $i ).
tff(a_1084,type,
a_1084: $i ).
tff(a_1074,type,
a_1074: $i ).
tff(e15,type,
e15: $i ).
tff(i14,type,
i14: $i ).
tff(a_1087,type,
a_1087: $i ).
tff(i11,type,
i11: $i ).
tff(a_1103,type,
a_1103: $i ).
tff(a_1108,type,
a_1108: $i ).
tff(e18,type,
e18: $i ).
tff(a_1101,type,
a_1101: $i ).
tff(e24,type,
e24: $i ).
tff(a_1105,type,
a_1105: $i ).
tff(a_1085,type,
a_1085: $i ).
tff(i23,type,
i23: $i ).
tff(a_1121,type,
a_1121: $i ).
tff(i30,type,
i30: $i ).
tff(a_1102,type,
a_1102: $i ).
tff(store,type,
store: ( $i * $i * $i ) > $i ).
tff(a_1070,type,
a_1070: $i ).
tff(a_1111,type,
a_1111: $i ).
tff(e20,type,
e20: $i ).
tff(e19,type,
e19: $i ).
tff(e16,type,
e16: $i ).
tff(i20,type,
i20: $i ).
tff(e2,type,
e2: $i ).
tff(a_1120,type,
a_1120: $i ).
tff(i18,type,
i18: $i ).
tff(i27,type,
i27: $i ).
tff(a_1099,type,
a_1099: $i ).
tff(i26,type,
i26: $i ).
tff(a_1072,type,
a_1072: $i ).
tff(a_1110,type,
a_1110: $i ).
tff(e13,type,
e13: $i ).
tff(a_1081,type,
a_1081: $i ).
tff(i22,type,
i22: $i ).
tff(e22,type,
e22: $i ).
tff(i12,type,
i12: $i ).
tff(i15,type,
i15: $i ).
tff(i17,type,
i17: $i ).
tff(i19,type,
i19: $i ).
tff(i21,type,
i21: $i ).
tff(a_1104,type,
a_1104: $i ).
tff(e9,type,
e9: $i ).
tff(a_1090,type,
a_1090: $i ).
tff(i25,type,
i25: $i ).
tff(i28,type,
i28: $i ).
tff(a_1126,type,
a_1126: $i ).
tff(a_1091,type,
a_1091: $i ).
tff(a_1077,type,
a_1077: $i ).
tff(e25,type,
e25: $i ).
tff(e26,type,
e26: $i ).
tff(i10,type,
i10: $i ).
tff(e_1131,type,
e_1131: $i ).
tff(e17,type,
e17: $i ).
tff(e27,type,
e27: $i ).
tff(a_1127,type,
a_1127: $i ).
tff(e10,type,
e10: $i ).
tff(e7,type,
e7: $i ).
tff(a_1098,type,
a_1098: $i ).
tff(a_1095,type,
a_1095: $i ).
tff(i8,type,
i8: $i ).
tff(i9,type,
i9: $i ).
tff(sk,type,
sk: ( $i * $i ) > $i ).
tff(i29,type,
i29: $i ).
tff(i7,type,
i7: $i ).
tff(a_1075,type,
a_1075: $i ).
tff(i1,type,
i1: $i ).
tff(a_1069,type,
a_1069: $i ).
tff(a_1113,type,
a_1113: $i ).
tff(i2,type,
i2: $i ).
tff(a_1071,type,
a_1071: $i ).
tff(e30,type,
e30: $i ).
tff(select,type,
select: ( $i * $i ) > $i ).
tff(a_1097,type,
a_1097: $i ).
tff(a_1122,type,
a_1122: $i ).
tff(a_1125,type,
a_1125: $i ).
tff(a_1093,type,
a_1093: $i ).
tff(a_1112,type,
a_1112: $i ).
tff(a_1114,type,
a_1114: $i ).
tff(e23,type,
e23: $i ).
tff(a_1118,type,
a_1118: $i ).
tff(e14,type,
e14: $i ).
tff(a_1115,type,
a_1115: $i ).
tff(a_1086,type,
a_1086: $i ).
tff(e12,type,
e12: $i ).
tff(e4,type,
e4: $i ).
tff(i13,type,
i13: $i ).
tff(a_1083,type,
a_1083: $i ).
tff(a_1076,type,
a_1076: $i ).
tff(a_1106,type,
a_1106: $i ).
tff(a_1123,type,
a_1123: $i ).
tff(a_1119,type,
a_1119: $i ).
tff(a_1124,type,
a_1124: $i ).
tff(e6,type,
e6: $i ).
tff(i5,type,
i5: $i ).
tff(i_1129,type,
i_1129: $i ).
tff(e11,type,
e11: $i ).
tff(a_1082,type,
a_1082: $i ).
tff(e28,type,
e28: $i ).
tff(i4,type,
i4: $i ).
tff(a_1079,type,
a_1079: $i ).
tff(e3,type,
e3: $i ).
tff(a_1073,type,
a_1073: $i ).
tff(a_1080,type,
a_1080: $i ).
tff(i24,type,
i24: $i ).
tff(e5,type,
e5: $i ).
tff(a_1088,type,
a_1088: $i ).
tff(i3,type,
i3: $i ).
tff(a_1117,type,
a_1117: $i ).
tff(a_1078,type,
a_1078: $i ).
tff(a_1128,type,
a_1128: $i ).
tff(i6,type,
i6: $i ).
tff(f_33,axiom,
a_1069 = store(a1,i1,e1),
file(unknown,unknown) ).
tff(f_26,axiom,
! [A,I,E] : ( select(store(A,I,E),I) = E ),
file(unknown,unknown) ).
tff(f_769,axiom,
i4 != i19,
file(unknown,unknown) ).
tff(f_51,axiom,
a_1087 = store(a_1086,i19,e19),
file(unknown,unknown) ).
tff(f_30,axiom,
! [I,J,A,E] :
( ( I = J )
| ( select(store(A,I,E),J) = select(A,J) ) ),
file(unknown,unknown) ).
tff(f_579,axiom,
i8 != i20,
file(unknown,unknown) ).
tff(f_52,axiom,
a_1088 = store(a_1087,i20,e20),
file(unknown,unknown) ).
tff(f_667,axiom,
i6 != i21,
file(unknown,unknown) ).
tff(f_53,axiom,
a_1089 = store(a_1088,i21,e21),
file(unknown,unknown) ).
tff(f_159,axiom,
i22 != i27,
file(unknown,unknown) ).
tff(f_54,axiom,
a_1090 = store(a_1089,i22,e22),
file(unknown,unknown) ).
tff(f_151,axiom,
i23 != i24,
file(unknown,unknown) ).
tff(f_89,axiom,
a_1125 = store(a_1124,i23,e23),
file(unknown,unknown) ).
tff(f_137,axiom,
i24 != i25,
file(unknown,unknown) ).
tff(f_90,axiom,
a_1126 = store(a_1125,i24,e24),
file(unknown,unknown) ).
tff(f_647,axiom,
i7 != i8,
file(unknown,unknown) ).
tff(f_91,axiom,
a_1127 = store(a_1126,i7,e7),
file(unknown,unknown) ).
tff(f_515,axiom,
i10 != i11,
file(unknown,unknown) ).
tff(f_92,axiom,
a_1128 = store(a_1127,i10,e10),
file(unknown,unknown) ).
tff(f_94,axiom,
e_1131 = select(a_1128,i_1129),
file(unknown,unknown) ).
tff(f_967,axiom,
e_1130 != e_1131,
file(unknown,unknown) ).
tff(f_42,axiom,
a_1078 = store(a_1077,i10,e10),
file(unknown,unknown) ).
tff(f_513,axiom,
i10 != i12,
file(unknown,unknown) ).
tff(f_44,axiom,
a_1080 = store(a_1079,i12,e12),
file(unknown,unknown) ).
tff(f_511,axiom,
i10 != i13,
file(unknown,unknown) ).
tff(f_509,axiom,
i10 != i14,
file(unknown,unknown) ).
tff(f_507,axiom,
i10 != i15,
file(unknown,unknown) ).
tff(f_47,axiom,
a_1083 = store(a_1082,i15,e15),
file(unknown,unknown) ).
tff(f_505,axiom,
i10 != i16,
file(unknown,unknown) ).
tff(f_503,axiom,
i10 != i17,
file(unknown,unknown) ).
tff(f_501,axiom,
i10 != i18,
file(unknown,unknown) ).
tff(f_499,axiom,
i10 != i19,
file(unknown,unknown) ).
tff(f_497,axiom,
i10 != i20,
file(unknown,unknown) ).
tff(f_495,axiom,
i10 != i21,
file(unknown,unknown) ).
tff(f_493,axiom,
i10 != i22,
file(unknown,unknown) ).
tff(f_491,axiom,
i10 != i23,
file(unknown,unknown) ).
tff(f_489,axiom,
i10 != i24,
file(unknown,unknown) ).
tff(f_56,axiom,
a_1092 = store(a_1091,i24,e24),
file(unknown,unknown) ).
tff(f_487,axiom,
i10 != i25,
file(unknown,unknown) ).
tff(f_485,axiom,
i10 != i26,
file(unknown,unknown) ).
tff(f_58,axiom,
a_1094 = store(a_1093,i26,e26),
file(unknown,unknown) ).
tff(f_483,axiom,
i10 != i27,
file(unknown,unknown) ).
tff(f_481,axiom,
i10 != i28,
file(unknown,unknown) ).
tff(f_479,axiom,
i10 != i29,
file(unknown,unknown) ).
tff(f_61,axiom,
a_1097 = store(a_1096,i29,e29),
file(unknown,unknown) ).
tff(f_477,axiom,
i10 != i30,
file(unknown,unknown) ).
tff(f_62,axiom,
a_1098 = store(a_1097,i30,e30),
file(unknown,unknown) ).
tff(f_93,axiom,
e_1130 = select(a_1098,i_1129),
file(unknown,unknown) ).
tff(f_60,axiom,
a_1096 = store(a_1095,i28,e28),
file(unknown,unknown) ).
tff(f_59,axiom,
a_1095 = store(a_1094,i27,e27),
file(unknown,unknown) ).
tff(f_57,axiom,
a_1093 = store(a_1092,i25,e25),
file(unknown,unknown) ).
tff(f_55,axiom,
a_1091 = store(a_1090,i23,e23),
file(unknown,unknown) ).
tff(f_50,axiom,
a_1086 = store(a_1085,i18,e18),
file(unknown,unknown) ).
tff(f_49,axiom,
a_1085 = store(a_1084,i17,e17),
file(unknown,unknown) ).
tff(f_48,axiom,
a_1084 = store(a_1083,i16,e16),
file(unknown,unknown) ).
tff(f_46,axiom,
a_1082 = store(a_1081,i14,e14),
file(unknown,unknown) ).
tff(f_45,axiom,
a_1081 = store(a_1080,i13,e13),
file(unknown,unknown) ).
tff(f_43,axiom,
a_1079 = store(a_1078,i11,e11),
file(unknown,unknown) ).
tff(f_39,axiom,
a_1075 = store(a_1074,i7,e7),
file(unknown,unknown) ).
tff(f_645,axiom,
i7 != i9,
file(unknown,unknown) ).
tff(f_41,axiom,
a_1077 = store(a_1076,i9,e9),
file(unknown,unknown) ).
tff(f_643,axiom,
i7 != i10,
file(unknown,unknown) ).
tff(f_641,axiom,
i7 != i11,
file(unknown,unknown) ).
tff(f_639,axiom,
i7 != i12,
file(unknown,unknown) ).
tff(f_637,axiom,
i7 != i13,
file(unknown,unknown) ).
tff(f_635,axiom,
i7 != i14,
file(unknown,unknown) ).
tff(f_633,axiom,
i7 != i15,
file(unknown,unknown) ).
tff(f_631,axiom,
i7 != i16,
file(unknown,unknown) ).
tff(f_629,axiom,
i7 != i17,
file(unknown,unknown) ).
tff(f_627,axiom,
i7 != i18,
file(unknown,unknown) ).
tff(f_625,axiom,
i7 != i19,
file(unknown,unknown) ).
tff(f_623,axiom,
i7 != i20,
file(unknown,unknown) ).
tff(f_621,axiom,
i7 != i21,
file(unknown,unknown) ).
tff(f_619,axiom,
i7 != i22,
file(unknown,unknown) ).
tff(f_617,axiom,
i7 != i23,
file(unknown,unknown) ).
tff(f_615,axiom,
i7 != i24,
file(unknown,unknown) ).
tff(f_613,axiom,
i7 != i25,
file(unknown,unknown) ).
tff(f_611,axiom,
i7 != i26,
file(unknown,unknown) ).
tff(f_609,axiom,
i7 != i27,
file(unknown,unknown) ).
tff(f_607,axiom,
i7 != i28,
file(unknown,unknown) ).
tff(f_605,axiom,
i7 != i29,
file(unknown,unknown) ).
tff(f_603,axiom,
i7 != i30,
file(unknown,unknown) ).
tff(f_40,axiom,
a_1076 = store(a_1075,i8,e8),
file(unknown,unknown) ).
tff(f_135,axiom,
i24 != i26,
file(unknown,unknown) ).
tff(f_133,axiom,
i24 != i27,
file(unknown,unknown) ).
tff(f_131,axiom,
i24 != i28,
file(unknown,unknown) ).
tff(f_129,axiom,
i24 != i29,
file(unknown,unknown) ).
tff(f_127,axiom,
i24 != i30,
file(unknown,unknown) ).
tff(f_149,axiom,
i23 != i25,
file(unknown,unknown) ).
tff(f_147,axiom,
i23 != i26,
file(unknown,unknown) ).
tff(f_145,axiom,
i23 != i27,
file(unknown,unknown) ).
tff(f_143,axiom,
i23 != i28,
file(unknown,unknown) ).
tff(f_141,axiom,
i23 != i29,
file(unknown,unknown) ).
tff(f_139,axiom,
i23 != i30,
file(unknown,unknown) ).
tff(f_239,axiom,
i18 != i25,
file(unknown,unknown) ).
tff(f_161,axiom,
i22 != i26,
file(unknown,unknown) ).
tff(f_805,axiom,
i3 != i27,
file(unknown,unknown) ).
tff(f_257,axiom,
i17 != i28,
file(unknown,unknown) ).
tff(f_699,axiom,
i5 != i29,
file(unknown,unknown) ).
tff(f_853,axiom,
i2 != i30,
file(unknown,unknown) ).
tff(f_68,axiom,
a_1104 = store(a_1103,i30,e30),
file(unknown,unknown) ).
tff(f_307,axiom,
i15 != i30,
file(unknown,unknown) ).
tff(f_117,axiom,
i25 != i30,
file(unknown,unknown) ).
tff(f_229,axiom,
i18 != i30,
file(unknown,unknown) ).
tff(f_187,axiom,
i20 != i30,
file(unknown,unknown) ).
tff(f_559,axiom,
i8 != i30,
file(unknown,unknown) ).
tff(f_169,axiom,
i21 != i30,
file(unknown,unknown) ).
tff(f_75,axiom,
a_1111 = store(a_1110,i21,e21),
file(unknown,unknown) ).
tff(f_649,axiom,
i6 != i30,
file(unknown,unknown) ).
tff(f_439,axiom,
i11 != i30,
file(unknown,unknown) ).
tff(f_337,axiom,
i14 != i30,
file(unknown,unknown) ).
tff(f_78,axiom,
a_1114 = store(a_1113,i14,e14),
file(unknown,unknown) ).
tff(f_97,axiom,
i29 != i30,
file(unknown,unknown) ).
tff(f_697,axiom,
i5 != i30,
file(unknown,unknown) ).
tff(f_109,axiom,
i26 != i30,
file(unknown,unknown) ).
tff(f_81,axiom,
a_1117 = store(a_1116,i26,e26),
file(unknown,unknown) ).
tff(f_153,axiom,
i22 != i30,
file(unknown,unknown) ).
tff(f_103,axiom,
i27 != i30,
file(unknown,unknown) ).
tff(f_799,axiom,
i3 != i30,
file(unknown,unknown) ).
tff(f_84,axiom,
a_1120 = store(a_1119,i3,e3),
file(unknown,unknown) ).
tff(f_403,axiom,
i12 != i30,
file(unknown,unknown) ).
tff(f_279,axiom,
i16 != i30,
file(unknown,unknown) ).
tff(f_99,axiom,
i28 != i30,
file(unknown,unknown) ).
tff(f_87,axiom,
a_1123 = store(a_1122,i28,e28),
file(unknown,unknown) ).
tff(f_253,axiom,
i17 != i30,
file(unknown,unknown) ).
tff(f_88,axiom,
a_1124 = store(a_1123,i17,e17),
file(unknown,unknown) ).
tff(f_86,axiom,
a_1122 = store(a_1121,i16,e16),
file(unknown,unknown) ).
tff(f_85,axiom,
a_1121 = store(a_1120,i12,e12),
file(unknown,unknown) ).
tff(f_83,axiom,
a_1119 = store(a_1118,i27,e27),
file(unknown,unknown) ).
tff(f_82,axiom,
a_1118 = store(a_1117,i22,e22),
file(unknown,unknown) ).
tff(f_80,axiom,
a_1116 = store(a_1115,i5,e5),
file(unknown,unknown) ).
tff(f_79,axiom,
a_1115 = store(a_1114,i29,e29),
file(unknown,unknown) ).
tff(f_77,axiom,
a_1113 = store(a_1112,i11,e11),
file(unknown,unknown) ).
tff(f_76,axiom,
a_1112 = store(a_1111,i6,e6),
file(unknown,unknown) ).
tff(f_74,axiom,
a_1110 = store(a_1109,i8,e8),
file(unknown,unknown) ).
tff(f_73,axiom,
a_1109 = store(a_1108,i20,e20),
file(unknown,unknown) ).
tff(f_72,axiom,
a_1108 = store(a_1107,i18,e18),
file(unknown,unknown) ).
tff(f_71,axiom,
a_1107 = store(a_1106,i25,e25),
file(unknown,unknown) ).
tff(f_70,axiom,
a_1106 = store(a_1105,i15,e15),
file(unknown,unknown) ).
tff(f_69,axiom,
a_1105 = store(a_1104,i2,e2),
file(unknown,unknown) ).
tff(f_111,axiom,
i26 != i29,
file(unknown,unknown) ).
tff(f_155,axiom,
i22 != i29,
file(unknown,unknown) ).
tff(f_105,axiom,
i27 != i29,
file(unknown,unknown) ).
tff(f_801,axiom,
i3 != i29,
file(unknown,unknown) ).
tff(f_405,axiom,
i12 != i29,
file(unknown,unknown) ).
tff(f_281,axiom,
i16 != i29,
file(unknown,unknown) ).
tff(f_101,axiom,
i28 != i29,
file(unknown,unknown) ).
tff(f_255,axiom,
i17 != i29,
file(unknown,unknown) ).
tff(f_409,axiom,
i12 != i27,
file(unknown,unknown) ).
tff(f_285,axiom,
i16 != i27,
file(unknown,unknown) ).
tff(f_107,axiom,
i27 != i28,
file(unknown,unknown) ).
tff(f_259,axiom,
i17 != i27,
file(unknown,unknown) ).
tff(f_115,axiom,
i26 != i27,
file(unknown,unknown) ).
tff(f_807,axiom,
i3 != i26,
file(unknown,unknown) ).
tff(f_411,axiom,
i12 != i26,
file(unknown,unknown) ).
tff(f_287,axiom,
i16 != i26,
file(unknown,unknown) ).
tff(f_113,axiom,
i26 != i28,
file(unknown,unknown) ).
tff(f_277,axiom,
i17 != i18,
file(unknown,unknown) ).
tff(f_275,axiom,
i17 != i19,
file(unknown,unknown) ).
tff(f_273,axiom,
i17 != i20,
file(unknown,unknown) ).
tff(f_271,axiom,
i17 != i21,
file(unknown,unknown) ).
tff(f_269,axiom,
i17 != i22,
file(unknown,unknown) ).
tff(f_267,axiom,
i17 != i23,
file(unknown,unknown) ).
tff(f_265,axiom,
i17 != i24,
file(unknown,unknown) ).
tff(f_263,axiom,
i17 != i25,
file(unknown,unknown) ).
tff(f_261,axiom,
i17 != i26,
file(unknown,unknown) ).
tff(f_197,axiom,
i20 != i25,
file(unknown,unknown) ).
tff(f_569,axiom,
i8 != i25,
file(unknown,unknown) ).
tff(f_179,axiom,
i21 != i25,
file(unknown,unknown) ).
tff(f_659,axiom,
i6 != i25,
file(unknown,unknown) ).
tff(f_449,axiom,
i11 != i25,
file(unknown,unknown) ).
tff(f_347,axiom,
i14 != i25,
file(unknown,unknown) ).
tff(f_119,axiom,
i25 != i29,
file(unknown,unknown) ).
tff(f_707,axiom,
i5 != i25,
file(unknown,unknown) ).
tff(f_125,axiom,
i25 != i26,
file(unknown,unknown) ).
tff(f_163,axiom,
i22 != i25,
file(unknown,unknown) ).
tff(f_123,axiom,
i25 != i27,
file(unknown,unknown) ).
tff(f_809,axiom,
i3 != i25,
file(unknown,unknown) ).
tff(f_413,axiom,
i12 != i25,
file(unknown,unknown) ).
tff(f_289,axiom,
i16 != i25,
file(unknown,unknown) ).
tff(f_815,axiom,
i3 != i22,
file(unknown,unknown) ).
tff(f_437,axiom,
i12 != i13,
file(unknown,unknown) ).
tff(f_305,axiom,
i16 != i17,
file(unknown,unknown) ).
tff(f_303,axiom,
i16 != i18,
file(unknown,unknown) ).
tff(f_301,axiom,
i16 != i19,
file(unknown,unknown) ).
tff(f_299,axiom,
i16 != i20,
file(unknown,unknown) ).
tff(f_297,axiom,
i16 != i21,
file(unknown,unknown) ).
tff(f_295,axiom,
i16 != i22,
file(unknown,unknown) ).
tff(f_435,axiom,
i12 != i14,
file(unknown,unknown) ).
tff(f_433,axiom,
i12 != i15,
file(unknown,unknown) ).
tff(f_431,axiom,
i12 != i16,
file(unknown,unknown) ).
tff(f_429,axiom,
i12 != i17,
file(unknown,unknown) ).
tff(f_427,axiom,
i12 != i18,
file(unknown,unknown) ).
tff(f_425,axiom,
i12 != i19,
file(unknown,unknown) ).
tff(f_423,axiom,
i12 != i20,
file(unknown,unknown) ).
tff(f_421,axiom,
i12 != i21,
file(unknown,unknown) ).
tff(f_419,axiom,
i12 != i22,
file(unknown,unknown) ).
tff(f_457,axiom,
i11 != i21,
file(unknown,unknown) ).
tff(f_355,axiom,
i14 != i21,
file(unknown,unknown) ).
tff(f_171,axiom,
i21 != i29,
file(unknown,unknown) ).
tff(f_715,axiom,
i5 != i21,
file(unknown,unknown) ).
tff(f_177,axiom,
i21 != i26,
file(unknown,unknown) ).
tff(f_185,axiom,
i21 != i22,
file(unknown,unknown) ).
tff(f_851,axiom,
i3 != i4,
file(unknown,unknown) ).
tff(f_35,axiom,
a_1071 = store(a_1070,i3,e3),
file(unknown,unknown) ).
tff(f_849,axiom,
i3 != i5,
file(unknown,unknown) ).
tff(f_847,axiom,
i3 != i6,
file(unknown,unknown) ).
tff(f_38,axiom,
a_1074 = store(a_1073,i6,e6),
file(unknown,unknown) ).
tff(f_845,axiom,
i3 != i7,
file(unknown,unknown) ).
tff(f_843,axiom,
i3 != i8,
file(unknown,unknown) ).
tff(f_841,axiom,
i3 != i9,
file(unknown,unknown) ).
tff(f_839,axiom,
i3 != i10,
file(unknown,unknown) ).
tff(f_837,axiom,
i3 != i11,
file(unknown,unknown) ).
tff(f_835,axiom,
i3 != i12,
file(unknown,unknown) ).
tff(f_833,axiom,
i3 != i13,
file(unknown,unknown) ).
tff(f_831,axiom,
i3 != i14,
file(unknown,unknown) ).
tff(f_829,axiom,
i3 != i15,
file(unknown,unknown) ).
tff(f_827,axiom,
i3 != i16,
file(unknown,unknown) ).
tff(f_825,axiom,
i3 != i17,
file(unknown,unknown) ).
tff(f_823,axiom,
i3 != i18,
file(unknown,unknown) ).
tff(f_821,axiom,
i3 != i19,
file(unknown,unknown) ).
tff(f_819,axiom,
i3 != i20,
file(unknown,unknown) ).
tff(f_817,axiom,
i3 != i21,
file(unknown,unknown) ).
tff(f_37,axiom,
a_1073 = store(a_1072,i5,e5),
file(unknown,unknown) ).
tff(f_36,axiom,
a_1072 = store(a_1071,i4,e4),
file(unknown,unknown) ).
tff(f_205,axiom,
i20 != i21,
file(unknown,unknown) ).
tff(f_669,axiom,
i6 != i20,
file(unknown,unknown) ).
tff(f_459,axiom,
i11 != i20,
file(unknown,unknown) ).
tff(f_357,axiom,
i14 != i20,
file(unknown,unknown) ).
tff(f_189,axiom,
i20 != i29,
file(unknown,unknown) ).
tff(f_717,axiom,
i5 != i20,
file(unknown,unknown) ).
tff(f_195,axiom,
i20 != i26,
file(unknown,unknown) ).
tff(f_65,axiom,
a_1101 = store(a_1100,i19,e19),
file(unknown,unknown) ).
tff(f_539,axiom,
i9 != i19,
file(unknown,unknown) ).
tff(f_207,axiom,
i19 != i30,
file(unknown,unknown) ).
tff(f_875,axiom,
i2 != i19,
file(unknown,unknown) ).
tff(f_329,axiom,
i15 != i19,
file(unknown,unknown) ).
tff(f_217,axiom,
i19 != i25,
file(unknown,unknown) ).
tff(f_251,axiom,
i18 != i19,
file(unknown,unknown) ).
tff(f_227,axiom,
i19 != i20,
file(unknown,unknown) ).
tff(f_581,axiom,
i8 != i19,
file(unknown,unknown) ).
tff(f_225,axiom,
i19 != i21,
file(unknown,unknown) ).
tff(f_671,axiom,
i6 != i19,
file(unknown,unknown) ).
tff(f_461,axiom,
i11 != i19,
file(unknown,unknown) ).
tff(f_359,axiom,
i14 != i19,
file(unknown,unknown) ).
tff(f_209,axiom,
i19 != i29,
file(unknown,unknown) ).
tff(f_719,axiom,
i5 != i19,
file(unknown,unknown) ).
tff(f_67,axiom,
a_1103 = store(a_1102,i9,e9),
file(unknown,unknown) ).
tff(f_66,axiom,
a_1102 = store(a_1101,i4,e4),
file(unknown,unknown) ).
tff(f_745,axiom,
i5 != i6,
file(unknown,unknown) ).
tff(f_743,axiom,
i5 != i7,
file(unknown,unknown) ).
tff(f_741,axiom,
i5 != i8,
file(unknown,unknown) ).
tff(f_739,axiom,
i5 != i9,
file(unknown,unknown) ).
tff(f_737,axiom,
i5 != i10,
file(unknown,unknown) ).
tff(f_735,axiom,
i5 != i11,
file(unknown,unknown) ).
tff(f_733,axiom,
i5 != i12,
file(unknown,unknown) ).
tff(f_731,axiom,
i5 != i13,
file(unknown,unknown) ).
tff(f_729,axiom,
i5 != i14,
file(unknown,unknown) ).
tff(f_727,axiom,
i5 != i15,
file(unknown,unknown) ).
tff(f_725,axiom,
i5 != i16,
file(unknown,unknown) ).
tff(f_723,axiom,
i5 != i17,
file(unknown,unknown) ).
tff(f_721,axiom,
i5 != i18,
file(unknown,unknown) ).
tff(f_695,axiom,
i6 != i7,
file(unknown,unknown) ).
tff(f_475,axiom,
i11 != i12,
file(unknown,unknown) ).
tff(f_367,axiom,
i14 != i15,
file(unknown,unknown) ).
tff(f_249,axiom,
i18 != i20,
file(unknown,unknown) ).
tff(f_583,axiom,
i8 != i18,
file(unknown,unknown) ).
tff(f_247,axiom,
i18 != i21,
file(unknown,unknown) ).
tff(f_673,axiom,
i6 != i18,
file(unknown,unknown) ).
tff(f_463,axiom,
i11 != i18,
file(unknown,unknown) ).
tff(f_361,axiom,
i14 != i18,
file(unknown,unknown) ).
tff(f_231,axiom,
i18 != i29,
file(unknown,unknown) ).
tff(f_473,axiom,
i11 != i13,
file(unknown,unknown) ).
tff(f_471,axiom,
i11 != i14,
file(unknown,unknown) ).
tff(f_317,axiom,
i15 != i25,
file(unknown,unknown) ).
tff(f_331,axiom,
i15 != i18,
file(unknown,unknown) ).
tff(f_327,axiom,
i15 != i20,
file(unknown,unknown) ).
tff(f_589,axiom,
i8 != i15,
file(unknown,unknown) ).
tff(f_325,axiom,
i15 != i21,
file(unknown,unknown) ).
tff(f_679,axiom,
i6 != i15,
file(unknown,unknown) ).
tff(f_469,axiom,
i11 != i15,
file(unknown,unknown) ).
tff(f_693,axiom,
i6 != i8,
file(unknown,unknown) ).
tff(f_691,axiom,
i6 != i9,
file(unknown,unknown) ).
tff(f_689,axiom,
i6 != i10,
file(unknown,unknown) ).
tff(f_687,axiom,
i6 != i11,
file(unknown,unknown) ).
tff(f_685,axiom,
i6 != i12,
file(unknown,unknown) ).
tff(f_683,axiom,
i6 != i13,
file(unknown,unknown) ).
tff(f_601,axiom,
i8 != i9,
file(unknown,unknown) ).
tff(f_943,axiom,
i1 != i13,
file(unknown,unknown) ).
tff(f_63,axiom,
a_1099 = store(a1,i13,e13),
file(unknown,unknown) ).
tff(f_391,axiom,
i13 != i19,
file(unknown,unknown) ).
tff(f_781,axiom,
i4 != i13,
file(unknown,unknown) ).
tff(f_551,axiom,
i9 != i13,
file(unknown,unknown) ).
tff(f_369,axiom,
i13 != i30,
file(unknown,unknown) ).
tff(f_887,axiom,
i2 != i13,
file(unknown,unknown) ).
tff(f_399,axiom,
i13 != i15,
file(unknown,unknown) ).
tff(f_379,axiom,
i13 != i25,
file(unknown,unknown) ).
tff(f_393,axiom,
i13 != i18,
file(unknown,unknown) ).
tff(f_389,axiom,
i13 != i20,
file(unknown,unknown) ).
tff(f_593,axiom,
i8 != i13,
file(unknown,unknown) ).
tff(f_64,axiom,
a_1100 = store(a_1099,i1,e1),
file(unknown,unknown) ).
tff(f_517,axiom,
i9 != i30,
file(unknown,unknown) ).
tff(f_895,axiom,
i2 != i9,
file(unknown,unknown) ).
tff(f_547,axiom,
i9 != i15,
file(unknown,unknown) ).
tff(f_907,axiom,
i2 != i3,
file(unknown,unknown) ).
tff(f_34,axiom,
a_1070 = store(a_1069,i2,e2),
file(unknown,unknown) ).
tff(f_905,axiom,
i2 != i4,
file(unknown,unknown) ).
tff(c_8,plain,
store(a1,i1,e1) = a_1069,
inference(cnfTransformation,[status(thm)],[f_33]) ).
tff(c_1257,plain,
! [A_11,I_12,E_13] : ( select(store(A_11,I_12,E_13),I_12) = E_13 ),
inference(cnfTransformation,[status(thm)],[f_26]) ).
tff(c_1344,plain,
select(a_1069,i1) = e1,
inference(superposition,[status(thm),theory(equality)],[c_8,c_1257]) ).
tff(c_806,plain,
i4 != i19,
inference(cnfTransformation,[status(thm)],[f_769]) ).
tff(c_44,plain,
store(a_1086,i19,e19) = a_1087,
inference(cnfTransformation,[status(thm)],[f_51]) ).
tff(c_1356,plain,
select(a_1087,i19) = e19,
inference(superposition,[status(thm),theory(equality)],[c_44,c_1257]) ).
tff(c_1467,plain,
! [A_14,I_15,E_16,J_17] :
( ( select(store(A_14,I_15,E_16),J_17) = select(A_14,J_17) )
| ( J_17 = I_15 ) ),
inference(cnfTransformation,[status(thm)],[f_30]) ).
tff(c_1573,plain,
! [J_17] :
( ( select(a_1087,J_17) = select(a_1086,J_17) )
| ( i19 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_44,c_1467]) ).
tff(c_616,plain,
i8 != i20,
inference(cnfTransformation,[status(thm)],[f_579]) ).
tff(c_46,plain,
store(a_1087,i20,e20) = a_1088,
inference(cnfTransformation,[status(thm)],[f_52]) ).
tff(c_1335,plain,
select(a_1088,i20) = e20,
inference(superposition,[status(thm),theory(equality)],[c_46,c_1257]) ).
tff(c_704,plain,
i6 != i21,
inference(cnfTransformation,[status(thm)],[f_667]) ).
tff(c_48,plain,
store(a_1088,i21,e21) = a_1089,
inference(cnfTransformation,[status(thm)],[f_53]) ).
tff(c_1320,plain,
select(a_1089,i21) = e21,
inference(superposition,[status(thm),theory(equality)],[c_48,c_1257]) ).
tff(c_1537,plain,
! [J_17] :
( ( select(a_1089,J_17) = select(a_1088,J_17) )
| ( i21 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_48,c_1467]) ).
tff(c_196,plain,
i27 != i22,
inference(cnfTransformation,[status(thm)],[f_159]) ).
tff(c_50,plain,
store(a_1089,i22,e22) = a_1090,
inference(cnfTransformation,[status(thm)],[f_54]) ).
tff(c_1407,plain,
select(a_1090,i22) = e22,
inference(superposition,[status(thm),theory(equality)],[c_50,c_1257]) ).
tff(c_188,plain,
i24 != i23,
inference(cnfTransformation,[status(thm)],[f_151]) ).
tff(c_120,plain,
store(a_1124,i23,e23) = a_1125,
inference(cnfTransformation,[status(thm)],[f_89]) ).
tff(c_1377,plain,
select(a_1125,i23) = e23,
inference(superposition,[status(thm),theory(equality)],[c_120,c_1257]) ).
tff(c_174,plain,
i25 != i24,
inference(cnfTransformation,[status(thm)],[f_137]) ).
tff(c_122,plain,
store(a_1125,i24,e24) = a_1126,
inference(cnfTransformation,[status(thm)],[f_90]) ).
tff(c_1398,plain,
select(a_1126,i24) = e24,
inference(superposition,[status(thm),theory(equality)],[c_122,c_1257]) ).
tff(c_9561,plain,
! [J_138] :
( ( select(a_1126,J_138) = select(a_1125,J_138) )
| ( i24 = J_138 ) ),
inference(superposition,[status(thm),theory(equality)],[c_122,c_1467]) ).
tff(c_684,plain,
i8 != i7,
inference(cnfTransformation,[status(thm)],[f_647]) ).
tff(c_124,plain,
store(a_1126,i7,e7) = a_1127,
inference(cnfTransformation,[status(thm)],[f_91]) ).
tff(c_1317,plain,
select(a_1127,i7) = e7,
inference(superposition,[status(thm),theory(equality)],[c_124,c_1257]) ).
tff(c_552,plain,
i11 != i10,
inference(cnfTransformation,[status(thm)],[f_515]) ).
tff(c_126,plain,
store(a_1127,i10,e10) = a_1128,
inference(cnfTransformation,[status(thm)],[f_92]) ).
tff(c_1353,plain,
select(a_1128,i10) = e10,
inference(superposition,[status(thm),theory(equality)],[c_126,c_1257]) ).
tff(c_3704,plain,
! [J_47] :
( ( select(a_1128,J_47) = select(a_1127,J_47) )
| ( i10 = J_47 ) ),
inference(superposition,[status(thm),theory(equality)],[c_126,c_1467]) ).
tff(c_130,plain,
select(a_1128,i_1129) = e_1131,
inference(cnfTransformation,[status(thm)],[f_94]) ).
tff(c_3725,plain,
( ( select(a_1127,i_1129) = e_1131 )
| ( i_1129 = i10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_3704,c_130]) ).
tff(c_3739,plain,
i_1129 = i10,
inference(splitLeft,[status(thm)],[c_3725]) ).
tff(c_3740,plain,
select(a_1128,i10) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_3739,c_130]) ).
tff(c_3743,plain,
e_1131 = e10,
inference(demodulation,[status(thm),theory(equality)],[c_1353,c_3740]) ).
tff(c_1004,plain,
e_1131 != e_1130,
inference(cnfTransformation,[status(thm)],[f_967]) ).
tff(c_3748,plain,
e_1130 != e10,
inference(demodulation,[status(thm),theory(equality)],[c_3743,c_1004]) ).
tff(c_26,plain,
store(a_1077,i10,e10) = a_1078,
inference(cnfTransformation,[status(thm)],[f_42]) ).
tff(c_1350,plain,
select(a_1078,i10) = e10,
inference(superposition,[status(thm),theory(equality)],[c_26,c_1257]) ).
tff(c_550,plain,
i12 != i10,
inference(cnfTransformation,[status(thm)],[f_513]) ).
tff(c_30,plain,
store(a_1079,i12,e12) = a_1080,
inference(cnfTransformation,[status(thm)],[f_44]) ).
tff(c_1531,plain,
! [J_17] :
( ( select(a_1080,J_17) = select(a_1079,J_17) )
| ( i12 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_30,c_1467]) ).
tff(c_548,plain,
i13 != i10,
inference(cnfTransformation,[status(thm)],[f_511]) ).
tff(c_546,plain,
i14 != i10,
inference(cnfTransformation,[status(thm)],[f_509]) ).
tff(c_544,plain,
i15 != i10,
inference(cnfTransformation,[status(thm)],[f_507]) ).
tff(c_36,plain,
store(a_1082,i15,e15) = a_1083,
inference(cnfTransformation,[status(thm)],[f_47]) ).
tff(c_1630,plain,
! [J_17] :
( ( select(a_1083,J_17) = select(a_1082,J_17) )
| ( i15 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_36,c_1467]) ).
tff(c_542,plain,
i16 != i10,
inference(cnfTransformation,[status(thm)],[f_505]) ).
tff(c_540,plain,
i17 != i10,
inference(cnfTransformation,[status(thm)],[f_503]) ).
tff(c_538,plain,
i18 != i10,
inference(cnfTransformation,[status(thm)],[f_501]) ).
tff(c_536,plain,
i19 != i10,
inference(cnfTransformation,[status(thm)],[f_499]) ).
tff(c_534,plain,
i20 != i10,
inference(cnfTransformation,[status(thm)],[f_497]) ).
tff(c_532,plain,
i21 != i10,
inference(cnfTransformation,[status(thm)],[f_495]) ).
tff(c_530,plain,
i22 != i10,
inference(cnfTransformation,[status(thm)],[f_493]) ).
tff(c_528,plain,
i23 != i10,
inference(cnfTransformation,[status(thm)],[f_491]) ).
tff(c_526,plain,
i24 != i10,
inference(cnfTransformation,[status(thm)],[f_489]) ).
tff(c_54,plain,
store(a_1091,i24,e24) = a_1092,
inference(cnfTransformation,[status(thm)],[f_56]) ).
tff(c_1588,plain,
! [J_17] :
( ( select(a_1092,J_17) = select(a_1091,J_17) )
| ( i24 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_54,c_1467]) ).
tff(c_524,plain,
i25 != i10,
inference(cnfTransformation,[status(thm)],[f_487]) ).
tff(c_522,plain,
i26 != i10,
inference(cnfTransformation,[status(thm)],[f_485]) ).
tff(c_58,plain,
store(a_1093,i26,e26) = a_1094,
inference(cnfTransformation,[status(thm)],[f_58]) ).
tff(c_4793,plain,
! [J_79] :
( ( select(a_1094,J_79) = select(a_1093,J_79) )
| ( i26 = J_79 ) ),
inference(superposition,[status(thm),theory(equality)],[c_58,c_1467]) ).
tff(c_520,plain,
i27 != i10,
inference(cnfTransformation,[status(thm)],[f_483]) ).
tff(c_518,plain,
i28 != i10,
inference(cnfTransformation,[status(thm)],[f_481]) ).
tff(c_516,plain,
i29 != i10,
inference(cnfTransformation,[status(thm)],[f_479]) ).
tff(c_64,plain,
store(a_1096,i29,e29) = a_1097,
inference(cnfTransformation,[status(thm)],[f_61]) ).
tff(c_4416,plain,
! [J_69] :
( ( select(a_1097,J_69) = select(a_1096,J_69) )
| ( i29 = J_69 ) ),
inference(superposition,[status(thm),theory(equality)],[c_64,c_1467]) ).
tff(c_514,plain,
i30 != i10,
inference(cnfTransformation,[status(thm)],[f_477]) ).
tff(c_66,plain,
store(a_1097,i30,e30) = a_1098,
inference(cnfTransformation,[status(thm)],[f_62]) ).
tff(c_4213,plain,
! [J_63] :
( ( select(a_1098,J_63) = select(a_1097,J_63) )
| ( i30 = J_63 ) ),
inference(superposition,[status(thm),theory(equality)],[c_66,c_1467]) ).
tff(c_128,plain,
select(a_1098,i_1129) = e_1130,
inference(cnfTransformation,[status(thm)],[f_93]) ).
tff(c_3741,plain,
select(a_1098,i10) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_3739,c_128]) ).
tff(c_4219,plain,
( ( select(a_1097,i10) = e_1130 )
| ( i30 = i10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_4213,c_3741]) ).
tff(c_4245,plain,
select(a_1097,i10) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_514,c_4219]) ).
tff(c_4422,plain,
( ( select(a_1096,i10) = e_1130 )
| ( i29 = i10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_4416,c_4245]) ).
tff(c_4448,plain,
select(a_1096,i10) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_516,c_4422]) ).
tff(c_62,plain,
store(a_1095,i28,e28) = a_1096,
inference(cnfTransformation,[status(thm)],[f_60]) ).
tff(c_1528,plain,
! [J_17] :
( ( select(a_1096,J_17) = select(a_1095,J_17) )
| ( i28 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_62,c_1467]) ).
tff(c_4456,plain,
( ( select(a_1095,i10) = e_1130 )
| ( i28 = i10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_4448,c_1528]) ).
tff(c_4474,plain,
select(a_1095,i10) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_518,c_4456]) ).
tff(c_60,plain,
store(a_1094,i27,e27) = a_1095,
inference(cnfTransformation,[status(thm)],[f_59]) ).
tff(c_1579,plain,
! [J_17] :
( ( select(a_1095,J_17) = select(a_1094,J_17) )
| ( i27 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_60,c_1467]) ).
tff(c_4485,plain,
( ( select(a_1094,i10) = e_1130 )
| ( i27 = i10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_4474,c_1579]) ).
tff(c_4503,plain,
select(a_1094,i10) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_520,c_4485]) ).
tff(c_4799,plain,
( ( select(a_1093,i10) = e_1130 )
| ( i26 = i10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_4793,c_4503]) ).
tff(c_4825,plain,
select(a_1093,i10) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_522,c_4799]) ).
tff(c_56,plain,
store(a_1092,i25,e25) = a_1093,
inference(cnfTransformation,[status(thm)],[f_57]) ).
tff(c_1549,plain,
! [J_17] :
( ( select(a_1093,J_17) = select(a_1092,J_17) )
| ( i25 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_56,c_1467]) ).
tff(c_4833,plain,
( ( select(a_1092,i10) = e_1130 )
| ( i25 = i10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_4825,c_1549]) ).
tff(c_4851,plain,
select(a_1092,i10) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_524,c_4833]) ).
tff(c_4878,plain,
( ( select(a_1091,i10) = e_1130 )
| ( i24 = i10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1588,c_4851]) ).
tff(c_4886,plain,
select(a_1091,i10) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_526,c_4878]) ).
tff(c_52,plain,
store(a_1090,i23,e23) = a_1091,
inference(cnfTransformation,[status(thm)],[f_55]) ).
tff(c_1657,plain,
! [J_17] :
( ( select(a_1091,J_17) = select(a_1090,J_17) )
| ( i23 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_52,c_1467]) ).
tff(c_4891,plain,
( ( select(a_1090,i10) = e_1130 )
| ( i23 = i10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_4886,c_1657]) ).
tff(c_4909,plain,
select(a_1090,i10) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_528,c_4891]) ).
tff(c_1624,plain,
! [J_17] :
( ( select(a_1090,J_17) = select(a_1089,J_17) )
| ( i22 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_50,c_1467]) ).
tff(c_4920,plain,
( ( select(a_1089,i10) = e_1130 )
| ( i22 = i10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_4909,c_1624]) ).
tff(c_4938,plain,
select(a_1089,i10) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_530,c_4920]) ).
tff(c_4965,plain,
( ( select(a_1088,i10) = e_1130 )
| ( i21 = i10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1537,c_4938]) ).
tff(c_4973,plain,
select(a_1088,i10) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_532,c_4965]) ).
tff(c_1552,plain,
! [J_17] :
( ( select(a_1088,J_17) = select(a_1087,J_17) )
| ( i20 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_46,c_1467]) ).
tff(c_5007,plain,
( ( select(a_1087,i10) = e_1130 )
| ( i20 = i10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_4973,c_1552]) ).
tff(c_5025,plain,
select(a_1087,i10) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_534,c_5007]) ).
tff(c_5036,plain,
( ( select(a_1086,i10) = e_1130 )
| ( i19 = i10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_5025,c_1573]) ).
tff(c_5054,plain,
select(a_1086,i10) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_536,c_5036]) ).
tff(c_42,plain,
store(a_1085,i18,e18) = a_1086,
inference(cnfTransformation,[status(thm)],[f_50]) ).
tff(c_1525,plain,
! [J_17] :
( ( select(a_1086,J_17) = select(a_1085,J_17) )
| ( i18 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_42,c_1467]) ).
tff(c_5065,plain,
( ( select(a_1085,i10) = e_1130 )
| ( i18 = i10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_5054,c_1525]) ).
tff(c_5083,plain,
select(a_1085,i10) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_538,c_5065]) ).
tff(c_40,plain,
store(a_1084,i17,e17) = a_1085,
inference(cnfTransformation,[status(thm)],[f_49]) ).
tff(c_1540,plain,
! [J_17] :
( ( select(a_1085,J_17) = select(a_1084,J_17) )
| ( i17 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_40,c_1467]) ).
tff(c_5094,plain,
( ( select(a_1084,i10) = e_1130 )
| ( i17 = i10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_5083,c_1540]) ).
tff(c_5112,plain,
select(a_1084,i10) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_540,c_5094]) ).
tff(c_38,plain,
store(a_1083,i16,e16) = a_1084,
inference(cnfTransformation,[status(thm)],[f_48]) ).
tff(c_1489,plain,
! [J_17] :
( ( select(a_1084,J_17) = select(a_1083,J_17) )
| ( i16 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_38,c_1467]) ).
tff(c_6086,plain,
( ( select(a_1083,i10) = e_1130 )
| ( i16 = i10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_5112,c_1489]) ).
tff(c_6105,plain,
select(a_1083,i10) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_542,c_6086]) ).
tff(c_6138,plain,
( ( select(a_1082,i10) = e_1130 )
| ( i15 = i10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1630,c_6105]) ).
tff(c_6147,plain,
select(a_1082,i10) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_544,c_6138]) ).
tff(c_34,plain,
store(a_1081,i14,e14) = a_1082,
inference(cnfTransformation,[status(thm)],[f_46]) ).
tff(c_1645,plain,
! [J_17] :
( ( select(a_1082,J_17) = select(a_1081,J_17) )
| ( i14 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_34,c_1467]) ).
tff(c_6158,plain,
( ( select(a_1081,i10) = e_1130 )
| ( i14 = i10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_6147,c_1645]) ).
tff(c_6177,plain,
select(a_1081,i10) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_546,c_6158]) ).
tff(c_32,plain,
store(a_1080,i13,e13) = a_1081,
inference(cnfTransformation,[status(thm)],[f_45]) ).
tff(c_1597,plain,
! [J_17] :
( ( select(a_1081,J_17) = select(a_1080,J_17) )
| ( i13 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_32,c_1467]) ).
tff(c_6194,plain,
( ( select(a_1080,i10) = e_1130 )
| ( i13 = i10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_6177,c_1597]) ).
tff(c_6213,plain,
select(a_1080,i10) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_548,c_6194]) ).
tff(c_6246,plain,
( ( select(a_1079,i10) = e_1130 )
| ( i12 = i10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1531,c_6213]) ).
tff(c_6255,plain,
select(a_1079,i10) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_550,c_6246]) ).
tff(c_28,plain,
store(a_1078,i11,e11) = a_1079,
inference(cnfTransformation,[status(thm)],[f_43]) ).
tff(c_1543,plain,
! [J_17] :
( ( select(a_1079,J_17) = select(a_1078,J_17) )
| ( i11 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_28,c_1467]) ).
tff(c_6267,plain,
( ( select(a_1078,i10) = e_1130 )
| ( i11 = i10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_6255,c_1543]) ).
tff(c_6286,plain,
( ( e_1130 = e10 )
| ( i11 = i10 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1350,c_6267]) ).
tff(c_6288,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_552,c_3748,c_6286]) ).
tff(c_6290,plain,
i_1129 != i10,
inference(splitRight,[status(thm)],[c_3725]) ).
tff(c_3734,plain,
( ( select(a_1127,i_1129) = e_1131 )
| ( i_1129 = i10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_130,c_3704]) ).
tff(c_6291,plain,
select(a_1127,i_1129) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_6290,c_3734]) ).
tff(c_1534,plain,
! [J_17] :
( ( select(a_1127,J_17) = select(a_1126,J_17) )
| ( i7 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_124,c_1467]) ).
tff(c_6295,plain,
( ( select(a_1126,i_1129) = e_1131 )
| ( i_1129 = i7 ) ),
inference(superposition,[status(thm),theory(equality)],[c_6291,c_1534]) ).
tff(c_6319,plain,
i_1129 = i7,
inference(splitLeft,[status(thm)],[c_6295]) ).
tff(c_6320,plain,
select(a_1127,i7) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_6319,c_6291]) ).
tff(c_6325,plain,
e_1131 = e7,
inference(demodulation,[status(thm),theory(equality)],[c_1317,c_6320]) ).
tff(c_6330,plain,
e_1130 != e7,
inference(demodulation,[status(thm),theory(equality)],[c_6325,c_1004]) ).
tff(c_20,plain,
store(a_1074,i7,e7) = a_1075,
inference(cnfTransformation,[status(thm)],[f_39]) ).
tff(c_1293,plain,
select(a_1075,i7) = e7,
inference(superposition,[status(thm),theory(equality)],[c_20,c_1257]) ).
tff(c_682,plain,
i9 != i7,
inference(cnfTransformation,[status(thm)],[f_645]) ).
tff(c_24,plain,
store(a_1076,i9,e9) = a_1077,
inference(cnfTransformation,[status(thm)],[f_41]) ).
tff(c_1591,plain,
! [J_17] :
( ( select(a_1077,J_17) = select(a_1076,J_17) )
| ( i9 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_24,c_1467]) ).
tff(c_680,plain,
i7 != i10,
inference(cnfTransformation,[status(thm)],[f_643]) ).
tff(c_678,plain,
i7 != i11,
inference(cnfTransformation,[status(thm)],[f_641]) ).
tff(c_676,plain,
i7 != i12,
inference(cnfTransformation,[status(thm)],[f_639]) ).
tff(c_674,plain,
i7 != i13,
inference(cnfTransformation,[status(thm)],[f_637]) ).
tff(c_672,plain,
i7 != i14,
inference(cnfTransformation,[status(thm)],[f_635]) ).
tff(c_670,plain,
i7 != i15,
inference(cnfTransformation,[status(thm)],[f_633]) ).
tff(c_668,plain,
i7 != i16,
inference(cnfTransformation,[status(thm)],[f_631]) ).
tff(c_666,plain,
i7 != i17,
inference(cnfTransformation,[status(thm)],[f_629]) ).
tff(c_664,plain,
i7 != i18,
inference(cnfTransformation,[status(thm)],[f_627]) ).
tff(c_662,plain,
i7 != i19,
inference(cnfTransformation,[status(thm)],[f_625]) ).
tff(c_7638,plain,
! [J_116] :
( ( select(a_1087,J_116) = select(a_1086,J_116) )
| ( i19 = J_116 ) ),
inference(superposition,[status(thm),theory(equality)],[c_44,c_1467]) ).
tff(c_660,plain,
i7 != i20,
inference(cnfTransformation,[status(thm)],[f_623]) ).
tff(c_658,plain,
i7 != i21,
inference(cnfTransformation,[status(thm)],[f_621]) ).
tff(c_656,plain,
i7 != i22,
inference(cnfTransformation,[status(thm)],[f_619]) ).
tff(c_654,plain,
i7 != i23,
inference(cnfTransformation,[status(thm)],[f_617]) ).
tff(c_652,plain,
i7 != i24,
inference(cnfTransformation,[status(thm)],[f_615]) ).
tff(c_650,plain,
i7 != i25,
inference(cnfTransformation,[status(thm)],[f_613]) ).
tff(c_648,plain,
i7 != i26,
inference(cnfTransformation,[status(thm)],[f_611]) ).
tff(c_1504,plain,
! [J_17] :
( ( select(a_1094,J_17) = select(a_1093,J_17) )
| ( i26 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_58,c_1467]) ).
tff(c_646,plain,
i7 != i27,
inference(cnfTransformation,[status(thm)],[f_609]) ).
tff(c_644,plain,
i7 != i28,
inference(cnfTransformation,[status(thm)],[f_607]) ).
tff(c_642,plain,
i7 != i29,
inference(cnfTransformation,[status(thm)],[f_605]) ).
tff(c_640,plain,
i7 != i30,
inference(cnfTransformation,[status(thm)],[f_603]) ).
tff(c_7145,plain,
! [J_110] :
( ( select(a_1098,J_110) = select(a_1097,J_110) )
| ( i30 = J_110 ) ),
inference(superposition,[status(thm),theory(equality)],[c_66,c_1467]) ).
tff(c_6323,plain,
select(a_1098,i7) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_6319,c_128]) ).
tff(c_7151,plain,
( ( select(a_1097,i7) = e_1130 )
| ( i7 = i30 ) ),
inference(superposition,[status(thm),theory(equality)],[c_7145,c_6323]) ).
tff(c_7177,plain,
select(a_1097,i7) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_640,c_7151]) ).
tff(c_1576,plain,
! [J_17] :
( ( select(a_1097,J_17) = select(a_1096,J_17) )
| ( i29 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_64,c_1467]) ).
tff(c_7185,plain,
( ( select(a_1096,i7) = e_1130 )
| ( i7 = i29 ) ),
inference(superposition,[status(thm),theory(equality)],[c_7177,c_1576]) ).
tff(c_7203,plain,
select(a_1096,i7) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_642,c_7185]) ).
tff(c_7230,plain,
( ( select(a_1095,i7) = e_1130 )
| ( i7 = i28 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1528,c_7203]) ).
tff(c_7238,plain,
select(a_1095,i7) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_644,c_7230]) ).
tff(c_7243,plain,
( ( select(a_1094,i7) = e_1130 )
| ( i7 = i27 ) ),
inference(superposition,[status(thm),theory(equality)],[c_7238,c_1579]) ).
tff(c_7261,plain,
select(a_1094,i7) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_646,c_7243]) ).
tff(c_7288,plain,
( ( select(a_1093,i7) = e_1130 )
| ( i7 = i26 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1504,c_7261]) ).
tff(c_7296,plain,
select(a_1093,i7) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_648,c_7288]) ).
tff(c_7317,plain,
( ( select(a_1092,i7) = e_1130 )
| ( i7 = i25 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1549,c_7296]) ).
tff(c_7325,plain,
select(a_1092,i7) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_650,c_7317]) ).
tff(c_7359,plain,
( ( select(a_1091,i7) = e_1130 )
| ( i7 = i24 ) ),
inference(superposition,[status(thm),theory(equality)],[c_7325,c_1588]) ).
tff(c_7377,plain,
select(a_1091,i7) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_652,c_7359]) ).
tff(c_7388,plain,
( ( select(a_1090,i7) = e_1130 )
| ( i7 = i23 ) ),
inference(superposition,[status(thm),theory(equality)],[c_7377,c_1657]) ).
tff(c_7406,plain,
select(a_1090,i7) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_654,c_7388]) ).
tff(c_7417,plain,
( ( select(a_1089,i7) = e_1130 )
| ( i7 = i22 ) ),
inference(superposition,[status(thm),theory(equality)],[c_7406,c_1624]) ).
tff(c_7435,plain,
select(a_1089,i7) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_656,c_7417]) ).
tff(c_7446,plain,
( ( select(a_1088,i7) = e_1130 )
| ( i7 = i21 ) ),
inference(superposition,[status(thm),theory(equality)],[c_7435,c_1537]) ).
tff(c_7464,plain,
select(a_1088,i7) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_658,c_7446]) ).
tff(c_7504,plain,
( ( select(a_1087,i7) = e_1130 )
| ( i7 = i20 ) ),
inference(superposition,[status(thm),theory(equality)],[c_7464,c_1552]) ).
tff(c_7522,plain,
select(a_1087,i7) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_660,c_7504]) ).
tff(c_7644,plain,
( ( select(a_1086,i7) = e_1130 )
| ( i7 = i19 ) ),
inference(superposition,[status(thm),theory(equality)],[c_7638,c_7522]) ).
tff(c_7670,plain,
select(a_1086,i7) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_662,c_7644]) ).
tff(c_7694,plain,
( ( select(a_1085,i7) = e_1130 )
| ( i7 = i18 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1525,c_7670]) ).
tff(c_7702,plain,
select(a_1085,i7) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_664,c_7694]) ).
tff(c_8670,plain,
( ( select(a_1084,i7) = e_1130 )
| ( i7 = i17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_7702,c_1540]) ).
tff(c_8689,plain,
select(a_1084,i7) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_666,c_8670]) ).
tff(c_8706,plain,
( ( select(a_1083,i7) = e_1130 )
| ( i7 = i16 ) ),
inference(superposition,[status(thm),theory(equality)],[c_8689,c_1489]) ).
tff(c_8725,plain,
select(a_1083,i7) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_668,c_8706]) ).
tff(c_8742,plain,
( ( select(a_1082,i7) = e_1130 )
| ( i7 = i15 ) ),
inference(superposition,[status(thm),theory(equality)],[c_8725,c_1630]) ).
tff(c_8761,plain,
select(a_1082,i7) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_670,c_8742]) ).
tff(c_8778,plain,
( ( select(a_1081,i7) = e_1130 )
| ( i7 = i14 ) ),
inference(superposition,[status(thm),theory(equality)],[c_8761,c_1645]) ).
tff(c_8797,plain,
select(a_1081,i7) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_672,c_8778]) ).
tff(c_8815,plain,
( ( select(a_1080,i7) = e_1130 )
| ( i7 = i13 ) ),
inference(superposition,[status(thm),theory(equality)],[c_8797,c_1597]) ).
tff(c_8834,plain,
select(a_1080,i7) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_674,c_8815]) ).
tff(c_8867,plain,
( ( select(a_1079,i7) = e_1130 )
| ( i7 = i12 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1531,c_8834]) ).
tff(c_8876,plain,
select(a_1079,i7) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_676,c_8867]) ).
tff(c_8887,plain,
( ( select(a_1078,i7) = e_1130 )
| ( i7 = i11 ) ),
inference(superposition,[status(thm),theory(equality)],[c_8876,c_1543]) ).
tff(c_8906,plain,
select(a_1078,i7) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_678,c_8887]) ).
tff(c_1567,plain,
! [J_17] :
( ( select(a_1078,J_17) = select(a_1077,J_17) )
| ( i10 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_26,c_1467]) ).
tff(c_8923,plain,
( ( select(a_1077,i7) = e_1130 )
| ( i7 = i10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_8906,c_1567]) ).
tff(c_8942,plain,
select(a_1077,i7) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_680,c_8923]) ).
tff(c_8975,plain,
( ( select(a_1076,i7) = e_1130 )
| ( i9 = i7 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1591,c_8942]) ).
tff(c_8984,plain,
select(a_1076,i7) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_682,c_8975]) ).
tff(c_22,plain,
store(a_1075,i8,e8) = a_1076,
inference(cnfTransformation,[status(thm)],[f_40]) ).
tff(c_1651,plain,
! [J_17] :
( ( select(a_1076,J_17) = select(a_1075,J_17) )
| ( i8 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_22,c_1467]) ).
tff(c_9022,plain,
( ( select(a_1075,i7) = e_1130 )
| ( i8 = i7 ) ),
inference(superposition,[status(thm),theory(equality)],[c_8984,c_1651]) ).
tff(c_9041,plain,
( ( e_1130 = e7 )
| ( i8 = i7 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1293,c_9022]) ).
tff(c_9043,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_684,c_6330,c_9041]) ).
tff(c_9044,plain,
select(a_1126,i_1129) = e_1131,
inference(splitRight,[status(thm)],[c_6295]) ).
tff(c_9567,plain,
( ( select(a_1125,i_1129) = e_1131 )
| ( i_1129 = i24 ) ),
inference(superposition,[status(thm),theory(equality)],[c_9561,c_9044]) ).
tff(c_9625,plain,
i_1129 = i24,
inference(splitLeft,[status(thm)],[c_9567]) ).
tff(c_9626,plain,
select(a_1126,i24) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_9625,c_9044]) ).
tff(c_9633,plain,
e_1131 = e24,
inference(demodulation,[status(thm),theory(equality)],[c_1398,c_9626]) ).
tff(c_9638,plain,
e_1130 != e24,
inference(demodulation,[status(thm),theory(equality)],[c_9633,c_1004]) ).
tff(c_1371,plain,
select(a_1092,i24) = e24,
inference(superposition,[status(thm),theory(equality)],[c_54,c_1257]) ).
tff(c_10194,plain,
! [J_151] :
( ( select(a_1093,J_151) = select(a_1092,J_151) )
| ( i25 = J_151 ) ),
inference(superposition,[status(thm),theory(equality)],[c_56,c_1467]) ).
tff(c_172,plain,
i26 != i24,
inference(cnfTransformation,[status(thm)],[f_135]) ).
tff(c_170,plain,
i27 != i24,
inference(cnfTransformation,[status(thm)],[f_133]) ).
tff(c_168,plain,
i28 != i24,
inference(cnfTransformation,[status(thm)],[f_131]) ).
tff(c_166,plain,
i29 != i24,
inference(cnfTransformation,[status(thm)],[f_129]) ).
tff(c_164,plain,
i30 != i24,
inference(cnfTransformation,[status(thm)],[f_127]) ).
tff(c_9962,plain,
! [J_148] :
( ( select(a_1098,J_148) = select(a_1097,J_148) )
| ( i30 = J_148 ) ),
inference(superposition,[status(thm),theory(equality)],[c_66,c_1467]) ).
tff(c_9631,plain,
select(a_1098,i24) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_9625,c_128]) ).
tff(c_9968,plain,
( ( select(a_1097,i24) = e_1130 )
| ( i30 = i24 ) ),
inference(superposition,[status(thm),theory(equality)],[c_9962,c_9631]) ).
tff(c_9994,plain,
select(a_1097,i24) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_164,c_9968]) ).
tff(c_10002,plain,
( ( select(a_1096,i24) = e_1130 )
| ( i29 = i24 ) ),
inference(superposition,[status(thm),theory(equality)],[c_9994,c_1576]) ).
tff(c_10020,plain,
select(a_1096,i24) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_166,c_10002]) ).
tff(c_10047,plain,
( ( select(a_1095,i24) = e_1130 )
| ( i28 = i24 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1528,c_10020]) ).
tff(c_10055,plain,
select(a_1095,i24) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_168,c_10047]) ).
tff(c_10060,plain,
( ( select(a_1094,i24) = e_1130 )
| ( i27 = i24 ) ),
inference(superposition,[status(thm),theory(equality)],[c_10055,c_1579]) ).
tff(c_10078,plain,
select(a_1094,i24) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_170,c_10060]) ).
tff(c_10105,plain,
( ( select(a_1093,i24) = e_1130 )
| ( i26 = i24 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1504,c_10078]) ).
tff(c_10113,plain,
select(a_1093,i24) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_172,c_10105]) ).
tff(c_10200,plain,
( ( select(a_1092,i24) = e_1130 )
| ( i25 = i24 ) ),
inference(superposition,[status(thm),theory(equality)],[c_10194,c_10113]) ).
tff(c_10226,plain,
( ( e_1130 = e24 )
| ( i25 = i24 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1371,c_10200]) ).
tff(c_10228,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_174,c_9638,c_10226]) ).
tff(c_10229,plain,
select(a_1125,i_1129) = e_1131,
inference(splitRight,[status(thm)],[c_9567]) ).
tff(c_1594,plain,
! [J_17] :
( ( select(a_1125,J_17) = select(a_1124,J_17) )
| ( i23 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_120,c_1467]) ).
tff(c_10234,plain,
( ( select(a_1124,i_1129) = e_1131 )
| ( i_1129 = i23 ) ),
inference(superposition,[status(thm),theory(equality)],[c_10229,c_1594]) ).
tff(c_10259,plain,
i_1129 = i23,
inference(splitLeft,[status(thm)],[c_10234]) ).
tff(c_10295,plain,
select(a_1125,i23) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_10259,c_10229]) ).
tff(c_10304,plain,
e_1131 = e23,
inference(demodulation,[status(thm),theory(equality)],[c_1377,c_10295]) ).
tff(c_10309,plain,
e_1130 != e23,
inference(demodulation,[status(thm),theory(equality)],[c_10304,c_1004]) ).
tff(c_1440,plain,
select(a_1091,i23) = e23,
inference(superposition,[status(thm),theory(equality)],[c_52,c_1257]) ).
tff(c_186,plain,
i25 != i23,
inference(cnfTransformation,[status(thm)],[f_149]) ).
tff(c_10639,plain,
! [J_155] :
( ( select(a_1093,J_155) = select(a_1092,J_155) )
| ( i25 = J_155 ) ),
inference(superposition,[status(thm),theory(equality)],[c_56,c_1467]) ).
tff(c_184,plain,
i26 != i23,
inference(cnfTransformation,[status(thm)],[f_147]) ).
tff(c_182,plain,
i27 != i23,
inference(cnfTransformation,[status(thm)],[f_145]) ).
tff(c_180,plain,
i28 != i23,
inference(cnfTransformation,[status(thm)],[f_143]) ).
tff(c_178,plain,
i29 != i23,
inference(cnfTransformation,[status(thm)],[f_141]) ).
tff(c_176,plain,
i30 != i23,
inference(cnfTransformation,[status(thm)],[f_139]) ).
tff(c_1555,plain,
! [J_17] :
( ( select(a_1098,J_17) = select(a_1097,J_17) )
| ( i30 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_66,c_1467]) ).
tff(c_10302,plain,
select(a_1098,i23) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_10259,c_128]) ).
tff(c_10366,plain,
( ( select(a_1097,i23) = e_1130 )
| ( i30 = i23 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1555,c_10302]) ).
tff(c_10374,plain,
select(a_1097,i23) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_176,c_10366]) ).
tff(c_10471,plain,
( ( select(a_1096,i23) = e_1130 )
| ( i29 = i23 ) ),
inference(superposition,[status(thm),theory(equality)],[c_10374,c_1576]) ).
tff(c_10489,plain,
select(a_1096,i23) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_178,c_10471]) ).
tff(c_10500,plain,
( ( select(a_1095,i23) = e_1130 )
| ( i28 = i23 ) ),
inference(superposition,[status(thm),theory(equality)],[c_10489,c_1528]) ).
tff(c_10518,plain,
select(a_1095,i23) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_180,c_10500]) ).
tff(c_10529,plain,
( ( select(a_1094,i23) = e_1130 )
| ( i27 = i23 ) ),
inference(superposition,[status(thm),theory(equality)],[c_10518,c_1579]) ).
tff(c_10547,plain,
select(a_1094,i23) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_182,c_10529]) ).
tff(c_10587,plain,
( ( select(a_1093,i23) = e_1130 )
| ( i26 = i23 ) ),
inference(superposition,[status(thm),theory(equality)],[c_10547,c_1504]) ).
tff(c_10605,plain,
select(a_1093,i23) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_184,c_10587]) ).
tff(c_10645,plain,
( ( select(a_1092,i23) = e_1130 )
| ( i25 = i23 ) ),
inference(superposition,[status(thm),theory(equality)],[c_10639,c_10605]) ).
tff(c_10671,plain,
select(a_1092,i23) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_186,c_10645]) ).
tff(c_10679,plain,
( ( select(a_1091,i23) = e_1130 )
| ( i24 = i23 ) ),
inference(superposition,[status(thm),theory(equality)],[c_10671,c_1588]) ).
tff(c_10697,plain,
( ( e_1130 = e23 )
| ( i24 = i23 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1440,c_10679]) ).
tff(c_10699,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_188,c_10309,c_10697]) ).
tff(c_10701,plain,
i_1129 != i23,
inference(splitRight,[status(thm)],[c_10234]) ).
tff(c_16966,plain,
! [J_207] :
( ( select(a_1091,J_207) = select(a_1090,J_207) )
| ( i23 = J_207 ) ),
inference(superposition,[status(thm),theory(equality)],[c_52,c_1467]) ).
tff(c_10230,plain,
i_1129 != i24,
inference(splitRight,[status(thm)],[c_9567]) ).
tff(c_276,plain,
i25 != i18,
inference(cnfTransformation,[status(thm)],[f_239]) ).
tff(c_1332,plain,
select(a_1093,i25) = e25,
inference(superposition,[status(thm),theory(equality)],[c_56,c_1257]) ).
tff(c_198,plain,
i26 != i22,
inference(cnfTransformation,[status(thm)],[f_161]) ).
tff(c_1287,plain,
select(a_1094,i26) = e26,
inference(superposition,[status(thm),theory(equality)],[c_58,c_1257]) ).
tff(c_842,plain,
i3 != i27,
inference(cnfTransformation,[status(thm)],[f_805]) ).
tff(c_1362,plain,
select(a_1095,i27) = e27,
inference(superposition,[status(thm),theory(equality)],[c_60,c_1257]) ).
tff(c_294,plain,
i28 != i17,
inference(cnfTransformation,[status(thm)],[f_257]) ).
tff(c_1311,plain,
select(a_1096,i28) = e28,
inference(superposition,[status(thm),theory(equality)],[c_62,c_1257]) ).
tff(c_736,plain,
i5 != i29,
inference(cnfTransformation,[status(thm)],[f_699]) ).
tff(c_1359,plain,
select(a_1097,i29) = e29,
inference(superposition,[status(thm),theory(equality)],[c_64,c_1257]) ).
tff(c_890,plain,
i30 != i2,
inference(cnfTransformation,[status(thm)],[f_853]) ).
tff(c_1338,plain,
select(a_1098,i30) = e30,
inference(superposition,[status(thm),theory(equality)],[c_66,c_1257]) ).
tff(c_10702,plain,
! [J_156] :
( ( select(a_1098,J_156) = select(a_1097,J_156) )
| ( i30 = J_156 ) ),
inference(superposition,[status(thm),theory(equality)],[c_66,c_1467]) ).
tff(c_10723,plain,
( ( select(a_1097,i_1129) = e_1130 )
| ( i_1129 = i30 ) ),
inference(superposition,[status(thm),theory(equality)],[c_10702,c_128]) ).
tff(c_10763,plain,
i_1129 = i30,
inference(splitLeft,[status(thm)],[c_10723]) ).
tff(c_10774,plain,
select(a_1098,i30) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_10763,c_128]) ).
tff(c_10776,plain,
e_1130 = e30,
inference(demodulation,[status(thm),theory(equality)],[c_1338,c_10774]) ).
tff(c_10782,plain,
e_1131 != e30,
inference(demodulation,[status(thm),theory(equality)],[c_10776,c_1004]) ).
tff(c_78,plain,
store(a_1103,i30,e30) = a_1104,
inference(cnfTransformation,[status(thm)],[f_68]) ).
tff(c_1365,plain,
select(a_1104,i30) = e30,
inference(superposition,[status(thm),theory(equality)],[c_78,c_1257]) ).
tff(c_344,plain,
i30 != i15,
inference(cnfTransformation,[status(thm)],[f_307]) ).
tff(c_154,plain,
i30 != i25,
inference(cnfTransformation,[status(thm)],[f_117]) ).
tff(c_266,plain,
i30 != i18,
inference(cnfTransformation,[status(thm)],[f_229]) ).
tff(c_224,plain,
i30 != i20,
inference(cnfTransformation,[status(thm)],[f_187]) ).
tff(c_596,plain,
i8 != i30,
inference(cnfTransformation,[status(thm)],[f_559]) ).
tff(c_206,plain,
i30 != i21,
inference(cnfTransformation,[status(thm)],[f_169]) ).
tff(c_92,plain,
store(a_1110,i21,e21) = a_1111,
inference(cnfTransformation,[status(thm)],[f_75]) ).
tff(c_1648,plain,
! [J_17] :
( ( select(a_1111,J_17) = select(a_1110,J_17) )
| ( i21 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_92,c_1467]) ).
tff(c_686,plain,
i6 != i30,
inference(cnfTransformation,[status(thm)],[f_649]) ).
tff(c_476,plain,
i30 != i11,
inference(cnfTransformation,[status(thm)],[f_439]) ).
tff(c_374,plain,
i30 != i14,
inference(cnfTransformation,[status(thm)],[f_337]) ).
tff(c_98,plain,
store(a_1113,i14,e14) = a_1114,
inference(cnfTransformation,[status(thm)],[f_78]) ).
tff(c_1606,plain,
! [J_17] :
( ( select(a_1114,J_17) = select(a_1113,J_17) )
| ( i14 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_98,c_1467]) ).
tff(c_134,plain,
i30 != i29,
inference(cnfTransformation,[status(thm)],[f_97]) ).
tff(c_734,plain,
i5 != i30,
inference(cnfTransformation,[status(thm)],[f_697]) ).
tff(c_146,plain,
i30 != i26,
inference(cnfTransformation,[status(thm)],[f_109]) ).
tff(c_104,plain,
store(a_1116,i26,e26) = a_1117,
inference(cnfTransformation,[status(thm)],[f_81]) ).
tff(c_11401,plain,
! [J_166] :
( ( select(a_1117,J_166) = select(a_1116,J_166) )
| ( i26 = J_166 ) ),
inference(superposition,[status(thm),theory(equality)],[c_104,c_1467]) ).
tff(c_190,plain,
i30 != i22,
inference(cnfTransformation,[status(thm)],[f_153]) ).
tff(c_140,plain,
i30 != i27,
inference(cnfTransformation,[status(thm)],[f_103]) ).
tff(c_836,plain,
i30 != i3,
inference(cnfTransformation,[status(thm)],[f_799]) ).
tff(c_110,plain,
store(a_1119,i3,e3) = a_1120,
inference(cnfTransformation,[status(thm)],[f_84]) ).
tff(c_1603,plain,
! [J_17] :
( ( select(a_1120,J_17) = select(a_1119,J_17) )
| ( i3 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_110,c_1467]) ).
tff(c_440,plain,
i30 != i12,
inference(cnfTransformation,[status(thm)],[f_403]) ).
tff(c_316,plain,
i30 != i16,
inference(cnfTransformation,[status(thm)],[f_279]) ).
tff(c_136,plain,
i30 != i28,
inference(cnfTransformation,[status(thm)],[f_99]) ).
tff(c_116,plain,
store(a_1122,i28,e28) = a_1123,
inference(cnfTransformation,[status(thm)],[f_87]) ).
tff(c_1636,plain,
! [J_17] :
( ( select(a_1123,J_17) = select(a_1122,J_17) )
| ( i28 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_116,c_1467]) ).
tff(c_290,plain,
i30 != i17,
inference(cnfTransformation,[status(thm)],[f_253]) ).
tff(c_118,plain,
store(a_1123,i17,e17) = a_1124,
inference(cnfTransformation,[status(thm)],[f_88]) ).
tff(c_1639,plain,
! [J_17] :
( ( select(a_1124,J_17) = select(a_1123,J_17) )
| ( i17 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_118,c_1467]) ).
tff(c_10700,plain,
select(a_1124,i_1129) = e_1131,
inference(splitRight,[status(thm)],[c_10234]) ).
tff(c_10765,plain,
select(a_1124,i30) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_10763,c_10700]) ).
tff(c_10957,plain,
( ( select(a_1123,i30) = e_1131 )
| ( i30 = i17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1639,c_10765]) ).
tff(c_10965,plain,
select(a_1123,i30) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_290,c_10957]) ).
tff(c_11016,plain,
( ( select(a_1122,i30) = e_1131 )
| ( i30 = i28 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1636,c_10965]) ).
tff(c_11024,plain,
select(a_1122,i30) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_136,c_11016]) ).
tff(c_114,plain,
store(a_1121,i16,e16) = a_1122,
inference(cnfTransformation,[status(thm)],[f_86]) ).
tff(c_1564,plain,
! [J_17] :
( ( select(a_1122,J_17) = select(a_1121,J_17) )
| ( i16 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_114,c_1467]) ).
tff(c_11029,plain,
( ( select(a_1121,i30) = e_1131 )
| ( i30 = i16 ) ),
inference(superposition,[status(thm),theory(equality)],[c_11024,c_1564]) ).
tff(c_11047,plain,
select(a_1121,i30) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_316,c_11029]) ).
tff(c_112,plain,
store(a_1120,i12,e12) = a_1121,
inference(cnfTransformation,[status(thm)],[f_85]) ).
tff(c_1609,plain,
! [J_17] :
( ( select(a_1121,J_17) = select(a_1120,J_17) )
| ( i12 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_112,c_1467]) ).
tff(c_11058,plain,
( ( select(a_1120,i30) = e_1131 )
| ( i30 = i12 ) ),
inference(superposition,[status(thm),theory(equality)],[c_11047,c_1609]) ).
tff(c_11076,plain,
select(a_1120,i30) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_440,c_11058]) ).
tff(c_11103,plain,
( ( select(a_1119,i30) = e_1131 )
| ( i30 = i3 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1603,c_11076]) ).
tff(c_11111,plain,
select(a_1119,i30) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_836,c_11103]) ).
tff(c_108,plain,
store(a_1118,i27,e27) = a_1119,
inference(cnfTransformation,[status(thm)],[f_83]) ).
tff(c_1654,plain,
! [J_17] :
( ( select(a_1119,J_17) = select(a_1118,J_17) )
| ( i27 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_108,c_1467]) ).
tff(c_11145,plain,
( ( select(a_1118,i30) = e_1131 )
| ( i30 = i27 ) ),
inference(superposition,[status(thm),theory(equality)],[c_11111,c_1654]) ).
tff(c_11163,plain,
select(a_1118,i30) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_140,c_11145]) ).
tff(c_106,plain,
store(a_1117,i22,e22) = a_1118,
inference(cnfTransformation,[status(thm)],[f_82]) ).
tff(c_1483,plain,
! [J_17] :
( ( select(a_1118,J_17) = select(a_1117,J_17) )
| ( i22 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_106,c_1467]) ).
tff(c_11174,plain,
( ( select(a_1117,i30) = e_1131 )
| ( i30 = i22 ) ),
inference(superposition,[status(thm),theory(equality)],[c_11163,c_1483]) ).
tff(c_11192,plain,
select(a_1117,i30) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_190,c_11174]) ).
tff(c_11407,plain,
( ( select(a_1116,i30) = e_1131 )
| ( i30 = i26 ) ),
inference(superposition,[status(thm),theory(equality)],[c_11401,c_11192]) ).
tff(c_11433,plain,
select(a_1116,i30) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_146,c_11407]) ).
tff(c_102,plain,
store(a_1115,i5,e5) = a_1116,
inference(cnfTransformation,[status(thm)],[f_80]) ).
tff(c_1507,plain,
! [J_17] :
( ( select(a_1116,J_17) = select(a_1115,J_17) )
| ( i5 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_102,c_1467]) ).
tff(c_11441,plain,
( ( select(a_1115,i30) = e_1131 )
| ( i5 = i30 ) ),
inference(superposition,[status(thm),theory(equality)],[c_11433,c_1507]) ).
tff(c_11459,plain,
select(a_1115,i30) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_734,c_11441]) ).
tff(c_100,plain,
store(a_1114,i29,e29) = a_1115,
inference(cnfTransformation,[status(thm)],[f_79]) ).
tff(c_1546,plain,
! [J_17] :
( ( select(a_1115,J_17) = select(a_1114,J_17) )
| ( i29 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_100,c_1467]) ).
tff(c_11499,plain,
( ( select(a_1114,i30) = e_1131 )
| ( i30 = i29 ) ),
inference(superposition,[status(thm),theory(equality)],[c_11459,c_1546]) ).
tff(c_11517,plain,
select(a_1114,i30) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_134,c_11499]) ).
tff(c_11544,plain,
( ( select(a_1113,i30) = e_1131 )
| ( i30 = i14 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1606,c_11517]) ).
tff(c_11552,plain,
select(a_1113,i30) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_374,c_11544]) ).
tff(c_96,plain,
store(a_1112,i11,e11) = a_1113,
inference(cnfTransformation,[status(thm)],[f_77]) ).
tff(c_1585,plain,
! [J_17] :
( ( select(a_1113,J_17) = select(a_1112,J_17) )
| ( i11 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_96,c_1467]) ).
tff(c_11557,plain,
( ( select(a_1112,i30) = e_1131 )
| ( i30 = i11 ) ),
inference(superposition,[status(thm),theory(equality)],[c_11552,c_1585]) ).
tff(c_11575,plain,
select(a_1112,i30) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_476,c_11557]) ).
tff(c_94,plain,
store(a_1111,i6,e6) = a_1112,
inference(cnfTransformation,[status(thm)],[f_76]) ).
tff(c_1642,plain,
! [J_17] :
( ( select(a_1112,J_17) = select(a_1111,J_17) )
| ( i6 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_94,c_1467]) ).
tff(c_11586,plain,
( ( select(a_1111,i30) = e_1131 )
| ( i6 = i30 ) ),
inference(superposition,[status(thm),theory(equality)],[c_11575,c_1642]) ).
tff(c_11604,plain,
select(a_1111,i30) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_686,c_11586]) ).
tff(c_11631,plain,
( ( select(a_1110,i30) = e_1131 )
| ( i30 = i21 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1648,c_11604]) ).
tff(c_11639,plain,
select(a_1110,i30) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_206,c_11631]) ).
tff(c_90,plain,
store(a_1109,i8,e8) = a_1110,
inference(cnfTransformation,[status(thm)],[f_74]) ).
tff(c_1522,plain,
! [J_17] :
( ( select(a_1110,J_17) = select(a_1109,J_17) )
| ( i8 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_90,c_1467]) ).
tff(c_11673,plain,
( ( select(a_1109,i30) = e_1131 )
| ( i8 = i30 ) ),
inference(superposition,[status(thm),theory(equality)],[c_11639,c_1522]) ).
tff(c_11691,plain,
select(a_1109,i30) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_596,c_11673]) ).
tff(c_88,plain,
store(a_1108,i20,e20) = a_1109,
inference(cnfTransformation,[status(thm)],[f_73]) ).
tff(c_1633,plain,
! [J_17] :
( ( select(a_1109,J_17) = select(a_1108,J_17) )
| ( i20 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_88,c_1467]) ).
tff(c_11702,plain,
( ( select(a_1108,i30) = e_1131 )
| ( i30 = i20 ) ),
inference(superposition,[status(thm),theory(equality)],[c_11691,c_1633]) ).
tff(c_11720,plain,
select(a_1108,i30) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_224,c_11702]) ).
tff(c_86,plain,
store(a_1107,i18,e18) = a_1108,
inference(cnfTransformation,[status(thm)],[f_72]) ).
tff(c_1660,plain,
! [J_17] :
( ( select(a_1108,J_17) = select(a_1107,J_17) )
| ( i18 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_86,c_1467]) ).
tff(c_11731,plain,
( ( select(a_1107,i30) = e_1131 )
| ( i30 = i18 ) ),
inference(superposition,[status(thm),theory(equality)],[c_11720,c_1660]) ).
tff(c_11749,plain,
select(a_1107,i30) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_266,c_11731]) ).
tff(c_84,plain,
store(a_1106,i25,e25) = a_1107,
inference(cnfTransformation,[status(thm)],[f_71]) ).
tff(c_1612,plain,
! [J_17] :
( ( select(a_1107,J_17) = select(a_1106,J_17) )
| ( i25 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_84,c_1467]) ).
tff(c_11760,plain,
( ( select(a_1106,i30) = e_1131 )
| ( i30 = i25 ) ),
inference(superposition,[status(thm),theory(equality)],[c_11749,c_1612]) ).
tff(c_11778,plain,
select(a_1106,i30) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_154,c_11760]) ).
tff(c_82,plain,
store(a_1105,i15,e15) = a_1106,
inference(cnfTransformation,[status(thm)],[f_70]) ).
tff(c_1621,plain,
! [J_17] :
( ( select(a_1106,J_17) = select(a_1105,J_17) )
| ( i15 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_82,c_1467]) ).
tff(c_11818,plain,
( ( select(a_1105,i30) = e_1131 )
| ( i30 = i15 ) ),
inference(superposition,[status(thm),theory(equality)],[c_11778,c_1621]) ).
tff(c_11836,plain,
select(a_1105,i30) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_344,c_11818]) ).
tff(c_80,plain,
store(a_1104,i2,e2) = a_1105,
inference(cnfTransformation,[status(thm)],[f_69]) ).
tff(c_1600,plain,
! [J_17] :
( ( select(a_1105,J_17) = select(a_1104,J_17) )
| ( i2 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_80,c_1467]) ).
tff(c_11847,plain,
( ( select(a_1104,i30) = e_1131 )
| ( i30 = i2 ) ),
inference(superposition,[status(thm),theory(equality)],[c_11836,c_1600]) ).
tff(c_11865,plain,
( ( e_1131 = e30 )
| ( i30 = i2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1365,c_11847]) ).
tff(c_11867,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_890,c_10782,c_11865]) ).
tff(c_11868,plain,
select(a_1097,i_1129) = e_1130,
inference(splitRight,[status(thm)],[c_10723]) ).
tff(c_11893,plain,
( ( select(a_1096,i_1129) = e_1130 )
| ( i_1129 = i29 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1576,c_11868]) ).
tff(c_11930,plain,
i_1129 = i29,
inference(splitLeft,[status(thm)],[c_11893]) ).
tff(c_11931,plain,
select(a_1097,i29) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_11930,c_11868]) ).
tff(c_11944,plain,
e_1130 = e29,
inference(demodulation,[status(thm),theory(equality)],[c_1359,c_11931]) ).
tff(c_11977,plain,
e_1131 != e29,
inference(demodulation,[status(thm),theory(equality)],[c_11944,c_1004]) ).
tff(c_1329,plain,
select(a_1115,i29) = e29,
inference(superposition,[status(thm),theory(equality)],[c_100,c_1257]) ).
tff(c_148,plain,
i29 != i26,
inference(cnfTransformation,[status(thm)],[f_111]) ).
tff(c_192,plain,
i29 != i22,
inference(cnfTransformation,[status(thm)],[f_155]) ).
tff(c_142,plain,
i29 != i27,
inference(cnfTransformation,[status(thm)],[f_105]) ).
tff(c_838,plain,
i3 != i29,
inference(cnfTransformation,[status(thm)],[f_801]) ).
tff(c_442,plain,
i29 != i12,
inference(cnfTransformation,[status(thm)],[f_405]) ).
tff(c_318,plain,
i29 != i16,
inference(cnfTransformation,[status(thm)],[f_281]) ).
tff(c_138,plain,
i29 != i28,
inference(cnfTransformation,[status(thm)],[f_101]) ).
tff(c_292,plain,
i29 != i17,
inference(cnfTransformation,[status(thm)],[f_255]) ).
tff(c_11933,plain,
select(a_1124,i29) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_11930,c_10700]) ).
tff(c_12155,plain,
( ( select(a_1123,i29) = e_1131 )
| ( i29 = i17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1639,c_11933]) ).
tff(c_12163,plain,
select(a_1123,i29) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_292,c_12155]) ).
tff(c_12214,plain,
( ( select(a_1122,i29) = e_1131 )
| ( i29 = i28 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1636,c_12163]) ).
tff(c_12222,plain,
select(a_1122,i29) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_138,c_12214]) ).
tff(c_12227,plain,
( ( select(a_1121,i29) = e_1131 )
| ( i29 = i16 ) ),
inference(superposition,[status(thm),theory(equality)],[c_12222,c_1564]) ).
tff(c_12245,plain,
select(a_1121,i29) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_318,c_12227]) ).
tff(c_12256,plain,
( ( select(a_1120,i29) = e_1131 )
| ( i29 = i12 ) ),
inference(superposition,[status(thm),theory(equality)],[c_12245,c_1609]) ).
tff(c_12274,plain,
select(a_1120,i29) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_442,c_12256]) ).
tff(c_12301,plain,
( ( select(a_1119,i29) = e_1131 )
| ( i3 = i29 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1603,c_12274]) ).
tff(c_12309,plain,
select(a_1119,i29) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_838,c_12301]) ).
tff(c_12343,plain,
( ( select(a_1118,i29) = e_1131 )
| ( i29 = i27 ) ),
inference(superposition,[status(thm),theory(equality)],[c_12309,c_1654]) ).
tff(c_12361,plain,
select(a_1118,i29) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_142,c_12343]) ).
tff(c_12372,plain,
( ( select(a_1117,i29) = e_1131 )
| ( i29 = i22 ) ),
inference(superposition,[status(thm),theory(equality)],[c_12361,c_1483]) ).
tff(c_12390,plain,
select(a_1117,i29) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_192,c_12372]) ).
tff(c_1558,plain,
! [J_17] :
( ( select(a_1117,J_17) = select(a_1116,J_17) )
| ( i26 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_104,c_1467]) ).
tff(c_12401,plain,
( ( select(a_1116,i29) = e_1131 )
| ( i29 = i26 ) ),
inference(superposition,[status(thm),theory(equality)],[c_12390,c_1558]) ).
tff(c_12419,plain,
select(a_1116,i29) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_148,c_12401]) ).
tff(c_12430,plain,
( ( select(a_1115,i29) = e_1131 )
| ( i5 = i29 ) ),
inference(superposition,[status(thm),theory(equality)],[c_12419,c_1507]) ).
tff(c_12448,plain,
( ( e_1131 = e29 )
| ( i5 = i29 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1329,c_12430]) ).
tff(c_12450,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_736,c_11977,c_12448]) ).
tff(c_12451,plain,
select(a_1096,i_1129) = e_1130,
inference(splitRight,[status(thm)],[c_11893]) ).
tff(c_12485,plain,
( ( select(a_1095,i_1129) = e_1130 )
| ( i_1129 = i28 ) ),
inference(superposition,[status(thm),theory(equality)],[c_12451,c_1528]) ).
tff(c_12510,plain,
i_1129 = i28,
inference(splitLeft,[status(thm)],[c_12485]) ).
tff(c_12540,plain,
select(a_1096,i28) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_12510,c_12451]) ).
tff(c_12555,plain,
e_1130 = e28,
inference(demodulation,[status(thm),theory(equality)],[c_1311,c_12540]) ).
tff(c_12560,plain,
e_1131 != e28,
inference(demodulation,[status(thm),theory(equality)],[c_12555,c_1004]) ).
tff(c_1419,plain,
select(a_1123,i28) = e28,
inference(superposition,[status(thm),theory(equality)],[c_116,c_1257]) ).
tff(c_12546,plain,
select(a_1125,i28) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_12510,c_10229]) ).
tff(c_12615,plain,
( ( select(a_1124,i28) = e_1131 )
| ( i28 = i23 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1594,c_12546]) ).
tff(c_12623,plain,
select(a_1124,i28) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_180,c_12615]) ).
tff(c_12777,plain,
( ( select(a_1123,i28) = e_1131 )
| ( i28 = i17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_12623,c_1639]) ).
tff(c_12795,plain,
( ( e_1131 = e28 )
| ( i28 = i17 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1419,c_12777]) ).
tff(c_12797,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_294,c_12560,c_12795]) ).
tff(c_12798,plain,
select(a_1095,i_1129) = e_1130,
inference(splitRight,[status(thm)],[c_12485]) ).
tff(c_12819,plain,
( ( select(a_1094,i_1129) = e_1130 )
| ( i_1129 = i27 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1579,c_12798]) ).
tff(c_12859,plain,
i_1129 = i27,
inference(splitLeft,[status(thm)],[c_12819]) ).
tff(c_12860,plain,
select(a_1095,i27) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_12859,c_12798]) ).
tff(c_12877,plain,
e_1130 = e27,
inference(demodulation,[status(thm),theory(equality)],[c_1362,c_12860]) ).
tff(c_12886,plain,
e_1131 != e27,
inference(demodulation,[status(thm),theory(equality)],[c_12877,c_1004]) ).
tff(c_1437,plain,
select(a_1119,i27) = e27,
inference(superposition,[status(thm),theory(equality)],[c_108,c_1257]) ).
tff(c_446,plain,
i27 != i12,
inference(cnfTransformation,[status(thm)],[f_409]) ).
tff(c_322,plain,
i27 != i16,
inference(cnfTransformation,[status(thm)],[f_285]) ).
tff(c_144,plain,
i28 != i27,
inference(cnfTransformation,[status(thm)],[f_107]) ).
tff(c_296,plain,
i27 != i17,
inference(cnfTransformation,[status(thm)],[f_259]) ).
tff(c_12866,plain,
select(a_1124,i27) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_12859,c_10700]) ).
tff(c_13084,plain,
( ( select(a_1123,i27) = e_1131 )
| ( i27 = i17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1639,c_12866]) ).
tff(c_13092,plain,
select(a_1123,i27) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_296,c_13084]) ).
tff(c_13157,plain,
( ( select(a_1122,i27) = e_1131 )
| ( i28 = i27 ) ),
inference(superposition,[status(thm),theory(equality)],[c_13092,c_1636]) ).
tff(c_13175,plain,
select(a_1122,i27) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_144,c_13157]) ).
tff(c_13222,plain,
( ( select(a_1121,i27) = e_1131 )
| ( i27 = i16 ) ),
inference(superposition,[status(thm),theory(equality)],[c_13175,c_1564]) ).
tff(c_13240,plain,
select(a_1121,i27) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_322,c_13222]) ).
tff(c_13267,plain,
( ( select(a_1120,i27) = e_1131 )
| ( i27 = i12 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1609,c_13240]) ).
tff(c_13275,plain,
select(a_1120,i27) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_446,c_13267]) ).
tff(c_13309,plain,
( ( select(a_1119,i27) = e_1131 )
| ( i3 = i27 ) ),
inference(superposition,[status(thm),theory(equality)],[c_13275,c_1603]) ).
tff(c_13327,plain,
( ( e_1131 = e27 )
| ( i3 = i27 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1437,c_13309]) ).
tff(c_13329,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_842,c_12886,c_13327]) ).
tff(c_13330,plain,
select(a_1094,i_1129) = e_1130,
inference(splitRight,[status(thm)],[c_12819]) ).
tff(c_13380,plain,
( ( select(a_1093,i_1129) = e_1130 )
| ( i_1129 = i26 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1504,c_13330]) ).
tff(c_15254,plain,
i_1129 = i26,
inference(splitLeft,[status(thm)],[c_13380]) ).
tff(c_15287,plain,
select(a_1094,i26) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_15254,c_13330]) ).
tff(c_15306,plain,
e_1130 = e26,
inference(demodulation,[status(thm),theory(equality)],[c_1287,c_15287]) ).
tff(c_15311,plain,
e_1131 != e26,
inference(demodulation,[status(thm),theory(equality)],[c_15306,c_1004]) ).
tff(c_1341,plain,
select(a_1117,i26) = e26,
inference(superposition,[status(thm),theory(equality)],[c_104,c_1257]) ).
tff(c_152,plain,
i27 != i26,
inference(cnfTransformation,[status(thm)],[f_115]) ).
tff(c_844,plain,
i3 != i26,
inference(cnfTransformation,[status(thm)],[f_807]) ).
tff(c_448,plain,
i26 != i12,
inference(cnfTransformation,[status(thm)],[f_411]) ).
tff(c_324,plain,
i26 != i16,
inference(cnfTransformation,[status(thm)],[f_287]) ).
tff(c_150,plain,
i28 != i26,
inference(cnfTransformation,[status(thm)],[f_113]) ).
tff(c_314,plain,
i18 != i17,
inference(cnfTransformation,[status(thm)],[f_277]) ).
tff(c_1422,plain,
select(a_1124,i17) = e17,
inference(superposition,[status(thm),theory(equality)],[c_118,c_1257]) ).
tff(c_10756,plain,
( ( select(a_1123,i_1129) = e_1131 )
| ( i_1129 = i17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1639,c_10700]) ).
tff(c_13389,plain,
i_1129 = i17,
inference(splitLeft,[status(thm)],[c_10756]) ).
tff(c_13398,plain,
select(a_1124,i17) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_13389,c_10700]) ).
tff(c_13409,plain,
e_1131 = e17,
inference(demodulation,[status(thm),theory(equality)],[c_1422,c_13398]) ).
tff(c_13414,plain,
e_1130 != e17,
inference(demodulation,[status(thm),theory(equality)],[c_13409,c_1004]) ).
tff(c_1323,plain,
select(a_1085,i17) = e17,
inference(superposition,[status(thm),theory(equality)],[c_40,c_1257]) ).
tff(c_312,plain,
i19 != i17,
inference(cnfTransformation,[status(thm)],[f_275]) ).
tff(c_310,plain,
i20 != i17,
inference(cnfTransformation,[status(thm)],[f_273]) ).
tff(c_308,plain,
i21 != i17,
inference(cnfTransformation,[status(thm)],[f_271]) ).
tff(c_306,plain,
i22 != i17,
inference(cnfTransformation,[status(thm)],[f_269]) ).
tff(c_304,plain,
i23 != i17,
inference(cnfTransformation,[status(thm)],[f_267]) ).
tff(c_14011,plain,
! [J_190] :
( ( select(a_1091,J_190) = select(a_1090,J_190) )
| ( i23 = J_190 ) ),
inference(superposition,[status(thm),theory(equality)],[c_52,c_1467]) ).
tff(c_302,plain,
i24 != i17,
inference(cnfTransformation,[status(thm)],[f_265]) ).
tff(c_300,plain,
i25 != i17,
inference(cnfTransformation,[status(thm)],[f_263]) ).
tff(c_298,plain,
i26 != i17,
inference(cnfTransformation,[status(thm)],[f_261]) ).
tff(c_13390,plain,
select(a_1094,i17) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_13389,c_13330]) ).
tff(c_13615,plain,
( ( select(a_1093,i17) = e_1130 )
| ( i26 = i17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1504,c_13390]) ).
tff(c_13623,plain,
select(a_1093,i17) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_298,c_13615]) ).
tff(c_13748,plain,
( ( select(a_1092,i17) = e_1130 )
| ( i25 = i17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_13623,c_1549]) ).
tff(c_13766,plain,
select(a_1092,i17) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_300,c_13748]) ).
tff(c_13814,plain,
( ( select(a_1091,i17) = e_1130 )
| ( i24 = i17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_13766,c_1588]) ).
tff(c_13832,plain,
select(a_1091,i17) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_302,c_13814]) ).
tff(c_14017,plain,
( ( select(a_1090,i17) = e_1130 )
| ( i23 = i17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_14011,c_13832]) ).
tff(c_14043,plain,
select(a_1090,i17) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_304,c_14017]) ).
tff(c_14051,plain,
( ( select(a_1089,i17) = e_1130 )
| ( i22 = i17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_14043,c_1624]) ).
tff(c_14069,plain,
select(a_1089,i17) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_306,c_14051]) ).
tff(c_14096,plain,
( ( select(a_1088,i17) = e_1130 )
| ( i21 = i17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1537,c_14069]) ).
tff(c_14104,plain,
select(a_1088,i17) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_308,c_14096]) ).
tff(c_15072,plain,
( ( select(a_1087,i17) = e_1130 )
| ( i20 = i17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_14104,c_1552]) ).
tff(c_15091,plain,
select(a_1087,i17) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_310,c_15072]) ).
tff(c_15108,plain,
( ( select(a_1086,i17) = e_1130 )
| ( i19 = i17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_15091,c_1573]) ).
tff(c_15127,plain,
select(a_1086,i17) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_312,c_15108]) ).
tff(c_15144,plain,
( ( select(a_1085,i17) = e_1130 )
| ( i18 = i17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_15127,c_1525]) ).
tff(c_15163,plain,
( ( e_1130 = e17 )
| ( i18 = i17 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1323,c_15144]) ).
tff(c_15165,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_314,c_13414,c_15163]) ).
tff(c_15166,plain,
select(a_1123,i_1129) = e_1131,
inference(splitRight,[status(thm)],[c_10756]) ).
tff(c_15285,plain,
select(a_1123,i26) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_15254,c_15166]) ).
tff(c_15397,plain,
( ( select(a_1122,i26) = e_1131 )
| ( i28 = i26 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1636,c_15285]) ).
tff(c_15405,plain,
select(a_1122,i26) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_150,c_15397]) ).
tff(c_15696,plain,
( ( select(a_1121,i26) = e_1131 )
| ( i26 = i16 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1564,c_15405]) ).
tff(c_15704,plain,
select(a_1121,i26) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_324,c_15696]) ).
tff(c_15756,plain,
( ( select(a_1120,i26) = e_1131 )
| ( i26 = i12 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1609,c_15704]) ).
tff(c_15764,plain,
select(a_1120,i26) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_448,c_15756]) ).
tff(c_15770,plain,
( ( select(a_1119,i26) = e_1131 )
| ( i3 = i26 ) ),
inference(superposition,[status(thm),theory(equality)],[c_15764,c_1603]) ).
tff(c_15788,plain,
select(a_1119,i26) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_844,c_15770]) ).
tff(c_15799,plain,
( ( select(a_1118,i26) = e_1131 )
| ( i27 = i26 ) ),
inference(superposition,[status(thm),theory(equality)],[c_15788,c_1654]) ).
tff(c_15817,plain,
select(a_1118,i26) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_152,c_15799]) ).
tff(c_15828,plain,
( ( select(a_1117,i26) = e_1131 )
| ( i26 = i22 ) ),
inference(superposition,[status(thm),theory(equality)],[c_15817,c_1483]) ).
tff(c_15846,plain,
( ( e_1131 = e26 )
| ( i26 = i22 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1341,c_15828]) ).
tff(c_15848,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_198,c_15311,c_15846]) ).
tff(c_15849,plain,
select(a_1093,i_1129) = e_1130,
inference(splitRight,[status(thm)],[c_13380]) ).
tff(c_15883,plain,
( ( select(a_1092,i_1129) = e_1130 )
| ( i_1129 = i25 ) ),
inference(superposition,[status(thm),theory(equality)],[c_15849,c_1549]) ).
tff(c_15937,plain,
i_1129 = i25,
inference(splitLeft,[status(thm)],[c_15883]) ).
tff(c_15938,plain,
select(a_1093,i25) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_15937,c_15849]) ).
tff(c_15962,plain,
e_1130 = e25,
inference(demodulation,[status(thm),theory(equality)],[c_1332,c_15938]) ).
tff(c_15967,plain,
e_1131 != e25,
inference(demodulation,[status(thm),theory(equality)],[c_15962,c_1004]) ).
tff(c_1395,plain,
select(a_1107,i25) = e25,
inference(superposition,[status(thm),theory(equality)],[c_84,c_1257]) ).
tff(c_234,plain,
i25 != i20,
inference(cnfTransformation,[status(thm)],[f_197]) ).
tff(c_606,plain,
i8 != i25,
inference(cnfTransformation,[status(thm)],[f_569]) ).
tff(c_216,plain,
i25 != i21,
inference(cnfTransformation,[status(thm)],[f_179]) ).
tff(c_696,plain,
i6 != i25,
inference(cnfTransformation,[status(thm)],[f_659]) ).
tff(c_486,plain,
i25 != i11,
inference(cnfTransformation,[status(thm)],[f_449]) ).
tff(c_384,plain,
i25 != i14,
inference(cnfTransformation,[status(thm)],[f_347]) ).
tff(c_156,plain,
i29 != i25,
inference(cnfTransformation,[status(thm)],[f_119]) ).
tff(c_744,plain,
i5 != i25,
inference(cnfTransformation,[status(thm)],[f_707]) ).
tff(c_162,plain,
i26 != i25,
inference(cnfTransformation,[status(thm)],[f_125]) ).
tff(c_200,plain,
i25 != i22,
inference(cnfTransformation,[status(thm)],[f_163]) ).
tff(c_160,plain,
i27 != i25,
inference(cnfTransformation,[status(thm)],[f_123]) ).
tff(c_846,plain,
i3 != i25,
inference(cnfTransformation,[status(thm)],[f_809]) ).
tff(c_450,plain,
i25 != i12,
inference(cnfTransformation,[status(thm)],[f_413]) ).
tff(c_326,plain,
i25 != i16,
inference(cnfTransformation,[status(thm)],[f_289]) ).
tff(c_12799,plain,
i_1129 != i28,
inference(splitRight,[status(thm)],[c_12485]) ).
tff(c_15171,plain,
( ( select(a_1122,i_1129) = e_1131 )
| ( i_1129 = i28 ) ),
inference(superposition,[status(thm),theory(equality)],[c_15166,c_1636]) ).
tff(c_15189,plain,
select(a_1122,i_1129) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_12799,c_15171]) ).
tff(c_15940,plain,
select(a_1122,i25) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_15937,c_15189]) ).
tff(c_16140,plain,
( ( select(a_1121,i25) = e_1131 )
| ( i25 = i16 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1564,c_15940]) ).
tff(c_16148,plain,
select(a_1121,i25) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_326,c_16140]) ).
tff(c_16360,plain,
( ( select(a_1120,i25) = e_1131 )
| ( i25 = i12 ) ),
inference(superposition,[status(thm),theory(equality)],[c_16148,c_1609]) ).
tff(c_16378,plain,
select(a_1120,i25) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_450,c_16360]) ).
tff(c_16457,plain,
( ( select(a_1119,i25) = e_1131 )
| ( i3 = i25 ) ),
inference(superposition,[status(thm),theory(equality)],[c_16378,c_1603]) ).
tff(c_16475,plain,
select(a_1119,i25) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_846,c_16457]) ).
tff(c_16502,plain,
( ( select(a_1118,i25) = e_1131 )
| ( i27 = i25 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1654,c_16475]) ).
tff(c_16510,plain,
select(a_1118,i25) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_160,c_16502]) ).
tff(c_16544,plain,
( ( select(a_1117,i25) = e_1131 )
| ( i25 = i22 ) ),
inference(superposition,[status(thm),theory(equality)],[c_16510,c_1483]) ).
tff(c_16562,plain,
select(a_1117,i25) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_200,c_16544]) ).
tff(c_16573,plain,
( ( select(a_1116,i25) = e_1131 )
| ( i26 = i25 ) ),
inference(superposition,[status(thm),theory(equality)],[c_16562,c_1558]) ).
tff(c_16591,plain,
select(a_1116,i25) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_162,c_16573]) ).
tff(c_16602,plain,
( ( select(a_1115,i25) = e_1131 )
| ( i5 = i25 ) ),
inference(superposition,[status(thm),theory(equality)],[c_16591,c_1507]) ).
tff(c_16620,plain,
select(a_1115,i25) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_744,c_16602]) ).
tff(c_16631,plain,
( ( select(a_1114,i25) = e_1131 )
| ( i29 = i25 ) ),
inference(superposition,[status(thm),theory(equality)],[c_16620,c_1546]) ).
tff(c_16649,plain,
select(a_1114,i25) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_156,c_16631]) ).
tff(c_16689,plain,
( ( select(a_1113,i25) = e_1131 )
| ( i25 = i14 ) ),
inference(superposition,[status(thm),theory(equality)],[c_16649,c_1606]) ).
tff(c_16707,plain,
select(a_1113,i25) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_384,c_16689]) ).
tff(c_16734,plain,
( ( select(a_1112,i25) = e_1131 )
| ( i25 = i11 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1585,c_16707]) ).
tff(c_16742,plain,
select(a_1112,i25) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_486,c_16734]) ).
tff(c_16747,plain,
( ( select(a_1111,i25) = e_1131 )
| ( i6 = i25 ) ),
inference(superposition,[status(thm),theory(equality)],[c_16742,c_1642]) ).
tff(c_16765,plain,
select(a_1111,i25) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_696,c_16747]) ).
tff(c_16776,plain,
( ( select(a_1110,i25) = e_1131 )
| ( i25 = i21 ) ),
inference(superposition,[status(thm),theory(equality)],[c_16765,c_1648]) ).
tff(c_16794,plain,
select(a_1110,i25) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_216,c_16776]) ).
tff(c_16821,plain,
( ( select(a_1109,i25) = e_1131 )
| ( i8 = i25 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1522,c_16794]) ).
tff(c_16829,plain,
select(a_1109,i25) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_606,c_16821]) ).
tff(c_16863,plain,
( ( select(a_1108,i25) = e_1131 )
| ( i25 = i20 ) ),
inference(superposition,[status(thm),theory(equality)],[c_16829,c_1633]) ).
tff(c_16881,plain,
select(a_1108,i25) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_234,c_16863]) ).
tff(c_16892,plain,
( ( select(a_1107,i25) = e_1131 )
| ( i25 = i18 ) ),
inference(superposition,[status(thm),theory(equality)],[c_16881,c_1660]) ).
tff(c_16910,plain,
( ( e_1131 = e25 )
| ( i25 = i18 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1395,c_16892]) ).
tff(c_16912,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_276,c_15967,c_16910]) ).
tff(c_16913,plain,
select(a_1092,i_1129) = e_1130,
inference(splitRight,[status(thm)],[c_15883]) ).
tff(c_16918,plain,
( ( select(a_1091,i_1129) = e_1130 )
| ( i_1129 = i24 ) ),
inference(superposition,[status(thm),theory(equality)],[c_16913,c_1588]) ).
tff(c_16936,plain,
select(a_1091,i_1129) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_10230,c_16918]) ).
tff(c_16972,plain,
( ( select(a_1090,i_1129) = e_1130 )
| ( i_1129 = i23 ) ),
inference(superposition,[status(thm),theory(equality)],[c_16966,c_16936]) ).
tff(c_16998,plain,
select(a_1090,i_1129) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_10701,c_16972]) ).
tff(c_17006,plain,
( ( select(a_1089,i_1129) = e_1130 )
| ( i_1129 = i22 ) ),
inference(superposition,[status(thm),theory(equality)],[c_16998,c_1624]) ).
tff(c_19837,plain,
i_1129 = i22,
inference(splitLeft,[status(thm)],[c_17006]) ).
tff(c_19871,plain,
select(a_1090,i22) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_19837,c_16998]) ).
tff(c_19899,plain,
e_1130 = e22,
inference(demodulation,[status(thm),theory(equality)],[c_1407,c_19871]) ).
tff(c_19904,plain,
e_1131 != e22,
inference(demodulation,[status(thm),theory(equality)],[c_19899,c_1004]) ).
tff(c_1266,plain,
select(a_1118,i22) = e22,
inference(superposition,[status(thm),theory(equality)],[c_106,c_1257]) ).
tff(c_852,plain,
i3 != i22,
inference(cnfTransformation,[status(thm)],[f_815]) ).
tff(c_474,plain,
i13 != i12,
inference(cnfTransformation,[status(thm)],[f_437]) ).
tff(c_1392,plain,
select(a_1121,i12) = e12,
inference(superposition,[status(thm),theory(equality)],[c_112,c_1257]) ).
tff(c_342,plain,
i17 != i16,
inference(cnfTransformation,[status(thm)],[f_305]) ).
tff(c_1347,plain,
select(a_1122,i16) = e16,
inference(superposition,[status(thm),theory(equality)],[c_114,c_1257]) ).
tff(c_15215,plain,
( ( select(a_1121,i_1129) = e_1131 )
| ( i_1129 = i16 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1564,c_15189]) ).
tff(c_17030,plain,
i_1129 = i16,
inference(splitLeft,[status(thm)],[c_15215]) ).
tff(c_17066,plain,
select(a_1122,i16) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_17030,c_15189]) ).
tff(c_17088,plain,
e_1131 = e16,
inference(demodulation,[status(thm),theory(equality)],[c_1347,c_17066]) ).
tff(c_17093,plain,
e_1130 != e16,
inference(demodulation,[status(thm),theory(equality)],[c_17088,c_1004]) ).
tff(c_1272,plain,
select(a_1084,i16) = e16,
inference(superposition,[status(thm),theory(equality)],[c_38,c_1257]) ).
tff(c_340,plain,
i18 != i16,
inference(cnfTransformation,[status(thm)],[f_303]) ).
tff(c_338,plain,
i19 != i16,
inference(cnfTransformation,[status(thm)],[f_301]) ).
tff(c_336,plain,
i20 != i16,
inference(cnfTransformation,[status(thm)],[f_299]) ).
tff(c_334,plain,
i21 != i16,
inference(cnfTransformation,[status(thm)],[f_297]) ).
tff(c_332,plain,
i22 != i16,
inference(cnfTransformation,[status(thm)],[f_295]) ).
tff(c_17060,plain,
select(a_1090,i16) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_17030,c_16998]) ).
tff(c_17584,plain,
( ( select(a_1089,i16) = e_1130 )
| ( i22 = i16 ) ),
inference(superposition,[status(thm),theory(equality)],[c_17060,c_1624]) ).
tff(c_17602,plain,
select(a_1089,i16) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_332,c_17584]) ).
tff(c_17646,plain,
( ( select(a_1088,i16) = e_1130 )
| ( i21 = i16 ) ),
inference(superposition,[status(thm),theory(equality)],[c_17602,c_1537]) ).
tff(c_17664,plain,
select(a_1088,i16) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_334,c_17646]) ).
tff(c_17675,plain,
( ( select(a_1087,i16) = e_1130 )
| ( i20 = i16 ) ),
inference(superposition,[status(thm),theory(equality)],[c_17664,c_1552]) ).
tff(c_17693,plain,
select(a_1087,i16) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_336,c_17675]) ).
tff(c_17720,plain,
( ( select(a_1086,i16) = e_1130 )
| ( i19 = i16 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1573,c_17693]) ).
tff(c_17728,plain,
select(a_1086,i16) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_338,c_17720]) ).
tff(c_17762,plain,
( ( select(a_1085,i16) = e_1130 )
| ( i18 = i16 ) ),
inference(superposition,[status(thm),theory(equality)],[c_17728,c_1525]) ).
tff(c_17780,plain,
select(a_1085,i16) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_340,c_17762]) ).
tff(c_17791,plain,
( ( select(a_1084,i16) = e_1130 )
| ( i17 = i16 ) ),
inference(superposition,[status(thm),theory(equality)],[c_17780,c_1540]) ).
tff(c_17809,plain,
( ( e_1130 = e16 )
| ( i17 = i16 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1272,c_17791]) ).
tff(c_17811,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_342,c_17093,c_17809]) ).
tff(c_17812,plain,
select(a_1121,i_1129) = e_1131,
inference(splitRight,[status(thm)],[c_15215]) ).
tff(c_17817,plain,
( ( select(a_1120,i_1129) = e_1131 )
| ( i_1129 = i12 ) ),
inference(superposition,[status(thm),theory(equality)],[c_17812,c_1609]) ).
tff(c_17842,plain,
i_1129 = i12,
inference(splitLeft,[status(thm)],[c_17817]) ).
tff(c_17843,plain,
select(a_1121,i12) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_17842,c_17812]) ).
tff(c_17873,plain,
e_1131 = e12,
inference(demodulation,[status(thm),theory(equality)],[c_1392,c_17843]) ).
tff(c_17907,plain,
e_1130 != e12,
inference(demodulation,[status(thm),theory(equality)],[c_17873,c_1004]) ).
tff(c_1314,plain,
select(a_1080,i12) = e12,
inference(superposition,[status(thm),theory(equality)],[c_30,c_1257]) ).
tff(c_472,plain,
i14 != i12,
inference(cnfTransformation,[status(thm)],[f_435]) ).
tff(c_470,plain,
i15 != i12,
inference(cnfTransformation,[status(thm)],[f_433]) ).
tff(c_468,plain,
i16 != i12,
inference(cnfTransformation,[status(thm)],[f_431]) ).
tff(c_466,plain,
i17 != i12,
inference(cnfTransformation,[status(thm)],[f_429]) ).
tff(c_464,plain,
i18 != i12,
inference(cnfTransformation,[status(thm)],[f_427]) ).
tff(c_462,plain,
i19 != i12,
inference(cnfTransformation,[status(thm)],[f_425]) ).
tff(c_460,plain,
i20 != i12,
inference(cnfTransformation,[status(thm)],[f_423]) ).
tff(c_458,plain,
i21 != i12,
inference(cnfTransformation,[status(thm)],[f_421]) ).
tff(c_456,plain,
i22 != i12,
inference(cnfTransformation,[status(thm)],[f_419]) ).
tff(c_17845,plain,
select(a_1090,i12) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_17842,c_16998]) ).
tff(c_17992,plain,
( ( select(a_1089,i12) = e_1130 )
| ( i22 = i12 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1624,c_17845]) ).
tff(c_18000,plain,
select(a_1089,i12) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_456,c_17992]) ).
tff(c_18212,plain,
( ( select(a_1088,i12) = e_1130 )
| ( i21 = i12 ) ),
inference(superposition,[status(thm),theory(equality)],[c_18000,c_1537]) ).
tff(c_18230,plain,
select(a_1088,i12) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_458,c_18212]) ).
tff(c_18536,plain,
( ( select(a_1087,i12) = e_1130 )
| ( i20 = i12 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1552,c_18230]) ).
tff(c_18544,plain,
select(a_1087,i12) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_460,c_18536]) ).
tff(c_18578,plain,
( ( select(a_1086,i12) = e_1130 )
| ( i19 = i12 ) ),
inference(superposition,[status(thm),theory(equality)],[c_18544,c_1573]) ).
tff(c_18596,plain,
select(a_1086,i12) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_462,c_18578]) ).
tff(c_18607,plain,
( ( select(a_1085,i12) = e_1130 )
| ( i18 = i12 ) ),
inference(superposition,[status(thm),theory(equality)],[c_18596,c_1525]) ).
tff(c_18625,plain,
select(a_1085,i12) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_464,c_18607]) ).
tff(c_18636,plain,
( ( select(a_1084,i12) = e_1130 )
| ( i17 = i12 ) ),
inference(superposition,[status(thm),theory(equality)],[c_18625,c_1540]) ).
tff(c_18654,plain,
select(a_1084,i12) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_466,c_18636]) ).
tff(c_18665,plain,
( ( select(a_1083,i12) = e_1130 )
| ( i16 = i12 ) ),
inference(superposition,[status(thm),theory(equality)],[c_18654,c_1489]) ).
tff(c_18683,plain,
select(a_1083,i12) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_468,c_18665]) ).
tff(c_19713,plain,
( ( select(a_1082,i12) = e_1130 )
| ( i15 = i12 ) ),
inference(superposition,[status(thm),theory(equality)],[c_18683,c_1630]) ).
tff(c_19732,plain,
select(a_1082,i12) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_470,c_19713]) ).
tff(c_19765,plain,
( ( select(a_1081,i12) = e_1130 )
| ( i14 = i12 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1645,c_19732]) ).
tff(c_19774,plain,
select(a_1081,i12) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_472,c_19765]) ).
tff(c_19785,plain,
( ( select(a_1080,i12) = e_1130 )
| ( i13 = i12 ) ),
inference(superposition,[status(thm),theory(equality)],[c_19774,c_1597]) ).
tff(c_19804,plain,
( ( e_1130 = e12 )
| ( i13 = i12 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1314,c_19785]) ).
tff(c_19806,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_474,c_17907,c_19804]) ).
tff(c_19807,plain,
select(a_1120,i_1129) = e_1131,
inference(splitRight,[status(thm)],[c_17817]) ).
tff(c_19867,plain,
select(a_1120,i22) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_19837,c_19807]) ).
tff(c_20132,plain,
( ( select(a_1119,i22) = e_1131 )
| ( i3 = i22 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1603,c_19867]) ).
tff(c_20140,plain,
select(a_1119,i22) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_852,c_20132]) ).
tff(c_20473,plain,
( ( select(a_1118,i22) = e_1131 )
| ( i27 = i22 ) ),
inference(superposition,[status(thm),theory(equality)],[c_20140,c_1654]) ).
tff(c_20491,plain,
( ( e_1131 = e22 )
| ( i27 = i22 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1266,c_20473]) ).
tff(c_20493,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_196,c_19904,c_20491]) ).
tff(c_20494,plain,
select(a_1089,i_1129) = e_1130,
inference(splitRight,[status(thm)],[c_17006]) ).
tff(c_20515,plain,
( ( select(a_1088,i_1129) = e_1130 )
| ( i_1129 = i21 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1537,c_20494]) ).
tff(c_23025,plain,
i_1129 = i21,
inference(splitLeft,[status(thm)],[c_20515]) ).
tff(c_23030,plain,
select(a_1089,i21) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_23025,c_20494]) ).
tff(c_23064,plain,
e_1130 = e21,
inference(demodulation,[status(thm),theory(equality)],[c_1320,c_23030]) ).
tff(c_23069,plain,
e_1131 != e21,
inference(demodulation,[status(thm),theory(equality)],[c_23064,c_1004]) ).
tff(c_1431,plain,
select(a_1111,i21) = e21,
inference(superposition,[status(thm),theory(equality)],[c_92,c_1257]) ).
tff(c_494,plain,
i21 != i11,
inference(cnfTransformation,[status(thm)],[f_457]) ).
tff(c_392,plain,
i21 != i14,
inference(cnfTransformation,[status(thm)],[f_355]) ).
tff(c_208,plain,
i29 != i21,
inference(cnfTransformation,[status(thm)],[f_171]) ).
tff(c_752,plain,
i5 != i21,
inference(cnfTransformation,[status(thm)],[f_715]) ).
tff(c_214,plain,
i26 != i21,
inference(cnfTransformation,[status(thm)],[f_177]) ).
tff(c_222,plain,
i22 != i21,
inference(cnfTransformation,[status(thm)],[f_185]) ).
tff(c_13331,plain,
i_1129 != i27,
inference(splitRight,[status(thm)],[c_12819]) ).
tff(c_888,plain,
i4 != i3,
inference(cnfTransformation,[status(thm)],[f_851]) ).
tff(c_1386,plain,
select(a_1120,i3) = e3,
inference(superposition,[status(thm),theory(equality)],[c_110,c_1257]) ).
tff(c_19812,plain,
( ( select(a_1119,i_1129) = e_1131 )
| ( i_1129 = i3 ) ),
inference(superposition,[status(thm),theory(equality)],[c_19807,c_1603]) ).
tff(c_20553,plain,
i_1129 = i3,
inference(splitLeft,[status(thm)],[c_19812]) ).
tff(c_20556,plain,
select(a_1120,i3) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_20553,c_19807]) ).
tff(c_20588,plain,
e_1131 = e3,
inference(demodulation,[status(thm),theory(equality)],[c_1386,c_20556]) ).
tff(c_20593,plain,
e_1130 != e3,
inference(demodulation,[status(thm),theory(equality)],[c_20588,c_1004]) ).
tff(c_12,plain,
store(a_1070,i3,e3) = a_1071,
inference(cnfTransformation,[status(thm)],[f_35]) ).
tff(c_1275,plain,
select(a_1071,i3) = e3,
inference(superposition,[status(thm),theory(equality)],[c_12,c_1257]) ).
tff(c_886,plain,
i5 != i3,
inference(cnfTransformation,[status(thm)],[f_849]) ).
tff(c_884,plain,
i6 != i3,
inference(cnfTransformation,[status(thm)],[f_847]) ).
tff(c_18,plain,
store(a_1073,i6,e6) = a_1074,
inference(cnfTransformation,[status(thm)],[f_38]) ).
tff(c_1486,plain,
! [J_17] :
( ( select(a_1074,J_17) = select(a_1073,J_17) )
| ( i6 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_18,c_1467]) ).
tff(c_882,plain,
i7 != i3,
inference(cnfTransformation,[status(thm)],[f_845]) ).
tff(c_1510,plain,
! [J_17] :
( ( select(a_1075,J_17) = select(a_1074,J_17) )
| ( i7 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_20,c_1467]) ).
tff(c_880,plain,
i8 != i3,
inference(cnfTransformation,[status(thm)],[f_843]) ).
tff(c_878,plain,
i9 != i3,
inference(cnfTransformation,[status(thm)],[f_841]) ).
tff(c_876,plain,
i3 != i10,
inference(cnfTransformation,[status(thm)],[f_839]) ).
tff(c_874,plain,
i3 != i11,
inference(cnfTransformation,[status(thm)],[f_837]) ).
tff(c_872,plain,
i3 != i12,
inference(cnfTransformation,[status(thm)],[f_835]) ).
tff(c_870,plain,
i3 != i13,
inference(cnfTransformation,[status(thm)],[f_833]) ).
tff(c_868,plain,
i3 != i14,
inference(cnfTransformation,[status(thm)],[f_831]) ).
tff(c_866,plain,
i3 != i15,
inference(cnfTransformation,[status(thm)],[f_829]) ).
tff(c_864,plain,
i3 != i16,
inference(cnfTransformation,[status(thm)],[f_827]) ).
tff(c_862,plain,
i3 != i17,
inference(cnfTransformation,[status(thm)],[f_825]) ).
tff(c_860,plain,
i3 != i18,
inference(cnfTransformation,[status(thm)],[f_823]) ).
tff(c_858,plain,
i3 != i19,
inference(cnfTransformation,[status(thm)],[f_821]) ).
tff(c_856,plain,
i3 != i20,
inference(cnfTransformation,[status(thm)],[f_819]) ).
tff(c_854,plain,
i3 != i21,
inference(cnfTransformation,[status(thm)],[f_817]) ).
tff(c_20554,plain,
select(a_1089,i3) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_20553,c_20494]) ).
tff(c_20793,plain,
( ( select(a_1088,i3) = e_1130 )
| ( i3 = i21 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1537,c_20554]) ).
tff(c_20801,plain,
select(a_1088,i3) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_854,c_20793]) ).
tff(c_21220,plain,
( ( select(a_1087,i3) = e_1130 )
| ( i3 = i20 ) ),
inference(superposition,[status(thm),theory(equality)],[c_20801,c_1552]) ).
tff(c_21238,plain,
select(a_1087,i3) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_856,c_21220]) ).
tff(c_22310,plain,
( ( select(a_1086,i3) = e_1130 )
| ( i3 = i19 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1573,c_21238]) ).
tff(c_22319,plain,
select(a_1086,i3) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_858,c_22310]) ).
tff(c_22330,plain,
( ( select(a_1085,i3) = e_1130 )
| ( i3 = i18 ) ),
inference(superposition,[status(thm),theory(equality)],[c_22319,c_1525]) ).
tff(c_22349,plain,
select(a_1085,i3) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_860,c_22330]) ).
tff(c_22366,plain,
( ( select(a_1084,i3) = e_1130 )
| ( i3 = i17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_22349,c_1540]) ).
tff(c_22385,plain,
select(a_1084,i3) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_862,c_22366]) ).
tff(c_22418,plain,
( ( select(a_1083,i3) = e_1130 )
| ( i3 = i16 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1489,c_22385]) ).
tff(c_22427,plain,
select(a_1083,i3) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_864,c_22418]) ).
tff(c_22439,plain,
( ( select(a_1082,i3) = e_1130 )
| ( i3 = i15 ) ),
inference(superposition,[status(thm),theory(equality)],[c_22427,c_1630]) ).
tff(c_22458,plain,
select(a_1082,i3) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_866,c_22439]) ).
tff(c_22475,plain,
( ( select(a_1081,i3) = e_1130 )
| ( i3 = i14 ) ),
inference(superposition,[status(thm),theory(equality)],[c_22458,c_1645]) ).
tff(c_22494,plain,
select(a_1081,i3) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_868,c_22475]) ).
tff(c_22511,plain,
( ( select(a_1080,i3) = e_1130 )
| ( i3 = i13 ) ),
inference(superposition,[status(thm),theory(equality)],[c_22494,c_1597]) ).
tff(c_22530,plain,
select(a_1080,i3) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_870,c_22511]) ).
tff(c_22547,plain,
( ( select(a_1079,i3) = e_1130 )
| ( i3 = i12 ) ),
inference(superposition,[status(thm),theory(equality)],[c_22530,c_1531]) ).
tff(c_22566,plain,
select(a_1079,i3) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_872,c_22547]) ).
tff(c_22610,plain,
( ( select(a_1078,i3) = e_1130 )
| ( i3 = i11 ) ),
inference(superposition,[status(thm),theory(equality)],[c_22566,c_1543]) ).
tff(c_22629,plain,
select(a_1078,i3) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_874,c_22610]) ).
tff(c_22662,plain,
( ( select(a_1077,i3) = e_1130 )
| ( i3 = i10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1567,c_22629]) ).
tff(c_22671,plain,
select(a_1077,i3) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_876,c_22662]) ).
tff(c_22682,plain,
( ( select(a_1076,i3) = e_1130 )
| ( i9 = i3 ) ),
inference(superposition,[status(thm),theory(equality)],[c_22671,c_1591]) ).
tff(c_22701,plain,
select(a_1076,i3) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_878,c_22682]) ).
tff(c_22718,plain,
( ( select(a_1075,i3) = e_1130 )
| ( i8 = i3 ) ),
inference(superposition,[status(thm),theory(equality)],[c_22701,c_1651]) ).
tff(c_22737,plain,
select(a_1075,i3) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_880,c_22718]) ).
tff(c_22770,plain,
( ( select(a_1074,i3) = e_1130 )
| ( i7 = i3 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1510,c_22737]) ).
tff(c_22779,plain,
select(a_1074,i3) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_882,c_22770]) ).
tff(c_22807,plain,
( ( select(a_1073,i3) = e_1130 )
| ( i6 = i3 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1486,c_22779]) ).
tff(c_22816,plain,
select(a_1073,i3) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_884,c_22807]) ).
tff(c_16,plain,
store(a_1072,i5,e5) = a_1073,
inference(cnfTransformation,[status(thm)],[f_37]) ).
tff(c_1519,plain,
! [J_17] :
( ( select(a_1073,J_17) = select(a_1072,J_17) )
| ( i5 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_16,c_1467]) ).
tff(c_22827,plain,
( ( select(a_1072,i3) = e_1130 )
| ( i5 = i3 ) ),
inference(superposition,[status(thm),theory(equality)],[c_22816,c_1519]) ).
tff(c_22846,plain,
select(a_1072,i3) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_886,c_22827]) ).
tff(c_14,plain,
store(a_1071,i4,e4) = a_1072,
inference(cnfTransformation,[status(thm)],[f_36]) ).
tff(c_1516,plain,
! [J_17] :
( ( select(a_1072,J_17) = select(a_1071,J_17) )
| ( i4 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_14,c_1467]) ).
tff(c_22863,plain,
( ( select(a_1071,i3) = e_1130 )
| ( i4 = i3 ) ),
inference(superposition,[status(thm),theory(equality)],[c_22846,c_1516]) ).
tff(c_22882,plain,
( ( e_1130 = e3 )
| ( i4 = i3 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1275,c_22863]) ).
tff(c_22884,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_888,c_20593,c_22882]) ).
tff(c_22885,plain,
select(a_1119,i_1129) = e_1131,
inference(splitRight,[status(thm)],[c_19812]) ).
tff(c_22890,plain,
( ( select(a_1118,i_1129) = e_1131 )
| ( i_1129 = i27 ) ),
inference(superposition,[status(thm),theory(equality)],[c_22885,c_1654]) ).
tff(c_22908,plain,
select(a_1118,i_1129) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_13331,c_22890]) ).
tff(c_23027,plain,
select(a_1118,i21) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_23025,c_22908]) ).
tff(c_23212,plain,
( ( select(a_1117,i21) = e_1131 )
| ( i22 = i21 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1483,c_23027]) ).
tff(c_23220,plain,
select(a_1117,i21) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_222,c_23212]) ).
tff(c_23446,plain,
( ( select(a_1116,i21) = e_1131 )
| ( i26 = i21 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1558,c_23220]) ).
tff(c_23454,plain,
select(a_1116,i21) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_214,c_23446]) ).
tff(c_24829,plain,
( ( select(a_1115,i21) = e_1131 )
| ( i5 = i21 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1507,c_23454]) ).
tff(c_24838,plain,
select(a_1115,i21) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_752,c_24829]) ).
tff(c_24851,plain,
( ( select(a_1114,i21) = e_1131 )
| ( i29 = i21 ) ),
inference(superposition,[status(thm),theory(equality)],[c_24838,c_1546]) ).
tff(c_24870,plain,
select(a_1114,i21) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_208,c_24851]) ).
tff(c_24887,plain,
( ( select(a_1113,i21) = e_1131 )
| ( i21 = i14 ) ),
inference(superposition,[status(thm),theory(equality)],[c_24870,c_1606]) ).
tff(c_24906,plain,
select(a_1113,i21) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_392,c_24887]) ).
tff(c_24939,plain,
( ( select(a_1112,i21) = e_1131 )
| ( i21 = i11 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1585,c_24906]) ).
tff(c_24948,plain,
select(a_1112,i21) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_494,c_24939]) ).
tff(c_24986,plain,
( ( select(a_1111,i21) = e_1131 )
| ( i6 = i21 ) ),
inference(superposition,[status(thm),theory(equality)],[c_24948,c_1642]) ).
tff(c_25005,plain,
( ( e_1131 = e21 )
| ( i6 = i21 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1431,c_24986]) ).
tff(c_25007,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_704,c_23069,c_25005]) ).
tff(c_25008,plain,
select(a_1088,i_1129) = e_1130,
inference(splitRight,[status(thm)],[c_20515]) ).
tff(c_25042,plain,
( ( select(a_1087,i_1129) = e_1130 )
| ( i_1129 = i20 ) ),
inference(superposition,[status(thm),theory(equality)],[c_25008,c_1552]) ).
tff(c_25067,plain,
i_1129 = i20,
inference(splitLeft,[status(thm)],[c_25042]) ).
tff(c_25068,plain,
select(a_1088,i20) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_25067,c_25008]) ).
tff(c_25108,plain,
e_1130 = e20,
inference(demodulation,[status(thm),theory(equality)],[c_1335,c_25068]) ).
tff(c_25113,plain,
e_1131 != e20,
inference(demodulation,[status(thm),theory(equality)],[c_25108,c_1004]) ).
tff(c_1416,plain,
select(a_1109,i20) = e20,
inference(superposition,[status(thm),theory(equality)],[c_88,c_1257]) ).
tff(c_242,plain,
i21 != i20,
inference(cnfTransformation,[status(thm)],[f_205]) ).
tff(c_706,plain,
i6 != i20,
inference(cnfTransformation,[status(thm)],[f_669]) ).
tff(c_496,plain,
i20 != i11,
inference(cnfTransformation,[status(thm)],[f_459]) ).
tff(c_394,plain,
i20 != i14,
inference(cnfTransformation,[status(thm)],[f_357]) ).
tff(c_226,plain,
i29 != i20,
inference(cnfTransformation,[status(thm)],[f_189]) ).
tff(c_754,plain,
i5 != i20,
inference(cnfTransformation,[status(thm)],[f_717]) ).
tff(c_232,plain,
i26 != i20,
inference(cnfTransformation,[status(thm)],[f_195]) ).
tff(c_20495,plain,
i_1129 != i22,
inference(splitRight,[status(thm)],[c_17006]) ).
tff(c_22934,plain,
( ( select(a_1117,i_1129) = e_1131 )
| ( i_1129 = i22 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1483,c_22908]) ).
tff(c_22942,plain,
select(a_1117,i_1129) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_20495,c_22934]) ).
tff(c_25070,plain,
select(a_1117,i20) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_25067,c_22942]) ).
tff(c_25240,plain,
( ( select(a_1116,i20) = e_1131 )
| ( i26 = i20 ) ),
inference(superposition,[status(thm),theory(equality)],[c_25070,c_1558]) ).
tff(c_25258,plain,
select(a_1116,i20) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_232,c_25240]) ).
tff(c_26908,plain,
( ( select(a_1115,i20) = e_1131 )
| ( i5 = i20 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1507,c_25258]) ).
tff(c_26917,plain,
select(a_1115,i20) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_754,c_26908]) ).
tff(c_26931,plain,
( ( select(a_1114,i20) = e_1131 )
| ( i29 = i20 ) ),
inference(superposition,[status(thm),theory(equality)],[c_26917,c_1546]) ).
tff(c_26950,plain,
select(a_1114,i20) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_226,c_26931]) ).
tff(c_26970,plain,
( ( select(a_1113,i20) = e_1131 )
| ( i20 = i14 ) ),
inference(superposition,[status(thm),theory(equality)],[c_26950,c_1606]) ).
tff(c_26989,plain,
select(a_1113,i20) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_394,c_26970]) ).
tff(c_27022,plain,
( ( select(a_1112,i20) = e_1131 )
| ( i20 = i11 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1585,c_26989]) ).
tff(c_27031,plain,
select(a_1112,i20) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_496,c_27022]) ).
tff(c_27042,plain,
( ( select(a_1111,i20) = e_1131 )
| ( i6 = i20 ) ),
inference(superposition,[status(thm),theory(equality)],[c_27031,c_1642]) ).
tff(c_27061,plain,
select(a_1111,i20) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_706,c_27042]) ).
tff(c_27078,plain,
( ( select(a_1110,i20) = e_1131 )
| ( i21 = i20 ) ),
inference(superposition,[status(thm),theory(equality)],[c_27061,c_1648]) ).
tff(c_27097,plain,
select(a_1110,i20) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_242,c_27078]) ).
tff(c_27114,plain,
( ( select(a_1109,i20) = e_1131 )
| ( i8 = i20 ) ),
inference(superposition,[status(thm),theory(equality)],[c_27097,c_1522]) ).
tff(c_27133,plain,
( ( e_1131 = e20 )
| ( i8 = i20 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1416,c_27114]) ).
tff(c_27135,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_616,c_25113,c_27133]) ).
tff(c_27136,plain,
select(a_1087,i_1129) = e_1130,
inference(splitRight,[status(thm)],[c_25042]) ).
tff(c_27194,plain,
( ( select(a_1086,i_1129) = e_1130 )
| ( i_1129 = i19 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1573,c_27136]) ).
tff(c_28264,plain,
i_1129 = i19,
inference(splitLeft,[status(thm)],[c_27194]) ).
tff(c_28266,plain,
select(a_1087,i19) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_28264,c_27136]) ).
tff(c_28308,plain,
e_1130 = e19,
inference(demodulation,[status(thm),theory(equality)],[c_1356,c_28266]) ).
tff(c_28313,plain,
e_1131 != e19,
inference(demodulation,[status(thm),theory(equality)],[c_28308,c_1004]) ).
tff(c_72,plain,
store(a_1100,i19,e19) = a_1101,
inference(cnfTransformation,[status(thm)],[f_65]) ).
tff(c_1284,plain,
select(a_1101,i19) = e19,
inference(superposition,[status(thm),theory(equality)],[c_72,c_1257]) ).
tff(c_576,plain,
i9 != i19,
inference(cnfTransformation,[status(thm)],[f_539]) ).
tff(c_244,plain,
i30 != i19,
inference(cnfTransformation,[status(thm)],[f_207]) ).
tff(c_912,plain,
i2 != i19,
inference(cnfTransformation,[status(thm)],[f_875]) ).
tff(c_366,plain,
i19 != i15,
inference(cnfTransformation,[status(thm)],[f_329]) ).
tff(c_254,plain,
i25 != i19,
inference(cnfTransformation,[status(thm)],[f_217]) ).
tff(c_288,plain,
i19 != i18,
inference(cnfTransformation,[status(thm)],[f_251]) ).
tff(c_264,plain,
i20 != i19,
inference(cnfTransformation,[status(thm)],[f_227]) ).
tff(c_618,plain,
i8 != i19,
inference(cnfTransformation,[status(thm)],[f_581]) ).
tff(c_262,plain,
i21 != i19,
inference(cnfTransformation,[status(thm)],[f_225]) ).
tff(c_708,plain,
i6 != i19,
inference(cnfTransformation,[status(thm)],[f_671]) ).
tff(c_498,plain,
i19 != i11,
inference(cnfTransformation,[status(thm)],[f_461]) ).
tff(c_396,plain,
i19 != i14,
inference(cnfTransformation,[status(thm)],[f_359]) ).
tff(c_246,plain,
i29 != i19,
inference(cnfTransformation,[status(thm)],[f_209]) ).
tff(c_756,plain,
i5 != i19,
inference(cnfTransformation,[status(thm)],[f_719]) ).
tff(c_15850,plain,
i_1129 != i26,
inference(splitRight,[status(thm)],[c_13380]) ).
tff(c_27138,plain,
! [J_249] :
( ( select(a_1117,J_249) = select(a_1116,J_249) )
| ( i26 = J_249 ) ),
inference(superposition,[status(thm),theory(equality)],[c_104,c_1467]) ).
tff(c_27144,plain,
( ( select(a_1116,i_1129) = e_1131 )
| ( i_1129 = i26 ) ),
inference(superposition,[status(thm),theory(equality)],[c_27138,c_22942]) ).
tff(c_27170,plain,
select(a_1116,i_1129) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_15850,c_27144]) ).
tff(c_28265,plain,
select(a_1116,i19) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_28264,c_27170]) ).
tff(c_28455,plain,
( ( select(a_1115,i19) = e_1131 )
| ( i5 = i19 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1507,c_28265]) ).
tff(c_28464,plain,
select(a_1115,i19) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_756,c_28455]) ).
tff(c_29281,plain,
( ( select(a_1114,i19) = e_1131 )
| ( i29 = i19 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1546,c_28464]) ).
tff(c_29290,plain,
select(a_1114,i19) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_246,c_29281]) ).
tff(c_29319,plain,
( ( select(a_1113,i19) = e_1131 )
| ( i19 = i14 ) ),
inference(superposition,[status(thm),theory(equality)],[c_29290,c_1606]) ).
tff(c_29338,plain,
select(a_1113,i19) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_396,c_29319]) ).
tff(c_29357,plain,
( ( select(a_1112,i19) = e_1131 )
| ( i19 = i11 ) ),
inference(superposition,[status(thm),theory(equality)],[c_29338,c_1585]) ).
tff(c_29376,plain,
select(a_1112,i19) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_498,c_29357]) ).
tff(c_29394,plain,
( ( select(a_1111,i19) = e_1131 )
| ( i6 = i19 ) ),
inference(superposition,[status(thm),theory(equality)],[c_29376,c_1642]) ).
tff(c_29413,plain,
select(a_1111,i19) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_708,c_29394]) ).
tff(c_29446,plain,
( ( select(a_1110,i19) = e_1131 )
| ( i21 = i19 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1648,c_29413]) ).
tff(c_29455,plain,
select(a_1110,i19) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_262,c_29446]) ).
tff(c_29466,plain,
( ( select(a_1109,i19) = e_1131 )
| ( i8 = i19 ) ),
inference(superposition,[status(thm),theory(equality)],[c_29455,c_1522]) ).
tff(c_29485,plain,
select(a_1109,i19) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_618,c_29466]) ).
tff(c_29502,plain,
( ( select(a_1108,i19) = e_1131 )
| ( i20 = i19 ) ),
inference(superposition,[status(thm),theory(equality)],[c_29485,c_1633]) ).
tff(c_29521,plain,
select(a_1108,i19) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_264,c_29502]) ).
tff(c_29554,plain,
( ( select(a_1107,i19) = e_1131 )
| ( i19 = i18 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1660,c_29521]) ).
tff(c_29563,plain,
select(a_1107,i19) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_288,c_29554]) ).
tff(c_29575,plain,
( ( select(a_1106,i19) = e_1131 )
| ( i25 = i19 ) ),
inference(superposition,[status(thm),theory(equality)],[c_29563,c_1612]) ).
tff(c_29594,plain,
select(a_1106,i19) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_254,c_29575]) ).
tff(c_29611,plain,
( ( select(a_1105,i19) = e_1131 )
| ( i19 = i15 ) ),
inference(superposition,[status(thm),theory(equality)],[c_29594,c_1621]) ).
tff(c_29630,plain,
select(a_1105,i19) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_366,c_29611]) ).
tff(c_29647,plain,
( ( select(a_1104,i19) = e_1131 )
| ( i2 = i19 ) ),
inference(superposition,[status(thm),theory(equality)],[c_29630,c_1600]) ).
tff(c_29666,plain,
select(a_1104,i19) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_912,c_29647]) ).
tff(c_1582,plain,
! [J_17] :
( ( select(a_1104,J_17) = select(a_1103,J_17) )
| ( i30 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_78,c_1467]) ).
tff(c_29683,plain,
( ( select(a_1103,i19) = e_1131 )
| ( i30 = i19 ) ),
inference(superposition,[status(thm),theory(equality)],[c_29666,c_1582]) ).
tff(c_29702,plain,
select(a_1103,i19) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_244,c_29683]) ).
tff(c_76,plain,
store(a_1102,i9,e9) = a_1103,
inference(cnfTransformation,[status(thm)],[f_67]) ).
tff(c_1618,plain,
! [J_17] :
( ( select(a_1103,J_17) = select(a_1102,J_17) )
| ( i9 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_76,c_1467]) ).
tff(c_29720,plain,
( ( select(a_1102,i19) = e_1131 )
| ( i9 = i19 ) ),
inference(superposition,[status(thm),theory(equality)],[c_29702,c_1618]) ).
tff(c_29739,plain,
select(a_1102,i19) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_576,c_29720]) ).
tff(c_74,plain,
store(a_1101,i4,e4) = a_1102,
inference(cnfTransformation,[status(thm)],[f_66]) ).
tff(c_1495,plain,
! [J_17] :
( ( select(a_1102,J_17) = select(a_1101,J_17) )
| ( i4 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_74,c_1467]) ).
tff(c_29756,plain,
( ( select(a_1101,i19) = e_1131 )
| ( i4 = i19 ) ),
inference(superposition,[status(thm),theory(equality)],[c_29739,c_1495]) ).
tff(c_29775,plain,
( ( e_1131 = e19 )
| ( i4 = i19 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1284,c_29756]) ).
tff(c_29777,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_806,c_28313,c_29775]) ).
tff(c_29779,plain,
i_1129 != i19,
inference(splitRight,[status(thm)],[c_27194]) ).
tff(c_1278,plain,
select(a_1102,i4) = e4,
inference(superposition,[status(thm),theory(equality)],[c_74,c_1257]) ).
tff(c_782,plain,
i6 != i5,
inference(cnfTransformation,[status(thm)],[f_745]) ).
tff(c_1290,plain,
select(a_1116,i5) = e5,
inference(superposition,[status(thm),theory(equality)],[c_102,c_1257]) ).
tff(c_27204,plain,
( ( select(a_1115,i_1129) = e_1131 )
| ( i_1129 = i5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_27170,c_1507]) ).
tff(c_29877,plain,
i_1129 = i5,
inference(splitLeft,[status(thm)],[c_27204]) ).
tff(c_29881,plain,
select(a_1116,i5) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_29877,c_27170]) ).
tff(c_29924,plain,
e_1131 = e5,
inference(demodulation,[status(thm),theory(equality)],[c_1290,c_29881]) ).
tff(c_29930,plain,
e_1130 != e5,
inference(demodulation,[status(thm),theory(equality)],[c_29924,c_1004]) ).
tff(c_1302,plain,
select(a_1073,i5) = e5,
inference(superposition,[status(thm),theory(equality)],[c_16,c_1257]) ).
tff(c_780,plain,
i7 != i5,
inference(cnfTransformation,[status(thm)],[f_743]) ).
tff(c_778,plain,
i8 != i5,
inference(cnfTransformation,[status(thm)],[f_741]) ).
tff(c_776,plain,
i9 != i5,
inference(cnfTransformation,[status(thm)],[f_739]) ).
tff(c_774,plain,
i5 != i10,
inference(cnfTransformation,[status(thm)],[f_737]) ).
tff(c_772,plain,
i5 != i11,
inference(cnfTransformation,[status(thm)],[f_735]) ).
tff(c_770,plain,
i5 != i12,
inference(cnfTransformation,[status(thm)],[f_733]) ).
tff(c_768,plain,
i5 != i13,
inference(cnfTransformation,[status(thm)],[f_731]) ).
tff(c_766,plain,
i5 != i14,
inference(cnfTransformation,[status(thm)],[f_729]) ).
tff(c_764,plain,
i5 != i15,
inference(cnfTransformation,[status(thm)],[f_727]) ).
tff(c_762,plain,
i5 != i16,
inference(cnfTransformation,[status(thm)],[f_725]) ).
tff(c_760,plain,
i5 != i17,
inference(cnfTransformation,[status(thm)],[f_723]) ).
tff(c_758,plain,
i5 != i18,
inference(cnfTransformation,[status(thm)],[f_721]) ).
tff(c_29778,plain,
select(a_1086,i_1129) = e_1130,
inference(splitRight,[status(thm)],[c_27194]) ).
tff(c_29878,plain,
select(a_1086,i5) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_29877,c_29778]) ).
tff(c_29999,plain,
( ( select(a_1085,i5) = e_1130 )
| ( i5 = i18 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1525,c_29878]) ).
tff(c_30008,plain,
select(a_1085,i5) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_758,c_29999]) ).
tff(c_30917,plain,
( ( select(a_1084,i5) = e_1130 )
| ( i5 = i17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_30008,c_1540]) ).
tff(c_30936,plain,
select(a_1084,i5) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_760,c_30917]) ).
tff(c_30975,plain,
( ( select(a_1083,i5) = e_1130 )
| ( i5 = i16 ) ),
inference(superposition,[status(thm),theory(equality)],[c_30936,c_1489]) ).
tff(c_30994,plain,
select(a_1083,i5) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_762,c_30975]) ).
tff(c_31012,plain,
( ( select(a_1082,i5) = e_1130 )
| ( i5 = i15 ) ),
inference(superposition,[status(thm),theory(equality)],[c_30994,c_1630]) ).
tff(c_31031,plain,
select(a_1082,i5) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_764,c_31012]) ).
tff(c_31064,plain,
( ( select(a_1081,i5) = e_1130 )
| ( i5 = i14 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1645,c_31031]) ).
tff(c_31073,plain,
select(a_1081,i5) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_766,c_31064]) ).
tff(c_31084,plain,
( ( select(a_1080,i5) = e_1130 )
| ( i5 = i13 ) ),
inference(superposition,[status(thm),theory(equality)],[c_31073,c_1597]) ).
tff(c_31103,plain,
select(a_1080,i5) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_768,c_31084]) ).
tff(c_31120,plain,
( ( select(a_1079,i5) = e_1130 )
| ( i5 = i12 ) ),
inference(superposition,[status(thm),theory(equality)],[c_31103,c_1531]) ).
tff(c_31139,plain,
select(a_1079,i5) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_770,c_31120]) ).
tff(c_31172,plain,
( ( select(a_1078,i5) = e_1130 )
| ( i5 = i11 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1543,c_31139]) ).
tff(c_31181,plain,
select(a_1078,i5) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_772,c_31172]) ).
tff(c_31193,plain,
( ( select(a_1077,i5) = e_1130 )
| ( i5 = i10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_31181,c_1567]) ).
tff(c_31212,plain,
select(a_1077,i5) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_774,c_31193]) ).
tff(c_31229,plain,
( ( select(a_1076,i5) = e_1130 )
| ( i9 = i5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_31212,c_1591]) ).
tff(c_31248,plain,
select(a_1076,i5) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_776,c_31229]) ).
tff(c_31265,plain,
( ( select(a_1075,i5) = e_1130 )
| ( i8 = i5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_31248,c_1651]) ).
tff(c_31284,plain,
select(a_1075,i5) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_778,c_31265]) ).
tff(c_31301,plain,
( ( select(a_1074,i5) = e_1130 )
| ( i7 = i5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_31284,c_1510]) ).
tff(c_31320,plain,
select(a_1074,i5) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_780,c_31301]) ).
tff(c_31338,plain,
( ( select(a_1073,i5) = e_1130 )
| ( i6 = i5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_31320,c_1486]) ).
tff(c_31357,plain,
( ( e_1130 = e5 )
| ( i6 = i5 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1302,c_31338]) ).
tff(c_31359,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_782,c_29930,c_31357]) ).
tff(c_31361,plain,
i_1129 != i5,
inference(splitRight,[status(thm)],[c_27204]) ).
tff(c_732,plain,
i7 != i6,
inference(cnfTransformation,[status(thm)],[f_695]) ).
tff(c_1425,plain,
select(a_1112,i6) = e6,
inference(superposition,[status(thm),theory(equality)],[c_94,c_1257]) ).
tff(c_512,plain,
i12 != i11,
inference(cnfTransformation,[status(thm)],[f_475]) ).
tff(c_1368,plain,
select(a_1113,i11) = e11,
inference(superposition,[status(thm),theory(equality)],[c_96,c_1257]) ).
tff(c_404,plain,
i15 != i14,
inference(cnfTransformation,[status(thm)],[f_367]) ).
tff(c_1389,plain,
select(a_1114,i14) = e14,
inference(superposition,[status(thm),theory(equality)],[c_98,c_1257]) ).
tff(c_12452,plain,
i_1129 != i29,
inference(splitRight,[status(thm)],[c_11893]) ).
tff(c_31360,plain,
select(a_1115,i_1129) = e_1131,
inference(splitRight,[status(thm)],[c_27204]) ).
tff(c_31371,plain,
( ( select(a_1114,i_1129) = e_1131 )
| ( i_1129 = i29 ) ),
inference(superposition,[status(thm),theory(equality)],[c_31360,c_1546]) ).
tff(c_31390,plain,
select(a_1114,i_1129) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_12452,c_31371]) ).
tff(c_31468,plain,
( ( select(a_1113,i_1129) = e_1131 )
| ( i_1129 = i14 ) ),
inference(superposition,[status(thm),theory(equality)],[c_31390,c_1606]) ).
tff(c_32942,plain,
i_1129 = i14,
inference(splitLeft,[status(thm)],[c_31468]) ).
tff(c_32948,plain,
select(a_1114,i14) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_32942,c_31390]) ).
tff(c_32997,plain,
e_1131 = e14,
inference(demodulation,[status(thm),theory(equality)],[c_1389,c_32948]) ).
tff(c_33038,plain,
e_1130 != e14,
inference(demodulation,[status(thm),theory(equality)],[c_32997,c_1004]) ).
tff(c_1428,plain,
select(a_1082,i14) = e14,
inference(superposition,[status(thm),theory(equality)],[c_34,c_1257]) ).
tff(c_17813,plain,
i_1129 != i16,
inference(splitRight,[status(thm)],[c_15215]) ).
tff(c_15167,plain,
i_1129 != i17,
inference(splitRight,[status(thm)],[c_10756]) ).
tff(c_286,plain,
i20 != i18,
inference(cnfTransformation,[status(thm)],[f_249]) ).
tff(c_1308,plain,
select(a_1086,i18) = e18,
inference(superposition,[status(thm),theory(equality)],[c_42,c_1257]) ).
tff(c_29867,plain,
( ( select(a_1085,i_1129) = e_1130 )
| ( i_1129 = i18 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1525,c_29778]) ).
tff(c_31495,plain,
i_1129 = i18,
inference(splitLeft,[status(thm)],[c_29867]) ).
tff(c_31500,plain,
select(a_1086,i18) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_31495,c_29778]) ).
tff(c_31546,plain,
e_1130 = e18,
inference(demodulation,[status(thm),theory(equality)],[c_1308,c_31500]) ).
tff(c_31552,plain,
e_1131 != e18,
inference(demodulation,[status(thm),theory(equality)],[c_31546,c_1004]) ).
tff(c_1443,plain,
select(a_1108,i18) = e18,
inference(superposition,[status(thm),theory(equality)],[c_86,c_1257]) ).
tff(c_620,plain,
i8 != i18,
inference(cnfTransformation,[status(thm)],[f_583]) ).
tff(c_284,plain,
i21 != i18,
inference(cnfTransformation,[status(thm)],[f_247]) ).
tff(c_710,plain,
i6 != i18,
inference(cnfTransformation,[status(thm)],[f_673]) ).
tff(c_500,plain,
i18 != i11,
inference(cnfTransformation,[status(thm)],[f_463]) ).
tff(c_398,plain,
i18 != i14,
inference(cnfTransformation,[status(thm)],[f_361]) ).
tff(c_268,plain,
i29 != i18,
inference(cnfTransformation,[status(thm)],[f_231]) ).
tff(c_31498,plain,
select(a_1115,i18) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_31495,c_31360]) ).
tff(c_31641,plain,
( ( select(a_1114,i18) = e_1131 )
| ( i29 = i18 ) ),
inference(superposition,[status(thm),theory(equality)],[c_31498,c_1546]) ).
tff(c_31660,plain,
select(a_1114,i18) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_268,c_31641]) ).
tff(c_32581,plain,
( ( select(a_1113,i18) = e_1131 )
| ( i18 = i14 ) ),
inference(superposition,[status(thm),theory(equality)],[c_31660,c_1606]) ).
tff(c_32600,plain,
select(a_1113,i18) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_398,c_32581]) ).
tff(c_32653,plain,
( ( select(a_1112,i18) = e_1131 )
| ( i18 = i11 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1585,c_32600]) ).
tff(c_32662,plain,
select(a_1112,i18) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_500,c_32653]) ).
tff(c_32673,plain,
( ( select(a_1111,i18) = e_1131 )
| ( i6 = i18 ) ),
inference(superposition,[status(thm),theory(equality)],[c_32662,c_1642]) ).
tff(c_32692,plain,
select(a_1111,i18) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_710,c_32673]) ).
tff(c_32709,plain,
( ( select(a_1110,i18) = e_1131 )
| ( i21 = i18 ) ),
inference(superposition,[status(thm),theory(equality)],[c_32692,c_1648]) ).
tff(c_32728,plain,
select(a_1110,i18) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_284,c_32709]) ).
tff(c_32761,plain,
( ( select(a_1109,i18) = e_1131 )
| ( i8 = i18 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1522,c_32728]) ).
tff(c_32770,plain,
select(a_1109,i18) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_620,c_32761]) ).
tff(c_32782,plain,
( ( select(a_1108,i18) = e_1131 )
| ( i20 = i18 ) ),
inference(superposition,[status(thm),theory(equality)],[c_32770,c_1633]) ).
tff(c_32801,plain,
( ( e_1131 = e18 )
| ( i20 = i18 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1443,c_32782]) ).
tff(c_32803,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_286,c_31552,c_32801]) ).
tff(c_32804,plain,
select(a_1085,i_1129) = e_1130,
inference(splitRight,[status(thm)],[c_29867]) ).
tff(c_32816,plain,
( ( select(a_1084,i_1129) = e_1130 )
| ( i_1129 = i17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_32804,c_1540]) ).
tff(c_32835,plain,
select(a_1084,i_1129) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_15167,c_32816]) ).
tff(c_32851,plain,
( ( select(a_1083,i_1129) = e_1130 )
| ( i_1129 = i16 ) ),
inference(superposition,[status(thm),theory(equality)],[c_32835,c_1489]) ).
tff(c_32870,plain,
select(a_1083,i_1129) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_17813,c_32851]) ).
tff(c_32944,plain,
select(a_1083,i14) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_32942,c_32870]) ).
tff(c_33863,plain,
( ( select(a_1082,i14) = e_1130 )
| ( i15 = i14 ) ),
inference(superposition,[status(thm),theory(equality)],[c_32944,c_1630]) ).
tff(c_33882,plain,
( ( e_1130 = e14 )
| ( i15 = i14 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1428,c_33863]) ).
tff(c_33884,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_404,c_33038,c_33882]) ).
tff(c_33885,plain,
select(a_1113,i_1129) = e_1131,
inference(splitRight,[status(thm)],[c_31468]) ).
tff(c_33896,plain,
( ( select(a_1112,i_1129) = e_1131 )
| ( i_1129 = i11 ) ),
inference(superposition,[status(thm),theory(equality)],[c_33885,c_1585]) ).
tff(c_37233,plain,
i_1129 = i11,
inference(splitLeft,[status(thm)],[c_33896]) ).
tff(c_37238,plain,
select(a_1113,i11) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_37233,c_33885]) ).
tff(c_37293,plain,
e_1131 = e11,
inference(demodulation,[status(thm),theory(equality)],[c_1368,c_37238]) ).
tff(c_37334,plain,
e_1130 != e11,
inference(demodulation,[status(thm),theory(equality)],[c_37293,c_1004]) ).
tff(c_1326,plain,
select(a_1079,i11) = e11,
inference(superposition,[status(thm),theory(equality)],[c_28,c_1257]) ).
tff(c_510,plain,
i13 != i11,
inference(cnfTransformation,[status(thm)],[f_473]) ).
tff(c_508,plain,
i14 != i11,
inference(cnfTransformation,[status(thm)],[f_471]) ).
tff(c_354,plain,
i25 != i15,
inference(cnfTransformation,[status(thm)],[f_317]) ).
tff(c_1413,plain,
select(a_1083,i15) = e15,
inference(superposition,[status(thm),theory(equality)],[c_36,c_1257]) ).
tff(c_32903,plain,
( ( select(a_1082,i_1129) = e_1130 )
| ( i_1129 = i15 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1630,c_32870]) ).
tff(c_33922,plain,
i_1129 = i15,
inference(splitLeft,[status(thm)],[c_32903]) ).
tff(c_33955,plain,
select(a_1083,i15) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_33922,c_32870]) ).
tff(c_34007,plain,
e_1130 = e15,
inference(demodulation,[status(thm),theory(equality)],[c_1413,c_33955]) ).
tff(c_34012,plain,
e_1131 != e15,
inference(demodulation,[status(thm),theory(equality)],[c_34007,c_1004]) ).
tff(c_1404,plain,
select(a_1106,i15) = e15,
inference(superposition,[status(thm),theory(equality)],[c_82,c_1257]) ).
tff(c_368,plain,
i18 != i15,
inference(cnfTransformation,[status(thm)],[f_331]) ).
tff(c_364,plain,
i20 != i15,
inference(cnfTransformation,[status(thm)],[f_327]) ).
tff(c_626,plain,
i8 != i15,
inference(cnfTransformation,[status(thm)],[f_589]) ).
tff(c_362,plain,
i21 != i15,
inference(cnfTransformation,[status(thm)],[f_325]) ).
tff(c_716,plain,
i6 != i15,
inference(cnfTransformation,[status(thm)],[f_679]) ).
tff(c_506,plain,
i15 != i11,
inference(cnfTransformation,[status(thm)],[f_469]) ).
tff(c_33952,plain,
select(a_1113,i15) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_33922,c_33885]) ).
tff(c_34304,plain,
( ( select(a_1112,i15) = e_1131 )
| ( i15 = i11 ) ),
inference(superposition,[status(thm),theory(equality)],[c_33952,c_1585]) ).
tff(c_34323,plain,
select(a_1112,i15) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_506,c_34304]) ).
tff(c_35242,plain,
( ( select(a_1111,i15) = e_1131 )
| ( i6 = i15 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1642,c_34323]) ).
tff(c_35251,plain,
select(a_1111,i15) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_716,c_35242]) ).
tff(c_36383,plain,
( ( select(a_1110,i15) = e_1131 )
| ( i21 = i15 ) ),
inference(superposition,[status(thm),theory(equality)],[c_35251,c_1648]) ).
tff(c_36403,plain,
select(a_1110,i15) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_362,c_36383]) ).
tff(c_36427,plain,
( ( select(a_1109,i15) = e_1131 )
| ( i8 = i15 ) ),
inference(superposition,[status(thm),theory(equality)],[c_36403,c_1522]) ).
tff(c_36447,plain,
select(a_1109,i15) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_626,c_36427]) ).
tff(c_37023,plain,
( ( select(a_1108,i15) = e_1131 )
| ( i20 = i15 ) ),
inference(superposition,[status(thm),theory(equality)],[c_36447,c_1633]) ).
tff(c_37043,plain,
select(a_1108,i15) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_364,c_37023]) ).
tff(c_37082,plain,
( ( select(a_1107,i15) = e_1131 )
| ( i18 = i15 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1660,c_37043]) ).
tff(c_37092,plain,
select(a_1107,i15) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_368,c_37082]) ).
tff(c_37109,plain,
( ( select(a_1106,i15) = e_1131 )
| ( i25 = i15 ) ),
inference(superposition,[status(thm),theory(equality)],[c_37092,c_1612]) ).
tff(c_37129,plain,
( ( e_1131 = e15 )
| ( i25 = i15 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1404,c_37109]) ).
tff(c_37131,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_354,c_34012,c_37129]) ).
tff(c_37132,plain,
select(a_1082,i_1129) = e_1130,
inference(splitRight,[status(thm)],[c_32903]) ).
tff(c_37236,plain,
select(a_1082,i11) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_37233,c_37132]) ).
tff(c_38550,plain,
( ( select(a_1081,i11) = e_1130 )
| ( i14 = i11 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1645,c_37236]) ).
tff(c_38559,plain,
select(a_1081,i11) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_508,c_38550]) ).
tff(c_38589,plain,
( ( select(a_1080,i11) = e_1130 )
| ( i13 = i11 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1597,c_38559]) ).
tff(c_38598,plain,
select(a_1080,i11) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_510,c_38589]) ).
tff(c_39750,plain,
( ( select(a_1079,i11) = e_1130 )
| ( i12 = i11 ) ),
inference(superposition,[status(thm),theory(equality)],[c_38598,c_1531]) ).
tff(c_39770,plain,
( ( e_1130 = e11 )
| ( i12 = i11 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1326,c_39750]) ).
tff(c_39772,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_512,c_37334,c_39770]) ).
tff(c_39773,plain,
select(a_1112,i_1129) = e_1131,
inference(splitRight,[status(thm)],[c_33896]) ).
tff(c_39785,plain,
( ( select(a_1111,i_1129) = e_1131 )
| ( i_1129 = i6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_39773,c_1642]) ).
tff(c_39870,plain,
i_1129 = i6,
inference(splitLeft,[status(thm)],[c_39785]) ).
tff(c_39872,plain,
select(a_1112,i6) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_39870,c_39773]) ).
tff(c_39933,plain,
e_1131 = e6,
inference(demodulation,[status(thm),theory(equality)],[c_1425,c_39872]) ).
tff(c_39938,plain,
e_1130 != e6,
inference(demodulation,[status(thm),theory(equality)],[c_39933,c_1004]) ).
tff(c_1269,plain,
select(a_1074,i6) = e6,
inference(superposition,[status(thm),theory(equality)],[c_18,c_1257]) ).
tff(c_730,plain,
i8 != i6,
inference(cnfTransformation,[status(thm)],[f_693]) ).
tff(c_728,plain,
i9 != i6,
inference(cnfTransformation,[status(thm)],[f_691]) ).
tff(c_726,plain,
i6 != i10,
inference(cnfTransformation,[status(thm)],[f_689]) ).
tff(c_724,plain,
i6 != i11,
inference(cnfTransformation,[status(thm)],[f_687]) ).
tff(c_722,plain,
i6 != i12,
inference(cnfTransformation,[status(thm)],[f_685]) ).
tff(c_720,plain,
i6 != i13,
inference(cnfTransformation,[status(thm)],[f_683]) ).
tff(c_33886,plain,
i_1129 != i14,
inference(splitRight,[status(thm)],[c_31468]) ).
tff(c_37143,plain,
( ( select(a_1081,i_1129) = e_1130 )
| ( i_1129 = i14 ) ),
inference(superposition,[status(thm),theory(equality)],[c_37132,c_1645]) ).
tff(c_37162,plain,
select(a_1081,i_1129) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_33886,c_37143]) ).
tff(c_39875,plain,
select(a_1081,i6) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_39870,c_37162]) ).
tff(c_39952,plain,
( ( select(a_1080,i6) = e_1130 )
| ( i6 = i13 ) ),
inference(superposition,[status(thm),theory(equality)],[c_39875,c_1597]) ).
tff(c_39971,plain,
select(a_1080,i6) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_720,c_39952]) ).
tff(c_42389,plain,
( ( select(a_1079,i6) = e_1130 )
| ( i6 = i12 ) ),
inference(superposition,[status(thm),theory(equality)],[c_39971,c_1531]) ).
tff(c_42409,plain,
select(a_1079,i6) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_722,c_42389]) ).
tff(c_42442,plain,
( ( select(a_1078,i6) = e_1130 )
| ( i6 = i11 ) ),
inference(superposition,[status(thm),theory(equality)],[c_42409,c_1543]) ).
tff(c_42462,plain,
select(a_1078,i6) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_724,c_42442]) ).
tff(c_42501,plain,
( ( select(a_1077,i6) = e_1130 )
| ( i6 = i10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1567,c_42462]) ).
tff(c_42511,plain,
select(a_1077,i6) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_726,c_42501]) ).
tff(c_43081,plain,
( ( select(a_1076,i6) = e_1130 )
| ( i9 = i6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_42511,c_1591]) ).
tff(c_43101,plain,
select(a_1076,i6) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_728,c_43081]) ).
tff(c_43124,plain,
( ( select(a_1075,i6) = e_1130 )
| ( i8 = i6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_43101,c_1651]) ).
tff(c_43144,plain,
select(a_1075,i6) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_730,c_43124]) ).
tff(c_43167,plain,
( ( select(a_1074,i6) = e_1130 )
| ( i7 = i6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_43144,c_1510]) ).
tff(c_43187,plain,
( ( e_1130 = e6 )
| ( i7 = i6 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1269,c_43167]) ).
tff(c_43189,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_732,c_39938,c_43187]) ).
tff(c_43191,plain,
i_1129 != i6,
inference(splitRight,[status(thm)],[c_39785]) ).
tff(c_9045,plain,
i_1129 != i7,
inference(splitRight,[status(thm)],[c_6295]) ).
tff(c_638,plain,
i9 != i8,
inference(cnfTransformation,[status(thm)],[f_601]) ).
tff(c_1305,plain,
select(a_1110,i8) = e8,
inference(superposition,[status(thm),theory(equality)],[c_90,c_1257]) ).
tff(c_25009,plain,
i_1129 != i21,
inference(splitRight,[status(thm)],[c_20515]) ).
tff(c_43190,plain,
select(a_1111,i_1129) = e_1131,
inference(splitRight,[status(thm)],[c_39785]) ).
tff(c_43201,plain,
( ( select(a_1110,i_1129) = e_1131 )
| ( i_1129 = i21 ) ),
inference(superposition,[status(thm),theory(equality)],[c_43190,c_1648]) ).
tff(c_43220,plain,
select(a_1110,i_1129) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_25009,c_43201]) ).
tff(c_43236,plain,
( ( select(a_1109,i_1129) = e_1131 )
| ( i_1129 = i8 ) ),
inference(superposition,[status(thm),theory(equality)],[c_43220,c_1522]) ).
tff(c_47182,plain,
i_1129 = i8,
inference(splitLeft,[status(thm)],[c_43236]) ).
tff(c_47190,plain,
select(a_1110,i8) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_47182,c_43220]) ).
tff(c_47255,plain,
e_1131 = e8,
inference(demodulation,[status(thm),theory(equality)],[c_1305,c_47190]) ).
tff(c_47260,plain,
e_1130 != e8,
inference(demodulation,[status(thm),theory(equality)],[c_47255,c_1004]) ).
tff(c_1434,plain,
select(a_1076,i8) = e8,
inference(superposition,[status(thm),theory(equality)],[c_22,c_1257]) ).
tff(c_39774,plain,
i_1129 != i11,
inference(splitRight,[status(thm)],[c_33896]) ).
tff(c_19808,plain,
i_1129 != i12,
inference(splitRight,[status(thm)],[c_17817]) ).
tff(c_980,plain,
i13 != i1,
inference(cnfTransformation,[status(thm)],[f_943]) ).
tff(c_1380,plain,
select(a_1081,i13) = e13,
inference(superposition,[status(thm),theory(equality)],[c_32,c_1257]) ).
tff(c_37178,plain,
( ( select(a_1080,i_1129) = e_1130 )
| ( i_1129 = i13 ) ),
inference(superposition,[status(thm),theory(equality)],[c_37162,c_1597]) ).
tff(c_43264,plain,
i_1129 = i13,
inference(splitLeft,[status(thm)],[c_37178]) ).
tff(c_43332,plain,
select(a_1081,i13) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_43264,c_37162]) ).
tff(c_43390,plain,
e_1130 = e13,
inference(demodulation,[status(thm),theory(equality)],[c_1380,c_43332]) ).
tff(c_43395,plain,
e_1131 != e13,
inference(demodulation,[status(thm),theory(equality)],[c_43390,c_1004]) ).
tff(c_68,plain,
store(a1,i13,e13) = a_1099,
inference(cnfTransformation,[status(thm)],[f_63]) ).
tff(c_1281,plain,
select(a_1099,i13) = e13,
inference(superposition,[status(thm),theory(equality)],[c_68,c_1257]) ).
tff(c_428,plain,
i19 != i13,
inference(cnfTransformation,[status(thm)],[f_391]) ).
tff(c_818,plain,
i4 != i13,
inference(cnfTransformation,[status(thm)],[f_781]) ).
tff(c_588,plain,
i9 != i13,
inference(cnfTransformation,[status(thm)],[f_551]) ).
tff(c_406,plain,
i30 != i13,
inference(cnfTransformation,[status(thm)],[f_369]) ).
tff(c_924,plain,
i2 != i13,
inference(cnfTransformation,[status(thm)],[f_887]) ).
tff(c_436,plain,
i15 != i13,
inference(cnfTransformation,[status(thm)],[f_399]) ).
tff(c_416,plain,
i25 != i13,
inference(cnfTransformation,[status(thm)],[f_379]) ).
tff(c_430,plain,
i18 != i13,
inference(cnfTransformation,[status(thm)],[f_393]) ).
tff(c_426,plain,
i20 != i13,
inference(cnfTransformation,[status(thm)],[f_389]) ).
tff(c_630,plain,
i8 != i13,
inference(cnfTransformation,[status(thm)],[f_593]) ).
tff(c_43325,plain,
select(a_1110,i13) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_43264,c_43220]) ).
tff(c_44733,plain,
( ( select(a_1109,i13) = e_1131 )
| ( i8 = i13 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1522,c_43325]) ).
tff(c_44742,plain,
select(a_1109,i13) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_630,c_44733]) ).
tff(c_45935,plain,
( ( select(a_1108,i13) = e_1131 )
| ( i20 = i13 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1633,c_44742]) ).
tff(c_45945,plain,
select(a_1108,i13) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_426,c_45935]) ).
tff(c_46544,plain,
( ( select(a_1107,i13) = e_1131 )
| ( i18 = i13 ) ),
inference(superposition,[status(thm),theory(equality)],[c_45945,c_1660]) ).
tff(c_46564,plain,
select(a_1107,i13) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_430,c_46544]) ).
tff(c_46587,plain,
( ( select(a_1106,i13) = e_1131 )
| ( i25 = i13 ) ),
inference(superposition,[status(thm),theory(equality)],[c_46564,c_1612]) ).
tff(c_46607,plain,
select(a_1106,i13) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_416,c_46587]) ).
tff(c_46646,plain,
( ( select(a_1105,i13) = e_1131 )
| ( i15 = i13 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1621,c_46607]) ).
tff(c_46656,plain,
select(a_1105,i13) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_436,c_46646]) ).
tff(c_46674,plain,
( ( select(a_1104,i13) = e_1131 )
| ( i2 = i13 ) ),
inference(superposition,[status(thm),theory(equality)],[c_46656,c_1600]) ).
tff(c_46694,plain,
select(a_1104,i13) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_924,c_46674]) ).
tff(c_46717,plain,
( ( select(a_1103,i13) = e_1131 )
| ( i30 = i13 ) ),
inference(superposition,[status(thm),theory(equality)],[c_46694,c_1582]) ).
tff(c_46737,plain,
select(a_1103,i13) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_406,c_46717]) ).
tff(c_46760,plain,
( ( select(a_1102,i13) = e_1131 )
| ( i9 = i13 ) ),
inference(superposition,[status(thm),theory(equality)],[c_46737,c_1618]) ).
tff(c_46780,plain,
select(a_1102,i13) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_588,c_46760]) ).
tff(c_46803,plain,
( ( select(a_1101,i13) = e_1131 )
| ( i4 = i13 ) ),
inference(superposition,[status(thm),theory(equality)],[c_46780,c_1495]) ).
tff(c_46823,plain,
select(a_1101,i13) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_818,c_46803]) ).
tff(c_1501,plain,
! [J_17] :
( ( select(a_1101,J_17) = select(a_1100,J_17) )
| ( i19 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_72,c_1467]) ).
tff(c_46847,plain,
( ( select(a_1100,i13) = e_1131 )
| ( i19 = i13 ) ),
inference(superposition,[status(thm),theory(equality)],[c_46823,c_1501]) ).
tff(c_46867,plain,
select(a_1100,i13) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_428,c_46847]) ).
tff(c_70,plain,
store(a_1099,i1,e1) = a_1100,
inference(cnfTransformation,[status(thm)],[f_64]) ).
tff(c_1513,plain,
! [J_17] :
( ( select(a_1100,J_17) = select(a_1099,J_17) )
| ( i1 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_70,c_1467]) ).
tff(c_46890,plain,
( ( select(a_1099,i13) = e_1131 )
| ( i13 = i1 ) ),
inference(superposition,[status(thm),theory(equality)],[c_46867,c_1513]) ).
tff(c_46910,plain,
( ( e_1131 = e13 )
| ( i13 = i1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1281,c_46890]) ).
tff(c_46912,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_980,c_43395,c_46910]) ).
tff(c_46913,plain,
select(a_1080,i_1129) = e_1130,
inference(splitRight,[status(thm)],[c_37178]) ).
tff(c_46983,plain,
( ( select(a_1079,i_1129) = e_1130 )
| ( i_1129 = i12 ) ),
inference(superposition,[status(thm),theory(equality)],[c_46913,c_1531]) ).
tff(c_47002,plain,
select(a_1079,i_1129) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_19808,c_46983]) ).
tff(c_47018,plain,
( ( select(a_1078,i_1129) = e_1130 )
| ( i_1129 = i11 ) ),
inference(superposition,[status(thm),theory(equality)],[c_47002,c_1543]) ).
tff(c_47037,plain,
select(a_1078,i_1129) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_39774,c_47018]) ).
tff(c_47070,plain,
( ( select(a_1077,i_1129) = e_1130 )
| ( i_1129 = i10 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1567,c_47037]) ).
tff(c_47079,plain,
select(a_1077,i_1129) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_6290,c_47070]) ).
tff(c_47184,plain,
select(a_1077,i8) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_47182,c_47079]) ).
tff(c_50496,plain,
( ( select(a_1076,i8) = e_1130 )
| ( i9 = i8 ) ),
inference(superposition,[status(thm),theory(equality)],[c_47184,c_1591]) ).
tff(c_50516,plain,
( ( e_1130 = e8 )
| ( i9 = i8 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1434,c_50496]) ).
tff(c_50518,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_638,c_47260,c_50516]) ).
tff(c_50520,plain,
i_1129 != i8,
inference(splitRight,[status(thm)],[c_43236]) ).
tff(c_554,plain,
i9 != i30,
inference(cnfTransformation,[status(thm)],[f_517]) ).
tff(c_1374,plain,
select(a_1077,i9) = e9,
inference(superposition,[status(thm),theory(equality)],[c_24,c_1257]) ).
tff(c_47091,plain,
( ( select(a_1076,i_1129) = e_1130 )
| ( i_1129 = i9 ) ),
inference(superposition,[status(thm),theory(equality)],[c_47079,c_1591]) ).
tff(c_50755,plain,
i_1129 = i9,
inference(splitLeft,[status(thm)],[c_47091]) ).
tff(c_50765,plain,
select(a_1077,i9) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_50755,c_47079]) ).
tff(c_50836,plain,
e_1130 = e9,
inference(demodulation,[status(thm),theory(equality)],[c_1374,c_50765]) ).
tff(c_50841,plain,
e_1131 != e9,
inference(demodulation,[status(thm),theory(equality)],[c_50836,c_1004]) ).
tff(c_1401,plain,
select(a_1103,i9) = e9,
inference(superposition,[status(thm),theory(equality)],[c_76,c_1257]) ).
tff(c_932,plain,
i9 != i2,
inference(cnfTransformation,[status(thm)],[f_895]) ).
tff(c_584,plain,
i9 != i15,
inference(cnfTransformation,[status(thm)],[f_547]) ).
tff(c_16914,plain,
i_1129 != i25,
inference(splitRight,[status(thm)],[c_15883]) ).
tff(c_32805,plain,
i_1129 != i18,
inference(splitRight,[status(thm)],[c_29867]) ).
tff(c_27137,plain,
i_1129 != i20,
inference(splitRight,[status(thm)],[c_25042]) ).
tff(c_50519,plain,
select(a_1109,i_1129) = e_1131,
inference(splitRight,[status(thm)],[c_43236]) ).
tff(c_50530,plain,
( ( select(a_1108,i_1129) = e_1131 )
| ( i_1129 = i20 ) ),
inference(superposition,[status(thm),theory(equality)],[c_50519,c_1633]) ).
tff(c_50549,plain,
select(a_1108,i_1129) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_27137,c_50530]) ).
tff(c_50565,plain,
( ( select(a_1107,i_1129) = e_1131 )
| ( i_1129 = i18 ) ),
inference(superposition,[status(thm),theory(equality)],[c_50549,c_1660]) ).
tff(c_50584,plain,
select(a_1107,i_1129) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_32805,c_50565]) ).
tff(c_50602,plain,
( ( select(a_1106,i_1129) = e_1131 )
| ( i_1129 = i25 ) ),
inference(superposition,[status(thm),theory(equality)],[c_50584,c_1612]) ).
tff(c_50621,plain,
select(a_1106,i_1129) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_16914,c_50602]) ).
tff(c_50759,plain,
select(a_1106,i9) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_50755,c_50621]) ).
tff(c_51152,plain,
( ( select(a_1105,i9) = e_1131 )
| ( i9 = i15 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1621,c_50759]) ).
tff(c_51161,plain,
select(a_1105,i9) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_584,c_51152]) ).
tff(c_54248,plain,
( ( select(a_1104,i9) = e_1131 )
| ( i9 = i2 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1600,c_51161]) ).
tff(c_54258,plain,
select(a_1104,i9) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_932,c_54248]) ).
tff(c_56029,plain,
( ( select(a_1103,i9) = e_1131 )
| ( i9 = i30 ) ),
inference(superposition,[status(thm),theory(equality)],[c_54258,c_1582]) ).
tff(c_56049,plain,
( ( e_1131 = e9 )
| ( i9 = i30 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1401,c_56029]) ).
tff(c_56051,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_554,c_50841,c_56049]) ).
tff(c_56052,plain,
select(a_1076,i_1129) = e_1130,
inference(splitRight,[status(thm)],[c_47091]) ).
tff(c_56063,plain,
( ( select(a_1075,i_1129) = e_1130 )
| ( i_1129 = i8 ) ),
inference(superposition,[status(thm),theory(equality)],[c_56052,c_1651]) ).
tff(c_56082,plain,
select(a_1075,i_1129) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_50520,c_56063]) ).
tff(c_56114,plain,
( ( select(a_1074,i_1129) = e_1130 )
| ( i_1129 = i7 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1510,c_56082]) ).
tff(c_56123,plain,
select(a_1074,i_1129) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_9045,c_56114]) ).
tff(c_56135,plain,
( ( select(a_1073,i_1129) = e_1130 )
| ( i_1129 = i6 ) ),
inference(superposition,[status(thm),theory(equality)],[c_56123,c_1486]) ).
tff(c_56154,plain,
select(a_1073,i_1129) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_43191,c_56135]) ).
tff(c_56171,plain,
( ( select(a_1072,i_1129) = e_1130 )
| ( i_1129 = i5 ) ),
inference(superposition,[status(thm),theory(equality)],[c_56154,c_1519]) ).
tff(c_56190,plain,
select(a_1072,i_1129) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_31361,c_56171]) ).
tff(c_56207,plain,
( ( select(a_1071,i_1129) = e_1130 )
| ( i_1129 = i4 ) ),
inference(superposition,[status(thm),theory(equality)],[c_56190,c_1516]) ).
tff(c_63411,plain,
i_1129 = i4,
inference(splitLeft,[status(thm)],[c_56207]) ).
tff(c_56053,plain,
i_1129 != i9,
inference(splitRight,[status(thm)],[c_47091]) ).
tff(c_11869,plain,
i_1129 != i30,
inference(splitRight,[status(thm)],[c_10723]) ).
tff(c_944,plain,
i3 != i2,
inference(cnfTransformation,[status(thm)],[f_907]) ).
tff(c_1383,plain,
select(a_1105,i2) = e2,
inference(superposition,[status(thm),theory(equality)],[c_80,c_1257]) ).
tff(c_37133,plain,
i_1129 != i15,
inference(splitRight,[status(thm)],[c_32903]) ).
tff(c_50654,plain,
( ( select(a_1105,i_1129) = e_1131 )
| ( i_1129 = i15 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1621,c_50621]) ).
tff(c_50663,plain,
select(a_1105,i_1129) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_37133,c_50654]) ).
tff(c_50728,plain,
( ( select(a_1104,i_1129) = e_1131 )
| ( i_1129 = i2 ) ),
inference(superposition,[status(thm),theory(equality)],[c_50663,c_1600]) ).
tff(c_56235,plain,
i_1129 = i2,
inference(splitLeft,[status(thm)],[c_50728]) ).
tff(c_56242,plain,
select(a_1105,i2) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_56235,c_50663]) ).
tff(c_56321,plain,
e_1131 = e2,
inference(demodulation,[status(thm),theory(equality)],[c_1383,c_56242]) ).
tff(c_56326,plain,
e_1130 != e2,
inference(demodulation,[status(thm),theory(equality)],[c_56321,c_1004]) ).
tff(c_10,plain,
store(a_1069,i2,e2) = a_1070,
inference(cnfTransformation,[status(thm)],[f_34]) ).
tff(c_1410,plain,
select(a_1070,i2) = e2,
inference(superposition,[status(thm),theory(equality)],[c_10,c_1257]) ).
tff(c_942,plain,
i4 != i2,
inference(cnfTransformation,[status(thm)],[f_905]) ).
tff(c_56236,plain,
select(a_1072,i2) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_56235,c_56190]) ).
tff(c_61805,plain,
( ( select(a_1071,i2) = e_1130 )
| ( i4 = i2 ) ),
inference(superposition,[status(thm),theory(equality)],[c_56236,c_1516]) ).
tff(c_61825,plain,
select(a_1071,i2) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_942,c_61805]) ).
tff(c_1492,plain,
! [J_17] :
( ( select(a_1071,J_17) = select(a_1070,J_17) )
| ( i3 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_12,c_1467]) ).
tff(c_61934,plain,
( ( select(a_1070,i2) = e_1130 )
| ( i3 = i2 ) ),
inference(superposition,[status(thm),theory(equality)],[c_61825,c_1492]) ).
tff(c_61954,plain,
( ( e_1130 = e2 )
| ( i3 = i2 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_1410,c_61934]) ).
tff(c_61956,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_944,c_56326,c_61954]) ).
tff(c_61957,plain,
select(a_1104,i_1129) = e_1131,
inference(splitRight,[status(thm)],[c_50728]) ).
tff(c_61968,plain,
( ( select(a_1103,i_1129) = e_1131 )
| ( i_1129 = i30 ) ),
inference(superposition,[status(thm),theory(equality)],[c_61957,c_1582]) ).
tff(c_61987,plain,
select(a_1103,i_1129) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_11869,c_61968]) ).
tff(c_62067,plain,
( ( select(a_1102,i_1129) = e_1131 )
| ( i_1129 = i9 ) ),
inference(superposition,[status(thm),theory(equality)],[c_61987,c_1618]) ).
tff(c_62086,plain,
select(a_1102,i_1129) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_56053,c_62067]) ).
tff(c_63412,plain,
select(a_1102,i4) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_63411,c_62086]) ).
tff(c_63502,plain,
e_1131 = e4,
inference(demodulation,[status(thm),theory(equality)],[c_1278,c_63412]) ).
tff(c_63508,plain,
e_1130 != e4,
inference(demodulation,[status(thm),theory(equality)],[c_63502,c_1004]) ).
tff(c_1299,plain,
select(a_1072,i4) = e4,
inference(superposition,[status(thm),theory(equality)],[c_14,c_1257]) ).
tff(c_63417,plain,
select(a_1072,i4) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_63411,c_56190]) ).
tff(c_63503,plain,
e_1130 = e4,
inference(demodulation,[status(thm),theory(equality)],[c_1299,c_63417]) ).
tff(c_63513,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_63508,c_63503]) ).
tff(c_63515,plain,
i_1129 != i4,
inference(splitRight,[status(thm)],[c_56207]) ).
tff(c_62119,plain,
( ( select(a_1101,i_1129) = e_1131 )
| ( i_1129 = i4 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1495,c_62086]) ).
tff(c_63704,plain,
select(a_1101,i_1129) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_63515,c_62119]) ).
tff(c_63720,plain,
( ( select(a_1100,i_1129) = e_1131 )
| ( i_1129 = i19 ) ),
inference(superposition,[status(thm),theory(equality)],[c_63704,c_1501]) ).
tff(c_63740,plain,
select(a_1100,i_1129) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_29779,c_63720]) ).
tff(c_63762,plain,
( ( select(a_1099,i_1129) = e_1131 )
| ( i_1129 = i1 ) ),
inference(superposition,[status(thm),theory(equality)],[c_63740,c_1513]) ).
tff(c_63790,plain,
i_1129 = i1,
inference(splitLeft,[status(thm)],[c_63762]) ).
tff(c_61958,plain,
i_1129 != i2,
inference(splitRight,[status(thm)],[c_50728]) ).
tff(c_22886,plain,
i_1129 != i3,
inference(splitRight,[status(thm)],[c_19812]) ).
tff(c_63514,plain,
select(a_1071,i_1129) = e_1130,
inference(splitRight,[status(thm)],[c_56207]) ).
tff(c_63531,plain,
( ( select(a_1070,i_1129) = e_1130 )
| ( i_1129 = i3 ) ),
inference(superposition,[status(thm),theory(equality)],[c_63514,c_1492]) ).
tff(c_63551,plain,
select(a_1070,i_1129) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_22886,c_63531]) ).
tff(c_1627,plain,
! [J_17] :
( ( select(a_1070,J_17) = select(a_1069,J_17) )
| ( i2 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_10,c_1467]) ).
tff(c_63573,plain,
( ( select(a_1069,i_1129) = e_1130 )
| ( i_1129 = i2 ) ),
inference(superposition,[status(thm),theory(equality)],[c_63551,c_1627]) ).
tff(c_63593,plain,
select(a_1069,i_1129) = e_1130,
inference(negUnitSimplification,[status(thm)],[c_61958,c_63573]) ).
tff(c_64367,plain,
select(a_1069,i1) = e_1130,
inference(demodulation,[status(thm),theory(equality)],[c_63790,c_63593]) ).
tff(c_64462,plain,
e_1130 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_1344,c_64367]) ).
tff(c_1296,plain,
select(a_1100,i1) = e1,
inference(superposition,[status(thm),theory(equality)],[c_70,c_1257]) ).
tff(c_64364,plain,
select(a_1100,i1) = e_1131,
inference(demodulation,[status(thm),theory(equality)],[c_63790,c_63740]) ).
tff(c_64461,plain,
e_1131 = e1,
inference(demodulation,[status(thm),theory(equality)],[c_1296,c_64364]) ).
tff(c_64467,plain,
e_1130 != e1,
inference(demodulation,[status(thm),theory(equality)],[c_64461,c_1004]) ).
tff(c_64477,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_64462,c_64467]) ).
tff(c_64479,plain,
i_1129 != i1,
inference(splitRight,[status(thm)],[c_63762]) ).
tff(c_46914,plain,
i_1129 != i13,
inference(splitRight,[status(thm)],[c_37178]) ).
tff(c_64478,plain,
select(a_1099,i_1129) = e_1131,
inference(splitRight,[status(thm)],[c_63762]) ).
tff(c_1498,plain,
! [J_17] :
( ( select(a_1099,J_17) = select(a1,J_17) )
| ( i13 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_68,c_1467]) ).
tff(c_64495,plain,
( ( select(a1,i_1129) = e_1131 )
| ( i_1129 = i13 ) ),
inference(superposition,[status(thm),theory(equality)],[c_64478,c_1498]) ).
tff(c_64515,plain,
select(a1,i_1129) = e_1131,
inference(negUnitSimplification,[status(thm)],[c_46914,c_64495]) ).
tff(c_1561,plain,
! [J_17] :
( ( select(a_1069,J_17) = select(a1,J_17) )
| ( i1 = J_17 ) ),
inference(superposition,[status(thm),theory(equality)],[c_8,c_1467]) ).
tff(c_63632,plain,
( ( select(a1,i_1129) = e_1130 )
| ( i_1129 = i1 ) ),
inference(superposition,[status(thm),theory(equality)],[c_1561,c_63593]) ).
tff(c_65132,plain,
( ( e_1131 = e_1130 )
| ( i_1129 = i1 ) ),
inference(demodulation,[status(thm),theory(equality)],[c_64515,c_63632]) ).
tff(c_65133,plain,
$false,
inference(negUnitSimplification,[status(thm)],[c_64479,c_1004,c_65132]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : SWV527-1.030 : TPTP v9.0.0. Released v4.0.0.
% 0.10/0.12 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.33 % Computer : n015.cluster.edu
% 0.13/0.33 % Model : x86_64 x86_64
% 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.33 % Memory : 8042.1875MB
% 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.33 % CPULimit : 300
% 0.13/0.33 % WCLimit : 300
% 0.13/0.33 % DateTime : Wed Apr 9 03:51:35 EDT 2025
% 0.13/0.33 % CPUTime :
% 60.11/36.62 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 60.69/36.99
% 60.69/36.99 % SZS output start CNFRefutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------