%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP400-1 : TPTP v9.3.1. Released v2.5.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n012.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:13:51 AM UTC 2026
% Result : Unsatisfiable 40.42s 11.92s
% Output : Refutation 79.46s
% Verified :
% SZS Type : Refutation
% Derivation depth : 28
% Number of leaves : 6
% Syntax : Number of formulae : 120 ( 109 unt; 0 def)
% Number of atoms : 131 ( 130 equ)
% Maximal formula atoms : 2 ( 1 avg)
% Number of connectives : 36 ( 25 ~; 11 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 8 ( 2 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 286 ( 286 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X0,multiply(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_multiply) ).
fof(f2,axiom,
! [X2,X0,X1] :
( multiply(X0,X1) != multiply(X2,X1)
| X0 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',right_cancellation) ).
fof(f3,axiom,
! [X2,X0,X1] :
( multiply(X0,X1) != multiply(X0,X2)
| X1 = X2 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_cancellation) ).
fof(f4,axiom,
! [X0,X1] : multiply(X0,X1) = multiply(X1,multiply(X0,commutator(X0,X1))),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',commutator) ).
fof(f5,axiom,
! [X2,X0,X1] : commutator(commutator(X0,X1),X2) = commutator(X0,commutator(X1,X2)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',associativity_of_commutator) ).
fof(f6,negated_conjecture,
commutator(multiply(a,b),c) != multiply(commutator(a,c),commutator(b,c)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_commutator_distributes_over_product) ).
fof(f13,plain,
! [X2,X0,X1] : multiply(commutator(X0,X1),X2) = multiply(X2,multiply(commutator(X0,X1),commutator(X0,commutator(X1,X2)))),
inference(superposition,[],[f4,f5]) ).
fof(f14,plain,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X2,multiply(X0,multiply(X1,commutator(multiply(X0,X1),X2)))),
inference(superposition,[],[f4,f1]) ).
fof(f16,plain,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X1,multiply(multiply(X0,commutator(X0,X1)),X2)),
inference(superposition,[],[f1,f4]) ).
fof(f17,plain,
! [X2,X0,X1] : multiply(X0,multiply(X1,X2)) = multiply(X1,multiply(X2,multiply(X0,commutator(X0,multiply(X1,X2))))),
inference(superposition,[],[f1,f4]) ).
fof(f18,plain,
! [X2,X0,X1] : multiply(multiply(X0,X1),X2) = multiply(X1,multiply(X0,multiply(commutator(X0,X1),X2))),
inference(forward_demodulation,[],[f16,f1]) ).
fof(f19,plain,
! [X2,X0,X1] : multiply(X0,multiply(X1,X2)) = multiply(X2,multiply(X0,multiply(X1,commutator(multiply(X0,X1),X2)))),
inference(forward_demodulation,[],[f14,f1]) ).
fof(f20,plain,
! [X2,X0,X1] : multiply(X0,multiply(X1,X2)) = multiply(X1,multiply(X0,multiply(commutator(X0,X1),X2))),
inference(forward_demodulation,[],[f18,f1]) ).
fof(f26,plain,
! [X0] : multiply(X0,commutator(X0,X0)) = X0,
inference(unit_resulting_resolution,[],[f3,f4]) ).
fof(f30,plain,
! [X2,X3,X0,X1] :
( multiply(X0,multiply(X1,X2)) != multiply(multiply(X0,X1),X3)
| X2 = X3 ),
inference(superposition,[],[f3,f1]) ).
fof(f31,plain,
! [X2,X0,X1] :
( multiply(X0,X1) != multiply(X1,X2)
| multiply(X0,commutator(X0,X1)) = X2 ),
inference(superposition,[],[f3,f4]) ).
fof(f33,plain,
! [X2,X3,X0,X1] :
( multiply(X0,multiply(X1,X2)) != multiply(X0,multiply(X1,X3))
| X2 = X3 ),
inference(forward_demodulation,[],[f30,f1]) ).
fof(f38,plain,
! [X2,X0,X1] : multiply(X1,multiply(X2,multiply(X0,commutator(X0,commutator(X1,X2))))) = multiply(X2,multiply(X1,multiply(X0,commutator(X1,X2)))),
inference(superposition,[],[f20,f4]) ).
fof(f41,plain,
! [X0,X1] : multiply(X0,multiply(X1,commutator(commutator(X0,X1),X0))) = multiply(X1,multiply(commutator(X0,X1),X0)),
inference(superposition,[],[f20,f4]) ).
fof(f54,plain,
! [X0,X1] : multiply(X1,multiply(commutator(X0,X1),X0)) = multiply(X0,multiply(X1,commutator(X0,commutator(X1,X0)))),
inference(forward_demodulation,[],[f41,f5]) ).
fof(f65,plain,
! [X0,X1] : multiply(X0,multiply(X1,commutator(multiply(a,b),c))) != multiply(X0,multiply(X1,multiply(commutator(a,c),commutator(b,c)))),
inference(unit_resulting_resolution,[],[f33,f6]) ).
fof(f67,plain,
! [X0,X1] : multiply(commutator(X0,X0),X1) = X1,
inference(unit_resulting_resolution,[],[f33,f20]) ).
fof(f79,plain,
! [X2,X0,X1] :
( multiply(X0,X1) != multiply(X1,multiply(X0,X2))
| commutator(X0,X1) = X2 ),
inference(superposition,[],[f33,f4]) ).
fof(f80,plain,
! [X2,X3,X0,X1] :
( multiply(X0,multiply(X1,X2)) != multiply(X1,multiply(X0,X3))
| multiply(commutator(X0,X1),X2) = X3 ),
inference(superposition,[],[f33,f20]) ).
fof(f105,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X1,multiply(X0,commutator(multiply(X1,X0),X1))),
inference(unit_resulting_resolution,[],[f3,f19]) ).
fof(f118,plain,
! [X2,X3,X0,X1] :
( multiply(X0,multiply(X1,X2)) != multiply(X2,multiply(X0,X3))
| multiply(X1,commutator(multiply(X0,X1),X2)) = X3 ),
inference(superposition,[],[f33,f19]) ).
fof(f119,plain,
! [X2,X0,X1] : multiply(X0,multiply(X1,multiply(X2,commutator(multiply(commutator(X0,X1),X2),X0)))) = multiply(X1,multiply(commutator(X0,X1),multiply(X2,X0))),
inference(superposition,[],[f20,f19]) ).
fof(f357,plain,
! [X2,X0,X1] : multiply(multiply(X0,X1),multiply(commutator(X2,multiply(X0,X1)),X2)) = multiply(X2,multiply(X0,multiply(X1,commutator(X2,commutator(multiply(X0,X1),X2))))),
inference(superposition,[],[f54,f1]) ).
fof(f392,plain,
! [X2,X0,X1] : multiply(X2,multiply(X0,multiply(X1,commutator(X2,commutator(multiply(X0,X1),X2))))) = multiply(X0,multiply(X1,multiply(commutator(X2,multiply(X0,X1)),X2))),
inference(forward_demodulation,[],[f357,f1]) ).
fof(f532,plain,
! [X0,X1] : commutator(X0,X1) = multiply(commutator(X0,X1),commutator(X0,commutator(X1,commutator(X0,X1)))),
inference(unit_resulting_resolution,[],[f3,f13]) ).
fof(f605,plain,
multiply(a,multiply(c,commutator(b,c))) != multiply(c,multiply(a,commutator(multiply(a,b),c))),
inference(superposition,[],[f65,f20]) ).
fof(f623,plain,
! [X0] : multiply(multiply(a,multiply(c,commutator(b,c))),X0) != multiply(multiply(c,multiply(a,commutator(multiply(a,b),c))),X0),
inference(unit_resulting_resolution,[],[f2,f605]) ).
fof(f627,plain,
! [X0] : multiply(multiply(a,multiply(c,commutator(b,c))),X0) != multiply(c,multiply(multiply(a,commutator(multiply(a,b),c)),X0)),
inference(forward_demodulation,[],[f623,f1]) ).
fof(f629,plain,
! [X0] : multiply(multiply(a,multiply(c,commutator(b,c))),X0) != multiply(c,multiply(a,multiply(commutator(multiply(a,b),c),X0))),
inference(forward_demodulation,[],[f627,f1]) ).
fof(f631,plain,
! [X0] : multiply(c,multiply(a,multiply(commutator(multiply(a,b),c),X0))) != multiply(a,multiply(multiply(c,commutator(b,c)),X0)),
inference(forward_demodulation,[],[f629,f1]) ).
fof(f633,plain,
! [X0] : multiply(c,multiply(a,multiply(commutator(multiply(a,b),c),X0))) != multiply(a,multiply(c,multiply(commutator(b,c),X0))),
inference(forward_demodulation,[],[f631,f1]) ).
fof(f646,plain,
! [X0,X1] : multiply(commutator(X0,X1),X1) = multiply(X1,commutator(multiply(X0,X1),X1)),
inference(unit_resulting_resolution,[],[f80,f19]) ).
fof(f647,plain,
! [X0,X1] : multiply(commutator(X0,X1),X0) = multiply(X0,commutator(X0,multiply(X1,X0))),
inference(unit_resulting_resolution,[],[f80,f17]) ).
fof(f648,plain,
! [X2,X0,X1] : multiply(commutator(commutator(X0,X0),X1),multiply(commutator(X0,X0),X2)) = X2,
inference(unit_resulting_resolution,[],[f80,f67]) ).
fof(f653,plain,
! [X2,X0,X1] : multiply(commutator(X0,X0),X1) = multiply(commutator(X2,commutator(X0,X0)),X1),
inference(unit_resulting_resolution,[],[f80,f67]) ).
fof(f664,plain,
! [X2,X0,X1] :
( multiply(X0,X1) != multiply(X0,multiply(X1,X2))
| multiply(commutator(X1,X0),commutator(X0,X1)) = X2 ),
inference(superposition,[],[f80,f4]) ).
fof(f709,plain,
! [X2,X0,X1] : multiply(commutator(commutator(X0,X0),X1),X2) = X2,
inference(forward_demodulation,[],[f648,f67]) ).
fof(f713,plain,
! [X2,X0,X1] : multiply(commutator(X2,commutator(X0,X0)),X1) = X1,
inference(forward_demodulation,[],[f653,f67]) ).
fof(f719,plain,
! [X2,X0,X1] : multiply(commutator(X0,commutator(X0,X1)),X2) = X2,
inference(forward_demodulation,[],[f709,f5]) ).
fof(f807,plain,
! [X0,X1] : commutator(multiply(X0,X1),X1) = multiply(commutator(X0,X1),commutator(commutator(X0,X1),X1)),
inference(unit_resulting_resolution,[],[f31,f646]) ).
fof(f816,plain,
! [X0] : multiply(commutator(X0,commutator(X0,X0)),commutator(X0,X0)) = multiply(commutator(X0,X0),commutator(X0,commutator(X0,X0))),
inference(superposition,[],[f646,f26]) ).
fof(f844,plain,
! [X0] : commutator(X0,commutator(X0,X0)) = multiply(commutator(X0,commutator(X0,X0)),commutator(X0,X0)),
inference(forward_demodulation,[],[f816,f67]) ).
fof(f852,plain,
! [X0,X1] : commutator(multiply(X0,X1),X1) = multiply(commutator(X0,X1),commutator(X0,commutator(X1,X1))),
inference(forward_demodulation,[],[f807,f5]) ).
fof(f856,plain,
! [X0] : commutator(X0,X0) = commutator(X0,commutator(X0,X0)),
inference(forward_demodulation,[],[f844,f713]) ).
fof(f870,plain,
! [X0,X1] : multiply(commutator(X1,X0),commutator(X0,X0)) = multiply(commutator(X0,X0),multiply(commutator(X1,X0),commutator(X1,commutator(X0,X0)))),
inference(superposition,[],[f13,f856]) ).
fof(f879,plain,
! [X0,X1] : multiply(commutator(X1,X0),commutator(X0,X0)) = multiply(commutator(X1,X0),commutator(X1,commutator(X0,X0))),
inference(forward_demodulation,[],[f870,f67]) ).
fof(f887,plain,
! [X0,X1] : commutator(multiply(X1,X0),X0) = multiply(commutator(X1,X0),commutator(X0,X0)),
inference(forward_demodulation,[],[f879,f852]) ).
fof(f1320,plain,
! [X2,X0,X1] : multiply(X1,multiply(commutator(X1,X2),X0)) = multiply(commutator(X1,X2),multiply(X1,X0)),
inference(superposition,[],[f20,f719]) ).
fof(f1487,plain,
! [X2,X0,X1] : multiply(commutator(commutator(X0,X1),X0),X2) = X2,
inference(unit_resulting_resolution,[],[f80,f1320]) ).
fof(f1498,plain,
! [X0,X1] : multiply(commutator(X0,X1),X0) = multiply(X0,multiply(commutator(X0,X1),commutator(X0,X0))),
inference(superposition,[],[f1320,f26]) ).
fof(f1587,plain,
! [X2,X0,X1] : multiply(commutator(X0,commutator(X1,X0)),X2) = X2,
inference(forward_demodulation,[],[f1487,f5]) ).
fof(f1636,plain,
! [X2,X0,X1] : multiply(X1,multiply(commutator(X2,X1),X0)) = multiply(commutator(X2,X1),multiply(X1,X0)),
inference(superposition,[],[f20,f1587]) ).
fof(f2367,plain,
! [X0,X1] : commutator(X0,X0) = commutator(X1,commutator(X0,X0)),
inference(unit_resulting_resolution,[],[f79,f67]) ).
fof(f2369,plain,
! [X2,X0,X1] : commutator(X0,commutator(X1,X0)) = commutator(X2,commutator(X0,commutator(X1,X0))),
inference(unit_resulting_resolution,[],[f79,f1587]) ).
fof(f2426,plain,
! [X0,X1] : commutator(X0,X1) = multiply(commutator(X0,X1),commutator(X1,commutator(X0,X1))),
inference(backward_demodulation,[],[f532,f2369]) ).
fof(f2581,plain,
! [X0,X1] :
( multiply(X0,X1) != multiply(X0,X1)
| commutator(X0,X1) = commutator(multiply(X1,X0),X1) ),
inference(superposition,[],[f79,f105]) ).
fof(f2620,plain,
! [X0,X1] : commutator(X0,X1) = commutator(multiply(X1,X0),X1),
inference(trivial_inequality_removal,[],[f2581]) ).
fof(f2765,plain,
! [X2,X0,X1] : commutator(commutator(X0,X1),X2) = commutator(multiply(X1,X0),commutator(X1,X2)),
inference(superposition,[],[f5,f2620]) ).
fof(f2793,plain,
! [X2,X0,X1] : commutator(X0,commutator(X1,X2)) = commutator(multiply(X1,X0),commutator(X1,X2)),
inference(forward_demodulation,[],[f2765,f5]) ).
fof(f2850,plain,
! [X2,X0,X1] : commutator(multiply(X0,X1),commutator(X1,X2)) = commutator(multiply(X0,commutator(X0,X1)),commutator(X1,X2)),
inference(superposition,[],[f2793,f4]) ).
fof(f3331,plain,
! [X0,X1] :
( multiply(X1,X0) != multiply(X1,X0)
| commutator(X0,X0) = multiply(commutator(X0,X1),commutator(X1,X0)) ),
inference(superposition,[],[f664,f26]) ).
fof(f3352,plain,
! [X0,X1] : commutator(X0,X0) = multiply(commutator(X0,X1),commutator(X1,X0)),
inference(trivial_inequality_removal,[],[f3331]) ).
fof(f3425,plain,
! [X0,X1] : commutator(X0,X0) = commutator(commutator(X0,X1),X0),
inference(superposition,[],[f719,f3352]) ).
fof(f3463,plain,
! [X0,X1] : commutator(X0,X0) = commutator(X0,commutator(X1,X0)),
inference(forward_demodulation,[],[f3425,f5]) ).
fof(f3504,plain,
! [X0,X1] : commutator(X0,X1) = multiply(commutator(X0,X1),commutator(X1,X1)),
inference(backward_demodulation,[],[f2426,f3463]) ).
fof(f3513,plain,
! [X2,X0,X1] : multiply(X0,multiply(X1,multiply(commutator(X2,multiply(X0,X1)),X2))) = multiply(X2,multiply(X0,multiply(X1,commutator(X2,X2)))),
inference(backward_demodulation,[],[f392,f3463]) ).
fof(f3556,plain,
! [X0,X1] : commutator(X1,X0) = commutator(multiply(X1,X0),X0),
inference(backward_demodulation,[],[f887,f3504]) ).
fof(f3672,plain,
! [X0,X1] : commutator(X0,X0) = commutator(commutator(X1,X1),X0),
inference(superposition,[],[f3556,f67]) ).
fof(f3683,plain,
! [X2,X0,X1] : commutator(commutator(X0,X1),X2) = commutator(multiply(X0,X1),commutator(X1,X2)),
inference(superposition,[],[f5,f3556]) ).
fof(f3718,plain,
! [X2,X0,X1] : commutator(X0,commutator(X1,X2)) = commutator(multiply(X0,X1),commutator(X1,X2)),
inference(forward_demodulation,[],[f3683,f5]) ).
fof(f3726,plain,
! [X0,X1] : commutator(X0,X0) = commutator(X1,commutator(X1,X0)),
inference(forward_demodulation,[],[f3672,f5]) ).
fof(f3752,plain,
! [X2,X0,X1] : commutator(X0,commutator(X1,X2)) = commutator(multiply(X0,commutator(X0,X1)),commutator(X1,X2)),
inference(backward_demodulation,[],[f2850,f3718]) ).
fof(f4287,plain,
! [X2,X0,X1] : commutator(commutator(X1,X2),commutator(X1,X2)) = commutator(multiply(X0,X1),commutator(X0,commutator(X1,X2))),
inference(superposition,[],[f3726,f3718]) ).
fof(f4394,plain,
! [X2,X0,X1] : commutator(X1,commutator(X0,commutator(X1,X2))) = commutator(commutator(X1,X2),commutator(X1,X2)),
inference(forward_demodulation,[],[f4287,f2793]) ).
fof(f4415,plain,
! [X2,X0,X1] : commutator(X1,commutator(X0,commutator(X1,X2))) = commutator(X1,commutator(X2,commutator(X1,X2))),
inference(forward_demodulation,[],[f4394,f5]) ).
fof(f4424,plain,
! [X2,X0,X1] : commutator(X1,commutator(X2,X2)) = commutator(X1,commutator(X0,commutator(X1,X2))),
inference(forward_demodulation,[],[f4415,f3463]) ).
fof(f4430,plain,
! [X2,X0,X1] : commutator(X2,X2) = commutator(X2,commutator(X0,commutator(X1,X2))),
inference(superposition,[],[f3463,f5]) ).
fof(f4465,plain,
! [X0,X1] : commutator(multiply(X0,X1),multiply(X0,X1)) = commutator(X0,commutator(X1,multiply(X0,X1))),
inference(superposition,[],[f3718,f3463]) ).
fof(f4908,plain,
! [X2,X0,X1] : multiply(X2,multiply(X1,multiply(multiply(X0,commutator(X0,X1)),commutator(X1,X2)))) = multiply(X1,multiply(X2,multiply(multiply(X0,commutator(X0,X1)),commutator(X0,commutator(X1,X2))))),
inference(superposition,[],[f38,f3752]) ).
fof(f4951,plain,
! [X2,X0,X1] : multiply(X2,multiply(X1,multiply(multiply(X0,commutator(X0,X1)),commutator(X1,X2)))) = multiply(X1,multiply(X2,multiply(X0,multiply(commutator(X0,X1),commutator(X0,commutator(X1,X2)))))),
inference(forward_demodulation,[],[f4908,f1]) ).
fof(f4992,plain,
! [X2,X0,X1] : multiply(X1,multiply(X2,multiply(X0,multiply(commutator(X0,X1),commutator(X0,commutator(X1,X2)))))) = multiply(X2,multiply(X1,multiply(X0,multiply(commutator(X0,X1),commutator(X1,X2))))),
inference(forward_demodulation,[],[f4951,f1]) ).
fof(f5015,plain,
! [X2,X0,X1] : multiply(X2,multiply(X0,multiply(X1,commutator(X1,X2)))) = multiply(X1,multiply(X2,multiply(X0,multiply(commutator(X0,X1),commutator(X0,commutator(X1,X2)))))),
inference(forward_demodulation,[],[f4992,f20]) ).
fof(f10010,plain,
! [X2,X0,X1] : multiply(X2,multiply(commutator(commutator(X0,X1),X2),multiply(X0,commutator(X0,X1)))) = multiply(commutator(X0,X1),multiply(X2,multiply(X0,commutator(commutator(commutator(X0,X1),X2),commutator(X0,X1))))),
inference(superposition,[],[f119,f3718]) ).
fof(f10044,plain,
! [X2,X0,X1] : multiply(X0,multiply(X1,multiply(X2,commutator(multiply(commutator(X0,commutator(X0,X1)),X2),X0)))) = multiply(X1,multiply(commutator(X0,X1),multiply(commutator(X0,commutator(X0,X1)),multiply(X2,X0)))),
inference(superposition,[],[f20,f119]) ).
fof(f10113,plain,
! [X2,X0,X1] : multiply(X1,multiply(commutator(X0,X1),multiply(X2,X0))) = multiply(X0,multiply(X1,multiply(X2,commutator(multiply(commutator(X0,commutator(X0,X1)),X2),X0)))),
inference(forward_demodulation,[],[f10044,f719]) ).
fof(f10137,plain,
! [X2,X0,X1] : multiply(X2,multiply(commutator(commutator(X0,X1),X2),multiply(X0,commutator(X0,X1)))) = multiply(commutator(X0,X1),multiply(X2,multiply(X0,commutator(commutator(X0,X1),commutator(X2,commutator(X0,X1)))))),
inference(forward_demodulation,[],[f10010,f5]) ).
fof(f10206,plain,
! [X2,X0,X1] : multiply(X1,multiply(commutator(X0,X1),multiply(X2,X0))) = multiply(X0,multiply(X1,multiply(X2,commutator(X2,X0)))),
inference(forward_demodulation,[],[f10113,f719]) ).
fof(f10226,plain,
! [X2,X0,X1] : multiply(X2,multiply(commutator(commutator(X0,X1),X2),multiply(X0,commutator(X0,X1)))) = multiply(commutator(X0,X1),multiply(X2,multiply(X0,commutator(X0,commutator(X1,commutator(X2,commutator(X0,X1))))))),
inference(forward_demodulation,[],[f10137,f5]) ).
fof(f10300,plain,
! [X2,X0,X1] : multiply(X2,multiply(commutator(commutator(X0,X1),X2),multiply(X0,commutator(X0,X1)))) = multiply(commutator(X0,X1),multiply(X2,multiply(X0,commutator(X0,commutator(X1,X1))))),
inference(forward_demodulation,[],[f10226,f4430]) ).
fof(f10353,plain,
! [X2,X0,X1] : multiply(X2,multiply(commutator(commutator(X0,X1),X2),multiply(X0,commutator(X0,X1)))) = multiply(commutator(X0,X1),multiply(X2,multiply(X0,commutator(X1,X1)))),
inference(forward_demodulation,[],[f10300,f2367]) ).
fof(f10385,plain,
! [X2,X0,X1] : multiply(commutator(X0,X1),multiply(X2,multiply(X0,commutator(X1,X1)))) = multiply(X2,multiply(commutator(X0,commutator(X1,X2)),multiply(X0,commutator(X0,X1)))),
inference(forward_demodulation,[],[f10353,f5]) ).
fof(f10404,plain,
! [X2,X0,X1] : multiply(commutator(X0,X1),multiply(X2,multiply(X0,commutator(X1,X1)))) = multiply(X2,multiply(X0,multiply(commutator(X0,commutator(X1,X2)),commutator(X0,X1)))),
inference(forward_demodulation,[],[f10385,f1320]) ).
fof(f10795,plain,
! [X0,X1] : multiply(X0,commutator(multiply(X1,X0),multiply(X1,X0))) = X0,
inference(unit_resulting_resolution,[],[f118,f1]) ).
fof(f10925,plain,
! [X0,X1] : multiply(X0,commutator(X1,commutator(X0,multiply(X1,X0)))) = X0,
inference(forward_demodulation,[],[f10795,f4465]) ).
fof(f20983,plain,
! [X2,X3,X0,X1] : multiply(commutator(X2,X0),commutator(X3,commutator(X0,X1))) = multiply(commutator(X3,commutator(X0,X1)),multiply(commutator(X2,X0),commutator(X2,commutator(X0,commutator(X1,X1))))),
inference(superposition,[],[f13,f4424]) ).
fof(f21097,plain,
! [X2,X3,X0,X1] : multiply(commutator(X2,X0),commutator(X3,commutator(X0,X1))) = multiply(commutator(X3,commutator(X0,X1)),multiply(commutator(X2,X0),commutator(X2,commutator(X1,X1)))),
inference(forward_demodulation,[],[f20983,f2367]) ).
fof(f21307,plain,
! [X2,X3,X0,X1] : multiply(commutator(X2,X0),commutator(X3,commutator(X0,X1))) = multiply(commutator(X3,commutator(X0,X1)),multiply(commutator(X2,X0),commutator(X1,X1))),
inference(forward_demodulation,[],[f21097,f2367]) ).
fof(f23574,plain,
! [X0,X1] : multiply(commutator(X0,X1),multiply(X0,commutator(X0,X0))) = multiply(commutator(X0,multiply(X1,X0)),X0),
inference(unit_resulting_resolution,[],[f80,f3513]) ).
fof(f23992,plain,
! [X0,X1] : multiply(X0,multiply(commutator(X0,X1),commutator(X0,X0))) = multiply(commutator(X0,multiply(X1,X0)),X0),
inference(forward_demodulation,[],[f23574,f1320]) ).
fof(f24122,plain,
! [X0,X1] : multiply(commutator(X0,X1),X0) = multiply(commutator(X0,multiply(X1,X0)),X0),
inference(forward_demodulation,[],[f23992,f1498]) ).
fof(f24385,plain,
! [X0,X1] : commutator(X0,X1) = commutator(X0,multiply(X1,X0)),
inference(unit_resulting_resolution,[],[f2,f24122]) ).
fof(f24570,plain,
! [X0,X1] : multiply(X0,commutator(X0,X1)) = multiply(commutator(X0,X1),X0),
inference(backward_demodulation,[],[f647,f24385]) ).
fof(f24588,plain,
! [X0,X1] : multiply(X0,commutator(X1,commutator(X0,X1))) = X0,
inference(backward_demodulation,[],[f10925,f24385]) ).
fof(f24764,plain,
! [X0,X1] : multiply(X0,commutator(X1,X1)) = X0,
inference(forward_demodulation,[],[f24588,f3463]) ).
fof(f25238,plain,
! [X2,X0,X1] : multiply(commutator(X0,X1),multiply(X2,X0)) = multiply(X2,multiply(X0,multiply(commutator(X0,commutator(X1,X2)),commutator(X0,X1)))),
inference(backward_demodulation,[],[f10404,f24764]) ).
fof(f25439,plain,
! [X2,X3,X0,X1] : multiply(commutator(X2,X0),commutator(X3,commutator(X0,X1))) = multiply(commutator(X3,commutator(X0,X1)),commutator(X2,X0)),
inference(backward_demodulation,[],[f21307,f24764]) ).
fof(f26275,plain,
! [X2,X0,X1] : multiply(commutator(X0,X1),multiply(X2,X0)) = multiply(X2,multiply(X0,multiply(commutator(X0,X1),commutator(X0,commutator(X1,X2))))),
inference(forward_demodulation,[],[f25238,f25439]) ).
fof(f26798,plain,
! [X2,X0,X1] : multiply(X1,multiply(commutator(X0,X1),multiply(X2,X0))) = multiply(X2,multiply(X0,multiply(X1,commutator(X1,X2)))),
inference(backward_demodulation,[],[f5015,f26275]) ).
fof(f33757,plain,
multiply(a,multiply(c,multiply(commutator(b,c),multiply(a,b)))) != multiply(c,multiply(a,multiply(multiply(a,b),commutator(multiply(a,b),c)))),
inference(superposition,[],[f633,f24570]) ).
fof(f33909,plain,
multiply(a,multiply(c,multiply(commutator(b,c),multiply(a,b)))) != multiply(a,multiply(commutator(c,a),multiply(multiply(a,b),c))),
inference(forward_demodulation,[],[f33757,f10206]) ).
fof(f33977,plain,
multiply(a,multiply(c,multiply(commutator(b,c),multiply(a,b)))) != multiply(a,multiply(commutator(c,a),multiply(a,multiply(b,c)))),
inference(forward_demodulation,[],[f33909,f1]) ).
fof(f34008,plain,
multiply(a,multiply(c,multiply(commutator(b,c),multiply(a,b)))) != multiply(a,multiply(a,multiply(commutator(c,a),multiply(b,c)))),
inference(forward_demodulation,[],[f33977,f1636]) ).
fof(f34019,plain,
multiply(a,multiply(b,multiply(c,multiply(a,commutator(a,b))))) != multiply(a,multiply(a,multiply(commutator(c,a),multiply(b,c)))),
inference(forward_demodulation,[],[f34008,f10206]) ).
fof(f34027,plain,
multiply(a,multiply(a,multiply(commutator(c,a),multiply(b,c)))) != multiply(a,multiply(a,multiply(commutator(c,a),multiply(b,c)))),
inference(forward_demodulation,[],[f34019,f26798]) ).
fof(f34028,plain,
$false,
inference(trivial_inequality_removal,[],[f34027]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP400-1 : TPTP v9.3.1. Released v2.5.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.06/0.33 % Computer : n012.cluster.edu
% 0.06/0.33 % Model : x86_64 x86_64
% 0.06/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.06/0.33 % Memory : 8046.5625MB
% 0.06/0.33 % OS : Linux 6.8.0-71-generic
% 0.06/0.33 % CPULimit : 300
% 0.06/0.33 % WCLimit : 300
% 0.06/0.33 % DateTime : Sun Sep 27 10:01:35 UTC 2026
% 0.06/0.33 % CPUTime :
% 0.06/0.33 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.36 Running first-order theorem proving
% 0.10/0.36 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 14.16/2.70 % (2132560)Input is clausal, will run a generic CNF schedule.
% 14.16/2.70 % (2132568)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1240915685:i=132376:av=off_3000 on theBenchmark for (3000ds/132376Mi)
% 14.16/2.70 % (2132567)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=3703100299:i=140167_3000 on theBenchmark for (3000ds/140167Mi)
% 14.16/2.70 % (2132570)lrs+10_1_sil=8000:sp=occurrence:random_seed=3220477858:i=107:sd=3:ss=axioms:sgt=8_3000 on theBenchmark for (3000ds/107Mi)
% 14.16/2.70 % (2132569)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=603699790:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_3000 on theBenchmark for (3000ds/137899Mi)
% 14.16/2.70 % (2132572)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1194228146:s2a=on:i=180:gtg=position_3000 on theBenchmark for (3000ds/180Mi)
% 14.16/2.70 % (2132571)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=154447227:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_3000 on theBenchmark for (3000ds/114Mi)
% 14.16/2.70 % (2132570)Instruction limit reached!
% 14.16/2.70 % (2132570)------------------------------
% 14.16/2.70 % (2132570)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.16/2.70 % (2132570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.16/2.70 % (2132570)CaDiCaL version: 2.1.3
% 14.16/2.70 % (2132570)Termination reason: Instruction limit
% 14.16/2.70 % (2132570)Termination phase: Saturation
% 14.16/2.70 % (2132570)Time elapsed: 0.057 s
% 14.16/2.70 % (2132570)Peak memory usage: 88 MB
% 14.16/2.70 % (2132570)Instructions burned: 109 (million)
% 14.16/2.70 % (2132573)dis-21_1_sil=8000:lcm=predicate:random_seed=3413842443:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_3000 on theBenchmark for (3000ds/117Mi)
% 14.16/2.70 % (2132573)Refutation not found, incomplete strategy
% 14.16/2.70 % (2132573)------------------------------
% 14.16/2.70 % (2132573)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.16/2.70 % (2132573)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.16/2.70 % (2132573)CaDiCaL version: 2.1.3
% 14.16/2.70 % (2132573)Termination reason: Refutation not found, incomplete strategy
% 14.16/2.70 % (2132573)Time elapsed: 0.002 s
% 14.16/2.70 % (2132573)Peak memory usage: 88 MB
% 14.16/2.70 % (2132571)Instruction limit reached!
% 14.16/2.70 % (2132571)------------------------------
% 14.16/2.70 % (2132571)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.16/2.70 % (2132571)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.16/2.70 % (2132571)CaDiCaL version: 2.1.3
% 14.16/2.70 % (2132571)Termination reason: Instruction limit
% 14.16/2.70 % (2132571)Termination phase: Saturation
% 14.16/2.70 % (2132571)Time elapsed: 0.064 s
% 14.16/2.70 % (2132571)Peak memory usage: 88 MB
% 14.16/2.70 % (2132571)Instructions burned: 114 (million)
% 14.16/2.70 % (2132572)Instruction limit reached!
% 14.16/2.70 % (2132572)------------------------------
% 14.16/2.70 % (2132572)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.16/2.70 % (2132572)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.16/2.70 % (2132572)CaDiCaL version: 2.1.3
% 14.16/2.70 % (2132572)Termination reason: Instruction limit
% 14.16/2.70 % (2132572)Termination phase: Saturation
% 14.16/2.70 % (2132572)Time elapsed: 0.091 s
% 14.16/2.70 % (2132572)Peak memory usage: 89 MB
% 14.16/2.70 % (2132572)Instructions burned: 182 (million)
% 14.16/2.70 % (2132582)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2614984001:st=3:avsq=on:s2a=on:i=189:s2at=1.2:avsqr=1,16:sd=2:bd=all:nm=64:ss=axioms:sgt=30_2997 on theBenchmark for (2997ds/189Mi)
% 14.16/2.70 % (2132573)------------------------------
% 14.16/2.70 % (2132573)------------------------------
% 14.16/2.70 % (2132581)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=2749912266:i=143:sd=2:aac=none:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/143Mi)
% 14.16/2.70 % (2132581)Refutation not found, incomplete strategy
% 14.16/2.70 % (2132581)------------------------------
% 14.16/2.70 % (2132581)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.16/2.70 % (2132581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.20/3.97 % (2132581)CaDiCaL version: 2.1.3
% 22.20/3.97 % (2132581)Termination reason: Refutation not found, incomplete strategy
% 22.20/3.97 % (2132581)Time elapsed: 0.001 s
% 22.20/3.97 % (2132581)Peak memory usage: 87 MB
% 22.20/3.97 % (2132582)Instruction limit reached!
% 22.20/3.97 % (2132582)------------------------------
% 22.20/3.97 % (2132582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.20/3.97 % (2132582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.20/3.97 % (2132582)CaDiCaL version: 2.1.3
% 22.20/3.97 % (2132582)Termination reason: Instruction limit
% 22.20/3.97 % (2132582)Termination phase: Saturation
% 22.20/3.97 % (2132582)Time elapsed: 0.104 s
% 22.20/3.97 % (2132582)Peak memory usage: 89 MB
% 22.20/3.97 % (2132582)Instructions burned: 191 (million)
% 22.20/3.97 % (2132583)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=756377566:st=4:i=219:sd=3:ss=axioms_2997 on theBenchmark for (2997ds/219Mi)
% 22.20/3.97 % (2132583)Refutation not found, incomplete strategy
% 22.20/3.97 % (2132583)------------------------------
% 22.20/3.97 % (2132583)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.20/3.97 % (2132583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.20/3.97 % (2132583)CaDiCaL version: 2.1.3
% 22.20/3.97 % (2132583)Termination reason: Refutation not found, incomplete strategy
% 22.20/3.97 % (2132583)Time elapsed: 0.001 s
% 22.20/3.97 % (2132583)Peak memory usage: 87 MB
% 22.20/3.97 % (2132586)lrs+10_64_to=lpo:sil=8000:random_seed=4098861217:i=126:bd=preordered_2995 on theBenchmark for (2995ds/126Mi)
% 22.20/3.97 % (2132587)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1475172612:avsq=on:i=194:fgj=on:bd=preordered_2995 on theBenchmark for (2995ds/194Mi)
% 22.20/3.97 % (2132581)------------------------------
% 22.20/3.97 % (2132581)------------------------------
% 22.20/3.97 % (2132586)Instruction limit reached!
% 22.20/3.97 % (2132586)------------------------------
% 22.20/3.97 % (2132586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.20/3.97 % (2132586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.20/3.97 % (2132586)CaDiCaL version: 2.1.3
% 22.20/3.97 % (2132586)Termination reason: Instruction limit
% 22.20/3.97 % (2132586)Termination phase: Saturation
% 22.20/3.97 % (2132586)Time elapsed: 0.065 s
% 22.20/3.97 % (2132586)Peak memory usage: 87 MB
% 22.20/3.97 % (2132586)Instructions burned: 127 (million)
% 22.20/3.97 % (2132583)------------------------------
% 22.20/3.97 % (2132583)------------------------------
% 22.20/3.97 % (2132587)Instruction limit reached!
% 22.20/3.97 % (2132587)------------------------------
% 22.20/3.97 % (2132587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.20/3.97 % (2132587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.20/3.97 % (2132587)CaDiCaL version: 2.1.3
% 22.20/3.97 % (2132587)Termination reason: Instruction limit
% 22.20/3.97 % (2132587)Termination phase: Saturation
% 22.20/3.97 % (2132587)Time elapsed: 0.109 s
% 22.20/3.97 % (2132587)Peak memory usage: 88 MB
% 22.20/3.97 % (2132587)Instructions burned: 194 (million)
% 22.20/3.97 % (2132591)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=4249721829:i=157:gtg=all_2993 on theBenchmark for (2993ds/157Mi)
% 22.20/3.97 % (2132594)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=2674553867:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2992 on theBenchmark for (2992ds/106Mi)
% 22.20/3.97 % (2132593)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=3792859737:i=3394:sd=4:ss=included:sgt=64_2992 on theBenchmark for (2992ds/3394Mi)
% 22.20/3.97 % (2132594)Instruction limit reached!
% 22.20/3.97 % (2132594)------------------------------
% 22.20/3.97 % (2132594)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.20/3.97 % (2132594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.20/3.97 % (2132594)CaDiCaL version: 2.1.3
% 22.20/3.97 % (2132594)Termination reason: Instruction limit
% 22.20/3.97 % (2132594)Termination phase: Saturation
% 22.20/3.97 % (2132594)Time elapsed: 0.045 s
% 22.20/3.97 % (2132594)Peak memory usage: 89 MB
% 22.20/3.97 % (2132594)Instructions burned: 107 (million)
% 22.20/3.97 % (2132591)Instruction limit reached!
% 22.20/3.97 % (2132591)------------------------------
% 22.20/3.97 % (2132591)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.20/3.97 % (2132591)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.50/5.65 % (2132591)CaDiCaL version: 2.1.3
% 34.50/5.65 % (2132591)Termination reason: Instruction limit
% 34.50/5.65 % (2132591)Termination phase: Saturation
% 34.50/5.65 % (2132591)Time elapsed: 0.087 s
% 34.50/5.65 % (2132591)Peak memory usage: 90 MB
% 34.50/5.65 % (2132591)Instructions burned: 158 (million)
% 34.50/5.65 % (2132595)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=2500307665:i=107_2992 on theBenchmark for (2992ds/107Mi)
% 34.50/5.65 % (2132595)Refutation not found, incomplete strategy
% 34.50/5.65 % (2132595)------------------------------
% 34.50/5.65 % (2132595)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.50/5.65 % (2132595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.50/5.65 % (2132595)CaDiCaL version: 2.1.3
% 34.50/5.65 % (2132595)Termination reason: Refutation not found, incomplete strategy
% 34.50/5.65 % (2132595)Time elapsed: 0.001 s
% 34.50/5.65 % (2132595)Peak memory usage: 87 MB
% 34.50/5.65 % (2132602)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=2430583884:cond=fast:i=5208:av=off_2990 on theBenchmark for (2990ds/5208Mi)
% 34.50/5.65 % (2132601)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=2495390049:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2990 on theBenchmark for (2990ds/242Mi)
% 34.50/5.65 % (2132595)------------------------------
% 34.50/5.65 % (2132595)------------------------------
% 34.50/5.65 % (2132601)Instruction limit reached!
% 34.50/5.65 % (2132601)------------------------------
% 34.50/5.65 % (2132601)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.50/5.65 % (2132601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.50/5.65 % (2132601)CaDiCaL version: 2.1.3
% 34.50/5.65 % (2132601)Termination reason: Instruction limit
% 34.50/5.65 % (2132601)Termination phase: Saturation
% 34.50/5.65 % (2132601)Time elapsed: 0.130 s
% 34.50/5.65 % (2132601)Peak memory usage: 90 MB
% 34.50/5.65 % (2132601)Instructions burned: 242 (million)
% 34.50/5.65 % (2132606)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3043097711:i=134:sd=2:doe=on:ss=axioms:sgt=14_2987 on theBenchmark for (2987ds/134Mi)
% 34.50/5.65 % (2132606)Instruction limit reached!
% 34.50/5.65 % (2132606)------------------------------
% 34.50/5.65 % (2132606)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.50/5.65 % (2132606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.50/5.65 % (2132606)CaDiCaL version: 2.1.3
% 34.50/5.65 % (2132606)Termination reason: Instruction limit
% 34.50/5.65 % (2132606)Termination phase: Saturation
% 34.50/5.65 % (2132606)Time elapsed: 0.073 s
% 34.50/5.65 % (2132606)Peak memory usage: 89 MB
% 34.50/5.65 % (2132606)Instructions burned: 136 (million)
% 34.50/5.65 % (2132607)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=2287685049:i=499:bd=all_2986 on theBenchmark for (2986ds/499Mi)
% 34.50/5.65 % (2132610)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=180299004:i=191:fgj=on:bd=all_2985 on theBenchmark for (2985ds/191Mi)
% 34.50/5.65 % (2132610)Instruction limit reached!
% 34.50/5.65 % (2132610)------------------------------
% 34.50/5.65 % (2132610)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.50/5.65 % (2132610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.50/5.65 % (2132610)CaDiCaL version: 2.1.3
% 34.50/5.65 % (2132610)Termination reason: Instruction limit
% 34.50/5.65 % (2132610)Termination phase: Saturation
% 34.50/5.65 % (2132610)Time elapsed: 0.098 s
% 34.50/5.65 % (2132610)Peak memory usage: 89 MB
% 34.50/5.65 % (2132610)Instructions burned: 192 (million)
% 34.50/5.65 % (2132607)Instruction limit reached!
% 34.50/5.65 % (2132607)------------------------------
% 34.50/5.65 % (2132607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 34.50/5.65 % (2132607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 34.50/5.65 % (2132607)CaDiCaL version: 2.1.3
% 34.50/5.65 % (2132607)Termination reason: Instruction limit
% 34.50/5.65 % (2132607)Termination phase: Saturation
% 34.50/5.65 % (2132607)Time elapsed: 0.258 s
% 34.50/5.65 % (2132607)Peak memory usage: 92 MB
% 34.50/5.65 % (2132607)Instructions burned: 500 (million)
% 34.50/5.65 % (2132613)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2304533054:i=264:kws=precedence:fsr=off_2981 on theBenchmark for (2981ds/264Mi)
% 60.96/9.31 % (2132614)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=4137734403:cond=on:i=156:bs=on:gtg=exists_all:er=known_2981 on theBenchmark for (2981ds/156Mi)
% 60.96/9.31 % (2132614)Instruction limit reached!
% 60.96/9.31 % (2132614)------------------------------
% 60.96/9.31 % (2132614)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.96/9.31 % (2132614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.96/9.31 % (2132614)CaDiCaL version: 2.1.3
% 60.96/9.31 % (2132614)Termination reason: Instruction limit
% 60.96/9.31 % (2132614)Termination phase: Saturation
% 60.96/9.31 % (2132614)Time elapsed: 0.088 s
% 60.96/9.31 % (2132614)Peak memory usage: 88 MB
% 60.96/9.31 % (2132614)Instructions burned: 156 (million)
% 60.96/9.31 % (2132613)Instruction limit reached!
% 60.96/9.31 % (2132613)------------------------------
% 60.96/9.31 % (2132613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.96/9.31 % (2132613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.96/9.31 % (2132613)CaDiCaL version: 2.1.3
% 60.96/9.31 % (2132613)Termination reason: Instruction limit
% 60.96/9.31 % (2132613)Termination phase: Saturation
% 60.96/9.31 % (2132613)Time elapsed: 0.139 s
% 60.96/9.31 % (2132613)Peak memory usage: 91 MB
% 60.96/9.31 % (2132613)Instructions burned: 264 (million)
% 60.96/9.31 % (2132619)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=1349942866:i=3256:kws=precedence:bd=preordered:av=off_2978 on theBenchmark for (2978ds/3256Mi)
% 60.96/9.31 % (2132620)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=1196796921:i=537:av=off:ss=included_2978 on theBenchmark for (2978ds/537Mi)
% 60.96/9.31 % (2132620)Instruction limit reached!
% 60.96/9.31 % (2132620)------------------------------
% 60.96/9.31 % (2132620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.96/9.31 % (2132620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.96/9.31 % (2132620)CaDiCaL version: 2.1.3
% 60.96/9.31 % (2132620)Termination reason: Instruction limit
% 60.96/9.31 % (2132620)Termination phase: Saturation
% 60.96/9.31 % (2132620)Time elapsed: 0.283 s
% 60.96/9.31 % (2132620)Peak memory usage: 94 MB
% 60.96/9.31 % (2132620)Instructions burned: 537 (million)
% 60.96/9.31 % (2132593)Instruction limit reached!
% 60.96/9.31 % (2132593)------------------------------
% 60.96/9.31 % (2132593)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.96/9.31 % (2132593)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.96/9.31 % (2132593)CaDiCaL version: 2.1.3
% 60.96/9.31 % (2132593)Termination reason: Instruction limit
% 60.96/9.31 % (2132593)Termination phase: Saturation
% 60.96/9.31 % (2132593)Time elapsed: 1.880 s
% 60.96/9.31 % (2132593)Peak memory usage: 146 MB
% 60.96/9.31 % (2132593)Instructions burned: 3395 (million)
% 60.96/9.31 % (2132623)ott+1010_32_to=lpo:sil=8000:urr=on:nwc=4:random_seed=3682199061:i=180:bd=preordered:av=off_2972 on theBenchmark for (2972ds/180Mi)
% 60.96/9.31 % (2132623)Instruction limit reached!
% 60.96/9.31 % (2132623)------------------------------
% 60.96/9.31 % (2132623)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.96/9.31 % (2132623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 60.96/9.31 % (2132623)CaDiCaL version: 2.1.3
% 60.96/9.31 % (2132623)Termination reason: Instruction limit
% 60.96/9.31 % (2132623)Termination phase: Saturation
% 60.96/9.31 % (2132623)Time elapsed: 0.056 s
% 60.96/9.31 % (2132623)Peak memory usage: 88 MB
% 60.96/9.31 % (2132623)Instructions burned: 182 (million)
% 60.96/9.31 % (2132624)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=1981333535:i=10307:s2at=3:bs=on:bd=preordered:fsd=on_2971 on theBenchmark for (2971ds/10307Mi)
% 60.96/9.31 % (2132626)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=3362887488:i=412:gtgl=4:gtg=exists_all_2970 on theBenchmark for (2970ds/412Mi)
% 60.96/9.31 % (2132626)Instruction limit reached!
% 60.96/9.31 % (2132626)------------------------------
% 60.96/9.31 % (2132626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 60.96/9.31 % (2132626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.21/11.78 % (2132626)CaDiCaL version: 2.1.3
% 77.21/11.78 % (2132626)Termination reason: Instruction limit
% 77.21/11.78 % (2132626)Termination phase: Saturation
% 77.21/11.78 % (2132626)Time elapsed: 0.216 s
% 77.21/11.78 % (2132626)Peak memory usage: 94 MB
% 77.21/11.78 % (2132626)Instructions burned: 413 (million)
% 77.21/11.78 % (2132629)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=1152363142:s2pl=no:i=8478:s2at=4:nm=6_2966 on theBenchmark for (2966ds/8478Mi)
% 77.21/11.78 % (2132602)Instruction limit reached!
% 77.21/11.78 % (2132602)------------------------------
% 77.21/11.78 % (2132602)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.21/11.78 % (2132602)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.21/11.78 % (2132602)CaDiCaL version: 2.1.3
% 77.21/11.78 % (2132602)Termination reason: Instruction limit
% 77.21/11.78 % (2132602)Termination phase: Saturation
% 77.21/11.78 % (2132602)Time elapsed: 2.616 s
% 77.21/11.78 % (2132602)Peak memory usage: 159 MB
% 77.21/11.78 % (2132602)Instructions burned: 5208 (million)
% 77.21/11.78 % (2132631)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=430326091:s2a=on:i=303:s2at=2:sd=1:kws=inv_arity:bs=on:ins=10:fdi=1024:sup=off:ss=included_2962 on theBenchmark for (2962ds/303Mi)
% 77.21/11.78 % (2132631)Instruction limit reached!
% 77.21/11.78 % (2132631)------------------------------
% 77.21/11.78 % (2132631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.21/11.78 % (2132631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.21/11.78 % (2132631)CaDiCaL version: 2.1.3
% 77.21/11.78 % (2132631)Termination reason: Instruction limit
% 77.21/11.78 % (2132631)Termination phase: Saturation
% 77.21/11.78 % (2132631)Time elapsed: 0.145 s
% 77.21/11.78 % (2132631)Peak memory usage: 90 MB
% 77.21/11.78 % (2132631)Instructions burned: 303 (million)
% 77.21/11.78 % (2132619)Instruction limit reached!
% 77.21/11.78 % (2132619)------------------------------
% 77.21/11.78 % (2132619)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.21/11.78 % (2132619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.21/11.78 % (2132619)CaDiCaL version: 2.1.3
% 77.21/11.78 % (2132619)Termination reason: Instruction limit
% 77.21/11.78 % (2132619)Termination phase: Saturation
% 77.21/11.78 % (2132619)Time elapsed: 1.842 s
% 77.21/11.78 % (2132619)Peak memory usage: 147 MB
% 77.21/11.78 % (2132619)Instructions burned: 3258 (million)
% 77.21/11.78 % (2132633)lrs+10_1_to=lpo:sil=16000:fde=none:sos=on:urr=on:bsr=on:random_seed=4132801617:st=4:i=720:sd=3:fsr=off:ss=axioms_2958 on theBenchmark for (2958ds/720Mi)
% 77.21/11.78 % (2132634)lrs-20_1_to=lpo:sil=32000:tgt=ground:sp=reverse_frequency:spb=goal:urr=on:bsr=unit_only:nwc=1.5:random_seed=996424049:i=598:bs=on:bd=preordered:av=off:ss=axioms_2958 on theBenchmark for (2958ds/598Mi)
% 77.21/11.78 % (2132633)Instruction limit reached!
% 77.21/11.78 % (2132633)------------------------------
% 77.21/11.78 % (2132633)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.21/11.78 % (2132633)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.21/11.78 % (2132633)CaDiCaL version: 2.1.3
% 77.21/11.78 % (2132633)Termination reason: Instruction limit
% 77.21/11.78 % (2132633)Termination phase: Saturation
% 77.21/11.78 % (2132633)Time elapsed: 0.347 s
% 77.21/11.78 % (2132633)Peak memory usage: 94 MB
% 77.21/11.78 % (2132633)Instructions burned: 720 (million)
% 77.21/11.78 % (2132634)Instruction limit reached!
% 77.21/11.78 % (2132634)------------------------------
% 77.21/11.78 % (2132634)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 77.21/11.78 % (2132634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 77.21/11.78 % (2132634)CaDiCaL version: 2.1.3
% 77.21/11.78 % (2132634)Termination reason: Instruction limit
% 77.21/11.78 % (2132634)Termination phase: Saturation
% 77.21/11.78 % (2132634)Time elapsed: 0.353 s
% 77.21/11.78 % (2132634)Peak memory usage: 93 MB
% 77.21/11.78 % (2132634)Instructions burned: 600 (million)
% 77.21/11.78 % (2132637)dis-1010_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:sp=occurrence:random_seed=1309656128:i=2989:sd=3:ss=axioms:sgt=60_2952 on theBenchmark for (2952ds/2989Mi)
% 77.21/11.78 % (2132638)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=3766925638:i=1997:bd=preordered:av=off:gtg=all:gsp=on_2952 on theBenchmark for (2952ds/1997Mi)
% 40.42/11.92 % (2132638)Instruction limit reached!
% 40.42/11.92 % (2132638)------------------------------
% 40.42/11.92 % (2132638)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.42/11.92 % (2132638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.42/11.92 % (2132638)CaDiCaL version: 2.1.3
% 40.42/11.92 % (2132638)Termination reason: Instruction limit
% 40.42/11.92 % (2132638)Termination phase: Saturation
% 40.42/11.92 % (2132638)Time elapsed: 0.910 s
% 40.42/11.92 % (2132638)Peak memory usage: 138 MB
% 40.42/11.92 % (2132638)Instructions burned: 1998 (million)
% 40.42/11.92 % (2132641)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=1289600360:i=2088:bd=preordered:av=off_2940 on theBenchmark for (2940ds/2088Mi)
% 40.42/11.92 % (2132637)Instruction limit reached!
% 40.42/11.92 % (2132637)------------------------------
% 40.42/11.92 % (2132637)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.42/11.92 % (2132637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.42/11.92 % (2132637)CaDiCaL version: 2.1.3
% 40.42/11.92 % (2132637)Termination reason: Instruction limit
% 40.42/11.92 % (2132637)Termination phase: Saturation
% 40.42/11.92 % (2132637)Time elapsed: 1.616 s
% 40.42/11.92 % (2132637)Peak memory usage: 147 MB
% 40.42/11.92 % (2132637)Instructions burned: 2990 (million)
% 40.42/11.92 % (2132644)lrs+1010_64:1_anc=all:to=lpo:sil=16000:fde=none:sp=const_frequency:urr=full:sac=on:random_seed=864762065:i=1098:nicw=on_2934 on theBenchmark for (2934ds/1098Mi)
% 40.42/11.92 % (2132641)Instruction limit reached!
% 40.42/11.92 % (2132641)------------------------------
% 40.42/11.92 % (2132641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.42/11.92 % (2132641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.42/11.92 % (2132641)CaDiCaL version: 2.1.3
% 40.42/11.92 % (2132641)Termination reason: Instruction limit
% 40.42/11.92 % (2132641)Termination phase: Saturation
% 40.42/11.92 % (2132641)Time elapsed: 1.171 s
% 40.42/11.92 % (2132641)Peak memory usage: 137 MB
% 40.42/11.92 % (2132641)Instructions burned: 2089 (million)
% 40.42/11.92 % (2132644)Instruction limit reached!
% 40.42/11.92 % (2132644)------------------------------
% 40.42/11.92 % (2132644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.42/11.92 % (2132644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.42/11.92 % (2132644)CaDiCaL version: 2.1.3
% 40.42/11.92 % (2132644)Termination reason: Instruction limit
% 40.42/11.92 % (2132644)Termination phase: Saturation
% 40.42/11.92 % (2132644)Time elapsed: 0.603 s
% 40.42/11.92 % (2132644)Peak memory usage: 100 MB
% 40.42/11.92 % (2132644)Instructions burned: 1098 (million)
% 40.42/11.92 % (2132647)lrs-1011_32:1_to=lpo:sil=32000:tgt=ground:sos=on:spb=goal_then_units:acc=on:random_seed=4023056099:i=433:bd=preordered_2926 on theBenchmark for (2926ds/433Mi)
% 40.42/11.92 % (2132647)Refutation not found, incomplete strategy
% 40.42/11.92 % (2132647)------------------------------
% 40.42/11.92 % (2132647)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.42/11.92 % (2132647)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.42/11.92 % (2132647)CaDiCaL version: 2.1.3
% 40.42/11.92 % (2132647)Termination reason: Refutation not found, incomplete strategy
% 40.42/11.92 % (2132647)Time elapsed: 0.001 s
% 40.42/11.92 % (2132647)Peak memory usage: 88 MB
% 40.42/11.92 % (2132647)Instructions burned: 1 (million)
% 40.42/11.92 % (2132648)lrs+1002_1_ncem=casc2026/models/loop3.pt:sil=32000:npcc=on:prc=on:etr=on:spb=goal:flr=on:random_seed=270553755:st=5.37:cond=on:i=2942:s2at=20:aac=none:fgj=on:bs=on:gtg=exists_sym:ss=axioms:er=filter:sgt=16_2926 on theBenchmark for (2926ds/2942Mi)
% 40.42/11.92 % (2132647)------------------------------
% 40.42/11.92 % (2132647)------------------------------
% 40.42/11.92 % (2132651)lrs+35_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=reverse_arity:urr=full:rp=on:br=off:random_seed=421897588:i=6922:s2at=5:sd=3:bd=all:ss=axioms:er=known:sgt=32_2922 on theBenchmark for (2922ds/6922Mi)
% 40.42/11.92 % (2132629)Instruction limit reached!
% 40.42/11.92 % (2132629)------------------------------
% 40.42/11.92 % (2132629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.42/11.92 % (2132629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.42/11.92 % (2132629)CaDiCaL version: 2.1.3
% 40.42/11.92 % (2132629)Termination reason: Instruction limit
% 40.42/11.92 % (2132629)Termination phase: Saturation
% 40.42/11.92 % (2132629)Time elapsed: 5.101 s
% 40.42/11.92 % (2132629)Peak memory usage: 163 MB
% 40.42/11.92 % (2132629)Instructions burned: 8478 (million)
% 40.42/11.92 % (2132655)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=531645224:s2a=on:i=596:s2at=2.3:gtgl=5:gtg=all:sup=off_2913 on theBenchmark for (2913ds/596Mi)
% 40.42/11.92 % (2132624)Instruction limit reached!
% 40.42/11.92 % (2132624)------------------------------
% 40.42/11.92 % (2132624)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.42/11.92 % (2132624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.42/11.92 % (2132624)CaDiCaL version: 2.1.3
% 40.42/11.92 % (2132624)Termination reason: Instruction limit
% 40.42/11.92 % (2132624)Termination phase: Saturation
% 40.42/11.92 % (2132624)Time elapsed: 6.130 s
% 40.42/11.92 % (2132624)Peak memory usage: 168 MB
% 40.42/11.92 % (2132624)Instructions burned: 10308 (million)
% 40.42/11.92 % (2132655)Instruction limit reached!
% 40.42/11.92 % (2132655)------------------------------
% 40.42/11.92 % (2132655)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.42/11.92 % (2132655)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.42/11.92 % (2132655)CaDiCaL version: 2.1.3
% 40.42/11.92 % (2132655)Termination reason: Instruction limit
% 40.42/11.92 % (2132655)Termination phase: Saturation
% 40.42/11.92 % (2132655)Time elapsed: 0.289 s
% 40.42/11.92 % (2132655)Peak memory usage: 92 MB
% 40.42/11.92 % (2132655)Instructions burned: 599 (million)
% 40.42/11.92 % (2132658)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3561259634:i=16411:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2907 on theBenchmark for (2907ds/16411Mi)
% 40.42/11.92 % (2132648)Instruction limit reached!
% 40.42/11.92 % (2132648)------------------------------
% 40.42/11.92 % (2132648)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.42/11.92 % (2132648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.42/11.92 % (2132648)CaDiCaL version: 2.1.3
% 40.42/11.92 % (2132648)Termination reason: Instruction limit
% 40.42/11.92 % (2132648)Termination phase: Saturation
% 40.42/11.92 % (2132648)Time elapsed: 1.724 s
% 40.42/11.92 % (2132648)Peak memory usage: 140 MB
% 40.42/11.92 % (2132648)Instructions burned: 2946 (million)
% 40.42/11.92 % (2132657)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=3421502617:i=4123:kws=inv_frequency:bd=preordered:av=off:er=known_2908 on theBenchmark for (2908ds/4123Mi)
% 40.42/11.92 % (2132660)lrs+0_1_ncem=casc2026/models/loop1.pt:sil=8000:tgt=full:npcc=on:sp=reverse_frequency:gs=on:random_seed=1829941895:i=1670:kws=inv_precedence:bd=all:av=off:gtg=exists_all_2906 on theBenchmark for (2906ds/1670Mi)
% 40.42/11.92 % (2132660)Instruction limit reached!
% 40.42/11.92 % (2132660)------------------------------
% 40.42/11.92 % (2132660)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.42/11.92 % (2132660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.42/11.92 % (2132660)CaDiCaL version: 2.1.3
% 40.42/11.92 % (2132660)Termination reason: Instruction limit
% 40.42/11.92 % (2132660)Termination phase: Saturation
% 40.42/11.92 % (2132660)Time elapsed: 0.809 s
% 40.42/11.92 % (2132660)Peak memory usage: 136 MB
% 40.42/11.92 % (2132660)Instructions burned: 1672 (million)
% 40.42/11.92 % (2132663)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=2426497716:st=3:cond=fast:i=1722:sd=2:ss=included:fsd=on_2895 on theBenchmark for (2895ds/1722Mi)
% 40.42/11.92 % (2132651)First to succeed.
% 40.42/11.92 % (2132651)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2132560"
% 40.42/11.92 % (2132663)Refutation not found, incomplete strategy
% 40.42/11.92 % (2132663)------------------------------
% 40.42/11.92 % (2132663)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 40.42/11.92 % (2132663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.42/11.92 % (2132663)CaDiCaL version: 2.1.3
% 40.42/11.92 % (2132663)Termination reason: Refutation not found, incomplete strategy
% 40.42/11.92 % (2132663)Time elapsed: 0.486 s
% 40.42/11.92 % (2132663)Peak memory usage: 127 MB
% 40.42/11.92 % (2132663)Instructions burned: 858 (million)
% 40.42/11.92 % (2132651)Refutation found. Thanks to Tanya!
% 40.42/11.92 % SZS status Unsatisfiable for theBenchmark
% 40.42/11.92 % SZS output start Proof for theBenchmark
% See solution above
% 79.46/12.10 % (2132651)------------------------------
% 79.46/12.10 % (2132651)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.46/12.10 % (2132651)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.46/12.10 % (2132651)CaDiCaL version: 2.1.3
% 79.46/12.10 % (2132651)Termination reason: Refutation
% 79.46/12.10 % (2132651)Time elapsed: 2.940 s
% 79.46/12.10 % (2132651)Peak memory usage: 163 MB
% 79.46/12.10 % (2132651)Instructions burned: 5390 (million)
% 79.46/12.10 % (2132651)------------------------------
% 79.46/12.10 % (2132651)------------------------------
% 79.46/12.10 % (2132560)Success in time 11.264 s
% 79.46/12.10 % Vampire exiting
%------------------------------------------------------------------------------