%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : DAT052_1 : TPTP v9.3.1. Released v5.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n003.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 09:47:11 AM UTC 2026
% Result : Theorem 1.15s 1.01s
% Output : Refutation 2.91s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 53
% Syntax : Number of formulae : 179 ( 53 unt; 0 typ; 47 def)
% Number of atoms : 410 ( 135 equ)
% Maximal formula atoms : 6 ( 2 avg)
% Number of connectives : 400 ( 169 ~; 162 |; 28 &)
% ( 33 <=>; 8 =>; 0 <=; 0 <~>)
% Maximal formula depth : 8 ( 3 avg)
% Maximal term depth : 4 ( 2 avg)
% Number arithmetic : 54 ( 0 atm; 40 fun; 14 num; 0 var)
% Number of types : 3 ( 1 usr; 1 ari; 0 dat; 0 cdt)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 36 ( 34 usr; 34 prp; 0-2 aty)
% Number of functors : 23 ( 21 usr; 17 con; 0-2 aty)
% Number of variables : 30 ( 24 !; 6 ?; 30 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
record: $tType ).
tff(func_def_0,type,
length: record > $int ).
tff(func_def_1,type,
next: record > record ).
tff(func_def_2,type,
data: record > $int ).
tff(func_def_3,type,
split1: record > record ).
tff(func_def_4,type,
split2: record > record ).
tff(func_def_8,type,
sK0: record ).
tff(func_def_9,type,
sK1: record ).
tff(func_def_10,type,
sF2: record ).
tff(func_def_11,type,
sF3: record ).
tff(func_def_12,type,
sF4: record ).
tff(func_def_13,type,
sF5: $int ).
tff(func_def_14,type,
sF6: record ).
tff(func_def_15,type,
sF7: $int ).
tff(func_def_16,type,
sF8: $int ).
tff(func_def_17,type,
sF9: $int ).
tff(func_def_18,type,
sF10: $int ).
tff(func_def_19,type,
sF11: record ).
tff(func_def_20,type,
sF12: $int ).
tff(func_def_21,type,
sF13: record ).
tff(func_def_22,type,
sF14: $int ).
tff(func_def_23,type,
sF15: $int ).
tff(pred_def_1,type,
isrecord: record > $o ).
tff(f3,axiom,
! [X0: record] :
( isrecord(X0)
=> ( length(X0) = $sum(length(next(X0)),1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax3) ).
tff(f5,axiom,
! [X0: record] :
( isrecord(X0)
=> isrecord(split1(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax5) ).
tff(f8,axiom,
! [X0: record] :
( ( isrecord(next(X0))
& isrecord(X0) )
=> ( next(split1(X0)) = split1(next(next(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax8) ).
tff(f11,axiom,
! [X0: record] :
( ( isrecord(next(X0))
& isrecord(X0) )
=> isrecord(split2(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax11) ).
tff(f13,axiom,
! [X0: record] :
( ( isrecord(next(X0))
& isrecord(X0) )
=> ( next(split2(X0)) = split2(next(next(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ax13) ).
tff(f14,conjecture,
! [X1: record,X0: record] :
( ( ( $sum(length(split1(X1)),length(split2(X1))) = length(X1) )
& ( X1 = next(next(X0)) )
& isrecord(X0)
& isrecord(next(X0)) )
=> ( $sum(length(split1(X0)),length(split2(X0))) = length(X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
tff(f15,negated_conjecture,
~ ! [X1: record,X0: record] :
( ( ( $sum(length(split1(X1)),length(split2(X1))) = length(X1) )
& ( X1 = next(next(X0)) )
& isrecord(X0)
& isrecord(next(X0)) )
=> ( $sum(length(split1(X0)),length(split2(X0))) = length(X0) ) ),
inference(negated_conjecture,[status(cth)],[f14]) ).
tff(f17,plain,
~ ! [X1: record,X0: record] :
( ( isrecord(next(X1))
& ( next(next(X1)) = X0 )
& isrecord(X1)
& ( length(X0) = $sum(length(split1(X0)),length(split2(X0))) ) )
=> ( $sum(length(split1(X1)),length(split2(X1))) = length(X1) ) ),
inference(rectify,[],[f15]) ).
tff(f18,plain,
! [X0: record] :
( ( next(split1(X0)) = split1(next(next(X0))) )
| ~ isrecord(next(X0))
| ~ isrecord(X0) ),
inference(ennf_transformation,[],[f8]) ).
tff(f19,plain,
! [X0: record] :
( ~ isrecord(next(X0))
| ( next(split1(X0)) = split1(next(next(X0))) )
| ~ isrecord(X0) ),
inference(flattening,[],[f18]) ).
tff(f22,plain,
! [X0: record] :
( ( length(X0) = $sum(length(next(X0)),1) )
| ~ isrecord(X0) ),
inference(ennf_transformation,[],[f3]) ).
tff(f24,plain,
! [X0: record] :
( ~ isrecord(X0)
| isrecord(split1(X0)) ),
inference(ennf_transformation,[],[f5]) ).
tff(f25,plain,
! [X0: record] :
( isrecord(split2(X0))
| ~ isrecord(next(X0))
| ~ isrecord(X0) ),
inference(ennf_transformation,[],[f11]) ).
tff(f26,plain,
! [X0: record] :
( ~ isrecord(X0)
| isrecord(split2(X0))
| ~ isrecord(next(X0)) ),
inference(flattening,[],[f25]) ).
tff(f29,plain,
? [X1: record,X0: record] :
( ( $sum(length(split1(X1)),length(split2(X1))) != length(X1) )
& isrecord(next(X1))
& ( next(next(X1)) = X0 )
& isrecord(X1)
& ( length(X0) = $sum(length(split1(X0)),length(split2(X0))) ) ),
inference(ennf_transformation,[],[f17]) ).
tff(f30,plain,
? [X1: record,X0: record] :
( isrecord(next(X1))
& ( next(next(X1)) = X0 )
& isrecord(X1)
& ( $sum(length(split1(X1)),length(split2(X1))) != length(X1) )
& ( length(X0) = $sum(length(split1(X0)),length(split2(X0))) ) ),
inference(flattening,[],[f29]) ).
tff(f31,plain,
! [X0: record] :
( ( next(split2(X0)) = split2(next(next(X0))) )
| ~ isrecord(next(X0))
| ~ isrecord(X0) ),
inference(ennf_transformation,[],[f13]) ).
tff(f32,plain,
! [X0: record] :
( ( next(split2(X0)) = split2(next(next(X0))) )
| ~ isrecord(X0)
| ~ isrecord(next(X0)) ),
inference(flattening,[],[f31]) ).
tff(f38,plain,
? [X0: record,X1: record] :
( isrecord(next(X0))
& ( next(next(X0)) = X1 )
& isrecord(X0)
& ( length(X0) != $sum(length(split1(X0)),length(split2(X0))) )
& ( $sum(length(split1(X1)),length(split2(X1))) = length(X1) ) ),
inference(rectify,[],[f30]) ).
tff(f39,plain,
( isrecord(next(sK0))
& ( next(next(sK0)) = sK1 )
& isrecord(sK0)
& ( $sum(length(split1(sK0)),length(split2(sK0))) != length(sK0) )
& ( length(sK1) = $sum(length(split1(sK1)),length(split2(sK1))) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK0,sK1]),skolemize(X0,sK0),skolemize(X1,sK1)],[f38]) ).
tff(f40,plain,
! [X0: record] :
( ( next(split2(X0)) = split2(next(next(X0))) )
| ~ isrecord(next(X0))
| ~ isrecord(X0) ),
inference(cnf_transformation,[],[f32]) ).
tff(f43,plain,
! [X0: record] :
( ( length(X0) = $sum(length(next(X0)),1) )
| ~ isrecord(X0) ),
inference(cnf_transformation,[],[f22]) ).
tff(f44,plain,
! [X0: record] :
( isrecord(split2(X0))
| ~ isrecord(next(X0))
| ~ isrecord(X0) ),
inference(cnf_transformation,[],[f26]) ).
tff(f45,plain,
length(sK1) = $sum(length(split1(sK1)),length(split2(sK1))),
inference(cnf_transformation,[],[f39]) ).
tff(f46,plain,
$sum(length(split1(sK0)),length(split2(sK0))) != length(sK0),
inference(cnf_transformation,[],[f39]) ).
tff(f47,plain,
isrecord(sK0),
inference(cnf_transformation,[],[f39]) ).
tff(f48,plain,
next(next(sK0)) = sK1,
inference(cnf_transformation,[],[f39]) ).
tff(f49,plain,
isrecord(next(sK0)),
inference(cnf_transformation,[],[f39]) ).
tff(f55,plain,
! [X0: record] :
( isrecord(split1(X0))
| ~ isrecord(X0) ),
inference(cnf_transformation,[],[f24]) ).
tff(f56,plain,
! [X0: record] :
( ( next(split1(X0)) = split1(next(next(X0))) )
| ~ isrecord(next(X0))
| ~ isrecord(X0) ),
inference(cnf_transformation,[],[f19]) ).
tff(f58,definition,
sF2 = next(sK0),
introduced(definition,[new_symbols(definition,[sF2])],[function_definition]) ).
tff(f59,plain,
next(sK0) = sF2,
inference(reorient_equations,[],[f58]) ).
tff(f60,plain,
isrecord(sF2),
inference(definition_folding,[],[f49,f59]) ).
tff(f61,definition,
sF3 = next(sF2),
introduced(definition,[new_symbols(definition,[sF3])],[function_definition]) ).
tff(f62,plain,
sF3 = sK1,
inference(definition_folding,[],[f48,f61,f59]) ).
tff(f63,definition,
sF4 = split1(sK0),
introduced(definition,[new_symbols(definition,[sF4])],[function_definition]) ).
tff(f64,definition,
sF5 = length(sF4),
introduced(definition,[new_symbols(definition,[sF5])],[function_definition]) ).
tff(f65,plain,
length(sF4) = sF5,
inference(reorient_equations,[],[f64]) ).
tff(f66,definition,
sF6 = split2(sK0),
introduced(definition,[new_symbols(definition,[sF6])],[function_definition]) ).
tff(f67,plain,
split2(sK0) = sF6,
inference(reorient_equations,[],[f66]) ).
tff(f68,definition,
sF7 = length(sF6),
introduced(definition,[new_symbols(definition,[sF7])],[function_definition]) ).
tff(f69,plain,
length(sF6) = sF7,
inference(reorient_equations,[],[f68]) ).
tff(f70,definition,
sF8 = $sum(sF5,sF7),
introduced(definition,[new_symbols(definition,[sF8])],[function_definition]) ).
tff(f71,plain,
$sum(sF5,sF7) = sF8,
inference(reorient_equations,[],[f70]) ).
tff(f72,definition,
sF9 = length(sK0),
introduced(definition,[new_symbols(definition,[sF9])],[function_definition]) ).
tff(f73,plain,
sF9 != sF8,
inference(definition_folding,[],[f46,f72,f71,f69,f67,f65,f63]) ).
tff(f74,definition,
sF10 = length(sK1),
introduced(definition,[new_symbols(definition,[sF10])],[function_definition]) ).
tff(f75,plain,
length(sK1) = sF10,
inference(reorient_equations,[],[f74]) ).
tff(f76,definition,
sF11 = split1(sK1),
introduced(definition,[new_symbols(definition,[sF11])],[function_definition]) ).
tff(f77,plain,
split1(sK1) = sF11,
inference(reorient_equations,[],[f76]) ).
tff(f78,definition,
sF12 = length(sF11),
introduced(definition,[new_symbols(definition,[sF12])],[function_definition]) ).
tff(f79,plain,
length(sF11) = sF12,
inference(reorient_equations,[],[f78]) ).
tff(f80,definition,
sF13 = split2(sK1),
introduced(definition,[new_symbols(definition,[sF13])],[function_definition]) ).
tff(f81,plain,
split2(sK1) = sF13,
inference(reorient_equations,[],[f80]) ).
tff(f82,definition,
sF14 = length(sF13),
introduced(definition,[new_symbols(definition,[sF14])],[function_definition]) ).
tff(f83,definition,
sF15 = $sum(sF12,sF14),
introduced(definition,[new_symbols(definition,[sF15])],[function_definition]) ).
tff(f84,plain,
$sum(sF12,sF14) = sF15,
inference(reorient_equations,[],[f83]) ).
tff(f85,plain,
sF10 = sF15,
inference(definition_folding,[],[f45,f84,f82,f81,f79,f77,f75]) ).
tff(f87,definition,
( spl16_1
<=> ( sF9 = sF8 ) ),
introduced(definition,[new_symbols(definition,[spl16_1])],[avatar_definition]) ).
tff(f89,plain,
( ( sF9 != sF8 )
| spl16_1 ),
inference(avatar_component_clause,[],[f87]) ).
tff(f90,plain,
~ spl16_1,
inference(avatar_split_clause,[],[f73,f87]) ).
tff(f92,definition,
( spl16_2
<=> ( split2(sK1) = sF13 ) ),
introduced(definition,[new_symbols(definition,[spl16_2])],[avatar_definition]) ).
tff(f94,plain,
( ( split2(sK1) = sF13 )
| ~ spl16_2 ),
inference(avatar_component_clause,[],[f92]) ).
tff(f95,plain,
spl16_2,
inference(avatar_split_clause,[],[f81,f92]) ).
tff(f97,definition,
( spl16_3
<=> ( length(sF6) = sF7 ) ),
introduced(definition,[new_symbols(definition,[spl16_3])],[avatar_definition]) ).
tff(f99,plain,
( ( length(sF6) = sF7 )
| ~ spl16_3 ),
inference(avatar_component_clause,[],[f97]) ).
tff(f100,plain,
spl16_3,
inference(avatar_split_clause,[],[f69,f97]) ).
tff(f102,definition,
( spl16_4
<=> ( $sum(sF12,sF14) = sF15 ) ),
introduced(definition,[new_symbols(definition,[spl16_4])],[avatar_definition]) ).
tff(f104,plain,
( ( $sum(sF12,sF14) = sF15 )
| ~ spl16_4 ),
inference(avatar_component_clause,[],[f102]) ).
tff(f105,plain,
spl16_4,
inference(avatar_split_clause,[],[f84,f102]) ).
tff(f107,definition,
( spl16_5
<=> ( sF9 = length(sK0) ) ),
introduced(definition,[new_symbols(definition,[spl16_5])],[avatar_definition]) ).
tff(f109,plain,
( ( sF9 = length(sK0) )
| ~ spl16_5 ),
inference(avatar_component_clause,[],[f107]) ).
tff(f110,plain,
spl16_5,
inference(avatar_split_clause,[],[f72,f107]) ).
tff(f112,definition,
( spl16_6
<=> ( sF3 = sK1 ) ),
introduced(definition,[new_symbols(definition,[spl16_6])],[avatar_definition]) ).
tff(f114,plain,
( ( sF3 = sK1 )
| ~ spl16_6 ),
inference(avatar_component_clause,[],[f112]) ).
tff(f115,plain,
spl16_6,
inference(avatar_split_clause,[],[f62,f112]) ).
tff(f117,definition,
( spl16_7
<=> ( sF3 = next(sF2) ) ),
introduced(definition,[new_symbols(definition,[spl16_7])],[avatar_definition]) ).
tff(f119,plain,
( ( sF3 = next(sF2) )
| ~ spl16_7 ),
inference(avatar_component_clause,[],[f117]) ).
tff(f120,plain,
spl16_7,
inference(avatar_split_clause,[],[f61,f117]) ).
tff(f122,definition,
( spl16_8
<=> ( length(sF11) = sF12 ) ),
introduced(definition,[new_symbols(definition,[spl16_8])],[avatar_definition]) ).
tff(f124,plain,
( ( length(sF11) = sF12 )
| ~ spl16_8 ),
inference(avatar_component_clause,[],[f122]) ).
tff(f125,plain,
spl16_8,
inference(avatar_split_clause,[],[f79,f122]) ).
tff(f127,definition,
( spl16_9
<=> isrecord(sF2) ),
introduced(definition,[new_symbols(definition,[spl16_9])],[avatar_definition]) ).
tff(f129,plain,
( isrecord(sF2)
| ~ spl16_9 ),
inference(avatar_component_clause,[],[f127]) ).
tff(f130,plain,
spl16_9,
inference(avatar_split_clause,[],[f60,f127]) ).
tff(f132,definition,
( spl16_10
<=> ( sF10 = sF15 ) ),
introduced(definition,[new_symbols(definition,[spl16_10])],[avatar_definition]) ).
tff(f134,plain,
( ( sF10 = sF15 )
| ~ spl16_10 ),
inference(avatar_component_clause,[],[f132]) ).
tff(f135,plain,
spl16_10,
inference(avatar_split_clause,[],[f85,f132]) ).
tff(f137,definition,
( spl16_11
<=> ( length(sK1) = sF10 ) ),
introduced(definition,[new_symbols(definition,[spl16_11])],[avatar_definition]) ).
tff(f139,plain,
( ( length(sK1) = sF10 )
| ~ spl16_11 ),
inference(avatar_component_clause,[],[f137]) ).
tff(f140,plain,
spl16_11,
inference(avatar_split_clause,[],[f75,f137]) ).
tff(f142,definition,
( spl16_12
<=> ( length(sF4) = sF5 ) ),
introduced(definition,[new_symbols(definition,[spl16_12])],[avatar_definition]) ).
tff(f144,plain,
( ( length(sF4) = sF5 )
| ~ spl16_12 ),
inference(avatar_component_clause,[],[f142]) ).
tff(f145,plain,
spl16_12,
inference(avatar_split_clause,[],[f65,f142]) ).
tff(f147,definition,
( spl16_13
<=> ( split2(sK0) = sF6 ) ),
introduced(definition,[new_symbols(definition,[spl16_13])],[avatar_definition]) ).
tff(f149,plain,
( ( split2(sK0) = sF6 )
| ~ spl16_13 ),
inference(avatar_component_clause,[],[f147]) ).
tff(f150,plain,
spl16_13,
inference(avatar_split_clause,[],[f67,f147]) ).
tff(f152,definition,
( spl16_14
<=> ( split1(sK1) = sF11 ) ),
introduced(definition,[new_symbols(definition,[spl16_14])],[avatar_definition]) ).
tff(f154,plain,
( ( split1(sK1) = sF11 )
| ~ spl16_14 ),
inference(avatar_component_clause,[],[f152]) ).
tff(f155,plain,
spl16_14,
inference(avatar_split_clause,[],[f77,f152]) ).
tff(f157,definition,
( spl16_15
<=> isrecord(sK0) ),
introduced(definition,[new_symbols(definition,[spl16_15])],[avatar_definition]) ).
tff(f159,plain,
( isrecord(sK0)
| ~ spl16_15 ),
inference(avatar_component_clause,[],[f157]) ).
tff(f160,plain,
spl16_15,
inference(avatar_split_clause,[],[f47,f157]) ).
tff(f162,definition,
( spl16_16
<=> ( $sum(sF5,sF7) = sF8 ) ),
introduced(definition,[new_symbols(definition,[spl16_16])],[avatar_definition]) ).
tff(f165,plain,
spl16_16,
inference(avatar_split_clause,[],[f71,f162]) ).
tff(f167,definition,
( spl16_17
<=> ( sF14 = length(sF13) ) ),
introduced(definition,[new_symbols(definition,[spl16_17])],[avatar_definition]) ).
tff(f169,plain,
( ( sF14 = length(sF13) )
| ~ spl16_17 ),
inference(avatar_component_clause,[],[f167]) ).
tff(f170,plain,
spl16_17,
inference(avatar_split_clause,[],[f82,f167]) ).
tff(f172,definition,
( spl16_18
<=> ( sF4 = split1(sK0) ) ),
introduced(definition,[new_symbols(definition,[spl16_18])],[avatar_definition]) ).
tff(f174,plain,
( ( sF4 = split1(sK0) )
| ~ spl16_18 ),
inference(avatar_component_clause,[],[f172]) ).
tff(f175,plain,
spl16_18,
inference(avatar_split_clause,[],[f63,f172]) ).
tff(f177,definition,
( spl16_19
<=> ( next(sK0) = sF2 ) ),
introduced(definition,[new_symbols(definition,[spl16_19])],[avatar_definition]) ).
tff(f179,plain,
( ( next(sK0) = sF2 )
| ~ spl16_19 ),
inference(avatar_component_clause,[],[f177]) ).
tff(f180,plain,
spl16_19,
inference(avatar_split_clause,[],[f59,f177]) ).
tff(f181,plain,
( ( sF8 != length(sK0) )
| spl16_1
| ~ spl16_5 ),
inference(superposition,[],[f89,f109]) ).
tff(f183,definition,
( spl16_20
<=> ( sF8 = length(sK0) ) ),
introduced(definition,[new_symbols(definition,[spl16_20])],[avatar_definition]) ).
tff(f186,plain,
( ~ spl16_20
| spl16_1
| ~ spl16_5 ),
inference(avatar_split_clause,[],[f181,f107,f87,f183]) ).
tff(f187,plain,
( ( sK1 = next(sF2) )
| ~ spl16_6
| ~ spl16_7 ),
inference(forward_demodulation,[],[f119,f114]) ).
tff(f189,definition,
( spl16_21
<=> ( sK1 = next(sF2) ) ),
introduced(definition,[new_symbols(definition,[spl16_21])],[avatar_definition]) ).
tff(f191,plain,
( ( sK1 = next(sF2) )
| ~ spl16_21 ),
inference(avatar_component_clause,[],[f189]) ).
tff(f192,plain,
( spl16_21
| ~ spl16_6
| ~ spl16_7 ),
inference(avatar_split_clause,[],[f187,f117,f112,f189]) ).
tff(f194,plain,
( ( length(sK1) = sF15 )
| ~ spl16_10
| ~ spl16_11 ),
inference(superposition,[],[f134,f139]) ).
tff(f196,definition,
( spl16_22
<=> ( length(sK1) = sF15 ) ),
introduced(definition,[new_symbols(definition,[spl16_22])],[avatar_definition]) ).
tff(f198,plain,
( ( length(sK1) = sF15 )
| ~ spl16_22 ),
inference(avatar_component_clause,[],[f196]) ).
tff(f199,plain,
( spl16_22
| ~ spl16_10
| ~ spl16_11 ),
inference(avatar_split_clause,[],[f194,f137,f132,f196]) ).
tff(f200,plain,
( ( length(split2(sK0)) = sF7 )
| ~ spl16_3
| ~ spl16_13 ),
inference(superposition,[],[f99,f149]) ).
tff(f202,definition,
( spl16_23
<=> ( length(split2(sK0)) = sF7 ) ),
introduced(definition,[new_symbols(definition,[spl16_23])],[avatar_definition]) ).
tff(f205,plain,
( spl16_23
| ~ spl16_3
| ~ spl16_13 ),
inference(avatar_split_clause,[],[f200,f147,f97,f202]) ).
tff(f206,plain,
( ( sF5 = length(split1(sK0)) )
| ~ spl16_12
| ~ spl16_18 ),
inference(superposition,[],[f144,f174]) ).
tff(f208,definition,
( spl16_24
<=> ( sF5 = length(split1(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl16_24])],[avatar_definition]) ).
tff(f211,plain,
( spl16_24
| ~ spl16_12
| ~ spl16_18 ),
inference(avatar_split_clause,[],[f206,f172,f142,f208]) ).
tff(f231,plain,
( ( length(sK1) = $sum(sF12,sF14) )
| ~ spl16_4
| ~ spl16_22 ),
inference(forward_demodulation,[],[f104,f198]) ).
tff(f232,plain,
( ( length(sK1) = $sum(length(sF11),sF14) )
| ~ spl16_4
| ~ spl16_8
| ~ spl16_22 ),
inference(forward_demodulation,[],[f231,f124]) ).
tff(f234,definition,
( spl16_28
<=> ( length(sK1) = $sum(length(sF11),sF14) ) ),
introduced(definition,[new_symbols(definition,[spl16_28])],[avatar_definition]) ).
tff(f237,plain,
( spl16_28
| ~ spl16_4
| ~ spl16_8
| ~ spl16_22 ),
inference(avatar_split_clause,[],[f232,f196,f122,f102,f234]) ).
tff(f259,definition,
( spl16_30
<=> isrecord(split2(sK0)) ),
introduced(definition,[new_symbols(definition,[spl16_30])],[avatar_definition]) ).
tff(f260,plain,
( ~ isrecord(split2(sK0))
| spl16_30 ),
inference(avatar_component_clause,[],[f259]) ).
tff(f277,definition,
( spl16_34
<=> isrecord(split1(sK0)) ),
introduced(definition,[new_symbols(definition,[spl16_34])],[avatar_definition]) ).
tff(f278,plain,
( ~ isrecord(split1(sK0))
| spl16_34 ),
inference(avatar_component_clause,[],[f277]) ).
tff(f343,plain,
( ~ isrecord(sF2)
| ( $sum(length(sK1),1) = length(sF2) )
| ~ spl16_21 ),
inference(superposition,[],[f43,f191]) ).
tff(f344,plain,
( ( $sum(length(sF2),1) = length(sK0) )
| ~ isrecord(sK0)
| ~ spl16_19 ),
inference(superposition,[],[f43,f179]) ).
tff(f347,plain,
( ( $sum(length(sK1),1) = length(sF2) )
| ~ spl16_9
| ~ spl16_21 ),
inference(forward_subsumption_resolution,[],[f343,f129]) ).
tff(f348,plain,
( ( $sum(length(sF2),1) = length(sK0) )
| ~ spl16_15
| ~ spl16_19 ),
inference(forward_subsumption_resolution,[],[f344,f159]) ).
tff(f350,definition,
( spl16_42
<=> ( $sum(length(sK1),1) = length(sF2) ) ),
introduced(definition,[new_symbols(definition,[spl16_42])],[avatar_definition]) ).
tff(f353,plain,
( spl16_42
| ~ spl16_9
| ~ spl16_21 ),
inference(avatar_split_clause,[],[f347,f189,f127,f350]) ).
tff(f355,definition,
( spl16_43
<=> ( $sum(length(sF2),1) = length(sK0) ) ),
introduced(definition,[new_symbols(definition,[spl16_43])],[avatar_definition]) ).
tff(f358,plain,
( spl16_43
| ~ spl16_15
| ~ spl16_19 ),
inference(avatar_split_clause,[],[f348,f177,f157,f355]) ).
tff(f378,plain,
( ( split2(next(sF2)) = next(split2(sK0)) )
| ~ isrecord(sK0)
| ~ isrecord(sF2)
| ~ spl16_19 ),
inference(superposition,[],[f40,f179]) ).
tff(f383,plain,
( ( split2(next(sF2)) = next(split2(sK0)) )
| ~ isrecord(sF2)
| ~ spl16_15
| ~ spl16_19 ),
inference(forward_subsumption_resolution,[],[f378,f159]) ).
tff(f389,plain,
( ( split2(next(sF2)) = next(split2(sK0)) )
| ~ spl16_9
| ~ spl16_15
| ~ spl16_19 ),
inference(forward_subsumption_resolution,[],[f383,f129]) ).
tff(f390,plain,
( ( split2(sK1) = next(split2(sK0)) )
| ~ spl16_9
| ~ spl16_15
| ~ spl16_19
| ~ spl16_21 ),
inference(forward_demodulation,[],[f389,f191]) ).
tff(f391,plain,
( ( next(split2(sK0)) = sF13 )
| ~ spl16_2
| ~ spl16_9
| ~ spl16_15
| ~ spl16_19
| ~ spl16_21 ),
inference(forward_demodulation,[],[f390,f94]) ).
tff(f393,definition,
( spl16_47
<=> ( next(split2(sK0)) = sF13 ) ),
introduced(definition,[new_symbols(definition,[spl16_47])],[avatar_definition]) ).
tff(f395,plain,
( ( next(split2(sK0)) = sF13 )
| ~ spl16_47 ),
inference(avatar_component_clause,[],[f393]) ).
tff(f396,plain,
( spl16_47
| ~ spl16_2
| ~ spl16_9
| ~ spl16_15
| ~ spl16_19
| ~ spl16_21 ),
inference(avatar_split_clause,[],[f391,f189,f177,f157,f127,f92,f393]) ).
tff(f398,plain,
( ( $sum(length(sF13),1) = length(split2(sK0)) )
| ~ isrecord(split2(sK0))
| ~ spl16_47 ),
inference(superposition,[],[f43,f395]) ).
tff(f400,plain,
( ~ isrecord(split2(sK0))
| ( $sum(sF14,1) = length(split2(sK0)) )
| ~ spl16_17
| ~ spl16_47 ),
inference(forward_demodulation,[],[f398,f169]) ).
tff(f416,definition,
( spl16_50
<=> ( $sum(sF14,1) = length(split2(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl16_50])],[avatar_definition]) ).
tff(f419,plain,
( ~ spl16_30
| spl16_50
| ~ spl16_17
| ~ spl16_47 ),
inference(avatar_split_clause,[],[f400,f393,f167,f416,f259]) ).
tff(f421,plain,
( ~ isrecord(sF2)
| ~ isrecord(sK0)
| ( next(split1(sK0)) = split1(next(sF2)) )
| ~ spl16_19 ),
inference(superposition,[],[f56,f179]) ).
tff(f428,plain,
( ~ isrecord(sK0)
| ( next(split1(sK0)) = split1(next(sF2)) )
| ~ spl16_9
| ~ spl16_19 ),
inference(forward_subsumption_resolution,[],[f421,f129]) ).
tff(f430,plain,
( ( next(split1(sK0)) = split1(next(sF2)) )
| ~ spl16_9
| ~ spl16_15
| ~ spl16_19 ),
inference(forward_subsumption_resolution,[],[f428,f159]) ).
tff(f436,plain,
( ( split1(sK1) = next(split1(sK0)) )
| ~ spl16_9
| ~ spl16_15
| ~ spl16_19
| ~ spl16_21 ),
inference(forward_demodulation,[],[f430,f191]) ).
tff(f437,plain,
( ( next(split1(sK0)) = sF11 )
| ~ spl16_9
| ~ spl16_14
| ~ spl16_15
| ~ spl16_19
| ~ spl16_21 ),
inference(forward_demodulation,[],[f436,f154]) ).
tff(f439,definition,
( spl16_52
<=> ( next(split1(sK0)) = sF11 ) ),
introduced(definition,[new_symbols(definition,[spl16_52])],[avatar_definition]) ).
tff(f441,plain,
( ( next(split1(sK0)) = sF11 )
| ~ spl16_52 ),
inference(avatar_component_clause,[],[f439]) ).
tff(f442,plain,
( spl16_52
| ~ spl16_9
| ~ spl16_14
| ~ spl16_15
| ~ spl16_19
| ~ spl16_21 ),
inference(avatar_split_clause,[],[f437,f189,f177,f157,f152,f127,f439]) ).
tff(f449,plain,
( ( $sum(length(sF11),1) = length(split1(sK0)) )
| ~ isrecord(split1(sK0))
| ~ spl16_52 ),
inference(superposition,[],[f43,f441]) ).
tff(f468,definition,
( spl16_56
<=> ( $sum(length(sF11),1) = length(split1(sK0)) ) ),
introduced(definition,[new_symbols(definition,[spl16_56])],[avatar_definition]) ).
tff(f471,plain,
( ~ spl16_34
| spl16_56
| ~ spl16_52 ),
inference(avatar_split_clause,[],[f449,f439,f468,f277]) ).
tff(f584,plain,
( ~ isrecord(sK0)
| spl16_34 ),
inference(resolution,[],[f278,f55]) ).
tff(f585,plain,
( $false
| ~ spl16_15
| spl16_34 ),
inference(forward_subsumption_resolution,[],[f584,f159]) ).
tff(f586,plain,
( ~ spl16_15
| spl16_34 ),
inference(avatar_contradiction_clause,[],[f585]) ).
tff(f598,plain,
( ~ isrecord(next(sK0))
| ~ isrecord(sK0)
| spl16_30 ),
inference(resolution,[],[f260,f44]) ).
tff(f599,plain,
( ~ isrecord(next(sK0))
| ~ spl16_15
| spl16_30 ),
inference(forward_subsumption_resolution,[],[f598,f159]) ).
tff(f600,plain,
( ~ isrecord(sF2)
| ~ spl16_15
| ~ spl16_19
| spl16_30 ),
inference(forward_demodulation,[],[f599,f179]) ).
tff(f601,plain,
( $false
| ~ spl16_9
| ~ spl16_15
| ~ spl16_19
| spl16_30 ),
inference(forward_subsumption_resolution,[],[f600,f129]) ).
tff(f602,plain,
( ~ spl16_9
| ~ spl16_15
| ~ spl16_19
| spl16_30 ),
inference(avatar_contradiction_clause,[],[f601]) ).
tff(f603,plain,
$false,
inference(avatar_smt_refutation,[],[f602,f586,f471,f442,f419,f396,f358,f353,f237,f211,f205,f199,f192,f186,f180,f175,f170,f165,f160,f155,f150,f145,f140,f135,f130,f125,f120,f115,f110,f105,f100,f95,f90]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : DAT052_1 : TPTP v9.3.1. Released v5.0.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.20 % Computer : n003.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Tue Sep 29 00:09:00 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.20 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 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
% 1.15/1.01 % (2154283)Detected arithmetic, will pick strategies from an ALASCA-aware ARI schedule.
% 1.15/1.01 % (2154289)dis+1002_1_to=kbo:sil=128000:tgt=ground:sas=z3:si=on:spb=units:tha=off:random_seed=1096540440:i=307:kws=precedence:nm=0:rtra=on_2999 on theBenchmark for (2999ds/307Mi)
% 1.15/1.01 % (2154290)dis+10_3_slsqr=1,4:to=lpo:sil=128000:thi=strong:si=on:uwa=off:s2agt=20:slsqc=1:slsq=on:random_seed=2380926451:i=201:slsql=off:asg=cautious:rtra=on:gtg=all:ss=axioms:sgt=16_2999 on theBenchmark for (2999ds/201Mi)
% 1.15/1.01 % (2154292)dis+21_64_to=kbo:sil=128000:si=on:sp=weighted_frequency:uwa=alasca_can_abstract:random_seed=2551298591:i=4:rtra=on_2999 on theBenchmark for (2999ds/4Mi)
% 1.15/1.01 % (2154291)lrs+1002_4:1_to=lpo:sil=64000:si=on:br=off:random_seed=516917690:s2a=on:i=7:rtra=on:inst=on_2999 on theBenchmark for (2999ds/7Mi)
% 1.15/1.01 % (2154288)dis+1002_16:1_to=lpo:sil=64000:sas=z3:si=on:norm_ineq=on:gve=force:uwa=one_side_constant:random_seed=504538875:i=12:doe=on:rtra=on:gtg=exists_top:ss=axioms_2999 on theBenchmark for (2999ds/12Mi)
% 1.15/1.01 % (2154292)Instruction limit reached!
% 1.15/1.01 % (2154292)------------------------------
% 1.15/1.01 % (2154292)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.15/1.01 % (2154292)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.15/1.01 % (2154292)CaDiCaL version: 2.1.3
% 1.15/1.01 % (2154292)Termination reason: Instruction limit
% 1.15/1.01 % (2154292)Termination phase: Saturation
% 1.15/1.01 % (2154292)Time elapsed: 0.004 s
% 1.15/1.01 % (2154292)Peak memory usage: 89 MB
% 1.15/1.01 % (2154292)Instructions burned: 5 (million)
% 1.15/1.01 % (2154291)Instruction limit reached!
% 1.15/1.01 % (2154291)------------------------------
% 1.15/1.01 % (2154291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.15/1.01 % (2154291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.15/1.01 % (2154291)CaDiCaL version: 2.1.3
% 1.15/1.01 % (2154291)Termination reason: Instruction limit
% 1.15/1.01 % (2154291)Termination phase: Saturation
% 1.15/1.01 % (2154291)Time elapsed: 0.006 s
% 1.15/1.01 % (2154291)Peak memory usage: 88 MB
% 1.15/1.01 % (2154291)Instructions burned: 7 (million)
% 1.15/1.01 % (2154289)First to succeed.
% 1.15/1.01 % (2154293)lrs+10_1_to=lpo:sas=z3:si=on:tha=off:random_seed=1693568088:i=46:rtra=on_2999 on theBenchmark for (2999ds/46Mi)
% 1.15/1.01 % (2154294)lrs+10_1_tgt=ground:sas=z3:si=on:random_seed=337929452:i=33:rtra=on_2999 on theBenchmark for (2999ds/33Mi)
% 1.15/1.01 % (2154289)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2154283"
% 1.15/1.01 % (2154288)Instruction limit reached!
% 1.15/1.01 % (2154288)------------------------------
% 1.15/1.01 % (2154288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.15/1.01 % (2154288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.15/1.01 % (2154288)CaDiCaL version: 2.1.3
% 1.15/1.01 % (2154288)Termination reason: Instruction limit
% 1.15/1.01 % (2154288)Termination phase: Saturation
% 1.15/1.01 % (2154288)Time elapsed: 0.032 s
% 1.15/1.01 % (2154288)Peak memory usage: 116 MB
% 1.15/1.01 % (2154288)Instructions burned: 13 (million)
% 1.15/1.01 % (2154294)Instruction limit reached!
% 1.15/1.01 % (2154294)------------------------------
% 1.15/1.01 % (2154294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.15/1.01 % (2154294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.15/1.01 % (2154294)CaDiCaL version: 2.1.3
% 1.15/1.01 % (2154294)Termination reason: Instruction limit
% 1.15/1.01 % (2154294)Termination phase: Saturation
% 1.15/1.01 % (2154294)Time elapsed: 0.045 s
% 1.15/1.01 % (2154294)Peak memory usage: 116 MB
% 1.15/1.01 % (2154294)Instructions burned: 33 (million)
% 1.15/1.01 % (2154293)Instruction limit reached!
% 1.15/1.01 % (2154293)------------------------------
% 1.15/1.01 % (2154293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.15/1.01 % (2154293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.15/1.01 % (2154293)CaDiCaL version: 2.1.3
% 1.15/1.01 % (2154293)Termination reason: Instruction limit
% 1.15/1.01 % (2154293)Termination phase: Saturation
% 1.15/1.01 % (2154293)Time elapsed: 0.057 s
% 1.15/1.01 % (2154293)Peak memory usage: 116 MB
% 1.15/1.01 % (2154293)Instructions burned: 46 (million)
% 1.15/1.01 % (2154290)Instruction limit reached!
% 1.15/1.01 % (2154290)------------------------------
% 1.15/1.01 % (2154290)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 1.15/1.01 % (2154290)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 1.15/1.01 % (2154290)CaDiCaL version: 2.1.3
% 1.15/1.01 % (2154290)Termination reason: Instruction limit
% 1.15/1.01 % (2154290)Termination phase: Saturation
% 1.15/1.01 % (2154290)Time elapsed: 0.147 s
% 1.15/1.01 % (2154290)Peak memory usage: 117 MB
% 1.15/1.01 % (2154290)Instructions burned: 201 (million)
% 1.15/1.01 % (2154301)dis+1011_2:1_to=kbo:sil=128000:tgt=full:fde=none:si=on:norm_ineq=on:spb=goal_then_units:tha=some:nwc=2:sac=on:random_seed=2009201720:i=29:thsqd=64:nm=0:thsqc=8:rtra=on:thsq=on:ev=off_2998 on theBenchmark for (2998ds/29Mi)
% 1.15/1.01 % (2154300)dis+11_3_anc=none:drc=ordering:si=on:urr=ec_only:bce=on:tha=off:sac=on:random_seed=1022995889:st=5:i=14:sd=10:rtra=on:ss=axioms:rawr=on_2998 on theBenchmark for (2998ds/14Mi)
% 1.15/1.01 % (2154289)Refutation found. Thanks to Tanya!
% 1.15/1.01 % SZS status Theorem for theBenchmark
% 1.15/1.01 % SZS output start Proof for theBenchmark
% See solution above
% 2.91/1.11 % (2154289)------------------------------
% 2.91/1.11 % (2154289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 2.91/1.11 % (2154289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 2.91/1.11 % (2154289)CaDiCaL version: 2.1.3
% 2.91/1.11 % (2154289)Termination reason: Refutation
% 2.91/1.11 % (2154289)Time elapsed: 0.055 s
% 2.91/1.11 % (2154289)Peak memory usage: 117 MB
% 2.91/1.11 % (2154289)Instructions burned: 104 (million)
% 2.91/1.11 % (2154289)------------------------------
% 2.91/1.11 % (2154289)------------------------------
% 2.91/1.11 % (2154283)Success in time 0.339 s
% 2.91/1.11 % Vampire exiting
%------------------------------------------------------------------------------