%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP084-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:12:32 AM UTC 2026
% Result : Unsatisfiable 279.76s 40.40s
% Output : Refutation 279.86s
% Verified :
% SZS Type : Refutation
% Derivation depth : 63
% Number of leaves : 2
% Syntax : Number of formulae : 207 ( 202 unt; 0 def)
% Number of atoms : 219 ( 218 equ)
% Maximal formula atoms : 4 ( 1 avg)
% Number of connectives : 30 ( 18 ~; 12 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 12 ( 6 avg)
% Maximal term depth : 19 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 9 con; 0-2 aty)
% Number of variables : 966 ( 966 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(multiply(X4,inverse(X5)),inverse(X3))))))),X5) = X4,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,negated_conjecture,
( multiply(inverse(a1),a1) != multiply(inverse(b1),b1)
| multiply(multiply(inverse(b2),b2),a2) != a2
| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| multiply(a4,b4) != multiply(b4,a4) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_these_axioms) ).
fof(f3,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| a2 != multiply(multiply(inverse(b2),b2),a2)
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1)
| multiply(a4,b4) != multiply(b4,a4) ),
inference(reorient_equations,[],[f2]) ).
fof(f7,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(X5,X6)),multiply(X6,X5))),multiply(inverse(multiply(X7,X8)),multiply(X7,inverse(multiply(multiply(X0,inverse(inverse(X9))),inverse(X8))))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(X0,inverse(X4))))))),X9),
inference(superposition,[],[f1,f1]) ).
fof(f8,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X4,X3))),multiply(inverse(multiply(X5,X6)),multiply(X5,inverse(multiply(multiply(X0,inverse(inverse(multiply(multiply(X7,inverse(X8)),inverse(X9))))),inverse(X6))))))),X9)),X0))),X8) = X7,
inference(superposition,[],[f1,f1]) ).
fof(f44,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(X4,inverse(X3))))))),X5),inverse(X5)) = X4,
inference(superposition,[],[f1,f7]) ).
fof(f80,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(X5,X6)),multiply(X6,X5))),multiply(inverse(multiply(X7,X8)),multiply(X7,inverse(multiply(X0,inverse(X8))))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,inverse(X4))),multiply(X3,inverse(X0))))),X4),
inference(superposition,[],[f1,f44]) ).
fof(f90,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(X0),multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X4,X3))),multiply(inverse(multiply(X5,X6)),multiply(X5,inverse(multiply(X0,inverse(X6))))))),X7),inverse(multiply(multiply(X8,inverse(X9)),inverse(inverse(X7)))))))),X9) = X8,
inference(superposition,[],[f1,f44]) ).
fof(f156,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,inverse(multiply(X4,inverse(X5))))))),X3),X5) = X4,
inference(superposition,[],[f1,f80]) ).
fof(f158,plain,
! [X2,X3,X0,X1,X9,X4] : multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,inverse(X4))))),X3),X9),inverse(X9)) = X4,
inference(superposition,[],[f44,f80]) ).
fof(f234,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(X5,X6)),multiply(X6,X5))),multiply(inverse(multiply(X7,inverse(inverse(X8)))),multiply(X7,inverse(multiply(X0,inverse(inverse(X4)))))))) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(X0))))),X8),
inference(superposition,[],[f1,f156]) ).
fof(f355,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(X4))))),X5),inverse(X5)),inverse(X3)) = X4,
inference(superposition,[],[f156,f234]) ).
fof(f398,plain,
! [X2,X3,X0,X1,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(multiply(X2,inverse(inverse(X3)))),multiply(X2,inverse(multiply(multiply(multiply(X4,inverse(X3)),inverse(X5)),inverse(inverse(X5)))))))) = X4,
inference(superposition,[],[f1,f234]) ).
fof(f464,plain,
! [X2,X3,X10,X0,X1,X9] : inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,inverse(X0))),multiply(X3,inverse(multiply(multiply(multiply(X9,X0),inverse(X10)),inverse(inverse(X10)))))))) = X9,
inference(superposition,[],[f398,f398]) ).
fof(f476,plain,
! [X2,X3,X0,X1,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,inverse(inverse(X4)))),multiply(X3,inverse(multiply(multiply(multiply(X5,inverse(X4)),X0),inverse(X0))))))) = X5,
inference(superposition,[],[f398,f398]) ).
fof(f489,plain,
! [X0,X4,X5] : multiply(multiply(X0,inverse(X4)),inverse(inverse(X4))) = multiply(multiply(X0,X5),inverse(X5)),
inference(superposition,[],[f44,f398]) ).
fof(f490,plain,
! [X2,X3,X0,X1,X6,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(multiply(multiply(multiply(X0,inverse(X5)),inverse(inverse(X5))),inverse(inverse(X6))),inverse(X4))))))) = multiply(X0,X6),
inference(superposition,[],[f7,f398]) ).
fof(f492,plain,
! [X2,X3,X0,X1,X6,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,inverse(inverse(X4)))),multiply(X3,inverse(multiply(multiply(multiply(multiply(X0,inverse(X5)),inverse(X6)),inverse(inverse(X6))),inverse(inverse(inverse(inverse(X5)))))))))) = multiply(X0,X4),
inference(superposition,[],[f234,f398]) ).
fof(f494,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(X0,multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X4,X3))),inverse(multiply(multiply(X8,inverse(X9)),inverse(multiply(inverse(multiply(X5,inverse(inverse(X6)))),multiply(X5,inverse(multiply(multiply(multiply(X0,inverse(X6)),inverse(X7)),inverse(inverse(X7))))))))))))),X9) = X8,
inference(superposition,[],[f1,f398]) ).
fof(f531,plain,
! [X2,X3,X0,X1] : multiply(multiply(multiply(X0,inverse(X2)),X3),inverse(X3)) = multiply(multiply(multiply(X0,X1),inverse(X1)),inverse(inverse(inverse(X2)))),
inference(superposition,[],[f489,f489]) ).
fof(f539,plain,
! [X3,X0,X1] : multiply(multiply(X0,X1),inverse(X1)) = multiply(multiply(X0,X3),inverse(X3)),
inference(superposition,[],[f489,f489]) ).
fof(f566,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X7,X8)),multiply(X8,X7))),multiply(inverse(multiply(X9,X10)),multiply(X9,inverse(multiply(multiply(X0,inverse(X6)),inverse(X10))))))),X6) = inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(X4,X5)),multiply(X4,inverse(multiply(multiply(multiply(X0,X1),inverse(X1)),inverse(X5))))))),
inference(superposition,[],[f7,f489]) ).
fof(f567,plain,
! [X2,X3,X0,X1,X6,X4,X5] : multiply(X0,inverse(X6)) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(X4,X5)),multiply(X4,inverse(multiply(multiply(multiply(X0,X1),inverse(X1)),inverse(X5))))))),inverse(X6)),
inference(superposition,[],[f1,f489]) ).
fof(f658,plain,
! [X2,X3,X0,X1,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(X4,X5)),multiply(X4,inverse(multiply(multiply(multiply(X0,X1),inverse(X1)),inverse(X5))))))) = X0,
inference(forward_demodulation,[],[f566,f1]) ).
fof(f777,plain,
! [X2,X3,X0,X1] : multiply(multiply(multiply(X0,X2),X3),inverse(X3)) = multiply(multiply(multiply(X0,X1),inverse(X1)),inverse(inverse(X2))),
inference(superposition,[],[f489,f539]) ).
fof(f893,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : multiply(multiply(X0,inverse(X2)),X7) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X4,X3))),multiply(inverse(multiply(X5,X6)),multiply(X5,inverse(multiply(multiply(multiply(multiply(X0,X1),inverse(X1)),inverse(inverse(inverse(X2)))),inverse(X6))))))),X7),
inference(superposition,[],[f1,f531]) ).
fof(f2529,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] : multiply(multiply(multiply(X0,X3),inverse(X3)),inverse(X4)) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X5,X6)),multiply(X6,X5))),multiply(inverse(multiply(X7,X8)),multiply(X7,inverse(multiply(multiply(multiply(multiply(multiply(X0,X1),X2),inverse(X2)),inverse(inverse(inverse(X1)))),inverse(X8))))))),inverse(X4)),
inference(superposition,[],[f567,f777]) ).
fof(f2751,plain,
! [X3,X0,X1,X4] : multiply(multiply(multiply(X0,X3),inverse(X3)),inverse(X4)) = multiply(multiply(multiply(X0,X1),inverse(X1)),inverse(X4)),
inference(forward_demodulation,[],[f2529,f893]) ).
fof(f2874,plain,
! [X2,X0,X1,X8] : multiply(multiply(multiply(X1,X2),inverse(X2)),X0) = multiply(multiply(multiply(X1,X8),inverse(X8)),X0),
inference(superposition,[],[f2751,f398]) ).
fof(f13077,plain,
! [X3,X0,X8,X6,X7,X4,X5] : multiply(X0,inverse(X5)) = multiply(X0,multiply(inverse(multiply(X6,inverse(inverse(X7)))),multiply(X6,inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X4,X3))),inverse(X5))),inverse(X7)),inverse(X8)),inverse(inverse(X8))))))),
inference(superposition,[],[f156,f494]) ).
fof(f18153,plain,
! [X2,X3,X0,X1,X6,X4,X5] : multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(multiply(X0,X1),inverse(X1))),multiply(multiply(X0,X4),inverse(X5))))),X4),X6),inverse(X6)) = X5,
inference(superposition,[],[f158,f539]) ).
fof(f18154,plain,
! [X2,X3,X0,X1,X6,X4,X5] : multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(multiply(X0,inverse(X1)),inverse(inverse(X1)))),multiply(multiply(X0,X4),inverse(X5))))),X4),X6),inverse(X6)) = X5,
inference(superposition,[],[f158,f489]) ).
fof(f21993,plain,
! [X10,X0,X11,X1,X8,X9,X7] : multiply(X1,X0) = multiply(X1,multiply(inverse(multiply(X7,inverse(inverse(X8)))),multiply(X7,inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X9,X10)),multiply(X10,X9))),X0)),inverse(X8)),inverse(X11)),inverse(inverse(X11))))))),
inference(superposition,[],[f13077,f476]) ).
fof(f22331,plain,
! [X2,X0,X1,X6,X5] : inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),inverse(X2))) = inverse(multiply(inverse(multiply(inverse(multiply(X5,X6)),multiply(X6,X5))),inverse(X2))),
inference(superposition,[],[f658,f13077]) ).
fof(f23014,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] : inverse(multiply(inverse(multiply(X7,X8)),multiply(X8,X7))) = multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X4,X3))),multiply(inverse(multiply(X5,inverse(X6))),multiply(X5,inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),inverse(X2))))))),X6),X2),
inference(superposition,[],[f156,f22331]) ).
fof(f23164,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] : multiply(inverse(multiply(inverse(multiply(X7,X8)),multiply(X8,X7))),inverse(X2)) = multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X4,X3))),multiply(inverse(multiply(X5,X6)),multiply(X5,inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),inverse(X2))))))),X9),inverse(X9)),inverse(X6)),
inference(superposition,[],[f355,f22331]) ).
fof(f23258,plain,
! [X2,X0,X1,X8,X7] : multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),inverse(X2)) = multiply(inverse(multiply(inverse(multiply(X7,X8)),multiply(X8,X7))),inverse(X2)),
inference(forward_demodulation,[],[f23164,f355]) ).
fof(f23260,plain,
! [X0,X1,X8,X7] : inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))) = inverse(multiply(inverse(multiply(X7,X8)),multiply(X8,X7))),
inference(forward_demodulation,[],[f23014,f156]) ).
fof(f23508,plain,
! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))) = inverse(multiply(inverse(multiply(inverse(X4),multiply(X0,X4))),multiply(multiply(X0,X1),inverse(X1)))),
inference(superposition,[],[f23260,f539]) ).
fof(f23997,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] : multiply(inverse(multiply(X6,X7)),multiply(X7,X6)) = multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(X4,X5)),multiply(X4,inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))))))),X8),inverse(X8)),inverse(X5)),
inference(superposition,[],[f355,f23260]) ).
fof(f24092,plain,
! [X0,X1,X6,X7] : multiply(inverse(multiply(X0,X1)),multiply(X1,X0)) = multiply(inverse(multiply(X6,X7)),multiply(X7,X6)),
inference(forward_demodulation,[],[f23997,f355]) ).
fof(f24273,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X2,X3)),multiply(X3,X2)) = multiply(inverse(multiply(multiply(X0,inverse(X1)),inverse(inverse(X1)))),multiply(inverse(X4),multiply(X0,X4))),
inference(superposition,[],[f24092,f489]) ).
fof(f24312,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(X2,X3)),multiply(X3,X2)) = multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(multiply(X5,X4),inverse(multiply(X4,X5)))),
inference(superposition,[],[f24092,f23260]) ).
fof(f24346,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X2,X3)),multiply(X3,X2)) = multiply(inverse(multiply(inverse(X4),multiply(X0,X4))),multiply(multiply(X0,X1),inverse(X1))),
inference(superposition,[],[f24092,f539]) ).
fof(f24347,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X2,X3)),multiply(X3,X2)) = multiply(inverse(multiply(inverse(X4),multiply(X0,X4))),multiply(multiply(X0,inverse(X1)),inverse(inverse(X1)))),
inference(superposition,[],[f24092,f489]) ).
fof(f24793,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : inverse(multiply(X6,X7)) = inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(X4,X5)),multiply(X4,inverse(multiply(multiply(multiply(inverse(multiply(X0,X1)),multiply(X1,X0)),inverse(multiply(X7,X6))),inverse(X5))))))),
inference(superposition,[],[f658,f24092]) ).
fof(f25568,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] : inverse(multiply(inverse(X6),multiply(X7,X6))) = inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(X4,X5)),multiply(X4,inverse(multiply(multiply(multiply(inverse(multiply(X0,X1)),multiply(X1,X0)),inverse(multiply(multiply(X7,inverse(X8)),inverse(inverse(X8))))),inverse(X5))))))),
inference(superposition,[],[f658,f24347]) ).
fof(f25610,plain,
! [X8,X6,X7] : inverse(multiply(inverse(X6),multiply(X7,X6))) = inverse(multiply(inverse(inverse(X8)),multiply(X7,inverse(X8)))),
inference(forward_demodulation,[],[f25568,f24793]) ).
fof(f25777,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(X2),multiply(multiply(X0,X3),X2))) = inverse(multiply(inverse(inverse(X3)),multiply(multiply(X0,X1),inverse(X1)))),
inference(superposition,[],[f25610,f539]) ).
fof(f26189,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : multiply(inverse(inverse(X6)),multiply(X1,inverse(X6))) = multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(X4,X5)),multiply(X4,inverse(multiply(inverse(X0),multiply(X1,X0))))))),X7),inverse(X7)),inverse(X5)),
inference(superposition,[],[f355,f25610]) ).
fof(f26286,plain,
! [X0,X1,X6] : multiply(inverse(X0),multiply(X1,X0)) = multiply(inverse(inverse(X6)),multiply(X1,inverse(X6))),
inference(forward_demodulation,[],[f26189,f355]) ).
fof(f26424,plain,
! [X2,X3,X0,X1] : multiply(inverse(X2),multiply(multiply(X0,X3),X2)) = multiply(inverse(inverse(X3)),multiply(multiply(X0,X1),inverse(X1))),
inference(superposition,[],[f26286,f539]) ).
fof(f26450,plain,
! [X2,X0,X1] : multiply(inverse(X0),multiply(X1,X0)) = multiply(inverse(X2),multiply(X1,X2)),
inference(superposition,[],[f26286,f26286]) ).
fof(f28199,plain,
! [X2,X0,X1,X4] : multiply(inverse(inverse(X0)),multiply(multiply(X1,X2),inverse(X2))) = multiply(inverse(inverse(X0)),multiply(multiply(X1,X4),inverse(X4))),
inference(superposition,[],[f26424,f26424]) ).
fof(f35978,plain,
! [X2,X0,X1,X8,X9] : multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),X0) = multiply(inverse(multiply(inverse(multiply(X8,X9)),multiply(X9,X8))),X0),
inference(superposition,[],[f23258,f476]) ).
fof(f40229,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] : inverse(multiply(multiply(X6,inverse(X7)),inverse(inverse(X7)))) = inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(X4,X5)),multiply(X4,inverse(multiply(multiply(multiply(inverse(multiply(X0,X1)),multiply(X1,X0)),inverse(multiply(inverse(X8),multiply(X6,X8)))),inverse(X5))))))),
inference(superposition,[],[f658,f24273]) ).
fof(f40308,plain,
! [X8,X6,X7] : inverse(multiply(multiply(X6,inverse(X7)),inverse(inverse(X7)))) = inverse(multiply(multiply(X6,X8),inverse(X8))),
inference(forward_demodulation,[],[f40229,f24793]) ).
fof(f41224,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(X2,X4),inverse(X4)) = multiply(multiply(X2,multiply(multiply(X0,X3),inverse(X3))),inverse(multiply(multiply(X0,inverse(X1)),inverse(inverse(X1))))),
inference(superposition,[],[f539,f40308]) ).
fof(f69830,plain,
! [X0,X8,X6,X7] : multiply(inverse(X0),multiply(multiply(X6,X7),inverse(X7))) = multiply(inverse(X0),multiply(multiply(X6,X8),inverse(X8))),
inference(superposition,[],[f28199,f476]) ).
fof(f70964,plain,
! [X0,X8,X6,X7] : multiply(X0,multiply(multiply(X6,X7),inverse(X7))) = multiply(X0,multiply(multiply(X6,X8),inverse(X8))),
inference(superposition,[],[f69830,f476]) ).
fof(f72683,plain,
! [X2,X3,X0,X1,X4] : multiply(X3,multiply(multiply(multiply(X0,X2),X4),inverse(X4))) = multiply(X3,multiply(multiply(multiply(X0,X1),inverse(X1)),inverse(inverse(X2)))),
inference(superposition,[],[f70964,f2874]) ).
fof(f82547,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] : multiply(X8,multiply(inverse(multiply(X6,X7)),multiply(X7,X6))) = inverse(multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X4,X3))),multiply(inverse(multiply(X5,inverse(inverse(multiply(inverse(multiply(inverse(X0),multiply(X1,X0))),multiply(multiply(X1,X2),inverse(X2))))))),multiply(X5,inverse(multiply(multiply(multiply(multiply(X8,inverse(X9)),inverse(X10)),inverse(inverse(X10))),inverse(inverse(inverse(inverse(X9)))))))))),
inference(superposition,[],[f492,f23508]) ).
fof(f82808,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : multiply(multiply(X0,X7),X6) = inverse(multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X4,X3))),multiply(inverse(multiply(X5,inverse(inverse(X6)))),multiply(X5,inverse(multiply(multiply(multiply(multiply(multiply(X0,X1),inverse(X1)),inverse(X2)),inverse(inverse(X2))),inverse(inverse(inverse(inverse(X7)))))))))),
inference(superposition,[],[f492,f2874]) ).
fof(f83505,plain,
! [X2,X0,X1,X8,X6,X7] : multiply(X8,multiply(inverse(multiply(X6,X7)),multiply(X7,X6))) = multiply(X8,multiply(inverse(multiply(inverse(X0),multiply(X1,X0))),multiply(multiply(X1,X2),inverse(X2)))),
inference(forward_demodulation,[],[f82547,f492]) ).
fof(f167675,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] : multiply(X0,inverse(multiply(multiply(X5,inverse(X8)),inverse(inverse(X8))))) = multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,inverse(X4))),multiply(X3,inverse(multiply(X0,inverse(multiply(multiply(X5,X6),inverse(X6))))))))),X4),X7),inverse(X7)),
inference(superposition,[],[f41224,f156]) ).
fof(f168913,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X6,X7)),multiply(X7,X6))),multiply(inverse(X4),multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(multiply(X2,X3)),multiply(X2,inverse(multiply(X4,inverse(X3))))))),X5),inverse(X5))))),multiply(multiply(X8,X9),inverse(X9))) = X8,
inference(superposition,[],[f90,f41224]) ).
fof(f169524,plain,
! [X8,X6,X9,X7,X4] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X6,X7)),multiply(X7,X6))),multiply(inverse(X4),X4))),multiply(multiply(X8,X9),inverse(X9))) = X8,
inference(forward_demodulation,[],[f168913,f44]) ).
fof(f169572,plain,
! [X0,X8,X6,X5] : multiply(X0,inverse(multiply(multiply(X5,X6),inverse(X6)))) = multiply(X0,inverse(multiply(multiply(X5,inverse(X8)),inverse(inverse(X8))))),
inference(forward_demodulation,[],[f167675,f158]) ).
fof(f170506,plain,
! [X2,X3,X0,X1] : multiply(X0,inverse(multiply(multiply(X1,X2),inverse(X2)))) = multiply(X0,inverse(multiply(multiply(X1,X3),inverse(X3)))),
inference(superposition,[],[f169572,f169572]) ).
fof(f178486,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))) = multiply(inverse(multiply(X2,X3)),multiply(X3,X2)),
inference(superposition,[],[f24092,f169524]) ).
fof(f178491,plain,
! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))) = multiply(inverse(multiply(inverse(X2),multiply(X3,X2))),multiply(multiply(X3,X4),inverse(X4))),
inference(superposition,[],[f24346,f169524]) ).
fof(f178525,plain,
! [X0,X4,X5] : multiply(multiply(X0,inverse(multiply(multiply(X0,X5),inverse(X5)))),inverse(inverse(X4))) = X4,
inference(superposition,[],[f355,f169524]) ).
fof(f179369,plain,
! [X2,X3,X0,X1] : multiply(multiply(multiply(X0,X2),inverse(multiply(multiply(multiply(X0,X1),inverse(X1)),inverse(inverse(X2))))),inverse(inverse(X3))) = X3,
inference(superposition,[],[f178525,f2874]) ).
fof(f179767,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X4,X3))),multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X5,X6)),multiply(X6,X5))),multiply(inverse(multiply(X7,X8)),multiply(X7,inverse(multiply(multiply(multiply(X0,inverse(X1)),inverse(X2)),inverse(X8))))))),X2)),multiply(X9,inverse(multiply(multiply(X9,X10),inverse(X10))))))),X1) = X0,
inference(superposition,[],[f8,f178525]) ).
fof(f179810,plain,
! [X2,X3,X0,X1,X6,X4,X5] : inverse(X0) = multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(multiply(X3,inverse(multiply(multiply(X3,X4),inverse(X4)))),X5)),X0))),X6),inverse(X6)),inverse(X5)),
inference(superposition,[],[f355,f178525]) ).
fof(f179981,plain,
! [X2,X3,X0,X1] : multiply(X0,inverse(inverse(inverse(X0)))) = multiply(multiply(multiply(X1,inverse(multiply(multiply(X1,X2),inverse(X2)))),X3),inverse(X3)),
inference(superposition,[],[f539,f178525]) ).
fof(f180264,plain,
! [X3,X10,X0,X1,X9,X4] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X4,X3))),multiply(inverse(multiply(X0,inverse(X1))),multiply(X9,inverse(multiply(multiply(X9,X10),inverse(X10))))))),X1) = X0,
inference(forward_demodulation,[],[f179767,f1]) ).
fof(f181404,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(inverse(multiply(X0,X1)),multiply(X1,X0)),X4) = multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),X4),
inference(superposition,[],[f35978,f178486]) ).
fof(f210552,plain,
! [X0,X1] : multiply(X0,inverse(inverse(inverse(X0)))) = multiply(X1,inverse(inverse(inverse(X1)))),
inference(superposition,[],[f179981,f179981]) ).
fof(f211218,plain,
! [X2,X3,X0,X1,X8,X6,X9,X7,X4,X5] : multiply(multiply(X3,inverse(multiply(multiply(X3,X4),inverse(X4)))),X5) = multiply(inverse(multiply(inverse(multiply(inverse(multiply(X6,X7)),multiply(X7,X6))),multiply(inverse(multiply(X8,X9)),multiply(X8,inverse(multiply(multiply(multiply(multiply(X0,inverse(multiply(multiply(X0,X1),inverse(X1)))),X2),inverse(X2)),inverse(X9))))))),X5),
inference(superposition,[],[f893,f179981]) ).
fof(f212209,plain,
! [X3,X0,X1,X4,X5] : multiply(multiply(X3,inverse(multiply(multiply(X3,X4),inverse(X4)))),X5) = multiply(multiply(X0,inverse(multiply(multiply(X0,X1),inverse(X1)))),X5),
inference(forward_demodulation,[],[f211218,f658]) ).
fof(f213560,plain,
! [X2,X0,X1] : multiply(multiply(X1,X2),inverse(X2)) = multiply(multiply(X0,inverse(inverse(inverse(X0)))),inverse(inverse(inverse(inverse(X1))))),
inference(superposition,[],[f539,f210552]) ).
fof(f213712,plain,
! [X2,X0,X1] : multiply(inverse(X1),multiply(X2,X1)) = multiply(inverse(inverse(inverse(inverse(X2)))),multiply(X0,inverse(inverse(inverse(X0))))),
inference(superposition,[],[f26450,f210552]) ).
fof(f215859,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : multiply(multiply(X6,inverse(inverse(inverse(X6)))),X5) = inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(X4,inverse(inverse(X5)))),multiply(X4,inverse(multiply(multiply(multiply(multiply(multiply(X0,X1),inverse(X1)),inverse(X7)),inverse(inverse(X7))),inverse(inverse(inverse(inverse(inverse(inverse(inverse(X0))))))))))))),
inference(superposition,[],[f492,f213560]) ).
fof(f216367,plain,
! [X0,X6,X5] : multiply(multiply(X0,inverse(inverse(inverse(X0)))),X5) = multiply(multiply(X6,inverse(inverse(inverse(X6)))),X5),
inference(forward_demodulation,[],[f215859,f82808]) ).
fof(f225779,plain,
! [X2,X3,X0,X1,X8,X6,X7,X4,X5] : multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X4,X3))),multiply(inverse(multiply(multiply(X5,inverse(multiply(multiply(X5,X6),inverse(X6)))),X7)),multiply(multiply(X0,inverse(multiply(multiply(X0,X1),inverse(X1)))),inverse(X2))))),X8),inverse(X8)),inverse(X7)) = X2,
inference(superposition,[],[f355,f212209]) ).
fof(f226034,plain,
! [X2,X0,X1] : inverse(multiply(multiply(X0,inverse(multiply(multiply(X0,X1),inverse(X1)))),inverse(X2))) = X2,
inference(forward_demodulation,[],[f225779,f179810]) ).
fof(f226897,plain,
! [X2,X3,X0,X1] : inverse(multiply(multiply(multiply(X0,X2),inverse(multiply(multiply(multiply(X0,X1),inverse(X1)),inverse(inverse(X2))))),inverse(X3))) = X3,
inference(superposition,[],[f226034,f2874]) ).
fof(f227509,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(X1,X4),inverse(X4)) = multiply(multiply(X1,multiply(multiply(X2,inverse(multiply(multiply(X2,X3),inverse(X3)))),inverse(X0))),X0),
inference(superposition,[],[f539,f226034]) ).
fof(f229987,plain,
! [X2,X3,X0,X1,X4,X5] : inverse(multiply(inverse(inverse(multiply(multiply(X3,inverse(multiply(multiply(X3,X4),inverse(X4)))),inverse(X2)))),multiply(multiply(X0,X5),inverse(X5)))) = inverse(multiply(inverse(X2),multiply(multiply(X0,X1),inverse(X1)))),
inference(superposition,[],[f25777,f227509]) ).
fof(f230877,plain,
! [X2,X0,X1,X5] : inverse(multiply(inverse(X2),multiply(multiply(X0,X5),inverse(X5)))) = inverse(multiply(inverse(X2),multiply(multiply(X0,X1),inverse(X1)))),
inference(forward_demodulation,[],[f229987,f226034]) ).
fof(f249623,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(multiply(multiply(X3,inverse(multiply(multiply(X3,X4),inverse(X4)))),inverse(X5)),inverse(inverse(X5)))),multiply(X0,inverse(inverse(inverse(X0))))))),X6),X7),inverse(X7)) = X6,
inference(superposition,[],[f18154,f179981]) ).
fof(f249654,plain,
! [X2,X3,X10,X0,X1,X8,X6,X9,X7,X4,X5] : multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X4,X3))),multiply(inverse(multiply(multiply(X5,inverse(X6)),inverse(inverse(X6)))),multiply(multiply(X5,X7),inverse(X0))))),X7),inverse(X8)),inverse(inverse(X8)))),X0))),X9),X10),inverse(X10)) = X9,
inference(superposition,[],[f18154,f18154]) ).
fof(f249688,plain,
! [X2,X3,X0,X1,X6,X4,X5] : inverse(inverse(multiply(X3,X5))) = multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(multiply(X3,inverse(X4)),inverse(inverse(X4)))),multiply(X0,inverse(inverse(inverse(X0))))))),X5),X6),inverse(X6)),
inference(superposition,[],[f18154,f210552]) ).
fof(f250997,plain,
! [X2,X10,X0,X1,X9] : multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(X0),X0))),X9),X10),inverse(X10)) = X9,
inference(forward_demodulation,[],[f249654,f18153]) ).
fof(f250999,plain,
! [X3,X6,X4] : inverse(inverse(multiply(multiply(X3,inverse(multiply(multiply(X3,X4),inverse(X4)))),X6))) = X6,
inference(forward_demodulation,[],[f249623,f249688]) ).
fof(f279075,plain,
! [X2,X3,X0,X1,X4] : multiply(X1,multiply(inverse(multiply(X2,inverse(inverse(X3)))),multiply(X2,inverse(X0)))) = multiply(X1,multiply(inverse(multiply(X4,inverse(inverse(X3)))),multiply(X4,inverse(X0)))),
inference(superposition,[],[f21993,f158]) ).
fof(f287867,plain,
! [X2,X3,X0,X1,X6,X4,X5] : multiply(X1,multiply(inverse(multiply(X2,inverse(inverse(X3)))),multiply(X2,inverse(inverse(X0))))) = multiply(X1,multiply(inverse(multiply(multiply(multiply(X4,X5),inverse(multiply(multiply(multiply(X4,X6),inverse(X6)),inverse(inverse(X5))))),inverse(inverse(X3)))),X0)),
inference(superposition,[],[f279075,f179369]) ).
fof(f289922,plain,
! [X2,X3,X0,X1] : multiply(X1,multiply(inverse(X3),X0)) = multiply(X1,multiply(inverse(multiply(X2,inverse(inverse(X3)))),multiply(X2,inverse(inverse(X0))))),
inference(forward_demodulation,[],[f287867,f226897]) ).
fof(f291307,plain,
! [X2,X3,X0,X1,X6,X4,X5] : multiply(inverse(multiply(X5,inverse(inverse(X3)))),multiply(X5,inverse(inverse(X4)))) = multiply(multiply(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(inverse(X2),X2))),multiply(inverse(X3),X4)),X6),inverse(X6)),
inference(superposition,[],[f250997,f289922]) ).
fof(f291446,plain,
! [X3,X4,X5] : multiply(inverse(X3),X4) = multiply(inverse(multiply(X5,inverse(inverse(X3)))),multiply(X5,inverse(inverse(X4)))),
inference(forward_demodulation,[],[f291307,f250997]) ).
fof(f292214,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X1,X2)),multiply(X2,X1)) = multiply(inverse(X0),X0),
inference(superposition,[],[f24092,f291446]) ).
fof(f293766,plain,
! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(X1),X1),
inference(superposition,[],[f291446,f292214]) ).
fof(f296691,plain,
! [X2,X0,X1] : multiply(multiply(inverse(multiply(inverse(X0),X0)),multiply(X1,inverse(X2))),X2) = X1,
inference(superposition,[],[f156,f293766]) ).
fof(f297669,plain,
! [X2,X0,X1,X4,X5] : multiply(multiply(multiply(inverse(multiply(inverse(X0),multiply(X1,X0))),multiply(multiply(X1,X2),inverse(X2))),multiply(X4,inverse(X5))),X5) = X4,
inference(superposition,[],[f296691,f178491]) ).
fof(f297931,plain,
! [X3,X0,X1,X4] : multiply(X3,X4) = multiply(multiply(inverse(multiply(X0,X1)),multiply(X1,X0)),multiply(X4,X3)),
inference(superposition,[],[f296691,f24312]) ).
fof(f297942,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X1,X0))),multiply(multiply(X2,X3),inverse(multiply(X3,X2)))),X4) = X4,
inference(superposition,[],[f296691,f24312]) ).
fof(f297943,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(inverse(X0),multiply(X1,X0))),multiply(multiply(X1,X2),inverse(X2))),X3) = X3,
inference(superposition,[],[f296691,f24346]) ).
fof(f297948,plain,
! [X0,X1] : multiply(multiply(inverse(X0),X0),X1) = X1,
inference(superposition,[],[f296691,f292214]) ).
fof(f297953,plain,
! [X0,X1] : inverse(inverse(X1)) = multiply(multiply(inverse(X0),X0),X1),
inference(superposition,[],[f296691,f293766]) ).
fof(f297954,plain,
! [X2,X0,X1] : inverse(inverse(X2)) = multiply(multiply(inverse(multiply(X0,X1)),multiply(X1,X0)),X2),
inference(superposition,[],[f296691,f292214]) ).
fof(f298018,plain,
! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),X0) = X0,
inference(superposition,[],[f181404,f296691]) ).
fof(f298881,plain,
! [X2,X3,X4] : multiply(multiply(multiply(X2,X3),inverse(multiply(X3,X2))),X4) = X4,
inference(forward_demodulation,[],[f297942,f298018]) ).
fof(f298883,plain,
! [X3,X4] : multiply(X3,X4) = inverse(inverse(multiply(X4,X3))),
inference(forward_demodulation,[],[f297931,f297954]) ).
fof(f299045,plain,
! [X4,X5] : multiply(multiply(X4,inverse(X5)),X5) = X4,
inference(forward_demodulation,[],[f297669,f297943]) ).
fof(f299148,plain,
! [X2,X3,X0,X1,X4,X5] : inverse(inverse(X0)) = multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(X0,inverse(X1))),multiply(X4,inverse(multiply(multiply(X4,X5),inverse(X5)))))))),
inference(superposition,[],[f298883,f180264]) ).
fof(f299468,plain,
! [X2,X0,X1] : multiply(X0,multiply(X1,inverse(multiply(multiply(X1,X2),inverse(X2))))) = X0,
inference(superposition,[],[f250999,f298883]) ).
fof(f299490,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : multiply(X6,X5) = inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(X4,inverse(inverse(X5)))),multiply(X4,inverse(multiply(multiply(multiply(multiply(X6,inverse(multiply(X1,X0))),inverse(X7)),inverse(inverse(X7))),inverse(inverse(multiply(X0,X1))))))))),
inference(superposition,[],[f492,f298883]) ).
fof(f299570,plain,
! [X2,X3,X0,X1] : multiply(multiply(X2,X3),inverse(X3)) = multiply(multiply(multiply(X1,X0),inverse(multiply(X0,X1))),inverse(inverse(inverse(inverse(X2))))),
inference(superposition,[],[f213560,f298883]) ).
fof(f299580,plain,
! [X2,X3,X0,X1] : multiply(multiply(X2,inverse(inverse(inverse(X2)))),X3) = multiply(multiply(multiply(X1,X0),inverse(multiply(X0,X1))),X3),
inference(superposition,[],[f216367,f298883]) ).
fof(f300007,plain,
! [X2,X3,X0,X1] : multiply(multiply(X2,inverse(inverse(inverse(X2)))),X3) = multiply(multiply(inverse(multiply(X1,X0)),inverse(inverse(multiply(X0,X1)))),X3),
inference(superposition,[],[f216367,f298883]) ).
fof(f300038,plain,
! [X2,X3,X0,X1] : multiply(inverse(X2),inverse(multiply(X1,X0))) = multiply(inverse(multiply(X3,inverse(inverse(X2)))),multiply(X3,inverse(multiply(X0,X1)))),
inference(superposition,[],[f291446,f298883]) ).
fof(f300049,plain,
! [X2,X3,X0,X1] : multiply(multiply(X2,inverse(inverse(inverse(X2)))),X3) = multiply(multiply(inverse(multiply(X1,X0)),multiply(X1,X0)),X3),
inference(forward_demodulation,[],[f300007,f298883]) ).
fof(f300187,plain,
! [X2,X3] : multiply(multiply(X2,inverse(inverse(inverse(X2)))),X3) = X3,
inference(forward_demodulation,[],[f299580,f298881]) ).
fof(f300195,plain,
! [X2,X3] : multiply(multiply(X2,X3),inverse(X3)) = inverse(inverse(inverse(inverse(X2)))),
inference(forward_demodulation,[],[f299570,f298881]) ).
fof(f300215,plain,
! [X0,X1,X6,X7,X4,X5] : multiply(X6,X5) = inverse(multiply(inverse(multiply(X4,inverse(inverse(X5)))),multiply(X4,inverse(multiply(multiply(multiply(multiply(X6,inverse(multiply(X1,X0))),inverse(X7)),inverse(inverse(X7))),inverse(inverse(multiply(X0,X1)))))))),
inference(forward_demodulation,[],[f299490,f298018]) ).
fof(f300529,plain,
! [X0,X1,X4,X5] : inverse(inverse(X0)) = multiply(X1,inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X4,inverse(multiply(multiply(X4,X5),inverse(X5))))))),
inference(forward_demodulation,[],[f299148,f298018]) ).
fof(f300541,plain,
! [X2,X3] : inverse(inverse(X3)) = multiply(multiply(X2,inverse(inverse(inverse(X2)))),X3),
inference(forward_demodulation,[],[f300049,f297953]) ).
fof(f300603,plain,
! [X0,X1,X6,X7,X5] : multiply(X6,X5) = inverse(multiply(inverse(X5),inverse(multiply(inverse(inverse(multiply(X0,X1))),multiply(multiply(multiply(X6,inverse(multiply(X1,X0))),inverse(X7)),inverse(inverse(X7))))))),
inference(forward_demodulation,[],[f300215,f300038]) ).
fof(f300665,plain,
! [X0,X1] : inverse(inverse(X0)) = multiply(X1,inverse(inverse(multiply(X0,inverse(X1))))),
inference(forward_demodulation,[],[f300529,f299468]) ).
fof(f300671,plain,
! [X3] : inverse(inverse(X3)) = X3,
inference(forward_demodulation,[],[f300541,f300187]) ).
fof(f300696,plain,
! [X0,X1,X6,X5] : multiply(X6,X5) = inverse(multiply(inverse(X5),inverse(multiply(inverse(inverse(multiply(X0,X1))),inverse(inverse(inverse(inverse(multiply(X6,inverse(multiply(X1,X0))))))))))),
inference(forward_demodulation,[],[f300603,f300195]) ).
fof(f300713,plain,
! [X0,X1] : inverse(inverse(X0)) = multiply(X1,multiply(inverse(X1),X0)),
inference(forward_demodulation,[],[f300665,f298883]) ).
fof(f300725,plain,
! [X0,X1,X6,X5] : multiply(X6,X5) = inverse(multiply(inverse(X5),inverse(multiply(inverse(inverse(multiply(X0,X1))),inverse(inverse(multiply(X6,inverse(multiply(X1,X0))))))))),
inference(forward_demodulation,[],[f300696,f300671]) ).
fof(f300741,plain,
! [X0,X1] : multiply(X1,multiply(inverse(X1),X0)) = X0,
inference(forward_demodulation,[],[f300713,f300671]) ).
fof(f300747,plain,
! [X0,X1,X6,X5] : multiply(X6,X5) = inverse(multiply(inverse(X5),inverse(multiply(inverse(inverse(multiply(X0,X1))),multiply(inverse(multiply(X1,X0)),X6))))),
inference(forward_demodulation,[],[f300725,f298883]) ).
fof(f300763,plain,
! [X0,X1,X6,X5] : multiply(X6,X5) = inverse(multiply(inverse(X5),inverse(multiply(multiply(X1,X0),multiply(inverse(multiply(X1,X0)),X6))))),
inference(forward_demodulation,[],[f300747,f298883]) ).
fof(f300771,plain,
! [X6,X5] : multiply(X6,X5) = inverse(multiply(inverse(X5),inverse(X6))),
inference(forward_demodulation,[],[f300763,f300741]) ).
fof(f300777,plain,
! [X2,X3,X0,X1,X6,X4,X5] : inverse(multiply(X0,X1)) = multiply(inverse(multiply(inverse(multiply(X2,X3)),multiply(X3,X2))),multiply(inverse(multiply(X4,X5)),multiply(X4,inverse(multiply(multiply(multiply(multiply(X0,inverse(X6)),inverse(inverse(X6))),inverse(inverse(X1))),inverse(X5)))))),
inference(superposition,[],[f300671,f490]) ).
fof(f300783,plain,
! [X2,X3,X0,X1,X4,X5] : inverse(X0) = multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,inverse(X4))),multiply(X3,inverse(multiply(multiply(multiply(X0,X4),inverse(X5)),inverse(inverse(X5))))))),
inference(superposition,[],[f300671,f464]) ).
fof(f300785,plain,
! [X2,X3,X0,X1,X4,X5] : inverse(X0) = multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(X3,inverse(inverse(X4)))),multiply(X3,inverse(multiply(multiply(multiply(X0,inverse(X4)),X5),inverse(X5)))))),
inference(superposition,[],[f300671,f476]) ).
fof(f300827,plain,
! [X0,X1] : inverse(multiply(X0,X1)) = inverse(multiply(X1,X0)),
inference(superposition,[],[f300671,f298883]) ).
fof(f300941,plain,
! [X2,X0,X1] : multiply(inverse(X1),X0) = multiply(inverse(multiply(X2,inverse(inverse(X1)))),multiply(X2,X0)),
inference(superposition,[],[f291446,f300671]) ).
fof(f300963,plain,
! [X2,X0,X1] : multiply(inverse(X1),multiply(X0,X1)) = multiply(inverse(inverse(X0)),multiply(X2,inverse(inverse(inverse(X2))))),
inference(superposition,[],[f213712,f300671]) ).
fof(f300978,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X1,X0),
inference(superposition,[],[f298883,f300671]) ).
fof(f301080,plain,
! [X2,X0,X1] : multiply(multiply(X1,X2),inverse(X2)) = multiply(multiply(X1,inverse(X0)),X0),
inference(superposition,[],[f539,f300671]) ).
fof(f301300,plain,
! [X2,X3,X0,X1,X4] : multiply(X1,multiply(multiply(multiply(X2,X3),X4),inverse(X4))) = multiply(X1,multiply(multiply(multiply(X2,inverse(X0)),X0),inverse(inverse(X3)))),
inference(superposition,[],[f72683,f300671]) ).
fof(f301317,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(X1,multiply(inverse(multiply(X2,X3)),multiply(X3,X2))) = multiply(X1,multiply(inverse(multiply(inverse(X4),multiply(X5,X4))),multiply(multiply(X5,inverse(X0)),X0))),
inference(superposition,[],[f83505,f300671]) ).
fof(f301358,plain,
! [X2,X3,X0,X1] : multiply(X1,inverse(multiply(multiply(X2,X3),inverse(X3)))) = multiply(X1,inverse(multiply(multiply(X2,inverse(X0)),X0))),
inference(superposition,[],[f170506,f300671]) ).
fof(f301411,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(X1),multiply(multiply(X2,X3),inverse(X3)))) = inverse(multiply(inverse(X1),multiply(multiply(X2,inverse(X0)),X0))),
inference(superposition,[],[f230877,f300671]) ).
fof(f301430,plain,
! [X2,X0,X1] : multiply(inverse(X1),inverse(X0)) = multiply(inverse(multiply(X2,inverse(inverse(X1)))),multiply(X2,inverse(X0))),
inference(superposition,[],[f291446,f300671]) ).
fof(f301436,plain,
! [X2,X0,X1] : multiply(inverse(X1),inverse(X0)) = multiply(inverse(multiply(X2,X1)),multiply(X2,inverse(X0))),
inference(forward_demodulation,[],[f301430,f300671]) ).
fof(f301449,plain,
! [X2,X3,X1] : inverse(multiply(inverse(X1),multiply(multiply(X2,X3),inverse(X3)))) = inverse(multiply(inverse(X1),X2)),
inference(forward_demodulation,[],[f301411,f299045]) ).
fof(f301498,plain,
! [X2,X3,X1] : multiply(X1,inverse(X2)) = multiply(X1,inverse(multiply(multiply(X2,X3),inverse(X3)))),
inference(forward_demodulation,[],[f301358,f299045]) ).
fof(f301513,plain,
! [X2,X3,X1,X4,X5] : multiply(X1,multiply(inverse(multiply(X2,X3)),multiply(X3,X2))) = multiply(X1,multiply(inverse(multiply(inverse(X4),multiply(X5,X4))),X5)),
inference(forward_demodulation,[],[f301317,f299045]) ).
fof(f301524,plain,
! [X2,X3,X0,X1,X4] : multiply(X1,multiply(multiply(multiply(X2,X3),X4),inverse(X4))) = multiply(X1,multiply(multiply(multiply(X2,inverse(X0)),X0),X3)),
inference(forward_demodulation,[],[f301300,f300671]) ).
fof(f301656,plain,
! [X2,X1] : multiply(multiply(X1,X2),inverse(X2)) = X1,
inference(forward_demodulation,[],[f301080,f299045]) ).
fof(f301752,plain,
! [X2,X0,X1] : multiply(inverse(X1),multiply(X0,X1)) = multiply(inverse(inverse(X0)),multiply(X2,inverse(X2))),
inference(forward_demodulation,[],[f300963,f300671]) ).
fof(f301773,plain,
! [X2,X0,X1] : multiply(inverse(X1),X0) = multiply(inverse(multiply(X2,X1)),multiply(X2,X0)),
inference(forward_demodulation,[],[f300941,f300671]) ).
fof(f301903,plain,
! [X3,X0,X4,X5] : inverse(X0) = multiply(inverse(multiply(X3,inverse(inverse(X4)))),multiply(X3,inverse(multiply(multiply(multiply(X0,inverse(X4)),X5),inverse(X5))))),
inference(forward_demodulation,[],[f300785,f298018]) ).
fof(f301905,plain,
! [X3,X0,X4,X5] : inverse(X0) = multiply(inverse(multiply(X3,inverse(X4))),multiply(X3,inverse(multiply(multiply(multiply(X0,X4),inverse(X5)),inverse(inverse(X5)))))),
inference(forward_demodulation,[],[f300783,f298018]) ).
fof(f301911,plain,
! [X0,X1,X6,X4,X5] : inverse(multiply(X0,X1)) = multiply(inverse(multiply(X4,X5)),multiply(X4,inverse(multiply(multiply(multiply(multiply(X0,inverse(X6)),inverse(inverse(X6))),inverse(inverse(X1))),inverse(X5))))),
inference(forward_demodulation,[],[f300777,f298018]) ).
fof(f301925,plain,
! [X2,X1] : inverse(multiply(inverse(X1),X2)) = inverse(multiply(inverse(X1),inverse(inverse(inverse(inverse(X2)))))),
inference(forward_demodulation,[],[f301449,f300195]) ).
fof(f301969,plain,
! [X2,X3,X1] : multiply(X1,inverse(X2)) = multiply(X1,inverse(multiply(inverse(X3),multiply(X2,X3)))),
inference(forward_demodulation,[],[f301498,f300827]) ).
fof(f301984,plain,
! [X2,X3,X1,X4,X5] : multiply(X1,multiply(inverse(multiply(X2,X3)),multiply(X3,X2))) = multiply(X1,multiply(X5,inverse(multiply(inverse(X4),multiply(X5,X4))))),
inference(forward_demodulation,[],[f301513,f300978]) ).
fof(f301995,plain,
! [X2,X3,X1,X4] : multiply(X1,multiply(multiply(multiply(X2,X3),X4),inverse(X4))) = multiply(X1,multiply(X2,X3)),
inference(forward_demodulation,[],[f301524,f299045]) ).
fof(f302123,plain,
! [X2,X1] : multiply(inverse(X2),multiply(X1,X2)) = X1,
inference(forward_demodulation,[],[f301656,f300978]) ).
fof(f302219,plain,
! [X2,X0,X1] : multiply(inverse(X1),multiply(X0,X1)) = multiply(X0,multiply(X2,inverse(X2))),
inference(forward_demodulation,[],[f301752,f300671]) ).
fof(f302344,plain,
! [X0,X4,X5] : inverse(X0) = multiply(inverse(X4),inverse(multiply(inverse(X5),multiply(multiply(X0,inverse(X4)),X5)))),
inference(forward_demodulation,[],[f301903,f300038]) ).
fof(f302346,plain,
! [X0,X4,X5] : inverse(X0) = multiply(inverse(inverse(X4)),inverse(multiply(multiply(multiply(X0,X4),inverse(X5)),inverse(inverse(X5))))),
inference(forward_demodulation,[],[f301905,f301436]) ).
fof(f302352,plain,
! [X0,X1,X6,X5] : inverse(multiply(X0,X1)) = multiply(inverse(X5),inverse(multiply(multiply(multiply(multiply(X0,inverse(X6)),inverse(inverse(X6))),inverse(inverse(X1))),inverse(X5)))),
inference(forward_demodulation,[],[f301911,f301436]) ).
fof(f302365,plain,
! [X2,X1] : inverse(multiply(inverse(X1),X2)) = multiply(inverse(inverse(inverse(X2))),X1),
inference(forward_demodulation,[],[f301925,f300771]) ).
fof(f302405,plain,
! [X2,X3,X1,X5] : multiply(X1,multiply(inverse(multiply(X2,X3)),multiply(X3,X2))) = multiply(X1,multiply(X5,inverse(X5))),
inference(forward_demodulation,[],[f301984,f301969]) ).
fof(f302415,plain,
! [X2,X3,X1] : multiply(X1,multiply(X2,X3)) = multiply(X1,inverse(inverse(inverse(inverse(multiply(X2,X3)))))),
inference(forward_demodulation,[],[f301995,f300195]) ).
fof(f302622,plain,
! [X2,X0] : multiply(X0,multiply(X2,inverse(X2))) = X0,
inference(forward_demodulation,[],[f302219,f302123]) ).
fof(f302735,plain,
! [X0,X4] : inverse(X0) = multiply(inverse(X4),inverse(multiply(X0,inverse(X4)))),
inference(forward_demodulation,[],[f302344,f301969]) ).
fof(f302737,plain,
! [X0,X4,X5] : inverse(X0) = multiply(inverse(inverse(X4)),inverse(multiply(inverse(inverse(X5)),multiply(multiply(X0,X4),inverse(X5))))),
inference(forward_demodulation,[],[f302346,f300827]) ).
fof(f302743,plain,
! [X0,X1,X6,X5] : inverse(multiply(X0,X1)) = multiply(inverse(X5),inverse(multiply(multiply(multiply(multiply(X0,inverse(X6)),inverse(inverse(X6))),X1),inverse(X5)))),
inference(forward_demodulation,[],[f302352,f300671]) ).
fof(f302752,plain,
! [X2,X1] : multiply(inverse(X2),X1) = inverse(multiply(inverse(X1),X2)),
inference(forward_demodulation,[],[f302365,f300671]) ).
fof(f302773,plain,
! [X2,X3,X1,X5] : multiply(X1,multiply(X5,inverse(X5))) = multiply(X1,multiply(multiply(X3,X2),inverse(multiply(X2,X3)))),
inference(forward_demodulation,[],[f302405,f300978]) ).
fof(f302783,plain,
! [X2,X3,X1] : multiply(X1,multiply(X2,X3)) = multiply(X1,inverse(inverse(multiply(X2,X3)))),
inference(forward_demodulation,[],[f302415,f300671]) ).
fof(f303063,plain,
! [X0,X4] : inverse(X0) = multiply(inverse(inverse(X4)),inverse(multiply(X0,X4))),
inference(forward_demodulation,[],[f302737,f301969]) ).
fof(f303068,plain,
! [X0,X1,X6] : inverse(multiply(X0,X1)) = inverse(multiply(multiply(multiply(X0,inverse(X6)),inverse(inverse(X6))),X1)),
inference(forward_demodulation,[],[f302743,f302735]) ).
fof(f303081,plain,
! [X2,X3,X1] : multiply(X1,multiply(multiply(X3,X2),inverse(multiply(X2,X3)))) = X1,
inference(forward_demodulation,[],[f302773,f302622]) ).
fof(f303089,plain,
! [X2,X3,X1] : multiply(X1,multiply(X2,X3)) = multiply(X1,multiply(X3,X2)),
inference(forward_demodulation,[],[f302783,f298883]) ).
fof(f303323,plain,
! [X0,X4] : inverse(X0) = multiply(X4,inverse(multiply(X0,X4))),
inference(forward_demodulation,[],[f303063,f300671]) ).
fof(f303328,plain,
! [X0,X1] : inverse(multiply(X0,X1)) = inverse(multiply(inverse(inverse(inverse(inverse(X0)))),X1)),
inference(forward_demodulation,[],[f303068,f300195]) ).
fof(f303550,plain,
! [X0,X1] : inverse(multiply(X0,X1)) = multiply(inverse(X1),inverse(inverse(inverse(X0)))),
inference(forward_demodulation,[],[f303328,f302752]) ).
fof(f303699,plain,
! [X0,X1] : inverse(multiply(X0,X1)) = multiply(inverse(X1),inverse(X0)),
inference(forward_demodulation,[],[f303550,f300671]) ).
fof(f311516,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X5,X6)),multiply(X6,X5))),multiply(inverse(multiply(X7,X3)),multiply(X7,inverse(X0))))),X4) = inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),multiply(inverse(multiply(inverse(inverse(X3)),inverse(inverse(X4)))),inverse(X0)))),
inference(superposition,[],[f234,f303323]) ).
fof(f313143,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X5,X6)),multiply(X6,X5))),multiply(inverse(multiply(X7,X3)),multiply(X7,inverse(X0))))),X4) = multiply(inverse(multiply(inverse(multiply(inverse(inverse(X3)),inverse(inverse(X4)))),inverse(X0))),multiply(inverse(multiply(X1,X2)),multiply(X2,X1))),
inference(forward_demodulation,[],[f311516,f302752]) ).
fof(f314472,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X5,X6)),multiply(X6,X5))),multiply(inverse(multiply(X7,X3)),multiply(X7,inverse(X0))))),X4) = multiply(inverse(multiply(inverse(multiply(inverse(inverse(X3)),inverse(inverse(X4)))),inverse(X0))),multiply(multiply(X2,X1),inverse(multiply(X1,X2)))),
inference(forward_demodulation,[],[f313143,f303089]) ).
fof(f315674,plain,
! [X3,X0,X6,X7,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X5,X6)),multiply(X6,X5))),multiply(inverse(multiply(X7,X3)),multiply(X7,inverse(X0))))),X4) = inverse(multiply(inverse(multiply(inverse(inverse(X3)),inverse(inverse(X4)))),inverse(X0))),
inference(forward_demodulation,[],[f314472,f303081]) ).
fof(f316734,plain,
! [X3,X0,X6,X7,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X5,X6)),multiply(X6,X5))),multiply(inverse(multiply(X7,X3)),multiply(X7,inverse(X0))))),X4) = multiply(X0,multiply(inverse(inverse(X3)),inverse(inverse(X4)))),
inference(forward_demodulation,[],[f315674,f300771]) ).
fof(f317615,plain,
! [X3,X0,X6,X7,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X5,X6)),multiply(X6,X5))),multiply(inverse(multiply(X7,X3)),multiply(X7,inverse(X0))))),X4) = multiply(X0,inverse(multiply(inverse(X4),inverse(X3)))),
inference(forward_demodulation,[],[f316734,f303699]) ).
fof(f318343,plain,
! [X3,X0,X6,X7,X4,X5] : multiply(inverse(multiply(inverse(multiply(inverse(multiply(X5,X6)),multiply(X6,X5))),multiply(inverse(multiply(X7,X3)),multiply(X7,inverse(X0))))),X4) = multiply(X0,multiply(X3,X4)),
inference(forward_demodulation,[],[f317615,f300771]) ).
fof(f318985,plain,
! [X3,X0,X6,X7,X4,X5] : multiply(X0,multiply(X3,X4)) = multiply(multiply(inverse(multiply(inverse(multiply(X7,X3)),multiply(X7,inverse(X0)))),multiply(inverse(multiply(X5,X6)),multiply(X6,X5))),X4),
inference(forward_demodulation,[],[f318343,f302752]) ).
fof(f319498,plain,
! [X3,X0,X6,X7,X4,X5] : multiply(X0,multiply(X3,X4)) = multiply(multiply(inverse(multiply(inverse(multiply(X7,X3)),multiply(X7,inverse(X0)))),multiply(multiply(X6,X5),inverse(multiply(X5,X6)))),X4),
inference(forward_demodulation,[],[f318985,f303089]) ).
fof(f319914,plain,
! [X3,X0,X7,X4] : multiply(X0,multiply(X3,X4)) = multiply(inverse(multiply(inverse(multiply(X7,X3)),multiply(X7,inverse(X0)))),X4),
inference(forward_demodulation,[],[f319498,f303081]) ).
fof(f320271,plain,
! [X3,X0,X7,X4] : multiply(X0,multiply(X3,X4)) = multiply(multiply(inverse(multiply(X7,inverse(X0))),multiply(X7,X3)),X4),
inference(forward_demodulation,[],[f319914,f302752]) ).
fof(f320585,plain,
! [X3,X0,X4] : multiply(multiply(inverse(inverse(X0)),X3),X4) = multiply(X0,multiply(X3,X4)),
inference(forward_demodulation,[],[f320271,f301773]) ).
fof(f320863,plain,
! [X3,X0,X4] : multiply(multiply(X0,X3),X4) = multiply(X0,multiply(X3,X4)),
inference(forward_demodulation,[],[f320585,f300671]) ).
fof(f323163,plain,
( multiply(a3,multiply(b3,c3)) != multiply(a3,multiply(b3,c3))
| a2 != multiply(multiply(inverse(b2),b2),a2)
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1)
| multiply(a4,b4) != multiply(b4,a4) ),
inference(superposition,[],[f3,f320863]) ).
fof(f323950,plain,
( a2 != multiply(multiply(inverse(b2),b2),a2)
| multiply(inverse(a1),a1) != multiply(inverse(b1),b1)
| multiply(a4,b4) != multiply(b4,a4) ),
inference(trivial_inequality_removal,[],[f323163]) ).
fof(f324734,plain,
( multiply(inverse(a1),a1) != multiply(inverse(b1),b1)
| multiply(a4,b4) != multiply(b4,a4) ),
inference(forward_subsumption_resolution,[],[f323950,f297948]) ).
fof(f326321,plain,
multiply(a4,b4) != multiply(b4,a4),
inference(forward_subsumption_resolution,[],[f324734,f293766]) ).
fof(f327870,plain,
$false,
inference(forward_subsumption_resolution,[],[f326321,f300978]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP084-1 : TPTP v9.3.1. Bugfixed v2.7.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.40 % Computer : n004.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Sun Sep 27 09:18:07 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.43 Running first-order theorem proving
% 0.13/0.43 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.71/2.48 % (3242675)Input is clausal, will run a generic CNF schedule.
% 10.71/2.48 % (3242748)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1418586712:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 10.71/2.48 % (3242739)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=292403827:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 10.71/2.48 % (3242740)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=3268587842:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 10.71/2.48 % (3242742)lrs+10_1_sil=8000:sp=occurrence:random_seed=364755469:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 10.71/2.48 % (3242738)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=1671099759:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 10.71/2.48 % (3242743)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=3751849862:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 10.71/2.48 % (3242750)dis-21_1_sil=8000:lcm=predicate:random_seed=3374737663:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 10.71/2.48 % (3242750)Refutation not found, incomplete strategy
% 10.71/2.48 % (3242750)------------------------------
% 10.71/2.48 % (3242750)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.71/2.48 % (3242750)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.71/2.48 % (3242750)CaDiCaL version: 2.1.3
% 10.71/2.48 % (3242750)Termination reason: Refutation not found, incomplete strategy
% 10.71/2.48 % (3242750)Time elapsed: 0.001 s
% 10.71/2.48 % (3242750)Peak memory usage: 88 MB
% 10.71/2.48 % (3242748)Instruction limit reached!
% 10.71/2.48 % (3242748)------------------------------
% 10.71/2.48 % (3242748)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.71/2.48 % (3242748)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.71/2.48 % (3242748)CaDiCaL version: 2.1.3
% 10.71/2.48 % (3242748)Termination reason: Instruction limit
% 10.71/2.48 % (3242748)Termination phase: Saturation
% 10.71/2.48 % (3242748)Time elapsed: 0.082 s
% 10.71/2.48 % (3242748)Peak memory usage: 89 MB
% 10.71/2.48 % (3242748)Instructions burned: 188 (million)
% 10.71/2.48 % (3242742)Instruction limit reached!
% 10.71/2.48 % (3242742)------------------------------
% 10.71/2.48 % (3242742)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.71/2.48 % (3242742)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.71/2.48 % (3242742)CaDiCaL version: 2.1.3
% 10.71/2.48 % (3242742)Termination reason: Instruction limit
% 10.71/2.48 % (3242742)Termination phase: Saturation
% 10.71/2.48 % (3242742)Time elapsed: 0.060 s
% 10.71/2.48 % (3242742)Peak memory usage: 89 MB
% 10.71/2.48 % (3242742)Instructions burned: 107 (million)
% 10.71/2.48 % (3242743)Instruction limit reached!
% 10.71/2.48 % (3242743)------------------------------
% 10.71/2.48 % (3242743)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.71/2.48 % (3242743)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.71/2.48 % (3242743)CaDiCaL version: 2.1.3
% 10.71/2.48 % (3242743)Termination reason: Instruction limit
% 10.71/2.48 % (3242743)Termination phase: Saturation
% 10.71/2.48 % (3242743)Time elapsed: 0.070 s
% 10.71/2.48 % (3242743)Peak memory usage: 88 MB
% 10.71/2.48 % (3242743)Instructions burned: 115 (million)
% 10.71/2.48 % (3242770)dis+1010_3_sil=8000:plsq=on:drc=off:fde=none:plsqc=1:bsd=on:plsqr=7,2:sos=on:spb=goal_then_units:random_seed=2155149510:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 10.71/2.48 % (3242770)Refutation not found, incomplete strategy
% 10.71/2.48 % (3242770)------------------------------
% 10.71/2.48 % (3242770)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.71/2.48 % (3242770)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.71/2.48 % (3242770)CaDiCaL version: 2.1.3
% 10.71/2.48 % (3242770)Termination reason: Refutation not found, incomplete strategy
% 10.71/2.48 % (3242770)Time elapsed: 0.001 s
% 10.71/2.48 % (3242770)Peak memory usage: 88 MB
% 10.71/2.48 % (3242771)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=933420082:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2996 on theBenchmark for (2996ds/189Mi)
% 19.55/3.62 % (3242771)Refutation not found, incomplete strategy
% 19.55/3.62 % (3242771)------------------------------
% 19.55/3.62 % (3242771)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.55/3.62 % (3242771)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.55/3.62 % (3242771)CaDiCaL version: 2.1.3
% 19.55/3.62 % (3242771)Termination reason: Refutation not found, incomplete strategy
% 19.55/3.62 % (3242771)Time elapsed: 0.001 s
% 19.55/3.62 % (3242771)Peak memory usage: 88 MB
% 19.55/3.62 % (3242772)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3343081811:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 19.55/3.62 % (3242750)------------------------------
% 19.55/3.62 % (3242750)------------------------------
% 19.55/3.62 % (3242772)Refutation not found, incomplete strategy
% 19.55/3.62 % (3242772)------------------------------
% 19.55/3.62 % (3242772)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.55/3.62 % (3242772)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.55/3.62 % (3242772)CaDiCaL version: 2.1.3
% 19.55/3.62 % (3242772)Termination reason: Refutation not found, incomplete strategy
% 19.55/3.62 % (3242772)Time elapsed: 0.001 s
% 19.55/3.62 % (3242772)Peak memory usage: 88 MB
% 19.55/3.62 % (3242770)------------------------------
% 19.55/3.62 % (3242770)------------------------------
% 19.55/3.62 % (3242816)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1809044728:avsq=on:i=194:fgj=on:bd=preordered_2994 on theBenchmark for (2994ds/194Mi)
% 19.55/3.62 % (3242810)lrs+10_64_to=lpo:sil=8000:random_seed=2143691117:i=126:bd=preordered_2994 on theBenchmark for (2994ds/126Mi)
% 19.55/3.62 % (3242771)------------------------------
% 19.55/3.62 % (3242771)------------------------------
% 19.55/3.62 % (3242816)Instruction limit reached!
% 19.55/3.62 % (3242816)------------------------------
% 19.55/3.62 % (3242816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.55/3.62 % (3242816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.55/3.62 % (3242816)CaDiCaL version: 2.1.3
% 19.55/3.62 % (3242816)Termination reason: Instruction limit
% 19.55/3.62 % (3242816)Termination phase: Saturation
% 19.55/3.62 % (3242816)Time elapsed: 0.054 s
% 19.55/3.62 % (3242816)Peak memory usage: 90 MB
% 19.55/3.62 % (3242816)Instructions burned: 194 (million)
% 19.55/3.62 % (3242810)Instruction limit reached!
% 19.55/3.62 % (3242810)------------------------------
% 19.55/3.62 % (3242810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.55/3.62 % (3242810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.55/3.62 % (3242810)CaDiCaL version: 2.1.3
% 19.55/3.62 % (3242810)Termination reason: Instruction limit
% 19.55/3.62 % (3242810)Termination phase: Saturation
% 19.55/3.62 % (3242810)Time elapsed: 0.067 s
% 19.55/3.62 % (3242810)Peak memory usage: 88 MB
% 19.55/3.62 % (3242810)Instructions burned: 126 (million)
% 19.55/3.62 % (3242772)------------------------------
% 19.55/3.62 % (3242772)------------------------------
% 19.55/3.62 % (3242868)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=2084818383:i=157:gtg=all_2992 on theBenchmark for (2992ds/157Mi)
% 19.55/3.62 % (3242872)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=4065375486:i=3394:sd=4:ss=included:sgt=64_2992 on theBenchmark for (2992ds/3394Mi)
% 19.55/3.63 % (3242873)lrs+1011_5_to=lpo:sil=8000:tgt=full:plsq=on:prc=on:drc=off:plsqr=31,4:sp=occurrence:urr=on:nwc=0.8:s2agt=16:br=off:random_seed=2902722026:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2992 on theBenchmark for (2992ds/106Mi)
% 19.55/3.63 % (3242868)Instruction limit reached!
% 19.55/3.63 % (3242868)------------------------------
% 19.55/3.63 % (3242868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.55/3.63 % (3242868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.55/3.63 % (3242868)CaDiCaL version: 2.1.3
% 19.55/3.63 % (3242868)Termination reason: Instruction limit
% 19.55/3.63 % (3242868)Termination phase: Saturation
% 19.55/3.63 % (3242868)Time elapsed: 0.045 s
% 19.55/3.63 % (3242868)Peak memory usage: 90 MB
% 19.55/3.63 % (3242868)Instructions burned: 158 (million)
% 19.55/3.63 % (3242877)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2109068985:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 19.55/3.63 % (3242877)Refutation not found, incomplete strategy
% 28.60/4.94 % (3242877)------------------------------
% 28.60/4.94 % (3242877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.60/4.94 % (3242877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.60/4.94 % (3242877)CaDiCaL version: 2.1.3
% 28.60/4.94 % (3242877)Termination reason: Refutation not found, incomplete strategy
% 28.60/4.94 % (3242877)Time elapsed: 0.001 s
% 28.60/4.94 % (3242877)Peak memory usage: 87 MB
% 28.60/4.94 % (3242873)Instruction limit reached!
% 28.60/4.94 % (3242873)------------------------------
% 28.60/4.94 % (3242873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.60/4.94 % (3242873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.60/4.94 % (3242873)CaDiCaL version: 2.1.3
% 28.60/4.94 % (3242873)Termination reason: Instruction limit
% 28.60/4.94 % (3242873)Termination phase: Saturation
% 28.60/4.94 % (3242873)Time elapsed: 0.063 s
% 28.60/4.94 % (3242873)Peak memory usage: 89 MB
% 28.60/4.94 % (3242873)Instructions burned: 106 (million)
% 28.60/4.94 % (3242892)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=3298619825:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2991 on theBenchmark for (2991ds/242Mi)
% 28.60/4.94 % (3242892)Instruction limit reached!
% 28.60/4.94 % (3242892)------------------------------
% 28.60/4.94 % (3242892)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.60/4.94 % (3242892)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.60/4.94 % (3242892)CaDiCaL version: 2.1.3
% 28.60/4.94 % (3242892)Termination reason: Instruction limit
% 28.60/4.94 % (3242892)Termination phase: Saturation
% 28.60/4.94 % (3242892)Time elapsed: 0.067 s
% 28.60/4.94 % (3242892)Peak memory usage: 90 MB
% 28.60/4.94 % (3242892)Instructions burned: 245 (million)
% 28.60/4.94 % (3242899)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=1050867382:cond=fast:i=5208:av=off_2990 on theBenchmark for (2990ds/5208Mi)
% 28.60/4.94 % (3242877)------------------------------
% 28.60/4.94 % (3242877)------------------------------
% 28.60/4.94 % (3242940)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3980250874:i=134:sd=2:doe=on:ss=axioms:sgt=14_2989 on theBenchmark for (2989ds/134Mi)
% 28.60/4.94 % (3242940)Instruction limit reached!
% 28.60/4.94 % (3242940)------------------------------
% 28.60/4.94 % (3242940)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.60/4.94 % (3242940)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.60/4.94 % (3242940)CaDiCaL version: 2.1.3
% 28.60/4.94 % (3242940)Termination reason: Instruction limit
% 28.60/4.94 % (3242940)Termination phase: Saturation
% 28.60/4.94 % (3242940)Time elapsed: 0.039 s
% 28.60/4.94 % (3242940)Peak memory usage: 89 MB
% 28.60/4.94 % (3242940)Instructions burned: 138 (million)
% 28.60/4.94 % (3242945)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2788654575:i=499:bd=all_2988 on theBenchmark for (2988ds/499Mi)
% 28.60/4.94 % (3242947)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=4154950700:i=191:fgj=on:bd=all_2987 on theBenchmark for (2987ds/191Mi)
% 28.60/4.94 % (3242947)Instruction limit reached!
% 28.60/4.94 % (3242947)------------------------------
% 28.60/4.94 % (3242947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.60/4.94 % (3242947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.60/4.94 % (3242947)CaDiCaL version: 2.1.3
% 28.60/4.94 % (3242947)Termination reason: Instruction limit
% 28.60/4.94 % (3242947)Termination phase: Saturation
% 28.60/4.94 % (3242947)Time elapsed: 0.054 s
% 28.60/4.94 % (3242947)Peak memory usage: 90 MB
% 28.60/4.94 % (3242947)Instructions burned: 192 (million)
% 28.60/4.94 % (3242950)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=405391684:i=264:kws=precedence:fsr=off_2985 on theBenchmark for (2985ds/264Mi)
% 28.60/4.94 % (3242945)Instruction limit reached!
% 28.60/4.94 % (3242945)------------------------------
% 28.60/4.94 % (3242945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 28.60/4.94 % (3242945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 28.60/4.94 % (3242945)CaDiCaL version: 2.1.3
% 28.60/4.94 % (3242945)Termination reason: Instruction limit
% 28.60/4.94 % (3242945)Termination phase: Saturation
% 28.60/4.94 % (3242945)Time elapsed: 0.267 s
% 52.98/8.35 % (3242945)Peak memory usage: 93 MB
% 52.98/8.35 % (3242945)Instructions burned: 499 (million)
% 52.98/8.35 % (3242950)Instruction limit reached!
% 52.98/8.35 % (3242950)------------------------------
% 52.98/8.35 % (3242950)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.98/8.35 % (3242950)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.98/8.35 % (3242950)CaDiCaL version: 2.1.3
% 52.98/8.35 % (3242950)Termination reason: Instruction limit
% 52.98/8.35 % (3242950)Termination phase: Saturation
% 52.98/8.35 % (3242950)Time elapsed: 0.077 s
% 52.98/8.35 % (3242950)Peak memory usage: 91 MB
% 52.98/8.35 % (3242950)Instructions burned: 268 (million)
% 52.98/8.35 % (3242953)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=reverse_frequency:spb=units:lcm=predicate:urr=on:s2agt=8:updr=off:random_seed=3790299238:i=3256:kws=precedence:bd=preordered:av=off_2983 on theBenchmark for (2983ds/3256Mi)
% 52.98/8.35 % (3242952)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=123975435:cond=on:i=156:bs=on:gtg=exists_all:er=known_2983 on theBenchmark for (2983ds/156Mi)
% 52.98/8.35 % (3242952)Instruction limit reached!
% 52.98/8.35 % (3242952)------------------------------
% 52.98/8.35 % (3242952)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.98/8.35 % (3242952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.98/8.35 % (3242952)CaDiCaL version: 2.1.3
% 52.98/8.35 % (3242952)Termination reason: Instruction limit
% 52.98/8.35 % (3242952)Termination phase: Saturation
% 52.98/8.35 % (3242952)Time elapsed: 0.086 s
% 52.98/8.35 % (3242952)Peak memory usage: 89 MB
% 52.98/8.35 % (3242952)Instructions burned: 157 (million)
% 52.98/8.35 % (3242956)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=215077441:i=537:av=off:ss=included_2981 on theBenchmark for (2981ds/537Mi)
% 52.98/8.35 % (3242956)Instruction limit reached!
% 52.98/8.35 % (3242956)------------------------------
% 52.98/8.35 % (3242956)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.98/8.35 % (3242956)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.98/8.35 % (3242956)CaDiCaL version: 2.1.3
% 52.98/8.35 % (3242956)Termination reason: Instruction limit
% 52.98/8.35 % (3242956)Termination phase: Saturation
% 52.98/8.35 % (3242956)Time elapsed: 0.280 s
% 52.98/8.35 % (3242956)Peak memory usage: 96 MB
% 52.98/8.35 % (3242956)Instructions burned: 537 (million)
% 52.98/8.35 % (3242958)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=2412567838:i=180:bd=preordered:av=off_2976 on theBenchmark for (2976ds/180Mi)
% 52.98/8.35 % (3242958)Instruction limit reached!
% 52.98/8.35 % (3242958)------------------------------
% 52.98/8.35 % (3242958)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.98/8.35 % (3242958)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.98/8.35 % (3242958)CaDiCaL version: 2.1.3
% 52.98/8.35 % (3242958)Termination reason: Instruction limit
% 52.98/8.35 % (3242958)Termination phase: Saturation
% 52.98/8.35 % (3242958)Time elapsed: 0.094 s
% 52.98/8.35 % (3242958)Peak memory usage: 89 MB
% 52.98/8.35 % (3242958)Instructions burned: 181 (million)
% 52.98/8.35 % (3242953)Instruction limit reached!
% 52.98/8.35 % (3242953)------------------------------
% 52.98/8.35 % (3242953)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.98/8.35 % (3242953)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.98/8.35 % (3242953)CaDiCaL version: 2.1.3
% 52.98/8.35 % (3242953)Termination reason: Instruction limit
% 52.98/8.35 % (3242953)Termination phase: Saturation
% 52.98/8.35 % (3242953)Time elapsed: 0.987 s
% 52.98/8.35 % (3242953)Peak memory usage: 150 MB
% 52.98/8.35 % (3242953)Instructions burned: 3258 (million)
% 52.98/8.35 % (3242960)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=1415457079:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2974 on theBenchmark for (2974ds/10307Mi)
% 52.98/8.35 % (3242872)Instruction limit reached!
% 52.98/8.35 % (3242872)------------------------------
% 52.98/8.35 % (3242872)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.98/8.35 % (3242872)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.98/8.35 % (3242872)CaDiCaL version: 2.1.3
% 52.98/8.35 % (3242872)Termination reason: Instruction limit
% 52.98/8.35 % (3242872)Termination phase: Saturation
% 52.98/8.35 % (3242872)Time elapsed: 1.867 s
% 52.98/8.35 % (3242872)Peak memory usage: 152 MB
% 64.24/9.99 % (3242872)Instructions burned: 3395 (million)
% 64.24/9.99 % (3242961)lrs-1010_1024_to=lpo:sil=8000:tgt=ground:plsq=on:plsqc=1:sas=cadical:plsqr=1,32:sp=arity:lma=off:spb=goal:acc=on:bce=on:nwc=1.2:alpa=false:random_seed=3882390276:i=412:gtgl=4:gtg=exists_all_2972 on theBenchmark for (2972ds/412Mi)
% 64.24/9.99 % (3242963)ott+1002_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:etr=on:spb=units:urr=on:bsr=unit_only:gs=on:s2agt=16:br=off:random_seed=1965641568:s2pl=no:i=8478:s2at=4:nm=6_2972 on theBenchmark for (2972ds/8478Mi)
% 64.24/9.99 % (3242961)Instruction limit reached!
% 64.24/9.99 % (3242961)------------------------------
% 64.24/9.99 % (3242961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.24/9.99 % (3242961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.24/9.99 % (3242961)CaDiCaL version: 2.1.3
% 64.24/9.99 % (3242961)Termination reason: Instruction limit
% 64.24/9.99 % (3242961)Termination phase: Saturation
% 64.24/9.99 % (3242961)Time elapsed: 0.115 s
% 64.24/9.99 % (3242961)Peak memory usage: 94 MB
% 64.24/9.99 % (3242961)Instructions burned: 414 (million)
% 64.24/9.99 % (3242966)ott-1011_2_sil=32000:bsd=on:sp=reverse_frequency:erd=off:urr=on:rnwc=on:gs=on:s2agt=70:updr=off:lftc=20:random_seed=3524388652:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2970 on theBenchmark for (2970ds/303Mi)
% 64.24/9.99 % (3242966)Refutation not found, incomplete strategy
% 64.24/9.99 % (3242966)------------------------------
% 64.24/9.99 % (3242966)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.24/9.99 % (3242966)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.24/9.99 % (3242966)CaDiCaL version: 2.1.3
% 64.24/9.99 % (3242966)Termination reason: Refutation not found, incomplete strategy
% 64.24/9.99 % (3242966)Time elapsed: 0.001 s
% 64.24/9.99 % (3242966)Peak memory usage: 88 MB
% 64.24/9.99 % (3242966)------------------------------
% 64.24/9.99 % (3242966)------------------------------
% 64.24/9.99 % (3242968)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=4254469482:st=4:i=720:sd=3:fsr=off:ss=axioms_2967 on theBenchmark for (2967ds/720Mi)
% 64.24/9.99 % (3242968)Refutation not found, incomplete strategy
% 64.24/9.99 % (3242968)------------------------------
% 64.24/9.99 % (3242968)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.24/9.99 % (3242968)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.24/9.99 % (3242968)CaDiCaL version: 2.1.3
% 64.24/9.99 % (3242968)Termination reason: Refutation not found, incomplete strategy
% 64.24/9.99 % (3242968)Time elapsed: 0.001 s
% 64.24/9.99 % (3242968)Peak memory usage: 88 MB
% 64.24/9.99 % (3242968)------------------------------
% 64.24/9.99 % (3242968)------------------------------
% 64.24/9.99 % (3242970)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=3236643735:i=598:bs=on:bd=preordered:av=off:ss=axioms_2964 on theBenchmark for (2964ds/598Mi)
% 64.24/9.99 % (3242970)Instruction limit reached!
% 64.24/9.99 % (3242970)------------------------------
% 64.24/9.99 % (3242970)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.24/9.99 % (3242970)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.24/9.99 % (3242970)CaDiCaL version: 2.1.3
% 64.24/9.99 % (3242970)Termination reason: Instruction limit
% 64.24/9.99 % (3242970)Termination phase: Saturation
% 64.24/9.99 % (3242970)Time elapsed: 0.182 s
% 64.24/9.99 % (3242970)Peak memory usage: 94 MB
% 64.24/9.99 % (3242970)Instructions burned: 601 (million)
% 64.24/9.99 % (3242899)Instruction limit reached!
% 64.24/9.99 % (3242899)------------------------------
% 64.24/9.99 % (3242899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 64.24/9.99 % (3242899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 64.24/9.99 % (3242899)CaDiCaL version: 2.1.3
% 64.24/9.99 % (3242899)Termination reason: Instruction limit
% 64.24/9.99 % (3242899)Termination phase: Saturation
% 64.24/9.99 % (3242899)Time elapsed: 2.776 s
% 64.24/9.99 % (3242899)Peak memory usage: 170 MB
% 64.24/9.99 % (3242899)Instructions burned: 5209 (million)
% 64.24/9.99 % (3242972)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=2591371723:i=2989:sd=3:ss=axioms:sgt=60_2961 on theBenchmark for (2961ds/2989Mi)
% 64.24/9.99 % (3242973)dis+1011_1_ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:bsd=on:sp=const_min:spb=goal_then_units:lcm=predicate:urr=ec_only:s2agt=16:random_seed=177034232:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2961 on theBenchmark for (2961ds/1997Mi)
% 89.80/13.59 % (3242972)Instruction limit reached!
% 89.80/13.59 % (3242972)------------------------------
% 89.80/13.59 % (3242972)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.80/13.59 % (3242972)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.80/13.59 % (3242972)CaDiCaL version: 2.1.3
% 89.80/13.59 % (3242972)Termination reason: Instruction limit
% 89.80/13.59 % (3242972)Termination phase: Saturation
% 89.80/13.59 % (3242972)Time elapsed: 0.881 s
% 89.80/13.59 % (3242972)Peak memory usage: 147 MB
% 89.80/13.59 % (3242972)Instructions burned: 2992 (million)
% 89.80/13.59 % (3242976)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:drc=off:sp=unary_frequency:urr=ec_only:fd=preordered:random_seed=1062497566:i=2088:bd=preordered:av=off_2951 on theBenchmark for (2951ds/2088Mi)
% 89.80/13.59 % (3242973)Instruction limit reached!
% 89.80/13.59 % (3242973)------------------------------
% 89.80/13.59 % (3242973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.80/13.59 % (3242973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.80/13.59 % (3242973)CaDiCaL version: 2.1.3
% 89.80/13.59 % (3242973)Termination reason: Instruction limit
% 89.80/13.59 % (3242973)Termination phase: Saturation
% 89.80/13.59 % (3242973)Time elapsed: 1.158 s
% 89.80/13.59 % (3242973)Peak memory usage: 137 MB
% 89.80/13.59 % (3242973)Instructions burned: 1999 (million)
% 89.80/13.59 % (3242978)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=964351941:i=1098:nicw=on_2947 on theBenchmark for (2947ds/1098Mi)
% 89.80/13.59 % (3242976)Instruction limit reached!
% 89.80/13.59 % (3242976)------------------------------
% 89.80/13.59 % (3242976)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.80/13.59 % (3242976)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.80/13.59 % (3242976)CaDiCaL version: 2.1.3
% 89.80/13.59 % (3242976)Termination reason: Instruction limit
% 89.80/13.59 % (3242976)Termination phase: Saturation
% 89.80/13.59 % (3242976)Time elapsed: 0.701 s
% 89.80/13.59 % (3242976)Peak memory usage: 139 MB
% 89.80/13.59 % (3242976)Instructions burned: 2091 (million)
% 89.80/13.59 % (3242980)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=1740839875:i=433:bd=preordered_2942 on theBenchmark for (2942ds/433Mi)
% 89.80/13.59 % (3242980)Refutation not found, incomplete strategy
% 89.80/13.59 % (3242980)------------------------------
% 89.80/13.59 % (3242980)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.80/13.59 % (3242980)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.80/13.59 % (3242980)CaDiCaL version: 2.1.3
% 89.80/13.59 % (3242980)Termination reason: Refutation not found, incomplete strategy
% 89.80/13.59 % (3242980)Time elapsed: 0.001 s
% 89.80/13.59 % (3242980)Peak memory usage: 88 MB
% 89.80/13.59 % (3242980)Instructions burned: 1 (million)
% 89.80/13.59 % (3242978)Instruction limit reached!
% 89.80/13.59 % (3242978)------------------------------
% 89.80/13.59 % (3242978)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 89.80/13.59 % (3242978)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 89.80/13.59 % (3242978)CaDiCaL version: 2.1.3
% 89.80/13.59 % (3242978)Termination reason: Instruction limit
% 89.80/13.59 % (3242978)Termination phase: Saturation
% 89.80/13.59 % (3242978)Time elapsed: 0.579 s
% 89.80/13.59 % (3242978)Peak memory usage: 101 MB
% 89.80/13.59 % (3242978)Instructions burned: 1098 (million)
% 89.80/13.59 % (3242980)------------------------------
% 89.80/13.59 % (3242980)------------------------------
% 89.80/13.59 % (3242982)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=4018419001:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2940 on theBenchmark for (2940ds/2942Mi)
% 89.80/13.59 % (3242983)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=1762613211:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2939 on theBenchmark for (2939ds/6922Mi)
% 89.80/13.59 % (3242963)Instruction limit reached!
% 89.80/13.59 % (3242963)------------------------------
% 89.80/13.59 % (3242963)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.76/16.66 % (3242963)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.76/16.66 % (3242963)CaDiCaL version: 2.1.3
% 111.76/16.66 % (3242963)Termination reason: Instruction limit
% 111.76/16.66 % (3242963)Termination phase: Saturation
% 111.76/16.66 % (3242963)Time elapsed: 4.544 s
% 111.76/16.66 % (3242963)Peak memory usage: 202 MB
% 111.76/16.66 % (3242963)Instructions burned: 8480 (million)
% 111.76/16.66 % (3242986)dis+10_5:1_sil=8000:tgt=full:plsq=on:plsqc=1:plsqr=32,1:urr=on:fd=off:nwc=0.5:br=off:slsqc=3:slsq=on:random_seed=4017413005:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2925 on theBenchmark for (2925ds/596Mi)
% 111.76/16.66 % (3242986)Refutation not found, incomplete strategy
% 111.76/16.66 % (3242986)------------------------------
% 111.76/16.66 % (3242986)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.76/16.66 % (3242986)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.76/16.66 % (3242986)CaDiCaL version: 2.1.3
% 111.76/16.66 % (3242986)Termination reason: Refutation not found, incomplete strategy
% 111.76/16.66 % (3242986)Time elapsed: 0.002 s
% 111.76/16.66 % (3242986)Peak memory usage: 88 MB
% 111.76/16.66 % (3242986)Instructions burned: 1 (million)
% 111.76/16.66 % (3242982)Instruction limit reached!
% 111.76/16.66 % (3242982)------------------------------
% 111.76/16.66 % (3242982)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.76/16.66 % (3242982)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.76/16.66 % (3242982)CaDiCaL version: 2.1.3
% 111.76/16.66 % (3242982)Termination reason: Instruction limit
% 111.76/16.66 % (3242982)Termination phase: Saturation
% 111.76/16.66 % (3242982)Time elapsed: 1.674 s
% 111.76/16.66 % (3242982)Peak memory usage: 145 MB
% 111.76/16.66 % (3242982)Instructions burned: 2943 (million)
% 111.76/16.66 % (3242986)------------------------------
% 111.76/16.66 % (3242986)------------------------------
% 111.76/16.66 % (3242988)lrs+21_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=non_intro:urr=on:fd=preordered:random_seed=2978663251:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2921 on theBenchmark for (2921ds/4123Mi)
% 111.76/16.66 % (3242989)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=4261655864:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2921 on theBenchmark for (2921ds/16411Mi)
% 111.76/16.66 % (3242983)Instruction limit reached!
% 111.76/16.66 % (3242983)------------------------------
% 111.76/16.66 % (3242983)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.76/16.66 % (3242983)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.76/16.66 % (3242983)CaDiCaL version: 2.1.3
% 111.76/16.66 % (3242983)Termination reason: Instruction limit
% 111.76/16.66 % (3242983)Termination phase: Saturation
% 111.76/16.66 % (3242983)Time elapsed: 2.075 s
% 111.76/16.66 % (3242983)Peak memory usage: 180 MB
% 111.76/16.66 % (3242983)Instructions burned: 6924 (million)
% 111.76/16.66 % (3242992)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=2279282087:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2917 on theBenchmark for (2917ds/1670Mi)
% 111.76/16.66 % (3242992)Instruction limit reached!
% 111.76/16.66 % (3242992)------------------------------
% 111.76/16.66 % (3242992)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.76/16.66 % (3242992)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.76/16.66 % (3242992)CaDiCaL version: 2.1.3
% 111.76/16.66 % (3242992)Termination reason: Instruction limit
% 111.76/16.66 % (3242992)Termination phase: Saturation
% 111.76/16.66 % (3242992)Time elapsed: 0.559 s
% 111.76/16.66 % (3242992)Peak memory usage: 136 MB
% 111.76/16.66 % (3242992)Instructions burned: 1673 (million)
% 111.76/16.66 % (3242994)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:prc=on:drc=off:fde=unused:sp=reverse_frequency:updr=off:random_seed=2650581403:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2910 on theBenchmark for (2910ds/1722Mi)
% 111.76/16.66 % (3242960)Instruction limit reached!
% 111.76/16.66 % (3242960)------------------------------
% 111.76/16.66 % (3242960)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 111.76/16.66 % (3242960)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 111.76/16.66 % (3242960)CaDiCaL version: 2.1.3
% 111.76/16.66 % (3242960)Termination reason: Instruction limit
% 111.76/16.66 % (3242960)Termination phase: Saturation
% 111.76/16.66 % (3242960)Time elapsed: 6.385 s
% 111.76/16.66 % (3242960)Peak memory usage: 179 MB
% 127.33/19.00 % (3242960)Instructions burned: 10308 (million)
% 127.33/19.00 % (3242996)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=3854280366:cts=off:cond=on:i=9530:bs=on:fsd=on_2908 on theBenchmark for (2908ds/9530Mi)
% 127.33/19.00 % (3242994)Instruction limit reached!
% 127.33/19.00 % (3242994)------------------------------
% 127.33/19.00 % (3242994)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.33/19.00 % (3242994)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.33/19.00 % (3242994)CaDiCaL version: 2.1.3
% 127.33/19.00 % (3242994)Termination reason: Instruction limit
% 127.33/19.00 % (3242994)Termination phase: Saturation
% 127.33/19.00 % (3242994)Time elapsed: 0.583 s
% 127.33/19.00 % (3242994)Peak memory usage: 136 MB
% 127.33/19.00 % (3242994)Instructions burned: 1724 (million)
% 127.33/19.00 % (3242998)lrs+10_1_ncem=casc2026/models/loop4.pt:sil=64000:npcc=on:sp=occurrence:random_seed=856787345:st=2:i=4495:sd=10:ss=included_2903 on theBenchmark for (2903ds/4495Mi)
% 127.33/19.00 % (3242988)Instruction limit reached!
% 127.33/19.00 % (3242988)------------------------------
% 127.33/19.00 % (3242988)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.33/19.00 % (3242988)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.33/19.00 % (3242988)CaDiCaL version: 2.1.3
% 127.33/19.00 % (3242988)Termination reason: Instruction limit
% 127.33/19.00 % (3242988)Termination phase: Saturation
% 127.33/19.00 % (3242988)Time elapsed: 2.302 s
% 127.33/19.00 % (3242988)Peak memory usage: 157 MB
% 127.33/19.00 % (3242988)Instructions burned: 4124 (million)
% 127.33/19.00 % (3243000)lrs+1002_1_sfv=off:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=reverse_arity:spb=non_intro:s2agt=16:random_seed=2233541776:cond=fast:i=4920:s2at=1.9:kws=inv_frequency:av=off:er=filter_2897 on theBenchmark for (2897ds/4920Mi)
% 127.33/19.00 % (3242998)Instruction limit reached!
% 127.33/19.00 % (3242998)------------------------------
% 127.33/19.00 % (3242998)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.33/19.00 % (3242998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.33/19.00 % (3242998)CaDiCaL version: 2.1.3
% 127.33/19.00 % (3242998)Termination reason: Instruction limit
% 127.33/19.00 % (3242998)Termination phase: Saturation
% 127.33/19.00 % (3242998)Time elapsed: 1.316 s
% 127.33/19.00 % (3242998)Peak memory usage: 163 MB
% 127.33/19.00 % (3242998)Instructions burned: 4497 (million)
% 127.33/19.00 % (3243002)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:lcm=reverse:bce=on:bsr=unit_only:random_seed=811274045:cts=off:cond=on:i=2083:s2at=-1:fgj=on:av=off_2888 on theBenchmark for (2888ds/2083Mi)
% 127.33/19.00 % (3243002)Instruction limit reached!
% 127.33/19.00 % (3243002)------------------------------
% 127.33/19.00 % (3243002)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.33/19.00 % (3243002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.33/19.00 % (3243002)CaDiCaL version: 2.1.3
% 127.33/19.00 % (3243002)Termination reason: Instruction limit
% 127.33/19.00 % (3243002)Termination phase: Saturation
% 127.33/19.00 % (3243002)Time elapsed: 0.682 s
% 127.33/19.00 % (3243002)Peak memory usage: 140 MB
% 127.33/19.00 % (3243002)Instructions burned: 2086 (million)
% 127.33/19.00 % (3243004)lrs+31_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=weighted_frequency:sos=all:spb=units:lcm=predicate:bsr=on:gs=on:random_seed=2843075674:i=4629:av=off:gsp=on_2880 on theBenchmark for (2880ds/4629Mi)
% 127.33/19.00 % (3243004)Refutation not found, incomplete strategy
% 127.33/19.00 % (3243004)------------------------------
% 127.33/19.00 % (3243004)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 127.33/19.00 % (3243004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 127.33/19.00 % (3243004)CaDiCaL version: 2.1.3
% 127.33/19.00 % (3243004)Termination reason: Refutation not found, incomplete strategy
% 127.33/19.00 % (3243004)Time elapsed: 0.334 s
% 127.33/19.00 % (3243004)Peak memory usage: 127 MB
% 127.33/19.00 % (3243004)Instructions burned: 858 (million)
% 127.33/19.00 % (3243004)------------------------------
% 127.33/19.00 % (3243004)------------------------------
% 127.33/19.00 % (3243006)dis+10_64_sil=16000:tgt=full:plsq=on:prc=on:drc=off:plsqc=2:plsqr=32,1:spb=goal:random_seed=411966396:i=1258:av=off_2874 on theBenchmark for (2874ds/1258Mi)
% 146.88/21.66 % (3243006)Instruction limit reached!
% 146.88/21.66 % (3243006)------------------------------
% 146.88/21.66 % (3243006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.88/21.66 % (3243006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.88/21.66 % (3243006)CaDiCaL version: 2.1.3
% 146.88/21.66 % (3243006)Termination reason: Instruction limit
% 146.88/21.66 % (3243006)Termination phase: Saturation
% 146.88/21.66 % (3243006)Time elapsed: 0.341 s
% 146.88/21.66 % (3243006)Peak memory usage: 91 MB
% 146.88/21.66 % (3243006)Instructions burned: 1262 (million)
% 146.88/21.66 % (3243000)Instruction limit reached!
% 146.88/21.66 % (3243000)------------------------------
% 146.88/21.66 % (3243000)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.88/21.66 % (3243000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.88/21.66 % (3243000)CaDiCaL version: 2.1.3
% 146.88/21.66 % (3243000)Termination reason: Instruction limit
% 146.88/21.66 % (3243000)Termination phase: Saturation
% 146.88/21.66 % (3243000)Time elapsed: 2.653 s
% 146.88/21.66 % (3243000)Peak memory usage: 166 MB
% 146.88/21.66 % (3243000)Instructions burned: 4921 (million)
% 146.88/21.66 % (3243066)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1176706732:i=7343:av=off:ss=included_2869 on theBenchmark for (2869ds/7343Mi)
% 146.88/21.66 % (3243090)lrs-1002_1_to=lpo:sil=16000:sp=reverse_arity:sos=on:random_seed=2370232233:i=1325:sd=2:ss=axioms:sgt=16_2868 on theBenchmark for (2868ds/1325Mi)
% 146.88/21.66 % (3243090)Refutation not found, incomplete strategy
% 146.88/21.66 % (3243090)------------------------------
% 146.88/21.66 % (3243090)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.88/21.66 % (3243090)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.88/21.66 % (3243090)CaDiCaL version: 2.1.3
% 146.88/21.66 % (3243090)Termination reason: Refutation not found, incomplete strategy
% 146.88/21.66 % (3243090)Time elapsed: 0.001 s
% 146.88/21.66 % (3243090)Peak memory usage: 88 MB
% 146.88/21.66 % (3243090)------------------------------
% 146.88/21.66 % (3243090)------------------------------
% 146.88/21.66 % (3243144)dis+1011_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=arity:lma=off:spb=intro:urr=ec_only:sac=on:random_seed=2746130191:st=3.9:cond=fast:i=2646:s2at=1.8:sd=5:amm=off:gtg=position:ss=axioms:fsd=on_2864 on theBenchmark for (2864ds/2646Mi)
% 146.88/21.66 % (3242996)Instruction limit reached!
% 146.88/21.66 % (3242996)------------------------------
% 146.88/21.66 % (3242996)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.88/21.66 % (3242996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.88/21.66 % (3242996)CaDiCaL version: 2.1.3
% 146.88/21.66 % (3242996)Termination reason: Instruction limit
% 146.88/21.66 % (3242996)Termination phase: Saturation
% 146.88/21.66 % (3242996)Time elapsed: 5.383 s
% 146.88/21.66 % (3242996)Peak memory usage: 191 MB
% 146.88/21.66 % (3242996)Instructions burned: 9530 (million)
% 146.88/21.66 % (3243260)dis-1003_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:sp=arity:sos=on:urr=on:random_seed=2452267900:i=1489:sd=2:ep=R:ss=axioms_2853 on theBenchmark for (2853ds/1489Mi)
% 146.88/21.66 % (3243144)Instruction limit reached!
% 146.88/21.66 % (3243144)------------------------------
% 146.88/21.66 % (3243144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.88/21.66 % (3243144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.88/21.66 % (3243144)CaDiCaL version: 2.1.3
% 146.88/21.66 % (3243144)Termination reason: Instruction limit
% 146.88/21.66 % (3243144)Termination phase: Saturation
% 146.88/21.66 % (3243144)Time elapsed: 1.953 s
% 146.88/21.66 % (3243144)Peak memory usage: 144 MB
% 146.88/21.66 % (3243144)Instructions burned: 2648 (million)
% 146.88/21.66 % (3243066)Instruction limit reached!
% 146.88/21.66 % (3243066)------------------------------
% 146.88/21.66 % (3243066)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 146.88/21.66 % (3243066)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 146.88/21.66 % (3243066)CaDiCaL version: 2.1.3
% 146.88/21.66 % (3243066)Termination reason: Instruction limit
% 146.88/21.66 % (3243066)Termination phase: Saturation
% 146.88/21.66 % (3243066)Time elapsed: 2.507 s
% 146.88/21.66 % (3243066)Peak memory usage: 188 MB
% 146.88/21.66 % (3243066)Instructions burned: 7345 (million)
% 146.88/21.66 % (3243260)Refutation not found, incomplete strategy
% 146.88/21.66 % (3243260)------------------------------
% 146.88/21.66 % (3243260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 163.49/24.00 % (3243260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.49/24.00 % (3243260)CaDiCaL version: 2.1.3
% 163.49/24.00 % (3243260)Termination reason: Refutation not found, incomplete strategy
% 163.49/24.00 % (3243260)Time elapsed: 0.878 s
% 163.49/24.00 % (3243260)Peak memory usage: 127 MB
% 163.49/24.00 % (3243260)Instructions burned: 860 (million)
% 163.49/24.00 % (3243285)lrs+20_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:fde=unused:sp=occurrence:sos=on:lcm=predicate:urr=full:sac=on:random_seed=679237030:i=1503_2843 on theBenchmark for (2843ds/1503Mi)
% 163.49/24.00 % (3243286)lrs+10_1_ncem=casc2026/models/loop3.pt:sil=16000:tgt=ground:npcc=on:random_seed=321909279:i=13942:kws=frequency_2843 on theBenchmark for (2843ds/13942Mi)
% 163.49/24.00 % (3243260)------------------------------
% 163.49/24.00 % (3243260)------------------------------
% 163.49/24.00 % (3243291)lrs-1002_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:bsd=on:sp=unary_frequency:spb=goal:lcm=predicate:acc=on:urr=full:bce=on:bsr=unit_only:s2agt=64:sac=on:random_seed=3235861718:i=3604:fsr=off:er=filter_2840 on theBenchmark for (2840ds/3604Mi)
% 163.49/24.00 % (3243285)Refutation not found, incomplete strategy
% 163.49/24.00 % (3243285)------------------------------
% 163.49/24.00 % (3243285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 163.49/24.00 % (3243285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.49/24.00 % (3243285)CaDiCaL version: 2.1.3
% 163.49/24.00 % (3243285)Termination reason: Refutation not found, incomplete strategy
% 163.49/24.00 % (3243285)Time elapsed: 0.596 s
% 163.49/24.00 % (3243285)Peak memory usage: 128 MB
% 163.49/24.00 % (3243285)Instructions burned: 890 (million)
% 163.49/24.00 % (3243285)------------------------------
% 163.49/24.00 % (3243285)------------------------------
% 163.49/24.00 % (3243399)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:random_seed=1771424359:i=1876:sd=1:ss=included:sgt=32_2832 on theBenchmark for (2832ds/1876Mi)
% 163.49/24.00 % (3242989)Instruction limit reached!
% 163.49/24.00 % (3242989)------------------------------
% 163.49/24.00 % (3242989)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 163.49/24.00 % (3242989)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.49/24.00 % (3242989)CaDiCaL version: 2.1.3
% 163.49/24.00 % (3242989)Termination reason: Instruction limit
% 163.49/24.00 % (3242989)Termination phase: Saturation
% 163.49/24.00 % (3242989)Time elapsed: 9.351 s
% 163.49/24.00 % (3242989)Peak memory usage: 255 MB
% 163.49/24.00 % (3242989)Instructions burned: 16412 (million)
% 163.49/24.00 % (3243448)lrs+10_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:fde=none:sp=arity:urr=on:br=off:random_seed=3083387911:i=1932:bd=preordered:ins=10:sup=off:ss=axioms_2825 on theBenchmark for (2825ds/1932Mi)
% 163.49/24.00 % (3243291)Instruction limit reached!
% 163.49/24.00 % (3243291)------------------------------
% 163.49/24.00 % (3243291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 163.49/24.00 % (3243291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.49/24.00 % (3243291)CaDiCaL version: 2.1.3
% 163.49/24.00 % (3243291)Termination reason: Instruction limit
% 163.49/24.00 % (3243291)Termination phase: Saturation
% 163.49/24.00 % (3243291)Time elapsed: 1.749 s
% 163.49/24.00 % (3243291)Peak memory usage: 156 MB
% 163.49/24.01 % (3243291)Instructions burned: 3605 (million)
% 163.49/24.01 % (3243399)Instruction limit reached!
% 163.49/24.01 % (3243399)------------------------------
% 163.49/24.01 % (3243399)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 163.49/24.01 % (3243399)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 163.49/24.01 % (3243399)CaDiCaL version: 2.1.3
% 163.49/24.01 % (3243399)Termination reason: Instruction limit
% 163.49/24.01 % (3243399)Termination phase: Saturation
% 163.49/24.01 % (3243399)Time elapsed: 1.086 s
% 163.49/24.01 % (3243399)Peak memory usage: 138 MB
% 163.49/24.01 % (3243399)Instructions burned: 1877 (million)
% 163.49/24.01 % (3243450)dis-1010_1_ncem=casc2026/models/loop1.pt:sil=8000:npcc=on:fde=unused:etr=on:sp=weighted_frequency:spb=goal_then_units:urr=ec_only:fd=preordered:kmz=on:random_seed=2712215741:s2pl=on:cond=fast:i=1980:s2at=2:kws=inv_precedence:doe=on:ins=1:av=off:gsp=on_2821 on theBenchmark for (2821ds/1980Mi)
% 163.49/24.01 % (3243451)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=unary_first:sos=all:spb=units:urr=on:br=off:random_seed=3328146703:i=3902:kws=inv_arity_squared:fgj=on:ss=axioms:sgt=11_2820 on theBenchmark for (2820ds/3902Mi)
% 182.54/26.64 % (3243448)Refutation not found, incomplete strategy
% 182.54/26.64 % (3243448)------------------------------
% 182.54/26.64 % (3243448)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 182.54/26.64 % (3243448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.54/26.64 % (3243448)CaDiCaL version: 2.1.3
% 182.54/26.64 % (3243448)Termination reason: Refutation not found, incomplete strategy
% 182.54/26.64 % (3243448)Time elapsed: 0.571 s
% 182.54/26.64 % (3243448)Peak memory usage: 127 MB
% 182.54/26.64 % (3243448)Instructions burned: 857 (million)
% 182.54/26.64 % (3243448)------------------------------
% 182.54/26.64 % (3243448)------------------------------
% 182.54/26.64 % (3243454)dis+10_32_sil=16000:tgt=ground:drc=off:sas=cadical:acc=on:alpa=false:avsqc=3:random_seed=1166929210:avsq=on:i=3916:aac=none:amm=off_2815 on theBenchmark for (2815ds/3916Mi)
% 182.54/26.64 % (3243451)Refutation not found, incomplete strategy
% 182.54/26.64 % (3243451)------------------------------
% 182.54/26.64 % (3243451)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 182.54/26.64 % (3243451)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.54/26.64 % (3243451)CaDiCaL version: 2.1.3
% 182.54/26.64 % (3243451)Termination reason: Refutation not found, incomplete strategy
% 182.54/26.64 % (3243451)Time elapsed: 0.569 s
% 182.54/26.64 % (3243451)Peak memory usage: 127 MB
% 182.54/26.64 % (3243451)Instructions burned: 859 (million)
% 182.54/26.64 % (3243451)------------------------------
% 182.54/26.64 % (3243451)------------------------------
% 182.54/26.64 % (3243456)dis+10_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=full:npcc=on:drc=ordering:lcm=predicate:random_seed=39063740:cond=on:i=3940:av=off:er=known_2810 on theBenchmark for (2810ds/3940Mi)
% 182.54/26.64 % (3243450)Instruction limit reached!
% 182.54/26.64 % (3243450)------------------------------
% 182.54/26.64 % (3243450)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 182.54/26.64 % (3243450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.54/26.64 % (3243450)CaDiCaL version: 2.1.3
% 182.54/26.64 % (3243450)Termination reason: Instruction limit
% 182.54/26.64 % (3243450)Termination phase: Saturation
% 182.54/26.64 % (3243450)Time elapsed: 1.130 s
% 182.54/26.64 % (3243450)Peak memory usage: 138 MB
% 182.54/26.64 % (3243450)Instructions burned: 1980 (million)
% 182.54/26.64 % (3243458)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=reverse_frequency:bce=on:random_seed=259615614:s2pl=on:i=3980:gtgl=3:kws=precedence:fgj=on:gtg=all_2808 on theBenchmark for (2808ds/3980Mi)
% 182.54/26.64 % (3243286)Instruction limit reached!
% 182.54/26.64 % (3243286)------------------------------
% 182.54/26.64 % (3243286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 182.54/26.64 % (3243286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.54/26.64 % (3243286)CaDiCaL version: 2.1.3
% 182.54/26.64 % (3243286)Termination reason: Instruction limit
% 182.54/26.64 % (3243286)Termination phase: Saturation
% 182.54/26.64 % (3243286)Time elapsed: 4.054 s
% 182.54/26.64 % (3243286)Peak memory usage: 228 MB
% 182.54/26.64 % (3243286)Instructions burned: 13946 (million)
% 182.54/26.64 % (3243460)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:prc=on:sp=reverse_frequency:spb=units:lsd=20:urr=ec_only:bce=on:fd=off:kmz=on:random_seed=2703830977:i=2087:s2at=3:kws=frequency:av=off:fsr=off_2800 on theBenchmark for (2800ds/2087Mi)
% 182.54/26.64 % (3243454)Instruction limit reached!
% 182.54/26.64 % (3243454)------------------------------
% 182.54/26.64 % (3243454)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 182.54/26.64 % (3243454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.54/26.64 % (3243454)CaDiCaL version: 2.1.3
% 182.54/26.64 % (3243454)Termination reason: Instruction limit
% 182.54/26.64 % (3243454)Termination phase: Saturation
% 182.54/26.64 % (3243454)Time elapsed: 1.752 s
% 182.54/26.64 % (3243454)Peak memory usage: 117 MB
% 182.54/26.64 % (3243454)Instructions burned: 3916 (million)
% 182.54/26.64 % (3243462)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=1084980067:cts=off:cond=on:i=4272:bs=on:fsd=on_2796 on theBenchmark for (2796ds/4272Mi)
% 182.54/26.64 % (3243460)Instruction limit reached!
% 182.54/26.64 % (3243460)------------------------------
% 182.54/26.64 % (3243460)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 225.63/32.75 % (3243460)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 225.63/32.75 % (3243460)CaDiCaL version: 2.1.3
% 225.63/32.75 % (3243460)Termination reason: Instruction limit
% 225.63/32.75 % (3243460)Termination phase: Saturation
% 225.63/32.75 % (3243460)Time elapsed: 0.667 s
% 225.63/32.75 % (3243460)Peak memory usage: 140 MB
% 225.63/32.75 % (3243460)Instructions burned: 2088 (million)
% 225.63/32.75 % (3243464)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=113224861:st=-1:i=2197:kws=precedence:av=off:ss=axioms:er=known_2792 on theBenchmark for (2792ds/2197Mi)
% 225.63/32.75 % (3243456)Instruction limit reached!
% 225.63/32.75 % (3243456)------------------------------
% 225.63/32.75 % (3243456)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 225.63/32.75 % (3243456)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 225.63/32.75 % (3243456)CaDiCaL version: 2.1.3
% 225.63/32.75 % (3243456)Termination reason: Instruction limit
% 225.63/32.75 % (3243456)Termination phase: Saturation
% 225.63/32.75 % (3243456)Time elapsed: 2.107 s
% 225.63/32.75 % (3243456)Peak memory usage: 155 MB
% 225.63/32.75 % (3243456)Instructions burned: 3942 (million)
% 225.63/32.75 % (3243466)dis+21_1_sil=8000:spb=goal_then_units:random_seed=3702211265:avsq=on:i=6508:avsqr=1,16:kws=arity_squared:fgj=on_2787 on theBenchmark for (2787ds/6508Mi)
% 225.63/32.75 % (3243458)Instruction limit reached!
% 225.63/32.75 % (3243458)------------------------------
% 225.63/32.75 % (3243458)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 225.63/32.75 % (3243458)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 225.63/32.75 % (3243458)CaDiCaL version: 2.1.3
% 225.63/32.75 % (3243458)Termination reason: Instruction limit
% 225.63/32.75 % (3243458)Termination phase: Saturation
% 225.63/32.75 % (3243458)Time elapsed: 2.190 s
% 225.63/32.75 % (3243458)Peak memory usage: 158 MB
% 225.63/32.75 % (3243458)Instructions burned: 3980 (million)
% 225.63/32.75 % (3243464)Instruction limit reached!
% 225.63/32.75 % (3243464)------------------------------
% 225.63/32.75 % (3243464)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 225.63/32.75 % (3243464)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 225.63/32.75 % (3243464)CaDiCaL version: 2.1.3
% 225.63/32.75 % (3243464)Termination reason: Instruction limit
% 225.63/32.75 % (3243464)Termination phase: Saturation
% 225.63/32.75 % (3243464)Time elapsed: 0.704 s
% 225.63/32.75 % (3243464)Peak memory usage: 140 MB
% 225.63/32.75 % (3243464)Instructions burned: 2200 (million)
% 225.63/32.75 % (3243468)dis-1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=occurrence:random_seed=3722047386:i=2330:fgj=on:av=off:fsr=off_2785 on theBenchmark for (2785ds/2330Mi)
% 225.63/32.75 % (3243469)dis+10_2_anc=none:sil=64000:bsr=on:rp=on:alpa=true:avsqc=1:random_seed=1953371224:avsq=on:i=7592:avsqr=1,16:bs=on:gsp=on_2783 on theBenchmark for (2783ds/7592Mi)
% 225.63/32.75 % (3243462)Instruction limit reached!
% 225.63/32.75 % (3243462)------------------------------
% 225.63/32.75 % (3243462)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 225.63/32.75 % (3243462)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 225.63/32.75 % (3243462)CaDiCaL version: 2.1.3
% 225.63/32.75 % (3243462)Termination reason: Instruction limit
% 225.63/32.75 % (3243462)Termination phase: Saturation
% 225.63/32.75 % (3243462)Time elapsed: 2.445 s
% 225.63/32.75 % (3243462)Peak memory usage: 158 MB
% 225.63/32.75 % (3243462)Instructions burned: 4272 (million)
% 225.63/32.75 % (3243468)Instruction limit reached!
% 225.63/32.75 % (3243468)------------------------------
% 225.63/32.75 % (3243468)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 225.63/32.75 % (3243468)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 225.63/32.75 % (3243468)CaDiCaL version: 2.1.3
% 225.63/32.75 % (3243468)Termination reason: Instruction limit
% 225.63/32.75 % (3243468)Termination phase: Saturation
% 225.63/32.75 % (3243468)Time elapsed: 1.300 s
% 225.63/32.75 % (3243468)Peak memory usage: 141 MB
% 225.63/32.75 % (3243468)Instructions burned: 2331 (million)
% 225.63/32.75 % (3243472)lrs-1002_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=ground:npcc=on:prc=on:sims=off:sp=reverse_frequency:spb=goal_then_units:bce=on:bsr=unit_only:gs=on:flr=on:random_seed=2848826590:i=2693:kws=precedence:ins=1:av=off_2770 on theBenchmark for (2770ds/2693Mi)
% 225.63/32.75 % (3243473)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:random_seed=1079352394:i=28651:sd=4:ss=included:sgt=64_2770 on theBenchmark for (2770ds/28651Mi)
% 275.55/39.89 % (3243469)Instruction limit reached!
% 275.55/39.89 % (3243469)------------------------------
% 275.55/39.89 % (3243469)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 275.55/39.89 % (3243469)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 275.55/39.89 % (3243469)CaDiCaL version: 2.1.3
% 275.55/39.89 % (3243469)Termination reason: Instruction limit
% 275.55/39.89 % (3243469)Termination phase: Saturation
% 275.55/39.89 % (3243469)Time elapsed: 1.972 s
% 275.55/39.89 % (3243469)Peak memory usage: 126 MB
% 275.55/39.89 % (3243469)Instructions burned: 7593 (million)
% 275.55/39.89 % (3243476)lrs-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_frequency:random_seed=1466881953:i=2700:kws=precedence:fgj=on:bd=preordered:ins=1_2762 on theBenchmark for (2762ds/2700Mi)
% 275.55/39.89 % (3243466)Instruction limit reached!
% 275.55/39.89 % (3243466)------------------------------
% 275.55/39.89 % (3243466)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 275.55/39.89 % (3243466)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 275.55/39.89 % (3243466)CaDiCaL version: 2.1.3
% 275.55/39.89 % (3243466)Termination reason: Instruction limit
% 275.55/39.89 % (3243466)Termination phase: Saturation
% 275.55/39.89 % (3243466)Time elapsed: 3.146 s
% 275.55/39.89 % (3243466)Peak memory usage: 122 MB
% 275.55/39.89 % (3243466)Instructions burned: 6510 (million)
% 275.55/39.89 % (3243472)Instruction limit reached!
% 275.55/39.89 % (3243472)------------------------------
% 275.55/39.89 % (3243472)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 275.55/39.89 % (3243472)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 275.55/39.89 % (3243472)CaDiCaL version: 2.1.3
% 275.55/39.89 % (3243472)Termination reason: Instruction limit
% 275.55/39.89 % (3243472)Termination phase: Saturation
% 275.55/39.89 % (3243472)Time elapsed: 1.535 s
% 275.55/39.89 % (3243472)Peak memory usage: 146 MB
% 275.55/39.89 % (3243472)Instructions burned: 2695 (million)
% 275.55/39.89 % (3243476)Instruction limit reached!
% 275.55/39.89 % (3243476)------------------------------
% 275.55/39.89 % (3243476)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 275.55/39.89 % (3243476)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 275.55/39.89 % (3243476)CaDiCaL version: 2.1.3
% 275.55/39.89 % (3243476)Termination reason: Instruction limit
% 275.55/39.89 % (3243476)Termination phase: Saturation
% 275.55/39.89 % (3243476)Time elapsed: 0.814 s
% 275.55/39.89 % (3243476)Peak memory usage: 144 MB
% 275.55/39.89 % (3243476)Instructions burned: 2702 (million)
% 275.55/39.89 % (3243478)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_min:sos=on:erd=off:spb=goal:lsd=20:urr=full:sac=on:random_seed=3175577836:i=3196:nm=4_2754 on theBenchmark for (2754ds/3196Mi)
% 275.55/39.89 % (3243480)dis+1011_1_sfv=off:ncem=casc2026/models/loop2.pt:sil=32000:tgt=ground:npcc=on:lcm=predicate:bce=on:sac=on:random_seed=1947690471:i=3264:bd=all:gtg=exists_sym:ss=included:er=known_2753 on theBenchmark for (2753ds/3264Mi)
% 275.55/39.89 % (3243479)ott+11_1_ncem=casc2026/models/loop4.pt:sil=64000:tgt=full:irw=on:npcc=on:spb=units:flr=on:random_seed=1989396271:cts=off:i=3254:av=off_2753 on theBenchmark for (2753ds/3254Mi)
% 275.55/39.89 % (3243478)Refutation not found, incomplete strategy
% 275.55/39.89 % (3243478)------------------------------
% 275.55/39.89 % (3243478)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 275.55/39.89 % (3243478)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 275.55/39.89 % (3243478)CaDiCaL version: 2.1.3
% 275.55/39.89 % (3243478)Termination reason: Refutation not found, incomplete strategy
% 275.55/39.89 % (3243478)Time elapsed: 0.587 s
% 275.55/39.89 % (3243478)Peak memory usage: 127 MB
% 275.55/39.89 % (3243478)Instructions burned: 890 (million)
% 275.55/39.89 % (3243478)------------------------------
% 275.55/39.89 % (3243478)------------------------------
% 275.55/39.89 % (3243484)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=unary_first:sos=on:lma=off:lsd=20:urr=on:kmz=on:sac=on:random_seed=1573901900:st=6:i=9708:kws=inv_frequency:doe=on:fgj=on:ss=axioms_2744 on theBenchmark for (2744ds/9708Mi)
% 275.55/39.89 % (3243480)Instruction limit reached!
% 275.55/39.89 % (3243480)------------------------------
% 275.55/39.89 % (3243480)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 275.55/39.89 % (3243480)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 239.50/40.40 % (3243480)CaDiCaL version: 2.1.3
% 239.50/40.40 % (3243480)Termination reason: Instruction limit
% 239.50/40.40 % (3243480)Termination phase: Saturation
% 239.50/40.40 % (3243480)Time elapsed: 0.975 s
% 239.50/40.40 % (3243480)Peak memory usage: 150 MB
% 239.50/40.40 % (3243480)Instructions burned: 3268 (million)
% 239.50/40.40 % (3243486)lrs+1010_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=4116113792:i=21997:s2at=5:gtg=all_2742 on theBenchmark for (2742ds/21997Mi)
% 239.50/40.40 % (3243484)Refutation not found, incomplete strategy
% 239.50/40.40 % (3243484)------------------------------
% 239.50/40.40 % (3243484)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 239.50/40.40 % (3243484)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 239.50/40.40 % (3243484)CaDiCaL version: 2.1.3
% 239.50/40.40 % (3243484)Termination reason: Refutation not found, incomplete strategy
% 239.50/40.40 % (3243484)Time elapsed: 0.553 s
% 239.50/40.40 % (3243484)Peak memory usage: 127 MB
% 239.50/40.40 % (3243484)Instructions burned: 890 (million)
% 239.50/40.40 % (3243484)------------------------------
% 239.50/40.40 % (3243484)------------------------------
% 239.50/40.40 % (3243479)Instruction limit reached!
% 239.50/40.40 % (3243479)------------------------------
% 239.50/40.40 % (3243479)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 239.50/40.40 % (3243479)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 239.50/40.40 % (3243479)CaDiCaL version: 2.1.3
% 239.50/40.40 % (3243479)Termination reason: Instruction limit
% 239.50/40.40 % (3243479)Termination phase: Saturation
% 239.50/40.40 % (3243479)Time elapsed: 1.767 s
% 239.50/40.40 % (3243479)Peak memory usage: 146 MB
% 239.50/40.40 % (3243479)Instructions burned: 3254 (million)
% 239.50/40.40 % (3243488)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2691615480:i=7551:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2735 on theBenchmark for (2735ds/7551Mi)
% 239.50/40.40 % (3243490)lrs+1011_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1537951903:i=8924:sd=1:ss=included_2733 on theBenchmark for (2733ds/8924Mi)
% 239.50/40.40 % (3243488)Instruction limit reached!
% 239.50/40.40 % (3243488)------------------------------
% 239.50/40.40 % (3243488)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 239.50/40.40 % (3243488)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 239.50/40.40 % (3243488)CaDiCaL version: 2.1.3
% 239.50/40.40 % (3243488)Termination reason: Instruction limit
% 239.50/40.40 % (3243488)Termination phase: Saturation
% 239.50/40.40 % (3243488)Time elapsed: 1.824 s
% 239.50/40.40 % (3243488)Peak memory usage: 137 MB
% 239.50/40.40 % (3243488)Instructions burned: 7555 (million)
% 239.50/40.40 % (3243645)lrs+1011_1_ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=arity:fd=preordered:random_seed=1503073183:i=9638:kws=frequency:bd=preordered_2715 on theBenchmark for (2715ds/9638Mi)
% 239.50/40.40 % (3243645)Instruction limit reached!
% 239.50/40.40 % (3243645)------------------------------
% 239.50/40.40 % (3243645)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 239.50/40.40 % (3243645)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 239.50/40.40 % (3243645)CaDiCaL version: 2.1.3
% 239.50/40.40 % (3243645)Termination reason: Instruction limit
% 279.76/40.40 % (3243645)Termination phase: Saturation
% 279.76/40.40 % (3243645)Time elapsed: 2.994 s
% 279.76/40.40 % (3243645)Peak memory usage: 200 MB
% 279.76/40.40 % (3243645)Instructions burned: 9641 (million)
% 279.76/40.40 % (3243917)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:prc=on:drc=off:sp=const_min:sos=on:lcm=predicate:s2agt=20:br=off:flr=on:random_seed=2225080426:i=5177:s2at=1.5:bd=preordered:ins=10:fdi=128_2684 on theBenchmark for (2684ds/5177Mi)
% 279.76/40.40 % (3243490)Instruction limit reached!
% 279.76/40.40 % (3243490)------------------------------
% 279.76/40.40 % (3243490)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 279.76/40.40 % (3243490)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 279.76/40.40 % (3243490)CaDiCaL version: 2.1.3
% 279.76/40.40 % (3243490)Termination reason: Instruction limit
% 279.76/40.40 % (3243490)Termination phase: Saturation
% 279.76/40.40 % (3243490)Time elapsed: 4.913 s
% 279.76/40.40 % (3243490)Peak memory usage: 212 MB
% 279.76/40.40 % (3243490)Instructions burned: 8924 (million)
% 279.76/40.40 % (3243919)lrs-1011_1_ncem=casc2026/models/loop4.pt:sil=32000:tgt=ground:npcc=on:sas=cadical:sp=unary_first:acc=on:alpa=false:random_seed=954040907:i=6464:aac=none:ins=10_2682 on theBenchmark for (2682ds/6464Mi)
% 279.76/40.40 % (3243917)Refutation not found, incomplete strategy
% 279.76/40.40 % (3243917)------------------------------
% 279.76/40.40 % (3243917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 279.76/40.40 % (3243917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 279.76/40.40 % (3243917)CaDiCaL version: 2.1.3
% 279.76/40.40 % (3243917)Termination reason: Refutation not found, incomplete strategy
% 279.76/40.40 % (3243917)Time elapsed: 0.499 s
% 279.76/40.40 % (3243917)Peak memory usage: 127 MB
% 279.76/40.40 % (3243917)Instructions burned: 861 (million)
% 279.76/40.40 % (3243917)------------------------------
% 279.76/40.40 % (3243917)------------------------------
% 279.76/40.40 % (3243921)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:erd=off:urr=on:bsr=on:fd=preordered:random_seed=2050546324:i=19192:av=off_2676 on theBenchmark for (2676ds/19192Mi)
% 279.76/40.40 % (3243919)Instruction limit reached!
% 279.76/40.40 % (3243919)------------------------------
% 279.76/40.40 % (3243919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 279.76/40.40 % (3243919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 279.76/40.40 % (3243919)CaDiCaL version: 2.1.3
% 279.76/40.40 % (3243919)Termination reason: Instruction limit
% 279.76/40.40 % (3243919)Termination phase: Saturation
% 279.76/40.40 % (3243919)Time elapsed: 2.054 s
% 279.76/40.40 % (3243919)Peak memory usage: 185 MB
% 279.76/40.40 % (3243919)Instructions burned: 6465 (million)
% 279.76/40.40 % (3243924)lrs+10_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=8000:npcc=on:prc=on:fde=unused:sp=const_min:random_seed=2095663021:i=7136:fgj=on:bd=preordered:ins=3:ss=included_2660 on theBenchmark for (2660ds/7136Mi)
% 279.76/40.40 % (3243924)Instruction limit reached!
% 279.76/40.40 % (3243924)------------------------------
% 279.76/40.40 % (3243924)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 279.76/40.40 % (3243924)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 279.76/40.40 % (3243924)CaDiCaL version: 2.1.3
% 279.76/40.40 % (3243924)Termination reason: Instruction limit
% 279.76/40.40 % (3243924)Termination phase: Saturation
% 279.76/40.40 % (3243924)Time elapsed: 2.170 s
% 279.76/40.40 % (3243924)Peak memory usage: 180 MB
% 279.76/40.40 % (3243924)Instructions burned: 7139 (million)
% 279.76/40.40 % (3243926)ott-1004_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:tgt=full:npcc=on:sas=cadical:sp=const_frequency:acc=on:urr=ec_only:gs=on:s2agt=40:alpa=false:sac=on:random_seed=353331216:cts=off:cond=on:i=7540:bs=on:fsd=on_2634 on theBenchmark for (2634ds/7540Mi)
% 279.76/40.40 % (3243486)Instruction limit reached!
% 279.76/40.40 % (3243486)------------------------------
% 279.76/40.40 % (3243486)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 279.76/40.40 % (3243486)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 279.76/40.40 % (3243486)CaDiCaL version: 2.1.3
% 279.76/40.40 % (3243486)Termination reason: Instruction limit
% 279.76/40.40 % (3243486)Termination phase: Saturation
% 279.76/40.40 % (3243486)Time elapsed: 11.429 s
% 279.76/40.40 % (3243486)Peak memory usage: 299 MB
% 279.76/40.40 % (3243486)Instructions burned: 21998 (million)
% 279.76/40.40 % (3243928)ott+1011_1_to=lpo:ncem=casc2026/models/loop5.pt:sil=64000:tgt=ground:npcc=on:drc=off:sp=const_frequency:random_seed=4262389339:i=15570:s2at=5:gtgl=4:gtg=exists_sym_2626 on theBenchmark for (2626ds/15570Mi)
% 279.76/40.40 % (3243473)Instruction limit reached!
% 279.76/40.40 % (3243473)------------------------------
% 279.76/40.40 % (3243473)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 279.76/40.40 % (3243473)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 279.76/40.40 % (3243473)CaDiCaL version: 2.1.3
% 279.76/40.40 % (3243473)Termination reason: Instruction limit
% 279.76/40.40 % (3243473)Termination phase: Saturation
% 279.76/40.40 % (3243473)Time elapsed: 15.444 s
% 279.76/40.40 % (3243473)Peak memory usage: 377 MB
% 279.76/40.40 % (3243473)Instructions burned: 28652 (million)
% 279.76/40.40 % (3243930)lrs+1011_1_anc=none:to=lpo:ncem=casc2026/models/loop6.pt:sil=32000:tgt=full:npcc=on:sp=unary_first:spb=goal:lsd=20:bce=on:bsr=on:fd=preordered:gs=on:random_seed=3765100121:i=15957:add=on:fgj=on_2613 on theBenchmark for (2613ds/15957Mi)
% 279.76/40.40 % (3243926)Instruction limit reached!
% 279.76/40.40 % (3243926)------------------------------
% 279.76/40.40 % (3243926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 279.76/40.40 % (3243926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 279.76/40.40 % (3243926)CaDiCaL version: 2.1.3
% 279.76/40.40 % (3243926)Termination reason: Instruction limit
% 279.76/40.40 % (3243926)Termination phase: Saturation
% 279.76/40.40 % (3243926)Time elapsed: 2.304 s
% 279.76/40.40 % (3243926)Peak memory usage: 179 MB
% 279.76/40.40 % (3243926)Instructions burned: 7541 (million)
% 279.76/40.40 % (3242739)First to succeed.
% 279.76/40.40 % (3242739)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3242675"
% 279.76/40.40 % (3243932)lrs+1010_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=32000:tgt=full:npcc=on:prc=on:drc=ordering:fde=none:sp=arity:spb=intro:urr=ec_only:s2agt=40:random_seed=2490413617:cond=on:i=8289:erml=3:bd=preordered:er=filter:proc=on_2609 on theBenchmark for (2609ds/8289Mi)
% 279.76/40.40 % (3242739)Refutation found. Thanks to Tanya!
% 279.76/40.40 % SZS status Unsatisfiable for theBenchmark
% 279.76/40.40 % SZS output start Proof for theBenchmark
% See solution above
% 279.86/40.60 % (3242739)------------------------------
% 279.86/40.60 % (3242739)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 279.86/40.60 % (3242739)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 279.86/40.60 % (3242739)CaDiCaL version: 2.1.3
% 279.86/40.60 % (3242739)Termination reason: Refutation
% 279.86/40.60 % (3242739)Time elapsed: 38.867 s
% 279.86/40.60 % (3242739)Peak memory usage: 751 MB
% 279.86/40.60 % (3242739)Instructions burned: 70727 (million)
% 279.86/40.60 % (3242739)------------------------------
% 279.86/40.60 % (3242739)------------------------------
% 279.86/40.60 % (3242675)Success in time 39.518 s
% 279.86/40.60 % Vampire exiting
%------------------------------------------------------------------------------