% 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 CC01CC1COCC232C4C02 % 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]: 32750 % Time elapsed: 0.800 s % ------------------------------ % ------------------------------ % fmb+10_1_av=off:bce=on:nm=6_1461 on CC01CC1COCC232C4C02 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]: 66139 % 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 CC01CC1COCC232C4C02 % SZS status CounterSatisfiable for CC01CC1COCC232C4C02 % # SZS output start Saturation. tff(u1756,axiom, (![X1, X0] : ((~t(i(X0,X1)) | t(X1) | ~t(X0))))). tff(u1755,axiom, (![X1, X3, X0, X2, X4] : ((~t(i(X1,i(o,i(i(X3,X4),X3)))) | t(i(X2,i(X0,X3))) | ~t(i(X0,X1)))))). tff(u1754,axiom, (![X11, X13, X10, X12] : ((~t(i(X10,i(o,i(i(i(i(X11,X12),X11),X13),i(i(X11,X12),X11))))) | t(X11) | ~t(i(o,X10)))))). tff(u1753,axiom, (![X1, X3, X5, X0, X2, X4] : ((~t(i(X1,i(X3,i(o,i(i(X2,X4),X2))))) | t(i(X0,i(X1,X2))) | ~t(i(i(X2,X5),X3)))))). tff(u1752,axiom, (![X16, X18, X20, X15, X17, X19, X14] : ((~t(i(X16,i(X14,i(o,i(i(i(i(i(o,i(i(X17,X18),X17)),X19),i(o,i(i(X17,X18),X17))),X20),i(i(i(o,i(i(X17,X18),X17)),X19),i(o,i(i(X17,X18),X17)))))))) | t(i(X15,i(X16,X17))) | ~t(i(o,X14)))))). tff(u1751,axiom, (![X16, X18, X20, X22, X17, X19, X21, X23, X24] : ((~t(i(X18,i(i(i(o,i(i(X19,X20),X19)),X21),i(X16,i(o,i(i(i(i(i(o,i(i(i(o,i(i(X19,X20),X19)),X22),i(o,i(i(X19,X20),X19)))),X23),i(o,i(i(i(o,i(i(X19,X20),X19)),X22),i(o,i(i(X19,X20),X19))))),X24),i(i(i(o,i(i(i(o,i(i(X19,X20),X19)),X22),i(o,i(i(X19,X20),X19)))),X23),i(o,i(i(i(o,i(i(X19,X20),X19)),X22),i(o,i(i(X19,X20),X19))))))))))) | t(i(X17,i(X18,X19))) | ~t(i(o,X16)))))). tff(u1750,axiom, (![X51, X53, X55, X52, X54] : ((~t(i(i(X54,X55),X53)) | t(i(X51,i(X52,X53))) | ~t(i(o,X55)))))). tff(u1749,axiom, (![X22, X25, X27, X21, X23, X24, X26, X28] : ((~t(i(i(X24,X28),X23)) | t(i(X22,i(i(X21,i(o,i(i(i(i(i(X23,i(o,i(i(X24,X25),X24))),X26),i(X23,i(o,i(i(X24,X25),X24)))),X27),i(i(i(X23,i(o,i(i(X24,X25),X24))),X26),i(X23,i(o,i(i(X24,X25),X24))))))),X24))) | ~t(i(o,X21)))))). tff(u1748,axiom, (![X1, X0, X2] : ((~t(i(i(X0,X1),X2)) | t(X0) | ~t(i(o,X0)))))). tff(u1747,axiom, (![X9, X11, X7, X8, X10, X12, X6] : ((~t(i(i(X8,X11),X12)) | t(i(X6,i(i(X7,i(o,i(i(i(i(X8,X9),X8),X10),i(i(X8,X9),X8)))),X8))) | ~t(i(o,X7)))))). tff(u1746,negated_conjecture, ~t(i(i(i(sK1,sK2),i(o,sK3)),i(sK4,i(i(sK3,sK1),i(sK5,i(sK0,sK1))))))). tff(u1745,axiom, (![X1, X3, X5, X0, X2, X4] : ((~t(i(i(X1,X4),i(X3,i(o,i(i(X1,X5),X1))))) | t(i(X0,i(i(i(X1,X2),X3),X1))))))). tff(u1744,axiom, (![X11, X13, X15, X10, X12, X14] : ((~t(i(i(X11,X12),i(X10,i(o,i(i(i(i(i(o,i(i(X11,X13),X11)),X14),i(o,i(i(X11,X13),X11))),X15),i(i(i(o,i(i(X11,X13),X11)),X14),i(o,i(i(X11,X13),X11)))))))) | t(X11) | ~t(i(o,X10)))))). tff(u1743,axiom, (![X1, X3, X5, X7, X0, X2, X4, X6] : ((~t(i(i(X3,X4),i(X0,i(o,i(i(i(i(i(o,i(i(X3,X5),X3)),X6),i(o,i(i(X3,X5),X3))),X7),i(i(i(o,i(i(X3,X5),X3)),X6),i(o,i(i(X3,X5),X3)))))))) | t(i(X1,i(X2,X3))) | ~t(i(o,X0)))))). tff(u1742,axiom, (![X9, X1, X3, X5, X7, X8, X0, X2, X4, X6] : ((~t(i(i(X3,X4),i(i(i(o,i(i(X3,X5),X3)),X6),i(X0,i(o,i(i(i(i(i(o,i(i(i(o,i(i(X3,X5),X3)),X7),i(o,i(i(X3,X5),X3)))),X8),i(o,i(i(i(o,i(i(X3,X5),X3)),X7),i(o,i(i(X3,X5),X3))))),X9),i(i(i(o,i(i(i(o,i(i(X3,X5),X3)),X7),i(o,i(i(X3,X5),X3)))),X8),i(o,i(i(i(o,i(i(X3,X5),X3)),X7),i(o,i(i(X3,X5),X3))))))))))) | t(i(X1,i(X2,X3))) | ~t(i(o,X0)))))). tff(u1741,axiom, (![X1, X3, X5, X7, X8, X0, X2, X4, X6] : ((~t(i(i(X0,X5),i(i(i(o,i(i(X0,X1),X0)),X6),i(i(i(o,i(i(i(o,i(i(X0,X1),X0)),X2),i(o,i(i(X0,X1),X0)))),X7),X8)))) | t(i(X3,i(X4,X0))) | ~t(i(o,i(o,i(i(i(o,i(i(X0,X1),X0)),X2),i(o,i(i(X0,X1),X0)))))))))). tff(u1740,axiom, (![X1, X3, X5, X0, X2, X4, X6] : ((~t(i(i(X0,X4),i(i(i(o,i(i(X0,X1),X0)),X5),X6))) | t(i(X2,i(X3,X0))) | ~t(i(o,i(o,i(i(X0,X1),X0)))))))). tff(u1739,axiom, (![X11, X13, X10, X12, X14] : ((~t(i(i(X10,X12),i(i(i(o,i(i(X10,X11),X10)),X13),X14))) | t(X10) | ~t(i(o,i(o,i(i(X10,X11),X10)))))))). tff(u1738,axiom, ((~(![X2] : (~t(i(o,X2))))) | (![X2] : (~t(i(o,X2)))))). tff(u1737,axiom, (![X3, X5, X4, X6] : ((~t(i(o,X6)) | t(i(X3,i(X4,X5))) | ~t(i(X6,X5)))))). tff(u1736,axiom, (![X1, X0] : ((~t(i(o,X0)) | t(i(X1,X0)))))). tff(u1735,axiom, (![X0] : ((~t(i(o,X0)) | t(X0))))). tff(u1734,axiom, (![X1, X3, X0, X2, X4] : ((~t(i(o,i(X1,i(o,i(i(i(i(X0,X2),X0),X3),i(i(X0,X2),X0)))))) | t(X0) | ~t(i(i(i(i(X0,X2),X0),X4),X1)))))). tff(u1733,axiom, (![X1, X3, X5, X0, X2, X4, X6] : ((~t(i(o,i(X5,i(o,i(i(i(i(i(o,i(i(X1,X2),X1)),X3),i(o,i(i(X1,X2),X1))),X6),i(i(i(o,i(i(X1,X2),X1)),X3),i(o,i(i(X1,X2),X1)))))))) | t(i(X0,i(i(i(i(i(i(o,i(i(X1,X2),X1)),X3),i(o,i(i(X1,X2),X1))),X4),X5),X1))))))). tff(u1732,axiom, (![X11, X13, X15, X10, X12, X14] : ((~t(i(o,i(X11,i(o,i(i(i(i(i(o,i(i(i(i(X10,X12),X10),X13),i(i(X10,X12),X10))),X14),i(o,i(i(i(i(X10,X12),X10),X13),i(i(X10,X12),X10)))),X15),i(i(i(o,i(i(i(i(X10,X12),X10),X13),i(i(X10,X12),X10))),X14),i(o,i(i(i(i(X10,X12),X10),X13),i(i(X10,X12),X10))))))))) | t(X10) | ~t(i(o,X11)))))). tff(u1731,axiom, (![X16, X18, X13, X15, X17, X19, X12, X14] : ((~t(i(o,i(X15,i(o,i(i(i(i(i(o,i(i(i(o,i(i(X14,X16),X14)),X17),i(o,i(i(X14,X16),X14)))),X18),i(o,i(i(i(o,i(i(X14,X16),X14)),X17),i(o,i(i(X14,X16),X14))))),X19),i(i(i(o,i(i(i(o,i(i(X14,X16),X14)),X17),i(o,i(i(X14,X16),X14)))),X18),i(o,i(i(i(o,i(i(X14,X16),X14)),X17),i(o,i(i(X14,X16),X14)))))))))) | ~t(i(o,X15)) | t(i(X12,i(X13,X14))))))). tff(u1730,axiom, (![X40, X34, X36, X38, X41, X33, X35, X37, X39] : ((~t(i(o,i(X36,i(o,i(i(i(i(i(o,i(i(i(i(i(o,i(i(X35,X37),X35)),X38),i(o,i(i(X35,X37),X35))),X39),i(i(i(o,i(i(X35,X37),X35)),X38),i(o,i(i(X35,X37),X35))))),X40),i(o,i(i(i(i(i(o,i(i(X35,X37),X35)),X38),i(o,i(i(X35,X37),X35))),X39),i(i(i(o,i(i(X35,X37),X35)),X38),i(o,i(i(X35,X37),X35)))))),X41),i(i(i(o,i(i(i(i(i(o,i(i(X35,X37),X35)),X38),i(o,i(i(X35,X37),X35))),X39),i(i(i(o,i(i(X35,X37),X35)),X38),i(o,i(i(X35,X37),X35))))),X40),i(o,i(i(i(i(i(o,i(i(X35,X37),X35)),X38),i(o,i(i(X35,X37),X35))),X39),i(i(i(o,i(i(X35,X37),X35)),X38),i(o,i(i(X35,X37),X35))))))))))) | t(i(X33,i(X34,X35))) | ~t(i(o,X36)))))). tff(u1729,axiom, (![X9, X11, X13, X15, X10, X12, X14] : ((~t(i(o,i(X9,i(o,i(i(X10,X11),X10))))) | t(i(X12,i(i(i(i(X9,i(o,i(i(X10,X11),X10))),X13),X14),X10))) | ~t(i(i(X10,X15),X9)))))). tff(u1728,axiom, (![X49, X46, X48, X47] : ((~t(i(o,i(i(X46,X47),X46))) | t(i(X48,i(X49,X46))))))). tff(u1727,axiom, (![X51, X50] : ((~t(i(o,i(i(X50,X51),X50))) | t(X50))))). tff(u1726,negated_conjecture, ~t(i(o,i(i(sK3,sK1),i(sK5,i(sK0,sK1)))))). tff(u1725,axiom, (![X1, X0, X2] : ((~t(i(o,i(i(i(i(X0,X1),X0),X2),i(i(X0,X1),X0)))) | t(X0))))). tff(u1724,axiom, (![X1, X3, X0, X2] : ((~t(i(o,i(i(i(i(i(o,i(i(X0,X1),X0)),X2),i(o,i(i(X0,X1),X0))),X3),i(i(i(o,i(i(X0,X1),X0)),X2),i(o,i(i(X0,X1),X0)))))) | t(X0))))). tff(u1723,axiom, (![X1, X3, X5, X0, X2, X4] : ((~t(i(o,i(i(i(i(i(o,i(i(X2,X3),X2)),X4),i(o,i(i(X2,X3),X2))),X5),i(i(i(o,i(i(X2,X3),X2)),X4),i(o,i(i(X2,X3),X2)))))) | t(i(X0,i(X1,X2))))))). tff(u1722,axiom, (![X16, X18, X20, X13, X15, X17, X19, X21, X12, X14] : ((~t(i(o,i(i(i(o,i(i(i(i(i(o,i(i(X14,X15),X14)),X16),i(o,i(i(X14,X15),X14))),X17),i(i(i(o,i(i(X14,X15),X14)),X16),i(o,i(i(X14,X15),X14))))),X18),i(i(i(o,i(i(i(o,i(i(i(i(i(o,i(i(X14,X15),X14)),X16),i(o,i(i(X14,X15),X14))),X17),i(i(i(o,i(i(X14,X15),X14)),X16),i(o,i(i(X14,X15),X14))))),X19),i(o,i(i(i(i(i(o,i(i(X14,X15),X14)),X16),i(o,i(i(X14,X15),X14))),X17),i(i(i(o,i(i(X14,X15),X14)),X16),i(o,i(i(X14,X15),X14))))))),X20),X21)))) | t(i(X12,i(X13,X14))) | ~t(i(o,i(o,i(i(i(o,i(i(i(i(i(o,i(i(X14,X15),X14)),X16),i(o,i(i(X14,X15),X14))),X17),i(i(i(o,i(i(X14,X15),X14)),X16),i(o,i(i(X14,X15),X14))))),X19),i(o,i(i(i(i(i(o,i(i(X14,X15),X14)),X16),i(o,i(i(X14,X15),X14))),X17),i(i(i(o,i(i(X14,X15),X14)),X16),i(o,i(i(X14,X15),X14))))))))))))). tff(u1721,axiom, (![X25, X27, X29, X23, X24, X26, X28] : ((~t(i(o,i(i(i(o,i(i(i(i(X23,X24),X23),X25),i(i(X23,X24),X23))),X27),i(i(i(o,i(i(i(o,i(i(i(i(X23,X24),X23),X25),i(i(X23,X24),X23))),X26),i(o,i(i(i(i(X23,X24),X23),X25),i(i(X23,X24),X23))))),X28),X29)))) | t(X23) | ~t(i(o,i(o,i(i(i(o,i(i(i(i(X23,X24),X23),X25),i(i(X23,X24),X23))),X26),i(o,i(i(i(i(X23,X24),X23),X25),i(i(X23,X24),X23))))))))))). tff(u1720,axiom, (![X1, X0, X2] : ((~t(i(o,i(i(i(o,i(i(X0,X1),X0)),X2),i(o,i(i(X0,X1),X0))))) | t(X0))))). tff(u1719,axiom, (![X1, X3, X0, X2, X4] : ((~t(i(o,i(i(i(o,i(i(X2,X3),X2)),X4),i(o,i(i(X2,X3),X2))))) | t(i(X0,i(X1,X2))))))). tff(u1718,axiom, (![X22, X32, X25, X27, X29, X31, X23, X24, X26, X28, X30] : ((~t(i(o,i(i(i(o,i(i(i(i(i(o,i(i(X24,X25),X24)),X26),i(o,i(i(X24,X25),X24))),X27),i(i(i(o,i(i(X24,X25),X24)),X26),i(o,i(i(X24,X25),X24))))),X28),i(X29,i(o,i(i(i(i(i(o,i(i(i(o,i(i(i(i(i(o,i(i(X24,X25),X24)),X26),i(o,i(i(X24,X25),X24))),X27),i(i(i(o,i(i(X24,X25),X24)),X26),i(o,i(i(X24,X25),X24))))),X30),i(o,i(i(i(i(i(o,i(i(X24,X25),X24)),X26),i(o,i(i(X24,X25),X24))),X27),i(i(i(o,i(i(X24,X25),X24)),X26),i(o,i(i(X24,X25),X24))))))),X31),i(o,i(i(i(o,i(i(i(i(i(o,i(i(X24,X25),X24)),X26),i(o,i(i(X24,X25),X24))),X27),i(i(i(o,i(i(X24,X25),X24)),X26),i(o,i(i(X24,X25),X24))))),X30),i(o,i(i(i(i(i(o,i(i(X24,X25),X24)),X26),i(o,i(i(X24,X25),X24))),X27),i(i(i(o,i(i(X24,X25),X24)),X26),i(o,i(i(X24,X25),X24)))))))),X32),i(i(i(o,i(i(i(o,i(i(i(i(i(o,i(i(X24,X25),X24)),X26),i(o,i(i(X24,X25),X24))),X27),i(i(i(o,i(i(X24,X25),X24)),X26),i(o,i(i(X24,X25),X24))))),X30),i(o,i(i(i(i(i(o,i(i(X24,X25),X24)),X26),i(o,i(i(X24,X25),X24))),X27),i(i(i(o,i(i(X24,X25),X24)),X26),i(o,i(i(X24,X25),X24))))))),X31),i(o,i(i(i(o,i(i(i(i(i(o,i(i(X24,X25),X24)),X26),i(o,i(i(X24,X25),X24))),X27),i(i(i(o,i(i(X24,X25),X24)),X26),i(o,i(i(X24,X25),X24))))),X30),i(o,i(i(i(i(i(o,i(i(X24,X25),X24)),X26),i(o,i(i(X24,X25),X24))),X27),i(i(i(o,i(i(X24,X25),X24)),X26),i(o,i(i(X24,X25),X24)))))))))))))) | t(i(X22,i(X23,X24))) | ~t(i(o,X29)))))). tff(u1717,axiom, (![X9, X5, X7, X8, X6] : ((~t(i(o,i(i(i(o,i(i(i(i(X5,X6),X5),X7),i(i(X5,X6),X5))),X8),X9))) | t(X5) | ~t(i(o,i(o,i(i(i(i(X5,X6),X5),X7),i(i(X5,X6),X5))))))))). tff(u1716,axiom, (![X1, X3, X0, X2] : ((~t(i(o,i(o,i(i(X2,X3),X2)))) | t(i(X0,i(X1,X2))))))). tff(u1715,axiom, (![X1, X0] : ((~t(i(o,i(o,i(i(X0,X1),X0)))) | t(X0))))). tff(u1714,axiom, (![X1, X0, X2] : ((~t(i(o,i(o,i(i(i(i(X0,X1),X0),X2),i(i(X0,X1),X0))))) | t(X0))))). tff(u1713,axiom, (![X32, X34, X31, X33, X30] : ((~t(i(o,i(o,i(i(i(i(X30,X31),X30),X34),i(i(X30,X31),X30))))) | ~t(i(i(i(i(X30,X31),X30),X32),X33)) | t(X30))))). tff(u1712,axiom, (![X1, X3, X0, X2] : ((~t(i(o,i(o,i(i(i(i(i(o,i(i(X0,X1),X0)),X2),i(o,i(i(X0,X1),X0))),X3),i(i(i(o,i(i(X0,X1),X0)),X2),i(o,i(i(X0,X1),X0))))))) | t(X0))))). tff(u1711,axiom, (![X1, X3, X5, X0, X2, X4] : ((~t(i(o,i(o,i(i(i(i(i(o,i(i(X0,X1),X0)),X2),i(o,i(i(X0,X1),X0))),X3),i(i(i(o,i(i(X0,X1),X0)),X2),i(o,i(i(X0,X1),X0))))))) | t(i(X4,i(X5,X0))))))). tff(u1710,axiom, (![X1, X3, X0, X2, X4] : ((~t(i(o,i(o,i(i(i(o,i(i(X2,X3),X2)),X4),i(o,i(i(X2,X3),X2)))))) | t(i(X0,i(X1,X2))))))). tff(u1709,axiom, (![X32, X34, X36, X38, X31, X33, X35, X37, X30] : ((~t(i(o,i(o,i(i(i(X30,i(o,i(i(X31,X32),X31))),X33),i(X30,i(o,i(i(X31,X32),X31))))))) | t(i(X34,i(i(i(i(X30,i(o,i(i(X31,X32),X31))),X35),i(i(i(o,i(i(i(X30,i(o,i(i(X31,X32),X31))),X33),i(X30,i(o,i(i(X31,X32),X31))))),X36),X37)),X31))) | ~t(i(i(X31,X38),X30)))))). tff(u1708,negated_conjecture, ~t(i(o,i(sK0,sK1)))). tff(u1707,negated_conjecture, ~t(i(o,i(sK5,i(sK0,sK1))))). tff(u1706,negated_conjecture, ~t(i(o,sK1))). tff(u1705,axiom, (![X1, X0, X2] : ((t(i(i(i(X0,X1),X2),X0)) | ~t(i(o,X0)))))). tff(u1704,axiom, (![X1, X3, X0, X2, X4] : ((t(i(i(i(X0,X2),i(i(i(o,i(i(X0,X1),X0)),X3),X4)),X0)) | ~t(i(o,i(o,i(i(X0,X1),X0)))))))). tff(u1703,axiom, (![X1, X3, X5, X0, X2, X4, X6] : ((t(i(i(i(X0,X3),i(i(i(o,i(i(X0,X1),X0)),X4),i(i(i(o,i(i(i(o,i(i(X0,X1),X0)),X2),i(o,i(i(X0,X1),X0)))),X5),X6))),X0)) | ~t(i(o,i(o,i(i(i(o,i(i(X0,X1),X0)),X2),i(o,i(i(X0,X1),X0)))))))))). tff(u1702,axiom, (![X1, X3, X5, X7, X0, X2, X4, X6] : ((t(i(i(i(X1,X2),i(i(i(o,i(i(X1,X3),X1)),X4),i(X0,i(o,i(i(i(i(i(o,i(i(i(o,i(i(X1,X3),X1)),X5),i(o,i(i(X1,X3),X1)))),X6),i(o,i(i(i(o,i(i(X1,X3),X1)),X5),i(o,i(i(X1,X3),X1))))),X7),i(i(i(o,i(i(i(o,i(i(X1,X3),X1)),X5),i(o,i(i(X1,X3),X1)))),X6),i(o,i(i(i(o,i(i(X1,X3),X1)),X5),i(o,i(i(X1,X3),X1)))))))))),X1)) | ~t(i(o,X0)))))). tff(u1701,axiom, (![X1, X3, X5, X0, X2, X4] : ((t(i(i(i(X1,X2),i(X0,i(o,i(i(i(i(i(o,i(i(X1,X3),X1)),X4),i(o,i(i(X1,X3),X1))),X5),i(i(i(o,i(i(X1,X3),X1)),X4),i(o,i(i(X1,X3),X1))))))),X1)) | ~t(i(o,X0)))))). tff(u1700,axiom, (![X1, X3, X0, X2] : ((t(i(i(X0,i(o,i(i(i(i(X1,X2),X1),X3),i(i(X1,X2),X1)))),X1)) | ~t(i(o,X0)))))). tff(u1699,axiom, (![X1, X3, X0, X2, X4] : (t(i(i(X0,X1),i(i(X1,i(o,i(i(X2,X3),X2))),i(X4,i(X0,X2)))))))). tff(u1698,axiom, (![X1, X3, X0, X2, X4] : ((t(i(i(X0,i(o,i(i(X1,X2),X1))),i(X3,i(X4,X1)))) | ~t(i(X4,X0)))))). tff(u1697,axiom, (![X1, X3, X0, X2] : ((t(i(X0,i(i(i(X1,X2),X3),X1))) | ~t(i(o,X1)))))). tff(u1696,axiom, (![X16, X11, X13, X15, X12, X14] : ((t(i(X13,i(i(i(X11,X14),i(i(i(o,i(i(X11,X12),X11)),X15),X16)),X11))) | ~t(i(o,i(o,i(i(X11,X12),X11)))))))). tff(u1695,axiom, (![X16, X18, X20, X22, X15, X17, X19, X21] : ((t(i(X18,i(i(i(X15,X19),i(i(i(o,i(i(X15,X16),X15)),X20),i(i(i(o,i(i(i(o,i(i(X15,X16),X15)),X17),i(o,i(i(X15,X16),X15)))),X21),X22))),X15))) | ~t(i(o,i(o,i(i(i(o,i(i(X15,X16),X15)),X17),i(o,i(i(X15,X16),X15)))))))))). tff(u1694,axiom, (![X18, X20, X22, X25, X17, X19, X21, X23, X24] : ((t(i(X18,i(i(i(X19,X20),i(i(i(o,i(i(X19,X21),X19)),X22),i(X17,i(o,i(i(i(i(i(o,i(i(i(o,i(i(X19,X21),X19)),X23),i(o,i(i(X19,X21),X19)))),X24),i(o,i(i(i(o,i(i(X19,X21),X19)),X23),i(o,i(i(X19,X21),X19))))),X25),i(i(i(o,i(i(i(o,i(i(X19,X21),X19)),X23),i(o,i(i(X19,X21),X19)))),X24),i(o,i(i(i(o,i(i(X19,X21),X19)),X23),i(o,i(i(X19,X21),X19)))))))))),X19))) | ~t(i(o,X17)))))). tff(u1693,axiom, (![X16, X18, X13, X15, X17, X19, X14] : ((t(i(X14,i(i(i(X15,X16),i(X13,i(o,i(i(i(i(i(o,i(i(X15,X17),X15)),X18),i(o,i(i(X15,X17),X15))),X19),i(i(i(o,i(i(X15,X17),X15)),X18),i(o,i(i(X15,X17),X15))))))),X15))) | ~t(i(o,X13)))))). tff(u1692,axiom, (![X1, X3, X0, X2, X4] : ((t(i(X0,i(i(X1,i(o,i(i(i(i(X2,X3),X2),X4),i(i(X2,X3),X2)))),X2))) | ~t(i(o,X1)))))). tff(u1691,axiom, (![X1, X3, X5, X0, X2, X4, X6] : ((t(i(X1,i(i(X0,i(o,i(i(i(i(i(i(i(o,i(i(X2,X3),X2)),X4),i(o,i(i(X2,X3),X2))),X5),i(i(i(o,i(i(X2,X3),X2)),X4),i(o,i(i(X2,X3),X2)))),X6),i(i(i(i(i(o,i(i(X2,X3),X2)),X4),i(o,i(i(X2,X3),X2))),X5),i(i(i(o,i(i(X2,X3),X2)),X4),i(o,i(i(X2,X3),X2))))))),X2))) | ~t(i(o,X0)))))). tff(u1690,axiom, (![X63, X65, X67, X60, X62, X64, X66, X61] : ((t(i(X60,i(i(i(i(X61,i(o,i(i(i(i(i(o,i(i(X62,X63),X62)),X64),i(o,i(i(X62,X63),X62))),X65),i(i(i(o,i(i(X62,X63),X62)),X64),i(o,i(i(X62,X63),X62)))))),X66),X67),X62))) | ~t(i(o,X61)) | ~t(i(o,i(X61,i(o,i(i(i(i(i(o,i(i(X62,X63),X62)),X64),i(o,i(i(X62,X63),X62))),X65),i(i(i(o,i(i(X62,X63),X62)),X64),i(o,i(i(X62,X63),X62)))))))))))). tff(u1689,axiom, (![X63, X65, X67, X62, X64, X66, X68, X61] : ((t(i(X61,i(i(X62,i(o,i(i(i(i(i(i(X63,X64),i(o,i(i(X65,X66),X65))),X67),i(i(X63,X64),i(o,i(i(X65,X66),X65)))),X68),i(i(i(i(X63,X64),i(o,i(i(X65,X66),X65))),X67),i(i(X63,X64),i(o,i(i(X65,X66),X65))))))),X65))) | ~t(i(o,X62)) | ~t(i(o,X64)))))). tff(u1688,axiom, (![X16, X18, X11, X13, X15, X17, X10, X12, X14] : ((t(i(X10,i(i(X11,i(o,i(i(i(i(i(i(X12,i(X13,X14)),i(o,i(i(X15,X16),X15))),X17),i(i(X12,i(X13,X14)),i(o,i(i(X15,X16),X15)))),X18),i(i(i(i(X12,i(X13,X14)),i(o,i(i(X15,X16),X15))),X17),i(i(X12,i(X13,X14)),i(o,i(i(X15,X16),X15))))))),X15))) | ~t(i(o,X11)) | ~t(i(X13,X15)))))). tff(u1687,axiom, (![X1, X3, X5, X0, X2, X4, X6] : ((t(i(X1,i(i(X0,i(o,i(i(i(i(i(X2,i(o,i(i(i(X2,X3),X4),i(X2,X3)))),X5),i(X2,i(o,i(i(i(X2,X3),X4),i(X2,X3))))),X6),i(i(i(X2,i(o,i(i(i(X2,X3),X4),i(X2,X3)))),X5),i(X2,i(o,i(i(i(X2,X3),X4),i(X2,X3)))))))),i(X2,X3)))) | ~t(i(o,X0)))))). tff(u1686,axiom, (![X1, X0, X2] : ((t(i(X1,i(X2,X0))) | ~t(i(o,X0)))))). % # 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]: 6780 % Time elapsed: 0.030 s % ------------------------------ % ------------------------------ % Success in time 195.242 s