% 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 CC01CC1CC23C1OC4C02 % 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]: 8571 % Time elapsed: 0.807 s % ------------------------------ % ------------------------------ % fmb+10_1_av=off:bce=on:nm=6_1461 on CC01CC1CC23C1OC4C02 TRYING [6] % 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]: 85840 % 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 CC01CC1CC23C1OC4C02 % 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]: 2694327 % Time elapsed: 25.800 s % ------------------------------ % ------------------------------ % dis+1_3_av=off:cond=on:nm=64:newcnf=on:nwc=1_87 on CC01CC1CC23C1OC4C02 % 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]: 223876 % Time elapsed: 11.500 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 CC01CC1CC23C1OC4C02 % SZS status CounterSatisfiable for CC01CC1CC23C1OC4C02 % # SZS output start Saturation. tff(u1864,axiom, (![X1, X0] : ((~t(i(X0,X1)) | ~t(X0) | t(X1))))). tff(u1863,axiom, (![X1, X3, X0, X2] : ((~t(i(X0,X1)) | ~t(i(X1,i(i(X2,X3),i(X1,o)))) | ~t(X0) | t(X2))))). tff(u1862,axiom, (![X22, X25, X21, X23, X24, X26] : ((~t(i(X21,X25)) | ~t(i(X25,i(i(X22,X26),i(X25,o)))) | ~t(i(X22,i(i(X23,X24),i(X22,o)))) | t(X23) | ~t(X21))))). tff(u1861,negated_conjecture, ((~(![X5, X7, X4, X6] : ((~t(i(X4,i(i(X5,X6),i(X4,o)))) | ~t(i(X7,X4)))))) | (![X5, X7, X4, X6] : ((~t(i(X4,i(i(X5,X6),i(X4,o)))) | ~t(i(X7,X4))))))). tff(u1860,axiom, (![X32, X25, X27, X29, X31, X26, X28, X30] : ((~t(i(X25,X31)) | ~t(i(X31,i(i(X26,X32),i(X31,o)))) | ~t(i(X27,i(i(X29,X30),i(X27,o)))) | ~t(i(X26,i(i(X27,X28),i(X26,o)))) | ~t(X25) | t(X29))))). tff(u1859,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X5, X6] : ((~t(i(X5,i(i(i(sK2,sK0),X6),i(X5,o)))) | ~t(i(i(sK4,sK0),X5))))))). tff(u1858,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X9, X8] : ((~t(i(X8,i(i(i(i(sK4,sK0),i(sK2,sK0)),X9),i(X8,o)))) | ~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),X8))))))). tff(u1857,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X5, X7, X4, X6] : ((~t(i(X5,i(i(i(i(i(sK2,sK0),X6),i(X4,o)),X7),i(X5,o)))) | ~t(i(X4,X5)) | ~t(i(i(sK4,sK0),X4))))))). tff(u1856,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X9, X7, X8, X6] : ((~t(i(X7,i(i(i(i(i(i(sK4,sK0),i(sK2,sK0)),X8),i(X6,o)),X9),i(X7,o)))) | ~t(i(X6,X7)) | ~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),X6))))))). tff(u1855,axiom, (![X16, X18, X20, X22, X15, X17, X19, X21] : ((~t(i(X18,X19)) | ~t(i(X19,i(i(X15,X20),i(X19,o)))) | ~t(i(X21,i(i(i(i(X16,X17),i(X15,o)),X22),i(X21,o)))) | ~t(X18) | ~t(i(X15,X21)) | t(X16))))). tff(u1854,axiom, (![X16, X18, X20, X22, X15, X17, X19, X21] : ((~t(i(X18,X15)) | ~t(i(X16,i(i(X19,X20),i(X16,o)))) | ~t(i(X21,i(i(i(i(X16,X17),i(X15,o)),X22),i(X21,o)))) | ~t(X18) | ~t(i(X15,X21)) | t(X19))))). tff(u1853,axiom, (![X16, X11, X13, X15, X12, X14] : ((~t(i(X14,X11)) | ~t(i(X15,i(i(i(i(X12,X13),i(X11,o)),X16),i(X15,o)))) | t(X12) | ~t(i(X11,X15)) | ~t(X14))))). tff(u1852,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X1, X3, X5, X0, X2, X4, X6] : ((~t(i(X0,X3)) | ~t(i(X3,i(i(X1,X4),i(X3,o)))) | ~t(i(X5,i(i(i(i(o,X2),i(i(X0,X1),o)),X6),i(X5,o)))) | ~t(i(i(X0,X1),X5))))))). tff(u1851,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X9, X5, X7, X8, X6] : ((~t(i(X7,i(i(i(i(X6,i(X5,o)),i(i(o,X8),i(i(X6,i(X5,o)),o))),X9),i(X7,o)))) | ~t(i(i(sK4,sK0),X7)) | ~t(i(X5,i(X6,i(X5,o))))))))). tff(u1850,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X9, X11, X13, X7, X8, X10, X12] : ((~t(i(X7,X10)) | ~t(i(X10,i(i(X8,X11),i(X10,o)))) | ~t(i(X12,i(i(i(i(X7,X8),i(i(o,X9),i(i(X7,X8),o))),X13),i(X12,o)))) | ~t(i(i(sK4,sK0),X12))))))). tff(u1849,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X9, X11, X13, X10, X12, X14] : ((~t(i(X11,i(i(i(i(i(i(i(sK2,sK0),X12),i(X9,o)),X13),i(X10,o)),X14),i(X11,o)))) | ~t(i(i(sK4,sK0),X9)) | ~t(i(X10,X11)) | ~t(i(X9,X10))))))). tff(u1848,axiom, (![X20, X22, X25, X19, X21, X23, X24, X26] : ((~t(i(X19,X25)) | ~t(i(X25,i(i(X20,X26),i(X25,o)))) | ~t(i(X21,i(i(i(i(X22,X23),i(i(X19,X20),o)),X24),i(X21,o)))) | ~t(i(i(X19,X20),X21)) | t(X22))))). tff(u1847,axiom, (![X16, X18, X20, X22, X15, X17, X19, X21] : ((~t(i(X20,X18)) | ~t(i(X21,i(i(i(i(i(i(X16,X17),i(X18,o)),X19),i(X15,o)),X22),i(X21,o)))) | ~t(i(X18,X15)) | ~t(X20) | ~t(i(X15,X21)) | t(X16))))). tff(u1846,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X16, X11, X13, X15, X10, X12, X14] : ((~t(i(X14,i(i(i(i(i(X10,o),X15),i(i(X12,i(X11,X13)),o)),X16),i(X14,o)))) | ~t(i(X11,i(sK2,sK0))) | ~t(i(i(X12,i(X11,X13)),X14)) | ~t(i(i(sK4,sK0),X10))))))). tff(u1845,axiom, (![X16, X9, X11, X13, X15, X17, X10, X12, X14] : ((~t(i(X13,X9)) | ~t(i(X9,i(i(X10,X11),i(X9,o)))) | ~t(i(X14,i(i(i(i(X15,X16),i(i(X12,i(X13,X10)),o)),X17),i(X14,o)))) | ~t(i(i(X12,i(X13,X10)),X14)) | t(X15))))). tff(u1844,axiom, (![X1, X3, X5, X7, X8, X0, X2, X4, X6] : ((~t(i(X5,i(i(i(i(X6,X7),i(i(i(X1,i(i(X2,X3),i(X1,o))),i(X4,i(X0,X2))),o)),X8),i(X5,o)))) | t(X6) | ~t(i(i(i(X1,i(i(X2,X3),i(X1,o))),i(X4,i(X0,X2))),X5)) | ~t(i(X0,X1)))))). tff(u1843,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X1, X3, X0, X2] : ((~t(i(X3,i(i(X0,i(X1,o)),i(i(o,X2),i(i(X0,i(X1,o)),o))))) | ~t(i(i(sK4,sK0),X3)) | ~t(i(X1,i(X0,i(X1,o))))))))). tff(u1842,axiom, ((~(![X1, X0, X4] : ((~t(i(i(X0,i(i(o,X1),i(X0,o))),X0)) | ~t(i(X4,i(X0,i(i(o,X1),i(X0,o))))) | ~t(X4))))) | (![X1, X3, X0, X2] : ((~t(i(X3,i(i(X0,i(X1,o)),i(i(o,X2),i(i(X0,i(X1,o)),o))))) | ~t(X3) | ~t(i(X1,i(X0,i(X1,o))))))))). tff(u1841,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X9, X5, X7, X8, X4, X6] : ((~t(i(X4,X8)) | ~t(i(X8,i(i(X5,X9),i(X8,o)))) | ~t(i(X7,i(i(X4,X5),i(i(o,X6),i(i(X4,X5),o))))) | ~t(i(i(sK4,sK0),X7))))))). tff(u1840,axiom, ((~(![X1, X0, X4] : ((~t(i(i(X0,i(i(o,X1),i(X0,o))),X0)) | ~t(i(X4,i(X0,i(i(o,X1),i(X0,o))))) | ~t(X4))))) | (![X9, X5, X7, X8, X4, X6] : ((~t(i(X4,X8)) | ~t(i(X8,i(i(X5,X9),i(X8,o)))) | ~t(i(X7,i(i(X4,X5),i(i(o,X6),i(i(X4,X5),o))))) | ~t(X7)))))). tff(u1839,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X1, X3, X0, X2, X4] : ((~t(i(X0,i(X1,i(X0,o)))) | ~t(i(X2,i(i(i(i(o,X3),i(i(X1,i(X0,o)),o)),X4),i(X2,o)))) | ~t(i(i(X1,i(X0,o)),X2))))))). tff(u1838,negated_conjecture, ((~(![X1, X2] : (~t(i(X1,i(X2,i(X1,o))))))) | (![X1, X2] : (~t(i(X1,i(X2,i(X1,o)))))))). tff(u1837,axiom, (![X9, X11, X7, X8, X10] : ((~t(i(X7,i(X7,X8))) | ~t(i(X9,i(i(i(i(X8,X10),i(i(X7,X8),o)),X11),i(X9,o)))) | ~t(i(i(X7,X8),X9)) | t(X8))))). tff(u1836,axiom, ((~(![X1, X0, X4] : ((~t(i(i(X0,i(i(o,X1),i(X0,o))),X0)) | ~t(i(X4,i(X0,i(i(o,X1),i(X0,o))))) | ~t(X4))))) | (![X1, X0, X4] : ((~t(i(i(X0,i(i(o,X1),i(X0,o))),X0)) | ~t(i(X4,i(X0,i(i(o,X1),i(X0,o))))) | ~t(X4)))))). tff(u1835,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X1, X3, X0, X2] : ((~t(i(i(X0,i(i(o,X1),i(X0,o))),X0)) | ~t(i(X2,i(i(i(i(o,X1),i(X0,o)),X3),i(X2,o)))) | ~t(i(X0,X2))))))). tff(u1834,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X5, X7, X4, X6] : ((~t(i(i(X4,i(i(o,X5),i(X4,o))),X4)) | ~t(i(X6,i(i(i(X4,i(i(o,X5),i(X4,o))),X7),i(X6,o)))) | ~t(i(i(sK4,sK0),X6))))))). tff(u1833,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X1, X0, X2] : ((~t(i(i(X1,i(i(o,X2),i(X1,o))),X1)) | ~t(i(X0,i(X1,i(i(o,X2),i(X1,o))))) | ~t(i(i(sK4,sK0),X0))))))). tff(u1832,negated_conjecture, ((~(![X1, X0, X4] : ((~t(i(i(i(sK2,sK0),X4),i(X0,i(i(o,X1),i(X0,o))))) | ~t(i(i(X0,i(i(o,X1),i(X0,o))),X0)))))) | (![X0, X2] : ((~t(i(i(X0,i(i(o,X2),i(X0,o))),X0)) | ~t(i(i(o,X2),i(sK2,sK0)))))))). tff(u1831,axiom, ((~(![X1, X0, X4] : ((~t(i(i(X0,i(i(o,X1),i(X0,o))),X0)) | ~t(i(X4,i(X0,i(i(o,X1),i(X0,o))))) | ~t(X4))))) | (![X16, X13, X15, X12, X14] : ((~t(i(i(X13,i(i(o,X14),i(X13,o))),X13)) | ~t(i(X12,X15)) | ~t(i(X15,i(i(i(X13,i(i(o,X14),i(X13,o))),X16),i(X15,o)))) | ~t(X12)))))). tff(u1830,negated_conjecture, ((~(![X1, X0, X4] : ((~t(i(i(sK0,X4),i(X0,i(i(o,X1),i(X0,o))))) | ~t(i(i(X0,i(i(o,X1),i(X0,o))),X0)))))) | (![X0, X2] : ((~t(i(i(X0,i(i(o,X2),i(X0,o))),X0)) | ~t(i(i(o,X2),sK0))))))). tff(u1829,axiom, ((~(![X1, X0, X4, X6] : ((~t(i(i(X0,i(i(o,X1),i(X0,o))),X0)) | ~t(i(X6,X4)) | ~t(i(X4,i(X0,i(i(o,X1),i(X0,o))))) | ~t(X6))))) | (![X1, X0, X4, X6] : ((~t(i(i(X0,i(i(o,X1),i(X0,o))),X0)) | ~t(i(X6,X4)) | ~t(i(X4,i(X0,i(i(o,X1),i(X0,o))))) | ~t(X6)))))). tff(u1828,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X1, X3, X0, X2] : ((~t(i(i(X3,i(i(o,X2),i(X3,o))),X3)) | ~t(i(X3,i(X0,i(i(o,X1),i(X0,o))))) | ~t(i(i(X0,i(i(o,X1),i(X0,o))),X0))))))). tff(u1827,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X16, X11, X13, X15, X12, X14] : ((~t(i(i(X13,i(i(o,X12),i(X13,o))),X13)) | ~t(i(X15,i(i(i(i(i(i(o,X12),i(X13,o)),X14),i(X11,o)),X16),i(X15,o)))) | ~t(i(X11,X15)) | ~t(i(X13,X11))))))). tff(u1826,negated_conjecture, ((~(![X1, X2] : (~t(i(X1,i(X2,i(X1,o))))))) | (![X1, X0] : (~t(i(i(X0,i(i(o,X1),i(X0,o))),X0)))))). tff(u1825,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X16, X13, X15, X12, X14] : ((~t(i(i(X13,i(i(o,X14),i(X13,o))),X13)) | ~t(i(i(sK4,sK0),X12)) | ~t(i(X12,X15)) | ~t(i(X15,i(i(i(X13,i(i(o,X14),i(X13,o))),X16),i(X15,o))))))))). tff(u1824,negated_conjecture, ((~(![X1, X0, X4] : ((~t(i(i(i(sK2,sK0),X4),i(X0,i(i(o,X1),i(X0,o))))) | ~t(i(i(X0,i(i(o,X1),i(X0,o))),X0)))))) | (![X9, X11, X8, X10, X12] : ((~t(i(i(X9,i(i(o,X10),i(X9,o))),X9)) | ~t(i(i(i(sK2,sK0),X8),X11)) | ~t(i(X11,i(i(i(X9,i(i(o,X10),i(X9,o))),X12),i(X11,o))))))))). tff(u1823,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X16, X11, X13, X15, X12, X14] : ((~t(i(i(i(sK2,sK0),X14),X11)) | ~t(i(X15,i(i(i(i(i(X12,o),X13),i(X11,o)),X16),i(X15,o)))) | ~t(i(X11,X15)) | ~t(i(i(sK4,sK0),X12))))))). tff(u1822,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X20, X22, X19, X21, X23, X24] : ((~t(i(i(i(sK2,sK0),X19),X23)) | ~t(i(X23,i(i(X20,X24),i(X23,o)))) | ~t(i(X20,i(i(i(X21,o),X22),i(X20,o)))) | ~t(i(i(sK4,sK0),X21))))))). tff(u1821,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X3, X5, X2, X4] : ((~t(i(i(i(sK2,sK0),X5),X3)) | ~t(i(X3,i(i(i(X2,o),X4),i(X3,o)))) | ~t(i(i(sK4,sK0),X2))))))). tff(u1820,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X3, X5, X2, X4] : ((~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),X2)) | ~t(i(X3,i(i(i(X2,o),X4),i(X3,o)))) | ~t(i(i(i(i(sK4,sK0),i(sK2,sK0)),X5),X3))))))). tff(u1819,axiom, ((~(![X1, X0, X4] : ((~t(i(i(X0,i(i(o,X1),i(X0,o))),X0)) | ~t(i(X4,i(X0,i(i(o,X1),i(X0,o))))) | ~t(X4))))) | (![X3, X5, X4, X6] : ((~t(i(i(X4,i(i(o,X6),i(X4,o))),X4)) | ~t(i(X3,i(i(i(X4,o),X5),i(X3,o)))) | ~t(i(i(o,X6),X3))))))). tff(u1818,negated_conjecture, ((~(![X1, X0, X4] : ((~t(i(i(sK0,X4),i(X0,i(i(o,X1),i(X0,o))))) | ~t(i(i(X0,i(i(o,X1),i(X0,o))),X0)))))) | (![X9, X11, X8, X10, X12] : ((~t(i(i(X9,i(i(o,X10),i(X9,o))),X9)) | ~t(i(i(sK0,X8),X11)) | ~t(i(X11,i(i(i(X9,i(i(o,X10),i(X9,o))),X12),i(X11,o))))))))). tff(u1817,axiom, (![X9, X5, X7, X8, X10, X6] : ((~t(i(X8,X5)) | ~t(i(i(X6,X7),X9)) | ~t(i(X9,i(i(i(X5,o),X10),i(X9,o)))) | t(X6) | ~t(X8))))). tff(u1816,axiom, (![X1, X3, X5, X7, X8, X0, X2, X4, X6] : ((~t(i(i(X5,X6),X7)) | ~t(i(X7,i(i(i(i(i(X1,i(i(X2,X3),i(X1,o))),i(X4,i(X0,X2))),o),X8),i(X7,o)))) | t(X5) | ~t(i(X0,X1)))))). tff(u1815,axiom, (![X16, X9, X11, X13, X15, X17, X10, X12, X14] : ((~t(i(X13,X9)) | ~t(i(i(X14,X15),X16)) | ~t(i(X9,i(i(X10,X11),i(X9,o)))) | ~t(i(X16,i(i(i(i(X12,i(X13,X10)),o),X17),i(X16,o)))) | t(X14))))). tff(u1814,axiom, (![X32, X34, X27, X29, X31, X33, X28, X30] : ((~t(i(X27,X33)) | ~t(i(i(X29,X30),X31)) | ~t(i(X33,i(i(X28,X34),i(X33,o)))) | ~t(i(X31,i(i(i(X28,o),X32),i(X31,o)))) | ~t(X27) | t(X29))))). tff(u1813,axiom, (![X32, X25, X27, X29, X31, X26, X28, X30] : ((~t(i(X28,X29)) | ~t(i(i(X25,X26),X31)) | ~t(i(X31,i(i(X27,X32),i(X31,o)))) | ~t(i(X27,i(i(i(X29,o),X30),i(X27,o)))) | ~t(X28) | t(X25))))). tff(u1812,axiom, (![X16, X18, X20, X22, X15, X17, X19, X21] : ((~t(i(X18,X16)) | ~t(i(i(X19,X20),X15)) | ~t(i(X21,i(i(i(i(i(X16,o),X17),i(X15,o)),X22),i(X21,o)))) | ~t(X18) | ~t(i(X15,X21)) | t(X19))))). tff(u1811,axiom, (![X1, X3, X0, X2] : ((~t(i(X2,i(i(i(X2,o),X3),i(X2,o)))) | ~t(i(i(X0,X1),X2)) | t(X0) | ~t(i(X0,X1)))))). tff(u1810,axiom, (![X20, X22, X25, X19, X21, X23, X24, X26] : ((~t(i(X19,X25)) | ~t(i(i(X21,X22),X23)) | ~t(i(X25,i(i(X20,X26),i(X25,o)))) | ~t(i(X23,i(i(i(i(X19,X20),o),X24),i(X23,o)))) | t(X21))))). tff(u1809,axiom, (![X9, X11, X13, X7, X8, X10, X12, X14] : ((~t(i(X10,X7)) | ~t(i(i(X8,X9),X13)) | ~t(i(X13,i(i(i(X7,o),X14),i(X13,o)))) | ~t(i(X8,i(i(X11,X12),i(X8,o)))) | ~t(X10) | t(X11))))). tff(u1808,axiom, (![X16, X11, X13, X15, X12, X14] : ((~t(i(i(X13,X14),X11)) | ~t(i(X15,i(i(i(i(i(X11,o),X12),i(X11,o)),X16),i(X15,o)))) | ~t(i(X13,X14)) | ~t(i(X11,X15)) | t(X13))))). tff(u1807,axiom, (![X20, X22, X19, X21, X23, X24] : ((~t(i(X21,i(i(i(X21,o),X22),i(X21,o)))) | ~t(i(i(X19,X20),X23)) | ~t(i(X23,i(i(X21,X24),i(X23,o)))) | ~t(i(X19,X20)) | t(X19))))). tff(u1806,axiom, (![X3, X5, X2, X4, X6] : ((~t(i(X2,i(X2,X3))) | ~t(i(i(X3,X6),X4)) | ~t(i(X4,i(i(i(i(X2,X3),o),X5),i(X4,o)))) | t(X3))))). tff(u1805,axiom, (![X9, X11, X13, X7, X8, X10, X12, X14] : ((~t(i(X10,X8)) | ~t(i(i(i(X8,o),X9),X13)) | ~t(i(i(X11,X12),X7)) | ~t(i(X13,i(i(i(X7,o),X14),i(X13,o)))) | ~t(X10) | t(X11))))). tff(u1804,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X9, X3, X5, X7, X8, X4, X6] : ((~t(i(i(i(X3,o),X9),X5)) | ~t(i(X5,i(i(i(i(X6,i(X4,X7)),o),X8),i(X5,o)))) | ~t(i(X4,i(sK2,sK0))) | ~t(i(i(sK4,sK0),X3))))))). tff(u1803,axiom, (![X9, X5, X7, X8, X10, X6] : ((~t(i(i(i(X5,o),X6),X9)) | ~t(i(i(X7,X8),X5)) | ~t(i(X9,i(i(i(X5,o),X10),i(X9,o)))) | ~t(i(X7,X8)) | t(X7))))). tff(u1802,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X9, X5, X7, X8, X10, X6] : ((~t(i(i(i(sK2,sK0),X8),X5)) | ~t(i(i(i(X6,o),X7),X9)) | ~t(i(X9,i(i(i(X5,o),X10),i(X9,o)))) | ~t(i(i(sK4,sK0),X6))))))). tff(u1801,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X16, X13, X15, X17, X12, X14] : ((~t(i(i(X12,i(i(o,X13),i(X12,o))),X16)) | ~t(i(X16,i(i(X12,X17),i(X16,o)))) | ~t(i(X14,i(i(i(i(o,X13),i(X12,o)),X15),i(X14,o)))) | ~t(i(X12,X14))))))). tff(u1800,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X11, X13, X10, X12, X14] : ((~t(i(i(X10,i(i(o,X11),i(X10,o))),X13)) | ~t(i(X13,i(i(X10,X14),i(X13,o)))) | ~t(i(X12,i(X10,i(i(o,X11),i(X10,o))))) | ~t(i(i(sK4,sK0),X12))))))). tff(u1799,axiom, ((~(![X1, X0, X4] : ((~t(i(i(X0,i(i(o,X1),i(X0,o))),X0)) | ~t(i(X4,i(X0,i(i(o,X1),i(X0,o))))) | ~t(X4))))) | (![X11, X13, X10, X12, X14] : ((~t(i(i(X10,i(i(o,X11),i(X10,o))),X13)) | ~t(i(X13,i(i(X10,X14),i(X13,o)))) | ~t(i(X12,i(X10,i(i(o,X11),i(X10,o))))) | ~t(X12)))))). tff(u1798,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X3, X5, X7, X8, X4, X6] : ((~t(i(X3,X4)) | ~t(i(X5,i(i(i(X4,o),X6),i(X5,o)))) | ~t(i(i(i(i(i(sK2,sK0),X7),i(X3,o)),X8),X5)) | ~t(i(i(sK4,sK0),X3))))))). tff(u1797,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X9, X5, X7, X8, X10, X6] : ((~t(i(i(X7,i(i(o,X6),i(X7,o))),X7)) | ~t(i(X7,X5)) | ~t(i(X9,i(i(i(X5,o),X10),i(X9,o)))) | ~t(i(i(i(i(o,X6),i(X7,o)),X8),X9))))))). tff(u1796,axiom, (![X9, X11, X13, X7, X8, X10, X12, X14] : ((~t(i(X12,X10)) | ~t(i(X10,X7)) | ~t(i(X13,i(i(i(X7,o),X14),i(X13,o)))) | ~t(i(i(i(i(X8,X9),i(X10,o)),X11),X13)) | ~t(X12) | t(X8))))). tff(u1795,axiom, (![X1, X0, X2] : ((~t(i(i(X0,X1),i(i(X1,X2),i(i(X0,X1),o)))) | ~t(i(X0,i(X0,X1))) | t(X1))))). tff(u1794,axiom, (![X16, X18, X20, X15, X17, X19] : ((~t(i(X15,X19)) | ~t(i(X19,i(i(X16,X20),i(X19,o)))) | ~t(i(i(X15,X16),i(i(X17,X18),i(i(X15,X16),o)))) | t(X17))))). tff(u1793,axiom, (![X18, X20, X22, X17, X19, X21, X23, X24] : ((~t(i(X17,X23)) | ~t(i(X23,i(i(X18,X24),i(X23,o)))) | ~t(i(X19,i(i(X21,X22),i(X19,o)))) | ~t(i(i(X17,X18),i(i(X19,X20),i(i(X17,X18),o)))) | t(X21))))). tff(u1792,axiom, (![X16, X18, X20, X22, X17, X19, X21, X23, X24] : ((~t(i(X17,X23)) | ~t(i(X23,i(i(X18,X24),i(X23,o)))) | ~t(i(i(X17,X18),i(i(X19,X20),i(i(X17,X18),o)))) | ~t(i(i(X16,X19),i(i(X21,X22),i(i(X16,X19),o)))) | t(X21))))). tff(u1791,axiom, (![X32, X25, X27, X29, X31, X26, X28, X30] : ((~t(i(X25,X31)) | ~t(i(X31,i(i(X26,X32),i(X31,o)))) | ~t(i(X26,i(i(X27,X28),i(X26,o)))) | ~t(i(i(X25,X27),i(i(X29,X30),i(i(X25,X27),o)))) | t(X29))))). tff(u1790,axiom, (![X1, X5, X0, X2, X4, X6] : ((~t(i(i(X0,i(i(o,X1),i(X0,o))),X0)) | ~t(i(X4,i(X0,i(i(o,X1),i(X0,o))))) | ~t(i(i(X4,X2),i(i(X5,X6),i(i(X4,X2),o)))) | t(X5))))). tff(u1789,axiom, (![X9, X11, X13, X7, X8, X10, X12, X14] : ((~t(i(X10,X7)) | ~t(i(i(X8,X9),X13)) | ~t(i(X13,i(i(i(X7,o),X14),i(X13,o)))) | ~t(i(i(X10,X8),i(i(X11,X12),i(i(X10,X8),o)))) | t(X11))))). tff(u1788,axiom, (![X16, X18, X20, X22, X15, X17, X19, X21] : ((~t(i(X18,X15)) | ~t(i(i(X18,X16),i(i(X19,X20),i(i(X18,X16),o)))) | ~t(i(X21,i(i(i(i(X16,X17),i(X15,o)),X22),i(X21,o)))) | ~t(i(X15,X21)) | t(X19))))). tff(u1787,axiom, ((~(![X18, X20, X22, X19, X21, X23, X24] : ((~t(i(X20,X21)) | ~t(i(X18,X23)) | ~t(i(X23,i(i(X19,X24),i(X23,o)))) | ~t(i(i(X18,X19),i(i(i(X21,o),X22),i(i(X18,X19),o)))) | ~t(X20))))) | (![X18, X20, X22, X19, X21, X23, X24] : ((~t(i(X20,X21)) | ~t(i(X18,X23)) | ~t(i(X23,i(i(X19,X24),i(X23,o)))) | ~t(i(i(X18,X19),i(i(i(X21,o),X22),i(i(X18,X19),o)))) | ~t(X20)))))). tff(u1786,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X16, X18, X13, X15, X17, X14] : ((~t(i(X13,X17)) | ~t(i(X17,i(i(X14,X18),i(X17,o)))) | ~t(i(i(X13,X14),i(i(i(X15,o),X16),i(i(X13,X14),o)))) | ~t(i(i(sK4,sK0),X15))))))). tff(u1785,axiom, (![X9, X11, X13, X15, X8, X12, X14] : ((~t(i(X13,X14)) | ~t(i(X12,X8)) | ~t(i(i(X11,i(X12,X9)),i(i(i(X14,o),X15),i(i(X11,i(X12,X9)),o)))) | ~t(X13) | t(X8))))). tff(u1784,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X9, X11, X8, X10, X6] : ((~t(i(i(X8,i(X9,X6)),i(i(i(X10,o),X11),i(i(X8,i(X9,X6)),o)))) | ~t(i(i(sK4,sK0),X10)) | ~t(i(X9,i(sK2,sK0)))))))). tff(u1783,axiom, (![X9, X11, X13, X15, X7, X8, X10, X12, X14] : ((~t(i(X11,X7)) | ~t(i(X12,i(i(X14,X15),i(X12,o)))) | ~t(i(X7,i(i(X8,X9),i(X7,o)))) | ~t(i(i(X10,i(X11,X8)),i(i(X12,X13),i(i(X10,i(X11,X8)),o)))) | t(X14))))). tff(u1782,axiom, (![X9, X11, X13, X7, X8, X10, X12] : ((~t(i(X11,X7)) | ~t(i(X7,i(i(X8,X9),i(X7,o)))) | ~t(i(i(X10,i(X11,X8)),i(i(X12,X13),i(i(X10,i(X11,X8)),o)))) | t(X12))))). tff(u1781,axiom, (![X9, X11, X7, X8, X10, X6] : ((~t(i(X10,X6)) | ~t(i(X6,i(i(X7,X8),i(X6,o)))) | ~t(i(i(X9,i(X10,X7)),i(i(i(i(X9,i(X10,X7)),o),X11),i(i(X9,i(X10,X7)),o)))) | t(X6))))). tff(u1780,axiom, ((~(![X1, X5, X0, X6] : ((~t(i(i(X0,i(i(o,X1),i(X0,o))),X0)) | ~t(i(i(X5,X6),i(X0,i(i(o,X1),i(X0,o))))) | t(X5))))) | (![X1, X5, X0, X6] : ((~t(i(i(X0,i(i(o,X1),i(X0,o))),X0)) | ~t(i(i(X5,X6),i(X0,i(i(o,X1),i(X0,o))))) | t(X5)))))). tff(u1779,negated_conjecture, ((~(![X1, X0, X4] : ((~t(i(i(i(sK2,sK0),X4),i(X0,i(i(o,X1),i(X0,o))))) | ~t(i(i(X0,i(i(o,X1),i(X0,o))),X0)))))) | (![X11, X13, X10, X12, X14] : ((~t(i(i(i(sK2,sK0),X12),i(X10,i(i(o,X11),i(X10,o))))) | ~t(i(i(X10,i(i(o,X11),i(X10,o))),X13)) | ~t(i(X13,i(i(X10,X14),i(X13,o))))))))). tff(u1778,negated_conjecture, ((~(![X1, X0, X4] : ((~t(i(i(i(sK2,sK0),X4),i(X0,i(i(o,X1),i(X0,o))))) | ~t(i(i(X0,i(i(o,X1),i(X0,o))),X0)))))) | (![X1, X0, X4] : ((~t(i(i(i(sK2,sK0),X4),i(X0,i(i(o,X1),i(X0,o))))) | ~t(i(i(X0,i(i(o,X1),i(X0,o))),X0))))))). tff(u1777,negated_conjecture, ((~(![X1, X0, X4] : ((~t(i(i(i(sK2,sK0),X4),i(X0,i(i(o,X1),i(X0,o))))) | ~t(i(i(X0,i(i(o,X1),i(X0,o))),X0)))))) | (![X1, X3, X0, X2] : ((~t(i(i(i(sK2,sK0),X3),i(i(X0,i(X1,o)),i(i(o,X2),i(i(X0,i(X1,o)),o))))) | ~t(i(X1,i(X0,i(X1,o))))))))). tff(u1776,negated_conjecture, ((~(![X1, X0, X4] : ((~t(i(i(i(sK2,sK0),X4),i(X0,i(i(o,X1),i(X0,o))))) | ~t(i(i(X0,i(i(o,X1),i(X0,o))),X0)))))) | (![X9, X5, X7, X8, X4, X6] : ((~t(i(i(i(sK2,sK0),X7),i(i(X4,X5),i(i(o,X6),i(i(X4,X5),o))))) | ~t(i(X8,i(i(X5,X9),i(X8,o)))) | ~t(i(X4,X8))))))). tff(u1775,axiom, (![X9, X11, X13, X15, X7, X8, X10, X12, X14] : ((~t(i(X11,X7)) | ~t(i(i(X10,i(X11,X8)),i(i(X12,X13),i(i(X10,i(X11,X8)),o)))) | ~t(i(i(i(X7,i(i(X8,X9),i(X7,o))),X12),i(i(X14,X15),i(i(i(X7,i(i(X8,X9),i(X7,o))),X12),o)))) | t(X14))))). tff(u1774,axiom, ((~(![X1, X0, X4] : ((~t(i(i(X0,i(i(o,X1),i(X0,o))),X0)) | ~t(i(X4,i(X0,i(i(o,X1),i(X0,o))))) | ~t(X4))))) | (![X1, X0, X2] : ((~t(i(i(i(X0,i(i(o,X1),i(X0,o))),i(i(o,X2),i(i(X0,i(i(o,X1),i(X0,o))),o))),i(X0,i(i(o,X1),i(X0,o))))) | ~t(i(i(X0,i(i(o,X1),i(X0,o))),X0))))))). tff(u1773,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X1, X0, X2] : ((~t(i(i(i(X0,i(i(o,X1),i(X0,o))),i(i(o,X2),i(i(X0,i(i(o,X1),i(X0,o))),o))),i(X0,i(i(o,X1),i(X0,o))))) | ~t(i(i(sK4,sK0),i(i(X0,i(i(o,X1),i(X0,o))),X0)))))))). tff(u1772,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | ~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0)))))). tff(u1771,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X1, X0] : ((~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(X0,i(i(o,X1),i(X0,o))))) | ~t(i(i(X0,i(i(o,X1),i(X0,o))),X0))))))). tff(u1770,negated_conjecture, ((~(![X1, X0, X4] : ((~t(i(i(sK0,X4),i(X0,i(i(o,X1),i(X0,o))))) | ~t(i(i(X0,i(i(o,X1),i(X0,o))),X0)))))) | (![X11, X13, X10, X12, X14] : ((~t(i(i(sK0,X12),i(X10,i(i(o,X11),i(X10,o))))) | ~t(i(i(X10,i(i(o,X11),i(X10,o))),X13)) | ~t(i(X13,i(i(X10,X14),i(X13,o))))))))). tff(u1769,negated_conjecture, ((~(![X1, X0, X4] : ((~t(i(i(sK0,X4),i(X0,i(i(o,X1),i(X0,o))))) | ~t(i(i(X0,i(i(o,X1),i(X0,o))),X0)))))) | (![X1, X0, X4] : ((~t(i(i(sK0,X4),i(X0,i(i(o,X1),i(X0,o))))) | ~t(i(i(X0,i(i(o,X1),i(X0,o))),X0))))))). tff(u1768,negated_conjecture, ((~(![X1, X0, X4] : ((~t(i(i(sK0,X4),i(X0,i(i(o,X1),i(X0,o))))) | ~t(i(i(X0,i(i(o,X1),i(X0,o))),X0)))))) | (![X1, X3, X0, X2] : ((~t(i(i(sK0,X3),i(i(X0,i(X1,o)),i(i(o,X2),i(i(X0,i(X1,o)),o))))) | ~t(i(X1,i(X0,i(X1,o))))))))). tff(u1767,negated_conjecture, ((~(![X1, X0, X4] : ((~t(i(i(sK0,X4),i(X0,i(i(o,X1),i(X0,o))))) | ~t(i(i(X0,i(i(o,X1),i(X0,o))),X0)))))) | (![X9, X5, X7, X8, X4, X6] : ((~t(i(i(sK0,X7),i(i(X4,X5),i(i(o,X6),i(i(X4,X5),o))))) | ~t(i(X8,i(i(X5,X9),i(X8,o)))) | ~t(i(X4,X8))))))). tff(u1766,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X9, X11, X8, X10] : ((~t(i(i(sK4,sK0),i(X8,i(i(o,X9),i(X8,o))))) | ~t(i(i(X8,i(i(o,X9),i(X8,o))),X10)) | ~t(i(X10,i(i(X8,X11),i(X10,o))))))))). tff(u1765,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X1, X0] : ((~t(i(i(sK4,sK0),i(X0,i(i(o,X1),i(X0,o))))) | ~t(i(i(X0,i(i(o,X1),i(X0,o))),X0))))))). tff(u1764,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X1, X0, X2] : ((~t(i(i(sK4,sK0),i(i(X0,i(X1,o)),i(i(o,X2),i(i(X0,i(X1,o)),o))))) | ~t(i(X1,i(X0,i(X1,o))))))))). tff(u1763,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X16, X18, X20, X22, X17, X19, X21, X23] : ((~t(i(i(sK4,sK0),i(i(X16,X19),i(i(o,X20),i(i(X16,X19),o))))) | ~t(i(i(X17,X18),i(i(X19,X21),i(i(X17,X18),o)))) | ~t(i(X22,i(i(X18,X23),i(X22,o)))) | ~t(i(X17,X22))))))). tff(u1762,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X25, X27, X29, X24, X26, X28, X30] : ((~t(i(i(sK4,sK0),i(i(X24,X26),i(i(o,X27),i(i(X24,X26),o))))) | ~t(i(X25,i(i(X26,X28),i(X25,o)))) | ~t(i(X24,X29)) | ~t(i(X29,i(i(X25,X30),i(X29,o))))))))). tff(u1761,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X16, X18, X13, X15, X17, X19, X14] : ((~t(i(X16,X13)) | ~t(i(i(sK4,sK0),i(i(X16,X14),i(i(o,X17),i(i(X16,X14),o))))) | ~t(i(X18,i(i(i(i(X14,X15),i(X13,o)),X19),i(X18,o)))) | ~t(i(X13,X18))))))). tff(u1760,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X1, X5, X0, X2, X4] : ((~t(i(i(sK4,sK0),i(i(X4,X2),i(i(o,X5),i(i(X4,X2),o))))) | ~t(i(X4,i(X0,i(i(o,X1),i(X0,o))))) | ~t(i(i(X0,i(i(o,X1),i(X0,o))),X0))))))). tff(u1759,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X9, X11, X7, X8, X10, X12, X6] : ((~t(i(i(sK4,sK0),i(i(X9,X7),i(i(o,X10),i(i(X9,X7),o))))) | ~t(i(X9,X6)) | ~t(i(X11,i(i(i(X6,o),X12),i(X11,o)))) | ~t(i(i(X7,X8),X11))))))). tff(u1758,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X3, X5, X7, X4, X6] : ((~t(i(i(sK4,sK0),i(i(X3,X4),i(i(o,X5),i(i(X3,X4),o))))) | ~t(i(X6,i(i(X4,X7),i(X6,o)))) | ~t(i(X3,X6))))))). tff(u1757,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X9, X11, X13, X15, X8, X10, X12, X14] : ((~t(i(i(sK4,sK0),i(i(i(X8,i(i(X9,X10),i(X8,o))),X13),i(i(o,X14),i(i(i(X8,i(i(X9,X10),i(X8,o))),X13),o))))) | ~t(i(i(X11,i(X12,X9)),i(i(X13,X15),i(i(X11,i(X12,X9)),o)))) | ~t(i(X12,X8))))))). tff(u1756,negated_conjecture, ((~~t(i(i(i(i(i(sK0,sK1),i(sK2,o)),sK3),sK4),i(i(sK4,sK0),i(sK2,sK0))))) | (![X3, X5, X4, X6] : ((~t(i(i(X4,i(i(o,X6),i(X4,o))),X4)) | ~t(i(i(sK4,sK0),i(X3,i(i(i(X4,o),X5),i(X3,o))))) | ~t(i(i(o,X6),X3))))))). tff(u1755,axiom, (![X1, X3, X0, X2, X4] : (t(i(i(X0,X1),i(i(X1,i(i(X2,X3),i(X1,o))),i(X4,i(X0,X2)))))))). tff(u1754,axiom, (![X1, X3, X0, X2, X4] : ((t(i(i(X1,i(i(X2,X3),i(X1,o))),i(X4,i(X0,X2)))) | ~t(i(X0,X1)))))). tff(u1753,axiom, (![X1, X0] : ((t(i(i(o,X1),i(X0,o))) | ~t(i(X0,i(X0,i(i(o,X1),i(X0,o))))) | ~t(i(i(X0,i(i(o,X1),i(X0,o))),X0)))))). tff(u1752,axiom, (![X1, X3, X0, X2, X4] : ((t(i(X4,i(X0,X2))) | ~t(i(X1,i(i(X2,X3),i(X1,o)))) | ~t(i(X0,X1)))))). tff(u1751,axiom, (![X1, X3, X0, X2] : ((t(i(X3,X1)) | ~t(i(X3,X0)) | ~t(i(X0,i(i(X1,X2),i(X0,o)))))))). % # 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]: 2302 % Time elapsed: 0.101 s % ------------------------------ % ------------------------------ % Success in time 330.773 s