%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GRP410-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 : n019.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:44 AM UTC 2026
% Result : Unsatisfiable 13.62s 3.97s
% Output : Refutation 13.62s
% Verified :
% SZS Type : Refutation
% Derivation depth : 43
% Number of leaves : 5
% Syntax : Number of formulae : 161 ( 161 unt; 3 def)
% Number of atoms : 161 ( 160 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 3 ( 3 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 3 avg)
% Maximal term depth : 18 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 7 ( 7 usr; 5 con; 0-2 aty)
% Number of variables : 331 ( 331 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,X2)))),multiply(X0,inverse(X2))),inverse(multiply(inverse(X2),X2))) = X1,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,negated_conjecture,
multiply(multiply(inverse(b2),b2),a2) != a2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_these_axioms_2) ).
fof(f3,plain,
a2 != multiply(multiply(inverse(b2),b2),a2),
inference(reorient_equations,[],[f2]) ).
fof(f4,definition,
sF0 = inverse(b2),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f5,plain,
inverse(b2) = sF0,
inference(reorient_equations,[],[f4]) ).
fof(f6,definition,
sF1 = multiply(sF0,b2),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f7,plain,
multiply(sF0,b2) = sF1,
inference(reorient_equations,[],[f6]) ).
fof(f8,definition,
sF2 = multiply(sF1,a2),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f9,plain,
multiply(sF1,a2) = sF2,
inference(reorient_equations,[],[f8]) ).
fof(f10,plain,
a2 != sF2,
inference(definition_folding,[],[f3,f9,f7,f5]) ).
fof(f11,plain,
! [X0] : sF0 = multiply(multiply(inverse(multiply(X0,inverse(sF1))),multiply(X0,inverse(b2))),inverse(multiply(inverse(b2),b2))),
inference(superposition,[],[f1,f7]) ).
fof(f12,plain,
! [X0] : sF1 = multiply(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2))),inverse(multiply(inverse(a2),a2))),
inference(superposition,[],[f1,f9]) ).
fof(f13,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X2,inverse(multiply(X0,X3)))),multiply(X2,inverse(X3))) = multiply(multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,inverse(inverse(multiply(inverse(X3),X3))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))),
inference(superposition,[],[f1,f1]) ).
fof(f14,plain,
! [X2,X0,X1] : inverse(X2) = multiply(multiply(inverse(X0),multiply(multiply(inverse(multiply(X1,inverse(multiply(X0,X2)))),multiply(X1,inverse(X2))),inverse(X2))),inverse(multiply(inverse(X2),X2))),
inference(superposition,[],[f1,f1]) ).
fof(f15,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(multiply(inverse(multiply(X1,inverse(multiply(X0,X2)))),multiply(X1,inverse(X2))),inverse(multiply(X3,multiply(inverse(X2),X2))))),X0),inverse(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2)))) = X3,
inference(superposition,[],[f1,f1]) ).
fof(f16,plain,
! [X0,X1] : multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,b2)))),multiply(X0,sF0)),inverse(multiply(sF0,b2))) = X1,
inference(superposition,[],[f1,f5]) ).
fof(f17,plain,
! [X0,X1] : multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,b2)))),multiply(X0,sF0)),inverse(sF1)) = X1,
inference(forward_demodulation,[],[f16,f7]) ).
fof(f18,plain,
! [X0] : sF0 = multiply(multiply(inverse(multiply(X0,inverse(sF1))),multiply(X0,sF0)),inverse(multiply(sF0,b2))),
inference(forward_demodulation,[],[f11,f5]) ).
fof(f19,plain,
! [X0] : sF0 = multiply(multiply(inverse(multiply(X0,inverse(sF1))),multiply(X0,sF0)),inverse(sF1)),
inference(forward_demodulation,[],[f18,f7]) ).
fof(f27,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X2,inverse(multiply(X0,b2)))),multiply(X2,sF0)) = multiply(multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,inverse(inverse(sF1)))),inverse(multiply(inverse(inverse(sF1)),inverse(sF1)))),
inference(superposition,[],[f1,f17]) ).
fof(f31,plain,
! [X0,X1] : multiply(inverse(multiply(X1,inverse(sF2))),multiply(X1,inverse(a2))) = multiply(multiply(inverse(multiply(X0,inverse(sF1))),multiply(X0,inverse(inverse(multiply(inverse(a2),a2))))),inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2))))),
inference(superposition,[],[f1,f12]) ).
fof(f49,plain,
! [X2,X0,X1] : inverse(X0) = multiply(multiply(inverse(inverse(X0)),multiply(multiply(inverse(inverse(X0)),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X0)))),multiply(X2,inverse(X0))),inverse(X0))),inverse(X0))),inverse(X0))),inverse(multiply(inverse(X0),X0))),
inference(superposition,[],[f14,f14]) ).
fof(f57,plain,
! [X2,X0,X1] : inverse(X0) = multiply(multiply(inverse(inverse(X0)),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X0)))),multiply(X2,inverse(X0))),inverse(X0))),inverse(X0))),inverse(multiply(inverse(X0),X0))),
inference(superposition,[],[f1,f14]) ).
fof(f89,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(multiply(inverse(inverse(X0)),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X0)))),multiply(X2,inverse(X0))),inverse(X0))),inverse(X0))),inverse(multiply(X3,multiply(inverse(X0),X0))))),inverse(X0)),inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))) = X3,
inference(superposition,[],[f15,f14]) ).
fof(f132,plain,
! [X0,X1] : multiply(inverse(sF1),multiply(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2))),inverse(a2))) = multiply(multiply(inverse(multiply(X1,inverse(inverse(a2)))),multiply(X1,inverse(inverse(multiply(inverse(a2),a2))))),inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2))))),
inference(superposition,[],[f13,f12]) ).
fof(f138,plain,
! [X2,X0,X1] : multiply(inverse(multiply(multiply(inverse(multiply(X0,inverse(sF1))),multiply(X0,sF0)),inverse(multiply(X1,sF1)))),sF0) = multiply(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(inverse(multiply(inverse(sF1),sF1))))),inverse(multiply(inverse(inverse(multiply(inverse(sF1),sF1))),inverse(multiply(inverse(sF1),sF1))))),
inference(superposition,[],[f13,f19]) ).
fof(f150,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X0,inverse(multiply(sF1,X1)))),multiply(X0,inverse(X1))) = multiply(multiply(inverse(sF0),multiply(multiply(inverse(multiply(X2,inverse(sF1))),multiply(X2,sF0)),inverse(inverse(multiply(inverse(X1),X1))))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))),
inference(superposition,[],[f13,f19]) ).
fof(f159,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X0,inverse(multiply(X1,X2)))),multiply(X0,inverse(X2))) = multiply(inverse(multiply(X3,inverse(multiply(X1,X2)))),multiply(X3,inverse(X2))),
inference(superposition,[],[f13,f13]) ).
fof(f162,plain,
! [X2,X0,X1] : inverse(X2) = multiply(multiply(inverse(X1),multiply(multiply(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X2),X2))))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2))))),inverse(X2))),inverse(multiply(inverse(X2),X2))),
inference(superposition,[],[f14,f13]) ).
fof(f167,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X0,inverse(multiply(multiply(X1,inverse(multiply(inverse(X2),X2))),X2)))),multiply(X0,inverse(X2))) = X1,
inference(superposition,[],[f1,f13]) ).
fof(f183,plain,
! [X0,X1] : multiply(inverse(multiply(X0,inverse(multiply(sF1,a2)))),multiply(X0,inverse(a2))) = multiply(inverse(multiply(X1,inverse(sF2))),multiply(X1,inverse(a2))),
inference(superposition,[],[f167,f12]) ).
fof(f187,plain,
! [X0,X1] : multiply(inverse(multiply(X0,inverse(multiply(multiply(X1,inverse(multiply(sF0,b2))),b2)))),multiply(X0,sF0)) = X1,
inference(superposition,[],[f167,f5]) ).
fof(f191,plain,
! [X0,X1] : multiply(inverse(multiply(multiply(inverse(multiply(X0,inverse(sF1))),multiply(X0,sF0)),inverse(multiply(multiply(X1,inverse(multiply(inverse(sF1),sF1))),sF1)))),sF0) = X1,
inference(superposition,[],[f167,f19]) ).
fof(f208,plain,
! [X0,X1] : multiply(inverse(multiply(X0,inverse(multiply(multiply(X1,inverse(sF1)),b2)))),multiply(X0,sF0)) = X1,
inference(forward_demodulation,[],[f187,f7]) ).
fof(f209,plain,
! [X0,X1] : multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2))) = multiply(inverse(multiply(X1,inverse(sF2))),multiply(X1,inverse(a2))),
inference(forward_demodulation,[],[f183,f9]) ).
fof(f231,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(X0,b2)))),multiply(X1,sF0)) = multiply(inverse(multiply(X2,inverse(multiply(X0,b2)))),multiply(X2,sF0)),
inference(superposition,[],[f208,f17]) ).
fof(f232,plain,
! [X0,X1] : multiply(inverse(multiply(X1,inverse(sF1))),multiply(X1,sF0)) = multiply(inverse(multiply(X0,inverse(multiply(sF0,b2)))),multiply(X0,sF0)),
inference(superposition,[],[f208,f19]) ).
fof(f245,plain,
! [X0,X1] : multiply(inverse(multiply(X0,inverse(sF1))),multiply(X0,sF0)) = multiply(inverse(multiply(X1,inverse(sF1))),multiply(X1,sF0)),
inference(forward_demodulation,[],[f232,f7]) ).
fof(f326,plain,
! [X3,X0,X1] : multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,inverse(inverse(sF1)))) = multiply(inverse(multiply(X3,inverse(X0))),multiply(X3,inverse(inverse(sF1)))),
inference(superposition,[],[f159,f17]) ).
fof(f338,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,inverse(multiply(X2,sF0)))) = multiply(inverse(multiply(X3,inverse(X0))),multiply(X3,inverse(multiply(X2,sF0)))),
inference(superposition,[],[f159,f208]) ).
fof(f738,plain,
! [X0,X1] : multiply(multiply(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(sF1)))),inverse(multiply(inverse(inverse(sF1)),inverse(sF1)))),inverse(sF1)) = X1,
inference(superposition,[],[f17,f27]) ).
fof(f2286,plain,
! [X2,X0,X1,X4] : multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X0))) = multiply(inverse(multiply(X4,inverse(X2))),multiply(X4,inverse(X0))),
inference(superposition,[],[f338,f191]) ).
fof(f2495,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X0,sF0)),multiply(X0,inverse(X1))) = multiply(inverse(multiply(X2,sF0)),multiply(X2,inverse(X1))),
inference(superposition,[],[f2286,f5]) ).
fof(f2800,plain,
! [X0,X1] : multiply(inverse(multiply(X1,sF0)),multiply(X1,sF0)) = multiply(inverse(multiply(X0,sF0)),multiply(X0,sF0)),
inference(superposition,[],[f2495,f5]) ).
fof(f3006,plain,
! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(multiply(X1,sF0)),multiply(X1,sF0)),
inference(superposition,[],[f2800,f191]) ).
fof(f3323,plain,
! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(X1),X1),
inference(superposition,[],[f3006,f3006]) ).
fof(f3566,plain,
! [X0] : multiply(sF0,b2) = multiply(inverse(X0),X0),
inference(superposition,[],[f3323,f5]) ).
fof(f4065,plain,
! [X0] : sF1 = multiply(inverse(X0),X0),
inference(forward_demodulation,[],[f3566,f7]) ).
fof(f4121,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2))),b2)))),multiply(X1,sF0)) = multiply(multiply(inverse(multiply(inverse(sF1),multiply(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2))),inverse(a2)))),multiply(multiply(inverse(multiply(X2,inverse(inverse(a2)))),multiply(X2,inverse(inverse(multiply(inverse(a2),a2))))),inverse(inverse(sF1)))),inverse(multiply(inverse(inverse(sF1)),inverse(sF1)))),
inference(superposition,[],[f27,f132]) ).
fof(f4124,plain,
! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2)))) = multiply(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2))))),multiply(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2))))),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(multiply(inverse(multiply(X2,inverse(inverse(a2)))),multiply(X2,inverse(inverse(multiply(inverse(a2),a2))))),inverse(multiply(X1,multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2))))))),multiply(inverse(sF1),multiply(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2))),inverse(a2)))),inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2)))))),inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2)))))),inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2)))))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2)))),multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2)))))),
inference(superposition,[],[f49,f132]) ).
fof(f4125,plain,
! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2)))) = multiply(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2))))),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(multiply(inverse(multiply(X2,inverse(inverse(a2)))),multiply(X2,inverse(inverse(multiply(inverse(a2),a2))))),inverse(multiply(X1,multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2))))))),multiply(inverse(sF1),multiply(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2))),inverse(a2)))),inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2)))))),inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2)))))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2)))),multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2)))))),
inference(superposition,[],[f57,f132]) ).
fof(f4130,plain,
! [X2,X0,X1] : inverse(X1) = multiply(multiply(inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2)))),multiply(multiply(multiply(inverse(multiply(inverse(sF1),multiply(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2))),inverse(a2)))),multiply(multiply(inverse(multiply(X2,inverse(inverse(a2)))),multiply(X2,inverse(inverse(multiply(inverse(a2),a2))))),inverse(inverse(multiply(inverse(X1),X1))))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))),inverse(X1))),inverse(multiply(inverse(X1),X1))),
inference(superposition,[],[f162,f132]) ).
fof(f4175,plain,
! [X2,X0,X1] : inverse(X1) = multiply(multiply(inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2)))),multiply(multiply(multiply(inverse(multiply(inverse(sF1),multiply(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2))),inverse(a2)))),multiply(multiply(inverse(multiply(X2,inverse(inverse(a2)))),multiply(X2,inverse(inverse(multiply(inverse(a2),a2))))),inverse(inverse(sF1)))),inverse(multiply(inverse(inverse(sF1)),inverse(sF1)))),inverse(X1))),inverse(sF1)),
inference(forward_demodulation,[],[f4130,f4065]) ).
fof(f4180,plain,
! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2)))) = multiply(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2))))),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(multiply(inverse(multiply(X2,inverse(inverse(a2)))),multiply(X2,inverse(inverse(multiply(inverse(a2),a2))))),inverse(multiply(X1,multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2))))))),multiply(inverse(sF1),multiply(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2))),inverse(a2)))),inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2)))))),inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2)))))),inverse(sF1)),
inference(forward_demodulation,[],[f4125,f4065]) ).
fof(f4181,plain,
! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2)))) = multiply(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2))))),multiply(multiply(inverse(inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2))))),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(multiply(inverse(multiply(X2,inverse(inverse(a2)))),multiply(X2,inverse(inverse(multiply(inverse(a2),a2))))),inverse(multiply(X1,multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2))))))),multiply(inverse(sF1),multiply(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2))),inverse(a2)))),inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2)))))),inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2)))))),inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2)))))),inverse(sF1)),
inference(forward_demodulation,[],[f4124,f4065]) ).
fof(f4184,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2))),b2)))),multiply(X1,sF0)) = multiply(multiply(inverse(multiply(inverse(sF1),multiply(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2))),inverse(a2)))),multiply(multiply(inverse(multiply(X2,inverse(inverse(a2)))),multiply(X2,inverse(inverse(multiply(inverse(a2),a2))))),inverse(inverse(sF1)))),inverse(sF1)),
inference(forward_demodulation,[],[f4121,f4065]) ).
fof(f4234,plain,
! [X2,X0,X1] : inverse(X1) = multiply(multiply(inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2)))),multiply(multiply(multiply(inverse(multiply(inverse(sF1),multiply(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2))),inverse(a2)))),multiply(multiply(inverse(multiply(X2,inverse(inverse(a2)))),multiply(X2,inverse(inverse(multiply(inverse(a2),a2))))),inverse(inverse(sF1)))),inverse(sF1)),inverse(X1))),inverse(sF1)),
inference(forward_demodulation,[],[f4175,f4065]) ).
fof(f4239,plain,
! [X2,X0,X1] : inverse(sF1) = multiply(multiply(inverse(inverse(sF1)),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(multiply(inverse(multiply(X2,inverse(inverse(a2)))),multiply(X2,inverse(inverse(multiply(inverse(a2),a2))))),inverse(multiply(X1,sF1)))),multiply(inverse(sF1),multiply(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2))),inverse(a2)))),inverse(sF1))),inverse(sF1))),inverse(sF1)),
inference(forward_demodulation,[],[f4180,f4065]) ).
fof(f4240,plain,
! [X2,X0,X1] : inverse(sF1) = multiply(multiply(inverse(inverse(sF1)),multiply(multiply(inverse(inverse(sF1)),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(multiply(inverse(multiply(X2,inverse(inverse(a2)))),multiply(X2,inverse(inverse(multiply(inverse(a2),a2))))),inverse(multiply(X1,sF1)))),multiply(inverse(sF1),multiply(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2))),inverse(a2)))),inverse(sF1))),inverse(sF1))),inverse(sF1))),inverse(sF1)),
inference(forward_demodulation,[],[f4181,f4065]) ).
fof(f4243,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(inverse(sF1)),inverse(sF1)),b2)))),multiply(X1,sF0)) = multiply(multiply(inverse(multiply(inverse(sF1),multiply(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2))),inverse(a2)))),multiply(multiply(inverse(multiply(X2,inverse(inverse(a2)))),multiply(X2,inverse(inverse(sF1)))),inverse(inverse(sF1)))),inverse(sF1)),
inference(forward_demodulation,[],[f4184,f4065]) ).
fof(f4279,plain,
! [X2,X0,X1] : inverse(X1) = multiply(multiply(inverse(multiply(inverse(inverse(sF1)),inverse(sF1))),multiply(multiply(multiply(inverse(multiply(inverse(sF1),multiply(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2))),inverse(a2)))),multiply(multiply(inverse(multiply(X2,inverse(inverse(a2)))),multiply(X2,inverse(inverse(sF1)))),inverse(inverse(sF1)))),inverse(sF1)),inverse(X1))),inverse(sF1)),
inference(forward_demodulation,[],[f4234,f4065]) ).
fof(f4282,plain,
! [X2,X0,X1] : inverse(sF1) = multiply(multiply(inverse(inverse(sF1)),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(multiply(inverse(multiply(X2,inverse(inverse(a2)))),multiply(X2,inverse(inverse(sF1)))),inverse(multiply(X1,sF1)))),multiply(inverse(sF1),multiply(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2))),inverse(a2)))),inverse(sF1))),inverse(sF1))),inverse(sF1)),
inference(forward_demodulation,[],[f4239,f4065]) ).
fof(f4283,plain,
! [X2,X0,X1] : inverse(sF1) = multiply(multiply(inverse(inverse(sF1)),multiply(multiply(inverse(inverse(sF1)),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(multiply(inverse(multiply(X2,inverse(inverse(a2)))),multiply(X2,inverse(inverse(sF1)))),inverse(multiply(X1,sF1)))),multiply(inverse(sF1),multiply(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2))),inverse(a2)))),inverse(sF1))),inverse(sF1))),inverse(sF1))),inverse(sF1)),
inference(forward_demodulation,[],[f4240,f4065]) ).
fof(f4286,plain,
! [X2,X0] : inverse(inverse(sF1)) = multiply(multiply(inverse(multiply(inverse(sF1),multiply(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2))),inverse(a2)))),multiply(multiply(inverse(multiply(X2,inverse(inverse(a2)))),multiply(X2,inverse(inverse(sF1)))),inverse(inverse(sF1)))),inverse(sF1)),
inference(forward_demodulation,[],[f4243,f208]) ).
fof(f4309,plain,
! [X2,X0,X1] : inverse(X1) = multiply(multiply(inverse(sF1),multiply(multiply(multiply(inverse(multiply(inverse(sF1),multiply(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2))),inverse(a2)))),multiply(multiply(inverse(multiply(X2,inverse(inverse(a2)))),multiply(X2,inverse(inverse(sF1)))),inverse(inverse(sF1)))),inverse(sF1)),inverse(X1))),inverse(sF1)),
inference(forward_demodulation,[],[f4279,f4065]) ).
fof(f4312,plain,
inverse(sF1) = multiply(multiply(inverse(inverse(sF1)),inverse(sF1)),inverse(sF1)),
inference(forward_demodulation,[],[f4283,f4282]) ).
fof(f4322,plain,
! [X1] : inverse(X1) = multiply(multiply(inverse(sF1),multiply(inverse(inverse(sF1)),inverse(X1))),inverse(sF1)),
inference(forward_demodulation,[],[f4309,f4286]) ).
fof(f4325,plain,
inverse(sF1) = multiply(sF1,inverse(sF1)),
inference(forward_demodulation,[],[f4312,f4065]) ).
fof(f4429,plain,
! [X0,X1] : multiply(inverse(multiply(X0,inverse(multiply(X1,b2)))),multiply(X0,sF0)) = multiply(multiply(inverse(sF1),multiply(inverse(inverse(X1)),inverse(inverse(sF1)))),inverse(multiply(inverse(inverse(sF1)),inverse(sF1)))),
inference(superposition,[],[f27,f4065]) ).
fof(f4449,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X2))) = multiply(inverse(multiply(inverse(inverse(X2)),inverse(X1))),sF1),
inference(superposition,[],[f2286,f4065]) ).
fof(f4450,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X2))) = multiply(inverse(sF1),multiply(inverse(inverse(X1)),inverse(X2))),
inference(superposition,[],[f2286,f4065]) ).
fof(f4454,plain,
! [X2,X0,X1] : multiply(multiply(inverse(multiply(X2,inverse(X0))),multiply(X2,inverse(inverse(multiply(inverse(X1),X1))))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))) = multiply(inverse(sF1),multiply(inverse(inverse(multiply(X0,X1))),inverse(X1))),
inference(superposition,[],[f13,f4065]) ).
fof(f4461,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X0,inverse(multiply(X1,X2)))),multiply(X0,inverse(X2))) = multiply(inverse(sF1),multiply(inverse(inverse(multiply(X1,X2))),inverse(X2))),
inference(superposition,[],[f159,f4065]) ).
fof(f4492,plain,
! [X0,X1] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(sF1)))) = multiply(inverse(multiply(inverse(inverse(inverse(sF1))),inverse(X1))),sF1),
inference(superposition,[],[f326,f4065]) ).
fof(f4521,plain,
! [X0] : multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2))) = multiply(multiply(inverse(sF1),multiply(inverse(inverse(sF1)),inverse(inverse(multiply(inverse(a2),a2))))),inverse(multiply(inverse(inverse(multiply(inverse(a2),a2))),inverse(multiply(inverse(a2),a2))))),
inference(superposition,[],[f31,f4065]) ).
fof(f4537,plain,
! [X0] : multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2))) = multiply(inverse(sF1),multiply(inverse(inverse(sF2)),inverse(a2))),
inference(superposition,[],[f209,f4065]) ).
fof(f4565,plain,
! [X0,X1] : multiply(inverse(multiply(X0,inverse(multiply(X1,b2)))),multiply(X0,sF0)) = multiply(inverse(multiply(inverse(sF0),inverse(multiply(X1,b2)))),sF1),
inference(superposition,[],[f231,f4065]) ).
fof(f4569,plain,
! [X0] : multiply(inverse(multiply(X0,inverse(sF1))),multiply(X0,sF0)) = multiply(inverse(multiply(inverse(sF0),inverse(sF1))),sF1),
inference(superposition,[],[f245,f4065]) ).
fof(f4623,plain,
! [X0] : multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2))) = multiply(multiply(inverse(sF1),multiply(inverse(inverse(sF1)),inverse(inverse(multiply(inverse(a2),a2))))),inverse(sF1)),
inference(forward_demodulation,[],[f4521,f4065]) ).
fof(f4670,plain,
! [X2,X0,X1] : multiply(inverse(sF1),multiply(inverse(inverse(multiply(X0,X1))),inverse(X1))) = multiply(multiply(inverse(multiply(X2,inverse(X0))),multiply(X2,inverse(inverse(multiply(inverse(X1),X1))))),inverse(sF1)),
inference(forward_demodulation,[],[f4454,f4065]) ).
fof(f4674,plain,
! [X2,X1] : multiply(inverse(multiply(inverse(inverse(X2)),inverse(X1))),sF1) = multiply(inverse(sF1),multiply(inverse(inverse(X1)),inverse(X2))),
inference(forward_demodulation,[],[f4449,f4450]) ).
fof(f4687,plain,
! [X0,X1] : multiply(inverse(multiply(X0,inverse(multiply(X1,b2)))),multiply(X0,sF0)) = multiply(multiply(inverse(sF1),multiply(inverse(inverse(X1)),inverse(inverse(sF1)))),inverse(sF1)),
inference(forward_demodulation,[],[f4429,f4065]) ).
fof(f4775,plain,
! [X0] : multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2))) = inverse(inverse(multiply(inverse(a2),a2))),
inference(forward_demodulation,[],[f4623,f4322]) ).
fof(f4801,plain,
! [X0,X1] : multiply(inverse(sF1),multiply(inverse(inverse(multiply(X0,X1))),inverse(X1))) = multiply(multiply(inverse(sF1),multiply(inverse(inverse(X0)),inverse(inverse(multiply(inverse(X1),X1))))),inverse(sF1)),
inference(forward_demodulation,[],[f4670,f4450]) ).
fof(f4810,plain,
! [X1] : multiply(inverse(multiply(inverse(sF0),inverse(multiply(X1,b2)))),sF1) = multiply(multiply(inverse(sF1),multiply(inverse(inverse(X1)),inverse(inverse(sF1)))),inverse(sF1)),
inference(forward_demodulation,[],[f4687,f4565]) ).
fof(f4868,plain,
! [X0] : multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2))) = inverse(inverse(sF1)),
inference(forward_demodulation,[],[f4775,f4065]) ).
fof(f4881,plain,
! [X0,X1] : multiply(inverse(sF1),multiply(inverse(inverse(multiply(X0,X1))),inverse(X1))) = multiply(multiply(inverse(sF1),multiply(inverse(inverse(X0)),inverse(inverse(sF1)))),inverse(sF1)),
inference(forward_demodulation,[],[f4801,f4065]) ).
fof(f4914,plain,
inverse(inverse(sF1)) = multiply(inverse(sF1),multiply(inverse(inverse(sF2)),inverse(a2))),
inference(forward_demodulation,[],[f4868,f4450]) ).
fof(f4918,plain,
! [X0,X1] : multiply(inverse(sF1),multiply(inverse(inverse(multiply(X0,X1))),inverse(X1))) = multiply(inverse(multiply(inverse(sF0),inverse(multiply(X0,b2)))),sF1),
inference(forward_demodulation,[],[f4881,f4810]) ).
fof(f4953,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(inverse(multiply(X4,inverse(X3))),multiply(X4,inverse(inverse(multiply(inverse(sF1),sF1))))),inverse(multiply(inverse(inverse(multiply(inverse(sF1),sF1))),inverse(multiply(inverse(sF1),sF1))))) = multiply(inverse(multiply(multiply(inverse(multiply(inverse(multiply(multiply(inverse(multiply(X2,inverse(sF1))),multiply(X2,sF0)),inverse(multiply(X1,sF1)))),inverse(sF1))),multiply(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(sF1),sF1))))),inverse(multiply(inverse(inverse(multiply(inverse(sF1),sF1))),inverse(multiply(inverse(sF1),sF1)))))),inverse(multiply(X3,sF1)))),sF0),
inference(superposition,[],[f138,f138]) ).
fof(f5019,plain,
! [X0] : multiply(inverse(multiply(multiply(inverse(multiply(X0,inverse(sF1))),multiply(X0,sF0)),inverse(multiply(inverse(multiply(inverse(sF1),sF1)),sF1)))),sF0) = multiply(sF1,inverse(multiply(inverse(inverse(multiply(inverse(sF1),sF1))),inverse(multiply(inverse(sF1),sF1))))),
inference(superposition,[],[f138,f4065]) ).
fof(f5026,plain,
! [X2,X0,X1] : multiply(inverse(multiply(multiply(inverse(multiply(X0,inverse(sF1))),multiply(X0,sF0)),inverse(multiply(X1,sF1)))),sF0) = multiply(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(inverse(multiply(inverse(sF1),sF1))))),inverse(sF1)),
inference(superposition,[],[f138,f4065]) ).
fof(f5064,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X2,inverse(sF1))),multiply(X2,sF0)) = multiply(inverse(multiply(inverse(multiply(multiply(inverse(multiply(X3,inverse(sF1))),multiply(X3,sF0)),inverse(multiply(X1,sF1)))),inverse(sF1))),multiply(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(sF1),sF1))))),inverse(multiply(inverse(inverse(multiply(inverse(sF1),sF1))),inverse(multiply(inverse(sF1),sF1)))))),
inference(superposition,[],[f245,f138]) ).
fof(f5191,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X2,inverse(sF1))),multiply(X2,sF0)) = multiply(inverse(multiply(inverse(multiply(multiply(inverse(multiply(X3,inverse(sF1))),multiply(X3,sF0)),inverse(multiply(X1,sF1)))),inverse(sF1))),multiply(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(sF1),sF1))))),inverse(sF1))),
inference(forward_demodulation,[],[f5064,f4065]) ).
fof(f5222,plain,
! [X0,X1] : multiply(inverse(multiply(multiply(inverse(multiply(X0,inverse(sF1))),multiply(X0,sF0)),inverse(multiply(X1,sF1)))),sF0) = multiply(multiply(inverse(sF1),multiply(inverse(inverse(X1)),inverse(inverse(multiply(inverse(sF1),sF1))))),inverse(sF1)),
inference(forward_demodulation,[],[f5026,f4450]) ).
fof(f5229,plain,
! [X0] : multiply(sF1,inverse(sF1)) = multiply(inverse(multiply(multiply(inverse(multiply(X0,inverse(sF1))),multiply(X0,sF0)),inverse(multiply(inverse(multiply(inverse(sF1),sF1)),sF1)))),sF0),
inference(forward_demodulation,[],[f5019,f4065]) ).
fof(f5282,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(inverse(multiply(X4,inverse(X3))),multiply(X4,inverse(inverse(multiply(inverse(sF1),sF1))))),inverse(sF1)) = multiply(inverse(multiply(multiply(inverse(multiply(inverse(multiply(multiply(inverse(multiply(X2,inverse(sF1))),multiply(X2,sF0)),inverse(multiply(X1,sF1)))),inverse(sF1))),multiply(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(sF1),sF1))))),inverse(sF1))),inverse(multiply(X3,sF1)))),sF0),
inference(forward_demodulation,[],[f4953,f4065]) ).
fof(f5345,plain,
! [X2,X3,X1] : multiply(inverse(multiply(X2,inverse(sF1))),multiply(X2,sF0)) = multiply(inverse(multiply(inverse(multiply(multiply(inverse(multiply(X3,inverse(sF1))),multiply(X3,sF0)),inverse(multiply(X1,sF1)))),inverse(sF1))),multiply(multiply(inverse(sF1),multiply(inverse(inverse(X1)),inverse(inverse(multiply(inverse(sF1),sF1))))),inverse(sF1))),
inference(forward_demodulation,[],[f5191,f4450]) ).
fof(f5376,plain,
! [X0,X1] : multiply(inverse(multiply(multiply(inverse(multiply(X0,inverse(sF1))),multiply(X0,sF0)),inverse(multiply(X1,sF1)))),sF0) = multiply(multiply(inverse(sF1),multiply(inverse(inverse(X1)),inverse(inverse(sF1)))),inverse(sF1)),
inference(forward_demodulation,[],[f5222,f4065]) ).
fof(f5383,plain,
! [X0] : multiply(inverse(multiply(multiply(inverse(multiply(X0,inverse(sF1))),multiply(X0,sF0)),inverse(multiply(inverse(sF1),sF1)))),sF0) = multiply(sF1,inverse(sF1)),
inference(forward_demodulation,[],[f5229,f4065]) ).
fof(f5433,plain,
! [X2,X3,X1,X4] : multiply(multiply(inverse(multiply(X4,inverse(X3))),multiply(X4,inverse(inverse(multiply(inverse(sF1),sF1))))),inverse(sF1)) = multiply(inverse(multiply(multiply(inverse(multiply(inverse(multiply(multiply(inverse(multiply(X2,inverse(sF1))),multiply(X2,sF0)),inverse(multiply(X1,sF1)))),inverse(sF1))),multiply(multiply(inverse(sF1),multiply(inverse(inverse(X1)),inverse(inverse(multiply(inverse(sF1),sF1))))),inverse(sF1))),inverse(multiply(X3,sF1)))),sF0),
inference(forward_demodulation,[],[f5282,f4450]) ).
fof(f5495,plain,
! [X2,X3,X1] : multiply(inverse(multiply(X2,inverse(sF1))),multiply(X2,sF0)) = multiply(inverse(multiply(inverse(multiply(multiply(inverse(multiply(X3,inverse(sF1))),multiply(X3,sF0)),inverse(multiply(X1,sF1)))),inverse(sF1))),multiply(multiply(inverse(sF1),multiply(inverse(inverse(X1)),inverse(inverse(sF1)))),inverse(sF1))),
inference(forward_demodulation,[],[f5345,f4065]) ).
fof(f5526,plain,
! [X0,X1] : multiply(inverse(multiply(multiply(inverse(multiply(X0,inverse(sF1))),multiply(X0,sF0)),inverse(multiply(X1,sF1)))),sF0) = multiply(inverse(multiply(inverse(sF0),inverse(multiply(X1,b2)))),sF1),
inference(forward_demodulation,[],[f5376,f4810]) ).
fof(f5533,plain,
! [X0] : inverse(sF1) = multiply(inverse(multiply(multiply(inverse(multiply(X0,inverse(sF1))),multiply(X0,sF0)),inverse(multiply(inverse(sF1),sF1)))),sF0),
inference(forward_demodulation,[],[f5383,f4325]) ).
fof(f5583,plain,
! [X2,X3,X1,X4] : multiply(multiply(inverse(multiply(X4,inverse(X3))),multiply(X4,inverse(inverse(sF1)))),inverse(sF1)) = multiply(inverse(multiply(multiply(inverse(multiply(inverse(multiply(multiply(inverse(multiply(X2,inverse(sF1))),multiply(X2,sF0)),inverse(multiply(X1,sF1)))),inverse(sF1))),multiply(multiply(inverse(sF1),multiply(inverse(inverse(X1)),inverse(inverse(sF1)))),inverse(sF1))),inverse(multiply(X3,sF1)))),sF0),
inference(forward_demodulation,[],[f5433,f4065]) ).
fof(f5645,plain,
! [X2,X3,X1] : multiply(inverse(multiply(X2,inverse(sF1))),multiply(X2,sF0)) = multiply(inverse(multiply(inverse(multiply(multiply(inverse(multiply(X3,inverse(sF1))),multiply(X3,sF0)),inverse(multiply(X1,sF1)))),inverse(sF1))),multiply(inverse(multiply(inverse(sF0),inverse(multiply(X1,b2)))),sF1)),
inference(forward_demodulation,[],[f5495,f4810]) ).
fof(f5676,plain,
! [X1] : multiply(inverse(multiply(inverse(sF0),inverse(multiply(X1,b2)))),sF1) = multiply(inverse(multiply(multiply(inverse(multiply(inverse(sF0),inverse(sF1))),sF1),inverse(multiply(X1,sF1)))),sF0),
inference(forward_demodulation,[],[f5526,f4569]) ).
fof(f5683,plain,
! [X0] : inverse(sF1) = multiply(inverse(multiply(multiply(inverse(multiply(X0,inverse(sF1))),multiply(X0,sF0)),inverse(sF1))),sF0),
inference(forward_demodulation,[],[f5533,f4065]) ).
fof(f5733,plain,
! [X2,X3,X1,X4] : multiply(multiply(inverse(multiply(X4,inverse(X3))),multiply(X4,inverse(inverse(sF1)))),inverse(sF1)) = multiply(inverse(multiply(multiply(inverse(multiply(inverse(multiply(multiply(inverse(multiply(X2,inverse(sF1))),multiply(X2,sF0)),inverse(multiply(X1,sF1)))),inverse(sF1))),multiply(inverse(multiply(inverse(sF0),inverse(multiply(X1,b2)))),sF1)),inverse(multiply(X3,sF1)))),sF0),
inference(forward_demodulation,[],[f5583,f4810]) ).
fof(f5795,plain,
! [X2,X1] : multiply(inverse(multiply(X2,inverse(sF1))),multiply(X2,sF0)) = multiply(inverse(multiply(inverse(multiply(multiply(inverse(multiply(inverse(sF0),inverse(sF1))),sF1),inverse(multiply(X1,sF1)))),inverse(sF1))),multiply(inverse(multiply(inverse(sF0),inverse(multiply(X1,b2)))),sF1)),
inference(forward_demodulation,[],[f5645,f4569]) ).
fof(f5832,plain,
inverse(sF1) = multiply(inverse(sF0),sF0),
inference(forward_demodulation,[],[f5683,f19]) ).
fof(f5881,plain,
! [X3,X1,X4] : multiply(multiply(inverse(multiply(X4,inverse(X3))),multiply(X4,inverse(inverse(sF1)))),inverse(sF1)) = multiply(inverse(multiply(multiply(inverse(multiply(inverse(multiply(multiply(inverse(multiply(inverse(sF0),inverse(sF1))),sF1),inverse(multiply(X1,sF1)))),inverse(sF1))),multiply(inverse(multiply(inverse(sF0),inverse(multiply(X1,b2)))),sF1)),inverse(multiply(X3,sF1)))),sF0),
inference(forward_demodulation,[],[f5733,f4569]) ).
fof(f5943,plain,
! [X1] : multiply(inverse(multiply(inverse(sF0),inverse(sF1))),sF1) = multiply(inverse(multiply(inverse(multiply(multiply(inverse(multiply(inverse(sF0),inverse(sF1))),sF1),inverse(multiply(X1,sF1)))),inverse(sF1))),multiply(inverse(multiply(inverse(sF0),inverse(multiply(X1,b2)))),sF1)),
inference(forward_demodulation,[],[f5795,f4569]) ).
fof(f5966,plain,
sF1 = inverse(sF1),
inference(forward_demodulation,[],[f5832,f4065]) ).
fof(f6006,plain,
! [X3,X1] : multiply(multiply(inverse(multiply(inverse(inverse(inverse(sF1))),inverse(X3))),sF1),inverse(sF1)) = multiply(inverse(multiply(multiply(inverse(multiply(inverse(multiply(multiply(inverse(multiply(inverse(sF0),inverse(sF1))),sF1),inverse(multiply(X1,sF1)))),inverse(sF1))),multiply(inverse(multiply(inverse(sF0),inverse(multiply(X1,b2)))),sF1)),inverse(multiply(X3,sF1)))),sF0),
inference(forward_demodulation,[],[f5881,f4492]) ).
fof(f6098,plain,
! [X3] : multiply(multiply(inverse(multiply(inverse(inverse(inverse(sF1))),inverse(X3))),sF1),inverse(sF1)) = multiply(inverse(multiply(multiply(inverse(multiply(inverse(sF0),inverse(sF1))),sF1),inverse(multiply(X3,sF1)))),sF0),
inference(forward_demodulation,[],[f6006,f5943]) ).
fof(f6157,plain,
! [X3] : multiply(inverse(multiply(inverse(sF0),inverse(multiply(X3,b2)))),sF1) = multiply(multiply(inverse(multiply(inverse(inverse(inverse(sF1))),inverse(X3))),sF1),inverse(sF1)),
inference(forward_demodulation,[],[f6098,f5676]) ).
fof(f6193,plain,
! [X3] : multiply(inverse(multiply(inverse(sF0),inverse(multiply(X3,b2)))),sF1) = multiply(multiply(inverse(multiply(inverse(inverse(sF1)),inverse(X3))),sF1),sF1),
inference(forward_demodulation,[],[f6157,f5966]) ).
fof(f6209,plain,
! [X3] : multiply(inverse(multiply(inverse(sF0),inverse(multiply(X3,b2)))),sF1) = multiply(multiply(inverse(sF1),multiply(inverse(inverse(X3)),inverse(sF1))),sF1),
inference(forward_demodulation,[],[f6193,f4674]) ).
fof(f6216,plain,
! [X3] : multiply(inverse(multiply(inverse(sF0),inverse(multiply(X3,b2)))),sF1) = multiply(multiply(sF1,multiply(inverse(inverse(X3)),sF1)),sF1),
inference(forward_demodulation,[],[f6209,f5966]) ).
fof(f6223,plain,
! [X0,X1] : multiply(multiply(inverse(multiply(X0,inverse(multiply(X1,b2)))),multiply(X0,sF0)),sF1) = X1,
inference(superposition,[],[f17,f5966]) ).
fof(f6224,plain,
! [X0] : sF0 = multiply(multiply(inverse(multiply(X0,sF1)),multiply(X0,sF0)),sF1),
inference(superposition,[],[f19,f5966]) ).
fof(f6292,plain,
sF1 = multiply(sF1,sF1),
inference(superposition,[],[f4065,f5966]) ).
fof(f6346,plain,
! [X1] : multiply(multiply(inverse(multiply(inverse(sF0),inverse(multiply(X1,b2)))),sF1),sF1) = X1,
inference(forward_demodulation,[],[f6223,f4565]) ).
fof(f6397,plain,
! [X1] : multiply(multiply(multiply(sF1,multiply(inverse(inverse(X1)),sF1)),sF1),sF1) = X1,
inference(forward_demodulation,[],[f6346,f6216]) ).
fof(f6551,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(sF0),multiply(multiply(inverse(multiply(X3,inverse(sF1))),multiply(X3,sF0)),inverse(inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))))),inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))),inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))))) = multiply(inverse(multiply(multiply(inverse(inverse(X0)),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X0)))),multiply(X2,inverse(X0))),inverse(X0))),inverse(X0))),inverse(multiply(sF1,multiply(inverse(X0),X0))))),inverse(X0)),
inference(superposition,[],[f150,f57]) ).
fof(f6828,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(sF0),multiply(multiply(inverse(multiply(X3,inverse(sF1))),multiply(X3,sF0)),inverse(inverse(multiply(inverse(sF1),sF1))))),inverse(multiply(inverse(inverse(multiply(inverse(sF1),sF1))),inverse(multiply(inverse(sF1),sF1))))) = multiply(inverse(multiply(multiply(inverse(inverse(X0)),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X0)))),multiply(X2,inverse(X0))),inverse(X0))),inverse(X0))),inverse(multiply(sF1,sF1)))),inverse(X0)),
inference(forward_demodulation,[],[f6551,f4065]) ).
fof(f6969,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(sF0),multiply(multiply(inverse(multiply(X3,inverse(sF1))),multiply(X3,sF0)),inverse(inverse(multiply(inverse(sF1),sF1))))),inverse(multiply(inverse(inverse(multiply(inverse(sF1),sF1))),inverse(multiply(inverse(sF1),sF1))))) = multiply(inverse(multiply(multiply(inverse(inverse(X0)),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X0)))),multiply(X2,inverse(X0))),inverse(X0))),inverse(X0))),inverse(sF1))),inverse(X0)),
inference(forward_demodulation,[],[f6828,f6292]) ).
fof(f7110,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(sF0),multiply(multiply(inverse(multiply(X3,sF1)),multiply(X3,sF0)),inverse(inverse(multiply(sF1,sF1))))),inverse(multiply(inverse(inverse(multiply(sF1,sF1))),inverse(multiply(sF1,sF1))))) = multiply(inverse(multiply(multiply(inverse(inverse(X0)),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X0)))),multiply(X2,inverse(X0))),inverse(X0))),inverse(X0))),sF1)),inverse(X0)),
inference(forward_demodulation,[],[f6969,f5966]) ).
fof(f7251,plain,
! [X3,X0,X1] : multiply(multiply(inverse(sF0),multiply(multiply(inverse(multiply(X3,sF1)),multiply(X3,sF0)),inverse(inverse(multiply(sF1,sF1))))),inverse(multiply(inverse(inverse(multiply(sF1,sF1))),inverse(multiply(sF1,sF1))))) = multiply(inverse(multiply(multiply(inverse(inverse(X0)),multiply(multiply(inverse(X1),multiply(multiply(inverse(sF1),multiply(inverse(inverse(multiply(X1,X0))),inverse(X0))),inverse(X0))),inverse(X0))),sF1)),inverse(X0)),
inference(forward_demodulation,[],[f7110,f4461]) ).
fof(f7392,plain,
! [X3,X0,X1] : multiply(multiply(inverse(sF0),multiply(multiply(inverse(multiply(X3,sF1)),multiply(X3,sF0)),inverse(inverse(multiply(sF1,sF1))))),inverse(multiply(inverse(inverse(multiply(sF1,sF1))),inverse(multiply(sF1,sF1))))) = multiply(inverse(multiply(multiply(inverse(inverse(X0)),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(inverse(sF0),inverse(multiply(X1,b2)))),sF1),inverse(X0))),inverse(X0))),sF1)),inverse(X0)),
inference(forward_demodulation,[],[f7251,f4918]) ).
fof(f7533,plain,
! [X3,X0,X1] : multiply(multiply(inverse(sF0),multiply(multiply(inverse(multiply(X3,sF1)),multiply(X3,sF0)),inverse(inverse(multiply(sF1,sF1))))),inverse(multiply(inverse(inverse(multiply(sF1,sF1))),inverse(multiply(sF1,sF1))))) = multiply(inverse(multiply(multiply(inverse(inverse(X0)),multiply(multiply(inverse(X1),multiply(multiply(multiply(sF1,multiply(inverse(inverse(X1)),sF1)),sF1),inverse(X0))),inverse(X0))),sF1)),inverse(X0)),
inference(forward_demodulation,[],[f7392,f6216]) ).
fof(f7673,plain,
! [X3,X0,X1] : multiply(inverse(multiply(multiply(inverse(inverse(X0)),multiply(multiply(inverse(X1),multiply(multiply(multiply(sF1,multiply(inverse(inverse(X1)),sF1)),sF1),inverse(X0))),inverse(X0))),sF1)),inverse(X0)) = multiply(multiply(inverse(sF0),multiply(multiply(inverse(multiply(X3,sF1)),multiply(X3,sF0)),inverse(inverse(multiply(sF1,sF1))))),inverse(sF1)),
inference(forward_demodulation,[],[f7533,f4065]) ).
fof(f7808,plain,
! [X3,X0,X1] : multiply(multiply(inverse(sF0),multiply(multiply(inverse(multiply(X3,sF1)),multiply(X3,sF0)),inverse(inverse(multiply(sF1,sF1))))),sF1) = multiply(inverse(multiply(multiply(inverse(inverse(X0)),multiply(multiply(inverse(X1),multiply(multiply(multiply(sF1,multiply(inverse(inverse(X1)),sF1)),sF1),inverse(X0))),inverse(X0))),sF1)),inverse(X0)),
inference(forward_demodulation,[],[f7673,f5966]) ).
fof(f7942,plain,
! [X3,X0,X1] : multiply(multiply(inverse(sF0),multiply(multiply(inverse(multiply(X3,sF1)),multiply(X3,sF0)),inverse(inverse(sF1)))),sF1) = multiply(inverse(multiply(multiply(inverse(inverse(X0)),multiply(multiply(inverse(X1),multiply(multiply(multiply(sF1,multiply(inverse(inverse(X1)),sF1)),sF1),inverse(X0))),inverse(X0))),sF1)),inverse(X0)),
inference(forward_demodulation,[],[f7808,f6292]) ).
fof(f8067,plain,
! [X3,X0,X1] : multiply(multiply(inverse(sF0),multiply(multiply(inverse(multiply(X3,sF1)),multiply(X3,sF0)),inverse(sF1))),sF1) = multiply(inverse(multiply(multiply(inverse(inverse(X0)),multiply(multiply(inverse(X1),multiply(multiply(multiply(sF1,multiply(inverse(inverse(X1)),sF1)),sF1),inverse(X0))),inverse(X0))),sF1)),inverse(X0)),
inference(forward_demodulation,[],[f7942,f5966]) ).
fof(f8186,plain,
! [X3,X0,X1] : multiply(multiply(inverse(sF0),multiply(multiply(inverse(multiply(X3,sF1)),multiply(X3,sF0)),sF1)),sF1) = multiply(inverse(multiply(multiply(inverse(inverse(X0)),multiply(multiply(inverse(X1),multiply(multiply(multiply(sF1,multiply(inverse(inverse(X1)),sF1)),sF1),inverse(X0))),inverse(X0))),sF1)),inverse(X0)),
inference(forward_demodulation,[],[f8067,f5966]) ).
fof(f8296,plain,
! [X0,X1] : multiply(multiply(inverse(sF0),sF0),sF1) = multiply(inverse(multiply(multiply(inverse(inverse(X0)),multiply(multiply(inverse(X1),multiply(multiply(multiply(sF1,multiply(inverse(inverse(X1)),sF1)),sF1),inverse(X0))),inverse(X0))),sF1)),inverse(X0)),
inference(forward_demodulation,[],[f8186,f6224]) ).
fof(f8391,plain,
! [X0,X1] : multiply(sF1,sF1) = multiply(inverse(multiply(multiply(inverse(inverse(X0)),multiply(multiply(inverse(X1),multiply(multiply(multiply(sF1,multiply(inverse(inverse(X1)),sF1)),sF1),inverse(X0))),inverse(X0))),sF1)),inverse(X0)),
inference(forward_demodulation,[],[f8296,f4065]) ).
fof(f8466,plain,
! [X0,X1] : sF1 = multiply(inverse(multiply(multiply(inverse(inverse(X0)),multiply(multiply(inverse(X1),multiply(multiply(multiply(sF1,multiply(inverse(inverse(X1)),sF1)),sF1),inverse(X0))),inverse(X0))),sF1)),inverse(X0)),
inference(forward_demodulation,[],[f8391,f6292]) ).
fof(f29032,plain,
! [X2,X0,X1] : inverse(multiply(inverse(inverse(a2)),inverse(sF2))) = multiply(multiply(inverse(multiply(multiply(inverse(inverse(inverse(a2))),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(a2))))),multiply(X2,inverse(inverse(a2)))),inverse(inverse(a2)))),inverse(inverse(a2)))),inverse(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2)))))),inverse(inverse(a2))),inverse(multiply(inverse(multiply(inverse(inverse(a2)),inverse(a2))),multiply(inverse(inverse(a2)),inverse(a2))))),
inference(superposition,[],[f89,f209]) ).
fof(f29235,plain,
! [X2,X0,X1] : inverse(multiply(inverse(inverse(a2)),inverse(sF2))) = multiply(multiply(inverse(multiply(multiply(inverse(inverse(inverse(a2))),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(a2))))),multiply(X2,inverse(inverse(a2)))),inverse(inverse(a2)))),inverse(inverse(a2)))),inverse(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2)))))),inverse(inverse(a2))),inverse(multiply(inverse(sF1),multiply(inverse(inverse(a2)),inverse(a2))))),
inference(forward_demodulation,[],[f29032,f4450]) ).
fof(f29540,plain,
! [X2,X0,X1] : inverse(multiply(inverse(inverse(a2)),inverse(sF2))) = multiply(multiply(inverse(multiply(multiply(inverse(inverse(inverse(a2))),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(a2))))),multiply(X2,inverse(inverse(a2)))),inverse(inverse(a2)))),inverse(inverse(a2)))),inverse(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2)))))),inverse(inverse(a2))),inverse(multiply(inverse(sF1),sF1))),
inference(forward_demodulation,[],[f29235,f4065]) ).
fof(f29845,plain,
! [X2,X0,X1] : inverse(multiply(inverse(inverse(a2)),inverse(sF2))) = multiply(multiply(inverse(multiply(multiply(inverse(inverse(inverse(a2))),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(a2))))),multiply(X2,inverse(inverse(a2)))),inverse(inverse(a2)))),inverse(inverse(a2)))),inverse(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2)))))),inverse(inverse(a2))),inverse(sF1)),
inference(forward_demodulation,[],[f29540,f4065]) ).
fof(f30150,plain,
! [X2,X0,X1] : inverse(multiply(inverse(inverse(a2)),inverse(sF2))) = multiply(multiply(inverse(multiply(multiply(inverse(inverse(inverse(a2))),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(a2))))),multiply(X2,inverse(inverse(a2)))),inverse(inverse(a2)))),inverse(inverse(a2)))),inverse(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(a2)))))),inverse(inverse(a2))),sF1),
inference(forward_demodulation,[],[f29845,f5966]) ).
fof(f30455,plain,
! [X2,X1] : inverse(multiply(inverse(inverse(a2)),inverse(sF2))) = multiply(multiply(inverse(multiply(multiply(inverse(inverse(inverse(a2))),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(a2))))),multiply(X2,inverse(inverse(a2)))),inverse(inverse(a2)))),inverse(inverse(a2)))),inverse(multiply(inverse(sF1),multiply(inverse(inverse(sF2)),inverse(a2)))))),inverse(inverse(a2))),sF1),
inference(forward_demodulation,[],[f30150,f4537]) ).
fof(f30759,plain,
! [X2,X1] : inverse(multiply(inverse(inverse(a2)),inverse(sF2))) = multiply(multiply(inverse(multiply(multiply(inverse(inverse(inverse(a2))),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(a2))))),multiply(X2,inverse(inverse(a2)))),inverse(inverse(a2)))),inverse(inverse(a2)))),inverse(inverse(inverse(sF1))))),inverse(inverse(a2))),sF1),
inference(forward_demodulation,[],[f30455,f4914]) ).
fof(f31061,plain,
! [X2,X1] : inverse(multiply(inverse(inverse(a2)),inverse(sF2))) = multiply(multiply(inverse(multiply(multiply(inverse(inverse(inverse(a2))),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(a2))))),multiply(X2,inverse(inverse(a2)))),inverse(inverse(a2)))),inverse(inverse(a2)))),inverse(inverse(sF1)))),inverse(inverse(a2))),sF1),
inference(forward_demodulation,[],[f30759,f5966]) ).
fof(f31358,plain,
! [X2,X1] : inverse(multiply(inverse(inverse(a2)),inverse(sF2))) = multiply(multiply(inverse(multiply(multiply(inverse(inverse(inverse(a2))),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(a2))))),multiply(X2,inverse(inverse(a2)))),inverse(inverse(a2)))),inverse(inverse(a2)))),inverse(sF1))),inverse(inverse(a2))),sF1),
inference(forward_demodulation,[],[f31061,f5966]) ).
fof(f31632,plain,
! [X2,X1] : inverse(multiply(inverse(inverse(a2)),inverse(sF2))) = multiply(multiply(inverse(multiply(multiply(inverse(inverse(inverse(a2))),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(a2))))),multiply(X2,inverse(inverse(a2)))),inverse(inverse(a2)))),inverse(inverse(a2)))),sF1)),inverse(inverse(a2))),sF1),
inference(forward_demodulation,[],[f31358,f5966]) ).
fof(f31884,plain,
! [X1] : inverse(multiply(inverse(inverse(a2)),inverse(sF2))) = multiply(multiply(inverse(multiply(multiply(inverse(inverse(inverse(a2))),multiply(multiply(inverse(X1),multiply(multiply(inverse(sF1),multiply(inverse(inverse(multiply(X1,inverse(a2)))),inverse(inverse(a2)))),inverse(inverse(a2)))),inverse(inverse(a2)))),sF1)),inverse(inverse(a2))),sF1),
inference(forward_demodulation,[],[f31632,f4461]) ).
fof(f32107,plain,
! [X1] : inverse(multiply(inverse(inverse(a2)),inverse(sF2))) = multiply(multiply(inverse(multiply(multiply(inverse(inverse(inverse(a2))),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(inverse(sF0),inverse(multiply(X1,b2)))),sF1),inverse(inverse(a2)))),inverse(inverse(a2)))),sF1)),inverse(inverse(a2))),sF1),
inference(forward_demodulation,[],[f31884,f4918]) ).
fof(f32303,plain,
! [X1] : inverse(multiply(inverse(inverse(a2)),inverse(sF2))) = multiply(multiply(inverse(multiply(multiply(inverse(inverse(inverse(a2))),multiply(multiply(inverse(X1),multiply(multiply(multiply(sF1,multiply(inverse(inverse(X1)),sF1)),sF1),inverse(inverse(a2)))),inverse(inverse(a2)))),sF1)),inverse(inverse(a2))),sF1),
inference(forward_demodulation,[],[f32107,f6216]) ).
fof(f32474,plain,
inverse(multiply(inverse(inverse(a2)),inverse(sF2))) = multiply(sF1,sF1),
inference(forward_demodulation,[],[f32303,f8466]) ).
fof(f32621,plain,
sF1 = inverse(multiply(inverse(inverse(a2)),inverse(sF2))),
inference(forward_demodulation,[],[f32474,f6292]) ).
fof(f33100,plain,
sF2 = multiply(multiply(multiply(sF1,multiply(inverse(inverse(a2)),inverse(inverse(sF1)))),inverse(multiply(inverse(inverse(sF1)),inverse(sF1)))),inverse(sF1)),
inference(superposition,[],[f738,f32621]) ).
fof(f33222,plain,
sF2 = multiply(multiply(multiply(sF1,multiply(inverse(inverse(a2)),inverse(sF1))),inverse(multiply(inverse(sF1),sF1))),sF1),
inference(forward_demodulation,[],[f33100,f5966]) ).
fof(f33294,plain,
sF2 = multiply(multiply(multiply(sF1,multiply(inverse(inverse(a2)),inverse(sF1))),inverse(sF1)),sF1),
inference(forward_demodulation,[],[f33222,f4065]) ).
fof(f33364,plain,
sF2 = multiply(multiply(multiply(sF1,multiply(inverse(inverse(a2)),sF1)),sF1),sF1),
inference(forward_demodulation,[],[f33294,f5966]) ).
fof(f33428,plain,
a2 = sF2,
inference(forward_demodulation,[],[f33364,f6397]) ).
fof(f33479,plain,
$false,
inference(forward_subsumption_resolution,[],[f33428,f10]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP410-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.39 % Computer : n019.cluster.edu
% 0.11/0.39 % Model : x86_64 x86_64
% 0.11/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.39 % Memory : 8046.5625MB
% 0.11/0.39 % OS : Linux 6.8.0-71-generic
% 0.11/0.39 % CPULimit : 300
% 0.11/0.39 % WCLimit : 300
% 0.11/0.39 % DateTime : Sun Sep 27 10:03:40 UTC 2026
% 0.11/0.39 % CPUTime :
% 0.11/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.42 Running first-order model finding
% 0.11/0.42 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
% 15.38/2.65 % (2851587)Will run a generic schedule for satisfiability detection.
% 15.38/2.65 % (2851596)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1210423333:i=116_3000 on theBenchmark for (3000ds/116Mi)
% 15.38/2.65 % (2851593)% WARNING: option uhcvi not known.
% 15.38/2.65 % (2851593)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2960347569:i=135531:add=off:rawr=on_3000 on theBenchmark for (3000ds/135531Mi)
% 15.38/2.65 % (2851592)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=4061096684_3000 on theBenchmark for (3000ds/0Mi)
% 15.38/2.65 % (2851594)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2957817225:i=88024:add=on:rawr=on_3000 on theBenchmark for (3000ds/88024Mi)
% 15.38/2.65 % (2851595)dis+10_1_sil=32000:sp=arity:random_seed=335748364:i=103:fgj=on_3000 on theBenchmark for (3000ds/103Mi)
% 15.38/2.65 % (2851598)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3466980095:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_3000 on theBenchmark for (3000ds/159Mi)
% 15.38/2.65 % (2851597)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=98635728:i=131_3000 on theBenchmark for (3000ds/131Mi)
% 15.38/2.65 % TRYING [1]
% 15.38/2.65 % TRYING [2]
% 15.38/2.65 % TRYING [3]
% 15.38/2.65 % (2851596)Instruction limit reached!
% 15.38/2.65 % (2851596)------------------------------
% 15.38/2.65 % (2851596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.38/2.65 % (2851596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.38/2.65 % (2851596)CaDiCaL version: 2.1.3
% 15.38/2.65 % (2851596)Termination reason: Instruction limit
% 15.38/2.65 % (2851596)Termination phase: Saturation
% 15.38/2.65 % (2851596)Time elapsed: 0.035 s
% 15.38/2.65 % (2851596)Peak memory usage: 12 MB
% 15.38/2.65 % (2851596)Instructions burned: 117 (million)
% 15.38/2.65 % (2851606)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1544368098:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 15.38/2.65 % TRYING [1]
% 15.38/2.65 % TRYING [2]
% 15.38/2.65 % TRYING [3]
% 15.38/2.65 % TRYING [4]
% 15.38/2.65 % (2851595)Instruction limit reached!
% 15.38/2.65 % (2851595)------------------------------
% 15.38/2.65 % (2851595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.38/2.65 % (2851595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.38/2.65 % (2851595)CaDiCaL version: 2.1.3
% 15.38/2.65 % (2851595)Termination reason: Instruction limit
% 15.38/2.65 % (2851595)Termination phase: Saturation
% 15.38/2.65 % (2851595)Time elapsed: 0.054 s
% 15.38/2.65 % (2851595)Peak memory usage: 11 MB
% 15.38/2.65 % (2851595)Instructions burned: 104 (million)
% 15.38/2.65 % TRYING [4]
% 15.38/2.65 % (2851608)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2578724232:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 15.38/2.65 % (2851597)Instruction limit reached!
% 15.38/2.65 % (2851597)------------------------------
% 15.38/2.65 % (2851597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.38/2.65 % (2851597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.38/2.65 % (2851597)CaDiCaL version: 2.1.3
% 15.38/2.65 % (2851597)Termination reason: Instruction limit
% 15.38/2.65 % (2851597)Termination phase: Saturation
% 15.38/2.65 % (2851597)Time elapsed: 0.073 s
% 15.38/2.65 % (2851597)Peak memory usage: 12 MB
% 15.38/2.65 % (2851597)Instructions burned: 131 (million)
% 15.38/2.65 % (2851598)Instruction limit reached!
% 15.38/2.65 % (2851598)------------------------------
% 15.38/2.65 % (2851598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.38/2.65 % (2851598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.38/2.65 % (2851598)CaDiCaL version: 2.1.3
% 15.38/2.65 % (2851598)Termination reason: Instruction limit
% 15.38/2.65 % (2851598)Termination phase: Saturation
% 15.38/2.65 % (2851598)Time elapsed: 0.091 s
% 15.38/2.65 % (2851598)Peak memory usage: 12 MB
% 15.38/2.65 % (2851598)Instructions burned: 159 (million)
% 15.38/2.65 % (2851613)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=3791791770:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 15.38/2.65 % (2851616)ott-21_1_sil=16000:fs=off:random_seed=2122903991:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 15.38/2.65 % (2851608)Instruction limit reached!
% 15.38/2.65 % (2851608)------------------------------
% 15.38/2.65 % (2851608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.38/2.65 % (2851608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/3.97 % (2851608)CaDiCaL version: 2.1.3
% 13.62/3.97 % (2851608)Termination reason: Instruction limit
% 13.62/3.97 % (2851608)Termination phase: Saturation
% 13.62/3.97 % (2851608)Time elapsed: 0.074 s
% 13.62/3.97 % (2851608)Peak memory usage: 12 MB
% 13.62/3.97 % (2851608)Instructions burned: 132 (million)
% 13.62/3.97 % (2851646)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2149839122:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 13.62/3.97 % (2851616)Instruction limit reached!
% 13.62/3.97 % (2851616)------------------------------
% 13.62/3.97 % (2851616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.62/3.97 % (2851616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/3.97 % (2851616)CaDiCaL version: 2.1.3
% 13.62/3.97 % (2851616)Termination reason: Instruction limit
% 13.62/3.97 % (2851616)Termination phase: Saturation
% 13.62/3.97 % (2851616)Time elapsed: 0.090 s
% 13.62/3.97 % (2851616)Peak memory usage: 12 MB
% 13.62/3.97 % (2851616)Instructions burned: 182 (million)
% 13.62/3.97 % (2851663)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3367419062:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 13.62/3.97 % TRYING [1]
% 13.62/3.97 % TRYING [2]
% 13.62/3.97 % TRYING [3]
% 13.62/3.97 % TRYING [4]
% 13.62/3.97 % (2851606)Instruction limit reached!
% 13.62/3.97 % (2851606)------------------------------
% 13.62/3.97 % (2851606)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.62/3.97 % (2851606)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/3.97 % (2851606)CaDiCaL version: 2.1.3
% 13.62/3.97 % (2851606)Termination reason: Instruction limit
% 13.62/3.97 % (2851606)Termination phase: Finite model building SAT solving
% 13.62/3.97 % (2851606)Time elapsed: 0.227 s
% 13.62/3.97 % (2851606)Peak memory usage: 12 MB
% 13.62/3.97 % (2851606)Instructions burned: 714 (million)
% 13.62/3.97 % (2851665)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3405108382:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 13.62/3.97 % (2851646)Instruction limit reached!
% 13.62/3.97 % (2851646)------------------------------
% 13.62/3.97 % (2851646)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.62/3.97 % (2851646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/3.97 % (2851646)CaDiCaL version: 2.1.3
% 13.62/3.97 % (2851646)Termination reason: Instruction limit
% 13.62/3.97 % (2851646)Termination phase: Saturation
% 13.62/3.97 % (2851646)Time elapsed: 0.239 s
% 13.62/3.97 % (2851646)Peak memory usage: 14 MB
% 13.62/3.97 % (2851646)Instructions burned: 478 (million)
% 13.62/3.97 % (2851667)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2735337696:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 13.62/3.97 % (2851613)Instruction limit reached!
% 13.62/3.97 % (2851613)------------------------------
% 13.62/3.97 % (2851613)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.62/3.97 % (2851613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/3.97 % (2851613)CaDiCaL version: 2.1.3
% 13.62/3.97 % (2851613)Termination reason: Instruction limit
% 13.62/3.97 % (2851613)Termination phase: Saturation
% 13.62/3.97 % (2851613)Time elapsed: 0.347 s
% 13.62/3.97 % (2851613)Peak memory usage: 16 MB
% 13.62/3.97 % (2851613)Instructions burned: 685 (million)
% 13.62/3.97 % TRYING [14]
% 13.62/3.97 % (2851669)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=251418021:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 13.62/3.97 % (2851665)Instruction limit reached!
% 13.62/3.97 % (2851665)------------------------------
% 13.62/3.97 % (2851665)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.62/3.97 % (2851665)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/3.97 % (2851665)CaDiCaL version: 2.1.3
% 13.62/3.97 % (2851665)Termination reason: Instruction limit
% 13.62/3.97 % (2851665)Termination phase: Saturation
% 13.62/3.97 % (2851665)Time elapsed: 0.324 s
% 13.62/3.97 % (2851665)Peak memory usage: 24 MB
% 13.62/3.97 % (2851665)Instructions burned: 1179 (million)
% 13.62/3.97 % (2851671)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=484131203:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 13.62/3.97 % (2851667)Instruction limit reached!
% 13.62/3.97 % (2851667)------------------------------
% 13.62/3.97 % (2851667)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.62/3.97 % (2851667)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/3.97 % (2851667)CaDiCaL version: 2.1.3
% 13.62/3.97 % (2851667)Termination reason: Instruction limit
% 13.62/3.97 % (2851667)Termination phase: Finite model building constraint generation
% 13.62/3.97 % (2851667)Time elapsed: 0.317 s
% 13.62/3.97 % (2851667)Peak memory usage: 80 MB
% 13.62/3.97 % (2851667)Instructions burned: 890 (million)
% 13.62/3.97 % (2851673)fmb+10_1_sil=64000:random_seed=1100844190:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 13.62/3.97 % (2851663)Instruction limit reached!
% 13.62/3.97 % (2851663)------------------------------
% 13.62/3.97 % (2851663)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.62/3.97 % (2851663)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/3.97 % TRYING [1]
% 13.62/3.97 % (2851663)CaDiCaL version: 2.1.3
% 13.62/3.97 % (2851663)Termination reason: Instruction limit
% 13.62/3.97 % (2851663)Termination phase: Finite model building SAT solving
% 13.62/3.97 % (2851663)Time elapsed: 0.550 s
% 13.62/3.97 % (2851663)Peak memory usage: 11 MB
% 13.62/3.97 % (2851663)Instructions burned: 865 (million)
% 13.62/3.97 % TRYING [2]
% 13.62/3.97 % TRYING [3]
% 13.62/3.97 % (2851675)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=165356466:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi)
% 13.62/3.97 % TRYING [20]
% 13.62/3.97 % TRYING [4]
% 13.62/3.97 % (2851669)Instruction limit reached!
% 13.62/3.97 % (2851669)------------------------------
% 13.62/3.97 % (2851669)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.62/3.97 % (2851669)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/3.97 % (2851669)CaDiCaL version: 2.1.3
% 13.62/3.97 % (2851669)Termination reason: Instruction limit
% 13.62/3.97 % (2851669)Termination phase: Saturation
% 13.62/3.97 % (2851669)Time elapsed: 0.377 s
% 13.62/3.97 % (2851669)Peak memory usage: 17 MB
% 13.62/3.97 % (2851669)Instructions burned: 692 (million)
% 13.62/3.97 % (2851671)Instruction limit reached!
% 13.62/3.97 % (2851671)------------------------------
% 13.62/3.97 % (2851671)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.62/3.97 % (2851671)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/3.97 % (2851671)CaDiCaL version: 2.1.3
% 13.62/3.97 % (2851671)Termination reason: Instruction limit
% 13.62/3.97 % (2851671)Termination phase: Saturation
% 13.62/3.97 % (2851671)Time elapsed: 0.228 s
% 13.62/3.97 % (2851671)Peak memory usage: 15 MB
% 13.62/3.97 % (2851671)Instructions burned: 879 (million)
% 13.62/3.97 % (2851678)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3070638148:i=5131_2991 on theBenchmark for (2991ds/5131Mi)
% 13.62/3.97 % (2851677)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3884602039:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi)
% 13.62/3.97 % TRYING [8]
% 13.62/3.97 % (2851677)Instruction limit reached!
% 13.62/3.97 % (2851677)------------------------------
% 13.62/3.97 % (2851677)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.62/3.97 % (2851677)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/3.97 % (2851677)CaDiCaL version: 2.1.3
% 13.62/3.97 % (2851677)Termination reason: Instruction limit
% 13.62/3.97 % (2851677)Termination phase: Finite model building SAT solving
% 13.62/3.97 % (2851677)Time elapsed: 0.485 s
% 13.62/3.97 % (2851677)Peak memory usage: 37 MB
% 13.62/3.97 % (2851677)Instructions burned: 921 (million)
% 13.62/3.97 % (2851681)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=711250465:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 13.62/3.97 % (2851681)Instruction limit reached!
% 13.62/3.97 % (2851681)------------------------------
% 13.62/3.97 % (2851681)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.62/3.97 % (2851681)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/3.97 % (2851681)CaDiCaL version: 2.1.3
% 13.62/3.97 % (2851681)Termination reason: Instruction limit
% 13.62/3.97 % (2851681)Termination phase: Saturation
% 13.62/3.97 % (2851681)Time elapsed: 0.705 s
% 13.62/3.97 % (2851681)Peak memory usage: 27 MB
% 13.62/3.97 % (2851681)Instructions burned: 1474 (million)
% 13.62/3.97 % (2851683)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=2143417207:i=6324_2979 on theBenchmark for (2979ds/6324Mi)
% 13.62/3.97 % TRYING [77]
% 13.62/3.97 % (2851678)Instruction limit reached!
% 13.62/3.97 % (2851678)------------------------------
% 13.62/3.97 % (2851678)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.62/3.97 % (2851678)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/3.97 % (2851678)CaDiCaL version: 2.1.3
% 13.62/3.97 % (2851678)Termination reason: Instruction limit
% 13.62/3.97 % (2851678)Termination phase: Saturation
% 13.62/3.97 % (2851678)Time elapsed: 1.352 s
% 13.62/3.97 % (2851678)Peak memory usage: 35 MB
% 13.62/3.97 % (2851678)Instructions burned: 5134 (million)
% 13.62/3.97 % (2851685)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=4290447251:fmbsr=2.30978:i=2174_2977 on theBenchmark for (2977ds/2174Mi)
% 13.62/3.97 % TRYING [16]
% 13.62/3.97 % TRYING [5]
% 13.62/3.97 % (2851685)Instruction limit reached!
% 13.62/3.97 % (2851685)------------------------------
% 13.62/3.97 % (2851685)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.62/3.97 % (2851685)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/3.97 % (2851685)CaDiCaL version: 2.1.3
% 13.62/3.97 % (2851685)Termination reason: Instruction limit
% 13.62/3.97 % (2851685)Termination phase: Finite model building constraint generation
% 13.62/3.97 % (2851685)Time elapsed: 0.395 s
% 13.62/3.97 % (2851685)Peak memory usage: 132 MB
% 13.62/3.97 % (2851685)Instructions burned: 2174 (million)
% 13.62/3.97 % (2851687)ott-2_1_sil=16000:newcnf=on:random_seed=3408344545:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2973 on theBenchmark for (2973ds/869Mi)
% 13.62/3.97 % (2851687)Instruction limit reached!
% 13.62/3.97 % (2851687)------------------------------
% 13.62/3.97 % (2851687)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.62/3.97 % (2851687)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/3.97 % (2851687)CaDiCaL version: 2.1.3
% 13.62/3.97 % (2851687)Termination reason: Instruction limit
% 13.62/3.97 % (2851687)Termination phase: Saturation
% 13.62/3.97 % (2851687)Time elapsed: 0.276 s
% 13.62/3.97 % (2851687)Peak memory usage: 21 MB
% 13.62/3.97 % (2851687)Instructions burned: 872 (million)
% 13.62/3.97 % (2851689)ott+10_1_sil=32000:tgt=ground:random_seed=1622688839:i=5114:av=off_2970 on theBenchmark for (2970ds/5114Mi)
% 13.62/3.97 % (2851689) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2851587-2851689"...
% 13.62/3.97 % (2851689)...printing done.
% 13.62/3.97 % (2851689)Refutation found. Thanks to Tanya!
% 13.62/3.97 % SZS status Unsatisfiable for theBenchmark
% 13.62/3.97 % SZS output start Proof for theBenchmark
% See solution above
% 13.62/3.97 % (2851689)------------------------------
% 13.62/3.97 % (2851689)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 13.62/3.97 % (2851689)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.62/3.97 % (2851689)CaDiCaL version: 2.1.3
% 13.62/3.97 % (2851689)Termination reason: Refutation
% 13.62/3.97 % (2851689)Time elapsed: 0.518 s
% 13.62/3.97 % (2851689)Peak memory usage: 28 MB
% 13.62/3.97 % (2851689)Instructions burned: 1892 (million)
% 13.62/3.97 % (2851587)Success in time 3.537 s
% 13.62/3.97 % Vampire exiting
%------------------------------------------------------------------------------