% 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 CCC01COC23C4CC30C20 % 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]: 18293 % Time elapsed: 0.800 s % ------------------------------ % ------------------------------ % fmb+10_1_av=off:bce=on:nm=6_1461 on CCC01COC23C4CC30C20 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]: 84817 % 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 CCC01COC23C4CC30C20 % SZS status CounterSatisfiable for CCC01COC23C4CC30C20 % # SZS output start Saturation. tff(u272,axiom, (![X1, X0] : ((~t(i(X0,X1)) | t(X1) | ~t(X0))))). tff(u271,axiom, ((~(![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2))))))) | (![X3, X2] : ((~t(i(X3,i(X2,X2))) | t(i(i(X2,X2),i(X2,X2)))))))). tff(u270,axiom, ((~(![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2))))))) | (~(![X9, X7, X8, X10] : (t(i(i(i(X7,X8),i(X9,o)),i(i(X10,X8),i(X9,o))))))) | (![X7, X6] : ((~t(i(X7,i(X6,o))) | t(i(i(X6,o),i(X6,o)))))))). tff(u269,axiom, ((~(![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2))))))) | (![X5, X7, X4, X6] : ((~t(i(X7,i(o,i(X4,X5)))) | t(i(i(o,i(X4,X5)),i(i(X5,X6),i(X4,X6))))))))). tff(u268,axiom, ((~(![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2))))))) | (![X11, X13, X12, X14] : ((~t(i(X14,i(i(X11,X12),X13))) | t(i(i(i(X11,X12),X13),i(i(X11,X12),X13)))))))). tff(u267,negated_conjecture, ~t(i(i(i(sK1,sK2),i(o,sK3)),i(sK4,i(i(sK3,sK1),i(sK5,i(sK0,sK1))))))). tff(u266,axiom, (![X1, X3, X0, X2, X4] : ((~t(i(i(X2,X4),i(o,i(X3,X1)))) | t(i(X0,i(i(X1,X2),i(X3,X2)))))))). tff(u265,axiom, ((~(![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2))))))) | (![X27, X29, X26, X28, X30] : ((~t(i(i(X30,o),i(o,i(X29,X27)))) | t(i(X26,i(i(X27,X28),i(X29,X28))))))))). tff(u264,axiom, ((~(![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2))))))) | (![X1, X3, X0, X2] : ((~t(i(i(X3,X1),i(X1,X2))) | t(i(i(X0,X1),i(X1,X2)))))))). tff(u263,axiom, ((~(![X9, X7, X8, X10] : (t(i(i(i(X7,X8),i(X9,o)),i(i(X10,X8),i(X9,o))))))) | (![X9, X11, X10, X12] : ((~t(i(i(X12,X10),i(X11,o))) | t(i(i(X9,X10),i(X11,o)))))))). tff(u262,axiom, ((~(![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2))))))) | (![X1, X3, X0, X2, X4] : ((~t(i(i(i(X4,X1),i(X1,X2)),X3)) | t(i(i(i(X0,X1),i(X1,X2)),X3))))))). tff(u261,axiom, ((~(![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2))))))) | (![X25, X27, X24, X26, X28] : ((~t(i(i(i(X28,X25),i(X26,o)),X27)) | t(i(i(i(X24,X25),i(X26,o)),X27))))))). tff(u260,axiom, ((~(![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2))))))) | (~(![X9, X7, X8, X10] : (t(i(i(i(X7,X8),i(X9,o)),i(i(X10,X8),i(X9,o))))))) | (![X1, X3, X0, X2] : ((~t(i(o,i(i(X1,X2),i(X3,X2)))) | t(i(i(X0,o),i(i(X1,X2),o)))))))). tff(u259,axiom, ((~(![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2))))))) | (![X32, X29, X31, X30] : ((~t(i(o,i(i(X29,X30),i(X32,X30)))) | t(i(i(i(X29,X30),X31),i(i(X29,X30),X31)))))))). tff(u258,axiom, ((~(![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2))))))) | (![X1, X3, X0, X2] : ((~t(i(o,i(i(X0,X1),i(X2,X1)))) | t(i(i(X3,i(X0,X1)),i(i(X0,X1),i(X0,X1))))))))). tff(u257,axiom, ((~(![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2))))))) | (![X9, X7, X8, X10] : ((~t(i(o,i(i(X7,X8),i(X9,X8)))) | t(i(i(X7,X8),X10)) | ~t(i(i(X9,X8),X10))))))). tff(u256,axiom, ((~(![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2))))))) | (![X9, X7, X8, X6] : ((t(i(i(i(X6,X7),X8),i(i(X9,X7),X8))) | ~t(i(o,i(i(X9,X7),i(X6,X7))))))))). tff(u255,axiom, ((~(![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2))))))) | (![X1, X3, X0, X2] : (t(i(i(i(i(X0,X1),i(X1,X2)),X3),i(i(i(X0,X1),i(X1,X2)),X3))))))). tff(u254,axiom, ((~(![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2))))))) | (![X5, X7, X4, X6] : (t(i(i(i(i(X4,X5),i(X6,o)),X7),i(i(i(X4,X5),i(X6,o)),X7))))))). tff(u253,axiom, ((~(![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2))))))) | (![X1, X3, X0, X2] : (t(i(i(X0,i(o,i(X1,X2))),i(i(o,i(X1,X2)),i(i(X2,X3),i(X1,X3))))))))). tff(u252,axiom, ((~(![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2))))))) | (![X1, X3, X0, X2, X4] : (t(i(i(i(X0,o),i(o,i(X1,X2))),i(X3,i(i(X2,X4),i(X1,X4))))))))). tff(u251,axiom, (![X1, X3, X0, X2, X4] : (t(i(i(i(X0,X1),i(o,i(X2,X3))),i(X4,i(i(X3,X0),i(X2,X0)))))))). tff(u250,axiom, ((~(![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2))))))) | (![X1, X0, X2] : (t(i(i(i(i(X0,X1),i(X2,X1)),i(i(X0,X1),i(X2,X1))),i(i(i(X0,X1),i(X2,X1)),i(i(X0,X1),i(X2,X1))))))))). tff(u249,axiom, (![X1, X3, X0, X2, X4] : (t(i(X0,i(i(i(X1,X2),i(X2,X3)),i(i(X4,X2),i(X2,X3)))))))). tff(u248,axiom, ((~(![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2))))))) | (![X1, X3, X0, X2, X4] : (t(i(X0,i(i(i(X1,X2),i(X3,o)),i(i(X4,X2),i(X3,o))))))))). tff(u247,axiom, ((~(![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2))))))) | (![X3, X5, X7, X4, X6] : (t(i(i(i(X3,X4),i(i(X5,X6),i(X7,X6))),i(i(X3,X4),i(i(X5,X6),i(X7,X6))))))))). tff(u246,axiom, ((~(![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2))))))) | (![X1, X3, X0, X2] : (t(i(i(o,i(i(X0,X1),i(X2,X1))),i(i(i(X2,X1),X3),i(i(X0,X1),X3)))))))). tff(u245,axiom, ((~(![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2))))))) | (![X1, X3, X0, X2] : (t(i(i(X0,i(i(X1,X2),X3)),i(i(i(X1,X2),X3),i(i(X1,X2),X3)))))))). tff(u244,axiom, ((~(![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2))))))) | (![X3, X5, X4] : (t(i(i(i(i(X3,X4),X5),i(i(X3,X4),X5)),i(i(i(X3,X4),X5),i(i(X3,X4),X5)))))))). tff(u243,axiom, ((~(![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2))))))) | (![X16, X18, X15, X17] : (t(i(i(i(i(X15,X16),X17),i(i(X18,X16),X17)),i(i(i(X15,X16),X17),i(i(X18,X16),X17)))))))). tff(u242,axiom, ((~(![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2))))))) | (![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2)))))))). tff(u241,axiom, ((~(![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2))))))) | (![X9, X10] : (t(i(i(X9,i(X10,X10)),i(i(X10,X10),i(X10,X10)))))))). tff(u240,axiom, ((~(![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2))))))) | (~(![X9, X7, X8, X10] : (t(i(i(i(X7,X8),i(X9,o)),i(i(X10,X8),i(X9,o))))))) | (![X1, X0] : (t(i(i(X0,i(X1,o)),i(i(X1,o),i(X1,o)))))))). tff(u239,axiom, ((~(![X9, X7, X8, X10] : (t(i(i(i(X7,X8),i(X9,o)),i(i(X10,X8),i(X9,o))))))) | (![X9, X7, X8, X10] : (t(i(i(i(X7,X8),i(X9,o)),i(i(X10,X8),i(X9,o)))))))). tff(u238,axiom, ((~(![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2))))))) | (~(![X9, X7, X8, X10] : (t(i(i(i(X7,X8),i(X9,o)),i(i(X10,X8),i(X9,o))))))) | (![X5, X7, X4, X6] : (t(i(i(X4,o),i(i(i(X5,X6),i(X6,X7)),o))))))). tff(u237,axiom, ((~(![X1, X3, X0, X2] : (t(i(i(i(X0,X1),i(X1,X2)),i(i(X3,X1),i(X1,X2))))))) | (~(![X9, X7, X8, X10] : (t(i(i(i(X7,X8),i(X9,o)),i(i(X10,X8),i(X9,o))))))) | (![X5, X7, X4, X6] : (t(i(i(X4,o),i(i(i(X5,X6),i(X7,o)),o))))))). tff(u236,axiom, ((~(![X11, X10, X12] : (t(i(i(i(X10,X11),i(X11,X12)),o))))) | (![X11, X10, X12] : (t(i(i(i(X10,X11),i(X11,X12)),o)))))). tff(u235,axiom, ((~(![X11, X10, X12] : (t(i(i(i(X10,X11),i(X12,o)),o))))) | (![X11, X10, X12] : (t(i(i(i(X10,X11),i(X12,o)),o)))))). tff(u234,axiom, ((~t(o)) | t(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]: 5500 % Time elapsed: 0.004 s % ------------------------------ % ------------------------------ % Success in time 197.97 s