%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : SET615+3 : TPTP v9.3.1. Released v2.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n018.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 12:44:10 PM UTC 2026
% Result : Theorem 2.28s 1.01s
% Output : Refutation 2.28s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 13
% Syntax : Number of formulae : 111 ( 22 unt; 9 def)
% Number of atoms : 291 ( 38 equ)
% Maximal formula atoms : 10 ( 2 avg)
% Number of connectives : 296 ( 116 ~; 154 |; 18 &)
% ( 8 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 4 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 7 ( 5 usr; 5 prp; 0-2 aty)
% Number of functors : 11 ( 11 usr; 8 con; 0-2 aty)
% Number of variables : 86 ( 0 sgn 81 !; 5 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1,X2] :
( member(X2,union(X0,X1))
<=> ( member(X2,X0)
| member(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',union_defn) ).
fof(f2,axiom,
! [X0,X1,X2] :
( member(X2,difference(X0,X1))
<=> ( member(X2,X0)
& ~ member(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',difference_defn) ).
fof(f7,axiom,
! [X0,X1] :
( X0 = X1
<=> ! [X2] :
( member(X2,X0)
<=> member(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',equal_member_defn) ).
fof(f8,conjecture,
! [X0,X1,X2] : difference(union(X0,X1),X2) = union(difference(X0,X2),difference(X1,X2)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',prove_difference_distributes_over_union) ).
fof(f9,negated_conjecture,
~ ! [X0,X1,X2] : difference(union(X0,X1),X2) = union(difference(X0,X2),difference(X1,X2)),
inference(negated_conjecture,[status(cth)],[f8]) ).
fof(f11,plain,
? [X0,X1,X2] : difference(union(X0,X1),X2) != union(difference(X0,X2),difference(X1,X2)),
inference(ennf_transformation,[],[f9]) ).
fof(f12,plain,
! [X0,X1,X2] :
( ( member(X2,union(X0,X1))
| ( ~ member(X2,X0)
& ~ member(X2,X1) ) )
& ( member(X2,X0)
| member(X2,X1)
| ~ member(X2,union(X0,X1)) ) ),
inference(nnf_transformation,[],[f1]) ).
fof(f13,plain,
! [X0,X1,X2] :
( ( member(X2,union(X0,X1))
| ( ~ member(X2,X0)
& ~ member(X2,X1) ) )
& ( member(X2,X0)
| member(X2,X1)
| ~ member(X2,union(X0,X1)) ) ),
inference(flattening,[],[f12]) ).
fof(f14,plain,
! [X0,X1,X2] :
( ( member(X2,difference(X0,X1))
| ~ member(X2,X0)
| member(X2,X1) )
& ( ( member(X2,X0)
& ~ member(X2,X1) )
| ~ member(X2,difference(X0,X1)) ) ),
inference(nnf_transformation,[],[f2]) ).
fof(f15,plain,
! [X0,X1,X2] :
( ( member(X2,difference(X0,X1))
| ~ member(X2,X0)
| member(X2,X1) )
& ( ( member(X2,X0)
& ~ member(X2,X1) )
| ~ member(X2,difference(X0,X1)) ) ),
inference(flattening,[],[f14]) ).
fof(f21,plain,
! [X0,X1] :
( ( X0 = X1
| ? [X2] :
( ( ~ member(X2,X1)
| ~ member(X2,X0) )
& ( member(X2,X1)
| member(X2,X0) ) ) )
& ( ! [X2] :
( ( member(X2,X0)
| ~ member(X2,X1) )
& ( member(X2,X1)
| ~ member(X2,X0) ) )
| X0 != X1 ) ),
inference(nnf_transformation,[],[f7]) ).
fof(f22,plain,
! [X0,X1] :
( ( X0 = X1
| ? [X2] :
( ( ~ member(X2,X1)
| ~ member(X2,X0) )
& ( member(X2,X1)
| member(X2,X0) ) ) )
& ( ! [X3] :
( ( member(X3,X0)
| ~ member(X3,X1) )
& ( member(X3,X1)
| ~ member(X3,X0) ) )
| X0 != X1 ) ),
inference(rectify,[],[f21]) ).
fof(f23,plain,
! [X0,X1] :
( ( X0 = X1
| ( ( ~ member(sK1(X0,X1),X1)
| ~ member(sK1(X0,X1),X0) )
& ( member(sK1(X0,X1),X1)
| member(sK1(X0,X1),X0) ) ) )
& ( ! [X3] :
( ( member(X3,X0)
| ~ member(X3,X1) )
& ( member(X3,X1)
| ~ member(X3,X0) ) )
| X0 != X1 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X2,sK1(X0,X1))],[f22]) ).
fof(f24,plain,
difference(union(sK2,sK3),sK4) != union(difference(sK2,sK4),difference(sK3,sK4)),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2,sK3,sK4]),skolemize(X0,sK2),skolemize(X1,sK3),skolemize(X2,sK4)],[f11]) ).
fof(f25,plain,
! [X2,X0,X1] :
( ~ member(X2,union(X0,X1))
| member(X2,X1)
| member(X2,X0) ),
inference(cnf_transformation,[],[f13]) ).
fof(f26,plain,
! [X2,X0,X1] :
( member(X2,union(X0,X1))
| ~ member(X2,X1) ),
inference(cnf_transformation,[],[f13]) ).
fof(f27,plain,
! [X2,X0,X1] :
( member(X2,union(X0,X1))
| ~ member(X2,X0) ),
inference(cnf_transformation,[],[f13]) ).
fof(f28,plain,
! [X2,X0,X1] :
( ~ member(X2,difference(X0,X1))
| ~ member(X2,X1) ),
inference(cnf_transformation,[],[f15]) ).
fof(f29,plain,
! [X2,X0,X1] :
( ~ member(X2,difference(X0,X1))
| member(X2,X0) ),
inference(cnf_transformation,[],[f15]) ).
fof(f30,plain,
! [X2,X0,X1] :
( member(X2,difference(X0,X1))
| ~ member(X2,X0)
| member(X2,X1) ),
inference(cnf_transformation,[],[f15]) ).
fof(f41,plain,
! [X0,X1] :
( member(sK1(X0,X1),X1)
| member(sK1(X0,X1),X0)
| X0 = X1 ),
inference(cnf_transformation,[],[f23]) ).
fof(f42,plain,
! [X0,X1] :
( ~ member(sK1(X0,X1),X1)
| X0 = X1
| ~ member(sK1(X0,X1),X0) ),
inference(cnf_transformation,[],[f23]) ).
fof(f43,plain,
difference(union(sK2,sK3),sK4) != union(difference(sK2,sK4),difference(sK3,sK4)),
inference(cnf_transformation,[],[f24]) ).
fof(f48,definition,
sF5 = union(sK2,sK3),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
fof(f49,plain,
union(sK2,sK3) = sF5,
inference(reorient_equations,[],[f48]) ).
fof(f50,definition,
sF6 = difference(sF5,sK4),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
fof(f51,plain,
difference(sF5,sK4) = sF6,
inference(reorient_equations,[],[f50]) ).
fof(f52,definition,
sF7 = difference(sK2,sK4),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
fof(f53,plain,
difference(sK2,sK4) = sF7,
inference(reorient_equations,[],[f52]) ).
fof(f54,definition,
sF8 = difference(sK3,sK4),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
fof(f55,plain,
difference(sK3,sK4) = sF8,
inference(reorient_equations,[],[f54]) ).
fof(f56,definition,
sF9 = union(sF7,sF8),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
fof(f57,plain,
union(sF7,sF8) = sF9,
inference(reorient_equations,[],[f56]) ).
fof(f58,plain,
sF6 != sF9,
inference(definition_folding,[],[f43,f57,f55,f53,f51,f49]) ).
fof(f59,plain,
! [X0] :
( ~ member(X0,sK3)
| member(X0,sF5) ),
inference(superposition,[],[f26,f49]) ).
fof(f63,plain,
! [X0] :
( ~ member(X0,sK2)
| member(X0,sF5) ),
inference(superposition,[],[f27,f49]) ).
fof(f67,plain,
! [X0] :
( ~ member(X0,sF6)
| ~ member(X0,sK4) ),
inference(superposition,[],[f28,f51]) ).
fof(f68,plain,
! [X0] :
( ~ member(X0,sF7)
| ~ member(X0,sK4) ),
inference(superposition,[],[f28,f53]) ).
fof(f69,plain,
! [X0] :
( ~ member(X0,sF8)
| ~ member(X0,sK4) ),
inference(superposition,[],[f28,f55]) ).
fof(f70,plain,
! [X0] :
( ~ member(X0,sF6)
| member(X0,sF5) ),
inference(superposition,[],[f29,f51]) ).
fof(f71,plain,
! [X0] :
( ~ member(X0,sF7)
| member(X0,sK2) ),
inference(superposition,[],[f29,f53]) ).
fof(f72,plain,
! [X0] :
( ~ member(X0,sF8)
| member(X0,sK3) ),
inference(superposition,[],[f29,f55]) ).
fof(f81,plain,
! [X0] :
( ~ member(X0,sF5)
| member(X0,sK3)
| member(X0,sK2) ),
inference(superposition,[],[f25,f49]) ).
fof(f82,plain,
! [X0] :
( ~ member(X0,sF9)
| member(X0,sF8)
| member(X0,sF7) ),
inference(superposition,[],[f25,f57]) ).
fof(f88,plain,
! [X0] :
( ~ member(X0,sF5)
| member(X0,sF6)
| member(X0,sK4) ),
inference(superposition,[],[f30,f51]) ).
fof(f89,plain,
! [X0] :
( ~ member(X0,sK2)
| member(X0,sF7)
| member(X0,sK4) ),
inference(superposition,[],[f30,f53]) ).
fof(f90,plain,
! [X0] :
( ~ member(X0,sK3)
| member(X0,sF8)
| member(X0,sK4) ),
inference(superposition,[],[f30,f55]) ).
fof(f108,plain,
! [X0] :
( member(sK1(sF6,X0),sF5)
| member(sK1(sF6,X0),X0)
| sF6 = X0 ),
inference(resolution,[],[f41,f70]) ).
fof(f119,plain,
! [X2,X0,X1] :
( ~ member(sK1(X0,union(X1,X2)),X1)
| ~ member(sK1(X0,union(X1,X2)),X0)
| union(X1,X2) = X0 ),
inference(resolution,[],[f42,f27]) ).
fof(f120,plain,
! [X2,X0,X1] :
( ~ member(sK1(X0,union(X1,X2)),X2)
| ~ member(sK1(X0,union(X1,X2)),X0)
| union(X1,X2) = X0 ),
inference(resolution,[],[f42,f26]) ).
fof(f125,plain,
! [X0] :
( member(sK1(X0,sF9),sF8)
| member(sK1(X0,sF9),X0)
| member(sK1(X0,sF9),sF7)
| sF9 = X0 ),
inference(resolution,[],[f82,f41]) ).
fof(f366,plain,
! [X0] :
( ~ member(sK1(X0,sF9),sF7)
| ~ member(sK1(X0,sF9),X0)
| sF9 = X0 ),
inference(superposition,[],[f119,f57]) ).
fof(f387,plain,
! [X0] :
( ~ member(sK1(X0,sF9),sF8)
| ~ member(sK1(X0,sF9),X0)
| sF9 = X0 ),
inference(superposition,[],[f120,f57]) ).
fof(f2171,plain,
( member(sK1(sF6,sF9),sF5)
| sF6 = sF9
| member(sK1(sF6,sF9),sF8)
| member(sK1(sF6,sF9),sF7) ),
inference(resolution,[],[f108,f82]) ).
fof(f2177,plain,
( member(sK1(sF6,sF9),sF5)
| member(sK1(sF6,sF9),sF8)
| member(sK1(sF6,sF9),sF7) ),
inference(forward_subsumption_resolution,[],[f2171,f58]) ).
fof(f3349,plain,
( member(sK1(sF6,sF9),sF8)
| member(sK1(sF6,sF9),sF7)
| sF6 = sF9
| ~ member(sK1(sF6,sF9),sK4) ),
inference(resolution,[],[f125,f67]) ).
fof(f4324,definition,
( spl10_114
<=> member(sK1(sF6,sF9),sF7) ),
introduced(definition,[new_symbols(definition,[spl10_114])],[avatar_definition]) ).
fof(f4325,plain,
( ~ member(sK1(sF6,sF9),sF7)
| spl10_114 ),
inference(avatar_component_clause,[],[f4324]) ).
fof(f4326,plain,
( member(sK1(sF6,sF9),sF7)
| ~ spl10_114 ),
inference(avatar_component_clause,[],[f4324]) ).
fof(f4328,definition,
( spl10_115
<=> member(sK1(sF6,sF9),sF5) ),
introduced(definition,[new_symbols(definition,[spl10_115])],[avatar_definition]) ).
fof(f4329,plain,
( ~ member(sK1(sF6,sF9),sF5)
| spl10_115 ),
inference(avatar_component_clause,[],[f4328]) ).
fof(f4330,plain,
( member(sK1(sF6,sF9),sF5)
| ~ spl10_115 ),
inference(avatar_component_clause,[],[f4328]) ).
fof(f7070,plain,
( ~ member(sK1(sF6,sF9),sF6)
| sF6 = sF9
| ~ spl10_114 ),
inference(resolution,[],[f4326,f366]) ).
fof(f7071,plain,
( member(sK1(sF6,sF9),sK2)
| ~ spl10_114 ),
inference(resolution,[],[f4326,f71]) ).
fof(f7080,plain,
( ~ member(sK1(sF6,sF9),sF6)
| ~ spl10_114 ),
inference(forward_subsumption_resolution,[],[f7070,f58]) ).
fof(f8159,plain,
( member(sK1(sF6,sF9),sF5)
| ~ spl10_114 ),
inference(resolution,[],[f7071,f63]) ).
fof(f8168,plain,
( $false
| ~ spl10_114
| spl10_115 ),
inference(forward_subsumption_resolution,[],[f8159,f4329]) ).
fof(f8169,plain,
( ~ spl10_114
| spl10_115 ),
inference(avatar_contradiction_clause,[],[f8168]) ).
fof(f8172,plain,
( member(sK1(sF6,sF9),sF7)
| sF6 = sF9
| ~ member(sK1(sF6,sF9),sK4) ),
inference(forward_subsumption_resolution,[],[f3349,f69]) ).
fof(f8174,plain,
( member(sK1(sF6,sF9),sF8)
| member(sK1(sF6,sF9),sF7)
| spl10_115 ),
inference(forward_subsumption_resolution,[],[f2177,f4329]) ).
fof(f8176,plain,
( sF6 = sF9
| ~ member(sK1(sF6,sF9),sK4) ),
inference(forward_subsumption_resolution,[],[f8172,f68]) ).
fof(f8179,plain,
~ member(sK1(sF6,sF9),sK4),
inference(forward_subsumption_resolution,[],[f8176,f58]) ).
fof(f9932,plain,
( member(sK1(sF6,sF9),sF8)
| spl10_114
| spl10_115 ),
inference(forward_subsumption_resolution,[],[f8174,f4325]) ).
fof(f9999,definition,
( spl10_216
<=> member(sK1(sF6,sF9),sK2) ),
introduced(definition,[new_symbols(definition,[spl10_216])],[avatar_definition]) ).
fof(f10000,plain,
( ~ member(sK1(sF6,sF9),sK2)
| spl10_216 ),
inference(avatar_component_clause,[],[f9999]) ).
fof(f10001,plain,
( member(sK1(sF6,sF9),sK2)
| ~ spl10_216 ),
inference(avatar_component_clause,[],[f9999]) ).
fof(f10008,definition,
( spl10_217
<=> member(sK1(sF6,sF9),sF6) ),
introduced(definition,[new_symbols(definition,[spl10_217])],[avatar_definition]) ).
fof(f10009,plain,
( member(sK1(sF6,sF9),sF6)
| ~ spl10_217 ),
inference(avatar_component_clause,[],[f10008]) ).
fof(f10010,plain,
( ~ member(sK1(sF6,sF9),sF6)
| spl10_217 ),
inference(avatar_component_clause,[],[f10008]) ).
fof(f10576,plain,
( member(sK1(sF6,sF9),sK3)
| spl10_114
| spl10_115 ),
inference(resolution,[],[f9932,f72]) ).
fof(f10608,plain,
( member(sK1(sF6,sF9),sF6)
| member(sK1(sF6,sF9),sK4)
| ~ spl10_115 ),
inference(resolution,[],[f4330,f88]) ).
fof(f10609,plain,
( member(sK1(sF6,sF9),sK3)
| member(sK1(sF6,sF9),sK2)
| ~ spl10_115 ),
inference(resolution,[],[f4330,f81]) ).
fof(f11422,plain,
( member(sK1(sF6,sF9),sF7)
| member(sK1(sF6,sF9),sK4)
| ~ spl10_216 ),
inference(resolution,[],[f10001,f89]) ).
fof(f11428,plain,
( member(sK1(sF6,sF9),sK4)
| spl10_114
| ~ spl10_216 ),
inference(forward_subsumption_resolution,[],[f11422,f4325]) ).
fof(f11429,plain,
( $false
| spl10_114
| ~ spl10_216 ),
inference(forward_subsumption_resolution,[],[f11428,f8179]) ).
fof(f11430,plain,
( spl10_114
| ~ spl10_216 ),
inference(avatar_contradiction_clause,[],[f11429]) ).
fof(f11431,plain,
( member(sK1(sF6,sF9),sK3)
| ~ spl10_115
| spl10_216 ),
inference(forward_subsumption_resolution,[],[f10609,f10000]) ).
fof(f11483,plain,
( member(sK1(sF6,sF9),sF8)
| member(sK1(sF6,sF9),sK4)
| ~ spl10_115
| spl10_216 ),
inference(resolution,[],[f11431,f90]) ).
fof(f11489,plain,
( member(sK1(sF6,sF9),sF8)
| ~ spl10_115
| spl10_216 ),
inference(forward_subsumption_resolution,[],[f11483,f8179]) ).
fof(f11558,plain,
( ~ member(sK1(sF6,sF9),sF6)
| sF6 = sF9
| ~ spl10_115
| spl10_216 ),
inference(resolution,[],[f11489,f387]) ).
fof(f11567,plain,
( sF6 = sF9
| ~ spl10_115
| spl10_216
| ~ spl10_217 ),
inference(forward_subsumption_resolution,[],[f11558,f10009]) ).
fof(f11568,plain,
( $false
| ~ spl10_115
| spl10_216
| ~ spl10_217 ),
inference(forward_subsumption_resolution,[],[f11567,f58]) ).
fof(f11569,plain,
( ~ spl10_115
| spl10_216
| ~ spl10_217 ),
inference(avatar_contradiction_clause,[],[f11568]) ).
fof(f11570,plain,
( member(sK1(sF6,sF9),sK4)
| ~ spl10_115
| spl10_217 ),
inference(forward_subsumption_resolution,[],[f10608,f10010]) ).
fof(f11571,plain,
( $false
| ~ spl10_115
| spl10_217 ),
inference(forward_subsumption_resolution,[],[f11570,f8179]) ).
fof(f11572,plain,
( ~ spl10_115
| spl10_217 ),
inference(avatar_contradiction_clause,[],[f11571]) ).
fof(f11573,plain,
( ~ spl10_217
| ~ spl10_114 ),
inference(avatar_split_clause,[],[f7080,f4324,f10008]) ).
fof(f11801,plain,
( member(sK1(sF6,sF9),sF5)
| spl10_114
| spl10_115 ),
inference(resolution,[],[f10576,f59]) ).
fof(f11806,plain,
( $false
| spl10_114
| spl10_115 ),
inference(forward_subsumption_resolution,[],[f11801,f4329]) ).
fof(f11807,plain,
( spl10_114
| spl10_115 ),
inference(avatar_contradiction_clause,[],[f11806]) ).
cnf(s288,plain,
( ~ spl10_114
| spl10_115 ),
inference(sat_conversion,[],[f8169]) ).
cnf(s383,plain,
( spl10_114
| ~ spl10_216 ),
inference(sat_conversion,[],[f11430]) ).
cnf(s387,plain,
( ~ spl10_115
| spl10_216
| ~ spl10_217 ),
inference(sat_conversion,[],[f11569]) ).
cnf(s388,plain,
( ~ spl10_115
| spl10_217 ),
inference(sat_conversion,[],[f11572]) ).
cnf(s389,plain,
( ~ spl10_114
| ~ spl10_217 ),
inference(sat_conversion,[],[f11573]) ).
cnf(s405,plain,
( spl10_114
| spl10_115 ),
inference(sat_conversion,[],[f11807]) ).
cnf(s406,plain,
spl10_114,
inference(rat,[],[s387,s388,s383,s405]) ).
cnf(s408,plain,
~ spl10_217,
inference(rat,[],[s389,s406]) ).
cnf(s409,plain,
spl10_115,
inference(rat,[],[s288,s406]) ).
cnf(s412,plain,
$false,
inference(rat,[],[s388,s408,s409]) ).
fof(f11808,plain,
$false,
inference(avatar_sat_refutation,[],[s412]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SET615+3 : TPTP v9.3.1. Released v2.2.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.40 % Computer : n018.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Mon Sep 28 02:21:39 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.43 Running first-order model finding
% 0.13/0.43 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
% 2.28/1.01 % (2930338)Will run a generic schedule for satisfiability detection.
% 2.28/1.01 % (2930349)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=2515436040:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 2.28/1.01 % (2930344)% WARNING: option uhcvi not known.
% 2.28/1.01 % (2930345)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=2330875639:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 2.28/1.01 % (2930343)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=2819914039_2999 on theBenchmark for (2999ds/0Mi)
% 2.28/1.01 % (2930344)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=2820114537:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 2.28/1.01 % (2930346)dis+10_1_sil=32000:sp=arity:random_seed=407115698:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 2.28/1.01 % (2930347)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2963774469:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 2.28/1.01 % (2930348)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=525994445:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 2.28/1.01 % TRYING [1]
% 2.28/1.01 % TRYING [2]
% 2.28/1.01 % TRYING [3]
% 2.28/1.01 % TRYING [4]
% 2.28/1.01 % (2930349)Instruction limit reached!
% 2.28/1.01 % (2930349)------------------------------
% 2.28/1.01 % (2930349)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.28/1.01 % (2930349)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.28/1.01 % (2930349)CaDiCaL version: 2.1.3
% 2.28/1.01 % (2930349)Termination reason: Instruction limit
% 2.28/1.01 % (2930349)Termination phase: Saturation
% 2.28/1.01 % (2930349)Time elapsed: 0.050 s
% 2.28/1.01 % (2930349)Peak memory usage: 13 MB
% 2.28/1.01 % (2930349)Instructions burned: 161 (million)
% 2.28/1.01 % TRYING [5]
% 2.28/1.01 % (2930357)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3373553297:i=714:nm=2_2999 on theBenchmark for (2999ds/714Mi)
% 2.28/1.01 % TRYING [1]
% 2.28/1.01 % (2930346)Instruction limit reached!
% 2.28/1.01 % (2930346)------------------------------
% 2.28/1.01 % (2930346)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.28/1.01 % (2930346)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.28/1.01 % (2930346)CaDiCaL version: 2.1.3
% 2.28/1.01 % (2930346)Termination reason: Instruction limit
% 2.28/1.01 % (2930346)Termination phase: Saturation
% 2.28/1.01 % (2930346)Time elapsed: 0.062 s
% 2.28/1.01 % (2930346)Peak memory usage: 12 MB
% 2.28/1.01 % (2930346)Instructions burned: 103 (million)
% 2.28/1.01 % TRYING [2]
% 2.28/1.01 % TRYING [3]
% 2.28/1.01 % TRYING [4]
% 2.28/1.01 % (2930347)Instruction limit reached!
% 2.28/1.01 % (2930347)------------------------------
% 2.28/1.01 % (2930347)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.28/1.01 % (2930347)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.28/1.01 % (2930347)CaDiCaL version: 2.1.3
% 2.28/1.01 % (2930347)Termination reason: Instruction limit
% 2.28/1.01 % (2930347)Termination phase: Saturation
% 2.28/1.01 % (2930347)Time elapsed: 0.065 s
% 2.28/1.01 % (2930347)Peak memory usage: 12 MB
% 2.28/1.01 % (2930347)Instructions burned: 116 (million)
% 2.28/1.01 % (2930348)Instruction limit reached!
% 2.28/1.01 % (2930348)------------------------------
% 2.28/1.01 % (2930348)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.28/1.01 % (2930348)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.28/1.01 % (2930348)CaDiCaL version: 2.1.3
% 2.28/1.01 % (2930348)Termination reason: Instruction limit
% 2.28/1.01 % (2930348)Termination phase: Saturation
% 2.28/1.01 % (2930348)Time elapsed: 0.076 s
% 2.28/1.01 % (2930348)Peak memory usage: 12 MB
% 2.28/1.01 % (2930348)Instructions burned: 131 (million)
% 2.28/1.01 % (2930359)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2127043109:i=131:bd=preordered:fsd=on_2999 on theBenchmark for (2999ds/131Mi)
% 2.28/1.01 % (2930360)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=2269993377:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 2.28/1.01 % TRYING [5]
% 2.28/1.01 % (2930361)ott-21_1_sil=16000:fs=off:random_seed=1402671302:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 2.28/1.01 % (2930359)Instruction limit reached!
% 2.28/1.01 % (2930359)------------------------------
% 2.28/1.01 % (2930359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.28/1.01 % (2930359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.28/1.01 % (2930359)CaDiCaL version: 2.1.3
% 2.28/1.01 % (2930359)Termination reason: Instruction limit
% 2.28/1.01 % (2930359)Termination phase: Saturation
% 2.28/1.01 % (2930359)Time elapsed: 0.081 s
% 2.28/1.01 % (2930359)Peak memory usage: 13 MB
% 2.28/1.01 % (2930359)Instructions burned: 131 (million)
% 2.28/1.01 % (2930365)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=968622510:i=477:bd=all_2998 on theBenchmark for (2998ds/477Mi)
% 2.28/1.01 % (2930361)Instruction limit reached!
% 2.28/1.01 % (2930361)------------------------------
% 2.28/1.01 % (2930361)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.28/1.01 % (2930361)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.28/1.01 % (2930361)CaDiCaL version: 2.1.3
% 2.28/1.01 % (2930361)Termination reason: Instruction limit
% 2.28/1.01 % (2930361)Termination phase: Saturation
% 2.28/1.01 % (2930361)Time elapsed: 0.091 s
% 2.28/1.01 % (2930361)Peak memory usage: 12 MB
% 2.28/1.01 % (2930361)Instructions burned: 181 (million)
% 2.28/1.01 % (2930367)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=1230120301:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 2.28/1.01 % TRYING [1]
% 2.28/1.01 % TRYING [2]
% 2.28/1.01 % TRYING [3]
% 2.28/1.01 % TRYING [4]
% 2.28/1.01 % TRYING [5]
% 2.28/1.01 % (2930357)Instruction limit reached!
% 2.28/1.01 % (2930357)------------------------------
% 2.28/1.01 % (2930357)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.28/1.01 % (2930357)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.28/1.01 % (2930357)CaDiCaL version: 2.1.3
% 2.28/1.01 % (2930357)Termination reason: Instruction limit
% 2.28/1.01 % (2930357)Termination phase: Finite model building SAT solving
% 2.28/1.01 % (2930357)Time elapsed: 0.231 s
% 2.28/1.01 % (2930357)Peak memory usage: 13 MB
% 2.28/1.01 % (2930357)Instructions burned: 715 (million)
% 2.28/1.01 % (2930369)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=4130414960:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 2.28/1.01 % (2930360)Instruction limit reached!
% 2.28/1.01 % (2930360)------------------------------
% 2.28/1.01 % (2930360)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.28/1.01 % (2930360)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.28/1.01 % (2930360)CaDiCaL version: 2.1.3
% 2.28/1.01 % (2930360)Termination reason: Instruction limit
% 2.28/1.01 % (2930360)Termination phase: Saturation
% 2.28/1.01 % (2930360)Time elapsed: 0.372 s
% 2.28/1.01 % (2930360)Peak memory usage: 17 MB
% 2.28/1.01 % (2930360)Instructions burned: 685 (million)
% 2.28/1.01 % (2930365)Instruction limit reached!
% 2.28/1.01 % (2930365)------------------------------
% 2.28/1.01 % (2930365)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.28/1.01 % (2930365)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.28/1.01 % (2930365)CaDiCaL version: 2.1.3
% 2.28/1.01 % (2930365)Termination reason: Instruction limit
% 2.28/1.01 % (2930365)Termination phase: Saturation
% 2.28/1.01 % (2930365)Time elapsed: 0.291 s
% 2.28/1.01 % (2930365)Peak memory usage: 14 MB
% 2.28/1.01 % (2930365)Instructions burned: 477 (million)
% 2.28/1.01 % (2930371)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=3161371101:i=889:ins=1_2995 on theBenchmark for (2995ds/889Mi)
% 2.28/1.01 % TRYING [14]
% 2.28/1.01 % (2930372)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=2949893050:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 2.28/1.01 % (2930369) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-2930338-2930369"...
% 2.28/1.01 % (2930369)...printing done.
% 2.28/1.01 % (2930369)Refutation found. Thanks to Tanya!
% 2.28/1.01 % SZS status Theorem for theBenchmark
% 2.28/1.01 % SZS output start Proof for theBenchmark
% See solution above
% 2.28/1.01 % (2930369)------------------------------
% 2.28/1.01 % (2930369)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 2.28/1.01 % (2930369)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.28/1.01 % (2930369)CaDiCaL version: 2.1.3
% 2.28/1.01 % (2930369)Termination reason: Refutation
% 2.28/1.01 % (2930369)Time elapsed: 0.225 s
% 2.28/1.01 % (2930369)Peak memory usage: 17 MB
% 2.28/1.01 % (2930369)Instructions burned: 740 (million)
% 2.28/1.01 % (2930338)Success in time 0.57 s
% 2.28/1.01 % Vampire exiting
%------------------------------------------------------------------------------