%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : BIO002+1 : TPTP v9.3.1. Bugfixed v6.4.1.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n001.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:17 AM UTC 2026
% Result : Theorem 52.95s 16.47s
% Output : Refutation 88.13s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 3
% Syntax : Number of formulae : 18 ( 9 unt; 0 def)
% Number of atoms : 630 ( 91 equ)
% Maximal formula atoms : 91 ( 35 avg)
% Number of connectives : 620 ( 8 ~; 3 |; 603 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 92 ( 36 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 52 ( 50 usr; 1 prp; 0-4 aty)
% Number of functors : 46 ( 42 usr; 16 con; 0-1 aty)
% Number of variables : 14 ( 12 !; 2 ?)
% 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/sandbox2/benchmark/Axioms/BIO001+0.ax',a528132) ).
fof(f9161,axiom,
cell_1(a_cell),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',a_cell) ).
fof(f9162,conjecture,
? [X0] : has_part_2(a_cell,X0),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ask) ).
fof(f9163,negated_conjecture,
~ ? [X0] : has_part_2(a_cell,X0),
inference(negated_conjecture,[status(cth)],[f9162]) ).
fof(f18898,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))
& 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)
& 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(f20388,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))
& 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)
& 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,[],[f18898]) ).
fof(f22702,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))
& 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)
& 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,[],[f20388]) ).
fof(f24512,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))
& 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)
& 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,[],[f22702]) ).
fof(f25742,plain,
! [X0] :
( cell_1(X0)
=> ( 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)
& 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,[],[f24512]) ).
fof(f30719,plain,
! [X0] :
( ( 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)
& 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)) )
| ~ cell_1(X0) ),
inference(ennf_transformation,[],[f25742]) ).
fof(f33257,plain,
! [X0] : ~ has_part_2(a_cell,X0),
inference(ennf_transformation,[],[f9163]) ).
fof(f65812,plain,
! [X0] :
( ~ cell_1(X0)
| has_part_2(X0,fn_cell_2(X0)) ),
inference(cnf_transformation,[],[f30719]) ).
fof(f218206,plain,
cell_1(a_cell),
inference(cnf_transformation,[],[f9161]) ).
fof(f218207,plain,
! [X0] : ~ has_part_2(a_cell,X0),
inference(cnf_transformation,[],[f33257]) ).
fof(f241247,plain,
! [X0] :
( ~ has_part_2(X0,fn_cell_2(X0))
| ~ cell_1(X0) ),
inference(consistent_polarity_flipping,[],[f65812]) ).
fof(f339537,plain,
! [X0] : has_part_2(a_cell,X0),
inference(consistent_polarity_flipping,[],[f218207]) ).
fof(f537406,plain,
~ cell_1(a_cell),
inference(resolution,[],[f241247,f339537]) ).
fof(f537407,plain,
$false,
inference(forward_subsumption_resolution,[],[f537406,f218206]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : BIO002+1 : TPTP v9.3.1. Bugfixed v6.4.1.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.19 % Computer : n001.cluster.edu
% 0.08/0.19 % Model : x86_64 x86_64
% 0.08/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.08/0.19 % Memory : 8046.5625MB
% 0.08/0.19 % OS : Linux 6.8.0-71-generic
% 0.08/0.19 % CPULimit : 300
% 0.08/0.19 % WCLimit : 300
% 0.08/0.19 % DateTime : Mon Sep 28 21:08:35 UTC 2026
% 0.08/0.19 % CPUTime :
% 0.08/0.19 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.08/0.22 Running first-order model finding
% 0.08/0.22 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 54.60/11.74 % (747290)Will run a generic schedule for satisfiability detection.
% 54.60/11.74 % (747317)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=1896167867_2956 on theBenchmark for (2956ds/0Mi)
% 54.60/11.74 % (747319)% WARNING: option uhcvi not known.
% 54.60/11.74 % (747320)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=979746040:i=88024:add=on:rawr=on_2956 on theBenchmark for (2956ds/88024Mi)
% 54.60/11.74 % (747319)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1363963604:i=135531:add=off:rawr=on_2956 on theBenchmark for (2956ds/135531Mi)
% 54.60/11.74 % (747321)dis+10_1_sil=32000:sp=arity:random_seed=2686390471:i=103:fgj=on_2956 on theBenchmark for (2956ds/103Mi)
% 54.60/11.74 % (747324)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=2058407245:i=131_2956 on theBenchmark for (2956ds/131Mi)
% 54.60/11.74 % (747323)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2131905713:i=116_2956 on theBenchmark for (2956ds/116Mi)
% 54.60/11.74 % (747328)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=1333752835:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2956 on theBenchmark for (2956ds/159Mi)
% 54.60/11.74 % (747321)Instruction limit reached!
% 54.60/11.74 % (747321)------------------------------
% 54.60/11.74 % (747321)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.60/11.74 % (747321)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.60/11.74 % (747321)CaDiCaL version: 2.1.3
% 54.60/11.74 % (747321)Termination reason: Instruction limit
% 54.60/11.74 % (747321)Termination phase: Preprocessing 1
% 54.60/11.74 % (747321)Time elapsed: 0.099 s
% 54.60/11.74 % (747321)Peak memory usage: 108 MB
% 54.60/11.74 % (747321)Instructions burned: 103 (million)
% 54.60/11.74 % (747324)Instruction limit reached!
% 54.60/11.74 % (747324)------------------------------
% 54.60/11.74 % (747324)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.60/11.74 % (747324)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.60/11.74 % (747324)CaDiCaL version: 2.1.3
% 54.60/11.74 % (747324)Termination reason: Instruction limit
% 54.60/11.74 % (747324)Termination phase: Preprocessing 1
% 54.60/11.74 % (747324)Time elapsed: 0.111 s
% 54.60/11.74 % (747324)Peak memory usage: 108 MB
% 54.60/11.74 % (747324)Instructions burned: 134 (million)
% 54.60/11.74 % (747323)Instruction limit reached!
% 54.60/11.74 % (747323)------------------------------
% 54.60/11.74 % (747323)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.60/11.74 % (747323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.60/11.74 % (747323)CaDiCaL version: 2.1.3
% 54.60/11.74 % (747323)Termination reason: Instruction limit
% 54.60/11.74 % (747323)Termination phase: Preprocessing 1
% 54.60/11.74 % (747323)Time elapsed: 0.126 s
% 54.60/11.74 % (747323)Peak memory usage: 108 MB
% 54.60/11.74 % (747323)Instructions burned: 116 (million)
% 54.60/11.74 % (747337)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=2025557756:i=131:bd=preordered:fsd=on_2954 on theBenchmark for (2954ds/131Mi)
% 54.60/11.74 % (747336)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2778523760:i=714:nm=2_2954 on theBenchmark for (2954ds/714Mi)
% 54.60/11.74 % (747338)dis+11_32_anc=none:slsqr=2,1:sil=64000:sas=cadical:lma=off:lsd=50:s2agt=8:slsqc=1:kmz=on:newcnf=on:slsq=on:random_seed=2802453200:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2954 on theBenchmark for (2954ds/684Mi)
% 54.60/11.74 % (747328)Instruction limit reached!
% 54.60/11.74 % (747328)------------------------------
% 54.60/11.74 % (747328)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.60/11.74 % (747328)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.60/11.74 % (747328)CaDiCaL version: 2.1.3
% 54.60/11.74 % (747328)Termination reason: Instruction limit
% 54.60/11.74 % (747328)Termination phase: Preprocessing 1
% 54.60/11.74 % (747328)Time elapsed: 0.167 s
% 54.60/11.74 % (747328)Peak memory usage: 108 MB
% 54.60/11.74 % (747328)Instructions burned: 159 (million)
% 54.60/11.74 % (747337)Instruction limit reached!
% 54.60/11.74 % (747337)------------------------------
% 54.60/11.74 % (747337)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 54.60/11.74 % (747337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 54.60/11.74 % (747337)CaDiCaL version: 2.1.3
% 54.60/11.74 % (747337)Termination reason: Instruction limit
% 54.60/11.74 % (747337)Termination phase: Preprocessing 1
% 54.60/11.74 % (747337)Time elapsed: 0.091 s
% 54.60/11.74 % (747337)Peak memory usage: 108 MB
% 52.95/16.47 % (747337)Instructions burned: 131 (million)
% 52.95/16.47 % (747342)ott-21_1_sil=16000:fs=off:random_seed=2578733197:i=180:av=off:fsr=off_2953 on theBenchmark for (2953ds/180Mi)
% 52.95/16.47 % (747344)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=2690385139:i=477:bd=all_2952 on theBenchmark for (2952ds/477Mi)
% 52.95/16.47 % (747342)Instruction limit reached!
% 52.95/16.47 % (747342)------------------------------
% 52.95/16.47 % (747342)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.95/16.47 % (747342)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.95/16.47 % (747342)CaDiCaL version: 2.1.3
% 52.95/16.47 % (747342)Termination reason: Instruction limit
% 52.95/16.47 % (747342)Termination phase: Preprocessing 1
% 52.95/16.47 % (747342)Time elapsed: 0.189 s
% 52.95/16.47 % (747342)Peak memory usage: 108 MB
% 52.95/16.47 % (747342)Instructions burned: 181 (million)
% 52.95/16.47 % (747350)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=3761091080:fmbsr=1.3:i=865:ins=25_2950 on theBenchmark for (2950ds/865Mi)
% 52.95/16.47 % (747338)Instruction limit reached!
% 52.95/16.47 % (747338)------------------------------
% 52.95/16.47 % (747338)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.95/16.47 % (747338)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.95/16.47 % (747338)CaDiCaL version: 2.1.3
% 52.95/16.47 % (747338)Termination reason: Instruction limit
% 52.95/16.47 % (747338)Termination phase: Preprocessing 1
% 52.95/16.47 % (747338)Time elapsed: 0.508 s
% 52.95/16.47 % (747338)Peak memory usage: 112 MB
% 52.95/16.47 % (747338)Instructions burned: 685 (million)
% 52.95/16.47 % (747355)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3870837860:i=1179_2948 on theBenchmark for (2948ds/1179Mi)
% 52.95/16.47 % (747344)Instruction limit reached!
% 52.95/16.47 % (747344)------------------------------
% 52.95/16.47 % (747344)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.95/16.47 % (747344)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.95/16.47 % (747344)CaDiCaL version: 2.1.3
% 52.95/16.47 % (747344)Termination reason: Instruction limit
% 52.95/16.47 % (747344)Termination phase: Unused predicate definition removal
% 52.95/16.47 % (747344)Time elapsed: 0.509 s
% 52.95/16.47 % (747344)Peak memory usage: 115 MB
% 52.95/16.47 % (747344)Instructions burned: 477 (million)
% 52.95/16.47 % (747336)Instruction limit reached!
% 52.95/16.47 % (747336)------------------------------
% 52.95/16.47 % (747336)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.95/16.47 % (747336)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.95/16.47 % (747336)CaDiCaL version: 2.1.3
% 52.95/16.47 % (747336)Termination reason: Instruction limit
% 52.95/16.47 % (747336)Termination phase: Unused predicate definition removal
% 52.95/16.47 % (747336)Time elapsed: 0.689 s
% 52.95/16.47 % (747336)Peak memory usage: 135 MB
% 52.95/16.47 % (747336)Instructions burned: 714 (million)
% 52.95/16.47 % (747359)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=2236434380:i=889:ins=1_2947 on theBenchmark for (2947ds/889Mi)
% 52.95/16.47 % (747362)ott+1_16_sil=32000:plsq=on:plsqc=2:sas=cadical:avsql=on:sp=reverse_frequency:plsqr=128,1:bsr=unit_only:rp=on:newcnf=on:random_seed=2795225464:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2946 on theBenchmark for (2946ds/692Mi)
% 52.95/16.47 % (747350)Instruction limit reached!
% 52.95/16.47 % (747350)------------------------------
% 52.95/16.47 % (747350)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.95/16.47 % (747350)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.95/16.47 % (747350)CaDiCaL version: 2.1.3
% 52.95/16.47 % (747350)Termination reason: Instruction limit
% 52.95/16.47 % (747350)Termination phase: Naming
% 52.95/16.47 % (747350)Time elapsed: 0.743 s
% 52.95/16.47 % (747350)Peak memory usage: 142 MB
% 52.95/16.47 % (747350)Instructions burned: 867 (million)
% 52.95/16.47 % (747366)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3101916237:i=879:kws=inv_precedence:fsr=off_2942 on theBenchmark for (2942ds/879Mi)
% 52.95/16.47 % (747362)Instruction limit reached!
% 52.95/16.47 % (747362)------------------------------
% 52.95/16.47 % (747362)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.95/16.47 % (747362)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.95/16.47 % (747362)CaDiCaL version: 2.1.3
% 52.95/16.47 % (747362)Termination reason: Instruction limit
% 52.95/16.47 % (747362)Termination phase: Preprocessing 1
% 52.95/16.47 % (747362)Time elapsed: 0.527 s
% 52.95/16.47 % (747362)Peak memory usage: 112 MB
% 52.95/16.47 % (747362)Instructions burned: 692 (million)
% 52.95/16.47 % (747369)fmb+10_1_sil=64000:random_seed=2361706401:i=22061:nm=2:gsp=on_2940 on theBenchmark for (2940ds/22061Mi)
% 52.95/16.47 % (747359)Instruction limit reached!
% 52.95/16.47 % (747359)------------------------------
% 52.95/16.47 % (747359)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.95/16.47 % (747359)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.95/16.47 % (747359)CaDiCaL version: 2.1.3
% 52.95/16.47 % (747359)Termination reason: Instruction limit
% 52.95/16.47 % (747359)Termination phase: Unused predicate definition removal
% 52.95/16.47 % (747359)Time elapsed: 0.950 s
% 52.95/16.47 % (747359)Peak memory usage: 146 MB
% 52.95/16.47 % (747359)Instructions burned: 891 (million)
% 52.95/16.47 % (747374)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2664063738:i=9515:nm=5_2936 on theBenchmark for (2936ds/9515Mi)
% 52.95/16.47 % (747355)Instruction limit reached!
% 52.95/16.47 % (747355)------------------------------
% 52.95/16.47 % (747355)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.95/16.47 % (747355)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.95/16.47 % (747355)CaDiCaL version: 2.1.3
% 52.95/16.47 % (747355)Termination reason: Instruction limit
% 52.95/16.47 % (747355)Termination phase: Naming
% 52.95/16.47 % (747355)Time elapsed: 1.271 s
% 52.95/16.47 % (747355)Peak memory usage: 147 MB
% 52.95/16.47 % (747355)Instructions burned: 1179 (million)
% 52.95/16.47 % (747377)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=928921326:fmbsr=1.7:i=920_2934 on theBenchmark for (2934ds/920Mi)
% 52.95/16.47 % (747366)Instruction limit reached!
% 52.95/16.47 % (747366)------------------------------
% 52.95/16.47 % (747366)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.95/16.47 % (747366)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.95/16.47 % (747366)CaDiCaL version: 2.1.3
% 52.95/16.47 % (747366)Termination reason: Instruction limit
% 52.95/16.47 % (747366)Termination phase: Unused predicate definition removal
% 52.95/16.47 % (747366)Time elapsed: 0.915 s
% 52.95/16.47 % (747366)Peak memory usage: 144 MB
% 52.95/16.47 % (747366)Instructions burned: 879 (million)
% 52.95/16.47 % (747380)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2049025704:i=5131_2932 on theBenchmark for (2932ds/5131Mi)
% 52.95/16.47 % (747377)Instruction limit reached!
% 52.95/16.47 % (747377)------------------------------
% 52.95/16.47 % (747377)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.95/16.47 % (747377)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.95/16.47 % (747377)CaDiCaL version: 2.1.3
% 52.95/16.47 % (747377)Termination reason: Instruction limit
% 52.95/16.47 % (747377)Termination phase: Unused predicate definition removal
% 52.95/16.47 % (747377)Time elapsed: 0.904 s
% 52.95/16.47 % (747377)Peak memory usage: 148 MB
% 52.95/16.47 % (747377)Instructions burned: 920 (million)
% 52.95/16.47 % (747393)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=4061629654:i=1472:ins=7:fdi=8:gsp=on_2925 on theBenchmark for (2925ds/1472Mi)
% 52.95/16.47 % (747393)Instruction limit reached!
% 52.95/16.47 % (747393)------------------------------
% 52.95/16.47 % (747393)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.95/16.47 % (747393)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.95/16.47 % (747393)CaDiCaL version: 2.1.3
% 52.95/16.47 % (747393)Termination reason: Instruction limit
% 52.95/16.47 % (747393)Termination phase: Naming
% 52.95/16.47 % (747393)Time elapsed: 1.409 s
% 52.95/16.47 % (747393)Peak memory usage: 147 MB
% 52.95/16.47 % (747393)Instructions burned: 1473 (million)
% 52.95/16.47 % (747403)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=3076061197:i=6324_2910 on theBenchmark for (2910ds/6324Mi)
% 52.95/16.47 % (747380)Instruction limit reached!
% 52.95/16.47 % (747380)------------------------------
% 52.95/16.47 % (747380)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.95/16.47 % (747380)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.95/16.47 % (747380)CaDiCaL version: 2.1.3
% 52.95/16.47 % (747380)Termination reason: Instruction limit
% 52.95/16.47 % (747380)Termination phase: Saturation
% 52.95/16.47 % (747380)Time elapsed: 4.761 s
% 52.95/16.47 % (747380)Peak memory usage: 223 MB
% 52.95/16.47 % (747380)Instructions burned: 5131 (million)
% 52.95/16.47 % (747416)fmb+10_1_fmbas=function:sil=32000:sas=cadical:fmbss=16:random_seed=3132340918:fmbsr=2.30978:i=2174_2884 on theBenchmark for (2884ds/2174Mi)
% 52.95/16.47 % (747416)Instruction limit reached!
% 52.95/16.47 % (747416)------------------------------
% 52.95/16.47 % (747416)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.95/16.47 % (747416)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.95/16.47 % (747416)CaDiCaL version: 2.1.3
% 52.95/16.47 % (747416)Termination reason: Instruction limit
% 52.95/16.47 % (747416)Termination phase: Preprocessing 3
% 52.95/16.47 % (747416)Time elapsed: 2.133 s
% 52.95/16.47 % (747416)Peak memory usage: 175 MB
% 52.95/16.47 % (747416)Instructions burned: 2174 (million)
% 52.95/16.47 % (747425)ott-2_1_sil=16000:newcnf=on:random_seed=162180433:avsq=on:i=869:avsqr=1,16:kws=inv_arity_squared_2861 on theBenchmark for (2861ds/869Mi)
% 52.95/16.47 % (747374)Instruction limit reached!
% 52.95/16.47 % (747374)------------------------------
% 52.95/16.47 % (747374)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.95/16.47 % (747374)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.95/16.47 % (747374)CaDiCaL version: 2.1.3
% 52.95/16.47 % (747374)Termination reason: Instruction limit
% 52.95/16.47 % (747374)Termination phase: Finite model building preprocessing
% 52.95/16.47 % (747374)Time elapsed: 8.401 s
% 52.95/16.47 % (747374)Peak memory usage: 348 MB
% 52.95/16.47 % (747374)Instructions burned: 9515 (million)
% 52.95/16.47 % (747425)Instruction limit reached!
% 52.95/16.47 % (747425)------------------------------
% 52.95/16.47 % (747425)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.95/16.47 % (747425)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.95/16.47 % (747425)CaDiCaL version: 2.1.3
% 52.95/16.47 % (747425)Termination reason: Instruction limit
% 52.95/16.47 % (747425)Termination phase: Unused predicate definition removal
% 52.95/16.47 % (747425)Time elapsed: 0.956 s
% 52.95/16.47 % (747425)Peak memory usage: 143 MB
% 52.95/16.47 % (747425)Instructions burned: 869 (million)
% 52.95/16.47 % (747434)ott+10_1_sil=32000:tgt=ground:random_seed=1848732322:i=5114:av=off_2851 on theBenchmark for (2851ds/5114Mi)
% 52.95/16.47 % (747435)fmb+10_1_sil=64000:sas=cadical:bce=on:rp=on:random_seed=1945295316:i=54282_2851 on theBenchmark for (2851ds/54282Mi)
% 52.95/16.47 % (747403)Instruction limit reached!
% 52.95/16.47 % (747403)------------------------------
% 52.95/16.47 % (747403)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 52.95/16.47 % (747403)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.95/16.47 % (747403)CaDiCaL version: 2.1.3
% 52.95/16.47 % (747403)Termination reason: Instruction limit
% 52.95/16.47 % (747403)Termination phase: Finite model building preprocessing
% 52.95/16.47 % (747403)Time elapsed: 6.315 s
% 52.95/16.47 % (747403)Peak memory usage: 253 MB
% 52.95/16.47 % (747403)Instructions burned: 6325 (million)
% 52.95/16.47 % (747443)dis-11_1_sil=16000:sp=reverse_frequency:alpa=true:random_seed=832114830:i=3512:aac=none_2845 on theBenchmark for (2845ds/3512Mi)
% 52.95/16.47 % (747319) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-747290-747319"...
% 52.95/16.47 % (747319)...printing done.
% 52.95/16.47 % (747319)Refutation found. Thanks to Tanya!
% 52.95/16.47 % SZS status Theorem for theBenchmark
% 52.95/16.47 % SZS output start Proof for theBenchmark
% See solution above
% 88.13/16.59 % (747319)------------------------------
% 88.13/16.59 % (747319)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 88.13/16.59 % (747319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 88.13/16.59 % (747319)CaDiCaL version: 2.1.3
% 88.13/16.59 % (747319)Termination reason: Refutation
% 88.13/16.59 % (747319)Time elapsed: 11.520 s
% 88.13/16.59 % (747319)Peak memory usage: 297 MB
% 88.13/16.59 % (747319)Instructions burned: 10672 (million)
% 88.13/16.59 % (747290)Success in time 16.24 s
% 88.13/16.59 % Vampire exiting
%------------------------------------------------------------------------------