%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : SEU377+1 : TPTP v9.3.1. Released v3.3.0.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% Computer : n004.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:48:36 PM UTC 2026
% Result : Theorem 105.21s 30.69s
% Output : Refutation 211.73s
% Verified :
% SZS Type : Refutation
% Derivation depth : 55
% Number of leaves : 44
% Syntax : Number of formulae : 382 ( 45 unt; 17 def)
% Number of atoms : 2040 ( 78 equ)
% Maximal formula atoms : 16 ( 5 avg)
% Number of connectives : 2874 (1216 ~;1461 |; 114 &)
% ( 32 <=>; 51 =>; 0 <=; 0 <~>)
% Maximal formula depth : 22 ( 7 avg)
% Maximal term depth : 3 ( 1 avg)
% Number of predicates : 39 ( 37 usr; 17 prp; 0-3 aty)
% Number of functors : 20 ( 20 usr; 5 con; 0-4 aty)
% Number of variables : 536 ( 0 sgn 523 !; 13 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0,X1] :
( ( one_sorted_str(X0)
& net_str(X1,X0) )
=> ( strict_net_str(X1,X0)
=> X1 = net_str_of(X0,the_carrier(X1),the_InternalRel(X1),the_mapping(X0,X1)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',abstractness_v6_waybel_0) ).
fof(f10,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0) )
=> ! [X1] :
( ( ~ empty_carrier(X1)
& net_str(X1,X0) )
=> ! [X2] :
( is_often_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',d12_waybel_0) ).
fof(f11,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(f13,axiom,
! [X0] :
( rel_str(X0)
=> ( transitive_relstr(X0)
<=> ! [X1] :
( element(X1,the_carrier(X0))
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ! [X3] :
( element(X3,the_carrier(X0))
=> ( ( related(X0,X1,X2)
& related(X0,X2,X3) )
=> related(X0,X1,X3) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d2_yellow_0) ).
fof(f14,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& rel_str(X0) )
=> ( directed_relstr(X0)
<=> ! [X1] :
( element(X1,the_carrier(X0))
=> ! [X2] :
( element(X2,the_carrier(X0))
=> ? [X3] :
( element(X3,the_carrier(X0))
& related(X0,X1,X3)
& related(X0,X2,X3) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d5_yellow_6) ).
fof(f15,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0) )
=> ! [X1] :
( ( ~ empty_carrier(X1)
& net_str(X1,X0) )
=> ! [X2] :
( element(X2,the_carrier(X1))
=> apply_netmap(X0,X1,X2) = apply_on_structs(X1,X0,the_mapping(X0,X1),X2) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',d8_waybel_0) ).
fof(f25,axiom,
! [X0,X1,X2] :
( ( 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(f26,axiom,
! [X0] :
( rel_str(X0)
=> one_sorted_str(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_orders_2) ).
fof(f28,axiom,
! [X0] :
( one_sorted_str(X0)
=> ! [X1] :
( net_str(X1,X0)
=> rel_str(X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_l1_waybel_0) ).
fof(f32,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(f34,axiom,
! [X0] :
( rel_str(X0)
=> relation_of2_as_subset(the_InternalRel(X0),the_carrier(X0),the_carrier(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_u1_orders_2) ).
fof(f36,axiom,
! [X0,X1] :
( ( one_sorted_str(X0)
& net_str(X1,X0) )
=> ( function(the_mapping(X0,X1))
& quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
& relation_of2_as_subset(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dt_u1_waybel_0) ).
fof(f41,axiom,
! [X0] :
? [X1] : element(X1,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',existence_m1_subset_1) ).
fof(f47,axiom,
! [X0,X1] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0)
& ~ empty_carrier(X1)
& net_str(X1,X0) )
=> ( ~ empty(the_mapping(X0,X1))
& relation(the_mapping(X0,X1))
& function(the_mapping(X0,X1))
& quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0)) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc15_yellow_6) ).
fof(f48,axiom,
! [X0,X1,X2] :
( ( one_sorted_str(X0)
& transitive_relstr(X1)
& net_str(X1,X0) )
=> ( transitive_relstr(preimage_subnetstr(X0,X1,X2))
& strict_net_str(preimage_subnetstr(X0,X1,X2),X0)
& full_subnetstr(preimage_subnetstr(X0,X1,X2),X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc17_yellow_6) ).
fof(f49,axiom,
! [X0] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0) )
=> ~ empty(the_carrier(X0)) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc1_struct_0) ).
fof(f51,axiom,
( empty(empty_set)
& relation(empty_set) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc4_relat_1) ).
fof(f53,axiom,
! [X0,X1,X2,X3] :
( ( one_sorted_str(X0)
& ~ empty(X1)
& relation_of2(X2,X1,X1)
& function(X3)
& quasi_total(X3,X1,the_carrier(X0))
& relation_of2(X3,X1,the_carrier(X0)) )
=> ( ~ empty_carrier(net_str_of(X0,X1,X2,X3))
& strict_net_str(net_str_of(X0,X1,X2,X3),X0) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fc6_waybel_0) ).
fof(f70,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(f71,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(f72,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(f75,axiom,
! [X0,X1] :
( in(X0,X1)
=> element(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t1_subset) ).
fof(f76,axiom,
! [X0] :
( one_sorted_str(X0)
=> ! [X1] :
( ( ~ empty_carrier(X1)
& net_str(X1,X0) )
=> ! [X2] :
( ( ~ empty_carrier(X2)
& full_subnetstr(X2,X0,X1)
& subnetstr(X2,X0,X1) )
=> ! [X3] :
( element(X3,the_carrier(X1))
=> ! [X4] :
( element(X4,the_carrier(X1))
=> ! [X5] :
( element(X5,the_carrier(X2))
=> ! [X6] :
( element(X6,the_carrier(X2))
=> ( ( X3 = X5
& X4 = X6
& related(X1,X3,X4) )
=> related(X2,X5,X6) ) ) ) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t21_yellow_6) ).
fof(f77,axiom,
! [X0,X1] :
( element(X0,X1)
=> ( empty(X1)
| in(X0,X1) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t2_subset) ).
fof(f78,conjecture,
! [X0] :
( ( ~ empty_carrier(X0)
& one_sorted_str(X0) )
=> ! [X1] :
( ( ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) )
=> ! [X2] :
( is_often_in(X0,X1,X2)
=> ( ~ empty_carrier(preimage_subnetstr(X0,X1,X2))
& directed_relstr(preimage_subnetstr(X0,X1,X2)) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t30_yellow_6) ).
fof(f79,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] :
( is_often_in(X0,X1,X2)
=> ( ~ empty_carrier(preimage_subnetstr(X0,X1,X2))
& directed_relstr(preimage_subnetstr(X0,X1,X2)) ) ) ) ),
inference(negated_conjecture,[status(cth)],[f78]) ).
fof(f81,axiom,
! [X0,X1,X2,X3] :
( ( function(X3)
& quasi_total(X3,X0,X1)
& relation_of2_as_subset(X3,X0,X1) )
=> ( X1 != empty_set
=> ! [X4] :
( in(X4,relation_inverse_image(X3,X2))
<=> ( in(X4,X0)
& in(apply(X3,X4),X2) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t46_funct_2) ).
fof(f85,axiom,
! [X0,X1] :
~ ( in(X0,X1)
& empty(X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',t7_boole) ).
fof(f98,plain,
! [X0,X1] :
( X1 = net_str_of(X0,the_carrier(X1),the_InternalRel(X1),the_mapping(X0,X1))
| ~ strict_net_str(X1,X0)
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(ennf_transformation,[],[f1]) ).
fof(f99,plain,
! [X0,X1] :
( X1 = net_str_of(X0,the_carrier(X1),the_InternalRel(X1),the_mapping(X0,X1))
| ~ strict_net_str(X1,X0)
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(flattening,[],[f98]) ).
fof(f108,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( is_often_in(X0,X1,X2)
<=> ! [X3] :
( ? [X4] :
( element(X4,the_carrier(X1))
& related(X1,X3,X4)
& in(apply_netmap(X0,X1,X4),X2) )
| ~ element(X3,the_carrier(X1)) ) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f10]) ).
fof(f109,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( is_often_in(X0,X1,X2)
<=> ! [X3] :
( ? [X4] :
( element(X4,the_carrier(X1))
& related(X1,X3,X4)
& in(apply_netmap(X0,X1,X4),X2) )
| ~ element(X3,the_carrier(X1)) ) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(flattening,[],[f108]) ).
fof(f110,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,[],[f11]) ).
fof(f111,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,[],[f110]) ).
fof(f113,plain,
! [X0] :
( ( transitive_relstr(X0)
<=> ! [X1] :
( ! [X2] :
( ! [X3] :
( related(X0,X1,X3)
| ~ related(X0,X1,X2)
| ~ related(X0,X2,X3)
| ~ element(X3,the_carrier(X0)) )
| ~ element(X2,the_carrier(X0)) )
| ~ element(X1,the_carrier(X0)) ) )
| ~ rel_str(X0) ),
inference(ennf_transformation,[],[f13]) ).
fof(f114,plain,
! [X0] :
( ( transitive_relstr(X0)
<=> ! [X1] :
( ! [X2] :
( ! [X3] :
( related(X0,X1,X3)
| ~ related(X0,X1,X2)
| ~ related(X0,X2,X3)
| ~ element(X3,the_carrier(X0)) )
| ~ element(X2,the_carrier(X0)) )
| ~ element(X1,the_carrier(X0)) ) )
| ~ rel_str(X0) ),
inference(flattening,[],[f113]) ).
fof(f115,plain,
! [X0] :
( ( directed_relstr(X0)
<=> ! [X1] :
( ! [X2] :
( ? [X3] :
( element(X3,the_carrier(X0))
& related(X0,X1,X3)
& related(X0,X2,X3) )
| ~ element(X2,the_carrier(X0)) )
| ~ element(X1,the_carrier(X0)) ) )
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(ennf_transformation,[],[f14]) ).
fof(f116,plain,
! [X0] :
( ( directed_relstr(X0)
<=> ! [X1] :
( ! [X2] :
( ? [X3] :
( element(X3,the_carrier(X0))
& related(X0,X1,X3)
& related(X0,X2,X3) )
| ~ element(X2,the_carrier(X0)) )
| ~ element(X1,the_carrier(X0)) ) )
| empty_carrier(X0)
| ~ rel_str(X0) ),
inference(flattening,[],[f115]) ).
fof(f117,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,[],[f15]) ).
fof(f118,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,[],[f117]) ).
fof(f127,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,[],[f25]) ).
fof(f128,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,[],[f127]) ).
fof(f129,plain,
! [X0] :
( one_sorted_str(X0)
| ~ rel_str(X0) ),
inference(ennf_transformation,[],[f26]) ).
fof(f130,plain,
! [X0] :
( ! [X1] :
( rel_str(X1)
| ~ net_str(X1,X0) )
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f28]) ).
fof(f132,plain,
! [X0,X1] :
( ! [X2] :
( net_str(X2,X0)
| ~ subnetstr(X2,X0,X1) )
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(ennf_transformation,[],[f32]) ).
fof(f133,plain,
! [X0,X1] :
( ! [X2] :
( net_str(X2,X0)
| ~ subnetstr(X2,X0,X1) )
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(flattening,[],[f132]) ).
fof(f135,plain,
! [X0] :
( relation_of2_as_subset(the_InternalRel(X0),the_carrier(X0),the_carrier(X0))
| ~ rel_str(X0) ),
inference(ennf_transformation,[],[f34]) ).
fof(f136,plain,
! [X0,X1] :
( ( function(the_mapping(X0,X1))
& quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
& relation_of2_as_subset(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0)) )
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(ennf_transformation,[],[f36]) ).
fof(f137,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,[],[f136]) ).
fof(f142,plain,
! [X0,X1] :
( ( ~ empty(the_mapping(X0,X1))
& relation(the_mapping(X0,X1))
& function(the_mapping(X0,X1))
& quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0)) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ net_str(X1,X0) ),
inference(ennf_transformation,[],[f47]) ).
fof(f143,plain,
! [X0,X1] :
( ( ~ empty(the_mapping(X0,X1))
& relation(the_mapping(X0,X1))
& function(the_mapping(X0,X1))
& quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0)) )
| empty_carrier(X0)
| ~ one_sorted_str(X0)
| empty_carrier(X1)
| ~ net_str(X1,X0) ),
inference(flattening,[],[f142]) ).
fof(f144,plain,
! [X0,X1,X2] :
( ( transitive_relstr(preimage_subnetstr(X0,X1,X2))
& strict_net_str(preimage_subnetstr(X0,X1,X2),X0)
& full_subnetstr(preimage_subnetstr(X0,X1,X2),X0,X1) )
| ~ one_sorted_str(X0)
| ~ transitive_relstr(X1)
| ~ net_str(X1,X0) ),
inference(ennf_transformation,[],[f48]) ).
fof(f145,plain,
! [X0,X1,X2] :
( ( transitive_relstr(preimage_subnetstr(X0,X1,X2))
& strict_net_str(preimage_subnetstr(X0,X1,X2),X0)
& full_subnetstr(preimage_subnetstr(X0,X1,X2),X0,X1) )
| ~ one_sorted_str(X0)
| ~ transitive_relstr(X1)
| ~ net_str(X1,X0) ),
inference(flattening,[],[f144]) ).
fof(f146,plain,
! [X0] :
( ~ empty(the_carrier(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f49]) ).
fof(f147,plain,
! [X0] :
( ~ empty(the_carrier(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(flattening,[],[f146]) ).
fof(f150,plain,
! [X0,X1,X2,X3] :
( ( ~ empty_carrier(net_str_of(X0,X1,X2,X3))
& strict_net_str(net_str_of(X0,X1,X2,X3),X0) )
| ~ one_sorted_str(X0)
| empty(X1)
| ~ relation_of2(X2,X1,X1)
| ~ function(X3)
| ~ quasi_total(X3,X1,the_carrier(X0))
| ~ relation_of2(X3,X1,the_carrier(X0)) ),
inference(ennf_transformation,[],[f53]) ).
fof(f151,plain,
! [X0,X1,X2,X3] :
( ( ~ empty_carrier(net_str_of(X0,X1,X2,X3))
& strict_net_str(net_str_of(X0,X1,X2,X3),X0) )
| ~ one_sorted_str(X0)
| empty(X1)
| ~ relation_of2(X2,X1,X1)
| ~ function(X3)
| ~ quasi_total(X3,X1,the_carrier(X0))
| ~ relation_of2(X3,X1,the_carrier(X0)) ),
inference(flattening,[],[f150]) ).
fof(f162,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,[],[f70]) ).
fof(f163,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,[],[f162]) ).
fof(f164,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,[],[f71]) ).
fof(f165,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,[],[f164]) ).
fof(f167,plain,
! [X0,X1] :
( element(X0,X1)
| ~ in(X0,X1) ),
inference(ennf_transformation,[],[f75]) ).
fof(f168,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( related(X2,X5,X6)
| X3 != X5
| X4 != X6
| ~ related(X1,X3,X4)
| ~ element(X6,the_carrier(X2)) )
| ~ element(X5,the_carrier(X2)) )
| ~ element(X4,the_carrier(X1)) )
| ~ element(X3,the_carrier(X1)) )
| empty_carrier(X2)
| ~ full_subnetstr(X2,X0,X1)
| ~ subnetstr(X2,X0,X1) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| ~ one_sorted_str(X0) ),
inference(ennf_transformation,[],[f76]) ).
fof(f169,plain,
! [X0] :
( ! [X1] :
( ! [X2] :
( ! [X3] :
( ! [X4] :
( ! [X5] :
( ! [X6] :
( related(X2,X5,X6)
| X3 != X5
| X4 != X6
| ~ related(X1,X3,X4)
| ~ element(X6,the_carrier(X2)) )
| ~ element(X5,the_carrier(X2)) )
| ~ element(X4,the_carrier(X1)) )
| ~ element(X3,the_carrier(X1)) )
| empty_carrier(X2)
| ~ full_subnetstr(X2,X0,X1)
| ~ subnetstr(X2,X0,X1) )
| empty_carrier(X1)
| ~ net_str(X1,X0) )
| ~ one_sorted_str(X0) ),
inference(flattening,[],[f168]) ).
fof(f170,plain,
! [X0,X1] :
( empty(X1)
| in(X0,X1)
| ~ element(X0,X1) ),
inference(ennf_transformation,[],[f77]) ).
fof(f171,plain,
! [X0,X1] :
( empty(X1)
| in(X0,X1)
| ~ element(X0,X1) ),
inference(flattening,[],[f170]) ).
fof(f172,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( empty_carrier(preimage_subnetstr(X0,X1,X2))
| ~ directed_relstr(preimage_subnetstr(X0,X1,X2)) )
& is_often_in(X0,X1,X2) )
& ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) )
& ~ empty_carrier(X0)
& one_sorted_str(X0) ),
inference(ennf_transformation,[],[f79]) ).
fof(f173,plain,
? [X0] :
( ? [X1] :
( ? [X2] :
( ( empty_carrier(preimage_subnetstr(X0,X1,X2))
| ~ directed_relstr(preimage_subnetstr(X0,X1,X2)) )
& is_often_in(X0,X1,X2) )
& ~ empty_carrier(X1)
& transitive_relstr(X1)
& directed_relstr(X1)
& net_str(X1,X0) )
& ~ empty_carrier(X0)
& one_sorted_str(X0) ),
inference(flattening,[],[f172]) ).
fof(f175,plain,
! [X0,X1,X2,X3] :
( ! [X4] :
( in(X4,relation_inverse_image(X3,X2))
<=> ( in(X4,X0)
& in(apply(X3,X4),X2) ) )
| empty_set = X1
| ~ function(X3)
| ~ quasi_total(X3,X0,X1)
| ~ relation_of2_as_subset(X3,X0,X1) ),
inference(ennf_transformation,[],[f81]) ).
fof(f176,plain,
! [X0,X1,X2,X3] :
( ! [X4] :
( in(X4,relation_inverse_image(X3,X2))
<=> ( in(X4,X0)
& in(apply(X3,X4),X2) ) )
| empty_set = X1
| ~ function(X3)
| ~ quasi_total(X3,X0,X1)
| ~ relation_of2_as_subset(X3,X0,X1) ),
inference(flattening,[],[f175]) ).
fof(f181,plain,
! [X0,X1] :
( ~ in(X0,X1)
| ~ empty(X1) ),
inference(ennf_transformation,[],[f85]) ).
fof(f183,plain,
! [X0,X1] :
( net_str_of(X0,the_carrier(X1),the_InternalRel(X1),the_mapping(X0,X1)) = X1
| ~ one_sorted_str(X0)
| ~ strict_net_str(X1,X0)
| ~ net_str(X1,X0) ),
inference(cnf_transformation,[],[f99]) ).
fof(f190,plain,
! [X2,X3,X0,X1] :
( in(apply_netmap(X0,X1,sK1(X0,X1,X2,X3)),X2)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X3,the_carrier(X1))
| ~ one_sorted_str(X0)
| ~ is_often_in(X0,X1,X2) ),
inference(cnf_transformation,[],[f109]) ).
fof(f191,plain,
! [X2,X3,X0,X1] :
( related(X1,X3,sK1(X0,X1,X2,X3))
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X3,the_carrier(X1))
| ~ one_sorted_str(X0)
| ~ is_often_in(X0,X1,X2) ),
inference(cnf_transformation,[],[f109]) ).
fof(f192,plain,
! [X2,X3,X0,X1] :
( element(sK1(X0,X1,X2,X3),the_carrier(X1))
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X3,the_carrier(X1))
| ~ one_sorted_str(X0)
| ~ is_often_in(X0,X1,X2) ),
inference(cnf_transformation,[],[f109]) ).
fof(f194,plain,
! [X2,X3,X0,X1] :
( preimage_subnetstr(X0,X1,X2) != X3
| ~ net_str(X1,X0)
| ~ subnetstr(X3,X0,X1)
| ~ strict_net_str(X3,X0)
| the_carrier(X3) = function_invverse_img_as_carrier_subset(X1,X0,the_mapping(X0,X1),X2)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f111]) ).
fof(f200,plain,
! [X2,X3,X0,X1] :
( ~ related(X0,X2,X3)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| ~ element(X3,the_carrier(X0))
| ~ rel_str(X0)
| ~ related(X0,X1,X2)
| related(X0,X1,X3)
| ~ transitive_relstr(X0) ),
inference(cnf_transformation,[],[f114]) ).
fof(f207,plain,
! [X2,X0,X1] :
( related(X0,X2,sK7(X0,X1,X2))
| empty_carrier(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| ~ rel_str(X0)
| ~ directed_relstr(X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f208,plain,
! [X2,X0,X1] :
( related(X0,X1,sK7(X0,X1,X2))
| empty_carrier(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| ~ rel_str(X0)
| ~ directed_relstr(X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f209,plain,
! [X2,X0,X1] :
( element(sK7(X0,X1,X2),the_carrier(X0))
| empty_carrier(X0)
| ~ element(X1,the_carrier(X0))
| ~ element(X2,the_carrier(X0))
| ~ rel_str(X0)
| ~ directed_relstr(X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f210,plain,
! [X3,X0] :
( ~ related(X0,sK6(X0),X3)
| empty_carrier(X0)
| ~ rel_str(X0)
| ~ related(X0,sK5(X0),X3)
| ~ element(X3,the_carrier(X0))
| directed_relstr(X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f211,plain,
! [X0] :
( element(sK6(X0),the_carrier(X0))
| empty_carrier(X0)
| ~ rel_str(X0)
| directed_relstr(X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f212,plain,
! [X0] :
( element(sK5(X0),the_carrier(X0))
| empty_carrier(X0)
| ~ rel_str(X0)
| directed_relstr(X0) ),
inference(cnf_transformation,[],[f116]) ).
fof(f213,plain,
! [X2,X0,X1] :
( apply_netmap(X0,X1,X2) = apply_on_structs(X1,X0,the_mapping(X0,X1),X2)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f118]) ).
fof(f219,plain,
! [X2,X0,X1] :
( subnetstr(preimage_subnetstr(X0,X1,X2),X0,X1)
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(cnf_transformation,[],[f128]) ).
fof(f221,plain,
! [X0] :
( ~ rel_str(X0)
| one_sorted_str(X0) ),
inference(cnf_transformation,[],[f129]) ).
fof(f222,plain,
! [X0,X1] :
( ~ net_str(X1,X0)
| ~ one_sorted_str(X0)
| rel_str(X1) ),
inference(cnf_transformation,[],[f130]) ).
fof(f224,plain,
! [X2,X0,X1] :
( ~ subnetstr(X2,X0,X1)
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0)
| net_str(X2,X0) ),
inference(cnf_transformation,[],[f133]) ).
fof(f226,plain,
! [X0] :
( relation_of2_as_subset(the_InternalRel(X0),the_carrier(X0),the_carrier(X0))
| ~ rel_str(X0) ),
inference(cnf_transformation,[],[f135]) ).
fof(f227,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,[],[f137]) ).
fof(f228,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,[],[f137]) ).
fof(f229,plain,
! [X0,X1] :
( function(the_mapping(X0,X1))
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(cnf_transformation,[],[f137]) ).
fof(f234,plain,
! [X0] : element(sK12(X0),X0),
inference(cnf_transformation,[],[f41]) ).
fof(f240,plain,
! [X0,X1] :
( quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0) ),
inference(cnf_transformation,[],[f143]) ).
fof(f241,plain,
! [X0,X1] :
( function(the_mapping(X0,X1))
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ net_str(X1,X0) ),
inference(cnf_transformation,[],[f143]) ).
fof(f244,plain,
! [X2,X0,X1] :
( full_subnetstr(preimage_subnetstr(X0,X1,X2),X0,X1)
| ~ transitive_relstr(X1)
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(cnf_transformation,[],[f145]) ).
fof(f245,plain,
! [X2,X0,X1] :
( strict_net_str(preimage_subnetstr(X0,X1,X2),X0)
| ~ transitive_relstr(X1)
| ~ one_sorted_str(X0)
| ~ net_str(X1,X0) ),
inference(cnf_transformation,[],[f145]) ).
fof(f247,plain,
! [X0] :
( ~ empty(the_carrier(X0))
| empty_carrier(X0)
| ~ one_sorted_str(X0) ),
inference(cnf_transformation,[],[f147]) ).
fof(f250,plain,
empty(empty_set),
inference(cnf_transformation,[],[f51]) ).
fof(f253,plain,
! [X2,X3,X0,X1] :
( ~ empty_carrier(net_str_of(X0,X1,X2,X3))
| ~ quasi_total(X3,X1,the_carrier(X0))
| ~ function(X3)
| ~ relation_of2(X2,X1,X1)
| empty(X1)
| ~ one_sorted_str(X0)
| ~ relation_of2(X3,X1,the_carrier(X0)) ),
inference(cnf_transformation,[],[f151]) ).
fof(f291,plain,
! [X2,X3,X0,X1] :
( apply_on_structs(X0,X1,X2,X3) = apply(X2,X3)
| ~ relation_of2(X2,the_carrier(X0),the_carrier(X1))
| ~ quasi_total(X2,the_carrier(X0),the_carrier(X1))
| ~ function(X2)
| ~ one_sorted_str(X1)
| empty_carrier(X1)
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ element(X3,the_carrier(X0)) ),
inference(cnf_transformation,[],[f163]) ).
fof(f292,plain,
! [X2,X3,X0,X1] :
( function_invverse_img_as_carrier_subset(X0,X1,X2,X3) = relation_inverse_image(X2,X3)
| ~ quasi_total(X2,the_carrier(X0),the_carrier(X1))
| ~ function(X2)
| ~ one_sorted_str(X1)
| ~ one_sorted_str(X0)
| ~ relation_of2(X2,the_carrier(X0),the_carrier(X1)) ),
inference(cnf_transformation,[],[f165]) ).
fof(f293,plain,
! [X2,X0,X1] :
( ~ relation_of2(X2,X0,X1)
| relation_of2_as_subset(X2,X0,X1) ),
inference(cnf_transformation,[],[f72]) ).
fof(f294,plain,
! [X2,X0,X1] :
( ~ relation_of2_as_subset(X2,X0,X1)
| relation_of2(X2,X0,X1) ),
inference(cnf_transformation,[],[f72]) ).
fof(f297,plain,
! [X0,X1] :
( ~ in(X0,X1)
| element(X0,X1) ),
inference(cnf_transformation,[],[f167]) ).
fof(f298,plain,
! [X2,X3,X0,X1,X6,X4,X5] :
( X4 != X6
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ subnetstr(X2,X0,X1)
| ~ full_subnetstr(X2,X0,X1)
| empty_carrier(X2)
| ~ element(X3,the_carrier(X1))
| ~ element(X4,the_carrier(X1))
| ~ element(X5,the_carrier(X2))
| ~ element(X6,the_carrier(X2))
| ~ related(X1,X3,X4)
| ~ one_sorted_str(X0)
| X3 != X5
| related(X2,X5,X6) ),
inference(cnf_transformation,[],[f169]) ).
fof(f299,plain,
! [X0,X1] :
( ~ element(X0,X1)
| in(X0,X1)
| empty(X1) ),
inference(cnf_transformation,[],[f171]) ).
fof(f300,plain,
( ~ directed_relstr(preimage_subnetstr(sK31,sK32,sK33))
| empty_carrier(preimage_subnetstr(sK31,sK32,sK33)) ),
inference(cnf_transformation,[],[f173]) ).
fof(f301,plain,
is_often_in(sK31,sK32,sK33),
inference(cnf_transformation,[],[f173]) ).
fof(f302,plain,
net_str(sK32,sK31),
inference(cnf_transformation,[],[f173]) ).
fof(f303,plain,
directed_relstr(sK32),
inference(cnf_transformation,[],[f173]) ).
fof(f304,plain,
transitive_relstr(sK32),
inference(cnf_transformation,[],[f173]) ).
fof(f305,plain,
~ empty_carrier(sK32),
inference(cnf_transformation,[],[f173]) ).
fof(f306,plain,
one_sorted_str(sK31),
inference(cnf_transformation,[],[f173]) ).
fof(f307,plain,
~ empty_carrier(sK31),
inference(cnf_transformation,[],[f173]) ).
fof(f310,plain,
! [X2,X3,X0,X1,X4] :
( ~ in(X4,relation_inverse_image(X3,X2))
| ~ quasi_total(X3,X0,X1)
| ~ function(X3)
| empty_set = X1
| in(X4,X0)
| ~ relation_of2_as_subset(X3,X0,X1) ),
inference(cnf_transformation,[],[f176]) ).
fof(f311,plain,
! [X2,X3,X0,X1,X4] :
( ~ in(apply(X3,X4),X2)
| ~ quasi_total(X3,X0,X1)
| ~ function(X3)
| empty_set = X1
| ~ relation_of2_as_subset(X3,X0,X1)
| ~ in(X4,X0)
| in(X4,relation_inverse_image(X3,X2)) ),
inference(cnf_transformation,[],[f176]) ).
fof(f315,plain,
! [X0,X1] :
( ~ in(X0,X1)
| ~ empty(X1) ),
inference(cnf_transformation,[],[f181]) ).
fof(f317,definition,
sF34 = preimage_subnetstr(sK31,sK32,sK33),
introduced(definition,[new_symbols(definition,[sF34])],[function_definition]) ).
fof(f318,plain,
preimage_subnetstr(sK31,sK32,sK33) = sF34,
inference(reorient_equations,[],[f317]) ).
fof(f319,plain,
( ~ directed_relstr(sF34)
| empty_carrier(sF34) ),
inference(definition_folding,[],[f300,f318,f318]) ).
fof(f321,definition,
( spl35_1
<=> empty_carrier(sF34) ),
introduced(definition,[new_symbols(definition,[spl35_1])],[avatar_definition]) ).
fof(f322,plain,
( ~ empty_carrier(sF34)
| spl35_1 ),
inference(avatar_component_clause,[],[f321]) ).
fof(f323,plain,
( empty_carrier(sF34)
| ~ spl35_1 ),
inference(avatar_component_clause,[],[f321]) ).
fof(f325,definition,
( spl35_2
<=> directed_relstr(sF34) ),
introduced(definition,[new_symbols(definition,[spl35_2])],[avatar_definition]) ).
fof(f327,plain,
( ~ directed_relstr(sF34)
| spl35_2 ),
inference(avatar_component_clause,[],[f325]) ).
fof(f328,plain,
( spl35_1
| ~ spl35_2 ),
inference(avatar_split_clause,[],[f319,f325,f321]) ).
fof(f334,plain,
! [X2,X0,X1] :
( apply_netmap(X0,X1,X2) = apply(the_mapping(X0,X1),X2)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ one_sorted_str(X0)
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ function(the_mapping(X0,X1))
| ~ one_sorted_str(X0)
| empty_carrier(X0)
| ~ one_sorted_str(X1)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1)) ),
inference(superposition,[],[f213,f291]) ).
fof(f335,plain,
! [X2,X0,X1] :
( apply_netmap(X0,X1,X2) = apply(the_mapping(X0,X1),X2)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ one_sorted_str(X0)
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ quasi_total(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ function(the_mapping(X0,X1))
| ~ one_sorted_str(X1) ),
inference(duplicate_literal_removal,[],[f334]) ).
fof(f337,plain,
! [X2,X0,X1] :
( apply_netmap(X0,X1,X2) = apply(the_mapping(X0,X1),X2)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ one_sorted_str(X0)
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ function(the_mapping(X0,X1))
| ~ one_sorted_str(X1) ),
inference(forward_subsumption_resolution,[],[f335,f240]) ).
fof(f339,plain,
! [X2,X0,X1] :
( apply_netmap(X0,X1,X2) = apply(the_mapping(X0,X1),X2)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ one_sorted_str(X0)
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ one_sorted_str(X1) ),
inference(forward_subsumption_resolution,[],[f337,f241]) ).
fof(f341,plain,
( strict_net_str(sF34,sK31)
| ~ transitive_relstr(sK32)
| ~ one_sorted_str(sK31)
| ~ net_str(sK32,sK31) ),
inference(superposition,[],[f245,f318]) ).
fof(f342,plain,
( strict_net_str(sF34,sK31)
| ~ one_sorted_str(sK31)
| ~ net_str(sK32,sK31) ),
inference(forward_subsumption_resolution,[],[f341,f304]) ).
fof(f343,plain,
( strict_net_str(sF34,sK31)
| ~ net_str(sK32,sK31) ),
inference(forward_subsumption_resolution,[],[f342,f306]) ).
fof(f344,plain,
strict_net_str(sF34,sK31),
inference(forward_subsumption_resolution,[],[f343,f302]) ).
fof(f345,plain,
( ~ one_sorted_str(sK31)
| rel_str(sK32) ),
inference(resolution,[],[f222,f302]) ).
fof(f346,plain,
rel_str(sK32),
inference(forward_subsumption_resolution,[],[f345,f306]) ).
fof(f361,plain,
( subnetstr(sF34,sK31,sK32)
| ~ one_sorted_str(sK31)
| ~ net_str(sK32,sK31) ),
inference(superposition,[],[f219,f318]) ).
fof(f362,plain,
( subnetstr(sF34,sK31,sK32)
| ~ net_str(sK32,sK31) ),
inference(forward_subsumption_resolution,[],[f361,f306]) ).
fof(f363,plain,
subnetstr(sF34,sK31,sK32),
inference(forward_subsumption_resolution,[],[f362,f302]) ).
fof(f364,plain,
( full_subnetstr(sF34,sK31,sK32)
| ~ transitive_relstr(sK32)
| ~ one_sorted_str(sK31)
| ~ net_str(sK32,sK31) ),
inference(superposition,[],[f244,f318]) ).
fof(f365,plain,
( full_subnetstr(sF34,sK31,sK32)
| ~ one_sorted_str(sK31)
| ~ net_str(sK32,sK31) ),
inference(forward_subsumption_resolution,[],[f364,f304]) ).
fof(f366,plain,
( full_subnetstr(sF34,sK31,sK32)
| ~ net_str(sK32,sK31) ),
inference(forward_subsumption_resolution,[],[f365,f306]) ).
fof(f367,plain,
full_subnetstr(sF34,sK31,sK32),
inference(forward_subsumption_resolution,[],[f366,f302]) ).
fof(f378,plain,
! [X0] :
( sF34 != X0
| ~ net_str(sK32,sK31)
| ~ subnetstr(X0,sK31,sK32)
| ~ strict_net_str(X0,sK31)
| the_carrier(X0) = function_invverse_img_as_carrier_subset(sK32,sK31,the_mapping(sK31,sK32),sK33)
| ~ one_sorted_str(sK31) ),
inference(superposition,[],[f194,f318]) ).
fof(f381,plain,
! [X0] :
( sF34 != X0
| ~ subnetstr(X0,sK31,sK32)
| ~ strict_net_str(X0,sK31)
| the_carrier(X0) = function_invverse_img_as_carrier_subset(sK32,sK31,the_mapping(sK31,sK32),sK33)
| ~ one_sorted_str(sK31) ),
inference(forward_subsumption_resolution,[],[f378,f302]) ).
fof(f383,plain,
! [X0] :
( sF34 != X0
| ~ subnetstr(X0,sK31,sK32)
| ~ strict_net_str(X0,sK31)
| the_carrier(X0) = function_invverse_img_as_carrier_subset(sK32,sK31,the_mapping(sK31,sK32),sK33) ),
inference(forward_subsumption_resolution,[],[f381,f306]) ).
fof(f394,plain,
! [X2,X3,X0,X1] :
( in(sK1(X0,X1,X2,X3),the_carrier(X1))
| empty(the_carrier(X1))
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X3,the_carrier(X1))
| ~ one_sorted_str(X0)
| ~ is_often_in(X0,X1,X2) ),
inference(resolution,[],[f299,f192]) ).
fof(f400,plain,
! [X2,X3,X0,X1,X4,X5] :
( X3 != X5
| empty_carrier(X0)
| ~ subnetstr(X2,X1,X0)
| ~ full_subnetstr(X2,X1,X0)
| empty_carrier(X2)
| ~ element(X3,the_carrier(X0))
| ~ element(X4,the_carrier(X0))
| ~ element(X5,the_carrier(X2))
| ~ element(X4,the_carrier(X2))
| ~ related(X0,X3,X4)
| ~ one_sorted_str(X1)
| ~ net_str(X0,X1)
| related(X2,X5,X4) ),
inference(equality_resolution,[],[f298]) ).
fof(f401,plain,
! [X2,X3,X0,X1,X4] :
( ~ full_subnetstr(X1,X2,X0)
| ~ subnetstr(X1,X2,X0)
| empty_carrier(X0)
| empty_carrier(X1)
| ~ element(X3,the_carrier(X0))
| ~ element(X4,the_carrier(X0))
| ~ element(X3,the_carrier(X1))
| ~ element(X4,the_carrier(X1))
| ~ related(X0,X3,X4)
| ~ one_sorted_str(X2)
| ~ net_str(X0,X2)
| related(X1,X3,X4) ),
inference(equality_resolution,[],[f400]) ).
fof(f413,plain,
! [X0,X1] :
( ~ subnetstr(sF34,sK31,sK32)
| empty_carrier(sK32)
| empty_carrier(sF34)
| ~ element(X0,the_carrier(sK32))
| ~ element(X1,the_carrier(sK32))
| ~ element(X0,the_carrier(sF34))
| ~ element(X1,the_carrier(sF34))
| ~ related(sK32,X0,X1)
| ~ one_sorted_str(sK31)
| ~ net_str(sK32,sK31)
| related(sF34,X0,X1) ),
inference(resolution,[],[f401,f367]) ).
fof(f415,plain,
! [X0,X1] :
( empty_carrier(sK32)
| empty_carrier(sF34)
| ~ element(X0,the_carrier(sK32))
| ~ element(X1,the_carrier(sK32))
| ~ element(X0,the_carrier(sF34))
| ~ element(X1,the_carrier(sF34))
| ~ related(sK32,X0,X1)
| ~ one_sorted_str(sK31)
| ~ net_str(sK32,sK31)
| related(sF34,X0,X1) ),
inference(forward_subsumption_resolution,[],[f413,f363]) ).
fof(f417,plain,
! [X0,X1] :
( empty_carrier(sF34)
| ~ element(X0,the_carrier(sK32))
| ~ element(X1,the_carrier(sK32))
| ~ element(X0,the_carrier(sF34))
| ~ element(X1,the_carrier(sF34))
| ~ related(sK32,X0,X1)
| ~ one_sorted_str(sK31)
| ~ net_str(sK32,sK31)
| related(sF34,X0,X1) ),
inference(forward_subsumption_resolution,[],[f415,f305]) ).
fof(f418,plain,
! [X0,X1] :
( empty_carrier(sF34)
| ~ element(X0,the_carrier(sK32))
| ~ element(X1,the_carrier(sK32))
| ~ element(X0,the_carrier(sF34))
| ~ element(X1,the_carrier(sF34))
| ~ related(sK32,X0,X1)
| ~ net_str(sK32,sK31)
| related(sF34,X0,X1) ),
inference(forward_subsumption_resolution,[],[f417,f306]) ).
fof(f419,plain,
! [X0,X1] :
( empty_carrier(sF34)
| ~ element(X0,the_carrier(sK32))
| ~ element(X1,the_carrier(sK32))
| ~ element(X0,the_carrier(sF34))
| ~ element(X1,the_carrier(sF34))
| ~ related(sK32,X0,X1)
| related(sF34,X0,X1) ),
inference(forward_subsumption_resolution,[],[f418,f302]) ).
fof(f421,definition,
( spl35_3
<=> ! [X0,X1] :
( ~ element(X0,the_carrier(sK32))
| related(sF34,X0,X1)
| ~ related(sK32,X0,X1)
| ~ element(X0,the_carrier(sF34))
| ~ element(X1,the_carrier(sK32))
| ~ element(X1,the_carrier(sF34)) ) ),
introduced(definition,[new_symbols(definition,[spl35_3])],[avatar_definition]) ).
fof(f422,plain,
( ! [X0,X1] :
( ~ related(sK32,X0,X1)
| related(sF34,X0,X1)
| ~ element(X0,the_carrier(sK32))
| ~ element(X0,the_carrier(sF34))
| ~ element(X1,the_carrier(sK32))
| ~ element(X1,the_carrier(sF34)) )
| ~ spl35_3 ),
inference(avatar_component_clause,[],[f421]) ).
fof(f423,plain,
( spl35_3
| spl35_1 ),
inference(avatar_split_clause,[],[f419,f321,f421]) ).
fof(f425,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,[],[f227,f294]) ).
fof(f426,plain,
one_sorted_str(sK32),
inference(resolution,[],[f221,f346]) ).
fof(f427,plain,
! [X2,X3,X0,X1,X4] :
( ~ element(X0,the_carrier(X1))
| ~ element(X2,the_carrier(X1))
| ~ element(sK1(X3,X1,X4,X2),the_carrier(X1))
| ~ rel_str(X1)
| ~ related(X1,X0,X2)
| related(X1,X0,sK1(X3,X1,X4,X2))
| ~ transitive_relstr(X1)
| empty_carrier(X3)
| ~ net_str(X1,X3)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ one_sorted_str(X3)
| ~ is_often_in(X3,X1,X4) ),
inference(resolution,[],[f200,f191]) ).
fof(f432,plain,
! [X2,X3,X0,X1,X4] :
( ~ element(X0,the_carrier(X1))
| ~ element(X2,the_carrier(X1))
| ~ element(sK1(X3,X1,X4,X2),the_carrier(X1))
| ~ rel_str(X1)
| ~ related(X1,X0,X2)
| related(X1,X0,sK1(X3,X1,X4,X2))
| ~ transitive_relstr(X1)
| empty_carrier(X3)
| ~ net_str(X1,X3)
| empty_carrier(X1)
| ~ one_sorted_str(X3)
| ~ is_often_in(X3,X1,X4) ),
inference(duplicate_literal_removal,[],[f427]) ).
fof(f435,plain,
! [X2,X3,X0,X1,X4] :
( ~ element(X0,the_carrier(X1))
| ~ element(X2,the_carrier(X1))
| ~ rel_str(X1)
| ~ related(X1,X0,X2)
| related(X1,X0,sK1(X3,X1,X4,X2))
| ~ transitive_relstr(X1)
| empty_carrier(X3)
| ~ net_str(X1,X3)
| empty_carrier(X1)
| ~ one_sorted_str(X3)
| ~ is_often_in(X3,X1,X4) ),
inference(forward_subsumption_resolution,[],[f432,f192]) ).
fof(f436,plain,
! [X2,X3,X0,X1,X4] :
( related(X1,X0,sK1(X3,X1,X4,X2))
| ~ element(X2,the_carrier(X1))
| ~ related(X1,X0,X2)
| ~ element(X0,the_carrier(X1))
| ~ transitive_relstr(X1)
| empty_carrier(X3)
| ~ net_str(X1,X3)
| empty_carrier(X1)
| ~ one_sorted_str(X3)
| ~ is_often_in(X3,X1,X4) ),
inference(forward_subsumption_resolution,[],[f435,f222]) ).
fof(f447,definition,
( spl35_5
<=> ! [X0] : ~ element(X0,the_carrier(sK32)) ),
introduced(definition,[new_symbols(definition,[spl35_5])],[avatar_definition]) ).
fof(f448,plain,
( ! [X0] : ~ element(X0,the_carrier(sK32))
| ~ spl35_5 ),
inference(avatar_component_clause,[],[f447]) ).
fof(f458,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ in(apply_netmap(X0,X1,X2),X3)
| ~ quasi_total(the_mapping(X0,X1),X4,X5)
| ~ function(the_mapping(X0,X1))
| empty_set = X5
| ~ relation_of2_as_subset(the_mapping(X0,X1),X4,X5)
| ~ in(X2,X4)
| in(X2,relation_inverse_image(the_mapping(X0,X1),X3))
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ one_sorted_str(X0)
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ one_sorted_str(X1) ),
inference(superposition,[],[f311,f339]) ).
fof(f459,plain,
! [X2,X3,X0,X1,X4,X5] :
( ~ in(apply_netmap(X0,X1,X2),X3)
| ~ quasi_total(the_mapping(X0,X1),X4,X5)
| empty_set = X5
| ~ relation_of2_as_subset(the_mapping(X0,X1),X4,X5)
| ~ in(X2,X4)
| in(X2,relation_inverse_image(the_mapping(X0,X1),X3))
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ one_sorted_str(X0)
| ~ relation_of2(the_mapping(X0,X1),the_carrier(X1),the_carrier(X0))
| ~ one_sorted_str(X1) ),
inference(forward_subsumption_resolution,[],[f458,f241]) ).
fof(f460,plain,
! [X2,X3,X0,X1,X4,X5] :
( in(X2,relation_inverse_image(the_mapping(X0,X1),X3))
| ~ quasi_total(the_mapping(X0,X1),X4,X5)
| empty_set = X5
| ~ relation_of2_as_subset(the_mapping(X0,X1),X4,X5)
| ~ in(X2,X4)
| ~ in(apply_netmap(X0,X1,X2),X3)
| empty_carrier(X0)
| ~ net_str(X1,X0)
| empty_carrier(X1)
| ~ element(X2,the_carrier(X1))
| ~ one_sorted_str(X0)
| ~ one_sorted_str(X1) ),
inference(forward_subsumption_resolution,[],[f459,f425]) ).
fof(f478,plain,
( ~ subnetstr(sF34,sK31,sK32)
| ~ strict_net_str(sF34,sK31)
| function_invverse_img_as_carrier_subset(sK32,sK31,the_mapping(sK31,sK32),sK33) = the_carrier(sF34) ),
inference(equality_resolution,[],[f383]) ).
fof(f479,plain,
( ~ strict_net_str(sF34,sK31)
| function_invverse_img_as_carrier_subset(sK32,sK31,the_mapping(sK31,sK32),sK33) = the_carrier(sF34) ),
inference(forward_subsumption_resolution,[],[f478,f363]) ).
fof(f480,plain,
function_invverse_img_as_carrier_subset(sK32,sK31,the_mapping(sK31,sK32),sK33) = the_carrier(sF34),
inference(forward_subsumption_resolution,[],[f479,f344]) ).
fof(f485,plain,
( the_carrier(sF34) = relation_inverse_image(the_mapping(sK31,sK32),sK33)
| ~ quasi_total(the_mapping(sK31,sK32),the_carrier(sK32),the_carrier(sK31))
| ~ function(the_mapping(sK31,sK32))
| ~ one_sorted_str(sK31)
| ~ one_sorted_str(sK32)
| ~ relation_of2(the_mapping(sK31,sK32),the_carrier(sK32),the_carrier(sK31)) ),
inference(superposition,[],[f292,f480]) ).
fof(f486,plain,
( the_carrier(sF34) = relation_inverse_image(the_mapping(sK31,sK32),sK33)
| ~ quasi_total(the_mapping(sK31,sK32),the_carrier(sK32),the_carrier(sK31))
| ~ function(the_mapping(sK31,sK32))
| ~ one_sorted_str(sK32)
| ~ relation_of2(the_mapping(sK31,sK32),the_carrier(sK32),the_carrier(sK31)) ),
inference(forward_subsumption_resolution,[],[f485,f306]) ).
fof(f490,plain,
( the_carrier(sF34) = relation_inverse_image(the_mapping(sK31,sK32),sK33)
| ~ quasi_total(the_mapping(sK31,sK32),the_carrier(sK32),the_carrier(sK31))
| ~ function(the_mapping(sK31,sK32))
| ~ relation_of2(the_mapping(sK31,sK32),the_carrier(sK32),the_carrier(sK31)) ),
inference(forward_subsumption_resolution,[],[f486,f426]) ).
fof(f514,plain,
! [X0] :
( in(sK5(X0),the_carrier(X0))
| ~ rel_str(X0)
| directed_relstr(X0)
| empty_carrier(X0)
| empty(the_carrier(X0)) ),
inference(resolution,[],[f212,f299]) ).
fof(f515,plain,
! [X0] :
( in(sK6(X0),the_carrier(X0))
| ~ rel_str(X0)
| directed_relstr(X0)
| empty_carrier(X0)
| empty(the_carrier(X0)) ),
inference(resolution,[],[f211,f299]) ).
fof(f571,definition,
( spl35_6
<=> relation_of2(the_mapping(sK31,sK32),the_carrier(sK32),the_carrier(sK31)) ),
introduced(definition,[new_symbols(definition,[spl35_6])],[avatar_definition]) ).
fof(f572,plain,
( relation_of2(the_mapping(sK31,sK32),the_carrier(sK32),the_carrier(sK31))
| ~ spl35_6 ),
inference(avatar_component_clause,[],[f571]) ).
fof(f573,plain,
( ~ relation_of2(the_mapping(sK31,sK32),the_carrier(sK32),the_carrier(sK31))
| spl35_6 ),
inference(avatar_component_clause,[],[f571]) ).
fof(f575,definition,
( spl35_7
<=> function(the_mapping(sK31,sK32)) ),
introduced(definition,[new_symbols(definition,[spl35_7])],[avatar_definition]) ).
fof(f576,plain,
( function(the_mapping(sK31,sK32))
| ~ spl35_7 ),
inference(avatar_component_clause,[],[f575]) ).
fof(f577,plain,
( ~ function(the_mapping(sK31,sK32))
| spl35_7 ),
inference(avatar_component_clause,[],[f575]) ).
fof(f579,definition,
( spl35_8
<=> quasi_total(the_mapping(sK31,sK32),the_carrier(sK32),the_carrier(sK31)) ),
introduced(definition,[new_symbols(definition,[spl35_8])],[avatar_definition]) ).
fof(f580,plain,
( quasi_total(the_mapping(sK31,sK32),the_carrier(sK32),the_carrier(sK31))
| ~ spl35_8 ),
inference(avatar_component_clause,[],[f579]) ).
fof(f581,plain,
( ~ quasi_total(the_mapping(sK31,sK32),the_carrier(sK32),the_carrier(sK31))
| spl35_8 ),
inference(avatar_component_clause,[],[f579]) ).
fof(f583,definition,
( spl35_9
<=> the_carrier(sF34) = relation_inverse_image(the_mapping(sK31,sK32),sK33) ),
introduced(definition,[new_symbols(definition,[spl35_9])],[avatar_definition]) ).
fof(f585,plain,
( the_carrier(sF34) = relation_inverse_image(the_mapping(sK31,sK32),sK33)
| ~ spl35_9 ),
inference(avatar_component_clause,[],[f583]) ).
fof(f586,plain,
( ~ spl35_6
| ~ spl35_7
| ~ spl35_8
| spl35_9 ),
inference(avatar_split_clause,[],[f490,f583,f579,f575,f571]) ).
fof(f587,plain,
( ~ net_str(sK32,sK31)
| ~ one_sorted_str(sK31)
| spl35_6 ),
inference(resolution,[],[f573,f425]) ).
fof(f588,plain,
( ~ one_sorted_str(sK31)
| spl35_6 ),
inference(forward_subsumption_resolution,[],[f587,f302]) ).
fof(f589,plain,
( $false
| spl35_6 ),
inference(forward_subsumption_resolution,[],[f588,f306]) ).
fof(f590,plain,
spl35_6,
inference(avatar_contradiction_clause,[],[f589]) ).
fof(f592,plain,
( empty_carrier(sK32)
| ~ one_sorted_str(sK31)
| empty_carrier(sK31)
| ~ net_str(sK32,sK31)
| spl35_7 ),
inference(resolution,[],[f577,f241]) ).
fof(f593,plain,
( ~ one_sorted_str(sK31)
| empty_carrier(sK31)
| ~ net_str(sK32,sK31)
| spl35_7 ),
inference(forward_subsumption_resolution,[],[f592,f305]) ).
fof(f595,plain,
( empty_carrier(sK31)
| ~ net_str(sK32,sK31)
| spl35_7 ),
inference(forward_subsumption_resolution,[],[f593,f306]) ).
fof(f598,plain,
( ~ net_str(sK32,sK31)
| spl35_7 ),
inference(forward_subsumption_resolution,[],[f595,f307]) ).
fof(f599,plain,
( $false
| spl35_7 ),
inference(forward_subsumption_resolution,[],[f598,f302]) ).
fof(f600,plain,
spl35_7,
inference(avatar_contradiction_clause,[],[f599]) ).
fof(f602,plain,
( empty_carrier(sK32)
| ~ one_sorted_str(sK31)
| empty_carrier(sK31)
| ~ net_str(sK32,sK31)
| spl35_8 ),
inference(resolution,[],[f581,f240]) ).
fof(f603,plain,
( ~ one_sorted_str(sK31)
| empty_carrier(sK31)
| ~ net_str(sK32,sK31)
| spl35_8 ),
inference(forward_subsumption_resolution,[],[f602,f305]) ).
fof(f605,plain,
( empty_carrier(sK31)
| ~ net_str(sK32,sK31)
| spl35_8 ),
inference(forward_subsumption_resolution,[],[f603,f306]) ).
fof(f608,plain,
( ~ net_str(sK32,sK31)
| spl35_8 ),
inference(forward_subsumption_resolution,[],[f605,f307]) ).
fof(f609,plain,
( $false
| spl35_8 ),
inference(forward_subsumption_resolution,[],[f608,f302]) ).
fof(f610,plain,
spl35_8,
inference(avatar_contradiction_clause,[],[f609]) ).
fof(f614,plain,
( ! [X2,X0,X1] :
( ~ in(X0,the_carrier(sF34))
| ~ quasi_total(the_mapping(sK31,sK32),X1,X2)
| ~ function(the_mapping(sK31,sK32))
| empty_set = X2
| in(X0,X1)
| ~ relation_of2_as_subset(the_mapping(sK31,sK32),X1,X2) )
| ~ spl35_9 ),
inference(superposition,[],[f310,f585]) ).
fof(f617,plain,
( ! [X2,X0,X1] :
( ~ relation_of2_as_subset(the_mapping(sK31,sK32),X1,X2)
| ~ quasi_total(the_mapping(sK31,sK32),X1,X2)
| empty_set = X2
| in(X0,X1)
| ~ in(X0,the_carrier(sF34)) )
| ~ spl35_7
| ~ spl35_9 ),
inference(forward_subsumption_resolution,[],[f614,f576]) ).
fof(f630,plain,
( relation_of2_as_subset(the_mapping(sK31,sK32),the_carrier(sK32),the_carrier(sK31))
| ~ spl35_6 ),
inference(resolution,[],[f572,f293]) ).
fof(f638,plain,
( ! [X0] :
( ~ quasi_total(the_mapping(sK31,sK32),the_carrier(sK32),the_carrier(sK31))
| empty_set = the_carrier(sK31)
| in(X0,the_carrier(sK32))
| ~ in(X0,the_carrier(sF34))
| ~ one_sorted_str(sK31)
| ~ net_str(sK32,sK31) )
| ~ spl35_7
| ~ spl35_9 ),
inference(resolution,[],[f617,f227]) ).
fof(f639,plain,
( ! [X0] :
( empty_set = the_carrier(sK31)
| in(X0,the_carrier(sK32))
| ~ in(X0,the_carrier(sF34))
| ~ one_sorted_str(sK31)
| ~ net_str(sK32,sK31) )
| ~ spl35_7
| ~ spl35_9 ),
inference(forward_subsumption_resolution,[],[f638,f228]) ).
fof(f640,plain,
( ! [X0] :
( empty_set = the_carrier(sK31)
| in(X0,the_carrier(sK32))
| ~ in(X0,the_carrier(sF34))
| ~ net_str(sK32,sK31) )
| ~ spl35_7
| ~ spl35_9 ),
inference(forward_subsumption_resolution,[],[f639,f306]) ).
fof(f641,plain,
( ! [X0] :
( empty_set = the_carrier(sK31)
| in(X0,the_carrier(sK32))
| ~ in(X0,the_carrier(sF34)) )
| ~ spl35_7
| ~ spl35_9 ),
inference(forward_subsumption_resolution,[],[f640,f302]) ).
fof(f643,definition,
( spl35_10
<=> ! [X0] :
( in(X0,the_carrier(sK32))
| ~ in(X0,the_carrier(sF34)) ) ),
introduced(definition,[new_symbols(definition,[spl35_10])],[avatar_definition]) ).
fof(f644,plain,
( ! [X0] :
( ~ in(X0,the_carrier(sF34))
| in(X0,the_carrier(sK32)) )
| ~ spl35_10 ),
inference(avatar_component_clause,[],[f643]) ).
fof(f646,definition,
( spl35_11
<=> empty_set = the_carrier(sK31) ),
introduced(definition,[new_symbols(definition,[spl35_11])],[avatar_definition]) ).
fof(f647,plain,
( empty_set != the_carrier(sK31)
| spl35_11 ),
inference(avatar_component_clause,[],[f646]) ).
fof(f648,plain,
( empty_set = the_carrier(sK31)
| ~ spl35_11 ),
inference(avatar_component_clause,[],[f646]) ).
fof(f649,plain,
( spl35_10
| spl35_11
| ~ spl35_7
| ~ spl35_9 ),
inference(avatar_split_clause,[],[f641,f583,f575,f646,f643]) ).
fof(f662,plain,
( ~ one_sorted_str(sK31)
| ~ net_str(sK32,sK31)
| net_str(sF34,sK31) ),
inference(resolution,[],[f224,f363]) ).
fof(f666,plain,
( ~ net_str(sK32,sK31)
| net_str(sF34,sK31) ),
inference(forward_subsumption_resolution,[],[f662,f306]) ).
fof(f667,plain,
net_str(sF34,sK31),
inference(forward_subsumption_resolution,[],[f666,f302]) ).
fof(f668,plain,
( ~ one_sorted_str(sK31)
| rel_str(sF34) ),
inference(resolution,[],[f667,f222]) ).
fof(f669,plain,
rel_str(sF34),
inference(forward_subsumption_resolution,[],[f668,f306]) ).
fof(f670,plain,
one_sorted_str(sF34),
inference(resolution,[],[f669,f221]) ).
fof(f724,plain,
( ~ empty(empty_set)
| empty_carrier(sK31)
| ~ one_sorted_str(sK31)
| ~ spl35_11 ),
inference(superposition,[],[f247,f648]) ).
fof(f739,plain,
( empty_carrier(sK31)
| ~ one_sorted_str(sK31)
| ~ spl35_11 ),
inference(forward_subsumption_resolution,[],[f724,f250]) ).
fof(f754,plain,
( ~ one_sorted_str(sK31)
| ~ spl35_11 ),
inference(forward_subsumption_resolution,[],[f739,f307]) ).
fof(f758,plain,
( $false
| ~ spl35_11 ),
inference(forward_subsumption_resolution,[],[f754,f306]) ).
fof(f759,plain,
~ spl35_11,
inference(avatar_contradiction_clause,[],[f758]) ).
fof(f816,plain,
! [X0,X1] :
( ~ empty_carrier(X0)
| ~ quasi_total(the_mapping(X1,X0),the_carrier(X0),the_carrier(X1))
| ~ function(the_mapping(X1,X0))
| ~ relation_of2(the_InternalRel(X0),the_carrier(X0),the_carrier(X0))
| empty(the_carrier(X0))
| ~ one_sorted_str(X1)
| ~ relation_of2(the_mapping(X1,X0),the_carrier(X0),the_carrier(X1))
| ~ one_sorted_str(X1)
| ~ strict_net_str(X0,X1)
| ~ net_str(X0,X1) ),
inference(superposition,[],[f253,f183]) ).
fof(f817,plain,
! [X0,X1] :
( ~ empty_carrier(X0)
| ~ quasi_total(the_mapping(X1,X0),the_carrier(X0),the_carrier(X1))
| ~ function(the_mapping(X1,X0))
| ~ relation_of2(the_InternalRel(X0),the_carrier(X0),the_carrier(X0))
| empty(the_carrier(X0))
| ~ one_sorted_str(X1)
| ~ relation_of2(the_mapping(X1,X0),the_carrier(X0),the_carrier(X1))
| ~ strict_net_str(X0,X1)
| ~ net_str(X0,X1) ),
inference(duplicate_literal_removal,[],[f816]) ).
fof(f818,plain,
! [X0,X1] :
( ~ empty_carrier(X0)
| ~ function(the_mapping(X1,X0))
| ~ relation_of2(the_InternalRel(X0),the_carrier(X0),the_carrier(X0))
| empty(the_carrier(X0))
| ~ one_sorted_str(X1)
| ~ relation_of2(the_mapping(X1,X0),the_carrier(X0),the_carrier(X1))
| ~ strict_net_str(X0,X1)
| ~ net_str(X0,X1) ),
inference(forward_subsumption_resolution,[],[f817,f228]) ).
fof(f819,plain,
! [X0,X1] :
( ~ empty_carrier(X0)
| ~ relation_of2(the_InternalRel(X0),the_carrier(X0),the_carrier(X0))
| empty(the_carrier(X0))
| ~ one_sorted_str(X1)
| ~ relation_of2(the_mapping(X1,X0),the_carrier(X0),the_carrier(X1))
| ~ strict_net_str(X0,X1)
| ~ net_str(X0,X1) ),
inference(forward_subsumption_resolution,[],[f818,f229]) ).
fof(f820,plain,
! [X0,X1] :
( ~ relation_of2(the_InternalRel(X0),the_carrier(X0),the_carrier(X0))
| ~ empty_carrier(X0)
| empty(the_carrier(X0))
| ~ one_sorted_str(X1)
| ~ strict_net_str(X0,X1)
| ~ net_str(X0,X1) ),
inference(forward_subsumption_resolution,[],[f819,f425]) ).
fof(f830,definition,
( spl35_15
<=> empty(the_carrier(sK32)) ),
introduced(definition,[new_symbols(definition,[spl35_15])],[avatar_definition]) ).
fof(f831,plain,
( empty(the_carrier(sK32))
| ~ spl35_15 ),
inference(avatar_component_clause,[],[f830]) ).
fof(f832,plain,
( ~ empty(the_carrier(sK32))
| spl35_15 ),
inference(avatar_component_clause,[],[f830]) ).
fof(f836,plain,
! [X0] :
( relation_of2(the_InternalRel(X0),the_carrier(X0),the_carrier(X0))
| ~ rel_str(X0) ),
inference(resolution,[],[f226,f294]) ).
fof(f842,plain,
! [X0,X1] :
( ~ empty_carrier(X0)
| empty(the_carrier(X0))
| ~ one_sorted_str(X1)
| ~ strict_net_str(X0,X1)
| ~ net_str(X0,X1)
| ~ rel_str(X0) ),
inference(resolution,[],[f820,f836]) ).
fof(f843,plain,
! [X0,X1] :
( ~ strict_net_str(X0,X1)
| empty(the_carrier(X0))
| ~ one_sorted_str(X1)
| ~ empty_carrier(X0)
| ~ net_str(X0,X1) ),
inference(forward_subsumption_resolution,[],[f842,f222]) ).
fof(f1030,plain,
( ! [X2,X0,X1] :
( in(X0,the_carrier(sF34))
| ~ quasi_total(the_mapping(sK31,sK32),X1,X2)
| empty_set = X2
| ~ relation_of2_as_subset(the_mapping(sK31,sK32),X1,X2)
| ~ in(X0,X1)
| ~ in(apply_netmap(sK31,sK32,X0),sK33)
| empty_carrier(sK31)
| ~ net_str(sK32,sK31)
| empty_carrier(sK32)
| ~ element(X0,the_carrier(sK32))
| ~ one_sorted_str(sK31)
| ~ one_sorted_str(sK32) )
| ~ spl35_9 ),
inference(superposition,[],[f460,f585]) ).
fof(f1034,plain,
( ! [X2,X0,X1] :
( in(X0,the_carrier(sF34))
| ~ quasi_total(the_mapping(sK31,sK32),X1,X2)
| empty_set = X2
| ~ relation_of2_as_subset(the_mapping(sK31,sK32),X1,X2)
| ~ in(X0,X1)
| ~ in(apply_netmap(sK31,sK32,X0),sK33)
| ~ net_str(sK32,sK31)
| empty_carrier(sK32)
| ~ element(X0,the_carrier(sK32))
| ~ one_sorted_str(sK31)
| ~ one_sorted_str(sK32) )
| ~ spl35_9 ),
inference(forward_subsumption_resolution,[],[f1030,f307]) ).
fof(f1038,plain,
( ! [X2,X0,X1] :
( in(X0,the_carrier(sF34))
| ~ quasi_total(the_mapping(sK31,sK32),X1,X2)
| empty_set = X2
| ~ relation_of2_as_subset(the_mapping(sK31,sK32),X1,X2)
| ~ in(X0,X1)
| ~ in(apply_netmap(sK31,sK32,X0),sK33)
| empty_carrier(sK32)
| ~ element(X0,the_carrier(sK32))
| ~ one_sorted_str(sK31)
| ~ one_sorted_str(sK32) )
| ~ spl35_9 ),
inference(forward_subsumption_resolution,[],[f1034,f302]) ).
fof(f1039,plain,
( ! [X2,X0,X1] :
( in(X0,the_carrier(sF34))
| ~ quasi_total(the_mapping(sK31,sK32),X1,X2)
| empty_set = X2
| ~ relation_of2_as_subset(the_mapping(sK31,sK32),X1,X2)
| ~ in(X0,X1)
| ~ in(apply_netmap(sK31,sK32,X0),sK33)
| ~ element(X0,the_carrier(sK32))
| ~ one_sorted_str(sK31)
| ~ one_sorted_str(sK32) )
| ~ spl35_9 ),
inference(forward_subsumption_resolution,[],[f1038,f305]) ).
fof(f1040,plain,
( ! [X2,X0,X1] :
( in(X0,the_carrier(sF34))
| ~ quasi_total(the_mapping(sK31,sK32),X1,X2)
| empty_set = X2
| ~ relation_of2_as_subset(the_mapping(sK31,sK32),X1,X2)
| ~ in(X0,X1)
| ~ in(apply_netmap(sK31,sK32,X0),sK33)
| ~ element(X0,the_carrier(sK32))
| ~ one_sorted_str(sK32) )
| ~ spl35_9 ),
inference(forward_subsumption_resolution,[],[f1039,f306]) ).
fof(f1041,plain,
( ! [X2,X0,X1] :
( ~ relation_of2_as_subset(the_mapping(sK31,sK32),X1,X2)
| ~ quasi_total(the_mapping(sK31,sK32),X1,X2)
| empty_set = X2
| in(X0,the_carrier(sF34))
| ~ in(X0,X1)
| ~ in(apply_netmap(sK31,sK32,X0),sK33)
| ~ element(X0,the_carrier(sK32)) )
| ~ spl35_9 ),
inference(forward_subsumption_resolution,[],[f1040,f426]) ).
fof(f1061,plain,
( empty(the_carrier(sF34))
| ~ one_sorted_str(sK31)
| ~ empty_carrier(sF34)
| ~ net_str(sF34,sK31) ),
inference(resolution,[],[f843,f344]) ).
fof(f1068,plain,
( empty(the_carrier(sF34))
| ~ empty_carrier(sF34)
| ~ net_str(sF34,sK31) ),
inference(forward_subsumption_resolution,[],[f1061,f306]) ).
fof(f1073,plain,
( empty(the_carrier(sF34))
| ~ net_str(sF34,sK31)
| ~ spl35_1 ),
inference(forward_subsumption_resolution,[],[f1068,f323]) ).
fof(f1074,plain,
( empty(the_carrier(sF34))
| ~ spl35_1 ),
inference(forward_subsumption_resolution,[],[f1073,f667]) ).
fof(f1229,plain,
( ~ rel_str(sF34)
| directed_relstr(sF34)
| empty_carrier(sF34)
| empty(the_carrier(sF34))
| in(sK5(sF34),the_carrier(sK32))
| ~ spl35_10 ),
inference(resolution,[],[f514,f644]) ).
fof(f1257,plain,
( ~ rel_str(sF34)
| directed_relstr(sF34)
| empty_carrier(sF34)
| empty(the_carrier(sF34))
| in(sK6(sF34),the_carrier(sK32))
| ~ spl35_10 ),
inference(resolution,[],[f515,f644]) ).
fof(f1318,plain,
( ! [X0] :
( ~ quasi_total(the_mapping(sK31,sK32),the_carrier(sK32),the_carrier(sK31))
| empty_set = the_carrier(sK31)
| in(X0,the_carrier(sF34))
| ~ in(X0,the_carrier(sK32))
| ~ in(apply_netmap(sK31,sK32,X0),sK33)
| ~ element(X0,the_carrier(sK32)) )
| ~ spl35_6
| ~ spl35_9 ),
inference(resolution,[],[f1041,f630]) ).
fof(f1321,plain,
( ! [X0] :
( empty_set = the_carrier(sK31)
| in(X0,the_carrier(sF34))
| ~ in(X0,the_carrier(sK32))
| ~ in(apply_netmap(sK31,sK32,X0),sK33)
| ~ element(X0,the_carrier(sK32)) )
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9 ),
inference(forward_subsumption_resolution,[],[f1318,f580]) ).
fof(f1323,plain,
( ! [X0] :
( in(X0,the_carrier(sF34))
| ~ in(X0,the_carrier(sK32))
| ~ in(apply_netmap(sK31,sK32,X0),sK33)
| ~ element(X0,the_carrier(sK32)) )
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11 ),
inference(forward_subsumption_resolution,[],[f1321,f647]) ).
fof(f1325,plain,
( ! [X0] :
( ~ in(apply_netmap(sK31,sK32,X0),sK33)
| ~ in(X0,the_carrier(sK32))
| in(X0,the_carrier(sF34)) )
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11 ),
inference(forward_subsumption_resolution,[],[f1323,f297]) ).
fof(f1328,plain,
( ! [X0] :
( ~ in(sK1(sK31,sK32,sK33,X0),the_carrier(sK32))
| in(sK1(sK31,sK32,sK33,X0),the_carrier(sF34))
| empty_carrier(sK31)
| ~ net_str(sK32,sK31)
| empty_carrier(sK32)
| ~ element(X0,the_carrier(sK32))
| ~ one_sorted_str(sK31)
| ~ is_often_in(sK31,sK32,sK33) )
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11 ),
inference(resolution,[],[f1325,f190]) ).
fof(f1335,plain,
( ! [X0] :
( ~ in(sK1(sK31,sK32,sK33,X0),the_carrier(sK32))
| in(sK1(sK31,sK32,sK33,X0),the_carrier(sF34))
| ~ net_str(sK32,sK31)
| empty_carrier(sK32)
| ~ element(X0,the_carrier(sK32))
| ~ one_sorted_str(sK31)
| ~ is_often_in(sK31,sK32,sK33) )
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11 ),
inference(forward_subsumption_resolution,[],[f1328,f307]) ).
fof(f1339,plain,
( ! [X0] :
( ~ in(sK1(sK31,sK32,sK33,X0),the_carrier(sK32))
| in(sK1(sK31,sK32,sK33,X0),the_carrier(sF34))
| empty_carrier(sK32)
| ~ element(X0,the_carrier(sK32))
| ~ one_sorted_str(sK31)
| ~ is_often_in(sK31,sK32,sK33) )
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11 ),
inference(forward_subsumption_resolution,[],[f1335,f302]) ).
fof(f1343,plain,
( ! [X0] :
( ~ in(sK1(sK31,sK32,sK33,X0),the_carrier(sK32))
| in(sK1(sK31,sK32,sK33,X0),the_carrier(sF34))
| ~ element(X0,the_carrier(sK32))
| ~ one_sorted_str(sK31)
| ~ is_often_in(sK31,sK32,sK33) )
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11 ),
inference(forward_subsumption_resolution,[],[f1339,f305]) ).
fof(f1347,plain,
( ! [X0] :
( ~ in(sK1(sK31,sK32,sK33,X0),the_carrier(sK32))
| in(sK1(sK31,sK32,sK33,X0),the_carrier(sF34))
| ~ element(X0,the_carrier(sK32))
| ~ is_often_in(sK31,sK32,sK33) )
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11 ),
inference(forward_subsumption_resolution,[],[f1343,f306]) ).
fof(f1348,plain,
( ! [X0] :
( ~ in(sK1(sK31,sK32,sK33,X0),the_carrier(sK32))
| in(sK1(sK31,sK32,sK33,X0),the_carrier(sF34))
| ~ element(X0,the_carrier(sK32)) )
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11 ),
inference(forward_subsumption_resolution,[],[f1347,f301]) ).
fof(f1349,plain,
( ! [X0] :
( in(sK1(sK31,sK32,sK33,X0),the_carrier(sF34))
| ~ element(X0,the_carrier(sK32))
| empty(the_carrier(sK32))
| empty_carrier(sK31)
| ~ net_str(sK32,sK31)
| empty_carrier(sK32)
| ~ element(X0,the_carrier(sK32))
| ~ one_sorted_str(sK31)
| ~ is_often_in(sK31,sK32,sK33) )
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11 ),
inference(resolution,[],[f1348,f394]) ).
fof(f1350,plain,
( ! [X0] :
( in(sK1(sK31,sK32,sK33,X0),the_carrier(sF34))
| ~ element(X0,the_carrier(sK32))
| empty(the_carrier(sK32))
| empty_carrier(sK31)
| ~ net_str(sK32,sK31)
| empty_carrier(sK32)
| ~ one_sorted_str(sK31)
| ~ is_often_in(sK31,sK32,sK33) )
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11 ),
inference(duplicate_literal_removal,[],[f1349]) ).
fof(f1351,plain,
( ! [X0] :
( in(sK1(sK31,sK32,sK33,X0),the_carrier(sF34))
| ~ element(X0,the_carrier(sK32))
| empty_carrier(sK31)
| ~ net_str(sK32,sK31)
| empty_carrier(sK32)
| ~ one_sorted_str(sK31)
| ~ is_often_in(sK31,sK32,sK33) )
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15 ),
inference(forward_subsumption_resolution,[],[f1350,f832]) ).
fof(f1352,plain,
( ! [X0] :
( in(sK1(sK31,sK32,sK33,X0),the_carrier(sF34))
| ~ element(X0,the_carrier(sK32))
| ~ net_str(sK32,sK31)
| empty_carrier(sK32)
| ~ one_sorted_str(sK31)
| ~ is_often_in(sK31,sK32,sK33) )
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15 ),
inference(forward_subsumption_resolution,[],[f1351,f307]) ).
fof(f1353,plain,
( ! [X0] :
( in(sK1(sK31,sK32,sK33,X0),the_carrier(sF34))
| ~ element(X0,the_carrier(sK32))
| empty_carrier(sK32)
| ~ one_sorted_str(sK31)
| ~ is_often_in(sK31,sK32,sK33) )
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15 ),
inference(forward_subsumption_resolution,[],[f1352,f302]) ).
fof(f1354,plain,
( ! [X0] :
( in(sK1(sK31,sK32,sK33,X0),the_carrier(sF34))
| ~ element(X0,the_carrier(sK32))
| ~ one_sorted_str(sK31)
| ~ is_often_in(sK31,sK32,sK33) )
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15 ),
inference(forward_subsumption_resolution,[],[f1353,f305]) ).
fof(f1355,plain,
( ! [X0] :
( in(sK1(sK31,sK32,sK33,X0),the_carrier(sF34))
| ~ element(X0,the_carrier(sK32))
| ~ is_often_in(sK31,sK32,sK33) )
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15 ),
inference(forward_subsumption_resolution,[],[f1354,f306]) ).
fof(f1356,plain,
( ! [X0] :
( in(sK1(sK31,sK32,sK33,X0),the_carrier(sF34))
| ~ element(X0,the_carrier(sK32)) )
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15 ),
inference(forward_subsumption_resolution,[],[f1355,f301]) ).
fof(f1361,plain,
( ! [X0] :
( ~ element(X0,the_carrier(sK32))
| ~ empty(the_carrier(sF34)) )
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15 ),
inference(resolution,[],[f1356,f315]) ).
fof(f1362,plain,
( ! [X0] : ~ element(X0,the_carrier(sK32))
| ~ spl35_1
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15 ),
inference(forward_subsumption_resolution,[],[f1361,f1074]) ).
fof(f1363,plain,
( spl35_5
| ~ spl35_1
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15 ),
inference(avatar_split_clause,[],[f1362,f830,f646,f583,f579,f571,f321,f447]) ).
fof(f1373,plain,
( $false
| ~ spl35_5 ),
inference(resolution,[],[f448,f234]) ).
fof(f1375,plain,
~ spl35_5,
inference(avatar_contradiction_clause,[],[f1373]) ).
fof(f1399,plain,
( empty_carrier(sK32)
| ~ one_sorted_str(sK32)
| ~ spl35_15 ),
inference(resolution,[],[f831,f247]) ).
fof(f1402,plain,
( ~ one_sorted_str(sK32)
| ~ spl35_15 ),
inference(forward_subsumption_resolution,[],[f1399,f305]) ).
fof(f1403,plain,
( $false
| ~ spl35_15 ),
inference(forward_subsumption_resolution,[],[f1402,f426]) ).
fof(f1404,plain,
~ spl35_15,
inference(avatar_contradiction_clause,[],[f1403]) ).
fof(f1405,plain,
( ! [X0] :
( in(sK1(sK31,sK32,sK33,X0),the_carrier(sF34))
| ~ element(X0,the_carrier(sK32))
| empty_carrier(sK31)
| ~ net_str(sK32,sK31)
| empty_carrier(sK32)
| ~ one_sorted_str(sK31)
| ~ is_often_in(sK31,sK32,sK33) )
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15 ),
inference(forward_subsumption_resolution,[],[f1350,f832]) ).
fof(f1411,plain,
( directed_relstr(sF34)
| empty_carrier(sF34)
| empty(the_carrier(sF34))
| in(sK5(sF34),the_carrier(sK32))
| ~ spl35_10 ),
inference(forward_subsumption_resolution,[],[f1229,f669]) ).
fof(f1413,plain,
( directed_relstr(sF34)
| empty_carrier(sF34)
| empty(the_carrier(sF34))
| in(sK6(sF34),the_carrier(sK32))
| ~ spl35_10 ),
inference(forward_subsumption_resolution,[],[f1257,f669]) ).
fof(f1414,plain,
( ! [X0] :
( in(sK1(sK31,sK32,sK33,X0),the_carrier(sF34))
| ~ element(X0,the_carrier(sK32))
| ~ net_str(sK32,sK31)
| empty_carrier(sK32)
| ~ one_sorted_str(sK31)
| ~ is_often_in(sK31,sK32,sK33) )
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15 ),
inference(forward_subsumption_resolution,[],[f1405,f307]) ).
fof(f1415,plain,
( ! [X0] :
( in(sK1(sK31,sK32,sK33,X0),the_carrier(sF34))
| ~ element(X0,the_carrier(sK32))
| empty_carrier(sK32)
| ~ one_sorted_str(sK31)
| ~ is_often_in(sK31,sK32,sK33) )
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15 ),
inference(forward_subsumption_resolution,[],[f1414,f302]) ).
fof(f1416,plain,
( ! [X0] :
( in(sK1(sK31,sK32,sK33,X0),the_carrier(sF34))
| ~ element(X0,the_carrier(sK32))
| ~ one_sorted_str(sK31)
| ~ is_often_in(sK31,sK32,sK33) )
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15 ),
inference(forward_subsumption_resolution,[],[f1415,f305]) ).
fof(f1417,plain,
( ! [X0] :
( in(sK1(sK31,sK32,sK33,X0),the_carrier(sF34))
| ~ element(X0,the_carrier(sK32))
| ~ is_often_in(sK31,sK32,sK33) )
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15 ),
inference(forward_subsumption_resolution,[],[f1416,f306]) ).
fof(f1418,plain,
( ! [X0] :
( in(sK1(sK31,sK32,sK33,X0),the_carrier(sF34))
| ~ element(X0,the_carrier(sK32)) )
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15 ),
inference(forward_subsumption_resolution,[],[f1417,f301]) ).
fof(f1421,plain,
( ! [X2,X3,X0,X1] :
( related(sF34,X0,sK1(X1,sK32,X2,X3))
| ~ element(X0,the_carrier(sK32))
| ~ element(X0,the_carrier(sF34))
| ~ element(sK1(X1,sK32,X2,X3),the_carrier(sK32))
| ~ element(sK1(X1,sK32,X2,X3),the_carrier(sF34))
| ~ element(X3,the_carrier(sK32))
| ~ related(sK32,X0,X3)
| ~ element(X0,the_carrier(sK32))
| ~ transitive_relstr(sK32)
| empty_carrier(X1)
| ~ net_str(sK32,X1)
| empty_carrier(sK32)
| ~ one_sorted_str(X1)
| ~ is_often_in(X1,sK32,X2) )
| ~ spl35_3 ),
inference(resolution,[],[f422,f436]) ).
fof(f1432,plain,
( ! [X2,X3,X0,X1] :
( related(sF34,X0,sK1(X1,sK32,X2,X3))
| ~ element(X0,the_carrier(sK32))
| ~ element(X0,the_carrier(sF34))
| ~ element(sK1(X1,sK32,X2,X3),the_carrier(sK32))
| ~ element(sK1(X1,sK32,X2,X3),the_carrier(sF34))
| ~ element(X3,the_carrier(sK32))
| ~ related(sK32,X0,X3)
| ~ transitive_relstr(sK32)
| empty_carrier(X1)
| ~ net_str(sK32,X1)
| empty_carrier(sK32)
| ~ one_sorted_str(X1)
| ~ is_often_in(X1,sK32,X2) )
| ~ spl35_3 ),
inference(duplicate_literal_removal,[],[f1421]) ).
fof(f1439,plain,
( ! [X2,X3,X0,X1] :
( related(sF34,X0,sK1(X1,sK32,X2,X3))
| ~ element(X0,the_carrier(sK32))
| ~ element(X0,the_carrier(sF34))
| ~ element(sK1(X1,sK32,X2,X3),the_carrier(sF34))
| ~ element(X3,the_carrier(sK32))
| ~ related(sK32,X0,X3)
| ~ transitive_relstr(sK32)
| empty_carrier(X1)
| ~ net_str(sK32,X1)
| empty_carrier(sK32)
| ~ one_sorted_str(X1)
| ~ is_often_in(X1,sK32,X2) )
| ~ spl35_3 ),
inference(forward_subsumption_resolution,[],[f1432,f192]) ).
fof(f1443,plain,
( empty_carrier(sF34)
| empty(the_carrier(sF34))
| in(sK5(sF34),the_carrier(sK32))
| spl35_2
| ~ spl35_10 ),
inference(forward_subsumption_resolution,[],[f1411,f327]) ).
fof(f1445,plain,
( empty_carrier(sF34)
| empty(the_carrier(sF34))
| in(sK6(sF34),the_carrier(sK32))
| spl35_2
| ~ spl35_10 ),
inference(forward_subsumption_resolution,[],[f1413,f327]) ).
fof(f1451,plain,
( ! [X2,X3,X0,X1] :
( related(sF34,X0,sK1(X1,sK32,X2,X3))
| ~ element(X0,the_carrier(sK32))
| ~ element(X0,the_carrier(sF34))
| ~ element(sK1(X1,sK32,X2,X3),the_carrier(sF34))
| ~ element(X3,the_carrier(sK32))
| ~ related(sK32,X0,X3)
| empty_carrier(X1)
| ~ net_str(sK32,X1)
| empty_carrier(sK32)
| ~ one_sorted_str(X1)
| ~ is_often_in(X1,sK32,X2) )
| ~ spl35_3 ),
inference(forward_subsumption_resolution,[],[f1439,f304]) ).
fof(f1454,plain,
( empty(the_carrier(sF34))
| in(sK5(sF34),the_carrier(sK32))
| spl35_1
| spl35_2
| ~ spl35_10 ),
inference(forward_subsumption_resolution,[],[f1443,f322]) ).
fof(f1456,plain,
( empty(the_carrier(sF34))
| in(sK6(sF34),the_carrier(sK32))
| spl35_1
| spl35_2
| ~ spl35_10 ),
inference(forward_subsumption_resolution,[],[f1445,f322]) ).
fof(f1462,plain,
( ! [X2,X3,X0,X1] :
( ~ element(sK1(X1,sK32,X2,X3),the_carrier(sF34))
| ~ element(X0,the_carrier(sK32))
| ~ element(X0,the_carrier(sF34))
| related(sF34,X0,sK1(X1,sK32,X2,X3))
| ~ element(X3,the_carrier(sK32))
| ~ related(sK32,X0,X3)
| empty_carrier(X1)
| ~ net_str(sK32,X1)
| ~ one_sorted_str(X1)
| ~ is_often_in(X1,sK32,X2) )
| ~ spl35_3 ),
inference(forward_subsumption_resolution,[],[f1451,f305]) ).
fof(f1473,definition,
( spl35_16
<=> in(sK6(sF34),the_carrier(sK32)) ),
introduced(definition,[new_symbols(definition,[spl35_16])],[avatar_definition]) ).
fof(f1475,plain,
( in(sK6(sF34),the_carrier(sK32))
| ~ spl35_16 ),
inference(avatar_component_clause,[],[f1473]) ).
fof(f1477,definition,
( spl35_17
<=> empty(the_carrier(sF34)) ),
introduced(definition,[new_symbols(definition,[spl35_17])],[avatar_definition]) ).
fof(f1479,plain,
( empty(the_carrier(sF34))
| ~ spl35_17 ),
inference(avatar_component_clause,[],[f1477]) ).
fof(f1480,plain,
( spl35_16
| spl35_17
| spl35_1
| spl35_2
| ~ spl35_10 ),
inference(avatar_split_clause,[],[f1456,f643,f325,f321,f1477,f1473]) ).
fof(f1481,plain,
( empty_carrier(sF34)
| ~ one_sorted_str(sF34)
| ~ spl35_17 ),
inference(resolution,[],[f1479,f247]) ).
fof(f1484,plain,
( ~ one_sorted_str(sF34)
| spl35_1
| ~ spl35_17 ),
inference(forward_subsumption_resolution,[],[f1481,f322]) ).
fof(f1485,plain,
( $false
| spl35_1
| ~ spl35_17 ),
inference(forward_subsumption_resolution,[],[f1484,f670]) ).
fof(f1486,plain,
( spl35_1
| ~ spl35_17 ),
inference(avatar_contradiction_clause,[],[f1485]) ).
fof(f1488,plain,
( element(sK6(sF34),the_carrier(sK32))
| ~ spl35_16 ),
inference(resolution,[],[f1475,f297]) ).
fof(f1492,definition,
( spl35_18
<=> in(sK5(sF34),the_carrier(sK32)) ),
introduced(definition,[new_symbols(definition,[spl35_18])],[avatar_definition]) ).
fof(f1494,plain,
( in(sK5(sF34),the_carrier(sK32))
| ~ spl35_18 ),
inference(avatar_component_clause,[],[f1492]) ).
fof(f1495,plain,
( spl35_18
| spl35_17
| spl35_1
| spl35_2
| ~ spl35_10 ),
inference(avatar_split_clause,[],[f1454,f643,f325,f321,f1477,f1492]) ).
fof(f1497,plain,
( element(sK5(sF34),the_carrier(sK32))
| ~ spl35_18 ),
inference(resolution,[],[f1494,f297]) ).
fof(f1502,plain,
( ! [X0] :
( element(sK1(sK31,sK32,sK33,X0),the_carrier(sF34))
| ~ element(X0,the_carrier(sK32)) )
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15 ),
inference(resolution,[],[f1418,f297]) ).
fof(f3934,plain,
( ! [X0,X1] :
( ~ element(X0,the_carrier(sK32))
| ~ element(X1,the_carrier(sK32))
| ~ element(X1,the_carrier(sF34))
| related(sF34,X1,sK1(sK31,sK32,sK33,X0))
| ~ element(X0,the_carrier(sK32))
| ~ related(sK32,X1,X0)
| empty_carrier(sK31)
| ~ net_str(sK32,sK31)
| ~ one_sorted_str(sK31)
| ~ is_often_in(sK31,sK32,sK33) )
| ~ spl35_3
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15 ),
inference(resolution,[],[f1502,f1462]) ).
fof(f3938,plain,
( ! [X0,X1] :
( ~ element(X0,the_carrier(sK32))
| ~ element(X1,the_carrier(sK32))
| ~ element(X1,the_carrier(sF34))
| related(sF34,X1,sK1(sK31,sK32,sK33,X0))
| ~ related(sK32,X1,X0)
| empty_carrier(sK31)
| ~ net_str(sK32,sK31)
| ~ one_sorted_str(sK31)
| ~ is_often_in(sK31,sK32,sK33) )
| ~ spl35_3
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15 ),
inference(duplicate_literal_removal,[],[f3934]) ).
fof(f3941,plain,
( ! [X0,X1] :
( ~ element(X0,the_carrier(sK32))
| ~ element(X1,the_carrier(sK32))
| ~ element(X1,the_carrier(sF34))
| related(sF34,X1,sK1(sK31,sK32,sK33,X0))
| ~ related(sK32,X1,X0)
| ~ net_str(sK32,sK31)
| ~ one_sorted_str(sK31)
| ~ is_often_in(sK31,sK32,sK33) )
| ~ spl35_3
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15 ),
inference(forward_subsumption_resolution,[],[f3938,f307]) ).
fof(f3944,plain,
( ! [X0,X1] :
( ~ element(X0,the_carrier(sK32))
| ~ element(X1,the_carrier(sK32))
| ~ element(X1,the_carrier(sF34))
| related(sF34,X1,sK1(sK31,sK32,sK33,X0))
| ~ related(sK32,X1,X0)
| ~ one_sorted_str(sK31)
| ~ is_often_in(sK31,sK32,sK33) )
| ~ spl35_3
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15 ),
inference(forward_subsumption_resolution,[],[f3941,f302]) ).
fof(f3947,plain,
( ! [X0,X1] :
( ~ element(X0,the_carrier(sK32))
| ~ element(X1,the_carrier(sK32))
| ~ element(X1,the_carrier(sF34))
| related(sF34,X1,sK1(sK31,sK32,sK33,X0))
| ~ related(sK32,X1,X0)
| ~ is_often_in(sK31,sK32,sK33) )
| ~ spl35_3
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15 ),
inference(forward_subsumption_resolution,[],[f3944,f306]) ).
fof(f3950,plain,
( ! [X0,X1] :
( related(sF34,X1,sK1(sK31,sK32,sK33,X0))
| ~ element(X1,the_carrier(sK32))
| ~ element(X1,the_carrier(sF34))
| ~ element(X0,the_carrier(sK32))
| ~ related(sK32,X1,X0) )
| ~ spl35_3
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15 ),
inference(forward_subsumption_resolution,[],[f3947,f301]) ).
fof(f3978,plain,
( ! [X0] :
( ~ element(sK6(sF34),the_carrier(sK32))
| ~ element(sK6(sF34),the_carrier(sF34))
| ~ element(X0,the_carrier(sK32))
| ~ related(sK32,sK6(sF34),X0)
| empty_carrier(sF34)
| ~ rel_str(sF34)
| ~ related(sF34,sK5(sF34),sK1(sK31,sK32,sK33,X0))
| ~ element(sK1(sK31,sK32,sK33,X0),the_carrier(sF34))
| directed_relstr(sF34) )
| ~ spl35_3
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15 ),
inference(resolution,[],[f3950,f210]) ).
fof(f3980,plain,
( ! [X0] :
( ~ element(sK6(sF34),the_carrier(sK32))
| ~ element(sK6(sF34),the_carrier(sF34))
| ~ element(X0,the_carrier(sK32))
| ~ related(sK32,sK6(sF34),X0)
| empty_carrier(sF34)
| ~ rel_str(sF34)
| ~ related(sF34,sK5(sF34),sK1(sK31,sK32,sK33,X0))
| directed_relstr(sF34) )
| ~ spl35_3
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15 ),
inference(forward_subsumption_resolution,[],[f3978,f1502]) ).
fof(f3985,plain,
( ! [X0] :
( ~ element(sK6(sF34),the_carrier(sF34))
| ~ element(X0,the_carrier(sK32))
| ~ related(sK32,sK6(sF34),X0)
| empty_carrier(sF34)
| ~ rel_str(sF34)
| ~ related(sF34,sK5(sF34),sK1(sK31,sK32,sK33,X0))
| directed_relstr(sF34) )
| ~ spl35_3
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15
| ~ spl35_16 ),
inference(forward_subsumption_resolution,[],[f3980,f1488]) ).
fof(f3990,plain,
( ! [X0] :
( ~ element(X0,the_carrier(sK32))
| ~ related(sK32,sK6(sF34),X0)
| empty_carrier(sF34)
| ~ rel_str(sF34)
| ~ related(sF34,sK5(sF34),sK1(sK31,sK32,sK33,X0))
| directed_relstr(sF34) )
| ~ spl35_3
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15
| ~ spl35_16 ),
inference(forward_subsumption_resolution,[],[f3985,f211]) ).
fof(f3994,plain,
( ! [X0] :
( ~ element(X0,the_carrier(sK32))
| ~ related(sK32,sK6(sF34),X0)
| ~ rel_str(sF34)
| ~ related(sF34,sK5(sF34),sK1(sK31,sK32,sK33,X0))
| directed_relstr(sF34) )
| spl35_1
| ~ spl35_3
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15
| ~ spl35_16 ),
inference(forward_subsumption_resolution,[],[f3990,f322]) ).
fof(f3996,plain,
( ! [X0] :
( ~ element(X0,the_carrier(sK32))
| ~ related(sK32,sK6(sF34),X0)
| ~ related(sF34,sK5(sF34),sK1(sK31,sK32,sK33,X0))
| directed_relstr(sF34) )
| spl35_1
| ~ spl35_3
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15
| ~ spl35_16 ),
inference(forward_subsumption_resolution,[],[f3994,f669]) ).
fof(f3998,plain,
( ! [X0] :
( ~ related(sF34,sK5(sF34),sK1(sK31,sK32,sK33,X0))
| ~ related(sK32,sK6(sF34),X0)
| ~ element(X0,the_carrier(sK32)) )
| spl35_1
| spl35_2
| ~ spl35_3
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15
| ~ spl35_16 ),
inference(forward_subsumption_resolution,[],[f3996,f327]) ).
fof(f4000,plain,
( ! [X0] :
( ~ related(sK32,sK6(sF34),X0)
| ~ element(X0,the_carrier(sK32))
| ~ element(sK5(sF34),the_carrier(sK32))
| ~ element(sK5(sF34),the_carrier(sF34))
| ~ element(X0,the_carrier(sK32))
| ~ related(sK32,sK5(sF34),X0) )
| spl35_1
| spl35_2
| ~ spl35_3
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15
| ~ spl35_16 ),
inference(resolution,[],[f3998,f3950]) ).
fof(f4001,plain,
( ! [X0] :
( ~ related(sK32,sK6(sF34),X0)
| ~ element(X0,the_carrier(sK32))
| ~ element(sK5(sF34),the_carrier(sK32))
| ~ element(sK5(sF34),the_carrier(sF34))
| ~ related(sK32,sK5(sF34),X0) )
| spl35_1
| spl35_2
| ~ spl35_3
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15
| ~ spl35_16 ),
inference(duplicate_literal_removal,[],[f4000]) ).
fof(f4003,plain,
( ! [X0] :
( ~ related(sK32,sK6(sF34),X0)
| ~ element(X0,the_carrier(sK32))
| ~ element(sK5(sF34),the_carrier(sF34))
| ~ related(sK32,sK5(sF34),X0) )
| spl35_1
| spl35_2
| ~ spl35_3
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15
| ~ spl35_16
| ~ spl35_18 ),
inference(forward_subsumption_resolution,[],[f4001,f1497]) ).
fof(f4006,definition,
( spl35_44
<=> element(sK5(sF34),the_carrier(sF34)) ),
introduced(definition,[new_symbols(definition,[spl35_44])],[avatar_definition]) ).
fof(f4008,plain,
( ~ element(sK5(sF34),the_carrier(sF34))
| spl35_44 ),
inference(avatar_component_clause,[],[f4006]) ).
fof(f4014,plain,
( empty_carrier(sF34)
| ~ rel_str(sF34)
| directed_relstr(sF34)
| spl35_44 ),
inference(resolution,[],[f4008,f212]) ).
fof(f4015,plain,
( ~ rel_str(sF34)
| directed_relstr(sF34)
| spl35_1
| spl35_44 ),
inference(forward_subsumption_resolution,[],[f4014,f322]) ).
fof(f4016,plain,
( directed_relstr(sF34)
| spl35_1
| spl35_44 ),
inference(forward_subsumption_resolution,[],[f4015,f669]) ).
fof(f4017,plain,
( $false
| spl35_1
| spl35_2
| spl35_44 ),
inference(forward_subsumption_resolution,[],[f4016,f327]) ).
fof(f4018,plain,
( spl35_1
| spl35_2
| spl35_44 ),
inference(avatar_contradiction_clause,[],[f4017]) ).
fof(f4032,definition,
( spl35_47
<=> ! [X0] :
( ~ related(sK32,sK6(sF34),X0)
| ~ related(sK32,sK5(sF34),X0)
| ~ element(X0,the_carrier(sK32)) ) ),
introduced(definition,[new_symbols(definition,[spl35_47])],[avatar_definition]) ).
fof(f4033,plain,
( ! [X0] :
( ~ related(sK32,sK6(sF34),X0)
| ~ related(sK32,sK5(sF34),X0)
| ~ element(X0,the_carrier(sK32)) )
| ~ spl35_47 ),
inference(avatar_component_clause,[],[f4032]) ).
fof(f4034,plain,
( ~ spl35_44
| spl35_47
| spl35_1
| spl35_2
| ~ spl35_3
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15
| ~ spl35_16
| ~ spl35_18 ),
inference(avatar_split_clause,[],[f4003,f1492,f1473,f830,f646,f583,f579,f571,f421,f325,f321,f4032,f4006]) ).
fof(f4038,plain,
( ! [X0] :
( ~ related(sK32,sK5(sF34),sK7(sK32,X0,sK6(sF34)))
| ~ element(sK7(sK32,X0,sK6(sF34)),the_carrier(sK32))
| empty_carrier(sK32)
| ~ element(X0,the_carrier(sK32))
| ~ element(sK6(sF34),the_carrier(sK32))
| ~ rel_str(sK32)
| ~ directed_relstr(sK32) )
| ~ spl35_47 ),
inference(resolution,[],[f4033,f207]) ).
fof(f4049,plain,
( ! [X0] :
( ~ related(sK32,sK5(sF34),sK7(sK32,X0,sK6(sF34)))
| empty_carrier(sK32)
| ~ element(X0,the_carrier(sK32))
| ~ element(sK6(sF34),the_carrier(sK32))
| ~ rel_str(sK32)
| ~ directed_relstr(sK32) )
| ~ spl35_47 ),
inference(forward_subsumption_resolution,[],[f4038,f209]) ).
fof(f4058,plain,
( ! [X0] :
( ~ related(sK32,sK5(sF34),sK7(sK32,X0,sK6(sF34)))
| ~ element(X0,the_carrier(sK32))
| ~ element(sK6(sF34),the_carrier(sK32))
| ~ rel_str(sK32)
| ~ directed_relstr(sK32) )
| ~ spl35_47 ),
inference(forward_subsumption_resolution,[],[f4049,f305]) ).
fof(f4067,plain,
( ! [X0] :
( ~ related(sK32,sK5(sF34),sK7(sK32,X0,sK6(sF34)))
| ~ element(X0,the_carrier(sK32))
| ~ rel_str(sK32)
| ~ directed_relstr(sK32) )
| ~ spl35_16
| ~ spl35_47 ),
inference(forward_subsumption_resolution,[],[f4058,f1488]) ).
fof(f4076,plain,
( ! [X0] :
( ~ related(sK32,sK5(sF34),sK7(sK32,X0,sK6(sF34)))
| ~ element(X0,the_carrier(sK32))
| ~ directed_relstr(sK32) )
| ~ spl35_16
| ~ spl35_47 ),
inference(forward_subsumption_resolution,[],[f4067,f346]) ).
fof(f4084,plain,
( ! [X0] :
( ~ related(sK32,sK5(sF34),sK7(sK32,X0,sK6(sF34)))
| ~ element(X0,the_carrier(sK32)) )
| ~ spl35_16
| ~ spl35_47 ),
inference(forward_subsumption_resolution,[],[f4076,f303]) ).
fof(f4093,plain,
( ~ element(sK5(sF34),the_carrier(sK32))
| empty_carrier(sK32)
| ~ element(sK5(sF34),the_carrier(sK32))
| ~ element(sK6(sF34),the_carrier(sK32))
| ~ rel_str(sK32)
| ~ directed_relstr(sK32)
| ~ spl35_16
| ~ spl35_47 ),
inference(resolution,[],[f4084,f208]) ).
fof(f4094,plain,
( ~ element(sK5(sF34),the_carrier(sK32))
| empty_carrier(sK32)
| ~ element(sK6(sF34),the_carrier(sK32))
| ~ rel_str(sK32)
| ~ directed_relstr(sK32)
| ~ spl35_16
| ~ spl35_47 ),
inference(duplicate_literal_removal,[],[f4093]) ).
fof(f4099,plain,
( empty_carrier(sK32)
| ~ element(sK6(sF34),the_carrier(sK32))
| ~ rel_str(sK32)
| ~ directed_relstr(sK32)
| ~ spl35_16
| ~ spl35_18
| ~ spl35_47 ),
inference(forward_subsumption_resolution,[],[f4094,f1497]) ).
fof(f4103,plain,
( ~ element(sK6(sF34),the_carrier(sK32))
| ~ rel_str(sK32)
| ~ directed_relstr(sK32)
| ~ spl35_16
| ~ spl35_18
| ~ spl35_47 ),
inference(forward_subsumption_resolution,[],[f4099,f305]) ).
fof(f4107,plain,
( ~ rel_str(sK32)
| ~ directed_relstr(sK32)
| ~ spl35_16
| ~ spl35_18
| ~ spl35_47 ),
inference(forward_subsumption_resolution,[],[f4103,f1488]) ).
fof(f4111,plain,
( ~ directed_relstr(sK32)
| ~ spl35_16
| ~ spl35_18
| ~ spl35_47 ),
inference(forward_subsumption_resolution,[],[f4107,f346]) ).
fof(f4115,plain,
( $false
| ~ spl35_16
| ~ spl35_18
| ~ spl35_47 ),
inference(forward_subsumption_resolution,[],[f4111,f303]) ).
fof(f4116,plain,
( ~ spl35_16
| ~ spl35_18
| ~ spl35_47 ),
inference(avatar_contradiction_clause,[],[f4115]) ).
cnf(s1,plain,
( spl35_1
| ~ spl35_2 ),
inference(sat_conversion,[],[f328]) ).
cnf(s2,plain,
( spl35_1
| spl35_3 ),
inference(sat_conversion,[],[f423]) ).
cnf(s4,plain,
( ~ spl35_6
| ~ spl35_7
| ~ spl35_8
| spl35_9 ),
inference(sat_conversion,[],[f586]) ).
cnf(s5,plain,
spl35_6,
inference(sat_conversion,[],[f590]) ).
cnf(s7,plain,
spl35_7,
inference(sat_conversion,[],[f600]) ).
cnf(s9,plain,
spl35_8,
inference(sat_conversion,[],[f610]) ).
cnf(s10,plain,
( ~ spl35_7
| ~ spl35_9
| spl35_10
| spl35_11 ),
inference(sat_conversion,[],[f649]) ).
cnf(s13,plain,
~ spl35_11,
inference(sat_conversion,[],[f759]) ).
cnf(s15,plain,
( ~ spl35_1
| spl35_5
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15 ),
inference(sat_conversion,[],[f1363]) ).
cnf(s16,plain,
~ spl35_5,
inference(sat_conversion,[],[f1375]) ).
cnf(s17,plain,
~ spl35_15,
inference(sat_conversion,[],[f1404]) ).
cnf(s19,plain,
( spl35_1
| spl35_2
| ~ spl35_10
| spl35_16
| spl35_17 ),
inference(sat_conversion,[],[f1480]) ).
cnf(s20,plain,
( spl35_1
| ~ spl35_17 ),
inference(sat_conversion,[],[f1486]) ).
cnf(s21,plain,
( spl35_1
| spl35_2
| ~ spl35_10
| spl35_17
| spl35_18 ),
inference(sat_conversion,[],[f1495]) ).
cnf(s44,plain,
( spl35_1
| spl35_2
| spl35_44 ),
inference(sat_conversion,[],[f4018]) ).
cnf(s46,plain,
( spl35_1
| spl35_2
| ~ spl35_3
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11
| spl35_15
| ~ spl35_16
| ~ spl35_18
| ~ spl35_44
| spl35_47 ),
inference(sat_conversion,[],[f4034]) ).
cnf(s47,plain,
( ~ spl35_16
| ~ spl35_18
| ~ spl35_47 ),
inference(sat_conversion,[],[f4116]) ).
cnf(s49,plain,
( ~ spl35_1
| ~ spl35_6
| ~ spl35_8
| ~ spl35_9
| spl35_11 ),
inference(rat,[],[s15,s17,s16]) ).
cnf(s51,plain,
( ~ spl35_7
| ~ spl35_9
| spl35_10 ),
inference(rat,[],[s10,s13]) ).
cnf(s54,plain,
spl35_9,
inference(rat,[],[s4,s9,s7,s5]) ).
cnf(s57,plain,
spl35_10,
inference(rat,[],[s51,s7,s54]) ).
cnf(s59,plain,
~ spl35_1,
inference(rat,[],[s49,s13,s5,s9,s54]) ).
cnf(s61,plain,
~ spl35_17,
inference(rat,[],[s20,s59]) ).
cnf(s69,plain,
spl35_3,
inference(rat,[],[s2,s59]) ).
cnf(s70,plain,
~ spl35_2,
inference(rat,[],[s1,s59]) ).
cnf(s71,plain,
spl35_44,
inference(rat,[],[s44,s59,s70]) ).
cnf(s74,plain,
spl35_18,
inference(rat,[],[s21,s61,s59,s57,s70]) ).
cnf(s75,plain,
spl35_16,
inference(rat,[],[s19,s61,s59,s57,s70]) ).
cnf(s76,plain,
~ spl35_47,
inference(rat,[],[s47,s74,s75]) ).
cnf(s77,plain,
$false,
inference(rat,[],[s46,s74,s71,s70,s69,s17,s13,s54,s9,s5,s59,s76,s75]) ).
fof(f4123,plain,
$false,
inference(avatar_sat_refutation,[],[s77]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : SEU377+1 : TPTP v9.3.1. Released v3.3.0.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.36 % Computer : n004.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 28 05:00:07 UTC 2026
% 0.09/0.37 % CPUTime :
% 0.09/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.09/0.40 Running first-order theorem proving
% 0.09/0.40 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
% 12.59/2.65 % (4162842)Detected formulas, will run a generic FOF schedule.
% 12.59/2.65 % (4162847)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=3648536129:i=141193_2999 on theBenchmark for (2999ds/141193Mi)
% 12.59/2.65 % (4162850)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=754961870:i=109:sd=1:ins=1:gsp=on:ss=axioms_2999 on theBenchmark for (2999ds/109Mi)
% 12.59/2.65 % (4162851)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=622539056:i=119:av=off:ss=axioms_2999 on theBenchmark for (2999ds/119Mi)
% 12.59/2.65 % (4162849)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=3052133921:i=141695:sd=1:nm=32:gsp=on:ss=included_2999 on theBenchmark for (2999ds/141695Mi)
% 12.59/2.65 % (4162848)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=3677629444:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/134677Mi)
% 12.59/2.65 % (4162852)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4115838165:s2a=on:i=139:gtg=position_2999 on theBenchmark for (2999ds/139Mi)
% 12.59/2.65 % (4162850)Refutation not found, incomplete strategy
% 12.59/2.65 % (4162850)------------------------------
% 12.59/2.65 % (4162850)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.59/2.65 % (4162850)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.59/2.65 % (4162850)CaDiCaL version: 2.1.3
% 12.59/2.65 % (4162850)Termination reason: Refutation not found, incomplete strategy
% 12.59/2.65 % (4162850)Time elapsed: 0.002 s
% 12.59/2.65 % (4162850)Peak memory usage: 87 MB
% 12.59/2.65 % (4162850)Instructions burned: 1 (million)
% 12.59/2.65 % (4162853)dis-21_1_sil=8000:lcm=predicate:random_seed=4159624766: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)
% 12.59/2.65 % (4162851)Instruction limit reached!
% 12.59/2.65 % (4162851)------------------------------
% 12.59/2.65 % (4162851)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.59/2.65 % (4162851)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.59/2.65 % (4162851)CaDiCaL version: 2.1.3
% 12.59/2.65 % (4162851)Termination reason: Instruction limit
% 12.59/2.65 % (4162851)Termination phase: Saturation
% 12.59/2.65 % (4162851)Time elapsed: 0.069 s
% 12.59/2.65 % (4162851)Peak memory usage: 88 MB
% 12.59/2.65 % (4162851)Instructions burned: 121 (million)
% 12.59/2.65 % (4162853)Instruction limit reached!
% 12.59/2.65 % (4162853)------------------------------
% 12.59/2.65 % (4162853)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.59/2.65 % (4162853)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.59/2.65 % (4162853)CaDiCaL version: 2.1.3
% 12.59/2.65 % (4162853)Termination reason: Instruction limit
% 12.59/2.65 % (4162853)Termination phase: Saturation
% 12.59/2.65 % (4162853)Time elapsed: 0.078 s
% 12.59/2.65 % (4162853)Peak memory usage: 90 MB
% 12.59/2.65 % (4162853)Instructions burned: 129 (million)
% 12.59/2.65 % (4162852)Instruction limit reached!
% 12.59/2.65 % (4162852)------------------------------
% 12.59/2.65 % (4162852)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.59/2.65 % (4162852)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.59/2.65 % (4162852)CaDiCaL version: 2.1.3
% 12.59/2.65 % (4162852)Termination reason: Instruction limit
% 12.59/2.65 % (4162852)Termination phase: Saturation
% 12.59/2.65 % (4162852)Time elapsed: 0.103 s
% 12.59/2.65 % (4162852)Peak memory usage: 90 MB
% 12.59/2.65 % (4162852)Instructions burned: 140 (million)
% 12.59/2.65 % (4162861)lrs+10_1_sil=8000:sp=occurrence:random_seed=357841495:i=285:sd=3:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/285Mi)
% 12.59/2.65 % (4162862)lrs+10_1_sil=32000:urr=on:br=off:random_seed=2231181136:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2997 on theBenchmark for (2997ds/157Mi)
% 12.59/2.65 % (4162862)Refutation not found, incomplete strategy
% 12.59/2.65 % (4162862)------------------------------
% 12.59/2.65 % (4162862)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.59/2.65 % (4162862)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.59/2.65 % (4162862)CaDiCaL version: 2.1.3
% 12.59/2.65 % (4162862)Termination reason: Refutation not found, incomplete strategy
% 20.98/3.89 % (4162862)Time elapsed: 0.006 s
% 20.98/3.89 % (4162862)Peak memory usage: 89 MB
% 20.98/3.89 % (4162862)Instructions burned: 7 (million)
% 20.98/3.89 % (4162850)------------------------------
% 20.98/3.89 % (4162850)------------------------------
% 20.98/3.89 % (4162863)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1373849583:i=325:sd=1:ss=axioms:sgt=32_2997 on theBenchmark for (2997ds/325Mi)
% 20.98/3.89 % (4162861)Instruction limit reached!
% 20.98/3.89 % (4162861)------------------------------
% 20.98/3.89 % (4162861)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.98/3.89 % (4162861)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.98/3.89 % (4162861)CaDiCaL version: 2.1.3
% 20.98/3.89 % (4162861)Termination reason: Instruction limit
% 20.98/3.89 % (4162861)Termination phase: Saturation
% 20.98/3.89 % (4162861)Time elapsed: 0.178 s
% 20.98/3.89 % (4162861)Peak memory usage: 93 MB
% 20.98/3.89 % (4162861)Instructions burned: 285 (million)
% 20.98/3.89 % (4162866)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=4175653069:s2a=on:i=248:s2at=1.23:gtg=position_2995 on theBenchmark for (2995ds/248Mi)
% 20.98/3.89 % (4162863)Instruction limit reached!
% 20.98/3.89 % (4162863)------------------------------
% 20.98/3.89 % (4162863)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.98/3.89 % (4162863)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.98/3.89 % (4162863)CaDiCaL version: 2.1.3
% 20.98/3.89 % (4162863)Termination reason: Instruction limit
% 20.98/3.89 % (4162863)Termination phase: Saturation
% 20.98/3.89 % (4162863)Time elapsed: 0.176 s
% 20.98/3.89 % (4162863)Peak memory usage: 90 MB
% 20.98/3.89 % (4162863)Instructions burned: 327 (million)
% 20.98/3.89 % (4162862)------------------------------
% 20.98/3.89 % (4162862)------------------------------
% 20.98/3.89 % (4162868)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=114055923:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2994 on theBenchmark for (2994ds/294Mi)
% 20.98/3.89 % (4162868)Refutation not found, incomplete strategy
% 20.98/3.89 % (4162868)------------------------------
% 20.98/3.89 % (4162868)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.98/3.89 % (4162868)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.98/3.89 % (4162868)CaDiCaL version: 2.1.3
% 20.98/3.89 % (4162868)Termination reason: Refutation not found, incomplete strategy
% 20.98/3.89 % (4162868)Time elapsed: 0.005 s
% 20.98/3.89 % (4162868)Peak memory usage: 88 MB
% 20.98/3.89 % (4162868)Instructions burned: 6 (million)
% 20.98/3.89 % (4162866)Instruction limit reached!
% 20.98/3.89 % (4162866)------------------------------
% 20.98/3.89 % (4162866)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.98/3.89 % (4162866)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.98/3.89 % (4162866)CaDiCaL version: 2.1.3
% 20.98/3.89 % (4162866)Termination reason: Instruction limit
% 20.98/3.89 % (4162866)Termination phase: Saturation
% 20.98/3.89 % (4162866)Time elapsed: 0.151 s
% 20.98/3.89 % (4162866)Peak memory usage: 92 MB
% 20.98/3.89 % (4162866)Instructions burned: 249 (million)
% 20.98/3.89 % (4162870)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=1638574978:i=2350_2993 on theBenchmark for (2993ds/2350Mi)
% 20.98/3.89 % (4162871)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=3878278457:cts=off:i=113:fsr=off:ss=included:sgt=4_2993 on theBenchmark for (2993ds/113Mi)
% 20.98/3.89 % (4162871)Instruction limit reached!
% 20.98/3.89 % (4162871)------------------------------
% 20.98/3.89 % (4162871)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.98/3.89 % (4162871)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.98/3.89 % (4162871)CaDiCaL version: 2.1.3
% 20.98/3.89 % (4162871)Termination reason: Instruction limit
% 20.98/3.89 % (4162871)Termination phase: Saturation
% 20.98/3.89 % (4162871)Time elapsed: 0.079 s
% 20.98/3.89 % (4162871)Peak memory usage: 91 MB
% 20.98/3.89 % (4162871)Instructions burned: 113 (million)
% 20.98/3.89 % (4162873)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1808014469:i=127:av=off:fsr=off:sup=off_2992 on theBenchmark for (2992ds/127Mi)
% 20.98/3.89 % (4162868)------------------------------
% 20.98/3.89 % (4162868)------------------------------
% 20.98/3.89 % (4162873)Instruction limit reached!
% 20.98/3.89 % (4162873)------------------------------
% 20.98/3.89 % (4162873)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.11/7.34 % (4162873)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.11/7.34 % (4162873)CaDiCaL version: 2.1.3
% 46.11/7.34 % (4162873)Termination reason: Instruction limit
% 46.11/7.34 % (4162873)Termination phase: Saturation
% 46.11/7.34 % (4162873)Time elapsed: 0.070 s
% 46.11/7.34 % (4162873)Peak memory usage: 89 MB
% 46.11/7.34 % (4162873)Instructions burned: 128 (million)
% 46.11/7.34 % (4162877)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=2633026255:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2991 on theBenchmark for (2991ds/114Mi)
% 46.11/7.34 % (4162878)lrs+10_1_sil=8000:sp=occurrence:random_seed=3282815821:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2990 on theBenchmark for (2990ds/907Mi)
% 46.11/7.34 % (4162879)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=3232976305:i=437:sd=1:aac=none:ss=included_2990 on theBenchmark for (2990ds/437Mi)
% 46.11/7.34 % (4162879)Refutation not found, incomplete strategy
% 46.11/7.34 % (4162879)------------------------------
% 46.11/7.34 % (4162879)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.11/7.34 % (4162879)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.11/7.34 % (4162879)CaDiCaL version: 2.1.3
% 46.11/7.34 % (4162879)Termination reason: Refutation not found, incomplete strategy
% 46.11/7.34 % (4162879)Time elapsed: 0.005 s
% 46.11/7.34 % (4162879)Peak memory usage: 88 MB
% 46.11/7.34 % (4162879)Instructions burned: 7 (million)
% 46.11/7.34 % (4162877)Instruction limit reached!
% 46.11/7.34 % (4162877)------------------------------
% 46.11/7.34 % (4162877)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.11/7.34 % (4162877)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.11/7.34 % (4162877)CaDiCaL version: 2.1.3
% 46.11/7.34 % (4162877)Termination reason: Instruction limit
% 46.11/7.34 % (4162877)Termination phase: Saturation
% 46.11/7.34 % (4162877)Time elapsed: 0.069 s
% 46.11/7.34 % (4162877)Peak memory usage: 89 MB
% 46.11/7.34 % (4162877)Instructions burned: 115 (million)
% 46.11/7.34 % (4162883)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3095293176:i=5202:ss=axioms:sgt=16_2988 on theBenchmark for (2988ds/5202Mi)
% 46.11/7.34 % (4162879)------------------------------
% 46.11/7.34 % (4162879)------------------------------
% 46.11/7.34 % (4162885)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=719391805:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2986 on theBenchmark for (2986ds/134Mi)
% 46.11/7.34 % (4162885)Instruction limit reached!
% 46.11/7.34 % (4162885)------------------------------
% 46.11/7.34 % (4162885)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.11/7.34 % (4162885)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.11/7.34 % (4162885)CaDiCaL version: 2.1.3
% 46.11/7.34 % (4162885)Termination reason: Instruction limit
% 46.11/7.34 % (4162885)Termination phase: Saturation
% 46.11/7.34 % (4162885)Time elapsed: 0.080 s
% 46.11/7.34 % (4162885)Peak memory usage: 91 MB
% 46.11/7.34 % (4162885)Instructions burned: 135 (million)
% 46.11/7.34 % (4162878)Instruction limit reached!
% 46.11/7.34 % (4162878)------------------------------
% 46.11/7.34 % (4162878)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.11/7.34 % (4162878)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.11/7.34 % (4162878)CaDiCaL version: 2.1.3
% 46.11/7.34 % (4162878)Termination reason: Instruction limit
% 46.11/7.34 % (4162878)Termination phase: Saturation
% 46.11/7.34 % (4162878)Time elapsed: 0.532 s
% 46.11/7.34 % (4162878)Peak memory usage: 100 MB
% 46.11/7.34 % (4162878)Instructions burned: 911 (million)
% 46.11/7.34 % (4162887)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=8754802:st=8:i=592:sd=3:ep=RST:ss=axioms_2983 on theBenchmark for (2983ds/592Mi)
% 46.11/7.34 % (4162887)Refutation not found, incomplete strategy
% 46.11/7.34 % (4162887)------------------------------
% 46.11/7.34 % (4162887)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 46.11/7.34 % (4162887)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 46.11/7.34 % (4162887)CaDiCaL version: 2.1.3
% 46.11/7.34 % (4162887)Termination reason: Refutation not found, incomplete strategy
% 46.11/7.34 % (4162887)Time elapsed: 0.005 s
% 46.11/7.34 % (4162887)Peak memory usage: 88 MB
% 46.11/7.34 % (4162887)Instructions burned: 8 (million)
% 46.11/7.34 % (4162888)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2367553061:st=3:i=13193:sd=3:ss=axioms_2983 on theBenchmark for (2983ds/13193Mi)
% 73.68/11.28 % (4162887)------------------------------
% 73.68/11.28 % (4162887)------------------------------
% 73.68/11.28 % (4162891)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=4050599453:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2979 on theBenchmark for (2979ds/125Mi)
% 73.68/11.28 % (4162891)Instruction limit reached!
% 73.68/11.28 % (4162891)------------------------------
% 73.68/11.28 % (4162891)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.68/11.28 % (4162891)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.68/11.28 % (4162891)CaDiCaL version: 2.1.3
% 73.68/11.28 % (4162891)Termination reason: Instruction limit
% 73.68/11.28 % (4162891)Termination phase: Saturation
% 73.68/11.28 % (4162891)Time elapsed: 0.079 s
% 73.68/11.28 % (4162891)Peak memory usage: 91 MB
% 73.68/11.28 % (4162891)Instructions burned: 126 (million)
% 73.68/11.28 % (4162870)Instruction limit reached!
% 73.68/11.28 % (4162870)------------------------------
% 73.68/11.28 % (4162870)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.68/11.28 % (4162870)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.68/11.28 % (4162870)CaDiCaL version: 2.1.3
% 73.68/11.28 % (4162870)Termination reason: Instruction limit
% 73.68/11.28 % (4162870)Termination phase: Saturation
% 73.68/11.28 % (4162870)Time elapsed: 1.547 s
% 73.68/11.28 % (4162870)Peak memory usage: 141 MB
% 73.68/11.28 % (4162870)Instructions burned: 2350 (million)
% 73.68/11.28 % (4162893)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=1873173003:i=134:gtgl=5:slsql=off:gtg=exists_sym_2977 on theBenchmark for (2977ds/134Mi)
% 73.68/11.28 % (4162894)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1666450721:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2976 on theBenchmark for (2976ds/141Mi)
% 73.68/11.28 % (4162894)Refutation not found, incomplete strategy
% 73.68/11.28 % (4162894)------------------------------
% 73.68/11.28 % (4162894)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.68/11.28 % (4162894)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.68/11.28 % (4162894)CaDiCaL version: 2.1.3
% 73.68/11.28 % (4162894)Termination reason: Refutation not found, incomplete strategy
% 73.68/11.28 % (4162894)Time elapsed: 0.002 s
% 73.68/11.28 % (4162894)Peak memory usage: 88 MB
% 73.68/11.28 % (4162894)Instructions burned: 2 (million)
% 73.68/11.28 % (4162893)Instruction limit reached!
% 73.68/11.28 % (4162893)------------------------------
% 73.68/11.28 % (4162893)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.68/11.28 % (4162893)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.68/11.28 % (4162893)CaDiCaL version: 2.1.3
% 73.68/11.28 % (4162893)Termination reason: Instruction limit
% 73.68/11.28 % (4162893)Termination phase: Saturation
% 73.68/11.28 % (4162893)Time elapsed: 0.079 s
% 73.68/11.28 % (4162893)Peak memory usage: 90 MB
% 73.68/11.28 % (4162893)Instructions burned: 135 (million)
% 73.68/11.28 % (4162897)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1234821997:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2974 on theBenchmark for (2974ds/431Mi)
% 73.68/11.28 % (4162894)------------------------------
% 73.68/11.28 % (4162894)------------------------------
% 73.68/11.28 % (4162899)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=2515938618:i=6060:aac=none:ins=25_2972 on theBenchmark for (2972ds/6060Mi)
% 73.68/11.28 % (4162897)Instruction limit reached!
% 73.68/11.28 % (4162897)------------------------------
% 73.68/11.28 % (4162897)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 73.68/11.28 % (4162897)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 73.68/11.28 % (4162897)CaDiCaL version: 2.1.3
% 73.68/11.28 % (4162897)Termination reason: Instruction limit
% 73.68/11.28 % (4162897)Termination phase: Saturation
% 73.68/11.28 % (4162897)Time elapsed: 0.208 s
% 73.68/11.28 % (4162897)Peak memory usage: 90 MB
% 73.68/11.28 % (4162897)Instructions burned: 431 (million)
% 73.68/11.28 % (4162901)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=1256781763:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2971 on theBenchmark for (2971ds/150Mi)
% 105.24/15.71 % (4162901)Instruction limit reached!
% 105.24/15.71 % (4162901)------------------------------
% 105.24/15.71 % (4162901)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.24/15.71 % (4162901)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.24/15.71 % (4162901)CaDiCaL version: 2.1.3
% 105.24/15.71 % (4162901)Termination reason: Instruction limit
% 105.24/15.71 % (4162901)Termination phase: Saturation
% 105.24/15.71 % (4162901)Time elapsed: 0.097 s
% 105.24/15.71 % (4162901)Peak memory usage: 91 MB
% 105.24/15.71 % (4162901)Instructions burned: 151 (million)
% 105.24/15.71 % (4162903)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=3660339318:i=14155:bd=all_2968 on theBenchmark for (2968ds/14155Mi)
% 105.24/15.71 % (4162883)Instruction limit reached!
% 105.24/15.71 % (4162883)------------------------------
% 105.24/15.71 % (4162883)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.24/15.71 % (4162883)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.24/15.71 % (4162883)CaDiCaL version: 2.1.3
% 105.24/15.71 % (4162883)Termination reason: Instruction limit
% 105.24/15.71 % (4162883)Termination phase: Saturation
% 105.24/15.71 % (4162883)Time elapsed: 2.911 s
% 105.24/15.71 % (4162883)Peak memory usage: 156 MB
% 105.24/15.71 % (4162883)Instructions burned: 5204 (million)
% 105.24/15.71 % (4162905)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1882960618:i=667:av=off:fsr=off_2957 on theBenchmark for (2957ds/667Mi)
% 105.24/15.71 % (4162905)Refutation not found, incomplete strategy
% 105.24/15.71 % (4162905)------------------------------
% 105.24/15.71 % (4162905)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.24/15.71 % (4162905)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.24/15.71 % (4162905)CaDiCaL version: 2.1.3
% 105.24/15.71 % (4162905)Termination reason: Refutation not found, incomplete strategy
% 105.24/15.71 % (4162905)Time elapsed: 0.005 s
% 105.24/15.71 % (4162905)Peak memory usage: 88 MB
% 105.24/15.71 % (4162905)Instructions burned: 8 (million)
% 105.24/15.71 % (4162905)------------------------------
% 105.24/15.71 % (4162905)------------------------------
% 105.24/15.71 % (4162907)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=3870305839:s2a=on:i=185:s2at=1.8:fdi=4_2953 on theBenchmark for (2953ds/185Mi)
% 105.24/15.71 % (4162907)Instruction limit reached!
% 105.24/15.71 % (4162907)------------------------------
% 105.24/15.71 % (4162907)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.24/15.71 % (4162907)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.24/15.71 % (4162907)CaDiCaL version: 2.1.3
% 105.24/15.71 % (4162907)Termination reason: Instruction limit
% 105.24/15.71 % (4162907)Termination phase: Saturation
% 105.24/15.71 % (4162907)Time elapsed: 0.116 s
% 105.24/15.71 % (4162907)Peak memory usage: 92 MB
% 105.24/15.71 % (4162907)Instructions burned: 186 (million)
% 105.24/15.71 % (4162909)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=2529076772:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2950 on theBenchmark for (2950ds/193Mi)
% 105.24/15.71 % (4162909)Instruction limit reached!
% 105.24/15.71 % (4162909)------------------------------
% 105.24/15.71 % (4162909)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.24/15.71 % (4162909)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.24/15.71 % (4162909)CaDiCaL version: 2.1.3
% 105.24/15.71 % (4162909)Termination reason: Instruction limit
% 105.24/15.71 % (4162909)Termination phase: Saturation
% 105.24/15.71 % (4162909)Time elapsed: 0.106 s
% 105.24/15.71 % (4162909)Peak memory usage: 91 MB
% 105.24/15.71 % (4162909)Instructions burned: 194 (million)
% 105.24/15.71 % (4162911)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=658117389:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2948 on theBenchmark for (2948ds/4850Mi)
% 105.24/15.71 % (4162899)Instruction limit reached!
% 105.24/15.71 % (4162899)------------------------------
% 105.24/15.71 % (4162899)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.24/15.71 % (4162899)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.24/15.71 % (4162899)CaDiCaL version: 2.1.3
% 105.24/15.71 % (4162899)Termination reason: Instruction limit
% 105.24/15.71 % (4162899)Termination phase: Saturation
% 105.24/15.71 % (4162899)Time elapsed: 3.628 s
% 105.24/15.71 % (4162899)Peak memory usage: 163 MB
% 134.27/20.02 % (4162899)Instructions burned: 6061 (million)
% 134.27/20.02 % (4162915)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1275096181:i=12111:sd=1:ss=included_2934 on theBenchmark for (2934ds/12111Mi)
% 134.27/20.02 % (4162911)Instruction limit reached!
% 134.27/20.02 % (4162911)------------------------------
% 134.27/20.02 % (4162911)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.27/20.02 % (4162911)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.27/20.02 % (4162911)CaDiCaL version: 2.1.3
% 134.27/20.02 % (4162911)Termination reason: Instruction limit
% 134.27/20.02 % (4162911)Termination phase: Saturation
% 134.27/20.02 % (4162911)Time elapsed: 2.995 s
% 134.27/20.02 % (4162911)Peak memory usage: 154 MB
% 134.27/20.02 % (4162911)Instructions burned: 4850 (million)
% 134.27/20.02 % (4162917)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3538422020:i=319:kws=precedence:fsr=off_2916 on theBenchmark for (2916ds/319Mi)
% 134.27/20.02 % (4162888)Instruction limit reached!
% 134.27/20.02 % (4162888)------------------------------
% 134.27/20.02 % (4162888)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.27/20.02 % (4162888)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.27/20.02 % (4162888)CaDiCaL version: 2.1.3
% 134.27/20.02 % (4162888)Termination reason: Instruction limit
% 134.27/20.02 % (4162888)Termination phase: Saturation
% 134.27/20.02 % (4162888)Time elapsed: 6.755 s
% 134.27/20.02 % (4162888)Peak memory usage: 248 MB
% 134.27/20.02 % (4162888)Instructions burned: 13195 (million)
% 134.27/20.02 % (4162917)Instruction limit reached!
% 134.27/20.02 % (4162917)------------------------------
% 134.27/20.02 % (4162917)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.27/20.02 % (4162917)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.27/20.02 % (4162917)CaDiCaL version: 2.1.3
% 134.27/20.02 % (4162917)Termination reason: Instruction limit
% 134.27/20.02 % (4162917)Termination phase: Saturation
% 134.27/20.02 % (4162917)Time elapsed: 0.202 s
% 134.27/20.02 % (4162917)Peak memory usage: 92 MB
% 134.27/20.02 % (4162917)Instructions burned: 320 (million)
% 134.27/20.02 % (4162919)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=273585770:i=2064:ep=RST_2914 on theBenchmark for (2914ds/2064Mi)
% 134.27/20.02 % (4162920)dis-1011_128_sil=32000:random_seed=1853265434:i=3706:ep=RST:av=off_2913 on theBenchmark for (2913ds/3706Mi)
% 134.27/20.02 % (4162919)Instruction limit reached!
% 134.27/20.02 % (4162919)------------------------------
% 134.27/20.02 % (4162919)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.27/20.02 % (4162919)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.27/20.02 % (4162919)CaDiCaL version: 2.1.3
% 134.27/20.02 % (4162919)Termination reason: Instruction limit
% 134.27/20.02 % (4162919)Termination phase: Saturation
% 134.27/20.02 % (4162919)Time elapsed: 1.142 s
% 134.27/20.02 % (4162919)Peak memory usage: 129 MB
% 134.27/20.02 % (4162919)Instructions burned: 2065 (million)
% 134.27/20.02 % (4162923)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=4005619912:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2901 on theBenchmark for (2901ds/757Mi)
% 134.27/20.02 % (4162923)Refutation not found, incomplete strategy
% 134.27/20.02 % (4162923)------------------------------
% 134.27/20.02 % (4162923)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.27/20.02 % (4162923)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.27/20.02 % (4162923)CaDiCaL version: 2.1.3
% 134.27/20.02 % (4162923)Termination reason: Refutation not found, incomplete strategy
% 134.27/20.02 % (4162923)Time elapsed: 0.005 s
% 134.27/20.02 % (4162923)Peak memory usage: 89 MB
% 134.27/20.02 % (4162923)Instructions burned: 5 (million)
% 134.27/20.02 % (4162903)Instruction limit reached!
% 134.27/20.02 % (4162903)------------------------------
% 134.27/20.02 % (4162903)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 134.27/20.02 % (4162903)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 134.27/20.02 % (4162903)CaDiCaL version: 2.1.3
% 134.27/20.02 % (4162903)Termination reason: Instruction limit
% 134.27/20.02 % (4162903)Termination phase: Saturation
% 134.27/20.02 % (4162903)Time elapsed: 6.945 s
% 134.27/20.02 % (4162903)Peak memory usage: 227 MB
% 134.27/20.02 % (4162903)Instructions burned: 14155 (million)
% 134.27/20.02 % (4162923)------------------------------
% 134.27/20.02 % (4162923)------------------------------
% 134.27/20.02 % (4162925)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=3482474012:i=13913:ss=axioms:sgt=8_2897 on theBenchmark for (2897ds/13913Mi)
% 162.45/23.79 % (4162926)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=3410627996:i=9925:aac=none_2896 on theBenchmark for (2896ds/9925Mi)
% 162.45/23.79 % (4162920)Instruction limit reached!
% 162.45/23.79 % (4162920)------------------------------
% 162.45/23.79 % (4162920)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 162.45/23.79 % (4162920)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.45/23.79 % (4162920)CaDiCaL version: 2.1.3
% 162.45/23.79 % (4162920)Termination reason: Instruction limit
% 162.45/23.79 % (4162920)Termination phase: Saturation
% 162.45/23.79 % (4162920)Time elapsed: 2.252 s
% 162.45/23.79 % (4162920)Peak memory usage: 104 MB
% 162.45/23.79 % (4162920)Instructions burned: 3706 (million)
% 162.45/23.79 % (4162929)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=2527541456:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2888 on theBenchmark for (2888ds/2479Mi)
% 162.45/23.79 % (4162929)Refutation not found, incomplete strategy
% 162.45/23.79 % (4162929)------------------------------
% 162.45/23.79 % (4162929)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 162.45/23.79 % (4162929)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.45/23.79 % (4162929)CaDiCaL version: 2.1.3
% 162.45/23.79 % (4162929)Termination reason: Refutation not found, incomplete strategy
% 162.45/23.79 % (4162929)Time elapsed: 0.005 s
% 162.45/23.79 % (4162929)Peak memory usage: 88 MB
% 162.45/23.79 % (4162929)Instructions burned: 6 (million)
% 162.45/23.79 % (4162929)------------------------------
% 162.45/23.79 % (4162929)------------------------------
% 162.45/23.79 % (4162931)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=18844145:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2884 on theBenchmark for (2884ds/440Mi)
% 162.45/23.79 % (4162931)Instruction limit reached!
% 162.45/23.79 % (4162931)------------------------------
% 162.45/23.79 % (4162931)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 162.45/23.79 % (4162931)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.45/23.79 % (4162931)CaDiCaL version: 2.1.3
% 162.45/23.79 % (4162931)Termination reason: Instruction limit
% 162.45/23.79 % (4162931)Termination phase: Saturation
% 162.45/23.79 % (4162931)Time elapsed: 0.237 s
% 162.45/23.79 % (4162931)Peak memory usage: 94 MB
% 162.45/23.79 % (4162931)Instructions burned: 442 (million)
% 162.45/23.79 % (4162933)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3631132567:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2880 on theBenchmark for (2880ds/11145Mi)
% 162.45/23.79 % (4162915)Instruction limit reached!
% 162.45/23.79 % (4162915)------------------------------
% 162.45/23.79 % (4162915)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 162.45/23.79 % (4162915)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.45/23.79 % (4162915)CaDiCaL version: 2.1.3
% 162.45/23.79 % (4162915)Termination reason: Instruction limit
% 162.45/23.79 % (4162915)Termination phase: Saturation
% 162.45/23.79 % (4162915)Time elapsed: 5.882 s
% 162.45/23.79 % (4162915)Peak memory usage: 234 MB
% 162.45/23.79 % (4162915)Instructions burned: 12111 (million)
% 162.45/23.79 % (4162935)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=4026772924:cts=off:i=3034:av=off:er=known:fsd=on_2874 on theBenchmark for (2874ds/3034Mi)
% 162.45/23.79 % (4162935)Instruction limit reached!
% 162.45/23.79 % (4162935)------------------------------
% 162.45/23.79 % (4162935)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 162.45/23.79 % (4162935)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 162.45/23.79 % (4162935)CaDiCaL version: 2.1.3
% 162.45/23.79 % (4162935)Termination reason: Instruction limit
% 162.45/23.79 % (4162935)Termination phase: Saturation
% 162.45/23.79 % (4162935)Time elapsed: 1.669 s
% 162.45/23.79 % (4162935)Peak memory usage: 144 MB
% 162.45/23.79 % (4162935)Instructions burned: 3035 (million)
% 162.45/23.79 % (4162937)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=154022975:st=2:s2a=on:i=524:s2at=2:ss=axioms_2855 on theBenchmark for (2855ds/524Mi)
% 162.45/23.79 % (4162937)Instruction limit reached!
% 162.45/23.79 % (4162937)------------------------------
% 162.45/23.79 % (4162937)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 191.46/27.85 % (4162937)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 191.46/27.85 % (4162937)CaDiCaL version: 2.1.3
% 191.46/27.85 % (4162937)Termination reason: Instruction limit
% 191.46/27.85 % (4162937)Termination phase: Saturation
% 191.46/27.85 % (4162937)Time elapsed: 0.269 s
% 191.46/27.85 % (4162937)Peak memory usage: 97 MB
% 191.46/27.85 % (4162937)Instructions burned: 524 (million)
% 191.46/27.85 % (4162939)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=3841960881:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2851 on theBenchmark for (2851ds/1016Mi)
% 191.46/27.85 % (4162939)Refutation not found, incomplete strategy
% 191.46/27.85 % (4162939)------------------------------
% 191.46/27.85 % (4162939)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 191.46/27.85 % (4162939)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 191.46/27.85 % (4162939)CaDiCaL version: 2.1.3
% 191.46/27.85 % (4162939)Termination reason: Refutation not found, incomplete strategy
% 191.46/27.85 % (4162939)Time elapsed: 0.003 s
% 191.46/27.85 % (4162939)Peak memory usage: 88 MB
% 191.46/27.85 % (4162939)Instructions burned: 3 (million)
% 191.46/27.85 % (4162939)------------------------------
% 191.46/27.85 % (4162939)------------------------------
% 191.46/27.85 % (4162941)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=40541579:i=14123:bd=preordered:ins=4_2847 on theBenchmark for (2847ds/14123Mi)
% 191.46/27.85 % (4162926)Instruction limit reached!
% 191.46/27.85 % (4162926)------------------------------
% 191.46/27.85 % (4162926)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 191.46/27.85 % (4162926)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 191.46/27.85 % (4162926)CaDiCaL version: 2.1.3
% 191.46/27.85 % (4162926)Termination reason: Instruction limit
% 191.46/27.85 % (4162926)Termination phase: Saturation
% 191.46/27.85 % (4162926)Time elapsed: 5.998 s
% 191.46/27.85 % (4162926)Peak memory usage: 183 MB
% 191.46/27.85 % (4162926)Instructions burned: 9925 (million)
% 191.46/27.85 % (4162943)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2460738888:i=5781:kws=precedence:bd=all:rawr=on_2834 on theBenchmark for (2834ds/5781Mi)
% 191.46/27.85 % (4162933)Instruction limit reached!
% 191.46/27.85 % (4162933)------------------------------
% 191.46/27.85 % (4162933)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 191.46/27.85 % (4162933)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 191.46/27.85 % (4162933)CaDiCaL version: 2.1.3
% 191.46/27.85 % (4162933)Termination reason: Instruction limit
% 191.46/27.85 % (4162933)Termination phase: Saturation
% 191.46/27.85 % (4162933)Time elapsed: 6.209 s
% 191.46/27.85 % (4162933)Peak memory usage: 194 MB
% 191.46/27.85 % (4162933)Instructions burned: 11147 (million)
% 191.46/27.85 % (4162945)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=3761859340:i=2448:gtgl=5:bd=preordered:gtg=all_2816 on theBenchmark for (2816ds/2448Mi)
% 191.46/27.85 % (4162925)Instruction limit reached!
% 191.46/27.85 % (4162925)------------------------------
% 191.46/27.85 % (4162925)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 191.46/27.85 % (4162925)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 191.46/27.85 % (4162925)CaDiCaL version: 2.1.3
% 191.46/27.85 % (4162925)Termination reason: Instruction limit
% 191.46/27.85 % (4162925)Termination phase: Saturation
% 191.46/27.85 % (4162925)Time elapsed: 8.110 s
% 191.46/27.85 % (4162925)Peak memory usage: 240 MB
% 191.46/27.85 % (4162925)Instructions burned: 13915 (million)
% 191.46/27.85 % (4162947)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=1278479071:i=3223:kws=precedence:fgj=on:av=off_2814 on theBenchmark for (2814ds/3223Mi)
% 191.46/27.85 % (4162943)Instruction limit reached!
% 191.46/27.85 % (4162943)------------------------------
% 191.46/27.85 % (4162943)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 191.46/27.85 % (4162943)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 191.46/27.85 % (4162943)CaDiCaL version: 2.1.3
% 191.46/27.85 % (4162943)Termination reason: Instruction limit
% 191.46/27.85 % (4162943)Termination phase: Saturation
% 191.46/27.85 % (4162943)Time elapsed: 2.271 s
% 191.46/27.85 % (4162943)Peak memory usage: 98 MB
% 191.46/27.85 % (4162943)Instructions burned: 5783 (million)
% 191.46/27.85 % (4162949)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3775812003:st=5.6:i=2033:sd=3:ss=axioms_2809 on theBenchmark for (2809ds/2033Mi)
% 105.21/30.69 % (4162949)Refutation not found, incomplete strategy
% 105.21/30.69 % (4162949)------------------------------
% 105.21/30.69 % (4162949)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.21/30.69 % (4162949)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.21/30.69 % (4162949)CaDiCaL version: 2.1.3
% 105.21/30.69 % (4162949)Termination reason: Refutation not found, incomplete strategy
% 105.21/30.69 % (4162949)Time elapsed: 0.629 s
% 105.21/30.69 % (4162949)Peak memory usage: 128 MB
% 105.21/30.69 % (4162949)Instructions burned: 914 (million)
% 105.21/30.69 % (4162945)Instruction limit reached!
% 105.21/30.69 % (4162945)------------------------------
% 105.21/30.69 % (4162945)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.21/30.69 % (4162945)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.21/30.69 % (4162945)CaDiCaL version: 2.1.3
% 105.21/30.69 % (4162945)Termination reason: Instruction limit
% 105.21/30.69 % (4162945)Termination phase: Saturation
% 105.21/30.69 % (4162945)Time elapsed: 1.375 s
% 105.21/30.69 % (4162945)Peak memory usage: 144 MB
% 105.21/30.69 % (4162945)Instructions burned: 2448 (million)
% 105.21/30.69 % (4162951)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=2292695175:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2801 on theBenchmark for (2801ds/2055Mi)
% 105.21/30.69 % (4162949)------------------------------
% 105.21/30.69 % (4162949)------------------------------
% 105.21/30.69 % (4162953)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=3312815088:i=21611:sd=3:ss=axioms_2799 on theBenchmark for (2799ds/21611Mi)
% 105.21/30.69 % (4162947)Instruction limit reached!
% 105.21/30.69 % (4162947)------------------------------
% 105.21/30.69 % (4162947)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.21/30.69 % (4162947)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.21/30.69 % (4162947)CaDiCaL version: 2.1.3
% 105.21/30.69 % (4162947)Termination reason: Instruction limit
% 105.21/30.69 % (4162947)Termination phase: Saturation
% 105.21/30.69 % (4162947)Time elapsed: 2.173 s
% 105.21/30.69 % (4162947)Peak memory usage: 147 MB
% 105.21/30.69 % (4162947)Instructions burned: 3223 (million)
% 105.21/30.69 % (4162955)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3571126072:i=4835:sd=13:ss=axioms:sgt=23_2791 on theBenchmark for (2791ds/4835Mi)
% 105.21/30.69 % (4162951)Instruction limit reached!
% 105.21/30.69 % (4162951)------------------------------
% 105.21/30.69 % (4162951)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.21/30.69 % (4162951)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.21/30.69 % (4162951)CaDiCaL version: 2.1.3
% 105.21/30.69 % (4162951)Termination reason: Instruction limit
% 105.21/30.69 % (4162951)Termination phase: Saturation
% 105.21/30.69 % (4162951)Time elapsed: 1.314 s
% 105.21/30.69 % (4162951)Peak memory usage: 138 MB
% 105.21/30.69 % (4162951)Instructions burned: 2056 (million)
% 105.21/30.69 % (4162957)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=1055041573:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2786 on theBenchmark for (2786ds/797Mi)
% 105.21/30.69 % (4162957)Instruction limit reached!
% 105.21/30.69 % (4162957)------------------------------
% 105.21/30.69 % (4162957)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.21/30.69 % (4162957)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.21/30.69 % (4162957)CaDiCaL version: 2.1.3
% 105.21/30.69 % (4162957)Termination reason: Instruction limit
% 105.21/30.69 % (4162957)Termination phase: Saturation
% 105.21/30.69 % (4162957)Time elapsed: 0.560 s
% 105.21/30.69 % (4162957)Peak memory usage: 106 MB
% 105.21/30.69 % (4162957)Instructions burned: 797 (million)
% 105.21/30.69 % (4162959)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=3837378516:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2779 on theBenchmark for (2779ds/2326Mi)
% 105.21/30.69 % (4162941)Instruction limit reached!
% 105.21/30.69 % (4162941)------------------------------
% 105.21/30.69 % (4162941)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.21/30.69 % (4162941)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.21/30.69 % (4162941)CaDiCaL version: 2.1.3
% 105.21/30.69 % (4162941)Termination reason: Instruction limit
% 105.21/30.69 % (4162941)Termination phase: Saturation
% 105.21/30.69 % (4162941)Time elapsed: 7.507 s
% 105.21/30.69 % (4162941)Peak memory usage: 208 MB
% 105.21/30.69 % (4162941)Instructions burned: 14124 (million)
% 105.21/30.69 % (4162961)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=3188325701:i=6038:nm=6_2770 on theBenchmark for (2770ds/6038Mi)
% 105.21/30.69 % (4162959)Instruction limit reached!
% 105.21/30.69 % (4162959)------------------------------
% 105.21/30.69 % (4162959)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.21/30.69 % (4162959)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.21/30.69 % (4162959)CaDiCaL version: 2.1.3
% 105.21/30.69 % (4162959)Termination reason: Instruction limit
% 105.21/30.69 % (4162959)Termination phase: Saturation
% 105.21/30.69 % (4162959)Time elapsed: 1.581 s
% 105.21/30.69 % (4162959)Peak memory usage: 105 MB
% 105.21/30.69 % (4162959)Instructions burned: 2327 (million)
% 105.21/30.69 % (4162955)Instruction limit reached!
% 105.21/30.69 % (4162955)------------------------------
% 105.21/30.69 % (4162955)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.21/30.69 % (4162955)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.21/30.69 % (4162955)CaDiCaL version: 2.1.3
% 105.21/30.69 % (4162955)Termination reason: Instruction limit
% 105.21/30.69 % (4162955)Termination phase: Saturation
% 105.21/30.69 % (4162955)Time elapsed: 2.882 s
% 105.21/30.69 % (4162955)Peak memory usage: 126 MB
% 105.21/30.69 % (4162955)Instructions burned: 4835 (million)
% 105.21/30.69 % (4162963)lrs+10_1_sil=32000:sp=occurrence:random_seed=4183793526:st=2:i=33334:sd=3:ss=included:sgt=32_2761 on theBenchmark for (2761ds/33334Mi)
% 105.21/30.69 % (4162964)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=2458394546:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2760 on theBenchmark for (2760ds/1008Mi)
% 105.21/30.69 % (4162964)Instruction limit reached!
% 105.21/30.69 % (4162964)------------------------------
% 105.21/30.69 % (4162964)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.21/30.69 % (4162964)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.21/30.69 % (4162964)CaDiCaL version: 2.1.3
% 105.21/30.69 % (4162964)Termination reason: Instruction limit
% 105.21/30.69 % (4162964)Termination phase: Saturation
% 105.21/30.69 % (4162964)Time elapsed: 0.487 s
% 105.21/30.69 % (4162964)Peak memory usage: 96 MB
% 105.21/30.69 % (4162964)Instructions burned: 1010 (million)
% 105.21/30.69 % (4162967)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=695148556:i=8327:s2at=5:bd=preordered_2753 on theBenchmark for (2753ds/8327Mi)
% 105.21/30.69 % (4162961)Instruction limit reached!
% 105.21/30.69 % (4162961)------------------------------
% 105.21/30.69 % (4162961)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.21/30.69 % (4162961)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.21/30.69 % (4162961)CaDiCaL version: 2.1.3
% 105.21/30.69 % (4162961)Termination reason: Instruction limit
% 105.21/30.69 % (4162961)Termination phase: Saturation
% 105.21/30.69 % (4162961)Time elapsed: 3.031 s
% 105.21/30.69 % (4162961)Peak memory usage: 169 MB
% 105.21/30.69 % (4162961)Instructions burned: 6040 (million)
% 105.21/30.69 % (4162969)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=3683415227:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2738 on theBenchmark for (2738ds/1083Mi)
% 105.21/30.69 % (4162969)Instruction limit reached!
% 105.21/30.69 % (4162969)------------------------------
% 105.21/30.69 % (4162969)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.21/30.69 % (4162969)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.21/30.69 % (4162969)CaDiCaL version: 2.1.3
% 105.21/30.69 % (4162969)Termination reason: Instruction limit
% 105.21/30.69 % (4162969)Termination phase: Saturation
% 105.21/30.69 % (4162969)Time elapsed: 0.500 s
% 105.21/30.69 % (4162969)Peak memory usage: 103 MB
% 105.21/30.69 % (4162969)Instructions burned: 1084 (million)
% 105.21/30.69 % (4162971)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=264162885:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2731 on theBenchmark for (2731ds/1084Mi)
% 105.21/30.69 % (4162971)Instruction limit reached!
% 105.21/30.69 % (4162971)------------------------------
% 105.21/30.69 % (4162971)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.21/30.69 % (4162971)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.21/30.69 % (4162971)CaDiCaL version: 2.1.3
% 105.21/30.69 % (4162971)Termination reason: Instruction limit
% 105.21/30.69 % (4162971)Termination phase: Saturation
% 105.21/30.69 % (4162971)Time elapsed: 0.562 s
% 105.21/30.69 % (4162971)Peak memory usage: 96 MB
% 105.21/30.69 % (4162971)Instructions burned: 1085 (million)
% 105.21/30.69 % (4162973)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=3852529318:i=6995:s2at=5:gtg=all_2724 on theBenchmark for (2724ds/6995Mi)
% 105.21/30.69 % (4162973)First to succeed.
% 105.21/30.69 % (4162973)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-4162842"
% 105.21/30.69 % (4162967)Instruction limit reached!
% 105.21/30.69 % (4162967)------------------------------
% 105.21/30.69 % (4162967)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 105.21/30.69 % (4162967)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 105.21/30.69 % (4162967)CaDiCaL version: 2.1.3
% 105.21/30.69 % (4162967)Termination reason: Instruction limit
% 105.21/30.69 % (4162967)Termination phase: Saturation
% 105.21/30.69 % (4162967)Time elapsed: 4.857 s
% 105.21/30.69 % (4162967)Peak memory usage: 191 MB
% 105.21/30.69 % (4162967)Instructions burned: 8329 (million)
% 105.21/30.69 % (4162973)Refutation found. Thanks to Tanya!
% 105.21/30.69 % SZS status Theorem for theBenchmark
% 105.21/30.69 % SZS output start Proof for theBenchmark
% See solution above
% 211.73/30.89 % (4162973)------------------------------
% 211.73/30.89 % (4162973)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 211.73/30.89 % (4162973)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 211.73/30.89 % (4162973)CaDiCaL version: 2.1.3
% 211.73/30.89 % (4162973)Termination reason: Refutation
% 211.73/30.89 % (4162973)Time elapsed: 1.730 s
% 211.73/30.89 % (4162973)Peak memory usage: 144 MB
% 211.73/30.89 % (4162973)Instructions burned: 2888 (million)
% 211.73/30.89 % (4162973)------------------------------
% 211.73/30.89 % (4162973)------------------------------
% 211.73/30.89 % (4162842)Success in time 29.84 s
% 211.73/30.89 % Vampire exiting
%------------------------------------------------------------------------------