% 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 CC01C2CCC30C1CN4N1C04 % 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]: 11129 % Time elapsed: 0.811 s % ------------------------------ % ------------------------------ % fmb+10_1_av=off:bce=on:nm=6_1461 on CC01C2CCC30C1CN4N1C04 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]: 53858 % 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 CC01C2CCC30C1CN4N1C04 % SZS status CounterSatisfiable for CC01C2CCC30C1CN4N1C04 % # SZS output start Saturation. tff(u126,axiom, (![X1, X0] : ((~t(i(X0,X1)) | t(X1) | ~t(X0))))). tff(u125,axiom, (![X16, X13, X15, X17, X12, X14] : ((~t(i(X16,i(n(i(n(X17),n(i(i(i(X12,X13),i(X14,i(n(X15),n(X14)))),i(X13,X15))))),n(X16)))) | ~t(i(X13,X14)) | t(X17) | ~t(i(i(i(i(X12,X13),i(X14,i(n(X15),n(X14)))),i(X13,X15)),X16)))))). tff(u124,axiom, (![X1, X3, X5, X0, X2, X4, X6] : ((~t(i(i(n(i(n(i(X5,i(n(X6),n(X5)))),n(i(i(i(X0,X1),i(X2,i(n(X3),n(X2)))),i(X1,X3))))),n(X4)),X5)) | ~t(i(X1,X2)) | t(i(i(n(i(n(i(X5,i(n(X6),n(X5)))),n(i(i(i(X0,X1),i(X2,i(n(X3),n(X2)))),i(X1,X3))))),n(X4)),X6)) | ~t(i(i(i(i(X0,X1),i(X2,i(n(X3),n(X2)))),i(X1,X3)),X4)))))). tff(u123,axiom, (![X1, X3, X0, X2] : ((~t(i(i(X1,i(n(i(n(X2),n(X0))),n(X1))),X0)) | t(i(n(i(i(X1,i(n(i(n(X2),n(X0))),n(X1))),X2)),X3)) | ~t(i(X0,X1)))))). tff(u122,axiom, (![X1, X0, X2] : ((~t(i(i(X0,i(n(i(n(X1),n(X2))),n(X0))),X2)) | t(i(i(X0,i(n(i(n(X1),n(X2))),n(X0))),X1)) | ~t(i(X2,X0)))))). tff(u121,axiom, (![X1, X3, X5, X0, X2, X4, X6] : ((~t(i(i(i(i(X2,X0),i(X1,i(n(X3),n(X1)))),i(X0,X3)),X4)) | ~t(i(X0,X1)) | t(i(n(X4),X5)) | ~t(i(n(X4),X6)))))). tff(u120,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(u119,axiom, (![X1, X3, X0, X2] : ((~t(i(i(X3,X0),i(X1,i(n(X2),n(X1))))) | t(i(X0,X2)) | ~t(i(X0,X1)))))). tff(u118,axiom, ((~(![X16, X18, X11, X13, X15, X17, X10, X12] : ((~t(i(i(i(i(X15,X12),i(X13,i(n(X16),n(X13)))),i(X12,X16)),n(i(i(i(X17,X10),i(X11,i(n(X18),n(X11)))),i(X10,X18))))) | ~t(i(X10,X11)) | ~t(i(X12,X13)))))) | (![X16, X18, X11, X13, X15, X17, X10, X12] : ((~t(i(i(i(i(X15,X12),i(X13,i(n(X16),n(X13)))),i(X12,X16)),n(i(i(i(X17,X10),i(X11,i(n(X18),n(X11)))),i(X10,X18))))) | ~t(i(X10,X11)) | ~t(i(X12,X13))))))). tff(u117,axiom, ((~(![X40, X42, X44, X34, X36, X41, X43, X45, X35, X37, X39] : ((~t(i(i(i(i(X39,X36),i(X37,i(n(X40),n(X37)))),i(X36,X40)),n(i(X41,i(i(i(X42,i(i(X43,X34),i(X35,i(n(X44),n(X35))))),i(i(X34,X44),i(n(X45),n(i(X34,X44))))),i(i(i(X43,X34),i(X35,i(n(X44),n(X35)))),X45)))))) | ~t(i(X34,X35)) | ~t(i(X36,X37)))))) | (![X40, X42, X44, X34, X36, X41, X43, X45, X35, X37, X39] : ((~t(i(i(i(i(X39,X36),i(X37,i(n(X40),n(X37)))),i(X36,X40)),n(i(X41,i(i(i(X42,i(i(X43,X34),i(X35,i(n(X44),n(X35))))),i(i(X34,X44),i(n(X45),n(i(X34,X44))))),i(i(i(X43,X34),i(X35,i(n(X44),n(X35)))),X45)))))) | ~t(i(X34,X35)) | ~t(i(X36,X37))))))). tff(u116,axiom, ((~(![X32, X34, X36, X27, X29, X31, X35, X26, X28, X30] : ((~t(i(i(i(i(X34,X31),i(X32,i(n(X35),n(X32)))),i(X31,X35)),n(i(i(X30,i(n(i(n(X36),n(i(i(i(X26,X27),i(X28,i(n(X29),n(X28)))),i(X27,X29))))),n(X30))),X36)))) | ~t(i(i(i(i(X26,X27),i(X28,i(n(X29),n(X28)))),i(X27,X29)),X30)) | ~t(i(X31,X32)) | ~t(i(X27,X28)))))) | (![X32, X34, X36, X27, X29, X31, X35, X26, X28, X30] : ((~t(i(i(i(i(X34,X31),i(X32,i(n(X35),n(X32)))),i(X31,X35)),n(i(i(X30,i(n(i(n(X36),n(i(i(i(X26,X27),i(X28,i(n(X29),n(X28)))),i(X27,X29))))),n(X30))),X36)))) | ~t(i(i(i(i(X26,X27),i(X28,i(n(X29),n(X28)))),i(X27,X29)),X30)) | ~t(i(X31,X32)) | ~t(i(X27,X28))))))). tff(u115,axiom, (![X18, X20, X17, X19, X21] : ((~t(i(n(i(i(X18,i(n(i(n(X19),n(X17))),n(X18))),X19)),X21)) | t(i(n(i(i(X18,i(n(i(n(X19),n(X17))),n(X18))),X19)),X20)) | ~t(i(X17,X18)) | ~t(i(i(X18,i(n(i(n(X19),n(X17))),n(X18))),X17)))))). tff(u114,axiom, (![X1, X3, X5, X0, X2, X4] : ((~t(i(n(i(i(i(X0,X1),i(X2,i(n(X3),n(X2)))),i(X1,X3))),X4)) | t(i(n(i(i(i(X0,X1),i(X2,i(n(X3),n(X2)))),i(X1,X3))),X5)) | ~t(i(X1,X2)))))). tff(u113,axiom, (![X1, X3, X5, X7, X8, X0, X2, X4, X6] : ((~t(i(n(i(X2,i(i(i(X3,i(i(X4,X0),i(X1,i(n(X5),n(X1))))),i(i(X0,X5),i(n(X6),n(i(X0,X5))))),i(i(i(X4,X0),i(X1,i(n(X5),n(X1)))),X6)))),X8)) | t(i(n(i(X2,i(i(i(X3,i(i(X4,X0),i(X1,i(n(X5),n(X1))))),i(i(X0,X5),i(n(X6),n(i(X0,X5))))),i(i(i(X4,X0),i(X1,i(n(X5),n(X1)))),X6)))),X7)) | ~t(i(X0,X1)))))). tff(u112,axiom, (![X18, X20, X22, X25, X27, X19, X21, X23, X24, X26] : ((~t(i(n(i(n(i(i(i(i(X26,X23),i(X24,i(n(X27),n(X24)))),i(X23,X27)),i(n(X25),n(i(i(i(X26,X23),i(X24,i(n(X27),n(X24)))),i(X23,X27)))))),n(i(i(i(X20,X18),i(X19,i(n(X21),n(X19)))),i(X18,X21))))),n(X22))) | ~t(i(i(i(i(X20,X18),i(X19,i(n(X21),n(X19)))),i(X18,X21)),X22)) | ~t(i(X23,X24)) | t(X25) | ~t(i(X18,X19)))))). tff(u111,axiom, ((~(![X9, X5, X8, X6] : ((~t(n(i(i(i(X8,X5),i(X6,i(n(X9),n(X6)))),i(X5,X9)))) | ~t(i(X5,X6)))))) | (![X9, X5, X8, X6] : ((~t(n(i(i(i(X8,X5),i(X6,i(n(X9),n(X6)))),i(X5,X9)))) | ~t(i(X5,X6))))))). tff(u110,axiom, ((~(![X32, X27, X29, X31, X33, X26, X30] : ((~t(n(i(X29,i(i(i(X30,i(i(X31,X26),i(X27,i(n(X32),n(X27))))),i(i(X26,X32),i(n(X33),n(i(X26,X32))))),i(i(i(X31,X26),i(X27,i(n(X32),n(X27)))),X33))))) | ~t(i(X26,X27)))))) | (![X32, X27, X29, X31, X33, X26, X30] : ((~t(n(i(X29,i(i(i(X30,i(i(X31,X26),i(X27,i(n(X32),n(X27))))),i(i(X26,X32),i(n(X33),n(i(X26,X32))))),i(i(i(X31,X26),i(X27,i(n(X32),n(X27)))),X33))))) | ~t(i(X26,X27))))))). tff(u109,axiom, ((~(![X20, X22, X25, X19, X21, X23] : ((~t(n(i(i(X23,i(n(i(n(X25),n(i(i(i(X19,X20),i(X21,i(n(X22),n(X21)))),i(X20,X22))))),n(X23))),X25))) | ~t(i(i(i(i(X19,X20),i(X21,i(n(X22),n(X21)))),i(X20,X22)),X23)) | ~t(i(X20,X21)))))) | (![X20, X22, X25, X19, X21, X23] : ((~t(n(i(i(X23,i(n(i(n(X25),n(i(i(i(X19,X20),i(X21,i(n(X22),n(X21)))),i(X20,X22))))),n(X23))),X25))) | ~t(i(i(i(i(X19,X20),i(X21,i(n(X22),n(X21)))),i(X20,X22)),X23)) | ~t(i(X20,X21))))))). tff(u108,axiom, (![X1, X3, X5, X0, X2, X4] : ((t(i(i(X0,i(n(i(n(X1),n(i(i(i(X2,X3),i(X4,i(n(X5),n(X4)))),i(X3,X5))))),n(X0))),X1)) | ~t(i(i(i(i(X2,X3),i(X4,i(n(X5),n(X4)))),i(X3,X5)),X0)) | ~t(i(X3,X4)))))). tff(u107,axiom, (![X9, X1, X3, X5, X7, X8, X0, X2, X4, X6] : ((t(i(i(n(i(n(i(i(i(i(X2,X3),i(X4,i(n(X5),n(X4)))),i(X3,X5)),i(n(X6),n(i(i(i(X2,X3),i(X4,i(n(X5),n(X4)))),i(X3,X5)))))),n(i(i(i(X7,X0),i(X1,i(n(X8),n(X1)))),i(X0,X8))))),n(X9)),X6)) | ~t(i(X0,X1)) | ~t(i(i(i(i(X7,X0),i(X1,i(n(X8),n(X1)))),i(X0,X8)),X9)) | ~t(i(X3,X4)))))). tff(u106,axiom, (![X1, X3, X0, X2, X4] : ((t(i(n(i(i(i(X2,X0),i(X1,i(n(X3),n(X1)))),i(X0,X3))),X4)) | ~t(i(X0,X1)))))). tff(u105,axiom, (![X1, X3, X5, X0, X2, X4, X6] : ((t(i(n(i(i(X0,i(n(i(n(X1),n(i(i(i(X2,X3),i(X4,i(n(X5),n(X4)))),i(X3,X5))))),n(X0))),X1)),X6)) | ~t(i(i(i(i(X2,X3),i(X4,i(n(X5),n(X4)))),i(X3,X5)),X0)) | ~t(i(X3,X4)))))). tff(u104,axiom, (![X1, X3, X5, X7, X0, X2, X4, X6] : ((t(i(n(i(X2,i(i(i(X3,i(i(X4,X0),i(X1,i(n(X5),n(X1))))),i(i(X0,X5),i(n(X6),n(i(X0,X5))))),i(i(i(X4,X0),i(X1,i(n(X5),n(X1)))),X6)))),X7)) | ~t(i(X0,X1)))))). tff(u103,axiom, (![X1, X3, X0, X2, X4] : (t(i(i(X0,X1),i(X2,i(i(i(X3,X0),i(X1,i(n(X4),n(X1)))),i(X0,X4)))))))). tff(u102,axiom, (![X1, X3, X0, X2, X4] : ((t(i(X0,i(i(i(X1,X2),i(X3,i(n(X4),n(X3)))),i(X2,X4)))) | ~t(i(X2,X3)))))). tff(u101,axiom, (![X1, X3, X0, X2] : ((t(i(i(i(X2,X0),i(X1,i(n(X3),n(X1)))),i(X0,X3))) | ~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]: 5500 % Time elapsed: 0.002 s % ------------------------------ % ------------------------------ % Success in time 199.325 s