%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PLA054_4 : TPTP v9.3.1. Released v8.2.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% Computer : n006.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:30:11 PM UTC 2026
% Result : Theorem 0.19s 0.48s
% Output : Refutation 0.19s
% Verified :
% SZS Type : Refutation
% Derivation depth : 15
% Number of leaves : 12
% Syntax : Number of formulae : 74 ( 15 unt; 0 typ; 6 def)
% Number of atoms : 334 ( 0 equ)
% Maximal formula atoms : 16 ( 4 avg)
% Number of connectives : 375 ( 150 ~; 145 |; 42 &)
% ( 6 <=>; 32 =>; 0 <=; 0 <~>)
% Maximal formula depth : 18 ( 6 avg)
% Maximal term depth : 2 ( 1 avg)
% Number of FOOLs : 35 ( 35 fml; 0 var)
% Number of types : 3 ( 1 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 16 ( 15 usr; 10 prp; 0-3 aty)
% Number of functors : 5 ( 5 usr; 3 con; 0-3 aty)
% Number of variables : 128 ( 0 sgn 112 !; 16 ?; 128 :)
% Comments :
%------------------------------------------------------------------------------
tff(type_def_5,type,
'$ki_world': $tType ).
tff(func_def_0,type,
'$ki_local_world': '$ki_world' ).
tff(func_def_4,type,
sK0: '$ki_world' > $i ).
tff(func_def_5,type,
sK1: ( '$ki_world' * $i * $i ) > $i ).
tff(func_def_7,type,
sK3: '$ki_world' ).
tff(func_def_8,type,
sK4: '$ki_world' ).
tff(pred_def_1,type,
'$ki_accessible': ( '$ki_world' * '$ki_world' ) > $o ).
tff(pred_def_2,type,
h: ( '$ki_world' * $i ) > $o ).
tff(pred_def_3,type,
closed: ( '$ki_world' * $i ) > $o ).
tff(pred_def_4,type,
combo: ( '$ki_world' * $i * $i ) > $o ).
tff(pred_def_5,type,
open: ( '$ki_world' * $i ) > $o ).
tff(pred_def_6,type,
'$ki_exists_in_world_$i': ( '$ki_world' * $i ) > $o ).
tff(f1,axiom,
! [X0: '$ki_world'] : '$ki_accessible'(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',mrel_reflexive) ).
tff(f3,axiom,
! [X0: '$ki_world',X1: $i] : '$ki_exists_in_world_$i'(X0,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p','$ki_exists_in_world_$i_const') ).
tff(f5,axiom,
! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> ! [X1: $i] :
( '$ki_exists_in_world_$i'(X0,X1)
=> ! [X2: $i] :
( '$ki_exists_in_world_$i'(X0,X2)
=> ? [X3: $i] :
( '$ki_exists_in_world_$i'(X0,X3)
& ! [X4: '$ki_world'] :
( '$ki_accessible'(X0,X4)
=> ( ( closed(X4,X1)
& combo(X4,X1,X2)
& h(X4,X3) )
=> ! [X5: '$ki_world'] :
( '$ki_accessible'(X4,X5)
=> open(X5,X1) ) ) )
& ! [X4: '$ki_world'] :
( '$ki_accessible'(X0,X4)
=> ( ( closed(X4,X1)
& ~ combo(X4,X1,X2)
& h(X4,o) )
=> ! [X5: '$ki_world'] :
( '$ki_accessible'(X4,X5)
=> closed(X5,X1) ) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax1) ).
tff(f6,axiom,
! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> closed(X0,d) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax2) ).
tff(f9,axiom,
? [X0: $i] :
( '$ki_exists_in_world_$i'('$ki_local_world',X0)
& ! [X1: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X1)
=> combo(X1,d,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ax5) ).
tff(f10,conjecture,
! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> ? [X1: $i] :
( '$ki_exists_in_world_$i'(X0,X1)
& ? [X2: $i] :
( '$ki_exists_in_world_$i'(X0,X2)
& ( ! [X3: '$ki_world'] :
( '$ki_accessible'(X0,X3)
=> ( combo(X3,d,X1)
& h(X3,X2) ) )
=> ! [X3: '$ki_world'] :
( '$ki_accessible'(X0,X3)
=> open(X3,d) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',verify) ).
tff(f11,negated_conjecture,
~ ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> ? [X1: $i] :
( '$ki_exists_in_world_$i'(X0,X1)
& ? [X2: $i] :
( '$ki_exists_in_world_$i'(X0,X2)
& ( ! [X3: '$ki_world'] :
( '$ki_accessible'(X0,X3)
=> ( combo(X3,d,X1)
& h(X3,X2) ) )
=> ! [X3: '$ki_world'] :
( '$ki_accessible'(X0,X3)
=> open(X3,d) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f10]) ).
tff(f12,plain,
! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> ! [X1: $i] :
( '$ki_exists_in_world_$i'(X0,X1)
=> ! [X2: $i] :
( '$ki_exists_in_world_$i'(X0,X2)
=> ? [X3: $i] :
( '$ki_exists_in_world_$i'(X0,X3)
& ! [X4: '$ki_world'] :
( '$ki_accessible'(X0,X4)
=> ( ( closed(X4,X1)
& combo(X4,X1,X2)
& h(X4,X3) )
=> ! [X5: '$ki_world'] :
( '$ki_accessible'(X4,X5)
=> open(X5,X1) ) ) )
& ! [X6: '$ki_world'] :
( '$ki_accessible'(X0,X6)
=> ( ( closed(X6,X1)
& ~ combo(X6,X1,X2)
& h(X6,o) )
=> ! [X7: '$ki_world'] :
( '$ki_accessible'(X6,X7)
=> closed(X7,X1) ) ) ) ) ) ) ),
inference(rectify,[],[f5]) ).
tff(f13,plain,
~ ! [X0: '$ki_world'] :
( '$ki_accessible'('$ki_local_world',X0)
=> ? [X1: $i] :
( '$ki_exists_in_world_$i'(X0,X1)
& ? [X2: $i] :
( '$ki_exists_in_world_$i'(X0,X2)
& ( ! [X3: '$ki_world'] :
( '$ki_accessible'(X0,X3)
=> ( combo(X3,d,X1)
& h(X3,X2) ) )
=> ! [X4: '$ki_world'] :
( '$ki_accessible'(X0,X4)
=> open(X4,d) ) ) ) ) ),
inference(rectify,[],[f11]) ).
tff(f16,plain,
! [X0: '$ki_world'] :
( ! [X1: $i] :
( ! [X2: $i] :
( ? [X3: $i] :
( '$ki_exists_in_world_$i'(X0,X3)
& ! [X4: '$ki_world'] :
( ! [X5: '$ki_world'] :
( open(X5,X1)
| ~ '$ki_accessible'(X4,X5) )
| ~ closed(X4,X1)
| ~ combo(X4,X1,X2)
| ~ h(X4,X3)
| ~ '$ki_accessible'(X0,X4) )
& ! [X6: '$ki_world'] :
( ! [X7: '$ki_world'] :
( closed(X7,X1)
| ~ '$ki_accessible'(X6,X7) )
| ~ closed(X6,X1)
| combo(X6,X1,X2)
| ~ h(X6,o)
| ~ '$ki_accessible'(X0,X6) ) )
| ~ '$ki_exists_in_world_$i'(X0,X2) )
| ~ '$ki_exists_in_world_$i'(X0,X1) )
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(ennf_transformation,[],[f12]) ).
tff(f17,plain,
! [X0: '$ki_world'] :
( ! [X1: $i] :
( ! [X2: $i] :
( ? [X3: $i] :
( '$ki_exists_in_world_$i'(X0,X3)
& ! [X4: '$ki_world'] :
( ! [X5: '$ki_world'] :
( open(X5,X1)
| ~ '$ki_accessible'(X4,X5) )
| ~ closed(X4,X1)
| ~ combo(X4,X1,X2)
| ~ h(X4,X3)
| ~ '$ki_accessible'(X0,X4) )
& ! [X6: '$ki_world'] :
( ! [X7: '$ki_world'] :
( closed(X7,X1)
| ~ '$ki_accessible'(X6,X7) )
| ~ closed(X6,X1)
| combo(X6,X1,X2)
| ~ h(X6,o)
| ~ '$ki_accessible'(X0,X6) ) )
| ~ '$ki_exists_in_world_$i'(X0,X2) )
| ~ '$ki_exists_in_world_$i'(X0,X1) )
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(flattening,[],[f16]) ).
tff(f18,plain,
! [X0: '$ki_world'] :
( closed(X0,d)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(ennf_transformation,[],[f6]) ).
tff(f23,plain,
? [X0: $i] :
( '$ki_exists_in_world_$i'('$ki_local_world',X0)
& ! [X1: '$ki_world'] :
( combo(X1,d,X0)
| ~ '$ki_accessible'('$ki_local_world',X1) ) ),
inference(ennf_transformation,[],[f9]) ).
tff(f24,plain,
? [X0: '$ki_world'] :
( ! [X1: $i] :
( ~ '$ki_exists_in_world_$i'(X0,X1)
| ! [X2: $i] :
( ~ '$ki_exists_in_world_$i'(X0,X2)
| ( ? [X4: '$ki_world'] :
( ~ open(X4,d)
& '$ki_accessible'(X0,X4) )
& ! [X3: '$ki_world'] :
( ( combo(X3,d,X1)
& h(X3,X2) )
| ~ '$ki_accessible'(X0,X3) ) ) ) )
& '$ki_accessible'('$ki_local_world',X0) ),
inference(ennf_transformation,[],[f13]) ).
tff(f26,plain,
! [X0: '$ki_world'] :
( ! [X1: $i] :
( ! [X2: $i] :
( ( '$ki_exists_in_world_$i'(X0,sK1(X0,X1,X2))
& ! [X4: '$ki_world'] :
( ! [X5: '$ki_world'] :
( open(X5,X1)
| ~ '$ki_accessible'(X4,X5) )
| ~ closed(X4,X1)
| ~ combo(X4,X1,X2)
| ~ h(X4,sK1(X0,X1,X2))
| ~ '$ki_accessible'(X0,X4) )
& ! [X6: '$ki_world'] :
( ! [X7: '$ki_world'] :
( closed(X7,X1)
| ~ '$ki_accessible'(X6,X7) )
| ~ closed(X6,X1)
| combo(X6,X1,X2)
| ~ h(X6,o)
| ~ '$ki_accessible'(X0,X6) ) )
| ~ '$ki_exists_in_world_$i'(X0,X2) )
| ~ '$ki_exists_in_world_$i'(X0,X1) )
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(X3,sK1(X0,X1,X2))],[f17]) ).
tff(f27,plain,
( '$ki_exists_in_world_$i'('$ki_local_world',sK2)
& ! [X1: '$ki_world'] :
( combo(X1,d,sK2)
| ~ '$ki_accessible'('$ki_local_world',X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(X0,sK2)],[f23]) ).
tff(f28,plain,
? [X0: '$ki_world'] :
( ! [X1: $i] :
( ~ '$ki_exists_in_world_$i'(X0,X1)
| ! [X2: $i] :
( ~ '$ki_exists_in_world_$i'(X0,X2)
| ( ? [X3: '$ki_world'] :
( ~ open(X3,d)
& '$ki_accessible'(X0,X3) )
& ! [X4: '$ki_world'] :
( ( combo(X4,d,X1)
& h(X4,X2) )
| ~ '$ki_accessible'(X0,X4) ) ) ) )
& '$ki_accessible'('$ki_local_world',X0) ),
inference(rectify,[],[f24]) ).
tff(f29,plain,
( ! [X1: $i] :
( ~ '$ki_exists_in_world_$i'(sK3,X1)
| ! [X2: $i] :
( ~ '$ki_exists_in_world_$i'(sK3,X2)
| ( ~ open(sK4,d)
& '$ki_accessible'(sK3,sK4)
& ! [X4: '$ki_world'] :
( ( combo(X4,d,X1)
& h(X4,X2) )
| ~ '$ki_accessible'(sK3,X4) ) ) ) )
& '$ki_accessible'('$ki_local_world',sK3) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3,sK4]),skolemize(X0,sK3),skolemize(X3,sK4)],[f28]) ).
tff(f30,plain,
! [X0: '$ki_world'] : '$ki_accessible'(X0,X0),
inference(cnf_transformation,[],[f1]) ).
tff(f32,plain,
! [X0: '$ki_world',X1: $i] : '$ki_exists_in_world_$i'(X0,X1),
inference(cnf_transformation,[],[f3]) ).
tff(f35,plain,
! [X2: $i,X0: '$ki_world',X1: $i,X4: '$ki_world',X5: '$ki_world'] :
( open(X5,X1)
| ~ '$ki_accessible'(X4,X5)
| ~ closed(X4,X1)
| ~ combo(X4,X1,X2)
| ~ h(X4,sK1(X0,X1,X2))
| ~ '$ki_accessible'(X0,X4)
| ~ '$ki_exists_in_world_$i'(X0,X2)
| ~ '$ki_exists_in_world_$i'(X0,X1)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(cnf_transformation,[],[f26]) ).
tff(f37,plain,
! [X0: '$ki_world'] :
( ~ '$ki_accessible'('$ki_local_world',X0)
| closed(X0,d) ),
inference(cnf_transformation,[],[f18]) ).
tff(f40,plain,
! [X1: '$ki_world'] :
( combo(X1,d,sK2)
| ~ '$ki_accessible'('$ki_local_world',X1) ),
inference(cnf_transformation,[],[f27]) ).
tff(f42,plain,
'$ki_accessible'('$ki_local_world',sK3),
inference(cnf_transformation,[],[f29]) ).
tff(f43,plain,
! [X2: $i,X1: $i,X4: '$ki_world'] :
( ~ '$ki_exists_in_world_$i'(sK3,X1)
| ~ '$ki_exists_in_world_$i'(sK3,X2)
| h(X4,X2)
| ~ '$ki_accessible'(sK3,X4) ),
inference(cnf_transformation,[],[f29]) ).
tff(f45,plain,
! [X2: $i,X1: $i] :
( ~ '$ki_exists_in_world_$i'(sK3,X1)
| ~ '$ki_exists_in_world_$i'(sK3,X2)
| '$ki_accessible'(sK3,sK4) ),
inference(cnf_transformation,[],[f29]) ).
tff(f46,plain,
! [X2: $i,X1: $i] :
( ~ '$ki_exists_in_world_$i'(sK3,X1)
| ~ '$ki_exists_in_world_$i'(sK3,X2)
| ~ open(sK4,d) ),
inference(cnf_transformation,[],[f29]) ).
tff(f48,definition,
( spl5_1
<=> ! [X2: $i,X4: '$ki_world'] :
( ~ '$ki_exists_in_world_$i'(sK3,X2)
| ~ '$ki_accessible'(sK3,X4)
| h(X4,X2) ) ),
introduced(definition,[new_symbols(definition,[spl5_1])],[avatar_definition]) ).
tff(f49,plain,
( ! [X2: $i,X4: '$ki_world'] :
( ~ '$ki_exists_in_world_$i'(sK3,X2)
| ~ '$ki_accessible'(sK3,X4)
| h(X4,X2) )
| ~ spl5_1 ),
inference(avatar_component_clause,[],[f48]) ).
tff(f51,definition,
( spl5_2
<=> ! [X1: $i] : ~ '$ki_exists_in_world_$i'(sK3,X1) ),
introduced(definition,[new_symbols(definition,[spl5_2])],[avatar_definition]) ).
tff(f52,plain,
( ! [X1: $i] : ~ '$ki_exists_in_world_$i'(sK3,X1)
| ~ spl5_2 ),
inference(avatar_component_clause,[],[f51]) ).
tff(f53,plain,
( spl5_1
| spl5_2 ),
inference(avatar_split_clause,[],[f43,f51,f48]) ).
tff(f59,definition,
( spl5_4
<=> '$ki_accessible'(sK3,sK4) ),
introduced(definition,[new_symbols(definition,[spl5_4])],[avatar_definition]) ).
tff(f61,plain,
( '$ki_accessible'(sK3,sK4)
| ~ spl5_4 ),
inference(avatar_component_clause,[],[f59]) ).
tff(f62,plain,
( spl5_4
| spl5_2
| spl5_2 ),
inference(avatar_split_clause,[],[f45,f51,f51,f59]) ).
tff(f64,definition,
( spl5_5
<=> open(sK4,d) ),
introduced(definition,[new_symbols(definition,[spl5_5])],[avatar_definition]) ).
tff(f66,plain,
( ~ open(sK4,d)
| spl5_5 ),
inference(avatar_component_clause,[],[f64]) ).
tff(f67,plain,
( ~ spl5_5
| spl5_2
| spl5_2 ),
inference(avatar_split_clause,[],[f46,f51,f51,f64]) ).
tff(f68,plain,
( $false
| ~ spl5_2 ),
inference(resolution,[],[f32,f52]) ).
tff(f69,plain,
~ spl5_2,
inference(avatar_contradiction_clause,[],[f68]) ).
tff(f70,plain,
( ! [X2: $i,X4: '$ki_world'] :
( ~ '$ki_accessible'(sK3,X4)
| h(X4,X2) )
| ~ spl5_1 ),
inference(forward_subsumption_resolution,[],[f49,f32]) ).
tff(f73,plain,
( ! [X0: $i] : h(sK3,X0)
| ~ spl5_1 ),
inference(resolution,[],[f70,f30]) ).
tff(f103,definition,
( spl5_9
<=> ! [X2: '$ki_world'] :
( ~ '$ki_accessible'(X2,sK3)
| ~ '$ki_accessible'('$ki_local_world',X2) ) ),
introduced(definition,[new_symbols(definition,[spl5_9])],[avatar_definition]) ).
tff(f104,plain,
( ! [X2: '$ki_world'] :
( ~ '$ki_accessible'('$ki_local_world',X2)
| ~ '$ki_accessible'(X2,sK3) )
| ~ spl5_9 ),
inference(avatar_component_clause,[],[f103]) ).
tff(f112,plain,
! [X2: $i,X0: '$ki_world',X1: $i,X4: '$ki_world',X5: '$ki_world'] :
( open(X5,X1)
| ~ '$ki_accessible'(X4,X5)
| ~ closed(X4,X1)
| ~ combo(X4,X1,X2)
| ~ h(X4,sK1(X0,X1,X2))
| ~ '$ki_accessible'(X0,X4)
| ~ '$ki_exists_in_world_$i'(X0,X2)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(forward_subsumption_resolution,[],[f35,f32]) ).
tff(f113,plain,
! [X2: $i,X0: '$ki_world',X1: $i,X4: '$ki_world',X5: '$ki_world'] :
( ~ h(X4,sK1(X0,X1,X2))
| ~ '$ki_accessible'(X4,X5)
| ~ closed(X4,X1)
| ~ combo(X4,X1,X2)
| open(X5,X1)
| ~ '$ki_accessible'(X0,X4)
| ~ '$ki_accessible'('$ki_local_world',X0) ),
inference(forward_subsumption_resolution,[],[f112,f32]) ).
tff(f114,plain,
( ~ '$ki_accessible'(sK3,sK3)
| ~ spl5_9 ),
inference(resolution,[],[f104,f42]) ).
tff(f119,plain,
( $false
| ~ spl5_9 ),
inference(forward_subsumption_resolution,[],[f114,f30]) ).
tff(f120,plain,
~ spl5_9,
inference(avatar_contradiction_clause,[],[f119]) ).
tff(f122,plain,
( ! [X2: $i,X3: '$ki_world',X0: '$ki_world',X1: $i] :
( ~ '$ki_accessible'(sK3,X0)
| ~ closed(sK3,X1)
| ~ combo(sK3,X1,X2)
| open(X0,X1)
| ~ '$ki_accessible'(X3,sK3)
| ~ '$ki_accessible'('$ki_local_world',X3) )
| ~ spl5_1 ),
inference(resolution,[],[f113,f73]) ).
tff(f124,definition,
( spl5_12
<=> ! [X2: $i,X0: '$ki_world',X1: $i] :
( ~ '$ki_accessible'(sK3,X0)
| open(X0,X1)
| ~ closed(sK3,X1)
| ~ combo(sK3,X1,X2) ) ),
introduced(definition,[new_symbols(definition,[spl5_12])],[avatar_definition]) ).
tff(f125,plain,
( ! [X2: $i,X0: '$ki_world',X1: $i] :
( ~ combo(sK3,X1,X2)
| open(X0,X1)
| ~ closed(sK3,X1)
| ~ '$ki_accessible'(sK3,X0) )
| ~ spl5_12 ),
inference(avatar_component_clause,[],[f124]) ).
tff(f126,plain,
( spl5_9
| spl5_12
| ~ spl5_1 ),
inference(avatar_split_clause,[],[f122,f48,f124,f103]) ).
tff(f134,plain,
( ! [X0: '$ki_world'] :
( open(X0,d)
| ~ closed(sK3,d)
| ~ '$ki_accessible'(sK3,X0)
| ~ '$ki_accessible'('$ki_local_world',sK3) )
| ~ spl5_12 ),
inference(resolution,[],[f125,f40]) ).
tff(f135,plain,
( ! [X0: '$ki_world'] :
( open(X0,d)
| ~ '$ki_accessible'(sK3,X0)
| ~ '$ki_accessible'('$ki_local_world',sK3) )
| ~ spl5_12 ),
inference(forward_subsumption_resolution,[],[f134,f37]) ).
tff(f138,plain,
( ! [X0: '$ki_world'] :
( ~ '$ki_accessible'(sK3,X0)
| open(X0,d) )
| ~ spl5_12 ),
inference(forward_subsumption_resolution,[],[f135,f42]) ).
tff(f154,plain,
( open(sK4,d)
| ~ spl5_4
| ~ spl5_12 ),
inference(resolution,[],[f138,f61]) ).
tff(f156,plain,
( $false
| ~ spl5_4
| spl5_5
| ~ spl5_12 ),
inference(forward_subsumption_resolution,[],[f154,f66]) ).
tff(f157,plain,
( ~ spl5_4
| spl5_5
| ~ spl5_12 ),
inference(avatar_contradiction_clause,[],[f156]) ).
cnf(s1,plain,
( spl5_1
| spl5_2 ),
inference(sat_conversion,[],[f53]) ).
cnf(s3,plain,
( spl5_2
| spl5_2
| spl5_4 ),
inference(sat_conversion,[],[f62]) ).
cnf(s4,plain,
( spl5_2
| spl5_4 ),
inference(rat,[],[s3]) ).
cnf(s5,plain,
( spl5_2
| spl5_2
| ~ spl5_5 ),
inference(sat_conversion,[],[f67]) ).
cnf(s6,plain,
( spl5_2
| ~ spl5_5 ),
inference(rat,[],[s5]) ).
cnf(s7,plain,
~ spl5_2,
inference(sat_conversion,[],[f69]) ).
cnf(s11,plain,
~ spl5_9,
inference(sat_conversion,[],[f120]) ).
cnf(s12,plain,
( ~ spl5_1
| spl5_9
| spl5_12 ),
inference(sat_conversion,[],[f126]) ).
cnf(s15,plain,
( ~ spl5_4
| spl5_5
| ~ spl5_12 ),
inference(sat_conversion,[],[f157]) ).
cnf(s17,plain,
~ spl5_5,
inference(rat,[],[s6,s7]) ).
cnf(s18,plain,
spl5_4,
inference(rat,[],[s4,s7]) ).
cnf(s19,plain,
~ spl5_12,
inference(rat,[],[s15,s17,s18]) ).
cnf(s20,plain,
~ spl5_1,
inference(rat,[],[s12,s11,s19]) ).
cnf(s22,plain,
$false,
inference(rat,[],[s1,s7,s20]) ).
tff(f158,plain,
$false,
inference(avatar_sat_refutation,[],[s22]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PLA054_4 : TPTP v9.3.1. Released v8.2.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.40 % Computer : n006.cluster.edu
% 0.13/0.40 % Model : x86_64 x86_64
% 0.13/0.40 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.40 % Memory : 8046.5625MB
% 0.13/0.40 % OS : Linux 6.8.0-71-generic
% 0.13/0.40 % CPULimit : 300
% 0.13/0.40 % WCLimit : 300
% 0.13/0.40 % DateTime : Sun Sep 27 22:15:10 UTC 2026
% 0.13/0.40 % CPUTime :
% 0.13/0.40 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 SAT
% 0.13/0.43 Running first-order model finding
% 0.13/0.43 Running: /export/starexec/sandbox/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.19/0.48 % (3377346)Will run a generic schedule for satisfiability detection.
% 0.19/0.48 % (3377362)dis+10_1_sil=32000:sp=arity:random_seed=3176405244:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.19/0.48 % (3377362) found proof, printing to "/export/starexec/sandbox/tmp/vampire-proof-3377346-3377362"...
% 0.19/0.48 % (3377362)...printing done.
% 0.19/0.48 % (3377362)Refutation found. Thanks to Tanya!
% 0.19/0.48 % SZS status Theorem for theBenchmark
% 0.19/0.48 % SZS output start Proof for theBenchmark
% See solution above
% 0.19/0.48 % (3377362)------------------------------
% 0.19/0.48 % (3377362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.19/0.48 % (3377362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.19/0.48 % (3377362)CaDiCaL version: 2.1.3
% 0.19/0.48 % (3377362)Termination reason: Refutation
% 0.19/0.48 % (3377362)Time elapsed: 0.002 s
% 0.19/0.48 % (3377362)Peak memory usage: 12 MB
% 0.19/0.48 % (3377362)Instructions burned: 4 (million)
% 0.19/0.48 % (3377346)Success in time 0.036 s
% 0.19/0.48 % Vampire exiting
%------------------------------------------------------------------------------