%------------------------------------------------------------------------------
% File : Vampire---5.0.1
% Problem : BIO002+1 : TPTP v9.3.1. Bugfixed v6.4.1.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% Computer : 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 : Tue Sep 29 09:35:14 AM UTC 2026
% Result : Theorem 197.92s 34.96s
% Output : Refutation 211.74s
% Verified :
% SZS Type : Refutation
% Derivation depth : 10
% Number of leaves : 4
% Syntax : Number of formulae : 21 ( 9 unt; 1 def)
% Number of atoms : 804 ( 117 equ)
% Maximal formula atoms : 91 ( 38 avg)
% Number of connectives : 793 ( 10 ~; 6 |; 771 &)
% ( 0 <=>; 6 =>; 0 <=; 0 <~>)
% Maximal formula depth : 92 ( 39 avg)
% Maximal term depth : 3 ( 2 avg)
% Number of predicates : 53 ( 51 usr; 1 prp; 0-4 aty)
% Number of functors : 46 ( 42 usr; 16 con; 0-1 aty)
% Number of variables : 16 ( 14 !; 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/sandbox/benchmark/theBenchmark.p',a528132) ).
fof(f9161,axiom,
cell_1(a_cell),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',a_cell) ).
fof(f9162,conjecture,
? [X0] : has_part_2(a_cell,X0),
file('/export/starexec/sandbox/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(f33606,definition,
! [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)) )
| ~ sP174(X0) ),
introduced(definition,[new_symbols(definition,[sP174])],[predicate_definition_introduction]) ).
fof(f33607,plain,
! [X0] :
( sP174(X0)
| ~ cell_1(X0) ),
inference(definition_folding,[],[f30719,f33606]) ).
fof(f35906,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)) )
| ~ sP174(X0) ),
inference(nnf_transformation,[],[f33606]) ).
fof(f69712,plain,
! [X0] :
( has_part_2(X0,fn_cell_28(X0))
| ~ sP174(X0) ),
inference(cnf_transformation,[],[f35906]) ).
fof(f69780,plain,
! [X0] :
( ~ cell_1(X0)
| sP174(X0) ),
inference(cnf_transformation,[],[f33607]) ).
fof(f223190,plain,
cell_1(a_cell),
inference(cnf_transformation,[],[f9161]) ).
fof(f223191,plain,
! [X0] : ~ has_part_2(a_cell,X0),
inference(cnf_transformation,[],[f33257]) ).
fof(f223193,plain,
sP174(a_cell),
inference(resolution,[],[f69780,f223190]) ).
fof(f223195,plain,
~ sP174(a_cell),
inference(resolution,[],[f69712,f223191]) ).
fof(f223196,plain,
$false,
inference(forward_subsumption_resolution,[],[f223195,f223193]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : BIO002+1 : TPTP v9.3.1. Bugfixed v6.4.1.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.19 % Computer : n015.cluster.edu
% 0.09/0.19 % Model : x86_64 x86_64
% 0.09/0.19 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.19 % Memory : 8046.5625MB
% 0.09/0.19 % OS : Linux 6.8.0-71-generic
% 0.09/0.19 % CPULimit : 300
% 0.09/0.19 % WCLimit : 300
% 0.09/0.19 % DateTime : Mon Sep 28 21:06:04 UTC 2026
% 0.09/0.19 % CPUTime :
% 0.09/0.19 Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.09/0.23 Running first-order theorem proving
% 0.09/0.23 Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.87/6.93 % (3020162)Detected formulas, will run a generic FOF schedule.
% 12.87/6.93 % (3020170)lrs+1010_1_to=lpo:sil=32000:sos=on:spb=goal_then_units:bce=on:random_seed=1905674422:i=109:sd=1:ins=1:gsp=on:ss=axioms_2950 on theBenchmark for (2950ds/109Mi)
% 12.87/6.93 % (3020168)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:lma=off:spb=units:urr=ec_only:bce=on:s2agt=64:updr=off:random_seed=182444952:i=134677:sd=20:aac=none:nm=16:ss=included:sgt=10_2950 on theBenchmark for (2950ds/134677Mi)
% 12.87/6.93 % (3020169)lrs+1010_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:npcc=on:prc=on:sos=all:bsr=unit_only:sac=on:random_seed=950231344:i=141695:sd=1:nm=32:gsp=on:ss=included_2950 on theBenchmark for (2950ds/141695Mi)
% 12.87/6.93 % (3020167)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2539201378:i=141193_2950 on theBenchmark for (2950ds/141193Mi)
% 12.87/6.93 % (3020170)Instruction limit reached!
% 12.87/6.93 % (3020170)------------------------------
% 12.87/6.93 % (3020170)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.87/6.93 % (3020170)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.87/6.93 % (3020170)CaDiCaL version: 2.1.3
% 12.87/6.93 % (3020170)Termination reason: Instruction limit
% 12.87/6.93 % (3020170)Termination phase: SInE selection
% 12.87/6.93 % (3020170)Time elapsed: 0.035 s
% 12.87/6.93 % (3020170)Peak memory usage: 181 MB
% 12.87/6.93 % (3020170)Instructions burned: 111 (million)
% 12.87/6.93 % (3020173)dis-21_1_sil=8000:lcm=predicate:random_seed=468571745:st=5:avsq=on:i=129:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2950 on theBenchmark for (2950ds/129Mi)
% 12.87/6.93 % (3020171)dis-1010_2:3_sil=16000:sp=reverse_frequency:random_seed=369836323:i=119:av=off:ss=axioms_2950 on theBenchmark for (2950ds/119Mi)
% 12.87/6.93 % (3020172)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4084512261:s2a=on:i=139:gtg=position_2950 on theBenchmark for (2950ds/139Mi)
% 12.87/6.93 % (3020171)Instruction limit reached!
% 12.87/6.93 % (3020171)------------------------------
% 12.87/6.93 % (3020171)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.87/6.93 % (3020171)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.87/6.93 % (3020171)CaDiCaL version: 2.1.3
% 12.87/6.93 % (3020171)Termination reason: Instruction limit
% 12.87/6.93 % (3020171)Termination phase: SInE selection
% 12.87/6.93 % (3020171)Time elapsed: 0.062 s
% 12.87/6.93 % (3020171)Peak memory usage: 181 MB
% 12.87/6.93 % (3020171)Instructions burned: 119 (million)
% 12.87/6.93 % (3020173)Instruction limit reached!
% 12.87/6.93 % (3020173)------------------------------
% 12.87/6.93 % (3020173)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.87/6.93 % (3020173)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.87/6.93 % (3020173)CaDiCaL version: 2.1.3
% 12.87/6.93 % (3020173)Termination reason: Instruction limit
% 12.87/6.93 % (3020173)Termination phase: SInE selection
% 12.87/6.93 % (3020173)Time elapsed: 0.067 s
% 12.87/6.93 % (3020173)Peak memory usage: 181 MB
% 12.87/6.93 % (3020173)Instructions burned: 130 (million)
% 12.87/6.93 % (3020180)lrs+10_1_sil=8000:sp=occurrence:random_seed=3944384102:i=285:sd=3:ss=axioms:sgt=8_2949 on theBenchmark for (2949ds/285Mi)
% 12.87/6.93 % (3020172)Instruction limit reached!
% 12.87/6.93 % (3020172)------------------------------
% 12.87/6.93 % (3020172)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.87/6.93 % (3020172)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.87/6.93 % (3020172)CaDiCaL version: 2.1.3
% 12.87/6.93 % (3020172)Termination reason: Instruction limit
% 12.87/6.93 % (3020172)Termination phase: Property scanning
% 12.87/6.93 % (3020172)Time elapsed: 0.083 s
% 12.87/6.93 % (3020172)Peak memory usage: 182 MB
% 12.87/6.93 % (3020172)Instructions burned: 140 (million)
% 12.87/6.93 % (3020180)Instruction limit reached!
% 12.87/6.93 % (3020180)------------------------------
% 12.87/6.93 % (3020180)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.87/6.93 % (3020180)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.87/6.93 % (3020180)CaDiCaL version: 2.1.3
% 12.87/6.93 % (3020180)Termination reason: Instruction limit
% 12.87/6.93 % (3020180)Termination phase: SInE selection
% 12.87/6.93 % (3020180)Time elapsed: 0.081 s
% 12.87/6.93 % (3020180)Peak memory usage: 181 MB
% 12.87/6.93 % (3020180)Instructions burned: 287 (million)
% 12.87/6.94 % (3020182)lrs+10_1_sil=32000:urr=on:br=off:random_seed=730862412:i=157:sd=1:gtg=position:ss=axioms:sgt=8_2948 on theBenchmark for (2948ds/157Mi)
% 12.87/6.94 % (3020183)lrs+1011_1_sil=32000:sp=occurrence:random_seed=1363325675:i=325:sd=1:ss=axioms:sgt=32_2948 on theBenchmark for (2948ds/325Mi)
% 12.87/6.94 % (3020185)dis+10_5:1_slsqr=1,4:sil=8000:fde=unused:erd=off:urr=full:fd=off:s2agt=8:br=off:slsq=on:random_seed=865459414:s2a=on:i=248:s2at=1.23:gtg=position_2947 on theBenchmark for (2947ds/248Mi)
% 12.87/6.94 % (3020182)Instruction limit reached!
% 12.87/6.94 % (3020182)------------------------------
% 12.87/6.94 % (3020182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.87/6.94 % (3020182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.87/6.94 % (3020182)CaDiCaL version: 2.1.3
% 12.87/6.94 % (3020182)Termination reason: Instruction limit
% 12.87/6.94 % (3020182)Termination phase: Property scanning
% 12.87/6.94 % (3020182)Time elapsed: 0.089 s
% 12.87/6.94 % (3020182)Peak memory usage: 182 MB
% 12.87/6.94 % (3020182)Instructions burned: 160 (million)
% 12.87/6.94 % (3020187)lrs+1002_1_to=lpo:sil=8000:sos=on:random_seed=1818181312:st=4:cts=off:i=294:sd=2:ins=7:amm=off:ss=axioms_2947 on theBenchmark for (2947ds/294Mi)
% 12.87/6.94 % (3020185)Instruction limit reached!
% 12.87/6.94 % (3020185)------------------------------
% 12.87/6.94 % (3020185)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.87/6.94 % (3020185)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.87/6.94 % (3020185)CaDiCaL version: 2.1.3
% 12.87/6.94 % (3020185)Termination reason: Instruction limit
% 12.87/6.94 % (3020185)Termination phase: Property scanning
% 12.87/6.94 % (3020185)Time elapsed: 0.125 s
% 12.87/6.94 % (3020185)Peak memory usage: 181 MB
% 12.87/6.94 % (3020185)Instructions burned: 249 (million)
% 12.87/6.94 % (3020187)Instruction limit reached!
% 12.87/6.94 % (3020187)------------------------------
% 12.87/6.94 % (3020187)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.87/6.94 % (3020187)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.87/6.94 % (3020187)CaDiCaL version: 2.1.3
% 12.87/6.94 % (3020187)Termination reason: Instruction limit
% 12.87/6.94 % (3020187)Termination phase: SInE selection
% 12.87/6.94 % (3020187)Time elapsed: 0.079 s
% 12.87/6.94 % (3020187)Peak memory usage: 181 MB
% 12.87/6.94 % (3020187)Instructions burned: 297 (million)
% 12.87/6.94 % (3020183)Instruction limit reached!
% 12.87/6.94 % (3020183)------------------------------
% 12.87/6.94 % (3020183)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.87/6.94 % (3020183)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.87/6.94 % (3020183)CaDiCaL version: 2.1.3
% 12.87/6.94 % (3020183)Termination reason: Instruction limit
% 12.87/6.94 % (3020183)Termination phase: SInE selection
% 12.87/6.94 % (3020183)Time elapsed: 0.162 s
% 12.87/6.94 % (3020183)Peak memory usage: 181 MB
% 12.87/6.94 % (3020183)Instructions burned: 327 (million)
% 12.87/6.94 % (3020191)lrs+10_1_ncem=casc2026/models/loop7.pt:sil=32000:tgt=ground:npcc=on:random_seed=3689776696:i=2350_2946 on theBenchmark for (2946ds/2350Mi)
% 12.87/6.94 % (3020193)lrs-1004_1_sil=8000:sp=occurrence:sos=all:erd=off:fs=off:bce=on:random_seed=2371788890:i=127:av=off:fsr=off:sup=off_2945 on theBenchmark for (2945ds/127Mi)
% 12.87/6.94 % (3020192)dis-1011_32:1_sfv=off:sil=16000:sos=all:erd=off:acc=on:fd=off:flr=on:random_seed=2303032895:cts=off:i=113:fsr=off:ss=included:sgt=4_2945 on theBenchmark for (2945ds/113Mi)
% 12.87/6.94 % (3020194)dis-1003_1024_sil=8000:sos=all:sac=on:random_seed=3817935499:cond=fast:i=114:sd=1:nm=0:fsr=off:gtg=exists_sym:ss=axioms_2945 on theBenchmark for (2945ds/114Mi)
% 12.87/6.94 % (3020193)Instruction limit reached!
% 12.87/6.94 % (3020193)------------------------------
% 12.87/6.94 % (3020193)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.87/6.94 % (3020193)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.87/6.94 % (3020193)CaDiCaL version: 2.1.3
% 12.87/6.94 % (3020193)Termination reason: Instruction limit
% 12.87/6.94 % (3020193)Termination phase: Preprocessing 1
% 12.87/6.94 % (3020193)Time elapsed: 0.050 s
% 12.87/6.94 % (3020193)Peak memory usage: 181 MB
% 12.87/6.94 % (3020193)Instructions burned: 128 (million)
% 12.87/6.94 % (3020192)Instruction limit reached!
% 12.87/6.94 % (3020192)------------------------------
% 12.87/6.94 % (3020192)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.00/7.16 % (3020192)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.00/7.16 % (3020192)CaDiCaL version: 2.1.3
% 16.00/7.16 % (3020192)Termination reason: Instruction limit
% 16.00/7.16 % (3020192)Termination phase: SInE selection
% 16.00/7.16 % (3020192)Time elapsed: 0.063 s
% 16.00/7.16 % (3020192)Peak memory usage: 181 MB
% 16.00/7.16 % (3020192)Instructions burned: 114 (million)
% 16.00/7.16 % (3020194)Instruction limit reached!
% 16.00/7.16 % (3020194)------------------------------
% 16.00/7.16 % (3020194)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.00/7.16 % (3020194)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.00/7.16 % (3020194)CaDiCaL version: 2.1.3
% 16.00/7.16 % (3020194)Termination reason: Instruction limit
% 16.00/7.16 % (3020194)Termination phase: Property scanning
% 16.00/7.16 % (3020194)Time elapsed: 0.077 s
% 16.00/7.16 % (3020194)Peak memory usage: 182 MB
% 16.00/7.16 % (3020194)Instructions burned: 115 (million)
% 16.00/7.16 % (3020199)lrs+10_1_sil=8000:sp=occurrence:random_seed=3593471862:st=1.2:i=907:sd=14:ss=axioms:sgt=12_2943 on theBenchmark for (2943ds/907Mi)
% 16.00/7.16 % (3020200)dis-1010_1_sil=16000:fde=unused:sp=occurrence:sos=on:random_seed=4227979330:i=437:sd=1:aac=none:ss=included_2943 on theBenchmark for (2943ds/437Mi)
% 16.00/7.16 % (3020201)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=498647498:i=5202:ss=axioms:sgt=16_2942 on theBenchmark for (2942ds/5202Mi)
% 16.00/7.16 % (3020199)Refutation not found, incomplete strategy
% 16.00/7.16 % (3020199)------------------------------
% 16.00/7.16 % (3020199)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.00/7.16 % (3020199)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.00/7.16 % (3020199)CaDiCaL version: 2.1.3
% 16.00/7.16 % (3020199)Termination reason: Refutation not found, incomplete strategy
% 16.00/7.16 % (3020199)Time elapsed: 0.170 s
% 16.00/7.16 % (3020199)Peak memory usage: 187 MB
% 16.00/7.16 % (3020199)Instructions burned: 557 (million)
% 16.00/7.16 % (3020200)Instruction limit reached!
% 16.00/7.16 % (3020200)------------------------------
% 16.00/7.16 % (3020200)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.00/7.16 % (3020200)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.00/7.16 % (3020200)CaDiCaL version: 2.1.3
% 16.00/7.16 % (3020200)Termination reason: Instruction limit
% 16.00/7.16 % (3020200)Termination phase: SInE selection
% 16.00/7.16 % (3020200)Time elapsed: 0.214 s
% 16.00/7.16 % (3020200)Peak memory usage: 181 MB
% 16.00/7.16 % (3020200)Instructions burned: 438 (million)
% 16.00/7.16 % (3020199)------------------------------
% 16.00/7.16 % (3020199)------------------------------
% 16.00/7.16 % (3020205)dis+10_3:1_sil=8000:acc=on:urr=on:br=off:sac=on:newcnf=on:random_seed=179052705:i=134:sd=2:doe=on:nm=16:sup=off:ss=included_2939 on theBenchmark for (2939ds/134Mi)
% 16.00/7.16 % (3020206)lrs+1002_8_sil=8000:sp=occurrence:sos=on:sac=on:random_seed=793518028:st=8:i=592:sd=3:ep=RST:ss=axioms_2938 on theBenchmark for (2938ds/592Mi)
% 16.00/7.16 % (3020205)Instruction limit reached!
% 16.00/7.16 % (3020205)------------------------------
% 16.00/7.16 % (3020205)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 16.00/7.16 % (3020205)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 16.00/7.16 % (3020205)CaDiCaL version: 2.1.3
% 16.00/7.16 % (3020205)Termination reason: Instruction limit
% 16.00/7.16 % (3020205)Termination phase: SInE selection
% 16.00/7.16 % (3020205)Time elapsed: 0.070 s
% 16.00/7.16 % (3020205)Peak memory usage: 181 MB
% 16.00/7.16 % (3020205)Instructions burned: 135 (million)
% 16.00/7.16 [W928 21:06:10.748477791 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 16.00/7.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 16.00/7.16 [W928 21:06:10.748511202 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 16.00/7.16 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 16.00/7.16 [W928 21:06:10.748556952 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.21/7.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.21/7.66 [W928 21:06:10.748569055 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.21/7.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.21/7.66 [W928 21:06:10.748598926 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.21/7.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.21/7.66 [W928 21:06:10.748663039 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.21/7.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.21/7.66 [W928 21:06:10.748700656 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.21/7.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.21/7.66 [W928 21:06:10.748711550 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.21/7.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.21/7.66 [W928 21:06:10.748740247 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.21/7.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.21/7.66 [W928 21:06:10.748751597 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.21/7.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.21/7.66 [W928 21:06:10.748776697 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.21/7.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.21/7.66 [W928 21:06:10.748788113 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.21/7.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.21/7.66 [W928 21:06:10.754873541 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.21/7.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.21/7.66 [W928 21:06:10.754919341 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.21/7.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.21/7.66 [W928 21:06:10.754965052 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 19.21/7.66 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 19.21/7.66 [W928 21:06:10.754978308 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 22.98/8.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 22.98/8.36 [W928 21:06:10.755014855 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 22.98/8.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 22.98/8.36 [W928 21:06:10.755028202 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 22.98/8.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 22.98/8.36 [W928 21:06:10.755055729 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 22.98/8.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 22.98/8.36 [W928 21:06:10.755066509 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 22.98/8.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 22.98/8.36 [W928 21:06:10.755107786 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 22.98/8.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 22.98/8.36 [W928 21:06:10.755118456 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 22.98/8.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 22.98/8.36 [W928 21:06:10.755145643 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 22.98/8.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 22.98/8.36 [W928 21:06:10.755155656 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 22.98/8.36 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 22.98/8.36 % (3020206)Instruction limit reached!
% 22.98/8.36 % (3020206)------------------------------
% 22.98/8.36 % (3020206)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.98/8.36 % (3020206)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.98/8.36 % (3020206)CaDiCaL version: 2.1.3
% 22.98/8.36 % (3020206)Termination reason: Instruction limit
% 22.98/8.36 % (3020206)Termination phase: SInE selection
% 22.98/8.36 % (3020206)Time elapsed: 0.143 s
% 22.98/8.36 % (3020206)Peak memory usage: 182 MB
% 22.98/8.36 % (3020206)Instructions burned: 596 (million)
% 22.98/8.36 % (3020209)lrs+10_1_ncem=casc2026/models/loop6.pt:sil=32000:npcc=on:random_seed=169847444:st=3:i=13193:sd=3:ss=axioms_2937 on theBenchmark for (2937ds/13193Mi)
% 22.98/8.36 % (3020210)lrs+1666_7_slsqr=4,1:sil=8000:plsq=on:plsqc=1:sos=on:urr=on:plsql=on:rp=on:alpa=false:sac=on:slsq=on:random_seed=1309363163:i=125:slsql=off:bs=unit_only:gtg=position:fdi=2:gsp=on:ss=axioms:sgt=8_2936 on theBenchmark for (2936ds/125Mi)
% 22.98/8.36 % (3020210)Instruction limit reached!
% 22.98/8.36 % (3020210)------------------------------
% 22.98/8.36 % (3020210)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 22.98/8.36 % (3020210)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 22.98/8.36 % (3020210)CaDiCaL version: 2.1.3
% 22.98/8.36 % (3020210)Termination reason: Instruction limit
% 22.98/8.36 % (3020210)Termination phase: Property scanning
% 22.98/8.36 % (3020210)Time elapsed: 0.044 s
% 22.98/8.36 % (3020210)Peak memory usage: 182 MB
% 22.98/8.36 % (3020210)Instructions burned: 127 (million)
% 25.77/8.72 % (3020213)lrs+10_1024_to=lpo:sil=8000:tgt=full:sp=arity:slsq=on:random_seed=2439584195:i=134:gtgl=5:slsql=off:gtg=exists_sym_2934 on theBenchmark for (2934ds/134Mi)
% 25.77/8.72 % (3020213)Instruction limit reached!
% 25.77/8.72 % (3020213)------------------------------
% 25.77/8.72 % (3020213)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.77/8.72 % (3020213)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.77/8.72 % (3020213)CaDiCaL version: 2.1.3
% 25.77/8.72 % (3020213)Termination reason: Instruction limit
% 25.77/8.72 % (3020213)Termination phase: Property scanning
% 25.77/8.72 % (3020213)Time elapsed: 0.046 s
% 25.77/8.72 % (3020213)Peak memory usage: 182 MB
% 25.77/8.72 % (3020213)Instructions burned: 139 (million)
% 25.77/8.72 % (3020215)lrs+10_1_sil=16000:plsq=on:plsqc=1:plsqr=32,1:sos=on:lcm=reverse:fd=off:newcnf=on:random_seed=1866265707:i=141:sd=1:gsp=on:sup=off:ss=axioms:sgt=8_2933 on theBenchmark for (2933ds/141Mi)
% 25.77/8.72 % (3020191)Instruction limit reached!
% 25.77/8.72 % (3020191)------------------------------
% 25.77/8.72 % (3020191)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.77/8.72 % (3020191)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.77/8.72 % (3020191)CaDiCaL version: 2.1.3
% 25.77/8.72 % (3020191)Termination reason: Instruction limit
% 25.77/8.72 % (3020191)Termination phase: Preprocessing 3
% 25.77/8.72 % (3020191)Time elapsed: 1.299 s
% 25.77/8.72 % (3020191)Peak memory usage: 218 MB
% 25.77/8.72 % (3020191)Instructions burned: 2350 (million)
% 25.77/8.72 % (3020215)Instruction limit reached!
% 25.77/8.72 % (3020215)------------------------------
% 25.77/8.72 % (3020215)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 25.77/8.72 % (3020215)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 25.77/8.72 % (3020215)CaDiCaL version: 2.1.3
% 25.77/8.72 % (3020215)Termination reason: Instruction limit
% 25.77/8.72 % (3020215)Termination phase: SInE selection
% 25.77/8.72 % (3020215)Time elapsed: 0.042 s
% 25.77/8.72 % (3020215)Peak memory usage: 181 MB
% 25.77/8.72 % (3020215)Instructions burned: 144 (million)
% 25.77/8.72 [W928 21:06:11.482216550 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 25.77/8.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 25.77/8.72 [W928 21:06:11.482249947 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 25.77/8.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 25.77/8.72 [W928 21:06:11.482295428 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 25.77/8.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 25.77/8.72 [W928 21:06:11.482309521 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 25.77/8.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 25.77/8.72 [W928 21:06:11.482338685 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 25.77/8.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 25.77/8.72 [W928 21:06:11.482350941 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 25.77/8.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 25.77/8.72 [W928 21:06:11.482379128 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 25.77/8.72 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 33.35/9.90 [W928 21:06:11.482400742 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 33.35/9.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 33.35/9.90 [W928 21:06:11.482431839 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 33.35/9.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 33.35/9.90 [W928 21:06:11.482445305 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 33.35/9.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 33.35/9.90 [W928 21:06:11.482472829 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 33.35/9.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 33.35/9.90 [W928 21:06:11.482484722 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 33.35/9.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 33.35/9.90 % (3020217)lrs+1011_1_sil=8000:plsq=on:sp=occurrence:fs=off:random_seed=3872871486:i=431:sd=1:fsr=off:sup=off:ss=axioms:sgt=64_2931 on theBenchmark for (2931ds/431Mi)
% 33.35/9.90 % (3020218)lrs+1010_1_ncem=casc2026/models/loop6.pt:sil=64000:tgt=full:npcc=on:prc=on:urr=ec_only:bsr=on:fd=preordered:gs=on:sac=on:newcnf=on:random_seed=2981794439:i=6060:aac=none:ins=25_2931 on theBenchmark for (2931ds/6060Mi)
% 33.35/9.90 [W928 21:06:12.174305524 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 33.35/9.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 33.35/9.90 [W928 21:06:12.174340587 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 33.35/9.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 33.35/9.90 [W928 21:06:12.174392634 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 33.35/9.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 33.35/9.90 [W928 21:06:12.174415691 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 33.35/9.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 33.35/9.90 [W928 21:06:12.174445278 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 33.35/9.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 33.35/9.90 [W928 21:06:12.174455795 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 33.35/9.90 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 33.35/9.90 [W928 21:06:12.174482325 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 39.33/10.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.33/10.94 [W928 21:06:12.174495638 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 39.33/10.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.33/10.94 [W928 21:06:12.174520865 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 39.33/10.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.33/10.94 [W928 21:06:12.174531212 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 39.33/10.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.33/10.94 [W928 21:06:12.174557452 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 39.33/10.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.33/10.94 [W928 21:06:12.174567646 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 39.33/10.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 39.33/10.94 % (3020217)Instruction limit reached!
% 39.33/10.94 % (3020217)------------------------------
% 39.33/10.94 % (3020217)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.33/10.94 % (3020217)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.33/10.94 % (3020217)CaDiCaL version: 2.1.3
% 39.33/10.94 % (3020217)Termination reason: Instruction limit
% 39.33/10.94 % (3020217)Termination phase: SInE selection
% 39.33/10.94 % (3020217)Time elapsed: 0.129 s
% 39.33/10.94 % (3020217)Peak memory usage: 182 MB
% 39.33/10.94 % (3020217)Instructions burned: 435 (million)
% 39.33/10.94 % (3020168)Refutation not found, incomplete strategy
% 39.33/10.94 % (3020168)------------------------------
% 39.33/10.94 % (3020168)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.33/10.94 % (3020168)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.33/10.94 % (3020168)CaDiCaL version: 2.1.3
% 39.33/10.94 % (3020168)Termination reason: Refutation not found, incomplete strategy
% 39.33/10.94 % (3020168)Time elapsed: 2.772 s
% 39.33/10.94 % (3020168)Peak memory usage: 541 MB
% 39.33/10.94 % (3020168)Instructions burned: 4012 (million)
% 39.33/10.94 % (3020221)lrs+10_16_anc=all:slsqr=32,1:sil=8000:avsql=on:sp=unary_frequency:lcm=predicate:urr=full:rp=on:br=off:slsqc=4:flr=on:sac=on:slsq=on:avsqc=1:random_seed=1270471930:avsq=on:s2a=on:i=150:kws=precedence:nicw=on:gsp=on:rawr=on_2922 on theBenchmark for (2922ds/150Mi)
% 39.33/10.94 % (3020169)Refutation not found, incomplete strategy
% 39.33/10.94 % (3020169)------------------------------
% 39.33/10.94 % (3020169)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.33/10.94 % (3020169)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.33/10.94 % (3020169)CaDiCaL version: 2.1.3
% 39.33/10.94 % (3020169)Termination reason: Refutation not found, incomplete strategy
% 39.33/10.94 % (3020169)Time elapsed: 2.811 s
% 39.33/10.94 % (3020169)Peak memory usage: 300 MB
% 39.33/10.94 % (3020169)Instructions burned: 4008 (million)
% 39.33/10.94 % (3020221)Instruction limit reached!
% 39.33/10.94 % (3020221)------------------------------
% 39.33/10.94 % (3020221)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 39.33/10.94 % (3020221)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 39.33/10.94 % (3020221)CaDiCaL version: 2.1.3
% 39.33/10.94 % (3020221)Termination reason: Instruction limit
% 39.33/10.94 % (3020221)Termination phase: SInE selection
% 39.33/10.94 % (3020221)Time elapsed: 0.047 s
% 39.33/10.94 % (3020221)Peak memory usage: 181 MB
% 39.33/10.94 % (3020221)Instructions burned: 150 (million)
% 39.33/10.94 % (3020223)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=arity:urr=on:random_seed=2244963333:i=14155:bd=all_2920 on theBenchmark for (2920ds/14155Mi)
% 52.05/12.42 % (3020168)------------------------------
% 52.05/12.42 % (3020168)------------------------------
% 52.05/12.42 % (3020169)------------------------------
% 52.05/12.42 % (3020169)------------------------------
% 52.05/12.42 % (3020225)lrs+10_1024_sil=16000:plsq=on:plsqr=32,1:sos=all:fs=off:gs=on:newcnf=on:random_seed=1033557113:i=667:av=off:fsr=off_2918 on theBenchmark for (2918ds/667Mi)
% 52.05/12.42 % (3020226)ott-1011_3:1_anc=all_dependent:to=lpo:sil=8000:drc=ordering:sas=cadical:fdtod=off:sp=reverse_frequency:spb=goal_then_units:urr=full:lftc=20:newcnf=on:random_seed=3308451310:s2a=on:i=185:s2at=1.8:fdi=4_2917 on theBenchmark for (2917ds/185Mi)
% 52.05/12.42 % (3020226)Instruction limit reached!
% 52.05/12.42 % (3020226)------------------------------
% 52.05/12.42 % (3020226)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.05/12.42 % (3020226)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.05/12.42 % (3020226)CaDiCaL version: 2.1.3
% 52.05/12.42 % (3020226)Termination reason: Instruction limit
% 52.05/12.42 % (3020226)Termination phase: SInE selection
% 52.05/12.42 % (3020226)Time elapsed: 0.103 s
% 52.05/12.42 % (3020226)Peak memory usage: 181 MB
% 52.05/12.42 % (3020226)Instructions burned: 187 (million)
% 52.05/12.42 % (3020201)Refutation not found, incomplete strategy
% 52.05/12.42 % (3020201)------------------------------
% 52.05/12.42 % (3020201)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.05/12.42 % (3020201)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.05/12.42 % (3020201)CaDiCaL version: 2.1.3
% 52.05/12.42 % (3020201)Termination reason: Refutation not found, incomplete strategy
% 52.05/12.42 % (3020201)Time elapsed: 2.756 s
% 52.05/12.42 % (3020201)Peak memory usage: 541 MB
% 52.05/12.42 % (3020201)Instructions burned: 4018 (million)
% 52.05/12.42 % (3020229)dis+1010_14_anc=all:to=lpo:sil=8000:sp=arity:slsq=on:random_seed=78136556:i=193:ins=10:fsr=off:ss=axioms:fsd=on_2914 on theBenchmark for (2914ds/193Mi)
% 52.05/12.42 % (3020229)Instruction limit reached!
% 52.05/12.42 % (3020229)------------------------------
% 52.05/12.42 % (3020229)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.05/12.42 % (3020229)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.05/12.42 % (3020229)CaDiCaL version: 2.1.3
% 52.05/12.42 % (3020229)Termination reason: Instruction limit
% 52.05/12.42 % (3020229)Termination phase: SInE selection
% 52.05/12.42 % (3020229)Time elapsed: 0.100 s
% 52.05/12.42 % (3020229)Peak memory usage: 181 MB
% 52.05/12.42 % (3020229)Instructions burned: 195 (million)
% 52.05/12.42 % (3020231)dis+1011_7_sil=8000:sp=occurrence:sos=all:fd=off:random_seed=4035399172:st=5.3:i=4850:sd=4:av=off:sup=off:ss=included:sgt=16_2912 on theBenchmark for (2912ds/4850Mi)
% 52.05/12.42 % (3020225)Instruction limit reached!
% 52.05/12.42 % (3020225)------------------------------
% 52.05/12.42 % (3020225)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.05/12.42 % (3020225)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.05/12.42 % (3020225)CaDiCaL version: 2.1.3
% 52.05/12.42 % (3020225)Termination reason: Instruction limit
% 52.05/12.42 % (3020225)Termination phase: Unused predicate definition removal
% 52.05/12.42 % (3020225)Time elapsed: 0.559 s
% 52.05/12.42 % (3020225)Peak memory usage: 208 MB
% 52.05/12.42 % (3020225)Instructions burned: 667 (million)
% 52.05/12.42 % (3020201)------------------------------
% 52.05/12.42 % (3020201)------------------------------
% 52.05/12.42 % (3020233)lrs+1011_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:random_seed=3359092632:i=12111:sd=1:ss=included_2910 on theBenchmark for (2910ds/12111Mi)
% 52.05/12.42 % (3020234)lrs-11_32_anc=all:sil=8000:spb=goal_then_units:sac=on:random_seed=3258561224:i=319:kws=precedence:fsr=off_2910 on theBenchmark for (2910ds/319Mi)
% 52.05/12.42 % (3020231)Refutation not found, incomplete strategy
% 52.05/12.42 % (3020231)------------------------------
% 52.05/12.42 % (3020231)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 52.05/12.42 % (3020231)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 52.05/12.42 % (3020231)CaDiCaL version: 2.1.3
% 52.05/12.42 % (3020231)Termination reason: Refutation not found, incomplete strategy
% 52.05/12.42 % (3020231)Time elapsed: 0.326 s
% 52.05/12.42 % (3020231)Peak memory usage: 187 MB
% 52.05/12.42 % (3020231)Instructions burned: 568 (million)
% 56.59/13.10 % (3020209)Refutation not found, incomplete strategy
% 56.59/13.10 % (3020209)------------------------------
% 56.59/13.10 % (3020209)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.59/13.10 % (3020209)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.59/13.10 % (3020209)CaDiCaL version: 2.1.3
% 56.59/13.10 % (3020209)Termination reason: Refutation not found, incomplete strategy
% 56.59/13.10 % (3020209)Time elapsed: 2.895 s
% 56.59/13.10 % (3020209)Peak memory usage: 510 MB
% 56.59/13.10 % (3020209)Instructions burned: 4281 (million)
% 56.59/13.10 % (3020234)Instruction limit reached!
% 56.59/13.10 % (3020234)------------------------------
% 56.59/13.10 % (3020234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.59/13.10 % (3020234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.59/13.10 % (3020234)CaDiCaL version: 2.1.3
% 56.59/13.10 % (3020234)Termination reason: Instruction limit
% 56.59/13.10 % (3020234)Termination phase: Preprocessing 1
% 56.59/13.10 % (3020234)Time elapsed: 0.210 s
% 56.59/13.10 % (3020234)Peak memory usage: 181 MB
% 56.59/13.10 % (3020234)Instructions burned: 320 (million)
% 56.59/13.10 % (3020237)dis+2_1024_sil=8000:sp=reverse_arity:sos=on:lcm=reverse:sac=on:random_seed=420796181:i=2064:ep=RST_2906 on theBenchmark for (2906ds/2064Mi)
% 56.59/13.10 % (3020231)------------------------------
% 56.59/13.10 % (3020231)------------------------------
% 56.59/13.10 % (3020209)------------------------------
% 56.59/13.10 % (3020209)------------------------------
% 56.59/13.10 % (3020239)dis-1011_128_sil=32000:random_seed=50752779:i=3706:ep=RST:av=off_2904 on theBenchmark for (2904ds/3706Mi)
% 56.59/13.10 % (3020240)lrs-1002_1_sil=8000:plsq=on:plsqr=32,1:sp=occurrence:sos=on:fs=off:gs=on:newcnf=on:random_seed=1745771768:i=757:sd=2:fsr=off:ss=axioms:sgt=40_2903 on theBenchmark for (2903ds/757Mi)
% 56.59/13.10 % (3020240)Refutation not found, incomplete strategy
% 56.59/13.10 % (3020240)------------------------------
% 56.59/13.10 % (3020240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 56.59/13.10 % (3020240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 56.59/13.10 % (3020240)CaDiCaL version: 2.1.3
% 56.59/13.10 % (3020240)Termination reason: Refutation not found, incomplete strategy
% 56.59/13.10 % (3020240)Time elapsed: 0.319 s
% 56.59/13.10 % (3020240)Peak memory usage: 187 MB
% 56.59/13.10 % (3020240)Instructions burned: 549 (million)
% 56.59/13.10 [W928 21:06:14.760793969 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 56.59/13.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 56.59/13.10 [W928 21:06:14.760827536 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 56.59/13.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 56.59/13.10 [W928 21:06:14.760875083 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 56.59/13.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 56.59/13.10 [W928 21:06:14.760887773 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 56.59/13.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 56.59/13.10 [W928 21:06:14.760915153 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 56.59/13.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 56.59/13.10 [W928 21:06:14.760926780 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 56.59/13.10 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 56.59/13.10 [W928 21:06:14.760955576 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 67.56/14.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.56/14.60 [W928 21:06:14.760966110 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 67.56/14.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.56/14.60 [W928 21:06:14.760991253 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 67.56/14.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.56/14.60 [W928 21:06:14.761023580 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 67.56/14.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.56/14.60 [W928 21:06:14.761051560 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 67.56/14.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.56/14.60 [W928 21:06:14.761061850 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 67.56/14.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.56/14.60 % (3020240)------------------------------
% 67.56/14.60 % (3020240)------------------------------
% 67.56/14.60 % (3020243)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sp=occurrence:random_seed=1878951669:i=13913:ss=axioms:sgt=8_2895 on theBenchmark for (2895ds/13913Mi)
% 67.56/14.60 % (3020237)Instruction limit reached!
% 67.56/14.60 % (3020237)------------------------------
% 67.56/14.60 % (3020237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.56/14.60 % (3020237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.56/14.60 % (3020237)CaDiCaL version: 2.1.3
% 67.56/14.60 % (3020237)Termination reason: Instruction limit
% 67.56/14.60 % (3020237)Termination phase: Property scanning
% 67.56/14.60 % (3020237)Time elapsed: 1.182 s
% 67.56/14.60 % (3020237)Peak memory usage: 227 MB
% 67.56/14.60 % (3020237)Instructions burned: 2066 (million)
% 67.56/14.60 % (3020245)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=const_frequency:sos=all:lma=off:random_seed=4071136875:i=9925:aac=none_2893 on theBenchmark for (2893ds/9925Mi)
% 67.56/14.60 % (3020239)Instruction limit reached!
% 67.56/14.60 % (3020239)------------------------------
% 67.56/14.60 % (3020239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 67.56/14.60 % (3020239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 67.56/14.60 % (3020239)CaDiCaL version: 2.1.3
% 67.56/14.60 % (3020239)Termination reason: Instruction limit
% 67.56/14.60 % (3020239)Termination phase: Property scanning
% 67.56/14.60 % (3020239)Time elapsed: 1.972 s
% 67.56/14.60 % (3020239)Peak memory usage: 239 MB
% 67.56/14.60 % (3020239)Instructions burned: 3707 (million)
% 67.56/14.60 [W928 21:06:16.241999375 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 67.56/14.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.56/14.60 [W928 21:06:16.242043842 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 67.56/14.60 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 67.56/14.60 [W928 21:06:16.242093963 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 71.95/15.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.95/15.28 [W928 21:06:16.242106286 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 71.95/15.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.95/15.28 [W928 21:06:16.242147576 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 71.95/15.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.95/15.28 [W928 21:06:16.242157850 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 71.95/15.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.95/15.28 [W928 21:06:16.242182993 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 71.95/15.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.95/15.28 [W928 21:06:16.242192997 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 71.95/15.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.95/15.28 [W928 21:06:16.242217617 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 71.95/15.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.95/15.28 [W928 21:06:16.242228134 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 71.95/15.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.95/15.28 [W928 21:06:16.242255610 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 71.95/15.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.95/15.28 [W928 21:06:16.242319888 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 71.95/15.28 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 71.95/15.28 % (3020247)dis-1010_50_to=lpo:sil=32000:sp=arity:sos=on:spb=goal_then_units:urr=ec_only:slsq=on:random_seed=3489676925:i=2479:sd=2:nm=16:fsr=off:ss=axioms_2882 on theBenchmark for (2882ds/2479Mi)
% 71.95/15.28 % (3020233)Refutation not found, incomplete strategy
% 71.95/15.28 % (3020233)------------------------------
% 71.95/15.28 % (3020233)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.95/15.28 % (3020233)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 71.95/15.28 % (3020233)CaDiCaL version: 2.1.3
% 71.95/15.28 % (3020233)Termination reason: Refutation not found, incomplete strategy
% 71.95/15.28 % (3020233)Time elapsed: 2.894 s
% 71.95/15.28 % (3020233)Peak memory usage: 549 MB
% 71.95/15.28 % (3020233)Instructions burned: 4042 (million)
% 71.95/15.28 % (3020233)------------------------------
% 71.95/15.28 % (3020233)------------------------------
% 71.95/15.28 % (3020247)Refutation not found, incomplete strategy
% 71.95/15.28 % (3020247)------------------------------
% 71.95/15.28 % (3020247)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 71.95/15.28 % (3020247)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.89/17.38 % (3020247)CaDiCaL version: 2.1.3
% 86.89/17.38 % (3020247)Termination reason: Refutation not found, incomplete strategy
% 86.89/17.38 % (3020247)Time elapsed: 0.585 s
% 86.89/17.38 % (3020247)Peak memory usage: 186 MB
% 86.89/17.38 % (3020247)Instructions burned: 1246 (million)
% 86.89/17.38 % (3020249)ott+1002_64_sil=16000:sp=const_min:nwc=0.5:random_seed=727839957:i=440:nm=2:av=off:gtg=exists_all:fdi=8:gsp=on_2876 on theBenchmark for (2876ds/440Mi)
% 86.89/17.38 % (3020218)Instruction limit reached!
% 86.89/17.38 % (3020218)------------------------------
% 86.89/17.38 % (3020218)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.89/17.38 % (3020218)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.89/17.38 % (3020218)CaDiCaL version: 2.1.3
% 86.89/17.38 % (3020218)Termination reason: Instruction limit
% 86.89/17.38 % (3020218)Termination phase: Saturation
% 86.89/17.38 % (3020218)Time elapsed: 4.934 s
% 86.89/17.38 % (3020218)Peak memory usage: 833 MB
% 86.89/17.38 % (3020218)Instructions burned: 6060 (million)
% 86.89/17.38 % (3020249)Instruction limit reached!
% 86.89/17.38 % (3020249)------------------------------
% 86.89/17.38 % (3020249)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.89/17.38 % (3020249)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.89/17.38 % (3020249)CaDiCaL version: 2.1.3
% 86.89/17.38 % (3020249)Termination reason: Instruction limit
% 86.89/17.38 % (3020249)Termination phase: Property scanning
% 86.89/17.38 % (3020249)Time elapsed: 0.198 s
% 86.89/17.38 % (3020249)Peak memory usage: 182 MB
% 86.89/17.38 % (3020249)Instructions burned: 440 (million)
% 86.89/17.38 % (3020247)------------------------------
% 86.89/17.38 % (3020247)------------------------------
% 86.89/17.38 % (3020251)dis-1011_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:erd=off:lsd=100:bsr=unit_only:random_seed=86553390:st=1.5:i=11145:s2at=3:sd=3:fsr=off:ss=axioms_2873 on theBenchmark for (2873ds/11145Mi)
% 86.89/17.38 % (3020252)lrs+1002_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_frequency:lcm=reverse:urr=on:bsr=on:random_seed=2690045658:cts=off:i=3034:av=off:er=known:fsd=on_2872 on theBenchmark for (2872ds/3034Mi)
% 86.89/17.38 % (3020253)lrs-1011_64:1_sil=8000:erd=off:urr=on:nwc=0.7:br=off:random_seed=2922730132:st=2:s2a=on:i=524:s2at=2:ss=axioms_2872 on theBenchmark for (2872ds/524Mi)
% 86.89/17.38 % (3020253)Instruction limit reached!
% 86.89/17.38 % (3020253)------------------------------
% 86.89/17.38 % (3020253)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.89/17.38 % (3020253)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.89/17.38 % (3020253)CaDiCaL version: 2.1.3
% 86.89/17.38 % (3020253)Termination reason: Instruction limit
% 86.89/17.38 % (3020253)Termination phase: SInE selection
% 86.89/17.38 % (3020253)Time elapsed: 0.244 s
% 86.89/17.38 % (3020253)Peak memory usage: 181 MB
% 86.89/17.38 % (3020253)Instructions burned: 527 (million)
% 86.89/17.38 % (3020257)lrs+1011_16:1_sil=8000:acc=on:urr=on:fd=preordered:flr=on:random_seed=646372833:avsq=on:i=1016:avsqr=676809,524288:sd=1:ss=axioms_2868 on theBenchmark for (2868ds/1016Mi)
% 86.89/17.38 % (3020243)Refutation not found, incomplete strategy
% 86.89/17.38 % (3020243)------------------------------
% 86.89/17.38 % (3020243)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.89/17.38 % (3020243)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.89/17.38 % (3020243)CaDiCaL version: 2.1.3
% 86.89/17.38 % (3020243)Termination reason: Refutation not found, incomplete strategy
% 86.89/17.38 % (3020243)Time elapsed: 2.775 s
% 86.89/17.38 % (3020243)Peak memory usage: 537 MB
% 86.89/17.38 % (3020243)Instructions burned: 3878 (million)
% 86.89/17.38 % (3020257)Refutation not found, incomplete strategy
% 86.89/17.38 % (3020257)------------------------------
% 86.89/17.38 % (3020257)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 86.89/17.38 % (3020257)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 86.89/17.38 % (3020257)CaDiCaL version: 2.1.3
% 86.89/17.38 % (3020257)Termination reason: Refutation not found, incomplete strategy
% 86.89/17.38 % (3020257)Time elapsed: 0.343 s
% 86.89/17.38 % (3020257)Peak memory usage: 186 MB
% 86.89/17.38 % (3020257)Instructions burned: 674 (million)
% 86.89/17.38 % (3020243)------------------------------
% 86.89/17.38 % (3020243)------------------------------
% 86.89/17.38 % (3020259)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:drc=off:fde=none:s2agt=16:random_seed=943945332:i=14123:bd=preordered:ins=4_2862 on theBenchmark for (2862ds/14123Mi)
% 92.80/18.18 % (3020257)------------------------------
% 92.80/18.18 % (3020257)------------------------------
% 92.80/18.18 % (3020261)dis+10_4096_slsqr=16,1:sil=32000:tgt=full:plsq=on:bsr=unit_only:slsqc=1:slsq=on:random_seed=1217172903:i=5781:kws=precedence:bd=all:rawr=on_2859 on theBenchmark for (2859ds/5781Mi)
% 92.80/18.18 [W928 21:06:18.732765189 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 92.80/18.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 92.80/18.18 [W928 21:06:18.732813403 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 92.80/18.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 92.80/18.18 [W928 21:06:18.732860053 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 92.80/18.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 92.80/18.18 [W928 21:06:18.732874140 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 92.80/18.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 92.80/18.18 [W928 21:06:18.732900703 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 92.80/18.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 92.80/18.18 [W928 21:06:18.732912710 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 92.80/18.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 92.80/18.18 [W928 21:06:18.732941083 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 92.80/18.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 92.80/18.18 [W928 21:06:18.732953237 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 92.80/18.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 92.80/18.18 [W928 21:06:18.732979784 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 92.80/18.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 92.80/18.18 [W928 21:06:18.732991664 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 92.80/18.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 92.80/18.18 [W928 21:06:18.733032181 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 92.80/18.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 92.80/18.18 [W928 21:06:18.733045331 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 92.80/18.18 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 92.80/18.18 % (3020252)Instruction limit reached!
% 96.97/18.88 % (3020252)------------------------------
% 96.97/18.88 % (3020252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.97/18.88 % (3020252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.97/18.88 % (3020252)CaDiCaL version: 2.1.3
% 96.97/18.88 % (3020252)Termination reason: Instruction limit
% 96.97/18.88 % (3020252)Termination phase: Property scanning
% 96.97/18.88 % (3020252)Time elapsed: 1.736 s
% 96.97/18.88 % (3020252)Peak memory usage: 227 MB
% 96.97/18.88 % (3020252)Instructions burned: 3036 (million)
% 96.97/18.88 % (3020263)lrs-1011_1_to=lpo:ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:drc=off:sp=reverse_frequency:erd=off:urr=on:br=off:random_seed=56440310:i=2448:gtgl=5:bd=preordered:gtg=all_2853 on theBenchmark for (2853ds/2448Mi)
% 96.97/18.88 % (3020223)Instruction limit reached!
% 96.97/18.88 % (3020223)------------------------------
% 96.97/18.88 % (3020223)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.97/18.88 % (3020223)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.97/18.88 % (3020223)CaDiCaL version: 2.1.3
% 96.97/18.88 % (3020223)Termination reason: Instruction limit
% 96.97/18.88 % (3020223)Termination phase: Saturation
% 96.97/18.88 % (3020223)Time elapsed: 6.869 s
% 96.97/18.88 % (3020223)Peak memory usage: 1305 MB
% 96.97/18.88 % (3020223)Instructions burned: 14156 (million)
% 96.97/18.88 % (3020265)lrs+1011_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:lcm=reverse:random_seed=878557170:i=3223:kws=precedence:fgj=on:av=off_2849 on theBenchmark for (2849ds/3223Mi)
% 96.97/18.88 % (3020263)Instruction limit reached!
% 96.97/18.88 % (3020263)------------------------------
% 96.97/18.88 % (3020263)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.97/18.88 % (3020263)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.97/18.88 % (3020263)CaDiCaL version: 2.1.3
% 96.97/18.88 % (3020263)Termination reason: Instruction limit
% 96.97/18.88 % (3020263)Termination phase: Property scanning
% 96.97/18.88 % (3020263)Time elapsed: 0.996 s
% 96.97/18.88 % (3020263)Peak memory usage: 182 MB
% 96.97/18.88 % (3020263)Instructions burned: 2448 (million)
% 96.97/18.88 % (3020251)Refutation not found, incomplete strategy
% 96.97/18.88 % (3020251)------------------------------
% 96.97/18.88 % (3020251)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.97/18.88 % (3020251)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.97/18.88 % (3020251)CaDiCaL version: 2.1.3
% 96.97/18.88 % (3020251)Termination reason: Refutation not found, incomplete strategy
% 96.97/18.88 % (3020251)Time elapsed: 3.026 s
% 96.97/18.88 % (3020251)Peak memory usage: 550 MB
% 96.97/18.88 % (3020251)Instructions burned: 4569 (million)
% 96.97/18.88 % (3020267)lrs+1002_1_ncem=casc2026/models/loop4.pt:sil=8000:npcc=on:sp=occurrence:sos=on:random_seed=2903090746:st=5.6:i=2033:sd=3:ss=axioms_2841 on theBenchmark for (2841ds/2033Mi)
% 96.97/18.88 % (3020265)Instruction limit reached!
% 96.97/18.88 % (3020265)------------------------------
% 96.97/18.88 % (3020265)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.97/18.88 % (3020265)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.97/18.88 % (3020265)CaDiCaL version: 2.1.3
% 96.97/18.88 % (3020265)Termination reason: Instruction limit
% 96.97/18.88 % (3020265)Termination phase: Property scanning
% 96.97/18.88 % (3020265)Time elapsed: 0.976 s
% 96.97/18.88 % (3020265)Peak memory usage: 227 MB
% 96.97/18.88 % (3020265)Instructions burned: 3225 (million)
% 96.97/18.88 % (3020251)------------------------------
% 96.97/18.88 % (3020251)------------------------------
% 96.97/18.88 % (3020269)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:bsd=on:random_seed=3257197853:i=2055:nm=16:gtg=position:ss=axioms:fsd=on_2838 on theBenchmark for (2838ds/2055Mi)
% 96.97/18.88 % (3020271)dis+1010_1_ncem=casc2026/models/loop7.pt:sil=64000:tgt=full:npcc=on:fde=unused:sp=const_frequency:spb=goal:acc=on:random_seed=92073738:i=21611:sd=3:ss=axioms_2837 on theBenchmark for (2837ds/21611Mi)
% 96.97/18.88 % (3020269)Instruction limit reached!
% 96.97/18.88 % (3020269)------------------------------
% 96.97/18.88 % (3020269)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 96.97/18.88 % (3020269)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 96.97/18.88 % (3020269)CaDiCaL version: 2.1.3
% 96.97/18.88 % (3020269)Termination reason: Instruction limit
% 96.97/18.88 % (3020269)Termination phase: SInE selection
% 96.97/18.88 % (3020269)Time elapsed: 0.488 s
% 107.99/20.38 % (3020269)Peak memory usage: 182 MB
% 107.99/20.38 % (3020269)Instructions burned: 2059 (million)
% 107.99/20.38 % (3020273)lrs+10_1_sil=8000:sp=occurrence:sos=all:lma=off:random_seed=3628252232:i=4835:sd=13:ss=axioms:sgt=23_2832 on theBenchmark for (2832ds/4835Mi)
% 107.99/20.38 % (3020273)Refutation not found, incomplete strategy
% 107.99/20.38 % (3020273)------------------------------
% 107.99/20.38 % (3020273)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.99/20.38 % (3020273)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.99/20.38 % (3020273)CaDiCaL version: 2.1.3
% 107.99/20.38 % (3020273)Termination reason: Refutation not found, incomplete strategy
% 107.99/20.38 % (3020273)Time elapsed: 0.174 s
% 107.99/20.38 % (3020273)Peak memory usage: 187 MB
% 107.99/20.38 % (3020273)Instructions burned: 549 (million)
% 107.99/20.38 % (3020267)Instruction limit reached!
% 107.99/20.38 % (3020267)------------------------------
% 107.99/20.38 % (3020267)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.99/20.38 % (3020267)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.99/20.38 % (3020267)CaDiCaL version: 2.1.3
% 107.99/20.38 % (3020267)Termination reason: Instruction limit
% 107.99/20.38 % (3020267)Termination phase: Saturation
% 107.99/20.38 % (3020267)Time elapsed: 1.112 s
% 107.99/20.38 % (3020267)Peak memory usage: 215 MB
% 107.99/20.38 % (3020267)Instructions burned: 2033 (million)
% 107.99/20.38 % (3020273)------------------------------
% 107.99/20.38 % (3020273)------------------------------
% 107.99/20.38 % (3020275)lrs+10_1_to=lpo:sil=32000:plsq=on:plsqc=1:bsd=on:plsqr=64,1:sp=reverse_frequency:bsr=unit_only:plsql=on:fd=off:slsqc=4:newcnf=on:slsq=on:random_seed=1710224167:st=5:i=797:s2at=3:sd=4:bs=unit_only:av=off:sup=off:ss=included_2829 on theBenchmark for (2829ds/797Mi)
% 107.99/20.38 % (3020261)Instruction limit reached!
% 107.99/20.38 % (3020261)------------------------------
% 107.99/20.38 % (3020261)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 107.99/20.38 % (3020261)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 107.99/20.38 % (3020261)CaDiCaL version: 2.1.3
% 107.99/20.38 % (3020261)Termination reason: Instruction limit
% 107.99/20.38 % (3020261)Termination phase: Saturation
% 107.99/20.38 % (3020261)Time elapsed: 3.077 s
% 107.99/20.38 % (3020261)Peak memory usage: 259 MB
% 107.99/20.38 % (3020261)Instructions burned: 5781 (million)
% 107.99/20.38 % (3020276)lrs-1011_5_sil=8000:sp=const_max:sos=on:lsd=50:rnwc=on:rp=on:nwc=2.6:alpa=false:random_seed=1480200137:i=2326:kws=inv_precedence:aac=none:nicw=on:bs=unit_only:nm=16:ins=2:fsd=on_2828 on theBenchmark for (2828ds/2326Mi)
% 107.99/20.38 % (3020278)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:sos=all:urr=on:br=off:random_seed=1621162962:i=6038:nm=6_2827 on theBenchmark for (2827ds/6038Mi)
% 107.99/20.38 [W928 21:06:22.001813620 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 107.99/20.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 107.99/20.38 [W928 21:06:22.001858374 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 107.99/20.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 107.99/20.38 [W928 21:06:22.001903934 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 107.99/20.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 107.99/20.38 [W928 21:06:22.001917754 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 107.99/20.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 107.99/20.38 [W928 21:06:22.001944864 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 107.99/20.38 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 118.47/21.91 [W928 21:06:22.001956971 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 118.47/21.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 118.47/21.91 [W928 21:06:22.001990611 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 118.47/21.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 118.47/21.91 [W928 21:06:22.002020755 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 118.47/21.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 118.47/21.91 [W928 21:06:22.002049188 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 118.47/21.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 118.47/21.91 [W928 21:06:22.002060372 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 118.47/21.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 118.47/21.91 [W928 21:06:22.002086385 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 118.47/21.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 118.47/21.91 [W928 21:06:22.002097099 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 118.47/21.91 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 118.47/21.91 % (3020275)Instruction limit reached!
% 118.47/21.91 % (3020275)------------------------------
% 118.47/21.91 % (3020275)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.47/21.91 % (3020275)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.47/21.91 % (3020275)CaDiCaL version: 2.1.3
% 118.47/21.91 % (3020275)Termination reason: Instruction limit
% 118.47/21.91 % (3020275)Termination phase: SInE selection
% 118.47/21.91 % (3020275)Time elapsed: 0.344 s
% 118.47/21.91 % (3020275)Peak memory usage: 182 MB
% 118.47/21.91 % (3020275)Instructions burned: 797 (million)
% 118.47/21.91 % (3020281)lrs+10_1_sil=32000:sp=occurrence:random_seed=42228559:st=2:i=33334:sd=3:ss=included:sgt=32_2824 on theBenchmark for (2824ds/33334Mi)
% 118.47/21.91 % (3020281)Refutation not found, incomplete strategy
% 118.47/21.91 % (3020281)------------------------------
% 118.47/21.91 % (3020281)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.47/21.91 % (3020281)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.47/21.91 % (3020281)CaDiCaL version: 2.1.3
% 118.47/21.91 % (3020281)Termination reason: Refutation not found, incomplete strategy
% 118.47/21.91 % (3020281)Time elapsed: 0.303 s
% 118.47/21.91 % (3020281)Peak memory usage: 187 MB
% 118.47/21.91 % (3020281)Instructions burned: 555 (million)
% 118.47/21.91 % (3020276)Instruction limit reached!
% 118.47/21.91 % (3020276)------------------------------
% 118.47/21.91 % (3020276)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 118.47/21.91 % (3020276)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 118.47/21.91 % (3020276)CaDiCaL version: 2.1.3
% 118.47/21.91 % (3020276)Termination reason: Instruction limit
% 118.47/21.91 % (3020276)Termination phase: Property scanning
% 118.47/21.91 % (3020276)Time elapsed: 0.770 s
% 118.47/21.91 % (3020276)Peak memory usage: 227 MB
% 118.47/21.91 % (3020276)Instructions burned: 2331 (million)
% 118.47/21.91 % (3020283)lrs+10_4_sil=8000:plsq=on:plsqr=1,64:sp=occurrence:urr=on:bsr=on:br=off:random_seed=1894474856:st=3.7:s2a=on:i=1008:s2at=1.2:sd=3:bd=all:av=off:fdi=8:sup=off:ss=axioms_2819 on theBenchmark for (2819ds/1008Mi)
% 121.51/22.29 % (3020281)------------------------------
% 121.51/22.29 % (3020281)------------------------------
% 121.51/22.29 % (3020283)Instruction limit reached!
% 121.51/22.29 % (3020283)------------------------------
% 121.51/22.29 % (3020283)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.51/22.29 % (3020283)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.51/22.29 % (3020283)CaDiCaL version: 2.1.3
% 121.51/22.29 % (3020283)Termination reason: Instruction limit
% 121.51/22.29 % (3020283)Termination phase: SInE selection
% 121.51/22.29 % (3020283)Time elapsed: 0.242 s
% 121.51/22.29 % (3020283)Peak memory usage: 182 MB
% 121.51/22.29 % (3020283)Instructions burned: 1012 (million)
% 121.51/22.29 % (3020285)lrs+10_1_to=lpo:ncem=casc2026/models/loop6.pt:sil=128000:tgt=ground:npcc=on:fde=none:sp=const_frequency:spb=intro:gs=on:random_seed=2998388403:i=8327:s2at=5:bd=preordered_2816 on theBenchmark for (2816ds/8327Mi)
% 121.51/22.29 % (3020286)lrs+1002_1_slsqr=3,2:sil=8000:tgt=full:plsq=on:fde=unused:plsqc=1:plsqr=3,2:sp=reverse_arity:spb=intro:urr=on:plsql=on:s2agt=16:br=off:slsqc=2:slsq=on:random_seed=2972040499:s2a=on:i=1083:s2at=1.87328:slsql=off:ep=RSTC:fdi=16_2815 on theBenchmark for (2815ds/1083Mi)
% 121.51/22.29 % (3020245)Instruction limit reached!
% 121.51/22.29 % (3020245)------------------------------
% 121.51/22.29 % (3020245)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.51/22.29 % (3020245)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.51/22.29 % (3020245)CaDiCaL version: 2.1.3
% 121.51/22.29 % (3020245)Termination reason: Instruction limit
% 121.51/22.29 % (3020245)Termination phase: Saturation
% 121.51/22.29 % (3020245)Time elapsed: 7.754 s
% 121.51/22.29 % (3020245)Peak memory usage: 1259 MB
% 121.51/22.29 % (3020245)Instructions burned: 9927 (million)
% 121.51/22.29 % (3020289)lrs-1004_3_to=lpo:sil=16000:drc=off:sims=off:spb=goal:fd=preordered:random_seed=428116255:i=1084:sd=1:bd=preordered:av=off:fsr=off:ss=axioms:sgt=14_2812 on theBenchmark for (2812ds/1084Mi)
% 121.51/22.29 % (3020286)Instruction limit reached!
% 121.51/22.29 % (3020286)------------------------------
% 121.51/22.29 % (3020286)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.51/22.29 % (3020286)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.51/22.29 % (3020286)CaDiCaL version: 2.1.3
% 121.51/22.29 % (3020286)Termination reason: Instruction limit
% 121.51/22.29 % (3020286)Termination phase: Unused predicate definition removal
% 121.51/22.29 % (3020286)Time elapsed: 0.384 s
% 121.51/22.29 % (3020286)Peak memory usage: 196 MB
% 121.51/22.29 % (3020286)Instructions burned: 1084 (million)
% 121.51/22.29 % (3020291)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:erd=off:spb=goal:sac=on:newcnf=on:random_seed=886638059:i=6995:s2at=5:gtg=all_2810 on theBenchmark for (2810ds/6995Mi)
% 121.51/22.29 % (3020271)Refutation not found, incomplete strategy
% 121.51/22.29 % (3020271)------------------------------
% 121.51/22.29 % (3020271)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.51/22.29 % (3020271)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.51/22.29 % (3020271)CaDiCaL version: 2.1.3
% 121.51/22.29 % (3020271)Termination reason: Refutation not found, incomplete strategy
% 121.51/22.29 % (3020271)Time elapsed: 2.757 s
% 121.51/22.29 % (3020271)Peak memory usage: 539 MB
% 121.51/22.29 % (3020271)Instructions burned: 4070 (million)
% 121.51/22.29 % (3020289)Refutation not found, incomplete strategy
% 121.51/22.29 % (3020289)------------------------------
% 121.51/22.29 % (3020289)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 121.51/22.29 % (3020289)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 121.51/22.29 % (3020289)CaDiCaL version: 2.1.3
% 121.51/22.29 % (3020289)Termination reason: Refutation not found, incomplete strategy
% 121.51/22.29 % (3020289)Time elapsed: 0.356 s
% 121.51/22.29 % (3020289)Peak memory usage: 186 MB
% 121.51/22.29 % (3020289)Instructions burned: 667 (million)
% 121.51/22.29 % (3020271)------------------------------
% 121.51/22.29 % (3020271)------------------------------
% 121.51/22.29 % (3020289)------------------------------
% 121.51/22.29 % (3020289)------------------------------
% 121.51/22.29 % (3020293)lrs+10_1_sil=32000:sp=occurrence:sos=on:urr=on:rnwc=on:random_seed=2280883005:st=2:i=6225:sd=15:ss=axioms_2805 on theBenchmark for (2805ds/6225Mi)
% 121.51/22.29 % (3020294)dis-1011_1_ncem=casc2026/models/loop7.pt:sil=64000:npcc=on:lcm=reverse:random_seed=2924563125:cond=fast:i=3372:sd=1:nm=16:gtg=position:ss=axioms_2804 on theBenchmark for (2804ds/3372Mi)
% 129.46/23.31 % (3020293)Refutation not found, incomplete strategy
% 129.46/23.31 % (3020293)------------------------------
% 129.46/23.31 % (3020293)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.46/23.31 % (3020293)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.46/23.31 % (3020293)CaDiCaL version: 2.1.3
% 129.46/23.31 % (3020293)Termination reason: Refutation not found, incomplete strategy
% 129.46/23.31 % (3020293)Time elapsed: 0.417 s
% 129.46/23.31 % (3020293)Peak memory usage: 186 MB
% 129.46/23.31 % (3020293)Instructions burned: 829 (million)
% 129.46/23.31 % (3020293)------------------------------
% 129.46/23.31 % (3020293)------------------------------
% 129.46/23.31 % (3020297)lrs+1010_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:sos=all:random_seed=4023538992:st=2.3:i=26457:sd=10:ss=included:sgt=8_2796 on theBenchmark for (2796ds/26457Mi)
% 129.46/23.31 % (3020291)Instruction limit reached!
% 129.46/23.31 % (3020291)------------------------------
% 129.46/23.31 % (3020291)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 129.46/23.31 % (3020291)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 129.46/23.31 % (3020291)CaDiCaL version: 2.1.3
% 129.46/23.31 % (3020291)Termination reason: Instruction limit
% 129.46/23.31 % (3020291)Termination phase: Property scanning
% 129.46/23.31 % (3020291)Time elapsed: 1.911 s
% 129.46/23.31 % (3020291)Peak memory usage: 283 MB
% 129.46/23.31 % (3020291)Instructions burned: 6995 (million)
% 129.46/23.31 % (3020299)lrs+10_1_anc=all:sfv=off:to=kbo:ncem=casc2026/models/loop7.pt:sil=128000:tgt=ground:npcc=on:sp=const_frequency:acc=on:urr=on:foolp=on:s2agt=20:sac=on:random_seed=1839880022:i=13494:s2at=1.31:bd=all:ins=10:gtg=exists_top_2790 on theBenchmark for (2790ds/13494Mi)
% 129.46/23.31 [W928 21:06:25.728944033 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 129.46/23.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 129.46/23.31 [W928 21:06:25.728987504 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 129.46/23.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 129.46/23.31 [W928 21:06:25.729047594 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 129.46/23.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 129.46/23.31 [W928 21:06:25.729059387 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 129.46/23.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 129.46/23.31 [W928 21:06:25.729087214 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 129.46/23.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 129.46/23.31 [W928 21:06:25.729099344 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 129.46/23.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 129.46/23.31 [W928 21:06:25.729128655 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 129.46/23.31 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 129.46/23.31 [W928 21:06:25.729139888 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 133.63/23.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 133.63/23.94 [W928 21:06:25.729164495 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 133.63/23.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 133.63/23.94 [W928 21:06:25.729174522 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 133.63/23.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 133.63/23.94 [W928 21:06:25.729200668 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 133.63/23.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 133.63/23.94 [W928 21:06:25.729217398 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 133.63/23.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 133.63/23.94 % (3020294)Instruction limit reached!
% 133.63/23.94 % (3020294)------------------------------
% 133.63/23.94 % (3020294)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 133.63/23.94 % (3020294)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 133.63/23.94 % (3020294)CaDiCaL version: 2.1.3
% 133.63/23.94 % (3020294)Termination reason: Instruction limit
% 133.63/23.94 % (3020294)Termination phase: Saturation
% 133.63/23.94 % (3020294)Time elapsed: 1.628 s
% 133.63/23.94 % (3020294)Peak memory usage: 237 MB
% 133.63/23.94 % (3020294)Instructions burned: 3372 (million)
% 133.63/23.94 % (3020301)dis-1010_1_ncem=casc2026/models/loop5.pt:sil=32000:npcc=on:fde=unused:sp=const_min:spb=goal_then_units:lcm=predicate:acc=on:flr=on:random_seed=1386286564:i=2503:nm=4:gsp=on:ss=axioms:sgt=15_2786 on theBenchmark for (2786ds/2503Mi)
% 133.63/23.94 [W928 21:06:26.103857558 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 133.63/23.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 133.63/23.94 [W928 21:06:26.103903702 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 133.63/23.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 133.63/23.94 [W928 21:06:26.103949189 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 133.63/23.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 133.63/23.94 [W928 21:06:26.103962362 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 133.63/23.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 133.63/23.94 [W928 21:06:26.103998453 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 133.63/23.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 133.63/23.94 [W928 21:06:26.104028703 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 133.63/23.94 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 133.63/23.94 [W928 21:06:26.104056096 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 141.80/25.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 141.80/25.11 [W928 21:06:26.104067206 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 141.80/25.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 141.80/25.11 [W928 21:06:26.104095450 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 141.80/25.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 141.80/25.11 [W928 21:06:26.104105733 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 141.80/25.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 141.80/25.11 [W928 21:06:26.104133327 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 141.80/25.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 141.80/25.11 [W928 21:06:26.104144314 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 141.80/25.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 141.80/25.11 % (3020278)Instruction limit reached!
% 141.80/25.11 % (3020278)------------------------------
% 141.80/25.11 % (3020278)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 141.80/25.11 % (3020278)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 141.80/25.11 % (3020278)CaDiCaL version: 2.1.3
% 141.80/25.11 % (3020278)Termination reason: Instruction limit
% 141.80/25.11 % (3020278)Termination phase: Saturation
% 141.80/25.11 % (3020278)Time elapsed: 4.488 s
% 141.80/25.11 % (3020278)Peak memory usage: 789 MB
% 141.80/25.11 % (3020278)Instructions burned: 6038 (million)
% 141.80/25.11 % (3020303)lrs+1011_1_ncem=casc2026/models/loop1.pt:sil=16000:npcc=on:sos=on:lsd=10:random_seed=999640968:i=2559:sd=1:ep=RSTC:ss=axioms_2780 on theBenchmark for (2780ds/2559Mi)
% 141.80/25.11 [W928 21:06:27.128312902 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 141.80/25.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 141.80/25.11 [W928 21:06:27.128357845 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 141.80/25.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 141.80/25.11 [W928 21:06:27.128403582 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 141.80/25.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 141.80/25.11 [W928 21:06:27.128416422 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 141.80/25.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 141.80/25.11 [W928 21:06:27.128442973 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 141.80/25.11 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 141.80/25.11 [W928 21:06:27.128454509 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 144.37/25.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 144.37/25.41 [W928 21:06:27.128481483 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 144.37/25.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 144.37/25.41 [W928 21:06:27.128491890 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 144.37/25.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 144.37/25.41 [W928 21:06:27.128516456 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 144.37/25.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 144.37/25.41 [W928 21:06:27.128537797 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 144.37/25.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 144.37/25.41 [W928 21:06:27.128565277 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 144.37/25.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 144.37/25.41 [W928 21:06:27.128575483 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 144.37/25.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 144.37/25.41 % (3020301)Instruction limit reached!
% 144.37/25.41 % (3020301)------------------------------
% 144.37/25.41 % (3020301)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 144.37/25.41 % (3020301)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 144.37/25.41 % (3020301)CaDiCaL version: 2.1.3
% 144.37/25.41 % (3020301)Termination reason: Instruction limit
% 144.37/25.41 % (3020301)Termination phase: Saturation
% 144.37/25.41 % (3020301)Time elapsed: 1.567 s
% 144.37/25.41 % (3020301)Peak memory usage: 350 MB
% 144.37/25.41 % (3020301)Instructions burned: 2506 (million)
% 144.37/25.41 % (3020305)ott+1_1_ncem=casc2026/models/loop8.pt:sil=64000:tgt=full:npcc=on:fdtod=off:random_seed=1418614268:i=30753:av=off:ss=included_2769 on theBenchmark for (2769ds/30753Mi)
% 144.37/25.41 [W928 21:06:27.756020557 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 144.37/25.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 144.37/25.41 [W928 21:06:27.756059444 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 144.37/25.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 144.37/25.41 [W928 21:06:27.756110951 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 144.37/25.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 144.37/25.41 [W928 21:06:27.756124234 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 144.37/25.41 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 144.37/25.41 [W928 21:06:27.756153345 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 154.02/26.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 154.02/26.98 [W928 21:06:27.756176638 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 154.02/26.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 154.02/26.98 [W928 21:06:27.756204882 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 154.02/26.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 154.02/26.98 [W928 21:06:27.756215585 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 154.02/26.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 154.02/26.98 [W928 21:06:27.756243292 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 154.02/26.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 154.02/26.98 [W928 21:06:27.756253682 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 154.02/26.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 154.02/26.98 [W928 21:06:27.756286286 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 154.02/26.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 154.02/26.98 [W928 21:06:27.756297232 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 154.02/26.98 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 154.02/26.98 % (3020297)Refutation not found, incomplete strategy
% 154.02/26.98 % (3020297)------------------------------
% 154.02/26.98 % (3020297)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.02/26.98 % (3020297)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.02/26.98 % (3020297)CaDiCaL version: 2.1.3
% 154.02/26.98 % (3020297)Termination reason: Refutation not found, incomplete strategy
% 154.02/26.98 % (3020297)Time elapsed: 2.913 s
% 154.02/26.98 % (3020297)Peak memory usage: 569 MB
% 154.02/26.98 % (3020297)Instructions burned: 4029 (million)
% 154.02/26.98 % (3020303)Instruction limit reached!
% 154.02/26.98 % (3020303)------------------------------
% 154.02/26.98 % (3020303)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 154.02/26.98 % (3020303)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 154.02/26.98 % (3020303)CaDiCaL version: 2.1.3
% 154.02/26.98 % (3020303)Termination reason: Instruction limit
% 154.02/26.98 % (3020303)Termination phase: Saturation
% 154.02/26.98 % (3020303)Time elapsed: 1.586 s
% 154.02/26.98 % (3020303)Peak memory usage: 350 MB
% 154.02/26.98 % (3020303)Instructions burned: 2561 (million)
% 154.02/26.98 % (3020297)------------------------------
% 154.02/26.98 % (3020297)------------------------------
% 154.02/26.98 % (3020307)lrs+10_1024_sil=64000:plsq=on:plsqc=4:plsqr=128,1:urr=on:plsql=on:br=off:random_seed=3372454459:i=26473:ep=RSTC_2762 on theBenchmark for (2762ds/26473Mi)
% 154.02/26.98 % (3020308)dis-1011_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:tgt=ground:npcc=on:sp=arity:sos=on:erd=off:rp=on:gs=on:kmz=on:random_seed=3071581146:cts=off:i=2759:kws=inv_arity:fgj=on_2762 on theBenchmark for (2762ds/2759Mi)
% 154.02/26.98 [W928 21:06:28.930646523 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 159.48/27.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 159.48/27.74 [W928 21:06:28.930681920 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 159.48/27.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 159.48/27.74 [W928 21:06:28.930736477 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 159.48/27.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 159.48/27.74 [W928 21:06:28.930803018 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 159.48/27.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 159.48/27.74 [W928 21:06:28.930840011 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 159.48/27.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 159.48/27.74 [W928 21:06:28.930851625 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 159.48/27.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 159.48/27.74 [W928 21:06:28.930878585 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 159.48/27.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 159.48/27.74 [W928 21:06:28.930889398 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 159.48/27.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 159.48/27.74 [W928 21:06:28.930915258 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 159.48/27.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 159.48/27.74 [W928 21:06:28.930926138 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 159.48/27.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 159.48/27.74 [W928 21:06:28.930953405 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 159.48/27.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 159.48/27.74 [W928 21:06:28.930964502 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 159.48/27.74 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 159.48/27.74 % (3020285)Instruction limit reached!
% 159.48/27.74 % (3020285)------------------------------
% 159.48/27.74 % (3020285)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 159.48/27.74 % (3020285)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 159.48/27.74 % (3020285)CaDiCaL version: 2.1.3
% 159.48/27.74 % (3020285)Termination reason: Instruction limit
% 159.48/27.74 % (3020285)Termination phase: Saturation
% 159.48/27.74 % (3020285)Time elapsed: 6.243 s
% 164.79/28.32 % (3020285)Peak memory usage: 1110 MB
% 164.79/28.32 % (3020285)Instructions burned: 8330 (million)
% 164.79/28.32 % (3020259)Instruction limit reached!
% 164.79/28.32 % (3020259)------------------------------
% 164.79/28.32 % (3020259)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 164.79/28.32 % (3020259)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 164.79/28.32 % (3020259)CaDiCaL version: 2.1.3
% 164.79/28.32 % (3020259)Termination reason: Instruction limit
% 164.79/28.32 % (3020259)Termination phase: Saturation
% 164.79/28.32 % (3020259)Time elapsed: 10.833 s
% 164.79/28.32 % (3020259)Peak memory usage: 1327 MB
% 164.79/28.32 % (3020259)Instructions burned: 14123 (million)
% 164.79/28.32 % (3020311)lrs-1011_1_anc=all_dependent:ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:fde=unused:sp=weighted_frequency:sos=all:spb=goal_then_units:urr=ec_only:sac=on:random_seed=4115009973:st=1.2:i=5665:sd=2:ep=RSTC:gsp=on:ss=axioms_2751 on theBenchmark for (2751ds/5665Mi)
% 164.79/28.32 % (3020312)dis+1011_1_anc=none:ncem=casc2026/models/loop3.pt:sil=16000:npcc=on:sos=on:lsd=20:urr=full:alpa=true:sac=on:random_seed=2026606055:i=1532:ep=RS:ss=axioms_2750 on theBenchmark for (2750ds/1532Mi)
% 164.79/28.32 % (3020308)Instruction limit reached!
% 164.79/28.32 % (3020308)------------------------------
% 164.79/28.32 % (3020308)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 164.79/28.32 % (3020308)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 164.79/28.32 % (3020308)CaDiCaL version: 2.1.3
% 164.79/28.32 % (3020308)Termination reason: Instruction limit
% 164.79/28.32 % (3020308)Termination phase: Property scanning
% 164.79/28.32 % (3020308)Time elapsed: 1.539 s
% 164.79/28.32 % (3020308)Peak memory usage: 227 MB
% 164.79/28.32 % (3020308)Instructions burned: 2759 (million)
% 164.79/28.32 % (3020315)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:erd=off:flr=on:newcnf=on:random_seed=2703569725:i=1565:sd=2:ss=axioms:sgt=32_2745 on theBenchmark for (2745ds/1565Mi)
% 164.79/28.32 % (3020312)Instruction limit reached!
% 164.79/28.32 % (3020312)------------------------------
% 164.79/28.32 % (3020312)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 164.79/28.32 % (3020312)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 164.79/28.32 % (3020312)CaDiCaL version: 2.1.3
% 164.79/28.32 % (3020312)Termination reason: Instruction limit
% 164.79/28.32 % (3020312)Termination phase: Saturation
% 164.79/28.32 % (3020312)Time elapsed: 0.838 s
% 164.79/28.32 % (3020312)Peak memory usage: 198 MB
% 164.79/28.32 % (3020312)Instructions burned: 1532 (million)
% 164.79/28.32 % (3020305)Refutation not found, incomplete strategy
% 164.79/28.32 % (3020305)------------------------------
% 164.79/28.32 % (3020305)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 164.79/28.32 % (3020305)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 164.79/28.32 % (3020305)CaDiCaL version: 2.1.3
% 164.79/28.32 % (3020305)Termination reason: Refutation not found, incomplete strategy
% 164.79/28.32 % (3020305)Time elapsed: 2.778 s
% 164.79/28.32 % (3020305)Peak memory usage: 530 MB
% 164.79/28.32 % (3020305)Instructions burned: 4016 (million)
% 164.79/28.32 % (3020317)lrs-1011_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=16000:npcc=on:sims=off:bsd=on:sp=unary_first:erd=off:spb=goal:lcm=reverse:gs=on:s2agt=8:random_seed=2090143023:i=1572:fgj=on:gsp=on_2740 on theBenchmark for (2740ds/1572Mi)
% 164.79/28.32 [W928 21:06:30.802503207 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 164.79/28.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 164.79/28.32 [W928 21:06:30.802536081 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 164.79/28.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 164.79/28.32 [W928 21:06:30.802583414 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 164.79/28.32 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 164.79/28.32 [W928 21:06:30.802596794 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 165.42/28.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 165.42/28.42 [W928 21:06:30.802623198 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 165.42/28.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 165.42/28.42 [W928 21:06:30.802644375 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 165.42/28.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 165.42/28.42 [W928 21:06:30.802671238 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 165.42/28.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 165.42/28.42 [W928 21:06:30.802681508 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 165.42/28.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 165.42/28.42 [W928 21:06:30.802704785 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 165.42/28.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 165.42/28.42 [W928 21:06:30.802714852 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 165.42/28.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 165.42/28.42 [W928 21:06:30.802746105 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 165.42/28.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 165.42/28.42 [W928 21:06:30.802756665 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 165.42/28.42 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 165.42/28.42 % (3020305)------------------------------
% 165.42/28.42 % (3020305)------------------------------
% 165.42/28.42 % (3020315)Instruction limit reached!
% 165.42/28.42 % (3020315)------------------------------
% 165.42/28.42 % (3020315)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 165.42/28.42 % (3020315)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.42/28.42 % (3020315)CaDiCaL version: 2.1.3
% 165.42/28.42 % (3020315)Termination reason: Instruction limit
% 165.42/28.42 % (3020315)Termination phase: Saturation
% 165.42/28.42 % (3020315)Time elapsed: 0.807 s
% 165.42/28.42 % (3020315)Peak memory usage: 199 MB
% 165.42/28.42 % (3020315)Instructions burned: 1566 (million)
% 165.42/28.42 % (3020319)lrs-1002_1_ncem=casc2026/models/loop8.pt:sil=64000:npcc=on:fde=none:sp=occurrence:sos=on:newcnf=on:random_seed=3804405737:i=6052:sd=4:ss=axioms:sgt=24_2736 on theBenchmark for (2736ds/6052Mi)
% 165.42/28.42 % (3020320)lrs+21_1_to=lpo:ncem=casc2026/models/loop2.pt:sil=16000:npcc=on:sp=arity:sos=on:erd=off:lcm=predicate:alpa=false:sac=on:random_seed=1537339140:i=3500:sd=1:bd=preordered:sup=off:ss=included_2735 on theBenchmark for (2735ds/3500Mi)
% 165.42/28.42 % (3020317)Instruction limit reached!
% 165.42/28.42 % (3020317)------------------------------
% 165.42/28.42 % (3020317)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 165.42/28.42 % (3020317)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 165.42/28.42 % (3020317)CaDiCaL version: 2.1.3
% 178.43/30.26 % (3020317)Termination reason: Instruction limit
% 178.43/30.26 % (3020317)Termination phase: Naming
% 178.43/30.26 % (3020317)Time elapsed: 0.988 s
% 178.43/30.26 % (3020317)Peak memory usage: 218 MB
% 178.43/30.26 % (3020317)Instructions burned: 1572 (million)
% 178.43/30.26 % (3020323)lrs+35_1_anc=all_dependent:ncem=casc2026/models/all5champsBiggishL14.pt:sil=32000:npcc=on:fde=none:sp=weighted_frequency:erd=off:spb=non_intro:updr=off:newcnf=on:random_seed=140598325:i=1842:sd=3:fgj=on:gtg=position:gsp=on:ss=axioms:sgt=20_2729 on theBenchmark for (2729ds/1842Mi)
% 178.43/30.26 % (3020299)Instruction limit reached!
% 178.43/30.26 % (3020299)------------------------------
% 178.43/30.26 % (3020299)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 178.43/30.26 % (3020299)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 178.43/30.26 % (3020299)CaDiCaL version: 2.1.3
% 178.43/30.26 % (3020299)Termination reason: Instruction limit
% 178.43/30.26 % (3020299)Termination phase: Saturation
% 178.43/30.26 % (3020299)Time elapsed: 6.253 s
% 178.43/30.26 % (3020299)Peak memory usage: 1267 MB
% 178.43/30.26 % (3020299)Instructions burned: 13495 (million)
% 178.43/30.26 % (3020325)lrs+11_1_anc=all_dependent:ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:bsr=unit_only:random_seed=2340546451:i=66096:add=on_2725 on theBenchmark for (2725ds/66096Mi)
% 178.43/30.26 [W928 21:06:32.135380620 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 178.43/30.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 178.43/30.26 [W928 21:06:32.135424240 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 178.43/30.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 178.43/30.26 [W928 21:06:32.135471494 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 178.43/30.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 178.43/30.26 [W928 21:06:32.135483884 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 178.43/30.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 178.43/30.26 [W928 21:06:32.135510418 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 178.43/30.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 178.43/30.26 [W928 21:06:32.135522291 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 178.43/30.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 178.43/30.26 [W928 21:06:32.135549411 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 178.43/30.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 178.43/30.26 [W928 21:06:32.135560725 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 178.43/30.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 178.43/30.26 [W928 21:06:32.135586625 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 178.43/30.26 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 178.43/30.26 [W928 21:06:32.135597875 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 194.67/32.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 194.67/32.57 [W928 21:06:32.135624915 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 194.67/32.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 194.67/32.57 [W928 21:06:32.135648195 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 194.67/32.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 194.67/32.57 [W928 21:06:32.237266619 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 194.67/32.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 194.67/32.57 [W928 21:06:32.237300999 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 194.67/32.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 194.67/32.57 [W928 21:06:32.237345606 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 194.67/32.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 194.67/32.57 [W928 21:06:32.237357927 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 194.67/32.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 194.67/32.57 [W928 21:06:32.237383637 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 194.67/32.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 194.67/32.57 [W928 21:06:32.237394807 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 194.67/32.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 194.67/32.57 [W928 21:06:32.237420914 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 194.67/32.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 194.67/32.57 [W928 21:06:32.237432587 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 194.67/32.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 194.67/32.57 [W928 21:06:32.237458027 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 194.67/32.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 194.67/32.57 [W928 21:06:32.237469791 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 194.67/32.57 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 194.67/32.57 [W928 21:06:32.237495617 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 202.59/33.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 202.59/33.61 [W928 21:06:32.237507241 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 202.59/33.61 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 202.59/33.61 % (3020311)Refutation not found, incomplete strategy
% 202.59/33.61 % (3020311)------------------------------
% 202.59/33.61 % (3020311)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 202.59/33.61 % (3020311)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.59/33.61 % (3020311)CaDiCaL version: 2.1.3
% 202.59/33.61 % (3020311)Termination reason: Refutation not found, incomplete strategy
% 202.59/33.61 % (3020311)Time elapsed: 2.832 s
% 202.59/33.61 % (3020311)Peak memory usage: 519 MB
% 202.59/33.61 % (3020311)Instructions burned: 4317 (million)
% 202.59/33.61 % (3020323)Instruction limit reached!
% 202.59/33.61 % (3020323)------------------------------
% 202.59/33.61 % (3020323)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 202.59/33.61 % (3020323)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.59/33.61 % (3020323)CaDiCaL version: 2.1.3
% 202.59/33.61 % (3020323)Termination reason: Instruction limit
% 202.59/33.61 % (3020323)Termination phase: SInE selection
% 202.59/33.61 % (3020323)Time elapsed: 0.753 s
% 202.59/33.61 % (3020323)Peak memory usage: 182 MB
% 202.59/33.61 % (3020323)Instructions burned: 1845 (million)
% 202.59/33.61 % (3020327)lrs+1011_1_to=lpo:ncem=casc2026/models/loop3.pt:sil=64000:npcc=on:random_seed=3935333388:i=1884:sd=1:nm=60:ss=axioms_2720 on theBenchmark for (2720ds/1884Mi)
% 202.59/33.61 % (3020311)------------------------------
% 202.59/33.61 % (3020311)------------------------------
% 202.59/33.61 % (3020329)lrs-1011_4:1_sil=16000:bsr=on:random_seed=209112365:cts=off:i=5469:bs=on:fsr=off_2717 on theBenchmark for (2717ds/5469Mi)
% 202.59/33.61 % (3020320)Instruction limit reached!
% 202.59/33.61 % (3020320)------------------------------
% 202.59/33.61 % (3020320)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 202.59/33.61 % (3020320)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.59/33.61 % (3020320)CaDiCaL version: 2.1.3
% 202.59/33.61 % (3020320)Termination reason: Instruction limit
% 202.59/33.61 % (3020320)Termination phase: Saturation
% 202.59/33.61 % (3020320)Time elapsed: 2.522 s
% 202.59/33.61 % (3020320)Peak memory usage: 549 MB
% 202.59/33.61 % (3020320)Instructions burned: 3500 (million)
% 202.59/33.61 % (3020327)Instruction limit reached!
% 202.59/33.61 % (3020327)------------------------------
% 202.59/33.61 % (3020327)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 202.59/33.61 % (3020327)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.59/33.61 % (3020327)CaDiCaL version: 2.1.3
% 202.59/33.61 % (3020327)Termination reason: Instruction limit
% 202.59/33.61 % (3020327)Termination phase: Saturation
% 202.59/33.61 % (3020327)Time elapsed: 1.046 s
% 202.59/33.61 % (3020327)Peak memory usage: 215 MB
% 202.59/33.61 % (3020327)Instructions burned: 1885 (million)
% 202.59/33.61 % (3020319)Refutation not found, incomplete strategy
% 202.59/33.61 % (3020319)------------------------------
% 202.59/33.61 % (3020319)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 202.59/33.61 % (3020319)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.59/33.61 % (3020319)CaDiCaL version: 2.1.3
% 202.59/33.61 % (3020319)Termination reason: Refutation not found, incomplete strategy
% 202.59/33.61 % (3020319)Time elapsed: 2.749 s
% 202.59/33.61 % (3020319)Peak memory usage: 550 MB
% 202.59/33.61 % (3020319)Instructions burned: 3873 (million)
% 202.59/33.61 % (3020331)lrs-1010_1_to=lpo:ncem=casc2026/models/loop8.pt:sil=64000:tgt=ground:npcc=on:sp=unary_frequency:urr=on:bce=on:alpa=false:sac=on:random_seed=1350550768:i=2037:s2at=10:gtgl=5:add=off:bd=preordered:ins=25:gtg=exists_all_2708 on theBenchmark for (2708ds/2037Mi)
% 202.59/33.61 % (3020332)lrs-30_1_ncem=casc2026/models/loop7.pt:sil=32000:npcc=on:urr=on:bce=on:rp=on:br=off:flr=on:random_seed=2737713426:st=-1:i=2110:kws=precedence:av=off:ss=axioms:er=known_2708 on theBenchmark for (2708ds/2110Mi)
% 202.59/33.61 % (3020319)------------------------------
% 202.59/33.61 % (3020319)------------------------------
% 202.59/33.69 % (3020335)dis-1010_1_anc=all_dependent:ncem=casc2026/models/loop5.pt:sil=32000:tgt=full:npcc=on:sp=unary_first:spb=goal:lcm=reverse:fd=off:flr=on:random_seed=1904976885:i=2430:add=off:aac=none:nm=16_2703 on theBenchmark for (2703ds/2430Mi)
% 202.59/33.69 % (3020331)Instruction limit reached!
% 202.59/33.69 % (3020331)------------------------------
% 202.59/33.69 % (3020331)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 202.59/33.69 % (3020331)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.59/33.69 % (3020331)CaDiCaL version: 2.1.3
% 202.59/33.69 % (3020331)Termination reason: Instruction limit
% 202.59/33.69 % (3020331)Termination phase: Property scanning
% 202.59/33.69 % (3020331)Time elapsed: 0.802 s
% 202.59/33.69 % (3020331)Peak memory usage: 182 MB
% 202.59/33.69 % (3020331)Instructions burned: 2038 (million)
% 202.59/33.69 % (3020337)lrs-1010_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:sp=unary_first:spb=units:acc=on:bsr=unit_only:gs=on:sac=on:random_seed=409160771:cond=fast:i=4891_2698 on theBenchmark for (2698ds/4891Mi)
% 202.59/33.69 % (3020332)Instruction limit reached!
% 202.59/33.69 % (3020332)------------------------------
% 202.59/33.69 % (3020332)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 202.59/33.69 % (3020332)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.59/33.69 % (3020332)CaDiCaL version: 2.1.3
% 202.59/33.69 % (3020332)Termination reason: Instruction limit
% 202.59/33.69 % (3020332)Termination phase: Unused predicate definition removal
% 202.59/33.69 % (3020332)Time elapsed: 1.102 s
% 202.59/33.69 % (3020332)Peak memory usage: 191 MB
% 202.59/33.69 % (3020332)Instructions burned: 2111 (million)
% 202.59/33.69 % (3020339)lrs+4_1_anc=all:ncem=casc2026/models/loop8.pt:sil=32000:tgt=full:npcc=on:sos=on:spb=goal_then_units:lcm=reverse:gs=on:s2agt=16:sac=on:newcnf=on:random_seed=189707916:st=2:i=14845:sd=2:ss=included:fsd=on_2695 on theBenchmark for (2695ds/14845Mi)
% 202.59/33.69 % (3020335)Instruction limit reached!
% 202.59/33.69 % (3020335)------------------------------
% 202.59/33.69 % (3020335)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 202.59/33.69 % (3020335)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.59/33.69 % (3020335)CaDiCaL version: 2.1.3
% 202.59/33.69 % (3020335)Termination reason: Instruction limit
% 202.59/33.69 % (3020335)Termination phase: Clausification
% 202.59/33.69 % (3020335)Time elapsed: 1.338 s
% 202.59/33.69 % (3020335)Peak memory usage: 218 MB
% 202.59/33.69 % (3020335)Instructions burned: 2430 (million)
% 202.59/33.69 % (3020341)lrs-1010_1_to=lpo:ncem=casc2026/models/loop4.pt:sil=32000:npcc=on:urr=ec_only:br=off:random_seed=3174230945:i=7534:sd=3:ins=1:gtg=exists_top:ss=included:sgt=8_2688 on theBenchmark for (2688ds/7534Mi)
% 202.59/33.69 % (3020329)Instruction limit reached!
% 202.59/33.69 % (3020329)------------------------------
% 202.59/33.69 % (3020329)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 202.59/33.69 % (3020329)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 202.59/33.69 % (3020329)CaDiCaL version: 2.1.3
% 202.59/33.69 % (3020329)Termination reason: Instruction limit
% 202.59/33.69 % (3020329)Termination phase: Saturation
% 202.59/33.69 % (3020329)Time elapsed: 3.337 s
% 202.59/33.69 % (3020329)Peak memory usage: 251 MB
% 202.59/33.69 % (3020329)Instructions burned: 5469 (million)
% 202.59/33.69 % (3020343)lrs-1002_1_ncem=casc2026/models/loop5.pt:sil=32000:tgt=ground:npcc=on:prc=on:fde=none:sims=off:spb=goal:bsr=unit_only:s2agt=32:random_seed=128672140:cond=fast:i=10353:bs=on:av=off:ss=axioms:fsd=on:sgt=64:fsdmm=10_2682 on theBenchmark for (2682ds/10353Mi)
% 202.59/33.69 [W928 21:06:36.392024677 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 202.59/33.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 202.59/33.69 [W928 21:06:36.392058331 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 202.59/33.69 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 202.59/33.69 [W928 21:06:36.392106565 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:36.392119741 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:36.392146122 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:36.392157278 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:36.392184225 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:36.392194995 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:36.392219502 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:36.392230399 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:36.392256799 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:36.392267502 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:37.427282713 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:37.427316847 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:37.427367197 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:37.427380841 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:37.427410281 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:37.427420627 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:37.427447134 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:37.427457098 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:37.427482358 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:37.427492451 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:37.427533778 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:37.427544562 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:37.508624751 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:37.508670218 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:37.508717929 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:37.508730692 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:37.508756216 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:37.508767992 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:37.508794546 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:37.508804543 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:37.508831023 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:37.508840940 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:37.508868630 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 [W928 21:06:37.508932514 register_special_ops.cpp:225] Warning: Creating a tensor from an empty intlist will create a tensor of default floating point type (currently Float) in python but a tensor of type int in torchscript.
% 197.92/34.96 Pass in a dtype argument to ensure consistent behavior (function createTensorFromList)
% 197.92/34.96 % (3020337)Instruction limit reached!
% 197.92/34.96 % (3020337)------------------------------
% 197.92/34.96 % (3020337)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 197.92/34.96 % (3020337)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.92/34.96 % (3020337)CaDiCaL version: 2.1.3
% 197.92/34.96 % (3020337)Termination reason: Instruction limit
% 197.92/34.96 % (3020337)Termination phase: Saturation
% 197.92/34.96 % (3020337)Time elapsed: 3.042 s
% 197.92/34.96 % (3020337)Peak memory usage: 431 MB
% 197.92/34.96 % (3020337)Instructions burned: 4891 (million)
% 197.92/34.96 % (3020339)Refutation not found, incomplete strategy
% 197.92/34.96 % (3020339)------------------------------
% 197.92/34.96 % (3020339)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 197.92/34.96 % (3020339)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 197.92/34.96 % (3020339)CaDiCaL version: 2.1.3
% 197.92/34.96 % (3020339)Termination reason: Refutation not found, incomplete strategy
% 197.92/34.96 % (3020339)Time elapsed: 2.864 s
% 197.92/34.96 % (3020339)Peak memory usage: 498 MB
% 197.92/34.96 % (3020339)Instructions burned: 4316 (million)
% 197.92/34.96 % (3020346)lrs+2_4096_sil=8000:plsq=on:plsqr=12672147,131072:sos=on:spb=goal:lcm=predicate:random_seed=4019119789:i=7860_2666 on theBenchmark for (2666ds/7860Mi)
% 197.92/34.96 % (3020167)First to succeed.
% 197.92/34.96 % (3020167)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-3020162"
% 197.92/34.96 % (3020339)------------------------------
% 197.92/34.96 % (3020339)------------------------------
% 197.92/34.96 % (3020348)ott+1011_1_anc=all_dependent:to=lpo:ncem=casc2026/models/loop5.pt:sil=8000:npcc=on:fde=unused:spb=goal:lsd=30:lcm=predicate:fd=off:gs=on:sac=on:random_seed=2178171253:i=7896:sd=2:bs=on:ss=included:sgt=20_2661 on theBenchmark for (2661ds/7896Mi)
% 197.92/34.96 % (3020167)Refutation found. Thanks to Tanya!
% 197.92/34.96 % SZS status Theorem for theBenchmark
% 197.92/34.96 % SZS output start Proof for theBenchmark
% See solution above
% 211.74/35.27 % (3020167)------------------------------
% 211.74/35.27 % (3020167)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 211.74/35.27 % (3020167)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 211.74/35.27 % (3020167)CaDiCaL version: 2.1.3
% 211.74/35.27 % (3020167)Termination reason: Refutation
% 211.74/35.27 % (3020167)Time elapsed: 28.533 s
% 211.74/35.27 % (3020167)Peak memory usage: 1582 MB
% 211.74/35.27 % (3020167)Instructions burned: 45131 (million)
% 211.74/35.27 % (3020167)------------------------------
% 211.74/35.27 % (3020167)------------------------------
% 211.74/35.27 % (3020162)Success in time 34.295 s
% 211.74/35.27 % Vampire exiting
%------------------------------------------------------------------------------