%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU390+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/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:40 PM UTC 2026
% Result : Theorem 6.25s 2.50s
% Output : Refutation 0.18s
% Verified :
% SZS Type : Refutation
% Derivation depth : 70
% Number of leaves : 37
% Syntax : Number of formulae : 359 ( 27 unt; 12 def)
% Number of atoms : 1930 ( 171 equ)
% Maximal formula atoms : 22 ( 5 avg)
% Number of connectives : 2659 (1088 ~;1304 |; 194 &)
% ( 26 <=>; 47 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 7 avg)
% Maximal term depth : 5 ( 1 avg)
% Number of predicates : 33 ( 31 usr; 11 prp; 0-4 aty)
% Number of functors : 24 ( 24 usr; 4 con; 0-4 aty)
% Number of variables : 512 ( 0 sgn 481 !; 31 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f7,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/sandbox2/benchmark/theBenchmark.p',d11_waybel_0) ).
fof(f8,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0) )
=> ! [X1] :
( ( ~ empty_carrier(X1)
& net_str(X1,X0) )
=> ! [X2] :
( element(X2,powerset(the_carrier(X0)))
=> ( netstr_induced_subset(X2,X0,X1)
<=> ? [X3] :
( element(X3,the_carrier(X1))
& X2 = relation_rng_as_subset(the_carrier(netstr_restr_to_element(X0,X1,X3)),the_carrier(X0),the_mapping(X0,netstr_restr_to_element(X0,X1,X3))) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_yellow19) ).
fof(f9,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0) )
=> ! [X1] :
( ( ~ empty_carrier(X1)
& net_str(X1,X0) )
=> ! [X2] :
( element(X2,the_carrier(X1))
=> ! [X3] :
( ( strict_net_str(X3,X0)
& net_str(X3,X0) )
=> ( X3 = netstr_restr_to_element(X0,X1,X2)
<=> ( ! [X4] :
( in(X4,the_carrier(X3))
<=> ? [X5] :
( element(X5,the_carrier(X1))
& X5 = X4
& related(X1,X2,X5) ) )
& the_InternalRel(X3) = relation_restriction_as_relation_of(the_InternalRel(X1),the_carrier(X3))
& the_mapping(X0,X3) = partfun_dom_restriction(the_carrier(X1),the_carrier(X0),the_mapping(X0,X1),the_carrier(X3)) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d7_waybel_9) ).
fof(f10,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0) )
=> ! [X1] :
( ( ~ empty_carrier(X1)
& net_str(X1,X0) )
=> ! [X2] :
( element(X2,the_carrier(X1))
=> apply_netmap(X0,X1,X2) = apply_on_structs(X1,X0,the_mapping(X0,X1),X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_waybel_0) ).
fof(f17,axiom,
! [X0,X1,X2,X3] :
( ( function(X2)
& relation_of2(X2,X0,X1) )
=> ( function(partfun_dom_restriction(X0,X1,X2,X3))
& relation_of2_as_subset(partfun_dom_restriction(X0,X1,X2,X3),X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k2_partfun1) ).
fof(f23,axiom,
! [X0,X1,X2] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0)
& ~ empty_carrier(X1)
& net_str(X1,X0)
& element(X2,the_carrier(X1)) )
=> ( strict_net_str(netstr_restr_to_element(X0,X1,X2),X0)
& net_str(netstr_restr_to_element(X0,X1,X2),X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_waybel_9) ).
fof(f24,axiom,
! [X0,X1,X2] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0)
& ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0)
& element(X2,the_carrier(X1)) )
=> ( strict_net_str(subnetstr_of_element(X0,X1,X2),X0)
& subnet(subnetstr_of_element(X0,X1,X2),X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k6_waybel_9) ).
fof(f26,axiom,
! [X0] :
( rel_str(X0)
=> one_sorted_str(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_orders_2) ).
fof(f28,axiom,
! [X0] :
( one_sorted_str(X0)
=> ! [X1] :
( net_str(X1,X0)
=> rel_str(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_waybel_0) ).
fof(f31,axiom,
! [X0,X1] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0)
& ~ empty_carrier(X1)
& net_str(X1,X0) )
=> ! [X2] :
( netstr_induced_subset(X2,X0,X1)
=> element(X2,powerset(the_carrier(X0))) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_yellow19) ).
fof(f33,axiom,
! [X0,X1] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0)
& ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) )
=> ! [X2] :
( subnet(X2,X0,X1)
=> ( ~ empty_carrier(X2)
& transitive_relstr(X2)
& directed_relstr(X2)
& net_str(X2,X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_yellow_6) ).
fof(f36,axiom,
! [X0,X1] :
( ( one_sorted_str(X0)
& net_str(X1,X0) )
=> ( function(the_mapping(X0,X1))
& quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
& relation_of2_as_subset(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_u1_waybel_0) ).
fof(f48,axiom,
! [X0,X1] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0)
& ~ empty_carrier(X1)
& net_str(X1,X0) )
=> ( ~ empty(the_mapping(X0,X1))
& relation(the_mapping(X0,X1))
& function(the_mapping(X0,X1))
& quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc15_yellow_6) ).
fof(f49,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0) )
=> ~ empty(the_carrier(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f53,axiom,
( empty(empty_set)
& relation(empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc4_relat_1) ).
fof(f74,axiom,
! [X0,X1,X2,X3] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0)
& ~ empty_carrier(X1)
& one_sorted_str(X1)
& function(X2)
& quasi_total(X2,the_carrier(X0),the_carrier(X1))
& relation_of2(X2,the_carrier(X0),the_carrier(X1))
& element(X3,the_carrier(X0)) )
=> apply_on_structs(X0,X1,X2,X3) = apply(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k1_waybel_0) ).
fof(f75,axiom,
! [X0,X1,X2,X3] :
( ( function(X2)
& relation_of2(X2,X0,X1) )
=> partfun_dom_restriction(X0,X1,X2,X3) = relation_dom_restriction(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k2_partfun1) ).
fof(f76,axiom,
! [X0,X1,X2] :
( relation_of2(X2,X0,X1)
=> relation_rng_as_subset(X0,X1,X2) = relation_rng(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k5_relset_1) ).
fof(f77,axiom,
! [X0,X1,X2] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0)
& ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0)
& element(X2,the_carrier(X1)) )
=> subnetstr_of_element(X0,X1,X2) = netstr_restr_to_element(X0,X1,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k6_waybel_9) ).
fof(f78,axiom,
! [X0,X1,X2] :
( relation_of2_as_subset(X2,X0,X1)
<=> relation_of2(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_m2_relset_1) ).
fof(f80,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0) )
=> ! [X1] :
( ( ~ empty_carrier(X1)
& directed_relstr(X1)
& net_str(X1,X0) )
=> ! [X2] :
( element(X2,the_carrier(X1))
=> ! [X3] :
( element(X3,the_carrier(X1))
=> ! [X4] :
( element(X4,the_carrier(netstr_restr_to_element(X0,X1,X2)))
=> ( X3 = X4
=> apply_netmap(X0,X1,X3) = apply_netmap(X0,netstr_restr_to_element(X0,X1,X2),X4) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t16_waybel_9) ).
fof(f81,axiom,
! [X0,X1] :
( in(X0,X1)
=> element(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
fof(f82,axiom,
! [X0,X1] :
( element(X0,X1)
=> ( empty(X1)
| in(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
fof(f87,axiom,
! [X0,X1,X2,X3] :
( ( function(X3)
& quasi_total(X3,X0,X1)
& relation_of2_as_subset(X3,X0,X1) )
=> ( in(X2,X0)
=> ( X1 = empty_set
| in(apply(X3,X2),relation_rng(X3)) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t6_funct_2) ).
fof(f90,conjecture,
! [X0] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0) )
=> ! [X1] :
( ( ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) )
=> ! [X2] :
( netstr_induced_subset(X2,X0,X1)
=> is_eventually_in(X0,X1,X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t9_yellow19) ).
fof(f91,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] :
( netstr_induced_subset(X2,X0,X1)
=> is_eventually_in(X0,X1,X2) ) ) ),
inference(negated_conjecture,[status(cth)],[f90]) ).
fof(f101,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,[],[f7]) ).
fof(f102,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,[],[f101]) ).
fof(f103,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( netstr_induced_subset(X2,X0,X1)
<=> ? [X3] :
( element(X3,the_carrier(X1))
& X2 = relation_rng_as_subset(the_carrier(netstr_restr_to_element(X0,X1,X3)),the_carrier(X0),the_mapping(X0,netstr_restr_to_element(X0,X1,X3))) ) )
| ~ element(X2,powerset(the_carrier(X0))) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f8]) ).
fof(f104,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( netstr_induced_subset(X2,X0,X1)
<=> ? [X3] :
( element(X3,the_carrier(X1))
& X2 = relation_rng_as_subset(the_carrier(netstr_restr_to_element(X0,X1,X3)),the_carrier(X0),the_mapping(X0,netstr_restr_to_element(X0,X1,X3))) ) )
| ~ element(X2,powerset(the_carrier(X0))) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(flattening,[],[f103]) ).
fof(f105,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( X3 = netstr_restr_to_element(X0,X1,X2)
<=> ( ! [X4] :
( in(X4,the_carrier(X3))
<=> ? [X5] :
( element(X5,the_carrier(X1))
& X5 = X4
& related(X1,X2,X5) ) )
& the_InternalRel(X3) = relation_restriction_as_relation_of(the_InternalRel(X1),the_carrier(X3))
& the_mapping(X0,X3) = partfun_dom_restriction(the_carrier(X1),the_carrier(X0),the_mapping(X0,X1),the_carrier(X3)) ) )
| ~ strict_net_str(X3,X0)
| ~ net_str(X3,X0) )
| ~ element(X2,the_carrier(X1)) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f9]) ).
fof(f106,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ( X3 = netstr_restr_to_element(X0,X1,X2)
<=> ( ! [X4] :
( in(X4,the_carrier(X3))
<=> ? [X5] :
( element(X5,the_carrier(X1))
& X5 = X4
& related(X1,X2,X5) ) )
& the_InternalRel(X3) = relation_restriction_as_relation_of(the_InternalRel(X1),the_carrier(X3))
& the_mapping(X0,X3) = partfun_dom_restriction(the_carrier(X1),the_carrier(X0),the_mapping(X0,X1),the_carrier(X3)) ) )
| ~ strict_net_str(X3,X0)
| ~ net_str(X3,X0) )
| ~ element(X2,the_carrier(X1)) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(flattening,[],[f105]) ).
fof(f107,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( apply_netmap(X0,X1,X2) = apply_on_structs(X1,X0,the_mapping(X0,X1),X2)
| ~ element(X2,the_carrier(X1)) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f10]) ).
fof(f108,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( apply_netmap(X0,X1,X2) = apply_on_structs(X1,X0,the_mapping(X0,X1),X2)
| ~ element(X2,the_carrier(X1)) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(flattening,[],[f107]) ).
fof(f114,plain,
! [X0,X1,X2,X3] :
( ( function(partfun_dom_restriction(X0,X1,X2,X3))
& relation_of2_as_subset(partfun_dom_restriction(X0,X1,X2,X3),X0,X1) )
| ~ function(X2)
| ~ relation_of2(X2,X0,X1) ),
inference(ennf_transformation,[],[f17]) ).
fof(f115,plain,
! [X0,X1,X2,X3] :
( ( function(partfun_dom_restriction(X0,X1,X2,X3))
& relation_of2_as_subset(partfun_dom_restriction(X0,X1,X2,X3),X0,X1) )
| ~ function(X2)
| ~ relation_of2(X2,X0,X1) ),
inference(flattening,[],[f114]) ).
fof(f120,plain,
! [X0,X1,X2] :
( ( strict_net_str(netstr_restr_to_element(X0,X1,X2),X0)
& net_str(netstr_restr_to_element(X0,X1,X2),X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ net_str(X1,X0)
| ~ element(X2,the_carrier(X1)) ),
inference(ennf_transformation,[],[f23]) ).
fof(f121,plain,
! [X0,X1,X2] :
( ( strict_net_str(netstr_restr_to_element(X0,X1,X2),X0)
& net_str(netstr_restr_to_element(X0,X1,X2),X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ net_str(X1,X0)
| ~ element(X2,the_carrier(X1)) ),
inference(flattening,[],[f120]) ).
fof(f122,plain,
! [X0,X1,X2] :
( ( strict_net_str(subnetstr_of_element(X0,X1,X2),X0)
& subnet(subnetstr_of_element(X0,X1,X2),X0,X1) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0)
| ~ element(X2,the_carrier(X1)) ),
inference(ennf_transformation,[],[f24]) ).
fof(f123,plain,
! [X0,X1,X2] :
( ( strict_net_str(subnetstr_of_element(X0,X1,X2),X0)
& subnet(subnetstr_of_element(X0,X1,X2),X0,X1) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0)
| ~ element(X2,the_carrier(X1)) ),
inference(flattening,[],[f122]) ).
fof(f125,plain,
! [X0] :
( one_sorted_str(X0)
| ~ rel_str(X0) ),
inference(ennf_transformation,[],[f26]) ).
fof(f126,plain,
! [X0] :
( ! [X1] :
( rel_str(X1)
| ~ net_str(X1,X0) )
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f28]) ).
fof(f127,plain,
! [X0,X1] :
( ! [X2] :
( element(X2,powerset(the_carrier(X0)))
| ~ netstr_induced_subset(X2,X0,X1) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ net_str(X1,X0) ),
inference(ennf_transformation,[],[f31]) ).
fof(f128,plain,
! [X0,X1] :
( ! [X2] :
( element(X2,powerset(the_carrier(X0)))
| ~ netstr_induced_subset(X2,X0,X1) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ net_str(X1,X0) ),
inference(flattening,[],[f127]) ).
fof(f130,plain,
! [X0,X1] :
( ! [X2] :
( ( ~ empty_carrier(X2)
& transitive_relstr(X2)
& directed_relstr(X2)
& net_str(X2,X0) )
| ~ subnet(X2,X0,X1) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0) ),
inference(ennf_transformation,[],[f33]) ).
fof(f131,plain,
! [X0,X1] :
( ! [X2] :
( ( ~ empty_carrier(X2)
& transitive_relstr(X2)
& directed_relstr(X2)
& net_str(X2,X0) )
| ~ subnet(X2,X0,X1) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0) ),
inference(flattening,[],[f130]) ).
fof(f133,plain,
! [X0,X1] :
( ( function(the_mapping(X0,X1))
& quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
& relation_of2_as_subset(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0)) )
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(ennf_transformation,[],[f36]) ).
fof(f134,plain,
! [X0,X1] :
( ( function(the_mapping(X0,X1))
& quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
& relation_of2_as_subset(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0)) )
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(flattening,[],[f133]) ).
fof(f144,plain,
! [X0,X1] :
( ( ~ empty(the_mapping(X0,X1))
& relation(the_mapping(X0,X1))
& function(the_mapping(X0,X1))
& quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0)) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ net_str(X1,X0) ),
inference(ennf_transformation,[],[f48]) ).
fof(f145,plain,
! [X0,X1] :
( ( ~ empty(the_mapping(X0,X1))
& relation(the_mapping(X0,X1))
& function(the_mapping(X0,X1))
& quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0)) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ net_str(X1,X0) ),
inference(flattening,[],[f144]) ).
fof(f146,plain,
! [X0] :
( ~ empty(the_carrier(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f49]) ).
fof(f147,plain,
! [X0] :
( ~ empty(the_carrier(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(flattening,[],[f146]) ).
fof(f171,plain,
! [X0,X1,X2,X3] :
( apply_on_structs(X0,X1,X2,X3) = apply(X2,X3)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ function(X2)
| ~ quasi_total(X2,the_carrier(X0),the_carrier(X1))
| ~ relation_of2(X2,the_carrier(X0),the_carrier(X1))
| ~ element(X3,the_carrier(X0)) ),
inference(ennf_transformation,[],[f74]) ).
fof(f172,plain,
! [X0,X1,X2,X3] :
( apply_on_structs(X0,X1,X2,X3) = apply(X2,X3)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ function(X2)
| ~ quasi_total(X2,the_carrier(X0),the_carrier(X1))
| ~ relation_of2(X2,the_carrier(X0),the_carrier(X1))
| ~ element(X3,the_carrier(X0)) ),
inference(flattening,[],[f171]) ).
fof(f173,plain,
! [X0,X1,X2,X3] :
( partfun_dom_restriction(X0,X1,X2,X3) = relation_dom_restriction(X2,X3)
| ~ function(X2)
| ~ relation_of2(X2,X0,X1) ),
inference(ennf_transformation,[],[f75]) ).
fof(f174,plain,
! [X0,X1,X2,X3] :
( partfun_dom_restriction(X0,X1,X2,X3) = relation_dom_restriction(X2,X3)
| ~ function(X2)
| ~ relation_of2(X2,X0,X1) ),
inference(flattening,[],[f173]) ).
fof(f175,plain,
! [X0,X1,X2] :
( relation_rng_as_subset(X0,X1,X2) = relation_rng(X2)
| ~ relation_of2(X2,X0,X1) ),
inference(ennf_transformation,[],[f76]) ).
fof(f176,plain,
! [X0,X1,X2] :
( subnetstr_of_element(X0,X1,X2) = netstr_restr_to_element(X0,X1,X2)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0)
| ~ element(X2,the_carrier(X1)) ),
inference(ennf_transformation,[],[f77]) ).
fof(f177,plain,
! [X0,X1,X2] :
( subnetstr_of_element(X0,X1,X2) = netstr_restr_to_element(X0,X1,X2)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0)
| ~ element(X2,the_carrier(X1)) ),
inference(flattening,[],[f176]) ).
fof(f178,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( apply_netmap(X0,X1,X3) = apply_netmap(X0,netstr_restr_to_element(X0,X1,X2),X4)
| X3 != X4
| ~ element(X4,the_carrier(netstr_restr_to_element(X0,X1,X2))) )
| ~ element(X3,the_carrier(X1)) )
| ~ element(X2,the_carrier(X1)) )
| empty_carrier(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f80]) ).
fof(f179,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( apply_netmap(X0,X1,X3) = apply_netmap(X0,netstr_restr_to_element(X0,X1,X2),X4)
| X3 != X4
| ~ element(X4,the_carrier(netstr_restr_to_element(X0,X1,X2))) )
| ~ element(X3,the_carrier(X1)) )
| ~ element(X2,the_carrier(X1)) )
| empty_carrier(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(flattening,[],[f178]) ).
fof(f180,plain,
! [X0,X1] :
( element(X0,X1)
| ~ in(X0,X1) ),
inference(ennf_transformation,[],[f81]) ).
fof(f181,plain,
! [X0,X1] :
( empty(X1)
| in(X0,X1)
| ~ element(X0,X1) ),
inference(ennf_transformation,[],[f82]) ).
fof(f182,plain,
! [X0,X1] :
( empty(X1)
| in(X0,X1)
| ~ element(X0,X1) ),
inference(flattening,[],[f181]) ).
fof(f188,plain,
! [X0,X1,X2,X3] :
( X1 = empty_set
| in(apply(X3,X2),relation_rng(X3))
| ~ in(X2,X0)
| ~ function(X3)
| ~ quasi_total(X3,X0,X1)
| ~ relation_of2_as_subset(X3,X0,X1) ),
inference(ennf_transformation,[],[f87]) ).
fof(f189,plain,
! [X0,X1,X2,X3] :
( X1 = empty_set
| in(apply(X3,X2),relation_rng(X3))
| ~ in(X2,X0)
| ~ function(X3)
| ~ quasi_total(X3,X0,X1)
| ~ relation_of2_as_subset(X3,X0,X1) ),
inference(flattening,[],[f188]) ).
fof(f192,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ is_eventually_in(X0,X1,X2)
& netstr_induced_subset(X2,X0,X1) )
& ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) )
& ~ empty_carrier(X0)
& one_sorted_str(X0) ),
inference(ennf_transformation,[],[f91]) ).
fof(f193,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ~ is_eventually_in(X0,X1,X2)
& netstr_induced_subset(X2,X0,X1) )
& ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) )
& ~ empty_carrier(X0)
& one_sorted_str(X0) ),
inference(flattening,[],[f192]) ).
fof(f194,definition,
! [X1,X2,X3,X0] :
( sP0(X1,X2,X3,X0)
<=> ( ! [X4] :
( in(X4,the_carrier(X3))
<=> ? [X5] :
( element(X5,the_carrier(X1))
& X5 = X4
& related(X1,X2,X5) ) )
& the_InternalRel(X3) = relation_restriction_as_relation_of(the_InternalRel(X1),the_carrier(X3))
& the_mapping(X0,X3) = partfun_dom_restriction(the_carrier(X1),the_carrier(X0),the_mapping(X0,X1),the_carrier(X3)) ) ),
introduced(definition,[new_symbols(definition,[sP0])],[predicate_definition_introduction]) ).
fof(f195,definition,
! [X0,X3,X2,X1] :
( ( X3 = netstr_restr_to_element(X0,X1,X2)
<=> sP0(X1,X2,X3,X0) )
| ~ sP1(X0,X3,X2,X1) ),
introduced(definition,[new_symbols(definition,[sP1])],[predicate_definition_introduction]) ).
fof(f196,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( sP1(X0,X3,X2,X1)
| ~ strict_net_str(X3,X0)
| ~ net_str(X3,X0) )
| ~ element(X2,the_carrier(X1)) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(definition_folding,[],[f106,f195,f194]) ).
fof(f197,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,[],[f102]) ).
fof(f198,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,[],[f197]) ).
fof(f199,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( is_eventually_in(X0,X1,X2)
| ! [X3] :
( ~ element(X3,the_carrier(X1))
| ( ~ in(apply_netmap(X0,X1,sK2(X0,X1,X2,X3)),X2)
& related(X1,X3,sK2(X0,X1,X2,X3))
& element(sK2(X0,X1,X2,X3),the_carrier(X1)) ) ) )
& ( ( element(sK3(X0,X1,X2),the_carrier(X1))
& ! [X6] :
( in(apply_netmap(X0,X1,X6),X2)
| ~ related(X1,sK3(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,[sK2,sK3]),skolemize(X4,sK2(X0,X1,X2,X3)),skolemize(X5,sK3(X0,X1,X2))],[f198]) ).
fof(f200,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( netstr_induced_subset(X2,X0,X1)
| ! [X3] :
( ~ element(X3,the_carrier(X1))
| relation_rng_as_subset(the_carrier(netstr_restr_to_element(X0,X1,X3)),the_carrier(X0),the_mapping(X0,netstr_restr_to_element(X0,X1,X3))) != X2 ) )
& ( ? [X3] :
( element(X3,the_carrier(X1))
& X2 = relation_rng_as_subset(the_carrier(netstr_restr_to_element(X0,X1,X3)),the_carrier(X0),the_mapping(X0,netstr_restr_to_element(X0,X1,X3))) )
| ~ netstr_induced_subset(X2,X0,X1) ) )
| ~ element(X2,powerset(the_carrier(X0))) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(nnf_transformation,[],[f104]) ).
fof(f201,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( netstr_induced_subset(X2,X0,X1)
| ! [X3] :
( ~ element(X3,the_carrier(X1))
| relation_rng_as_subset(the_carrier(netstr_restr_to_element(X0,X1,X3)),the_carrier(X0),the_mapping(X0,netstr_restr_to_element(X0,X1,X3))) != X2 ) )
& ( ? [X4] :
( element(X4,the_carrier(X1))
& relation_rng_as_subset(the_carrier(netstr_restr_to_element(X0,X1,X4)),the_carrier(X0),the_mapping(X0,netstr_restr_to_element(X0,X1,X4))) = X2 )
| ~ netstr_induced_subset(X2,X0,X1) ) )
| ~ element(X2,powerset(the_carrier(X0))) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(rectify,[],[f200]) ).
fof(f202,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( netstr_induced_subset(X2,X0,X1)
| ! [X3] :
( ~ element(X3,the_carrier(X1))
| relation_rng_as_subset(the_carrier(netstr_restr_to_element(X0,X1,X3)),the_carrier(X0),the_mapping(X0,netstr_restr_to_element(X0,X1,X3))) != X2 ) )
& ( ( element(sK4(X0,X1,X2),the_carrier(X1))
& relation_rng_as_subset(the_carrier(netstr_restr_to_element(X0,X1,sK4(X0,X1,X2))),the_carrier(X0),the_mapping(X0,netstr_restr_to_element(X0,X1,sK4(X0,X1,X2)))) = X2 )
| ~ netstr_induced_subset(X2,X0,X1) ) )
| ~ element(X2,powerset(the_carrier(X0))) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(X4,sK4(X0,X1,X2))],[f201]) ).
fof(f203,plain,
! [X0,X3,X2,X1] :
( ( ( X3 = netstr_restr_to_element(X0,X1,X2)
| ~ sP0(X1,X2,X3,X0) )
& ( sP0(X1,X2,X3,X0)
| netstr_restr_to_element(X0,X1,X2) != X3 ) )
| ~ sP1(X0,X3,X2,X1) ),
inference(nnf_transformation,[],[f195]) ).
fof(f204,plain,
! [X0,X1,X2,X3] :
( ( ( netstr_restr_to_element(X0,X3,X2) = X1
| ~ sP0(X3,X2,X1,X0) )
& ( sP0(X3,X2,X1,X0)
| netstr_restr_to_element(X0,X3,X2) != X1 ) )
| ~ sP1(X0,X1,X2,X3) ),
inference(rectify,[],[f203]) ).
fof(f205,plain,
! [X1,X2,X3,X0] :
( ( sP0(X1,X2,X3,X0)
| ? [X4] :
( ( ! [X5] :
( ~ element(X5,the_carrier(X1))
| X4 != X5
| ~ related(X1,X2,X5) )
| ~ in(X4,the_carrier(X3)) )
& ( ? [X5] :
( element(X5,the_carrier(X1))
& X5 = X4
& related(X1,X2,X5) )
| in(X4,the_carrier(X3)) ) )
| the_InternalRel(X3) != relation_restriction_as_relation_of(the_InternalRel(X1),the_carrier(X3))
| the_mapping(X0,X3) != partfun_dom_restriction(the_carrier(X1),the_carrier(X0),the_mapping(X0,X1),the_carrier(X3)) )
& ( ( ! [X4] :
( ( in(X4,the_carrier(X3))
| ! [X5] :
( ~ element(X5,the_carrier(X1))
| X4 != X5
| ~ related(X1,X2,X5) ) )
& ( ? [X5] :
( element(X5,the_carrier(X1))
& X5 = X4
& related(X1,X2,X5) )
| ~ in(X4,the_carrier(X3)) ) )
& the_InternalRel(X3) = relation_restriction_as_relation_of(the_InternalRel(X1),the_carrier(X3))
& the_mapping(X0,X3) = partfun_dom_restriction(the_carrier(X1),the_carrier(X0),the_mapping(X0,X1),the_carrier(X3)) )
| ~ sP0(X1,X2,X3,X0) ) ),
inference(nnf_transformation,[],[f194]) ).
fof(f206,plain,
! [X1,X2,X3,X0] :
( ( sP0(X1,X2,X3,X0)
| ? [X4] :
( ( ! [X5] :
( ~ element(X5,the_carrier(X1))
| X4 != X5
| ~ related(X1,X2,X5) )
| ~ in(X4,the_carrier(X3)) )
& ( ? [X5] :
( element(X5,the_carrier(X1))
& X5 = X4
& related(X1,X2,X5) )
| in(X4,the_carrier(X3)) ) )
| the_InternalRel(X3) != relation_restriction_as_relation_of(the_InternalRel(X1),the_carrier(X3))
| the_mapping(X0,X3) != partfun_dom_restriction(the_carrier(X1),the_carrier(X0),the_mapping(X0,X1),the_carrier(X3)) )
& ( ( ! [X4] :
( ( in(X4,the_carrier(X3))
| ! [X5] :
( ~ element(X5,the_carrier(X1))
| X4 != X5
| ~ related(X1,X2,X5) ) )
& ( ? [X5] :
( element(X5,the_carrier(X1))
& X5 = X4
& related(X1,X2,X5) )
| ~ in(X4,the_carrier(X3)) ) )
& the_InternalRel(X3) = relation_restriction_as_relation_of(the_InternalRel(X1),the_carrier(X3))
& the_mapping(X0,X3) = partfun_dom_restriction(the_carrier(X1),the_carrier(X0),the_mapping(X0,X1),the_carrier(X3)) )
| ~ sP0(X1,X2,X3,X0) ) ),
inference(flattening,[],[f205]) ).
fof(f207,plain,
! [X0,X1,X2,X3] :
( ( sP0(X0,X1,X2,X3)
| ? [X4] :
( ( ! [X5] :
( ~ element(X5,the_carrier(X0))
| X4 != X5
| ~ related(X0,X1,X5) )
| ~ in(X4,the_carrier(X2)) )
& ( ? [X6] :
( element(X6,the_carrier(X0))
& X4 = X6
& related(X0,X1,X6) )
| in(X4,the_carrier(X2)) ) )
| the_InternalRel(X2) != relation_restriction_as_relation_of(the_InternalRel(X0),the_carrier(X2))
| the_mapping(X3,X2) != partfun_dom_restriction(the_carrier(X0),the_carrier(X3),the_mapping(X3,X0),the_carrier(X2)) )
& ( ( ! [X7] :
( ( in(X7,the_carrier(X2))
| ! [X8] :
( ~ element(X8,the_carrier(X0))
| X7 != X8
| ~ related(X0,X1,X8) ) )
& ( ? [X9] :
( element(X9,the_carrier(X0))
& X7 = X9
& related(X0,X1,X9) )
| ~ in(X7,the_carrier(X2)) ) )
& the_InternalRel(X2) = relation_restriction_as_relation_of(the_InternalRel(X0),the_carrier(X2))
& the_mapping(X3,X2) = partfun_dom_restriction(the_carrier(X0),the_carrier(X3),the_mapping(X3,X0),the_carrier(X2)) )
| ~ sP0(X0,X1,X2,X3) ) ),
inference(rectify,[],[f206]) ).
fof(f208,plain,
! [X0,X1,X2,X3] :
( ( sP0(X0,X1,X2,X3)
| ( ( ! [X5] :
( ~ element(X5,the_carrier(X0))
| sK5(X0,X1,X2) != X5
| ~ related(X0,X1,X5) )
| ~ in(sK5(X0,X1,X2),the_carrier(X2)) )
& ( ( element(sK6(X0,X1,X2),the_carrier(X0))
& sK5(X0,X1,X2) = sK6(X0,X1,X2)
& related(X0,X1,sK6(X0,X1,X2)) )
| in(sK5(X0,X1,X2),the_carrier(X2)) ) )
| the_InternalRel(X2) != relation_restriction_as_relation_of(the_InternalRel(X0),the_carrier(X2))
| the_mapping(X3,X2) != partfun_dom_restriction(the_carrier(X0),the_carrier(X3),the_mapping(X3,X0),the_carrier(X2)) )
& ( ( ! [X7] :
( ( in(X7,the_carrier(X2))
| ! [X8] :
( ~ element(X8,the_carrier(X0))
| X7 != X8
| ~ related(X0,X1,X8) ) )
& ( ( element(sK7(X0,X1,X7),the_carrier(X0))
& sK7(X0,X1,X7) = X7
& related(X0,X1,sK7(X0,X1,X7)) )
| ~ in(X7,the_carrier(X2)) ) )
& the_InternalRel(X2) = relation_restriction_as_relation_of(the_InternalRel(X0),the_carrier(X2))
& the_mapping(X3,X2) = partfun_dom_restriction(the_carrier(X0),the_carrier(X3),the_mapping(X3,X0),the_carrier(X2)) )
| ~ sP0(X0,X1,X2,X3) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5,sK6,sK7]),skolemize(X4,sK5(X0,X1,X2)),skolemize(X6,sK6(X0,X1,X2)),skolemize(X9,sK7(X0,X1,X7))],[f207]) ).
fof(f231,plain,
! [X0,X1,X2] :
( ( relation_of2_as_subset(X2,X0,X1)
| ~ relation_of2(X2,X0,X1) )
& ( relation_of2(X2,X0,X1)
| ~ relation_of2_as_subset(X2,X0,X1) ) ),
inference(nnf_transformation,[],[f78]) ).
fof(f232,plain,
( ~ is_eventually_in(sK30,sK31,sK32)
& netstr_induced_subset(sK32,sK30,sK31)
& ~ empty_carrier(sK31)
& transitive_relstr(sK31)
& directed_relstr(sK31)
& net_str(sK31,sK30)
& ~ empty_carrier(sK30)
& one_sorted_str(sK30) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK30,sK31,sK32]),skolemize(X0,sK30),skolemize(X1,sK31),skolemize(X2,sK32)],[f193]) ).
fof(f241,plain,
! [X2,X3,X0,X1] :
( element(sK2(X0,X1,X2,X3),the_carrier(X1))
| ~ element(X3,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,[],[f199]) ).
fof(f242,plain,
! [X2,X3,X0,X1] :
( related(X1,X3,sK2(X0,X1,X2,X3))
| ~ element(X3,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,[],[f199]) ).
fof(f243,plain,
! [X2,X3,X0,X1] :
( ~ in(apply_netmap(X0,X1,sK2(X0,X1,X2,X3)),X2)
| ~ element(X3,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,[],[f199]) ).
fof(f244,plain,
! [X2,X0,X1] :
( relation_rng_as_subset(the_carrier(netstr_restr_to_element(X0,X1,sK4(X0,X1,X2))),the_carrier(X0),the_mapping(X0,netstr_restr_to_element(X0,X1,sK4(X0,X1,X2)))) = X2
| ~ netstr_induced_subset(X2,X0,X1)
| ~ element(X2,powerset(the_carrier(X0)))
| empty_carrier(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f202]) ).
fof(f245,plain,
! [X2,X0,X1] :
( element(sK4(X0,X1,X2),the_carrier(X1))
| ~ netstr_induced_subset(X2,X0,X1)
| ~ element(X2,powerset(the_carrier(X0)))
| empty_carrier(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f202]) ).
fof(f247,plain,
! [X2,X3,X0,X1] :
( sP0(X3,X2,X1,X0)
| netstr_restr_to_element(X0,X3,X2) != X1
| ~ sP1(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f204]) ).
fof(f249,plain,
! [X2,X3,X0,X1] :
( ~ sP0(X0,X1,X2,X3)
| the_mapping(X3,X2) = partfun_dom_restriction(the_carrier(X0),the_carrier(X3),the_mapping(X3,X0),the_carrier(X2)) ),
inference(cnf_transformation,[],[f208]) ).
fof(f254,plain,
! [X2,X3,X0,X1,X8,X7] :
( in(X7,the_carrier(X2))
| ~ element(X8,the_carrier(X0))
| X7 != X8
| ~ related(X0,X1,X8)
| ~ sP0(X0,X1,X2,X3) ),
inference(cnf_transformation,[],[f208]) ).
fof(f259,plain,
! [X2,X3,X0,X1] :
( sP1(X0,X3,X2,X1)
| ~ strict_net_str(X3,X0)
| ~ net_str(X3,X0)
| ~ element(X2,the_carrier(X1))
| empty_carrier(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f196]) ).
fof(f260,plain,
! [X2,X0,X1] :
( ~ element(X2,the_carrier(X1))
| apply_netmap(X0,X1,X2) = apply_on_structs(X1,X0,the_mapping(X0,X1),X2)
| empty_carrier(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f108]) ).
fof(f266,plain,
! [X2,X3,X0,X1] :
( function(partfun_dom_restriction(X0,X1,X2,X3))
| ~ function(X2)
| ~ relation_of2(X2,X0,X1) ),
inference(cnf_transformation,[],[f115]) ).
fof(f270,plain,
! [X2,X0,X1] :
( net_str(netstr_restr_to_element(X0,X1,X2),X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ net_str(X1,X0)
| ~ element(X2,the_carrier(X1)) ),
inference(cnf_transformation,[],[f121]) ).
fof(f271,plain,
! [X2,X0,X1] :
( strict_net_str(netstr_restr_to_element(X0,X1,X2),X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ net_str(X1,X0)
| ~ element(X2,the_carrier(X1)) ),
inference(cnf_transformation,[],[f121]) ).
fof(f272,plain,
! [X2,X0,X1] :
( subnet(subnetstr_of_element(X0,X1,X2),X0,X1)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0)
| ~ element(X2,the_carrier(X1)) ),
inference(cnf_transformation,[],[f123]) ).
fof(f275,plain,
! [X0] :
( ~ rel_str(X0)
| one_sorted_str(X0) ),
inference(cnf_transformation,[],[f125]) ).
fof(f276,plain,
! [X0,X1] :
( ~ net_str(X1,X0)
| rel_str(X1)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f126]) ).
fof(f277,plain,
! [X2,X0,X1] :
( ~ netstr_induced_subset(X2,X0,X1)
| element(X2,powerset(the_carrier(X0)))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ net_str(X1,X0) ),
inference(cnf_transformation,[],[f128]) ).
fof(f279,plain,
! [X2,X0,X1] :
( ~ subnet(X2,X0,X1)
| net_str(X2,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0) ),
inference(cnf_transformation,[],[f131]) ).
fof(f282,plain,
! [X2,X0,X1] :
( ~ subnet(X2,X0,X1)
| ~ empty_carrier(X2)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0) ),
inference(cnf_transformation,[],[f131]) ).
fof(f284,plain,
! [X0,X1] :
( relation_of2_as_subset(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(cnf_transformation,[],[f134]) ).
fof(f285,plain,
! [X0,X1] :
( quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(cnf_transformation,[],[f134]) ).
fof(f286,plain,
! [X0,X1] :
( function(the_mapping(X0,X1))
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(cnf_transformation,[],[f134]) ).
fof(f301,plain,
! [X0,X1] :
( quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ net_str(X1,X0) ),
inference(cnf_transformation,[],[f145]) ).
fof(f302,plain,
! [X0,X1] :
( function(the_mapping(X0,X1))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ net_str(X1,X0) ),
inference(cnf_transformation,[],[f145]) ).
fof(f305,plain,
! [X0] :
( ~ empty(the_carrier(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f147]) ).
fof(f314,plain,
empty(empty_set),
inference(cnf_transformation,[],[f53]) ).
fof(f361,plain,
! [X2,X3,X0,X1] :
( ~ quasi_total(X2,the_carrier(X0),the_carrier(X1))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ function(X2)
| apply_on_structs(X0,X1,X2,X3) = apply(X2,X3)
| ~ relation_of2(X2,the_carrier(X0),the_carrier(X1))
| ~ element(X3,the_carrier(X0)) ),
inference(cnf_transformation,[],[f172]) ).
fof(f362,plain,
! [X2,X3,X0,X1] :
( ~ relation_of2(X2,X0,X1)
| ~ function(X2)
| partfun_dom_restriction(X0,X1,X2,X3) = relation_dom_restriction(X2,X3) ),
inference(cnf_transformation,[],[f174]) ).
fof(f363,plain,
! [X2,X0,X1] :
( ~ relation_of2(X2,X0,X1)
| relation_rng_as_subset(X0,X1,X2) = relation_rng(X2) ),
inference(cnf_transformation,[],[f175]) ).
fof(f364,plain,
! [X2,X0,X1] :
( ~ element(X2,the_carrier(X1))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0)
| netstr_restr_to_element(X0,X1,X2) = subnetstr_of_element(X0,X1,X2) ),
inference(cnf_transformation,[],[f177]) ).
fof(f365,plain,
! [X2,X0,X1] :
( ~ relation_of2_as_subset(X2,X0,X1)
| relation_of2(X2,X0,X1) ),
inference(cnf_transformation,[],[f231]) ).
fof(f368,plain,
! [X2,X3,X0,X1,X4] :
( apply_netmap(X0,X1,X3) = apply_netmap(X0,netstr_restr_to_element(X0,X1,X2),X4)
| X3 != X4
| ~ element(X4,the_carrier(netstr_restr_to_element(X0,X1,X2)))
| ~ element(X3,the_carrier(X1))
| ~ element(X2,the_carrier(X1))
| empty_carrier(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f179]) ).
fof(f369,plain,
! [X0,X1] :
( ~ in(X0,X1)
| element(X0,X1) ),
inference(cnf_transformation,[],[f180]) ).
fof(f370,plain,
! [X0,X1] :
( ~ element(X0,X1)
| in(X0,X1)
| empty(X1) ),
inference(cnf_transformation,[],[f182]) ).
fof(f375,plain,
! [X2,X3,X0,X1] :
( ~ relation_of2_as_subset(X3,X0,X1)
| in(apply(X3,X2),relation_rng(X3))
| ~ in(X2,X0)
| ~ function(X3)
| ~ quasi_total(X3,X0,X1)
| empty_set = X1 ),
inference(cnf_transformation,[],[f189]) ).
fof(f378,plain,
one_sorted_str(sK30),
inference(cnf_transformation,[],[f232]) ).
fof(f379,plain,
~ empty_carrier(sK30),
inference(cnf_transformation,[],[f232]) ).
fof(f380,plain,
net_str(sK31,sK30),
inference(cnf_transformation,[],[f232]) ).
fof(f381,plain,
directed_relstr(sK31),
inference(cnf_transformation,[],[f232]) ).
fof(f382,plain,
transitive_relstr(sK31),
inference(cnf_transformation,[],[f232]) ).
fof(f383,plain,
~ empty_carrier(sK31),
inference(cnf_transformation,[],[f232]) ).
fof(f384,plain,
netstr_induced_subset(sK32,sK30,sK31),
inference(cnf_transformation,[],[f232]) ).
fof(f385,plain,
~ is_eventually_in(sK30,sK31,sK32),
inference(cnf_transformation,[],[f232]) ).
fof(f387,plain,
! [X2,X3,X0] :
( ~ sP1(X0,netstr_restr_to_element(X0,X3,X2),X2,X3)
| sP0(X3,X2,netstr_restr_to_element(X0,X3,X2),X0) ),
inference(equality_resolution,[],[f247]) ).
fof(f389,plain,
! [X2,X3,X0,X1,X8] :
( ~ sP0(X0,X1,X2,X3)
| ~ element(X8,the_carrier(X0))
| ~ related(X0,X1,X8)
| in(X8,the_carrier(X2)) ),
inference(equality_resolution,[],[f254]) ).
fof(f390,plain,
! [X2,X0,X1,X4] :
( ~ element(X4,the_carrier(netstr_restr_to_element(X0,X1,X2)))
| apply_netmap(X0,X1,X4) = apply_netmap(X0,netstr_restr_to_element(X0,X1,X2),X4)
| ~ element(X4,the_carrier(X1))
| ~ element(X2,the_carrier(X1))
| empty_carrier(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(equality_resolution,[],[f368]) ).
fof(f391,plain,
! [X2,X0,X1] :
( ~ netstr_induced_subset(X2,X0,X1)
| relation_rng_as_subset(the_carrier(netstr_restr_to_element(X0,X1,sK4(X0,X1,X2))),the_carrier(X0),the_mapping(X0,netstr_restr_to_element(X0,X1,sK4(X0,X1,X2)))) = X2
| empty_carrier(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(forward_subsumption_resolution,[],[f244,f277]) ).
fof(f392,plain,
! [X2,X0,X1] :
( element(sK4(X0,X1,X2),the_carrier(X1))
| ~ netstr_induced_subset(X2,X0,X1)
| empty_carrier(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(forward_subsumption_resolution,[],[f245,f277]) ).
fof(f398,plain,
( sK32 = relation_rng_as_subset(the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(sK30),the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))))
| empty_carrier(sK31)
| ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30) ),
inference(resolution,[],[f391,f384]) ).
fof(f399,plain,
( sK32 = relation_rng_as_subset(the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(sK30),the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))))
| ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30) ),
inference(forward_subsumption_resolution,[],[f398,f383]) ).
fof(f400,plain,
( sK32 = relation_rng_as_subset(the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(sK30),the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))))
| empty_carrier(sK30)
| ~ one_sorted_str(sK30) ),
inference(forward_subsumption_resolution,[],[f399,f380]) ).
fof(f401,plain,
( sK32 = relation_rng_as_subset(the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(sK30),the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))))
| ~ one_sorted_str(sK30) ),
inference(forward_subsumption_resolution,[],[f400,f379]) ).
fof(f402,plain,
sK32 = relation_rng_as_subset(the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(sK30),the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))),
inference(forward_subsumption_resolution,[],[f401,f378]) ).
fof(f405,plain,
! [X2,X0,X1] :
( sP0(X0,X1,netstr_restr_to_element(X2,X0,X1),X2)
| ~ strict_net_str(netstr_restr_to_element(X2,X0,X1),X2)
| ~ net_str(netstr_restr_to_element(X2,X0,X1),X2)
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ net_str(X0,X2)
| empty_carrier(X2)
| ~ one_sorted_str(X2) ),
inference(resolution,[],[f387,f259]) ).
fof(f406,plain,
! [X2,X0,X1] :
( sP0(X0,X1,netstr_restr_to_element(X2,X0,X1),X2)
| ~ net_str(netstr_restr_to_element(X2,X0,X1),X2)
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ net_str(X0,X2)
| empty_carrier(X2)
| ~ one_sorted_str(X2) ),
inference(forward_subsumption_resolution,[],[f405,f271]) ).
fof(f407,plain,
! [X2,X0,X1] :
( sP0(X0,X1,netstr_restr_to_element(X2,X0,X1),X2)
| ~ element(X1,the_carrier(X0))
| empty_carrier(X0)
| ~ net_str(X0,X2)
| empty_carrier(X2)
| ~ one_sorted_str(X2) ),
inference(forward_subsumption_resolution,[],[f406,f270]) ).
fof(f422,plain,
! [X2,X3,X0,X1] :
( empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0)
| netstr_restr_to_element(X0,X1,sK4(X2,X1,X3)) = subnetstr_of_element(X0,X1,sK4(X2,X1,X3))
| ~ netstr_induced_subset(X3,X2,X1)
| empty_carrier(X1)
| ~ net_str(X1,X2)
| empty_carrier(X2)
| ~ one_sorted_str(X2) ),
inference(resolution,[],[f364,f392]) ).
fof(f423,plain,
! [X2,X3,X0,X1] :
( ~ netstr_induced_subset(X3,X2,X1)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0)
| netstr_restr_to_element(X0,X1,sK4(X2,X1,X3)) = subnetstr_of_element(X0,X1,sK4(X2,X1,X3))
| empty_carrier(X0)
| ~ net_str(X1,X2)
| empty_carrier(X2)
| ~ one_sorted_str(X2) ),
inference(duplicate_literal_removal,[],[f422]) ).
fof(f427,plain,
! [X2,X3,X0,X1] :
( in(X3,the_carrier(netstr_restr_to_element(X2,X1,X0)))
| empty_carrier(X1)
| ~ net_str(X1,X2)
| empty_carrier(X2)
| ~ one_sorted_str(X2)
| ~ element(X3,the_carrier(X1))
| ~ related(X1,X0,X3)
| ~ element(X0,the_carrier(X1)) ),
inference(resolution,[],[f407,f389]) ).
fof(f430,plain,
! [X0,X1] :
( relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(resolution,[],[f284,f365]) ).
fof(f509,plain,
! [X2,X3,X0,X1] :
( element(X2,the_carrier(netstr_restr_to_element(X1,X0,X3)))
| ~ net_str(X0,X1)
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ element(X2,the_carrier(X0))
| ~ related(X0,X3,X2)
| ~ element(X3,the_carrier(X0))
| empty_carrier(X0) ),
inference(resolution,[],[f427,f369]) ).
fof(f512,plain,
! [X0,X1] :
( ~ net_str(X0,X1)
| relation_rng_as_subset(the_carrier(X0),the_carrier(X1),the_mapping(X1,X0)) = relation_rng(the_mapping(X1,X0))
| ~ one_sorted_str(X1) ),
inference(resolution,[],[f363,f430]) ).
fof(f523,plain,
! [X0] :
( ~ one_sorted_str(X0)
| empty_carrier(sK31)
| ~ transitive_relstr(sK31)
| ~ directed_relstr(sK31)
| ~ net_str(sK31,X0)
| netstr_restr_to_element(X0,sK31,sK4(sK30,sK31,sK32)) = subnetstr_of_element(X0,sK31,sK4(sK30,sK31,sK32))
| empty_carrier(X0)
| ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30) ),
inference(resolution,[],[f423,f384]) ).
fof(f524,plain,
! [X0] :
( ~ one_sorted_str(X0)
| ~ transitive_relstr(sK31)
| ~ directed_relstr(sK31)
| ~ net_str(sK31,X0)
| netstr_restr_to_element(X0,sK31,sK4(sK30,sK31,sK32)) = subnetstr_of_element(X0,sK31,sK4(sK30,sK31,sK32))
| empty_carrier(X0)
| ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30) ),
inference(forward_subsumption_resolution,[],[f523,f383]) ).
fof(f525,plain,
! [X0] :
( ~ one_sorted_str(X0)
| ~ directed_relstr(sK31)
| ~ net_str(sK31,X0)
| netstr_restr_to_element(X0,sK31,sK4(sK30,sK31,sK32)) = subnetstr_of_element(X0,sK31,sK4(sK30,sK31,sK32))
| empty_carrier(X0)
| ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30) ),
inference(forward_subsumption_resolution,[],[f524,f382]) ).
fof(f526,plain,
! [X0] :
( ~ one_sorted_str(X0)
| ~ net_str(sK31,X0)
| netstr_restr_to_element(X0,sK31,sK4(sK30,sK31,sK32)) = subnetstr_of_element(X0,sK31,sK4(sK30,sK31,sK32))
| empty_carrier(X0)
| ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30) ),
inference(forward_subsumption_resolution,[],[f525,f381]) ).
fof(f527,plain,
! [X0] :
( ~ one_sorted_str(X0)
| ~ net_str(sK31,X0)
| netstr_restr_to_element(X0,sK31,sK4(sK30,sK31,sK32)) = subnetstr_of_element(X0,sK31,sK4(sK30,sK31,sK32))
| empty_carrier(X0)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30) ),
inference(forward_subsumption_resolution,[],[f526,f380]) ).
fof(f528,plain,
! [X0] :
( ~ one_sorted_str(X0)
| ~ net_str(sK31,X0)
| netstr_restr_to_element(X0,sK31,sK4(sK30,sK31,sK32)) = subnetstr_of_element(X0,sK31,sK4(sK30,sK31,sK32))
| empty_carrier(X0)
| ~ one_sorted_str(sK30) ),
inference(forward_subsumption_resolution,[],[f527,f379]) ).
fof(f529,plain,
! [X0] :
( ~ net_str(sK31,X0)
| ~ one_sorted_str(X0)
| netstr_restr_to_element(X0,sK31,sK4(sK30,sK31,sK32)) = subnetstr_of_element(X0,sK31,sK4(sK30,sK31,sK32))
| empty_carrier(X0) ),
inference(forward_subsumption_resolution,[],[f528,f378]) ).
fof(f530,plain,
( ~ one_sorted_str(sK30)
| netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)) = subnetstr_of_element(sK30,sK31,sK4(sK30,sK31,sK32))
| empty_carrier(sK30) ),
inference(resolution,[],[f529,f380]) ).
fof(f531,plain,
( netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)) = subnetstr_of_element(sK30,sK31,sK4(sK30,sK31,sK32))
| empty_carrier(sK30) ),
inference(forward_subsumption_resolution,[],[f530,f378]) ).
fof(f532,plain,
netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)) = subnetstr_of_element(sK30,sK31,sK4(sK30,sK31,sK32)),
inference(forward_subsumption_resolution,[],[f531,f379]) ).
fof(f633,definition,
( spl33_9
<=> element(sK4(sK30,sK31,sK32),the_carrier(sK31)) ),
introduced(definition,[new_symbols(definition,[spl33_9])],[avatar_definition]) ).
fof(f634,plain,
( element(sK4(sK30,sK31,sK32),the_carrier(sK31))
| ~ spl33_9 ),
inference(avatar_component_clause,[],[f633]) ).
fof(f635,plain,
( ~ element(sK4(sK30,sK31,sK32),the_carrier(sK31))
| spl33_9 ),
inference(avatar_component_clause,[],[f633]) ).
fof(f637,definition,
( spl33_10
<=> relation_of2(the_mapping(sK30,sK31),the_carrier(sK31),the_carrier(sK30)) ),
introduced(definition,[new_symbols(definition,[spl33_10])],[avatar_definition]) ).
fof(f638,plain,
( relation_of2(the_mapping(sK30,sK31),the_carrier(sK31),the_carrier(sK30))
| ~ spl33_10 ),
inference(avatar_component_clause,[],[f637]) ).
fof(f639,plain,
( ~ relation_of2(the_mapping(sK30,sK31),the_carrier(sK31),the_carrier(sK30))
| spl33_10 ),
inference(avatar_component_clause,[],[f637]) ).
fof(f645,definition,
( spl33_12
<=> function(the_mapping(sK30,sK31)) ),
introduced(definition,[new_symbols(definition,[spl33_12])],[avatar_definition]) ).
fof(f646,plain,
( function(the_mapping(sK30,sK31))
| ~ spl33_12 ),
inference(avatar_component_clause,[],[f645]) ).
fof(f647,plain,
( ~ function(the_mapping(sK30,sK31))
| spl33_12 ),
inference(avatar_component_clause,[],[f645]) ).
fof(f653,plain,
( ~ netstr_induced_subset(sK32,sK30,sK31)
| empty_carrier(sK31)
| ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| spl33_9 ),
inference(resolution,[],[f635,f392]) ).
fof(f654,plain,
( empty_carrier(sK31)
| ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| spl33_9 ),
inference(forward_subsumption_resolution,[],[f653,f384]) ).
fof(f655,plain,
( ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| spl33_9 ),
inference(forward_subsumption_resolution,[],[f654,f383]) ).
fof(f656,plain,
( empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| spl33_9 ),
inference(forward_subsumption_resolution,[],[f655,f380]) ).
fof(f657,plain,
( ~ one_sorted_str(sK30)
| spl33_9 ),
inference(forward_subsumption_resolution,[],[f656,f379]) ).
fof(f658,plain,
( $false
| spl33_9 ),
inference(forward_subsumption_resolution,[],[f657,f378]) ).
fof(f659,plain,
spl33_9,
inference(avatar_contradiction_clause,[],[f658]) ).
fof(f688,plain,
( ~ net_str(sK31,sK30)
| ~ one_sorted_str(sK30)
| spl33_10 ),
inference(resolution,[],[f639,f430]) ).
fof(f689,plain,
( ~ one_sorted_str(sK30)
| spl33_10 ),
inference(forward_subsumption_resolution,[],[f688,f380]) ).
fof(f690,plain,
( $false
| spl33_10 ),
inference(forward_subsumption_resolution,[],[f689,f378]) ).
fof(f691,plain,
spl33_10,
inference(avatar_contradiction_clause,[],[f690]) ).
fof(f703,plain,
( empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| empty_carrier(sK31)
| ~ net_str(sK31,sK30)
| spl33_12 ),
inference(resolution,[],[f647,f302]) ).
fof(f704,plain,
( ~ one_sorted_str(sK30)
| empty_carrier(sK31)
| ~ net_str(sK31,sK30)
| spl33_12 ),
inference(forward_subsumption_resolution,[],[f703,f379]) ).
fof(f706,plain,
( empty_carrier(sK31)
| ~ net_str(sK31,sK30)
| spl33_12 ),
inference(forward_subsumption_resolution,[],[f704,f378]) ).
fof(f709,plain,
( ~ net_str(sK31,sK30)
| spl33_12 ),
inference(forward_subsumption_resolution,[],[f706,f383]) ).
fof(f710,plain,
( $false
| spl33_12 ),
inference(forward_subsumption_resolution,[],[f709,f380]) ).
fof(f711,plain,
spl33_12,
inference(avatar_contradiction_clause,[],[f710]) ).
fof(f713,plain,
( ! [X0] :
( ~ function(the_mapping(sK30,sK31))
| partfun_dom_restriction(the_carrier(sK31),the_carrier(sK30),the_mapping(sK30,sK31),X0) = relation_dom_restriction(the_mapping(sK30,sK31),X0) )
| ~ spl33_10 ),
inference(resolution,[],[f638,f362]) ).
fof(f715,plain,
( ! [X0] : partfun_dom_restriction(the_carrier(sK31),the_carrier(sK30),the_mapping(sK30,sK31),X0) = relation_dom_restriction(the_mapping(sK30,sK31),X0)
| ~ spl33_10
| ~ spl33_12 ),
inference(forward_subsumption_resolution,[],[f713,f646]) ).
fof(f716,plain,
( ! [X0] :
( function(relation_dom_restriction(the_mapping(sK30,sK31),X0))
| ~ function(the_mapping(sK30,sK31))
| ~ relation_of2(the_mapping(sK30,sK31),the_carrier(sK31),the_carrier(sK30)) )
| ~ spl33_10
| ~ spl33_12 ),
inference(superposition,[],[f266,f715]) ).
fof(f717,plain,
( ! [X0] :
( function(relation_dom_restriction(the_mapping(sK30,sK31),X0))
| ~ relation_of2(the_mapping(sK30,sK31),the_carrier(sK31),the_carrier(sK30)) )
| ~ spl33_10
| ~ spl33_12 ),
inference(forward_subsumption_resolution,[],[f716,f646]) ).
fof(f718,plain,
( ! [X0] : function(relation_dom_restriction(the_mapping(sK30,sK31),X0))
| ~ spl33_10
| ~ spl33_12 ),
inference(forward_subsumption_resolution,[],[f717,f638]) ).
fof(f779,plain,
! [X2,X0,X1] :
( in(apply(the_mapping(X0,X1),X2),relation_rng(the_mapping(X0,X1)))
| ~ in(X2,the_carrier(X1))
| ~ function(the_mapping(X0,X1))
| ~ quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| the_carrier(X0) = empty_set
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(resolution,[],[f375,f284]) ).
fof(f783,plain,
! [X2,X0,X1] :
( in(apply(the_mapping(X0,X1),X2),relation_rng(the_mapping(X0,X1)))
| ~ in(X2,the_carrier(X1))
| ~ quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| the_carrier(X0) = empty_set
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(forward_subsumption_resolution,[],[f779,f286]) ).
fof(f785,plain,
! [X2,X0,X1] :
( in(apply(the_mapping(X0,X1),X2),relation_rng(the_mapping(X0,X1)))
| ~ in(X2,the_carrier(X1))
| the_carrier(X0) = empty_set
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(forward_subsumption_resolution,[],[f783,f285]) ).
fof(f787,definition,
( spl33_19
<=> empty_set = the_carrier(sK30) ),
introduced(definition,[new_symbols(definition,[spl33_19])],[avatar_definition]) ).
fof(f788,plain,
( empty_set != the_carrier(sK30)
| spl33_19 ),
inference(avatar_component_clause,[],[f787]) ).
fof(f789,plain,
( empty_set = the_carrier(sK30)
| ~ spl33_19 ),
inference(avatar_component_clause,[],[f787]) ).
fof(f818,plain,
( ~ empty(empty_set)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ spl33_19 ),
inference(superposition,[],[f305,f789]) ).
fof(f835,plain,
( empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ spl33_19 ),
inference(forward_subsumption_resolution,[],[f818,f314]) ).
fof(f855,plain,
( ~ one_sorted_str(sK30)
| ~ spl33_19 ),
inference(forward_subsumption_resolution,[],[f835,f379]) ).
fof(f859,plain,
( $false
| ~ spl33_19 ),
inference(forward_subsumption_resolution,[],[f855,f378]) ).
fof(f860,plain,
~ spl33_19,
inference(avatar_contradiction_clause,[],[f859]) ).
fof(f879,plain,
! [X2,X0,X1] :
( ~ element(X2,the_carrier(X1))
| the_mapping(X0,netstr_restr_to_element(X0,X1,X2)) = partfun_dom_restriction(the_carrier(X1),the_carrier(X0),the_mapping(X0,X1),the_carrier(netstr_restr_to_element(X0,X1,X2)))
| empty_carrier(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(resolution,[],[f249,f407]) ).
fof(f888,plain,
( ! [X0] :
( the_mapping(X0,netstr_restr_to_element(X0,sK31,sK4(sK30,sK31,sK32))) = partfun_dom_restriction(the_carrier(sK31),the_carrier(X0),the_mapping(X0,sK31),the_carrier(netstr_restr_to_element(X0,sK31,sK4(sK30,sK31,sK32))))
| empty_carrier(sK31)
| ~ net_str(sK31,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0) )
| ~ spl33_9 ),
inference(resolution,[],[f879,f634]) ).
fof(f894,plain,
( ! [X0] :
( ~ net_str(sK31,X0)
| the_mapping(X0,netstr_restr_to_element(X0,sK31,sK4(sK30,sK31,sK32))) = partfun_dom_restriction(the_carrier(sK31),the_carrier(X0),the_mapping(X0,sK31),the_carrier(netstr_restr_to_element(X0,sK31,sK4(sK30,sK31,sK32))))
| empty_carrier(X0)
| ~ one_sorted_str(X0) )
| ~ spl33_9 ),
inference(forward_subsumption_resolution,[],[f888,f383]) ).
fof(f895,plain,
( the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))) = partfun_dom_restriction(the_carrier(sK31),the_carrier(sK30),the_mapping(sK30,sK31),the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))))
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ spl33_9 ),
inference(resolution,[],[f894,f380]) ).
fof(f896,plain,
( the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))) = partfun_dom_restriction(the_carrier(sK31),the_carrier(sK30),the_mapping(sK30,sK31),the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))))
| ~ one_sorted_str(sK30)
| ~ spl33_9 ),
inference(forward_subsumption_resolution,[],[f895,f379]) ).
fof(f897,plain,
( the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))) = partfun_dom_restriction(the_carrier(sK31),the_carrier(sK30),the_mapping(sK30,sK31),the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))))
| ~ spl33_9 ),
inference(forward_subsumption_resolution,[],[f896,f378]) ).
fof(f898,plain,
( the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))) = relation_dom_restriction(the_mapping(sK30,sK31),the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))))
| ~ spl33_9
| ~ spl33_10
| ~ spl33_12 ),
inference(forward_demodulation,[],[f897,f715]) ).
fof(f922,plain,
( function(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))))
| ~ spl33_9
| ~ spl33_10
| ~ spl33_12 ),
inference(superposition,[],[f718,f898]) ).
fof(f974,plain,
( subnet(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,sK31)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| empty_carrier(sK31)
| ~ transitive_relstr(sK31)
| ~ directed_relstr(sK31)
| ~ net_str(sK31,sK30)
| ~ element(sK4(sK30,sK31,sK32),the_carrier(sK31)) ),
inference(superposition,[],[f272,f532]) ).
fof(f979,plain,
( subnet(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,sK31)
| ~ one_sorted_str(sK30)
| empty_carrier(sK31)
| ~ transitive_relstr(sK31)
| ~ directed_relstr(sK31)
| ~ net_str(sK31,sK30)
| ~ element(sK4(sK30,sK31,sK32),the_carrier(sK31)) ),
inference(forward_subsumption_resolution,[],[f974,f379]) ).
fof(f980,plain,
( subnet(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,sK31)
| empty_carrier(sK31)
| ~ transitive_relstr(sK31)
| ~ directed_relstr(sK31)
| ~ net_str(sK31,sK30)
| ~ element(sK4(sK30,sK31,sK32),the_carrier(sK31)) ),
inference(forward_subsumption_resolution,[],[f979,f378]) ).
fof(f981,plain,
( subnet(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,sK31)
| ~ transitive_relstr(sK31)
| ~ directed_relstr(sK31)
| ~ net_str(sK31,sK30)
| ~ element(sK4(sK30,sK31,sK32),the_carrier(sK31)) ),
inference(forward_subsumption_resolution,[],[f980,f383]) ).
fof(f982,plain,
( subnet(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,sK31)
| ~ directed_relstr(sK31)
| ~ net_str(sK31,sK30)
| ~ element(sK4(sK30,sK31,sK32),the_carrier(sK31)) ),
inference(forward_subsumption_resolution,[],[f981,f382]) ).
fof(f983,plain,
( subnet(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,sK31)
| ~ net_str(sK31,sK30)
| ~ element(sK4(sK30,sK31,sK32),the_carrier(sK31)) ),
inference(forward_subsumption_resolution,[],[f982,f381]) ).
fof(f984,plain,
( subnet(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,sK31)
| ~ element(sK4(sK30,sK31,sK32),the_carrier(sK31)) ),
inference(forward_subsumption_resolution,[],[f983,f380]) ).
fof(f985,plain,
( subnet(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,sK31)
| ~ spl33_9 ),
inference(forward_subsumption_resolution,[],[f984,f634]) ).
fof(f986,plain,
( net_str(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| empty_carrier(sK31)
| ~ transitive_relstr(sK31)
| ~ directed_relstr(sK31)
| ~ net_str(sK31,sK30)
| ~ spl33_9 ),
inference(resolution,[],[f985,f279]) ).
fof(f989,plain,
( ~ empty_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| empty_carrier(sK31)
| ~ transitive_relstr(sK31)
| ~ directed_relstr(sK31)
| ~ net_str(sK31,sK30)
| ~ spl33_9 ),
inference(resolution,[],[f985,f282]) ).
fof(f990,plain,
( ~ empty_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))
| ~ one_sorted_str(sK30)
| empty_carrier(sK31)
| ~ transitive_relstr(sK31)
| ~ directed_relstr(sK31)
| ~ net_str(sK31,sK30)
| ~ spl33_9 ),
inference(forward_subsumption_resolution,[],[f989,f379]) ).
fof(f993,plain,
( net_str(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30)
| ~ one_sorted_str(sK30)
| empty_carrier(sK31)
| ~ transitive_relstr(sK31)
| ~ directed_relstr(sK31)
| ~ net_str(sK31,sK30)
| ~ spl33_9 ),
inference(forward_subsumption_resolution,[],[f986,f379]) ).
fof(f994,plain,
( ~ empty_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))
| empty_carrier(sK31)
| ~ transitive_relstr(sK31)
| ~ directed_relstr(sK31)
| ~ net_str(sK31,sK30)
| ~ spl33_9 ),
inference(forward_subsumption_resolution,[],[f990,f378]) ).
fof(f997,plain,
( net_str(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30)
| empty_carrier(sK31)
| ~ transitive_relstr(sK31)
| ~ directed_relstr(sK31)
| ~ net_str(sK31,sK30)
| ~ spl33_9 ),
inference(forward_subsumption_resolution,[],[f993,f378]) ).
fof(f998,plain,
( ~ empty_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))
| ~ transitive_relstr(sK31)
| ~ directed_relstr(sK31)
| ~ net_str(sK31,sK30)
| ~ spl33_9 ),
inference(forward_subsumption_resolution,[],[f994,f383]) ).
fof(f1001,plain,
( net_str(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30)
| ~ transitive_relstr(sK31)
| ~ directed_relstr(sK31)
| ~ net_str(sK31,sK30)
| ~ spl33_9 ),
inference(forward_subsumption_resolution,[],[f997,f383]) ).
fof(f1002,plain,
( ~ empty_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))
| ~ directed_relstr(sK31)
| ~ net_str(sK31,sK30)
| ~ spl33_9 ),
inference(forward_subsumption_resolution,[],[f998,f382]) ).
fof(f1005,plain,
( net_str(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30)
| ~ directed_relstr(sK31)
| ~ net_str(sK31,sK30)
| ~ spl33_9 ),
inference(forward_subsumption_resolution,[],[f1001,f382]) ).
fof(f1006,plain,
( ~ empty_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))
| ~ net_str(sK31,sK30)
| ~ spl33_9 ),
inference(forward_subsumption_resolution,[],[f1002,f381]) ).
fof(f1009,plain,
( net_str(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30)
| ~ net_str(sK31,sK30)
| ~ spl33_9 ),
inference(forward_subsumption_resolution,[],[f1005,f381]) ).
fof(f1010,plain,
( ~ empty_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))
| ~ spl33_9 ),
inference(forward_subsumption_resolution,[],[f1006,f380]) ).
fof(f1013,plain,
( net_str(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30)
| ~ spl33_9 ),
inference(forward_subsumption_resolution,[],[f1009,f380]) ).
fof(f1016,plain,
( relation_rng_as_subset(the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(sK30),the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))) = relation_rng(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))))
| ~ one_sorted_str(sK30)
| ~ spl33_9 ),
inference(resolution,[],[f1013,f512]) ).
fof(f1017,plain,
( rel_str(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))
| ~ one_sorted_str(sK30)
| ~ spl33_9 ),
inference(resolution,[],[f1013,f276]) ).
fof(f1018,plain,
( rel_str(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))
| ~ spl33_9 ),
inference(forward_subsumption_resolution,[],[f1017,f378]) ).
fof(f1019,plain,
( relation_rng_as_subset(the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(sK30),the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))) = relation_rng(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))))
| ~ spl33_9 ),
inference(forward_subsumption_resolution,[],[f1016,f378]) ).
fof(f1022,plain,
( sK32 = relation_rng(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))))
| ~ spl33_9 ),
inference(forward_demodulation,[],[f1019,f402]) ).
fof(f1026,plain,
( one_sorted_str(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))
| ~ spl33_9 ),
inference(resolution,[],[f1018,f275]) ).
fof(f1036,plain,
( ! [X0] :
( in(apply(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0),sK32)
| ~ in(X0,the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))))
| empty_set = the_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ net_str(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30) )
| ~ spl33_9 ),
inference(superposition,[],[f785,f1022]) ).
fof(f1037,plain,
( ! [X0] :
( in(apply(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0),sK32)
| ~ in(X0,the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))))
| ~ one_sorted_str(sK30)
| ~ net_str(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30) )
| ~ spl33_9
| spl33_19 ),
inference(forward_subsumption_resolution,[],[f1036,f788]) ).
fof(f1038,plain,
( ! [X0] :
( in(apply(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0),sK32)
| ~ in(X0,the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))))
| ~ net_str(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30) )
| ~ spl33_9
| spl33_19 ),
inference(forward_subsumption_resolution,[],[f1037,f378]) ).
fof(f1039,plain,
( ! [X0] :
( in(apply(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0),sK32)
| ~ in(X0,the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))) )
| ~ spl33_9
| spl33_19 ),
inference(forward_subsumption_resolution,[],[f1038,f1013]) ).
fof(f1157,definition,
( spl33_27
<=> element(sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)),the_carrier(sK31)) ),
introduced(definition,[new_symbols(definition,[spl33_27])],[avatar_definition]) ).
fof(f1158,plain,
( element(sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)),the_carrier(sK31))
| ~ spl33_27 ),
inference(avatar_component_clause,[],[f1157]) ).
fof(f1159,plain,
( ~ element(sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)),the_carrier(sK31))
| spl33_27 ),
inference(avatar_component_clause,[],[f1157]) ).
fof(f1165,plain,
( ~ element(sK4(sK30,sK31,sK32),the_carrier(sK31))
| is_eventually_in(sK30,sK31,sK32)
| empty_carrier(sK31)
| ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| spl33_27 ),
inference(resolution,[],[f1159,f241]) ).
fof(f1166,plain,
( is_eventually_in(sK30,sK31,sK32)
| empty_carrier(sK31)
| ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ spl33_9
| spl33_27 ),
inference(forward_subsumption_resolution,[],[f1165,f634]) ).
fof(f1167,plain,
( empty_carrier(sK31)
| ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ spl33_9
| spl33_27 ),
inference(forward_subsumption_resolution,[],[f1166,f385]) ).
fof(f1168,plain,
( ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ spl33_9
| spl33_27 ),
inference(forward_subsumption_resolution,[],[f1167,f383]) ).
fof(f1169,plain,
( empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ spl33_9
| spl33_27 ),
inference(forward_subsumption_resolution,[],[f1168,f380]) ).
fof(f1170,plain,
( ~ one_sorted_str(sK30)
| ~ spl33_9
| spl33_27 ),
inference(forward_subsumption_resolution,[],[f1169,f379]) ).
fof(f1171,plain,
( $false
| ~ spl33_9
| spl33_27 ),
inference(forward_subsumption_resolution,[],[f1170,f378]) ).
fof(f1172,plain,
( ~ spl33_9
| spl33_27 ),
inference(avatar_contradiction_clause,[],[f1171]) ).
fof(f1764,definition,
( spl33_53
<=> relation_of2(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(sK30)) ),
introduced(definition,[new_symbols(definition,[spl33_53])],[avatar_definition]) ).
fof(f1765,plain,
( relation_of2(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(sK30))
| ~ spl33_53 ),
inference(avatar_component_clause,[],[f1764]) ).
fof(f1766,plain,
( ~ relation_of2(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(sK30))
| spl33_53 ),
inference(avatar_component_clause,[],[f1764]) ).
fof(f1768,definition,
( spl33_54
<=> quasi_total(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(sK30)) ),
introduced(definition,[new_symbols(definition,[spl33_54])],[avatar_definition]) ).
fof(f1769,plain,
( quasi_total(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(sK30))
| ~ spl33_54 ),
inference(avatar_component_clause,[],[f1768]) ).
fof(f1770,plain,
( ~ quasi_total(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(sK30))
| spl33_54 ),
inference(avatar_component_clause,[],[f1768]) ).
fof(f1776,plain,
( ~ net_str(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30)
| ~ one_sorted_str(sK30)
| spl33_53 ),
inference(resolution,[],[f1766,f430]) ).
fof(f1777,plain,
( ~ one_sorted_str(sK30)
| ~ spl33_9
| spl33_53 ),
inference(forward_subsumption_resolution,[],[f1776,f1013]) ).
fof(f1778,plain,
( $false
| ~ spl33_9
| spl33_53 ),
inference(forward_subsumption_resolution,[],[f1777,f378]) ).
fof(f1779,plain,
( ~ spl33_9
| spl33_53 ),
inference(avatar_contradiction_clause,[],[f1778]) ).
fof(f1785,plain,
( empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| empty_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))
| ~ net_str(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30)
| spl33_54 ),
inference(resolution,[],[f1770,f301]) ).
fof(f1786,plain,
( ~ one_sorted_str(sK30)
| empty_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))
| ~ net_str(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30)
| spl33_54 ),
inference(forward_subsumption_resolution,[],[f1785,f379]) ).
fof(f1788,plain,
( empty_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))
| ~ net_str(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30)
| spl33_54 ),
inference(forward_subsumption_resolution,[],[f1786,f378]) ).
fof(f1791,plain,
( ~ net_str(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30)
| ~ spl33_9
| spl33_54 ),
inference(forward_subsumption_resolution,[],[f1788,f1010]) ).
fof(f1792,plain,
( $false
| ~ spl33_9
| spl33_54 ),
inference(forward_subsumption_resolution,[],[f1791,f1013]) ).
fof(f1793,plain,
( ~ spl33_9
| spl33_54 ),
inference(avatar_contradiction_clause,[],[f1792]) ).
fof(f1794,plain,
( ! [X0] :
( empty_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))
| ~ one_sorted_str(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ function(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))))
| apply(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0) = apply_on_structs(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0)
| ~ relation_of2(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(sK30))
| ~ element(X0,the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))) )
| ~ spl33_54 ),
inference(resolution,[],[f1769,f361]) ).
fof(f1795,plain,
( ! [X0] :
( ~ one_sorted_str(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ function(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))))
| apply(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0) = apply_on_structs(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0)
| ~ relation_of2(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(sK30))
| ~ element(X0,the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))) )
| ~ spl33_9
| ~ spl33_54 ),
inference(forward_subsumption_resolution,[],[f1794,f1010]) ).
fof(f1796,plain,
( ! [X0] :
( empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ function(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))))
| apply(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0) = apply_on_structs(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0)
| ~ relation_of2(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(sK30))
| ~ element(X0,the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))) )
| ~ spl33_9
| ~ spl33_54 ),
inference(forward_subsumption_resolution,[],[f1795,f1026]) ).
fof(f1797,plain,
( ! [X0] :
( ~ one_sorted_str(sK30)
| ~ function(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))))
| apply(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0) = apply_on_structs(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0)
| ~ relation_of2(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(sK30))
| ~ element(X0,the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))) )
| ~ spl33_9
| ~ spl33_54 ),
inference(forward_subsumption_resolution,[],[f1796,f379]) ).
fof(f1798,plain,
( ! [X0] :
( ~ function(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))))
| apply(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0) = apply_on_structs(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0)
| ~ relation_of2(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(sK30))
| ~ element(X0,the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))) )
| ~ spl33_9
| ~ spl33_54 ),
inference(forward_subsumption_resolution,[],[f1797,f378]) ).
fof(f1799,plain,
( ! [X0] :
( apply(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0) = apply_on_structs(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0)
| ~ relation_of2(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),the_carrier(sK30))
| ~ element(X0,the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))) )
| ~ spl33_9
| ~ spl33_10
| ~ spl33_12
| ~ spl33_54 ),
inference(forward_subsumption_resolution,[],[f1798,f922]) ).
fof(f1800,plain,
( ! [X0] :
( ~ element(X0,the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))))
| apply(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0) = apply_on_structs(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0) )
| ~ spl33_9
| ~ spl33_10
| ~ spl33_12
| ~ spl33_53
| ~ spl33_54 ),
inference(forward_subsumption_resolution,[],[f1799,f1765]) ).
fof(f1808,plain,
( ! [X0] :
( apply(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0) = apply_on_structs(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0)
| ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ element(X0,the_carrier(sK31))
| ~ related(sK31,sK4(sK30,sK31,sK32),X0)
| ~ element(sK4(sK30,sK31,sK32),the_carrier(sK31))
| empty_carrier(sK31) )
| ~ spl33_9
| ~ spl33_10
| ~ spl33_12
| ~ spl33_53
| ~ spl33_54 ),
inference(resolution,[],[f1800,f509]) ).
fof(f1822,plain,
( ! [X0] :
( apply(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0) = apply_on_structs(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ element(X0,the_carrier(sK31))
| ~ related(sK31,sK4(sK30,sK31,sK32),X0)
| ~ element(sK4(sK30,sK31,sK32),the_carrier(sK31))
| empty_carrier(sK31) )
| ~ spl33_9
| ~ spl33_10
| ~ spl33_12
| ~ spl33_53
| ~ spl33_54 ),
inference(forward_subsumption_resolution,[],[f1808,f380]) ).
fof(f1825,plain,
( ! [X0] :
( apply(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0) = apply_on_structs(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0)
| ~ one_sorted_str(sK30)
| ~ element(X0,the_carrier(sK31))
| ~ related(sK31,sK4(sK30,sK31,sK32),X0)
| ~ element(sK4(sK30,sK31,sK32),the_carrier(sK31))
| empty_carrier(sK31) )
| ~ spl33_9
| ~ spl33_10
| ~ spl33_12
| ~ spl33_53
| ~ spl33_54 ),
inference(forward_subsumption_resolution,[],[f1822,f379]) ).
fof(f1826,plain,
( ! [X0] :
( apply(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0) = apply_on_structs(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0)
| ~ element(X0,the_carrier(sK31))
| ~ related(sK31,sK4(sK30,sK31,sK32),X0)
| ~ element(sK4(sK30,sK31,sK32),the_carrier(sK31))
| empty_carrier(sK31) )
| ~ spl33_9
| ~ spl33_10
| ~ spl33_12
| ~ spl33_53
| ~ spl33_54 ),
inference(forward_subsumption_resolution,[],[f1825,f378]) ).
fof(f1827,plain,
( ! [X0] :
( apply(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0) = apply_on_structs(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0)
| ~ element(X0,the_carrier(sK31))
| ~ related(sK31,sK4(sK30,sK31,sK32),X0)
| empty_carrier(sK31) )
| ~ spl33_9
| ~ spl33_10
| ~ spl33_12
| ~ spl33_53
| ~ spl33_54 ),
inference(forward_subsumption_resolution,[],[f1826,f634]) ).
fof(f1828,plain,
( ! [X0] :
( ~ related(sK31,sK4(sK30,sK31,sK32),X0)
| ~ element(X0,the_carrier(sK31))
| apply(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0) = apply_on_structs(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),X0) )
| ~ spl33_9
| ~ spl33_10
| ~ spl33_12
| ~ spl33_53
| ~ spl33_54 ),
inference(forward_subsumption_resolution,[],[f1827,f383]) ).
fof(f1829,plain,
( ! [X0,X1] :
( ~ element(sK2(X0,sK31,X1,sK4(sK30,sK31,sK32)),the_carrier(sK31))
| apply(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),sK2(X0,sK31,X1,sK4(sK30,sK31,sK32))) = apply_on_structs(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),sK2(X0,sK31,X1,sK4(sK30,sK31,sK32)))
| ~ element(sK4(sK30,sK31,sK32),the_carrier(sK31))
| is_eventually_in(X0,sK31,X1)
| empty_carrier(sK31)
| ~ net_str(sK31,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0) )
| ~ spl33_9
| ~ spl33_10
| ~ spl33_12
| ~ spl33_53
| ~ spl33_54 ),
inference(resolution,[],[f1828,f242]) ).
fof(f1830,plain,
( ! [X0,X1] :
( ~ element(sK2(X0,sK31,X1,sK4(sK30,sK31,sK32)),the_carrier(sK31))
| apply(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),sK2(X0,sK31,X1,sK4(sK30,sK31,sK32))) = apply_on_structs(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),sK2(X0,sK31,X1,sK4(sK30,sK31,sK32)))
| is_eventually_in(X0,sK31,X1)
| empty_carrier(sK31)
| ~ net_str(sK31,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0) )
| ~ spl33_9
| ~ spl33_10
| ~ spl33_12
| ~ spl33_53
| ~ spl33_54 ),
inference(forward_subsumption_resolution,[],[f1829,f634]) ).
fof(f1831,plain,
( ! [X0,X1] :
( ~ element(sK2(X0,sK31,X1,sK4(sK30,sK31,sK32)),the_carrier(sK31))
| apply(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),sK2(X0,sK31,X1,sK4(sK30,sK31,sK32))) = apply_on_structs(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),sK2(X0,sK31,X1,sK4(sK30,sK31,sK32)))
| is_eventually_in(X0,sK31,X1)
| ~ net_str(sK31,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0) )
| ~ spl33_9
| ~ spl33_10
| ~ spl33_12
| ~ spl33_53
| ~ spl33_54 ),
inference(forward_subsumption_resolution,[],[f1830,f383]) ).
fof(f1833,plain,
( apply(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32))) = apply_on_structs(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)))
| is_eventually_in(sK30,sK31,sK32)
| ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ spl33_9
| ~ spl33_10
| ~ spl33_12
| ~ spl33_27
| ~ spl33_53
| ~ spl33_54 ),
inference(resolution,[],[f1831,f1158]) ).
fof(f1835,plain,
( apply(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32))) = apply_on_structs(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)))
| ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ spl33_9
| ~ spl33_10
| ~ spl33_12
| ~ spl33_27
| ~ spl33_53
| ~ spl33_54 ),
inference(forward_subsumption_resolution,[],[f1833,f385]) ).
fof(f1837,plain,
( apply(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32))) = apply_on_structs(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)))
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ spl33_9
| ~ spl33_10
| ~ spl33_12
| ~ spl33_27
| ~ spl33_53
| ~ spl33_54 ),
inference(forward_subsumption_resolution,[],[f1835,f380]) ).
fof(f1839,plain,
( apply(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32))) = apply_on_structs(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)))
| ~ one_sorted_str(sK30)
| ~ spl33_9
| ~ spl33_10
| ~ spl33_12
| ~ spl33_27
| ~ spl33_53
| ~ spl33_54 ),
inference(forward_subsumption_resolution,[],[f1837,f379]) ).
fof(f1840,plain,
( apply(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32))) = apply_on_structs(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)))
| ~ spl33_9
| ~ spl33_10
| ~ spl33_12
| ~ spl33_27
| ~ spl33_53
| ~ spl33_54 ),
inference(forward_subsumption_resolution,[],[f1839,f378]) ).
fof(f1850,definition,
( spl33_56
<=> element(sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)),the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))) ),
introduced(definition,[new_symbols(definition,[spl33_56])],[avatar_definition]) ).
fof(f1851,plain,
( element(sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)),the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))))
| ~ spl33_56 ),
inference(avatar_component_clause,[],[f1850]) ).
fof(f1852,plain,
( ~ element(sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)),the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))))
| spl33_56 ),
inference(avatar_component_clause,[],[f1850]) ).
fof(f1858,plain,
( ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ element(sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)),the_carrier(sK31))
| ~ related(sK31,sK4(sK30,sK31,sK32),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)))
| ~ element(sK4(sK30,sK31,sK32),the_carrier(sK31))
| empty_carrier(sK31)
| spl33_56 ),
inference(resolution,[],[f1852,f509]) ).
fof(f1859,plain,
( empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ element(sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)),the_carrier(sK31))
| ~ related(sK31,sK4(sK30,sK31,sK32),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)))
| ~ element(sK4(sK30,sK31,sK32),the_carrier(sK31))
| empty_carrier(sK31)
| spl33_56 ),
inference(forward_subsumption_resolution,[],[f1858,f380]) ).
fof(f1860,plain,
( ~ one_sorted_str(sK30)
| ~ element(sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)),the_carrier(sK31))
| ~ related(sK31,sK4(sK30,sK31,sK32),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)))
| ~ element(sK4(sK30,sK31,sK32),the_carrier(sK31))
| empty_carrier(sK31)
| spl33_56 ),
inference(forward_subsumption_resolution,[],[f1859,f379]) ).
fof(f1861,plain,
( ~ element(sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)),the_carrier(sK31))
| ~ related(sK31,sK4(sK30,sK31,sK32),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)))
| ~ element(sK4(sK30,sK31,sK32),the_carrier(sK31))
| empty_carrier(sK31)
| spl33_56 ),
inference(forward_subsumption_resolution,[],[f1860,f378]) ).
fof(f1862,plain,
( ~ related(sK31,sK4(sK30,sK31,sK32),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)))
| ~ element(sK4(sK30,sK31,sK32),the_carrier(sK31))
| empty_carrier(sK31)
| ~ spl33_27
| spl33_56 ),
inference(forward_subsumption_resolution,[],[f1861,f1158]) ).
fof(f1863,plain,
( ~ related(sK31,sK4(sK30,sK31,sK32),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)))
| empty_carrier(sK31)
| ~ spl33_9
| ~ spl33_27
| spl33_56 ),
inference(forward_subsumption_resolution,[],[f1862,f634]) ).
fof(f1864,plain,
( ~ related(sK31,sK4(sK30,sK31,sK32),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)))
| ~ spl33_9
| ~ spl33_27
| spl33_56 ),
inference(forward_subsumption_resolution,[],[f1863,f383]) ).
fof(f1865,plain,
( ~ element(sK4(sK30,sK31,sK32),the_carrier(sK31))
| is_eventually_in(sK30,sK31,sK32)
| empty_carrier(sK31)
| ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ spl33_9
| ~ spl33_27
| spl33_56 ),
inference(resolution,[],[f1864,f242]) ).
fof(f1866,plain,
( is_eventually_in(sK30,sK31,sK32)
| empty_carrier(sK31)
| ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ spl33_9
| ~ spl33_27
| spl33_56 ),
inference(forward_subsumption_resolution,[],[f1865,f634]) ).
fof(f1867,plain,
( empty_carrier(sK31)
| ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ spl33_9
| ~ spl33_27
| spl33_56 ),
inference(forward_subsumption_resolution,[],[f1866,f385]) ).
fof(f1868,plain,
( ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ spl33_9
| ~ spl33_27
| spl33_56 ),
inference(forward_subsumption_resolution,[],[f1867,f383]) ).
fof(f1869,plain,
( empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ spl33_9
| ~ spl33_27
| spl33_56 ),
inference(forward_subsumption_resolution,[],[f1868,f380]) ).
fof(f1870,plain,
( ~ one_sorted_str(sK30)
| ~ spl33_9
| ~ spl33_27
| spl33_56 ),
inference(forward_subsumption_resolution,[],[f1869,f379]) ).
fof(f1871,plain,
( $false
| ~ spl33_9
| ~ spl33_27
| spl33_56 ),
inference(forward_subsumption_resolution,[],[f1870,f378]) ).
fof(f1872,plain,
( ~ spl33_9
| ~ spl33_27
| spl33_56 ),
inference(avatar_contradiction_clause,[],[f1871]) ).
fof(f1874,plain,
( apply_netmap(sK30,sK31,sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32))) = apply_netmap(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)))
| ~ element(sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)),the_carrier(sK31))
| ~ element(sK4(sK30,sK31,sK32),the_carrier(sK31))
| empty_carrier(sK31)
| ~ directed_relstr(sK31)
| ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ spl33_56 ),
inference(resolution,[],[f1851,f390]) ).
fof(f1875,plain,
( ! [X0] :
( apply_netmap(X0,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32))) = apply_on_structs(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),X0,the_mapping(X0,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)))
| empty_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))
| ~ net_str(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0) )
| ~ spl33_56 ),
inference(resolution,[],[f1851,f260]) ).
fof(f1886,plain,
( in(sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)),the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))))
| empty(the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))))
| ~ spl33_56 ),
inference(resolution,[],[f1851,f370]) ).
fof(f1888,definition,
( spl33_58
<=> empty(the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))) ),
introduced(definition,[new_symbols(definition,[spl33_58])],[avatar_definition]) ).
fof(f1890,plain,
( empty(the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))))
| ~ spl33_58 ),
inference(avatar_component_clause,[],[f1888]) ).
fof(f1892,definition,
( spl33_59
<=> in(sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)),the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))) ),
introduced(definition,[new_symbols(definition,[spl33_59])],[avatar_definition]) ).
fof(f1894,plain,
( in(sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)),the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))))
| ~ spl33_59 ),
inference(avatar_component_clause,[],[f1892]) ).
fof(f1895,plain,
( spl33_58
| spl33_59
| ~ spl33_56 ),
inference(avatar_split_clause,[],[f1886,f1850,f1892,f1888]) ).
fof(f1905,plain,
( ! [X0] :
( ~ net_str(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),X0)
| apply_netmap(X0,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32))) = apply_on_structs(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),X0,the_mapping(X0,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)))
| empty_carrier(X0)
| ~ one_sorted_str(X0) )
| ~ spl33_9
| ~ spl33_56 ),
inference(forward_subsumption_resolution,[],[f1875,f1010]) ).
fof(f1906,plain,
( apply_netmap(sK30,sK31,sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32))) = apply_netmap(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)))
| ~ element(sK4(sK30,sK31,sK32),the_carrier(sK31))
| empty_carrier(sK31)
| ~ directed_relstr(sK31)
| ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ spl33_27
| ~ spl33_56 ),
inference(forward_subsumption_resolution,[],[f1874,f1158]) ).
fof(f1918,plain,
( apply_netmap(sK30,sK31,sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32))) = apply_netmap(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)))
| empty_carrier(sK31)
| ~ directed_relstr(sK31)
| ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ spl33_9
| ~ spl33_27
| ~ spl33_56 ),
inference(forward_subsumption_resolution,[],[f1906,f634]) ).
fof(f1921,plain,
( apply_netmap(sK30,sK31,sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32))) = apply_netmap(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)))
| ~ directed_relstr(sK31)
| ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ spl33_9
| ~ spl33_27
| ~ spl33_56 ),
inference(forward_subsumption_resolution,[],[f1918,f383]) ).
fof(f1922,plain,
( apply_netmap(sK30,sK31,sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32))) = apply_netmap(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)))
| ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ spl33_9
| ~ spl33_27
| ~ spl33_56 ),
inference(forward_subsumption_resolution,[],[f1921,f381]) ).
fof(f1923,plain,
( apply_netmap(sK30,sK31,sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32))) = apply_netmap(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)))
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ spl33_9
| ~ spl33_27
| ~ spl33_56 ),
inference(forward_subsumption_resolution,[],[f1922,f380]) ).
fof(f1924,plain,
( apply_netmap(sK30,sK31,sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32))) = apply_netmap(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)))
| ~ one_sorted_str(sK30)
| ~ spl33_9
| ~ spl33_27
| ~ spl33_56 ),
inference(forward_subsumption_resolution,[],[f1923,f379]) ).
fof(f1925,plain,
( apply_netmap(sK30,sK31,sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32))) = apply_netmap(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)))
| ~ spl33_9
| ~ spl33_27
| ~ spl33_56 ),
inference(forward_subsumption_resolution,[],[f1924,f378]) ).
fof(f1941,plain,
( empty_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))
| ~ one_sorted_str(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))
| ~ spl33_58 ),
inference(resolution,[],[f1890,f305]) ).
fof(f1947,plain,
( ~ one_sorted_str(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)))
| ~ spl33_9
| ~ spl33_58 ),
inference(forward_subsumption_resolution,[],[f1941,f1010]) ).
fof(f1948,plain,
( $false
| ~ spl33_9
| ~ spl33_58 ),
inference(forward_subsumption_resolution,[],[f1947,f1026]) ).
fof(f1949,plain,
( ~ spl33_9
| ~ spl33_58 ),
inference(avatar_contradiction_clause,[],[f1948]) ).
fof(f3635,plain,
( apply_on_structs(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32))) = apply_netmap(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)))
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ spl33_9
| ~ spl33_56 ),
inference(resolution,[],[f1905,f1013]) ).
fof(f3637,plain,
( apply_on_structs(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32))) = apply_netmap(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)))
| ~ one_sorted_str(sK30)
| ~ spl33_9
| ~ spl33_56 ),
inference(forward_subsumption_resolution,[],[f3635,f379]) ).
fof(f3639,plain,
( apply_on_structs(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32))) = apply_netmap(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)))
| ~ spl33_9
| ~ spl33_56 ),
inference(forward_subsumption_resolution,[],[f3637,f378]) ).
fof(f3641,plain,
( apply_netmap(sK30,sK31,sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32))) = apply_on_structs(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32)),sK30,the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)))
| ~ spl33_9
| ~ spl33_27
| ~ spl33_56 ),
inference(forward_demodulation,[],[f3639,f1925]) ).
fof(f3643,plain,
( apply_netmap(sK30,sK31,sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32))) = apply(the_mapping(sK30,netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))),sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)))
| ~ spl33_9
| ~ spl33_10
| ~ spl33_12
| ~ spl33_27
| ~ spl33_53
| ~ spl33_54
| ~ spl33_56 ),
inference(forward_demodulation,[],[f3641,f1840]) ).
fof(f3649,plain,
( in(apply_netmap(sK30,sK31,sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32))),sK32)
| ~ in(sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32)),the_carrier(netstr_restr_to_element(sK30,sK31,sK4(sK30,sK31,sK32))))
| ~ spl33_9
| ~ spl33_10
| ~ spl33_12
| spl33_19
| ~ spl33_27
| ~ spl33_53
| ~ spl33_54
| ~ spl33_56 ),
inference(superposition,[],[f1039,f3643]) ).
fof(f3652,plain,
( in(apply_netmap(sK30,sK31,sK2(sK30,sK31,sK32,sK4(sK30,sK31,sK32))),sK32)
| ~ spl33_9
| ~ spl33_10
| ~ spl33_12
| spl33_19
| ~ spl33_27
| ~ spl33_53
| ~ spl33_54
| ~ spl33_56
| ~ spl33_59 ),
inference(forward_subsumption_resolution,[],[f3649,f1894]) ).
fof(f3657,plain,
( ~ element(sK4(sK30,sK31,sK32),the_carrier(sK31))
| is_eventually_in(sK30,sK31,sK32)
| empty_carrier(sK31)
| ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ spl33_9
| ~ spl33_10
| ~ spl33_12
| spl33_19
| ~ spl33_27
| ~ spl33_53
| ~ spl33_54
| ~ spl33_56
| ~ spl33_59 ),
inference(resolution,[],[f3652,f243]) ).
fof(f3664,plain,
( is_eventually_in(sK30,sK31,sK32)
| empty_carrier(sK31)
| ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ spl33_9
| ~ spl33_10
| ~ spl33_12
| spl33_19
| ~ spl33_27
| ~ spl33_53
| ~ spl33_54
| ~ spl33_56
| ~ spl33_59 ),
inference(forward_subsumption_resolution,[],[f3657,f634]) ).
fof(f3665,plain,
( empty_carrier(sK31)
| ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ spl33_9
| ~ spl33_10
| ~ spl33_12
| spl33_19
| ~ spl33_27
| ~ spl33_53
| ~ spl33_54
| ~ spl33_56
| ~ spl33_59 ),
inference(forward_subsumption_resolution,[],[f3664,f385]) ).
fof(f3666,plain,
( ~ net_str(sK31,sK30)
| empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ spl33_9
| ~ spl33_10
| ~ spl33_12
| spl33_19
| ~ spl33_27
| ~ spl33_53
| ~ spl33_54
| ~ spl33_56
| ~ spl33_59 ),
inference(forward_subsumption_resolution,[],[f3665,f383]) ).
fof(f3667,plain,
( empty_carrier(sK30)
| ~ one_sorted_str(sK30)
| ~ spl33_9
| ~ spl33_10
| ~ spl33_12
| spl33_19
| ~ spl33_27
| ~ spl33_53
| ~ spl33_54
| ~ spl33_56
| ~ spl33_59 ),
inference(forward_subsumption_resolution,[],[f3666,f380]) ).
fof(f3668,plain,
( ~ one_sorted_str(sK30)
| ~ spl33_9
| ~ spl33_10
| ~ spl33_12
| spl33_19
| ~ spl33_27
| ~ spl33_53
| ~ spl33_54
| ~ spl33_56
| ~ spl33_59 ),
inference(forward_subsumption_resolution,[],[f3667,f379]) ).
fof(f3669,plain,
( $false
| ~ spl33_9
| ~ spl33_10
| ~ spl33_12
| spl33_19
| ~ spl33_27
| ~ spl33_53
| ~ spl33_54
| ~ spl33_56
| ~ spl33_59 ),
inference(forward_subsumption_resolution,[],[f3668,f378]) ).
fof(f3670,plain,
( ~ spl33_9
| ~ spl33_10
| ~ spl33_12
| spl33_19
| ~ spl33_27
| ~ spl33_53
| ~ spl33_54
| ~ spl33_56
| ~ spl33_59 ),
inference(avatar_contradiction_clause,[],[f3669]) ).
cnf(s6,plain,
spl33_9,
inference(sat_conversion,[],[f659]) ).
cnf(s9,plain,
spl33_10,
inference(sat_conversion,[],[f691]) ).
cnf(s13,plain,
spl33_12,
inference(sat_conversion,[],[f711]) ).
cnf(s19,plain,
~ spl33_19,
inference(sat_conversion,[],[f860]) ).
cnf(s23,plain,
( ~ spl33_9
| spl33_27 ),
inference(sat_conversion,[],[f1172]) ).
cnf(s47,plain,
( ~ spl33_9
| spl33_53 ),
inference(sat_conversion,[],[f1779]) ).
cnf(s49,plain,
( ~ spl33_9
| spl33_54 ),
inference(sat_conversion,[],[f1793]) ).
cnf(s51,plain,
( ~ spl33_9
| ~ spl33_27
| spl33_56 ),
inference(sat_conversion,[],[f1872]) ).
cnf(s52,plain,
( ~ spl33_56
| spl33_58
| spl33_59 ),
inference(sat_conversion,[],[f1895]) ).
cnf(s54,plain,
( ~ spl33_9
| ~ spl33_58 ),
inference(sat_conversion,[],[f1949]) ).
cnf(s150,plain,
( ~ spl33_9
| ~ spl33_10
| ~ spl33_12
| spl33_19
| ~ spl33_27
| ~ spl33_53
| ~ spl33_54
| ~ spl33_56
| ~ spl33_59 ),
inference(sat_conversion,[],[f3670]) ).
cnf(s170,plain,
~ spl33_58,
inference(rat,[],[s54,s6]) ).
cnf(s171,plain,
spl33_54,
inference(rat,[],[s49,s6]) ).
cnf(s172,plain,
spl33_53,
inference(rat,[],[s47,s6]) ).
cnf(s178,plain,
spl33_27,
inference(rat,[],[s23,s6]) ).
cnf(s187,plain,
spl33_56,
inference(rat,[],[s51,s6,s178]) ).
cnf(s199,plain,
spl33_59,
inference(rat,[],[s52,s170,s187]) ).
cnf(s200,plain,
$false,
inference(rat,[],[s150,s178,s172,s171,s6,s9,s19,s13,s199,s187]) ).
fof(f3671,plain,
$false,
inference(avatar_sat_refutation,[],[s200]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU390+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.39 % Computer : n026.cluster.edu
% 0.12/0.39 % Model : x86_64 x86_64
% 0.12/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.39 % Memory : 8046.5625MB
% 0.12/0.39 % OS : Linux 6.8.0-71-generic
% 0.12/0.39 % CPULimit : 300
% 0.12/0.39 % WCLimit : 300
% 0.12/0.39 % DateTime : Mon Sep 28 05:06:57 UTC 2026
% 0.12/0.39 % CPUTime :
% 0.12/0.39 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.12/0.42 Running first-order theorem proving
% 0.12/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.61/2.21 % (3474001)Detected formulas, will run a generic FOF schedule.
% 9.61/2.21 % (3474010)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=38829108:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 9.61/2.21 % (3474010)Instruction limit reached!
% 9.61/2.21 % (3474010)------------------------------
% 9.61/2.21 % (3474010)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.61/2.21 % (3474010)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.61/2.21 % (3474010)CaDiCaL version: 2.1.3
% 9.61/2.21 % (3474010)Termination reason: Instruction limit
% 9.61/2.21 % (3474010)Termination phase: Saturation
% 9.61/2.21 % (3474010)Time elapsed: 0.040 s
% 9.61/2.21 % (3474010)Peak memory usage: 89 MB
% 9.61/2.21 % (3474010)Instructions burned: 122 (million)
% 9.61/2.21 % (3474006)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=2316528026:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 9.61/2.21 % (3474009)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1885425442:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 9.61/2.21 % (3474007)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=2572628041:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 9.61/2.21 % (3474008)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=173284070:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 9.61/2.21 % (3474009)Refutation not found, incomplete strategy
% 9.61/2.21 % (3474009)------------------------------
% 9.61/2.21 % (3474009)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.61/2.21 % (3474009)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.61/2.21 % (3474009)CaDiCaL version: 2.1.3
% 9.61/2.21 % (3474009)Termination reason: Refutation not found, incomplete strategy
% 9.61/2.21 % (3474009)Time elapsed: 0.003 s
% 9.61/2.21 % (3474009)Peak memory usage: 88 MB
% 9.61/2.21 % (3474009)Instructions burned: 2 (million)
% 9.61/2.21 % (3474012)dis-21_1_sil=8000:lcm=predicate:random_seed=1786270423: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)
% 9.61/2.21 % (3474011)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3530081596:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 9.61/2.21 % (3474012)Instruction limit reached!
% 9.61/2.21 % (3474012)------------------------------
% 9.61/2.21 % (3474012)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.61/2.21 % (3474012)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.61/2.21 % (3474012)CaDiCaL version: 2.1.3
% 9.61/2.21 % (3474012)Termination reason: Instruction limit
% 9.61/2.21 % (3474012)Termination phase: Saturation
% 9.61/2.21 % (3474012)Time elapsed: 0.061 s
% 9.61/2.21 % (3474012)Peak memory usage: 89 MB
% 9.61/2.21 % (3474012)Instructions burned: 131 (million)
% 9.61/2.21 % (3474014)lrs+10_1_sil=8000:sp=occurrence:random_seed=4253657176:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 9.61/2.21 % (3474011)Instruction limit reached!
% 9.61/2.21 % (3474011)------------------------------
% 9.61/2.21 % (3474011)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.61/2.21 % (3474011)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.61/2.21 % (3474011)CaDiCaL version: 2.1.3
% 9.61/2.21 % (3474011)Termination reason: Instruction limit
% 9.61/2.21 % (3474011)Termination phase: Saturation
% 9.61/2.21 % (3474011)Time elapsed: 0.099 s
% 9.61/2.21 % (3474011)Peak memory usage: 90 MB
% 9.61/2.21 % (3474011)Instructions burned: 140 (million)
% 9.61/2.21 % (3474014)Instruction limit reached!
% 9.61/2.21 % (3474014)------------------------------
% 9.61/2.21 % (3474014)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.61/2.21 % (3474014)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.61/2.21 % (3474014)CaDiCaL version: 2.1.3
% 9.61/2.21 % (3474014)Termination reason: Instruction limit
% 9.61/2.21 % (3474014)Termination phase: Saturation
% 9.61/2.21 % (3474014)Time elapsed: 0.091 s
% 9.61/2.21 % (3474014)Peak memory usage: 92 MB
% 9.61/2.21 % (3474014)Instructions burned: 286 (million)
% 9.61/2.21 % (3474021)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2487443421:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 6.25/2.50 % (3474023)lrs+1011_1_sil=32000:sp=occurrence:random_seed=3977669244:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 6.25/2.50 % (3474009)------------------------------
% 6.25/2.50 % (3474009)------------------------------
% 6.25/2.50 % (3474024)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=946541487:s2a=on:i=248:s2at=1.23:gtg=position_2996 on theBenchmark for (2996ds/248Mi)
% 6.25/2.50 % (3474021)Instruction limit reached!
% 6.25/2.50 % (3474021)------------------------------
% 6.25/2.50 % (3474021)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.25/2.50 % (3474021)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/2.50 % (3474021)CaDiCaL version: 2.1.3
% 6.25/2.50 % (3474021)Termination reason: Instruction limit
% 6.25/2.50 % (3474021)Termination phase: Saturation
% 6.25/2.50 % (3474021)Time elapsed: 0.083 s
% 6.25/2.50 % (3474021)Peak memory usage: 89 MB
% 6.25/2.50 % (3474021)Instructions burned: 157 (million)
% 6.25/2.50 % (3474024)Instruction limit reached!
% 6.25/2.50 % (3474024)------------------------------
% 6.25/2.50 % (3474024)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.25/2.50 % (3474024)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/2.50 % (3474024)CaDiCaL version: 2.1.3
% 6.25/2.50 % (3474024)Termination reason: Instruction limit
% 6.25/2.50 % (3474024)Termination phase: Saturation
% 6.25/2.50 % (3474024)Time elapsed: 0.079 s
% 6.25/2.50 % (3474024)Peak memory usage: 91 MB
% 6.25/2.50 % (3474024)Instructions burned: 249 (million)
% 6.25/2.50 % (3474027)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2120922087:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 6.25/2.50 % (3474027)Refutation not found, incomplete strategy
% 6.25/2.50 % (3474027)------------------------------
% 6.25/2.50 % (3474027)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.25/2.50 % (3474027)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/2.50 % (3474027)CaDiCaL version: 2.1.3
% 6.25/2.50 % (3474027)Termination reason: Refutation not found, incomplete strategy
% 6.25/2.50 % (3474027)Time elapsed: 0.005 s
% 6.25/2.50 % (3474027)Peak memory usage: 88 MB
% 6.25/2.50 % (3474027)Instructions burned: 7 (million)
% 6.25/2.50 % (3474029)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3982261368:i=2350_2995 on theBenchmark for (2995ds/2350Mi)
% 6.25/2.50 % (3474030)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=801943305:cts=off:i=113:fsr=off:ss=included:sgt=4_2995 on theBenchmark for (2995ds/113Mi)
% 6.25/2.50 % (3474023)Instruction limit reached!
% 6.25/2.50 % (3474023)------------------------------
% 6.25/2.50 % (3474023)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.25/2.50 % (3474023)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/2.50 % (3474023)CaDiCaL version: 2.1.3
% 6.25/2.50 % (3474023)Termination reason: Instruction limit
% 6.25/2.50 % (3474023)Termination phase: Saturation
% 6.25/2.50 % (3474023)Time elapsed: 0.200 s
% 6.25/2.50 % (3474023)Peak memory usage: 91 MB
% 6.25/2.50 % (3474023)Instructions burned: 325 (million)
% 6.25/2.50 % (3474030)Instruction limit reached!
% 6.25/2.50 % (3474030)------------------------------
% 6.25/2.50 % (3474030)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.25/2.50 % (3474030)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/2.50 % (3474030)CaDiCaL version: 2.1.3
% 6.25/2.50 % (3474030)Termination reason: Instruction limit
% 6.25/2.50 % (3474030)Termination phase: Saturation
% 6.25/2.50 % (3474030)Time elapsed: 0.040 s
% 6.25/2.50 % (3474030)Peak memory usage: 91 MB
% 6.25/2.50 % (3474030)Instructions burned: 113 (million)
% 6.25/2.50 % (3474035)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=829008436:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2993 on theBenchmark for (2993ds/114Mi)
% 6.25/2.50 % (3474034)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2541584124:i=127:av=off:fsr=off:sup=off_2993 on theBenchmark for (2993ds/127Mi)
% 6.25/2.50 % (3474035)Instruction limit reached!
% 6.25/2.50 % (3474035)------------------------------
% 6.25/2.50 % (3474035)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.25/2.50 % (3474035)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/2.50 % (3474035)CaDiCaL version: 2.1.3
% 6.25/2.50 % (3474035)Termination reason: Instruction limit
% 6.25/2.50 % (3474035)Termination phase: Saturation
% 6.25/2.50 % (3474035)Time elapsed: 0.038 s
% 6.25/2.50 % (3474035)Peak memory usage: 89 MB
% 6.25/2.50 % (3474035)Instructions burned: 116 (million)
% 6.25/2.50 % (3474027)------------------------------
% 6.25/2.50 % (3474027)------------------------------
% 6.25/2.50 % (3474034)Instruction limit reached!
% 6.25/2.50 % (3474034)------------------------------
% 6.25/2.50 % (3474034)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.25/2.50 % (3474034)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/2.50 % (3474034)CaDiCaL version: 2.1.3
% 6.25/2.50 % (3474034)Termination reason: Instruction limit
% 6.25/2.50 % (3474034)Termination phase: Saturation
% 6.25/2.50 % (3474034)Time elapsed: 0.071 s
% 6.25/2.50 % (3474034)Peak memory usage: 89 MB
% 6.25/2.50 % (3474034)Instructions burned: 127 (million)
% 6.25/2.50 % (3474038)lrs+10_1_sil=8000:sp=occurrence:random_seed=1575670472:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 6.25/2.50 % (3474039)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4264434305:i=437:sd=1:aac=none:ss=included_2992 on theBenchmark for (2992ds/437Mi)
% 6.25/2.50 % (3474039)Refutation not found, incomplete strategy
% 6.25/2.50 % (3474039)------------------------------
% 6.25/2.50 % (3474039)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.25/2.50 % (3474039)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/2.50 % (3474039)CaDiCaL version: 2.1.3
% 6.25/2.50 % (3474039)Termination reason: Refutation not found, incomplete strategy
% 6.25/2.50 % (3474039)Time elapsed: 0.006 s
% 6.25/2.50 % (3474039)Peak memory usage: 88 MB
% 6.25/2.50 % (3474039)Instructions burned: 9 (million)
% 6.25/2.50 % (3474040)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=481128394:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi)
% 6.25/2.50 % (3474038)Instruction limit reached!
% 6.25/2.50 % (3474038)------------------------------
% 6.25/2.50 % (3474038)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.25/2.50 % (3474038)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/2.50 % (3474038)CaDiCaL version: 2.1.3
% 6.25/2.50 % (3474038)Termination reason: Instruction limit
% 6.25/2.50 % (3474038)Termination phase: Saturation
% 6.25/2.50 % (3474038)Time elapsed: 0.285 s
% 6.25/2.50 % (3474038)Peak memory usage: 101 MB
% 6.25/2.50 % (3474038)Instructions burned: 908 (million)
% 6.25/2.50 % (3474039)------------------------------
% 6.25/2.50 % (3474039)------------------------------
% 6.25/2.50 % (3474044)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=3309913316:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2988 on theBenchmark for (2988ds/134Mi)
% 6.25/2.50 % (3474044)Instruction limit reached!
% 6.25/2.50 % (3474044)------------------------------
% 6.25/2.50 % (3474044)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.25/2.50 % (3474044)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/2.50 % (3474044)CaDiCaL version: 2.1.3
% 6.25/2.50 % (3474044)Termination reason: Instruction limit
% 6.25/2.50 % (3474044)Termination phase: Saturation
% 6.25/2.50 % (3474044)Time elapsed: 0.044 s
% 6.25/2.50 % (3474044)Peak memory usage: 91 MB
% 6.25/2.50 % (3474044)Instructions burned: 135 (million)
% 6.25/2.50 % (3474045)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3202786521:st=8:i=592:sd=3:ep=RST:ss=axioms_2988 on theBenchmark for (2988ds/592Mi)
% 6.25/2.50 % (3474045)Refutation not found, incomplete strategy
% 6.25/2.50 % (3474045)------------------------------
% 6.25/2.50 % (3474045)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 6.25/2.50 % (3474045)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 6.25/2.50 % (3474045)CaDiCaL version: 2.1.3
% 6.25/2.50 % (3474045)Termination reason: Refutation not found, incomplete strategy
% 6.25/2.50 % (3474045)Time elapsed: 0.006 s
% 6.25/2.50 % (3474045)Peak memory usage: 88 MB
% 6.25/2.50 % (3474045)Instructions burned: 9 (million)
% 6.25/2.50 % (3474047)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=923077248:st=3:i=13193:sd=3:ss=axioms_2987 on theBenchmark for (2987ds/13193Mi)
% 6.25/2.50 % (3474006)First to succeed.
% 6.25/2.50 % (3474006)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3474001"
% 6.25/2.50 % (3474045)------------------------------
% 6.25/2.50 % (3474045)------------------------------
% 6.25/2.50 % (3474006)Refutation found. Thanks to Tanya!
% 6.25/2.50 % SZS status Theorem for theBenchmark
% 6.25/2.50 % SZS output start Proof for theBenchmark
% See solution above
% 0.18/2.70 % (3474006)------------------------------
% 0.18/2.70 % (3474006)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.18/2.70 % (3474006)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.18/2.70 % (3474006)CaDiCaL version: 2.1.3
% 0.18/2.70 % (3474006)Termination reason: Refutation
% 0.18/2.70 % (3474006)Time elapsed: 1.223 s
% 0.18/2.70 % (3474006)Peak memory usage: 135 MB
% 0.18/2.70 % (3474006)Instructions burned: 1781 (million)
% 0.18/2.70 % (3474006)------------------------------
% 0.18/2.70 % (3474006)------------------------------
% 0.18/2.70 % (3474001)Success in time 1.64 s
% 0.18/2.70 % Vampire exiting
%------------------------------------------------------------------------------