%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SET967+1 : TPTP v9.3.1. Released v3.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n004.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:42:26 PM UTC 2026
% Result : Theorem 12.61s 2.75s
% Output : Refutation 13.96s
% Verified :
% SZS Type : Refutation
% Derivation depth : 29
% Number of leaves : 33
% Syntax : Number of formulae : 288 ( 30 unt; 26 def)
% Number of atoms : 846 ( 105 equ)
% Maximal formula atoms : 14 ( 2 avg)
% Number of connectives : 874 ( 316 ~; 509 |; 28 &)
% ( 20 <=>; 1 =>; 0 <=; 0 <~>)
% Maximal formula depth : 11 ( 4 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 20 ( 18 usr; 18 prp; 0-2 aty)
% Number of functors : 20 ( 20 usr; 12 con; 0-3 aty)
% Number of variables : 217 ( 1 sgn 209 !; 8 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f4,axiom,
! [X0,X1,X2] :
( X2 = set_union2(X0,X1)
<=> ! [X3] :
( in(X3,X2)
<=> ( in(X3,X0)
| in(X3,X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_xboole_0) ).
fof(f5,axiom,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_tarski) ).
fof(f9,axiom,
! [X0,X1] : set_union2(X0,X0) = X0,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',idempotence_k2_xboole_0) ).
fof(f10,axiom,
! [X0,X1,X2,X3] :
( in(ordered_pair(X0,X1),cartesian_product2(X2,X3))
<=> ( in(X0,X2)
& in(X1,X3) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',l55_zfmisc_1) ).
fof(f13,axiom,
! [X0,X1,X2] :
~ ( in(X0,cartesian_product2(X1,X2))
& ! [X3,X4] : ordered_pair(X3,X4) != X0 ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t102_zfmisc_1) ).
fof(f14,axiom,
! [X0,X1,X2,X3] :
( in(ordered_pair(X0,X1),cartesian_product2(X2,X3))
=> in(ordered_pair(X1,X0),cartesian_product2(X3,X2)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t107_zfmisc_1) ).
fof(f16,conjecture,
! [X0,X1,X2] :
( cartesian_product2(set_union2(X0,X1),X2) = set_union2(cartesian_product2(X0,X2),cartesian_product2(X1,X2))
& cartesian_product2(X2,set_union2(X0,X1)) = set_union2(cartesian_product2(X2,X0),cartesian_product2(X2,X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t120_zfmisc_1) ).
fof(f17,negated_conjecture,
~ ! [X0,X1,X2] :
( cartesian_product2(set_union2(X0,X1),X2) = set_union2(cartesian_product2(X0,X2),cartesian_product2(X1,X2))
& cartesian_product2(X2,set_union2(X0,X1)) = set_union2(cartesian_product2(X2,X0),cartesian_product2(X2,X1)) ),
inference(negated_conjecture,[status(cth)],[f16]) ).
fof(f18,plain,
! [X0] : set_union2(X0,X0) = X0,
inference(rectify,[],[f9]) ).
fof(f23,plain,
! [X0,X1,X2] :
( ~ in(X0,cartesian_product2(X1,X2))
| ? [X3,X4] : ordered_pair(X3,X4) = X0 ),
inference(ennf_transformation,[],[f13]) ).
fof(f24,plain,
! [X0,X1,X2,X3] :
( in(ordered_pair(X1,X0),cartesian_product2(X3,X2))
| ~ in(ordered_pair(X0,X1),cartesian_product2(X2,X3)) ),
inference(ennf_transformation,[],[f14]) ).
fof(f27,plain,
? [X0,X1,X2] :
( cartesian_product2(set_union2(X0,X1),X2) != set_union2(cartesian_product2(X0,X2),cartesian_product2(X1,X2))
| cartesian_product2(X2,set_union2(X0,X1)) != set_union2(cartesian_product2(X2,X0),cartesian_product2(X2,X1)) ),
inference(ennf_transformation,[],[f17]) ).
fof(f28,plain,
! [X0,X1,X2] :
( ( X2 = set_union2(X0,X1)
| ? [X3] :
( ( ( ~ in(X3,X0)
& ~ in(X3,X1) )
| ~ in(X3,X2) )
& ( in(X3,X0)
| in(X3,X1)
| in(X3,X2) ) ) )
& ( ! [X3] :
( ( in(X3,X2)
| ( ~ in(X3,X0)
& ~ in(X3,X1) ) )
& ( in(X3,X0)
| in(X3,X1)
| ~ in(X3,X2) ) )
| set_union2(X0,X1) != X2 ) ),
inference(nnf_transformation,[],[f4]) ).
fof(f29,plain,
! [X0,X1,X2] :
( ( X2 = set_union2(X0,X1)
| ? [X3] :
( ( ( ~ in(X3,X0)
& ~ in(X3,X1) )
| ~ in(X3,X2) )
& ( in(X3,X0)
| in(X3,X1)
| in(X3,X2) ) ) )
& ( ! [X3] :
( ( in(X3,X2)
| ( ~ in(X3,X0)
& ~ in(X3,X1) ) )
& ( in(X3,X0)
| in(X3,X1)
| ~ in(X3,X2) ) )
| set_union2(X0,X1) != X2 ) ),
inference(flattening,[],[f28]) ).
fof(f30,plain,
! [X0,X1,X2] :
( ( X2 = set_union2(X0,X1)
| ? [X3] :
( ( ( ~ in(X3,X0)
& ~ in(X3,X1) )
| ~ in(X3,X2) )
& ( in(X3,X0)
| in(X3,X1)
| in(X3,X2) ) ) )
& ( ! [X4] :
( ( in(X4,X2)
| ( ~ in(X4,X0)
& ~ in(X4,X1) ) )
& ( in(X4,X0)
| in(X4,X1)
| ~ in(X4,X2) ) )
| set_union2(X0,X1) != X2 ) ),
inference(rectify,[],[f29]) ).
fof(f31,plain,
! [X0,X1,X2] :
( ( X2 = set_union2(X0,X1)
| ( ( ( ~ in(sK0(X0,X1,X2),X0)
& ~ in(sK0(X0,X1,X2),X1) )
| ~ in(sK0(X0,X1,X2),X2) )
& ( in(sK0(X0,X1,X2),X0)
| in(sK0(X0,X1,X2),X1)
| in(sK0(X0,X1,X2),X2) ) ) )
& ( ! [X4] :
( ( in(X4,X2)
| ( ~ in(X4,X0)
& ~ in(X4,X1) ) )
& ( in(X4,X0)
| in(X4,X1)
| ~ in(X4,X2) ) )
| set_union2(X0,X1) != X2 ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0]),skolemize(X3,sK0(X0,X1,X2))],[f30]) ).
fof(f32,plain,
! [X0,X1,X2,X3] :
( ( in(ordered_pair(X0,X1),cartesian_product2(X2,X3))
| ~ in(X0,X2)
| ~ in(X1,X3) )
& ( ( in(X0,X2)
& in(X1,X3) )
| ~ in(ordered_pair(X0,X1),cartesian_product2(X2,X3)) ) ),
inference(nnf_transformation,[],[f10]) ).
fof(f33,plain,
! [X0,X1,X2,X3] :
( ( in(ordered_pair(X0,X1),cartesian_product2(X2,X3))
| ~ in(X0,X2)
| ~ in(X1,X3) )
& ( ( in(X0,X2)
& in(X1,X3) )
| ~ in(ordered_pair(X0,X1),cartesian_product2(X2,X3)) ) ),
inference(flattening,[],[f32]) ).
fof(f36,plain,
! [X0,X1,X2] :
( ~ in(X0,cartesian_product2(X1,X2))
| ordered_pair(sK3(X0),sK4(X0)) = X0 ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4]),skolemize(X3,sK3(X0)),skolemize(X4,sK4(X0))],[f23]) ).
fof(f39,plain,
( cartesian_product2(set_union2(sK9,sK10),sK11) != set_union2(cartesian_product2(sK9,sK11),cartesian_product2(sK10,sK11))
| cartesian_product2(sK11,set_union2(sK9,sK10)) != set_union2(cartesian_product2(sK11,sK9),cartesian_product2(sK11,sK10)) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9,sK10,sK11]),skolemize(X0,sK9),skolemize(X1,sK10),skolemize(X2,sK11)],[f27]) ).
fof(f43,plain,
! [X2,X0,X1,X4] :
( in(X4,X0)
| in(X4,X1)
| ~ in(X4,X2)
| set_union2(X0,X1) != X2 ),
inference(cnf_transformation,[],[f31]) ).
fof(f44,plain,
! [X2,X0,X1,X4] :
( in(X4,X2)
| ~ in(X4,X1)
| set_union2(X0,X1) != X2 ),
inference(cnf_transformation,[],[f31]) ).
fof(f45,plain,
! [X2,X0,X1,X4] :
( in(X4,X2)
| ~ in(X4,X0)
| set_union2(X0,X1) != X2 ),
inference(cnf_transformation,[],[f31]) ).
fof(f46,plain,
! [X2,X0,X1] :
( in(sK0(X0,X1,X2),X2)
| in(sK0(X0,X1,X2),X1)
| in(sK0(X0,X1,X2),X0)
| set_union2(X0,X1) = X2 ),
inference(cnf_transformation,[],[f31]) ).
fof(f48,plain,
! [X2,X0,X1] :
( ~ in(sK0(X0,X1,X2),X2)
| ~ in(sK0(X0,X1,X2),X0)
| set_union2(X0,X1) = X2 ),
inference(cnf_transformation,[],[f31]) ).
fof(f49,plain,
! [X0,X1] : ordered_pair(X0,X1) = unordered_pair(unordered_pair(X0,X1),singleton(X0)),
inference(cnf_transformation,[],[f5]) ).
fof(f53,plain,
! [X0] : set_union2(X0,X0) = X0,
inference(cnf_transformation,[],[f18]) ).
fof(f54,plain,
! [X2,X3,X0,X1] :
( in(X1,X3)
| ~ in(ordered_pair(X0,X1),cartesian_product2(X2,X3)) ),
inference(cnf_transformation,[],[f33]) ).
fof(f55,plain,
! [X2,X3,X0,X1] :
( in(X0,X2)
| ~ in(ordered_pair(X0,X1),cartesian_product2(X2,X3)) ),
inference(cnf_transformation,[],[f33]) ).
fof(f56,plain,
! [X2,X3,X0,X1] :
( in(ordered_pair(X0,X1),cartesian_product2(X2,X3))
| ~ in(X0,X2)
| ~ in(X1,X3) ),
inference(cnf_transformation,[],[f33]) ).
fof(f59,plain,
! [X2,X0,X1] :
( ~ in(X0,cartesian_product2(X1,X2))
| ordered_pair(sK3(X0),sK4(X0)) = X0 ),
inference(cnf_transformation,[],[f36]) ).
fof(f60,plain,
! [X2,X3,X0,X1] :
( in(ordered_pair(X1,X0),cartesian_product2(X3,X2))
| ~ in(ordered_pair(X0,X1),cartesian_product2(X2,X3)) ),
inference(cnf_transformation,[],[f24]) ).
fof(f69,plain,
( cartesian_product2(set_union2(sK9,sK10),sK11) != set_union2(cartesian_product2(sK9,sK11),cartesian_product2(sK10,sK11))
| cartesian_product2(sK11,set_union2(sK9,sK10)) != set_union2(cartesian_product2(sK11,sK9),cartesian_product2(sK11,sK10)) ),
inference(cnf_transformation,[],[f39]) ).
fof(f71,plain,
! [X2,X3,X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),cartesian_product2(X2,X3))
| ~ in(X0,X2)
| ~ in(X1,X3) ),
inference(definition_unfolding,[],[f56,f49]) ).
fof(f72,plain,
! [X2,X3,X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),cartesian_product2(X2,X3))
| in(X0,X2) ),
inference(definition_unfolding,[],[f55,f49]) ).
fof(f73,plain,
! [X2,X3,X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),cartesian_product2(X2,X3))
| in(X1,X3) ),
inference(definition_unfolding,[],[f54,f49]) ).
fof(f74,plain,
! [X2,X0,X1] :
( ~ in(X0,cartesian_product2(X1,X2))
| unordered_pair(unordered_pair(sK3(X0),sK4(X0)),singleton(sK3(X0))) = X0 ),
inference(definition_unfolding,[],[f59,f49]) ).
fof(f75,plain,
! [X2,X3,X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),cartesian_product2(X2,X3))
| in(unordered_pair(unordered_pair(X1,X0),singleton(X1)),cartesian_product2(X3,X2)) ),
inference(definition_unfolding,[],[f60,f49,f49]) ).
fof(f84,plain,
! [X0,X1,X4] :
( in(X4,set_union2(X0,X1))
| ~ in(X4,X0) ),
inference(equality_resolution,[],[f45]) ).
fof(f85,plain,
! [X0,X1,X4] :
( in(X4,set_union2(X0,X1))
| ~ in(X4,X1) ),
inference(equality_resolution,[],[f44]) ).
fof(f86,plain,
! [X0,X1,X4] :
( ~ in(X4,set_union2(X0,X1))
| in(X4,X1)
| in(X4,X0) ),
inference(equality_resolution,[],[f43]) ).
fof(f87,definition,
sF12 = set_union2(sK9,sK10),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
fof(f88,plain,
set_union2(sK9,sK10) = sF12,
inference(reorient_equations,[],[f87]) ).
fof(f89,definition,
sF13 = cartesian_product2(sF12,sK11),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
fof(f90,plain,
cartesian_product2(sF12,sK11) = sF13,
inference(reorient_equations,[],[f89]) ).
fof(f91,definition,
sF14 = cartesian_product2(sK9,sK11),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
fof(f92,plain,
cartesian_product2(sK9,sK11) = sF14,
inference(reorient_equations,[],[f91]) ).
fof(f93,definition,
sF15 = cartesian_product2(sK10,sK11),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
fof(f94,plain,
cartesian_product2(sK10,sK11) = sF15,
inference(reorient_equations,[],[f93]) ).
fof(f95,definition,
sF16 = set_union2(sF14,sF15),
introduced(definition,[new_symbols(definition,[sF16])],[function_definition]) ).
fof(f96,plain,
set_union2(sF14,sF15) = sF16,
inference(reorient_equations,[],[f95]) ).
fof(f97,definition,
sF17 = cartesian_product2(sK11,sF12),
introduced(definition,[new_symbols(definition,[sF17])],[function_definition]) ).
fof(f98,plain,
cartesian_product2(sK11,sF12) = sF17,
inference(reorient_equations,[],[f97]) ).
fof(f99,definition,
sF18 = cartesian_product2(sK11,sK9),
introduced(definition,[new_symbols(definition,[sF18])],[function_definition]) ).
fof(f100,plain,
cartesian_product2(sK11,sK9) = sF18,
inference(reorient_equations,[],[f99]) ).
fof(f101,definition,
sF19 = cartesian_product2(sK11,sK10),
introduced(definition,[new_symbols(definition,[sF19])],[function_definition]) ).
fof(f102,plain,
cartesian_product2(sK11,sK10) = sF19,
inference(reorient_equations,[],[f101]) ).
fof(f103,definition,
sF20 = set_union2(sF18,sF19),
introduced(definition,[new_symbols(definition,[sF20])],[function_definition]) ).
fof(f104,plain,
set_union2(sF18,sF19) = sF20,
inference(reorient_equations,[],[f103]) ).
fof(f105,plain,
( sF13 != sF16
| sF17 != sF20 ),
inference(definition_folding,[],[f69,f104,f102,f100,f98,f88,f96,f94,f92,f90,f88]) ).
fof(f107,definition,
( spl21_1
<=> sF17 = sF20 ),
introduced(definition,[new_symbols(definition,[spl21_1])],[avatar_definition]) ).
fof(f108,plain,
( sF17 = sF20
| ~ spl21_1 ),
inference(avatar_component_clause,[],[f107]) ).
fof(f109,plain,
( sF17 != sF20
| spl21_1 ),
inference(avatar_component_clause,[],[f107]) ).
fof(f111,definition,
( spl21_2
<=> sF13 = sF16 ),
introduced(definition,[new_symbols(definition,[spl21_2])],[avatar_definition]) ).
fof(f113,plain,
( sF13 != sF16
| spl21_2 ),
inference(avatar_component_clause,[],[f111]) ).
fof(f114,plain,
( ~ spl21_1
| ~ spl21_2 ),
inference(avatar_split_clause,[],[f105,f111,f107]) ).
fof(f117,plain,
! [X0] :
( ~ in(X0,sF14)
| in(X0,sF16) ),
inference(superposition,[],[f84,f96]) ).
fof(f118,plain,
! [X0] :
( ~ in(X0,sF15)
| in(X0,sF16) ),
inference(superposition,[],[f85,f96]) ).
fof(f119,plain,
! [X0] :
( ~ in(X0,sF16)
| in(X0,sF15)
| in(X0,sF14) ),
inference(superposition,[],[f86,f96]) ).
fof(f120,plain,
! [X0] :
( ~ in(X0,sF18)
| in(X0,sF20) ),
inference(superposition,[],[f84,f104]) ).
fof(f121,plain,
! [X0] :
( ~ in(X0,sF19)
| in(X0,sF20) ),
inference(superposition,[],[f85,f104]) ).
fof(f122,plain,
! [X0] :
( ~ in(X0,sF20)
| in(X0,sF19)
| in(X0,sF18) ),
inference(superposition,[],[f86,f104]) ).
fof(f123,plain,
! [X0] :
( ~ in(X0,sK9)
| in(X0,sF12) ),
inference(superposition,[],[f84,f88]) ).
fof(f124,plain,
! [X0] :
( ~ in(X0,sK10)
| in(X0,sF12) ),
inference(superposition,[],[f85,f88]) ).
fof(f125,plain,
! [X0] :
( ~ in(X0,sF12)
| in(X0,sK10)
| in(X0,sK9) ),
inference(superposition,[],[f86,f88]) ).
fof(f126,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sF17)
| in(unordered_pair(unordered_pair(X1,X0),singleton(X1)),cartesian_product2(sF12,sK11)) ),
inference(superposition,[],[f75,f98]) ).
fof(f129,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sF17)
| in(unordered_pair(unordered_pair(X1,X0),singleton(X1)),sF13) ),
inference(forward_demodulation,[],[f126,f90]) ).
fof(f138,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sF14)
| in(X1,sK11) ),
inference(superposition,[],[f73,f92]) ).
fof(f140,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sF17)
| in(X1,sF12) ),
inference(superposition,[],[f73,f98]) ).
fof(f141,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sF19)
| in(X1,sK10) ),
inference(superposition,[],[f73,f102]) ).
fof(f142,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sF18)
| in(X1,sK9) ),
inference(superposition,[],[f73,f100]) ).
fof(f143,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sF13)
| in(X1,sK11) ),
inference(superposition,[],[f73,f90]) ).
fof(f145,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sF15)
| in(X0,sK10) ),
inference(superposition,[],[f72,f94]) ).
fof(f146,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sF17)
| in(X0,sK11) ),
inference(superposition,[],[f72,f98]) ).
fof(f147,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sF19)
| in(X0,sK11) ),
inference(superposition,[],[f72,f102]) ).
fof(f148,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sF18)
| in(X0,sK11) ),
inference(superposition,[],[f72,f100]) ).
fof(f149,plain,
! [X0,X1] :
( ~ in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sF13)
| in(X0,sF12) ),
inference(superposition,[],[f72,f90]) ).
fof(f153,plain,
! [X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sF14)
| ~ in(X0,sK9)
| ~ in(X1,sK11) ),
inference(superposition,[],[f71,f92]) ).
fof(f154,plain,
! [X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sF15)
| ~ in(X0,sK10)
| ~ in(X1,sK11) ),
inference(superposition,[],[f71,f94]) ).
fof(f155,plain,
! [X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sF17)
| ~ in(X0,sK11)
| ~ in(X1,sF12) ),
inference(superposition,[],[f71,f98]) ).
fof(f156,plain,
! [X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sF19)
| ~ in(X0,sK11)
| ~ in(X1,sK10) ),
inference(superposition,[],[f71,f102]) ).
fof(f157,plain,
! [X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sF18)
| ~ in(X0,sK11)
| ~ in(X1,sK9) ),
inference(superposition,[],[f71,f100]) ).
fof(f160,plain,
! [X0] :
( ~ in(X0,sF14)
| unordered_pair(unordered_pair(sK3(X0),sK4(X0)),singleton(sK3(X0))) = X0 ),
inference(superposition,[],[f74,f92]) ).
fof(f161,plain,
! [X0] :
( ~ in(X0,sF15)
| unordered_pair(unordered_pair(sK3(X0),sK4(X0)),singleton(sK3(X0))) = X0 ),
inference(superposition,[],[f74,f94]) ).
fof(f162,plain,
! [X0] :
( ~ in(X0,sF17)
| unordered_pair(unordered_pair(sK3(X0),sK4(X0)),singleton(sK3(X0))) = X0 ),
inference(superposition,[],[f74,f98]) ).
fof(f163,plain,
! [X0] :
( ~ in(X0,sF19)
| unordered_pair(unordered_pair(sK3(X0),sK4(X0)),singleton(sK3(X0))) = X0 ),
inference(superposition,[],[f74,f102]) ).
fof(f164,plain,
! [X0] :
( ~ in(X0,sF18)
| unordered_pair(unordered_pair(sK3(X0),sK4(X0)),singleton(sK3(X0))) = X0 ),
inference(superposition,[],[f74,f100]) ).
fof(f165,plain,
! [X0] :
( ~ in(X0,sF13)
| unordered_pair(unordered_pair(sK3(X0),sK4(X0)),singleton(sK3(X0))) = X0 ),
inference(superposition,[],[f74,f90]) ).
fof(f226,plain,
! [X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sF20)
| ~ in(X1,sK9)
| ~ in(X0,sK11) ),
inference(resolution,[],[f157,f120]) ).
fof(f233,plain,
! [X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sF16)
| ~ in(X1,sK11)
| ~ in(X0,sK9) ),
inference(resolution,[],[f153,f117]) ).
fof(f240,plain,
! [X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sF20)
| ~ in(X1,sK10)
| ~ in(X0,sK11) ),
inference(resolution,[],[f156,f121]) ).
fof(f247,plain,
! [X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sF16)
| ~ in(X1,sK11)
| ~ in(X0,sK10) ),
inference(resolution,[],[f154,f118]) ).
fof(f720,plain,
! [X0,X1] :
( in(sK0(sF16,X0,X1),sF15)
| in(sK0(sF16,X0,X1),X1)
| in(sK0(sF16,X0,X1),X0)
| set_union2(sF16,X0) = X1
| in(sK0(sF16,X0,X1),sF14) ),
inference(resolution,[],[f46,f119]) ).
fof(f726,plain,
! [X0,X1] :
( in(sK0(sF20,X0,X1),sF19)
| in(sK0(sF20,X0,X1),X1)
| in(sK0(sF20,X0,X1),X0)
| set_union2(sF20,X0) = X1
| in(sK0(sF20,X0,X1),sF18) ),
inference(resolution,[],[f46,f122]) ).
fof(f752,plain,
! [X0] :
( in(sK0(sF20,sF20,X0),sF19)
| in(sK0(sF20,sF20,X0),X0)
| set_union2(sF20,sF20) = X0
| in(sK0(sF20,sF20,X0),sF18)
| in(sK0(sF20,sF20,X0),sF19)
| in(sK0(sF20,sF20,X0),sF18) ),
inference(resolution,[],[f726,f122]) ).
fof(f756,plain,
! [X0] :
( in(sK0(sF20,sF20,X0),sF19)
| in(sK0(sF20,sF20,X0),X0)
| set_union2(sF20,sF20) = X0
| in(sK0(sF20,sF20,X0),sF18) ),
inference(duplicate_literal_removal,[],[f752]) ).
fof(f760,plain,
! [X0] :
( in(sK0(sF20,sF20,X0),sF19)
| in(sK0(sF20,sF20,X0),X0)
| sF20 = X0
| in(sK0(sF20,sF20,X0),sF18) ),
inference(forward_demodulation,[],[f756,f53]) ).
fof(f784,plain,
( in(sK0(sF20,sF20,sF17),sF19)
| sF17 = sF20
| in(sK0(sF20,sF20,sF17),sF18)
| sK0(sF20,sF20,sF17) = unordered_pair(unordered_pair(sK3(sK0(sF20,sF20,sF17)),sK4(sK0(sF20,sF20,sF17))),singleton(sK3(sK0(sF20,sF20,sF17)))) ),
inference(resolution,[],[f760,f162]) ).
fof(f801,plain,
( sF17 = sF20
| in(sK0(sF20,sF20,sF17),sF18)
| sK0(sF20,sF20,sF17) = unordered_pair(unordered_pair(sK3(sK0(sF20,sF20,sF17)),sK4(sK0(sF20,sF20,sF17))),singleton(sK3(sK0(sF20,sF20,sF17)))) ),
inference(forward_subsumption_resolution,[],[f784,f163]) ).
fof(f860,plain,
( sF17 = sF20
| sK0(sF20,sF20,sF17) = unordered_pair(unordered_pair(sK3(sK0(sF20,sF20,sF17)),sK4(sK0(sF20,sF20,sF17))),singleton(sK3(sK0(sF20,sF20,sF17)))) ),
inference(forward_subsumption_resolution,[],[f801,f164]) ).
fof(f863,plain,
( sK0(sF20,sF20,sF17) = unordered_pair(unordered_pair(sK3(sK0(sF20,sF20,sF17)),sK4(sK0(sF20,sF20,sF17))),singleton(sK3(sK0(sF20,sF20,sF17))))
| spl21_1 ),
inference(forward_subsumption_resolution,[],[f860,f109]) ).
fof(f888,plain,
( ~ in(sK0(sF20,sF20,sF17),sF17)
| in(sK4(sK0(sF20,sF20,sF17)),sF12)
| spl21_1 ),
inference(superposition,[],[f140,f863]) ).
fof(f889,plain,
( ~ in(sK0(sF20,sF20,sF17),sF19)
| in(sK4(sK0(sF20,sF20,sF17)),sK10)
| spl21_1 ),
inference(superposition,[],[f141,f863]) ).
fof(f890,plain,
( ~ in(sK0(sF20,sF20,sF17),sF18)
| in(sK4(sK0(sF20,sF20,sF17)),sK9)
| spl21_1 ),
inference(superposition,[],[f142,f863]) ).
fof(f894,plain,
( ~ in(sK0(sF20,sF20,sF17),sF17)
| in(sK3(sK0(sF20,sF20,sF17)),sK11)
| spl21_1 ),
inference(superposition,[],[f146,f863]) ).
fof(f895,plain,
( ~ in(sK0(sF20,sF20,sF17),sF19)
| in(sK3(sK0(sF20,sF20,sF17)),sK11)
| spl21_1 ),
inference(superposition,[],[f147,f863]) ).
fof(f896,plain,
( ~ in(sK0(sF20,sF20,sF17),sF18)
| in(sK3(sK0(sF20,sF20,sF17)),sK11)
| spl21_1 ),
inference(superposition,[],[f148,f863]) ).
fof(f900,plain,
( in(sK0(sF20,sF20,sF17),sF17)
| ~ in(sK3(sK0(sF20,sF20,sF17)),sK11)
| ~ in(sK4(sK0(sF20,sF20,sF17)),sF12)
| spl21_1 ),
inference(superposition,[],[f155,f863]) ).
fof(f901,plain,
( in(sK0(sF20,sF20,sF17),sF19)
| ~ in(sK3(sK0(sF20,sF20,sF17)),sK11)
| ~ in(sK4(sK0(sF20,sF20,sF17)),sK10)
| spl21_1 ),
inference(superposition,[],[f156,f863]) ).
fof(f902,plain,
( in(sK0(sF20,sF20,sF17),sF18)
| ~ in(sK3(sK0(sF20,sF20,sF17)),sK11)
| ~ in(sK4(sK0(sF20,sF20,sF17)),sK9)
| spl21_1 ),
inference(superposition,[],[f157,f863]) ).
fof(f904,plain,
( in(sK0(sF20,sF20,sF17),sF20)
| ~ in(sK4(sK0(sF20,sF20,sF17)),sK9)
| ~ in(sK3(sK0(sF20,sF20,sF17)),sK11)
| spl21_1 ),
inference(superposition,[],[f226,f863]) ).
fof(f906,plain,
( in(sK0(sF20,sF20,sF17),sF20)
| ~ in(sK4(sK0(sF20,sF20,sF17)),sK10)
| ~ in(sK3(sK0(sF20,sF20,sF17)),sK11)
| spl21_1 ),
inference(superposition,[],[f240,f863]) ).
fof(f1249,definition,
( spl21_64
<=> in(sK3(sK0(sF20,sF20,sF17)),sK11) ),
introduced(definition,[new_symbols(definition,[spl21_64])],[avatar_definition]) ).
fof(f1253,definition,
( spl21_65
<=> in(sK4(sK0(sF20,sF20,sF17)),sK10) ),
introduced(definition,[new_symbols(definition,[spl21_65])],[avatar_definition]) ).
fof(f1254,plain,
( in(sK4(sK0(sF20,sF20,sF17)),sK10)
| ~ spl21_65 ),
inference(avatar_component_clause,[],[f1253]) ).
fof(f1255,plain,
( ~ in(sK4(sK0(sF20,sF20,sF17)),sK10)
| spl21_65 ),
inference(avatar_component_clause,[],[f1253]) ).
fof(f1257,definition,
( spl21_66
<=> in(sK0(sF20,sF20,sF17),sF20) ),
introduced(definition,[new_symbols(definition,[spl21_66])],[avatar_definition]) ).
fof(f1259,plain,
( in(sK0(sF20,sF20,sF17),sF20)
| ~ spl21_66 ),
inference(avatar_component_clause,[],[f1257]) ).
fof(f1260,plain,
( ~ spl21_64
| ~ spl21_65
| spl21_66
| spl21_1 ),
inference(avatar_split_clause,[],[f906,f107,f1257,f1253,f1249]) ).
fof(f1267,definition,
( spl21_68
<=> in(sK4(sK0(sF20,sF20,sF17)),sK9) ),
introduced(definition,[new_symbols(definition,[spl21_68])],[avatar_definition]) ).
fof(f1268,plain,
( in(sK4(sK0(sF20,sF20,sF17)),sK9)
| ~ spl21_68 ),
inference(avatar_component_clause,[],[f1267]) ).
fof(f1269,plain,
( ~ in(sK4(sK0(sF20,sF20,sF17)),sK9)
| spl21_68 ),
inference(avatar_component_clause,[],[f1267]) ).
fof(f1270,plain,
( ~ spl21_64
| ~ spl21_68
| spl21_66
| spl21_1 ),
inference(avatar_split_clause,[],[f904,f107,f1257,f1267,f1249]) ).
fof(f1281,definition,
( spl21_71
<=> in(sK0(sF20,sF20,sF17),sF18) ),
introduced(definition,[new_symbols(definition,[spl21_71])],[avatar_definition]) ).
fof(f1282,plain,
( ~ in(sK0(sF20,sF20,sF17),sF18)
| spl21_71 ),
inference(avatar_component_clause,[],[f1281]) ).
fof(f1284,plain,
( ~ spl21_68
| ~ spl21_64
| spl21_71
| spl21_1 ),
inference(avatar_split_clause,[],[f902,f107,f1281,f1249,f1267]) ).
fof(f1286,definition,
( spl21_72
<=> in(sK0(sF20,sF20,sF17),sF19) ),
introduced(definition,[new_symbols(definition,[spl21_72])],[avatar_definition]) ).
fof(f1287,plain,
( ~ in(sK0(sF20,sF20,sF17),sF19)
| spl21_72 ),
inference(avatar_component_clause,[],[f1286]) ).
fof(f1289,plain,
( ~ spl21_65
| ~ spl21_64
| spl21_72
| spl21_1 ),
inference(avatar_split_clause,[],[f901,f107,f1286,f1249,f1253]) ).
fof(f1291,definition,
( spl21_73
<=> in(sK4(sK0(sF20,sF20,sF17)),sF12) ),
introduced(definition,[new_symbols(definition,[spl21_73])],[avatar_definition]) ).
fof(f1292,plain,
( in(sK4(sK0(sF20,sF20,sF17)),sF12)
| ~ spl21_73 ),
inference(avatar_component_clause,[],[f1291]) ).
fof(f1293,plain,
( ~ in(sK4(sK0(sF20,sF20,sF17)),sF12)
| spl21_73 ),
inference(avatar_component_clause,[],[f1291]) ).
fof(f1295,definition,
( spl21_74
<=> in(sK0(sF20,sF20,sF17),sF17) ),
introduced(definition,[new_symbols(definition,[spl21_74])],[avatar_definition]) ).
fof(f1296,plain,
( ~ in(sK0(sF20,sF20,sF17),sF17)
| spl21_74 ),
inference(avatar_component_clause,[],[f1295]) ).
fof(f1297,plain,
( in(sK0(sF20,sF20,sF17),sF17)
| ~ spl21_74 ),
inference(avatar_component_clause,[],[f1295]) ).
fof(f1298,plain,
( ~ spl21_73
| ~ spl21_64
| spl21_74
| spl21_1 ),
inference(avatar_split_clause,[],[f900,f107,f1295,f1249,f1291]) ).
fof(f1310,plain,
( spl21_64
| ~ spl21_71
| spl21_1 ),
inference(avatar_split_clause,[],[f896,f107,f1281,f1249]) ).
fof(f1311,plain,
( spl21_64
| ~ spl21_72
| spl21_1 ),
inference(avatar_split_clause,[],[f895,f107,f1286,f1249]) ).
fof(f1312,plain,
( spl21_64
| ~ spl21_74
| spl21_1 ),
inference(avatar_split_clause,[],[f894,f107,f1295,f1249]) ).
fof(f1316,plain,
( spl21_68
| ~ spl21_71
| spl21_1 ),
inference(avatar_split_clause,[],[f890,f107,f1281,f1267]) ).
fof(f1317,plain,
( spl21_65
| ~ spl21_72
| spl21_1 ),
inference(avatar_split_clause,[],[f889,f107,f1286,f1253]) ).
fof(f1318,plain,
( spl21_73
| ~ spl21_74
| spl21_1 ),
inference(avatar_split_clause,[],[f888,f107,f1295,f1291]) ).
fof(f1351,plain,
( in(sK0(sF20,sF20,sF17),sF19)
| sF17 = sF20
| in(sK0(sF20,sF20,sF17),sF18)
| spl21_74 ),
inference(resolution,[],[f1296,f760]) ).
fof(f1352,plain,
( sF17 = sF20
| in(sK0(sF20,sF20,sF17),sF18)
| spl21_72
| spl21_74 ),
inference(forward_subsumption_resolution,[],[f1351,f1287]) ).
fof(f1353,plain,
( in(sK0(sF20,sF20,sF17),sF18)
| spl21_1
| spl21_72
| spl21_74 ),
inference(forward_subsumption_resolution,[],[f1352,f109]) ).
fof(f1354,plain,
( $false
| spl21_1
| spl21_71
| spl21_72
| spl21_74 ),
inference(forward_subsumption_resolution,[],[f1353,f1282]) ).
fof(f1355,plain,
( spl21_1
| spl21_71
| spl21_72
| spl21_74 ),
inference(avatar_contradiction_clause,[],[f1354]) ).
fof(f1366,plain,
( in(sK4(sK0(sF20,sF20,sF17)),sF12)
| ~ spl21_68 ),
inference(resolution,[],[f1268,f123]) ).
fof(f1367,plain,
( $false
| ~ spl21_68
| spl21_73 ),
inference(forward_subsumption_resolution,[],[f1366,f1293]) ).
fof(f1368,plain,
( ~ spl21_68
| spl21_73 ),
inference(avatar_contradiction_clause,[],[f1367]) ).
fof(f1383,plain,
( in(sK4(sK0(sF20,sF20,sF17)),sF12)
| ~ spl21_65 ),
inference(resolution,[],[f1254,f124]) ).
fof(f1384,plain,
( $false
| ~ spl21_65
| spl21_73 ),
inference(forward_subsumption_resolution,[],[f1383,f1293]) ).
fof(f1385,plain,
( ~ spl21_65
| spl21_73 ),
inference(avatar_contradiction_clause,[],[f1384]) ).
fof(f1386,plain,
( in(sK4(sK0(sF20,sF20,sF17)),sK10)
| in(sK4(sK0(sF20,sF20,sF17)),sK9)
| ~ spl21_73 ),
inference(resolution,[],[f1292,f125]) ).
fof(f1387,plain,
( ~ in(sK0(sF20,sF20,sF17),sF20)
| sF17 = set_union2(sF20,sF20)
| ~ spl21_74 ),
inference(resolution,[],[f1297,f48]) ).
fof(f1391,plain,
( sF17 = set_union2(sF20,sF20)
| ~ spl21_66
| ~ spl21_74 ),
inference(forward_subsumption_resolution,[],[f1387,f1259]) ).
fof(f1393,plain,
( sF17 = sF20
| ~ spl21_66
| ~ spl21_74 ),
inference(forward_demodulation,[],[f1391,f53]) ).
fof(f1396,plain,
( $false
| spl21_1
| ~ spl21_66
| ~ spl21_74 ),
inference(forward_subsumption_resolution,[],[f1393,f109]) ).
fof(f1397,plain,
( spl21_1
| ~ spl21_66
| ~ spl21_74 ),
inference(avatar_contradiction_clause,[],[f1396]) ).
fof(f1402,plain,
( in(sK4(sK0(sF20,sF20,sF17)),sK9)
| spl21_65
| ~ spl21_73 ),
inference(forward_subsumption_resolution,[],[f1386,f1255]) ).
fof(f1403,plain,
( $false
| spl21_65
| spl21_68
| ~ spl21_73 ),
inference(forward_subsumption_resolution,[],[f1402,f1269]) ).
fof(f1404,plain,
( spl21_65
| spl21_68
| ~ spl21_73 ),
inference(avatar_contradiction_clause,[],[f1403]) ).
fof(f2921,plain,
( ! [X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sF17)
| ~ in(X1,sK9)
| ~ in(X0,sK11) )
| ~ spl21_1 ),
inference(superposition,[],[f226,f108]) ).
fof(f2922,plain,
( ! [X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sF17)
| ~ in(X1,sK10)
| ~ in(X0,sK11) )
| ~ spl21_1 ),
inference(superposition,[],[f240,f108]) ).
fof(f2988,plain,
( ! [X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sF13)
| ~ in(X1,sK11)
| ~ in(X0,sK9) )
| ~ spl21_1 ),
inference(resolution,[],[f2921,f129]) ).
fof(f3013,plain,
( ! [X0,X1] :
( in(unordered_pair(unordered_pair(X0,X1),singleton(X0)),sF13)
| ~ in(X1,sK11)
| ~ in(X0,sK10) )
| ~ spl21_1 ),
inference(resolution,[],[f2922,f129]) ).
fof(f17855,plain,
! [X0] :
( in(sK0(sF16,X0,sF13),sF15)
| in(sK0(sF16,X0,sF13),X0)
| sF13 = set_union2(sF16,X0)
| in(sK0(sF16,X0,sF13),sF14)
| sK0(sF16,X0,sF13) = unordered_pair(unordered_pair(sK3(sK0(sF16,X0,sF13)),sK4(sK0(sF16,X0,sF13))),singleton(sK3(sK0(sF16,X0,sF13)))) ),
inference(resolution,[],[f720,f165]) ).
fof(f17911,plain,
! [X0] :
( in(sK0(sF16,X0,sF13),X0)
| sF13 = set_union2(sF16,X0)
| in(sK0(sF16,X0,sF13),sF14)
| sK0(sF16,X0,sF13) = unordered_pair(unordered_pair(sK3(sK0(sF16,X0,sF13)),sK4(sK0(sF16,X0,sF13))),singleton(sK3(sK0(sF16,X0,sF13)))) ),
inference(forward_subsumption_resolution,[],[f17855,f161]) ).
fof(f17939,plain,
! [X0] :
( in(sK0(sF16,X0,sF13),X0)
| sF13 = set_union2(sF16,X0)
| sK0(sF16,X0,sF13) = unordered_pair(unordered_pair(sK3(sK0(sF16,X0,sF13)),sK4(sK0(sF16,X0,sF13))),singleton(sK3(sK0(sF16,X0,sF13)))) ),
inference(forward_subsumption_resolution,[],[f17911,f160]) ).
fof(f18028,plain,
( sF13 = set_union2(sF16,sF16)
| sK0(sF16,sF16,sF13) = unordered_pair(unordered_pair(sK3(sK0(sF16,sF16,sF13)),sK4(sK0(sF16,sF16,sF13))),singleton(sK3(sK0(sF16,sF16,sF13))))
| in(sK0(sF16,sF16,sF13),sF15)
| in(sK0(sF16,sF16,sF13),sF14) ),
inference(resolution,[],[f17939,f119]) ).
fof(f18052,plain,
( sF13 = set_union2(sF16,sF16)
| sK0(sF16,sF16,sF13) = unordered_pair(unordered_pair(sK3(sK0(sF16,sF16,sF13)),sK4(sK0(sF16,sF16,sF13))),singleton(sK3(sK0(sF16,sF16,sF13))))
| in(sK0(sF16,sF16,sF13),sF14) ),
inference(forward_subsumption_resolution,[],[f18028,f161]) ).
fof(f18094,plain,
( sF13 = set_union2(sF16,sF16)
| sK0(sF16,sF16,sF13) = unordered_pair(unordered_pair(sK3(sK0(sF16,sF16,sF13)),sK4(sK0(sF16,sF16,sF13))),singleton(sK3(sK0(sF16,sF16,sF13)))) ),
inference(forward_subsumption_resolution,[],[f18052,f160]) ).
fof(f18123,plain,
( sF13 = sF16
| sK0(sF16,sF16,sF13) = unordered_pair(unordered_pair(sK3(sK0(sF16,sF16,sF13)),sK4(sK0(sF16,sF16,sF13))),singleton(sK3(sK0(sF16,sF16,sF13)))) ),
inference(forward_demodulation,[],[f18094,f53]) ).
fof(f18132,plain,
( sK0(sF16,sF16,sF13) = unordered_pair(unordered_pair(sK3(sK0(sF16,sF16,sF13)),sK4(sK0(sF16,sF16,sF13))),singleton(sK3(sK0(sF16,sF16,sF13))))
| spl21_2 ),
inference(forward_subsumption_resolution,[],[f18123,f113]) ).
fof(f18152,plain,
( ! [X0,X1] :
( ~ in(sK0(sF16,sF16,sF13),cartesian_product2(X0,X1))
| in(sK3(sK0(sF16,sF16,sF13)),X0) )
| spl21_2 ),
inference(superposition,[],[f72,f18132]) ).
fof(f18153,plain,
( ! [X0,X1] :
( ~ in(sK0(sF16,sF16,sF13),cartesian_product2(X0,X1))
| in(sK4(sK0(sF16,sF16,sF13)),X1) )
| spl21_2 ),
inference(superposition,[],[f73,f18132]) ).
fof(f18162,plain,
( ~ in(sK0(sF16,sF16,sF13),sF14)
| in(sK4(sK0(sF16,sF16,sF13)),sK11)
| spl21_2 ),
inference(superposition,[],[f138,f18132]) ).
fof(f18167,plain,
( ~ in(sK0(sF16,sF16,sF13),sF13)
| in(sK4(sK0(sF16,sF16,sF13)),sK11)
| spl21_2 ),
inference(superposition,[],[f143,f18132]) ).
fof(f18169,plain,
( ~ in(sK0(sF16,sF16,sF13),sF15)
| in(sK3(sK0(sF16,sF16,sF13)),sK10)
| spl21_2 ),
inference(superposition,[],[f145,f18132]) ).
fof(f18173,plain,
( ~ in(sK0(sF16,sF16,sF13),sF13)
| in(sK3(sK0(sF16,sF16,sF13)),sF12)
| spl21_2 ),
inference(superposition,[],[f149,f18132]) ).
fof(f18181,plain,
( in(sK0(sF16,sF16,sF13),sF16)
| ~ in(sK4(sK0(sF16,sF16,sF13)),sK11)
| ~ in(sK3(sK0(sF16,sF16,sF13)),sK9)
| spl21_2 ),
inference(superposition,[],[f233,f18132]) ).
fof(f18183,plain,
( in(sK0(sF16,sF16,sF13),sF16)
| ~ in(sK4(sK0(sF16,sF16,sF13)),sK11)
| ~ in(sK3(sK0(sF16,sF16,sF13)),sK10)
| spl21_2 ),
inference(superposition,[],[f247,f18132]) ).
fof(f18187,plain,
( in(sK0(sF16,sF16,sF13),sF13)
| ~ in(sK4(sK0(sF16,sF16,sF13)),sK11)
| ~ in(sK3(sK0(sF16,sF16,sF13)),sK9)
| ~ spl21_1
| spl21_2 ),
inference(superposition,[],[f2988,f18132]) ).
fof(f18188,plain,
( in(sK0(sF16,sF16,sF13),sF13)
| ~ in(sK4(sK0(sF16,sF16,sF13)),sK11)
| ~ in(sK3(sK0(sF16,sF16,sF13)),sK10)
| ~ spl21_1
| spl21_2 ),
inference(superposition,[],[f3013,f18132]) ).
fof(f18437,definition,
( spl21_608
<=> in(sK3(sK0(sF16,sF16,sF13)),sK10) ),
introduced(definition,[new_symbols(definition,[spl21_608])],[avatar_definition]) ).
fof(f18439,plain,
( ~ in(sK3(sK0(sF16,sF16,sF13)),sK10)
| spl21_608 ),
inference(avatar_component_clause,[],[f18437]) ).
fof(f18441,definition,
( spl21_609
<=> in(sK4(sK0(sF16,sF16,sF13)),sK11) ),
introduced(definition,[new_symbols(definition,[spl21_609])],[avatar_definition]) ).
fof(f18442,plain,
( in(sK4(sK0(sF16,sF16,sF13)),sK11)
| ~ spl21_609 ),
inference(avatar_component_clause,[],[f18441]) ).
fof(f18445,definition,
( spl21_610
<=> in(sK0(sF16,sF16,sF13),sF13) ),
introduced(definition,[new_symbols(definition,[spl21_610])],[avatar_definition]) ).
fof(f18446,plain,
( ~ in(sK0(sF16,sF16,sF13),sF13)
| spl21_610 ),
inference(avatar_component_clause,[],[f18445]) ).
fof(f18447,plain,
( in(sK0(sF16,sF16,sF13),sF13)
| ~ spl21_610 ),
inference(avatar_component_clause,[],[f18445]) ).
fof(f18448,plain,
( ~ spl21_608
| ~ spl21_609
| spl21_610
| ~ spl21_1
| spl21_2 ),
inference(avatar_split_clause,[],[f18188,f111,f107,f18445,f18441,f18437]) ).
fof(f18454,definition,
( spl21_611
<=> in(sK0(sF16,sF16,sF13),sF16) ),
introduced(definition,[new_symbols(definition,[spl21_611])],[avatar_definition]) ).
fof(f18455,plain,
( ~ in(sK0(sF16,sF16,sF13),sF16)
| spl21_611 ),
inference(avatar_component_clause,[],[f18454]) ).
fof(f18456,plain,
( in(sK0(sF16,sF16,sF13),sF16)
| ~ spl21_611 ),
inference(avatar_component_clause,[],[f18454]) ).
fof(f18457,plain,
( ~ spl21_608
| ~ spl21_609
| spl21_611
| spl21_2 ),
inference(avatar_split_clause,[],[f18183,f111,f18454,f18441,f18437]) ).
fof(f18462,definition,
( spl21_612
<=> in(sK3(sK0(sF16,sF16,sF13)),sF12) ),
introduced(definition,[new_symbols(definition,[spl21_612])],[avatar_definition]) ).
fof(f18463,plain,
( in(sK3(sK0(sF16,sF16,sF13)),sF12)
| ~ spl21_612 ),
inference(avatar_component_clause,[],[f18462]) ).
fof(f18471,plain,
( spl21_612
| ~ spl21_610
| spl21_2 ),
inference(avatar_split_clause,[],[f18173,f111,f18445,f18462]) ).
fof(f18477,plain,
( spl21_609
| ~ spl21_610
| spl21_2 ),
inference(avatar_split_clause,[],[f18167,f111,f18445,f18441]) ).
fof(f18483,definition,
( spl21_613
<=> in(sK0(sF16,sF16,sF13),sF14) ),
introduced(definition,[new_symbols(definition,[spl21_613])],[avatar_definition]) ).
fof(f18484,plain,
( in(sK0(sF16,sF16,sF13),sF14)
| ~ spl21_613 ),
inference(avatar_component_clause,[],[f18483]) ).
fof(f18485,plain,
( ~ in(sK0(sF16,sF16,sF13),sF14)
| spl21_613 ),
inference(avatar_component_clause,[],[f18483]) ).
fof(f18486,plain,
( spl21_609
| ~ spl21_613
| spl21_2 ),
inference(avatar_split_clause,[],[f18162,f111,f18483,f18441]) ).
fof(f18772,plain,
( ~ in(sK0(sF16,sF16,sF13),sF15)
| in(sK4(sK0(sF16,sF16,sF13)),sK11)
| spl21_2 ),
inference(superposition,[],[f18153,f94]) ).
fof(f18787,plain,
( ~ in(sK0(sF16,sF16,sF13),sF14)
| in(sK3(sK0(sF16,sF16,sF13)),sK9)
| spl21_2 ),
inference(superposition,[],[f18152,f92]) ).
fof(f22083,plain,
( in(sK3(sK0(sF16,sF16,sF13)),sK9)
| spl21_2
| ~ spl21_613 ),
inference(forward_subsumption_resolution,[],[f18787,f18484]) ).
fof(f22107,plain,
( in(sK0(sF16,sF16,sF13),sF16)
| ~ in(sK3(sK0(sF16,sF16,sF13)),sK9)
| spl21_2
| ~ spl21_609 ),
inference(forward_subsumption_resolution,[],[f18181,f18442]) ).
fof(f22108,plain,
( ~ in(sK4(sK0(sF16,sF16,sF13)),sK11)
| ~ in(sK3(sK0(sF16,sF16,sF13)),sK9)
| ~ spl21_1
| spl21_2
| spl21_610 ),
inference(forward_subsumption_resolution,[],[f18187,f18446]) ).
fof(f22110,plain,
( ~ in(sK3(sK0(sF16,sF16,sF13)),sK9)
| ~ spl21_1
| spl21_2
| ~ spl21_609
| spl21_610 ),
inference(forward_subsumption_resolution,[],[f22108,f18442]) ).
fof(f22112,plain,
( $false
| ~ spl21_1
| spl21_2
| ~ spl21_609
| spl21_610
| ~ spl21_613 ),
inference(forward_subsumption_resolution,[],[f22110,f22083]) ).
fof(f22113,plain,
( ~ spl21_1
| spl21_2
| ~ spl21_609
| spl21_610
| ~ spl21_613 ),
inference(avatar_contradiction_clause,[],[f22112]) ).
fof(f22114,plain,
( ~ in(sK0(sF16,sF16,sF13),sF16)
| sF13 = set_union2(sF16,sF16)
| ~ spl21_610 ),
inference(resolution,[],[f18447,f48]) ).
fof(f22119,plain,
( sF13 = set_union2(sF16,sF16)
| ~ spl21_610
| ~ spl21_611 ),
inference(forward_subsumption_resolution,[],[f22114,f18456]) ).
fof(f22121,plain,
( sF13 = sF16
| ~ spl21_610
| ~ spl21_611 ),
inference(forward_demodulation,[],[f22119,f53]) ).
fof(f22124,plain,
( $false
| spl21_2
| ~ spl21_610
| ~ spl21_611 ),
inference(forward_subsumption_resolution,[],[f22121,f113]) ).
fof(f22125,plain,
( spl21_2
| ~ spl21_610
| ~ spl21_611 ),
inference(avatar_contradiction_clause,[],[f22124]) ).
fof(f22132,plain,
( ~ in(sK3(sK0(sF16,sF16,sF13)),sK9)
| spl21_2
| ~ spl21_609
| spl21_611 ),
inference(forward_subsumption_resolution,[],[f22107,f18455]) ).
fof(f22193,plain,
( in(sK3(sK0(sF16,sF16,sF13)),sK10)
| in(sK3(sK0(sF16,sF16,sF13)),sK9)
| ~ spl21_612 ),
inference(resolution,[],[f18463,f125]) ).
fof(f22194,plain,
( in(sK3(sK0(sF16,sF16,sF13)),sK9)
| spl21_608
| ~ spl21_612 ),
inference(forward_subsumption_resolution,[],[f22193,f18439]) ).
fof(f22195,plain,
( $false
| spl21_2
| spl21_608
| ~ spl21_609
| spl21_611
| ~ spl21_612 ),
inference(forward_subsumption_resolution,[],[f22194,f22132]) ).
fof(f22196,plain,
( spl21_2
| spl21_608
| ~ spl21_609
| spl21_611
| ~ spl21_612 ),
inference(avatar_contradiction_clause,[],[f22195]) ).
fof(f22216,plain,
( in(sK0(sF16,sF16,sF13),sF15)
| in(sK0(sF16,sF16,sF13),sF14)
| ~ spl21_611 ),
inference(resolution,[],[f18456,f119]) ).
fof(f22217,plain,
( in(sK0(sF16,sF16,sF13),sF15)
| ~ spl21_611
| spl21_613 ),
inference(forward_subsumption_resolution,[],[f22216,f18485]) ).
fof(f22622,plain,
( ~ in(sK0(sF16,sF16,sF13),sF15)
| spl21_2
| spl21_608 ),
inference(forward_subsumption_resolution,[],[f18169,f18439]) ).
fof(f22625,definition,
( spl21_783
<=> in(sK0(sF16,sF16,sF13),sF15) ),
introduced(definition,[new_symbols(definition,[spl21_783])],[avatar_definition]) ).
fof(f22627,plain,
( ~ in(sK0(sF16,sF16,sF13),sF15)
| spl21_783 ),
inference(avatar_component_clause,[],[f22625]) ).
fof(f22728,plain,
( spl21_609
| ~ spl21_783
| spl21_2 ),
inference(avatar_split_clause,[],[f18772,f111,f22625,f18441]) ).
fof(f22729,plain,
( spl21_783
| ~ spl21_611
| spl21_613 ),
inference(avatar_split_clause,[],[f22217,f18483,f18454,f22625]) ).
fof(f22964,plain,
( ~ spl21_783
| spl21_2
| spl21_608 ),
inference(avatar_split_clause,[],[f22622,f18437,f111,f22625]) ).
fof(f23415,plain,
( in(sK0(sF16,sF16,sF13),sF15)
| in(sK0(sF16,sF16,sF13),sF13)
| sF13 = set_union2(sF16,sF16)
| in(sK0(sF16,sF16,sF13),sF14)
| spl21_611 ),
inference(resolution,[],[f18455,f720]) ).
fof(f23416,plain,
( in(sK0(sF16,sF16,sF13),sF13)
| sF13 = set_union2(sF16,sF16)
| in(sK0(sF16,sF16,sF13),sF14)
| spl21_611
| spl21_783 ),
inference(forward_subsumption_resolution,[],[f23415,f22627]) ).
fof(f23417,plain,
( sF13 = set_union2(sF16,sF16)
| in(sK0(sF16,sF16,sF13),sF14)
| spl21_610
| spl21_611
| spl21_783 ),
inference(forward_subsumption_resolution,[],[f23416,f18446]) ).
fof(f23418,plain,
( sF13 = set_union2(sF16,sF16)
| spl21_610
| spl21_611
| spl21_613
| spl21_783 ),
inference(forward_subsumption_resolution,[],[f23417,f18485]) ).
fof(f23419,plain,
( sF13 = sF16
| spl21_610
| spl21_611
| spl21_613
| spl21_783 ),
inference(forward_demodulation,[],[f23418,f53]) ).
fof(f23420,plain,
( $false
| spl21_2
| spl21_610
| spl21_611
| spl21_613
| spl21_783 ),
inference(forward_subsumption_resolution,[],[f23419,f113]) ).
fof(f23421,plain,
( spl21_2
| spl21_610
| spl21_611
| spl21_613
| spl21_783 ),
inference(avatar_contradiction_clause,[],[f23420]) ).
cnf(s1,plain,
( ~ spl21_1
| ~ spl21_2 ),
inference(sat_conversion,[],[f114]) ).
cnf(s83,plain,
( spl21_1
| ~ spl21_64
| ~ spl21_65
| spl21_66 ),
inference(sat_conversion,[],[f1260]) ).
cnf(s85,plain,
( spl21_1
| ~ spl21_64
| spl21_66
| ~ spl21_68 ),
inference(sat_conversion,[],[f1270]) ).
cnf(s87,plain,
( spl21_1
| ~ spl21_64
| ~ spl21_68
| spl21_71 ),
inference(sat_conversion,[],[f1284]) ).
cnf(s88,plain,
( spl21_1
| ~ spl21_64
| ~ spl21_65
| spl21_72 ),
inference(sat_conversion,[],[f1289]) ).
cnf(s89,plain,
( spl21_1
| ~ spl21_64
| ~ spl21_73
| spl21_74 ),
inference(sat_conversion,[],[f1298]) ).
cnf(s93,plain,
( spl21_1
| spl21_64
| ~ spl21_71 ),
inference(sat_conversion,[],[f1310]) ).
cnf(s94,plain,
( spl21_1
| spl21_64
| ~ spl21_72 ),
inference(sat_conversion,[],[f1311]) ).
cnf(s95,plain,
( spl21_1
| spl21_64
| ~ spl21_74 ),
inference(sat_conversion,[],[f1312]) ).
cnf(s99,plain,
( spl21_1
| spl21_68
| ~ spl21_71 ),
inference(sat_conversion,[],[f1316]) ).
cnf(s100,plain,
( spl21_1
| spl21_65
| ~ spl21_72 ),
inference(sat_conversion,[],[f1317]) ).
cnf(s101,plain,
( spl21_1
| spl21_73
| ~ spl21_74 ),
inference(sat_conversion,[],[f1318]) ).
cnf(s110,plain,
( spl21_1
| spl21_71
| spl21_72
| spl21_74 ),
inference(sat_conversion,[],[f1355]) ).
cnf(s111,plain,
( ~ spl21_68
| spl21_73 ),
inference(sat_conversion,[],[f1368]) ).
cnf(s114,plain,
( ~ spl21_65
| spl21_73 ),
inference(sat_conversion,[],[f1385]) ).
cnf(s116,plain,
( spl21_1
| ~ spl21_66
| ~ spl21_74 ),
inference(sat_conversion,[],[f1397]) ).
cnf(s119,plain,
( spl21_65
| spl21_68
| ~ spl21_73 ),
inference(sat_conversion,[],[f1404]) ).
cnf(s1790,plain,
( ~ spl21_1
| spl21_2
| ~ spl21_608
| ~ spl21_609
| spl21_610 ),
inference(sat_conversion,[],[f18448]) ).
cnf(s1791,plain,
( spl21_2
| ~ spl21_608
| ~ spl21_609
| spl21_611 ),
inference(sat_conversion,[],[f18457]) ).
cnf(s1793,plain,
( spl21_2
| ~ spl21_610
| spl21_612 ),
inference(sat_conversion,[],[f18471]) ).
cnf(s1794,plain,
( spl21_2
| spl21_609
| ~ spl21_610 ),
inference(sat_conversion,[],[f18477]) ).
cnf(s1795,plain,
( spl21_2
| spl21_609
| ~ spl21_613 ),
inference(sat_conversion,[],[f18486]) ).
cnf(s2304,plain,
( ~ spl21_1
| spl21_2
| ~ spl21_609
| spl21_610
| ~ spl21_613 ),
inference(sat_conversion,[],[f22113]) ).
cnf(s2306,plain,
( spl21_2
| ~ spl21_610
| ~ spl21_611 ),
inference(sat_conversion,[],[f22125]) ).
cnf(s2318,plain,
( spl21_2
| spl21_608
| ~ spl21_609
| spl21_611
| ~ spl21_612 ),
inference(sat_conversion,[],[f22196]) ).
cnf(s2351,plain,
( spl21_2
| spl21_609
| ~ spl21_783 ),
inference(sat_conversion,[],[f22728]) ).
cnf(s2352,plain,
( ~ spl21_611
| spl21_613
| spl21_783 ),
inference(sat_conversion,[],[f22729]) ).
cnf(s2367,plain,
( spl21_2
| spl21_608
| ~ spl21_783 ),
inference(sat_conversion,[],[f22964]) ).
cnf(s2405,plain,
( spl21_2
| spl21_610
| spl21_611
| spl21_613
| spl21_783 ),
inference(sat_conversion,[],[f23421]) ).
cnf(s2406,plain,
( spl21_64
| spl21_1 ),
inference(rat,[],[s110,s93,s94,s95]) ).
cnf(s2407,plain,
( spl21_72
| spl21_71
| spl21_1 ),
inference(rat,[],[s119,s101,s88,s110,s87,s2406]) ).
cnf(s2408,plain,
( ~ spl21_65
| spl21_1 ),
inference(rat,[],[s116,s89,s83,s114,s2406]) ).
cnf(s2409,plain,
spl21_1,
inference(rat,[],[s116,s89,s85,s111,s99,s2407,s100,s2408,s2406]) ).
cnf(s2410,plain,
~ spl21_2,
inference(rat,[],[s1,s2409]) ).
cnf(s2411,plain,
( spl21_609
| spl21_783 ),
inference(rat,[],[s2405,s2352,s1794,s1795,s2410]) ).
cnf(s2412,plain,
( spl21_610
| spl21_783 ),
inference(rat,[],[s2405,s2352,s2304,s2411,s2410,s2409]) ).
cnf(s2413,plain,
spl21_608,
inference(rat,[],[s2318,s1793,s2306,s2412,s2411,s2367,s2410]) ).
cnf(s2414,plain,
~ spl21_609,
inference(rat,[],[s2306,s1790,s1791,s2410,s2409,s2413]) ).
cnf(s2415,plain,
~ spl21_783,
inference(rat,[],[s2351,s2410,s2414]) ).
cnf(s2418,plain,
$false,
inference(rat,[],[s2411,s2415,s2414]) ).
fof(f23422,plain,
$false,
inference(avatar_sat_refutation,[],[s2418]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SET967+1 : TPTP v9.3.1. Released v3.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.38 % Computer : n004.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 28 03:17:07 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.41 Running first-order theorem proving
% 0.11/0.41 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 11.55/2.53 % (4117577)Detected formulas, will run a generic FOF schedule.
% 11.55/2.53 % (4117586)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=1409176048:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 11.55/2.53 % (4117586)Instruction limit reached!
% 11.55/2.53 % (4117586)------------------------------
% 11.55/2.53 % (4117586)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.55/2.53 % (4117586)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.55/2.53 % (4117586)CaDiCaL version: 2.1.3
% 11.55/2.53 % (4117586)Termination reason: Instruction limit
% 11.55/2.53 % (4117586)Termination phase: Saturation
% 11.55/2.53 % (4117586)Time elapsed: 0.039 s
% 11.55/2.53 % (4117586)Peak memory usage: 88 MB
% 11.55/2.53 % (4117586)Instructions burned: 119 (million)
% 11.55/2.53 % (4117583)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=3857476548:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 11.55/2.53 % (4117585)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1873777835:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 11.55/2.53 % (4117582)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2097922058:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 11.55/2.53 % (4117588)dis-21_1_sil=8000:lcm=predicate:random_seed=2442285585:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 11.55/2.53 % (4117584)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=218522377:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 11.55/2.53 % (4117587)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=1586017793:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 11.55/2.53 % (4117585)Refutation not found, incomplete strategy
% 11.55/2.53 % (4117585)------------------------------
% 11.55/2.53 % (4117585)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.55/2.53 % (4117585)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.55/2.53 % (4117585)CaDiCaL version: 2.1.3
% 11.55/2.53 % (4117585)Termination reason: Refutation not found, incomplete strategy
% 11.55/2.53 % (4117585)Time elapsed: 0.002 s
% 11.55/2.53 % (4117585)Peak memory usage: 88 MB
% 11.55/2.53 % (4117585)Instructions burned: 1 (million)
% 11.55/2.53 % (4117588)Instruction limit reached!
% 11.55/2.53 % (4117588)------------------------------
% 11.55/2.53 % (4117588)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.55/2.53 % (4117588)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.55/2.53 % (4117588)CaDiCaL version: 2.1.3
% 11.55/2.53 % (4117588)Termination reason: Instruction limit
% 11.55/2.53 % (4117588)Termination phase: Saturation
% 11.55/2.53 % (4117588)Time elapsed: 0.072 s
% 11.55/2.53 % (4117588)Peak memory usage: 89 MB
% 11.55/2.53 % (4117588)Instructions burned: 130 (million)
% 11.55/2.53 % (4117587)Instruction limit reached!
% 11.55/2.53 % (4117587)------------------------------
% 11.55/2.53 % (4117587)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.55/2.53 % (4117587)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.55/2.53 % (4117587)CaDiCaL version: 2.1.3
% 11.55/2.53 % (4117587)Termination reason: Instruction limit
% 11.55/2.53 % (4117587)Termination phase: Saturation
% 11.55/2.53 % (4117587)Time elapsed: 0.088 s
% 11.55/2.53 % (4117587)Peak memory usage: 89 MB
% 11.55/2.53 % (4117587)Instructions burned: 140 (million)
% 11.55/2.53 % (4117590)lrs+10_1_sil=8000:sp=occurrence:random_seed=2933147892:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 11.55/2.53 % (4117590)Instruction limit reached!
% 11.55/2.53 % (4117590)------------------------------
% 11.55/2.53 % (4117590)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.55/2.53 % (4117590)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.55/2.53 % (4117590)CaDiCaL version: 2.1.3
% 11.55/2.53 % (4117590)Termination reason: Instruction limit
% 11.55/2.53 % (4117590)Termination phase: Saturation
% 11.55/2.53 % (4117590)Time elapsed: 0.086 s
% 11.55/2.53 % (4117590)Peak memory usage: 90 MB
% 11.55/2.53 % (4117590)Instructions burned: 288 (million)
% 12.61/2.75 % (4117597)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2866881548:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 12.61/2.75 % (4117597)Refutation not found, incomplete strategy
% 12.61/2.75 % (4117597)------------------------------
% 12.61/2.75 % (4117597)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.61/2.75 % (4117597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.61/2.75 % (4117597)CaDiCaL version: 2.1.3
% 12.61/2.75 % (4117597)Termination reason: Refutation not found, incomplete strategy
% 12.61/2.75 % (4117597)Time elapsed: 0.008 s
% 12.61/2.75 % (4117597)Peak memory usage: 89 MB
% 12.61/2.75 % (4117597)Instructions burned: 11 (million)
% 12.61/2.75 % (4117585)------------------------------
% 12.61/2.75 % (4117585)------------------------------
% 12.61/2.75 % (4117598)lrs+1011_1_sil=32000:sp=occurrence:random_seed=65231591:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 12.61/2.75 % (4117600)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=3510451836:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 12.61/2.75 % (4117600)Instruction limit reached!
% 12.61/2.75 % (4117600)------------------------------
% 12.61/2.75 % (4117600)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.61/2.75 % (4117600)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.61/2.75 % (4117600)CaDiCaL version: 2.1.3
% 12.61/2.75 % (4117600)Termination reason: Instruction limit
% 12.61/2.75 % (4117600)Termination phase: Saturation
% 12.61/2.75 % (4117600)Time elapsed: 0.073 s
% 12.61/2.75 % (4117600)Peak memory usage: 90 MB
% 12.61/2.75 % (4117600)Instructions burned: 249 (million)
% 12.61/2.75 % (4117603)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2860380827:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 12.61/2.75 % (4117603)Refutation not found, incomplete strategy
% 12.61/2.75 % (4117603)------------------------------
% 12.61/2.75 % (4117603)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.61/2.75 % (4117603)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.61/2.75 % (4117603)CaDiCaL version: 2.1.3
% 12.61/2.75 % (4117603)Termination reason: Refutation not found, incomplete strategy
% 12.61/2.75 % (4117603)Time elapsed: 0.003 s
% 12.61/2.75 % (4117603)Peak memory usage: 88 MB
% 12.61/2.75 % (4117603)Instructions burned: 2 (million)
% 12.61/2.75 % (4117598)Instruction limit reached!
% 12.61/2.75 % (4117598)------------------------------
% 12.61/2.75 % (4117598)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.61/2.75 % (4117598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.61/2.75 % (4117598)CaDiCaL version: 2.1.3
% 12.61/2.75 % (4117598)Termination reason: Instruction limit
% 12.61/2.75 % (4117598)Termination phase: Saturation
% 12.61/2.75 % (4117598)Time elapsed: 0.196 s
% 12.61/2.75 % (4117598)Peak memory usage: 90 MB
% 12.61/2.75 % (4117598)Instructions burned: 325 (million)
% 12.61/2.75 % (4117597)------------------------------
% 12.61/2.75 % (4117597)------------------------------
% 12.61/2.75 % (4117605)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=331654026:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 12.61/2.75 % (4117607)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=1618710598:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 12.61/2.75 % (4117608)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1731715041:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 12.61/2.75 % (4117608)Refutation not found, incomplete strategy
% 12.61/2.75 % (4117608)------------------------------
% 12.61/2.75 % (4117608)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.61/2.75 % (4117608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.61/2.75 % (4117608)CaDiCaL version: 2.1.3
% 12.61/2.75 % (4117608)Termination reason: Refutation not found, incomplete strategy
% 12.61/2.75 % (4117608)Time elapsed: 0.002 s
% 12.61/2.75 % (4117608)Peak memory usage: 88 MB
% 12.61/2.75 % (4117608)Instructions burned: 1 (million)
% 12.61/2.75 % (4117603)------------------------------
% 12.61/2.75 % (4117603)------------------------------
% 12.61/2.75 % (4117607)Instruction limit reached!
% 12.61/2.75 % (4117607)------------------------------
% 12.61/2.75 % (4117607)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.61/2.75 % (4117607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.61/2.75 % (4117607)CaDiCaL version: 2.1.3
% 12.61/2.75 % (4117607)Termination reason: Instruction limit
% 12.61/2.75 % (4117607)Termination phase: Saturation
% 12.61/2.75 % (4117607)Time elapsed: 0.072 s
% 12.61/2.75 % (4117607)Peak memory usage: 89 MB
% 12.61/2.75 % (4117607)Instructions burned: 114 (million)
% 12.61/2.75 % (4117612)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=380353895:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 12.61/2.75 % (4117613)lrs+10_1_sil=8000:sp=occurrence:random_seed=4246751903:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2991 on theBenchmark for (2991ds/907Mi)
% 12.61/2.75 % (4117608)------------------------------
% 12.61/2.75 % (4117608)------------------------------
% 12.61/2.75 % (4117612)Instruction limit reached!
% 12.61/2.75 % (4117612)------------------------------
% 12.61/2.75 % (4117612)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.61/2.75 % (4117612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.61/2.75 % (4117612)CaDiCaL version: 2.1.3
% 12.61/2.75 % (4117612)Termination reason: Instruction limit
% 12.61/2.75 % (4117612)Termination phase: Saturation
% 12.61/2.75 % (4117612)Time elapsed: 0.065 s
% 12.61/2.75 % (4117612)Peak memory usage: 89 MB
% 12.61/2.75 % (4117612)Instructions burned: 115 (million)
% 12.61/2.75 % (4117616)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=154602587:i=437:sd=1:aac=none:ss=included_2989 on theBenchmark for (2989ds/437Mi)
% 12.61/2.75 % (4117616)Refutation not found, incomplete strategy
% 12.61/2.75 % (4117616)------------------------------
% 12.61/2.75 % (4117616)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.61/2.75 % (4117616)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.61/2.75 % (4117616)CaDiCaL version: 2.1.3
% 12.61/2.75 % (4117616)Termination reason: Refutation not found, incomplete strategy
% 12.61/2.75 % (4117616)Time elapsed: 0.002 s
% 12.61/2.75 % (4117616)Peak memory usage: 88 MB
% 12.61/2.75 % (4117616)Instructions burned: 2 (million)
% 12.61/2.75 % (4117617)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3051533658:i=5202:ss=axioms:sgt=16_2989 on theBenchmark for (2989ds/5202Mi)
% 12.61/2.75 % (4117616)------------------------------
% 12.61/2.75 % (4117616)------------------------------
% 12.61/2.75 % (4117613)Instruction limit reached!
% 12.61/2.75 % (4117613)------------------------------
% 12.61/2.75 % (4117613)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.61/2.75 % (4117613)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.61/2.75 % (4117613)CaDiCaL version: 2.1.3
% 12.61/2.75 % (4117613)Termination reason: Instruction limit
% 12.61/2.75 % (4117613)Termination phase: Saturation
% 12.61/2.75 % (4117613)Time elapsed: 0.472 s
% 12.61/2.75 % (4117613)Peak memory usage: 93 MB
% 12.61/2.75 % (4117613)Instructions burned: 908 (million)
% 12.61/2.75 % (4117605)Instruction limit reached!
% 12.61/2.75 % (4117605)------------------------------
% 12.61/2.75 % (4117605)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.61/2.75 % (4117605)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.61/2.75 % (4117605)CaDiCaL version: 2.1.3
% 12.61/2.75 % (4117605)Termination reason: Instruction limit
% 12.61/2.75 % (4117605)Termination phase: Saturation
% 12.61/2.75 % (4117605)Time elapsed: 0.827 s
% 12.61/2.75 % (4117605)Peak memory usage: 141 MB
% 12.61/2.75 % (4117605)Instructions burned: 2351 (million)
% 12.61/2.75 % (4117620)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=500064692:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2985 on theBenchmark for (2985ds/134Mi)
% 12.61/2.75 % (4117621)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=2561586927:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi)
% 12.61/2.75 % (4117582)First to succeed.
% 12.61/2.75 % (4117582)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4117577"
% 12.61/2.75 % (4117622)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=3880524090:st=3:i=13193:sd=3:ss=axioms_2984 on theBenchmark for (2984ds/13193Mi)
% 12.61/2.75 % (4117620)Instruction limit reached!
% 12.61/2.75 % (4117620)------------------------------
% 12.61/2.75 % (4117620)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.61/2.75 % (4117620)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.61/2.75 % (4117620)CaDiCaL version: 2.1.3
% 12.61/2.75 % (4117620)Termination reason: Instruction limit
% 12.61/2.75 % (4117620)Termination phase: Saturation
% 12.61/2.75 % (4117620)Time elapsed: 0.081 s
% 12.61/2.75 % (4117620)Peak memory usage: 91 MB
% 12.61/2.75 % (4117620)Instructions burned: 135 (million)
% 12.61/2.75 % (4117584)Also succeeded, but the first one will report.
% 12.61/2.75 % (4117626)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=1008723023:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2983 on theBenchmark for (2983ds/125Mi)
% 12.61/2.75 % (4117582)Refutation found. Thanks to Tanya!
% 12.61/2.75 % SZS status Theorem for theBenchmark
% 12.61/2.75 % SZS output start Proof for theBenchmark
% See solution above
% 13.96/2.95 % (4117582)------------------------------
% 13.96/2.95 % (4117582)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.96/2.95 % (4117582)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.96/2.95 % (4117582)CaDiCaL version: 2.1.3
% 13.96/2.95 % (4117582)Termination reason: Refutation
% 13.96/2.95 % (4117582)Time elapsed: 1.461 s
% 13.96/2.95 % (4117582)Peak memory usage: 143 MB
% 13.96/2.95 % (4117582)Instructions burned: 2389 (million)
% 13.96/2.95 % (4117582)------------------------------
% 13.96/2.95 % (4117582)------------------------------
% 13.96/2.95 % (4117577)Success in time 1.892 s
% 13.96/2.95 % Vampire exiting
%------------------------------------------------------------------------------