%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU373+1 : TPTP v8.2.0. Released v3.3.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n027.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:42 EDT 2024 % Result : Theorem 20.14s 20.21s % Output : CNFRefutation 20.14s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SEU373+1 : TPTP v8.2.0. Released v3.3.0. % 0.00/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n027.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Fri Jun 21 16:07:23 EDT 2024 % 0.12/0.33 % CPUTime : % 0.18/0.56 start to proof:theBenchmark % 20.14/20.19 %------------------------------------------- % 20.14/20.19 % File :CSE---1.7 % 20.14/20.19 % Problem :theBenchmark % 20.14/20.19 % Transform :cnf % 20.14/20.19 % Format :tptp:raw % 20.14/20.19 % Command :java -jar mcs_scs.jar %d %s % 20.14/20.19 % 20.14/20.19 % Result :Theorem 19.600000s % 20.14/20.19 % Output :CNFRefutation 19.600000s % 20.14/20.19 %------------------------------------------- % 20.14/20.20 %------------------------------------------------------------------------------ % 20.14/20.20 % File : SEU373+1 : TPTP v8.2.0. Released v3.3.0. % 20.14/20.20 % Domain : Set theory % 20.14/20.20 % Problem : MPTP bushy problem t19_yellow_6 % 20.14/20.20 % Version : [Urb07] axioms : Especial. % 20.14/20.20 % English : % 20.14/20.20 % 20.14/20.20 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 20.14/20.20 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 20.14/20.20 % Source : [Urb07] % 20.14/20.20 % Names : bushy-t19_yellow_6 [Urb07] % 20.14/20.20 % 20.14/20.20 % Status : Theorem % 20.14/20.20 % Rating : 0.17 v8.2.0, 0.14 v8.1.0, 0.06 v7.4.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.07 v6.4.0, 0.12 v6.3.0, 0.08 v6.1.0, 0.13 v5.5.0, 0.11 v5.4.0, 0.14 v5.3.0, 0.19 v5.2.0, 0.05 v5.1.0, 0.10 v5.0.0, 0.12 v4.1.0, 0.13 v4.0.0, 0.17 v3.7.0, 0.05 v3.4.0, 0.16 v3.3.0 % 20.14/20.20 % Syntax : Number of formulae : 59 ( 14 unt; 0 def) % 20.14/20.20 % Number of atoms : 140 ( 4 equ) % 20.14/20.20 % Maximal formula atoms : 6 ( 2 avg) % 20.14/20.20 % Number of connectives : 93 ( 12 ~; 1 |; 39 &) % 20.14/20.20 % ( 4 <=>; 37 =>; 0 <=; 0 <~>) % 20.14/20.20 % Maximal formula depth : 9 ( 4 avg) % 20.14/20.20 % Maximal term depth : 3 ( 1 avg) % 20.14/20.20 % Number of predicates : 18 ( 16 usr; 1 prp; 0-3 aty) % 20.14/20.20 % Number of functors : 8 ( 8 usr; 1 con; 0-4 aty) % 20.14/20.20 % Number of variables : 98 ( 80 !; 18 ?) % 20.14/20.20 % SPC : FOF_THM_RFO_SEQ % 20.14/20.20 % 20.14/20.20 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 20.14/20.20 % library, www.mizar.org % 20.14/20.20 %------------------------------------------------------------------------------ % 20.14/20.20 fof(antisymmetry_r2_hidden,axiom, % 20.14/20.20 ! [A,B] : % 20.14/20.20 ( in(A,B) % 20.14/20.20 => ~ in(B,A) ) ). % 20.14/20.20 % 20.14/20.20 fof(cc1_funct_1,axiom, % 20.14/20.20 ! [A] : % 20.14/20.20 ( empty(A) % 20.14/20.20 => function(A) ) ). % 20.14/20.20 % 20.14/20.20 fof(cc1_relat_1,axiom, % 20.14/20.20 ! [A] : % 20.14/20.20 ( empty(A) % 20.14/20.20 => relation(A) ) ). % 20.14/20.20 % 20.14/20.20 fof(cc1_relset_1,axiom, % 20.14/20.20 ! [A,B,C] : % 20.14/20.20 ( element(C,powerset(cartesian_product2(A,B))) % 20.14/20.20 => relation(C) ) ). % 20.14/20.20 % 20.14/20.20 fof(cc2_funct_1,axiom, % 20.14/20.20 ! [A] : % 20.14/20.20 ( ( relation(A) % 20.14/20.20 & empty(A) % 20.14/20.20 & function(A) ) % 20.14/20.20 => ( relation(A) % 20.14/20.20 & function(A) % 20.14/20.20 & one_to_one(A) ) ) ). % 20.14/20.20 % 20.14/20.20 fof(d13_yellow_0,axiom, % 20.14/20.20 ! [A] : % 20.14/20.20 ( rel_str(A) % 20.14/20.20 => ! [B] : % 20.14/20.20 ( rel_str(B) % 20.14/20.20 => ( subrelstr(B,A) % 20.14/20.20 <=> ( subset(the_carrier(B),the_carrier(A)) % 20.14/20.20 & subset(the_InternalRel(B),the_InternalRel(A)) ) ) ) ) ). % 20.14/20.20 % 20.14/20.20 fof(d8_yellow_6,axiom, % 20.14/20.20 ! [A] : % 20.14/20.20 ( one_sorted_str(A) % 20.14/20.20 => ! [B] : % 20.14/20.20 ( net_str(B,A) % 20.14/20.20 => ! [C] : % 20.14/20.20 ( net_str(C,A) % 20.14/20.20 => ( subnetstr(C,A,B) % 20.14/20.20 <=> ( subrelstr(C,B) % 20.14/20.20 & the_mapping(A,C) = relation_dom_restr_as_relation_of(the_carrier(B),the_carrier(A),the_mapping(A,B),the_carrier(C)) ) ) ) ) ) ). % 20.14/20.20 % 20.14/20.20 fof(dt_k1_xboole_0,axiom, % 20.14/20.20 $true ). % 20.14/20.20 % 20.14/20.20 fof(dt_k1_zfmisc_1,axiom, % 20.14/20.20 $true ). % 20.14/20.20 % 20.14/20.20 fof(dt_k2_zfmisc_1,axiom, % 20.14/20.20 $true ). % 20.14/20.20 % 20.14/20.20 fof(dt_k7_relat_1,axiom, % 20.14/20.20 ! [A,B] : % 20.14/20.20 ( relation(A) % 20.14/20.20 => relation(relation_dom_restriction(A,B)) ) ). % 20.14/20.20 % 20.14/20.20 fof(dt_k8_relset_1,axiom, % 20.14/20.20 ! [A,B,C,D] : % 20.14/20.20 ( relation_of2(C,A,B) % 20.14/20.20 => relation_of2_as_subset(relation_dom_restr_as_relation_of(A,B,C,D),A,B) ) ). % 20.14/20.20 % 20.14/20.20 fof(dt_l1_orders_2,axiom, % 20.14/20.20 ! [A] : % 20.14/20.20 ( rel_str(A) % 20.14/20.20 => one_sorted_str(A) ) ). % 20.14/20.20 % 20.14/20.20 fof(dt_l1_struct_0,axiom, % 20.14/20.20 $true ). % 20.14/20.20 % 20.14/20.20 fof(dt_l1_waybel_0,axiom, % 20.14/20.20 ! [A] : % 20.14/20.20 ( one_sorted_str(A) % 20.14/20.20 => ! [B] : % 20.14/20.20 ( net_str(B,A) % 20.14/20.20 => rel_str(B) ) ) ). % 20.14/20.20 % 20.14/20.20 fof(dt_m1_relset_1,axiom, % 20.14/20.20 $true ). % 20.14/20.20 % 20.14/20.20 fof(dt_m1_subset_1,axiom, % 20.14/20.20 $true ). % 20.14/20.20 % 20.14/20.20 fof(dt_m1_yellow_0,axiom, % 20.14/20.20 ! [A] : % 20.14/20.20 ( rel_str(A) % 20.14/20.20 => ! [B] : % 20.14/20.20 ( subrelstr(B,A) % 20.14/20.20 => rel_str(B) ) ) ). % 20.14/20.20 % 20.14/20.20 fof(dt_m1_yellow_6,axiom, % 20.14/20.20 ! [A,B] : % 20.14/20.20 ( ( one_sorted_str(A) % 20.14/20.20 & net_str(B,A) ) % 20.14/20.20 => ! [C] : % 20.14/20.20 ( subnetstr(C,A,B) % 20.14/20.20 => net_str(C,A) ) ) ). % 20.14/20.20 % 20.14/20.20 fof(dt_m2_relset_1,axiom, % 20.14/20.20 ! [A,B,C] : % 20.14/20.20 ( relation_of2_as_subset(C,A,B) % 20.14/20.20 => element(C,powerset(cartesian_product2(A,B))) ) ). % 20.14/20.20 % 20.14/20.20 fof(dt_u1_orders_2,axiom, % 20.14/20.20 ! [A] : % 20.14/20.20 ( rel_str(A) % 20.14/20.20 => relation_of2_as_subset(the_InternalRel(A),the_carrier(A),the_carrier(A)) ) ). % 20.14/20.20 % 20.14/20.20 fof(dt_u1_struct_0,axiom, % 20.14/20.20 $true ). % 20.14/20.20 % 20.14/20.20 fof(dt_u1_waybel_0,axiom, % 20.14/20.20 ! [A,B] : % 20.14/20.20 ( ( one_sorted_str(A) % 20.14/20.20 & net_str(B,A) ) % 20.14/20.20 => ( function(the_mapping(A,B)) % 20.14/20.20 & quasi_total(the_mapping(A,B),the_carrier(B),the_carrier(A)) % 20.14/20.20 & relation_of2_as_subset(the_mapping(A,B),the_carrier(B),the_carrier(A)) ) ) ). % 20.14/20.20 % 20.14/20.20 fof(existence_l1_orders_2,axiom, % 20.14/20.20 ? [A] : rel_str(A) ). % 20.14/20.20 % 20.14/20.20 fof(existence_l1_struct_0,axiom, % 20.14/20.20 ? [A] : one_sorted_str(A) ). % 20.14/20.20 % 20.14/20.20 fof(existence_l1_waybel_0,axiom, % 20.14/20.20 ! [A] : % 20.14/20.20 ( one_sorted_str(A) % 20.14/20.20 => ? [B] : net_str(B,A) ) ). % 20.14/20.20 % 20.14/20.20 fof(existence_m1_relset_1,axiom, % 20.14/20.20 ! [A,B] : % 20.14/20.20 ? [C] : relation_of2(C,A,B) ). % 20.14/20.20 % 20.14/20.20 fof(existence_m1_subset_1,axiom, % 20.14/20.20 ! [A] : % 20.14/20.20 ? [B] : element(B,A) ). % 20.14/20.20 % 20.14/20.20 fof(existence_m1_yellow_0,axiom, % 20.14/20.20 ! [A] : % 20.14/20.20 ( rel_str(A) % 20.14/20.20 => ? [B] : subrelstr(B,A) ) ). % 20.14/20.20 % 20.14/20.20 fof(existence_m1_yellow_6,axiom, % 20.14/20.20 ! [A,B] : % 20.14/20.20 ( ( one_sorted_str(A) % 20.14/20.20 & net_str(B,A) ) % 20.14/20.20 => ? [C] : subnetstr(C,A,B) ) ). % 20.14/20.20 % 20.14/20.20 fof(existence_m2_relset_1,axiom, % 20.14/20.20 ! [A,B] : % 20.14/20.20 ? [C] : relation_of2_as_subset(C,A,B) ). % 20.14/20.20 % 20.14/20.20 fof(fc12_relat_1,axiom, % 20.14/20.20 ( empty(empty_set) % 20.14/20.20 & relation(empty_set) % 20.14/20.20 & relation_empty_yielding(empty_set) ) ). % 20.14/20.20 % 20.14/20.20 fof(fc13_relat_1,axiom, % 20.14/20.20 ! [A,B] : % 20.14/20.20 ( ( relation(A) % 20.14/20.20 & relation_empty_yielding(A) ) % 20.14/20.20 => ( relation(relation_dom_restriction(A,B)) % 20.14/20.20 & relation_empty_yielding(relation_dom_restriction(A,B)) ) ) ). % 20.14/20.21 % 20.14/20.21 fof(fc1_subset_1,axiom, % 20.14/20.21 ! [A] : ~ empty(powerset(A)) ). % 20.14/20.21 % 20.14/20.21 fof(fc4_funct_1,axiom, % 20.14/20.21 ! [A,B] : % 20.14/20.21 ( ( relation(A) % 20.14/20.21 & function(A) ) % 20.14/20.21 => ( relation(relation_dom_restriction(A,B)) % 20.14/20.21 & function(relation_dom_restriction(A,B)) ) ) ). % 20.14/20.21 % 20.14/20.21 fof(fc4_relat_1,axiom, % 20.14/20.21 ( empty(empty_set) % 20.14/20.21 & relation(empty_set) ) ). % 20.14/20.21 % 20.14/20.21 fof(fc4_subset_1,axiom, % 20.14/20.21 ! [A,B] : % 20.14/20.21 ( ( ~ empty(A) % 20.14/20.21 & ~ empty(B) ) % 20.14/20.21 => ~ empty(cartesian_product2(A,B)) ) ). % 20.14/20.21 % 20.14/20.21 fof(rc1_funct_1,axiom, % 20.14/20.21 ? [A] : % 20.14/20.21 ( relation(A) % 20.14/20.21 & function(A) ) ). % 20.14/20.21 % 20.14/20.21 fof(rc1_pboole,axiom, % 20.14/20.21 ? [A] : % 20.14/20.21 ( relation(A) % 20.14/20.21 & relation_empty_yielding(A) % 20.14/20.21 & function(A) ) ). % 20.14/20.21 % 20.14/20.21 fof(rc1_relat_1,axiom, % 20.14/20.21 ? [A] : % 20.14/20.21 ( empty(A) % 20.14/20.21 & relation(A) ) ). % 20.14/20.21 % 20.14/20.21 fof(rc1_subset_1,axiom, % 20.14/20.21 ! [A] : % 20.14/20.21 ( ~ empty(A) % 20.14/20.21 => ? [B] : % 20.14/20.21 ( element(B,powerset(A)) % 20.14/20.21 & ~ empty(B) ) ) ). % 20.14/20.21 % 20.14/20.21 fof(rc2_funct_1,axiom, % 20.14/20.21 ? [A] : % 20.14/20.21 ( relation(A) % 20.14/20.21 & empty(A) % 20.14/20.21 & function(A) ) ). % 20.14/20.21 % 20.14/20.21 fof(rc2_relat_1,axiom, % 20.14/20.21 ? [A] : % 20.14/20.21 ( ~ empty(A) % 20.14/20.21 & relation(A) ) ). % 20.14/20.21 % 20.14/20.21 fof(rc2_subset_1,axiom, % 20.14/20.21 ! [A] : % 20.14/20.21 ? [B] : % 20.14/20.21 ( element(B,powerset(A)) % 20.14/20.21 & empty(B) ) ). % 20.14/20.21 % 20.14/20.21 fof(rc3_funct_1,axiom, % 20.14/20.21 ? [A] : % 20.14/20.21 ( relation(A) % 20.14/20.21 & function(A) % 20.14/20.21 & one_to_one(A) ) ). % 20.14/20.21 % 20.14/20.21 fof(rc3_relat_1,axiom, % 20.14/20.21 ? [A] : % 20.14/20.21 ( relation(A) % 20.14/20.21 & relation_empty_yielding(A) ) ). % 20.14/20.21 % 20.14/20.21 fof(rc4_funct_1,axiom, % 20.14/20.21 ? [A] : % 20.14/20.21 ( relation(A) % 20.14/20.21 & relation_empty_yielding(A) % 20.14/20.21 & function(A) ) ). % 20.14/20.21 % 20.14/20.21 fof(redefinition_k8_relset_1,axiom, % 20.14/20.21 ! [A,B,C,D] : % 20.14/20.21 ( relation_of2(C,A,B) % 20.14/20.21 => relation_dom_restr_as_relation_of(A,B,C,D) = relation_dom_restriction(C,D) ) ). % 20.14/20.21 % 20.14/20.21 fof(redefinition_m2_relset_1,axiom, % 20.14/20.21 ! [A,B,C] : % 20.14/20.21 ( relation_of2_as_subset(C,A,B) % 20.14/20.21 <=> relation_of2(C,A,B) ) ). % 20.14/20.21 % 20.14/20.21 fof(reflexivity_r1_tarski,axiom, % 20.14/20.21 ! [A,B] : subset(A,A) ). % 20.14/20.21 % 20.14/20.21 fof(t19_yellow_6,conjecture, % 20.14/20.21 ! [A] : % 20.14/20.21 ( one_sorted_str(A) % 20.14/20.21 => ! [B] : % 20.14/20.21 ( net_str(B,A) % 20.14/20.21 => ! [C] : % 20.14/20.21 ( subnetstr(C,A,B) % 20.14/20.21 => subset(the_carrier(C),the_carrier(B)) ) ) ) ). % 20.14/20.21 % 20.14/20.21 fof(t1_subset,axiom, % 20.14/20.21 ! [A,B] : % 20.14/20.21 ( in(A,B) % 20.14/20.21 => element(A,B) ) ). % 20.14/20.21 % 20.14/20.21 fof(t2_subset,axiom, % 20.14/20.21 ! [A,B] : % 20.14/20.21 ( element(A,B) % 20.14/20.21 => ( empty(B) % 20.14/20.21 | in(A,B) ) ) ). % 20.14/20.21 % 20.14/20.21 fof(t3_subset,axiom, % 20.14/20.21 ! [A,B] : % 20.14/20.21 ( element(A,powerset(B)) % 20.14/20.21 <=> subset(A,B) ) ). % 20.14/20.21 % 20.14/20.21 fof(t4_subset,axiom, % 20.14/20.21 ! [A,B,C] : % 20.14/20.21 ( ( in(A,B) % 20.14/20.21 & element(B,powerset(C)) ) % 20.14/20.21 => element(A,C) ) ). % 20.14/20.21 % 20.14/20.21 fof(t5_subset,axiom, % 20.14/20.21 ! [A,B,C] : % 20.14/20.21 ~ ( in(A,B) % 20.14/20.21 & element(B,powerset(C)) % 20.14/20.21 & empty(C) ) ). % 20.14/20.21 % 20.14/20.21 fof(t6_boole,axiom, % 20.14/20.21 ! [A] : % 20.14/20.21 ( empty(A) % 20.14/20.21 => A = empty_set ) ). % 20.14/20.21 % 20.14/20.21 fof(t7_boole,axiom, % 20.14/20.21 ! [A,B] : % 20.14/20.21 ~ ( in(A,B) % 20.14/20.21 & empty(B) ) ). % 20.14/20.21 % 20.14/20.21 fof(t8_boole,axiom, % 20.14/20.21 ! [A,B] : % 20.14/20.21 ~ ( empty(A) % 20.14/20.21 & A != B % 20.14/20.21 & empty(B) ) ). % 20.14/20.21 % 20.14/20.21 %------------------------------------------------------------------------------ % 20.14/20.21 %------------------------------------------- % 20.14/20.21 % Proof found % 20.14/20.21 % SZS status Theorem for theBenchmark % 20.14/20.21 % SZS output start Proof % 20.14/20.21 %ClaNum:138(EqnAxiom:56) % 20.14/20.21 %VarNum:241(SingletonVarNum:97) % 20.14/20.21 %MaxLitNum:6 % 20.14/20.21 %MaxfuncDepth:2 % 20.14/20.21 %SharedTerms:45 % 20.14/20.21 %goalClause: 79 85 89 94 % 20.14/20.21 %singleGoalClaCount:4 % 20.14/20.21 [58]P1(a1) % 20.14/20.21 [59]P1(a3) % 20.14/20.21 [60]P1(a5) % 20.14/20.21 [61]P3(a7) % 20.14/20.21 [62]P3(a4) % 20.14/20.21 [63]P3(a5) % 20.14/20.21 [64]P3(a8) % 20.14/20.21 [65]P3(a11) % 20.14/20.21 [67]P4(a1) % 20.14/20.21 [68]P4(a7) % 20.14/20.21 [69]P4(a4) % 20.14/20.21 [70]P4(a3) % 20.14/20.21 [71]P4(a5) % 20.14/20.21 [72]P4(a9) % 20.14/20.21 [73]P4(a8) % 20.14/20.21 [74]P4(a12) % 20.14/20.21 [75]P4(a11) % 20.14/20.21 [76]P5(a8) % 20.14/20.21 [77]P9(a13) % 20.14/20.21 [78]P6(a15) % 20.14/20.21 [79]P6(a14) % 20.14/20.21 [80]P11(a1) % 20.14/20.21 [81]P11(a4) % 20.14/20.21 [82]P11(a12) % 20.14/20.21 [83]P11(a11) % 20.14/20.21 [85]P7(a16,a14) % 20.14/20.21 [89]P13(a17,a14,a16) % 20.14/20.21 [92]~P1(a9) % 20.14/20.21 [94]~P12(f25(a17),f25(a16)) % 20.14/20.21 [86]P12(x861,x861) % 20.14/20.21 [84]P1(f10(x841)) % 20.14/20.21 [87]P2(f18(x871),x871) % 20.14/20.21 [88]P2(f10(x881),f24(x881)) % 20.14/20.21 [93]~P1(f24(x931)) % 20.14/20.21 [90]P14(f19(x901,x902),x901,x902) % 20.14/20.21 [91]P15(f21(x911,x912),x911,x912) % 20.14/20.21 [95]~P1(x951)+E(x951,a1) % 20.14/20.21 [96]~P1(x961)+P3(x961) % 20.14/20.21 [97]~P1(x971)+P4(x971) % 20.14/20.21 [98]~P9(x981)+P6(x981) % 20.14/20.21 [100]P1(x1001)+~P1(f6(x1001)) % 20.14/20.21 [102]~P9(x1021)+P16(f22(x1021),x1021) % 20.14/20.21 [103]~P6(x1031)+P7(f20(x1031),x1031) % 20.14/20.21 [105]P1(x1051)+P2(f6(x1051),f24(x1051)) % 20.14/20.21 [124]~P9(x1241)+P15(f28(x1241),f25(x1241),f25(x1241)) % 20.14/20.21 [104]~P1(x1041)+~P8(x1042,x1041) % 20.14/20.21 [108]~P8(x1081,x1082)+P2(x1081,x1082) % 20.14/20.21 [116]~P8(x1162,x1161)+~P8(x1161,x1162) % 20.14/20.21 [109]~P4(x1091)+P4(f26(x1091,x1092)) % 20.14/20.21 [111]~P12(x1111,x1112)+P2(x1111,f24(x1112)) % 20.14/20.21 [117]P12(x1171,x1172)+~P2(x1171,f24(x1172)) % 20.14/20.21 [131]~P15(x1311,x1312,x1313)+P14(x1311,x1312,x1313) % 20.14/20.21 [132]~P14(x1321,x1322,x1323)+P15(x1321,x1322,x1323) % 20.14/20.21 [127]P4(x1271)+~P2(x1271,f24(f2(x1272,x1273))) % 20.14/20.21 [134]~P15(x1341,x1342,x1343)+P2(x1341,f24(f2(x1342,x1343))) % 20.14/20.21 [135]~P14(x1353,x1351,x1352)+E(f27(x1351,x1352,x1353,x1354),f26(x1353,x1354)) % 20.14/20.21 [138]~P14(x1383,x1381,x1382)+P15(f27(x1381,x1382,x1383,x1384),x1381,x1382) % 20.14/20.21 [99]~P1(x992)+~P1(x991)+E(x991,x992) % 20.14/20.21 [106]~P16(x1061,x1062)+P9(x1061)+~P9(x1062) % 20.14/20.21 [107]~P7(x1071,x1072)+P9(x1071)+~P6(x1072) % 20.14/20.21 [110]~P2(x1102,x1101)+P1(x1101)+P8(x1102,x1101) % 20.14/20.21 [112]~P3(x1121)+~P4(x1121)+P3(f26(x1121,x1122)) % 20.14/20.21 [115]~P4(x1151)+~P11(x1151)+P11(f26(x1151,x1152)) % 20.14/20.21 [118]P1(x1181)+P1(x1182)+~P1(f2(x1182,x1181)) % 20.14/20.21 [119]~P6(x1191)+~P7(x1192,x1191)+P3(f29(x1191,x1192)) % 20.14/20.21 [125]~P6(x1251)+~P7(x1252,x1251)+P13(f23(x1251,x1252),x1251,x1252) % 20.14/20.21 [128]~P6(x1281)+~P7(x1282,x1281)+P15(f29(x1281,x1282),f25(x1282),f25(x1281)) % 20.14/20.21 [129]~P6(x1291)+~P7(x1292,x1291)+P10(f29(x1291,x1292),f25(x1292),f25(x1291)) % 20.14/20.21 [120]~P1(x1201)+~P8(x1202,x1203)+~P2(x1203,f24(x1201)) % 20.14/20.21 [123]P2(x1231,x1232)+~P8(x1231,x1233)+~P2(x1233,f24(x1232)) % 20.14/20.21 [101]~P1(x1011)+~P3(x1011)+~P4(x1011)+P5(x1011) % 20.14/20.21 [121]~P9(x1212)+~P9(x1211)+~P16(x1211,x1212)+P12(f25(x1211),f25(x1212)) % 20.14/20.21 [122]~P9(x1222)+~P9(x1221)+~P16(x1221,x1222)+P12(f28(x1221),f28(x1222)) % 20.14/20.21 [130]~P6(x1302)+~P13(x1301,x1302,x1303)+P7(x1301,x1302)+~P7(x1303,x1302) % 20.14/20.21 [126]~P9(x1262)+~P9(x1261)+P16(x1261,x1262)+~P12(f25(x1261),f25(x1262))+~P12(f28(x1261),f28(x1262)) % 20.14/20.21 [133]~P7(x1332,x1333)+~P7(x1331,x1333)+~P13(x1331,x1333,x1332)+P16(x1331,x1332)+~P6(x1333) % 20.14/20.21 [136]~P6(x1362)+~P7(x1361,x1362)+~P7(x1363,x1362)+~P13(x1363,x1362,x1361)+E(f27(f25(x1361),f25(x1362),f29(x1362,x1361),f25(x1363)),f29(x1362,x1363)) % 20.14/20.21 [137]~P6(x1372)+~P16(x1371,x1373)+~P7(x1373,x1372)+~P7(x1371,x1372)+P13(x1371,x1372,x1373)+~E(f27(f25(x1373),f25(x1372),f29(x1372,x1373),f25(x1371)),f29(x1372,x1371)) % 20.14/20.21 %EqnAxiom % 20.14/20.21 [1]E(x11,x11) % 20.14/20.21 [2]E(x22,x21)+~E(x21,x22) % 20.14/20.21 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 20.14/20.21 [4]~E(x41,x42)+E(f10(x41),f10(x42)) % 20.14/20.21 [5]~E(x51,x52)+E(f18(x51),f18(x52)) % 20.14/20.21 [6]~E(x61,x62)+E(f27(x61,x63,x64,x65),f27(x62,x63,x64,x65)) % 20.14/20.21 [7]~E(x71,x72)+E(f27(x73,x71,x74,x75),f27(x73,x72,x74,x75)) % 20.14/20.21 [8]~E(x81,x82)+E(f27(x83,x84,x81,x85),f27(x83,x84,x82,x85)) % 20.14/20.21 [9]~E(x91,x92)+E(f27(x93,x94,x95,x91),f27(x93,x94,x95,x92)) % 20.14/20.21 [10]~E(x101,x102)+E(f24(x101),f24(x102)) % 20.14/20.21 [11]~E(x111,x112)+E(f19(x111,x113),f19(x112,x113)) % 20.14/20.21 [12]~E(x121,x122)+E(f19(x123,x121),f19(x123,x122)) % 20.14/20.21 [13]~E(x131,x132)+E(f21(x131,x133),f21(x132,x133)) % 20.14/20.21 [14]~E(x141,x142)+E(f21(x143,x141),f21(x143,x142)) % 20.14/20.21 [15]~E(x151,x152)+E(f29(x151,x153),f29(x152,x153)) % 20.14/20.21 [16]~E(x161,x162)+E(f29(x163,x161),f29(x163,x162)) % 20.14/20.21 [17]~E(x171,x172)+E(f25(x171),f25(x172)) % 20.14/20.21 [18]~E(x181,x182)+E(f2(x181,x183),f2(x182,x183)) % 20.14/20.21 [19]~E(x191,x192)+E(f2(x193,x191),f2(x193,x192)) % 20.14/20.21 [20]~E(x201,x202)+E(f6(x201),f6(x202)) % 20.14/20.21 [21]~E(x211,x212)+E(f22(x211),f22(x212)) % 20.14/20.21 [22]~E(x221,x222)+E(f20(x221),f20(x222)) % 20.14/20.21 [23]~E(x231,x232)+E(f28(x231),f28(x232)) % 20.14/20.21 [24]~E(x241,x242)+E(f23(x241,x243),f23(x242,x243)) % 20.14/20.21 [25]~E(x251,x252)+E(f23(x253,x251),f23(x253,x252)) % 20.14/20.21 [26]~E(x261,x262)+E(f26(x261,x263),f26(x262,x263)) % 20.14/20.21 [27]~E(x271,x272)+E(f26(x273,x271),f26(x273,x272)) % 20.14/20.21 [28]~P1(x281)+P1(x282)+~E(x281,x282) % 20.14/20.21 [29]P14(x292,x293,x294)+~E(x291,x292)+~P14(x291,x293,x294) % 20.14/20.21 [30]P14(x303,x302,x304)+~E(x301,x302)+~P14(x303,x301,x304) % 20.14/20.21 [31]P14(x313,x314,x312)+~E(x311,x312)+~P14(x313,x314,x311) % 20.14/20.21 [32]P15(x322,x323,x324)+~E(x321,x322)+~P15(x321,x323,x324) % 20.14/20.21 [33]P15(x333,x332,x334)+~E(x331,x332)+~P15(x333,x331,x334) % 20.14/20.21 [34]P15(x343,x344,x342)+~E(x341,x342)+~P15(x343,x344,x341) % 20.14/20.21 [35]P7(x352,x353)+~E(x351,x352)+~P7(x351,x353) % 20.14/20.21 [36]P7(x363,x362)+~E(x361,x362)+~P7(x363,x361) % 20.14/20.21 [37]~P3(x371)+P3(x372)+~E(x371,x372) % 20.14/20.21 [38]P2(x382,x383)+~E(x381,x382)+~P2(x381,x383) % 20.14/20.21 [39]P2(x393,x392)+~E(x391,x392)+~P2(x393,x391) % 20.14/20.21 [40]P8(x402,x403)+~E(x401,x402)+~P8(x401,x403) % 20.14/20.21 [41]P8(x413,x412)+~E(x411,x412)+~P8(x413,x411) % 20.14/20.21 [42]P12(x422,x423)+~E(x421,x422)+~P12(x421,x423) % 20.14/20.21 [43]P12(x433,x432)+~E(x431,x432)+~P12(x433,x431) % 20.14/20.21 [44]P16(x442,x443)+~E(x441,x442)+~P16(x441,x443) % 20.14/20.21 [45]P16(x453,x452)+~E(x451,x452)+~P16(x453,x451) % 20.14/20.21 [46]~P4(x461)+P4(x462)+~E(x461,x462) % 20.14/20.21 [47]P13(x472,x473,x474)+~E(x471,x472)+~P13(x471,x473,x474) % 20.14/20.21 [48]P13(x483,x482,x484)+~E(x481,x482)+~P13(x483,x481,x484) % 20.14/20.21 [49]P13(x493,x494,x492)+~E(x491,x492)+~P13(x493,x494,x491) % 20.14/20.21 [50]~P9(x501)+P9(x502)+~E(x501,x502) % 20.14/20.21 [51]~P6(x511)+P6(x512)+~E(x511,x512) % 20.14/20.21 [52]~P11(x521)+P11(x522)+~E(x521,x522) % 20.14/20.21 [53]P10(x532,x533,x534)+~E(x531,x532)+~P10(x531,x533,x534) % 20.14/20.21 [54]P10(x543,x542,x544)+~E(x541,x542)+~P10(x543,x541,x544) % 20.14/20.21 [55]P10(x553,x554,x552)+~E(x551,x552)+~P10(x553,x554,x551) % 20.14/20.21 [56]~P5(x561)+P5(x562)+~E(x561,x562) % 20.14/20.21 % 20.14/20.21 %------------------------------------------- % 20.14/20.21 cnf(372,plain, % 20.14/20.21 (P3(f26(a1,x3721))), % 20.14/20.21 inference(scs_inference,[],[58,67,96,112])). % 20.14/20.21 cnf(544,plain, % 20.14/20.21 (~P9(a16)+~P7(a17,a14)+~P9(a17)), % 20.14/20.21 inference(scs_inference,[],[79,89,85,94,372,121,133])). % 20.14/20.21 cnf(3511,plain, % 20.14/20.21 (~P9(a16)+~P9(a17)), % 20.14/20.22 inference(scs_inference,[],[85,79,89,544,130])). % 20.14/20.22 cnf(3527,plain, % 20.14/20.22 (~P9(a17)), % 20.14/20.22 inference(scs_inference,[],[79,85,3511,107])). % 20.14/20.22 cnf(3532,plain, % 20.14/20.22 ($false), % 20.14/20.22 inference(scs_inference,[],[85,89,79,3527,77,106,107,130]), % 20.14/20.22 ['proof']). % 20.14/20.22 % SZS output end Proof % 20.14/20.22 % Total time :19.600000s %------------------------------------------------------------------------------