% 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 C0CCN12CCC13C2C0N4C41 % 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]: 9466 % Time elapsed: 0.800 s % ------------------------------ % ------------------------------ % fmb+10_1_av=off:bce=on:nm=6_1461 on C0CCN12CCC13C2C0N4C41 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]: 94540 % 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 C0CCN12CCC13C2C0N4C41 % SZS status CounterSatisfiable for C0CCN12CCC13C2C0N4C41 % # SZS output start Saturation. tff(u658,axiom, (![X1, X0] : ((~t(i(X0,X1)) | t(X1) | ~t(X0))))). tff(u657,axiom, (![X5, X4, X6] : ((~t(i(X6,n(X4))) | ~t(X6) | t(i(X4,X5)))))). tff(u656,axiom, ((~(![X5, X6] : ((~t(i(X5,n(X6))) | ~t(X5) | ~t(X6))))) | (![X5, X6] : ((~t(i(X5,n(X6))) | ~t(X5) | ~t(X6)))))). tff(u655,axiom, (![X1, X0, X2] : ((~t(i(X0,n(n(X1)))) | t(i(X2,X1)) | ~t(X0))))). tff(u654,axiom, ((~(![X1] : (t(i(X1,n(n(X1))))))) | (![X9, X7, X8] : ((~t(i(X9,n(n(n(n(X8)))))) | t(i(X7,X8)) | ~t(X9)))))). tff(u653,axiom, ((~(![X1] : (t(i(X1,n(n(X1))))))) | (~(![X27, X29, X24, X28, X30] : ((~t(i(i(n(X27),X30),i(X29,i(X28,n(X24))))) | ~t(X27) | ~t(X24) | ~t(i(n(n(X27)),X29)) | ~t(X28))))) | (![X22, X21] : ((~t(i(X21,n(n(n(n(n(X22))))))) | ~t(X22) | ~t(X21)))))). tff(u652,axiom, ((~(![X1] : (t(i(X1,n(n(X1))))))) | (![X27, X29, X28] : ((~t(i(X27,n(n(n(n(n(X28))))))) | t(i(X28,X29)) | ~t(X27)))))). tff(u651,axiom, ((~(![X27, X29, X24, X28, X30] : ((~t(i(i(n(X27),X30),i(X29,i(X28,n(X24))))) | ~t(X27) | ~t(X24) | ~t(i(n(n(X27)),X29)) | ~t(X28))))) | (![X1, X0] : ((~t(i(X1,n(n(n(X0))))) | ~t(X0) | ~t(X1)))))). tff(u650,axiom, (![X1, X0, X2] : ((~t(i(X2,n(n(n(X0))))) | t(i(X0,X1)) | ~t(X2))))). tff(u649,axiom, (![X25, X27, X26, X28] : ((~t(i(X25,n(i(X26,X27)))) | ~t(X25) | t(i(X28,X26)))))). tff(u648,axiom, (![X11, X13, X15, X12, X14] : ((~t(i(X13,n(i(i(X14,n(n(X12))),X15)))) | t(i(X11,X12)) | ~t(X13) | ~t(X14))))). tff(u647,axiom, ((~(![X27, X29, X24, X28, X30] : ((~t(i(i(n(X27),X30),i(X29,i(X28,n(X24))))) | ~t(X27) | ~t(X24) | ~t(i(n(n(X27)),X29)) | ~t(X28))))) | (![X16, X18, X15, X17] : ((~t(i(X15,n(i(i(X16,n(n(n(X17)))),X18)))) | ~t(X17) | ~t(X15) | ~t(X16)))))). tff(u646,axiom, (![X20, X22, X19, X21, X23] : ((~t(i(X19,n(i(i(X20,n(n(n(X21)))),X22)))) | t(i(X21,X23)) | ~t(X19) | ~t(X20))))). tff(u645,axiom, (![X9, X5, X7, X8, X10, X4, X6] : ((~t(i(X6,n(i(i(n(X7),X8),i(i(i(X7,X9),i(X8,i(n(X5),n(X10)))),i(X10,X7)))))) | t(i(X4,X5)) | ~t(X6))))). tff(u644,axiom, ((~(![X27, X29, X24, X28, X30] : ((~t(i(i(n(X27),X30),i(X29,i(X28,n(X24))))) | ~t(X27) | ~t(X24) | ~t(i(n(n(X27)),X29)) | ~t(X28))))) | (![X9, X11, X13, X10, X12, X14] : ((~t(i(X9,n(i(i(n(X10),X11),i(i(i(X10,X12),i(X11,i(n(n(X13)),n(X14)))),i(X14,X10)))))) | ~t(X13) | ~t(X9)))))). tff(u643,axiom, (![X16, X18, X13, X15, X17, X12, X14] : ((~t(i(X12,n(i(i(n(X13),X14),i(i(i(X13,X15),i(X14,i(n(n(X16)),n(X17)))),i(X17,X13)))))) | t(i(X16,X18)) | ~t(X12))))). tff(u642,axiom, ((~(![X27, X29, X24, X28, X30] : ((~t(i(i(n(X27),X30),i(X29,i(X28,n(X24))))) | ~t(X27) | ~t(X24) | ~t(i(n(n(X27)),X29)) | ~t(X28))))) | (![X7, X8, X6] : ((~t(i(X7,n(i(n(X6),X8)))) | ~t(X7) | ~t(X6)))))). tff(u641,axiom, (![X9, X11, X10, X12] : ((~t(i(X11,n(i(n(X9),X12)))) | ~t(X11) | t(i(X9,X10)))))). tff(u640,axiom, ((~(![X27, X29, X24, X28, X30] : ((~t(i(i(n(X27),X30),i(X29,i(X28,n(X24))))) | ~t(X27) | ~t(X24) | ~t(i(n(n(X27)),X29)) | ~t(X28))))) | (![X16, X18, X15, X17] : ((~t(i(X17,i(X18,n(X16)))) | ~t(X16) | ~t(i(n(n(X15)),X17)) | ~t(X18) | ~t(X15)))))). tff(u639,axiom, (![X18, X20, X22, X19, X21] : ((~t(i(X21,i(X19,n(X18)))) | ~t(X19) | ~t(i(n(n(X20)),X21)) | t(i(X20,X22)) | ~t(X18))))). tff(u638,axiom, (![X5, X7, X4, X6] : ((~t(i(X4,i(X5,n(X6)))) | ~t(i(n(X7),X4)) | t(i(X6,X7)) | ~t(X5))))). tff(u637,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(u636,axiom, (![X1, X3, X0, X2, X4] : ((~t(i(i(X1,X4),i(X2,i(X0,n(X3))))) | ~t(i(n(X1),X2)) | t(i(X3,X1)) | ~t(X0))))). tff(u635,axiom, ((~(![X27, X29, X24, X28, X30] : ((~t(i(i(n(X27),X30),i(X29,i(X28,n(X24))))) | ~t(X27) | ~t(X24) | ~t(i(n(n(X27)),X29)) | ~t(X28))))) | (![X27, X29, X24, X28, X30] : ((~t(i(i(n(X27),X30),i(X29,i(X28,n(X24))))) | ~t(X27) | ~t(X24) | ~t(i(n(n(X27)),X29)) | ~t(X28)))))). tff(u634,axiom, (![X20, X22, X25, X21, X23, X24] : ((~t(i(i(n(X20),X25),i(X24,i(X23,n(X22))))) | ~t(X22) | ~t(X23) | ~t(i(n(n(X20)),X24)) | t(i(X20,X21)))))). tff(u633,axiom, (![X20, X22, X21, X23, X24] : ((~t(i(i(n(X20),X21),i(X22,i(X23,n(X24))))) | t(i(X20,n(n(X20)))) | ~t(X24) | ~t(X23))))). tff(u632,negated_conjecture, ~t(i(i(sK4,sK0),i(sK3,sK0)))). tff(u631,axiom, (![X1, X0, X2] : ((~t(i(n(X1),X0)) | ~t(n(X0)) | t(i(X2,X1)))))). tff(u630,axiom, (![X11, X13, X10, X12] : ((~t(i(n(X10),X11)) | t(i(X12,X10)) | ~t(X13) | ~t(i(X13,n(X12))))))). tff(u629,axiom, (![X1, X3, X0, X2] : ((~t(i(n(X0),X1)) | t(i(X2,X0)) | ~t(i(X3,n(X1))) | ~t(X3))))). tff(u628,axiom, (![X1, X0, X2] : ((~t(i(n(X0),X1)) | ~t(X0) | t(i(X2,X0)))))). tff(u627,axiom, ((~(![X27, X29, X24, X28, X30] : ((~t(i(i(n(X27),X30),i(X29,i(X28,n(X24))))) | ~t(X27) | ~t(X24) | ~t(i(n(n(X27)),X29)) | ~t(X28))))) | (![X1, X0, X2] : ((~t(i(n(n(X0)),X1)) | ~t(i(X2,n(X1))) | ~t(X0) | ~t(X2)))))). tff(u626,axiom, ((~(![X27, X29, X24, X28, X30] : ((~t(i(i(n(X27),X30),i(X29,i(X28,n(X24))))) | ~t(X27) | ~t(X24) | ~t(i(n(n(X27)),X29)) | ~t(X28))))) | (![X1, X0] : ((~t(i(n(n(X0)),X1)) | ~t(X0) | ~t(n(X1))))))). tff(u625,axiom, (![X1, X3, X0, X2] : ((~t(i(n(n(X2)),X1)) | ~t(i(X0,n(X1))) | t(i(X2,X3)) | ~t(X0))))). tff(u624,axiom, (![X1, X0, X2] : ((~t(i(n(n(X0)),X1)) | t(i(X0,X2)) | ~t(n(X1)))))). tff(u623,axiom, (![X1, X3, X0, X2] : ((~t(i(n(i(X1,n(X0))),X3)) | ~t(X1) | t(i(X0,i(i(X1,n(X0)),X2))))))). tff(u622,axiom, (![X1, X3, X0, X2, X4] : ((~t(i(n(i(i(X0,n(X1)),X2)),X3)) | t(i(X1,i(i(X0,n(X1)),X2))) | ~t(X0) | ~t(i(n(i(X0,n(X1))),X4)))))). tff(u621,axiom, (![X1, X3, X0, X2, X4] : ((~t(i(n(n(n(X0))),i(i(n(X0),X1),i(X2,i(X3,n(X4)))))) | t(i(X0,n(n(X0)))) | ~t(X4) | ~t(X3))))). tff(u620,axiom, ((~(![X27, X29, X24, X28, X30] : ((~t(i(i(n(X27),X30),i(X29,i(X28,n(X24))))) | ~t(X27) | ~t(X24) | ~t(i(n(n(X27)),X29)) | ~t(X28))))) | (![X9, X5, X7, X8, X4, X6] : ((~t(i(n(n(X5)),i(i(n(X4),X6),i(X7,i(X8,n(X9)))))) | ~t(X4) | ~t(X9) | ~t(X5) | ~t(X8) | ~t(i(n(n(X4)),X7))))))). tff(u619,axiom, (![X9, X11, X5, X7, X8, X10, X6] : ((~t(i(n(n(X6)),i(i(n(X7),X8),i(X9,i(X10,n(X5)))))) | ~t(X5) | t(i(X6,X11)) | ~t(X7) | ~t(X10) | ~t(i(n(n(X7)),X9)))))). tff(u618,axiom, ((~(![X27, X29, X24, X28, X30] : ((~t(i(i(n(X27),X30),i(X29,i(X28,n(X24))))) | ~t(X27) | ~t(X24) | ~t(i(n(n(X27)),X29)) | ~t(X28))))) | (![X1, X0, X2] : ((~t(i(n(n(X0)),i(X1,n(i(n(X0),X2))))) | ~t(X0) | ~t(X1)))))). tff(u617,axiom, (![X1, X3, X0, X2] : ((~t(i(n(n(X0)),i(X1,n(i(n(X0),X2))))) | t(i(X0,X3)) | ~t(X1))))). tff(u616,axiom, ((~(![X27, X29, X24, X28, X30] : ((~t(i(i(n(X27),X30),i(X29,i(X28,n(X24))))) | ~t(X27) | ~t(X24) | ~t(i(n(n(X27)),X29)) | ~t(X28))))) | (![X1, X0, X2] : ((~t(i(n(n(X0)),i(X1,n(X2)))) | ~t(X0) | ~t(X1) | ~t(X2)))))). tff(u615,axiom, (![X1, X3, X0, X2] : ((~t(i(n(n(X0)),i(X1,n(X2)))) | t(i(X0,X3)) | ~t(X1) | ~t(X2))))). tff(u614,axiom, (![X1, X3, X0, X2] : ((~t(i(n(X1),i(X0,n(i(X1,X2))))) | ~t(X0) | t(i(X3,X1)))))). tff(u613,axiom, (![X1, X3, X0, X2] : ((~t(i(n(X0),i(X1,n(X2)))) | t(i(X3,X0)) | ~t(X1) | ~t(X2))))). tff(u612,axiom, (![X9, X5, X7, X8, X4, X6] : ((~t(i(n(X4),i(i(n(X5),X6),i(X7,i(X8,n(X9)))))) | t(i(X5,X4)) | ~t(X9) | ~t(X8) | ~t(i(n(n(X5)),X7)))))). tff(u611,axiom, ((~(![X1] : (t(i(X1,n(n(X1))))))) | (![X1, X0, X2] : ((~t(i(n(X1),n(X0))) | ~t(X0) | t(i(X2,X1))))))). tff(u610,axiom, ((~(![X1] : (t(i(X1,n(n(X1))))))) | (~(![X27, X29, X24, X28, X30] : ((~t(i(i(n(X27),X30),i(X29,i(X28,n(X24))))) | ~t(X27) | ~t(X24) | ~t(i(n(n(X27)),X29)) | ~t(X28))))) | (![X1, X0] : ((~t(i(n(n(X0)),n(X1))) | ~t(X0) | ~t(X1)))))). tff(u609,axiom, ((~(![X1] : (t(i(X1,n(n(X1))))))) | (![X1, X0, X2] : ((~t(i(n(n(X0)),n(X1))) | t(i(X0,X2)) | ~t(X1)))))). tff(u608,negated_conjecture, ~t(i(sK3,sK0))). tff(u607,axiom, ((~(![X5, X6] : ((~t(i(X5,n(X6))) | ~t(X5) | ~t(X6))))) | (![X1] : ((~t(n(X1)) | ~t(X1)))))). tff(u606,axiom, (![X1, X0, X2] : ((~t(n(i(X0,X1))) | t(i(X2,X0)))))). tff(u605,negated_conjecture, ~t(n(i(i(i(i(sK0,sK1),i(n(sK2),n(sK3))),sK2),sK4)))). tff(u604,axiom, (![X1, X3, X0, X2] : ((~t(n(i(i(X0,n(n(X2))),X3))) | t(i(X1,X2)) | ~t(X0))))). tff(u603,axiom, ((~(![X27, X29, X24, X28, X30] : ((~t(i(i(n(X27),X30),i(X29,i(X28,n(X24))))) | ~t(X27) | ~t(X24) | ~t(i(n(n(X27)),X29)) | ~t(X28))))) | (![X11, X13, X12] : ((~t(n(i(i(X12,n(n(n(X11)))),X13))) | ~t(X11) | ~t(X12)))))). tff(u602,axiom, (![X16, X18, X15, X17] : ((~t(n(i(i(X17,n(n(n(X15)))),X18))) | t(i(X15,X16)) | ~t(X17))))). tff(u601,axiom, (![X1, X3, X5, X0, X2, X4] : ((~t(n(i(i(n(X0),X1),i(i(i(X0,X2),i(X1,i(n(X3),n(X4)))),i(X4,X0))))) | t(i(X5,X3)))))). tff(u600,axiom, ((~(![X27, X29, X24, X28, X30] : ((~t(i(i(n(X27),X30),i(X29,i(X28,n(X24))))) | ~t(X27) | ~t(X24) | ~t(i(n(n(X27)),X29)) | ~t(X28))))) | (![X9, X7, X8, X10, X6] : ((~t(n(i(i(n(X7),X8),i(i(i(X7,X9),i(X8,i(n(n(X6)),n(X10)))),i(X10,X7))))) | ~t(X6)))))). tff(u599,axiom, (![X9, X11, X13, X10, X12, X14] : ((~t(n(i(i(n(X11),X12),i(i(i(X11,X13),i(X12,i(n(n(X9)),n(X14)))),i(X14,X11))))) | t(i(X9,X10)))))). tff(u598,axiom, ((~(![X27, X29, X24, X28, X30] : ((~t(i(i(n(X27),X30),i(X29,i(X28,n(X24))))) | ~t(X27) | ~t(X24) | ~t(i(n(n(X27)),X29)) | ~t(X28))))) | (![X1, X0] : ((~t(n(i(n(X0),X1))) | ~t(X0)))))). tff(u597,axiom, ((~(![X27, X29, X24, X28, X30] : ((~t(i(i(n(X27),X30),i(X29,i(X28,n(X24))))) | ~t(X27) | ~t(X24) | ~t(i(n(n(X27)),X29)) | ~t(X28))))) | (![X1, X0, X2] : ((~t(n(i(n(X0),X2))) | ~t(i(n(n(X0)),X1)) | ~t(X0)))))). tff(u596,axiom, (![X1, X0, X2] : ((~t(n(i(n(X0),X1))) | t(i(X0,X2)))))). tff(u595,axiom, (![X1, X3, X0, X2] : ((~t(n(i(n(X0),X3))) | t(i(X0,X2)) | ~t(i(n(n(X0)),X1)))))). tff(u594,negated_conjecture, ~t(n(i(sK4,sK0)))). tff(u593,axiom, (![X1, X0] : ((~t(n(n(X0))) | t(i(X1,X0)))))). tff(u592,axiom, ((~(![X1] : (t(i(X1,n(n(X1))))))) | (![X1, X0] : ((~t(n(n(n(n(X0))))) | t(i(X1,X0))))))). tff(u591,axiom, ((~(![X1] : (t(i(X1,n(n(X1))))))) | (~(![X27, X29, X24, X28, X30] : ((~t(i(i(n(X27),X30),i(X29,i(X28,n(X24))))) | ~t(X27) | ~t(X24) | ~t(i(n(n(X27)),X29)) | ~t(X28))))) | (![X15] : ((~t(n(n(n(n(n(X15)))))) | ~t(X15)))))). tff(u590,axiom, ((~(![X1] : (t(i(X1,n(n(X1))))))) | (![X22, X21] : ((~t(n(n(n(n(n(X21)))))) | t(i(X21,X22))))))). tff(u589,axiom, ((~(![X27, X29, X24, X28, X30] : ((~t(i(i(n(X27),X30),i(X29,i(X28,n(X24))))) | ~t(X27) | ~t(X24) | ~t(i(n(n(X27)),X29)) | ~t(X28))))) | (![X0] : ((~t(n(n(n(X0)))) | ~t(X0)))))). tff(u588,axiom, (![X1, X0] : ((~t(n(n(n(X0)))) | t(i(X0,X1)))))). tff(u587,negated_conjecture, ~t(n(sK3))). tff(u586,negated_conjecture, ~t(sK0)). tff(u585,axiom, (![X1, X0] : ((t(i(X0,X1)) | ~t(n(X0)))))). tff(u584,axiom, (![X1, X0] : ((t(i(X1,X0)) | ~t(X0))))). tff(u583,axiom, ((~(![X1] : (t(i(X1,n(n(X1))))))) | (![X3, X2] : ((t(i(n(X2),X3)) | ~t(X2)))))). tff(u582,axiom, (![X1, X0, X2] : ((t(i(i(X0,n(X1)),X2)) | ~t(X0) | ~t(X1))))). tff(u581,axiom, (![X1, X3, X0, X2, X4] : (t(i(X0,i(i(n(X1),X2),i(i(i(X1,X3),i(X2,i(X0,n(X4)))),i(X4,X1)))))))). tff(u580,axiom, (![X1, X3, X0, X2, X4] : ((t(i(i(n(X0),X1),i(i(i(X0,X2),i(X1,i(X3,n(X4)))),i(X4,X0)))) | ~t(X3))))). tff(u579,axiom, (![X1, X0, X2] : ((t(i(X1,i(i(X0,n(X1)),X2))) | ~t(X0))))). tff(u578,axiom, (![X1, X3, X0, X2, X4] : ((t(i(i(i(X1,X2),i(X3,i(X0,n(X4)))),i(X4,X1))) | ~t(X0) | ~t(i(n(X1),X3)))))). tff(u577,axiom, (![X0] : ((t(i(n(X0),n(n(n(X0))))) | ~t(X0))))). tff(u576,axiom, ((~(![X1] : (t(i(X1,n(n(X1))))))) | (![X1] : (t(i(X1,n(n(X1)))))))). tff(u575,axiom, (![X0] : ((t(i(X0,n(n(X0)))) | ~t(n(X0)))))). tff(u574,axiom, (![X0] : ((t(n(n(n(X0)))) | ~t(X0) | ~t(n(X0)))))). tff(u573,axiom, ((~(![X1] : (t(i(X1,n(n(X1))))))) | (![X3] : ((t(n(n(X3))) | ~t(X3)))))). tff(u572,axiom, (![X0] : ((t(n(n(X0))) | ~t(n(X0)) | ~t(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]: 5756 % Time elapsed: 0.008 s % ------------------------------ % ------------------------------ % Success in time 208.843 s