%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GRP051-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 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:16:30 AM UTC 2026
% Result : Unsatisfiable 145.34s 31.44s
% Output : Refutation 145.34s
% Verified :
% SZS Type : Refutation
% Derivation depth : 86
% Number of leaves : 5
% Syntax : Number of formulae : 259 ( 245 unt; 3 def)
% Number of atoms : 277 ( 250 equ)
% Maximal formula atoms : 3 ( 1 avg)
% Number of connectives : 34 ( 16 ~; 15 |; 0 &)
% ( 3 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 7 ( 4 avg)
% Maximal term depth : 14 ( 3 avg)
% Number of predicates : 5 ( 3 usr; 4 prp; 0-2 aty)
% Number of functors : 9 ( 9 usr; 7 con; 0-2 aty)
% Number of variables : 788 ( 0 sgn 788 !; 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(inverse(a1),a1) != multiply(inverse(b1),b1)
| multiply(multiply(inverse(b2),b2),a2) != a2
| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_these_axioms) ).
fof(f3,plain,
( multiply(inverse(a1),a1) != multiply(inverse(b1),b1)
| a2 != multiply(multiply(inverse(b2),b2),a2)
| multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)) ),
inference(reorient_equations,[],[f2]) ).
fof(f5,definition,
( spl0_1
<=> multiply(multiply(a3,b3),c3) = multiply(a3,multiply(b3,c3)) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f7,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| spl0_1 ),
inference(avatar_component_clause,[],[f5]) ).
fof(f9,definition,
( spl0_2
<=> a2 = multiply(multiply(inverse(b2),b2),a2) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f11,plain,
( a2 != multiply(multiply(inverse(b2),b2),a2)
| spl0_2 ),
inference(avatar_component_clause,[],[f9]) ).
fof(f13,definition,
( spl0_3
<=> multiply(inverse(a1),a1) = multiply(inverse(b1),b1) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f15,plain,
( multiply(inverse(a1),a1) != multiply(inverse(b1),b1)
| spl0_3 ),
inference(avatar_component_clause,[],[f13]) ).
fof(f16,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f3,f13,f9,f5]) ).
fof(f17,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(f18,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(f19,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(f24,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(X1),X1)) = multiply(multiply(inverse(X2),multiply(multiply(inverse(multiply(multiply(inverse(multiply(X3,inverse(multiply(X0,X1)))),multiply(X3,inverse(X1))),inverse(multiply(X2,multiply(inverse(X1),X1))))),X0),inverse(multiply(inverse(X1),X1)))),inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1)))),
inference(superposition,[],[f18,f1]) ).
fof(f27,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X0)))),multiply(X2,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,[],[f1,f18]) ).
fof(f28,plain,
! [X2,X3,X0,X1] : multiply(inverse(X2),multiply(multiply(inverse(multiply(X3,inverse(multiply(X2,X0)))),multiply(X3,inverse(X0))),inverse(X0))) = multiply(multiply(inverse(multiply(X1,inverse(inverse(X0)))),multiply(X1,inverse(inverse(multiply(inverse(X0),X0))))),inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0))))),
inference(superposition,[],[f1,f18]) ).
fof(f88,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,[],[f17,f17]) ).
fof(f93,plain,
! [X2,X0,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(multiply(inverse(X2),X2))) = X1,
inference(superposition,[],[f1,f17]) ).
fof(f98,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,f17]) ).
fof(f134,plain,
! [X2,X3,X0,X1] : inverse(multiply(X2,inverse(multiply(multiply(X0,inverse(multiply(inverse(X3),X3))),X3)))) = multiply(multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,inverse(multiply(X2,inverse(X3))))),inverse(multiply(inverse(multiply(X2,inverse(X3))),multiply(X2,inverse(X3))))),
inference(superposition,[],[f1,f98]) ).
fof(f158,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X1,inverse(X0))),multiply(X1,inverse(multiply(X2,inverse(X3))))) = multiply(inverse(multiply(X4,inverse(X0))),multiply(X4,inverse(multiply(X2,inverse(X3))))),
inference(superposition,[],[f88,f98]) ).
fof(f227,plain,
! [X2,X0,X1,X6] : multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X0))) = multiply(inverse(multiply(X6,inverse(X2))),multiply(X6,inverse(X0))),
inference(superposition,[],[f158,f19]) ).
fof(f357,plain,
! [X2,X3,X0,X1,X4] : inverse(multiply(X4,inverse(X1))) = multiply(multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X2)))))),multiply(X3,inverse(multiply(X4,inverse(X2))))),inverse(multiply(inverse(multiply(X4,inverse(X2))),multiply(X4,inverse(X2))))),
inference(superposition,[],[f1,f227]) ).
fof(f358,plain,
! [X2,X0,X1,X4] : inverse(multiply(X4,inverse(X1))) = inverse(multiply(X4,inverse(multiply(multiply(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X2))),inverse(multiply(inverse(X2),X2))),X2)))),
inference(forward_demodulation,[],[f357,f134]) ).
fof(f427,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(X3))),inverse(multiply(inverse(X3),X3))),X3) = multiply(multiply(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(inverse(multiply(inverse(X4),X4))))),inverse(multiply(inverse(inverse(multiply(inverse(X4),X4))),inverse(multiply(inverse(X4),X4))))),inverse(multiply(inverse(X4),X4))),
inference(superposition,[],[f93,f358]) ).
fof(f454,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(X0,inverse(multiply(multiply(multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(X4))),inverse(multiply(inverse(X4),X4))),X4))) = multiply(multiply(multiply(inverse(multiply(X2,inverse(multiply(X0,inverse(X1))))),multiply(X2,inverse(inverse(multiply(inverse(X5),X5))))),inverse(multiply(inverse(inverse(multiply(inverse(X5),X5))),inverse(multiply(inverse(X5),X5))))),inverse(multiply(inverse(X5),X5))),
inference(superposition,[],[f93,f358]) ).
fof(f458,plain,
! [X3,X0,X1,X4] : multiply(X0,inverse(X1)) = multiply(X0,inverse(multiply(multiply(multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(X4))),inverse(multiply(inverse(X4),X4))),X4))),
inference(forward_demodulation,[],[f454,f93]) ).
fof(f473,plain,
! [X2,X3,X1] : multiply(multiply(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(X3))),inverse(multiply(inverse(X3),X3))),X3) = X1,
inference(forward_demodulation,[],[f427,f93]) ).
fof(f485,plain,
! [X2,X3,X0,X1] : multiply(inverse(X2),X2) = multiply(multiply(multiply(inverse(X0),multiply(multiply(inverse(multiply(X1,inverse(multiply(X0,X2)))),multiply(X1,inverse(X2))),inverse(X3))),inverse(multiply(inverse(X3),X3))),X3),
inference(superposition,[],[f473,f1]) ).
fof(f703,plain,
! [X0,X1] : multiply(inverse(X1),X1) = multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(X1),X1)))),multiply(inverse(X1),X1)),
inference(superposition,[],[f485,f1]) ).
fof(f776,plain,
! [X2,X0,X1] : multiply(inverse(X2),X2) = multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X0)))),multiply(X1,inverse(multiply(inverse(X0),X0)))),
inference(superposition,[],[f98,f703]) ).
fof(f813,plain,
! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(X1),X1),
inference(superposition,[],[f776,f776]) ).
fof(f971,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(X1,inverse(multiply(X2,X3)))),multiply(X1,inverse(X3))),inverse(multiply(inverse(X0),X0))) = X2,
inference(superposition,[],[f1,f813]) ).
fof(f973,plain,
! [X2,X3,X0,X1] : inverse(X1) = multiply(multiply(inverse(X2),multiply(multiply(inverse(multiply(X3,inverse(multiply(X2,X1)))),multiply(X3,inverse(X1))),inverse(X1))),inverse(multiply(inverse(X0),X0))),
inference(superposition,[],[f18,f813]) ).
fof(f976,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,inverse(multiply(multiply(X2,inverse(multiply(inverse(X0),X0))),X3)))),multiply(X1,inverse(X3))) = X2,
inference(superposition,[],[f98,f813]) ).
fof(f980,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(X1),X1) = multiply(multiply(multiply(inverse(X2),multiply(multiply(inverse(multiply(X3,inverse(multiply(X2,X1)))),multiply(X3,inverse(X1))),inverse(X4))),inverse(multiply(inverse(X0),X0))),X4),
inference(superposition,[],[f485,f813]) ).
fof(f984,plain,
! [X2,X0] : multiply(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(X2),X2))),X2) = X2,
inference(superposition,[],[f473,f813]) ).
fof(f990,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(inverse(multiply(multiply(inverse(multiply(X1,inverse(multiply(X2,X3)))),multiply(X1,inverse(X3))),inverse(multiply(X4,multiply(inverse(X3),X3))))),X2),inverse(multiply(inverse(X0),X0))) = X4,
inference(superposition,[],[f19,f813]) ).
fof(f1004,plain,
! [X2,X0,X1] : inverse(inverse(multiply(inverse(X2),X2))) = multiply(inverse(multiply(X1,inverse(multiply(multiply(inverse(X0),X0),X2)))),multiply(X1,inverse(X2))),
inference(superposition,[],[f98,f813]) ).
fof(f1007,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(X0),X0)) = inverse(multiply(inverse(inverse(multiply(multiply(multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X3))),inverse(multiply(inverse(X3),X3))),X3))),inverse(X2))),
inference(superposition,[],[f358,f813]) ).
fof(f1027,plain,
! [X2,X0] : inverse(multiply(inverse(X0),X0)) = inverse(multiply(inverse(inverse(X2)),inverse(X2))),
inference(forward_demodulation,[],[f1007,f473]) ).
fof(f1052,plain,
! [X0,X1] : inverse(multiply(inverse(X0),X0)) = inverse(multiply(inverse(X1),X1)),
inference(superposition,[],[f1027,f1027]) ).
fof(f1192,plain,
! [X2,X0,X1] : multiply(inverse(X2),X2) = multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X1),X1)),
inference(superposition,[],[f813,f1052]) ).
fof(f1218,plain,
! [X2,X0,X1] : multiply(multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(X0),X0))),X2) = X2,
inference(superposition,[],[f984,f1052]) ).
fof(f1269,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X0))) = multiply(inverse(multiply(multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(X4),X4))),inverse(X2))),inverse(X0)),
inference(superposition,[],[f227,f1218]) ).
fof(f1278,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,inverse(X0))) = multiply(inverse(inverse(X2)),inverse(X0)),
inference(forward_demodulation,[],[f1269,f1218]) ).
fof(f1526,plain,
! [X2,X0,X1] : multiply(inverse(inverse(X2)),inverse(X1)) = multiply(inverse(multiply(inverse(inverse(X1)),inverse(X2))),multiply(inverse(X0),X0)),
inference(superposition,[],[f1278,f813]) ).
fof(f1740,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(X4),X4))) = multiply(multiply(inverse(multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X0)))),multiply(X2,inverse(X0))),inverse(X0))),inverse(multiply(inverse(X0),X0)))),inverse(X0)),inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))),
inference(superposition,[],[f27,f1218]) ).
fof(f1744,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(X3),X3)) = multiply(multiply(inverse(multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X3)))),multiply(X2,inverse(X3))),inverse(X3))),inverse(multiply(inverse(X0),X0)))),inverse(X3)),inverse(multiply(inverse(X0),X0))),
inference(superposition,[],[f27,f1052]) ).
fof(f1835,plain,
! [X3,X0] : inverse(multiply(inverse(X3),X3)) = multiply(multiply(inverse(inverse(X3)),inverse(X3)),inverse(multiply(inverse(X0),X0))),
inference(forward_demodulation,[],[f1744,f973]) ).
fof(f1839,plain,
! [X3,X0,X4] : multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(X4),X4))) = multiply(multiply(inverse(inverse(X0)),inverse(X0)),inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))),
inference(forward_demodulation,[],[f1740,f973]) ).
fof(f1907,plain,
! [X3,X0,X4] : inverse(multiply(inverse(X0),X0)) = multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(X4),X4))),
inference(forward_demodulation,[],[f1839,f1835]) ).
fof(f2060,plain,
! [X3,X0] : multiply(inverse(multiply(inverse(X0),X0)),X3) = X3,
inference(superposition,[],[f1218,f1907]) ).
fof(f2425,plain,
! [X2,X3,X0,X1] : inverse(X2) = multiply(multiply(inverse(multiply(X1,inverse(multiply(inverse(X0),X0)))),multiply(X1,inverse(X2))),inverse(multiply(inverse(X3),X3))),
inference(superposition,[],[f971,f1052]) ).
fof(f2462,plain,
! [X2,X0,X1] : multiply(multiply(inverse(inverse(multiply(X0,X1))),inverse(X1)),inverse(multiply(inverse(X2),X2))) = X0,
inference(superposition,[],[f971,f2060]) ).
fof(f2494,plain,
! [X2,X3,X0,X1,X4,X5] : multiply(X1,inverse(multiply(inverse(X2),X2))) = multiply(X1,inverse(multiply(multiply(multiply(inverse(X0),multiply(multiply(inverse(multiply(X3,inverse(multiply(X0,X4)))),multiply(X3,inverse(X4))),inverse(X5))),inverse(multiply(inverse(X5),X5))),X5))),
inference(superposition,[],[f458,f971]) ).
fof(f2503,plain,
! [X2,X1,X4] : multiply(X1,inverse(multiply(inverse(X2),X2))) = multiply(X1,inverse(multiply(inverse(X4),X4))),
inference(forward_demodulation,[],[f2494,f980]) ).
fof(f2553,plain,
! [X2,X3,X0] : inverse(X2) = multiply(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(X2)),inverse(multiply(inverse(X3),X3))),
inference(forward_demodulation,[],[f2425,f1278]) ).
fof(f2768,plain,
! [X2,X0,X1] : inverse(multiply(inverse(X2),X2)) = inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X1),X1)))),
inference(superposition,[],[f1052,f2503]) ).
fof(f2784,plain,
! [X2,X0,X1] : multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X1),X1)))),X2) = X2,
inference(superposition,[],[f2060,f2503]) ).
fof(f6551,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(X2),X2)) = multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(X0),X0)),X3)))),multiply(X1,inverse(X3))),
inference(superposition,[],[f976,f2060]) ).
fof(f6716,plain,
! [X2,X3,X0] : inverse(multiply(inverse(X2),X2)) = multiply(inverse(inverse(multiply(inverse(multiply(inverse(X0),X0)),X3))),inverse(X3)),
inference(forward_demodulation,[],[f6551,f1278]) ).
fof(f6773,plain,
! [X2,X3] : inverse(multiply(inverse(X2),X2)) = multiply(inverse(inverse(X3)),inverse(X3)),
inference(forward_demodulation,[],[f6716,f2060]) ).
fof(f6895,plain,
! [X2,X0,X1] : inverse(X1) = multiply(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(X1)),multiply(inverse(inverse(X0)),inverse(X0))),
inference(superposition,[],[f2553,f6773]) ).
fof(f6914,plain,
! [X2,X0] : multiply(multiply(inverse(inverse(X0)),inverse(X0)),X2) = X2,
inference(superposition,[],[f2784,f6773]) ).
fof(f6929,plain,
! [X2,X0,X1] : inverse(X1) = multiply(multiply(inverse(multiply(inverse(inverse(X0)),inverse(X0))),inverse(X1)),inverse(multiply(inverse(X2),X2))),
inference(superposition,[],[f2462,f6773]) ).
fof(f6934,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(inverse(multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,multiply(inverse(X3),X3))))),multiply(X2,multiply(inverse(inverse(X0)),inverse(X0)))),multiply(inverse(inverse(X0)),inverse(X0)))),inverse(multiply(X4,multiply(multiply(inverse(inverse(X0)),inverse(X0)),multiply(inverse(X3),X3)))))),multiply(inverse(inverse(X0)),inverse(X0))),inverse(multiply(inverse(multiply(multiply(inverse(inverse(X0)),inverse(X0)),multiply(inverse(X3),X3))),multiply(multiply(inverse(inverse(X0)),inverse(X0)),multiply(inverse(X3),X3))))) = X4,
inference(superposition,[],[f27,f6773]) ).
fof(f6935,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(inverse(multiply(X4,inverse(inverse(X3)))),multiply(X4,inverse(inverse(multiply(inverse(X3),X3))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))) = multiply(multiply(inverse(inverse(X0)),inverse(X0)),multiply(multiply(inverse(multiply(X2,inverse(multiply(multiply(inverse(X1),X1),X3)))),multiply(X2,inverse(X3))),inverse(X3))),
inference(superposition,[],[f28,f6773]) ).
fof(f6936,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,multiply(inverse(X3),X3))))),multiply(X2,multiply(inverse(inverse(X0)),inverse(X0)))),multiply(inverse(inverse(X0)),inverse(X0)))) = multiply(multiply(inverse(multiply(X4,inverse(multiply(inverse(inverse(X0)),inverse(X0))))),multiply(X4,inverse(inverse(multiply(multiply(inverse(inverse(X0)),inverse(X0)),multiply(inverse(X3),X3)))))),inverse(multiply(inverse(inverse(multiply(multiply(inverse(inverse(X0)),inverse(X0)),multiply(inverse(X3),X3)))),inverse(multiply(multiply(inverse(inverse(X0)),inverse(X0)),multiply(inverse(X3),X3)))))),
inference(superposition,[],[f28,f6773]) ).
fof(f6960,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,multiply(inverse(inverse(X0)),inverse(X0)))) = multiply(inverse(inverse(X2)),multiply(inverse(inverse(X0)),inverse(X0))),
inference(superposition,[],[f1278,f6773]) ).
fof(f6970,plain,
! [X2,X0,X1] : multiply(inverse(multiply(multiply(inverse(inverse(X0)),inverse(X0)),multiply(inverse(X1),X1))),X2) = X2,
inference(superposition,[],[f2060,f6773]) ).
fof(f7009,plain,
! [X0,X1] : inverse(multiply(inverse(X0),X0)) = multiply(inverse(X1),X1),
inference(superposition,[],[f813,f6773]) ).
fof(f7029,plain,
! [X2,X0] : multiply(inverse(inverse(multiply(inverse(X0),X0))),X2) = X2,
inference(superposition,[],[f2060,f6773]) ).
fof(f7154,plain,
! [X2,X3,X0,X1] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,multiply(inverse(X3),X3))))),multiply(X2,multiply(inverse(inverse(X0)),inverse(X0)))),multiply(inverse(inverse(X0)),inverse(X0)))) = multiply(multiply(inverse(inverse(multiply(inverse(inverse(X0)),inverse(X0)))),inverse(inverse(multiply(multiply(inverse(inverse(X0)),inverse(X0)),multiply(inverse(X3),X3))))),inverse(multiply(inverse(inverse(multiply(multiply(inverse(inverse(X0)),inverse(X0)),multiply(inverse(X3),X3)))),inverse(multiply(multiply(inverse(inverse(X0)),inverse(X0)),multiply(inverse(X3),X3)))))),
inference(forward_demodulation,[],[f6936,f1278]) ).
fof(f7155,plain,
! [X3,X0,X4] : multiply(multiply(inverse(multiply(X4,inverse(inverse(X3)))),multiply(X4,inverse(inverse(multiply(inverse(X3),X3))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))) = multiply(multiply(inverse(inverse(X0)),inverse(X0)),multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(X3))),
inference(forward_demodulation,[],[f6935,f1004]) ).
fof(f7156,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(inverse(multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,multiply(inverse(X3),X3))))),multiply(X2,multiply(inverse(inverse(X0)),inverse(X0)))),multiply(inverse(inverse(X0)),inverse(X0)))),inverse(multiply(X4,multiply(multiply(inverse(inverse(X0)),inverse(X0)),multiply(inverse(X3),X3)))))),multiply(inverse(inverse(X0)),inverse(X0))),inverse(multiply(multiply(inverse(inverse(X0)),inverse(X0)),multiply(inverse(X3),X3)))) = X4,
inference(forward_demodulation,[],[f6934,f6970]) ).
fof(f7159,plain,
! [X2,X1] : inverse(X1) = multiply(inverse(X1),inverse(multiply(inverse(X2),X2))),
inference(forward_demodulation,[],[f6929,f2060]) ).
fof(f7179,plain,
! [X0,X1] : inverse(X1) = multiply(inverse(X1),multiply(inverse(inverse(X0)),inverse(X0))),
inference(forward_demodulation,[],[f6895,f7029]) ).
fof(f7230,plain,
! [X2,X3,X0,X1] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,multiply(inverse(X3),X3))))),multiply(X2,multiply(inverse(inverse(X0)),inverse(X0)))),multiply(inverse(inverse(X0)),inverse(X0)))) = inverse(inverse(multiply(multiply(inverse(inverse(X0)),inverse(X0)),multiply(inverse(X3),X3)))),
inference(forward_demodulation,[],[f7154,f2553]) ).
fof(f7231,plain,
! [X3,X4] : multiply(multiply(inverse(multiply(X4,inverse(inverse(X3)))),multiply(X4,inverse(inverse(multiply(inverse(X3),X3))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))) = multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(X3)),
inference(forward_demodulation,[],[f7155,f6914]) ).
fof(f7232,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(inverse(multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,multiply(inverse(X3),X3))))),multiply(X2,multiply(inverse(inverse(X0)),inverse(X0)))),multiply(inverse(inverse(X0)),inverse(X0)))),inverse(multiply(X4,multiply(inverse(X3),X3))))),multiply(inverse(inverse(X0)),inverse(X0))),inverse(multiply(inverse(X3),X3))) = X4,
inference(forward_demodulation,[],[f7156,f6914]) ).
fof(f7250,plain,
! [X2,X3,X0,X1] : inverse(inverse(multiply(inverse(X3),X3))) = multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,multiply(inverse(X3),X3))))),multiply(X2,multiply(inverse(inverse(X0)),inverse(X0)))),multiply(inverse(inverse(X0)),inverse(X0)))),
inference(forward_demodulation,[],[f7230,f6914]) ).
fof(f7251,plain,
! [X3,X4] : inverse(X3) = multiply(multiply(inverse(multiply(X4,inverse(inverse(X3)))),multiply(X4,inverse(inverse(multiply(inverse(X3),X3))))),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))),
inference(forward_demodulation,[],[f7231,f7029]) ).
fof(f7252,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,multiply(inverse(X3),X3))))),multiply(X2,multiply(inverse(inverse(X0)),inverse(X0)))),multiply(inverse(inverse(X0)),inverse(X0)))),inverse(multiply(X4,multiply(inverse(X3),X3))))),inverse(multiply(inverse(X3),X3))) = X4,
inference(forward_demodulation,[],[f7232,f7179]) ).
fof(f7260,plain,
! [X3,X0,X1] : inverse(inverse(multiply(inverse(X3),X3))) = multiply(inverse(X1),multiply(multiply(inverse(inverse(multiply(X1,multiply(inverse(X3),X3)))),multiply(inverse(inverse(X0)),inverse(X0))),multiply(inverse(inverse(X0)),inverse(X0)))),
inference(forward_demodulation,[],[f7250,f6960]) ).
fof(f7261,plain,
! [X3,X4] : inverse(X3) = multiply(multiply(inverse(multiply(X4,inverse(inverse(X3)))),multiply(X4,inverse(inverse(multiply(inverse(X3),X3))))),inverse(inverse(inverse(multiply(inverse(X3),X3))))),
inference(forward_demodulation,[],[f7251,f7159]) ).
fof(f7262,plain,
! [X2,X3,X0,X1,X4] : inverse(multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,multiply(inverse(X3),X3))))),multiply(X2,multiply(inverse(inverse(X0)),inverse(X0)))),multiply(inverse(inverse(X0)),inverse(X0)))),inverse(multiply(X4,multiply(inverse(X3),X3))))) = X4,
inference(forward_demodulation,[],[f7252,f7159]) ).
fof(f7263,plain,
! [X3,X0,X1] : inverse(inverse(multiply(inverse(X3),X3))) = multiply(inverse(X1),multiply(inverse(inverse(multiply(X1,multiply(inverse(X3),X3)))),multiply(inverse(inverse(X0)),inverse(X0)))),
inference(forward_demodulation,[],[f7260,f7179]) ).
fof(f7264,plain,
! [X3] : inverse(X3) = multiply(multiply(inverse(inverse(inverse(X3))),inverse(inverse(multiply(inverse(X3),X3)))),inverse(inverse(inverse(multiply(inverse(X3),X3))))),
inference(forward_demodulation,[],[f7261,f1278]) ).
fof(f7265,plain,
! [X3,X0,X1,X4] : inverse(multiply(multiply(inverse(X1),multiply(multiply(inverse(inverse(multiply(X1,multiply(inverse(X3),X3)))),multiply(inverse(inverse(X0)),inverse(X0))),multiply(inverse(inverse(X0)),inverse(X0)))),inverse(multiply(X4,multiply(inverse(X3),X3))))) = X4,
inference(forward_demodulation,[],[f7262,f6960]) ).
fof(f7266,plain,
! [X3,X1] : inverse(inverse(multiply(inverse(X3),X3))) = multiply(inverse(X1),inverse(inverse(multiply(X1,multiply(inverse(X3),X3))))),
inference(forward_demodulation,[],[f7263,f7179]) ).
fof(f7267,plain,
! [X3,X0,X1,X4] : inverse(multiply(multiply(inverse(X1),multiply(inverse(inverse(multiply(X1,multiply(inverse(X3),X3)))),multiply(inverse(inverse(X0)),inverse(X0)))),inverse(multiply(X4,multiply(inverse(X3),X3))))) = X4,
inference(forward_demodulation,[],[f7265,f7179]) ).
fof(f7268,plain,
! [X3,X1,X4] : inverse(multiply(multiply(inverse(X1),inverse(inverse(multiply(X1,multiply(inverse(X3),X3))))),inverse(multiply(X4,multiply(inverse(X3),X3))))) = X4,
inference(forward_demodulation,[],[f7267,f7179]) ).
fof(f7269,plain,
! [X3,X4] : inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(X4,multiply(inverse(X3),X3))))) = X4,
inference(forward_demodulation,[],[f7268,f7266]) ).
fof(f7270,plain,
! [X3,X4] : inverse(inverse(multiply(X4,multiply(inverse(X3),X3)))) = X4,
inference(forward_demodulation,[],[f7269,f7029]) ).
fof(f7498,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(inverse(multiply(inverse(X0),X0))),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(multiply(inverse(multiply(X2,inverse(multiply(X3,X0)))),multiply(X2,inverse(X0))),inverse(multiply(X1,multiply(inverse(X0),X0))))),X3),inverse(multiply(inverse(X0),X0)))),inverse(X4))) = multiply(inverse(inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))),inverse(X4)),
inference(superposition,[],[f1278,f24]) ).
fof(f7507,plain,
! [X2,X3,X0,X1,X4] : inverse(X4) = multiply(inverse(inverse(multiply(inverse(X0),X0))),multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(multiply(inverse(multiply(X2,inverse(multiply(X3,X0)))),multiply(X2,inverse(X0))),inverse(multiply(X1,multiply(inverse(X0),X0))))),X3),inverse(multiply(inverse(X0),X0)))),inverse(X4))),
inference(forward_demodulation,[],[f7498,f7029]) ).
fof(f7734,plain,
! [X2,X3,X0,X1,X4] : inverse(X4) = multiply(multiply(inverse(X1),multiply(multiply(inverse(multiply(multiply(inverse(multiply(X2,inverse(multiply(X3,X0)))),multiply(X2,inverse(X0))),inverse(multiply(X1,multiply(inverse(X0),X0))))),X3),inverse(multiply(inverse(X0),X0)))),inverse(X4)),
inference(forward_demodulation,[],[f7507,f7029]) ).
fof(f7944,plain,
! [X1,X4] : inverse(X4) = multiply(multiply(inverse(X1),X1),inverse(X4)),
inference(forward_demodulation,[],[f7734,f990]) ).
fof(f8403,plain,
! [X2,X3,X0,X1] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X0)))),multiply(X2,inverse(X0))),inverse(X0))) = multiply(multiply(inverse(multiply(multiply(inverse(X3),X3),inverse(inverse(X0)))),inverse(inverse(multiply(inverse(X0),X0)))),inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0))))),
inference(superposition,[],[f28,f7944]) ).
fof(f8414,plain,
! [X2,X3,X0,X1] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X0)))),multiply(X2,inverse(X0))),inverse(X0))) = multiply(multiply(inverse(multiply(multiply(inverse(X3),X3),inverse(inverse(X0)))),inverse(inverse(multiply(inverse(X0),X0)))),inverse(inverse(inverse(multiply(inverse(X0),X0))))),
inference(forward_demodulation,[],[f8403,f7159]) ).
fof(f8465,plain,
! [X2,X0,X1] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X0)))),multiply(X2,inverse(X0))),inverse(X0))) = multiply(multiply(inverse(inverse(inverse(X0))),inverse(inverse(multiply(inverse(X0),X0)))),inverse(inverse(inverse(multiply(inverse(X0),X0))))),
inference(forward_demodulation,[],[f8414,f7944]) ).
fof(f8484,plain,
! [X2,X0,X1] : inverse(X0) = multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X0)))),multiply(X2,inverse(X0))),inverse(X0))),
inference(forward_demodulation,[],[f8465,f7264]) ).
fof(f8491,plain,
! [X0,X1] : inverse(X0) = multiply(inverse(X1),multiply(multiply(inverse(inverse(multiply(X1,X0))),inverse(X0)),inverse(X0))),
inference(forward_demodulation,[],[f8484,f1278]) ).
fof(f8516,plain,
! [X2,X0] : multiply(multiply(inverse(X0),X0),X2) = X2,
inference(superposition,[],[f6914,f813]) ).
fof(f8888,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X3)))),multiply(X2,inverse(X3))),inverse(X3))) = multiply(multiply(inverse(multiply(X4,inverse(inverse(X3)))),multiply(X4,inverse(multiply(inverse(X0),X0)))),inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X0),X0)))),
inference(superposition,[],[f28,f7009]) ).
fof(f8909,plain,
! [X2,X0,X1] : inverse(X1) = multiply(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(X1)),multiply(inverse(X0),X0)),
inference(superposition,[],[f2553,f7009]) ).
fof(f9273,plain,
! [X0,X1] : inverse(X1) = multiply(inverse(X1),multiply(inverse(X0),X0)),
inference(forward_demodulation,[],[f8909,f7029]) ).
fof(f9286,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X3)))),multiply(X2,inverse(X3))),inverse(X3))) = multiply(multiply(inverse(multiply(X4,inverse(inverse(X3)))),multiply(X4,inverse(multiply(inverse(X0),X0)))),inverse(multiply(inverse(X0),X0))),
inference(forward_demodulation,[],[f8888,f2060]) ).
fof(f9395,plain,
! [X2,X3,X0,X1] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X3)))),multiply(X2,inverse(X3))),inverse(X3))) = multiply(multiply(inverse(inverse(inverse(X3))),inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X0),X0))),
inference(forward_demodulation,[],[f9286,f1278]) ).
fof(f9435,plain,
! [X2,X3,X0,X1] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X3)))),multiply(X2,inverse(X3))),inverse(X3))) = multiply(inverse(inverse(inverse(X3))),inverse(multiply(inverse(X0),X0))),
inference(forward_demodulation,[],[f9395,f7159]) ).
fof(f9450,plain,
! [X2,X3,X1] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X3)))),multiply(X2,inverse(X3))),inverse(X3))) = inverse(inverse(inverse(X3))),
inference(forward_demodulation,[],[f9435,f7159]) ).
fof(f9456,plain,
! [X3,X1] : multiply(inverse(X1),multiply(multiply(inverse(inverse(multiply(X1,X3))),inverse(X3)),inverse(X3))) = inverse(inverse(inverse(X3))),
inference(forward_demodulation,[],[f9450,f1278]) ).
fof(f9459,plain,
! [X3] : inverse(X3) = inverse(inverse(inverse(X3))),
inference(forward_demodulation,[],[f9456,f8491]) ).
fof(f10004,plain,
! [X2,X0,X1] : inverse(inverse(multiply(X1,multiply(X0,inverse(multiply(X0,multiply(inverse(X2),X2))))))) = X1,
inference(superposition,[],[f7270,f7270]) ).
fof(f10008,plain,
! [X2,X0,X1] : inverse(inverse(multiply(X2,multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X1),X1))))) = X2,
inference(superposition,[],[f7270,f1192]) ).
fof(f10027,plain,
! [X2,X0,X1] : inverse(multiply(inverse(inverse(X2)),inverse(X1))) = inverse(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X2))))),
inference(superposition,[],[f7270,f227]) ).
fof(f10064,plain,
! [X0,X1] : inverse(X0) = inverse(multiply(X0,multiply(inverse(X1),X1))),
inference(superposition,[],[f9459,f7270]) ).
fof(f10065,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,multiply(X0,multiply(inverse(X3),X3)))))),multiply(X2,inverse(multiply(X0,multiply(inverse(X3),X3))))),inverse(multiply(X0,multiply(inverse(X3),X3))))) = multiply(multiply(inverse(multiply(X4,X0)),multiply(X4,inverse(inverse(multiply(inverse(multiply(X0,multiply(inverse(X3),X3))),multiply(X0,multiply(inverse(X3),X3))))))),inverse(multiply(inverse(inverse(multiply(inverse(multiply(X0,multiply(inverse(X3),X3))),multiply(X0,multiply(inverse(X3),X3))))),inverse(multiply(inverse(multiply(X0,multiply(inverse(X3),X3))),multiply(X0,multiply(inverse(X3),X3))))))),
inference(superposition,[],[f28,f7270]) ).
fof(f10072,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(multiply(X0,multiply(inverse(X3),X3))))))),multiply(X2,X0)),X0)) = multiply(multiply(inverse(multiply(X4,inverse(X0))),multiply(X4,inverse(inverse(multiply(X0,inverse(multiply(X0,multiply(inverse(X3),X3)))))))),inverse(multiply(inverse(inverse(multiply(X0,inverse(multiply(X0,multiply(inverse(X3),X3)))))),inverse(multiply(X0,inverse(multiply(X0,multiply(inverse(X3),X3)))))))),
inference(superposition,[],[f28,f7270]) ).
fof(f10095,plain,
! [X3,X0,X1] : multiply(inverse(multiply(X1,X0)),multiply(X1,inverse(X3))) = multiply(inverse(X0),inverse(X3)),
inference(superposition,[],[f1278,f7270]) ).
fof(f10096,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,X0)) = multiply(inverse(inverse(X2)),X0),
inference(superposition,[],[f1278,f7270]) ).
fof(f10097,plain,
! [X2,X3,X0] : multiply(inverse(X0),inverse(X2)) = multiply(inverse(multiply(inverse(inverse(X2)),X0)),multiply(inverse(X3),X3)),
inference(superposition,[],[f1526,f7270]) ).
fof(f10098,plain,
! [X3,X0,X1] : multiply(inverse(inverse(X1)),X0) = multiply(inverse(multiply(inverse(X0),inverse(X1))),multiply(inverse(X3),X3)),
inference(superposition,[],[f1526,f7270]) ).
fof(f10108,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(inverse(multiply(X1,inverse(multiply(X0,multiply(inverse(X2),X2)))))),X0),inverse(multiply(inverse(X3),X3))) = X1,
inference(superposition,[],[f2462,f7270]) ).
fof(f10113,plain,
! [X2,X3,X0] : multiply(multiply(inverse(inverse(multiply(inverse(X2),X2))),X0),inverse(multiply(inverse(X3),X3))) = X0,
inference(superposition,[],[f2553,f7270]) ).
fof(f10119,plain,
! [X2,X3,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X3),X3)))) = inverse(multiply(X0,inverse(multiply(X0,multiply(inverse(X1),X1))))),
inference(superposition,[],[f2768,f7270]) ).
fof(f10135,plain,
! [X2,X0,X1] : multiply(multiply(X0,inverse(multiply(X0,multiply(inverse(X1),X1)))),X2) = X2,
inference(superposition,[],[f8516,f7270]) ).
fof(f10136,plain,
! [X0] : inverse(inverse(X0)) = X0,
inference(superposition,[],[f9459,f7270]) ).
fof(f10150,plain,
! [X2,X0,X1] : inverse(inverse(inverse(multiply(inverse(X2),X2)))) = inverse(multiply(X0,inverse(multiply(X0,multiply(inverse(X1),X1))))),
inference(forward_demodulation,[],[f10119,f7159]) ).
fof(f10156,plain,
! [X3,X0] : multiply(X0,inverse(multiply(inverse(X3),X3))) = X0,
inference(forward_demodulation,[],[f10113,f7029]) ).
fof(f10157,plain,
! [X2,X3,X0,X1] : multiply(multiply(multiply(X1,inverse(multiply(X0,multiply(inverse(X2),X2)))),X0),inverse(multiply(inverse(X3),X3))) = X1,
inference(forward_demodulation,[],[f10108,f10136]) ).
fof(f10166,plain,
! [X0,X1] : inverse(multiply(inverse(X0),inverse(X1))) = multiply(inverse(inverse(X1)),X0),
inference(forward_demodulation,[],[f10098,f9273]) ).
fof(f10167,plain,
! [X2,X0] : multiply(inverse(X0),inverse(X2)) = inverse(multiply(inverse(inverse(X2)),X0)),
inference(forward_demodulation,[],[f10097,f9273]) ).
fof(f10168,plain,
! [X2,X0,X1] : multiply(X2,X0) = multiply(inverse(multiply(X1,inverse(X2))),multiply(X1,X0)),
inference(forward_demodulation,[],[f10096,f10136]) ).
fof(f10182,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(multiply(X0,multiply(inverse(X3),X3))))))),multiply(X2,X0)),X0)) = multiply(multiply(inverse(multiply(X4,inverse(X0))),multiply(X4,multiply(X0,inverse(multiply(X0,multiply(inverse(X3),X3)))))),inverse(multiply(multiply(X0,inverse(multiply(X0,multiply(inverse(X3),X3)))),inverse(multiply(X0,inverse(multiply(X0,multiply(inverse(X3),X3)))))))),
inference(forward_demodulation,[],[f10072,f10136]) ).
fof(f10189,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,multiply(X0,multiply(inverse(X3),X3)))))),multiply(X2,inverse(multiply(X0,multiply(inverse(X3),X3))))),inverse(multiply(X0,multiply(inverse(X3),X3))))) = multiply(multiply(inverse(multiply(X4,X0)),multiply(X4,inverse(inverse(multiply(inverse(multiply(X0,multiply(inverse(X3),X3))),multiply(X0,multiply(inverse(X3),X3))))))),inverse(inverse(inverse(multiply(inverse(multiply(X0,multiply(inverse(X3),X3))),multiply(X0,multiply(inverse(X3),X3))))))),
inference(forward_demodulation,[],[f10065,f7159]) ).
fof(f10208,plain,
! [X2,X0,X1] : multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X2))) = inverse(multiply(inverse(inverse(X2)),inverse(X1))),
inference(forward_demodulation,[],[f10027,f10136]) ).
fof(f10218,plain,
! [X2,X0,X1] : multiply(X2,multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X1),X1))) = X2,
inference(forward_demodulation,[],[f10008,f10136]) ).
fof(f10222,plain,
! [X2,X0,X1] : multiply(X1,multiply(X0,inverse(multiply(X0,multiply(inverse(X2),X2))))) = X1,
inference(forward_demodulation,[],[f10004,f10136]) ).
fof(f10248,plain,
! [X2,X0] : inverse(inverse(inverse(multiply(inverse(X2),X2)))) = inverse(multiply(X0,inverse(X0))),
inference(forward_demodulation,[],[f10150,f10064]) ).
fof(f10253,plain,
! [X2,X0,X1] : multiply(multiply(X1,inverse(multiply(X0,multiply(inverse(X2),X2)))),X0) = X1,
inference(forward_demodulation,[],[f10157,f10156]) ).
fof(f10258,plain,
! [X0,X1] : multiply(X1,X0) = inverse(multiply(inverse(X0),inverse(X1))),
inference(forward_demodulation,[],[f10166,f10136]) ).
fof(f10259,plain,
! [X2,X0] : inverse(multiply(X2,X0)) = multiply(inverse(X0),inverse(X2)),
inference(forward_demodulation,[],[f10167,f10136]) ).
fof(f10264,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(multiply(X0,multiply(inverse(X3),X3))))))),multiply(X2,X0)),X0)) = multiply(multiply(inverse(multiply(X4,inverse(X0))),multiply(X4,multiply(X0,inverse(multiply(X0,multiply(inverse(X3),X3)))))),inverse(inverse(multiply(X0,inverse(multiply(X0,multiply(inverse(X3),X3))))))),
inference(forward_demodulation,[],[f10182,f10135]) ).
fof(f10271,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,multiply(X0,multiply(inverse(X3),X3)))))),multiply(X2,inverse(multiply(X0,multiply(inverse(X3),X3))))),inverse(multiply(X0,multiply(inverse(X3),X3))))) = multiply(multiply(inverse(multiply(X4,X0)),multiply(X4,inverse(inverse(multiply(inverse(multiply(X0,multiply(inverse(X3),X3))),multiply(X0,multiply(inverse(X3),X3))))))),inverse(multiply(inverse(multiply(X0,multiply(inverse(X3),X3))),multiply(X0,multiply(inverse(X3),X3))))),
inference(forward_demodulation,[],[f10189,f10136]) ).
fof(f10275,plain,
! [X2,X0,X1] : inverse(multiply(X2,inverse(X1))) = multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,inverse(X2))),
inference(forward_demodulation,[],[f10208,f10136]) ).
fof(f10284,plain,
! [X2,X1] : multiply(X2,multiply(inverse(X1),X1)) = X2,
inference(forward_demodulation,[],[f10218,f2060]) ).
fof(f10287,plain,
! [X0,X1] : multiply(X1,multiply(X0,inverse(X0))) = X1,
inference(forward_demodulation,[],[f10222,f10064]) ).
fof(f10307,plain,
! [X2,X0] : inverse(multiply(inverse(X2),X2)) = inverse(multiply(X0,inverse(X0))),
inference(forward_demodulation,[],[f10248,f10136]) ).
fof(f10309,plain,
! [X0,X1] : multiply(multiply(X1,inverse(X0)),X0) = X1,
inference(forward_demodulation,[],[f10253,f10064]) ).
fof(f10315,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(multiply(X0,multiply(inverse(X3),X3))))))),multiply(X2,X0)),X0)) = multiply(multiply(inverse(multiply(X4,inverse(X0))),multiply(X4,multiply(X0,inverse(multiply(X0,multiply(inverse(X3),X3)))))),multiply(X0,inverse(multiply(X0,multiply(inverse(X3),X3))))),
inference(forward_demodulation,[],[f10264,f10136]) ).
fof(f10321,plain,
! [X2,X3,X0,X1,X4] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,multiply(X0,multiply(inverse(X3),X3)))))),multiply(X2,inverse(multiply(X0,multiply(inverse(X3),X3))))),inverse(multiply(X0,multiply(inverse(X3),X3))))) = multiply(inverse(multiply(X4,X0)),multiply(X4,inverse(inverse(multiply(inverse(multiply(X0,multiply(inverse(X3),X3))),multiply(X0,multiply(inverse(X3),X3))))))),
inference(forward_demodulation,[],[f10271,f10156]) ).
fof(f10324,plain,
! [X2,X1] : multiply(X1,inverse(X2)) = inverse(multiply(X2,inverse(X1))),
inference(forward_demodulation,[],[f10275,f10168]) ).
fof(f10340,plain,
! [X2,X0,X1,X4] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(X0))))),multiply(X2,X0)),X0)) = multiply(multiply(inverse(multiply(X4,inverse(X0))),multiply(X4,multiply(X0,inverse(X0)))),multiply(X0,inverse(X0))),
inference(forward_demodulation,[],[f10315,f10064]) ).
fof(f10345,plain,
! [X2,X3,X0,X1] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,multiply(X0,multiply(inverse(X3),X3)))))),multiply(X2,inverse(multiply(X0,multiply(inverse(X3),X3))))),inverse(multiply(X0,multiply(inverse(X3),X3))))) = multiply(inverse(X0),inverse(inverse(multiply(inverse(multiply(X0,multiply(inverse(X3),X3))),multiply(X0,multiply(inverse(X3),X3)))))),
inference(forward_demodulation,[],[f10321,f10095]) ).
fof(f10351,plain,
! [X2,X0,X1,X4] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(X0))))),multiply(X2,X0)),X0)) = multiply(inverse(multiply(X4,inverse(X0))),multiply(X4,multiply(X0,inverse(X0)))),
inference(forward_demodulation,[],[f10340,f10287]) ).
fof(f10356,plain,
! [X2,X3,X0,X1] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,multiply(X0,multiply(inverse(X3),X3)))))),multiply(X2,inverse(multiply(X0,multiply(inverse(X3),X3))))),inverse(multiply(X0,multiply(inverse(X3),X3))))) = inverse(multiply(inverse(multiply(inverse(multiply(X0,multiply(inverse(X3),X3))),multiply(X0,multiply(inverse(X3),X3)))),X0)),
inference(forward_demodulation,[],[f10345,f10259]) ).
fof(f10360,plain,
! [X2,X0,X1] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(X0))))),multiply(X2,X0)),X0)) = multiply(X0,multiply(X0,inverse(X0))),
inference(forward_demodulation,[],[f10351,f10168]) ).
fof(f10365,plain,
! [X2,X3,X0,X1] : inverse(X0) = multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,multiply(X0,multiply(inverse(X3),X3)))))),multiply(X2,inverse(multiply(X0,multiply(inverse(X3),X3))))),inverse(multiply(X0,multiply(inverse(X3),X3))))),
inference(forward_demodulation,[],[f10356,f2060]) ).
fof(f10367,plain,
! [X2,X0,X1] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,inverse(X0))))),multiply(X2,X0)),X0)) = X0,
inference(forward_demodulation,[],[f10360,f10287]) ).
fof(f10371,plain,
! [X2,X3,X0,X1] : inverse(X0) = multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,multiply(X0,multiply(inverse(X3),X3)))))),multiply(X2,inverse(X0))),inverse(X0))),
inference(forward_demodulation,[],[f10365,f10064]) ).
fof(f10372,plain,
! [X0,X1] : multiply(inverse(X1),multiply(multiply(multiply(X1,inverse(X0)),X0),X0)) = X0,
inference(forward_demodulation,[],[f10367,f10168]) ).
fof(f10375,plain,
! [X3,X0,X1] : inverse(X0) = multiply(inverse(X1),multiply(multiply(multiply(X1,multiply(X0,multiply(inverse(X3),X3))),inverse(X0)),inverse(X0))),
inference(forward_demodulation,[],[f10371,f10168]) ).
fof(f10376,plain,
! [X0,X1] : multiply(inverse(X1),multiply(X1,X0)) = X0,
inference(forward_demodulation,[],[f10372,f10309]) ).
fof(f10378,plain,
! [X0,X1] : inverse(X0) = multiply(inverse(X1),multiply(multiply(multiply(X1,X0),inverse(X0)),inverse(X0))),
inference(forward_demodulation,[],[f10375,f10284]) ).
fof(f10402,plain,
! [X2,X0,X1] : multiply(multiply(multiply(X0,X1),inverse(X1)),inverse(multiply(inverse(X2),X2))) = X0,
inference(superposition,[],[f2462,f10136]) ).
fof(f10549,plain,
! [X0,X1] : multiply(multiply(X0,X1),inverse(X1)) = X0,
inference(forward_demodulation,[],[f10402,f10156]) ).
fof(f14624,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(multiply(X0,inverse(inverse(X1))),inverse(multiply(multiply(X2,inverse(multiply(inverse(X3),X3))),X1)))),X0) = X2,
inference(superposition,[],[f976,f10309]) ).
fof(f14640,plain,
! [X2,X3,X0,X1] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X3)))),multiply(X2,inverse(X3))),inverse(X3))) = multiply(multiply(inverse(multiply(multiply(X0,inverse(inverse(inverse(multiply(inverse(X3),X3))))),inverse(inverse(X3)))),X0),inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),inverse(multiply(inverse(X3),X3))))),
inference(superposition,[],[f28,f10309]) ).
fof(f14662,plain,
! [X2,X3,X0,X1] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X3)))),multiply(X2,inverse(X3))),inverse(X3))) = multiply(inverse(multiply(multiply(X0,inverse(inverse(inverse(multiply(inverse(X3),X3))))),inverse(inverse(X3)))),X0),
inference(forward_demodulation,[],[f14640,f10156]) ).
fof(f14678,plain,
! [X2,X3,X0,X1] : multiply(multiply(multiply(multiply(X2,inverse(multiply(inverse(X3),X3))),X1),inverse(multiply(X0,inverse(inverse(X1))))),X0) = X2,
inference(forward_demodulation,[],[f14624,f10324]) ).
fof(f14744,plain,
! [X2,X3,X0,X1] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X3)))),multiply(X2,inverse(X3))),inverse(X3))) = multiply(multiply(inverse(X3),inverse(multiply(X0,inverse(inverse(inverse(multiply(inverse(X3),X3))))))),X0),
inference(forward_demodulation,[],[f14662,f10324]) ).
fof(f14760,plain,
! [X2,X3,X0,X1] : multiply(multiply(multiply(multiply(X2,inverse(multiply(inverse(X3),X3))),X1),multiply(inverse(X1),inverse(X0))),X0) = X2,
inference(forward_demodulation,[],[f14678,f10324]) ).
fof(f14803,plain,
! [X2,X3,X0,X1] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X3)))),multiply(X2,inverse(X3))),inverse(X3))) = multiply(inverse(multiply(multiply(X0,inverse(inverse(inverse(multiply(inverse(X3),X3))))),X3)),X0),
inference(forward_demodulation,[],[f14744,f10259]) ).
fof(f14814,plain,
! [X2,X3,X0,X1] : multiply(multiply(multiply(multiply(X2,inverse(multiply(inverse(X3),X3))),X1),inverse(multiply(X0,X1))),X0) = X2,
inference(forward_demodulation,[],[f14760,f10259]) ).
fof(f14843,plain,
! [X2,X3,X0,X1] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X3)))),multiply(X2,inverse(X3))),inverse(X3))) = multiply(inverse(multiply(multiply(X0,inverse(multiply(inverse(X3),X3))),X3)),X0),
inference(forward_demodulation,[],[f14803,f10136]) ).
fof(f14851,plain,
! [X2,X0,X1] : multiply(multiply(multiply(X2,X1),inverse(multiply(X0,X1))),X0) = X2,
inference(forward_demodulation,[],[f14814,f10156]) ).
fof(f14873,plain,
! [X2,X3,X0,X1] : multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(X1,X3)))),multiply(X2,inverse(X3))),inverse(X3))) = multiply(inverse(multiply(X0,X3)),X0),
inference(forward_demodulation,[],[f14843,f10156]) ).
fof(f14896,plain,
! [X3,X0,X1] : multiply(inverse(X1),multiply(multiply(multiply(X1,X3),inverse(X3)),inverse(X3))) = multiply(inverse(multiply(X0,X3)),X0),
inference(forward_demodulation,[],[f14873,f10168]) ).
fof(f14915,plain,
! [X3,X0] : inverse(X3) = multiply(inverse(multiply(X0,X3)),X0),
inference(forward_demodulation,[],[f14896,f10378]) ).
fof(f14956,plain,
! [X0,X1] : multiply(X0,multiply(inverse(X0),X1)) = X1,
inference(superposition,[],[f10376,f10136]) ).
fof(f15471,plain,
! [X2,X3,X0,X1] : inverse(multiply(X1,inverse(multiply(multiply(X0,inverse(multiply(inverse(X2),X2))),X3)))) = multiply(X0,inverse(multiply(X1,inverse(X3)))),
inference(superposition,[],[f10549,f976]) ).
fof(f15632,plain,
! [X2,X3,X0,X1] : inverse(multiply(X1,inverse(multiply(multiply(X0,inverse(multiply(inverse(X2),X2))),X3)))) = multiply(X0,multiply(X3,inverse(X1))),
inference(forward_demodulation,[],[f15471,f10324]) ).
fof(f15695,plain,
! [X2,X3,X0,X1] : multiply(X0,multiply(X3,inverse(X1))) = multiply(multiply(multiply(X0,inverse(multiply(inverse(X2),X2))),X3),inverse(X1)),
inference(forward_demodulation,[],[f15632,f10324]) ).
fof(f15734,plain,
! [X3,X0,X1] : multiply(X0,multiply(X3,inverse(X1))) = multiply(multiply(X0,X3),inverse(X1)),
inference(forward_demodulation,[],[f15695,f10156]) ).
fof(f26013,plain,
! [X0,X1] : inverse(multiply(inverse(X1),X0)) = multiply(inverse(X0),X1),
inference(superposition,[],[f10309,f14915]) ).
fof(f27813,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(X0,inverse(multiply(multiply(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(X3))),inverse(multiply(inverse(X3),X3))),X3))),X4) = inverse(multiply(inverse(X4),inverse(multiply(X0,inverse(X1))))),
inference(superposition,[],[f10258,f358]) ).
fof(f28211,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(X0,inverse(multiply(multiply(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(X3))),inverse(multiply(inverse(X3),X3))),X3))),X4) = multiply(multiply(X0,inverse(X1)),inverse(inverse(X4))),
inference(forward_demodulation,[],[f27813,f10324]) ).
fof(f28371,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(X0,inverse(multiply(multiply(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(X3))),inverse(multiply(inverse(X3),X3))),X3))),X4) = multiply(X0,multiply(inverse(X1),inverse(inverse(X4)))),
inference(forward_demodulation,[],[f28211,f15734]) ).
fof(f28500,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(X0,inverse(multiply(multiply(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(X3))),inverse(multiply(inverse(X3),X3))),X3))),X4) = multiply(X0,inverse(multiply(inverse(X4),X1))),
inference(forward_demodulation,[],[f28371,f10259]) ).
fof(f28595,plain,
! [X2,X3,X0,X1,X4] : multiply(multiply(X0,inverse(multiply(multiply(multiply(inverse(multiply(X2,inverse(X1))),multiply(X2,inverse(X3))),inverse(multiply(inverse(X3),X3))),X3))),X4) = multiply(X0,multiply(inverse(X1),X4)),
inference(forward_demodulation,[],[f28500,f26013]) ).
fof(f28671,plain,
! [X0,X1,X4] : multiply(multiply(X0,inverse(X1)),X4) = multiply(X0,multiply(inverse(X1),X4)),
inference(forward_demodulation,[],[f28595,f458]) ).
fof(f29164,plain,
! [X2,X0,X1] : multiply(inverse(X2),multiply(X0,X1)) = inverse(multiply(multiply(inverse(X1),inverse(X0)),X2)),
inference(superposition,[],[f10259,f10258]) ).
fof(f29459,plain,
! [X2,X0,X1] : multiply(inverse(X2),multiply(X0,X1)) = inverse(multiply(inverse(X1),multiply(inverse(X0),X2))),
inference(forward_demodulation,[],[f29164,f28671]) ).
fof(f29598,plain,
! [X2,X0,X1] : multiply(inverse(X2),multiply(X0,X1)) = multiply(inverse(multiply(inverse(X0),X2)),X1),
inference(forward_demodulation,[],[f29459,f26013]) ).
fof(f29701,plain,
! [X2,X0,X1] : multiply(inverse(X2),multiply(X0,X1)) = multiply(multiply(inverse(X2),X0),X1),
inference(forward_demodulation,[],[f29598,f26013]) ).
fof(f30248,plain,
! [X2,X0,X1] : inverse(multiply(X2,multiply(X0,X1))) = multiply(multiply(inverse(X1),inverse(X0)),inverse(X2)),
inference(superposition,[],[f10324,f10258]) ).
fof(f30462,plain,
! [X2,X0,X1] : inverse(multiply(multiply(X1,inverse(X0)),X2)) = multiply(inverse(X2),multiply(X0,inverse(X1))),
inference(superposition,[],[f10259,f10324]) ).
fof(f30463,plain,
! [X2,X0,X1] : multiply(multiply(X0,inverse(X1)),inverse(X2)) = inverse(multiply(X2,multiply(X1,inverse(X0)))),
inference(superposition,[],[f10259,f10324]) ).
fof(f30478,plain,
! [X2,X0,X1] : inverse(multiply(X2,multiply(X1,inverse(X0)))) = multiply(X0,multiply(inverse(X1),inverse(X2))),
inference(forward_demodulation,[],[f30463,f28671]) ).
fof(f30479,plain,
! [X2,X0,X1] : multiply(inverse(X2),multiply(X0,inverse(X1))) = inverse(multiply(X1,multiply(inverse(X0),X2))),
inference(forward_demodulation,[],[f30462,f28671]) ).
fof(f30672,plain,
! [X2,X0,X1] : inverse(multiply(X2,multiply(X0,X1))) = multiply(inverse(X1),multiply(inverse(X0),inverse(X2))),
inference(forward_demodulation,[],[f30248,f29701]) ).
fof(f30686,plain,
! [X2,X0,X1] : multiply(X0,inverse(multiply(X2,X1))) = inverse(multiply(X2,multiply(X1,inverse(X0)))),
inference(forward_demodulation,[],[f30478,f10259]) ).
fof(f30846,plain,
! [X2,X0,X1] : inverse(multiply(X2,multiply(X0,X1))) = multiply(inverse(X1),inverse(multiply(X2,X0))),
inference(forward_demodulation,[],[f30672,f10259]) ).
fof(f30982,plain,
! [X2,X0,X1] : inverse(multiply(X2,multiply(X0,X1))) = inverse(multiply(multiply(X2,X0),X1)),
inference(forward_demodulation,[],[f30846,f10259]) ).
fof(f44701,plain,
! [X2,X0,X1] : inverse(multiply(multiply(inverse(X1),X0),X2)) = multiply(inverse(X2),multiply(inverse(X0),X1)),
inference(superposition,[],[f10259,f26013]) ).
fof(f44730,plain,
! [X2,X0,X1] : multiply(inverse(X2),multiply(inverse(X0),X1)) = inverse(multiply(inverse(X1),multiply(X0,X2))),
inference(forward_demodulation,[],[f44701,f30982]) ).
fof(f44948,plain,
! [X2,X0,X1] : multiply(inverse(X2),multiply(inverse(X0),X1)) = multiply(inverse(multiply(X0,X2)),X1),
inference(forward_demodulation,[],[f44730,f26013]) ).
fof(f50504,plain,
! [X2,X3,X0,X1] : multiply(multiply(multiply(inverse(multiply(X0,inverse(X0))),multiply(inverse(X1),X1)),inverse(multiply(inverse(X2),X2))),X3) = X3,
inference(superposition,[],[f1218,f10307]) ).
fof(f50594,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(X3,inverse(inverse(inverse(X1))))),multiply(X3,inverse(inverse(multiply(inverse(inverse(X1)),inverse(X1)))))),inverse(multiply(inverse(inverse(multiply(inverse(inverse(X1)),inverse(X1)))),inverse(multiply(inverse(inverse(X1)),inverse(X1)))))) = multiply(inverse(X1),multiply(multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),X0)))),multiply(X2,inverse(inverse(X1)))),inverse(inverse(X1)))),
inference(superposition,[],[f28,f10307]) ).
fof(f50809,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(X3,inverse(inverse(inverse(X1))))),multiply(X3,inverse(inverse(multiply(inverse(inverse(X1)),inverse(X1)))))),inverse(multiply(inverse(inverse(multiply(inverse(inverse(X1)),inverse(X1)))),inverse(multiply(inverse(inverse(X1)),inverse(X1)))))) = multiply(inverse(X1),multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),X0)))),multiply(multiply(X2,inverse(inverse(X1))),inverse(inverse(X1))))),
inference(forward_demodulation,[],[f50594,f29701]) ).
fof(f50892,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(X0,inverse(X0))),multiply(inverse(X1),X1)),multiply(inverse(multiply(inverse(X2),X2)),X3)) = X3,
inference(forward_demodulation,[],[f50504,f28671]) ).
fof(f51197,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(X3,inverse(inverse(inverse(X1))))),multiply(X3,inverse(inverse(multiply(inverse(inverse(X1)),inverse(X1)))))),inverse(multiply(inverse(inverse(multiply(inverse(inverse(X1)),inverse(X1)))),inverse(multiply(inverse(inverse(X1)),inverse(X1)))))) = multiply(inverse(multiply(multiply(X2,inverse(multiply(inverse(X0),X0))),X1)),multiply(multiply(X2,inverse(inverse(X1))),inverse(inverse(X1)))),
inference(forward_demodulation,[],[f50809,f44948]) ).
fof(f51276,plain,
! [X2,X3,X0,X1] : multiply(inverse(multiply(X0,inverse(X0))),multiply(multiply(inverse(X1),X1),multiply(inverse(multiply(inverse(X2),X2)),X3))) = X3,
inference(forward_demodulation,[],[f50892,f29701]) ).
fof(f51522,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(X3,inverse(inverse(inverse(X1))))),multiply(X3,inverse(inverse(multiply(inverse(inverse(X1)),inverse(X1)))))),inverse(multiply(inverse(inverse(multiply(inverse(inverse(X1)),inverse(X1)))),inverse(multiply(inverse(inverse(X1)),inverse(X1)))))) = multiply(inverse(multiply(multiply(X2,inverse(multiply(inverse(X0),X0))),X1)),multiply(X2,multiply(inverse(inverse(X1)),inverse(inverse(X1))))),
inference(forward_demodulation,[],[f51197,f28671]) ).
fof(f51585,plain,
! [X2,X3,X0] : multiply(inverse(multiply(X0,inverse(X0))),multiply(inverse(multiply(inverse(X2),X2)),X3)) = X3,
inference(forward_demodulation,[],[f51276,f8516]) ).
fof(f51777,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(X3,inverse(inverse(inverse(X1))))),multiply(X3,inverse(inverse(multiply(inverse(inverse(X1)),inverse(X1)))))),inverse(multiply(inverse(inverse(multiply(inverse(inverse(X1)),inverse(X1)))),inverse(multiply(inverse(inverse(X1)),inverse(X1)))))) = multiply(inverse(multiply(multiply(X2,inverse(multiply(inverse(X0),X0))),X1)),multiply(X2,inverse(multiply(inverse(X1),inverse(X1))))),
inference(forward_demodulation,[],[f51522,f10259]) ).
fof(f51824,plain,
! [X2,X3,X0] : multiply(inverse(multiply(multiply(inverse(X2),X2),multiply(X0,inverse(X0)))),X3) = X3,
inference(forward_demodulation,[],[f51585,f44948]) ).
fof(f51980,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(X3,inverse(inverse(inverse(X1))))),multiply(X3,inverse(inverse(multiply(inverse(inverse(X1)),inverse(X1)))))),inverse(multiply(inverse(inverse(multiply(inverse(inverse(X1)),inverse(X1)))),inverse(multiply(inverse(inverse(X1)),inverse(X1)))))) = multiply(inverse(multiply(multiply(X2,inverse(multiply(inverse(X0),X0))),X1)),multiply(X2,multiply(X1,inverse(inverse(X1))))),
inference(forward_demodulation,[],[f51777,f10324]) ).
fof(f52020,plain,
! [X2,X3,X0] : multiply(multiply(X0,inverse(multiply(multiply(inverse(X2),X2),X0))),X3) = X3,
inference(forward_demodulation,[],[f51824,f30686]) ).
fof(f52130,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(inverse(multiply(X1,inverse(X1)))))),inverse(multiply(inverse(inverse(multiply(X1,inverse(X1)))),inverse(multiply(X1,inverse(X1)))))) = multiply(inverse(multiply(multiply(X2,inverse(multiply(inverse(X0),X0))),X1)),multiply(X2,multiply(X1,X1))),
inference(forward_demodulation,[],[f51980,f10136]) ).
fof(f52163,plain,
! [X2,X3,X0] : multiply(X0,multiply(inverse(multiply(multiply(inverse(X2),X2),X0)),X3)) = X3,
inference(forward_demodulation,[],[f52020,f28671]) ).
fof(f52253,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(inverse(multiply(X1,inverse(X1)))))),inverse(multiply(inverse(inverse(multiply(X1,inverse(X1)))),inverse(multiply(X1,inverse(X1)))))) = multiply(inverse(multiply(X2,multiply(inverse(multiply(inverse(X0),X0)),X1))),multiply(X2,multiply(X1,X1))),
inference(forward_demodulation,[],[f52130,f30982]) ).
fof(f52281,plain,
! [X2,X3,X0] : multiply(X0,multiply(inverse(multiply(inverse(X2),multiply(X2,X0))),X3)) = X3,
inference(forward_demodulation,[],[f52163,f30982]) ).
fof(f52364,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(inverse(multiply(X1,inverse(X1)))))),inverse(multiply(inverse(inverse(multiply(X1,inverse(X1)))),inverse(multiply(X1,inverse(X1)))))) = multiply(multiply(inverse(X1),multiply(multiply(inverse(X0),X0),inverse(X2))),multiply(X2,multiply(X1,X1))),
inference(forward_demodulation,[],[f52253,f30479]) ).
fof(f52385,plain,
! [X2,X3,X0] : multiply(X0,multiply(multiply(inverse(multiply(X2,X0)),X2),X3)) = X3,
inference(forward_demodulation,[],[f52281,f26013]) ).
fof(f52466,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(inverse(multiply(X1,inverse(X1)))))),inverse(multiply(inverse(inverse(multiply(X1,inverse(X1)))),inverse(multiply(X1,inverse(X1)))))) = multiply(inverse(X1),multiply(multiply(multiply(inverse(X0),X0),inverse(X2)),multiply(X2,multiply(X1,X1)))),
inference(forward_demodulation,[],[f52364,f29701]) ).
fof(f52485,plain,
! [X2,X3,X0] : multiply(X0,multiply(inverse(multiply(X2,X0)),multiply(X2,X3))) = X3,
inference(forward_demodulation,[],[f52385,f29701]) ).
fof(f52556,plain,
! [X2,X3,X0,X1] : multiply(multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(inverse(multiply(X1,inverse(X1)))))),inverse(multiply(inverse(inverse(multiply(X1,inverse(X1)))),inverse(multiply(X1,inverse(X1)))))) = multiply(inverse(X1),multiply(multiply(inverse(X0),X0),multiply(inverse(X2),multiply(X2,multiply(X1,X1))))),
inference(forward_demodulation,[],[f52466,f28671]) ).
fof(f52643,plain,
! [X2,X3,X1] : multiply(multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(inverse(multiply(X1,inverse(X1)))))),inverse(multiply(inverse(inverse(multiply(X1,inverse(X1)))),inverse(multiply(X1,inverse(X1)))))) = multiply(inverse(X1),multiply(inverse(X2),multiply(X2,multiply(X1,X1)))),
inference(forward_demodulation,[],[f52556,f8516]) ).
fof(f52726,plain,
! [X2,X3,X1] : multiply(multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,inverse(inverse(multiply(X1,inverse(X1)))))),inverse(multiply(inverse(inverse(multiply(X1,inverse(X1)))),inverse(multiply(X1,inverse(X1)))))) = multiply(inverse(multiply(X2,X1)),multiply(X2,multiply(X1,X1))),
inference(forward_demodulation,[],[f52643,f44948]) ).
fof(f52806,plain,
! [X2,X3,X1] : multiply(inverse(multiply(X2,X1)),multiply(X2,multiply(X1,X1))) = multiply(inverse(multiply(X3,inverse(X1))),multiply(multiply(X3,inverse(inverse(multiply(X1,inverse(X1))))),inverse(multiply(inverse(inverse(multiply(X1,inverse(X1)))),inverse(multiply(X1,inverse(X1))))))),
inference(forward_demodulation,[],[f52726,f29701]) ).
fof(f52886,plain,
! [X2,X3,X1] : multiply(inverse(multiply(X2,X1)),multiply(X2,multiply(X1,X1))) = multiply(inverse(multiply(X3,inverse(X1))),multiply(X3,multiply(inverse(inverse(multiply(X1,inverse(X1)))),inverse(multiply(inverse(inverse(multiply(X1,inverse(X1)))),inverse(multiply(X1,inverse(X1)))))))),
inference(forward_demodulation,[],[f52806,f28671]) ).
fof(f52962,plain,
! [X2,X1] : multiply(X1,multiply(inverse(inverse(multiply(X1,inverse(X1)))),inverse(multiply(inverse(inverse(multiply(X1,inverse(X1)))),inverse(multiply(X1,inverse(X1))))))) = multiply(inverse(multiply(X2,X1)),multiply(X2,multiply(X1,X1))),
inference(forward_demodulation,[],[f52886,f10168]) ).
fof(f53035,plain,
! [X2,X1] : multiply(X1,inverse(multiply(multiply(inverse(inverse(multiply(X1,inverse(X1)))),inverse(multiply(X1,inverse(X1)))),inverse(multiply(X1,inverse(X1)))))) = multiply(inverse(multiply(X2,X1)),multiply(X2,multiply(X1,X1))),
inference(forward_demodulation,[],[f52962,f10259]) ).
fof(f53105,plain,
! [X2,X1] : multiply(X1,multiply(multiply(X1,inverse(X1)),inverse(multiply(inverse(inverse(multiply(X1,inverse(X1)))),inverse(multiply(X1,inverse(X1))))))) = multiply(inverse(multiply(X2,X1)),multiply(X2,multiply(X1,X1))),
inference(forward_demodulation,[],[f53035,f10324]) ).
fof(f53172,plain,
! [X2,X1] : multiply(X1,multiply(X1,multiply(inverse(X1),inverse(multiply(inverse(inverse(multiply(X1,inverse(X1)))),inverse(multiply(X1,inverse(X1)))))))) = multiply(inverse(multiply(X2,X1)),multiply(X2,multiply(X1,X1))),
inference(forward_demodulation,[],[f53105,f28671]) ).
fof(f53232,plain,
! [X2,X1] : multiply(X1,inverse(multiply(inverse(inverse(multiply(X1,inverse(X1)))),inverse(multiply(X1,inverse(X1)))))) = multiply(inverse(multiply(X2,X1)),multiply(X2,multiply(X1,X1))),
inference(forward_demodulation,[],[f53172,f14956]) ).
fof(f53284,plain,
! [X2,X1] : multiply(inverse(multiply(X2,X1)),multiply(X2,multiply(X1,X1))) = X1,
inference(forward_demodulation,[],[f53232,f10156]) ).
fof(f88378,plain,
! [X2,X0,X1] : multiply(inverse(X1),X0) = multiply(inverse(multiply(X2,X1)),multiply(X2,X0)),
inference(superposition,[],[f10376,f52485]) ).
fof(f89831,plain,
! [X0,X1] : multiply(multiply(X1,X0),X0) = multiply(X1,multiply(X0,X0)),
inference(superposition,[],[f14956,f53284]) ).
fof(f90867,plain,
! [X2,X0,X1] : multiply(X0,X2) = multiply(multiply(multiply(X0,X1),inverse(multiply(X2,X1))),multiply(X2,X2)),
inference(superposition,[],[f89831,f14851]) ).
fof(f91053,plain,
! [X2,X0,X1] : multiply(X0,X2) = multiply(multiply(X0,X1),multiply(inverse(multiply(X2,X1)),multiply(X2,X2))),
inference(forward_demodulation,[],[f90867,f28671]) ).
fof(f91157,plain,
! [X2,X0,X1] : multiply(X0,X2) = multiply(multiply(X0,X1),multiply(inverse(X1),X2)),
inference(forward_demodulation,[],[f91053,f88378]) ).
fof(f92546,plain,
! [X2,X0,X1] : multiply(X1,multiply(X2,X0)) = multiply(multiply(X1,X2),X0),
inference(superposition,[],[f91157,f10376]) ).
fof(f105099,plain,
( multiply(a3,multiply(b3,c3)) != multiply(a3,multiply(b3,c3))
| spl0_1 ),
inference(superposition,[],[f7,f92546]) ).
fof(f105186,plain,
( $false
| spl0_1 ),
inference(trivial_inequality_removal,[],[f105099]) ).
fof(f105187,plain,
spl0_1,
inference(avatar_contradiction_clause,[],[f105186]) ).
fof(f107285,plain,
( $false
| spl0_2 ),
inference(forward_subsumption_resolution,[],[f11,f8516]) ).
fof(f107286,plain,
spl0_2,
inference(avatar_contradiction_clause,[],[f107285]) ).
fof(f107287,plain,
( $false
| spl0_3 ),
inference(forward_subsumption_resolution,[],[f15,f813]) ).
fof(f107288,plain,
spl0_3,
inference(avatar_contradiction_clause,[],[f107287]) ).
cnf(s1,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3 ),
inference(sat_conversion,[],[f16]) ).
cnf(s2,plain,
spl0_1,
inference(sat_conversion,[],[f105187]) ).
cnf(s3,plain,
spl0_2,
inference(sat_conversion,[],[f107286]) ).
cnf(s4,plain,
spl0_3,
inference(sat_conversion,[],[f107288]) ).
cnf(s5,plain,
$false,
inference(rat,[],[s1,s4,s3,s2]) ).
fof(f107289,plain,
$false,
inference(avatar_sat_refutation,[],[s5]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP051-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.36 % Computer : n001.cluster.edu
% 0.11/0.36 % Model : x86_64 x86_64
% 0.11/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.36 % Memory : 8046.5625MB
% 0.11/0.36 % OS : Linux 6.8.0-71-generic
% 0.11/0.36 % CPULimit : 300
% 0.11/0.36 % WCLimit : 300
% 0.11/0.36 % DateTime : Sun Sep 27 09:22:45 UTC 2026
% 0.11/0.37 % CPUTime :
% 0.11/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.40 Running first-order model finding
% 0.11/0.40 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
% 19.80/3.22 % (3285044)Will run a generic schedule for satisfiability detection.
% 19.80/3.22 % (3285050)% WARNING: option uhcvi not known.
% 19.80/3.22 % (3285054)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3282952132:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 19.80/3.22 % (3285051)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3849674679:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 19.80/3.22 % (3285049)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3236894665_2999 on theBenchmark for (2999ds/0Mi)
% 19.80/3.22 % (3285052)dis+10_1_sil=32000:sp=arity:random_seed=820207970:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 19.80/3.22 % (3285050)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2366961911:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 19.80/3.22 % (3285053)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=12692181:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 19.80/3.22 % (3285055)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2927916553:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 19.80/3.22 % TRYING [1]
% 19.80/3.22 % TRYING [2]
% 19.80/3.22 % TRYING [3]
% 19.80/3.22 % (3285054)Instruction limit reached!
% 19.80/3.22 % (3285054)------------------------------
% 19.80/3.22 % (3285054)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.80/3.22 % (3285054)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.80/3.22 % (3285054)CaDiCaL version: 2.1.3
% 19.80/3.22 % (3285054)Termination reason: Instruction limit
% 19.80/3.22 % (3285054)Termination phase: Saturation
% 19.80/3.22 % (3285054)Time elapsed: 0.041 s
% 19.80/3.22 % (3285054)Peak memory usage: 13 MB
% 19.80/3.22 % (3285054)Instructions burned: 134 (million)
% 19.80/3.22 % (3285052)Instruction limit reached!
% 19.80/3.22 % (3285052)------------------------------
% 19.80/3.22 % (3285052)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.80/3.22 % (3285052)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.80/3.22 % (3285052)CaDiCaL version: 2.1.3
% 19.80/3.22 % (3285052)Termination reason: Instruction limit
% 19.80/3.22 % (3285052)Termination phase: Saturation
% 19.80/3.22 % (3285052)Time elapsed: 0.056 s
% 19.80/3.22 % (3285052)Peak memory usage: 12 MB
% 19.80/3.22 % (3285052)Instructions burned: 104 (million)
% 19.80/3.22 % TRYING [4]
% 19.80/3.22 % (3285063)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3092535078:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 19.80/3.22 % TRYING [1]
% 19.80/3.22 % TRYING [2]
% 19.80/3.22 % TRYING [3]
% 19.80/3.22 % (3285053)Instruction limit reached!
% 19.80/3.22 % (3285053)------------------------------
% 19.80/3.22 % (3285053)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.80/3.22 % (3285053)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.80/3.22 % (3285053)CaDiCaL version: 2.1.3
% 19.80/3.22 % (3285053)Termination reason: Instruction limit
% 19.80/3.22 % (3285053)Termination phase: Saturation
% 19.80/3.22 % (3285053)Time elapsed: 0.067 s
% 19.80/3.22 % (3285053)Peak memory usage: 13 MB
% 19.80/3.22 % (3285053)Instructions burned: 116 (million)
% 19.80/3.22 % (3285064)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3780535972:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 19.80/3.22 % (3285067)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=3427897780:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 19.80/3.22 % (3285055)Instruction limit reached!
% 19.80/3.22 % (3285055)------------------------------
% 19.80/3.22 % (3285055)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.80/3.22 % (3285055)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.80/3.22 % (3285055)CaDiCaL version: 2.1.3
% 19.80/3.22 % (3285055)Termination reason: Instruction limit
% 19.80/3.22 % (3285055)Termination phase: Saturation
% 19.80/3.22 % (3285055)Time elapsed: 0.094 s
% 19.80/3.22 % (3285055)Peak memory usage: 12 MB
% 19.80/3.22 % (3285055)Instructions burned: 159 (million)
% 19.80/3.22 % (3285064)Instruction limit reached!
% 19.80/3.22 % (3285064)------------------------------
% 19.80/3.22 % (3285064)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 19.80/3.22 % (3285064)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.80/3.22 % (3285064)CaDiCaL version: 2.1.3
% 19.80/3.22 % (3285064)Termination reason: Instruction limit
% 43.85/6.60 % (3285064)Termination phase: Saturation
% 43.85/6.60 % (3285064)Time elapsed: 0.041 s
% 43.85/6.60 % (3285064)Peak memory usage: 13 MB
% 43.85/6.60 % (3285064)Instructions burned: 133 (million)
% 43.85/6.60 % (3285069)ott-21_1_sil=16000:fs=off:random_seed=2603636824:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 43.85/6.60 % (3285070)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2275882274:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 43.85/6.60 % TRYING [4]
% 43.85/6.60 % (3285069)Instruction limit reached!
% 43.85/6.60 % (3285069)------------------------------
% 43.85/6.60 % (3285069)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.85/6.60 % (3285069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.85/6.60 % (3285069)CaDiCaL version: 2.1.3
% 43.85/6.60 % (3285069)Termination reason: Instruction limit
% 43.85/6.60 % (3285069)Termination phase: Saturation
% 43.85/6.60 % (3285069)Time elapsed: 0.089 s
% 43.85/6.60 % (3285069)Peak memory usage: 11 MB
% 43.85/6.60 % (3285069)Instructions burned: 181 (million)
% 43.85/6.60 % (3285073)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2364953645:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 43.85/6.60 % TRYING [1]
% 43.85/6.60 % TRYING [2]
% 43.85/6.60 % TRYING [3]
% 43.85/6.60 % (3285070)Instruction limit reached!
% 43.85/6.60 % (3285070)------------------------------
% 43.85/6.60 % (3285070)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.85/6.60 % (3285070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.85/6.60 % (3285070)CaDiCaL version: 2.1.3
% 43.85/6.60 % (3285070)Termination reason: Instruction limit
% 43.85/6.60 % (3285070)Termination phase: Saturation
% 43.85/6.60 % (3285070)Time elapsed: 0.126 s
% 43.85/6.60 % (3285070)Peak memory usage: 14 MB
% 43.85/6.60 % (3285070)Instructions burned: 479 (million)
% 43.85/6.60 % TRYING [4]
% 43.85/6.60 % (3285075)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3157127627:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 43.85/6.60 % (3285067)Instruction limit reached!
% 43.85/6.60 % (3285067)------------------------------
% 43.85/6.60 % (3285067)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.85/6.60 % (3285067)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.85/6.60 % (3285067)CaDiCaL version: 2.1.3
% 43.85/6.60 % (3285067)Termination reason: Instruction limit
% 43.85/6.60 % (3285067)Termination phase: Saturation
% 43.85/6.60 % (3285067)Time elapsed: 0.325 s
% 43.85/6.60 % (3285067)Peak memory usage: 16 MB
% 43.85/6.60 % (3285067)Instructions burned: 686 (million)
% 43.85/6.60 % (3285077)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=166167018:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 43.85/6.60 % TRYING [14]
% 43.85/6.60 % (3285063)Instruction limit reached!
% 43.85/6.60 % (3285063)------------------------------
% 43.85/6.60 % (3285063)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.85/6.60 % (3285063)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.85/6.60 % (3285063)CaDiCaL version: 2.1.3
% 43.85/6.60 % (3285063)Termination reason: Instruction limit
% 43.85/6.60 % (3285063)Termination phase: Finite model building SAT solving
% 43.85/6.60 % (3285063)Time elapsed: 0.422 s
% 43.85/6.60 % (3285063)Peak memory usage: 12 MB
% 43.85/6.60 % (3285063)Instructions burned: 714 (million)
% 43.85/6.60 % (3285079)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=3736907781:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 43.85/6.60 % (3285075)Instruction limit reached!
% 43.85/6.60 % (3285075)------------------------------
% 43.85/6.60 % (3285075)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 43.85/6.60 % (3285075)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.85/6.60 % (3285075)CaDiCaL version: 2.1.3
% 43.85/6.60 % (3285075)Termination reason: Instruction limit
% 43.85/6.60 % (3285075)Termination phase: Saturation
% 43.85/6.60 % (3285075)Time elapsed: 0.335 s
% 43.85/6.60 % (3285075)Peak memory usage: 25 MB
% 43.85/6.60 % (3285075)Instructions burned: 1192 (million)
% 43.85/6.60 % (3285081)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3484333132:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 43.85/6.60 % (3285077)Instruction limit reached!
% 43.85/6.60 % (3285077)------------------------------
% 43.85/6.60 % (3285077)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.80/19.76 % (3285077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.80/19.76 % (3285077)CaDiCaL version: 2.1.3
% 136.80/19.76 % (3285077)Termination reason: Instruction limit
% 136.80/19.76 % (3285077)Termination phase: Finite model building constraint generation
% 136.80/19.76 % (3285077)Time elapsed: 0.321 s
% 136.80/19.76 % (3285077)Peak memory usage: 80 MB
% 136.80/19.76 % (3285077)Instructions burned: 890 (million)
% 136.80/19.76 % (3285073)Instruction limit reached!
% 136.80/19.76 % (3285073)------------------------------
% 136.80/19.76 % (3285073)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.80/19.76 % (3285073)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.80/19.76 % (3285073)CaDiCaL version: 2.1.3
% 136.80/19.76 % (3285073)Termination reason: Instruction limit
% 136.80/19.76 % (3285073)Termination phase: Finite model building SAT solving
% 136.80/19.76 % (3285073)Time elapsed: 0.550 s
% 136.80/19.76 % (3285073)Peak memory usage: 12 MB
% 136.80/19.76 % (3285073)Instructions burned: 866 (million)
% 136.80/19.76 % (3285083)fmb+10_1_sil=64000:random_seed=162493222:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 136.80/19.76 % TRYING [1]
% 136.80/19.76 % TRYING [2]
% 136.80/19.76 % TRYING [3]
% 136.80/19.76 % (3285084)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2482721781:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 136.80/19.76 % TRYING [20]
% 136.80/19.76 % TRYING [4]
% 136.80/19.76 % (3285081)Instruction limit reached!
% 136.80/19.76 % (3285081)------------------------------
% 136.80/19.76 % (3285081)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.80/19.76 % (3285081)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.80/19.76 % (3285081)CaDiCaL version: 2.1.3
% 136.80/19.76 % (3285081)Termination reason: Instruction limit
% 136.80/19.76 % (3285081)Termination phase: Saturation
% 136.80/19.76 % (3285081)Time elapsed: 0.229 s
% 136.80/19.76 % (3285081)Peak memory usage: 16 MB
% 136.80/19.76 % (3285081)Instructions burned: 880 (million)
% 136.80/19.76 % (3285087)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3200815158:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi)
% 136.80/19.76 % TRYING [8]
% 136.80/19.76 % (3285079)Instruction limit reached!
% 136.80/19.76 % (3285079)------------------------------
% 136.80/19.76 % (3285079)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.80/19.76 % (3285079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.80/19.76 % (3285079)CaDiCaL version: 2.1.3
% 136.80/19.76 % (3285079)Termination reason: Instruction limit
% 136.80/19.76 % (3285079)Termination phase: Saturation
% 136.80/19.76 % (3285079)Time elapsed: 0.377 s
% 136.80/19.76 % (3285079)Peak memory usage: 19 MB
% 136.80/19.76 % (3285079)Instructions burned: 692 (million)
% 136.80/19.76 % (3285089)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=3923234005:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 136.80/19.76 % (3285087)Instruction limit reached!
% 136.80/19.76 % (3285087)------------------------------
% 136.80/19.76 % (3285087)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.80/19.76 % (3285087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.80/19.76 % (3285087)CaDiCaL version: 2.1.3
% 136.80/19.76 % (3285087)Termination reason: Instruction limit
% 136.80/19.76 % (3285087)Termination phase: Finite model building SAT solving
% 136.80/19.76 % (3285087)Time elapsed: 0.259 s
% 136.80/19.76 % (3285087)Peak memory usage: 34 MB
% 136.80/19.76 % (3285087)Instructions burned: 921 (million)
% 136.80/19.76 % (3285091)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1493667464:i=1472:ins=7:fdi=8:gsp=on_2988 on theBenchmark for (2988ds/1472Mi)
% 136.80/19.76 % (3285091)Instruction limit reached!
% 136.80/19.76 % (3285091)------------------------------
% 136.80/19.76 % (3285091)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 136.80/19.76 % (3285091)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 136.80/19.76 % (3285091)CaDiCaL version: 2.1.3
% 136.80/19.76 % (3285091)Termination reason: Instruction limit
% 136.80/19.76 % (3285091)Termination phase: Saturation
% 136.80/19.76 % (3285091)Time elapsed: 0.337 s
% 136.80/19.76 % (3285091)Peak memory usage: 23 MB
% 136.80/19.76 % (3285091)Instructions burned: 1475 (million)
% 136.80/19.76 % (3285093)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1673043529:i=6324_2985 on theBenchmark for (2985ds/6324Mi)
% 136.80/19.76 % TRYING [77]
% 136.80/19.76 % (3285093)Instruction limit reached!
% 136.80/19.76 % (3285093)------------------------------
% 136.80/19.76 % (3285093)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 219.10/31.37 % (3285093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 219.10/31.37 % (3285093)CaDiCaL version: 2.1.3
% 219.10/31.37 % (3285093)Termination reason: Instruction limit
% 219.10/31.37 % (3285093)Termination phase: Finite model building constraint generation
% 219.10/31.37 % (3285093)Time elapsed: 1.314 s
% 219.10/31.37 % (3285093)Peak memory usage: 521 MB
% 219.10/31.37 % (3285093)Instructions burned: 6325 (million)
% 219.10/31.37 % (3285095)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=522603607:fmbsr=2.30978:i=2174_2971 on theBenchmark for (2971ds/2174Mi)
% 219.10/31.37 % TRYING [16]
% 219.10/31.37 % (3285095)Instruction limit reached!
% 219.10/31.37 % (3285095)------------------------------
% 219.10/31.37 % (3285095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 219.10/31.37 % (3285095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 219.10/31.37 % (3285095)CaDiCaL version: 2.1.3
% 219.10/31.37 % (3285095)Termination reason: Instruction limit
% 219.10/31.37 % (3285095)Termination phase: Finite model building constraint generation
% 219.10/31.37 % (3285095)Time elapsed: 0.399 s
% 219.10/31.37 % (3285095)Peak memory usage: 133 MB
% 219.10/31.37 % (3285095)Instructions burned: 2178 (million)
% 219.10/31.37 % (3285097)ott-2_1_sil=16000:newcnf=on:random_seed=226437691:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2967 on theBenchmark for (2967ds/869Mi)
% 219.10/31.37 % (3285089)Instruction limit reached!
% 219.10/31.37 % (3285089)------------------------------
% 219.10/31.37 % (3285089)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 219.10/31.37 % (3285089)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 219.10/31.37 % (3285089)CaDiCaL version: 2.1.3
% 219.10/31.37 % (3285089)Termination reason: Instruction limit
% 219.10/31.37 % (3285089)Termination phase: Saturation
% 219.10/31.37 % (3285089)Time elapsed: 2.546 s
% 219.10/31.37 % (3285089)Peak memory usage: 35 MB
% 219.10/31.37 % (3285089)Instructions burned: 5133 (million)
% 219.10/31.37 % (3285099)ott+10_1_sil=32000:tgt=ground:random_seed=408358638:i=5114:av=off_2965 on theBenchmark for (2965ds/5114Mi)
% 219.10/31.37 % (3285097)Instruction limit reached!
% 219.10/31.37 % (3285097)------------------------------
% 219.10/31.37 % (3285097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 219.10/31.37 % (3285097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 219.10/31.37 % (3285097)CaDiCaL version: 2.1.3
% 219.10/31.37 % (3285097)Termination reason: Instruction limit
% 219.10/31.37 % (3285097)Termination phase: Saturation
% 219.10/31.37 % (3285097)Time elapsed: 0.251 s
% 219.10/31.37 % (3285097)Peak memory usage: 21 MB
% 219.10/31.37 % (3285097)Instructions burned: 871 (million)
% 219.10/31.37 % (3285101)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2797143284:i=54282_2964 on theBenchmark for (2964ds/54282Mi)
% 219.10/31.37 % TRYING [1]
% 219.10/31.37 % TRYING [2]
% 219.10/31.37 % TRYING [3]
% 219.10/31.37 % TRYING [4]
% 219.10/31.37 % (3285084)Instruction limit reached!
% 219.10/31.37 % (3285084)------------------------------
% 219.10/31.37 % (3285084)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 219.10/31.37 % (3285084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 219.10/31.37 % (3285084)CaDiCaL version: 2.1.3
% 219.10/31.37 % (3285084)Termination reason: Instruction limit
% 219.10/31.37 % (3285084)Termination phase: Finite model building constraint generation
% 219.10/31.37 % (3285084)Time elapsed: 3.571 s
% 219.10/31.37 % (3285084)Peak memory usage: 652 MB
% 219.10/31.37 % (3285084)Instructions burned: 9516 (million)
% 219.10/31.37 % (3285103)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=439921389:i=3512:aac=none_2955 on theBenchmark for (2955ds/3512Mi)
% 219.10/31.37 % (3285099)Instruction limit reached!
% 219.10/31.37 % (3285099)------------------------------
% 219.10/31.37 % (3285099)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 219.10/31.37 % (3285099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 219.10/31.37 % (3285099)CaDiCaL version: 2.1.3
% 219.10/31.37 % (3285099)Termination reason: Instruction limit
% 219.10/31.37 % (3285099)Termination phase: Saturation
% 219.10/31.37 % (3285099)Time elapsed: 2.583 s
% 219.10/31.37 % (3285099)Peak memory usage: 62 MB
% 219.10/31.37 % (3285099)Instructions burned: 5115 (million)
% 219.10/31.37 % (3285105)dis+21_1_sil=32000:sas=cadical:random_seed=2251123863:i=3773:amm=off_2939 on theBenchmark for (2939ds/3773Mi)
% 219.10/31.37 % (3285103)Instruction limit reached!
% 219.10/31.37 % (3285103)------------------------------
% 219.10/31.37 % (3285103)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.34/31.43 % (3285103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.34/31.43 % (3285103)CaDiCaL version: 2.1.3
% 145.34/31.43 % (3285103)Termination reason: Instruction limit
% 145.34/31.43 % (3285103)Termination phase: Saturation
% 145.34/31.43 % (3285103)Time elapsed: 1.701 s
% 145.34/31.43 % (3285103)Peak memory usage: 29 MB
% 145.34/31.43 % (3285103)Instructions burned: 3513 (million)
% 145.34/31.43 % (3285107)ott+11_1_sil=16000:gs=on:random_seed=1193709190:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2937 on theBenchmark for (2937ds/2251Mi)
% 145.34/31.43 % TRYING [5]
% 145.34/31.43 % TRYING [5]
% 145.34/31.43 % (3285107)Instruction limit reached!
% 145.34/31.43 % (3285107)------------------------------
% 145.34/31.43 % (3285107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.34/31.43 % (3285107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.34/31.43 % (3285107)CaDiCaL version: 2.1.3
% 145.34/31.43 % (3285107)Termination reason: Instruction limit
% 145.34/31.43 % (3285107)Termination phase: Saturation
% 145.34/31.43 % (3285107)Time elapsed: 1.191 s
% 145.34/31.43 % (3285107)Peak memory usage: 32 MB
% 145.34/31.43 % (3285107)Instructions burned: 2251 (million)
% 145.34/31.43 % (3285109)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3767956034:fmbsr=1.6:i=67534_2925 on theBenchmark for (2925ds/67534Mi)
% 145.34/31.43 % TRYING [7]
% 145.34/31.43 % (3285105)Instruction limit reached!
% 145.34/31.43 % (3285105)------------------------------
% 145.34/31.43 % (3285105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.34/31.43 % (3285105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.34/31.43 % (3285105)CaDiCaL version: 2.1.3
% 145.34/31.43 % (3285105)Termination reason: Instruction limit
% 145.34/31.43 % (3285105)Termination phase: Saturation
% 145.34/31.43 % (3285105)Time elapsed: 1.833 s
% 145.34/31.43 % (3285105)Peak memory usage: 30 MB
% 145.34/31.43 % (3285105)Instructions burned: 3774 (million)
% 145.34/31.43 % (3285111)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=2149931877:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2920 on theBenchmark for (2920ds/4591Mi)
% 145.34/31.43 % (3285111)Instruction limit reached!
% 145.34/31.44 % (3285111)------------------------------
% 145.34/31.44 % (3285111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.34/31.44 % (3285111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.34/31.44 % (3285111)CaDiCaL version: 2.1.3
% 145.34/31.44 % (3285111)Termination reason: Instruction limit
% 145.34/31.44 % (3285111)Termination phase: Saturation
% 145.34/31.44 % (3285111)Time elapsed: 1.820 s
% 145.34/31.44 % (3285111)Peak memory usage: 40 MB
% 145.34/31.44 % (3285111)Instructions burned: 4594 (million)
% 145.34/31.44 % (3285114)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=2232069316:i=29340_2902 on theBenchmark for (2902ds/29340Mi)
% 145.34/31.44 % (3285083)Instruction limit reached!
% 145.34/31.44 % (3285083)------------------------------
% 145.34/31.44 % (3285083)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.34/31.44 % (3285083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.34/31.44 % (3285083)CaDiCaL version: 2.1.3
% 145.34/31.44 % (3285083)Termination reason: Instruction limit
% 145.34/31.44 % (3285083)Termination phase: Finite model building SAT solving
% 145.34/31.44 % (3285083)Time elapsed: 13.860 s
% 145.34/31.44 % (3285083)Peak memory usage: 14 MB
% 145.34/31.44 % (3285083)Instructions burned: 22061 (million)
% 145.34/31.44 % (3285116)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=3472533362:i=5211_2853 on theBenchmark for (2853ds/5211Mi)
% 145.34/31.44 % (3285116)Instruction limit reached!
% 145.34/31.44 % (3285116)------------------------------
% 145.34/31.44 % (3285116)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.34/31.44 % (3285116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.34/31.44 % (3285116)CaDiCaL version: 2.1.3
% 145.34/31.44 % (3285116)Termination reason: Instruction limit
% 145.34/31.44 % (3285116)Termination phase: Saturation
% 145.34/31.44 % (3285116)Time elapsed: 2.549 s
% 145.34/31.44 % (3285116)Peak memory usage: 35 MB
% 145.34/31.44 % (3285116)Instructions burned: 5212 (million)
% 145.34/31.44 % (3285118)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3007006213:i=5497:nm=2_2827 on theBenchmark for (2827ds/5497Mi)
% 145.34/31.44 % TRYING [17]
% 145.34/31.44 % (3285118)Instruction limit reached!
% 145.34/31.44 % (3285118)------------------------------
% 145.34/31.44 % (3285118)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.34/31.44 % (3285118)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.34/31.44 % (3285118)CaDiCaL version: 2.1.3
% 145.34/31.44 % (3285118)Termination reason: Instruction limit
% 145.34/31.44 % (3285118)Termination phase: Finite model building constraint generation
% 145.34/31.44 % (3285118)Time elapsed: 2.089 s
% 145.34/31.44 % (3285118)Peak memory usage: 384 MB
% 145.34/31.44 % (3285118)Instructions burned: 5497 (million)
% 145.34/31.44 % (3285120)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3356109610:fmbsr=2:i=46332_2805 on theBenchmark for (2805ds/46332Mi)
% 145.34/31.44 % TRYING [15]
% 145.34/31.44 % (3285101)Instruction limit reached!
% 145.34/31.44 % (3285101)------------------------------
% 145.34/31.44 % (3285101)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.34/31.44 % (3285101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.34/31.44 % (3285101)CaDiCaL version: 2.1.3
% 145.34/31.44 % (3285101)Termination reason: Instruction limit
% 145.34/31.44 % (3285101)Termination phase: Finite model building SAT solving
% 145.34/31.44 % (3285101)Time elapsed: 17.994 s
% 145.34/31.44 % (3285101)Peak memory usage: 26 MB
% 145.34/31.44 % (3285101)Instructions burned: 54283 (million)
% 145.34/31.44 % (3285122)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=3272803584:i=14071_2784 on theBenchmark for (2784ds/14071Mi)
% 145.34/31.44 % TRYING [12]
% 145.34/31.44 % (3285114)Instruction limit reached!
% 145.34/31.44 % (3285114)------------------------------
% 145.34/31.44 % (3285114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.34/31.44 % (3285114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.34/31.44 % (3285114)CaDiCaL version: 2.1.3
% 145.34/31.44 % (3285114)Termination reason: Instruction limit
% 145.34/31.44 % (3285114)Termination phase: Saturation
% 145.34/31.44 % (3285114)Time elapsed: 13.731 s
% 145.34/31.44 % (3285114)Peak memory usage: 154 MB
% 145.34/31.44 % (3285114)Instructions burned: 29342 (million)
% 145.34/31.44 % (3285124)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3904168948:i=22565:add=on:rawr=on_2764 on theBenchmark for (2764ds/22565Mi)
% 145.34/31.44 % (3285122)Instruction limit reached!
% 145.34/31.44 % (3285122)------------------------------
% 145.34/31.44 % (3285122)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.34/31.44 % (3285122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.34/31.44 % (3285122)CaDiCaL version: 2.1.3
% 145.34/31.44 % (3285122)Termination reason: Instruction limit
% 145.34/31.44 % (3285122)Termination phase: Finite model building SAT solving
% 145.34/31.44 % (3285122)Time elapsed: 5.673 s
% 145.34/31.44 % (3285122)Peak memory usage: 186 MB
% 145.34/31.44 % (3285122)Instructions burned: 14077 (million)
% 145.34/31.44 % (3285126)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=3061171859:i=8173:av=off_2727 on theBenchmark for (2727ds/8173Mi)
% 145.34/31.44 % (3285051)Instruction limit reached!
% 145.34/31.44 % (3285051)------------------------------
% 145.34/31.44 % (3285051)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.34/31.44 % (3285051)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.34/31.44 % (3285051)CaDiCaL version: 2.1.3
% 145.34/31.44 % (3285051)Termination reason: Instruction limit
% 145.34/31.44 % (3285051)Termination phase: Saturation
% 145.34/31.44 % (3285051)Time elapsed: 28.775 s
% 145.34/31.44 % (3285051)Peak memory usage: 202 MB
% 145.34/31.44 % (3285051)Instructions burned: 88025 (million)
% 145.34/31.44 % (3285128)dis+10_16:1_sil=16000:random_seed=4188808295:i=9155:fsr=off_2711 on theBenchmark for (2711ds/9155Mi)
% 145.34/31.44 % (3285126)Instruction limit reached!
% 145.34/31.44 % (3285126)------------------------------
% 145.34/31.44 % (3285126)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.34/31.44 % (3285126)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.34/31.44 % (3285126)CaDiCaL version: 2.1.3
% 145.34/31.44 % (3285126)Termination reason: Instruction limit
% 145.34/31.44 % (3285126)Termination phase: Saturation
% 145.34/31.44 % (3285126)Time elapsed: 2.577 s
% 145.34/31.44 % (3285126)Peak memory usage: 91 MB
% 145.34/31.44 % (3285126)Instructions burned: 8175 (million)
% 145.34/31.44 % (3285130)ott-3_8_sil=64000:random_seed=3370391944:i=20139:bs=on_2701 on theBenchmark for (2701ds/20139Mi)
% 145.34/31.44 % (3285130) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3285044-3285130"...
% 145.34/31.44 % (3285130)...printing done.
% 145.34/31.44 % (3285130)Refutation found. Thanks to Tanya!
% 145.34/31.44 % SZS status Unsatisfiable for theBenchmark
% 145.34/31.44 % SZS output start Proof for theBenchmark
% See solution above
% 145.34/31.44 % (3285130)------------------------------
% 145.34/31.44 % (3285130)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 145.34/31.44 % (3285130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 145.34/31.44 % (3285130)CaDiCaL version: 2.1.3
% 145.34/31.44 % (3285130)Termination reason: Refutation
% 145.34/31.44 % (3285130)Time elapsed: 1.111 s
% 145.34/31.44 % (3285130)Peak memory usage: 42 MB
% 145.34/31.44 % (3285130)Instructions burned: 3639 (million)
% 145.34/31.44 % (3285044)Success in time 31.032 s
% 145.34/31.44 % Vampire exiting
%------------------------------------------------------------------------------