%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : GRP411-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:13:56 AM UTC 2026
% Result : Unsatisfiable 9.93s 2.25s
% Output : Refutation 10.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 49
% Number of leaves : 6
% Syntax : Number of formulae : 191 ( 191 unt; 4 def)
% Number of atoms : 191 ( 190 equ)
% Maximal formula atoms : 1 ( 1 avg)
% Number of connectives : 2 ( 2 ~; 0 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 6 ( 4 avg)
% Maximal term depth : 16 ( 3 avg)
% Number of predicates : 2 ( 0 usr; 1 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 482 ( 482 !; 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/sandbox/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_these_axioms_3) ).
fof(f3,definition,
sF0 = multiply(a3,b3),
introduced(definition,[new_symbols(definition,[sF0])],[function_definition]) ).
fof(f4,plain,
multiply(a3,b3) = sF0,
inference(reorient_equations,[],[f3]) ).
fof(f5,definition,
sF1 = multiply(sF0,c3),
introduced(definition,[new_symbols(definition,[sF1])],[function_definition]) ).
fof(f6,plain,
multiply(sF0,c3) = sF1,
inference(reorient_equations,[],[f5]) ).
fof(f7,definition,
sF2 = multiply(b3,c3),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
fof(f8,plain,
multiply(b3,c3) = sF2,
inference(reorient_equations,[],[f7]) ).
fof(f9,definition,
sF3 = multiply(a3,sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f10,plain,
multiply(a3,sF2) = sF3,
inference(reorient_equations,[],[f9]) ).
fof(f11,plain,
sF1 != sF3,
inference(definition_folding,[],[f2,f10,f8,f6,f4]) ).
fof(f12,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(f13,plain,
! [X0] : a3 = multiply(multiply(inverse(multiply(X0,inverse(sF0))),multiply(X0,inverse(b3))),inverse(multiply(inverse(b3),b3))),
inference(superposition,[],[f1,f4]) ).
fof(f14,plain,
! [X0] : a3 = multiply(multiply(inverse(multiply(X0,inverse(sF3))),multiply(X0,inverse(sF2))),inverse(multiply(inverse(sF2),sF2))),
inference(superposition,[],[f1,f10]) ).
fof(f15,plain,
! [X0] : b3 = multiply(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(c3))),inverse(multiply(inverse(c3),c3))),
inference(superposition,[],[f1,f8]) ).
fof(f16,plain,
! [X0] : sF0 = multiply(multiply(inverse(multiply(X0,inverse(sF1))),multiply(X0,inverse(c3))),inverse(multiply(inverse(c3),c3))),
inference(superposition,[],[f1,f6]) ).
fof(f17,plain,
! [X2,X0,X1] : inverse(X0) = multiply(multiply(inverse(X2),multiply(multiply(inverse(multiply(X1,inverse(multiply(X2,X0)))),multiply(X1,inverse(X0))),inverse(X0))),inverse(multiply(inverse(X0),X0))),
inference(superposition,[],[f1,f1]) ).
fof(f18,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(multiply(inverse(multiply(X1,inverse(multiply(X2,X0)))),multiply(X1,inverse(X0))),inverse(multiply(X3,multiply(inverse(X0),X0))))),X2),inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))) = X3,
inference(superposition,[],[f1,f1]) ).
fof(f24,plain,
! [X0,X1] : multiply(inverse(multiply(X1,inverse(sF3))),multiply(X1,inverse(sF2))) = multiply(multiply(inverse(multiply(X0,inverse(a3))),multiply(X0,inverse(inverse(multiply(inverse(sF2),sF2))))),inverse(multiply(inverse(inverse(multiply(inverse(sF2),sF2))),inverse(multiply(inverse(sF2),sF2))))),
inference(superposition,[],[f1,f14]) ).
fof(f27,plain,
! [X0,X1] : multiply(inverse(multiply(X1,inverse(sF2))),multiply(X1,inverse(c3))) = multiply(multiply(inverse(multiply(X0,inverse(b3))),multiply(X0,inverse(inverse(multiply(inverse(c3),c3))))),inverse(multiply(inverse(inverse(multiply(inverse(c3),c3))),inverse(multiply(inverse(c3),c3))))),
inference(superposition,[],[f1,f15]) ).
fof(f29,plain,
! [X0,X1] : multiply(multiply(inverse(multiply(multiply(inverse(multiply(X0,inverse(sF1))),multiply(X0,inverse(c3))),inverse(multiply(X1,multiply(inverse(c3),c3))))),sF0),inverse(multiply(inverse(multiply(inverse(c3),c3)),multiply(inverse(c3),c3)))) = X1,
inference(superposition,[],[f1,f16]) ).
fof(f200,plain,
! [X2,X0,X1] : multiply(multiply(inverse(multiply(multiply(inverse(multiply(X2,inverse(b3))),multiply(X2,inverse(inverse(multiply(inverse(c3),c3))))),inverse(multiply(X0,multiply(inverse(inverse(multiply(inverse(c3),c3))),inverse(multiply(inverse(c3),c3))))))),multiply(inverse(multiply(X1,inverse(sF2))),multiply(X1,inverse(c3)))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(c3),c3))),inverse(multiply(inverse(c3),c3)))),multiply(inverse(inverse(multiply(inverse(c3),c3))),inverse(multiply(inverse(c3),c3)))))) = X0,
inference(superposition,[],[f18,f15]) ).
fof(f406,plain,
! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(c3),c3))),inverse(multiply(inverse(c3),c3)))) = multiply(multiply(inverse(X0),multiply(multiply(inverse(multiply(multiply(inverse(multiply(X1,inverse(b3))),multiply(X1,inverse(inverse(multiply(inverse(c3),c3))))),inverse(multiply(X0,multiply(inverse(inverse(multiply(inverse(c3),c3))),inverse(multiply(inverse(c3),c3))))))),multiply(inverse(multiply(X2,inverse(sF2))),multiply(X2,inverse(c3)))),inverse(multiply(inverse(inverse(multiply(inverse(c3),c3))),inverse(multiply(inverse(c3),c3)))))),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(c3),c3))),inverse(multiply(inverse(c3),c3)))),multiply(inverse(inverse(multiply(inverse(c3),c3))),inverse(multiply(inverse(c3),c3)))))),
inference(superposition,[],[f17,f27]) ).
fof(f487,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(X2,inverse(inverse(multiply(X0,inverse(sF3)))))),multiply(X2,inverse(inverse(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(sF2))))))),inverse(multiply(inverse(inverse(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(sF2))))),inverse(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(sF2))))))) = multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(X3,inverse(a3))),multiply(X3,inverse(inverse(multiply(inverse(sF2),sF2))))),inverse(multiply(inverse(inverse(multiply(inverse(sF2),sF2))),inverse(multiply(inverse(sF2),sF2)))))))),multiply(X1,inverse(multiply(X0,inverse(sF2))))),
inference(superposition,[],[f12,f24]) ).
fof(f575,plain,
! [X2,X0,X1,X4] : multiply(inverse(multiply(X2,inverse(multiply(X0,X1)))),multiply(X2,inverse(X1))) = multiply(inverse(multiply(X4,inverse(multiply(X0,X1)))),multiply(X4,inverse(X1))),
inference(superposition,[],[f12,f12]) ).
fof(f580,plain,
! [X3,X0,X1] : multiply(multiply(multiply(inverse(multiply(X3,inverse(X0))),multiply(X3,inverse(inverse(multiply(inverse(X1),X1))))),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))),inverse(multiply(inverse(X1),X1))) = X0,
inference(superposition,[],[f1,f12]) ).
fof(f585,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X2,inverse(multiply(multiply(X0,inverse(multiply(inverse(X1),X1))),X1)))),multiply(X2,inverse(X1))) = X0,
inference(superposition,[],[f1,f12]) ).
fof(f629,plain,
! [X2,X3,X0,X1] : inverse(multiply(multiply(inverse(multiply(X2,inverse(multiply(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))))),X0)))),multiply(X2,inverse(X0))),inverse(multiply(X1,multiply(inverse(X0),X0))))) = multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))))),
inference(superposition,[],[f585,f18]) ).
fof(f665,plain,
! [X2,X3,X0,X1] : inverse(multiply(X0,inverse(multiply(multiply(X1,inverse(multiply(inverse(X2),X2))),X2)))) = multiply(multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(multiply(X0,inverse(X2))))),inverse(multiply(inverse(multiply(X0,inverse(X2))),multiply(X0,inverse(X2))))),
inference(superposition,[],[f1,f585]) ).
fof(f798,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(multiply(X0,inverse(X2))))) = multiply(inverse(multiply(X4,inverse(X1))),multiply(X4,inverse(multiply(X0,inverse(X2))))),
inference(superposition,[],[f575,f585]) ).
fof(f980,plain,
! [X2,X3,X0,X4] : multiply(inverse(multiply(X3,inverse(X4))),multiply(X3,inverse(X2))) = multiply(inverse(multiply(X0,inverse(X4))),multiply(X0,inverse(X2))),
inference(superposition,[],[f798,f29]) ).
fof(f1120,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(inverse(b3),b3)))),multiply(X1,inverse(X2))) = multiply(inverse(a3),multiply(multiply(inverse(multiply(X0,inverse(sF0))),multiply(X0,inverse(b3))),inverse(X2))),
inference(superposition,[],[f980,f13]) ).
fof(f1289,plain,
! [X2,X3,X0,X1,X4] : inverse(multiply(X1,inverse(X0))) = multiply(multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(X2,inverse(X0))),multiply(X2,inverse(X3)))))),multiply(X4,inverse(multiply(X1,inverse(X3))))),inverse(multiply(inverse(multiply(X1,inverse(X3))),multiply(X1,inverse(X3))))),
inference(superposition,[],[f1,f980]) ).
fof(f1290,plain,
! [X2,X3,X0,X1] : inverse(multiply(X1,inverse(X0))) = inverse(multiply(X1,inverse(multiply(multiply(multiply(inverse(multiply(X2,inverse(X0))),multiply(X2,inverse(X3))),inverse(multiply(inverse(X3),X3))),X3)))),
inference(forward_demodulation,[],[f1289,f665]) ).
fof(f1304,plain,
! [X2,X0,X1] : inverse(multiply(X2,inverse(multiply(inverse(c3),c3)))) = inverse(multiply(X2,inverse(multiply(multiply(multiply(inverse(b3),multiply(multiply(inverse(multiply(X1,inverse(sF2))),multiply(X1,inverse(c3))),inverse(X0))),inverse(multiply(inverse(X0),X0))),X0)))),
inference(superposition,[],[f1290,f15]) ).
fof(f1918,plain,
! [X1] : multiply(inverse(multiply(X1,inverse(multiply(inverse(b3),b3)))),multiply(X1,inverse(multiply(inverse(b3),b3)))) = multiply(inverse(a3),a3),
inference(superposition,[],[f1120,f13]) ).
fof(f1969,plain,
! [X1] : multiply(inverse(X1),X1) = multiply(inverse(a3),a3),
inference(superposition,[],[f1918,f1]) ).
fof(f1995,plain,
! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(X1),X1),
inference(superposition,[],[f1969,f1969]) ).
fof(f2005,plain,
! [X2,X1] : inverse(multiply(X2,inverse(X1))) = inverse(multiply(X2,inverse(multiply(multiply(multiply(inverse(a3),a3),inverse(multiply(inverse(X1),X1))),X1)))),
inference(superposition,[],[f1290,f1969]) ).
fof(f2012,plain,
! [X2,X1] : multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(inverse(X1),X1)),X1)))),multiply(X2,inverse(X1))) = multiply(multiply(inverse(a3),a3),inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X1),X1))))),
inference(superposition,[],[f12,f1969]) ).
fof(f2042,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(X0))) = multiply(inverse(multiply(inverse(inverse(X0)),inverse(X1))),multiply(inverse(a3),a3)),
inference(superposition,[],[f980,f1969]) ).
fof(f2045,plain,
! [X0,X1] : multiply(inverse(a3),multiply(multiply(inverse(multiply(X1,inverse(sF0))),multiply(X1,inverse(b3))),inverse(X0))) = multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(b3),b3)))),multiply(inverse(a3),a3)),
inference(superposition,[],[f1120,f1969]) ).
fof(f2047,plain,
! [X2,X0,X1] : inverse(multiply(X2,inverse(X0))) = inverse(multiply(X2,inverse(multiply(multiply(multiply(inverse(multiply(inverse(a3),a3)),multiply(inverse(inverse(X0)),inverse(X1))),inverse(multiply(inverse(X1),X1))),X1)))),
inference(superposition,[],[f1290,f1969]) ).
fof(f2055,plain,
! [X0,X1] : inverse(inverse(multiply(inverse(X0),X0))) = multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(a3),a3),X0)))),multiply(X1,inverse(X0))),
inference(superposition,[],[f585,f1969]) ).
fof(f2056,plain,
! [X0,X1] : multiply(inverse(a3),multiply(multiply(inverse(multiply(X1,inverse(sF0))),multiply(X1,inverse(b3))),inverse(X0))) = multiply(inverse(multiply(inverse(a3),a3)),multiply(inverse(inverse(multiply(inverse(b3),b3))),inverse(X0))),
inference(superposition,[],[f1120,f1969]) ).
fof(f2333,plain,
! [X0] : multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(b3),b3)))),multiply(inverse(a3),a3)) = multiply(inverse(multiply(inverse(a3),a3)),multiply(inverse(inverse(multiply(inverse(b3),b3))),inverse(X0))),
inference(forward_demodulation,[],[f2045,f2056]) ).
fof(f2336,plain,
! [X2,X1] : multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(inverse(X1),X1)),X1)))),multiply(X2,inverse(X1))) = multiply(multiply(inverse(a3),a3),inverse(multiply(inverse(a3),a3))),
inference(forward_demodulation,[],[f2012,f1969]) ).
fof(f2651,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(X2,inverse(multiply(X3,X1)))),multiply(X2,inverse(X1))),inverse(multiply(inverse(X0),X0))) = X3,
inference(superposition,[],[f1,f1995]) ).
fof(f2654,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X2,inverse(multiply(multiply(X3,inverse(multiply(inverse(X0),X0))),X1)))),multiply(X2,inverse(X1))) = X3,
inference(superposition,[],[f585,f1995]) ).
fof(f2665,plain,
! [X0,X1] : a3 = multiply(multiply(inverse(multiply(X1,inverse(sF0))),multiply(X1,inverse(b3))),inverse(multiply(inverse(X0),X0))),
inference(superposition,[],[f13,f1995]) ).
fof(f2668,plain,
! [X0,X1] : b3 = multiply(multiply(inverse(multiply(X1,inverse(sF2))),multiply(X1,inverse(c3))),inverse(multiply(inverse(X0),X0))),
inference(superposition,[],[f15,f1995]) ).
fof(f2751,plain,
! [X2,X0] : multiply(inverse(a3),a3) = multiply(inverse(multiply(X2,inverse(multiply(inverse(b3),b3)))),multiply(X2,inverse(multiply(inverse(X0),X0)))),
inference(superposition,[],[f1120,f2665]) ).
fof(f2773,plain,
! [X0,X1] : b3 = multiply(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(inverse(sF2)),inverse(c3))),inverse(multiply(inverse(X1),X1))),
inference(superposition,[],[f2668,f1995]) ).
fof(f2793,plain,
! [X2,X0,X1] : multiply(inverse(b3),multiply(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(c3))),inverse(X1))) = multiply(inverse(a3),multiply(multiply(inverse(multiply(X2,inverse(sF0))),multiply(X2,inverse(b3))),inverse(X1))),
inference(superposition,[],[f1120,f2668]) ).
fof(f2808,plain,
! [X0,X1] : multiply(inverse(b3),multiply(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(c3))),inverse(X1))) = multiply(inverse(multiply(inverse(a3),a3)),multiply(inverse(inverse(multiply(inverse(b3),b3))),inverse(X1))),
inference(forward_demodulation,[],[f2793,f2056]) ).
fof(f2809,plain,
! [X2,X0] : inverse(multiply(X2,inverse(multiply(inverse(c3),c3)))) = inverse(multiply(X2,inverse(multiply(multiply(multiply(inverse(multiply(inverse(a3),a3)),multiply(inverse(inverse(multiply(inverse(b3),b3))),inverse(X0))),inverse(multiply(inverse(X0),X0))),X0)))),
inference(backward_demodulation,[],[f1304,f2808]) ).
fof(f2816,plain,
! [X2] : inverse(multiply(X2,inverse(multiply(inverse(b3),b3)))) = inverse(multiply(X2,inverse(multiply(inverse(c3),c3)))),
inference(forward_demodulation,[],[f2809,f2047]) ).
fof(f2854,plain,
! [X0] : multiply(inverse(multiply(inverse(a3),a3)),multiply(inverse(inverse(multiply(inverse(b3),b3))),inverse(X0))) = multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(c3),c3)))),multiply(inverse(a3),a3)),
inference(backward_demodulation,[],[f2333,f2816]) ).
fof(f2871,plain,
! [X2,X0] : multiply(inverse(a3),a3) = multiply(inverse(multiply(X2,inverse(multiply(inverse(c3),c3)))),multiply(X2,inverse(multiply(inverse(X0),X0)))),
inference(backward_demodulation,[],[f2751,f2816]) ).
fof(f2886,plain,
! [X2,X0,X1] : multiply(multiply(inverse(multiply(multiply(inverse(multiply(X2,inverse(b3))),multiply(X2,inverse(inverse(multiply(inverse(c3),c3))))),inverse(multiply(X0,multiply(inverse(inverse(multiply(inverse(c3),c3))),inverse(multiply(inverse(c3),c3))))))),multiply(inverse(multiply(X1,inverse(sF2))),multiply(X1,inverse(c3)))),inverse(multiply(inverse(a3),a3))) = X0,
inference(backward_demodulation,[],[f200,f2871]) ).
fof(f2890,plain,
! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(c3),c3))),inverse(multiply(inverse(c3),c3)))) = multiply(multiply(inverse(X0),multiply(multiply(inverse(multiply(multiply(inverse(multiply(X1,inverse(b3))),multiply(X1,inverse(inverse(multiply(inverse(c3),c3))))),inverse(multiply(X0,multiply(inverse(inverse(multiply(inverse(c3),c3))),inverse(multiply(inverse(c3),c3))))))),multiply(inverse(multiply(X2,inverse(sF2))),multiply(X2,inverse(c3)))),inverse(multiply(inverse(inverse(multiply(inverse(c3),c3))),inverse(multiply(inverse(c3),c3)))))),inverse(multiply(inverse(a3),a3))),
inference(backward_demodulation,[],[f406,f2871]) ).
fof(f2967,plain,
! [X2,X0,X1] : inverse(multiply(inverse(a3),a3)) = multiply(multiply(inverse(X0),multiply(multiply(inverse(multiply(multiply(inverse(multiply(X1,inverse(b3))),multiply(X1,inverse(inverse(multiply(inverse(c3),c3))))),inverse(multiply(X0,multiply(inverse(a3),a3))))),multiply(inverse(multiply(X2,inverse(sF2))),multiply(X2,inverse(c3)))),inverse(multiply(inverse(a3),a3)))),inverse(multiply(inverse(a3),a3))),
inference(forward_demodulation,[],[f2890,f1969]) ).
fof(f2971,plain,
! [X2,X0,X1] : multiply(multiply(inverse(multiply(multiply(inverse(multiply(X2,inverse(b3))),multiply(X2,inverse(inverse(multiply(inverse(c3),c3))))),inverse(multiply(X0,multiply(inverse(a3),a3))))),multiply(inverse(multiply(X1,inverse(sF2))),multiply(X1,inverse(c3)))),inverse(multiply(inverse(a3),a3))) = X0,
inference(forward_demodulation,[],[f2886,f1969]) ).
fof(f2989,plain,
! [X0] : inverse(multiply(inverse(a3),a3)) = multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(a3),a3))),
inference(backward_demodulation,[],[f2967,f2971]) ).
fof(f2997,plain,
! [X2,X1] : inverse(multiply(inverse(a3),a3)) = multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(inverse(X1),X1)),X1)))),multiply(X2,inverse(X1))),
inference(backward_demodulation,[],[f2336,f2989]) ).
fof(f3014,plain,
! [X0,X1] : inverse(multiply(inverse(X0),X0)) = multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(X0),X0))),
inference(superposition,[],[f2989,f1995]) ).
fof(f3029,plain,
! [X2,X1] : inverse(multiply(X2,inverse(X1))) = inverse(multiply(X2,inverse(multiply(inverse(multiply(inverse(X1),X1)),X1)))),
inference(backward_demodulation,[],[f2005,f3014]) ).
fof(f3030,plain,
! [X2,X1] : multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(X1))) = inverse(multiply(inverse(a3),a3)),
inference(backward_demodulation,[],[f2997,f3029]) ).
fof(f3031,plain,
multiply(inverse(a3),a3) = inverse(multiply(inverse(a3),a3)),
inference(forward_demodulation,[],[f3030,f1969]) ).
fof(f3120,plain,
! [X0] : multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(c3),c3)))),multiply(inverse(a3),a3)) = multiply(multiply(inverse(a3),a3),multiply(inverse(inverse(multiply(inverse(b3),b3))),inverse(X0))),
inference(backward_demodulation,[],[f2854,f3031]) ).
fof(f3265,plain,
! [X0] : multiply(inverse(X0),X0) = inverse(multiply(inverse(X0),X0)),
inference(superposition,[],[f3031,f1995]) ).
fof(f3283,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(multiply(inverse(multiply(X1,inverse(multiply(X2,X0)))),multiply(X1,inverse(X0))),inverse(multiply(X3,multiply(inverse(X0),X0))))),X2),inverse(multiply(multiply(inverse(X0),X0),multiply(inverse(X0),X0)))) = X3,
inference(backward_demodulation,[],[f18,f3265]) ).
fof(f3349,plain,
! [X3,X0,X1] : multiply(multiply(multiply(inverse(multiply(X3,inverse(X0))),multiply(X3,inverse(multiply(inverse(X1),X1)))),inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1)))),multiply(inverse(X1),X1)) = X0,
inference(backward_demodulation,[],[f580,f3265]) ).
fof(f3365,plain,
! [X2,X3,X0,X1] : inverse(multiply(multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(inverse(inverse(multiply(multiply(inverse(X0),X0),multiply(inverse(X0),X0)))),inverse(multiply(multiply(inverse(X0),X0),multiply(inverse(X0),X0))))),X0)))),multiply(X2,inverse(X0))),inverse(multiply(X1,multiply(inverse(X0),X0))))) = multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(inverse(multiply(multiply(inverse(X0),X0),multiply(inverse(X0),X0)))))),
inference(backward_demodulation,[],[f629,f3265]) ).
fof(f3431,plain,
! [X0,X1] : inverse(multiply(inverse(X0),X0)) = multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(a3),a3),X0)))),multiply(X1,inverse(X0))),
inference(backward_demodulation,[],[f2055,f3265]) ).
fof(f3434,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(X2,inverse(multiply(X3,X1)))),multiply(X2,inverse(X1))),multiply(inverse(X0),X0)) = X3,
inference(backward_demodulation,[],[f2651,f3265]) ).
fof(f3437,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X2,inverse(multiply(multiply(X3,multiply(inverse(X0),X0)),X1)))),multiply(X2,inverse(X1))) = X3,
inference(backward_demodulation,[],[f2654,f3265]) ).
fof(f3451,plain,
! [X0,X1] : b3 = multiply(multiply(multiply(inverse(X0),X0),multiply(inverse(inverse(sF2)),inverse(c3))),inverse(multiply(inverse(X1),X1))),
inference(backward_demodulation,[],[f2773,f3265]) ).
fof(f3456,plain,
! [X2,X0] : multiply(inverse(a3),a3) = multiply(inverse(multiply(X2,inverse(multiply(inverse(c3),c3)))),multiply(X2,multiply(inverse(X0),X0))),
inference(backward_demodulation,[],[f2871,f3265]) ).
fof(f3457,plain,
! [X0,X1] : multiply(inverse(X0),X0) = multiply(multiply(inverse(X1),X1),multiply(inverse(X0),X0)),
inference(backward_demodulation,[],[f3014,f3265]) ).
fof(f3458,plain,
! [X2,X1] : inverse(multiply(X2,inverse(X1))) = inverse(multiply(X2,inverse(multiply(multiply(inverse(X1),X1),X1)))),
inference(backward_demodulation,[],[f3029,f3265]) ).
fof(f3660,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(X3,inverse(a3))),multiply(X3,inverse(inverse(multiply(inverse(sF2),sF2))))),inverse(multiply(inverse(inverse(multiply(inverse(sF2),sF2))),inverse(multiply(inverse(sF2),sF2)))))))),multiply(X1,inverse(multiply(X0,inverse(sF2))))) = multiply(multiply(inverse(multiply(X2,inverse(inverse(multiply(X0,inverse(sF3)))))),multiply(X2,inverse(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(sF2)))))),inverse(multiply(inverse(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(sF2)))),multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(sF2)))))),
inference(backward_demodulation,[],[f487,f3265]) ).
fof(f3737,plain,
! [X2] : inverse(multiply(X2,multiply(inverse(b3),b3))) = inverse(multiply(X2,inverse(multiply(inverse(c3),c3)))),
inference(backward_demodulation,[],[f2816,f3265]) ).
fof(f3754,plain,
! [X0] : multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(c3),c3)))),multiply(inverse(a3),a3)) = multiply(multiply(inverse(a3),a3),multiply(inverse(multiply(inverse(b3),b3)),inverse(X0))),
inference(backward_demodulation,[],[f3120,f3265]) ).
fof(f4005,plain,
! [X0] : multiply(inverse(multiply(inverse(inverse(X0)),inverse(multiply(inverse(c3),c3)))),multiply(inverse(a3),a3)) = multiply(multiply(inverse(a3),a3),multiply(multiply(inverse(b3),b3),inverse(X0))),
inference(forward_demodulation,[],[f3754,f3265]) ).
fof(f4019,plain,
! [X2] : inverse(multiply(X2,multiply(inverse(b3),b3))) = inverse(multiply(X2,multiply(inverse(c3),c3))),
inference(forward_demodulation,[],[f3737,f3265]) ).
fof(f4088,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(X3,inverse(a3))),multiply(X3,inverse(inverse(multiply(inverse(sF2),sF2))))),inverse(multiply(inverse(inverse(multiply(inverse(sF2),sF2))),inverse(multiply(inverse(sF2),sF2)))))))),multiply(X1,inverse(multiply(X0,inverse(sF2))))) = multiply(multiply(inverse(multiply(X2,inverse(inverse(multiply(X0,inverse(sF3)))))),multiply(X2,inverse(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(sF2)))))),multiply(inverse(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(sF2)))),multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(sF2))))),
inference(forward_demodulation,[],[f3660,f3265]) ).
fof(f4272,plain,
! [X2,X0] : multiply(inverse(a3),a3) = multiply(inverse(multiply(X2,multiply(inverse(c3),c3))),multiply(X2,multiply(inverse(X0),X0))),
inference(forward_demodulation,[],[f3456,f3265]) ).
fof(f4274,plain,
! [X0,X1] : b3 = multiply(multiply(multiply(inverse(X0),X0),multiply(inverse(inverse(sF2)),inverse(c3))),multiply(inverse(X1),X1)),
inference(forward_demodulation,[],[f3451,f3265]) ).
fof(f4276,plain,
! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(a3),a3),X0)))),multiply(X1,inverse(X0))),
inference(forward_demodulation,[],[f3431,f3265]) ).
fof(f4323,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(inverse(multiply(inverse(X0),X0))))) = inverse(multiply(multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0)))),X0)))),multiply(X2,inverse(X0))),inverse(multiply(X1,multiply(inverse(X0),X0))))),
inference(forward_demodulation,[],[f3365,f3457]) ).
fof(f4336,plain,
! [X3,X0,X1] : multiply(multiply(multiply(inverse(multiply(X3,inverse(X0))),multiply(X3,inverse(multiply(inverse(X1),X1)))),multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1))),multiply(inverse(X1),X1)) = X0,
inference(forward_demodulation,[],[f3349,f3265]) ).
fof(f4399,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(multiply(inverse(multiply(X1,inverse(multiply(X2,X0)))),multiply(X1,inverse(X0))),inverse(multiply(X3,multiply(inverse(X0),X0))))),X2),inverse(multiply(inverse(X0),X0))) = X3,
inference(forward_demodulation,[],[f3283,f3457]) ).
fof(f4438,plain,
! [X0] : multiply(multiply(inverse(a3),a3),multiply(multiply(inverse(b3),b3),inverse(X0))) = multiply(inverse(multiply(inverse(inverse(X0)),multiply(inverse(c3),c3))),multiply(inverse(a3),a3)),
inference(forward_demodulation,[],[f4005,f3265]) ).
fof(f4524,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(X3,inverse(a3))),multiply(X3,inverse(inverse(multiply(inverse(sF2),sF2))))),inverse(multiply(inverse(inverse(multiply(inverse(sF2),sF2))),inverse(multiply(inverse(sF2),sF2)))))))),multiply(X1,inverse(multiply(X0,inverse(sF2))))) = multiply(multiply(inverse(multiply(X2,inverse(inverse(multiply(X0,inverse(sF3)))))),multiply(X2,inverse(multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(sF2)))))),multiply(inverse(a3),a3)),
inference(forward_demodulation,[],[f4088,f1969]) ).
fof(f4729,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(inverse(multiply(inverse(X0),X0))))) = inverse(multiply(multiply(inverse(multiply(X2,inverse(multiply(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0))),X0)))),multiply(X2,inverse(X0))),inverse(multiply(X1,multiply(inverse(X0),X0))))),
inference(forward_demodulation,[],[f4323,f3265]) ).
fof(f4742,plain,
! [X3,X0,X1] : multiply(multiply(multiply(inverse(multiply(X3,inverse(X0))),multiply(X3,inverse(multiply(inverse(X1),X1)))),multiply(inverse(a3),a3)),multiply(inverse(X1),X1)) = X0,
inference(forward_demodulation,[],[f4336,f1969]) ).
fof(f4805,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(multiply(inverse(multiply(X1,inverse(multiply(X2,X0)))),multiply(X1,inverse(X0))),inverse(multiply(X3,multiply(inverse(X0),X0))))),X2),multiply(inverse(X0),X0)) = X3,
inference(forward_demodulation,[],[f4399,f3265]) ).
fof(f4906,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(X3,inverse(a3))),multiply(X3,inverse(inverse(multiply(inverse(sF2),sF2))))),inverse(multiply(inverse(inverse(multiply(inverse(sF2),sF2))),inverse(multiply(inverse(sF2),sF2)))))))),multiply(X1,inverse(multiply(X0,inverse(sF2))))) = multiply(multiply(inverse(multiply(X2,inverse(inverse(multiply(X0,inverse(sF3)))))),multiply(X2,multiply(inverse(multiply(X0,inverse(sF2))),multiply(X0,inverse(sF2))))),multiply(inverse(a3),a3)),
inference(forward_demodulation,[],[f4524,f3265]) ).
fof(f5054,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(inverse(multiply(inverse(X0),X0))))) = inverse(multiply(multiply(inverse(multiply(X2,inverse(multiply(multiply(inverse(a3),a3),X0)))),multiply(X2,inverse(X0))),inverse(multiply(X1,multiply(inverse(X0),X0))))),
inference(forward_demodulation,[],[f4729,f1969]) ).
fof(f5067,plain,
! [X3,X0,X1] : multiply(multiply(multiply(inverse(multiply(X3,inverse(X0))),multiply(X3,multiply(inverse(X1),X1))),multiply(inverse(a3),a3)),multiply(inverse(X1),X1)) = X0,
inference(forward_demodulation,[],[f4742,f3265]) ).
fof(f5210,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(X3,inverse(a3))),multiply(X3,inverse(inverse(multiply(inverse(sF2),sF2))))),inverse(multiply(inverse(inverse(multiply(inverse(sF2),sF2))),inverse(multiply(inverse(sF2),sF2)))))))),multiply(X1,inverse(multiply(X0,inverse(sF2))))) = multiply(multiply(inverse(multiply(X2,inverse(inverse(multiply(X0,inverse(sF3)))))),multiply(X2,multiply(inverse(a3),a3))),multiply(inverse(a3),a3)),
inference(forward_demodulation,[],[f4906,f1969]) ).
fof(f5332,plain,
! [X3,X0,X1] : multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(inverse(multiply(inverse(X0),X0))))) = inverse(multiply(multiply(inverse(X0),X0),inverse(multiply(X1,multiply(inverse(X0),X0))))),
inference(forward_demodulation,[],[f5054,f4276]) ).
fof(f5433,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(X2,inverse(inverse(multiply(X0,inverse(sF3)))))),multiply(X2,multiply(inverse(a3),a3))),multiply(inverse(a3),a3)) = multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(X3,inverse(a3))),multiply(X3,inverse(inverse(multiply(inverse(sF2),sF2))))),multiply(inverse(inverse(multiply(inverse(sF2),sF2))),inverse(multiply(inverse(sF2),sF2))))))),multiply(X1,inverse(multiply(X0,inverse(sF2))))),
inference(forward_demodulation,[],[f5210,f3265]) ).
fof(f5521,plain,
! [X3,X0,X1] : multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(multiply(inverse(X0),X0)))) = inverse(multiply(multiply(inverse(X0),X0),inverse(multiply(X1,multiply(inverse(X0),X0))))),
inference(forward_demodulation,[],[f5332,f3265]) ).
fof(f5592,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(X2,inverse(inverse(multiply(X0,inverse(sF3)))))),multiply(X2,multiply(inverse(a3),a3))),multiply(inverse(a3),a3)) = multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(X3,inverse(a3))),multiply(X3,inverse(inverse(multiply(inverse(sF2),sF2))))),multiply(inverse(a3),a3))))),multiply(X1,inverse(multiply(X0,inverse(sF2))))),
inference(forward_demodulation,[],[f5433,f1969]) ).
fof(f5648,plain,
! [X3,X0,X1] : multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,multiply(inverse(X0),X0))) = inverse(multiply(multiply(inverse(X0),X0),inverse(multiply(X1,multiply(inverse(X0),X0))))),
inference(forward_demodulation,[],[f5521,f3265]) ).
fof(f5694,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(X2,inverse(inverse(multiply(X0,inverse(sF3)))))),multiply(X2,multiply(inverse(a3),a3))),multiply(inverse(a3),a3)) = multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(X3,inverse(a3))),multiply(X3,inverse(multiply(inverse(sF2),sF2)))),multiply(inverse(a3),a3))))),multiply(X1,inverse(multiply(X0,inverse(sF2))))),
inference(forward_demodulation,[],[f5592,f3265]) ).
fof(f5755,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(X2,inverse(inverse(multiply(X0,inverse(sF3)))))),multiply(X2,multiply(inverse(a3),a3))),multiply(inverse(a3),a3)) = multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(X3,inverse(a3))),multiply(X3,multiply(inverse(sF2),sF2))),multiply(inverse(a3),a3))))),multiply(X1,inverse(multiply(X0,inverse(sF2))))),
inference(forward_demodulation,[],[f5694,f3265]) ).
fof(f5797,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(X2,inverse(inverse(multiply(X0,inverse(sF3)))))),multiply(X2,multiply(inverse(a3),a3))),multiply(inverse(a3),a3)) = multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(X3,inverse(a3))),multiply(X3,multiply(inverse(a3),a3))),multiply(inverse(a3),a3))))),multiply(X1,inverse(multiply(X0,inverse(sF2))))),
inference(forward_demodulation,[],[f5755,f1969]) ).
fof(f5874,plain,
! [X0,X1] : inverse(multiply(X1,multiply(inverse(c3),c3))) = inverse(multiply(X1,multiply(inverse(X0),X0))),
inference(superposition,[],[f4019,f1995]) ).
fof(f5897,plain,
! [X0,X1] : inverse(multiply(inverse(c3),c3)) = inverse(multiply(multiply(inverse(X0),X0),multiply(inverse(X1),X1))),
inference(superposition,[],[f5874,f3457]) ).
fof(f5898,plain,
! [X2,X0,X1] : inverse(multiply(X1,multiply(inverse(X0),X0))) = inverse(multiply(X1,multiply(inverse(X2),X2))),
inference(superposition,[],[f5874,f5874]) ).
fof(f5940,plain,
! [X1] : inverse(multiply(inverse(c3),c3)) = inverse(multiply(inverse(X1),X1)),
inference(forward_demodulation,[],[f5897,f3457]) ).
fof(f5941,plain,
! [X1] : multiply(inverse(c3),c3) = inverse(multiply(inverse(X1),X1)),
inference(forward_demodulation,[],[f5940,f3265]) ).
fof(f6037,plain,
! [X2,X0,X1] : inverse(multiply(X2,inverse(multiply(X1,multiply(inverse(c3),c3))))) = inverse(multiply(X2,inverse(multiply(multiply(inverse(multiply(X1,multiply(inverse(c3),c3))),multiply(X1,multiply(inverse(X0),X0))),multiply(X1,multiply(inverse(X0),X0)))))),
inference(superposition,[],[f3458,f5874]) ).
fof(f6040,plain,
! [X2,X0,X1] : inverse(multiply(X2,inverse(X0))) = inverse(multiply(X2,inverse(multiply(multiply(inverse(X1),X1),X0)))),
inference(superposition,[],[f3458,f1995]) ).
fof(f6095,plain,
! [X2,X0,X1] : inverse(multiply(X2,inverse(multiply(X1,multiply(inverse(c3),c3))))) = inverse(multiply(X2,inverse(multiply(multiply(inverse(a3),a3),multiply(X1,multiply(inverse(X0),X0)))))),
inference(forward_demodulation,[],[f6037,f4272]) ).
fof(f6109,plain,
! [X2,X0,X1] : inverse(multiply(X2,inverse(multiply(X1,multiply(inverse(c3),c3))))) = inverse(multiply(X2,inverse(multiply(X1,multiply(inverse(X0),X0))))),
inference(forward_demodulation,[],[f6095,f6040]) ).
fof(f6131,plain,
! [X2,X0,X1] : inverse(multiply(inverse(X2),X2)) = inverse(multiply(inverse(inverse(multiply(multiply(inverse(X0),X0),X1))),inverse(X1))),
inference(superposition,[],[f6040,f1995]) ).
fof(f6158,plain,
! [X0,X1] : multiply(inverse(c3),c3) = inverse(multiply(inverse(inverse(multiply(multiply(inverse(X0),X0),X1))),inverse(X1))),
inference(forward_demodulation,[],[f6131,f5941]) ).
fof(f6195,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(inverse(multiply(multiply(inverse(multiply(X4,inverse(multiply(X2,multiply(inverse(X0),X0))))),multiply(X4,inverse(multiply(inverse(X1),X1)))),inverse(multiply(X3,multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1)))))),X2),multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1))) = X3,
inference(superposition,[],[f4805,f5898]) ).
fof(f6254,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(inverse(multiply(multiply(inverse(multiply(X4,inverse(multiply(X2,multiply(inverse(X0),X0))))),multiply(X4,inverse(multiply(inverse(X1),X1)))),inverse(multiply(X3,multiply(inverse(a3),a3))))),X2),multiply(inverse(a3),a3)) = X3,
inference(forward_demodulation,[],[f6195,f1969]) ).
fof(f6288,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(inverse(multiply(multiply(inverse(multiply(X4,inverse(multiply(X2,multiply(inverse(X0),X0))))),multiply(X4,inverse(multiply(inverse(X1),X1)))),inverse(multiply(X3,multiply(inverse(c3),c3))))),X2),multiply(inverse(a3),a3)) = X3,
inference(forward_demodulation,[],[f6254,f6109]) ).
fof(f6297,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(inverse(multiply(multiply(inverse(multiply(X4,inverse(multiply(X2,multiply(inverse(X0),X0))))),multiply(X4,multiply(inverse(X1),X1))),inverse(multiply(X3,multiply(inverse(c3),c3))))),X2),multiply(inverse(a3),a3)) = X3,
inference(forward_demodulation,[],[f6288,f3265]) ).
fof(f6562,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(X3))) = multiply(multiply(inverse(c3),c3),multiply(inverse(inverse(multiply(multiply(inverse(X0),X0),X1))),inverse(X3))),
inference(superposition,[],[f980,f6158]) ).
fof(f6898,plain,
! [X2,X0,X1] : inverse(X0) = multiply(multiply(inverse(multiply(X2,multiply(inverse(c3),c3))),multiply(X2,inverse(X0))),multiply(inverse(X1),X1)),
inference(superposition,[],[f3434,f5941]) ).
fof(f6899,plain,
! [X2,X3,X0,X1] : inverse(inverse(multiply(multiply(inverse(X0),X0),X1))) = multiply(multiply(inverse(multiply(X3,multiply(inverse(c3),c3))),multiply(X3,inverse(inverse(X1)))),multiply(inverse(X2),X2)),
inference(superposition,[],[f3434,f6158]) ).
fof(f6902,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(inverse(multiply(X4,inverse(multiply(X2,multiply(inverse(X0),X0))))),multiply(X4,inverse(multiply(inverse(X1),X1)))),multiply(inverse(X3),X3)) = X2,
inference(superposition,[],[f3434,f5898]) ).
fof(f6908,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(inverse(multiply(X0,X1))),inverse(X1))),multiply(inverse(X3),X3)) = X0,
inference(superposition,[],[f3434,f1995]) ).
fof(f6956,plain,
! [X2,X3,X0,X1] : multiply(multiply(multiply(inverse(X2),X2),multiply(inverse(inverse(multiply(X0,X1))),inverse(X1))),multiply(inverse(X3),X3)) = X0,
inference(forward_demodulation,[],[f6908,f3265]) ).
fof(f6960,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(inverse(multiply(X4,inverse(multiply(X2,multiply(inverse(X0),X0))))),multiply(X4,multiply(inverse(X1),X1))),multiply(inverse(X3),X3)) = X2,
inference(forward_demodulation,[],[f6902,f3265]) ).
fof(f6963,plain,
! [X0,X1] : inverse(inverse(X1)) = inverse(inverse(multiply(multiply(inverse(X0),X0),X1))),
inference(backward_demodulation,[],[f6899,f6898]) ).
fof(f6986,plain,
! [X2,X3,X1] : multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(X3))) = multiply(multiply(inverse(c3),c3),multiply(inverse(inverse(X1)),inverse(X3))),
inference(backward_demodulation,[],[f6562,f6963]) ).
fof(f7272,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X4,inverse(multiply(multiply(X2,multiply(inverse(X3),X3)),multiply(inverse(X0),X0))))),multiply(X4,inverse(multiply(inverse(X1),X1)))) = X2,
inference(superposition,[],[f3437,f5898]) ).
fof(f7301,plain,
! [X0,X1,X4] : multiply(X1,multiply(inverse(X0),X0)) = multiply(X1,multiply(inverse(X4),X4)),
inference(superposition,[],[f3434,f3437]) ).
fof(f7316,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X4,inverse(multiply(multiply(X2,multiply(inverse(X3),X3)),multiply(inverse(X0),X0))))),multiply(X4,multiply(inverse(X1),X1))) = X2,
inference(forward_demodulation,[],[f7272,f3265]) ).
fof(f9019,plain,
! [X2,X3,X0,X1] : inverse(X1) = multiply(multiply(multiply(inverse(X3),X3),multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(X1))),multiply(inverse(X2),X2)),
inference(superposition,[],[f6956,f1995]) ).
fof(f9058,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(multiply(inverse(X4),X4),multiply(inverse(inverse(multiply(X2,multiply(inverse(X0),X0)))),inverse(multiply(inverse(X1),X1)))),multiply(inverse(X3),X3)) = X2,
inference(superposition,[],[f6956,f5898]) ).
fof(f9119,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(multiply(inverse(X4),X4),multiply(inverse(inverse(multiply(X2,multiply(inverse(X0),X0)))),multiply(inverse(X1),X1))),multiply(inverse(X3),X3)) = X2,
inference(forward_demodulation,[],[f9058,f3265]) ).
fof(f9139,plain,
! [X2,X3,X0,X1] : inverse(X1) = multiply(multiply(multiply(inverse(X3),X3),multiply(inverse(multiply(inverse(X0),X0)),inverse(X1))),multiply(inverse(X2),X2)),
inference(forward_demodulation,[],[f9019,f3265]) ).
fof(f9180,plain,
! [X2,X3,X0,X1] : inverse(X1) = multiply(multiply(multiply(inverse(X3),X3),multiply(multiply(inverse(X0),X0),inverse(X1))),multiply(inverse(X2),X2)),
inference(forward_demodulation,[],[f9139,f3265]) ).
fof(f9206,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(X2),X2),X1) = multiply(multiply(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,multiply(inverse(X3),X3))),multiply(inverse(a3),a3)),multiply(inverse(X3),X3)),
inference(superposition,[],[f5067,f6040]) ).
fof(f9282,plain,
! [X2,X3,X0,X1] : multiply(multiply(multiply(inverse(multiply(X2,inverse(X0))),multiply(X2,multiply(inverse(X1),X1))),multiply(inverse(a3),a3)),multiply(inverse(X3),X3)) = X0,
inference(superposition,[],[f7301,f5067]) ).
fof(f9303,plain,
! [X2,X1] : multiply(multiply(inverse(X2),X2),X1) = X1,
inference(forward_demodulation,[],[f9206,f9282]) ).
fof(f9505,plain,
! [X1] : b3 = multiply(multiply(inverse(inverse(sF2)),inverse(c3)),multiply(inverse(X1),X1)),
inference(backward_demodulation,[],[f4274,f9303]) ).
fof(f9529,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(inverse(multiply(X2,multiply(inverse(X0),X0)))),multiply(inverse(X1),X1)),multiply(inverse(X3),X3)) = X2,
inference(backward_demodulation,[],[f9119,f9303]) ).
fof(f9543,plain,
! [X2,X0,X1] : inverse(X1) = multiply(multiply(multiply(inverse(X0),X0),inverse(X1)),multiply(inverse(X2),X2)),
inference(backward_demodulation,[],[f9180,f9303]) ).
fof(f9606,plain,
! [X0] : multiply(multiply(inverse(b3),b3),inverse(X0)) = multiply(inverse(multiply(inverse(inverse(X0)),multiply(inverse(c3),c3))),multiply(inverse(a3),a3)),
inference(backward_demodulation,[],[f4438,f9303]) ).
fof(f9616,plain,
! [X2,X3,X1] : multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(X3))) = multiply(inverse(inverse(X1)),inverse(X3)),
inference(backward_demodulation,[],[f6986,f9303]) ).
fof(f9625,plain,
! [X3,X0,X1] : multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,multiply(inverse(X0),X0))) = inverse(inverse(multiply(X1,multiply(inverse(X0),X0)))),
inference(backward_demodulation,[],[f5648,f9303]) ).
fof(f9697,plain,
! [X2,X3,X0,X1] : multiply(inverse(inverse(multiply(multiply(X2,multiply(inverse(X0),X0)),multiply(inverse(X1),X1)))),multiply(inverse(X3),X3)) = X2,
inference(backward_demodulation,[],[f6960,f9625]) ).
fof(f9698,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(inverse(inverse(multiply(multiply(X2,multiply(inverse(X0),X0)),multiply(inverse(X1),X1)))),inverse(multiply(X3,multiply(inverse(c3),c3))))),X2),multiply(inverse(a3),a3)) = X3,
inference(backward_demodulation,[],[f6297,f9625]) ).
fof(f9699,plain,
! [X2,X3,X0,X1] : inverse(inverse(multiply(multiply(multiply(X2,multiply(inverse(X3),X3)),multiply(inverse(X0),X0)),multiply(inverse(X1),X1)))) = X2,
inference(backward_demodulation,[],[f7316,f9625]) ).
fof(f9768,plain,
! [X3,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(X3,inverse(a3))),multiply(X3,multiply(inverse(a3),a3))),multiply(inverse(a3),a3))))),multiply(X1,inverse(multiply(X0,inverse(sF2))))) = multiply(inverse(inverse(multiply(inverse(multiply(X0,inverse(sF3))),multiply(inverse(a3),a3)))),multiply(inverse(a3),a3)),
inference(backward_demodulation,[],[f5797,f9625]) ).
fof(f10038,plain,
! [X0,X1] : multiply(inverse(inverse(X1)),inverse(X0)) = multiply(inverse(multiply(inverse(inverse(X0)),inverse(X1))),multiply(inverse(a3),a3)),
inference(backward_demodulation,[],[f2042,f9616]) ).
fof(f10084,plain,
! [X0] : inverse(X0) = multiply(inverse(multiply(inverse(inverse(X0)),multiply(inverse(c3),c3))),multiply(inverse(a3),a3)),
inference(forward_demodulation,[],[f9606,f9303]) ).
fof(f10126,plain,
! [X2,X1] : inverse(X1) = multiply(inverse(X1),multiply(inverse(X2),X2)),
inference(forward_demodulation,[],[f9543,f9303]) ).
fof(f10368,plain,
! [X3,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(X3,inverse(a3))),multiply(X3,multiply(inverse(a3),a3))),multiply(inverse(a3),a3))))),multiply(X1,inverse(multiply(X0,inverse(sF2))))) = multiply(inverse(inverse(multiply(inverse(multiply(X0,inverse(sF3))),multiply(inverse(c3),c3)))),multiply(inverse(a3),a3)),
inference(forward_demodulation,[],[f9768,f5874]) ).
fof(f10659,plain,
! [X0,X1] : multiply(inverse(inverse(X1)),inverse(X0)) = inverse(multiply(inverse(inverse(X0)),inverse(X1))),
inference(backward_demodulation,[],[f10038,f10126]) ).
fof(f10660,plain,
! [X0] : inverse(X0) = inverse(multiply(inverse(inverse(X0)),multiply(inverse(c3),c3))),
inference(backward_demodulation,[],[f10084,f10126]) ).
fof(f10663,plain,
! [X2,X3,X0] : multiply(inverse(inverse(multiply(X2,multiply(inverse(X0),X0)))),multiply(inverse(X3),X3)) = X2,
inference(backward_demodulation,[],[f9529,f10126]) ).
fof(f10664,plain,
! [X2,X0,X1] : inverse(inverse(multiply(multiply(X2,multiply(inverse(X0),X0)),multiply(inverse(X1),X1)))) = X2,
inference(backward_demodulation,[],[f9697,f10126]) ).
fof(f10869,plain,
! [X3,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(X3,inverse(a3))),multiply(X3,multiply(inverse(a3),a3))),multiply(inverse(a3),a3))))),multiply(X1,inverse(multiply(X0,inverse(sF2))))) = inverse(inverse(multiply(inverse(multiply(X0,inverse(sF3))),multiply(inverse(c3),c3)))),
inference(forward_demodulation,[],[f10368,f10126]) ).
fof(f11111,plain,
! [X2,X3] : multiply(multiply(inverse(multiply(X2,inverse(multiply(X3,multiply(inverse(c3),c3))))),X2),multiply(inverse(a3),a3)) = X3,
inference(backward_demodulation,[],[f9698,f10664]) ).
fof(f11112,plain,
! [X2,X3] : multiply(X2,multiply(inverse(X3),X3)) = X2,
inference(backward_demodulation,[],[f9699,f10664]) ).
fof(f11113,plain,
! [X2,X0] : inverse(inverse(multiply(X2,multiply(inverse(X0),X0)))) = X2,
inference(forward_demodulation,[],[f10663,f10126]) ).
fof(f11117,plain,
! [X0] : inverse(X0) = inverse(inverse(inverse(X0))),
inference(forward_demodulation,[],[f10660,f10126]) ).
fof(f11310,plain,
! [X3,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(X3,inverse(a3))),multiply(X3,multiply(inverse(a3),a3))),multiply(inverse(a3),a3))))),multiply(X1,inverse(multiply(X0,inverse(sF2))))) = inverse(inverse(inverse(multiply(X0,inverse(sF3))))),
inference(forward_demodulation,[],[f10869,f10126]) ).
fof(f11657,plain,
b3 = multiply(inverse(inverse(sF2)),inverse(c3)),
inference(backward_demodulation,[],[f9505,f11112]) ).
fof(f11670,plain,
! [X2,X3] : multiply(inverse(multiply(X2,inverse(multiply(X3,multiply(inverse(c3),c3))))),X2) = X3,
inference(forward_demodulation,[],[f11111,f11112]) ).
fof(f11672,plain,
! [X2] : inverse(inverse(X2)) = X2,
inference(forward_demodulation,[],[f11113,f11112]) ).
fof(f11852,plain,
! [X3,X0,X1] : inverse(multiply(X0,inverse(sF3))) = multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(multiply(X3,inverse(a3))),multiply(X3,multiply(inverse(a3),a3))),multiply(inverse(a3),a3))))),multiply(X1,inverse(multiply(X0,inverse(sF2))))),
inference(forward_demodulation,[],[f11310,f11117]) ).
fof(f12181,plain,
! [X2,X3] : multiply(inverse(multiply(X2,inverse(X3))),X2) = X3,
inference(forward_demodulation,[],[f11670,f11112]) ).
fof(f12183,plain,
! [X2,X3,X1] : multiply(X1,inverse(X3)) = multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(X3))),
inference(backward_demodulation,[],[f9616,f11672]) ).
fof(f12184,plain,
! [X0,X1] : inverse(multiply(X0,inverse(X1))) = multiply(inverse(inverse(X1)),inverse(X0)),
inference(backward_demodulation,[],[f10659,f11672]) ).
fof(f12193,plain,
b3 = multiply(sF2,inverse(c3)),
inference(backward_demodulation,[],[f11657,f11672]) ).
fof(f12363,plain,
! [X3,X0,X1] : inverse(multiply(X0,inverse(sF3))) = multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(X3,inverse(a3))),multiply(X3,multiply(inverse(a3),a3)))))),multiply(X1,inverse(multiply(X0,inverse(sF2))))),
inference(forward_demodulation,[],[f11852,f11112]) ).
fof(f12658,plain,
! [X0,X1] : multiply(X1,inverse(X0)) = inverse(multiply(X0,inverse(X1))),
inference(forward_demodulation,[],[f12184,f11672]) ).
fof(f12776,plain,
! [X3,X0] : inverse(multiply(X0,inverse(sF3))) = multiply(multiply(inverse(multiply(X3,inverse(a3))),multiply(X3,multiply(inverse(a3),a3))),inverse(multiply(X0,inverse(sF2)))),
inference(forward_demodulation,[],[f12363,f12183]) ).
fof(f13024,plain,
! [X2,X3] : multiply(multiply(X3,inverse(X2)),X2) = X3,
inference(backward_demodulation,[],[f12181,f12658]) ).
fof(f13128,plain,
! [X3,X0] : inverse(multiply(X0,inverse(sF3))) = multiply(multiply(inverse(multiply(X3,inverse(a3))),multiply(X3,multiply(inverse(a3),a3))),multiply(sF2,inverse(X0))),
inference(forward_demodulation,[],[f12776,f12658]) ).
fof(f13416,plain,
! [X3,X0] : inverse(multiply(X0,inverse(sF3))) = multiply(multiply(inverse(multiply(X3,inverse(a3))),X3),multiply(sF2,inverse(X0))),
inference(forward_demodulation,[],[f13128,f11112]) ).
fof(f13655,plain,
! [X3,X0] : inverse(multiply(X0,inverse(sF3))) = multiply(multiply(multiply(a3,inverse(X3)),X3),multiply(sF2,inverse(X0))),
inference(forward_demodulation,[],[f13416,f12658]) ).
fof(f13820,plain,
! [X0] : inverse(multiply(X0,inverse(sF3))) = multiply(a3,multiply(sF2,inverse(X0))),
inference(forward_demodulation,[],[f13655,f13024]) ).
fof(f13947,plain,
! [X0] : multiply(sF3,inverse(X0)) = multiply(a3,multiply(sF2,inverse(X0))),
inference(forward_demodulation,[],[f13820,f12658]) ).
fof(f14902,plain,
multiply(a3,b3) = multiply(sF3,inverse(c3)),
inference(superposition,[],[f13947,f12193]) ).
fof(f14917,plain,
sF0 = multiply(sF3,inverse(c3)),
inference(forward_demodulation,[],[f14902,f4]) ).
fof(f14924,plain,
multiply(sF0,c3) = sF3,
inference(superposition,[],[f13024,f14917]) ).
fof(f14926,plain,
sF1 = sF3,
inference(backward_demodulation,[],[f6,f14924]) ).
fof(f14927,plain,
$false,
inference(forward_subsumption_resolution,[],[f14926,f11]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP411-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.37 % Computer : n001.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.37 % CPULimit : 300
% 0.11/0.37 % WCLimit : 300
% 0.11/0.37 % DateTime : Sun Sep 27 10:09:22 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 9.93/2.25 % (3320019)Detected a unit-equality problem, will run specialized UEQ schedule.
% 9.93/2.25 % (3320109)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=3781971269:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 9.93/2.25 % (3320108)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=1836669821:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 9.93/2.25 % (3320107)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=3969554184:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 9.93/2.25 % (3320103)lrs+1002_1_ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:drc=off:sp=reverse_frequency:spb=goal:acc=on:s2agt=16:kmz=on:sac=on:random_seed=4066362586:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 9.93/2.25 % (3320105)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=2611693826:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 9.93/2.25 % (3320106)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=3971053794:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 9.93/2.25 % (3320104)lrs+11_1_ncem=casc2026/models/loop6.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=673596224:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 9.93/2.25 % (3320106)Instruction limit reached!
% 9.93/2.25 % (3320106)------------------------------
% 9.93/2.25 % (3320106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.93/2.25 % (3320106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.93/2.25 % (3320106)CaDiCaL version: 2.1.3
% 9.93/2.25 % (3320106)Termination reason: Instruction limit
% 9.93/2.25 % (3320106)Termination phase: Saturation
% 9.93/2.25 % (3320106)Time elapsed: 0.075 s
% 9.93/2.25 % (3320106)Peak memory usage: 89 MB
% 9.93/2.25 % (3320106)Instructions burned: 137 (million)
% 9.93/2.25 % (3320107)Instruction limit reached!
% 9.93/2.25 % (3320107)------------------------------
% 9.93/2.25 % (3320107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.93/2.25 % (3320107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.93/2.25 % (3320107)CaDiCaL version: 2.1.3
% 9.93/2.25 % (3320107)Termination reason: Instruction limit
% 9.93/2.25 % (3320107)Termination phase: Saturation
% 9.93/2.25 % (3320107)Time elapsed: 0.094 s
% 9.93/2.25 % (3320107)Peak memory usage: 89 MB
% 9.93/2.25 % (3320107)Instructions burned: 182 (million)
% 9.93/2.25 % (3320108)Instruction limit reached!
% 9.93/2.25 % (3320108)------------------------------
% 9.93/2.25 % (3320108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.93/2.25 % (3320108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.93/2.25 % (3320108)CaDiCaL version: 2.1.3
% 9.93/2.25 % (3320108)Termination reason: Instruction limit
% 9.93/2.25 % (3320108)Termination phase: Saturation
% 9.93/2.25 % (3320108)Time elapsed: 0.156 s
% 9.93/2.25 % (3320108)Peak memory usage: 90 MB
% 9.93/2.25 % (3320108)Instructions burned: 259 (million)
% 9.93/2.25 % (3320117)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=2302211393:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 9.93/2.25 % (3320118)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=649274814:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 9.93/2.25 % (3320119)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=2594179405:i=215:ep=RSTC_2996 on theBenchmark for (2996ds/215Mi)
% 9.93/2.25 % (3320109)Instruction limit reached!
% 9.93/2.25 % (3320109)------------------------------
% 9.93/2.25 % (3320109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.93/2.25 % (3320109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.93/2.25 % (3320109)CaDiCaL version: 2.1.3
% 9.93/2.25 % (3320109)Termination reason: Instruction limit
% 9.93/2.25 % (3320109)Termination phase: Saturation
% 9.93/2.25 % (3320109)Time elapsed: 0.320 s
% 9.93/2.25 % (3320109)Peak memory usage: 94 MB
% 9.93/2.25 % (3320109)Instructions burned: 1188 (million)
% 9.93/2.25 % (3320123)lrs+11_1_sil=16000:tgt=full:fde=none:sp=reverse_frequency:lma=off:fs=off:acc=on:bsr=unit_only:rp=on:random_seed=3678519577:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2995 on theBenchmark for (2995ds/317Mi)
% 9.93/2.25 % (3320119)Instruction limit reached!
% 9.93/2.25 % (3320119)------------------------------
% 9.93/2.25 % (3320119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.93/2.25 % (3320119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.93/2.25 % (3320119)CaDiCaL version: 2.1.3
% 9.93/2.25 % (3320119)Termination reason: Instruction limit
% 9.93/2.25 % (3320119)Termination phase: Saturation
% 9.93/2.25 % (3320119)Time elapsed: 0.129 s
% 9.93/2.25 % (3320119)Peak memory usage: 89 MB
% 9.93/2.25 % (3320119)Instructions burned: 215 (million)
% 9.93/2.25 % (3320123)Instruction limit reached!
% 9.93/2.25 % (3320123)------------------------------
% 9.93/2.25 % (3320123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.93/2.25 % (3320123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.93/2.25 % (3320123)CaDiCaL version: 2.1.3
% 9.93/2.25 % (3320123)Termination reason: Instruction limit
% 9.93/2.25 % (3320123)Termination phase: Saturation
% 9.93/2.25 % (3320123)Time elapsed: 0.084 s
% 9.93/2.25 % (3320123)Peak memory usage: 89 MB
% 9.93/2.25 % (3320123)Instructions burned: 318 (million)
% 9.93/2.25 % (3320125)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:sp=arity:lcm=predicate:urr=on:s2agt=16:br=off:random_seed=97197203:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2994 on theBenchmark for (2994ds/12125Mi)
% 9.93/2.25 % (3320126)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=3799485872:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2993 on theBenchmark for (2993ds/2836Mi)
% 9.93/2.25 % (3320126)First to succeed.
% 9.93/2.25 % (3320126)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3320019"
% 9.93/2.25 % (3320126)Refutation found. Thanks to Tanya!
% 9.93/2.25 % SZS status Unsatisfiable for theBenchmark
% 9.93/2.25 % SZS output start Proof for theBenchmark
% See solution above
% 10.39/2.34 % (3320126)------------------------------
% 10.39/2.34 % (3320126)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.39/2.34 % (3320126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.39/2.34 % (3320126)CaDiCaL version: 2.1.3
% 10.39/2.34 % (3320126)Termination reason: Refutation
% 10.39/2.34 % (3320126)Time elapsed: 0.538 s
% 10.39/2.34 % (3320126)Peak memory usage: 99 MB
% 10.39/2.34 % (3320126)Instructions burned: 1813 (million)
% 10.39/2.34 % (3320126)------------------------------
% 10.39/2.34 % (3320126)------------------------------
% 10.39/2.34 % (3320019)Success in time 1.4 s
% 10.39/2.34 % Vampire exiting
%------------------------------------------------------------------------------