%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : GRP775+1 : TPTP v9.3.1. Released v4.1.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n001.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 10:18:45 AM UTC 2026
% Result : Theorem 4.33s 1.06s
% Output : Refutation 4.33s
% Verified :
% SZS Type : Refutation
% Derivation depth : 21
% Number of leaves : 20
% Syntax : Number of formulae : 199 ( 38 unt; 14 def)
% Number of atoms : 488 ( 166 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 527 ( 238 ~; 247 |; 26 &)
% ( 15 <=>; 0 =>; 0 <=; 1 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 15 ( 13 usr; 11 prp; 0-2 aty)
% Number of functors : 8 ( 8 usr; 6 con; 0-2 aty)
% Number of variables : 94 ( 0 sgn 85 !; 9 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1,X2] : product(product(X2,X1),X0) = product(X2,product(X1,X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos01) ).
fof(f2,axiom,
! [X0] : product(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos02) ).
fof(f3,axiom,
! [X0,X1] :
( l(X0,X1)
<=> ( product(X0,X1) = X0
& product(X1,X0) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos03) ).
fof(f4,axiom,
! [X0,X1] :
( r(X0,X1)
<=> ( product(X0,X1) = X1
& product(X1,X0) = X0 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos04) ).
fof(f5,axiom,
! [X0,X1] :
( d(X0,X1)
<=> ? [X2] :
( r(X0,X2)
& l(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',sos05) ).
fof(f6,conjecture,
! [X0,X1] :
( d(X0,X1)
<=> ( product(X0,product(X1,X0)) = X0
& product(X1,product(X0,X1)) = X1 ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',goals) ).
fof(f7,negated_conjecture,
~ ! [X0,X1] :
( d(X0,X1)
<=> ( product(X0,product(X1,X0)) = X0
& product(X1,product(X0,X1)) = X1 ) ),
inference(negated_conjecture,[status(cth)],[f6]) ).
fof(f8,plain,
? [X0,X1] :
( d(X0,X1)
<~> ( product(X0,product(X1,X0)) = X0
& product(X1,product(X0,X1)) = X1 ) ),
inference(ennf_transformation,[],[f7]) ).
fof(f9,plain,
! [X0,X1] :
( ( l(X0,X1)
| product(X0,X1) != X0
| product(X1,X0) != X1 )
& ( ( product(X0,X1) = X0
& product(X1,X0) = X1 )
| ~ l(X0,X1) ) ),
inference(nnf_transformation,[],[f3]) ).
fof(f10,plain,
! [X0,X1] :
( ( l(X0,X1)
| product(X0,X1) != X0
| product(X1,X0) != X1 )
& ( ( product(X0,X1) = X0
& product(X1,X0) = X1 )
| ~ l(X0,X1) ) ),
inference(flattening,[],[f9]) ).
fof(f11,plain,
! [X0,X1] :
( ( r(X0,X1)
| product(X0,X1) != X1
| product(X1,X0) != X0 )
& ( ( product(X0,X1) = X1
& product(X1,X0) = X0 )
| ~ r(X0,X1) ) ),
inference(nnf_transformation,[],[f4]) ).
fof(f12,plain,
! [X0,X1] :
( ( r(X0,X1)
| product(X0,X1) != X1
| product(X1,X0) != X0 )
& ( ( product(X0,X1) = X1
& product(X1,X0) = X0 )
| ~ r(X0,X1) ) ),
inference(flattening,[],[f11]) ).
fof(f13,plain,
! [X0,X1] :
( ( d(X0,X1)
| ! [X2] :
( ~ r(X0,X2)
| ~ l(X2,X1) ) )
& ( ? [X2] :
( r(X0,X2)
& l(X2,X1) )
| ~ d(X0,X1) ) ),
inference(nnf_transformation,[],[f5]) ).
fof(f14,plain,
! [X0,X1] :
( ( d(X0,X1)
| ! [X2] :
( ~ r(X0,X2)
| ~ l(X2,X1) ) )
& ( ? [X3] :
( r(X0,X3)
& l(X3,X1) )
| ~ d(X0,X1) ) ),
inference(rectify,[],[f13]) ).
fof(f15,plain,
! [X0,X1] :
( ( d(X0,X1)
| ! [X2] :
( ~ r(X0,X2)
| ~ l(X2,X1) ) )
& ( ( r(X0,sK0(X0,X1))
& l(sK0(X0,X1),X1) )
| ~ d(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X3,sK0(X0,X1))],[f14]) ).
fof(f16,plain,
? [X0,X1] :
( ( product(X0,product(X1,X0)) != X0
| product(X1,product(X0,X1)) != X1
| ~ d(X0,X1) )
& ( ( product(X0,product(X1,X0)) = X0
& product(X1,product(X0,X1)) = X1 )
| d(X0,X1) ) ),
inference(nnf_transformation,[],[f8]) ).
fof(f17,plain,
? [X0,X1] :
( ( product(X0,product(X1,X0)) != X0
| product(X1,product(X0,X1)) != X1
| ~ d(X0,X1) )
& ( ( product(X0,product(X1,X0)) = X0
& product(X1,product(X0,X1)) = X1 )
| d(X0,X1) ) ),
inference(flattening,[],[f16]) ).
fof(f18,plain,
( ( sK1 != product(sK1,product(sK2,sK1))
| sK2 != product(sK2,product(sK1,sK2))
| ~ d(sK1,sK2) )
& ( ( sK1 = product(sK1,product(sK2,sK1))
& sK2 = product(sK2,product(sK1,sK2)) )
| d(sK1,sK2) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1,sK2]),skolemize(X0,sK1),skolemize(X1,sK2)],[f17]) ).
fof(f19,plain,
! [X2,X0,X1] : product(product(X2,X1),X0) = product(X2,product(X1,X0)),
inference(cnf_transformation,[],[f1]) ).
fof(f20,plain,
! [X0] : product(X0,X0) = X0,
inference(cnf_transformation,[],[f2]) ).
fof(f21,plain,
! [X0,X1] :
( ~ l(X0,X1)
| product(X1,X0) = X1 ),
inference(cnf_transformation,[],[f10]) ).
fof(f22,plain,
! [X0,X1] :
( ~ l(X0,X1)
| product(X0,X1) = X0 ),
inference(cnf_transformation,[],[f10]) ).
fof(f23,plain,
! [X0,X1] :
( product(X1,X0) != X1
| product(X0,X1) != X0
| l(X0,X1) ),
inference(cnf_transformation,[],[f10]) ).
fof(f24,plain,
! [X0,X1] :
( ~ r(X0,X1)
| product(X1,X0) = X0 ),
inference(cnf_transformation,[],[f12]) ).
fof(f25,plain,
! [X0,X1] :
( ~ r(X0,X1)
| product(X0,X1) = X1 ),
inference(cnf_transformation,[],[f12]) ).
fof(f26,plain,
! [X0,X1] :
( product(X1,X0) != X0
| product(X0,X1) != X1
| r(X0,X1) ),
inference(cnf_transformation,[],[f12]) ).
fof(f27,plain,
! [X0,X1] :
( ~ d(X0,X1)
| l(sK0(X0,X1),X1) ),
inference(cnf_transformation,[],[f15]) ).
fof(f28,plain,
! [X0,X1] :
( ~ d(X0,X1)
| r(X0,sK0(X0,X1)) ),
inference(cnf_transformation,[],[f15]) ).
fof(f29,plain,
! [X2,X0,X1] :
( ~ r(X0,X2)
| d(X0,X1)
| ~ l(X2,X1) ),
inference(cnf_transformation,[],[f15]) ).
fof(f30,plain,
( sK2 = product(sK2,product(sK1,sK2))
| d(sK1,sK2) ),
inference(cnf_transformation,[],[f18]) ).
fof(f31,plain,
( sK1 = product(sK1,product(sK2,sK1))
| d(sK1,sK2) ),
inference(cnf_transformation,[],[f18]) ).
fof(f32,plain,
( sK1 != product(sK1,product(sK2,sK1))
| sK2 != product(sK2,product(sK1,sK2))
| ~ d(sK1,sK2) ),
inference(cnf_transformation,[],[f18]) ).
fof(f33,definition,
sF3 = product(sK2,sK1),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
fof(f34,plain,
product(sK2,sK1) = sF3,
inference(reorient_equations,[],[f33]) ).
fof(f35,definition,
sF4 = product(sK1,sF3),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
fof(f36,plain,
product(sK1,sF3) = sF4,
inference(reorient_equations,[],[f35]) ).
fof(f37,definition,
sF5 = product(sK1,sK2),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f38,plain,
product(sK1,sK2) = sF5,
inference(reorient_equations,[],[f37]) ).
fof(f39,definition,
sF6 = product(sK2,sF5),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f40,plain,
product(sK2,sF5) = sF6,
inference(reorient_equations,[],[f39]) ).
fof(f41,plain,
( sK1 != sF4
| sK2 != sF6
| ~ d(sK1,sK2) ),
inference(definition_folding,[],[f32,f40,f38,f36,f34]) ).
fof(f42,plain,
( sK1 = sF4
| d(sK1,sK2) ),
inference(definition_folding,[],[f31,f36,f34]) ).
fof(f43,plain,
( sK2 = sF6
| d(sK1,sK2) ),
inference(definition_folding,[],[f30,f40,f38]) ).
fof(f45,definition,
( spl7_1
<=> d(sK1,sK2) ),
introduced(definition,[new_symbols(definition,[spl7_1])],[avatar_definition]) ).
fof(f46,plain,
( ~ d(sK1,sK2)
| spl7_1 ),
inference(avatar_component_clause,[],[f45]) ).
fof(f47,plain,
( d(sK1,sK2)
| ~ spl7_1 ),
inference(avatar_component_clause,[],[f45]) ).
fof(f49,definition,
( spl7_2
<=> sK2 = sF6 ),
introduced(definition,[new_symbols(definition,[spl7_2])],[avatar_definition]) ).
fof(f50,plain,
( sK2 != sF6
| spl7_2 ),
inference(avatar_component_clause,[],[f49]) ).
fof(f51,plain,
( sK2 = sF6
| ~ spl7_2 ),
inference(avatar_component_clause,[],[f49]) ).
fof(f52,plain,
( spl7_1
| spl7_2 ),
inference(avatar_split_clause,[],[f43,f49,f45]) ).
fof(f54,definition,
( spl7_3
<=> sK1 = sF4 ),
introduced(definition,[new_symbols(definition,[spl7_3])],[avatar_definition]) ).
fof(f55,plain,
( sK1 != sF4
| spl7_3 ),
inference(avatar_component_clause,[],[f54]) ).
fof(f56,plain,
( sK1 = sF4
| ~ spl7_3 ),
inference(avatar_component_clause,[],[f54]) ).
fof(f57,plain,
( spl7_1
| spl7_3 ),
inference(avatar_split_clause,[],[f42,f54,f45]) ).
fof(f58,plain,
( ~ spl7_1
| ~ spl7_2
| ~ spl7_3 ),
inference(avatar_split_clause,[],[f41,f54,f49,f45]) ).
fof(f59,plain,
! [X0,X1] : product(X0,X1) = product(X0,product(X0,X1)),
inference(superposition,[],[f19,f20]) ).
fof(f62,plain,
! [X0] : product(sK1,product(sK2,X0)) = product(sF5,X0),
inference(superposition,[],[f19,f38]) ).
fof(f63,plain,
! [X0] : product(sF3,X0) = product(sK2,product(sK1,X0)),
inference(superposition,[],[f19,f34]) ).
fof(f66,plain,
! [X0,X1] : product(X0,X1) = product(X0,product(X1,product(X0,X1))),
inference(superposition,[],[f20,f19]) ).
fof(f75,plain,
! [X2,X0,X1] :
( product(X0,X1) != product(X0,product(X1,X2))
| product(X2,product(X0,X1)) != X2
| l(X2,product(X0,X1)) ),
inference(superposition,[],[f23,f19]) ).
fof(f79,plain,
( sK2 != sF6
| sF5 != product(sF5,sK2)
| l(sF5,sK2) ),
inference(superposition,[],[f23,f40]) ).
fof(f84,plain,
( sF5 != product(sF5,sK2)
| l(sF5,sK2)
| ~ spl7_2 ),
inference(forward_subsumption_resolution,[],[f79,f51]) ).
fof(f89,definition,
( spl7_4
<=> l(sF5,sK2) ),
introduced(definition,[new_symbols(definition,[spl7_4])],[avatar_definition]) ).
fof(f90,plain,
( ~ l(sF5,sK2)
| spl7_4 ),
inference(avatar_component_clause,[],[f89]) ).
fof(f91,plain,
( l(sF5,sK2)
| ~ spl7_4 ),
inference(avatar_component_clause,[],[f89]) ).
fof(f93,definition,
( spl7_5
<=> sF5 = product(sF5,sK2) ),
introduced(definition,[new_symbols(definition,[spl7_5])],[avatar_definition]) ).
fof(f94,plain,
( sF5 = product(sF5,sK2)
| ~ spl7_5 ),
inference(avatar_component_clause,[],[f93]) ).
fof(f95,plain,
( sF5 != product(sF5,sK2)
| spl7_5 ),
inference(avatar_component_clause,[],[f93]) ).
fof(f96,plain,
( spl7_4
| ~ spl7_5
| ~ spl7_2 ),
inference(avatar_split_clause,[],[f84,f49,f93,f89]) ).
fof(f116,definition,
( spl7_10
<=> l(sF3,sK1) ),
introduced(definition,[new_symbols(definition,[spl7_10])],[avatar_definition]) ).
fof(f117,plain,
( ~ l(sF3,sK1)
| spl7_10 ),
inference(avatar_component_clause,[],[f116]) ).
fof(f118,plain,
( l(sF3,sK1)
| ~ spl7_10 ),
inference(avatar_component_clause,[],[f116]) ).
fof(f269,plain,
sF5 = product(sK1,sF5),
inference(superposition,[],[f59,f38]) ).
fof(f322,plain,
product(sK1,sF3) = product(sF5,sK1),
inference(superposition,[],[f62,f34]) ).
fof(f324,plain,
product(sK1,sK2) = product(sF5,sK2),
inference(superposition,[],[f62,f20]) ).
fof(f326,plain,
! [X0] : product(sF5,X0) = product(sK1,product(sF5,X0)),
inference(superposition,[],[f59,f62]) ).
fof(f334,plain,
sF5 = product(sF5,sK2),
inference(forward_demodulation,[],[f324,f38]) ).
fof(f336,plain,
sF4 = product(sF5,sK1),
inference(forward_demodulation,[],[f322,f36]) ).
fof(f338,plain,
( $false
| spl7_5 ),
inference(forward_subsumption_resolution,[],[f334,f95]) ).
fof(f339,plain,
spl7_5,
inference(avatar_contradiction_clause,[],[f338]) ).
fof(f340,plain,
( sK1 = product(sF5,sK1)
| ~ spl7_3 ),
inference(forward_demodulation,[],[f336,f56]) ).
fof(f349,plain,
product(sK2,sF5) = product(sF3,sK2),
inference(superposition,[],[f63,f38]) ).
fof(f351,plain,
! [X0] : product(sK2,product(sF5,X0)) = product(sF3,product(sK2,X0)),
inference(superposition,[],[f63,f62]) ).
fof(f357,plain,
! [X0] :
( sK2 != product(sF3,X0)
| product(sK1,X0) != product(product(sK1,X0),sK2)
| l(product(sK1,X0),sK2) ),
inference(superposition,[],[f23,f63]) ).
fof(f360,plain,
! [X0] :
( product(sK1,X0) != product(sK1,product(X0,sK2))
| sK2 != product(sF3,X0)
| l(product(sK1,X0),sK2) ),
inference(forward_demodulation,[],[f357,f19]) ).
fof(f366,plain,
sF6 = product(sF3,sK2),
inference(forward_demodulation,[],[f349,f40]) ).
fof(f377,plain,
( sK1 = product(sK1,sF3)
| ~ spl7_10 ),
inference(resolution,[],[f118,f21]) ).
fof(f438,plain,
( sK1 != sK1
| sF5 != product(sK1,sF5)
| r(sK1,sF5)
| ~ spl7_3 ),
inference(superposition,[],[f26,f340]) ).
fof(f441,plain,
( sF5 != product(sK1,sF5)
| r(sK1,sF5)
| ~ spl7_3 ),
inference(trivial_inequality_removal,[],[f438]) ).
fof(f442,plain,
( r(sK1,sF5)
| ~ spl7_3 ),
inference(forward_subsumption_resolution,[],[f441,f269]) ).
fof(f474,plain,
! [X0,X1] :
( product(X0,X1) != product(X1,product(X0,X1))
| product(product(X1,product(X0,X1)),X0) != X0
| r(product(X1,product(X0,X1)),X0) ),
inference(superposition,[],[f26,f66]) ).
fof(f493,plain,
! [X0,X1] :
( product(X1,product(product(X0,X1),X0)) != X0
| product(X0,X1) != product(X1,product(X0,X1))
| r(product(X1,product(X0,X1)),X0) ),
inference(forward_demodulation,[],[f474,f19]) ).
fof(f517,plain,
! [X0,X1] :
( product(X1,product(X0,product(X1,X0))) != X0
| product(X0,X1) != product(X1,product(X0,X1))
| r(product(X1,product(X0,X1)),X0) ),
inference(forward_demodulation,[],[f493,f19]) ).
fof(f528,plain,
! [X0,X1] :
( product(X0,X1) != product(X1,product(X0,X1))
| product(X1,X0) != X0
| r(product(X1,product(X0,X1)),X0) ),
inference(forward_demodulation,[],[f517,f66]) ).
fof(f530,plain,
( ! [X0] :
( ~ l(sF5,X0)
| d(sK1,X0) )
| ~ spl7_3 ),
inference(resolution,[],[f442,f29]) ).
fof(f540,plain,
! [X0,X1] :
( product(X1,sK1) != product(X1,product(sF5,X0))
| product(sK2,X0) != product(product(sK2,X0),product(X1,sK1))
| l(product(sK2,X0),product(X1,sK1)) ),
inference(superposition,[],[f75,f62]) ).
fof(f542,plain,
! [X0] :
( sF5 != product(sF5,product(X0,sK2))
| product(X0,sK2) != product(X0,sF6)
| l(sF5,product(X0,sK2)) ),
inference(superposition,[],[f75,f40]) ).
fof(f569,plain,
! [X0,X1] :
( product(sK2,X0) != product(sK2,product(X0,product(X1,sK1)))
| product(X1,sK1) != product(X1,product(sF5,X0))
| l(product(sK2,X0),product(X1,sK1)) ),
inference(forward_demodulation,[],[f540,f19]) ).
fof(f598,plain,
( sK1 = sF4
| ~ spl7_10 ),
inference(superposition,[],[f377,f36]) ).
fof(f861,plain,
( d(sK1,sK2)
| ~ spl7_3
| ~ spl7_4 ),
inference(resolution,[],[f91,f530]) ).
fof(f863,plain,
( sK2 = product(sK2,sF5)
| ~ spl7_4 ),
inference(resolution,[],[f91,f21]) ).
fof(f1090,plain,
( $false
| spl7_1
| ~ spl7_3
| ~ spl7_4 ),
inference(forward_subsumption_resolution,[],[f861,f46]) ).
fof(f1091,plain,
( spl7_1
| ~ spl7_3
| ~ spl7_4 ),
inference(avatar_contradiction_clause,[],[f1090]) ).
fof(f1112,plain,
( $false
| spl7_3
| ~ spl7_10 ),
inference(forward_subsumption_resolution,[],[f598,f55]) ).
fof(f1113,plain,
( spl7_3
| ~ spl7_10 ),
inference(avatar_contradiction_clause,[],[f1112]) ).
fof(f1134,plain,
( r(sK1,sK0(sK1,sK2))
| ~ spl7_1 ),
inference(resolution,[],[f47,f28]) ).
fof(f1135,plain,
( l(sK0(sK1,sK2),sK2)
| ~ spl7_1 ),
inference(resolution,[],[f47,f27]) ).
fof(f1139,plain,
( sK0(sK1,sK2) = product(sK1,sK0(sK1,sK2))
| ~ spl7_1 ),
inference(resolution,[],[f1134,f25]) ).
fof(f1140,plain,
( sK1 = product(sK0(sK1,sK2),sK1)
| ~ spl7_1 ),
inference(resolution,[],[f1134,f24]) ).
fof(f1143,plain,
( sK0(sK1,sK2) = product(sK0(sK1,sK2),sK2)
| ~ spl7_1 ),
inference(resolution,[],[f1135,f22]) ).
fof(f1144,plain,
( sK2 = product(sK2,sK0(sK1,sK2))
| ~ spl7_1 ),
inference(resolution,[],[f1135,f21]) ).
fof(f1153,plain,
( sK2 = product(sK2,product(sF5,sK2))
| ~ spl7_4 ),
inference(superposition,[],[f66,f863]) ).
fof(f1159,plain,
( sK2 = product(sF3,product(sK2,sK2))
| ~ spl7_4 ),
inference(forward_demodulation,[],[f1153,f351]) ).
fof(f1161,plain,
( sK2 = product(sF3,sK2)
| ~ spl7_4 ),
inference(forward_demodulation,[],[f1159,f20]) ).
fof(f1220,plain,
( ! [X0] : product(sK1,X0) = product(sK0(sK1,sK2),product(sK1,X0))
| ~ spl7_1 ),
inference(superposition,[],[f19,f1140]) ).
fof(f1239,plain,
( product(sK1,sK2) = product(sF5,sK0(sK1,sK2))
| ~ spl7_1 ),
inference(superposition,[],[f62,f1144]) ).
fof(f1240,plain,
( ! [X0] : product(sK2,X0) = product(sK2,product(sK0(sK1,sK2),X0))
| ~ spl7_1 ),
inference(superposition,[],[f19,f1144]) ).
fof(f1250,plain,
( sF5 = product(sF5,sK0(sK1,sK2))
| ~ spl7_1 ),
inference(forward_demodulation,[],[f1239,f38]) ).
fof(f1298,plain,
( product(sK2,sK0(sK1,sK2)) = product(sF3,sK0(sK1,sK2))
| ~ spl7_1 ),
inference(superposition,[],[f63,f1139]) ).
fof(f1299,plain,
( ! [X0] : product(sK0(sK1,sK2),X0) = product(sK1,product(sK0(sK1,sK2),X0))
| ~ spl7_1 ),
inference(superposition,[],[f19,f1139]) ).
fof(f1309,plain,
( sK2 = product(sF3,sK0(sK1,sK2))
| ~ spl7_1 ),
inference(forward_demodulation,[],[f1298,f1144]) ).
fof(f1448,plain,
( sK2 = sF6
| ~ spl7_4 ),
inference(superposition,[],[f366,f1161]) ).
fof(f3699,definition,
( spl7_38
<=> sF5 = sK0(sK1,sK2) ),
introduced(definition,[new_symbols(definition,[spl7_38])],[avatar_definition]) ).
fof(f3700,plain,
( sF5 = sK0(sK1,sK2)
| ~ spl7_38 ),
inference(avatar_component_clause,[],[f3699]) ).
fof(f3701,plain,
( sF5 != sK0(sK1,sK2)
| spl7_38 ),
inference(avatar_component_clause,[],[f3699]) ).
fof(f4811,definition,
( spl7_42
<=> sK0(sK1,sK2) = product(sK0(sK1,sK2),sF5) ),
introduced(definition,[new_symbols(definition,[spl7_42])],[avatar_definition]) ).
fof(f4812,plain,
( sK0(sK1,sK2) = product(sK0(sK1,sK2),sF5)
| ~ spl7_42 ),
inference(avatar_component_clause,[],[f4811]) ).
fof(f4813,plain,
( sK0(sK1,sK2) != product(sK0(sK1,sK2),sF5)
| spl7_42 ),
inference(avatar_component_clause,[],[f4811]) ).
fof(f4831,definition,
( spl7_46
<=> r(sK0(sK1,sK2),sF5) ),
introduced(definition,[new_symbols(definition,[spl7_46])],[avatar_definition]) ).
fof(f4833,plain,
( r(sK0(sK1,sK2),sF5)
| ~ spl7_46 ),
inference(avatar_component_clause,[],[f4831]) ).
fof(f4835,definition,
( spl7_47
<=> sF5 = product(sK0(sK1,sK2),sF5) ),
introduced(definition,[new_symbols(definition,[spl7_47])],[avatar_definition]) ).
fof(f4836,plain,
( sF5 = product(sK0(sK1,sK2),sF5)
| ~ spl7_47 ),
inference(avatar_component_clause,[],[f4835]) ).
fof(f4837,plain,
( sF5 != product(sK0(sK1,sK2),sF5)
| spl7_47 ),
inference(avatar_component_clause,[],[f4835]) ).
fof(f4852,plain,
( product(sK1,sK2) != product(sF5,sK2)
| sK2 != product(sF3,sK2)
| l(product(sK1,sK2),sK2) ),
inference(superposition,[],[f360,f62]) ).
fof(f4907,plain,
( sK2 = product(sF3,sK2)
| ~ spl7_1 ),
inference(superposition,[],[f59,f1309]) ).
fof(f5252,plain,
( sF5 != product(sF5,sK0(sK1,sK2))
| sK0(sK1,sK2) != product(sK0(sK1,sK2),sF6)
| l(sF5,sK0(sK1,sK2))
| ~ spl7_1 ),
inference(superposition,[],[f542,f1143]) ).
fof(f5266,plain,
( sK0(sK1,sK2) != product(sK0(sK1,sK2),sF6)
| l(sF5,sK0(sK1,sK2))
| ~ spl7_1 ),
inference(forward_subsumption_resolution,[],[f5252,f1250]) ).
fof(f5274,plain,
( sK0(sK1,sK2) != product(sK0(sK1,sK2),sK2)
| l(sF5,sK0(sK1,sK2))
| ~ spl7_1
| ~ spl7_2 ),
inference(forward_demodulation,[],[f5266,f51]) ).
fof(f5282,plain,
( l(sF5,sK0(sK1,sK2))
| ~ spl7_1
| ~ spl7_2 ),
inference(forward_subsumption_resolution,[],[f5274,f1143]) ).
fof(f5312,plain,
( sK0(sK1,sK2) = product(sK0(sK1,sK2),sF5)
| ~ spl7_1
| ~ spl7_2 ),
inference(resolution,[],[f5282,f21]) ).
fof(f5313,plain,
( $false
| ~ spl7_1
| ~ spl7_2
| spl7_42 ),
inference(forward_subsumption_resolution,[],[f5312,f4813]) ).
fof(f5314,plain,
( ~ spl7_1
| ~ spl7_2
| spl7_42 ),
inference(avatar_contradiction_clause,[],[f5313]) ).
fof(f5709,plain,
( sF5 != product(sK0(sK1,sK2),sF5)
| sF5 != product(sK0(sK1,sK2),sF5)
| r(product(sK0(sK1,sK2),sF5),sF5)
| ~ spl7_1 ),
inference(superposition,[],[f528,f1250]) ).
fof(f5731,plain,
( sF5 != product(sK0(sK1,sK2),sF5)
| r(product(sK0(sK1,sK2),sF5),sF5)
| ~ spl7_1 ),
inference(duplicate_literal_removal,[],[f5709]) ).
fof(f11602,plain,
( ! [X0] : product(sF5,X0) = product(sK0(sK1,sK2),product(sF5,X0))
| ~ spl7_1 ),
inference(superposition,[],[f1220,f326]) ).
fof(f11605,plain,
( sF5 = product(sK0(sK1,sK2),sF5)
| ~ spl7_1 ),
inference(superposition,[],[f1220,f38]) ).
fof(f11736,plain,
( $false
| ~ spl7_1
| spl7_47 ),
inference(forward_subsumption_resolution,[],[f11605,f4837]) ).
fof(f11737,plain,
( ~ spl7_1
| spl7_47 ),
inference(avatar_contradiction_clause,[],[f11736]) ).
fof(f11811,plain,
( r(product(sK0(sK1,sK2),sF5),sF5)
| ~ spl7_1
| ~ spl7_47 ),
inference(forward_subsumption_resolution,[],[f5731,f4836]) ).
fof(f11813,plain,
( r(sK0(sK1,sK2),sF5)
| ~ spl7_1
| ~ spl7_42
| ~ spl7_47 ),
inference(forward_demodulation,[],[f11811,f4812]) ).
fof(f11815,plain,
( spl7_46
| ~ spl7_1
| ~ spl7_42
| ~ spl7_47 ),
inference(avatar_split_clause,[],[f11813,f4835,f4811,f45,f4831]) ).
fof(f11948,plain,
( sK0(sK1,sK2) = product(sF5,sK0(sK1,sK2))
| ~ spl7_46 ),
inference(resolution,[],[f4833,f24]) ).
fof(f11949,plain,
( sF5 = sK0(sK1,sK2)
| ~ spl7_1
| ~ spl7_46 ),
inference(forward_demodulation,[],[f11948,f1250]) ).
fof(f11950,plain,
( $false
| ~ spl7_1
| spl7_38
| ~ spl7_46 ),
inference(forward_subsumption_resolution,[],[f11949,f3701]) ).
fof(f11951,plain,
( ~ spl7_1
| spl7_38
| ~ spl7_46 ),
inference(avatar_contradiction_clause,[],[f11950]) ).
fof(f11980,plain,
( sK1 = product(sF5,sK1)
| ~ spl7_1
| ~ spl7_38 ),
inference(superposition,[],[f1140,f3700]) ).
fof(f12795,plain,
( product(sK2,sK1) != product(sK2,product(sK0(sK1,sK2),sK1))
| product(sK0(sK1,sK2),sK1) != product(sK0(sK1,sK2),product(sF5,sK1))
| l(product(sK2,sK1),product(sK0(sK1,sK2),sK1))
| ~ spl7_1 ),
inference(superposition,[],[f569,f1299]) ).
fof(f12850,plain,
( product(sK0(sK1,sK2),sK1) != product(sK0(sK1,sK2),product(sF5,sK1))
| l(product(sK2,sK1),product(sK0(sK1,sK2),sK1))
| ~ spl7_1 ),
inference(forward_subsumption_resolution,[],[f12795,f1240]) ).
fof(f12911,plain,
( product(sF5,sK1) != product(sK0(sK1,sK2),sK1)
| l(product(sK2,sK1),product(sK0(sK1,sK2),sK1))
| ~ spl7_1 ),
inference(forward_demodulation,[],[f12850,f11602]) ).
fof(f12963,plain,
( sK1 != product(sF5,sK1)
| l(product(sK2,sK1),product(sK0(sK1,sK2),sK1))
| ~ spl7_1 ),
inference(forward_demodulation,[],[f12911,f1140]) ).
fof(f13002,plain,
( l(product(sK2,sK1),product(sK0(sK1,sK2),sK1))
| ~ spl7_1
| ~ spl7_38 ),
inference(forward_subsumption_resolution,[],[f12963,f11980]) ).
fof(f13031,plain,
( l(product(sK2,sK1),sK1)
| ~ spl7_1
| ~ spl7_38 ),
inference(forward_demodulation,[],[f13002,f1140]) ).
fof(f13051,plain,
( l(sF3,sK1)
| ~ spl7_1
| ~ spl7_38 ),
inference(forward_demodulation,[],[f13031,f34]) ).
fof(f13063,plain,
( $false
| ~ spl7_1
| spl7_10
| ~ spl7_38 ),
inference(forward_subsumption_resolution,[],[f13051,f117]) ).
fof(f13064,plain,
( ~ spl7_1
| spl7_10
| ~ spl7_38 ),
inference(avatar_contradiction_clause,[],[f13063]) ).
fof(f13166,plain,
( $false
| spl7_2
| ~ spl7_4 ),
inference(forward_subsumption_resolution,[],[f1448,f50]) ).
fof(f13167,plain,
( spl7_2
| ~ spl7_4 ),
inference(avatar_contradiction_clause,[],[f13166]) ).
fof(f14724,plain,
( product(sK1,sK2) != sF5
| sK2 != product(sF3,sK2)
| l(product(sK1,sK2),sK2)
| ~ spl7_5 ),
inference(forward_demodulation,[],[f4852,f94]) ).
fof(f15102,plain,
( sK2 != product(sF3,sK2)
| l(product(sK1,sK2),sK2)
| ~ spl7_5 ),
inference(forward_subsumption_resolution,[],[f14724,f38]) ).
fof(f15387,plain,
( l(product(sK1,sK2),sK2)
| ~ spl7_1
| ~ spl7_5 ),
inference(forward_subsumption_resolution,[],[f15102,f4907]) ).
fof(f15614,plain,
( l(sF5,sK2)
| ~ spl7_1
| ~ spl7_5 ),
inference(forward_demodulation,[],[f15387,f38]) ).
fof(f15768,plain,
( $false
| ~ spl7_1
| spl7_4
| ~ spl7_5 ),
inference(forward_subsumption_resolution,[],[f15614,f90]) ).
fof(f15769,plain,
( ~ spl7_1
| spl7_4
| ~ spl7_5 ),
inference(avatar_contradiction_clause,[],[f15768]) ).
cnf(s1,plain,
( spl7_1
| spl7_2 ),
inference(sat_conversion,[],[f52]) ).
cnf(s2,plain,
( spl7_1
| spl7_3 ),
inference(sat_conversion,[],[f57]) ).
cnf(s3,plain,
( ~ spl7_1
| ~ spl7_2
| ~ spl7_3 ),
inference(sat_conversion,[],[f58]) ).
cnf(s4,plain,
( ~ spl7_2
| spl7_4
| ~ spl7_5 ),
inference(sat_conversion,[],[f96]) ).
cnf(s16,plain,
spl7_5,
inference(sat_conversion,[],[f339]) ).
cnf(s25,plain,
( spl7_1
| ~ spl7_3
| ~ spl7_4 ),
inference(sat_conversion,[],[f1091]) ).
cnf(s27,plain,
( spl7_3
| ~ spl7_10 ),
inference(sat_conversion,[],[f1113]) ).
cnf(s41,plain,
( ~ spl7_1
| ~ spl7_2
| spl7_42 ),
inference(sat_conversion,[],[f5314]) ).
cnf(s56,plain,
( ~ spl7_1
| spl7_47 ),
inference(sat_conversion,[],[f11737]) ).
cnf(s57,plain,
( ~ spl7_1
| ~ spl7_42
| spl7_46
| ~ spl7_47 ),
inference(sat_conversion,[],[f11815]) ).
cnf(s58,plain,
( ~ spl7_1
| spl7_38
| ~ spl7_46 ),
inference(sat_conversion,[],[f11951]) ).
cnf(s59,plain,
( ~ spl7_1
| spl7_10
| ~ spl7_38 ),
inference(sat_conversion,[],[f13064]) ).
cnf(s64,plain,
( spl7_2
| ~ spl7_4 ),
inference(sat_conversion,[],[f13167]) ).
cnf(s87,plain,
( ~ spl7_1
| spl7_4
| ~ spl7_5 ),
inference(sat_conversion,[],[f15769]) ).
cnf(s89,plain,
( ~ spl7_2
| spl7_4 ),
inference(rat,[],[s4,s16]) ).
cnf(s90,plain,
spl7_1,
inference(rat,[],[s89,s25,s1,s2]) ).
cnf(s91,plain,
spl7_4,
inference(rat,[],[s87,s16,s90]) ).
cnf(s92,plain,
spl7_47,
inference(rat,[],[s56,s90]) ).
cnf(s95,plain,
spl7_2,
inference(rat,[],[s64,s91]) ).
cnf(s99,plain,
~ spl7_3,
inference(rat,[],[s3,s90,s95]) ).
cnf(s100,plain,
spl7_42,
inference(rat,[],[s41,s90,s95]) ).
cnf(s102,plain,
~ spl7_10,
inference(rat,[],[s27,s99]) ).
cnf(s103,plain,
spl7_46,
inference(rat,[],[s57,s92,s90,s100]) ).
cnf(s107,plain,
~ spl7_38,
inference(rat,[],[s59,s90,s102]) ).
cnf(s108,plain,
$false,
inference(rat,[],[s58,s90,s103,s107]) ).
fof(f16335,plain,
$false,
inference(avatar_sat_refutation,[],[s108]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : GRP775+1 : TPTP v9.3.1. Released v4.1.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.39 % Computer : n001.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Sun Sep 27 10:49:45 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.12/0.42 Running first-order model finding
% 0.12/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.33/1.06 % (3376086)Will run a generic schedule for satisfiability detection.
% 4.33/1.06 % (3376094)dis+10_1_sil=32000:sp=arity:random_seed=2074159103:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 4.33/1.06 % (3376092)% WARNING: option uhcvi not known.
% 4.33/1.06 % (3376092)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1573943601:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 4.33/1.06 % (3376091)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=954836387_2999 on theBenchmark for (2999ds/0Mi)
% 4.33/1.06 % (3376093)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=3426153314:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 4.33/1.06 % (3376095)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=147525236:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 4.33/1.06 % (3376096)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1927825600:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 4.33/1.06 % (3376097)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2505163125:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 4.33/1.06 % TRYING [1]
% 4.33/1.06 % TRYING [2]
% 4.33/1.06 % TRYING [3]
% 4.33/1.06 % TRYING [4]
% 4.33/1.06 % TRYING [5]
% 4.33/1.06 % TRYING [6]
% 4.33/1.06 % (3376094)Instruction limit reached!
% 4.33/1.06 % (3376094)------------------------------
% 4.33/1.06 % (3376094)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.33/1.06 % (3376094)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/1.06 % (3376094)CaDiCaL version: 2.1.3
% 4.33/1.06 % (3376094)Termination reason: Instruction limit
% 4.33/1.06 % (3376094)Termination phase: Saturation
% 4.33/1.06 % (3376094)Time elapsed: 0.033 s
% 4.33/1.06 % (3376094)Peak memory usage: 12 MB
% 4.33/1.06 % (3376094)Instructions burned: 105 (million)
% 4.33/1.06 % (3376105)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3778500836:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 4.33/1.06 % TRYING [1]
% 4.33/1.06 % TRYING [2]
% 4.33/1.06 % TRYING [3]
% 4.33/1.06 % TRYING [4]
% 4.33/1.06 % TRYING [5]
% 4.33/1.06 % TRYING [7]
% 4.33/1.06 % TRYING [6]
% 4.33/1.06 % (3376095)Instruction limit reached!
% 4.33/1.06 % (3376095)------------------------------
% 4.33/1.06 % (3376095)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.33/1.06 % (3376095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/1.06 % (3376095)CaDiCaL version: 2.1.3
% 4.33/1.06 % (3376095)Termination reason: Instruction limit
% 4.33/1.06 % (3376095)Termination phase: Saturation
% 4.33/1.06 % (3376095)Time elapsed: 0.066 s
% 4.33/1.06 % (3376095)Peak memory usage: 13 MB
% 4.33/1.06 % (3376095)Instructions burned: 116 (million)
% 4.33/1.06 % TRYING [7]
% 4.33/1.06 % (3376096)Instruction limit reached!
% 4.33/1.06 % (3376096)------------------------------
% 4.33/1.06 % (3376096)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.33/1.06 % (3376096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/1.06 % (3376096)CaDiCaL version: 2.1.3
% 4.33/1.06 % (3376096)Termination reason: Instruction limit
% 4.33/1.06 % (3376096)Termination phase: Saturation
% 4.33/1.06 % (3376096)Time elapsed: 0.076 s
% 4.33/1.06 % (3376096)Peak memory usage: 12 MB
% 4.33/1.06 % (3376096)Instructions burned: 131 (million)
% 4.33/1.06 % (3376107)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2158699757:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 4.33/1.06 % (3376108)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=3485030117:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 4.33/1.06 % TRYING [8]
% 4.33/1.06 % TRYING [8]
% 4.33/1.06 % (3376097)Instruction limit reached!
% 4.33/1.06 % (3376097)------------------------------
% 4.33/1.06 % (3376097)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.33/1.06 % (3376097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/1.06 % (3376097)CaDiCaL version: 2.1.3
% 4.33/1.06 % (3376097)Termination reason: Instruction limit
% 4.33/1.06 % (3376097)Termination phase: Saturation
% 4.33/1.06 % (3376097)Time elapsed: 0.108 s
% 4.33/1.06 % (3376097)Peak memory usage: 13 MB
% 4.33/1.06 % (3376097)Instructions burned: 160 (million)
% 4.33/1.06 % (3376111)ott-21_1_sil=16000:fs=off:random_seed=3253520675:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 4.33/1.06 % TRYING [9]
% 4.33/1.06 % (3376107)Instruction limit reached!
% 4.33/1.06 % (3376107)------------------------------
% 4.33/1.06 % (3376107)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.33/1.06 % (3376107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/1.06 % (3376107)CaDiCaL version: 2.1.3
% 4.33/1.06 % (3376107)Termination reason: Instruction limit
% 4.33/1.06 % (3376107)Termination phase: Saturation
% 4.33/1.06 % (3376107)Time elapsed: 0.079 s
% 4.33/1.06 % (3376107)Peak memory usage: 12 MB
% 4.33/1.06 % (3376107)Instructions burned: 132 (million)
% 4.33/1.06 % (3376105)Instruction limit reached!
% 4.33/1.06 % (3376105)------------------------------
% 4.33/1.06 % (3376105)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.33/1.06 % (3376105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/1.06 % (3376105)CaDiCaL version: 2.1.3
% 4.33/1.06 % (3376105)Termination reason: Instruction limit
% 4.33/1.06 % (3376105)Termination phase: Finite model building constraint generation
% 4.33/1.06 % (3376105)Time elapsed: 0.147 s
% 4.33/1.06 % (3376105)Peak memory usage: 25 MB
% 4.33/1.06 % (3376105)Instructions burned: 715 (million)
% 4.33/1.06 % TRYING [9]
% 4.33/1.06 % (3376113)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=1019191834:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 4.33/1.06 % (3376114)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=4198782821:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 4.33/1.06 % TRYING [1]
% 4.33/1.06 % TRYING [2]
% 4.33/1.06 % TRYING [3]
% 4.33/1.06 % TRYING [4]
% 4.33/1.06 % (3376111)Instruction limit reached!
% 4.33/1.06 % (3376111)------------------------------
% 4.33/1.06 % (3376111)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.33/1.06 % (3376111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/1.06 % (3376111)CaDiCaL version: 2.1.3
% 4.33/1.06 % (3376111)Termination reason: Instruction limit
% 4.33/1.06 % (3376111)Termination phase: Saturation
% 4.33/1.06 % (3376111)Time elapsed: 0.073 s
% 4.33/1.06 % (3376111)Peak memory usage: 12 MB
% 4.33/1.06 % (3376111)Instructions burned: 182 (million)
% 4.33/1.06 % TRYING [5]
% 4.33/1.06 % TRYING [6]
% 4.33/1.06 % (3376117)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=2700348063:i=1179_2997 on theBenchmark for (2997ds/1179Mi)
% 4.33/1.06 % TRYING [7]
% 4.33/1.06 % TRYING [8]
% 4.33/1.06 % TRYING [10]
% 4.33/1.06 % (3376114)Instruction limit reached!
% 4.33/1.06 % (3376114)------------------------------
% 4.33/1.06 % (3376114)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.33/1.06 % (3376114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/1.06 % (3376114)CaDiCaL version: 2.1.3
% 4.33/1.06 % (3376114)Termination reason: Instruction limit
% 4.33/1.06 % (3376114)Termination phase: Finite model building SAT solving
% 4.33/1.06 % (3376114)Time elapsed: 0.170 s
% 4.33/1.06 % (3376114)Peak memory usage: 21 MB
% 4.33/1.06 % (3376114)Instructions burned: 869 (million)
% 4.33/1.06 % (3376119)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3679895604:i=889:ins=1_2996 on theBenchmark for (2996ds/889Mi)
% 4.33/1.06 % TRYING [14]
% 4.33/1.06 % (3376108)Instruction limit reached!
% 4.33/1.06 % (3376108)------------------------------
% 4.33/1.06 % (3376108)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.33/1.06 % (3376108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/1.06 % (3376108)CaDiCaL version: 2.1.3
% 4.33/1.06 % (3376108)Termination reason: Instruction limit
% 4.33/1.06 % (3376108)Termination phase: Saturation
% 4.33/1.06 % (3376108)Time elapsed: 0.362 s
% 4.33/1.06 % (3376108)Peak memory usage: 18 MB
% 4.33/1.06 % (3376108)Instructions burned: 685 (million)
% 4.33/1.06 % (3376121)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=1219075337:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2995 on theBenchmark for (2995ds/692Mi)
% 4.33/1.06 % (3376113)Instruction limit reached!
% 4.33/1.06 % (3376113)------------------------------
% 4.33/1.06 % (3376113)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.33/1.06 % (3376113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/1.06 % (3376113)CaDiCaL version: 2.1.3
% 4.33/1.06 % (3376113)Termination reason: Instruction limit
% 4.33/1.06 % (3376113)Termination phase: Saturation
% 4.33/1.06 % (3376113)Time elapsed: 0.303 s
% 4.33/1.06 % (3376113)Peak memory usage: 16 MB
% 4.33/1.06 % (3376113)Instructions burned: 477 (million)
% 4.33/1.06 % (3376123)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=4603522:i=879:kws=inv_precedence:fsr=off_2994 on theBenchmark for (2994ds/879Mi)
% 4.33/1.06 % (3376119)Instruction limit reached!
% 4.33/1.06 % (3376119)------------------------------
% 4.33/1.06 % (3376119)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.33/1.06 % (3376119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/1.06 % (3376119)CaDiCaL version: 2.1.3
% 4.33/1.06 % (3376119)Termination reason: Instruction limit
% 4.33/1.06 % (3376119)Termination phase: Finite model building constraint generation
% 4.33/1.06 % (3376119)Time elapsed: 0.179 s
% 4.33/1.06 % (3376119)Peak memory usage: 79 MB
% 4.33/1.06 % (3376119)Instructions burned: 893 (million)
% 4.33/1.06 % (3376125)fmb+10_1_sil=64000:random_seed=2180970618:i=22061:nm=2:gsp=on_2994 on theBenchmark for (2994ds/22061Mi)
% 4.33/1.06 % TRYING [1]
% 4.33/1.06 % TRYING [2]
% 4.33/1.06 % TRYING [3]
% 4.33/1.06 % TRYING [4]
% 4.33/1.06 % TRYING [5]
% 4.33/1.06 % (3376117) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3376086-3376117"...
% 4.33/1.06 % (3376117)...printing done.
% 4.33/1.06 % (3376117)Refutation found. Thanks to Tanya!
% 4.33/1.06 % SZS status Theorem for theBenchmark
% 4.33/1.06 % SZS output start Proof for theBenchmark
% See solution above
% 4.33/1.06 % (3376117)------------------------------
% 4.33/1.06 % (3376117)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 4.33/1.06 % (3376117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.33/1.06 % (3376117)CaDiCaL version: 2.1.3
% 4.33/1.06 % (3376117)Termination reason: Refutation
% 4.33/1.06 % (3376117)Time elapsed: 0.367 s
% 4.33/1.06 % (3376117)Peak memory usage: 16 MB
% 4.33/1.06 % (3376117)Instructions burned: 645 (million)
% 4.33/1.06 % (3376086)Success in time 0.63 s
% 4.33/1.06 % Vampire exiting
%------------------------------------------------------------------------------