%------------------------------------------------------------------------------
% File : Drodi-SAT---4.1.1
% Problem : BIO003+1 : TPTP v9.3.1. Bugfixed v6.4.1.
% Transfm : none
% Format : tptp:raw
% Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n015.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 : Thu Sep 24 12:06:15 PM UTC 2026
% Result : Theorem 80.06s 47.02s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BIO003+1 : TPTP v9.3.1. Bugfixed v6.4.1.
% 0.00/0.04 % Command : drodi -satmode(on) -timeout(300) /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n015.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Mon Sep 21 13:49:36 UTC 2026
% 0.09/0.37 % CPUTime :
% 41.90/42.14 % Drodi V4.1.1
% 80.06/47.02 % Refutation found
% 80.06/47.02 % SZS status Theorem for theBenchmark: Theorem is valid
% 80.06/47.02 % SZS output start CNFRefutation for theBenchmark
% 80.06/47.02 fof(f3477,axiom,(
% 80.06/47.02 (! [X] :( cell_1(X)=> ( original_name_2(X,'Cell')& description_2(X,'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(X,'The basic unit from which living organisms are made.')& concept2words_2(X,cell)& living_entity_1(X)& cell_pole_1(fn_cell_1(X))& cytoskeleton_1(fn_cell_2(X))& surface_1(fn_cell_4(X))& shape_value_1(fn_cell_5(X))& specific_surface_area_value_1(fn_cell_7(X))& motor_protein_1(fn_cell_8(X))& protein_enzyme_1(fn_cell_9(X))& size_value_1(fn_cell_11(X))& structural_complexity_value_1(fn_cell_13(X))& ribosome_1(fn_cell_14(X))& length_value_1(fn_cell_18(X))& length_value_1(fn_cell_19(X))& length_value_1(fn_cell_20(X))& membrane_potential_1(fn_cell_21(X))& volume_value_1(fn_cell_22(X))& genome_1(fn_cell_24(X))& chromosome_1(fn_cell_25(X))& tangible_entity_1(fn_cell_26(X))& phospholipid_bilayer_1(fn_cell_26(X))& surface_1(fn_cell_27(X))& cytoplasmic_side_1(fn_cell_27(X))& mixture_1(fn_cell_28(X))& cytoplasm_1(fn_cell_28(X))& substance_1(fn_cell_29(X))& cytosol_1(fn_cell_29(X))& plasma_membrane_1(fn_cell_30(X))& cell_1(fn_cytoplasm_7(fn_cell_28(X)))& cytoplasm_1(fn_cytoplasmic_side_1(fn_cell_27(X)))& substance_1(fn_mixture_1(fn_cell_28(X)))& cytosol_1(fn_cytoplasm_8(fn_cell_28(X)))& tangible_entity_1(fn_biomembrane_63(fn_cell_30(X)))& phospholipid_bilayer_1(fn_biomembrane_63(fn_cell_30(X)))& tangible_entity_1(fn_plasma_membrane_71(fn_cell_30(X)))& phospholipid_bilayer_1(fn_plasma_membrane_71(fn_cell_30(X)))& surface_1(fn_biomembrane_47(fn_cell_30(X)))& cytoplasmic_side_1(fn_plasma_membrane_66(fn_cell_30(X)))& is_across_2(fn_cell_21(X),fn_cell_30(X))& shape_2(X,fn_cell_5(X))& specific_surface_area_2(X,fn_cell_7(X))& size_2(X,fn_cell_11(X))& structural_complexity_2(X,fn_cell_13(X))& diameter_2(X,fn_cell_18(X))& volume_2(X,fn_cell_22(X))& exactCardinality(X,has_region_0,"2",cell_pole_0)& has_region_2(X,fn_cell_1(X))& has_region_2(X,fn_cell_4(X))& minCardinality(X,has_part_0,"1",chromosome_0)& has_part_2(X,fn_cell_2(X))& has_part_2(X,fn_cell_25(X))& has_part_2(X,fn_cell_24(X))& has_part_2(X,fn_cell_8(X))& has_part_2(X,fn_cell_14(X))& has_part_2(X,fn_cell_30(X))& is_inside_2(fn_cell_28(X),fn_cell_30(X))& has_part_2(fn_cell_28(X),fn_cell_9(X))& the_cardinal_value_2(fn_cell_20(X),"100.0e0")& cardinal_unit_class_2(fn_cell_20(X),micrometer_0)& greater_than_or_equal_to_2(fn_cell_20(X),fn_cell_18(X))& the_cardinal_value_2(fn_cell_19(X),"0.1e0")& cardinal_unit_class_2(fn_cell_19(X),micrometer_0)& greater_than_or_equal_to_2(fn_cell_18(X),fn_cell_19(X))& is_inside_2(fn_cell_14(X),fn_cell_29(X))& the_scalar_value_2(fn_cell_13(X),simple_0)& scalar_unit_class_2(fn_cell_13(X),organism_0)& directly_proportional_2(fn_cell_11(X),fn_cell_22(X))& is_oriented_toward_2(fn_cell_27(X),fn_cell_28(X))& is_at_2(fn_cell_26(X),fn_cell_4(X))& has_part_2(X,fn_cell_28(X))& has_part_2(fn_cell_28(X),fn_cell_29(X))& has_region_2(fn_cell_30(X),fn_cell_27(X))& has_part_2(fn_cell_30(X),fn_cell_26(X))& is_facing_2(fn_cell_27(X),fn_cell_28(X))& X = fn_cytoplasm_7(fn_cell_28(X))& fn_cell_29(X) = fn_mixture_1(fn_cell_28(X))& fn_cell_29(X) = fn_cytoplasm_8(fn_cell_28(X))& fn_cell_27(X) = fn_biomembrane_47(fn_cell_30(X))& fn_cell_27(X) = fn_plasma_membrane_66(fn_cell_30(X))& fn_cell_26(X) = fn_biomembrane_63(fn_cell_30(X))& fn_cell_26(X) = fn_plasma_membrane_71(fn_cell_30(X))& fn_cell_28(X) = fn_cytoplasmic_side_1(fn_cell_27(X))& fn_mixture_1(fn_cell_28(X)) = fn_cytoplasm_8(fn_cell_28(X))& fn_cytoplasm_8(fn_cell_28(X)) = fn_biomembrane_63(fn_cell_30(X))& fn_biomembrane_63(fn_cell_30(X)) = fn_plasma_membrane_71(fn_cell_30(X))& fn_plasma_membrane_71(fn_cell_30(X)) = fn_biomembrane_47(fn_cell_30(X))& fn_biomembrane_47(fn_cell_30(X)) = fn_plasma_membrane_66(fn_cell_30(X)) ) ) )),
% 80.06/47.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 80.06/47.02 fof(f9161,axiom,(
% 80.06/47.02 cell_1(a_cell) ),
% 80.06/47.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 80.06/47.02 fof(f9162,conjecture,(
% 80.06/47.02 cytoskeleton_1(fn_cell_2(a_cell)) ),
% 80.06/47.02 file('/export/starexec/sandbox/benchmark/theBenchmark.p')).
% 80.06/47.02 fof(f9163,negated_conjecture,(
% 80.06/47.02 ~(cytoskeleton_1(fn_cell_2(a_cell)) )),
% 80.06/47.02 inference(negated_conjecture,[status(cth)],[f9162])).
% 80.06/47.02 fof(f72773,plain,(
% 80.06/47.02 ![X]: (~cell_1(X)|(((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((((original_name_2(X,'Cell')&description_2(X,'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(X,'The basic unit from which living organisms are made.'))&concept2words_2(X,cell))&living_entity_1(X))&cell_pole_1(fn_cell_1(X)))&cytoskeleton_1(fn_cell_2(X)))&surface_1(fn_cell_4(X)))&shape_value_1(fn_cell_5(X)))&specific_surface_area_value_1(fn_cell_7(X)))&motor_protein_1(fn_cell_8(X)))&protein_enzyme_1(fn_cell_9(X)))&size_value_1(fn_cell_11(X)))&structural_complexity_value_1(fn_cell_13(X)))&ribosome_1(fn_cell_14(X)))&length_value_1(fn_cell_18(X)))&length_value_1(fn_cell_19(X)))&length_value_1(fn_cell_20(X)))&membrane_potential_1(fn_cell_21(X)))&volume_value_1(fn_cell_22(X)))&genome_1(fn_cell_24(X)))&chromosome_1(fn_cell_25(X)))&tangible_entity_1(fn_cell_26(X)))&phospholipid_bilayer_1(fn_cell_26(X)))&surface_1(fn_cell_27(X)))&cytoplasmic_side_1(fn_cell_27(X)))&mixture_1(fn_cell_28(X)))&cytoplasm_1(fn_cell_28(X)))&substance_1(fn_cell_29(X)))&cytosol_1(fn_cell_29(X)))&plasma_membrane_1(fn_cell_30(X)))&cell_1(fn_cytoplasm_7(fn_cell_28(X))))&cytoplasm_1(fn_cytoplasmic_side_1(fn_cell_27(X))))&substance_1(fn_mixture_1(fn_cell_28(X))))&cytosol_1(fn_cytoplasm_8(fn_cell_28(X))))&tangible_entity_1(fn_biomembrane_63(fn_cell_30(X))))&phospholipid_bilayer_1(fn_biomembrane_63(fn_cell_30(X))))&tangible_entity_1(fn_plasma_membrane_71(fn_cell_30(X))))&phospholipid_bilayer_1(fn_plasma_membrane_71(fn_cell_30(X))))&surface_1(fn_biomembrane_47(fn_cell_30(X))))&cytoplasmic_side_1(fn_plasma_membrane_66(fn_cell_30(X))))&is_across_2(fn_cell_21(X),fn_cell_30(X)))&shape_2(X,fn_cell_5(X)))&specific_surface_area_2(X,fn_cell_7(X)))&size_2(X,fn_cell_11(X)))&structural_complexity_2(X,fn_cell_13(X)))&diameter_2(X,fn_cell_18(X)))&volume_2(X,fn_cell_22(X)))&exactCardinality(X,has_region_0,"2",cell_pole_0))&has_region_2(X,fn_cell_1(X)))&has_region_2(X,fn_cell_4(X)))&minCardinality(X,has_part_0,"1",chromosome_0))&has_part_2(X,fn_cell_2(X)))&has_part_2(X,fn_cell_25(X)))&has_part_2(X,fn_cell_24(X)))&has_part_2(X,fn_cell_8(X)))&has_part_2(X,fn_cell_14(X)))&has_part_2(X,fn_cell_30(X)))&is_inside_2(fn_cell_28(X),fn_cell_30(X)))&has_part_2(fn_cell_28(X),fn_cell_9(X)))&the_cardinal_value_2(fn_cell_20(X),"100.0e0"))&cardinal_unit_class_2(fn_cell_20(X),micrometer_0))&greater_than_or_equal_to_2(fn_cell_20(X),fn_cell_18(X)))&the_cardinal_value_2(fn_cell_19(X),"0.1e0"))&cardinal_unit_class_2(fn_cell_19(X),micrometer_0))&greater_than_or_equal_to_2(fn_cell_18(X),fn_cell_19(X)))&is_inside_2(fn_cell_14(X),fn_cell_29(X)))&the_scalar_value_2(fn_cell_13(X),simple_0))&scalar_unit_class_2(fn_cell_13(X),organism_0))&directly_proportional_2(fn_cell_11(X),fn_cell_22(X)))&is_oriented_toward_2(fn_cell_27(X),fn_cell_28(X)))&is_at_2(fn_cell_26(X),fn_cell_4(X)))&has_part_2(X,fn_cell_28(X)))&has_part_2(fn_cell_28(X),fn_cell_29(X)))&has_region_2(fn_cell_30(X),fn_cell_27(X)))&has_part_2(fn_cell_30(X),fn_cell_26(X)))&is_facing_2(fn_cell_27(X),fn_cell_28(X)))&X=fn_cytoplasm_7(fn_cell_28(X)))&fn_cell_29(X)=fn_mixture_1(fn_cell_28(X)))&fn_cell_29(X)=fn_cytoplasm_8(fn_cell_28(X)))&fn_cell_27(X)=fn_biomembrane_47(fn_cell_30(X)))&fn_cell_27(X)=fn_plasma_membrane_66(fn_cell_30(X)))&fn_cell_26(X)=fn_biomembrane_63(fn_cell_30(X)))&fn_cell_26(X)=fn_plasma_membrane_71(fn_cell_30(X)))&fn_cell_28(X)=fn_cytoplasmic_side_1(fn_cell_27(X)))&fn_mixture_1(fn_cell_28(X))=fn_cytoplasm_8(fn_cell_28(X)))&fn_cytoplasm_8(fn_cell_28(X))=fn_biomembrane_63(fn_cell_30(X)))&fn_biomembrane_63(fn_cell_30(X))=fn_plasma_membrane_71(fn_cell_30(X)))&fn_plasma_membrane_71(fn_cell_30(X))=fn_biomembrane_47(fn_cell_30(X)))&fn_biomembrane_47(fn_cell_30(X))=fn_plasma_membrane_66(fn_cell_30(X))))),
% 82.91/48.32 inference(pre_NNF_transformation,[status(thm)],[f3477])).
% 82.91/48.32 fof(f72780,plain,(
% 82.91/48.32 ![X0]: (~cell_1(X0)|cytoskeleton_1(fn_cell_2(X0)))),
% 82.91/48.32 inference(cnf_transformation,[status(thm)],[f72773])).
% 82.91/48.32 fof(f382292,plain,(
% 82.91/48.32 cell_1(a_cell)),
% 82.91/48.32 inference(cnf_transformation,[status(thm)],[f9161])).
% 82.91/48.32 fof(f382293,plain,(
% 82.91/48.32 ~cytoskeleton_1(fn_cell_2(a_cell))),
% 82.91/48.32 inference(cnf_transformation,[status(thm)],[f9163])).
% 82.91/48.32 fof(f382294,plain,(
% 82.91/48.32 cytoskeleton_1(fn_cell_2(a_cell))),
% 82.91/48.32 inference(resolution,[status(thm)],[f72780,f382292])).
% 82.91/48.32 fof(f382295,plain,(
% 82.91/48.32 $false),
% 82.91/48.32 inference(forward_subsumption_resolution,[status(thm)],[f382294,f382293])).
% 82.91/48.32 % SZS output end CNFRefutation for theBenchmark.p
% 43.81/48.74 % Elapsed time: 47.846483 seconds
% 43.81/48.74 % CPU time: 81.995075 seconds
% 43.81/48.74 % Total memory used: 12.736 GB
% 43.81/48.74 % Net memory used: 12.676 GB
%------------------------------------------------------------------------------