%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU385+2 : 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 : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:48:39 PM UTC 2026
% Result : Theorem 35.05s 5.87s
% Output : Refutation 35.84s
% Verified :
% SZS Type : Refutation
% Derivation depth : 40
% Number of leaves : 21
% Syntax : Number of formulae : 181 ( 34 unt; 5 def)
% Number of atoms : 814 ( 107 equ)
% Maximal formula atoms : 14 ( 4 avg)
% Number of connectives : 1061 ( 428 ~; 508 |; 85 &)
% ( 7 <=>; 33 =>; 0 <=; 0 <~>)
% Maximal formula depth : 20 ( 7 avg)
% Maximal term depth : 4 ( 1 avg)
% Number of predicates : 17 ( 15 usr; 1 prp; 0-3 aty)
% Number of functors : 21 ( 21 usr; 10 con; 0-4 aty)
% Number of variables : 302 ( 289 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f197,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(f209,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(f290,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(f309,axiom,
! [X0] :
( rel_str(X0)
=> one_sorted_str(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_orders_2) ).
fof(f312,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(f326,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(f352,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(f364,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0) )
=> ~ empty(the_carrier(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f372,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(f542,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(f546,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(f564,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(f661,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(f662,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)],[f661]) ).
fof(f680,axiom,
! [X0,X1] :
( in(X0,X1)
=> element(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
fof(f723,axiom,
! [X0,X1] :
( element(X0,X1)
=> ( empty(X1)
| in(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
fof(f829,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(f1194,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,[],[f197]) ).
fof(f1195,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,[],[f1194]) ).
fof(f1213,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,[],[f209]) ).
fof(f1214,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,[],[f1213]) ).
fof(f1298,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,[],[f290]) ).
fof(f1299,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,[],[f1298]) ).
fof(f1323,plain,
! [X0] :
( one_sorted_str(X0)
| ~ rel_str(X0) ),
inference(ennf_transformation,[],[f309]) ).
fof(f1325,plain,
! [X0] :
( ! [X1] :
( rel_str(X1)
| ~ net_str(X1,X0) )
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f312]) ).
fof(f1339,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,[],[f326]) ).
fof(f1340,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,[],[f1339]) ).
fof(f1364,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,[],[f352]) ).
fof(f1365,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,[],[f1364]) ).
fof(f1375,plain,
! [X0] :
( ~ empty(the_carrier(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f364]) ).
fof(f1376,plain,
! [X0] :
( ~ empty(the_carrier(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(flattening,[],[f1375]) ).
fof(f1380,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,[],[f372]) ).
fof(f1381,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,[],[f1380]) ).
fof(f1533,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,[],[f542]) ).
fof(f1534,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,[],[f1533]) ).
fof(f1539,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,[],[f546]) ).
fof(f1540,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,[],[f1539]) ).
fof(f1719,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,[],[f662]) ).
fof(f1720,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,[],[f1719]) ).
fof(f1742,plain,
! [X0,X1] :
( element(X0,X1)
| ~ in(X0,X1) ),
inference(ennf_transformation,[],[f680]) ).
fof(f1809,plain,
! [X0,X1] :
( empty(X1)
| in(X0,X1)
| ~ element(X0,X1) ),
inference(ennf_transformation,[],[f723]) ).
fof(f1810,plain,
! [X0,X1] :
( empty(X1)
| in(X0,X1)
| ~ element(X0,X1) ),
inference(flattening,[],[f1809]) ).
fof(f1946,plain,
! [X0,X1,X2] :
( apply(relation_dom_restriction(X2,X0),X1) = apply(X2,X1)
| ~ in(X1,X0)
| ~ relation(X2)
| ~ function(X2) ),
inference(ennf_transformation,[],[f829]) ).
fof(f1947,plain,
! [X0,X1,X2] :
( apply(relation_dom_restriction(X2,X0),X1) = apply(X2,X1)
| ~ in(X1,X0)
| ~ relation(X2)
| ~ function(X2) ),
inference(flattening,[],[f1946]) ).
fof(f2610,plain,
! [X2,X3,X0,X1,X4] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ net_str(X3,X0)
| ~ strict_net_str(X3,X0)
| sK124(X1,X2,X4) = X4
| ~ in(X4,the_carrier(X3))
| netstr_restr_to_element(X0,X1,X2) != X3 ),
inference(cnf_transformation,[],[f1195]) ).
fof(f2611,plain,
! [X2,X3,X0,X1,X4] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ net_str(X3,X0)
| ~ strict_net_str(X3,X0)
| element(sK124(X1,X2,X4),the_carrier(X1))
| ~ in(X4,the_carrier(X3))
| netstr_restr_to_element(X0,X1,X2) != X3 ),
inference(cnf_transformation,[],[f1195]) ).
fof(f2617,plain,
! [X2,X3,X0,X1] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ net_str(X3,X0)
| ~ strict_net_str(X3,X0)
| the_mapping(X0,X3) = partfun_dom_restriction(the_carrier(X1),the_carrier(X0),the_mapping(X0,X1),the_carrier(X3))
| netstr_restr_to_element(X0,X1,X2) != X3 ),
inference(cnf_transformation,[],[f1195]) ).
fof(f2684,plain,
! [X2,X0,X1] :
( apply_netmap(X0,X1,X2) = apply_on_structs(X1,X0,the_mapping(X0,X1),X2)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f1214]) ).
fof(f2792,plain,
! [X2,X0,X1] :
( net_str(netstr_restr_to_element(X0,X1,X2),X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ element(X2,the_carrier(X1)) ),
inference(cnf_transformation,[],[f1299]) ).
fof(f2793,plain,
! [X2,X0,X1] :
( strict_net_str(netstr_restr_to_element(X0,X1,X2),X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ element(X2,the_carrier(X1)) ),
inference(cnf_transformation,[],[f1299]) ).
fof(f2818,plain,
! [X0] :
( ~ rel_str(X0)
| one_sorted_str(X0) ),
inference(cnf_transformation,[],[f1323]) ).
fof(f2820,plain,
! [X0,X1] :
( ~ net_str(X1,X0)
| ~ one_sorted_str(X0)
| rel_str(X1) ),
inference(cnf_transformation,[],[f1325]) ).
fof(f2837,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,[],[f1340]) ).
fof(f2873,plain,
! [X0,X1] :
( quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0) ),
inference(cnf_transformation,[],[f1365]) ).
fof(f2874,plain,
! [X0,X1] :
( ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| function(the_mapping(X0,X1)) ),
inference(cnf_transformation,[],[f1365]) ).
fof(f2875,plain,
! [X0,X1] :
( ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| relation(the_mapping(X0,X1)) ),
inference(cnf_transformation,[],[f1365]) ).
fof(f2920,plain,
! [X0] :
( ~ empty(the_carrier(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f1376]) ).
fof(f2967,plain,
! [X2,X0,X1] :
( ~ empty_carrier(netstr_restr_to_element(X0,X1,X2))
| ~ net_str(X1,X0)
| ~ directed_relstr(X1)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ element(X2,the_carrier(X1)) ),
inference(cnf_transformation,[],[f1381]) ).
fof(f3679,plain,
! [X2,X3,X0,X1] :
( apply(X2,X3) = apply_on_structs(X0,X1,X2,X3)
| ~ relation_of2(X2,the_carrier(X0),the_carrier(X1))
| ~ quasi_total(X2,the_carrier(X0),the_carrier(X1))
| ~ function(X2)
| ~ one_sorted_str(X1)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ element(X3,the_carrier(X0)) ),
inference(cnf_transformation,[],[f1534]) ).
fof(f3683,plain,
! [X2,X3,X0,X1] :
( partfun_dom_restriction(X0,X1,X2,X3) = relation_dom_restriction(X2,X3)
| ~ function(X2)
| ~ relation_of2(X2,X0,X1) ),
inference(cnf_transformation,[],[f1540]) ).
fof(f3702,plain,
! [X2,X0,X1] :
( ~ relation_of2_as_subset(X2,X0,X1)
| relation_of2(X2,X0,X1) ),
inference(cnf_transformation,[],[f564]) ).
fof(f4655,plain,
element(sK544,the_carrier(netstr_restr_to_element(sK540,sK541,sK542))),
inference(cnf_transformation,[],[f1720]) ).
fof(f4656,plain,
sK543 = sK544,
inference(cnf_transformation,[],[f1720]) ).
fof(f4657,plain,
apply_netmap(sK540,sK541,sK543) != apply_netmap(sK540,netstr_restr_to_element(sK540,sK541,sK542),sK544),
inference(cnf_transformation,[],[f1720]) ).
fof(f4659,plain,
element(sK542,the_carrier(sK541)),
inference(cnf_transformation,[],[f1720]) ).
fof(f4660,plain,
net_str(sK541,sK540),
inference(cnf_transformation,[],[f1720]) ).
fof(f4661,plain,
directed_relstr(sK541),
inference(cnf_transformation,[],[f1720]) ).
fof(f4662,plain,
~ empty_carrier(sK541),
inference(cnf_transformation,[],[f1720]) ).
fof(f4663,plain,
one_sorted_str(sK540),
inference(cnf_transformation,[],[f1720]) ).
fof(f4664,plain,
~ empty_carrier(sK540),
inference(cnf_transformation,[],[f1720]) ).
fof(f4693,plain,
! [X0,X1] :
( ~ in(X0,X1)
| element(X0,X1) ),
inference(cnf_transformation,[],[f1742]) ).
fof(f4768,plain,
! [X0,X1] :
( ~ element(X0,X1)
| in(X0,X1)
| empty(X1) ),
inference(cnf_transformation,[],[f1810]) ).
fof(f4963,plain,
! [X2,X0,X1] :
( apply(relation_dom_restriction(X2,X0),X1) = apply(X2,X1)
| ~ relation(X2)
| ~ in(X1,X0)
| ~ function(X2) ),
inference(cnf_transformation,[],[f1947]) ).
fof(f6043,plain,
apply_netmap(sK540,netstr_restr_to_element(sK540,sK541,sK542),sK544) != apply_netmap(sK540,sK541,sK544),
inference(definition_unfolding,[],[f4657,f4656]) ).
fof(f6309,plain,
! [X2,X0,X1] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ net_str(netstr_restr_to_element(X0,X1,X2),X0)
| ~ strict_net_str(netstr_restr_to_element(X0,X1,X2),X0)
| the_mapping(X0,netstr_restr_to_element(X0,X1,X2)) = partfun_dom_restriction(the_carrier(X1),the_carrier(X0),the_mapping(X0,X1),the_carrier(netstr_restr_to_element(X0,X1,X2))) ),
inference(equality_resolution,[],[f2617]) ).
fof(f6313,plain,
! [X2,X0,X1,X4] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ net_str(netstr_restr_to_element(X0,X1,X2),X0)
| ~ strict_net_str(netstr_restr_to_element(X0,X1,X2),X0)
| element(sK124(X1,X2,X4),the_carrier(X1))
| ~ in(X4,the_carrier(netstr_restr_to_element(X0,X1,X2))) ),
inference(equality_resolution,[],[f2611]) ).
fof(f6314,plain,
! [X2,X0,X1,X4] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ net_str(netstr_restr_to_element(X0,X1,X2),X0)
| ~ strict_net_str(netstr_restr_to_element(X0,X1,X2),X0)
| sK124(X1,X2,X4) = X4
| ~ in(X4,the_carrier(netstr_restr_to_element(X0,X1,X2))) ),
inference(equality_resolution,[],[f2610]) ).
fof(f6533,definition,
sF579 = the_carrier(sK541),
introduced(definition,[new_symbols(definition,[sF579])],[function_definition]) ).
fof(f6534,plain,
the_carrier(sK541) = sF579,
inference(reorient_equations,[],[f6533]) ).
fof(f6535,plain,
element(sK542,sF579),
inference(definition_folding,[],[f4659,f6534]) ).
fof(f6537,definition,
sF580 = netstr_restr_to_element(sK540,sK541,sK542),
introduced(definition,[new_symbols(definition,[sF580])],[function_definition]) ).
fof(f6538,plain,
netstr_restr_to_element(sK540,sK541,sK542) = sF580,
inference(reorient_equations,[],[f6537]) ).
fof(f6539,definition,
sF581 = apply_netmap(sK540,sF580,sK544),
introduced(definition,[new_symbols(definition,[sF581])],[function_definition]) ).
fof(f6540,plain,
apply_netmap(sK540,sF580,sK544) = sF581,
inference(reorient_equations,[],[f6539]) ).
fof(f6541,definition,
sF582 = apply_netmap(sK540,sK541,sK544),
introduced(definition,[new_symbols(definition,[sF582])],[function_definition]) ).
fof(f6542,plain,
apply_netmap(sK540,sK541,sK544) = sF582,
inference(reorient_equations,[],[f6541]) ).
fof(f6543,plain,
sF581 != sF582,
inference(definition_folding,[],[f6043,f6542,f6540,f6538]) ).
fof(f6544,definition,
sF583 = the_carrier(sF580),
introduced(definition,[new_symbols(definition,[sF583])],[function_definition]) ).
fof(f6545,plain,
the_carrier(sF580) = sF583,
inference(reorient_equations,[],[f6544]) ).
fof(f6546,plain,
element(sK544,sF583),
inference(definition_folding,[],[f4655,f6545,f6538]) ).
fof(f6653,plain,
! [X2,X0,X1,X4] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ strict_net_str(netstr_restr_to_element(X0,X1,X2),X0)
| sK124(X1,X2,X4) = X4
| ~ in(X4,the_carrier(netstr_restr_to_element(X0,X1,X2))) ),
inference(forward_subsumption_resolution,[],[f6314,f2792]) ).
fof(f6654,plain,
! [X2,X0,X1,X4] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ strict_net_str(netstr_restr_to_element(X0,X1,X2),X0)
| element(sK124(X1,X2,X4),the_carrier(X1))
| ~ in(X4,the_carrier(netstr_restr_to_element(X0,X1,X2))) ),
inference(forward_subsumption_resolution,[],[f6313,f2792]) ).
fof(f6656,plain,
! [X2,X0,X1] :
( ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ strict_net_str(netstr_restr_to_element(X0,X1,X2),X0)
| the_mapping(X0,netstr_restr_to_element(X0,X1,X2)) = partfun_dom_restriction(the_carrier(X1),the_carrier(X0),the_mapping(X0,X1),the_carrier(netstr_restr_to_element(X0,X1,X2))) ),
inference(forward_subsumption_resolution,[],[f6309,f2792]) ).
fof(f6740,plain,
! [X2,X0,X1,X4] :
( ~ in(X4,the_carrier(netstr_restr_to_element(X0,X1,X2)))
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| sK124(X1,X2,X4) = X4
| ~ one_sorted_str(X0) ),
inference(forward_subsumption_resolution,[],[f6653,f2793]) ).
fof(f6741,plain,
! [X2,X0,X1,X4] :
( ~ in(X4,the_carrier(netstr_restr_to_element(X0,X1,X2)))
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| element(sK124(X1,X2,X4),the_carrier(X1))
| ~ one_sorted_str(X0) ),
inference(forward_subsumption_resolution,[],[f6654,f2793]) ).
fof(f6743,plain,
! [X2,X0,X1] :
( the_mapping(X0,netstr_restr_to_element(X0,X1,X2)) = partfun_dom_restriction(the_carrier(X1),the_carrier(X0),the_mapping(X0,X1),the_carrier(netstr_restr_to_element(X0,X1,X2)))
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ one_sorted_str(X0) ),
inference(forward_subsumption_resolution,[],[f6656,f2793]) ).
fof(f6791,plain,
! [X0] :
( ~ in(X0,the_carrier(sF580))
| empty_carrier(sK540)
| ~ net_str(sK541,sK540)
| empty_carrier(sK541)
| ~ element(sK542,the_carrier(sK541))
| sK124(sK541,sK542,X0) = X0
| ~ one_sorted_str(sK540) ),
inference(superposition,[],[f6740,f6538]) ).
fof(f6793,plain,
( net_str(sF580,sK540)
| ~ net_str(sK541,sK540)
| empty_carrier(sK541)
| ~ one_sorted_str(sK540)
| empty_carrier(sK540)
| ~ element(sK542,the_carrier(sK541)) ),
inference(superposition,[],[f2792,f6538]) ).
fof(f6794,plain,
( net_str(sF580,sK540)
| empty_carrier(sK541)
| ~ one_sorted_str(sK540)
| empty_carrier(sK540)
| ~ element(sK542,the_carrier(sK541)) ),
inference(forward_subsumption_resolution,[],[f6793,f4660]) ).
fof(f6796,plain,
! [X0] :
( ~ in(X0,the_carrier(sF580))
| ~ net_str(sK541,sK540)
| empty_carrier(sK541)
| ~ element(sK542,the_carrier(sK541))
| sK124(sK541,sK542,X0) = X0
| ~ one_sorted_str(sK540) ),
inference(forward_subsumption_resolution,[],[f6791,f4664]) ).
fof(f6798,plain,
( net_str(sF580,sK540)
| ~ one_sorted_str(sK540)
| empty_carrier(sK540)
| ~ element(sK542,the_carrier(sK541)) ),
inference(forward_subsumption_resolution,[],[f6794,f4662]) ).
fof(f6800,plain,
! [X0] :
( ~ in(X0,the_carrier(sF580))
| empty_carrier(sK541)
| ~ element(sK542,the_carrier(sK541))
| sK124(sK541,sK542,X0) = X0
| ~ one_sorted_str(sK540) ),
inference(forward_subsumption_resolution,[],[f6796,f4660]) ).
fof(f6802,plain,
( net_str(sF580,sK540)
| empty_carrier(sK540)
| ~ element(sK542,the_carrier(sK541)) ),
inference(forward_subsumption_resolution,[],[f6798,f4663]) ).
fof(f6804,plain,
! [X0] :
( ~ in(X0,the_carrier(sF580))
| ~ element(sK542,the_carrier(sK541))
| sK124(sK541,sK542,X0) = X0
| ~ one_sorted_str(sK540) ),
inference(forward_subsumption_resolution,[],[f6800,f4662]) ).
fof(f6806,plain,
( net_str(sF580,sK540)
| ~ element(sK542,the_carrier(sK541)) ),
inference(forward_subsumption_resolution,[],[f6802,f4664]) ).
fof(f6808,plain,
! [X0] :
( ~ in(X0,the_carrier(sF580))
| ~ element(sK542,the_carrier(sK541))
| sK124(sK541,sK542,X0) = X0 ),
inference(forward_subsumption_resolution,[],[f6804,f4663]) ).
fof(f6810,plain,
( ~ element(sK542,sF579)
| net_str(sF580,sK540) ),
inference(forward_demodulation,[],[f6806,f6534]) ).
fof(f6812,plain,
! [X0] :
( ~ in(X0,sF583)
| ~ element(sK542,the_carrier(sK541))
| sK124(sK541,sK542,X0) = X0 ),
inference(forward_demodulation,[],[f6808,f6545]) ).
fof(f6814,plain,
net_str(sF580,sK540),
inference(forward_subsumption_resolution,[],[f6810,f6535]) ).
fof(f6816,plain,
! [X0] :
( ~ element(sK542,sF579)
| ~ in(X0,sF583)
| sK124(sK541,sK542,X0) = X0 ),
inference(forward_demodulation,[],[f6812,f6534]) ).
fof(f6820,plain,
! [X0] :
( sK124(sK541,sK542,X0) = X0
| ~ in(X0,sF583) ),
inference(forward_subsumption_resolution,[],[f6816,f6535]) ).
fof(f6842,plain,
( ~ empty_carrier(sF580)
| ~ net_str(sK541,sK540)
| ~ directed_relstr(sK541)
| empty_carrier(sK541)
| ~ one_sorted_str(sK540)
| empty_carrier(sK540)
| ~ element(sK542,the_carrier(sK541)) ),
inference(superposition,[],[f2967,f6538]) ).
fof(f6843,plain,
( ~ empty_carrier(sF580)
| ~ directed_relstr(sK541)
| empty_carrier(sK541)
| ~ one_sorted_str(sK540)
| empty_carrier(sK540)
| ~ element(sK542,the_carrier(sK541)) ),
inference(forward_subsumption_resolution,[],[f6842,f4660]) ).
fof(f6844,plain,
( ~ empty_carrier(sF580)
| empty_carrier(sK541)
| ~ one_sorted_str(sK540)
| empty_carrier(sK540)
| ~ element(sK542,the_carrier(sK541)) ),
inference(forward_subsumption_resolution,[],[f6843,f4661]) ).
fof(f6845,plain,
( ~ empty_carrier(sF580)
| ~ one_sorted_str(sK540)
| empty_carrier(sK540)
| ~ element(sK542,the_carrier(sK541)) ),
inference(forward_subsumption_resolution,[],[f6844,f4662]) ).
fof(f6846,plain,
( ~ empty_carrier(sF580)
| empty_carrier(sK540)
| ~ element(sK542,the_carrier(sK541)) ),
inference(forward_subsumption_resolution,[],[f6845,f4663]) ).
fof(f6847,plain,
( ~ empty_carrier(sF580)
| ~ element(sK542,the_carrier(sK541)) ),
inference(forward_subsumption_resolution,[],[f6846,f4664]) ).
fof(f6848,plain,
( ~ element(sK542,sF579)
| ~ empty_carrier(sF580) ),
inference(forward_demodulation,[],[f6847,f6534]) ).
fof(f6849,plain,
~ empty_carrier(sF580),
inference(forward_subsumption_resolution,[],[f6848,f6535]) ).
fof(f6868,plain,
! [X0] :
( ~ in(X0,the_carrier(sF580))
| empty_carrier(sK540)
| ~ net_str(sK541,sK540)
| empty_carrier(sK541)
| ~ element(sK542,the_carrier(sK541))
| element(sK124(sK541,sK542,X0),the_carrier(sK541))
| ~ one_sorted_str(sK540) ),
inference(superposition,[],[f6741,f6538]) ).
fof(f6872,plain,
! [X0] :
( ~ in(X0,the_carrier(sF580))
| ~ net_str(sK541,sK540)
| empty_carrier(sK541)
| ~ element(sK542,the_carrier(sK541))
| element(sK124(sK541,sK542,X0),the_carrier(sK541))
| ~ one_sorted_str(sK540) ),
inference(forward_subsumption_resolution,[],[f6868,f4664]) ).
fof(f6873,plain,
! [X0] :
( ~ in(X0,the_carrier(sF580))
| empty_carrier(sK541)
| ~ element(sK542,the_carrier(sK541))
| element(sK124(sK541,sK542,X0),the_carrier(sK541))
| ~ one_sorted_str(sK540) ),
inference(forward_subsumption_resolution,[],[f6872,f4660]) ).
fof(f6874,plain,
! [X0] :
( ~ in(X0,the_carrier(sF580))
| ~ element(sK542,the_carrier(sK541))
| element(sK124(sK541,sK542,X0),the_carrier(sK541))
| ~ one_sorted_str(sK540) ),
inference(forward_subsumption_resolution,[],[f6873,f4662]) ).
fof(f6875,plain,
! [X0] :
( ~ in(X0,the_carrier(sF580))
| ~ element(sK542,the_carrier(sK541))
| element(sK124(sK541,sK542,X0),the_carrier(sK541)) ),
inference(forward_subsumption_resolution,[],[f6874,f4663]) ).
fof(f6876,plain,
! [X0] :
( ~ in(X0,sF583)
| ~ element(sK542,the_carrier(sK541))
| element(sK124(sK541,sK542,X0),the_carrier(sK541)) ),
inference(forward_demodulation,[],[f6875,f6545]) ).
fof(f6877,plain,
! [X0] :
( ~ element(sK542,sF579)
| ~ in(X0,sF583)
| element(sK124(sK541,sK542,X0),the_carrier(sK541)) ),
inference(forward_demodulation,[],[f6876,f6534]) ).
fof(f6878,plain,
! [X0] :
( ~ in(X0,sF583)
| element(sK124(sK541,sK542,X0),the_carrier(sK541)) ),
inference(forward_subsumption_resolution,[],[f6877,f6535]) ).
fof(f6879,plain,
! [X0] :
( element(sK124(sK541,sK542,X0),sF579)
| ~ in(X0,sF583) ),
inference(forward_demodulation,[],[f6878,f6534]) ).
fof(f6881,plain,
( ~ empty(sF583)
| empty_carrier(sF580)
| ~ one_sorted_str(sF580) ),
inference(superposition,[],[f2920,f6545]) ).
fof(f6883,plain,
( ~ empty(sF583)
| ~ one_sorted_str(sF580) ),
inference(forward_subsumption_resolution,[],[f6881,f6849]) ).
fof(f6888,plain,
( ~ one_sorted_str(sK540)
| rel_str(sF580) ),
inference(resolution,[],[f2820,f6814]) ).
fof(f6889,plain,
( ~ one_sorted_str(sK540)
| rel_str(sK541) ),
inference(resolution,[],[f2820,f4660]) ).
fof(f6891,plain,
rel_str(sK541),
inference(forward_subsumption_resolution,[],[f6889,f4663]) ).
fof(f6892,plain,
rel_str(sF580),
inference(forward_subsumption_resolution,[],[f6888,f4663]) ).
fof(f6918,plain,
! [X0] :
( element(X0,sF579)
| ~ in(X0,sF583)
| ~ in(X0,sF583) ),
inference(superposition,[],[f6879,f6820]) ).
fof(f6919,plain,
! [X0] :
( ~ in(X0,sF583)
| element(X0,sF579) ),
inference(duplicate_literal_removal,[],[f6918]) ).
fof(f6953,plain,
one_sorted_str(sK541),
inference(resolution,[],[f2818,f6891]) ).
fof(f7042,plain,
one_sorted_str(sF580),
inference(resolution,[],[f6892,f2818]) ).
fof(f7044,plain,
~ empty(sF583),
inference(backward_subsumption_resolution,[],[f6883,f7042]) ).
fof(f7055,plain,
( in(sK544,sF583)
| empty(sF583) ),
inference(resolution,[],[f4768,f6546]) ).
fof(f7058,plain,
in(sK544,sF583),
inference(forward_subsumption_resolution,[],[f7055,f7044]) ).
fof(f7426,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,[],[f2837,f3702]) ).
fof(f7777,plain,
! [X2,X0,X1] :
( apply_netmap(X0,X1,X2) = apply(the_mapping(X0,X1),X2)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ one_sorted_str(X0)
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ function(the_mapping(X0,X1))
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ one_sorted_str(X1)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1)) ),
inference(superposition,[],[f2684,f3679]) ).
fof(f7778,plain,
! [X2,X0,X1] :
( apply_netmap(X0,X1,X2) = apply(the_mapping(X0,X1),X2)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ one_sorted_str(X0)
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ function(the_mapping(X0,X1))
| ~ one_sorted_str(X1) ),
inference(duplicate_literal_removal,[],[f7777]) ).
fof(f7780,plain,
! [X2,X0,X1] :
( apply_netmap(X0,X1,X2) = apply(the_mapping(X0,X1),X2)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ one_sorted_str(X0)
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ function(the_mapping(X0,X1))
| ~ one_sorted_str(X1) ),
inference(forward_subsumption_resolution,[],[f7778,f2873]) ).
fof(f7782,plain,
! [X2,X0,X1] :
( apply_netmap(X0,X1,X2) = apply(the_mapping(X0,X1),X2)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ one_sorted_str(X0)
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ one_sorted_str(X1) ),
inference(forward_subsumption_resolution,[],[f7780,f2874]) ).
fof(f7784,plain,
! [X2,X0,X1] :
( apply_netmap(X0,X1,X2) = apply(the_mapping(X0,X1),X2)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X1) ),
inference(forward_subsumption_resolution,[],[f7782,f7426]) ).
fof(f9622,plain,
! [X2,X0,X1] :
( the_mapping(X1,netstr_restr_to_element(X1,X0,X2)) = relation_dom_restriction(the_mapping(X1,X0),the_carrier(netstr_restr_to_element(X1,X0,X2)))
| empty_carrier(X1)
| ~ net_str(X0,X1)
| empty_carrier(X0)
| ~ element(X2,the_carrier(X0))
| ~ one_sorted_str(X1)
| ~ function(the_mapping(X1,X0))
| ~ relation_of2(the_mapping(X1,X0),the_carrier(X0),the_carrier(X1)) ),
inference(superposition,[],[f6743,f3683]) ).
fof(f9633,plain,
! [X2,X0,X1] :
( the_mapping(X1,netstr_restr_to_element(X1,X0,X2)) = relation_dom_restriction(the_mapping(X1,X0),the_carrier(netstr_restr_to_element(X1,X0,X2)))
| empty_carrier(X1)
| ~ net_str(X0,X1)
| empty_carrier(X0)
| ~ element(X2,the_carrier(X0))
| ~ one_sorted_str(X1)
| ~ relation_of2(the_mapping(X1,X0),the_carrier(X0),the_carrier(X1)) ),
inference(forward_subsumption_resolution,[],[f9622,f2874]) ).
fof(f9643,plain,
! [X2,X0,X1] :
( the_mapping(X1,netstr_restr_to_element(X1,X0,X2)) = relation_dom_restriction(the_mapping(X1,X0),the_carrier(netstr_restr_to_element(X1,X0,X2)))
| empty_carrier(X1)
| ~ net_str(X0,X1)
| empty_carrier(X0)
| ~ element(X2,the_carrier(X0))
| ~ one_sorted_str(X1) ),
inference(forward_subsumption_resolution,[],[f9633,f7426]) ).
fof(f9671,plain,
! [X2,X3,X0,X1] :
( apply(the_mapping(X2,X1),X3) = apply(the_mapping(X2,netstr_restr_to_element(X2,X1,X0)),X3)
| ~ relation(the_mapping(X2,X1))
| ~ in(X3,the_carrier(netstr_restr_to_element(X2,X1,X0)))
| ~ function(the_mapping(X2,X1))
| empty_carrier(X2)
| ~ net_str(X1,X2)
| empty_carrier(X1)
| ~ element(X0,the_carrier(X1))
| ~ one_sorted_str(X2) ),
inference(superposition,[],[f4963,f9643]) ).
fof(f9678,plain,
! [X2,X3,X0,X1] :
( apply(the_mapping(X2,X1),X3) = apply(the_mapping(X2,netstr_restr_to_element(X2,X1,X0)),X3)
| ~ in(X3,the_carrier(netstr_restr_to_element(X2,X1,X0)))
| ~ function(the_mapping(X2,X1))
| empty_carrier(X2)
| ~ net_str(X1,X2)
| empty_carrier(X1)
| ~ element(X0,the_carrier(X1))
| ~ one_sorted_str(X2) ),
inference(forward_subsumption_resolution,[],[f9671,f2875]) ).
fof(f9683,plain,
! [X2,X3,X0,X1] :
( apply(the_mapping(X2,X1),X3) = apply(the_mapping(X2,netstr_restr_to_element(X2,X1,X0)),X3)
| ~ in(X3,the_carrier(netstr_restr_to_element(X2,X1,X0)))
| empty_carrier(X2)
| ~ net_str(X1,X2)
| empty_carrier(X1)
| ~ element(X0,the_carrier(X1))
| ~ one_sorted_str(X2) ),
inference(forward_subsumption_resolution,[],[f9678,f2874]) ).
fof(f9698,plain,
! [X0] :
( apply(the_mapping(sK540,sK541),X0) = apply(the_mapping(sK540,sF580),X0)
| ~ in(X0,the_carrier(sF580))
| empty_carrier(sK540)
| ~ net_str(sK541,sK540)
| empty_carrier(sK541)
| ~ element(sK542,the_carrier(sK541))
| ~ one_sorted_str(sK540) ),
inference(superposition,[],[f9683,f6538]) ).
fof(f9706,plain,
! [X0] :
( apply(the_mapping(sK540,sK541),X0) = apply(the_mapping(sK540,sF580),X0)
| ~ in(X0,the_carrier(sF580))
| ~ net_str(sK541,sK540)
| empty_carrier(sK541)
| ~ element(sK542,the_carrier(sK541))
| ~ one_sorted_str(sK540) ),
inference(forward_subsumption_resolution,[],[f9698,f4664]) ).
fof(f9709,plain,
! [X0] :
( apply(the_mapping(sK540,sK541),X0) = apply(the_mapping(sK540,sF580),X0)
| ~ in(X0,the_carrier(sF580))
| empty_carrier(sK541)
| ~ element(sK542,the_carrier(sK541))
| ~ one_sorted_str(sK540) ),
inference(forward_subsumption_resolution,[],[f9706,f4660]) ).
fof(f9710,plain,
! [X0] :
( apply(the_mapping(sK540,sK541),X0) = apply(the_mapping(sK540,sF580),X0)
| ~ in(X0,the_carrier(sF580))
| ~ element(sK542,the_carrier(sK541))
| ~ one_sorted_str(sK540) ),
inference(forward_subsumption_resolution,[],[f9709,f4662]) ).
fof(f9711,plain,
! [X0] :
( apply(the_mapping(sK540,sK541),X0) = apply(the_mapping(sK540,sF580),X0)
| ~ in(X0,the_carrier(sF580))
| ~ element(sK542,the_carrier(sK541)) ),
inference(forward_subsumption_resolution,[],[f9710,f4663]) ).
fof(f9712,plain,
! [X0] :
( ~ in(X0,sF583)
| apply(the_mapping(sK540,sK541),X0) = apply(the_mapping(sK540,sF580),X0)
| ~ element(sK542,the_carrier(sK541)) ),
inference(forward_demodulation,[],[f9711,f6545]) ).
fof(f9713,plain,
! [X0] :
( ~ element(sK542,sF579)
| ~ in(X0,sF583)
| apply(the_mapping(sK540,sK541),X0) = apply(the_mapping(sK540,sF580),X0) ),
inference(forward_demodulation,[],[f9712,f6534]) ).
fof(f9714,plain,
! [X0] :
( apply(the_mapping(sK540,sK541),X0) = apply(the_mapping(sK540,sF580),X0)
| ~ in(X0,sF583) ),
inference(forward_subsumption_resolution,[],[f9713,f6535]) ).
fof(f9716,plain,
! [X0] :
( apply_netmap(sK540,sF580,X0) = apply(the_mapping(sK540,sK541),X0)
| empty_carrier(sK540)
| ~ net_str(sF580,sK540)
| empty_carrier(sF580)
| ~ element(X0,the_carrier(sF580))
| ~ one_sorted_str(sK540)
| ~ one_sorted_str(sF580)
| ~ in(X0,sF583) ),
inference(superposition,[],[f7784,f9714]) ).
fof(f9718,plain,
! [X0] :
( apply_netmap(sK540,sF580,X0) = apply(the_mapping(sK540,sK541),X0)
| ~ net_str(sF580,sK540)
| empty_carrier(sF580)
| ~ element(X0,the_carrier(sF580))
| ~ one_sorted_str(sK540)
| ~ one_sorted_str(sF580)
| ~ in(X0,sF583) ),
inference(forward_subsumption_resolution,[],[f9716,f4664]) ).
fof(f9720,plain,
! [X0] :
( apply_netmap(sK540,sF580,X0) = apply(the_mapping(sK540,sK541),X0)
| empty_carrier(sF580)
| ~ element(X0,the_carrier(sF580))
| ~ one_sorted_str(sK540)
| ~ one_sorted_str(sF580)
| ~ in(X0,sF583) ),
inference(forward_subsumption_resolution,[],[f9718,f6814]) ).
fof(f9722,plain,
! [X0] :
( apply_netmap(sK540,sF580,X0) = apply(the_mapping(sK540,sK541),X0)
| ~ element(X0,the_carrier(sF580))
| ~ one_sorted_str(sK540)
| ~ one_sorted_str(sF580)
| ~ in(X0,sF583) ),
inference(forward_subsumption_resolution,[],[f9720,f6849]) ).
fof(f9724,plain,
! [X0] :
( apply_netmap(sK540,sF580,X0) = apply(the_mapping(sK540,sK541),X0)
| ~ element(X0,the_carrier(sF580))
| ~ one_sorted_str(sF580)
| ~ in(X0,sF583) ),
inference(forward_subsumption_resolution,[],[f9722,f4663]) ).
fof(f9726,plain,
! [X0] :
( apply_netmap(sK540,sF580,X0) = apply(the_mapping(sK540,sK541),X0)
| ~ element(X0,the_carrier(sF580))
| ~ in(X0,sF583) ),
inference(forward_subsumption_resolution,[],[f9724,f7042]) ).
fof(f9728,plain,
! [X0] :
( ~ element(X0,sF583)
| apply_netmap(sK540,sF580,X0) = apply(the_mapping(sK540,sK541),X0)
| ~ in(X0,sF583) ),
inference(forward_demodulation,[],[f9726,f6545]) ).
fof(f9730,plain,
! [X0] :
( apply_netmap(sK540,sF580,X0) = apply(the_mapping(sK540,sK541),X0)
| ~ in(X0,sF583) ),
inference(forward_subsumption_resolution,[],[f9728,f4693]) ).
fof(f9733,plain,
! [X0] :
( apply_netmap(sK540,sF580,X0) = apply_netmap(sK540,sK541,X0)
| empty_carrier(sK540)
| ~ net_str(sK541,sK540)
| empty_carrier(sK541)
| ~ element(X0,the_carrier(sK541))
| ~ one_sorted_str(sK540)
| ~ one_sorted_str(sK541)
| ~ in(X0,sF583) ),
inference(superposition,[],[f7784,f9730]) ).
fof(f9735,plain,
! [X0] :
( apply_netmap(sK540,sF580,X0) = apply_netmap(sK540,sK541,X0)
| ~ net_str(sK541,sK540)
| empty_carrier(sK541)
| ~ element(X0,the_carrier(sK541))
| ~ one_sorted_str(sK540)
| ~ one_sorted_str(sK541)
| ~ in(X0,sF583) ),
inference(forward_subsumption_resolution,[],[f9733,f4664]) ).
fof(f9737,plain,
! [X0] :
( apply_netmap(sK540,sF580,X0) = apply_netmap(sK540,sK541,X0)
| empty_carrier(sK541)
| ~ element(X0,the_carrier(sK541))
| ~ one_sorted_str(sK540)
| ~ one_sorted_str(sK541)
| ~ in(X0,sF583) ),
inference(forward_subsumption_resolution,[],[f9735,f4660]) ).
fof(f9739,plain,
! [X0] :
( apply_netmap(sK540,sF580,X0) = apply_netmap(sK540,sK541,X0)
| ~ element(X0,the_carrier(sK541))
| ~ one_sorted_str(sK540)
| ~ one_sorted_str(sK541)
| ~ in(X0,sF583) ),
inference(forward_subsumption_resolution,[],[f9737,f4662]) ).
fof(f9741,plain,
! [X0] :
( apply_netmap(sK540,sF580,X0) = apply_netmap(sK540,sK541,X0)
| ~ element(X0,the_carrier(sK541))
| ~ one_sorted_str(sK541)
| ~ in(X0,sF583) ),
inference(forward_subsumption_resolution,[],[f9739,f4663]) ).
fof(f9743,plain,
! [X0] :
( apply_netmap(sK540,sF580,X0) = apply_netmap(sK540,sK541,X0)
| ~ element(X0,the_carrier(sK541))
| ~ in(X0,sF583) ),
inference(forward_subsumption_resolution,[],[f9741,f6953]) ).
fof(f9745,plain,
! [X0] :
( ~ element(X0,sF579)
| apply_netmap(sK540,sF580,X0) = apply_netmap(sK540,sK541,X0)
| ~ in(X0,sF583) ),
inference(forward_demodulation,[],[f9743,f6534]) ).
fof(f9747,plain,
! [X0] :
( apply_netmap(sK540,sF580,X0) = apply_netmap(sK540,sK541,X0)
| ~ in(X0,sF583) ),
inference(forward_subsumption_resolution,[],[f9745,f6919]) ).
fof(f9749,plain,
( apply_netmap(sK540,sK541,sK544) = sF581
| ~ in(sK544,sF583) ),
inference(superposition,[],[f9747,f6540]) ).
fof(f9756,plain,
apply_netmap(sK540,sK541,sK544) = sF581,
inference(forward_subsumption_resolution,[],[f9749,f7058]) ).
fof(f9773,plain,
sF581 = sF582,
inference(superposition,[],[f6542,f9756]) ).
fof(f9774,plain,
$false,
inference(forward_subsumption_resolution,[],[f9773,f6543]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SEU385+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.38 % Computer : n004.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Mon Sep 28 05:03:03 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.10/0.42 Running first-order theorem proving
% 0.10/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
% 13.44/2.89 % (4164087)Detected formulas, will run a generic FOF schedule.
% 13.44/2.89 % (4164094)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=2374141031:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 13.44/2.89 % (4164095)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1688227441:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 13.44/2.89 % (4164092)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=2960147287:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 13.44/2.89 % (4164093)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=4256100175:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 13.44/2.89 % (4164096)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=694422189:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 13.44/2.89 % (4164097)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=290246119:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 13.44/2.89 % (4164098)dis-21_1_sil=8000:lcm=predicate:random_seed=1078622482:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/129Mi)
% 13.44/2.89 % (4164095)Instruction limit reached!
% 13.44/2.89 % (4164095)------------------------------
% 13.44/2.89 % (4164095)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.44/2.89 % (4164095)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.44/2.89 % (4164095)CaDiCaL version: 2.1.3
% 13.44/2.89 % (4164095)Termination reason: Instruction limit
% 13.44/2.89 % (4164095)Termination phase: Blocked clause elimination
% 13.44/2.89 % (4164095)Time elapsed: 0.061 s
% 13.44/2.89 % (4164095)Peak memory usage: 90 MB
% 13.44/2.89 % (4164095)Instructions burned: 110 (million)
% 13.44/2.89 % (4164098)Instruction limit reached!
% 13.44/2.89 % (4164098)------------------------------
% 13.44/2.89 % (4164098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.44/2.89 % (4164098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.44/2.89 % (4164098)CaDiCaL version: 2.1.3
% 13.44/2.89 % (4164098)Termination reason: Instruction limit
% 13.44/2.89 % (4164098)Termination phase: Saturation
% 13.44/2.89 % (4164098)Time elapsed: 0.067 s
% 13.44/2.89 % (4164098)Peak memory usage: 92 MB
% 13.44/2.89 % (4164098)Instructions burned: 130 (million)
% 13.44/2.89 % (4164096)Instruction limit reached!
% 13.44/2.89 % (4164096)------------------------------
% 13.44/2.89 % (4164096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.44/2.89 % (4164096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.44/2.89 % (4164096)CaDiCaL version: 2.1.3
% 13.44/2.89 % (4164096)Termination reason: Instruction limit
% 13.44/2.89 % (4164096)Termination phase: Saturation
% 13.44/2.89 % (4164096)Time elapsed: 0.069 s
% 13.44/2.89 % (4164096)Peak memory usage: 92 MB
% 13.44/2.89 % (4164096)Instructions burned: 120 (million)
% 13.44/2.89 % (4164097)Instruction limit reached!
% 13.44/2.89 % (4164097)------------------------------
% 13.44/2.89 % (4164097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 13.44/2.89 % (4164097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 13.44/2.89 % (4164097)CaDiCaL version: 2.1.3
% 13.44/2.89 % (4164097)Termination reason: Instruction limit
% 13.44/2.89 % (4164097)Termination phase: Saturation
% 13.44/2.89 % (4164097)Time elapsed: 0.078 s
% 13.44/2.89 % (4164097)Peak memory usage: 92 MB
% 13.44/2.89 % (4164097)Instructions burned: 139 (million)
% 13.44/2.89 % (4164106)lrs+10_1_sil=8000:sp=occurrence:random_seed=2672543243:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 13.44/2.89 % (4164107)lrs+10_1_sil=32000:urr=on:br=off:random_seed=1083337089:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 13.44/2.89 % (4164108)lrs+1011_1_sil=32000:sp=occurrence:random_seed=4106678545:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 13.44/2.89 % (4164109)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=3512014280:s2a=on:i=248:s2at=1.23:gtg=position_2997 on theBenchmark for (2997ds/248Mi)
% 13.44/2.89 % (4164107)Instruction limit reached!
% 19.61/3.76 % (4164107)------------------------------
% 19.61/3.76 % (4164107)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.61/3.76 % (4164107)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.61/3.76 % (4164107)CaDiCaL version: 2.1.3
% 19.61/3.76 % (4164107)Termination reason: Instruction limit
% 19.61/3.76 % (4164107)Termination phase: Saturation
% 19.61/3.76 % (4164107)Time elapsed: 0.084 s
% 19.61/3.76 % (4164107)Peak memory usage: 92 MB
% 19.61/3.76 % (4164107)Instructions burned: 158 (million)
% 19.61/3.76 % (4164106)Instruction limit reached!
% 19.61/3.76 % (4164106)------------------------------
% 19.61/3.76 % (4164106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.61/3.76 % (4164106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.61/3.76 % (4164106)CaDiCaL version: 2.1.3
% 19.61/3.76 % (4164106)Termination reason: Instruction limit
% 19.61/3.76 % (4164106)Termination phase: Saturation
% 19.61/3.76 % (4164106)Time elapsed: 0.175 s
% 19.61/3.76 % (4164106)Peak memory usage: 95 MB
% 19.61/3.76 % (4164106)Instructions burned: 286 (million)
% 19.61/3.76 % (4164109)Instruction limit reached!
% 19.61/3.76 % (4164109)------------------------------
% 19.61/3.76 % (4164109)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.61/3.76 % (4164109)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.61/3.76 % (4164109)CaDiCaL version: 2.1.3
% 19.61/3.76 % (4164109)Termination reason: Instruction limit
% 19.61/3.76 % (4164109)Termination phase: Saturation
% 19.61/3.76 % (4164109)Time elapsed: 0.148 s
% 19.61/3.76 % (4164109)Peak memory usage: 95 MB
% 19.61/3.76 % (4164109)Instructions burned: 248 (million)
% 19.61/3.76 % (4164108)Instruction limit reached!
% 19.61/3.76 % (4164108)------------------------------
% 19.61/3.76 % (4164108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.61/3.76 % (4164108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.61/3.76 % (4164108)CaDiCaL version: 2.1.3
% 19.61/3.76 % (4164108)Termination reason: Instruction limit
% 19.61/3.76 % (4164108)Termination phase: Saturation
% 19.61/3.76 % (4164108)Time elapsed: 0.206 s
% 19.61/3.76 % (4164108)Peak memory usage: 95 MB
% 19.61/3.76 % (4164108)Instructions burned: 326 (million)
% 19.61/3.76 % (4164114)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=2017889467:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2995 on theBenchmark for (2995ds/294Mi)
% 19.61/3.76 % (4164115)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=2742861192:i=2350_2994 on theBenchmark for (2994ds/2350Mi)
% 19.61/3.76 % (4164116)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3535491333:cts=off:i=113:fsr=off:ss=included:sgt=4_2994 on theBenchmark for (2994ds/113Mi)
% 19.61/3.76 % (4164117)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3310179615:i=127:av=off:fsr=off:sup=off_2994 on theBenchmark for (2994ds/127Mi)
% 19.61/3.76 % (4164116)Instruction limit reached!
% 19.61/3.76 % (4164116)------------------------------
% 19.61/3.76 % (4164116)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.61/3.76 % (4164116)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.61/3.76 % (4164116)CaDiCaL version: 2.1.3
% 19.61/3.76 % (4164116)Termination reason: Instruction limit
% 19.61/3.76 % (4164116)Termination phase: Saturation
% 19.61/3.76 % (4164116)Time elapsed: 0.062 s
% 19.61/3.76 % (4164116)Peak memory usage: 92 MB
% 19.61/3.76 % (4164116)Instructions burned: 113 (million)
% 19.61/3.76 % (4164114)Instruction limit reached!
% 19.61/3.76 % (4164114)------------------------------
% 19.61/3.76 % (4164114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.61/3.76 % (4164114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.61/3.76 % (4164114)CaDiCaL version: 2.1.3
% 19.61/3.76 % (4164114)Termination reason: Instruction limit
% 19.61/3.76 % (4164114)Termination phase: Saturation
% 19.61/3.76 % (4164114)Time elapsed: 0.177 s
% 19.61/3.76 % (4164114)Peak memory usage: 94 MB
% 19.61/3.76 % (4164114)Instructions burned: 295 (million)
% 19.61/3.76 % (4164117)Instruction limit reached!
% 19.61/3.76 % (4164117)------------------------------
% 19.61/3.76 % (4164117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.61/3.76 % (4164117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.61/3.76 % (4164117)CaDiCaL version: 2.1.3
% 19.61/3.76 % (4164117)Termination reason: Instruction limit
% 35.05/5.87 % (4164117)Termination phase: Blocked clause elimination
% 35.05/5.87 % (4164117)Time elapsed: 0.071 s
% 35.05/5.87 % (4164117)Peak memory usage: 90 MB
% 35.05/5.87 % (4164117)Instructions burned: 127 (million)
% 35.05/5.87 % (4164122)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=173024599:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2992 on theBenchmark for (2992ds/114Mi)
% 35.05/5.87 % (4164123)lrs+10_1_sil=8000:sp=occurrence:random_seed=2875927574:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2992 on theBenchmark for (2992ds/907Mi)
% 35.05/5.87 % (4164122)Instruction limit reached!
% 35.05/5.87 % (4164122)------------------------------
% 35.05/5.87 % (4164122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.05/5.87 % (4164122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.05/5.87 % (4164122)CaDiCaL version: 2.1.3
% 35.05/5.87 % (4164122)Termination reason: Instruction limit
% 35.05/5.87 % (4164122)Termination phase: Saturation
% 35.05/5.87 % (4164122)Time elapsed: 0.067 s
% 35.05/5.87 % (4164122)Peak memory usage: 90 MB
% 35.05/5.87 % (4164122)Instructions burned: 115 (million)
% 35.05/5.87 % (4164124)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2701503052:i=437:sd=1:aac=none:ss=included_2991 on theBenchmark for (2991ds/437Mi)
% 35.05/5.87 % (4164128)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1513641522:i=5202:ss=axioms:sgt=16_2990 on theBenchmark for (2990ds/5202Mi)
% 35.05/5.87 % (4164124)Instruction limit reached!
% 35.05/5.87 % (4164124)------------------------------
% 35.05/5.87 % (4164124)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.05/5.87 % (4164124)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.05/5.87 % (4164124)CaDiCaL version: 2.1.3
% 35.05/5.87 % (4164124)Termination reason: Instruction limit
% 35.05/5.87 % (4164124)Termination phase: Saturation
% 35.05/5.87 % (4164124)Time elapsed: 0.261 s
% 35.05/5.87 % (4164124)Peak memory usage: 96 MB
% 35.05/5.87 % (4164124)Instructions burned: 437 (million)
% 35.05/5.87 % (4164130)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2400677146:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2987 on theBenchmark for (2987ds/134Mi)
% 35.05/5.87 % (4164130)Instruction limit reached!
% 35.05/5.87 % (4164130)------------------------------
% 35.05/5.87 % (4164130)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.05/5.87 % (4164130)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.05/5.87 % (4164130)CaDiCaL version: 2.1.3
% 35.05/5.87 % (4164130)Termination reason: Instruction limit
% 35.05/5.87 % (4164130)Termination phase: Property scanning
% 35.05/5.87 % (4164130)Time elapsed: 0.068 s
% 35.05/5.87 % (4164130)Peak memory usage: 90 MB
% 35.05/5.87 % (4164130)Instructions burned: 135 (million)
% 35.05/5.87 % (4164123)Instruction limit reached!
% 35.05/5.87 % (4164123)------------------------------
% 35.05/5.87 % (4164123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.05/5.87 % (4164123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.05/5.87 % (4164123)CaDiCaL version: 2.1.3
% 35.05/5.87 % (4164123)Termination reason: Instruction limit
% 35.05/5.87 % (4164123)Termination phase: Saturation
% 35.05/5.87 % (4164123)Time elapsed: 0.569 s
% 35.05/5.87 % (4164123)Peak memory usage: 105 MB
% 35.05/5.87 % (4164123)Instructions burned: 908 (million)
% 35.05/5.87 % (4164132)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=3137474545:st=8:i=592:sd=3:ep=RST:ss=axioms_2985 on theBenchmark for (2985ds/592Mi)
% 35.05/5.87 % (4164133)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=180054443:st=3:i=13193:sd=3:ss=axioms_2985 on theBenchmark for (2985ds/13193Mi)
% 35.05/5.87 % (4164132)Instruction limit reached!
% 35.05/5.87 % (4164132)------------------------------
% 35.05/5.87 % (4164132)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.05/5.87 % (4164132)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.05/5.87 % (4164132)CaDiCaL version: 2.1.3
% 35.05/5.87 % (4164132)Termination reason: Instruction limit
% 35.05/5.87 % (4164132)Termination phase: Saturation
% 35.05/5.87 % (4164132)Time elapsed: 0.355 s
% 35.05/5.87 % (4164132)Peak memory usage: 102 MB
% 35.05/5.87 % (4164132)Instructions burned: 593 (million)
% 35.05/5.87 % (4164136)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=730082799:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2980 on theBenchmark for (2980ds/125Mi)
% 35.05/5.87 % (4164115)Instruction limit reached!
% 35.05/5.87 % (4164115)------------------------------
% 35.05/5.87 % (4164115)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.05/5.87 % (4164115)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.05/5.87 % (4164115)CaDiCaL version: 2.1.3
% 35.05/5.87 % (4164115)Termination reason: Instruction limit
% 35.05/5.87 % (4164115)Termination phase: Saturation
% 35.05/5.87 % (4164115)Time elapsed: 1.446 s
% 35.05/5.87 % (4164115)Peak memory usage: 166 MB
% 35.05/5.87 % (4164115)Instructions burned: 2351 (million)
% 35.05/5.87 % (4164136)Instruction limit reached!
% 35.05/5.87 % (4164136)------------------------------
% 35.05/5.87 % (4164136)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.05/5.87 % (4164136)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.05/5.87 % (4164136)CaDiCaL version: 2.1.3
% 35.05/5.87 % (4164136)Termination reason: Instruction limit
% 35.05/5.87 % (4164136)Termination phase: Saturation
% 35.05/5.87 % (4164136)Time elapsed: 0.074 s
% 35.05/5.87 % (4164136)Peak memory usage: 92 MB
% 35.05/5.87 % (4164136)Instructions burned: 125 (million)
% 35.05/5.87 % (4164140)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3247827912:i=134:gtgl=5:slsql=off:gtg=exists_sym_2978 on theBenchmark for (2978ds/134Mi)
% 35.05/5.87 % (4164141)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=333876793:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2978 on theBenchmark for (2978ds/141Mi)
% 35.05/5.87 % (4164140)Instruction limit reached!
% 35.05/5.87 % (4164140)------------------------------
% 35.05/5.87 % (4164140)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.05/5.87 % (4164140)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.05/5.87 % (4164140)CaDiCaL version: 2.1.3
% 35.05/5.87 % (4164140)Termination reason: Instruction limit
% 35.05/5.87 % (4164140)Termination phase: Saturation
% 35.05/5.87 % (4164140)Time elapsed: 0.070 s
% 35.05/5.87 % (4164140)Peak memory usage: 92 MB
% 35.05/5.87 % (4164140)Instructions burned: 134 (million)
% 35.05/5.87 % (4164141)Instruction limit reached!
% 35.05/5.87 % (4164141)------------------------------
% 35.05/5.87 % (4164141)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.05/5.87 % (4164141)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.05/5.87 % (4164141)CaDiCaL version: 2.1.3
% 35.05/5.87 % (4164141)Termination reason: Instruction limit
% 35.05/5.87 % (4164141)Termination phase: Saturation
% 35.05/5.87 % (4164141)Time elapsed: 0.073 s
% 35.05/5.87 % (4164141)Peak memory usage: 91 MB
% 35.05/5.87 % (4164141)Instructions burned: 141 (million)
% 35.05/5.87 % (4164178)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3947034207:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2976 on theBenchmark for (2976ds/431Mi)
% 35.05/5.87 % (4164180)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=2089745258:i=6060:aac=none:ins=25_2976 on theBenchmark for (2976ds/6060Mi)
% 35.05/5.87 % (4164178)Instruction limit reached!
% 35.05/5.87 % (4164178)------------------------------
% 35.05/5.87 % (4164178)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.05/5.87 % (4164178)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.05/5.87 % (4164178)CaDiCaL version: 2.1.3
% 35.05/5.87 % (4164178)Termination reason: Instruction limit
% 35.05/5.87 % (4164178)Termination phase: Saturation
% 35.05/5.87 % (4164178)Time elapsed: 0.252 s
% 35.05/5.87 % (4164178)Peak memory usage: 96 MB
% 35.05/5.87 % (4164178)Instructions burned: 431 (million)
% 35.05/5.87 % (4164301)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=3982266896:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2973 on theBenchmark for (2973ds/150Mi)
% 35.05/5.87 % (4164301)Instruction limit reached!
% 35.05/5.87 % (4164301)------------------------------
% 35.05/5.87 % (4164301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.05/5.87 % (4164301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.05/5.87 % (4164301)CaDiCaL version: 2.1.3
% 35.05/5.87 % (4164301)Termination reason: Instruction limit
% 35.05/5.87 % (4164301)Termination phase: Saturation
% 35.05/5.87 % (4164301)Time elapsed: 0.080 s
% 35.05/5.87 % (4164301)Peak memory usage: 93 MB
% 35.05/5.87 % (4164301)Instructions burned: 150 (million)
% 35.05/5.87 % (4164354)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1278131629:i=14155:bd=all_2971 on theBenchmark for (2971ds/14155Mi)
% 35.05/5.87 % (4164128)Instruction limit reached!
% 35.05/5.87 % (4164128)------------------------------
% 35.05/5.87 % (4164128)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.05/5.87 % (4164128)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.05/5.87 % (4164128)CaDiCaL version: 2.1.3
% 35.05/5.87 % (4164128)Termination reason: Instruction limit
% 35.05/5.87 % (4164128)Termination phase: Saturation
% 35.05/5.87 % (4164128)Time elapsed: 3.008 s
% 35.05/5.87 % (4164128)Peak memory usage: 163 MB
% 35.05/5.87 % (4164128)Instructions burned: 5202 (million)
% 35.05/5.87 % (4164393)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2761792278:i=667:av=off:fsr=off_2959 on theBenchmark for (2959ds/667Mi)
% 35.05/5.87 % (4164393)Instruction limit reached!
% 35.05/5.87 % (4164393)------------------------------
% 35.05/5.87 % (4164393)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.05/5.87 % (4164393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.05/5.87 % (4164393)CaDiCaL version: 2.1.3
% 35.05/5.87 % (4164393)Termination reason: Instruction limit
% 35.05/5.87 % (4164393)Termination phase: Saturation
% 35.05/5.87 % (4164393)Time elapsed: 0.321 s
% 35.05/5.87 % (4164393)Peak memory usage: 95 MB
% 35.05/5.87 % (4164393)Instructions burned: 667 (million)
% 35.05/5.87 % (4164395)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=2326785819:s2a=on:i=185:s2at=1.8:fdi=4_2954 on theBenchmark for (2954ds/185Mi)
% 35.05/5.87 % (4164180)First to succeed.
% 35.05/5.87 % (4164180)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4164087"
% 35.05/5.87 % (4164395)Instruction limit reached!
% 35.05/5.87 % (4164395)------------------------------
% 35.05/5.87 % (4164395)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.05/5.87 % (4164395)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.05/5.87 % (4164395)CaDiCaL version: 2.1.3
% 35.05/5.87 % (4164395)Termination reason: Instruction limit
% 35.05/5.87 % (4164395)Termination phase: Saturation
% 35.05/5.87 % (4164395)Time elapsed: 0.098 s
% 35.05/5.87 % (4164395)Peak memory usage: 93 MB
% 35.05/5.87 % (4164395)Instructions burned: 186 (million)
% 35.05/5.87 % (4164397)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=4023798658:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2952 on theBenchmark for (2952ds/193Mi)
% 35.05/5.87 % (4164180)Refutation found. Thanks to Tanya!
% 35.05/5.87 % SZS status Theorem for theBenchmark
% 35.05/5.87 % SZS output start Proof for theBenchmark
% See solution above
% 35.84/6.06 % (4164180)------------------------------
% 35.84/6.06 % (4164180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 35.84/6.06 % (4164180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 35.84/6.06 % (4164180)CaDiCaL version: 2.1.3
% 35.84/6.06 % (4164180)Termination reason: Refutation
% 35.84/6.06 % (4164180)Time elapsed: 2.296 s
% 35.84/6.06 % (4164180)Peak memory usage: 175 MB
% 35.84/6.06 % (4164180)Instructions burned: 3070 (million)
% 35.84/6.06 % (4164180)------------------------------
% 35.84/6.06 % (4164180)------------------------------
% 35.84/6.06 % (4164087)Success in time 5.008 s
% 35.84/6.06 % Vampire exiting
%------------------------------------------------------------------------------