%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU401+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 : 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:48:44 PM UTC 2026
% Result : Theorem 9.23s 3.04s
% Output : Refutation 15.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 27
% Number of leaves : 27
% Syntax : Number of formulae : 241 ( 29 unt; 17 def)
% Number of atoms : 878 ( 167 equ)
% Maximal formula atoms : 36 ( 3 avg)
% Number of connectives : 1037 ( 400 ~; 407 |; 185 &)
% ( 30 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 25 ( 4 avg)
% Maximal term depth : 6 ( 2 avg)
% Number of predicates : 32 ( 30 usr; 18 prp; 0-3 aty)
% Number of functors : 16 ( 16 usr; 5 con; 0-3 aty)
% Number of variables : 208 ( 2 sgn 149 !; 59 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f98,axiom,
! [X0,X1] :
( X0 = X1
<=> ( subset(X0,X1)
& subset(X1,X0) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d10_xboole_0) ).
fof(f175,axiom,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X0)
=> in(X2,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',d3_tarski) ).
fof(f325,axiom,
! [X0] :
( rel_str(X0)
=> one_sorted_str(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_orders_2) ).
fof(f326,axiom,
! [X0] :
( top_str(X0)
=> one_sorted_str(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',dt_l1_pre_topc) ).
fof(f328,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(f386,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0) )
=> ~ empty(the_carrier(X0)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f680,conjecture,
! [X0,X1,X2] :
( ( ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0)
& ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) )
=> ! [X3,X4,X5] :
( ( ! [X6] :
( in(X6,X4)
<=> ( in(X6,the_carrier(X1))
& ? [X7] :
( netstr_induced_subset(X7,X0,X1)
& ? [X8] :
( element(X8,the_carrier(X1))
& X3 = topstr_closure(X0,X7)
& X6 = X8
& X7 = relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X8)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X8))) ) ) ) )
& ! [X6] :
( in(X6,X5)
<=> ( in(X6,the_carrier(X1))
& ? [X9] :
( netstr_induced_subset(X9,X0,X1)
& ? [X10] :
( element(X10,the_carrier(X1))
& X3 = topstr_closure(X0,X9)
& X6 = X10
& X9 = relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X10)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X10))) ) ) ) ) )
=> X4 = X5 ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',s2_xboole_0__e6_39_3__yellow19__1) ).
fof(f681,negated_conjecture,
~ ! [X0,X1,X2] :
( ( ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0)
& ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) )
=> ! [X3,X4,X5] :
( ( ! [X6] :
( in(X6,X4)
<=> ( in(X6,the_carrier(X1))
& ? [X7] :
( netstr_induced_subset(X7,X0,X1)
& ? [X8] :
( element(X8,the_carrier(X1))
& X3 = topstr_closure(X0,X7)
& X6 = X8
& X7 = relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X8)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X8))) ) ) ) )
& ! [X6] :
( in(X6,X5)
<=> ( in(X6,the_carrier(X1))
& ? [X9] :
( netstr_induced_subset(X9,X0,X1)
& ? [X10] :
( element(X10,the_carrier(X1))
& X3 = topstr_closure(X0,X9)
& X6 = X10
& X9 = relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X10)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X10))) ) ) ) ) )
=> X4 = X5 ) ),
inference(negated_conjecture,[status(cth)],[f680]) ).
fof(f701,axiom,
! [X0] :
( one_sorted_str(X0)
=> cast_as_carrier_subset(X0) = the_carrier(X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t12_pre_topc) ).
fof(f749,axiom,
! [X0,X1] :
( in(X0,X1)
=> element(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t1_subset) ).
fof(f795,axiom,
! [X0,X1] :
( element(X0,X1)
=> ( empty(X1)
| in(X0,X1) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',t2_subset) ).
fof(f975,plain,
~ ! [X0,X1] :
( ( ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0)
& ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) )
=> ! [X3,X4,X5] :
( ( ! [X6] :
( in(X6,X4)
<=> ( in(X6,the_carrier(X1))
& ? [X7] :
( netstr_induced_subset(X7,X0,X1)
& ? [X8] :
( element(X8,the_carrier(X1))
& X3 = topstr_closure(X0,X7)
& X6 = X8
& X7 = relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X8)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X8))) ) ) ) )
& ! [X9] :
( in(X9,X5)
<=> ( in(X9,the_carrier(X1))
& ? [X10] :
( netstr_induced_subset(X10,X0,X1)
& ? [X11] :
( element(X11,the_carrier(X1))
& topstr_closure(X0,X10) = X3
& X9 = X11
& relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X11)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X11))) = X10 ) ) ) ) )
=> X4 = X5 ) ),
inference(rectify,[],[f681]) ).
fof(f1243,plain,
! [X0,X1] :
( subset(X0,X1)
<=> ! [X2] :
( in(X2,X1)
| ~ in(X2,X0) ) ),
inference(ennf_transformation,[],[f175]) ).
fof(f1414,plain,
! [X0] :
( one_sorted_str(X0)
| ~ rel_str(X0) ),
inference(ennf_transformation,[],[f325]) ).
fof(f1415,plain,
! [X0] :
( one_sorted_str(X0)
| ~ top_str(X0) ),
inference(ennf_transformation,[],[f326]) ).
fof(f1416,plain,
! [X0] :
( ! [X1] :
( rel_str(X1)
| ~ net_str(X1,X0) )
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f328]) ).
fof(f1478,plain,
! [X0] :
( ~ empty(the_carrier(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f386]) ).
fof(f1479,plain,
! [X0] :
( ~ empty(the_carrier(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(flattening,[],[f1478]) ).
fof(f1836,plain,
? [X0,X1] :
( ? [X3,X4,X5] :
( X4 != X5
& ! [X6] :
( in(X6,X4)
<=> ( in(X6,the_carrier(X1))
& ? [X7] :
( netstr_induced_subset(X7,X0,X1)
& ? [X8] :
( element(X8,the_carrier(X1))
& X3 = topstr_closure(X0,X7)
& X6 = X8
& X7 = relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X8)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X8))) ) ) ) )
& ! [X9] :
( in(X9,X5)
<=> ( in(X9,the_carrier(X1))
& ? [X10] :
( netstr_induced_subset(X10,X0,X1)
& ? [X11] :
( element(X11,the_carrier(X1))
& topstr_closure(X0,X10) = X3
& X9 = X11
& relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X11)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X11))) = X10 ) ) ) ) )
& ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0)
& ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) ),
inference(ennf_transformation,[],[f975]) ).
fof(f1837,plain,
? [X0,X1] :
( ? [X3,X4,X5] :
( X4 != X5
& ! [X6] :
( in(X6,X4)
<=> ( in(X6,the_carrier(X1))
& ? [X7] :
( netstr_induced_subset(X7,X0,X1)
& ? [X8] :
( element(X8,the_carrier(X1))
& X3 = topstr_closure(X0,X7)
& X6 = X8
& X7 = relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X8)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X8))) ) ) ) )
& ! [X9] :
( in(X9,X5)
<=> ( in(X9,the_carrier(X1))
& ? [X10] :
( netstr_induced_subset(X10,X0,X1)
& ? [X11] :
( element(X11,the_carrier(X1))
& topstr_closure(X0,X10) = X3
& X9 = X11
& relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X11)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X11))) = X10 ) ) ) ) )
& ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0)
& ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) ),
inference(flattening,[],[f1836]) ).
fof(f1861,plain,
! [X0] :
( cast_as_carrier_subset(X0) = the_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f701]) ).
fof(f1929,plain,
! [X0,X1] :
( element(X0,X1)
| ~ in(X0,X1) ),
inference(ennf_transformation,[],[f749]) ).
fof(f2002,plain,
! [X0,X1] :
( empty(X1)
| in(X0,X1)
| ~ element(X0,X1) ),
inference(ennf_transformation,[],[f795]) ).
fof(f2003,plain,
! [X0,X1] :
( empty(X1)
| in(X0,X1)
| ~ element(X0,X1) ),
inference(flattening,[],[f2002]) ).
fof(f2263,plain,
! [X0,X1] :
( ( X0 = X1
| ~ subset(X0,X1)
| ~ subset(X1,X0) )
& ( ( subset(X0,X1)
& subset(X1,X0) )
| X0 != X1 ) ),
inference(nnf_transformation,[],[f98]) ).
fof(f2264,plain,
! [X0,X1] :
( ( X0 = X1
| ~ subset(X0,X1)
| ~ subset(X1,X0) )
& ( ( subset(X0,X1)
& subset(X1,X0) )
| X0 != X1 ) ),
inference(flattening,[],[f2263]) ).
fof(f2440,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ? [X2] :
( ~ in(X2,X1)
& in(X2,X0) ) )
& ( ! [X2] :
( in(X2,X1)
| ~ in(X2,X0) )
| ~ subset(X0,X1) ) ),
inference(nnf_transformation,[],[f1243]) ).
fof(f2441,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ? [X2] :
( ~ in(X2,X1)
& in(X2,X0) ) )
& ( ! [X3] :
( in(X3,X1)
| ~ in(X3,X0) )
| ~ subset(X0,X1) ) ),
inference(rectify,[],[f2440]) ).
fof(f2442,plain,
! [X0,X1] :
( ( subset(X0,X1)
| ( ~ in(sK137(X0,X1),X1)
& in(sK137(X0,X1),X0) ) )
& ( ! [X3] :
( in(X3,X1)
| ~ in(X3,X0) )
| ~ subset(X0,X1) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK137]),skolemize(X2,sK137(X0,X1))],[f2441]) ).
fof(f2951,plain,
? [X0,X1] :
( ? [X3,X4,X5] :
( X4 != X5
& ! [X6] :
( ( in(X6,X4)
| ~ in(X6,the_carrier(X1))
| ! [X7] :
( ~ netstr_induced_subset(X7,X0,X1)
| ! [X8] :
( ~ element(X8,the_carrier(X1))
| topstr_closure(X0,X7) != X3
| X6 != X8
| relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X8)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X8))) != X7 ) ) )
& ( ( in(X6,the_carrier(X1))
& ? [X7] :
( netstr_induced_subset(X7,X0,X1)
& ? [X8] :
( element(X8,the_carrier(X1))
& X3 = topstr_closure(X0,X7)
& X6 = X8
& X7 = relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X8)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X8))) ) ) )
| ~ in(X6,X4) ) )
& ! [X9] :
( ( in(X9,X5)
| ~ in(X9,the_carrier(X1))
| ! [X10] :
( ~ netstr_induced_subset(X10,X0,X1)
| ! [X11] :
( ~ element(X11,the_carrier(X1))
| topstr_closure(X0,X10) != X3
| X9 != X11
| relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X11)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X11))) != X10 ) ) )
& ( ( in(X9,the_carrier(X1))
& ? [X10] :
( netstr_induced_subset(X10,X0,X1)
& ? [X11] :
( element(X11,the_carrier(X1))
& topstr_closure(X0,X10) = X3
& X9 = X11
& relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X11)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X11))) = X10 ) ) )
| ~ in(X9,X5) ) ) )
& ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0)
& ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) ),
inference(nnf_transformation,[],[f1837]) ).
fof(f2952,plain,
? [X0,X1] :
( ? [X3,X4,X5] :
( X4 != X5
& ! [X6] :
( ( in(X6,X4)
| ~ in(X6,the_carrier(X1))
| ! [X7] :
( ~ netstr_induced_subset(X7,X0,X1)
| ! [X8] :
( ~ element(X8,the_carrier(X1))
| topstr_closure(X0,X7) != X3
| X6 != X8
| relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X8)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X8))) != X7 ) ) )
& ( ( in(X6,the_carrier(X1))
& ? [X7] :
( netstr_induced_subset(X7,X0,X1)
& ? [X8] :
( element(X8,the_carrier(X1))
& X3 = topstr_closure(X0,X7)
& X6 = X8
& X7 = relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X8)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X8))) ) ) )
| ~ in(X6,X4) ) )
& ! [X9] :
( ( in(X9,X5)
| ~ in(X9,the_carrier(X1))
| ! [X10] :
( ~ netstr_induced_subset(X10,X0,X1)
| ! [X11] :
( ~ element(X11,the_carrier(X1))
| topstr_closure(X0,X10) != X3
| X9 != X11
| relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X11)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X11))) != X10 ) ) )
& ( ( in(X9,the_carrier(X1))
& ? [X10] :
( netstr_induced_subset(X10,X0,X1)
& ? [X11] :
( element(X11,the_carrier(X1))
& topstr_closure(X0,X10) = X3
& X9 = X11
& relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X11)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X11))) = X10 ) ) )
| ~ in(X9,X5) ) ) )
& ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0)
& ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) ),
inference(flattening,[],[f2951]) ).
fof(f2953,plain,
? [X0,X1] :
( ? [X2,X3,X4] :
( X3 != X4
& ! [X5] :
( ( in(X5,X3)
| ~ in(X5,the_carrier(X1))
| ! [X6] :
( ~ netstr_induced_subset(X6,X0,X1)
| ! [X7] :
( ~ element(X7,the_carrier(X1))
| topstr_closure(X0,X6) != X2
| X5 != X7
| relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X7)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X7))) != X6 ) ) )
& ( ( in(X5,the_carrier(X1))
& ? [X8] :
( netstr_induced_subset(X8,X0,X1)
& ? [X9] :
( element(X9,the_carrier(X1))
& topstr_closure(X0,X8) = X2
& X5 = X9
& relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X9)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X9))) = X8 ) ) )
| ~ in(X5,X3) ) )
& ! [X10] :
( ( in(X10,X4)
| ~ in(X10,the_carrier(X1))
| ! [X11] :
( ~ netstr_induced_subset(X11,X0,X1)
| ! [X12] :
( ~ element(X12,the_carrier(X1))
| topstr_closure(X0,X11) != X2
| X10 != X12
| relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X12)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X12))) != X11 ) ) )
& ( ( in(X10,the_carrier(X1))
& ? [X13] :
( netstr_induced_subset(X13,X0,X1)
& ? [X14] :
( element(X14,the_carrier(X1))
& topstr_closure(X0,X13) = X2
& X10 = X14
& relation_rng_as_subset(the_carrier(subnetstr_of_element(X0,X1,X14)),the_carrier(X0),the_mapping(X0,subnetstr_of_element(X0,X1,X14))) = X13 ) ) )
| ~ in(X10,X4) ) ) )
& ~ empty_carrier(X0)
& topological_space(X0)
& top_str(X0)
& ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) ),
inference(rectify,[],[f2952]) ).
fof(f2954,plain,
( sK619 != sK620
& ! [X5] :
( ( in(X5,sK619)
| ~ in(X5,the_carrier(sK617))
| ! [X6] :
( ~ netstr_induced_subset(X6,sK616,sK617)
| ! [X7] :
( ~ element(X7,the_carrier(sK617))
| sK618 != topstr_closure(sK616,X6)
| X5 != X7
| relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,X7)),the_carrier(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,X7))) != X6 ) ) )
& ( ( in(X5,the_carrier(sK617))
& netstr_induced_subset(sK621(X5),sK616,sK617)
& element(sK622(X5),the_carrier(sK617))
& sK618 = topstr_closure(sK616,sK621(X5))
& sK622(X5) = X5
& sK621(X5) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,sK622(X5))),the_carrier(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,sK622(X5)))) )
| ~ in(X5,sK619) ) )
& ! [X10] :
( ( in(X10,sK620)
| ~ in(X10,the_carrier(sK617))
| ! [X11] :
( ~ netstr_induced_subset(X11,sK616,sK617)
| ! [X12] :
( ~ element(X12,the_carrier(sK617))
| sK618 != topstr_closure(sK616,X11)
| X10 != X12
| relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,X12)),the_carrier(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,X12))) != X11 ) ) )
& ( ( in(X10,the_carrier(sK617))
& netstr_induced_subset(sK623(X10),sK616,sK617)
& element(sK624(X10),the_carrier(sK617))
& sK618 = topstr_closure(sK616,sK623(X10))
& sK624(X10) = X10
& sK623(X10) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,sK624(X10))),the_carrier(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,sK624(X10)))) )
| ~ in(X10,sK620) ) )
& ~ empty_carrier(sK616)
& topological_space(sK616)
& top_str(sK616)
& ~ empty_carrier(sK617)
& transitive_relstr(sK617)
& directed_relstr(sK617)
& net_str(sK617,sK616) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK616,sK617,sK618,sK619,sK620,sK621,sK622,sK623,sK624]),skolemize(X0,sK616),skolemize(X1,sK617),skolemize(X2,sK618),skolemize(X3,sK619),skolemize(X4,sK620),skolemize(X8,sK621(X5)),skolemize(X9,sK622(X5)),skolemize(X13,sK623(X10)),skolemize(X14,sK624(X10))],[f2953]) ).
fof(f3419,plain,
! [X0,X1] :
( ~ subset(X1,X0)
| ~ subset(X0,X1)
| X0 = X1 ),
inference(cnf_transformation,[],[f2264]) ).
fof(f3749,plain,
! [X0,X1] :
( in(sK137(X0,X1),X0)
| subset(X0,X1) ),
inference(cnf_transformation,[],[f2442]) ).
fof(f3750,plain,
! [X0,X1] :
( ~ in(sK137(X0,X1),X1)
| subset(X0,X1) ),
inference(cnf_transformation,[],[f2442]) ).
fof(f4107,plain,
! [X0] :
( ~ rel_str(X0)
| one_sorted_str(X0) ),
inference(cnf_transformation,[],[f1414]) ).
fof(f4108,plain,
! [X0] :
( ~ top_str(X0)
| one_sorted_str(X0) ),
inference(cnf_transformation,[],[f1415]) ).
fof(f4109,plain,
! [X0,X1] :
( ~ one_sorted_str(X0)
| ~ net_str(X1,X0)
| rel_str(X1) ),
inference(cnf_transformation,[],[f1416]) ).
fof(f4224,plain,
! [X0] :
( ~ empty(the_carrier(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f1479]) ).
fof(f5792,plain,
net_str(sK617,sK616),
inference(cnf_transformation,[],[f2954]) ).
fof(f5795,plain,
~ empty_carrier(sK617),
inference(cnf_transformation,[],[f2954]) ).
fof(f5796,plain,
top_str(sK616),
inference(cnf_transformation,[],[f2954]) ).
fof(f5799,plain,
! [X10] :
( ~ in(X10,sK620)
| sK623(X10) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,sK624(X10))),the_carrier(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,sK624(X10)))) ),
inference(cnf_transformation,[],[f2954]) ).
fof(f5800,plain,
! [X10] :
( ~ in(X10,sK620)
| sK624(X10) = X10 ),
inference(cnf_transformation,[],[f2954]) ).
fof(f5801,plain,
! [X10] :
( ~ in(X10,sK620)
| sK618 = topstr_closure(sK616,sK623(X10)) ),
inference(cnf_transformation,[],[f2954]) ).
fof(f5802,plain,
! [X10] :
( element(sK624(X10),the_carrier(sK617))
| ~ in(X10,sK620) ),
inference(cnf_transformation,[],[f2954]) ).
fof(f5803,plain,
! [X10] :
( netstr_induced_subset(sK623(X10),sK616,sK617)
| ~ in(X10,sK620) ),
inference(cnf_transformation,[],[f2954]) ).
fof(f5805,plain,
! [X10,X11,X12] :
( in(X10,sK620)
| ~ in(X10,the_carrier(sK617))
| ~ netstr_induced_subset(X11,sK616,sK617)
| ~ element(X12,the_carrier(sK617))
| sK618 != topstr_closure(sK616,X11)
| X10 != X12
| relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,X12)),the_carrier(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,X12))) != X11 ),
inference(cnf_transformation,[],[f2954]) ).
fof(f5806,plain,
! [X5] :
( ~ in(X5,sK619)
| sK621(X5) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,sK622(X5))),the_carrier(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,sK622(X5)))) ),
inference(cnf_transformation,[],[f2954]) ).
fof(f5807,plain,
! [X5] :
( ~ in(X5,sK619)
| sK622(X5) = X5 ),
inference(cnf_transformation,[],[f2954]) ).
fof(f5808,plain,
! [X5] :
( ~ in(X5,sK619)
| sK618 = topstr_closure(sK616,sK621(X5)) ),
inference(cnf_transformation,[],[f2954]) ).
fof(f5809,plain,
! [X5] :
( element(sK622(X5),the_carrier(sK617))
| ~ in(X5,sK619) ),
inference(cnf_transformation,[],[f2954]) ).
fof(f5810,plain,
! [X5] :
( netstr_induced_subset(sK621(X5),sK616,sK617)
| ~ in(X5,sK619) ),
inference(cnf_transformation,[],[f2954]) ).
fof(f5812,plain,
! [X6,X7,X5] :
( in(X5,sK619)
| ~ in(X5,the_carrier(sK617))
| ~ netstr_induced_subset(X6,sK616,sK617)
| ~ element(X7,the_carrier(sK617))
| sK618 != topstr_closure(sK616,X6)
| X5 != X7
| relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,X7)),the_carrier(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,X7))) != X6 ),
inference(cnf_transformation,[],[f2954]) ).
fof(f5813,plain,
sK619 != sK620,
inference(cnf_transformation,[],[f2954]) ).
fof(f5855,plain,
! [X0] :
( ~ one_sorted_str(X0)
| the_carrier(X0) = cast_as_carrier_subset(X0) ),
inference(cnf_transformation,[],[f1861]) ).
fof(f5937,plain,
! [X0,X1] :
( element(X0,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[],[f1929]) ).
fof(f6021,plain,
! [X0,X1] :
( ~ element(X0,X1)
| in(X0,X1)
| empty(X1) ),
inference(cnf_transformation,[],[f2003]) ).
fof(f7691,plain,
! [X6,X7] :
( in(X7,sK619)
| ~ in(X7,the_carrier(sK617))
| ~ netstr_induced_subset(X6,sK616,sK617)
| ~ element(X7,the_carrier(sK617))
| sK618 != topstr_closure(sK616,X6)
| relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,X7)),the_carrier(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,X7))) != X6 ),
inference(equality_resolution,[],[f5812]) ).
fof(f7692,plain,
! [X7] :
( in(X7,sK619)
| ~ in(X7,the_carrier(sK617))
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,X7)),the_carrier(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,X7))),sK616,sK617)
| ~ element(X7,the_carrier(sK617))
| sK618 != topstr_closure(sK616,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,X7)),the_carrier(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,X7)))) ),
inference(equality_resolution,[],[f7691]) ).
fof(f7693,plain,
! [X11,X12] :
( in(X12,sK620)
| ~ in(X12,the_carrier(sK617))
| ~ netstr_induced_subset(X11,sK616,sK617)
| ~ element(X12,the_carrier(sK617))
| sK618 != topstr_closure(sK616,X11)
| relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,X12)),the_carrier(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,X12))) != X11 ),
inference(equality_resolution,[],[f5805]) ).
fof(f7694,plain,
! [X12] :
( in(X12,sK620)
| ~ in(X12,the_carrier(sK617))
| ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,X12)),the_carrier(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,X12))),sK616,sK617)
| ~ element(X12,the_carrier(sK617))
| sK618 != topstr_closure(sK616,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,X12)),the_carrier(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,X12)))) ),
inference(equality_resolution,[],[f7693]) ).
fof(f7796,plain,
! [X12] :
( ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,X12)),the_carrier(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,X12))),sK616,sK617)
| ~ in(X12,the_carrier(sK617))
| in(X12,sK620)
| sK618 != topstr_closure(sK616,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,X12)),the_carrier(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,X12)))) ),
inference(forward_subsumption_resolution,[],[f7694,f5937]) ).
fof(f7797,plain,
! [X7] :
( ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,X7)),the_carrier(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,X7))),sK616,sK617)
| ~ in(X7,the_carrier(sK617))
| in(X7,sK619)
| sK618 != topstr_closure(sK616,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,X7)),the_carrier(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,X7)))) ),
inference(forward_subsumption_resolution,[],[f7692,f5937]) ).
fof(f8347,plain,
one_sorted_str(sK616),
inference(resolution,[],[f4108,f5796]) ).
fof(f8349,plain,
the_carrier(sK616) = cast_as_carrier_subset(sK616),
inference(resolution,[],[f8347,f5855]) ).
fof(f8355,plain,
! [X0] :
( ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,X0)),cast_as_carrier_subset(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,X0))),sK616,sK617)
| ~ in(X0,the_carrier(sK617))
| in(X0,sK620)
| sK618 != topstr_closure(sK616,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,X0)),cast_as_carrier_subset(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,X0)))) ),
inference(superposition,[],[f7796,f8349]) ).
fof(f8356,plain,
! [X0] :
( ~ netstr_induced_subset(relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,X0)),cast_as_carrier_subset(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,X0))),sK616,sK617)
| ~ in(X0,the_carrier(sK617))
| in(X0,sK619)
| sK618 != topstr_closure(sK616,relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,X0)),cast_as_carrier_subset(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,X0)))) ),
inference(superposition,[],[f7797,f8349]) ).
fof(f8451,plain,
! [X0] :
( in(sK622(X0),the_carrier(sK617))
| empty(the_carrier(sK617))
| ~ in(X0,sK619) ),
inference(resolution,[],[f6021,f5809]) ).
fof(f8452,plain,
! [X0] :
( in(sK624(X0),the_carrier(sK617))
| empty(the_carrier(sK617))
| ~ in(X0,sK620) ),
inference(resolution,[],[f6021,f5802]) ).
fof(f8464,definition,
( spl673_78
<=> empty(the_carrier(sK617)) ),
introduced(definition,[new_symbols(definition,[spl673_78])],[avatar_definition]) ).
fof(f8465,plain,
( empty(the_carrier(sK617))
| ~ spl673_78 ),
inference(avatar_component_clause,[],[f8464]) ).
fof(f8471,definition,
( spl673_80
<=> ! [X0] :
( in(sK624(X0),the_carrier(sK617))
| ~ in(X0,sK620) ) ),
introduced(definition,[new_symbols(definition,[spl673_80])],[avatar_definition]) ).
fof(f8472,plain,
( ! [X0] :
( ~ in(X0,sK620)
| in(sK624(X0),the_carrier(sK617)) )
| ~ spl673_80 ),
inference(avatar_component_clause,[],[f8471]) ).
fof(f8473,plain,
( spl673_78
| spl673_80 ),
inference(avatar_split_clause,[],[f8452,f8471,f8464]) ).
fof(f8475,definition,
( spl673_81
<=> ! [X0] :
( in(sK622(X0),the_carrier(sK617))
| ~ in(X0,sK619) ) ),
introduced(definition,[new_symbols(definition,[spl673_81])],[avatar_definition]) ).
fof(f8476,plain,
( ! [X0] :
( ~ in(X0,sK619)
| in(sK622(X0),the_carrier(sK617)) )
| ~ spl673_81 ),
inference(avatar_component_clause,[],[f8475]) ).
fof(f8477,plain,
( spl673_78
| spl673_81 ),
inference(avatar_split_clause,[],[f8451,f8475,f8464]) ).
fof(f8478,plain,
( empty_carrier(sK617)
| ~ one_sorted_str(sK617)
| ~ spl673_78 ),
inference(resolution,[],[f8465,f4224]) ).
fof(f8479,plain,
( ~ one_sorted_str(sK617)
| ~ spl673_78 ),
inference(forward_subsumption_resolution,[],[f8478,f5795]) ).
fof(f8719,plain,
! [X0] :
( ~ net_str(X0,sK616)
| rel_str(X0) ),
inference(resolution,[],[f4109,f8347]) ).
fof(f8720,plain,
rel_str(sK617),
inference(resolution,[],[f8719,f5792]) ).
fof(f9096,plain,
one_sorted_str(sK617),
inference(resolution,[],[f4107,f8720]) ).
fof(f9098,plain,
( $false
| ~ spl673_78 ),
inference(forward_subsumption_resolution,[],[f9096,f8479]) ).
fof(f9099,plain,
~ spl673_78,
inference(avatar_contradiction_clause,[],[f9098]) ).
fof(f9124,plain,
the_carrier(sK617) = cast_as_carrier_subset(sK617),
inference(resolution,[],[f9096,f5855]) ).
fof(f18945,plain,
! [X0] :
( subset(sK619,X0)
| sK621(sK137(sK619,X0)) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,sK622(sK137(sK619,X0)))),the_carrier(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,sK622(sK137(sK619,X0))))) ),
inference(resolution,[],[f3749,f5806]) ).
fof(f18946,plain,
! [X0] :
( subset(sK619,X0)
| sK137(sK619,X0) = sK622(sK137(sK619,X0)) ),
inference(resolution,[],[f3749,f5807]) ).
fof(f18947,plain,
! [X0] :
( subset(sK619,X0)
| sK618 = topstr_closure(sK616,sK621(sK137(sK619,X0))) ),
inference(resolution,[],[f3749,f5808]) ).
fof(f19019,plain,
! [X0] :
( subset(sK619,X0)
| sK621(sK137(sK619,X0)) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,sK622(sK137(sK619,X0)))),cast_as_carrier_subset(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,sK622(sK137(sK619,X0))))) ),
inference(forward_demodulation,[],[f18945,f8349]) ).
fof(f19060,plain,
! [X0] :
( ~ subset(X0,sK619)
| sK137(sK619,X0) = sK622(sK137(sK619,X0))
| sK619 = X0 ),
inference(resolution,[],[f18946,f3419]) ).
fof(f19105,definition,
( spl673_775
<=> sK137(sK620,sK619) = sK624(sK137(sK620,sK619)) ),
introduced(definition,[new_symbols(definition,[spl673_775])],[avatar_definition]) ).
fof(f19106,plain,
( sK137(sK620,sK619) = sK624(sK137(sK620,sK619))
| ~ spl673_775 ),
inference(avatar_component_clause,[],[f19105]) ).
fof(f19108,definition,
( spl673_776
<=> sK137(sK619,sK620) = sK622(sK137(sK619,sK620)) ),
introduced(definition,[new_symbols(definition,[spl673_776])],[avatar_definition]) ).
fof(f19109,plain,
( sK137(sK619,sK620) = sK622(sK137(sK619,sK620))
| ~ spl673_776 ),
inference(avatar_component_clause,[],[f19108]) ).
fof(f19112,definition,
( spl673_777
<=> sK618 = topstr_closure(sK616,sK623(sK137(sK620,sK619))) ),
introduced(definition,[new_symbols(definition,[spl673_777])],[avatar_definition]) ).
fof(f19113,plain,
( sK618 = topstr_closure(sK616,sK623(sK137(sK620,sK619)))
| ~ spl673_777 ),
inference(avatar_component_clause,[],[f19112]) ).
fof(f19116,definition,
( spl673_778
<=> sK623(sK137(sK620,sK619)) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,sK624(sK137(sK620,sK619)))),cast_as_carrier_subset(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,sK624(sK137(sK620,sK619))))) ),
introduced(definition,[new_symbols(definition,[spl673_778])],[avatar_definition]) ).
fof(f19117,plain,
( sK623(sK137(sK620,sK619)) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,sK624(sK137(sK620,sK619)))),cast_as_carrier_subset(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,sK624(sK137(sK620,sK619)))))
| ~ spl673_778 ),
inference(avatar_component_clause,[],[f19116]) ).
fof(f19126,definition,
( spl673_779
<=> in(sK137(sK619,sK620),sK619) ),
introduced(definition,[new_symbols(definition,[spl673_779])],[avatar_definition]) ).
fof(f19127,plain,
( ~ in(sK137(sK619,sK620),sK619)
| spl673_779 ),
inference(avatar_component_clause,[],[f19126]) ).
fof(f19136,definition,
( spl673_782
<=> sK621(sK137(sK619,sK620)) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,sK137(sK619,sK620))),cast_as_carrier_subset(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,sK137(sK619,sK620)))) ),
introduced(definition,[new_symbols(definition,[spl673_782])],[avatar_definition]) ).
fof(f19137,plain,
( sK621(sK137(sK619,sK620)) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,sK137(sK619,sK620))),cast_as_carrier_subset(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,sK137(sK619,sK620))))
| ~ spl673_782 ),
inference(avatar_component_clause,[],[f19136]) ).
fof(f19140,plain,
( subset(sK619,sK620)
| spl673_779 ),
inference(resolution,[],[f19127,f3749]) ).
fof(f19144,plain,
( ~ subset(sK620,sK619)
| sK619 = sK620
| spl673_779 ),
inference(resolution,[],[f19140,f3419]) ).
fof(f19145,plain,
( ~ subset(sK620,sK619)
| spl673_779 ),
inference(forward_subsumption_resolution,[],[f19144,f5813]) ).
fof(f19165,definition,
( spl673_783
<=> in(sK137(sK619,sK620),cast_as_carrier_subset(sK617)) ),
introduced(definition,[new_symbols(definition,[spl673_783])],[avatar_definition]) ).
fof(f19166,plain,
( in(sK137(sK619,sK620),cast_as_carrier_subset(sK617))
| ~ spl673_783 ),
inference(avatar_component_clause,[],[f19165]) ).
fof(f19541,plain,
( sK623(sK137(sK620,sK619)) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,sK137(sK620,sK619))),cast_as_carrier_subset(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,sK137(sK620,sK619))))
| ~ spl673_775
| ~ spl673_778 ),
inference(forward_demodulation,[],[f19117,f19106]) ).
fof(f19549,definition,
( spl673_844
<=> in(sK137(sK620,sK619),sK620) ),
introduced(definition,[new_symbols(definition,[spl673_844])],[avatar_definition]) ).
fof(f19550,plain,
( ~ in(sK137(sK620,sK619),sK620)
| spl673_844 ),
inference(avatar_component_clause,[],[f19549]) ).
fof(f19559,definition,
( spl673_847
<=> in(sK137(sK620,sK619),sK619) ),
introduced(definition,[new_symbols(definition,[spl673_847])],[avatar_definition]) ).
fof(f19560,plain,
( in(sK137(sK620,sK619),sK619)
| ~ spl673_847 ),
inference(avatar_component_clause,[],[f19559]) ).
fof(f19563,plain,
( subset(sK620,sK619)
| spl673_844 ),
inference(resolution,[],[f19550,f3749]) ).
fof(f19568,plain,
( sK137(sK619,sK620) = sK622(sK137(sK619,sK620))
| sK619 = sK620
| spl673_844 ),
inference(resolution,[],[f19563,f19060]) ).
fof(f19571,plain,
( ~ subset(sK619,sK620)
| sK619 = sK620
| spl673_844 ),
inference(resolution,[],[f19563,f3419]) ).
fof(f19572,plain,
( ~ subset(sK619,sK620)
| spl673_844 ),
inference(forward_subsumption_resolution,[],[f19571,f5813]) ).
fof(f19573,plain,
( sK137(sK619,sK620) = sK622(sK137(sK619,sK620))
| spl673_844 ),
inference(forward_subsumption_resolution,[],[f19568,f5813]) ).
fof(f19574,plain,
( spl673_776
| spl673_844 ),
inference(avatar_split_clause,[],[f19573,f19549,f19108]) ).
fof(f19588,definition,
( spl673_848
<=> in(sK137(sK620,sK619),cast_as_carrier_subset(sK617)) ),
introduced(definition,[new_symbols(definition,[spl673_848])],[avatar_definition]) ).
fof(f19589,plain,
( in(sK137(sK620,sK619),cast_as_carrier_subset(sK617))
| ~ spl673_848 ),
inference(avatar_component_clause,[],[f19588]) ).
fof(f20697,plain,
( ~ netstr_induced_subset(sK623(sK137(sK620,sK619)),sK616,sK617)
| ~ in(sK137(sK620,sK619),the_carrier(sK617))
| in(sK137(sK620,sK619),sK619)
| sK618 != topstr_closure(sK616,sK623(sK137(sK620,sK619)))
| ~ spl673_775
| ~ spl673_778 ),
inference(superposition,[],[f8356,f19541]) ).
fof(f20718,plain,
( ~ netstr_induced_subset(sK623(sK137(sK620,sK619)),sK616,sK617)
| ~ in(sK137(sK620,sK619),the_carrier(sK617))
| in(sK137(sK620,sK619),sK619)
| ~ spl673_775
| ~ spl673_777
| ~ spl673_778 ),
inference(forward_subsumption_resolution,[],[f20697,f19113]) ).
fof(f20730,plain,
( ~ in(sK137(sK620,sK619),cast_as_carrier_subset(sK617))
| ~ netstr_induced_subset(sK623(sK137(sK620,sK619)),sK616,sK617)
| in(sK137(sK620,sK619),sK619)
| ~ spl673_775
| ~ spl673_777
| ~ spl673_778 ),
inference(forward_demodulation,[],[f20718,f9124]) ).
fof(f20742,plain,
( ~ netstr_induced_subset(sK623(sK137(sK620,sK619)),sK616,sK617)
| in(sK137(sK620,sK619),sK619)
| ~ spl673_775
| ~ spl673_777
| ~ spl673_778
| ~ spl673_848 ),
inference(forward_subsumption_resolution,[],[f20730,f19589]) ).
fof(f20747,definition,
( spl673_936
<=> netstr_induced_subset(sK623(sK137(sK620,sK619)),sK616,sK617) ),
introduced(definition,[new_symbols(definition,[spl673_936])],[avatar_definition]) ).
fof(f20748,plain,
( ~ netstr_induced_subset(sK623(sK137(sK620,sK619)),sK616,sK617)
| spl673_936 ),
inference(avatar_component_clause,[],[f20747]) ).
fof(f20767,plain,
( in(sK137(sK620,sK619),sK620)
| ~ spl673_844 ),
inference(avatar_component_clause,[],[f19549]) ).
fof(f20809,plain,
( in(sK624(sK137(sK620,sK619)),the_carrier(sK617))
| ~ spl673_80
| ~ spl673_844 ),
inference(resolution,[],[f20767,f8472]) ).
fof(f20853,plain,
( in(sK624(sK137(sK620,sK619)),cast_as_carrier_subset(sK617))
| ~ spl673_80
| ~ spl673_844 ),
inference(forward_demodulation,[],[f20809,f9124]) ).
fof(f20862,plain,
( in(sK137(sK620,sK619),cast_as_carrier_subset(sK617))
| ~ spl673_80
| ~ spl673_775
| ~ spl673_844 ),
inference(forward_demodulation,[],[f20853,f19106]) ).
fof(f20887,plain,
( ~ in(sK137(sK620,sK619),sK620)
| spl673_936 ),
inference(resolution,[],[f20748,f5803]) ).
fof(f20889,plain,
( $false
| ~ spl673_844
| spl673_936 ),
inference(forward_subsumption_resolution,[],[f20887,f20767]) ).
fof(f20890,plain,
( ~ spl673_844
| spl673_936 ),
inference(avatar_contradiction_clause,[],[f20889]) ).
fof(f20891,plain,
( subset(sK620,sK619)
| ~ spl673_847 ),
inference(resolution,[],[f19560,f3750]) ).
fof(f20944,plain,
( sK137(sK619,sK620) = sK622(sK137(sK619,sK620))
| sK619 = sK620
| ~ spl673_847 ),
inference(resolution,[],[f20891,f19060]) ).
fof(f20947,plain,
( ~ subset(sK619,sK620)
| sK619 = sK620
| ~ spl673_847 ),
inference(resolution,[],[f20891,f3419]) ).
fof(f20948,plain,
( ~ subset(sK619,sK620)
| ~ spl673_847 ),
inference(forward_subsumption_resolution,[],[f20947,f5813]) ).
fof(f20949,plain,
( sK137(sK619,sK620) = sK622(sK137(sK619,sK620))
| ~ spl673_847 ),
inference(forward_subsumption_resolution,[],[f20944,f5813]) ).
fof(f20950,plain,
( spl673_776
| ~ spl673_847 ),
inference(avatar_split_clause,[],[f20949,f19559,f19108]) ).
fof(f20957,plain,
( spl673_848
| ~ spl673_80
| ~ spl673_775
| ~ spl673_844 ),
inference(avatar_split_clause,[],[f20862,f19549,f19105,f8471,f19588]) ).
fof(f21420,plain,
( sK621(sK137(sK619,sK620)) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,sK622(sK137(sK619,sK620)))),cast_as_carrier_subset(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,sK622(sK137(sK619,sK620)))))
| spl673_844 ),
inference(resolution,[],[f19572,f19019]) ).
fof(f21421,plain,
( sK618 = topstr_closure(sK616,sK621(sK137(sK619,sK620)))
| spl673_844 ),
inference(resolution,[],[f19572,f18947]) ).
fof(f21423,plain,
( sK621(sK137(sK619,sK620)) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,sK137(sK619,sK620))),cast_as_carrier_subset(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,sK137(sK619,sK620))))
| ~ spl673_776
| spl673_844 ),
inference(forward_demodulation,[],[f21420,f19109]) ).
fof(f21424,plain,
( spl673_782
| ~ spl673_776
| spl673_844 ),
inference(avatar_split_clause,[],[f21423,f19549,f19108,f19136]) ).
fof(f22270,plain,
( ~ netstr_induced_subset(sK621(sK137(sK619,sK620)),sK616,sK617)
| ~ in(sK137(sK619,sK620),the_carrier(sK617))
| in(sK137(sK619,sK620),sK620)
| sK618 != topstr_closure(sK616,sK621(sK137(sK619,sK620)))
| ~ spl673_782 ),
inference(superposition,[],[f8355,f19137]) ).
fof(f22293,plain,
( ~ netstr_induced_subset(sK621(sK137(sK619,sK620)),sK616,sK617)
| ~ in(sK137(sK619,sK620),the_carrier(sK617))
| in(sK137(sK619,sK620),sK620)
| ~ spl673_782
| spl673_844 ),
inference(forward_subsumption_resolution,[],[f22270,f21421]) ).
fof(f22300,plain,
( ~ in(sK137(sK619,sK620),cast_as_carrier_subset(sK617))
| ~ netstr_induced_subset(sK621(sK137(sK619,sK620)),sK616,sK617)
| in(sK137(sK619,sK620),sK620)
| ~ spl673_782
| spl673_844 ),
inference(forward_demodulation,[],[f22293,f9124]) ).
fof(f22311,definition,
( spl673_1000
<=> netstr_induced_subset(sK621(sK137(sK619,sK620)),sK616,sK617) ),
introduced(definition,[new_symbols(definition,[spl673_1000])],[avatar_definition]) ).
fof(f22312,plain,
( ~ netstr_induced_subset(sK621(sK137(sK619,sK620)),sK616,sK617)
| spl673_1000 ),
inference(avatar_component_clause,[],[f22311]) ).
fof(f22317,plain,
( in(sK137(sK619,sK620),sK619)
| ~ spl673_779 ),
inference(avatar_component_clause,[],[f19126]) ).
fof(f22320,definition,
( spl673_1002
<=> in(sK137(sK619,sK620),sK620) ),
introduced(definition,[new_symbols(definition,[spl673_1002])],[avatar_definition]) ).
fof(f22321,plain,
( in(sK137(sK619,sK620),sK620)
| ~ spl673_1002 ),
inference(avatar_component_clause,[],[f22320]) ).
fof(f22339,plain,
( in(sK622(sK137(sK619,sK620)),the_carrier(sK617))
| ~ spl673_81
| ~ spl673_779 ),
inference(resolution,[],[f22317,f8476]) ).
fof(f22386,plain,
( in(sK622(sK137(sK619,sK620)),cast_as_carrier_subset(sK617))
| ~ spl673_81
| ~ spl673_779 ),
inference(forward_demodulation,[],[f22339,f9124]) ).
fof(f22393,plain,
( in(sK137(sK619,sK620),cast_as_carrier_subset(sK617))
| ~ spl673_81
| ~ spl673_776
| ~ spl673_779 ),
inference(forward_demodulation,[],[f22386,f19109]) ).
fof(f22399,plain,
( subset(sK619,sK620)
| ~ spl673_1002 ),
inference(resolution,[],[f22321,f3750]) ).
fof(f22446,plain,
( $false
| spl673_844
| ~ spl673_1002 ),
inference(forward_subsumption_resolution,[],[f22399,f19572]) ).
fof(f22447,plain,
( spl673_844
| ~ spl673_1002 ),
inference(avatar_contradiction_clause,[],[f22446]) ).
fof(f22456,plain,
( ~ in(sK137(sK619,sK620),sK619)
| spl673_1000 ),
inference(resolution,[],[f22312,f5810]) ).
fof(f22458,plain,
( $false
| ~ spl673_779
| spl673_1000 ),
inference(forward_subsumption_resolution,[],[f22456,f22317]) ).
fof(f22459,plain,
( ~ spl673_779
| spl673_1000 ),
inference(avatar_contradiction_clause,[],[f22458]) ).
fof(f22464,plain,
( spl673_1002
| ~ spl673_1000
| ~ spl673_783
| ~ spl673_782
| spl673_844 ),
inference(avatar_split_clause,[],[f22300,f19549,f19136,f19165,f22311,f22320]) ).
fof(f22467,plain,
( spl673_783
| ~ spl673_81
| ~ spl673_776
| ~ spl673_779 ),
inference(avatar_split_clause,[],[f22393,f19126,f19108,f8475,f19165]) ).
fof(f22476,plain,
( $false
| spl673_779
| spl673_844 ),
inference(forward_subsumption_resolution,[],[f19140,f19572]) ).
fof(f22477,plain,
( spl673_779
| spl673_844 ),
inference(avatar_contradiction_clause,[],[f22476]) ).
fof(f22493,plain,
( $false
| spl673_779
| ~ spl673_847 ),
inference(forward_subsumption_resolution,[],[f19145,f20891]) ).
fof(f22494,plain,
( spl673_779
| ~ spl673_847 ),
inference(avatar_contradiction_clause,[],[f22493]) ).
fof(f22511,plain,
( ~ in(sK137(sK619,sK620),cast_as_carrier_subset(sK617))
| ~ netstr_induced_subset(sK621(sK137(sK619,sK620)),sK616,sK617)
| in(sK137(sK619,sK620),sK620)
| sK618 != topstr_closure(sK616,sK621(sK137(sK619,sK620)))
| ~ spl673_782 ),
inference(forward_demodulation,[],[f22270,f9124]) ).
fof(f22522,plain,
( ~ netstr_induced_subset(sK621(sK137(sK619,sK620)),sK616,sK617)
| in(sK137(sK619,sK620),sK620)
| sK618 != topstr_closure(sK616,sK621(sK137(sK619,sK620)))
| ~ spl673_782
| ~ spl673_783 ),
inference(forward_subsumption_resolution,[],[f22511,f19166]) ).
fof(f22561,definition,
( spl673_1018
<=> sK618 = topstr_closure(sK616,sK621(sK137(sK619,sK620))) ),
introduced(definition,[new_symbols(definition,[spl673_1018])],[avatar_definition]) ).
fof(f22562,plain,
( sK618 != topstr_closure(sK616,sK621(sK137(sK619,sK620)))
| spl673_1018 ),
inference(avatar_component_clause,[],[f22561]) ).
fof(f22563,plain,
( ~ spl673_1018
| spl673_1002
| ~ spl673_1000
| ~ spl673_782
| ~ spl673_783 ),
inference(avatar_split_clause,[],[f22522,f19165,f19136,f22311,f22320,f22561]) ).
fof(f22568,plain,
( sK621(sK137(sK619,sK620)) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,sK622(sK137(sK619,sK620)))),the_carrier(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,sK622(sK137(sK619,sK620)))))
| ~ spl673_779 ),
inference(resolution,[],[f22317,f5806]) ).
fof(f22570,plain,
( sK618 = topstr_closure(sK616,sK621(sK137(sK619,sK620)))
| ~ spl673_779 ),
inference(resolution,[],[f22317,f5808]) ).
fof(f22610,plain,
( $false
| ~ spl673_779
| spl673_1018 ),
inference(forward_subsumption_resolution,[],[f22570,f22562]) ).
fof(f22611,plain,
( ~ spl673_779
| spl673_1018 ),
inference(avatar_contradiction_clause,[],[f22610]) ).
fof(f22612,plain,
( sK621(sK137(sK619,sK620)) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,sK137(sK619,sK620))),the_carrier(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,sK137(sK619,sK620))))
| ~ spl673_776
| ~ spl673_779 ),
inference(forward_demodulation,[],[f22568,f19109]) ).
fof(f22618,plain,
( sK621(sK137(sK619,sK620)) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,sK137(sK619,sK620))),cast_as_carrier_subset(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,sK137(sK619,sK620))))
| ~ spl673_776
| ~ spl673_779 ),
inference(forward_demodulation,[],[f22612,f8349]) ).
fof(f22621,plain,
( spl673_782
| ~ spl673_776
| ~ spl673_779 ),
inference(avatar_split_clause,[],[f22618,f19126,f19108,f19136]) ).
fof(f22680,plain,
( sK623(sK137(sK620,sK619)) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,sK624(sK137(sK620,sK619)))),the_carrier(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,sK624(sK137(sK620,sK619)))))
| ~ spl673_844 ),
inference(resolution,[],[f20767,f5799]) ).
fof(f22681,plain,
( sK137(sK620,sK619) = sK624(sK137(sK620,sK619))
| ~ spl673_844 ),
inference(resolution,[],[f20767,f5800]) ).
fof(f22682,plain,
( sK618 = topstr_closure(sK616,sK623(sK137(sK620,sK619)))
| ~ spl673_844 ),
inference(resolution,[],[f20767,f5801]) ).
fof(f22725,plain,
( sK623(sK137(sK620,sK619)) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,sK137(sK620,sK619))),the_carrier(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,sK137(sK620,sK619))))
| ~ spl673_775
| ~ spl673_844 ),
inference(forward_demodulation,[],[f22680,f19106]) ).
fof(f22731,plain,
( sK623(sK137(sK620,sK619)) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,sK137(sK620,sK619))),cast_as_carrier_subset(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,sK137(sK620,sK619))))
| ~ spl673_775
| ~ spl673_844 ),
inference(forward_demodulation,[],[f22725,f8349]) ).
fof(f22747,plain,
( ~ netstr_induced_subset(sK623(sK137(sK620,sK619)),sK616,sK617)
| ~ in(sK137(sK620,sK619),the_carrier(sK617))
| in(sK137(sK620,sK619),sK619)
| sK618 != topstr_closure(sK616,sK623(sK137(sK620,sK619)))
| ~ spl673_775
| ~ spl673_844 ),
inference(superposition,[],[f8356,f22731]) ).
fof(f22768,plain,
( ~ netstr_induced_subset(sK623(sK137(sK620,sK619)),sK616,sK617)
| ~ in(sK137(sK620,sK619),the_carrier(sK617))
| in(sK137(sK620,sK619),sK619)
| ~ spl673_775
| ~ spl673_777
| ~ spl673_844 ),
inference(forward_subsumption_resolution,[],[f22747,f19113]) ).
fof(f22774,plain,
( ~ in(sK137(sK620,sK619),cast_as_carrier_subset(sK617))
| ~ netstr_induced_subset(sK623(sK137(sK620,sK619)),sK616,sK617)
| in(sK137(sK620,sK619),sK619)
| ~ spl673_775
| ~ spl673_777
| ~ spl673_844 ),
inference(forward_demodulation,[],[f22768,f9124]) ).
fof(f22780,plain,
( ~ netstr_induced_subset(sK623(sK137(sK620,sK619)),sK616,sK617)
| in(sK137(sK620,sK619),sK619)
| ~ spl673_775
| ~ spl673_777
| ~ spl673_844
| ~ spl673_848 ),
inference(forward_subsumption_resolution,[],[f22774,f19589]) ).
fof(f22784,plain,
( spl673_847
| ~ spl673_936
| ~ spl673_775
| ~ spl673_777
| ~ spl673_844
| ~ spl673_848 ),
inference(avatar_split_clause,[],[f22780,f19588,f19549,f19112,f19105,f20747,f19559]) ).
fof(f22791,plain,
( spl673_775
| ~ spl673_844 ),
inference(avatar_split_clause,[],[f22681,f19549,f19105]) ).
fof(f22792,plain,
( sK623(sK137(sK620,sK619)) = relation_rng_as_subset(the_carrier(subnetstr_of_element(sK616,sK617,sK624(sK137(sK620,sK619)))),cast_as_carrier_subset(sK616),the_mapping(sK616,subnetstr_of_element(sK616,sK617,sK624(sK137(sK620,sK619)))))
| ~ spl673_844 ),
inference(forward_demodulation,[],[f22680,f8349]) ).
fof(f22794,plain,
( spl673_778
| ~ spl673_844 ),
inference(avatar_split_clause,[],[f22792,f19549,f19116]) ).
fof(f22802,plain,
( spl673_847
| ~ spl673_936
| ~ spl673_775
| ~ spl673_777
| ~ spl673_778
| ~ spl673_848 ),
inference(avatar_split_clause,[],[f20742,f19588,f19116,f19112,f19105,f20747,f19559]) ).
fof(f22806,plain,
( $false
| ~ spl673_847
| ~ spl673_1002 ),
inference(forward_subsumption_resolution,[],[f20948,f22399]) ).
fof(f22807,plain,
( ~ spl673_847
| ~ spl673_1002 ),
inference(avatar_contradiction_clause,[],[f22806]) ).
fof(f22811,plain,
( spl673_777
| ~ spl673_844 ),
inference(avatar_split_clause,[],[f22682,f19549,f19112]) ).
cnf(s71,plain,
( spl673_78
| spl673_80 ),
inference(sat_conversion,[],[f8473]) ).
cnf(s72,plain,
( spl673_78
| spl673_81 ),
inference(sat_conversion,[],[f8477]) ).
cnf(s92,plain,
~ spl673_78,
inference(sat_conversion,[],[f9099]) ).
cnf(s893,plain,
( spl673_776
| spl673_844 ),
inference(sat_conversion,[],[f19574]) ).
cnf(s994,plain,
( ~ spl673_844
| spl673_936 ),
inference(sat_conversion,[],[f20890]) ).
cnf(s996,plain,
( spl673_776
| ~ spl673_847 ),
inference(sat_conversion,[],[f20950]) ).
cnf(s998,plain,
( ~ spl673_80
| ~ spl673_775
| ~ spl673_844
| spl673_848 ),
inference(sat_conversion,[],[f20957]) ).
cnf(s1024,plain,
( ~ spl673_776
| spl673_782
| spl673_844 ),
inference(sat_conversion,[],[f21424]) ).
cnf(s1064,plain,
( spl673_844
| ~ spl673_1002 ),
inference(sat_conversion,[],[f22447]) ).
cnf(s1066,plain,
( ~ spl673_779
| spl673_1000 ),
inference(sat_conversion,[],[f22459]) ).
cnf(s1068,plain,
( ~ spl673_782
| ~ spl673_783
| spl673_844
| ~ spl673_1000
| spl673_1002 ),
inference(sat_conversion,[],[f22464]) ).
cnf(s1070,plain,
( ~ spl673_81
| ~ spl673_776
| ~ spl673_779
| spl673_783 ),
inference(sat_conversion,[],[f22467]) ).
cnf(s1073,plain,
( spl673_779
| spl673_844 ),
inference(sat_conversion,[],[f22477]) ).
cnf(s1078,plain,
( spl673_779
| ~ spl673_847 ),
inference(sat_conversion,[],[f22494]) ).
cnf(s1093,plain,
( ~ spl673_782
| ~ spl673_783
| ~ spl673_1000
| spl673_1002
| ~ spl673_1018 ),
inference(sat_conversion,[],[f22563]) ).
cnf(s1095,plain,
( ~ spl673_779
| spl673_1018 ),
inference(sat_conversion,[],[f22611]) ).
cnf(s1096,plain,
( ~ spl673_776
| ~ spl673_779
| spl673_782 ),
inference(sat_conversion,[],[f22621]) ).
cnf(s1098,plain,
( ~ spl673_775
| ~ spl673_777
| ~ spl673_844
| spl673_847
| ~ spl673_848
| ~ spl673_936 ),
inference(sat_conversion,[],[f22784]) ).
cnf(s1099,plain,
( spl673_775
| ~ spl673_844 ),
inference(sat_conversion,[],[f22791]) ).
cnf(s1100,plain,
( spl673_778
| ~ spl673_844 ),
inference(sat_conversion,[],[f22794]) ).
cnf(s1105,plain,
( ~ spl673_775
| ~ spl673_777
| ~ spl673_778
| spl673_847
| ~ spl673_848
| ~ spl673_936 ),
inference(sat_conversion,[],[f22802]) ).
cnf(s1107,plain,
( ~ spl673_847
| ~ spl673_1002 ),
inference(sat_conversion,[],[f22807]) ).
cnf(s1108,plain,
( spl673_777
| ~ spl673_844 ),
inference(sat_conversion,[],[f22811]) ).
cnf(s1189,plain,
spl673_81,
inference(rat,[],[s72,s92]) ).
cnf(s1190,plain,
spl673_80,
inference(rat,[],[s71,s92]) ).
cnf(s1194,plain,
( ~ spl673_1002
| ~ spl673_775 ),
inference(rat,[],[s1098,s998,s994,s1108,s1064,s1107,s1190]) ).
cnf(s1197,plain,
( ~ spl673_779
| spl673_1002
| spl673_844 ),
inference(rat,[],[s1070,s1068,s1066,s1024,s893,s1189]) ).
cnf(s1198,plain,
spl673_844,
inference(rat,[],[s1197,s1064,s1073]) ).
cnf(s1199,plain,
spl673_777,
inference(rat,[],[s1108,s1198]) ).
cnf(s1200,plain,
spl673_778,
inference(rat,[],[s1100,s1198]) ).
cnf(s1201,plain,
spl673_775,
inference(rat,[],[s1099,s1198]) ).
cnf(s1202,plain,
spl673_936,
inference(rat,[],[s994,s1198]) ).
cnf(s1204,plain,
spl673_848,
inference(rat,[],[s998,s1201,s1190,s1198]) ).
cnf(s1206,plain,
~ spl673_1002,
inference(rat,[],[s1194,s1201]) ).
cnf(s1215,plain,
spl673_847,
inference(rat,[],[s1105,s1202,s1200,s1199,s1201,s1204]) ).
cnf(s1295,plain,
spl673_779,
inference(rat,[],[s1078,s1215]) ).
cnf(s1296,plain,
spl673_776,
inference(rat,[],[s996,s1215]) ).
cnf(s1297,plain,
spl673_1018,
inference(rat,[],[s1095,s1295]) ).
cnf(s1298,plain,
spl673_1000,
inference(rat,[],[s1066,s1295]) ).
cnf(s1300,plain,
spl673_783,
inference(rat,[],[s1070,s1296,s1189,s1295]) ).
cnf(s1301,plain,
spl673_782,
inference(rat,[],[s1096,s1295,s1296]) ).
cnf(s1303,plain,
$false,
inference(rat,[],[s1093,s1301,s1206,s1298,s1297,s1300]) ).
fof(f22817,plain,
$false,
inference(avatar_sat_refutation,[],[s1303]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU401+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.13/0.39 % Computer : n004.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Mon Sep 28 05:08:22 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.13/0.43 Running first-order theorem proving
% 0.13/0.43 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
% 13.32/2.86 % (4166050)Detected formulas, will run a generic FOF schedule.
% 13.32/2.86 % (4166056)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=3410158683:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 13.32/2.86 % (4166057)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=1775856754:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 13.32/2.86 % (4166058)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=255259668:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 13.32/2.86 % (4166060)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2395541085:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 13.32/2.86 % (4166059)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=252621154:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 13.32/2.86 % (4166061)dis-21_1_sil=8000:lcm=predicate:random_seed=2216962356: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)
% 13.32/2.86 % (4166055)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=1515142636:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 13.32/2.86 % (4166058)Instruction limit reached!
% 13.32/2.86 % (4166058)------------------------------
% 13.32/2.86 % (4166058)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.32/2.86 % (4166058)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.32/2.86 % (4166058)CaDiCaL version: 2.1.3
% 13.32/2.86 % (4166058)Termination reason: Instruction limit
% 13.32/2.86 % (4166058)Termination phase: Blocked clause elimination
% 13.32/2.86 % (4166058)Time elapsed: 0.059 s
% 13.32/2.86 % (4166058)Peak memory usage: 91 MB
% 13.32/2.86 % (4166058)Instructions burned: 110 (million)
% 13.32/2.86 % (4166061)Instruction limit reached!
% 13.32/2.86 % (4166061)------------------------------
% 13.32/2.86 % (4166061)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.32/2.86 % (4166061)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.32/2.86 % (4166061)CaDiCaL version: 2.1.3
% 13.32/2.86 % (4166061)Termination reason: Instruction limit
% 13.32/2.86 % (4166061)Termination phase: Property scanning
% 13.32/2.86 % (4166061)Time elapsed: 0.065 s
% 13.32/2.86 % (4166061)Peak memory usage: 91 MB
% 13.32/2.86 % (4166061)Instructions burned: 131 (million)
% 13.32/2.86 % (4166059)Instruction limit reached!
% 13.32/2.86 % (4166059)------------------------------
% 13.32/2.86 % (4166059)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.32/2.86 % (4166059)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.32/2.86 % (4166059)CaDiCaL version: 2.1.3
% 13.32/2.86 % (4166059)Termination reason: Instruction limit
% 13.32/2.86 % (4166059)Termination phase: Saturation
% 13.32/2.86 % (4166059)Time elapsed: 0.066 s
% 13.32/2.86 % (4166059)Peak memory usage: 92 MB
% 13.32/2.86 % (4166059)Instructions burned: 119 (million)
% 13.32/2.86 % (4166060)Instruction limit reached!
% 13.32/2.86 % (4166060)------------------------------
% 13.32/2.86 % (4166060)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.32/2.86 % (4166060)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.32/2.86 % (4166060)CaDiCaL version: 2.1.3
% 13.32/2.86 % (4166060)Termination reason: Instruction limit
% 13.32/2.86 % (4166060)Termination phase: Saturation
% 13.32/2.86 % (4166060)Time elapsed: 0.074 s
% 13.32/2.86 % (4166060)Peak memory usage: 92 MB
% 13.32/2.86 % (4166060)Instructions burned: 140 (million)
% 13.32/2.86 % (4166071)lrs+1011_1_sil=32000:sp=occurrence:random_seed=132873506:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 13.32/2.86 % (4166069)lrs+10_1_sil=8000:sp=occurrence:random_seed=1225170856:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 13.32/2.86 % (4166070)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4151033712:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 13.32/2.86 % (4166072)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=2254137522:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 13.32/2.86 % (4166070)Instruction limit reached!
% 9.23/3.04 % (4166070)------------------------------
% 9.23/3.04 % (4166070)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.23/3.04 % (4166070)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.23/3.04 % (4166070)CaDiCaL version: 2.1.3
% 9.23/3.04 % (4166070)Termination reason: Instruction limit
% 9.23/3.04 % (4166070)Termination phase: Saturation
% 9.23/3.04 % (4166070)Time elapsed: 0.078 s
% 9.23/3.04 % (4166070)Peak memory usage: 90 MB
% 9.23/3.04 % (4166070)Instructions burned: 157 (million)
% 9.23/3.04 % (4166072)Instruction limit reached!
% 9.23/3.04 % (4166072)------------------------------
% 9.23/3.04 % (4166072)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.23/3.04 % (4166072)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.23/3.04 % (4166072)CaDiCaL version: 2.1.3
% 9.23/3.04 % (4166072)Termination reason: Instruction limit
% 9.23/3.04 % (4166072)Termination phase: Saturation
% 9.23/3.04 % (4166072)Time elapsed: 0.152 s
% 9.23/3.04 % (4166072)Peak memory usage: 95 MB
% 9.23/3.04 % (4166072)Instructions burned: 248 (million)
% 9.23/3.04 % (4166069)Instruction limit reached!
% 9.23/3.04 % (4166069)------------------------------
% 9.23/3.04 % (4166069)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.23/3.04 % (4166069)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.23/3.04 % (4166069)CaDiCaL version: 2.1.3
% 9.23/3.04 % (4166069)Termination reason: Instruction limit
% 9.23/3.04 % (4166069)Termination phase: Saturation
% 9.23/3.04 % (4166069)Time elapsed: 0.168 s
% 9.23/3.04 % (4166069)Peak memory usage: 95 MB
% 9.23/3.04 % (4166069)Instructions burned: 286 (million)
% 9.23/3.04 % (4166071)Instruction limit reached!
% 9.23/3.04 % (4166071)------------------------------
% 9.23/3.04 % (4166071)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.23/3.04 % (4166071)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.23/3.04 % (4166071)CaDiCaL version: 2.1.3
% 9.23/3.04 % (4166071)Termination reason: Instruction limit
% 9.23/3.04 % (4166071)Termination phase: Saturation
% 9.23/3.04 % (4166071)Time elapsed: 0.199 s
% 9.23/3.04 % (4166071)Peak memory usage: 96 MB
% 9.23/3.04 % (4166071)Instructions burned: 325 (million)
% 9.23/3.04 % (4166077)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1977458259:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 9.23/3.04 % (4166079)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3069348674:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 9.23/3.04 % (4166078)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2639973699:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 9.23/3.04 % (4166080)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2614489328:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 9.23/3.04 % (4166079)Instruction limit reached!
% 9.23/3.04 % (4166079)------------------------------
% 9.23/3.04 % (4166079)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.23/3.04 % (4166079)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.23/3.04 % (4166079)CaDiCaL version: 2.1.3
% 9.23/3.04 % (4166079)Termination reason: Instruction limit
% 9.23/3.04 % (4166079)Termination phase: Saturation
% 9.23/3.04 % (4166079)Time elapsed: 0.060 s
% 9.23/3.04 % (4166079)Peak memory usage: 92 MB
% 9.23/3.04 % (4166079)Instructions burned: 114 (million)
% 9.23/3.04 % (4166077)Instruction limit reached!
% 9.23/3.04 % (4166077)------------------------------
% 9.23/3.04 % (4166077)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.23/3.04 % (4166077)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.23/3.04 % (4166077)CaDiCaL version: 2.1.3
% 9.23/3.04 % (4166077)Termination reason: Instruction limit
% 9.23/3.04 % (4166077)Termination phase: Saturation
% 9.23/3.04 % (4166077)Time elapsed: 0.175 s
% 9.23/3.04 % (4166077)Peak memory usage: 94 MB
% 9.23/3.04 % (4166077)Instructions burned: 295 (million)
% 9.23/3.04 % (4166080)Instruction limit reached!
% 9.23/3.04 % (4166080)------------------------------
% 9.23/3.04 % (4166080)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.23/3.04 % (4166080)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.23/3.04 % (4166080)CaDiCaL version: 2.1.3
% 9.23/3.04 % (4166080)Termination reason: Instruction limit
% 9.23/3.04 % (4166080)Termination phase: Blocked clause elimination
% 9.23/3.04 % (4166080)Time elapsed: 0.069 s
% 9.23/3.04 % (4166080)Peak memory usage: 91 MB
% 9.23/3.04 % (4166080)Instructions burned: 127 (million)
% 9.23/3.04 % (4166085)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3818227279:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 9.23/3.04 % (4166086)lrs+10_1_sil=8000:sp=occurrence:random_seed=1279111141:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 9.23/3.04 % (4166085)Instruction limit reached!
% 9.23/3.04 % (4166085)------------------------------
% 9.23/3.04 % (4166085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.23/3.04 % (4166085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.23/3.04 % (4166085)CaDiCaL version: 2.1.3
% 9.23/3.04 % (4166085)Termination reason: Instruction limit
% 9.23/3.04 % (4166085)Termination phase: Saturation
% 9.23/3.04 % (4166085)Time elapsed: 0.053 s
% 9.23/3.04 % (4166085)Peak memory usage: 90 MB
% 9.23/3.04 % (4166085)Instructions burned: 116 (million)
% 9.23/3.04 % (4166087)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3598648124:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 9.23/3.04 % (4166091)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3925663733:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 9.23/3.04 % (4166087)Instruction limit reached!
% 9.23/3.04 % (4166087)------------------------------
% 9.23/3.04 % (4166087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.23/3.04 % (4166087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.23/3.04 % (4166087)CaDiCaL version: 2.1.3
% 9.23/3.04 % (4166087)Termination reason: Instruction limit
% 9.23/3.04 % (4166087)Termination phase: Saturation
% 9.23/3.04 % (4166087)Time elapsed: 0.258 s
% 9.23/3.04 % (4166087)Peak memory usage: 97 MB
% 9.23/3.04 % (4166087)Instructions burned: 438 (million)
% 9.23/3.04 % (4166093)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4238035303:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 9.23/3.04 % (4166093)Instruction limit reached!
% 9.23/3.04 % (4166093)------------------------------
% 9.23/3.04 % (4166093)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.23/3.04 % (4166093)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.23/3.04 % (4166093)CaDiCaL version: 2.1.3
% 9.23/3.04 % (4166093)Termination reason: Instruction limit
% 9.23/3.04 % (4166093)Termination phase: Property scanning
% 9.23/3.04 % (4166093)Time elapsed: 0.070 s
% 9.23/3.04 % (4166093)Peak memory usage: 91 MB
% 9.23/3.04 % (4166093)Instructions burned: 136 (million)
% 9.23/3.04 % (4166086)Instruction limit reached!
% 9.23/3.04 % (4166086)------------------------------
% 9.23/3.04 % (4166086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.23/3.04 % (4166086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.23/3.04 % (4166086)CaDiCaL version: 2.1.3
% 9.23/3.04 % (4166086)Termination reason: Instruction limit
% 9.23/3.04 % (4166086)Termination phase: Saturation
% 9.23/3.04 % (4166086)Time elapsed: 0.571 s
% 9.23/3.04 % (4166086)Peak memory usage: 106 MB
% 9.23/3.04 % (4166086)Instructions burned: 909 (million)
% 9.23/3.04 % (4166095)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3638066437:st=8:i=592:sd=3:ep=RST:ss=axioms_2986 on theBenchmark for (2986ds/592Mi)
% 9.23/3.04 % (4166096)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=1548675763:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 9.23/3.04 % (4166095)Instruction limit reached!
% 9.23/3.04 % (4166095)------------------------------
% 9.23/3.04 % (4166095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.23/3.04 % (4166095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.23/3.04 % (4166095)CaDiCaL version: 2.1.3
% 9.23/3.04 % (4166095)Termination reason: Instruction limit
% 9.23/3.04 % (4166095)Termination phase: Saturation
% 9.23/3.04 % (4166095)Time elapsed: 0.356 s
% 9.23/3.04 % (4166095)Peak memory usage: 99 MB
% 9.23/3.04 % (4166095)Instructions burned: 593 (million)
% 9.23/3.04 % (4166056)First to succeed.
% 9.23/3.04 % (4166056)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-4166050"
% 9.23/3.04 % (4166099)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=3799755737:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2981 on theBenchmark for (2981ds/125Mi)
% 9.23/3.04 % (4166099)Instruction limit reached!
% 9.23/3.04 % (4166099)------------------------------
% 9.23/3.04 % (4166099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.23/3.04 % (4166099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.23/3.04 % (4166099)CaDiCaL version: 2.1.3
% 9.23/3.04 % (4166099)Termination reason: Instruction limit
% 9.23/3.04 % (4166099)Termination phase: Saturation
% 9.23/3.04 % (4166099)Time elapsed: 0.071 s
% 9.23/3.04 % (4166099)Peak memory usage: 92 MB
% 9.23/3.04 % (4166099)Instructions burned: 125 (million)
% 9.23/3.04 % (4166055)Also succeeded, but the first one will report.
% 9.23/3.04 % (4166078)Instruction limit reached!
% 9.23/3.04 % (4166078)------------------------------
% 9.23/3.04 % (4166078)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.23/3.04 % (4166078)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.23/3.04 % (4166078)CaDiCaL version: 2.1.3
% 9.23/3.04 % (4166078)Termination reason: Instruction limit
% 9.23/3.04 % (4166078)Termination phase: Saturation
% 9.23/3.04 % (4166078)Time elapsed: 1.434 s
% 9.23/3.04 % (4166078)Peak memory usage: 175 MB
% 9.23/3.04 % (4166078)Instructions burned: 2350 (million)
% 9.23/3.04 % (4166056)Refutation found. Thanks to Tanya!
% 9.23/3.04 % SZS status Theorem for theBenchmark
% 9.23/3.04 % SZS output start Proof for theBenchmark
% See solution above
% 15.73/3.24 % (4166056)------------------------------
% 15.73/3.24 % (4166056)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.73/3.24 % (4166056)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.73/3.24 % (4166056)CaDiCaL version: 2.1.3
% 15.73/3.24 % (4166056)Termination reason: Refutation
% 15.73/3.24 % (4166056)Time elapsed: 1.818 s
% 15.73/3.24 % (4166056)Peak memory usage: 175 MB
% 15.73/3.24 % (4166056)Instructions burned: 4850 (million)
% 15.73/3.24 % (4166056)------------------------------
% 15.73/3.24 % (4166056)------------------------------
% 15.73/3.24 % (4166050)Success in time 2.174 s
% 15.73/3.24 % Vampire exiting
%------------------------------------------------------------------------------