%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : BIO003+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 : n006.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:18 AM UTC 2026
% Result : Theorem 26.39s 12.91s
% Output : Refutation 26.39s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 3
% Syntax : Number of formulae : 19 ( 10 unt; 0 def)
% Number of atoms : 631 ( 91 equ)
% Maximal formula atoms : 91 ( 33 avg)
% Number of connectives : 619 ( 7 ~; 3 |; 603 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 92 ( 34 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 : 9 ( 9 !; 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/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,
cytoskeleton_1(fn_cell_2(a_cell)),
file('/export/starexec/sandbox2/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(f18896,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(f20336,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,[],[f18896]) ).
fof(f21389,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,[],[f20336]) ).
fof(f23990,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,[],[f21389]) ).
fof(f26517,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,[],[f23990]) ).
fof(f30720,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,[],[f26517]) ).
fof(f65858,plain,
! [X0] :
( ~ cell_1(X0)
| cytoskeleton_1(fn_cell_2(X0)) ),
inference(cnf_transformation,[],[f30720]) ).
fof(f218206,plain,
cell_1(a_cell),
inference(cnf_transformation,[],[f9161]) ).
fof(f218207,plain,
~ cytoskeleton_1(fn_cell_2(a_cell)),
inference(cnf_transformation,[],[f9164]) ).
fof(f239565,plain,
! [X0] :
( ~ cytoskeleton_1(fn_cell_2(X0))
| cell_1(X0) ),
inference(consistent_polarity_flipping,[],[f65858]) ).
fof(f337405,plain,
~ cell_1(a_cell),
inference(consistent_polarity_flipping,[],[f218206]) ).
fof(f337406,plain,
cytoskeleton_1(fn_cell_2(a_cell)),
inference(consistent_polarity_flipping,[],[f218207]) ).
fof(f356065,plain,
cell_1(a_cell),
inference(resolution,[],[f239565,f337406]) ).
fof(f356068,plain,
$false,
inference(forward_subsumption_resolution,[],[f356065,f337405]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.05 % Problem : BIO003+1 : TPTP v9.3.1. Bugfixed v6.4.1.
% 0.00/0.10 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.27/0.32 % Computer : n006.cluster.edu
% 0.27/0.32 % Model : x86_64 x86_64
% 0.27/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.27/0.32 % Memory : 8046.5625MB
% 0.27/0.32 % OS : Linux 6.8.0-71-generic
% 0.27/0.32 % CPULimit : 300
% 0.27/0.32 % WCLimit : 300
% 0.27/0.32 % DateTime : Mon Sep 28 21:02:27 UTC 2026
% 0.27/0.32 % CPUTime :
% 0.27/0.32 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.27/0.36 Running first-order model finding
% 0.27/0.36 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
% 26.39/12.91 % (196796)Will run a generic schedule for satisfiability detection.
% 26.39/12.91 % (196801)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=186701196_2929 on theBenchmark for (2929ds/0Mi)
% 26.39/12.91 % (196802)% WARNING: option uhcvi not known.
% 26.39/12.91 % (196802)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=1559151338:i=135531:add=off:rawr=on_2929 on theBenchmark for (2929ds/135531Mi)
% 26.39/12.91 % (196803)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=1900884590:i=88024:add=on:rawr=on_2929 on theBenchmark for (2929ds/88024Mi)
% 26.39/12.91 % (196804)dis+10_1_sil=32000:sp=arity:random_seed=1259980966:i=103:fgj=on_2929 on theBenchmark for (2929ds/103Mi)
% 26.39/12.91 % (196805)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=980039107:i=116_2929 on theBenchmark for (2929ds/116Mi)
% 26.39/12.91 % (196807)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=1895151210:i=131_2929 on theBenchmark for (2929ds/131Mi)
% 26.39/12.91 % (196808)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=931687066:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2929 on theBenchmark for (2929ds/159Mi)
% 26.39/12.91 % (196804)Instruction limit reached!
% 26.39/12.91 % (196804)------------------------------
% 26.39/12.91 % (196804)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.39/12.91 % (196804)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.39/12.91 % (196804)CaDiCaL version: 2.1.3
% 26.39/12.91 % (196804)Termination reason: Instruction limit
% 26.39/12.91 % (196804)Termination phase: Preprocessing 1
% 26.39/12.91 % (196804)Time elapsed: 0.103 s
% 26.39/12.91 % (196804)Peak memory usage: 108 MB
% 26.39/12.91 % (196804)Instructions burned: 103 (million)
% 26.39/12.91 % (196805)Instruction limit reached!
% 26.39/12.91 % (196805)------------------------------
% 26.39/12.91 % (196805)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.39/12.91 % (196805)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.39/12.91 % (196805)CaDiCaL version: 2.1.3
% 26.39/12.91 % (196805)Termination reason: Instruction limit
% 26.39/12.91 % (196805)Termination phase: Preprocessing 1
% 26.39/12.91 % (196805)Time elapsed: 0.125 s
% 26.39/12.91 % (196805)Peak memory usage: 108 MB
% 26.39/12.91 % (196805)Instructions burned: 116 (million)
% 26.39/12.91 % (196807)Instruction limit reached!
% 26.39/12.91 % (196807)------------------------------
% 26.39/12.91 % (196807)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.39/12.91 % (196807)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.39/12.91 % (196807)CaDiCaL version: 2.1.3
% 26.39/12.91 % (196807)Termination reason: Instruction limit
% 26.39/12.91 % (196807)Termination phase: Preprocessing 1
% 26.39/12.91 % (196807)Time elapsed: 0.132 s
% 26.39/12.91 % (196807)Peak memory usage: 108 MB
% 26.39/12.91 % (196807)Instructions burned: 131 (million)
% 26.39/12.91 % (196815)fmb+10_1_fmbas=predicate:sil=64000:sas=cadical:random_seed=2301874182:i=714:nm=2_2927 on theBenchmark for (2927ds/714Mi)
% 26.39/12.91 % (196816)ott+32_1_sil=16000:bsd=on:sp=const_max:bce=on:random_seed=3650184135:i=131:bd=preordered:fsd=on_2927 on theBenchmark for (2927ds/131Mi)
% 26.39/12.91 % (196808)Instruction limit reached!
% 26.39/12.91 % (196808)------------------------------
% 26.39/12.91 % (196808)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.39/12.91 % (196808)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.39/12.91 % (196808)CaDiCaL version: 2.1.3
% 26.39/12.91 % (196808)Termination reason: Instruction limit
% 26.39/12.91 % (196808)Termination phase: Preprocessing 1
% 26.39/12.91 % (196808)Time elapsed: 0.163 s
% 26.39/12.91 % (196808)Peak memory usage: 108 MB
% 26.39/12.91 % (196808)Instructions burned: 159 (million)
% 26.39/12.91 % (196817)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=3642940006:i=684:slsql=off:bs=unit_only:nicw=on:rawr=on_2926 on theBenchmark for (2926ds/684Mi)
% 26.39/12.91 % (196821)ott-21_1_sil=16000:fs=off:random_seed=1877132453:i=180:av=off:fsr=off_2926 on theBenchmark for (2926ds/180Mi)
% 26.39/12.91 % (196816)Instruction limit reached!
% 26.39/12.91 % (196816)------------------------------
% 26.39/12.91 % (196816)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.39/12.91 % (196816)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.39/12.91 % (196816)CaDiCaL version: 2.1.3
% 26.39/12.91 % (196816)Termination reason: Instruction limit
% 26.39/12.91 % (196816)Termination phase: Preprocessing 1
% 26.39/12.91 % (196816)Time elapsed: 0.130 s
% 26.39/12.91 % (196816)Peak memory usage: 108 MB
% 26.39/12.91 % (196816)Instructions burned: 131 (million)
% 26.39/12.91 % (196823)dis+10_4_sil=64000:sp=reverse_arity:bsr=on:sac=on:cn=on:random_seed=3685854234:i=477:bd=all_2925 on theBenchmark for (2925ds/477Mi)
% 26.39/12.91 % (196821)Instruction limit reached!
% 26.39/12.91 % (196821)------------------------------
% 26.39/12.91 % (196821)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.39/12.91 % (196821)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.39/12.91 % (196821)CaDiCaL version: 2.1.3
% 26.39/12.91 % (196821)Termination reason: Instruction limit
% 26.39/12.91 % (196821)Termination phase: Preprocessing 1
% 26.39/12.91 % (196821)Time elapsed: 0.180 s
% 26.39/12.91 % (196821)Peak memory usage: 108 MB
% 26.39/12.91 % (196821)Instructions burned: 180 (million)
% 26.39/12.91 % (196825)fmb+10_1_sil=64000:erd=off:updr=off:random_seed=2010797810:fmbsr=1.3:i=865:ins=25_2924 on theBenchmark for (2924ds/865Mi)
% 26.39/12.91 % (196817)Instruction limit reached!
% 26.39/12.91 % (196817)------------------------------
% 26.39/12.91 % (196817)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.39/12.91 % (196817)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.39/12.91 % (196817)CaDiCaL version: 2.1.3
% 26.39/12.91 % (196817)Termination reason: Instruction limit
% 26.39/12.91 % (196817)Termination phase: Preprocessing 1
% 26.39/12.91 % (196817)Time elapsed: 0.480 s
% 26.39/12.91 % (196817)Peak memory usage: 112 MB
% 26.39/12.91 % (196817)Instructions burned: 684 (million)
% 26.39/12.91 % (196827)ott+10_1_to=lpo:sil=64000:tgt=full:sp=arity:spb=goal_then_units:random_seed=3322766560:i=1179_2921 on theBenchmark for (2921ds/1179Mi)
% 26.39/12.91 % (196815)Instruction limit reached!
% 26.39/12.91 % (196815)------------------------------
% 26.39/12.91 % (196815)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.39/12.91 % (196815)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.39/12.91 % (196815)CaDiCaL version: 2.1.3
% 26.39/12.91 % (196815)Termination reason: Instruction limit
% 26.39/12.91 % (196815)Termination phase: Unused predicate definition removal
% 26.39/12.91 % (196815)Time elapsed: 0.741 s
% 26.39/12.91 % (196815)Peak memory usage: 135 MB
% 26.39/12.91 % (196815)Instructions burned: 714 (million)
% 26.39/12.91 % (196823)Instruction limit reached!
% 26.39/12.91 % (196823)------------------------------
% 26.39/12.91 % (196823)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.39/12.91 % (196823)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.39/12.91 % (196823)CaDiCaL version: 2.1.3
% 26.39/12.91 % (196823)Termination reason: Instruction limit
% 26.39/12.91 % (196823)Termination phase: Unused predicate definition removal
% 26.39/12.91 % (196823)Time elapsed: 0.532 s
% 26.39/12.91 % (196823)Peak memory usage: 115 MB
% 26.39/12.91 % (196823)Instructions burned: 477 (million)
% 26.39/12.91 % (196829)fmb+10_1_sil=64000:erd=off:fmbss=14:random_seed=1481648200:i=889:ins=1_2919 on theBenchmark for (2919ds/889Mi)
% 26.39/12.91 % (196830)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=3270648134:avsq=on:s2a=on:i=692:avsqr=8,1:kws=arity_squared:bs=unit_only:nm=2:rawr=on_2919 on theBenchmark for (2919ds/692Mi)
% 26.39/12.91 % (196825)Instruction limit reached!
% 26.39/12.91 % (196825)------------------------------
% 26.39/12.91 % (196825)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.39/12.91 % (196825)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.39/12.91 % (196825)CaDiCaL version: 2.1.3
% 26.39/12.91 % (196825)Termination reason: Instruction limit
% 26.39/12.91 % (196825)Termination phase: Naming
% 26.39/12.91 % (196825)Time elapsed: 0.842 s
% 26.39/12.91 % (196825)Peak memory usage: 142 MB
% 26.39/12.91 % (196825)Instructions burned: 866 (million)
% 26.39/12.91 % (196833)dis-10_1_anc=none:sil=64000:spb=goal:newcnf=on:cn=on:random_seed=3864437282:i=879:kws=inv_precedence:fsr=off_2914 on theBenchmark for (2914ds/879Mi)
% 26.39/12.91 % (196830)Instruction limit reached!
% 26.39/12.91 % (196830)------------------------------
% 26.39/12.91 % (196830)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.39/12.91 % (196830)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.39/12.91 % (196830)CaDiCaL version: 2.1.3
% 26.39/12.91 % (196830)Termination reason: Instruction limit
% 26.39/12.91 % (196830)Termination phase: Preprocessing 1
% 26.39/12.91 % (196830)Time elapsed: 0.490 s
% 26.39/12.91 % (196830)Peak memory usage: 112 MB
% 26.39/12.91 % (196830)Instructions burned: 692 (million)
% 26.39/12.91 % (196835)fmb+10_1_sil=64000:random_seed=138677269:i=22061:nm=2:gsp=on_2913 on theBenchmark for (2913ds/22061Mi)
% 26.39/12.91 % (196829)Instruction limit reached!
% 26.39/12.91 % (196829)------------------------------
% 26.39/12.91 % (196829)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.39/12.91 % (196829)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.39/12.91 % (196829)CaDiCaL version: 2.1.3
% 26.39/12.91 % (196829)Termination reason: Instruction limit
% 26.39/12.91 % (196829)Termination phase: Unused predicate definition removal
% 26.39/12.91 % (196829)Time elapsed: 0.909 s
% 26.39/12.91 % (196829)Peak memory usage: 146 MB
% 26.39/12.91 % (196829)Instructions burned: 890 (million)
% 26.39/12.91 % (196827)Instruction limit reached!
% 26.39/12.91 % (196827)------------------------------
% 26.39/12.91 % (196827)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.39/12.91 % (196827)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.39/12.91 % (196827)CaDiCaL version: 2.1.3
% 26.39/12.91 % (196827)Termination reason: Instruction limit
% 26.39/12.91 % (196827)Termination phase: Naming
% 26.39/12.91 % (196827)Time elapsed: 1.200 s
% 26.39/12.91 % (196827)Peak memory usage: 147 MB
% 26.39/12.91 % (196827)Instructions burned: 1180 (million)
% 26.39/12.91 % (196837)fmb+10_1_sil=16000:sas=cadical:fmbss=20:random_seed=2188592652:i=9515:nm=5_2909 on theBenchmark for (2909ds/9515Mi)
% 26.39/12.91 % (196838)fmb+10_1_sil=64000:sas=cadical:fmbss=8:random_seed=2521144421:fmbsr=1.7:i=920_2908 on theBenchmark for (2908ds/920Mi)
% 26.39/12.91 % (196833)Instruction limit reached!
% 26.39/12.91 % (196833)------------------------------
% 26.39/12.91 % (196833)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.39/12.91 % (196833)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.39/12.91 % (196833)CaDiCaL version: 2.1.3
% 26.39/12.91 % (196833)Termination reason: Instruction limit
% 26.39/12.91 % (196833)Termination phase: Unused predicate definition removal
% 26.39/12.91 % (196833)Time elapsed: 0.978 s
% 26.39/12.91 % (196833)Peak memory usage: 144 MB
% 26.39/12.91 % (196833)Instructions burned: 879 (million)
% 26.39/12.91 % (196841)dis-4_1_sil=16000:drc=ordering:sp=const_frequency:sac=on:newcnf=on:random_seed=2013786027:i=5131_2904 on theBenchmark for (2904ds/5131Mi)
% 26.39/12.91 % (196838)Instruction limit reached!
% 26.39/12.91 % (196838)------------------------------
% 26.39/12.91 % (196838)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.39/12.91 % (196838)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.39/12.91 % (196838)CaDiCaL version: 2.1.3
% 26.39/12.91 % (196838)Termination reason: Instruction limit
% 26.39/12.91 % (196838)Termination phase: Unused predicate definition removal
% 26.39/12.91 % (196838)Time elapsed: 0.941 s
% 26.39/12.91 % (196838)Peak memory usage: 148 MB
% 26.39/12.91 % (196838)Instructions burned: 921 (million)
% 26.39/12.91 % (196843)ott+11_16_sil=32000:fde=unused:bsd=on:sas=cadical:sp=arity:spb=units:lsd=10:nwc=3:random_seed=1248326310:i=1472:ins=7:fdi=8:gsp=on_2898 on theBenchmark for (2898ds/1472Mi)
% 26.39/12.91 % (196843)Instruction limit reached!
% 26.39/12.91 % (196843)------------------------------
% 26.39/12.91 % (196843)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.39/12.91 % (196843)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.39/12.91 % (196843)CaDiCaL version: 2.1.3
% 26.39/12.91 % (196843)Termination reason: Instruction limit
% 26.39/12.91 % (196843)Termination phase: Naming
% 26.39/12.91 % (196843)Time elapsed: 1.375 s
% 26.39/12.91 % (196843)Peak memory usage: 147 MB
% 26.39/12.91 % (196843)Instructions burned: 1472 (million)
% 26.39/12.91 % (196845)fmb+10_1_sil=16000:sas=cadical:bce=on:fmbss=77:random_seed=1876195643:i=6324_2884 on theBenchmark for (2884ds/6324Mi)
% 26.39/12.91 % (196802) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-196796-196802"...
% 26.39/12.91 % (196802)...printing done.
% 26.39/12.91 % (196802)Refutation found. Thanks to Tanya!
% 26.39/12.91 % SZS status Theorem for theBenchmark
% 26.39/12.91 % SZS output start Proof for theBenchmark
% See solution above
% 26.39/13.03 % (196802)------------------------------
% 26.39/13.03 % (196802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 26.39/13.03 % (196802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 26.39/13.03 % (196802)CaDiCaL version: 2.1.3
% 26.39/13.03 % (196802)Termination reason: Refutation
% 26.39/13.03 % (196802)Time elapsed: 5.163 s
% 26.39/13.03 % (196802)Peak memory usage: 232 MB
% 26.39/13.03 % (196802)Instructions burned: 5519 (million)
% 26.39/13.03 % (196796)Success in time 12.529 s
% 26.39/13.03 % Vampire exiting
%------------------------------------------------------------------------------