%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GRP420-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 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:17:47 AM UTC 2026
% Result : Unsatisfiable 66.47s 9.86s
% Output : Refutation 66.47s
% Verified :
% SZS Type : Refutation
% Derivation depth : 47
% Number of leaves : 2
% Syntax : Number of formulae : 98 ( 98 unt; 0 def)
% Number of atoms : 98 ( 97 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 4 avg)
% Maximal term depth : 21 ( 4 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 : 290 ( 290 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X0,X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_these_axioms_3) ).
fof(f3,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X2,X3)) = inverse(multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X4,inverse(multiply(inverse(X4),X4)))))))),multiply(X1,X4))),
inference(superposition,[],[f1,f1]) ).
fof(f15,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X0)),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X1,X2)) = X0,
inference(superposition,[],[f3,f1]) ).
fof(f17,plain,
! [X2,X0,X1] : inverse(inverse(multiply(inverse(multiply(X0,inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X0,X2)))) = X1,
inference(superposition,[],[f1,f3]) ).
fof(f20,plain,
! [X2,X3,X0,X1,X6,X4,X5] : inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(X4),inverse(multiply(multiply(inverse(multiply(X5,inverse(multiply(X1,inverse(multiply(X6,inverse(multiply(inverse(X6),X6)))))))),multiply(X5,X6)),inverse(multiply(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X0,X2)),multiply(inverse(multiply(X5,inverse(multiply(X1,inverse(multiply(X6,inverse(multiply(inverse(X6),X6)))))))),multiply(X5,X6)))))))))),multiply(X3,multiply(inverse(multiply(X5,inverse(multiply(X1,inverse(multiply(X6,inverse(multiply(inverse(X6),X6)))))))),multiply(X5,X6))))) = X4,
inference(superposition,[],[f1,f3]) ).
fof(f27,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X0)),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),inverse(multiply(inverse(inverse(X3)),inverse(multiply(multiply(X1,X2),inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X2))))))))),X0) = X3,
inference(superposition,[],[f15,f15]) ).
fof(f33,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X0)),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),inverse(multiply(inverse(X3),inverse(multiply(multiply(X1,X2),inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X2))))))))),X0)) = X3,
inference(superposition,[],[f1,f15]) ).
fof(f317,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X2,inverse(multiply(inverse(inverse(inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))),inverse(multiply(X4,inverse(multiply(inverse(X4),X4)))))))),inverse(multiply(inverse(X0),inverse(multiply(multiply(X2,X4),inverse(multiply(inverse(multiply(X2,X4)),multiply(X2,X4)))))))) = inverse(multiply(inverse(multiply(X1,X0)),multiply(X1,X3))),
inference(superposition,[],[f1,f33]) ).
fof(f476,plain,
! [X2,X0,X1,X5] : inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))) = inverse(multiply(inverse(multiply(X5,X1)),multiply(X5,X2))),
inference(superposition,[],[f317,f317]) ).
fof(f506,plain,
! [X2,X0,X1] : multiply(inverse(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,X2)))),inverse(multiply(X2,inverse(multiply(inverse(X2),X2))))) = X1,
inference(superposition,[],[f27,f317]) ).
fof(f507,plain,
! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))) = X1,
inference(superposition,[],[f33,f317]) ).
fof(f682,plain,
! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X3),inverse(multiply(multiply(X4,X1),inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X1))))))))),multiply(X2,multiply(X4,X1)))) = X3,
inference(superposition,[],[f1,f476]) ).
fof(f3758,plain,
! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),inverse(multiply(multiply(X3,X4),inverse(multiply(inverse(X0),X0)))))))),multiply(X1,multiply(X3,X4)))) = X2,
inference(superposition,[],[f682,f27]) ).
fof(f3999,plain,
! [X2,X0,X1,X5] : inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(X2),inverse(multiply(X0,inverse(multiply(inverse(X5),X5)))))))),multiply(X1,X0))) = X2,
inference(superposition,[],[f3758,f15]) ).
fof(f4241,plain,
! [X2,X3,X0] : multiply(inverse(X0),inverse(multiply(X2,inverse(multiply(inverse(X2),X2))))) = multiply(inverse(X0),inverse(multiply(X2,inverse(multiply(inverse(X3),X3))))),
inference(superposition,[],[f506,f3999]) ).
fof(f4598,plain,
! [X2,X3,X0,X1] : multiply(X1,inverse(multiply(inverse(X2),X2))) = multiply(inverse(inverse(multiply(inverse(multiply(inverse(X0),inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))),multiply(inverse(X0),X3)))),inverse(multiply(X3,inverse(multiply(inverse(X3),X3))))),
inference(superposition,[],[f506,f4241]) ).
fof(f4667,plain,
! [X2,X1] : multiply(X1,inverse(multiply(inverse(X1),X1))) = multiply(X1,inverse(multiply(inverse(X2),X2))),
inference(forward_demodulation,[],[f4598,f506]) ).
fof(f4717,plain,
! [X2,X0,X1] : multiply(X0,inverse(multiply(inverse(X1),X1))) = multiply(X0,inverse(multiply(inverse(X2),X2))),
inference(superposition,[],[f4667,f4667]) ).
fof(f4895,plain,
! [X2,X0,X1] : multiply(inverse(X1),X1) = multiply(inverse(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X0),X0)))),multiply(X0,X2)))),inverse(multiply(X2,inverse(multiply(inverse(X2),X2))))),
inference(superposition,[],[f506,f4667]) ).
fof(f4918,plain,
! [X2,X0,X1] : inverse(multiply(inverse(X1),X1)) = inverse(multiply(inverse(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X0),X0)))),multiply(X0,X2)))),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))),
inference(superposition,[],[f507,f4667]) ).
fof(f4974,plain,
! [X0,X1] : inverse(multiply(inverse(X0),X0)) = inverse(multiply(inverse(X1),X1)),
inference(forward_demodulation,[],[f4918,f507]) ).
fof(f4975,plain,
! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(X1),X1),
inference(forward_demodulation,[],[f4895,f506]) ).
fof(f5107,plain,
! [X2,X0] : inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))) = X2,
inference(superposition,[],[f507,f4975]) ).
fof(f5958,plain,
! [X2,X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X2),X2))),
inference(superposition,[],[f4717,f4975]) ).
fof(f10434,plain,
! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(X2,inverse(multiply(inverse(X0),X0)))))) = X2,
inference(superposition,[],[f5107,f4975]) ).
fof(f10762,plain,
! [X2,X0] : inverse(multiply(inverse(X0),X0)) = inverse(inverse(multiply(inverse(X2),X2))),
inference(superposition,[],[f10434,f5958]) ).
fof(f11395,plain,
! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(X2),X2)) = inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(X0),X0)),inverse(multiply(X3,inverse(multiply(inverse(X4),X4)))))))),multiply(X1,X3))),
inference(superposition,[],[f3999,f10762]) ).
fof(f11428,plain,
! [X2,X0] : inverse(multiply(inverse(X2),X2)) = multiply(inverse(X0),X0),
inference(forward_demodulation,[],[f11395,f3999]) ).
fof(f11489,plain,
! [X2,X0,X1] : multiply(inverse(X2),X2) = inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X1),X1))),
inference(superposition,[],[f11428,f4974]) ).
fof(f11518,plain,
! [X2,X0] : multiply(inverse(X2),X2) = inverse(inverse(multiply(inverse(X0),X0))),
inference(superposition,[],[f11428,f11428]) ).
fof(f11567,plain,
! [X2,X0,X1] : inverse(multiply(inverse(X1),X1)) = multiply(inverse(inverse(multiply(inverse(X0),X0))),multiply(inverse(X2),X2)),
inference(superposition,[],[f11428,f10762]) ).
fof(f11569,plain,
! [X2,X0,X1] : inverse(multiply(inverse(X1),X1)) = multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X2),X2)),
inference(superposition,[],[f11428,f4974]) ).
fof(f12486,plain,
! [X2,X0] : inverse(multiply(multiply(inverse(X0),X0),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))) = X2,
inference(superposition,[],[f507,f11518]) ).
fof(f34568,plain,
! [X2,X0,X1] : inverse(multiply(multiply(inverse(X1),X1),inverse(multiply(X2,multiply(inverse(X0),X0))))) = X2,
inference(superposition,[],[f12486,f11428]) ).
fof(f54610,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X2),inverse(multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3))))))))),inverse(multiply(inverse(X0),X0)))) = X2,
inference(superposition,[],[f1,f11567]) ).
fof(f54623,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(inverse(X2)),inverse(multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3))))))))),inverse(multiply(inverse(X0),X0))) = X2,
inference(superposition,[],[f15,f11567]) ).
fof(f54624,plain,
! [X2,X3,X0,X1] : inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(X2,inverse(multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3))))))))),inverse(multiply(inverse(X0),X0))))) = X2,
inference(superposition,[],[f17,f11567]) ).
fof(f54699,plain,
! [X2,X3,X0,X1] : inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(X2,inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(X0),X0))))) = X2,
inference(forward_demodulation,[],[f54624,f34568]) ).
fof(f54700,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(inverse(X2)),inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(X0),X0))) = X2,
inference(forward_demodulation,[],[f54623,f34568]) ).
fof(f54713,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X2),inverse(multiply(inverse(X3),X3)))))),inverse(multiply(inverse(X0),X0)))) = X2,
inference(forward_demodulation,[],[f54610,f34568]) ).
fof(f54777,plain,
! [X2,X0] : inverse(inverse(multiply(X2,inverse(multiply(inverse(X0),X0))))) = X2,
inference(forward_demodulation,[],[f54699,f10434]) ).
fof(f54778,plain,
! [X2,X0] : multiply(inverse(inverse(X2)),inverse(multiply(inverse(X0),X0))) = X2,
inference(forward_demodulation,[],[f54700,f10434]) ).
fof(f54791,plain,
! [X2,X0] : inverse(multiply(inverse(X2),inverse(multiply(inverse(X0),X0)))) = X2,
inference(forward_demodulation,[],[f54713,f10434]) ).
fof(f54946,plain,
! [X0,X1] : inverse(inverse(multiply(X1,multiply(inverse(X0),X0)))) = X1,
inference(superposition,[],[f54777,f11489]) ).
fof(f56163,plain,
! [X0,X1] : multiply(inverse(inverse(X1)),multiply(inverse(X0),X0)) = X1,
inference(superposition,[],[f54778,f11489]) ).
fof(f57488,plain,
! [X0,X1] : inverse(multiply(inverse(X1),multiply(inverse(X0),X0))) = X1,
inference(superposition,[],[f54791,f11489]) ).
fof(f57751,plain,
! [X0,X1] : inverse(X0) = inverse(multiply(multiply(inverse(X1),X1),X0)),
inference(superposition,[],[f12486,f54791]) ).
fof(f57780,plain,
! [X0,X1] : inverse(inverse(multiply(X1,inverse(multiply(inverse(X1),X1))))) = inverse(inverse(multiply(X0,multiply(inverse(X0),X1)))),
inference(superposition,[],[f17,f54791]) ).
fof(f58047,plain,
! [X0,X1] : inverse(inverse(multiply(X0,multiply(inverse(X0),X1)))) = X1,
inference(forward_demodulation,[],[f57780,f54777]) ).
fof(f59645,plain,
! [X2,X0,X1] : inverse(multiply(inverse(X0),multiply(inverse(X2),X2))) = multiply(multiply(inverse(X1),X1),X0),
inference(superposition,[],[f57488,f57751]) ).
fof(f59647,plain,
! [X0,X1] : multiply(multiply(inverse(X1),X1),X0) = X0,
inference(forward_demodulation,[],[f59645,f57488]) ).
fof(f59962,plain,
! [X2,X0] : multiply(inverse(multiply(inverse(X0),X0)),X2) = X2,
inference(superposition,[],[f59647,f11569]) ).
fof(f65974,plain,
! [X0,X1] : inverse(inverse(multiply(inverse(multiply(inverse(X0),X0)),X1))) = X1,
inference(superposition,[],[f58047,f57751]) ).
fof(f66267,plain,
! [X1] : inverse(inverse(X1)) = X1,
inference(forward_demodulation,[],[f65974,f59962]) ).
fof(f66519,plain,
! [X0,X1] : multiply(X0,inverse(multiply(inverse(X1),X1))) = X0,
inference(superposition,[],[f66267,f54777]) ).
fof(f66520,plain,
! [X0,X1] : multiply(X0,multiply(inverse(X1),X1)) = X0,
inference(superposition,[],[f66267,f54946]) ).
fof(f66521,plain,
! [X0,X1] : multiply(X1,multiply(inverse(X1),X0)) = X0,
inference(superposition,[],[f66267,f58047]) ).
fof(f66704,plain,
! [X0,X1] : multiply(inverse(X1),X1) = multiply(X0,inverse(X0)),
inference(superposition,[],[f4975,f66267]) ).
fof(f66857,plain,
! [X0,X1] : multiply(inverse(inverse(X1)),multiply(X0,inverse(X0))) = X1,
inference(superposition,[],[f56163,f66267]) ).
fof(f66861,plain,
! [X0,X1] : inverse(inverse(multiply(inverse(X0),multiply(X0,X1)))) = X1,
inference(superposition,[],[f58047,f66267]) ).
fof(f66864,plain,
! [X0,X1] : multiply(inverse(X0),multiply(X0,X1)) = X1,
inference(forward_demodulation,[],[f66861,f66267]) ).
fof(f66865,plain,
! [X0,X1] : multiply(X1,multiply(X0,inverse(X0))) = X1,
inference(forward_demodulation,[],[f66857,f66267]) ).
fof(f67402,plain,
! [X2,X0,X1] : multiply(inverse(inverse(multiply(inverse(multiply(X0,inverse(X1))),X0))),inverse(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2)))))) = X1,
inference(superposition,[],[f506,f66520]) ).
fof(f67403,plain,
! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(X0,X1)),X0))),inverse(multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))))))) = X1,
inference(superposition,[],[f507,f66520]) ).
fof(f67926,plain,
! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(X0,X1)),X0))),inverse(multiply(inverse(X2),X2)))) = X1,
inference(forward_demodulation,[],[f67403,f34568]) ).
fof(f67927,plain,
! [X2,X0,X1] : multiply(inverse(inverse(multiply(inverse(multiply(X0,inverse(X1))),X0))),inverse(multiply(inverse(X2),X2))) = X1,
inference(forward_demodulation,[],[f67402,f34568]) ).
fof(f68164,plain,
! [X0,X1] : inverse(multiply(inverse(multiply(X0,X1)),X0)) = X1,
inference(forward_demodulation,[],[f67926,f54791]) ).
fof(f68165,plain,
! [X0,X1] : multiply(inverse(multiply(X0,inverse(X1))),X0) = X1,
inference(forward_demodulation,[],[f67927,f54778]) ).
fof(f70956,plain,
! [X0,X1] : inverse(inverse(inverse(multiply(X0,inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(inverse(inverse(X0)),inverse(X0))))))))))) = X1,
inference(superposition,[],[f17,f66865]) ).
fof(f71032,plain,
! [X0,X1] : inverse(multiply(X0,inverse(multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(inverse(inverse(X0)),inverse(X0))))))))) = X1,
inference(forward_demodulation,[],[f70956,f66267]) ).
fof(f71453,plain,
! [X0,X1] : inverse(multiply(X0,inverse(multiply(X1,X0)))) = X1,
inference(forward_demodulation,[],[f71032,f54791]) ).
fof(f74368,plain,
! [X2,X0,X1] : multiply(inverse(inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(X1,X2)))),inverse(multiply(X2,inverse(multiply(inverse(X2),X2))))) = X1,
inference(superposition,[],[f506,f66704]) ).
fof(f74423,plain,
! [X2,X0,X1] : inverse(inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(multiply(X1,inverse(multiply(X2,inverse(multiply(inverse(X2),X2))))),X2)))) = X1,
inference(superposition,[],[f17,f66704]) ).
fof(f74616,plain,
! [X2,X0,X1] : multiply(inverse(multiply(inverse(X0),X0)),multiply(multiply(X1,inverse(multiply(X2,inverse(multiply(inverse(X2),X2))))),X2)) = X1,
inference(forward_demodulation,[],[f74423,f66267]) ).
fof(f74658,plain,
! [X2,X0,X1] : multiply(inverse(inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(X1,X2)))),inverse(X2)) = X1,
inference(forward_demodulation,[],[f74368,f66519]) ).
fof(f75309,plain,
! [X2,X1] : multiply(multiply(X1,inverse(multiply(X2,inverse(multiply(inverse(X2),X2))))),X2) = X1,
inference(forward_demodulation,[],[f74616,f59962]) ).
fof(f75345,plain,
! [X2,X0,X1] : multiply(multiply(inverse(multiply(inverse(X0),X0)),multiply(X1,X2)),inverse(X2)) = X1,
inference(forward_demodulation,[],[f74658,f66267]) ).
fof(f75723,plain,
! [X2,X1] : multiply(multiply(X1,inverse(X2)),X2) = X1,
inference(forward_demodulation,[],[f75309,f66519]) ).
fof(f75752,plain,
! [X2,X1] : multiply(multiply(X1,X2),inverse(X2)) = X1,
inference(forward_demodulation,[],[f75345,f59962]) ).
fof(f77135,plain,
! [X0,X1] : inverse(X1) = multiply(X0,inverse(multiply(X1,X0))),
inference(superposition,[],[f75752,f66864]) ).
fof(f82065,plain,
! [X0,X1] : multiply(X1,X0) = inverse(multiply(inverse(X0),inverse(X1))),
inference(superposition,[],[f68164,f66864]) ).
fof(f82094,plain,
! [X0,X1] : inverse(multiply(inverse(X0),X1)) = multiply(inverse(X1),X0),
inference(superposition,[],[f68164,f66521]) ).
fof(f83755,plain,
! [X0,X1] : inverse(multiply(X1,inverse(X0))) = multiply(X0,inverse(X1)),
inference(superposition,[],[f75752,f68165]) ).
fof(f122381,plain,
! [X2,X3,X0,X1,X6,X4,X5] : multiply(inverse(multiply(X3,multiply(inverse(multiply(X5,inverse(multiply(X1,inverse(multiply(X6,inverse(multiply(inverse(X6),X6)))))))),multiply(X5,X6)))),multiply(X3,inverse(multiply(inverse(X4),inverse(multiply(multiply(inverse(multiply(X5,inverse(multiply(X1,inverse(multiply(X6,inverse(multiply(inverse(X6),X6)))))))),multiply(X5,X6)),inverse(multiply(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X0,X2)),multiply(inverse(multiply(X5,inverse(multiply(X1,inverse(multiply(X6,inverse(multiply(inverse(X6),X6)))))))),multiply(X5,X6)))))))))) = X4,
inference(forward_demodulation,[],[f20,f82094]) ).
fof(f122382,plain,
! [X2,X3,X0,X1,X6,X4,X5] : multiply(inverse(multiply(X3,multiply(inverse(multiply(X5,inverse(multiply(X1,inverse(multiply(X6,inverse(multiply(inverse(X6),X6)))))))),multiply(X5,X6)))),multiply(X3,multiply(multiply(multiply(inverse(multiply(X5,inverse(multiply(X1,inverse(multiply(X6,inverse(multiply(inverse(X6),X6)))))))),multiply(X5,X6)),inverse(multiply(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X0,X2)),multiply(inverse(multiply(X5,inverse(multiply(X1,inverse(multiply(X6,inverse(multiply(inverse(X6),X6)))))))),multiply(X5,X6))))),X4))) = X4,
inference(forward_demodulation,[],[f122381,f82065]) ).
fof(f122383,plain,
! [X2,X3,X0,X1,X6,X4,X5] : multiply(inverse(multiply(X3,multiply(inverse(multiply(X5,inverse(multiply(X1,inverse(multiply(X6,inverse(multiply(inverse(X6),X6)))))))),multiply(X5,X6)))),multiply(X3,multiply(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X0,X2))),X4))) = X4,
inference(forward_demodulation,[],[f122382,f77135]) ).
fof(f122384,plain,
! [X3,X1,X6,X4,X5] : multiply(inverse(multiply(X3,multiply(inverse(multiply(X5,inverse(multiply(X1,inverse(multiply(X6,inverse(multiply(inverse(X6),X6)))))))),multiply(X5,X6)))),multiply(X3,multiply(X1,X4))) = X4,
inference(forward_demodulation,[],[f122383,f1]) ).
fof(f122385,plain,
! [X3,X1,X6,X4,X5] : multiply(inverse(multiply(X3,multiply(multiply(multiply(X1,inverse(multiply(X6,inverse(multiply(inverse(X6),X6))))),inverse(X5)),multiply(X5,X6)))),multiply(X3,multiply(X1,X4))) = X4,
inference(forward_demodulation,[],[f122384,f83755]) ).
fof(f122386,plain,
! [X3,X1,X6,X4,X5] : multiply(inverse(multiply(X3,multiply(multiply(multiply(X1,inverse(X6)),inverse(X5)),multiply(X5,X6)))),multiply(X3,multiply(X1,X4))) = X4,
inference(forward_demodulation,[],[f122385,f71453]) ).
fof(f122694,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X2,multiply(multiply(multiply(X0,inverse(X1)),inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X1))))),multiply(multiply(inverse(X3),X3),X1)))),multiply(X2,multiply(X0,X4))) = X4,
inference(superposition,[],[f122386,f4667]) ).
fof(f123768,plain,
! [X2,X0,X1,X4] : multiply(inverse(multiply(X2,multiply(multiply(multiply(X0,inverse(X1)),inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X1))))),X1))),multiply(X2,multiply(X0,X4))) = X4,
inference(forward_demodulation,[],[f122694,f59647]) ).
fof(f124454,plain,
! [X2,X0,X1,X4] : multiply(inverse(multiply(X2,multiply(multiply(X0,inverse(X1)),X1))),multiply(X2,multiply(X0,X4))) = X4,
inference(forward_demodulation,[],[f123768,f66519]) ).
fof(f124994,plain,
! [X2,X0,X4] : multiply(inverse(multiply(X2,X0)),multiply(X2,multiply(X0,X4))) = X4,
inference(forward_demodulation,[],[f124454,f75723]) ).
fof(f130287,plain,
! [X2,X0,X1] : multiply(X1,multiply(X2,X0)) = inverse(inverse(multiply(multiply(X1,X2),X0))),
inference(superposition,[],[f58047,f124994]) ).
fof(f130522,plain,
! [X2,X0,X1] : multiply(X1,multiply(X2,X0)) = multiply(multiply(X1,X2),X0),
inference(forward_demodulation,[],[f130287,f66267]) ).
fof(f132030,plain,
multiply(a3,multiply(b3,c3)) != multiply(a3,multiply(b3,c3)),
inference(superposition,[],[f2,f130522]) ).
fof(f132300,plain,
$false,
inference(trivial_inequality_removal,[],[f132030]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GRP420-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.03/0.31 % Computer : n012.cluster.edu
% 0.03/0.31 % Model : x86_64 x86_64
% 0.03/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.03/0.31 % Memory : 8046.5625MB
% 0.03/0.31 % OS : Linux 6.8.0-71-generic
% 0.03/0.31 % CPULimit : 300
% 0.03/0.31 % WCLimit : 300
% 0.03/0.31 % DateTime : Sun Sep 27 10:03:35 UTC 2026
% 0.03/0.31 % CPUTime :
% 0.03/0.31 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.03/0.33 Running first-order model finding
% 0.03/0.34 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 22.17/3.55 % (2135574)Will run a generic schedule for satisfiability detection.
% 22.17/3.55 % (2135582)dis+10_1_sil=32000:sp=arity:random_seed=4269441590:i=103:fgj=on_3000 on theBenchmark for (3000ds/103Mi)
% 22.17/3.55 % (2135580)% WARNING: option uhcvi not known.
% 22.17/3.55 % (2135580)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=3054053367:i=135531:add=off:rawr=on_3000 on theBenchmark for (3000ds/135531Mi)
% 22.17/3.55 % (2135579)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=259392174_3000 on theBenchmark for (3000ds/0Mi)
% 22.17/3.55 % (2135581)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1662300319:i=88024:add=on:rawr=on_3000 on theBenchmark for (3000ds/88024Mi)
% 22.17/3.55 % (2135584)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3776318620:i=131_3000 on theBenchmark for (3000ds/131Mi)
% 22.17/3.55 % (2135583)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2681459852:i=116_3000 on theBenchmark for (3000ds/116Mi)
% 22.17/3.55 % (2135585)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=242855986:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_3000 on theBenchmark for (3000ds/159Mi)
% 22.17/3.55 % TRYING [1]
% 22.17/3.55 % TRYING [2]
% 22.17/3.55 % TRYING [3]
% 22.17/3.55 % TRYING [4]
% 22.17/3.55 % (2135582)Instruction limit reached!
% 22.17/3.55 % (2135582)------------------------------
% 22.17/3.55 % (2135582)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.17/3.55 % (2135582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.17/3.55 % (2135582)CaDiCaL version: 2.1.3
% 22.17/3.55 % (2135582)Termination reason: Instruction limit
% 22.17/3.55 % (2135582)Termination phase: Saturation
% 22.17/3.55 % (2135582)Time elapsed: 0.040 s
% 22.17/3.55 % (2135582)Peak memory usage: 12 MB
% 22.17/3.55 % (2135582)Instructions burned: 104 (million)
% 22.17/3.55 % (2135598)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=442947264:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 22.17/3.55 % TRYING [1]
% 22.17/3.55 % TRYING [2]
% 22.17/3.55 % TRYING [3]
% 22.17/3.55 % (2135583)Instruction limit reached!
% 22.17/3.55 % (2135583)------------------------------
% 22.17/3.55 % (2135583)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.17/3.55 % (2135583)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.17/3.55 % (2135583)CaDiCaL version: 2.1.3
% 22.17/3.55 % (2135583)Termination reason: Instruction limit
% 22.17/3.55 % (2135583)Termination phase: Saturation
% 22.17/3.55 % (2135583)Time elapsed: 0.055 s
% 22.17/3.55 % (2135583)Peak memory usage: 12 MB
% 22.17/3.55 % (2135583)Instructions burned: 116 (million)
% 22.17/3.55 % (2135584)Instruction limit reached!
% 22.17/3.55 % (2135584)------------------------------
% 22.17/3.55 % (2135584)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.17/3.55 % (2135584)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.17/3.55 % (2135584)CaDiCaL version: 2.1.3
% 22.17/3.55 % (2135584)Termination reason: Instruction limit
% 22.17/3.55 % (2135584)Termination phase: Saturation
% 22.17/3.55 % (2135584)Time elapsed: 0.056 s
% 22.17/3.55 % (2135584)Peak memory usage: 13 MB
% 22.17/3.55 % (2135584)Instructions burned: 132 (million)
% 22.17/3.55 % TRYING [4]
% 22.17/3.55 % (2135600)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1436757322:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 22.17/3.55 % (2135601)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2120998498:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 22.17/3.55 % (2135585)Instruction limit reached!
% 22.17/3.55 % (2135585)------------------------------
% 22.17/3.55 % (2135585)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.17/3.55 % (2135585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.17/3.55 % (2135585)CaDiCaL version: 2.1.3
% 22.17/3.55 % (2135585)Termination reason: Instruction limit
% 22.17/3.55 % (2135585)Termination phase: Saturation
% 22.17/3.55 % (2135585)Time elapsed: 0.077 s
% 22.17/3.55 % (2135585)Peak memory usage: 13 MB
% 22.17/3.55 % (2135585)Instructions burned: 160 (million)
% 22.17/3.55 % (2135604)ott-21_1_sil=16000:fs=off:random_seed=3733860992:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 22.17/3.55 % (2135600)Instruction limit reached!
% 22.17/3.55 % (2135600)------------------------------
% 22.17/3.55 % (2135600)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.17/3.55 % (2135600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.61/6.70 % (2135600)CaDiCaL version: 2.1.3
% 44.61/6.70 % (2135600)Termination reason: Instruction limit
% 44.61/6.70 % (2135600)Termination phase: Saturation
% 44.61/6.70 % (2135600)Time elapsed: 0.062 s
% 44.61/6.70 % (2135600)Peak memory usage: 13 MB
% 44.61/6.70 % (2135600)Instructions burned: 132 (million)
% 44.61/6.70 % (2135608)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1207908746:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 44.61/6.70 % (2135604)Instruction limit reached!
% 44.61/6.70 % (2135604)------------------------------
% 44.61/6.70 % (2135604)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.61/6.70 % (2135604)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.61/6.70 % (2135604)CaDiCaL version: 2.1.3
% 44.61/6.70 % (2135604)Termination reason: Instruction limit
% 44.61/6.70 % (2135604)Termination phase: Saturation
% 44.61/6.70 % (2135604)Time elapsed: 0.078 s
% 44.61/6.70 % (2135604)Peak memory usage: 11 MB
% 44.61/6.70 % (2135604)Instructions burned: 181 (million)
% 44.61/6.70 % (2135610)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2352241921:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 44.61/6.70 % TRYING [1]
% 44.61/6.70 % TRYING [2]
% 44.61/6.70 % TRYING [3]
% 44.61/6.70 % TRYING [4]
% 44.61/6.70 % (2135601)Instruction limit reached!
% 44.61/6.70 % (2135601)------------------------------
% 44.61/6.70 % (2135601)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.61/6.70 % (2135601)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.61/6.70 % (2135601)CaDiCaL version: 2.1.3
% 44.61/6.70 % (2135601)Termination reason: Instruction limit
% 44.61/6.70 % (2135601)Termination phase: Saturation
% 44.61/6.70 % (2135601)Time elapsed: 0.268 s
% 44.61/6.70 % (2135601)Peak memory usage: 16 MB
% 44.61/6.70 % (2135601)Instructions burned: 686 (million)
% 44.61/6.70 % (2135618)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=619562203:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 44.61/6.70 % (2135598)Instruction limit reached!
% 44.61/6.70 % (2135598)------------------------------
% 44.61/6.70 % (2135598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.61/6.70 % (2135598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.61/6.70 % (2135598)CaDiCaL version: 2.1.3
% 44.61/6.70 % (2135598)Termination reason: Instruction limit
% 44.61/6.70 % (2135598)Termination phase: Finite model building SAT solving
% 44.61/6.70 % (2135598)Time elapsed: 0.321 s
% 44.61/6.70 % (2135598)Peak memory usage: 12 MB
% 44.61/6.70 % (2135598)Instructions burned: 715 (million)
% 44.61/6.70 % (2135608)Instruction limit reached!
% 44.61/6.70 % (2135608)------------------------------
% 44.61/6.70 % (2135608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.61/6.70 % (2135608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.61/6.70 % (2135608)CaDiCaL version: 2.1.3
% 44.61/6.70 % (2135608)Termination reason: Instruction limit
% 44.61/6.70 % (2135608)Termination phase: Saturation
% 44.61/6.70 % (2135608)Time elapsed: 0.223 s
% 44.61/6.70 % (2135608)Peak memory usage: 14 MB
% 44.61/6.70 % (2135608)Instructions burned: 485 (million)
% 44.61/6.70 % (2135620)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=262375616:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi)
% 44.61/6.70 % (2135621)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1133277065:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi)
% 44.61/6.70 % TRYING [14]
% 44.61/6.70 % (2135610)Instruction limit reached!
% 44.61/6.70 % (2135610)------------------------------
% 44.61/6.70 % (2135610)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.61/6.70 % (2135610)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.61/6.70 % (2135610)CaDiCaL version: 2.1.3
% 44.61/6.70 % (2135610)Termination reason: Instruction limit
% 44.61/6.70 % (2135610)Termination phase: Finite model building SAT solving
% 44.61/6.70 % (2135610)Time elapsed: 0.397 s
% 44.61/6.70 % (2135610)Peak memory usage: 11 MB
% 44.61/6.70 % (2135610)Instructions burned: 865 (million)
% 44.61/6.70 % (2135626)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=784225223:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 44.61/6.70 % (2135621)Instruction limit reached!
% 44.61/6.70 % (2135621)------------------------------
% 44.61/6.70 % (2135621)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.47/9.86 % (2135621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.47/9.86 % (2135621)CaDiCaL version: 2.1.3
% 66.47/9.86 % (2135621)Termination reason: Instruction limit
% 66.47/9.86 % (2135621)Termination phase: Saturation
% 66.47/9.86 % (2135621)Time elapsed: 0.303 s
% 66.47/9.86 % (2135621)Peak memory usage: 18 MB
% 66.47/9.86 % (2135621)Instructions burned: 693 (million)
% 66.47/9.86 % (2135632)fmb+10_1_sil=64000:random_seed=904635377:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 66.47/9.86 % TRYING [1]
% 66.47/9.86 % TRYING [2]
% 66.47/9.86 % TRYING [3]
% 66.47/9.86 % TRYING [4]
% 66.47/9.86 % (2135620)Instruction limit reached!
% 66.47/9.86 % (2135620)------------------------------
% 66.47/9.86 % (2135620)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.47/9.86 % (2135620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.47/9.86 % (2135620)CaDiCaL version: 2.1.3
% 66.47/9.86 % (2135620)Termination reason: Instruction limit
% 66.47/9.86 % (2135620)Termination phase: Finite model building constraint generation
% 66.47/9.86 % (2135620)Time elapsed: 0.352 s
% 66.47/9.86 % (2135620)Peak memory usage: 80 MB
% 66.47/9.86 % (2135620)Instructions burned: 890 (million)
% 66.47/9.86 % (2135634)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2720313972:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi)
% 66.47/9.86 % TRYING [20]
% 66.47/9.86 % (2135618)Instruction limit reached!
% 66.47/9.86 % (2135618)------------------------------
% 66.47/9.86 % (2135618)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.47/9.86 % (2135618)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.47/9.86 % (2135618)CaDiCaL version: 2.1.3
% 66.47/9.86 % (2135618)Termination reason: Instruction limit
% 66.47/9.86 % (2135618)Termination phase: Saturation
% 66.47/9.86 % (2135618)Time elapsed: 0.492 s
% 66.47/9.86 % (2135618)Peak memory usage: 17 MB
% 66.47/9.86 % (2135618)Instructions burned: 1181 (million)
% 66.47/9.86 % (2135640)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=781249090:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi)
% 66.47/9.86 % TRYING [8]
% 66.47/9.86 % (2135626)Instruction limit reached!
% 66.47/9.86 % (2135626)------------------------------
% 66.47/9.86 % (2135626)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.47/9.86 % (2135626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.47/9.86 % (2135626)CaDiCaL version: 2.1.3
% 66.47/9.86 % (2135626)Termination reason: Instruction limit
% 66.47/9.86 % (2135626)Termination phase: Saturation
% 66.47/9.86 % (2135626)Time elapsed: 0.366 s
% 66.47/9.86 % (2135626)Peak memory usage: 15 MB
% 66.47/9.86 % (2135626)Instructions burned: 879 (million)
% 66.47/9.86 % (2135642)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3697271709:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 66.47/9.86 % (2135640)Instruction limit reached!
% 66.47/9.86 % (2135640)------------------------------
% 66.47/9.86 % (2135640)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.47/9.86 % (2135640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.47/9.86 % (2135640)CaDiCaL version: 2.1.3
% 66.47/9.86 % (2135640)Termination reason: Instruction limit
% 66.47/9.86 % (2135640)Termination phase: Finite model building SAT solving
% 66.47/9.86 % (2135640)Time elapsed: 0.431 s
% 66.47/9.86 % (2135640)Peak memory usage: 37 MB
% 66.47/9.86 % (2135640)Instructions burned: 922 (million)
% 66.47/9.86 % (2135646)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=715744043:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 66.47/9.86 % TRYING [5]
% 66.47/9.86 % (2135646)Instruction limit reached!
% 66.47/9.86 % (2135646)------------------------------
% 66.47/9.86 % (2135646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.47/9.86 % (2135646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.47/9.86 % (2135646)CaDiCaL version: 2.1.3
% 66.47/9.86 % (2135646)Termination reason: Instruction limit
% 66.47/9.86 % (2135646)Termination phase: Saturation
% 66.47/9.86 % (2135646)Time elapsed: 0.738 s
% 66.47/9.86 % (2135646)Peak memory usage: 28 MB
% 66.47/9.86 % (2135646)Instructions burned: 1472 (million)
% 66.47/9.86 % (2135650)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=345898077:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 66.47/9.86 % TRYING [77]
% 66.47/9.86 % (2135642)Instruction limit reached!
% 66.47/9.86 % (2135642)------------------------------
% 66.47/9.86 % (2135642)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.47/9.86 % (2135642)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.47/9.86 % (2135642)CaDiCaL version: 2.1.3
% 66.47/9.86 % (2135642)Termination reason: Instruction limit
% 66.47/9.86 % (2135642)Termination phase: Saturation
% 66.47/9.86 % (2135642)Time elapsed: 2.202 s
% 66.47/9.86 % (2135642)Peak memory usage: 35 MB
% 66.47/9.86 % (2135642)Instructions burned: 5132 (million)
% 66.47/9.86 % (2135654)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3982314215:fmbsr=2.30978:i=2174_2967 on theBenchmark for (2967ds/2174Mi)
% 66.47/9.86 % TRYING [16]
% 66.47/9.86 % (2135654)Instruction limit reached!
% 66.47/9.86 % (2135654)------------------------------
% 66.47/9.86 % (2135654)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.47/9.86 % (2135654)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.47/9.86 % (2135654)CaDiCaL version: 2.1.3
% 66.47/9.86 % (2135654)Termination reason: Instruction limit
% 66.47/9.86 % (2135654)Termination phase: Finite model building constraint generation
% 66.47/9.86 % (2135654)Time elapsed: 0.562 s
% 66.47/9.86 % (2135654)Peak memory usage: 154 MB
% 66.47/9.86 % (2135654)Instructions burned: 2174 (million)
% 66.47/9.86 % (2135656)ott-2_1_sil=16000:newcnf=on:random_seed=1448993832:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2962 on theBenchmark for (2962ds/869Mi)
% 66.47/9.86 % (2135656)Instruction limit reached!
% 66.47/9.86 % (2135656)------------------------------
% 66.47/9.86 % (2135656)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.47/9.86 % (2135656)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.47/9.86 % (2135656)CaDiCaL version: 2.1.3
% 66.47/9.86 % (2135656)Termination reason: Instruction limit
% 66.47/9.86 % (2135656)Termination phase: Saturation
% 66.47/9.86 % (2135656)Time elapsed: 0.343 s
% 66.47/9.86 % (2135656)Peak memory usage: 21 MB
% 66.47/9.86 % (2135656)Instructions burned: 871 (million)
% 66.47/9.86 % (2135662)ott+10_1_sil=32000:tgt=ground:random_seed=4036858463:i=5114:av=off_2958 on theBenchmark for (2958ds/5114Mi)
% 66.47/9.86 % (2135650)Instruction limit reached!
% 66.47/9.86 % (2135650)------------------------------
% 66.47/9.86 % (2135650)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.47/9.86 % (2135650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.47/9.86 % (2135650)CaDiCaL version: 2.1.3
% 66.47/9.86 % (2135650)Termination reason: Instruction limit
% 66.47/9.86 % (2135650)Termination phase: Finite model building constraint generation
% 66.47/9.86 % (2135650)Time elapsed: 2.229 s
% 66.47/9.86 % (2135650)Peak memory usage: 523 MB
% 66.47/9.86 % (2135650)Instructions burned: 6324 (million)
% 66.47/9.86 % (2135666)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1794001344:i=54282_2956 on theBenchmark for (2956ds/54282Mi)
% 66.47/9.86 % TRYING [1]
% 66.47/9.86 % TRYING [2]
% 66.47/9.86 % TRYING [3]
% 66.47/9.86 % TRYING [4]
% 66.47/9.86 % (2135634)Instruction limit reached!
% 66.47/9.86 % (2135634)------------------------------
% 66.47/9.86 % (2135634)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.47/9.86 % (2135634)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.47/9.86 % (2135634)CaDiCaL version: 2.1.3
% 66.47/9.86 % (2135634)Termination reason: Instruction limit
% 66.47/9.86 % (2135634)Termination phase: Finite model building constraint generation
% 66.47/9.86 % (2135634)Time elapsed: 3.821 s
% 66.47/9.86 % (2135634)Peak memory usage: 659 MB
% 66.47/9.86 % (2135634)Instructions burned: 9515 (million)
% 66.47/9.86 % (2135668)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=860037297:i=3512:aac=none_2952 on theBenchmark for (2952ds/3512Mi)
% 66.47/9.86 % TRYING [5]
% 66.47/9.86 % TRYING [5]
% 66.47/9.86 % (2135668)Instruction limit reached!
% 66.47/9.86 % (2135668)------------------------------
% 66.47/9.86 % (2135668)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.47/9.86 % (2135668)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.47/9.86 % (2135668)CaDiCaL version: 2.1.3
% 66.47/9.86 % (2135668)Termination reason: Instruction limit
% 66.47/9.86 % (2135668)Termination phase: Saturation
% 66.47/9.86 % (2135668)Time elapsed: 1.536 s
% 66.47/9.86 % (2135668)Peak memory usage: 31 MB
% 66.47/9.86 % (2135668)Instructions burned: 3514 (million)
% 66.47/9.86 % (2135674)dis+21_1_sil=32000:sas=cadical:random_seed=783019303:i=3773:amm=off_2937 on theBenchmark for (2937ds/3773Mi)
% 66.47/9.86 % (2135662)Instruction limit reached!
% 66.47/9.86 % (2135662)------------------------------
% 66.47/9.86 % (2135662)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.47/9.86 % (2135662)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.47/9.86 % (2135662)CaDiCaL version: 2.1.3
% 66.47/9.86 % (2135662)Termination reason: Instruction limit
% 66.47/9.86 % (2135662)Termination phase: Saturation
% 66.47/9.86 % (2135662)Time elapsed: 2.190 s
% 66.47/9.86 % (2135662)Peak memory usage: 37 MB
% 66.47/9.86 % (2135662)Instructions burned: 5114 (million)
% 66.47/9.86 % (2135678)ott+11_1_sil=16000:gs=on:random_seed=419916270:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2936 on theBenchmark for (2936ds/2251Mi)
% 66.47/9.86 % (2135678)Instruction limit reached!
% 66.47/9.86 % (2135678)------------------------------
% 66.47/9.86 % (2135678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.47/9.86 % (2135678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.47/9.86 % (2135678)CaDiCaL version: 2.1.3
% 66.47/9.86 % (2135678)Termination reason: Instruction limit
% 66.47/9.86 % (2135678)Termination phase: Saturation
% 66.47/9.86 % (2135678)Time elapsed: 0.976 s
% 66.47/9.86 % (2135678)Peak memory usage: 32 MB
% 66.47/9.86 % (2135678)Instructions burned: 2253 (million)
% 66.47/9.86 % (2135682)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1894537275:fmbsr=1.6:i=67534_2926 on theBenchmark for (2926ds/67534Mi)
% 66.47/9.86 % TRYING [7]
% 66.47/9.86 % (2135674)Instruction limit reached!
% 66.47/9.86 % (2135674)------------------------------
% 66.47/9.86 % (2135674)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.47/9.86 % (2135674)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.47/9.86 % (2135674)CaDiCaL version: 2.1.3
% 66.47/9.86 % (2135674)Termination reason: Instruction limit
% 66.47/9.86 % (2135674)Termination phase: Saturation
% 66.47/9.86 % (2135674)Time elapsed: 1.490 s
% 66.47/9.86 % (2135674)Peak memory usage: 32 MB
% 66.47/9.86 % (2135674)Instructions burned: 3774 (million)
% 66.47/9.86 % (2135684)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3959760406:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2922 on theBenchmark for (2922ds/4591Mi)
% 66.47/9.86 % (2135581) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2135574-2135581"...
% 66.47/9.86 % (2135581)...printing done.
% 66.47/9.86 % (2135581)Refutation found. Thanks to Tanya!
% 66.47/9.86 % SZS status Unsatisfiable for theBenchmark
% 66.47/9.86 % SZS output start Proof for theBenchmark
% See solution above
% 66.47/9.86 % (2135581)------------------------------
% 66.47/9.86 % (2135581)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 66.47/9.86 % (2135581)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 66.47/9.86 % (2135581)CaDiCaL version: 2.1.3
% 66.47/9.86 % (2135581)Termination reason: Refutation
% 66.47/9.86 % (2135581)Time elapsed: 9.474 s
% 66.47/9.86 % (2135581)Peak memory usage: 80 MB
% 66.47/9.86 % (2135581)Instructions burned: 29603 (million)
% 66.47/9.86 % (2135574)Success in time 9.52 s
% 66.47/9.86 % Vampire exiting
%------------------------------------------------------------------------------