%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP060-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/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:29 AM UTC 2026
% Result : Unsatisfiable 17.13s 3.44s
% Output : Refutation 17.89s
% Verified :
% SZS Type : Refutation
% Derivation depth : 33
% Number of leaves : 2
% Syntax : Number of formulae : 97 ( 95 unt; 0 def)
% Number of atoms : 101 ( 100 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 11 ( 7 ~; 4 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 5 avg)
% Maximal term depth : 13 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 365 ( 365 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X3,X0,X1] : multiply(X0,inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),inverse(multiply(X3,X1))),X0))))) = X3,
file('/export/starexec/sandbox2/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)) ),
file('/export/starexec/sandbox2/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) ),
inference(reorient_equations,[],[f2]) ).
fof(f5,plain,
! [X2,X3,X0,X1,X4] : multiply(X1,inverse(multiply(multiply(X2,multiply(multiply(inverse(X2),inverse(multiply(X0,X3))),inverse(X4))),multiply(X4,multiply(X0,X1))))) = X3,
inference(superposition,[],[f1,f1]) ).
fof(f6,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),inverse(multiply(X0,X1))),multiply(inverse(X3),inverse(multiply(X4,X5))))))),inverse(multiply(X5,multiply(X3,X0)))) = X4,
inference(superposition,[],[f1,f1]) ).
fof(f7,plain,
! [X2,X3,X0,X1,X6,X4,X5] : inverse(multiply(X4,multiply(X5,multiply(multiply(inverse(X5),inverse(multiply(X0,X4))),X3)))) = multiply(X1,inverse(multiply(multiply(X2,multiply(multiply(inverse(X2),inverse(X0)),inverse(X6))),multiply(X6,multiply(X3,X1))))),
inference(superposition,[],[f5,f1]) ).
fof(f16,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(X5,multiply(multiply(inverse(X5),inverse(multiply(X3,X0))),inverse(X2))) = multiply(X1,inverse(multiply(multiply(X2,multiply(X3,inverse(X4))),multiply(X4,multiply(X0,X1))))),
inference(superposition,[],[f1,f5]) ).
fof(f116,plain,
! [X2,X3,X0,X1] : multiply(X0,multiply(multiply(inverse(X0),inverse(multiply(multiply(inverse(X1),inverse(multiply(X2,X3))),X2))),inverse(X1))) = X3,
inference(superposition,[],[f5,f16]) ).
fof(f272,plain,
! [X2,X3,X0,X1,X4] : multiply(X4,multiply(X0,inverse(multiply(multiply(X1,multiply(multiply(inverse(X1),inverse(X2)),inverse(X3))),multiply(X3,multiply(X4,X0)))))) = X2,
inference(superposition,[],[f1,f7]) ).
fof(f299,plain,
! [X2,X3,X0,X1] : inverse(multiply(X0,multiply(X1,multiply(multiply(inverse(X1),inverse(multiply(multiply(X2,X3),X0))),X2)))) = X3,
inference(superposition,[],[f5,f7]) ).
fof(f351,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(inverse(X4),inverse(multiply(X2,X0))),inverse(X1)) = inverse(multiply(multiply(X1,multiply(X2,inverse(X3))),multiply(X3,multiply(X0,X4)))),
inference(superposition,[],[f299,f5]) ).
fof(f423,plain,
! [X2,X0,X1,X4,X5] : multiply(multiply(inverse(X4),inverse(multiply(X5,X0))),X5) = multiply(X1,multiply(X2,inverse(multiply(X0,multiply(X4,multiply(X1,X2)))))),
inference(superposition,[],[f272,f116]) ).
fof(f538,plain,
! [X2,X3,X0,X1,X6,X4,X5] : multiply(X5,multiply(X6,inverse(multiply(inverse(multiply(X3,multiply(X4,multiply(multiply(inverse(X4),inverse(multiply(X0,X3))),X2)))),multiply(X1,multiply(X5,X6)))))) = multiply(multiply(inverse(X1),inverse(X0)),X2),
inference(superposition,[],[f423,f1]) ).
fof(f593,plain,
! [X2,X3,X0,X1,X4] : multiply(X4,inverse(multiply(X2,multiply(X3,multiply(X0,multiply(X1,inverse(multiply(X2,multiply(X3,multiply(X0,X1)))))))))) = X4,
inference(superposition,[],[f1,f423]) ).
fof(f737,plain,
! [X2,X3,X0,X1] : multiply(X3,inverse(multiply(X2,multiply(X0,multiply(multiply(inverse(X0),inverse(multiply(X1,X2))),X1))))) = X3,
inference(superposition,[],[f593,f423]) ).
fof(f779,plain,
! [X2,X3,X0,X1,X6,X7,X4,X5] : multiply(X6,inverse(multiply(multiply(X5,multiply(X1,inverse(X7))),multiply(X7,multiply(multiply(X2,multiply(X3,multiply(X4,inverse(multiply(X1,multiply(X2,multiply(X3,X4))))))),X6))))) = multiply(X0,multiply(inverse(X0),inverse(X5))),
inference(superposition,[],[f16,f593]) ).
fof(f804,plain,
! [X2,X3,X0,X1,X6,X4,X5] : multiply(X0,multiply(inverse(X0),inverse(X5))) = multiply(X6,multiply(multiply(inverse(X6),inverse(multiply(X1,multiply(X2,multiply(X3,multiply(X4,inverse(multiply(X1,multiply(X2,multiply(X3,X4)))))))))),inverse(X5))),
inference(forward_demodulation,[],[f779,f351]) ).
fof(f825,plain,
! [X0,X6,X5] : multiply(X0,multiply(inverse(X0),inverse(X5))) = multiply(X6,multiply(inverse(X6),inverse(X5))),
inference(forward_demodulation,[],[f804,f593]) ).
fof(f851,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(X0,inverse(X0)) = multiply(X1,multiply(inverse(X1),inverse(multiply(X2,multiply(X3,multiply(X4,multiply(X5,inverse(multiply(X2,multiply(X3,multiply(X4,X5))))))))))),
inference(superposition,[],[f825,f593]) ).
fof(f962,plain,
! [X0,X1] : multiply(X0,inverse(X0)) = multiply(X1,inverse(X1)),
inference(forward_demodulation,[],[f851,f593]) ).
fof(f1036,plain,
! [X2,X3,X0,X1] : inverse(X3) = inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),inverse(multiply(multiply(X0,inverse(X0)),X1))),X3)))),
inference(superposition,[],[f299,f962]) ).
fof(f1053,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(X1),inverse(multiply(X2,X3)))),inverse(multiply(X3,multiply(X1,multiply(X0,inverse(X0)))))) = X2,
inference(superposition,[],[f1,f962]) ).
fof(f1821,plain,
! [X2,X3,X0,X1,X6,X4,X5] : multiply(multiply(inverse(X1),inverse(X0)),X0) = multiply(X5,multiply(X6,inverse(multiply(inverse(multiply(X2,multiply(X3,multiply(multiply(inverse(X3),inverse(multiply(X4,X2))),X4)))),multiply(X1,multiply(X5,X6)))))),
inference(superposition,[],[f423,f737]) ).
fof(f1872,plain,
! [X0,X1,X4] : multiply(multiply(inverse(X1),inverse(X0)),X0) = multiply(multiply(inverse(X1),inverse(X4)),X4),
inference(forward_demodulation,[],[f1821,f538]) ).
fof(f1915,plain,
! [X0,X4,X5] : multiply(multiply(X0,inverse(X4)),X4) = multiply(multiply(X0,inverse(X5)),X5),
inference(superposition,[],[f1872,f299]) ).
fof(f1987,plain,
! [X2,X3,X0,X1] : multiply(multiply(X2,X3),inverse(multiply(X3,multiply(X0,multiply(multiply(inverse(X0),inverse(X1)),X1))))) = X2,
inference(superposition,[],[f1,f1872]) ).
fof(f2092,plain,
! [X2,X0,X1] : multiply(multiply(X0,inverse(X0)),X1) = multiply(multiply(X1,inverse(X2)),X2),
inference(superposition,[],[f1915,f962]) ).
fof(f2781,plain,
! [X2,X0,X1] : multiply(X2,inverse(X2)) = multiply(X0,multiply(multiply(inverse(X0),inverse(X1)),X1)),
inference(superposition,[],[f962,f1987]) ).
fof(f2954,plain,
! [X2,X3,X0,X1,X4] : inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),inverse(multiply(multiply(X0,inverse(X0)),X1))),X3)))) = multiply(multiply(inverse(X3),inverse(X4)),X4),
inference(superposition,[],[f299,f2781]) ).
fof(f2972,plain,
! [X3,X4] : inverse(X3) = multiply(multiply(inverse(X3),inverse(X4)),X4),
inference(forward_demodulation,[],[f2954,f1036]) ).
fof(f3022,plain,
! [X0,X4] : multiply(multiply(X0,inverse(X4)),X4) = X0,
inference(superposition,[],[f2972,f299]) ).
fof(f3033,plain,
! [X2,X3,X0,X1,X4,X5] : inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),inverse(multiply(X3,X1))),multiply(inverse(X4),inverse(multiply(X0,X5))))))) = multiply(X0,multiply(X5,multiply(X4,X3))),
inference(superposition,[],[f2972,f6]) ).
fof(f3054,plain,
! [X0,X1] : inverse(X0) = multiply(multiply(X1,inverse(X1)),inverse(X0)),
inference(superposition,[],[f2092,f2972]) ).
fof(f3133,plain,
! [X2,X3,X0,X1] : multiply(X0,X1) = multiply(X0,multiply(X1,multiply(X2,multiply(multiply(inverse(X2),inverse(X3)),X3)))),
inference(superposition,[],[f3022,f1987]) ).
fof(f3145,plain,
! [X0,X1] : multiply(X0,X1) = multiply(X0,inverse(inverse(X1))),
inference(superposition,[],[f3022,f3022]) ).
fof(f3149,plain,
! [X2,X0,X1] : multiply(X2,inverse(X2)) = multiply(multiply(multiply(inverse(X0),inverse(X1)),X1),X0),
inference(superposition,[],[f3022,f2092]) ).
fof(f3206,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),inverse(multiply(X3,X1))),multiply(inverse(X4),inverse(multiply(X5,multiply(X0,inverse(multiply(X4,X3)))))))))),inverse(X0)) = X5,
inference(superposition,[],[f6,f3022]) ).
fof(f3226,plain,
! [X3,X0,X4,X5] : multiply(multiply(X5,multiply(multiply(X0,inverse(multiply(X4,X3))),multiply(X4,X3))),inverse(X0)) = X5,
inference(forward_demodulation,[],[f3206,f3033]) ).
fof(f3236,plain,
! [X2,X0] : multiply(X2,inverse(X2)) = multiply(inverse(X0),X0),
inference(forward_demodulation,[],[f3149,f3022]) ).
fof(f3246,plain,
! [X2,X0,X1] : multiply(X0,X1) = multiply(X0,multiply(X1,multiply(X2,inverse(X2)))),
inference(forward_demodulation,[],[f3133,f3022]) ).
fof(f3248,plain,
! [X0,X5] : multiply(multiply(X5,X0),inverse(X0)) = X5,
inference(forward_demodulation,[],[f3226,f3022]) ).
fof(f3299,plain,
! [X0,X1] : multiply(multiply(inverse(inverse(X0)),inverse(X1)),X1) = X0,
inference(superposition,[],[f2092,f3248]) ).
fof(f3348,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(forward_demodulation,[],[f3299,f3022]) ).
fof(f3446,plain,
! [X2,X0,X1] : multiply(multiply(X1,inverse(X2)),X2) = multiply(multiply(inverse(X0),X0),X1),
inference(superposition,[],[f2092,f3348]) ).
fof(f3457,plain,
! [X0,X1] : multiply(multiply(inverse(X0),X0),X1) = X1,
inference(forward_demodulation,[],[f3446,f3022]) ).
fof(f3495,plain,
! [X2,X0] : multiply(inverse(X0),X0) = multiply(inverse(X2),X2),
inference(superposition,[],[f3236,f3236]) ).
fof(f3580,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(X4,inverse(multiply(multiply(X3,multiply(X1,inverse(X5))),multiply(X5,multiply(X2,X4))))) = multiply(inverse(multiply(X1,X2)),multiply(multiply(X0,inverse(X0)),inverse(X3))),
inference(superposition,[],[f16,f3236]) ).
fof(f3705,plain,
! [X2,X3,X1,X4,X5] : multiply(X4,inverse(multiply(multiply(X3,multiply(X1,inverse(X5))),multiply(X5,multiply(X2,X4))))) = multiply(inverse(multiply(X1,X2)),inverse(X3)),
inference(forward_demodulation,[],[f3580,f3054]) ).
fof(f3790,plain,
! [X2,X3,X1,X4] : multiply(X4,multiply(multiply(inverse(X4),inverse(multiply(X1,X2))),inverse(X3))) = multiply(inverse(multiply(X1,X2)),inverse(X3)),
inference(forward_demodulation,[],[f3705,f351]) ).
fof(f3882,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(X0,multiply(multiply(inverse(X0),inverse(multiply(X1,X2))),X3)) = multiply(X4,inverse(multiply(multiply(inverse(X3),multiply(X1,inverse(X5))),multiply(X5,multiply(X2,X4))))),
inference(superposition,[],[f16,f3145]) ).
fof(f3931,plain,
! [X2,X3,X0,X1,X4] : multiply(X0,multiply(multiply(inverse(X0),inverse(multiply(X1,X2))),X3)) = multiply(X4,multiply(multiply(inverse(X4),inverse(multiply(X1,X2))),inverse(inverse(X3)))),
inference(forward_demodulation,[],[f3882,f351]) ).
fof(f3993,plain,
! [X2,X3,X0,X1] : multiply(X0,multiply(multiply(inverse(X0),inverse(multiply(X1,X2))),X3)) = multiply(inverse(multiply(X1,X2)),inverse(inverse(X3))),
inference(forward_demodulation,[],[f3931,f3790]) ).
fof(f4010,plain,
! [X2,X3,X0,X1] : multiply(X0,multiply(multiply(inverse(X0),inverse(multiply(X1,X2))),X3)) = multiply(inverse(multiply(X1,X2)),X3),
inference(forward_demodulation,[],[f3993,f3145]) ).
fof(f4123,plain,
! [X2,X3,X0,X1] : multiply(X1,multiply(multiply(inverse(X1),inverse(multiply(multiply(inverse(X0),X0),X2))),inverse(inverse(multiply(X2,X3))))) = X3,
inference(superposition,[],[f116,f3495]) ).
fof(f4132,plain,
! [X2,X3,X0,X1,X6,X4,X5] : inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),inverse(multiply(X3,X1))),X4)))) = multiply(X5,inverse(multiply(multiply(inverse(X3),multiply(multiply(inverse(X0),X0),inverse(X6))),multiply(X6,multiply(X4,X5))))),
inference(superposition,[],[f7,f3495]) ).
fof(f4240,plain,
! [X2,X3,X0,X1,X4,X5] : inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),inverse(multiply(X3,X1))),X4)))) = multiply(X5,multiply(multiply(inverse(X5),inverse(multiply(multiply(inverse(X0),X0),X4))),inverse(inverse(X3)))),
inference(forward_demodulation,[],[f4132,f351]) ).
fof(f4247,plain,
! [X2,X3,X0] : multiply(inverse(multiply(multiply(inverse(X0),X0),X2)),inverse(inverse(multiply(X2,X3)))) = X3,
inference(forward_demodulation,[],[f4123,f3790]) ).
fof(f4351,plain,
! [X2,X3,X0,X1,X4] : inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),inverse(multiply(X3,X1))),X4)))) = multiply(inverse(multiply(multiply(inverse(X0),X0),X4)),inverse(inverse(X3))),
inference(forward_demodulation,[],[f4240,f3790]) ).
fof(f4352,plain,
! [X2,X3,X0] : multiply(inverse(multiply(multiply(inverse(X0),X0),X2)),multiply(X2,X3)) = X3,
inference(forward_demodulation,[],[f4247,f3145]) ).
fof(f4395,plain,
! [X2,X3,X0,X1,X4] : inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),inverse(multiply(X3,X1))),X4)))) = multiply(inverse(multiply(multiply(inverse(X0),X0),X4)),X3),
inference(forward_demodulation,[],[f4351,f3145]) ).
fof(f4396,plain,
! [X2,X3] : multiply(inverse(X2),multiply(X2,X3)) = X3,
inference(forward_demodulation,[],[f4352,f3457]) ).
fof(f4416,plain,
! [X2,X3,X1,X4] : inverse(multiply(X1,multiply(X2,multiply(multiply(inverse(X2),inverse(multiply(X3,X1))),X4)))) = multiply(inverse(X4),X3),
inference(forward_demodulation,[],[f4395,f3457]) ).
fof(f4422,plain,
! [X3,X1,X4] : multiply(inverse(X4),X3) = inverse(multiply(X1,multiply(inverse(multiply(X3,X1)),X4))),
inference(forward_demodulation,[],[f4416,f4010]) ).
fof(f4445,plain,
! [X0,X1] : inverse(X1) = multiply(inverse(multiply(X0,X1)),X0),
inference(superposition,[],[f4396,f3248]) ).
fof(f4454,plain,
! [X2,X3,X0,X1] : inverse(multiply(X2,multiply(X1,multiply(X3,inverse(X3))))) = multiply(inverse(inverse(multiply(inverse(X1),inverse(multiply(X0,X2))))),X0),
inference(superposition,[],[f4396,f1053]) ).
fof(f4478,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(X3,inverse(multiply(multiply(X4,multiply(multiply(inverse(X4),inverse(X1)),inverse(X5))),multiply(X5,multiply(X2,X3))))) = inverse(multiply(multiply(inverse(X0),inverse(multiply(X1,inverse(X0)))),X2)),
inference(superposition,[],[f7,f4396]) ).
fof(f4493,plain,
! [X2,X3,X0,X1,X4] : multiply(X1,multiply(multiply(inverse(X1),inverse(multiply(X2,X3))),inverse(X4))) = multiply(X0,inverse(multiply(multiply(X4,multiply(X2,inverse(inverse(X3)))),X0))),
inference(superposition,[],[f16,f4396]) ).
fof(f4496,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(inverse(X1)),inverse(multiply(X2,X3))),X2) = multiply(X1,multiply(X0,inverse(multiply(X3,X0)))),
inference(superposition,[],[f423,f4396]) ).
fof(f4528,plain,
! [X0,X1] : inverse(X1) = multiply(X0,inverse(multiply(X1,X0))),
inference(superposition,[],[f3248,f4396]) ).
fof(f4550,plain,
! [X2,X3,X1] : multiply(X1,inverse(X3)) = multiply(multiply(inverse(inverse(X1)),inverse(multiply(X2,X3))),X2),
inference(forward_demodulation,[],[f4496,f4528]) ).
fof(f4553,plain,
! [X2,X3,X1,X4] : multiply(X1,multiply(multiply(inverse(X1),inverse(multiply(X2,X3))),inverse(X4))) = inverse(multiply(X4,multiply(X2,inverse(inverse(X3))))),
inference(forward_demodulation,[],[f4493,f4528]) ).
fof(f4567,plain,
! [X2,X3,X1,X4,X5] : inverse(multiply(inverse(X1),X2)) = multiply(X3,inverse(multiply(multiply(X4,multiply(multiply(inverse(X4),inverse(X1)),inverse(X5))),multiply(X5,multiply(X2,X3))))),
inference(forward_demodulation,[],[f4478,f4528]) ).
fof(f4579,plain,
! [X2,X3,X0,X1] : inverse(multiply(X2,multiply(X1,multiply(X3,inverse(X3))))) = multiply(multiply(inverse(X1),inverse(multiply(X0,X2))),X0),
inference(forward_demodulation,[],[f4454,f3348]) ).
fof(f4616,plain,
! [X2,X3,X1] : multiply(multiply(X1,inverse(multiply(X2,X3))),X2) = multiply(X1,inverse(X3)),
inference(forward_demodulation,[],[f4550,f3348]) ).
fof(f4619,plain,
! [X2,X3,X1,X4] : multiply(X1,multiply(multiply(inverse(X1),inverse(multiply(X2,X3))),inverse(X4))) = inverse(multiply(X4,multiply(X2,X3))),
inference(forward_demodulation,[],[f4553,f3145]) ).
fof(f4630,plain,
! [X2,X3,X1,X4] : inverse(multiply(inverse(X1),X2)) = multiply(X3,multiply(multiply(inverse(X3),inverse(multiply(multiply(inverse(X4),inverse(X1)),X2))),inverse(X4))),
inference(forward_demodulation,[],[f4567,f351]) ).
fof(f4638,plain,
! [X2,X0,X1] : inverse(multiply(X2,X1)) = multiply(multiply(inverse(X1),inverse(multiply(X0,X2))),X0),
inference(forward_demodulation,[],[f4579,f3246]) ).
fof(f4656,plain,
! [X2,X3,X4] : multiply(inverse(multiply(X2,X3)),inverse(X4)) = inverse(multiply(X4,multiply(X2,X3))),
inference(forward_demodulation,[],[f4619,f4010]) ).
fof(f4660,plain,
! [X2,X1,X4] : inverse(multiply(inverse(X1),X2)) = multiply(inverse(multiply(multiply(inverse(X4),inverse(X1)),X2)),inverse(X4)),
inference(forward_demodulation,[],[f4630,f3790]) ).
fof(f4664,plain,
! [X2,X1] : multiply(inverse(X1),inverse(X2)) = inverse(multiply(X2,X1)),
inference(forward_demodulation,[],[f4638,f4616]) ).
fof(f4672,plain,
! [X2,X1,X4] : inverse(multiply(inverse(X1),X2)) = inverse(multiply(X4,multiply(multiply(inverse(X4),inverse(X1)),X2))),
inference(forward_demodulation,[],[f4660,f4656]) ).
fof(f4678,plain,
! [X2,X1,X4] : inverse(multiply(inverse(X1),X2)) = inverse(multiply(X4,multiply(inverse(multiply(X1,X4)),X2))),
inference(forward_demodulation,[],[f4672,f4664]) ).
fof(f4681,plain,
! [X2,X1] : inverse(multiply(inverse(X1),X2)) = multiply(inverse(X2),X1),
inference(forward_demodulation,[],[f4678,f4422]) ).
fof(f5112,plain,
! [X2,X3,X0,X1] : inverse(multiply(X0,X3)) = multiply(X1,multiply(multiply(inverse(X1),inverse(multiply(multiply(inverse(X2),inverse(inverse(X0))),X3))),inverse(X2))),
inference(superposition,[],[f116,f4528]) ).
fof(f5213,plain,
! [X2,X3,X0] : inverse(multiply(X0,X3)) = multiply(inverse(multiply(multiply(inverse(X2),inverse(inverse(X0))),X3)),inverse(X2)),
inference(forward_demodulation,[],[f5112,f3790]) ).
fof(f5310,plain,
! [X2,X3,X0] : inverse(multiply(X0,X3)) = inverse(multiply(X2,multiply(multiply(inverse(X2),inverse(inverse(X0))),X3))),
inference(forward_demodulation,[],[f5213,f4656]) ).
fof(f5365,plain,
! [X2,X3,X0] : inverse(multiply(X0,X3)) = inverse(multiply(X2,multiply(multiply(inverse(X2),X0),X3))),
inference(forward_demodulation,[],[f5310,f3145]) ).
fof(f7601,plain,
! [X2,X3,X0,X1] : multiply(X0,X3) = inverse(multiply(X1,multiply(multiply(inverse(X1),inverse(multiply(multiply(X2,X0),X3))),X2))),
inference(superposition,[],[f4445,f299]) ).
fof(f7670,plain,
! [X2,X3,X0,X1,X4] : multiply(X3,multiply(X4,inverse(inverse(X0)))) = multiply(multiply(inverse(X1),inverse(multiply(X2,inverse(multiply(multiply(X1,multiply(X3,X4)),X0))))),X2),
inference(superposition,[],[f423,f4445]) ).
fof(f7716,plain,
! [X3,X0,X1,X4] : multiply(X3,multiply(X4,inverse(inverse(X0)))) = multiply(inverse(X1),inverse(inverse(multiply(multiply(X1,multiply(X3,X4)),X0)))),
inference(forward_demodulation,[],[f7670,f4616]) ).
fof(f7780,plain,
! [X2,X3,X0] : multiply(X0,X3) = inverse(multiply(inverse(multiply(multiply(X2,X0),X3)),X2)),
inference(forward_demodulation,[],[f7601,f5365]) ).
fof(f7842,plain,
! [X3,X0,X1,X4] : multiply(X3,multiply(X4,inverse(inverse(X0)))) = multiply(inverse(X1),multiply(multiply(X1,multiply(X3,X4)),X0)),
inference(forward_demodulation,[],[f7716,f3145]) ).
fof(f7879,plain,
! [X2,X3,X0] : multiply(X0,X3) = multiply(inverse(X2),multiply(multiply(X2,X0),X3)),
inference(forward_demodulation,[],[f7780,f4681]) ).
fof(f7931,plain,
! [X3,X0,X1,X4] : multiply(X3,multiply(X4,X0)) = multiply(inverse(X1),multiply(multiply(X1,multiply(X3,X4)),X0)),
inference(forward_demodulation,[],[f7842,f3145]) ).
fof(f8007,plain,
! [X3,X0,X4] : multiply(X3,multiply(X4,X0)) = multiply(multiply(X3,X4),X0),
inference(forward_demodulation,[],[f7931,f7879]) ).
fof(f8225,plain,
a2 != multiply(multiply(inverse(b2),b2),a2),
inference(unit_resulting_resolution,[],[f3,f3495,f8007]) ).
fof(f8677,plain,
$false,
inference(forward_subsumption_resolution,[],[f8225,f3457]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP060-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/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:17:37 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.13/0.46 Running first-order theorem proving
% 0.13/0.46 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.82/3.10 % (3241030)Input is clausal, will run a generic CNF schedule.
% 14.82/3.10 % (3241049)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=1559676084:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 14.82/3.10 % (3241048)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=1920593903:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 14.82/3.10 % (3241047)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=256171742:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 14.82/3.10 % (3241051)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=612518429:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 14.82/3.10 % (3241052)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4071130253:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 14.82/3.10 % (3241050)lrs+10_1_sil=8000:sp=occurrence:random_seed=2842995460:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 14.82/3.10 % (3241053)dis-21_1_sil=8000:lcm=predicate:random_seed=962587330: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)
% 14.82/3.10 % (3241053)Refutation not found, incomplete strategy
% 14.82/3.10 % (3241053)------------------------------
% 14.82/3.10 % (3241053)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.82/3.10 % (3241053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.82/3.10 % (3241053)CaDiCaL version: 2.1.3
% 14.82/3.10 % (3241053)Termination reason: Refutation not found, incomplete strategy
% 14.82/3.10 % (3241053)Time elapsed: 0.002 s
% 14.82/3.10 % (3241053)Peak memory usage: 88 MB
% 14.82/3.10 % (3241050)Instruction limit reached!
% 14.82/3.10 % (3241050)------------------------------
% 14.82/3.10 % (3241050)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.82/3.10 % (3241050)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.82/3.10 % (3241050)CaDiCaL version: 2.1.3
% 14.82/3.10 % (3241050)Termination reason: Instruction limit
% 14.82/3.10 % (3241050)Termination phase: Saturation
% 14.82/3.10 % (3241050)Time elapsed: 0.109 s
% 14.82/3.10 % (3241050)Peak memory usage: 90 MB
% 14.82/3.10 % (3241050)Instructions burned: 107 (million)
% 14.82/3.10 % (3241051)Instruction limit reached!
% 14.82/3.10 % (3241051)------------------------------
% 14.82/3.10 % (3241051)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.82/3.10 % (3241051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.82/3.10 % (3241051)CaDiCaL version: 2.1.3
% 14.82/3.10 % (3241051)Termination reason: Instruction limit
% 14.82/3.10 % (3241051)Termination phase: Saturation
% 14.82/3.10 % (3241051)Time elapsed: 0.114 s
% 14.82/3.10 % (3241051)Peak memory usage: 89 MB
% 14.82/3.10 % (3241051)Instructions burned: 114 (million)
% 14.82/3.10 % (3241052)Instruction limit reached!
% 14.82/3.10 % (3241052)------------------------------
% 14.82/3.10 % (3241052)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.82/3.10 % (3241052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.82/3.10 % (3241052)CaDiCaL version: 2.1.3
% 14.82/3.10 % (3241052)Termination reason: Instruction limit
% 14.82/3.10 % (3241052)Termination phase: Saturation
% 14.82/3.10 % (3241052)Time elapsed: 0.163 s
% 14.82/3.10 % (3241052)Peak memory usage: 90 MB
% 14.82/3.10 % (3241052)Instructions burned: 181 (million)
% 14.82/3.10 % (3241062)ott-1010_1_to=lpo:sil=16000:sos=on:spb=units:urr=on:bce=on:br=off:random_seed=2433367315: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)
% 14.82/3.10 % (3241062)Refutation not found, incomplete strategy
% 14.82/3.10 % (3241062)------------------------------
% 14.82/3.10 % (3241062)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 14.82/3.10 % (3241062)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 14.82/3.10 % (3241062)CaDiCaL version: 2.1.3
% 14.82/3.10 % (3241062)Termination reason: Refutation not found, incomplete strategy
% 14.82/3.10 % (3241062)Time elapsed: 0.001 s
% 14.82/3.10 % (3241062)Peak memory usage: 88 MB
% 14.82/3.10 % (3241061)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=518855818:i=143:sd=2:aac=none:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/143Mi)
% 17.13/3.44 % (3241061)Refutation not found, incomplete strategy
% 17.13/3.44 % (3241061)------------------------------
% 17.13/3.44 % (3241061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.13/3.44 % (3241061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.13/3.44 % (3241061)CaDiCaL version: 2.1.3
% 17.13/3.44 % (3241061)Termination reason: Refutation not found, incomplete strategy
% 17.13/3.44 % (3241061)Time elapsed: 0.002 s
% 17.13/3.44 % (3241061)Peak memory usage: 88 MB
% 17.13/3.44 % (3241063)lrs-1002_1_to=lpo:sil=8000:fde=none:sos=on:random_seed=3161953789:st=4:i=219:sd=3:ss=axioms_2996 on theBenchmark for (2996ds/219Mi)
% 17.13/3.44 % (3241063)Refutation not found, incomplete strategy
% 17.13/3.44 % (3241063)------------------------------
% 17.13/3.44 % (3241063)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.13/3.44 % (3241063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.13/3.44 % (3241063)CaDiCaL version: 2.1.3
% 17.13/3.44 % (3241063)Termination reason: Refutation not found, incomplete strategy
% 17.13/3.44 % (3241063)Time elapsed: 0.002 s
% 17.13/3.44 % (3241063)Peak memory usage: 88 MB
% 17.13/3.44 % (3241053)------------------------------
% 17.13/3.44 % (3241053)------------------------------
% 17.13/3.44 % (3241062)------------------------------
% 17.13/3.44 % (3241062)------------------------------
% 17.13/3.44 % (3241069)lrs+10_64_to=lpo:sil=8000:random_seed=508699138:i=126:bd=preordered_2993 on theBenchmark for (2993ds/126Mi)
% 17.13/3.44 % (3241061)------------------------------
% 17.13/3.44 % (3241061)------------------------------
% 17.13/3.44 % (3241070)lrs+1011_16_to=lpo:sil=8000:drc=off:sp=reverse_frequency:spb=goal_then_units:random_seed=1634497605:avsq=on:i=194:fgj=on:bd=preordered_2992 on theBenchmark for (2992ds/194Mi)
% 17.13/3.44 % (3241063)------------------------------
% 17.13/3.44 % (3241063)------------------------------
% 17.13/3.44 % (3241069)Instruction limit reached!
% 17.13/3.44 % (3241069)------------------------------
% 17.13/3.44 % (3241069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.13/3.44 % (3241069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.13/3.44 % (3241069)CaDiCaL version: 2.1.3
% 17.13/3.44 % (3241069)Termination reason: Instruction limit
% 17.13/3.44 % (3241069)Termination phase: Saturation
% 17.13/3.44 % (3241069)Time elapsed: 0.124 s
% 17.13/3.44 % (3241069)Peak memory usage: 88 MB
% 17.13/3.44 % (3241069)Instructions burned: 126 (million)
% 17.13/3.44 % (3241072)lrs+10_1_sil=8000:tgt=full:acc=on:random_seed=4103094660:i=157:gtg=all_2990 on theBenchmark for (2990ds/157Mi)
% 17.13/3.44 % (3241070)Instruction limit reached!
% 17.13/3.44 % (3241070)------------------------------
% 17.13/3.44 % (3241070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.13/3.44 % (3241070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.13/3.44 % (3241070)CaDiCaL version: 2.1.3
% 17.13/3.44 % (3241070)Termination reason: Instruction limit
% 17.13/3.44 % (3241070)Termination phase: Saturation
% 17.13/3.44 % (3241070)Time elapsed: 0.178 s
% 17.13/3.44 % (3241070)Peak memory usage: 90 MB
% 17.13/3.44 % (3241070)Instructions burned: 194 (million)
% 17.13/3.44 % (3241074)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:random_seed=1134244161:i=3394:sd=4:ss=included:sgt=64_2990 on theBenchmark for (2990ds/3394Mi)
% 17.13/3.44 % (3241075)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=2806355167:cts=off:s2a=on:i=106:fsr=off:gsp=on:ss=axioms:sgt=16:rawr=on_2989 on theBenchmark for (2989ds/106Mi)
% 17.13/3.44 % (3241072)Instruction limit reached!
% 17.13/3.44 % (3241072)------------------------------
% 17.13/3.44 % (3241072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.13/3.44 % (3241072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.13/3.44 % (3241072)CaDiCaL version: 2.1.3
% 17.13/3.44 % (3241072)Termination reason: Instruction limit
% 17.13/3.44 % (3241072)Termination phase: Saturation
% 17.13/3.44 % (3241072)Time elapsed: 0.144 s
% 17.13/3.44 % (3241072)Peak memory usage: 92 MB
% 17.13/3.44 % (3241072)Instructions burned: 157 (million)
% 17.13/3.44 % (3241078)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=1845447676:i=107_2988 on theBenchmark for (2988ds/107Mi)
% 17.13/3.44 % (3241078)Refutation not found, incomplete strategy
% 17.13/3.44 % (3241078)------------------------------
% 17.13/3.44 % (3241078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.13/3.44 % (3241078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.13/3.44 % (3241078)CaDiCaL version: 2.1.3
% 17.13/3.44 % (3241078)Termination reason: Refutation not found, incomplete strategy
% 17.13/3.44 % (3241078)Time elapsed: 0.001 s
% 17.13/3.44 % (3241078)Peak memory usage: 88 MB
% 17.13/3.44 % (3241075)Instruction limit reached!
% 17.13/3.44 % (3241075)------------------------------
% 17.13/3.44 % (3241075)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.13/3.44 % (3241075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.13/3.44 % (3241075)CaDiCaL version: 2.1.3
% 17.13/3.44 % (3241075)Termination reason: Instruction limit
% 17.13/3.44 % (3241075)Termination phase: Saturation
% 17.13/3.44 % (3241075)Time elapsed: 0.078 s
% 17.13/3.44 % (3241075)Peak memory usage: 90 MB
% 17.13/3.44 % (3241075)Instructions burned: 107 (million)
% 17.13/3.44 % (3241082)lrs+1011_20_sil=64000:tgt=ground:plsq=on:fde=unused:plsqc=1:plsqr=14,1:plsql=on:nwc=0.6:random_seed=1579554520:st=6:i=242:gtgl=5:kws=arity_squared:av=off:gtg=exists_sym:ss=included_2987 on theBenchmark for (2987ds/242Mi)
% 17.13/3.44 % (3241085)lrs+1010_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:tgt=ground:npcc=on:sims=off:random_seed=4234255197:cond=fast:i=5208:av=off_2986 on theBenchmark for (2986ds/5208Mi)
% 17.13/3.44 % (3241082)Instruction limit reached!
% 17.13/3.44 % (3241082)------------------------------
% 17.13/3.44 % (3241082)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.13/3.44 % (3241082)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.13/3.44 % (3241082)CaDiCaL version: 2.1.3
% 17.13/3.44 % (3241082)Termination reason: Instruction limit
% 17.13/3.44 % (3241082)Termination phase: Saturation
% 17.13/3.44 % (3241082)Time elapsed: 0.121 s
% 17.13/3.44 % (3241082)Peak memory usage: 93 MB
% 17.13/3.44 % (3241082)Instructions burned: 244 (million)
% 17.13/3.44 % (3241078)------------------------------
% 17.13/3.44 % (3241078)------------------------------
% 17.13/3.44 % (3241124)lrs+1011_16_sil=32000:erd=off:bce=on:random_seed=3442507401:i=134:sd=2:doe=on:ss=axioms:sgt=14_2984 on theBenchmark for (2984ds/134Mi)
% 17.13/3.44 % (3241133)ott+10_5:4_to=lpo:sil=8000:prc=on:fde=unused:sp=unary_frequency:spb=goal:urr=on:random_seed=4086227884:i=499:bd=all_2984 on theBenchmark for (2984ds/499Mi)
% 17.13/3.44 % (3241124)Instruction limit reached!
% 17.13/3.44 % (3241124)------------------------------
% 17.13/3.44 % (3241124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.13/3.44 % (3241124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.13/3.44 % (3241124)CaDiCaL version: 2.1.3
% 17.13/3.44 % (3241124)Termination reason: Instruction limit
% 17.13/3.44 % (3241124)Termination phase: Saturation
% 17.13/3.44 % (3241124)Time elapsed: 0.082 s
% 17.13/3.44 % (3241124)Peak memory usage: 90 MB
% 17.13/3.44 % (3241124)Instructions burned: 135 (million)
% 17.13/3.44 % (3241197)lrs+10_64_to=lpo:sil=8000:prc=on:sp=reverse_frequency:nwc=5:alpa=false:flr=on:random_seed=476710052:i=191:fgj=on:bd=all_2982 on theBenchmark for (2982ds/191Mi)
% 17.13/3.44 % (3241197)Instruction limit reached!
% 17.13/3.44 % (3241197)------------------------------
% 17.13/3.44 % (3241197)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.13/3.44 % (3241197)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.13/3.44 % (3241197)CaDiCaL version: 2.1.3
% 17.13/3.44 % (3241197)Termination reason: Instruction limit
% 17.13/3.44 % (3241197)Termination phase: Saturation
% 17.13/3.44 % (3241197)Time elapsed: 0.117 s
% 17.13/3.44 % (3241197)Peak memory usage: 90 MB
% 17.13/3.44 % (3241197)Instructions burned: 192 (million)
% 17.13/3.44 % (3241133)Instruction limit reached!
% 17.13/3.44 % (3241133)------------------------------
% 17.13/3.44 % (3241133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.13/3.44 % (3241133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.13/3.44 % (3241133)CaDiCaL version: 2.1.3
% 17.13/3.44 % (3241133)Termination reason: Instruction limit
% 17.13/3.44 % (3241133)Termination phase: Saturation
% 17.13/3.44 % (3241133)Time elapsed: 0.294 s
% 17.13/3.44 % (3241133)Peak memory usage: 95 MB
% 17.13/3.44 % (3241133)Instructions burned: 500 (million)
% 17.13/3.44 % (3241246)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3414969418:i=264:kws=precedence:fsr=off_2980 on theBenchmark for (2980ds/264Mi)
% 17.13/3.44 % (3241247)lrs-22_64_to=lpo:sil=8000:sp=const_frequency:urr=ec_only:nwc=4:flr=on:random_seed=262083777:cond=on:i=156:bs=on:gtg=exists_all:er=known_2980 on theBenchmark for (2980ds/156Mi)
% 17.13/3.44 % (3241048)First to succeed.
% 17.13/3.44 % (3241048)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3241030"
% 17.13/3.44 % (3241247)Instruction limit reached!
% 17.13/3.44 % (3241247)------------------------------
% 17.13/3.44 % (3241247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.13/3.44 % (3241247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.13/3.44 % (3241247)CaDiCaL version: 2.1.3
% 17.13/3.44 % (3241247)Termination reason: Instruction limit
% 17.13/3.44 % (3241247)Termination phase: Saturation
% 17.13/3.44 % (3241247)Time elapsed: 0.101 s
% 17.13/3.44 % (3241247)Peak memory usage: 90 MB
% 17.13/3.44 % (3241247)Instructions burned: 157 (million)
% 17.13/3.44 % (3241246)Instruction limit reached!
% 17.13/3.44 % (3241246)------------------------------
% 17.13/3.44 % (3241246)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.13/3.44 % (3241246)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.13/3.44 % (3241246)CaDiCaL version: 2.1.3
% 17.13/3.44 % (3241246)Termination reason: Instruction limit
% 17.13/3.44 % (3241246)Termination phase: Saturation
% 17.13/3.44 % (3241246)Time elapsed: 0.162 s
% 17.13/3.44 % (3241246)Peak memory usage: 92 MB
% 17.13/3.44 % (3241246)Instructions burned: 265 (million)
% 17.13/3.44 % (3241250)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=2939840836:i=3256:kws=precedence:bd=preordered:av=off_2978 on theBenchmark for (2978ds/3256Mi)
% 17.13/3.44 % (3241251)dis+1003_128_sil=8000:tgt=full:fd=off:random_seed=140134576:i=537:av=off:ss=included_2977 on theBenchmark for (2977ds/537Mi)
% 17.13/3.44 % (3241048)Refutation found. Thanks to Tanya!
% 17.13/3.44 % SZS status Unsatisfiable for theBenchmark
% 17.13/3.44 % SZS output start Proof for theBenchmark
% See solution above
% 17.89/3.63 % (3241048)------------------------------
% 17.89/3.63 % (3241048)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 17.89/3.63 % (3241048)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.89/3.63 % (3241048)CaDiCaL version: 2.1.3
% 17.89/3.63 % (3241048)Termination reason: Refutation
% 17.89/3.63 % (3241048)Time elapsed: 1.951 s
% 17.89/3.63 % (3241048)Peak memory usage: 146 MB
% 17.89/3.63 % (3241048)Instructions burned: 2618 (million)
% 17.89/3.63 % (3241048)------------------------------
% 17.89/3.63 % (3241048)------------------------------
% 17.89/3.63 % (3241030)Success in time 2.429 s
% 17.89/3.63 % Vampire exiting
%------------------------------------------------------------------------------