%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SEU112+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 : n023.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:01:04 EDT 2024 % Result : Theorem 50.52s 50.67s % Output : CNFRefutation 50.57s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.12 % Problem : SEU112+1 : TPTP v8.2.0. Released v3.2.0. % 0.02/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.10/0.32 % Computer : n023.cluster.edu % 0.10/0.32 % Model : x86_64 x86_64 % 0.10/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.32 % Memory : 8042.1875MB % 0.10/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.32 % CPULimit : 300 % 0.10/0.32 % WCLimit : 300 % 0.10/0.32 % DateTime : Fri Jun 21 17:43:24 EDT 2024 % 0.10/0.32 % CPUTime : % 0.49/0.55 start to proof:theBenchmark % 50.45/50.65 %------------------------------------------- % 50.45/50.65 % File :CSE---1.7 % 50.45/50.65 % Problem :theBenchmark % 50.45/50.65 % Transform :cnf % 50.45/50.65 % Format :tptp:raw % 50.45/50.65 % Command :java -jar mcs_scs.jar %d %s % 50.45/50.65 % 50.45/50.65 % Result :Theorem 49.970000s % 50.45/50.65 % Output :CNFRefutation 49.970000s % 50.45/50.65 %------------------------------------------- % 50.52/50.66 %------------------------------------------------------------------------------ % 50.52/50.66 % File : SEU112+1 : TPTP v8.2.0. Released v3.2.0. % 50.52/50.66 % Domain : Set theory % 50.52/50.66 % Problem : Boolean domains, theorem 25 % 50.52/50.66 % Version : [Urb06] axioms : Especial. % 50.52/50.66 % English : % 50.52/50.66 % 50.52/50.66 % Refs : [TD90] Trybulec & Darmochwal (1990), Boolean Domains % 50.52/50.66 % : [Urb06] Urban (2006), Email to G. Sutcliffe % 50.52/50.66 % Source : [Urb06] % 50.52/50.66 % Names : finsub_1__t25_finsub_1 [Urb06] % 50.52/50.66 % 50.52/50.66 % Status : Theorem % 50.52/50.66 % Rating : 0.14 v8.2.0, 0.17 v8.1.0, 0.19 v7.5.0, 0.22 v7.4.0, 0.17 v7.0.0, 0.13 v6.4.0, 0.19 v6.3.0, 0.21 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.0.0, 0.12 v4.1.0, 0.17 v4.0.1, 0.26 v4.0.0, 0.25 v3.7.0, 0.15 v3.5.0, 0.16 v3.4.0, 0.26 v3.3.0, 0.21 v3.2.0 % 50.52/50.66 % Syntax : Number of formulae : 40 ( 12 unt; 0 def) % 50.52/50.67 % Number of atoms : 97 ( 5 equ) % 50.52/50.67 % Maximal formula atoms : 10 ( 2 avg) % 50.52/50.67 % Number of connectives : 78 ( 21 ~; 1 |; 36 &) % 50.52/50.67 % ( 1 <=>; 19 =>; 0 <=; 0 <~>) % 50.52/50.67 % Maximal formula depth : 12 ( 4 avg) % 50.52/50.67 % Maximal term depth : 3 ( 1 avg) % 50.52/50.67 % Number of predicates : 17 ( 16 usr; 0 prp; 1-2 aty) % 50.52/50.67 % Number of functors : 4 ( 4 usr; 1 con; 0-2 aty) % 50.52/50.67 % Number of variables : 68 ( 58 !; 10 ?) % 50.52/50.67 % SPC : FOF_THM_RFO_SEQ % 50.52/50.67 % 50.52/50.67 % Comments : Translated by MPTP 0.2 from the original problem in the Mizar % 50.52/50.67 % library, www.mizar.org % 50.52/50.67 %------------------------------------------------------------------------------ % 50.52/50.67 fof(antisymmetry_r2_hidden,axiom, % 50.52/50.67 ! [A,B] : % 50.52/50.67 ( in(A,B) % 50.52/50.67 => ~ in(B,A) ) ). % 50.52/50.67 % 50.52/50.67 fof(cc1_finset_1,axiom, % 50.52/50.67 ! [A] : % 50.52/50.67 ( empty(A) % 50.52/50.67 => finite(A) ) ). % 50.52/50.67 % 50.52/50.67 fof(cc1_finsub_1,axiom, % 50.52/50.67 ! [A] : % 50.52/50.67 ( preboolean(A) % 50.52/50.67 => ( cup_closed(A) % 50.52/50.67 & diff_closed(A) ) ) ). % 50.52/50.67 % 50.52/50.67 fof(cc2_finset_1,axiom, % 50.52/50.67 ! [A] : % 50.52/50.67 ( finite(A) % 50.52/50.67 => ! [B] : % 50.52/50.67 ( element(B,powerset(A)) % 50.52/50.67 => finite(B) ) ) ). % 50.52/50.67 % 50.52/50.67 fof(cc2_finsub_1,axiom, % 50.52/50.67 ! [A] : % 50.52/50.67 ( ( cup_closed(A) % 50.52/50.67 & diff_closed(A) ) % 50.52/50.67 => preboolean(A) ) ). % 50.52/50.67 % 50.52/50.67 fof(cc3_finsub_1,axiom, % 50.52/50.67 ! [A,B] : % 50.52/50.67 ( element(B,finite_subsets(A)) % 50.52/50.67 => finite(B) ) ). % 50.52/50.67 % 50.52/50.67 fof(commutativity_k2_xboole_0,axiom, % 50.52/50.67 ! [A,B] : set_union2(A,B) = set_union2(B,A) ). % 50.52/50.67 % 50.52/50.67 fof(dt_k5_finsub_1,axiom, % 50.52/50.67 ! [A] : preboolean(finite_subsets(A)) ). % 50.52/50.67 % 50.52/50.67 fof(existence_m1_subset_1,axiom, % 50.52/50.67 ! [A] : % 50.52/50.67 ? [B] : element(B,A) ). % 50.52/50.67 % 50.52/50.67 fof(fc1_finsub_1,axiom, % 50.52/50.67 ! [A] : % 50.52/50.67 ( ~ empty(powerset(A)) % 50.52/50.67 & cup_closed(powerset(A)) % 50.52/50.67 & diff_closed(powerset(A)) % 50.52/50.67 & preboolean(powerset(A)) ) ). % 50.52/50.67 % 50.52/50.67 fof(fc1_subset_1,axiom, % 50.52/50.67 ! [A] : ~ empty(powerset(A)) ). % 50.52/50.67 % 50.52/50.67 fof(fc1_xboole_0,axiom, % 50.52/50.67 empty(empty_set) ). % 50.52/50.67 % 50.52/50.67 fof(fc2_finsub_1,axiom, % 50.52/50.67 ! [A] : % 50.52/50.67 ( ~ empty(finite_subsets(A)) % 50.52/50.67 & cup_closed(finite_subsets(A)) % 50.52/50.67 & diff_closed(finite_subsets(A)) % 50.52/50.67 & preboolean(finite_subsets(A)) ) ). % 50.52/50.67 % 50.52/50.67 fof(fc2_xboole_0,axiom, % 50.52/50.67 ! [A,B] : % 50.52/50.67 ( ~ empty(A) % 50.52/50.67 => ~ empty(set_union2(A,B)) ) ). % 50.52/50.67 % 50.52/50.67 fof(fc3_xboole_0,axiom, % 50.52/50.67 ! [A,B] : % 50.52/50.67 ( ~ empty(A) % 50.52/50.67 => ~ empty(set_union2(B,A)) ) ). % 50.52/50.67 % 50.52/50.67 fof(fc9_finset_1,axiom, % 50.52/50.67 ! [A,B] : % 50.52/50.67 ( ( finite(A) % 50.52/50.67 & finite(B) ) % 50.52/50.67 => finite(set_union2(A,B)) ) ). % 50.52/50.67 % 50.52/50.67 fof(idempotence_k2_xboole_0,axiom, % 50.52/50.67 ! [A,B] : set_union2(A,A) = A ). % 50.52/50.67 % 50.52/50.67 fof(rc1_finset_1,axiom, % 50.52/50.67 ? [A] : % 50.52/50.67 ( ~ empty(A) % 50.52/50.67 & finite(A) ) ). % 50.52/50.67 % 50.52/50.67 fof(rc1_finsub_1,axiom, % 50.52/50.67 ? [A] : % 50.52/50.67 ( ~ empty(A) % 50.52/50.67 & cup_closed(A) % 50.52/50.67 & cap_closed(A) % 50.52/50.67 & diff_closed(A) % 50.52/50.67 & preboolean(A) ) ). % 50.52/50.67 % 50.52/50.67 fof(rc1_subset_1,axiom, % 50.52/50.67 ! [A] : % 50.52/50.67 ( ~ empty(A) % 50.52/50.67 => ? [B] : % 50.52/50.67 ( element(B,powerset(A)) % 50.52/50.67 & ~ empty(B) ) ) ). % 50.52/50.67 % 50.52/50.67 fof(rc1_xboole_0,axiom, % 50.52/50.67 ? [A] : empty(A) ). % 50.52/50.67 % 50.52/50.67 fof(rc2_finset_1,axiom, % 50.52/50.67 ! [A] : % 50.52/50.67 ? [B] : % 50.52/50.67 ( element(B,powerset(A)) % 50.52/50.67 & empty(B) % 50.52/50.67 & relation(B) % 50.52/50.67 & function(B) % 50.52/50.67 & one_to_one(B) % 50.52/50.67 & epsilon_transitive(B) % 50.52/50.67 & epsilon_connected(B) % 50.52/50.67 & ordinal(B) % 50.52/50.67 & natural(B) % 50.52/50.67 & finite(B) ) ). % 50.52/50.67 % 50.52/50.67 fof(rc2_subset_1,axiom, % 50.52/50.67 ! [A] : % 50.52/50.67 ? [B] : % 50.52/50.67 ( element(B,powerset(A)) % 50.52/50.67 & empty(B) ) ). % 50.52/50.67 % 50.52/50.67 fof(rc2_xboole_0,axiom, % 50.52/50.67 ? [A] : ~ empty(A) ). % 50.52/50.67 % 50.52/50.67 fof(rc3_finset_1,axiom, % 50.52/50.67 ! [A] : % 50.52/50.67 ( ~ empty(A) % 50.52/50.67 => ? [B] : % 50.52/50.67 ( element(B,powerset(A)) % 50.52/50.67 & ~ empty(B) % 50.52/50.67 & finite(B) ) ) ). % 50.52/50.67 % 50.52/50.67 fof(rc4_finset_1,axiom, % 50.52/50.67 ! [A] : % 50.52/50.67 ( ~ empty(A) % 50.52/50.67 => ? [B] : % 50.52/50.67 ( element(B,powerset(A)) % 50.52/50.67 & ~ empty(B) % 50.52/50.67 & finite(B) ) ) ). % 50.52/50.67 % 50.52/50.67 fof(reflexivity_r1_tarski,axiom, % 50.52/50.67 ! [A,B] : subset(A,A) ). % 50.52/50.67 % 50.52/50.67 fof(t1_boole,axiom, % 50.52/50.67 ! [A] : set_union2(A,empty_set) = A ). % 50.52/50.67 % 50.52/50.67 fof(t1_subset,axiom, % 50.52/50.67 ! [A,B] : % 50.52/50.67 ( in(A,B) % 50.52/50.67 => element(A,B) ) ). % 50.52/50.67 % 50.52/50.67 fof(t23_finsub_1,axiom, % 50.52/50.67 ! [A,B] : % 50.52/50.67 ( subset(A,B) % 50.52/50.67 => subset(finite_subsets(A),finite_subsets(B)) ) ). % 50.52/50.67 % 50.52/50.67 fof(t25_finsub_1,conjecture, % 50.52/50.67 ! [A,B] : subset(set_union2(finite_subsets(A),finite_subsets(B)),finite_subsets(set_union2(A,B))) ). % 50.52/50.67 % 50.52/50.67 fof(t2_subset,axiom, % 50.52/50.67 ! [A,B] : % 50.52/50.67 ( element(A,B) % 50.52/50.67 => ( empty(B) % 50.52/50.67 | in(A,B) ) ) ). % 50.52/50.67 % 50.52/50.67 fof(t3_subset,axiom, % 50.52/50.67 ! [A,B] : % 50.52/50.67 ( element(A,powerset(B)) % 50.52/50.67 <=> subset(A,B) ) ). % 50.52/50.67 % 50.52/50.67 fof(t4_subset,axiom, % 50.52/50.67 ! [A,B,C] : % 50.52/50.67 ( ( in(A,B) % 50.52/50.67 & element(B,powerset(C)) ) % 50.52/50.67 => element(A,C) ) ). % 50.52/50.67 % 50.52/50.67 fof(t5_subset,axiom, % 50.52/50.67 ! [A,B,C] : % 50.52/50.67 ~ ( in(A,B) % 50.52/50.67 & element(B,powerset(C)) % 50.52/50.67 & empty(C) ) ). % 50.52/50.67 % 50.52/50.67 fof(t6_boole,axiom, % 50.52/50.67 ! [A] : % 50.52/50.67 ( empty(A) % 50.52/50.67 => A = empty_set ) ). % 50.52/50.67 % 50.52/50.67 fof(t7_boole,axiom, % 50.52/50.67 ! [A,B] : % 50.52/50.67 ~ ( in(A,B) % 50.52/50.67 & empty(B) ) ). % 50.52/50.67 % 50.52/50.67 fof(t7_xboole_1,axiom, % 50.52/50.67 ! [A,B] : subset(A,set_union2(A,B)) ). % 50.52/50.67 % 50.52/50.67 fof(t8_boole,axiom, % 50.52/50.67 ! [A,B] : % 50.52/50.67 ~ ( empty(A) % 50.52/50.67 & A != B % 50.52/50.67 & empty(B) ) ). % 50.52/50.67 % 50.52/50.67 fof(t8_xboole_1,axiom, % 50.52/50.67 ! [A,B,C] : % 50.52/50.67 ( ( subset(A,B) % 50.52/50.67 & subset(C,B) ) % 50.52/50.67 => subset(set_union2(A,C),B) ) ). % 50.52/50.67 % 50.52/50.67 %------------------------------------------------------------------------------ % 50.52/50.67 %------------------------------------------- % 50.52/50.67 % Proof found % 50.52/50.67 % SZS status Theorem for theBenchmark % 50.52/50.67 % SZS output start Proof % 50.52/50.67 %ClaNum:100(EqnAxiom:32) % 50.52/50.67 %VarNum:135(SingletonVarNum:76) % 50.52/50.67 %MaxLitNum:3 % 50.52/50.67 %MaxfuncDepth:2 % 50.52/50.67 %SharedTerms:23 % 50.52/50.67 %goalClause: 71 % 50.52/50.67 %singleGoalClaCount:1 % 50.52/50.67 [33]P1(a1) % 50.52/50.67 [34]P1(a2) % 50.52/50.67 [35]P6(a3) % 50.52/50.67 [36]P9(a8) % 50.52/50.67 [37]P2(a8) % 50.52/50.67 [38]P4(a8) % 50.52/50.67 [39]P3(a8) % 50.52/50.67 [65]~P1(a3) % 50.52/50.67 [66]~P1(a8) % 50.52/50.67 [67]~P1(a14) % 50.52/50.67 [71]~P16(f16(f13(a5),f13(a7)),f13(f16(a5,a7))) % 50.52/50.67 [58]P16(x581,x581) % 50.52/50.67 [40]P1(f10(x401)) % 50.52/50.67 [41]P1(f11(x411)) % 50.52/50.67 [42]P6(f10(x421)) % 50.52/50.67 [43]P9(f12(x431)) % 50.52/50.67 [45]P9(f13(x451)) % 50.52/50.67 [46]P2(f12(x461)) % 50.52/50.67 [47]P2(f13(x471)) % 50.52/50.67 [48]P4(f12(x481)) % 50.52/50.67 [49]P4(f13(x491)) % 50.52/50.67 [50]P15(f10(x501)) % 50.52/50.67 [51]P10(f10(x511)) % 50.52/50.67 [52]P11(f10(x521)) % 50.52/50.67 [53]P7(f10(x531)) % 50.52/50.67 [54]P8(f10(x541)) % 50.52/50.67 [55]P14(f10(x551)) % 50.52/50.67 [56]P12(f10(x561)) % 50.52/50.67 [57]E(f16(x571,a1),x571) % 50.52/50.67 [59]E(f16(x591,x591),x591) % 50.52/50.67 [60]P5(f4(x601),x601) % 50.52/50.67 [61]P5(f10(x611),f12(x611)) % 50.52/50.67 [62]P5(f11(x621),f12(x621)) % 50.52/50.67 [69]~P1(f12(x691)) % 50.52/50.67 [70]~P1(f13(x701)) % 50.52/50.67 [63]E(f16(x631,x632),f16(x632,x631)) % 50.52/50.67 [64]P16(x641,f16(x641,x642)) % 50.52/50.67 [72]~P1(x721)+E(x721,a1) % 50.52/50.67 [73]~P1(x731)+P6(x731) % 50.52/50.67 [74]~P9(x741)+P2(x741) % 50.52/50.67 [75]~P9(x751)+P4(x751) % 50.52/50.67 [76]P1(x761)+P6(f15(x761)) % 50.52/50.67 [77]P1(x771)+P6(f6(x771)) % 50.52/50.67 [80]P1(x801)+~P1(f9(x801)) % 50.52/50.67 [81]P1(x811)+~P1(f15(x811)) % 50.52/50.67 [82]P1(x821)+~P1(f6(x821)) % 50.52/50.67 [84]P1(x841)+P5(f9(x841),f12(x841)) % 50.52/50.67 [85]P1(x851)+P5(f15(x851),f12(x851)) % 50.52/50.67 [86]P1(x861)+P5(f6(x861),f12(x861)) % 50.52/50.67 [83]~P1(x831)+~P13(x832,x831) % 50.52/50.67 [88]~P13(x881,x882)+P5(x881,x882) % 50.52/50.67 [93]~P13(x932,x931)+~P13(x931,x932) % 50.52/50.67 [87]P6(x871)+~P5(x871,f13(x872)) % 50.52/50.67 [90]~P16(x901,x902)+P5(x901,f12(x902)) % 50.52/50.67 [94]P16(x941,x942)+~P5(x941,f12(x942)) % 50.52/50.67 [95]~P16(x951,x952)+P16(f13(x951),f13(x952)) % 50.52/50.67 [96]P1(x961)+~P1(f16(x962,x961)) % 50.52/50.67 [97]P1(x971)+~P1(f16(x971,x972)) % 50.52/50.67 [79]~P2(x791)+~P4(x791)+P9(x791) % 50.52/50.67 [78]~P1(x782)+~P1(x781)+E(x781,x782) % 50.52/50.67 [89]~P5(x892,x891)+P1(x891)+P13(x892,x891) % 50.52/50.67 [91]P6(x911)+~P6(x912)+~P5(x911,f12(x912)) % 50.52/50.67 [92]~P6(x922)+~P6(x921)+P6(f16(x921,x922)) % 50.52/50.67 [98]~P1(x981)+~P13(x982,x983)+~P5(x983,f12(x981)) % 50.52/50.67 [99]P5(x991,x992)+~P13(x991,x993)+~P5(x993,f12(x992)) % 50.52/50.67 [100]~P16(x1002,x1003)+~P16(x1001,x1003)+P16(f16(x1001,x1002),x1003) % 50.52/50.67 %EqnAxiom % 50.52/50.67 [1]E(x11,x11) % 50.52/50.67 [2]E(x22,x21)+~E(x21,x22) % 50.52/50.67 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 50.52/50.67 [4]~E(x41,x42)+E(f10(x41),f10(x42)) % 50.52/50.67 [5]~E(x51,x52)+E(f11(x51),f11(x52)) % 50.52/50.67 [6]~E(x61,x62)+E(f16(x61,x63),f16(x62,x63)) % 50.52/50.67 [7]~E(x71,x72)+E(f16(x73,x71),f16(x73,x72)) % 50.52/50.67 [8]~E(x81,x82)+E(f12(x81),f12(x82)) % 50.52/50.67 [9]~E(x91,x92)+E(f13(x91),f13(x92)) % 50.52/50.67 [10]~E(x101,x102)+E(f15(x101),f15(x102)) % 50.52/50.67 [11]~E(x111,x112)+E(f9(x111),f9(x112)) % 50.52/50.67 [12]~E(x121,x122)+E(f6(x121),f6(x122)) % 50.52/50.67 [13]~E(x131,x132)+E(f4(x131),f4(x132)) % 50.52/50.67 [14]~P1(x141)+P1(x142)+~E(x141,x142) % 50.52/50.67 [15]P16(x152,x153)+~E(x151,x152)+~P16(x151,x153) % 50.52/50.67 [16]P16(x163,x162)+~E(x161,x162)+~P16(x163,x161) % 50.52/50.67 [17]~P6(x171)+P6(x172)+~E(x171,x172) % 50.52/50.67 [18]~P9(x181)+P9(x182)+~E(x181,x182) % 50.52/50.67 [19]~P2(x191)+P2(x192)+~E(x191,x192) % 50.52/50.67 [20]~P4(x201)+P4(x202)+~E(x201,x202) % 50.52/50.67 [21]~P3(x211)+P3(x212)+~E(x211,x212) % 50.52/50.67 [22]P5(x222,x223)+~E(x221,x222)+~P5(x221,x223) % 50.52/50.67 [23]P5(x233,x232)+~E(x231,x232)+~P5(x233,x231) % 50.52/50.67 [24]P13(x242,x243)+~E(x241,x242)+~P13(x241,x243) % 50.52/50.67 [25]P13(x253,x252)+~E(x251,x252)+~P13(x253,x251) % 50.52/50.67 [26]~P8(x261)+P8(x262)+~E(x261,x262) % 50.52/50.67 [27]~P7(x271)+P7(x272)+~E(x271,x272) % 50.52/50.67 [28]~P11(x281)+P11(x282)+~E(x281,x282) % 50.52/50.67 [29]~P10(x291)+P10(x292)+~E(x291,x292) % 50.52/50.67 [30]~P15(x301)+P15(x302)+~E(x301,x302) % 50.52/50.67 [31]~P12(x311)+P12(x312)+~E(x311,x312) % 50.52/50.67 [32]~P14(x321)+P14(x322)+~E(x321,x322) % 50.52/50.67 % 50.52/50.67 %------------------------------------------- % 50.57/50.68 cnf(101,plain, % 50.57/50.68 (P16(f4(f12(x1011)),x1011)), % 50.57/50.68 inference(scs_inference,[],[60,94])). % 50.57/50.68 cnf(102,plain, % 50.57/50.68 (P5(f4(x1021),x1021)), % 50.57/50.68 inference(rename_variables,[],[60])). % 50.57/50.68 cnf(104,plain, % 50.57/50.68 (E(x1041,f16(x1041,x1041))), % 50.57/50.68 inference(scs_inference,[],[59,60,94,2])). % 50.57/50.68 cnf(107,plain, % 50.57/50.68 (P6(f4(f13(x1071)))), % 50.57/50.68 inference(scs_inference,[],[59,60,102,33,94,2,83,87])). % 50.57/50.68 cnf(108,plain, % 50.57/50.68 (P5(f4(x1081),x1081)), % 50.57/50.68 inference(rename_variables,[],[60])). % 50.57/50.68 cnf(111,plain, % 50.57/50.68 (P16(x1111,x1111)), % 50.57/50.68 inference(rename_variables,[],[58])). % 50.57/50.68 cnf(114,plain, % 50.57/50.68 (P13(f4(a3),a3)), % 50.57/50.68 inference(scs_inference,[],[71,58,111,59,60,102,108,65,33,94,2,83,87,15,16,89])). % 50.57/50.68 cnf(115,plain, % 50.57/50.68 (P5(f4(x1151),x1151)), % 50.57/50.68 inference(rename_variables,[],[60])). % 50.57/50.68 cnf(118,plain, % 50.57/50.68 (E(f16(x1181,x1182),f16(x1182,x1181))), % 50.57/50.68 inference(rename_variables,[],[63])). % 50.57/50.68 cnf(120,plain, % 50.57/50.68 (P5(f4(f16(x1201,x1202)),f16(x1202,x1201))), % 50.57/50.68 inference(scs_inference,[],[71,58,111,59,60,102,108,115,63,118,65,33,94,2,83,87,15,16,89,3,22,23])). % 50.57/50.68 cnf(121,plain, % 50.57/50.68 (P5(f4(x1211),x1211)), % 50.57/50.68 inference(rename_variables,[],[60])). % 50.57/50.68 cnf(123,plain, % 50.57/50.68 (P5(f4(x1231),x1231)), % 50.57/50.68 inference(rename_variables,[],[60])). % 50.57/50.68 cnf(125,plain, % 50.57/50.68 (~P13(x1251,f4(f12(a1)))), % 50.57/50.68 inference(scs_inference,[],[71,58,111,59,60,102,108,115,121,123,63,118,65,33,35,94,2,83,87,15,16,89,3,22,23,91,98])). % 50.57/50.68 cnf(128,plain, % 50.57/50.68 (~P1(f16(a3,a1))), % 50.57/50.68 inference(scs_inference,[],[71,58,111,59,60,102,108,115,121,123,63,118,57,65,33,35,94,2,83,87,15,16,89,3,22,23,91,98,14])). % 50.57/50.68 cnf(130,plain, % 50.57/50.68 (~E(a3,a1)), % 50.57/50.68 inference(scs_inference,[],[71,58,111,59,60,102,108,115,121,123,63,118,57,65,33,35,94,2,83,87,15,16,89,3,22,23,91,98,14,25])). % 50.57/50.68 cnf(135,plain, % 50.57/50.68 (~P16(a7,f16(a5,a7))+~P16(f13(a5),f13(f16(a5,a7)))), % 50.57/50.68 inference(scs_inference,[],[71,58,111,59,60,102,108,115,121,123,63,118,57,65,33,35,94,2,83,87,15,16,89,3,22,23,91,98,14,25,93,100,95])). % 50.57/50.68 cnf(140,plain, % 50.57/50.68 (P16(f10(x1401),x1401)), % 50.57/50.68 inference(scs_inference,[],[61,94])). % 50.57/50.68 cnf(144,plain, % 50.57/50.68 (E(x1441,f16(x1441,a1))), % 50.57/50.68 inference(scs_inference,[],[61,57,34,94,83,2])). % 50.57/50.68 cnf(145,plain, % 50.57/50.68 (P3(f16(a8,a8))), % 50.57/50.68 inference(scs_inference,[],[104,61,57,34,39,94,83,2,21])). % 50.57/50.68 cnf(146,plain, % 50.57/50.68 (E(x1461,f16(x1461,x1461))), % 50.57/50.68 inference(rename_variables,[],[104])). % 50.57/50.68 cnf(147,plain, % 50.57/50.68 (P13(f16(f4(a3),f4(a3)),a3)), % 50.57/50.68 inference(scs_inference,[],[104,146,61,57,114,34,39,94,83,2,21,24])). % 50.57/50.68 cnf(148,plain, % 50.57/50.68 (E(x1481,f16(x1481,x1481))), % 50.57/50.68 inference(rename_variables,[],[104])). % 50.57/50.68 cnf(149,plain, % 50.57/50.68 (P8(f16(f10(x1491),f10(x1491)))), % 50.57/50.68 inference(scs_inference,[],[104,146,148,61,57,114,34,39,54,94,83,2,21,24,26])). % 50.57/50.68 cnf(150,plain, % 50.57/50.68 (E(x1501,f16(x1501,x1501))), % 50.57/50.68 inference(rename_variables,[],[104])). % 50.57/50.68 cnf(151,plain, % 50.57/50.68 (P7(f16(f10(x1511),f10(x1511)))), % 50.57/50.68 inference(scs_inference,[],[104,146,148,150,61,57,114,34,39,53,54,94,83,2,21,24,26,27])). % 50.57/50.68 cnf(152,plain, % 50.57/50.68 (E(x1521,f16(x1521,x1521))), % 50.57/50.68 inference(rename_variables,[],[104])). % 50.57/50.68 cnf(153,plain, % 50.57/50.68 (P11(f16(f10(x1531),f10(x1531)))), % 50.57/50.68 inference(scs_inference,[],[104,146,148,150,152,61,57,114,34,39,52,53,54,94,83,2,21,24,26,27,28])). % 50.57/50.68 cnf(154,plain, % 50.57/50.68 (E(x1541,f16(x1541,x1541))), % 50.57/50.68 inference(rename_variables,[],[104])). % 50.57/50.68 cnf(155,plain, % 50.57/50.68 (P10(f16(f10(x1551),f10(x1551)))), % 50.57/50.68 inference(scs_inference,[],[104,146,148,150,152,154,61,57,114,34,39,51,52,53,54,94,83,2,21,24,26,27,28,29])). % 50.57/50.68 cnf(156,plain, % 50.57/50.68 (E(x1561,f16(x1561,x1561))), % 50.57/50.68 inference(rename_variables,[],[104])). % 50.57/50.68 cnf(157,plain, % 50.57/50.68 (P15(f16(f10(x1571),f10(x1571)))), % 50.57/50.68 inference(scs_inference,[],[104,146,148,150,152,154,156,61,57,114,34,39,50,51,52,53,54,94,83,2,21,24,26,27,28,29,30])). % 50.57/50.68 cnf(158,plain, % 50.57/50.68 (E(x1581,f16(x1581,x1581))), % 50.57/50.68 inference(rename_variables,[],[104])). % 50.57/50.68 cnf(159,plain, % 50.57/50.68 (P12(f16(f10(x1591),f10(x1591)))), % 50.57/50.68 inference(scs_inference,[],[104,146,148,150,152,154,156,158,61,57,114,34,39,50,51,52,53,54,56,94,83,2,21,24,26,27,28,29,30,31])). % 50.57/50.68 cnf(160,plain, % 50.57/50.68 (E(x1601,f16(x1601,x1601))), % 50.57/50.68 inference(rename_variables,[],[104])). % 50.57/50.68 cnf(161,plain, % 50.57/50.68 (P14(f16(f10(x1611),f10(x1611)))), % 50.57/50.68 inference(scs_inference,[],[104,146,148,150,152,154,156,158,160,61,57,114,34,39,50,51,52,53,54,55,56,94,83,2,21,24,26,27,28,29,30,31,32])). % 50.57/50.68 cnf(162,plain, % 50.57/50.68 (E(x1621,f16(x1621,x1621))), % 50.57/50.68 inference(rename_variables,[],[104])). % 50.57/50.68 cnf(163,plain, % 50.57/50.68 (P13(f4(f16(a1,a3)),f16(a3,a1))), % 50.57/50.68 inference(scs_inference,[],[104,146,148,150,152,154,156,158,160,120,61,57,128,114,34,39,50,51,52,53,54,55,56,94,83,2,21,24,26,27,28,29,30,31,32,89])). % 50.57/50.68 cnf(164,plain, % 50.57/50.68 (P5(f4(f16(x1641,x1642)),f16(x1642,x1641))), % 50.57/50.68 inference(rename_variables,[],[120])). % 50.57/50.68 cnf(169,plain, % 50.57/50.68 (P16(f16(x1691,x1691),f16(x1691,x1692))), % 50.57/50.68 inference(scs_inference,[],[104,146,148,150,152,154,156,158,160,162,120,61,62,64,57,107,128,114,34,39,50,51,52,53,54,55,56,94,83,2,21,24,26,27,28,29,30,31,32,89,91,15])). % 50.57/50.68 cnf(171,plain, % 50.57/50.68 (P4(f16(a8,a8))), % 50.57/50.68 inference(scs_inference,[],[104,146,148,150,152,154,156,158,160,162,120,61,62,64,57,107,128,114,38,34,39,50,51,52,53,54,55,56,94,83,2,21,24,26,27,28,29,30,31,32,89,91,15,20])). % 50.57/50.68 cnf(172,plain, % 50.57/50.68 (E(x1721,f16(x1721,x1721))), % 50.57/50.68 inference(rename_variables,[],[104])). % 50.57/50.69 cnf(175,plain, % 50.57/50.69 (P5(f16(f10(x1751),f10(x1751)),f12(x1751))), % 50.57/50.69 inference(scs_inference,[],[104,146,148,150,152,154,156,158,160,162,172,120,61,62,64,57,107,125,128,114,38,34,39,50,51,52,53,54,55,56,94,83,2,21,24,26,27,28,29,30,31,32,89,91,15,20,25,22])). % 50.57/50.69 cnf(176,plain, % 50.57/50.69 (E(x1761,f16(x1761,x1761))), % 50.57/50.69 inference(rename_variables,[],[104])). % 50.57/50.69 cnf(177,plain, % 50.57/50.69 (~P13(x1771,f10(a2))), % 50.57/50.69 inference(scs_inference,[],[104,146,148,150,152,154,156,158,160,162,172,120,61,62,64,57,107,125,128,114,38,34,39,50,51,52,53,54,55,56,94,83,2,21,24,26,27,28,29,30,31,32,89,91,15,20,25,22,98])). % 50.57/50.69 cnf(180,plain, % 50.57/50.69 (E(f16(x1801,x1802),f16(f16(x1802,x1801),f16(x1802,x1801)))), % 50.57/50.69 inference(scs_inference,[],[104,146,148,150,152,154,156,158,160,162,172,176,120,61,62,64,63,57,107,125,128,114,38,34,39,50,51,52,53,54,55,56,94,83,2,21,24,26,27,28,29,30,31,32,89,91,15,20,25,22,98,3])). % 50.57/50.69 cnf(181,plain, % 50.57/50.69 (E(x1811,f16(x1811,x1811))), % 50.57/50.69 inference(rename_variables,[],[104])). % 50.57/50.69 cnf(182,plain, % 50.57/50.69 (P1(f16(a2,a2))), % 50.57/50.69 inference(scs_inference,[],[104,146,148,150,152,154,156,158,160,162,172,176,181,120,61,62,64,63,57,107,125,128,114,38,34,39,50,51,52,53,54,55,56,94,83,2,21,24,26,27,28,29,30,31,32,89,91,15,20,25,22,98,3,14])). % 50.57/50.69 cnf(183,plain, % 50.57/50.69 (E(x1831,f16(x1831,x1831))), % 50.57/50.69 inference(rename_variables,[],[104])). % 50.57/50.69 cnf(184,plain, % 50.57/50.69 (P6(f16(f4(f13(x1841)),a1))), % 50.57/50.69 inference(scs_inference,[],[104,146,148,150,152,154,156,158,160,162,172,176,181,120,61,62,64,63,57,107,125,128,114,38,34,39,50,51,52,53,54,55,56,94,83,2,21,24,26,27,28,29,30,31,32,89,91,15,20,25,22,98,3,14,17])). % 50.57/50.69 cnf(185,plain, % 50.57/50.69 (P2(f16(a8,a8))), % 50.57/50.69 inference(scs_inference,[],[104,146,148,150,152,154,156,158,160,162,172,176,181,183,120,61,62,64,63,57,107,125,128,114,38,34,37,39,50,51,52,53,54,55,56,94,83,2,21,24,26,27,28,29,30,31,32,89,91,15,20,25,22,98,3,14,17,19])). % 50.57/50.69 cnf(186,plain, % 50.57/50.69 (E(x1861,f16(x1861,x1861))), % 50.57/50.69 inference(rename_variables,[],[104])). % 50.57/50.69 cnf(188,plain, % 50.57/50.69 (E(x1881,f16(x1881,x1881))), % 50.57/50.69 inference(rename_variables,[],[104])). % 50.57/50.69 cnf(189,plain, % 50.57/50.69 (P16(f4(f12(x1891)),f16(x1891,x1891))), % 50.57/50.69 inference(scs_inference,[],[101,104,146,148,150,152,154,156,158,160,162,172,176,181,183,186,188,120,164,61,62,64,63,57,107,125,128,114,38,34,37,39,50,51,52,53,54,55,56,94,83,2,21,24,26,27,28,29,30,31,32,89,91,15,20,25,22,98,3,14,17,19,23,16])). % 50.57/50.69 cnf(191,plain, % 50.57/50.69 (P9(f16(a8,a8))), % 50.57/50.69 inference(scs_inference,[],[101,104,146,148,150,152,154,156,158,160,162,172,176,181,183,186,188,120,164,61,62,64,63,57,107,125,128,114,38,34,36,37,39,50,51,52,53,54,55,56,94,83,2,21,24,26,27,28,29,30,31,32,89,91,15,20,25,22,98,3,14,17,19,23,16,18])). % 50.57/50.69 cnf(206,plain, % 50.57/50.69 (E(f16(f16(x2061,x2062),f16(x2061,x2062)),f16(x2062,x2061))), % 50.57/50.69 inference(scs_inference,[],[175,180,163,182,93,83,94,2])). % 50.57/50.69 cnf(207,plain, % 50.57/50.69 (P7(f16(f16(f10(x2071),f10(x2071)),a1))), % 50.57/50.69 inference(scs_inference,[],[175,180,144,151,163,182,93,83,94,2,27])). % 50.57/50.69 cnf(208,plain, % 50.57/50.69 (E(x2081,f16(x2081,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(209,plain, % 50.57/50.69 (P13(f4(a8),a8)), % 50.57/50.69 inference(scs_inference,[],[60,175,180,144,151,163,182,66,93,83,94,2,27,89])). % 50.57/50.69 cnf(210,plain, % 50.57/50.69 (P5(f4(x2101),x2101)), % 50.57/50.69 inference(rename_variables,[],[60])). % 50.57/50.69 cnf(212,plain, % 50.57/50.69 (P13(f16(f4(f16(a1,a3)),a1),f16(a3,a1))), % 50.57/50.69 inference(scs_inference,[],[60,175,180,144,208,151,163,182,66,93,83,94,2,27,89,24])). % 50.57/50.69 cnf(213,plain, % 50.57/50.69 (E(x2131,f16(x2131,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(214,plain, % 50.57/50.69 (P3(f16(f16(a8,a8),f16(a8,a8)))), % 50.57/50.69 inference(scs_inference,[],[60,175,180,144,208,151,163,145,182,66,93,83,94,2,27,89,24,21])). % 50.57/50.69 cnf(215,plain, % 50.57/50.69 (E(f16(x2151,x2152),f16(f16(x2152,x2151),f16(x2152,x2151)))), % 50.57/50.69 inference(rename_variables,[],[180])). % 50.57/50.69 cnf(216,plain, % 50.57/50.69 (P10(f16(f16(f10(x2161),f10(x2161)),a1))), % 50.57/50.69 inference(scs_inference,[],[60,175,180,144,208,213,151,155,163,145,182,66,93,83,94,2,27,89,24,21,29])). % 50.57/50.69 cnf(217,plain, % 50.57/50.69 (E(x2171,f16(x2171,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(218,plain, % 50.57/50.69 (P11(f16(f16(f10(x2181),f10(x2181)),a1))), % 50.57/50.69 inference(scs_inference,[],[60,175,180,144,208,213,217,151,153,155,163,145,182,66,93,83,94,2,27,89,24,21,29,28])). % 50.57/50.69 cnf(219,plain, % 50.57/50.69 (E(x2191,f16(x2191,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(220,plain, % 50.57/50.69 (P12(f16(f16(f10(x2201),f10(x2201)),a1))), % 50.57/50.69 inference(scs_inference,[],[60,175,180,144,208,213,217,219,151,153,155,159,163,145,182,66,93,83,94,2,27,89,24,21,29,28,31])). % 50.57/50.69 cnf(221,plain, % 50.57/50.69 (E(x2211,f16(x2211,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(222,plain, % 50.57/50.69 (P15(f16(f16(f10(x2221),f10(x2221)),a1))), % 50.57/50.69 inference(scs_inference,[],[60,175,180,144,208,213,217,219,221,151,153,155,157,159,163,145,182,66,93,83,94,2,27,89,24,21,29,28,31,30])). % 50.57/50.69 cnf(223,plain, % 50.57/50.69 (E(x2231,f16(x2231,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(224,plain, % 50.57/50.69 (P8(f16(f16(f10(x2241),f10(x2241)),a1))), % 50.57/50.69 inference(scs_inference,[],[60,175,180,144,208,213,217,219,221,223,149,151,153,155,157,159,163,145,182,66,93,83,94,2,27,89,24,21,29,28,31,30,26])). % 50.57/50.69 cnf(225,plain, % 50.57/50.69 (E(x2251,f16(x2251,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(226,plain, % 50.57/50.69 (P16(f16(f4(f12(x2261)),a1),f16(x2261,x2261))), % 50.57/50.69 inference(scs_inference,[],[189,60,175,180,144,208,213,217,219,221,223,225,149,151,153,155,157,159,163,145,182,66,93,83,94,2,27,89,24,21,29,28,31,30,26,15])). % 50.57/50.69 cnf(227,plain, % 50.57/50.69 (E(x2271,f16(x2271,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(228,plain, % 50.57/50.69 (P14(f16(f16(f10(x2281),f10(x2281)),a1))), % 50.57/50.69 inference(scs_inference,[],[189,60,175,180,144,208,213,217,219,221,223,225,227,149,151,153,155,157,159,161,163,145,182,66,93,83,94,2,27,89,24,21,29,28,31,30,26,15,32])). % 50.57/50.69 cnf(229,plain, % 50.57/50.69 (E(x2291,f16(x2291,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(230,plain, % 50.57/50.69 (~P13(x2301,f4(f12(f16(a2,a2))))), % 50.57/50.69 inference(scs_inference,[],[189,60,210,175,180,144,208,213,217,219,221,223,225,227,149,151,153,155,157,159,161,163,145,182,66,93,83,94,2,27,89,24,21,29,28,31,30,26,15,32,98])). % 50.57/50.69 cnf(231,plain, % 50.57/50.69 (P5(f4(x2311),x2311)), % 50.57/50.69 inference(rename_variables,[],[60])). % 50.57/50.69 cnf(237,plain, % 50.57/50.69 (P4(f16(f16(a8,a8),f16(a8,a8)))), % 50.57/50.69 inference(scs_inference,[],[189,60,210,175,180,215,144,208,213,217,219,221,223,225,227,63,149,151,153,155,157,159,161,171,177,184,163,145,182,66,93,83,94,2,27,89,24,21,29,28,31,30,26,15,32,98,25,17,20])). % 50.57/50.69 cnf(238,plain, % 50.57/50.69 (E(f16(x2381,x2382),f16(f16(x2382,x2381),f16(x2382,x2381)))), % 50.57/50.69 inference(rename_variables,[],[180])). % 50.57/50.69 cnf(239,plain, % 50.57/50.69 (P2(f16(f16(a8,a8),f16(a8,a8)))), % 50.57/50.69 inference(scs_inference,[],[189,60,210,175,180,215,238,144,208,213,217,219,221,223,225,227,63,149,151,153,155,157,159,161,185,171,177,184,163,145,182,66,93,83,94,2,27,89,24,21,29,28,31,30,26,15,32,98,25,17,20,19])). % 50.57/50.69 cnf(240,plain, % 50.57/50.69 (E(f16(x2401,x2402),f16(f16(x2402,x2401),f16(x2402,x2401)))), % 50.57/50.69 inference(rename_variables,[],[180])). % 50.57/50.69 cnf(241,plain, % 50.57/50.69 (P1(f16(f16(a2,a2),f16(a2,a2)))), % 50.57/50.69 inference(scs_inference,[],[189,60,210,175,180,215,238,240,144,208,213,217,219,221,223,225,227,63,149,151,153,155,157,159,161,185,171,177,184,163,145,182,66,93,83,94,2,27,89,24,21,29,28,31,30,26,15,32,98,25,17,20,19,14])). % 50.57/50.69 cnf(242,plain, % 50.57/50.69 (E(f16(x2421,x2422),f16(f16(x2422,x2421),f16(x2422,x2421)))), % 50.57/50.69 inference(rename_variables,[],[180])). % 50.57/50.69 cnf(243,plain, % 50.57/50.69 (P5(f16(f4(x2431),a1),x2431)), % 50.57/50.69 inference(scs_inference,[],[189,60,210,231,175,180,215,238,240,144,208,213,217,219,221,223,225,227,229,63,149,151,153,155,157,159,161,185,171,177,184,163,145,182,66,93,83,94,2,27,89,24,21,29,28,31,30,26,15,32,98,25,17,20,19,14,22])). % 50.57/50.69 cnf(244,plain, % 50.57/50.69 (E(x2441,f16(x2441,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(247,plain, % 50.57/50.69 (P9(f16(f16(a8,a8),f16(a8,a8)))), % 50.57/50.69 inference(scs_inference,[],[140,189,60,210,231,175,180,215,238,240,242,144,208,213,217,219,221,223,225,227,229,63,149,151,153,155,157,159,161,191,185,171,177,184,163,145,182,66,93,83,94,2,27,89,24,21,29,28,31,30,26,15,32,98,25,17,20,19,14,22,16,18])). % 50.57/50.69 cnf(248,plain, % 50.57/50.69 (E(f16(x2481,x2482),f16(f16(x2482,x2481),f16(x2482,x2481)))), % 50.57/50.69 inference(rename_variables,[],[180])). % 50.57/50.69 cnf(249,plain, % 50.57/50.69 (E(x2491,f16(f16(a1,x2491),f16(a1,x2491)))), % 50.57/50.69 inference(scs_inference,[],[140,189,60,210,231,175,180,215,238,240,242,248,144,208,213,217,219,221,223,225,227,229,244,63,149,151,153,155,157,159,161,191,185,171,177,184,163,145,182,66,93,83,94,2,27,89,24,21,29,28,31,30,26,15,32,98,25,17,20,19,14,22,16,18,3])). % 50.57/50.69 cnf(261,plain, % 50.57/50.69 (~P13(x2611,f16(f16(a2,a2),f16(a2,a2)))), % 50.57/50.69 inference(scs_inference,[],[241,212,93,83])). % 50.57/50.69 cnf(268,plain, % 50.57/50.69 (E(f16(x2681,x2682),f16(x2682,x2681))), % 50.57/50.69 inference(rename_variables,[],[63])). % 50.57/50.69 cnf(269,plain, % 50.57/50.69 (P13(f4(a14),a14)), % 50.57/50.69 inference(scs_inference,[],[60,249,243,63,241,207,212,67,93,83,94,2,27,89])). % 50.57/50.69 cnf(270,plain, % 50.57/50.69 (P5(f4(x2701),x2701)), % 50.57/50.69 inference(rename_variables,[],[60])). % 50.57/50.69 cnf(273,plain, % 50.57/50.69 (E(f16(x2731,x2732),f16(x2732,x2731))), % 50.57/50.69 inference(rename_variables,[],[63])). % 50.57/50.69 cnf(274,plain, % 50.57/50.69 (P3(f16(f16(f16(a8,a8),f16(a8,a8)),a1))), % 50.57/50.69 inference(scs_inference,[],[60,249,243,144,63,268,214,241,207,216,212,67,93,83,94,2,27,89,29,21])). % 50.57/50.69 cnf(275,plain, % 50.57/50.69 (E(x2751,f16(x2751,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(277,plain, % 50.57/50.69 (E(f16(x2771,x2772),f16(x2772,x2771))), % 50.57/50.69 inference(rename_variables,[],[63])). % 50.57/50.69 cnf(278,plain, % 50.57/50.69 (P16(f16(x2781,x2782),f16(f16(x2782,x2781),x2783))), % 50.57/50.69 inference(scs_inference,[],[169,60,206,249,243,144,63,268,273,214,241,207,216,228,212,67,93,83,94,2,27,89,29,21,32,15])). % 50.57/50.69 cnf(280,plain, % 50.57/50.69 (~P13(x2801,f11(f16(a2,a2)))), % 50.57/50.69 inference(scs_inference,[],[169,60,206,249,243,144,62,63,268,273,182,214,241,207,216,228,212,67,93,83,94,2,27,89,29,21,32,15,98])). % 50.57/50.69 cnf(284,plain, % 50.57/50.69 (E(f16(x2841,x2842),f16(x2842,x2841))), % 50.57/50.69 inference(rename_variables,[],[63])). % 50.57/50.69 cnf(286,plain, % 50.57/50.69 (E(f16(x2861,x2862),f16(x2862,x2861))), % 50.57/50.69 inference(rename_variables,[],[63])). % 50.57/50.69 cnf(288,plain, % 50.57/50.69 (E(f16(x2881,x2882),f16(x2882,x2881))), % 50.57/50.69 inference(rename_variables,[],[63])). % 50.57/50.69 cnf(293,plain, % 50.57/50.69 (P4(f16(f16(a8,a8),a1))), % 50.57/50.69 inference(scs_inference,[],[169,60,206,249,243,144,275,62,63,268,273,277,284,286,288,182,171,214,230,241,207,216,218,220,222,224,228,212,67,93,83,94,2,27,89,29,21,32,15,98,28,26,31,25,30,20])). % 50.57/50.69 cnf(294,plain, % 50.57/50.69 (E(x2941,f16(x2941,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(295,plain, % 50.57/50.69 (P1(f16(f16(a2,a2),a1))), % 50.57/50.69 inference(scs_inference,[],[169,60,206,249,243,144,275,294,62,63,268,273,277,284,286,288,182,171,214,230,241,207,216,218,220,222,224,228,212,67,93,83,94,2,27,89,29,21,32,15,98,28,26,31,25,30,20,14])). % 50.57/50.69 cnf(296,plain, % 50.57/50.69 (E(x2961,f16(x2961,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(301,plain, % 50.57/50.69 (E(f16(f16(x3011,x3012),f16(x3011,x3012)),f16(f16(x3012,x3011),f16(x3012,x3011)))), % 50.57/50.69 inference(scs_inference,[],[140,169,60,270,206,249,243,104,144,275,294,62,63,268,273,277,284,286,288,182,171,214,230,241,207,216,218,220,222,224,228,212,67,93,83,94,2,27,89,29,21,32,15,98,28,26,31,25,30,20,14,16,23,3])). % 50.57/50.69 cnf(303,plain, % 50.57/50.69 (P2(f16(f16(f16(a8,a8),f16(a8,a8)),a1))), % 50.57/50.69 inference(scs_inference,[],[140,169,60,270,206,249,243,104,144,275,294,296,62,63,268,273,277,284,286,288,182,171,239,214,230,241,207,216,218,220,222,224,228,212,67,93,83,94,2,27,89,29,21,32,15,98,28,26,31,25,30,20,14,16,23,3,19])). % 50.57/50.69 cnf(304,plain, % 50.57/50.69 (E(x3041,f16(x3041,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(305,plain, % 50.57/50.69 (P9(f16(f16(f16(a8,a8),f16(a8,a8)),a1))), % 50.57/50.69 inference(scs_inference,[],[140,169,60,270,206,249,243,104,144,275,294,296,304,62,63,268,273,277,284,286,288,182,171,247,239,214,230,241,207,216,218,220,222,224,228,212,67,93,83,94,2,27,89,29,21,32,15,98,28,26,31,25,30,20,14,16,23,3,19,18])). % 50.57/50.69 cnf(313,plain, % 50.57/50.69 (~P13(x3131,f16(f16(a2,a2),a1))), % 50.57/50.69 inference(scs_inference,[],[295,83])). % 50.57/50.69 cnf(317,plain, % 50.57/50.69 (P16(f11(x3171),x3171)), % 50.57/50.69 inference(scs_inference,[],[62,295,209,83,93,94])). % 50.57/50.69 cnf(319,plain, % 50.57/50.69 (P13(f4(f12(x3191)),f12(x3191))), % 50.57/50.69 inference(scs_inference,[],[60,62,295,209,69,83,93,94,89])). % 50.57/50.69 cnf(320,plain, % 50.57/50.69 (P5(f4(x3201),x3201)), % 50.57/50.69 inference(rename_variables,[],[60])). % 50.57/50.69 cnf(322,plain, % 50.57/50.69 (~P13(x3221,f10(f16(a2,a2)))), % 50.57/50.69 inference(scs_inference,[],[60,62,61,182,295,209,69,83,93,94,89,98])). % 50.57/50.69 cnf(326,plain, % 50.57/50.69 (E(f16(x3261,x3262),f16(x3262,x3261))), % 50.57/50.69 inference(rename_variables,[],[63])). % 50.57/50.69 cnf(329,plain, % 50.57/50.69 (P16(x3291,f16(f16(a1,x3291),x3292))), % 50.57/50.69 inference(scs_inference,[],[278,57,60,62,61,63,182,280,274,295,147,209,69,83,93,94,89,98,21,25,15])). % 50.57/50.69 cnf(332,plain, % 50.57/50.69 (E(f16(x3321,x3322),f16(x3322,x3321))), % 50.57/50.69 inference(rename_variables,[],[63])). % 50.57/50.69 cnf(335,plain, % 50.57/50.69 (E(f16(x3351,a1),f16(x3351,x3351))), % 50.57/50.69 inference(scs_inference,[],[101,278,57,60,104,62,61,63,326,182,280,303,274,295,147,209,69,83,93,94,89,98,21,25,15,19,16,3])). % 50.57/50.69 cnf(339,plain, % 50.57/50.69 (P5(f4(f16(x3391,a1)),x3391)), % 50.57/50.69 inference(scs_inference,[],[101,278,57,60,320,104,62,61,63,326,332,182,280,305,303,274,295,147,209,69,83,93,94,89,98,21,25,15,19,16,3,18,23])). % 50.57/50.69 cnf(354,plain, % 50.57/50.69 (~P13(x3541,f10(x3542))), % 50.57/50.69 inference(scs_inference,[],[319,40,93,83])). % 50.57/50.69 cnf(357,plain, % 50.57/50.69 (P5(f4(f16(x3571,a1)),x3571)), % 50.57/50.69 inference(rename_variables,[],[339])). % 50.57/50.69 cnf(359,plain, % 50.57/50.69 (E(f16(x3591,x3591),f16(x3591,a1))), % 50.57/50.69 inference(scs_inference,[],[339,335,319,40,93,83,94,2])). % 50.57/50.69 cnf(360,plain, % 50.57/50.69 (P13(f16(f4(f12(x3601)),a1),f12(x3601))), % 50.57/50.69 inference(scs_inference,[],[144,339,335,319,40,93,83,94,2,24])). % 50.57/50.69 cnf(361,plain, % 50.57/50.69 (E(x3611,f16(x3611,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(362,plain, % 50.57/50.69 (P13(f16(f4(f13(x3621)),a1),f13(x3621))), % 50.57/50.69 inference(scs_inference,[],[243,144,339,335,319,70,40,93,83,94,2,24,89])). % 50.57/50.69 cnf(363,plain, % 50.57/50.69 (P5(f16(f4(x3631),a1),x3631)), % 50.57/50.69 inference(rename_variables,[],[243])). % 50.57/50.69 cnf(365,plain, % 50.57/50.69 (P7(f16(f10(x3651),a1))), % 50.57/50.69 inference(scs_inference,[],[243,144,339,335,319,70,151,40,93,83,94,2,24,89,27])). % 50.57/50.69 cnf(368,plain, % 50.57/50.69 (P11(f16(f10(x3681),a1))), % 50.57/50.69 inference(scs_inference,[],[243,144,339,335,212,319,322,70,151,153,40,93,83,94,2,24,89,27,25,28])). % 50.57/50.69 cnf(369,plain, % 50.57/50.69 (P10(f16(f10(x3691),a1))), % 50.57/50.69 inference(scs_inference,[],[243,144,339,335,212,319,322,70,151,153,155,40,93,83,94,2,24,89,27,25,28,29])). % 50.57/50.69 cnf(370,plain, % 50.57/50.69 (P15(f16(f10(x3701),a1))), % 50.57/50.69 inference(scs_inference,[],[243,144,339,335,212,319,322,70,151,153,155,157,40,93,83,94,2,24,89,27,25,28,29,30])). % 50.57/50.69 cnf(371,plain, % 50.57/50.69 (P4(f16(f16(f16(a8,a8),a1),a1))), % 50.57/50.69 inference(scs_inference,[],[243,144,361,339,335,293,212,319,322,70,151,153,155,157,40,93,83,94,2,24,89,27,25,28,29,30,20])). % 50.57/50.69 cnf(372,plain, % 50.57/50.69 (E(x3721,f16(x3721,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(373,plain, % 50.57/50.69 (P14(f16(f10(x3731),a1))), % 50.57/50.69 inference(scs_inference,[],[243,144,361,339,335,293,212,319,322,70,151,153,155,157,161,40,93,83,94,2,24,89,27,25,28,29,30,20,32])). % 50.57/50.69 cnf(374,plain, % 50.57/50.69 (P8(f16(f10(x3741),a1))), % 50.57/50.69 inference(scs_inference,[],[243,144,361,339,335,293,212,319,322,70,149,151,153,155,157,161,40,93,83,94,2,24,89,27,25,28,29,30,20,32,26])). % 50.57/50.69 cnf(375,plain, % 50.57/50.69 (P12(f16(f10(x3751),a1))), % 50.57/50.69 inference(scs_inference,[],[243,144,361,339,335,293,212,319,322,70,149,151,153,155,157,159,161,40,93,83,94,2,24,89,27,25,28,29,30,20,32,26,31])). % 50.57/50.69 cnf(382,plain, % 50.57/50.69 (E(f16(x3821,x3821),f16(f16(a1,x3821),f16(a1,x3821)))), % 50.57/50.69 inference(scs_inference,[],[317,329,59,243,144,361,372,339,357,335,249,293,212,319,322,70,149,151,153,155,157,159,161,40,93,83,94,2,24,89,27,25,28,29,30,20,32,26,31,15,22,16,3])). % 50.57/50.69 cnf(388,plain, % 50.57/50.69 (P1(f16(f16(a1,a2),f16(a1,a2)))), % 50.57/50.69 inference(scs_inference,[],[317,329,59,243,363,144,361,372,339,357,335,249,182,293,212,319,322,70,149,151,153,155,157,159,161,40,93,83,94,2,24,89,27,25,28,29,30,20,32,26,31,15,22,16,3,23,79,14])). % 50.57/50.69 cnf(389,plain, % 50.57/50.69 (P1(f16(a1,a2))), % 50.57/50.69 inference(scs_inference,[],[317,329,59,243,363,144,361,372,339,357,335,249,182,293,212,319,322,70,149,151,153,155,157,159,161,40,93,83,94,2,24,89,27,25,28,29,30,20,32,26,31,15,22,16,3,23,79,14,96])). % 50.57/50.69 cnf(396,plain, % 50.57/50.69 (~P13(x3961,f16(a1,a2))), % 50.57/50.69 inference(scs_inference,[],[389,83])). % 50.57/50.69 cnf(400,plain, % 50.57/50.69 (E(f16(f16(a1,x4001),f16(a1,x4001)),f16(x4001,x4001))), % 50.57/50.69 inference(scs_inference,[],[382,360,389,83,93,2])). % 50.57/50.69 cnf(401,plain, % 50.57/50.69 (P13(f4(f13(x4011)),f13(x4011))), % 50.57/50.69 inference(scs_inference,[],[57,382,360,362,389,83,93,2,24])). % 50.57/50.69 cnf(403,plain, % 50.57/50.69 (P13(f4(f16(a3,a1)),f16(a3,a1))), % 50.57/50.69 inference(scs_inference,[],[57,60,382,360,362,389,128,83,93,2,24,89])). % 50.57/50.69 cnf(404,plain, % 50.57/50.69 (P5(f4(x4041),x4041)), % 50.57/50.69 inference(rename_variables,[],[60])). % 50.57/50.69 cnf(406,plain, % 50.57/50.69 (P7(f16(a1,f10(x4061)))), % 50.57/50.69 inference(scs_inference,[],[57,60,63,382,360,362,389,365,128,83,93,2,24,89,27])). % 50.57/50.69 cnf(407,plain, % 50.57/50.69 (E(f16(x4071,x4072),f16(x4072,x4071))), % 50.57/50.69 inference(rename_variables,[],[63])). % 50.57/50.69 cnf(408,plain, % 50.57/50.69 (P11(f16(a1,f10(x4081)))), % 50.57/50.69 inference(scs_inference,[],[57,60,63,407,382,360,362,389,365,368,128,83,93,2,24,89,27,28])). % 50.57/50.69 cnf(409,plain, % 50.57/50.69 (E(f16(x4091,x4092),f16(x4092,x4091))), % 50.57/50.69 inference(rename_variables,[],[63])). % 50.57/50.69 cnf(412,plain, % 50.57/50.69 (P10(f16(a1,f10(x4121)))), % 50.57/50.69 inference(scs_inference,[],[57,60,63,407,409,382,212,354,360,362,389,365,368,369,128,83,93,2,24,89,27,28,25,29])). % 50.57/50.69 cnf(413,plain, % 50.57/50.69 (E(f16(x4131,x4132),f16(x4132,x4131))), % 50.57/50.69 inference(rename_variables,[],[63])). % 50.57/50.69 cnf(414,plain, % 50.57/50.69 (P12(f16(a1,f10(x4141)))), % 50.57/50.69 inference(scs_inference,[],[57,60,63,407,409,413,382,212,354,360,362,389,365,368,369,375,128,83,93,2,24,89,27,28,25,29,31])). % 50.57/50.69 cnf(415,plain, % 50.57/50.69 (E(f16(x4151,x4152),f16(x4152,x4151))), % 50.57/50.69 inference(rename_variables,[],[63])). % 50.57/50.69 cnf(416,plain, % 50.57/50.69 (P8(f16(a1,f10(x4161)))), % 50.57/50.69 inference(scs_inference,[],[57,60,63,407,409,413,415,382,212,354,360,362,389,365,368,369,374,375,128,83,93,2,24,89,27,28,25,29,31,26])). % 50.57/50.69 cnf(417,plain, % 50.57/50.69 (E(f16(x4171,x4172),f16(x4172,x4171))), % 50.57/50.69 inference(rename_variables,[],[63])). % 50.57/50.69 cnf(418,plain, % 50.57/50.69 (P15(f16(a1,f10(x4181)))), % 50.57/50.69 inference(scs_inference,[],[57,60,63,407,409,413,415,417,382,212,354,360,362,389,365,368,369,370,374,375,128,83,93,2,24,89,27,28,25,29,31,26,30])). % 50.57/50.69 cnf(419,plain, % 50.57/50.69 (E(f16(x4191,x4192),f16(x4192,x4191))), % 50.57/50.69 inference(rename_variables,[],[63])). % 50.57/50.69 cnf(420,plain, % 50.57/50.69 (P14(f16(a1,f10(x4201)))), % 50.57/50.69 inference(scs_inference,[],[57,60,63,407,409,413,415,417,419,382,212,354,360,362,389,365,368,369,370,373,374,375,128,83,93,2,24,89,27,28,25,29,31,26,30,32])). % 50.57/50.69 cnf(421,plain, % 50.57/50.69 (E(f16(x4211,x4212),f16(x4212,x4211))), % 50.57/50.69 inference(rename_variables,[],[63])). % 50.57/50.69 cnf(423,plain, % 50.57/50.69 (E(f16(x4231,x4231),f16(x4231,a1))), % 50.57/50.69 inference(rename_variables,[],[359])). % 50.57/50.69 cnf(428,plain, % 50.57/50.69 (P16(x4281,f16(f16(x4281,x4281),x4282))), % 50.57/50.69 inference(scs_inference,[],[278,59,57,60,63,407,409,413,415,417,419,421,144,62,382,359,293,212,354,360,362,389,365,368,369,370,373,374,375,214,128,83,93,2,24,89,27,28,25,29,31,26,30,32,21,20,22,15])). % 50.57/50.69 cnf(430,plain, % 50.57/50.69 (P1(f16(a2,a1))), % 50.57/50.69 inference(scs_inference,[],[278,59,57,60,63,407,409,413,415,417,419,421,144,62,382,359,423,182,293,212,354,360,362,389,365,368,369,370,373,374,375,214,128,83,93,2,24,89,27,28,25,29,31,26,30,32,21,20,22,15,14])). % 50.57/50.69 cnf(431,plain, % 50.57/50.69 (E(f16(x4311,x4311),f16(x4311,a1))), % 50.57/50.69 inference(rename_variables,[],[359])). % 50.57/50.69 cnf(433,plain, % 50.57/50.69 (E(f16(x4331,x4331),f16(x4331,a1))), % 50.57/50.69 inference(rename_variables,[],[359])). % 50.57/50.69 cnf(434,plain, % 50.57/50.69 (E(f16(f16(x4341,x4341),f16(x4341,x4341)),f16(f16(a1,x4341),f16(a1,x4341)))), % 50.57/50.69 inference(scs_inference,[],[278,59,57,60,63,407,409,413,415,417,419,421,144,62,382,359,423,431,182,293,212,354,360,362,389,365,368,369,370,373,374,375,239,214,128,83,93,2,24,89,27,28,25,29,31,26,30,32,21,20,22,15,14,19,3])). % 50.57/50.69 cnf(435,plain, % 50.57/50.69 (E(f16(x4351,x4351),x4351)), % 50.57/50.69 inference(rename_variables,[],[59])). % 50.57/50.69 cnf(440,plain, % 50.57/50.69 (P5(f4(f16(x4401,x4401)),x4401)), % 50.57/50.69 inference(scs_inference,[],[140,278,59,435,57,60,404,63,407,409,413,415,417,419,421,144,62,382,359,423,431,433,182,293,212,354,360,362,389,365,368,369,370,373,374,375,247,239,214,128,83,93,2,24,89,27,28,25,29,31,26,30,32,21,20,22,15,14,19,3,16,18,23])). % 50.57/50.69 cnf(444,plain, % 50.57/50.69 (P16(f16(f11(x4441),a1),x4441)), % 50.57/50.69 inference(scs_inference,[],[140,278,59,435,57,60,404,63,407,409,413,415,417,419,421,144,62,382,359,423,431,433,182,293,212,354,360,362,389,365,368,369,370,373,374,375,247,239,214,128,83,93,2,24,89,27,28,25,29,31,26,30,32,21,20,22,15,14,19,3,16,18,23,87,94])). % 50.57/50.69 cnf(459,plain, % 50.57/50.69 (~P13(x4591,f16(f16(a1,a2),f16(a1,a2)))), % 50.57/50.69 inference(scs_inference,[],[388,401,93,83])). % 50.57/50.69 cnf(462,plain, % 50.57/50.69 (P5(f4(f16(x4621,x4621)),x4621)), % 50.57/50.69 inference(rename_variables,[],[440])). % 50.57/50.69 cnf(465,plain, % 50.57/50.69 (P13(f16(f4(f16(a3,a1)),a1),f16(a3,a1))), % 50.57/50.69 inference(scs_inference,[],[144,440,434,388,401,403,93,83,94,2,24])). % 50.57/50.69 cnf(466,plain, % 50.57/50.69 (E(x4661,f16(x4661,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(468,plain, % 50.57/50.69 (E(x4681,f16(x4681,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(470,plain, % 50.57/50.69 (E(x4701,f16(x4701,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(474,plain, % 50.57/50.69 (E(x4741,f16(x4741,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(476,plain, % 50.57/50.69 (E(f16(f16(x4761,x4761),f16(x4761,x4761)),f16(f16(a1,x4761),f16(a1,x4761)))), % 50.57/50.69 inference(rename_variables,[],[434])). % 50.57/50.69 cnf(477,plain, % 50.57/50.69 (P3(f16(f16(a1,a8),f16(a1,a8)))), % 50.57/50.69 inference(scs_inference,[],[144,466,468,470,440,434,476,388,237,212,401,396,406,408,412,403,214,93,83,94,2,24,27,28,25,29,20,21])). % 50.57/50.69 cnf(478,plain, % 50.57/50.69 (E(f16(f16(x4781,x4781),f16(x4781,x4781)),f16(f16(a1,x4781),f16(a1,x4781)))), % 50.57/50.69 inference(rename_variables,[],[434])). % 50.57/50.69 cnf(480,plain, % 50.57/50.69 (E(x4801,f16(x4801,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(482,plain, % 50.57/50.69 (E(x4821,f16(x4821,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(484,plain, % 50.57/50.69 (E(x4841,f16(x4841,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(488,plain, % 50.57/50.69 (E(x4881,f16(x4881,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(489,plain, % 50.57/50.69 (P5(f16(f10(x4891),a1),f12(x4891))), % 50.57/50.69 inference(scs_inference,[],[428,59,61,144,466,468,470,474,480,482,484,488,440,434,476,388,237,212,401,396,406,408,412,414,416,418,420,403,214,93,83,94,2,24,27,28,25,29,20,21,31,26,32,15,30,22])). % 50.57/50.69 cnf(490,plain, % 50.57/50.69 (E(x4901,f16(x4901,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(491,plain, % 50.57/50.69 (P2(f16(f16(a1,a8),f16(a1,a8)))), % 50.57/50.69 inference(scs_inference,[],[428,59,61,144,466,468,470,474,480,482,484,488,440,434,476,478,388,237,212,401,396,406,408,412,414,416,418,420,403,239,214,93,83,94,2,24,27,28,25,29,20,21,31,26,32,15,30,22,19])). % 50.57/50.69 cnf(492,plain, % 50.57/50.69 (E(f16(f16(x4921,x4921),f16(x4921,x4921)),f16(f16(a1,x4921),f16(a1,x4921)))), % 50.57/50.69 inference(rename_variables,[],[434])). % 50.57/50.69 cnf(495,plain, % 50.57/50.69 (P9(f16(f16(a1,a8),f16(a1,a8)))), % 50.57/50.69 inference(scs_inference,[],[444,428,59,61,144,466,468,470,474,480,482,484,488,440,434,476,478,492,388,237,212,401,396,406,408,412,414,416,418,420,403,247,239,214,93,83,94,2,24,27,28,25,29,20,21,31,26,32,15,30,22,19,16,18])). % 50.57/50.69 cnf(502,plain, % 50.57/50.69 (~P13(x5021,f16(f10(f16(a2,a2)),a1))), % 50.57/50.69 inference(scs_inference,[],[444,428,59,61,144,466,468,470,474,480,482,484,488,490,440,462,434,476,478,492,182,388,237,212,401,396,406,408,412,414,416,418,420,403,247,239,214,93,83,94,2,24,27,28,25,29,20,21,31,26,32,15,30,22,19,16,18,23,99,98])). % 50.57/50.69 cnf(508,plain, % 50.57/50.69 (~P13(x5081,f16(a2,a1))), % 50.57/50.69 inference(scs_inference,[],[430,83])). % 50.57/50.69 cnf(512,plain, % 50.57/50.69 (P16(f16(f10(x5121),a1),x5121)), % 50.57/50.69 inference(scs_inference,[],[489,430,269,83,93,94])). % 50.57/50.69 cnf(514,plain, % 50.57/50.69 (P13(f16(a1,f4(f16(a1,a3))),f16(a3,a1))), % 50.57/50.69 inference(scs_inference,[],[63,489,430,212,269,83,93,94,24])). % 50.57/50.69 cnf(515,plain, % 50.57/50.69 (E(f16(x5151,x5152),f16(x5152,x5151))), % 50.57/50.69 inference(rename_variables,[],[63])). % 50.57/50.69 cnf(519,plain, % 50.57/50.69 (E(f16(x5191,x5192),f16(x5192,x5191))), % 50.57/50.69 inference(rename_variables,[],[63])). % 50.57/50.69 cnf(522,plain, % 50.57/50.69 (P3(f16(a1,a8))), % 50.57/50.69 inference(scs_inference,[],[226,59,63,515,359,489,171,430,212,261,269,477,83,93,94,24,25,15,20,21])). % 50.57/50.69 cnf(523,plain, % 50.57/50.69 (E(f16(x5231,x5231),x5231)), % 50.57/50.69 inference(rename_variables,[],[59])). % 50.57/50.69 cnf(524,plain, % 50.57/50.69 (P5(f16(a1,f4(x5241)),x5241)), % 50.57/50.69 inference(scs_inference,[],[226,59,63,515,519,243,359,489,171,430,212,261,269,477,83,93,94,24,25,15,20,21,22])). % 50.57/50.69 cnf(527,plain, % 50.57/50.69 (E(f16(x5271,x5271),x5271)), % 50.57/50.69 inference(rename_variables,[],[59])). % 50.57/50.69 cnf(528,plain, % 50.57/50.69 (~E(f16(a3,a1),f16(a2,a2))), % 50.57/50.69 inference(scs_inference,[],[226,59,523,63,515,519,180,243,359,489,171,430,212,261,491,269,477,83,93,94,24,25,15,20,21,22,19,3])). % 50.57/50.69 cnf(534,plain, % 50.57/50.69 (P5(f11(x5341),f16(f12(x5341),f12(x5341)))), % 50.57/50.69 inference(scs_inference,[],[101,226,59,523,527,63,515,519,180,243,62,104,359,489,171,430,212,495,261,491,269,477,83,93,94,24,25,15,20,21,22,19,3,16,18,23])). % 50.57/50.69 cnf(543,plain, % 50.57/50.69 (~P13(x5431,f11(x5432))), % 50.57/50.69 inference(scs_inference,[],[514,41,93,83])). % 50.57/50.69 cnf(548,plain, % 50.57/50.69 (P13(f16(f4(a8),a1),a8)), % 50.57/50.69 inference(scs_inference,[],[144,524,514,209,41,93,83,94,24])). % 50.57/50.69 cnf(549,plain, % 50.57/50.69 (E(x5491,f16(x5491,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(555,plain, % 50.57/50.69 (E(f16(f16(x5551,x5552),f16(x5551,x5552)),f16(x5552,x5551))), % 50.57/50.69 inference(rename_variables,[],[206])). % 50.57/50.69 cnf(557,plain, % 50.57/50.69 (E(x5571,f16(x5571,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(564,plain, % 50.57/50.69 (P5(f11(x5641),f16(f12(x5641),a1))), % 50.57/50.69 inference(scs_inference,[],[428,57,206,555,63,62,382,144,549,557,534,524,371,212,508,514,209,491,477,41,93,83,94,24,25,20,21,22,15,19,3,23])). % 50.57/50.69 cnf(579,plain, % 50.57/50.69 (P13(f16(f4(a14),f4(a14)),a14)), % 50.57/50.69 inference(scs_inference,[],[104,465,269,93,24])). % 50.57/50.69 cnf(580,plain, % 50.57/50.69 (E(x5801,f16(x5801,x5801))), % 50.57/50.69 inference(rename_variables,[],[104])). % 50.57/50.69 cnf(583,plain, % 50.57/50.69 (P3(f16(f16(a8,a1),f16(a8,a1)))), % 50.57/50.69 inference(scs_inference,[],[301,104,212,543,465,269,477,93,24,25,21])). % 50.57/50.69 cnf(584,plain, % 50.57/50.69 (E(f16(f16(x5841,x5842),f16(x5841,x5842)),f16(f16(x5842,x5841),f16(x5842,x5841)))), % 50.57/50.69 inference(rename_variables,[],[301])). % 50.57/50.69 cnf(586,plain, % 50.57/50.69 (E(x5861,f16(x5861,x5861))), % 50.57/50.69 inference(rename_variables,[],[104])). % 50.57/50.69 cnf(588,plain, % 50.57/50.69 (E(f16(f16(x5881,x5882),f16(x5881,x5882)),f16(f16(x5882,x5881),f16(x5882,x5881)))), % 50.57/50.69 inference(rename_variables,[],[301])). % 50.57/50.69 cnf(589,plain, % 50.57/50.69 (~E(f16(a3,a1),f16(f16(a1,a2),f16(a1,a2)))), % 50.57/50.69 inference(scs_inference,[],[301,584,62,400,104,580,528,212,543,465,269,491,477,93,24,25,21,22,19,3])). % 50.57/50.69 cnf(595,plain, % 50.57/50.69 (P5(f10(x5951),f16(f12(x5951),f12(x5951)))), % 50.57/50.69 inference(scs_inference,[],[512,59,61,301,584,588,62,400,104,580,586,528,212,543,465,269,495,491,477,93,24,25,21,22,19,3,16,18,23])). % 50.57/50.69 cnf(610,plain, % 50.57/50.69 (P13(f16(f4(a8),f4(a8)),a8)), % 50.57/50.69 inference(scs_inference,[],[104,579,209,93,24])). % 50.57/50.69 cnf(611,plain, % 50.57/50.69 (E(x6111,f16(x6111,x6111))), % 50.57/50.69 inference(rename_variables,[],[104])). % 50.57/50.69 cnf(618,plain, % 50.57/50.69 (~E(f16(a3,a1),f16(f16(a2,a1),f16(a2,a1)))), % 50.57/50.69 inference(scs_inference,[],[301,359,104,611,595,589,583,459,579,209,93,24,25,21,22,3])). % 50.57/50.69 cnf(645,plain, % 50.57/50.69 (P13(f16(f4(a14),a1),a14)), % 50.57/50.69 inference(scs_inference,[],[144,610,269,93,24])). % 50.57/50.69 cnf(646,plain, % 50.57/50.69 (E(x6461,f16(x6461,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(651,plain, % 50.57/50.69 (~E(f16(a3,a1),f16(f10(f16(a2,a2)),a1))), % 50.57/50.69 inference(scs_inference,[],[329,57,144,646,212,522,502,610,269,93,24,15,21,25])). % 50.57/50.69 cnf(678,plain, % 50.57/50.69 (P5(f16(f11(x6781),f11(x6781)),f16(f12(x6781),a1))), % 50.57/50.69 inference(scs_inference,[],[57,104,64,564,212,313,651,548,6,93,25,15,22])). % 50.57/50.69 cnf(680,plain, % 50.57/50.69 (~E(f16(a3,a1),f16(f16(a2,a1),a1))), % 50.57/50.69 inference(scs_inference,[],[57,335,104,618,64,564,212,313,651,548,6,93,25,15,22,3])). % 50.57/50.69 cnf(695,plain, % 50.57/50.69 (P13(f16(f4(a3),a1),a3)), % 50.57/50.69 inference(scs_inference,[],[144,680,645,114,6,93,24])). % 50.57/50.69 cnf(1023,plain, % 50.57/50.69 (E(a2,a1)), % 50.57/50.69 inference(scs_inference,[],[182,97,72])). % 50.57/50.69 cnf(1286,plain, % 50.57/50.69 (P5(f9(a3),f12(a3))), % 50.57/50.69 inference(scs_inference,[],[130,84,72])). % 50.57/50.69 cnf(1287,plain, % 50.57/50.69 (P16(f9(a3),a3)), % 50.57/50.69 inference(scs_inference,[],[1286,94])). % 50.57/50.69 cnf(1292,plain, % 50.57/50.69 (E(x12921,f16(x12921,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(1293,plain, % 50.57/50.69 (P5(f16(f9(a3),a1),f12(a3))), % 50.57/50.69 inference(scs_inference,[],[144,1292,1286,35,94,91,15,22])). % 50.57/50.69 cnf(1294,plain, % 50.57/50.69 (E(x12941,f16(x12941,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(1296,plain, % 50.57/50.69 (E(x12961,f16(x12961,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(1297,plain, % 50.57/50.69 (P16(f9(a3),f16(a3,a1))), % 50.57/50.69 inference(scs_inference,[],[144,1292,1294,1296,1286,35,94,91,15,22,23,16])). % 50.57/50.69 cnf(1307,plain, % 50.57/50.69 (E(x13071,f16(x13071,x13071))), % 50.57/50.69 inference(rename_variables,[],[104])). % 50.57/50.69 cnf(1308,plain, % 50.57/50.69 (P5(f16(f9(a3),f9(a3)),f12(a3))), % 50.57/50.69 inference(scs_inference,[],[1287,104,1307,1286,1293,35,91,15,22])). % 50.57/50.69 cnf(1309,plain, % 50.57/50.69 (E(x13091,f16(x13091,x13091))), % 50.57/50.69 inference(rename_variables,[],[104])). % 50.57/50.69 cnf(1310,plain, % 50.57/50.69 (P5(f9(a3),f16(f12(a3),f12(a3)))), % 50.57/50.69 inference(scs_inference,[],[1287,104,1307,1309,1286,1293,35,91,15,22,23])). % 50.57/50.69 cnf(1322,plain, % 50.57/50.69 (E(x13221,f16(x13221,a1))), % 50.57/50.69 inference(rename_variables,[],[144])). % 50.57/50.69 cnf(1323,plain, % 50.57/50.69 (P5(f16(f9(a3),a1),f16(f12(a3),f12(a3)))), % 50.57/50.69 inference(scs_inference,[],[1297,144,1322,1308,1310,35,91,15,22])). % 50.57/50.69 cnf(1524,plain, % 50.57/50.69 (P5(f16(f4(a2),f4(a2)),a1)), % 50.57/50.69 inference(scs_inference,[],[317,428,1023,60,104,15,23,16,22])). % 50.57/50.69 cnf(1533,plain, % 50.57/50.69 (P16(f10(a2),a1)), % 50.57/50.69 inference(scs_inference,[],[140,329,1023,524,359,1524,15,22,23,16])). % 50.57/50.69 cnf(1564,plain, % 50.57/50.69 (P16(f16(f10(a2),f10(a2)),a1)), % 50.57/50.69 inference(scs_inference,[],[1533,104,15])). % 50.57/50.69 cnf(1587,plain, % 50.57/50.69 (P16(f16(f10(a2),a1),a1)), % 50.57/50.69 inference(scs_inference,[],[1564,359,15])). % 50.57/50.69 cnf(1678,plain, % 50.57/50.69 (~P16(a7,f16(a5,a7))), % 50.57/50.69 inference(scs_inference,[],[64,135,95])). % 50.57/50.69 cnf(2207,plain, % 50.57/50.69 (P13(f16(a1,f4(f13(x22071))),f13(x22071))), % 50.57/50.69 inference(scs_inference,[],[63,362,24])). % 50.57/50.69 cnf(2220,plain, % 50.57/50.69 (E(f16(x22201,x22202),f16(x22202,x22201))), % 50.57/50.69 inference(rename_variables,[],[63])). % 50.57/50.69 cnf(2222,plain, % 50.57/50.69 (E(f16(x22221,x22222),f16(x22222,x22221))), % 50.57/50.69 inference(rename_variables,[],[63])). % 50.57/50.69 cnf(2224,plain, % 50.57/50.69 (E(f16(x22241,x22242),f16(x22242,x22241))), % 50.57/50.69 inference(rename_variables,[],[63])). % 50.57/50.69 cnf(2226,plain, % 50.57/50.69 (E(f16(x22261,x22262),f16(x22262,x22261))), % 50.57/50.69 inference(rename_variables,[],[63])). % 50.57/50.69 cnf(2227,plain, % 50.57/50.69 (P16(f16(x22271,x22271),f16(x22272,x22271))), % 50.57/50.69 inference(scs_inference,[],[63,2220,2222,2224,2226,169,1587,678,1323,695,2207,93,24,22,23,15,16])). % 50.57/50.69 cnf(2277,plain, % 50.57/50.69 ($false), % 50.57/50.69 inference(scs_inference,[],[2227,59,1678,15]), % 50.57/50.69 ['proof']). % 50.57/50.69 % SZS output end Proof % 50.57/50.69 % Total time :49.970000s %------------------------------------------------------------------------------