% ott+10_128_av=off:bs=on:gsp=input_only:irw=on:lcm=predicate:lma=on:nm=0:nwc=1:sp=occurrence:urr=on:updr=off:uhcvi=on_4 on CCC01CC2N0C3N3CC43C40 % Time limit reached! % ------------------------------ % Version: Vampire 4.5.1 (commit 57a6f78c on 2020-07-15 11:59:04 +0200) % Termination reason: Time limit % Termination phase: Saturation % Memory used [KB]: 12665 % Time elapsed: 0.800 s % ------------------------------ % ------------------------------ % fmb+10_1_av=off:bce=on:nm=6_1461 on CCC01CC2N0C3N3CC43C40 TRYING [5] % Time limit reached! % ------------------------------ % Version: Vampire 4.5.1 (commit 57a6f78c on 2020-07-15 11:59:04 +0200) % Termination reason: Time limit % Termination phase: Finite model building SAT solving % Memory used [KB]: 48613 % Time elapsed: 190.100 s % ------------------------------ % ------------------------------ % dis+10_3_add=large:afp=10000:afq=2.0:amm=sco:anc=none:cond=on:fsr=off:gsp=input_only:lma=on:nm=16:nwc=1:sac=on:updr=off_197 on CCC01CC2N0C3N3CC43C40 % Time limit reached! % ------------------------------ % Version: Vampire 4.5.1 (commit 57a6f78c on 2020-07-15 11:59:04 +0200) % Termination reason: Time limit % Termination phase: Saturation % Memory used [KB]: 856489 % Time elapsed: 25.800 s % ------------------------------ % ------------------------------ % dis+1_3_av=off:cond=on:nm=64:newcnf=on:nwc=1_87 on CCC01CC2N0C3N3CC43C40 % Time limit reached! % ------------------------------ % Version: Vampire 4.5.1 (commit 57a6f78c on 2020-07-15 11:59:04 +0200) % Termination reason: Time limit % Memory used [KB]: 485109 % Time elapsed: 11.533 s % ------------------------------ % ------------------------------ % ott-3_5_awrs=decay:awrsf=128:afr=on:afp=40000:afq=1.0:amm=off:anc=none:bce=on:cond=fast:lma=on:nm=64:newcnf=on:nwc=1.1:sas=z3:sp=frequency:updr=off_146 on CCC01CC2N0C3N3CC43C40 % Time limit reached! % ------------------------------ % Version: Vampire 4.5.1 (commit 57a6f78c on 2020-07-15 11:59:04 +0200) % Termination reason: Time limit % Termination phase: Saturation % Memory used [KB]: 26097 % Time elapsed: 19.100 s % ------------------------------ % ------------------------------ % ott+2_5_afp=4000:afq=2.0:anc=none:bce=on:fsr=off:gsp=input_only:lma=on:nm=32:nwc=1:sp=reverse_arity_315 on CCC01CC2N0C3N3CC43C40 % Time limit reached! % ------------------------------ % Version: Vampire 4.5.1 (commit 57a6f78c on 2020-07-15 11:59:04 +0200) % Termination reason: Time limit % Termination phase: Saturation % Memory used [KB]: 2165465 % Time elapsed: 41.100 s % ------------------------------ % ------------------------------ % fmb+10_1_av=off:bce=on:fmbes=smt:fmbsr=1.4:fde=none:ile=on:updr=off_600 on CCC01CC2N0C3N3CC43C40 TRYING [5] % Time limit reached! % ------------------------------ % Version: Vampire 4.5.1 (commit 57a6f78c on 2020-07-15 11:59:04 +0200) % Termination reason: Time limit % Termination phase: Finite model building SAT solving % Memory used [KB]: 31598 % Time elapsed: 78.200 s % ------------------------------ % ------------------------------ % fmb+10_1_av=off:bce=on:fmbsr=1.3:nm=2:newcnf=on_1200 on CCC01CC2N0C3N3CC43C40 TRYING [5] % Time limit reached! % ------------------------------ % Version: Vampire 4.5.1 (commit 57a6f78c on 2020-07-15 11:59:04 +0200) % Termination reason: Time limit % Termination phase: Finite model building SAT solving % Memory used [KB]: 44263 % Time elapsed: 156.200 s % ------------------------------ % ------------------------------ % fmb+10_1_av=off:fmbsr=1.1:updr=off_300 on CCC01CC2N0C3N3CC43C40 TRYING [5] % Time limit reached! % ------------------------------ % Version: Vampire 4.5.1 (commit 57a6f78c on 2020-07-15 11:59:04 +0200) % Termination reason: Time limit % Termination phase: Finite model building SAT solving % Memory used [KB]: 25202 % Time elapsed: 39.200 s % ------------------------------ % ------------------------------ % fmb+10_1_av=off:fmbsr=1.6_1200 on CCC01CC2N0C3N3CC43C40 TRYING [5] % Time limit reached! % ------------------------------ % Version: Vampire 4.5.1 (commit 57a6f78c on 2020-07-15 11:59:04 +0200) % Termination reason: Time limit % Termination phase: Finite model building SAT solving % Memory used [KB]: 38378 % Time elapsed: 156.200 s % ------------------------------ % ------------------------------ % fmb+10_1_av=off:fde=unused:ile=on:irw=on:lcm=predicate:lma=on:nm=16:nwc=1.7:sos=all:sp=reverse_arity_300 on CCC01CC2N0C3N3CC43C40 TRYING [5] % Time limit reached! % ------------------------------ % Version: Vampire 4.5.1 (commit 57a6f78c on 2020-07-15 11:59:04 +0200) % Termination reason: Time limit % Termination phase: Finite model building SAT solving % Memory used [KB]: 25330 % Time elapsed: 39.200 s % ------------------------------ % ------------------------------ % fmb+10_1_av=off:fmbsr=1.5:updr=off_300 on CCC01CC2N0C3N3CC43C40 TRYING [5] % Time limit reached! % ------------------------------ % Version: Vampire 4.5.1 (commit 57a6f78c on 2020-07-15 11:59:04 +0200) % Termination reason: Time limit % Termination phase: Finite model building SAT solving % Memory used [KB]: 25074 % Time elapsed: 39.200 s % ------------------------------ % ------------------------------ % lrs+11_6_aac=none:add=off:afp=100000:afq=1.1:amm=off:anc=none:bd=off:fsr=off:gs=on:gsem=off:nwc=1:sas=z3:sp=occurrence_300 on CCC01CC2N0C3N3CC43C40 % Time limit reached! % ------------------------------ % Version: Vampire 4.5.1 (commit 57a6f78c on 2020-07-15 11:59:04 +0200) % Termination reason: Time limit % Termination phase: Saturation % Memory used [KB]: 931967 % Time elapsed: 39.200 s % ------------------------------ % ------------------------------ % fmb+10_1_av=off:fmbsr=1.4_300 on CCC01CC2N0C3N3CC43C40 TRYING [5] % Time limit reached! % ------------------------------ % Version: Vampire 4.5.1 (commit 57a6f78c on 2020-07-15 11:59:04 +0200) % Termination reason: Time limit % Termination phase: Finite model building SAT solving % Memory used [KB]: 25458 % Time elapsed: 39.200 s % ------------------------------ % ------------------------------ % dis+11_5_add=large:afr=on:afp=1000:afq=1.0:anc=none:bsr=on:fsr=off:nm=64:newcnf=on:nwc=1:updr=off_300 on CCC01CC2N0C3N3CC43C40 % SZS status CounterSatisfiable for CCC01CC2N0C3N3CC43C40 % # SZS output start Saturation. tff(u3649,axiom, (![X1, X0] : ((~t(i(X0,X1)) | ~t(X0) | t(X1))))). tff(u3648,axiom, (![X1, X0, X2] : ((~t(i(X0,X1)) | ~t(X0) | t(i(n(X1),X2)))))). tff(u3647,axiom, (![X11, X13, X10, X12] : ((~t(i(X10,X11)) | t(i(n(i(n(X11),X12)),X13)) | ~t(X10))))). tff(u3646,axiom, (![X16, X13, X15, X12, X14] : ((~t(i(X16,X12)) | ~t(X16) | t(i(n(i(n(i(n(X12),X13)),X14)),X15)))))). tff(u3645,axiom, (![X16, X18, X15, X17, X19, X14] : ((~t(i(X14,X15)) | t(i(n(i(n(i(n(i(n(X15),X16)),X17)),X18)),X19)) | ~t(X14))))). tff(u3644,axiom, (![X51, X53, X55, X56, X52, X54, X57] : ((~t(i(X57,X51)) | ~t(X57) | t(i(n(i(n(i(n(i(n(i(n(X51),X52)),X53)),X54)),X55)),X56)))))). tff(u3643,axiom, (![X82, X84, X86, X79, X81, X83, X85, X80] : ((~t(i(X79,X80)) | t(i(n(i(n(i(n(i(n(i(n(i(n(X80),X81)),X82)),X83)),X84)),X85)),X86)) | ~t(X79))))). tff(u3642,axiom, (![X113, X115, X117, X119, X120, X114, X116, X118, X121] : ((~t(i(X121,X113)) | ~t(X121) | t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(X113),X114)),X115)),X116)),X117)),X118)),X119)),X120)))))). tff(u3641,axiom, (![X160, X162, X153, X155, X157, X159, X161, X154, X156, X158] : ((~t(i(X153,X154)) | t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(X154),X155)),X156)),X157)),X158)),X159)),X160)),X161)),X162)) | ~t(X153))))). tff(u3640,axiom, (![X201, X203, X205, X207, X199, X209, X200, X202, X204, X206, X208] : ((~t(i(X209,X199)) | ~t(X209) | t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(X199),X200)),X201)),X202)),X203)),X204)),X205)),X206)),X207)),X208)))))). tff(u3639,axiom, (![X254, X256, X258, X252, X262, X260, X253, X257, X259, X251, X255, X261] : ((~t(i(X251,X252)) | t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(X252),X253)),X254)),X255)),X256)),X257)),X258)),X259)),X260)),X261)),X262)) | ~t(X251))))). tff(u3638,axiom, (![X319, X317, X311, X309, X320, X314, X312, X318, X316, X310, X321, X315, X313] : ((~t(i(X321,X309)) | ~t(X321) | t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(X309),X310)),X311)),X312)),X313)),X314)),X315)),X316)),X317)),X318)),X319)),X320)))))). tff(u3637,axiom, (![X381, X375, X373, X386, X384, X378, X376, X382, X380, X374, X385, X379, X377, X383] : ((~t(i(X373,X374)) | t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(X374),X375)),X376)),X377)),X378)),X379)),X380)),X381)),X382)),X383)),X384)),X385)),X386)) | ~t(X373))))). tff(u3636,axiom, (![X456, X450, X448, X454, X452, X446, X444, X457, X451, X449, X455, X453, X443, X447, X445] : ((~t(i(X457,X443)) | ~t(X457) | t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(X443),X444)),X445)),X446)),X447)),X448)),X449)),X450)),X451)),X452)),X453)),X454)),X455)),X456)))))). tff(u3635,axiom, (![X519, X523, X521, X527, X525, X531, X529, X533, X522, X520, X526, X524, X530, X528, X534, X532] : ((~t(i(X519,X520)) | t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(X520),X521)),X522)),X523)),X524)),X525)),X526)),X527)),X528)),X529)),X530)),X531)),X532)),X533)),X534)) | ~t(X519))))). tff(u3634,axiom, (![X610, X608, X614, X612, X616, X603, X605, X601, X607, X611, X609, X615, X613, X617, X602, X604, X606] : ((~t(i(X617,X601)) | ~t(X617) | t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(X601),X602)),X603)),X604)),X605)),X606)),X607)),X608)),X609)),X610)),X611)),X612)),X613)),X614)),X615)),X616)))))). tff(u3633,axiom, (![X705, X701, X692, X690, X694, X696, X698, X702, X706, X704, X700, X691, X693, X689, X695, X697, X699, X703] : ((~t(i(X689,X690)) | t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(X690),X691)),X692)),X693)),X694)),X695)),X696)),X697)),X698)),X699)),X700)),X701)),X702)),X703)),X704)),X705)),X706)) | ~t(X689))))). tff(u3632,axiom, (![X792, X794, X801, X789, X791, X785, X787, X797, X799, X793, X795, X800, X783, X788, X790, X784, X786, X796, X798] : ((~t(i(X801,X783)) | ~t(X801) | t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(X783),X784)),X785)),X786)),X787)),X788)),X789)),X790)),X791)),X792)),X793)),X794)),X795)),X796)),X797)),X798)),X799)),X800)))))). tff(u3631,axiom, (![X900, X902, X896, X898, X884, X886, X888, X892, X894, X901, X890, X897, X899, X885, X887, X889, X891, X883, X893, X895] : ((~t(i(X883,X884)) | t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(X884),X885)),X886)),X887)),X888)),X889)),X890)),X891)),X892)),X893)),X894)),X895)),X896)),X897)),X898)),X899)),X900)),X901)),X902)) | ~t(X883))))). tff(u3630,negated_conjecture, ~t(i(i(i(i(i(sK0,sK1),i(n(sK2),n(sK3))),sK2),sK4),i(i(sK4,sK0),i(sK3,sK0))))). tff(u3629,axiom, (![X1, X3, X0, X2, X4] : ((~t(i(i(X0,X1),i(i(X2,n(X0)),i(X3,n(X3))))) | t(i(i(X4,X3),i(X4,X0))))))). tff(u3628,axiom, (![X1, X3, X5, X0, X2, X4] : ((~t(i(i(X0,X1),i(i(X2,n(X0)),i(X3,n(X3))))) | t(i(n(i(i(X4,X3),i(X4,X0))),X5)))))). tff(u3627,axiom, (![X1, X3, X5, X0, X2, X4, X6] : ((~t(i(i(X2,X5),i(i(X6,n(X2)),i(X1,n(X1))))) | t(i(n(i(n(i(i(X0,X1),i(X0,X2))),X3)),X4)))))). tff(u3626,axiom, (![X1, X3, X5, X7, X0, X2, X4, X6] : ((~t(i(i(X0,X1),i(i(X2,n(X0)),i(X3,n(X3))))) | t(i(n(i(n(i(n(i(i(X4,X3),i(X4,X0))),X5)),X6)),X7)))))). tff(u3625,axiom, (![X40, X42, X36, X38, X41, X43, X35, X37, X39] : ((~t(i(i(X37,X42),i(i(X43,n(X37)),i(X36,n(X36))))) | t(i(n(i(n(i(n(i(n(i(i(X35,X36),i(X35,X37))),X38)),X39)),X40)),X41)))))). tff(u3624,axiom, (![X63, X65, X67, X69, X62, X64, X66, X68, X70, X61] : ((~t(i(i(X61,X62),i(i(X63,n(X61)),i(X64,n(X64))))) | t(i(n(i(n(i(n(i(n(i(n(i(i(X65,X64),i(X65,X61))),X66)),X67)),X68)),X69)),X70)))))). tff(u3623,axiom, (![X96, X98, X100, X102, X93, X95, X97, X99, X101, X103, X94] : ((~t(i(i(X95,X102),i(i(X103,n(X95)),i(X94,n(X94))))) | t(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X93,X94),i(X93,X95))),X96)),X97)),X98)),X99)),X100)),X101)))))). tff(u3622,axiom, (![X137, X139, X141, X131, X133, X135, X136, X138, X140, X142, X132, X134] : ((~t(i(i(X131,X132),i(i(X133,n(X131)),i(X134,n(X134))))) | t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X135,X134),i(X135,X131))),X136)),X137)),X138)),X139)),X140)),X141)),X142)))))). tff(u3621,axiom, (![X179, X181, X183, X184, X186, X176, X178, X180, X182, X175, X185, X187, X177] : ((~t(i(i(X177,X186),i(i(X187,n(X177)),i(X176,n(X176))))) | t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X175,X176),i(X175,X177))),X178)),X179)),X180)),X181)),X182)),X183)),X184)),X185)))))). tff(u3620,axiom, (![X232, X234, X236, X238, X226, X228, X230, X233, X235, X237, X225, X227, X229, X231] : ((~t(i(i(X225,X226),i(i(X227,n(X225)),i(X228,n(X228))))) | t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X229,X228),i(X229,X225))),X230)),X231)),X232)),X233)),X234)),X235)),X236)),X237)),X238)))))). tff(u3619,axiom, (![X286, X284, X289, X291, X293, X295, X283, X281, X287, X285, X288, X290, X292, X294, X282] : ((~t(i(i(X283,X294),i(i(X295,n(X283)),i(X282,n(X282))))) | t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X281,X282),i(X281,X283))),X284)),X285)),X286)),X287)),X288)),X289)),X290)),X291)),X292)),X293)))))). tff(u3618,axiom, (![X348, X355, X353, X347, X357, X345, X351, X349, X343, X352, X354, X356, X358, X346, X344, X350] : ((~t(i(i(X343,X344),i(i(X345,n(X343)),i(X346,n(X346))))) | t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X347,X346),i(X347,X343))),X348)),X349)),X350)),X351)),X352)),X353)),X354)),X355)),X356)),X357)),X358)))))). tff(u3617,axiom, (![X427, X425, X411, X419, X417, X423, X421, X415, X413, X426, X424, X418, X416, X422, X420, X414, X412] : ((~t(i(i(X413,X426),i(i(X427,n(X413)),i(X412,n(X412))))) | t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X411,X412),i(X411,X413))),X414)),X415)),X416)),X417)),X418)),X419)),X420)),X421)),X422)),X423)),X424)),X425)))))). tff(u3616,axiom, (![X497, X501, X491, X489, X495, X493, X487, X485, X498, X496, X502, X500, X490, X488, X494, X492, X486, X499] : ((~t(i(i(X485,X486),i(i(X487,n(X485)),i(X488,n(X488))))) | t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X489,X488),i(X489,X485))),X490)),X491)),X492)),X493)),X494)),X495)),X496)),X497)),X498)),X499)),X500)),X501)),X502)))))). tff(u3615,axiom, (![X579, X577, X583, X581, X566, X570, X568, X574, X572, X578, X576, X582, X580, X567, X565, X571, X569, X575, X573] : ((~t(i(i(X567,X582),i(i(X583,n(X567)),i(X566,n(X566))))) | t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X565,X566),i(X565,X567))),X568)),X569)),X570)),X571)),X572)),X573)),X574)),X575)),X576)),X577)),X578)),X579)),X580)),X581)))))). tff(u3614,axiom, (![X655, X651, X657, X659, X653, X661, X665, X663, X669, X667, X656, X658, X660, X654, X652, X662, X664, X670, X668, X666] : ((~t(i(i(X651,X652),i(i(X653,n(X651)),i(X654,n(X654))))) | t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X655,X654),i(X655,X651))),X656)),X657)),X658)),X659)),X660)),X661)),X662)),X663)),X664)),X665)),X666)),X667)),X668)),X669)),X670)))))). tff(u3613,axiom, (![X746, X744, X750, X748, X754, X752, X758, X756, X762, X760, X743, X747, X745, X751, X749, X755, X753, X759, X757, X763, X761] : ((~t(i(i(X745,X762),i(i(X763,n(X745)),i(X744,n(X744))))) | t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X743,X744),i(X743,X745))),X746)),X747)),X748)),X749)),X750)),X751)),X752)),X753)),X754)),X755)),X756)),X757)),X758)),X759)),X760)),X761)))))). tff(u3612,axiom, (![X862, X856, X858, X844, X846, X853, X842, X855, X849, X851, X861, X857, X859, X845, X847, X841, X843, X852, X854, X848, X850, X860] : ((~t(i(i(X841,X842),i(i(X843,n(X841)),i(X844,n(X844))))) | t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X845,X844),i(X845,X841))),X846)),X847)),X848)),X849)),X850)),X851)),X852)),X853)),X854)),X855)),X856)),X857)),X858)),X859)),X860)),X861)),X862)))))). tff(u3611,axiom, (![X959, X964, X966, X960, X962, X948, X950, X952, X954, X956, X946, X958, X965, X967, X961, X963, X945, X949, X951, X953, X955, X947, X957] : ((~t(i(i(X947,X966),i(i(X967,n(X947)),i(X946,n(X946))))) | t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X945,X946),i(X945,X947))),X948)),X949)),X950)),X951)),X952)),X953)),X954)),X955)),X956)),X957)),X958)),X959)),X960)),X961)),X962)),X963)),X964)),X965)))))). tff(u3610,axiom, ((~(![X1, X5, X0, X6] : ((~t(n(i(n(i(X0,i(n(X1),X5))),X6))) | ~t(i(X0,X1)))))) | (![X1, X5, X0, X6] : ((~t(n(i(n(i(X0,i(n(X1),X5))),X6))) | ~t(i(X0,X1))))))). tff(u3609,axiom, ((~(![X5, X7, X8, X6] : (~t(n(i(n(i(i(X5,X6),i(X5,i(n(X6),X7)))),X8)))))) | (![X5, X7, X8, X6] : (~t(n(i(n(i(i(X5,X6),i(X5,i(n(X6),X7)))),X8))))))). tff(u3608,axiom, ((~(![X1, X3, X0, X2, X4] : ((~t(n(i(n(i(n(i(X0,i(n(X1),X2))),X3)),X4))) | ~t(i(X0,X1)))))) | (![X1, X3, X0, X2, X4] : ((~t(n(i(n(i(n(i(X0,i(n(X1),X2))),X3)),X4))) | ~t(i(X0,X1))))))). tff(u3607,axiom, ((~(![X1, X3, X0, X2, X4] : (~t(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)))))) | (![X1, X3, X0, X2, X4] : (~t(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4))))))). tff(u3606,axiom, ((~(![X9, X1, X7, X8, X10, X0] : ((~t(n(i(n(i(n(i(n(i(X0,i(n(X1),X7))),X8)),X9)),X10))) | ~t(i(X0,X1)))))) | (![X9, X1, X7, X8, X10, X0] : ((~t(n(i(n(i(n(i(n(i(X0,i(n(X1),X7))),X8)),X9)),X10))) | ~t(i(X0,X1))))))). tff(u3605,axiom, ((~(![X1, X3, X5, X0, X2, X4] : (~t(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)))))) | (![X1, X3, X5, X0, X2, X4] : (~t(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5))))))). tff(u3604,axiom, ((~(![X1, X3, X5, X0, X2, X4, X6] : ((~t(n(i(n(i(n(i(n(i(n(i(X0,i(n(X1),X2))),X3)),X4)),X5)),X6))) | ~t(i(X0,X1)))))) | (![X1, X3, X5, X0, X2, X4, X6] : ((~t(n(i(n(i(n(i(n(i(n(i(X0,i(n(X1),X2))),X3)),X4)),X5)),X6))) | ~t(i(X0,X1))))))). tff(u3603,axiom, ((~(![X1, X3, X5, X0, X2, X4, X6] : (~t(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)))))) | (![X1, X3, X5, X0, X2, X4, X6] : (~t(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6))))))). tff(u3602,axiom, ((~(![X1, X3, X5, X7, X0, X2, X4, X6] : ((~t(n(i(n(i(n(i(n(i(n(i(n(i(X0,i(n(X1),X2))),X3)),X4)),X5)),X6)),X7))) | ~t(i(X0,X1)))))) | (![X1, X3, X5, X7, X0, X2, X4, X6] : ((~t(n(i(n(i(n(i(n(i(n(i(n(i(X0,i(n(X1),X2))),X3)),X4)),X5)),X6)),X7))) | ~t(i(X0,X1))))))). tff(u3601,axiom, ((~(![X1, X3, X5, X7, X0, X2, X4, X6] : (~t(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)))))) | (![X1, X3, X5, X7, X0, X2, X4, X6] : (~t(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7))))))). tff(u3600,axiom, ((~(![X1, X3, X5, X7, X8, X0, X2, X4, X6] : ((~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X0,i(n(X1),X2))),X3)),X4)),X5)),X6)),X7)),X8))) | ~t(i(X0,X1)))))) | (![X1, X3, X5, X7, X8, X0, X2, X4, X6] : ((~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X0,i(n(X1),X2))),X3)),X4)),X5)),X6)),X7)),X8))) | ~t(i(X0,X1))))))). tff(u3599,axiom, ((~(![X1, X3, X5, X7, X8, X0, X2, X4, X6] : (~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)))))) | (![X1, X3, X5, X7, X8, X0, X2, X4, X6] : (~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8))))))). tff(u3598,axiom, ((~(![X9, X1, X3, X5, X7, X8, X0, X2, X4, X6] : ((~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X0,i(n(X1),X2))),X3)),X4)),X5)),X6)),X7)),X8)),X9))) | ~t(i(X0,X1)))))) | (![X9, X1, X3, X5, X7, X8, X0, X2, X4, X6] : ((~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X0,i(n(X1),X2))),X3)),X4)),X5)),X6)),X7)),X8)),X9))) | ~t(i(X0,X1))))))). tff(u3597,axiom, ((~(![X9, X1, X3, X5, X7, X8, X0, X2, X4, X6] : (~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)))))) | (![X9, X1, X3, X5, X7, X8, X0, X2, X4, X6] : (~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9))))))). tff(u3596,axiom, ((~(![X9, X1, X3, X5, X7, X8, X10, X0, X2, X4, X6] : ((~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X0,i(n(X1),X2))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10))) | ~t(i(X0,X1)))))) | (![X9, X1, X3, X5, X7, X8, X10, X0, X2, X4, X6] : ((~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X0,i(n(X1),X2))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10))) | ~t(i(X0,X1))))))). tff(u3595,axiom, ((~(![X9, X1, X3, X5, X7, X8, X10, X0, X2, X4, X6] : (~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)))))) | (![X9, X1, X3, X5, X7, X8, X10, X0, X2, X4, X6] : (~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10))))))). tff(u3594,axiom, ((~(![X9, X1, X3, X5, X7, X8, X10, X0, X2, X4, X6] : (~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(X0),X1)),X2)),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)))))) | (![X9, X1, X3, X5, X7, X8, X10, X0, X2, X4, X6] : (~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(X0),X1)),X2)),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10))))))). tff(u3593,axiom, ((~(![X9, X11, X1, X3, X5, X7, X8, X10, X0, X2, X4, X6] : ((~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X0,i(n(X1),X2))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11))) | ~t(i(X0,X1)))))) | (![X9, X11, X1, X3, X5, X7, X8, X10, X0, X2, X4, X6] : ((~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X0,i(n(X1),X2))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11))) | ~t(i(X0,X1))))))). tff(u3592,axiom, ((~(![X9, X11, X1, X3, X5, X7, X8, X10, X0, X2, X4, X6] : (~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)))))) | (![X9, X11, X1, X3, X5, X7, X8, X10, X0, X2, X4, X6] : (~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11))))))). tff(u3591,axiom, ((~(![X9, X11, X1, X3, X5, X7, X8, X10, X12, X0, X2, X4, X6] : ((~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X0,i(n(X1),X2))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12))) | ~t(i(X0,X1)))))) | (![X9, X11, X1, X3, X5, X7, X8, X10, X12, X0, X2, X4, X6] : ((~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X0,i(n(X1),X2))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12))) | ~t(i(X0,X1))))))). tff(u3590,axiom, ((~(![X9, X11, X1, X3, X5, X7, X8, X10, X12, X0, X2, X4, X6] : (~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)))))) | (![X9, X11, X1, X3, X5, X7, X8, X10, X12, X0, X2, X4, X6] : (~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12))))))). tff(u3589,axiom, ((~(![X9, X11, X13, X1, X3, X5, X7, X8, X10, X12, X0, X2, X4, X6] : ((~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X0,i(n(X1),X2))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13))) | ~t(i(X0,X1)))))) | (![X9, X11, X13, X1, X3, X5, X7, X8, X10, X12, X0, X2, X4, X6] : ((~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X0,i(n(X1),X2))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13))) | ~t(i(X0,X1))))))). tff(u3588,axiom, ((~(![X9, X11, X13, X1, X3, X5, X7, X8, X10, X12, X0, X2, X4, X6] : (~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13)))))) | (![X9, X11, X13, X1, X3, X5, X7, X8, X10, X12, X0, X2, X4, X6] : (~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13))))))). tff(u3587,axiom, ((~(![X9, X11, X13, X1, X3, X5, X7, X8, X10, X12, X14, X0, X2, X4, X6] : ((~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X0,i(n(X1),X2))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13)),X14))) | ~t(i(X0,X1)))))) | (![X9, X11, X13, X1, X3, X5, X7, X8, X10, X12, X14, X0, X2, X4, X6] : ((~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X0,i(n(X1),X2))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13)),X14))) | ~t(i(X0,X1))))))). tff(u3586,axiom, ((~(![X9, X11, X13, X1, X3, X5, X7, X8, X10, X12, X14, X0, X2, X4, X6] : (~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13)),X14)))))) | (![X9, X11, X13, X1, X3, X5, X7, X8, X10, X12, X14, X0, X2, X4, X6] : (~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13)),X14))))))). tff(u3585,axiom, ((~(![X9, X11, X13, X15, X1, X3, X5, X7, X8, X10, X12, X14, X0, X2, X4, X6] : ((~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X0,i(n(X1),X2))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13)),X14)),X15))) | ~t(i(X0,X1)))))) | (![X9, X11, X13, X15, X1, X3, X5, X7, X8, X10, X12, X14, X0, X2, X4, X6] : ((~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X0,i(n(X1),X2))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13)),X14)),X15))) | ~t(i(X0,X1))))))). tff(u3584,axiom, ((~(![X9, X11, X13, X15, X1, X3, X5, X7, X8, X10, X12, X14, X0, X2, X4, X6] : (~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13)),X14)),X15)))))) | (![X9, X11, X13, X15, X1, X3, X5, X7, X8, X10, X12, X14, X0, X2, X4, X6] : (~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13)),X14)),X15))))))). tff(u3583,axiom, ((~(![X16, X9, X11, X13, X15, X1, X3, X5, X7, X8, X10, X12, X14, X0, X2, X4, X6] : ((~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X0,i(n(X1),X2))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13)),X14)),X15)),X16))) | ~t(i(X0,X1)))))) | (![X16, X9, X11, X13, X15, X1, X3, X5, X7, X8, X10, X12, X14, X0, X2, X4, X6] : ((~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X0,i(n(X1),X2))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13)),X14)),X15)),X16))) | ~t(i(X0,X1))))))). tff(u3582,axiom, ((~(![X16, X9, X11, X13, X15, X1, X3, X5, X7, X8, X10, X12, X14, X0, X2, X4, X6] : (~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13)),X14)),X15)),X16)))))) | (![X16, X9, X11, X13, X15, X1, X3, X5, X7, X8, X10, X12, X14, X0, X2, X4, X6] : (~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13)),X14)),X15)),X16))))))). tff(u3581,axiom, ((~(![X16, X9, X11, X13, X15, X1, X3, X5, X7, X17, X8, X10, X12, X14, X0, X2, X4, X6] : ((~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X0,i(n(X1),X2))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13)),X14)),X15)),X16)),X17))) | ~t(i(X0,X1)))))) | (![X16, X9, X11, X13, X15, X1, X3, X5, X7, X17, X8, X10, X12, X14, X0, X2, X4, X6] : ((~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X0,i(n(X1),X2))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13)),X14)),X15)),X16)),X17))) | ~t(i(X0,X1))))))). tff(u3580,axiom, ((~(![X16, X9, X11, X13, X15, X1, X3, X5, X7, X17, X8, X10, X12, X14, X0, X2, X4, X6] : (~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13)),X14)),X15)),X16)),X17)))))) | (![X16, X9, X11, X13, X15, X1, X3, X5, X7, X17, X8, X10, X12, X14, X0, X2, X4, X6] : (~t(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13)),X14)),X15)),X16)),X17))))))). tff(u3579,axiom, ((~(![X1, X0, X2] : ((~t(n(i(X0,i(n(X1),X2)))) | ~t(i(X0,X1)))))) | (![X1, X0, X2] : ((~t(n(i(X0,i(n(X1),X2)))) | ~t(i(X0,X1))))))). tff(u3578,axiom, ((~(![X1, X0, X2] : (~t(n(i(i(X0,X1),i(X0,i(n(X1),X2)))))))) | (![X1, X0, X2] : (~t(n(i(i(X0,X1),i(X0,i(n(X1),X2))))))))). tff(u3577,axiom, (![X1, X3, X0, X2] : (t(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3))))). tff(u3576,axiom, (![X9, X7, X8, X6] : ((t(i(n(i(X6,i(n(X7),X8))),X9)) | ~t(i(X6,X7)))))). tff(u3575,axiom, (![X1, X3, X0, X2, X4] : (t(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4))))). tff(u3574,axiom, (![X9, X11, X7, X8, X10] : ((t(i(n(i(n(i(X7,i(n(X8),X9))),X10)),X11)) | ~t(i(X7,X8)))))). tff(u3573,axiom, (![X1, X3, X5, X0, X2, X4] : (t(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5))))). tff(u3572,axiom, (![X9, X11, X13, X8, X10, X12] : ((t(i(n(i(n(i(n(i(X8,i(n(X9),X10))),X11)),X12)),X13)) | ~t(i(X8,X9)))))). tff(u3571,axiom, (![X1, X3, X5, X0, X2, X4, X6] : (t(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6))))). tff(u3570,axiom, (![X49, X44, X46, X48, X50, X45, X47] : ((t(i(n(i(n(i(n(i(n(i(X44,i(n(X45),X46))),X47)),X48)),X49)),X50)) | ~t(i(X44,X45)))))). tff(u3569,axiom, (![X1, X3, X5, X7, X0, X2, X4, X6] : (t(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7))))). tff(u3568,axiom, (![X73, X75, X77, X71, X72, X74, X76, X78] : ((t(i(n(i(n(i(n(i(n(i(n(i(X71,i(n(X72),X73))),X74)),X75)),X76)),X77)),X78)) | ~t(i(X71,X72)))))). tff(u3567,axiom, (![X1, X3, X5, X7, X8, X0, X2, X4, X6] : (t(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8))))). tff(u3566,axiom, (![X104, X106, X108, X110, X112, X105, X107, X109, X111] : ((t(i(n(i(n(i(n(i(n(i(n(i(n(i(X104,i(n(X105),X106))),X107)),X108)),X109)),X110)),X111)),X112)) | ~t(i(X104,X105)))))). tff(u3565,axiom, (![X9, X1, X3, X5, X7, X8, X0, X2, X4, X6] : (t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9))))). tff(u3564,axiom, (![X148, X150, X143, X145, X147, X149, X151, X152, X144, X146] : ((t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X143,i(n(X144),X145))),X146)),X147)),X148)),X149)),X150)),X151)),X152)) | ~t(i(X143,X144)))))). tff(u3563,axiom, (![X9, X1, X3, X5, X7, X8, X10, X0, X2, X4, X6] : (t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10))))). tff(u3562,axiom, (![X193, X195, X197, X188, X190, X192, X194, X196, X198, X189, X191] : ((t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X188,i(n(X189),X190))),X191)),X192)),X193)),X194)),X195)),X196)),X197)),X198)) | ~t(i(X188,X189)))))). tff(u3561,axiom, (![X9, X11, X1, X3, X5, X7, X8, X10, X0, X2, X4, X6] : (t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11))))). tff(u3560,axiom, (![X245, X247, X248, X250, X240, X242, X244, X246, X239, X249, X241, X243] : ((t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X239,i(n(X240),X241))),X242)),X243)),X244)),X245)),X246)),X247)),X248)),X249)),X250)) | ~t(i(X239,X240)))))). tff(u3559,axiom, (![X9, X11, X1, X3, X5, X7, X8, X10, X12, X0, X2, X4, X6] : (t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12))))). tff(u3558,axiom, (![X307, X305, X299, X297, X303, X301, X306, X304, X308, X298, X296, X302, X300] : ((t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X296,i(n(X297),X298))),X299)),X300)),X301)),X302)),X303)),X304)),X305)),X306)),X307)),X308)) | ~t(i(X296,X297)))))). tff(u3557,axiom, (![X9, X11, X13, X1, X3, X5, X7, X8, X10, X12, X0, X2, X4, X6] : (t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13))))). tff(u3556,axiom, (![X371, X369, X363, X361, X367, X365, X359, X370, X368, X372, X362, X360, X366, X364] : ((t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X359,i(n(X360),X361))),X362)),X363)),X364)),X365)),X366)),X367)),X368)),X369)),X370)),X371)),X372)) | ~t(i(X359,X360)))))). tff(u3555,axiom, (![X9, X11, X13, X1, X3, X5, X7, X8, X10, X12, X14, X0, X2, X4, X6] : (t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13)),X14))))). tff(u3554,axiom, (![X435, X433, X439, X437, X431, X429, X442, X440, X434, X432, X438, X436, X430, X428, X441] : ((t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X428,i(n(X429),X430))),X431)),X432)),X433)),X434)),X435)),X436)),X437)),X438)),X439)),X440)),X441)),X442)) | ~t(i(X428,X429)))))). tff(u3553,axiom, (![X9, X11, X13, X15, X1, X3, X5, X7, X8, X10, X12, X14, X0, X2, X4, X6] : (t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13)),X14)),X15))))). tff(u3552,axiom, (![X515, X513, X517, X506, X504, X510, X508, X514, X512, X518, X516, X507, X505, X511, X509, X503] : ((t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X503,i(n(X504),X505))),X506)),X507)),X508)),X509)),X510)),X511)),X512)),X513)),X514)),X515)),X516)),X517)),X518)) | ~t(i(X503,X504)))))). tff(u3551,axiom, (![X16, X9, X11, X13, X15, X1, X3, X5, X7, X8, X10, X12, X14, X0, X2, X4, X6] : (t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13)),X14)),X15)),X16))))). tff(u3550,axiom, (![X587, X585, X591, X589, X595, X593, X599, X597, X586, X584, X590, X588, X594, X592, X598, X596, X600] : ((t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X584,i(n(X585),X586))),X587)),X588)),X589)),X590)),X591)),X592)),X593)),X594)),X595)),X596)),X597)),X598)),X599)),X600)) | ~t(i(X584,X585)))))). tff(u3549,axiom, (![X16, X9, X11, X13, X15, X1, X3, X5, X7, X17, X8, X10, X12, X14, X0, X2, X4, X6] : (t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13)),X14)),X15)),X16)),X17))))). tff(u3548,axiom, (![X674, X672, X678, X676, X682, X680, X686, X684, X688, X671, X675, X673, X679, X677, X683, X681, X687, X685] : ((t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X671,i(n(X672),X673))),X674)),X675)),X676)),X677)),X678)),X679)),X680)),X681)),X682)),X683)),X684)),X685)),X686)),X687)),X688)) | ~t(i(X671,X672)))))). tff(u3547,axiom, (![X16, X18, X9, X11, X13, X15, X1, X3, X5, X7, X17, X8, X10, X12, X14, X0, X2, X4, X6] : (t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13)),X14)),X15)),X16)),X17)),X18))))). tff(u3546,axiom, (![X772, X774, X768, X770, X780, X782, X776, X778, X766, X764, X773, X775, X769, X771, X781, X777, X779, X767, X765] : ((t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X764,i(n(X765),X766))),X767)),X768)),X769)),X770)),X771)),X772)),X773)),X774)),X775)),X776)),X777)),X778)),X779)),X780)),X781)),X782)) | ~t(i(X764,X765)))))). tff(u3545,axiom, (![X16, X18, X9, X11, X13, X15, X1, X3, X5, X7, X17, X19, X8, X10, X12, X14, X0, X2, X4, X6] : (t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13)),X14)),X15)),X16)),X17)),X18)),X19))))). tff(u3544,axiom, (![X869, X871, X865, X867, X877, X879, X873, X875, X880, X882, X863, X868, X870, X864, X866, X876, X878, X872, X874, X881] : ((t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X863,i(n(X864),X865))),X866)),X867)),X868)),X869)),X870)),X871)),X872)),X873)),X874)),X875)),X876)),X877)),X878)),X879)),X880)),X881)),X882)) | ~t(i(X863,X864)))))). tff(u3543,axiom, ((~(![X579, X577, X583, X581, X587, X585, X589, X570, X574, X572, X578, X576, X582, X580, X586, X584, X588, X571, X575, X573] : (t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(X570),X571)),X572)),X573)),X574)),X575)),X576)),X577)),X578)),X579)),X580)),X581)),X582)),X583)),X584)),X585)),X586)),X587)),X588)),X589))))) | (![X579, X577, X583, X581, X587, X585, X589, X570, X574, X572, X578, X576, X582, X580, X586, X584, X588, X571, X575, X573] : (t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(X570),X571)),X572)),X573)),X574)),X575)),X576)),X577)),X578)),X579)),X580)),X581)),X582)),X583)),X584)),X585)),X586)),X587)),X588)),X589)))))). tff(u3542,axiom, (![X16, X18, X20, X9, X11, X13, X15, X1, X3, X5, X7, X17, X19, X8, X10, X12, X14, X0, X2, X4, X6] : (t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13)),X14)),X15)),X16)),X17)),X18)),X19)),X20))))). tff(u3541,axiom, (![X986, X968, X972, X974, X970, X981, X983, X977, X979, X985, X987, X973, X975, X969, X971, X980, X982, X976, X978, X988, X984] : ((t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(X968,i(n(X969),X970))),X971)),X972)),X973)),X974)),X975)),X976)),X977)),X978)),X979)),X980)),X981)),X982)),X983)),X984)),X985)),X986)),X987)),X988)) | ~t(i(X968,X969)))))). tff(u3540,axiom, (![X16, X18, X20, X9, X11, X13, X15, X1, X3, X5, X7, X17, X19, X21, X8, X10, X12, X14, X0, X2, X4, X6] : (t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13)),X14)),X15)),X16)),X17)),X18)),X19)),X20)),X21))))). tff(u3539,axiom, (![X16, X18, X20, X22, X9, X11, X13, X15, X1, X3, X5, X7, X17, X19, X21, X8, X10, X12, X14, X0, X2, X4, X6] : (t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13)),X14)),X15)),X16)),X17)),X18)),X19)),X20)),X21)),X22))))). tff(u3538,axiom, (![X16, X18, X20, X22, X9, X11, X13, X15, X1, X3, X5, X7, X8, X17, X19, X21, X23, X10, X12, X14, X0, X2, X4, X6] : (t(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(n(i(i(X0,X1),i(X0,i(n(X1),X2)))),X3)),X4)),X5)),X6)),X7)),X8)),X9)),X10)),X11)),X12)),X13)),X14)),X15)),X16)),X17)),X18)),X19)),X20)),X21)),X22)),X23))))). tff(u3537,axiom, (![X1, X3, X0, X2, X4] : (t(i(i(i(X0,X1),i(i(X2,n(X0)),i(X3,n(X3)))),i(i(X4,X3),i(X4,X0))))))). tff(u3536,axiom, (![X1, X0, X2] : (t(i(i(X0,X1),i(X0,i(n(X1),X2))))))). tff(u3535,axiom, (![X1, X0, X2] : ((t(i(X0,i(n(X1),X2))) | ~t(i(X0,X1)))))). % # SZS output end Saturation. % ------------------------------ % Version: Vampire 4.5.1 (commit 57a6f78c on 2020-07-15 11:59:04 +0200) % Termination reason: Satisfiable % Memory used [KB]: 11257 % Time elapsed: 0.093 s % ------------------------------ % ------------------------------ % Success in time 934.829 s