%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU379+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 : n012.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:37 PM UTC 2026
% Result : Theorem 156.95s 34.13s
% Output : Refutation 236.61s
% Verified :
% SZS Type : Refutation
% Derivation depth : 48
% Number of leaves : 26
% Syntax : Number of formulae : 226 ( 21 unt; 1 def)
% Number of atoms : 1349 ( 85 equ)
% Maximal formula atoms : 18 ( 5 avg)
% Number of connectives : 1943 ( 820 ~; 913 |; 144 &)
% ( 21 <=>; 45 =>; 0 <=; 0 <~>)
% Maximal formula depth : 24 ( 9 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 23 ( 21 usr; 1 prp; 0-3 aty)
% Number of functors : 22 ( 22 usr; 5 con; 0-4 aty)
% Number of variables : 550 ( 532 !; 18 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f28,axiom,
! [X0,X1,X2] :
( element(X2,powerset(cartesian_product2(X0,X1)))
=> relation(X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',cc1_relset_1) ).
fof(f74,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0) )
=> ! [X1] :
( ( ~ empty_carrier(X1)
& net_str(X1,X0) )
=> ! [X2] :
( is_eventually_in(X0,X1,X2)
<=> ? [X3] :
( element(X3,the_carrier(X1))
& ! [X4] :
( element(X4,the_carrier(X1))
=> ( related(X1,X3,X4)
=> in(apply_netmap(X0,X1,X4),X2) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d11_waybel_0) ).
fof(f81,axiom,
! [X0] :
( ( relation(X0)
& function(X0) )
=> ! [X1,X2] :
( X2 = relation_inverse_image(X0,X1)
<=> ! [X3] :
( in(X3,X2)
<=> ( in(X3,relation_dom(X0))
& in(apply(X0,X3),X1) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d13_funct_1) ).
fof(f86,axiom,
! [X0] :
( one_sorted_str(X0)
=> ! [X1] :
( net_str(X1,X0)
=> ! [X2,X3] :
( ( strict_net_str(X3,X0)
& subnetstr(X3,X0,X1) )
=> ( X3 = preimage_subnetstr(X0,X1,X2)
<=> ( full_subrelstr(X3,X1)
& subrelstr(X3,X1)
& the_carrier(X3) = function_invverse_img_as_carrier_subset(X1,X0,the_mapping(X0,X1),X2) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d13_yellow_6) ).
fof(f109,axiom,
! [X0] :
( one_sorted_str(X0)
=> ( empty_carrier(X0)
<=> empty(the_carrier(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d1_struct_0) ).
fof(f128,axiom,
! [X0,X1] :
( ( ~ empty(X0)
=> ( element(X1,X0)
<=> in(X1,X0) ) )
& ( empty(X0)
=> ( element(X1,X0)
<=> empty(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_subset_1) ).
fof(f184,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(f187,axiom,
! [X0] :
( one_sorted_str(X0)
=> ! [X1] :
( net_str(X1,X0)
=> ! [X2] :
( net_str(X2,X0)
=> ( subnetstr(X2,X0,X1)
<=> ( subrelstr(X2,X1)
& the_mapping(X0,X2) = relation_dom_restr_as_relation_of(the_carrier(X1),the_carrier(X0),the_mapping(X0,X1),the_carrier(X2)) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_yellow_6) ).
fof(f220,axiom,
! [X0,X1] :
( rel_str(X0)
=> element(join_on_relstr(X0,X1),the_carrier(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k1_yellow_0) ).
fof(f258,axiom,
! [X0,X1,X2,X3] :
( ( one_sorted_str(X0)
& 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(function_invverse_img_as_carrier_subset(X0,X1,X2,X3),powerset(the_carrier(X0))) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k5_pre_topc) ).
fof(f268,axiom,
! [X0,X1,X2] :
( ( one_sorted_str(X0)
& net_str(X1,X0) )
=> ( strict_net_str(preimage_subnetstr(X0,X1,X2),X0)
& subnetstr(preimage_subnetstr(X0,X1,X2),X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_k6_yellow_6) ).
fof(f280,axiom,
! [X0] :
( rel_str(X0)
=> one_sorted_str(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_orders_2) ).
fof(f283,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(f290,axiom,
! [X0,X1] :
( ( one_sorted_str(X0)
& net_str(X1,X0) )
=> ! [X2] :
( subnetstr(X2,X0,X1)
=> net_str(X2,X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m1_yellow_6) ).
fof(f291,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(f292,axiom,
! [X0,X1] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0)
& ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) )
=> ! [X2] :
( subnet(X2,X0,X1)
=> ( ~ empty_carrier(X2)
& transitive_relstr(X2)
& directed_relstr(X2)
& net_str(X2,X0) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_m2_yellow_6) ).
fof(f297,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(f493,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(f503,axiom,
! [X0,X1,X2,X3] :
( ( one_sorted_str(X0)
& one_sorted_str(X1)
& function(X2)
& quasi_total(X2,the_carrier(X0),the_carrier(X1))
& relation_of2(X2,the_carrier(X0),the_carrier(X1)) )
=> function_invverse_img_as_carrier_subset(X0,X1,X2,X3) = relation_inverse_image(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k5_pre_topc) ).
fof(f512,axiom,
! [X0,X1,X2,X3] :
( relation_of2(X2,X0,X1)
=> relation_dom_restr_as_relation_of(X0,X1,X2,X3) = relation_dom_restriction(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',redefinition_k8_relset_1) ).
fof(f513,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(f625,axiom,
! [X0,X1] :
( in(X0,X1)
=> element(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
fof(f685,conjecture,
! [X0] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0) )
=> ! [X1] :
( ( ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) )
=> ! [X2,X3] :
( subnet(X3,X0,X1)
=> ( X3 = preimage_subnetstr(X0,X1,X2)
=> is_eventually_in(X0,X3,X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t32_yellow_6) ).
fof(f686,negated_conjecture,
~ ! [X0] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0) )
=> ! [X1] :
( ( ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) )
=> ! [X2,X3] :
( subnet(X3,X0,X1)
=> ( X3 = preimage_subnetstr(X0,X1,X2)
=> is_eventually_in(X0,X3,X2) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f685]) ).
fof(f732,axiom,
! [X0,X1,X2] :
( ( in(X0,X1)
& element(X1,powerset(X2)) )
=> element(X0,X2) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t4_subset) ).
fof(f773,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(f1100,plain,
? [X0] :
( ? [X1] :
( ? [X2,X3] :
( ~ is_eventually_in(X0,X3,X2)
& X3 = preimage_subnetstr(X0,X1,X2)
& subnet(X3,X0,X1) )
& ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) )
& ~ empty_carrier(X0)
& one_sorted_str(X0) ),
inference(ennf_transformation,[],[f686]) ).
fof(f1101,plain,
? [X0] :
( ? [X1] :
( ? [X2,X3] :
( ~ is_eventually_in(X0,X3,X2)
& X3 = preimage_subnetstr(X0,X1,X2)
& subnet(X3,X0,X1) )
& ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) )
& ~ empty_carrier(X0)
& one_sorted_str(X0) ),
inference(flattening,[],[f1100]) ).
fof(f1205,plain,
! [X0,X1,X2] :
( apply(relation_dom_restriction(X2,X0),X1) = apply(X2,X1)
| ~ in(X1,X0)
| ~ relation(X2)
| ~ function(X2) ),
inference(ennf_transformation,[],[f773]) ).
fof(f1206,plain,
! [X0,X1,X2] :
( apply(relation_dom_restriction(X2,X0),X1) = apply(X2,X1)
| ~ in(X1,X0)
| ~ relation(X2)
| ~ function(X2) ),
inference(flattening,[],[f1205]) ).
fof(f1232,plain,
! [X0,X1] :
( element(X0,X1)
| ~ in(X0,X1) ),
inference(ennf_transformation,[],[f625]) ).
fof(f1337,plain,
! [X0] :
( ! [X1,X2] :
( X2 = relation_inverse_image(X0,X1)
<=> ! [X3] :
( in(X3,X2)
<=> ( in(X3,relation_dom(X0))
& in(apply(X0,X3),X1) ) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(ennf_transformation,[],[f81]) ).
fof(f1338,plain,
! [X0] :
( ! [X1,X2] :
( X2 = relation_inverse_image(X0,X1)
<=> ! [X3] :
( in(X3,X2)
<=> ( in(X3,relation_dom(X0))
& in(apply(X0,X3),X1) ) ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(flattening,[],[f1337]) ).
fof(f1360,plain,
! [X0,X1,X2] :
( element(X0,X2)
| ~ in(X0,X1)
| ~ element(X1,powerset(X2)) ),
inference(ennf_transformation,[],[f732]) ).
fof(f1361,plain,
! [X0,X1,X2] :
( element(X0,X2)
| ~ in(X0,X1)
| ~ element(X1,powerset(X2)) ),
inference(flattening,[],[f1360]) ).
fof(f1366,plain,
! [X0] :
( ( empty_carrier(X0)
<=> empty(the_carrier(X0)) )
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f109]) ).
fof(f1402,plain,
! [X0,X1,X2] :
( element(X2,powerset(cartesian_product2(X0,X1)))
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(ennf_transformation,[],[f291]) ).
fof(f1410,plain,
! [X0,X1,X2] :
( relation(X2)
| ~ element(X2,powerset(cartesian_product2(X0,X1))) ),
inference(ennf_transformation,[],[f28]) ).
fof(f1411,plain,
! [X0,X1,X2,X3] :
( relation_dom_restr_as_relation_of(X0,X1,X2,X3) = relation_dom_restriction(X2,X3)
| ~ relation_of2(X2,X0,X1) ),
inference(ennf_transformation,[],[f512]) ).
fof(f1423,plain,
! [X0,X1] :
( ( ( element(X1,X0)
<=> in(X1,X0) )
| empty(X0) )
& ( ( element(X1,X0)
<=> empty(X1) )
| ~ empty(X0) ) ),
inference(ennf_transformation,[],[f128]) ).
fof(f1453,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,[],[f493]) ).
fof(f1454,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,[],[f1453]) ).
fof(f1455,plain,
! [X0] :
( one_sorted_str(X0)
| ~ rel_str(X0) ),
inference(ennf_transformation,[],[f280]) ).
fof(f1483,plain,
! [X0,X1] :
( ! [X2] :
( ( ~ empty_carrier(X2)
& transitive_relstr(X2)
& directed_relstr(X2)
& net_str(X2,X0) )
| ~ subnet(X2,X0,X1) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0) ),
inference(ennf_transformation,[],[f292]) ).
fof(f1484,plain,
! [X0,X1] :
( ! [X2] :
( ( ~ empty_carrier(X2)
& transitive_relstr(X2)
& directed_relstr(X2)
& net_str(X2,X0) )
| ~ subnet(X2,X0,X1) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0) ),
inference(flattening,[],[f1483]) ).
fof(f1566,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,[],[f297]) ).
fof(f1567,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,[],[f1566]) ).
fof(f1576,plain,
! [X0,X1,X2,X3] :
( function_invverse_img_as_carrier_subset(X0,X1,X2,X3) = relation_inverse_image(X2,X3)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X1)
| ~ function(X2)
| ~ quasi_total(X2,the_carrier(X0),the_carrier(X1))
| ~ relation_of2(X2,the_carrier(X0),the_carrier(X1)) ),
inference(ennf_transformation,[],[f503]) ).
fof(f1577,plain,
! [X0,X1,X2,X3] :
( function_invverse_img_as_carrier_subset(X0,X1,X2,X3) = relation_inverse_image(X2,X3)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X1)
| ~ function(X2)
| ~ quasi_total(X2,the_carrier(X0),the_carrier(X1))
| ~ relation_of2(X2,the_carrier(X0),the_carrier(X1)) ),
inference(flattening,[],[f1576]) ).
fof(f1599,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( is_eventually_in(X0,X1,X2)
<=> ? [X3] :
( element(X3,the_carrier(X1))
& ! [X4] :
( in(apply_netmap(X0,X1,X4),X2)
| ~ related(X1,X3,X4)
| ~ element(X4,the_carrier(X1)) ) ) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f74]) ).
fof(f1600,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( is_eventually_in(X0,X1,X2)
<=> ? [X3] :
( element(X3,the_carrier(X1))
& ! [X4] :
( in(apply_netmap(X0,X1,X4),X2)
| ~ related(X1,X3,X4)
| ~ element(X4,the_carrier(X1)) ) ) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(flattening,[],[f1599]) ).
fof(f1629,plain,
! [X0,X1] :
( ! [X2] :
( net_str(X2,X0)
| ~ subnetstr(X2,X0,X1) )
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(ennf_transformation,[],[f290]) ).
fof(f1630,plain,
! [X0,X1] :
( ! [X2] :
( net_str(X2,X0)
| ~ subnetstr(X2,X0,X1) )
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(flattening,[],[f1629]) ).
fof(f1631,plain,
! [X0] :
( ! [X1] :
( rel_str(X1)
| ~ net_str(X1,X0) )
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f283]) ).
fof(f1632,plain,
! [X0,X1,X2] :
( ( strict_net_str(preimage_subnetstr(X0,X1,X2),X0)
& subnetstr(preimage_subnetstr(X0,X1,X2),X0,X1) )
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(ennf_transformation,[],[f268]) ).
fof(f1633,plain,
! [X0,X1,X2] :
( ( strict_net_str(preimage_subnetstr(X0,X1,X2),X0)
& subnetstr(preimage_subnetstr(X0,X1,X2),X0,X1) )
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(flattening,[],[f1632]) ).
fof(f1639,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( subnetstr(X2,X0,X1)
<=> ( subrelstr(X2,X1)
& the_mapping(X0,X2) = relation_dom_restr_as_relation_of(the_carrier(X1),the_carrier(X0),the_mapping(X0,X1),the_carrier(X2)) ) )
| ~ net_str(X2,X0) )
| ~ net_str(X1,X0) )
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f187]) ).
fof(f1640,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,[],[f184]) ).
fof(f1641,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,[],[f1640]) ).
fof(f1642,plain,
! [X0] :
( ! [X1] :
( ! [X2,X3] :
( ( X3 = preimage_subnetstr(X0,X1,X2)
<=> ( full_subrelstr(X3,X1)
& subrelstr(X3,X1)
& the_carrier(X3) = function_invverse_img_as_carrier_subset(X1,X0,the_mapping(X0,X1),X2) ) )
| ~ strict_net_str(X3,X0)
| ~ subnetstr(X3,X0,X1) )
| ~ net_str(X1,X0) )
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f86]) ).
fof(f1643,plain,
! [X0] :
( ! [X1] :
( ! [X2,X3] :
( ( X3 = preimage_subnetstr(X0,X1,X2)
<=> ( full_subrelstr(X3,X1)
& subrelstr(X3,X1)
& the_carrier(X3) = function_invverse_img_as_carrier_subset(X1,X0,the_mapping(X0,X1),X2) ) )
| ~ strict_net_str(X3,X0)
| ~ subnetstr(X3,X0,X1) )
| ~ net_str(X1,X0) )
| ~ one_sorted_str(X0) ),
inference(flattening,[],[f1642]) ).
fof(f1676,plain,
! [X0,X1,X2,X3] :
( element(function_invverse_img_as_carrier_subset(X0,X1,X2,X3),powerset(the_carrier(X0)))
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X1)
| ~ function(X2)
| ~ quasi_total(X2,the_carrier(X0),the_carrier(X1))
| ~ relation_of2(X2,the_carrier(X0),the_carrier(X1)) ),
inference(ennf_transformation,[],[f258]) ).
fof(f1677,plain,
! [X0,X1,X2,X3] :
( element(function_invverse_img_as_carrier_subset(X0,X1,X2,X3),powerset(the_carrier(X0)))
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X1)
| ~ function(X2)
| ~ quasi_total(X2,the_carrier(X0),the_carrier(X1))
| ~ relation_of2(X2,the_carrier(X0),the_carrier(X1)) ),
inference(flattening,[],[f1676]) ).
fof(f1769,plain,
! [X0,X1] :
( element(join_on_relstr(X0,X1),the_carrier(X0))
| ~ rel_str(X0) ),
inference(ennf_transformation,[],[f220]) ).
fof(f2157,plain,
( ~ is_eventually_in(sK209,sK212,sK211)
& sK212 = preimage_subnetstr(sK209,sK210,sK211)
& subnet(sK212,sK209,sK210)
& ~ empty_carrier(sK210)
& transitive_relstr(sK210)
& directed_relstr(sK210)
& net_str(sK210,sK209)
& ~ empty_carrier(sK209)
& one_sorted_str(sK209) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK209,sK210,sK211,sK212]),skolemize(X0,sK209),skolemize(X1,sK210),skolemize(X2,sK211),skolemize(X3,sK212)],[f1101]) ).
fof(f2430,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = relation_inverse_image(X0,X1)
| ? [X3] :
( ( ~ in(X3,relation_dom(X0))
| ~ in(apply(X0,X3),X1)
| ~ in(X3,X2) )
& ( ( in(X3,relation_dom(X0))
& in(apply(X0,X3),X1) )
| in(X3,X2) ) ) )
& ( ! [X3] :
( ( in(X3,X2)
| ~ in(X3,relation_dom(X0))
| ~ in(apply(X0,X3),X1) )
& ( ( in(X3,relation_dom(X0))
& in(apply(X0,X3),X1) )
| ~ in(X3,X2) ) )
| relation_inverse_image(X0,X1) != X2 ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(nnf_transformation,[],[f1338]) ).
fof(f2431,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = relation_inverse_image(X0,X1)
| ? [X3] :
( ( ~ in(X3,relation_dom(X0))
| ~ in(apply(X0,X3),X1)
| ~ in(X3,X2) )
& ( ( in(X3,relation_dom(X0))
& in(apply(X0,X3),X1) )
| in(X3,X2) ) ) )
& ( ! [X3] :
( ( in(X3,X2)
| ~ in(X3,relation_dom(X0))
| ~ in(apply(X0,X3),X1) )
& ( ( in(X3,relation_dom(X0))
& in(apply(X0,X3),X1) )
| ~ in(X3,X2) ) )
| relation_inverse_image(X0,X1) != X2 ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(flattening,[],[f2430]) ).
fof(f2432,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = relation_inverse_image(X0,X1)
| ? [X3] :
( ( ~ in(X3,relation_dom(X0))
| ~ in(apply(X0,X3),X1)
| ~ in(X3,X2) )
& ( ( in(X3,relation_dom(X0))
& in(apply(X0,X3),X1) )
| in(X3,X2) ) ) )
& ( ! [X4] :
( ( in(X4,X2)
| ~ in(X4,relation_dom(X0))
| ~ in(apply(X0,X4),X1) )
& ( ( in(X4,relation_dom(X0))
& in(apply(X0,X4),X1) )
| ~ in(X4,X2) ) )
| relation_inverse_image(X0,X1) != X2 ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(rectify,[],[f2431]) ).
fof(f2433,plain,
! [X0] :
( ! [X1,X2] :
( ( X2 = relation_inverse_image(X0,X1)
| ( ( ~ in(sK410(X0,X1,X2),relation_dom(X0))
| ~ in(apply(X0,sK410(X0,X1,X2)),X1)
| ~ in(sK410(X0,X1,X2),X2) )
& ( ( in(sK410(X0,X1,X2),relation_dom(X0))
& in(apply(X0,sK410(X0,X1,X2)),X1) )
| in(sK410(X0,X1,X2),X2) ) ) )
& ( ! [X4] :
( ( in(X4,X2)
| ~ in(X4,relation_dom(X0))
| ~ in(apply(X0,X4),X1) )
& ( ( in(X4,relation_dom(X0))
& in(apply(X0,X4),X1) )
| ~ in(X4,X2) ) )
| relation_inverse_image(X0,X1) != X2 ) )
| ~ relation(X0)
| ~ function(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK410]),skolemize(X3,sK410(X0,X1,X2))],[f2432]) ).
fof(f2463,plain,
! [X0] :
( ( ( empty_carrier(X0)
| ~ empty(the_carrier(X0)) )
& ( empty(the_carrier(X0))
| ~ empty_carrier(X0) ) )
| ~ one_sorted_str(X0) ),
inference(nnf_transformation,[],[f1366]) ).
fof(f2490,plain,
! [X0,X1] :
( ( ( ( element(X1,X0)
| ~ in(X1,X0) )
& ( in(X1,X0)
| ~ element(X1,X0) ) )
| empty(X0) )
& ( ( ( element(X1,X0)
| ~ empty(X1) )
& ( empty(X1)
| ~ element(X1,X0) ) )
| ~ empty(X0) ) ),
inference(nnf_transformation,[],[f1423]) ).
fof(f2599,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,[],[f513]) ).
fof(f2627,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( is_eventually_in(X0,X1,X2)
| ! [X3] :
( ~ element(X3,the_carrier(X1))
| ? [X4] :
( ~ in(apply_netmap(X0,X1,X4),X2)
& related(X1,X3,X4)
& element(X4,the_carrier(X1)) ) ) )
& ( ? [X3] :
( element(X3,the_carrier(X1))
& ! [X4] :
( in(apply_netmap(X0,X1,X4),X2)
| ~ related(X1,X3,X4)
| ~ element(X4,the_carrier(X1)) ) )
| ~ is_eventually_in(X0,X1,X2) ) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(nnf_transformation,[],[f1600]) ).
fof(f2628,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( is_eventually_in(X0,X1,X2)
| ! [X3] :
( ~ element(X3,the_carrier(X1))
| ? [X4] :
( ~ in(apply_netmap(X0,X1,X4),X2)
& related(X1,X3,X4)
& element(X4,the_carrier(X1)) ) ) )
& ( ? [X5] :
( element(X5,the_carrier(X1))
& ! [X6] :
( in(apply_netmap(X0,X1,X6),X2)
| ~ related(X1,X5,X6)
| ~ element(X6,the_carrier(X1)) ) )
| ~ is_eventually_in(X0,X1,X2) ) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(rectify,[],[f2627]) ).
fof(f2629,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( is_eventually_in(X0,X1,X2)
| ! [X3] :
( ~ element(X3,the_carrier(X1))
| ( ~ in(apply_netmap(X0,X1,sK544(X0,X1,X2,X3)),X2)
& related(X1,X3,sK544(X0,X1,X2,X3))
& element(sK544(X0,X1,X2,X3),the_carrier(X1)) ) ) )
& ( ( element(sK545(X0,X1,X2),the_carrier(X1))
& ! [X6] :
( in(apply_netmap(X0,X1,X6),X2)
| ~ related(X1,sK545(X0,X1,X2),X6)
| ~ element(X6,the_carrier(X1)) ) )
| ~ is_eventually_in(X0,X1,X2) ) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK544,sK545]),skolemize(X4,sK544(X0,X1,X2,X3)),skolemize(X5,sK545(X0,X1,X2))],[f2628]) ).
fof(f2644,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( subnetstr(X2,X0,X1)
| ~ subrelstr(X2,X1)
| the_mapping(X0,X2) != relation_dom_restr_as_relation_of(the_carrier(X1),the_carrier(X0),the_mapping(X0,X1),the_carrier(X2)) )
& ( ( subrelstr(X2,X1)
& the_mapping(X0,X2) = relation_dom_restr_as_relation_of(the_carrier(X1),the_carrier(X0),the_mapping(X0,X1),the_carrier(X2)) )
| ~ subnetstr(X2,X0,X1) ) )
| ~ net_str(X2,X0) )
| ~ net_str(X1,X0) )
| ~ one_sorted_str(X0) ),
inference(nnf_transformation,[],[f1639]) ).
fof(f2645,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ( ( subnetstr(X2,X0,X1)
| ~ subrelstr(X2,X1)
| the_mapping(X0,X2) != relation_dom_restr_as_relation_of(the_carrier(X1),the_carrier(X0),the_mapping(X0,X1),the_carrier(X2)) )
& ( ( subrelstr(X2,X1)
& the_mapping(X0,X2) = relation_dom_restr_as_relation_of(the_carrier(X1),the_carrier(X0),the_mapping(X0,X1),the_carrier(X2)) )
| ~ subnetstr(X2,X0,X1) ) )
| ~ net_str(X2,X0) )
| ~ net_str(X1,X0) )
| ~ one_sorted_str(X0) ),
inference(flattening,[],[f2644]) ).
fof(f2646,plain,
! [X0] :
( ! [X1] :
( ! [X2,X3] :
( ( ( X3 = preimage_subnetstr(X0,X1,X2)
| ~ full_subrelstr(X3,X1)
| ~ subrelstr(X3,X1)
| the_carrier(X3) != function_invverse_img_as_carrier_subset(X1,X0,the_mapping(X0,X1),X2) )
& ( ( full_subrelstr(X3,X1)
& subrelstr(X3,X1)
& the_carrier(X3) = function_invverse_img_as_carrier_subset(X1,X0,the_mapping(X0,X1),X2) )
| preimage_subnetstr(X0,X1,X2) != X3 ) )
| ~ strict_net_str(X3,X0)
| ~ subnetstr(X3,X0,X1) )
| ~ net_str(X1,X0) )
| ~ one_sorted_str(X0) ),
inference(nnf_transformation,[],[f1643]) ).
fof(f2647,plain,
! [X0] :
( ! [X1] :
( ! [X2,X3] :
( ( ( X3 = preimage_subnetstr(X0,X1,X2)
| ~ full_subrelstr(X3,X1)
| ~ subrelstr(X3,X1)
| the_carrier(X3) != function_invverse_img_as_carrier_subset(X1,X0,the_mapping(X0,X1),X2) )
& ( ( full_subrelstr(X3,X1)
& subrelstr(X3,X1)
& the_carrier(X3) = function_invverse_img_as_carrier_subset(X1,X0,the_mapping(X0,X1),X2) )
| preimage_subnetstr(X0,X1,X2) != X3 ) )
| ~ strict_net_str(X3,X0)
| ~ subnetstr(X3,X0,X1) )
| ~ net_str(X1,X0) )
| ~ one_sorted_str(X0) ),
inference(flattening,[],[f2646]) ).
fof(f3209,plain,
one_sorted_str(sK209),
inference(cnf_transformation,[],[f2157]) ).
fof(f3210,plain,
~ empty_carrier(sK209),
inference(cnf_transformation,[],[f2157]) ).
fof(f3211,plain,
net_str(sK210,sK209),
inference(cnf_transformation,[],[f2157]) ).
fof(f3212,plain,
directed_relstr(sK210),
inference(cnf_transformation,[],[f2157]) ).
fof(f3213,plain,
transitive_relstr(sK210),
inference(cnf_transformation,[],[f2157]) ).
fof(f3214,plain,
~ empty_carrier(sK210),
inference(cnf_transformation,[],[f2157]) ).
fof(f3215,plain,
subnet(sK212,sK209,sK210),
inference(cnf_transformation,[],[f2157]) ).
fof(f3216,plain,
sK212 = preimage_subnetstr(sK209,sK210,sK211),
inference(cnf_transformation,[],[f2157]) ).
fof(f3217,plain,
~ is_eventually_in(sK209,sK212,sK211),
inference(cnf_transformation,[],[f2157]) ).
fof(f3373,plain,
! [X2,X0,X1] :
( apply(relation_dom_restriction(X2,X0),X1) = apply(X2,X1)
| ~ in(X1,X0)
| ~ relation(X2)
| ~ function(X2) ),
inference(cnf_transformation,[],[f1206]) ).
fof(f3415,plain,
! [X0,X1] :
( element(X0,X1)
| ~ in(X0,X1) ),
inference(cnf_transformation,[],[f1232]) ).
fof(f3904,plain,
! [X2,X0,X1,X4] :
( in(apply(X0,X4),X1)
| ~ in(X4,X2)
| relation_inverse_image(X0,X1) != X2
| ~ relation(X0)
| ~ function(X0) ),
inference(cnf_transformation,[],[f2433]) ).
fof(f3978,plain,
! [X2,X0,X1] :
( ~ element(X1,powerset(X2))
| ~ in(X0,X1)
| element(X0,X2) ),
inference(cnf_transformation,[],[f1361]) ).
fof(f3987,plain,
! [X0] :
( ~ empty(the_carrier(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f2463]) ).
fof(f4064,plain,
! [X2,X0,X1] :
( element(X2,powerset(cartesian_product2(X0,X1)))
| ~ relation_of2_as_subset(X2,X0,X1) ),
inference(cnf_transformation,[],[f1402]) ).
fof(f4072,plain,
! [X2,X0,X1] :
( ~ element(X2,powerset(cartesian_product2(X0,X1)))
| relation(X2) ),
inference(cnf_transformation,[],[f1410]) ).
fof(f4073,plain,
! [X2,X3,X0,X1] :
( relation_dom_restr_as_relation_of(X0,X1,X2,X3) = relation_dom_restriction(X2,X3)
| ~ relation_of2(X2,X0,X1) ),
inference(cnf_transformation,[],[f1411]) ).
fof(f4101,plain,
! [X0,X1] :
( ~ element(X1,X0)
| in(X1,X0)
| empty(X0) ),
inference(cnf_transformation,[],[f2490]) ).
fof(f4205,plain,
! [X2,X3,X0,X1] :
( apply(X2,X3) = apply_on_structs(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)) ),
inference(cnf_transformation,[],[f1454]) ).
fof(f4207,plain,
! [X0] :
( one_sorted_str(X0)
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f1455]) ).
fof(f4362,plain,
! [X2,X0,X1] :
( ~ subnet(X2,X0,X1)
| net_str(X2,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0) ),
inference(cnf_transformation,[],[f1484]) ).
fof(f4365,plain,
! [X2,X0,X1] :
( ~ subnet(X2,X0,X1)
| ~ empty_carrier(X2)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ transitive_relstr(X1)
| ~ directed_relstr(X1)
| ~ net_str(X1,X0) ),
inference(cnf_transformation,[],[f1484]) ).
fof(f4549,plain,
! [X2,X0,X1] :
( ~ relation_of2_as_subset(X2,X0,X1)
| relation_of2(X2,X0,X1) ),
inference(cnf_transformation,[],[f2599]) ).
fof(f4552,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,[],[f1567]) ).
fof(f4553,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,[],[f1567]) ).
fof(f4554,plain,
! [X0,X1] :
( function(the_mapping(X0,X1))
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(cnf_transformation,[],[f1567]) ).
fof(f4571,plain,
! [X2,X3,X0,X1] :
( function_invverse_img_as_carrier_subset(X0,X1,X2,X3) = relation_inverse_image(X2,X3)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X1)
| ~ function(X2)
| ~ quasi_total(X2,the_carrier(X0),the_carrier(X1))
| ~ relation_of2(X2,the_carrier(X0),the_carrier(X1)) ),
inference(cnf_transformation,[],[f1577]) ).
fof(f4628,plain,
! [X2,X3,X0,X1] :
( element(sK544(X0,X1,X2,X3),the_carrier(X1))
| ~ element(X3,the_carrier(X1))
| is_eventually_in(X0,X1,X2)
| empty_carrier(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f2629]) ).
fof(f4630,plain,
! [X2,X3,X0,X1] :
( ~ in(apply_netmap(X0,X1,sK544(X0,X1,X2,X3)),X2)
| ~ element(X3,the_carrier(X1))
| is_eventually_in(X0,X1,X2)
| empty_carrier(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f2629]) ).
fof(f4669,plain,
! [X2,X0,X1] :
( ~ subnetstr(X2,X0,X1)
| net_str(X2,X0)
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(cnf_transformation,[],[f1630]) ).
fof(f4670,plain,
! [X0,X1] :
( ~ net_str(X1,X0)
| rel_str(X1)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f1631]) ).
fof(f4671,plain,
! [X2,X0,X1] :
( subnetstr(preimage_subnetstr(X0,X1,X2),X0,X1)
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(cnf_transformation,[],[f1633]) ).
fof(f4672,plain,
! [X2,X0,X1] :
( strict_net_str(preimage_subnetstr(X0,X1,X2),X0)
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(cnf_transformation,[],[f1633]) ).
fof(f4679,plain,
! [X2,X0,X1] :
( the_mapping(X0,X2) = relation_dom_restr_as_relation_of(the_carrier(X1),the_carrier(X0),the_mapping(X0,X1),the_carrier(X2))
| ~ subnetstr(X2,X0,X1)
| ~ net_str(X2,X0)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f2645]) ).
fof(f4682,plain,
! [X2,X0,X1] :
( 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(cnf_transformation,[],[f1641]) ).
fof(f4683,plain,
! [X2,X3,X0,X1] :
( the_carrier(X3) = function_invverse_img_as_carrier_subset(X1,X0,the_mapping(X0,X1),X2)
| preimage_subnetstr(X0,X1,X2) != X3
| ~ strict_net_str(X3,X0)
| ~ subnetstr(X3,X0,X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f2647]) ).
fof(f4781,plain,
! [X2,X3,X0,X1] :
( element(function_invverse_img_as_carrier_subset(X0,X1,X2,X3),powerset(the_carrier(X0)))
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X1)
| ~ function(X2)
| ~ quasi_total(X2,the_carrier(X0),the_carrier(X1))
| ~ relation_of2(X2,the_carrier(X0),the_carrier(X1)) ),
inference(cnf_transformation,[],[f1677]) ).
fof(f4975,plain,
! [X0,X1] :
( element(join_on_relstr(X0,X1),the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f1769]) ).
fof(f5311,plain,
! [X0,X1,X4] :
( in(apply(X0,X4),X1)
| ~ in(X4,relation_inverse_image(X0,X1))
| ~ relation(X0)
| ~ function(X0) ),
inference(equality_resolution,[],[f3904]) ).
fof(f5361,plain,
! [X2,X0,X1] :
( function_invverse_img_as_carrier_subset(X1,X0,the_mapping(X0,X1),X2) = the_carrier(preimage_subnetstr(X0,X1,X2))
| ~ strict_net_str(preimage_subnetstr(X0,X1,X2),X0)
| ~ subnetstr(preimage_subnetstr(X0,X1,X2),X0,X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(equality_resolution,[],[f4683]) ).
fof(f5369,definition,
sF591 = preimage_subnetstr(sK209,sK210,sK211),
introduced(definition,[new_symbols(definition,[sF591])],[function_definition]) ).
fof(f5370,plain,
preimage_subnetstr(sK209,sK210,sK211) = sF591,
inference(reorient_equations,[],[f5369]) ).
fof(f5371,plain,
sK212 = sF591,
inference(definition_folding,[],[f3216,f5370]) ).
fof(f5560,plain,
sK212 = preimage_subnetstr(sK209,sK210,sK211),
inference(forward_demodulation,[],[f5370,f5371]) ).
fof(f5586,plain,
( rel_str(sK210)
| ~ one_sorted_str(sK209) ),
inference(resolution,[],[f4670,f3211]) ).
fof(f5587,plain,
rel_str(sK210),
inference(forward_subsumption_resolution,[],[f5586,f3209]) ).
fof(f5595,plain,
( ~ empty_carrier(sK212)
| empty_carrier(sK209)
| ~ one_sorted_str(sK209)
| empty_carrier(sK210)
| ~ transitive_relstr(sK210)
| ~ directed_relstr(sK210)
| ~ net_str(sK210,sK209) ),
inference(resolution,[],[f4365,f3215]) ).
fof(f5596,plain,
( ~ empty_carrier(sK212)
| ~ one_sorted_str(sK209)
| empty_carrier(sK210)
| ~ transitive_relstr(sK210)
| ~ directed_relstr(sK210)
| ~ net_str(sK210,sK209) ),
inference(forward_subsumption_resolution,[],[f5595,f3210]) ).
fof(f5597,plain,
( ~ empty_carrier(sK212)
| empty_carrier(sK210)
| ~ transitive_relstr(sK210)
| ~ directed_relstr(sK210)
| ~ net_str(sK210,sK209) ),
inference(forward_subsumption_resolution,[],[f5596,f3209]) ).
fof(f5598,plain,
( ~ empty_carrier(sK212)
| ~ transitive_relstr(sK210)
| ~ directed_relstr(sK210)
| ~ net_str(sK210,sK209) ),
inference(forward_subsumption_resolution,[],[f5597,f3214]) ).
fof(f5599,plain,
( ~ empty_carrier(sK212)
| ~ directed_relstr(sK210)
| ~ net_str(sK210,sK209) ),
inference(forward_subsumption_resolution,[],[f5598,f3213]) ).
fof(f5600,plain,
( ~ empty_carrier(sK212)
| ~ net_str(sK210,sK209) ),
inference(forward_subsumption_resolution,[],[f5599,f3212]) ).
fof(f5601,plain,
~ empty_carrier(sK212),
inference(forward_subsumption_resolution,[],[f5600,f3211]) ).
fof(f5610,plain,
( subnetstr(sK212,sK209,sK210)
| ~ one_sorted_str(sK209)
| ~ net_str(sK210,sK209) ),
inference(superposition,[],[f4671,f5560]) ).
fof(f5611,plain,
( subnetstr(sK212,sK209,sK210)
| ~ net_str(sK210,sK209) ),
inference(forward_subsumption_resolution,[],[f5610,f3209]) ).
fof(f5612,plain,
subnetstr(sK212,sK209,sK210),
inference(forward_subsumption_resolution,[],[f5611,f3211]) ).
fof(f5620,plain,
! [X2,X0,X1] :
( apply_netmap(X0,X1,X2) = apply(the_mapping(X0,X1),X2)
| ~ element(X2,the_carrier(X1))
| empty_carrier(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ function(the_mapping(X0,X1))
| ~ quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ element(X2,the_carrier(X1)) ),
inference(superposition,[],[f4682,f4205]) ).
fof(f5621,plain,
! [X2,X0,X1] :
( apply_netmap(X0,X1,X2) = apply(the_mapping(X0,X1),X2)
| ~ element(X2,the_carrier(X1))
| empty_carrier(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X1)
| ~ function(the_mapping(X0,X1))
| ~ quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0)) ),
inference(duplicate_literal_removal,[],[f5620]) ).
fof(f5623,plain,
! [X2,X0,X1] :
( apply_netmap(X0,X1,X2) = apply(the_mapping(X0,X1),X2)
| ~ element(X2,the_carrier(X1))
| empty_carrier(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X1)
| ~ quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0)) ),
inference(forward_subsumption_resolution,[],[f5621,f4554]) ).
fof(f5625,plain,
! [X2,X0,X1] :
( apply_netmap(X0,X1,X2) = apply(the_mapping(X0,X1),X2)
| ~ element(X2,the_carrier(X1))
| empty_carrier(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X1)
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0)) ),
inference(forward_subsumption_resolution,[],[f5623,f4553]) ).
fof(f5627,plain,
( net_str(sK212,sK209)
| empty_carrier(sK209)
| ~ one_sorted_str(sK209)
| empty_carrier(sK210)
| ~ transitive_relstr(sK210)
| ~ directed_relstr(sK210)
| ~ net_str(sK210,sK209) ),
inference(resolution,[],[f4362,f3215]) ).
fof(f5628,plain,
( net_str(sK212,sK209)
| ~ one_sorted_str(sK209)
| empty_carrier(sK210)
| ~ transitive_relstr(sK210)
| ~ directed_relstr(sK210)
| ~ net_str(sK210,sK209) ),
inference(forward_subsumption_resolution,[],[f5627,f3210]) ).
fof(f5629,plain,
( net_str(sK212,sK209)
| empty_carrier(sK210)
| ~ transitive_relstr(sK210)
| ~ directed_relstr(sK210)
| ~ net_str(sK210,sK209) ),
inference(forward_subsumption_resolution,[],[f5628,f3209]) ).
fof(f5630,plain,
( net_str(sK212,sK209)
| ~ transitive_relstr(sK210)
| ~ directed_relstr(sK210)
| ~ net_str(sK210,sK209) ),
inference(forward_subsumption_resolution,[],[f5629,f3214]) ).
fof(f5631,plain,
( net_str(sK212,sK209)
| ~ directed_relstr(sK210)
| ~ net_str(sK210,sK209) ),
inference(forward_subsumption_resolution,[],[f5630,f3213]) ).
fof(f5632,plain,
( net_str(sK212,sK209)
| ~ net_str(sK210,sK209) ),
inference(forward_subsumption_resolution,[],[f5631,f3212]) ).
fof(f5633,plain,
net_str(sK212,sK209),
inference(forward_subsumption_resolution,[],[f5632,f3211]) ).
fof(f5635,plain,
( rel_str(sK212)
| ~ one_sorted_str(sK209) ),
inference(resolution,[],[f5633,f4670]) ).
fof(f5636,plain,
rel_str(sK212),
inference(forward_subsumption_resolution,[],[f5635,f3209]) ).
fof(f5639,plain,
! [X2,X0,X1] :
( the_carrier(preimage_subnetstr(X0,X1,X2)) = relation_inverse_image(the_mapping(X0,X1),X2)
| ~ strict_net_str(preimage_subnetstr(X0,X1,X2),X0)
| ~ subnetstr(preimage_subnetstr(X0,X1,X2),X0,X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X1)
| ~ one_sorted_str(X0)
| ~ function(the_mapping(X0,X1))
| ~ quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0)) ),
inference(superposition,[],[f5361,f4571]) ).
fof(f5640,plain,
! [X2,X0,X1] :
( the_carrier(preimage_subnetstr(X0,X1,X2)) = relation_inverse_image(the_mapping(X0,X1),X2)
| ~ strict_net_str(preimage_subnetstr(X0,X1,X2),X0)
| ~ subnetstr(preimage_subnetstr(X0,X1,X2),X0,X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X1)
| ~ function(the_mapping(X0,X1))
| ~ quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0)) ),
inference(duplicate_literal_removal,[],[f5639]) ).
fof(f5642,plain,
! [X2,X0,X1] :
( the_carrier(preimage_subnetstr(X0,X1,X2)) = relation_inverse_image(the_mapping(X0,X1),X2)
| ~ subnetstr(preimage_subnetstr(X0,X1,X2),X0,X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X1)
| ~ function(the_mapping(X0,X1))
| ~ quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0)) ),
inference(forward_subsumption_resolution,[],[f5640,f4672]) ).
fof(f5644,plain,
! [X2,X0,X1] :
( the_carrier(preimage_subnetstr(X0,X1,X2)) = relation_inverse_image(the_mapping(X0,X1),X2)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X1)
| ~ function(the_mapping(X0,X1))
| ~ quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0)) ),
inference(forward_subsumption_resolution,[],[f5642,f4671]) ).
fof(f5646,plain,
! [X2,X0,X1] :
( the_carrier(preimage_subnetstr(X0,X1,X2)) = relation_inverse_image(the_mapping(X0,X1),X2)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X1)
| ~ quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0)) ),
inference(forward_subsumption_resolution,[],[f5644,f4554]) ).
fof(f5648,plain,
! [X2,X0,X1] :
( the_carrier(preimage_subnetstr(X0,X1,X2)) = relation_inverse_image(the_mapping(X0,X1),X2)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X1)
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0)) ),
inference(forward_subsumption_resolution,[],[f5646,f4553]) ).
fof(f5670,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,[],[f4552,f4549]) ).
fof(f5733,plain,
! [X2,X0,X1] :
( ~ relation_of2_as_subset(X0,X1,X2)
| relation(X0) ),
inference(resolution,[],[f4072,f4064]) ).
fof(f5735,plain,
! [X0,X1] :
( relation(the_mapping(X0,X1))
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(resolution,[],[f5733,f4552]) ).
fof(f5996,plain,
! [X2,X3,X0,X1] :
( in(sK544(X0,X1,X2,X3),the_carrier(X1))
| empty(the_carrier(X1))
| ~ element(X3,the_carrier(X1))
| is_eventually_in(X0,X1,X2)
| empty_carrier(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(resolution,[],[f4101,f4628]) ).
fof(f6971,plain,
! [X2,X0,X1] :
( element(the_carrier(preimage_subnetstr(X0,X1,X2)),powerset(the_carrier(X1)))
| ~ one_sorted_str(X1)
| ~ one_sorted_str(X0)
| ~ function(the_mapping(X0,X1))
| ~ quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ strict_net_str(preimage_subnetstr(X0,X1,X2),X0)
| ~ subnetstr(preimage_subnetstr(X0,X1,X2),X0,X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(superposition,[],[f4781,f5361]) ).
fof(f6975,plain,
! [X2,X0,X1] :
( element(the_carrier(preimage_subnetstr(X0,X1,X2)),powerset(the_carrier(X1)))
| ~ one_sorted_str(X1)
| ~ one_sorted_str(X0)
| ~ function(the_mapping(X0,X1))
| ~ quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ strict_net_str(preimage_subnetstr(X0,X1,X2),X0)
| ~ subnetstr(preimage_subnetstr(X0,X1,X2),X0,X1)
| ~ net_str(X1,X0) ),
inference(duplicate_literal_removal,[],[f6971]) ).
fof(f6977,plain,
! [X2,X0,X1] :
( element(the_carrier(preimage_subnetstr(X0,X1,X2)),powerset(the_carrier(X1)))
| ~ one_sorted_str(X1)
| ~ one_sorted_str(X0)
| ~ quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ strict_net_str(preimage_subnetstr(X0,X1,X2),X0)
| ~ subnetstr(preimage_subnetstr(X0,X1,X2),X0,X1)
| ~ net_str(X1,X0) ),
inference(forward_subsumption_resolution,[],[f6975,f4554]) ).
fof(f6982,plain,
! [X2,X0,X1] :
( element(the_carrier(preimage_subnetstr(X0,X1,X2)),powerset(the_carrier(X1)))
| ~ one_sorted_str(X1)
| ~ one_sorted_str(X0)
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ strict_net_str(preimage_subnetstr(X0,X1,X2),X0)
| ~ subnetstr(preimage_subnetstr(X0,X1,X2),X0,X1)
| ~ net_str(X1,X0) ),
inference(forward_subsumption_resolution,[],[f6977,f4553]) ).
fof(f6984,plain,
! [X2,X0,X1] :
( element(the_carrier(preimage_subnetstr(X0,X1,X2)),powerset(the_carrier(X1)))
| ~ one_sorted_str(X1)
| ~ one_sorted_str(X0)
| ~ strict_net_str(preimage_subnetstr(X0,X1,X2),X0)
| ~ subnetstr(preimage_subnetstr(X0,X1,X2),X0,X1)
| ~ net_str(X1,X0) ),
inference(forward_subsumption_resolution,[],[f6982,f5670]) ).
fof(f6985,plain,
! [X2,X0,X1] :
( element(the_carrier(preimage_subnetstr(X0,X1,X2)),powerset(the_carrier(X1)))
| ~ one_sorted_str(X1)
| ~ one_sorted_str(X0)
| ~ subnetstr(preimage_subnetstr(X0,X1,X2),X0,X1)
| ~ net_str(X1,X0) ),
inference(forward_subsumption_resolution,[],[f6984,f4672]) ).
fof(f6986,plain,
! [X2,X0,X1] :
( element(the_carrier(preimage_subnetstr(X0,X1,X2)),powerset(the_carrier(X1)))
| ~ one_sorted_str(X1)
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(forward_subsumption_resolution,[],[f6985,f4671]) ).
fof(f6987,plain,
! [X2,X3,X0,X1] :
( ~ in(X2,the_carrier(preimage_subnetstr(X1,X0,X3)))
| ~ one_sorted_str(X1)
| ~ net_str(X0,X1)
| ~ one_sorted_str(X0)
| element(X2,the_carrier(X0)) ),
inference(resolution,[],[f6986,f3978]) ).
fof(f6990,plain,
( element(the_carrier(sK212),powerset(the_carrier(sK210)))
| ~ one_sorted_str(sK210)
| ~ one_sorted_str(sK209)
| ~ net_str(sK210,sK209) ),
inference(superposition,[],[f6986,f5560]) ).
fof(f6992,plain,
( element(the_carrier(sK212),powerset(the_carrier(sK210)))
| ~ one_sorted_str(sK210)
| ~ net_str(sK210,sK209) ),
inference(forward_subsumption_resolution,[],[f6990,f3209]) ).
fof(f6994,plain,
( element(the_carrier(sK212),powerset(the_carrier(sK210)))
| ~ one_sorted_str(sK210) ),
inference(forward_subsumption_resolution,[],[f6992,f3211]) ).
fof(f6995,plain,
! [X0] :
( element(X0,the_carrier(sK210))
| ~ in(X0,the_carrier(sK212))
| ~ one_sorted_str(sK210) ),
inference(resolution,[],[f6994,f3978]) ).
fof(f7226,plain,
! [X2,X3,X0,X1] :
( in(apply_netmap(X0,X1,X2),X3)
| ~ in(X2,relation_inverse_image(the_mapping(X0,X1),X3))
| ~ relation(the_mapping(X0,X1))
| ~ function(the_mapping(X0,X1))
| ~ element(X2,the_carrier(X1))
| empty_carrier(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X1)
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0)) ),
inference(superposition,[],[f5311,f5625]) ).
fof(f7233,plain,
! [X2,X3,X0,X1] :
( in(apply_netmap(X0,X1,X2),X3)
| ~ in(X2,relation_inverse_image(the_mapping(X0,X1),X3))
| ~ function(the_mapping(X0,X1))
| ~ element(X2,the_carrier(X1))
| empty_carrier(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X1)
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0)) ),
inference(forward_subsumption_resolution,[],[f7226,f5735]) ).
fof(f7236,plain,
! [X2,X3,X0,X1] :
( in(apply_netmap(X0,X1,X2),X3)
| ~ in(X2,relation_inverse_image(the_mapping(X0,X1),X3))
| ~ element(X2,the_carrier(X1))
| empty_carrier(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X1)
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0)) ),
inference(forward_subsumption_resolution,[],[f7233,f4554]) ).
fof(f7237,plain,
! [X2,X3,X0,X1] :
( ~ in(X2,relation_inverse_image(the_mapping(X0,X1),X3))
| in(apply_netmap(X0,X1,X2),X3)
| ~ element(X2,the_carrier(X1))
| empty_carrier(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X1) ),
inference(forward_subsumption_resolution,[],[f7236,f5670]) ).
fof(f7247,plain,
! [X2,X3,X0,X1] :
( ~ in(X3,the_carrier(preimage_subnetstr(X0,X1,X2)))
| in(apply_netmap(X0,X1,X3),X2)
| ~ element(X3,the_carrier(X1))
| empty_carrier(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X1)
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0)) ),
inference(superposition,[],[f7237,f5648]) ).
fof(f7248,plain,
! [X2,X3,X0,X1] :
( ~ in(X3,the_carrier(preimage_subnetstr(X0,X1,X2)))
| in(apply_netmap(X0,X1,X3),X2)
| ~ element(X3,the_carrier(X1))
| empty_carrier(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X1)
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0)) ),
inference(duplicate_literal_removal,[],[f7247]) ).
fof(f7249,plain,
! [X2,X3,X0,X1] :
( ~ in(X3,the_carrier(preimage_subnetstr(X0,X1,X2)))
| in(apply_netmap(X0,X1,X3),X2)
| empty_carrier(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X1)
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0)) ),
inference(forward_subsumption_resolution,[],[f7248,f6987]) ).
fof(f7251,plain,
! [X2,X3,X0,X1] :
( ~ in(X3,the_carrier(preimage_subnetstr(X0,X1,X2)))
| in(apply_netmap(X0,X1,X3),X2)
| empty_carrier(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X1) ),
inference(forward_subsumption_resolution,[],[f7249,f5670]) ).
fof(f7267,plain,
! [X0] :
( ~ in(X0,the_carrier(sK212))
| in(apply_netmap(sK209,sK210,X0),sK211)
| empty_carrier(sK210)
| ~ net_str(sK210,sK209)
| empty_carrier(sK209)
| ~ one_sorted_str(sK209)
| ~ one_sorted_str(sK210) ),
inference(superposition,[],[f7251,f5560]) ).
fof(f7271,plain,
! [X0] :
( ~ in(X0,the_carrier(sK212))
| in(apply_netmap(sK209,sK210,X0),sK211)
| ~ net_str(sK210,sK209)
| empty_carrier(sK209)
| ~ one_sorted_str(sK209)
| ~ one_sorted_str(sK210) ),
inference(forward_subsumption_resolution,[],[f7267,f3214]) ).
fof(f7273,plain,
! [X0] :
( ~ in(X0,the_carrier(sK212))
| in(apply_netmap(sK209,sK210,X0),sK211)
| empty_carrier(sK209)
| ~ one_sorted_str(sK209)
| ~ one_sorted_str(sK210) ),
inference(forward_subsumption_resolution,[],[f7271,f3211]) ).
fof(f7275,plain,
! [X0] :
( ~ in(X0,the_carrier(sK212))
| in(apply_netmap(sK209,sK210,X0),sK211)
| ~ one_sorted_str(sK209)
| ~ one_sorted_str(sK210) ),
inference(forward_subsumption_resolution,[],[f7273,f3210]) ).
fof(f7277,plain,
! [X0] :
( in(apply_netmap(sK209,sK210,X0),sK211)
| ~ in(X0,the_carrier(sK212))
| ~ one_sorted_str(sK210) ),
inference(forward_subsumption_resolution,[],[f7275,f3209]) ).
fof(f8021,plain,
! [X2,X0,X1] :
( the_mapping(X1,X0) = relation_dom_restriction(the_mapping(X1,X2),the_carrier(X0))
| ~ subnetstr(X0,X1,X2)
| ~ net_str(X0,X1)
| ~ net_str(X2,X1)
| ~ one_sorted_str(X1)
| ~ relation_of2(the_mapping(X1,X2),the_carrier(X2),the_carrier(X1)) ),
inference(superposition,[],[f4679,f4073]) ).
fof(f8022,plain,
! [X2,X0,X1] :
( the_mapping(X1,X0) = relation_dom_restriction(the_mapping(X1,X2),the_carrier(X0))
| ~ subnetstr(X0,X1,X2)
| ~ net_str(X2,X1)
| ~ one_sorted_str(X1)
| ~ relation_of2(the_mapping(X1,X2),the_carrier(X2),the_carrier(X1)) ),
inference(forward_subsumption_resolution,[],[f8021,f4669]) ).
fof(f8024,plain,
! [X2,X0,X1] :
( the_mapping(X1,X0) = relation_dom_restriction(the_mapping(X1,X2),the_carrier(X0))
| ~ subnetstr(X0,X1,X2)
| ~ net_str(X2,X1)
| ~ one_sorted_str(X1) ),
inference(forward_subsumption_resolution,[],[f8022,f5670]) ).
fof(f8028,plain,
! [X2,X3,X0,X1] :
( apply(the_mapping(X2,X0),X3) = apply(the_mapping(X2,X1),X3)
| ~ in(X3,the_carrier(X1))
| ~ relation(the_mapping(X2,X0))
| ~ function(the_mapping(X2,X0))
| ~ subnetstr(X1,X2,X0)
| ~ net_str(X0,X2)
| ~ one_sorted_str(X2) ),
inference(superposition,[],[f3373,f8024]) ).
fof(f8029,plain,
! [X2,X3,X0,X1] :
( apply(the_mapping(X2,X0),X3) = apply(the_mapping(X2,X1),X3)
| ~ in(X3,the_carrier(X1))
| ~ function(the_mapping(X2,X0))
| ~ subnetstr(X1,X2,X0)
| ~ net_str(X0,X2)
| ~ one_sorted_str(X2) ),
inference(forward_subsumption_resolution,[],[f8028,f5735]) ).
fof(f8031,plain,
! [X2,X3,X0,X1] :
( apply(the_mapping(X2,X0),X3) = apply(the_mapping(X2,X1),X3)
| ~ in(X3,the_carrier(X1))
| ~ subnetstr(X1,X2,X0)
| ~ net_str(X0,X2)
| ~ one_sorted_str(X2) ),
inference(forward_subsumption_resolution,[],[f8029,f4554]) ).
fof(f8051,plain,
! [X2,X3,X0,X1] :
( apply(the_mapping(X0,X1),X2) = apply_netmap(X0,X3,X2)
| ~ element(X2,the_carrier(X3))
| empty_carrier(X3)
| ~ net_str(X3,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X3)
| ~ relation_of2(the_mapping(X0,X3),the_carrier(X3),the_carrier(X0))
| ~ in(X2,the_carrier(X3))
| ~ subnetstr(X3,X0,X1)
| ~ net_str(X1,X0)
| ~ one_sorted_str(X0) ),
inference(superposition,[],[f5625,f8031]) ).
fof(f8058,plain,
! [X2,X3,X0,X1] :
( apply(the_mapping(X0,X1),X2) = apply_netmap(X0,X3,X2)
| ~ element(X2,the_carrier(X3))
| empty_carrier(X3)
| ~ net_str(X3,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X3)
| ~ relation_of2(the_mapping(X0,X3),the_carrier(X3),the_carrier(X0))
| ~ in(X2,the_carrier(X3))
| ~ subnetstr(X3,X0,X1)
| ~ net_str(X1,X0) ),
inference(duplicate_literal_removal,[],[f8051]) ).
fof(f8070,plain,
! [X2,X3,X0,X1] :
( apply(the_mapping(X0,X1),X2) = apply_netmap(X0,X3,X2)
| empty_carrier(X3)
| ~ net_str(X3,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X3)
| ~ relation_of2(the_mapping(X0,X3),the_carrier(X3),the_carrier(X0))
| ~ in(X2,the_carrier(X3))
| ~ subnetstr(X3,X0,X1)
| ~ net_str(X1,X0) ),
inference(forward_subsumption_resolution,[],[f8058,f3415]) ).
fof(f8085,plain,
! [X2,X3,X0,X1] :
( apply(the_mapping(X0,X1),X2) = apply_netmap(X0,X3,X2)
| empty_carrier(X3)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X3)
| ~ relation_of2(the_mapping(X0,X3),the_carrier(X3),the_carrier(X0))
| ~ in(X2,the_carrier(X3))
| ~ subnetstr(X3,X0,X1)
| ~ net_str(X1,X0) ),
inference(forward_subsumption_resolution,[],[f8070,f4669]) ).
fof(f8364,plain,
! [X2,X3,X0,X1,X4] :
( ~ in(apply(the_mapping(X0,X1),sK544(X0,X2,X3,X4)),X3)
| ~ element(X4,the_carrier(X2))
| is_eventually_in(X0,X2,X3)
| empty_carrier(X2)
| ~ net_str(X2,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X2)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X2)
| ~ relation_of2(the_mapping(X0,X2),the_carrier(X2),the_carrier(X0))
| ~ in(sK544(X0,X2,X3,X4),the_carrier(X2))
| ~ subnetstr(X2,X0,X1)
| ~ net_str(X1,X0) ),
inference(superposition,[],[f4630,f8085]) ).
fof(f8393,plain,
! [X2,X3,X0,X1,X4] :
( ~ in(apply(the_mapping(X0,X1),sK544(X0,X2,X3,X4)),X3)
| ~ element(X4,the_carrier(X2))
| is_eventually_in(X0,X2,X3)
| empty_carrier(X2)
| ~ net_str(X2,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X2)
| ~ relation_of2(the_mapping(X0,X2),the_carrier(X2),the_carrier(X0))
| ~ in(sK544(X0,X2,X3,X4),the_carrier(X2))
| ~ subnetstr(X2,X0,X1)
| ~ net_str(X1,X0) ),
inference(duplicate_literal_removal,[],[f8364]) ).
fof(f8436,plain,
! [X2,X3,X0,X1,X4] :
( ~ in(apply(the_mapping(X0,X1),sK544(X0,X2,X3,X4)),X3)
| ~ element(X4,the_carrier(X2))
| is_eventually_in(X0,X2,X3)
| empty_carrier(X2)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X2)
| ~ relation_of2(the_mapping(X0,X2),the_carrier(X2),the_carrier(X0))
| ~ in(sK544(X0,X2,X3,X4),the_carrier(X2))
| ~ subnetstr(X2,X0,X1)
| ~ net_str(X1,X0) ),
inference(forward_subsumption_resolution,[],[f8393,f4669]) ).
fof(f8503,plain,
! [X2,X3,X0,X1,X4] :
( ~ in(apply_netmap(X0,X1,sK544(X0,X2,X3,X4)),X3)
| ~ element(X4,the_carrier(X2))
| is_eventually_in(X0,X2,X3)
| empty_carrier(X2)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X2)
| ~ relation_of2(the_mapping(X0,X2),the_carrier(X2),the_carrier(X0))
| ~ in(sK544(X0,X2,X3,X4),the_carrier(X2))
| ~ subnetstr(X2,X0,X1)
| ~ net_str(X1,X0)
| ~ element(sK544(X0,X2,X3,X4),the_carrier(X1))
| empty_carrier(X1)
| ~ net_str(X1,X0)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X1)
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0)) ),
inference(superposition,[],[f8436,f5625]) ).
fof(f8504,plain,
! [X2,X3,X0,X1,X4] :
( ~ in(apply_netmap(X0,X1,sK544(X0,X2,X3,X4)),X3)
| ~ element(X4,the_carrier(X2))
| is_eventually_in(X0,X2,X3)
| empty_carrier(X2)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X2)
| ~ relation_of2(the_mapping(X0,X2),the_carrier(X2),the_carrier(X0))
| ~ in(sK544(X0,X2,X3,X4),the_carrier(X2))
| ~ subnetstr(X2,X0,X1)
| ~ net_str(X1,X0)
| ~ element(sK544(X0,X2,X3,X4),the_carrier(X1))
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0)) ),
inference(duplicate_literal_removal,[],[f8503]) ).
fof(f8509,plain,
! [X2,X3,X0,X1,X4] :
( ~ in(apply_netmap(X0,X1,sK544(X0,X2,X3,X4)),X3)
| ~ element(X4,the_carrier(X2))
| is_eventually_in(X0,X2,X3)
| empty_carrier(X2)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X2)
| ~ relation_of2(the_mapping(X0,X2),the_carrier(X2),the_carrier(X0))
| ~ in(sK544(X0,X2,X3,X4),the_carrier(X2))
| ~ subnetstr(X2,X0,X1)
| ~ net_str(X1,X0)
| ~ element(sK544(X0,X2,X3,X4),the_carrier(X1))
| empty_carrier(X1)
| ~ one_sorted_str(X1) ),
inference(forward_subsumption_resolution,[],[f8504,f5670]) ).
fof(f8518,plain,
! [X0,X1] :
( ~ element(X0,the_carrier(X1))
| is_eventually_in(sK209,X1,sK211)
| empty_carrier(X1)
| empty_carrier(sK209)
| ~ one_sorted_str(sK209)
| ~ one_sorted_str(X1)
| ~ relation_of2(the_mapping(sK209,X1),the_carrier(X1),the_carrier(sK209))
| ~ in(sK544(sK209,X1,sK211,X0),the_carrier(X1))
| ~ subnetstr(X1,sK209,sK210)
| ~ net_str(sK210,sK209)
| ~ element(sK544(sK209,X1,sK211,X0),the_carrier(sK210))
| empty_carrier(sK210)
| ~ one_sorted_str(sK210)
| ~ in(sK544(sK209,X1,sK211,X0),the_carrier(sK212))
| ~ one_sorted_str(sK210) ),
inference(resolution,[],[f8509,f7277]) ).
fof(f8539,plain,
! [X0,X1] :
( ~ element(X0,the_carrier(X1))
| is_eventually_in(sK209,X1,sK211)
| empty_carrier(X1)
| empty_carrier(sK209)
| ~ one_sorted_str(sK209)
| ~ one_sorted_str(X1)
| ~ relation_of2(the_mapping(sK209,X1),the_carrier(X1),the_carrier(sK209))
| ~ in(sK544(sK209,X1,sK211,X0),the_carrier(X1))
| ~ subnetstr(X1,sK209,sK210)
| ~ net_str(sK210,sK209)
| ~ element(sK544(sK209,X1,sK211,X0),the_carrier(sK210))
| empty_carrier(sK210)
| ~ one_sorted_str(sK210)
| ~ in(sK544(sK209,X1,sK211,X0),the_carrier(sK212)) ),
inference(duplicate_literal_removal,[],[f8518]) ).
fof(f8545,plain,
! [X0,X1] :
( ~ element(X0,the_carrier(X1))
| is_eventually_in(sK209,X1,sK211)
| empty_carrier(X1)
| empty_carrier(sK209)
| ~ one_sorted_str(sK209)
| ~ one_sorted_str(X1)
| ~ relation_of2(the_mapping(sK209,X1),the_carrier(X1),the_carrier(sK209))
| ~ in(sK544(sK209,X1,sK211,X0),the_carrier(X1))
| ~ subnetstr(X1,sK209,sK210)
| ~ net_str(sK210,sK209)
| empty_carrier(sK210)
| ~ one_sorted_str(sK210)
| ~ in(sK544(sK209,X1,sK211,X0),the_carrier(sK212)) ),
inference(forward_subsumption_resolution,[],[f8539,f6995]) ).
fof(f8549,plain,
! [X0,X1] :
( ~ element(X0,the_carrier(X1))
| is_eventually_in(sK209,X1,sK211)
| empty_carrier(X1)
| ~ one_sorted_str(sK209)
| ~ one_sorted_str(X1)
| ~ relation_of2(the_mapping(sK209,X1),the_carrier(X1),the_carrier(sK209))
| ~ in(sK544(sK209,X1,sK211,X0),the_carrier(X1))
| ~ subnetstr(X1,sK209,sK210)
| ~ net_str(sK210,sK209)
| empty_carrier(sK210)
| ~ one_sorted_str(sK210)
| ~ in(sK544(sK209,X1,sK211,X0),the_carrier(sK212)) ),
inference(forward_subsumption_resolution,[],[f8545,f3210]) ).
fof(f8553,plain,
! [X0,X1] :
( ~ element(X0,the_carrier(X1))
| is_eventually_in(sK209,X1,sK211)
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ relation_of2(the_mapping(sK209,X1),the_carrier(X1),the_carrier(sK209))
| ~ in(sK544(sK209,X1,sK211,X0),the_carrier(X1))
| ~ subnetstr(X1,sK209,sK210)
| ~ net_str(sK210,sK209)
| empty_carrier(sK210)
| ~ one_sorted_str(sK210)
| ~ in(sK544(sK209,X1,sK211,X0),the_carrier(sK212)) ),
inference(forward_subsumption_resolution,[],[f8549,f3209]) ).
fof(f8557,plain,
! [X0,X1] :
( ~ element(X0,the_carrier(X1))
| is_eventually_in(sK209,X1,sK211)
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ relation_of2(the_mapping(sK209,X1),the_carrier(X1),the_carrier(sK209))
| ~ in(sK544(sK209,X1,sK211,X0),the_carrier(X1))
| ~ subnetstr(X1,sK209,sK210)
| empty_carrier(sK210)
| ~ one_sorted_str(sK210)
| ~ in(sK544(sK209,X1,sK211,X0),the_carrier(sK212)) ),
inference(forward_subsumption_resolution,[],[f8553,f3211]) ).
fof(f8560,plain,
! [X0,X1] :
( ~ relation_of2(the_mapping(sK209,X1),the_carrier(X1),the_carrier(sK209))
| is_eventually_in(sK209,X1,sK211)
| empty_carrier(X1)
| ~ one_sorted_str(X1)
| ~ element(X0,the_carrier(X1))
| ~ in(sK544(sK209,X1,sK211,X0),the_carrier(X1))
| ~ subnetstr(X1,sK209,sK210)
| ~ one_sorted_str(sK210)
| ~ in(sK544(sK209,X1,sK211,X0),the_carrier(sK212)) ),
inference(forward_subsumption_resolution,[],[f8557,f3214]) ).
fof(f8561,plain,
! [X0,X1] :
( is_eventually_in(sK209,X0,sK211)
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ in(sK544(sK209,X0,sK211,X1),the_carrier(X0))
| ~ subnetstr(X0,sK209,sK210)
| ~ one_sorted_str(sK210)
| ~ in(sK544(sK209,X0,sK211,X1),the_carrier(sK212))
| ~ net_str(X0,sK209)
| ~ one_sorted_str(sK209) ),
inference(resolution,[],[f8560,f5670]) ).
fof(f8564,plain,
! [X0,X1] :
( ~ in(sK544(sK209,X0,sK211,X1),the_carrier(sK212))
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| ~ element(X1,the_carrier(X0))
| ~ in(sK544(sK209,X0,sK211,X1),the_carrier(X0))
| ~ subnetstr(X0,sK209,sK210)
| ~ one_sorted_str(sK210)
| is_eventually_in(sK209,X0,sK211)
| ~ net_str(X0,sK209) ),
inference(forward_subsumption_resolution,[],[f8561,f3209]) ).
fof(f8567,plain,
! [X0] :
( ~ in(sK544(sK209,sK212,sK211,X0),the_carrier(sK212))
| empty_carrier(sK212)
| ~ one_sorted_str(sK212)
| ~ element(X0,the_carrier(sK212))
| ~ subnetstr(sK212,sK209,sK210)
| ~ one_sorted_str(sK210)
| is_eventually_in(sK209,sK212,sK211)
| ~ net_str(sK212,sK209) ),
inference(factoring,[],[f8564]) ).
fof(f8569,plain,
! [X0] :
( ~ in(sK544(sK209,sK212,sK211,X0),the_carrier(sK212))
| ~ one_sorted_str(sK212)
| ~ element(X0,the_carrier(sK212))
| ~ subnetstr(sK212,sK209,sK210)
| ~ one_sorted_str(sK210)
| is_eventually_in(sK209,sK212,sK211)
| ~ net_str(sK212,sK209) ),
inference(forward_subsumption_resolution,[],[f8567,f5601]) ).
fof(f8571,plain,
! [X0] :
( ~ in(sK544(sK209,sK212,sK211,X0),the_carrier(sK212))
| ~ one_sorted_str(sK212)
| ~ element(X0,the_carrier(sK212))
| ~ one_sorted_str(sK210)
| is_eventually_in(sK209,sK212,sK211)
| ~ net_str(sK212,sK209) ),
inference(forward_subsumption_resolution,[],[f8569,f5612]) ).
fof(f8573,plain,
! [X0] :
( ~ in(sK544(sK209,sK212,sK211,X0),the_carrier(sK212))
| ~ one_sorted_str(sK212)
| ~ element(X0,the_carrier(sK212))
| ~ one_sorted_str(sK210)
| ~ net_str(sK212,sK209) ),
inference(forward_subsumption_resolution,[],[f8571,f3217]) ).
fof(f8575,plain,
! [X0] :
( ~ in(sK544(sK209,sK212,sK211,X0),the_carrier(sK212))
| ~ one_sorted_str(sK212)
| ~ element(X0,the_carrier(sK212))
| ~ one_sorted_str(sK210) ),
inference(forward_subsumption_resolution,[],[f8573,f5633]) ).
fof(f8577,plain,
! [X0] :
( ~ one_sorted_str(sK212)
| ~ element(X0,the_carrier(sK212))
| ~ one_sorted_str(sK210)
| empty(the_carrier(sK212))
| ~ element(X0,the_carrier(sK212))
| is_eventually_in(sK209,sK212,sK211)
| empty_carrier(sK212)
| ~ net_str(sK212,sK209)
| empty_carrier(sK209)
| ~ one_sorted_str(sK209) ),
inference(resolution,[],[f8575,f5996]) ).
fof(f8578,plain,
! [X0] :
( ~ one_sorted_str(sK212)
| ~ element(X0,the_carrier(sK212))
| ~ one_sorted_str(sK210)
| empty(the_carrier(sK212))
| is_eventually_in(sK209,sK212,sK211)
| empty_carrier(sK212)
| ~ net_str(sK212,sK209)
| empty_carrier(sK209)
| ~ one_sorted_str(sK209) ),
inference(duplicate_literal_removal,[],[f8577]) ).
fof(f8579,plain,
! [X0] :
( ~ one_sorted_str(sK212)
| ~ element(X0,the_carrier(sK212))
| ~ one_sorted_str(sK210)
| is_eventually_in(sK209,sK212,sK211)
| empty_carrier(sK212)
| ~ net_str(sK212,sK209)
| empty_carrier(sK209)
| ~ one_sorted_str(sK209) ),
inference(forward_subsumption_resolution,[],[f8578,f3987]) ).
fof(f8580,plain,
! [X0] :
( ~ one_sorted_str(sK212)
| ~ element(X0,the_carrier(sK212))
| ~ one_sorted_str(sK210)
| empty_carrier(sK212)
| ~ net_str(sK212,sK209)
| empty_carrier(sK209)
| ~ one_sorted_str(sK209) ),
inference(forward_subsumption_resolution,[],[f8579,f3217]) ).
fof(f8581,plain,
! [X0] :
( ~ one_sorted_str(sK212)
| ~ element(X0,the_carrier(sK212))
| ~ one_sorted_str(sK210)
| ~ net_str(sK212,sK209)
| empty_carrier(sK209)
| ~ one_sorted_str(sK209) ),
inference(forward_subsumption_resolution,[],[f8580,f5601]) ).
fof(f8582,plain,
! [X0] :
( ~ one_sorted_str(sK212)
| ~ element(X0,the_carrier(sK212))
| ~ one_sorted_str(sK210)
| empty_carrier(sK209)
| ~ one_sorted_str(sK209) ),
inference(forward_subsumption_resolution,[],[f8581,f5633]) ).
fof(f8583,plain,
! [X0] :
( ~ one_sorted_str(sK212)
| ~ element(X0,the_carrier(sK212))
| ~ one_sorted_str(sK210)
| ~ one_sorted_str(sK209) ),
inference(forward_subsumption_resolution,[],[f8582,f3210]) ).
fof(f8584,plain,
! [X0] :
( ~ element(X0,the_carrier(sK212))
| ~ one_sorted_str(sK212)
| ~ one_sorted_str(sK210) ),
inference(forward_subsumption_resolution,[],[f8583,f3209]) ).
fof(f8589,plain,
( ~ one_sorted_str(sK212)
| ~ one_sorted_str(sK210)
| ~ rel_str(sK212) ),
inference(resolution,[],[f8584,f4975]) ).
fof(f8627,plain,
( ~ one_sorted_str(sK210)
| ~ rel_str(sK212) ),
inference(forward_subsumption_resolution,[],[f8589,f4207]) ).
fof(f8635,plain,
~ one_sorted_str(sK210),
inference(forward_subsumption_resolution,[],[f8627,f5636]) ).
fof(f8640,plain,
~ rel_str(sK210),
inference(resolution,[],[f8635,f4207]) ).
fof(f8641,plain,
$false,
inference(forward_subsumption_resolution,[],[f8640,f5587]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.01 % Problem : SEU379+2 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.03 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.04/0.31 % Computer : n012.cluster.edu
% 0.04/0.31 % Model : x86_64 x86_64
% 0.04/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.04/0.31 % Memory : 8046.5625MB
% 0.04/0.31 % OS : Linux 6.8.0-71-generic
% 0.04/0.31 % CPULimit : 300
% 0.04/0.31 % WCLimit : 300
% 0.04/0.31 % DateTime : Mon Sep 28 05:00:54 UTC 2026
% 0.04/0.31 % CPUTime :
% 0.04/0.31 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.08/0.33 Running first-order theorem proving
% 0.08/0.33 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
% 7.90/1.86 % (3027747)Detected formulas, will run a generic FOF schedule.
% 7.90/1.86 % (3027754)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=2452912519:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 7.90/1.86 % (3027753)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=2267649652:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 7.90/1.86 % (3027758)dis-21_1_sil=8000:lcm=predicate:random_seed=3056712917: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)
% 7.90/1.86 % (3027755)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1217219758:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 7.90/1.86 % (3027752)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=2610004974:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 7.90/1.86 % (3027757)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=3223357828:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 7.90/1.86 % (3027756)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=4262045105:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 7.90/1.86 % (3027755)Instruction limit reached!
% 7.90/1.86 % (3027755)------------------------------
% 7.90/1.86 % (3027755)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.90/1.86 % (3027755)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.90/1.86 % (3027755)CaDiCaL version: 2.1.3
% 7.90/1.86 % (3027755)Termination reason: Instruction limit
% 7.90/1.86 % (3027755)Termination phase: Blocked clause elimination
% 7.90/1.86 % (3027755)Time elapsed: 0.033 s
% 7.90/1.86 % (3027755)Peak memory usage: 90 MB
% 7.90/1.86 % (3027755)Instructions burned: 110 (million)
% 7.90/1.86 % (3027758)Instruction limit reached!
% 7.90/1.86 % (3027758)------------------------------
% 7.90/1.86 % (3027758)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.90/1.86 % (3027758)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.90/1.86 % (3027758)CaDiCaL version: 2.1.3
% 7.90/1.86 % (3027758)Termination reason: Instruction limit
% 7.90/1.86 % (3027758)Termination phase: Saturation
% 7.90/1.86 % (3027758)Time elapsed: 0.037 s
% 7.90/1.86 % (3027758)Peak memory usage: 92 MB
% 7.90/1.86 % (3027758)Instructions burned: 129 (million)
% 7.90/1.86 % (3027756)Instruction limit reached!
% 7.90/1.86 % (3027756)------------------------------
% 7.90/1.86 % (3027756)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.90/1.86 % (3027756)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.90/1.86 % (3027756)CaDiCaL version: 2.1.3
% 7.90/1.86 % (3027756)Termination reason: Instruction limit
% 7.90/1.86 % (3027756)Termination phase: Saturation
% 7.90/1.86 % (3027756)Time elapsed: 0.041 s
% 7.90/1.86 % (3027756)Peak memory usage: 91 MB
% 7.90/1.86 % (3027756)Instructions burned: 121 (million)
% 7.90/1.86 % (3027757)Instruction limit reached!
% 7.90/1.86 % (3027757)------------------------------
% 7.90/1.86 % (3027757)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.90/1.86 % (3027757)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.90/1.86 % (3027757)CaDiCaL version: 2.1.3
% 7.90/1.86 % (3027757)Termination reason: Instruction limit
% 7.90/1.86 % (3027757)Termination phase: Saturation
% 7.90/1.86 % (3027757)Time elapsed: 0.045 s
% 7.90/1.86 % (3027757)Peak memory usage: 92 MB
% 7.90/1.86 % (3027757)Instructions burned: 140 (million)
% 7.90/1.86 % (3027766)lrs+10_1_sil=8000:sp=occurrence:random_seed=2508525359:i=285:sd=3:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/285Mi)
% 7.90/1.86 % (3027767)lrs+10_1_sil=32000:urr=on:br=off:random_seed=3165648539:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2998 on theBenchmark for (2998ds/157Mi)
% 7.90/1.86 % (3027768)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1302196709:i=325:sd=1:ss=axioms:sgt=32_2998 on theBenchmark for (2998ds/325Mi)
% 7.90/1.86 % (3027769)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=3380359326:s2a=on:i=248:s2at=1.23:gtg=position_2998 on theBenchmark for (2998ds/248Mi)
% 7.90/1.86 % (3027767)Instruction limit reached!
% 12.80/2.46 % (3027767)------------------------------
% 12.80/2.46 % (3027767)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.46 % (3027767)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.46 % (3027767)CaDiCaL version: 2.1.3
% 12.80/2.46 % (3027767)Termination reason: Instruction limit
% 12.80/2.46 % (3027767)Termination phase: Saturation
% 12.80/2.46 % (3027767)Time elapsed: 0.047 s
% 12.80/2.46 % (3027767)Peak memory usage: 90 MB
% 12.80/2.46 % (3027767)Instructions burned: 159 (million)
% 12.80/2.46 % (3027766)Instruction limit reached!
% 12.80/2.46 % (3027766)------------------------------
% 12.80/2.46 % (3027766)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.46 % (3027766)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.46 % (3027766)CaDiCaL version: 2.1.3
% 12.80/2.46 % (3027766)Termination reason: Instruction limit
% 12.80/2.46 % (3027766)Termination phase: Saturation
% 12.80/2.46 % (3027766)Time elapsed: 0.097 s
% 12.80/2.46 % (3027766)Peak memory usage: 95 MB
% 12.80/2.46 % (3027766)Instructions burned: 287 (million)
% 12.80/2.46 % (3027769)Instruction limit reached!
% 12.80/2.46 % (3027769)------------------------------
% 12.80/2.46 % (3027769)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.46 % (3027769)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.46 % (3027769)CaDiCaL version: 2.1.3
% 12.80/2.46 % (3027769)Termination reason: Instruction limit
% 12.80/2.46 % (3027769)Termination phase: Saturation
% 12.80/2.46 % (3027769)Time elapsed: 0.081 s
% 12.80/2.46 % (3027769)Peak memory usage: 94 MB
% 12.80/2.46 % (3027769)Instructions burned: 251 (million)
% 12.80/2.46 % (3027768)Instruction limit reached!
% 12.80/2.46 % (3027768)------------------------------
% 12.80/2.46 % (3027768)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.46 % (3027768)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.46 % (3027768)CaDiCaL version: 2.1.3
% 12.80/2.46 % (3027768)Termination reason: Instruction limit
% 12.80/2.46 % (3027768)Termination phase: Saturation
% 12.80/2.46 % (3027768)Time elapsed: 0.118 s
% 12.80/2.46 % (3027768)Peak memory usage: 96 MB
% 12.80/2.46 % (3027768)Instructions burned: 326 (million)
% 12.80/2.46 % (3027774)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3811529968:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2996 on theBenchmark for (2996ds/294Mi)
% 12.80/2.46 % (3027775)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3335334712:i=2350_2996 on theBenchmark for (2996ds/2350Mi)
% 12.80/2.46 % (3027776)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2754055421:cts=off:i=113:fsr=off:ss=included:sgt=4_2996 on theBenchmark for (2996ds/113Mi)
% 12.80/2.46 % (3027777)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=3999984873:i=127:av=off:fsr=off:sup=off_2995 on theBenchmark for (2995ds/127Mi)
% 12.80/2.46 % (3027776)Instruction limit reached!
% 12.80/2.46 % (3027776)------------------------------
% 12.80/2.46 % (3027776)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.46 % (3027776)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.46 % (3027776)CaDiCaL version: 2.1.3
% 12.80/2.46 % (3027776)Termination reason: Instruction limit
% 12.80/2.46 % (3027776)Termination phase: Saturation
% 12.80/2.46 % (3027776)Time elapsed: 0.039 s
% 12.80/2.46 % (3027776)Peak memory usage: 92 MB
% 12.80/2.46 % (3027776)Instructions burned: 116 (million)
% 12.80/2.46 % (3027774)Instruction limit reached!
% 12.80/2.46 % (3027774)------------------------------
% 12.80/2.46 % (3027774)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.46 % (3027774)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.46 % (3027774)CaDiCaL version: 2.1.3
% 12.80/2.46 % (3027774)Termination reason: Instruction limit
% 12.80/2.46 % (3027774)Termination phase: Saturation
% 12.80/2.46 % (3027774)Time elapsed: 0.109 s
% 12.80/2.46 % (3027774)Peak memory usage: 94 MB
% 12.80/2.46 % (3027774)Instructions burned: 296 (million)
% 12.80/2.46 % (3027777)Instruction limit reached!
% 12.80/2.46 % (3027777)------------------------------
% 12.80/2.46 % (3027777)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.80/2.46 % (3027777)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.80/2.46 % (3027777)CaDiCaL version: 2.1.3
% 12.80/2.46 % (3027777)Termination reason: Instruction limit
% 32.33/5.16 % (3027777)Termination phase: Blocked clause elimination
% 32.33/5.16 % (3027777)Time elapsed: 0.043 s
% 32.33/5.16 % (3027777)Peak memory usage: 90 MB
% 32.33/5.16 % (3027777)Instructions burned: 129 (million)
% 32.33/5.16 % (3027783)lrs+10_1_sil=8000:sp=occurrence:random_seed=3092733728:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2994 on theBenchmark for (2994ds/907Mi)
% 32.33/5.16 % (3027782)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=670943621:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2994 on theBenchmark for (2994ds/114Mi)
% 32.33/5.16 % (3027784)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2427122896:i=437:sd=1:aac=none:ss=included_2994 on theBenchmark for (2994ds/437Mi)
% 32.33/5.16 % (3027782)Instruction limit reached!
% 32.33/5.16 % (3027782)------------------------------
% 32.33/5.16 % (3027782)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.33/5.16 % (3027782)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.33/5.16 % (3027782)CaDiCaL version: 2.1.3
% 32.33/5.16 % (3027782)Termination reason: Instruction limit
% 32.33/5.16 % (3027782)Termination phase: Saturation
% 32.33/5.16 % (3027782)Time elapsed: 0.038 s
% 32.33/5.16 % (3027782)Peak memory usage: 90 MB
% 32.33/5.16 % (3027782)Instructions burned: 115 (million)
% 32.33/5.16 % (3027784)Instruction limit reached!
% 32.33/5.16 % (3027784)------------------------------
% 32.33/5.16 % (3027784)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.33/5.16 % (3027784)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.33/5.16 % (3027784)CaDiCaL version: 2.1.3
% 32.33/5.16 % (3027784)Termination reason: Instruction limit
% 32.33/5.16 % (3027784)Termination phase: Saturation
% 32.33/5.16 % (3027784)Time elapsed: 0.146 s
% 32.33/5.16 % (3027784)Peak memory usage: 96 MB
% 32.33/5.16 % (3027784)Instructions burned: 439 (million)
% 32.33/5.16 % (3027788)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=1982597574:i=5202:ss=axioms:sgt=16_2992 on theBenchmark for (2992ds/5202Mi)
% 32.33/5.16 % (3027790)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=4248430860:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2991 on theBenchmark for (2991ds/134Mi)
% 32.33/5.16 % (3027783)Instruction limit reached!
% 32.33/5.16 % (3027783)------------------------------
% 32.33/5.16 % (3027783)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.33/5.16 % (3027783)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.33/5.16 % (3027783)CaDiCaL version: 2.1.3
% 32.33/5.16 % (3027783)Termination reason: Instruction limit
% 32.33/5.16 % (3027783)Termination phase: Saturation
% 32.33/5.16 % (3027783)Time elapsed: 0.323 s
% 32.33/5.16 % (3027783)Peak memory usage: 105 MB
% 32.33/5.16 % (3027783)Instructions burned: 909 (million)
% 32.33/5.16 % (3027790)Instruction limit reached!
% 32.33/5.16 % (3027790)------------------------------
% 32.33/5.16 % (3027790)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.33/5.16 % (3027790)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.33/5.16 % (3027790)CaDiCaL version: 2.1.3
% 32.33/5.16 % (3027790)Termination reason: Instruction limit
% 32.33/5.16 % (3027790)Termination phase: Saturation
% 32.33/5.16 % (3027790)Time elapsed: 0.037 s
% 32.33/5.16 % (3027790)Peak memory usage: 91 MB
% 32.33/5.16 % (3027790)Instructions burned: 136 (million)
% 32.33/5.16 % (3027792)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=849288719:st=8:i=592:sd=3:ep=RST:ss=axioms_2989 on theBenchmark for (2989ds/592Mi)
% 32.33/5.16 % (3027793)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2570637597:st=3:i=13193:sd=3:ss=axioms_2989 on theBenchmark for (2989ds/13193Mi)
% 32.33/5.16 % (3027775)Instruction limit reached!
% 32.33/5.16 % (3027775)------------------------------
% 32.33/5.16 % (3027775)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.33/5.16 % (3027775)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.33/5.16 % (3027775)CaDiCaL version: 2.1.3
% 32.33/5.16 % (3027775)Termination reason: Instruction limit
% 32.33/5.16 % (3027775)Termination phase: Saturation
% 32.33/5.16 % (3027775)Time elapsed: 0.786 s
% 32.33/5.16 % (3027775)Peak memory usage: 163 MB
% 32.33/5.16 % (3027775)Instructions burned: 2356 (million)
% 32.33/5.16 % (3027792)Instruction limit reached!
% 32.33/5.16 % (3027792)------------------------------
% 32.33/5.16 % (3027792)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.33/5.16 % (3027792)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.02/6.72 % (3027792)CaDiCaL version: 2.1.3
% 43.02/6.72 % (3027792)Termination reason: Instruction limit
% 43.02/6.72 % (3027792)Termination phase: Saturation
% 43.02/6.72 % (3027792)Time elapsed: 0.203 s
% 43.02/6.72 % (3027792)Peak memory usage: 102 MB
% 43.02/6.72 % (3027792)Instructions burned: 593 (million)
% 43.02/6.72 % (3027796)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=1433154439:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2987 on theBenchmark for (2987ds/125Mi)
% 43.02/6.72 % (3027796)Instruction limit reached!
% 43.02/6.72 % (3027796)------------------------------
% 43.02/6.72 % (3027796)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.02/6.72 % (3027796)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.02/6.72 % (3027796)CaDiCaL version: 2.1.3
% 43.02/6.72 % (3027796)Termination reason: Instruction limit
% 43.02/6.72 % (3027796)Termination phase: Saturation
% 43.02/6.72 % (3027796)Time elapsed: 0.042 s
% 43.02/6.72 % (3027796)Peak memory usage: 92 MB
% 43.02/6.72 % (3027796)Instructions burned: 125 (million)
% 43.02/6.72 % (3027797)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2547565322:i=134:gtgl=5:slsql=off:gtg=exists_sym_2986 on theBenchmark for (2986ds/134Mi)
% 43.02/6.72 % (3027797)Instruction limit reached!
% 43.02/6.72 % (3027797)------------------------------
% 43.02/6.72 % (3027797)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.02/6.72 % (3027797)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.02/6.72 % (3027797)CaDiCaL version: 2.1.3
% 43.02/6.72 % (3027797)Termination reason: Instruction limit
% 43.02/6.72 % (3027797)Termination phase: Saturation
% 43.02/6.72 % (3027797)Time elapsed: 0.039 s
% 43.02/6.72 % (3027797)Peak memory usage: 92 MB
% 43.02/6.72 % (3027797)Instructions burned: 135 (million)
% 43.02/6.72 % (3027800)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=510878783:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2985 on theBenchmark for (2985ds/141Mi)
% 43.02/6.72 % (3027800)Instruction limit reached!
% 43.02/6.72 % (3027800)------------------------------
% 43.02/6.72 % (3027800)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.02/6.72 % (3027800)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.02/6.72 % (3027800)CaDiCaL version: 2.1.3
% 43.02/6.72 % (3027800)Termination reason: Instruction limit
% 43.02/6.72 % (3027800)Termination phase: Saturation
% 43.02/6.72 % (3027800)Time elapsed: 0.040 s
% 43.02/6.72 % (3027800)Peak memory usage: 92 MB
% 43.02/6.72 % (3027800)Instructions burned: 141 (million)
% 43.02/6.72 % (3027801)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=248964792:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2985 on theBenchmark for (2985ds/431Mi)
% 43.02/6.72 % (3027804)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=2721969479:i=6060:aac=none:ins=25_2983 on theBenchmark for (2983ds/6060Mi)
% 43.02/6.72 % (3027801)Instruction limit reached!
% 43.02/6.72 % (3027801)------------------------------
% 43.02/6.72 % (3027801)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.02/6.72 % (3027801)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.02/6.72 % (3027801)CaDiCaL version: 2.1.3
% 43.02/6.72 % (3027801)Termination reason: Instruction limit
% 43.02/6.72 % (3027801)Termination phase: Saturation
% 43.02/6.72 % (3027801)Time elapsed: 0.136 s
% 43.02/6.72 % (3027801)Peak memory usage: 96 MB
% 43.02/6.72 % (3027801)Instructions burned: 432 (million)
% 43.02/6.72 % (3027806)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=1078372427:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2982 on theBenchmark for (2982ds/150Mi)
% 43.02/6.72 % (3027806)Instruction limit reached!
% 43.02/6.72 % (3027806)------------------------------
% 43.02/6.72 % (3027806)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 43.02/6.72 % (3027806)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 43.02/6.72 % (3027806)CaDiCaL version: 2.1.3
% 43.02/6.72 % (3027806)Termination reason: Instruction limit
% 43.02/6.72 % (3027806)Termination phase: Saturation
% 43.02/6.72 % (3027806)Time elapsed: 0.045 s
% 61.75/9.33 % (3027806)Peak memory usage: 93 MB
% 61.75/9.33 % (3027806)Instructions burned: 150 (million)
% 61.75/9.33 % (3027808)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=1561288899:i=14155:bd=all_2980 on theBenchmark for (2980ds/14155Mi)
% 61.75/9.33 % (3027788)Instruction limit reached!
% 61.75/9.33 % (3027788)------------------------------
% 61.75/9.33 % (3027788)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.75/9.33 % (3027788)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.75/9.33 % (3027788)CaDiCaL version: 2.1.3
% 61.75/9.33 % (3027788)Termination reason: Instruction limit
% 61.75/9.33 % (3027788)Termination phase: Saturation
% 61.75/9.33 % (3027788)Time elapsed: 1.734 s
% 61.75/9.33 % (3027788)Peak memory usage: 164 MB
% 61.75/9.33 % (3027788)Instructions burned: 5203 (million)
% 61.75/9.33 % (3027810)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=929563921:i=667:av=off:fsr=off_2974 on theBenchmark for (2974ds/667Mi)
% 61.75/9.33 % (3027810)Instruction limit reached!
% 61.75/9.33 % (3027810)------------------------------
% 61.75/9.33 % (3027810)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.75/9.33 % (3027810)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.75/9.33 % (3027810)CaDiCaL version: 2.1.3
% 61.75/9.33 % (3027810)Termination reason: Instruction limit
% 61.75/9.33 % (3027810)Termination phase: Saturation
% 61.75/9.33 % (3027810)Time elapsed: 0.172 s
% 61.75/9.33 % (3027810)Peak memory usage: 93 MB
% 61.75/9.33 % (3027810)Instructions burned: 668 (million)
% 61.75/9.33 % (3027812)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=1420408596:s2a=on:i=185:s2at=1.8:fdi=4_2971 on theBenchmark for (2971ds/185Mi)
% 61.75/9.33 % (3027812)Instruction limit reached!
% 61.75/9.33 % (3027812)------------------------------
% 61.75/9.33 % (3027812)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.75/9.33 % (3027812)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.75/9.33 % (3027812)CaDiCaL version: 2.1.3
% 61.75/9.33 % (3027812)Termination reason: Instruction limit
% 61.75/9.33 % (3027812)Termination phase: Saturation
% 61.75/9.33 % (3027812)Time elapsed: 0.053 s
% 61.75/9.33 % (3027812)Peak memory usage: 93 MB
% 61.75/9.33 % (3027812)Instructions burned: 188 (million)
% 61.75/9.33 % (3027814)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=4246926543:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2969 on theBenchmark for (2969ds/193Mi)
% 61.75/9.33 % (3027814)Instruction limit reached!
% 61.75/9.33 % (3027814)------------------------------
% 61.75/9.33 % (3027814)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.75/9.33 % (3027814)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.75/9.33 % (3027814)CaDiCaL version: 2.1.3
% 61.75/9.33 % (3027814)Termination reason: Instruction limit
% 61.75/9.33 % (3027814)Termination phase: Saturation
% 61.75/9.33 % (3027814)Time elapsed: 0.061 s
% 61.75/9.33 % (3027814)Peak memory usage: 95 MB
% 61.75/9.33 % (3027814)Instructions burned: 193 (million)
% 61.75/9.33 % (3027816)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=4223724321:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2967 on theBenchmark for (2967ds/4850Mi)
% 61.75/9.33 % (3027804)Instruction limit reached!
% 61.75/9.33 % (3027804)------------------------------
% 61.75/9.33 % (3027804)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.75/9.33 % (3027804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.75/9.33 % (3027804)CaDiCaL version: 2.1.3
% 61.75/9.33 % (3027804)Termination reason: Instruction limit
% 61.75/9.33 % (3027804)Termination phase: Saturation
% 61.75/9.33 % (3027804)Time elapsed: 1.937 s
% 61.75/9.33 % (3027804)Peak memory usage: 169 MB
% 61.75/9.33 % (3027804)Instructions burned: 6060 (million)
% 61.75/9.33 % (3027818)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=489359451:i=12111:sd=1:ss=included_2963 on theBenchmark for (2963ds/12111Mi)
% 61.75/9.33 % (3027793)Instruction limit reached!
% 61.75/9.33 % (3027793)------------------------------
% 61.75/9.33 % (3027793)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.75/9.33 % (3027793)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.41/11.91 % (3027793)CaDiCaL version: 2.1.3
% 79.41/11.91 % (3027793)Termination reason: Instruction limit
% 79.41/11.91 % (3027793)Termination phase: Saturation
% 79.41/11.91 % (3027793)Time elapsed: 3.499 s
% 79.41/11.91 % (3027793)Peak memory usage: 201 MB
% 79.41/11.91 % (3027793)Instructions burned: 13194 (million)
% 79.41/11.91 % (3027821)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=996459439:i=319:kws=precedence:fsr=off_2953 on theBenchmark for (2953ds/319Mi)
% 79.41/11.91 % (3027821)Instruction limit reached!
% 79.41/11.91 % (3027821)------------------------------
% 79.41/11.91 % (3027821)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.41/11.91 % (3027821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.41/11.91 % (3027821)CaDiCaL version: 2.1.3
% 79.41/11.91 % (3027821)Termination reason: Instruction limit
% 79.41/11.91 % (3027821)Termination phase: Saturation
% 79.41/11.91 % (3027821)Time elapsed: 0.092 s
% 79.41/11.91 % (3027821)Peak memory usage: 97 MB
% 79.41/11.91 % (3027821)Instructions burned: 324 (million)
% 79.41/11.91 % (3027816)Instruction limit reached!
% 79.41/11.91 % (3027816)------------------------------
% 79.41/11.91 % (3027816)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.41/11.91 % (3027816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.41/11.91 % (3027816)CaDiCaL version: 2.1.3
% 79.41/11.91 % (3027816)Termination reason: Instruction limit
% 79.41/11.91 % (3027816)Termination phase: Saturation
% 79.41/11.91 % (3027816)Time elapsed: 1.578 s
% 79.41/11.91 % (3027816)Peak memory usage: 144 MB
% 79.41/11.91 % (3027816)Instructions burned: 4851 (million)
% 79.41/11.91 % (3027823)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=1234298683:i=2064:ep=RST_2951 on theBenchmark for (2951ds/2064Mi)
% 79.41/11.91 % (3027824)dis-1011_128_sil=32000:random_seed=2666426875:i=3706:ep=RST:av=off_2950 on theBenchmark for (2950ds/3706Mi)
% 79.41/11.91 % (3027823)Instruction limit reached!
% 79.41/11.91 % (3027823)------------------------------
% 79.41/11.91 % (3027823)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.41/11.91 % (3027823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.41/11.91 % (3027823)CaDiCaL version: 2.1.3
% 79.41/11.91 % (3027823)Termination reason: Instruction limit
% 79.41/11.91 % (3027823)Termination phase: Saturation
% 79.41/11.91 % (3027823)Time elapsed: 0.647 s
% 79.41/11.91 % (3027823)Peak memory usage: 124 MB
% 79.41/11.91 % (3027823)Instructions burned: 2064 (million)
% 79.41/11.91 % (3027808)Instruction limit reached!
% 79.41/11.91 % (3027808)------------------------------
% 79.41/11.91 % (3027808)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.41/11.91 % (3027808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.41/11.91 % (3027808)CaDiCaL version: 2.1.3
% 79.41/11.91 % (3027808)Termination reason: Instruction limit
% 79.41/11.91 % (3027808)Termination phase: Saturation
% 79.41/11.91 % (3027808)Time elapsed: 3.729 s
% 79.41/11.91 % (3027808)Peak memory usage: 232 MB
% 79.41/11.91 % (3027808)Instructions burned: 14156 (million)
% 79.41/11.91 % (3027827)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=2911242184:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2943 on theBenchmark for (2943ds/757Mi)
% 79.41/11.91 % (3027829)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1559871375:i=13913:ss=axioms:sgt=8_2942 on theBenchmark for (2942ds/13913Mi)
% 79.41/11.91 % (3027827)Instruction limit reached!
% 79.41/11.91 % (3027827)------------------------------
% 79.41/11.91 % (3027827)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.41/11.91 % (3027827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.41/11.91 % (3027827)CaDiCaL version: 2.1.3
% 79.41/11.91 % (3027827)Termination reason: Instruction limit
% 79.41/11.91 % (3027827)Termination phase: Saturation
% 79.41/11.91 % (3027827)Time elapsed: 0.279 s
% 79.41/11.91 % (3027827)Peak memory usage: 109 MB
% 79.41/11.91 % (3027827)Instructions burned: 757 (million)
% 79.41/11.91 % (3027824)Instruction limit reached!
% 79.41/11.91 % (3027824)------------------------------
% 79.41/11.91 % (3027824)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 79.41/11.91 % (3027824)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 79.41/11.91 % (3027824)CaDiCaL version: 2.1.3
% 79.41/11.91 % (3027824)Termination reason: Instruction limit
% 79.41/11.91 % (3027824)Termination phase: Saturation
% 79.41/11.91 % (3027824)Time elapsed: 1.066 s
% 79.41/11.91 % (3027824)Peak memory usage: 122 MB
% 94.97/14.07 % (3027824)Instructions burned: 3709 (million)
% 94.97/14.07 % (3027831)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=1627670398:i=9925:aac=none_2939 on theBenchmark for (2939ds/9925Mi)
% 94.97/14.07 % (3027832)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3326453078:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2938 on theBenchmark for (2938ds/2479Mi)
% 94.97/14.07 % (3027818)Instruction limit reached!
% 94.97/14.07 % (3027818)------------------------------
% 94.97/14.07 % (3027818)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.97/14.07 % (3027818)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.97/14.07 % (3027818)CaDiCaL version: 2.1.3
% 94.97/14.07 % (3027818)Termination reason: Instruction limit
% 94.97/14.07 % (3027818)Termination phase: Saturation
% 94.97/14.07 % (3027818)Time elapsed: 3.182 s
% 94.97/14.07 % (3027818)Peak memory usage: 218 MB
% 94.97/14.07 % (3027818)Instructions burned: 12116 (million)
% 94.97/14.07 % (3027835)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=3440070663:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2929 on theBenchmark for (2929ds/440Mi)
% 94.97/14.07 % (3027832)Instruction limit reached!
% 94.97/14.07 % (3027832)------------------------------
% 94.97/14.07 % (3027832)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.97/14.07 % (3027832)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.97/14.07 % (3027832)CaDiCaL version: 2.1.3
% 94.97/14.07 % (3027832)Termination reason: Instruction limit
% 94.97/14.07 % (3027832)Termination phase: Saturation
% 94.97/14.07 % (3027832)Time elapsed: 0.862 s
% 94.97/14.07 % (3027832)Peak memory usage: 112 MB
% 94.97/14.07 % (3027832)Instructions burned: 2482 (million)
% 94.97/14.07 % (3027835)Instruction limit reached!
% 94.97/14.07 % (3027835)------------------------------
% 94.97/14.07 % (3027835)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.97/14.07 % (3027835)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.97/14.07 % (3027835)CaDiCaL version: 2.1.3
% 94.97/14.07 % (3027835)Termination reason: Instruction limit
% 94.97/14.07 % (3027835)Termination phase: Saturation
% 94.97/14.07 % (3027835)Time elapsed: 0.136 s
% 94.97/14.07 % (3027835)Peak memory usage: 97 MB
% 94.97/14.07 % (3027835)Instructions burned: 443 (million)
% 94.97/14.07 % (3027837)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3355038507:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2928 on theBenchmark for (2928ds/11145Mi)
% 94.97/14.07 % (3027838)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=1515858738:cts=off:i=3034:av=off:er=known:fsd=on_2927 on theBenchmark for (2927ds/3034Mi)
% 94.97/14.07 % (3027838)Instruction limit reached!
% 94.97/14.07 % (3027838)------------------------------
% 94.97/14.07 % (3027838)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.97/14.07 % (3027838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.97/14.07 % (3027838)CaDiCaL version: 2.1.3
% 94.97/14.07 % (3027838)Termination reason: Instruction limit
% 94.97/14.07 % (3027838)Termination phase: Saturation
% 94.97/14.07 % (3027838)Time elapsed: 1.010 s
% 94.97/14.07 % (3027838)Peak memory usage: 156 MB
% 94.97/14.07 % (3027838)Instructions burned: 3036 (million)
% 94.97/14.07 % (3027841)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=3747239773:st=2:s2a=on:i=524:s2at=2:ss=axioms_2915 on theBenchmark for (2915ds/524Mi)
% 94.97/14.07 % (3027841)Instruction limit reached!
% 94.97/14.07 % (3027841)------------------------------
% 94.97/14.07 % (3027841)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.97/14.07 % (3027841)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 94.97/14.07 % (3027841)CaDiCaL version: 2.1.3
% 94.97/14.07 % (3027841)Termination reason: Instruction limit
% 94.97/14.07 % (3027841)Termination phase: Saturation
% 94.97/14.07 % (3027841)Time elapsed: 0.162 s
% 94.97/14.07 % (3027841)Peak memory usage: 97 MB
% 94.97/14.07 % (3027841)Instructions burned: 526 (million)
% 94.97/14.07 % (3027831)Instruction limit reached!
% 94.97/14.07 % (3027831)------------------------------
% 94.97/14.07 % (3027831)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 94.97/14.07 % (3027831)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.94/17.78 % (3027831)CaDiCaL version: 2.1.3
% 120.94/17.78 % (3027831)Termination reason: Instruction limit
% 120.94/17.78 % (3027831)Termination phase: Saturation
% 120.94/17.78 % (3027831)Time elapsed: 2.592 s
% 120.94/17.78 % (3027831)Peak memory usage: 191 MB
% 120.94/17.78 % (3027831)Instructions burned: 9926 (million)
% 120.94/17.78 % (3027843)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=2873939882:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2912 on theBenchmark for (2912ds/1016Mi)
% 120.94/17.78 % (3027844)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=837175073:i=14123:bd=preordered:ins=4_2911 on theBenchmark for (2911ds/14123Mi)
% 120.94/17.78 % (3027843)Instruction limit reached!
% 120.94/17.78 % (3027843)------------------------------
% 120.94/17.78 % (3027843)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.94/17.78 % (3027843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.94/17.78 % (3027843)CaDiCaL version: 2.1.3
% 120.94/17.78 % (3027843)Termination reason: Instruction limit
% 120.94/17.78 % (3027843)Termination phase: Saturation
% 120.94/17.78 % (3027843)Time elapsed: 0.349 s
% 120.94/17.78 % (3027843)Peak memory usage: 121 MB
% 120.94/17.78 % (3027843)Instructions burned: 1016 (million)
% 120.94/17.78 % (3027847)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2019359338:i=5781:kws=precedence:bd=all:rawr=on_2908 on theBenchmark for (2908ds/5781Mi)
% 120.94/17.78 % (3027829)Instruction limit reached!
% 120.94/17.78 % (3027829)------------------------------
% 120.94/17.78 % (3027829)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.94/17.78 % (3027829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.94/17.78 % (3027829)CaDiCaL version: 2.1.3
% 120.94/17.78 % (3027829)Termination reason: Instruction limit
% 120.94/17.78 % (3027829)Termination phase: Saturation
% 120.94/17.78 % (3027829)Time elapsed: 4.033 s
% 120.94/17.78 % (3027829)Peak memory usage: 212 MB
% 120.94/17.78 % (3027829)Instructions burned: 13914 (million)
% 120.94/17.78 % (3027849)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=839879161:i=2448:gtgl=5:bd=preordered:gtg=all_2900 on theBenchmark for (2900ds/2448Mi)
% 120.94/17.78 % (3027849)Instruction limit reached!
% 120.94/17.78 % (3027849)------------------------------
% 120.94/17.78 % (3027849)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.94/17.78 % (3027849)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.94/17.78 % (3027849)CaDiCaL version: 2.1.3
% 120.94/17.78 % (3027849)Termination reason: Instruction limit
% 120.94/17.78 % (3027849)Termination phase: Saturation
% 120.94/17.78 % (3027849)Time elapsed: 0.820 s
% 120.94/17.78 % (3027849)Peak memory usage: 169 MB
% 120.94/17.78 % (3027849)Instructions burned: 2448 (million)
% 120.94/17.78 % (3027851)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=1489921834:i=3223:kws=precedence:fgj=on:av=off_2890 on theBenchmark for (2890ds/3223Mi)
% 120.94/17.78 % (3027837)Instruction limit reached!
% 120.94/17.78 % (3027837)------------------------------
% 120.94/17.78 % (3027837)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.94/17.78 % (3027837)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.94/17.78 % (3027837)CaDiCaL version: 2.1.3
% 120.94/17.78 % (3027837)Termination reason: Instruction limit
% 120.94/17.78 % (3027837)Termination phase: Saturation
% 120.94/17.78 % (3027837)Time elapsed: 3.859 s
% 120.94/17.78 % (3027837)Peak memory usage: 213 MB
% 120.94/17.78 % (3027837)Instructions burned: 11147 (million)
% 120.94/17.78 % (3027847)Instruction limit reached!
% 120.94/17.78 % (3027847)------------------------------
% 120.94/17.78 % (3027847)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 120.94/17.78 % (3027847)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 120.94/17.78 % (3027847)CaDiCaL version: 2.1.3
% 120.94/17.78 % (3027847)Termination reason: Instruction limit
% 120.94/17.78 % (3027847)Termination phase: Saturation
% 120.94/17.78 % (3027847)Time elapsed: 1.897 s
% 120.94/17.78 % (3027847)Peak memory usage: 143 MB
% 120.94/17.78 % (3027847)Instructions burned: 5781 (million)
% 120.94/17.78 % (3027853)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3696408645:st=5.6:i=2033:sd=3:ss=axioms_2888 on theBenchmark for (2888ds/2033Mi)
% 120.94/17.78 % (3027854)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=2325534264:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2887 on theBenchmark for (2887ds/2055Mi)
% 142.79/20.83 % (3027853)Instruction limit reached!
% 142.79/20.83 % (3027853)------------------------------
% 142.79/20.83 % (3027853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.79/20.83 % (3027853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.79/20.83 % (3027853)CaDiCaL version: 2.1.3
% 142.79/20.83 % (3027853)Termination reason: Instruction limit
% 142.79/20.83 % (3027853)Termination phase: Saturation
% 142.79/20.83 % (3027853)Time elapsed: 0.690 s
% 142.79/20.83 % (3027853)Peak memory usage: 146 MB
% 142.79/20.83 % (3027853)Instructions burned: 2034 (million)
% 142.79/20.83 % (3027854)Instruction limit reached!
% 142.79/20.83 % (3027854)------------------------------
% 142.79/20.83 % (3027854)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.79/20.83 % (3027854)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.79/20.83 % (3027854)CaDiCaL version: 2.1.3
% 142.79/20.83 % (3027854)Termination reason: Instruction limit
% 142.79/20.83 % (3027854)Termination phase: Saturation
% 142.79/20.83 % (3027854)Time elapsed: 0.723 s
% 142.79/20.83 % (3027854)Peak memory usage: 140 MB
% 142.79/20.83 % (3027854)Instructions burned: 2057 (million)
% 142.79/20.83 % (3027857)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=790668862:i=21611:sd=3:ss=axioms_2879 on theBenchmark for (2879ds/21611Mi)
% 142.79/20.83 % (3027851)Instruction limit reached!
% 142.79/20.83 % (3027851)------------------------------
% 142.79/20.83 % (3027851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.79/20.83 % (3027851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.79/20.83 % (3027851)CaDiCaL version: 2.1.3
% 142.79/20.83 % (3027851)Termination reason: Instruction limit
% 142.79/20.83 % (3027851)Termination phase: Saturation
% 142.79/20.83 % (3027851)Time elapsed: 1.141 s
% 142.79/20.83 % (3027851)Peak memory usage: 154 MB
% 142.79/20.83 % (3027851)Instructions burned: 3224 (million)
% 142.79/20.83 % (3027858)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=772491443:i=4835:sd=13:ss=axioms:sgt=23_2878 on theBenchmark for (2878ds/4835Mi)
% 142.79/20.83 % (3027861)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=3765117743:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2877 on theBenchmark for (2877ds/797Mi)
% 142.79/20.83 % (3027844)Instruction limit reached!
% 142.79/20.83 % (3027844)------------------------------
% 142.79/20.83 % (3027844)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.79/20.83 % (3027844)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.79/20.83 % (3027844)CaDiCaL version: 2.1.3
% 142.79/20.83 % (3027844)Termination reason: Instruction limit
% 142.79/20.83 % (3027844)Termination phase: Saturation
% 142.79/20.83 % (3027844)Time elapsed: 3.643 s
% 142.79/20.83 % (3027844)Peak memory usage: 218 MB
% 142.79/20.83 % (3027844)Instructions burned: 14126 (million)
% 142.79/20.83 % (3027861)Instruction limit reached!
% 142.79/20.83 % (3027861)------------------------------
% 142.79/20.83 % (3027861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.79/20.83 % (3027861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.79/20.83 % (3027861)CaDiCaL version: 2.1.3
% 142.79/20.83 % (3027861)Termination reason: Instruction limit
% 142.79/20.83 % (3027861)Termination phase: Saturation
% 142.79/20.83 % (3027861)Time elapsed: 0.241 s
% 142.79/20.83 % (3027861)Peak memory usage: 98 MB
% 142.79/20.83 % (3027861)Instructions burned: 799 (million)
% 142.79/20.83 % (3027863)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3952172997:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2873 on theBenchmark for (2873ds/2326Mi)
% 142.79/20.83 % (3027864)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=3043581291:i=6038:nm=6_2873 on theBenchmark for (2873ds/6038Mi)
% 142.79/20.83 % (3027863)Instruction limit reached!
% 142.79/20.83 % (3027863)------------------------------
% 142.79/20.83 % (3027863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 142.79/20.83 % (3027863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 142.79/20.83 % (3027863)CaDiCaL version: 2.1.3
% 142.79/20.83 % (3027863)Termination reason: Instruction limit
% 182.98/26.59 % (3027863)Termination phase: Saturation
% 182.98/26.59 % (3027863)Time elapsed: 0.804 s
% 182.98/26.59 % (3027863)Peak memory usage: 115 MB
% 182.98/26.59 % (3027863)Instructions burned: 2326 (million)
% 182.98/26.59 % (3027867)lrs+10_1_sil=32000:sp=occurrence:random_seed=776022213:st=2:i=33334:sd=3:ss=included:sgt=32_2864 on theBenchmark for (2864ds/33334Mi)
% 182.98/26.59 % (3027858)Instruction limit reached!
% 182.98/26.59 % (3027858)------------------------------
% 182.98/26.59 % (3027858)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 182.98/26.59 % (3027858)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.98/26.59 % (3027858)CaDiCaL version: 2.1.3
% 182.98/26.59 % (3027858)Termination reason: Instruction limit
% 182.98/26.59 % (3027858)Termination phase: Saturation
% 182.98/26.59 % (3027858)Time elapsed: 1.624 s
% 182.98/26.59 % (3027858)Peak memory usage: 146 MB
% 182.98/26.59 % (3027858)Instructions burned: 4835 (million)
% 182.98/26.59 % (3027869)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=2748390516:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2861 on theBenchmark for (2861ds/1008Mi)
% 182.98/26.59 % (3027869)Instruction limit reached!
% 182.98/26.59 % (3027869)------------------------------
% 182.98/26.59 % (3027869)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 182.98/26.59 % (3027869)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.98/26.59 % (3027869)CaDiCaL version: 2.1.3
% 182.98/26.59 % (3027869)Termination reason: Instruction limit
% 182.98/26.59 % (3027869)Termination phase: Saturation
% 182.98/26.59 % (3027869)Time elapsed: 0.319 s
% 182.98/26.59 % (3027869)Peak memory usage: 99 MB
% 182.98/26.59 % (3027869)Instructions burned: 1012 (million)
% 182.98/26.59 % (3027871)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:sp=const_frequency:spb=intro:gs=on:random_seed=1497970012:i=8327:s2at=5:bd=preordered_2856 on theBenchmark for (2856ds/8327Mi)
% 182.98/26.59 % (3027864)Instruction limit reached!
% 182.98/26.59 % (3027864)------------------------------
% 182.98/26.59 % (3027864)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 182.98/26.59 % (3027864)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.98/26.59 % (3027864)CaDiCaL version: 2.1.3
% 182.98/26.59 % (3027864)Termination reason: Instruction limit
% 182.98/26.59 % (3027864)Termination phase: Saturation
% 182.98/26.59 % (3027864)Time elapsed: 1.731 s
% 182.98/26.59 % (3027864)Peak memory usage: 178 MB
% 182.98/26.59 % (3027864)Instructions burned: 6040 (million)
% 182.98/26.59 % (3027873)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=1547264423:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2855 on theBenchmark for (2855ds/1083Mi)
% 182.98/26.59 % (3027873)Instruction limit reached!
% 182.98/26.59 % (3027873)------------------------------
% 182.98/26.59 % (3027873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 182.98/26.59 % (3027873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.98/26.59 % (3027873)CaDiCaL version: 2.1.3
% 182.98/26.59 % (3027873)Termination reason: Instruction limit
% 182.98/26.59 % (3027873)Termination phase: Saturation
% 182.98/26.59 % (3027873)Time elapsed: 0.262 s
% 182.98/26.59 % (3027873)Peak memory usage: 101 MB
% 182.98/26.59 % (3027873)Instructions burned: 1085 (million)
% 182.98/26.59 % (3027875)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=866687021:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2851 on theBenchmark for (2851ds/1084Mi)
% 182.98/26.59 % (3027875)Instruction limit reached!
% 182.98/26.59 % (3027875)------------------------------
% 182.98/26.59 % (3027875)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 182.98/26.59 % (3027875)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 182.98/26.59 % (3027875)CaDiCaL version: 2.1.3
% 182.98/26.59 % (3027875)Termination reason: Instruction limit
% 182.98/26.59 % (3027875)Termination phase: Saturation
% 182.98/26.59 % (3027875)Time elapsed: 0.371 s
% 182.98/26.59 % (3027875)Peak memory usage: 107 MB
% 182.98/26.59 % (3027875)Instructions burned: 1085 (million)
% 182.98/26.59 % (3027877)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=3280156103:i=6995:s2at=5:gtg=all_2846 on theBenchmark for (2846ds/6995Mi)
% 182.98/26.59 % (3027871)Instruction limit reached!
% 182.98/26.59 % (3027871)------------------------------
% 194.92/28.24 % (3027871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 194.92/28.24 % (3027871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 194.92/28.24 % (3027871)CaDiCaL version: 2.1.3
% 194.92/28.24 % (3027871)Termination reason: Instruction limit
% 194.92/28.24 % (3027871)Termination phase: Saturation
% 194.92/28.24 % (3027871)Time elapsed: 2.801 s
% 194.92/28.24 % (3027871)Peak memory usage: 199 MB
% 194.92/28.24 % (3027871)Instructions burned: 8329 (million)
% 194.92/28.24 % (3027877)Instruction limit reached!
% 194.92/28.24 % (3027877)------------------------------
% 194.92/28.24 % (3027877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 194.92/28.24 % (3027877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 194.92/28.24 % (3027877)CaDiCaL version: 2.1.3
% 194.92/28.24 % (3027877)Termination reason: Instruction limit
% 194.92/28.24 % (3027877)Termination phase: Saturation
% 194.92/28.24 % (3027877)Time elapsed: 1.844 s
% 194.92/28.24 % (3027877)Peak memory usage: 176 MB
% 194.92/28.24 % (3027877)Instructions burned: 6997 (million)
% 194.92/28.24 % (3027879)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=1557532267:st=2:i=6225:sd=15:ss=axioms_2827 on theBenchmark for (2827ds/6225Mi)
% 194.92/28.24 % (3027880)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=1407278221:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2826 on theBenchmark for (2826ds/3372Mi)
% 194.92/28.24 % (3027857)Instruction limit reached!
% 194.92/28.24 % (3027857)------------------------------
% 194.92/28.24 % (3027857)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 194.92/28.24 % (3027857)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 194.92/28.24 % (3027857)CaDiCaL version: 2.1.3
% 194.92/28.24 % (3027857)Termination reason: Instruction limit
% 194.92/28.24 % (3027857)Termination phase: Saturation
% 194.92/28.24 % (3027857)Time elapsed: 5.718 s
% 194.92/28.24 % (3027857)Peak memory usage: 209 MB
% 194.92/28.24 % (3027857)Instructions burned: 21614 (million)
% 194.92/28.24 % (3027880)Refutation not found, incomplete strategy
% 194.92/28.24 % (3027880)------------------------------
% 194.92/28.24 % (3027880)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 194.92/28.24 % (3027880)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 194.92/28.24 % (3027880)CaDiCaL version: 2.1.3
% 194.92/28.24 % (3027880)Termination reason: Refutation not found, incomplete strategy
% 194.92/28.24 % (3027880)Time elapsed: 0.342 s
% 194.92/28.24 % (3027880)Peak memory usage: 129 MB
% 194.92/28.24 % (3027880)Instructions burned: 932 (million)
% 194.92/28.24 % (3027883)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=962632553:st=2.3:i=26457:sd=10:ss=included:sgt=8_2821 on theBenchmark for (2821ds/26457Mi)
% 194.92/28.24 % (3027880)------------------------------
% 194.92/28.24 % (3027880)------------------------------
% 194.92/28.24 % (3027885)lrs+10_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:foolp=on:s2agt=20:sac=on:random_seed=2502138706:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2819 on theBenchmark for (2819ds/13494Mi)
% 194.92/28.24 % (3027879)Instruction limit reached!
% 194.92/28.24 % (3027879)------------------------------
% 194.92/28.24 % (3027879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 194.92/28.24 % (3027879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 194.92/28.24 % (3027879)CaDiCaL version: 2.1.3
% 194.92/28.24 % (3027879)Termination reason: Instruction limit
% 194.92/28.24 % (3027879)Termination phase: Saturation
% 194.92/28.24 % (3027879)Time elapsed: 1.896 s
% 194.92/28.24 % (3027879)Peak memory usage: 191 MB
% 194.92/28.24 % (3027879)Instructions burned: 6227 (million)
% 194.92/28.24 % (3027887)dis-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:fde=unused:sp=const_min:spb=goal_then_units:lcm=predicate:acc=on:flr=on:random_seed=2239677978:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2806 on theBenchmark for (2806ds/2503Mi)
% 194.92/28.24 % (3027887)Instruction limit reached!
% 194.92/28.24 % (3027887)------------------------------
% 194.92/28.24 % (3027887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 194.92/28.24 % (3027887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 194.92/28.24 % (3027887)CaDiCaL version: 2.1.3
% 194.92/28.24 % (3027887)Termination reason: Instruction limit
% 194.92/28.24 % (3027887)Termination phase: Saturation
% 194.92/28.24 % (3027887)Time elapsed: 0.851 s
% 214.79/31.07 % (3027887)Peak memory usage: 154 MB
% 214.79/31.07 % (3027887)Instructions burned: 2504 (million)
% 214.79/31.07 % (3027889)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=1478759635:i=2559:sd=1:ep=RSTC:ss=axioms_2796 on theBenchmark for (2796ds/2559Mi)
% 214.79/31.07 % (3027889)Instruction limit reached!
% 214.79/31.07 % (3027889)------------------------------
% 214.79/31.07 % (3027889)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 214.79/31.07 % (3027889)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.79/31.07 % (3027889)CaDiCaL version: 2.1.3
% 214.79/31.07 % (3027889)Termination reason: Instruction limit
% 214.79/31.07 % (3027889)Termination phase: Saturation
% 214.79/31.07 % (3027889)Time elapsed: 0.821 s
% 214.79/31.07 % (3027889)Peak memory usage: 150 MB
% 214.79/31.07 % (3027889)Instructions burned: 2561 (million)
% 214.79/31.07 % (3027891)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=4280439387:i=30753:av=off:ss=included_2787 on theBenchmark for (2787ds/30753Mi)
% 214.79/31.07 % (3027885)Instruction limit reached!
% 214.79/31.07 % (3027885)------------------------------
% 214.79/31.07 % (3027885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 214.79/31.07 % (3027885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.79/31.07 % (3027885)CaDiCaL version: 2.1.3
% 214.79/31.07 % (3027885)Termination reason: Instruction limit
% 214.79/31.07 % (3027885)Termination phase: Saturation
% 214.79/31.07 % (3027885)Time elapsed: 4.313 s
% 214.79/31.07 % (3027885)Peak memory usage: 258 MB
% 214.79/31.07 % (3027885)Instructions burned: 13495 (million)
% 214.79/31.07 % (3027893)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=2767411910:i=26473:ep=RSTC_2775 on theBenchmark for (2775ds/26473Mi)
% 214.79/31.07 % (3027752)Instruction limit reached!
% 214.79/31.07 % (3027752)------------------------------
% 214.79/31.07 % (3027752)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 214.79/31.07 % (3027752)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.79/31.07 % (3027752)CaDiCaL version: 2.1.3
% 214.79/31.07 % (3027752)Termination reason: Instruction limit
% 214.79/31.07 % (3027752)Termination phase: Saturation
% 214.79/31.07 % (3027752)Time elapsed: 23.641 s
% 214.79/31.07 % (3027752)Peak memory usage: 214 MB
% 214.79/31.07 % (3027752)Instructions burned: 141196 (million)
% 214.79/31.07 % (3027895)dis-1011_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:tgt=ground:npcc=on:sp=arity:sos=on:erd=off:rp=on:gs=on:kmz=on:random_seed=241155591:cts=off:i=2759:kws=inv_arity:fgj=on_2762 on theBenchmark for (2762ds/2759Mi)
% 214.79/31.07 % (3027895)Instruction limit reached!
% 214.79/31.07 % (3027895)------------------------------
% 214.79/31.07 % (3027895)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 214.79/31.07 % (3027895)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.79/31.07 % (3027895)CaDiCaL version: 2.1.3
% 214.79/31.07 % (3027895)Termination reason: Instruction limit
% 214.79/31.07 % (3027895)Termination phase: Saturation
% 214.79/31.07 % (3027895)Time elapsed: 0.941 s
% 214.79/31.07 % (3027895)Peak memory usage: 160 MB
% 214.79/31.07 % (3027895)Instructions burned: 2759 (million)
% 214.79/31.07 % (3027897)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:fde=unused:sp=weighted_frequency:sos=all:spb=goal_then_units:urr=ec_only:sac=on:random_seed=2842561196:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2751 on theBenchmark for (2751ds/5665Mi)
% 214.79/31.07 % (3027883)Instruction limit reached!
% 214.79/31.07 % (3027883)------------------------------
% 214.79/31.07 % (3027883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 214.79/31.07 % (3027883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 214.79/31.07 % (3027883)CaDiCaL version: 2.1.3
% 214.79/31.07 % (3027883)Termination reason: Instruction limit
% 214.79/31.07 % (3027883)Termination phase: Saturation
% 214.79/31.07 % (3027883)Time elapsed: 7.382 s
% 214.79/31.07 % (3027883)Peak memory usage: 302 MB
% 214.79/31.07 % (3027883)Instructions burned: 26457 (million)
% 214.79/31.07 % (3027899)dis+1011_1_anc=none:ncem=casc2026/models/loop3.pt:sil=16000:npcc=on:sos=on:lsd=20:urr=full:alpa=true:sac=on:random_seed=907913330:i=1532:ep=RS:ss=axioms_2745 on theBenchmark for (2745ds/1532Mi)
% 214.79/31.07 % (3027899)Instruction limit reached!
% 214.79/31.07 % (3027899)------------------------------
% 214.79/31.07 % (3027899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.95/34.13 % (3027899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.95/34.13 % (3027899)CaDiCaL version: 2.1.3
% 156.95/34.13 % (3027899)Termination reason: Instruction limit
% 156.95/34.13 % (3027899)Termination phase: Saturation
% 156.95/34.13 % (3027899)Time elapsed: 0.529 s
% 156.95/34.13 % (3027899)Peak memory usage: 152 MB
% 156.95/34.13 % (3027899)Instructions burned: 1533 (million)
% 156.95/34.13 % (3027901)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=3769232463:i=1565:sd=2:ss=axioms:sgt=32_2739 on theBenchmark for (2739ds/1565Mi)
% 156.95/34.13 % (3027867)Instruction limit reached!
% 156.95/34.13 % (3027867)------------------------------
% 156.95/34.13 % (3027867)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.95/34.13 % (3027867)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.95/34.13 % (3027867)CaDiCaL version: 2.1.3
% 156.95/34.13 % (3027867)Termination reason: Instruction limit
% 156.95/34.13 % (3027867)Termination phase: Saturation
% 156.95/34.13 % (3027867)Time elapsed: 12.530 s
% 156.95/34.13 % (3027867)Peak memory usage: 420 MB
% 156.95/34.13 % (3027867)Instructions burned: 33336 (million)
% 156.95/34.13 % (3027903)lrs-1011_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:sims=off:bsd=on:sp=unary_first:erd=off:spb=goal:lcm=reverse:gs=on:s2agt=8:random_seed=2269437429:i=1572:fgj=on:gsp=on_2737 on theBenchmark for (2737ds/1572Mi)
% 156.95/34.13 % (3027901)Instruction limit reached!
% 156.95/34.13 % (3027901)------------------------------
% 156.95/34.13 % (3027901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.95/34.13 % (3027901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.95/34.13 % (3027901)CaDiCaL version: 2.1.3
% 156.95/34.13 % (3027901)Termination reason: Instruction limit
% 156.95/34.13 % (3027901)Termination phase: Saturation
% 156.95/34.13 % (3027901)Time elapsed: 0.545 s
% 156.95/34.13 % (3027901)Peak memory usage: 157 MB
% 156.95/34.13 % (3027901)Instructions burned: 1566 (million)
% 156.95/34.13 % (3027897)Instruction limit reached!
% 156.95/34.13 % (3027897)------------------------------
% 156.95/34.13 % (3027897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.95/34.13 % (3027897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.95/34.13 % (3027897)CaDiCaL version: 2.1.3
% 156.95/34.13 % (3027897)Termination reason: Instruction limit
% 156.95/34.13 % (3027897)Termination phase: Saturation
% 156.95/34.13 % (3027897)Time elapsed: 1.821 s
% 156.95/34.13 % (3027897)Peak memory usage: 180 MB
% 156.95/34.13 % (3027897)Instructions burned: 5668 (million)
% 156.95/34.13 % (3027905)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=1844091995:i=6052:sd=4:ss=axioms:sgt=24_2732 on theBenchmark for (2732ds/6052Mi)
% 156.95/34.13 % (3027903)Instruction limit reached!
% 156.95/34.13 % (3027903)------------------------------
% 156.95/34.13 % (3027903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.95/34.13 % (3027903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.95/34.13 % (3027903)CaDiCaL version: 2.1.3
% 156.95/34.13 % (3027903)Termination reason: Instruction limit
% 156.95/34.13 % (3027903)Termination phase: Saturation
% 156.95/34.13 % (3027903)Time elapsed: 0.554 s
% 156.95/34.13 % (3027903)Peak memory usage: 157 MB
% 156.95/34.13 % (3027903)Instructions burned: 1574 (million)
% 156.95/34.13 % (3027906)lrs+21_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=arity:sos=on:erd=off:lcm=predicate:alpa=false:sac=on:random_seed=1201959511:i=3500:sd=1:bd=preordered:sup=off:ss=included_2731 on theBenchmark for (2731ds/3500Mi)
% 156.95/34.13 % (3027908)lrs+35_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:npcc=on:fde=none:sp=weighted_frequency:erd=off:spb=non_intro:updr=off:newcnf=on:random_seed=3411780310:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2730 on theBenchmark for (2730ds/1842Mi)
% 156.95/34.13 % (3027908)Instruction limit reached!
% 156.95/34.13 % (3027908)------------------------------
% 156.95/34.13 % (3027908)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.95/34.13 % (3027908)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.95/34.13 % (3027908)CaDiCaL version: 2.1.3
% 156.95/34.13 % (3027908)Termination reason: Instruction limit
% 156.95/34.13 % (3027908)Termination phase: Saturation
% 156.95/34.13 % (3027908)Time elapsed: 0.618 s
% 156.95/34.13 % (3027908)Peak memory usage: 139 MB
% 156.95/34.13 % (3027908)Instructions burned: 1844 (million)
% 156.95/34.13 % (3027911)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=783289710:i=66096:add=on_2722 on theBenchmark for (2722ds/66096Mi)
% 156.95/34.13 % (3027906)Instruction limit reached!
% 156.95/34.13 % (3027906)------------------------------
% 156.95/34.13 % (3027906)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.95/34.13 % (3027906)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.95/34.13 % (3027906)CaDiCaL version: 2.1.3
% 156.95/34.13 % (3027906)Termination reason: Instruction limit
% 156.95/34.13 % (3027906)Termination phase: Saturation
% 156.95/34.13 % (3027906)Time elapsed: 1.141 s
% 156.95/34.13 % (3027906)Peak memory usage: 160 MB
% 156.95/34.13 % (3027906)Instructions burned: 3503 (million)
% 156.95/34.13 % (3027913)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=1713736817:i=1884:sd=1:nm=60:ss=axioms_2718 on theBenchmark for (2718ds/1884Mi)
% 156.95/34.13 % (3027905)Instruction limit reached!
% 156.95/34.13 % (3027905)------------------------------
% 156.95/34.13 % (3027905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.95/34.13 % (3027905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.95/34.13 % (3027905)CaDiCaL version: 2.1.3
% 156.95/34.13 % (3027905)Termination reason: Instruction limit
% 156.95/34.13 % (3027905)Termination phase: Saturation
% 156.95/34.13 % (3027905)Time elapsed: 1.790 s
% 156.95/34.13 % (3027905)Peak memory usage: 170 MB
% 156.95/34.13 % (3027905)Instructions burned: 6053 (million)
% 156.95/34.13 % (3027915)lrs-1011_4:1_sil=16000:bsr=on:random_seed=3027703675:cts=off:i=5469:bs=on:fsr=off_2712 on theBenchmark for (2712ds/5469Mi)
% 156.95/34.13 % (3027913)Instruction limit reached!
% 156.95/34.13 % (3027913)------------------------------
% 156.95/34.13 % (3027913)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.95/34.13 % (3027913)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.95/34.13 % (3027913)CaDiCaL version: 2.1.3
% 156.95/34.13 % (3027913)Termination reason: Instruction limit
% 156.95/34.13 % (3027913)Termination phase: Saturation
% 156.95/34.13 % (3027913)Time elapsed: 0.636 s
% 156.95/34.13 % (3027913)Peak memory usage: 144 MB
% 156.95/34.13 % (3027913)Instructions burned: 1885 (million)
% 156.95/34.13 % (3027917)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=unary_frequency:urr=on:bce=on:alpa=false:sac=on:random_seed=435213665:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2711 on theBenchmark for (2711ds/2037Mi)
% 156.95/34.13 % (3027917)Instruction limit reached!
% 156.95/34.13 % (3027917)------------------------------
% 156.95/34.13 % (3027917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.95/34.13 % (3027917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.95/34.13 % (3027917)CaDiCaL version: 2.1.3
% 156.95/34.13 % (3027917)Termination reason: Instruction limit
% 156.95/34.13 % (3027917)Termination phase: Saturation
% 156.95/34.13 % (3027917)Time elapsed: 0.694 s
% 156.95/34.13 % (3027917)Peak memory usage: 160 MB
% 156.95/34.13 % (3027917)Instructions burned: 2038 (million)
% 156.95/34.13 % (3027919)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=284141709:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2702 on theBenchmark for (2702ds/2110Mi)
% 156.95/34.13 % (3027891)Instruction limit reached!
% 156.95/34.13 % (3027891)------------------------------
% 156.95/34.13 % (3027891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.95/34.13 % (3027891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.95/34.13 % (3027891)CaDiCaL version: 2.1.3
% 156.95/34.13 % (3027891)Termination reason: Instruction limit
% 156.95/34.13 % (3027891)Termination phase: Saturation
% 156.95/34.13 % (3027891)Time elapsed: 9.104 s
% 156.95/34.13 % (3027891)Peak memory usage: 382 MB
% 156.95/34.13 % (3027891)Instructions burned: 30754 (million)
% 156.95/34.13 % (3027919)Instruction limit reached!
% 156.95/34.13 % (3027919)------------------------------
% 156.95/34.13 % (3027919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.95/34.13 % (3027919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.95/34.13 % (3027919)CaDiCaL version: 2.1.3
% 156.95/34.13 % (3027919)Termination reason: Instruction limit
% 156.95/34.13 % (3027919)Termination phase: Saturation
% 156.95/34.13 % (3027919)Time elapsed: 0.684 s
% 156.95/34.13 % (3027919)Peak memory usage: 165 MB
% 156.95/34.13 % (3027919)Instructions burned: 2112 (million)
% 156.95/34.13 % (3027922)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:spb=units:acc=on:bsr=unit_only:gs=on:sac=on:random_seed=1253483052:cond=fast:i=4891_2694 on theBenchmark for (2694ds/4891Mi)
% 156.95/34.13 % (3027921)dis-1010_1_anc=all_dependent:ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_first:spb=goal:lcm=reverse:fd=off:flr=on:random_seed=164167095:i=2430:add=off:aac=none:nm=16_2694 on theBenchmark for (2694ds/2430Mi)
% 156.95/34.13 % (3027915)Instruction limit reached!
% 156.95/34.13 % (3027915)------------------------------
% 156.95/34.13 % (3027915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.95/34.13 % (3027915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.95/34.13 % (3027915)CaDiCaL version: 2.1.3
% 156.95/34.13 % (3027915)Termination reason: Instruction limit
% 156.95/34.13 % (3027915)Termination phase: Saturation
% 156.95/34.13 % (3027915)Time elapsed: 1.931 s
% 156.95/34.13 % (3027915)Peak memory usage: 108 MB
% 156.95/34.13 % (3027915)Instructions burned: 5470 (million)
% 156.95/34.13 % (3027925)lrs+4_1_anc=all:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sos=on:spb=goal_then_units:lcm=reverse:gs=on:s2agt=16:sac=on:newcnf=on:random_seed=1061970443:st=2:i=14845:sd=2:ss=included:fsd=on_2692 on theBenchmark for (2692ds/14845Mi)
% 156.95/34.13 % (3027921)Instruction limit reached!
% 156.95/34.13 % (3027921)------------------------------
% 156.95/34.13 % (3027921)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.95/34.13 % (3027921)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.95/34.13 % (3027921)CaDiCaL version: 2.1.3
% 156.95/34.13 % (3027921)Termination reason: Instruction limit
% 156.95/34.13 % (3027921)Termination phase: Saturation
% 156.95/34.13 % (3027921)Time elapsed: 0.847 s
% 156.95/34.13 % (3027921)Peak memory usage: 149 MB
% 156.95/34.13 % (3027921)Instructions burned: 2433 (million)
% 156.95/34.13 % (3027927)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=290210742:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2684 on theBenchmark for (2684ds/7534Mi)
% 156.95/34.13 % (3027893)Instruction limit reached!
% 156.95/34.13 % (3027893)------------------------------
% 156.95/34.13 % (3027893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.95/34.13 % (3027893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.95/34.13 % (3027893)CaDiCaL version: 2.1.3
% 156.95/34.13 % (3027893)Termination reason: Instruction limit
% 156.95/34.13 % (3027893)Termination phase: Saturation
% 156.95/34.13 % (3027893)Time elapsed: 9.411 s
% 156.95/34.13 % (3027893)Peak memory usage: 704 MB
% 156.95/34.13 % (3027893)Instructions burned: 26474 (million)
% 156.95/34.13 % (3027929)lrs-1002_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=ground:npcc=on:prc=on:fde=none:sims=off:spb=goal:bsr=unit_only:s2agt=32:random_seed=772668728:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2679 on theBenchmark for (2679ds/10353Mi)
% 156.95/34.13 % (3027922)Instruction limit reached!
% 156.95/34.13 % (3027922)------------------------------
% 156.95/34.13 % (3027922)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 156.95/34.13 % (3027922)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 156.95/34.13 % (3027922)CaDiCaL version: 2.1.3
% 156.95/34.13 % (3027922)Termination reason: Instruction limit
% 156.95/34.13 % (3027922)Termination phase: Saturation
% 156.95/34.13 % (3027922)Time elapsed: 1.603 s
% 156.95/34.13 % (3027922)Peak memory usage: 163 MB
% 156.95/34.13 % (3027922)Instructions burned: 4894 (million)
% 156.95/34.13 % (3027931)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=857573208:i=7860_2677 on theBenchmark for (2677ds/7860Mi)
% 156.95/34.13 % (3027929)First to succeed.
% 156.95/34.13 % (3027929)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-3027747"
% 156.95/34.13 % (3027929)Refutation found. Thanks to Tanya!
% 156.95/34.13 % SZS status Theorem for theBenchmark
% 156.95/34.13 % SZS output start Proof for theBenchmark
% See solution above
% 236.61/34.23 % (3027929)------------------------------
% 236.61/34.23 % (3027929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 236.61/34.23 % (3027929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 236.61/34.23 % (3027929)CaDiCaL version: 2.1.3
% 236.61/34.23 % (3027929)Termination reason: Refutation
% 236.61/34.23 % (3027929)Time elapsed: 1.146 s
% 236.61/34.23 % (3027929)Peak memory usage: 161 MB
% 236.61/34.23 % (3027929)Instructions burned: 3283 (million)
% 236.61/34.23 % (3027929)------------------------------
% 236.61/34.23 % (3027929)------------------------------
% 236.61/34.23 % (3027747)Success in time 33.602 s
% 236.61/34.23 % Vampire exiting
%------------------------------------------------------------------------------