%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GRP405-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n016.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:17:43 AM UTC 2026
% Result : Unsatisfiable 220.71s 41.43s
% Output : Refutation 220.71s
% Verified :
% SZS Type : Refutation
% Derivation depth : 30
% Number of leaves : 73
% Syntax : Number of formulae : 476 ( 78 unt; 71 def)
% Number of atoms : 1252 ( 259 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 1483 ( 707 ~; 705 |; 0 &)
% ( 71 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 13 ( 5 avg)
% Maximal term depth : 13 ( 3 avg)
% Number of predicates : 73 ( 71 usr; 72 prp; 0-2 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-2 aty)
% Number of variables : 922 ( 0 sgn 922 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),X2)),inverse(multiply(X1,multiply(inverse(X1),X1)))))) = X2,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,negated_conjecture,
multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_these_axioms_3) ).
fof(f4,definition,
( spl0_1
<=> multiply(multiply(a3,b3),c3) = multiply(a3,multiply(b3,c3)) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f6,plain,
( multiply(multiply(a3,b3),c3) != multiply(a3,multiply(b3,c3))
| spl0_1 ),
inference(avatar_component_clause,[],[f4]) ).
fof(f7,plain,
~ spl0_1,
inference(avatar_split_clause,[],[f2,f4]) ).
fof(f9,definition,
( spl0_2
<=> ! [X2,X0,X1] : multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),X2)),inverse(multiply(X1,multiply(inverse(X1),X1)))))) = X2 ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f10,plain,
( ! [X2,X0,X1] : multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),X2)),inverse(multiply(X1,multiply(inverse(X1),X1)))))) = X2
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f9]) ).
fof(f11,plain,
spl0_2,
inference(avatar_split_clause,[],[f1,f9]) ).
fof(f13,plain,
( ! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),X3)),X0)),inverse(multiply(X3,multiply(inverse(X3),X3))))) = multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(X2,multiply(inverse(X2),X2))))))
| ~ spl0_2 ),
inference(superposition,[],[f10,f10]) ).
fof(f15,definition,
( spl0_3
<=> ! [X0,X3,X2,X1] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),X3)),X0)),inverse(multiply(X3,multiply(inverse(X3),X3))))) = multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(X2,multiply(inverse(X2),X2)))))) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f16,plain,
( ! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),X3)),X0)),inverse(multiply(X3,multiply(inverse(X3),X3))))) = multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(X2,multiply(inverse(X2),X2))))))
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f15]) ).
fof(f17,plain,
( spl0_3
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f13,f9,f15]) ).
fof(f39,plain,
( ! [X2,X0,X1] : multiply(inverse(multiply(X0,X2)),multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(X2,multiply(inverse(X2),X2))))))) = X1
| ~ spl0_2
| ~ spl0_3 ),
inference(superposition,[],[f10,f16]) ).
fof(f43,plain,
( ! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),X2)),multiply(inverse(multiply(X0,X1)),X3))),inverse(multiply(X2,multiply(inverse(X2),X2))))) = X3
| ~ spl0_2
| ~ spl0_3 ),
inference(superposition,[],[f10,f16]) ).
fof(f60,definition,
( spl0_8
<=> ! [X0,X3,X2,X1] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),X2)),multiply(inverse(multiply(X0,X1)),X3))),inverse(multiply(X2,multiply(inverse(X2),X2))))) = X3 ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f61,plain,
( ! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),X2)),multiply(inverse(multiply(X0,X1)),X3))),inverse(multiply(X2,multiply(inverse(X2),X2))))) = X3
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f60]) ).
fof(f62,plain,
( spl0_8
| ~ spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f43,f15,f9,f60]) ).
fof(f76,definition,
( spl0_12
<=> ! [X2,X0,X1] : multiply(inverse(multiply(X0,X2)),multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(X2,multiply(inverse(X2),X2))))))) = X1 ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f77,plain,
( ! [X2,X0,X1] : multiply(inverse(multiply(X0,X2)),multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(X2,multiply(inverse(X2),X2))))))) = X1
| ~ spl0_12 ),
inference(avatar_component_clause,[],[f76]) ).
fof(f78,plain,
( spl0_12
| ~ spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f39,f15,f9,f76]) ).
fof(f146,plain,
( ! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(inverse(multiply(X0,X2)),X4)),X1) = multiply(inverse(multiply(X3,X4)),multiply(X3,multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(X2,multiply(inverse(X2),X2))))))))
| ~ spl0_3
| ~ spl0_12 ),
inference(superposition,[],[f77,f16]) ).
fof(f165,definition,
( spl0_31
<=> ! [X4,X0,X3,X2,X1] : multiply(inverse(multiply(inverse(multiply(X0,X2)),X4)),X1) = multiply(inverse(multiply(X3,X4)),multiply(X3,multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(X2,multiply(inverse(X2),X2)))))))) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f166,plain,
( ! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(inverse(multiply(X0,X2)),X4)),X1) = multiply(inverse(multiply(X3,X4)),multiply(X3,multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(X2,multiply(inverse(X2),X2))))))))
| ~ spl0_31 ),
inference(avatar_component_clause,[],[f165]) ).
fof(f167,plain,
( spl0_31
| ~ spl0_3
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f146,f76,f15,f165]) ).
fof(f205,plain,
( ! [X0,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(X0,X4)),multiply(X0,X5))),inverse(multiply(X4,multiply(inverse(X4),X4))))) = X5
| ~ spl0_8 ),
inference(superposition,[],[f61,f61]) ).
fof(f217,plain,
( ! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(inverse(multiply(X3,X4)),X2)),multiply(inverse(multiply(X3,X4)),X0)) = multiply(inverse(multiply(X1,X2)),multiply(X1,X0))
| ~ spl0_8
| ~ spl0_12 ),
inference(superposition,[],[f77,f61]) ).
fof(f269,definition,
( spl0_49
<=> ! [X4,X0,X3,X2,X1] : multiply(inverse(multiply(inverse(multiply(X3,X4)),X2)),multiply(inverse(multiply(X3,X4)),X0)) = multiply(inverse(multiply(X1,X2)),multiply(X1,X0)) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f270,plain,
( ! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(inverse(multiply(X3,X4)),X2)),multiply(inverse(multiply(X3,X4)),X0)) = multiply(inverse(multiply(X1,X2)),multiply(X1,X0))
| ~ spl0_49 ),
inference(avatar_component_clause,[],[f269]) ).
fof(f271,plain,
( spl0_49
| ~ spl0_8
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f217,f76,f60,f269]) ).
fof(f301,definition,
( spl0_57
<=> ! [X4,X5,X0] : inverse(multiply(inverse(multiply(inverse(multiply(X0,X4)),multiply(X0,X5))),inverse(multiply(X4,multiply(inverse(X4),X4))))) = X5 ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f302,plain,
( ! [X0,X4,X5] : inverse(multiply(inverse(multiply(inverse(multiply(X0,X4)),multiply(X0,X5))),inverse(multiply(X4,multiply(inverse(X4),X4))))) = X5
| ~ spl0_57 ),
inference(avatar_component_clause,[],[f301]) ).
fof(f303,plain,
( spl0_57
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f205,f60,f301]) ).
fof(f348,plain,
( ! [X2,X0,X1] : inverse(multiply(X2,multiply(inverse(X2),X2))) = multiply(inverse(multiply(X1,X2)),inverse(multiply(X0,inverse(multiply(multiply(X1,X0),multiply(inverse(multiply(X1,X0)),multiply(X1,X0)))))))
| ~ spl0_2
| ~ spl0_57 ),
inference(superposition,[],[f10,f302]) ).
fof(f350,plain,
( ! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,X2)),multiply(X1,X0)) = multiply(inverse(multiply(X3,X2)),multiply(X3,X0))
| ~ spl0_12
| ~ spl0_57 ),
inference(superposition,[],[f77,f302]) ).
fof(f408,definition,
( spl0_75
<=> ! [X0,X3,X2,X1] : multiply(inverse(multiply(X1,X2)),multiply(X1,X0)) = multiply(inverse(multiply(X3,X2)),multiply(X3,X0)) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f409,plain,
( ! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,X2)),multiply(X1,X0)) = multiply(inverse(multiply(X3,X2)),multiply(X3,X0))
| ~ spl0_75 ),
inference(avatar_component_clause,[],[f408]) ).
fof(f410,plain,
( spl0_75
| ~ spl0_12
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f350,f301,f76,f408]) ).
fof(f416,definition,
( spl0_77
<=> ! [X2,X0,X1] : inverse(multiply(X2,multiply(inverse(X2),X2))) = multiply(inverse(multiply(X1,X2)),inverse(multiply(X0,inverse(multiply(multiply(X1,X0),multiply(inverse(multiply(X1,X0)),multiply(X1,X0))))))) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f417,plain,
( ! [X2,X0,X1] : inverse(multiply(X2,multiply(inverse(X2),X2))) = multiply(inverse(multiply(X1,X2)),inverse(multiply(X0,inverse(multiply(multiply(X1,X0),multiply(inverse(multiply(X1,X0)),multiply(X1,X0)))))))
| ~ spl0_77 ),
inference(avatar_component_clause,[],[f416]) ).
fof(f418,plain,
( spl0_77
| ~ spl0_2
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f348,f301,f9,f416]) ).
fof(f477,plain,
( ! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),X0)),inverse(multiply(X3,multiply(inverse(X3),X3))))))),multiply(X1,X4)) = multiply(inverse(X0),multiply(X2,X4))
| ~ spl0_2
| ~ spl0_75 ),
inference(superposition,[],[f409,f10]) ).
fof(f481,plain,
( ! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(X3,multiply(X4,X2))),multiply(X3,X5)) = multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))),multiply(inverse(multiply(X4,X1)),X5))
| ~ spl0_75 ),
inference(superposition,[],[f409,f409]) ).
fof(f484,plain,
( ! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X1,inverse(multiply(X2,multiply(inverse(X2),X2))))),multiply(X1,X3)) = multiply(X0,multiply(inverse(multiply(inverse(multiply(X4,X2)),multiply(X4,X0))),X3))
| ~ spl0_57
| ~ spl0_75 ),
inference(superposition,[],[f409,f302]) ).
fof(f489,plain,
( ! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(X3,X4)),multiply(X3,multiply(X5,X2))) = multiply(inverse(multiply(inverse(multiply(X5,X1)),X4)),multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))
| ~ spl0_75 ),
inference(superposition,[],[f409,f409]) ).
fof(f516,plain,
( ! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(inverse(multiply(X2,multiply(X3,X1))),multiply(X2,X4))),inverse(multiply(multiply(X3,X1),multiply(inverse(multiply(X0,X1)),multiply(X0,X1)))))) = X4
| ~ spl0_57
| ~ spl0_75 ),
inference(superposition,[],[f302,f409]) ).
fof(f521,plain,
( ! [X2,X3,X0,X1,X4] : multiply(X2,inverse(multiply(inverse(multiply(inverse(multiply(X2,multiply(X3,X1))),X4)),inverse(multiply(multiply(X3,X1),multiply(inverse(multiply(X0,X1)),multiply(X0,X1))))))) = X4
| ~ spl0_2
| ~ spl0_75 ),
inference(superposition,[],[f10,f409]) ).
fof(f556,definition,
( spl0_93
<=> ! [X2,X4,X0,X3,X1] : multiply(X2,inverse(multiply(inverse(multiply(inverse(multiply(X2,multiply(X3,X1))),X4)),inverse(multiply(multiply(X3,X1),multiply(inverse(multiply(X0,X1)),multiply(X0,X1))))))) = X4 ),
introduced(definition,[new_symbols(definition,[spl0_93])],[avatar_definition]) ).
fof(f557,plain,
( ! [X2,X3,X0,X1,X4] : multiply(X2,inverse(multiply(inverse(multiply(inverse(multiply(X2,multiply(X3,X1))),X4)),inverse(multiply(multiply(X3,X1),multiply(inverse(multiply(X0,X1)),multiply(X0,X1))))))) = X4
| ~ spl0_93 ),
inference(avatar_component_clause,[],[f556]) ).
fof(f558,plain,
( spl0_93
| ~ spl0_2
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f521,f408,f9,f556]) ).
fof(f576,definition,
( spl0_98
<=> ! [X2,X4,X0,X3,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X2,multiply(X3,X1))),multiply(X2,X4))),inverse(multiply(multiply(X3,X1),multiply(inverse(multiply(X0,X1)),multiply(X0,X1)))))) = X4 ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f577,plain,
( ! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(inverse(multiply(X2,multiply(X3,X1))),multiply(X2,X4))),inverse(multiply(multiply(X3,X1),multiply(inverse(multiply(X0,X1)),multiply(X0,X1)))))) = X4
| ~ spl0_98 ),
inference(avatar_component_clause,[],[f576]) ).
fof(f578,plain,
( spl0_98
| ~ spl0_57
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f516,f408,f301,f576]) ).
fof(f581,definition,
( spl0_99
<=> ! [X3,X4,X0,X5,X2,X1] : multiply(inverse(multiply(X3,X4)),multiply(X3,multiply(X5,X2))) = multiply(inverse(multiply(inverse(multiply(X5,X1)),X4)),multiply(inverse(multiply(X0,X1)),multiply(X0,X2))) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f582,plain,
( ! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(X3,X4)),multiply(X3,multiply(X5,X2))) = multiply(inverse(multiply(inverse(multiply(X5,X1)),X4)),multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))
| ~ spl0_99 ),
inference(avatar_component_clause,[],[f581]) ).
fof(f583,plain,
( spl0_99
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f489,f408,f581]) ).
fof(f593,definition,
( spl0_102
<=> ! [X4,X0,X3,X2,X1] : multiply(inverse(multiply(X1,inverse(multiply(X2,multiply(inverse(X2),X2))))),multiply(X1,X3)) = multiply(X0,multiply(inverse(multiply(inverse(multiply(X4,X2)),multiply(X4,X0))),X3)) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f594,plain,
( ! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X1,inverse(multiply(X2,multiply(inverse(X2),X2))))),multiply(X1,X3)) = multiply(X0,multiply(inverse(multiply(inverse(multiply(X4,X2)),multiply(X4,X0))),X3))
| ~ spl0_102 ),
inference(avatar_component_clause,[],[f593]) ).
fof(f595,plain,
( spl0_102
| ~ spl0_57
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f484,f408,f301,f593]) ).
fof(f605,definition,
( spl0_105
<=> ! [X2,X3,X4,X0,X5,X1] : multiply(inverse(multiply(X3,multiply(X4,X2))),multiply(X3,X5)) = multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))),multiply(inverse(multiply(X4,X1)),X5)) ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f606,plain,
( ! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(X3,multiply(X4,X2))),multiply(X3,X5)) = multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))),multiply(inverse(multiply(X4,X1)),X5))
| ~ spl0_105 ),
inference(avatar_component_clause,[],[f605]) ).
fof(f607,plain,
( spl0_105
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f481,f408,f605]) ).
fof(f617,definition,
( spl0_108
<=> ! [X4,X0,X3,X2,X1] : multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),X0)),inverse(multiply(X3,multiply(inverse(X3),X3))))))),multiply(X1,X4)) = multiply(inverse(X0),multiply(X2,X4)) ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f618,plain,
( ! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),X0)),inverse(multiply(X3,multiply(inverse(X3),X3))))))),multiply(X1,X4)) = multiply(inverse(X0),multiply(X2,X4))
| ~ spl0_108 ),
inference(avatar_component_clause,[],[f617]) ).
fof(f619,plain,
( spl0_108
| ~ spl0_2
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f477,f408,f9,f617]) ).
fof(f774,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] : multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),X4)),X0)),inverse(multiply(X4,multiply(inverse(X4),X4))))))),multiply(X1,multiply(X2,X5))) = multiply(inverse(X0),multiply(inverse(multiply(X6,X3)),multiply(X6,X5)))
| ~ spl0_2
| ~ spl0_99 ),
inference(superposition,[],[f582,f10]) ).
fof(f1100,plain,
( ! [X2,X3,X0,X6,X5] : multiply(inverse(X0),multiply(inverse(multiply(X6,X3)),multiply(X6,X5))) = multiply(inverse(X0),multiply(inverse(multiply(X2,X3)),multiply(X2,X5)))
| ~ spl0_2
| ~ spl0_99
| ~ spl0_108 ),
inference(forward_demodulation,[],[f774,f618]) ).
fof(f1236,definition,
( spl0_191
<=> ! [X5,X4,X0,X3,X2] : multiply(inverse(X0),multiply(inverse(multiply(X5,X3)),multiply(X5,X4))) = multiply(inverse(X0),multiply(inverse(multiply(X2,X3)),multiply(X2,X4))) ),
introduced(definition,[new_symbols(definition,[spl0_191])],[avatar_definition]) ).
fof(f1237,plain,
( ! [X2,X3,X0,X4,X5] : multiply(inverse(X0),multiply(inverse(multiply(X5,X3)),multiply(X5,X4))) = multiply(inverse(X0),multiply(inverse(multiply(X2,X3)),multiply(X2,X4)))
| ~ spl0_191 ),
inference(avatar_component_clause,[],[f1236]) ).
fof(f1239,plain,
( spl0_191
| ~ spl0_2
| ~ spl0_99
| ~ spl0_108 ),
inference(avatar_split_clause,[],[f1100,f617,f581,f9,f1236]) ).
fof(f1284,plain,
( ! [X0,X6,X7,X4,X5] : multiply(X0,multiply(inverse(multiply(X4,X5)),multiply(X4,X6))) = multiply(X0,multiply(inverse(multiply(X7,X5)),multiply(X7,X6)))
| ~ spl0_8
| ~ spl0_191 ),
inference(superposition,[],[f1237,f61]) ).
fof(f1565,definition,
( spl0_228
<=> ! [X5,X4,X0,X6,X3] : multiply(X0,multiply(inverse(multiply(X3,X4)),multiply(X3,X5))) = multiply(X0,multiply(inverse(multiply(X6,X4)),multiply(X6,X5))) ),
introduced(definition,[new_symbols(definition,[spl0_228])],[avatar_definition]) ).
fof(f1566,plain,
( ! [X3,X0,X6,X4,X5] : multiply(X0,multiply(inverse(multiply(X3,X4)),multiply(X3,X5))) = multiply(X0,multiply(inverse(multiply(X6,X4)),multiply(X6,X5)))
| ~ spl0_228 ),
inference(avatar_component_clause,[],[f1565]) ).
fof(f1568,plain,
( spl0_228
| ~ spl0_8
| ~ spl0_191 ),
inference(avatar_split_clause,[],[f1284,f1236,f60,f1565]) ).
fof(f2032,plain,
( ! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(X1,multiply(X2,X3))),multiply(X1,multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(X4,multiply(inverse(X4),X4)))))))) = multiply(inverse(multiply(inverse(multiply(X5,X4)),multiply(X5,X3))),X0)
| ~ spl0_12
| ~ spl0_105 ),
inference(superposition,[],[f606,f77]) ).
fof(f2119,plain,
( ! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(X0,multiply(X1,X2))),multiply(X0,multiply(X1,X3))) = multiply(inverse(multiply(X4,multiply(X5,X2))),multiply(X4,multiply(X5,X3)))
| ~ spl0_99
| ~ spl0_105 ),
inference(superposition,[],[f582,f606]) ).
fof(f2264,definition,
( spl0_280
<=> ! [X3,X4,X0,X5,X2,X1] : multiply(inverse(multiply(X0,multiply(X1,X2))),multiply(X0,multiply(X1,X3))) = multiply(inverse(multiply(X4,multiply(X5,X2))),multiply(X4,multiply(X5,X3))) ),
introduced(definition,[new_symbols(definition,[spl0_280])],[avatar_definition]) ).
fof(f2265,plain,
( ! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(X0,multiply(X1,X2))),multiply(X0,multiply(X1,X3))) = multiply(inverse(multiply(X4,multiply(X5,X2))),multiply(X4,multiply(X5,X3)))
| ~ spl0_280 ),
inference(avatar_component_clause,[],[f2264]) ).
fof(f2266,plain,
( spl0_280
| ~ spl0_99
| ~ spl0_105 ),
inference(avatar_split_clause,[],[f2119,f605,f581,f2264]) ).
fof(f2389,plain,
( ! [X2,X3,X0,X4,X5] : multiply(inverse(multiply(inverse(multiply(X5,X4)),multiply(X5,X3))),X0) = multiply(inverse(multiply(inverse(multiply(X2,X4)),multiply(X2,X3))),X0)
| ~ spl0_12
| ~ spl0_31
| ~ spl0_105 ),
inference(forward_demodulation,[],[f2032,f166]) ).
fof(f2617,definition,
( spl0_364
<=> ! [X5,X4,X0,X3,X2] : multiply(inverse(multiply(inverse(multiply(X5,X4)),multiply(X5,X3))),X0) = multiply(inverse(multiply(inverse(multiply(X2,X4)),multiply(X2,X3))),X0) ),
introduced(definition,[new_symbols(definition,[spl0_364])],[avatar_definition]) ).
fof(f2618,plain,
( ! [X2,X3,X0,X4,X5] : multiply(inverse(multiply(inverse(multiply(X5,X4)),multiply(X5,X3))),X0) = multiply(inverse(multiply(inverse(multiply(X2,X4)),multiply(X2,X3))),X0)
| ~ spl0_364 ),
inference(avatar_component_clause,[],[f2617]) ).
fof(f2619,plain,
( spl0_364
| ~ spl0_12
| ~ spl0_31
| ~ spl0_105 ),
inference(avatar_split_clause,[],[f2389,f605,f165,f76,f2617]) ).
fof(f5247,plain,
( ! [X2,X3,X0,X1,X4,X5] : multiply(X0,multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X0))),X3)) = multiply(X4,multiply(inverse(multiply(inverse(multiply(X5,X2)),multiply(X5,X4))),X3))
| ~ spl0_57
| ~ spl0_102 ),
inference(superposition,[],[f594,f302]) ).
fof(f6037,definition,
( spl0_819
<=> ! [X5,X3,X0,X6,X2,X1] : multiply(X0,multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X0))),X3)) = multiply(X5,multiply(inverse(multiply(inverse(multiply(X6,X2)),multiply(X6,X5))),X3)) ),
introduced(definition,[new_symbols(definition,[spl0_819])],[avatar_definition]) ).
fof(f6038,plain,
( ! [X2,X3,X0,X1,X6,X5] : multiply(X0,multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X0))),X3)) = multiply(X5,multiply(inverse(multiply(inverse(multiply(X6,X2)),multiply(X6,X5))),X3))
| ~ spl0_819 ),
inference(avatar_component_clause,[],[f6037]) ).
fof(f6100,plain,
( spl0_819
| ~ spl0_57
| ~ spl0_102 ),
inference(avatar_split_clause,[],[f5247,f593,f301,f6037]) ).
fof(f6264,plain,
( ! [X2,X3,X0,X1,X6,X4,X5] : multiply(X1,multiply(inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(multiply(inverse(multiply(X3,X4)),X0)),inverse(multiply(X4,multiply(inverse(X4),X4))))))),multiply(X2,X1))),X5)) = multiply(X6,multiply(inverse(multiply(inverse(X0),multiply(X3,X6))),X5))
| ~ spl0_2
| ~ spl0_819 ),
inference(superposition,[],[f6038,f10]) ).
fof(f6936,plain,
( ! [X3,X0,X1,X6,X5] : multiply(X6,multiply(inverse(multiply(inverse(X0),multiply(X3,X6))),X5)) = multiply(X1,multiply(inverse(multiply(inverse(X0),multiply(X3,X1))),X5))
| ~ spl0_2
| ~ spl0_108
| ~ spl0_819 ),
inference(forward_demodulation,[],[f6264,f618]) ).
fof(f6950,definition,
( spl0_951
<=> ! [X0,X8,X3,X1,X7] : multiply(X8,multiply(inverse(multiply(inverse(X0),multiply(X3,X8))),X7)) = multiply(X1,multiply(inverse(multiply(inverse(X0),multiply(X3,X1))),X7)) ),
introduced(definition,[new_symbols(definition,[spl0_951])],[avatar_definition]) ).
fof(f6951,plain,
( ! [X3,X0,X1,X8,X7] : multiply(X8,multiply(inverse(multiply(inverse(X0),multiply(X3,X8))),X7)) = multiply(X1,multiply(inverse(multiply(inverse(X0),multiply(X3,X1))),X7))
| ~ spl0_951 ),
inference(avatar_component_clause,[],[f6950]) ).
fof(f6953,plain,
( spl0_951
| ~ spl0_2
| ~ spl0_108
| ~ spl0_819 ),
inference(avatar_split_clause,[],[f6936,f6037,f617,f9,f6950]) ).
fof(f7107,plain,
( ! [X2,X3,X0,X1,X4,X5] : multiply(X2,multiply(inverse(multiply(X0,multiply(X1,X2))),multiply(X0,X3))) = multiply(X4,multiply(inverse(multiply(inverse(X5),multiply(X1,X4))),multiply(inverse(X5),X3)))
| ~ spl0_75
| ~ spl0_951 ),
inference(superposition,[],[f6951,f409]) ).
fof(f7515,definition,
( spl0_1005
<=> ! [X5,X4,X0,X3,X2,X1] : multiply(X4,multiply(inverse(multiply(X5,multiply(X2,X4))),multiply(X5,X3))) = multiply(X0,multiply(inverse(multiply(inverse(X1),multiply(X2,X0))),multiply(inverse(X1),X3))) ),
introduced(definition,[new_symbols(definition,[spl0_1005])],[avatar_definition]) ).
fof(f7516,plain,
( ! [X2,X3,X0,X1,X4,X5] : multiply(X4,multiply(inverse(multiply(X5,multiply(X2,X4))),multiply(X5,X3))) = multiply(X0,multiply(inverse(multiply(inverse(X1),multiply(X2,X0))),multiply(inverse(X1),X3)))
| ~ spl0_1005 ),
inference(avatar_component_clause,[],[f7515]) ).
fof(f7547,plain,
( spl0_1005
| ~ spl0_75
| ~ spl0_951 ),
inference(avatar_split_clause,[],[f7107,f6950,f408,f7515]) ).
fof(f10551,plain,
( ! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(X1,X0)),multiply(X1,inverse(X2)))),inverse(multiply(X0,multiply(inverse(X0),X0)))) = X2
| ~ spl0_12
| ~ spl0_77 ),
inference(superposition,[],[f77,f417]) ).
fof(f10823,definition,
( spl0_1296
<=> ! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(X1,X0)),multiply(X1,inverse(X2)))),inverse(multiply(X0,multiply(inverse(X0),X0)))) = X2 ),
introduced(definition,[new_symbols(definition,[spl0_1296])],[avatar_definition]) ).
fof(f10824,plain,
( ! [X2,X0,X1] : multiply(inverse(multiply(inverse(multiply(X1,X0)),multiply(X1,inverse(X2)))),inverse(multiply(X0,multiply(inverse(X0),X0)))) = X2
| ~ spl0_1296 ),
inference(avatar_component_clause,[],[f10823]) ).
fof(f10825,plain,
( spl0_1296
| ~ spl0_12
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f10551,f416,f76,f10823]) ).
fof(f11546,plain,
( ! [X2,X3,X0,X4] : multiply(inverse(X0),X0) = multiply(X3,multiply(inverse(multiply(inverse(multiply(X4,X2)),multiply(X4,X3))),inverse(multiply(X2,multiply(inverse(X2),X2)))))
| ~ spl0_819
| ~ spl0_1296 ),
inference(superposition,[],[f6038,f10824]) ).
fof(f11761,definition,
( spl0_1480
<=> ! [X0,X3,X2,X1] : multiply(inverse(X0),X0) = multiply(X3,multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X3))),inverse(multiply(X2,multiply(inverse(X2),X2))))) ),
introduced(definition,[new_symbols(definition,[spl0_1480])],[avatar_definition]) ).
fof(f11762,plain,
( ! [X2,X3,X0,X1] : multiply(inverse(X0),X0) = multiply(X3,multiply(inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X3))),inverse(multiply(X2,multiply(inverse(X2),X2)))))
| ~ spl0_1480 ),
inference(avatar_component_clause,[],[f11761]) ).
fof(f11769,plain,
( spl0_1480
| ~ spl0_819
| ~ spl0_1296 ),
inference(avatar_split_clause,[],[f11546,f10823,f6037,f11761]) ).
fof(f12187,plain,
( ! [X0,X1] : multiply(inverse(X1),X1) = multiply(inverse(X0),X0)
| ~ spl0_1296
| ~ spl0_1480 ),
inference(superposition,[],[f11762,f10824]) ).
fof(f12464,plain,
( ! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(inverse(multiply(X3,X4)),multiply(X3,inverse(multiply(X1,X2))))),inverse(multiply(X4,multiply(inverse(X4),X4)))) = multiply(X1,inverse(multiply(inverse(multiply(inverse(X0),X0)),inverse(multiply(X2,multiply(inverse(X2),X2))))))
| ~ spl0_2
| ~ spl0_1480 ),
inference(superposition,[],[f10,f11762]) ).
fof(f12472,plain,
( ! [X2,X3,X0,X1,X4,X5] : multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X4,X5)),multiply(X4,inverse(multiply(inverse(multiply(X1,X2)),X3))))),inverse(multiply(X5,multiply(inverse(X5),X5))))),inverse(multiply(X2,multiply(inverse(X2),X2)))))) = inverse(multiply(inverse(multiply(inverse(X0),X0)),inverse(multiply(X3,multiply(inverse(X3),X3)))))
| ~ spl0_3
| ~ spl0_1480 ),
inference(superposition,[],[f16,f11762]) ).
fof(f12493,plain,
( ! [X2,X3,X0,X1] : multiply(X1,inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),X3)),inverse(multiply(X2,multiply(inverse(X2),X2)))))) = inverse(multiply(inverse(multiply(inverse(X0),X0)),inverse(multiply(X3,multiply(inverse(X3),X3)))))
| ~ spl0_3
| ~ spl0_57
| ~ spl0_1480 ),
inference(forward_demodulation,[],[f12472,f302]) ).
fof(f12501,plain,
( ! [X2,X0,X1] : multiply(X1,X2) = multiply(X1,inverse(multiply(inverse(multiply(inverse(X0),X0)),inverse(multiply(X2,multiply(inverse(X2),X2))))))
| ~ spl0_2
| ~ spl0_1296
| ~ spl0_1480 ),
inference(forward_demodulation,[],[f12464,f10824]) ).
fof(f13180,definition,
( spl0_1706
<=> ! [X0,X1] : multiply(inverse(X1),X1) = multiply(inverse(X0),X0) ),
introduced(definition,[new_symbols(definition,[spl0_1706])],[avatar_definition]) ).
fof(f13181,plain,
( ! [X0,X1] : multiply(inverse(X1),X1) = multiply(inverse(X0),X0)
| ~ spl0_1706 ),
inference(avatar_component_clause,[],[f13180]) ).
fof(f13183,plain,
( spl0_1706
| ~ spl0_1296
| ~ spl0_1480 ),
inference(avatar_split_clause,[],[f12187,f11761,f10823,f13180]) ).
fof(f13576,plain,
( ! [X3,X0] : inverse(multiply(inverse(multiply(inverse(X0),X0)),inverse(multiply(X3,multiply(inverse(X3),X3))))) = X3
| ~ spl0_2
| ~ spl0_3
| ~ spl0_57
| ~ spl0_1480 ),
inference(forward_demodulation,[],[f12493,f10]) ).
fof(f13606,definition,
( spl0_1809
<=> ! [X2,X0,X1] : multiply(X1,X2) = multiply(X1,inverse(multiply(inverse(multiply(inverse(X0),X0)),inverse(multiply(X2,multiply(inverse(X2),X2)))))) ),
introduced(definition,[new_symbols(definition,[spl0_1809])],[avatar_definition]) ).
fof(f13607,plain,
( ! [X2,X0,X1] : multiply(X1,X2) = multiply(X1,inverse(multiply(inverse(multiply(inverse(X0),X0)),inverse(multiply(X2,multiply(inverse(X2),X2))))))
| ~ spl0_1809 ),
inference(avatar_component_clause,[],[f13606]) ).
fof(f13608,plain,
( spl0_1809
| ~ spl0_2
| ~ spl0_1296
| ~ spl0_1480 ),
inference(avatar_split_clause,[],[f12501,f11761,f10823,f9,f13606]) ).
fof(f13647,definition,
( spl0_1819
<=> ! [X0,X3] : inverse(multiply(inverse(multiply(inverse(X0),X0)),inverse(multiply(X3,multiply(inverse(X3),X3))))) = X3 ),
introduced(definition,[new_symbols(definition,[spl0_1819])],[avatar_definition]) ).
fof(f13648,plain,
( ! [X3,X0] : inverse(multiply(inverse(multiply(inverse(X0),X0)),inverse(multiply(X3,multiply(inverse(X3),X3))))) = X3
| ~ spl0_1819 ),
inference(avatar_component_clause,[],[f13647]) ).
fof(f13649,plain,
( spl0_1819
| ~ spl0_2
| ~ spl0_3
| ~ spl0_57
| ~ spl0_1480 ),
inference(avatar_split_clause,[],[f13576,f11761,f301,f15,f9,f13647]) ).
fof(f13919,plain,
( ! [X2,X3,X0,X1] : multiply(X1,multiply(inverse(X0),X0)) = multiply(X1,multiply(inverse(multiply(X2,X3)),multiply(X2,X3)))
| ~ spl0_228
| ~ spl0_1706 ),
inference(superposition,[],[f1566,f13181]) ).
fof(f13926,plain,
( ! [X2,X0] : multiply(inverse(multiply(inverse(X0),X0)),inverse(multiply(inverse(X2),multiply(inverse(inverse(X2)),inverse(X2))))) = X2
| ~ spl0_1296
| ~ spl0_1706 ),
inference(superposition,[],[f10824,f13181]) ).
fof(f14329,definition,
( spl0_1890
<=> ! [X2,X0] : multiply(inverse(multiply(inverse(X0),X0)),inverse(multiply(inverse(X2),multiply(inverse(inverse(X2)),inverse(X2))))) = X2 ),
introduced(definition,[new_symbols(definition,[spl0_1890])],[avatar_definition]) ).
fof(f14330,plain,
( ! [X2,X0] : multiply(inverse(multiply(inverse(X0),X0)),inverse(multiply(inverse(X2),multiply(inverse(inverse(X2)),inverse(X2))))) = X2
| ~ spl0_1890 ),
inference(avatar_component_clause,[],[f14329]) ).
fof(f14331,plain,
( spl0_1890
| ~ spl0_1296
| ~ spl0_1706 ),
inference(avatar_split_clause,[],[f13926,f13180,f10823,f14329]) ).
fof(f14342,definition,
( spl0_1893
<=> ! [X0,X3,X2,X1] : multiply(X1,multiply(inverse(X0),X0)) = multiply(X1,multiply(inverse(multiply(X2,X3)),multiply(X2,X3))) ),
introduced(definition,[new_symbols(definition,[spl0_1893])],[avatar_definition]) ).
fof(f14343,plain,
( ! [X2,X3,X0,X1] : multiply(X1,multiply(inverse(X0),X0)) = multiply(X1,multiply(inverse(multiply(X2,X3)),multiply(X2,X3)))
| ~ spl0_1893 ),
inference(avatar_component_clause,[],[f14342]) ).
fof(f14344,plain,
( spl0_1893
| ~ spl0_228
| ~ spl0_1706 ),
inference(avatar_split_clause,[],[f13919,f13180,f1565,f14342]) ).
fof(f14457,plain,
( ! [X2,X0,X1] : inverse(multiply(inverse(multiply(inverse(X1),X1)),inverse(multiply(X2,multiply(inverse(X0),X0))))) = X2
| ~ spl0_1706
| ~ spl0_1819 ),
inference(superposition,[],[f13648,f13181]) ).
fof(f14756,definition,
( spl0_1964
<=> ! [X2,X0,X1] : inverse(multiply(inverse(multiply(inverse(X1),X1)),inverse(multiply(X2,multiply(inverse(X0),X0))))) = X2 ),
introduced(definition,[new_symbols(definition,[spl0_1964])],[avatar_definition]) ).
fof(f14757,plain,
( ! [X2,X0,X1] : inverse(multiply(inverse(multiply(inverse(X1),X1)),inverse(multiply(X2,multiply(inverse(X0),X0))))) = X2
| ~ spl0_1964 ),
inference(avatar_component_clause,[],[f14756]) ).
fof(f14758,plain,
( spl0_1964
| ~ spl0_1706
| ~ spl0_1819 ),
inference(avatar_split_clause,[],[f14457,f13647,f13180,f14756]) ).
fof(f15390,plain,
( ! [X2,X0,X1] : multiply(X1,multiply(inverse(X2),X2)) = multiply(X1,multiply(inverse(X0),X0))
| ~ spl0_12
| ~ spl0_1893 ),
inference(superposition,[],[f14343,f77]) ).
fof(f16390,definition,
( spl0_2181
<=> ! [X2,X0,X1] : multiply(X0,multiply(inverse(X1),X1)) = multiply(X0,multiply(inverse(X2),X2)) ),
introduced(definition,[new_symbols(definition,[spl0_2181])],[avatar_definition]) ).
fof(f16391,plain,
( ! [X2,X0,X1] : multiply(X0,multiply(inverse(X1),X1)) = multiply(X0,multiply(inverse(X2),X2))
| ~ spl0_2181 ),
inference(avatar_component_clause,[],[f16390]) ).
fof(f16427,plain,
( spl0_2181
| ~ spl0_12
| ~ spl0_1893 ),
inference(avatar_split_clause,[],[f15390,f14342,f76,f16390]) ).
fof(f17019,plain,
( ! [X2,X0,X1] : multiply(inverse(X2),X2) = multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X1),X1))
| ~ spl0_1706
| ~ spl0_2181 ),
inference(superposition,[],[f13181,f16391]) ).
fof(f17118,definition,
( spl0_2220
<=> ! [X2,X0,X1] : multiply(inverse(X2),X2) = multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X1),X1)) ),
introduced(definition,[new_symbols(definition,[spl0_2220])],[avatar_definition]) ).
fof(f17119,plain,
( ! [X2,X0,X1] : multiply(inverse(X2),X2) = multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X1),X1))
| ~ spl0_2220 ),
inference(avatar_component_clause,[],[f17118]) ).
fof(f17120,plain,
( spl0_2220
| ~ spl0_1706
| ~ spl0_2181 ),
inference(avatar_split_clause,[],[f17019,f16390,f13180,f17118]) ).
fof(f20057,plain,
( ! [X2,X0,X1] : multiply(inverse(multiply(inverse(X1),X1)),inverse(multiply(inverse(X2),multiply(inverse(X0),X0)))) = X2
| ~ spl0_1706
| ~ spl0_1890 ),
inference(superposition,[],[f14330,f13181]) ).
fof(f20059,plain,
( ! [X2,X0,X1] : multiply(inverse(X2),X2) = multiply(inverse(multiply(inverse(X1),X1)),inverse(multiply(inverse(X0),X0)))
| ~ spl0_1890
| ~ spl0_2220 ),
inference(superposition,[],[f14330,f17119]) ).
fof(f20309,definition,
( spl0_2640
<=> ! [X2,X0,X1] : multiply(inverse(X2),X2) = multiply(inverse(multiply(inverse(X1),X1)),inverse(multiply(inverse(X0),X0))) ),
introduced(definition,[new_symbols(definition,[spl0_2640])],[avatar_definition]) ).
fof(f20310,plain,
( ! [X2,X0,X1] : multiply(inverse(X2),X2) = multiply(inverse(multiply(inverse(X1),X1)),inverse(multiply(inverse(X0),X0)))
| ~ spl0_2640 ),
inference(avatar_component_clause,[],[f20309]) ).
fof(f20321,definition,
( spl0_2643
<=> ! [X2,X0,X1] : multiply(inverse(multiply(inverse(X2),X2)),inverse(multiply(inverse(X0),multiply(inverse(X1),X1)))) = X0 ),
introduced(definition,[new_symbols(definition,[spl0_2643])],[avatar_definition]) ).
fof(f20322,plain,
( ! [X2,X0,X1] : multiply(inverse(multiply(inverse(X2),X2)),inverse(multiply(inverse(X0),multiply(inverse(X1),X1)))) = X0
| ~ spl0_2643 ),
inference(avatar_component_clause,[],[f20321]) ).
fof(f20324,plain,
( spl0_2640
| ~ spl0_1890
| ~ spl0_2220 ),
inference(avatar_split_clause,[],[f20059,f17118,f14329,f20309]) ).
fof(f20329,plain,
( spl0_2643
| ~ spl0_1706
| ~ spl0_1890 ),
inference(avatar_split_clause,[],[f20057,f14329,f13180,f20321]) ).
fof(f21309,plain,
( ! [X2,X0,X1] : inverse(multiply(inverse(X2),X2)) = multiply(inverse(X1),inverse(multiply(inverse(multiply(inverse(X0),X0)),inverse(multiply(X1,multiply(inverse(X1),X1))))))
| ~ spl0_2
| ~ spl0_2640 ),
inference(superposition,[],[f10,f20310]) ).
fof(f21628,plain,
( ! [X2,X1] : multiply(inverse(X1),X1) = inverse(multiply(inverse(X2),X2))
| ~ spl0_2
| ~ spl0_1809
| ~ spl0_2640 ),
inference(forward_demodulation,[],[f21309,f13607]) ).
fof(f22291,definition,
( spl0_2938
<=> ! [X4,X1] : multiply(inverse(X1),X1) = inverse(multiply(inverse(X4),X4)) ),
introduced(definition,[new_symbols(definition,[spl0_2938])],[avatar_definition]) ).
fof(f22292,plain,
( ! [X1,X4] : multiply(inverse(X1),X1) = inverse(multiply(inverse(X4),X4))
| ~ spl0_2938 ),
inference(avatar_component_clause,[],[f22291]) ).
fof(f22309,plain,
( spl0_2938
| ~ spl0_2
| ~ spl0_1809
| ~ spl0_2640 ),
inference(avatar_split_clause,[],[f21628,f20309,f13606,f9,f22291]) ).
fof(f22317,plain,
( ! [X2,X0,X1] : inverse(multiply(inverse(X2),X2)) = multiply(multiply(inverse(X0),X0),multiply(inverse(X1),X1))
| ~ spl0_2938 ),
inference(superposition,[],[f22292,f22292]) ).
fof(f22358,plain,
( ! [X2,X0,X1] : multiply(inverse(X1),X1) = inverse(multiply(multiply(inverse(X0),X0),multiply(inverse(X2),X2)))
| ~ spl0_2938 ),
inference(superposition,[],[f22292,f22292]) ).
fof(f22364,plain,
( ! [X0,X1] : multiply(inverse(X1),X1) = inverse(inverse(multiply(inverse(X0),X0)))
| ~ spl0_2938 ),
inference(superposition,[],[f22292,f22292]) ).
fof(f22411,plain,
( ! [X2,X0] : inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(X2,multiply(inverse(X2),X2))))) = X2
| ~ spl0_1819
| ~ spl0_2938 ),
inference(superposition,[],[f13648,f22292]) ).
fof(f22632,plain,
( ! [X2,X3,X0] : inverse(multiply(multiply(inverse(X0),X0),inverse(multiply(X2,multiply(inverse(X3),X3))))) = X2
| ~ spl0_1964
| ~ spl0_2938 ),
inference(superposition,[],[f14757,f22292]) ).
fof(f22640,plain,
( ! [X2,X3,X0] : multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(X2),multiply(inverse(X3),X3)))) = X2
| ~ spl0_2643
| ~ spl0_2938 ),
inference(superposition,[],[f20322,f22292]) ).
fof(f23011,definition,
( spl0_3011
<=> ! [X2,X0,X3] : multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(X2),multiply(inverse(X3),X3)))) = X2 ),
introduced(definition,[new_symbols(definition,[spl0_3011])],[avatar_definition]) ).
fof(f23012,plain,
( ! [X2,X3,X0] : multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(X2),multiply(inverse(X3),X3)))) = X2
| ~ spl0_3011 ),
inference(avatar_component_clause,[],[f23011]) ).
fof(f23013,plain,
( spl0_3011
| ~ spl0_2643
| ~ spl0_2938 ),
inference(avatar_split_clause,[],[f22640,f22291,f20321,f23011]) ).
fof(f23025,definition,
( spl0_3014
<=> ! [X2,X0,X3] : inverse(multiply(multiply(inverse(X0),X0),inverse(multiply(X2,multiply(inverse(X3),X3))))) = X2 ),
introduced(definition,[new_symbols(definition,[spl0_3014])],[avatar_definition]) ).
fof(f23026,plain,
( ! [X2,X3,X0] : inverse(multiply(multiply(inverse(X0),X0),inverse(multiply(X2,multiply(inverse(X3),X3))))) = X2
| ~ spl0_3014 ),
inference(avatar_component_clause,[],[f23025]) ).
fof(f23027,plain,
( spl0_3014
| ~ spl0_1964
| ~ spl0_2938 ),
inference(avatar_split_clause,[],[f22632,f22291,f14756,f23025]) ).
fof(f23409,definition,
( spl0_3107
<=> ! [X0,X3] : inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(X3,multiply(inverse(X3),X3))))) = X3 ),
introduced(definition,[new_symbols(definition,[spl0_3107])],[avatar_definition]) ).
fof(f23410,plain,
( ! [X3,X0] : inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(X3,multiply(inverse(X3),X3))))) = X3
| ~ spl0_3107 ),
inference(avatar_component_clause,[],[f23409]) ).
fof(f23562,plain,
( spl0_3107
| ~ spl0_1819
| ~ spl0_2938 ),
inference(avatar_split_clause,[],[f22411,f22291,f13647,f23409]) ).
fof(f23636,definition,
( spl0_3156
<=> ! [X0,X1] : multiply(inverse(X1),X1) = inverse(inverse(multiply(inverse(X0),X0))) ),
introduced(definition,[new_symbols(definition,[spl0_3156])],[avatar_definition]) ).
fof(f23637,plain,
( ! [X0,X1] : multiply(inverse(X1),X1) = inverse(inverse(multiply(inverse(X0),X0)))
| ~ spl0_3156 ),
inference(avatar_component_clause,[],[f23636]) ).
fof(f23638,plain,
( spl0_3156
| ~ spl0_2938 ),
inference(avatar_split_clause,[],[f22364,f22291,f23636]) ).
fof(f23653,definition,
( spl0_3160
<=> ! [X2,X0,X1] : multiply(inverse(X1),X1) = inverse(multiply(multiply(inverse(X0),X0),multiply(inverse(X2),X2))) ),
introduced(definition,[new_symbols(definition,[spl0_3160])],[avatar_definition]) ).
fof(f23654,plain,
( ! [X2,X0,X1] : multiply(inverse(X1),X1) = inverse(multiply(multiply(inverse(X0),X0),multiply(inverse(X2),X2)))
| ~ spl0_3160 ),
inference(avatar_component_clause,[],[f23653]) ).
fof(f23655,plain,
( spl0_3160
| ~ spl0_2938 ),
inference(avatar_split_clause,[],[f22358,f22291,f23653]) ).
fof(f23691,definition,
( spl0_3169
<=> ! [X2,X0,X1] : inverse(multiply(inverse(X2),X2)) = multiply(multiply(inverse(X0),X0),multiply(inverse(X1),X1)) ),
introduced(definition,[new_symbols(definition,[spl0_3169])],[avatar_definition]) ).
fof(f23692,plain,
( ! [X2,X0,X1] : inverse(multiply(inverse(X2),X2)) = multiply(multiply(inverse(X0),X0),multiply(inverse(X1),X1))
| ~ spl0_3169 ),
inference(avatar_component_clause,[],[f23691]) ).
fof(f23693,plain,
( spl0_3169
| ~ spl0_2938 ),
inference(avatar_split_clause,[],[f22317,f22291,f23691]) ).
fof(f38978,plain,
( ! [X2,X3,X0,X1] : multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(X3),inverse(multiply(multiply(inverse(X0),X0),multiply(inverse(X1),X1)))))) = X3
| ~ spl0_3011
| ~ spl0_3160 ),
inference(superposition,[],[f23012,f23654]) ).
fof(f40227,definition,
( spl0_5684
<=> ! [X0,X3,X2,X1] : multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(X3),inverse(multiply(multiply(inverse(X0),X0),multiply(inverse(X1),X1)))))) = X3 ),
introduced(definition,[new_symbols(definition,[spl0_5684])],[avatar_definition]) ).
fof(f40228,plain,
( ! [X2,X3,X0,X1] : multiply(multiply(inverse(X2),X2),inverse(multiply(inverse(X3),inverse(multiply(multiply(inverse(X0),X0),multiply(inverse(X1),X1)))))) = X3
| ~ spl0_5684 ),
inference(avatar_component_clause,[],[f40227]) ).
fof(f40229,plain,
( spl0_5684
| ~ spl0_3011
| ~ spl0_3160 ),
inference(avatar_split_clause,[],[f38978,f23653,f23011,f40227]) ).
fof(f41172,plain,
( ! [X2,X3,X0,X1] : multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),X3)),inverse(multiply(multiply(inverse(X2),X2),multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))))))) = X3
| ~ spl0_2
| ~ spl0_3169 ),
inference(superposition,[],[f10,f23692]) ).
fof(f41173,plain,
( ! [X2,X3,X0,X1,X4] : multiply(multiply(inverse(X1),X1),inverse(multiply(inverse(X4),inverse(multiply(multiply(inverse(X2),X2),multiply(inverse(multiply(inverse(X2),X2)),multiply(inverse(X2),X2))))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),X3)),X4)),inverse(multiply(X3,multiply(inverse(X3),X3)))))
| ~ spl0_3
| ~ spl0_3169 ),
inference(superposition,[],[f16,f23692]) ).
fof(f41417,plain,
( ! [X3,X0,X4] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),X3)),X4)),inverse(multiply(X3,multiply(inverse(X3),X3))))) = X4
| ~ spl0_3
| ~ spl0_3169
| ~ spl0_5684 ),
inference(forward_demodulation,[],[f41173,f40228]) ).
fof(f41418,plain,
( ! [X3,X0] : multiply(inverse(inverse(multiply(inverse(X0),X0))),X3) = X3
| ~ spl0_2
| ~ spl0_3169
| ~ spl0_5684 ),
inference(forward_demodulation,[],[f41172,f40228]) ).
fof(f42403,definition,
( spl0_6065
<=> ! [X0,X3] : multiply(inverse(inverse(multiply(inverse(X0),X0))),X3) = X3 ),
introduced(definition,[new_symbols(definition,[spl0_6065])],[avatar_definition]) ).
fof(f42404,plain,
( ! [X3,X0] : multiply(inverse(inverse(multiply(inverse(X0),X0))),X3) = X3
| ~ spl0_6065 ),
inference(avatar_component_clause,[],[f42403]) ).
fof(f42407,definition,
( spl0_6066
<=> ! [X4,X0,X3] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),X3)),X4)),inverse(multiply(X3,multiply(inverse(X3),X3))))) = X4 ),
introduced(definition,[new_symbols(definition,[spl0_6066])],[avatar_definition]) ).
fof(f42408,plain,
( ! [X3,X0,X4] : inverse(multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),X3)),X4)),inverse(multiply(X3,multiply(inverse(X3),X3))))) = X4
| ~ spl0_6066 ),
inference(avatar_component_clause,[],[f42407]) ).
fof(f42409,plain,
( spl0_6066
| ~ spl0_3
| ~ spl0_3169
| ~ spl0_5684 ),
inference(avatar_split_clause,[],[f41417,f40227,f23691,f15,f42407]) ).
fof(f42410,plain,
( spl0_6065
| ~ spl0_2
| ~ spl0_3169
| ~ spl0_5684 ),
inference(avatar_split_clause,[],[f41418,f40227,f23691,f9,f42403]) ).
fof(f42413,plain,
( ! [X3,X4] : inverse(multiply(inverse(multiply(inverse(X3),X4)),inverse(multiply(X3,multiply(inverse(X3),X3))))) = X4
| ~ spl0_6065
| ~ spl0_6066 ),
inference(forward_demodulation,[],[f42408,f42404]) ).
fof(f42415,definition,
( spl0_6067
<=> ! [X4,X3] : inverse(multiply(inverse(multiply(inverse(X3),X4)),inverse(multiply(X3,multiply(inverse(X3),X3))))) = X4 ),
introduced(definition,[new_symbols(definition,[spl0_6067])],[avatar_definition]) ).
fof(f42416,plain,
( ! [X3,X4] : inverse(multiply(inverse(multiply(inverse(X3),X4)),inverse(multiply(X3,multiply(inverse(X3),X3))))) = X4
| ~ spl0_6067 ),
inference(avatar_component_clause,[],[f42415]) ).
fof(f42417,plain,
( spl0_6067
| ~ spl0_6065
| ~ spl0_6066 ),
inference(avatar_split_clause,[],[f42413,f42407,f42403,f42415]) ).
fof(f42489,plain,
( ! [X2,X0] : multiply(inverse(multiply(inverse(X0),X0)),X2) = X2
| ~ spl0_2938
| ~ spl0_6065 ),
inference(superposition,[],[f42404,f22292]) ).
fof(f42499,plain,
( ! [X2,X0] : multiply(multiply(inverse(X0),X0),X2) = X2
| ~ spl0_3156
| ~ spl0_6065 ),
inference(superposition,[],[f42404,f23637]) ).
fof(f42638,plain,
( ! [X2,X3,X0,X1] : multiply(inverse(multiply(X1,X2)),multiply(X1,X0)) = multiply(inverse(multiply(inverse(inverse(multiply(inverse(X3),X3))),X2)),X0)
| ~ spl0_75
| ~ spl0_6065 ),
inference(superposition,[],[f409,f42404]) ).
fof(f42654,plain,
( ! [X2,X3,X0,X1,X4] : multiply(X3,multiply(inverse(multiply(inverse(multiply(X4,X2)),multiply(X4,X3))),X0)) = multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(X2,multiply(inverse(X2),X2))))),X0)
| ~ spl0_102
| ~ spl0_6065 ),
inference(superposition,[],[f594,f42404]) ).
fof(f42668,plain,
( ! [X2,X3,X0,X1,X4] : multiply(X1,multiply(inverse(multiply(X2,X0)),multiply(X2,X3))) = multiply(X1,multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(X4),X4))),X3)))
| ~ spl0_228
| ~ spl0_6065 ),
inference(superposition,[],[f1566,f42404]) ).
fof(f42676,plain,
( ! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(inverse(multiply(X4,X2)),multiply(X4,X0))),X3) = multiply(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),X2)),X0)),X3)
| ~ spl0_364
| ~ spl0_6065 ),
inference(superposition,[],[f2618,f42404]) ).
fof(f42882,plain,
( ! [X2,X3,X0,X4] : multiply(inverse(multiply(inverse(multiply(X4,X2)),multiply(X4,X0))),X3) = multiply(inverse(multiply(inverse(X2),X0)),X3)
| ~ spl0_364
| ~ spl0_6065 ),
inference(forward_demodulation,[],[f42676,f42404]) ).
fof(f42890,plain,
( ! [X2,X3,X0,X1] : multiply(X1,multiply(inverse(multiply(X2,X0)),multiply(X2,X3))) = multiply(X1,multiply(inverse(X0),X3))
| ~ spl0_228
| ~ spl0_6065 ),
inference(forward_demodulation,[],[f42668,f42404]) ).
fof(f42904,plain,
( ! [X2,X3,X0,X4] : multiply(X2,X0) = multiply(X3,multiply(inverse(multiply(inverse(multiply(X4,X2)),multiply(X4,X3))),X0))
| ~ spl0_102
| ~ spl0_3107
| ~ spl0_6065 ),
inference(forward_demodulation,[],[f42654,f23410]) ).
fof(f42914,plain,
( ! [X2,X0,X1] : multiply(inverse(multiply(X1,X2)),multiply(X1,X0)) = multiply(inverse(X2),X0)
| ~ spl0_75
| ~ spl0_6065 ),
inference(forward_demodulation,[],[f42638,f42404]) ).
fof(f42950,definition,
( spl0_6089
<=> ! [X2,X0] : multiply(multiply(inverse(X0),X0),X2) = X2 ),
introduced(definition,[new_symbols(definition,[spl0_6089])],[avatar_definition]) ).
fof(f42951,plain,
( ! [X2,X0] : multiply(multiply(inverse(X0),X0),X2) = X2
| ~ spl0_6089 ),
inference(avatar_component_clause,[],[f42950]) ).
fof(f42952,plain,
( spl0_6089
| ~ spl0_3156
| ~ spl0_6065 ),
inference(avatar_split_clause,[],[f42499,f42403,f23636,f42950]) ).
fof(f42954,definition,
( spl0_6090
<=> ! [X2,X0] : multiply(inverse(multiply(inverse(X0),X0)),X2) = X2 ),
introduced(definition,[new_symbols(definition,[spl0_6090])],[avatar_definition]) ).
fof(f42955,plain,
( ! [X2,X0] : multiply(inverse(multiply(inverse(X0),X0)),X2) = X2
| ~ spl0_6090 ),
inference(avatar_component_clause,[],[f42954]) ).
fof(f42974,plain,
( spl0_6090
| ~ spl0_2938
| ~ spl0_6065 ),
inference(avatar_split_clause,[],[f42489,f42403,f22291,f42954]) ).
fof(f43203,definition,
( spl0_6146
<=> ! [X4,X0,X3,X2] : multiply(inverse(multiply(inverse(multiply(X4,X2)),multiply(X4,X0))),X3) = multiply(inverse(multiply(inverse(X2),X0)),X3) ),
introduced(definition,[new_symbols(definition,[spl0_6146])],[avatar_definition]) ).
fof(f43204,plain,
( ! [X2,X3,X0,X4] : multiply(inverse(multiply(inverse(multiply(X4,X2)),multiply(X4,X0))),X3) = multiply(inverse(multiply(inverse(X2),X0)),X3)
| ~ spl0_6146 ),
inference(avatar_component_clause,[],[f43203]) ).
fof(f43205,plain,
( spl0_6146
| ~ spl0_364
| ~ spl0_6065 ),
inference(avatar_split_clause,[],[f42882,f42403,f2617,f43203]) ).
fof(f43207,definition,
( spl0_6147
<=> ! [X0,X3,X2,X1] : multiply(X1,multiply(inverse(multiply(X2,X0)),multiply(X2,X3))) = multiply(X1,multiply(inverse(X0),X3)) ),
introduced(definition,[new_symbols(definition,[spl0_6147])],[avatar_definition]) ).
fof(f43208,plain,
( ! [X2,X3,X0,X1] : multiply(X1,multiply(inverse(multiply(X2,X0)),multiply(X2,X3))) = multiply(X1,multiply(inverse(X0),X3))
| ~ spl0_6147 ),
inference(avatar_component_clause,[],[f43207]) ).
fof(f43209,plain,
( spl0_6147
| ~ spl0_228
| ~ spl0_6065 ),
inference(avatar_split_clause,[],[f42890,f42403,f1565,f43207]) ).
fof(f43227,definition,
( spl0_6152
<=> ! [X4,X0,X3,X2] : multiply(X2,X0) = multiply(X3,multiply(inverse(multiply(inverse(multiply(X4,X2)),multiply(X4,X3))),X0)) ),
introduced(definition,[new_symbols(definition,[spl0_6152])],[avatar_definition]) ).
fof(f43228,plain,
( ! [X2,X3,X0,X4] : multiply(X2,X0) = multiply(X3,multiply(inverse(multiply(inverse(multiply(X4,X2)),multiply(X4,X3))),X0))
| ~ spl0_6152 ),
inference(avatar_component_clause,[],[f43227]) ).
fof(f43229,plain,
( spl0_6152
| ~ spl0_102
| ~ spl0_3107
| ~ spl0_6065 ),
inference(avatar_split_clause,[],[f42904,f42403,f23409,f593,f43227]) ).
fof(f43243,definition,
( spl0_6156
<=> ! [X2,X0,X1] : multiply(inverse(multiply(X1,X2)),multiply(X1,X0)) = multiply(inverse(X2),X0) ),
introduced(definition,[new_symbols(definition,[spl0_6156])],[avatar_definition]) ).
fof(f43244,plain,
( ! [X2,X0,X1] : multiply(inverse(multiply(X1,X2)),multiply(X1,X0)) = multiply(inverse(X2),X0)
| ~ spl0_6156 ),
inference(avatar_component_clause,[],[f43243]) ).
fof(f43245,plain,
( spl0_6156
| ~ spl0_75
| ~ spl0_6065 ),
inference(avatar_split_clause,[],[f42914,f42403,f408,f43243]) ).
fof(f43282,plain,
( ! [X2,X3,X0] : multiply(X2,X0) = multiply(X3,multiply(inverse(multiply(inverse(X2),X3)),X0))
| ~ spl0_6146
| ~ spl0_6152 ),
inference(forward_demodulation,[],[f43228,f43204]) ).
fof(f43298,definition,
( spl0_6161
<=> ! [X2,X0,X3] : multiply(X2,X0) = multiply(X3,multiply(inverse(multiply(inverse(X2),X3)),X0)) ),
introduced(definition,[new_symbols(definition,[spl0_6161])],[avatar_definition]) ).
fof(f43299,plain,
( ! [X2,X3,X0] : multiply(X2,X0) = multiply(X3,multiply(inverse(multiply(inverse(X2),X3)),X0))
| ~ spl0_6161 ),
inference(avatar_component_clause,[],[f43298]) ).
fof(f43300,plain,
( spl0_6161
| ~ spl0_6146
| ~ spl0_6152 ),
inference(avatar_split_clause,[],[f43282,f43227,f43203,f43298]) ).
fof(f43406,plain,
( ! [X0,X1] : inverse(inverse(multiply(X0,multiply(inverse(X1),X1)))) = X0
| ~ spl0_3014
| ~ spl0_6089 ),
inference(superposition,[],[f23026,f42951]) ).
fof(f43647,definition,
( spl0_6164
<=> ! [X0,X1] : inverse(inverse(multiply(X0,multiply(inverse(X1),X1)))) = X0 ),
introduced(definition,[new_symbols(definition,[spl0_6164])],[avatar_definition]) ).
fof(f43648,plain,
( ! [X0,X1] : inverse(inverse(multiply(X0,multiply(inverse(X1),X1)))) = X0
| ~ spl0_6164 ),
inference(avatar_component_clause,[],[f43647]) ).
fof(f43649,plain,
( spl0_6164
| ~ spl0_3014
| ~ spl0_6089 ),
inference(avatar_split_clause,[],[f43406,f42950,f23025,f43647]) ).
fof(f44102,plain,
( ! [X2,X0,X1] : multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(X2,multiply(inverse(X2),X2)))))) = inverse(multiply(inverse(X0),inverse(multiply(multiply(X1,X2),multiply(inverse(multiply(X1,X2)),multiply(X1,X2))))))
| ~ spl0_3
| ~ spl0_6090 ),
inference(superposition,[],[f16,f42955]) ).
fof(f44234,plain,
( ! [X2,X3,X0,X1,X4,X5] : multiply(X1,multiply(inverse(multiply(X2,multiply(inverse(multiply(inverse(X3),X3)),X1))),multiply(X2,X4))) = multiply(X0,multiply(inverse(multiply(inverse(X5),X0)),multiply(inverse(X5),X4)))
| ~ spl0_1005
| ~ spl0_6090 ),
inference(superposition,[],[f7516,f42955]) ).
fof(f44365,plain,
( ! [X2,X3,X1,X4,X5] : multiply(X1,multiply(inverse(multiply(X2,multiply(inverse(multiply(inverse(X3),X3)),X1))),multiply(X2,X4))) = multiply(X5,multiply(inverse(X5),X4))
| ~ spl0_1005
| ~ spl0_6090
| ~ spl0_6161 ),
inference(forward_demodulation,[],[f44234,f43299]) ).
fof(f44431,plain,
( ! [X2,X0,X1] : multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(X2,multiply(inverse(X2),X2)))))) = inverse(multiply(inverse(X0),inverse(multiply(multiply(X1,X2),multiply(inverse(X2),X2)))))
| ~ spl0_3
| ~ spl0_6090
| ~ spl0_6147 ),
inference(forward_demodulation,[],[f44102,f43208]) ).
fof(f44541,plain,
( ! [X3,X1,X4,X5] : multiply(X5,multiply(inverse(X5),X4)) = multiply(X1,multiply(inverse(multiply(inverse(multiply(inverse(X3),X3)),X1)),X4))
| ~ spl0_1005
| ~ spl0_6090
| ~ spl0_6147
| ~ spl0_6161 ),
inference(forward_demodulation,[],[f44365,f43208]) ).
fof(f44570,definition,
( spl0_6187
<=> ! [X2,X0,X1] : multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(X2,multiply(inverse(X2),X2)))))) = inverse(multiply(inverse(X0),inverse(multiply(multiply(X1,X2),multiply(inverse(X2),X2))))) ),
introduced(definition,[new_symbols(definition,[spl0_6187])],[avatar_definition]) ).
fof(f44571,plain,
( ! [X2,X0,X1] : multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(X2,multiply(inverse(X2),X2)))))) = inverse(multiply(inverse(X0),inverse(multiply(multiply(X1,X2),multiply(inverse(X2),X2)))))
| ~ spl0_6187 ),
inference(avatar_component_clause,[],[f44570]) ).
fof(f44572,plain,
( spl0_6187
| ~ spl0_3
| ~ spl0_6090
| ~ spl0_6147 ),
inference(avatar_split_clause,[],[f44431,f43207,f42954,f15,f44570]) ).
fof(f44631,plain,
( ! [X3,X4,X5] : multiply(multiply(inverse(X3),X3),X4) = multiply(X5,multiply(inverse(X5),X4))
| ~ spl0_1005
| ~ spl0_6090
| ~ spl0_6147
| ~ spl0_6161 ),
inference(forward_demodulation,[],[f44541,f43299]) ).
fof(f44666,plain,
( ! [X4,X5] : multiply(X5,multiply(inverse(X5),X4)) = X4
| ~ spl0_1005
| ~ spl0_6089
| ~ spl0_6090
| ~ spl0_6147
| ~ spl0_6161 ),
inference(forward_demodulation,[],[f44631,f42951]) ).
fof(f44677,definition,
( spl0_6197
<=> ! [X4,X0] : multiply(X0,multiply(inverse(X0),X4)) = X4 ),
introduced(definition,[new_symbols(definition,[spl0_6197])],[avatar_definition]) ).
fof(f44678,plain,
( ! [X0,X4] : multiply(X0,multiply(inverse(X0),X4)) = X4
| ~ spl0_6197 ),
inference(avatar_component_clause,[],[f44677]) ).
fof(f44681,plain,
( spl0_6197
| ~ spl0_1005
| ~ spl0_6089
| ~ spl0_6090
| ~ spl0_6147
| ~ spl0_6161 ),
inference(avatar_split_clause,[],[f44666,f43298,f43207,f42954,f42950,f7515,f44677]) ).
fof(f44728,plain,
( ! [X2,X0,X1] : multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(X2,multiply(inverse(X2),X2)))))) = multiply(multiply(X1,X2),X0)
| ~ spl0_12
| ~ spl0_6197 ),
inference(superposition,[],[f44678,f77]) ).
fof(f44729,plain,
( ! [X2,X3,X0,X1,X4] : multiply(X4,X3) = multiply(multiply(X4,X2),multiply(inverse(multiply(inverse(multiply(X0,X1)),X2)),multiply(inverse(multiply(X0,X1)),X3)))
| ~ spl0_49
| ~ spl0_6197 ),
inference(superposition,[],[f44678,f270]) ).
fof(f44735,plain,
( ! [X2,X3,X0,X1,X4,X5] : multiply(X4,multiply(X5,X3)) = multiply(multiply(X4,multiply(X5,X2)),multiply(inverse(multiply(X0,multiply(X1,X2))),multiply(X0,multiply(X1,X3))))
| ~ spl0_280
| ~ spl0_6197 ),
inference(superposition,[],[f44678,f2265]) ).
fof(f44765,plain,
( ! [X0,X1] : multiply(X1,X0) = multiply(inverse(inverse(X1)),X0)
| ~ spl0_6197 ),
inference(superposition,[],[f44678,f44678]) ).
fof(f44768,plain,
( ! [X2,X3,X0,X1] : inverse(multiply(inverse(X3),inverse(multiply(X1,multiply(inverse(X1),X1))))) = multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),X1)),X2)),X3)),inverse(multiply(X2,multiply(inverse(X2),X2))))))
| ~ spl0_3
| ~ spl0_6197 ),
inference(superposition,[],[f44678,f16]) ).
fof(f44800,plain,
( ! [X0,X1] : inverse(multiply(inverse(multiply(inverse(X1),X1)),inverse(X0))) = X0
| ~ spl0_1819
| ~ spl0_6197 ),
inference(superposition,[],[f13648,f44678]) ).
fof(f44812,plain,
( ! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(X0),multiply(X1,X2))),inverse(multiply(multiply(inverse(X1),X0),multiply(inverse(multiply(X3,X0)),multiply(X3,X0)))))) = X2
| ~ spl0_98
| ~ spl0_6197 ),
inference(superposition,[],[f577,f44678]) ).
fof(f44868,plain,
( ! [X2,X3,X0,X1,X4] : multiply(X1,multiply(inverse(multiply(X2,multiply(inverse(X3),X0))),multiply(X2,X4))) = multiply(X1,multiply(inverse(X0),multiply(X3,X4)))
| ~ spl0_228
| ~ spl0_6197 ),
inference(superposition,[],[f1566,f44678]) ).
fof(f44929,plain,
( ! [X2,X3,X0,X1,X4] : multiply(X4,X0) = multiply(inverse(multiply(X1,inverse(multiply(X2,multiply(inverse(X2),X2))))),multiply(X1,multiply(inverse(inverse(multiply(inverse(multiply(X3,X2)),multiply(X3,X4)))),X0)))
| ~ spl0_102
| ~ spl0_6197 ),
inference(superposition,[],[f594,f44678]) ).
fof(f44936,plain,
( ! [X2,X3,X0,X1,X4] : multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(multiply(X2,X3),multiply(inverse(multiply(X4,X3)),multiply(X4,X3))))))) = multiply(inverse(inverse(multiply(X1,multiply(X2,X3)))),X0)
| ~ spl0_93
| ~ spl0_6197 ),
inference(superposition,[],[f557,f44678]) ).
fof(f44937,plain,
( ! [X2,X3,X0,X1] : multiply(inverse(inverse(multiply(X1,multiply(X2,X3)))),X0) = multiply(X1,inverse(multiply(inverse(X0),inverse(multiply(multiply(X2,X3),multiply(inverse(X3),X3))))))
| ~ spl0_93
| ~ spl0_6147
| ~ spl0_6197 ),
inference(forward_demodulation,[],[f44936,f43208]) ).
fof(f44948,plain,
( ! [X2,X3,X0,X4] : multiply(X4,X0) = multiply(inverse(inverse(multiply(X2,multiply(inverse(X2),X2)))),multiply(inverse(inverse(multiply(inverse(multiply(X3,X2)),multiply(X3,X4)))),X0))
| ~ spl0_102
| ~ spl0_6156
| ~ spl0_6197 ),
inference(forward_demodulation,[],[f44929,f43244]) ).
fof(f45007,plain,
( ! [X3,X0,X1,X4] : multiply(X1,multiply(inverse(X0),multiply(X3,X4))) = multiply(X1,multiply(inverse(multiply(inverse(X3),X0)),X4))
| ~ spl0_228
| ~ spl0_6147
| ~ spl0_6197 ),
inference(forward_demodulation,[],[f44868,f43208]) ).
fof(f45055,plain,
( ! [X2,X0,X1] : inverse(multiply(inverse(multiply(inverse(X0),multiply(X1,X2))),inverse(multiply(multiply(inverse(X1),X0),multiply(inverse(X0),X0))))) = X2
| ~ spl0_98
| ~ spl0_6147
| ~ spl0_6197 ),
inference(forward_demodulation,[],[f44812,f43208]) ).
fof(f45075,plain,
( ! [X0] : inverse(inverse(X0)) = X0
| ~ spl0_1819
| ~ spl0_6090
| ~ spl0_6197 ),
inference(forward_demodulation,[],[f44800,f42955]) ).
fof(f45099,plain,
( ! [X2,X3,X0,X1] : inverse(multiply(inverse(X3),inverse(multiply(X1,multiply(inverse(X1),X1))))) = multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),X1)),X2)),X3)),inverse(X2))))
| ~ spl0_3
| ~ spl0_6197 ),
inference(forward_demodulation,[],[f44768,f44678]) ).
fof(f45103,definition,
( spl0_6207
<=> ! [X0,X1] : multiply(X1,X0) = multiply(inverse(inverse(X1)),X0) ),
introduced(definition,[new_symbols(definition,[spl0_6207])],[avatar_definition]) ).
fof(f45104,plain,
( ! [X0,X1] : multiply(X1,X0) = multiply(inverse(inverse(X1)),X0)
| ~ spl0_6207 ),
inference(avatar_component_clause,[],[f45103]) ).
fof(f45105,plain,
( spl0_6207
| ~ spl0_6197 ),
inference(avatar_split_clause,[],[f44765,f44677,f45103]) ).
fof(f45138,plain,
( ! [X2,X3,X1,X4,X5] : multiply(X4,multiply(X5,X3)) = multiply(multiply(X4,multiply(X5,X2)),multiply(inverse(multiply(X1,X2)),multiply(X1,X3)))
| ~ spl0_280
| ~ spl0_6147
| ~ spl0_6197 ),
inference(forward_demodulation,[],[f44735,f43208]) ).
fof(f45144,plain,
( ! [X2,X3,X4] : multiply(X4,X3) = multiply(multiply(X4,X2),multiply(inverse(X2),X3))
| ~ spl0_49
| ~ spl0_6147
| ~ spl0_6197 ),
inference(forward_demodulation,[],[f44729,f43208]) ).
fof(f45145,plain,
( ! [X2,X0,X1] : multiply(multiply(X1,X2),X0) = multiply(X1,inverse(multiply(inverse(X0),inverse(X2))))
| ~ spl0_12
| ~ spl0_6197 ),
inference(forward_demodulation,[],[f44728,f44678]) ).
fof(f45201,plain,
( ! [X2,X3,X0,X1] : multiply(X1,multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(X3,multiply(inverse(X3),X3))))))) = multiply(inverse(inverse(multiply(X1,multiply(X2,X3)))),X0)
| ~ spl0_93
| ~ spl0_6147
| ~ spl0_6187
| ~ spl0_6197 ),
inference(forward_demodulation,[],[f44937,f44571]) ).
fof(f45204,plain,
( ! [X2,X0,X4] : multiply(X4,X0) = multiply(inverse(inverse(multiply(X2,multiply(inverse(X2),X2)))),multiply(inverse(inverse(multiply(inverse(X2),X4))),X0))
| ~ spl0_102
| ~ spl0_6156
| ~ spl0_6197 ),
inference(forward_demodulation,[],[f44948,f43244]) ).
fof(f45234,definition,
( spl0_6219
<=> ! [X0] : inverse(inverse(X0)) = X0 ),
introduced(definition,[new_symbols(definition,[spl0_6219])],[avatar_definition]) ).
fof(f45235,plain,
( ! [X0] : inverse(inverse(X0)) = X0
| ~ spl0_6219 ),
inference(avatar_component_clause,[],[f45234]) ).
fof(f45298,definition,
( spl0_6231
<=> ! [X4,X0,X3,X1] : multiply(X1,multiply(inverse(X0),multiply(X3,X4))) = multiply(X1,multiply(inverse(multiply(inverse(X3),X0)),X4)) ),
introduced(definition,[new_symbols(definition,[spl0_6231])],[avatar_definition]) ).
fof(f45299,plain,
( ! [X3,X0,X1,X4] : multiply(X1,multiply(inverse(X0),multiply(X3,X4))) = multiply(X1,multiply(inverse(multiply(inverse(X3),X0)),X4))
| ~ spl0_6231 ),
inference(avatar_component_clause,[],[f45298]) ).
fof(f45300,plain,
( spl0_6231
| ~ spl0_228
| ~ spl0_6147
| ~ spl0_6197 ),
inference(avatar_split_clause,[],[f45007,f44677,f43207,f1565,f45298]) ).
fof(f45374,plain,
( ! [X2,X0,X1] : multiply(inverse(X1),inverse(multiply(inverse(multiply(inverse(X0),multiply(X1,X2))),inverse(multiply(X0,multiply(inverse(X0),X0)))))) = X2
| ~ spl0_98
| ~ spl0_6147
| ~ spl0_6187
| ~ spl0_6197 ),
inference(forward_demodulation,[],[f45055,f44571]) ).
fof(f45378,definition,
( spl0_6243
<=> ! [X2,X0,X1] : multiply(X0,X1) = multiply(multiply(X0,X2),multiply(inverse(X2),X1)) ),
introduced(definition,[new_symbols(definition,[spl0_6243])],[avatar_definition]) ).
fof(f45379,plain,
( ! [X2,X0,X1] : multiply(X0,X1) = multiply(multiply(X0,X2),multiply(inverse(X2),X1))
| ~ spl0_6243 ),
inference(avatar_component_clause,[],[f45378]) ).
fof(f45384,plain,
( spl0_6219
| ~ spl0_1819
| ~ spl0_6090
| ~ spl0_6197 ),
inference(avatar_split_clause,[],[f45075,f44677,f42954,f13647,f45234]) ).
fof(f45412,plain,
( ! [X2,X3,X0,X1] : multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),X1)),X2)),X3)),inverse(X2)))) = inverse(multiply(inverse(X3),inverse(X1)))
| ~ spl0_3
| ~ spl0_6197 ),
inference(forward_demodulation,[],[f45099,f44678]) ).
fof(f45436,plain,
( ! [X2,X3,X4,X5] : multiply(X4,multiply(X5,X3)) = multiply(multiply(X4,multiply(X5,X2)),multiply(inverse(X2),X3))
| ~ spl0_280
| ~ spl0_6147
| ~ spl0_6197 ),
inference(forward_demodulation,[],[f45138,f43208]) ).
fof(f45444,plain,
( spl0_6243
| ~ spl0_49
| ~ spl0_6147
| ~ spl0_6197 ),
inference(avatar_split_clause,[],[f45144,f44677,f43207,f269,f45378]) ).
fof(f45446,definition,
( spl0_6252
<=> ! [X2,X0,X1] : multiply(multiply(X1,X2),X0) = multiply(X1,inverse(multiply(inverse(X0),inverse(X2)))) ),
introduced(definition,[new_symbols(definition,[spl0_6252])],[avatar_definition]) ).
fof(f45447,plain,
( ! [X2,X0,X1] : multiply(multiply(X1,X2),X0) = multiply(X1,inverse(multiply(inverse(X0),inverse(X2))))
| ~ spl0_6252 ),
inference(avatar_component_clause,[],[f45446]) ).
fof(f45448,plain,
( spl0_6252
| ~ spl0_12
| ~ spl0_6197 ),
inference(avatar_split_clause,[],[f45145,f44677,f76,f45446]) ).
fof(f45469,plain,
( ! [X2,X3,X0,X1] : multiply(inverse(inverse(multiply(X1,multiply(X2,X3)))),X0) = multiply(X1,multiply(X2,inverse(multiply(inverse(X0),inverse(X3)))))
| ~ spl0_93
| ~ spl0_6147
| ~ spl0_6187
| ~ spl0_6197 ),
inference(forward_demodulation,[],[f45201,f44678]) ).
fof(f45470,plain,
( ! [X2,X0,X4] : multiply(X4,X0) = multiply(X2,multiply(inverse(inverse(multiply(inverse(X2),X4))),X0))
| ~ spl0_102
| ~ spl0_6156
| ~ spl0_6164
| ~ spl0_6197 ),
inference(forward_demodulation,[],[f45204,f43648]) ).
fof(f45535,plain,
( ! [X2,X1] : multiply(inverse(X1),multiply(X1,X2)) = X2
| ~ spl0_98
| ~ spl0_6067
| ~ spl0_6147
| ~ spl0_6187
| ~ spl0_6197 ),
inference(forward_demodulation,[],[f45374,f42416]) ).
fof(f45552,definition,
( spl0_6267
<=> ! [X0,X3,X2,X1] : multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),X1)),X2)),X3)),inverse(X2)))) = inverse(multiply(inverse(X3),inverse(X1))) ),
introduced(definition,[new_symbols(definition,[spl0_6267])],[avatar_definition]) ).
fof(f45553,plain,
( ! [X2,X3,X0,X1] : multiply(X0,inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(inverse(X0),X1)),X2)),X3)),inverse(X2)))) = inverse(multiply(inverse(X3),inverse(X1)))
| ~ spl0_6267 ),
inference(avatar_component_clause,[],[f45552]) ).
fof(f45554,plain,
( spl0_6267
| ~ spl0_3
| ~ spl0_6197 ),
inference(avatar_split_clause,[],[f45412,f44677,f15,f45552]) ).
fof(f45581,definition,
( spl0_6272
<=> ! [X3,X4,X5,X2] : multiply(X4,multiply(X5,X3)) = multiply(multiply(X4,multiply(X5,X2)),multiply(inverse(X2),X3)) ),
introduced(definition,[new_symbols(definition,[spl0_6272])],[avatar_definition]) ).
fof(f45582,plain,
( ! [X2,X3,X4,X5] : multiply(X4,multiply(X5,X3)) = multiply(multiply(X4,multiply(X5,X2)),multiply(inverse(X2),X3))
| ~ spl0_6272 ),
inference(avatar_component_clause,[],[f45581]) ).
fof(f45583,plain,
( spl0_6272
| ~ spl0_280
| ~ spl0_6147
| ~ spl0_6197 ),
inference(avatar_split_clause,[],[f45436,f44677,f43207,f2264,f45581]) ).
fof(f45607,definition,
( spl0_6278
<=> ! [X0,X3,X2,X1] : multiply(inverse(inverse(multiply(X1,multiply(X2,X3)))),X0) = multiply(X1,multiply(X2,inverse(multiply(inverse(X0),inverse(X3))))) ),
introduced(definition,[new_symbols(definition,[spl0_6278])],[avatar_definition]) ).
fof(f45608,plain,
( ! [X2,X3,X0,X1] : multiply(inverse(inverse(multiply(X1,multiply(X2,X3)))),X0) = multiply(X1,multiply(X2,inverse(multiply(inverse(X0),inverse(X3)))))
| ~ spl0_6278 ),
inference(avatar_component_clause,[],[f45607]) ).
fof(f45609,plain,
( spl0_6278
| ~ spl0_93
| ~ spl0_6147
| ~ spl0_6187
| ~ spl0_6197 ),
inference(avatar_split_clause,[],[f45469,f44677,f44570,f43207,f556,f45607]) ).
fof(f45611,definition,
( spl0_6279
<=> ! [X4,X0,X2] : multiply(X4,X0) = multiply(X2,multiply(inverse(inverse(multiply(inverse(X2),X4))),X0)) ),
introduced(definition,[new_symbols(definition,[spl0_6279])],[avatar_definition]) ).
fof(f45612,plain,
( ! [X2,X0,X4] : multiply(X4,X0) = multiply(X2,multiply(inverse(inverse(multiply(inverse(X2),X4))),X0))
| ~ spl0_6279 ),
inference(avatar_component_clause,[],[f45611]) ).
fof(f45613,plain,
( spl0_6279
| ~ spl0_102
| ~ spl0_6156
| ~ spl0_6164
| ~ spl0_6197 ),
inference(avatar_split_clause,[],[f45470,f44677,f43647,f43243,f593,f45611]) ).
fof(f45632,definition,
( spl0_6283
<=> ! [X2,X1] : multiply(inverse(X1),multiply(X1,X2)) = X2 ),
introduced(definition,[new_symbols(definition,[spl0_6283])],[avatar_definition]) ).
fof(f45633,plain,
( ! [X2,X1] : multiply(inverse(X1),multiply(X1,X2)) = X2
| ~ spl0_6283 ),
inference(avatar_component_clause,[],[f45632]) ).
fof(f45635,plain,
( spl0_6283
| ~ spl0_98
| ~ spl0_6067
| ~ spl0_6147
| ~ spl0_6187
| ~ spl0_6197 ),
inference(avatar_split_clause,[],[f45535,f44677,f44570,f43207,f42415,f576,f45632]) ).
fof(f45686,plain,
( ! [X2,X3,X0,X1] : inverse(multiply(inverse(X3),inverse(X1))) = multiply(multiply(X0,X2),multiply(inverse(multiply(inverse(multiply(inverse(X0),X1)),X2)),X3))
| ~ spl0_6252
| ~ spl0_6267 ),
inference(forward_demodulation,[],[f45553,f45447]) ).
fof(f45692,plain,
( ! [X2,X3,X0,X1] : multiply(inverse(inverse(multiply(X1,multiply(X2,X3)))),X0) = multiply(X1,multiply(multiply(X2,X3),X0))
| ~ spl0_6252
| ~ spl0_6278 ),
inference(forward_demodulation,[],[f45608,f45447]) ).
fof(f45693,plain,
( ! [X2,X0,X4] : multiply(X4,X0) = multiply(X2,multiply(multiply(inverse(X2),X4),X0))
| ~ spl0_6207
| ~ spl0_6279 ),
inference(forward_demodulation,[],[f45612,f45104]) ).
fof(f45741,plain,
( ! [X2,X3,X0,X1] : inverse(multiply(inverse(X3),inverse(X1))) = multiply(multiply(X0,X2),multiply(inverse(X2),multiply(multiply(inverse(X0),X1),X3)))
| ~ spl0_6231
| ~ spl0_6252
| ~ spl0_6267 ),
inference(forward_demodulation,[],[f45686,f45299]) ).
fof(f45746,plain,
( ! [X2,X3,X0,X1] : multiply(multiply(X1,multiply(X2,X3)),X0) = multiply(X1,multiply(multiply(X2,X3),X0))
| ~ spl0_6207
| ~ spl0_6252
| ~ spl0_6278 ),
inference(forward_demodulation,[],[f45692,f45104]) ).
fof(f45748,definition,
( spl0_6296
<=> ! [X4,X0,X2] : multiply(X4,X0) = multiply(X2,multiply(multiply(inverse(X2),X4),X0)) ),
introduced(definition,[new_symbols(definition,[spl0_6296])],[avatar_definition]) ).
fof(f45749,plain,
( ! [X2,X0,X4] : multiply(X4,X0) = multiply(X2,multiply(multiply(inverse(X2),X4),X0))
| ~ spl0_6296 ),
inference(avatar_component_clause,[],[f45748]) ).
fof(f45750,plain,
( spl0_6296
| ~ spl0_6207
| ~ spl0_6279 ),
inference(avatar_split_clause,[],[f45693,f45611,f45103,f45748]) ).
fof(f45757,definition,
( spl0_6298
<=> ! [X0,X3,X2,X1] : multiply(multiply(X1,multiply(X2,X3)),X0) = multiply(X1,multiply(multiply(X2,X3),X0)) ),
introduced(definition,[new_symbols(definition,[spl0_6298])],[avatar_definition]) ).
fof(f45758,plain,
( ! [X2,X3,X0,X1] : multiply(multiply(X1,multiply(X2,X3)),X0) = multiply(X1,multiply(multiply(X2,X3),X0))
| ~ spl0_6298 ),
inference(avatar_component_clause,[],[f45757]) ).
fof(f45785,plain,
( ! [X3,X0,X1] : inverse(multiply(inverse(X3),inverse(X1))) = multiply(X0,multiply(multiply(inverse(X0),X1),X3))
| ~ spl0_6231
| ~ spl0_6243
| ~ spl0_6252
| ~ spl0_6267 ),
inference(forward_demodulation,[],[f45741,f45379]) ).
fof(f45788,plain,
( spl0_6298
| ~ spl0_6207
| ~ spl0_6252
| ~ spl0_6278 ),
inference(avatar_split_clause,[],[f45746,f45607,f45446,f45103,f45757]) ).
fof(f45800,definition,
( spl0_6306
<=> ! [X0,X1,X3] : inverse(multiply(inverse(X3),inverse(X1))) = multiply(X0,multiply(multiply(inverse(X0),X1),X3)) ),
introduced(definition,[new_symbols(definition,[spl0_6306])],[avatar_definition]) ).
fof(f45801,plain,
( ! [X3,X0,X1] : inverse(multiply(inverse(X3),inverse(X1))) = multiply(X0,multiply(multiply(inverse(X0),X1),X3))
| ~ spl0_6306 ),
inference(avatar_component_clause,[],[f45800]) ).
fof(f45802,plain,
( spl0_6306
| ~ spl0_6231
| ~ spl0_6243
| ~ spl0_6252
| ~ spl0_6267 ),
inference(avatar_split_clause,[],[f45785,f45552,f45446,f45378,f45298,f45800]) ).
fof(f45807,plain,
( ! [X3,X1] : multiply(X1,X3) = inverse(multiply(inverse(X3),inverse(X1)))
| ~ spl0_6296
| ~ spl0_6306 ),
inference(forward_demodulation,[],[f45801,f45749]) ).
fof(f45817,definition,
( spl0_6309
<=> ! [X0,X3] : multiply(X3,X0) = inverse(multiply(inverse(X0),inverse(X3))) ),
introduced(definition,[new_symbols(definition,[spl0_6309])],[avatar_definition]) ).
fof(f45818,plain,
( ! [X3,X0] : multiply(X3,X0) = inverse(multiply(inverse(X0),inverse(X3)))
| ~ spl0_6309 ),
inference(avatar_component_clause,[],[f45817]) ).
fof(f45820,plain,
( spl0_6309
| ~ spl0_6296
| ~ spl0_6306 ),
inference(avatar_split_clause,[],[f45807,f45800,f45748,f45817]) ).
fof(f45887,plain,
( ! [X2,X3,X0,X1] : multiply(X1,inverse(multiply(inverse(X3),inverse(multiply(X2,multiply(inverse(X2),X2)))))) = inverse(multiply(inverse(multiply(inverse(multiply(inverse(multiply(X1,X2)),inverse(X0))),X3)),inverse(multiply(inverse(X0),multiply(X0,inverse(X0))))))
| ~ spl0_3
| ~ spl0_6219 ),
inference(superposition,[],[f16,f45235]) ).
fof(f46058,plain,
( ! [X2,X3,X0,X1] : multiply(X1,inverse(multiply(inverse(X3),inverse(multiply(X2,multiply(inverse(X2),X2)))))) = multiply(multiply(inverse(X0),multiply(X0,inverse(X0))),multiply(inverse(multiply(inverse(multiply(X1,X2)),inverse(X0))),X3))
| ~ spl0_3
| ~ spl0_6219
| ~ spl0_6309 ),
inference(forward_demodulation,[],[f45887,f45818]) ).
fof(f46128,plain,
( ! [X2,X3,X0,X1] : multiply(X1,inverse(multiply(inverse(X3),inverse(multiply(X2,multiply(inverse(X2),X2)))))) = multiply(multiply(inverse(X0),multiply(X0,inverse(X0))),multiply(inverse(inverse(X0)),multiply(multiply(X1,X2),X3)))
| ~ spl0_3
| ~ spl0_6219
| ~ spl0_6231
| ~ spl0_6309 ),
inference(forward_demodulation,[],[f46058,f45299]) ).
fof(f46158,plain,
( ! [X2,X3,X0,X1] : multiply(X1,inverse(multiply(inverse(X3),inverse(multiply(X2,multiply(inverse(X2),X2)))))) = multiply(inverse(X0),multiply(X0,multiply(multiply(X1,X2),X3)))
| ~ spl0_3
| ~ spl0_6219
| ~ spl0_6231
| ~ spl0_6272
| ~ spl0_6309 ),
inference(forward_demodulation,[],[f46128,f45582]) ).
fof(f46178,plain,
( ! [X2,X3,X1] : multiply(X1,inverse(multiply(inverse(X3),inverse(multiply(X2,multiply(inverse(X2),X2)))))) = multiply(multiply(X1,X2),X3)
| ~ spl0_3
| ~ spl0_6219
| ~ spl0_6231
| ~ spl0_6272
| ~ spl0_6283
| ~ spl0_6309 ),
inference(forward_demodulation,[],[f46158,f45633]) ).
fof(f46194,plain,
( ! [X2,X3,X1] : multiply(multiply(X1,X2),X3) = multiply(multiply(X1,multiply(X2,multiply(inverse(X2),X2))),X3)
| ~ spl0_3
| ~ spl0_6219
| ~ spl0_6231
| ~ spl0_6252
| ~ spl0_6272
| ~ spl0_6283
| ~ spl0_6309 ),
inference(forward_demodulation,[],[f46178,f45447]) ).
fof(f46206,plain,
( ! [X2,X3,X1] : multiply(multiply(X1,X2),X3) = multiply(X1,multiply(multiply(X2,multiply(inverse(X2),X2)),X3))
| ~ spl0_3
| ~ spl0_6219
| ~ spl0_6231
| ~ spl0_6252
| ~ spl0_6272
| ~ spl0_6283
| ~ spl0_6298
| ~ spl0_6309 ),
inference(forward_demodulation,[],[f46194,f45758]) ).
fof(f46214,plain,
( ! [X2,X3,X1] : multiply(multiply(X1,X2),X3) = multiply(X1,multiply(X2,multiply(multiply(inverse(X2),X2),X3)))
| ~ spl0_3
| ~ spl0_6219
| ~ spl0_6231
| ~ spl0_6252
| ~ spl0_6272
| ~ spl0_6283
| ~ spl0_6298
| ~ spl0_6309 ),
inference(forward_demodulation,[],[f46206,f45758]) ).
fof(f46217,plain,
( ! [X2,X3,X1] : multiply(X1,multiply(X2,X3)) = multiply(multiply(X1,X2),X3)
| ~ spl0_3
| ~ spl0_6219
| ~ spl0_6231
| ~ spl0_6252
| ~ spl0_6272
| ~ spl0_6283
| ~ spl0_6296
| ~ spl0_6298
| ~ spl0_6309 ),
inference(forward_demodulation,[],[f46214,f45749]) ).
fof(f46221,definition,
( spl0_6321
<=> ! [X2,X1,X3] : multiply(X1,multiply(X2,X3)) = multiply(multiply(X1,X2),X3) ),
introduced(definition,[new_symbols(definition,[spl0_6321])],[avatar_definition]) ).
fof(f46222,plain,
( ! [X2,X3,X1] : multiply(X1,multiply(X2,X3)) = multiply(multiply(X1,X2),X3)
| ~ spl0_6321 ),
inference(avatar_component_clause,[],[f46221]) ).
fof(f46223,plain,
( spl0_6321
| ~ spl0_3
| ~ spl0_6219
| ~ spl0_6231
| ~ spl0_6252
| ~ spl0_6272
| ~ spl0_6283
| ~ spl0_6296
| ~ spl0_6298
| ~ spl0_6309 ),
inference(avatar_split_clause,[],[f46217,f45817,f45757,f45748,f45632,f45581,f45446,f45298,f45234,f15,f46221]) ).
fof(f46233,plain,
( $false
| spl0_1
| ~ spl0_6321 ),
inference(backward_subsumption_resolution,[],[f6,f46222]) ).
fof(f46234,plain,
( spl0_1
| ~ spl0_6321 ),
inference(avatar_contradiction_clause,[],[f46233]) ).
cnf(s1,plain,
~ spl0_1,
inference(sat_conversion,[],[f7]) ).
cnf(s2,plain,
spl0_2,
inference(sat_conversion,[],[f11]) ).
cnf(s3,plain,
( ~ spl0_2
| spl0_3 ),
inference(sat_conversion,[],[f17]) ).
cnf(s8,plain,
( ~ spl0_2
| ~ spl0_3
| spl0_8 ),
inference(sat_conversion,[],[f62]) ).
cnf(s12,plain,
( ~ spl0_2
| ~ spl0_3
| spl0_12 ),
inference(sat_conversion,[],[f78]) ).
cnf(s33,plain,
( ~ spl0_3
| ~ spl0_12
| spl0_31 ),
inference(sat_conversion,[],[f167]) ).
cnf(s51,plain,
( ~ spl0_8
| ~ spl0_12
| spl0_49 ),
inference(sat_conversion,[],[f271]) ).
cnf(s59,plain,
( ~ spl0_8
| spl0_57 ),
inference(sat_conversion,[],[f303]) ).
cnf(s78,plain,
( ~ spl0_12
| ~ spl0_57
| spl0_75 ),
inference(sat_conversion,[],[f410]) ).
cnf(s80,plain,
( ~ spl0_2
| ~ spl0_57
| spl0_77 ),
inference(sat_conversion,[],[f418]) ).
cnf(s98,plain,
( ~ spl0_2
| ~ spl0_75
| spl0_93 ),
inference(sat_conversion,[],[f558]) ).
cnf(s103,plain,
( ~ spl0_57
| ~ spl0_75
| spl0_98 ),
inference(sat_conversion,[],[f578]) ).
cnf(s116,plain,
( ~ spl0_75
| spl0_99 ),
inference(sat_conversion,[],[f583]) ).
cnf(s120,plain,
( ~ spl0_57
| ~ spl0_75
| spl0_102 ),
inference(sat_conversion,[],[f595]) ).
cnf(s123,plain,
( ~ spl0_75
| spl0_105 ),
inference(sat_conversion,[],[f607]) ).
cnf(s127,plain,
( ~ spl0_2
| ~ spl0_75
| spl0_108 ),
inference(sat_conversion,[],[f619]) ).
cnf(s245,plain,
( ~ spl0_2
| ~ spl0_99
| ~ spl0_108
| spl0_191 ),
inference(sat_conversion,[],[f1239]) ).
cnf(s314,plain,
( ~ spl0_8
| ~ spl0_191
| spl0_228 ),
inference(sat_conversion,[],[f1568]) ).
cnf(s461,plain,
( ~ spl0_99
| ~ spl0_105
| spl0_280 ),
inference(sat_conversion,[],[f2266]) ).
cnf(s578,plain,
( ~ spl0_12
| ~ spl0_31
| ~ spl0_105
| spl0_364 ),
inference(sat_conversion,[],[f2619]) ).
cnf(s1512,plain,
( ~ spl0_57
| ~ spl0_102
| spl0_819 ),
inference(sat_conversion,[],[f6100]) ).
cnf(s1848,plain,
( ~ spl0_2
| ~ spl0_108
| ~ spl0_819
| spl0_951 ),
inference(sat_conversion,[],[f6953]) ).
cnf(s2017,plain,
( ~ spl0_75
| ~ spl0_951
| spl0_1005 ),
inference(sat_conversion,[],[f7547]) ).
cnf(s2804,plain,
( ~ spl0_12
| ~ spl0_77
| spl0_1296 ),
inference(sat_conversion,[],[f10825]) ).
cnf(s3060,plain,
( ~ spl0_819
| ~ spl0_1296
| spl0_1480 ),
inference(sat_conversion,[],[f11769]) ).
cnf(s3384,plain,
( ~ spl0_1296
| ~ spl0_1480
| spl0_1706 ),
inference(sat_conversion,[],[f13183]) ).
cnf(s3542,plain,
( ~ spl0_2
| ~ spl0_1296
| ~ spl0_1480
| spl0_1809 ),
inference(sat_conversion,[],[f13608]) ).
cnf(s3555,plain,
( ~ spl0_2
| ~ spl0_3
| ~ spl0_57
| ~ spl0_1480
| spl0_1819 ),
inference(sat_conversion,[],[f13649]) ).
cnf(s3646,plain,
( ~ spl0_1296
| ~ spl0_1706
| spl0_1890 ),
inference(sat_conversion,[],[f14331]) ).
cnf(s3652,plain,
( ~ spl0_228
| ~ spl0_1706
| spl0_1893 ),
inference(sat_conversion,[],[f14344]) ).
cnf(s3856,plain,
( ~ spl0_1706
| ~ spl0_1819
| spl0_1964 ),
inference(sat_conversion,[],[f14758]) ).
cnf(s4224,plain,
( ~ spl0_12
| ~ spl0_1893
| spl0_2181 ),
inference(sat_conversion,[],[f16427]) ).
cnf(s4274,plain,
( ~ spl0_1706
| ~ spl0_2181
| spl0_2220 ),
inference(sat_conversion,[],[f17120]) ).
cnf(s5104,plain,
( ~ spl0_1890
| ~ spl0_2220
| spl0_2640 ),
inference(sat_conversion,[],[f20324]) ).
cnf(s5106,plain,
( ~ spl0_1706
| ~ spl0_1890
| spl0_2643 ),
inference(sat_conversion,[],[f20329]) ).
cnf(s5590,plain,
( ~ spl0_2
| ~ spl0_1809
| ~ spl0_2640
| spl0_2938 ),
inference(sat_conversion,[],[f22309]) ).
cnf(s5674,plain,
( ~ spl0_2643
| ~ spl0_2938
| spl0_3011 ),
inference(sat_conversion,[],[f23013]) ).
cnf(s5679,plain,
( ~ spl0_1964
| ~ spl0_2938
| spl0_3014 ),
inference(sat_conversion,[],[f23027]) ).
cnf(s5875,plain,
( ~ spl0_1819
| ~ spl0_2938
| spl0_3107 ),
inference(sat_conversion,[],[f23562]) ).
cnf(s5905,plain,
( ~ spl0_2938
| spl0_3156 ),
inference(sat_conversion,[],[f23638]) ).
cnf(s5911,plain,
( ~ spl0_2938
| spl0_3160 ),
inference(sat_conversion,[],[f23655]) ).
cnf(s5940,plain,
( ~ spl0_2938
| spl0_3169 ),
inference(sat_conversion,[],[f23693]) ).
cnf(s9638,plain,
( ~ spl0_3011
| ~ spl0_3160
| spl0_5684 ),
inference(sat_conversion,[],[f40229]) ).
cnf(s10229,plain,
( ~ spl0_3
| ~ spl0_3169
| ~ spl0_5684
| spl0_6066 ),
inference(sat_conversion,[],[f42409]) ).
cnf(s10230,plain,
( ~ spl0_2
| ~ spl0_3169
| ~ spl0_5684
| spl0_6065 ),
inference(sat_conversion,[],[f42410]) ).
cnf(s10233,plain,
( ~ spl0_6065
| ~ spl0_6066
| spl0_6067 ),
inference(sat_conversion,[],[f42417]) ).
cnf(s10273,plain,
( ~ spl0_3156
| ~ spl0_6065
| spl0_6089 ),
inference(sat_conversion,[],[f42952]) ).
cnf(s10280,plain,
( ~ spl0_2938
| ~ spl0_6065
| spl0_6090 ),
inference(sat_conversion,[],[f42974]) ).
cnf(s10378,plain,
( ~ spl0_364
| ~ spl0_6065
| spl0_6146 ),
inference(sat_conversion,[],[f43205]) ).
cnf(s10386,plain,
( ~ spl0_228
| ~ spl0_6065
| spl0_6147 ),
inference(sat_conversion,[],[f43209]) ).
cnf(s10400,plain,
( ~ spl0_102
| ~ spl0_3107
| ~ spl0_6065
| spl0_6152 ),
inference(sat_conversion,[],[f43229]) ).
cnf(s10410,plain,
( ~ spl0_75
| ~ spl0_6065
| spl0_6156 ),
inference(sat_conversion,[],[f43245]) ).
cnf(s10431,plain,
( ~ spl0_6146
| ~ spl0_6152
| spl0_6161 ),
inference(sat_conversion,[],[f43300]) ).
cnf(s10436,plain,
( ~ spl0_3014
| ~ spl0_6089
| spl0_6164 ),
inference(sat_conversion,[],[f43649]) ).
cnf(s10493,plain,
( ~ spl0_3
| ~ spl0_6090
| ~ spl0_6147
| spl0_6187 ),
inference(sat_conversion,[],[f44572]) ).
cnf(s10528,plain,
( ~ spl0_1005
| ~ spl0_6089
| ~ spl0_6090
| ~ spl0_6147
| ~ spl0_6161
| spl0_6197 ),
inference(sat_conversion,[],[f44681]) ).
cnf(s10548,plain,
( ~ spl0_6197
| spl0_6207 ),
inference(sat_conversion,[],[f45105]) ).
cnf(s10583,plain,
( ~ spl0_228
| ~ spl0_6147
| ~ spl0_6197
| spl0_6231 ),
inference(sat_conversion,[],[f45300]) ).
cnf(s10609,plain,
( ~ spl0_1819
| ~ spl0_6090
| ~ spl0_6197
| spl0_6219 ),
inference(sat_conversion,[],[f45384]) ).
cnf(s10625,plain,
( ~ spl0_49
| ~ spl0_6147
| ~ spl0_6197
| spl0_6243 ),
inference(sat_conversion,[],[f45444]) ).
cnf(s10626,plain,
( ~ spl0_12
| ~ spl0_6197
| spl0_6252 ),
inference(sat_conversion,[],[f45448]) ).
cnf(s10654,plain,
( ~ spl0_3
| ~ spl0_6197
| spl0_6267 ),
inference(sat_conversion,[],[f45554]) ).
cnf(s10664,plain,
( ~ spl0_280
| ~ spl0_6147
| ~ spl0_6197
| spl0_6272 ),
inference(sat_conversion,[],[f45583]) ).
cnf(s10672,plain,
( ~ spl0_93
| ~ spl0_6147
| ~ spl0_6187
| ~ spl0_6197
| spl0_6278 ),
inference(sat_conversion,[],[f45609]) ).
cnf(s10673,plain,
( ~ spl0_102
| ~ spl0_6156
| ~ spl0_6164
| ~ spl0_6197
| spl0_6279 ),
inference(sat_conversion,[],[f45613]) ).
cnf(s10685,plain,
( ~ spl0_98
| ~ spl0_6067
| ~ spl0_6147
| ~ spl0_6187
| ~ spl0_6197
| spl0_6283 ),
inference(sat_conversion,[],[f45635]) ).
cnf(s10702,plain,
( ~ spl0_6207
| ~ spl0_6279
| spl0_6296 ),
inference(sat_conversion,[],[f45750]) ).
cnf(s10710,plain,
( ~ spl0_6207
| ~ spl0_6252
| ~ spl0_6278
| spl0_6298 ),
inference(sat_conversion,[],[f45788]) ).
cnf(s10713,plain,
( ~ spl0_6231
| ~ spl0_6243
| ~ spl0_6252
| ~ spl0_6267
| spl0_6306 ),
inference(sat_conversion,[],[f45802]) ).
cnf(s10717,plain,
( ~ spl0_6296
| ~ spl0_6306
| spl0_6309 ),
inference(sat_conversion,[],[f45820]) ).
cnf(s10757,plain,
( ~ spl0_3
| ~ spl0_6219
| ~ spl0_6231
| ~ spl0_6252
| ~ spl0_6272
| ~ spl0_6283
| ~ spl0_6296
| ~ spl0_6298
| ~ spl0_6309
| spl0_6321 ),
inference(sat_conversion,[],[f46223]) ).
cnf(s10760,plain,
( spl0_1
| ~ spl0_6321 ),
inference(sat_conversion,[],[f46234]) ).
cnf(s10762,plain,
spl0_3,
inference(rat,[],[s3,s2]) ).
cnf(s10778,plain,
spl0_12,
inference(rat,[],[s12,s2,s10762]) ).
cnf(s10782,plain,
spl0_8,
inference(rat,[],[s8,s2,s10762]) ).
cnf(s10793,plain,
spl0_31,
inference(rat,[],[s33,s10762,s10778]) ).
cnf(s10803,plain,
spl0_57,
inference(rat,[],[s59,s10782]) ).
cnf(s10811,plain,
spl0_49,
inference(rat,[],[s51,s10778,s10782]) ).
cnf(s10832,plain,
spl0_77,
inference(rat,[],[s80,s2,s10803]) ).
cnf(s10834,plain,
spl0_75,
inference(rat,[],[s78,s10778,s10803]) ).
cnf(s10901,plain,
spl0_1296,
inference(rat,[],[s2804,s10778,s10832]) ).
cnf(s10912,plain,
spl0_108,
inference(rat,[],[s127,s2,s10834]) ).
cnf(s10915,plain,
spl0_105,
inference(rat,[],[s123,s10834]) ).
cnf(s10918,plain,
spl0_102,
inference(rat,[],[s120,s10803,s10834]) ).
cnf(s10921,plain,
spl0_99,
inference(rat,[],[s116,s10834]) ).
cnf(s10922,plain,
spl0_98,
inference(rat,[],[s103,s10803,s10834]) ).
cnf(s10927,plain,
spl0_93,
inference(rat,[],[s98,s2,s10834]) ).
cnf(s11050,plain,
spl0_364,
inference(rat,[],[s578,s10793,s10778,s10915]) ).
cnf(s11078,plain,
spl0_819,
inference(rat,[],[s1512,s10803,s10918]) ).
cnf(s11208,plain,
spl0_280,
inference(rat,[],[s461,s10915,s10921]) ).
cnf(s11216,plain,
spl0_191,
inference(rat,[],[s245,s10912,s2,s10921]) ).
cnf(s11595,plain,
spl0_1480,
inference(rat,[],[s3060,s10901,s11078]) ).
cnf(s11687,plain,
spl0_951,
inference(rat,[],[s1848,s10912,s2,s11078]) ).
cnf(s11849,plain,
spl0_228,
inference(rat,[],[s314,s10782,s11216]) ).
cnf(s11965,plain,
spl0_1706,
inference(rat,[],[s3384,s10901,s11595]) ).
cnf(s12087,plain,
spl0_1809,
inference(rat,[],[s3542,s10901,s2,s11595]) ).
cnf(s12088,plain,
spl0_1819,
inference(rat,[],[s3555,s10803,s10762,s2,s11595]) ).
cnf(s12151,plain,
spl0_1005,
inference(rat,[],[s2017,s10834,s11687]) ).
cnf(s12310,plain,
spl0_1893,
inference(rat,[],[s3652,s11849,s11965]) ).
cnf(s12314,plain,
spl0_1890,
inference(rat,[],[s3646,s10901,s11965]) ).
cnf(s12386,plain,
spl0_1964,
inference(rat,[],[s3856,s11965,s12088]) ).
cnf(s12595,plain,
spl0_2181,
inference(rat,[],[s4224,s10778,s12310]) ).
cnf(s12725,plain,
spl0_2643,
inference(rat,[],[s5106,s11965,s12314]) ).
cnf(s13066,plain,
spl0_2220,
inference(rat,[],[s4274,s11965,s12595]) ).
cnf(s13155,plain,
spl0_2640,
inference(rat,[],[s5104,s12314,s13066]) ).
cnf(s13561,plain,
spl0_2938,
inference(rat,[],[s5590,s12087,s2,s13155]) ).
cnf(s13589,plain,
spl0_3169,
inference(rat,[],[s5940,s13561]) ).
cnf(s13598,plain,
spl0_3160,
inference(rat,[],[s5911,s13561]) ).
cnf(s13601,plain,
spl0_3156,
inference(rat,[],[s5905,s13561]) ).
cnf(s13617,plain,
spl0_3107,
inference(rat,[],[s5875,s12088,s13561]) ).
cnf(s13741,plain,
spl0_3014,
inference(rat,[],[s5679,s12386,s13561]) ).
cnf(s13744,plain,
spl0_3011,
inference(rat,[],[s5674,s12725,s13561]) ).
cnf(s15344,plain,
spl0_5684,
inference(rat,[],[s9638,s13598,s13744]) ).
cnf(s16559,plain,
spl0_6065,
inference(rat,[],[s10230,s13589,s2,s15344]) ).
cnf(s16560,plain,
spl0_6066,
inference(rat,[],[s10229,s13589,s10762,s15344]) ).
cnf(s16830,plain,
spl0_6156,
inference(rat,[],[s10410,s10834,s16559]) ).
cnf(s16838,plain,
spl0_6147,
inference(rat,[],[s10386,s11849,s16559]) ).
cnf(s16839,plain,
spl0_6146,
inference(rat,[],[s10378,s11050,s16559]) ).
cnf(s16890,plain,
spl0_6090,
inference(rat,[],[s10280,s13561,s16559]) ).
cnf(s16892,plain,
spl0_6089,
inference(rat,[],[s10273,s13601,s16559]) ).
cnf(s16915,plain,
spl0_6152,
inference(rat,[],[s10400,s13617,s10918,s16559]) ).
cnf(s16916,plain,
spl0_6067,
inference(rat,[],[s10233,s16559,s16560]) ).
cnf(s16923,plain,
spl0_6187,
inference(rat,[],[s10493,s16838,s10762,s16890]) ).
cnf(s16944,plain,
spl0_6164,
inference(rat,[],[s10436,s13741,s16892]) ).
cnf(s16947,plain,
spl0_6161,
inference(rat,[],[s10431,s16839,s16915]) ).
cnf(s16954,plain,
spl0_6197,
inference(rat,[],[s10528,s16892,s16890,s16838,s12151,s16947]) ).
cnf(s16957,plain,
spl0_6267,
inference(rat,[],[s10654,s10762,s16954]) ).
cnf(s16960,plain,
spl0_6252,
inference(rat,[],[s10626,s10778,s16954]) ).
cnf(s16976,plain,
spl0_6207,
inference(rat,[],[s10548,s16954]) ).
cnf(s16987,plain,
spl0_6243,
inference(rat,[],[s10625,s16838,s10811,s16954]) ).
cnf(s17010,plain,
spl0_6272,
inference(rat,[],[s10664,s16838,s11208,s16954]) ).
cnf(s17015,plain,
spl0_6231,
inference(rat,[],[s10583,s16838,s11849,s16954]) ).
cnf(s17016,plain,
spl0_6219,
inference(rat,[],[s10609,s16890,s12088,s16954]) ).
cnf(s17023,plain,
spl0_6279,
inference(rat,[],[s10673,s16944,s16830,s10918,s16954]) ).
cnf(s17036,plain,
spl0_6278,
inference(rat,[],[s10672,s16923,s16838,s10927,s16954]) ).
cnf(s17045,plain,
spl0_6283,
inference(rat,[],[s10685,s16923,s16916,s16838,s10922,s16954]) ).
cnf(s17047,plain,
spl0_6298,
inference(rat,[],[s10710,s16960,s17036,s16976]) ).
cnf(s17059,plain,
spl0_6306,
inference(rat,[],[s10713,s16987,s16957,s16960,s17015]) ).
cnf(s17070,plain,
spl0_6296,
inference(rat,[],[s10702,s16976,s17023]) ).
cnf(s17075,plain,
spl0_6309,
inference(rat,[],[s10717,s17059,s17070]) ).
cnf(s17081,plain,
spl0_6321,
inference(rat,[],[s10757,s17070,s17016,s17047,s17015,s17045,s17010,s16960,s10762,s17075]) ).
cnf(s17082,plain,
spl0_1,
inference(rat,[],[s10760,s17081]) ).
cnf(s17083,plain,
$false,
inference(rat,[],[s1,s17082]) ).
fof(f46235,plain,
$false,
inference(avatar_sat_refutation,[],[s17083]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : GRP405-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.04 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.36 % Computer : n016.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Sun Sep 27 10:07:02 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.40 Running first-order model finding
% 0.10/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
% 15.44/2.68 % (2390223)Will run a generic schedule for satisfiability detection.
% 15.44/2.68 % (2390233)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3873811684:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.44/2.68 % (2390229)% WARNING: option uhcvi not known.
% 15.44/2.68 % (2390228)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3948026116_2999 on theBenchmark for (2999ds/0Mi)
% 15.44/2.68 % (2390230)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3623279990:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.44/2.68 % (2390234)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=4139814129:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.44/2.68 % (2390231)dis+10_1_sil=32000:sp=arity:random_seed=813593538:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.44/2.68 % (2390232)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2991828895:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.44/2.68 % TRYING [1]
% 15.44/2.68 % TRYING [2]
% 15.44/2.68 % TRYING [3]
% 15.44/2.68 % (2390229)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=689697827:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.44/2.68 % (2390233)Instruction limit reached!
% 15.44/2.68 % (2390233)------------------------------
% 15.44/2.68 % (2390233)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.44/2.68 % (2390233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.44/2.68 % (2390233)CaDiCaL version: 2.1.3
% 15.44/2.68 % (2390233)Termination reason: Instruction limit
% 15.44/2.68 % (2390233)Termination phase: Saturation
% 15.44/2.68 % (2390233)Time elapsed: 0.042 s
% 15.44/2.68 % (2390233)Peak memory usage: 13 MB
% 15.44/2.68 % (2390233)Instructions burned: 131 (million)
% 15.44/2.68 % (2390242)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2649157811:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 15.44/2.68 % TRYING [1]
% 15.44/2.68 % TRYING [2]
% 15.44/2.68 % TRYING [3]
% 15.44/2.68 % (2390231)Instruction limit reached!
% 15.44/2.68 % (2390231)------------------------------
% 15.44/2.68 % (2390231)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.44/2.68 % (2390231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.44/2.68 % (2390231)CaDiCaL version: 2.1.3
% 15.44/2.68 % (2390231)Termination reason: Instruction limit
% 15.44/2.68 % (2390231)Termination phase: Saturation
% 15.44/2.68 % (2390231)Time elapsed: 0.055 s
% 15.44/2.68 % (2390231)Peak memory usage: 12 MB
% 15.44/2.68 % (2390231)Instructions burned: 103 (million)
% 15.44/2.68 % TRYING [4]
% 15.44/2.68 % (2390232)Instruction limit reached!
% 15.44/2.68 % (2390232)------------------------------
% 15.44/2.68 % (2390232)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.44/2.68 % (2390232)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.44/2.68 % (2390232)CaDiCaL version: 2.1.3
% 15.44/2.68 % (2390232)Termination reason: Instruction limit
% 15.44/2.68 % (2390232)Termination phase: Saturation
% 15.44/2.68 % (2390232)Time elapsed: 0.068 s
% 15.44/2.68 % (2390232)Peak memory usage: 12 MB
% 15.44/2.68 % (2390232)Instructions burned: 116 (million)
% 15.44/2.68 % (2390244)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=634318341:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 15.44/2.68 % TRYING [4]
% 15.44/2.68 % (2390245)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=968457027:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.44/2.68 % (2390234)Instruction limit reached!
% 15.44/2.68 % (2390234)------------------------------
% 15.44/2.68 % (2390234)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.44/2.68 % (2390234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.44/2.68 % (2390234)CaDiCaL version: 2.1.3
% 15.44/2.68 % (2390234)Termination reason: Instruction limit
% 15.44/2.68 % (2390234)Termination phase: Saturation
% 15.44/2.68 % (2390234)Time elapsed: 0.099 s
% 15.44/2.68 % (2390234)Peak memory usage: 12 MB
% 15.44/2.68 % (2390234)Instructions burned: 160 (million)
% 15.44/2.68 % (2390248)ott-21_1_sil=16000:fs=off:random_seed=1109019350:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 15.44/2.68 % (2390244)Instruction limit reached!
% 15.44/2.68 % (2390244)------------------------------
% 15.44/2.68 % (2390244)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.44/2.68 % (2390244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.14/5.93 % (2390244)CaDiCaL version: 2.1.3
% 37.14/5.93 % (2390244)Termination reason: Instruction limit
% 37.14/5.93 % (2390244)Termination phase: Saturation
% 37.14/5.93 % (2390244)Time elapsed: 0.073 s
% 37.14/5.93 % (2390244)Peak memory usage: 13 MB
% 37.14/5.93 % (2390244)Instructions burned: 132 (million)
% 37.14/5.93 % (2390250)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=4154588064:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 37.14/5.93 % (2390248)Instruction limit reached!
% 37.14/5.93 % (2390248)------------------------------
% 37.14/5.93 % (2390248)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.14/5.93 % (2390248)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.14/5.93 % (2390248)CaDiCaL version: 2.1.3
% 37.14/5.93 % (2390248)Termination reason: Instruction limit
% 37.14/5.93 % (2390248)Termination phase: Saturation
% 37.14/5.93 % (2390248)Time elapsed: 0.091 s
% 37.14/5.93 % (2390248)Peak memory usage: 11 MB
% 37.14/5.93 % (2390248)Instructions burned: 182 (million)
% 37.14/5.93 % (2390252)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4103128069:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 37.14/5.93 % TRYING [1]
% 37.14/5.93 % TRYING [2]
% 37.14/5.93 % TRYING [3]
% 37.14/5.93 % TRYING [4]
% 37.14/5.93 % (2390242)Instruction limit reached!
% 37.14/5.93 % (2390242)------------------------------
% 37.14/5.93 % (2390242)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.14/5.93 % (2390242)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.14/5.93 % (2390242)CaDiCaL version: 2.1.3
% 37.14/5.93 % (2390242)Termination reason: Instruction limit
% 37.14/5.93 % (2390242)Termination phase: Finite model building SAT solving
% 37.14/5.93 % (2390242)Time elapsed: 0.230 s
% 37.14/5.93 % (2390242)Peak memory usage: 12 MB
% 37.14/5.93 % (2390242)Instructions burned: 716 (million)
% 37.14/5.93 % (2390254)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1580203382:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 37.14/5.93 % (2390250)Instruction limit reached!
% 37.14/5.93 % (2390250)------------------------------
% 37.14/5.93 % (2390250)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.14/5.93 % (2390250)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.14/5.93 % (2390250)CaDiCaL version: 2.1.3
% 37.14/5.93 % (2390250)Termination reason: Instruction limit
% 37.14/5.93 % (2390250)Termination phase: Saturation
% 37.14/5.93 % (2390250)Time elapsed: 0.237 s
% 37.14/5.93 % (2390250)Peak memory usage: 15 MB
% 37.14/5.93 % (2390250)Instructions burned: 479 (million)
% 37.14/5.93 % (2390256)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=149047856:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 37.14/5.93 % (2390245)Instruction limit reached!
% 37.14/5.93 % (2390245)------------------------------
% 37.14/5.93 % (2390245)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.14/5.93 % (2390245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.14/5.93 % (2390245)CaDiCaL version: 2.1.3
% 37.14/5.93 % (2390245)Termination reason: Instruction limit
% 37.14/5.93 % (2390245)Termination phase: Saturation
% 37.14/5.93 % (2390245)Time elapsed: 0.340 s
% 37.14/5.93 % (2390245)Peak memory usage: 17 MB
% 37.14/5.93 % (2390245)Instructions burned: 685 (million)
% 37.14/5.93 % (2390258)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=3245957489:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 37.14/5.93 % TRYING [14]
% 37.14/5.93 % (2390254)Instruction limit reached!
% 37.14/5.93 % (2390254)------------------------------
% 37.14/5.93 % (2390254)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 37.14/5.93 % (2390254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 37.14/5.93 % (2390254)CaDiCaL version: 2.1.3
% 37.14/5.93 % (2390254)Termination reason: Instruction limit
% 37.14/5.93 % (2390254)Termination phase: Saturation
% 37.14/5.93 % (2390254)Time elapsed: 0.342 s
% 37.14/5.93 % (2390254)Peak memory usage: 22 MB
% 37.14/5.93 % (2390254)Instructions burned: 1183 (million)
% 37.14/5.93 % (2390260)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2365874524:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 37.14/5.93 % (2390256)Instruction limit reached!
% 37.14/5.93 % (2390256)------------------------------
% 37.14/5.93 % (2390256)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 130.32/18.86 % (2390256)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.32/18.86 % (2390256)CaDiCaL version: 2.1.3
% 130.32/18.86 % (2390256)Termination reason: Instruction limit
% 130.32/18.86 % (2390256)Termination phase: Finite model building constraint generation
% 130.32/18.86 % (2390256)Time elapsed: 0.316 s
% 130.32/18.86 % (2390256)Peak memory usage: 79 MB
% 130.32/18.86 % (2390256)Instructions burned: 890 (million)
% 130.32/18.86 % (2390252)Instruction limit reached!
% 130.32/18.86 % (2390252)------------------------------
% 130.32/18.86 % (2390252)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 130.32/18.86 % (2390252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.32/18.86 % (2390252)CaDiCaL version: 2.1.3
% 130.32/18.86 % (2390252)Termination reason: Instruction limit
% 130.32/18.86 % (2390252)Termination phase: Finite model building SAT solving
% 130.32/18.86 % (2390252)Time elapsed: 0.533 s
% 130.32/18.86 % (2390252)Peak memory usage: 11 MB
% 130.32/18.86 % (2390252)Instructions burned: 865 (million)
% 130.32/18.86 % (2390262)fmb+10_1_sil=64000:random_seed=2163055482:i=22061:nm=2:gsp=on_2992 on theBenchmark for (2992ds/22061Mi)
% 130.32/18.86 % TRYING [1]
% 130.32/18.86 % TRYING [2]
% 130.32/18.86 % TRYING [3]
% 130.32/18.86 % (2390263)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2445123064:i=9515:nm=5_2991 on theBenchmark for (2991ds/9515Mi)
% 130.32/18.86 % TRYING [20]
% 130.32/18.86 % TRYING [4]
% 130.32/18.86 % (2390258)Instruction limit reached!
% 130.32/18.86 % (2390258)------------------------------
% 130.32/18.86 % (2390258)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 130.32/18.86 % (2390258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.32/18.86 % (2390258)CaDiCaL version: 2.1.3
% 130.32/18.86 % (2390258)Termination reason: Instruction limit
% 130.32/18.86 % (2390258)Termination phase: Saturation
% 130.32/18.86 % (2390258)Time elapsed: 0.412 s
% 130.32/18.86 % (2390258)Peak memory usage: 17 MB
% 130.32/18.86 % (2390258)Instructions burned: 693 (million)
% 130.32/18.86 % (2390260)Instruction limit reached!
% 130.32/18.86 % (2390260)------------------------------
% 130.32/18.86 % (2390260)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 130.32/18.86 % (2390260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.32/18.86 % (2390260)CaDiCaL version: 2.1.3
% 130.32/18.86 % (2390260)Termination reason: Instruction limit
% 130.32/18.86 % (2390260)Termination phase: Saturation
% 130.32/18.86 % (2390260)Time elapsed: 0.226 s
% 130.32/18.86 % (2390260)Peak memory usage: 16 MB
% 130.32/18.86 % (2390260)Instructions burned: 879 (million)
% 130.32/18.86 % (2390267)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2543652255:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 130.32/18.86 % (2390266)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=3475302452:fmbsr=1.7:i=920_2990 on theBenchmark for (2990ds/920Mi)
% 130.32/18.86 % TRYING [8]
% 130.32/18.86 % TRYING [5]
% 130.32/18.86 % (2390266)Instruction limit reached!
% 130.32/18.86 % (2390266)------------------------------
% 130.32/18.86 % (2390266)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 130.32/18.86 % (2390266)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.32/18.86 % (2390266)CaDiCaL version: 2.1.3
% 130.32/18.86 % (2390266)Termination reason: Instruction limit
% 130.32/18.86 % (2390266)Termination phase: Finite model building SAT solving
% 130.32/18.86 % (2390266)Time elapsed: 0.473 s
% 130.32/18.86 % (2390266)Peak memory usage: 37 MB
% 130.32/18.86 % (2390266)Instructions burned: 921 (million)
% 130.32/18.86 % (2390270)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3456090691:i=1472:ins=7:fdi=8:gsp=on_2986 on theBenchmark for (2986ds/1472Mi)
% 130.32/18.86 % (2390270)Instruction limit reached!
% 130.32/18.86 % (2390270)------------------------------
% 130.32/18.86 % (2390270)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 130.32/18.86 % (2390270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 130.32/18.86 % (2390270)CaDiCaL version: 2.1.3
% 130.32/18.86 % (2390270)Termination reason: Instruction limit
% 130.32/18.86 % (2390270)Termination phase: Saturation
% 130.32/18.86 % (2390270)Time elapsed: 0.721 s
% 130.32/18.86 % (2390270)Peak memory usage: 28 MB
% 130.32/18.86 % (2390270)Instructions burned: 1473 (million)
% 130.32/18.86 % (2390272)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1730860155:i=6324_2978 on theBenchmark for (2978ds/6324Mi)
% 130.32/18.86 % TRYING [77]
% 130.32/18.86 % (2390267)Instruction limit reached!
% 130.32/18.86 % (2390267)------------------------------
% 218.79/31.33 % (2390267)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 218.79/31.33 % (2390267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.79/31.33 % (2390267)CaDiCaL version: 2.1.3
% 218.79/31.33 % (2390267)Termination reason: Instruction limit
% 218.79/31.33 % (2390267)Termination phase: Saturation
% 218.79/31.33 % (2390267)Time elapsed: 1.352 s
% 218.79/31.33 % (2390267)Peak memory usage: 43 MB
% 218.79/31.33 % (2390267)Instructions burned: 5133 (million)
% 218.79/31.33 % (2390274)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3478673989:fmbsr=2.30978:i=2174_2977 on theBenchmark for (2977ds/2174Mi)
% 218.79/31.33 % TRYING [16]
% 218.79/31.33 % TRYING [5]
% 218.79/31.33 % (2390274)Instruction limit reached!
% 218.79/31.33 % (2390274)------------------------------
% 218.79/31.33 % (2390274)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 218.79/31.33 % (2390274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.79/31.33 % (2390274)CaDiCaL version: 2.1.3
% 218.79/31.33 % (2390274)Termination reason: Instruction limit
% 218.79/31.33 % (2390274)Termination phase: Finite model building constraint generation
% 218.79/31.33 % (2390274)Time elapsed: 0.423 s
% 218.79/31.33 % (2390274)Peak memory usage: 153 MB
% 218.79/31.33 % (2390274)Instructions burned: 2175 (million)
% 218.79/31.33 % (2390276)ott-2_1_sil=16000:newcnf=on:random_seed=849376380:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2972 on theBenchmark for (2972ds/869Mi)
% 218.79/31.33 % (2390276)Instruction limit reached!
% 218.79/31.33 % (2390276)------------------------------
% 218.79/31.33 % (2390276)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 218.79/31.33 % (2390276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.79/31.33 % (2390276)CaDiCaL version: 2.1.3
% 218.79/31.33 % (2390276)Termination reason: Instruction limit
% 218.79/31.33 % (2390276)Termination phase: Saturation
% 218.79/31.33 % (2390276)Time elapsed: 0.265 s
% 218.79/31.33 % (2390276)Peak memory usage: 22 MB
% 218.79/31.33 % (2390276)Instructions burned: 871 (million)
% 218.79/31.33 % (2390278)ott+10_1_sil=32000:tgt=ground:random_seed=1641108178:i=5114:av=off_2970 on theBenchmark for (2970ds/5114Mi)
% 218.79/31.33 % (2390272)Instruction limit reached!
% 218.79/31.33 % (2390272)------------------------------
% 218.79/31.33 % (2390272)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 218.79/31.33 % (2390272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.79/31.33 % (2390272)CaDiCaL version: 2.1.3
% 218.79/31.33 % (2390272)Termination reason: Instruction limit
% 218.79/31.33 % (2390272)Termination phase: Finite model building constraint generation
% 218.79/31.33 % (2390272)Time elapsed: 2.352 s
% 218.79/31.33 % (2390272)Peak memory usage: 522 MB
% 218.79/31.33 % (2390272)Instructions burned: 6326 (million)
% 218.79/31.33 % (2390280)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=425961477:i=54282_2954 on theBenchmark for (2954ds/54282Mi)
% 218.79/31.33 % TRYING [1]
% 218.79/31.33 % TRYING [2]
% 218.79/31.33 % TRYING [3]
% 218.79/31.33 % (2390263)Instruction limit reached!
% 218.79/31.33 % (2390263)------------------------------
% 218.79/31.33 % (2390263)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 218.79/31.33 % (2390263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.79/31.33 % (2390263)CaDiCaL version: 2.1.3
% 218.79/31.33 % (2390263)Termination reason: Instruction limit
% 218.79/31.33 % (2390263)Termination phase: Finite model building constraint generation
% 218.79/31.33 % (2390263)Time elapsed: 3.763 s
% 218.79/31.33 % (2390263)Peak memory usage: 656 MB
% 218.79/31.33 % (2390263)Instructions burned: 9516 (million)
% 218.79/31.33 % (2390278)Instruction limit reached!
% 218.79/31.33 % (2390278)------------------------------
% 218.79/31.33 % (2390278)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 218.79/31.33 % (2390278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.79/31.33 % (2390278)CaDiCaL version: 2.1.3
% 218.79/31.33 % (2390278)Termination reason: Instruction limit
% 218.79/31.33 % (2390278)Termination phase: Saturation
% 218.79/31.33 % (2390278)Time elapsed: 1.592 s
% 218.79/31.33 % (2390278)Peak memory usage: 53 MB
% 218.79/31.33 % (2390278)Instructions burned: 5114 (million)
% 218.79/31.33 % (2390282)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=2542406413:i=3512:aac=none_2953 on theBenchmark for (2953ds/3512Mi)
% 218.79/31.33 % TRYING [4]
% 218.79/31.33 % (2390284)dis+21_1_sil=32000:sas=cadical:random_seed=3448074608:i=3773:amm=off_2953 on theBenchmark for (2953ds/3773Mi)
% 218.79/31.33 % (2390282)Instruction limit reached!
% 218.79/31.33 % (2390282)------------------------------
% 220.71/41.43 % (2390282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.71/41.43 % (2390282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.71/41.43 % (2390282)CaDiCaL version: 2.1.3
% 220.71/41.43 % (2390282)Termination reason: Instruction limit
% 220.71/41.43 % (2390282)Termination phase: Saturation
% 220.71/41.43 % (2390282)Time elapsed: 0.907 s
% 220.71/41.43 % (2390282)Peak memory usage: 31 MB
% 220.71/41.43 % (2390282)Instructions burned: 3513 (million)
% 220.71/41.43 % (2390286)ott+11_1_sil=16000:gs=on:random_seed=2474612445:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2944 on theBenchmark for (2944ds/2251Mi)
% 220.71/41.43 % TRYING [5]
% 220.71/41.43 % (2390286)Instruction limit reached!
% 220.71/41.43 % (2390286)------------------------------
% 220.71/41.43 % (2390286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.71/41.43 % (2390286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.71/41.43 % (2390286)CaDiCaL version: 2.1.3
% 220.71/41.43 % (2390286)Termination reason: Instruction limit
% 220.71/41.43 % (2390286)Termination phase: Saturation
% 220.71/41.43 % (2390286)Time elapsed: 0.646 s
% 220.71/41.43 % (2390286)Peak memory usage: 35 MB
% 220.71/41.43 % (2390286)Instructions burned: 2255 (million)
% 220.71/41.43 % (2390288)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=2850782947:fmbsr=1.6:i=67534_2938 on theBenchmark for (2938ds/67534Mi)
% 220.71/41.43 % TRYING [7]
% 220.71/41.43 % (2390284)Instruction limit reached!
% 220.71/41.43 % (2390284)------------------------------
% 220.71/41.43 % (2390284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.71/41.43 % (2390284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.71/41.43 % (2390284)CaDiCaL version: 2.1.3
% 220.71/41.43 % (2390284)Termination reason: Instruction limit
% 220.71/41.43 % (2390284)Termination phase: Saturation
% 220.71/41.43 % (2390284)Time elapsed: 1.814 s
% 220.71/41.43 % (2390284)Peak memory usage: 32 MB
% 220.71/41.43 % (2390284)Instructions burned: 3773 (million)
% 220.71/41.43 % (2390290)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3008906082:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2935 on theBenchmark for (2935ds/4591Mi)
% 220.71/41.43 % (2390290)Instruction limit reached!
% 220.71/41.43 % (2390290)------------------------------
% 220.71/41.43 % (2390290)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.71/41.43 % (2390290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.71/41.43 % (2390290)CaDiCaL version: 2.1.3
% 220.71/41.43 % (2390290)Termination reason: Instruction limit
% 220.71/41.43 % (2390290)Termination phase: Saturation
% 220.71/41.43 % (2390290)Time elapsed: 1.732 s
% 220.71/41.43 % (2390290)Peak memory usage: 28 MB
% 220.71/41.43 % (2390290)Instructions burned: 4592 (million)
% 220.71/41.43 % (2390292)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3079299042:i=29340_2917 on theBenchmark for (2917ds/29340Mi)
% 220.71/41.43 % (2390262)Instruction limit reached!
% 220.71/41.43 % (2390262)------------------------------
% 220.71/41.43 % (2390262)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.71/41.43 % (2390262)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.71/41.43 % (2390262)CaDiCaL version: 2.1.3
% 220.71/41.43 % (2390262)Termination reason: Instruction limit
% 220.71/41.43 % (2390262)Termination phase: Finite model building SAT solving
% 220.71/41.43 % (2390262)Time elapsed: 12.832 s
% 220.71/41.43 % (2390262)Peak memory usage: 18 MB
% 220.71/41.43 % (2390262)Instructions burned: 22061 (million)
% 220.71/41.43 % (2390294)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=799898309:i=5211_2863 on theBenchmark for (2863ds/5211Mi)
% 220.71/41.43 % (2390294)Instruction limit reached!
% 220.71/41.43 % (2390294)------------------------------
% 220.71/41.43 % (2390294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.71/41.43 % (2390294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.71/41.43 % (2390294)CaDiCaL version: 2.1.3
% 220.71/41.43 % (2390294)Termination reason: Instruction limit
% 220.71/41.43 % (2390294)Termination phase: Saturation
% 220.71/41.43 % (2390294)Time elapsed: 2.552 s
% 220.71/41.43 % (2390294)Peak memory usage: 43 MB
% 220.71/41.43 % (2390294)Instructions burned: 5213 (million)
% 220.71/41.43 % (2390296)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3177835287:i=5497:nm=2_2837 on theBenchmark for (2837ds/5497Mi)
% 220.71/41.43 % TRYING [17]
% 220.71/41.43 % (2390296)Instruction limit reached!
% 220.71/41.43 % (2390296)------------------------------
% 220.71/41.43 % (2390296)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.71/41.43 % (2390296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.71/41.43 % (2390296)CaDiCaL version: 2.1.3
% 220.71/41.43 % (2390296)Termination reason: Instruction limit
% 220.71/41.43 % (2390296)Termination phase: Finite model building constraint generation
% 220.71/41.43 % (2390296)Time elapsed: 2.216 s
% 220.71/41.43 % (2390296)Peak memory usage: 383 MB
% 220.71/41.43 % (2390296)Instructions burned: 5498 (million)
% 220.71/41.43 % (2390300)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=4076922605:fmbsr=2:i=46332_2815 on theBenchmark for (2815ds/46332Mi)
% 220.71/41.43 % TRYING [15]
% 220.71/41.43 % (2390292)Instruction limit reached!
% 220.71/41.43 % (2390292)------------------------------
% 220.71/41.43 % (2390292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.71/41.43 % (2390292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.71/41.43 % (2390292)CaDiCaL version: 2.1.3
% 220.71/41.43 % (2390292)Termination reason: Instruction limit
% 220.71/41.43 % (2390292)Termination phase: Saturation
% 220.71/41.43 % (2390292)Time elapsed: 14.166 s
% 220.71/41.43 % (2390292)Peak memory usage: 168 MB
% 220.71/41.43 % (2390292)Instructions burned: 29341 (million)
% 220.71/41.43 % (2390302)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=111389891:i=14071_2775 on theBenchmark for (2775ds/14071Mi)
% 220.71/41.43 % TRYING [12]
% 220.71/41.43 % (2390230)Instruction limit reached!
% 220.71/41.43 % (2390230)------------------------------
% 220.71/41.43 % (2390230)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.71/41.43 % (2390230)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.71/41.43 % (2390230)CaDiCaL version: 2.1.3
% 220.71/41.43 % (2390230)Termination reason: Instruction limit
% 220.71/41.43 % (2390230)Termination phase: Saturation
% 220.71/41.43 % (2390230)Time elapsed: 24.058 s
% 220.71/41.43 % (2390230)Peak memory usage: 89 MB
% 220.71/41.43 % (2390230)Instructions burned: 88026 (million)
% 220.71/41.43 % (2390304)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4221275855:i=22565:add=on:rawr=on_2758 on theBenchmark for (2758ds/22565Mi)
% 220.71/41.43 % (2390288)Instruction limit reached!
% 220.71/41.43 % (2390288)------------------------------
% 220.71/41.43 % (2390288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.71/41.43 % (2390288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.71/41.43 % (2390288)CaDiCaL version: 2.1.3
% 220.71/41.43 % (2390288)Termination reason: Instruction limit
% 220.71/41.43 % (2390288)Termination phase: Finite model building SAT solving
% 220.71/41.43 % (2390288)Time elapsed: 19.616 s
% 220.71/41.43 % (2390288)Peak memory usage: 38 MB
% 220.71/41.43 % (2390288)Instructions burned: 67535 (million)
% 220.71/41.43 % (2390306)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=2390895019:i=8173:av=off_2741 on theBenchmark for (2741ds/8173Mi)
% 220.71/41.43 % (2390306)Instruction limit reached!
% 220.71/41.43 % (2390306)------------------------------
% 220.71/41.43 % (2390306)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.71/41.43 % (2390306)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.71/41.43 % (2390306)CaDiCaL version: 2.1.3
% 220.71/41.43 % (2390306)Termination reason: Instruction limit
% 220.71/41.43 % (2390306)Termination phase: Saturation
% 220.71/41.43 % (2390306)Time elapsed: 2.330 s
% 220.71/41.43 % (2390306)Peak memory usage: 81 MB
% 220.71/41.43 % (2390306)Instructions burned: 8176 (million)
% 220.71/41.43 % (2390308)dis+10_16:1_sil=16000:random_seed=4238066172:i=9155:fsr=off_2718 on theBenchmark for (2718ds/9155Mi)
% 220.71/41.43 % (2390308)Instruction limit reached!
% 220.71/41.43 % (2390308)------------------------------
% 220.71/41.43 % (2390308)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.71/41.43 % (2390308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.71/41.43 % (2390308)CaDiCaL version: 2.1.3
% 220.71/41.43 % (2390308)Termination reason: Instruction limit
% 220.71/41.43 % (2390308)Termination phase: Saturation
% 220.71/41.43 % (2390308)Time elapsed: 2.504 s
% 220.71/41.43 % (2390308)Peak memory usage: 68 MB
% 220.71/41.43 % (2390308)Instructions burned: 9157 (million)
% 220.71/41.43 % (2390310)ott-3_8_sil=64000:random_seed=4222214912:i=20139:bs=on_2693 on theBenchmark for (2693ds/20139Mi)
% 220.71/41.43 % (2390302)Instruction limit reached!
% 220.71/41.43 % (2390302)------------------------------
% 220.71/41.43 % (2390302)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.71/41.43 % (2390302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.71/41.43 % (2390302)CaDiCaL version: 2.1.3
% 220.71/41.43 % (2390302)Termination reason: Instruction limit
% 220.71/41.43 % (2390302)Termination phase: Finite model building SAT solving
% 220.71/41.43 % (2390302)Time elapsed: 8.444 s
% 220.71/41.43 % (2390302)Peak memory usage: 177 MB
% 220.71/41.43 % (2390302)Instructions burned: 14071 (million)
% 220.71/41.43 % (2390312)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1573043411:fmbsr=2:i=32576_2690 on theBenchmark for (2690ds/32576Mi)
% 220.71/41.43 % TRYING [9]
% 220.71/41.43 % (2390304)Instruction limit reached!
% 220.71/41.43 % (2390304)------------------------------
% 220.71/41.43 % (2390304)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.71/41.43 % (2390304)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.71/41.43 % (2390304)CaDiCaL version: 2.1.3
% 220.71/41.43 % (2390304)Termination reason: Instruction limit
% 220.71/41.43 % (2390304)Termination phase: Saturation
% 220.71/41.43 % (2390304)Time elapsed: 6.834 s
% 220.71/41.43 % (2390304)Peak memory usage: 49 MB
% 220.71/41.43 % (2390304)Instructions burned: 22568 (million)
% 220.71/41.43 % (2390314)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3281524930:i=11404_2690 on theBenchmark for (2690ds/11404Mi)
% 220.71/41.43 % TRYING [6]
% 220.71/41.43 % (2390280)Instruction limit reached!
% 220.71/41.43 % (2390280)------------------------------
% 220.71/41.43 % (2390280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.71/41.43 % (2390280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.71/41.43 % (2390280)CaDiCaL version: 2.1.3
% 220.71/41.43 % (2390280)Termination reason: Instruction limit
% 220.71/41.43 % (2390280)Termination phase: Finite model building SAT solving
% 220.71/41.43 % (2390280)Time elapsed: 30.821 s
% 220.71/41.43 % (2390280)Peak memory usage: 25 MB
% 220.71/41.43 % (2390280)Instructions burned: 54283 (million)
% 220.71/41.43 % (2390316)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1161322417:i=14134_2645 on theBenchmark for (2645ds/14134Mi)
% 220.71/41.43 % (2390314)Instruction limit reached!
% 220.71/41.43 % (2390314)------------------------------
% 220.71/41.43 % (2390314)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.71/41.43 % (2390314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.71/41.43 % (2390314)CaDiCaL version: 2.1.3
% 220.71/41.43 % (2390314)Termination reason: Instruction limit
% 220.71/41.43 % (2390314)Termination phase: Saturation
% 220.71/41.43 % (2390314)Time elapsed: 5.745 s
% 220.71/41.43 % (2390314)Peak memory usage: 132 MB
% 220.71/41.43 % (2390314)Instructions burned: 11405 (million)
% 220.71/41.43 % (2390318)dis+33_16_sil=32000:sac=on:random_seed=1837628954:i=15851:nm=0_2632 on theBenchmark for (2632ds/15851Mi)
% 220.71/41.43 % (2390310)Instruction limit reached!
% 220.71/41.43 % (2390310)------------------------------
% 220.71/41.43 % (2390310)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.71/41.43 % (2390310)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.71/41.43 % (2390310)CaDiCaL version: 2.1.3
% 220.71/41.43 % (2390310)Termination reason: Instruction limit
% 220.71/41.43 % (2390310)Termination phase: Saturation
% 220.71/41.43 % (2390310)Time elapsed: 6.518 s
% 220.71/41.43 % (2390310)Peak memory usage: 89 MB
% 220.71/41.43 % (2390310)Instructions burned: 20141 (million)
% 220.71/41.43 % (2390320)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2936101541:avsq=on:i=17627:add=on:amm=off_2627 on theBenchmark for (2627ds/17627Mi)
% 220.71/41.43 % (2390320)Instruction limit reached!
% 220.71/41.43 % (2390320)------------------------------
% 220.71/41.43 % (2390320)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.71/41.43 % (2390320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.71/41.43 % (2390320)CaDiCaL version: 2.1.3
% 220.71/41.43 % (2390320)Termination reason: Instruction limit
% 220.71/41.43 % (2390320)Termination phase: Saturation
% 220.71/41.43 % (2390320)Time elapsed: 2.964 s
% 220.71/41.43 % (2390320)Peak memory usage: 47 MB
% 220.71/41.43 % (2390320)Instructions burned: 17630 (million)
% 220.71/41.43 % (2390322)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=799787947:s2a=on:i=53295_2598 on theBenchmark for (2598ds/53295Mi)
% 220.71/41.43 % (2390322) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2390223-2390322"...
% 220.71/41.43 % (2390322)...printing done.
% 220.71/41.43 % (2390322)Refutation found. Thanks to Tanya!
% 220.71/41.43 % SZS status Unsatisfiable for theBenchmark
% 220.71/41.43 % SZS output start Proof for theBenchmark
% See solution above
% 220.71/41.44 % (2390322)------------------------------
% 220.71/41.44 % (2390322)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 220.71/41.44 % (2390322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 220.71/41.44 % (2390322)CaDiCaL version: 2.1.3
% 220.71/41.44 % (2390322)Termination reason: Refutation
% 220.71/41.44 % (2390322)Time elapsed: 0.744 s
% 220.71/41.44 % (2390322)Peak memory usage: 47 MB
% 220.71/41.44 % (2390322)Instructions burned: 2412 (million)
% 220.71/41.44 % (2390223)Success in time 41.02 s
% 220.71/41.44 % Vampire exiting
%------------------------------------------------------------------------------