% 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 C0CCOC12CC0CC231C42 % 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]: 6268 % Time elapsed: 0.800 s % ------------------------------ % ------------------------------ % fmb+10_1_av=off:bce=on:nm=6_1461 on C0CCOC12CC0CC231C42 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]: 83538 % 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 C0CCOC12CC0CC231C42 % 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]: 6396 % Time elapsed: 25.800 s % ------------------------------ % ------------------------------ % dis+1_3_av=off:cond=on:nm=64:newcnf=on:nwc=1_87 on C0CCOC12CC0CC231C42 % 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]: 106309 % 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 C0CCOC12CC0CC231C42 % 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]: 19317 % Time elapsed: 19.100 s % ------------------------------ % ------------------------------ % ott+2_5_afp=4000:afq=2.0:anc=none:bce=on:fsr=off:gsp=input_only:lma=on:nm=32:nwc=1:sp=reverse_arity_315 on C0CCOC12CC0CC231C42 % 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]: 7675 % Time elapsed: 41.100 s % ------------------------------ % ------------------------------ % fmb+10_1_av=off:bce=on:fmbes=smt:fmbsr=1.4:fde=none:ile=on:updr=off_600 on C0CCOC12CC0CC231C42 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]: 74071 % Time elapsed: 78.200 s % ------------------------------ % ------------------------------ % fmb+10_1_av=off:bce=on:fmbsr=1.3:nm=2:newcnf=on_1200 on C0CCOC12CC0CC231C42 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]: 81747 % Time elapsed: 156.200 s % ------------------------------ % ------------------------------ % fmb+10_1_av=off:fmbsr=1.1:updr=off_300 on C0CCOC12CC0CC231C42 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]: 48741 % Time elapsed: 39.200 s % ------------------------------ % ------------------------------ % fmb+10_1_av=off:fmbsr=1.6_1200 on C0CCOC12CC0CC231C42 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]: 82258 % Time elapsed: 156.200 s % ------------------------------ % ------------------------------ % fmb+10_1_av=off:fde=unused:ile=on:irw=on:lcm=predicate:lma=on:nm=16:nwc=1.7:sos=all:sp=reverse_arity_300 on C0CCOC12CC0CC231C42 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]: 48741 % Time elapsed: 39.200 s % ------------------------------ % ------------------------------ % fmb+10_1_av=off:fmbsr=1.5:updr=off_300 on C0CCOC12CC0CC231C42 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]: 48741 % Time elapsed: 39.200 s % ------------------------------ % ------------------------------ % lrs+11_6_aac=none:add=off:afp=100000:afq=1.1:amm=off:anc=none:bd=off:fsr=off:gs=on:gsem=off:nwc=1:sas=z3:sp=occurrence_300 on C0CCOC12CC0CC231C42 % SZS status CounterSatisfiable for C0CCOC12CC0CC231C42 % # SZS output start Saturation. tff(u43,axiom, (![X1, X0] : ((~t(i(X0,X1)) | t(X1) | ~t(X0))))). tff(u42,axiom, (![X1, X3, X5, X0, X2, X4, X6] : ((~t(i(X0,i(i(i(i(o,i(i(X2,X3),X4)),i(X5,X2)),X6),i(o,i(X4,X2))))) | t(i(X1,i(i(o,i(i(X2,X3),X4)),i(X5,X2)))) | ~t(X0))))). tff(u41,negated_conjecture, ((~~t(i(i(i(sK1,sK2),i(o,sK3)),i(sK4,i(i(sK3,sK1),i(sK5,i(sK0,sK1))))))) | ~t(i(i(i(sK1,sK2),i(o,sK3)),i(sK4,i(i(sK3,sK1),i(sK5,i(sK0,sK1)))))))). tff(u40,axiom, (![X1, X3, X5, X0, X2, X4, X6] : ((~t(i(i(o,i(i(i(X1,X2),X3),i(o,i(i(X2,X4),X5)))),i(X6,i(X1,X2)))) | t(i(X0,i(i(o,i(i(i(X1,X2),X3),i(o,i(i(X2,X4),X5)))),i(X6,i(X1,X2))))))))). tff(u39,axiom, (![X1, X3, X0, X2, X4] : ((~t(i(o,i(X3,X1))) | t(i(i(X0,i(i(X1,X2),X3)),i(X4,X1))) | ~t(X0))))). tff(u38,axiom, (![X1, X3, X5, X0, X2, X4] : ((~t(i(o,i(X5,i(X3,X1)))) | t(i(X0,i(i(o,i(i(X1,X2),X3)),i(X4,X1)))) | ~t(i(i(o,i(i(X1,X2),X3)),i(X4,X1))))))). tff(u37,axiom, ((~~t(o)) | ~t(o))). tff(u36,axiom, (![X1, X3, X0, X2, X4] : (t(i(X0,i(i(o,i(X1,X2)),i(i(X0,i(i(X2,X3),X1)),i(X4,X2)))))))). tff(u35,axiom, (![X1, X3, X0, X2, X4] : ((t(i(i(o,i(X0,X1)),i(i(X2,i(i(X1,X3),X0)),i(X4,X1)))) | ~t(X2))))). tff(u34,axiom, (![X1, X3, X5, X0, X2, X4, X6] : ((t(i(i(X0,i(i(i(i(o,i(i(X1,X2),X3)),i(X4,X1)),X5),i(o,i(X3,X1)))),i(X6,i(i(o,i(i(X1,X2),X3)),i(X4,X1))))) | ~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]: 5373 % Time elapsed: 0.035 s % ------------------------------ % ------------------------------ % Success in time 813.877 s