%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : NUM409+1 : TPTP v8.2.0. Released v3.2.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n019.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 12:24:07 EDT 2024 % Result : Theorem 58.84s 58.91s % Output : CNFRefutation 58.84s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : NUM409+1 : TPTP v8.2.0. Released v3.2.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.34 % Computer : n019.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.35 % CPULimit : 300 % 0.12/0.35 % WCLimit : 300 % 0.12/0.35 % DateTime : Sun Jun 23 03:46:39 EDT 2024 % 0.12/0.35 % CPUTime : % 0.55/0.57 start to proof:theBenchmark % 58.84/58.89 %------------------------------------------- % 58.84/58.89 % File :CSE---1.7 % 58.84/58.89 % Problem :theBenchmark % 58.84/58.89 % Transform :cnf % 58.84/58.89 % Format :tptp:raw % 58.84/58.89 % Command :java -jar mcs_scs.jar %d %s % 58.84/58.89 % 58.84/58.89 % Result :Theorem 58.270000s % 58.84/58.89 % Output :CNFRefutation 58.270000s % 58.84/58.89 %------------------------------------------- % 58.84/58.90 %------------------------------------------------------------------------------ % 58.84/58.90 % File : NUM409+1 : TPTP v8.2.0. Released v3.2.0. % 58.84/58.90 % Domain : Number Theory (Ordinals) % 58.84/58.90 % Problem : Ordinal numbers, theorem 45 % 58.84/58.90 % Version : [Urb06] axioms : Especial. % 58.84/58.90 % English : % 58.84/58.90 % 58.84/58.90 % Refs : [Ban90] Bancerek (1990), The Ordinal Numbers % 58.84/58.90 % [Urb06] Urban (2006), Email to G. Sutcliffe % 58.84/58.90 % Source : [Urb06] % 58.84/58.90 % Names : ordinal1__t45_ordinal1 [Urb06] % 58.84/58.90 % 58.84/58.90 % Status : Theorem % 58.84/58.90 % Rating : 0.17 v7.5.0, 0.19 v7.4.0, 0.10 v7.3.0, 0.07 v7.1.0, 0.09 v7.0.0, 0.07 v6.4.0, 0.12 v6.3.0, 0.17 v6.2.0, 0.24 v6.1.0, 0.30 v6.0.0, 0.26 v5.4.0, 0.32 v5.3.0, 0.33 v5.2.0, 0.10 v5.1.0, 0.14 v5.0.0, 0.25 v4.1.0, 0.30 v4.0.1, 0.39 v4.0.0, 0.38 v3.7.0, 0.20 v3.5.0, 0.21 v3.3.0, 0.14 v3.2.0 % 58.84/58.90 % Syntax : Number of formulae : 51 ( 11 unt; 0 def) % 58.84/58.90 % Number of atoms : 139 ( 7 equ) % 58.84/58.90 % Maximal formula atoms : 8 ( 2 avg) % 58.84/58.90 % Number of connectives : 101 ( 13 ~; 1 |; 60 &) % 58.84/58.90 % ( 6 <=>; 21 =>; 0 <=; 0 <~>) % 58.84/58.90 % Maximal formula depth : 8 ( 4 avg) % 58.84/58.90 % Maximal term depth : 3 ( 1 avg) % 58.84/58.90 % Number of predicates : 16 ( 15 usr; 0 prp; 1-2 aty) % 58.84/58.90 % Number of functors : 7 ( 7 usr; 1 con; 0-2 aty) % 58.84/58.90 % Number of variables : 68 ( 51 !; 17 ?) % 58.84/58.90 % SPC : FOF_THM_RFO_SEQ % 58.84/58.90 % 58.84/58.90 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 58.84/58.90 % library, www.mizar.org % 58.84/58.90 %------------------------------------------------------------------------------ % 58.84/58.90 fof(antisymmetry_r2_hidden,axiom, % 58.84/58.90 ! [A,B] : % 58.84/58.90 ( in(A,B) % 58.84/58.90 => ~ in(B,A) ) ). % 58.84/58.90 % 58.84/58.90 fof(cc1_funct_1,axiom, % 58.84/58.90 ! [A] : % 58.84/58.90 ( empty(A) % 58.84/58.90 => function(A) ) ). % 58.84/58.90 % 58.84/58.90 fof(cc1_ordinal1,axiom, % 58.84/58.90 ! [A] : % 58.84/58.90 ( ordinal(A) % 58.84/58.90 => ( epsilon_transitive(A) % 58.84/58.90 & epsilon_connected(A) ) ) ). % 58.84/58.90 % 58.84/58.90 fof(cc1_relat_1,axiom, % 58.84/58.90 ! [A] : % 58.84/58.90 ( empty(A) % 58.84/58.90 => relation(A) ) ). % 58.84/58.90 % 58.84/58.90 fof(cc2_funct_1,axiom, % 58.84/58.90 ! [A] : % 58.84/58.90 ( ( relation(A) % 58.84/58.90 & empty(A) % 58.84/58.90 & function(A) ) % 58.84/58.90 => ( relation(A) % 58.84/58.90 & function(A) % 58.84/58.90 & one_to_one(A) ) ) ). % 58.84/58.90 % 58.84/58.90 fof(cc2_ordinal1,axiom, % 58.84/58.90 ! [A] : % 58.84/58.90 ( ( epsilon_transitive(A) % 58.84/58.90 & epsilon_connected(A) ) % 58.84/58.90 => ordinal(A) ) ). % 58.84/58.90 % 58.84/58.90 fof(cc3_ordinal1,axiom, % 58.84/58.90 ! [A] : % 58.84/58.90 ( empty(A) % 58.84/58.90 => ( epsilon_transitive(A) % 58.84/58.90 & epsilon_connected(A) % 58.84/58.90 & ordinal(A) ) ) ). % 58.84/58.90 % 58.84/58.90 fof(commutativity_k2_tarski,axiom, % 58.84/58.90 ! [A,B] : unordered_pair(A,B) = unordered_pair(B,A) ). % 58.84/58.90 % 58.84/58.90 fof(d4_relat_1,axiom, % 58.84/58.90 ! [A] : % 58.84/58.90 ( relation(A) % 58.84/58.90 => ! [B] : % 58.84/58.90 ( B = relation_dom(A) % 58.84/58.90 <=> ! [C] : % 58.84/58.90 ( in(C,B) % 58.84/58.90 <=> ? [D] : in(ordered_pair(C,D),A) ) ) ) ). % 58.84/58.90 % 58.84/58.90 fof(d5_tarski,axiom, % 58.84/58.90 ! [A,B] : ordered_pair(A,B) = unordered_pair(unordered_pair(A,B),singleton(A)) ). % 58.84/58.90 % 58.84/58.90 fof(d7_ordinal1,axiom, % 58.84/58.90 ! [A] : % 58.84/58.90 ( ( relation(A) % 58.84/58.90 & function(A) ) % 58.84/58.90 => ( transfinite_sequence(A) % 58.84/58.90 <=> ordinal(relation_dom(A)) ) ) ). % 58.84/58.90 % 58.84/58.90 fof(d8_ordinal1,axiom, % 58.84/58.90 ! [A,B] : % 58.84/58.90 ( ( relation(B) % 58.84/58.90 & function(B) % 58.84/58.90 & transfinite_sequence(B) ) % 58.84/58.90 => ( transfinite_sequence_of(B,A) % 58.84/58.90 <=> subset(relation_rng(B),A) ) ) ). % 58.84/58.90 % 58.84/58.90 fof(dt_m1_ordinal1,axiom, % 58.84/58.90 ! [A,B] : % 58.84/58.90 ( transfinite_sequence_of(B,A) % 58.84/58.90 => ( relation(B) % 58.84/58.90 & function(B) % 58.84/58.90 & transfinite_sequence(B) ) ) ). % 58.84/58.90 % 58.84/58.90 fof(existence_m1_ordinal1,axiom, % 58.84/58.90 ! [A] : % 58.84/58.90 ? [B] : transfinite_sequence_of(B,A) ). % 58.84/58.90 % 58.84/58.90 fof(existence_m1_subset_1,axiom, % 58.84/58.90 ! [A] : % 58.84/58.90 ? [B] : element(B,A) ). % 58.84/58.90 % 58.84/58.90 fof(fc12_relat_1,axiom, % 58.84/58.90 ( empty(empty_set) % 58.84/58.90 & relation(empty_set) % 58.84/58.90 & relation_empty_yielding(empty_set) ) ). % 58.84/58.90 % 58.84/58.90 fof(fc1_xboole_0,axiom, % 58.84/58.90 empty(empty_set) ). % 58.84/58.90 % 58.84/58.90 fof(fc1_zfmisc_1,axiom, % 58.84/58.90 ! [A,B] : ~ empty(ordered_pair(A,B)) ). % 58.84/58.90 % 58.84/58.90 fof(fc2_ordinal1,axiom, % 58.84/58.90 ( relation(empty_set) % 58.84/58.90 & relation_empty_yielding(empty_set) % 58.84/58.90 & function(empty_set) % 58.84/58.90 & one_to_one(empty_set) % 58.84/58.90 & empty(empty_set) % 58.84/58.90 & epsilon_transitive(empty_set) % 58.84/58.90 & epsilon_connected(empty_set) % 58.84/58.90 & ordinal(empty_set) ) ). % 58.84/58.90 % 58.84/58.90 fof(fc4_relat_1,axiom, % 58.84/58.90 ( empty(empty_set) % 58.84/58.90 & relation(empty_set) ) ). % 58.84/58.91 % 58.84/58.91 fof(fc5_relat_1,axiom, % 58.84/58.91 ! [A] : % 58.84/58.91 ( ( ~ empty(A) % 58.84/58.91 & relation(A) ) % 58.84/58.91 => ~ empty(relation_dom(A)) ) ). % 58.84/58.91 % 58.84/58.91 fof(fc6_funct_1,axiom, % 58.84/58.91 ! [A] : % 58.84/58.91 ( ( relation(A) % 58.84/58.91 & relation_non_empty(A) % 58.84/58.91 & function(A) ) % 58.84/58.91 => with_non_empty_elements(relation_rng(A)) ) ). % 58.84/58.91 % 58.84/58.91 fof(fc6_relat_1,axiom, % 58.84/58.91 ! [A] : % 58.84/58.91 ( ( ~ empty(A) % 58.84/58.91 & relation(A) ) % 58.84/58.91 => ~ empty(relation_rng(A)) ) ). % 58.84/58.91 % 58.84/58.91 fof(fc7_relat_1,axiom, % 58.84/58.91 ! [A] : % 58.84/58.91 ( empty(A) % 58.84/58.91 => ( empty(relation_dom(A)) % 58.84/58.91 & relation(relation_dom(A)) ) ) ). % 58.84/58.91 % 58.84/58.91 fof(fc8_relat_1,axiom, % 58.84/58.91 ! [A] : % 58.84/58.91 ( empty(A) % 58.84/58.91 => ( empty(relation_rng(A)) % 58.84/58.91 & relation(relation_rng(A)) ) ) ). % 58.84/58.91 % 58.84/58.91 fof(rc1_funct_1,axiom, % 58.84/58.91 ? [A] : % 58.84/58.91 ( relation(A) % 58.84/58.91 & function(A) ) ). % 58.84/58.91 % 58.84/58.91 fof(rc1_ordinal1,axiom, % 58.84/58.91 ? [A] : % 58.84/58.91 ( epsilon_transitive(A) % 58.84/58.91 & epsilon_connected(A) % 58.84/58.91 & ordinal(A) ) ). % 58.84/58.91 % 58.84/58.91 fof(rc1_relat_1,axiom, % 58.84/58.91 ? [A] : % 58.84/58.91 ( empty(A) % 58.84/58.91 & relation(A) ) ). % 58.84/58.91 % 58.84/58.91 fof(rc1_xboole_0,axiom, % 58.84/58.91 ? [A] : empty(A) ). % 58.84/58.91 % 58.84/58.91 fof(rc2_funct_1,axiom, % 58.84/58.91 ? [A] : % 58.84/58.91 ( relation(A) % 58.84/58.91 & empty(A) % 58.84/58.91 & function(A) ) ). % 58.84/58.91 % 58.84/58.91 fof(rc2_ordinal1,axiom, % 58.84/58.91 ? [A] : % 58.84/58.91 ( relation(A) % 58.84/58.91 & function(A) % 58.84/58.91 & one_to_one(A) % 58.84/58.91 & empty(A) % 58.84/58.91 & epsilon_transitive(A) % 58.84/58.91 & epsilon_connected(A) % 58.84/58.91 & ordinal(A) ) ). % 58.84/58.91 % 58.84/58.91 fof(rc2_relat_1,axiom, % 58.84/58.91 ? [A] : % 58.84/58.91 ( ~ empty(A) % 58.84/58.91 & relation(A) ) ). % 58.84/58.91 % 58.84/58.91 fof(rc2_xboole_0,axiom, % 58.84/58.91 ? [A] : ~ empty(A) ). % 58.84/58.91 % 58.84/58.91 fof(rc3_funct_1,axiom, % 58.84/58.91 ? [A] : % 58.84/58.91 ( relation(A) % 58.84/58.91 & function(A) % 58.84/58.91 & one_to_one(A) ) ). % 58.84/58.91 % 58.84/58.91 fof(rc3_ordinal1,axiom, % 58.84/58.91 ? [A] : % 58.84/58.91 ( ~ empty(A) % 58.84/58.91 & epsilon_transitive(A) % 58.84/58.91 & epsilon_connected(A) % 58.84/58.91 & ordinal(A) ) ). % 58.84/58.91 % 58.84/58.91 fof(rc3_relat_1,axiom, % 58.84/58.91 ? [A] : % 58.84/58.91 ( relation(A) % 58.84/58.91 & relation_empty_yielding(A) ) ). % 58.84/58.91 % 58.84/58.91 fof(rc4_funct_1,axiom, % 58.84/58.91 ? [A] : % 58.84/58.91 ( relation(A) % 58.84/58.91 & relation_empty_yielding(A) % 58.84/58.91 & function(A) ) ). % 58.84/58.91 % 58.84/58.91 fof(rc4_ordinal1,axiom, % 58.84/58.91 ? [A] : % 58.84/58.91 ( relation(A) % 58.84/58.91 & function(A) % 58.84/58.91 & transfinite_sequence(A) ) ). % 58.84/58.91 % 58.84/58.91 fof(rc5_funct_1,axiom, % 58.84/58.91 ? [A] : % 58.84/58.91 ( relation(A) % 58.84/58.91 & relation_non_empty(A) % 58.84/58.91 & function(A) ) ). % 58.84/58.91 % 58.84/58.91 fof(reflexivity_r1_tarski,axiom, % 58.84/58.91 ! [A,B] : subset(A,A) ). % 58.84/58.91 % 58.84/58.91 fof(t1_subset,axiom, % 58.84/58.91 ! [A,B] : % 58.84/58.91 ( in(A,B) % 58.84/58.91 => element(A,B) ) ). % 58.84/58.91 % 58.84/58.91 fof(t2_subset,axiom, % 58.84/58.91 ! [A,B] : % 58.84/58.91 ( element(A,B) % 58.84/58.91 => ( empty(B) % 58.84/58.91 | in(A,B) ) ) ). % 58.84/58.91 % 58.84/58.91 fof(t2_xboole_1,axiom, % 58.84/58.91 ! [A] : subset(empty_set,A) ). % 58.84/58.91 % 58.84/58.91 fof(t3_subset,axiom, % 58.84/58.91 ! [A,B] : % 58.84/58.91 ( element(A,powerset(B)) % 58.84/58.91 <=> subset(A,B) ) ). % 58.84/58.91 % 58.84/58.91 fof(t45_ordinal1,conjecture, % 58.84/58.91 ! [A] : transfinite_sequence_of(empty_set,A) ). % 58.84/58.91 % 58.84/58.91 fof(t4_subset,axiom, % 58.84/58.91 ! [A,B,C] : % 58.84/58.91 ( ( in(A,B) % 58.84/58.91 & element(B,powerset(C)) ) % 58.84/58.91 => element(A,C) ) ). % 58.84/58.91 % 58.84/58.91 fof(t5_subset,axiom, % 58.84/58.91 ! [A,B,C] : % 58.84/58.91 ~ ( in(A,B) % 58.84/58.91 & element(B,powerset(C)) % 58.84/58.91 & empty(C) ) ). % 58.84/58.91 % 58.84/58.91 fof(t65_relat_1,axiom, % 58.84/58.91 ! [A] : % 58.84/58.91 ( relation(A) % 58.84/58.91 => ( relation_dom(A) = empty_set % 58.84/58.91 <=> relation_rng(A) = empty_set ) ) ). % 58.84/58.91 % 58.84/58.91 fof(t6_boole,axiom, % 58.84/58.91 ! [A] : % 58.84/58.91 ( empty(A) % 58.84/58.91 => A = empty_set ) ). % 58.84/58.91 % 58.84/58.91 fof(t7_boole,axiom, % 58.84/58.91 ! [A,B] : % 58.84/58.91 ~ ( in(A,B) % 58.84/58.91 & empty(B) ) ). % 58.84/58.91 % 58.84/58.91 fof(t8_boole,axiom, % 58.84/58.91 ! [A,B] : % 58.84/58.91 ~ ( empty(A) % 58.84/58.91 & A != B % 58.84/58.91 & empty(B) ) ). % 58.84/58.91 % 58.84/58.91 %------------------------------------------------------------------------------ % 58.84/58.91 %------------------------------------------- % 58.84/58.91 % Proof found % 58.84/58.91 % SZS status Theorem for theBenchmark % 58.84/58.91 % SZS output start Proof % 58.84/58.91 %ClaNum:136(EqnAxiom:37) % 58.84/58.91 %VarNum:176(SingletonVarNum:71) % 58.84/58.91 %MaxLitNum:5 % 58.84/58.91 %MaxfuncDepth:3 % 58.84/58.91 %SharedTerms:64 % 58.84/58.91 %goalClause: 96 % 58.84/58.91 %singleGoalClaCount:1 % 58.84/58.91 [41]P1(a1) % 58.84/58.91 [42]P1(a2) % 58.84/58.91 [43]P1(a21) % 58.84/58.91 [44]P1(a3) % 58.84/58.91 [45]P1(a4) % 58.84/58.91 [46]P3(a1) % 58.84/58.91 [47]P3(a5) % 58.84/58.91 [48]P3(a3) % 58.84/58.91 [49]P3(a4) % 58.84/58.91 [50]P3(a6) % 58.84/58.91 [51]P3(a9) % 58.84/58.91 [52]P3(a12) % 58.84/58.91 [53]P3(a13) % 58.84/58.91 [54]P6(a1) % 58.84/58.91 [55]P6(a20) % 58.84/58.91 [56]P6(a4) % 58.84/58.91 [57]P6(a10) % 58.84/58.91 [58]P4(a1) % 58.84/58.91 [59]P4(a20) % 58.84/58.91 [60]P4(a4) % 58.84/58.91 [61]P4(a10) % 58.84/58.91 [62]P5(a1) % 58.84/58.91 [63]P5(a20) % 58.84/58.91 [64]P5(a4) % 58.84/58.91 [65]P5(a10) % 58.84/58.91 [68]P9(a1) % 58.84/58.91 [69]P9(a5) % 58.84/58.91 [70]P9(a2) % 58.84/58.91 [71]P9(a3) % 58.84/58.91 [72]P9(a4) % 58.84/58.91 [73]P9(a7) % 58.84/58.91 [74]P9(a6) % 58.84/58.91 [75]P9(a11) % 58.84/58.91 [76]P9(a9) % 58.84/58.91 [77]P9(a12) % 58.84/58.91 [78]P9(a13) % 58.84/58.91 [79]P7(a1) % 58.84/58.91 [80]P7(a4) % 58.84/58.91 [81]P7(a6) % 58.84/58.91 [82]P10(a12) % 58.84/58.91 [84]P11(a1) % 58.84/58.91 [85]P11(a11) % 58.84/58.91 [86]P11(a9) % 58.84/58.91 [87]P12(a13) % 58.84/58.91 [93]~P1(a7) % 58.84/58.91 [94]~P1(a8) % 58.84/58.91 [95]~P1(a10) % 58.84/58.91 [96]~P14(a1,a15) % 58.84/58.91 [88]P13(a1,x881) % 58.84/58.91 [89]P13(x891,x891) % 58.84/58.91 [90]P14(f14(x901),x901) % 58.84/58.91 [91]P2(f19(x911),x911) % 58.84/58.91 [92]E(f22(x921,x922),f22(x922,x921)) % 58.84/58.91 [97]~P1(f22(f22(x971,x972),f23(x971))) % 58.84/58.91 [98]~P1(x981)+E(x981,a1) % 58.84/58.91 [99]~P1(x991)+P3(x991) % 58.84/58.91 [100]~P1(x1001)+P6(x1001) % 58.84/58.91 [101]~P1(x1011)+P4(x1011) % 58.84/58.91 [102]~P6(x1021)+P4(x1021) % 58.84/58.91 [103]~P1(x1031)+P5(x1031) % 58.84/58.91 [104]~P6(x1041)+P5(x1041) % 58.84/58.91 [105]~P1(x1051)+P9(x1051) % 58.84/58.91 [107]~P1(x1071)+P1(f24(x1071)) % 58.84/58.91 [108]~P1(x1081)+P1(f26(x1081)) % 58.84/58.91 [109]~P1(x1091)+P9(f24(x1091)) % 58.84/58.91 [110]~P1(x1101)+P9(f26(x1101)) % 58.84/58.91 [115]P3(x1151)+~P14(x1151,x1152) % 58.84/58.91 [116]P9(x1161)+~P14(x1161,x1162) % 58.84/58.91 [117]P10(x1171)+~P14(x1171,x1172) % 58.84/58.91 [120]~P1(x1201)+~P8(x1202,x1201) % 58.84/58.91 [124]~P8(x1241,x1242)+P2(x1241,x1242) % 58.84/58.91 [127]~P8(x1272,x1271)+~P8(x1271,x1272) % 58.84/58.91 [126]~P13(x1261,x1262)+P2(x1261,f25(x1262)) % 58.84/58.91 [128]P13(x1281,x1282)+~P2(x1281,f25(x1282)) % 58.84/58.91 [113]~P4(x1131)+~P5(x1131)+P6(x1131) % 58.84/58.91 [111]~P9(x1111)+~E(f26(x1111),a1)+E(f24(x1111),a1) % 58.84/58.91 [112]~P9(x1121)+~E(f24(x1121),a1)+E(f26(x1121),a1) % 58.84/58.91 [118]~P9(x1181)+P1(x1181)+~P1(f24(x1181)) % 58.84/58.91 [119]~P9(x1191)+P1(x1191)+~P1(f26(x1191)) % 58.84/58.91 [106]~P1(x1062)+~P1(x1061)+E(x1061,x1062) % 58.84/58.91 [125]~P2(x1252,x1251)+P1(x1251)+P8(x1252,x1251) % 58.84/58.91 [129]~P1(x1291)+~P8(x1292,x1293)+~P2(x1293,f25(x1291)) % 58.84/58.91 [132]P2(x1321,x1322)+~P8(x1321,x1323)+~P2(x1323,f25(x1322)) % 58.84/58.91 [114]~P1(x1141)+~P3(x1141)+~P9(x1141)+P7(x1141) % 58.84/58.91 [121]~P3(x1211)+~P9(x1211)+~P10(x1211)+P6(f24(x1211)) % 58.84/58.91 [122]~P3(x1221)+~P9(x1221)+~P12(x1221)+P15(f26(x1221)) % 58.84/58.91 [123]~P3(x1231)+~P9(x1231)+P10(x1231)+~P6(f24(x1231)) % 58.84/58.91 [134]~P9(x1342)+P8(f17(x1342,x1341),x1341)+E(x1341,f24(x1342))+P8(f22(f22(f17(x1342,x1341),f18(x1342,x1341)),f23(f17(x1342,x1341))),x1342) % 58.84/58.91 [136]~P9(x1362)+~P8(x1361,x1363)+~E(x1363,f24(x1362))+P8(f22(f22(x1361,f16(x1362,x1363,x1361)),f23(x1361)),x1362) % 58.84/58.91 [135]~P9(x1352)+~P8(f17(x1352,x1351),x1351)+E(x1351,f24(x1352))+~P8(f22(f22(f17(x1352,x1351),x1353),f23(f17(x1352,x1351))),x1352) % 58.84/58.91 [133]~P9(x1333)+P8(x1331,x1332)+~E(x1332,f24(x1333))+~P8(f22(f22(x1331,x1334),f23(x1331)),x1333) % 58.84/58.91 [130]~P3(x1301)+~P9(x1301)+~P10(x1301)+~P14(x1301,x1302)+P13(f26(x1301),x1302) % 58.84/58.91 [131]~P3(x1311)+~P9(x1311)+~P10(x1311)+P14(x1311,x1312)+~P13(f26(x1311),x1312) % 58.84/58.91 %EqnAxiom % 58.84/58.91 [1]E(x11,x11) % 58.84/58.91 [2]E(x22,x21)+~E(x21,x22) % 58.84/58.91 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.84/58.91 [4]~E(x41,x42)+E(f14(x41),f14(x42)) % 58.84/58.91 [5]~E(x51,x52)+E(f19(x51),f19(x52)) % 58.84/58.91 [6]~E(x61,x62)+E(f22(x61,x63),f22(x62,x63)) % 58.84/58.91 [7]~E(x71,x72)+E(f22(x73,x71),f22(x73,x72)) % 58.84/58.91 [8]~E(x81,x82)+E(f24(x81),f24(x82)) % 58.84/58.91 [9]~E(x91,x92)+E(f23(x91),f23(x92)) % 58.84/58.91 [10]~E(x101,x102)+E(f17(x101,x103),f17(x102,x103)) % 58.84/58.91 [11]~E(x111,x112)+E(f17(x113,x111),f17(x113,x112)) % 58.84/58.91 [12]~E(x121,x122)+E(f16(x121,x123,x124),f16(x122,x123,x124)) % 58.84/58.91 [13]~E(x131,x132)+E(f16(x133,x131,x134),f16(x133,x132,x134)) % 58.84/58.91 [14]~E(x141,x142)+E(f16(x143,x144,x141),f16(x143,x144,x142)) % 58.84/58.91 [15]~E(x151,x152)+E(f26(x151),f26(x152)) % 58.84/58.91 [16]~E(x161,x162)+E(f25(x161),f25(x162)) % 58.84/58.91 [17]~E(x171,x172)+E(f18(x171,x173),f18(x172,x173)) % 58.84/58.91 [18]~E(x181,x182)+E(f18(x183,x181),f18(x183,x182)) % 58.84/58.91 [19]~P1(x191)+P1(x192)+~E(x191,x192) % 58.84/58.91 [20]P8(x202,x203)+~E(x201,x202)+~P8(x201,x203) % 58.84/58.91 [21]P8(x213,x212)+~E(x211,x212)+~P8(x213,x211) % 58.84/58.91 [22]~P9(x221)+P9(x222)+~E(x221,x222) % 58.84/58.91 [23]P2(x232,x233)+~E(x231,x232)+~P2(x231,x233) % 58.84/58.91 [24]P2(x243,x242)+~E(x241,x242)+~P2(x243,x241) % 58.84/58.91 [25]~P3(x251)+P3(x252)+~E(x251,x252) % 58.84/58.91 [26]P13(x262,x263)+~E(x261,x262)+~P13(x261,x263) % 58.84/58.91 [27]P13(x273,x272)+~E(x271,x272)+~P13(x273,x271) % 58.84/58.91 [28]~P10(x281)+P10(x282)+~E(x281,x282) % 58.84/58.91 [29]P14(x292,x293)+~E(x291,x292)+~P14(x291,x293) % 58.84/58.91 [30]P14(x303,x302)+~E(x301,x302)+~P14(x303,x301) % 58.84/58.91 [31]~P4(x311)+P4(x312)+~E(x311,x312) % 58.84/58.91 [32]~P6(x321)+P6(x322)+~E(x321,x322) % 58.84/58.91 [33]~P5(x331)+P5(x332)+~E(x331,x332) % 58.84/58.91 [34]~P7(x341)+P7(x342)+~E(x341,x342) % 58.84/58.91 [35]~P15(x351)+P15(x352)+~E(x351,x352) % 58.84/58.91 [36]~P11(x361)+P11(x362)+~E(x361,x362) % 58.84/58.91 [37]~P12(x371)+P12(x372)+~E(x371,x372) % 58.84/58.91 % 58.84/58.91 %------------------------------------------- % 58.84/58.92 cnf(138,plain, % 58.84/58.92 (~P9(x1381)+~P8(x1382,f24(x1381))+P8(f22(f22(x1382,f16(x1381,f24(x1381),x1382)),f23(x1382)),x1381)), % 58.84/58.92 inference(equality_inference,[],[136])). % 58.84/58.92 cnf(139,plain, % 58.84/58.92 (P13(f19(f25(x1391)),x1391)), % 58.84/58.92 inference(scs_inference,[],[91,128])). % 58.84/58.92 cnf(140,plain, % 58.84/58.92 (P2(f19(x1401),x1401)), % 58.84/58.92 inference(rename_variables,[],[91])). % 58.84/58.92 cnf(142,plain, % 58.84/58.92 (~P8(x1421,a1)), % 58.84/58.92 inference(scs_inference,[],[91,41,128,120])). % 58.84/58.92 cnf(144,plain, % 58.84/58.92 (~E(f14(a15),a1)), % 58.84/58.92 inference(scs_inference,[],[96,90,91,41,128,120,29])). % 58.84/58.92 cnf(145,plain, % 58.84/58.92 (P14(f14(x1451),x1451)), % 58.84/58.92 inference(rename_variables,[],[90])). % 58.84/58.92 cnf(148,plain, % 58.84/58.92 (~P1(f14(a15))), % 58.84/58.92 inference(scs_inference,[],[96,90,145,92,91,41,128,120,29,30,106])). % 58.84/58.92 cnf(154,plain, % 58.84/58.92 (P2(f19(x1541),x1541)), % 58.84/58.92 inference(rename_variables,[],[91])). % 58.84/58.92 cnf(156,plain, % 58.84/58.92 (~P8(x1561,f24(a1))), % 58.84/58.92 inference(scs_inference,[],[96,89,90,145,92,68,91,140,41,93,128,120,29,30,106,26,27,125,138])). % 58.84/58.92 cnf(158,plain, % 58.84/58.92 (~P1(f22(f23(x1581),f22(x1581,x1582)))), % 58.84/58.92 inference(scs_inference,[],[96,89,90,145,92,68,91,140,41,93,97,128,120,29,30,106,26,27,125,138,19])). % 58.84/58.92 cnf(159,plain, % 58.84/58.92 (E(f22(x1591,x1592),f22(x1592,x1591))), % 58.84/58.92 inference(rename_variables,[],[92])). % 58.84/58.92 cnf(160,plain, % 58.84/58.92 (~E(a7,f24(a1))), % 58.84/58.92 inference(scs_inference,[],[96,89,90,145,92,68,91,140,41,93,97,128,120,29,30,106,26,27,125,138,19,21])). % 58.84/58.92 cnf(161,plain, % 58.84/58.93 (P2(f19(f22(x1611,x1612)),f22(x1612,x1611))), % 58.84/58.93 inference(scs_inference,[],[96,89,90,145,92,159,68,91,140,154,41,93,97,128,120,29,30,106,26,27,125,138,19,21,24])). % 58.84/58.93 cnf(178,plain, % 58.84/58.93 (~P8(x1781,a2)), % 58.84/58.93 inference(scs_inference,[],[42,120])). % 58.84/58.93 cnf(180,plain, % 58.84/58.93 (~P8(x1801,f24(a2))), % 58.84/58.93 inference(scs_inference,[],[70,42,120,138])). % 58.84/58.93 cnf(183,plain, % 58.84/58.93 (P2(f19(x1831),x1831)), % 58.84/58.93 inference(rename_variables,[],[91])). % 58.84/58.93 cnf(188,plain, % 58.84/58.93 (P8(f17(a1,a7),a7)), % 58.84/58.93 inference(scs_inference,[],[148,70,68,160,42,91,183,142,120,138,129,125,134])). % 58.84/58.93 cnf(194,plain, % 58.84/58.93 (~E(f14(a15),f24(a1))), % 58.84/58.93 inference(scs_inference,[],[148,70,68,92,156,160,42,91,183,142,120,138,129,125,134,127,31,21])). % 58.84/58.93 cnf(201,plain, % 58.84/58.93 (~P8(x2011,a21)), % 58.84/58.93 inference(scs_inference,[],[43,120])). % 58.84/58.93 cnf(203,plain, % 58.84/58.93 (~P8(a7,f17(a1,a7))), % 58.84/58.93 inference(scs_inference,[],[188,43,120,127])). % 58.84/58.93 cnf(208,plain, % 58.84/58.93 (P8(f19(f22(f22(x2081,x2082),f23(x2081))),f22(f23(x2081),f22(x2081,x2082)))), % 58.84/58.93 inference(scs_inference,[],[188,161,158,43,91,120,127,129,125])). % 58.84/58.93 cnf(213,plain, % 58.84/58.93 (P8(f17(a2,a7),a7)), % 58.84/58.93 inference(scs_inference,[],[188,70,161,158,180,43,91,178,120,127,129,125,21,134])). % 58.84/58.93 cnf(221,plain, % 58.84/58.93 (~P8(x2211,a4)), % 58.84/58.93 inference(scs_inference,[],[45,120])). % 58.84/58.93 cnf(225,plain, % 58.84/58.93 (~P8(x2251,f24(a4))), % 58.84/58.93 inference(scs_inference,[],[213,72,45,120,127,138])). % 58.84/58.93 cnf(228,plain, % 58.84/58.93 (P2(f19(x2281),x2281)), % 58.84/58.93 inference(rename_variables,[],[91])). % 58.84/58.93 cnf(230,plain, % 58.84/58.93 (P8(f19(a8),a8)), % 58.84/58.93 inference(scs_inference,[],[213,72,45,91,228,94,120,127,138,129,125])). % 58.84/58.93 cnf(240,plain, % 58.84/58.93 (~P8(x2401,a3)), % 58.84/58.93 inference(scs_inference,[],[44,120])). % 58.84/58.93 cnf(244,plain, % 58.84/58.93 (~P8(x2441,f24(a3))), % 58.84/58.93 inference(scs_inference,[],[71,230,44,120,127,138])). % 58.84/58.93 cnf(247,plain, % 58.84/58.93 (P2(f19(x2471),x2471)), % 58.84/58.93 inference(rename_variables,[],[91])). % 58.84/58.93 cnf(249,plain, % 58.84/58.93 (P8(f19(a10),a10)), % 58.84/58.93 inference(scs_inference,[],[71,230,44,91,247,95,120,127,138,129,125])). % 58.84/58.93 cnf(254,plain, % 58.84/58.93 (P8(f17(a4,a7),a7)), % 58.84/58.93 inference(scs_inference,[],[213,71,72,225,230,44,91,247,221,95,120,127,138,129,125,21,134])). % 58.84/58.93 cnf(265,plain, % 58.84/58.93 (P8(f19(f22(f23(x2651),f22(x2651,x2652))),f22(f22(x2651,x2652),f23(x2651)))), % 58.84/58.93 inference(scs_inference,[],[254,161,97,127,125])). % 58.84/58.93 cnf(266,plain, % 58.84/58.93 (P2(f19(f22(x2661,x2662)),f22(x2662,x2661))), % 58.84/58.93 inference(rename_variables,[],[161])). % 58.84/58.93 cnf(268,plain, % 58.84/58.93 (~E(a7,f24(a3))), % 58.84/58.93 inference(scs_inference,[],[254,161,244,97,127,125,21])). % 58.84/58.93 cnf(269,plain, % 58.84/58.93 (~P8(x2691,f24(a3))), % 58.84/58.93 inference(rename_variables,[],[244])). % 58.84/58.93 cnf(270,plain, % 58.84/58.93 (P8(f17(a1,f14(a15)),f14(a15))), % 58.84/58.93 inference(scs_inference,[],[254,68,161,194,244,142,97,127,125,21,134])). % 58.84/58.93 cnf(274,plain, % 58.84/58.93 (P2(x2741,f22(x2742,x2743))+~E(f19(f22(x2743,x2742)),x2741)), % 58.84/58.93 inference(scs_inference,[],[92,254,68,161,266,194,244,142,97,127,125,21,134,36,23])). % 58.84/58.93 cnf(275,plain, % 58.84/58.93 (P2(x2751,x2752)+~P8(x2751,f19(f25(x2752)))), % 58.84/58.93 inference(scs_inference,[],[92,254,68,161,266,194,244,91,142,97,127,125,21,134,36,23,132])). % 58.84/58.93 cnf(278,plain, % 58.84/58.93 (~P9(f24(a3))+~P8(x2781,f24(f24(a3)))), % 58.84/58.93 inference(scs_inference,[],[92,254,68,161,266,194,244,269,91,142,97,127,125,21,134,36,23,132,138])). % 58.84/58.93 cnf(289,plain, % 58.84/58.93 (~P8(x2891,a3)), % 58.84/58.93 inference(rename_variables,[],[240])). % 58.84/58.93 cnf(291,plain, % 58.84/58.93 (P8(f17(a3,a7),a7)), % 58.84/58.93 inference(scs_inference,[],[270,71,268,180,240,289,127,21,136,134])). % 58.84/58.93 cnf(301,plain, % 58.84/58.93 (P8(f19(f22(f23(x3011),f22(x3011,x3012))),f22(f23(x3011),f22(x3011,x3012)))), % 58.84/58.93 inference(scs_inference,[],[291,91,158,127,125])). % 58.84/58.93 cnf(319,plain, % 58.84/58.93 (~P9(f24(a1))+~P8(x3191,f24(f24(a1)))), % 58.84/58.93 inference(scs_inference,[],[265,244,156,127,21,138])). % 58.84/58.93 cnf(332,plain, % 58.84/58.93 (P8(f19(f22(f22(x3321,x3322),f23(x3321))),f22(f22(x3321,x3322),f23(x3321)))), % 58.84/58.93 inference(scs_inference,[],[91,301,97,127,125])). % 58.84/58.93 cnf(346,plain, % 58.84/58.93 (~E(f22(f22(x3461,x3462),f23(x3461)),f24(a4))), % 58.84/58.93 inference(scs_inference,[],[332,225,127,21])). % 58.84/58.93 cnf(349,plain, % 58.84/58.93 (P2(x3491,x3492)+~E(f19(x3492),x3491)), % 58.84/58.93 inference(scs_inference,[],[92,91,332,225,127,21,37,23])). % 58.84/58.93 cnf(358,plain, % 58.84/58.93 (~P9(f24(a2))+~P8(x3581,f24(f24(a2)))), % 58.84/58.93 inference(scs_inference,[],[249,244,180,127,21,138])). % 58.84/58.93 cnf(369,plain, % 58.84/58.93 (~E(a8,f24(a1))), % 58.84/58.93 inference(scs_inference,[],[156,208,230,127,21])). % 58.84/58.93 cnf(371,plain, % 58.84/58.93 (P13(x3711,x3712)+~E(f19(f25(x3712)),x3711)), % 58.84/58.93 inference(scs_inference,[],[139,156,208,230,127,21,26])). % 58.84/58.93 cnf(382,plain, % 58.84/58.93 (~E(f22(f22(x3821,x3822),f23(x3821)),f24(a1))), % 58.84/58.93 inference(scs_inference,[],[156,265,21])). % 58.84/58.93 cnf(393,plain, % 58.84/58.93 (P13(x3931,x3932)+~E(a1,x3931)), % 58.84/58.93 inference(scs_inference,[],[88,208,244,21,26])). % 58.84/58.93 cnf(403,plain, % 58.84/58.93 (~E(f22(f22(x4031,x4032),f23(x4031)),f24(a2))), % 58.84/58.93 inference(scs_inference,[],[332,180,21])). % 58.84/58.93 cnf(409,plain, % 58.84/58.93 (P5(f24(a4))), % 58.84/58.93 inference(scs_inference,[],[45,103,107])). % 58.84/58.93 cnf(414,plain, % 58.84/58.93 (P10(a4)+~P4(f24(a4))), % 58.84/58.93 inference(scs_inference,[],[49,72,301,225,409,21,113,123])). % 58.84/58.93 cnf(509,plain, % 58.84/58.93 (~P8(x5091,f24(a1))), % 58.84/58.93 inference(rename_variables,[],[156])). % 58.84/58.93 cnf(511,plain, % 58.84/58.93 (~P9(f24(a1))+P8(f17(f24(a1),a7),a7)), % 58.84/58.93 inference(scs_inference,[],[291,51,76,156,509,114,136,134])). % 58.84/58.93 cnf(551,plain, % 58.84/58.93 (~P9(a21)+~E(a7,f24(a21))), % 58.84/58.93 inference(scs_inference,[],[291,201,136])). % 58.84/58.93 cnf(591,plain, % 58.84/58.93 (~P9(a21)+E(f24(a1),f24(a21))), % 58.84/58.93 inference(scs_inference,[],[156,201,134])). % 58.84/58.93 cnf(595,plain, % 58.84/58.93 (E(f24(a21),f24(a1))+~P9(a21)), % 58.84/58.93 inference(scs_inference,[],[156,201,134,2])). % 58.84/58.93 cnf(638,plain, % 58.84/58.93 (E(f24(a21),a1)), % 58.84/58.93 inference(scs_inference,[],[43,98,107])). % 58.84/58.93 cnf(639,plain, % 58.84/58.93 (E(a1,f24(a21))), % 58.84/58.93 inference(scs_inference,[],[638,2])). % 58.84/58.93 cnf(640,plain, % 58.84/58.93 (P1(f24(a21))), % 58.84/58.93 inference(scs_inference,[],[638,41,2,19])). % 58.84/58.93 cnf(642,plain, % 58.84/58.93 (P9(f24(a21))), % 58.84/58.93 inference(scs_inference,[],[144,638,68,41,2,19,3,22])). % 58.84/58.93 cnf(643,plain, % 58.84/58.93 (P11(f24(a21))), % 58.84/58.93 inference(scs_inference,[],[144,638,68,41,84,2,19,3,22,36])). % 58.84/58.93 cnf(644,plain, % 58.84/58.93 (P3(f24(a21))), % 58.84/58.93 inference(scs_inference,[],[144,46,638,68,41,84,2,19,3,22,36,25])). % 58.84/58.93 cnf(645,plain, % 58.84/58.93 (P5(f24(a21))), % 58.84/58.93 inference(scs_inference,[],[144,46,638,68,41,62,84,2,19,3,22,36,25,33])). % 58.84/58.93 cnf(646,plain, % 58.84/58.93 (P4(f24(a21))), % 58.84/58.93 inference(scs_inference,[],[144,46,638,68,41,62,58,84,2,19,3,22,36,25,33,31])). % 58.84/58.93 cnf(647,plain, % 58.84/58.93 (P6(f24(a21))), % 58.84/58.93 inference(scs_inference,[],[144,46,638,68,41,62,54,58,84,2,19,3,22,36,25,33,31,32])). % 58.84/58.93 cnf(649,plain, % 58.84/58.93 (P7(f24(a21))), % 58.84/58.93 inference(scs_inference,[],[144,46,638,68,88,41,62,54,58,79,84,2,19,3,22,36,25,33,31,32,26,34])). % 58.84/58.93 cnf(650,plain, % 58.84/58.93 (~P8(x6501,f24(a21))), % 58.84/58.93 inference(scs_inference,[],[144,46,638,68,88,41,62,54,58,79,84,2,19,3,22,36,25,33,31,32,26,34,120])). % 58.84/58.93 cnf(652,plain, % 58.84/58.93 (~P9(a21)+E(f26(a21),a1)), % 58.84/58.93 inference(scs_inference,[],[144,46,638,68,88,41,62,54,58,79,84,2,19,3,22,36,25,33,31,32,26,34,120,112])). % 58.84/58.93 cnf(654,plain, % 58.84/58.93 (~P8(x6541,f24(f24(a21)))), % 58.84/58.93 inference(scs_inference,[],[144,46,638,68,88,41,62,54,58,79,84,2,19,3,22,36,25,33,31,32,26,34,120,112,138])). % 58.84/58.93 cnf(660,plain, % 58.84/58.93 (~P9(a21)+P8(f17(a21,f14(a15)),f14(a15))), % 58.84/58.93 inference(scs_inference,[],[144,46,638,68,88,41,201,62,54,58,79,84,2,19,3,22,36,25,33,31,32,26,34,120,112,138,37,35,28,123,134])). % 58.84/58.93 cnf(663,plain, % 58.84/58.93 (P1(f26(f24(a3)))), % 58.84/58.93 inference(scs_inference,[],[44,108,107])). % 58.84/58.93 cnf(667,plain, % 58.84/58.93 (~P8(x6671,f24(a21))), % 58.84/58.93 inference(rename_variables,[],[650])). % 58.84/58.93 cnf(678,plain, % 58.84/58.93 (~P10(a1)+P10(f24(a21))), % 58.84/58.93 inference(scs_inference,[],[291,642,639,663,650,667,120,136,134,127,119,35,37,28])). % 58.84/58.93 cnf(693,plain, % 58.84/58.93 (~P1(f24(a4))+P10(a4)), % 58.84/58.93 inference(scs_inference,[],[414,101])). % 58.84/58.93 cnf(705,plain, % 58.84/58.93 (P10(a21)+~P9(a21)+~P3(a21)), % 58.84/58.93 inference(scs_inference,[],[647,123])). % 58.84/58.93 cnf(718,plain, % 58.84/58.93 (~P8(x7181,f19(f25(f24(a21))))), % 58.84/58.93 inference(scs_inference,[],[91,640,129])). % 58.84/58.93 cnf(817,plain, % 58.84/58.93 (P2(f19(f24(a21)),a1)), % 58.84/58.93 inference(scs_inference,[],[638,91,24])). % 58.84/58.93 cnf(819,plain, % 58.84/58.93 (P13(f19(f25(f24(a21))),a1)), % 58.84/58.93 inference(scs_inference,[],[638,139,91,24,27])). % 58.84/58.93 cnf(821,plain, % 58.84/58.93 (P14(f14(f24(a21)),a1)), % 58.84/58.93 inference(scs_inference,[],[638,139,90,91,24,27,30])). % 58.84/58.93 cnf(824,plain, % 58.84/58.93 (P14(x8241,a1)+~E(f14(f24(a21)),x8241)), % 58.84/58.93 inference(scs_inference,[],[638,139,90,91,24,27,30,23,29])). % 58.84/58.93 cnf(842,plain, % 58.84/58.93 (P10(a4)), % 58.84/58.93 inference(scs_inference,[],[45,693,107])). % 58.84/58.93 cnf(858,plain, % 58.84/58.93 (~P8(a7,f25(f24(a21)))), % 58.84/58.93 inference(scs_inference,[],[640,291,124,129])). % 58.84/58.93 cnf(950,plain, % 58.84/58.93 (P14(f14(a1),f24(a21))), % 58.84/58.93 inference(scs_inference,[],[639,90,270,654,21,30])). % 58.84/58.93 cnf(952,plain, % 58.84/58.93 (P2(f19(a1),f24(a21))), % 58.84/58.93 inference(scs_inference,[],[639,90,270,654,91,21,30,24])). % 58.84/58.93 cnf(956,plain, % 58.84/58.93 (P8(f17(a2,f22(f22(x9561,x9562),f23(x9561))),f22(f22(x9561,x9562),f23(x9561)))), % 58.84/58.93 inference(scs_inference,[],[639,90,270,139,70,403,654,91,178,21,30,24,27,134])). % 58.84/58.93 cnf(967,plain, % 58.84/58.93 (~P8(f22(f22(x9671,x9672),f23(x9671)),f17(a2,f22(f22(x9671,x9672),f23(x9671))))), % 58.84/58.93 inference(scs_inference,[],[956,127])). % 58.84/58.93 cnf(971,plain, % 58.84/58.93 (P8(f17(a1,a8),a8)), % 58.84/58.93 inference(scs_inference,[],[956,68,369,654,142,127,21,134])). % 58.84/58.93 cnf(983,plain, % 58.84/58.93 (~P8(a8,f17(a1,a8))), % 58.84/58.93 inference(scs_inference,[],[971,127])). % 58.84/58.93 cnf(987,plain, % 58.84/58.93 (P8(f17(a4,f22(f22(x9871,x9872),f23(x9871))),f22(f22(x9871,x9872),f23(x9871)))), % 58.84/58.93 inference(scs_inference,[],[971,72,346,654,221,127,21,134])). % 58.84/58.93 cnf(994,plain, % 58.84/58.93 (~P8(f22(f22(x9941,x9942),f23(x9941)),f17(a4,f22(f22(x9941,x9942),f23(x9941))))), % 58.84/58.93 inference(scs_inference,[],[987,127])). % 58.84/58.93 cnf(1090,plain, % 58.84/58.93 (P13(f19(f25(f26(a21))),a1)+~P9(a21)), % 58.84/58.93 inference(scs_inference,[],[139,652,27])). % 58.84/58.93 cnf(1234,plain, % 58.84/58.93 (P2(f24(a21),f25(x12341))), % 58.84/58.93 inference(scs_inference,[],[639,126,393])). % 58.84/58.93 cnf(1235,plain, % 58.84/58.93 (P2(a1,f25(x12351))), % 58.84/58.93 inference(scs_inference,[],[638,1234,23])). % 58.84/58.93 cnf(1279,plain, % 58.84/58.93 (E(f14(f24(a21)),f14(f24(a1)))+~P9(a21)), % 58.84/58.93 inference(scs_inference,[],[595,4])). % 58.84/58.93 cnf(1375,plain, % 58.84/58.93 (E(f19(f22(f22(x13751,x13752),x13753)),f19(f22(f22(x13752,x13751),x13753)))), % 58.84/58.93 inference(scs_inference,[],[92,5,6])). % 58.84/58.93 cnf(1407,plain, % 58.84/58.93 (E(f26(f24(f22(x14071,x14072))),f26(f24(f22(x14072,x14071))))), % 58.84/58.93 inference(scs_inference,[],[92,15,8])). % 58.84/58.93 cnf(1669,plain, % 58.84/58.93 (P1(f24(f24(a3)))+~P9(f24(a3))), % 58.84/58.93 inference(scs_inference,[],[91,278,125])). % 58.84/58.93 cnf(1685,plain, % 58.84/58.93 (~P9(f24(a3))+E(f24(f24(a3)),a1)), % 58.84/58.93 inference(scs_inference,[],[1669,98])). % 58.84/58.93 cnf(1732,plain, % 58.84/58.93 (P1(f24(f24(a1)))+~P9(f24(a1))), % 58.84/58.93 inference(scs_inference,[],[91,319,125])). % 58.84/58.93 cnf(1748,plain, % 58.84/58.93 (~P9(f24(a1))+E(f24(f24(a1)),a1)), % 58.84/58.93 inference(scs_inference,[],[1732,98])). % 58.84/58.93 cnf(1795,plain, % 58.84/58.93 (P1(f24(f24(a2)))+~P9(f24(a2))), % 58.84/58.93 inference(scs_inference,[],[91,358,125])). % 58.84/58.93 cnf(1811,plain, % 58.84/58.93 (~P9(f24(a2))+E(f24(f24(a2)),a1)), % 58.84/58.93 inference(scs_inference,[],[1795,98])). % 58.84/58.93 cnf(2036,plain, % 58.84/58.93 (E(f24(f24(a3)),a1)), % 58.84/58.93 inference(scs_inference,[],[44,1685,109])). % 58.84/58.93 cnf(2037,plain, % 58.84/58.93 (E(a1,f24(f24(a3)))), % 58.84/58.93 inference(scs_inference,[],[2036,2])). % 58.84/58.93 cnf(2040,plain, % 58.84/58.93 (P6(f24(f24(a3)))), % 58.84/58.93 inference(scs_inference,[],[2036,62,54,79,2,34,33,32])). % 58.84/58.93 cnf(2041,plain, % 58.84/58.93 (P9(f24(f24(a3)))), % 58.84/58.93 inference(scs_inference,[],[2036,68,62,54,79,2,34,33,32,22])). % 58.84/58.93 cnf(2042,plain, % 58.84/58.93 (~E(f14(a15),f24(f24(a3)))), % 58.84/58.93 inference(scs_inference,[],[144,2036,68,62,54,79,2,34,33,32,22,3])). % 58.84/58.93 cnf(2046,plain, % 58.84/58.93 (P3(f24(f24(a3)))), % 58.84/58.93 inference(scs_inference,[],[144,46,2036,68,41,62,54,58,79,84,2,34,33,32,22,3,19,31,36,25])). % 58.84/58.93 cnf(2060,plain, % 58.84/58.93 (~P10(a1)+P10(f24(f24(a3)))), % 58.84/58.93 inference(scs_inference,[],[2037,28])). % 58.84/58.93 cnf(2075,plain, % 58.84/58.93 (E(a1,f26(f24(a3)))+~P9(f24(a3))), % 58.84/58.93 inference(scs_inference,[],[144,2036,112,3,2])). % 58.84/58.93 cnf(2098,plain, % 58.84/58.93 (~P10(f24(f24(a3)))+P14(f24(f24(a3)),f26(f24(f24(a3))))), % 58.84/58.93 inference(scs_inference,[],[89,2036,2046,2042,2041,244,2040,35,37,134,123,131])). % 58.84/58.93 cnf(2113,plain, % 58.84/58.93 (P14(f24(f24(a3)),f26(f24(f24(a3))))+~P10(a1)), % 58.84/58.93 inference(scs_inference,[],[2060,2098])). % 58.84/58.93 cnf(2224,plain, % 58.84/58.93 (P14(f14(f24(a21)),f24(f24(a3)))), % 58.84/58.93 inference(scs_inference,[],[821,2037,30])). % 58.84/58.93 cnf(2228,plain, % 58.84/58.93 (P8(f17(a1,f22(f22(x22281,x22282),f23(x22281))),f22(f22(x22281,x22282),f23(x22281)))), % 58.84/58.93 inference(scs_inference,[],[821,2037,819,68,382,1235,817,142,30,27,24,23,134])). % 58.84/58.93 cnf(2245,plain, % 58.84/58.93 (P14(f14(f24(f24(a3))),a1)), % 58.84/58.93 inference(scs_inference,[],[2036,90,2228,127,30])). % 58.84/58.93 cnf(2358,plain, % 58.84/58.93 (E(f24(f24(a1)),a1)), % 58.84/58.93 inference(scs_inference,[],[41,1748,109])). % 58.84/58.93 cnf(2359,plain, % 58.84/58.93 (E(a1,f24(f24(a1)))), % 58.84/58.93 inference(scs_inference,[],[2358,2])). % 58.84/58.93 cnf(2361,plain, % 58.84/58.93 (~E(f14(a15),f24(f24(a1)))), % 58.84/58.93 inference(scs_inference,[],[144,2358,2,393,3])). % 58.84/58.93 cnf(2362,plain, % 58.84/58.93 (P1(f24(f24(a1)))), % 58.84/58.93 inference(scs_inference,[],[144,2358,41,2,393,3,19])). % 58.84/58.93 cnf(2364,plain, % 58.84/58.93 (P3(f24(f24(a1)))), % 58.84/58.93 inference(scs_inference,[],[144,46,2358,41,79,2,393,3,19,34,25])). % 58.84/58.93 cnf(2367,plain, % 58.84/58.93 (P6(f24(f24(a1)))), % 58.84/58.93 inference(scs_inference,[],[144,46,2358,41,62,54,79,84,2,393,3,19,34,25,33,36,32])). % 58.84/58.93 cnf(2369,plain, % 58.84/58.93 (P9(f24(f24(a1)))), % 58.84/58.93 inference(scs_inference,[],[58,144,46,2358,68,41,62,54,79,84,2,393,3,19,34,25,33,36,32,31,22])). % 58.84/58.93 cnf(2370,plain, % 58.84/58.93 (~P8(x23701,f24(f24(a1)))), % 58.84/58.93 inference(scs_inference,[],[58,144,46,2358,68,41,62,54,79,84,2,393,3,19,34,25,33,36,32,31,22,120])). % 58.84/58.93 cnf(2372,plain, % 58.84/58.93 (P1(f24(a1))+~P9(f24(a1))), % 58.84/58.93 inference(scs_inference,[],[58,144,46,2358,68,41,62,54,79,84,2,393,3,19,34,25,33,36,32,31,22,120,118])). % 58.84/58.93 cnf(2388,plain, % 58.84/58.93 (E(a1,f26(f24(a1)))+~P9(f24(a1))), % 58.84/58.93 inference(scs_inference,[],[2358,112,2])). % 58.84/58.93 cnf(2392,plain, % 58.84/58.93 (~P10(a1)+P10(f24(f24(a1)))), % 58.84/58.93 inference(scs_inference,[],[2359,28])). % 58.84/58.93 cnf(2412,plain, % 58.84/58.93 (~P10(f24(f24(a1)))+P10(a1)), % 58.84/58.93 inference(scs_inference,[],[2358,28])). % 58.84/58.93 cnf(2430,plain, % 58.84/58.93 (~P10(f24(f24(a1)))+P14(f24(f24(a1)),f26(f24(f24(a1))))), % 58.84/58.93 inference(scs_inference,[],[89,2358,2361,2364,2369,156,2367,37,35,134,123,131])). % 58.84/58.93 cnf(2472,plain, % 58.84/58.93 (P14(f24(f24(a1)),f26(f24(f24(a1))))+~P10(a1)), % 58.84/58.93 inference(scs_inference,[],[2392,2430])). % 58.84/58.93 cnf(2517,plain, % 58.84/58.93 (P10(a1)+~P6(f24(f24(f24(a1))))), % 58.84/58.93 inference(scs_inference,[],[2369,2364,2412,123])). % 58.84/58.93 cnf(2615,plain, % 58.84/58.93 (~E(a8,f24(a2))), % 58.84/58.93 inference(scs_inference,[],[971,70,178,136])). % 58.84/58.93 cnf(2655,plain, % 58.84/58.93 (~E(a8,f24(f24(f24(a1))))), % 58.84/58.93 inference(scs_inference,[],[971,2369,2370,136])). % 58.84/58.93 cnf(2770,plain, % 58.84/58.93 (~P1(f24(f24(f24(a1))))+P10(a1)), % 58.84/58.93 inference(scs_inference,[],[2517,100])). % 58.84/58.93 cnf(2807,plain, % 58.84/58.93 (P8(f17(a2,a8),a8)), % 58.84/58.93 inference(scs_inference,[],[70,2615,178,134])). % 58.84/58.93 cnf(2842,plain, % 58.84/58.93 (P10(a1)), % 58.84/58.93 inference(scs_inference,[],[2362,2770,107])). % 58.84/58.93 cnf(2843,plain, % 58.84/58.93 (P10(f24(a21))), % 58.84/58.93 inference(scs_inference,[],[2842,678])). % 58.84/58.93 cnf(2845,plain, % 58.84/58.93 (P14(f24(f24(a3)),f26(f24(f24(a3))))), % 58.84/58.93 inference(scs_inference,[],[2842,2113])). % 58.84/58.93 cnf(2847,plain, % 58.84/58.93 (P14(f24(f24(a1)),f26(f24(f24(a1))))), % 58.84/58.93 inference(scs_inference,[],[2842,2472])). % 58.84/58.93 cnf(2860,plain, % 58.84/58.93 (P14(a1,f26(f24(f24(a1))))), % 58.84/58.93 inference(scs_inference,[],[2847,2358,29])). % 58.84/58.93 cnf(2862,plain, % 58.84/58.93 (~P1(a15)+~P1(f26(f24(f24(a1))))), % 58.84/58.93 inference(scs_inference,[],[96,2847,2358,29,30,106])). % 58.84/58.93 cnf(2878,plain, % 58.84/58.93 (P14(a1,f26(f24(f24(a3))))), % 58.84/58.93 inference(scs_inference,[],[2845,2036,29])). % 58.84/58.93 cnf(2917,plain, % 58.84/58.93 (~P1(a15)), % 58.84/58.93 inference(scs_inference,[],[2362,2862,108])). % 58.84/58.93 cnf(2918,plain, % 58.84/58.93 (P8(f19(a15),a15)), % 58.84/58.93 inference(scs_inference,[],[2917,91,125])). % 58.84/58.93 cnf(2945,plain, % 58.84/58.93 (E(f24(f24(a2)),a1)), % 58.84/58.93 inference(scs_inference,[],[42,1811,109])). % 58.84/58.93 cnf(2946,plain, % 58.84/58.93 (E(a1,f24(f24(a2)))), % 58.84/58.93 inference(scs_inference,[],[2945,2])). % 58.84/58.93 cnf(2947,plain, % 58.84/58.93 (P1(f24(f24(a2)))), % 58.84/58.93 inference(scs_inference,[],[2945,41,2,19])). % 58.84/58.93 cnf(2953,plain, % 58.84/58.93 (P9(f24(f24(a2)))), % 58.84/58.93 inference(scs_inference,[],[144,2945,68,41,62,54,58,79,2,19,31,34,3,33,32,22])). % 58.84/58.93 cnf(2955,plain, % 58.84/58.93 (P10(f24(f24(a2)))), % 58.84/58.93 inference(scs_inference,[],[144,2945,2842,68,41,62,54,58,79,84,2,19,31,34,3,33,32,22,36,28])). % 58.84/58.93 cnf(2956,plain, % 58.84/58.93 (P3(f24(f24(a2)))), % 58.84/58.93 inference(scs_inference,[],[144,46,2945,2842,68,41,62,54,58,79,84,2,19,31,34,3,33,32,22,36,28,25])). % 58.84/58.93 cnf(2957,plain, % 58.84/58.93 (P13(f24(f24(a2)),x29571)), % 58.84/58.93 inference(scs_inference,[],[144,46,2945,2842,68,41,62,54,58,79,84,2,19,31,34,3,33,32,22,36,28,25,393])). % 58.84/58.93 cnf(2973,plain, % 58.84/58.93 (P14(f24(f24(a2)),f26(f24(f24(a2))))), % 58.84/58.93 inference(scs_inference,[],[89,2953,2955,2956,131])). % 58.84/58.93 cnf(2977,plain, % 58.84/58.93 (P14(a1,f26(f24(f24(a2))))), % 58.84/58.93 inference(scs_inference,[],[89,2953,2955,2956,2946,2945,131,37,29])). % 58.84/58.93 cnf(2988,plain, % 58.84/58.93 (P14(f24(f24(a3)),f26(f24(f24(a2))))), % 58.84/58.93 inference(scs_inference,[],[2977,2037,29])). % 58.84/58.93 cnf(2999,plain, % 58.84/58.93 (P14(f24(f24(a2)),x29991)+~E(f26(f24(f24(a2))),x29991)), % 58.84/58.93 inference(scs_inference,[],[2973,30])). % 58.84/58.93 cnf(3006,plain, % 58.84/58.93 (P14(f24(f24(a3)),x30061)+~E(f26(f24(f24(a2))),x30061)), % 58.84/58.93 inference(scs_inference,[],[2988,30])). % 58.84/58.93 cnf(3074,plain, % 58.84/58.93 (P14(f24(a21),f26(f24(f24(a3))))), % 58.84/58.93 inference(scs_inference,[],[2245,2878,639,30,29])). % 58.84/58.93 cnf(3085,plain, % 58.84/58.93 (P14(f24(a21),f26(f24(f24(a1))))), % 58.84/58.93 inference(scs_inference,[],[2860,639,29])). % 58.84/58.93 cnf(3090,plain, % 58.84/58.93 (P14(f24(a21),f26(f24(f24(a2))))), % 58.84/58.93 inference(scs_inference,[],[2977,639,29])). % 58.84/58.93 cnf(3095,plain, % 58.84/58.93 (P14(f24(a21),x30951)+~E(f26(f24(f24(a2))),x30951)), % 58.84/58.93 inference(scs_inference,[],[3090,30])). % 58.84/58.93 cnf(3292,plain, % 58.84/58.93 (E(a1,f26(f24(a3)))), % 58.84/58.93 inference(scs_inference,[],[44,2075,109])). % 58.84/58.93 cnf(3294,plain, % 58.84/58.93 (E(f26(f24(a3)),a1)), % 58.84/58.93 inference(scs_inference,[],[3292,393,2])). % 58.84/58.93 cnf(3296,plain, % 58.84/58.93 (P3(f26(f24(a3)))), % 58.84/58.93 inference(scs_inference,[],[46,3292,58,393,2,31,25])). % 58.84/58.93 cnf(3297,plain, % 58.84/58.93 (P10(f26(f24(a3)))), % 58.84/58.93 inference(scs_inference,[],[46,3292,2842,58,393,2,31,25,28])). % 58.84/58.93 cnf(3300,plain, % 58.84/58.93 (P9(f26(f24(a3)))), % 58.84/58.93 inference(scs_inference,[],[46,3292,2842,68,54,58,79,393,2,31,25,28,32,34,22])). % 58.84/58.93 cnf(3301,plain, % 58.84/58.93 (E(f24(a21),f26(f24(a3)))), % 58.84/58.93 inference(scs_inference,[],[46,638,3292,2842,68,54,58,79,393,2,31,25,28,32,34,22,3])). % 58.84/58.93 cnf(3327,plain, % 58.84/58.93 (P14(a1,f26(f26(f24(a3))))), % 58.84/58.93 inference(scs_inference,[],[144,89,3294,3296,3297,3300,3301,2,3,131,29])). % 58.84/58.93 cnf(3335,plain, % 58.84/58.93 (P14(f24(a21),f26(f26(f24(a3))))), % 58.84/58.93 inference(scs_inference,[],[3327,639,29])). % 58.84/58.93 cnf(3455,plain, % 58.84/58.93 (P2(f19(f24(f24(a1))),a1)), % 58.84/58.93 inference(scs_inference,[],[2358,91,24])). % 58.84/58.93 cnf(3458,plain, % 58.84/58.93 (P14(f14(a1),f26(f24(a3)))), % 58.84/58.93 inference(scs_inference,[],[3085,950,2358,3301,91,24,29,30])). % 58.84/58.93 cnf(3464,plain, % 58.84/58.93 (P14(f26(f24(a3)),f26(f24(f24(a2))))), % 58.84/58.93 inference(scs_inference,[],[3090,3301,952,24,29])). % 58.84/58.93 cnf(3465,plain, % 58.84/58.93 (P14(f14(f24(f24(a1))),a1)), % 58.84/58.93 inference(scs_inference,[],[3090,2358,3301,90,952,24,29,30])). % 58.84/58.93 cnf(3471,plain, % 58.84/58.93 (P2(f19(f24(f24(a1))),f24(a21))), % 58.84/58.93 inference(scs_inference,[],[639,3455,24])). % 58.84/58.93 cnf(3509,plain, % 58.84/58.93 (P14(f26(f24(a3)),x35091)+~E(f26(f24(f24(a2))),x35091)), % 58.84/58.93 inference(scs_inference,[],[3464,30])). % 58.84/58.93 cnf(3757,plain, % 58.84/58.93 (E(a1,f26(f24(a1)))), % 58.84/58.93 inference(scs_inference,[],[41,2388,109])). % 58.84/58.93 cnf(3759,plain, % 58.84/58.93 (E(f26(f24(a1)),a1)), % 58.84/58.93 inference(scs_inference,[],[3757,393,2])). % 58.84/58.93 cnf(3763,plain, % 58.84/58.93 (P10(f26(f24(a1)))), % 58.84/58.93 inference(scs_inference,[],[3757,2842,41,58,79,393,2,19,31,34,28])). % 58.84/58.93 cnf(3765,plain, % 58.84/58.93 (P9(f26(f24(a1)))), % 58.84/58.93 inference(scs_inference,[],[3757,2842,68,41,54,58,79,393,2,19,31,34,28,32,22])). % 58.84/58.93 cnf(3768,plain, % 58.84/58.93 (E(f24(a21),f26(f24(a1)))), % 58.84/58.93 inference(scs_inference,[],[638,3757,2842,68,41,62,54,58,79,84,393,2,19,31,34,28,32,22,33,36,3])). % 58.84/58.93 cnf(3769,plain, % 58.84/58.93 (P3(f26(f24(a1)))), % 58.84/58.93 inference(scs_inference,[],[46,638,3757,2842,68,41,62,54,58,79,84,393,2,19,31,34,28,32,22,33,36,3,25])). % 58.84/58.93 cnf(3770,plain, % 58.84/58.93 (~P8(x37701,f26(f24(a1)))), % 58.84/58.93 inference(scs_inference,[],[46,638,3757,2842,68,41,62,54,58,79,84,393,2,19,31,34,28,32,22,33,36,3,25,120])). % 58.84/58.93 cnf(3784,plain, % 58.84/58.93 (E(f26(f24(a1)),f24(a21))), % 58.84/58.93 inference(scs_inference,[],[3768,2])). % 58.84/58.93 cnf(3785,plain, % 58.84/58.93 (~E(f14(a15),f26(f24(a1)))), % 58.84/58.93 inference(scs_inference,[],[144,3759,3768,2,3])). % 58.84/58.93 cnf(3790,plain, % 58.84/58.93 (P14(a1,f26(f26(f24(a1))))), % 58.84/58.93 inference(scs_inference,[],[144,89,3759,3763,3765,3769,3768,2,3,131,35,29])). % 58.84/58.93 cnf(3791,plain, % 58.84/58.93 (P14(f26(f24(a1)),x37911)+~E(f26(f26(f24(a1))),x37911)), % 58.84/58.93 inference(scs_inference,[],[144,89,3759,3763,3765,3769,3768,2,3,131,35,29,30])). % 58.84/58.93 cnf(3799,plain, % 58.84/58.93 (P14(f24(a21),f26(f26(f24(a1))))), % 58.84/58.93 inference(scs_inference,[],[96,3790,639,30,29])). % 58.84/58.93 cnf(3806,plain, % 58.84/58.93 (P14(f24(a21),x38061)+~E(f26(f26(f24(a1))),x38061)), % 58.84/58.93 inference(scs_inference,[],[3799,30])). % 58.84/58.93 cnf(3895,plain, % 58.84/58.93 (P14(a1,f26(a1))), % 58.84/58.93 inference(scs_inference,[],[68,821,3074,46,819,291,2359,89,3768,3765,2842,1234,3471,3770,27,29,30,24,23,136,131])). % 58.84/58.93 cnf(3917,plain, % 58.84/58.93 (P14(f26(f24(a1)),f26(f24(f24(a2))))), % 58.84/58.93 inference(scs_inference,[],[3090,3768,29])). % 58.84/58.93 cnf(3925,plain, % 58.84/58.93 (P14(f14(a1),f26(f24(a1)))), % 58.84/58.93 inference(scs_inference,[],[950,3335,3768,29,30])). % 58.84/58.93 cnf(3938,plain, % 58.84/58.93 (P14(f24(f24(a1)),f26(f24(f24(a2))))), % 58.84/58.93 inference(scs_inference,[],[2977,2359,29])). % 58.84/58.93 cnf(3958,plain, % 58.84/58.93 (P14(f24(f24(a1)),f26(f26(f24(a1))))), % 58.84/58.93 inference(scs_inference,[],[3790,2359,29])). % 58.84/58.93 cnf(3966,plain, % 58.84/58.93 (P14(f26(f24(a1)),x39661)+~E(f26(f24(f24(a2))),x39661)), % 58.84/58.93 inference(scs_inference,[],[3917,3895,2359,29,30])). % 58.84/58.93 cnf(4027,plain, % 58.84/58.93 (P14(f24(f24(a1)),x40271)+~E(f26(f24(f24(a2))),x40271)), % 58.84/58.93 inference(scs_inference,[],[3938,30])). % 58.84/58.93 cnf(4039,plain, % 58.84/58.93 (P14(f24(f24(a1)),x40391)+~E(f26(f26(f24(a1))),x40391)), % 58.84/58.93 inference(scs_inference,[],[3958,30])). % 58.84/58.93 cnf(4151,plain, % 58.84/58.93 (P13(f19(f25(a1)),f24(f24(a1)))), % 58.84/58.93 inference(scs_inference,[],[2359,139,27])). % 58.84/58.93 cnf(4153,plain, % 58.84/58.93 (P14(f14(a1),f24(f24(a1)))), % 58.84/58.93 inference(scs_inference,[],[2359,90,139,27,30])). % 58.84/58.93 cnf(4205,plain, % 58.84/58.93 (~P8(x42051,f19(f25(f24(f24(a1)))))), % 58.84/58.93 inference(scs_inference,[],[1375,2362,91,274,349,129])). % 58.84/58.93 cnf(4226,plain, % 58.84/58.93 (P8(f19(f22(f22(x42261,x42262),f23(x42262))),f22(f23(x42262),f22(x42262,x42261)))), % 58.84/58.93 inference(scs_inference,[],[1375,208,20])). % 58.84/58.93 cnf(4246,plain, % 58.84/58.93 (P1(f24(f24(f24(a2))))), % 58.84/58.93 inference(scs_inference,[],[2947,43,103,107])). % 58.84/58.93 cnf(4248,plain, % 58.84/58.93 (P1(f26(f24(f24(a2))))), % 58.84/58.93 inference(scs_inference,[],[2947,43,103,107,108])). % 58.84/58.93 cnf(4257,plain, % 58.84/58.93 (E(f19(f26(f24(a1))),f19(f24(a21)))), % 58.84/58.93 inference(scs_inference,[],[4151,2947,2807,3784,43,103,107,108,110,124,126,4,5])). % 58.84/58.93 cnf(4273,plain, % 58.84/58.93 (E(a21,a1)), % 58.84/58.93 inference(scs_inference,[],[4151,2947,2807,3784,43,103,107,108,110,124,126,4,5,9,15,16,6,7,10,11,17,18,12,13,14,3806,3791,4039,98])). % 58.84/58.93 cnf(4275,plain, % 58.84/58.93 (P3(a21)), % 58.84/58.93 inference(scs_inference,[],[4151,2947,2807,3784,43,103,107,108,110,124,126,4,5,9,15,16,6,7,10,11,17,18,12,13,14,3806,3791,4039,98,99])). % 58.84/58.93 cnf(4279,plain, % 58.84/58.93 (P3(f14(a1))), % 58.84/58.93 inference(scs_inference,[],[4151,4153,2947,2807,3784,43,103,107,108,110,124,126,4,5,9,15,16,6,7,10,11,17,18,12,13,14,3806,3791,4039,98,99,101,115])). % 58.84/58.93 cnf(4283,plain, % 58.84/58.93 (P9(f14(a1))), % 58.84/58.93 inference(scs_inference,[],[4151,4153,2947,2807,3784,43,103,107,108,110,124,126,4,5,9,15,16,6,7,10,11,17,18,12,13,14,3806,3791,4039,98,99,101,115,100,116])). % 58.84/58.93 cnf(4287,plain, % 58.84/58.93 (P9(a21)), % 58.84/58.93 inference(scs_inference,[],[4151,4153,2947,2807,3784,43,103,107,108,110,124,126,4,5,9,15,16,6,7,10,11,17,18,12,13,14,3806,3791,4039,98,99,101,115,100,116,109,105])). % 58.84/58.93 cnf(4291,plain, % 58.84/58.93 (P10(f14(a1))), % 58.84/58.93 inference(scs_inference,[],[3785,4151,4153,2947,2807,3784,43,103,107,108,110,124,126,4,5,9,15,16,6,7,10,11,17,18,12,13,14,3806,3791,4039,98,99,101,115,100,116,109,105,8,2,117])). % 58.84/58.93 cnf(4293,plain, % 58.84/58.93 (P10(a21)), % 58.84/58.93 inference(scs_inference,[],[3785,4151,4153,2947,2807,3784,43,103,107,108,110,124,126,4,5,9,15,16,6,7,10,11,17,18,12,13,14,3806,3791,4039,98,99,101,115,100,116,109,105,8,2,117,705])). % 58.84/58.93 cnf(4294,plain, % 58.84/58.93 (~P8(x42941,f24(f26(f24(a1))))), % 58.84/58.93 inference(scs_inference,[],[3785,4151,4153,2947,2807,3770,3784,3765,43,103,107,108,110,124,126,4,5,9,15,16,6,7,10,11,17,18,12,13,14,3806,3791,4039,98,99,101,115,100,116,109,105,8,2,117,705,138])). % 58.84/58.93 cnf(4297,plain, % 58.84/58.93 (P1(f19(f25(f24(a21))))), % 58.84/58.93 inference(scs_inference,[],[718,3785,4151,4153,2947,2807,3770,3784,3765,43,91,103,107,108,110,124,126,4,5,9,15,16,6,7,10,11,17,18,12,13,14,3806,3791,4039,98,99,101,115,100,116,109,105,8,2,117,705,138,125])). % 58.84/58.93 cnf(4304,plain, % 58.84/58.93 (~P1(f24(a7))), % 58.84/58.93 inference(scs_inference,[],[858,718,4226,3785,4151,4153,2947,2807,3770,3784,3765,93,43,73,91,103,107,108,110,124,126,4,5,9,15,16,6,7,10,11,17,18,12,13,14,3806,3791,4039,98,99,101,115,100,116,109,105,8,2,117,705,138,125,129,21,118])). % 58.84/58.93 cnf(4306,plain, % 58.84/58.93 (~P1(f26(a7))), % 58.84/58.93 inference(scs_inference,[],[858,718,4226,3785,4151,4153,2947,2807,3770,3784,3765,93,43,73,91,103,107,108,110,124,126,4,5,9,15,16,6,7,10,11,17,18,12,13,14,3806,3791,4039,98,99,101,115,100,116,109,105,8,2,117,705,138,125,129,21,118,119])). % 58.84/58.93 cnf(4308,plain, % 58.84/58.93 (~E(f24(a21),f14(a15))), % 58.84/58.93 inference(scs_inference,[],[858,718,4226,3785,4151,4153,2947,2807,3770,3784,3765,93,43,73,91,103,107,108,110,124,126,4,5,9,15,16,6,7,10,11,17,18,12,13,14,3806,3791,4039,98,99,101,115,100,116,109,105,8,2,117,705,138,125,129,21,118,119,3])). % 58.84/58.93 cnf(4310,plain, % 58.84/58.93 (E(f22(x43101,x43102),f22(x43102,x43101))), % 58.84/58.93 inference(rename_variables,[],[92])). % 58.84/58.93 cnf(4311,plain, % 58.84/58.93 (~E(f24(f24(a2)),a8)), % 58.84/58.93 inference(scs_inference,[],[858,718,4226,3785,4151,4153,2947,2807,3770,94,3784,3765,93,43,73,91,92,103,107,108,110,124,126,4,5,9,15,16,6,7,10,11,17,18,12,13,14,3806,3791,4039,98,99,101,115,100,116,109,105,8,2,117,705,138,125,129,21,118,119,3,23,19])). % 58.84/58.93 cnf(4312,plain, % 58.84/58.93 (~P14(f24(f24(a2)),a15)), % 58.84/58.93 inference(scs_inference,[],[96,858,718,4226,3785,4151,4153,2947,2807,3770,94,3784,3765,93,43,2945,73,91,92,103,107,108,110,124,126,4,5,9,15,16,6,7,10,11,17,18,12,13,14,3806,3791,4039,98,99,101,115,100,116,109,105,8,2,117,705,138,125,129,21,118,119,3,23,19,29])). % 58.84/58.93 cnf(4319,plain, % 58.84/58.93 (P8(f17(f24(f24(a1)),a8),a8)), % 58.84/58.93 inference(scs_inference,[],[96,87,858,718,4226,3785,4151,4153,2655,2947,2807,3770,82,94,3784,77,78,53,52,3765,93,2370,43,2945,2369,73,91,92,103,107,108,110,124,126,4,5,9,15,16,6,7,10,11,17,18,12,13,14,3806,3791,4039,98,99,101,115,100,116,109,105,8,2,117,705,138,125,129,21,118,119,3,23,19,29,121,114,122,134])). % 58.84/58.93 cnf(4325,plain, % 58.84/58.93 (P13(x43251,x43251)), % 58.84/58.93 inference(rename_variables,[],[89])). % 58.84/58.93 cnf(4334,plain, % 58.84/58.93 (P14(f14(f24(f24(a1))),f24(f24(a2)))), % 58.84/58.93 inference(scs_inference,[],[96,87,842,858,718,4226,3785,4151,4153,2655,2947,2807,3770,3799,82,2843,94,3465,49,3784,2946,77,78,644,53,52,3765,93,642,2370,43,72,2945,2369,73,89,91,92,103,107,108,110,124,126,4,5,9,15,16,6,7,10,11,17,18,12,13,14,3806,3791,4039,98,99,101,115,100,116,109,105,8,2,117,705,138,125,129,21,118,119,3,23,19,29,121,114,122,134,130,131,104,102,349,127,30])). % 58.84/58.93 cnf(4342,plain, % 58.84/58.93 (E(f26(a21),a1)), % 58.84/58.93 inference(scs_inference,[],[96,87,842,858,718,4226,967,1407,3785,4151,4153,2655,2947,2807,3770,3799,82,2843,94,3465,3455,49,3784,2946,77,78,644,53,52,3765,93,642,2370,43,72,2945,2369,73,89,4325,638,91,92,4310,103,107,108,110,124,126,4,5,9,15,16,6,7,10,11,17,18,12,13,14,3806,3791,4039,98,99,101,115,100,116,109,105,8,2,117,705,138,125,129,21,118,119,3,23,19,29,121,114,122,134,130,131,104,102,349,127,30,24,132,26,20,112])). % 58.84/58.93 cnf(4349,plain, % 58.84/58.93 (~E(a7,f24(a21))), % 58.84/58.93 inference(scs_inference,[],[4287,551])). % 58.84/58.93 cnf(4350,plain, % 58.84/58.93 (E(f24(a1),f24(a21))), % 58.84/58.93 inference(scs_inference,[],[4287,591])). % 58.84/58.93 cnf(4351,plain, % 58.84/58.93 (E(f24(a21),f24(a1))), % 58.84/58.93 inference(scs_inference,[],[4287,595])). % 58.84/58.93 cnf(4352,plain, % 58.84/58.93 (P8(f17(a21,f14(a15)),f14(a15))), % 58.84/58.93 inference(scs_inference,[],[4287,660])). % 58.84/58.93 cnf(4354,plain, % 58.84/58.93 (P13(f19(f25(f26(a21))),a1)), % 58.84/58.93 inference(scs_inference,[],[4287,1090])). % 58.84/58.93 cnf(4356,plain, % 58.84/58.93 (E(f14(f24(a21)),f14(f24(a1)))), % 58.84/58.93 inference(scs_inference,[],[4287,1279])). % 58.84/58.93 cnf(4358,plain, % 58.84/58.93 (P2(f24(f24(a2)),f25(x43581))), % 58.84/58.93 inference(scs_inference,[],[2957,126])). % 58.84/58.93 cnf(4364,plain, % 58.84/58.93 (P1(f26(f24(f24(f24(a2)))))), % 58.84/58.93 inference(scs_inference,[],[4246,2957,126,103,110,108])). % 58.84/58.93 cnf(4366,plain, % 58.84/58.93 (E(f17(a21,x43661),f17(a1,x43661))), % 58.84/58.93 inference(scs_inference,[],[4273,4246,2957,126,103,110,108,10])). % 58.84/58.93 cnf(4373,plain, % 58.84/58.93 (P3(f14(f24(f24(a1))))), % 58.84/58.93 inference(scs_inference,[],[4273,4246,4334,2957,126,103,110,108,10,107,101,11,7,115])). % 58.84/58.93 cnf(4375,plain, % 58.84/58.93 (E(f16(x43751,x43752,a21),f16(x43751,x43752,a1))), % 58.84/58.93 inference(scs_inference,[],[4273,4246,4334,2957,126,103,110,108,10,107,101,11,7,115,14])). % 58.84/58.93 cnf(4379,plain, % 58.84/58.93 (E(f24(f24(f24(a2))),a1)), % 58.84/58.93 inference(scs_inference,[],[4273,4246,4319,4334,2957,126,103,110,108,10,107,101,11,7,115,14,16,124,98])). % 58.84/58.93 cnf(4383,plain, % 58.84/58.93 (E(f16(a21,x43831,x43832),f16(a1,x43831,x43832))), % 58.84/58.93 inference(scs_inference,[],[4273,4246,4319,4334,2957,126,103,110,108,10,107,101,11,7,115,14,16,124,98,5,4,12])). % 58.84/58.93 cnf(4385,plain, % 58.84/58.93 (E(f16(x43851,a21,x43852),f16(x43851,a1,x43852))), % 58.84/58.93 inference(scs_inference,[],[4273,4246,4319,4334,2957,126,103,110,108,10,107,101,11,7,115,14,16,124,98,5,4,12,15,13])). % 58.84/58.93 cnf(4396,plain, % 58.84/58.93 (P9(f14(f24(f24(a1))))), % 58.84/58.93 inference(scs_inference,[],[4273,4246,4319,4334,2957,126,103,110,108,10,107,101,11,7,115,14,16,124,98,5,4,12,15,13,99,9,17,18,6,100,109,116])). % 58.84/58.93 cnf(4400,plain, % 58.84/58.93 (E(f24(f26(a21)),f24(a1))), % 58.84/58.93 inference(scs_inference,[],[4273,4342,4246,4297,4319,4334,2957,126,103,110,108,10,107,101,11,7,115,14,16,124,98,5,4,12,15,13,99,9,17,18,6,100,109,116,105,8])). % 58.84/58.93 cnf(4402,plain, % 58.84/58.93 (P10(f14(f24(f24(a1))))), % 58.84/58.93 inference(scs_inference,[],[4273,4342,4311,4246,4297,4319,4334,2957,126,103,110,108,10,107,101,11,7,115,14,16,124,98,5,4,12,15,13,99,9,17,18,6,100,109,116,105,8,2,117])). % 58.84/58.93 cnf(4404,plain, % 58.84/58.93 (P1(f24(f26(f24(a1))))), % 58.84/58.93 inference(scs_inference,[],[4273,4342,4311,4294,4246,4297,4319,4334,2957,91,126,103,110,108,10,107,101,11,7,115,14,16,124,98,5,4,12,15,13,99,9,17,18,6,100,109,116,105,8,2,117,125])). % 58.84/58.93 cnf(4406,plain, % 58.84/58.93 (P2(f19(x44061),x44061)), % 58.84/58.93 inference(rename_variables,[],[91])). % 58.84/58.93 cnf(4418,plain, % 58.84/58.93 (~E(a15,f24(a21))), % 58.84/58.93 inference(scs_inference,[],[96,4273,4287,203,4342,4279,4283,4291,4304,4308,4311,4294,4246,4297,4319,4257,4334,2957,2918,201,3301,91,4406,126,103,110,108,10,107,101,11,7,115,14,16,124,98,5,4,12,15,13,99,9,17,18,6,100,109,116,105,8,2,117,125,129,21,3,23,19,29,121,136])). % 58.84/58.93 cnf(4419,plain, % 58.84/58.93 (~P8(x44191,a21)), % 58.84/58.93 inference(rename_variables,[],[201])). % 58.84/58.93 cnf(4425,plain, % 58.84/58.93 (P13(f26(f14(a1)),f26(f24(a3)))), % 58.84/58.93 inference(scs_inference,[],[96,4273,4287,203,4342,4279,4283,4291,4304,4308,4311,4294,4246,4297,4319,4257,4334,2957,3458,2918,221,201,4419,3301,91,4406,126,103,110,108,10,107,101,11,7,115,14,16,124,98,5,4,12,15,13,99,9,17,18,6,100,109,116,105,8,2,117,125,129,21,3,23,19,29,121,136,134,130])). % 58.84/58.93 cnf(4430,plain, % 58.84/58.93 (~P2(f26(a21),f25(a15))), % 58.84/58.93 inference(scs_inference,[],[96,4273,4275,4287,4293,203,4342,4279,4283,4291,4304,4308,4311,4294,4246,4297,4319,4257,4334,2957,3458,2918,221,201,4419,3301,91,4406,126,103,110,108,10,107,101,11,7,115,14,16,124,98,5,4,12,15,13,99,9,17,18,6,100,109,116,105,8,2,117,125,129,21,3,23,19,29,121,136,134,130,131,371,128])). % 58.84/58.93 cnf(4432,plain, % 58.84/58.93 (~E(a1,f26(a21))), % 58.84/58.93 inference(scs_inference,[],[96,4273,4275,4287,4293,203,4342,4279,4283,4291,4304,4308,4311,4294,4246,4297,4319,4257,4334,2957,3458,2918,221,201,4419,3301,91,4406,126,103,110,108,10,107,101,11,7,115,14,16,124,98,5,4,12,15,13,99,9,17,18,6,100,109,116,105,8,2,117,125,129,21,3,23,19,29,121,136,134,130,131,371,128,393])). % 58.84/58.93 cnf(4453,plain, % 58.84/58.93 (P14(f14(f24(a1)),a1)), % 58.84/58.93 inference(scs_inference,[],[4356,824])). % 58.84/58.93 cnf(4504,plain, % 58.84/58.93 (P1(f19(f25(f24(f24(a1)))))), % 58.84/58.93 inference(scs_inference,[],[4350,4430,4418,4352,4356,4425,4248,4404,4205,2224,91,824,126,275,107,103,108,110,98,124,101,115,99,14,5,11,10,7,17,18,9,16,15,109,4,12,13,116,100,6,127,105,117,8,2,125])). % 58.84/58.93 cnf(4522,plain, % 58.84/58.93 (P13(f16(x45221,x45222,a1),f16(x45221,x45222,a21))), % 58.84/58.93 inference(scs_inference,[],[983,4350,4375,4351,4366,649,4430,4418,4352,4356,4425,4248,4404,4354,994,4205,2224,643,2843,2946,642,646,645,89,91,647,92,824,126,275,107,103,108,110,98,124,101,115,99,14,5,11,10,7,17,18,9,16,15,109,4,12,13,116,100,6,127,105,117,8,2,125,129,27,28,33,21,20,34,36,22,32,31,26])). % 58.84/58.93 cnf(4536,plain, % 58.84/58.93 (P8(f17(a21,a7),a7)), % 58.84/58.93 inference(scs_inference,[],[96,983,4349,4350,4375,4383,4351,4366,649,4306,4430,4418,4352,4358,4400,4356,4425,4248,4373,4396,4402,4404,4354,4379,994,4205,2224,643,2843,4287,2946,142,201,642,646,645,68,89,91,647,92,824,126,275,107,103,108,110,98,124,101,115,99,14,5,11,10,7,17,18,9,16,15,109,4,12,13,116,100,6,127,105,117,8,2,125,129,27,28,33,21,20,34,36,22,32,31,26,23,3,19,29,121,136,134])). % 58.84/58.93 cnf(4543,plain, % 58.84/58.93 (P1(f24(a1))), % 58.84/58.93 inference(scs_inference,[],[96,983,4349,4350,4375,4383,4351,4366,649,4306,4430,4418,4352,4358,4400,4356,4425,4248,4373,4396,4402,4404,4354,4379,994,4205,4312,2224,2955,3925,643,4279,4291,2843,4287,2956,4283,2946,142,201,642,2953,646,645,68,89,91,647,92,824,126,275,107,103,108,110,98,124,101,115,99,14,5,11,10,7,17,18,9,16,15,109,4,12,13,116,100,6,127,105,117,8,2,125,129,27,28,33,21,20,34,36,22,32,31,26,23,3,19,29,121,136,134,130,131,2372])). % 58.84/58.93 cnf(4544,plain, % 58.84/58.93 (P8(f17(f24(a1),a7),a7)), % 58.84/58.93 inference(scs_inference,[],[96,983,4349,4350,4375,4383,4351,4366,649,4306,4430,4418,4352,4358,4400,4356,4425,4248,4373,4396,4402,4404,4354,4379,994,4205,4312,2224,2955,3925,643,4279,4291,2843,4287,2956,4283,2946,142,201,642,2953,646,645,68,89,91,647,92,824,126,275,107,103,108,110,98,124,101,115,99,14,5,11,10,7,17,18,9,16,15,109,4,12,13,116,100,6,127,105,117,8,2,125,129,27,28,33,21,20,34,36,22,32,31,26,23,3,19,29,121,136,134,130,131,2372,511])). % 58.84/58.93 cnf(4551,plain, % 58.84/58.93 (~P2(f26(f24(f24(a2))),f25(a15))), % 58.84/58.93 inference(scs_inference,[],[96,983,4349,4350,4375,4383,4351,4366,649,4306,4430,4418,4352,4358,4400,4356,4425,4248,4373,4396,4402,4404,4354,4379,994,4205,4312,2224,2955,3925,643,4279,4291,2843,4287,2956,4283,2946,142,201,642,2953,646,645,68,89,91,647,92,824,126,275,107,103,108,110,98,124,101,115,99,14,5,11,10,7,17,18,9,16,15,109,4,12,13,116,100,6,127,105,117,8,2,125,129,27,28,33,21,20,34,36,22,32,31,26,23,3,19,29,121,136,134,130,131,2372,511,3095,2999,3006,3509,3966,4027,128])). % 58.84/58.93 cnf(4625,plain, % 58.84/58.93 ($false), % 58.84/58.93 inference(scs_inference,[],[4385,4522,4432,4543,4536,4453,4544,4551,4364,4504,4297,4342,126,108,107,275,110,98,103,115,101,124,5,11,14,99,116,109,9,15,13,16,10,17,18,7,100,127,12,4,105,6,117,8,2]), % 58.84/58.93 ['proof']). % 58.84/58.93 % SZS output end Proof % 58.84/58.93 % Total time :58.270000s %------------------------------------------------------------------------------