%------------------------------------------------------------------------------
% File : Vampire-SAT---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 SAT
% Computer : n016.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:53:05 PM UTC 2026
% Result : Theorem 17.98s 4.40s
% Output : Refutation 17.98s
% Verified :
% SZS Type : Refutation
% Derivation depth : 37
% Number of leaves : 27
% Syntax : Number of formulae : 245 ( 60 unt; 7 def)
% Number of atoms : 1023 ( 162 equ)
% Maximal formula atoms : 22 ( 4 avg)
% Number of connectives : 1291 ( 513 ~; 589 |; 144 &)
% ( 10 <=>; 35 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 6 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 19 ( 17 usr; 1 prp; 0-4 aty)
% Number of functors : 27 ( 27 usr; 10 con; 0-4 aty)
% Number of variables : 411 ( 387 !; 24 ?)
% 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(f27,axiom,
! [X0,X1,X2,X3] :
( ( ~ empty(X0)
& ~ empty_carrier(X1)
& one_sorted_str(X1)
& function(X2)
& quasi_total(X2,X0,the_carrier(X1))
& relation_of2(X2,X0,the_carrier(X1))
& element(X3,X0) )
=> element(apply_on_set_and_struct2(X0,X1,X2,X3),the_carrier(X1)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k7_yellow_2) ).
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(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(f54,axiom,
! [X0,X1] :
? [X2] :
( relation_of2(X2,X0,X1)
& relation(X2)
& function(X2)
& quasi_total(X2,X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rc1_funct_2) ).
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(f67,axiom,
! [X0,X1,X2,X3] :
( ( ~ empty(X0)
& ~ empty_carrier(X1)
& one_sorted_str(X1)
& function(X2)
& quasi_total(X2,X0,the_carrier(X1))
& relation_of2(X2,X0,the_carrier(X1))
& element(X3,X0) )
=> apply_on_set_and_struct2(X0,X1,X2,X3) = apply(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k7_yellow_2) ).
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(f79,axiom,
! [X0,X1] :
~ ( in(X0,X1)
& empty(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
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(f120,plain,
! [X0,X1,X2,X3] :
( element(apply_on_set_and_struct2(X0,X1,X2,X3),the_carrier(X1))
| empty(X0)
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ function(X2)
| ~ quasi_total(X2,X0,the_carrier(X1))
| ~ relation_of2(X2,X0,the_carrier(X1))
| ~ element(X3,X0) ),
inference(ennf_transformation,[],[f27]) ).
fof(f121,plain,
! [X0,X1,X2,X3] :
( element(apply_on_set_and_struct2(X0,X1,X2,X3),the_carrier(X1))
| empty(X0)
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ function(X2)
| ~ quasi_total(X2,X0,the_carrier(X1))
| ~ relation_of2(X2,X0,the_carrier(X1))
| ~ element(X3,X0) ),
inference(flattening,[],[f120]) ).
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(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(f153,plain,
! [X0,X1,X2,X3] :
( apply_on_set_and_struct2(X0,X1,X2,X3) = apply(X2,X3)
| empty(X0)
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ function(X2)
| ~ quasi_total(X2,X0,the_carrier(X1))
| ~ relation_of2(X2,X0,the_carrier(X1))
| ~ element(X3,X0) ),
inference(ennf_transformation,[],[f67]) ).
fof(f154,plain,
! [X0,X1,X2,X3] :
( apply_on_set_and_struct2(X0,X1,X2,X3) = apply(X2,X3)
| empty(X0)
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ function(X2)
| ~ quasi_total(X2,X0,the_carrier(X1))
| ~ relation_of2(X2,X0,the_carrier(X1))
| ~ element(X3,X0) ),
inference(flattening,[],[f153]) ).
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(f167,plain,
! [X0,X1] :
( ~ in(X0,X1)
| ~ empty(X1) ),
inference(ennf_transformation,[],[f79]) ).
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(f186,plain,
! [X0,X1] :
( relation_of2(sK13(X0,X1),X0,X1)
& relation(sK13(X0,X1))
& function(sK13(X0,X1))
& quasi_total(sK13(X0,X1),X0,X1) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(X2,sK13(X0,X1))],[f54]) ).
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(f241,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,[],[f118]) ).
fof(f243,plain,
! [X2,X3,X0,X1] :
( element(apply_on_set_and_struct2(X0,X1,X2,X3),the_carrier(X1))
| empty(X0)
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ function(X2)
| ~ quasi_total(X2,X0,the_carrier(X1))
| ~ relation_of2(X2,X0,the_carrier(X1))
| ~ element(X3,X0) ),
inference(cnf_transformation,[],[f121]) ).
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(f249,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,[],[f127]) ).
fof(f250,plain,
! [X0,X1] :
( function(the_mapping(X0,X1))
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(cnf_transformation,[],[f127]) ).
fof(f266,plain,
! [X0] :
( ~ empty(the_carrier(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f134]) ).
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(f282,plain,
! [X0,X1] : quasi_total(sK13(X0,X1),X0,X1),
inference(cnf_transformation,[],[f186]) ).
fof(f283,plain,
! [X0,X1] : function(sK13(X0,X1)),
inference(cnf_transformation,[],[f186]) ).
fof(f285,plain,
! [X0,X1] : relation_of2(sK13(X0,X1),X0,X1),
inference(cnf_transformation,[],[f186]) ).
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(f308,plain,
! [X2,X3,X0,X1] :
( ~ quasi_total(X2,X0,the_carrier(X1))
| empty(X0)
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ function(X2)
| apply_on_set_and_struct2(X0,X1,X2,X3) = apply(X2,X3)
| ~ relation_of2(X2,X0,the_carrier(X1))
| ~ element(X3,X0) ),
inference(cnf_transformation,[],[f154]) ).
fof(f309,plain,
! [X2,X0,X1] :
( ~ relation_of2_as_subset(X2,X0,X1)
| relation_of2(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(f329,plain,
! [X0,X1] :
( ~ in(X0,X1)
| ~ empty(X1) ),
inference(cnf_transformation,[],[f167]) ).
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(f370,plain,
( rel_str(sK24)
| ~ one_sorted_str(sK23) ),
inference(resolution,[],[f245,f314]) ).
fof(f375,plain,
rel_str(sK24),
inference(forward_subsumption_resolution,[],[f370,f312]) ).
fof(f376,plain,
one_sorted_str(sK24),
inference(resolution,[],[f375,f244]) ).
fof(f378,plain,
( ~ empty(sF32)
| empty_carrier(sK24)
| ~ one_sorted_str(sK24) ),
inference(superposition,[],[f266,f347]) ).
fof(f379,plain,
( ~ empty(sF32)
| ~ one_sorted_str(sK24) ),
inference(forward_subsumption_resolution,[],[f378,f316]) ).
fof(f380,plain,
~ empty(sF32),
inference(forward_subsumption_resolution,[],[f379,f376]) ).
fof(f410,plain,
( in(sK27,sF31)
| empty(sF31) ),
inference(resolution,[],[f323,f345]) ).
fof(f443,plain,
! [X2,X0,X1] :
( ~ relation_of2_as_subset(X0,X1,X2)
| relation(X0) ),
inference(resolution,[],[f246,f206]) ).
fof(f469,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(f470,plain,
! [X0] :
( relation_of2_as_subset(the_mapping(X0,sF28),sF31,the_carrier(X0))
| ~ one_sorted_str(X0)
| ~ net_str(sF28,X0) ),
inference(superposition,[],[f248,f344]) ).
fof(f471,plain,
! [X0] :
( relation_of2_as_subset(the_mapping(X0,sK24),sF32,the_carrier(X0))
| ~ one_sorted_str(X0)
| ~ net_str(sK24,X0) ),
inference(superposition,[],[f248,f347]) ).
fof(f478,plain,
! [X0] :
( quasi_total(the_mapping(X0,sF28),sF31,the_carrier(X0))
| ~ one_sorted_str(X0)
| ~ net_str(sF28,X0) ),
inference(superposition,[],[f249,f344]) ).
fof(f479,plain,
! [X0] :
( quasi_total(the_mapping(X0,sK24),sF32,the_carrier(X0))
| ~ one_sorted_str(X0)
| ~ net_str(sK24,X0) ),
inference(superposition,[],[f249,f347]) ).
fof(f541,plain,
! [X0] :
( ~ relation(X0)
| apply(X0,sK27) = apply(relation_dom_restriction(X0,sF31),sK27)
| ~ function(X0)
| empty(sF31) ),
inference(resolution,[],[f328,f410]) ).
fof(f543,plain,
( ~ sP1(sK23,sF28,sK25,sK24)
| sP0(sK24,sK25,sF28,sK23) ),
inference(superposition,[],[f333,f337]) ).
fof(f592,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(f594,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,[],[f592,f313]) ).
fof(f595,plain,
( net_str(sF28,sK23)
| empty_carrier(sK24)
| ~ net_str(sK24,sK23)
| ~ element(sK25,the_carrier(sK24)) ),
inference(forward_subsumption_resolution,[],[f594,f312]) ).
fof(f596,plain,
( net_str(sF28,sK23)
| ~ net_str(sK24,sK23)
| ~ element(sK25,the_carrier(sK24)) ),
inference(forward_subsumption_resolution,[],[f595,f316]) ).
fof(f597,plain,
( net_str(sF28,sK23)
| ~ element(sK25,the_carrier(sK24)) ),
inference(forward_subsumption_resolution,[],[f596,f314]) ).
fof(f598,plain,
( ~ element(sK25,sF32)
| net_str(sF28,sK23) ),
inference(forward_demodulation,[],[f597,f347]) ).
fof(f599,plain,
net_str(sF28,sK23),
inference(forward_subsumption_resolution,[],[f598,f349]) ).
fof(f600,plain,
( rel_str(sF28)
| ~ one_sorted_str(sK23) ),
inference(resolution,[],[f599,f245]) ).
fof(f601,plain,
rel_str(sF28),
inference(forward_subsumption_resolution,[],[f600,f312]) ).
fof(f603,plain,
( strict_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,[],[f241,f337]) ).
fof(f605,plain,
( strict_net_str(sF28,sK23)
| ~ one_sorted_str(sK23)
| empty_carrier(sK24)
| ~ net_str(sK24,sK23)
| ~ element(sK25,the_carrier(sK24)) ),
inference(forward_subsumption_resolution,[],[f603,f313]) ).
fof(f607,plain,
( strict_net_str(sF28,sK23)
| empty_carrier(sK24)
| ~ net_str(sK24,sK23)
| ~ element(sK25,the_carrier(sK24)) ),
inference(forward_subsumption_resolution,[],[f605,f312]) ).
fof(f608,plain,
( strict_net_str(sF28,sK23)
| ~ net_str(sK24,sK23)
| ~ element(sK25,the_carrier(sK24)) ),
inference(forward_subsumption_resolution,[],[f607,f316]) ).
fof(f609,plain,
( strict_net_str(sF28,sK23)
| ~ element(sK25,the_carrier(sK24)) ),
inference(forward_subsumption_resolution,[],[f608,f314]) ).
fof(f610,plain,
( ~ element(sK25,sF32)
| strict_net_str(sF28,sK23) ),
inference(forward_demodulation,[],[f609,f347]) ).
fof(f611,plain,
strict_net_str(sF28,sK23),
inference(forward_subsumption_resolution,[],[f610,f349]) ).
fof(f612,plain,
one_sorted_str(sF28),
inference(resolution,[],[f601,f244]) ).
fof(f633,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(f634,plain,
( ~ empty_carrier(sF28)
| ~ one_sorted_str(sK23)
| empty_carrier(sK24)
| ~ directed_relstr(sK24)
| ~ net_str(sK24,sK23)
| ~ element(sK25,the_carrier(sK24)) ),
inference(forward_subsumption_resolution,[],[f633,f313]) ).
fof(f635,plain,
( ~ empty_carrier(sF28)
| empty_carrier(sK24)
| ~ directed_relstr(sK24)
| ~ net_str(sK24,sK23)
| ~ element(sK25,the_carrier(sK24)) ),
inference(forward_subsumption_resolution,[],[f634,f312]) ).
fof(f636,plain,
( ~ empty_carrier(sF28)
| ~ directed_relstr(sK24)
| ~ net_str(sK24,sK23)
| ~ element(sK25,the_carrier(sK24)) ),
inference(forward_subsumption_resolution,[],[f635,f316]) ).
fof(f637,plain,
( ~ empty_carrier(sF28)
| ~ net_str(sK24,sK23)
| ~ element(sK25,the_carrier(sK24)) ),
inference(forward_subsumption_resolution,[],[f636,f315]) ).
fof(f638,plain,
( ~ empty_carrier(sF28)
| ~ element(sK25,the_carrier(sK24)) ),
inference(forward_subsumption_resolution,[],[f637,f314]) ).
fof(f639,plain,
( ~ element(sK25,sF32)
| ~ empty_carrier(sF28) ),
inference(forward_demodulation,[],[f638,f347]) ).
fof(f640,plain,
~ empty_carrier(sF28),
inference(forward_subsumption_resolution,[],[f639,f349]) ).
fof(f656,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(f657,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(f659,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,[],[f657,f316]) ).
fof(f660,plain,
! [X0,X1] :
( ~ element(X0,sF31)
| apply_netmap(X1,sF28,X0) = apply_on_structs(sF28,X1,the_mapping(X1,sF28),X0)
| ~ net_str(sF28,X1)
| empty_carrier(X1)
| ~ one_sorted_str(X1) ),
inference(forward_subsumption_resolution,[],[f656,f640]) ).
fof(f716,plain,
! [X2,X3,X0,X1] :
( empty(X0)
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ function(X2)
| ~ quasi_total(X2,X0,the_carrier(X1))
| ~ relation_of2(X2,X0,the_carrier(X1))
| ~ element(X3,X0)
| in(apply_on_set_and_struct2(X0,X1,X2,X3),the_carrier(X1))
| empty(the_carrier(X1)) ),
inference(resolution,[],[f243,f323]) ).
fof(f722,plain,
! [X2,X3,X0,X1] :
( in(apply_on_set_and_struct2(X0,X1,X2,X3),the_carrier(X1))
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ function(X2)
| ~ quasi_total(X2,X0,the_carrier(X1))
| ~ relation_of2(X2,X0,the_carrier(X1))
| ~ element(X3,X0)
| empty(X0) ),
inference(forward_subsumption_resolution,[],[f716,f266]) ).
fof(f728,plain,
! [X2,X0,X1] :
( ~ quasi_total(X0,X1,sF31)
| empty(X1)
| empty_carrier(sF28)
| ~ one_sorted_str(sF28)
| ~ function(X0)
| apply_on_set_and_struct2(X1,sF28,X0,X2) = apply(X0,X2)
| ~ relation_of2(X0,X1,sF31)
| ~ element(X2,X1) ),
inference(superposition,[],[f308,f344]) ).
fof(f733,plain,
! [X2,X0,X1] :
( ~ quasi_total(X0,X1,sF31)
| empty(X1)
| ~ one_sorted_str(sF28)
| ~ function(X0)
| apply_on_set_and_struct2(X1,sF28,X0,X2) = apply(X0,X2)
| ~ relation_of2(X0,X1,sF31)
| ~ element(X2,X1) ),
inference(forward_subsumption_resolution,[],[f728,f640]) ).
fof(f738,plain,
! [X2,X0,X1] :
( ~ quasi_total(X0,X1,sF31)
| empty(X1)
| ~ function(X0)
| apply_on_set_and_struct2(X1,sF28,X0,X2) = apply(X0,X2)
| ~ relation_of2(X0,X1,sF31)
| ~ element(X2,X1) ),
inference(forward_subsumption_resolution,[],[f733,f612]) ).
fof(f776,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(f777,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(X0,X2) = apply_on_structs(sK24,X1,X0,X2)
| ~ relation_of2(X0,sF32,the_carrier(X1))
| ~ element(X2,sF32) ),
inference(superposition,[],[f306,f347]) ).
fof(f784,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(X0,X2) = apply_on_structs(sK24,X1,X0,X2)
| ~ relation_of2(X0,sF32,the_carrier(X1))
| ~ element(X2,sF32) ),
inference(forward_subsumption_resolution,[],[f777,f316]) ).
fof(f785,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) ),
inference(forward_subsumption_resolution,[],[f776,f640]) ).
fof(f791,plain,
! [X2,X0,X1] :
( ~ quasi_total(X0,sF32,the_carrier(X1))
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ function(X0)
| apply(X0,X2) = apply_on_structs(sK24,X1,X0,X2)
| ~ relation_of2(X0,sF32,the_carrier(X1))
| ~ element(X2,sF32) ),
inference(forward_subsumption_resolution,[],[f784,f376]) ).
fof(f792,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) ),
inference(forward_subsumption_resolution,[],[f785,f612]) ).
fof(f897,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,[],[f659,f348]) ).
fof(f900,plain,
! [X0] :
( ~ net_str(sF28,X0)
| apply_netmap(X0,sF28,sK27) = apply_on_structs(sF28,X0,the_mapping(X0,sF28),sK27)
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(resolution,[],[f660,f345]) ).
fof(f917,plain,
! [X0,X1] :
( empty(X0)
| ~ function(sK13(X0,sF31))
| apply_on_set_and_struct2(X0,sF28,sK13(X0,sF31),X1) = apply(sK13(X0,sF31),X1)
| ~ relation_of2(sK13(X0,sF31),X0,sF31)
| ~ element(X1,X0) ),
inference(resolution,[],[f738,f282]) ).
fof(f918,plain,
! [X0,X1] :
( empty(X0)
| apply_on_set_and_struct2(X0,sF28,sK13(X0,sF31),X1) = apply(sK13(X0,sF31),X1)
| ~ relation_of2(sK13(X0,sF31),X0,sF31)
| ~ element(X1,X0) ),
inference(forward_subsumption_resolution,[],[f917,f283]) ).
fof(f919,plain,
! [X0,X1] :
( ~ element(X1,X0)
| apply_on_set_and_struct2(X0,sF28,sK13(X0,sF31),X1) = apply(sK13(X0,sF31),X1)
| empty(X0) ),
inference(forward_subsumption_resolution,[],[f918,f285]) ).
fof(f973,plain,
! [X0,X1] :
( relation(the_mapping(X0,X1))
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(resolution,[],[f443,f248]) ).
fof(f1112,plain,
( sP0(sK24,sK25,sF28,sK23)
| ~ 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) ),
inference(resolution,[],[f543,f230]) ).
fof(f1113,plain,
( sP0(sK24,sK25,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) ),
inference(forward_subsumption_resolution,[],[f1112,f611]) ).
fof(f1114,plain,
( sP0(sK24,sK25,sF28,sK23)
| ~ element(sK25,the_carrier(sK24))
| empty_carrier(sK24)
| ~ net_str(sK24,sK23)
| empty_carrier(sK23)
| ~ one_sorted_str(sK23) ),
inference(forward_subsumption_resolution,[],[f1113,f599]) ).
fof(f1115,plain,
( sP0(sK24,sK25,sF28,sK23)
| ~ element(sK25,the_carrier(sK24))
| ~ net_str(sK24,sK23)
| empty_carrier(sK23)
| ~ one_sorted_str(sK23) ),
inference(forward_subsumption_resolution,[],[f1114,f316]) ).
fof(f1116,plain,
( sP0(sK24,sK25,sF28,sK23)
| ~ element(sK25,the_carrier(sK24))
| empty_carrier(sK23)
| ~ one_sorted_str(sK23) ),
inference(forward_subsumption_resolution,[],[f1115,f314]) ).
fof(f1117,plain,
( sP0(sK24,sK25,sF28,sK23)
| ~ element(sK25,the_carrier(sK24))
| ~ one_sorted_str(sK23) ),
inference(forward_subsumption_resolution,[],[f1116,f313]) ).
fof(f1118,plain,
( sP0(sK24,sK25,sF28,sK23)
| ~ element(sK25,the_carrier(sK24)) ),
inference(forward_subsumption_resolution,[],[f1117,f312]) ).
fof(f1119,plain,
( ~ element(sK25,sF32)
| sP0(sK24,sK25,sF28,sK23) ),
inference(forward_demodulation,[],[f1118,f347]) ).
fof(f1120,plain,
sP0(sK24,sK25,sF28,sK23),
inference(forward_subsumption_resolution,[],[f1119,f349]) ).
fof(f1121,plain,
the_mapping(sK23,sF28) = partfun_dom_restriction(the_carrier(sK24),the_carrier(sK23),the_mapping(sK23,sK24),the_carrier(sF28)),
inference(resolution,[],[f1120,f220]) ).
fof(f1132,plain,
the_mapping(sK23,sF28) = partfun_dom_restriction(the_carrier(sK24),the_carrier(sK23),the_mapping(sK23,sK24),sF31),
inference(forward_demodulation,[],[f1121,f344]) ).
fof(f1135,plain,
the_mapping(sK23,sF28) = partfun_dom_restriction(sF32,the_carrier(sK23),the_mapping(sK23,sK24),sF31),
inference(forward_demodulation,[],[f1132,f347]) ).
fof(f1177,plain,
! [X0] :
( relation_of2(the_mapping(X0,sF28),sF31,the_carrier(X0))
| ~ net_str(sF28,X0)
| ~ one_sorted_str(X0) ),
inference(resolution,[],[f470,f309]) ).
fof(f1187,plain,
! [X0] :
( relation_of2(the_mapping(X0,sK24),sF32,the_carrier(X0))
| ~ net_str(sK24,X0)
| ~ one_sorted_str(X0) ),
inference(resolution,[],[f471,f309]) ).
fof(f1204,plain,
! [X0,X1] :
( ~ one_sorted_str(X0)
| ~ net_str(sF28,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) ),
inference(resolution,[],[f478,f792]) ).
fof(f1218,plain,
! [X0,X1] :
( ~ one_sorted_str(X0)
| ~ net_str(sF28,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) ),
inference(duplicate_literal_removal,[],[f1204]) ).
fof(f1227,plain,
! [X0,X1] :
( ~ one_sorted_str(X0)
| ~ net_str(sF28,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) ),
inference(forward_subsumption_resolution,[],[f1218,f250]) ).
fof(f1235,plain,
! [X0,X1] :
( ~ element(X1,sF31)
| ~ net_str(sF28,X0)
| empty_carrier(X0)
| apply(the_mapping(X0,sF28),X1) = apply_on_structs(sF28,X0,the_mapping(X0,sF28),X1)
| ~ one_sorted_str(X0) ),
inference(forward_subsumption_resolution,[],[f1227,f1177]) ).
fof(f1236,plain,
! [X0,X1] :
( ~ one_sorted_str(X0)
| ~ net_str(sK24,X0)
| 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) ),
inference(resolution,[],[f479,f791]) ).
fof(f1250,plain,
! [X0,X1] :
( ~ one_sorted_str(X0)
| ~ net_str(sK24,X0)
| empty_carrier(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) ),
inference(duplicate_literal_removal,[],[f1236]) ).
fof(f1259,plain,
! [X0,X1] :
( ~ one_sorted_str(X0)
| ~ net_str(sK24,X0)
| empty_carrier(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) ),
inference(forward_subsumption_resolution,[],[f1250,f250]) ).
fof(f1267,plain,
! [X0,X1] :
( ~ element(X1,sF32)
| ~ net_str(sK24,X0)
| empty_carrier(X0)
| apply(the_mapping(X0,sK24),X1) = apply_on_structs(sK24,X0,the_mapping(X0,sK24),X1)
| ~ one_sorted_str(X0) ),
inference(forward_subsumption_resolution,[],[f1259,f1187]) ).
fof(f1339,plain,
! [X2,X0,X1] :
( ~ net_str(X0,X1)
| ~ one_sorted_str(X1)
| ~ function(the_mapping(X1,X0))
| partfun_dom_restriction(the_carrier(X0),the_carrier(X1),the_mapping(X1,X0),X2) = relation_dom_restriction(the_mapping(X1,X0),X2) ),
inference(resolution,[],[f469,f307]) ).
fof(f1345,plain,
! [X2,X0,X1] :
( ~ net_str(X0,X1)
| ~ one_sorted_str(X1)
| partfun_dom_restriction(the_carrier(X0),the_carrier(X1),the_mapping(X1,X0),X2) = relation_dom_restriction(the_mapping(X1,X0),X2) ),
inference(forward_subsumption_resolution,[],[f1339,f250]) ).
fof(f1656,plain,
! [X2,X0,X1] :
( in(apply_on_set_and_struct2(X0,sF28,X1,X2),sF31)
| empty_carrier(sF28)
| ~ one_sorted_str(sF28)
| ~ function(X1)
| ~ quasi_total(X1,X0,sF31)
| ~ relation_of2(X1,X0,sF31)
| ~ element(X2,X0)
| empty(X0) ),
inference(superposition,[],[f722,f344]) ).
fof(f1658,plain,
! [X2,X0,X1] :
( in(apply_on_set_and_struct2(X0,sF28,X1,X2),sF31)
| ~ one_sorted_str(sF28)
| ~ function(X1)
| ~ quasi_total(X1,X0,sF31)
| ~ relation_of2(X1,X0,sF31)
| ~ element(X2,X0)
| empty(X0) ),
inference(forward_subsumption_resolution,[],[f1656,f640]) ).
fof(f1659,plain,
! [X2,X0,X1] :
( in(apply_on_set_and_struct2(X0,sF28,X1,X2),sF31)
| ~ function(X1)
| ~ quasi_total(X1,X0,sF31)
| ~ relation_of2(X1,X0,sF31)
| ~ element(X2,X0)
| empty(X0) ),
inference(forward_subsumption_resolution,[],[f1658,f612]) ).
fof(f2208,plain,
( apply_on_set_and_struct2(sF32,sF28,sK13(sF32,sF31),sK27) = apply(sK13(sF32,sF31),sK27)
| empty(sF32) ),
inference(resolution,[],[f919,f348]) ).
fof(f2218,plain,
apply_on_set_and_struct2(sF32,sF28,sK13(sF32,sF31),sK27) = apply(sK13(sF32,sF31),sK27),
inference(forward_subsumption_resolution,[],[f2208,f380]) ).
fof(f2280,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,[],[f897,f314]) ).
fof(f2281,plain,
( apply_netmap(sK23,sK24,sK27) = apply_on_structs(sK24,sK23,the_mapping(sK23,sK24),sK27)
| ~ one_sorted_str(sK23) ),
inference(forward_subsumption_resolution,[],[f2280,f313]) ).
fof(f2282,plain,
apply_netmap(sK23,sK24,sK27) = apply_on_structs(sK24,sK23,the_mapping(sK23,sK24),sK27),
inference(forward_subsumption_resolution,[],[f2281,f312]) ).
fof(f2283,plain,
sF30 = apply_on_structs(sK24,sK23,the_mapping(sK23,sK24),sK27),
inference(forward_demodulation,[],[f2282,f341]) ).
fof(f2284,plain,
( apply_netmap(sK23,sF28,sK27) = apply_on_structs(sF28,sK23,the_mapping(sK23,sF28),sK27)
| empty_carrier(sK23)
| ~ one_sorted_str(sK23) ),
inference(resolution,[],[f900,f599]) ).
fof(f2285,plain,
( apply_netmap(sK23,sF28,sK27) = apply_on_structs(sF28,sK23,the_mapping(sK23,sF28),sK27)
| ~ one_sorted_str(sK23) ),
inference(forward_subsumption_resolution,[],[f2284,f313]) ).
fof(f2286,plain,
apply_netmap(sK23,sF28,sK27) = apply_on_structs(sF28,sK23,the_mapping(sK23,sF28),sK27),
inference(forward_subsumption_resolution,[],[f2285,f312]) ).
fof(f2287,plain,
sF29 = apply_on_structs(sF28,sK23,the_mapping(sK23,sF28),sK27),
inference(forward_demodulation,[],[f2286,f339]) ).
fof(f2536,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) ),
inference(resolution,[],[f1235,f345]) ).
fof(f2546,plain,
! [X0] :
( ~ net_str(sK24,X0)
| empty_carrier(X0)
| apply_on_structs(sK24,X0,the_mapping(X0,sK24),sK27) = apply(the_mapping(X0,sK24),sK27)
| ~ one_sorted_str(X0) ),
inference(resolution,[],[f1267,f348]) ).
fof(f2878,plain,
( in(apply(sK13(sF32,sF31),sK27),sF31)
| ~ function(sK13(sF32,sF31))
| ~ quasi_total(sK13(sF32,sF31),sF32,sF31)
| ~ relation_of2(sK13(sF32,sF31),sF32,sF31)
| ~ element(sK27,sF32)
| empty(sF32) ),
inference(superposition,[],[f1659,f2218]) ).
fof(f2885,plain,
( in(apply(sK13(sF32,sF31),sK27),sF31)
| ~ quasi_total(sK13(sF32,sF31),sF32,sF31)
| ~ relation_of2(sK13(sF32,sF31),sF32,sF31)
| ~ element(sK27,sF32)
| empty(sF32) ),
inference(forward_subsumption_resolution,[],[f2878,f283]) ).
fof(f2890,plain,
( in(apply(sK13(sF32,sF31),sK27),sF31)
| ~ relation_of2(sK13(sF32,sF31),sF32,sF31)
| ~ element(sK27,sF32)
| empty(sF32) ),
inference(forward_subsumption_resolution,[],[f2885,f282]) ).
fof(f2895,plain,
( in(apply(sK13(sF32,sF31),sK27),sF31)
| ~ element(sK27,sF32)
| empty(sF32) ),
inference(forward_subsumption_resolution,[],[f2890,f285]) ).
fof(f2900,plain,
( in(apply(sK13(sF32,sF31),sK27),sF31)
| empty(sF32) ),
inference(forward_subsumption_resolution,[],[f2895,f348]) ).
fof(f2905,plain,
in(apply(sK13(sF32,sF31),sK27),sF31),
inference(forward_subsumption_resolution,[],[f2900,f380]) ).
fof(f2954,plain,
~ empty(sF31),
inference(resolution,[],[f2905,f329]) ).
fof(f3510,plain,
! [X0,X1] :
( ~ one_sorted_str(X0)
| ~ net_str(X1,X0)
| apply(the_mapping(X0,X1),sK27) = apply(relation_dom_restriction(the_mapping(X0,X1),sF31),sK27)
| ~ function(the_mapping(X0,X1))
| empty(sF31) ),
inference(resolution,[],[f973,f541]) ).
fof(f3515,plain,
! [X0,X1] :
( ~ one_sorted_str(X0)
| ~ net_str(X1,X0)
| apply(the_mapping(X0,X1),sK27) = apply(relation_dom_restriction(the_mapping(X0,X1),sF31),sK27)
| ~ function(the_mapping(X0,X1)) ),
inference(forward_subsumption_resolution,[],[f3510,f2954]) ).
fof(f3518,plain,
! [X0,X1] :
( ~ net_str(X1,X0)
| ~ one_sorted_str(X0)
| apply(the_mapping(X0,X1),sK27) = apply(relation_dom_restriction(the_mapping(X0,X1),sF31),sK27) ),
inference(forward_subsumption_resolution,[],[f3515,f250]) ).
fof(f4617,plain,
! [X0] :
( ~ one_sorted_str(sK23)
| partfun_dom_restriction(the_carrier(sK24),the_carrier(sK23),the_mapping(sK23,sK24),X0) = relation_dom_restriction(the_mapping(sK23,sK24),X0) ),
inference(resolution,[],[f1345,f314]) ).
fof(f4627,plain,
! [X0] : partfun_dom_restriction(the_carrier(sK24),the_carrier(sK23),the_mapping(sK23,sK24),X0) = relation_dom_restriction(the_mapping(sK23,sK24),X0),
inference(forward_subsumption_resolution,[],[f4617,f312]) ).
fof(f4632,plain,
! [X0] : relation_dom_restriction(the_mapping(sK23,sK24),X0) = partfun_dom_restriction(sF32,the_carrier(sK23),the_mapping(sK23,sK24),X0),
inference(forward_demodulation,[],[f4627,f347]) ).
fof(f4661,plain,
the_mapping(sK23,sF28) = relation_dom_restriction(the_mapping(sK23,sK24),sF31),
inference(superposition,[],[f1135,f4632]) ).
fof(f8887,plain,
( ~ one_sorted_str(sK23)
| apply(the_mapping(sK23,sK24),sK27) = apply(relation_dom_restriction(the_mapping(sK23,sK24),sF31),sK27) ),
inference(resolution,[],[f3518,f314]) ).
fof(f8897,plain,
apply(the_mapping(sK23,sK24),sK27) = apply(relation_dom_restriction(the_mapping(sK23,sK24),sF31),sK27),
inference(forward_subsumption_resolution,[],[f8887,f312]) ).
fof(f8901,plain,
apply(the_mapping(sK23,sF28),sK27) = apply(the_mapping(sK23,sK24),sK27),
inference(forward_demodulation,[],[f8897,f4661]) ).
fof(f10235,plain,
( empty_carrier(sK23)
| apply_on_structs(sF28,sK23,the_mapping(sK23,sF28),sK27) = apply(the_mapping(sK23,sF28),sK27)
| ~ one_sorted_str(sK23) ),
inference(resolution,[],[f2536,f599]) ).
fof(f10236,plain,
( apply_on_structs(sF28,sK23,the_mapping(sK23,sF28),sK27) = apply(the_mapping(sK23,sF28),sK27)
| ~ one_sorted_str(sK23) ),
inference(forward_subsumption_resolution,[],[f10235,f313]) ).
fof(f10237,plain,
apply_on_structs(sF28,sK23,the_mapping(sK23,sF28),sK27) = apply(the_mapping(sK23,sF28),sK27),
inference(forward_subsumption_resolution,[],[f10236,f312]) ).
fof(f10238,plain,
apply_on_structs(sF28,sK23,the_mapping(sK23,sF28),sK27) = apply(the_mapping(sK23,sK24),sK27),
inference(forward_demodulation,[],[f10237,f8901]) ).
fof(f10239,plain,
sF29 = apply(the_mapping(sK23,sK24),sK27),
inference(forward_demodulation,[],[f10238,f2287]) ).
fof(f10244,plain,
( empty_carrier(sK23)
| apply_on_structs(sK24,sK23,the_mapping(sK23,sK24),sK27) = apply(the_mapping(sK23,sK24),sK27)
| ~ one_sorted_str(sK23) ),
inference(resolution,[],[f2546,f314]) ).
fof(f10245,plain,
( apply_on_structs(sK24,sK23,the_mapping(sK23,sK24),sK27) = apply(the_mapping(sK23,sK24),sK27)
| ~ one_sorted_str(sK23) ),
inference(forward_subsumption_resolution,[],[f10244,f313]) ).
fof(f10246,plain,
apply_on_structs(sK24,sK23,the_mapping(sK23,sK24),sK27) = apply(the_mapping(sK23,sK24),sK27),
inference(forward_subsumption_resolution,[],[f10245,f312]) ).
fof(f10247,plain,
sF29 = apply_on_structs(sK24,sK23,the_mapping(sK23,sK24),sK27),
inference(forward_demodulation,[],[f10246,f10239]) ).
fof(f10249,plain,
sF29 = sF30,
inference(superposition,[],[f2283,f10247]) ).
fof(f10253,plain,
$false,
inference(forward_subsumption_resolution,[],[f10249,f342]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU385+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.38 % Computer : n016.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:07:59 UTC 2026
% 0.11/0.38 % CPUTime :
% 0.11/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.11/0.42 Running first-order model finding
% 0.11/0.42 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 15.39/2.68 % (3271588)Will run a generic schedule for satisfiability detection.
% 15.39/2.68 % (3271595)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4170128703:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 15.39/2.68 % (3271594)% WARNING: option uhcvi not known.
% 15.39/2.68 % (3271593)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3165583379_2999 on theBenchmark for (2999ds/0Mi)
% 15.39/2.68 % (3271594)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=273224584:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 15.39/2.68 % (3271596)dis+10_1_sil=32000:sp=arity:random_seed=2920311264:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 15.39/2.68 % (3271598)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=3494768844:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 15.39/2.68 % (3271597)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=1681165057:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 15.39/2.68 % (3271599)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=766655061:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 15.39/2.69 % TRYING [1]
% 15.39/2.69 % TRYING [2]
% 15.39/2.69 % TRYING [3]
% 15.39/2.69 % TRYING [4]
% 15.39/2.69 % (3271596)Instruction limit reached!
% 15.39/2.69 % (3271596)------------------------------
% 15.39/2.69 % (3271596)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.39/2.69 % (3271596)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.39/2.69 % (3271596)CaDiCaL version: 2.1.3
% 15.39/2.69 % (3271596)Termination reason: Instruction limit
% 15.39/2.69 % (3271596)Termination phase: Saturation
% 15.39/2.69 % (3271596)Time elapsed: 0.068 s
% 15.39/2.69 % (3271596)Peak memory usage: 13 MB
% 15.39/2.69 % (3271596)Instructions burned: 103 (million)
% 15.39/2.69 % (3271597)Instruction limit reached!
% 15.39/2.69 % (3271597)------------------------------
% 15.39/2.69 % (3271597)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.39/2.69 % (3271597)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.39/2.69 % (3271597)CaDiCaL version: 2.1.3
% 15.39/2.69 % (3271597)Termination reason: Instruction limit
% 15.39/2.69 % (3271597)Termination phase: Saturation
% 15.39/2.69 % (3271597)Time elapsed: 0.072 s
% 15.39/2.69 % (3271597)Peak memory usage: 13 MB
% 15.39/2.69 % (3271597)Instructions burned: 117 (million)
% 15.39/2.69 % (3271598)Instruction limit reached!
% 15.39/2.69 % (3271598)------------------------------
% 15.39/2.69 % (3271598)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.39/2.69 % (3271598)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.39/2.69 % (3271598)CaDiCaL version: 2.1.3
% 15.39/2.69 % (3271598)Termination reason: Instruction limit
% 15.39/2.69 % (3271598)Termination phase: Saturation
% 15.39/2.69 % (3271598)Time elapsed: 0.080 s
% 15.39/2.69 % (3271598)Peak memory usage: 14 MB
% 15.39/2.69 % (3271598)Instructions burned: 132 (million)
% 15.39/2.69 % (3271607)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=3233031096:i=714:nm=2_2998 on theBenchmark for (2998ds/714Mi)
% 15.39/2.69 % (3271608)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=1824431343:i=131:bd=preordered:fsd=on_2998 on theBenchmark for (2998ds/131Mi)
% 15.39/2.69 % (3271599)Instruction limit reached!
% 15.39/2.69 % (3271599)------------------------------
% 15.39/2.69 % (3271599)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.39/2.69 % (3271599)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.39/2.69 % (3271599)CaDiCaL version: 2.1.3
% 15.39/2.69 % (3271599)Termination reason: Instruction limit
% 15.39/2.69 % (3271599)Termination phase: Saturation
% 15.39/2.69 % (3271599)Time elapsed: 0.095 s
% 15.39/2.69 % (3271599)Peak memory usage: 15 MB
% 15.39/2.69 % (3271599)Instructions burned: 160 (million)
% 15.39/2.69 % TRYING [1]
% 15.39/2.69 % TRYING [2]
% 15.39/2.69 % (3271609)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=1642064179:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2998 on theBenchmark for (2998ds/684Mi)
% 15.39/2.69 % TRYING [3]
% 15.39/2.69 % (3271612)ott-21_1_sil=16000:fs=off:random_seed=2178691268:i=180:av=off:fsr=off_2998 on theBenchmark for (2998ds/180Mi)
% 15.39/2.69 % (3271608)Instruction limit reached!
% 15.39/2.69 % (3271608)------------------------------
% 15.39/2.69 % (3271608)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 15.39/2.69 % (3271608)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.98/4.40 % (3271608)CaDiCaL version: 2.1.3
% 17.98/4.40 % (3271608)Termination reason: Instruction limit
% 17.98/4.40 % (3271608)Termination phase: Saturation
% 17.98/4.40 % (3271608)Time elapsed: 0.086 s
% 17.98/4.40 % (3271608)Peak memory usage: 14 MB
% 17.98/4.40 % (3271608)Instructions burned: 131 (million)
% 17.98/4.40 % TRYING [5]
% 17.98/4.40 % (3271615)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2360365527:i=477:bd=all_2997 on theBenchmark for (2997ds/477Mi)
% 17.98/4.40 % TRYING [4]
% 17.98/4.40 % (3271612)Instruction limit reached!
% 17.98/4.40 % (3271612)------------------------------
% 17.98/4.40 % (3271612)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.98/4.40 % (3271612)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.98/4.40 % (3271612)CaDiCaL version: 2.1.3
% 17.98/4.40 % (3271612)Termination reason: Instruction limit
% 17.98/4.40 % (3271612)Termination phase: Saturation
% 17.98/4.40 % (3271612)Time elapsed: 0.098 s
% 17.98/4.40 % (3271612)Peak memory usage: 13 MB
% 17.98/4.40 % (3271612)Instructions burned: 180 (million)
% 17.98/4.40 % (3271617)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=362596633:fmbsr=1.3:i=865:ins=25_2997 on theBenchmark for (2997ds/865Mi)
% 17.98/4.40 % TRYING [1]
% 17.98/4.40 % TRYING [2]
% 17.98/4.40 % TRYING [3]
% 17.98/4.40 % (3271607)Instruction limit reached!
% 17.98/4.40 % (3271607)------------------------------
% 17.98/4.40 % (3271607)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.98/4.40 % (3271607)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.98/4.40 % (3271607)CaDiCaL version: 2.1.3
% 17.98/4.40 % (3271607)Termination reason: Instruction limit
% 17.98/4.40 % (3271607)Termination phase: Finite model building constraint generation
% 17.98/4.40 % (3271607)Time elapsed: 0.235 s
% 17.98/4.40 % (3271607)Peak memory usage: 24 MB
% 17.98/4.40 % (3271607)Instructions burned: 715 (million)
% 17.98/4.40 % (3271619)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=88095442:i=1179_2996 on theBenchmark for (2996ds/1179Mi)
% 17.98/4.40 % TRYING [4]
% 17.98/4.40 % (3271609)Instruction limit reached!
% 17.98/4.40 % (3271609)------------------------------
% 17.98/4.40 % (3271609)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.98/4.40 % (3271609)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.98/4.40 % (3271609)CaDiCaL version: 2.1.3
% 17.98/4.40 % (3271609)Termination reason: Instruction limit
% 17.98/4.40 % (3271609)Termination phase: Saturation
% 17.98/4.40 % (3271609)Time elapsed: 0.408 s
% 17.98/4.40 % (3271609)Peak memory usage: 20 MB
% 17.98/4.40 % (3271609)Instructions burned: 685 (million)
% 17.98/4.40 % (3271621)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1682051436:i=889:ins=1_2994 on theBenchmark for (2994ds/889Mi)
% 17.98/4.40 % (3271615)Instruction limit reached!
% 17.98/4.40 % (3271615)------------------------------
% 17.98/4.40 % (3271615)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.98/4.40 % (3271615)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.98/4.40 % (3271615)CaDiCaL version: 2.1.3
% 17.98/4.40 % (3271615)Termination reason: Instruction limit
% 17.98/4.40 % (3271615)Termination phase: Saturation
% 17.98/4.40 % (3271615)Time elapsed: 0.332 s
% 17.98/4.40 % (3271615)Peak memory usage: 15 MB
% 17.98/4.40 % (3271615)Instructions burned: 479 (million)
% 17.98/4.40 % (3271623)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=1283979557:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2994 on theBenchmark for (2994ds/692Mi)
% 17.98/4.40 % (3271617)Instruction limit reached!
% 17.98/4.40 % (3271617)------------------------------
% 17.98/4.40 % (3271617)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.98/4.40 % (3271617)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.98/4.40 % (3271617)CaDiCaL version: 2.1.3
% 17.98/4.40 % (3271617)Termination reason: Instruction limit
% 17.98/4.40 % (3271617)Termination phase: Finite model building SAT solving
% 17.98/4.40 % (3271617)Time elapsed: 0.344 s
% 17.98/4.40 % (3271617)Peak memory usage: 29 MB
% 17.98/4.40 % (3271617)Instructions burned: 869 (million)
% 17.98/4.40 % (3271625)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=880238152:i=879:kws=inv_precedence:fsr=off_2993 on theBenchmark for (2993ds/879Mi)
% 17.98/4.40 % TRYING [6]
% 17.98/4.40 % (3271621)Instruction limit reached!
% 17.98/4.40 % (3271621)------------------------------
% 17.98/4.40 % (3271621)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.98/4.40 % (3271621)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.98/4.40 % (3271621)CaDiCaL version: 2.1.3
% 17.98/4.40 % (3271621)Termination reason: Instruction limit
% 17.98/4.40 % (3271621)Termination phase: Finite model building constraint generation
% 17.98/4.40 % (3271621)Time elapsed: 0.412 s
% 17.98/4.40 % (3271621)Peak memory usage: 107 MB
% 17.98/4.40 % (3271621)Instructions burned: 891 (million)
% 17.98/4.40 % (3271623)Instruction limit reached!
% 17.98/4.40 % (3271623)------------------------------
% 17.98/4.40 % (3271623)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.98/4.40 % (3271623)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.98/4.40 % (3271623)CaDiCaL version: 2.1.3
% 17.98/4.40 % (3271623)Termination reason: Instruction limit
% 17.98/4.40 % (3271623)Termination phase: Saturation
% 17.98/4.40 % (3271623)Time elapsed: 0.391 s
% 17.98/4.40 % (3271623)Peak memory usage: 20 MB
% 17.98/4.40 % (3271623)Instructions burned: 692 (million)
% 17.98/4.40 % (3271627)fmb+10_1_sil=64000:random_seed=2393421140:i=22061:nm=2:gsp=on_2990 on theBenchmark for (2990ds/22061Mi)
% 17.98/4.40 % TRYING [1]
% 17.98/4.40 % TRYING [2]
% 17.98/4.40 % (3271628)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=1099795507:i=9515:nm=5_2990 on theBenchmark for (2990ds/9515Mi)
% 17.98/4.40 % TRYING [20]
% 17.98/4.40 % TRYING [3]
% 17.98/4.40 % (3271619)Instruction limit reached!
% 17.98/4.40 % (3271619)------------------------------
% 17.98/4.40 % (3271619)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.98/4.40 % (3271619)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.98/4.40 % (3271619)CaDiCaL version: 2.1.3
% 17.98/4.40 % (3271619)Termination reason: Instruction limit
% 17.98/4.40 % (3271619)Termination phase: Saturation
% 17.98/4.40 % (3271619)Time elapsed: 0.699 s
% 17.98/4.40 % (3271619)Peak memory usage: 30 MB
% 17.98/4.40 % (3271619)Instructions burned: 1179 (million)
% 17.98/4.40 % (3271631)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=4127756071:fmbsr=1.7:i=920_2989 on theBenchmark for (2989ds/920Mi)
% 17.98/4.40 % TRYING [8]
% 17.98/4.40 % (3271625)Instruction limit reached!
% 17.98/4.40 % (3271625)------------------------------
% 17.98/4.40 % (3271625)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.98/4.40 % (3271625)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.98/4.40 % (3271625)CaDiCaL version: 2.1.3
% 17.98/4.40 % (3271625)Termination reason: Instruction limit
% 17.98/4.40 % (3271625)Termination phase: Saturation
% 17.98/4.40 % (3271625)Time elapsed: 0.513 s
% 17.98/4.40 % (3271625)Peak memory usage: 19 MB
% 17.98/4.40 % (3271625)Instructions burned: 879 (million)
% 17.98/4.40 % (3271633)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=807095639:i=5131_2988 on theBenchmark for (2988ds/5131Mi)
% 17.98/4.40 % TRYING [4]
% 17.98/4.40 % (3271631)Instruction limit reached!
% 17.98/4.40 % (3271631)------------------------------
% 17.98/4.40 % (3271631)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.98/4.40 % (3271631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.98/4.40 % (3271631)CaDiCaL version: 2.1.3
% 17.98/4.40 % (3271631)Termination reason: Instruction limit
% 17.98/4.40 % (3271631)Termination phase: Finite model building constraint generation
% 17.98/4.40 % (3271631)Time elapsed: 0.302 s
% 17.98/4.40 % (3271631)Peak memory usage: 59 MB
% 17.98/4.40 % (3271631)Instructions burned: 921 (million)
% 17.98/4.40 % (3271635)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=748026679:i=1472:ins=7:fdi=8:gsp=on_2985 on theBenchmark for (2985ds/1472Mi)
% 17.98/4.40 % TRYING [7]
% 17.98/4.40 % (3271635)Instruction limit reached!
% 17.98/4.40 % (3271635)------------------------------
% 17.98/4.40 % (3271635)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.98/4.40 % (3271635)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.98/4.40 % (3271635)CaDiCaL version: 2.1.3
% 17.98/4.40 % (3271635)Termination reason: Instruction limit
% 17.98/4.40 % (3271635)Termination phase: Saturation
% 17.98/4.40 % (3271635)Time elapsed: 0.794 s
% 17.98/4.40 % (3271635)Peak memory usage: 24 MB
% 17.98/4.40 % (3271635)Instructions burned: 1473 (million)
% 17.98/4.40 % (3271637)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3723759812:i=6324_2977 on theBenchmark for (2977ds/6324Mi)
% 17.98/4.40 % (3271637)Cannot represent all propositional literals internally
% 17.98/4.40 % (3271637)Refutation not found, incomplete strategy
% 17.98/4.40 % (3271637)------------------------------
% 17.98/4.40 % (3271637)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.98/4.40 % (3271637)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.98/4.40 % (3271637)CaDiCaL version: 2.1.3
% 17.98/4.40 % (3271637)Termination reason: Refutation not found, incomplete strategy
% 17.98/4.40 % (3271637)Time elapsed: 0.012 s
% 17.98/4.40 % (3271637)Peak memory usage: 11 MB
% 17.98/4.40 % (3271637)Instructions burned: 23 (million)
% 17.98/4.40 % (3271637)------------------------------
% 17.98/4.40 % (3271637)------------------------------
% 17.98/4.40 % (3271639)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=2568771187:fmbsr=2.30978:i=2174_2977 on theBenchmark for (2977ds/2174Mi)
% 17.98/4.40 % TRYING [16]
% 17.98/4.40 % (3271639)Instruction limit reached!
% 17.98/4.40 % (3271639)------------------------------
% 17.98/4.40 % (3271639)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.98/4.40 % (3271639)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.98/4.40 % (3271639)CaDiCaL version: 2.1.3
% 17.98/4.40 % (3271639)Termination reason: Instruction limit
% 17.98/4.40 % (3271639)Termination phase: Finite model building constraint generation
% 17.98/4.40 % (3271639)Time elapsed: 0.748 s
% 17.98/4.40 % (3271639)Peak memory usage: 131 MB
% 17.98/4.40 % (3271639)Instructions burned: 2175 (million)
% 17.98/4.40 % (3271641)ott-2_1_sil=16000:newcnf=on:random_seed=1851494545:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2969 on theBenchmark for (2969ds/869Mi)
% 17.98/4.40 % (3271641)Instruction limit reached!
% 17.98/4.40 % (3271641)------------------------------
% 17.98/4.40 % (3271641)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.98/4.40 % (3271641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.98/4.40 % (3271641)CaDiCaL version: 2.1.3
% 17.98/4.40 % (3271641)Termination reason: Instruction limit
% 17.98/4.40 % (3271641)Termination phase: Saturation
% 17.98/4.40 % (3271641)Time elapsed: 0.502 s
% 17.98/4.40 % (3271641)Peak memory usage: 19 MB
% 17.98/4.40 % (3271641)Instructions burned: 870 (million)
% 17.98/4.40 % (3271643)ott+10_1_sil=32000:tgt=ground:random_seed=3566753378:i=5114:av=off_2964 on theBenchmark for (2964ds/5114Mi)
% 17.98/4.40 % (3271643) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-3271588-3271643"...
% 17.98/4.40 % (3271643)...printing done.
% 17.98/4.40 % (3271643)Refutation found. Thanks to Tanya!
% 17.98/4.40 % SZS status Theorem for theBenchmark
% 17.98/4.40 % SZS output start Proof for theBenchmark
% See solution above
% 17.98/4.41 % (3271643)------------------------------
% 17.98/4.41 % (3271643)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 17.98/4.41 % (3271643)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 17.98/4.41 % (3271643)CaDiCaL version: 2.1.3
% 17.98/4.41 % (3271643)Termination reason: Refutation
% 17.98/4.41 % (3271643)Time elapsed: 0.315 s
% 17.98/4.41 % (3271643)Peak memory usage: 19 MB
% 17.98/4.41 % (3271643)Instructions burned: 521 (million)
% 17.98/4.41 % (3271588)Success in time 3.979 s
% 17.98/4.41 % Vampire exiting
%------------------------------------------------------------------------------