%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU376+2 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n026.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:48:36 PM UTC 2026
% Result : Theorem 4.50s 1.78s
% Output : Refutation 6.27s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 9
% Syntax : Number of formulae : 101 ( 16 unt; 4 def)
% Number of atoms : 526 ( 0 equ)
% Maximal formula atoms : 14 ( 5 avg)
% Number of connectives : 703 ( 278 ~; 306 |; 88 &)
% ( 13 <=>; 18 =>; 0 <=; 0 <~>)
% Maximal formula depth : 16 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 16 ( 15 usr; 5 prp; 0-3 aty)
% Number of functors : 12 ( 12 usr; 3 con; 0-4 aty)
% Number of variables : 162 ( 0 sgn 133 !; 29 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f72,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0) )
=> ! [X1] :
( ( ~ empty_carrier(X1)
& net_str(X1,X0) )
=> ! [X2] :
( is_eventually_in(X0,X1,X2)
<=> ? [X3] :
( element(X3,the_carrier(X1))
& ! [X4] :
( element(X4,the_carrier(X1))
=> ( related(X1,X3,X4)
=> in(apply_netmap(X0,X1,X4),X2) ) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d11_waybel_0) ).
fof(f77,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0) )
=> ! [X1] :
( ( ~ empty_carrier(X1)
& net_str(X1,X0) )
=> ! [X2] :
( is_often_in(X0,X1,X2)
<=> ! [X3] :
( element(X3,the_carrier(X1))
=> ? [X4] :
( element(X4,the_carrier(X1))
& related(X1,X3,X4)
& in(apply_netmap(X0,X1,X4),X2) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d12_waybel_0) ).
fof(f160,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& rel_str(X0) )
=> ( directed_relstr(X0)
<=> ! [X1] :
( element(X1,the_carrier(X0))
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ? [X3] :
( element(X3,the_carrier(X0))
& related(X0,X1,X3)
& related(X0,X2,X3) ) ) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d5_yellow_6) ).
fof(f273,axiom,
! [X0] :
( one_sorted_str(X0)
=> ! [X1] :
( net_str(X1,X0)
=> rel_str(X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_waybel_0) ).
fof(f640,conjecture,
! [X0] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0) )
=> ! [X1] :
( ( ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) )
=> ! [X2] :
( is_eventually_in(X0,X1,X2)
=> is_often_in(X0,X1,X2) ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t28_yellow_6) ).
fof(f641,negated_conjecture,
~ ! [X0] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0) )
=> ! [X1] :
( ( ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) )
=> ! [X2] :
( is_eventually_in(X0,X1,X2)
=> is_often_in(X0,X1,X2) ) ) ),
inference(negated_conjecture,[status(cth)],[f640]) ).
fof(f940,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( is_eventually_in(X0,X1,X2)
<=> ? [X3] :
( element(X3,the_carrier(X1))
& ! [X4] :
( in(apply_netmap(X0,X1,X4),X2)
| ~ related(X1,X3,X4)
| ~ element(X4,the_carrier(X1)) ) ) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f72]) ).
fof(f941,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( is_eventually_in(X0,X1,X2)
<=> ? [X3] :
( element(X3,the_carrier(X1))
& ! [X4] :
( in(apply_netmap(X0,X1,X4),X2)
| ~ related(X1,X3,X4)
| ~ element(X4,the_carrier(X1)) ) ) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(flattening,[],[f940]) ).
fof(f947,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( is_often_in(X0,X1,X2)
<=> ! [X3] :
( ? [X4] :
( element(X4,the_carrier(X1))
& related(X1,X3,X4)
& in(apply_netmap(X0,X1,X4),X2) )
| ~ element(X3,the_carrier(X1)) ) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f77]) ).
fof(f948,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( is_often_in(X0,X1,X2)
<=> ! [X3] :
( ? [X4] :
( element(X4,the_carrier(X1))
& related(X1,X3,X4)
& in(apply_netmap(X0,X1,X4),X2) )
| ~ element(X3,the_carrier(X1)) ) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(flattening,[],[f947]) ).
fof(f1042,plain,
! [X0] :
( ( directed_relstr(X0)
<=> ! [X1] :
( ! [X2] :
( ? [X3] :
( element(X3,the_carrier(X0))
& related(X0,X1,X3)
& related(X0,X2,X3) )
| ~ element(X2,the_carrier(X0)) )
| ~ element(X1,the_carrier(X0)) ) )
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(ennf_transformation,[],[f160]) ).
fof(f1043,plain,
! [X0] :
( ( directed_relstr(X0)
<=> ! [X1] :
( ! [X2] :
( ? [X3] :
( element(X3,the_carrier(X0))
& related(X0,X1,X3)
& related(X0,X2,X3) )
| ~ element(X2,the_carrier(X0)) )
| ~ element(X1,the_carrier(X0)) ) )
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(flattening,[],[f1042]) ).
fof(f1161,plain,
! [X0] :
( ! [X1] :
( rel_str(X1)
| ~ net_str(X1,X0) )
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f273]) ).
fof(f1593,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ is_often_in(X0,X1,X2)
& is_eventually_in(X0,X1,X2) )
& ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) )
& ~ empty_carrier(X0)
& one_sorted_str(X0) ),
inference(ennf_transformation,[],[f641]) ).
fof(f1594,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ is_often_in(X0,X1,X2)
& is_eventually_in(X0,X1,X2) )
& ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) )
& ~ empty_carrier(X0)
& one_sorted_str(X0) ),
inference(flattening,[],[f1593]) ).
fof(f1880,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( is_eventually_in(X0,X1,X2)
| ! [X3] :
( ~ element(X3,the_carrier(X1))
| ? [X4] :
( ~ in(apply_netmap(X0,X1,X4),X2)
& related(X1,X3,X4)
& element(X4,the_carrier(X1)) ) ) )
& ( ? [X3] :
( element(X3,the_carrier(X1))
& ! [X4] :
( in(apply_netmap(X0,X1,X4),X2)
| ~ related(X1,X3,X4)
| ~ element(X4,the_carrier(X1)) ) )
| ~ is_eventually_in(X0,X1,X2) ) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(nnf_transformation,[],[f941]) ).
fof(f1881,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( is_eventually_in(X0,X1,X2)
| ! [X3] :
( ~ element(X3,the_carrier(X1))
| ? [X4] :
( ~ in(apply_netmap(X0,X1,X4),X2)
& related(X1,X3,X4)
& element(X4,the_carrier(X1)) ) ) )
& ( ? [X5] :
( element(X5,the_carrier(X1))
& ! [X6] :
( in(apply_netmap(X0,X1,X6),X2)
| ~ related(X1,X5,X6)
| ~ element(X6,the_carrier(X1)) ) )
| ~ is_eventually_in(X0,X1,X2) ) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(rectify,[],[f1880]) ).
fof(f1882,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( is_eventually_in(X0,X1,X2)
| ! [X3] :
( ~ element(X3,the_carrier(X1))
| ( ~ in(apply_netmap(X0,X1,sK71(X0,X1,X2,X3)),X2)
& related(X1,X3,sK71(X0,X1,X2,X3))
& element(sK71(X0,X1,X2,X3),the_carrier(X1)) ) ) )
& ( ( element(sK72(X0,X1,X2),the_carrier(X1))
& ! [X6] :
( in(apply_netmap(X0,X1,X6),X2)
| ~ related(X1,sK72(X0,X1,X2),X6)
| ~ element(X6,the_carrier(X1)) ) )
| ~ is_eventually_in(X0,X1,X2) ) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK71,sK72]),skolemize(X4,sK71(X0,X1,X2,X3)),skolemize(X5,sK72(X0,X1,X2))],[f1881]) ).
fof(f1891,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( is_often_in(X0,X1,X2)
| ? [X3] :
( ! [X4] :
( ~ element(X4,the_carrier(X1))
| ~ related(X1,X3,X4)
| ~ in(apply_netmap(X0,X1,X4),X2) )
& element(X3,the_carrier(X1)) ) )
& ( ! [X3] :
( ? [X4] :
( element(X4,the_carrier(X1))
& related(X1,X3,X4)
& in(apply_netmap(X0,X1,X4),X2) )
| ~ element(X3,the_carrier(X1)) )
| ~ is_often_in(X0,X1,X2) ) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(nnf_transformation,[],[f948]) ).
fof(f1892,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( is_often_in(X0,X1,X2)
| ? [X3] :
( ! [X4] :
( ~ element(X4,the_carrier(X1))
| ~ related(X1,X3,X4)
| ~ in(apply_netmap(X0,X1,X4),X2) )
& element(X3,the_carrier(X1)) ) )
& ( ! [X5] :
( ? [X6] :
( element(X6,the_carrier(X1))
& related(X1,X5,X6)
& in(apply_netmap(X0,X1,X6),X2) )
| ~ element(X5,the_carrier(X1)) )
| ~ is_often_in(X0,X1,X2) ) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(rectify,[],[f1891]) ).
fof(f1893,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( is_often_in(X0,X1,X2)
| ( ! [X4] :
( ~ element(X4,the_carrier(X1))
| ~ related(X1,sK78(X0,X1,X2),X4)
| ~ in(apply_netmap(X0,X1,X4),X2) )
& element(sK78(X0,X1,X2),the_carrier(X1)) ) )
& ( ! [X5] :
( ( element(sK79(X0,X1,X2,X5),the_carrier(X1))
& related(X1,X5,sK79(X0,X1,X2,X5))
& in(apply_netmap(X0,X1,sK79(X0,X1,X2,X5)),X2) )
| ~ element(X5,the_carrier(X1)) )
| ~ is_often_in(X0,X1,X2) ) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK78,sK79]),skolemize(X3,sK78(X0,X1,X2)),skolemize(X6,sK79(X0,X1,X2,X5))],[f1892]) ).
fof(f2082,plain,
! [X0] :
( ( ( directed_relstr(X0)
| ? [X1] :
( ? [X2] :
( ! [X3] :
( ~ element(X3,the_carrier(X0))
| ~ related(X0,X1,X3)
| ~ related(X0,X2,X3) )
& element(X2,the_carrier(X0)) )
& element(X1,the_carrier(X0)) ) )
& ( ! [X1] :
( ! [X2] :
( ? [X3] :
( element(X3,the_carrier(X0))
& related(X0,X1,X3)
& related(X0,X2,X3) )
| ~ element(X2,the_carrier(X0)) )
| ~ element(X1,the_carrier(X0)) )
| ~ directed_relstr(X0) ) )
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(nnf_transformation,[],[f1043]) ).
fof(f2083,plain,
! [X0] :
( ( ( directed_relstr(X0)
| ? [X1] :
( ? [X2] :
( ! [X3] :
( ~ element(X3,the_carrier(X0))
| ~ related(X0,X1,X3)
| ~ related(X0,X2,X3) )
& element(X2,the_carrier(X0)) )
& element(X1,the_carrier(X0)) ) )
& ( ! [X4] :
( ! [X5] :
( ? [X6] :
( element(X6,the_carrier(X0))
& related(X0,X4,X6)
& related(X0,X5,X6) )
| ~ element(X5,the_carrier(X0)) )
| ~ element(X4,the_carrier(X0)) )
| ~ directed_relstr(X0) ) )
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(rectify,[],[f2082]) ).
fof(f2084,plain,
! [X0] :
( ( ( directed_relstr(X0)
| ( ! [X3] :
( ~ element(X3,the_carrier(X0))
| ~ related(X0,sK169(X0),X3)
| ~ related(X0,sK170(X0),X3) )
& element(sK170(X0),the_carrier(X0))
& element(sK169(X0),the_carrier(X0)) ) )
& ( ! [X4] :
( ! [X5] :
( ( element(sK171(X0,X4,X5),the_carrier(X0))
& related(X0,X4,sK171(X0,X4,X5))
& related(X0,X5,sK171(X0,X4,X5)) )
| ~ element(X5,the_carrier(X0)) )
| ~ element(X4,the_carrier(X0)) )
| ~ directed_relstr(X0) ) )
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK169,sK170,sK171]),skolemize(X1,sK169(X0)),skolemize(X2,sK170(X0)),skolemize(X6,sK171(X0,X4,X5))],[f2083]) ).
fof(f2553,plain,
( ~ is_often_in(sK553,sK554,sK555)
& is_eventually_in(sK553,sK554,sK555)
& ~ empty_carrier(sK554)
& transitive_relstr(sK554)
& directed_relstr(sK554)
& net_str(sK554,sK553)
& ~ empty_carrier(sK553)
& one_sorted_str(sK553) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK553,sK554,sK555]),skolemize(X0,sK553),skolemize(X1,sK554),skolemize(X2,sK555)],[f1594]) ).
fof(f2796,plain,
! [X2,X0,X1,X6] :
( ~ net_str(X1,X0)
| ~ related(X1,sK72(X0,X1,X2),X6)
| ~ element(X6,the_carrier(X1))
| ~ is_eventually_in(X0,X1,X2)
| empty_carrier(X1)
| in(apply_netmap(X0,X1,X6),X2)
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f1882]) ).
fof(f2797,plain,
! [X2,X0,X1] :
( element(sK72(X0,X1,X2),the_carrier(X1))
| ~ is_eventually_in(X0,X1,X2)
| empty_carrier(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f1882]) ).
fof(f2821,plain,
! [X2,X0,X1] :
( element(sK78(X0,X1,X2),the_carrier(X1))
| is_often_in(X0,X1,X2)
| empty_carrier(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f1893]) ).
fof(f2822,plain,
! [X2,X0,X1,X4] :
( ~ in(apply_netmap(X0,X1,X4),X2)
| ~ element(X4,the_carrier(X1))
| ~ related(X1,sK78(X0,X1,X2),X4)
| is_often_in(X0,X1,X2)
| empty_carrier(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f1893]) ).
fof(f3161,plain,
! [X0,X4,X5] :
( related(X0,X5,sK171(X0,X4,X5))
| ~ element(X5,the_carrier(X0))
| ~ element(X4,the_carrier(X0))
| ~ directed_relstr(X0)
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f2084]) ).
fof(f3162,plain,
! [X0,X4,X5] :
( related(X0,X4,sK171(X0,X4,X5))
| ~ element(X5,the_carrier(X0))
| ~ element(X4,the_carrier(X0))
| ~ directed_relstr(X0)
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f2084]) ).
fof(f3163,plain,
! [X0,X4,X5] :
( element(sK171(X0,X4,X5),the_carrier(X0))
| ~ element(X5,the_carrier(X0))
| ~ element(X4,the_carrier(X0))
| ~ directed_relstr(X0)
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f2084]) ).
fof(f3366,plain,
! [X0,X1] :
( rel_str(X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f1161]) ).
fof(f4700,plain,
one_sorted_str(sK553),
inference(cnf_transformation,[],[f2553]) ).
fof(f4701,plain,
~ empty_carrier(sK553),
inference(cnf_transformation,[],[f2553]) ).
fof(f4702,plain,
net_str(sK554,sK553),
inference(cnf_transformation,[],[f2553]) ).
fof(f4703,plain,
directed_relstr(sK554),
inference(cnf_transformation,[],[f2553]) ).
fof(f4705,plain,
~ empty_carrier(sK554),
inference(cnf_transformation,[],[f2553]) ).
fof(f4706,plain,
is_eventually_in(sK553,sK554,sK555),
inference(cnf_transformation,[],[f2553]) ).
fof(f4707,plain,
~ is_often_in(sK553,sK554,sK555),
inference(cnf_transformation,[],[f2553]) ).
fof(f5593,plain,
! [X0,X1] :
( ~ related(sK554,sK72(sK553,sK554,X0),X1)
| ~ element(X1,the_carrier(sK554))
| ~ is_eventually_in(sK553,sK554,X0)
| empty_carrier(sK554)
| in(apply_netmap(sK553,sK554,X1),X0)
| empty_carrier(sK553)
| ~ one_sorted_str(sK553) ),
inference(resolution,[],[f2796,f4702]) ).
fof(f5598,plain,
! [X0,X1] :
( ~ related(sK554,sK72(sK553,sK554,X0),X1)
| ~ element(X1,the_carrier(sK554))
| ~ is_eventually_in(sK553,sK554,X0)
| in(apply_netmap(sK553,sK554,X1),X0)
| empty_carrier(sK553)
| ~ one_sorted_str(sK553) ),
inference(forward_subsumption_resolution,[],[f5593,f4705]) ).
fof(f5599,plain,
! [X0,X1] :
( ~ related(sK554,sK72(sK553,sK554,X0),X1)
| ~ element(X1,the_carrier(sK554))
| ~ is_eventually_in(sK553,sK554,X0)
| in(apply_netmap(sK553,sK554,X1),X0)
| ~ one_sorted_str(sK553) ),
inference(forward_subsumption_resolution,[],[f5598,f4701]) ).
fof(f5600,plain,
! [X0,X1] :
( ~ is_eventually_in(sK553,sK554,X0)
| ~ element(X1,the_carrier(sK554))
| ~ related(sK554,sK72(sK553,sK554,X0),X1)
| in(apply_netmap(sK553,sK554,X1),X0) ),
inference(forward_subsumption_resolution,[],[f5599,f4700]) ).
fof(f5601,plain,
! [X0] :
( in(apply_netmap(sK553,sK554,X0),sK555)
| ~ related(sK554,sK72(sK553,sK554,sK555),X0)
| ~ element(X0,the_carrier(sK554)) ),
inference(resolution,[],[f5600,f4706]) ).
fof(f5619,plain,
! [X0] :
( ~ related(sK554,sK72(sK553,sK554,sK555),X0)
| ~ element(X0,the_carrier(sK554))
| ~ element(X0,the_carrier(sK554))
| ~ related(sK554,sK78(sK553,sK554,sK555),X0)
| is_often_in(sK553,sK554,sK555)
| empty_carrier(sK554)
| ~ net_str(sK554,sK553)
| empty_carrier(sK553)
| ~ one_sorted_str(sK553) ),
inference(resolution,[],[f5601,f2822]) ).
fof(f5620,plain,
! [X0] :
( ~ related(sK554,sK72(sK553,sK554,sK555),X0)
| ~ element(X0,the_carrier(sK554))
| ~ related(sK554,sK78(sK553,sK554,sK555),X0)
| is_often_in(sK553,sK554,sK555)
| empty_carrier(sK554)
| ~ net_str(sK554,sK553)
| empty_carrier(sK553)
| ~ one_sorted_str(sK553) ),
inference(duplicate_literal_removal,[],[f5619]) ).
fof(f5621,plain,
! [X0] :
( ~ related(sK554,sK72(sK553,sK554,sK555),X0)
| ~ element(X0,the_carrier(sK554))
| ~ related(sK554,sK78(sK553,sK554,sK555),X0)
| empty_carrier(sK554)
| ~ net_str(sK554,sK553)
| empty_carrier(sK553)
| ~ one_sorted_str(sK553) ),
inference(forward_subsumption_resolution,[],[f5620,f4707]) ).
fof(f5622,plain,
! [X0] :
( ~ related(sK554,sK72(sK553,sK554,sK555),X0)
| ~ element(X0,the_carrier(sK554))
| ~ related(sK554,sK78(sK553,sK554,sK555),X0)
| ~ net_str(sK554,sK553)
| empty_carrier(sK553)
| ~ one_sorted_str(sK553) ),
inference(forward_subsumption_resolution,[],[f5621,f4705]) ).
fof(f5623,plain,
! [X0] :
( ~ related(sK554,sK72(sK553,sK554,sK555),X0)
| ~ element(X0,the_carrier(sK554))
| ~ related(sK554,sK78(sK553,sK554,sK555),X0)
| empty_carrier(sK553)
| ~ one_sorted_str(sK553) ),
inference(forward_subsumption_resolution,[],[f5622,f4702]) ).
fof(f5624,plain,
! [X0] :
( ~ related(sK554,sK72(sK553,sK554,sK555),X0)
| ~ element(X0,the_carrier(sK554))
| ~ related(sK554,sK78(sK553,sK554,sK555),X0)
| ~ one_sorted_str(sK553) ),
inference(forward_subsumption_resolution,[],[f5623,f4701]) ).
fof(f5625,plain,
! [X0] :
( ~ related(sK554,sK78(sK553,sK554,sK555),X0)
| ~ element(X0,the_carrier(sK554))
| ~ related(sK554,sK72(sK553,sK554,sK555),X0) ),
inference(forward_subsumption_resolution,[],[f5624,f4700]) ).
fof(f5630,plain,
! [X0] :
( ~ element(sK171(sK554,sK78(sK553,sK554,sK555),X0),the_carrier(sK554))
| ~ related(sK554,sK72(sK553,sK554,sK555),sK171(sK554,sK78(sK553,sK554,sK555),X0))
| ~ element(X0,the_carrier(sK554))
| ~ element(sK78(sK553,sK554,sK555),the_carrier(sK554))
| ~ directed_relstr(sK554)
| empty_carrier(sK554)
| ~ rel_str(sK554) ),
inference(resolution,[],[f5625,f3162]) ).
fof(f5632,plain,
! [X0] :
( ~ related(sK554,sK72(sK553,sK554,sK555),sK171(sK554,sK78(sK553,sK554,sK555),X0))
| ~ element(X0,the_carrier(sK554))
| ~ element(sK78(sK553,sK554,sK555),the_carrier(sK554))
| ~ directed_relstr(sK554)
| empty_carrier(sK554)
| ~ rel_str(sK554) ),
inference(forward_subsumption_resolution,[],[f5630,f3163]) ).
fof(f5637,plain,
! [X0] :
( ~ related(sK554,sK72(sK553,sK554,sK555),sK171(sK554,sK78(sK553,sK554,sK555),X0))
| ~ element(X0,the_carrier(sK554))
| ~ element(sK78(sK553,sK554,sK555),the_carrier(sK554))
| empty_carrier(sK554)
| ~ rel_str(sK554) ),
inference(forward_subsumption_resolution,[],[f5632,f4703]) ).
fof(f5642,definition,
( spl578_59
<=> rel_str(sK554) ),
introduced(definition,[new_symbols(definition,[spl578_59])],[avatar_definition]) ).
fof(f5643,plain,
( rel_str(sK554)
| ~ spl578_59 ),
inference(avatar_component_clause,[],[f5642]) ).
fof(f5644,plain,
( ~ rel_str(sK554)
| spl578_59 ),
inference(avatar_component_clause,[],[f5642]) ).
fof(f5646,definition,
( spl578_60
<=> element(sK78(sK553,sK554,sK555),the_carrier(sK554)) ),
introduced(definition,[new_symbols(definition,[spl578_60])],[avatar_definition]) ).
fof(f5647,plain,
( element(sK78(sK553,sK554,sK555),the_carrier(sK554))
| ~ spl578_60 ),
inference(avatar_component_clause,[],[f5646]) ).
fof(f5648,plain,
( ~ element(sK78(sK553,sK554,sK555),the_carrier(sK554))
| spl578_60 ),
inference(avatar_component_clause,[],[f5646]) ).
fof(f5653,plain,
! [X0] :
( ~ related(sK554,sK72(sK553,sK554,sK555),sK171(sK554,sK78(sK553,sK554,sK555),X0))
| ~ element(X0,the_carrier(sK554))
| ~ element(sK78(sK553,sK554,sK555),the_carrier(sK554))
| ~ rel_str(sK554) ),
inference(forward_subsumption_resolution,[],[f5637,f4705]) ).
fof(f5664,definition,
( spl578_64
<=> ! [X0] :
( ~ related(sK554,sK72(sK553,sK554,sK555),sK171(sK554,sK78(sK553,sK554,sK555),X0))
| ~ element(X0,the_carrier(sK554)) ) ),
introduced(definition,[new_symbols(definition,[spl578_64])],[avatar_definition]) ).
fof(f5665,plain,
( ! [X0] :
( ~ related(sK554,sK72(sK553,sK554,sK555),sK171(sK554,sK78(sK553,sK554,sK555),X0))
| ~ element(X0,the_carrier(sK554)) )
| ~ spl578_64 ),
inference(avatar_component_clause,[],[f5664]) ).
fof(f5666,plain,
( ~ spl578_59
| ~ spl578_60
| spl578_64 ),
inference(avatar_split_clause,[],[f5653,f5664,f5646,f5642]) ).
fof(f5671,plain,
( is_often_in(sK553,sK554,sK555)
| empty_carrier(sK554)
| ~ net_str(sK554,sK553)
| empty_carrier(sK553)
| ~ one_sorted_str(sK553)
| spl578_60 ),
inference(resolution,[],[f5648,f2821]) ).
fof(f5672,plain,
( empty_carrier(sK554)
| ~ net_str(sK554,sK553)
| empty_carrier(sK553)
| ~ one_sorted_str(sK553)
| spl578_60 ),
inference(forward_subsumption_resolution,[],[f5671,f4707]) ).
fof(f5673,plain,
( ~ net_str(sK554,sK553)
| empty_carrier(sK553)
| ~ one_sorted_str(sK553)
| spl578_60 ),
inference(forward_subsumption_resolution,[],[f5672,f4705]) ).
fof(f5674,plain,
( empty_carrier(sK553)
| ~ one_sorted_str(sK553)
| spl578_60 ),
inference(forward_subsumption_resolution,[],[f5673,f4702]) ).
fof(f5675,plain,
( ~ one_sorted_str(sK553)
| spl578_60 ),
inference(forward_subsumption_resolution,[],[f5674,f4701]) ).
fof(f5676,plain,
( $false
| spl578_60 ),
inference(forward_subsumption_resolution,[],[f5675,f4700]) ).
fof(f5677,plain,
spl578_60,
inference(avatar_contradiction_clause,[],[f5676]) ).
fof(f5678,plain,
( ! [X0] :
( ~ net_str(sK554,X0)
| ~ one_sorted_str(X0) )
| spl578_59 ),
inference(resolution,[],[f5644,f3366]) ).
fof(f5679,plain,
( ~ one_sorted_str(sK553)
| spl578_59 ),
inference(resolution,[],[f5678,f4702]) ).
fof(f5682,plain,
( $false
| spl578_59 ),
inference(forward_subsumption_resolution,[],[f5679,f4700]) ).
fof(f5683,plain,
spl578_59,
inference(avatar_contradiction_clause,[],[f5682]) ).
fof(f5706,plain,
( ~ element(sK72(sK553,sK554,sK555),the_carrier(sK554))
| ~ element(sK72(sK553,sK554,sK555),the_carrier(sK554))
| ~ element(sK78(sK553,sK554,sK555),the_carrier(sK554))
| ~ directed_relstr(sK554)
| empty_carrier(sK554)
| ~ rel_str(sK554)
| ~ spl578_64 ),
inference(resolution,[],[f5665,f3161]) ).
fof(f5709,plain,
( ~ element(sK72(sK553,sK554,sK555),the_carrier(sK554))
| ~ element(sK78(sK553,sK554,sK555),the_carrier(sK554))
| ~ directed_relstr(sK554)
| empty_carrier(sK554)
| ~ rel_str(sK554)
| ~ spl578_64 ),
inference(duplicate_literal_removal,[],[f5706]) ).
fof(f5712,definition,
( spl578_69
<=> element(sK72(sK553,sK554,sK555),the_carrier(sK554)) ),
introduced(definition,[new_symbols(definition,[spl578_69])],[avatar_definition]) ).
fof(f5714,plain,
( ~ element(sK72(sK553,sK554,sK555),the_carrier(sK554))
| spl578_69 ),
inference(avatar_component_clause,[],[f5712]) ).
fof(f5719,plain,
( ~ element(sK72(sK553,sK554,sK555),the_carrier(sK554))
| ~ directed_relstr(sK554)
| empty_carrier(sK554)
| ~ rel_str(sK554)
| ~ spl578_60
| ~ spl578_64 ),
inference(forward_subsumption_resolution,[],[f5709,f5647]) ).
fof(f5721,plain,
( ~ element(sK72(sK553,sK554,sK555),the_carrier(sK554))
| empty_carrier(sK554)
| ~ rel_str(sK554)
| ~ spl578_60
| ~ spl578_64 ),
inference(forward_subsumption_resolution,[],[f5719,f4703]) ).
fof(f5726,plain,
( ~ element(sK72(sK553,sK554,sK555),the_carrier(sK554))
| ~ rel_str(sK554)
| ~ spl578_60
| ~ spl578_64 ),
inference(forward_subsumption_resolution,[],[f5721,f4705]) ).
fof(f5727,plain,
( ~ element(sK72(sK553,sK554,sK555),the_carrier(sK554))
| ~ spl578_59
| ~ spl578_60
| ~ spl578_64 ),
inference(forward_subsumption_resolution,[],[f5726,f5643]) ).
fof(f5728,plain,
( ~ spl578_69
| ~ spl578_59
| ~ spl578_60
| ~ spl578_64 ),
inference(avatar_split_clause,[],[f5727,f5664,f5646,f5642,f5712]) ).
fof(f5729,plain,
( ~ is_eventually_in(sK553,sK554,sK555)
| empty_carrier(sK554)
| ~ net_str(sK554,sK553)
| empty_carrier(sK553)
| ~ one_sorted_str(sK553)
| spl578_69 ),
inference(resolution,[],[f5714,f2797]) ).
fof(f5730,plain,
( empty_carrier(sK554)
| ~ net_str(sK554,sK553)
| empty_carrier(sK553)
| ~ one_sorted_str(sK553)
| spl578_69 ),
inference(forward_subsumption_resolution,[],[f5729,f4706]) ).
fof(f5731,plain,
( ~ net_str(sK554,sK553)
| empty_carrier(sK553)
| ~ one_sorted_str(sK553)
| spl578_69 ),
inference(forward_subsumption_resolution,[],[f5730,f4705]) ).
fof(f5732,plain,
( empty_carrier(sK553)
| ~ one_sorted_str(sK553)
| spl578_69 ),
inference(forward_subsumption_resolution,[],[f5731,f4702]) ).
fof(f5733,plain,
( ~ one_sorted_str(sK553)
| spl578_69 ),
inference(forward_subsumption_resolution,[],[f5732,f4701]) ).
fof(f5734,plain,
( $false
| spl578_69 ),
inference(forward_subsumption_resolution,[],[f5733,f4700]) ).
fof(f5735,plain,
spl578_69,
inference(avatar_contradiction_clause,[],[f5734]) ).
cnf(s59,plain,
( ~ spl578_59
| ~ spl578_60
| spl578_64 ),
inference(sat_conversion,[],[f5666]) ).
cnf(s61,plain,
spl578_60,
inference(sat_conversion,[],[f5677]) ).
cnf(s62,plain,
spl578_59,
inference(sat_conversion,[],[f5683]) ).
cnf(s68,plain,
( ~ spl578_59
| ~ spl578_60
| ~ spl578_64
| ~ spl578_69 ),
inference(sat_conversion,[],[f5728]) ).
cnf(s69,plain,
spl578_69,
inference(sat_conversion,[],[f5735]) ).
cnf(s70,plain,
( ~ spl578_59
| ~ spl578_60
| ~ spl578_64 ),
inference(rat,[],[s68,s69]) ).
cnf(s74,plain,
~ spl578_64,
inference(rat,[],[s70,s62,s61]) ).
cnf(s78,plain,
$false,
inference(rat,[],[s59,s74,s61,s62]) ).
fof(f5736,plain,
$false,
inference(avatar_sat_refutation,[],[s78]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU376+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.16/0.42 % Computer : n026.cluster.edu
% 0.16/0.42 % Model : x86_64 x86_64
% 0.16/0.42 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.42 % Memory : 8046.5625MB
% 0.16/0.42 % OS : Linux 6.8.0-71-generic
% 0.16/0.42 % CPULimit : 300
% 0.16/0.42 % WCLimit : 300
% 0.16/0.42 % DateTime : Mon Sep 28 05:02:11 UTC 2026
% 0.16/0.43 % CPUTime :
% 0.16/0.43 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.20/0.48 Running first-order theorem proving
% 0.20/0.48 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 4.50/1.78 % (3471262)Detected formulas, will run a generic FOF schedule.
% 4.50/1.78 % (3471268)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=140172773:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 4.50/1.78 % (3471271)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3791930650:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 4.50/1.78 % (3471270)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1474218862:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 4.50/1.78 % (3471269)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=2545048115:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 4.50/1.78 % (3471267)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=3868516349:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 4.50/1.78 % (3471273)dis-21_1_sil=8000:lcm=predicate:random_seed=1518310838: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)
% 4.50/1.78 % (3471272)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=958216189:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 4.50/1.78 % (3471270)Instruction limit reached!
% 4.50/1.78 % (3471270)------------------------------
% 4.50/1.78 % (3471270)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.50/1.78 % (3471270)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.50/1.78 % (3471270)CaDiCaL version: 2.1.3
% 4.50/1.78 % (3471270)Termination reason: Instruction limit
% 4.50/1.78 % (3471270)Termination phase: Blocked clause elimination
% 4.50/1.78 % (3471270)Time elapsed: 0.103 s
% 4.50/1.78 % (3471270)Peak memory usage: 90 MB
% 4.50/1.78 % (3471270)Instructions burned: 110 (million)
% 4.50/1.78 % (3471271)Instruction limit reached!
% 4.50/1.78 % (3471271)------------------------------
% 4.50/1.78 % (3471271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.50/1.78 % (3471271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.50/1.78 % (3471271)CaDiCaL version: 2.1.3
% 4.50/1.78 % (3471271)Termination reason: Instruction limit
% 4.50/1.78 % (3471271)Termination phase: Saturation
% 4.50/1.78 % (3471271)Time elapsed: 0.122 s
% 4.50/1.78 % (3471271)Peak memory usage: 91 MB
% 4.50/1.78 % (3471271)Instructions burned: 119 (million)
% 4.50/1.78 % (3471273)Instruction limit reached!
% 4.50/1.78 % (3471273)------------------------------
% 4.50/1.78 % (3471273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 4.50/1.78 % (3471273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 4.50/1.78 % (3471273)CaDiCaL version: 2.1.3
% 4.50/1.78 % (3471273)Termination reason: Instruction limit
% 4.50/1.78 % (3471273)Termination phase: Saturation
% 4.50/1.78 % (3471273)Time elapsed: 0.118 s
% 4.50/1.78 % (3471273)Peak memory usage: 92 MB
% 4.50/1.78 % (3471273)Instructions burned: 130 (million)
% 4.50/1.78 % (3471272)First to succeed.
% 4.50/1.78 % (3471272)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3471262"
% 4.50/1.78 % (3471282)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2650630294:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/157Mi)
% 4.50/1.78 % (3471281)lrs+10_1_sil=8000:sp=occurrence:random_seed=2878494333:i=285:sd=3:ss=axioms:sgt=8_2996 on theBenchmark for (2996ds/285Mi)
% 4.50/1.78 % (3471282)Also succeeded, but the first one will report.
% 4.50/1.78 % (3471283)lrs+1011_1_sil=32000:sp=occurrence:random_seed=660487621:i=325:sd=1:ss=axioms:sgt=32_2996 on theBenchmark for (2996ds/325Mi)
% 4.50/1.78 % (3471272)Refutation found. Thanks to Tanya!
% 4.50/1.78 % SZS status Theorem for theBenchmark
% 4.50/1.78 % SZS output start Proof for theBenchmark
% See solution above
% 6.27/2.01 % (3471272)------------------------------
% 6.27/2.01 % (3471272)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.27/2.01 % (3471272)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.27/2.01 % (3471272)CaDiCaL version: 2.1.3
% 6.27/2.01 % (3471272)Termination reason: Refutation
% 6.27/2.01 % (3471272)Time elapsed: 0.129 s
% 6.27/2.01 % (3471272)Peak memory usage: 93 MB
% 6.27/2.01 % (3471272)Instructions burned: 132 (million)
% 6.27/2.01 % (3471272)------------------------------
% 6.27/2.01 % (3471272)------------------------------
% 6.27/2.01 % (3471262)Success in time 0.823 s
% 6.27/2.01 % Vampire exiting
%------------------------------------------------------------------------------