%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU292+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:17 EDT 2024 % Result : Theorem 58.70s 58.77s % Output : CNFRefutation 58.70s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SEU292+1 : TPTP v8.2.0. Released v3.3.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n022.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:03:24 EDT 2024 % 0.12/0.33 % CPUTime : % 0.49/0.56 start to proof:theBenchmark % 58.70/58.74 %------------------------------------------- % 58.70/58.74 % File :CSE---1.7 % 58.70/58.74 % Problem :theBenchmark % 58.70/58.74 % Transform :cnf % 58.70/58.74 % Format :tptp:raw % 58.70/58.74 % Command :java -jar mcs_scs.jar %d %s % 58.70/58.74 % 58.70/58.74 % Result :Theorem 58.120000s % 58.70/58.74 % Output :CNFRefutation 58.120000s % 58.70/58.74 %------------------------------------------- % 58.70/58.75 %------------------------------------------------------------------------------ % 58.70/58.75 % File : SEU292+1 : TPTP v8.2.0. Released v3.3.0. % 58.70/58.75 % Domain : Set theory % 58.70/58.75 % Problem : MPTP bushy problem t21_funct_2 % 58.70/58.75 % Version : [Urb07] axioms : Especial. % 58.70/58.75 % English : % 58.70/58.75 % 58.70/58.75 % Refs : [Ban01] Bancerek et al. (2001), On the Characterizations of Co % 58.70/58.75 % : [Urb07] Urban (2006), Email to G. Sutcliffe % 58.70/58.75 % Source : [Urb07] % 58.70/58.75 % Names : bushy-t21_funct_2 [Urb07] % 58.70/58.75 % 58.70/58.75 % Status : Theorem % 58.70/58.75 % Rating : 0.28 v8.1.0, 0.25 v7.5.0, 0.28 v7.4.0, 0.17 v7.3.0, 0.21 v7.1.0, 0.30 v7.0.0, 0.27 v6.4.0, 0.35 v6.3.0, 0.33 v6.2.0, 0.36 v6.1.0, 0.43 v6.0.0, 0.35 v5.5.0, 0.44 v5.4.0, 0.50 v5.3.0, 0.56 v5.2.0, 0.45 v5.1.0, 0.52 v5.0.0, 0.50 v4.1.0, 0.52 v4.0.0, 0.58 v3.7.0, 0.50 v3.5.0, 0.53 v3.4.0, 0.63 v3.3.0 % 58.70/58.75 % Syntax : Number of formulae : 56 ( 15 unt; 0 def) % 58.70/58.75 % Number of atoms : 144 ( 12 equ) % 58.70/58.75 % Maximal formula atoms : 9 ( 2 avg) % 58.70/58.75 % Number of connectives : 103 ( 15 ~; 3 |; 51 &) % 58.70/58.75 % ( 4 <=>; 30 =>; 0 <=; 0 <~>) % 58.70/58.75 % Maximal formula depth : 10 ( 4 avg) % 58.70/58.75 % Maximal term depth : 3 ( 1 avg) % 58.70/58.75 % Number of predicates : 13 ( 11 usr; 1 prp; 0-3 aty) % 58.70/58.75 % Number of functors : 7 ( 7 usr; 1 con; 0-3 aty) % 58.70/58.75 % Number of variables : 91 ( 74 !; 17 ?) % 58.70/58.75 % SPC : FOF_THM_RFO_SEQ % 58.70/58.75 % 58.70/58.75 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 58.70/58.75 % library, www.mizar.org % 58.70/58.75 %------------------------------------------------------------------------------ % 58.70/58.75 fof(antisymmetry_r2_hidden,axiom, % 58.70/58.75 ! [A,B] : % 58.70/58.75 ( in(A,B) % 58.70/58.75 => ~ in(B,A) ) ). % 58.70/58.75 % 58.70/58.75 fof(cc1_funct_1,axiom, % 58.70/58.75 ! [A] : % 58.70/58.75 ( empty(A) % 58.70/58.75 => function(A) ) ). % 58.70/58.75 % 58.70/58.75 fof(cc1_relat_1,axiom, % 58.70/58.75 ! [A] : % 58.70/58.75 ( empty(A) % 58.70/58.75 => relation(A) ) ). % 58.70/58.75 % 58.70/58.75 fof(cc1_relset_1,axiom, % 58.70/58.75 ! [A,B,C] : % 58.70/58.75 ( element(C,powerset(cartesian_product2(A,B))) % 58.70/58.75 => relation(C) ) ). % 58.70/58.75 % 58.70/58.75 fof(cc2_funct_1,axiom, % 58.70/58.76 ! [A] : % 58.70/58.76 ( ( relation(A) % 58.70/58.76 & empty(A) % 58.70/58.76 & function(A) ) % 58.70/58.76 => ( relation(A) % 58.70/58.76 & function(A) % 58.70/58.76 & one_to_one(A) ) ) ). % 58.70/58.76 % 58.70/58.76 fof(d1_funct_2,axiom, % 58.70/58.76 ! [A,B,C] : % 58.70/58.76 ( relation_of2_as_subset(C,A,B) % 58.70/58.76 => ( ( ( B = empty_set % 58.70/58.76 => A = empty_set ) % 58.70/58.76 => ( quasi_total(C,A,B) % 58.70/58.76 <=> A = relation_dom_as_subset(A,B,C) ) ) % 58.70/58.76 & ( B = empty_set % 58.70/58.76 => ( A = empty_set % 58.70/58.76 | ( quasi_total(C,A,B) % 58.70/58.76 <=> C = empty_set ) ) ) ) ) ). % 58.70/58.76 % 58.70/58.76 fof(dt_k1_funct_1,axiom, % 58.70/58.76 $true ). % 58.70/58.76 % 58.70/58.76 fof(dt_k1_relat_1,axiom, % 58.70/58.76 $true ). % 58.70/58.76 % 58.70/58.76 fof(dt_k1_xboole_0,axiom, % 58.70/58.76 $true ). % 58.70/58.76 % 58.70/58.76 fof(dt_k1_zfmisc_1,axiom, % 58.70/58.76 $true ). % 58.70/58.76 % 58.70/58.76 fof(dt_k2_zfmisc_1,axiom, % 58.70/58.76 $true ). % 58.70/58.76 % 58.70/58.76 fof(dt_k4_relset_1,axiom, % 58.70/58.76 ! [A,B,C] : % 58.70/58.76 ( relation_of2(C,A,B) % 58.70/58.76 => element(relation_dom_as_subset(A,B,C),powerset(A)) ) ). % 58.70/58.76 % 58.70/58.76 fof(dt_k5_relat_1,axiom, % 58.70/58.76 ! [A,B] : % 58.70/58.76 ( ( relation(A) % 58.70/58.76 & relation(B) ) % 58.70/58.76 => relation(relation_composition(A,B)) ) ). % 58.70/58.76 % 58.70/58.76 fof(dt_m1_relset_1,axiom, % 58.70/58.76 $true ). % 58.70/58.76 % 58.70/58.76 fof(dt_m1_subset_1,axiom, % 58.70/58.76 $true ). % 58.70/58.76 % 58.70/58.76 fof(dt_m2_relset_1,axiom, % 58.70/58.76 ! [A,B,C] : % 58.70/58.76 ( relation_of2_as_subset(C,A,B) % 58.70/58.76 => element(C,powerset(cartesian_product2(A,B))) ) ). % 58.70/58.76 % 58.70/58.76 fof(existence_m1_relset_1,axiom, % 58.70/58.76 ! [A,B] : % 58.70/58.76 ? [C] : relation_of2(C,A,B) ). % 58.70/58.76 % 58.70/58.76 fof(existence_m1_subset_1,axiom, % 58.70/58.76 ! [A] : % 58.70/58.76 ? [B] : element(B,A) ). % 58.70/58.76 % 58.70/58.76 fof(existence_m2_relset_1,axiom, % 58.70/58.76 ! [A,B] : % 58.70/58.76 ? [C] : relation_of2_as_subset(C,A,B) ). % 58.70/58.76 % 58.70/58.76 fof(fc10_relat_1,axiom, % 58.70/58.76 ! [A,B] : % 58.70/58.76 ( ( empty(A) % 58.70/58.76 & relation(B) ) % 58.70/58.76 => ( empty(relation_composition(B,A)) % 58.70/58.76 & relation(relation_composition(B,A)) ) ) ). % 58.70/58.76 % 58.70/58.76 fof(fc12_relat_1,axiom, % 58.70/58.76 ( empty(empty_set) % 58.70/58.76 & relation(empty_set) % 58.70/58.76 & relation_empty_yielding(empty_set) ) ). % 58.70/58.76 % 58.70/58.76 fof(fc1_funct_1,axiom, % 58.70/58.76 ! [A,B] : % 58.70/58.76 ( ( relation(A) % 58.70/58.76 & function(A) % 58.70/58.76 & relation(B) % 58.70/58.76 & function(B) ) % 58.70/58.76 => ( relation(relation_composition(A,B)) % 58.70/58.76 & function(relation_composition(A,B)) ) ) ). % 58.70/58.76 % 58.70/58.76 fof(fc1_subset_1,axiom, % 58.70/58.76 ! [A] : ~ empty(powerset(A)) ). % 58.70/58.76 % 58.70/58.76 fof(fc1_xboole_0,axiom, % 58.70/58.76 empty(empty_set) ). % 58.70/58.76 % 58.70/58.76 fof(fc4_relat_1,axiom, % 58.70/58.76 ( empty(empty_set) % 58.70/58.76 & relation(empty_set) ) ). % 58.70/58.76 % 58.70/58.76 fof(fc4_subset_1,axiom, % 58.70/58.76 ! [A,B] : % 58.70/58.76 ( ( ~ empty(A) % 58.70/58.76 & ~ empty(B) ) % 58.70/58.76 => ~ empty(cartesian_product2(A,B)) ) ). % 58.70/58.76 % 58.70/58.76 fof(fc5_relat_1,axiom, % 58.70/58.76 ! [A] : % 58.70/58.76 ( ( ~ empty(A) % 58.70/58.76 & relation(A) ) % 58.70/58.76 => ~ empty(relation_dom(A)) ) ). % 58.70/58.76 % 58.70/58.76 fof(fc7_relat_1,axiom, % 58.70/58.76 ! [A] : % 58.70/58.76 ( empty(A) % 58.70/58.76 => ( empty(relation_dom(A)) % 58.70/58.76 & relation(relation_dom(A)) ) ) ). % 58.70/58.76 % 58.70/58.76 fof(fc9_relat_1,axiom, % 58.70/58.76 ! [A,B] : % 58.70/58.76 ( ( empty(A) % 58.70/58.76 & relation(B) ) % 58.70/58.76 => ( empty(relation_composition(A,B)) % 58.70/58.76 & relation(relation_composition(A,B)) ) ) ). % 58.70/58.76 % 58.70/58.76 fof(rc1_funct_1,axiom, % 58.70/58.76 ? [A] : % 58.70/58.76 ( relation(A) % 58.70/58.76 & function(A) ) ). % 58.70/58.76 % 58.70/58.76 fof(rc1_funct_2,axiom, % 58.70/58.76 ! [A,B] : % 58.70/58.76 ? [C] : % 58.70/58.76 ( relation_of2(C,A,B) % 58.70/58.76 & relation(C) % 58.70/58.76 & function(C) % 58.70/58.76 & quasi_total(C,A,B) ) ). % 58.70/58.76 % 58.70/58.76 fof(rc1_partfun1,axiom, % 58.70/58.76 ? [A] : % 58.70/58.76 ( relation(A) % 58.70/58.76 & function(A) % 58.70/58.76 & one_to_one(A) % 58.70/58.76 & empty(A) ) ). % 58.70/58.76 % 58.70/58.76 fof(rc1_relat_1,axiom, % 58.70/58.76 ? [A] : % 58.70/58.76 ( empty(A) % 58.70/58.76 & relation(A) ) ). % 58.70/58.76 % 58.70/58.76 fof(rc1_subset_1,axiom, % 58.70/58.76 ! [A] : % 58.70/58.76 ( ~ empty(A) % 58.70/58.76 => ? [B] : % 58.70/58.76 ( element(B,powerset(A)) % 58.70/58.76 & ~ empty(B) ) ) ). % 58.70/58.76 % 58.70/58.76 fof(rc1_xboole_0,axiom, % 58.70/58.76 ? [A] : empty(A) ). % 58.70/58.76 % 58.70/58.76 fof(rc2_funct_1,axiom, % 58.70/58.76 ? [A] : % 58.70/58.76 ( relation(A) % 58.70/58.76 & empty(A) % 58.70/58.76 & function(A) ) ). % 58.70/58.76 % 58.70/58.76 fof(rc2_partfun1,axiom, % 58.70/58.76 ! [A,B] : % 58.70/58.76 ? [C] : % 58.70/58.76 ( relation_of2(C,A,B) % 58.70/58.76 & relation(C) % 58.70/58.76 & function(C) ) ). % 58.70/58.76 % 58.70/58.76 fof(rc2_relat_1,axiom, % 58.70/58.76 ? [A] : % 58.70/58.76 ( ~ empty(A) % 58.70/58.76 & relation(A) ) ). % 58.70/58.76 % 58.70/58.76 fof(rc2_subset_1,axiom, % 58.70/58.76 ! [A] : % 58.70/58.76 ? [B] : % 58.70/58.76 ( element(B,powerset(A)) % 58.70/58.76 & empty(B) ) ). % 58.70/58.76 % 58.70/58.76 fof(rc2_xboole_0,axiom, % 58.70/58.76 ? [A] : ~ empty(A) ). % 58.70/58.76 % 58.70/58.76 fof(rc3_funct_1,axiom, % 58.70/58.76 ? [A] : % 58.70/58.76 ( relation(A) % 58.70/58.76 & function(A) % 58.70/58.76 & one_to_one(A) ) ). % 58.70/58.76 % 58.70/58.76 fof(rc3_relat_1,axiom, % 58.70/58.76 ? [A] : % 58.70/58.76 ( relation(A) % 58.70/58.76 & relation_empty_yielding(A) ) ). % 58.70/58.76 % 58.70/58.76 fof(rc4_funct_1,axiom, % 58.70/58.76 ? [A] : % 58.70/58.76 ( relation(A) % 58.70/58.76 & relation_empty_yielding(A) % 58.70/58.76 & function(A) ) ). % 58.70/58.76 % 58.70/58.76 fof(redefinition_k4_relset_1,axiom, % 58.70/58.76 ! [A,B,C] : % 58.70/58.76 ( relation_of2(C,A,B) % 58.70/58.76 => relation_dom_as_subset(A,B,C) = relation_dom(C) ) ). % 58.70/58.76 % 58.70/58.76 fof(redefinition_m2_relset_1,axiom, % 58.70/58.76 ! [A,B,C] : % 58.70/58.76 ( relation_of2_as_subset(C,A,B) % 58.70/58.76 <=> relation_of2(C,A,B) ) ). % 58.70/58.76 % 58.70/58.76 fof(reflexivity_r1_tarski,axiom, % 58.70/58.76 ! [A,B] : subset(A,A) ). % 58.70/58.76 % 58.70/58.76 fof(t1_subset,axiom, % 58.70/58.76 ! [A,B] : % 58.70/58.76 ( in(A,B) % 58.70/58.76 => element(A,B) ) ). % 58.70/58.76 % 58.70/58.76 fof(t21_funct_2,conjecture, % 58.70/58.76 ! [A,B,C,D] : % 58.70/58.76 ( ( function(D) % 58.70/58.76 & quasi_total(D,A,B) % 58.70/58.76 & relation_of2_as_subset(D,A,B) ) % 58.70/58.76 => ! [E] : % 58.70/58.76 ( ( relation(E) % 58.70/58.76 & function(E) ) % 58.70/58.76 => ( in(C,A) % 58.70/58.76 => ( B = empty_set % 58.70/58.76 | apply(relation_composition(D,E),C) = apply(E,apply(D,C)) ) ) ) ) ). % 58.70/58.76 % 58.70/58.76 fof(t23_funct_1,axiom, % 58.70/58.76 ! [A,B] : % 58.70/58.76 ( ( relation(B) % 58.70/58.76 & function(B) ) % 58.70/58.76 => ! [C] : % 58.70/58.76 ( ( relation(C) % 58.70/58.76 & function(C) ) % 58.70/58.76 => ( in(A,relation_dom(B)) % 58.70/58.76 => apply(relation_composition(B,C),A) = apply(C,apply(B,A)) ) ) ) ). % 58.70/58.76 % 58.70/58.76 fof(t2_subset,axiom, % 58.70/58.76 ! [A,B] : % 58.70/58.76 ( element(A,B) % 58.70/58.76 => ( empty(B) % 58.70/58.76 | in(A,B) ) ) ). % 58.70/58.76 % 58.70/58.76 fof(t3_subset,axiom, % 58.70/58.76 ! [A,B] : % 58.70/58.76 ( element(A,powerset(B)) % 58.70/58.76 <=> subset(A,B) ) ). % 58.70/58.76 % 58.70/58.76 fof(t4_subset,axiom, % 58.70/58.76 ! [A,B,C] : % 58.70/58.76 ( ( in(A,B) % 58.70/58.76 & element(B,powerset(C)) ) % 58.70/58.76 => element(A,C) ) ). % 58.70/58.76 % 58.70/58.77 fof(t5_subset,axiom, % 58.70/58.77 ! [A,B,C] : % 58.70/58.77 ~ ( in(A,B) % 58.70/58.77 & element(B,powerset(C)) % 58.70/58.77 & empty(C) ) ). % 58.70/58.77 % 58.70/58.77 fof(t6_boole,axiom, % 58.70/58.77 ! [A] : % 58.70/58.77 ( empty(A) % 58.70/58.77 => A = empty_set ) ). % 58.70/58.77 % 58.70/58.77 fof(t7_boole,axiom, % 58.70/58.77 ! [A,B] : % 58.70/58.77 ~ ( in(A,B) % 58.70/58.77 & empty(B) ) ). % 58.70/58.77 % 58.70/58.77 fof(t8_boole,axiom, % 58.70/58.77 ! [A,B] : % 58.70/58.77 ~ ( empty(A) % 58.70/58.77 & A != B % 58.70/58.77 & empty(B) ) ). % 58.70/58.77 % 58.70/58.77 %------------------------------------------------------------------------------ % 58.70/58.77 %------------------------------------------- % 58.70/58.77 % Proof found % 58.70/58.77 % SZS status Theorem for theBenchmark % 58.70/58.77 % SZS output start Proof % 58.70/58.77 %ClaNum:135(EqnAxiom:45) % 58.70/58.77 %VarNum:237(SingletonVarNum:105) % 58.70/58.77 %MaxLitNum:6 % 58.70/58.77 %MaxfuncDepth:2 % 58.70/58.77 %SharedTerms:54 % 58.70/58.77 %goalClause: 58 59 70 77 85 86 92 96 % 58.70/58.77 %singleGoalClaCount:8 % 58.70/58.77 [48]P1(a1) % 58.70/58.77 [49]P1(a4) % 58.70/58.77 [50]P1(a23) % 58.70/58.77 [51]P1(a24) % 58.70/58.77 [52]P1(a5) % 58.70/58.77 [53]P3(a6) % 58.70/58.77 [54]P3(a4) % 58.70/58.77 [55]P3(a5) % 58.70/58.77 [56]P3(a7) % 58.70/58.77 [57]P3(a12) % 58.70/58.77 [58]P3(a14) % 58.70/58.77 [59]P3(a19) % 58.70/58.77 [61]P4(a1) % 58.70/58.77 [62]P4(a6) % 58.70/58.77 [63]P4(a4) % 58.70/58.77 [64]P4(a23) % 58.70/58.77 [65]P4(a5) % 58.70/58.77 [66]P4(a8) % 58.70/58.77 [67]P4(a7) % 58.70/58.77 [68]P4(a13) % 58.70/58.77 [69]P4(a12) % 58.70/58.77 [70]P4(a19) % 58.70/58.77 [71]P5(a4) % 58.70/58.77 [72]P5(a7) % 58.70/58.77 [73]P8(a1) % 58.70/58.77 [74]P8(a13) % 58.70/58.77 [75]P8(a12) % 58.70/58.77 [77]P6(a15,a16) % 58.70/58.77 [85]P10(a14,a16,a17) % 58.70/58.77 [86]P7(a14,a16,a17) % 58.70/58.77 [92]~E(a17,a1) % 58.70/58.77 [93]~P1(a8) % 58.70/58.77 [94]~P1(a11) % 58.70/58.77 [96]~E(f2(f27(a14,a19),a15),f2(a19,f2(a14,a15))) % 58.70/58.77 [78]P9(x781,x781) % 58.70/58.77 [76]P1(f10(x761)) % 58.70/58.77 [79]P2(f20(x791),x791) % 58.70/58.77 [80]P2(f10(x801),f26(x801)) % 58.70/58.77 [95]~P1(f26(x951)) % 58.70/58.77 [81]P3(f22(x811,x812)) % 58.70/58.77 [82]P3(f9(x821,x822)) % 58.70/58.77 [83]P4(f22(x831,x832)) % 58.70/58.77 [84]P4(f9(x841,x842)) % 58.70/58.77 [87]P10(f21(x871,x872),x871,x872) % 58.70/58.77 [88]P7(f22(x881,x882),x881,x882) % 58.70/58.77 [89]P11(f18(x891,x892),x891,x892) % 58.70/58.77 [90]P11(f22(x901,x902),x901,x902) % 58.70/58.77 [91]P11(f9(x911,x912),x911,x912) % 58.70/58.77 [97]~P1(x971)+E(x971,a1) % 58.70/58.77 [98]~P1(x981)+P3(x981) % 58.70/58.77 [99]~P1(x991)+P4(x991) % 58.70/58.77 [101]~P1(x1011)+P1(f28(x1011)) % 58.70/58.77 [102]~P1(x1021)+P4(f28(x1021)) % 58.70/58.77 [103]P1(x1031)+~P1(f25(x1031)) % 58.70/58.77 [107]P1(x1071)+P2(f25(x1071),f26(x1071)) % 58.70/58.77 [106]~P1(x1061)+~P6(x1062,x1061) % 58.70/58.77 [108]~P6(x1081,x1082)+P2(x1081,x1082) % 58.70/58.77 [116]~P6(x1162,x1161)+~P6(x1161,x1162) % 58.70/58.77 [110]~P9(x1101,x1102)+P2(x1101,f26(x1102)) % 58.70/58.77 [117]P9(x1171,x1172)+~P2(x1171,f26(x1172)) % 58.70/58.77 [124]~P11(x1241,x1242,x1243)+P10(x1241,x1242,x1243) % 58.70/58.77 [125]~P10(x1251,x1252,x1253)+P11(x1251,x1252,x1253) % 58.70/58.77 [127]~P11(x1273,x1271,x1272)+E(f29(x1271,x1272,x1273),f28(x1273)) % 58.70/58.77 [131]~P11(x1313,x1311,x1312)+P2(f29(x1311,x1312,x1313),f26(x1311)) % 58.70/58.77 [123]P4(x1231)+~P2(x1231,f26(f3(x1232,x1233))) % 58.70/58.77 [129]~P10(x1291,x1292,x1293)+P2(x1291,f26(f3(x1292,x1293))) % 58.70/58.77 [105]~P4(x1051)+P1(x1051)+~P1(f28(x1051)) % 58.70/58.77 [100]~P1(x1002)+~P1(x1001)+E(x1001,x1002) % 58.70/58.77 [109]~P2(x1092,x1091)+P1(x1091)+P6(x1092,x1091) % 58.70/58.77 [111]~P1(x1112)+~P4(x1111)+P1(f27(x1111,x1112)) % 58.70/58.77 [112]~P1(x1121)+~P4(x1122)+P1(f27(x1121,x1122)) % 58.70/58.77 [113]~P1(x1132)+~P4(x1131)+P4(f27(x1131,x1132)) % 58.70/58.77 [114]~P1(x1141)+~P4(x1142)+P4(f27(x1141,x1142)) % 58.70/58.77 [115]~P4(x1152)+~P4(x1151)+P4(f27(x1151,x1152)) % 58.70/58.77 [118]P1(x1181)+P1(x1182)+~P1(f3(x1182,x1181)) % 58.70/58.77 [121]~P1(x1211)+~P6(x1212,x1213)+~P2(x1213,f26(x1211)) % 58.70/58.77 [122]P2(x1221,x1222)+~P6(x1221,x1223)+~P2(x1223,f26(x1222)) % 58.70/58.77 [104]~P1(x1041)+~P3(x1041)+~P4(x1041)+P5(x1041) % 58.70/58.77 [132]~P10(x1323,x1322,x1321)+~P7(x1323,x1322,x1321)+E(f29(x1322,x1321,x1323),x1322)+E(x1321,a1) % 58.70/58.77 [133]~P10(x1332,x1333,x1331)+P7(x1332,x1333,x1331)+~E(f29(x1333,x1331,x1332),x1333)+E(x1331,a1) % 58.70/58.77 [134]~P10(x1343,x1341,x1342)+~P7(x1343,x1341,x1342)+~E(x1341,a1)+E(f29(x1341,x1342,x1343),x1341) % 58.70/58.77 [135]~P10(x1351,x1352,x1353)+P7(x1351,x1352,x1353)+~E(x1352,a1)+~E(f29(x1352,x1353,x1351),x1352) % 58.70/58.77 [119]~P3(x1192)+~P3(x1191)+~P4(x1192)+~P4(x1191)+P3(f27(x1191,x1192)) % 58.70/58.77 [128]~P10(x1282,x1281,x1283)+P7(x1282,x1281,x1283)+~E(x1283,a1)+~E(x1282,a1)+E(x1281,a1) % 58.70/58.77 [130]~P10(x1302,x1301,x1303)+~P7(x1302,x1301,x1303)+E(x1301,a1)+E(x1302,a1)+~E(x1303,a1) % 58.70/58.77 [126]~P3(x1262)+~P3(x1261)+~P4(x1262)+~P4(x1261)+~P6(x1263,f28(x1261))+E(f2(f27(x1261,x1262),x1263),f2(x1262,f2(x1261,x1263))) % 58.70/58.77 %EqnAxiom % 58.70/58.77 [1]E(x11,x11) % 58.70/58.77 [2]E(x22,x21)+~E(x21,x22) % 58.70/58.77 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.70/58.77 [4]~E(x41,x42)+E(f10(x41),f10(x42)) % 58.70/58.77 [5]~E(x51,x52)+E(f20(x51),f20(x52)) % 58.70/58.77 [6]~E(x61,x62)+E(f29(x61,x63,x64),f29(x62,x63,x64)) % 58.70/58.77 [7]~E(x71,x72)+E(f29(x73,x71,x74),f29(x73,x72,x74)) % 58.70/58.77 [8]~E(x81,x82)+E(f29(x83,x84,x81),f29(x83,x84,x82)) % 58.70/58.77 [9]~E(x91,x92)+E(f26(x91),f26(x92)) % 58.70/58.77 [10]~E(x101,x102)+E(f22(x101,x103),f22(x102,x103)) % 58.70/58.77 [11]~E(x111,x112)+E(f22(x113,x111),f22(x113,x112)) % 58.70/58.77 [12]~E(x121,x122)+E(f9(x121,x123),f9(x122,x123)) % 58.70/58.77 [13]~E(x131,x132)+E(f9(x133,x131),f9(x133,x132)) % 58.70/58.77 [14]~E(x141,x142)+E(f27(x141,x143),f27(x142,x143)) % 58.70/58.77 [15]~E(x151,x152)+E(f27(x153,x151),f27(x153,x152)) % 58.70/58.77 [16]~E(x161,x162)+E(f2(x161,x163),f2(x162,x163)) % 58.70/58.77 [17]~E(x171,x172)+E(f2(x173,x171),f2(x173,x172)) % 58.70/58.77 [18]~E(x181,x182)+E(f21(x181,x183),f21(x182,x183)) % 58.70/58.77 [19]~E(x191,x192)+E(f21(x193,x191),f21(x193,x192)) % 58.70/58.77 [20]~E(x201,x202)+E(f3(x201,x203),f3(x202,x203)) % 58.70/58.77 [21]~E(x211,x212)+E(f3(x213,x211),f3(x213,x212)) % 58.70/58.77 [22]~E(x221,x222)+E(f18(x221,x223),f18(x222,x223)) % 58.70/58.77 [23]~E(x231,x232)+E(f18(x233,x231),f18(x233,x232)) % 58.70/58.77 [24]~E(x241,x242)+E(f28(x241),f28(x242)) % 58.70/58.77 [25]~E(x251,x252)+E(f25(x251),f25(x252)) % 58.70/58.77 [26]~P1(x261)+P1(x262)+~E(x261,x262) % 58.70/58.77 [27]P10(x272,x273,x274)+~E(x271,x272)+~P10(x271,x273,x274) % 58.70/58.77 [28]P10(x283,x282,x284)+~E(x281,x282)+~P10(x283,x281,x284) % 58.70/58.77 [29]P10(x293,x294,x292)+~E(x291,x292)+~P10(x293,x294,x291) % 58.70/58.77 [30]P7(x302,x303,x304)+~E(x301,x302)+~P7(x301,x303,x304) % 58.70/58.77 [31]P7(x313,x312,x314)+~E(x311,x312)+~P7(x313,x311,x314) % 58.70/58.77 [32]P7(x323,x324,x322)+~E(x321,x322)+~P7(x323,x324,x321) % 58.70/58.77 [33]P6(x332,x333)+~E(x331,x332)+~P6(x331,x333) % 58.70/58.77 [34]P6(x343,x342)+~E(x341,x342)+~P6(x343,x341) % 58.70/58.77 [35]~P3(x351)+P3(x352)+~E(x351,x352) % 58.70/58.77 [36]~P4(x361)+P4(x362)+~E(x361,x362) % 58.70/58.77 [37]P2(x372,x373)+~E(x371,x372)+~P2(x371,x373) % 58.70/58.77 [38]P2(x383,x382)+~E(x381,x382)+~P2(x383,x381) % 58.70/58.77 [39]P9(x392,x393)+~E(x391,x392)+~P9(x391,x393) % 58.70/58.77 [40]P9(x403,x402)+~E(x401,x402)+~P9(x403,x401) % 58.70/58.77 [41]P11(x412,x413,x414)+~E(x411,x412)+~P11(x411,x413,x414) % 58.70/58.77 [42]P11(x423,x422,x424)+~E(x421,x422)+~P11(x423,x421,x424) % 58.70/58.77 [43]P11(x433,x434,x432)+~E(x431,x432)+~P11(x433,x434,x431) % 58.70/58.77 [44]~P5(x441)+P5(x442)+~E(x441,x442) % 58.70/58.77 [45]~P8(x451)+P8(x452)+~E(x451,x452) % 58.70/58.77 % 58.70/58.77 %------------------------------------------- % 58.70/58.78 cnf(138,plain, % 58.70/58.78 (~P1(a17)), % 58.70/58.78 inference(scs_inference,[],[92,97])). % 58.70/58.78 cnf(140,plain, % 58.70/58.78 (~P6(x1401,a1)), % 58.70/58.78 inference(scs_inference,[],[92,48,97,106])). % 58.70/58.78 cnf(145,plain, % 58.70/58.78 (P2(f20(x1451),x1451)), % 58.70/58.78 inference(rename_variables,[],[79])). % 58.70/58.78 cnf(147,plain, % 58.70/58.78 (P9(f20(f26(x1471)),x1471)), % 58.70/58.78 inference(scs_inference,[],[77,92,48,79,145,97,106,116,123,117])). % 58.70/58.78 cnf(148,plain, % 58.70/58.78 (P2(f20(x1481),x1481)), % 58.70/58.78 inference(rename_variables,[],[79])). % 58.70/58.78 cnf(150,plain, % 58.70/58.78 (~P6(x1501,f20(f26(a1)))), % 58.70/58.78 inference(scs_inference,[],[77,92,48,79,145,148,97,106,116,123,117,121])). % 58.70/58.78 cnf(151,plain, % 58.70/58.78 (P2(f20(x1511),x1511)), % 58.70/58.78 inference(rename_variables,[],[79])). % 58.70/58.78 cnf(153,plain, % 58.70/58.78 (~E(a16,a1)), % 58.70/58.78 inference(scs_inference,[],[77,92,48,79,145,148,97,106,116,123,117,121,34])). % 58.70/58.78 cnf(154,plain, % 58.70/58.78 (P6(f20(a8),a8)), % 58.70/58.78 inference(scs_inference,[],[77,92,48,79,145,148,151,93,97,106,116,123,117,121,34,109])). % 58.70/58.78 cnf(173,plain, % 58.70/58.78 (P2(f10(x1731),f26(x1731))), % 58.70/58.78 inference(rename_variables,[],[80])). % 58.70/58.78 cnf(175,plain, % 58.70/58.78 (P9(f10(x1751),x1751)), % 58.70/58.78 inference(scs_inference,[],[80,173,123,117])). % 58.70/58.78 cnf(177,plain, % 58.70/58.78 (~P1(a16)), % 58.70/58.78 inference(scs_inference,[],[153,80,173,123,117,97])). % 58.70/58.78 cnf(179,plain, % 58.70/58.78 (~P6(x1791,a4)), % 58.70/58.78 inference(scs_inference,[],[153,49,80,173,123,117,97,106])). % 58.70/58.78 cnf(183,plain, % 58.70/58.78 (~P6(x1831,f10(a1))), % 58.70/58.78 inference(scs_inference,[],[153,48,154,49,80,173,123,117,97,106,116,121])). % 58.70/58.78 cnf(184,plain, % 58.70/58.78 (P2(f10(x1841),f26(x1841))), % 58.70/58.78 inference(rename_variables,[],[80])). % 58.70/58.78 cnf(188,plain, % 58.70/58.78 (P6(f20(a17),a17)), % 58.70/58.78 inference(scs_inference,[],[77,150,138,153,48,154,49,80,173,79,123,117,97,106,116,121,34,109])). % 58.70/58.78 cnf(194,plain, % 58.70/58.78 (P2(x1941,f26(x1942))+~E(f10(x1942),x1941)), % 58.70/58.78 inference(scs_inference,[],[86,77,150,138,153,48,154,49,80,173,184,79,123,117,97,106,116,121,34,109,31,32,33,37])). % 58.70/58.78 cnf(196,plain, % 58.70/58.78 (P9(x1961,x1962)+~E(x1962,x1961)), % 58.70/58.78 inference(scs_inference,[],[86,77,150,138,153,48,154,49,78,80,173,184,79,123,117,97,106,116,121,34,109,31,32,33,37,38,39])). % 58.70/58.78 cnf(203,plain, % 58.70/58.78 (~P6(x2031,a23)), % 58.70/58.78 inference(scs_inference,[],[50,106])). % 58.70/58.78 cnf(209,plain, % 58.70/58.78 (P6(f20(a16),a16)), % 58.70/58.78 inference(scs_inference,[],[77,183,177,188,50,79,106,116,34,109])). % 58.70/58.78 cnf(212,plain, % 58.70/58.78 (P9(f10(x2121),x2122)+~E(x2121,x2122)), % 58.70/58.78 inference(scs_inference,[],[77,183,177,188,50,175,79,106,116,34,109,40])). % 58.70/58.78 cnf(214,plain, % 58.70/58.78 (P11(f18(x2141,x2142),x2143,x2142)+~E(x2141,x2143)), % 58.70/58.78 inference(scs_inference,[],[77,183,177,188,50,175,89,79,106,116,34,109,40,41,42])). % 58.70/58.78 cnf(215,plain, % 58.70/58.78 (P11(f18(x2151,x2152),x2151,x2153)+~E(x2152,x2153)), % 58.70/58.78 inference(scs_inference,[],[77,183,177,188,50,175,89,79,106,116,34,109,40,41,42,43])). % 58.70/58.78 cnf(224,plain, % 58.70/58.78 (~P6(x2241,a24)), % 58.70/58.78 inference(scs_inference,[],[51,106])). % 58.70/58.78 cnf(228,plain, % 58.70/58.78 (P6(f20(a11),a11)), % 58.70/58.78 inference(scs_inference,[],[209,51,94,79,106,116,109])). % 58.70/58.78 cnf(233,plain, % 58.70/58.78 (P11(f22(x2331,x2332),x2333,x2332)+~E(x2331,x2333)), % 58.70/58.78 inference(scs_inference,[],[140,209,51,154,90,94,79,106,116,109,34,42])). % 58.70/58.78 cnf(236,plain, % 58.70/58.78 (P9(f20(f26(x2361)),x2362)+~E(x2361,x2362)), % 58.70/58.78 inference(scs_inference,[],[140,209,51,154,147,88,90,94,79,106,116,109,34,42,30,41,40])). % 58.70/58.78 cnf(237,plain, % 58.70/58.78 (P7(f22(x2371,x2372),x2371,x2373)+~E(x2372,x2373)), % 58.70/58.78 inference(scs_inference,[],[140,209,51,154,147,88,90,94,79,106,116,109,34,42,30,41,40,32])). % 58.70/58.78 cnf(238,plain, % 58.70/58.78 (P10(f21(x2381,x2382),x2381,x2383)+~E(x2382,x2383)), % 58.70/58.78 inference(scs_inference,[],[140,209,51,154,147,87,88,90,94,79,106,116,109,34,42,30,41,40,32,29])). % 58.70/58.78 cnf(245,plain, % 58.70/58.78 (~P6(x2451,f10(x2452))), % 58.70/58.78 inference(scs_inference,[],[76,106])). % 58.70/58.78 cnf(249,plain, % 58.70/58.78 (P6(f10(x2491),f26(x2491))), % 58.70/58.78 inference(scs_inference,[],[228,76,80,95,106,116,109])). % 58.70/58.78 cnf(256,plain, % 58.70/58.78 (P2(x2561,x2562)+~E(f20(x2562),x2561)), % 58.70/58.78 inference(scs_inference,[],[77,179,228,76,80,95,175,87,79,106,116,109,34,39,27,37])). % 58.70/58.78 cnf(257,plain, % 58.70/58.78 (P10(f21(x2571,x2572),x2573,x2572)+~E(x2571,x2573)), % 58.70/58.78 inference(scs_inference,[],[77,179,228,76,80,95,175,87,79,106,116,109,34,39,27,37,28])). % 58.70/58.78 cnf(258,plain, % 58.70/58.78 (P2(f20(x2581),x2582)+~E(x2581,x2582)), % 58.70/58.78 inference(scs_inference,[],[77,179,228,76,80,95,175,87,79,106,116,109,34,39,27,37,28,38])). % 58.70/58.78 cnf(259,plain, % 58.70/58.78 (P11(f9(x2591,x2592),x2591,x2593)+~E(x2592,x2593)), % 58.70/58.78 inference(scs_inference,[],[77,179,228,76,80,91,95,175,87,79,106,116,109,34,39,27,37,28,38,43])). % 58.70/58.78 cnf(270,plain, % 58.70/58.78 (P7(f22(x2701,x2702),x2703,x2702)+~E(x2701,x2703)), % 58.70/58.78 inference(scs_inference,[],[77,245,52,88,106,34,31])). % 58.70/58.78 cnf(272,plain, % 58.70/58.78 (P11(f9(x2721,x2722),x2723,x2722)+~E(x2721,x2723)), % 58.70/58.78 inference(scs_inference,[],[77,245,52,91,88,106,34,31,41,42])). % 58.70/58.78 cnf(280,plain, % 58.70/58.78 (P9(x2801,x2802)+~E(x2801,x2802)), % 58.70/58.78 inference(scs_inference,[],[77,203,78,147,34,39,40])). % 58.70/58.78 cnf(281,plain, % 58.70/58.78 (P11(f22(x2811,x2812),x2811,x2813)+~E(x2812,x2813)), % 58.70/58.78 inference(scs_inference,[],[77,203,78,147,90,34,39,40,43])). % 58.70/58.78 cnf(339,plain, % 58.70/58.78 (~P3(x3391)+~P4(x3391)+P5(x3391)+~P1(x3391)), % 58.70/58.78 inference(rename_variables,[],[104])). % 58.70/58.78 cnf(340,plain, % 58.70/58.78 (~P4(a14)+~P6(a15,f28(a14))), % 58.70/58.78 inference(scs_inference,[],[58,92,96,59,70,224,249,57,69,34,104,339,130,126])). % 58.70/58.78 cnf(398,plain, % 58.70/58.78 (P1(f27(a1,a1))), % 58.70/58.78 inference(scs_inference,[],[48,99,111])). % 58.70/58.78 cnf(399,plain, % 58.70/58.78 (~P6(x3991,f27(a1,a1))), % 58.70/58.78 inference(scs_inference,[],[398,106])). % 58.70/58.78 cnf(527,plain, % 58.70/58.78 (~P1(f25(a17))), % 58.70/58.78 inference(scs_inference,[],[92,103,97])). % 58.70/58.78 cnf(528,plain, % 58.70/58.78 (P6(f20(f25(a17)),f25(a17))), % 58.70/58.78 inference(scs_inference,[],[527,79,109])). % 58.70/58.78 cnf(533,plain, % 58.70/58.78 (~P6(f25(a17),f20(f25(a17)))), % 58.70/58.78 inference(scs_inference,[],[140,527,79,109,34,116])). % 58.70/58.78 cnf(578,plain, % 58.70/58.78 (E(f28(f18(x5781,x5782)),f29(x5781,x5782,f18(x5781,x5782)))), % 58.70/58.78 inference(scs_inference,[],[89,2,127])). % 58.70/58.78 cnf(579,plain, % 58.70/58.78 (E(f29(x5791,x5792,f18(x5791,x5792)),f28(f18(x5791,x5792)))), % 58.70/58.78 inference(scs_inference,[],[578,2])). % 58.70/58.78 cnf(645,plain, % 58.70/58.78 (~E(a16,f28(a14))+~P4(a14)), % 58.70/58.78 inference(scs_inference,[],[77,340,34])). % 58.70/58.78 cnf(661,plain, % 58.70/58.78 (~E(f28(a14),a16)+~P4(a14)), % 58.70/58.78 inference(scs_inference,[],[645,2])). % 58.70/58.78 cnf(677,plain, % 58.70/58.78 (~E(x6771,a16)+~E(f28(a14),x6771)+~P4(a14)), % 58.70/58.78 inference(scs_inference,[],[661,3])). % 58.70/58.78 cnf(693,plain, % 58.70/58.78 (P2(f25(a17),f26(a17))), % 58.70/58.78 inference(scs_inference,[],[92,107,97])). % 58.70/58.78 cnf(696,plain, % 58.70/58.78 (P6(f25(a17),f26(a17))), % 58.70/58.78 inference(scs_inference,[],[693,95,117,109])). % 58.70/58.78 cnf(702,plain, % 58.70/58.78 (~P6(f26(a17),f25(a17))), % 58.70/58.78 inference(scs_inference,[],[533,528,693,95,117,109,122,34,116])). % 58.70/58.78 cnf(732,plain, % 58.70/58.78 (~E(f26(a17),f25(a17))+~E(f25(a17),f26(a17))), % 58.70/58.78 inference(scs_inference,[],[702,527,696,79,109,122,33,34])). % 58.70/58.78 cnf(754,plain, % 58.70/58.78 (P2(f28(f18(x7541,x7542)),f26(f29(x7541,x7542,f18(x7541,x7542))))), % 58.70/58.78 inference(scs_inference,[],[579,110,196])). % 58.70/58.78 cnf(834,plain, % 58.70/58.78 (E(f29(a16,a17,a14),f28(a14))), % 58.70/58.78 inference(scs_inference,[],[85,125,127])). % 58.70/58.78 cnf(835,plain, % 58.70/58.78 (P7(f22(x8351,f29(a16,a17,a14)),x8351,f28(a14))), % 58.70/58.78 inference(scs_inference,[],[834,237])). % 58.70/58.78 cnf(836,plain, % 58.70/58.78 (P10(f21(x8361,f29(a16,a17,a14)),x8361,f28(a14))), % 58.70/58.78 inference(scs_inference,[],[834,237,238])). % 58.70/58.78 cnf(837,plain, % 58.70/58.78 (P10(f21(f29(a16,a17,a14),x8371),f28(a14),x8371)), % 58.70/58.78 inference(scs_inference,[],[834,237,238,257])). % 58.70/58.78 cnf(838,plain, % 58.70/58.78 (P7(f22(f29(a16,a17,a14),x8381),f28(a14),x8381)), % 58.70/58.78 inference(scs_inference,[],[834,237,238,257,270])). % 58.70/58.78 cnf(840,plain, % 58.70/58.78 (P11(f18(f29(a16,a17,a14),x8401),f28(a14),x8401)), % 58.70/58.78 inference(scs_inference,[],[834,237,238,257,270,212,214])). % 58.70/58.78 cnf(841,plain, % 58.70/58.78 (P11(f18(x8411,f29(a16,a17,a14)),x8411,f28(a14))), % 58.70/58.78 inference(scs_inference,[],[834,237,238,257,270,212,214,215])). % 58.70/58.78 cnf(842,plain, % 58.70/58.78 (P11(f22(f29(a16,a17,a14),x8421),f28(a14),x8421)), % 58.70/58.78 inference(scs_inference,[],[834,237,238,257,270,212,214,215,233])). % 58.70/58.78 cnf(843,plain, % 58.70/58.78 (P9(f20(f26(f29(a16,a17,a14))),f28(a14))), % 58.70/58.78 inference(scs_inference,[],[834,237,238,257,270,212,214,215,233,236])). % 58.70/58.78 cnf(845,plain, % 58.70/58.78 (P11(f9(x8451,f29(a16,a17,a14)),x8451,f28(a14))), % 58.70/58.78 inference(scs_inference,[],[834,237,238,257,270,212,214,215,233,236,258,259])). % 58.70/58.78 cnf(846,plain, % 58.70/58.78 (P11(f9(f29(a16,a17,a14),x8461),f28(a14),x8461)), % 58.70/58.78 inference(scs_inference,[],[834,237,238,257,270,212,214,215,233,236,258,259,272])). % 58.70/58.78 cnf(847,plain, % 58.70/58.78 (P11(f22(x8471,f29(a16,a17,a14)),x8471,f28(a14))), % 58.70/58.78 inference(scs_inference,[],[834,237,238,257,270,212,214,215,233,236,258,259,272,281])). % 58.70/58.78 cnf(848,plain, % 58.70/58.78 (P9(f28(a14),f29(a16,a17,a14))), % 58.70/58.78 inference(scs_inference,[],[834,237,238,257,270,212,214,215,233,236,258,259,272,281,196])). % 58.70/58.78 cnf(849,plain, % 58.70/58.78 (P9(f29(a16,a17,a14),f28(a14))), % 58.70/58.78 inference(scs_inference,[],[834,237,238,257,270,212,214,215,233,236,258,259,272,281,196,280])). % 58.70/58.78 cnf(850,plain, % 58.70/58.78 (E(f28(a14),f29(a16,a17,a14))), % 58.70/58.78 inference(scs_inference,[],[834,237,238,257,270,212,214,215,233,236,258,259,272,281,196,280,2])). % 58.70/58.78 cnf(862,plain, % 58.70/58.78 (P10(f21(x8621,f28(a14)),x8621,f29(a16,a17,a14))), % 58.70/58.78 inference(scs_inference,[],[850,238])). % 58.70/58.78 cnf(864,plain, % 58.70/58.78 (P11(f18(f28(a14),x8641),f29(a16,a17,a14),x8641)), % 58.70/58.78 inference(scs_inference,[],[850,238,258,214])). % 58.70/58.78 cnf(865,plain, % 58.70/58.78 (P11(f9(f28(a14),x8651),f29(a16,a17,a14),x8651)), % 58.70/58.78 inference(scs_inference,[],[850,238,258,214,272])). % 58.70/58.78 cnf(866,plain, % 58.70/58.78 (P7(f22(f28(a14),x8661),f29(a16,a17,a14),x8661)), % 58.70/58.78 inference(scs_inference,[],[850,238,258,214,272,270])). % 58.70/58.78 cnf(867,plain, % 58.70/58.78 (P7(f22(x8671,f28(a14)),x8671,f29(a16,a17,a14))), % 58.70/58.78 inference(scs_inference,[],[850,238,258,214,272,270,237])). % 58.70/58.78 cnf(868,plain, % 58.70/58.78 (P11(f22(f28(a14),x8681),f29(a16,a17,a14),x8681)), % 58.70/58.78 inference(scs_inference,[],[850,238,258,214,272,270,237,233])). % 58.70/58.78 cnf(869,plain, % 58.70/58.78 (P11(f18(x8691,f28(a14)),x8691,f29(a16,a17,a14))), % 58.70/58.78 inference(scs_inference,[],[850,238,258,214,272,270,237,233,215])). % 58.70/58.78 cnf(870,plain, % 58.70/58.78 (P11(f22(x8701,f28(a14)),x8701,f29(a16,a17,a14))), % 58.70/58.78 inference(scs_inference,[],[850,238,258,214,272,270,237,233,215,281])). % 58.70/58.78 cnf(871,plain, % 58.70/58.78 (P9(f10(f28(a14)),f29(a16,a17,a14))), % 58.70/58.78 inference(scs_inference,[],[850,238,258,214,272,270,237,233,215,281,212])). % 58.70/58.78 cnf(872,plain, % 58.70/58.78 (P11(f9(x8721,f28(a14)),x8721,f29(a16,a17,a14))), % 58.70/58.78 inference(scs_inference,[],[850,238,258,214,272,270,237,233,215,281,212,259])). % 58.70/58.78 cnf(873,plain, % 58.70/58.78 (P9(f20(f26(f28(a14))),f29(a16,a17,a14))), % 58.70/58.78 inference(scs_inference,[],[850,238,258,214,272,270,237,233,215,281,212,259,236])). % 58.70/58.78 cnf(874,plain, % 58.70/58.78 (P10(f21(f28(a14),x8741),f29(a16,a17,a14),x8741)), % 58.70/58.78 inference(scs_inference,[],[850,238,258,214,272,270,237,233,215,281,212,259,236,257])). % 58.70/58.78 cnf(877,plain, % 58.70/58.78 (P11(f9(f29(x8771,x8772,f18(x8771,x8772)),f29(a16,a17,a14)),f28(f18(x8771,x8772)),f29(a16,a17,a14))), % 58.70/58.78 inference(scs_inference,[],[579,850,845,238,258,214,272,270,237,233,215,281,212,259,236,257,42,43])). % 58.70/58.78 cnf(879,plain, % 58.70/58.78 (P10(f21(f29(x8791,x8792,f18(x8791,x8792)),f28(a14)),f28(f18(x8791,x8792)),f29(a16,a17,a14))), % 58.70/58.78 inference(scs_inference,[],[579,850,845,238,258,214,272,270,237,233,215,281,212,259,236,257,42,43,31,28])). % 58.70/58.78 cnf(887,plain, % 58.70/58.78 (P11(f22(f29(x8871,x8872,f18(x8871,x8872)),f29(a16,a17,a14)),f28(f18(x8871,x8872)),f28(a14))), % 58.70/58.78 inference(scs_inference,[],[579,847,42])). % 58.70/58.78 cnf(889,plain, % 58.70/58.78 (P11(f22(f29(x8891,x8892,f18(x8891,x8892)),f29(a16,a17,a14)),f28(f18(x8891,x8892)),f29(a16,a17,a14))), % 58.70/58.78 inference(scs_inference,[],[579,850,847,42,43])). % 58.70/58.78 cnf(898,plain, % 58.70/58.78 (P11(f18(f29(x8981,x8982,f18(x8981,x8982)),f28(a14)),f28(f18(x8981,x8982)),f28(a14))), % 58.70/58.78 inference(scs_inference,[],[579,869,834,42,43])). % 58.70/58.78 cnf(921,plain, % 58.70/58.78 (P11(f9(f29(x9211,x9212,f18(x9211,x9212)),f28(a14)),f28(f18(x9211,x9212)),f28(a14))), % 58.70/58.78 inference(scs_inference,[],[579,872,834,42,43])). % 58.70/58.78 cnf(933,plain, % 58.70/58.78 (P7(x9331,x9332,f28(a14))+~E(f22(x9332,f29(a16,a17,a14)),x9331)), % 58.70/58.78 inference(scs_inference,[],[835,843,39,30])). % 58.70/58.78 cnf(949,plain, % 58.70/58.78 (P10(x9491,x9492,f28(a14))+~E(f21(x9492,f29(a16,a17,a14)),x9491)), % 58.70/58.78 inference(scs_inference,[],[836,873,877,39,41,27])). % 58.70/58.78 cnf(960,plain, % 58.70/58.78 (P7(x9601,x9602,f29(a16,a17,a14))+~E(f22(x9602,f28(a14)),x9601)), % 58.70/58.78 inference(scs_inference,[],[879,867,871,887,39,41,27,30])). % 58.70/58.78 cnf(968,plain, % 58.70/58.78 (P7(x9681,f28(a14),x9682)+~E(f22(f29(a16,a17,a14),x9682),x9681)), % 58.70/58.78 inference(scs_inference,[],[838,889,41,30])). % 58.70/58.78 cnf(982,plain, % 58.70/58.78 (P7(x9821,f29(a16,a17,a14),x9822)+~E(f22(f28(a14),x9822),x9821)), % 58.70/58.78 inference(scs_inference,[],[866,898,41,30])). % 58.70/58.78 cnf(983,plain, % 58.70/58.78 (P10(x9831,x9832,f29(a16,a17,a14))+~E(f21(x9832,f28(a14)),x9831)), % 58.70/58.78 inference(scs_inference,[],[862,866,898,41,30,27])). % 58.70/58.78 cnf(1005,plain, % 58.70/58.78 (P10(x10051,f28(a14),x10052)+~E(f21(f29(a16,a17,a14),x10052),x10051)), % 58.70/58.78 inference(scs_inference,[],[837,921,41,27])). % 58.70/58.78 cnf(1010,plain, % 58.70/58.78 (P11(x10101,x10102,f28(a14))+~E(f18(x10102,f29(a16,a17,a14)),x10101)), % 58.70/58.78 inference(scs_inference,[],[841,41])). % 58.70/58.78 cnf(1022,plain, % 58.70/58.78 (P10(x10221,f29(a16,a17,a14),x10222)+~E(f21(f28(a14),x10222),x10221)), % 58.70/58.78 inference(scs_inference,[],[874,27])). % 58.70/58.78 cnf(1023,plain, % 58.70/58.78 (P10(x10231,f29(a16,a17,a14),f28(f18(x10232,x10233)))+~E(f21(f28(a14),f29(x10232,x10233,f18(x10232,x10233))),x10231)), % 58.70/58.78 inference(scs_inference,[],[579,874,27,29])). % 58.70/58.78 cnf(1027,plain, % 58.70/58.78 (P10(f21(f28(a14),f29(x10271,x10272,f18(x10271,x10272))),f29(a16,a17,a14),f28(f18(x10271,x10272)))), % 58.70/58.78 inference(equality_inference,[],[1023])). % 58.70/58.78 cnf(1028,plain, % 58.70/58.78 (P11(x10281,x10282,f28(a14))+~E(f9(x10282,f29(a16,a17,a14)),x10281)), % 58.70/58.78 inference(scs_inference,[],[845,41])). % 58.70/58.78 cnf(1032,plain, % 58.70/58.78 (P11(x10321,x10322,f28(a14))+~E(f22(x10322,f29(a16,a17,a14)),x10321)), % 58.70/58.78 inference(scs_inference,[],[847,41])). % 58.70/58.78 cnf(1036,plain, % 58.70/58.78 (P11(x10361,x10362,f29(a16,a17,a14))+~E(f18(x10362,f28(a14)),x10361)), % 58.70/58.78 inference(scs_inference,[],[869,41])). % 58.70/58.78 cnf(1040,plain, % 58.70/58.78 (P11(x10401,x10402,f29(a16,a17,a14))+~E(f22(x10402,f28(a14)),x10401)), % 58.70/58.78 inference(scs_inference,[],[870,41])). % 58.70/58.78 cnf(1044,plain, % 58.70/58.78 (P11(x10441,x10442,f29(a16,a17,a14))+~E(f9(x10442,f28(a14)),x10441)), % 58.70/58.78 inference(scs_inference,[],[872,41])). % 58.70/58.78 cnf(1048,plain, % 58.70/58.78 (P11(x10481,f28(a14),x10482)+~E(f18(f29(a16,a17,a14),x10482),x10481)), % 58.70/58.78 inference(scs_inference,[],[840,41])). % 58.70/58.78 cnf(1049,plain, % 58.70/58.78 (P11(x10491,f28(a14),f28(f18(x10492,x10493)))+~E(f18(f29(a16,a17,a14),f29(x10492,x10493,f18(x10492,x10493))),x10491)), % 58.70/58.78 inference(scs_inference,[],[579,840,41,43])). % 58.70/58.78 cnf(1053,plain, % 58.70/58.78 (P11(f18(f29(a16,a17,a14),f29(x10531,x10532,f18(x10531,x10532))),f28(a14),f28(f18(x10531,x10532)))), % 58.70/58.78 inference(equality_inference,[],[1049])). % 58.70/58.78 cnf(1055,plain, % 58.70/58.78 (P11(x10551,f28(a14),x10552)+~E(f22(f29(a16,a17,a14),x10552),x10551)), % 58.70/58.78 inference(scs_inference,[],[842,41])). % 58.70/58.78 cnf(1056,plain, % 58.70/58.78 (P11(x10561,f28(a14),f28(f18(x10562,x10563)))+~E(f22(f29(a16,a17,a14),f29(x10562,x10563,f18(x10562,x10563))),x10561)), % 58.70/58.78 inference(scs_inference,[],[579,842,41,43])). % 58.70/58.78 cnf(1062,plain, % 58.70/58.78 (P11(x10621,f28(a14),x10622)+~E(f9(f29(a16,a17,a14),x10622),x10621)), % 58.70/58.78 inference(scs_inference,[],[846,41])). % 58.70/58.78 cnf(1068,plain, % 58.70/58.78 (P11(x10681,f29(a16,a17,a14),x10682)+~E(f18(f28(a14),x10682),x10681)), % 58.70/58.78 inference(scs_inference,[],[864,41])). % 58.70/58.78 cnf(1073,plain, % 58.70/58.78 (P11(x10731,f29(a16,a17,a14),x10732)+~E(f9(f28(a14),x10732),x10731)), % 58.70/58.78 inference(scs_inference,[],[865,41])). % 58.70/58.78 cnf(1081,plain, % 58.70/58.78 (P11(x10811,f29(a16,a17,a14),x10812)+~E(f22(f28(a14),x10812),x10811)), % 58.70/58.78 inference(scs_inference,[],[868,41])). % 58.70/58.78 cnf(1213,plain, % 58.70/58.78 (P11(f9(f29(a16,a17,a14),f28(a14)),f28(a14),f29(a16,a17,a14))), % 58.70/58.78 inference(scs_inference,[],[850,846,43])). % 58.70/58.78 cnf(1215,plain, % 58.70/58.78 (P10(f21(f29(a16,a17,a14),f28(a14)),f28(a14),f29(a16,a17,a14))), % 58.70/58.78 inference(scs_inference,[],[850,837,846,43,29])). % 58.70/58.78 cnf(2089,plain, % 58.70/58.78 (~E(f26(a17),f25(a17))), % 58.70/58.78 inference(scs_inference,[],[732,2])). % 58.70/58.78 cnf(2363,plain, % 58.70/58.78 (P2(f29(a16,a17,a14),f26(a16))), % 58.70/58.78 inference(scs_inference,[],[85,131,125])). % 58.70/58.78 cnf(2366,plain, % 58.70/58.78 (P2(f28(a14),f26(a16))), % 58.70/58.78 inference(scs_inference,[],[834,2363,117,37])). % 58.70/58.78 cnf(2454,plain, % 58.70/58.78 (P6(f28(a14),f26(a16))), % 58.70/58.78 inference(scs_inference,[],[2366,95,109])). % 58.70/58.78 cnf(3331,plain, % 58.70/58.78 (~P1(f25(a8))), % 58.70/58.78 inference(scs_inference,[],[93,103])). % 58.70/58.78 cnf(3373,plain, % 58.70/58.78 (P1(f28(f27(a1,a1)))), % 58.70/58.78 inference(scs_inference,[],[1027,848,1213,1215,398,93,90,77,834,103,110,125,107,4,5,9,24,25,129,10,11,12,13,14,15,16,17,18,19,20,21,22,23,127,131,6,7,8,1049,1056,108,102,101])). % 58.70/58.78 cnf(3379,plain, % 58.70/58.78 (E(f27(a1,a1),a1)), % 58.70/58.78 inference(scs_inference,[],[1027,848,1213,1215,398,93,90,77,834,103,110,125,107,4,5,9,24,25,129,10,11,12,13,14,15,16,17,18,19,20,21,22,23,127,131,6,7,8,1049,1056,108,102,101,98,99,97])). % 58.70/58.78 cnf(3388,plain, % 58.70/58.78 (P4(f27(a4,f27(a1,a1)))), % 58.70/58.78 inference(scs_inference,[],[63,2089,1027,1053,848,1213,1215,398,93,90,77,834,103,110,125,107,4,5,9,24,25,129,10,11,12,13,14,15,16,17,18,19,20,21,22,23,127,131,6,7,8,1049,1056,108,102,101,98,99,97,2,124,111,112,113])). % 58.70/58.78 cnf(3394,plain, % 58.70/58.78 (~P1(f3(a8,a8))), % 58.70/58.78 inference(scs_inference,[],[63,2089,1027,1053,848,1213,1215,398,93,90,77,834,103,110,125,107,4,5,9,24,25,129,10,11,12,13,14,15,16,17,18,19,20,21,22,23,127,131,6,7,8,1049,1056,108,102,101,98,99,97,2,124,111,112,113,114,115,118])). % 58.70/58.78 cnf(3403,plain, % 58.70/58.78 (P6(f10(f29(a16,a17,a14)),f26(f28(a14)))), % 58.70/58.78 inference(scs_inference,[],[63,66,2089,1027,1053,754,848,1213,1215,398,93,95,90,249,77,834,103,110,125,107,4,5,9,24,25,129,10,11,12,13,14,15,16,17,18,19,20,21,22,23,127,131,6,7,8,1049,1056,108,102,101,98,99,97,2,124,111,112,113,114,115,118,3,35,105,109,34])). % 58.70/58.78 cnf(3407,plain, % 58.70/58.78 (~E(f27(a1,a1),a8)), % 58.70/58.78 inference(scs_inference,[],[63,66,2089,1027,1053,754,848,1213,1215,2454,398,93,95,90,249,77,834,103,110,125,107,4,5,9,24,25,129,10,11,12,13,14,15,16,17,18,19,20,21,22,23,127,131,6,7,8,1049,1056,108,102,101,98,99,97,2,124,111,112,113,114,115,118,3,35,105,109,34,121,26])). % 58.70/58.78 cnf(3412,plain, % 58.70/58.78 (~E(f20(f26(f27(a1,a1))),f26(a16))), % 58.70/58.78 inference(scs_inference,[],[63,66,2089,1027,1053,754,54,848,1213,1215,2454,398,93,95,90,249,77,834,103,110,125,107,4,5,9,24,25,129,10,11,12,13,14,15,16,17,18,19,20,21,22,23,127,131,6,7,8,1049,1056,108,102,101,98,99,97,2,124,111,112,113,114,115,118,3,35,105,109,34,121,26,104,119,256])). % 58.70/58.78 cnf(3416,plain, % 58.70/58.78 (~E(f29(a16,a17,a14),a16)+~P4(a14)), % 58.70/58.78 inference(scs_inference,[],[63,66,2089,1027,1053,754,54,848,1213,1215,2454,398,93,95,90,249,77,834,850,103,110,125,107,4,5,9,24,25,129,10,11,12,13,14,15,16,17,18,19,20,21,22,23,127,131,6,7,8,1049,1056,108,102,101,98,99,97,2,124,111,112,113,114,115,118,3,35,105,109,34,121,26,104,119,256,194,116,677])). % 58.70/58.78 cnf(3421,plain, % 58.70/58.78 (E(f28(f18(x34211,x34212)),f29(x34211,x34212,f18(x34211,x34212)))), % 58.70/58.78 inference(rename_variables,[],[578])). % 58.70/58.78 cnf(3424,plain, % 58.70/58.78 (P10(f21(f28(f18(x34241,x34242)),f28(a14)),f29(x34241,x34242,f18(x34241,x34242)),f29(a16,a17,a14))), % 58.70/58.78 inference(scs_inference,[],[63,66,2089,1027,1053,754,54,848,1213,1215,2454,398,93,862,867,95,90,249,79,578,3421,77,834,850,103,110,125,107,4,5,9,24,25,129,10,11,12,13,14,15,16,17,18,19,20,21,22,23,127,131,6,7,8,1049,1056,108,102,101,98,99,97,2,124,111,112,113,114,115,118,3,35,105,109,34,121,26,104,119,256,194,116,677,38,37,31,28])). % 58.70/58.78 cnf(3428,plain, % 58.70/58.78 (P11(f18(f10(f29(a16,a17,a14)),f28(a14)),f10(f28(a14)),f29(a16,a17,a14))), % 58.70/58.78 inference(scs_inference,[],[63,66,2089,1027,1053,754,54,848,1213,1215,2454,398,93,865,862,867,869,95,90,249,79,578,3421,77,834,850,103,110,125,107,4,5,9,24,25,129,10,11,12,13,14,15,16,17,18,19,20,21,22,23,127,131,6,7,8,1049,1056,108,102,101,98,99,97,2,124,111,112,113,114,115,118,3,35,105,109,34,121,26,104,119,256,194,116,677,38,37,31,28,43,42])). % 58.70/58.78 cnf(3455,plain, % 58.70/58.78 (E(f9(f27(a1,a1),x34551),f9(a1,x34551))), % 58.70/58.78 inference(scs_inference,[],[3331,3379,3424,849,870,91,127,131,125,103,107,110,20,12])). % 58.70/58.78 cnf(3458,plain, % 58.70/58.78 (E(f22(f27(a1,a1),x34581),f22(a1,x34581))), % 58.70/58.78 inference(scs_inference,[],[3331,3379,3424,849,870,91,127,131,125,103,107,110,20,12,24,14,10])). % 58.70/58.78 cnf(3465,plain, % 58.70/58.78 (E(f22(x34651,f27(a1,a1)),f22(x34651,a1))), % 58.70/58.78 inference(scs_inference,[],[3331,3379,3373,3424,849,870,91,127,131,125,103,107,110,20,12,24,14,10,102,17,6,101,11])). % 58.70/58.78 cnf(3473,plain, % 58.70/58.78 (E(f21(f27(a1,a1),x34731),f21(a1,x34731))), % 58.70/58.78 inference(scs_inference,[],[3331,3379,3373,3403,3424,849,870,87,91,127,131,125,103,107,110,20,12,24,14,10,102,17,6,101,11,129,5,98,108,18])). % 58.70/58.78 cnf(3482,plain, % 58.70/58.78 (E(f18(f27(a1,a1),x34821),f18(a1,x34821))), % 58.70/58.78 inference(scs_inference,[],[3331,3379,3373,3403,3424,849,76,870,87,91,127,131,125,103,107,110,20,12,24,14,10,102,17,6,101,11,129,5,98,108,18,7,99,15,4,21,16,8,22])). % 58.70/58.78 cnf(3483,plain, % 58.70/58.78 (E(f9(x34831,f27(a1,a1)),f9(x34831,a1))), % 58.70/58.78 inference(scs_inference,[],[3331,3379,3373,3403,3424,849,76,870,87,91,127,131,125,103,107,110,20,12,24,14,10,102,17,6,101,11,129,5,98,108,18,7,99,15,4,21,16,8,22,13])). % 58.70/58.78 cnf(3485,plain, % 58.70/58.78 (E(f21(x34851,f27(a1,a1)),f21(x34851,a1))), % 58.70/58.78 inference(scs_inference,[],[3331,3379,3373,3403,3424,849,76,870,87,91,127,131,125,103,107,110,20,12,24,14,10,102,17,6,101,11,129,5,98,108,18,7,99,15,4,21,16,8,22,13,25,19])). % 58.70/58.78 cnf(3486,plain, % 58.70/58.78 (E(f18(x34861,f27(a1,a1)),f18(x34861,a1))), % 58.70/58.78 inference(scs_inference,[],[3331,3379,3373,3403,3424,849,76,870,87,91,127,131,125,103,107,110,20,12,24,14,10,102,17,6,101,11,129,5,98,108,18,7,99,15,4,21,16,8,22,13,25,19,23])). % 58.70/58.78 cnf(3505,plain, % 58.70/58.78 (P1(f20(f26(a1)))), % 58.70/58.78 inference(scs_inference,[],[64,3331,3379,3373,3403,3424,3428,3412,849,76,870,87,150,91,79,127,131,125,103,107,110,20,12,24,14,10,102,17,6,101,11,129,5,98,108,18,7,99,15,4,21,16,8,22,13,25,19,23,9,97,2,124,113,111,114,118,115,112,109])). % 58.70/58.78 cnf(3515,plain, % 58.70/58.78 (E(f29(a16,a17,a14),a16)), % 58.70/58.78 inference(scs_inference,[],[64,3331,3379,3407,3388,3373,3403,3424,3428,3412,849,76,870,87,399,150,91,79,85,86,92,127,131,125,103,107,110,20,12,24,14,10,102,17,6,101,11,129,5,98,108,18,7,99,15,4,21,16,8,22,13,25,19,23,9,97,2,124,113,111,114,118,115,112,109,3,34,36,121,26,132])). % 58.70/58.78 cnf(3523,plain, % 58.70/58.78 (P10(f21(a1,f28(a14)),f27(a1,a1),f29(a16,a17,a14))), % 58.70/58.78 inference(scs_inference,[],[64,3331,3379,3407,3388,3373,3403,3424,3428,3412,849,76,870,87,399,150,91,79,85,86,92,127,131,125,103,107,110,20,12,24,14,10,102,17,6,101,11,129,5,98,108,18,7,99,15,4,21,16,8,22,13,25,19,23,9,97,2,124,113,111,114,118,115,112,109,3,34,36,121,26,132,3416,960,1036,1040,1044,982,983])). % 58.70/58.78 cnf(3528,plain, % 58.70/58.78 (~P2(a14,f26(f3(x35281,x35282)))), % 58.70/58.78 inference(scs_inference,[],[64,3331,3379,3407,3388,3373,3403,3424,3428,3412,849,76,870,87,399,150,91,79,85,86,92,127,131,125,103,107,110,20,12,24,14,10,102,17,6,101,11,129,5,98,108,18,7,99,15,4,21,16,8,22,13,25,19,23,9,97,2,124,113,111,114,118,115,112,109,3,34,36,121,26,132,3416,960,1036,1040,1044,982,983,1022,1062,1068,1081,123])). % 58.70/58.78 cnf(3548,plain, % 58.70/58.78 (E(f22(f27(a1,a1),x35481),f22(a1,x35481))), % 58.70/58.78 inference(rename_variables,[],[3458])). % 58.70/58.78 cnf(3558,plain, % 58.70/58.78 (E(f22(x35581,f27(a1,a1)),f22(x35581,a1))), % 58.70/58.78 inference(rename_variables,[],[3465])). % 58.70/58.78 cnf(3584,plain, % 58.70/58.78 ($false), % 58.70/58.78 inference(scs_inference,[],[3394,3515,3455,3458,3548,3465,3558,3473,3482,3483,3485,3486,3523,3505,3528,871,841,85,1073,933,1010,1028,1032,949,968,1005,1048,1055,125,103,131,110,101,102,107,98,256,12,10,129]), % 58.70/58.78 ['proof']). % 58.70/58.78 % SZS output end Proof % 58.70/58.78 % Total time :58.120000s %------------------------------------------------------------------------------