%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GRP419-1 : TPTP v9.3.1. Released v2.6.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n012.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:17:46 AM UTC 2026
% Result : Unsatisfiable 150.90s 32.82s
% Output : Refutation 150.90s
% Verified :
% SZS Type : Refutation
% Derivation depth : 34
% Number of leaves : 55
% Syntax : Number of formulae : 345 ( 61 unt; 53 def)
% Number of atoms : 822 ( 182 equ)
% Maximal formula atoms : 5 ( 2 avg)
% Number of connectives : 916 ( 439 ~; 424 |; 0 &)
% ( 53 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 15 ( 3 avg)
% Number of predicates : 55 ( 53 usr; 54 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 531 ( 0 sgn 531 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X0,X2))) = X1,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',single_axiom) ).
fof(f2,negated_conjecture,
multiply(multiply(inverse(b2),b2),a2) != a2,
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_these_axioms_2) ).
fof(f3,plain,
a2 != multiply(multiply(inverse(b2),b2),a2),
inference(reorient_equations,[],[f2]) ).
fof(f5,definition,
( spl0_1
<=> a2 = multiply(multiply(inverse(b2),b2),a2) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f7,plain,
( a2 != multiply(multiply(inverse(b2),b2),a2)
| spl0_1 ),
inference(avatar_component_clause,[],[f5]) ).
fof(f8,plain,
~ spl0_1,
inference(avatar_split_clause,[],[f3,f5]) ).
fof(f10,definition,
( spl0_2
<=> ! [X2,X0,X1] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X0,X2))) = X1 ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f11,plain,
( ! [X2,X0,X1] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X0,X2))) = X1
| ~ spl0_2 ),
inference(avatar_component_clause,[],[f10]) ).
fof(f12,plain,
spl0_2,
inference(avatar_split_clause,[],[f1,f10]) ).
fof(f13,plain,
( ! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X2,X3)) = inverse(multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X4,inverse(multiply(inverse(X4),X4)))))))),multiply(X1,X4)))
| ~ spl0_2 ),
inference(superposition,[],[f11,f11]) ).
fof(f20,definition,
( spl0_4
<=> ! [X2,X4,X0,X3,X1] : multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X2,X3)) = inverse(multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X4,inverse(multiply(inverse(X4),X4)))))))),multiply(X1,X4))) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f21,plain,
( ! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X2,X3)) = inverse(multiply(inverse(multiply(X1,inverse(multiply(X0,inverse(multiply(X4,inverse(multiply(inverse(X4),X4)))))))),multiply(X1,X4)))
| ~ spl0_4 ),
inference(avatar_component_clause,[],[f20]) ).
fof(f22,plain,
( spl0_4
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f13,f10,f20]) ).
fof(f35,plain,
( ! [X2,X0,X1] : inverse(inverse(multiply(inverse(multiply(X0,inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X0,X2)))) = X1
| ~ spl0_2
| ~ spl0_4 ),
inference(superposition,[],[f11,f21]) ).
fof(f37,plain,
( ! [X2,X0,X1] : multiply(inverse(multiply(X0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X0,X2)) = X1
| ~ spl0_2
| ~ spl0_4 ),
inference(superposition,[],[f11,f21]) ).
fof(f49,definition,
( spl0_7
<=> ! [X2,X0,X1] : multiply(inverse(multiply(X0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X0,X2)) = X1 ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f50,plain,
( ! [X2,X0,X1] : multiply(inverse(multiply(X0,inverse(multiply(inverse(inverse(X1)),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X0,X2)) = X1
| ~ spl0_7 ),
inference(avatar_component_clause,[],[f49]) ).
fof(f51,plain,
( spl0_7
| ~ spl0_2
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f37,f20,f10,f49]) ).
fof(f57,definition,
( spl0_9
<=> ! [X2,X0,X1] : inverse(inverse(multiply(inverse(multiply(X0,inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X0,X2)))) = X1 ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f58,plain,
( ! [X2,X0,X1] : inverse(inverse(multiply(inverse(multiply(X0,inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),multiply(X0,X2)))) = X1
| ~ spl0_9 ),
inference(avatar_component_clause,[],[f57]) ).
fof(f59,plain,
( spl0_9
| ~ spl0_2
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f35,f20,f10,f57]) ).
fof(f106,plain,
( ! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X0)),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),inverse(multiply(inverse(inverse(X3)),inverse(multiply(multiply(X1,X2),inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X2))))))))),X0) = X3
| ~ spl0_7 ),
inference(superposition,[],[f50,f50]) ).
fof(f112,plain,
( ! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X0)),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),inverse(multiply(inverse(X3),inverse(multiply(multiply(X1,X2),inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X2))))))))),X0)) = X3
| ~ spl0_2
| ~ spl0_7 ),
inference(superposition,[],[f11,f50]) ).
fof(f114,definition,
( spl0_20
<=> ! [X0,X3,X2,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X0)),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),inverse(multiply(inverse(X3),inverse(multiply(multiply(X1,X2),inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X2))))))))),X0)) = X3 ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f115,plain,
( ! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X0)),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),inverse(multiply(inverse(X3),inverse(multiply(multiply(X1,X2),inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X2))))))))),X0)) = X3
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f114]) ).
fof(f116,plain,
( spl0_20
| ~ spl0_2
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f112,f49,f10,f114]) ).
fof(f126,definition,
( spl0_23
<=> ! [X0,X3,X2,X1] : multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X0)),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),inverse(multiply(inverse(inverse(X3)),inverse(multiply(multiply(X1,X2),inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X2))))))))),X0) = X3 ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f127,plain,
( ! [X2,X3,X0,X1] : multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X0)),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),inverse(multiply(inverse(inverse(X3)),inverse(multiply(multiply(X1,X2),inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X2))))))))),X0) = X3
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f126]) ).
fof(f128,plain,
( spl0_23
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f106,f49,f126]) ).
fof(f150,plain,
( ! [X2,X3,X0,X1] : inverse(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X0)),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),inverse(multiply(X3,inverse(multiply(multiply(X1,X2),inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X2))))))))),X0))) = X3
| ~ spl0_7
| ~ spl0_9 ),
inference(superposition,[],[f58,f50]) ).
fof(f179,definition,
( spl0_32
<=> ! [X0,X3,X2,X1] : inverse(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X0)),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),inverse(multiply(X3,inverse(multiply(multiply(X1,X2),inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X2))))))))),X0))) = X3 ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f180,plain,
( ! [X2,X3,X0,X1] : inverse(inverse(multiply(inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X0)),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))),inverse(multiply(X3,inverse(multiply(multiply(X1,X2),inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X2))))))))),X0))) = X3
| ~ spl0_32 ),
inference(avatar_component_clause,[],[f179]) ).
fof(f181,plain,
( spl0_32
| ~ spl0_7
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f150,f57,f49,f179]) ).
fof(f524,plain,
( ! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X2,inverse(multiply(inverse(inverse(inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))),inverse(multiply(X4,inverse(multiply(inverse(X4),X4)))))))),inverse(multiply(inverse(X0),inverse(multiply(multiply(X2,X4),inverse(multiply(inverse(multiply(X2,X4)),multiply(X2,X4)))))))) = inverse(multiply(inverse(multiply(X1,X0)),multiply(X1,X3)))
| ~ spl0_2
| ~ spl0_20 ),
inference(superposition,[],[f11,f115]) ).
fof(f637,definition,
( spl0_83
<=> ! [X2,X4,X0,X3,X1] : multiply(inverse(multiply(X2,inverse(multiply(inverse(inverse(inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))),inverse(multiply(X4,inverse(multiply(inverse(X4),X4)))))))),inverse(multiply(inverse(X0),inverse(multiply(multiply(X2,X4),inverse(multiply(inverse(multiply(X2,X4)),multiply(X2,X4)))))))) = inverse(multiply(inverse(multiply(X1,X0)),multiply(X1,X3))) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f638,plain,
( ! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X2,inverse(multiply(inverse(inverse(inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))),inverse(multiply(X4,inverse(multiply(inverse(X4),X4)))))))),inverse(multiply(inverse(X0),inverse(multiply(multiply(X2,X4),inverse(multiply(inverse(multiply(X2,X4)),multiply(X2,X4)))))))) = inverse(multiply(inverse(multiply(X1,X0)),multiply(X1,X3)))
| ~ spl0_83 ),
inference(avatar_component_clause,[],[f637]) ).
fof(f639,plain,
( spl0_83
| ~ spl0_2
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f524,f114,f10,f637]) ).
fof(f1166,plain,
( ! [X2,X0,X1,X5] : inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))) = inverse(multiply(inverse(multiply(X5,X1)),multiply(X5,X2)))
| ~ spl0_83 ),
inference(superposition,[],[f638,f638]) ).
fof(f1200,plain,
( ! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))) = X1
| ~ spl0_20
| ~ spl0_83 ),
inference(superposition,[],[f115,f638]) ).
fof(f1202,plain,
( ! [X2,X0,X1] : inverse(X1) = inverse(inverse(multiply(inverse(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))
| ~ spl0_32
| ~ spl0_83 ),
inference(superposition,[],[f180,f638]) ).
fof(f1210,plain,
( ! [X2,X3,X0,X1,X4] : multiply(inverse(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,X2)))),multiply(inverse(multiply(X3,inverse(multiply(inverse(inverse(inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))),inverse(multiply(X4,inverse(multiply(inverse(X4),X4)))))))),multiply(X3,X4))) = X1
| ~ spl0_7
| ~ spl0_83 ),
inference(superposition,[],[f50,f638]) ).
fof(f1481,plain,
( ! [X2,X0,X1] : multiply(inverse(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,X2)))),inverse(multiply(X2,inverse(multiply(inverse(X2),X2))))) = X1
| ~ spl0_7
| ~ spl0_83 ),
inference(forward_demodulation,[],[f1210,f50]) ).
fof(f1490,definition,
( spl0_214
<=> ! [X2,X0,X1] : inverse(X1) = inverse(inverse(multiply(inverse(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))),inverse(multiply(X2,inverse(multiply(inverse(X2),X2))))))) ),
introduced(definition,[new_symbols(definition,[spl0_214])],[avatar_definition]) ).
fof(f1491,plain,
( ! [X2,X0,X1] : inverse(X1) = inverse(inverse(multiply(inverse(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))
| ~ spl0_214 ),
inference(avatar_component_clause,[],[f1490]) ).
fof(f1492,plain,
( spl0_214
| ~ spl0_32
| ~ spl0_83 ),
inference(avatar_split_clause,[],[f1202,f637,f179,f1490]) ).
fof(f1494,definition,
( spl0_215
<=> ! [X2,X0,X1] : multiply(inverse(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,X2)))),inverse(multiply(X2,inverse(multiply(inverse(X2),X2))))) = X1 ),
introduced(definition,[new_symbols(definition,[spl0_215])],[avatar_definition]) ).
fof(f1495,plain,
( ! [X2,X0,X1] : multiply(inverse(inverse(multiply(inverse(multiply(X0,inverse(X1))),multiply(X0,X2)))),inverse(multiply(X2,inverse(multiply(inverse(X2),X2))))) = X1
| ~ spl0_215 ),
inference(avatar_component_clause,[],[f1494]) ).
fof(f1498,definition,
( spl0_216
<=> ! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))) = X1 ),
introduced(definition,[new_symbols(definition,[spl0_216])],[avatar_definition]) ).
fof(f1499,plain,
( ! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))) = X1
| ~ spl0_216 ),
inference(avatar_component_clause,[],[f1498]) ).
fof(f1500,plain,
( spl0_216
| ~ spl0_20
| ~ spl0_83 ),
inference(avatar_split_clause,[],[f1200,f637,f114,f1498]) ).
fof(f1570,definition,
( spl0_232
<=> ! [X0,X5,X2,X1] : inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))) = inverse(multiply(inverse(multiply(X5,X1)),multiply(X5,X2))) ),
introduced(definition,[new_symbols(definition,[spl0_232])],[avatar_definition]) ).
fof(f1571,plain,
( ! [X2,X0,X1,X5] : inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))) = inverse(multiply(inverse(multiply(X5,X1)),multiply(X5,X2)))
| ~ spl0_232 ),
inference(avatar_component_clause,[],[f1570]) ).
fof(f1572,plain,
( spl0_232
| ~ spl0_83 ),
inference(avatar_split_clause,[],[f1166,f637,f1570]) ).
fof(f1733,plain,
( spl0_215
| ~ spl0_7
| ~ spl0_83 ),
inference(avatar_split_clause,[],[f1481,f637,f49,f1494]) ).
fof(f1915,plain,
( ! [X2,X3,X0,X1,X4] : inverse(inverse(multiply(inverse(multiply(X2,inverse(multiply(X3,inverse(multiply(multiply(X4,X1),inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X1))))))))),multiply(X2,multiply(X4,X1))))) = X3
| ~ spl0_9
| ~ spl0_232 ),
inference(superposition,[],[f58,f1571]) ).
fof(f1932,plain,
( ! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(X4,X1)),multiply(X4,X2)) = inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))),inverse(multiply(X5,inverse(multiply(inverse(X5),X5)))))))),multiply(X3,X5)))
| ~ spl0_2
| ~ spl0_232 ),
inference(superposition,[],[f11,f1571]) ).
fof(f2033,plain,
( ! [X2,X0,X1,X4] : multiply(inverse(multiply(X0,X1)),multiply(X0,X2)) = multiply(inverse(multiply(X4,X1)),multiply(X4,X2))
| ~ spl0_2
| ~ spl0_232 ),
inference(forward_demodulation,[],[f1932,f11]) ).
fof(f2087,definition,
( spl0_309
<=> ! [X4,X0,X3,X2,X1] : inverse(inverse(multiply(inverse(multiply(X2,inverse(multiply(X3,inverse(multiply(multiply(X4,X1),inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X1))))))))),multiply(X2,multiply(X4,X1))))) = X3 ),
introduced(definition,[new_symbols(definition,[spl0_309])],[avatar_definition]) ).
fof(f2088,plain,
( ! [X2,X3,X0,X1,X4] : inverse(inverse(multiply(inverse(multiply(X2,inverse(multiply(X3,inverse(multiply(multiply(X4,X1),inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X1))))))))),multiply(X2,multiply(X4,X1))))) = X3
| ~ spl0_309 ),
inference(avatar_component_clause,[],[f2087]) ).
fof(f2089,plain,
( spl0_309
| ~ spl0_9
| ~ spl0_232 ),
inference(avatar_split_clause,[],[f1915,f1570,f57,f2087]) ).
fof(f2196,definition,
( spl0_333
<=> ! [X0,X6,X2,X1] : multiply(inverse(multiply(X0,X1)),multiply(X0,X2)) = multiply(inverse(multiply(X6,X1)),multiply(X6,X2)) ),
introduced(definition,[new_symbols(definition,[spl0_333])],[avatar_definition]) ).
fof(f2197,plain,
( ! [X2,X0,X1,X6] : multiply(inverse(multiply(X0,X1)),multiply(X0,X2)) = multiply(inverse(multiply(X6,X1)),multiply(X6,X2))
| ~ spl0_333 ),
inference(avatar_component_clause,[],[f2196]) ).
fof(f2201,plain,
( spl0_333
| ~ spl0_2
| ~ spl0_232 ),
inference(avatar_split_clause,[],[f2033,f1570,f10,f2196]) ).
fof(f2267,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_333 ),
inference(superposition,[],[f2197,f2197]) ).
fof(f2385,plain,
( ! [X2,X3,X0,X1,X4,X5] : inverse(multiply(inverse(multiply(X3,X4)),multiply(X3,multiply(X5,X2)))) = inverse(multiply(inverse(multiply(inverse(multiply(X5,X1)),X4)),multiply(inverse(multiply(X0,X1)),multiply(X0,X2))))
| ~ spl0_232
| ~ spl0_333 ),
inference(superposition,[],[f1571,f2197]) ).
fof(f2387,definition,
( spl0_334
<=> ! [X3,X4,X0,X5,X2,X1] : inverse(multiply(inverse(multiply(X3,X4)),multiply(X3,multiply(X5,X2)))) = inverse(multiply(inverse(multiply(inverse(multiply(X5,X1)),X4)),multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))) ),
introduced(definition,[new_symbols(definition,[spl0_334])],[avatar_definition]) ).
fof(f2388,plain,
( ! [X2,X3,X0,X1,X4,X5] : inverse(multiply(inverse(multiply(X3,X4)),multiply(X3,multiply(X5,X2)))) = inverse(multiply(inverse(multiply(inverse(multiply(X5,X1)),X4)),multiply(inverse(multiply(X0,X1)),multiply(X0,X2))))
| ~ spl0_334 ),
inference(avatar_component_clause,[],[f2387]) ).
fof(f2389,plain,
( spl0_334
| ~ spl0_232
| ~ spl0_333 ),
inference(avatar_split_clause,[],[f2385,f2196,f1570,f2387]) ).
fof(f2443,definition,
( spl0_348
<=> ! [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_348])],[avatar_definition]) ).
fof(f2444,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_348 ),
inference(avatar_component_clause,[],[f2443]) ).
fof(f2445,plain,
( spl0_348
| ~ spl0_333 ),
inference(avatar_split_clause,[],[f2267,f2196,f2443]) ).
fof(f2876,plain,
( ! [X2,X3,X0,X1] : inverse(inverse(multiply(inverse(multiply(X1,X0)),multiply(X1,X3)))) = inverse(inverse(multiply(inverse(multiply(X2,X0)),multiply(X2,X3))))
| ~ spl0_9
| ~ spl0_216 ),
inference(superposition,[],[f58,f1499]) ).
fof(f3035,definition,
( spl0_437
<=> ! [X0,X3,X2,X1] : inverse(inverse(multiply(inverse(multiply(X1,X0)),multiply(X1,X3)))) = inverse(inverse(multiply(inverse(multiply(X2,X0)),multiply(X2,X3)))) ),
introduced(definition,[new_symbols(definition,[spl0_437])],[avatar_definition]) ).
fof(f3036,plain,
( ! [X2,X3,X0,X1] : inverse(inverse(multiply(inverse(multiply(X1,X0)),multiply(X1,X3)))) = inverse(inverse(multiply(inverse(multiply(X2,X0)),multiply(X2,X3))))
| ~ spl0_437 ),
inference(avatar_component_clause,[],[f3035]) ).
fof(f3037,plain,
( spl0_437
| ~ spl0_9
| ~ spl0_216 ),
inference(avatar_split_clause,[],[f2876,f1498,f57,f3035]) ).
fof(f9857,plain,
( ! [X2,X0,X1,X6,X4] : inverse(inverse(multiply(inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(X0,inverse(multiply(inverse(multiply(X6,X4)),multiply(X6,X4))))))))),multiply(X1,X0)))) = X2
| ~ spl0_23
| ~ spl0_309 ),
inference(superposition,[],[f2088,f127]) ).
fof(f10118,definition,
( spl0_1369
<=> ! [X4,X0,X6,X2,X1] : inverse(inverse(multiply(inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(X0,inverse(multiply(inverse(multiply(X6,X4)),multiply(X6,X4))))))))),multiply(X1,X0)))) = X2 ),
introduced(definition,[new_symbols(definition,[spl0_1369])],[avatar_definition]) ).
fof(f10119,plain,
( ! [X2,X0,X1,X6,X4] : inverse(inverse(multiply(inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(X0,inverse(multiply(inverse(multiply(X6,X4)),multiply(X6,X4))))))))),multiply(X1,X0)))) = X2
| ~ spl0_1369 ),
inference(avatar_component_clause,[],[f10118]) ).
fof(f10120,plain,
( spl0_1369
| ~ spl0_23
| ~ spl0_309 ),
inference(avatar_split_clause,[],[f9857,f2087,f126,f10118]) ).
fof(f10275,plain,
( ! [X2,X3,X0,X1] : inverse(inverse(multiply(inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(X3,inverse(multiply(inverse(X0),X0)))))))),multiply(X1,X3)))) = X2
| ~ spl0_7
| ~ spl0_1369 ),
inference(superposition,[],[f10119,f50]) ).
fof(f10630,definition,
( spl0_1459
<=> ! [X0,X3,X2,X1] : inverse(inverse(multiply(inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(X3,inverse(multiply(inverse(X0),X0)))))))),multiply(X1,X3)))) = X2 ),
introduced(definition,[new_symbols(definition,[spl0_1459])],[avatar_definition]) ).
fof(f10631,plain,
( ! [X2,X3,X0,X1] : inverse(inverse(multiply(inverse(multiply(X1,inverse(multiply(X2,inverse(multiply(X3,inverse(multiply(inverse(X0),X0)))))))),multiply(X1,X3)))) = X2
| ~ spl0_1459 ),
inference(avatar_component_clause,[],[f10630]) ).
fof(f10638,plain,
( spl0_1459
| ~ spl0_7
| ~ spl0_1369 ),
inference(avatar_split_clause,[],[f10275,f10118,f49,f10630]) ).
fof(f10786,plain,
( ! [X2,X3,X0] : multiply(X0,inverse(multiply(X2,inverse(multiply(inverse(X2),X2))))) = multiply(X0,inverse(multiply(X2,inverse(multiply(inverse(X3),X3)))))
| ~ spl0_215
| ~ spl0_1459 ),
inference(superposition,[],[f1495,f10631]) ).
fof(f10957,definition,
( spl0_1505
<=> ! [X2,X0,X3] : multiply(X0,inverse(multiply(X2,inverse(multiply(inverse(X2),X2))))) = multiply(X0,inverse(multiply(X2,inverse(multiply(inverse(X3),X3))))) ),
introduced(definition,[new_symbols(definition,[spl0_1505])],[avatar_definition]) ).
fof(f10958,plain,
( ! [X2,X3,X0] : multiply(X0,inverse(multiply(X2,inverse(multiply(inverse(X2),X2))))) = multiply(X0,inverse(multiply(X2,inverse(multiply(inverse(X3),X3)))))
| ~ spl0_1505 ),
inference(avatar_component_clause,[],[f10957]) ).
fof(f10959,plain,
( spl0_1505
| ~ spl0_215
| ~ spl0_1459 ),
inference(avatar_split_clause,[],[f10786,f10630,f1494,f10957]) ).
fof(f11346,plain,
( ! [X2,X3,X0,X1] : multiply(X1,inverse(multiply(inverse(X2),X2))) = multiply(inverse(inverse(multiply(inverse(multiply(X0,inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))),multiply(X0,X3)))),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))
| ~ spl0_215
| ~ spl0_1505 ),
inference(superposition,[],[f1495,f10958]) ).
fof(f11368,plain,
( ! [X2,X3,X0,X1] : inverse(multiply(X1,inverse(multiply(inverse(X2),X2)))) = inverse(multiply(inverse(inverse(multiply(inverse(multiply(X0,inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))))),multiply(X0,X3)))),inverse(multiply(X3,inverse(multiply(inverse(X3),X3))))))
| ~ spl0_216
| ~ spl0_1505 ),
inference(superposition,[],[f1499,f10958]) ).
fof(f11560,plain,
( ! [X2,X1] : inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))) = inverse(multiply(X1,inverse(multiply(inverse(X2),X2))))
| ~ spl0_216
| ~ spl0_1505 ),
inference(forward_demodulation,[],[f11368,f1499]) ).
fof(f11630,plain,
( ! [X2,X1] : multiply(X1,inverse(multiply(inverse(X1),X1))) = multiply(X1,inverse(multiply(inverse(X2),X2)))
| ~ spl0_215
| ~ spl0_1505 ),
inference(forward_demodulation,[],[f11346,f1495]) ).
fof(f12181,definition,
( spl0_1721
<=> ! [X2,X1] : inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))) = inverse(multiply(X1,inverse(multiply(inverse(X2),X2)))) ),
introduced(definition,[new_symbols(definition,[spl0_1721])],[avatar_definition]) ).
fof(f12182,plain,
( ! [X2,X1] : inverse(multiply(X1,inverse(multiply(inverse(X1),X1)))) = inverse(multiply(X1,inverse(multiply(inverse(X2),X2))))
| ~ spl0_1721 ),
inference(avatar_component_clause,[],[f12181]) ).
fof(f12183,plain,
( spl0_1721
| ~ spl0_216
| ~ spl0_1505 ),
inference(avatar_split_clause,[],[f11560,f10957,f1498,f12181]) ).
fof(f12189,definition,
( spl0_1723
<=> ! [X2,X1] : multiply(X1,inverse(multiply(inverse(X1),X1))) = multiply(X1,inverse(multiply(inverse(X2),X2))) ),
introduced(definition,[new_symbols(definition,[spl0_1723])],[avatar_definition]) ).
fof(f12190,plain,
( ! [X2,X1] : multiply(X1,inverse(multiply(inverse(X1),X1))) = multiply(X1,inverse(multiply(inverse(X2),X2)))
| ~ spl0_1723 ),
inference(avatar_component_clause,[],[f12189]) ).
fof(f12191,plain,
( spl0_1723
| ~ spl0_215
| ~ spl0_1505 ),
inference(avatar_split_clause,[],[f11630,f10957,f1494,f12189]) ).
fof(f12443,plain,
( ! [X2,X0,X1] : multiply(inverse(X1),X1) = multiply(inverse(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X0),X0)))),multiply(X0,X2)))),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))
| ~ spl0_215
| ~ spl0_1723 ),
inference(superposition,[],[f1495,f12190]) ).
fof(f12462,plain,
( ! [X2,X0,X1] : inverse(inverse(multiply(inverse(X1),X1))) = inverse(inverse(multiply(inverse(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X0),X0)))),multiply(X0,X2)))),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))))
| ~ spl0_214
| ~ spl0_1723 ),
inference(superposition,[],[f1491,f12190]) ).
fof(f12465,plain,
( ! [X2,X0,X1] : inverse(multiply(inverse(X1),X1)) = inverse(multiply(inverse(inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X0),X0)))),multiply(X0,X2)))),inverse(multiply(X2,inverse(multiply(inverse(X2),X2))))))
| ~ spl0_216
| ~ spl0_1723 ),
inference(superposition,[],[f1499,f12190]) ).
fof(f12657,plain,
( ! [X0,X1] : inverse(multiply(inverse(X0),X0)) = inverse(multiply(inverse(X1),X1))
| ~ spl0_216
| ~ spl0_1723 ),
inference(forward_demodulation,[],[f12465,f1499]) ).
fof(f12666,plain,
( ! [X0,X1] : inverse(inverse(multiply(inverse(X0),X0))) = inverse(inverse(multiply(inverse(X1),X1)))
| ~ spl0_214
| ~ spl0_1723 ),
inference(forward_demodulation,[],[f12462,f1491]) ).
fof(f12727,plain,
( ! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(X1),X1)
| ~ spl0_215
| ~ spl0_1723 ),
inference(forward_demodulation,[],[f12443,f1495]) ).
fof(f13299,definition,
( spl0_1910
<=> ! [X0,X1] : inverse(multiply(inverse(X0),X0)) = inverse(multiply(inverse(X1),X1)) ),
introduced(definition,[new_symbols(definition,[spl0_1910])],[avatar_definition]) ).
fof(f13300,plain,
( ! [X0,X1] : inverse(multiply(inverse(X0),X0)) = inverse(multiply(inverse(X1),X1))
| ~ spl0_1910 ),
inference(avatar_component_clause,[],[f13299]) ).
fof(f13301,plain,
( spl0_1910
| ~ spl0_216
| ~ spl0_1723 ),
inference(avatar_split_clause,[],[f12657,f12189,f1498,f13299]) ).
fof(f13303,definition,
( spl0_1911
<=> ! [X0,X1] : inverse(inverse(multiply(inverse(X0),X0))) = inverse(inverse(multiply(inverse(X1),X1))) ),
introduced(definition,[new_symbols(definition,[spl0_1911])],[avatar_definition]) ).
fof(f13304,plain,
( ! [X0,X1] : inverse(inverse(multiply(inverse(X0),X0))) = inverse(inverse(multiply(inverse(X1),X1)))
| ~ spl0_1911 ),
inference(avatar_component_clause,[],[f13303]) ).
fof(f13305,plain,
( spl0_1911
| ~ spl0_214
| ~ spl0_1723 ),
inference(avatar_split_clause,[],[f12666,f12189,f1490,f13303]) ).
fof(f13307,definition,
( spl0_1912
<=> ! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(X1),X1) ),
introduced(definition,[new_symbols(definition,[spl0_1912])],[avatar_definition]) ).
fof(f13308,plain,
( ! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(X1),X1)
| ~ spl0_1912 ),
inference(avatar_component_clause,[],[f13307]) ).
fof(f13309,plain,
( spl0_1912
| ~ spl0_215
| ~ spl0_1723 ),
inference(avatar_split_clause,[],[f12727,f12189,f1494,f13307]) ).
fof(f13649,plain,
( ! [X2,X0] : inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))) = X2
| ~ spl0_216
| ~ spl0_1912 ),
inference(superposition,[],[f1499,f13308]) ).
fof(f13674,plain,
( ! [X0] : a2 != multiply(multiply(inverse(X0),X0),a2)
| spl0_1
| ~ spl0_1912 ),
inference(superposition,[],[f7,f13308]) ).
fof(f14170,definition,
( spl0_2004
<=> ! [X0] : a2 != multiply(multiply(inverse(X0),X0),a2) ),
introduced(definition,[new_symbols(definition,[spl0_2004])],[avatar_definition]) ).
fof(f14171,plain,
( ! [X0] : a2 != multiply(multiply(inverse(X0),X0),a2)
| ~ spl0_2004 ),
inference(avatar_component_clause,[],[f14170]) ).
fof(f14172,plain,
( spl0_2004
| spl0_1
| ~ spl0_1912 ),
inference(avatar_split_clause,[],[f13674,f13307,f5,f14170]) ).
fof(f14200,definition,
( spl0_2011
<=> ! [X2,X0] : inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))) = X2 ),
introduced(definition,[new_symbols(definition,[spl0_2011])],[avatar_definition]) ).
fof(f14201,plain,
( ! [X2,X0] : inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(X2,inverse(multiply(inverse(X2),X2)))))) = X2
| ~ spl0_2011 ),
inference(avatar_component_clause,[],[f14200]) ).
fof(f14202,plain,
( spl0_2011
| ~ spl0_216
| ~ spl0_1912 ),
inference(avatar_split_clause,[],[f13649,f13307,f1498,f14200]) ).
fof(f14917,plain,
( ! [X2,X0,X1] : multiply(inverse(X2),X2) = multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X1),X1))
| ~ spl0_1910
| ~ spl0_1912 ),
inference(superposition,[],[f13308,f13300]) ).
fof(f14924,definition,
( spl0_2065
<=> ! [X2,X0,X1] : multiply(inverse(X2),X2) = multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X1),X1)) ),
introduced(definition,[new_symbols(definition,[spl0_2065])],[avatar_definition]) ).
fof(f14925,plain,
( ! [X2,X0,X1] : multiply(inverse(X2),X2) = multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X1),X1))
| ~ spl0_2065 ),
inference(avatar_component_clause,[],[f14924]) ).
fof(f14926,plain,
( spl0_2065
| ~ spl0_1910
| ~ spl0_1912 ),
inference(avatar_split_clause,[],[f14917,f13307,f13299,f14924]) ).
fof(f15406,plain,
( ! [X2,X0,X1] : multiply(inverse(X2),X2) = multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X1),X1)))
| ~ spl0_1911
| ~ spl0_1912 ),
inference(superposition,[],[f13308,f13304]) ).
fof(f15413,definition,
( spl0_2118
<=> ! [X2,X0,X1] : multiply(inverse(X2),X2) = multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X1),X1))) ),
introduced(definition,[new_symbols(definition,[spl0_2118])],[avatar_definition]) ).
fof(f15414,plain,
( ! [X2,X0,X1] : multiply(inverse(X2),X2) = multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(inverse(X1),X1)))
| ~ spl0_2118 ),
inference(avatar_component_clause,[],[f15413]) ).
fof(f15415,plain,
( spl0_2118
| ~ spl0_1911
| ~ spl0_1912 ),
inference(avatar_split_clause,[],[f15406,f13307,f13303,f15413]) ).
fof(f23914,plain,
( ! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(X2,inverse(multiply(inverse(X0),X0)))))) = X2
| ~ spl0_1912
| ~ spl0_2011 ),
inference(superposition,[],[f14201,f13308]) ).
fof(f24371,definition,
( spl0_3364
<=> ! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(X1,inverse(multiply(inverse(X2),X2)))))) = X1 ),
introduced(definition,[new_symbols(definition,[spl0_3364])],[avatar_definition]) ).
fof(f24372,plain,
( ! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),inverse(multiply(X1,inverse(multiply(inverse(X2),X2)))))) = X1
| ~ spl0_3364 ),
inference(avatar_component_clause,[],[f24371]) ).
fof(f24426,plain,
( spl0_3364
| ~ spl0_1912
| ~ spl0_2011 ),
inference(avatar_split_clause,[],[f23914,f14200,f13307,f24371]) ).
fof(f24858,plain,
( ! [X2,X0] : inverse(multiply(inverse(X0),X0)) = inverse(inverse(multiply(inverse(X2),X2)))
| ~ spl0_2118
| ~ spl0_3364 ),
inference(superposition,[],[f24372,f15414]) ).
fof(f24920,plain,
( ! [X2,X0,X1] : multiply(inverse(X1),X1) = multiply(inverse(inverse(multiply(inverse(X0),X0))),multiply(inverse(X2),X2))
| ~ spl0_2065
| ~ spl0_3364 ),
inference(superposition,[],[f14925,f24372]) ).
fof(f25392,definition,
( spl0_3522
<=> ! [X2,X0,X1] : multiply(inverse(X1),X1) = multiply(inverse(inverse(multiply(inverse(X0),X0))),multiply(inverse(X2),X2)) ),
introduced(definition,[new_symbols(definition,[spl0_3522])],[avatar_definition]) ).
fof(f25393,plain,
( ! [X2,X0,X1] : multiply(inverse(X1),X1) = multiply(inverse(inverse(multiply(inverse(X0),X0))),multiply(inverse(X2),X2))
| ~ spl0_3522 ),
inference(avatar_component_clause,[],[f25392]) ).
fof(f25394,plain,
( spl0_3522
| ~ spl0_2065
| ~ spl0_3364 ),
inference(avatar_split_clause,[],[f24920,f24371,f14924,f25392]) ).
fof(f25412,definition,
( spl0_3527
<=> ! [X0,X1] : inverse(multiply(inverse(X1),X1)) = inverse(inverse(multiply(inverse(X0),X0))) ),
introduced(definition,[new_symbols(definition,[spl0_3527])],[avatar_definition]) ).
fof(f25413,plain,
( ! [X0,X1] : inverse(multiply(inverse(X1),X1)) = inverse(inverse(multiply(inverse(X0),X0)))
| ~ spl0_3527 ),
inference(avatar_component_clause,[],[f25412]) ).
fof(f25519,plain,
( spl0_3527
| ~ spl0_2118
| ~ spl0_3364 ),
inference(avatar_split_clause,[],[f24858,f24371,f15413,f25412]) ).
fof(f26226,plain,
( ! [X2,X3,X0,X1] : inverse(multiply(inverse(X2),X2)) = inverse(multiply(inverse(multiply(X1,inverse(multiply(inverse(multiply(inverse(X0),X0)),inverse(multiply(X3,inverse(multiply(inverse(X3),X3)))))))),multiply(X1,X3)))
| ~ spl0_2
| ~ spl0_3527 ),
inference(superposition,[],[f11,f25413]) ).
fof(f26485,plain,
( ! [X2,X0] : inverse(multiply(inverse(X2),X2)) = multiply(inverse(X0),X0)
| ~ spl0_2
| ~ spl0_3527 ),
inference(forward_demodulation,[],[f26226,f11]) ).
fof(f27305,definition,
( spl0_3861
<=> ! [X2,X0] : inverse(multiply(inverse(X2),X2)) = multiply(inverse(X0),X0) ),
introduced(definition,[new_symbols(definition,[spl0_3861])],[avatar_definition]) ).
fof(f27306,plain,
( ! [X2,X0] : inverse(multiply(inverse(X2),X2)) = multiply(inverse(X0),X0)
| ~ spl0_3861 ),
inference(avatar_component_clause,[],[f27305]) ).
fof(f27328,plain,
( spl0_3861
| ~ spl0_2
| ~ spl0_3527 ),
inference(avatar_split_clause,[],[f26485,f25412,f10,f27305]) ).
fof(f27373,plain,
( ! [X2,X0,X1] : multiply(inverse(X2),X2) = inverse(multiply(multiply(inverse(X0),X0),multiply(inverse(X1),X1)))
| ~ spl0_3861 ),
inference(superposition,[],[f27306,f27306]) ).
fof(f27407,plain,
( ! [X2,X0] : multiply(inverse(X2),X2) = inverse(inverse(multiply(inverse(X0),X0)))
| ~ spl0_3861 ),
inference(superposition,[],[f27306,f27306]) ).
fof(f27755,plain,
( ! [X0] : a2 != multiply(inverse(multiply(inverse(X0),X0)),a2)
| ~ spl0_2004
| ~ spl0_3861 ),
inference(superposition,[],[f14171,f27306]) ).
fof(f28147,definition,
( spl0_3914
<=> ! [X0] : a2 != multiply(inverse(multiply(inverse(X0),X0)),a2) ),
introduced(definition,[new_symbols(definition,[spl0_3914])],[avatar_definition]) ).
fof(f28148,plain,
( ! [X0] : a2 != multiply(inverse(multiply(inverse(X0),X0)),a2)
| ~ spl0_3914 ),
inference(avatar_component_clause,[],[f28147]) ).
fof(f28175,plain,
( spl0_3914
| ~ spl0_2004
| ~ spl0_3861 ),
inference(avatar_split_clause,[],[f27755,f27305,f14170,f28147]) ).
fof(f28612,definition,
( spl0_4026
<=> ! [X0,X1] : multiply(inverse(X0),X0) = inverse(inverse(multiply(inverse(X1),X1))) ),
introduced(definition,[new_symbols(definition,[spl0_4026])],[avatar_definition]) ).
fof(f28613,plain,
( ! [X0,X1] : multiply(inverse(X0),X0) = inverse(inverse(multiply(inverse(X1),X1)))
| ~ spl0_4026 ),
inference(avatar_component_clause,[],[f28612]) ).
fof(f28896,plain,
( spl0_4026
| ~ spl0_3861 ),
inference(avatar_split_clause,[],[f27407,f27305,f28612]) ).
fof(f28959,definition,
( spl0_4105
<=> ! [X2,X0,X1] : multiply(inverse(X2),X2) = inverse(multiply(multiply(inverse(X0),X0),multiply(inverse(X1),X1))) ),
introduced(definition,[new_symbols(definition,[spl0_4105])],[avatar_definition]) ).
fof(f28960,plain,
( ! [X2,X0,X1] : multiply(inverse(X2),X2) = inverse(multiply(multiply(inverse(X0),X0),multiply(inverse(X1),X1)))
| ~ spl0_4105 ),
inference(avatar_component_clause,[],[f28959]) ).
fof(f28961,plain,
( spl0_4105
| ~ spl0_3861 ),
inference(avatar_split_clause,[],[f27373,f27305,f28959]) ).
fof(f30009,plain,
( ! [X2,X3,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(X2,inverse(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(X3),X3)))))))) = X2
| ~ spl0_3364
| ~ spl0_4026 ),
inference(superposition,[],[f24372,f28613]) ).
fof(f30046,definition,
( spl0_4203
<=> ! [X0,X3,X2,X1] : inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(X2,inverse(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(X3),X3)))))))) = X2 ),
introduced(definition,[new_symbols(definition,[spl0_4203])],[avatar_definition]) ).
fof(f30047,plain,
( ! [X2,X3,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(X2,inverse(multiply(multiply(inverse(X0),X0),inverse(multiply(inverse(X3),X3)))))))) = X2
| ~ spl0_4203 ),
inference(avatar_component_clause,[],[f30046]) ).
fof(f30048,plain,
( spl0_4203
| ~ spl0_3364
| ~ spl0_4026 ),
inference(avatar_split_clause,[],[f30009,f28612,f24371,f30046]) ).
fof(f70994,plain,
( ! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(inverse(X2),inverse(multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3))))))))),multiply(inverse(X0),X0))) = X2
| ~ spl0_2
| ~ spl0_3522 ),
inference(superposition,[],[f11,f25393]) ).
fof(f70999,plain,
( ! [X2,X3,X0,X1] : inverse(inverse(multiply(inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),inverse(multiply(X2,inverse(multiply(multiply(inverse(X3),X3),inverse(multiply(inverse(multiply(inverse(X3),X3)),multiply(inverse(X3),X3))))))))),multiply(inverse(X0),X0)))) = X2
| ~ spl0_9
| ~ spl0_3522 ),
inference(superposition,[],[f58,f25393]) ).
fof(f71228,plain,
( ! [X2,X0] : inverse(inverse(multiply(X2,multiply(inverse(X0),X0)))) = X2
| ~ spl0_9
| ~ spl0_3522
| ~ spl0_4203 ),
inference(forward_demodulation,[],[f70999,f30047]) ).
fof(f71233,plain,
( ! [X2,X0] : inverse(multiply(inverse(X2),multiply(inverse(X0),X0))) = X2
| ~ spl0_2
| ~ spl0_3522
| ~ spl0_4203 ),
inference(forward_demodulation,[],[f70994,f30047]) ).
fof(f72451,definition,
( spl0_10843
<=> ! [X2,X0] : inverse(inverse(multiply(X2,multiply(inverse(X0),X0)))) = X2 ),
introduced(definition,[new_symbols(definition,[spl0_10843])],[avatar_definition]) ).
fof(f72452,plain,
( ! [X2,X0] : inverse(inverse(multiply(X2,multiply(inverse(X0),X0)))) = X2
| ~ spl0_10843 ),
inference(avatar_component_clause,[],[f72451]) ).
fof(f72488,plain,
( spl0_10843
| ~ spl0_9
| ~ spl0_3522
| ~ spl0_4203 ),
inference(avatar_split_clause,[],[f71228,f30046,f25392,f57,f72451]) ).
fof(f72502,definition,
( spl0_10855
<=> ! [X2,X0] : inverse(multiply(inverse(X2),multiply(inverse(X0),X0))) = X2 ),
introduced(definition,[new_symbols(definition,[spl0_10855])],[avatar_definition]) ).
fof(f72503,plain,
( ! [X2,X0] : inverse(multiply(inverse(X2),multiply(inverse(X0),X0))) = X2
| ~ spl0_10855 ),
inference(avatar_component_clause,[],[f72502]) ).
fof(f72504,plain,
( spl0_10855
| ~ spl0_2
| ~ spl0_3522
| ~ spl0_4203 ),
inference(avatar_split_clause,[],[f71233,f30046,f25392,f10,f72502]) ).
fof(f72613,plain,
( ! [X2,X0,X1] : inverse(inverse(multiply(X2,inverse(multiply(multiply(inverse(X0),X0),multiply(inverse(X1),X1)))))) = X2
| ~ spl0_4105
| ~ spl0_10843 ),
inference(superposition,[],[f72452,f28960]) ).
fof(f72631,plain,
( ! [X2,X0,X1] : inverse(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))) = inverse(multiply(inverse(X2),X1))
| ~ spl0_333
| ~ spl0_10843 ),
inference(superposition,[],[f72452,f2197]) ).
fof(f73409,definition,
( spl0_10986
<=> ! [X2,X0,X1] : inverse(inverse(multiply(inverse(multiply(X2,X1)),multiply(X2,X0)))) = inverse(multiply(inverse(X0),X1)) ),
introduced(definition,[new_symbols(definition,[spl0_10986])],[avatar_definition]) ).
fof(f73410,plain,
( ! [X2,X0,X1] : inverse(inverse(multiply(inverse(multiply(X2,X1)),multiply(X2,X0)))) = inverse(multiply(inverse(X0),X1))
| ~ spl0_10986 ),
inference(avatar_component_clause,[],[f73409]) ).
fof(f73489,plain,
( spl0_10986
| ~ spl0_333
| ~ spl0_10843 ),
inference(avatar_split_clause,[],[f72631,f72451,f2196,f73409]) ).
fof(f73537,definition,
( spl0_11012
<=> ! [X2,X0,X1] : inverse(inverse(multiply(X2,inverse(multiply(multiply(inverse(X0),X0),multiply(inverse(X1),X1)))))) = X2 ),
introduced(definition,[new_symbols(definition,[spl0_11012])],[avatar_definition]) ).
fof(f73538,plain,
( ! [X2,X0,X1] : inverse(inverse(multiply(X2,inverse(multiply(multiply(inverse(X0),X0),multiply(inverse(X1),X1)))))) = X2
| ~ spl0_11012 ),
inference(avatar_component_clause,[],[f73537]) ).
fof(f73539,plain,
( spl0_11012
| ~ spl0_4105
| ~ spl0_10843 ),
inference(avatar_split_clause,[],[f72613,f72451,f28959,f73537]) ).
fof(f74885,plain,
( ! [X0,X1] : inverse(multiply(inverse(X1),inverse(multiply(inverse(X0),X0)))) = X1
| ~ spl0_3861
| ~ spl0_10855 ),
inference(superposition,[],[f72503,f27306]) ).
fof(f74907,plain,
( ! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(inverse(multiply(X0,X1)),X2)),multiply(inverse(multiply(X3,X1)),multiply(X3,X4)))) = multiply(inverse(multiply(X0,X4)),X2)
| ~ spl0_348
| ~ spl0_10855 ),
inference(superposition,[],[f72503,f2444]) ).
fof(f74980,plain,
( ! [X2,X0,X1] : inverse(X1) = inverse(inverse(multiply(inverse(inverse(multiply(inverse(multiply(X2,X1)),multiply(X2,multiply(inverse(X0),X0))))),inverse(multiply(multiply(inverse(X0),X0),multiply(inverse(X0),X0))))))
| ~ spl0_214
| ~ spl0_10855 ),
inference(superposition,[],[f1491,f72503]) ).
fof(f75120,plain,
( ! [X2,X3,X0,X1] : inverse(inverse(multiply(inverse(multiply(X1,multiply(inverse(X2),X2))),multiply(X1,X3)))) = inverse(inverse(multiply(X0,multiply(inverse(X0),X3))))
| ~ spl0_437
| ~ spl0_10855 ),
inference(superposition,[],[f3036,f72503]) ).
fof(f75705,plain,
( ! [X2,X3,X0] : inverse(multiply(inverse(X3),multiply(inverse(X2),X2))) = inverse(inverse(multiply(X0,multiply(inverse(X0),X3))))
| ~ spl0_437
| ~ spl0_10855
| ~ spl0_10986 ),
inference(forward_demodulation,[],[f75120,f73410]) ).
fof(f75805,definition,
( spl0_11324
<=> ! [X4,X0,X3,X2,X1] : multiply(inverse(multiply(X0,X1)),X2) = inverse(multiply(inverse(multiply(inverse(multiply(X0,X3)),X2)),multiply(inverse(multiply(X4,X3)),multiply(X4,X1)))) ),
introduced(definition,[new_symbols(definition,[spl0_11324])],[avatar_definition]) ).
fof(f75806,plain,
( ! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X0,X1)),X2) = inverse(multiply(inverse(multiply(inverse(multiply(X0,X3)),X2)),multiply(inverse(multiply(X4,X3)),multiply(X4,X1))))
| ~ spl0_11324 ),
inference(avatar_component_clause,[],[f75805]) ).
fof(f75833,plain,
( ! [X2,X0,X1] : inverse(X1) = inverse(inverse(multiply(inverse(multiply(X2,X1)),multiply(X2,multiply(inverse(X0),X0)))))
| ~ spl0_214
| ~ spl0_10855
| ~ spl0_11012 ),
inference(forward_demodulation,[],[f74980,f73538]) ).
fof(f75837,definition,
( spl0_11331
<=> ! [X0,X1] : inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))) = X0 ),
introduced(definition,[new_symbols(definition,[spl0_11331])],[avatar_definition]) ).
fof(f75838,plain,
( ! [X0,X1] : inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))) = X0
| ~ spl0_11331 ),
inference(avatar_component_clause,[],[f75837]) ).
fof(f75857,plain,
( spl0_11324
| ~ spl0_348
| ~ spl0_10855 ),
inference(avatar_split_clause,[],[f74907,f72502,f2443,f75805]) ).
fof(f75906,plain,
( spl0_11331
| ~ spl0_3861
| ~ spl0_10855 ),
inference(avatar_split_clause,[],[f74885,f72502,f27305,f75837]) ).
fof(f76147,plain,
( ! [X3,X0] : inverse(inverse(multiply(X0,multiply(inverse(X0),X3)))) = X3
| ~ spl0_437
| ~ spl0_10855
| ~ spl0_10986 ),
inference(forward_demodulation,[],[f75705,f72503]) ).
fof(f76178,plain,
( ! [X0,X1] : inverse(X1) = inverse(multiply(inverse(multiply(inverse(X0),X0)),X1))
| ~ spl0_214
| ~ spl0_10855
| ~ spl0_10986
| ~ spl0_11012 ),
inference(forward_demodulation,[],[f75833,f73410]) ).
fof(f76236,definition,
( spl0_11404
<=> ! [X0,X3] : inverse(inverse(multiply(X0,multiply(inverse(X0),X3)))) = X3 ),
introduced(definition,[new_symbols(definition,[spl0_11404])],[avatar_definition]) ).
fof(f76237,plain,
( ! [X3,X0] : inverse(inverse(multiply(X0,multiply(inverse(X0),X3)))) = X3
| ~ spl0_11404 ),
inference(avatar_component_clause,[],[f76236]) ).
fof(f76238,plain,
( spl0_11404
| ~ spl0_437
| ~ spl0_10855
| ~ spl0_10986 ),
inference(avatar_split_clause,[],[f76147,f73409,f72502,f3035,f76236]) ).
fof(f76257,definition,
( spl0_11409
<=> ! [X0,X1] : inverse(X1) = inverse(multiply(inverse(multiply(inverse(X0),X0)),X1)) ),
introduced(definition,[new_symbols(definition,[spl0_11409])],[avatar_definition]) ).
fof(f76258,plain,
( ! [X0,X1] : inverse(X1) = inverse(multiply(inverse(multiply(inverse(X0),X0)),X1))
| ~ spl0_11409 ),
inference(avatar_component_clause,[],[f76257]) ).
fof(f76259,plain,
( spl0_11409
| ~ spl0_214
| ~ spl0_10855
| ~ spl0_10986
| ~ spl0_11012 ),
inference(avatar_split_clause,[],[f76178,f73537,f73409,f72502,f1490,f76257]) ).
fof(f76427,plain,
( ! [X2,X0,X1] : inverse(inverse(multiply(inverse(multiply(inverse(X1),X1)),multiply(inverse(multiply(inverse(X0),X0)),X2)))) = X2
| ~ spl0_3527
| ~ spl0_11404 ),
inference(superposition,[],[f76237,f25413]) ).
fof(f77175,plain,
( ! [X2,X0] : inverse(inverse(multiply(inverse(multiply(inverse(X0),X0)),X2))) = X2
| ~ spl0_3527
| ~ spl0_11404
| ~ spl0_11409 ),
inference(forward_demodulation,[],[f76427,f76258]) ).
fof(f77385,plain,
( ! [X2] : inverse(inverse(X2)) = X2
| ~ spl0_3527
| ~ spl0_11404
| ~ spl0_11409 ),
inference(forward_demodulation,[],[f77175,f76258]) ).
fof(f77505,definition,
( spl0_11608
<=> ! [X2] : inverse(inverse(X2)) = X2 ),
introduced(definition,[new_symbols(definition,[spl0_11608])],[avatar_definition]) ).
fof(f77506,plain,
( ! [X2] : inverse(inverse(X2)) = X2
| ~ spl0_11608 ),
inference(avatar_component_clause,[],[f77505]) ).
fof(f77507,plain,
( spl0_11608
| ~ spl0_3527
| ~ spl0_11404
| ~ spl0_11409 ),
inference(avatar_split_clause,[],[f77385,f76257,f76236,f25412,f77505]) ).
fof(f77872,plain,
( ! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,inverse(X0))))),inverse(multiply(inverse(X0),inverse(multiply(X0,inverse(X0))))))) = X2
| ~ spl0_216
| ~ spl0_11608 ),
inference(superposition,[],[f1499,f77506]) ).
fof(f77877,plain,
( ! [X0,X1] : inverse(multiply(inverse(X0),inverse(multiply(inverse(X1),X1)))) = inverse(multiply(inverse(X0),inverse(multiply(X0,inverse(X0)))))
| ~ spl0_1721
| ~ spl0_11608 ),
inference(superposition,[],[f12182,f77506]) ).
fof(f77924,plain,
( ! [X0] : a2 != multiply(inverse(multiply(X0,inverse(X0))),a2)
| ~ spl0_3914
| ~ spl0_11608 ),
inference(superposition,[],[f28148,f77506]) ).
fof(f77981,plain,
( ! [X0,X1] : inverse(inverse(multiply(X1,multiply(X0,inverse(X0))))) = X1
| ~ spl0_10843
| ~ spl0_11608 ),
inference(superposition,[],[f72452,f77506]) ).
fof(f78001,plain,
( ! [X0,X1] : multiply(X1,multiply(X0,inverse(X0))) = X1
| ~ spl0_10843
| ~ spl0_11608 ),
inference(forward_demodulation,[],[f77981,f77506]) ).
fof(f78127,definition,
( spl0_11662
<=> ! [X0] : a2 != multiply(inverse(multiply(X0,inverse(X0))),a2) ),
introduced(definition,[new_symbols(definition,[spl0_11662])],[avatar_definition]) ).
fof(f78128,plain,
( ! [X0] : a2 != multiply(inverse(multiply(X0,inverse(X0))),a2)
| ~ spl0_11662 ),
inference(avatar_component_clause,[],[f78127]) ).
fof(f78129,plain,
( spl0_11662
| ~ spl0_3914
| ~ spl0_11608 ),
inference(avatar_split_clause,[],[f77924,f77505,f28147,f78127]) ).
fof(f78223,plain,
( ! [X0] : inverse(multiply(inverse(X0),inverse(multiply(X0,inverse(X0))))) = X0
| ~ spl0_1721
| ~ spl0_11331
| ~ spl0_11608 ),
inference(forward_demodulation,[],[f77877,f75838]) ).
fof(f78230,plain,
( ! [X2,X0] : inverse(multiply(inverse(multiply(inverse(inverse(X0)),X2)),inverse(multiply(inverse(X0),inverse(multiply(X0,inverse(X0))))))) = X2
| ~ spl0_216
| ~ spl0_10986
| ~ spl0_11608 ),
inference(forward_demodulation,[],[f77872,f73410]) ).
fof(f78370,definition,
( spl0_11693
<=> ! [X0,X1] : multiply(X1,multiply(X0,inverse(X0))) = X1 ),
introduced(definition,[new_symbols(definition,[spl0_11693])],[avatar_definition]) ).
fof(f78371,plain,
( ! [X0,X1] : multiply(X1,multiply(X0,inverse(X0))) = X1
| ~ spl0_11693 ),
inference(avatar_component_clause,[],[f78370]) ).
fof(f78373,plain,
( spl0_11693
| ~ spl0_10843
| ~ spl0_11608 ),
inference(avatar_split_clause,[],[f78001,f77505,f72451,f78370]) ).
fof(f78438,definition,
( spl0_11698
<=> ! [X0] : inverse(multiply(inverse(X0),inverse(multiply(X0,inverse(X0))))) = X0 ),
introduced(definition,[new_symbols(definition,[spl0_11698])],[avatar_definition]) ).
fof(f78439,plain,
( ! [X0] : inverse(multiply(inverse(X0),inverse(multiply(X0,inverse(X0))))) = X0
| ~ spl0_11698 ),
inference(avatar_component_clause,[],[f78438]) ).
fof(f78440,plain,
( spl0_11698
| ~ spl0_1721
| ~ spl0_11331
| ~ spl0_11608 ),
inference(avatar_split_clause,[],[f78223,f77505,f75837,f12181,f78438]) ).
fof(f78449,plain,
( ! [X2,X0] : inverse(multiply(inverse(multiply(X0,X2)),inverse(multiply(inverse(X0),inverse(multiply(X0,inverse(X0))))))) = X2
| ~ spl0_216
| ~ spl0_10986
| ~ spl0_11608 ),
inference(forward_demodulation,[],[f78230,f77506]) ).
fof(f78591,definition,
( spl0_11720
<=> ! [X2,X0] : inverse(multiply(inverse(multiply(X0,X2)),inverse(multiply(inverse(X0),inverse(multiply(X0,inverse(X0))))))) = X2 ),
introduced(definition,[new_symbols(definition,[spl0_11720])],[avatar_definition]) ).
fof(f78592,plain,
( ! [X2,X0] : inverse(multiply(inverse(multiply(X0,X2)),inverse(multiply(inverse(X0),inverse(multiply(X0,inverse(X0))))))) = X2
| ~ spl0_11720 ),
inference(avatar_component_clause,[],[f78591]) ).
fof(f78593,plain,
( spl0_11720
| ~ spl0_216
| ~ spl0_10986
| ~ spl0_11608 ),
inference(avatar_split_clause,[],[f78449,f77505,f73409,f1498,f78591]) ).
fof(f78728,plain,
( ! [X2,X0] : inverse(multiply(inverse(multiply(X0,X2)),X0)) = X2
| ~ spl0_11698
| ~ spl0_11720 ),
inference(forward_demodulation,[],[f78592,f78439]) ).
fof(f78768,definition,
( spl0_11746
<=> ! [X2,X0] : inverse(multiply(inverse(multiply(X0,X2)),X0)) = X2 ),
introduced(definition,[new_symbols(definition,[spl0_11746])],[avatar_definition]) ).
fof(f78769,plain,
( ! [X2,X0] : inverse(multiply(inverse(multiply(X0,X2)),X0)) = X2
| ~ spl0_11746 ),
inference(avatar_component_clause,[],[f78768]) ).
fof(f78770,plain,
( spl0_11746
| ~ spl0_11698
| ~ spl0_11720 ),
inference(avatar_split_clause,[],[f78728,f78591,f78438,f78768]) ).
fof(f82470,plain,
( ! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(X0,X1)),X0)) = inverse(multiply(inverse(multiply(inverse(multiply(X2,X3)),X1)),multiply(inverse(multiply(X4,X3)),multiply(X4,inverse(X2)))))
| ~ spl0_334
| ~ spl0_11693 ),
inference(superposition,[],[f2388,f78371]) ).
fof(f82646,plain,
( ! [X2,X0,X1] : inverse(multiply(inverse(multiply(X0,X1)),X0)) = multiply(inverse(multiply(X2,inverse(X2))),X1)
| ~ spl0_334
| ~ spl0_11324
| ~ spl0_11693 ),
inference(forward_demodulation,[],[f82470,f75806]) ).
fof(f82998,plain,
( ! [X2,X1] : multiply(inverse(multiply(X2,inverse(X2))),X1) = X1
| ~ spl0_334
| ~ spl0_11324
| ~ spl0_11693
| ~ spl0_11746 ),
inference(forward_demodulation,[],[f82646,f78769]) ).
fof(f83249,definition,
( spl0_11867
<=> ! [X2,X3] : multiply(inverse(multiply(X3,inverse(X3))),X2) = X2 ),
introduced(definition,[new_symbols(definition,[spl0_11867])],[avatar_definition]) ).
fof(f83250,plain,
( ! [X2,X3] : multiply(inverse(multiply(X3,inverse(X3))),X2) = X2
| ~ spl0_11867 ),
inference(avatar_component_clause,[],[f83249]) ).
fof(f83291,plain,
( spl0_11867
| ~ spl0_334
| ~ spl0_11324
| ~ spl0_11693
| ~ spl0_11746 ),
inference(avatar_split_clause,[],[f82998,f78768,f78370,f75805,f2387,f83249]) ).
fof(f84281,plain,
( $false
| ~ spl0_11662
| ~ spl0_11867 ),
inference(backward_subsumption_resolution,[],[f78128,f83250]) ).
fof(f84282,plain,
( ~ spl0_11662
| ~ spl0_11867 ),
inference(avatar_contradiction_clause,[],[f84281]) ).
cnf(s1,plain,
~ spl0_1,
inference(sat_conversion,[],[f8]) ).
cnf(s2,plain,
spl0_2,
inference(sat_conversion,[],[f12]) ).
cnf(s4,plain,
( ~ spl0_2
| spl0_4 ),
inference(sat_conversion,[],[f22]) ).
cnf(s7,plain,
( ~ spl0_2
| ~ spl0_4
| spl0_7 ),
inference(sat_conversion,[],[f51]) ).
cnf(s9,plain,
( ~ spl0_2
| ~ spl0_4
| spl0_9 ),
inference(sat_conversion,[],[f59]) ).
cnf(s22,plain,
( ~ spl0_2
| ~ spl0_7
| spl0_20 ),
inference(sat_conversion,[],[f116]) ).
cnf(s25,plain,
( ~ spl0_7
| spl0_23 ),
inference(sat_conversion,[],[f128]) ).
cnf(s34,plain,
( ~ spl0_7
| ~ spl0_9
| spl0_32 ),
inference(sat_conversion,[],[f181]) ).
cnf(s131,plain,
( ~ spl0_2
| ~ spl0_20
| spl0_83 ),
inference(sat_conversion,[],[f639]) ).
cnf(s296,plain,
( ~ spl0_32
| ~ spl0_83
| spl0_214 ),
inference(sat_conversion,[],[f1492]) ).
cnf(s298,plain,
( ~ spl0_20
| ~ spl0_83
| spl0_216 ),
inference(sat_conversion,[],[f1500]) ).
cnf(s325,plain,
( ~ spl0_83
| spl0_232 ),
inference(sat_conversion,[],[f1572]) ).
cnf(s371,plain,
( ~ spl0_7
| ~ spl0_83
| spl0_215 ),
inference(sat_conversion,[],[f1733]) ).
cnf(s429,plain,
( ~ spl0_9
| ~ spl0_232
| spl0_309 ),
inference(sat_conversion,[],[f2089]) ).
cnf(s529,plain,
( ~ spl0_2
| ~ spl0_232
| spl0_333 ),
inference(sat_conversion,[],[f2201]) ).
cnf(s540,plain,
( ~ spl0_232
| ~ spl0_333
| spl0_334 ),
inference(sat_conversion,[],[f2389]) ).
cnf(s576,plain,
( ~ spl0_333
| spl0_348 ),
inference(sat_conversion,[],[f2445]) ).
cnf(s725,plain,
( ~ spl0_9
| ~ spl0_216
| spl0_437 ),
inference(sat_conversion,[],[f3037]) ).
cnf(s2432,plain,
( ~ spl0_23
| ~ spl0_309
| spl0_1369 ),
inference(sat_conversion,[],[f10120]) ).
cnf(s2544,plain,
( ~ spl0_7
| ~ spl0_1369
| spl0_1459 ),
inference(sat_conversion,[],[f10638]) ).
cnf(s2597,plain,
( ~ spl0_215
| ~ spl0_1459
| spl0_1505 ),
inference(sat_conversion,[],[f10959]) ).
cnf(s2932,plain,
( ~ spl0_216
| ~ spl0_1505
| spl0_1721 ),
inference(sat_conversion,[],[f12183]) ).
cnf(s2934,plain,
( ~ spl0_215
| ~ spl0_1505
| spl0_1723 ),
inference(sat_conversion,[],[f12191]) ).
cnf(s3188,plain,
( ~ spl0_216
| ~ spl0_1723
| spl0_1910 ),
inference(sat_conversion,[],[f13301]) ).
cnf(s3189,plain,
( ~ spl0_214
| ~ spl0_1723
| spl0_1911 ),
inference(sat_conversion,[],[f13305]) ).
cnf(s3190,plain,
( ~ spl0_215
| ~ spl0_1723
| spl0_1912 ),
inference(sat_conversion,[],[f13309]) ).
cnf(s3327,plain,
( spl0_1
| ~ spl0_1912
| spl0_2004 ),
inference(sat_conversion,[],[f14172]) ).
cnf(s3336,plain,
( ~ spl0_216
| ~ spl0_1912
| spl0_2011 ),
inference(sat_conversion,[],[f14202]) ).
cnf(s3601,plain,
( ~ spl0_1910
| ~ spl0_1912
| spl0_2065 ),
inference(sat_conversion,[],[f14926]) ).
cnf(s3729,plain,
( ~ spl0_1911
| ~ spl0_1912
| spl0_2118 ),
inference(sat_conversion,[],[f15415]) ).
cnf(s5812,plain,
( ~ spl0_1912
| ~ spl0_2011
| spl0_3364 ),
inference(sat_conversion,[],[f24426]) ).
cnf(s6005,plain,
( ~ spl0_2065
| ~ spl0_3364
| spl0_3522 ),
inference(sat_conversion,[],[f25394]) ).
cnf(s6047,plain,
( ~ spl0_2118
| ~ spl0_3364
| spl0_3527 ),
inference(sat_conversion,[],[f25519]) ).
cnf(s6465,plain,
( ~ spl0_2
| ~ spl0_3527
| spl0_3861 ),
inference(sat_conversion,[],[f27328]) ).
cnf(s6554,plain,
( ~ spl0_2004
| ~ spl0_3861
| spl0_3914 ),
inference(sat_conversion,[],[f28175]) ).
cnf(s6795,plain,
( ~ spl0_3861
| spl0_4026 ),
inference(sat_conversion,[],[f28896]) ).
cnf(s6820,plain,
( ~ spl0_3861
| spl0_4105 ),
inference(sat_conversion,[],[f28961]) ).
cnf(s6971,plain,
( ~ spl0_3364
| ~ spl0_4026
| spl0_4203 ),
inference(sat_conversion,[],[f30048]) ).
cnf(s16416,plain,
( ~ spl0_9
| ~ spl0_3522
| ~ spl0_4203
| spl0_10843 ),
inference(sat_conversion,[],[f72488]) ).
cnf(s16420,plain,
( ~ spl0_2
| ~ spl0_3522
| ~ spl0_4203
| spl0_10855 ),
inference(sat_conversion,[],[f72504]) ).
cnf(s16609,plain,
( ~ spl0_333
| ~ spl0_10843
| spl0_10986 ),
inference(sat_conversion,[],[f73489]) ).
cnf(s16624,plain,
( ~ spl0_4105
| ~ spl0_10843
| spl0_11012 ),
inference(sat_conversion,[],[f73539]) ).
cnf(s17082,plain,
( ~ spl0_348
| ~ spl0_10855
| spl0_11324 ),
inference(sat_conversion,[],[f75857]) ).
cnf(s17097,plain,
( ~ spl0_3861
| ~ spl0_10855
| spl0_11331 ),
inference(sat_conversion,[],[f75906]) ).
cnf(s17200,plain,
( ~ spl0_437
| ~ spl0_10855
| ~ spl0_10986
| spl0_11404 ),
inference(sat_conversion,[],[f76238]) ).
cnf(s17206,plain,
( ~ spl0_214
| ~ spl0_10855
| ~ spl0_10986
| ~ spl0_11012
| spl0_11409 ),
inference(sat_conversion,[],[f76259]) ).
cnf(s17439,plain,
( ~ spl0_3527
| ~ spl0_11404
| ~ spl0_11409
| spl0_11608 ),
inference(sat_conversion,[],[f77507]) ).
cnf(s17499,plain,
( ~ spl0_3914
| ~ spl0_11608
| spl0_11662 ),
inference(sat_conversion,[],[f78129]) ).
cnf(s17546,plain,
( ~ spl0_10843
| ~ spl0_11608
| spl0_11693 ),
inference(sat_conversion,[],[f78373]) ).
cnf(s17582,plain,
( ~ spl0_1721
| ~ spl0_11331
| ~ spl0_11608
| spl0_11698 ),
inference(sat_conversion,[],[f78440]) ).
cnf(s17640,plain,
( ~ spl0_216
| ~ spl0_10986
| ~ spl0_11608
| spl0_11720 ),
inference(sat_conversion,[],[f78593]) ).
cnf(s17689,plain,
( ~ spl0_11698
| ~ spl0_11720
| spl0_11746 ),
inference(sat_conversion,[],[f78770]) ).
cnf(s17889,plain,
( ~ spl0_334
| ~ spl0_11324
| ~ spl0_11693
| ~ spl0_11746
| spl0_11867 ),
inference(sat_conversion,[],[f83291]) ).
cnf(s17924,plain,
( ~ spl0_11662
| ~ spl0_11867 ),
inference(sat_conversion,[],[f84282]) ).
cnf(s17925,plain,
spl0_4,
inference(rat,[],[s4,s2]) ).
cnf(s17937,plain,
spl0_9,
inference(rat,[],[s9,s2,s17925]) ).
cnf(s17939,plain,
spl0_7,
inference(rat,[],[s7,s2,s17925]) ).
cnf(s17984,plain,
spl0_32,
inference(rat,[],[s34,s17937,s17939]) ).
cnf(s17989,plain,
spl0_23,
inference(rat,[],[s25,s17939]) ).
cnf(s17992,plain,
spl0_20,
inference(rat,[],[s22,s2,s17939]) ).
cnf(s18091,plain,
spl0_83,
inference(rat,[],[s131,s2,s17992]) ).
cnf(s18139,plain,
spl0_215,
inference(rat,[],[s371,s17939,s18091]) ).
cnf(s18177,plain,
spl0_232,
inference(rat,[],[s325,s18091]) ).
cnf(s18194,plain,
spl0_216,
inference(rat,[],[s298,s17992,s18091]) ).
cnf(s18195,plain,
spl0_214,
inference(rat,[],[s296,s17984,s18091]) ).
cnf(s18299,plain,
spl0_333,
inference(rat,[],[s529,s2,s18177]) ).
cnf(s18323,plain,
spl0_309,
inference(rat,[],[s429,s17937,s18177]) ).
cnf(s18390,plain,
spl0_437,
inference(rat,[],[s725,s17937,s18194]) ).
cnf(s18448,plain,
spl0_348,
inference(rat,[],[s576,s18299]) ).
cnf(s18462,plain,
spl0_334,
inference(rat,[],[s540,s18177,s18299]) ).
cnf(s18606,plain,
spl0_1369,
inference(rat,[],[s2432,s17989,s18323]) ).
cnf(s19195,plain,
spl0_1459,
inference(rat,[],[s2544,s17939,s18606]) ).
cnf(s19400,plain,
spl0_1505,
inference(rat,[],[s2597,s18139,s19195]) ).
cnf(s19587,plain,
spl0_1723,
inference(rat,[],[s2934,s18139,s19400]) ).
cnf(s19589,plain,
spl0_1721,
inference(rat,[],[s2932,s18194,s19400]) ).
cnf(s19779,plain,
spl0_1912,
inference(rat,[],[s3190,s18139,s19587]) ).
cnf(s19780,plain,
spl0_1911,
inference(rat,[],[s3189,s18195,s19587]) ).
cnf(s19781,plain,
spl0_1910,
inference(rat,[],[s3188,s18194,s19587]) ).
cnf(s20130,plain,
spl0_2011,
inference(rat,[],[s3336,s18194,s19779]) ).
cnf(s20275,plain,
spl0_2118,
inference(rat,[],[s3729,s19779,s19780]) ).
cnf(s20332,plain,
spl0_2065,
inference(rat,[],[s3601,s19779,s19781]) ).
cnf(s20544,plain,
spl0_3364,
inference(rat,[],[s5812,s19779,s20130]) ).
cnf(s21474,plain,
spl0_3527,
inference(rat,[],[s6047,s20275,s20544]) ).
cnf(s21503,plain,
spl0_3522,
inference(rat,[],[s6005,s20332,s20544]) ).
cnf(s21593,plain,
spl0_3861,
inference(rat,[],[s6465,s2,s21474]) ).
cnf(s22279,plain,
spl0_4105,
inference(rat,[],[s6820,s21593]) ).
cnf(s22296,plain,
spl0_4026,
inference(rat,[],[s6795,s21593]) ).
cnf(s23325,plain,
spl0_4203,
inference(rat,[],[s6971,s20544,s22296]) ).
cnf(s25712,plain,
spl0_10855,
inference(rat,[],[s16420,s21503,s2,s23325]) ).
cnf(s25717,plain,
spl0_10843,
inference(rat,[],[s16416,s21503,s17937,s23325]) ).
cnf(s27201,plain,
spl0_11331,
inference(rat,[],[s17097,s21593,s25712]) ).
cnf(s27209,plain,
spl0_11324,
inference(rat,[],[s17082,s18448,s25712]) ).
cnf(s27370,plain,
spl0_11012,
inference(rat,[],[s16624,s22279,s25717]) ).
cnf(s27376,plain,
spl0_10986,
inference(rat,[],[s16609,s18299,s25717]) ).
cnf(s27641,plain,
spl0_11409,
inference(rat,[],[s17206,s27370,s25712,s18195,s27376]) ).
cnf(s27647,plain,
spl0_11404,
inference(rat,[],[s17200,s25712,s18390,s27376]) ).
cnf(s27669,plain,
spl0_11608,
inference(rat,[],[s17439,s27641,s21474,s27647]) ).
cnf(s27848,plain,
spl0_11693,
inference(rat,[],[s17546,s25717,s27669]) ).
cnf(s27907,plain,
spl0_11720,
inference(rat,[],[s17640,s27376,s18194,s27669]) ).
cnf(s27921,plain,
spl0_11698,
inference(rat,[],[s17582,s27201,s19589,s27669]) ).
cnf(s28002,plain,
spl0_11746,
inference(rat,[],[s17689,s27907,s27921]) ).
cnf(s28038,plain,
spl0_11867,
inference(rat,[],[s17889,s27848,s27209,s18462,s28002]) ).
cnf(s28066,plain,
~ spl0_11662,
inference(rat,[],[s17924,s28038]) ).
cnf(s28074,plain,
~ spl0_3914,
inference(rat,[],[s17499,s27669,s28066]) ).
cnf(s28081,plain,
~ spl0_2004,
inference(rat,[],[s6554,s21593,s28074]) ).
cnf(s28084,plain,
spl0_1,
inference(rat,[],[s3327,s19779,s28081]) ).
cnf(s28085,plain,
$false,
inference(rat,[],[s1,s28084]) ).
fof(f84283,plain,
$false,
inference(avatar_sat_refutation,[],[s28085]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : GRP419-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.04/0.31 % Computer : n012.cluster.edu
% 0.04/0.31 % Model : x86_64 x86_64
% 0.04/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.31 % Memory : 8046.5625MB
% 0.04/0.31 % OS : Linux 6.8.0-71-generic
% 0.04/0.31 % CPULimit : 300
% 0.04/0.31 % WCLimit : 300
% 0.04/0.31 % DateTime : Sun Sep 27 10:03:35 UTC 2026
% 0.04/0.31 % CPUTime :
% 0.04/0.31 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.08/0.33 Running first-order model finding
% 0.08/0.33 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 22.19/3.54 % (2135542)Will run a generic schedule for satisfiability detection.
% 22.19/3.54 % (2135548)% WARNING: option uhcvi not known.
% 22.19/3.54 % (2135548)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1385868420:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 22.19/3.54 % (2135547)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=534990731_2999 on theBenchmark for (2999ds/0Mi)
% 22.19/3.54 % (2135549)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3202738735:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 22.19/3.54 % (2135550)dis+10_1_sil=32000:sp=arity:random_seed=993215056:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 22.19/3.54 % (2135551)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=3165978750:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 22.19/3.54 % (2135552)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1508709989:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 22.19/3.54 % (2135553)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3455233379:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 22.19/3.54 % TRYING [1]
% 22.19/3.54 % TRYING [2]
% 22.19/3.54 % TRYING [3]
% 22.19/3.54 % TRYING [4]
% 22.19/3.54 % (2135550)Instruction limit reached!
% 22.19/3.54 % (2135550)------------------------------
% 22.19/3.54 % (2135550)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.19/3.54 % (2135550)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.19/3.54 % (2135550)CaDiCaL version: 2.1.3
% 22.19/3.54 % (2135550)Termination reason: Instruction limit
% 22.19/3.54 % (2135550)Termination phase: Saturation
% 22.19/3.54 % (2135550)Time elapsed: 0.028 s
% 22.19/3.54 % (2135550)Peak memory usage: 11 MB
% 22.19/3.54 % (2135550)Instructions burned: 106 (million)
% 22.19/3.54 % (2135551)Instruction limit reached!
% 22.19/3.54 % (2135551)------------------------------
% 22.19/3.54 % (2135551)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.19/3.54 % (2135551)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.19/3.54 % (2135551)CaDiCaL version: 2.1.3
% 22.19/3.54 % (2135551)Termination reason: Instruction limit
% 22.19/3.54 % (2135551)Termination phase: Saturation
% 22.19/3.54 % (2135551)Time elapsed: 0.034 s
% 22.19/3.54 % (2135551)Peak memory usage: 12 MB
% 22.19/3.54 % (2135551)Instructions burned: 117 (million)
% 22.19/3.54 % (2135565)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=1836472151:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 22.19/3.54 % TRYING [1]
% 22.19/3.54 % TRYING [2]
% 22.19/3.54 % TRYING [3]
% 22.19/3.54 % (2135552)Instruction limit reached!
% 22.19/3.54 % (2135552)------------------------------
% 22.19/3.54 % (2135552)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.19/3.54 % (2135552)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.19/3.54 % (2135552)CaDiCaL version: 2.1.3
% 22.19/3.54 % (2135552)Termination reason: Instruction limit
% 22.19/3.54 % (2135552)Termination phase: Saturation
% 22.19/3.54 % (2135552)Time elapsed: 0.042 s
% 22.19/3.54 % (2135552)Peak memory usage: 12 MB
% 22.19/3.54 % (2135552)Instructions burned: 132 (million)
% 22.19/3.54 % (2135566)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1371785135:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 22.19/3.54 % TRYING [4]
% 22.19/3.54 % (2135570)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=1063042994:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2999 on theBenchmark for (2999ds/684Mi)
% 22.19/3.54 % (2135553)Instruction limit reached!
% 22.19/3.54 % (2135553)------------------------------
% 22.19/3.54 % (2135553)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.19/3.54 % (2135553)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.19/3.54 % (2135553)CaDiCaL version: 2.1.3
% 22.19/3.54 % (2135553)Termination reason: Instruction limit
% 22.19/3.54 % (2135553)Termination phase: Saturation
% 22.19/3.54 % (2135553)Time elapsed: 0.070 s
% 22.19/3.54 % (2135553)Peak memory usage: 13 MB
% 22.19/3.54 % (2135553)Instructions burned: 161 (million)
% 22.19/3.54 % (2135566)Instruction limit reached!
% 22.19/3.54 % (2135566)------------------------------
% 22.19/3.54 % (2135566)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 22.19/3.54 % (2135566)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.19/3.54 % (2135566)CaDiCaL version: 2.1.3
% 44.04/6.67 % (2135566)Termination reason: Instruction limit
% 44.04/6.67 % (2135566)Termination phase: Saturation
% 44.04/6.67 % (2135566)Time elapsed: 0.038 s
% 44.04/6.67 % (2135566)Peak memory usage: 12 MB
% 44.04/6.67 % (2135566)Instructions burned: 133 (million)
% 44.04/6.67 % (2135594)ott-21_1_sil=16000:fs=off:random_seed=4252900102:i=180:av=off:fsr=off_2999 on theBenchmark for (2999ds/180Mi)
% 44.04/6.67 % (2135595)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2948467877:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 44.04/6.67 % (2135594)Instruction limit reached!
% 44.04/6.67 % (2135594)------------------------------
% 44.04/6.67 % (2135594)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.04/6.67 % (2135594)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.04/6.67 % (2135594)CaDiCaL version: 2.1.3
% 44.04/6.67 % (2135594)Termination reason: Instruction limit
% 44.04/6.67 % (2135594)Termination phase: Saturation
% 44.04/6.67 % (2135594)Time elapsed: 0.071 s
% 44.04/6.67 % (2135594)Peak memory usage: 11 MB
% 44.04/6.67 % (2135594)Instructions burned: 181 (million)
% 44.04/6.67 % (2135605)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2680155132:fmbsr=1.3:i=865:ins=25_2998 on theBenchmark for (2998ds/865Mi)
% 44.04/6.67 % TRYING [1]
% 44.04/6.67 % TRYING [2]
% 44.04/6.67 % TRYING [3]
% 44.04/6.67 % TRYING [4]
% 44.04/6.67 % (2135595)Instruction limit reached!
% 44.04/6.67 % (2135595)------------------------------
% 44.04/6.67 % (2135595)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.04/6.67 % (2135595)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.04/6.67 % (2135595)CaDiCaL version: 2.1.3
% 44.04/6.67 % (2135595)Termination reason: Instruction limit
% 44.04/6.67 % (2135595)Termination phase: Saturation
% 44.04/6.67 % (2135595)Time elapsed: 0.188 s
% 44.04/6.67 % (2135595)Peak memory usage: 13 MB
% 44.04/6.67 % (2135595)Instructions burned: 477 (million)
% 44.04/6.67 % (2135612)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1468599240:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 44.04/6.67 % (2135565)Instruction limit reached!
% 44.04/6.67 % (2135565)------------------------------
% 44.04/6.67 % (2135565)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.04/6.67 % (2135565)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.04/6.67 % (2135565)CaDiCaL version: 2.1.3
% 44.04/6.67 % (2135565)Termination reason: Instruction limit
% 44.04/6.67 % (2135565)Termination phase: Finite model building SAT solving
% 44.04/6.67 % (2135565)Time elapsed: 0.275 s
% 44.04/6.67 % (2135565)Peak memory usage: 12 MB
% 44.04/6.67 % (2135565)Instructions burned: 716 (million)
% 44.04/6.67 % (2135614)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1866198705:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi)
% 44.04/6.67 % TRYING [14]
% 44.04/6.67 % (2135570)Instruction limit reached!
% 44.04/6.67 % (2135570)------------------------------
% 44.04/6.67 % (2135570)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.04/6.67 % (2135570)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.04/6.67 % (2135570)CaDiCaL version: 2.1.3
% 44.04/6.67 % (2135570)Termination reason: Instruction limit
% 44.04/6.67 % (2135570)Termination phase: Saturation
% 44.04/6.67 % (2135570)Time elapsed: 0.303 s
% 44.04/6.67 % (2135570)Peak memory usage: 16 MB
% 44.04/6.67 % (2135570)Instructions burned: 684 (million)
% 44.04/6.67 % (2135616)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=1814889535:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2996 on theBenchmark for (2996ds/692Mi)
% 44.04/6.67 % (2135605)Instruction limit reached!
% 44.04/6.67 % (2135605)------------------------------
% 44.04/6.67 % (2135605)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 44.04/6.67 % (2135605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 44.04/6.67 % (2135605)CaDiCaL version: 2.1.3
% 44.04/6.67 % (2135605)Termination reason: Instruction limit
% 44.04/6.67 % (2135605)Termination phase: Finite model building SAT solving
% 44.04/6.67 % (2135605)Time elapsed: 0.417 s
% 44.04/6.67 % (2135605)Peak memory usage: 12 MB
% 44.04/6.67 % (2135605)Instructions burned: 867 (million)
% 44.04/6.67 % (2135624)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=2467147216:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 44.04/6.67 % TRYING [5]
% 44.04/6.67 % (2135614)Instruction limit reached!
% 44.04/6.67 % (2135614)------------------------------
% 88.49/13.00 % (2135614)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 88.49/13.00 % (2135614)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.49/13.00 % (2135614)CaDiCaL version: 2.1.3
% 88.49/13.00 % (2135614)Termination reason: Instruction limit
% 88.49/13.00 % (2135614)Termination phase: Finite model building constraint generation
% 88.49/13.00 % (2135614)Time elapsed: 0.344 s
% 88.49/13.00 % (2135614)Peak memory usage: 80 MB
% 88.49/13.00 % (2135614)Instructions burned: 889 (million)
% 88.49/13.00 % (2135627)fmb+10_1_sil=64000:random_seed=1962595590:i=22061:nm=2:gsp=on_2993 on theBenchmark for (2993ds/22061Mi)
% 88.49/13.00 % TRYING [1]
% 88.49/13.00 % TRYING [2]
% 88.49/13.00 % TRYING [3]
% 88.49/13.00 % TRYING [4]
% 88.49/13.00 % (2135616)Instruction limit reached!
% 88.49/13.00 % (2135616)------------------------------
% 88.49/13.00 % (2135616)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 88.49/13.00 % (2135616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.49/13.00 % (2135616)CaDiCaL version: 2.1.3
% 88.49/13.00 % (2135616)Termination reason: Instruction limit
% 88.49/13.00 % (2135616)Termination phase: Saturation
% 88.49/13.00 % (2135616)Time elapsed: 0.340 s
% 88.49/13.00 % (2135616)Peak memory usage: 17 MB
% 88.49/13.00 % (2135616)Instructions burned: 692 (million)
% 88.49/13.00 % (2135630)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1208901898:i=9515:nm=5_2992 on theBenchmark for (2992ds/9515Mi)
% 88.49/13.00 % TRYING [20]
% 88.49/13.00 % (2135612)Instruction limit reached!
% 88.49/13.00 % (2135612)------------------------------
% 88.49/13.00 % (2135612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 88.49/13.00 % (2135612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.49/13.00 % (2135612)CaDiCaL version: 2.1.3
% 88.49/13.00 % (2135612)Termination reason: Instruction limit
% 88.49/13.00 % (2135612)Termination phase: Saturation
% 88.49/13.00 % (2135612)Time elapsed: 0.516 s
% 88.49/13.00 % (2135612)Peak memory usage: 20 MB
% 88.49/13.00 % (2135612)Instructions burned: 1180 (million)
% 88.49/13.00 % (2135635)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=1809422782:fmbsr=1.7:i=920_2991 on theBenchmark for (2991ds/920Mi)
% 88.49/13.00 % TRYING [8]
% 88.49/13.00 % (2135624)Instruction limit reached!
% 88.49/13.00 % (2135624)------------------------------
% 88.49/13.00 % (2135624)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 88.49/13.00 % (2135624)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.49/13.00 % (2135624)CaDiCaL version: 2.1.3
% 88.49/13.00 % (2135624)Termination reason: Instruction limit
% 88.49/13.00 % (2135624)Termination phase: Saturation
% 88.49/13.00 % (2135624)Time elapsed: 0.280 s
% 88.49/13.00 % (2135624)Peak memory usage: 15 MB
% 88.49/13.00 % (2135624)Instructions burned: 881 (million)
% 88.49/13.00 % (2135638)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2055364000:i=5131_2990 on theBenchmark for (2990ds/5131Mi)
% 88.49/13.00 % (2135635)Instruction limit reached!
% 88.49/13.00 % (2135635)------------------------------
% 88.49/13.00 % (2135635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 88.49/13.00 % (2135635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.49/13.00 % (2135635)CaDiCaL version: 2.1.3
% 88.49/13.00 % (2135635)Termination reason: Instruction limit
% 88.49/13.00 % (2135635)Termination phase: Finite model building SAT solving
% 88.49/13.00 % (2135635)Time elapsed: 0.373 s
% 88.49/13.00 % (2135635)Peak memory usage: 37 MB
% 88.49/13.00 % (2135635)Instructions burned: 921 (million)
% 88.49/13.00 % (2135644)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1723234196:i=1472:ins=7:fdi=8:gsp=on_2987 on theBenchmark for (2987ds/1472Mi)
% 88.49/13.00 % (2135644)Instruction limit reached!
% 88.49/13.00 % (2135644)------------------------------
% 88.49/13.00 % (2135644)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 88.49/13.00 % (2135644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.49/13.00 % (2135644)CaDiCaL version: 2.1.3
% 88.49/13.00 % (2135644)Termination reason: Instruction limit
% 88.49/13.00 % (2135644)Termination phase: Saturation
% 88.49/13.00 % (2135644)Time elapsed: 0.677 s
% 88.49/13.00 % (2135644)Peak memory usage: 24 MB
% 88.49/13.00 % (2135644)Instructions burned: 1473 (million)
% 88.49/13.00 % (2135648)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1442064013:i=6324_2980 on theBenchmark for (2980ds/6324Mi)
% 88.49/13.00 % TRYING [77]
% 88.49/13.00 % TRYING [5]
% 88.49/13.00 % (2135638)Instruction limit reached!
% 88.49/13.00 % (2135638)------------------------------
% 176.23/25.43 % (2135638)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 176.23/25.43 % (2135638)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.23/25.43 % (2135638)CaDiCaL version: 2.1.3
% 176.23/25.43 % (2135638)Termination reason: Instruction limit
% 176.23/25.43 % (2135638)Termination phase: Saturation
% 176.23/25.43 % (2135638)Time elapsed: 2.282 s
% 176.23/25.43 % (2135638)Peak memory usage: 34 MB
% 176.23/25.43 % (2135638)Instructions burned: 5132 (million)
% 176.23/25.43 % (2135652)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2044754180:fmbsr=2.30978:i=2174_2967 on theBenchmark for (2967ds/2174Mi)
% 176.23/25.43 % TRYING [16]
% 176.23/25.43 % (2135648)Instruction limit reached!
% 176.23/25.43 % (2135648)------------------------------
% 176.23/25.43 % (2135648)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 176.23/25.43 % (2135648)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.23/25.43 % (2135648)CaDiCaL version: 2.1.3
% 176.23/25.43 % (2135648)Termination reason: Instruction limit
% 176.23/25.43 % (2135648)Termination phase: Finite model building constraint generation
% 176.23/25.43 % (2135648)Time elapsed: 1.968 s
% 176.23/25.43 % (2135648)Peak memory usage: 522 MB
% 176.23/25.43 % (2135648)Instructions burned: 6326 (million)
% 176.23/25.43 % (2135658)ott-2_1_sil=16000:newcnf=on:random_seed=888975072:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2960 on theBenchmark for (2960ds/869Mi)
% 176.23/25.43 % (2135652)Instruction limit reached!
% 176.23/25.43 % (2135652)------------------------------
% 176.23/25.43 % (2135652)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 176.23/25.43 % (2135652)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.23/25.43 % (2135652)CaDiCaL version: 2.1.3
% 176.23/25.43 % (2135652)Termination reason: Instruction limit
% 176.23/25.43 % (2135652)Termination phase: Finite model building constraint generation
% 176.23/25.43 % (2135652)Time elapsed: 0.817 s
% 176.23/25.43 % (2135652)Peak memory usage: 153 MB
% 176.23/25.43 % (2135652)Instructions burned: 2175 (million)
% 176.23/25.43 % (2135660)ott+10_1_sil=32000:tgt=ground:random_seed=752295713:i=5114:av=off_2959 on theBenchmark for (2959ds/5114Mi)
% 176.23/25.43 % (2135658)Instruction limit reached!
% 176.23/25.43 % (2135658)------------------------------
% 176.23/25.43 % (2135658)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 176.23/25.43 % (2135658)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.23/25.43 % (2135658)CaDiCaL version: 2.1.3
% 176.23/25.43 % (2135658)Termination reason: Instruction limit
% 176.23/25.43 % (2135658)Termination phase: Saturation
% 176.23/25.43 % (2135658)Time elapsed: 0.312 s
% 176.23/25.43 % (2135658)Peak memory usage: 21 MB
% 176.23/25.43 % (2135658)Instructions burned: 870 (million)
% 176.23/25.43 % (2135664)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=2364994126:i=54282_2956 on theBenchmark for (2956ds/54282Mi)
% 176.23/25.43 % TRYING [1]
% 176.23/25.43 % TRYING [2]
% 176.23/25.43 % TRYING [3]
% 176.23/25.43 % TRYING [4]
% 176.23/25.43 % (2135630)Instruction limit reached!
% 176.23/25.43 % (2135630)------------------------------
% 176.23/25.43 % (2135630)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 176.23/25.43 % (2135630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.23/25.43 % (2135630)CaDiCaL version: 2.1.3
% 176.23/25.43 % (2135630)Termination reason: Instruction limit
% 176.23/25.43 % (2135630)Termination phase: Finite model building constraint generation
% 176.23/25.43 % (2135630)Time elapsed: 4.004 s
% 176.23/25.43 % (2135630)Peak memory usage: 658 MB
% 176.23/25.43 % (2135630)Instructions burned: 9516 (million)
% 176.23/25.43 % (2135670)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=1731444867:i=3512:aac=none_2951 on theBenchmark for (2951ds/3512Mi)
% 176.23/25.43 % TRYING [5]
% 176.23/25.43 % (2135670)Instruction limit reached!
% 176.23/25.43 % (2135670)------------------------------
% 176.23/25.43 % (2135670)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 176.23/25.43 % (2135670)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 176.23/25.43 % (2135670)CaDiCaL version: 2.1.3
% 176.23/25.43 % (2135670)Termination reason: Instruction limit
% 176.23/25.43 % (2135670)Termination phase: Saturation
% 176.23/25.43 % (2135670)Time elapsed: 1.369 s
% 176.23/25.43 % (2135670)Peak memory usage: 31 MB
% 176.23/25.43 % (2135670)Instructions burned: 3513 (million)
% 176.23/25.43 % (2135672)dis+21_1_sil=32000:sas=cadical:random_seed=3025757550:i=3773:amm=off_2937 on theBenchmark for (2937ds/3773Mi)
% 176.23/25.43 % (2135660)Instruction limit reached!
% 176.23/25.43 % (2135660)------------------------------
% 218.24/31.37 % (2135660)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 218.24/31.37 % (2135660)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.24/31.37 % (2135660)CaDiCaL version: 2.1.3
% 218.24/31.37 % (2135660)Termination reason: Instruction limit
% 218.24/31.37 % (2135660)Termination phase: Saturation
% 218.24/31.37 % (2135660)Time elapsed: 2.257 s
% 218.24/31.37 % (2135660)Peak memory usage: 46 MB
% 218.24/31.37 % (2135660)Instructions burned: 5115 (million)
% 218.24/31.37 % (2135675)ott+11_1_sil=16000:gs=on:random_seed=2405658577:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2936 on theBenchmark for (2936ds/2251Mi)
% 218.24/31.37 % (2135675)Instruction limit reached!
% 218.24/31.37 % (2135675)------------------------------
% 218.24/31.37 % (2135675)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 218.24/31.37 % (2135675)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.24/31.37 % (2135675)CaDiCaL version: 2.1.3
% 218.24/31.37 % (2135675)Termination reason: Instruction limit
% 218.24/31.37 % (2135675)Termination phase: Saturation
% 218.24/31.37 % (2135675)Time elapsed: 0.926 s
% 218.24/31.37 % (2135675)Peak memory usage: 32 MB
% 218.24/31.37 % (2135675)Instructions burned: 2252 (million)
% 218.24/31.37 % (2135680)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=1488711201:fmbsr=1.6:i=67534_2927 on theBenchmark for (2927ds/67534Mi)
% 218.24/31.37 % TRYING [7]
% 218.24/31.37 % (2135672)Instruction limit reached!
% 218.24/31.37 % (2135672)------------------------------
% 218.24/31.37 % (2135672)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 218.24/31.37 % (2135672)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.24/31.37 % (2135672)CaDiCaL version: 2.1.3
% 218.24/31.37 % (2135672)Termination reason: Instruction limit
% 218.24/31.37 % (2135672)Termination phase: Saturation
% 218.24/31.37 % (2135672)Time elapsed: 1.654 s
% 218.24/31.37 % (2135672)Peak memory usage: 31 MB
% 218.24/31.37 % (2135672)Instructions burned: 3773 (million)
% 218.24/31.37 % (2135686)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3118943169:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2920 on theBenchmark for (2920ds/4591Mi)
% 218.24/31.37 % (2135686)Instruction limit reached!
% 218.24/31.37 % (2135686)------------------------------
% 218.24/31.37 % (2135686)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 218.24/31.37 % (2135686)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.24/31.37 % (2135686)CaDiCaL version: 2.1.3
% 218.24/31.37 % (2135686)Termination reason: Instruction limit
% 218.24/31.37 % (2135686)Termination phase: Saturation
% 218.24/31.37 % (2135686)Time elapsed: 1.747 s
% 218.24/31.37 % (2135686)Peak memory usage: 24 MB
% 218.24/31.37 % (2135686)Instructions burned: 4591 (million)
% 218.24/31.37 % (2135692)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=4293516796:i=29340_2902 on theBenchmark for (2902ds/29340Mi)
% 218.24/31.37 % (2135627)Instruction limit reached!
% 218.24/31.37 % (2135627)------------------------------
% 218.24/31.37 % (2135627)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 218.24/31.37 % (2135627)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.24/31.37 % (2135627)CaDiCaL version: 2.1.3
% 218.24/31.37 % (2135627)Termination reason: Instruction limit
% 218.24/31.37 % (2135627)Termination phase: Finite model building SAT solving
% 218.24/31.37 % (2135627)Time elapsed: 9.358 s
% 218.24/31.37 % (2135627)Peak memory usage: 17 MB
% 218.24/31.37 % (2135627)Instructions burned: 22061 (million)
% 218.24/31.37 % (2135796)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=791084605:i=5211_2899 on theBenchmark for (2899ds/5211Mi)
% 218.24/31.37 % (2135796)Instruction limit reached!
% 218.24/31.37 % (2135796)------------------------------
% 218.24/31.37 % (2135796)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 218.24/31.37 % (2135796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 218.24/31.37 % (2135796)CaDiCaL version: 2.1.3
% 218.24/31.37 % (2135796)Termination reason: Instruction limit
% 218.24/31.37 % (2135796)Termination phase: Saturation
% 218.24/31.37 % (2135796)Time elapsed: 1.319 s
% 218.24/31.37 % (2135796)Peak memory usage: 33 MB
% 218.24/31.37 % (2135796)Instructions burned: 5212 (million)
% 218.24/31.37 % (2135845)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=3322025110:i=5497:nm=2_2885 on theBenchmark for (2885ds/5497Mi)
% 218.24/31.37 % TRYING [17]
% 218.24/31.37 % (2135845)Instruction limit reached!
% 218.24/31.37 % (2135845)------------------------------
% 150.90/32.81 % (2135845)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 150.90/32.81 % (2135845)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.90/32.81 % (2135845)CaDiCaL version: 2.1.3
% 150.90/32.81 % (2135845)Termination reason: Instruction limit
% 150.90/32.81 % (2135845)Termination phase: Finite model building constraint generation
% 150.90/32.81 % (2135845)Time elapsed: 1.254 s
% 150.90/32.81 % (2135845)Peak memory usage: 384 MB
% 150.90/32.81 % (2135845)Instructions burned: 5500 (million)
% 150.90/32.81 % (2135847)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=1399636972:fmbsr=2:i=46332_2873 on theBenchmark for (2873ds/46332Mi)
% 150.90/32.81 % TRYING [15]
% 150.90/32.81 % (2135692)Instruction limit reached!
% 150.90/32.81 % (2135692)------------------------------
% 150.90/32.81 % (2135692)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 150.90/32.81 % (2135692)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.90/32.81 % (2135692)CaDiCaL version: 2.1.3
% 150.90/32.81 % (2135692)Termination reason: Instruction limit
% 150.90/32.81 % (2135692)Termination phase: Saturation
% 150.90/32.81 % (2135692)Time elapsed: 8.123 s
% 150.90/32.81 % (2135692)Peak memory usage: 120 MB
% 150.90/32.81 % (2135692)Instructions burned: 29344 (million)
% 150.90/32.81 % (2136280)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2429071797:i=14071_2821 on theBenchmark for (2821ds/14071Mi)
% 150.90/32.81 % TRYING [12]
% 150.90/32.81 % (2135549)Instruction limit reached!
% 150.90/32.81 % (2135549)------------------------------
% 150.90/32.81 % (2135549)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 150.90/32.81 % (2135549)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.90/32.81 % (2135549)CaDiCaL version: 2.1.3
% 150.90/32.81 % (2135549)Termination reason: Instruction limit
% 150.90/32.81 % (2135549)Termination phase: Saturation
% 150.90/32.81 % (2135549)Time elapsed: 19.273 s
% 150.90/32.81 % (2135549)Peak memory usage: 126 MB
% 150.90/32.81 % (2135549)Instructions burned: 88029 (million)
% 150.90/32.81 % (2136282)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1947026491:i=22565:add=on:rawr=on_2806 on theBenchmark for (2806ds/22565Mi)
% 150.90/32.81 % (2136280)Instruction limit reached!
% 150.90/32.81 % (2136280)------------------------------
% 150.90/32.81 % (2136280)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 150.90/32.81 % (2136280)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.90/32.81 % (2136280)CaDiCaL version: 2.1.3
% 150.90/32.81 % (2136280)Termination reason: Instruction limit
% 150.90/32.81 % (2136280)Termination phase: Finite model building SAT solving
% 150.90/32.81 % (2136280)Time elapsed: 5.114 s
% 150.90/32.81 % (2136280)Peak memory usage: 176 MB
% 150.90/32.81 % (2136280)Instructions burned: 14072 (million)
% 150.90/32.81 % (2136284)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1044489051:i=8173:av=off_2769 on theBenchmark for (2769ds/8173Mi)
% 150.90/32.81 % (2136282)Instruction limit reached!
% 150.90/32.81 % (2136282)------------------------------
% 150.90/32.81 % (2136282)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 150.90/32.81 % (2136282)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.90/32.81 % (2136282)CaDiCaL version: 2.1.3
% 150.90/32.81 % (2136282)Termination reason: Instruction limit
% 150.90/32.81 % (2136282)Termination phase: Saturation
% 150.90/32.81 % (2136282)Time elapsed: 4.326 s
% 150.90/32.81 % (2136282)Peak memory usage: 65 MB
% 150.90/32.81 % (2136282)Instructions burned: 22566 (million)
% 150.90/32.81 % (2136286)dis+10_16:1_sil=16000:random_seed=974194552:i=9155:fsr=off_2763 on theBenchmark for (2763ds/9155Mi)
% 150.90/32.81 % (2135664)Instruction limit reached!
% 150.90/32.81 % (2135664)------------------------------
% 150.90/32.81 % (2135664)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 150.90/32.81 % (2135664)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.90/32.81 % (2135664)CaDiCaL version: 2.1.3
% 150.90/32.81 % (2135664)Termination reason: Instruction limit
% 150.90/32.81 % (2135664)Termination phase: Finite model building SAT solving
% 150.90/32.81 % (2135664)Time elapsed: 20.345 s
% 150.90/32.81 % (2135664)Peak memory usage: 23 MB
% 150.90/32.81 % (2135664)Instructions burned: 54284 (million)
% 150.90/32.81 % (2136288)ott-3_8_sil=64000:random_seed=845038368:i=20139:bs=on_2753 on theBenchmark for (2753ds/20139Mi)
% 150.90/32.81 % (2136284)Instruction limit reached!
% 150.90/32.81 % (2136284)------------------------------
% 150.90/32.81 % (2136284)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 150.90/32.81 % (2136284)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.90/32.81 % (2136284)CaDiCaL version: 2.1.3
% 150.90/32.81 % (2136284)Termination reason: Instruction limit
% 150.90/32.81 % (2136284)Termination phase: Saturation
% 150.90/32.81 % (2136284)Time elapsed: 2.081 s
% 150.90/32.81 % (2136284)Peak memory usage: 98 MB
% 150.90/32.81 % (2136284)Instructions burned: 8176 (million)
% 150.90/32.81 % (2136290)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=1989389645:fmbsr=2:i=32576_2748 on theBenchmark for (2748ds/32576Mi)
% 150.90/32.81 % TRYING [9]
% 150.90/32.81 % (2135680)Instruction limit reached!
% 150.90/32.81 % (2135680)------------------------------
% 150.90/32.81 % (2135680)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 150.90/32.81 % (2135680)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.90/32.81 % (2135680)CaDiCaL version: 2.1.3
% 150.90/32.81 % (2135680)Termination reason: Instruction limit
% 150.90/32.81 % (2135680)Termination phase: Finite model building SAT solving
% 150.90/32.81 % (2135680)Time elapsed: 18.500 s
% 150.90/32.82 % (2135680)Peak memory usage: 45 MB
% 150.90/32.82 % (2135680)Instructions burned: 67538 (million)
% 150.90/32.82 % (2136292)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=2563006410:i=11404_2741 on theBenchmark for (2741ds/11404Mi)
% 150.90/32.82 % (2136286)Instruction limit reached!
% 150.90/32.82 % (2136286)------------------------------
% 150.90/32.82 % (2136286)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 150.90/32.82 % (2136286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.90/32.82 % (2136286)CaDiCaL version: 2.1.3
% 150.90/32.82 % (2136286)Termination reason: Instruction limit
% 150.90/32.82 % (2136286)Termination phase: Saturation
% 150.90/32.82 % (2136286)Time elapsed: 2.355 s
% 150.90/32.82 % (2136286)Peak memory usage: 42 MB
% 150.90/32.82 % (2136286)Instructions burned: 9156 (million)
% 150.90/32.82 % (2136294)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=1099140225:i=14134_2739 on theBenchmark for (2739ds/14134Mi)
% 150.90/32.82 % (2136292)Instruction limit reached!
% 150.90/32.82 % (2136292)------------------------------
% 150.90/32.82 % (2136292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 150.90/32.82 % (2136292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.90/32.82 % (2136292)CaDiCaL version: 2.1.3
% 150.90/32.82 % (2136292)Termination reason: Instruction limit
% 150.90/32.82 % (2136292)Termination phase: Saturation
% 150.90/32.82 % (2136292)Time elapsed: 2.836 s
% 150.90/32.82 % (2136292)Peak memory usage: 138 MB
% 150.90/32.82 % (2136292)Instructions burned: 11407 (million)
% 150.90/32.82 % (2136298)dis+33_16_sil=32000:sac=on:random_seed=2269057555:i=15851:nm=0_2713 on theBenchmark for (2713ds/15851Mi)
% 150.90/32.82 % (2136294)Instruction limit reached!
% 150.90/32.82 % (2136294)------------------------------
% 150.90/32.82 % (2136294)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 150.90/32.82 % (2136294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.90/32.82 % (2136294)CaDiCaL version: 2.1.3
% 150.90/32.82 % (2136294)Termination reason: Instruction limit
% 150.90/32.82 % (2136294)Termination phase: Saturation
% 150.90/32.82 % (2136294)Time elapsed: 4.049 s
% 150.90/32.82 % (2136294)Peak memory usage: 180 MB
% 150.90/32.82 % (2136294)Instructions burned: 14137 (million)
% 150.90/32.82 % (2136558)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=3075460081:avsq=on:i=17627:add=on:amm=off_2699 on theBenchmark for (2699ds/17627Mi)
% 150.90/32.82 % (2136288)Instruction limit reached!
% 150.90/32.82 % (2136288)------------------------------
% 150.90/32.82 % (2136288)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 150.90/32.82 % (2136288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.90/32.82 % (2136288)CaDiCaL version: 2.1.3
% 150.90/32.82 % (2136288)Termination reason: Instruction limit
% 150.90/32.82 % (2136288)Termination phase: Saturation
% 150.90/32.82 % (2136288)Time elapsed: 6.302 s
% 150.90/32.82 % (2136288)Peak memory usage: 139 MB
% 150.90/32.82 % (2136288)Instructions burned: 20140 (million)
% 150.90/32.82 % (2136722)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=4259724192:s2a=on:i=53295_2690 on theBenchmark for (2690ds/53295Mi)
% 150.90/32.82 % (2135847)Instruction limit reached!
% 150.90/32.82 % (2135847)------------------------------
% 150.90/32.82 % (2135847)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 150.90/32.82 % (2135847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.90/32.82 % (2135847)CaDiCaL version: 2.1.3
% 150.90/32.82 % (2135847)Termination reason: Instruction limit
% 150.90/32.82 % (2135847)Termination phase: Finite model building SAT solving
% 150.90/32.82 % (2135847)Time elapsed: 18.324 s
% 150.90/32.82 % (2135847)Peak memory usage: 465 MB
% 150.90/32.82 % (2135847)Instructions burned: 46332 (million)
% 150.90/32.82 % (2136724)fmb+10_1_sil=32000:sas=cadical:fmbss=16:random_seed=2809048109:i=26857:ins=20_2689 on theBenchmark for (2689ds/26857Mi)
% 150.90/32.82 % TRYING [16]
% 150.90/32.82 % (2136722) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2135542-2136722"...
% 150.90/32.82 % (2136722)...printing done.
% 150.90/32.82 % (2136722)Refutation found. Thanks to Tanya!
% 150.90/32.82 % SZS status Unsatisfiable for theBenchmark
% 150.90/32.82 % SZS output start Proof for theBenchmark
% See solution above
% 150.90/32.82 % (2136722)------------------------------
% 150.90/32.82 % (2136722)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 150.90/32.82 % (2136722)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 150.90/32.82 % (2136722)CaDiCaL version: 2.1.3
% 150.90/32.82 % (2136722)Termination reason: Refutation
% 150.90/32.82 % (2136722)Time elapsed: 1.436 s
% 150.90/32.82 % (2136722)Peak memory usage: 76 MB
% 150.90/32.82 % (2136722)Instructions burned: 4984 (million)
% 150.90/32.82 % (2135542)Success in time 32.481 s
% 150.90/32.82 % Vampire exiting
%------------------------------------------------------------------------------