%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GRP422-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 : n019.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:17:47 AM UTC 2026
% Result : Unsatisfiable 233.60s 42.71s
% Output : Refutation 233.60s
% Verified :
% SZS Type : Refutation
% Derivation depth : 24
% Number of leaves : 27
% Syntax : Number of formulae : 161 ( 33 unt; 25 def)
% Number of atoms : 369 ( 82 equ)
% Maximal formula atoms : 4 ( 2 avg)
% Number of connectives : 410 ( 202 ~; 183 |; 0 &)
% ( 25 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 18 ( 3 avg)
% Number of predicates : 27 ( 25 usr; 26 prp; 0-2 aty)
% Number of functors : 4 ( 4 usr; 2 con; 0-2 aty)
% Number of variables : 237 ( 0 sgn 237 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X2,X0,X1] : inverse(multiply(inverse(multiply(X0,inverse(multiply(inverse(X1),multiply(inverse(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),multiply(inverse(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),multiply(inverse(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(f15,plain,
( ! [X2,X0,X1] : multiply(inverse(X2),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))) = inverse(multiply(inverse(multiply(X1,X0)),multiply(X1,X2)))
| ~ spl0_2 ),
inference(superposition,[],[f11,f11]) ).
fof(f17,definition,
( spl0_3
<=> ! [X2,X0,X1] : multiply(inverse(X2),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))) = inverse(multiply(inverse(multiply(X1,X0)),multiply(X1,X2))) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f18,plain,
( ! [X2,X0,X1] : multiply(inverse(X2),inverse(multiply(inverse(X0),multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(inverse(multiply(inverse(X2),X2))),inverse(multiply(inverse(X2),X2)))))))) = inverse(multiply(inverse(multiply(X1,X0)),multiply(X1,X2)))
| ~ spl0_3 ),
inference(avatar_component_clause,[],[f17]) ).
fof(f19,plain,
( spl0_3
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f15,f10,f17]) ).
fof(f34,plain,
( ! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))) = inverse(multiply(inverse(multiply(X3,X1)),multiply(X3,X2)))
| ~ spl0_3 ),
inference(superposition,[],[f18,f18]) ).
fof(f39,plain,
( ! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))) = X1
| ~ spl0_2
| ~ spl0_3 ),
inference(superposition,[],[f11,f18]) ).
fof(f66,definition,
( spl0_11
<=> ! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))) = X1 ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f67,plain,
( ! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2)))),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))) = X1
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f66]) ).
fof(f68,plain,
( spl0_11
| ~ spl0_2
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f39,f17,f10,f66]) ).
fof(f82,definition,
( spl0_15
<=> ! [X0,X3,X2,X1] : inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))) = inverse(multiply(inverse(multiply(X3,X1)),multiply(X3,X2))) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f83,plain,
( ! [X2,X3,X0,X1] : inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X2))) = inverse(multiply(inverse(multiply(X3,X1)),multiply(X3,X2)))
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f82]) ).
fof(f84,plain,
( spl0_15
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f34,f17,f82]) ).
fof(f142,plain,
( ! [X2,X3,X0,X1] : multiply(inverse(X2),X1) = inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(multiply(inverse(X2),X2))))))),multiply(X3,X2)))
| ~ spl0_2
| ~ spl0_15 ),
inference(superposition,[],[f11,f83]) ).
fof(f145,plain,
( ! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X3),multiply(inverse(multiply(X4,X1)),inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X1)))))))),multiply(X2,multiply(X4,X1)))) = X3
| ~ spl0_2
| ~ spl0_15 ),
inference(superposition,[],[f11,f83]) ).
fof(f150,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))),multiply(inverse(X5),inverse(multiply(inverse(X5),X5))))))),multiply(X3,X5)))
| ~ spl0_2
| ~ spl0_15 ),
inference(superposition,[],[f11,f83]) ).
fof(f151,plain,
( ! [X2,X0,X1,X4] : multiply(inverse(multiply(X0,X1)),multiply(X0,X2)) = multiply(inverse(multiply(X4,X1)),multiply(X4,X2))
| ~ spl0_2
| ~ spl0_15 ),
inference(forward_demodulation,[],[f150,f11]) ).
fof(f169,definition,
( spl0_26
<=> ! [X4,X0,X3,X2,X1] : inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X3),multiply(inverse(multiply(X4,X1)),inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X1)))))))),multiply(X2,multiply(X4,X1)))) = X3 ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f170,plain,
( ! [X2,X3,X0,X1,X4] : inverse(multiply(inverse(multiply(X2,inverse(multiply(inverse(X3),multiply(inverse(multiply(X4,X1)),inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X1)))))))),multiply(X2,multiply(X4,X1)))) = X3
| ~ spl0_26 ),
inference(avatar_component_clause,[],[f169]) ).
fof(f171,plain,
( spl0_26
| ~ spl0_2
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f145,f82,f10,f169]) ).
fof(f181,definition,
( spl0_29
<=> ! [X0,X3,X2,X1] : multiply(inverse(X2),X1) = inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(multiply(inverse(X2),X2))))))),multiply(X3,X2))) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f182,plain,
( ! [X2,X3,X0,X1] : multiply(inverse(X2),X1) = inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,inverse(multiply(inverse(X2),X2))))))),multiply(X3,X2)))
| ~ spl0_29 ),
inference(avatar_component_clause,[],[f181]) ).
fof(f183,plain,
( spl0_29
| ~ spl0_2
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f142,f82,f10,f181]) ).
fof(f206,definition,
( spl0_35
<=> ! [X4,X0,X2,X1] : multiply(inverse(multiply(X0,X1)),multiply(X0,X2)) = multiply(inverse(multiply(X4,X1)),multiply(X4,X2)) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f207,plain,
( ! [X2,X0,X1,X4] : multiply(inverse(multiply(X0,X1)),multiply(X0,X2)) = multiply(inverse(multiply(X4,X1)),multiply(X4,X2))
| ~ spl0_35 ),
inference(avatar_component_clause,[],[f206]) ).
fof(f208,plain,
( spl0_35
| ~ spl0_2
| ~ spl0_15 ),
inference(avatar_split_clause,[],[f151,f82,f10,f206]) ).
fof(f224,plain,
( ! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X1,multiply(X2,X3))),multiply(X1,X4)) = multiply(X0,multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),multiply(inverse(X3),inverse(multiply(inverse(X3),X3))))))),X4))
| ~ spl0_2
| ~ spl0_35 ),
inference(superposition,[],[f207,f11]) ).
fof(f292,definition,
( spl0_43
<=> ! [X4,X0,X3,X2,X1] : multiply(inverse(multiply(X1,multiply(X2,X3))),multiply(X1,X4)) = multiply(X0,multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),multiply(inverse(X3),inverse(multiply(inverse(X3),X3))))))),X4)) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f293,plain,
( ! [X2,X3,X0,X1,X4] : multiply(inverse(multiply(X1,multiply(X2,X3))),multiply(X1,X4)) = multiply(X0,multiply(inverse(multiply(X2,inverse(multiply(inverse(X0),multiply(inverse(X3),inverse(multiply(inverse(X3),X3))))))),X4))
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f292]) ).
fof(f294,plain,
( spl0_43
| ~ spl0_2
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f224,f206,f10,f292]) ).
fof(f435,plain,
( ! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(X2,X1)),X3) = inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(X5,X3)),multiply(X5,inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X1)))))))),multiply(X4,multiply(X2,X1))))
| ~ spl0_29
| ~ spl0_35 ),
inference(superposition,[],[f182,f207]) ).
fof(f530,definition,
( spl0_79
<=> ! [X3,X4,X0,X5,X2,X1] : multiply(inverse(multiply(X2,X1)),X3) = inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(X5,X3)),multiply(X5,inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X1)))))))),multiply(X4,multiply(X2,X1)))) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f531,plain,
( ! [X2,X3,X0,X1,X4,X5] : multiply(inverse(multiply(X2,X1)),X3) = inverse(multiply(inverse(multiply(X4,inverse(multiply(inverse(multiply(X5,X3)),multiply(X5,inverse(multiply(inverse(multiply(X0,X1)),multiply(X0,X1)))))))),multiply(X4,multiply(X2,X1))))
| ~ spl0_79 ),
inference(avatar_component_clause,[],[f530]) ).
fof(f533,plain,
( spl0_79
| ~ spl0_29
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f435,f206,f181,f530]) ).
fof(f6317,plain,
( ! [X2,X3,X0,X1,X4,X5] : inverse(multiply(inverse(multiply(X5,inverse(multiply(inverse(multiply(X0,multiply(X1,X2))),multiply(X0,inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(inverse(X4)),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))))),multiply(X3,inverse(multiply(inverse(inverse(X4)),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))))))))))),multiply(X5,multiply(X1,inverse(multiply(inverse(inverse(X4)),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))))))) = X4
| ~ spl0_26
| ~ spl0_43 ),
inference(superposition,[],[f170,f293]) ).
fof(f6617,plain,
( ! [X2,X1,X4] : multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X4)),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))))),multiply(X1,X2)) = X4
| ~ spl0_26
| ~ spl0_43
| ~ spl0_79 ),
inference(forward_demodulation,[],[f6317,f531]) ).
fof(f7139,definition,
( spl0_973
<=> ! [X2,X1,X3] : multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X3)),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))))),multiply(X1,X2)) = X3 ),
introduced(definition,[new_symbols(definition,[spl0_973])],[avatar_definition]) ).
fof(f7140,plain,
( ! [X2,X3,X1] : multiply(inverse(multiply(X1,inverse(multiply(inverse(inverse(X3)),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))))),multiply(X1,X2)) = X3
| ~ spl0_973 ),
inference(avatar_component_clause,[],[f7139]) ).
fof(f7142,plain,
( spl0_973
| ~ spl0_26
| ~ spl0_43
| ~ spl0_79 ),
inference(avatar_split_clause,[],[f6617,f530,f292,f169,f7139]) ).
fof(f7256,plain,
( ! [X2,X3,X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(multiply(X1,multiply(X2,X3))),multiply(X1,multiply(X2,X3)))
| ~ spl0_43
| ~ spl0_973 ),
inference(superposition,[],[f293,f7140]) ).
fof(f7499,definition,
( spl0_1013
<=> ! [X0,X3,X2,X1] : multiply(inverse(X0),X0) = multiply(inverse(multiply(X1,multiply(X2,X3))),multiply(X1,multiply(X2,X3))) ),
introduced(definition,[new_symbols(definition,[spl0_1013])],[avatar_definition]) ).
fof(f7500,plain,
( ! [X2,X3,X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(multiply(X1,multiply(X2,X3))),multiply(X1,multiply(X2,X3)))
| ~ spl0_1013 ),
inference(avatar_component_clause,[],[f7499]) ).
fof(f7501,plain,
( spl0_1013
| ~ spl0_43
| ~ spl0_973 ),
inference(avatar_split_clause,[],[f7256,f7139,f292,f7499]) ).
fof(f7762,plain,
( ! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(X1),X1)
| ~ spl0_973
| ~ spl0_1013 ),
inference(superposition,[],[f7500,f7140]) ).
fof(f8736,definition,
( spl0_1216
<=> ! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(X1),X1) ),
introduced(definition,[new_symbols(definition,[spl0_1216])],[avatar_definition]) ).
fof(f8737,plain,
( ! [X0,X1] : multiply(inverse(X0),X0) = multiply(inverse(X1),X1)
| ~ spl0_1216 ),
inference(avatar_component_clause,[],[f8736]) ).
fof(f8739,plain,
( spl0_1216
| ~ spl0_973
| ~ spl0_1013 ),
inference(avatar_split_clause,[],[f7762,f7499,f7139,f8736]) ).
fof(f9060,plain,
( ! [X2,X0] : inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))) = X2
| ~ spl0_11
| ~ spl0_1216 ),
inference(superposition,[],[f67,f8737]) ).
fof(f9097,plain,
( ! [X0] : a2 != multiply(multiply(inverse(X0),X0),a2)
| spl0_1
| ~ spl0_1216 ),
inference(superposition,[],[f7,f8737]) ).
fof(f9108,plain,
( ! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X1),X2)))),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))) = X1
| ~ spl0_11
| ~ spl0_1216 ),
inference(superposition,[],[f67,f8737]) ).
fof(f9421,definition,
( spl0_1295
<=> ! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X1),X2)))),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))) = X1 ),
introduced(definition,[new_symbols(definition,[spl0_1295])],[avatar_definition]) ).
fof(f9422,plain,
( ! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(X1),X2)))),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))) = X1
| ~ spl0_1295 ),
inference(avatar_component_clause,[],[f9421]) ).
fof(f9423,plain,
( spl0_1295
| ~ spl0_11
| ~ spl0_1216 ),
inference(avatar_split_clause,[],[f9108,f8736,f66,f9421]) ).
fof(f9465,definition,
( spl0_1306
<=> ! [X0] : a2 != multiply(multiply(inverse(X0),X0),a2) ),
introduced(definition,[new_symbols(definition,[spl0_1306])],[avatar_definition]) ).
fof(f9466,plain,
( ! [X0] : a2 != multiply(multiply(inverse(X0),X0),a2)
| ~ spl0_1306 ),
inference(avatar_component_clause,[],[f9465]) ).
fof(f9467,plain,
( spl0_1306
| spl0_1
| ~ spl0_1216 ),
inference(avatar_split_clause,[],[f9097,f8736,f5,f9465]) ).
fof(f9514,definition,
( spl0_1318
<=> ! [X2,X0] : inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))) = X2 ),
introduced(definition,[new_symbols(definition,[spl0_1318])],[avatar_definition]) ).
fof(f9515,plain,
( ! [X2,X0] : inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),multiply(inverse(X2),inverse(multiply(inverse(X2),X2))))) = X2
| ~ spl0_1318 ),
inference(avatar_component_clause,[],[f9514]) ).
fof(f9516,plain,
( spl0_1318
| ~ spl0_11
| ~ spl0_1216 ),
inference(avatar_split_clause,[],[f9060,f8736,f66,f9514]) ).
fof(f15756,plain,
( ! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),multiply(inverse(X2),inverse(multiply(inverse(X0),X0))))) = X2
| ~ spl0_1216
| ~ spl0_1318 ),
inference(superposition,[],[f9515,f8737]) ).
fof(f16109,definition,
( spl0_1954
<=> ! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),multiply(inverse(X2),inverse(multiply(inverse(X0),X0))))) = X2 ),
introduced(definition,[new_symbols(definition,[spl0_1954])],[avatar_definition]) ).
fof(f16110,plain,
( ! [X2,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),multiply(inverse(X2),inverse(multiply(inverse(X0),X0))))) = X2
| ~ spl0_1954 ),
inference(avatar_component_clause,[],[f16109]) ).
fof(f16177,plain,
( spl0_1954
| ~ spl0_1216
| ~ spl0_1318 ),
inference(avatar_split_clause,[],[f15756,f9514,f8736,f16109]) ).
fof(f16856,plain,
( ! [X2,X0,X1] : inverse(multiply(inverse(X2),X2)) = inverse(multiply(inverse(inverse(multiply(inverse(X1),X1))),multiply(inverse(X0),X0)))
| ~ spl0_1216
| ~ spl0_1954 ),
inference(superposition,[],[f16110,f8737]) ).
fof(f17190,definition,
( spl0_2063
<=> ! [X2,X0,X1] : inverse(multiply(inverse(X2),X2)) = inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),multiply(inverse(X1),X1))) ),
introduced(definition,[new_symbols(definition,[spl0_2063])],[avatar_definition]) ).
fof(f17191,plain,
( ! [X2,X0,X1] : inverse(multiply(inverse(X2),X2)) = inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),multiply(inverse(X1),X1)))
| ~ spl0_2063 ),
inference(avatar_component_clause,[],[f17190]) ).
fof(f17208,plain,
( spl0_2063
| ~ spl0_1216
| ~ spl0_1954 ),
inference(avatar_split_clause,[],[f16856,f16109,f8736,f17190]) ).
fof(f17787,plain,
( ! [X2,X3,X0,X1] : multiply(inverse(X2),X2) = inverse(multiply(inverse(inverse(multiply(inverse(multiply(inverse(X0),X0)),multiply(inverse(inverse(multiply(inverse(X1),X1))),X3)))),multiply(inverse(X3),inverse(multiply(inverse(X3),X3)))))
| ~ spl0_11
| ~ spl0_2063 ),
inference(superposition,[],[f67,f17191]) ).
fof(f18061,plain,
( ! [X2,X1] : multiply(inverse(X2),X2) = inverse(multiply(inverse(X1),X1))
| ~ spl0_11
| ~ spl0_1295
| ~ spl0_2063 ),
inference(forward_demodulation,[],[f17787,f9422]) ).
fof(f18737,definition,
( spl0_2313
<=> ! [X2,X1] : multiply(inverse(X2),X2) = inverse(multiply(inverse(X1),X1)) ),
introduced(definition,[new_symbols(definition,[spl0_2313])],[avatar_definition]) ).
fof(f18738,plain,
( ! [X2,X1] : multiply(inverse(X2),X2) = inverse(multiply(inverse(X1),X1))
| ~ spl0_2313 ),
inference(avatar_component_clause,[],[f18737]) ).
fof(f18744,plain,
( spl0_2313
| ~ spl0_11
| ~ spl0_1295
| ~ spl0_2063 ),
inference(avatar_split_clause,[],[f18061,f17190,f9421,f66,f18737]) ).
fof(f18855,plain,
( ! [X0,X1] : multiply(inverse(X1),X1) = inverse(inverse(multiply(inverse(X0),X0)))
| ~ spl0_2313 ),
inference(superposition,[],[f18738,f18738]) ).
fof(f18907,plain,
( ! [X0] : a2 != multiply(inverse(multiply(inverse(X0),X0)),a2)
| ~ spl0_1306
| ~ spl0_2313 ),
inference(superposition,[],[f9466,f18738]) ).
fof(f19012,plain,
( ! [X2,X3,X0,X1] : multiply(inverse(X1),X2) = inverse(multiply(inverse(multiply(X3,inverse(multiply(inverse(inverse(multiply(inverse(X0),X0))),multiply(inverse(X2),inverse(multiply(inverse(X1),X1))))))),multiply(X3,X1)))
| ~ spl0_29
| ~ spl0_2313 ),
inference(superposition,[],[f182,f18738]) ).
fof(f19851,plain,
( ! [X2,X3,X1] : multiply(inverse(X1),X2) = inverse(multiply(inverse(multiply(X3,X2)),multiply(X3,X1)))
| ~ spl0_29
| ~ spl0_1954
| ~ spl0_2313 ),
inference(forward_demodulation,[],[f19012,f16110]) ).
fof(f19920,definition,
( spl0_2487
<=> ! [X0] : a2 != multiply(inverse(multiply(inverse(X0),X0)),a2) ),
introduced(definition,[new_symbols(definition,[spl0_2487])],[avatar_definition]) ).
fof(f19921,plain,
( ! [X0] : a2 != multiply(inverse(multiply(inverse(X0),X0)),a2)
| ~ spl0_2487 ),
inference(avatar_component_clause,[],[f19920]) ).
fof(f20072,plain,
( spl0_2487
| ~ spl0_1306
| ~ spl0_2313 ),
inference(avatar_split_clause,[],[f18907,f18737,f9465,f19920]) ).
fof(f20121,definition,
( spl0_2529
<=> ! [X0,X1] : multiply(inverse(X1),X1) = inverse(inverse(multiply(inverse(X0),X0))) ),
introduced(definition,[new_symbols(definition,[spl0_2529])],[avatar_definition]) ).
fof(f20122,plain,
( ! [X0,X1] : multiply(inverse(X1),X1) = inverse(inverse(multiply(inverse(X0),X0)))
| ~ spl0_2529 ),
inference(avatar_component_clause,[],[f20121]) ).
fof(f20123,plain,
( spl0_2529
| ~ spl0_2313 ),
inference(avatar_split_clause,[],[f18855,f18737,f20121]) ).
fof(f20265,definition,
( spl0_2561
<=> ! [X2,X1,X3] : multiply(inverse(X1),X2) = inverse(multiply(inverse(multiply(X3,X2)),multiply(X3,X1))) ),
introduced(definition,[new_symbols(definition,[spl0_2561])],[avatar_definition]) ).
fof(f20266,plain,
( ! [X2,X3,X1] : multiply(inverse(X1),X2) = inverse(multiply(inverse(multiply(X3,X2)),multiply(X3,X1)))
| ~ spl0_2561 ),
inference(avatar_component_clause,[],[f20265]) ).
fof(f20267,plain,
( spl0_2561
| ~ spl0_29
| ~ spl0_1954
| ~ spl0_2313 ),
inference(avatar_split_clause,[],[f19851,f18737,f16109,f181,f20265]) ).
fof(f20313,plain,
( ! [X0] : a2 != multiply(inverse(inverse(multiply(inverse(X0),X0))),a2)
| ~ spl0_2313
| ~ spl0_2487 ),
inference(superposition,[],[f19921,f18738]) ).
fof(f20388,definition,
( spl0_2570
<=> ! [X0] : a2 != multiply(inverse(inverse(multiply(inverse(X0),X0))),a2) ),
introduced(definition,[new_symbols(definition,[spl0_2570])],[avatar_definition]) ).
fof(f20389,plain,
( ! [X0] : a2 != multiply(inverse(inverse(multiply(inverse(X0),X0))),a2)
| ~ spl0_2570 ),
inference(avatar_component_clause,[],[f20388]) ).
fof(f20390,plain,
( spl0_2570
| ~ spl0_2313
| ~ spl0_2487 ),
inference(avatar_split_clause,[],[f20313,f19920,f18737,f20388]) ).
fof(f20830,plain,
( ! [X2,X3,X0,X1] : inverse(multiply(inverse(inverse(multiply(inverse(multiply(X1,X2)),multiply(X1,X3)))),multiply(inverse(X3),inverse(inverse(inverse(multiply(inverse(X0),X0))))))) = X2
| ~ spl0_11
| ~ spl0_2529 ),
inference(superposition,[],[f67,f20122]) ).
fof(f20868,plain,
( ! [X0] : a2 != multiply(inverse(inverse(inverse(inverse(multiply(inverse(X0),X0))))),a2)
| ~ spl0_2529
| ~ spl0_2570 ),
inference(superposition,[],[f20389,f20122]) ).
fof(f21509,definition,
( spl0_2693
<=> ! [X0] : a2 != multiply(inverse(inverse(inverse(inverse(multiply(inverse(X0),X0))))),a2) ),
introduced(definition,[new_symbols(definition,[spl0_2693])],[avatar_definition]) ).
fof(f21510,plain,
( ! [X0] : a2 != multiply(inverse(inverse(inverse(inverse(multiply(inverse(X0),X0))))),a2)
| ~ spl0_2693 ),
inference(avatar_component_clause,[],[f21509]) ).
fof(f21511,plain,
( spl0_2693
| ~ spl0_2529
| ~ spl0_2570 ),
inference(avatar_split_clause,[],[f20868,f20388,f20121,f21509]) ).
fof(f21580,plain,
( ! [X2,X3,X0] : inverse(multiply(inverse(multiply(inverse(X3),X2)),multiply(inverse(X3),inverse(inverse(inverse(multiply(inverse(X0),X0))))))) = X2
| ~ spl0_11
| ~ spl0_2529
| ~ spl0_2561 ),
inference(forward_demodulation,[],[f20830,f20266]) ).
fof(f21937,plain,
( ! [X2,X0] : multiply(inverse(inverse(inverse(inverse(multiply(inverse(X0),X0))))),X2) = X2
| ~ spl0_11
| ~ spl0_2529
| ~ spl0_2561 ),
inference(forward_demodulation,[],[f21580,f20266]) ).
fof(f22041,definition,
( spl0_2795
<=> ! [X2,X0] : multiply(inverse(inverse(inverse(inverse(multiply(inverse(X0),X0))))),X2) = X2 ),
introduced(definition,[new_symbols(definition,[spl0_2795])],[avatar_definition]) ).
fof(f22042,plain,
( ! [X2,X0] : multiply(inverse(inverse(inverse(inverse(multiply(inverse(X0),X0))))),X2) = X2
| ~ spl0_2795 ),
inference(avatar_component_clause,[],[f22041]) ).
fof(f22049,plain,
( spl0_2795
| ~ spl0_11
| ~ spl0_2529
| ~ spl0_2561 ),
inference(avatar_split_clause,[],[f21937,f20265,f20121,f66,f22041]) ).
fof(f22073,plain,
( $false
| ~ spl0_2693
| ~ spl0_2795 ),
inference(backward_subsumption_resolution,[],[f21510,f22042]) ).
fof(f22074,plain,
( ~ spl0_2693
| ~ spl0_2795 ),
inference(avatar_contradiction_clause,[],[f22073]) ).
cnf(s1,plain,
~ spl0_1,
inference(sat_conversion,[],[f8]) ).
cnf(s2,plain,
spl0_2,
inference(sat_conversion,[],[f12]) ).
cnf(s3,plain,
( ~ spl0_2
| spl0_3 ),
inference(sat_conversion,[],[f19]) ).
cnf(s11,plain,
( ~ spl0_2
| ~ spl0_3
| spl0_11 ),
inference(sat_conversion,[],[f68]) ).
cnf(s16,plain,
( ~ spl0_3
| spl0_15 ),
inference(sat_conversion,[],[f84]) ).
cnf(s27,plain,
( ~ spl0_2
| ~ spl0_15
| spl0_26 ),
inference(sat_conversion,[],[f171]) ).
cnf(s30,plain,
( ~ spl0_2
| ~ spl0_15
| spl0_29 ),
inference(sat_conversion,[],[f183]) ).
cnf(s51,plain,
( ~ spl0_2
| ~ spl0_15
| spl0_35 ),
inference(sat_conversion,[],[f208]) ).
cnf(s67,plain,
( ~ spl0_2
| ~ spl0_35
| spl0_43 ),
inference(sat_conversion,[],[f294]) ).
cnf(s130,plain,
( ~ spl0_29
| ~ spl0_35
| spl0_79 ),
inference(sat_conversion,[],[f533]) ).
cnf(s1923,plain,
( ~ spl0_26
| ~ spl0_43
| ~ spl0_79
| spl0_973 ),
inference(sat_conversion,[],[f7142]) ).
cnf(s1978,plain,
( ~ spl0_43
| ~ spl0_973
| spl0_1013 ),
inference(sat_conversion,[],[f7501]) ).
cnf(s2312,plain,
( ~ spl0_973
| ~ spl0_1013
| spl0_1216 ),
inference(sat_conversion,[],[f8739]) ).
cnf(s2430,plain,
( ~ spl0_11
| ~ spl0_1216
| spl0_1295 ),
inference(sat_conversion,[],[f9423]) ).
cnf(s2441,plain,
( spl0_1
| ~ spl0_1216
| spl0_1306 ),
inference(sat_conversion,[],[f9467]) ).
cnf(s2457,plain,
( ~ spl0_11
| ~ spl0_1216
| spl0_1318 ),
inference(sat_conversion,[],[f9516]) ).
cnf(s3977,plain,
( ~ spl0_1216
| ~ spl0_1318
| spl0_1954 ),
inference(sat_conversion,[],[f16177]) ).
cnf(s4117,plain,
( ~ spl0_1216
| ~ spl0_1954
| spl0_2063 ),
inference(sat_conversion,[],[f17208]) ).
cnf(s4512,plain,
( ~ spl0_11
| ~ spl0_1295
| ~ spl0_2063
| spl0_2313 ),
inference(sat_conversion,[],[f18744]) ).
cnf(s4807,plain,
( ~ spl0_1306
| ~ spl0_2313
| spl0_2487 ),
inference(sat_conversion,[],[f20072]) ).
cnf(s4832,plain,
( ~ spl0_2313
| spl0_2529 ),
inference(sat_conversion,[],[f20123]) ).
cnf(s4904,plain,
( ~ spl0_29
| ~ spl0_1954
| ~ spl0_2313
| spl0_2561 ),
inference(sat_conversion,[],[f20267]) ).
cnf(s4918,plain,
( ~ spl0_2313
| ~ spl0_2487
| spl0_2570 ),
inference(sat_conversion,[],[f20390]) ).
cnf(s5117,plain,
( ~ spl0_2529
| ~ spl0_2570
| spl0_2693 ),
inference(sat_conversion,[],[f21511]) ).
cnf(s5318,plain,
( ~ spl0_11
| ~ spl0_2529
| ~ spl0_2561
| spl0_2795 ),
inference(sat_conversion,[],[f22049]) ).
cnf(s5325,plain,
( ~ spl0_2693
| ~ spl0_2795 ),
inference(sat_conversion,[],[f22074]) ).
cnf(s5332,plain,
spl0_3,
inference(rat,[],[s3,s2]) ).
cnf(s5339,plain,
spl0_15,
inference(rat,[],[s16,s5332]) ).
cnf(s5343,plain,
spl0_11,
inference(rat,[],[s11,s2,s5332]) ).
cnf(s5349,plain,
spl0_35,
inference(rat,[],[s51,s2,s5339]) ).
cnf(s5355,plain,
spl0_29,
inference(rat,[],[s30,s2,s5339]) ).
cnf(s5358,plain,
spl0_26,
inference(rat,[],[s27,s2,s5339]) ).
cnf(s5385,plain,
spl0_43,
inference(rat,[],[s67,s2,s5349]) ).
cnf(s5439,plain,
spl0_79,
inference(rat,[],[s130,s5349,s5355]) ).
cnf(s5621,plain,
spl0_973,
inference(rat,[],[s1923,s5358,s5439,s5385]) ).
cnf(s5997,plain,
spl0_1013,
inference(rat,[],[s1978,s5385,s5621]) ).
cnf(s6209,plain,
spl0_1216,
inference(rat,[],[s2312,s5621,s5997]) ).
cnf(s6482,plain,
spl0_1318,
inference(rat,[],[s2457,s5343,s6209]) ).
cnf(s6504,plain,
spl0_1295,
inference(rat,[],[s2430,s5343,s6209]) ).
cnf(s6681,plain,
spl0_1954,
inference(rat,[],[s3977,s6209,s6482]) ).
cnf(s6834,plain,
spl0_2063,
inference(rat,[],[s4117,s6209,s6681]) ).
cnf(s7077,plain,
spl0_2313,
inference(rat,[],[s4512,s6504,s5343,s6834]) ).
cnf(s7441,plain,
spl0_2529,
inference(rat,[],[s4832,s7077]) ).
cnf(s7628,plain,
spl0_2561,
inference(rat,[],[s4904,s6681,s5355,s7077]) ).
cnf(s7828,plain,
spl0_2795,
inference(rat,[],[s5318,s7441,s5343,s7628]) ).
cnf(s7993,plain,
~ spl0_2693,
inference(rat,[],[s5325,s7828]) ).
cnf(s7996,plain,
~ spl0_2570,
inference(rat,[],[s5117,s7441,s7993]) ).
cnf(s7997,plain,
~ spl0_2487,
inference(rat,[],[s4918,s7077,s7996]) ).
cnf(s7998,plain,
~ spl0_1306,
inference(rat,[],[s4807,s7077,s7997]) ).
cnf(s8002,plain,
spl0_1,
inference(rat,[],[s2441,s6209,s7998]) ).
cnf(s8003,plain,
$false,
inference(rat,[],[s1,s8002]) ).
fof(f22088,plain,
$false,
inference(avatar_sat_refutation,[],[s8003]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : GRP422-1 : TPTP v9.3.1. Released v2.6.0.
% 0.00/0.07 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.16/0.44 % Computer : n019.cluster.edu
% 0.16/0.44 % Model : x86_64 x86_64
% 0.16/0.44 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.44 % Memory : 8046.5625MB
% 0.16/0.44 % OS : Linux 6.8.0-71-generic
% 0.16/0.44 % CPULimit : 300
% 0.16/0.44 % WCLimit : 300
% 0.16/0.44 % DateTime : Sun Sep 27 10:04:03 UTC 2026
% 0.16/0.44 % CPUTime :
% 0.16/0.44 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.21/0.49 Running first-order model finding
% 0.21/0.49 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
% 18.05/3.11 % (2852796)Will run a generic schedule for satisfiability detection.
% 18.05/3.11 % (2852805)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=65178864:i=116_3000 on theBenchmark for (3000ds/116Mi)
% 18.05/3.11 % (2852806)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1130227871:i=131_3000 on theBenchmark for (3000ds/131Mi)
% 18.05/3.11 % (2852802)% WARNING: option uhcvi not known.
% 18.05/3.11 % (2852803)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1485000647:i=88024:add=on:rawr=on_3000 on theBenchmark for (3000ds/88024Mi)
% 18.05/3.11 % (2852801)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1201061857_3000 on theBenchmark for (3000ds/0Mi)
% 18.05/3.11 % (2852802)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4143311153:i=135531:add=off:rawr=on_3000 on theBenchmark for (3000ds/135531Mi)
% 18.05/3.11 % (2852804)dis+10_1_sil=32000:sp=arity:random_seed=2961076918:i=103:fgj=on_3000 on theBenchmark for (3000ds/103Mi)
% 18.05/3.11 % (2852807)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3565040202:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_3000 on theBenchmark for (3000ds/159Mi)
% 18.05/3.11 % TRYING [1]
% 18.05/3.11 % TRYING [2]
% 18.05/3.11 % TRYING [3]
% 18.05/3.11 % TRYING [4]
% 18.05/3.11 % (2852805)Instruction limit reached!
% 18.05/3.11 % (2852805)------------------------------
% 18.05/3.11 % (2852805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.05/3.11 % (2852805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.05/3.11 % (2852805)CaDiCaL version: 2.1.3
% 18.05/3.11 % (2852805)Termination reason: Instruction limit
% 18.05/3.11 % (2852805)Termination phase: Saturation
% 18.05/3.11 % (2852805)Time elapsed: 0.058 s
% 18.05/3.11 % (2852805)Peak memory usage: 12 MB
% 18.05/3.11 % (2852805)Instructions burned: 117 (million)
% 18.05/3.11 % (2852815)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2458892662:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 18.05/3.11 % TRYING [1]
% 18.05/3.11 % TRYING [2]
% 18.05/3.11 % TRYING [3]
% 18.05/3.11 % (2852804)Instruction limit reached!
% 18.05/3.11 % (2852804)------------------------------
% 18.05/3.11 % (2852804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.05/3.11 % (2852804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.05/3.11 % (2852804)CaDiCaL version: 2.1.3
% 18.05/3.11 % (2852804)Termination reason: Instruction limit
% 18.05/3.11 % (2852804)Termination phase: Saturation
% 18.05/3.11 % (2852804)Time elapsed: 0.091 s
% 18.05/3.11 % (2852804)Peak memory usage: 11 MB
% 18.05/3.11 % (2852804)Instructions burned: 103 (million)
% 18.05/3.11 % TRYING [4]
% 18.05/3.11 % (2852806)Instruction limit reached!
% 18.05/3.11 % (2852806)------------------------------
% 18.05/3.11 % (2852806)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.05/3.11 % (2852806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.05/3.11 % (2852806)CaDiCaL version: 2.1.3
% 18.05/3.11 % (2852806)Termination reason: Instruction limit
% 18.05/3.11 % (2852806)Termination phase: Saturation
% 18.05/3.11 % (2852806)Time elapsed: 0.129 s
% 18.05/3.11 % (2852806)Peak memory usage: 13 MB
% 18.05/3.11 % (2852806)Instructions burned: 131 (million)
% 18.05/3.11 % (2852817)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1421804500:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 18.05/3.11 % (2852818)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=455267974:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 18.05/3.11 % (2852807)Instruction limit reached!
% 18.05/3.11 % (2852807)------------------------------
% 18.05/3.11 % (2852807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.05/3.11 % (2852807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 18.05/3.11 % (2852807)CaDiCaL version: 2.1.3
% 18.05/3.11 % (2852807)Termination reason: Instruction limit
% 18.05/3.11 % (2852807)Termination phase: Saturation
% 18.05/3.11 % (2852807)Time elapsed: 0.154 s
% 18.05/3.11 % (2852807)Peak memory usage: 13 MB
% 18.05/3.11 % (2852807)Instructions burned: 159 (million)
% 18.05/3.11 % (2852821)ott-21_1_sil=16000:fs=off:random_seed=20083869:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 18.05/3.11 % (2852817)Instruction limit reached!
% 18.05/3.11 % (2852817)------------------------------
% 18.05/3.11 % (2852817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 18.05/3.11 % (2852817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.48/6.27 % (2852817)CaDiCaL version: 2.1.3
% 40.48/6.27 % (2852817)Termination reason: Instruction limit
% 40.48/6.27 % (2852817)Termination phase: Saturation
% 40.48/6.27 % (2852817)Time elapsed: 0.128 s
% 40.48/6.27 % (2852817)Peak memory usage: 13 MB
% 40.48/6.27 % (2852817)Instructions burned: 132 (million)
% 40.48/6.27 % (2852823)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1108406432:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 40.48/6.27 % (2852821)Instruction limit reached!
% 40.48/6.27 % (2852821)------------------------------
% 40.48/6.27 % (2852821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.48/6.27 % (2852821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.48/6.27 % (2852821)CaDiCaL version: 2.1.3
% 40.48/6.27 % (2852821)Termination reason: Instruction limit
% 40.48/6.27 % (2852821)Termination phase: Saturation
% 40.48/6.27 % (2852821)Time elapsed: 0.152 s
% 40.48/6.27 % (2852821)Peak memory usage: 11 MB
% 40.48/6.27 % (2852821)Instructions burned: 181 (million)
% 40.48/6.27 % (2852825)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4251181922:fmbsr=1.3:i=865:ins=25_2996 on theBenchmark for (2996ds/865Mi)
% 40.48/6.27 % TRYING [1]
% 40.48/6.27 % TRYING [2]
% 40.48/6.27 % TRYING [3]
% 40.48/6.27 % TRYING [4]
% 40.48/6.27 % (2852815)Instruction limit reached!
% 40.48/6.27 % (2852815)------------------------------
% 40.48/6.27 % (2852815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.48/6.27 % (2852815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.48/6.27 % (2852815)CaDiCaL version: 2.1.3
% 40.48/6.27 % (2852815)Termination reason: Instruction limit
% 40.48/6.27 % (2852815)Termination phase: Finite model building SAT solving
% 40.48/6.27 % (2852815)Time elapsed: 0.335 s
% 40.48/6.27 % (2852815)Peak memory usage: 12 MB
% 40.48/6.27 % (2852815)Instructions burned: 715 (million)
% 40.48/6.27 % (2852827)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=1476233405:i=1179_2995 on theBenchmark for (2995ds/1179Mi)
% 40.48/6.27 % (2852823)Instruction limit reached!
% 40.48/6.27 % (2852823)------------------------------
% 40.48/6.27 % (2852823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.48/6.27 % (2852823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.48/6.27 % (2852823)CaDiCaL version: 2.1.3
% 40.48/6.27 % (2852823)Termination reason: Instruction limit
% 40.48/6.27 % (2852823)Termination phase: Saturation
% 40.48/6.27 % (2852823)Time elapsed: 0.398 s
% 40.48/6.27 % (2852823)Peak memory usage: 14 MB
% 40.48/6.27 % (2852823)Instructions burned: 479 (million)
% 40.48/6.27 % (2852818)Instruction limit reached!
% 40.48/6.27 % (2852818)------------------------------
% 40.48/6.27 % (2852818)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.48/6.27 % (2852818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.48/6.27 % (2852818)CaDiCaL version: 2.1.3
% 40.48/6.27 % (2852818)Termination reason: Instruction limit
% 40.48/6.27 % (2852818)Termination phase: Saturation
% 40.48/6.27 % (2852818)Time elapsed: 0.555 s
% 40.48/6.27 % (2852818)Peak memory usage: 16 MB
% 40.48/6.27 % (2852818)Instructions burned: 685 (million)
% 40.48/6.27 % (2852830)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=31039774:i=889:ins=1_2992 on theBenchmark for (2992ds/889Mi)
% 40.48/6.27 % (2852832)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=4052681049:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2992 on theBenchmark for (2992ds/692Mi)
% 40.48/6.27 % TRYING [14]
% 40.48/6.27 % TRYING [5]
% 40.48/6.27 % (2852827)Instruction limit reached!
% 40.48/6.27 % (2852827)------------------------------
% 40.48/6.27 % (2852827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 40.48/6.27 % (2852827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 40.48/6.27 % (2852827)CaDiCaL version: 2.1.3
% 40.48/6.27 % (2852827)Termination reason: Instruction limit
% 40.48/6.27 % (2852827)Termination phase: Saturation
% 40.48/6.27 % (2852827)Time elapsed: 0.446 s
% 40.48/6.27 % (2852827)Peak memory usage: 23 MB
% 40.48/6.27 % (2852827)Instructions burned: 1179 (million)
% 40.48/6.27 % (2852871)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3342856519:i=879:kws=inv_precedence:fsr=off_2990 on theBenchmark for (2990ds/879Mi)
% 40.48/6.27 % (2852825)Instruction limit reached!
% 40.48/6.27 % (2852825)------------------------------
% 40.48/6.27 % (2852825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.59/20.06 % (2852825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.59/20.06 % (2852825)CaDiCaL version: 2.1.3
% 138.59/20.06 % (2852825)Termination reason: Instruction limit
% 138.59/20.06 % (2852825)Termination phase: Finite model building SAT solving
% 138.59/20.06 % (2852825)Time elapsed: 0.579 s
% 138.59/20.06 % (2852825)Peak memory usage: 12 MB
% 138.59/20.06 % (2852825)Instructions burned: 866 (million)
% 138.59/20.06 % (2852898)fmb+10_1_sil=64000:random_seed=2913908024:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 138.59/20.06 % TRYING [1]
% 138.59/20.06 % TRYING [2]
% 138.59/20.06 % TRYING [3]
% 138.59/20.06 % TRYING [4]
% 138.59/20.06 % (2852830)Instruction limit reached!
% 138.59/20.06 % (2852830)------------------------------
% 138.59/20.06 % (2852830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.59/20.06 % (2852830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.59/20.06 % (2852830)CaDiCaL version: 2.1.3
% 138.59/20.06 % (2852830)Termination reason: Instruction limit
% 138.59/20.06 % (2852830)Termination phase: Finite model building constraint generation
% 138.59/20.06 % (2852830)Time elapsed: 0.315 s
% 138.59/20.06 % (2852830)Peak memory usage: 80 MB
% 138.59/20.06 % (2852830)Instructions burned: 890 (million)
% 138.59/20.06 % (2852921)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=4080240381:i=9515:nm=5_2989 on theBenchmark for (2989ds/9515Mi)
% 138.59/20.06 % TRYING [20]
% 138.59/20.06 % TRYING [5]
% 138.59/20.06 % (2852832)Instruction limit reached!
% 138.59/20.06 % (2852832)------------------------------
% 138.59/20.06 % (2852832)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.59/20.06 % (2852832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.59/20.06 % (2852832)CaDiCaL version: 2.1.3
% 138.59/20.06 % (2852832)Termination reason: Instruction limit
% 138.59/20.06 % (2852832)Termination phase: Saturation
% 138.59/20.06 % (2852832)Time elapsed: 0.409 s
% 138.59/20.06 % (2852832)Peak memory usage: 18 MB
% 138.59/20.06 % (2852832)Instructions burned: 693 (million)
% 138.59/20.06 % (2852945)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2243797015:fmbsr=1.7:i=920_2988 on theBenchmark for (2988ds/920Mi)
% 138.59/20.06 % TRYING [8]
% 138.59/20.06 % (2852871)Instruction limit reached!
% 138.59/20.06 % (2852871)------------------------------
% 138.59/20.06 % (2852871)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.59/20.06 % (2852871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.59/20.06 % (2852871)CaDiCaL version: 2.1.3
% 138.59/20.06 % (2852871)Termination reason: Instruction limit
% 138.59/20.06 % (2852871)Termination phase: Saturation
% 138.59/20.06 % (2852871)Time elapsed: 0.358 s
% 138.59/20.06 % (2852871)Peak memory usage: 16 MB
% 138.59/20.06 % (2852871)Instructions burned: 881 (million)
% 138.59/20.06 % (2852952)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=4178623517:i=5131_2987 on theBenchmark for (2987ds/5131Mi)
% 138.59/20.06 % TRYING [5]
% 138.59/20.06 % (2852945)Instruction limit reached!
% 138.59/20.06 % (2852945)------------------------------
% 138.59/20.06 % (2852945)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.59/20.06 % (2852945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.59/20.06 % (2852945)CaDiCaL version: 2.1.3
% 138.59/20.06 % (2852945)Termination reason: Instruction limit
% 138.59/20.06 % (2852945)Termination phase: Finite model building SAT solving
% 138.59/20.06 % (2852945)Time elapsed: 0.460 s
% 138.59/20.06 % (2852945)Peak memory usage: 37 MB
% 138.59/20.06 % (2852945)Instructions burned: 921 (million)
% 138.59/20.06 % (2852996)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=3907629901:i=1472:ins=7:fdi=8:gsp=on_2983 on theBenchmark for (2983ds/1472Mi)
% 138.59/20.06 % (2852996)Instruction limit reached!
% 138.59/20.06 % (2852996)------------------------------
% 138.59/20.06 % (2852996)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 138.59/20.06 % (2852996)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 138.59/20.06 % (2852996)CaDiCaL version: 2.1.3
% 138.59/20.06 % (2852996)Termination reason: Instruction limit
% 138.59/20.06 % (2852996)Termination phase: Saturation
% 138.59/20.06 % (2852996)Time elapsed: 0.573 s
% 138.59/20.06 % (2852996)Peak memory usage: 18 MB
% 138.59/20.06 % (2852996)Instructions burned: 1473 (million)
% 138.59/20.06 % (2852998)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1439665633:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 138.59/20.06 % TRYING [77]
% 138.59/20.06 % (2852952)Instruction limit reached!
% 138.59/20.06 % (2852952)------------------------------
% 219.18/31.47 % (2852952)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 219.18/31.47 % (2852952)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 219.18/31.47 % (2852952)CaDiCaL version: 2.1.3
% 219.18/31.47 % (2852952)Termination reason: Instruction limit
% 219.18/31.47 % (2852952)Termination phase: Saturation
% 219.18/31.47 % (2852952)Time elapsed: 1.313 s
% 219.18/31.47 % (2852952)Peak memory usage: 43 MB
% 219.18/31.47 % (2852952)Instructions burned: 5133 (million)
% 219.18/31.47 % (2853000)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=1581324838:fmbsr=2.30978:i=2174_2973 on theBenchmark for (2973ds/2174Mi)
% 219.18/31.47 % TRYING [16]
% 219.18/31.47 % (2853000)Instruction limit reached!
% 219.18/31.47 % (2853000)------------------------------
% 219.18/31.47 % (2853000)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 219.18/31.47 % (2853000)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 219.18/31.47 % (2853000)CaDiCaL version: 2.1.3
% 219.18/31.47 % (2853000)Termination reason: Instruction limit
% 219.18/31.47 % (2853000)Termination phase: Finite model building constraint generation
% 219.18/31.47 % (2853000)Time elapsed: 0.424 s
% 219.18/31.47 % (2853000)Peak memory usage: 154 MB
% 219.18/31.47 % (2853000)Instructions burned: 2178 (million)
% 219.18/31.47 % (2853002)ott-2_1_sil=16000:newcnf=on:random_seed=2526984284:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2969 on theBenchmark for (2969ds/869Mi)
% 219.18/31.47 % (2853002)Instruction limit reached!
% 219.18/31.47 % (2853002)------------------------------
% 219.18/31.47 % (2853002)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 219.18/31.47 % (2853002)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 219.18/31.47 % (2853002)CaDiCaL version: 2.1.3
% 219.18/31.47 % (2853002)Termination reason: Instruction limit
% 219.18/31.47 % (2853002)Termination phase: Saturation
% 219.18/31.47 % (2853002)Time elapsed: 0.251 s
% 219.18/31.47 % (2853002)Peak memory usage: 19 MB
% 219.18/31.47 % (2853002)Instructions burned: 869 (million)
% 219.18/31.47 % (2853004)ott+10_1_sil=32000:tgt=ground:random_seed=2139677645:i=5114:av=off_2966 on theBenchmark for (2966ds/5114Mi)
% 219.18/31.47 % (2852998)Instruction limit reached!
% 219.18/31.47 % (2852998)------------------------------
% 219.18/31.47 % (2852998)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 219.18/31.47 % (2852998)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 219.18/31.47 % (2852998)CaDiCaL version: 2.1.3
% 219.18/31.47 % (2852998)Termination reason: Instruction limit
% 219.18/31.47 % (2852998)Termination phase: Finite model building constraint generation
% 219.18/31.47 % (2852998)Time elapsed: 2.322 s
% 219.18/31.47 % (2852998)Peak memory usage: 522 MB
% 219.18/31.47 % (2852998)Instructions burned: 6326 (million)
% 219.18/31.47 % (2853006)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1847527497:i=54282_2953 on theBenchmark for (2953ds/54282Mi)
% 219.18/31.47 % TRYING [1]
% 219.18/31.47 % TRYING [2]
% 219.18/31.47 % TRYING [3]
% 219.18/31.47 % TRYING [4]
% 219.18/31.47 % (2852921)Instruction limit reached!
% 219.18/31.47 % (2852921)------------------------------
% 219.18/31.47 % (2852921)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 219.18/31.47 % (2852921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 219.18/31.47 % (2852921)CaDiCaL version: 2.1.3
% 219.18/31.47 % (2852921)Termination reason: Instruction limit
% 219.18/31.47 % (2852921)Termination phase: Finite model building constraint generation
% 219.18/31.47 % (2852921)Time elapsed: 3.728 s
% 219.18/31.47 % (2852921)Peak memory usage: 663 MB
% 219.18/31.47 % (2852921)Instructions burned: 9515 (million)
% 219.18/31.47 % (2853004)Instruction limit reached!
% 219.18/31.47 % (2853004)------------------------------
% 219.18/31.47 % (2853004)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 219.18/31.47 % (2853004)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 219.18/31.47 % (2853004)CaDiCaL version: 2.1.3
% 219.18/31.47 % (2853004)Termination reason: Instruction limit
% 219.18/31.47 % (2853004)Termination phase: Saturation
% 219.18/31.47 % (2853004)Time elapsed: 1.529 s
% 219.18/31.47 % (2853004)Peak memory usage: 46 MB
% 219.18/31.47 % (2853004)Instructions burned: 5115 (million)
% 219.18/31.47 % (2853008)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=496908951:i=3512:aac=none_2951 on theBenchmark for (2951ds/3512Mi)
% 219.18/31.47 % (2853010)dis+21_1_sil=32000:sas=cadical:random_seed=3488673366:i=3773:amm=off_2951 on theBenchmark for (2951ds/3773Mi)
% 219.18/31.47 % TRYING [5]
% 219.18/31.47 % (2853008)Instruction limit reached!
% 219.18/31.47 % (2853008)------------------------------
% 233.60/42.71 % (2853008)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.60/42.71 % (2853008)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.60/42.71 % (2853008)CaDiCaL version: 2.1.3
% 233.60/42.71 % (2853008)Termination reason: Instruction limit
% 233.60/42.71 % (2853008)Termination phase: Saturation
% 233.60/42.71 % (2853008)Time elapsed: 0.889 s
% 233.60/42.71 % (2853008)Peak memory usage: 29 MB
% 233.60/42.71 % (2853008)Instructions burned: 3513 (million)
% 233.60/42.71 % (2853012)ott+11_1_sil=16000:gs=on:random_seed=1172034605:s2a=on:i=2251:s2at=3:kws=inv_arity_squared:nm=2:fsr=off:fsd=on_2942 on theBenchmark for (2942ds/2251Mi)
% 233.60/42.71 % (2853012)Instruction limit reached!
% 233.60/42.71 % (2853012)------------------------------
% 233.60/42.71 % (2853012)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.60/42.71 % (2853012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.60/42.71 % (2853012)CaDiCaL version: 2.1.3
% 233.60/42.71 % (2853012)Termination reason: Instruction limit
% 233.60/42.71 % (2853012)Termination phase: Saturation
% 233.60/42.71 % (2853012)Time elapsed: 0.617 s
% 233.60/42.71 % (2853012)Peak memory usage: 29 MB
% 233.60/42.71 % (2853012)Instructions burned: 2254 (million)
% 233.60/42.71 % (2853014)fmb+10_1_fmbas=predicate:sil=64000:tgt=ground:fmbss=7:random_seed=3987732232:fmbsr=1.6:i=67534_2935 on theBenchmark for (2935ds/67534Mi)
% 233.60/42.71 % TRYING [7]
% 233.60/42.71 % (2853010)Instruction limit reached!
% 233.60/42.71 % (2853010)------------------------------
% 233.60/42.71 % (2853010)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.60/42.71 % (2853010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.60/42.71 % (2853010)CaDiCaL version: 2.1.3
% 233.60/42.71 % (2853010)Termination reason: Instruction limit
% 233.60/42.71 % (2853010)Termination phase: Saturation
% 233.60/42.71 % (2853010)Time elapsed: 1.792 s
% 233.60/42.71 % (2853010)Peak memory usage: 30 MB
% 233.60/42.71 % (2853010)Instructions burned: 3773 (million)
% 233.60/42.71 % (2853016)ott-22_32_sil=16000:tgt=full:fdtod=off:sp=weighted_frequency:rnwc=on:alpa=false:random_seed=3626191495:avsq=on:i=4591:add=off:avsqr=1,16:kws=inv_arity:nm=10:ins=9:fdi=4_2932 on theBenchmark for (2932ds/4591Mi)
% 233.60/42.71 % (2853016)Instruction limit reached!
% 233.60/42.71 % (2853016)------------------------------
% 233.60/42.71 % (2853016)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.60/42.71 % (2853016)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.60/42.71 % (2853016)CaDiCaL version: 2.1.3
% 233.60/42.71 % (2853016)Termination reason: Instruction limit
% 233.60/42.71 % (2853016)Termination phase: Saturation
% 233.60/42.71 % (2853016)Time elapsed: 2.130 s
% 233.60/42.71 % (2853016)Peak memory usage: 62 MB
% 233.60/42.71 % (2853016)Instructions burned: 4591 (million)
% 233.60/42.71 % (2853018)dis+10_64_to=lpo:sil=32000:spb=intro:urr=on:sac=on:random_seed=3970716876:i=29340_2911 on theBenchmark for (2911ds/29340Mi)
% 233.60/42.71 % (2852898)Instruction limit reached!
% 233.60/42.71 % (2852898)------------------------------
% 233.60/42.71 % (2852898)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.60/42.71 % (2852898)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.60/42.71 % (2852898)CaDiCaL version: 2.1.3
% 233.60/42.71 % (2852898)Termination reason: Instruction limit
% 233.60/42.71 % (2852898)Termination phase: Finite model building SAT solving
% 233.60/42.71 % (2852898)Time elapsed: 13.299 s
% 233.60/42.71 % (2852898)Peak memory usage: 19 MB
% 233.60/42.71 % (2852898)Instructions burned: 22061 (million)
% 233.60/42.71 % (2853152)dis-10_1_sil=64000:sas=cadical:cn=on:random_seed=2522001120:i=5211_2856 on theBenchmark for (2856ds/5211Mi)
% 233.60/42.71 % (2853152)Instruction limit reached!
% 233.60/42.71 % (2853152)------------------------------
% 233.60/42.71 % (2853152)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.60/42.71 % (2853152)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.60/42.71 % (2853152)CaDiCaL version: 2.1.3
% 233.60/42.71 % (2853152)Termination reason: Instruction limit
% 233.60/42.71 % (2853152)Termination phase: Saturation
% 233.60/42.71 % (2853152)Time elapsed: 3.052 s
% 233.60/42.71 % (2853152)Peak memory usage: 43 MB
% 233.60/42.71 % (2853152)Instructions burned: 5212 (million)
% 233.60/42.71 % (2853292)fmb+10_1_sil=32000:sas=cadical:bce=on:fmbss=17:random_seed=712464363:i=5497:nm=2_2826 on theBenchmark for (2826ds/5497Mi)
% 233.60/42.71 % TRYING [17]
% 233.60/42.71 % (2853292)Instruction limit reached!
% 233.60/42.71 % (2853292)------------------------------
% 233.60/42.71 % (2853292)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.60/42.71 % (2853292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.60/42.71 % (2853292)CaDiCaL version: 2.1.3
% 233.60/42.71 % (2853292)Termination reason: Instruction limit
% 233.60/42.71 % (2853292)Termination phase: Finite model building constraint generation
% 233.60/42.71 % (2853292)Time elapsed: 2.156 s
% 233.60/42.71 % (2853292)Peak memory usage: 384 MB
% 233.60/42.71 % (2853292)Instructions burned: 5499 (million)
% 233.60/42.71 % (2853446)fmb+10_1_fmbas=predicate:sil=64000:tgt=full:sas=cadical:fmbss=15:random_seed=3040096822:fmbsr=2:i=46332_2803 on theBenchmark for (2803ds/46332Mi)
% 233.60/42.71 % TRYING [15]
% 233.60/42.71 % (2853014)Instruction limit reached!
% 233.60/42.71 % (2853014)------------------------------
% 233.60/42.71 % (2853014)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.60/42.71 % (2853014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.60/42.71 % (2853014)CaDiCaL version: 2.1.3
% 233.60/42.71 % (2853014)Termination reason: Instruction limit
% 233.60/42.71 % (2853014)Termination phase: Finite model building SAT solving
% 233.60/42.71 % (2853014)Time elapsed: 16.779 s
% 233.60/42.71 % (2853014)Peak memory usage: 46 MB
% 233.60/42.71 % (2853014)Instructions burned: 67536 (million)
% 233.60/42.71 % (2853448)fmb+10_1_sil=128000:tgt=full:sas=cadical:fmbss=12:random_seed=2338828079:i=14071_2768 on theBenchmark for (2768ds/14071Mi)
% 233.60/42.71 % TRYING [12]
% 233.60/42.71 % (2853018)Instruction limit reached!
% 233.60/42.71 % (2853018)------------------------------
% 233.60/42.71 % (2853018)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.60/42.71 % (2853018)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.60/42.71 % (2853018)CaDiCaL version: 2.1.3
% 233.60/42.71 % (2853018)Termination reason: Instruction limit
% 233.60/42.71 % (2853018)Termination phase: Saturation
% 233.60/42.71 % (2853018)Time elapsed: 15.112 s
% 233.60/42.71 % (2853018)Peak memory usage: 174 MB
% 233.60/42.71 % (2853018)Instructions burned: 29342 (million)
% 233.60/42.71 % (2853450)dis+10_161_sil=128000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2446213109:i=22565:add=on:rawr=on_2759 on theBenchmark for (2759ds/22565Mi)
% 233.60/42.71 % (2852803)Instruction limit reached!
% 233.60/42.71 % (2852803)------------------------------
% 233.60/42.71 % (2852803)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.60/42.71 % (2852803)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.60/42.71 % (2852803)CaDiCaL version: 2.1.3
% 233.60/42.71 % (2852803)Termination reason: Instruction limit
% 233.60/42.71 % (2852803)Termination phase: Saturation
% 233.60/42.71 % (2852803)Time elapsed: 26.828 s
% 233.60/42.71 % (2852803)Peak memory usage: 133 MB
% 233.60/42.71 % (2852803)Instructions burned: 88024 (million)
% 233.60/42.71 % (2853452)ott+4_1_sil=16000:sp=arity:gs=on:random_seed=1605869259:i=8173:av=off_2731 on theBenchmark for (2731ds/8173Mi)
% 233.60/42.71 % (2853448)Instruction limit reached!
% 233.60/42.71 % (2853448)------------------------------
% 233.60/42.71 % (2853448)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.60/42.71 % (2853448)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.60/42.71 % (2853448)CaDiCaL version: 2.1.3
% 233.60/42.71 % (2853448)Termination reason: Instruction limit
% 233.60/42.71 % (2853448)Termination phase: Finite model building SAT solving
% 233.60/42.71 % (2853448)Time elapsed: 4.868 s
% 233.60/42.71 % (2853448)Peak memory usage: 188 MB
% 233.60/42.71 % (2853448)Instructions burned: 14073 (million)
% 233.60/42.71 % (2853454)dis+10_16:1_sil=16000:random_seed=2074642512:i=9155:fsr=off_2719 on theBenchmark for (2719ds/9155Mi)
% 233.60/42.71 % (2853454)Instruction limit reached!
% 233.60/42.71 % (2853454)------------------------------
% 233.60/42.71 % (2853454)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.60/42.71 % (2853454)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.60/42.71 % (2853454)CaDiCaL version: 2.1.3
% 233.60/42.71 % (2853454)Termination reason: Instruction limit
% 233.60/42.71 % (2853454)Termination phase: Saturation
% 233.60/42.71 % (2853454)Time elapsed: 2.772 s
% 233.60/42.71 % (2853454)Peak memory usage: 50 MB
% 233.60/42.71 % (2853454)Instructions burned: 9158 (million)
% 233.60/42.71 % (2853735)ott-3_8_sil=64000:random_seed=2924102432:i=20139:bs=on_2691 on theBenchmark for (2691ds/20139Mi)
% 233.60/42.71 % (2853452)Instruction limit reached!
% 233.60/42.71 % (2853452)------------------------------
% 233.60/42.71 % (2853452)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.60/42.71 % (2853452)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.60/42.71 % (2853452)CaDiCaL version: 2.1.3
% 233.60/42.71 % (2853452)Termination reason: Instruction limit
% 233.60/42.71 % (2853452)Termination phase: Saturation
% 233.60/42.71 % (2853452)Time elapsed: 4.069 s
% 233.60/42.71 % (2853452)Peak memory usage: 67 MB
% 233.60/42.71 % (2853452)Instructions burned: 8174 (million)
% 233.60/42.71 % (2853757)fmb+10_1_sil=64000:tgt=ground:sas=cadical:bce=on:fmbss=9:random_seed=3770248384:fmbsr=2:i=32576_2690 on theBenchmark for (2690ds/32576Mi)
% 233.60/42.71 % TRYING [9]
% 233.60/42.71 % (2853450)Instruction limit reached!
% 233.60/42.71 % (2853450)------------------------------
% 233.60/42.71 % (2853450)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.60/42.71 % (2853450)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.60/42.71 % (2853450)CaDiCaL version: 2.1.3
% 233.60/42.71 % (2853450)Termination reason: Instruction limit
% 233.60/42.71 % (2853450)Termination phase: Saturation
% 233.60/42.71 % (2853450)Time elapsed: 8.012 s
% 233.60/42.71 % (2853450)Peak memory usage: 67 MB
% 233.60/42.71 % (2853450)Instructions burned: 22568 (million)
% 233.60/42.71 % (2853891)ott+10_8:1_sil=16000:sp=arity:gs=on:random_seed=3500982686:i=11404_2679 on theBenchmark for (2679ds/11404Mi)
% 233.60/42.71 % (2853735)Instruction limit reached!
% 233.60/42.71 % (2853735)------------------------------
% 233.60/42.71 % (2853735)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.60/42.71 % (2853735)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.60/42.71 % (2853735)CaDiCaL version: 2.1.3
% 233.60/42.71 % (2853735)Termination reason: Instruction limit
% 233.60/42.71 % (2853735)Termination phase: Saturation
% 233.60/42.71 % (2853735)Time elapsed: 6.440 s
% 233.60/42.71 % (2853735)Peak memory usage: 141 MB
% 233.60/42.71 % (2853735)Instructions burned: 20141 (million)
% 233.60/42.71 % (2853893)ott-11_1_sil=16000:alpa=false:sac=on:random_seed=594776215:i=14134_2626 on theBenchmark for (2626ds/14134Mi)
% 233.60/42.71 % (2853891)Instruction limit reached!
% 233.60/42.71 % (2853891)------------------------------
% 233.60/42.71 % (2853891)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.60/42.71 % (2853891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.60/42.71 % (2853891)CaDiCaL version: 2.1.3
% 233.60/42.71 % (2853891)Termination reason: Instruction limit
% 233.60/42.71 % (2853891)Termination phase: Saturation
% 233.60/42.71 % (2853891)Time elapsed: 5.482 s
% 233.60/42.71 % (2853891)Peak memory usage: 91 MB
% 233.60/42.71 % (2853891)Instructions burned: 11405 (million)
% 233.60/42.71 % (2853895)dis+33_16_sil=32000:sac=on:random_seed=2805654920:i=15851:nm=0_2624 on theBenchmark for (2624ds/15851Mi)
% 233.60/42.71 % TRYING [6]
% 233.60/42.71 % (2853006)Instruction limit reached!
% 233.60/42.71 % (2853006)------------------------------
% 233.60/42.71 % (2853006)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.60/42.71 % (2853006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.60/42.71 % (2853006)CaDiCaL version: 2.1.3
% 233.60/42.71 % (2853006)Termination reason: Instruction limit
% 233.60/42.71 % (2853006)Termination phase: Finite model building SAT solving
% 233.60/42.71 % (2853006)Time elapsed: 33.437 s
% 233.60/42.71 % (2853006)Peak memory usage: 24 MB
% 233.60/42.71 % (2853006)Instructions burned: 54282 (million)
% 233.60/42.71 % (2853898)dis+4_1024_sil=32000:avsql=on:sp=occurrence:gs=on:avsqc=1:random_seed=2345434597:avsq=on:i=17627:add=on:amm=off_2618 on theBenchmark for (2618ds/17627Mi)
% 233.60/42.71 % (2853893)Instruction limit reached!
% 233.60/42.71 % (2853893)------------------------------
% 233.60/42.71 % (2853893)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.60/42.71 % (2853893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.60/42.71 % (2853893)CaDiCaL version: 2.1.3
% 233.60/42.71 % (2853893)Termination reason: Instruction limit
% 233.60/42.71 % (2853893)Termination phase: Saturation
% 233.60/42.71 % (2853893)Time elapsed: 4.392 s
% 233.60/42.71 % (2853893)Peak memory usage: 125 MB
% 233.60/42.71 % (2853893)Instructions burned: 14137 (million)
% 233.60/42.71 % (2853900)ott+10_64_anc=all:sil=128000:sas=cadical:bsr=unit_only:nwc=1:cn=on:random_seed=700806916:s2a=on:i=53295_2582 on theBenchmark for (2582ds/53295Mi)
% 233.60/42.71 % (2853900) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2852796-2853900"...
% 233.60/42.71 % (2853900)...printing done.
% 233.60/42.71 % (2853900)Refutation found. Thanks to Tanya!
% 233.60/42.71 % SZS status Unsatisfiable for theBenchmark
% 233.60/42.71 % SZS output start Proof for theBenchmark
% See solution above
% 233.60/42.71 % (2853900)------------------------------
% 233.60/42.71 % (2853900)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 233.60/42.71 % (2853900)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 233.60/42.71 % (2853900)CaDiCaL version: 2.1.3
% 233.60/42.71 % (2853900)Termination reason: Refutation
% 233.60/42.71 % (2853900)Time elapsed: 0.367 s
% 233.60/42.71 % (2853900)Peak memory usage: 30 MB
% 233.60/42.71 % (2853900)Instructions burned: 1212 (million)
% 233.60/42.71 % (2852796)Success in time 42.208 s
% 233.60/42.71 % Vampire exiting
%------------------------------------------------------------------------------