%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PRO012+2 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n025.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 13:39:46 EDT 2024 % Result : Theorem 182.17s 182.12s % Output : CNFRefutation 182.23s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : PRO012+2 : TPTP v8.2.0. Released v4.0.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n025.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Thu Jun 20 06:40:24 EDT 2024 % 0.12/0.33 % CPUTime : % 0.49/0.58 start to proof:theBenchmark % 182.10/182.10 %------------------------------------------- % 182.10/182.10 % File :CSE---1.7 % 182.10/182.10 % Problem :theBenchmark % 182.10/182.10 % Transform :cnf % 182.10/182.10 % Format :tptp:raw % 182.10/182.10 % Command :java -jar mcs_scs.jar %d %s % 182.10/182.10 % 182.10/182.10 % Result :Theorem 181.450000s % 182.10/182.10 % Output :CNFRefutation 181.450000s % 182.10/182.10 %------------------------------------------- % 182.10/182.11 %------------------------------------------------------------------------------ % 182.10/182.11 % File : PRO012+2 : TPTP v8.2.0. Released v4.0.0. % 182.10/182.11 % Domain : Processes % 182.10/182.11 % Problem : PSL cliff problem coe-7.1.4-no-leaf % 182.10/182.11 % Version : Especial : Reduced > Especial. % 182.10/182.11 % English : % 182.10/182.11 % Refs : [Hal09] Halcomb (2009), Email to G. Sutcliffe % 182.10/182.11 % Source : [Hal09] % 182.10/182.11 % Names : minimal-subset-p9__coe-7.1.4-no-leaf-pd [Hal09] % 182.10/182.11 % 182.10/182.11 % Status : Theorem % 182.10/182.11 % Rating : 0.17 v8.2.0, 0.14 v8.1.0, 0.19 v7.5.0, 0.22 v7.4.0, 0.10 v7.2.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.16 v6.1.0, 0.20 v6.0.0, 0.17 v5.5.0, 0.22 v5.4.0, 0.21 v5.3.0, 0.26 v5.2.0, 0.15 v5.1.0, 0.19 v5.0.0, 0.21 v4.1.0, 0.26 v4.0.1, 0.22 v4.0.0 % 182.10/182.11 % Syntax : Number of formulae : 46 ( 12 unt; 0 def) % 182.10/182.11 % Number of atoms : 138 ( 12 equ) % 182.10/182.11 % Maximal formula atoms : 11 ( 3 avg) % 182.10/182.11 % Number of connectives : 109 ( 17 ~; 6 |; 50 &) % 182.10/182.11 % ( 7 <=>; 29 =>; 0 <=; 0 <~>) % 182.10/182.11 % Maximal formula depth : 15 ( 5 avg) % 182.10/182.11 % Maximal term depth : 1 ( 1 avg) % 182.10/182.11 % Number of predicates : 18 ( 17 usr; 0 prp; 1-3 aty) % 182.10/182.11 % Number of functors : 5 ( 5 usr; 5 con; 0-0 aty) % 182.10/182.11 % Number of variables : 103 ( 82 !; 21 ?) % 182.10/182.11 % SPC : FOF_THM_RFO_SEQ % 182.10/182.11 % 182.10/182.11 % Comments : % 182.10/182.11 %------------------------------------------------------------------------------ % 182.10/182.11 fof(sos,axiom, % 182.10/182.11 ! [X0,X1,X2,X3] : % 182.10/182.11 ( ( min_precedes(X0,X1,X3) % 182.10/182.11 & min_precedes(X1,X2,X3) ) % 182.10/182.11 => min_precedes(X0,X2,X3) ) ). % 182.10/182.11 % 182.10/182.11 fof(sos_01,axiom, % 182.10/182.11 ! [X4,X5,X6] : % 182.10/182.11 ( ( earlier(X4,X5) % 182.10/182.11 & earlier(X5,X6) ) % 182.10/182.11 => earlier(X4,X6) ) ). % 182.10/182.11 % 182.10/182.11 fof(sos_02,axiom, % 182.10/182.11 ! [X7,X8,X9,X10] : % 182.10/182.11 ( ( occurrence_of(X9,X10) % 182.10/182.11 & root_occ(X7,X9) % 182.10/182.11 & root_occ(X8,X9) ) % 182.10/182.11 => X7 = X8 ) ). % 182.10/182.11 % 182.10/182.11 fof(sos_03,axiom, % 182.10/182.11 ! [X11,X12,X13,X14] : % 182.10/182.11 ( ( occurrence_of(X13,X14) % 182.10/182.11 & ~ atomic(X14) % 182.10/182.11 & leaf_occ(X11,X13) % 182.10/182.11 & leaf_occ(X12,X13) ) % 182.10/182.11 => X11 = X12 ) ). % 182.10/182.11 % 182.10/182.11 fof(sos_04,axiom, % 182.10/182.11 ! [X15,X16,X17] : % 182.10/182.11 ( next_subocc(X15,X16,X17) % 182.10/182.11 <=> ( min_precedes(X15,X16,X17) % 182.10/182.11 & ~ ? [X18] : % 182.10/182.11 ( min_precedes(X15,X18,X17) % 182.10/182.11 & min_precedes(X18,X16,X17) ) ) ) ). % 182.10/182.11 % 182.10/182.11 fof(sos_05,axiom, % 182.10/182.11 ! [X19,X20,X21] : % 182.10/182.11 ( next_subocc(X19,X20,X21) % 182.10/182.11 => ( arboreal(X19) % 182.10/182.11 & arboreal(X20) ) ) ). % 182.10/182.11 % 182.10/182.11 fof(sos_06,axiom, % 182.10/182.11 ! [X22,X23,X24] : % 182.10/182.11 ( min_precedes(X22,X23,X24) % 182.10/182.11 => precedes(X22,X23) ) ). % 182.10/182.11 % 182.10/182.11 fof(sos_07,axiom, % 182.10/182.11 ! [X25,X26,X27] : % 182.10/182.11 ( min_precedes(X25,X26,X27) % 182.10/182.11 => ~ root(X26,X27) ) ). % 182.10/182.11 % 182.10/182.11 fof(sos_08,axiom, % 182.10/182.11 ! [X28,X29] : % 182.10/182.11 ( precedes(X28,X29) % 182.10/182.11 <=> ( earlier(X28,X29) % 182.10/182.11 & legal(X29) ) ) ). % 182.10/182.11 % 182.10/182.11 fof(sos_09,axiom, % 182.10/182.11 ! [X30,X31] : % 182.10/182.11 ( earlier(X30,X31) % 182.10/182.11 => ~ earlier(X31,X30) ) ). % 182.10/182.11 % 182.10/182.11 fof(sos_10,axiom, % 182.10/182.11 ! [X32,X33] : % 182.10/182.11 ( root_occ(X32,X33) % 182.10/182.11 <=> ? [X34] : % 182.10/182.11 ( occurrence_of(X33,X34) % 182.10/182.11 & subactivity_occurrence(X32,X33) % 182.10/182.11 & root(X32,X34) ) ) ). % 182.10/182.11 % 182.10/182.11 fof(sos_11,axiom, % 182.10/182.11 ! [X35,X36] : % 182.10/182.11 ( leaf_occ(X35,X36) % 182.10/182.11 <=> ? [X37] : % 182.10/182.12 ( occurrence_of(X36,X37) % 182.10/182.12 & subactivity_occurrence(X35,X36) % 182.10/182.12 & leaf(X35,X37) ) ) ). % 182.10/182.12 % 182.10/182.12 fof(sos_12,axiom, % 182.10/182.12 ! [X38,X39] : % 182.10/182.12 ( root(X38,X39) % 182.10/182.12 => legal(X38) ) ). % 182.10/182.12 % 182.10/182.12 fof(sos_13,axiom, % 182.10/182.12 ! [X40,X41] : % 182.10/182.12 ( occurrence_of(X40,X41) % 182.10/182.12 => ( arboreal(X40) % 182.10/182.12 <=> atomic(X41) ) ) ). % 182.10/182.12 % 182.10/182.12 fof(sos_14,axiom, % 182.10/182.12 ! [X42,X43] : % 182.10/182.12 ( leaf(X42,X43) % 182.10/182.12 <=> ( ( root(X42,X43) % 182.10/182.12 | ? [X44] : min_precedes(X44,X42,X43) ) % 182.10/182.12 & ~ ? [X45] : min_precedes(X42,X45,X43) ) ) ). % 182.10/182.12 % 182.10/182.12 fof(sos_15,axiom, % 182.10/182.12 ! [X46,X47] : % 182.10/182.12 ( atocc(X46,X47) % 182.10/182.12 <=> ? [X48] : % 182.10/182.12 ( subactivity(X47,X48) % 182.10/182.12 & atomic(X48) % 182.10/182.12 & occurrence_of(X46,X48) ) ) ). % 182.10/182.12 % 182.10/182.12 fof(sos_16,axiom, % 182.10/182.12 ! [X49,X50] : % 182.10/182.12 ( ( atocc(X49,X50) % 182.10/182.12 & legal(X49) ) % 182.10/182.12 => root(X49,X50) ) ). % 182.10/182.12 % 182.10/182.12 fof(sos_17,axiom, % 182.10/182.12 ! [X51] : % 182.10/182.12 ( legal(X51) % 182.10/182.12 => arboreal(X51) ) ). % 182.10/182.12 % 182.10/182.12 fof(sos_18,axiom, % 182.10/182.12 ! [X52] : % 182.10/182.12 ( activity_occurrence(X52) % 182.10/182.12 => ? [X53] : % 182.10/182.12 ( activity(X53) % 182.10/182.12 & occurrence_of(X52,X53) ) ) ). % 182.10/182.12 % 182.10/182.12 fof(sos_19,axiom, % 182.10/182.12 ! [X54,X55] : % 182.10/182.12 ( subactivity_occurrence(X54,X55) % 182.10/182.12 => ( activity_occurrence(X54) % 182.10/182.12 & activity_occurrence(X55) ) ) ). % 182.10/182.12 % 182.10/182.12 fof(sos_20,axiom, % 182.10/182.12 ! [X56,X57,X58] : % 182.10/182.12 ( ( occurrence_of(X56,X58) % 182.10/182.12 & root_occ(X57,X56) ) % 182.10/182.12 => ~ ? [X59] : min_precedes(X59,X57,X58) ) ). % 182.10/182.12 % 182.10/182.12 fof(sos_21,axiom, % 182.10/182.12 ! [X60,X61,X62] : % 182.10/182.12 ( ( occurrence_of(X60,X62) % 182.10/182.12 & leaf_occ(X61,X60) ) % 182.10/182.12 => ~ ? [X63] : min_precedes(X61,X63,X62) ) ). % 182.10/182.12 % 182.10/182.12 fof(sos_22,axiom, % 182.10/182.12 ! [X64,X65,X66] : % 182.10/182.12 ( ( occurrence_of(X64,X65) % 182.10/182.12 & occurrence_of(X64,X66) ) % 182.10/182.12 => X65 = X66 ) ). % 182.10/182.12 % 182.10/182.12 fof(sos_23,axiom, % 182.10/182.12 ! [X67,X68] : % 182.10/182.12 ( ( leaf(X67,X68) % 182.10/182.12 & ~ atomic(X68) ) % 182.10/182.12 => ? [X69] : % 182.10/182.12 ( occurrence_of(X69,X68) % 182.10/182.12 & leaf_occ(X67,X69) ) ) ). % 182.10/182.12 % 182.10/182.12 fof(sos_24,axiom, % 182.10/182.12 ! [X70,X71,X72] : % 182.10/182.12 ( min_precedes(X71,X72,X70) % 182.10/182.12 => ? [X73] : % 182.10/182.12 ( occurrence_of(X73,X70) % 182.10/182.12 & subactivity_occurrence(X71,X73) % 182.10/182.12 & subactivity_occurrence(X72,X73) ) ) ). % 182.10/182.12 % 182.10/182.12 fof(sos_25,axiom, % 182.10/182.12 ! [X74,X75] : % 182.10/182.12 ( ( leaf(X74,X75) % 182.10/182.12 & ~ atomic(X75) ) % 182.10/182.12 => ? [X76] : % 182.10/182.12 ( occurrence_of(X76,X75) % 182.10/182.12 & leaf_occ(X74,X76) ) ) ). % 182.10/182.12 % 182.10/182.12 fof(sos_26,axiom, % 182.10/182.12 ! [X77,X78,X79] : % 182.10/182.12 ( min_precedes(X78,X79,X77) % 182.10/182.12 => ? [X80,X81] : % 182.10/182.12 ( subactivity(X80,X77) % 182.10/182.12 & subactivity(X81,X77) % 182.10/182.12 & atocc(X78,X80) % 182.10/182.12 & atocc(X79,X81) ) ) ). % 182.10/182.12 % 182.10/182.12 fof(sos_27,axiom, % 182.10/182.12 ! [X82,X83] : % 182.10/182.12 ( root(X83,X82) % 182.10/182.12 => ? [X84] : % 182.10/182.12 ( subactivity(X84,X82) % 182.10/182.12 & atocc(X83,X84) ) ) ). % 182.10/182.12 % 182.10/182.12 fof(sos_28,axiom, % 182.10/182.12 ! [X85,X86,X87,X88] : % 182.10/182.12 ( ( occurrence_of(X86,X85) % 182.10/182.12 & arboreal(X87) % 182.10/182.12 & arboreal(X88) % 182.10/182.12 & subactivity_occurrence(X87,X86) % 182.10/182.12 & subactivity_occurrence(X88,X86) ) % 182.10/182.12 => ( min_precedes(X87,X88,X85) % 182.10/182.12 | min_precedes(X88,X87,X85) % 182.10/182.12 | X87 = X88 ) ) ). % 182.10/182.12 % 182.10/182.12 fof(sos_29,axiom, % 182.10/182.12 ! [X89,X90] : % 182.10/182.12 ( occurrence_of(X90,X89) % 182.10/182.12 => ( activity(X89) % 182.10/182.12 & activity_occurrence(X90) ) ) ). % 182.10/182.12 % 182.10/182.12 fof(sos_30,axiom, % 182.10/182.12 ! [X91,X92] : % 182.10/182.12 ( ( occurrence_of(X92,X91) % 182.10/182.12 & ~ atomic(X91) ) % 182.10/182.12 => ? [X93] : % 182.10/182.12 ( root(X93,X91) % 182.10/182.12 & subactivity_occurrence(X93,X92) ) ) ). % 182.10/182.12 % 182.10/182.12 fof(sos_31,axiom, % 182.10/182.12 ! [X94] : % 182.10/182.12 ( activity(X94) % 182.10/182.12 => subactivity(X94,X94) ) ). % 182.10/182.12 % 182.10/182.12 fof(sos_32,axiom, % 182.10/182.12 ! [X95] : % 182.10/182.12 ( occurrence_of(X95,tptp0) % 182.10/182.12 => ? [X96,X97,X98] : % 182.10/182.12 ( occurrence_of(X96,tptp3) % 182.10/182.12 & root_occ(X96,X95) % 182.10/182.12 & occurrence_of(X97,tptp4) % 182.10/182.12 & min_precedes(X96,X97,tptp0) % 182.10/182.12 & ( occurrence_of(X98,tptp2) % 182.10/182.12 | occurrence_of(X98,tptp1) ) % 182.10/182.12 & min_precedes(X97,X98,tptp0) % 182.10/182.12 & ! [X99] : % 182.10/182.12 ( min_precedes(X96,X99,tptp0) % 182.10/182.12 => ( X99 = X97 % 182.10/182.12 | X99 = X98 ) ) ) ) ). % 182.10/182.12 % 182.10/182.12 fof(sos_33,axiom, % 182.10/182.12 activity(tptp0) ). % 182.10/182.12 % 182.10/182.12 fof(sos_34,axiom, % 182.10/182.12 ~ atomic(tptp0) ). % 182.10/182.12 % 182.10/182.12 fof(sos_35,axiom, % 182.10/182.12 atomic(tptp4) ). % 182.10/182.12 % 182.10/182.12 fof(sos_36,axiom, % 182.10/182.12 atomic(tptp2) ). % 182.10/182.12 % 182.10/182.12 fof(sos_37,axiom, % 182.10/182.12 atomic(tptp1) ). % 182.10/182.12 % 182.10/182.12 fof(sos_38,axiom, % 182.10/182.12 atomic(tptp3) ). % 182.10/182.12 % 182.10/182.12 fof(sos_39,axiom, % 182.10/182.12 tptp4 != tptp3 ). % 182.10/182.12 % 182.10/182.12 fof(sos_40,axiom, % 182.10/182.12 tptp4 != tptp2 ). % 182.17/182.12 % 182.17/182.12 fof(sos_41,axiom, % 182.17/182.12 tptp4 != tptp1 ). % 182.17/182.12 % 182.17/182.12 fof(sos_42,axiom, % 182.17/182.12 tptp3 != tptp2 ). % 182.17/182.12 % 182.17/182.12 fof(sos_43,axiom, % 182.17/182.12 tptp3 != tptp1 ). % 182.17/182.12 % 182.17/182.12 fof(sos_44,axiom, % 182.17/182.12 tptp2 != tptp1 ). % 182.17/182.12 % 182.17/182.12 fof(goals,conjecture, % 182.17/182.12 ! [X100] : % 182.17/182.12 ( occurrence_of(X100,tptp0) % 182.17/182.12 => ? [X101,X102] : % 182.17/182.12 ( occurrence_of(X101,tptp3) % 182.17/182.12 & root_occ(X101,X100) % 182.17/182.12 & ( occurrence_of(X102,tptp2) % 182.17/182.12 | occurrence_of(X102,tptp1) ) % 182.17/182.12 & min_precedes(X101,X102,tptp0) ) ) ). % 182.17/182.12 % 182.17/182.12 %------------------------------------------------------------------------------ % 182.17/182.12 %------------------------------------------- % 182.17/182.12 % Proof found % 182.17/182.12 % SZS status Theorem for theBenchmark % 182.17/182.12 % SZS output start Proof % 182.17/182.12 %ClaNum:153(EqnAxiom:68) % 182.17/182.12 %VarNum:400(SingletonVarNum:169) % 182.17/182.12 %MaxLitNum:8 % 182.17/182.12 %MaxfuncDepth:1 % 182.17/182.12 %SharedTerms:19 % 182.17/182.12 %goalClause: 74 139 140 % 182.17/182.12 %singleGoalClaCount:1 % 182.17/182.12 [69]P1(a1) % 182.17/182.12 [70]P1(a23) % 182.17/182.12 [71]P1(a2) % 182.17/182.12 [72]P1(a3) % 182.17/182.12 [73]P2(a4) % 182.17/182.12 [74]P6(a5,a4) % 182.17/182.12 [75]~E(a1,a23) % 182.17/182.12 [76]~E(a1,a2) % 182.17/182.12 [77]~E(a2,a23) % 182.17/182.12 [78]~E(a1,a3) % 182.17/182.12 [79]~E(a3,a23) % 182.17/182.12 [80]~E(a3,a2) % 182.17/182.12 [81]~P1(a4) % 182.17/182.12 [82]~P7(x821)+P3(x821) % 182.17/182.12 [84]~P2(x841)+P13(x841,x841) % 182.17/182.12 [83]~P4(x831)+P2(f14(x831)) % 182.17/182.12 [91]~P4(x911)+P6(x911,f14(x911)) % 182.17/182.12 [97]~P6(x971,a4)+P6(f6(x971),a1) % 182.17/182.12 [98]~P6(x981,a4)+P6(f12(x981),a23) % 182.17/182.12 [99]~P6(x991,a4)+P16(f6(x991),x991) % 182.17/182.12 [126]~P6(x1261,a4)+P11(f6(x1261),f12(x1261),a4) % 182.17/182.12 [127]~P6(x1271,a4)+P11(f12(x1271),f13(x1271),a4) % 182.17/182.12 [85]P7(x851)+~P14(x852,x851) % 182.17/182.12 [86]P7(x861)+~P15(x861,x862) % 182.17/182.12 [87]P4(x871)+~P6(x871,x872) % 182.17/182.12 [88]P4(x881)+~P17(x882,x881) % 182.17/182.12 [89]P4(x891)+~P17(x891,x892) % 182.17/182.12 [90]P2(x901)+~P6(x902,x901) % 182.17/182.12 [94]~P14(x941,x942)+P8(x941,x942) % 182.17/182.12 [95]~P16(x951,x952)+P17(x951,x952) % 182.17/182.12 [96]~P9(x961,x962)+P17(x961,x962) % 182.17/182.12 [102]~P8(x1022,x1021)+~P8(x1021,x1022) % 182.17/182.12 [104]~P5(x1041,x1042)+P1(f15(x1041,x1042)) % 182.17/182.12 [107]~P16(x1072,x1071)+P6(x1071,f16(x1072,x1071)) % 182.17/182.12 [108]~P9(x1082,x1081)+P6(x1081,f18(x1082,x1081)) % 182.17/182.12 [109]~P5(x1091,x1092)+P6(x1091,f15(x1091,x1092)) % 182.17/182.12 [110]~P16(x1101,x1102)+P15(x1101,f16(x1101,x1102)) % 182.17/182.12 [111]~P9(x1111,x1112)+P10(x1111,f18(x1111,x1112)) % 182.17/182.12 [112]~P15(x1121,x1122)+P5(x1121,f7(x1122,x1121)) % 182.17/182.12 [113]~P5(x1132,x1131)+P13(x1131,f15(x1132,x1131)) % 182.17/182.12 [114]~P15(x1142,x1141)+P13(f7(x1141,x1142),x1141) % 182.17/182.12 [128]P3(x1281)+~P12(x1282,x1281,x1283) % 182.17/182.12 [129]P3(x1291)+~P12(x1291,x1292,x1293) % 182.17/182.13 [130]P14(x1301,x1302)+~P11(x1301,x1302,x1303) % 182.17/182.13 [131]~P15(x1311,x1312)+~P11(x1313,x1311,x1312) % 182.17/182.13 [132]~P10(x1321,x1322)+~P11(x1321,x1323,x1322) % 182.17/182.13 [138]~P12(x1381,x1382,x1383)+P11(x1381,x1382,x1383) % 182.17/182.13 [143]~P11(x1433,x1431,x1432)+P17(x1431,f22(x1432,x1433,x1431)) % 182.17/182.13 [144]~P11(x1441,x1443,x1442)+P17(x1441,f22(x1442,x1441,x1443)) % 182.17/182.13 [145]~P11(x1451,x1453,x1452)+P5(x1451,f9(x1452,x1451,x1453)) % 182.17/182.13 [146]~P11(x1463,x1461,x1462)+P5(x1461,f10(x1462,x1463,x1461)) % 182.17/182.13 [147]~P11(x1472,x1473,x1471)+P6(f22(x1471,x1472,x1473),x1471) % 182.17/182.13 [148]~P11(x1482,x1483,x1481)+P13(f9(x1481,x1482,x1483),x1481) % 182.17/182.13 [149]~P11(x1492,x1493,x1491)+P13(f10(x1491,x1492,x1493),x1491) % 182.17/182.13 [105]~P6(x1051,a4)+P6(f13(x1051),a2)+P6(f13(x1051),a3) % 182.17/182.13 [92]~P6(x922,x921)+P1(x921)+~P3(x922) % 182.17/182.13 [93]~P6(x931,x932)+P3(x931)+~P1(x932) % 182.17/182.13 [100]~P7(x1002)+~P8(x1001,x1002)+P14(x1001,x1002) % 182.17/182.13 [101]~P7(x1011)+~P5(x1011,x1012)+P15(x1011,x1012) % 182.17/182.13 [116]~P10(x1162,x1161)+P1(x1161)+P9(x1162,f21(x1162,x1161)) % 182.17/182.13 [117]~P10(x1172,x1171)+P1(x1171)+P9(x1172,f8(x1172,x1171)) % 182.17/182.13 [118]~P10(x1182,x1181)+P1(x1181)+P6(f21(x1182,x1181),x1181) % 182.17/182.13 [119]~P10(x1192,x1191)+P1(x1191)+P6(f8(x1192,x1191),x1191) % 182.17/182.13 [120]~P6(x1202,x1201)+P1(x1201)+P15(f11(x1201,x1202),x1201) % 182.17/182.13 [121]~P6(x1212,x1211)+P1(x1211)+P17(f11(x1211,x1212),x1212) % 182.17/182.13 [133]~P15(x1331,x1332)+P10(x1331,x1332)+P11(x1331,f19(x1331,x1332),x1332) % 182.17/182.13 [134]~P10(x1341,x1342)+P15(x1341,x1342)+P11(f20(x1341,x1342),x1341,x1342) % 182.17/182.13 [103]~P6(x1033,x1031)+E(x1031,x1032)+~P6(x1033,x1032) % 182.17/182.13 [106]~P8(x1061,x1063)+P8(x1061,x1062)+~P8(x1063,x1062) % 182.17/182.13 [141]P10(x1411,x1412)+~P11(x1413,x1411,x1412)+P11(x1411,f19(x1411,x1412),x1412) % 182.17/182.13 [152]~P11(x1521,x1522,x1523)+P12(x1521,x1522,x1523)+P11(x1521,f17(x1521,x1522,x1523),x1523) % 182.17/182.13 [153]~P11(x1531,x1532,x1533)+P12(x1531,x1532,x1533)+P11(f17(x1531,x1532,x1533),x1532,x1533) % 182.17/182.13 [136]~P6(x1361,x1362)+~P11(x1364,x1363,x1362)+~P16(x1363,x1361) % 182.17/182.13 [137]~P6(x1371,x1372)+~P11(x1373,x1374,x1372)+~P9(x1373,x1371) % 182.17/182.13 [150]~P11(x1501,x1504,x1503)+P11(x1501,x1502,x1503)+~P11(x1504,x1502,x1503) % 182.17/182.13 [151]~P12(x1514,x1512,x1513)+~P11(x1511,x1512,x1513)+~P11(x1514,x1511,x1513) % 182.17/182.13 [139]~P11(x1391,x1392,a4)+~P16(x1391,a5)+~P6(x1391,a1)+~P6(x1392,a2) % 182.17/182.13 [140]~P11(x1401,x1402,a4)+~P16(x1401,a5)+~P6(x1401,a1)+~P6(x1402,a3) % 182.17/182.13 [135]E(x1351,f13(x1352))+~P6(x1352,a4)+E(x1351,f12(x1352))+~P11(f6(x1352),x1351,a4) % 182.17/182.13 [115]~P6(x1151,x1153)+~P13(x1152,x1153)+P5(x1151,x1152)+~P1(x1153) % 182.17/182.13 [124]~P15(x1241,x1243)+~P17(x1241,x1242)+P16(x1241,x1242)+~P6(x1242,x1243) % 182.17/182.13 [125]~P17(x1251,x1252)+~P10(x1251,x1253)+P9(x1251,x1252)+~P6(x1252,x1253) % 182.17/182.13 [122]~P16(x1222,x1223)+~P16(x1221,x1223)+E(x1221,x1222)+~P6(x1223,x1224) % 182.17/182.13 [123]~P9(x1232,x1234)+~P9(x1231,x1234)+E(x1231,x1232)+~P6(x1234,x1233)+P1(x1233) % 182.17/182.13 [142]P11(x1421,x1422,x1423)+~P3(x1422)+~P3(x1421)+~P17(x1422,x1424)+~P17(x1421,x1424)+E(x1421,x1422)+P11(x1422,x1421,x1423)+~P6(x1424,x1423) % 182.17/182.13 %EqnAxiom % 182.17/182.13 [1]E(x11,x11) % 182.17/182.13 [2]E(x22,x21)+~E(x21,x22) % 182.17/182.13 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 182.17/182.13 [4]~E(x41,x42)+E(f14(x41),f14(x42)) % 182.17/182.13 [5]~E(x51,x52)+E(f17(x51,x53,x54),f17(x52,x53,x54)) % 182.17/182.13 [6]~E(x61,x62)+E(f17(x63,x61,x64),f17(x63,x62,x64)) % 182.17/182.13 [7]~E(x71,x72)+E(f17(x73,x74,x71),f17(x73,x74,x72)) % 182.17/182.13 [8]~E(x81,x82)+E(f6(x81),f6(x82)) % 182.17/182.13 [9]~E(x91,x92)+E(f12(x91),f12(x92)) % 182.17/182.13 [10]~E(x101,x102)+E(f10(x101,x103,x104),f10(x102,x103,x104)) % 182.17/182.13 [11]~E(x111,x112)+E(f10(x113,x111,x114),f10(x113,x112,x114)) % 182.17/182.13 [12]~E(x121,x122)+E(f10(x123,x124,x121),f10(x123,x124,x122)) % 182.17/182.13 [13]~E(x131,x132)+E(f15(x131,x133),f15(x132,x133)) % 182.17/182.13 [14]~E(x141,x142)+E(f15(x143,x141),f15(x143,x142)) % 182.17/182.13 [15]~E(x151,x152)+E(f13(x151),f13(x152)) % 182.17/182.13 [16]~E(x161,x162)+E(f22(x161,x163,x164),f22(x162,x163,x164)) % 182.17/182.13 [17]~E(x171,x172)+E(f22(x173,x171,x174),f22(x173,x172,x174)) % 182.17/182.13 [18]~E(x181,x182)+E(f22(x183,x184,x181),f22(x183,x184,x182)) % 182.17/182.13 [19]~E(x191,x192)+E(f16(x191,x193),f16(x192,x193)) % 182.17/182.13 [20]~E(x201,x202)+E(f16(x203,x201),f16(x203,x202)) % 182.17/182.13 [21]~E(x211,x212)+E(f18(x211,x213),f18(x212,x213)) % 182.17/182.13 [22]~E(x221,x222)+E(f18(x223,x221),f18(x223,x222)) % 182.17/182.13 [23]~E(x231,x232)+E(f19(x231,x233),f19(x232,x233)) % 182.17/182.13 [24]~E(x241,x242)+E(f19(x243,x241),f19(x243,x242)) % 182.17/182.13 [25]~E(x251,x252)+E(f9(x251,x253,x254),f9(x252,x253,x254)) % 182.17/182.13 [26]~E(x261,x262)+E(f9(x263,x261,x264),f9(x263,x262,x264)) % 182.17/182.13 [27]~E(x271,x272)+E(f9(x273,x274,x271),f9(x273,x274,x272)) % 182.17/182.13 [28]~E(x281,x282)+E(f20(x281,x283),f20(x282,x283)) % 182.17/182.13 [29]~E(x291,x292)+E(f20(x293,x291),f20(x293,x292)) % 182.17/182.13 [30]~E(x301,x302)+E(f7(x301,x303),f7(x302,x303)) % 182.17/182.13 [31]~E(x311,x312)+E(f7(x313,x311),f7(x313,x312)) % 182.17/182.13 [32]~E(x321,x322)+E(f11(x321,x323),f11(x322,x323)) % 182.17/182.13 [33]~E(x331,x332)+E(f11(x333,x331),f11(x333,x332)) % 182.17/182.13 [34]~E(x341,x342)+E(f8(x341,x343),f8(x342,x343)) % 182.17/182.13 [35]~E(x351,x352)+E(f8(x353,x351),f8(x353,x352)) % 182.17/182.13 [36]~E(x361,x362)+E(f21(x361,x363),f21(x362,x363)) % 182.17/182.13 [37]~E(x371,x372)+E(f21(x373,x371),f21(x373,x372)) % 182.17/182.13 [38]~P1(x381)+P1(x382)+~E(x381,x382) % 182.17/182.13 [39]P11(x392,x393,x394)+~E(x391,x392)+~P11(x391,x393,x394) % 182.17/182.13 [40]P11(x403,x402,x404)+~E(x401,x402)+~P11(x403,x401,x404) % 182.17/182.13 [41]P11(x413,x414,x412)+~E(x411,x412)+~P11(x413,x414,x411) % 182.17/182.13 [42]P13(x422,x423)+~E(x421,x422)+~P13(x421,x423) % 182.17/182.13 [43]P13(x433,x432)+~E(x431,x432)+~P13(x433,x431) % 182.17/182.13 [44]P12(x442,x443,x444)+~E(x441,x442)+~P12(x441,x443,x444) % 182.17/182.13 [45]P12(x453,x452,x454)+~E(x451,x452)+~P12(x453,x451,x454) % 182.17/182.13 [46]P12(x463,x464,x462)+~E(x461,x462)+~P12(x463,x464,x461) % 182.17/182.13 [47]~P2(x471)+P2(x472)+~E(x471,x472) % 182.17/182.13 [48]P6(x482,x483)+~E(x481,x482)+~P6(x481,x483) % 182.17/182.13 [49]P6(x493,x492)+~E(x491,x492)+~P6(x493,x491) % 182.17/182.13 [50]P10(x502,x503)+~E(x501,x502)+~P10(x501,x503) % 182.17/182.13 [51]P10(x513,x512)+~E(x511,x512)+~P10(x513,x511) % 182.17/182.13 [52]~P3(x521)+P3(x522)+~E(x521,x522) % 182.17/182.13 [53]~P7(x531)+P7(x532)+~E(x531,x532) % 182.17/182.13 [54]P15(x542,x543)+~E(x541,x542)+~P15(x541,x543) % 182.17/182.13 [55]P15(x553,x552)+~E(x551,x552)+~P15(x553,x551) % 182.17/182.13 [56]~P4(x561)+P4(x562)+~E(x561,x562) % 182.17/182.13 [57]P9(x572,x573)+~E(x571,x572)+~P9(x571,x573) % 182.17/182.13 [58]P9(x583,x582)+~E(x581,x582)+~P9(x583,x581) % 182.17/182.13 [59]P16(x592,x593)+~E(x591,x592)+~P16(x591,x593) % 182.17/182.13 [60]P16(x603,x602)+~E(x601,x602)+~P16(x603,x601) % 182.17/182.13 [61]P5(x612,x613)+~E(x611,x612)+~P5(x611,x613) % 182.17/182.13 [62]P5(x623,x622)+~E(x621,x622)+~P5(x623,x621) % 182.17/182.13 [63]P14(x632,x633)+~E(x631,x632)+~P14(x631,x633) % 182.17/182.13 [64]P14(x643,x642)+~E(x641,x642)+~P14(x643,x641) % 182.17/182.13 [65]P17(x652,x653)+~E(x651,x652)+~P17(x651,x653) % 182.17/182.13 [66]P17(x663,x662)+~E(x661,x662)+~P17(x663,x661) % 182.17/182.13 [67]P8(x672,x673)+~E(x671,x672)+~P8(x671,x673) % 182.17/182.13 [68]P8(x683,x682)+~E(x681,x682)+~P8(x683,x681) % 182.17/182.13 % 182.17/182.13 %------------------------------------------- % 182.17/182.14 cnf(154,plain, % 182.17/182.14 (~P3(a5)), % 182.17/182.14 inference(scs_inference,[],[74,81,92])). % 182.17/182.14 cnf(156,plain, % 182.17/182.14 (~P6(a5,a1)), % 182.17/182.14 inference(scs_inference,[],[74,69,81,92,93])). % 182.17/182.14 cnf(158,plain, % 182.17/182.14 (~E(a4,a1)), % 182.17/182.14 inference(scs_inference,[],[74,69,81,92,93,49])). % 182.17/182.14 cnf(159,plain, % 182.17/182.14 (~P7(a5)), % 182.17/182.14 inference(scs_inference,[],[74,69,81,92,93,49,82])). % 182.17/182.14 cnf(161,plain, % 182.17/182.14 (~P15(a5,x1611)), % 182.17/182.14 inference(scs_inference,[],[74,69,81,92,93,49,82,86])). % 182.17/182.14 cnf(171,plain, % 182.17/182.14 (P6(x1711,a4)+~E(a5,x1711)), % 182.17/182.14 inference(scs_inference,[],[74,69,81,92,93,49,82,86,110,128,129,85,48])). % 182.17/182.14 cnf(172,plain, % 182.17/182.14 (~P11(x1721,a5,x1722)), % 182.17/182.14 inference(scs_inference,[],[74,69,81,92,93,49,82,86,110,128,129,85,48,130])). % 182.17/182.14 cnf(190,plain, % 182.17/182.14 (~P6(a5,a2)), % 182.17/182.14 inference(scs_inference,[],[154,71,93])). % 182.17/182.14 cnf(195,plain, % 182.17/182.14 (~P6(a5,a3)), % 182.17/182.14 inference(scs_inference,[],[154,72,93])). % 182.17/182.14 cnf(238,plain, % 182.17/182.14 (~P17(x2381,x2382)+P6(x2382,f14(x2382))), % 182.17/182.14 inference(scs_inference,[],[88,91])). % 182.17/182.14 cnf(239,plain, % 182.17/182.14 (~P17(x2391,x2392)+P2(f14(x2391))), % 182.17/182.14 inference(scs_inference,[],[89,83])). % 182.17/182.14 cnf(240,plain, % 182.17/182.14 (P13(a4,a4)), % 182.17/182.14 inference(scs_inference,[],[74,90,84])). % 182.17/182.14 cnf(241,plain, % 182.17/182.14 (P13(a4,x2411)+~E(a4,x2411)), % 182.17/182.14 inference(scs_inference,[],[240,43])). % 182.17/182.14 cnf(242,plain, % 182.17/182.14 (P13(x2421,a4)+~E(a4,x2421)), % 182.17/182.14 inference(scs_inference,[],[240,43,42])). % 182.17/182.14 cnf(249,plain, % 182.17/182.14 (~P8(x2491,x2492)+~P14(x2492,x2491)), % 182.17/182.14 inference(scs_inference,[],[94,102])). % 182.17/182.14 cnf(253,plain, % 182.17/182.14 (P6(x2531,f14(x2531))+~P16(x2532,x2531)), % 182.17/182.14 inference(scs_inference,[],[95,238])). % 182.17/182.14 cnf(285,plain, % 182.17/182.14 (~P8(x2851,x2852)+~P11(x2852,x2851,x2853)), % 182.17/182.14 inference(scs_inference,[],[249,130])). % 182.17/182.14 cnf(300,plain, % 182.17/182.14 (~P11(x3001,x3002,a4)+P6(f6(f22(a4,x3001,x3002)),a1)), % 182.17/182.14 inference(scs_inference,[],[97,147])). % 182.17/182.14 cnf(312,plain, % 182.17/182.14 (~E(a5,x3121)+P6(f12(x3121),a23)), % 182.17/182.14 inference(scs_inference,[],[98,171])). % 182.17/182.14 cnf(313,plain, % 182.17/182.14 (P6(f12(a5),a23)), % 182.17/182.14 inference(equality_inference,[],[312])). % 182.17/182.14 cnf(326,plain, % 182.17/182.14 (P17(f6(a5),a5)), % 182.17/182.14 inference(scs_inference,[],[74,99,95])). % 182.17/182.14 cnf(331,plain, % 182.17/182.14 (~P15(x3311,x3312)+P1(f15(x3311,f7(x3312,x3311)))), % 182.17/182.14 inference(scs_inference,[],[104,112])). % 182.17/182.14 cnf(332,plain, % 182.17/182.14 (~P11(x3321,f11(a4,a5),a4)), % 182.17/182.14 inference(scs_inference,[],[81,74,131,120])). % 182.17/182.14 cnf(333,plain, % 182.17/182.14 (~P12(x3331,f11(a4,a5),a4)), % 182.17/182.14 inference(scs_inference,[],[332,138])). % 182.17/182.14 cnf(343,plain, % 182.17/182.14 (~P16(x3431,x3432)+P4(x3432)), % 182.17/182.14 inference(scs_inference,[],[253,87])). % 182.17/182.14 cnf(358,plain, % 182.17/182.14 (~P11(x3581,x3582,x3583)+~P14(x3582,x3581)), % 182.17/182.14 inference(scs_inference,[],[285,94])). % 182.17/182.14 cnf(377,plain, % 182.17/182.14 (~P11(x3771,x3772,x3773)+~P11(x3772,x3771,x3774)), % 182.17/182.14 inference(scs_inference,[],[358,130])). % 182.17/182.14 cnf(378,plain, % 182.17/182.14 (~E(x3781,x3782)+E(f14(x3782),f14(x3781))), % 182.17/182.14 inference(scs_inference,[],[4,2])). % 182.17/182.14 cnf(380,plain, % 182.17/182.14 (~E(x3801,x3802)+E(f6(f17(x3801,x3803,x3804)),f6(f17(x3802,x3803,x3804)))), % 182.17/182.14 inference(scs_inference,[],[8,5])). % 182.17/182.14 cnf(382,plain, % 182.17/182.14 (~E(x3821,x3822)+E(f12(f17(x3823,x3821,x3824)),f12(f17(x3823,x3822,x3824)))), % 182.17/182.14 inference(scs_inference,[],[9,6])). % 182.17/182.14 cnf(384,plain, % 182.17/182.14 (~E(x3841,x3842)+E(f13(f17(x3843,x3844,x3841)),f13(f17(x3843,x3844,x3842)))), % 182.17/182.14 inference(scs_inference,[],[15,7])). % 182.17/182.14 cnf(386,plain, % 182.17/182.14 (P6(a5,f16(f6(a5),a5))), % 182.17/182.14 inference(scs_inference,[],[74,107,99])). % 182.17/182.14 cnf(388,plain, % 182.17/182.14 (P6(x3881,f16(f6(a5),a5))+~E(a5,x3881)), % 182.17/182.14 inference(scs_inference,[],[156,386,49,48])). % 182.17/182.14 cnf(389,plain, % 182.17/182.14 (E(a4,f16(f6(a5),a5))), % 182.17/182.14 inference(scs_inference,[],[74,156,386,49,48,103])). % 182.17/182.14 cnf(399,plain, % 182.17/182.14 (E(f16(f6(a5),a5),a4)), % 182.17/182.14 inference(scs_inference,[],[389,241,242,2])). % 182.17/182.14 cnf(400,plain, % 182.17/182.14 (~P1(f16(f6(a5),a5))), % 182.17/182.14 inference(scs_inference,[],[389,81,241,242,2,38])). % 182.17/182.14 cnf(514,plain, % 182.17/182.14 (~P15(x5141,x5142)+P6(x5141,f15(x5141,f7(x5142,x5141)))), % 182.17/182.14 inference(scs_inference,[],[109,112])). % 182.17/182.14 cnf(515,plain, % 182.17/182.14 (~P11(x5151,x5152,x5153)+P13(f9(x5153,x5151,x5152),f15(x5151,f9(x5153,x5151,x5152)))), % 182.17/182.14 inference(scs_inference,[],[113,145])). % 182.17/182.14 cnf(516,plain, % 182.17/182.14 (P13(f7(a4,f11(a4,a5)),a4)), % 182.17/182.14 inference(scs_inference,[],[81,74,114,120])). % 182.17/182.14 cnf(557,plain, % 182.17/182.14 (~P11(f12(a5),f6(a5),x5571)), % 182.17/182.14 inference(scs_inference,[],[74,377,126])). % 182.17/182.14 cnf(558,plain, % 182.17/182.14 (~P12(f12(a5),f6(a5),x5581)), % 182.17/182.14 inference(scs_inference,[],[557,138])). % 182.17/182.14 cnf(612,plain, % 182.17/182.14 (~P11(x6121,x6122,a4)+P11(f12(f22(a4,x6121,x6122)),f13(f22(a4,x6121,x6122)),a4)), % 182.17/182.14 inference(scs_inference,[],[127,147])). % 182.17/182.14 cnf(613,plain, % 182.17/182.14 (~E(f15(x6131,f7(x6132,x6131)),a4)+~P15(x6131,x6132)), % 182.17/182.14 inference(scs_inference,[],[81,331,38])). % 182.17/182.14 cnf(661,plain, % 182.17/182.14 (~P6(f12(a5),a2)), % 182.17/182.14 inference(scs_inference,[],[77,313,103])). % 182.17/182.14 cnf(685,plain, % 182.17/182.14 (P17(f6(a5),f22(a4,f6(a5),f12(a5)))), % 182.17/182.14 inference(scs_inference,[],[74,144,126])). % 182.17/182.14 cnf(686,plain, % 182.17/182.14 (P17(f6(a5),x6861)+~E(f22(a4,f6(a5),f12(a5)),x6861)), % 182.17/182.14 inference(scs_inference,[],[685,66])). % 182.17/182.14 cnf(692,plain, % 182.17/182.14 (P5(f13(a5),f10(a4,f12(a5),f13(a5)))), % 182.17/182.14 inference(scs_inference,[],[74,146,127])). % 182.17/182.14 cnf(694,plain, % 182.17/182.14 (P5(f13(a5),x6941)+~E(f10(a4,f12(a5),f13(a5)),x6941)), % 182.17/182.14 inference(scs_inference,[],[692,61,62])). % 182.17/182.14 cnf(695,plain, % 182.17/182.14 (P17(x6951,f22(a4,f6(a5),f12(a5)))+~E(f6(a5),x6951)), % 182.17/182.14 inference(scs_inference,[],[692,685,61,62,65])). % 182.17/182.14 cnf(709,plain, % 182.17/182.14 (P13(f10(a4,f12(a5),f13(a5)),a4)), % 182.17/182.14 inference(scs_inference,[],[74,149,127])). % 182.17/182.14 cnf(719,plain, % 182.17/182.14 (~P15(x7191,x7192)+P4(x7191)), % 182.17/182.14 inference(scs_inference,[],[514,87])). % 182.17/182.14 cnf(720,plain, % 182.17/182.14 (~P15(x7201,x7202)+P2(f14(x7201))), % 182.17/182.14 inference(scs_inference,[],[719,83])). % 182.17/182.14 cnf(721,plain, % 182.17/182.14 (P13(f14(x7211),f14(x7211))+~P15(x7211,x7212)), % 182.17/182.14 inference(scs_inference,[],[720,84])). % 182.17/182.14 cnf(759,plain, % 182.17/182.14 (P6(f6(f22(a4,f6(a5),f12(a5))),a1)), % 182.17/182.14 inference(scs_inference,[],[74,300,126])). % 182.17/182.14 cnf(804,plain, % 182.17/182.14 (~P11(x8041,x8042,x8043)+P13(x8044,f15(x8041,f9(x8043,x8041,x8042)))+~E(f9(x8043,x8041,x8042),x8044)), % 182.17/182.14 inference(scs_inference,[],[515,42])). % 182.17/182.14 cnf(806,plain, % 182.17/182.14 (P15(f11(a4,a5),f16(f6(a5),a5))), % 182.17/182.14 inference(scs_inference,[],[389,81,74,55,120])). % 182.17/182.14 cnf(813,plain, % 182.17/182.14 (P15(f11(a4,a5),a4)), % 182.17/182.14 inference(scs_inference,[],[399,161,806,131,138,54,55])). % 182.17/182.14 cnf(835,plain, % 182.17/182.14 (~P8(x8351,x8352)+~P14(x8352,x8353)+P8(x8351,x8353)), % 182.17/182.14 inference(scs_inference,[],[106,94])). % 182.17/182.14 cnf(837,plain, % 182.17/182.14 (~P8(x8371,x8372)+~P8(x8372,x8373)+~P14(x8373,x8371)), % 182.17/182.14 inference(scs_inference,[],[835,102])). % 182.17/182.14 cnf(838,plain, % 182.17/182.14 (~P8(x8381,x8382)+~P11(x8383,x8381,x8384)+~P8(x8382,x8383)), % 182.17/182.14 inference(scs_inference,[],[837,130])). % 182.17/182.14 cnf(847,plain, % 182.17/182.14 (P17(f11(a4,a5),a5)), % 182.17/182.14 inference(scs_inference,[],[74,389,400,121,38])). % 182.17/182.14 cnf(848,plain, % 182.17/182.14 (P17(x8481,a5)+~E(f11(a4,a5),x8481)), % 182.17/182.14 inference(scs_inference,[],[847,65])). % 182.17/182.14 cnf(887,plain, % 182.17/182.14 (~P8(x8871,x8872)+~P14(x8872,x8873)+~P11(x8873,x8871,x8874)), % 182.17/182.14 inference(scs_inference,[],[838,94])). % 182.17/182.14 cnf(890,plain, % 182.17/182.14 (P11(f6(a5),f12(a5),f16(f6(a5),a5))), % 182.17/182.14 inference(scs_inference,[],[389,74,41,126])). % 182.17/182.14 cnf(891,plain, % 182.17/182.14 (P11(f6(a5),f12(a5),a4)), % 182.17/182.14 inference(scs_inference,[],[890,399,41])). % 182.17/182.14 cnf(892,plain, % 182.17/182.14 (~P11(x8921,f6(a5),f16(f6(a5),a5))+P11(x8921,f12(a5),f16(f6(a5),a5))), % 182.17/182.14 inference(scs_inference,[],[890,399,41,150])). % 182.17/182.14 cnf(894,plain, % 182.17/182.14 (~E(f12(a5),f11(a4,a5))), % 182.17/182.14 inference(scs_inference,[],[890,399,332,41,150,40])). % 182.17/182.14 cnf(896,plain, % 182.17/182.14 (~P12(x8961,f6(a5),f16(f6(a5),a5))+P11(x8961,f12(a5),f16(f6(a5),a5))), % 182.17/182.14 inference(scs_inference,[],[890,399,332,41,150,40,138])). % 182.17/182.14 cnf(903,plain, % 182.17/182.14 (P14(x9031,f12(a5))+~P11(x9031,f6(a5),f16(f6(a5),a5))), % 182.17/182.14 inference(scs_inference,[],[892,130])). % 182.17/182.14 cnf(904,plain, % 182.17/182.14 (~P12(f6(a5),x9041,f16(f6(a5),a5))+~P11(f12(a5),x9041,f16(f6(a5),a5))), % 182.17/182.14 inference(scs_inference,[],[890,151])). % 182.17/182.14 cnf(908,plain, % 182.17/182.14 (P11(x9081,f12(a5),f16(f6(a5),a5))+~E(f6(a5),x9081)), % 182.17/182.14 inference(scs_inference,[],[890,891,151,150,39])). % 182.17/182.14 cnf(909,plain, % 182.17/182.14 (P11(x9091,f12(a5),a4)+~E(f6(a5),x9091)), % 182.17/182.14 inference(scs_inference,[],[890,891,399,151,150,39,41])). % 182.17/182.14 cnf(914,plain, % 182.17/182.14 (~P12(f6(a5),x9141,a4)+~P11(f12(a5),x9141,a4)), % 182.17/182.14 inference(scs_inference,[],[891,151])). % 182.17/182.14 cnf(916,plain, % 182.17/182.14 (~P16(f11(a4,a5),a5)+~P16(f12(a5),a5)), % 182.17/182.14 inference(scs_inference,[],[74,891,894,151,122])). % 182.17/182.14 cnf(924,plain, % 182.17/182.14 (~P16(x9241,a5)+~E(x9241,f12(a5))+~P16(f11(a4,a5),a5)), % 182.17/182.14 inference(scs_inference,[],[916,59])). % 182.17/182.14 cnf(931,plain, % 182.17/182.14 (~P12(f6(a5),f13(a5),a4)), % 182.17/182.14 inference(scs_inference,[],[74,914,127])). % 182.17/182.14 cnf(1010,plain, % 182.17/182.14 (~E(x10101,a5)+~P7(x10101)), % 182.17/182.14 inference(scs_inference,[],[154,82,53])). % 182.17/182.14 cnf(1012,plain, % 182.17/182.14 (P13(f14(x10121),f14(x10121))+~P4(x10121)), % 182.17/182.14 inference(scs_inference,[],[83,84])). % 182.17/182.14 cnf(1015,plain, % 182.17/182.14 (~E(f14(x10151),x10152)+~P4(x10151)+P2(x10152)), % 182.17/182.14 inference(scs_inference,[],[83,47])). % 182.17/182.14 cnf(1020,plain, % 182.17/182.14 (~P14(x10201,x10202)+~E(x10202,a5)), % 182.17/182.14 inference(scs_inference,[],[85,1010])). % 182.17/182.14 cnf(1022,plain, % 182.17/182.14 (P3(f11(a4,a5))), % 182.17/182.14 inference(scs_inference,[],[806,86,82])). % 182.17/182.14 cnf(1023,plain, % 182.17/182.14 (~P6(f11(a4,a5),a4)), % 182.17/182.14 inference(scs_inference,[],[81,1022,92])). % 182.17/182.14 cnf(1025,plain, % 182.17/182.14 (P7(f11(a4,a5))), % 182.17/182.14 inference(scs_inference,[],[81,74,86,120])). % 182.17/182.14 cnf(1026,plain, % 182.17/182.14 (~P6(f11(a4,a5),f16(f6(a5),a5))), % 182.17/182.14 inference(scs_inference,[],[400,1022,92])). % 182.17/182.14 cnf(1028,plain, % 182.17/182.14 (~E(a5,f11(a4,a5))), % 182.17/182.14 inference(scs_inference,[],[74,1023,400,1022,92,48])). % 182.17/182.14 cnf(1029,plain, % 182.17/182.14 (P14(x10291,f11(a4,a5))+~P8(x10291,f11(a4,a5))), % 182.17/182.14 inference(scs_inference,[],[813,86,100])). % 182.17/182.14 cnf(1031,plain, % 182.17/182.14 (P15(f11(a4,a5),x10311)+~P5(f11(a4,a5),x10311)), % 182.17/182.14 inference(scs_inference,[],[806,86,101])). % 182.17/182.14 cnf(1032,plain, % 182.17/182.14 (P15(f11(a4,a5),f7(a4,f11(a4,a5)))), % 182.17/182.14 inference(scs_inference,[],[813,1031,112])). % 182.17/182.14 cnf(1033,plain, % 182.17/182.14 (~P11(x10331,f11(a4,a5),f7(a4,f11(a4,a5)))), % 182.17/182.14 inference(scs_inference,[],[1032,131])). % 182.17/182.14 cnf(1035,plain, % 182.17/182.14 (~P12(x10351,f11(a4,a5),f7(a4,f11(a4,a5)))), % 182.17/182.14 inference(scs_inference,[],[1032,131,138])). % 182.17/182.14 cnf(1037,plain, % 182.17/182.14 (P15(f11(a4,a5),x10371)+~E(f7(a4,f11(a4,a5)),x10371)), % 182.17/182.14 inference(scs_inference,[],[1032,131,138,55])). % 182.17/182.14 cnf(1039,plain, % 182.17/182.14 (P6(a5,f14(a5))), % 182.17/182.14 inference(scs_inference,[],[74,87,91])). % 182.17/182.14 cnf(1040,plain, % 182.17/182.14 (~E(f14(a5),a1)), % 182.17/182.14 inference(scs_inference,[],[156,1039,49])). % 182.17/182.14 cnf(1042,plain, % 182.17/182.14 (E(a4,f14(a5))), % 182.17/182.14 inference(scs_inference,[],[74,156,1039,49,48,103])). % 182.17/182.14 cnf(1047,plain, % 182.17/182.14 (P4(f6(a5))), % 182.17/182.14 inference(scs_inference,[],[74,87,97])). % 182.17/182.14 cnf(1048,plain, % 182.17/182.14 (E(f14(a5),a4)), % 182.17/182.14 inference(scs_inference,[],[1042,2])). % 182.17/182.14 cnf(1051,plain, % 182.17/182.14 (~P1(f14(a5))), % 182.17/182.14 inference(scs_inference,[],[1042,81,2,241,242,38])). % 182.17/182.14 cnf(1052,plain, % 182.17/182.14 (E(f16(f6(a5),a5),f14(a5))), % 182.17/182.14 inference(scs_inference,[],[1042,399,81,2,241,242,38,3])). % 182.17/182.14 cnf(1053,plain, % 182.17/182.14 (~P6(f11(a4,a5),f14(a5))), % 182.17/182.14 inference(scs_inference,[],[1022,1042,399,81,2,241,242,38,3,92])). % 182.17/182.14 cnf(1058,plain, % 182.17/182.14 (P2(x10581)+~E(f14(f6(a5)),x10581)), % 182.17/182.14 inference(scs_inference,[],[1022,389,1047,1042,195,399,81,1039,2,241,242,38,3,92,42,43,49,1015])). % 182.17/182.14 cnf(1066,plain, % 182.17/182.14 (P2(f14(f6(a5)))), % 182.17/182.14 inference(equality_inference,[],[1058])). % 182.17/182.14 cnf(1068,plain, % 182.17/182.14 (E(f14(a5),f16(f6(a5),a5))), % 182.17/182.14 inference(scs_inference,[],[1052,2])). % 182.17/182.14 cnf(1110,plain, % 182.17/182.14 (~P17(x11101,f14(a5))+P4(a4)), % 182.17/182.14 inference(scs_inference,[],[1048,56,719,89,343,87,88])). % 182.17/182.14 cnf(1202,plain, % 182.17/182.14 (P11(f6(a5),f12(a5),f14(a5))), % 182.17/182.14 inference(scs_inference,[],[1042,891,41])). % 182.17/182.14 cnf(1203,plain, % 182.17/182.14 (P15(f11(a4,a5),f14(a5))), % 182.17/182.14 inference(scs_inference,[],[1042,891,813,41,55])). % 182.17/182.14 cnf(1204,plain, % 182.17/182.14 (P13(f7(a4,f11(a4,a5)),f14(a5))), % 182.17/182.14 inference(scs_inference,[],[1042,891,516,813,41,55,43])). % 182.17/182.14 cnf(1205,plain, % 182.17/182.14 (~P11(x12051,f11(a4,a5),f14(a5))), % 182.17/182.14 inference(scs_inference,[],[1042,891,516,813,41,55,43,131])). % 182.17/182.14 cnf(1207,plain, % 182.17/182.14 (~P12(x12071,f11(a4,a5),f14(a5))), % 182.17/182.14 inference(scs_inference,[],[1042,891,516,813,41,55,43,131,138])). % 182.17/182.14 cnf(1209,plain, % 182.17/182.14 (P11(x12091,f12(a5),f14(a5))+~E(f6(a5),x12091)), % 182.17/182.14 inference(scs_inference,[],[1042,891,516,813,41,55,43,131,138,39])). % 182.17/182.14 cnf(1218,plain, % 182.17/182.14 (~P11(x12181,f6(a5),f14(a5))+P11(x12181,f12(a5),f14(a5))), % 182.17/182.14 inference(scs_inference,[],[1042,1202,709,43,151,150])). % 182.17/182.14 cnf(1281,plain, % 182.17/182.14 (~E(f14(a5),a2)), % 182.17/182.14 inference(scs_inference,[],[190,1039,49])). % 182.17/182.14 cnf(1587,plain, % 182.17/182.14 (P14(x15871,f12(a5))+~P11(x15871,f6(a5),f14(a5))), % 182.17/182.14 inference(scs_inference,[],[1218,130])). % 182.17/182.14 cnf(1694,plain, % 182.17/182.14 (P4(f13(a5))), % 182.17/182.14 inference(scs_inference,[],[692,87,109])). % 182.17/182.14 cnf(1698,plain, % 182.17/182.14 (P4(f22(f16(f6(a5),a5),f6(a5),f12(a5)))), % 182.17/182.14 inference(scs_inference,[],[890,87,147])). % 182.17/182.14 cnf(1719,plain, % 182.17/182.14 (P6(f11(a4,a5),f14(f11(a4,a5)))), % 182.17/182.14 inference(scs_inference,[],[847,89,91])). % 182.17/182.14 cnf(1721,plain, % 182.17/182.14 (P6(x17211,f14(f11(a4,a5)))+~E(f11(a4,a5),x17211)), % 182.17/182.14 inference(scs_inference,[],[1053,1719,49,48])). % 182.17/182.14 cnf(1752,plain, % 182.17/182.14 (P2(a1)), % 182.17/182.14 inference(scs_inference,[],[74,90,97])). % 182.17/182.14 cnf(1753,plain, % 182.17/182.14 (P2(a23)), % 182.17/182.14 inference(scs_inference,[],[74,90,98])). % 182.17/182.14 cnf(1754,plain, % 182.17/182.14 (P2(f15(f13(a5),f10(a4,f12(a5),f13(a5))))), % 182.17/182.14 inference(scs_inference,[],[692,90,109])). % 182.17/182.14 cnf(1764,plain, % 182.17/182.14 (P2(a3)+P6(f13(a5),a2)), % 182.17/182.14 inference(scs_inference,[],[74,90,105])). % 182.17/182.14 cnf(1882,plain, % 182.17/182.14 (~P16(a1,f11(a4,a5))+~P16(f14(a5),f11(a4,a5))), % 182.17/182.14 inference(scs_inference,[],[1719,1040,122])). % 182.17/182.14 cnf(1936,plain, % 182.17/182.14 (~P16(a1,x19361)+~E(x19361,f11(a4,a5))+~P16(f14(a5),f11(a4,a5))), % 182.17/182.14 inference(scs_inference,[],[1882,60])). % 182.17/182.14 cnf(2480,plain, % 182.17/182.14 (E(f12(f16(f6(a5),a5)),f12(a4))), % 182.17/182.14 inference(scs_inference,[],[389,2,9])). % 182.17/182.14 cnf(2486,plain, % 182.17/182.14 (E(f13(f16(f6(a5),a5)),f13(a4))), % 182.17/182.14 inference(scs_inference,[],[389,2,15])). % 182.17/182.14 cnf(2487,plain, % 182.17/182.14 (E(f22(f16(f6(a5),a5),x24871,x24872),f22(a4,x24871,x24872))), % 182.17/182.14 inference(scs_inference,[],[389,2,16])). % 182.17/182.14 cnf(2491,plain, % 182.17/182.14 (E(f16(x24911,f16(f6(a5),a5)),f16(x24911,a4))), % 182.17/182.14 inference(scs_inference,[],[389,2,20])). % 182.17/182.14 cnf(2495,plain, % 182.17/182.14 (E(f19(x24951,f16(f6(a5),a5)),f19(x24951,a4))), % 182.17/182.14 inference(scs_inference,[],[389,2,24])). % 182.17/182.14 cnf(2496,plain, % 182.17/182.14 (E(f9(f16(f6(a5),a5),x24961,x24962),f9(a4,x24961,x24962))), % 182.17/182.14 inference(scs_inference,[],[389,2,25])). % 182.17/182.14 cnf(2501,plain, % 182.17/182.14 (E(f7(f16(f6(a5),a5),x25011),f7(a4,x25011))), % 182.17/182.14 inference(scs_inference,[],[389,2,30])). % 182.17/182.14 cnf(2503,plain, % 182.17/182.14 (E(f11(f16(f6(a5),a5),x25031),f11(a4,x25031))), % 182.17/182.14 inference(scs_inference,[],[389,2,32])). % 182.17/182.14 cnf(2510,plain, % 182.17/182.14 (E(f6(f16(f6(a5),a5)),f6(a4))), % 182.17/182.14 inference(scs_inference,[],[389,2,8])). % 182.17/182.14 cnf(2511,plain, % 182.17/182.14 (~E(a4,f15(f11(a4,a5),f7(a4,f11(a4,a5))))), % 182.17/182.14 inference(scs_inference,[],[813,2,613])). % 182.17/182.14 cnf(2519,plain, % 182.17/182.14 (~E(a1,f14(a5))), % 182.17/182.14 inference(scs_inference,[],[158,1048,2,3])). % 182.17/182.14 cnf(2525,plain, % 182.17/182.14 (P6(x25251,f14(f6(a5)))+~E(f6(a5),x25251)), % 182.17/182.14 inference(scs_inference,[],[1047,91,48])). % 182.17/182.14 cnf(2526,plain, % 182.17/182.14 (P6(f6(a5),f14(f6(a5)))), % 182.17/182.14 inference(equality_inference,[],[2525])). % 182.17/182.14 cnf(2527,plain, % 182.17/182.14 (P6(f6(a5),x25271)+~E(f14(f6(a5)),x25271)), % 182.17/182.14 inference(scs_inference,[],[2526,49])). % 182.17/182.14 cnf(2550,plain, % 182.17/182.14 (P1(f14(f6(a5)))+~P3(f6(a5))), % 182.17/182.14 inference(scs_inference,[],[1047,91,92])). % 182.17/182.14 cnf(2551,plain, % 182.17/182.14 (~E(f14(f6(a5)),a4)+~P3(f6(a5))), % 182.17/182.14 inference(scs_inference,[],[81,2550,38])). % 182.17/182.14 cnf(2569,plain, % 182.17/182.14 (~P17(x25691,f14(a5))+P6(a4,f14(a4))), % 182.17/182.14 inference(scs_inference,[],[91,1110])). % 182.17/182.14 cnf(2570,plain, % 182.17/182.14 (P2(f14(a4))+~P17(x25701,f14(a5))), % 182.17/182.14 inference(scs_inference,[],[2569,90])). % 182.17/182.14 cnf(2571,plain, % 182.17/182.14 (~E(f22(a4,f6(a5),f12(a5)),f14(a5))+P2(f14(a4))), % 182.17/182.14 inference(scs_inference,[],[2570,686])). % 182.17/182.14 cnf(2572,plain, % 182.17/182.14 (~E(f14(a5),f22(a4,f6(a5),f12(a5)))+P2(f14(a4))), % 182.17/182.14 inference(scs_inference,[],[2571,2])). % 182.17/182.14 cnf(2573,plain, % 182.17/182.14 (~E(a4,f22(a4,f6(a5),f12(a5)))+P2(f14(a4))), % 182.17/182.14 inference(scs_inference,[],[1048,2572,3])). % 182.17/182.14 cnf(2574,plain, % 182.17/182.14 (~E(f22(a4,f6(a5),f12(a5)),a4)+P2(f14(a4))), % 182.17/182.14 inference(scs_inference,[],[2573,2])). % 182.17/182.14 cnf(2575,plain, % 182.17/182.14 (~P6(a5,f22(a4,f6(a5),f12(a5)))+P2(f14(a4))), % 182.17/182.14 inference(scs_inference,[],[74,2574,103])). % 182.17/182.14 cnf(2576,plain, % 182.17/182.14 (P13(f14(a4),f14(a4))+~P6(a5,f22(a4,f6(a5),f12(a5)))), % 182.17/182.14 inference(scs_inference,[],[2575,84])). % 182.17/182.14 cnf(2577,plain, % 182.17/182.14 (P13(x25771,f14(a4))+~E(f14(a4),x25771)+~P6(a5,f22(a4,f6(a5),f12(a5)))), % 182.17/182.14 inference(scs_inference,[],[2576,42])). % 182.17/182.14 cnf(2754,plain, % 182.17/182.14 (~E(a1,a4)), % 182.17/182.14 inference(scs_inference,[],[2519,1042,3])). % 182.17/182.14 cnf(2757,plain, % 182.17/182.14 (~E(a1,f16(f6(a5),a5))), % 182.17/182.14 inference(scs_inference,[],[2519,1052,3])). % 182.17/182.14 cnf(2973,plain, % 182.17/182.14 (P6(f12(a5),f14(f12(a5)))), % 182.17/182.14 inference(scs_inference,[],[313,91,87])). % 182.17/182.14 cnf(3503,plain, % 182.17/182.14 (P13(a1,a1)), % 182.17/182.14 inference(scs_inference,[],[1752,84])). % 182.17/182.14 cnf(3507,plain, % 182.17/182.14 (~P8(f12(a5),f6(a5))), % 182.17/182.14 inference(scs_inference,[],[1752,1202,84,132,285])). % 182.17/182.14 cnf(3511,plain, % 182.17/182.14 (P16(f6(a5),a5)), % 182.17/182.14 inference(scs_inference,[],[74,1752,1202,84,132,285,358,99])). % 182.17/182.14 cnf(3513,plain, % 182.17/182.14 (P6(f6(a5),a1)), % 182.17/182.14 inference(scs_inference,[],[74,1752,1202,84,132,285,358,99,97])). % 182.17/182.14 cnf(3515,plain, % 182.17/182.14 (P11(f12(a5),f13(a5),a4)), % 182.17/182.14 inference(scs_inference,[],[74,1752,1202,84,132,285,358,99,97,127])). % 182.17/182.14 cnf(3517,plain, % 182.17/182.14 (~P11(f13(a5),f12(a5),x35171)), % 182.17/182.14 inference(scs_inference,[],[74,1752,1202,84,132,285,358,99,97,127,377])). % 182.17/182.14 cnf(3521,plain, % 182.17/182.14 (~P15(f12(a5),f14(a5))), % 182.17/182.14 inference(scs_inference,[],[74,1752,1202,84,132,285,358,99,97,127,377,130,131])). % 182.17/182.14 cnf(3523,plain, % 182.17/182.14 (P7(f12(a5))), % 182.17/182.14 inference(scs_inference,[],[74,1752,1202,84,132,285,358,99,97,127,377,130,131,85])). % 182.17/182.14 cnf(3526,plain, % 182.17/182.14 (P3(f12(a5))), % 182.17/182.14 inference(scs_inference,[],[74,1752,1202,1281,84,132,285,358,99,97,127,377,130,131,85,2,82])). % 182.17/182.14 cnf(3530,plain, % 182.17/182.14 (~P9(f6(a5),a5)), % 182.17/182.14 inference(scs_inference,[],[74,1752,1202,1281,1039,84,132,285,358,99,97,127,377,130,131,85,2,82,136,137])). % 182.17/182.14 cnf(3532,plain, % 182.17/182.14 (~P8(f13(a5),f6(a5))), % 182.17/182.14 inference(scs_inference,[],[74,1752,1202,1281,1039,84,132,285,358,99,97,127,377,130,131,85,2,82,136,137,887])). % 182.17/182.14 cnf(3537,plain, % 182.17/182.14 (~P6(f6(a5),a4)), % 182.17/182.14 inference(scs_inference,[],[74,1752,2754,557,1202,1281,1039,84,132,285,358,99,97,127,377,130,131,85,2,82,136,137,887,150,103])). % 182.17/182.14 cnf(3539,plain, % 182.17/182.14 (~E(f6(a5),f13(a5))), % 182.17/182.14 inference(scs_inference,[],[74,1752,2754,557,1202,1281,1039,84,132,285,358,99,97,127,377,130,131,85,2,82,136,137,887,150,103,39])). % 182.17/182.14 cnf(3541,plain, % 182.17/182.14 (P3(f6(a5))), % 182.17/182.14 inference(scs_inference,[],[74,1752,2754,557,71,1202,1281,69,1039,81,84,132,285,358,99,97,127,377,130,131,85,2,82,136,137,887,150,103,39,38,93])). % 182.17/182.14 cnf(3543,plain, % 182.17/182.14 (P5(f6(a5),a1)), % 182.17/182.14 inference(scs_inference,[],[74,1752,2754,557,71,1202,1281,69,1039,81,84,132,285,358,99,97,127,377,130,131,85,2,82,136,137,887,150,103,39,38,93,115])). % 182.17/182.14 cnf(3545,plain, % 182.17/182.14 (~P10(f6(a5),a4)), % 182.17/182.14 inference(scs_inference,[],[74,1752,2754,557,71,1202,1281,69,326,1039,81,84,132,285,358,99,97,127,377,130,131,85,2,82,136,137,887,150,103,39,38,93,115,125])). % 182.17/182.14 cnf(3547,plain, % 182.17/182.14 (P16(f11(a4,a5),a5)), % 182.17/182.14 inference(scs_inference,[],[74,1752,2754,557,71,1202,1281,69,326,813,847,1039,81,84,132,285,358,99,97,127,377,130,131,85,2,82,136,137,887,150,103,39,38,93,115,125,124])). % 182.17/182.14 cnf(3549,plain, % 182.17/182.14 (P8(f6(a5),f12(a5))), % 182.17/182.14 inference(scs_inference,[],[74,1752,2754,557,71,1202,1281,69,326,813,847,1039,81,84,132,285,358,99,97,127,377,130,131,85,2,82,136,137,887,150,103,39,38,93,115,125,124,94])). % 182.17/182.14 cnf(3551,plain, % 182.17/182.14 (~E(a5,f6(a5))), % 182.17/182.14 inference(scs_inference,[],[74,1752,2754,557,71,1202,1281,69,326,813,847,1039,81,84,132,285,358,99,97,127,377,130,131,85,2,82,136,137,887,150,103,39,38,93,115,125,124,94,171])). % 182.17/182.14 cnf(3560,plain, % 182.17/182.14 (~E(x35601,f12(a5))+~P16(x35601,a5)), % 182.17/182.14 inference(scs_inference,[],[3547,924])). % 182.17/182.14 cnf(3561,plain, % 182.17/182.14 (P1(f14(f6(a5)))), % 182.17/182.14 inference(scs_inference,[],[3541,2550])). % 182.17/182.14 cnf(3562,plain, % 182.17/182.14 (~E(f14(f6(a5)),a4)), % 182.17/182.14 inference(scs_inference,[],[3541,2551])). % 182.17/182.14 cnf(3563,plain, % 182.17/182.14 (~E(f12(a5),f6(a5))), % 182.17/182.14 inference(scs_inference,[],[3511,3560,2])). % 182.17/182.14 cnf(3565,plain, % 182.17/182.14 (~E(f11(a4,a5),f12(a5))), % 182.17/182.14 inference(scs_inference,[],[3547,3560])). % 182.17/182.14 cnf(3569,plain, % 182.17/182.14 (~P10(f12(a5),a4)), % 182.17/182.14 inference(scs_inference,[],[1753,3515,3547,3560,84,132])). % 182.17/182.14 cnf(3577,plain, % 182.17/182.14 (~P15(f13(a5),a4)), % 182.17/182.14 inference(scs_inference,[],[1753,3515,3547,3560,84,132,285,358,130,131])). % 182.17/182.14 cnf(3579,plain, % 182.17/182.14 (P7(f13(a5))), % 182.17/182.14 inference(scs_inference,[],[1753,3515,3547,3560,84,132,285,358,130,131,85])). % 182.17/182.14 cnf(3581,plain, % 182.17/182.14 (P3(f13(a5))), % 182.17/182.14 inference(scs_inference,[],[1753,3515,3547,3560,84,132,285,358,130,131,85,82])). % 182.17/182.14 cnf(3583,plain, % 182.17/182.14 (~E(f6(a5),f12(a5))), % 182.17/182.14 inference(scs_inference,[],[1753,3515,3563,3547,3560,84,132,285,358,130,131,85,82,2])). % 182.17/182.14 cnf(3584,plain, % 182.17/182.14 (~P12(f6(a5),f13(a5),f14(a5))), % 182.17/182.14 inference(scs_inference,[],[1753,3515,931,3563,3547,1048,3560,84,132,285,358,130,131,85,82,2,46])). % 182.17/182.14 cnf(3587,plain, % 182.17/182.14 (P8(f6(a5),f13(a5))), % 182.17/182.14 inference(scs_inference,[],[74,1753,3515,931,3563,3549,3547,1048,3560,84,132,285,358,130,131,85,82,2,46,136,835])). % 182.17/182.14 cnf(3589,plain, % 182.17/182.14 (~P11(f13(a5),f6(a5),x35891)), % 182.17/182.14 inference(scs_inference,[],[74,1753,3515,931,3563,3549,3547,1048,3560,84,132,285,358,130,131,85,82,2,46,136,835,887])). % 182.17/182.14 cnf(3593,plain, % 182.17/182.14 (~P15(f12(a5),a4)), % 182.17/182.14 inference(scs_inference,[],[74,1753,3515,931,3563,3521,3549,3547,1042,1048,3560,84,132,285,358,130,131,85,82,2,46,136,835,887,137,55])). % 182.17/182.14 cnf(3594,plain, % 182.17/182.14 (P14(f6(a5),f13(a5))), % 182.17/182.14 inference(scs_inference,[],[74,1753,3515,931,3563,3521,3549,3547,1042,1048,3560,84,132,285,358,130,131,85,82,2,46,136,835,887,137,55,100])). % 182.17/182.14 cnf(3596,plain, % 182.17/182.14 (~P6(f6(a5),f14(a5))), % 182.17/182.14 inference(scs_inference,[],[74,1753,3515,931,3563,3521,3549,3547,3537,1042,1048,3560,84,132,285,358,130,131,85,82,2,46,136,835,887,137,55,100,49])). % 182.17/182.14 cnf(3598,plain, % 182.17/182.14 (P5(f12(a5),a23)), % 182.17/182.14 inference(scs_inference,[],[74,1753,3515,931,3563,3521,3549,3547,3537,1051,72,70,1042,1048,313,3560,84,132,285,358,130,131,85,82,2,46,136,835,887,137,55,100,49,38,115])). % 182.17/182.14 cnf(3602,plain, % 182.17/182.14 (~E(f13(a5),a5)), % 182.17/182.14 inference(scs_inference,[],[74,1753,3515,931,3563,3521,3549,3547,3537,1051,72,70,1042,1048,313,3560,84,132,285,358,130,131,85,82,2,46,136,835,887,137,55,100,49,38,115,249,1020])). % 182.17/182.14 cnf(3604,plain, % 182.17/182.14 (P8(f12(a5),f13(a5))), % 182.17/182.14 inference(scs_inference,[],[74,1753,3515,931,3563,3521,3549,3547,3537,1051,72,70,1042,1048,313,3560,84,132,285,358,130,131,85,82,2,46,136,835,887,137,55,100,49,38,115,249,1020,94])). % 182.17/182.14 cnf(3606,plain, % 182.17/182.14 (~P14(f13(a5),x36061)+~P8(x36061,f6(a5))), % 182.17/182.14 inference(scs_inference,[],[74,1753,3515,931,3563,3521,3549,3547,3537,1051,72,70,1042,1048,313,3560,84,132,285,358,130,131,85,82,2,46,136,835,887,137,55,100,49,38,115,249,1020,94,837])). % 182.17/182.14 cnf(3615,plain, % 182.17/182.14 (~P5(f13(a5),a4)), % 182.17/182.14 inference(scs_inference,[],[3602,3579,3577,2,101])). % 182.17/182.14 cnf(3617,plain, % 182.17/182.14 (~P15(f13(a5),f14(a5))), % 182.17/182.14 inference(scs_inference,[],[3602,3579,3577,1048,2,101,55])). % 182.17/182.14 cnf(3618,plain, % 182.17/182.14 (~P11(f6(a5),f6(a5),a4)), % 182.17/182.14 inference(scs_inference,[],[74,3583,3602,3539,3579,3577,1048,2,101,55,135])). % 182.17/182.14 cnf(3628,plain, % 182.17/182.14 (~P11(f6(a5),f6(a5),f14(a5))), % 182.17/182.14 inference(scs_inference,[],[3551,3618,1048,2,41])). % 182.17/182.14 cnf(3630,plain, % 182.17/182.14 (P15(f12(a5),a23)), % 182.17/182.14 inference(scs_inference,[],[3551,3598,3618,3604,3507,3523,1048,2,41,68,101])). % 182.17/182.14 cnf(3632,plain, % 182.17/182.14 (~P5(f13(a5),f14(a5))), % 182.17/182.14 inference(scs_inference,[],[3551,3598,3618,3615,3604,3507,3523,1048,2,41,68,101,62])). % 182.17/182.14 cnf(3642,plain, % 182.17/182.14 (~E(a3,a1)), % 182.17/182.14 inference(scs_inference,[],[78,2])). % 182.17/182.14 cnf(3643,plain, % 182.17/182.14 (~P12(x36431,f13(a5),f14(a5))+~E(x36431,f6(a5))), % 182.17/182.14 inference(scs_inference,[],[3584,78,2,44])). % 182.17/182.14 cnf(3656,plain, % 182.17/182.14 (~E(a2,a1)), % 182.17/182.14 inference(scs_inference,[],[76,2])). % 182.17/182.14 cnf(3667,plain, % 182.17/182.14 (~P10(f12(a5),f14(a5))), % 182.17/182.14 inference(scs_inference,[],[3569,1048,51])). % 182.17/182.14 cnf(3673,plain, % 182.17/182.14 (~E(f13(a5),f11(a4,a5))), % 182.17/182.14 inference(scs_inference,[],[3515,332,40])). % 182.17/182.14 cnf(3698,plain, % 182.17/182.14 (~P6(f13(a5),f14(a5))), % 182.17/182.14 inference(scs_inference,[],[3581,3587,1051,837,92])). % 182.17/182.14 cnf(3714,plain, % 182.17/182.14 (~P16(a4,x37141)+P16(f14(a5),x37141)), % 182.17/182.14 inference(scs_inference,[],[1042,59])). % 182.17/182.14 cnf(3724,plain, % 182.17/182.14 (~P12(f12(a5),x37241,x37242)+~E(x37241,f6(a5))), % 182.17/182.14 inference(scs_inference,[],[558,1042,50,45])). % 182.17/182.14 cnf(3740,plain, % 182.17/182.14 (~P16(f14(a5),x37401)+P2(f16(a4,x37401))), % 182.17/182.14 inference(scs_inference,[],[1048,59,107,3714,95,90])). % 182.17/182.14 cnf(3764,plain, % 182.17/182.14 (P15(f6(a5),a1)+~P7(f6(a5))), % 182.17/182.14 inference(scs_inference,[],[3543,101])). % 182.17/182.14 cnf(3774,plain, % 182.17/182.14 (~P11(x37741,a4,x37742)+P11(x37741,f14(a5),x37742)), % 182.17/182.14 inference(scs_inference,[],[1042,40])). % 182.17/182.14 cnf(3784,plain, % 182.17/182.14 (~P14(x37841,a4)+P14(x37841,f14(a5))), % 182.17/182.14 inference(scs_inference,[],[1042,64])). % 182.17/182.14 cnf(3836,plain, % 182.17/182.14 (~P8(f14(a5),x38361)+P8(a4,x38361)), % 182.17/182.14 inference(scs_inference,[],[1048,67])). % 182.17/182.14 cnf(3864,plain, % 182.17/182.14 (~P6(f6(a5),a3)), % 182.17/182.14 inference(scs_inference,[],[3642,3513,103])). % 182.17/182.14 cnf(3879,plain, % 182.17/182.14 (~P11(x38791,f14(a5),x38792)+P11(x38791,a4,x38792)), % 182.17/182.14 inference(scs_inference,[],[1048,40])). % 182.17/182.14 cnf(3909,plain, % 182.17/182.14 (~P8(x39091,a4)+P8(x39091,f14(a5))), % 182.17/182.14 inference(scs_inference,[],[1042,68])). % 182.17/182.14 cnf(3947,plain, % 182.17/182.14 (~P6(f6(a5),a2)), % 182.17/182.14 inference(scs_inference,[],[3656,3513,103])). % 182.17/182.14 cnf(3954,plain, % 182.17/182.14 (~P8(f13(a5),f11(a4,a5))+P11(f11(a4,a5),f6(a5),f14(a5))), % 182.17/182.14 inference(scs_inference,[],[1205,3532,1022,3541,326,847,1039,68,142])). % 182.17/182.14 cnf(3975,plain, % 182.17/182.14 (~P6(x39751,a3)+~E(x39751,f6(a5))), % 182.17/182.14 inference(scs_inference,[],[3864,48])). % 182.17/182.14 cnf(3981,plain, % 182.17/182.14 (~P8(x39811,f14(a5))+P8(x39811,a4)), % 182.17/182.14 inference(scs_inference,[],[1048,68])). % 182.17/182.14 cnf(4005,plain, % 182.17/182.14 (~P6(f6(a5),a23)), % 182.17/182.14 inference(scs_inference,[],[75,3513,103])). % 182.17/182.14 cnf(4010,plain, % 182.17/182.14 (P6(f13(a5),a3)+P6(f13(a5),a2)), % 182.17/182.14 inference(scs_inference,[],[74,3589,3581,3539,3541,75,3513,326,103,142,105])). % 182.17/182.14 cnf(4016,plain, % 182.17/182.14 (E(f11(a4,a5),f6(a5))+P11(f11(a4,a5),f6(a5),f14(a5))), % 182.17/182.14 inference(scs_inference,[],[1205,1022,3541,326,847,1039,142])). % 182.17/182.14 cnf(4038,plain, % 182.17/182.14 (P11(f11(a4,a5),f6(a5),f14(a5))+E(f6(a5),f11(a4,a5))), % 182.17/182.14 inference(scs_inference,[],[1205,1022,3541,326,847,1039,142])). % 182.17/182.14 cnf(4063,plain, % 182.17/182.14 (~P14(x40631,f14(a5))+P14(x40631,a4)), % 182.17/182.14 inference(scs_inference,[],[3526,3565,1205,1022,847,1039,1048,142,64])). % 182.17/182.14 cnf(4068,plain, % 182.17/182.14 (~P8(f13(a5),x40681)+~P11(x40681,f6(a5),x40682)), % 182.17/182.14 inference(scs_inference,[],[3587,838])). % 182.17/182.14 cnf(4077,plain, % 182.17/182.14 (P9(f11(a4,a5),a5)+~P10(f11(a4,a5),f14(a5))), % 182.17/182.14 inference(scs_inference,[],[847,1039,125])). % 182.17/182.14 cnf(4079,plain, % 182.17/182.15 (~P6(x40791,a2)+~E(x40791,f6(a5))), % 182.17/182.15 inference(scs_inference,[],[3947,847,1039,125,48])). % 182.17/182.15 cnf(4106,plain, % 182.17/182.15 (~P6(f13(a5),a3)+~P13(a4,a3)), % 182.17/182.15 inference(scs_inference,[],[3615,72,115])). % 182.17/182.15 cnf(4163,plain, % 182.17/182.15 (~P9(x41631,a5)+~E(x41631,f6(a5))), % 182.17/182.15 inference(scs_inference,[],[3530,57])). % 182.17/182.15 cnf(4178,plain, % 182.17/182.15 (~P12(x41781,x41782,f14(a5))+~E(x41782,f11(a4,a5))), % 182.17/182.15 inference(scs_inference,[],[1207,45])). % 182.17/182.15 cnf(4188,plain, % 182.17/182.15 (~P10(x41881,a4)+~E(x41881,f6(a5))), % 182.17/182.15 inference(scs_inference,[],[3545,50])). % 182.17/182.15 cnf(4189,plain, % 182.17/182.15 (~E(x41891,f11(a4,a5))+~E(a5,x41891)), % 182.17/182.15 inference(scs_inference,[],[1028,3545,50,3])). % 182.17/182.15 cnf(4195,plain, % 182.17/182.15 (E(f11(a4,a5),f6(a5))+P11(f11(a4,a5),f6(a5),a4)), % 182.17/182.15 inference(scs_inference,[],[1022,3541,332,326,847,74,142])). % 182.17/182.15 cnf(4198,plain, % 182.17/182.15 (P11(f11(a4,a5),f6(a5),a4)+~P6(f11(a4,a5),a3)), % 182.17/182.15 inference(scs_inference,[],[1022,3541,332,326,847,74,142,3975])). % 182.17/182.15 cnf(4199,plain, % 182.17/182.15 (P11(f11(a4,a5),f6(a5),a4)+~P6(f11(a4,a5),a2)), % 182.17/182.15 inference(scs_inference,[],[1022,3541,332,326,847,74,142,3975,4079])). % 182.17/182.15 cnf(4200,plain, % 182.17/182.15 (P11(f11(a4,a5),f6(a5),a4)+~P9(f11(a4,a5),a5)), % 182.17/182.15 inference(scs_inference,[],[1022,3541,332,326,847,74,142,3975,4079,4163])). % 182.17/182.15 cnf(4201,plain, % 182.17/182.15 (P11(f11(a4,a5),f6(a5),a4)+~P10(f11(a4,a5),a4)), % 182.17/182.15 inference(scs_inference,[],[1022,3541,332,326,847,74,142,3975,4079,4163,4188])). % 182.17/182.15 cnf(4202,plain, % 182.17/182.15 (P11(f11(a4,a5),f6(a5),a4)+~P12(f11(a4,a5),f13(a5),f14(a5))), % 182.17/182.15 inference(scs_inference,[],[1022,3541,332,326,847,74,142,3975,4079,4163,4188,3643])). % 182.17/182.15 cnf(4206,plain, % 182.17/182.15 (~P12(x42061,x42062,a4)+~E(x42062,f11(a4,a5))), % 182.17/182.15 inference(scs_inference,[],[333,45])). % 182.17/182.15 cnf(4238,plain, % 182.17/182.15 (~E(f6(a5),x42381)+~P11(x42381,f6(a5),f14(a5))), % 182.17/182.15 inference(scs_inference,[],[3628,39,2])). % 182.17/182.15 cnf(4288,plain, % 182.17/182.15 (E(f6(a5),f11(a4,a5))+P11(f11(a4,a5),f6(a5),a4)), % 182.17/182.15 inference(scs_inference,[],[3541,1022,332,326,847,74,142])). % 182.17/182.15 cnf(4292,plain, % 182.17/182.15 (P11(f11(a4,a5),f6(a5),a4)+P11(f11(a4,a5),f12(a5),a4)), % 182.17/182.15 inference(scs_inference,[],[3541,1022,332,326,847,74,142,4206,909])). % 182.17/182.15 cnf(4293,plain, % 182.17/182.15 (P11(f11(a4,a5),f6(a5),a4)+P11(f11(a4,a5),f12(a5),f14(a5))), % 182.17/182.15 inference(scs_inference,[],[3541,1022,332,326,847,74,142,4206,909,1209])). % 182.17/182.15 cnf(4294,plain, % 182.17/182.15 (P11(f11(a4,a5),f6(a5),a4)+~P11(f11(a4,a5),f6(a5),f14(a5))), % 182.17/182.15 inference(scs_inference,[],[3541,1022,332,326,847,74,142,4206,909,1209,4238])). % 182.17/182.15 cnf(4295,plain, % 182.17/182.15 (P11(f11(a4,a5),f6(a5),a4)+P14(f11(a4,a5),f12(a5))), % 182.17/182.15 inference(scs_inference,[],[3541,1022,332,326,847,74,142,4206,909,1209,4238,130])). % 182.17/182.15 cnf(4297,plain, % 182.17/182.15 (P11(f11(a4,a5),f6(a5),a4)+~P10(f11(a4,a5),f14(a5))), % 182.17/182.15 inference(scs_inference,[],[3541,1022,332,326,847,74,142,4206,909,1209,4238,130,132])). % 182.17/182.15 cnf(4303,plain, % 182.17/182.15 (P11(f11(a4,a5),f6(a5),a4)+~P8(f12(a5),f11(a4,a5))), % 182.17/182.15 inference(scs_inference,[],[3541,1022,332,326,847,74,142,4206,909,1209,4238,130,132,358,377,285])). % 182.17/182.15 cnf(4336,plain, % 182.17/182.15 (~E(x43361,f11(a4,a5))+~E(f13(a5),x43361)), % 182.17/182.15 inference(scs_inference,[],[3673,3])). % 182.17/182.15 cnf(4337,plain, % 182.17/182.15 (~E(x43371,f13(a5))+~E(x43371,f11(a4,a5))), % 182.17/182.15 inference(scs_inference,[],[3673,3,2])). % 182.17/182.15 cnf(4372,plain, % 182.17/182.15 (~E(x43721,f12(a5))+~E(f11(a4,a5),x43721)), % 182.17/182.15 inference(scs_inference,[],[3565,3])). % 182.17/182.15 cnf(4381,plain, % 182.17/182.15 (~E(x43811,f12(a5))+~E(x43811,f6(a5))), % 182.17/182.15 inference(scs_inference,[],[3563,3,2])). % 182.17/182.15 cnf(4397,plain, % 182.17/182.15 (~E(x43971,f11(a4,a5))+~E(f12(a5),x43971)), % 182.17/182.15 inference(scs_inference,[],[894,3])). % 182.17/182.15 cnf(4398,plain, % 182.17/182.15 (~E(x43981,f12(a5))+~E(x43981,f11(a4,a5))), % 182.17/182.15 inference(scs_inference,[],[894,3,2])). % 182.17/182.15 cnf(4451,plain, % 182.17/182.15 (~P14(f14(a5),x44511)+P8(a4,x44511)), % 182.17/182.15 inference(scs_inference,[],[3836,94])). % 182.17/182.15 cnf(4453,plain, % 182.17/182.15 (~P8(f14(a5),x44531)+~P8(x44531,a4)), % 182.17/182.15 inference(scs_inference,[],[3909,102])). % 182.17/182.15 cnf(4477,plain, % 182.17/182.15 (~P11(x44771,f14(a5),x44772)+P14(x44771,a4)), % 182.17/182.15 inference(scs_inference,[],[4063,130])). % 182.17/182.15 cnf(4494,plain, % 182.17/182.15 (~P13(a4,a3)+P6(f13(a5),a2)), % 182.17/182.15 inference(scs_inference,[],[4106,4010])). % 182.17/182.15 cnf(4537,plain, % 182.17/182.15 (~P8(f14(a5),a4)), % 182.17/182.15 inference(scs_inference,[],[4453,3909])). % 182.17/182.15 cnf(4538,plain, % 182.17/182.15 (~P8(a4,a4)), % 182.17/182.15 inference(scs_inference,[],[4537,1042,67])). % 182.17/182.15 cnf(4545,plain, % 182.17/182.15 (~P14(a4,f14(a5))), % 182.17/182.15 inference(scs_inference,[],[4537,1042,1048,67,68,3981,4451,64,63,4063])). % 182.17/182.15 cnf(4548,plain, % 182.17/182.15 (~P11(f14(a5),a4,x45481)), % 182.17/182.15 inference(scs_inference,[],[4537,1042,1048,67,68,3981,4451,64,63,4063,4477,40])). % 182.17/182.15 cnf(4551,plain, % 182.17/182.15 (~P11(a4,f14(a5),x45511)), % 182.17/182.15 inference(scs_inference,[],[4537,1042,1048,67,68,3981,4451,64,63,4063,4477,40,106,39])). % 182.17/182.15 cnf(4555,plain, % 182.17/182.15 (~P11(a4,a4,x45551)), % 182.17/182.15 inference(scs_inference,[],[4551,3774])). % 182.17/182.15 cnf(4567,plain, % 182.17/182.15 (~P11(a4,x45671,a4)+~P11(x45671,f14(a5),f14(a5))), % 182.17/182.15 inference(scs_inference,[],[4551,1042,150,41])). % 182.17/182.15 cnf(4618,plain, % 182.17/182.15 (~P14(x46181,f6(a5))+~P14(f13(a5),x46181)), % 182.17/182.15 inference(scs_inference,[],[3606,94])). % 182.17/182.15 cnf(4635,plain, % 182.17/182.15 (~E(f16(a4,x46351),x46352)+P2(x46352)+~P16(f14(a5),x46351)), % 182.17/182.15 inference(scs_inference,[],[3740,47])). % 182.17/182.15 cnf(4678,plain, % 182.17/182.15 (~E(a5,f11(f14(a5),a5))), % 182.17/182.15 inference(scs_inference,[],[1048,4189,32])). % 182.17/182.15 cnf(4696,plain, % 182.17/182.15 (~E(x46961,a5)+~E(f6(x46961),f12(a5))), % 182.17/182.15 inference(scs_inference,[],[4381,8])). % 182.17/182.15 cnf(4739,plain, % 182.17/182.15 (~P11(f13(a5),x47391,x47392)+~P14(x47391,f6(a5))), % 182.17/182.15 inference(scs_inference,[],[4618,130])). % 182.17/182.15 cnf(4759,plain, % 182.17/182.15 (~E(f12(a5),f6(x47591))+~E(x47591,a5)), % 182.17/182.15 inference(scs_inference,[],[4696,2])). % 182.17/182.15 cnf(4778,plain, % 182.17/182.15 (~E(x47781,f6(x47782))+~E(f12(a5),x47781)+~E(x47782,a5)), % 182.17/182.15 inference(scs_inference,[],[4759,3])). % 182.17/182.15 cnf(4894,plain, % 182.17/182.15 (~P8(f13(a5),f11(a4,a5))), % 182.17/182.15 inference(scs_inference,[],[4068,3954])). % 182.17/182.15 cnf(4903,plain, % 182.17/182.15 (~P8(f13(a5),x49031)+~E(x49031,f11(a4,a5))), % 182.17/182.15 inference(scs_inference,[],[4894,67,68])). % 182.17/182.15 cnf(4913,plain, % 182.17/182.15 (~E(f11(f14(a5),a5),f13(a5))), % 182.17/182.15 inference(scs_inference,[],[1048,4337,32])). % 182.17/182.15 cnf(4921,plain, % 182.17/182.15 (~E(f11(f14(a5),a5),f12(a5))), % 182.17/182.15 inference(scs_inference,[],[1042,4372,32])). % 182.17/182.15 cnf(4989,plain, % 182.17/182.15 (~P14(f14(a5),f6(a5))+~P11(f13(a5),a4,x49891)), % 182.17/182.15 inference(scs_inference,[],[4739,3774])). % 182.17/182.15 cnf(5137,plain, % 182.17/182.15 (~P12(x51371,f14(a5),f14(a5))+~P11(a4,x51371,a4)), % 182.17/182.15 inference(scs_inference,[],[4567,138])). % 182.17/182.15 cnf(5175,plain, % 182.17/182.15 (~P14(f14(a5),x51751)+~E(x51751,f6(a5))+~P11(f13(a5),a4,x51752)), % 182.17/182.15 inference(scs_inference,[],[4989,64])). % 182.17/182.15 cnf(5237,plain, % 182.17/182.15 (~P11(f14(a5),x52371,a4)+~P12(x52371,f14(a5),f14(a5))), % 182.17/182.15 inference(scs_inference,[],[1048,5137,39])). % 182.17/182.15 cnf(5355,plain, % 182.17/182.15 (P9(f11(a4,a5),a5)+P11(f11(a4,a5),f19(f11(a4,a5),f14(a5)),f14(a5))), % 182.17/182.15 inference(scs_inference,[],[1203,4077,133])). % 182.17/182.15 cnf(5395,plain, % 182.17/182.15 (~P12(x53951,f14(a5),a4)+~P11(f14(a5),x53951,a4)), % 182.17/182.15 inference(scs_inference,[],[1042,5237,46])). % 182.17/182.15 cnf(5396,plain, % 182.17/182.15 (~P12(f14(a5),x53961,a4)+~P12(x53961,f14(a5),a4)), % 182.17/182.15 inference(scs_inference,[],[5395,138])). % 182.17/182.15 cnf(5397,plain, % 182.17/182.15 (~P12(x53971,f14(a5),f14(a5))+~P12(f14(a5),x53971,a4)), % 182.17/182.15 inference(scs_inference,[],[1048,5396,46])). % 182.17/182.15 cnf(5484,plain, % 182.17/182.15 (~P12(f14(a5),x54841,f14(a5))+~P12(x54841,f14(a5),f14(a5))), % 182.17/182.15 inference(scs_inference,[],[1048,5397,46])). % 182.17/182.15 cnf(5588,plain, % 182.17/182.15 (P11(f11(a4,a5),f6(a5),a4)+P11(f11(a4,a5),f19(f11(a4,a5),a4),a4)), % 182.17/182.15 inference(scs_inference,[],[813,4201,133])). % 182.17/182.15 cnf(5623,plain, % 182.17/182.15 (~P12(x56231,a4,f14(a5))+~P12(f14(a5),x56231,f14(a5))), % 182.17/182.15 inference(scs_inference,[],[1042,5484,45])). % 182.17/182.15 cnf(5627,plain, % 182.17/182.15 (~P12(f14(a5),a4,f14(a5))), % 182.17/182.15 inference(scs_inference,[],[1042,5623,45])). % 182.17/182.15 cnf(5628,plain, % 182.17/182.15 (~P12(a4,a4,f14(a5))), % 182.17/182.15 inference(scs_inference,[],[5627,1042,44])). % 182.17/182.15 cnf(5629,plain, % 182.17/182.15 (~P12(f14(a5),a4,a4)), % 182.17/182.15 inference(scs_inference,[],[5627,1042,44,46])). % 182.17/182.15 cnf(5630,plain, % 182.17/182.15 (~P12(f14(a5),f14(a5),f14(a5))), % 182.17/182.15 inference(scs_inference,[],[5627,1042,1048,44,46,45])). % 182.17/182.15 cnf(5634,plain, % 182.17/182.15 (~P12(a4,a4,a4)), % 182.17/182.15 inference(scs_inference,[],[5628,5630,1042,44,46])). % 182.17/182.15 cnf(5635,plain, % 182.17/182.15 (~P12(f14(a5),f14(a5),a4)), % 182.17/182.15 inference(scs_inference,[],[5628,5630,5629,1042,1048,44,46,45])). % 182.17/182.15 cnf(5636,plain, % 182.17/182.15 (~P12(a4,f14(a5),a4)), % 182.17/182.15 inference(scs_inference,[],[5635,1042,44])). % 182.17/182.15 cnf(5641,plain, % 182.17/182.15 (P5(f11(a4,a5),f7(f7(a4,f11(a4,a5)),f11(a4,a5)))), % 182.17/182.15 inference(scs_inference,[],[1032,112])). % 182.17/182.15 cnf(5643,plain, % 182.17/182.15 (P13(f7(f7(a4,f11(a4,a5)),f11(a4,a5)),f7(a4,f11(a4,a5)))), % 182.17/182.15 inference(scs_inference,[],[1032,112,114])). % 182.17/182.15 cnf(5652,plain, % 182.17/182.15 (P6(f11(a4,a5),f15(f11(a4,a5),f7(f7(a4,f11(a4,a5)),f11(a4,a5))))), % 182.17/182.15 inference(scs_inference,[],[2480,1032,3630,112,114,721,8,9,15,331,514])). % 182.17/182.15 cnf(5674,plain, % 182.17/182.15 (E(f17(f12(f16(f6(a5),a5)),x56741,x56742),f17(f12(a4),x56741,x56742))), % 182.17/182.15 inference(scs_inference,[],[2480,1032,3630,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5])). % 182.17/182.15 cnf(5675,plain, % 182.17/182.15 (E(f17(x56751,f12(f16(f6(a5),a5)),x56752),f17(x56751,f12(a4),x56752))), % 182.17/182.15 inference(scs_inference,[],[2480,1032,3630,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6])). % 182.17/182.15 cnf(5686,plain, % 182.17/182.15 (P6(f6(f22(a4,f12(a5),f13(a5))),a1)), % 182.17/182.15 inference(scs_inference,[],[2480,1032,3630,3515,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300])). % 182.17/182.15 cnf(5693,plain, % 182.17/182.15 (P11(f12(f22(a4,f6(a5),f12(a5))),f13(f22(a4,f6(a5),f12(a5))),a4)), % 182.17/182.15 inference(scs_inference,[],[2480,1032,1068,3630,1202,891,3515,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612])). % 182.17/182.15 cnf(5697,plain, % 182.17/182.15 (P6(f22(a4,f6(a5),f12(a5)),f14(f22(a4,f6(a5),f12(a5))))), % 182.17/182.15 inference(scs_inference,[],[2480,685,1032,1068,3630,1202,891,3515,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238])). % 182.17/182.15 cnf(5699,plain, % 182.17/182.15 (P17(f12(a5),f22(f14(a5),f6(a5),f12(a5)))), % 182.17/182.15 inference(scs_inference,[],[2480,685,1032,1068,3630,1202,891,3515,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143])). % 182.17/182.15 cnf(5701,plain, % 182.17/182.15 (P13(f10(f14(a5),f6(a5),f12(a5)),f14(a5))), % 182.17/182.15 inference(scs_inference,[],[2480,685,1032,1068,3630,1202,891,3515,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149])). % 182.17/182.15 cnf(5705,plain, % 182.17/182.15 (P5(f12(a5),f10(f14(a5),f6(a5),f12(a5)))), % 182.17/182.15 inference(scs_inference,[],[2480,3598,685,1032,1068,3630,1202,891,3515,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146])). % 182.17/182.15 cnf(5707,plain, % 182.17/182.15 (P13(f9(f14(a5),f6(a5),f12(a5)),f14(a5))), % 182.17/182.15 inference(scs_inference,[],[2480,3598,685,1032,1068,3630,1202,891,3515,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148])). % 182.17/182.15 cnf(5709,plain, % 182.17/182.15 (P6(f12(a5),f15(f12(a5),a23))), % 182.17/182.15 inference(scs_inference,[],[2480,3598,685,1032,1068,3630,1202,891,3515,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109])). % 182.17/182.15 cnf(5711,plain, % 182.17/182.15 (P5(f6(a5),f9(f14(a5),f6(a5),f12(a5)))), % 182.17/182.15 inference(scs_inference,[],[2480,3598,685,1032,1068,3630,1202,891,3515,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145])). % 182.17/182.15 cnf(5713,plain, % 182.17/182.15 (P6(f22(f16(f6(a5),a5),f6(a5),f12(a5)),f14(f22(f16(f6(a5),a5),f6(a5),f12(a5))))), % 182.17/182.15 inference(scs_inference,[],[1698,2480,3598,685,1032,1068,3630,1202,891,3515,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91])). % 182.17/182.15 cnf(5715,plain, % 182.17/182.15 (P6(f22(f14(a5),f6(a5),f12(a5)),f14(a5))), % 182.17/182.15 inference(scs_inference,[],[1698,2480,3598,685,1032,1068,3630,1202,891,3515,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147])). % 182.17/182.15 cnf(5719,plain, % 182.17/182.15 (P17(f6(a5),f22(f14(a5),f6(a5),f12(a5)))), % 182.17/182.15 inference(scs_inference,[],[1698,2480,3598,685,1032,1068,3630,1202,891,3515,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144])). % 182.17/182.15 cnf(5721,plain, % 182.17/182.15 (P6(a5,f16(f11(a4,a5),a5))), % 182.17/182.15 inference(scs_inference,[],[1698,2480,3598,685,1032,1068,3630,1202,891,3547,3515,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144,107])). % 182.17/182.15 cnf(5725,plain, % 182.17/182.15 (~P15(f12(a5),f16(f6(a5),a5))), % 182.17/182.15 inference(scs_inference,[],[1698,2480,3598,685,1032,1068,3630,1202,891,3547,890,3515,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144,107,83,131])). % 182.17/182.15 cnf(5734,plain, % 182.17/182.15 (P4(f22(a4,f6(a5),f12(a5)))), % 182.17/182.15 inference(scs_inference,[],[4678,1698,2480,3598,685,1032,1068,3630,1202,891,3547,890,3515,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144,107,83,131,130,2,90,85,88])). % 182.17/182.15 cnf(5736,plain, % 182.17/182.15 (P15(f11(a4,a5),f16(f11(a4,a5),a5))), % 182.17/182.15 inference(scs_inference,[],[4678,1698,2480,3598,685,1032,1068,3630,1202,891,3547,890,3515,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144,107,83,131,130,2,90,85,88,110])). % 182.17/182.15 cnf(5744,plain, % 182.17/182.15 (P4(f6(f22(a4,f12(a5),f13(a5))))), % 182.17/182.15 inference(scs_inference,[],[4678,1698,2480,3598,685,1032,1068,3630,1202,891,3547,890,3515,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144,107,83,131,130,2,90,85,88,110,132,358,377,87])). % 182.17/182.15 cnf(5753,plain, % 182.17/182.15 (~P10(f12(a5),f16(f6(a5),a5))), % 182.17/182.15 inference(scs_inference,[],[1066,4678,3562,1698,2480,3598,685,3569,1032,1068,3630,1202,891,3547,890,3515,399,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144,107,83,131,130,2,90,85,88,110,132,358,377,87,82,285,84,3,51])). % 182.17/182.15 cnf(5754,plain, % 182.17/182.15 (P15(f11(f16(f6(a5),a5),a5),f16(f6(a5),a5))), % 182.17/182.15 inference(scs_inference,[],[1066,4678,3562,1698,2480,3598,685,3569,1032,1068,400,3630,1202,891,386,3547,890,3515,399,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144,107,83,131,130,2,90,85,88,110,132,358,377,87,82,285,84,3,51,120])). % 182.17/182.15 cnf(5758,plain, % 182.17/182.15 (P11(f12(a5),f19(f12(a5),f14(a5)),f14(a5))), % 182.17/182.15 inference(scs_inference,[],[1066,4678,3562,1698,2480,759,2757,3598,685,3569,3667,1032,1068,400,3630,1202,891,386,3547,890,3515,399,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144,107,83,131,130,2,90,85,88,110,132,358,377,87,82,285,84,3,51,120,103,141])). % 182.17/182.15 cnf(5760,plain, % 182.17/182.15 (~E(f14(f6(a5)),f14(a5))), % 182.23/182.15 inference(scs_inference,[],[1066,3561,4678,3562,1698,2480,759,2757,3598,685,3569,3667,1032,1068,400,3630,1202,1051,891,386,3547,890,3515,399,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144,107,83,131,130,2,90,85,88,110,132,358,377,87,82,285,84,3,51,120,103,141,38])). % 182.23/182.15 cnf(5762,plain, % 182.23/182.15 (E(f11(f16(f6(a5),a5),x57621),f11(a4,x57621))), % 182.23/182.15 inference(rename_variables,[],[2503])). % 182.23/182.15 cnf(5766,plain, % 182.23/182.15 (~P16(f12(a5),f22(f14(a5),f6(a5),f12(a5)))), % 182.23/182.15 inference(scs_inference,[],[1066,3561,4678,3562,1698,2480,2503,759,1033,4538,2757,3598,685,3569,3667,1032,1068,400,3630,1202,1051,891,386,3547,890,3515,399,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144,107,83,131,130,2,90,85,88,110,132,358,377,87,82,285,84,3,51,120,103,141,38,40,121,67,136])). % 182.23/182.15 cnf(5769,plain, % 182.23/182.15 (~P14(a4,f16(f6(a5),a5))), % 182.23/182.15 inference(scs_inference,[],[1066,3561,4678,3562,1698,2480,2503,759,1033,3596,4538,2757,4545,3598,685,3569,3667,1032,1068,400,1052,3630,1202,1051,891,386,3547,890,3515,399,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144,107,83,131,130,2,90,85,88,110,132,358,377,87,82,285,84,3,51,120,103,141,38,40,121,67,136,49,64])). % 182.23/182.15 cnf(5770,plain, % 182.23/182.15 (~P6(f11(f16(f6(a5),a5),a5),f16(f6(a5),a5))), % 182.23/182.15 inference(scs_inference,[],[1026,1066,3561,4678,3562,1698,2480,2503,5762,759,1033,3596,4538,2757,4545,3598,685,3569,3667,1032,1068,400,1052,3630,1202,1051,891,386,3547,890,3515,399,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144,107,83,131,130,2,90,85,88,110,132,358,377,87,82,285,84,3,51,120,103,141,38,40,121,67,136,49,64,48])). % 182.23/182.15 cnf(5771,plain, % 182.23/182.15 (E(f11(f16(f6(a5),a5),x57711),f11(a4,x57711))), % 182.23/182.15 inference(rename_variables,[],[2503])). % 182.23/182.15 cnf(5772,plain, % 182.23/182.15 (~P11(x57721,f11(a4,a5),f7(f16(f6(a5),a5),f11(a4,a5)))), % 182.23/182.15 inference(scs_inference,[],[1026,1066,3561,4678,3562,1698,2480,2501,2503,5762,759,1033,3596,4538,2757,4545,3598,685,3569,3667,1032,1068,400,1052,3630,1202,1051,891,386,3547,890,3515,399,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144,107,83,131,130,2,90,85,88,110,132,358,377,87,82,285,84,3,51,120,103,141,38,40,121,67,136,49,64,48,41])). % 182.23/182.15 cnf(5774,plain, % 182.23/182.15 (~P14(f16(f6(a5),a5),f14(a5))), % 182.23/182.15 inference(scs_inference,[],[1026,1066,3561,4678,3562,1698,2480,2501,2503,5762,759,1033,3596,4538,2757,4545,3598,685,3569,3667,1032,1068,400,1052,3630,1202,1051,891,386,3547,890,3515,399,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144,107,83,131,130,2,90,85,88,110,132,358,377,87,82,285,84,3,51,120,103,141,38,40,121,67,136,49,64,48,41,63])). % 182.23/182.15 cnf(5775,plain, % 182.23/182.15 (~P8(f13(a5),f11(f16(f6(a5),a5),a5))), % 182.23/182.15 inference(scs_inference,[],[1026,1066,3561,4678,3562,1698,2480,2501,2503,5762,5771,759,1033,3596,4538,2757,4545,3598,685,3569,3667,1032,1068,4894,400,1052,3630,1202,1051,891,386,3547,890,3515,399,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144,107,83,131,130,2,90,85,88,110,132,358,377,87,82,285,84,3,51,120,103,141,38,40,121,67,136,49,64,48,41,63,68])). % 182.23/182.15 cnf(5776,plain, % 182.23/182.15 (E(f11(f16(f6(a5),a5),x57761),f11(a4,x57761))), % 182.23/182.15 inference(rename_variables,[],[2503])). % 182.23/182.15 cnf(5784,plain, % 182.23/182.15 (P1(f14(f11(a4,a5)))), % 182.23/182.15 inference(scs_inference,[],[5634,1026,1066,3561,4678,3562,1698,2480,2501,2503,5762,5771,759,1033,3596,159,4538,4555,2757,4545,3598,685,3569,3667,1032,1068,4894,400,1052,3630,1202,1051,891,386,3547,890,1022,3515,399,1719,74,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144,107,83,131,130,2,90,85,88,110,132,358,377,87,82,285,84,3,51,120,103,141,38,40,121,67,136,49,64,48,41,63,68,46,44,45,137,39,53,92])). % 182.23/182.15 cnf(5786,plain, % 182.23/182.15 (~P5(f13(a5),f16(f6(a5),a5))), % 182.23/182.15 inference(scs_inference,[],[5634,1026,1066,3561,4678,3562,1698,2480,2501,2503,5762,5771,759,1033,3596,159,4538,4555,2757,4545,3598,685,3569,3667,1032,1068,3632,4894,400,1052,3630,1202,1051,891,386,3547,890,1022,3515,399,1719,74,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144,107,83,131,130,2,90,85,88,110,132,358,377,87,82,285,84,3,51,120,103,141,38,40,121,67,136,49,64,48,41,63,68,46,44,45,137,39,53,92,62])). % 182.23/182.15 cnf(5787,plain, % 182.23/182.15 (P15(f13(a5),f10(a4,f12(a5),f13(a5)))), % 182.23/182.15 inference(scs_inference,[],[5634,1026,1066,3561,4678,3562,1698,2480,2501,2503,5762,5771,759,1033,3596,159,4538,4555,2757,4545,3598,3579,685,3569,3667,1032,1068,3632,4894,400,1052,3630,1202,1051,891,692,386,3547,890,1022,3515,399,1719,74,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144,107,83,131,130,2,90,85,88,110,132,358,377,87,82,285,84,3,51,120,103,141,38,40,121,67,136,49,64,48,41,63,68,46,44,45,137,39,53,92,62,101])). % 182.23/182.15 cnf(5789,plain, % 182.23/182.15 (P3(f6(f22(a4,f6(a5),f12(a5))))), % 182.23/182.15 inference(scs_inference,[],[5634,1026,1066,3561,4678,3562,1698,2480,2501,2503,5762,5771,759,1033,3596,159,4538,4555,2757,4545,3598,3579,685,3569,3667,1032,1068,3632,4894,400,1052,69,3630,1202,1051,891,692,386,3547,890,1022,3515,399,1719,74,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144,107,83,131,130,2,90,85,88,110,132,358,377,87,82,285,84,3,51,120,103,141,38,40,121,67,136,49,64,48,41,63,68,46,44,45,137,39,53,92,62,101,93])). % 182.23/182.15 cnf(5791,plain, % 182.23/182.15 (~P11(f6(a5),f11(f14(a5),a5),a4)), % 182.23/182.15 inference(scs_inference,[],[5634,4913,4921,1026,1066,3561,4678,3562,1698,2480,2501,2503,5762,5771,759,1033,3596,159,4538,4555,2757,4545,3598,3579,685,3569,3667,1032,1068,3632,4894,400,1052,69,3630,1202,1051,891,692,386,3547,890,1022,3515,399,1719,74,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144,107,83,131,130,2,90,85,88,110,132,358,377,87,82,285,84,3,51,120,103,141,38,40,121,67,136,49,64,48,41,63,68,46,44,45,137,39,53,92,62,101,93,135])). % 182.23/182.15 cnf(5793,plain, % 182.23/182.15 (P5(f6(a5),f14(f6(a5)))), % 182.23/182.15 inference(scs_inference,[],[5634,4913,4921,1026,1066,3561,4678,3562,1698,2480,2501,2503,5762,5771,759,1033,3596,159,4538,4555,2757,4545,3598,3579,685,3569,3667,1032,1068,3632,4894,400,1052,69,3630,1202,1051,891,692,386,3547,890,1022,3515,399,1719,74,2526,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144,107,83,131,130,2,90,85,88,110,132,358,377,87,82,285,84,3,51,120,103,141,38,40,121,67,136,49,64,48,41,63,68,46,44,45,137,39,53,92,62,101,93,135,115])). % 182.23/182.15 cnf(5795,plain, % 182.23/182.15 (P16(f11(f16(f6(a5),a5),a5),a5)), % 182.23/182.15 inference(scs_inference,[],[5634,4913,4921,1026,1066,3561,4678,3562,1698,2480,2501,2503,5762,5771,759,1033,3596,159,4538,4555,2757,4545,3598,3579,685,3569,3667,1032,1068,3632,4894,400,1052,69,3630,1202,1051,891,692,386,3547,890,1022,3515,399,1719,74,2526,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144,107,83,131,130,2,90,85,88,110,132,358,377,87,82,285,84,3,51,120,103,141,38,40,121,67,136,49,64,48,41,63,68,46,44,45,137,39,53,92,62,101,93,135,115,124])). % 182.23/182.15 cnf(5800,plain, % 182.23/182.15 (E(f11(f16(f6(a5),a5),x58001),f11(a4,x58001))), % 182.23/182.15 inference(rename_variables,[],[2503])). % 182.23/182.15 cnf(5802,plain, % 182.23/182.15 (~E(f14(f6(a5)),a23)), % 182.23/182.15 inference(scs_inference,[],[5634,4913,4921,1026,1066,3561,4678,3562,1698,2480,2501,2503,5762,5771,5776,759,4005,1033,3596,159,4538,4555,2757,4545,3598,3579,685,3569,3667,1032,1068,3632,4894,400,1052,69,3630,1202,1051,891,692,386,3547,890,1022,3515,399,1719,74,2526,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144,107,83,131,130,2,90,85,88,110,132,358,377,87,82,285,84,3,51,120,103,141,38,40,121,67,136,49,64,48,41,63,68,46,44,45,137,39,53,92,62,101,93,135,115,124,239,4189,388,2527])). % 182.23/182.15 cnf(5804,plain, % 182.23/182.15 (E(f11(f16(f6(a5),a5),x58041),f11(a4,x58041))), % 182.23/182.15 inference(rename_variables,[],[2503])). % 182.23/182.15 cnf(5805,plain, % 182.23/182.15 (~E(f11(f16(f6(a5),a5),a5),f13(a5))), % 182.23/182.15 inference(scs_inference,[],[5634,4913,4921,1026,1066,3561,4678,3562,1698,2480,2501,2503,5762,5771,5776,5800,5804,759,4005,1033,3596,159,4538,4555,2757,4545,3598,3579,685,3569,3667,1032,1068,3632,4894,400,1052,69,3630,1202,1051,891,692,386,3547,890,1022,3515,399,1719,74,2526,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144,107,83,131,130,2,90,85,88,110,132,358,377,87,82,285,84,3,51,120,103,141,38,40,121,67,136,49,64,48,41,63,68,46,44,45,137,39,53,92,62,101,93,135,115,124,239,4189,388,2527,4336,4337])). % 182.23/182.15 cnf(5806,plain, % 182.23/182.15 (E(f11(f16(f6(a5),a5),x58061),f11(a4,x58061))), % 182.23/182.15 inference(rename_variables,[],[2503])). % 182.23/182.15 cnf(5808,plain, % 182.23/182.15 (E(f11(f16(f6(a5),a5),x58081),f11(a4,x58081))), % 182.23/182.15 inference(rename_variables,[],[2503])). % 182.23/182.15 cnf(5809,plain, % 182.23/182.15 (~E(f11(f16(f6(a5),a5),a5),f12(a5))), % 182.23/182.15 inference(scs_inference,[],[5634,4913,4921,1026,1066,3561,4678,3562,1698,2480,2501,2503,5762,5771,5776,5800,5804,5806,5808,759,4005,1033,3596,159,4538,4555,2757,4545,3598,3579,685,3569,3667,1032,1068,3632,4894,400,1052,69,3630,1202,1051,891,692,386,3547,890,1022,3515,399,1719,74,2526,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144,107,83,131,130,2,90,85,88,110,132,358,377,87,82,285,84,3,51,120,103,141,38,40,121,67,136,49,64,48,41,63,68,46,44,45,137,39,53,92,62,101,93,135,115,124,239,4189,388,2527,4336,4337,4397,4398])). % 182.23/182.15 cnf(5810,plain, % 182.23/182.15 (E(f11(f16(f6(a5),a5),x58101),f11(a4,x58101))), % 182.23/182.15 inference(rename_variables,[],[2503])). % 182.23/182.15 cnf(5812,plain, % 182.23/182.15 (E(f11(f16(f6(a5),a5),x58121),f11(a4,x58121))), % 182.23/182.15 inference(rename_variables,[],[2503])). % 182.23/182.15 cnf(5821,plain, % 182.23/182.15 (P7(f11(f16(f6(a5),a5),a5))), % 182.23/182.15 inference(scs_inference,[],[5634,4913,4921,1026,1066,3561,4678,3562,1698,2480,2501,2503,5762,5771,5776,5800,5804,5806,5808,5810,5812,759,4005,1033,3596,159,4538,4555,2757,4545,3598,3579,685,3569,3667,1032,1068,3632,4894,400,1052,69,3630,1202,1051,891,692,386,3547,890,1022,3515,399,1719,74,2526,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144,107,83,131,130,2,90,85,88,110,132,358,377,87,82,285,84,3,51,120,103,141,38,40,121,67,136,49,64,48,41,63,68,46,44,45,137,39,53,92,62,101,93,135,115,124,239,4189,388,2527,4336,4337,4397,4398,4178,3784,4206,719,94,3879,86])). % 182.23/182.15 cnf(5826,plain, % 182.23/182.15 (P13(f9(a4,f6(a5),f12(a5)),f15(f6(a5),f9(f16(f6(a5),a5),f6(a5),f12(a5))))), % 182.23/182.15 inference(scs_inference,[],[5634,4913,4921,1026,1066,3561,4678,3562,1698,2480,2496,2491,2501,2503,5762,5771,5776,5800,5804,5806,5808,5810,5812,759,4005,1033,3596,159,4538,4555,2757,4545,3598,3579,685,3569,3667,1032,1068,3632,4894,400,1052,69,3630,1202,1051,891,692,386,3547,890,1022,3515,399,1719,74,2526,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144,107,83,131,130,2,90,85,88,110,132,358,377,87,82,285,84,3,51,120,103,141,38,40,121,67,136,49,64,48,41,63,68,46,44,45,137,39,53,92,62,101,93,135,115,124,239,4189,388,2527,4336,4337,4397,4398,4178,3784,4206,719,94,3879,86,4635,804])). % 182.23/182.15 cnf(5829,plain, % 182.23/182.15 (~P12(f6(a5),f19(f12(a5),f14(a5)),f14(a5))), % 182.23/182.15 inference(scs_inference,[],[5634,4913,4921,1026,1066,3561,4678,3562,1698,2480,2496,2491,2501,2503,5762,5771,5776,5800,5804,5806,5808,5810,5812,759,4005,1033,3596,159,4538,4555,2757,4545,3598,3579,685,3569,3667,1032,1068,3632,4894,400,1052,69,3630,1202,1051,891,692,386,3547,890,1022,3515,399,1719,74,2526,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144,107,83,131,130,2,90,85,88,110,132,358,377,87,82,285,84,3,51,120,103,141,38,40,121,67,136,49,64,48,41,63,68,46,44,45,137,39,53,92,62,101,93,135,115,124,239,4189,388,2527,4336,4337,4397,4398,4178,3784,4206,719,94,3879,86,4635,804,151])). % 182.23/182.15 cnf(5832,plain, % 182.23/182.15 (~P8(f16(f6(a5),a5),f14(a5))), % 182.23/182.15 inference(scs_inference,[],[5634,4913,4921,1026,1066,3561,4678,3562,1698,2480,2496,2491,2501,2503,5762,5771,5776,5800,5804,5806,5808,5810,5812,759,4005,1033,3596,159,4538,4555,2757,4545,3598,3617,3579,685,3569,3667,1032,1068,3632,4894,400,1052,69,3630,1202,1051,891,692,386,3547,890,1022,3515,399,1719,74,2526,112,114,721,8,9,15,331,514,13,14,19,20,21,22,23,24,28,29,30,31,32,33,34,35,36,37,613,5,6,7,10,11,12,16,17,18,25,26,27,300,380,382,384,515,612,378,4,238,143,149,113,146,148,109,145,91,147,104,144,107,83,131,130,2,90,85,88,110,132,358,377,87,82,285,84,3,51,120,103,141,38,40,121,67,136,49,64,48,41,63,68,46,44,45,137,39,53,92,62,101,93,135,115,124,239,4189,388,2527,4336,4337,4397,4398,4178,3784,4206,719,94,3879,86,4635,804,151,55,3981])). % 182.23/182.15 cnf(5846,plain, % 182.23/182.15 (P6(f11(a4,a5),f15(f11(a4,a5),f7(f16(f11(a4,a5),a5),f11(a4,a5))))), % 182.23/182.15 inference(scs_inference,[],[5736,5787,613,721,514])). % 182.23/182.15 cnf(5848,plain, % 182.23/182.15 (P11(f12(f22(a4,f12(a5),f13(a5))),f13(f22(a4,f12(a5),f13(a5))),a4)), % 182.23/182.15 inference(scs_inference,[],[5736,5787,3515,613,721,514,612])). % 182.23/182.15 cnf(5852,plain, % 182.23/182.15 (E(f7(x58521,f13(f16(f6(a5),a5))),f7(x58521,f13(a4)))), % 182.23/182.15 inference(scs_inference,[],[5736,5787,2486,3515,613,721,514,612,331,31])). % 182.23/182.15 cnf(5853,plain, % 182.23/182.15 (E(f9(f13(f16(f6(a5),a5)),x58531,x58532),f9(f13(a4),x58531,x58532))), % 182.23/182.15 inference(scs_inference,[],[5736,5787,2486,3515,613,721,514,612,331,31,25])). % 182.23/182.15 cnf(5854,plain, % 182.23/182.15 (E(f9(x58541,f13(f16(f6(a5),a5)),x58542),f9(x58541,f13(a4),x58542))), % 182.23/182.15 inference(scs_inference,[],[5736,5787,2486,3515,613,721,514,612,331,31,25,26])). % 182.23/182.15 cnf(5857,plain, % 182.23/182.15 (E(f15(f13(f16(f6(a5),a5)),x58571),f15(f13(a4),x58571))), % 182.23/182.15 inference(scs_inference,[],[5736,5787,2486,1052,3515,613,721,514,612,331,31,25,26,382,8,13])). % 182.23/182.15 cnf(5860,plain, % 182.23/182.15 (P6(f22(f14(a5),f6(a5),f12(a5)),f14(f22(f14(a5),f6(a5),f12(a5))))), % 182.23/182.15 inference(scs_inference,[],[5699,5736,5787,2486,1052,3515,613,721,514,612,331,31,25,26,382,8,13,29,35,238])). % 182.23/182.15 cnf(5866,plain, % 182.23/182.15 (P5(f11(a4,a5),f7(f16(f11(a4,a5),a5),f11(a4,a5)))), % 182.23/182.15 inference(scs_inference,[],[5699,5736,5787,2486,1052,3515,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112])). % 182.23/182.15 cnf(5868,plain, % 182.23/182.15 (E(f16(f13(f16(f6(a5),a5)),x58681),f16(f13(a4),x58681))), % 182.23/182.15 inference(scs_inference,[],[5699,5736,5787,2486,1052,3515,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19])). % 182.23/182.15 cnf(5876,plain, % 182.23/182.15 (E(f15(x58761,f13(f16(f6(a5),a5))),f15(x58761,f13(a4)))), % 182.23/182.15 inference(scs_inference,[],[5699,5736,5787,2486,1052,891,3515,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14])). % 182.23/182.15 cnf(5877,plain, % 182.23/182.15 (E(f10(f13(f16(f6(a5),a5)),x58771,x58772),f10(f13(a4),x58771,x58772))), % 182.23/182.15 inference(scs_inference,[],[5699,5736,5787,2486,1052,891,3515,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10])). % 182.23/182.15 cnf(5878,plain, % 182.23/182.15 (E(f22(x58781,f13(f16(f6(a5),a5)),x58782),f22(x58781,f13(a4),x58782))), % 182.23/182.15 inference(scs_inference,[],[5699,5736,5787,2486,1052,891,3515,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17])). % 182.23/182.15 cnf(5879,plain, % 182.23/182.15 (E(f22(x58791,x58792,f13(f16(f6(a5),a5))),f22(x58791,x58792,f13(a4)))), % 182.23/182.15 inference(scs_inference,[],[5699,5736,5787,2486,1052,891,3515,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18])). % 182.23/182.15 cnf(5884,plain, % 182.23/182.15 (E(f7(f13(f16(f6(a5),a5)),x58841),f7(f13(a4),x58841))), % 182.23/182.15 inference(scs_inference,[],[5699,5736,5787,2486,1052,891,3515,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30])). % 182.23/182.15 cnf(5895,plain, % 182.23/182.15 (E(f10(x58951,x58952,f13(f16(f6(a5),a5))),f10(x58951,x58952,f13(a4)))), % 182.23/182.15 inference(scs_inference,[],[5699,5736,5787,2486,1052,891,3515,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30,34,27,4,36,6,384,9,20,33,7,12])). % 182.23/182.15 cnf(5896,plain, % 182.23/182.15 (E(f19(f13(f16(f6(a5),a5)),x58961),f19(f13(a4),x58961))), % 182.23/182.15 inference(scs_inference,[],[5699,5736,5787,2486,1052,891,3515,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30,34,27,4,36,6,384,9,20,33,7,12,23])). % 182.23/182.15 cnf(5897,plain, % 182.23/182.15 (E(f19(x58971,f13(f16(f6(a5),a5))),f19(x58971,f13(a4)))), % 182.23/182.15 inference(scs_inference,[],[5699,5736,5787,2486,1052,891,3515,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30,34,27,4,36,6,384,9,20,33,7,12,23,24])). % 182.23/182.15 cnf(5898,plain, % 182.23/182.15 (P13(f10(f14(a5),f12(a5),f19(f12(a5),f14(a5))),f14(a5))), % 182.23/182.15 inference(scs_inference,[],[5758,5699,5736,5787,2486,1052,891,3515,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30,34,27,4,36,6,384,9,20,33,7,12,23,24,149])). % 182.23/182.15 cnf(5904,plain, % 182.23/182.15 (P5(f19(f12(a5),f14(a5)),f10(f14(a5),f12(a5),f19(f12(a5),f14(a5))))), % 182.23/182.15 inference(scs_inference,[],[5758,5699,5705,5736,5787,2486,1052,891,3515,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30,34,27,4,36,6,384,9,20,33,7,12,23,24,149,143,113,146])). % 182.23/182.15 cnf(5906,plain, % 182.23/182.15 (P13(f9(f14(a5),f12(a5),f19(f12(a5),f14(a5))),f14(a5))), % 182.23/182.15 inference(scs_inference,[],[5758,5699,5705,5736,5787,2486,1052,891,3515,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30,34,27,4,36,6,384,9,20,33,7,12,23,24,149,143,113,146,148])). % 182.23/182.15 cnf(5910,plain, % 182.23/182.15 (P5(f12(a5),f9(f14(a5),f12(a5),f19(f12(a5),f14(a5))))), % 182.23/182.15 inference(scs_inference,[],[5758,5699,5705,5736,5787,5744,2486,1052,891,3515,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30,34,27,4,36,6,384,9,20,33,7,12,23,24,149,143,113,146,148,91,145])). % 182.23/182.15 cnf(5912,plain, % 182.23/182.15 (P6(f12(a5),f15(f12(a5),f10(f14(a5),f6(a5),f12(a5))))), % 182.23/182.15 inference(scs_inference,[],[5758,5699,5705,5736,5787,5744,2486,1052,891,3515,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30,34,27,4,36,6,384,9,20,33,7,12,23,24,149,143,113,146,148,91,145,109])). % 182.23/182.15 cnf(5914,plain, % 182.23/182.15 (P6(f22(f14(a5),f12(a5),f19(f12(a5),f14(a5))),f14(a5))), % 182.23/182.15 inference(scs_inference,[],[5758,5699,5705,5736,5787,5744,2486,1052,891,3515,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30,34,27,4,36,6,384,9,20,33,7,12,23,24,149,143,113,146,148,91,145,109,147])). % 182.23/182.15 cnf(5916,plain, % 182.23/182.15 (~P15(f19(f12(a5),f14(a5)),f14(a5))), % 182.23/182.15 inference(scs_inference,[],[5758,5699,5705,5736,5787,5744,2486,1052,891,3515,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30,34,27,4,36,6,384,9,20,33,7,12,23,24,149,143,113,146,148,91,145,109,147,131])). % 182.23/182.15 cnf(5926,plain, % 182.23/182.15 (P4(f19(f12(a5),f14(a5)))), % 182.23/182.15 inference(scs_inference,[],[5758,5699,5705,5734,5736,5787,5744,5795,2486,1052,891,3515,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30,34,27,4,36,6,384,9,20,33,7,12,23,24,149,143,113,146,148,91,145,109,147,131,83,104,144,107,89])). % 182.23/182.15 cnf(5933,plain, % 182.23/182.15 (P7(f19(f12(a5),f14(a5)))), % 182.23/182.15 inference(scs_inference,[],[5758,5760,5699,5705,5709,5734,5736,5787,5744,5795,2486,1052,891,3515,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30,34,27,4,36,6,384,9,20,33,7,12,23,24,149,143,113,146,148,91,145,109,147,131,83,104,144,107,89,130,2,90,85])). % 182.23/182.15 cnf(5935,plain, % 182.23/182.15 (P4(f22(f14(a5),f6(a5),f12(a5)))), % 182.23/182.15 inference(scs_inference,[],[5758,5760,5699,5705,5709,5734,5736,5787,5744,5795,2486,1052,891,3515,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30,34,27,4,36,6,384,9,20,33,7,12,23,24,149,143,113,146,148,91,145,109,147,131,83,104,144,107,89,130,2,90,85,88])). % 182.23/182.15 cnf(5943,plain, % 182.23/182.15 (~P11(f19(f12(a5),f14(a5)),f12(a5),x59431)), % 182.23/182.15 inference(scs_inference,[],[5758,5760,5699,5705,5709,5734,5736,5787,5744,5795,5693,2486,1052,891,3515,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30,34,27,4,36,6,384,9,20,33,7,12,23,24,149,143,113,146,148,91,145,109,147,131,83,104,144,107,89,130,2,90,85,88,110,132,358,377])). % 182.23/182.15 cnf(5949,plain, % 182.23/182.15 (~P8(f19(f12(a5),f14(a5)),f12(a5))), % 182.23/182.15 inference(scs_inference,[],[5758,5760,5699,5705,5709,5734,5736,5787,5744,5821,5795,5693,2486,1052,891,3515,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30,34,27,4,36,6,384,9,20,33,7,12,23,24,149,143,113,146,148,91,145,109,147,131,83,104,144,107,89,130,2,90,85,88,110,132,358,377,87,82,285])). % 182.23/182.15 cnf(5958,plain, % 182.23/182.15 (P15(f11(f14(a5),f22(f14(a5),f6(a5),f12(a5))),f14(a5))), % 182.23/182.15 inference(scs_inference,[],[5715,5758,5760,5699,5705,5709,5734,5736,5787,5744,5821,1754,5795,5693,5674,5675,2486,3549,1052,1051,891,3515,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30,34,27,4,36,6,384,9,20,33,7,12,23,24,149,143,113,146,148,91,145,109,147,131,83,104,144,107,89,130,2,90,85,88,110,132,358,377,87,82,285,84,3,838,120])). % 182.23/182.15 cnf(5966,plain, % 182.23/182.15 (P11(f12(a5),f19(f12(a5),f16(f6(a5),a5)),f16(f6(a5),a5))), % 182.23/182.15 inference(scs_inference,[],[5715,5758,5760,5699,5705,5709,5734,5736,5753,5787,5791,5744,5821,1754,5795,2511,5693,5674,5675,2486,3549,1052,1051,891,890,3515,74,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30,34,27,4,36,6,384,9,20,33,7,12,23,24,149,143,113,146,148,91,145,109,147,131,83,104,144,107,89,130,2,90,85,88,110,132,358,377,87,82,285,84,3,838,120,150,835,103,141])). % 182.23/182.15 cnf(5969,plain, % 182.23/182.15 (P11(f12(a5),f19(f12(a5),a4),f16(f6(a5),a5))), % 182.23/182.15 inference(scs_inference,[],[5715,5758,5760,5699,5705,5709,5734,5736,5784,5753,5787,5791,5744,5821,1754,5795,2511,5693,5674,5675,2486,2495,3549,400,1052,1051,891,890,3515,74,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30,34,27,4,36,6,384,9,20,33,7,12,23,24,149,143,113,146,148,91,145,109,147,131,83,104,144,107,89,130,2,90,85,88,110,132,358,377,87,82,285,84,3,838,120,150,835,103,141,38,40])). % 182.23/182.15 cnf(5975,plain, % 182.23/182.15 (~E(f11(a4,a5),f19(f12(a5),f14(a5)))), % 182.23/182.15 inference(scs_inference,[],[5715,5758,5760,5699,5705,5709,5734,5736,5784,5753,5787,5791,5744,5821,1754,5795,2511,5693,5674,5675,2486,2495,3549,1203,400,1052,1051,891,890,3515,74,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30,34,27,4,36,6,384,9,20,33,7,12,23,24,149,143,113,146,148,91,145,109,147,131,83,104,144,107,89,130,2,90,85,88,110,132,358,377,87,82,285,84,3,838,120,150,835,103,141,38,40,121,136,54])). % 182.23/182.15 cnf(5977,plain, % 182.23/182.15 (~P14(f16(f6(a5),a5),f16(f6(a5),a5))), % 182.23/182.15 inference(scs_inference,[],[5715,5758,5774,5760,5699,5705,5709,5734,5736,5784,5753,5787,5791,5744,5821,1754,5795,2511,5770,5693,5674,5675,2486,2495,3549,1068,1203,400,1052,1051,891,890,3515,74,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30,34,27,4,36,6,384,9,20,33,7,12,23,24,149,143,113,146,148,91,145,109,147,131,83,104,144,107,89,130,2,90,85,88,110,132,358,377,87,82,285,84,3,838,120,150,835,103,141,38,40,121,136,54,49,64])). % 182.23/182.15 cnf(5981,plain, % 182.23/182.15 (~P14(f14(a5),f16(f6(a5),a5))), % 182.23/182.15 inference(scs_inference,[],[5715,5758,5774,5760,5699,5705,5709,5734,5736,5769,5784,5753,5787,5791,5744,5821,1754,5795,2511,5770,5713,5693,5674,5675,2486,2487,2495,3549,1068,1203,400,1052,1051,891,890,3515,399,1048,74,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30,34,27,4,36,6,384,9,20,33,7,12,23,24,149,143,113,146,148,91,145,109,147,131,83,104,144,107,89,130,2,90,85,88,110,132,358,377,87,82,285,84,3,838,120,150,835,103,141,38,40,121,136,54,49,64,48,41,63])). % 182.23/182.15 cnf(5985,plain, % 182.23/182.15 (E(f11(f16(f6(a5),a5),x59851),f11(a4,x59851))), % 182.23/182.15 inference(rename_variables,[],[2503])). % 182.23/182.15 cnf(5986,plain, % 182.23/182.15 (~P9(f12(a5),f22(f14(a5),f6(a5),f12(a5)))), % 182.23/182.15 inference(scs_inference,[],[5636,5715,5758,5774,5832,5760,5699,5705,5709,5734,5736,5769,5784,1035,5753,5787,5791,5744,5821,1754,5795,2511,5770,5713,5693,5674,5675,2486,2487,2495,2503,3549,1068,1203,400,1052,1051,891,890,3515,399,1048,74,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30,34,27,4,36,6,384,9,20,33,7,12,23,24,149,143,113,146,148,91,145,109,147,131,83,104,144,107,89,130,2,90,85,88,110,132,358,377,87,82,285,84,3,838,120,150,835,103,141,38,40,121,136,54,49,64,48,41,63,68,44,45,137])). % 182.23/182.15 cnf(5989,plain, % 182.23/182.15 (~P3(f22(f14(a5),f6(a5),f12(a5)))), % 182.23/182.15 inference(scs_inference,[],[5636,5715,5758,5774,5832,5760,5699,5705,5709,5734,5736,5769,5784,1035,5753,5787,5791,5744,5821,5789,1754,5795,2511,5770,5713,5693,5674,5675,2486,2487,2495,2503,3549,1068,1203,400,154,1052,1051,891,890,3515,399,1048,74,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30,34,27,4,36,6,384,9,20,33,7,12,23,24,149,143,113,146,148,91,145,109,147,131,83,104,144,107,89,130,2,90,85,88,110,132,358,377,87,82,285,84,3,838,120,150,835,103,141,38,40,121,136,54,49,64,48,41,63,68,44,45,137,52,92])). % 182.23/182.15 cnf(5993,plain, % 182.23/182.15 (P15(f12(a5),f10(f14(a5),f6(a5),f12(a5)))), % 182.23/182.15 inference(scs_inference,[],[5636,5715,5758,5774,5832,5760,5699,5705,5709,5734,5736,5769,5784,1035,5753,5787,5791,5744,5821,5789,1754,5795,2511,5770,5713,5693,5674,5675,2486,2487,2495,2503,3549,3523,1068,1203,400,154,1052,1051,891,890,3515,399,1048,74,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30,34,27,4,36,6,384,9,20,33,7,12,23,24,149,143,113,146,148,91,145,109,147,131,83,104,144,107,89,130,2,90,85,88,110,132,358,377,87,82,285,84,3,838,120,150,835,103,141,38,40,121,136,54,49,64,48,41,63,68,44,45,137,52,92,100,101])). % 182.23/182.15 cnf(6001,plain, % 182.23/182.15 (~P15(f12(a5),f14(f22(f14(a5),f6(a5),f12(a5))))), % 182.23/182.15 inference(scs_inference,[],[5636,5715,5758,5774,5832,5760,5699,5705,5709,5734,5736,5769,5784,1035,5753,5766,5787,5791,5809,5805,5744,5821,5789,1754,5686,5795,2511,5770,5713,5693,5674,5675,2486,2487,2495,3503,2503,3549,3523,1068,1203,400,69,154,1052,1051,891,890,3515,399,1048,74,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30,34,27,4,36,6,384,9,20,33,7,12,23,24,149,143,113,146,148,91,145,109,147,131,83,104,144,107,89,130,2,90,85,88,110,132,358,377,87,82,285,84,3,838,120,150,835,103,141,38,40,121,136,54,49,64,48,41,63,68,44,45,137,52,92,100,101,93,135,115,124])). % 182.23/182.15 cnf(6009,plain, % 182.23/182.15 (~E(f19(f12(a5),f14(a5)),a5)), % 182.23/182.15 inference(scs_inference,[],[5636,5715,5758,5774,5832,5760,5699,5705,5709,5734,5736,5769,5784,1035,5753,5766,5787,5791,5809,5805,5744,5821,5789,1754,5686,5795,2511,5770,5713,5693,5674,5675,2486,2487,2495,3503,2503,3549,3523,1068,1203,400,69,154,1052,1051,891,890,3515,399,1048,74,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30,34,27,4,36,6,384,9,20,33,7,12,23,24,149,143,113,146,148,91,145,109,147,131,83,104,144,107,89,130,2,90,85,88,110,132,358,377,87,82,285,84,3,838,120,150,835,103,141,38,40,121,136,54,49,64,48,41,63,68,44,45,137,52,92,100,101,93,135,115,124,903,720,1587,1010])). % 182.23/182.15 cnf(6012,plain, % 182.23/182.15 (P8(f12(a5),f19(f12(a5),f14(a5)))), % 182.23/182.15 inference(scs_inference,[],[5636,5715,5758,5774,5832,5760,5699,5705,5709,5734,5736,5769,5784,1035,5753,5766,5787,5791,5809,5805,5744,5821,5789,1754,5686,5795,2511,5770,5713,5693,5674,5675,2486,2487,2495,3503,2503,3549,3523,1068,1203,400,69,154,1052,1051,891,890,3515,399,1048,74,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30,34,27,4,36,6,384,9,20,33,7,12,23,24,149,143,113,146,148,91,145,109,147,131,83,104,144,107,89,130,2,90,85,88,110,132,358,377,87,82,285,84,3,838,120,150,835,103,141,38,40,121,136,54,49,64,48,41,63,68,44,45,137,52,92,100,101,93,135,115,124,903,720,1587,1010,239,94])). % 182.23/182.15 cnf(6018,plain, % 182.23/182.15 (~P14(f19(f12(a5),f14(a5)),f6(a5))), % 182.23/182.15 inference(scs_inference,[],[5636,5715,5758,5774,5832,5760,5699,5705,5709,5734,5736,5769,5784,1035,5753,5766,5787,5791,5809,5805,5744,5821,5789,1754,5686,5795,2511,5770,5713,5693,5674,5675,2486,2487,2495,3503,2503,3549,3523,1068,1203,400,69,154,1052,1051,891,890,3515,399,1048,74,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30,34,27,4,36,6,384,9,20,33,7,12,23,24,149,143,113,146,148,91,145,109,147,131,83,104,144,107,89,130,2,90,85,88,110,132,358,377,87,82,285,84,3,838,120,150,835,103,141,38,40,121,136,54,49,64,48,41,63,68,44,45,137,52,92,100,101,93,135,115,124,903,720,1587,1010,239,94,719,86,249])). % 182.23/182.15 cnf(6023,plain, % 182.23/182.15 (~P11(f19(f12(a5),f14(a5)),f6(a5),x60231)), % 182.23/182.15 inference(scs_inference,[],[5636,5715,5758,5774,5832,5760,5699,5705,5709,5734,5736,5769,5784,1035,5753,5766,5787,5791,5809,5805,5744,5821,5789,1754,5686,5795,2511,5770,5713,5693,5674,5675,2486,2487,2495,3503,2503,5985,3549,3523,1068,1203,400,69,154,1052,1051,891,890,3515,399,1048,74,613,721,514,612,331,31,25,26,382,8,13,29,35,238,32,5,22,380,112,19,28,37,16,114,515,14,10,17,18,378,11,15,21,30,34,27,4,36,6,384,9,20,33,7,12,23,24,149,143,113,146,148,91,145,109,147,131,83,104,144,107,89,130,2,90,85,88,110,132,358,377,87,82,285,84,3,838,120,150,835,103,141,38,40,121,136,54,49,64,48,41,63,68,44,45,137,52,92,100,101,93,135,115,124,903,720,1587,1010,239,94,719,86,249,1936,887])). % 182.23/182.15 cnf(6037,plain, % 182.23/182.15 (~P7(f22(f14(a5),f6(a5),f12(a5)))), % 182.23/182.15 inference(scs_inference,[],[4551,5989,138,82])). % 182.23/182.15 cnf(6039,plain, % 182.23/182.15 (~P11(f19(f12(a5),f16(f6(a5),a5)),f12(a5),x60391)), % 182.23/182.15 inference(scs_inference,[],[4551,5966,5989,138,82,377])). % 182.23/182.15 cnf(6041,plain, % 182.23/182.15 (~P12(f22(f14(a5),f6(a5),f12(a5)),x60411,x60412)), % 182.23/182.15 inference(scs_inference,[],[4551,5966,5989,138,82,377,129])). % 182.23/182.15 cnf(6043,plain, % 182.23/182.15 (~P14(x60431,f22(f14(a5),f6(a5),f12(a5)))), % 182.23/182.15 inference(scs_inference,[],[4551,5966,5989,138,82,377,129,85])). % 182.23/182.15 cnf(6045,plain, % 182.23/182.15 (~P12(x60451,f22(f14(a5),f6(a5),f12(a5)),x60452)), % 182.23/182.15 inference(scs_inference,[],[4551,5966,5989,138,82,377,129,85,128])). % 182.23/182.15 cnf(6052,plain, % 182.23/182.15 (~P15(f22(f14(a5),f6(a5),f12(a5)),x60521)), % 182.23/182.15 inference(scs_inference,[],[4551,2480,5769,5966,5989,138,82,377,129,85,128,1218,2,130,86])). % 182.23/182.15 cnf(6054,plain, % 182.23/182.15 (~P14(f13(a5),f11(a4,a5))), % 182.23/182.15 inference(scs_inference,[],[4551,2480,4894,5769,5966,5989,138,82,377,129,85,128,1218,2,130,86,94])). % 182.23/182.15 cnf(6058,plain, % 182.23/182.15 (~E(f14(f6(a5)),a3)), % 182.23/182.15 inference(scs_inference,[],[4551,2480,3630,4894,5769,3864,5966,5989,138,82,377,129,85,128,1218,2,130,86,94,131,2527])). % 182.23/182.15 cnf(6065,plain, % 182.23/182.15 (P15(f11(a4,a5),f7(f7(a4,f11(a4,a5)),f11(a4,a5)))), % 182.23/182.15 inference(scs_inference,[],[4551,3517,2480,3630,3615,4894,5769,3864,5966,5943,5989,5641,138,82,377,129,85,128,1218,2,130,86,94,131,2527,1209,896,694,1031])). % 182.23/182.15 cnf(6071,plain, % 182.23/182.15 (~P6(f22(f14(a5),f6(a5),f12(a5)),a1)), % 182.23/182.15 inference(scs_inference,[],[4551,3517,2480,69,3630,3615,4894,1698,5769,3864,5966,5943,5989,5641,138,82,377,129,85,128,1218,2,130,86,94,131,2527,1209,896,694,1031,904,1012,93])). % 182.23/182.15 cnf(6073,plain, % 182.23/182.15 (~P5(f12(a5),f14(a5))), % 182.23/182.15 inference(scs_inference,[],[4551,3517,2480,69,3630,3615,4894,3523,1698,5769,3521,3864,5966,5943,5989,5641,138,82,377,129,85,128,1218,2,130,86,94,131,2527,1209,896,694,1031,904,1012,93,101])). % 182.23/182.15 cnf(6075,plain, % 182.23/182.15 (P13(f10(f14(a5),f6(a5),f12(a5)),a4)), % 182.23/182.15 inference(scs_inference,[],[1048,4551,3517,2480,69,3630,3615,4894,3523,1698,5769,5701,3521,3864,5966,5943,5989,5641,138,82,377,129,85,128,1218,2,130,86,94,131,2527,1209,896,694,1031,904,1012,93,101,43])). % 182.23/182.15 cnf(6076,plain, % 182.23/182.15 (~E(f10(f14(a5),f6(a5),f12(a5)),f14(a5))), % 182.23/182.15 inference(scs_inference,[],[1048,4551,3517,2480,69,3630,3615,5705,4894,3523,1698,5769,5701,3521,3864,5966,5943,5989,5641,138,82,377,129,85,128,1218,2,130,86,94,131,2527,1209,896,694,1031,904,1012,93,101,43,62])). % 182.23/182.15 cnf(6077,plain, % 182.23/182.15 (P15(f11(f14(a5),f22(f14(a5),f6(a5),f12(a5))),a4)), % 182.23/182.15 inference(scs_inference,[],[1048,4551,3517,2480,69,3630,3615,5705,4894,3523,1698,5769,5701,3521,3864,5966,5943,5989,5958,5641,138,82,377,129,85,128,1218,2,130,86,94,131,2527,1209,896,694,1031,904,1012,93,101,43,62,55])). % 182.23/182.15 cnf(6079,plain, % 182.23/182.15 (P11(f12(a5),f13(a5),f16(f6(a5),a5))), % 182.23/182.15 inference(scs_inference,[],[1048,389,3515,4551,3517,2480,69,3630,3507,3615,5705,4894,3523,1698,5769,5701,3521,3864,5966,5943,5989,6012,5958,5641,138,82,377,129,85,128,1218,2,130,86,94,131,2527,1209,896,694,1031,904,1012,93,101,43,62,55,68,41])). % 182.23/182.15 cnf(6084,plain, % 182.23/182.15 (~P11(x60841,f6(a5),a4)), % 182.23/182.15 inference(scs_inference,[],[74,1048,389,3515,4551,3517,2480,3511,161,69,3630,3507,5715,3615,5705,4894,3523,1698,661,5709,5769,5701,3521,3698,3864,5966,5943,5989,6012,5958,5641,138,82,377,129,85,128,1218,2,130,86,94,131,2527,1209,896,694,1031,904,1012,93,101,43,62,55,68,41,48,49,54,136])). % 182.23/182.15 cnf(6088,plain, % 182.23/182.15 (P11(f6(a5),f13(a5),a4)), % 182.23/182.15 inference(scs_inference,[],[74,1048,389,3515,172,4551,3517,2480,3511,161,891,69,3630,3507,5715,3615,5705,4894,3523,1698,661,5709,5769,5701,3521,3698,3864,5966,5943,5989,6012,5958,5641,138,82,377,129,85,128,1218,2,130,86,94,131,2527,1209,896,694,1031,904,1012,93,101,43,62,55,68,41,48,49,54,136,40,150])). % 182.23/182.15 cnf(6095,plain, % 182.23/182.15 (~P16(f22(f14(a5),f6(a5),f12(a5)),x60951)), % 182.23/182.15 inference(scs_inference,[],[74,1048,389,3515,172,4551,3517,2480,3511,3547,161,891,69,3630,3507,5715,3615,5705,4894,3523,1698,661,5709,5769,5701,2487,3521,3698,3864,5878,5966,5975,5943,5989,6012,5958,5641,138,82,377,129,85,128,1218,2,130,86,94,131,2527,1209,896,694,1031,904,1012,93,101,43,62,55,68,41,48,49,54,136,40,150,3,122,110])). % 182.23/182.15 cnf(6097,plain, % 182.23/182.15 (P11(f11(a4,a5),f19(f11(a4,a5),a4),a4)), % 182.23/182.15 inference(scs_inference,[],[74,1048,389,3515,172,4551,3517,2480,3511,3547,161,891,69,3630,3507,5715,3615,5705,4894,3523,1698,661,5709,5769,5701,2487,3521,3698,3864,5878,5966,5975,5943,5989,6012,5958,5641,138,82,377,129,85,128,1218,2,130,86,94,131,2527,1209,896,694,1031,904,1012,93,101,43,62,55,68,41,48,49,54,136,40,150,3,122,110,5588])). % 182.23/182.15 cnf(6098,plain, % 182.23/182.15 (~P10(f11(a4,a5),f14(a5))), % 182.23/182.15 inference(scs_inference,[],[74,1048,389,3515,172,4551,3517,2480,3511,3547,161,891,69,3630,3507,5715,3615,5705,4894,3523,1698,661,5709,5769,5701,2487,3521,3698,3864,5878,5966,5975,5943,5989,6012,5958,5641,138,82,377,129,85,128,1218,2,130,86,94,131,2527,1209,896,694,1031,904,1012,93,101,43,62,55,68,41,48,49,54,136,40,150,3,122,110,5588,4297])). % 182.23/182.15 cnf(6099,plain, % 182.23/182.15 (P11(f11(a4,a5),f12(a5),f14(a5))), % 182.23/182.15 inference(scs_inference,[],[74,1048,389,3515,172,4551,3517,2480,3511,3547,161,891,69,3630,3507,5715,3615,5705,4894,3523,1698,661,5709,5769,5701,2487,3521,3698,3864,5878,5966,5975,5943,5989,6012,5958,5641,138,82,377,129,85,128,1218,2,130,86,94,131,2527,1209,896,694,1031,904,1012,93,101,43,62,55,68,41,48,49,54,136,40,150,3,122,110,5588,4297,4293])). % 182.23/182.15 cnf(6100,plain, % 182.23/182.15 (~P9(f11(a4,a5),a5)), % 182.23/182.15 inference(scs_inference,[],[74,1048,389,3515,172,4551,3517,2480,3511,3547,161,891,69,3630,3507,5715,3615,5705,4894,3523,1698,661,5709,5769,5701,2487,3521,3698,3864,5878,5966,5975,5943,5989,6012,5958,5641,138,82,377,129,85,128,1218,2,130,86,94,131,2527,1209,896,694,1031,904,1012,93,101,43,62,55,68,41,48,49,54,136,40,150,3,122,110,5588,4297,4293,4200])). % 182.23/182.15 cnf(6101,plain, % 182.23/182.15 (~P10(f11(a4,a5),a4)), % 182.23/182.15 inference(scs_inference,[],[74,1048,389,3515,172,4551,3517,2480,3511,3547,161,891,69,3630,3507,5715,3615,5705,4894,3523,1698,661,5709,5769,5701,2487,3521,3698,3864,5878,5966,5975,5943,5989,6012,5958,5641,138,82,377,129,85,128,1218,2,130,86,94,131,2527,1209,896,694,1031,904,1012,93,101,43,62,55,68,41,48,49,54,136,40,150,3,122,110,5588,4297,4293,4200,4201])). % 182.23/182.15 cnf(6112,plain, % 182.23/182.15 (E(f11(a4,a5),f6(a5))), % 182.23/182.15 inference(scs_inference,[],[6084,4195])). % 182.23/182.15 cnf(6113,plain, % 182.23/182.15 (~P6(f11(a4,a5),a3)), % 182.23/182.15 inference(scs_inference,[],[6084,4198])). % 182.23/182.15 cnf(6114,plain, % 182.23/182.15 (~P6(f11(a4,a5),a2)), % 182.23/182.15 inference(scs_inference,[],[6084,4199])). % 182.23/182.15 cnf(6115,plain, % 182.23/182.15 (~P12(f11(a4,a5),f13(a5),f14(a5))), % 182.23/182.15 inference(scs_inference,[],[6084,4202])). % 182.23/182.15 cnf(6117,plain, % 182.23/182.15 (E(f6(a5),f11(a4,a5))), % 182.23/182.15 inference(scs_inference,[],[6084,4288])). % 182.23/182.15 cnf(6119,plain, % 182.23/182.15 (P11(f11(a4,a5),f12(a5),a4)), % 182.23/182.15 inference(scs_inference,[],[6084,4292])). % 182.23/182.15 cnf(6120,plain, % 182.23/182.15 (~P11(f11(a4,a5),f6(a5),f14(a5))), % 182.23/182.15 inference(scs_inference,[],[6084,4294])). % 182.23/182.15 cnf(6121,plain, % 182.23/182.15 (P14(f11(a4,a5),f12(a5))), % 182.23/182.15 inference(scs_inference,[],[6084,4295])). % 182.23/182.15 cnf(6124,plain, % 182.23/182.15 (~P8(f12(a5),f11(a4,a5))), % 182.23/182.15 inference(scs_inference,[],[6084,4303])). % 182.23/182.15 cnf(6126,plain, % 182.23/182.15 (P11(f11(a4,a5),f19(f11(a4,a5),f14(a5)),f14(a5))), % 182.23/182.15 inference(scs_inference,[],[6100,5355])). % 182.23/182.15 cnf(6129,plain, % 182.23/182.15 (~P11(f19(f11(a4,a5),a4),f11(a4,a5),x61291)), % 182.23/182.15 inference(scs_inference,[],[4548,6097,138,377])). % 182.23/182.15 cnf(6132,plain, % 182.23/182.15 (~P11(f13(a5),f11(a4,a5),x61321)), % 182.23/182.15 inference(scs_inference,[],[4548,2486,6097,6054,138,377,2,130])). % 182.23/182.15 cnf(6134,plain, % 182.23/182.15 (~P14(f13(a5),f11(f16(f6(a5),a5),a5))), % 182.23/182.15 inference(scs_inference,[],[4548,2486,6097,5775,6054,138,377,2,130,94])). % 182.23/182.15 cnf(6136,plain, % 182.23/182.15 (~P11(x61361,f11(a4,a5),f16(f11(a4,a5),a5))), % 182.23/182.15 inference(scs_inference,[],[4548,2486,5736,6097,5775,6054,138,377,2,130,94,131])). % 182.23/182.15 cnf(6140,plain, % 182.23/182.15 (~P11(f19(f12(a5),f16(f6(a5),a5)),f12(a5),x61401)), % 182.23/182.15 inference(rename_variables,[],[6039])). % 182.23/182.15 cnf(6154,plain, % 182.23/182.15 (~P5(f19(f12(a5),f14(a5)),f14(a5))), % 182.23/182.15 inference(scs_inference,[],[4548,2486,5736,3632,5943,5734,3947,6097,5969,6039,6140,5933,5866,5916,5775,6054,138,377,2,130,94,131,2527,1209,694,896,1012,1031,904,892,101])). % 182.23/182.15 cnf(6156,plain, % 182.23/182.15 (P13(f9(f14(a5),f6(a5),f12(a5)),a4)), % 182.23/182.15 inference(scs_inference,[],[1048,4548,2486,5736,3632,5943,5734,3947,6097,5969,6039,6140,5933,5866,5916,5775,6054,5707,138,377,2,130,94,131,2527,1209,694,896,1012,1031,904,892,101,43])). % 182.23/182.15 cnf(6159,plain, % 182.23/182.15 (P11(f12(a5),f19(f12(a5),f14(a5)),a4)), % 182.23/182.15 inference(scs_inference,[],[1048,399,4548,2486,5758,5736,3632,5943,5734,3947,6097,5969,6039,6140,5754,5933,5866,5904,5916,5775,6054,5707,138,377,2,130,94,131,2527,1209,694,896,1012,1031,904,892,101,43,62,55,41])). % 182.23/182.15 cnf(6166,plain, % 182.23/182.15 (~P12(f11(a4,a5),f19(f12(a5),f14(a5)),f14(a5))), % 182.23/182.15 inference(scs_inference,[],[74,1048,399,172,4548,2486,5758,5736,3632,5795,661,5686,156,5943,5734,2973,3947,6099,6097,5969,6039,6140,5754,5933,5866,5904,5916,5775,6054,5707,138,377,2,130,94,131,2527,1209,694,896,1012,1031,904,892,101,43,62,55,41,48,49,136,40,151])). % 182.23/182.15 cnf(6168,plain, % 182.23/182.15 (P11(f6(a5),f19(f12(a5),f14(a5)),f14(a5))), % 182.23/182.15 inference(scs_inference,[],[74,1048,399,172,4548,2486,1202,5758,5736,3632,5795,661,5686,156,5943,5734,2973,3947,6099,6097,5969,6039,6140,5754,5933,5866,5904,5916,5775,6054,5707,138,377,2,130,94,131,2527,1209,694,896,1012,1031,904,892,101,43,62,55,41,48,49,136,40,151,150])). % 182.23/182.15 cnf(6175,plain, % 182.23/182.15 (~P12(f6(a5),f19(f12(a5),f14(a5)),a4)), % 182.23/182.15 inference(scs_inference,[],[74,1048,399,172,4548,2486,3511,1202,5758,5736,3632,5795,661,5686,156,5943,5734,2495,2973,3947,5896,6099,6097,5969,6039,6140,5754,5933,5866,5904,5916,5775,6054,5707,138,377,2,130,94,131,2527,1209,694,896,1012,1031,904,892,101,43,62,55,41,48,49,136,40,151,150,3,122,914])). % 182.23/182.15 cnf(6183,plain, % 182.23/182.15 (E(f11(a4,a5),f6(a5))), % 182.23/182.15 inference(scs_inference,[],[6120,4016])). % 182.23/182.15 cnf(6184,plain, % 182.23/182.15 (E(f6(a5),f11(a4,a5))), % 182.23/182.15 inference(scs_inference,[],[6120,4038])). % 182.23/182.15 cnf(6189,plain, % 182.23/182.15 (~P11(f19(f12(a5),a4),f12(a5),x61891)), % 182.23/182.15 inference(scs_inference,[],[3517,5969,138,377])). % 182.23/182.15 cnf(6208,plain, % 182.23/182.15 (P6(f11(a4,a5),f14(f6(a5)))), % 182.23/182.15 inference(scs_inference,[],[3517,2495,5958,5969,6039,6117,6079,5977,5926,5786,138,377,2,1218,130,131,1209,694,896,1012,904,4178,2525])). % 182.23/182.15 cnf(6213,plain, % 182.23/182.15 (P13(f10(f14(a5),f12(a5),f19(f12(a5),f14(a5))),a4)), % 182.23/182.15 inference(scs_inference,[],[1048,3517,3523,2495,5958,5969,6039,6112,6117,6079,5725,5977,5898,5926,5786,138,377,2,1218,130,131,1209,694,896,1012,904,4178,2525,3724,695,101,43])). % 182.23/182.15 cnf(6217,plain, % 182.23/182.15 (P7(f6(a5))), % 182.23/182.15 inference(scs_inference,[],[1048,389,3517,3523,1025,2495,5958,5969,6039,5641,6112,6117,6079,5910,5725,5977,5898,6073,5926,6077,5786,138,377,2,1218,130,131,1209,694,896,1012,904,4178,2525,3724,695,101,43,61,62,55,53])). % 182.23/182.15 cnf(6218,plain, % 182.23/182.15 (P11(f6(a5),f19(f11(a4,a5),a4),a4)), % 182.23/182.15 inference(scs_inference,[],[1048,389,3517,3523,1025,6097,2495,5958,5969,6039,5641,6112,6117,6079,5910,5725,5977,5898,6073,5926,6077,5786,138,377,2,1218,130,131,1209,694,896,1012,904,4178,2525,3724,695,101,43,61,62,55,53,39])). % 182.23/182.15 cnf(6219,plain, % 182.23/182.15 (P11(f12(a5),f19(f12(a5),f16(f6(a5),a5)),a4)), % 182.23/182.15 inference(scs_inference,[],[1048,389,399,3517,3523,5966,1025,6097,2495,5958,5969,6039,5641,6112,6117,6079,5910,5725,5977,5898,6073,5926,6077,5786,138,377,2,1218,130,131,1209,694,896,1012,904,4178,2525,3724,695,101,43,61,62,55,53,39,41])). % 182.23/182.15 cnf(6222,plain, % 182.23/182.15 (P6(f22(f14(a5),f12(a5),f19(f12(a5),f14(a5))),a4)), % 182.23/182.15 inference(scs_inference,[],[1048,389,399,3517,3594,3523,5966,1025,6097,2495,5958,3698,5969,6039,5641,6112,6117,5914,6079,5910,5725,5977,5898,6073,5926,6077,5786,138,377,2,1218,130,131,1209,694,896,1012,904,4178,2525,3724,695,101,43,61,62,55,53,39,41,48,63,49])). % 182.23/182.15 cnf(6225,plain, % 182.23/182.15 (~P12(f11(a4,a5),f13(a5),a4)), % 182.23/182.15 inference(scs_inference,[],[1048,389,399,3515,172,3517,3594,3523,5966,1025,6097,2495,5958,3698,5969,6039,5641,6112,6117,5914,6119,6079,5910,5725,5977,5898,6073,5926,6077,5786,138,377,2,1218,130,131,1209,694,896,1012,904,4178,2525,3724,695,101,43,61,62,55,53,39,41,48,63,49,40,151])). % 182.23/182.15 cnf(6228,plain, % 182.23/182.15 (~P14(f19(f12(a5),f14(a5)),f11(a4,a5))), % 182.23/182.15 inference(scs_inference,[],[1048,389,399,3515,172,3517,3587,3594,3523,5966,1025,6097,2495,5958,3698,5969,6039,5641,6012,6112,6117,5914,6119,6079,5910,5725,6124,5977,5898,6073,5926,6077,5786,138,377,2,1218,130,131,1209,694,896,1012,904,4178,2525,3724,695,101,43,61,62,55,53,39,41,48,63,49,40,151,67,835])). % 182.23/182.15 cnf(6230,plain, % 182.23/182.15 (P11(f6(a5),f19(f12(a5),f16(f6(a5),a5)),f16(f6(a5),a5))), % 182.23/182.15 inference(scs_inference,[],[1048,389,399,3515,172,3517,890,3587,3594,3523,5966,1025,6097,2495,5958,3698,5969,6039,5641,6012,6112,6117,5914,6119,6079,5910,5725,6124,5977,5898,6073,5926,6077,5786,138,377,2,1218,130,131,1209,694,896,1012,904,4178,2525,3724,695,101,43,61,62,55,53,39,41,48,63,49,40,151,67,835,150])). % 182.23/182.15 cnf(6232,plain, % 182.23/182.15 (P17(f11(a4,a5),f22(f14(a5),f6(a5),f12(a5)))), % 182.23/182.15 inference(scs_inference,[],[1048,389,399,3515,172,3517,890,3587,3594,3523,5966,1025,6097,2495,5958,3698,5969,6039,5641,6012,6112,6117,5914,6119,6079,5719,5910,5725,6124,5977,5898,6073,5926,6077,5786,138,377,2,1218,130,131,1209,694,896,1012,904,4178,2525,3724,695,101,43,61,62,55,53,39,41,48,63,49,40,151,67,835,150,65])). % 182.23/182.15 cnf(6233,plain, % 182.23/182.15 (~P8(f19(f12(a5),f14(a5)),f11(a4,a5))), % 182.23/182.15 inference(scs_inference,[],[1048,389,399,3515,172,3517,890,3587,3594,3523,5966,1025,6097,2495,5958,3698,5969,6039,5641,6012,6112,6117,5914,6119,6079,6121,5719,5910,5725,6124,5977,5898,6073,5926,6077,5786,138,377,2,1218,130,131,1209,694,896,1012,904,4178,2525,3724,695,101,43,61,62,55,53,39,41,48,63,49,40,151,67,835,150,65,837])). % 182.23/182.15 cnf(6242,plain, % 182.23/182.15 (P15(f6(a5),a1)), % 182.23/182.15 inference(scs_inference,[],[74,1048,389,399,3515,172,3517,890,3511,3587,3594,3523,5966,1025,6097,2495,5958,3698,5969,6039,5641,2491,6012,6112,6117,5868,5914,6119,6079,6121,5719,5910,5725,6124,5977,5898,6073,5926,6077,5786,138,377,2,1218,130,131,1209,694,896,1012,904,4178,2525,3724,695,101,43,61,62,55,53,39,41,48,63,49,40,151,67,835,150,65,837,3,122,914,3764])). % 182.23/182.15 cnf(6256,plain, % 182.23/182.15 (E(f22(a4,x62561,x62562),f22(f16(f6(a5),a5),x62561,x62562))), % 182.23/182.15 inference(scs_inference,[],[3589,2487,6126,138,377,2])). % 182.23/182.15 cnf(6262,plain, % 182.23/182.15 (~P11(f19(f12(a5),a4),f12(a5),x62621)), % 182.23/182.15 inference(rename_variables,[],[6189])). % 182.23/182.15 cnf(6273,plain, % 182.23/182.15 (P11(f6(a5),f19(f11(a4,a5),f14(a5)),f14(a5))), % 182.23/182.15 inference(scs_inference,[],[1048,3589,3523,6112,2487,5866,5754,6126,6189,6262,6001,6228,5906,5935,138,377,2,130,131,896,1012,892,101,43,61,39])). % 182.23/182.15 cnf(6302,plain, % 182.23/182.15 (~P11(x63021,f22(f14(a5),f6(a5),f12(a5)),x63022)), % 182.23/182.15 inference(scs_inference,[],[5878,5791,6273,6043,138,377,2,130])). % 182.23/182.15 cnf(6304,plain, % 182.23/182.15 (~P11(x63041,f13(a5),f10(a4,f12(a5),f13(a5)))), % 182.23/182.15 inference(scs_inference,[],[5878,5791,5787,6273,6043,138,377,2,130,131])). % 182.23/182.15 cnf(6306,plain, % 182.23/182.15 (~P10(f22(f14(a5),f6(a5),f12(a5)),x63061)), % 182.23/182.15 inference(scs_inference,[],[5878,5791,5787,6273,6043,6052,138,377,2,130,131,134])). % 182.23/182.15 cnf(6310,plain, % 182.23/182.15 (P5(f11(a4,a5),a1)), % 182.23/182.15 inference(scs_inference,[],[6117,3523,5878,5791,5787,3543,6273,6043,6052,3593,138,377,2,130,131,134,101,61])). % 182.23/182.15 cnf(6312,plain, % 182.23/182.15 (P11(f11(a4,a5),f13(a5),a4)), % 182.23/182.15 inference(scs_inference,[],[389,6117,3523,5878,5791,5787,3543,6088,6273,6043,6075,6052,3593,138,377,2,130,131,134,101,61,43,39])). % 182.23/182.15 cnf(6313,plain, % 182.23/182.15 (~E(a4,f10(a4,f12(a5),f13(a5)))), % 182.23/182.15 inference(scs_inference,[],[389,3515,6117,3523,5878,5791,5787,3543,6088,6273,6043,6075,6052,3593,138,377,2,130,131,134,101,61,43,39,41])). % 182.23/182.15 cnf(6324,plain, % 182.23/182.15 (~P9(f22(f14(a5),f6(a5),f12(a5)),x63241)), % 182.23/182.15 inference(scs_inference,[],[389,3515,172,890,6117,3523,5878,5791,5652,6079,1026,5787,2501,3543,5852,6256,5697,6088,6273,5848,6043,6075,6052,3593,138,377,2,130,131,134,101,61,43,39,41,48,49,40,150,3,111])). % 182.23/182.15 cnf(6326,plain, % 182.23/182.15 (P15(f11(a4,a5),a1)), % 182.23/182.15 inference(scs_inference,[],[389,3515,172,890,6117,3523,5878,5791,5652,6079,1026,5787,2501,3543,5852,6256,5697,6088,6273,5848,6043,6075,6052,3593,138,377,2,130,131,134,101,61,43,39,41,48,49,40,150,3,111,1031])). % 182.23/182.15 cnf(6344,plain, % 182.23/182.15 (P11(f11(a4,a5),f19(f12(a5),f14(a5)),f14(a5))), % 182.23/182.15 inference(scs_inference,[],[389,6117,2491,5943,5848,6077,6168,5711,5981,6156,138,377,2,130,131,61,43,39])). % 182.23/182.15 cnf(6345,plain, % 182.23/182.15 (P11(f12(a5),f19(f12(a5),a4),a4)), % 182.23/182.15 inference(scs_inference,[],[389,399,6117,5969,2491,5943,5848,6077,6168,5711,5981,6156,138,377,2,130,131,61,43,39,41])). % 182.23/182.15 cnf(6346,plain, % 182.23/182.15 (P6(f6(a5),f15(f11(a4,a5),f7(f16(f11(a4,a5),a5),f11(a4,a5))))), % 182.23/182.15 inference(scs_inference,[],[389,399,6117,6112,5969,2491,5943,5848,6077,5846,6168,5711,5981,6156,138,377,2,130,131,61,43,39,41,48])). % 182.23/182.15 cnf(6348,plain, % 182.23/182.15 (P11(f6(a5),f19(f12(a5),f14(a5)),a4)), % 182.23/182.15 inference(scs_inference,[],[389,399,891,6117,6112,5969,1026,2491,5943,5848,6077,5846,6168,5711,5981,6156,6159,138,377,2,130,131,61,43,39,41,48,49,150])). % 182.23/182.15 cnf(6353,plain, % 182.23/182.15 (P15(f11(a4,a5),f9(f14(a5),f6(a5),f12(a5)))), % 182.23/182.15 inference(scs_inference,[],[389,399,891,6117,6112,5969,5878,1026,2491,5943,6256,5848,6077,5846,6168,5711,5981,6156,6159,138,377,2,130,131,61,43,39,41,48,49,150,3,1031])). % 182.23/182.15 cnf(6355,plain, % 182.23/182.15 (~P12(f6(a5),f19(f12(a5),a4),a4)), % 182.23/182.15 inference(scs_inference,[],[389,399,891,6117,6112,5969,5878,1026,2491,5943,6256,5848,6077,5846,6168,5711,5981,6156,6159,138,377,2,130,131,61,43,39,41,48,49,150,3,1031,914])). % 182.23/182.15 cnf(6370,plain, % 182.23/182.15 (E(f7(a4,x63701),f7(f16(f6(a5),a5),x63701))), % 182.23/182.15 inference(scs_inference,[],[2501,6039,6230,138,377,2])). % 182.23/182.15 cnf(6373,plain, % 182.23/182.15 (~P11(x63731,f11(a4,a5),f9(f14(a5),f6(a5),f12(a5)))), % 182.23/182.15 inference(scs_inference,[],[2501,6039,6353,6230,6134,138,377,2,130,131])). % 182.23/182.15 cnf(6378,plain, % 182.23/182.15 (P13(f7(f16(f6(a5),a5),f11(a4,a5)),a4)), % 182.23/182.15 inference(scs_inference,[],[6117,2501,6039,516,6353,5793,5643,6230,6134,138,377,2,130,131,1037,61,43,42])). % 182.23/182.15 cnf(6380,plain, % 182.23/182.15 (P11(f11(a4,a5),f19(f11(a4,a5),f14(a5)),a4)), % 182.23/182.15 inference(scs_inference,[],[1048,6117,6126,2501,6039,516,6348,6353,5793,5643,6230,6134,138,377,2,130,131,1037,61,43,42,39,41])). % 182.23/182.15 cnf(6383,plain, % 182.23/182.15 (P11(f6(a5),f19(f12(a5),a4),a4)), % 182.23/182.15 inference(scs_inference,[],[1048,891,6117,6126,2501,6039,516,1023,5860,6222,6345,6348,6071,6353,5793,5643,6230,6134,138,377,2,130,131,1037,61,43,42,39,41,48,49,150])). % 182.23/182.15 cnf(6390,plain, % 182.23/182.15 (P15(f11(a4,a5),f14(f6(a5)))), % 182.23/182.15 inference(scs_inference,[],[74,1048,3547,891,6117,6126,2501,6039,516,5852,1023,5884,5860,6222,6345,6348,6071,6353,5793,5643,6230,6134,138,377,2,130,131,1037,61,43,42,39,41,48,49,150,3,122,1031])). % 182.23/182.15 cnf(6402,plain, % 182.23/182.15 (~P11(x64021,f11(a4,a5),f14(f6(a5)))), % 182.23/182.15 inference(scs_inference,[],[5852,5772,6383,6390,138,377,2,131])). % 182.23/182.15 cnf(6407,plain, % 182.23/182.15 (P11(f11(a4,a5),f19(f12(a5),f16(f6(a5),a5)),f16(f6(a5),a5))), % 182.23/182.15 inference(scs_inference,[],[389,6117,5852,6230,5772,1204,6370,6383,6390,6378,138,377,2,131,43,42,39])). % 182.23/182.15 cnf(6415,plain, % 182.23/182.15 (P5(f6(a5),x64151)+~E(f9(f14(a5),f6(a5),f12(a5)),x64151)), % 182.23/182.15 inference(scs_inference,[],[389,891,6117,5852,5848,6222,5711,6230,5772,2496,1204,5854,6370,6383,6390,6378,6219,138,377,2,131,43,42,39,41,49,150,3,62])). % 182.23/182.15 cnf(6429,plain, % 182.23/182.15 (P11(f11(a4,a5),f19(f12(a5),a4),a4)), % 182.23/182.15 inference(scs_inference,[],[6117,2510,6383,6189,6407,6326,138,377,2,131,39])). % 182.23/182.15 cnf(6438,plain, % 182.23/182.15 (P13(x64381,f14(a5))+~E(f10(f14(a5),f6(a5),f12(a5)),x64381)), % 182.23/182.15 inference(scs_inference,[],[389,6117,661,5852,5701,2510,6079,6370,6383,6390,6189,5912,6407,6213,6304,6326,138,377,2,131,39,41,49,3,43,55,42])). % 182.23/182.15 cnf(6445,plain, % 182.23/182.15 (~P11(f19(f12(a5),a4),f11(a4,a5),x64451)), % 182.23/182.15 inference(scs_inference,[],[6304,6429,138,377])). % 182.23/182.15 cnf(6447,plain, % 182.23/182.15 (E(f9(a4,x64471,x64472),f9(f16(f6(a5),a5),x64471,x64472))), % 182.23/182.15 inference(scs_inference,[],[2496,6304,6429,138,377,2])). % 182.23/182.15 cnf(6508,plain, % 182.23/182.15 (P11(f6(a5),f19(f11(a4,a5),f14(a5)),a4)), % 182.23/182.15 inference(scs_inference,[],[6112,3864,5675,6447,6129,5826,6346,6380,6065,138,2,131,49,42,39])). % 182.23/182.15 cnf(6561,plain, % 182.23/182.15 (~P11(x65611,f12(a5),f10(f14(a5),f6(a5),f12(a5)))), % 182.23/182.15 inference(scs_inference,[],[5853,6445,5993,2,138,131])). % 182.23/182.15 cnf(6611,plain, % 182.23/182.15 (~E(a4,f10(f14(a5),f6(a5),f12(a5)))), % 182.23/182.15 inference(scs_inference,[],[891,6561,5877,5895,6023,2,138,3,41])). % 182.23/182.15 cnf(6613,plain, % 182.23/182.15 (P13(x66131,a4)+~E(f10(f14(a5),f6(a5),f12(a5)),x66131)), % 182.23/182.15 inference(scs_inference,[],[891,6561,5877,6075,5895,6023,2,138,3,41,42])). % 182.23/182.15 cnf(6622,plain, % 182.23/182.15 (E(f15(f13(f16(f6(a5),a5)),f13(f16(f6(a5),a5))),f15(f13(a4),f13(a4)))), % 182.23/182.15 inference(scs_inference,[],[5879,5857,5876,6132,2,138,3])). % 182.23/182.15 cnf(6884,plain, % 182.23/182.15 (~P12(x68841,f11(a4,a5),f9(f14(a5),f6(a5),f12(a5)))), % 182.23/182.15 inference(scs_inference,[],[5897,6373,2,138])). % 182.23/182.15 cnf(6928,plain, % 182.23/182.15 (~P12(x69281,f11(a4,a5),f16(f11(a4,a5),a5))), % 182.23/182.15 inference(scs_inference,[],[6622,6136,2,138])). % 182.23/182.15 cnf(7588,plain, % 182.23/182.15 (P11(f12(a5),f13(a5),f14(a5))), % 182.23/182.15 inference(scs_inference,[],[1042,3515,41])). % 182.23/182.15 cnf(7589,plain, % 182.23/182.15 (P11(f6(a5),f13(a5),f14(a5))), % 182.23/182.15 inference(scs_inference,[],[1042,3515,1202,41,150])). % 182.23/182.15 cnf(7597,plain, % 182.23/182.15 (P11(f11(a4,a5),f13(a5),f14(a5))), % 182.23/182.15 inference(scs_inference,[],[6117,7589,39])). % 182.23/182.15 cnf(7823,plain, % 182.23/182.15 (E(f9(x78231,a4,x78232),f9(x78231,f14(a5),x78232))), % 182.23/182.15 inference(scs_inference,[],[6217,5793,6326,1042,6184,6183,1721,908,101,114,26])). % 182.23/182.15 cnf(7825,plain, % 182.23/182.15 (E(f9(a4,x78251,x78252),f9(f14(a5),x78251,x78252))), % 182.23/182.15 inference(scs_inference,[],[6217,5793,6326,1042,6184,6183,1721,908,101,114,26,19,25])). % 182.23/182.15 cnf(7827,plain, % 182.23/182.15 (E(f10(a4,x78271,x78272),f10(f14(a5),x78271,x78272))), % 182.23/182.15 inference(scs_inference,[],[6217,5793,6326,1042,6184,6183,1721,908,101,114,26,19,25,13,10])). % 182.23/182.15 cnf(7835,plain, % 182.23/182.15 (E(f14(a4),f14(f14(a5)))), % 182.23/182.15 inference(scs_inference,[],[6217,5793,6326,1042,6184,6183,1721,908,101,114,26,19,25,13,10,112,28,8,31,22,17,4])). % 182.23/182.15 cnf(7842,plain, % 182.23/182.15 (E(f22(a4,x78421,x78422),f22(f14(a5),x78421,x78422))), % 182.23/182.15 inference(scs_inference,[],[6217,5793,6326,1042,6184,6183,1721,908,101,114,26,19,25,13,10,112,28,8,31,22,17,4,36,35,20,14,29,30,16])). % 182.23/182.15 cnf(7858,plain, % 182.23/182.15 (E(f19(x78581,a4),f19(x78581,f14(a5)))), % 182.23/182.15 inference(scs_inference,[],[6217,5793,6326,1042,6184,6183,1721,908,101,114,26,19,25,13,10,112,28,8,31,22,17,4,36,35,20,14,29,30,16,12,11,34,32,27,9,5,37,18,15,378,23,6,21,33,24])). % 182.23/182.15 cnf(7861,plain, % 182.23/182.15 (E(f17(x78611,x78612,a4),f17(x78611,x78612,f14(a5)))), % 182.23/182.15 inference(scs_inference,[],[6217,5793,7597,6326,1042,6184,6183,1721,908,101,114,26,19,25,13,10,112,28,8,31,22,17,4,36,35,20,14,29,30,16,12,11,34,32,27,9,5,37,18,15,378,23,6,21,33,24,149,7])). % 182.23/182.15 cnf(7874,plain, % 182.23/182.15 (P1(f15(f11(a4,a5),a1))), % 182.23/182.15 inference(scs_inference,[],[6101,6217,5793,399,6310,7597,6326,1694,1042,6184,6183,1721,908,101,114,26,19,25,13,10,112,28,8,31,22,17,4,36,35,20,14,29,30,16,12,11,34,32,27,9,5,37,18,15,378,23,6,21,33,24,149,7,113,143,146,148,91,51,848,104])). % 182.23/182.15 cnf(7876,plain, % 182.23/182.15 (P17(f11(a4,a5),f22(f14(a5),f11(a4,a5),f13(a5)))), % 182.23/182.15 inference(scs_inference,[],[6101,6217,5793,399,6310,7597,6326,1694,1042,6184,6183,1721,908,101,114,26,19,25,13,10,112,28,8,31,22,17,4,36,35,20,14,29,30,16,12,11,34,32,27,9,5,37,18,15,378,23,6,21,33,24,149,7,113,143,146,148,91,51,848,104,144])). % 182.23/182.15 cnf(7878,plain, % 182.23/182.15 (P11(f11(a4,a5),f17(f11(a4,a5),f13(a5),f14(a5)),f14(a5))), % 182.23/182.15 inference(scs_inference,[],[6101,6115,6217,5793,399,6310,7597,6326,1694,1042,6184,6183,1721,908,101,114,26,19,25,13,10,112,28,8,31,22,17,4,36,35,20,14,29,30,16,12,11,34,32,27,9,5,37,18,15,378,23,6,21,33,24,149,7,113,143,146,148,91,51,848,104,144,152])). % 182.23/182.15 cnf(7880,plain, % 182.23/182.15 (P11(f17(f11(a4,a5),f13(a5),f14(a5)),f13(a5),f14(a5))), % 182.23/182.15 inference(scs_inference,[],[6101,6115,6217,5793,399,6310,7597,6326,1694,1042,6184,6183,1721,908,101,114,26,19,25,13,10,112,28,8,31,22,17,4,36,35,20,14,29,30,16,12,11,34,32,27,9,5,37,18,15,378,23,6,21,33,24,149,7,113,143,146,148,91,51,848,104,144,152,153])). % 182.23/182.15 cnf(7885,plain, % 182.23/182.15 (~P16(f19(f11(a4,a5),f14(a5)),a5)), % 182.23/182.15 inference(scs_inference,[],[74,6101,6115,6217,5793,5986,6508,399,6310,7597,6326,1694,1042,6184,6183,1721,908,101,114,26,19,25,13,10,112,28,8,31,22,17,4,36,35,20,14,29,30,16,12,11,34,32,27,9,5,37,18,15,378,23,6,21,33,24,149,7,113,143,146,148,91,51,848,104,144,152,153,58,89,136])). % 182.23/182.15 cnf(7888,plain, % 182.23/182.15 (~P15(f22(a4,f6(a5),f12(a5)),x78881)), % 182.23/182.15 inference(scs_inference,[],[74,6101,6115,6324,6217,5793,5986,6052,6508,399,6310,7597,6326,1694,1042,6184,6183,1721,908,101,114,26,19,25,13,10,112,28,8,31,22,17,4,36,35,20,14,29,30,16,12,11,34,32,27,9,5,37,18,15,378,23,6,21,33,24,149,7,113,143,146,148,91,51,848,104,144,152,153,58,89,136,57,54])). % 182.23/182.15 cnf(7898,plain, % 182.23/182.15 (P15(f6(a5),f16(f6(a5),a5))), % 182.23/182.15 inference(scs_inference,[],[74,5829,6101,6115,6225,6041,6324,6217,6071,6402,5793,6306,6043,5986,6052,6508,399,6310,7597,6326,1694,1042,3511,6184,6183,1721,908,101,114,26,19,25,13,10,112,28,8,31,22,17,4,36,35,20,14,29,30,16,12,11,34,32,27,9,5,37,18,15,378,23,6,21,33,24,149,7,113,143,146,148,91,51,848,104,144,152,153,58,89,136,57,54,64,40,46,50,48,44,88,45,110])). % 182.23/182.15 cnf(7900,plain, % 182.23/182.15 (~P9(f11(a4,a5),f22(f14(a5),f6(a5),f12(a5)))), % 182.23/182.15 inference(scs_inference,[],[74,5829,6101,6115,6225,6041,6324,6217,6071,6402,5793,6306,6043,5986,6052,5715,6508,6344,399,6310,7597,6326,1694,1042,3511,6184,6183,1721,908,101,114,26,19,25,13,10,112,28,8,31,22,17,4,36,35,20,14,29,30,16,12,11,34,32,27,9,5,37,18,15,378,23,6,21,33,24,149,7,113,143,146,148,91,51,848,104,144,152,153,58,89,136,57,54,64,40,46,50,48,44,88,45,110,137])). % 182.23/182.15 cnf(7902,plain, % 182.23/182.15 (~P10(f17(f11(a4,a5),f13(a5),f14(a5)),f14(a5))), % 182.23/182.15 inference(scs_inference,[],[74,5829,6101,6115,6225,6041,6324,6217,6071,6402,5793,6306,6043,5986,6052,5715,6508,6344,399,6310,7597,6326,1694,1042,3511,6184,6183,1721,908,101,114,26,19,25,13,10,112,28,8,31,22,17,4,36,35,20,14,29,30,16,12,11,34,32,27,9,5,37,18,15,378,23,6,21,33,24,149,7,113,143,146,148,91,51,848,104,144,152,153,58,89,136,57,54,64,40,46,50,48,44,88,45,110,137,132])). % 182.23/182.15 cnf(7904,plain, % 182.23/182.15 (~P14(f19(f11(a4,a5),f14(a5)),f6(a5))), % 182.23/182.15 inference(scs_inference,[],[74,5829,6101,6115,6225,6041,6324,6217,6071,6402,5793,6306,6043,5986,6052,5715,6508,6344,399,6310,7597,6326,1694,1042,3511,6184,6183,1721,908,101,114,26,19,25,13,10,112,28,8,31,22,17,4,36,35,20,14,29,30,16,12,11,34,32,27,9,5,37,18,15,378,23,6,21,33,24,149,7,113,143,146,148,91,51,848,104,144,152,153,58,89,136,57,54,64,40,46,50,48,44,88,45,110,137,132,358])). % 182.23/182.15 cnf(7909,plain, % 182.23/182.15 (~P6(f19(f11(a4,a5),f14(a5)),a2)), % 182.23/182.15 inference(scs_inference,[],[74,5829,6101,6115,6225,6041,6095,6324,6217,6071,6402,5793,6306,6043,6232,5986,6052,5715,6508,6344,399,6310,7597,6326,1694,3513,1203,1042,3511,6184,6183,1721,908,101,114,26,19,25,13,10,112,28,8,31,22,17,4,36,35,20,14,29,30,16,12,11,34,32,27,9,5,37,18,15,378,23,6,21,33,24,149,7,113,143,146,148,91,51,848,104,144,152,153,58,89,136,57,54,64,40,46,50,48,44,88,45,110,137,132,358,124,59,139])). % 182.23/182.15 cnf(7915,plain, % 182.23/182.15 (P5(f11(a4,a5),f9(f14(a5),f11(a4,a5),f13(a5)))), % 182.23/182.15 inference(scs_inference,[],[74,5829,6101,6115,6225,6041,6095,6324,6217,6071,6402,5793,6306,6043,6232,5986,6052,5715,6508,6344,399,6310,7597,6326,1694,6121,3513,1203,1042,3511,6184,6183,1721,908,101,114,26,19,25,13,10,112,28,8,31,22,17,4,36,35,20,14,29,30,16,12,11,34,32,27,9,5,37,18,15,378,23,6,21,33,24,149,7,113,143,146,148,91,51,848,104,144,152,153,58,89,136,57,54,64,40,46,50,48,44,88,45,110,137,132,358,124,59,139,94,140,145])). % 182.23/182.15 cnf(7917,plain, % 182.23/182.15 (~P1(f16(f11(a4,a5),a5))), % 182.23/182.15 inference(scs_inference,[],[74,5829,6101,6115,6225,6041,6095,6324,6217,6071,6402,5793,6306,6043,6232,5721,5986,6052,5715,6508,6344,399,6310,7597,6326,1694,154,6121,3513,1203,1042,3511,6184,6183,1721,908,101,114,26,19,25,13,10,112,28,8,31,22,17,4,36,35,20,14,29,30,16,12,11,34,32,27,9,5,37,18,15,378,23,6,21,33,24,149,7,113,143,146,148,91,51,848,104,144,152,153,58,89,136,57,54,64,40,46,50,48,44,88,45,110,137,132,358,124,59,139,94,140,145,93])). % 182.23/182.15 cnf(7922,plain, % 182.23/182.15 (~P8(f19(f12(a5),a4),f11(a4,a5))), % 182.23/182.15 inference(scs_inference,[],[74,69,5829,6101,6115,6225,6041,6095,6324,6217,6071,6154,6402,5793,6306,6043,6232,6233,5721,5986,6052,5715,6508,6344,399,6310,7597,6326,1694,154,6121,3513,1203,1042,3511,6184,6183,1721,908,101,114,26,19,25,13,10,112,28,8,31,22,17,4,36,35,20,14,29,30,16,12,11,34,32,27,9,5,37,18,15,378,23,6,21,33,24,149,7,113,143,146,148,91,51,848,104,144,152,153,58,89,136,57,54,64,40,46,50,48,44,88,45,110,137,132,358,124,59,139,94,140,145,93,115,61,67])). % 182.23/182.15 cnf(7925,plain, % 182.23/182.15 (~P14(f19(f12(a5),a4),f6(a5))), % 182.23/182.15 inference(scs_inference,[],[74,69,5829,6101,6115,6225,6041,6095,6324,6217,6071,6154,6402,5791,5793,6306,6043,6232,6233,5721,5986,6052,6018,5715,6508,6344,399,6310,7597,6326,1694,154,6121,6088,3513,1203,1042,3511,6184,6183,1721,908,101,114,26,19,25,13,10,112,28,8,31,22,17,4,36,35,20,14,29,30,16,12,11,34,32,27,9,5,37,18,15,378,23,6,21,33,24,149,7,113,143,146,148,91,51,848,104,144,152,153,58,89,136,57,54,64,40,46,50,48,44,88,45,110,137,132,358,124,59,139,94,140,145,93,115,61,67,150,63])). % 182.23/182.15 cnf(7926,plain, % 182.23/182.15 (P1(f14(f13(a5)))), % 182.23/182.15 inference(scs_inference,[],[74,69,5829,6101,6115,6225,6041,6095,6324,6217,6071,6154,6402,5791,5793,6306,6043,6232,6233,5721,5986,6052,6018,5715,6508,6344,399,6310,7597,6326,1694,3581,154,6121,6088,3513,1203,1042,3511,6184,6183,1721,908,101,114,26,19,25,13,10,112,28,8,31,22,17,4,36,35,20,14,29,30,16,12,11,34,32,27,9,5,37,18,15,378,23,6,21,33,24,149,7,113,143,146,148,91,51,848,104,144,152,153,58,89,136,57,54,64,40,46,50,48,44,88,45,110,137,132,358,124,59,139,94,140,145,93,115,61,67,150,63,92])). % 182.23/182.15 cnf(7928,plain, % 182.23/182.15 (P3(f19(f12(a5),f14(a5)))), % 182.23/182.15 inference(scs_inference,[],[74,69,5829,6101,6115,6225,6041,6095,6324,6217,5933,6071,6154,6402,5791,5793,6306,6043,6232,6233,5721,5986,6052,6018,5715,6508,6344,399,6310,7597,6326,1694,3581,154,6121,6088,3513,1203,1042,3511,6184,6183,1721,908,101,114,26,19,25,13,10,112,28,8,31,22,17,4,36,35,20,14,29,30,16,12,11,34,32,27,9,5,37,18,15,378,23,6,21,33,24,149,7,113,143,146,148,91,51,848,104,144,152,153,58,89,136,57,54,64,40,46,50,48,44,88,45,110,137,132,358,124,59,139,94,140,145,93,115,61,67,150,63,92,82])). % 182.23/182.15 cnf(7931,plain, % 182.23/182.15 (~P8(f19(f11(a4,a5),f14(a5)),f6(a5))), % 182.23/182.15 inference(scs_inference,[],[74,69,5829,6101,6115,6225,6041,6095,6324,6217,5933,6071,6154,6402,5791,5793,6306,6043,6232,6233,5721,5986,6052,6018,5715,6508,6344,399,6310,7597,6326,1694,3581,154,6121,6088,3513,1203,1042,3511,6184,6183,1721,908,101,114,26,19,25,13,10,112,28,8,31,22,17,4,36,35,20,14,29,30,16,12,11,34,32,27,9,5,37,18,15,378,23,6,21,33,24,149,7,113,143,146,148,91,51,848,104,144,152,153,58,89,136,57,54,64,40,46,50,48,44,88,45,110,137,132,358,124,59,139,94,140,145,93,115,61,67,150,63,92,82,694,285])). % 182.23/182.15 cnf(7933,plain, % 182.23/182.16 (P6(f11(a4,a5),f15(f11(a4,a5),a1))), % 182.23/182.16 inference(scs_inference,[],[74,69,5829,6101,6115,6225,6041,6095,6324,6217,5933,6071,6154,6402,5791,5793,6306,6043,6232,6233,5721,5986,6052,6018,5715,6508,6344,399,6310,7597,6326,1694,3581,154,6121,6088,3513,1203,1042,3511,6184,6183,1721,908,101,114,26,19,25,13,10,112,28,8,31,22,17,4,36,35,20,14,29,30,16,12,11,34,32,27,9,5,37,18,15,378,23,6,21,33,24,149,7,113,143,146,148,91,51,848,104,144,152,153,58,89,136,57,54,64,40,46,50,48,44,88,45,110,137,132,358,124,59,139,94,140,145,93,115,61,67,150,63,92,82,694,285,109])). % 182.23/182.16 cnf(7936,plain, % 182.23/182.16 (~P11(f17(f11(a4,a5),f13(a5),f14(a5)),f11(a4,a5),x79361)), % 182.23/182.16 inference(scs_inference,[],[74,71,69,5829,6101,6115,6225,6041,6095,6324,6217,5933,6071,6154,6402,5791,5793,6306,6043,6232,6233,5721,5986,6052,6018,5715,400,6508,6344,399,6310,7597,6326,1694,3581,154,6121,6088,3513,1203,1042,3511,6184,6183,1721,908,101,114,26,19,25,13,10,112,28,8,31,22,17,4,36,35,20,14,29,30,16,12,11,34,32,27,9,5,37,18,15,378,23,6,21,33,24,149,7,113,143,146,148,91,51,848,104,144,152,153,58,89,136,57,54,64,40,46,50,48,44,88,45,110,137,132,358,124,59,139,94,140,145,93,115,61,67,150,63,92,82,694,285,109,38,377])). % 182.23/182.16 cnf(7938,plain, % 182.23/182.16 (~P6(a5,f10(a4,f12(a5),f13(a5)))), % 182.23/182.16 inference(scs_inference,[],[74,71,69,5829,6101,6115,6225,6041,6095,6313,6324,6217,5933,6071,6154,6402,5791,5793,6306,6043,6232,6233,5721,5986,6052,6018,5715,400,6508,6344,399,6310,7597,6326,1694,3581,154,6121,6088,3513,1203,1042,3511,6184,6183,1721,908,101,114,26,19,25,13,10,112,28,8,31,22,17,4,36,35,20,14,29,30,16,12,11,34,32,27,9,5,37,18,15,378,23,6,21,33,24,149,7,113,143,146,148,91,51,848,104,144,152,153,58,89,136,57,54,64,40,46,50,48,44,88,45,110,137,132,358,124,59,139,94,140,145,93,115,61,67,150,63,92,82,694,285,109,38,377,103])). % 182.23/182.16 cnf(7940,plain, % 182.23/182.16 (P14(f6(a5),f19(f11(a4,a5),f14(a5)))), % 182.23/182.16 inference(scs_inference,[],[74,71,69,5829,6101,6115,6225,6041,6095,6313,6324,6217,5933,6071,6154,6402,5791,5793,6306,6043,6232,6233,5721,5986,6052,6018,5715,400,6508,6344,399,6310,7597,6326,1694,3581,154,6121,6088,3513,1203,1042,3511,6184,6183,1721,908,101,114,26,19,25,13,10,112,28,8,31,22,17,4,36,35,20,14,29,30,16,12,11,34,32,27,9,5,37,18,15,378,23,6,21,33,24,149,7,113,143,146,148,91,51,848,104,144,152,153,58,89,136,57,54,64,40,46,50,48,44,88,45,110,137,132,358,124,59,139,94,140,145,93,115,61,67,150,63,92,82,694,285,109,38,377,103,130])). % 182.23/182.16 cnf(7942,plain, % 182.23/182.16 (P6(f22(f14(a5),f11(a4,a5),f13(a5)),f14(a5))), % 182.23/182.16 inference(scs_inference,[],[74,71,69,5829,6101,6115,6225,6041,6095,6313,6324,6217,5933,6071,6154,6402,5791,5793,6306,6043,6232,6233,5721,5986,6052,6018,5715,400,6508,6344,399,6310,7597,6326,1694,3581,154,6121,6088,3513,1203,1042,3511,6184,6183,1721,908,101,114,26,19,25,13,10,112,28,8,31,22,17,4,36,35,20,14,29,30,16,12,11,34,32,27,9,5,37,18,15,378,23,6,21,33,24,149,7,113,143,146,148,91,51,848,104,144,152,153,58,89,136,57,54,64,40,46,50,48,44,88,45,110,137,132,358,124,59,139,94,140,145,93,115,61,67,150,63,92,82,694,285,109,38,377,103,130,147])). % 182.23/182.16 cnf(7944,plain, % 182.23/182.16 (~P15(f19(f11(a4,a5),f14(a5)),a4)), % 182.23/182.16 inference(scs_inference,[],[74,71,69,5829,6101,6115,6225,6041,6095,6313,6324,6217,5933,6071,6154,6402,5791,5793,6306,6043,6232,6233,5721,5986,6052,6018,5715,400,6508,6344,399,6310,7597,6326,1694,3581,154,6121,6088,3513,1203,1042,3511,6184,6183,1721,908,101,114,26,19,25,13,10,112,28,8,31,22,17,4,36,35,20,14,29,30,16,12,11,34,32,27,9,5,37,18,15,378,23,6,21,33,24,149,7,113,143,146,148,91,51,848,104,144,152,153,58,89,136,57,54,64,40,46,50,48,44,88,45,110,137,132,358,124,59,139,94,140,145,93,115,61,67,150,63,92,82,694,285,109,38,377,103,130,147,131])). % 182.23/182.16 cnf(7976,plain, % 182.23/182.16 (P11(f11(a4,a5),f17(f11(a4,a5),f13(a5),a4),a4)), % 182.23/182.16 inference(scs_inference,[],[6225,6312,152])). % 182.23/182.16 cnf(7985,plain, % 182.23/182.16 (E(f10(x79851,x79852,f14(a5)),f10(x79851,x79852,a4))), % 182.23/182.16 inference(scs_inference,[],[7878,6225,7589,6242,6312,1048,152,148,114,358,14,12])). % 182.23/182.16 cnf(7990,plain, % 182.23/182.16 (E(f10(x79901,f14(a5),x79902),f10(x79901,a4,x79902))), % 182.23/182.16 inference(scs_inference,[],[7915,7878,6225,1025,7589,6242,6312,1048,152,148,114,358,14,12,101,9,33,11])). % 182.23/182.16 cnf(7992,plain, % 182.23/182.16 (E(f17(x79921,x79922,f14(a5)),f17(x79921,x79922,a4))), % 182.23/182.16 inference(scs_inference,[],[7915,7878,6225,1025,7589,6242,6312,1048,152,148,114,358,14,12,101,9,33,11,25,7])). % 182.23/182.16 cnf(7996,plain, % 182.23/182.16 (P11(f17(f6(a5),f13(a5),f14(a5)),f13(a5),f14(a5))), % 182.23/182.16 inference(scs_inference,[],[7915,7878,6225,1025,6383,7589,6242,3584,6312,3513,3511,1048,152,148,114,358,14,12,101,9,33,11,25,7,27,139,153])). % 182.23/182.16 cnf(8015,plain, % 182.23/182.16 (E(f11(f14(a5),x80151),f11(a4,x80151))), % 182.23/182.16 inference(scs_inference,[],[7888,7898,7915,7878,6225,1025,6383,7589,6242,3584,6312,3513,3543,3511,1048,152,148,114,358,14,12,101,9,33,11,25,7,27,139,153,112,146,36,144,30,88,113,18,54,17,34,32])). % 182.23/182.16 cnf(8017,plain, % 182.23/182.16 (E(f9(a4,x80171,x80172),f9(f14(a5),x80171,x80172))), % 182.23/182.16 inference(rename_variables,[],[7825])). % 182.23/182.16 cnf(8018,plain, % 182.23/182.16 (~P14(f19(f11(a4,a5),f14(a5)),f11(a4,a5))), % 182.23/182.16 inference(scs_inference,[],[6884,7888,7898,7915,7825,7878,7904,6225,1025,6383,7589,6242,3584,6312,3513,3543,3511,1048,6183,152,148,114,358,14,12,101,9,33,11,25,7,27,139,153,112,146,36,144,30,88,113,18,54,17,34,32,46,64])). % 182.23/182.16 cnf(8029,plain, % 182.23/182.16 (E(f19(x80291,a4),f19(x80291,f14(a5)))), % 182.23/182.16 inference(rename_variables,[],[7858])). % 182.23/182.16 cnf(8032,plain, % 182.23/182.16 (P16(f11(a4,a5),f22(f14(a5),f11(a4,a5),f13(a5)))), % 182.23/182.16 inference(scs_inference,[],[6884,7888,7898,7900,7915,7876,7825,7858,7878,7904,7885,7942,6225,1025,6383,7589,6242,3584,6312,3513,3543,1203,3511,1048,6184,6183,152,148,114,358,14,12,101,9,33,11,25,7,27,139,153,112,146,36,144,30,88,113,18,54,17,34,32,46,64,143,22,35,19,57,16,26,13,59,104,124])). % 182.23/182.16 cnf(8037,plain, % 182.23/182.16 (E(f22(a4,x80371,x80372),f22(f14(a5),x80371,x80372))), % 182.23/182.16 inference(rename_variables,[],[7842])). % 182.23/182.16 cnf(8042,plain, % 182.23/182.16 (E(f19(x80421,a4),f19(x80421,f14(a5)))), % 182.23/182.16 inference(rename_variables,[],[7858])). % 182.23/182.16 cnf(8045,plain, % 182.23/182.16 (~P9(f11(a4,a5),f22(f14(a5),f11(a4,a5),f13(a5)))), % 182.23/182.16 inference(scs_inference,[],[6884,7888,7898,7900,7915,7876,7825,7842,7858,8029,7878,7904,7885,7942,7880,7909,6225,1025,6302,6383,7589,6242,3584,6312,3513,3543,1203,3511,1048,6184,6183,152,148,114,358,14,12,101,9,33,11,25,7,27,139,153,112,146,36,144,30,88,113,18,54,17,34,32,46,64,143,22,35,19,57,16,26,13,59,104,124,149,40,136,15,48,145,137])). % 182.23/182.16 cnf(8050,plain, % 182.23/182.16 (E(f10(f14(a5),x80501,x80502),f10(a4,x80501,x80502))), % 182.23/182.16 inference(scs_inference,[],[6884,7888,7898,7900,7915,7876,7825,7842,7858,8029,7878,7904,7885,7942,7880,7909,6225,1025,6302,6383,7589,6242,3584,6312,3513,3543,1203,3511,1048,6184,6183,152,148,114,358,14,12,101,9,33,11,25,7,27,139,153,112,146,36,144,30,88,113,18,54,17,34,32,46,64,143,22,35,19,57,16,26,13,59,104,124,149,40,136,15,48,145,137,28,31,37,10])). % 182.23/182.16 cnf(8056,plain, % 182.23/182.16 (E(f19(x80561,f14(a5)),f19(x80561,a4))), % 182.23/182.16 inference(scs_inference,[],[6884,7888,7898,7900,7915,7876,7825,7842,7858,8029,7878,7904,7885,7940,7942,7880,7909,6225,1025,6302,6383,7589,6242,3584,6312,3513,3543,1203,3511,1048,6184,6183,152,148,114,358,14,12,101,9,33,11,25,7,27,139,153,112,146,36,144,30,88,113,18,54,17,34,32,46,64,143,22,35,19,57,16,26,13,59,104,124,149,40,136,15,48,145,137,28,31,37,10,29,20,5,85,24])). % 182.23/182.16 cnf(8057,plain, % 182.23/182.16 (E(f6(f14(a5)),f6(a4))), % 182.23/182.16 inference(scs_inference,[],[6884,7888,7898,7900,7915,7876,7825,7842,7858,8029,7878,7904,7885,7940,7942,7880,7909,6225,1025,6302,6383,7589,6242,3584,6312,3513,3543,1203,3511,1048,6184,6183,152,148,114,358,14,12,101,9,33,11,25,7,27,139,153,112,146,36,144,30,88,113,18,54,17,34,32,46,64,143,22,35,19,57,16,26,13,59,104,124,149,40,136,15,48,145,137,28,31,37,10,29,20,5,85,24,8])). % 182.23/182.16 cnf(8062,plain, % 182.23/182.16 (P8(f6(a5),f19(f11(a4,a5),f14(a5)))), % 182.23/182.16 inference(scs_inference,[],[6175,6884,7888,7898,7900,7915,7876,7825,7842,7858,8029,7878,7904,7885,7940,7942,7880,7909,6225,1025,6302,6383,7589,6242,3584,6312,3513,3543,1203,3511,1048,6184,6183,152,148,114,358,14,12,101,9,33,11,25,7,27,139,153,112,146,36,144,30,88,113,18,54,17,34,32,46,64,143,22,35,19,57,16,26,13,59,104,124,149,40,136,15,48,145,137,28,31,37,10,29,20,5,85,24,8,21,44,23,6,94])). % 182.23/182.16 cnf(8067,plain, % 182.23/182.16 (E(f17(x80671,x80672,a4),f17(x80671,x80672,f14(a5)))), % 182.23/182.16 inference(rename_variables,[],[7861])). % 182.23/182.16 cnf(8074,plain, % 182.23/182.16 (~P11(f17(f11(a4,a5),f13(a5),f14(a5)),f6(a5),f14(a5))), % 182.23/182.16 inference(scs_inference,[],[72,6045,6175,6884,7888,7898,7900,7915,7876,7825,7842,8037,7861,7858,8029,7878,7904,7885,7940,7942,7902,7880,7909,6225,6120,1025,6302,6383,5989,7589,6242,3584,6312,3513,3543,1203,3511,1048,6184,6183,152,148,114,358,14,12,101,9,33,11,25,7,27,139,153,112,146,36,144,30,88,113,18,54,17,34,32,46,64,143,22,35,19,57,16,26,13,59,104,124,149,40,136,15,48,145,137,28,31,37,10,29,20,5,85,24,8,21,44,23,6,94,45,50,140,93,82,150])). % 182.23/182.16 cnf(8076,plain, % 182.23/182.16 (~P3(f22(f14(a5),f11(a4,a5),f13(a5)))), % 182.23/182.16 inference(scs_inference,[],[72,6045,6175,6884,7888,7898,7900,7915,7876,7825,7842,8037,7861,7858,8029,7878,7904,7885,7940,7942,7902,7880,7909,6225,6120,1025,1051,6302,6383,5989,7589,6242,3584,6312,3513,3543,1203,3511,1048,6184,6183,152,148,114,358,14,12,101,9,33,11,25,7,27,139,153,112,146,36,144,30,88,113,18,54,17,34,32,46,64,143,22,35,19,57,16,26,13,59,104,124,149,40,136,15,48,145,137,28,31,37,10,29,20,5,85,24,8,21,44,23,6,94,45,50,140,93,82,150,92])). % 182.23/182.16 cnf(8078,plain, % 182.23/182.16 (~P8(f19(f11(a4,a5),a4),f6(a5))), % 182.23/182.16 inference(scs_inference,[],[72,6045,6175,6884,7888,7898,7900,7915,7876,7825,7842,8037,7861,7858,8029,8042,7878,7904,7931,7885,7940,7942,7902,7880,7909,6225,6120,1025,1051,6302,6383,5989,7589,6242,3584,6312,3513,3543,1203,3511,1048,6184,6183,152,148,114,358,14,12,101,9,33,11,25,7,27,139,153,112,146,36,144,30,88,113,18,54,17,34,32,46,64,143,22,35,19,57,16,26,13,59,104,124,149,40,136,15,48,145,137,28,31,37,10,29,20,5,85,24,8,21,44,23,6,94,45,50,140,93,82,150,92,67])). % 182.23/182.16 cnf(8080,plain, % 182.23/182.16 (~P8(f17(f11(a4,a5),f13(a5),f14(a5)),f11(a4,a5))), % 182.23/182.16 inference(scs_inference,[],[72,6045,6175,6884,7888,7898,7900,7915,7876,7825,7842,8037,7861,7858,8029,8042,7878,7904,7931,7885,7940,7942,7902,7880,7909,6225,6120,1025,1051,6302,6383,5989,7589,6242,3584,6312,3513,3543,1203,3511,1048,6184,6183,152,148,114,358,14,12,101,9,33,11,25,7,27,139,153,112,146,36,144,30,88,113,18,54,17,34,32,46,64,143,22,35,19,57,16,26,13,59,104,124,149,40,136,15,48,145,137,28,31,37,10,29,20,5,85,24,8,21,44,23,6,94,45,50,140,93,82,150,92,67,285])). % 182.23/182.16 cnf(8083,plain, % 182.23/182.16 (~P11(f13(a5),f17(f11(a4,a5),f13(a5),f14(a5)),x80831)), % 182.23/182.16 inference(scs_inference,[],[72,81,6045,6175,6884,7888,7898,7900,7915,7876,7825,7842,8037,7861,7874,7858,8029,8042,7878,7904,7931,7885,7940,7942,7902,7880,7909,6225,6120,1025,1051,6302,6383,5989,7589,6242,3584,6312,3513,3543,1203,3511,1048,6184,6183,152,148,114,358,14,12,101,9,33,11,25,7,27,139,153,112,146,36,144,30,88,113,18,54,17,34,32,46,64,143,22,35,19,57,16,26,13,59,104,124,149,40,136,15,48,145,137,28,31,37,10,29,20,5,85,24,8,21,44,23,6,94,45,50,140,93,82,150,92,67,285,38,377])). % 182.23/182.16 cnf(8085,plain, % 182.23/182.16 (~P6(f11(a4,a5),a23)), % 182.23/182.16 inference(scs_inference,[],[72,81,5802,6045,6175,6884,7888,7898,7900,7915,7876,7825,7842,8037,7861,7874,7858,8029,8042,7878,7904,7931,7885,7940,7942,7902,7880,7909,6225,6120,1025,1051,6208,6302,6383,5989,7589,6242,3584,6312,3513,3543,1203,3511,1048,6184,6183,152,148,114,358,14,12,101,9,33,11,25,7,27,139,153,112,146,36,144,30,88,113,18,54,17,34,32,46,64,143,22,35,19,57,16,26,13,59,104,124,149,40,136,15,48,145,137,28,31,37,10,29,20,5,85,24,8,21,44,23,6,94,45,50,140,93,82,150,92,67,285,38,377,103])). % 182.23/182.16 cnf(8087,plain, % 182.23/182.16 (P6(f6(a5),f15(f6(a5),a1))), % 182.23/182.16 inference(scs_inference,[],[72,81,5802,6045,6175,6884,7888,7898,7900,7915,7876,7825,7842,8037,7861,7874,7858,8029,8042,7878,7904,7931,7885,7940,7942,7902,7880,7909,6225,6120,1025,1051,6208,6302,6383,5989,7589,6242,3584,6312,3513,3543,1203,3511,1048,6184,6183,152,148,114,358,14,12,101,9,33,11,25,7,27,139,153,112,146,36,144,30,88,113,18,54,17,34,32,46,64,143,22,35,19,57,16,26,13,59,104,124,149,40,136,15,48,145,137,28,31,37,10,29,20,5,85,24,8,21,44,23,6,94,45,50,140,93,82,150,92,67,285,38,377,103,109])). % 182.23/182.16 cnf(8090,plain, % 182.23/182.16 (P6(f22(f14(a5),f6(a5),f13(a5)),f14(a5))), % 182.23/182.16 inference(scs_inference,[],[72,81,7922,5802,6045,6175,6884,7888,7898,7900,7915,7876,7825,7842,8037,7861,7874,7858,8029,8042,7878,7904,7931,7885,7940,7942,7902,7880,7909,6225,6120,1025,1051,6208,6302,6383,5989,7589,6242,3584,6312,3513,3543,1203,3511,1048,6184,6183,152,148,114,358,14,12,101,9,33,11,25,7,27,139,153,112,146,36,144,30,88,113,18,54,17,34,32,46,64,143,22,35,19,57,16,26,13,59,104,124,149,40,136,15,48,145,137,28,31,37,10,29,20,5,85,24,8,21,44,23,6,94,45,50,140,93,82,150,92,67,285,38,377,103,109,68,147])). % 182.23/182.16 cnf(8092,plain, % 182.23/182.16 (P14(f11(a4,a5),f17(f11(a4,a5),f13(a5),f14(a5)))), % 182.23/182.16 inference(scs_inference,[],[72,81,7922,5802,6045,6175,6884,7888,7898,7900,7915,7876,7825,7842,8037,7861,7874,7858,8029,8042,7878,7904,7931,7885,7940,7942,7902,7880,7909,6225,6120,1025,1051,6208,6302,6383,5989,7589,6242,3584,6312,3513,3543,1203,3511,1048,6184,6183,152,148,114,358,14,12,101,9,33,11,25,7,27,139,153,112,146,36,144,30,88,113,18,54,17,34,32,46,64,143,22,35,19,57,16,26,13,59,104,124,149,40,136,15,48,145,137,28,31,37,10,29,20,5,85,24,8,21,44,23,6,94,45,50,140,93,82,150,92,67,285,38,377,103,109,68,147,130])). % 182.23/182.16 cnf(8094,plain, % 182.23/182.16 (~P15(f17(f11(a4,a5),f13(a5),f14(a5)),f14(a5))), % 182.23/182.16 inference(scs_inference,[],[72,81,7922,5802,6045,6175,6884,7888,7898,7900,7915,7876,7825,7842,8037,7861,7874,7858,8029,8042,7878,7904,7931,7885,7940,7942,7902,7880,7909,6225,6120,1025,1051,6208,6302,6383,5989,7589,6242,3584,6312,3513,3543,1203,3511,1048,6184,6183,152,148,114,358,14,12,101,9,33,11,25,7,27,139,153,112,146,36,144,30,88,113,18,54,17,34,32,46,64,143,22,35,19,57,16,26,13,59,104,124,149,40,136,15,48,145,137,28,31,37,10,29,20,5,85,24,8,21,44,23,6,94,45,50,140,93,82,150,92,67,285,38,377,103,109,68,147,130,131])). % 182.23/182.16 cnf(8102,plain, % 182.23/182.16 (~E(a23,f14(f6(a5)))), % 182.23/182.16 inference(scs_inference,[],[72,81,7922,5802,6045,6175,6884,7888,7898,7900,6113,7915,7876,7933,7825,7827,7842,8037,7861,7874,7858,8029,8042,7878,7904,7931,7885,7940,7942,7902,7880,7909,6225,6120,6561,1025,1051,6208,6037,6302,6383,5989,7589,6242,3584,6312,3513,3543,1203,3511,1048,6184,6183,152,148,114,358,14,12,101,9,33,11,25,7,27,139,153,112,146,36,144,30,88,113,18,54,17,34,32,46,64,143,22,35,19,57,16,26,13,59,104,124,149,40,136,15,48,145,137,28,31,37,10,29,20,5,85,24,8,21,44,23,6,94,45,50,140,93,82,150,92,67,285,38,377,103,109,68,147,130,131,53,41,49,90,2])). % 182.23/182.16 cnf(8110,plain, % 182.23/182.16 (P5(f6(a5),f9(a4,f6(a5),f12(a5)))), % 182.23/182.16 inference(scs_inference,[],[72,81,7922,5802,6045,6175,6884,7888,7898,7900,6113,7936,7915,7876,7933,7823,7825,8017,7827,7842,8037,7861,8067,7874,7858,8029,8042,7878,7904,7931,7885,7940,7942,7902,7880,7909,6225,6120,6561,1025,1051,6208,6037,6302,6383,5989,7589,6242,3584,6312,3513,3543,1203,3511,1048,6184,6183,152,148,114,358,14,12,101,9,33,11,25,7,27,139,153,112,146,36,144,30,88,113,18,54,17,34,32,46,64,143,22,35,19,57,16,26,13,59,104,124,149,40,136,15,48,145,137,28,31,37,10,29,20,5,85,24,8,21,44,23,6,94,45,50,140,93,82,150,92,67,285,38,377,103,109,68,147,130,131,53,41,49,90,2,3,39,6613,6438,6415])). % 182.23/182.16 cnf(8121,plain, % 182.23/182.16 (~P10(f17(f6(a5),f13(a5),f14(a5)),f14(a5))), % 182.23/182.16 inference(scs_inference,[],[72,81,7922,5802,6045,6175,6884,7888,7898,7900,6113,7936,7915,7876,7933,7823,7825,8017,7827,7842,8037,7861,8067,7874,7858,8029,8042,7878,7904,7931,7885,7940,7942,7902,7880,7909,6225,6120,6561,1025,1051,6208,6037,6302,6383,5989,7589,6242,3584,6312,3513,3543,1203,3511,1048,6184,6183,152,148,114,358,14,12,101,9,33,11,25,7,27,139,153,112,146,36,144,30,88,113,18,54,17,34,32,46,64,143,22,35,19,57,16,26,13,59,104,124,149,40,136,15,48,145,137,28,31,37,10,29,20,5,85,24,8,21,44,23,6,94,45,50,140,93,82,150,92,67,285,38,377,103,109,68,147,130,131,53,41,49,90,2,3,39,6613,6438,6415,5175,4903,1029,4178,4206,1020,65,132])). % 182.23/182.16 cnf(8133,plain, % 182.23/182.16 (P11(f6(a5),f17(f6(a5),f13(a5),f14(a5)),f14(a5))), % 182.23/182.16 inference(scs_inference,[],[7589,3584,152])). % 182.23/182.16 cnf(8143,plain, % 182.23/182.16 (P11(f17(f11(a4,a5),f13(a5),a4),f13(a5),a4)), % 182.23/182.16 inference(scs_inference,[],[7996,8110,6225,6217,7589,3584,7588,6312,3630,152,101,148,358,114,153])). % 182.23/182.16 cnf(8156,plain, % 182.23/182.16 (E(f17(x81561,x81562,a4),f17(x81561,x81562,f14(a5)))), % 182.23/182.16 inference(rename_variables,[],[7861])). % 182.23/182.16 cnf(8157,plain, % 182.23/182.16 (P14(f11(a4,a5),f17(f11(a4,a5),f13(a5),a4))), % 182.23/182.16 inference(scs_inference,[],[7996,8110,8092,7992,8094,7861,6225,6217,6348,7589,3584,7588,6119,6312,3513,1203,3630,3511,152,101,148,358,114,153,146,112,139,149,132,54,64])). % 182.23/182.16 cnf(8171,plain, % 182.23/182.16 (E(f11(f14(a5),x81711),f11(a4,x81711))), % 182.23/182.16 inference(rename_variables,[],[8015])). % 182.23/182.16 cnf(8174,plain, % 182.23/182.16 (~P16(f17(f11(a4,a5),f13(a5),a4),a5)), % 182.23/182.16 inference(scs_inference,[],[74,70,7996,8110,8032,8092,6114,7992,8015,8094,7976,7861,6225,6217,6348,7589,3584,7588,6119,313,6312,3513,1203,3630,3511,6183,152,101,148,358,114,153,146,112,139,149,132,54,64,144,88,59,145,115,143,48,94,136])). % 182.23/182.16 cnf(8181,plain, % 182.23/182.16 (P7(f17(f11(a4,a5),f13(a5),f14(a5)))), % 182.23/182.16 inference(scs_inference,[],[74,70,81,7996,7928,8110,8032,8045,8092,6114,7992,8015,8094,8090,7976,7861,6225,7878,6217,6348,7589,3584,7588,6119,313,6312,3513,1203,3630,3511,6184,6183,152,101,148,358,114,153,146,112,139,149,132,54,64,144,88,59,145,115,143,48,94,136,57,137,92,85])). % 182.23/182.16 cnf(8184,plain, % 182.23/182.16 (E(f17(x81841,x81842,a4),f17(x81841,x81842,f14(a5)))), % 182.23/182.16 inference(rename_variables,[],[7861])). % 182.23/182.16 cnf(8186,plain, % 182.23/182.16 (E(f19(x81861,a4),f19(x81861,f14(a5)))), % 182.23/182.16 inference(rename_variables,[],[7858])). % 182.23/182.16 cnf(8198,plain, % 182.23/182.16 (E(f17(x81981,x81982,a4),f17(x81981,x81982,f14(a5)))), % 182.23/182.16 inference(rename_variables,[],[7861])). % 182.23/182.16 cnf(8200,plain, % 182.23/182.16 (~P11(f13(a5),f17(f6(a5),f13(a5),f14(a5)),x82001)), % 182.23/182.16 inference(scs_inference,[],[74,71,70,81,6166,7996,8018,7917,7928,8110,8032,8045,8080,8092,6114,7992,8083,8015,8171,8094,8090,7976,7861,8156,8184,7858,8186,6225,6098,7878,6217,6348,7589,3584,7588,6119,313,6312,3513,1203,3630,3511,6184,6183,152,101,148,358,114,153,146,112,139,149,132,54,64,144,88,59,145,115,143,48,94,136,57,137,92,85,40,63,140,50,82,285,45,67,38,377])). % 182.23/182.16 cnf(8202,plain, % 182.23/182.16 (P6(f22(f14(a5),f12(a5),f13(a5)),f14(a5))), % 182.23/182.16 inference(scs_inference,[],[74,71,70,81,6166,7996,8018,7917,7928,8110,8032,8045,8080,8092,6114,7992,8083,8015,8171,8094,8090,7976,7861,8156,8184,7858,8186,6225,6098,7878,6217,6348,7589,3584,7588,6119,313,6312,3513,1203,3630,3511,6184,6183,152,101,148,358,114,153,146,112,139,149,132,54,64,144,88,59,145,115,143,48,94,136,57,137,92,85,40,63,140,50,82,285,45,67,38,377,147])). % 182.23/182.16 cnf(8206,plain, % 182.23/182.16 (~P6(a5,f10(f14(a5),f6(a5),f12(a5)))), % 182.23/182.16 inference(scs_inference,[],[74,71,70,81,6166,7996,8018,6611,7917,7928,8110,8032,8045,8080,8092,6114,7992,8083,8015,8171,8094,8090,7976,7861,8156,8184,7858,8186,6225,6098,7878,6217,6348,7589,3584,7588,6119,313,6312,3513,1203,3630,3511,6184,6183,152,101,148,358,114,153,146,112,139,149,132,54,64,144,88,59,145,115,143,48,94,136,57,137,92,85,40,63,140,50,82,285,45,67,38,377,147,130,103])). % 182.23/182.16 cnf(8212,plain, % 182.23/182.16 (E(f10(f14(a5),x82121,x82122),f10(a4,x82121,x82122))), % 182.23/182.16 inference(rename_variables,[],[8050])). % 182.23/182.16 cnf(8225,plain, % 182.23/182.16 (~P15(f17(f11(a4,a5),f13(a5),f14(a5)),a4)), % 182.23/182.16 inference(scs_inference,[],[74,71,70,81,6076,6166,7996,8018,6009,6355,6611,7917,7928,8087,8110,8032,8045,8080,8092,6114,7992,8050,8212,8083,8015,8171,8078,7938,8094,8090,8074,7976,7861,8156,8184,8198,7858,8186,6225,6098,7878,7835,6217,6348,7589,3584,7588,6119,313,6312,3513,1203,3630,1042,3511,6184,6183,152,101,148,358,114,153,146,112,139,149,132,54,64,144,88,59,145,115,143,48,94,136,57,137,92,85,40,63,140,50,82,285,45,67,38,377,147,130,103,68,131,49,90,2,3,39,2577,1020,44,55])). % 182.23/182.16 cnf(8267,plain, % 182.23/182.16 (E(f17(x82671,x82672,a4),f17(x82671,x82672,f14(a5)))), % 182.23/182.16 inference(rename_variables,[],[7861])). % 182.23/182.16 cnf(8271,plain, % 182.23/182.16 (E(f11(f14(a5),x82711),f11(a4,x82711))), % 182.23/182.16 inference(rename_variables,[],[8015])). % 182.23/182.16 cnf(8286,plain, % 182.23/182.16 (E(f19(x82861,a4),f19(x82861,f14(a5)))), % 182.23/182.16 inference(rename_variables,[],[7858])). % 182.23/182.16 cnf(8292,plain, % 182.23/182.16 (E(f19(x82921,a4),f19(x82921,f14(a5)))), % 182.23/182.16 inference(rename_variables,[],[7858])). % 182.23/182.16 cnf(8294,plain, % 182.23/182.16 (E(f17(x82941,x82942,a4),f17(x82941,x82942,f14(a5)))), % 182.23/182.16 inference(rename_variables,[],[7861])). % 182.23/182.16 cnf(8323,plain, % 182.23/182.16 (P6(f13(a5),a3)), % 182.23/182.16 inference(scs_inference,[],[74,72,81,8057,8133,6058,6928,8076,8181,8157,7985,7990,8121,8200,8056,7925,7926,8206,8174,8202,8085,7944,8225,8143,8102,7904,7992,8015,8271,7861,8267,8294,7858,8286,8292,7996,8062,7827,6100,1051,5949,6218,931,6119,6099,313,6088,3513,813,3511,6184,6183,152,146,101,148,358,153,112,139,132,149,144,145,137,136,61,92,48,59,143,85,93,64,94,140,54,57,285,63,40,82,45,50,130,67,147,377,103,131,38,68,49,2,3,4494,4778,4010])). % 182.23/182.16 cnf(8333,plain, % 182.23/182.16 (P5(f13(a5),a3)), % 182.23/182.16 inference(scs_inference,[],[74,72,81,8057,8133,6058,6928,8076,8181,8157,7985,7990,8121,8200,8056,7925,7926,8206,8174,8202,8085,7944,8225,8143,8102,7904,7992,8015,8271,7861,8267,8294,7858,8286,8292,7996,8062,7827,6100,1051,5949,6218,931,6119,6099,313,6088,3513,813,3511,6184,6183,152,146,101,148,358,153,112,139,132,149,144,145,137,136,61,92,48,59,143,85,93,64,94,140,54,57,285,63,40,82,45,50,130,67,147,377,103,131,38,68,49,2,3,4494,4778,4010,1764,87,249,84,1020,115])). % 182.23/182.16 cnf(8352,plain, % 182.23/182.16 ($false), % 182.23/182.16 inference(scs_inference,[],[8323,8333,3579,6088,3513,3511,101,140]), % 182.23/182.16 ['proof']). % 182.23/182.16 % SZS output end Proof % 182.23/182.16 % Total time :181.450000s %------------------------------------------------------------------------------