%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU385+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 : n011.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:39 PM UTC 2026
% Result : Theorem 8.70s 2.06s
% Output : Refutation 9.04s
% Verified :
% SZS Type : Refutation
% Derivation depth : 26
% Number of leaves : 35
% Syntax : Number of formulae : 278 ( 53 unt; 18 def)
% Number of atoms : 1127 ( 145 equ)
% Maximal formula atoms : 22 ( 4 avg)
% Number of connectives : 1415 ( 566 ~; 657 |; 137 &)
% ( 21 <=>; 34 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 30 ( 28 usr; 12 prp; 0-4 aty)
% Number of functors : 25 ( 25 usr; 10 con; 0-4 aty)
% Number of variables : 329 ( 0 sgn 306 !; 23 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f7,axiom,
! [X0,X1,X2] :
( element(X2,powerset(cartesian_product2(X0,X1)))
=> relation(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f13,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(f14,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(f25,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(f28,axiom,
! [X0] :
( rel_str(X0)
=> one_sorted_str(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_orders_2) ).
fof(f30,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(f33,axiom,
! [X0,X1,X2] :
( relation_of2_as_subset(X2,X0,X1)
=> element(X2,powerset(cartesian_product2(X0,X1))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_relset_1) ).
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(f44,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(f46,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0) )
=> ~ empty(the_carrier(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f48,axiom,
! [X0,X1,X2] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0)
& ~ empty_carrier(X1)
& directed_relstr(X1)
& net_str(X1,X0)
& element(X2,the_carrier(X1)) )
=> ( ~ empty_carrier(netstr_restr_to_element(X0,X1,X2))
& strict_net_str(netstr_restr_to_element(X0,X1,X2),X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc22_waybel_9) ).
fof(f65,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(f66,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(f68,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(f70,conjecture,
! [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(f71,negated_conjecture,
~ ! [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) ) ) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f70]) ).
fof(f73,axiom,
! [X0,X1] :
( element(X0,X1)
=> ( empty(X1)
| in(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
fof(f78,axiom,
! [X0,X1,X2] :
( ( relation(X2)
& function(X2) )
=> ( in(X1,X0)
=> apply(relation_dom_restriction(X2,X0),X1) = apply(X2,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t72_funct_1) ).
fof(f93,plain,
! [X0,X1,X2] :
( relation(X2)
| ~ element(X2,powerset(cartesian_product2(X0,X1))) ),
inference(ennf_transformation,[],[f7]) ).
fof(f103,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,[],[f13]) ).
fof(f104,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,[],[f103]) ).
fof(f105,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,[],[f14]) ).
fof(f106,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,[],[f105]) ).
fof(f117,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,[],[f25]) ).
fof(f118,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,[],[f117]) ).
fof(f122,plain,
! [X0] :
( one_sorted_str(X0)
| ~ rel_str(X0) ),
inference(ennf_transformation,[],[f28]) ).
fof(f123,plain,
! [X0] :
( ! [X1] :
( rel_str(X1)
| ~ net_str(X1,X0) )
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f30]) ).
fof(f124,plain,
! [X0,X1,X2] :
( element(X2,powerset(cartesian_product2(X0,X1)))
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(ennf_transformation,[],[f33]) ).
fof(f126,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(f127,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,[],[f126]) ).
fof(f131,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,[],[f44]) ).
fof(f132,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,[],[f131]) ).
fof(f133,plain,
! [X0] :
( ~ empty(the_carrier(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f46]) ).
fof(f134,plain,
! [X0] :
( ~ empty(the_carrier(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(flattening,[],[f133]) ).
fof(f135,plain,
! [X0,X1,X2] :
( ( ~ empty_carrier(netstr_restr_to_element(X0,X1,X2))
& strict_net_str(netstr_restr_to_element(X0,X1,X2),X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0)
| ~ element(X2,the_carrier(X1)) ),
inference(ennf_transformation,[],[f48]) ).
fof(f136,plain,
! [X0,X1,X2] :
( ( ~ empty_carrier(netstr_restr_to_element(X0,X1,X2))
& strict_net_str(netstr_restr_to_element(X0,X1,X2),X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0)
| ~ element(X2,the_carrier(X1)) ),
inference(flattening,[],[f135]) ).
fof(f149,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,[],[f65]) ).
fof(f150,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,[],[f149]) ).
fof(f151,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,[],[f66]) ).
fof(f152,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,[],[f151]) ).
fof(f155,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,[],[f71]) ).
fof(f156,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,[],[f155]) ).
fof(f158,plain,
! [X0,X1] :
( empty(X1)
| in(X0,X1)
| ~ element(X0,X1) ),
inference(ennf_transformation,[],[f73]) ).
fof(f159,plain,
! [X0,X1] :
( empty(X1)
| in(X0,X1)
| ~ element(X0,X1) ),
inference(flattening,[],[f158]) ).
fof(f165,plain,
! [X0,X1,X2] :
( apply(relation_dom_restriction(X2,X0),X1) = apply(X2,X1)
| ~ in(X1,X0)
| ~ relation(X2)
| ~ function(X2) ),
inference(ennf_transformation,[],[f78]) ).
fof(f166,plain,
! [X0,X1,X2] :
( apply(relation_dom_restriction(X2,X0),X1) = apply(X2,X1)
| ~ in(X1,X0)
| ~ relation(X2)
| ~ function(X2) ),
inference(flattening,[],[f165]) ).
fof(f169,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(f170,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(f171,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,[],[f104,f170,f169]) ).
fof(f172,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,[],[f170]) ).
fof(f173,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,[],[f172]) ).
fof(f174,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,[],[f169]) ).
fof(f175,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,[],[f174]) ).
fof(f176,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,[],[f175]) ).
fof(f177,plain,
! [X0,X1,X2,X3] :
( ( sP0(X0,X1,X2,X3)
| ( ( ! [X5] :
( ~ element(X5,the_carrier(X0))
| sK2(X0,X1,X2) != X5
| ~ related(X0,X1,X5) )
| ~ in(sK2(X0,X1,X2),the_carrier(X2)) )
& ( ( element(sK3(X0,X1,X2),the_carrier(X0))
& sK2(X0,X1,X2) = sK3(X0,X1,X2)
& related(X0,X1,sK3(X0,X1,X2)) )
| in(sK2(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(sK4(X0,X1,X7),the_carrier(X0))
& sK4(X0,X1,X7) = X7
& related(X0,X1,sK4(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,[sK2,sK3,sK4]),skolemize(X4,sK2(X0,X1,X2)),skolemize(X6,sK3(X0,X1,X2)),skolemize(X9,sK4(X0,X1,X7))],[f176]) ).
fof(f196,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,[],[f68]) ).
fof(f197,plain,
( apply_netmap(sK23,sK24,sK26) != apply_netmap(sK23,netstr_restr_to_element(sK23,sK24,sK25),sK27)
& sK26 = sK27
& element(sK27,the_carrier(netstr_restr_to_element(sK23,sK24,sK25)))
& element(sK26,the_carrier(sK24))
& element(sK25,the_carrier(sK24))
& ~ empty_carrier(sK24)
& directed_relstr(sK24)
& net_str(sK24,sK23)
& ~ empty_carrier(sK23)
& one_sorted_str(sK23) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23,sK24,sK25,sK26,sK27]),skolemize(X0,sK23),skolemize(X1,sK24),skolemize(X2,sK25),skolemize(X3,sK26),skolemize(X4,sK27)],[f156]) ).
fof(f206,plain,
! [X2,X0,X1] :
( ~ element(X2,powerset(cartesian_product2(X0,X1)))
| relation(X2) ),
inference(cnf_transformation,[],[f93]) ).
fof(f218,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,[],[f173]) ).
fof(f220,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,[],[f177]) ).
fof(f230,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,[],[f171]) ).
fof(f231,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,[],[f106]) ).
fof(f240,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,[],[f118]) ).
fof(f244,plain,
! [X0] :
( ~ rel_str(X0)
| one_sorted_str(X0) ),
inference(cnf_transformation,[],[f122]) ).
fof(f245,plain,
! [X0,X1] :
( ~ net_str(X1,X0)
| rel_str(X1)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f123]) ).
fof(f246,plain,
! [X2,X0,X1] :
( element(X2,powerset(cartesian_product2(X0,X1)))
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(cnf_transformation,[],[f124]) ).
fof(f248,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,[],[f127]) ).
fof(f250,plain,
! [X0,X1] :
( function(the_mapping(X0,X1))
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(cnf_transformation,[],[f127]) ).
fof(f258,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,[],[f132]) ).
fof(f259,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,[],[f132]) ).
fof(f266,plain,
! [X0] :
( ~ empty(the_carrier(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f134]) ).
fof(f268,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)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0)
| ~ element(X2,the_carrier(X1)) ),
inference(cnf_transformation,[],[f136]) ).
fof(f269,plain,
! [X2,X0,X1] :
( ~ empty_carrier(netstr_restr_to_element(X0,X1,X2))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0)
| ~ element(X2,the_carrier(X1)) ),
inference(cnf_transformation,[],[f136]) ).
fof(f306,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,[],[f150]) ).
fof(f307,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,[],[f152]) ).
fof(f309,plain,
! [X2,X0,X1] :
( ~ relation_of2_as_subset(X2,X0,X1)
| relation_of2(X2,X0,X1) ),
inference(cnf_transformation,[],[f196]) ).
fof(f310,plain,
! [X2,X0,X1] :
( ~ relation_of2(X2,X0,X1)
| relation_of2_as_subset(X2,X0,X1) ),
inference(cnf_transformation,[],[f196]) ).
fof(f312,plain,
one_sorted_str(sK23),
inference(cnf_transformation,[],[f197]) ).
fof(f313,plain,
~ empty_carrier(sK23),
inference(cnf_transformation,[],[f197]) ).
fof(f314,plain,
net_str(sK24,sK23),
inference(cnf_transformation,[],[f197]) ).
fof(f315,plain,
directed_relstr(sK24),
inference(cnf_transformation,[],[f197]) ).
fof(f316,plain,
~ empty_carrier(sK24),
inference(cnf_transformation,[],[f197]) ).
fof(f317,plain,
element(sK25,the_carrier(sK24)),
inference(cnf_transformation,[],[f197]) ).
fof(f318,plain,
element(sK26,the_carrier(sK24)),
inference(cnf_transformation,[],[f197]) ).
fof(f319,plain,
element(sK27,the_carrier(netstr_restr_to_element(sK23,sK24,sK25))),
inference(cnf_transformation,[],[f197]) ).
fof(f320,plain,
sK26 = sK27,
inference(cnf_transformation,[],[f197]) ).
fof(f321,plain,
apply_netmap(sK23,sK24,sK26) != apply_netmap(sK23,netstr_restr_to_element(sK23,sK24,sK25),sK27),
inference(cnf_transformation,[],[f197]) ).
fof(f323,plain,
! [X0,X1] :
( ~ element(X0,X1)
| in(X0,X1)
| empty(X1) ),
inference(cnf_transformation,[],[f159]) ).
fof(f328,plain,
! [X2,X0,X1] :
( ~ in(X1,X0)
| apply(relation_dom_restriction(X2,X0),X1) = apply(X2,X1)
| ~ relation(X2)
| ~ function(X2) ),
inference(cnf_transformation,[],[f166]) ).
fof(f331,plain,
apply_netmap(sK23,netstr_restr_to_element(sK23,sK24,sK25),sK27) != apply_netmap(sK23,sK24,sK27),
inference(definition_unfolding,[],[f321,f320]) ).
fof(f332,plain,
element(sK27,the_carrier(sK24)),
inference(definition_unfolding,[],[f318,f320]) ).
fof(f333,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,[],[f218]) ).
fof(f336,definition,
sF28 = netstr_restr_to_element(sK23,sK24,sK25),
introduced(definition,[new_symbols(definition,[sF28])],[function_definition]) ).
fof(f337,plain,
netstr_restr_to_element(sK23,sK24,sK25) = sF28,
inference(reorient_equations,[],[f336]) ).
fof(f338,definition,
sF29 = apply_netmap(sK23,sF28,sK27),
introduced(definition,[new_symbols(definition,[sF29])],[function_definition]) ).
fof(f339,plain,
apply_netmap(sK23,sF28,sK27) = sF29,
inference(reorient_equations,[],[f338]) ).
fof(f340,definition,
sF30 = apply_netmap(sK23,sK24,sK27),
introduced(definition,[new_symbols(definition,[sF30])],[function_definition]) ).
fof(f341,plain,
apply_netmap(sK23,sK24,sK27) = sF30,
inference(reorient_equations,[],[f340]) ).
fof(f342,plain,
sF29 != sF30,
inference(definition_folding,[],[f331,f341,f339,f337]) ).
fof(f343,definition,
sF31 = the_carrier(sF28),
introduced(definition,[new_symbols(definition,[sF31])],[function_definition]) ).
fof(f344,plain,
the_carrier(sF28) = sF31,
inference(reorient_equations,[],[f343]) ).
fof(f345,plain,
element(sK27,sF31),
inference(definition_folding,[],[f319,f344,f337]) ).
fof(f346,definition,
sF32 = the_carrier(sK24),
introduced(definition,[new_symbols(definition,[sF32])],[function_definition]) ).
fof(f347,plain,
the_carrier(sK24) = sF32,
inference(reorient_equations,[],[f346]) ).
fof(f348,plain,
element(sK27,sF32),
inference(definition_folding,[],[f332,f347]) ).
fof(f349,plain,
element(sK25,sF32),
inference(definition_folding,[],[f317,f347]) ).
fof(f350,plain,
! [X0,X1] :
( ~ element(X0,sF32)
| apply_netmap(X1,sK24,X0) = apply_on_structs(sK24,X1,the_mapping(X1,sK24),X0)
| empty_carrier(sK24)
| ~ net_str(sK24,X1)
| empty_carrier(X1)
| ~ one_sorted_str(X1) ),
inference(superposition,[],[f231,f347]) ).
fof(f351,plain,
! [X0,X1] :
( ~ element(X0,sF32)
| apply_netmap(X1,sK24,X0) = apply_on_structs(sK24,X1,the_mapping(X1,sK24),X0)
| ~ net_str(sK24,X1)
| empty_carrier(X1)
| ~ one_sorted_str(X1) ),
inference(forward_subsumption_resolution,[],[f350,f316]) ).
fof(f352,plain,
! [X0,X1] :
( ~ element(X0,sF31)
| apply_netmap(X1,sF28,X0) = apply_on_structs(sF28,X1,the_mapping(X1,sF28),X0)
| empty_carrier(sF28)
| ~ net_str(sF28,X1)
| empty_carrier(X1)
| ~ one_sorted_str(X1) ),
inference(superposition,[],[f231,f344]) ).
fof(f354,definition,
( spl33_1
<=> empty_carrier(sF28) ),
introduced(definition,[new_symbols(definition,[spl33_1])],[avatar_definition]) ).
fof(f355,plain,
( ~ empty_carrier(sF28)
| spl33_1 ),
inference(avatar_component_clause,[],[f354]) ).
fof(f356,plain,
( empty_carrier(sF28)
| ~ spl33_1 ),
inference(avatar_component_clause,[],[f354]) ).
fof(f358,definition,
( spl33_2
<=> ! [X0,X1] :
( ~ element(X0,sF31)
| ~ one_sorted_str(X1)
| empty_carrier(X1)
| ~ net_str(sF28,X1)
| apply_netmap(X1,sF28,X0) = apply_on_structs(sF28,X1,the_mapping(X1,sF28),X0) ) ),
introduced(definition,[new_symbols(definition,[spl33_2])],[avatar_definition]) ).
fof(f359,plain,
( ! [X0,X1] :
( ~ element(X0,sF31)
| ~ one_sorted_str(X1)
| empty_carrier(X1)
| ~ net_str(sF28,X1)
| apply_netmap(X1,sF28,X0) = apply_on_structs(sF28,X1,the_mapping(X1,sF28),X0) )
| ~ spl33_2 ),
inference(avatar_component_clause,[],[f358]) ).
fof(f360,plain,
( spl33_1
| spl33_2 ),
inference(avatar_split_clause,[],[f352,f358,f354]) ).
fof(f361,plain,
! [X0] :
( quasi_total(the_mapping(X0,sK24),sF32,the_carrier(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(sK24)
| ~ net_str(sK24,X0) ),
inference(superposition,[],[f258,f347]) ).
fof(f362,plain,
! [X0] :
( quasi_total(the_mapping(X0,sF28),sF31,the_carrier(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(sF28)
| ~ net_str(sF28,X0) ),
inference(superposition,[],[f258,f344]) ).
fof(f366,definition,
( spl33_3
<=> one_sorted_str(sF28) ),
introduced(definition,[new_symbols(definition,[spl33_3])],[avatar_definition]) ).
fof(f367,plain,
( one_sorted_str(sF28)
| ~ spl33_3 ),
inference(avatar_component_clause,[],[f366]) ).
fof(f368,plain,
( ~ one_sorted_str(sF28)
| spl33_3 ),
inference(avatar_component_clause,[],[f366]) ).
fof(f375,definition,
( spl33_5
<=> ! [X0] :
( quasi_total(the_mapping(X0,sF28),sF31,the_carrier(X0))
| ~ net_str(sF28,X0)
| ~ one_sorted_str(X0)
| empty_carrier(X0) ) ),
introduced(definition,[new_symbols(definition,[spl33_5])],[avatar_definition]) ).
fof(f376,plain,
( ! [X0] :
( quasi_total(the_mapping(X0,sF28),sF31,the_carrier(X0))
| ~ net_str(sF28,X0)
| ~ one_sorted_str(X0)
| empty_carrier(X0) )
| ~ spl33_5 ),
inference(avatar_component_clause,[],[f375]) ).
fof(f377,plain,
( spl33_1
| spl33_5 ),
inference(avatar_split_clause,[],[f362,f375,f354]) ).
fof(f378,plain,
! [X0] :
( quasi_total(the_mapping(X0,sK24),sF32,the_carrier(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ net_str(sK24,X0) ),
inference(forward_subsumption_resolution,[],[f361,f316]) ).
fof(f380,definition,
( spl33_6
<=> one_sorted_str(sK24) ),
introduced(definition,[new_symbols(definition,[spl33_6])],[avatar_definition]) ).
fof(f381,plain,
( one_sorted_str(sK24)
| ~ spl33_6 ),
inference(avatar_component_clause,[],[f380]) ).
fof(f382,plain,
( ~ one_sorted_str(sK24)
| spl33_6 ),
inference(avatar_component_clause,[],[f380]) ).
fof(f387,plain,
( strict_net_str(sF28,sK23)
| empty_carrier(sK23)
| ~ one_sorted_str(sK23)
| empty_carrier(sK24)
| ~ directed_relstr(sK24)
| ~ net_str(sK24,sK23)
| ~ element(sK25,the_carrier(sK24)) ),
inference(superposition,[],[f268,f337]) ).
fof(f388,plain,
( strict_net_str(sF28,sK23)
| ~ one_sorted_str(sK23)
| empty_carrier(sK24)
| ~ directed_relstr(sK24)
| ~ net_str(sK24,sK23)
| ~ element(sK25,the_carrier(sK24)) ),
inference(forward_subsumption_resolution,[],[f387,f313]) ).
fof(f389,plain,
( strict_net_str(sF28,sK23)
| empty_carrier(sK24)
| ~ directed_relstr(sK24)
| ~ net_str(sK24,sK23)
| ~ element(sK25,the_carrier(sK24)) ),
inference(forward_subsumption_resolution,[],[f388,f312]) ).
fof(f390,plain,
( strict_net_str(sF28,sK23)
| ~ directed_relstr(sK24)
| ~ net_str(sK24,sK23)
| ~ element(sK25,the_carrier(sK24)) ),
inference(forward_subsumption_resolution,[],[f389,f316]) ).
fof(f391,plain,
( strict_net_str(sF28,sK23)
| ~ net_str(sK24,sK23)
| ~ element(sK25,the_carrier(sK24)) ),
inference(forward_subsumption_resolution,[],[f390,f315]) ).
fof(f392,plain,
( strict_net_str(sF28,sK23)
| ~ element(sK25,the_carrier(sK24)) ),
inference(forward_subsumption_resolution,[],[f391,f314]) ).
fof(f393,plain,
( ~ element(sK25,sF32)
| strict_net_str(sF28,sK23) ),
inference(forward_demodulation,[],[f392,f347]) ).
fof(f394,plain,
strict_net_str(sF28,sK23),
inference(forward_subsumption_resolution,[],[f393,f349]) ).
fof(f395,plain,
! [X0] :
( ~ net_str(sK24,X0)
| apply_netmap(X0,sK24,sK27) = apply_on_structs(sK24,X0,the_mapping(X0,sK24),sK27)
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(resolution,[],[f351,f348]) ).
fof(f400,plain,
( apply_netmap(sK23,sK24,sK27) = apply_on_structs(sK24,sK23,the_mapping(sK23,sK24),sK27)
| empty_carrier(sK23)
| ~ one_sorted_str(sK23) ),
inference(resolution,[],[f395,f314]) ).
fof(f401,plain,
( apply_netmap(sK23,sK24,sK27) = apply_on_structs(sK24,sK23,the_mapping(sK23,sK24),sK27)
| ~ one_sorted_str(sK23) ),
inference(forward_subsumption_resolution,[],[f400,f313]) ).
fof(f402,plain,
apply_netmap(sK23,sK24,sK27) = apply_on_structs(sK24,sK23,the_mapping(sK23,sK24),sK27),
inference(forward_subsumption_resolution,[],[f401,f312]) ).
fof(f403,plain,
sF30 = apply_on_structs(sK24,sK23,the_mapping(sK23,sK24),sK27),
inference(forward_demodulation,[],[f402,f341]) ).
fof(f406,plain,
( ~ empty(sF31)
| empty_carrier(sF28)
| ~ one_sorted_str(sF28) ),
inference(superposition,[],[f266,f344]) ).
fof(f407,plain,
( ~ empty_carrier(sF28)
| empty_carrier(sK23)
| ~ one_sorted_str(sK23)
| empty_carrier(sK24)
| ~ directed_relstr(sK24)
| ~ net_str(sK24,sK23)
| ~ element(sK25,the_carrier(sK24)) ),
inference(superposition,[],[f269,f337]) ).
fof(f408,plain,
( empty_carrier(sK23)
| ~ one_sorted_str(sK23)
| empty_carrier(sK24)
| ~ directed_relstr(sK24)
| ~ net_str(sK24,sK23)
| ~ element(sK25,the_carrier(sK24))
| ~ spl33_1 ),
inference(forward_subsumption_resolution,[],[f407,f356]) ).
fof(f409,plain,
( ~ one_sorted_str(sK23)
| empty_carrier(sK24)
| ~ directed_relstr(sK24)
| ~ net_str(sK24,sK23)
| ~ element(sK25,the_carrier(sK24))
| ~ spl33_1 ),
inference(forward_subsumption_resolution,[],[f408,f313]) ).
fof(f410,plain,
( empty_carrier(sK24)
| ~ directed_relstr(sK24)
| ~ net_str(sK24,sK23)
| ~ element(sK25,the_carrier(sK24))
| ~ spl33_1 ),
inference(forward_subsumption_resolution,[],[f409,f312]) ).
fof(f411,plain,
( ~ directed_relstr(sK24)
| ~ net_str(sK24,sK23)
| ~ element(sK25,the_carrier(sK24))
| ~ spl33_1 ),
inference(forward_subsumption_resolution,[],[f410,f316]) ).
fof(f412,plain,
( ~ net_str(sK24,sK23)
| ~ element(sK25,the_carrier(sK24))
| ~ spl33_1 ),
inference(forward_subsumption_resolution,[],[f411,f315]) ).
fof(f413,plain,
( ~ element(sK25,the_carrier(sK24))
| ~ spl33_1 ),
inference(forward_subsumption_resolution,[],[f412,f314]) ).
fof(f414,plain,
( ~ element(sK25,sF32)
| ~ spl33_1 ),
inference(forward_demodulation,[],[f413,f347]) ).
fof(f415,plain,
( $false
| ~ spl33_1 ),
inference(forward_subsumption_resolution,[],[f414,f349]) ).
fof(f416,plain,
~ spl33_1,
inference(avatar_contradiction_clause,[],[f415]) ).
fof(f417,plain,
( net_str(sF28,sK23)
| empty_carrier(sK23)
| ~ one_sorted_str(sK23)
| empty_carrier(sK24)
| ~ net_str(sK24,sK23)
| ~ element(sK25,the_carrier(sK24)) ),
inference(superposition,[],[f240,f337]) ).
fof(f418,plain,
( net_str(sF28,sK23)
| ~ one_sorted_str(sK23)
| empty_carrier(sK24)
| ~ net_str(sK24,sK23)
| ~ element(sK25,the_carrier(sK24)) ),
inference(forward_subsumption_resolution,[],[f417,f313]) ).
fof(f419,plain,
( net_str(sF28,sK23)
| empty_carrier(sK24)
| ~ net_str(sK24,sK23)
| ~ element(sK25,the_carrier(sK24)) ),
inference(forward_subsumption_resolution,[],[f418,f312]) ).
fof(f420,plain,
( net_str(sF28,sK23)
| ~ net_str(sK24,sK23)
| ~ element(sK25,the_carrier(sK24)) ),
inference(forward_subsumption_resolution,[],[f419,f316]) ).
fof(f421,plain,
( net_str(sF28,sK23)
| ~ element(sK25,the_carrier(sK24)) ),
inference(forward_subsumption_resolution,[],[f420,f314]) ).
fof(f422,plain,
( ~ element(sK25,sF32)
| net_str(sF28,sK23) ),
inference(forward_demodulation,[],[f421,f347]) ).
fof(f423,plain,
net_str(sF28,sK23),
inference(forward_subsumption_resolution,[],[f422,f349]) ).
fof(f446,plain,
( rel_str(sK24)
| ~ one_sorted_str(sK23) ),
inference(resolution,[],[f245,f314]) ).
fof(f448,plain,
( rel_str(sF28)
| ~ one_sorted_str(sK23) ),
inference(resolution,[],[f245,f423]) ).
fof(f450,plain,
rel_str(sF28),
inference(forward_subsumption_resolution,[],[f448,f312]) ).
fof(f451,plain,
rel_str(sK24),
inference(forward_subsumption_resolution,[],[f446,f312]) ).
fof(f453,plain,
! [X2,X0,X1] :
( ~ quasi_total(X0,sF32,the_carrier(X1))
| empty_carrier(sK24)
| ~ one_sorted_str(sK24)
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ function(X0)
| apply_on_structs(sK24,X1,X0,X2) = apply(X0,X2)
| ~ relation_of2(X0,sF32,the_carrier(X1))
| ~ element(X2,sF32) ),
inference(superposition,[],[f306,f347]) ).
fof(f454,plain,
! [X2,X0,X1] :
( ~ quasi_total(X0,sF31,the_carrier(X1))
| empty_carrier(sF28)
| ~ one_sorted_str(sF28)
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ function(X0)
| apply(X0,X2) = apply_on_structs(sF28,X1,X0,X2)
| ~ relation_of2(X0,sF31,the_carrier(X1))
| ~ element(X2,sF31) ),
inference(superposition,[],[f306,f344]) ).
fof(f465,plain,
( ~ sP1(sK23,sF28,sK25,sK24)
| sP0(sK24,sK25,sF28,sK23) ),
inference(superposition,[],[f333,f337]) ).
fof(f467,definition,
( spl33_8
<=> sP0(sK24,sK25,sF28,sK23) ),
introduced(definition,[new_symbols(definition,[spl33_8])],[avatar_definition]) ).
fof(f469,plain,
( sP0(sK24,sK25,sF28,sK23)
| ~ spl33_8 ),
inference(avatar_component_clause,[],[f467]) ).
fof(f471,definition,
( spl33_9
<=> sP1(sK23,sF28,sK25,sK24) ),
introduced(definition,[new_symbols(definition,[spl33_9])],[avatar_definition]) ).
fof(f473,plain,
( ~ sP1(sK23,sF28,sK25,sK24)
| spl33_9 ),
inference(avatar_component_clause,[],[f471]) ).
fof(f474,plain,
( spl33_8
| ~ spl33_9 ),
inference(avatar_split_clause,[],[f465,f471,f467]) ).
fof(f477,plain,
( in(sK27,sF31)
| empty(sF31) ),
inference(resolution,[],[f323,f345]) ).
fof(f505,definition,
( spl33_15
<=> empty(sF31) ),
introduced(definition,[new_symbols(definition,[spl33_15])],[avatar_definition]) ).
fof(f507,plain,
( empty(sF31)
| ~ spl33_15 ),
inference(avatar_component_clause,[],[f505]) ).
fof(f509,definition,
( spl33_16
<=> in(sK27,sF31) ),
introduced(definition,[new_symbols(definition,[spl33_16])],[avatar_definition]) ).
fof(f511,plain,
( in(sK27,sF31)
| ~ spl33_16 ),
inference(avatar_component_clause,[],[f509]) ).
fof(f512,plain,
( spl33_15
| spl33_16 ),
inference(avatar_split_clause,[],[f477,f509,f505]) ).
fof(f543,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,[],[f248,f309]) ).
fof(f549,plain,
! [X0] :
( relation_of2(the_mapping(X0,sK24),sF32,the_carrier(X0))
| ~ net_str(sK24,X0)
| ~ one_sorted_str(X0) ),
inference(superposition,[],[f543,f347]) ).
fof(f550,plain,
! [X0] :
( relation_of2(the_mapping(X0,sF28),sF31,the_carrier(X0))
| ~ net_str(sF28,X0)
| ~ one_sorted_str(X0) ),
inference(superposition,[],[f543,f344]) ).
fof(f554,plain,
( ~ strict_net_str(sF28,sK23)
| ~ net_str(sF28,sK23)
| ~ element(sK25,the_carrier(sK24))
| empty_carrier(sK24)
| ~ net_str(sK24,sK23)
| empty_carrier(sK23)
| ~ one_sorted_str(sK23)
| spl33_9 ),
inference(resolution,[],[f473,f230]) ).
fof(f555,plain,
( ~ net_str(sF28,sK23)
| ~ element(sK25,the_carrier(sK24))
| empty_carrier(sK24)
| ~ net_str(sK24,sK23)
| empty_carrier(sK23)
| ~ one_sorted_str(sK23)
| spl33_9 ),
inference(forward_subsumption_resolution,[],[f554,f394]) ).
fof(f556,plain,
( ~ element(sK25,the_carrier(sK24))
| empty_carrier(sK24)
| ~ net_str(sK24,sK23)
| empty_carrier(sK23)
| ~ one_sorted_str(sK23)
| spl33_9 ),
inference(forward_subsumption_resolution,[],[f555,f423]) ).
fof(f557,plain,
( ~ element(sK25,the_carrier(sK24))
| ~ net_str(sK24,sK23)
| empty_carrier(sK23)
| ~ one_sorted_str(sK23)
| spl33_9 ),
inference(forward_subsumption_resolution,[],[f556,f316]) ).
fof(f558,plain,
( ~ element(sK25,the_carrier(sK24))
| empty_carrier(sK23)
| ~ one_sorted_str(sK23)
| spl33_9 ),
inference(forward_subsumption_resolution,[],[f557,f314]) ).
fof(f559,plain,
( ~ element(sK25,the_carrier(sK24))
| ~ one_sorted_str(sK23)
| spl33_9 ),
inference(forward_subsumption_resolution,[],[f558,f313]) ).
fof(f560,plain,
( ~ element(sK25,the_carrier(sK24))
| spl33_9 ),
inference(forward_subsumption_resolution,[],[f559,f312]) ).
fof(f561,plain,
( ~ element(sK25,sF32)
| spl33_9 ),
inference(forward_demodulation,[],[f560,f347]) ).
fof(f562,plain,
( $false
| spl33_9 ),
inference(forward_subsumption_resolution,[],[f561,f349]) ).
fof(f563,plain,
spl33_9,
inference(avatar_contradiction_clause,[],[f562]) ).
fof(f577,plain,
( ! [X0] :
( ~ net_str(sF28,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| apply_netmap(X0,sF28,sK27) = apply_on_structs(sF28,X0,the_mapping(X0,sF28),sK27) )
| ~ spl33_2 ),
inference(resolution,[],[f359,f345]) ).
fof(f578,plain,
( empty_carrier(sK23)
| ~ one_sorted_str(sK23)
| apply_netmap(sK23,sF28,sK27) = apply_on_structs(sF28,sK23,the_mapping(sK23,sF28),sK27)
| ~ spl33_2 ),
inference(resolution,[],[f577,f423]) ).
fof(f579,plain,
( ~ one_sorted_str(sK23)
| apply_netmap(sK23,sF28,sK27) = apply_on_structs(sF28,sK23,the_mapping(sK23,sF28),sK27)
| ~ spl33_2 ),
inference(forward_subsumption_resolution,[],[f578,f313]) ).
fof(f580,plain,
( apply_netmap(sK23,sF28,sK27) = apply_on_structs(sF28,sK23,the_mapping(sK23,sF28),sK27)
| ~ spl33_2 ),
inference(forward_subsumption_resolution,[],[f579,f312]) ).
fof(f581,plain,
( sF29 = apply_on_structs(sF28,sK23,the_mapping(sK23,sF28),sK27)
| ~ spl33_2 ),
inference(forward_demodulation,[],[f580,f339]) ).
fof(f582,plain,
( the_mapping(sK23,sF28) = partfun_dom_restriction(the_carrier(sK24),the_carrier(sK23),the_mapping(sK23,sK24),the_carrier(sF28))
| ~ spl33_8 ),
inference(resolution,[],[f220,f469]) ).
fof(f584,plain,
( the_mapping(sK23,sF28) = partfun_dom_restriction(the_carrier(sK24),the_carrier(sK23),the_mapping(sK23,sK24),sF31)
| ~ spl33_8 ),
inference(forward_demodulation,[],[f582,f344]) ).
fof(f585,plain,
( the_mapping(sK23,sF28) = partfun_dom_restriction(sF32,the_carrier(sK23),the_mapping(sK23,sK24),sF31)
| ~ spl33_8 ),
inference(forward_demodulation,[],[f584,f347]) ).
fof(f592,plain,
one_sorted_str(sK24),
inference(resolution,[],[f244,f451]) ).
fof(f593,plain,
one_sorted_str(sF28),
inference(resolution,[],[f244,f450]) ).
fof(f594,plain,
( $false
| spl33_3 ),
inference(forward_subsumption_resolution,[],[f593,f368]) ).
fof(f595,plain,
spl33_3,
inference(avatar_contradiction_clause,[],[f594]) ).
fof(f596,plain,
( $false
| spl33_6 ),
inference(forward_subsumption_resolution,[],[f592,f382]) ).
fof(f597,plain,
spl33_6,
inference(avatar_contradiction_clause,[],[f596]) ).
fof(f601,plain,
! [X2,X0,X1] :
( ~ quasi_total(X0,sF32,the_carrier(X1))
| ~ one_sorted_str(sK24)
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ function(X0)
| apply_on_structs(sK24,X1,X0,X2) = apply(X0,X2)
| ~ relation_of2(X0,sF32,the_carrier(X1))
| ~ element(X2,sF32) ),
inference(forward_subsumption_resolution,[],[f453,f316]) ).
fof(f609,plain,
( empty_carrier(sF28)
| ~ one_sorted_str(sF28)
| ~ spl33_15 ),
inference(forward_subsumption_resolution,[],[f406,f507]) ).
fof(f612,plain,
( ! [X2,X0,X1] :
( ~ quasi_total(X0,sF31,the_carrier(X1))
| ~ one_sorted_str(sF28)
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ function(X0)
| apply(X0,X2) = apply_on_structs(sF28,X1,X0,X2)
| ~ relation_of2(X0,sF31,the_carrier(X1))
| ~ element(X2,sF31) )
| spl33_1 ),
inference(forward_subsumption_resolution,[],[f454,f355]) ).
fof(f623,plain,
( ! [X2,X0,X1] :
( ~ quasi_total(X0,sF32,the_carrier(X1))
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ function(X0)
| apply_on_structs(sK24,X1,X0,X2) = apply(X0,X2)
| ~ relation_of2(X0,sF32,the_carrier(X1))
| ~ element(X2,sF32) )
| ~ spl33_6 ),
inference(forward_subsumption_resolution,[],[f601,f381]) ).
fof(f640,plain,
( ~ one_sorted_str(sF28)
| spl33_1
| ~ spl33_15 ),
inference(forward_subsumption_resolution,[],[f609,f355]) ).
fof(f643,plain,
( ! [X2,X0,X1] :
( ~ quasi_total(X0,sF31,the_carrier(X1))
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ function(X0)
| apply(X0,X2) = apply_on_structs(sF28,X1,X0,X2)
| ~ relation_of2(X0,sF31,the_carrier(X1))
| ~ element(X2,sF31) )
| spl33_1
| ~ spl33_3 ),
inference(forward_subsumption_resolution,[],[f612,f367]) ).
fof(f663,plain,
( $false
| spl33_1
| ~ spl33_3
| ~ spl33_15 ),
inference(forward_subsumption_resolution,[],[f640,f367]) ).
fof(f664,plain,
( spl33_1
| ~ spl33_3
| ~ spl33_15 ),
inference(avatar_contradiction_clause,[],[f663]) ).
fof(f718,plain,
( ! [X0,X1] :
( empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ function(the_mapping(X0,sK24))
| apply(the_mapping(X0,sK24),X1) = apply_on_structs(sK24,X0,the_mapping(X0,sK24),X1)
| ~ relation_of2(the_mapping(X0,sK24),sF32,the_carrier(X0))
| ~ element(X1,sF32)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ net_str(sK24,X0) )
| ~ spl33_6 ),
inference(resolution,[],[f623,f378]) ).
fof(f721,plain,
( ! [X0,X1] :
( empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ function(the_mapping(X0,sK24))
| apply(the_mapping(X0,sK24),X1) = apply_on_structs(sK24,X0,the_mapping(X0,sK24),X1)
| ~ relation_of2(the_mapping(X0,sK24),sF32,the_carrier(X0))
| ~ element(X1,sF32)
| ~ net_str(sK24,X0) )
| ~ spl33_6 ),
inference(duplicate_literal_removal,[],[f718]) ).
fof(f724,plain,
( ! [X0,X1] :
( empty_carrier(X0)
| ~ one_sorted_str(X0)
| apply(the_mapping(X0,sK24),X1) = apply_on_structs(sK24,X0,the_mapping(X0,sK24),X1)
| ~ relation_of2(the_mapping(X0,sK24),sF32,the_carrier(X0))
| ~ element(X1,sF32)
| ~ net_str(sK24,X0) )
| ~ spl33_6 ),
inference(forward_subsumption_resolution,[],[f721,f250]) ).
fof(f727,plain,
( ! [X0,X1] :
( ~ element(X1,sF32)
| ~ one_sorted_str(X0)
| apply(the_mapping(X0,sK24),X1) = apply_on_structs(sK24,X0,the_mapping(X0,sK24),X1)
| empty_carrier(X0)
| ~ net_str(sK24,X0) )
| ~ spl33_6 ),
inference(forward_subsumption_resolution,[],[f724,f549]) ).
fof(f730,plain,
( ! [X0] :
( ~ net_str(sK24,X0)
| apply_on_structs(sK24,X0,the_mapping(X0,sK24),sK27) = apply(the_mapping(X0,sK24),sK27)
| empty_carrier(X0)
| ~ one_sorted_str(X0) )
| ~ spl33_6 ),
inference(resolution,[],[f727,f348]) ).
fof(f735,plain,
( apply_on_structs(sK24,sK23,the_mapping(sK23,sK24),sK27) = apply(the_mapping(sK23,sK24),sK27)
| empty_carrier(sK23)
| ~ one_sorted_str(sK23)
| ~ spl33_6 ),
inference(resolution,[],[f730,f314]) ).
fof(f736,plain,
( apply_on_structs(sK24,sK23,the_mapping(sK23,sK24),sK27) = apply(the_mapping(sK23,sK24),sK27)
| ~ one_sorted_str(sK23)
| ~ spl33_6 ),
inference(forward_subsumption_resolution,[],[f735,f313]) ).
fof(f737,plain,
( apply_on_structs(sK24,sK23,the_mapping(sK23,sK24),sK27) = apply(the_mapping(sK23,sK24),sK27)
| ~ spl33_6 ),
inference(forward_subsumption_resolution,[],[f736,f312]) ).
fof(f738,plain,
( sF30 = apply(the_mapping(sK23,sK24),sK27)
| ~ spl33_6 ),
inference(forward_demodulation,[],[f737,f403]) ).
fof(f768,plain,
( ! [X0,X1] :
( ~ net_str(sF28,X0)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ function(the_mapping(X0,sF28))
| apply(the_mapping(X0,sF28),X1) = apply_on_structs(sF28,X0,the_mapping(X0,sF28),X1)
| ~ relation_of2(the_mapping(X0,sF28),sF31,the_carrier(X0))
| ~ element(X1,sF31) )
| spl33_1
| ~ spl33_3
| ~ spl33_5 ),
inference(resolution,[],[f376,f643]) ).
fof(f771,plain,
( ! [X0,X1] :
( ~ net_str(sF28,X0)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ function(the_mapping(X0,sF28))
| apply(the_mapping(X0,sF28),X1) = apply_on_structs(sF28,X0,the_mapping(X0,sF28),X1)
| ~ relation_of2(the_mapping(X0,sF28),sF31,the_carrier(X0))
| ~ element(X1,sF31) )
| spl33_1
| ~ spl33_3
| ~ spl33_5 ),
inference(duplicate_literal_removal,[],[f768]) ).
fof(f773,plain,
( ! [X0,X1] :
( ~ net_str(sF28,X0)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| apply(the_mapping(X0,sF28),X1) = apply_on_structs(sF28,X0,the_mapping(X0,sF28),X1)
| ~ relation_of2(the_mapping(X0,sF28),sF31,the_carrier(X0))
| ~ element(X1,sF31) )
| spl33_1
| ~ spl33_3
| ~ spl33_5 ),
inference(forward_subsumption_resolution,[],[f771,f250]) ).
fof(f775,plain,
( ! [X0,X1] :
( ~ element(X1,sF31)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| apply(the_mapping(X0,sF28),X1) = apply_on_structs(sF28,X0,the_mapping(X0,sF28),X1)
| ~ net_str(sF28,X0) )
| spl33_1
| ~ spl33_3
| ~ spl33_5 ),
inference(forward_subsumption_resolution,[],[f773,f550]) ).
fof(f803,definition,
( spl33_28
<=> function(the_mapping(sK23,sK24)) ),
introduced(definition,[new_symbols(definition,[spl33_28])],[avatar_definition]) ).
fof(f804,plain,
( function(the_mapping(sK23,sK24))
| ~ spl33_28 ),
inference(avatar_component_clause,[],[f803]) ).
fof(f805,plain,
( ~ function(the_mapping(sK23,sK24))
| spl33_28 ),
inference(avatar_component_clause,[],[f803]) ).
fof(f815,definition,
( spl33_31
<=> relation_of2(the_mapping(sK23,sK24),sF32,the_carrier(sK23)) ),
introduced(definition,[new_symbols(definition,[spl33_31])],[avatar_definition]) ).
fof(f816,plain,
( relation_of2(the_mapping(sK23,sK24),sF32,the_carrier(sK23))
| ~ spl33_31 ),
inference(avatar_component_clause,[],[f815]) ).
fof(f817,plain,
( ~ relation_of2(the_mapping(sK23,sK24),sF32,the_carrier(sK23))
| spl33_31 ),
inference(avatar_component_clause,[],[f815]) ).
fof(f820,plain,
( empty_carrier(sK23)
| ~ one_sorted_str(sK23)
| empty_carrier(sK24)
| ~ net_str(sK24,sK23)
| spl33_28 ),
inference(resolution,[],[f805,f259]) ).
fof(f821,plain,
( ~ one_sorted_str(sK23)
| empty_carrier(sK24)
| ~ net_str(sK24,sK23)
| spl33_28 ),
inference(forward_subsumption_resolution,[],[f820,f313]) ).
fof(f823,plain,
( empty_carrier(sK24)
| ~ net_str(sK24,sK23)
| spl33_28 ),
inference(forward_subsumption_resolution,[],[f821,f312]) ).
fof(f826,plain,
( ~ net_str(sK24,sK23)
| spl33_28 ),
inference(forward_subsumption_resolution,[],[f823,f316]) ).
fof(f827,plain,
( $false
| spl33_28 ),
inference(forward_subsumption_resolution,[],[f826,f314]) ).
fof(f828,plain,
spl33_28,
inference(avatar_contradiction_clause,[],[f827]) ).
fof(f838,plain,
( ~ net_str(sK24,sK23)
| ~ one_sorted_str(sK23)
| spl33_31 ),
inference(resolution,[],[f817,f549]) ).
fof(f839,plain,
( ~ one_sorted_str(sK23)
| spl33_31 ),
inference(forward_subsumption_resolution,[],[f838,f314]) ).
fof(f840,plain,
( $false
| spl33_31 ),
inference(forward_subsumption_resolution,[],[f839,f312]) ).
fof(f841,plain,
spl33_31,
inference(avatar_contradiction_clause,[],[f840]) ).
fof(f853,plain,
( relation_of2_as_subset(the_mapping(sK23,sK24),sF32,the_carrier(sK23))
| ~ spl33_31 ),
inference(resolution,[],[f816,f310]) ).
fof(f854,plain,
( ! [X0] :
( ~ function(the_mapping(sK23,sK24))
| partfun_dom_restriction(sF32,the_carrier(sK23),the_mapping(sK23,sK24),X0) = relation_dom_restriction(the_mapping(sK23,sK24),X0) )
| ~ spl33_31 ),
inference(resolution,[],[f816,f307]) ).
fof(f855,plain,
( ! [X0] : partfun_dom_restriction(sF32,the_carrier(sK23),the_mapping(sK23,sK24),X0) = relation_dom_restriction(the_mapping(sK23,sK24),X0)
| ~ spl33_28
| ~ spl33_31 ),
inference(forward_subsumption_resolution,[],[f854,f804]) ).
fof(f865,plain,
( the_mapping(sK23,sF28) = relation_dom_restriction(the_mapping(sK23,sK24),sF31)
| ~ spl33_8
| ~ spl33_28
| ~ spl33_31 ),
inference(superposition,[],[f585,f855]) ).
fof(f869,plain,
( ! [X0] :
( ~ relation(X0)
| apply(X0,sK27) = apply(relation_dom_restriction(X0,sF31),sK27)
| ~ function(X0) )
| ~ spl33_16 ),
inference(resolution,[],[f511,f328]) ).
fof(f873,plain,
( ! [X0] :
( ~ net_str(sF28,X0)
| empty_carrier(X0)
| apply_on_structs(sF28,X0,the_mapping(X0,sF28),sK27) = apply(the_mapping(X0,sF28),sK27)
| ~ one_sorted_str(X0) )
| spl33_1
| ~ spl33_3
| ~ spl33_5 ),
inference(resolution,[],[f775,f345]) ).
fof(f874,plain,
( empty_carrier(sK23)
| apply_on_structs(sF28,sK23,the_mapping(sK23,sF28),sK27) = apply(the_mapping(sK23,sF28),sK27)
| ~ one_sorted_str(sK23)
| spl33_1
| ~ spl33_3
| ~ spl33_5 ),
inference(resolution,[],[f873,f423]) ).
fof(f875,plain,
( apply_on_structs(sF28,sK23,the_mapping(sK23,sF28),sK27) = apply(the_mapping(sK23,sF28),sK27)
| ~ one_sorted_str(sK23)
| spl33_1
| ~ spl33_3
| ~ spl33_5 ),
inference(forward_subsumption_resolution,[],[f874,f313]) ).
fof(f876,plain,
( apply_on_structs(sF28,sK23,the_mapping(sK23,sF28),sK27) = apply(the_mapping(sK23,sF28),sK27)
| spl33_1
| ~ spl33_3
| ~ spl33_5 ),
inference(forward_subsumption_resolution,[],[f875,f312]) ).
fof(f877,plain,
( sF29 = apply(the_mapping(sK23,sF28),sK27)
| spl33_1
| ~ spl33_2
| ~ spl33_3
| ~ spl33_5 ),
inference(forward_demodulation,[],[f876,f581]) ).
fof(f913,plain,
! [X2,X0,X1] :
( ~ relation_of2_as_subset(X0,X1,X2)
| relation(X0) ),
inference(resolution,[],[f246,f206]) ).
fof(f918,plain,
( relation(the_mapping(sK23,sK24))
| ~ spl33_31 ),
inference(resolution,[],[f913,f853]) ).
fof(f987,plain,
( apply(the_mapping(sK23,sK24),sK27) = apply(relation_dom_restriction(the_mapping(sK23,sK24),sF31),sK27)
| ~ function(the_mapping(sK23,sK24))
| ~ spl33_16
| ~ spl33_31 ),
inference(resolution,[],[f918,f869]) ).
fof(f992,plain,
( apply(the_mapping(sK23,sK24),sK27) = apply(relation_dom_restriction(the_mapping(sK23,sK24),sF31),sK27)
| ~ spl33_16
| ~ spl33_28
| ~ spl33_31 ),
inference(forward_subsumption_resolution,[],[f987,f804]) ).
fof(f995,plain,
( apply(the_mapping(sK23,sK24),sK27) = apply(the_mapping(sK23,sF28),sK27)
| ~ spl33_8
| ~ spl33_16
| ~ spl33_28
| ~ spl33_31 ),
inference(forward_demodulation,[],[f992,f865]) ).
fof(f996,plain,
( sF29 = apply(the_mapping(sK23,sK24),sK27)
| spl33_1
| ~ spl33_2
| ~ spl33_3
| ~ spl33_5
| ~ spl33_8
| ~ spl33_16
| ~ spl33_28
| ~ spl33_31 ),
inference(forward_demodulation,[],[f995,f877]) ).
fof(f997,plain,
( sF29 = sF30
| spl33_1
| ~ spl33_2
| ~ spl33_3
| ~ spl33_5
| ~ spl33_6
| ~ spl33_8
| ~ spl33_16
| ~ spl33_28
| ~ spl33_31 ),
inference(forward_demodulation,[],[f996,f738]) ).
fof(f998,plain,
( $false
| spl33_1
| ~ spl33_2
| ~ spl33_3
| ~ spl33_5
| ~ spl33_6
| ~ spl33_8
| ~ spl33_16
| ~ spl33_28
| ~ spl33_31 ),
inference(forward_subsumption_resolution,[],[f997,f342]) ).
fof(f999,plain,
( spl33_1
| ~ spl33_2
| ~ spl33_3
| ~ spl33_5
| ~ spl33_6
| ~ spl33_8
| ~ spl33_16
| ~ spl33_28
| ~ spl33_31 ),
inference(avatar_contradiction_clause,[],[f998]) ).
cnf(s1,plain,
( spl33_1
| spl33_2 ),
inference(sat_conversion,[],[f360]) ).
cnf(s3,plain,
( spl33_1
| spl33_5 ),
inference(sat_conversion,[],[f377]) ).
cnf(s5,plain,
~ spl33_1,
inference(sat_conversion,[],[f416]) ).
cnf(s6,plain,
( spl33_8
| ~ spl33_9 ),
inference(sat_conversion,[],[f474]) ).
cnf(s10,plain,
( spl33_15
| spl33_16 ),
inference(sat_conversion,[],[f512]) ).
cnf(s13,plain,
spl33_9,
inference(sat_conversion,[],[f563]) ).
cnf(s14,plain,
spl33_3,
inference(sat_conversion,[],[f595]) ).
cnf(s15,plain,
spl33_6,
inference(sat_conversion,[],[f597]) ).
cnf(s22,plain,
( spl33_1
| ~ spl33_3
| ~ spl33_15 ),
inference(sat_conversion,[],[f664]) ).
cnf(s28,plain,
spl33_28,
inference(sat_conversion,[],[f828]) ).
cnf(s31,plain,
spl33_31,
inference(sat_conversion,[],[f841]) ).
cnf(s32,plain,
( spl33_1
| ~ spl33_2
| ~ spl33_3
| ~ spl33_5
| ~ spl33_6
| ~ spl33_8
| ~ spl33_16
| ~ spl33_28
| ~ spl33_31 ),
inference(sat_conversion,[],[f999]) ).
cnf(s40,plain,
spl33_8,
inference(rat,[],[s6,s13]) ).
cnf(s41,plain,
~ spl33_15,
inference(rat,[],[s22,s14,s5]) ).
cnf(s43,plain,
spl33_16,
inference(rat,[],[s10,s41]) ).
cnf(s45,plain,
spl33_5,
inference(rat,[],[s3,s5]) ).
cnf(s46,plain,
~ spl33_2,
inference(rat,[],[s32,s31,s28,s43,s40,s15,s5,s14,s45]) ).
cnf(s48,plain,
$false,
inference(rat,[],[s1,s46,s5]) ).
fof(f1000,plain,
$false,
inference(avatar_sat_refutation,[],[s48]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU385+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.11/0.38 % Computer : n011.cluster.edu
% 0.11/0.38 % Model : x86_64 x86_64
% 0.11/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38 % Memory : 8046.5625MB
% 0.11/0.38 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Mon Sep 28 05:03:16 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.11/0.42 Running first-order theorem proving
% 0.11/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
% 8.70/2.06 % (3030398)Detected formulas, will run a generic FOF schedule.
% 8.70/2.06 % (3030405)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=1144303432:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 8.70/2.06 % (3030404)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=302424538:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 8.70/2.06 % (3030403)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=1702792033:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 8.70/2.06 % (3030409)dis-21_1_sil=8000:lcm=predicate:random_seed=4006586642: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)
% 8.70/2.06 % (3030408)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=2489377210:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 8.70/2.06 % (3030407)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=3625927640:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 8.70/2.06 % (3030406)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2385312453:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 8.70/2.06 % (3030406)Refutation not found, incomplete strategy
% 8.70/2.06 % (3030406)------------------------------
% 8.70/2.06 % (3030406)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.70/2.06 % (3030406)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.70/2.06 % (3030406)CaDiCaL version: 2.1.3
% 8.70/2.06 % (3030406)Termination reason: Refutation not found, incomplete strategy
% 8.70/2.06 % (3030406)Time elapsed: 0.003 s
% 8.70/2.06 % (3030406)Peak memory usage: 88 MB
% 8.70/2.06 % (3030406)Instructions burned: 2 (million)
% 8.70/2.06 % (3030407)Instruction limit reached!
% 8.70/2.06 % (3030407)------------------------------
% 8.70/2.06 % (3030407)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.70/2.06 % (3030407)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.70/2.06 % (3030407)CaDiCaL version: 2.1.3
% 8.70/2.06 % (3030407)Termination reason: Instruction limit
% 8.70/2.06 % (3030407)Termination phase: Saturation
% 8.70/2.06 % (3030407)Time elapsed: 0.063 s
% 8.70/2.06 % (3030407)Peak memory usage: 88 MB
% 8.70/2.06 % (3030407)Instructions burned: 120 (million)
% 8.70/2.06 % (3030409)Instruction limit reached!
% 8.70/2.06 % (3030409)------------------------------
% 8.70/2.06 % (3030409)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.70/2.06 % (3030409)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.70/2.06 % (3030409)CaDiCaL version: 2.1.3
% 8.70/2.06 % (3030409)Termination reason: Instruction limit
% 8.70/2.06 % (3030409)Termination phase: Saturation
% 8.70/2.06 % (3030409)Time elapsed: 0.075 s
% 8.70/2.06 % (3030409)Peak memory usage: 92 MB
% 8.70/2.06 % (3030409)Instructions burned: 130 (million)
% 8.70/2.06 % (3030408)Instruction limit reached!
% 8.70/2.06 % (3030408)------------------------------
% 8.70/2.06 % (3030408)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.70/2.06 % (3030408)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.70/2.06 % (3030408)CaDiCaL version: 2.1.3
% 8.70/2.06 % (3030408)Termination reason: Instruction limit
% 8.70/2.06 % (3030408)Termination phase: Saturation
% 8.70/2.06 % (3030408)Time elapsed: 0.096 s
% 8.70/2.06 % (3030408)Peak memory usage: 89 MB
% 8.70/2.06 % (3030408)Instructions burned: 140 (million)
% 8.70/2.06 % (3030417)lrs+10_1_sil=8000:sp=occurrence:random_seed=164761818:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 8.70/2.06 % (3030418)lrs+10_1_sil=32000:urr=on:br=off:random_seed=4147258918:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 8.70/2.06 % (3030406)------------------------------
% 8.70/2.06 % (3030406)------------------------------
% 8.70/2.06 % (3030418)Refutation not found, incomplete strategy
% 8.70/2.06 % (3030418)------------------------------
% 8.70/2.06 % (3030418)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.70/2.06 % (3030418)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.70/2.06 % (3030418)CaDiCaL version: 2.1.3
% 8.70/2.06 % (3030418)Termination reason: Refutation not found, incomplete strategy
% 8.70/2.06 % (3030418)Time elapsed: 0.020 s
% 8.70/2.06 % (3030418)Peak memory usage: 89 MB
% 8.70/2.06 % (3030418)Instructions burned: 32 (million)
% 8.70/2.06 % (3030419)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1184098673:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 8.70/2.06 % (3030417)Instruction limit reached!
% 8.70/2.06 % (3030417)------------------------------
% 8.70/2.06 % (3030417)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.70/2.06 % (3030417)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.70/2.06 % (3030417)CaDiCaL version: 2.1.3
% 8.70/2.06 % (3030417)Termination reason: Instruction limit
% 8.70/2.06 % (3030417)Termination phase: Saturation
% 8.70/2.06 % (3030417)Time elapsed: 0.185 s
% 8.70/2.06 % (3030417)Peak memory usage: 93 MB
% 8.70/2.06 % (3030417)Instructions burned: 285 (million)
% 8.70/2.06 % (3030422)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=1518136716:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 8.70/2.06 % (3030419)Instruction limit reached!
% 8.70/2.06 % (3030419)------------------------------
% 8.70/2.06 % (3030419)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.70/2.06 % (3030419)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.70/2.06 % (3030419)CaDiCaL version: 2.1.3
% 8.70/2.06 % (3030419)Termination reason: Instruction limit
% 8.70/2.06 % (3030419)Termination phase: Saturation
% 8.70/2.06 % (3030419)Time elapsed: 0.210 s
% 8.70/2.06 % (3030419)Peak memory usage: 91 MB
% 8.70/2.06 % (3030419)Instructions burned: 326 (million)
% 8.70/2.06 % (3030418)------------------------------
% 8.70/2.06 % (3030418)------------------------------
% 8.70/2.06 % (3030424)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1869955418:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 8.70/2.06 % (3030422)Instruction limit reached!
% 8.70/2.06 % (3030422)------------------------------
% 8.70/2.06 % (3030422)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.70/2.06 % (3030422)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.70/2.06 % (3030422)CaDiCaL version: 2.1.3
% 8.70/2.06 % (3030422)Termination reason: Instruction limit
% 8.70/2.06 % (3030422)Termination phase: Saturation
% 8.70/2.06 % (3030422)Time elapsed: 0.147 s
% 8.70/2.06 % (3030422)Peak memory usage: 92 MB
% 8.70/2.06 % (3030422)Instructions burned: 248 (million)
% 8.70/2.06 % (3030424)Refutation not found, incomplete strategy
% 8.70/2.06 % (3030424)------------------------------
% 8.70/2.06 % (3030424)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.70/2.06 % (3030424)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.70/2.06 % (3030424)CaDiCaL version: 2.1.3
% 8.70/2.06 % (3030424)Termination reason: Refutation not found, incomplete strategy
% 8.70/2.06 % (3030424)Time elapsed: 0.006 s
% 8.70/2.06 % (3030424)Peak memory usage: 89 MB
% 8.70/2.06 % (3030424)Instructions burned: 8 (million)
% 8.70/2.06 % (3030426)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2857489998:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 8.70/2.06 % (3030427)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2694457103:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 8.70/2.06 % (3030427)Instruction limit reached!
% 8.70/2.06 % (3030427)------------------------------
% 8.70/2.06 % (3030427)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.70/2.06 % (3030427)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.70/2.06 % (3030427)CaDiCaL version: 2.1.3
% 8.70/2.06 % (3030427)Termination reason: Instruction limit
% 8.70/2.06 % (3030427)Termination phase: Saturation
% 8.70/2.06 % (3030427)Time elapsed: 0.079 s
% 8.70/2.06 % (3030427)Peak memory usage: 91 MB
% 8.70/2.06 % (3030427)Instructions burned: 113 (million)
% 8.70/2.06 % (3030429)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3140951384:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 8.70/2.06 % (3030403)First to succeed.
% 8.70/2.06 % (3030403)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3030398"
% 8.70/2.06 % (3030429)Instruction limit reached!
% 8.70/2.06 % (3030429)------------------------------
% 8.70/2.06 % (3030429)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.70/2.06 % (3030429)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.70/2.06 % (3030429)CaDiCaL version: 2.1.3
% 8.70/2.06 % (3030429)Termination reason: Instruction limit
% 8.70/2.06 % (3030429)Termination phase: Saturation
% 8.70/2.06 % (3030429)Time elapsed: 0.069 s
% 8.70/2.06 % (3030429)Peak memory usage: 89 MB
% 8.70/2.06 % (3030429)Instructions burned: 127 (million)
% 8.70/2.06 % (3030424)------------------------------
% 8.70/2.06 % (3030424)------------------------------
% 8.70/2.06 % (3030433)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=4115974132:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 8.70/2.06 % (3030434)lrs+10_1_sil=8000:sp=occurrence:random_seed=1809097409:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 8.70/2.06 % (3030433)Instruction limit reached!
% 8.70/2.06 % (3030433)------------------------------
% 8.70/2.06 % (3030433)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.70/2.06 % (3030433)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.70/2.06 % (3030433)CaDiCaL version: 2.1.3
% 8.70/2.06 % (3030433)Termination reason: Instruction limit
% 8.70/2.06 % (3030433)Termination phase: Saturation
% 8.70/2.06 % (3030433)Time elapsed: 0.071 s
% 8.70/2.06 % (3030433)Peak memory usage: 89 MB
% 8.70/2.06 % (3030433)Instructions burned: 115 (million)
% 8.70/2.06 % (3030435)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=1749069974:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 8.70/2.06 % (3030435)Refutation not found, incomplete strategy
% 8.70/2.06 % (3030435)------------------------------
% 8.70/2.06 % (3030435)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 8.70/2.06 % (3030435)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 8.70/2.06 % (3030435)CaDiCaL version: 2.1.3
% 8.70/2.06 % (3030435)Termination reason: Refutation not found, incomplete strategy
% 8.70/2.06 % (3030435)Time elapsed: 0.006 s
% 8.70/2.06 % (3030435)Peak memory usage: 89 MB
% 8.70/2.06 % (3030435)Instructions burned: 8 (million)
% 8.70/2.06 % (3030403)Refutation found. Thanks to Tanya!
% 8.70/2.06 % SZS status Theorem for theBenchmark
% 8.70/2.06 % SZS output start Proof for theBenchmark
% See solution above
% 9.04/2.25 % (3030403)------------------------------
% 9.04/2.25 % (3030403)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 9.04/2.25 % (3030403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 9.04/2.25 % (3030403)CaDiCaL version: 2.1.3
% 9.04/2.25 % (3030403)Termination reason: Refutation
% 9.04/2.25 % (3030403)Time elapsed: 0.760 s
% 9.04/2.25 % (3030403)Peak memory usage: 130 MB
% 9.04/2.25 % (3030403)Instructions burned: 1089 (million)
% 9.04/2.25 % (3030403)------------------------------
% 9.04/2.25 % (3030403)------------------------------
% 9.04/2.25 % (3030398)Success in time 1.198 s
% 9.04/2.25 % Vampire exiting
%------------------------------------------------------------------------------