%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : BIO003+1 : TPTP v9.3.1. Bugfixed v6.4.1.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : n026.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 09:35:14 AM UTC 2026
% Result : Theorem 172.35s 31.43s
% Output : Refutation 188.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 19
% Number of leaves : 4
% Syntax : Number of formulae : 30 ( 9 unt; 1 def)
% Number of atoms : 1437 ( 234 equ)
% Maximal formula atoms : 91 ( 47 avg)
% Number of connectives : 1417 ( 10 ~; 6 |;1386 &)
% ( 0 <=>; 15 =>; 0 <=; 0 <~>)
% Maximal formula depth : 92 ( 49 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 53 ( 51 usr; 1 prp; 0-4 aty)
% Number of functors : 46 ( 42 usr; 16 con; 0-1 aty)
% Number of variables : 21 ( 21 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f3477,axiom,
! [X0] :
( cell_1(X0)
=> ( original_name_2(X0,'Cell')
& description_2(X0,'The basic unit from which living organisms are made, consisting of an aqueous solution of organic molecules enclosed by a membrane. All cells arise from existing cells, usually by a process of division into two. (Alberts:ECB:G-3).')
& user_description_2(X0,'The basic unit from which living organisms are made.')
& concept2words_2(X0,cell)
& living_entity_1(X0)
& cell_pole_1(fn_cell_1(X0))
& cytoskeleton_1(fn_cell_2(X0))
& surface_1(fn_cell_4(X0))
& shape_value_1(fn_cell_5(X0))
& specific_surface_area_value_1(fn_cell_7(X0))
& motor_protein_1(fn_cell_8(X0))
& protein_enzyme_1(fn_cell_9(X0))
& size_value_1(fn_cell_11(X0))
& structural_complexity_value_1(fn_cell_13(X0))
& ribosome_1(fn_cell_14(X0))
& length_value_1(fn_cell_18(X0))
& length_value_1(fn_cell_19(X0))
& length_value_1(fn_cell_20(X0))
& membrane_potential_1(fn_cell_21(X0))
& volume_value_1(fn_cell_22(X0))
& genome_1(fn_cell_24(X0))
& chromosome_1(fn_cell_25(X0))
& tangible_entity_1(fn_cell_26(X0))
& phospholipid_bilayer_1(fn_cell_26(X0))
& surface_1(fn_cell_27(X0))
& cytoplasmic_side_1(fn_cell_27(X0))
& mixture_1(fn_cell_28(X0))
& cytoplasm_1(fn_cell_28(X0))
& substance_1(fn_cell_29(X0))
& cytosol_1(fn_cell_29(X0))
& plasma_membrane_1(fn_cell_30(X0))
& cell_1(fn_cytoplasm_7(fn_cell_28(X0)))
& cytoplasm_1(fn_cytoplasmic_side_1(fn_cell_27(X0)))
& substance_1(fn_mixture_1(fn_cell_28(X0)))
& cytosol_1(fn_cytoplasm_8(fn_cell_28(X0)))
& tangible_entity_1(fn_biomembrane_63(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_biomembrane_63(fn_cell_30(X0)))
& tangible_entity_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& surface_1(fn_biomembrane_47(fn_cell_30(X0)))
& cytoplasmic_side_1(fn_plasma_membrane_66(fn_cell_30(X0)))
& is_across_2(fn_cell_21(X0),fn_cell_30(X0))
& shape_2(X0,fn_cell_5(X0))
& specific_surface_area_2(X0,fn_cell_7(X0))
& size_2(X0,fn_cell_11(X0))
& structural_complexity_2(X0,fn_cell_13(X0))
& diameter_2(X0,fn_cell_18(X0))
& volume_2(X0,fn_cell_22(X0))
& exactCardinality(X0,has_region_0,"2",cell_pole_0)
& has_region_2(X0,fn_cell_1(X0))
& has_region_2(X0,fn_cell_4(X0))
& minCardinality(X0,has_part_0,"1",chromosome_0)
& has_part_2(X0,fn_cell_2(X0))
& has_part_2(X0,fn_cell_25(X0))
& has_part_2(X0,fn_cell_24(X0))
& has_part_2(X0,fn_cell_8(X0))
& has_part_2(X0,fn_cell_14(X0))
& has_part_2(X0,fn_cell_30(X0))
& is_inside_2(fn_cell_28(X0),fn_cell_30(X0))
& has_part_2(fn_cell_28(X0),fn_cell_9(X0))
& the_cardinal_value_2(fn_cell_20(X0),"100.0e0")
& cardinal_unit_class_2(fn_cell_20(X0),micrometer_0)
& greater_than_or_equal_to_2(fn_cell_20(X0),fn_cell_18(X0))
& the_cardinal_value_2(fn_cell_19(X0),"0.1e0")
& cardinal_unit_class_2(fn_cell_19(X0),micrometer_0)
& greater_than_or_equal_to_2(fn_cell_18(X0),fn_cell_19(X0))
& is_inside_2(fn_cell_14(X0),fn_cell_29(X0))
& the_scalar_value_2(fn_cell_13(X0),simple_0)
& scalar_unit_class_2(fn_cell_13(X0),organism_0)
& directly_proportional_2(fn_cell_11(X0),fn_cell_22(X0))
& is_oriented_toward_2(fn_cell_27(X0),fn_cell_28(X0))
& is_at_2(fn_cell_26(X0),fn_cell_4(X0))
& has_part_2(X0,fn_cell_28(X0))
& has_part_2(fn_cell_28(X0),fn_cell_29(X0))
& has_region_2(fn_cell_30(X0),fn_cell_27(X0))
& has_part_2(fn_cell_30(X0),fn_cell_26(X0))
& is_facing_2(fn_cell_27(X0),fn_cell_28(X0))
& X0 = fn_cytoplasm_7(fn_cell_28(X0))
& fn_cell_29(X0) = fn_mixture_1(fn_cell_28(X0))
& fn_cell_29(X0) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cell_27(X0) = fn_biomembrane_47(fn_cell_30(X0))
& fn_cell_27(X0) = fn_plasma_membrane_66(fn_cell_30(X0))
& fn_cell_26(X0) = fn_biomembrane_63(fn_cell_30(X0))
& fn_cell_26(X0) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_cell_28(X0) = fn_cytoplasmic_side_1(fn_cell_27(X0))
& fn_mixture_1(fn_cell_28(X0)) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cytoplasm_8(fn_cell_28(X0)) = fn_biomembrane_63(fn_cell_30(X0))
& fn_biomembrane_63(fn_cell_30(X0)) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_plasma_membrane_71(fn_cell_30(X0)) = fn_biomembrane_47(fn_cell_30(X0))
& fn_biomembrane_47(fn_cell_30(X0)) = fn_plasma_membrane_66(fn_cell_30(X0)) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a528132) ).
fof(f9161,axiom,
cell_1(a_cell),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_cell) ).
fof(f9162,conjecture,
cytoskeleton_1(fn_cell_2(a_cell)),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',ask) ).
fof(f9163,negated_conjecture,
~ cytoskeleton_1(fn_cell_2(a_cell)),
inference(negated_conjecture,[status(cth)],[f9162]) ).
fof(f9164,plain,
~ cytoskeleton_1(fn_cell_2(a_cell)),
inference(flattening,[],[f9163]) ).
fof(f16952,plain,
! [X0] :
( cell_1(X0)
=> ( original_name_2(X0,'Cell')
& description_2(X0,'The basic unit from which living organisms are made, consisting of an aqueous solution of organic molecules enclosed by a membrane. All cells arise from existing cells, usually by a process of division into two. (Alberts:ECB:G-3).')
& user_description_2(X0,'The basic unit from which living organisms are made.')
& concept2words_2(X0,cell)
& living_entity_1(X0)
& cell_pole_1(fn_cell_1(X0))
& cytoskeleton_1(fn_cell_2(X0))
& shape_value_1(fn_cell_5(X0))
& specific_surface_area_value_1(fn_cell_7(X0))
& motor_protein_1(fn_cell_8(X0))
& protein_enzyme_1(fn_cell_9(X0))
& size_value_1(fn_cell_11(X0))
& structural_complexity_value_1(fn_cell_13(X0))
& ribosome_1(fn_cell_14(X0))
& length_value_1(fn_cell_18(X0))
& length_value_1(fn_cell_19(X0))
& length_value_1(fn_cell_20(X0))
& membrane_potential_1(fn_cell_21(X0))
& volume_value_1(fn_cell_22(X0))
& genome_1(fn_cell_24(X0))
& chromosome_1(fn_cell_25(X0))
& tangible_entity_1(fn_cell_26(X0))
& phospholipid_bilayer_1(fn_cell_26(X0))
& cytoplasmic_side_1(fn_cell_27(X0))
& mixture_1(fn_cell_28(X0))
& cytoplasm_1(fn_cell_28(X0))
& substance_1(fn_cell_29(X0))
& cytosol_1(fn_cell_29(X0))
& plasma_membrane_1(fn_cell_30(X0))
& cell_1(fn_cytoplasm_7(fn_cell_28(X0)))
& cytoplasm_1(fn_cytoplasmic_side_1(fn_cell_27(X0)))
& substance_1(fn_mixture_1(fn_cell_28(X0)))
& cytosol_1(fn_cytoplasm_8(fn_cell_28(X0)))
& tangible_entity_1(fn_biomembrane_63(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_biomembrane_63(fn_cell_30(X0)))
& tangible_entity_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& cytoplasmic_side_1(fn_plasma_membrane_66(fn_cell_30(X0)))
& is_across_2(fn_cell_21(X0),fn_cell_30(X0))
& shape_2(X0,fn_cell_5(X0))
& specific_surface_area_2(X0,fn_cell_7(X0))
& size_2(X0,fn_cell_11(X0))
& structural_complexity_2(X0,fn_cell_13(X0))
& diameter_2(X0,fn_cell_18(X0))
& volume_2(X0,fn_cell_22(X0))
& exactCardinality(X0,has_region_0,"2",cell_pole_0)
& has_region_2(X0,fn_cell_1(X0))
& has_region_2(X0,fn_cell_4(X0))
& minCardinality(X0,has_part_0,"1",chromosome_0)
& has_part_2(X0,fn_cell_2(X0))
& has_part_2(X0,fn_cell_25(X0))
& has_part_2(X0,fn_cell_24(X0))
& has_part_2(X0,fn_cell_8(X0))
& has_part_2(X0,fn_cell_14(X0))
& has_part_2(X0,fn_cell_30(X0))
& is_inside_2(fn_cell_28(X0),fn_cell_30(X0))
& has_part_2(fn_cell_28(X0),fn_cell_9(X0))
& the_cardinal_value_2(fn_cell_20(X0),"100.0e0")
& cardinal_unit_class_2(fn_cell_20(X0),micrometer_0)
& greater_than_or_equal_to_2(fn_cell_20(X0),fn_cell_18(X0))
& the_cardinal_value_2(fn_cell_19(X0),"0.1e0")
& cardinal_unit_class_2(fn_cell_19(X0),micrometer_0)
& greater_than_or_equal_to_2(fn_cell_18(X0),fn_cell_19(X0))
& is_inside_2(fn_cell_14(X0),fn_cell_29(X0))
& the_scalar_value_2(fn_cell_13(X0),simple_0)
& scalar_unit_class_2(fn_cell_13(X0),organism_0)
& directly_proportional_2(fn_cell_11(X0),fn_cell_22(X0))
& is_oriented_toward_2(fn_cell_27(X0),fn_cell_28(X0))
& is_at_2(fn_cell_26(X0),fn_cell_4(X0))
& has_part_2(X0,fn_cell_28(X0))
& has_part_2(fn_cell_28(X0),fn_cell_29(X0))
& has_region_2(fn_cell_30(X0),fn_cell_27(X0))
& has_part_2(fn_cell_30(X0),fn_cell_26(X0))
& is_facing_2(fn_cell_27(X0),fn_cell_28(X0))
& X0 = fn_cytoplasm_7(fn_cell_28(X0))
& fn_cell_29(X0) = fn_mixture_1(fn_cell_28(X0))
& fn_cell_29(X0) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cell_27(X0) = fn_biomembrane_47(fn_cell_30(X0))
& fn_cell_27(X0) = fn_plasma_membrane_66(fn_cell_30(X0))
& fn_cell_26(X0) = fn_biomembrane_63(fn_cell_30(X0))
& fn_cell_26(X0) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_cell_28(X0) = fn_cytoplasmic_side_1(fn_cell_27(X0))
& fn_mixture_1(fn_cell_28(X0)) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cytoplasm_8(fn_cell_28(X0)) = fn_biomembrane_63(fn_cell_30(X0))
& fn_biomembrane_63(fn_cell_30(X0)) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_plasma_membrane_71(fn_cell_30(X0)) = fn_biomembrane_47(fn_cell_30(X0))
& fn_biomembrane_47(fn_cell_30(X0)) = fn_plasma_membrane_66(fn_cell_30(X0)) ) ),
inference(pure_predicate_removal,[],[f3477]) ).
fof(f17806,plain,
! [X0] :
( cell_1(X0)
=> ( original_name_2(X0,'Cell')
& description_2(X0,'The basic unit from which living organisms are made, consisting of an aqueous solution of organic molecules enclosed by a membrane. All cells arise from existing cells, usually by a process of division into two. (Alberts:ECB:G-3).')
& user_description_2(X0,'The basic unit from which living organisms are made.')
& concept2words_2(X0,cell)
& living_entity_1(X0)
& cell_pole_1(fn_cell_1(X0))
& cytoskeleton_1(fn_cell_2(X0))
& shape_value_1(fn_cell_5(X0))
& specific_surface_area_value_1(fn_cell_7(X0))
& motor_protein_1(fn_cell_8(X0))
& protein_enzyme_1(fn_cell_9(X0))
& size_value_1(fn_cell_11(X0))
& structural_complexity_value_1(fn_cell_13(X0))
& ribosome_1(fn_cell_14(X0))
& length_value_1(fn_cell_18(X0))
& length_value_1(fn_cell_19(X0))
& length_value_1(fn_cell_20(X0))
& membrane_potential_1(fn_cell_21(X0))
& volume_value_1(fn_cell_22(X0))
& genome_1(fn_cell_24(X0))
& chromosome_1(fn_cell_25(X0))
& tangible_entity_1(fn_cell_26(X0))
& phospholipid_bilayer_1(fn_cell_26(X0))
& cytoplasmic_side_1(fn_cell_27(X0))
& mixture_1(fn_cell_28(X0))
& cytoplasm_1(fn_cell_28(X0))
& substance_1(fn_cell_29(X0))
& cytosol_1(fn_cell_29(X0))
& plasma_membrane_1(fn_cell_30(X0))
& cell_1(fn_cytoplasm_7(fn_cell_28(X0)))
& cytoplasm_1(fn_cytoplasmic_side_1(fn_cell_27(X0)))
& substance_1(fn_mixture_1(fn_cell_28(X0)))
& cytosol_1(fn_cytoplasm_8(fn_cell_28(X0)))
& tangible_entity_1(fn_biomembrane_63(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_biomembrane_63(fn_cell_30(X0)))
& tangible_entity_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& cytoplasmic_side_1(fn_plasma_membrane_66(fn_cell_30(X0)))
& is_across_2(fn_cell_21(X0),fn_cell_30(X0))
& shape_2(X0,fn_cell_5(X0))
& specific_surface_area_2(X0,fn_cell_7(X0))
& size_2(X0,fn_cell_11(X0))
& structural_complexity_2(X0,fn_cell_13(X0))
& diameter_2(X0,fn_cell_18(X0))
& volume_2(X0,fn_cell_22(X0))
& exactCardinality(X0,has_region_0,"2",cell_pole_0)
& has_region_2(X0,fn_cell_1(X0))
& has_region_2(X0,fn_cell_4(X0))
& minCardinality(X0,has_part_0,"1",chromosome_0)
& has_part_2(X0,fn_cell_2(X0))
& has_part_2(X0,fn_cell_25(X0))
& has_part_2(X0,fn_cell_24(X0))
& has_part_2(X0,fn_cell_8(X0))
& has_part_2(X0,fn_cell_14(X0))
& has_part_2(X0,fn_cell_30(X0))
& is_inside_2(fn_cell_28(X0),fn_cell_30(X0))
& has_part_2(fn_cell_28(X0),fn_cell_9(X0))
& the_cardinal_value_2(fn_cell_20(X0),"100.0e0")
& cardinal_unit_class_2(fn_cell_20(X0),micrometer_0)
& greater_than_or_equal_to_2(fn_cell_20(X0),fn_cell_18(X0))
& the_cardinal_value_2(fn_cell_19(X0),"0.1e0")
& cardinal_unit_class_2(fn_cell_19(X0),micrometer_0)
& greater_than_or_equal_to_2(fn_cell_18(X0),fn_cell_19(X0))
& is_inside_2(fn_cell_14(X0),fn_cell_29(X0))
& the_scalar_value_2(fn_cell_13(X0),simple_0)
& directly_proportional_2(fn_cell_11(X0),fn_cell_22(X0))
& is_oriented_toward_2(fn_cell_27(X0),fn_cell_28(X0))
& is_at_2(fn_cell_26(X0),fn_cell_4(X0))
& has_part_2(X0,fn_cell_28(X0))
& has_part_2(fn_cell_28(X0),fn_cell_29(X0))
& has_region_2(fn_cell_30(X0),fn_cell_27(X0))
& has_part_2(fn_cell_30(X0),fn_cell_26(X0))
& is_facing_2(fn_cell_27(X0),fn_cell_28(X0))
& X0 = fn_cytoplasm_7(fn_cell_28(X0))
& fn_cell_29(X0) = fn_mixture_1(fn_cell_28(X0))
& fn_cell_29(X0) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cell_27(X0) = fn_biomembrane_47(fn_cell_30(X0))
& fn_cell_27(X0) = fn_plasma_membrane_66(fn_cell_30(X0))
& fn_cell_26(X0) = fn_biomembrane_63(fn_cell_30(X0))
& fn_cell_26(X0) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_cell_28(X0) = fn_cytoplasmic_side_1(fn_cell_27(X0))
& fn_mixture_1(fn_cell_28(X0)) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cytoplasm_8(fn_cell_28(X0)) = fn_biomembrane_63(fn_cell_30(X0))
& fn_biomembrane_63(fn_cell_30(X0)) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_plasma_membrane_71(fn_cell_30(X0)) = fn_biomembrane_47(fn_cell_30(X0))
& fn_biomembrane_47(fn_cell_30(X0)) = fn_plasma_membrane_66(fn_cell_30(X0)) ) ),
inference(pure_predicate_removal,[],[f16952]) ).
fof(f19084,plain,
! [X0] :
( cell_1(X0)
=> ( original_name_2(X0,'Cell')
& user_description_2(X0,'The basic unit from which living organisms are made.')
& concept2words_2(X0,cell)
& living_entity_1(X0)
& cell_pole_1(fn_cell_1(X0))
& cytoskeleton_1(fn_cell_2(X0))
& shape_value_1(fn_cell_5(X0))
& specific_surface_area_value_1(fn_cell_7(X0))
& motor_protein_1(fn_cell_8(X0))
& protein_enzyme_1(fn_cell_9(X0))
& size_value_1(fn_cell_11(X0))
& structural_complexity_value_1(fn_cell_13(X0))
& ribosome_1(fn_cell_14(X0))
& length_value_1(fn_cell_18(X0))
& length_value_1(fn_cell_19(X0))
& length_value_1(fn_cell_20(X0))
& membrane_potential_1(fn_cell_21(X0))
& volume_value_1(fn_cell_22(X0))
& genome_1(fn_cell_24(X0))
& chromosome_1(fn_cell_25(X0))
& tangible_entity_1(fn_cell_26(X0))
& phospholipid_bilayer_1(fn_cell_26(X0))
& cytoplasmic_side_1(fn_cell_27(X0))
& mixture_1(fn_cell_28(X0))
& cytoplasm_1(fn_cell_28(X0))
& substance_1(fn_cell_29(X0))
& cytosol_1(fn_cell_29(X0))
& plasma_membrane_1(fn_cell_30(X0))
& cell_1(fn_cytoplasm_7(fn_cell_28(X0)))
& cytoplasm_1(fn_cytoplasmic_side_1(fn_cell_27(X0)))
& substance_1(fn_mixture_1(fn_cell_28(X0)))
& cytosol_1(fn_cytoplasm_8(fn_cell_28(X0)))
& tangible_entity_1(fn_biomembrane_63(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_biomembrane_63(fn_cell_30(X0)))
& tangible_entity_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& cytoplasmic_side_1(fn_plasma_membrane_66(fn_cell_30(X0)))
& is_across_2(fn_cell_21(X0),fn_cell_30(X0))
& shape_2(X0,fn_cell_5(X0))
& specific_surface_area_2(X0,fn_cell_7(X0))
& size_2(X0,fn_cell_11(X0))
& structural_complexity_2(X0,fn_cell_13(X0))
& diameter_2(X0,fn_cell_18(X0))
& volume_2(X0,fn_cell_22(X0))
& exactCardinality(X0,has_region_0,"2",cell_pole_0)
& has_region_2(X0,fn_cell_1(X0))
& has_region_2(X0,fn_cell_4(X0))
& minCardinality(X0,has_part_0,"1",chromosome_0)
& has_part_2(X0,fn_cell_2(X0))
& has_part_2(X0,fn_cell_25(X0))
& has_part_2(X0,fn_cell_24(X0))
& has_part_2(X0,fn_cell_8(X0))
& has_part_2(X0,fn_cell_14(X0))
& has_part_2(X0,fn_cell_30(X0))
& is_inside_2(fn_cell_28(X0),fn_cell_30(X0))
& has_part_2(fn_cell_28(X0),fn_cell_9(X0))
& the_cardinal_value_2(fn_cell_20(X0),"100.0e0")
& cardinal_unit_class_2(fn_cell_20(X0),micrometer_0)
& greater_than_or_equal_to_2(fn_cell_20(X0),fn_cell_18(X0))
& the_cardinal_value_2(fn_cell_19(X0),"0.1e0")
& cardinal_unit_class_2(fn_cell_19(X0),micrometer_0)
& greater_than_or_equal_to_2(fn_cell_18(X0),fn_cell_19(X0))
& is_inside_2(fn_cell_14(X0),fn_cell_29(X0))
& the_scalar_value_2(fn_cell_13(X0),simple_0)
& directly_proportional_2(fn_cell_11(X0),fn_cell_22(X0))
& is_oriented_toward_2(fn_cell_27(X0),fn_cell_28(X0))
& is_at_2(fn_cell_26(X0),fn_cell_4(X0))
& has_part_2(X0,fn_cell_28(X0))
& has_part_2(fn_cell_28(X0),fn_cell_29(X0))
& has_region_2(fn_cell_30(X0),fn_cell_27(X0))
& has_part_2(fn_cell_30(X0),fn_cell_26(X0))
& is_facing_2(fn_cell_27(X0),fn_cell_28(X0))
& X0 = fn_cytoplasm_7(fn_cell_28(X0))
& fn_cell_29(X0) = fn_mixture_1(fn_cell_28(X0))
& fn_cell_29(X0) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cell_27(X0) = fn_biomembrane_47(fn_cell_30(X0))
& fn_cell_27(X0) = fn_plasma_membrane_66(fn_cell_30(X0))
& fn_cell_26(X0) = fn_biomembrane_63(fn_cell_30(X0))
& fn_cell_26(X0) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_cell_28(X0) = fn_cytoplasmic_side_1(fn_cell_27(X0))
& fn_mixture_1(fn_cell_28(X0)) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cytoplasm_8(fn_cell_28(X0)) = fn_biomembrane_63(fn_cell_30(X0))
& fn_biomembrane_63(fn_cell_30(X0)) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_plasma_membrane_71(fn_cell_30(X0)) = fn_biomembrane_47(fn_cell_30(X0))
& fn_biomembrane_47(fn_cell_30(X0)) = fn_plasma_membrane_66(fn_cell_30(X0)) ) ),
inference(pure_predicate_removal,[],[f17806]) ).
fof(f20092,plain,
! [X0] :
( cell_1(X0)
=> ( original_name_2(X0,'Cell')
& user_description_2(X0,'The basic unit from which living organisms are made.')
& living_entity_1(X0)
& cell_pole_1(fn_cell_1(X0))
& cytoskeleton_1(fn_cell_2(X0))
& shape_value_1(fn_cell_5(X0))
& specific_surface_area_value_1(fn_cell_7(X0))
& motor_protein_1(fn_cell_8(X0))
& protein_enzyme_1(fn_cell_9(X0))
& size_value_1(fn_cell_11(X0))
& structural_complexity_value_1(fn_cell_13(X0))
& ribosome_1(fn_cell_14(X0))
& length_value_1(fn_cell_18(X0))
& length_value_1(fn_cell_19(X0))
& length_value_1(fn_cell_20(X0))
& membrane_potential_1(fn_cell_21(X0))
& volume_value_1(fn_cell_22(X0))
& genome_1(fn_cell_24(X0))
& chromosome_1(fn_cell_25(X0))
& tangible_entity_1(fn_cell_26(X0))
& phospholipid_bilayer_1(fn_cell_26(X0))
& cytoplasmic_side_1(fn_cell_27(X0))
& mixture_1(fn_cell_28(X0))
& cytoplasm_1(fn_cell_28(X0))
& substance_1(fn_cell_29(X0))
& cytosol_1(fn_cell_29(X0))
& plasma_membrane_1(fn_cell_30(X0))
& cell_1(fn_cytoplasm_7(fn_cell_28(X0)))
& cytoplasm_1(fn_cytoplasmic_side_1(fn_cell_27(X0)))
& substance_1(fn_mixture_1(fn_cell_28(X0)))
& cytosol_1(fn_cytoplasm_8(fn_cell_28(X0)))
& tangible_entity_1(fn_biomembrane_63(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_biomembrane_63(fn_cell_30(X0)))
& tangible_entity_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& cytoplasmic_side_1(fn_plasma_membrane_66(fn_cell_30(X0)))
& is_across_2(fn_cell_21(X0),fn_cell_30(X0))
& shape_2(X0,fn_cell_5(X0))
& specific_surface_area_2(X0,fn_cell_7(X0))
& size_2(X0,fn_cell_11(X0))
& structural_complexity_2(X0,fn_cell_13(X0))
& diameter_2(X0,fn_cell_18(X0))
& volume_2(X0,fn_cell_22(X0))
& exactCardinality(X0,has_region_0,"2",cell_pole_0)
& has_region_2(X0,fn_cell_1(X0))
& has_region_2(X0,fn_cell_4(X0))
& minCardinality(X0,has_part_0,"1",chromosome_0)
& has_part_2(X0,fn_cell_2(X0))
& has_part_2(X0,fn_cell_25(X0))
& has_part_2(X0,fn_cell_24(X0))
& has_part_2(X0,fn_cell_8(X0))
& has_part_2(X0,fn_cell_14(X0))
& has_part_2(X0,fn_cell_30(X0))
& is_inside_2(fn_cell_28(X0),fn_cell_30(X0))
& has_part_2(fn_cell_28(X0),fn_cell_9(X0))
& the_cardinal_value_2(fn_cell_20(X0),"100.0e0")
& cardinal_unit_class_2(fn_cell_20(X0),micrometer_0)
& greater_than_or_equal_to_2(fn_cell_20(X0),fn_cell_18(X0))
& the_cardinal_value_2(fn_cell_19(X0),"0.1e0")
& cardinal_unit_class_2(fn_cell_19(X0),micrometer_0)
& greater_than_or_equal_to_2(fn_cell_18(X0),fn_cell_19(X0))
& is_inside_2(fn_cell_14(X0),fn_cell_29(X0))
& the_scalar_value_2(fn_cell_13(X0),simple_0)
& directly_proportional_2(fn_cell_11(X0),fn_cell_22(X0))
& is_oriented_toward_2(fn_cell_27(X0),fn_cell_28(X0))
& is_at_2(fn_cell_26(X0),fn_cell_4(X0))
& has_part_2(X0,fn_cell_28(X0))
& has_part_2(fn_cell_28(X0),fn_cell_29(X0))
& has_region_2(fn_cell_30(X0),fn_cell_27(X0))
& has_part_2(fn_cell_30(X0),fn_cell_26(X0))
& is_facing_2(fn_cell_27(X0),fn_cell_28(X0))
& X0 = fn_cytoplasm_7(fn_cell_28(X0))
& fn_cell_29(X0) = fn_mixture_1(fn_cell_28(X0))
& fn_cell_29(X0) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cell_27(X0) = fn_biomembrane_47(fn_cell_30(X0))
& fn_cell_27(X0) = fn_plasma_membrane_66(fn_cell_30(X0))
& fn_cell_26(X0) = fn_biomembrane_63(fn_cell_30(X0))
& fn_cell_26(X0) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_cell_28(X0) = fn_cytoplasmic_side_1(fn_cell_27(X0))
& fn_mixture_1(fn_cell_28(X0)) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cytoplasm_8(fn_cell_28(X0)) = fn_biomembrane_63(fn_cell_30(X0))
& fn_biomembrane_63(fn_cell_30(X0)) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_plasma_membrane_71(fn_cell_30(X0)) = fn_biomembrane_47(fn_cell_30(X0))
& fn_biomembrane_47(fn_cell_30(X0)) = fn_plasma_membrane_66(fn_cell_30(X0)) ) ),
inference(pure_predicate_removal,[],[f19084]) ).
fof(f22068,plain,
! [X0] :
( cell_1(X0)
=> ( original_name_2(X0,'Cell')
& living_entity_1(X0)
& cell_pole_1(fn_cell_1(X0))
& cytoskeleton_1(fn_cell_2(X0))
& shape_value_1(fn_cell_5(X0))
& specific_surface_area_value_1(fn_cell_7(X0))
& motor_protein_1(fn_cell_8(X0))
& protein_enzyme_1(fn_cell_9(X0))
& size_value_1(fn_cell_11(X0))
& structural_complexity_value_1(fn_cell_13(X0))
& ribosome_1(fn_cell_14(X0))
& length_value_1(fn_cell_18(X0))
& length_value_1(fn_cell_19(X0))
& length_value_1(fn_cell_20(X0))
& membrane_potential_1(fn_cell_21(X0))
& volume_value_1(fn_cell_22(X0))
& genome_1(fn_cell_24(X0))
& chromosome_1(fn_cell_25(X0))
& tangible_entity_1(fn_cell_26(X0))
& phospholipid_bilayer_1(fn_cell_26(X0))
& cytoplasmic_side_1(fn_cell_27(X0))
& mixture_1(fn_cell_28(X0))
& cytoplasm_1(fn_cell_28(X0))
& substance_1(fn_cell_29(X0))
& cytosol_1(fn_cell_29(X0))
& plasma_membrane_1(fn_cell_30(X0))
& cell_1(fn_cytoplasm_7(fn_cell_28(X0)))
& cytoplasm_1(fn_cytoplasmic_side_1(fn_cell_27(X0)))
& substance_1(fn_mixture_1(fn_cell_28(X0)))
& cytosol_1(fn_cytoplasm_8(fn_cell_28(X0)))
& tangible_entity_1(fn_biomembrane_63(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_biomembrane_63(fn_cell_30(X0)))
& tangible_entity_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& cytoplasmic_side_1(fn_plasma_membrane_66(fn_cell_30(X0)))
& is_across_2(fn_cell_21(X0),fn_cell_30(X0))
& shape_2(X0,fn_cell_5(X0))
& specific_surface_area_2(X0,fn_cell_7(X0))
& size_2(X0,fn_cell_11(X0))
& structural_complexity_2(X0,fn_cell_13(X0))
& diameter_2(X0,fn_cell_18(X0))
& volume_2(X0,fn_cell_22(X0))
& exactCardinality(X0,has_region_0,"2",cell_pole_0)
& has_region_2(X0,fn_cell_1(X0))
& has_region_2(X0,fn_cell_4(X0))
& minCardinality(X0,has_part_0,"1",chromosome_0)
& has_part_2(X0,fn_cell_2(X0))
& has_part_2(X0,fn_cell_25(X0))
& has_part_2(X0,fn_cell_24(X0))
& has_part_2(X0,fn_cell_8(X0))
& has_part_2(X0,fn_cell_14(X0))
& has_part_2(X0,fn_cell_30(X0))
& is_inside_2(fn_cell_28(X0),fn_cell_30(X0))
& has_part_2(fn_cell_28(X0),fn_cell_9(X0))
& the_cardinal_value_2(fn_cell_20(X0),"100.0e0")
& cardinal_unit_class_2(fn_cell_20(X0),micrometer_0)
& greater_than_or_equal_to_2(fn_cell_20(X0),fn_cell_18(X0))
& the_cardinal_value_2(fn_cell_19(X0),"0.1e0")
& cardinal_unit_class_2(fn_cell_19(X0),micrometer_0)
& greater_than_or_equal_to_2(fn_cell_18(X0),fn_cell_19(X0))
& is_inside_2(fn_cell_14(X0),fn_cell_29(X0))
& the_scalar_value_2(fn_cell_13(X0),simple_0)
& directly_proportional_2(fn_cell_11(X0),fn_cell_22(X0))
& is_oriented_toward_2(fn_cell_27(X0),fn_cell_28(X0))
& is_at_2(fn_cell_26(X0),fn_cell_4(X0))
& has_part_2(X0,fn_cell_28(X0))
& has_part_2(fn_cell_28(X0),fn_cell_29(X0))
& has_region_2(fn_cell_30(X0),fn_cell_27(X0))
& has_part_2(fn_cell_30(X0),fn_cell_26(X0))
& is_facing_2(fn_cell_27(X0),fn_cell_28(X0))
& X0 = fn_cytoplasm_7(fn_cell_28(X0))
& fn_cell_29(X0) = fn_mixture_1(fn_cell_28(X0))
& fn_cell_29(X0) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cell_27(X0) = fn_biomembrane_47(fn_cell_30(X0))
& fn_cell_27(X0) = fn_plasma_membrane_66(fn_cell_30(X0))
& fn_cell_26(X0) = fn_biomembrane_63(fn_cell_30(X0))
& fn_cell_26(X0) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_cell_28(X0) = fn_cytoplasmic_side_1(fn_cell_27(X0))
& fn_mixture_1(fn_cell_28(X0)) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cytoplasm_8(fn_cell_28(X0)) = fn_biomembrane_63(fn_cell_30(X0))
& fn_biomembrane_63(fn_cell_30(X0)) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_plasma_membrane_71(fn_cell_30(X0)) = fn_biomembrane_47(fn_cell_30(X0))
& fn_biomembrane_47(fn_cell_30(X0)) = fn_plasma_membrane_66(fn_cell_30(X0)) ) ),
inference(pure_predicate_removal,[],[f20092]) ).
fof(f23906,plain,
! [X0] :
( cell_1(X0)
=> ( living_entity_1(X0)
& cell_pole_1(fn_cell_1(X0))
& cytoskeleton_1(fn_cell_2(X0))
& shape_value_1(fn_cell_5(X0))
& specific_surface_area_value_1(fn_cell_7(X0))
& motor_protein_1(fn_cell_8(X0))
& protein_enzyme_1(fn_cell_9(X0))
& size_value_1(fn_cell_11(X0))
& structural_complexity_value_1(fn_cell_13(X0))
& ribosome_1(fn_cell_14(X0))
& length_value_1(fn_cell_18(X0))
& length_value_1(fn_cell_19(X0))
& length_value_1(fn_cell_20(X0))
& membrane_potential_1(fn_cell_21(X0))
& volume_value_1(fn_cell_22(X0))
& genome_1(fn_cell_24(X0))
& chromosome_1(fn_cell_25(X0))
& tangible_entity_1(fn_cell_26(X0))
& phospholipid_bilayer_1(fn_cell_26(X0))
& cytoplasmic_side_1(fn_cell_27(X0))
& mixture_1(fn_cell_28(X0))
& cytoplasm_1(fn_cell_28(X0))
& substance_1(fn_cell_29(X0))
& cytosol_1(fn_cell_29(X0))
& plasma_membrane_1(fn_cell_30(X0))
& cell_1(fn_cytoplasm_7(fn_cell_28(X0)))
& cytoplasm_1(fn_cytoplasmic_side_1(fn_cell_27(X0)))
& substance_1(fn_mixture_1(fn_cell_28(X0)))
& cytosol_1(fn_cytoplasm_8(fn_cell_28(X0)))
& tangible_entity_1(fn_biomembrane_63(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_biomembrane_63(fn_cell_30(X0)))
& tangible_entity_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& cytoplasmic_side_1(fn_plasma_membrane_66(fn_cell_30(X0)))
& is_across_2(fn_cell_21(X0),fn_cell_30(X0))
& shape_2(X0,fn_cell_5(X0))
& specific_surface_area_2(X0,fn_cell_7(X0))
& size_2(X0,fn_cell_11(X0))
& structural_complexity_2(X0,fn_cell_13(X0))
& diameter_2(X0,fn_cell_18(X0))
& volume_2(X0,fn_cell_22(X0))
& exactCardinality(X0,has_region_0,"2",cell_pole_0)
& has_region_2(X0,fn_cell_1(X0))
& has_region_2(X0,fn_cell_4(X0))
& minCardinality(X0,has_part_0,"1",chromosome_0)
& has_part_2(X0,fn_cell_2(X0))
& has_part_2(X0,fn_cell_25(X0))
& has_part_2(X0,fn_cell_24(X0))
& has_part_2(X0,fn_cell_8(X0))
& has_part_2(X0,fn_cell_14(X0))
& has_part_2(X0,fn_cell_30(X0))
& is_inside_2(fn_cell_28(X0),fn_cell_30(X0))
& has_part_2(fn_cell_28(X0),fn_cell_9(X0))
& the_cardinal_value_2(fn_cell_20(X0),"100.0e0")
& cardinal_unit_class_2(fn_cell_20(X0),micrometer_0)
& greater_than_or_equal_to_2(fn_cell_20(X0),fn_cell_18(X0))
& the_cardinal_value_2(fn_cell_19(X0),"0.1e0")
& cardinal_unit_class_2(fn_cell_19(X0),micrometer_0)
& greater_than_or_equal_to_2(fn_cell_18(X0),fn_cell_19(X0))
& is_inside_2(fn_cell_14(X0),fn_cell_29(X0))
& the_scalar_value_2(fn_cell_13(X0),simple_0)
& directly_proportional_2(fn_cell_11(X0),fn_cell_22(X0))
& is_oriented_toward_2(fn_cell_27(X0),fn_cell_28(X0))
& is_at_2(fn_cell_26(X0),fn_cell_4(X0))
& has_part_2(X0,fn_cell_28(X0))
& has_part_2(fn_cell_28(X0),fn_cell_29(X0))
& has_region_2(fn_cell_30(X0),fn_cell_27(X0))
& has_part_2(fn_cell_30(X0),fn_cell_26(X0))
& is_facing_2(fn_cell_27(X0),fn_cell_28(X0))
& X0 = fn_cytoplasm_7(fn_cell_28(X0))
& fn_cell_29(X0) = fn_mixture_1(fn_cell_28(X0))
& fn_cell_29(X0) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cell_27(X0) = fn_biomembrane_47(fn_cell_30(X0))
& fn_cell_27(X0) = fn_plasma_membrane_66(fn_cell_30(X0))
& fn_cell_26(X0) = fn_biomembrane_63(fn_cell_30(X0))
& fn_cell_26(X0) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_cell_28(X0) = fn_cytoplasmic_side_1(fn_cell_27(X0))
& fn_mixture_1(fn_cell_28(X0)) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cytoplasm_8(fn_cell_28(X0)) = fn_biomembrane_63(fn_cell_30(X0))
& fn_biomembrane_63(fn_cell_30(X0)) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_plasma_membrane_71(fn_cell_30(X0)) = fn_biomembrane_47(fn_cell_30(X0))
& fn_biomembrane_47(fn_cell_30(X0)) = fn_plasma_membrane_66(fn_cell_30(X0)) ) ),
inference(pure_predicate_removal,[],[f22068]) ).
fof(f26232,plain,
! [X0] :
( cell_1(X0)
=> ( living_entity_1(X0)
& cell_pole_1(fn_cell_1(X0))
& cytoskeleton_1(fn_cell_2(X0))
& shape_value_1(fn_cell_5(X0))
& specific_surface_area_value_1(fn_cell_7(X0))
& motor_protein_1(fn_cell_8(X0))
& protein_enzyme_1(fn_cell_9(X0))
& size_value_1(fn_cell_11(X0))
& structural_complexity_value_1(fn_cell_13(X0))
& ribosome_1(fn_cell_14(X0))
& length_value_1(fn_cell_18(X0))
& length_value_1(fn_cell_19(X0))
& length_value_1(fn_cell_20(X0))
& membrane_potential_1(fn_cell_21(X0))
& volume_value_1(fn_cell_22(X0))
& genome_1(fn_cell_24(X0))
& chromosome_1(fn_cell_25(X0))
& tangible_entity_1(fn_cell_26(X0))
& phospholipid_bilayer_1(fn_cell_26(X0))
& cytoplasmic_side_1(fn_cell_27(X0))
& mixture_1(fn_cell_28(X0))
& cytoplasm_1(fn_cell_28(X0))
& substance_1(fn_cell_29(X0))
& cytosol_1(fn_cell_29(X0))
& plasma_membrane_1(fn_cell_30(X0))
& cell_1(fn_cytoplasm_7(fn_cell_28(X0)))
& cytoplasm_1(fn_cytoplasmic_side_1(fn_cell_27(X0)))
& substance_1(fn_mixture_1(fn_cell_28(X0)))
& cytosol_1(fn_cytoplasm_8(fn_cell_28(X0)))
& tangible_entity_1(fn_biomembrane_63(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_biomembrane_63(fn_cell_30(X0)))
& tangible_entity_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& cytoplasmic_side_1(fn_plasma_membrane_66(fn_cell_30(X0)))
& is_across_2(fn_cell_21(X0),fn_cell_30(X0))
& shape_2(X0,fn_cell_5(X0))
& specific_surface_area_2(X0,fn_cell_7(X0))
& size_2(X0,fn_cell_11(X0))
& structural_complexity_2(X0,fn_cell_13(X0))
& diameter_2(X0,fn_cell_18(X0))
& volume_2(X0,fn_cell_22(X0))
& exactCardinality(X0,has_region_0,"2",cell_pole_0)
& has_region_2(X0,fn_cell_1(X0))
& has_region_2(X0,fn_cell_4(X0))
& minCardinality(X0,has_part_0,"1",chromosome_0)
& has_part_2(X0,fn_cell_2(X0))
& has_part_2(X0,fn_cell_25(X0))
& has_part_2(X0,fn_cell_24(X0))
& has_part_2(X0,fn_cell_8(X0))
& has_part_2(X0,fn_cell_14(X0))
& has_part_2(X0,fn_cell_30(X0))
& is_inside_2(fn_cell_28(X0),fn_cell_30(X0))
& has_part_2(fn_cell_28(X0),fn_cell_9(X0))
& the_cardinal_value_2(fn_cell_20(X0),"100.0e0")
& greater_than_or_equal_to_2(fn_cell_20(X0),fn_cell_18(X0))
& the_cardinal_value_2(fn_cell_19(X0),"0.1e0")
& greater_than_or_equal_to_2(fn_cell_18(X0),fn_cell_19(X0))
& is_inside_2(fn_cell_14(X0),fn_cell_29(X0))
& the_scalar_value_2(fn_cell_13(X0),simple_0)
& directly_proportional_2(fn_cell_11(X0),fn_cell_22(X0))
& is_oriented_toward_2(fn_cell_27(X0),fn_cell_28(X0))
& is_at_2(fn_cell_26(X0),fn_cell_4(X0))
& has_part_2(X0,fn_cell_28(X0))
& has_part_2(fn_cell_28(X0),fn_cell_29(X0))
& has_region_2(fn_cell_30(X0),fn_cell_27(X0))
& has_part_2(fn_cell_30(X0),fn_cell_26(X0))
& is_facing_2(fn_cell_27(X0),fn_cell_28(X0))
& X0 = fn_cytoplasm_7(fn_cell_28(X0))
& fn_cell_29(X0) = fn_mixture_1(fn_cell_28(X0))
& fn_cell_29(X0) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cell_27(X0) = fn_biomembrane_47(fn_cell_30(X0))
& fn_cell_27(X0) = fn_plasma_membrane_66(fn_cell_30(X0))
& fn_cell_26(X0) = fn_biomembrane_63(fn_cell_30(X0))
& fn_cell_26(X0) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_cell_28(X0) = fn_cytoplasmic_side_1(fn_cell_27(X0))
& fn_mixture_1(fn_cell_28(X0)) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cytoplasm_8(fn_cell_28(X0)) = fn_biomembrane_63(fn_cell_30(X0))
& fn_biomembrane_63(fn_cell_30(X0)) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_plasma_membrane_71(fn_cell_30(X0)) = fn_biomembrane_47(fn_cell_30(X0))
& fn_biomembrane_47(fn_cell_30(X0)) = fn_plasma_membrane_66(fn_cell_30(X0)) ) ),
inference(pure_predicate_removal,[],[f23906]) ).
fof(f26354,plain,
! [X0] :
( cell_1(X0)
=> ( living_entity_1(X0)
& cell_pole_1(fn_cell_1(X0))
& cytoskeleton_1(fn_cell_2(X0))
& shape_value_1(fn_cell_5(X0))
& specific_surface_area_value_1(fn_cell_7(X0))
& motor_protein_1(fn_cell_8(X0))
& protein_enzyme_1(fn_cell_9(X0))
& size_value_1(fn_cell_11(X0))
& structural_complexity_value_1(fn_cell_13(X0))
& ribosome_1(fn_cell_14(X0))
& length_value_1(fn_cell_18(X0))
& length_value_1(fn_cell_19(X0))
& length_value_1(fn_cell_20(X0))
& membrane_potential_1(fn_cell_21(X0))
& volume_value_1(fn_cell_22(X0))
& genome_1(fn_cell_24(X0))
& chromosome_1(fn_cell_25(X0))
& tangible_entity_1(fn_cell_26(X0))
& phospholipid_bilayer_1(fn_cell_26(X0))
& cytoplasmic_side_1(fn_cell_27(X0))
& mixture_1(fn_cell_28(X0))
& cytoplasm_1(fn_cell_28(X0))
& substance_1(fn_cell_29(X0))
& cytosol_1(fn_cell_29(X0))
& plasma_membrane_1(fn_cell_30(X0))
& cell_1(fn_cytoplasm_7(fn_cell_28(X0)))
& cytoplasm_1(fn_cytoplasmic_side_1(fn_cell_27(X0)))
& substance_1(fn_mixture_1(fn_cell_28(X0)))
& cytosol_1(fn_cytoplasm_8(fn_cell_28(X0)))
& tangible_entity_1(fn_biomembrane_63(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_biomembrane_63(fn_cell_30(X0)))
& tangible_entity_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& cytoplasmic_side_1(fn_plasma_membrane_66(fn_cell_30(X0)))
& is_across_2(fn_cell_21(X0),fn_cell_30(X0))
& shape_2(X0,fn_cell_5(X0))
& specific_surface_area_2(X0,fn_cell_7(X0))
& size_2(X0,fn_cell_11(X0))
& structural_complexity_2(X0,fn_cell_13(X0))
& diameter_2(X0,fn_cell_18(X0))
& volume_2(X0,fn_cell_22(X0))
& exactCardinality(X0,has_region_0,"2",cell_pole_0)
& has_region_2(X0,fn_cell_1(X0))
& has_region_2(X0,fn_cell_4(X0))
& minCardinality(X0,has_part_0,"1",chromosome_0)
& has_part_2(X0,fn_cell_2(X0))
& has_part_2(X0,fn_cell_25(X0))
& has_part_2(X0,fn_cell_24(X0))
& has_part_2(X0,fn_cell_8(X0))
& has_part_2(X0,fn_cell_14(X0))
& has_part_2(X0,fn_cell_30(X0))
& is_inside_2(fn_cell_28(X0),fn_cell_30(X0))
& has_part_2(fn_cell_28(X0),fn_cell_9(X0))
& the_cardinal_value_2(fn_cell_20(X0),"100.0e0")
& greater_than_or_equal_to_2(fn_cell_20(X0),fn_cell_18(X0))
& the_cardinal_value_2(fn_cell_19(X0),"0.1e0")
& greater_than_or_equal_to_2(fn_cell_18(X0),fn_cell_19(X0))
& is_inside_2(fn_cell_14(X0),fn_cell_29(X0))
& directly_proportional_2(fn_cell_11(X0),fn_cell_22(X0))
& is_oriented_toward_2(fn_cell_27(X0),fn_cell_28(X0))
& is_at_2(fn_cell_26(X0),fn_cell_4(X0))
& has_part_2(X0,fn_cell_28(X0))
& has_part_2(fn_cell_28(X0),fn_cell_29(X0))
& has_region_2(fn_cell_30(X0),fn_cell_27(X0))
& has_part_2(fn_cell_30(X0),fn_cell_26(X0))
& is_facing_2(fn_cell_27(X0),fn_cell_28(X0))
& X0 = fn_cytoplasm_7(fn_cell_28(X0))
& fn_cell_29(X0) = fn_mixture_1(fn_cell_28(X0))
& fn_cell_29(X0) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cell_27(X0) = fn_biomembrane_47(fn_cell_30(X0))
& fn_cell_27(X0) = fn_plasma_membrane_66(fn_cell_30(X0))
& fn_cell_26(X0) = fn_biomembrane_63(fn_cell_30(X0))
& fn_cell_26(X0) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_cell_28(X0) = fn_cytoplasmic_side_1(fn_cell_27(X0))
& fn_mixture_1(fn_cell_28(X0)) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cytoplasm_8(fn_cell_28(X0)) = fn_biomembrane_63(fn_cell_30(X0))
& fn_biomembrane_63(fn_cell_30(X0)) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_plasma_membrane_71(fn_cell_30(X0)) = fn_biomembrane_47(fn_cell_30(X0))
& fn_biomembrane_47(fn_cell_30(X0)) = fn_plasma_membrane_66(fn_cell_30(X0)) ) ),
inference(pure_predicate_removal,[],[f26232]) ).
fof(f26679,plain,
! [X0] :
( cell_1(X0)
=> ( living_entity_1(X0)
& cell_pole_1(fn_cell_1(X0))
& cytoskeleton_1(fn_cell_2(X0))
& shape_value_1(fn_cell_5(X0))
& specific_surface_area_value_1(fn_cell_7(X0))
& motor_protein_1(fn_cell_8(X0))
& protein_enzyme_1(fn_cell_9(X0))
& size_value_1(fn_cell_11(X0))
& structural_complexity_value_1(fn_cell_13(X0))
& ribosome_1(fn_cell_14(X0))
& membrane_potential_1(fn_cell_21(X0))
& volume_value_1(fn_cell_22(X0))
& genome_1(fn_cell_24(X0))
& chromosome_1(fn_cell_25(X0))
& tangible_entity_1(fn_cell_26(X0))
& phospholipid_bilayer_1(fn_cell_26(X0))
& cytoplasmic_side_1(fn_cell_27(X0))
& mixture_1(fn_cell_28(X0))
& cytoplasm_1(fn_cell_28(X0))
& substance_1(fn_cell_29(X0))
& cytosol_1(fn_cell_29(X0))
& plasma_membrane_1(fn_cell_30(X0))
& cell_1(fn_cytoplasm_7(fn_cell_28(X0)))
& cytoplasm_1(fn_cytoplasmic_side_1(fn_cell_27(X0)))
& substance_1(fn_mixture_1(fn_cell_28(X0)))
& cytosol_1(fn_cytoplasm_8(fn_cell_28(X0)))
& tangible_entity_1(fn_biomembrane_63(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_biomembrane_63(fn_cell_30(X0)))
& tangible_entity_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& cytoplasmic_side_1(fn_plasma_membrane_66(fn_cell_30(X0)))
& is_across_2(fn_cell_21(X0),fn_cell_30(X0))
& shape_2(X0,fn_cell_5(X0))
& specific_surface_area_2(X0,fn_cell_7(X0))
& size_2(X0,fn_cell_11(X0))
& structural_complexity_2(X0,fn_cell_13(X0))
& diameter_2(X0,fn_cell_18(X0))
& volume_2(X0,fn_cell_22(X0))
& exactCardinality(X0,has_region_0,"2",cell_pole_0)
& has_region_2(X0,fn_cell_1(X0))
& has_region_2(X0,fn_cell_4(X0))
& minCardinality(X0,has_part_0,"1",chromosome_0)
& has_part_2(X0,fn_cell_2(X0))
& has_part_2(X0,fn_cell_25(X0))
& has_part_2(X0,fn_cell_24(X0))
& has_part_2(X0,fn_cell_8(X0))
& has_part_2(X0,fn_cell_14(X0))
& has_part_2(X0,fn_cell_30(X0))
& is_inside_2(fn_cell_28(X0),fn_cell_30(X0))
& has_part_2(fn_cell_28(X0),fn_cell_9(X0))
& the_cardinal_value_2(fn_cell_20(X0),"100.0e0")
& greater_than_or_equal_to_2(fn_cell_20(X0),fn_cell_18(X0))
& the_cardinal_value_2(fn_cell_19(X0),"0.1e0")
& greater_than_or_equal_to_2(fn_cell_18(X0),fn_cell_19(X0))
& is_inside_2(fn_cell_14(X0),fn_cell_29(X0))
& directly_proportional_2(fn_cell_11(X0),fn_cell_22(X0))
& is_oriented_toward_2(fn_cell_27(X0),fn_cell_28(X0))
& is_at_2(fn_cell_26(X0),fn_cell_4(X0))
& has_part_2(X0,fn_cell_28(X0))
& has_part_2(fn_cell_28(X0),fn_cell_29(X0))
& has_region_2(fn_cell_30(X0),fn_cell_27(X0))
& has_part_2(fn_cell_30(X0),fn_cell_26(X0))
& is_facing_2(fn_cell_27(X0),fn_cell_28(X0))
& X0 = fn_cytoplasm_7(fn_cell_28(X0))
& fn_cell_29(X0) = fn_mixture_1(fn_cell_28(X0))
& fn_cell_29(X0) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cell_27(X0) = fn_biomembrane_47(fn_cell_30(X0))
& fn_cell_27(X0) = fn_plasma_membrane_66(fn_cell_30(X0))
& fn_cell_26(X0) = fn_biomembrane_63(fn_cell_30(X0))
& fn_cell_26(X0) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_cell_28(X0) = fn_cytoplasmic_side_1(fn_cell_27(X0))
& fn_mixture_1(fn_cell_28(X0)) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cytoplasm_8(fn_cell_28(X0)) = fn_biomembrane_63(fn_cell_30(X0))
& fn_biomembrane_63(fn_cell_30(X0)) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_plasma_membrane_71(fn_cell_30(X0)) = fn_biomembrane_47(fn_cell_30(X0))
& fn_biomembrane_47(fn_cell_30(X0)) = fn_plasma_membrane_66(fn_cell_30(X0)) ) ),
inference(pure_predicate_removal,[],[f26354]) ).
fof(f26912,plain,
! [X0] :
( cell_1(X0)
=> ( living_entity_1(X0)
& cell_pole_1(fn_cell_1(X0))
& cytoskeleton_1(fn_cell_2(X0))
& shape_value_1(fn_cell_5(X0))
& specific_surface_area_value_1(fn_cell_7(X0))
& motor_protein_1(fn_cell_8(X0))
& protein_enzyme_1(fn_cell_9(X0))
& size_value_1(fn_cell_11(X0))
& structural_complexity_value_1(fn_cell_13(X0))
& ribosome_1(fn_cell_14(X0))
& membrane_potential_1(fn_cell_21(X0))
& genome_1(fn_cell_24(X0))
& chromosome_1(fn_cell_25(X0))
& tangible_entity_1(fn_cell_26(X0))
& phospholipid_bilayer_1(fn_cell_26(X0))
& cytoplasmic_side_1(fn_cell_27(X0))
& mixture_1(fn_cell_28(X0))
& cytoplasm_1(fn_cell_28(X0))
& substance_1(fn_cell_29(X0))
& cytosol_1(fn_cell_29(X0))
& plasma_membrane_1(fn_cell_30(X0))
& cell_1(fn_cytoplasm_7(fn_cell_28(X0)))
& cytoplasm_1(fn_cytoplasmic_side_1(fn_cell_27(X0)))
& substance_1(fn_mixture_1(fn_cell_28(X0)))
& cytosol_1(fn_cytoplasm_8(fn_cell_28(X0)))
& tangible_entity_1(fn_biomembrane_63(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_biomembrane_63(fn_cell_30(X0)))
& tangible_entity_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& cytoplasmic_side_1(fn_plasma_membrane_66(fn_cell_30(X0)))
& is_across_2(fn_cell_21(X0),fn_cell_30(X0))
& shape_2(X0,fn_cell_5(X0))
& specific_surface_area_2(X0,fn_cell_7(X0))
& size_2(X0,fn_cell_11(X0))
& structural_complexity_2(X0,fn_cell_13(X0))
& diameter_2(X0,fn_cell_18(X0))
& volume_2(X0,fn_cell_22(X0))
& exactCardinality(X0,has_region_0,"2",cell_pole_0)
& has_region_2(X0,fn_cell_1(X0))
& has_region_2(X0,fn_cell_4(X0))
& minCardinality(X0,has_part_0,"1",chromosome_0)
& has_part_2(X0,fn_cell_2(X0))
& has_part_2(X0,fn_cell_25(X0))
& has_part_2(X0,fn_cell_24(X0))
& has_part_2(X0,fn_cell_8(X0))
& has_part_2(X0,fn_cell_14(X0))
& has_part_2(X0,fn_cell_30(X0))
& is_inside_2(fn_cell_28(X0),fn_cell_30(X0))
& has_part_2(fn_cell_28(X0),fn_cell_9(X0))
& the_cardinal_value_2(fn_cell_20(X0),"100.0e0")
& greater_than_or_equal_to_2(fn_cell_20(X0),fn_cell_18(X0))
& the_cardinal_value_2(fn_cell_19(X0),"0.1e0")
& greater_than_or_equal_to_2(fn_cell_18(X0),fn_cell_19(X0))
& is_inside_2(fn_cell_14(X0),fn_cell_29(X0))
& directly_proportional_2(fn_cell_11(X0),fn_cell_22(X0))
& is_oriented_toward_2(fn_cell_27(X0),fn_cell_28(X0))
& is_at_2(fn_cell_26(X0),fn_cell_4(X0))
& has_part_2(X0,fn_cell_28(X0))
& has_part_2(fn_cell_28(X0),fn_cell_29(X0))
& has_region_2(fn_cell_30(X0),fn_cell_27(X0))
& has_part_2(fn_cell_30(X0),fn_cell_26(X0))
& is_facing_2(fn_cell_27(X0),fn_cell_28(X0))
& X0 = fn_cytoplasm_7(fn_cell_28(X0))
& fn_cell_29(X0) = fn_mixture_1(fn_cell_28(X0))
& fn_cell_29(X0) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cell_27(X0) = fn_biomembrane_47(fn_cell_30(X0))
& fn_cell_27(X0) = fn_plasma_membrane_66(fn_cell_30(X0))
& fn_cell_26(X0) = fn_biomembrane_63(fn_cell_30(X0))
& fn_cell_26(X0) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_cell_28(X0) = fn_cytoplasmic_side_1(fn_cell_27(X0))
& fn_mixture_1(fn_cell_28(X0)) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cytoplasm_8(fn_cell_28(X0)) = fn_biomembrane_63(fn_cell_30(X0))
& fn_biomembrane_63(fn_cell_30(X0)) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_plasma_membrane_71(fn_cell_30(X0)) = fn_biomembrane_47(fn_cell_30(X0))
& fn_biomembrane_47(fn_cell_30(X0)) = fn_plasma_membrane_66(fn_cell_30(X0)) ) ),
inference(pure_predicate_removal,[],[f26679]) ).
fof(f27153,plain,
! [X0] :
( cell_1(X0)
=> ( living_entity_1(X0)
& cell_pole_1(fn_cell_1(X0))
& cytoskeleton_1(fn_cell_2(X0))
& shape_value_1(fn_cell_5(X0))
& specific_surface_area_value_1(fn_cell_7(X0))
& motor_protein_1(fn_cell_8(X0))
& protein_enzyme_1(fn_cell_9(X0))
& structural_complexity_value_1(fn_cell_13(X0))
& ribosome_1(fn_cell_14(X0))
& membrane_potential_1(fn_cell_21(X0))
& genome_1(fn_cell_24(X0))
& chromosome_1(fn_cell_25(X0))
& tangible_entity_1(fn_cell_26(X0))
& phospholipid_bilayer_1(fn_cell_26(X0))
& cytoplasmic_side_1(fn_cell_27(X0))
& mixture_1(fn_cell_28(X0))
& cytoplasm_1(fn_cell_28(X0))
& substance_1(fn_cell_29(X0))
& cytosol_1(fn_cell_29(X0))
& plasma_membrane_1(fn_cell_30(X0))
& cell_1(fn_cytoplasm_7(fn_cell_28(X0)))
& cytoplasm_1(fn_cytoplasmic_side_1(fn_cell_27(X0)))
& substance_1(fn_mixture_1(fn_cell_28(X0)))
& cytosol_1(fn_cytoplasm_8(fn_cell_28(X0)))
& tangible_entity_1(fn_biomembrane_63(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_biomembrane_63(fn_cell_30(X0)))
& tangible_entity_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& cytoplasmic_side_1(fn_plasma_membrane_66(fn_cell_30(X0)))
& is_across_2(fn_cell_21(X0),fn_cell_30(X0))
& shape_2(X0,fn_cell_5(X0))
& specific_surface_area_2(X0,fn_cell_7(X0))
& size_2(X0,fn_cell_11(X0))
& structural_complexity_2(X0,fn_cell_13(X0))
& diameter_2(X0,fn_cell_18(X0))
& volume_2(X0,fn_cell_22(X0))
& exactCardinality(X0,has_region_0,"2",cell_pole_0)
& has_region_2(X0,fn_cell_1(X0))
& has_region_2(X0,fn_cell_4(X0))
& minCardinality(X0,has_part_0,"1",chromosome_0)
& has_part_2(X0,fn_cell_2(X0))
& has_part_2(X0,fn_cell_25(X0))
& has_part_2(X0,fn_cell_24(X0))
& has_part_2(X0,fn_cell_8(X0))
& has_part_2(X0,fn_cell_14(X0))
& has_part_2(X0,fn_cell_30(X0))
& is_inside_2(fn_cell_28(X0),fn_cell_30(X0))
& has_part_2(fn_cell_28(X0),fn_cell_9(X0))
& the_cardinal_value_2(fn_cell_20(X0),"100.0e0")
& greater_than_or_equal_to_2(fn_cell_20(X0),fn_cell_18(X0))
& the_cardinal_value_2(fn_cell_19(X0),"0.1e0")
& greater_than_or_equal_to_2(fn_cell_18(X0),fn_cell_19(X0))
& is_inside_2(fn_cell_14(X0),fn_cell_29(X0))
& directly_proportional_2(fn_cell_11(X0),fn_cell_22(X0))
& is_oriented_toward_2(fn_cell_27(X0),fn_cell_28(X0))
& is_at_2(fn_cell_26(X0),fn_cell_4(X0))
& has_part_2(X0,fn_cell_28(X0))
& has_part_2(fn_cell_28(X0),fn_cell_29(X0))
& has_region_2(fn_cell_30(X0),fn_cell_27(X0))
& has_part_2(fn_cell_30(X0),fn_cell_26(X0))
& is_facing_2(fn_cell_27(X0),fn_cell_28(X0))
& X0 = fn_cytoplasm_7(fn_cell_28(X0))
& fn_cell_29(X0) = fn_mixture_1(fn_cell_28(X0))
& fn_cell_29(X0) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cell_27(X0) = fn_biomembrane_47(fn_cell_30(X0))
& fn_cell_27(X0) = fn_plasma_membrane_66(fn_cell_30(X0))
& fn_cell_26(X0) = fn_biomembrane_63(fn_cell_30(X0))
& fn_cell_26(X0) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_cell_28(X0) = fn_cytoplasmic_side_1(fn_cell_27(X0))
& fn_mixture_1(fn_cell_28(X0)) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cytoplasm_8(fn_cell_28(X0)) = fn_biomembrane_63(fn_cell_30(X0))
& fn_biomembrane_63(fn_cell_30(X0)) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_plasma_membrane_71(fn_cell_30(X0)) = fn_biomembrane_47(fn_cell_30(X0))
& fn_biomembrane_47(fn_cell_30(X0)) = fn_plasma_membrane_66(fn_cell_30(X0)) ) ),
inference(pure_predicate_removal,[],[f26912]) ).
fof(f27509,plain,
! [X0] :
( cell_1(X0)
=> ( living_entity_1(X0)
& cell_pole_1(fn_cell_1(X0))
& cytoskeleton_1(fn_cell_2(X0))
& shape_value_1(fn_cell_5(X0))
& specific_surface_area_value_1(fn_cell_7(X0))
& motor_protein_1(fn_cell_8(X0))
& protein_enzyme_1(fn_cell_9(X0))
& structural_complexity_value_1(fn_cell_13(X0))
& ribosome_1(fn_cell_14(X0))
& membrane_potential_1(fn_cell_21(X0))
& genome_1(fn_cell_24(X0))
& chromosome_1(fn_cell_25(X0))
& tangible_entity_1(fn_cell_26(X0))
& phospholipid_bilayer_1(fn_cell_26(X0))
& cytoplasmic_side_1(fn_cell_27(X0))
& mixture_1(fn_cell_28(X0))
& cytoplasm_1(fn_cell_28(X0))
& substance_1(fn_cell_29(X0))
& cytosol_1(fn_cell_29(X0))
& plasma_membrane_1(fn_cell_30(X0))
& cell_1(fn_cytoplasm_7(fn_cell_28(X0)))
& cytoplasm_1(fn_cytoplasmic_side_1(fn_cell_27(X0)))
& substance_1(fn_mixture_1(fn_cell_28(X0)))
& cytosol_1(fn_cytoplasm_8(fn_cell_28(X0)))
& tangible_entity_1(fn_biomembrane_63(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_biomembrane_63(fn_cell_30(X0)))
& tangible_entity_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& cytoplasmic_side_1(fn_plasma_membrane_66(fn_cell_30(X0)))
& is_across_2(fn_cell_21(X0),fn_cell_30(X0))
& shape_2(X0,fn_cell_5(X0))
& specific_surface_area_2(X0,fn_cell_7(X0))
& size_2(X0,fn_cell_11(X0))
& structural_complexity_2(X0,fn_cell_13(X0))
& diameter_2(X0,fn_cell_18(X0))
& volume_2(X0,fn_cell_22(X0))
& exactCardinality(X0,has_region_0,"2",cell_pole_0)
& has_region_2(X0,fn_cell_1(X0))
& has_region_2(X0,fn_cell_4(X0))
& minCardinality(X0,has_part_0,"1",chromosome_0)
& has_part_2(X0,fn_cell_2(X0))
& has_part_2(X0,fn_cell_25(X0))
& has_part_2(X0,fn_cell_24(X0))
& has_part_2(X0,fn_cell_8(X0))
& has_part_2(X0,fn_cell_14(X0))
& has_part_2(X0,fn_cell_30(X0))
& is_inside_2(fn_cell_28(X0),fn_cell_30(X0))
& has_part_2(fn_cell_28(X0),fn_cell_9(X0))
& the_cardinal_value_2(fn_cell_20(X0),"100.0e0")
& the_cardinal_value_2(fn_cell_19(X0),"0.1e0")
& is_inside_2(fn_cell_14(X0),fn_cell_29(X0))
& directly_proportional_2(fn_cell_11(X0),fn_cell_22(X0))
& is_oriented_toward_2(fn_cell_27(X0),fn_cell_28(X0))
& is_at_2(fn_cell_26(X0),fn_cell_4(X0))
& has_part_2(X0,fn_cell_28(X0))
& has_part_2(fn_cell_28(X0),fn_cell_29(X0))
& has_region_2(fn_cell_30(X0),fn_cell_27(X0))
& has_part_2(fn_cell_30(X0),fn_cell_26(X0))
& is_facing_2(fn_cell_27(X0),fn_cell_28(X0))
& X0 = fn_cytoplasm_7(fn_cell_28(X0))
& fn_cell_29(X0) = fn_mixture_1(fn_cell_28(X0))
& fn_cell_29(X0) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cell_27(X0) = fn_biomembrane_47(fn_cell_30(X0))
& fn_cell_27(X0) = fn_plasma_membrane_66(fn_cell_30(X0))
& fn_cell_26(X0) = fn_biomembrane_63(fn_cell_30(X0))
& fn_cell_26(X0) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_cell_28(X0) = fn_cytoplasmic_side_1(fn_cell_27(X0))
& fn_mixture_1(fn_cell_28(X0)) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cytoplasm_8(fn_cell_28(X0)) = fn_biomembrane_63(fn_cell_30(X0))
& fn_biomembrane_63(fn_cell_30(X0)) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_plasma_membrane_71(fn_cell_30(X0)) = fn_biomembrane_47(fn_cell_30(X0))
& fn_biomembrane_47(fn_cell_30(X0)) = fn_plasma_membrane_66(fn_cell_30(X0)) ) ),
inference(pure_predicate_removal,[],[f27153]) ).
fof(f27552,plain,
! [X0] :
( cell_1(X0)
=> ( living_entity_1(X0)
& cell_pole_1(fn_cell_1(X0))
& cytoskeleton_1(fn_cell_2(X0))
& shape_value_1(fn_cell_5(X0))
& motor_protein_1(fn_cell_8(X0))
& protein_enzyme_1(fn_cell_9(X0))
& structural_complexity_value_1(fn_cell_13(X0))
& ribosome_1(fn_cell_14(X0))
& membrane_potential_1(fn_cell_21(X0))
& genome_1(fn_cell_24(X0))
& chromosome_1(fn_cell_25(X0))
& tangible_entity_1(fn_cell_26(X0))
& phospholipid_bilayer_1(fn_cell_26(X0))
& cytoplasmic_side_1(fn_cell_27(X0))
& mixture_1(fn_cell_28(X0))
& cytoplasm_1(fn_cell_28(X0))
& substance_1(fn_cell_29(X0))
& cytosol_1(fn_cell_29(X0))
& plasma_membrane_1(fn_cell_30(X0))
& cell_1(fn_cytoplasm_7(fn_cell_28(X0)))
& cytoplasm_1(fn_cytoplasmic_side_1(fn_cell_27(X0)))
& substance_1(fn_mixture_1(fn_cell_28(X0)))
& cytosol_1(fn_cytoplasm_8(fn_cell_28(X0)))
& tangible_entity_1(fn_biomembrane_63(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_biomembrane_63(fn_cell_30(X0)))
& tangible_entity_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& cytoplasmic_side_1(fn_plasma_membrane_66(fn_cell_30(X0)))
& is_across_2(fn_cell_21(X0),fn_cell_30(X0))
& shape_2(X0,fn_cell_5(X0))
& specific_surface_area_2(X0,fn_cell_7(X0))
& size_2(X0,fn_cell_11(X0))
& structural_complexity_2(X0,fn_cell_13(X0))
& diameter_2(X0,fn_cell_18(X0))
& volume_2(X0,fn_cell_22(X0))
& exactCardinality(X0,has_region_0,"2",cell_pole_0)
& has_region_2(X0,fn_cell_1(X0))
& has_region_2(X0,fn_cell_4(X0))
& minCardinality(X0,has_part_0,"1",chromosome_0)
& has_part_2(X0,fn_cell_2(X0))
& has_part_2(X0,fn_cell_25(X0))
& has_part_2(X0,fn_cell_24(X0))
& has_part_2(X0,fn_cell_8(X0))
& has_part_2(X0,fn_cell_14(X0))
& has_part_2(X0,fn_cell_30(X0))
& is_inside_2(fn_cell_28(X0),fn_cell_30(X0))
& has_part_2(fn_cell_28(X0),fn_cell_9(X0))
& the_cardinal_value_2(fn_cell_20(X0),"100.0e0")
& the_cardinal_value_2(fn_cell_19(X0),"0.1e0")
& is_inside_2(fn_cell_14(X0),fn_cell_29(X0))
& directly_proportional_2(fn_cell_11(X0),fn_cell_22(X0))
& is_oriented_toward_2(fn_cell_27(X0),fn_cell_28(X0))
& is_at_2(fn_cell_26(X0),fn_cell_4(X0))
& has_part_2(X0,fn_cell_28(X0))
& has_part_2(fn_cell_28(X0),fn_cell_29(X0))
& has_region_2(fn_cell_30(X0),fn_cell_27(X0))
& has_part_2(fn_cell_30(X0),fn_cell_26(X0))
& is_facing_2(fn_cell_27(X0),fn_cell_28(X0))
& X0 = fn_cytoplasm_7(fn_cell_28(X0))
& fn_cell_29(X0) = fn_mixture_1(fn_cell_28(X0))
& fn_cell_29(X0) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cell_27(X0) = fn_biomembrane_47(fn_cell_30(X0))
& fn_cell_27(X0) = fn_plasma_membrane_66(fn_cell_30(X0))
& fn_cell_26(X0) = fn_biomembrane_63(fn_cell_30(X0))
& fn_cell_26(X0) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_cell_28(X0) = fn_cytoplasmic_side_1(fn_cell_27(X0))
& fn_mixture_1(fn_cell_28(X0)) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cytoplasm_8(fn_cell_28(X0)) = fn_biomembrane_63(fn_cell_30(X0))
& fn_biomembrane_63(fn_cell_30(X0)) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_plasma_membrane_71(fn_cell_30(X0)) = fn_biomembrane_47(fn_cell_30(X0))
& fn_biomembrane_47(fn_cell_30(X0)) = fn_plasma_membrane_66(fn_cell_30(X0)) ) ),
inference(pure_predicate_removal,[],[f27509]) ).
fof(f28465,plain,
! [X0] :
( cell_1(X0)
=> ( living_entity_1(X0)
& cell_pole_1(fn_cell_1(X0))
& cytoskeleton_1(fn_cell_2(X0))
& shape_value_1(fn_cell_5(X0))
& motor_protein_1(fn_cell_8(X0))
& protein_enzyme_1(fn_cell_9(X0))
& structural_complexity_value_1(fn_cell_13(X0))
& ribosome_1(fn_cell_14(X0))
& membrane_potential_1(fn_cell_21(X0))
& genome_1(fn_cell_24(X0))
& chromosome_1(fn_cell_25(X0))
& tangible_entity_1(fn_cell_26(X0))
& phospholipid_bilayer_1(fn_cell_26(X0))
& cytoplasmic_side_1(fn_cell_27(X0))
& mixture_1(fn_cell_28(X0))
& cytoplasm_1(fn_cell_28(X0))
& substance_1(fn_cell_29(X0))
& cytosol_1(fn_cell_29(X0))
& plasma_membrane_1(fn_cell_30(X0))
& cell_1(fn_cytoplasm_7(fn_cell_28(X0)))
& cytoplasm_1(fn_cytoplasmic_side_1(fn_cell_27(X0)))
& substance_1(fn_mixture_1(fn_cell_28(X0)))
& cytosol_1(fn_cytoplasm_8(fn_cell_28(X0)))
& tangible_entity_1(fn_biomembrane_63(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_biomembrane_63(fn_cell_30(X0)))
& tangible_entity_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& cytoplasmic_side_1(fn_plasma_membrane_66(fn_cell_30(X0)))
& is_across_2(fn_cell_21(X0),fn_cell_30(X0))
& shape_2(X0,fn_cell_5(X0))
& specific_surface_area_2(X0,fn_cell_7(X0))
& size_2(X0,fn_cell_11(X0))
& structural_complexity_2(X0,fn_cell_13(X0))
& diameter_2(X0,fn_cell_18(X0))
& volume_2(X0,fn_cell_22(X0))
& exactCardinality(X0,has_region_0,"2",cell_pole_0)
& has_region_2(X0,fn_cell_1(X0))
& has_region_2(X0,fn_cell_4(X0))
& minCardinality(X0,has_part_0,"1",chromosome_0)
& has_part_2(X0,fn_cell_2(X0))
& has_part_2(X0,fn_cell_25(X0))
& has_part_2(X0,fn_cell_24(X0))
& has_part_2(X0,fn_cell_8(X0))
& has_part_2(X0,fn_cell_14(X0))
& has_part_2(X0,fn_cell_30(X0))
& is_inside_2(fn_cell_28(X0),fn_cell_30(X0))
& has_part_2(fn_cell_28(X0),fn_cell_9(X0))
& the_cardinal_value_2(fn_cell_20(X0),"100.0e0")
& the_cardinal_value_2(fn_cell_19(X0),"0.1e0")
& is_inside_2(fn_cell_14(X0),fn_cell_29(X0))
& is_oriented_toward_2(fn_cell_27(X0),fn_cell_28(X0))
& is_at_2(fn_cell_26(X0),fn_cell_4(X0))
& has_part_2(X0,fn_cell_28(X0))
& has_part_2(fn_cell_28(X0),fn_cell_29(X0))
& has_region_2(fn_cell_30(X0),fn_cell_27(X0))
& has_part_2(fn_cell_30(X0),fn_cell_26(X0))
& is_facing_2(fn_cell_27(X0),fn_cell_28(X0))
& X0 = fn_cytoplasm_7(fn_cell_28(X0))
& fn_cell_29(X0) = fn_mixture_1(fn_cell_28(X0))
& fn_cell_29(X0) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cell_27(X0) = fn_biomembrane_47(fn_cell_30(X0))
& fn_cell_27(X0) = fn_plasma_membrane_66(fn_cell_30(X0))
& fn_cell_26(X0) = fn_biomembrane_63(fn_cell_30(X0))
& fn_cell_26(X0) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_cell_28(X0) = fn_cytoplasmic_side_1(fn_cell_27(X0))
& fn_mixture_1(fn_cell_28(X0)) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cytoplasm_8(fn_cell_28(X0)) = fn_biomembrane_63(fn_cell_30(X0))
& fn_biomembrane_63(fn_cell_30(X0)) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_plasma_membrane_71(fn_cell_30(X0)) = fn_biomembrane_47(fn_cell_30(X0))
& fn_biomembrane_47(fn_cell_30(X0)) = fn_plasma_membrane_66(fn_cell_30(X0)) ) ),
inference(pure_predicate_removal,[],[f27552]) ).
fof(f28794,plain,
! [X0] :
( ( living_entity_1(X0)
& cell_pole_1(fn_cell_1(X0))
& cytoskeleton_1(fn_cell_2(X0))
& shape_value_1(fn_cell_5(X0))
& motor_protein_1(fn_cell_8(X0))
& protein_enzyme_1(fn_cell_9(X0))
& structural_complexity_value_1(fn_cell_13(X0))
& ribosome_1(fn_cell_14(X0))
& membrane_potential_1(fn_cell_21(X0))
& genome_1(fn_cell_24(X0))
& chromosome_1(fn_cell_25(X0))
& tangible_entity_1(fn_cell_26(X0))
& phospholipid_bilayer_1(fn_cell_26(X0))
& cytoplasmic_side_1(fn_cell_27(X0))
& mixture_1(fn_cell_28(X0))
& cytoplasm_1(fn_cell_28(X0))
& substance_1(fn_cell_29(X0))
& cytosol_1(fn_cell_29(X0))
& plasma_membrane_1(fn_cell_30(X0))
& cell_1(fn_cytoplasm_7(fn_cell_28(X0)))
& cytoplasm_1(fn_cytoplasmic_side_1(fn_cell_27(X0)))
& substance_1(fn_mixture_1(fn_cell_28(X0)))
& cytosol_1(fn_cytoplasm_8(fn_cell_28(X0)))
& tangible_entity_1(fn_biomembrane_63(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_biomembrane_63(fn_cell_30(X0)))
& tangible_entity_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& cytoplasmic_side_1(fn_plasma_membrane_66(fn_cell_30(X0)))
& is_across_2(fn_cell_21(X0),fn_cell_30(X0))
& shape_2(X0,fn_cell_5(X0))
& specific_surface_area_2(X0,fn_cell_7(X0))
& size_2(X0,fn_cell_11(X0))
& structural_complexity_2(X0,fn_cell_13(X0))
& diameter_2(X0,fn_cell_18(X0))
& volume_2(X0,fn_cell_22(X0))
& exactCardinality(X0,has_region_0,"2",cell_pole_0)
& has_region_2(X0,fn_cell_1(X0))
& has_region_2(X0,fn_cell_4(X0))
& minCardinality(X0,has_part_0,"1",chromosome_0)
& has_part_2(X0,fn_cell_2(X0))
& has_part_2(X0,fn_cell_25(X0))
& has_part_2(X0,fn_cell_24(X0))
& has_part_2(X0,fn_cell_8(X0))
& has_part_2(X0,fn_cell_14(X0))
& has_part_2(X0,fn_cell_30(X0))
& is_inside_2(fn_cell_28(X0),fn_cell_30(X0))
& has_part_2(fn_cell_28(X0),fn_cell_9(X0))
& the_cardinal_value_2(fn_cell_20(X0),"100.0e0")
& the_cardinal_value_2(fn_cell_19(X0),"0.1e0")
& is_inside_2(fn_cell_14(X0),fn_cell_29(X0))
& is_oriented_toward_2(fn_cell_27(X0),fn_cell_28(X0))
& is_at_2(fn_cell_26(X0),fn_cell_4(X0))
& has_part_2(X0,fn_cell_28(X0))
& has_part_2(fn_cell_28(X0),fn_cell_29(X0))
& has_region_2(fn_cell_30(X0),fn_cell_27(X0))
& has_part_2(fn_cell_30(X0),fn_cell_26(X0))
& is_facing_2(fn_cell_27(X0),fn_cell_28(X0))
& X0 = fn_cytoplasm_7(fn_cell_28(X0))
& fn_cell_29(X0) = fn_mixture_1(fn_cell_28(X0))
& fn_cell_29(X0) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cell_27(X0) = fn_biomembrane_47(fn_cell_30(X0))
& fn_cell_27(X0) = fn_plasma_membrane_66(fn_cell_30(X0))
& fn_cell_26(X0) = fn_biomembrane_63(fn_cell_30(X0))
& fn_cell_26(X0) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_cell_28(X0) = fn_cytoplasmic_side_1(fn_cell_27(X0))
& fn_mixture_1(fn_cell_28(X0)) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cytoplasm_8(fn_cell_28(X0)) = fn_biomembrane_63(fn_cell_30(X0))
& fn_biomembrane_63(fn_cell_30(X0)) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_plasma_membrane_71(fn_cell_30(X0)) = fn_biomembrane_47(fn_cell_30(X0))
& fn_biomembrane_47(fn_cell_30(X0)) = fn_plasma_membrane_66(fn_cell_30(X0)) )
| ~ cell_1(X0) ),
inference(ennf_transformation,[],[f28465]) ).
fof(f31749,definition,
! [X0] :
( ( living_entity_1(X0)
& cell_pole_1(fn_cell_1(X0))
& cytoskeleton_1(fn_cell_2(X0))
& shape_value_1(fn_cell_5(X0))
& motor_protein_1(fn_cell_8(X0))
& protein_enzyme_1(fn_cell_9(X0))
& structural_complexity_value_1(fn_cell_13(X0))
& ribosome_1(fn_cell_14(X0))
& membrane_potential_1(fn_cell_21(X0))
& genome_1(fn_cell_24(X0))
& chromosome_1(fn_cell_25(X0))
& tangible_entity_1(fn_cell_26(X0))
& phospholipid_bilayer_1(fn_cell_26(X0))
& cytoplasmic_side_1(fn_cell_27(X0))
& mixture_1(fn_cell_28(X0))
& cytoplasm_1(fn_cell_28(X0))
& substance_1(fn_cell_29(X0))
& cytosol_1(fn_cell_29(X0))
& plasma_membrane_1(fn_cell_30(X0))
& cell_1(fn_cytoplasm_7(fn_cell_28(X0)))
& cytoplasm_1(fn_cytoplasmic_side_1(fn_cell_27(X0)))
& substance_1(fn_mixture_1(fn_cell_28(X0)))
& cytosol_1(fn_cytoplasm_8(fn_cell_28(X0)))
& tangible_entity_1(fn_biomembrane_63(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_biomembrane_63(fn_cell_30(X0)))
& tangible_entity_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& cytoplasmic_side_1(fn_plasma_membrane_66(fn_cell_30(X0)))
& is_across_2(fn_cell_21(X0),fn_cell_30(X0))
& shape_2(X0,fn_cell_5(X0))
& specific_surface_area_2(X0,fn_cell_7(X0))
& size_2(X0,fn_cell_11(X0))
& structural_complexity_2(X0,fn_cell_13(X0))
& diameter_2(X0,fn_cell_18(X0))
& volume_2(X0,fn_cell_22(X0))
& exactCardinality(X0,has_region_0,"2",cell_pole_0)
& has_region_2(X0,fn_cell_1(X0))
& has_region_2(X0,fn_cell_4(X0))
& minCardinality(X0,has_part_0,"1",chromosome_0)
& has_part_2(X0,fn_cell_2(X0))
& has_part_2(X0,fn_cell_25(X0))
& has_part_2(X0,fn_cell_24(X0))
& has_part_2(X0,fn_cell_8(X0))
& has_part_2(X0,fn_cell_14(X0))
& has_part_2(X0,fn_cell_30(X0))
& is_inside_2(fn_cell_28(X0),fn_cell_30(X0))
& has_part_2(fn_cell_28(X0),fn_cell_9(X0))
& the_cardinal_value_2(fn_cell_20(X0),"100.0e0")
& the_cardinal_value_2(fn_cell_19(X0),"0.1e0")
& is_inside_2(fn_cell_14(X0),fn_cell_29(X0))
& is_oriented_toward_2(fn_cell_27(X0),fn_cell_28(X0))
& is_at_2(fn_cell_26(X0),fn_cell_4(X0))
& has_part_2(X0,fn_cell_28(X0))
& has_part_2(fn_cell_28(X0),fn_cell_29(X0))
& has_region_2(fn_cell_30(X0),fn_cell_27(X0))
& has_part_2(fn_cell_30(X0),fn_cell_26(X0))
& is_facing_2(fn_cell_27(X0),fn_cell_28(X0))
& X0 = fn_cytoplasm_7(fn_cell_28(X0))
& fn_cell_29(X0) = fn_mixture_1(fn_cell_28(X0))
& fn_cell_29(X0) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cell_27(X0) = fn_biomembrane_47(fn_cell_30(X0))
& fn_cell_27(X0) = fn_plasma_membrane_66(fn_cell_30(X0))
& fn_cell_26(X0) = fn_biomembrane_63(fn_cell_30(X0))
& fn_cell_26(X0) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_cell_28(X0) = fn_cytoplasmic_side_1(fn_cell_27(X0))
& fn_mixture_1(fn_cell_28(X0)) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cytoplasm_8(fn_cell_28(X0)) = fn_biomembrane_63(fn_cell_30(X0))
& fn_biomembrane_63(fn_cell_30(X0)) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_plasma_membrane_71(fn_cell_30(X0)) = fn_biomembrane_47(fn_cell_30(X0))
& fn_biomembrane_47(fn_cell_30(X0)) = fn_plasma_membrane_66(fn_cell_30(X0)) )
| ~ sP6(X0) ),
introduced(definition,[new_symbols(definition,[sP6])],[predicate_definition_introduction]) ).
fof(f31750,plain,
! [X0] :
( sP6(X0)
| ~ cell_1(X0) ),
inference(definition_folding,[],[f28794,f31749]) ).
fof(f34065,plain,
! [X0] :
( ( living_entity_1(X0)
& cell_pole_1(fn_cell_1(X0))
& cytoskeleton_1(fn_cell_2(X0))
& shape_value_1(fn_cell_5(X0))
& motor_protein_1(fn_cell_8(X0))
& protein_enzyme_1(fn_cell_9(X0))
& structural_complexity_value_1(fn_cell_13(X0))
& ribosome_1(fn_cell_14(X0))
& membrane_potential_1(fn_cell_21(X0))
& genome_1(fn_cell_24(X0))
& chromosome_1(fn_cell_25(X0))
& tangible_entity_1(fn_cell_26(X0))
& phospholipid_bilayer_1(fn_cell_26(X0))
& cytoplasmic_side_1(fn_cell_27(X0))
& mixture_1(fn_cell_28(X0))
& cytoplasm_1(fn_cell_28(X0))
& substance_1(fn_cell_29(X0))
& cytosol_1(fn_cell_29(X0))
& plasma_membrane_1(fn_cell_30(X0))
& cell_1(fn_cytoplasm_7(fn_cell_28(X0)))
& cytoplasm_1(fn_cytoplasmic_side_1(fn_cell_27(X0)))
& substance_1(fn_mixture_1(fn_cell_28(X0)))
& cytosol_1(fn_cytoplasm_8(fn_cell_28(X0)))
& tangible_entity_1(fn_biomembrane_63(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_biomembrane_63(fn_cell_30(X0)))
& tangible_entity_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& phospholipid_bilayer_1(fn_plasma_membrane_71(fn_cell_30(X0)))
& cytoplasmic_side_1(fn_plasma_membrane_66(fn_cell_30(X0)))
& is_across_2(fn_cell_21(X0),fn_cell_30(X0))
& shape_2(X0,fn_cell_5(X0))
& specific_surface_area_2(X0,fn_cell_7(X0))
& size_2(X0,fn_cell_11(X0))
& structural_complexity_2(X0,fn_cell_13(X0))
& diameter_2(X0,fn_cell_18(X0))
& volume_2(X0,fn_cell_22(X0))
& exactCardinality(X0,has_region_0,"2",cell_pole_0)
& has_region_2(X0,fn_cell_1(X0))
& has_region_2(X0,fn_cell_4(X0))
& minCardinality(X0,has_part_0,"1",chromosome_0)
& has_part_2(X0,fn_cell_2(X0))
& has_part_2(X0,fn_cell_25(X0))
& has_part_2(X0,fn_cell_24(X0))
& has_part_2(X0,fn_cell_8(X0))
& has_part_2(X0,fn_cell_14(X0))
& has_part_2(X0,fn_cell_30(X0))
& is_inside_2(fn_cell_28(X0),fn_cell_30(X0))
& has_part_2(fn_cell_28(X0),fn_cell_9(X0))
& the_cardinal_value_2(fn_cell_20(X0),"100.0e0")
& the_cardinal_value_2(fn_cell_19(X0),"0.1e0")
& is_inside_2(fn_cell_14(X0),fn_cell_29(X0))
& is_oriented_toward_2(fn_cell_27(X0),fn_cell_28(X0))
& is_at_2(fn_cell_26(X0),fn_cell_4(X0))
& has_part_2(X0,fn_cell_28(X0))
& has_part_2(fn_cell_28(X0),fn_cell_29(X0))
& has_region_2(fn_cell_30(X0),fn_cell_27(X0))
& has_part_2(fn_cell_30(X0),fn_cell_26(X0))
& is_facing_2(fn_cell_27(X0),fn_cell_28(X0))
& X0 = fn_cytoplasm_7(fn_cell_28(X0))
& fn_cell_29(X0) = fn_mixture_1(fn_cell_28(X0))
& fn_cell_29(X0) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cell_27(X0) = fn_biomembrane_47(fn_cell_30(X0))
& fn_cell_27(X0) = fn_plasma_membrane_66(fn_cell_30(X0))
& fn_cell_26(X0) = fn_biomembrane_63(fn_cell_30(X0))
& fn_cell_26(X0) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_cell_28(X0) = fn_cytoplasmic_side_1(fn_cell_27(X0))
& fn_mixture_1(fn_cell_28(X0)) = fn_cytoplasm_8(fn_cell_28(X0))
& fn_cytoplasm_8(fn_cell_28(X0)) = fn_biomembrane_63(fn_cell_30(X0))
& fn_biomembrane_63(fn_cell_30(X0)) = fn_plasma_membrane_71(fn_cell_30(X0))
& fn_plasma_membrane_71(fn_cell_30(X0)) = fn_biomembrane_47(fn_cell_30(X0))
& fn_biomembrane_47(fn_cell_30(X0)) = fn_plasma_membrane_66(fn_cell_30(X0)) )
| ~ sP6(X0) ),
inference(nnf_transformation,[],[f31749]) ).
fof(f35220,plain,
cell_1(a_cell),
inference(cnf_transformation,[],[f9161]) ).
fof(f35221,plain,
~ cytoskeleton_1(fn_cell_2(a_cell)),
inference(cnf_transformation,[],[f9164]) ).
fof(f38960,plain,
! [X0] :
( cytoskeleton_1(fn_cell_2(X0))
| ~ sP6(X0) ),
inference(cnf_transformation,[],[f34065]) ).
fof(f38963,plain,
! [X0] :
( ~ cell_1(X0)
| sP6(X0) ),
inference(cnf_transformation,[],[f31750]) ).
fof(f210722,plain,
sP6(a_cell),
inference(resolution,[],[f38963,f35220]) ).
fof(f211398,plain,
~ sP6(a_cell),
inference(resolution,[],[f38960,f35221]) ).
fof(f211400,plain,
$false,
inference(forward_subsumption_resolution,[],[f211398,f210722]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BIO003+1 : TPTP v9.3.1. Bugfixed v6.4.1.
% 0.00/0.06 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 % Computer : n026.cluster.edu
% 0.09/0.23 % Model : x86_64 x86_64
% 0.09/0.23 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.23 % Memory : 8046.5625MB
% 0.09/0.23 % OS : Linux 6.8.0-71-generic
% 0.09/0.23 % CPULimit : 300
% 0.09/0.23 % WCLimit : 300
% 0.09/0.23 % DateTime : Mon Sep 28 21:05:27 UTC 2026
% 0.09/0.23 % CPUTime :
% 0.09/0.23 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.20/0.26 Running first-order theorem proving
% 0.20/0.26 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.86/6.55 % (71917)Detected formulas, will run a generic FOF schedule.
% 10.86/6.55 % (72084)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=1127676509:i=141695:sd=1:nm=32:gsp=on:ss=included_2950 on theBenchmark for (2950ds/141695Mi)
% 10.86/6.55 % (72082)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=907378325:i=141193_2950 on theBenchmark for (2950ds/141193Mi)
% 10.86/6.55 % (72086)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=90699595:i=119:av=off:ss=axioms_2950 on theBenchmark for (2950ds/119Mi)
% 10.86/6.55 % (72085)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=2464685137:i=109:sd=1:ins=1:gsp=on:ss=axioms_2950 on theBenchmark for (2950ds/109Mi)
% 10.86/6.55 % (72083)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=818824648:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2950 on theBenchmark for (2950ds/134677Mi)
% 10.86/6.55 % (72088)dis-21_1_sil=8000:lcm=predicate:random_seed=737376052:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2950 on theBenchmark for (2950ds/129Mi)
% 10.86/6.55 % (72087)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=98389922:s2a=on:i=139:gtg=position_2950 on theBenchmark for (2950ds/139Mi)
% 10.86/6.55 % (72086)Instruction limit reached!
% 10.86/6.55 % (72086)------------------------------
% 10.86/6.55 % (72086)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.86/6.55 % (72086)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.86/6.55 % (72086)CaDiCaL version: 2.1.3
% 10.86/6.55 % (72086)Termination reason: Instruction limit
% 10.86/6.55 % (72086)Termination phase: SInE selection
% 10.86/6.55 % (72086)Time elapsed: 0.062 s
% 10.86/6.55 % (72086)Peak memory usage: 181 MB
% 10.86/6.55 % (72086)Instructions burned: 121 (million)
% 10.86/6.55 % (72085)Instruction limit reached!
% 10.86/6.55 % (72085)------------------------------
% 10.86/6.55 % (72085)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.86/6.55 % (72085)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.86/6.55 % (72085)CaDiCaL version: 2.1.3
% 10.86/6.55 % (72085)Termination reason: Instruction limit
% 10.86/6.55 % (72085)Termination phase: SInE selection
% 10.86/6.55 % (72085)Time elapsed: 0.071 s
% 10.86/6.55 % (72085)Peak memory usage: 181 MB
% 10.86/6.55 % (72085)Instructions burned: 109 (million)
% 10.86/6.55 % (72088)Instruction limit reached!
% 10.86/6.55 % (72088)------------------------------
% 10.86/6.55 % (72088)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.86/6.55 % (72088)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.86/6.55 % (72088)CaDiCaL version: 2.1.3
% 10.86/6.55 % (72088)Termination reason: Instruction limit
% 10.86/6.55 % (72088)Termination phase: SInE selection
% 10.86/6.55 % (72088)Time elapsed: 0.067 s
% 10.86/6.55 % (72088)Peak memory usage: 181 MB
% 10.86/6.55 % (72088)Instructions burned: 130 (million)
% 10.86/6.55 % (72087)Instruction limit reached!
% 10.86/6.55 % (72087)------------------------------
% 10.86/6.55 % (72087)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 10.86/6.55 % (72087)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 10.86/6.55 % (72087)CaDiCaL version: 2.1.3
% 10.86/6.55 % (72087)Termination reason: Instruction limit
% 10.86/6.55 % (72087)Termination phase: Property scanning
% 10.86/6.55 % (72087)Time elapsed: 0.082 s
% 10.86/6.55 % (72087)Peak memory usage: 181 MB
% 10.86/6.55 % (72087)Instructions burned: 142 (million)
% 10.86/6.55 % (72096)lrs+10_1_sil=8000:sp=occurrence:random_seed=3097725535:i=285:sd=3:ss=axioms:sgt=8_2948 on theBenchmark for (2948ds/285Mi)
% 10.86/6.55 % (72097)lrs+10_1_sil=32000:urr=on:br=off:random_seed=984913886:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2948 on theBenchmark for (2948ds/157Mi)
% 10.86/6.55 % (72098)lrs+1011_1_sil=32000:sp=occurrence:random_seed=651590250:i=325:sd=1:ss=axioms:sgt=32_2948 on theBenchmark for (2948ds/325Mi)
% 10.86/6.55 % (72099)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=695806704:s2a=on:i=248:s2at=1.23:gtg=position_2948 on theBenchmark for (2948ds/248Mi)
% 10.86/6.55 % (72097)Instruction limit reached!
% 10.86/6.55 % (72097)------------------------------
% 10.86/6.55 % (72097)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.46/7.10 % (72097)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.46/7.10 % (72097)CaDiCaL version: 2.1.3
% 15.46/7.10 % (72097)Termination reason: Instruction limit
% 15.46/7.10 % (72097)Termination phase: Property scanning
% 15.46/7.10 % (72097)Time elapsed: 0.087 s
% 15.46/7.10 % (72097)Peak memory usage: 182 MB
% 15.46/7.10 % (72097)Instructions burned: 159 (million)
% 15.46/7.10 % (72096)Instruction limit reached!
% 15.46/7.10 % (72096)------------------------------
% 15.46/7.10 % (72096)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.46/7.10 % (72096)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.46/7.10 % (72096)CaDiCaL version: 2.1.3
% 15.46/7.10 % (72096)Termination reason: Instruction limit
% 15.46/7.10 % (72096)Termination phase: SInE selection
% 15.46/7.10 % (72096)Time elapsed: 0.133 s
% 15.46/7.10 % (72096)Peak memory usage: 181 MB
% 15.46/7.10 % (72096)Instructions burned: 285 (million)
% 15.46/7.10 % (72099)Instruction limit reached!
% 15.46/7.10 % (72099)------------------------------
% 15.46/7.10 % (72099)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.46/7.10 % (72099)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.46/7.10 % (72099)CaDiCaL version: 2.1.3
% 15.46/7.10 % (72099)Termination reason: Instruction limit
% 15.46/7.10 % (72099)Termination phase: Property scanning
% 15.46/7.10 % (72099)Time elapsed: 0.122 s
% 15.46/7.10 % (72099)Peak memory usage: 182 MB
% 15.46/7.10 % (72099)Instructions burned: 250 (million)
% 15.46/7.10 % (72104)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=3120542472:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2946 on theBenchmark for (2946ds/294Mi)
% 15.46/7.10 % (72098)Instruction limit reached!
% 15.46/7.10 % (72098)------------------------------
% 15.46/7.10 % (72098)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.46/7.10 % (72098)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.46/7.10 % (72098)CaDiCaL version: 2.1.3
% 15.46/7.10 % (72098)Termination reason: Instruction limit
% 15.46/7.10 % (72098)Termination phase: SInE selection
% 15.46/7.10 % (72098)Time elapsed: 0.221 s
% 15.46/7.10 % (72098)Peak memory usage: 181 MB
% 15.46/7.10 % (72098)Instructions burned: 326 (million)
% 15.46/7.10 % (72105)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3455805875:i=2350_2945 on theBenchmark for (2945ds/2350Mi)
% 15.46/7.10 % (72106)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=279770580:cts=off:i=113:fsr=off:ss=included:sgt=4_2945 on theBenchmark for (2945ds/113Mi)
% 15.46/7.10 % (72104)Instruction limit reached!
% 15.46/7.10 % (72104)------------------------------
% 15.46/7.10 % (72104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.46/7.10 % (72104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.46/7.10 % (72104)CaDiCaL version: 2.1.3
% 15.46/7.10 % (72104)Termination reason: Instruction limit
% 15.46/7.10 % (72104)Termination phase: SInE selection
% 15.46/7.10 % (72104)Time elapsed: 0.132 s
% 15.46/7.10 % (72104)Peak memory usage: 181 MB
% 15.46/7.10 % (72104)Instructions burned: 297 (million)
% 15.46/7.10 % (72106)Instruction limit reached!
% 15.46/7.10 % (72106)------------------------------
% 15.46/7.10 % (72106)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 15.46/7.10 % (72106)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 15.46/7.10 % (72106)CaDiCaL version: 2.1.3
% 15.46/7.10 % (72106)Termination reason: Instruction limit
% 15.46/7.10 % (72106)Termination phase: SInE selection
% 15.46/7.10 % (72106)Time elapsed: 0.058 s
% 15.46/7.10 % (72106)Peak memory usage: 181 MB
% 15.46/7.10 % (72106)Instructions burned: 114 (million)
% 15.46/7.10 % (72108)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=1241540560:i=127:av=off:fsr=off:sup=off_2944 on theBenchmark for (2944ds/127Mi)
% 15.46/7.10 [W928 21:05:33.759575832 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 15.46/7.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 15.46/7.10 [W928 21:05:33.759595983 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 15.46/7.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.26/7.77 [W928 21:05:33.759627314 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.26/7.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.26/7.77 [W928 21:05:33.759643366 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.26/7.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.26/7.77 [W928 21:05:33.759658023 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.26/7.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.26/7.77 [W928 21:05:33.759663436 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.26/7.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.26/7.77 [W928 21:05:33.759677285 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.26/7.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.26/7.77 [W928 21:05:33.759682676 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.26/7.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.26/7.77 [W928 21:05:33.759696237 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.26/7.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.26/7.77 [W928 21:05:33.759701673 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.26/7.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.26/7.77 [W928 21:05:33.759716955 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.26/7.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.26/7.77 [W928 21:05:33.759722317 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.26/7.77 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.26/7.77 % (72108)Instruction limit reached!
% 19.26/7.77 % (72108)------------------------------
% 19.26/7.77 % (72108)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 19.26/7.77 % (72108)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 19.26/7.77 % (72108)CaDiCaL version: 2.1.3
% 19.26/7.77 % (72108)Termination reason: Instruction limit
% 19.26/7.77 % (72108)Termination phase: Preprocessing 1
% 19.26/7.77 % (72108)Time elapsed: 0.080 s
% 19.26/7.77 % (72108)Peak memory usage: 181 MB
% 19.26/7.77 % (72108)Instructions burned: 127 (million)
% 19.26/7.77 % (72111)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3650202027:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2943 on theBenchmark for (2943ds/114Mi)
% 19.26/7.77 % (72113)lrs+10_1_sil=8000:sp=occurrence:random_seed=561640393:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2943 on theBenchmark for (2943ds/907Mi)
% 19.26/7.77 % (72111)Instruction limit reached!
% 19.26/7.77 % (72111)------------------------------
% 20.31/7.97 % (72111)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.31/7.97 % (72111)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.31/7.97 % (72111)CaDiCaL version: 2.1.3
% 20.31/7.97 % (72111)Termination reason: Instruction limit
% 20.31/7.97 % (72111)Termination phase: Property scanning
% 20.31/7.97 % (72111)Time elapsed: 0.072 s
% 20.31/7.97 % (72111)Peak memory usage: 181 MB
% 20.31/7.97 % (72111)Instructions burned: 115 (million)
% 20.31/7.97 % (72114)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=2487014844:i=437:sd=1:aac=none:ss=included_2942 on theBenchmark for (2942ds/437Mi)
% 20.31/7.97 % (72117)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2832835823:i=5202:ss=axioms:sgt=16_2941 on theBenchmark for (2941ds/5202Mi)
% 20.31/7.97 % (72114)Instruction limit reached!
% 20.31/7.97 % (72114)------------------------------
% 20.31/7.97 % (72114)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.31/7.97 % (72114)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.31/7.97 % (72114)CaDiCaL version: 2.1.3
% 20.31/7.97 % (72114)Termination reason: Instruction limit
% 20.31/7.97 % (72114)Termination phase: SInE selection
% 20.31/7.97 % (72114)Time elapsed: 0.204 s
% 20.31/7.97 % (72114)Peak memory usage: 181 MB
% 20.31/7.97 % (72114)Instructions burned: 443 (million)
% 20.31/7.97 % (72113)Refutation not found, incomplete strategy
% 20.31/7.97 % (72113)------------------------------
% 20.31/7.97 % (72113)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.31/7.97 % (72113)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.31/7.97 % (72113)CaDiCaL version: 2.1.3
% 20.31/7.97 % (72113)Termination reason: Refutation not found, incomplete strategy
% 20.31/7.97 % (72113)Time elapsed: 0.311 s
% 20.31/7.97 % (72113)Peak memory usage: 187 MB
% 20.31/7.97 % (72113)Instructions burned: 557 (million)
% 20.31/7.97 % (72120)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=2910481143:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2939 on theBenchmark for (2939ds/134Mi)
% 20.31/7.97 % (72120)Instruction limit reached!
% 20.31/7.97 % (72120)------------------------------
% 20.31/7.97 % (72120)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 20.31/7.97 % (72120)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 20.31/7.97 % (72120)CaDiCaL version: 2.1.3
% 20.31/7.97 % (72120)Termination reason: Instruction limit
% 20.31/7.97 % (72120)Termination phase: SInE selection
% 20.31/7.97 % (72120)Time elapsed: 0.070 s
% 20.31/7.97 % (72120)Peak memory usage: 181 MB
% 20.31/7.97 % (72120)Instructions burned: 136 (million)
% 20.31/7.97 % (72113)------------------------------
% 20.31/7.97 % (72113)------------------------------
% 20.31/7.97 [W928 21:05:34.504067328 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.31/7.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.31/7.97 [W928 21:05:34.504103918 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.31/7.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.31/7.97 [W928 21:05:34.504154861 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.31/7.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.31/7.97 [W928 21:05:34.504168385 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.31/7.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.31/7.97 [W928 21:05:34.504195345 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 20.31/7.97 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 20.31/7.97 [W928 21:05:34.504207338 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 30.25/9.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.25/9.14 [W928 21:05:34.504234278 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 30.25/9.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.25/9.14 [W928 21:05:34.504245288 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 30.25/9.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.25/9.14 [W928 21:05:34.504271275 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 30.25/9.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.25/9.14 [W928 21:05:34.504282128 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 30.25/9.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.25/9.14 [W928 21:05:34.504307082 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 30.25/9.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.25/9.14 [W928 21:05:34.504317918 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 30.25/9.14 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 30.25/9.14 % (72122)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=275645237:st=8:i=592:sd=3:ep=RST:ss=axioms_2936 on theBenchmark for (2936ds/592Mi)
% 30.25/9.14 % (72123)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=2802901689:st=3:i=13193:sd=3:ss=axioms_2935 on theBenchmark for (2935ds/13193Mi)
% 30.25/9.14 % (72084)Refutation not found, incomplete strategy
% 30.25/9.14 % (72084)------------------------------
% 30.25/9.14 % (72084)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.25/9.14 % (72084)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.25/9.14 % (72084)CaDiCaL version: 2.1.3
% 30.25/9.14 % (72084)Termination reason: Refutation not found, incomplete strategy
% 30.25/9.14 % (72084)Time elapsed: 1.636 s
% 30.25/9.14 % (72084)Peak memory usage: 580 MB
% 30.25/9.14 % (72084)Instructions burned: 4000 (million)
% 30.25/9.14 % (72122)Instruction limit reached!
% 30.25/9.14 % (72122)------------------------------
% 30.25/9.14 % (72122)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.25/9.14 % (72122)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.25/9.14 % (72122)CaDiCaL version: 2.1.3
% 30.25/9.14 % (72122)Termination reason: Instruction limit
% 30.25/9.14 % (72122)Termination phase: SInE selection
% 30.25/9.14 % (72122)Time elapsed: 0.274 s
% 30.25/9.14 % (72122)Peak memory usage: 182 MB
% 30.25/9.14 % (72122)Instructions burned: 592 (million)
% 30.25/9.14 % (72084)------------------------------
% 30.25/9.14 % (72084)------------------------------
% 30.25/9.14 % (72133)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=3114970391:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2932 on theBenchmark for (2932ds/125Mi)
% 30.25/9.14 % (72105)Instruction limit reached!
% 30.25/9.14 % (72105)------------------------------
% 30.25/9.14 % (72105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 30.25/9.14 % (72105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 30.25/9.14 % (72105)CaDiCaL version: 2.1.3
% 32.09/9.48 % (72105)Termination reason: Instruction limit
% 32.09/9.48 % (72105)Termination phase: Preprocessing 3
% 32.09/9.48 % (72105)Time elapsed: 1.531 s
% 32.09/9.48 % (72105)Peak memory usage: 218 MB
% 32.09/9.48 % (72105)Instructions burned: 2351 (million)
% 32.09/9.48 % (72133)Instruction limit reached!
% 32.09/9.48 % (72133)------------------------------
% 32.09/9.48 % (72133)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.09/9.48 % (72133)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.09/9.48 % (72133)CaDiCaL version: 2.1.3
% 32.09/9.48 % (72133)Termination reason: Instruction limit
% 32.09/9.48 % (72133)Termination phase: Property scanning
% 32.09/9.48 % (72133)Time elapsed: 0.115 s
% 32.09/9.48 % (72133)Peak memory usage: 182 MB
% 32.09/9.48 % (72133)Instructions burned: 125 (million)
% 32.09/9.48 % (72144)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=3817926311:i=134:gtgl=5:slsql=off:gtg=exists_sym_2930 on theBenchmark for (2930ds/134Mi)
% 32.09/9.48 % (72144)Instruction limit reached!
% 32.09/9.48 % (72144)------------------------------
% 32.09/9.48 % (72144)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 32.09/9.48 % (72144)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 32.09/9.48 % (72144)CaDiCaL version: 2.1.3
% 32.09/9.48 % (72144)Termination reason: Instruction limit
% 32.09/9.48 % (72144)Termination phase: Property scanning
% 32.09/9.48 % (72144)Time elapsed: 0.077 s
% 32.09/9.48 % (72144)Peak memory usage: 182 MB
% 32.09/9.48 % (72144)Instructions burned: 135 (million)
% 32.09/9.48 [W928 21:05:35.372174962 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.09/9.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.09/9.48 [W928 21:05:35.372209992 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.09/9.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.09/9.48 [W928 21:05:35.372266519 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.09/9.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.09/9.48 [W928 21:05:35.372279286 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.09/9.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.09/9.48 [W928 21:05:35.372305072 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.09/9.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.09/9.48 [W928 21:05:35.372316156 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.09/9.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.09/9.48 [W928 21:05:35.372340826 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.09/9.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.09/9.48 [W928 21:05:35.372351809 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 32.09/9.48 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 32.09/9.48 [W928 21:05:35.372377216 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 45.46/11.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 45.46/11.35 [W928 21:05:35.372388189 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 45.46/11.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 45.46/11.35 [W928 21:05:35.372420179 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 45.46/11.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 45.46/11.35 [W928 21:05:35.372430209 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 45.46/11.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 45.46/11.35 % (72147)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=3304033998:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2929 on theBenchmark for (2929ds/141Mi)
% 45.46/11.35 % (72148)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=1797858585:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2928 on theBenchmark for (2928ds/431Mi)
% 45.46/11.35 % (72147)Instruction limit reached!
% 45.46/11.35 % (72147)------------------------------
% 45.46/11.35 % (72147)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.46/11.35 % (72147)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.46/11.35 % (72147)CaDiCaL version: 2.1.3
% 45.46/11.35 % (72147)Termination reason: Instruction limit
% 45.46/11.35 % (72147)Termination phase: SInE selection
% 45.46/11.35 % (72147)Time elapsed: 0.103 s
% 45.46/11.35 % (72147)Peak memory usage: 181 MB
% 45.46/11.35 % (72147)Instructions burned: 141 (million)
% 45.46/11.35 % (72154)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=1559695692:i=6060:aac=none:ins=25_2927 on theBenchmark for (2927ds/6060Mi)
% 45.46/11.35 % (72148)Instruction limit reached!
% 45.46/11.35 % (72148)------------------------------
% 45.46/11.35 % (72148)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.46/11.35 % (72148)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.46/11.35 % (72148)CaDiCaL version: 2.1.3
% 45.46/11.35 % (72148)Termination reason: Instruction limit
% 45.46/11.35 % (72148)Termination phase: SInE selection
% 45.46/11.35 % (72148)Time elapsed: 0.312 s
% 45.46/11.35 % (72148)Peak memory usage: 182 MB
% 45.46/11.35 % (72148)Instructions burned: 431 (million)
% 45.46/11.35 % (72161)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=708196151:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2925 on theBenchmark for (2925ds/150Mi)
% 45.46/11.35 % (72161)Instruction limit reached!
% 45.46/11.35 % (72161)------------------------------
% 45.46/11.35 % (72161)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 45.46/11.35 % (72161)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 45.46/11.35 % (72161)CaDiCaL version: 2.1.3
% 45.46/11.35 % (72161)Termination reason: Instruction limit
% 45.46/11.35 % (72161)Termination phase: SInE selection
% 45.46/11.35 % (72161)Time elapsed: 0.113 s
% 45.46/11.35 % (72161)Peak memory usage: 181 MB
% 45.46/11.35 % (72161)Instructions burned: 150 (million)
% 45.46/11.35 % (72167)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2893315123:i=14155:bd=all_2923 on theBenchmark for (2923ds/14155Mi)
% 45.46/11.35 % (72170)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=2028234030:i=667:av=off:fsr=off_2922 on theBenchmark for (2922ds/667Mi)
% 45.46/11.35 [W928 21:05:36.545200257 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 45.46/11.35 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 45.46/11.35 [W928 21:05:36.545260997 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 51.80/12.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 51.80/12.21 [W928 21:05:36.545343847 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 51.80/12.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 51.80/12.21 [W928 21:05:36.545364084 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 51.80/12.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 51.80/12.21 [W928 21:05:36.545414087 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 51.80/12.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 51.80/12.21 [W928 21:05:36.545433244 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 51.80/12.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 51.80/12.21 [W928 21:05:36.545479910 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 51.80/12.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 51.80/12.21 [W928 21:05:36.545497294 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 51.80/12.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 51.80/12.21 [W928 21:05:36.545539491 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 51.80/12.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 51.80/12.21 [W928 21:05:36.545556637 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 51.80/12.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 51.80/12.21 [W928 21:05:36.545603377 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 51.80/12.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 51.80/12.21 [W928 21:05:36.545622677 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 51.80/12.21 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 51.80/12.21 % (72083)Refutation not found, incomplete strategy
% 51.80/12.21 % (72083)------------------------------
% 51.80/12.21 % (72083)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 51.80/12.21 % (72083)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 51.80/12.21 % (72083)CaDiCaL version: 2.1.3
% 51.80/12.21 % (72083)Termination reason: Refutation not found, incomplete strategy
% 51.80/12.21 % (72083)Time elapsed: 3.459 s
% 51.80/12.21 % (72083)Peak memory usage: 600 MB
% 51.80/12.21 % (72083)Instructions burned: 4306 (million)
% 51.80/12.21 % (72170)Instruction limit reached!
% 51.80/12.21 % (72170)------------------------------
% 51.80/12.21 % (72170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.34/13.62 % (72170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.34/13.62 % (72170)CaDiCaL version: 2.1.3
% 61.34/13.62 % (72170)Termination reason: Instruction limit
% 61.34/13.62 % (72170)Termination phase: Unused predicate definition removal
% 61.34/13.62 % (72170)Time elapsed: 0.781 s
% 61.34/13.62 % (72170)Peak memory usage: 208 MB
% 61.34/13.62 % (72170)Instructions burned: 667 (million)
% 61.34/13.62 % (72182)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=126708025:s2a=on:i=185:s2at=1.8:fdi=4_2911 on theBenchmark for (2911ds/185Mi)
% 61.34/13.62 % (72083)------------------------------
% 61.34/13.62 % (72083)------------------------------
% 61.34/13.62 % (72182)Instruction limit reached!
% 61.34/13.62 % (72182)------------------------------
% 61.34/13.62 % (72182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.34/13.62 % (72182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.34/13.62 % (72182)CaDiCaL version: 2.1.3
% 61.34/13.62 % (72182)Termination reason: Instruction limit
% 61.34/13.62 % (72182)Termination phase: SInE selection
% 61.34/13.62 % (72182)Time elapsed: 0.139 s
% 61.34/13.62 % (72182)Peak memory usage: 181 MB
% 61.34/13.62 % (72182)Instructions burned: 186 (million)
% 61.34/13.62 % (72187)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=3503703158:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2908 on theBenchmark for (2908ds/193Mi)
% 61.34/13.62 % (72117)Refutation not found, incomplete strategy
% 61.34/13.62 % (72117)------------------------------
% 61.34/13.62 % (72117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.34/13.62 % (72117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.34/13.62 % (72117)CaDiCaL version: 2.1.3
% 61.34/13.62 % (72117)Termination reason: Refutation not found, incomplete strategy
% 61.34/13.62 % (72117)Time elapsed: 3.343 s
% 61.34/13.62 % (72117)Peak memory usage: 530 MB
% 61.34/13.62 % (72117)Instructions burned: 4008 (million)
% 61.34/13.62 % (72187)Instruction limit reached!
% 61.34/13.62 % (72187)------------------------------
% 61.34/13.62 % (72187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.34/13.62 % (72187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.34/13.62 % (72187)CaDiCaL version: 2.1.3
% 61.34/13.62 % (72187)Termination reason: Instruction limit
% 61.34/13.62 % (72187)Termination phase: SInE selection
% 61.34/13.62 % (72187)Time elapsed: 0.156 s
% 61.34/13.62 % (72187)Peak memory usage: 181 MB
% 61.34/13.62 % (72187)Instructions burned: 194 (million)
% 61.34/13.62 % (72188)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=2833087084:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2908 on theBenchmark for (2908ds/4850Mi)
% 61.34/13.62 % (72191)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=1619354476:i=12111:sd=1:ss=included_2905 on theBenchmark for (2905ds/12111Mi)
% 61.34/13.62 % (72117)------------------------------
% 61.34/13.62 % (72117)------------------------------
% 61.34/13.62 % (72188)Refutation not found, incomplete strategy
% 61.34/13.62 % (72188)------------------------------
% 61.34/13.62 % (72188)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.34/13.62 % (72188)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.34/13.62 % (72188)CaDiCaL version: 2.1.3
% 61.34/13.62 % (72188)Termination reason: Refutation not found, incomplete strategy
% 61.34/13.62 % (72188)Time elapsed: 0.508 s
% 61.34/13.62 % (72188)Peak memory usage: 187 MB
% 61.34/13.62 % (72188)Instructions burned: 568 (million)
% 61.34/13.62 % (72199)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=2749894353:i=319:kws=precedence:fsr=off_2900 on theBenchmark for (2900ds/319Mi)
% 61.34/13.62 % (72199)Instruction limit reached!
% 61.34/13.62 % (72199)------------------------------
% 61.34/13.62 % (72199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 61.34/13.62 % (72199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 61.34/13.62 % (72199)CaDiCaL version: 2.1.3
% 61.34/13.62 % (72199)Termination reason: Instruction limit
% 61.34/13.62 % (72199)Termination phase: Preprocessing 1
% 61.34/13.62 % (72199)Time elapsed: 0.282 s
% 61.34/13.62 % (72199)Peak memory usage: 181 MB
% 61.34/13.62 % (72199)Instructions burned: 319 (million)
% 61.34/13.62 % (72188)------------------------------
% 61.34/13.62 % (72188)------------------------------
% 61.34/13.62 % (72206)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=3524674615:i=2064:ep=RST_2895 on theBenchmark for (2895ds/2064Mi)
% 71.00/14.98 % (72207)dis-1011_128_sil=32000:random_seed=407412636:i=3706:ep=RST:av=off_2894 on theBenchmark for (2894ds/3706Mi)
% 71.00/14.98 % (72123)Refutation not found, incomplete strategy
% 71.00/14.98 % (72123)------------------------------
% 71.00/14.98 % (72123)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.00/14.98 % (72123)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.00/14.98 % (72123)CaDiCaL version: 2.1.3
% 71.00/14.98 % (72123)Termination reason: Refutation not found, incomplete strategy
% 71.00/14.98 % (72123)Time elapsed: 4.422 s
% 71.00/14.98 % (72123)Peak memory usage: 300 MB
% 71.00/14.98 % (72123)Instructions burned: 4283 (million)
% 71.00/14.98 % (72154)Instruction limit reached!
% 71.00/14.98 % (72154)------------------------------
% 71.00/14.98 % (72154)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.00/14.98 % (72154)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.00/14.98 % (72154)CaDiCaL version: 2.1.3
% 71.00/14.98 % (72154)Termination reason: Instruction limit
% 71.00/14.98 % (72154)Termination phase: Saturation
% 71.00/14.98 % (72154)Time elapsed: 3.765 s
% 71.00/14.98 % (72154)Peak memory usage: 496 MB
% 71.00/14.98 % (72154)Instructions burned: 6060 (million)
% 71.00/14.98 [W928 21:05:39.607890704 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 71.00/14.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.00/14.98 [W928 21:05:39.607938361 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 71.00/14.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.00/14.98 [W928 21:05:39.608031741 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 71.00/14.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.00/14.98 [W928 21:05:39.608055808 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 71.00/14.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.00/14.98 [W928 21:05:39.608108635 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 71.00/14.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.00/14.98 [W928 21:05:39.608128208 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 71.00/14.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.00/14.98 [W928 21:05:39.608179315 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 71.00/14.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.00/14.98 [W928 21:05:39.608199788 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 71.00/14.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.00/14.98 [W928 21:05:39.608251518 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 71.00/14.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.00/14.98 [W928 21:05:39.608273128 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 87.50/17.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 87.50/17.25 [W928 21:05:39.608322098 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 87.50/17.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 87.50/17.25 [W928 21:05:39.608342552 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 87.50/17.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 87.50/17.25 % (72123)------------------------------
% 87.50/17.25 % (72123)------------------------------
% 87.50/17.25 % (72214)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=526629835:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2886 on theBenchmark for (2886ds/757Mi)
% 87.50/17.25 % (72216)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1526461267:i=13913:ss=axioms:sgt=8_2884 on theBenchmark for (2884ds/13913Mi)
% 87.50/17.25 % (72206)Instruction limit reached!
% 87.50/17.25 % (72206)------------------------------
% 87.50/17.25 % (72206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.50/17.25 % (72206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.50/17.25 % (72206)CaDiCaL version: 2.1.3
% 87.50/17.25 % (72206)Termination reason: Instruction limit
% 87.50/17.25 % (72206)Termination phase: Property scanning
% 87.50/17.25 % (72206)Time elapsed: 1.363 s
% 87.50/17.25 % (72206)Peak memory usage: 227 MB
% 87.50/17.25 % (72206)Instructions burned: 2065 (million)
% 87.50/17.25 % (72221)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=2197477158:i=9925:aac=none_2879 on theBenchmark for (2879ds/9925Mi)
% 87.50/17.25 % (72214)Instruction limit reached!
% 87.50/17.25 % (72214)------------------------------
% 87.50/17.25 % (72214)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 87.50/17.25 % (72214)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 87.50/17.25 % (72214)CaDiCaL version: 2.1.3
% 87.50/17.25 % (72214)Termination reason: Instruction limit
% 87.50/17.25 % (72214)Termination phase: Preprocessing 1
% 87.50/17.25 % (72214)Time elapsed: 0.719 s
% 87.50/17.25 % (72214)Peak memory usage: 184 MB
% 87.50/17.25 % (72214)Instructions burned: 757 (million)
% 87.50/17.25 % (72225)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=373262723:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2876 on theBenchmark for (2876ds/2479Mi)
% 87.50/17.25 [W928 21:05:40.019783430 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 87.50/17.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 87.50/17.25 [W928 21:05:40.019833870 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 87.50/17.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 87.50/17.25 [W928 21:05:40.019888102 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 87.50/17.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 87.50/17.25 [W928 21:05:40.019908029 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 87.50/17.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 87.50/17.25 [W928 21:05:40.019937556 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 103.91/19.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 103.91/19.60 [W928 21:05:40.019947642 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 103.91/19.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 103.91/19.60 [W928 21:05:40.019973751 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 103.91/19.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 103.91/19.60 [W928 21:05:40.019983705 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 103.91/19.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 103.91/19.60 [W928 21:05:41.020015002 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 103.91/19.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 103.91/19.60 [W928 21:05:41.020042206 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 103.91/19.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 103.91/19.60 [W928 21:05:41.020067468 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 103.91/19.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 103.91/19.60 [W928 21:05:41.020077078 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 103.91/19.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 103.91/19.60 % (72225)Refutation not found, incomplete strategy
% 103.91/19.60 % (72225)------------------------------
% 103.91/19.60 % (72225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.91/19.60 % (72225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.91/19.60 % (72225)CaDiCaL version: 2.1.3
% 103.91/19.60 % (72225)Termination reason: Refutation not found, incomplete strategy
% 103.91/19.60 % (72225)Time elapsed: 0.892 s
% 103.91/19.60 % (72225)Peak memory usage: 186 MB
% 103.91/19.60 % (72225)Instructions burned: 1245 (million)
% 103.91/19.60 % (72225)------------------------------
% 103.91/19.60 % (72225)------------------------------
% 103.91/19.60 % (72207)Instruction limit reached!
% 103.91/19.60 % (72207)------------------------------
% 103.91/19.60 % (72207)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.91/19.60 % (72207)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.91/19.60 % (72207)CaDiCaL version: 2.1.3
% 103.91/19.60 % (72207)Termination reason: Instruction limit
% 103.91/19.60 % (72207)Termination phase: Property scanning
% 103.91/19.60 % (72207)Time elapsed: 3.267 s
% 103.91/19.60 % (72207)Peak memory usage: 239 MB
% 103.91/19.60 % (72207)Instructions burned: 3707 (million)
% 103.91/19.60 % (72191)Refutation not found, incomplete strategy
% 103.91/19.60 % (72191)------------------------------
% 103.91/19.60 % (72191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 103.91/19.60 % (72191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 103.91/19.60 % (72191)CaDiCaL version: 2.1.3
% 103.91/19.60 % (72191)Termination reason: Refutation not found, incomplete strategy
% 103.91/19.60 % (72191)Time elapsed: 4.539 s
% 103.91/19.60 % (72191)Peak memory usage: 550 MB
% 103.91/19.60 % (72191)Instructions burned: 4037 (million)
% 103.91/19.60 % (72238)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=257963381:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2859 on theBenchmark for (2859ds/440Mi)
% 125.85/22.78 % (72239)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=3788858695:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2858 on theBenchmark for (2858ds/11145Mi)
% 125.85/22.78 % (72216)Refutation not found, incomplete strategy
% 125.85/22.78 % (72216)------------------------------
% 125.85/22.78 % (72216)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.85/22.78 % (72216)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.85/22.78 % (72216)CaDiCaL version: 2.1.3
% 125.85/22.78 % (72216)Termination reason: Refutation not found, incomplete strategy
% 125.85/22.78 % (72216)Time elapsed: 2.802 s
% 125.85/22.78 % (72216)Peak memory usage: 537 MB
% 125.85/22.78 % (72216)Instructions burned: 3872 (million)
% 125.85/22.78 % (72238)Instruction limit reached!
% 125.85/22.78 % (72238)------------------------------
% 125.85/22.78 % (72238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.85/22.78 % (72238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.85/22.78 % (72238)CaDiCaL version: 2.1.3
% 125.85/22.78 % (72238)Termination reason: Instruction limit
% 125.85/22.78 % (72238)Termination phase: Property scanning
% 125.85/22.78 % (72238)Time elapsed: 0.371 s
% 125.85/22.78 % (72238)Peak memory usage: 182 MB
% 125.85/22.78 % (72238)Instructions burned: 441 (million)
% 125.85/22.78 % (72191)------------------------------
% 125.85/22.78 % (72191)------------------------------
% 125.85/22.78 % (72244)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=3539625019:cts=off:i=3034:av=off:er=known:fsd=on_2853 on theBenchmark for (2853ds/3034Mi)
% 125.85/22.78 % (72216)------------------------------
% 125.85/22.78 % (72216)------------------------------
% 125.85/22.78 % (72245)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=2511445313:st=2:s2a=on:i=524:s2at=2:ss=axioms_2852 on theBenchmark for (2852ds/524Mi)
% 125.85/22.78 % (72247)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=3756279310:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2850 on theBenchmark for (2850ds/1016Mi)
% 125.85/22.78 % (72245)Instruction limit reached!
% 125.85/22.78 % (72245)------------------------------
% 125.85/22.78 % (72245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.85/22.78 % (72245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.85/22.78 % (72245)CaDiCaL version: 2.1.3
% 125.85/22.78 % (72245)Termination reason: Instruction limit
% 125.85/22.78 % (72245)Termination phase: SInE selection
% 125.85/22.78 % (72245)Time elapsed: 0.362 s
% 125.85/22.78 % (72245)Peak memory usage: 181 MB
% 125.85/22.78 % (72245)Instructions burned: 524 (million)
% 125.85/22.78 % (72247)Refutation not found, incomplete strategy
% 125.85/22.78 % (72247)------------------------------
% 125.85/22.78 % (72247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 125.85/22.78 % (72247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 125.85/22.78 % (72247)CaDiCaL version: 2.1.3
% 125.85/22.78 % (72247)Termination reason: Refutation not found, incomplete strategy
% 125.85/22.78 % (72247)Time elapsed: 0.341 s
% 125.85/22.78 % (72247)Peak memory usage: 186 MB
% 125.85/22.78 % (72247)Instructions burned: 669 (million)
% 125.85/22.78 % (72250)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=1673721061:i=14123:bd=preordered:ins=4_2846 on theBenchmark for (2846ds/14123Mi)
% 125.85/22.78 % (72247)------------------------------
% 125.85/22.78 % (72247)------------------------------
% 125.85/22.78 % (72255)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=2482193252:i=5781:kws=precedence:bd=all:rawr=on_2841 on theBenchmark for (2841ds/5781Mi)
% 125.85/22.78 [W928 21:05:44.657526500 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 125.85/22.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 125.85/22.78 [W928 21:05:44.657584960 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 125.85/22.78 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 125.85/22.78 [W928 21:05:44.657674007 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 129.05/23.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 129.05/23.13 [W928 21:05:44.657691260 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 129.05/23.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 129.05/23.13 [W928 21:05:44.657732507 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 129.05/23.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 129.05/23.13 [W928 21:05:44.657748814 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 129.05/23.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 129.05/23.13 [W928 21:05:44.657789684 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 129.05/23.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 129.05/23.13 [W928 21:05:44.657807770 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 129.05/23.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 129.05/23.13 [W928 21:05:44.657851544 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 129.05/23.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 129.05/23.13 [W928 21:05:44.657933634 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 129.05/23.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 129.05/23.13 [W928 21:05:44.658027174 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 129.05/23.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 129.05/23.13 [W928 21:05:44.658083764 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 129.05/23.13 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 129.05/23.13 % (72244)Instruction limit reached!
% 129.05/23.13 % (72244)------------------------------
% 129.05/23.13 % (72244)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.05/23.13 % (72244)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.05/23.13 % (72244)CaDiCaL version: 2.1.3
% 129.05/23.13 % (72244)Termination reason: Instruction limit
% 129.05/23.13 % (72244)Termination phase: Property scanning
% 129.05/23.13 % (72244)Time elapsed: 2.601 s
% 129.05/23.13 % (72244)Peak memory usage: 227 MB
% 129.05/23.13 % (72244)Instructions burned: 3035 (million)
% 129.05/23.13 % (72260)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=1687099389:i=2448:gtgl=5:bd=preordered:gtg=all_2824 on theBenchmark for (2824ds/2448Mi)
% 129.05/23.13 % (72255)Instruction limit reached!
% 129.05/23.13 % (72255)------------------------------
% 129.05/23.13 % (72255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.05/23.13 % (72255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.05/23.13 % (72255)CaDiCaL version: 2.1.3
% 155.83/26.85 % (72255)Termination reason: Instruction limit
% 155.83/26.85 % (72255)Termination phase: Saturation
% 155.83/26.85 % (72255)Time elapsed: 2.795 s
% 155.83/26.85 % (72255)Peak memory usage: 237 MB
% 155.83/26.85 % (72255)Instructions burned: 5781 (million)
% 155.83/26.85 % (72239)Refutation not found, incomplete strategy
% 155.83/26.85 % (72239)------------------------------
% 155.83/26.85 % (72239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.83/26.85 % (72239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.83/26.85 % (72239)CaDiCaL version: 2.1.3
% 155.83/26.85 % (72239)Termination reason: Refutation not found, incomplete strategy
% 155.83/26.85 % (72239)Time elapsed: 4.613 s
% 155.83/26.85 % (72239)Peak memory usage: 300 MB
% 155.83/26.85 % (72239)Instructions burned: 4566 (million)
% 155.83/26.85 % (72268)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=3416787186:i=3223:kws=precedence:fgj=on:av=off_2810 on theBenchmark for (2810ds/3223Mi)
% 155.83/26.85 % (72239)------------------------------
% 155.83/26.85 % (72239)------------------------------
% 155.83/26.85 % (72260)Instruction limit reached!
% 155.83/26.85 % (72260)------------------------------
% 155.83/26.85 % (72260)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.83/26.85 % (72260)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.83/26.85 % (72260)CaDiCaL version: 2.1.3
% 155.83/26.85 % (72260)Termination reason: Instruction limit
% 155.83/26.85 % (72260)Termination phase: Property scanning
% 155.83/26.85 % (72260)Time elapsed: 1.862 s
% 155.83/26.85 % (72260)Peak memory usage: 182 MB
% 155.83/26.85 % (72260)Instructions burned: 2448 (million)
% 155.83/26.85 % (72273)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=3163384785:st=5.6:i=2033:sd=3:ss=axioms_2803 on theBenchmark for (2803ds/2033Mi)
% 155.83/26.85 % (72274)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=61013118:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2803 on theBenchmark for (2803ds/2055Mi)
% 155.83/26.85 % (72268)Instruction limit reached!
% 155.83/26.85 % (72268)------------------------------
% 155.83/26.85 % (72268)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.83/26.85 % (72268)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.83/26.85 % (72268)CaDiCaL version: 2.1.3
% 155.83/26.85 % (72268)Termination reason: Instruction limit
% 155.83/26.85 % (72268)Termination phase: Property scanning
% 155.83/26.85 % (72268)Time elapsed: 1.746 s
% 155.83/26.85 % (72268)Peak memory usage: 227 MB
% 155.83/26.85 % (72268)Instructions burned: 3224 (million)
% 155.83/26.85 % (72281)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=4280933008:i=21611:sd=3:ss=axioms_2791 on theBenchmark for (2791ds/21611Mi)
% 155.83/26.85 % (72274)Instruction limit reached!
% 155.83/26.85 % (72274)------------------------------
% 155.83/26.85 % (72274)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.83/26.85 % (72274)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.83/26.85 % (72274)CaDiCaL version: 2.1.3
% 155.83/26.85 % (72274)Termination reason: Instruction limit
% 155.83/26.85 % (72274)Termination phase: SInE selection
% 155.83/26.85 % (72274)Time elapsed: 1.531 s
% 155.83/26.85 % (72274)Peak memory usage: 182 MB
% 155.83/26.85 % (72274)Instructions burned: 2056 (million)
% 155.83/26.85 % (72273)Instruction limit reached!
% 155.83/26.85 % (72273)------------------------------
% 155.83/26.85 % (72273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 155.83/26.85 % (72273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 155.83/26.85 % (72273)CaDiCaL version: 2.1.3
% 155.83/26.85 % (72273)Termination reason: Instruction limit
% 155.83/26.85 % (72273)Termination phase: Saturation
% 155.83/26.85 % (72273)Time elapsed: 1.727 s
% 155.83/26.85 % (72273)Peak memory usage: 215 MB
% 155.83/26.85 % (72273)Instructions burned: 2034 (million)
% 155.83/26.85 % (72286)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3006262307:i=4835:sd=13:ss=axioms:sgt=23_2785 on theBenchmark for (2785ds/4835Mi)
% 155.83/26.85 % (72288)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=2363635086:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2783 on theBenchmark for (2783ds/797Mi)
% 155.83/26.85 [W928 21:05:50.178965202 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 186.94/31.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 186.94/31.25 [W928 21:05:50.179013790 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 186.94/31.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 186.94/31.25 [W928 21:05:50.179063849 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 186.94/31.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 186.94/31.25 [W928 21:05:50.179073666 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 186.94/31.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 186.94/31.25 [W928 21:05:50.179097229 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 186.94/31.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 186.94/31.25 [W928 21:05:50.179106172 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 186.94/31.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 186.94/31.25 [W928 21:05:50.179128425 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 186.94/31.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 186.94/31.25 [W928 21:05:50.179137308 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 186.94/31.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 186.94/31.25 [W928 21:05:50.179159686 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 186.94/31.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 186.94/31.25 [W928 21:05:50.179178380 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 186.94/31.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 186.94/31.25 [W928 21:05:50.179202459 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 186.94/31.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 186.94/31.25 [W928 21:05:50.179211255 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 186.94/31.25 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 186.94/31.25 % (72288)Instruction limit reached!
% 186.94/31.25 % (72288)------------------------------
% 186.94/31.25 % (72288)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 186.94/31.25 % (72288)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 186.94/31.25 % (72288)CaDiCaL version: 2.1.3
% 186.94/31.25 % (72288)Termination reason: Instruction limit
% 186.94/31.25 % (72288)Termination phase: SInE selection
% 186.94/31.25 % (72288)Time elapsed: 0.557 s
% 186.94/31.25 % (72288)Peak memory usage: 182 MB
% 172.35/31.43 % (72288)Instructions burned: 797 (million)
% 172.35/31.43 % (72167)Instruction limit reached!
% 172.35/31.43 % (72167)------------------------------
% 172.35/31.43 % (72167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.35/31.43 % (72167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.35/31.43 % (72167)CaDiCaL version: 2.1.3
% 172.35/31.43 % (72167)Termination reason: Instruction limit
% 172.35/31.43 % (72167)Termination phase: Saturation
% 172.35/31.43 % (72167)Time elapsed: 14.669 s
% 172.35/31.43 % (72167)Peak memory usage: 801 MB
% 172.35/31.43 % (72167)Instructions burned: 14155 (million)
% 172.35/31.43 % (72294)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=2726880228:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2775 on theBenchmark for (2775ds/2326Mi)
% 172.35/31.43 % (72296)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=739199894:i=6038:nm=6_2773 on theBenchmark for (2773ds/6038Mi)
% 172.35/31.43 % (72221)Instruction limit reached!
% 172.35/31.43 % (72221)------------------------------
% 172.35/31.43 % (72221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.35/31.43 % (72221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.35/31.43 % (72221)CaDiCaL version: 2.1.3
% 172.35/31.43 % (72221)Termination reason: Instruction limit
% 172.35/31.43 % (72221)Termination phase: Saturation
% 172.35/31.43 % (72221)Time elapsed: 10.806 s
% 172.35/31.43 % (72221)Peak memory usage: 768 MB
% 172.35/31.43 % (72221)Instructions burned: 9925 (million)
% 172.35/31.43 % (72298)lrs+10_1_sil=32000:sp=occurrence:random_seed=19544910:st=2:i=33334:sd=3:ss=included:sgt=32_2767 on theBenchmark for (2767ds/33334Mi)
% 172.35/31.43 % (72281)Refutation not found, incomplete strategy
% 172.35/31.43 % (72281)------------------------------
% 172.35/31.43 % (72281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.35/31.43 % (72281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.35/31.43 % (72281)CaDiCaL version: 2.1.3
% 172.35/31.43 % (72281)Termination reason: Refutation not found, incomplete strategy
% 172.35/31.43 % (72281)Time elapsed: 2.486 s
% 172.35/31.43 % (72281)Peak memory usage: 300 MB
% 172.35/31.43 % (72281)Instructions burned: 4070 (million)
% 172.35/31.43 % (72281)------------------------------
% 172.35/31.43 % (72281)------------------------------
% 172.35/31.43 % (72302)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=3167196861:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2761 on theBenchmark for (2761ds/1008Mi)
% 172.35/31.43 % (72302)Instruction limit reached!
% 172.35/31.43 % (72302)------------------------------
% 172.35/31.43 % (72302)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.35/31.43 % (72302)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.35/31.43 % (72302)CaDiCaL version: 2.1.3
% 172.35/31.43 % (72302)Termination reason: Instruction limit
% 172.35/31.43 % (72302)Termination phase: SInE selection
% 172.35/31.43 % (72302)Time elapsed: 0.668 s
% 172.35/31.43 % (72302)Peak memory usage: 182 MB
% 172.35/31.43 % (72302)Instructions burned: 1008 (million)
% 172.35/31.43 % (72294)Instruction limit reached!
% 172.35/31.43 % (72294)------------------------------
% 172.35/31.43 % (72294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.35/31.43 % (72294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.35/31.43 % (72294)CaDiCaL version: 2.1.3
% 172.35/31.43 % (72294)Termination reason: Instruction limit
% 172.35/31.43 % (72294)Termination phase: Property scanning
% 172.35/31.43 % (72294)Time elapsed: 2.160 s
% 172.35/31.43 % (72294)Peak memory usage: 227 MB
% 172.35/31.43 % (72294)Instructions burned: 2326 (million)
% 172.35/31.43 % (72307)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=913528033:i=8327:s2at=5:bd=preordered_2752 on theBenchmark for (2752ds/8327Mi)
% 172.35/31.43 % (72309)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=78944889:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2751 on theBenchmark for (2751ds/1083Mi)
% 172.35/31.43 % (72309)Instruction limit reached!
% 172.35/31.43 % (72309)------------------------------
% 172.35/31.43 % (72309)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.35/31.43 % (72309)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.35/31.43 % (72309)CaDiCaL version: 2.1.3
% 172.35/31.43 % (72309)Termination reason: Instruction limit
% 172.35/31.43 % (72309)Termination phase: Unused predicate definition removal
% 172.35/31.43 % (72309)Time elapsed: 1.040 s
% 172.35/31.43 % (72309)Peak memory usage: 196 MB
% 172.35/31.43 % (72309)Instructions burned: 1083 (million)
% 172.35/31.43 % (72314)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=3294682749:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2738 on theBenchmark for (2738ds/1084Mi)
% 172.35/31.43 % (72286)Instruction limit reached!
% 172.35/31.43 % (72286)------------------------------
% 172.35/31.43 % (72286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.35/31.43 % (72286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.35/31.43 % (72286)CaDiCaL version: 2.1.3
% 172.35/31.43 % (72286)Termination reason: Instruction limit
% 172.35/31.43 % (72286)Termination phase: Saturation
% 172.35/31.43 % (72286)Time elapsed: 4.821 s
% 172.35/31.43 % (72286)Peak memory usage: 278 MB
% 172.35/31.43 % (72286)Instructions burned: 4835 (million)
% 172.35/31.43 % (72318)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=4126618225:i=6995:s2at=5:gtg=all_2734 on theBenchmark for (2734ds/6995Mi)
% 172.35/31.43 % (72314)Refutation not found, incomplete strategy
% 172.35/31.43 % (72314)------------------------------
% 172.35/31.43 % (72314)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.35/31.43 % (72314)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.35/31.43 % (72314)CaDiCaL version: 2.1.3
% 172.35/31.43 % (72314)Termination reason: Refutation not found, incomplete strategy
% 172.35/31.43 % (72314)Time elapsed: 0.502 s
% 172.35/31.43 % (72314)Peak memory usage: 187 MB
% 172.35/31.43 % (72314)Instructions burned: 665 (million)
% 172.35/31.43 % (72314)------------------------------
% 172.35/31.43 % (72314)------------------------------
% 172.35/31.43 % (72322)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=1308000356:st=2:i=6225:sd=15:ss=axioms_2726 on theBenchmark for (2726ds/6225Mi)
% 172.35/31.43 % (72322)Refutation not found, incomplete strategy
% 172.35/31.43 % (72322)------------------------------
% 172.35/31.43 % (72322)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.35/31.43 % (72322)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.35/31.43 % (72322)CaDiCaL version: 2.1.3
% 172.35/31.43 % (72322)Termination reason: Refutation not found, incomplete strategy
% 172.35/31.43 % (72322)Time elapsed: 0.610 s
% 172.35/31.43 % (72322)Peak memory usage: 186 MB
% 172.35/31.43 % (72322)Instructions burned: 829 (million)
% 172.35/31.43 % (72322)------------------------------
% 172.35/31.43 % (72322)------------------------------
% 172.35/31.43 % (72333)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=3641751664:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2713 on theBenchmark for (2713ds/3372Mi)
% 172.35/31.43 % (72296)Instruction limit reached!
% 172.35/31.43 % (72296)------------------------------
% 172.35/31.43 % (72296)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 172.35/31.43 % (72296)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 172.35/31.43 % (72296)CaDiCaL version: 2.1.3
% 172.35/31.43 % (72296)Termination reason: Instruction limit
% 172.35/31.43 % (72296)Termination phase: Saturation
% 172.35/31.43 % (72296)Time elapsed: 6.666 s
% 172.35/31.43 % (72296)Peak memory usage: 812 MB
% 172.35/31.43 % (72296)Instructions burned: 6038 (million)
% 172.35/31.43 % (72415)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=798756114:st=2.3:i=26457:sd=10:ss=included:sgt=8_2702 on theBenchmark for (2702ds/26457Mi)
% 172.35/31.43 % (72298)First to succeed.
% 172.35/31.43 % (72298)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-71917"
% 172.35/31.43 [W928 21:05:58.654075158 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 172.35/31.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 172.35/31.43 [W928 21:05:58.654109288 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 172.35/31.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 172.35/31.43 [W928 21:05:58.654160035 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 172.35/31.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 172.35/31.43 [W928 21:05:58.654172245 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 172.35/31.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 172.35/31.43 [W928 21:05:58.654197061 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 172.35/31.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 172.35/31.43 [W928 21:05:58.654207078 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 172.35/31.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 172.35/31.43 [W928 21:05:58.654231501 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 172.35/31.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 172.35/31.43 [W928 21:05:58.654241418 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 172.35/31.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 172.35/31.43 [W928 21:05:58.654264638 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 172.35/31.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 172.35/31.43 [W928 21:05:58.654274648 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 172.35/31.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 172.35/31.43 [W928 21:05:58.654299548 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 172.35/31.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 172.35/31.43 [W928 21:05:58.654362965 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 172.35/31.43 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 172.35/31.43 % (72298)Refutation found. Thanks to Tanya!
% 172.35/31.43 % SZS status Theorem for theBenchmark
% 172.35/31.43 % SZS output start Proof for theBenchmark
% See solution above
% 188.07/31.67 % (72298)------------------------------
% 188.07/31.67 % (72298)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 188.07/31.67 % (72298)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 188.07/31.67 % (72298)CaDiCaL version: 2.1.3
% 188.07/31.67 % (72298)Termination reason: Refutation
% 188.07/31.67 % (72298)Time elapsed: 6.646 s
% 188.07/31.67 % (72298)Peak memory usage: 348 MB
% 188.07/31.67 % (72298)Instructions burned: 7984 (million)
% 188.07/31.67 % (72298)------------------------------
% 188.07/31.67 % (72298)------------------------------
% 188.07/31.67 % (71917)Success in time 30.726 s
% 188.07/31.67 % Vampire exiting
%------------------------------------------------------------------------------