%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU387+1 : TPTP v8.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n022.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Jun 24 15:02:46 EDT 2024 % Result : Theorem 0.47s 0.66s % Output : CNFRefutation 0.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.05/0.09 % Problem : SEU387+1 : TPTP v8.2.0. Released v3.3.0. % 0.05/0.09 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.09/0.29 % Computer : n022.cluster.edu % 0.09/0.29 % Model : x86_64 x86_64 % 0.09/0.29 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.29 % Memory : 8042.1875MB % 0.09/0.29 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.29 % CPULimit : 300 % 0.09/0.29 % WCLimit : 300 % 0.09/0.29 % DateTime : Fri Jun 21 13:20:08 EDT 2024 % 0.09/0.29 % CPUTime : % 0.14/0.53 start to proof:theBenchmark % 0.47/0.64 %------------------------------------------- % 0.47/0.64 % File :CSE---1.7 % 0.47/0.64 % Problem :theBenchmark % 0.47/0.64 % Transform :cnf % 0.47/0.64 % Format :tptp:raw % 0.47/0.64 % Command :java -jar mcs_scs.jar %d %s % 0.47/0.64 % 0.47/0.64 % Result :Theorem 0.040000s % 0.47/0.64 % Output :CNFRefutation 0.040000s % 0.47/0.64 %------------------------------------------- % 0.47/0.64 %------------------------------------------------------------------------------ % 0.47/0.64 % File : SEU387+1 : TPTP v8.2.0. Released v3.3.0. % 0.47/0.64 % Domain : Set theory % 0.47/0.64 % Problem : MPTP bushy problem t2_yellow19 % 0.47/0.64 % Version : [Urb07] axioms : Especial. % 0.47/0.64 % English : % 0.47/0.64 % 0.47/0.64 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 0.47/0.64 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 0.47/0.64 % Source : [Urb07] % 0.47/0.64 % Names : bushy-t2_yellow19 [Urb07] % 0.47/0.64 % 0.47/0.64 % Status : Theorem % 0.47/0.64 % Rating : 0.28 v8.2.0, 0.25 v7.5.0, 0.28 v7.4.0, 0.17 v7.3.0, 0.21 v7.2.0, 0.17 v7.1.0, 0.22 v7.0.0, 0.20 v6.4.0, 0.27 v6.3.0, 0.17 v6.2.0, 0.24 v6.1.0, 0.33 v6.0.0, 0.17 v5.5.0, 0.30 v5.4.0, 0.36 v5.3.0, 0.41 v5.2.0, 0.30 v5.1.0, 0.29 v5.0.0, 0.33 v4.1.0, 0.35 v4.0.1, 0.39 v4.0.0, 0.42 v3.7.0, 0.45 v3.5.0, 0.47 v3.3.0 % 0.47/0.64 % Syntax : Number of formulae : 85 ( 15 unt; 0 def) % 0.47/0.64 % Number of atoms : 406 ( 7 equ) % 0.47/0.64 % Maximal formula atoms : 20 ( 4 avg) % 0.47/0.64 % Number of connectives : 397 ( 76 ~; 1 |; 255 &) % 0.47/0.64 % ( 3 <=>; 62 =>; 0 <=; 0 <~>) % 0.47/0.64 % Maximal formula depth : 21 ( 6 avg) % 0.47/0.64 % Maximal term depth : 4 ( 1 avg) % 0.47/0.64 % Number of predicates : 37 ( 35 usr; 1 prp; 0-3 aty) % 0.47/0.64 % Number of functors : 8 ( 8 usr; 1 con; 0-2 aty) % 0.47/0.64 % Number of variables : 117 ( 90 !; 27 ?) % 0.47/0.64 % SPC : FOF_THM_RFO_SEQ % 0.47/0.64 % 0.47/0.64 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 0.47/0.64 % library, www.mizar.org % 0.47/0.64 %------------------------------------------------------------------------------ % 0.47/0.64 fof(abstractness_v1_orders_2,axiom, % 0.47/0.64 ! [A] : % 0.47/0.64 ( rel_str(A) % 0.47/0.64 => ( strict_rel_str(A) % 0.47/0.64 => A = rel_str_of(the_carrier(A),the_InternalRel(A)) ) ) ). % 0.47/0.64 % 0.47/0.64 fof(antisymmetry_r2_hidden,axiom, % 0.47/0.64 ! [A,B] : % 0.47/0.64 ( in(A,B) % 0.47/0.64 => ~ in(B,A) ) ). % 0.47/0.64 % 0.47/0.64 fof(cc10_waybel_0,axiom, % 0.47/0.64 ! [A] : % 0.47/0.64 ( rel_str(A) % 0.47/0.64 => ( ( ~ empty_carrier(A) % 0.47/0.64 & reflexive_relstr(A) % 0.47/0.64 & complete_relstr(A) ) % 0.47/0.64 => ( ~ empty_carrier(A) % 0.47/0.64 & reflexive_relstr(A) % 0.47/0.64 & up_complete_relstr(A) % 0.47/0.64 & join_complete_relstr(A) ) ) ) ). % 0.47/0.64 % 0.47/0.64 fof(cc11_waybel_0,axiom, % 0.47/0.64 ! [A] : % 0.47/0.64 ( rel_str(A) % 0.47/0.64 => ( ( ~ empty_carrier(A) % 0.47/0.64 & reflexive_relstr(A) % 0.47/0.64 & join_complete_relstr(A) ) % 0.47/0.64 => ( ~ empty_carrier(A) % 0.47/0.64 & reflexive_relstr(A) % 0.47/0.64 & lower_bounded_relstr(A) ) ) ) ). % 0.47/0.64 % 0.47/0.64 fof(cc12_waybel_0,axiom, % 0.47/0.64 ! [A] : % 0.47/0.64 ( rel_str(A) % 0.47/0.64 => ( ( ~ empty_carrier(A) % 0.47/0.64 & reflexive_relstr(A) % 0.47/0.64 & transitive_relstr(A) % 0.47/0.64 & antisymmetric_relstr(A) % 0.47/0.64 & with_suprema_relstr(A) % 0.47/0.64 & lower_bounded_relstr(A) % 0.47/0.64 & up_complete_relstr(A) ) % 0.47/0.64 => ( ~ empty_carrier(A) % 0.47/0.64 & reflexive_relstr(A) % 0.47/0.64 & transitive_relstr(A) % 0.47/0.64 & antisymmetric_relstr(A) % 0.47/0.64 & with_suprema_relstr(A) % 0.47/0.64 & with_infima_relstr(A) % 0.47/0.64 & complete_relstr(A) % 0.47/0.64 & lower_bounded_relstr(A) % 0.47/0.64 & upper_bounded_relstr(A) % 0.47/0.64 & bounded_relstr(A) ) ) ) ). % 0.47/0.64 % 0.47/0.64 fof(cc13_waybel_0,axiom, % 0.47/0.64 ! [A] : % 0.47/0.64 ( rel_str(A) % 0.47/0.64 => ( ( ~ empty_carrier(A) % 0.47/0.64 & reflexive_relstr(A) % 0.47/0.64 & antisymmetric_relstr(A) % 0.47/0.64 & join_complete_relstr(A) ) % 0.47/0.64 => ( ~ empty_carrier(A) % 0.47/0.64 & reflexive_relstr(A) % 0.47/0.64 & antisymmetric_relstr(A) % 0.47/0.64 & with_infima_relstr(A) ) ) ) ). % 0.47/0.64 % 0.47/0.64 fof(cc14_waybel_0,axiom, % 0.47/0.64 ! [A] : % 0.47/0.64 ( rel_str(A) % 0.47/0.64 => ( ( ~ empty_carrier(A) % 0.47/0.64 & reflexive_relstr(A) % 0.47/0.64 & antisymmetric_relstr(A) % 0.47/0.64 & upper_bounded_relstr(A) % 0.47/0.64 & join_complete_relstr(A) ) % 0.47/0.64 => ( ~ empty_carrier(A) % 0.47/0.64 & reflexive_relstr(A) % 0.47/0.64 & antisymmetric_relstr(A) % 0.47/0.64 & with_suprema_relstr(A) % 0.47/0.64 & upper_bounded_relstr(A) ) ) ) ). % 0.47/0.64 % 0.47/0.64 fof(cc1_finset_1,axiom, % 0.47/0.64 ! [A] : % 0.47/0.64 ( empty(A) % 0.47/0.64 => finite(A) ) ). % 0.47/0.64 % 0.47/0.64 fof(cc1_lattice3,axiom, % 0.47/0.64 ! [A] : % 0.47/0.64 ( rel_str(A) % 0.47/0.64 => ( with_suprema_relstr(A) % 0.47/0.64 => ~ empty_carrier(A) ) ) ). % 0.47/0.64 % 0.47/0.64 fof(cc1_relat_1,axiom, % 0.47/0.64 ! [A] : % 0.47/0.64 ( empty(A) % 0.47/0.64 => relation(A) ) ). % 0.47/0.64 % 0.47/0.64 fof(cc1_relset_1,axiom, % 0.47/0.64 ! [A,B,C] : % 0.47/0.64 ( element(C,powerset(cartesian_product2(A,B))) % 0.47/0.64 => relation(C) ) ). % 0.47/0.64 % 0.47/0.64 fof(cc1_yellow_0,axiom, % 0.47/0.64 ! [A] : % 0.47/0.64 ( rel_str(A) % 0.47/0.64 => ( ( ~ empty_carrier(A) % 0.47/0.64 & complete_relstr(A) ) % 0.47/0.64 => ( ~ empty_carrier(A) % 0.47/0.64 & with_suprema_relstr(A) % 0.47/0.64 & with_infima_relstr(A) ) ) ) ). % 0.47/0.64 % 0.47/0.64 fof(cc2_finset_1,axiom, % 0.47/0.64 ! [A] : % 0.47/0.64 ( finite(A) % 0.47/0.64 => ! [B] : % 0.47/0.64 ( element(B,powerset(A)) % 0.47/0.64 => finite(B) ) ) ). % 0.47/0.64 % 0.47/0.64 fof(cc2_lattice3,axiom, % 0.47/0.64 ! [A] : % 0.47/0.64 ( rel_str(A) % 0.47/0.64 => ( with_infima_relstr(A) % 0.47/0.64 => ~ empty_carrier(A) ) ) ). % 0.47/0.64 % 0.47/0.64 fof(cc2_yellow_0,axiom, % 0.47/0.64 ! [A] : % 0.47/0.64 ( rel_str(A) % 0.47/0.64 => ( ( ~ empty_carrier(A) % 0.47/0.65 & reflexive_relstr(A) % 0.47/0.65 & trivial_carrier(A) ) % 0.47/0.65 => ( ~ empty_carrier(A) % 0.47/0.65 & reflexive_relstr(A) % 0.47/0.65 & transitive_relstr(A) % 0.47/0.65 & antisymmetric_relstr(A) % 0.47/0.65 & complete_relstr(A) ) ) ) ). % 0.47/0.65 % 0.47/0.65 fof(cc3_yellow_0,axiom, % 0.47/0.65 ! [A] : % 0.47/0.65 ( rel_str(A) % 0.47/0.65 => ( ( ~ empty_carrier(A) % 0.47/0.65 & complete_relstr(A) ) % 0.47/0.65 => ( ~ empty_carrier(A) % 0.47/0.65 & bounded_relstr(A) ) ) ) ). % 0.47/0.65 % 0.47/0.65 fof(cc4_yellow_0,axiom, % 0.47/0.65 ! [A] : % 0.47/0.65 ( rel_str(A) % 0.47/0.65 => ( bounded_relstr(A) % 0.47/0.65 => ( lower_bounded_relstr(A) % 0.47/0.65 & upper_bounded_relstr(A) ) ) ) ). % 0.47/0.65 % 0.47/0.65 fof(cc5_waybel_0,axiom, % 0.47/0.65 ! [A] : % 0.47/0.65 ( rel_str(A) % 0.47/0.65 => ( ( ~ empty_carrier(A) % 0.47/0.65 & reflexive_relstr(A) % 0.47/0.65 & trivial_carrier(A) ) % 0.47/0.65 => ( ~ empty_carrier(A) % 0.47/0.65 & reflexive_relstr(A) % 0.47/0.65 & connected_relstr(A) ) ) ) ). % 0.47/0.65 % 0.47/0.65 fof(cc5_yellow_0,axiom, % 0.47/0.65 ! [A] : % 0.47/0.65 ( rel_str(A) % 0.47/0.65 => ( ( lower_bounded_relstr(A) % 0.47/0.65 & upper_bounded_relstr(A) ) % 0.47/0.65 => bounded_relstr(A) ) ) ). % 0.47/0.65 % 0.47/0.65 fof(cc9_waybel_0,axiom, % 0.47/0.65 ! [A] : % 0.47/0.65 ( rel_str(A) % 0.47/0.65 => ( ( reflexive_relstr(A) % 0.47/0.65 & with_suprema_relstr(A) % 0.47/0.65 & up_complete_relstr(A) ) % 0.47/0.65 => ( ~ empty_carrier(A) % 0.47/0.65 & reflexive_relstr(A) % 0.47/0.65 & with_suprema_relstr(A) % 0.47/0.65 & upper_bounded_relstr(A) ) ) ) ). % 0.47/0.65 % 0.47/0.65 fof(dt_g1_orders_2,axiom, % 0.47/0.65 ! [A,B] : % 0.47/0.65 ( relation_of2(B,A,A) % 0.47/0.65 => ( strict_rel_str(rel_str_of(A,B)) % 0.47/0.65 & rel_str(rel_str_of(A,B)) ) ) ). % 0.47/0.65 % 0.47/0.65 fof(dt_k1_xboole_0,axiom, % 0.47/0.65 $true ). % 0.47/0.65 % 0.47/0.65 fof(dt_k1_zfmisc_1,axiom, % 0.47/0.65 $true ). % 0.47/0.65 % 0.47/0.65 fof(dt_k2_zfmisc_1,axiom, % 0.47/0.65 $true ). % 0.47/0.65 % 0.47/0.65 fof(dt_k3_yellow_0,axiom, % 0.47/0.65 ! [A] : % 0.47/0.65 ( rel_str(A) % 0.47/0.65 => element(bottom_of_relstr(A),the_carrier(A)) ) ). % 0.47/0.65 % 0.47/0.65 fof(dt_k3_yellow_1,axiom, % 0.47/0.65 ! [A] : % 0.47/0.65 ( strict_rel_str(boole_POSet(A)) % 0.47/0.65 & rel_str(boole_POSet(A)) ) ). % 0.47/0.65 % 0.47/0.65 fof(dt_l1_orders_2,axiom, % 0.47/0.65 ! [A] : % 0.47/0.65 ( rel_str(A) % 0.47/0.65 => one_sorted_str(A) ) ). % 0.47/0.65 % 0.47/0.65 fof(dt_l1_struct_0,axiom, % 0.47/0.65 $true ). % 0.47/0.65 % 0.47/0.65 fof(dt_m1_relset_1,axiom, % 0.47/0.65 $true ). % 0.47/0.65 % 0.47/0.65 fof(dt_m1_subset_1,axiom, % 0.47/0.65 $true ). % 0.47/0.65 % 0.47/0.65 fof(dt_m2_relset_1,axiom, % 0.47/0.65 ! [A,B,C] : % 0.47/0.65 ( relation_of2_as_subset(C,A,B) % 0.47/0.65 => element(C,powerset(cartesian_product2(A,B))) ) ). % 0.47/0.65 % 0.47/0.65 fof(dt_u1_orders_2,axiom, % 0.47/0.65 ! [A] : % 0.47/0.65 ( rel_str(A) % 0.47/0.65 => relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A)) ) ). % 0.47/0.65 % 0.47/0.65 fof(dt_u1_struct_0,axiom, % 0.47/0.65 $true ). % 0.47/0.65 % 0.47/0.65 fof(existence_l1_orders_2,axiom, % 0.47/0.65 ? [A] : rel_str(A) ). % 0.47/0.65 % 0.47/0.65 fof(existence_l1_struct_0,axiom, % 0.47/0.65 ? [A] : one_sorted_str(A) ). % 0.47/0.65 % 0.47/0.65 fof(existence_m1_relset_1,axiom, % 0.47/0.65 ! [A,B] : % 0.47/0.65 ? [C] : relation_of2(C,A,B) ). % 0.47/0.65 % 0.47/0.65 fof(existence_m1_subset_1,axiom, % 0.47/0.65 ! [A] : % 0.47/0.65 ? [B] : element(B,A) ). % 0.47/0.65 % 0.47/0.65 fof(existence_m2_relset_1,axiom, % 0.47/0.65 ! [A,B] : % 0.47/0.65 ? [C] : relation_of2_as_subset(C,A,B) ). % 0.47/0.65 % 0.47/0.65 fof(fc12_relat_1,axiom, % 0.47/0.65 ( empty(empty_set) % 0.47/0.65 & relation(empty_set) % 0.47/0.65 & relation_empty_yielding(empty_set) ) ). % 0.47/0.65 % 0.47/0.65 fof(fc14_finset_1,axiom, % 0.47/0.65 ! [A,B] : % 0.47/0.65 ( ( finite(A) % 0.47/0.65 & finite(B) ) % 0.47/0.65 => finite(cartesian_product2(A,B)) ) ). % 0.47/0.65 % 0.47/0.65 fof(fc1_struct_0,axiom, % 0.47/0.65 ! [A] : % 0.47/0.65 ( ( ~ empty_carrier(A) % 0.47/0.65 & one_sorted_str(A) ) % 0.47/0.65 => ~ empty(the_carrier(A)) ) ). % 0.47/0.65 % 0.47/0.65 fof(fc1_subset_1,axiom, % 0.47/0.65 ! [A] : ~ empty(powerset(A)) ). % 0.47/0.65 % 0.47/0.65 fof(fc1_waybel_7,axiom, % 0.47/0.65 ! [A] : % 0.47/0.65 ( ~ empty_carrier(boole_POSet(A)) % 0.47/0.65 & strict_rel_str(boole_POSet(A)) % 0.47/0.65 & reflexive_relstr(boole_POSet(A)) % 0.47/0.65 & transitive_relstr(boole_POSet(A)) % 0.47/0.65 & antisymmetric_relstr(boole_POSet(A)) % 0.47/0.65 & lower_bounded_relstr(boole_POSet(A)) % 0.47/0.65 & upper_bounded_relstr(boole_POSet(A)) % 0.47/0.65 & bounded_relstr(boole_POSet(A)) % 0.47/0.65 & up_complete_relstr(boole_POSet(A)) % 0.47/0.65 & join_complete_relstr(boole_POSet(A)) % 0.47/0.65 & ~ v1_yellow_3(boole_POSet(A)) % 0.47/0.65 & distributive_relstr(boole_POSet(A)) % 0.47/0.65 & heyting_relstr(boole_POSet(A)) % 0.47/0.65 & complemented_relstr(boole_POSet(A)) % 0.47/0.65 & boolean_relstr(boole_POSet(A)) % 0.47/0.65 & with_suprema_relstr(boole_POSet(A)) % 0.47/0.65 & with_infima_relstr(boole_POSet(A)) % 0.47/0.65 & complete_relstr(boole_POSet(A)) ) ). % 0.47/0.65 % 0.47/0.65 fof(fc2_waybel_7,axiom, % 0.47/0.65 ! [A] : % 0.47/0.65 ( ~ empty(A) % 0.47/0.65 => ( ~ empty_carrier(boole_POSet(A)) % 0.47/0.65 & ~ trivial_carrier(boole_POSet(A)) % 0.47/0.65 & strict_rel_str(boole_POSet(A)) % 0.47/0.65 & reflexive_relstr(boole_POSet(A)) % 0.47/0.65 & transitive_relstr(boole_POSet(A)) % 0.47/0.65 & antisymmetric_relstr(boole_POSet(A)) % 0.47/0.65 & lower_bounded_relstr(boole_POSet(A)) % 0.47/0.65 & upper_bounded_relstr(boole_POSet(A)) % 0.47/0.65 & bounded_relstr(boole_POSet(A)) % 0.47/0.65 & up_complete_relstr(boole_POSet(A)) % 0.47/0.65 & join_complete_relstr(boole_POSet(A)) % 0.47/0.65 & ~ v1_yellow_3(boole_POSet(A)) % 0.47/0.65 & distributive_relstr(boole_POSet(A)) % 0.47/0.65 & heyting_relstr(boole_POSet(A)) % 0.47/0.65 & complemented_relstr(boole_POSet(A)) % 0.47/0.65 & boolean_relstr(boole_POSet(A)) % 0.47/0.65 & with_suprema_relstr(boole_POSet(A)) % 0.47/0.65 & with_infima_relstr(boole_POSet(A)) % 0.47/0.65 & complete_relstr(boole_POSet(A)) ) ) ). % 0.47/0.65 % 0.47/0.65 fof(fc4_relat_1,axiom, % 0.47/0.65 ( empty(empty_set) % 0.47/0.65 & relation(empty_set) ) ). % 0.47/0.65 % 0.47/0.65 fof(fc4_subset_1,axiom, % 0.47/0.65 ! [A,B] : % 0.47/0.65 ( ( ~ empty(A) % 0.47/0.65 & ~ empty(B) ) % 0.47/0.65 => ~ empty(cartesian_product2(A,B)) ) ). % 0.47/0.65 % 0.47/0.65 fof(fc7_yellow_1,axiom, % 0.47/0.65 ! [A] : % 0.47/0.65 ( ~ empty_carrier(boole_POSet(A)) % 0.47/0.65 & strict_rel_str(boole_POSet(A)) % 0.47/0.65 & reflexive_relstr(boole_POSet(A)) % 0.47/0.65 & transitive_relstr(boole_POSet(A)) % 0.47/0.65 & antisymmetric_relstr(boole_POSet(A)) ) ). % 0.47/0.65 % 0.47/0.65 fof(fc8_yellow_1,axiom, % 0.47/0.65 ! [A] : % 0.47/0.65 ( ~ empty_carrier(boole_POSet(A)) % 0.47/0.65 & strict_rel_str(boole_POSet(A)) % 0.47/0.65 & reflexive_relstr(boole_POSet(A)) % 0.47/0.65 & transitive_relstr(boole_POSet(A)) % 0.47/0.65 & antisymmetric_relstr(boole_POSet(A)) % 0.47/0.65 & lower_bounded_relstr(boole_POSet(A)) % 0.47/0.65 & upper_bounded_relstr(boole_POSet(A)) % 0.47/0.65 & bounded_relstr(boole_POSet(A)) % 0.47/0.65 & with_suprema_relstr(boole_POSet(A)) % 0.47/0.65 & with_infima_relstr(boole_POSet(A)) % 0.47/0.65 & complete_relstr(boole_POSet(A)) ) ). % 0.47/0.65 % 0.47/0.65 fof(fc8_yellow_6,axiom, % 0.47/0.65 ! [A] : % 0.47/0.65 ( ~ empty_carrier(boole_POSet(A)) % 0.47/0.65 & strict_rel_str(boole_POSet(A)) % 0.47/0.65 & reflexive_relstr(boole_POSet(A)) % 0.47/0.65 & transitive_relstr(boole_POSet(A)) % 0.47/0.65 & antisymmetric_relstr(boole_POSet(A)) % 0.47/0.65 & lower_bounded_relstr(boole_POSet(A)) % 0.47/0.65 & upper_bounded_relstr(boole_POSet(A)) % 0.47/0.65 & bounded_relstr(boole_POSet(A)) % 0.47/0.65 & directed_relstr(boole_POSet(A)) % 0.47/0.65 & up_complete_relstr(boole_POSet(A)) % 0.47/0.65 & join_complete_relstr(boole_POSet(A)) % 0.47/0.65 & ~ v1_yellow_3(boole_POSet(A)) % 0.47/0.65 & with_suprema_relstr(boole_POSet(A)) % 0.47/0.65 & with_infima_relstr(boole_POSet(A)) % 0.47/0.65 & complete_relstr(boole_POSet(A)) ) ). % 0.47/0.65 % 0.47/0.65 fof(free_g1_orders_2,axiom, % 0.47/0.65 ! [A,B] : % 0.47/0.65 ( relation_of2(B,A,A) % 0.47/0.65 => ! [C,D] : % 0.47/0.65 ( rel_str_of(A,B) = rel_str_of(C,D) % 0.47/0.65 => ( A = C % 0.47/0.65 & B = D ) ) ) ). % 0.47/0.65 % 0.47/0.65 fof(rc10_waybel_0,axiom, % 0.47/0.65 ! [A] : % 0.47/0.65 ( ( ~ empty_carrier(A) % 0.47/0.65 & reflexive_relstr(A) % 0.47/0.65 & transitive_relstr(A) % 0.47/0.65 & rel_str(A) ) % 0.47/0.65 => ? [B] : % 0.47/0.65 ( element(B,powerset(the_carrier(A))) % 0.47/0.65 & ~ empty(B) % 0.47/0.65 & filtered_subset(B,A) % 0.47/0.65 & upper_relstr_subset(B,A) ) ) ). % 0.47/0.65 % 0.47/0.65 fof(rc12_waybel_0,axiom, % 0.47/0.65 ? [A] : % 0.47/0.65 ( rel_str(A) % 0.47/0.65 & ~ empty_carrier(A) % 0.47/0.65 & reflexive_relstr(A) % 0.47/0.65 & transitive_relstr(A) % 0.47/0.65 & antisymmetric_relstr(A) % 0.47/0.65 & connected_relstr(A) ) ). % 0.47/0.65 % 0.47/0.65 fof(rc13_waybel_0,axiom, % 0.47/0.65 ? [A] : % 0.47/0.65 ( rel_str(A) % 0.47/0.65 & ~ empty_carrier(A) % 0.47/0.65 & strict_rel_str(A) % 0.47/0.65 & reflexive_relstr(A) % 0.47/0.65 & transitive_relstr(A) % 0.47/0.65 & antisymmetric_relstr(A) % 0.47/0.65 & with_suprema_relstr(A) % 0.47/0.65 & with_infima_relstr(A) % 0.47/0.65 & complete_relstr(A) % 0.47/0.65 & lower_bounded_relstr(A) % 0.47/0.65 & upper_bounded_relstr(A) % 0.47/0.65 & bounded_relstr(A) % 0.47/0.65 & up_complete_relstr(A) % 0.47/0.65 & join_complete_relstr(A) ) ). % 0.47/0.65 % 0.47/0.65 fof(rc1_finset_1,axiom, % 0.47/0.65 ? [A] : % 0.47/0.65 ( ~ empty(A) % 0.47/0.65 & finite(A) ) ). % 0.47/0.65 % 0.47/0.65 fof(rc1_lattice3,axiom, % 0.47/0.65 ? [A] : % 0.47/0.65 ( rel_str(A) % 0.47/0.65 & ~ empty_carrier(A) % 0.47/0.65 & strict_rel_str(A) % 0.47/0.65 & reflexive_relstr(A) % 0.47/0.65 & transitive_relstr(A) % 0.47/0.65 & antisymmetric_relstr(A) % 0.47/0.65 & complete_relstr(A) ) ). % 0.47/0.65 % 0.47/0.65 fof(rc1_relat_1,axiom, % 0.47/0.65 ? [A] : % 0.47/0.65 ( empty(A) % 0.47/0.65 & relation(A) ) ). % 0.47/0.65 % 0.47/0.65 fof(rc1_subset_1,axiom, % 0.47/0.65 ! [A] : % 0.47/0.65 ( ~ empty(A) % 0.47/0.65 => ? [B] : % 0.47/0.65 ( element(B,powerset(A)) % 0.47/0.65 & ~ empty(B) ) ) ). % 0.47/0.65 % 0.47/0.65 fof(rc1_waybel_7,axiom, % 0.47/0.65 ? [A] : % 0.47/0.65 ( rel_str(A) % 0.47/0.65 & ~ empty_carrier(A) % 0.47/0.65 & ~ trivial_carrier(A) % 0.47/0.65 & strict_rel_str(A) % 0.47/0.65 & reflexive_relstr(A) % 0.47/0.65 & transitive_relstr(A) % 0.47/0.65 & antisymmetric_relstr(A) % 0.47/0.65 & lower_bounded_relstr(A) % 0.47/0.65 & upper_bounded_relstr(A) % 0.47/0.65 & bounded_relstr(A) % 0.47/0.65 & ~ v1_yellow_3(A) % 0.47/0.65 & distributive_relstr(A) % 0.47/0.65 & heyting_relstr(A) % 0.47/0.65 & complemented_relstr(A) % 0.47/0.65 & boolean_relstr(A) % 0.47/0.65 & with_suprema_relstr(A) % 0.47/0.65 & with_infima_relstr(A) ) ). % 0.47/0.65 % 0.47/0.65 fof(rc1_yellow_0,axiom, % 0.47/0.65 ? [A] : % 0.47/0.65 ( rel_str(A) % 0.47/0.65 & ~ empty_carrier(A) % 0.47/0.65 & strict_rel_str(A) % 0.47/0.65 & reflexive_relstr(A) % 0.47/0.65 & transitive_relstr(A) % 0.47/0.65 & antisymmetric_relstr(A) % 0.47/0.65 & with_suprema_relstr(A) % 0.47/0.65 & with_infima_relstr(A) % 0.47/0.65 & complete_relstr(A) % 0.47/0.65 & trivial_carrier(A) ) ). % 0.47/0.65 % 0.47/0.65 fof(rc2_lattice3,axiom, % 0.47/0.65 ? [A] : % 0.47/0.65 ( rel_str(A) % 0.47/0.65 & ~ empty_carrier(A) % 0.47/0.65 & strict_rel_str(A) % 0.47/0.65 & reflexive_relstr(A) % 0.47/0.65 & transitive_relstr(A) % 0.47/0.65 & antisymmetric_relstr(A) % 0.47/0.65 & with_suprema_relstr(A) % 0.47/0.65 & with_infima_relstr(A) % 0.47/0.65 & complete_relstr(A) ) ). % 0.47/0.65 % 0.47/0.65 fof(rc2_relat_1,axiom, % 0.47/0.65 ? [A] : % 0.47/0.65 ( ~ empty(A) % 0.47/0.65 & relation(A) ) ). % 0.47/0.65 % 0.47/0.65 fof(rc2_subset_1,axiom, % 0.47/0.65 ! [A] : % 0.47/0.65 ? [B] : % 0.47/0.65 ( element(B,powerset(A)) % 0.47/0.65 & empty(B) ) ). % 0.47/0.65 % 0.47/0.65 fof(rc2_waybel_7,axiom, % 0.47/0.65 ! [A] : % 0.47/0.65 ? [B] : % 0.47/0.65 ( element(B,powerset(powerset(A))) % 0.47/0.65 & ~ empty(B) % 0.47/0.65 & finite(B) ) ). % 0.47/0.65 % 0.47/0.65 fof(rc2_yellow_0,axiom, % 0.47/0.65 ? [A] : % 0.47/0.65 ( rel_str(A) % 0.47/0.65 & ~ empty_carrier(A) % 0.47/0.65 & reflexive_relstr(A) % 0.47/0.65 & transitive_relstr(A) % 0.47/0.65 & antisymmetric_relstr(A) % 0.47/0.65 & with_suprema_relstr(A) % 0.47/0.65 & with_infima_relstr(A) % 0.47/0.65 & complete_relstr(A) % 0.47/0.65 & lower_bounded_relstr(A) % 0.47/0.65 & upper_bounded_relstr(A) % 0.47/0.65 & bounded_relstr(A) ) ). % 0.47/0.65 % 0.47/0.65 fof(rc3_finset_1,axiom, % 0.47/0.65 ! [A] : % 0.47/0.65 ( ~ empty(A) % 0.47/0.65 => ? [B] : % 0.47/0.65 ( element(B,powerset(A)) % 0.47/0.65 & ~ empty(B) % 0.47/0.65 & finite(B) ) ) ). % 0.47/0.65 % 0.47/0.65 fof(rc3_relat_1,axiom, % 0.47/0.65 ? [A] : % 0.47/0.65 ( relation(A) % 0.47/0.65 & relation_empty_yielding(A) ) ). % 0.47/0.65 % 0.47/0.65 fof(rc3_struct_0,axiom, % 0.47/0.65 ? [A] : % 0.47/0.65 ( one_sorted_str(A) % 0.47/0.65 & ~ empty_carrier(A) ) ). % 0.47/0.65 % 0.47/0.65 fof(rc3_waybel_7,axiom, % 0.47/0.65 ! [A] : % 0.47/0.65 ( one_sorted_str(A) % 0.47/0.65 => ? [B] : % 0.47/0.65 ( element(B,powerset(powerset(the_carrier(A)))) % 0.47/0.65 & ~ empty(B) % 0.47/0.66 & finite(B) ) ) ). % 0.47/0.66 % 0.47/0.66 fof(rc4_finset_1,axiom, % 0.47/0.66 ! [A] : % 0.47/0.66 ( ~ empty(A) % 0.47/0.66 => ? [B] : % 0.47/0.66 ( element(B,powerset(A)) % 0.47/0.66 & ~ empty(B) % 0.47/0.66 & finite(B) ) ) ). % 0.47/0.66 % 0.47/0.66 fof(rc4_waybel_7,axiom, % 0.47/0.66 ! [A] : % 0.47/0.66 ( ( ~ empty_carrier(A) % 0.47/0.66 & ~ trivial_carrier(A) % 0.47/0.66 & reflexive_relstr(A) % 0.47/0.66 & transitive_relstr(A) % 0.47/0.66 & antisymmetric_relstr(A) % 0.47/0.66 & upper_bounded_relstr(A) % 0.47/0.66 & rel_str(A) ) % 0.47/0.66 => ? [B] : % 0.47/0.66 ( element(B,powerset(the_carrier(A))) % 0.47/0.66 & ~ empty(B) % 0.47/0.66 & proper_element(B,powerset(the_carrier(A))) % 0.47/0.66 & filtered_subset(B,A) % 0.47/0.66 & upper_relstr_subset(B,A) ) ) ). % 0.47/0.66 % 0.47/0.66 fof(rc4_yellow_6,axiom, % 0.47/0.66 ? [A] : % 0.47/0.66 ( rel_str(A) % 0.47/0.66 & ~ empty_carrier(A) % 0.47/0.66 & strict_rel_str(A) % 0.47/0.66 & transitive_relstr(A) % 0.47/0.66 & directed_relstr(A) ) ). % 0.47/0.66 % 0.47/0.66 fof(rc5_struct_0,axiom, % 0.47/0.66 ! [A] : % 0.47/0.66 ( ( ~ empty_carrier(A) % 0.47/0.66 & one_sorted_str(A) ) % 0.47/0.66 => ? [B] : % 0.47/0.66 ( element(B,powerset(the_carrier(A))) % 0.47/0.66 & ~ empty(B) ) ) ). % 0.47/0.66 % 0.47/0.66 fof(redefinition_m2_relset_1,axiom, % 0.47/0.66 ! [A,B,C] : % 0.47/0.66 ( relation_of2_as_subset(C,A,B) % 0.47/0.66 <=> relation_of2(C,A,B) ) ). % 0.47/0.66 % 0.47/0.66 fof(reflexivity_r1_tarski,axiom, % 0.47/0.66 ! [A,B] : subset(A,A) ). % 0.47/0.66 % 0.47/0.66 fof(t18_yellow_1,axiom, % 0.47/0.66 ! [A] : bottom_of_relstr(boole_POSet(A)) = empty_set ). % 0.47/0.66 % 0.47/0.66 fof(t1_subset,axiom, % 0.47/0.66 ! [A,B] : % 0.47/0.66 ( in(A,B) % 0.47/0.66 => element(A,B) ) ). % 0.47/0.66 % 0.47/0.66 fof(t2_subset,axiom, % 0.47/0.66 ! [A,B] : % 0.47/0.66 ( element(A,B) % 0.47/0.66 => ( empty(B) % 0.47/0.66 | in(A,B) ) ) ). % 0.47/0.66 % 0.47/0.66 fof(t2_yellow19,conjecture, % 0.47/0.66 ! [A] : % 0.47/0.66 ( ~ empty(A) % 0.47/0.66 => ! [B] : % 0.47/0.66 ( ( ~ empty(B) % 0.47/0.66 & filtered_subset(B,boole_POSet(A)) % 0.47/0.66 & upper_relstr_subset(B,boole_POSet(A)) % 0.47/0.66 & proper_element(B,powerset(the_carrier(boole_POSet(A)))) % 0.47/0.66 & element(B,powerset(the_carrier(boole_POSet(A)))) ) % 0.47/0.66 => ! [C] : % 0.47/0.66 ~ ( in(C,B) % 0.47/0.66 & empty(C) ) ) ) ). % 0.47/0.66 % 0.47/0.66 fof(t3_subset,axiom, % 0.47/0.66 ! [A,B] : % 0.47/0.66 ( element(A,powerset(B)) % 0.47/0.66 <=> subset(A,B) ) ). % 0.47/0.66 % 0.47/0.66 fof(t4_subset,axiom, % 0.47/0.66 ! [A,B,C] : % 0.47/0.66 ( ( in(A,B) % 0.47/0.66 & element(B,powerset(C)) ) % 0.47/0.66 => element(A,C) ) ). % 0.47/0.66 % 0.47/0.66 fof(t5_subset,axiom, % 0.47/0.66 ! [A,B,C] : % 0.47/0.66 ~ ( in(A,B) % 0.47/0.66 & element(B,powerset(C)) % 0.47/0.66 & empty(C) ) ). % 0.47/0.66 % 0.47/0.66 fof(t6_boole,axiom, % 0.47/0.66 ! [A] : % 0.47/0.66 ( empty(A) % 0.47/0.66 => A = empty_set ) ). % 0.47/0.66 % 0.47/0.66 fof(t7_boole,axiom, % 0.47/0.66 ! [A,B] : % 0.47/0.66 ~ ( in(A,B) % 0.47/0.66 & empty(B) ) ). % 0.47/0.66 % 0.47/0.66 fof(t8_boole,axiom, % 0.47/0.66 ! [A,B] : % 0.47/0.66 ~ ( empty(A) % 0.47/0.66 & A != B % 0.47/0.66 & empty(B) ) ). % 0.47/0.66 % 0.47/0.66 fof(t8_waybel_7,axiom, % 0.47/0.66 ! [A] : % 0.47/0.66 ( ( ~ empty_carrier(A) % 0.47/0.66 & reflexive_relstr(A) % 0.47/0.66 & transitive_relstr(A) % 0.47/0.66 & antisymmetric_relstr(A) % 0.47/0.66 & lower_bounded_relstr(A) % 0.47/0.66 & rel_str(A) ) % 0.47/0.66 => ! [B] : % 0.47/0.66 ( ( ~ empty(B) % 0.47/0.66 & filtered_subset(B,A) % 0.47/0.66 & upper_relstr_subset(B,A) % 0.47/0.66 & element(B,powerset(the_carrier(A))) ) % 0.47/0.66 => ( proper_element(B,powerset(the_carrier(A))) % 0.47/0.66 <=> ~ in(bottom_of_relstr(A),B) ) ) ) ). % 0.47/0.66 % 0.47/0.66 %------------------------------------------------------------------------------ % 0.47/0.66 %------------------------------------------- % 0.47/0.66 % Proof found % 0.47/0.66 % SZS status Theorem for theBenchmark % 0.47/0.66 % SZS output start Proof % 0.47/0.66 %ClaNum:331(EqnAxiom:71) % 0.47/0.66 %VarNum:409(SingletonVarNum:139) % 0.47/0.66 %MaxLitNum:12 % 0.47/0.66 %MaxfuncDepth:3 % 0.47/0.66 %SharedTerms:120 % 0.47/0.66 %goalClause: 138 204 206 207 211 212 226 227 % 0.47/0.66 %singleGoalClaCount:8 % 0.47/0.66 [72]P1(a1) % 0.47/0.66 [73]P1(a16) % 0.47/0.66 [74]P1(a33) % 0.47/0.66 [75]P1(a2) % 0.47/0.66 [76]P1(a7) % 0.47/0.66 [77]P1(a10) % 0.47/0.66 [78]P1(a11) % 0.47/0.66 [79]P1(a12) % 0.47/0.66 [80]P1(a17) % 0.47/0.66 [81]P22(a33) % 0.47/0.66 [82]P22(a2) % 0.47/0.66 [83]P22(a7) % 0.47/0.66 [84]P22(a10) % 0.47/0.66 [85]P22(a11) % 0.47/0.66 [86]P22(a17) % 0.47/0.66 [87]P2(a16) % 0.47/0.66 [88]P2(a33) % 0.47/0.66 [89]P2(a2) % 0.47/0.66 [90]P2(a7) % 0.47/0.66 [91]P2(a10) % 0.47/0.66 [92]P2(a11) % 0.47/0.66 [93]P2(a12) % 0.47/0.66 [94]P3(a33) % 0.47/0.66 [95]P3(a2) % 0.47/0.66 [96]P3(a10) % 0.47/0.66 [97]P3(a11) % 0.47/0.66 [98]P3(a12) % 0.47/0.66 [99]P27(a33) % 0.47/0.66 [100]P8(a33) % 0.47/0.66 [101]P19(a33) % 0.47/0.66 [102]P19(a7) % 0.47/0.66 [103]P19(a12) % 0.47/0.66 [104]P28(a16) % 0.47/0.66 [105]P28(a33) % 0.47/0.66 [106]P28(a2) % 0.47/0.66 [107]P28(a7) % 0.47/0.66 [108]P28(a10) % 0.47/0.66 [109]P28(a11) % 0.47/0.66 [110]P28(a12) % 0.47/0.66 [111]P28(a17) % 0.47/0.66 [112]P4(a16) % 0.47/0.66 [113]P4(a33) % 0.47/0.66 [114]P4(a2) % 0.47/0.66 [115]P4(a7) % 0.47/0.66 [116]P4(a10) % 0.47/0.66 [117]P4(a11) % 0.47/0.66 [118]P4(a12) % 0.47/0.66 [119]P31(a33) % 0.47/0.66 [120]P31(a7) % 0.47/0.66 [121]P31(a10) % 0.47/0.66 [122]P31(a11) % 0.47/0.66 [123]P31(a12) % 0.47/0.66 [124]P32(a33) % 0.47/0.66 [125]P32(a7) % 0.47/0.66 [126]P32(a10) % 0.47/0.66 [127]P32(a11) % 0.47/0.66 [128]P32(a12) % 0.47/0.66 [129]P33(a33) % 0.47/0.66 [130]P33(a7) % 0.47/0.66 [131]P33(a12) % 0.47/0.66 [132]P5(a33) % 0.47/0.66 [133]P5(a7) % 0.47/0.66 [134]P5(a12) % 0.47/0.66 [136]P9(a3) % 0.47/0.66 [137]P9(a8) % 0.47/0.66 [138]P9(a24) % 0.47/0.66 [139]P14(a34) % 0.47/0.66 [141]P23(a3) % 0.47/0.66 [142]P23(a8) % 0.47/0.66 [143]P23(a13) % 0.47/0.66 [144]P23(a18) % 0.47/0.66 [145]P30(a10) % 0.47/0.66 [146]P10(a16) % 0.47/0.66 [147]P20(a25) % 0.47/0.66 [148]P20(a20) % 0.47/0.66 [149]P24(a3) % 0.47/0.66 [150]P24(a18) % 0.47/0.66 [151]P11(a7) % 0.47/0.66 [152]P17(a7) % 0.47/0.66 [153]P7(a7) % 0.47/0.66 [154]P6(a7) % 0.47/0.66 [155]P12(a17) % 0.47/0.66 [204]P18(a24,a26) % 0.47/0.66 [215]~P16(a16) % 0.47/0.66 [216]~P16(a33) % 0.47/0.66 [217]~P16(a2) % 0.47/0.66 [218]~P16(a7) % 0.47/0.66 [219]~P16(a10) % 0.47/0.66 [220]~P16(a11) % 0.47/0.66 [221]~P16(a12) % 0.47/0.66 [222]~P16(a20) % 0.47/0.66 [223]~P16(a17) % 0.47/0.66 [224]~P9(a34) % 0.47/0.66 [225]~P9(a13) % 0.47/0.66 [226]~P9(a27) % 0.47/0.66 [227]~P9(a26) % 0.47/0.66 [228]~P30(a7) % 0.47/0.66 [229]~P35(a7) % 0.47/0.66 [206]P15(a26,f4(a27)) % 0.47/0.66 [207]P34(a26,f4(a27)) % 0.47/0.66 [211]P13(a26,f35(f36(f4(a27)))) % 0.47/0.66 [212]P21(a26,f35(f36(f4(a27)))) % 0.47/0.66 [205]P29(x2051,x2051) % 0.47/0.66 [157]P1(f4(x1571)) % 0.47/0.66 [162]P22(f4(x1621)) % 0.47/0.66 [166]P2(f4(x1661)) % 0.47/0.66 [169]P3(f4(x1691)) % 0.47/0.66 [171]P27(f4(x1711)) % 0.47/0.66 [173]P8(f4(x1731)) % 0.47/0.66 [176]P19(f4(x1761)) % 0.47/0.66 [180]P28(f4(x1801)) % 0.47/0.66 [184]P4(f4(x1841)) % 0.47/0.66 [187]P31(f4(x1871)) % 0.47/0.66 [190]P32(f4(x1901)) % 0.47/0.66 [193]P33(f4(x1931)) % 0.47/0.66 [196]P5(f4(x1961)) % 0.47/0.66 [197]P9(f14(x1971)) % 0.47/0.66 [198]P14(f15(x1981)) % 0.47/0.66 [199]P11(f4(x1991)) % 0.47/0.66 [200]P17(f4(x2001)) % 0.47/0.66 [201]P7(f4(x2011)) % 0.47/0.66 [202]P6(f4(x2021)) % 0.47/0.66 [203]P12(f4(x2031)) % 0.47/0.66 [208]P13(f29(x2081),x2081) % 0.47/0.66 [209]P13(f14(x2091),f35(x2091)) % 0.47/0.66 [233]~P16(f4(x2331)) % 0.47/0.66 [234]~P9(f35(x2341)) % 0.47/0.66 [235]~P9(f15(x2351)) % 0.47/0.66 [237]~P35(f4(x2371)) % 0.47/0.66 [156]E(f5(f4(x1561)),a3) % 0.47/0.66 [210]P13(f15(x2101),f35(f35(x2101))) % 0.47/0.66 [213]P25(f30(x2131,x2132),x2131,x2132) % 0.47/0.66 [214]P26(f31(x2141,x2142),x2141,x2142) % 0.47/0.66 [238]~P9(x2381)+E(x2381,a3) % 0.47/0.66 [239]~P9(x2391)+P14(x2391) % 0.47/0.66 [240]~P9(x2401)+P23(x2401) % 0.47/0.66 [241]~P1(x2411)+P20(x2411) % 0.47/0.66 [254]P9(x2541)+P14(f19(x2541)) % 0.47/0.66 [255]P9(x2551)+P14(f21(x2551)) % 0.47/0.66 [261]~P20(x2611)+P14(f22(x2611)) % 0.47/0.66 [265]P9(x2651)+~P9(f9(x2651)) % 0.47/0.66 [266]P9(x2661)+~P9(f19(x2661)) % 0.47/0.66 [267]P9(x2671)+~P9(f21(x2671)) % 0.47/0.66 [268]P9(x2681)+~P30(f4(x2681)) % 0.47/0.66 [275]~P20(x2751)+~P9(f22(x2751)) % 0.47/0.66 [287]P9(x2871)+P13(f9(x2871),f35(x2871)) % 0.47/0.66 [288]P9(x2881)+P13(f19(x2881),f35(x2881)) % 0.47/0.66 [289]P9(x2891)+P13(f21(x2891),f35(x2891)) % 0.47/0.66 [291]~P1(x2911)+P13(f5(x2911),f36(x2911)) % 0.47/0.66 [319]~P1(x3191)+P26(f37(x3191),f36(x3191),f36(x3191)) % 0.47/0.66 [318]~P20(x3181)+P13(f22(x3181),f35(f35(f36(x3181)))) % 0.47/0.66 [279]~P9(x2791)+~P18(x2792,x2791) % 0.47/0.66 [293]~P18(x2931,x2932)+P13(x2931,x2932) % 0.47/0.66 [302]~P18(x3022,x3021)+~P18(x3021,x3022) % 0.47/0.66 [298]~P29(x2981,x2982)+P13(x2981,f35(x2982)) % 0.47/0.66 [305]P29(x3051,x3052)+~P13(x3051,f35(x3052)) % 0.47/0.66 [322]~P25(x3222,x3221,x3221)+P1(f38(x3221,x3222)) % 0.47/0.66 [323]~P25(x3232,x3231,x3231)+P22(f38(x3231,x3232)) % 0.47/0.66 [327]~P26(x3271,x3272,x3273)+P25(x3271,x3272,x3273) % 0.47/0.66 [328]~P25(x3281,x3282,x3283)+P26(x3281,x3282,x3283) % 0.47/0.66 [324]P23(x3241)+~P13(x3241,f35(f6(x3242,x3243))) % 0.47/0.66 [329]~P26(x3291,x3292,x3293)+P13(x3291,f35(f6(x3292,x3293))) % 0.47/0.66 [262]~P1(x2621)+~P5(x2621)+P19(x2621) % 0.47/0.66 [263]~P1(x2631)+~P5(x2631)+P33(x2631) % 0.47/0.66 [270]~P16(x2701)+~P31(x2701)+~P1(x2701) % 0.47/0.66 [271]~P16(x2711)+~P32(x2711)+~P1(x2711) % 0.47/0.66 [277]~P20(x2771)+P16(x2771)+~P9(f36(x2771)) % 0.47/0.66 [278]~P20(x2781)+P16(x2781)+~P9(f28(x2781)) % 0.47/0.66 [296]~P1(x2961)+~P22(x2961)+E(f38(f36(x2961),f37(x2961)),x2961) % 0.47/0.66 [306]~P20(x3061)+P16(x3061)+P13(f28(x3061),f35(f36(x3061))) % 0.47/0.66 [260]~P9(x2602)+~P9(x2601)+E(x2601,x2602) % 0.47/0.66 [295]~P13(x2952,x2951)+P9(x2951)+P18(x2952,x2951) % 0.47/0.66 [299]P14(x2991)+~P14(x2992)+~P13(x2991,f35(x2992)) % 0.47/0.66 [300]~P14(x3002)+~P14(x3001)+P14(f6(x3001,x3002)) % 0.47/0.66 [307]P9(x3071)+P9(x3072)+~P9(f6(x3072,x3071)) % 0.47/0.66 [313]~P9(x3131)+~P18(x3132,x3133)+~P13(x3133,f35(x3131)) % 0.47/0.66 [317]P13(x3171,x3172)+~P18(x3171,x3173)+~P13(x3173,f35(x3172)) % 0.47/0.66 [325]~P25(x3251,x3253,x3253)+E(x3251,x3252)+~E(f38(x3253,x3251),f38(x3254,x3252)) % 0.47/0.66 [326]~P25(x3263,x3261,x3261)+E(x3261,x3262)+~E(f38(x3261,x3263),f38(x3262,x3264)) % 0.47/0.66 [272]P31(x2721)+~P1(x2721)+~P3(x2721)+P16(x2721) % 0.47/0.66 [273]P32(x2731)+~P1(x2731)+~P3(x2731)+P16(x2731) % 0.47/0.66 [274]P5(x2741)+~P1(x2741)+~P3(x2741)+P16(x2741) % 0.47/0.66 [276]~P1(x2761)+~P19(x2761)+~P33(x2761)+P5(x2761) % 0.47/0.66 [280]P3(x2801)+~P1(x2801)+~P2(x2801)+~P30(x2801)+P16(x2801) % 0.47/0.66 [281]P27(x2811)+~P1(x2811)+~P2(x2811)+~P3(x2811)+P16(x2811) % 0.47/0.66 [282]P8(x2821)+~P1(x2821)+~P2(x2821)+~P3(x2821)+P16(x2821) % 0.47/0.66 [283]P19(x2831)+~P1(x2831)+~P2(x2831)+~P8(x2831)+P16(x2831) % 0.47/0.66 [284]P28(x2841)+~P1(x2841)+~P2(x2841)+~P30(x2841)+P16(x2841) % 0.47/0.66 [285]P4(x2851)+~P1(x2851)+~P2(x2851)+~P30(x2851)+P16(x2851) % 0.47/0.66 [286]P10(x2861)+~P1(x2861)+~P2(x2861)+~P30(x2861)+P16(x2861) % 0.47/0.66 [290]~P1(x2901)+~P2(x2901)+~P27(x2901)+~P31(x2901)+P33(x2901) % 0.47/0.66 [297]~P1(x2971)+~P2(x2971)+~P28(x2971)+P16(x2971)+~P9(f32(x2971)) % 0.47/0.66 [303]~P1(x3031)+~P2(x3031)+~P28(x3031)+P16(x3031)+P15(f32(x3031),x3031) % 0.47/0.66 [304]~P1(x3041)+~P2(x3041)+~P28(x3041)+P16(x3041)+P34(f32(x3041),x3041) % 0.47/0.66 [314]~P1(x3141)+~P2(x3141)+~P28(x3141)+P16(x3141)+P13(f32(x3141),f35(f36(x3141))) % 0.47/0.66 [294]P32(x2941)+~P1(x2941)+~P2(x2941)+~P8(x2941)+~P4(x2941)+P16(x2941) % 0.47/0.66 [301]P31(x3011)+~P1(x3011)+~P2(x3011)+~P8(x3011)+~P4(x3011)+~P33(x3011)+P16(x3011) % 0.47/0.66 [312]P30(x3121)+~P1(x3121)+~P2(x3121)+~P28(x3121)+~P4(x3121)+~P33(x3121)+P16(x3121)+~P9(f23(x3121)) % 0.47/0.66 [315]P30(x3151)+~P1(x3151)+~P2(x3151)+~P28(x3151)+~P4(x3151)+~P33(x3151)+P16(x3151)+P15(f23(x3151),x3151) % 0.47/0.66 [316]P30(x3161)+~P1(x3161)+~P2(x3161)+~P28(x3161)+~P4(x3161)+~P33(x3161)+P16(x3161)+P34(f23(x3161),x3161) % 0.47/0.66 [320]P30(x3201)+~P1(x3201)+~P2(x3201)+~P28(x3201)+~P4(x3201)+~P33(x3201)+P16(x3201)+P13(f23(x3201),f35(f36(x3201))) % 0.47/0.66 [321]P30(x3211)+~P1(x3211)+~P2(x3211)+~P28(x3211)+~P4(x3211)+~P33(x3211)+P16(x3211)+P21(f23(x3211),f35(f36(x3211))) % 0.47/0.66 [308]P3(x3081)+~P1(x3081)+~P2(x3081)+~P27(x3081)+~P19(x3081)+~P28(x3081)+~P4(x3081)+~P31(x3081)+P16(x3081) % 0.47/0.66 [309]P32(x3091)+~P1(x3091)+~P2(x3091)+~P27(x3091)+~P19(x3091)+~P28(x3091)+~P4(x3091)+~P31(x3091)+P16(x3091) % 0.47/0.66 [311]P5(x3111)+~P1(x3111)+~P2(x3111)+~P27(x3111)+~P19(x3111)+~P28(x3111)+~P4(x3111)+~P31(x3111)+P16(x3111) % 0.47/0.66 [330]~P1(x3301)+~P2(x3301)+~P19(x3301)+~P28(x3301)+~P4(x3301)+~P15(x3302,x3301)+~P34(x3302,x3301)+P16(x3301)+P9(x3302)+P18(f5(x3301),x3302)+P21(x3302,f35(f36(x3301)))+~P13(x3302,f35(f36(x3301))) % 0.47/0.66 [331]~P1(x3311)+~P2(x3311)+~P19(x3311)+~P28(x3311)+~P4(x3311)+~P15(x3312,x3311)+~P34(x3312,x3311)+P16(x3311)+P9(x3312)+~P18(f5(x3311),x3312)+~P13(x3312,f35(f36(x3311)))+~P21(x3312,f35(f36(x3311))) % 0.47/0.66 %EqnAxiom % 0.47/0.66 [1]E(x11,x11) % 0.47/0.66 [2]E(x22,x21)+~E(x21,x22) % 0.47/0.66 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 0.47/0.66 [4]~E(x41,x42)+E(f4(x41),f4(x42)) % 0.47/0.66 [5]~E(x51,x52)+E(f5(x51),f5(x52)) % 0.47/0.66 [6]~E(x61,x62)+E(f35(x61),f35(x62)) % 0.47/0.66 [7]~E(x71,x72)+E(f36(x71),f36(x72)) % 0.47/0.66 [8]~E(x81,x82)+E(f21(x81),f21(x82)) % 0.47/0.66 [9]~E(x91,x92)+E(f6(x91,x93),f6(x92,x93)) % 0.47/0.66 [10]~E(x101,x102)+E(f6(x103,x101),f6(x103,x102)) % 0.47/0.66 [11]~E(x111,x112)+E(f22(x111),f22(x112)) % 0.47/0.66 [12]~E(x121,x122)+E(f19(x121),f19(x122)) % 0.47/0.66 [13]~E(x131,x132)+E(f30(x131,x133),f30(x132,x133)) % 0.47/0.66 [14]~E(x141,x142)+E(f30(x143,x141),f30(x143,x142)) % 0.47/0.66 [15]~E(x151,x152)+E(f37(x151),f37(x152)) % 0.47/0.66 [16]~E(x161,x162)+E(f32(x161),f32(x162)) % 0.47/0.66 [17]~E(x171,x172)+E(f9(x171),f9(x172)) % 0.47/0.66 [18]~E(x181,x182)+E(f28(x181),f28(x182)) % 0.47/0.66 [19]~E(x191,x192)+E(f23(x191),f23(x192)) % 0.47/0.66 [20]~E(x201,x202)+E(f38(x201,x203),f38(x202,x203)) % 0.47/0.66 [21]~E(x211,x212)+E(f38(x213,x211),f38(x213,x212)) % 0.47/0.66 [22]~E(x221,x222)+E(f15(x221),f15(x222)) % 0.47/0.66 [23]~E(x231,x232)+E(f29(x231),f29(x232)) % 0.47/0.66 [24]~E(x241,x242)+E(f14(x241),f14(x242)) % 0.47/0.66 [25]~E(x251,x252)+E(f31(x251,x253),f31(x252,x253)) % 0.47/0.66 [26]~E(x261,x262)+E(f31(x263,x261),f31(x263,x262)) % 0.47/0.66 [27]~P1(x271)+P1(x272)+~E(x271,x272) % 0.47/0.66 [28]P21(x282,x283)+~E(x281,x282)+~P21(x281,x283) % 0.47/0.66 [29]P21(x293,x292)+~E(x291,x292)+~P21(x293,x291) % 0.47/0.66 [30]P13(x302,x303)+~E(x301,x302)+~P13(x301,x303) % 0.47/0.66 [31]P13(x313,x312)+~E(x311,x312)+~P13(x313,x311) % 0.47/0.66 [32]P18(x322,x323)+~E(x321,x322)+~P18(x321,x323) % 0.47/0.67 [33]P18(x333,x332)+~E(x331,x332)+~P18(x333,x331) % 0.47/0.67 [34]P34(x342,x343)+~E(x341,x342)+~P34(x341,x343) % 0.47/0.67 [35]P34(x353,x352)+~E(x351,x352)+~P34(x353,x351) % 0.47/0.67 [36]P15(x362,x363)+~E(x361,x362)+~P15(x361,x363) % 0.47/0.67 [37]P15(x373,x372)+~E(x371,x372)+~P15(x373,x371) % 0.47/0.67 [38]~P4(x381)+P4(x382)+~E(x381,x382) % 0.47/0.67 [39]~P28(x391)+P28(x392)+~E(x391,x392) % 0.47/0.67 [40]~P19(x401)+P19(x402)+~E(x401,x402) % 0.47/0.67 [41]~P22(x411)+P22(x412)+~E(x411,x412) % 0.47/0.67 [42]~P33(x421)+P33(x422)+~E(x421,x422) % 0.47/0.67 [43]~P14(x431)+P14(x432)+~E(x431,x432) % 0.47/0.67 [44]~P2(x441)+P2(x442)+~E(x441,x442) % 0.47/0.67 [45]P29(x452,x453)+~E(x451,x452)+~P29(x451,x453) % 0.47/0.67 [46]P29(x463,x462)+~E(x461,x462)+~P29(x463,x461) % 0.47/0.67 [47]~P16(x471)+P16(x472)+~E(x471,x472) % 0.47/0.67 [48]~P9(x481)+P9(x482)+~E(x481,x482) % 0.47/0.67 [49]~P30(x491)+P30(x492)+~E(x491,x492) % 0.47/0.67 [50]P25(x502,x503,x504)+~E(x501,x502)+~P25(x501,x503,x504) % 0.47/0.67 [51]P25(x513,x512,x514)+~E(x511,x512)+~P25(x513,x511,x514) % 0.47/0.67 [52]P25(x523,x524,x522)+~E(x521,x522)+~P25(x523,x524,x521) % 0.47/0.67 [53]~P10(x531)+P10(x532)+~E(x531,x532) % 0.47/0.67 [54]~P5(x541)+P5(x542)+~E(x541,x542) % 0.47/0.67 [55]~P35(x551)+P35(x552)+~E(x551,x552) % 0.47/0.67 [56]~P31(x561)+P31(x562)+~E(x561,x562) % 0.47/0.67 [57]~P3(x571)+P3(x572)+~E(x571,x572) % 0.47/0.67 [58]~P32(x581)+P32(x582)+~E(x581,x582) % 0.47/0.67 [59]~P23(x591)+P23(x592)+~E(x591,x592) % 0.47/0.67 [60]~P8(x601)+P8(x602)+~E(x601,x602) % 0.47/0.67 [61]~P12(x611)+P12(x612)+~E(x611,x612) % 0.47/0.67 [62]~P27(x621)+P27(x622)+~E(x621,x622) % 0.47/0.67 [63]P26(x632,x633,x634)+~E(x631,x632)+~P26(x631,x633,x634) % 0.47/0.67 [64]P26(x643,x642,x644)+~E(x641,x642)+~P26(x643,x641,x644) % 0.47/0.67 [65]P26(x653,x654,x652)+~E(x651,x652)+~P26(x653,x654,x651) % 0.47/0.67 [66]~P11(x661)+P11(x662)+~E(x661,x662) % 0.47/0.67 [67]~P20(x671)+P20(x672)+~E(x671,x672) % 0.47/0.67 [68]~P24(x681)+P24(x682)+~E(x681,x682) % 0.47/0.67 [69]~P7(x691)+P7(x692)+~E(x691,x692) % 0.47/0.67 [70]~P17(x701)+P17(x702)+~E(x701,x702) % 0.47/0.67 [71]~P6(x711)+P6(x712)+~E(x711,x712) % 0.47/0.67 % 0.47/0.67 %------------------------------------------- % 0.47/0.67 cnf(340,plain, % 0.47/0.67 (P13(f29(x3401),x3401)), % 0.47/0.67 inference(rename_variables,[],[208])). % 0.47/0.67 cnf(343,plain, % 0.47/0.67 (P13(f29(x3431),x3431)), % 0.47/0.67 inference(rename_variables,[],[208])). % 0.47/0.67 cnf(346,plain, % 0.47/0.67 (P13(f29(x3461),x3461)), % 0.47/0.67 inference(rename_variables,[],[208])). % 0.47/0.67 cnf(355,plain, % 0.47/0.67 (P9(f5(f4(x3551)))), % 0.47/0.67 inference(scs_inference,[],[138,204,226,211,136,208,340,343,346,139,156,279,305,2,324,295,299,313,317,31,33,48])). % 0.47/0.67 cnf(357,plain, % 0.47/0.67 (P29(x3571,x3571)), % 0.47/0.67 inference(rename_variables,[],[205])). % 0.47/0.67 cnf(361,plain, % 0.47/0.67 (P25(f30(x3611,x3612),x3611,x3612)), % 0.47/0.67 inference(rename_variables,[],[213])). % 0.47/0.67 cnf(366,plain, % 0.47/0.67 (P26(f31(x3661,x3662),x3661,x3662)), % 0.47/0.67 inference(rename_variables,[],[214])). % 0.47/0.67 cnf(398,plain, % 0.47/0.67 (~E(a24,a3)), % 0.47/0.67 inference(scs_inference,[],[138,204,226,227,206,207,211,212,136,205,357,213,361,214,366,208,340,343,346,75,77,89,91,95,139,141,145,149,217,219,157,166,176,180,184,233,156,279,305,2,324,295,299,313,317,31,33,48,45,46,51,52,59,64,65,68,272,273,274,281,282,283,286,290,331,302,28,32,3])). % 0.47/0.67 cnf(413,plain, % 0.47/0.67 ($false), % 0.47/0.67 inference(scs_inference,[],[138,355,398,279,238]), % 0.47/0.67 ['proof']). % 0.47/0.67 % SZS output end Proof % 0.47/0.67 % Total time :0.040000s %------------------------------------------------------------------------------