%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PRO017+2 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n020.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:48 EDT 2024 % Result : Theorem 180.85s 182.03s % Output : CNFRefutation 180.96s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.13 % Problem : PRO017+2 : TPTP v8.2.0. Released v4.0.0. % 0.07/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n020.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Thu Jun 20 06:31:39 EDT 2024 % 0.13/0.34 % CPUTime : % 0.20/0.59 start to proof:theBenchmark % 180.85/182.00 %------------------------------------------- % 180.85/182.00 % File :CSE---1.7 % 180.85/182.00 % Problem :theBenchmark % 180.85/182.00 % Transform :cnf % 180.85/182.00 % Format :tptp:raw % 180.85/182.00 % Command :java -jar mcs_scs.jar %d %s % 180.85/182.00 % 180.85/182.00 % Result :Theorem 180.190000s % 180.85/182.00 % Output :CNFRefutation 180.190000s % 180.85/182.00 %------------------------------------------- % 180.85/182.01 %------------------------------------------------------------------------------ % 180.85/182.01 % File : PRO017+2 : TPTP v8.2.0. Released v4.0.0. % 180.85/182.01 % Domain : Processes % 180.85/182.01 % Problem : PSL cliff problem coe-7.3.1 % 180.85/182.01 % Version : Especial : Reduced > Especial. % 180.85/182.01 % English : % 180.85/182.01 % Refs : [Hal09] Halcomb (2009), Email to G. Sutcliffe % 180.85/182.01 % Source : [Hal09] % 180.85/182.01 % Names : minimal-subset-p9__coe-7.3.1-pd [Hal09] % 180.85/182.01 % 180.85/182.01 % Status : Theorem % 180.85/182.01 % Rating : 0.36 v8.2.0, 0.31 v7.5.0, 0.38 v7.4.0, 0.30 v7.3.0, 0.31 v7.2.0, 0.28 v7.1.0, 0.26 v7.0.0, 0.23 v6.4.0, 0.27 v6.3.0, 0.33 v6.2.0, 0.40 v6.1.0, 0.53 v6.0.0, 0.39 v5.5.0, 0.52 v5.4.0, 0.54 v5.3.0, 0.56 v5.2.0, 0.45 v5.1.0, 0.52 v5.0.0, 0.54 v4.1.0, 0.57 v4.0.0 % 180.85/182.01 % Syntax : Number of formulae : 46 ( 12 unt; 0 def) % 180.85/182.01 % Number of atoms : 145 ( 12 equ) % 180.85/182.01 % Maximal formula atoms : 14 ( 3 avg) % 180.85/182.01 % Number of connectives : 118 ( 19 ~; 6 |; 57 &) % 180.85/182.01 % ( 7 <=>; 29 =>; 0 <=; 0 <~>) % 180.85/182.01 % Maximal formula depth : 16 ( 5 avg) % 180.85/182.01 % Maximal term depth : 1 ( 1 avg) % 180.85/182.01 % Number of predicates : 18 ( 17 usr; 0 prp; 1-3 aty) % 180.85/182.01 % Number of functors : 5 ( 5 usr; 5 con; 0-0 aty) % 180.85/182.01 % Number of variables : 105 ( 84 !; 21 ?) % 180.85/182.01 % SPC : FOF_THM_RFO_SEQ % 180.85/182.01 % 180.85/182.01 % Comments : % 180.85/182.01 %------------------------------------------------------------------------------ % 180.85/182.01 fof(sos,axiom, % 180.85/182.01 ! [X0,X1,X2,X3] : % 180.85/182.01 ( ( min_precedes(X0,X1,X3) % 180.85/182.01 & min_precedes(X1,X2,X3) ) % 180.85/182.01 => min_precedes(X0,X2,X3) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_01,axiom, % 180.85/182.02 ! [X4,X5,X6] : % 180.85/182.02 ( ( earlier(X4,X5) % 180.85/182.02 & earlier(X5,X6) ) % 180.85/182.02 => earlier(X4,X6) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_02,axiom, % 180.85/182.02 ! [X7,X8,X9,X10] : % 180.85/182.02 ( ( occurrence_of(X9,X10) % 180.85/182.02 & root_occ(X7,X9) % 180.85/182.02 & root_occ(X8,X9) ) % 180.85/182.02 => X7 = X8 ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_03,axiom, % 180.85/182.02 ! [X11,X12,X13,X14] : % 180.85/182.02 ( ( occurrence_of(X13,X14) % 180.85/182.02 & ~ atomic(X14) % 180.85/182.02 & leaf_occ(X11,X13) % 180.85/182.02 & leaf_occ(X12,X13) ) % 180.85/182.02 => X11 = X12 ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_04,axiom, % 180.85/182.02 ! [X15,X16,X17] : % 180.85/182.02 ( next_subocc(X15,X16,X17) % 180.85/182.02 <=> ( min_precedes(X15,X16,X17) % 180.85/182.02 & ~ ? [X18] : % 180.85/182.02 ( min_precedes(X15,X18,X17) % 180.85/182.02 & min_precedes(X18,X16,X17) ) ) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_05,axiom, % 180.85/182.02 ! [X19,X20,X21] : % 180.85/182.02 ( next_subocc(X19,X20,X21) % 180.85/182.02 => ( arboreal(X19) % 180.85/182.02 & arboreal(X20) ) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_06,axiom, % 180.85/182.02 ! [X22,X23,X24] : % 180.85/182.02 ( min_precedes(X22,X23,X24) % 180.85/182.02 => precedes(X22,X23) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_07,axiom, % 180.85/182.02 ! [X25,X26,X27] : % 180.85/182.02 ( min_precedes(X25,X26,X27) % 180.85/182.02 => ~ root(X26,X27) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_08,axiom, % 180.85/182.02 ! [X28,X29] : % 180.85/182.02 ( precedes(X28,X29) % 180.85/182.02 <=> ( earlier(X28,X29) % 180.85/182.02 & legal(X29) ) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_09,axiom, % 180.85/182.02 ! [X30,X31] : % 180.85/182.02 ( earlier(X30,X31) % 180.85/182.02 => ~ earlier(X31,X30) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_10,axiom, % 180.85/182.02 ! [X32,X33] : % 180.85/182.02 ( root_occ(X32,X33) % 180.85/182.02 <=> ? [X34] : % 180.85/182.02 ( occurrence_of(X33,X34) % 180.85/182.02 & subactivity_occurrence(X32,X33) % 180.85/182.02 & root(X32,X34) ) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_11,axiom, % 180.85/182.02 ! [X35,X36] : % 180.85/182.02 ( leaf_occ(X35,X36) % 180.85/182.02 <=> ? [X37] : % 180.85/182.02 ( occurrence_of(X36,X37) % 180.85/182.02 & subactivity_occurrence(X35,X36) % 180.85/182.02 & leaf(X35,X37) ) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_12,axiom, % 180.85/182.02 ! [X38,X39] : % 180.85/182.02 ( root(X38,X39) % 180.85/182.02 => legal(X38) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_13,axiom, % 180.85/182.02 ! [X40,X41] : % 180.85/182.02 ( occurrence_of(X40,X41) % 180.85/182.02 => ( arboreal(X40) % 180.85/182.02 <=> atomic(X41) ) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_14,axiom, % 180.85/182.02 ! [X42,X43] : % 180.85/182.02 ( leaf(X42,X43) % 180.85/182.02 <=> ( ( root(X42,X43) % 180.85/182.02 | ? [X44] : min_precedes(X44,X42,X43) ) % 180.85/182.02 & ~ ? [X45] : min_precedes(X42,X45,X43) ) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_15,axiom, % 180.85/182.02 ! [X46,X47] : % 180.85/182.02 ( atocc(X46,X47) % 180.85/182.02 <=> ? [X48] : % 180.85/182.02 ( subactivity(X47,X48) % 180.85/182.02 & atomic(X48) % 180.85/182.02 & occurrence_of(X46,X48) ) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_16,axiom, % 180.85/182.02 ! [X49,X50] : % 180.85/182.02 ( ( atocc(X49,X50) % 180.85/182.02 & legal(X49) ) % 180.85/182.02 => root(X49,X50) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_17,axiom, % 180.85/182.02 ! [X51] : % 180.85/182.02 ( legal(X51) % 180.85/182.02 => arboreal(X51) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_18,axiom, % 180.85/182.02 ! [X52] : % 180.85/182.02 ( activity_occurrence(X52) % 180.85/182.02 => ? [X53] : % 180.85/182.02 ( activity(X53) % 180.85/182.02 & occurrence_of(X52,X53) ) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_19,axiom, % 180.85/182.02 ! [X54,X55] : % 180.85/182.02 ( subactivity_occurrence(X54,X55) % 180.85/182.02 => ( activity_occurrence(X54) % 180.85/182.02 & activity_occurrence(X55) ) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_20,axiom, % 180.85/182.02 ! [X56,X57,X58] : % 180.85/182.02 ( ( occurrence_of(X56,X58) % 180.85/182.02 & root_occ(X57,X56) ) % 180.85/182.02 => ~ ? [X59] : min_precedes(X59,X57,X58) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_21,axiom, % 180.85/182.02 ! [X60,X61,X62] : % 180.85/182.02 ( ( occurrence_of(X60,X62) % 180.85/182.02 & leaf_occ(X61,X60) ) % 180.85/182.02 => ~ ? [X63] : min_precedes(X61,X63,X62) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_22,axiom, % 180.85/182.02 ! [X64,X65,X66] : % 180.85/182.02 ( ( occurrence_of(X64,X65) % 180.85/182.02 & occurrence_of(X64,X66) ) % 180.85/182.02 => X65 = X66 ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_23,axiom, % 180.85/182.02 ! [X67,X68] : % 180.85/182.02 ( ( leaf(X67,X68) % 180.85/182.02 & ~ atomic(X68) ) % 180.85/182.02 => ? [X69] : % 180.85/182.02 ( occurrence_of(X69,X68) % 180.85/182.02 & leaf_occ(X67,X69) ) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_24,axiom, % 180.85/182.02 ! [X70,X71,X72] : % 180.85/182.02 ( min_precedes(X71,X72,X70) % 180.85/182.02 => ? [X73] : % 180.85/182.02 ( occurrence_of(X73,X70) % 180.85/182.02 & subactivity_occurrence(X71,X73) % 180.85/182.02 & subactivity_occurrence(X72,X73) ) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_25,axiom, % 180.85/182.02 ! [X74,X75] : % 180.85/182.02 ( ( leaf(X74,X75) % 180.85/182.02 & ~ atomic(X75) ) % 180.85/182.02 => ? [X76] : % 180.85/182.02 ( occurrence_of(X76,X75) % 180.85/182.02 & leaf_occ(X74,X76) ) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_26,axiom, % 180.85/182.02 ! [X77,X78,X79] : % 180.85/182.02 ( min_precedes(X78,X79,X77) % 180.85/182.02 => ? [X80,X81] : % 180.85/182.02 ( subactivity(X80,X77) % 180.85/182.02 & subactivity(X81,X77) % 180.85/182.02 & atocc(X78,X80) % 180.85/182.02 & atocc(X79,X81) ) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_27,axiom, % 180.85/182.02 ! [X82,X83] : % 180.85/182.02 ( root(X83,X82) % 180.85/182.02 => ? [X84] : % 180.85/182.02 ( subactivity(X84,X82) % 180.85/182.02 & atocc(X83,X84) ) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_28,axiom, % 180.85/182.02 ! [X85,X86,X87,X88] : % 180.85/182.02 ( ( occurrence_of(X86,X85) % 180.85/182.02 & arboreal(X87) % 180.85/182.02 & arboreal(X88) % 180.85/182.02 & subactivity_occurrence(X87,X86) % 180.85/182.02 & subactivity_occurrence(X88,X86) ) % 180.85/182.02 => ( min_precedes(X87,X88,X85) % 180.85/182.02 | min_precedes(X88,X87,X85) % 180.85/182.02 | X87 = X88 ) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_29,axiom, % 180.85/182.02 ! [X89,X90] : % 180.85/182.02 ( occurrence_of(X90,X89) % 180.85/182.02 => ( activity(X89) % 180.85/182.02 & activity_occurrence(X90) ) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_30,axiom, % 180.85/182.02 ! [X91,X92] : % 180.85/182.02 ( ( occurrence_of(X92,X91) % 180.85/182.02 & ~ atomic(X91) ) % 180.85/182.02 => ? [X93] : % 180.85/182.02 ( root(X93,X91) % 180.85/182.02 & subactivity_occurrence(X93,X92) ) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_31,axiom, % 180.85/182.02 ! [X94] : % 180.85/182.02 ( activity(X94) % 180.85/182.02 => subactivity(X94,X94) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_32,axiom, % 180.85/182.02 ! [X95,X96] : % 180.85/182.02 ( ( occurrence_of(X96,tptp0) % 180.85/182.02 & subactivity_occurrence(X95,X96) % 180.85/182.02 & arboreal(X95) % 180.85/182.02 & ~ leaf_occ(X95,X96) ) % 180.85/182.02 => ? [X97,X98,X99] : % 180.85/182.02 ( occurrence_of(X97,tptp3) % 180.85/182.02 & next_subocc(X95,X97,tptp0) % 180.85/182.02 & occurrence_of(X98,tptp4) % 180.85/182.02 & min_precedes(X97,X98,tptp0) % 180.85/182.02 & ( occurrence_of(X99,tptp2) % 180.85/182.02 | occurrence_of(X99,tptp1) ) % 180.85/182.02 & min_precedes(X98,X99,tptp0) % 180.85/182.02 & ! [X100] : % 180.85/182.02 ( min_precedes(X97,X100,tptp0) % 180.85/182.02 => ( X100 = X98 % 180.85/182.02 | X100 = X99 ) ) ) ) ). % 180.85/182.02 % 180.85/182.02 fof(sos_33,axiom, % 180.85/182.02 activity(tptp0) ). % 180.85/182.02 % 180.85/182.02 fof(sos_34,axiom, % 180.85/182.02 ~ atomic(tptp0) ). % 180.85/182.02 % 180.85/182.03 fof(sos_35,axiom, % 180.85/182.03 atomic(tptp4) ). % 180.85/182.03 % 180.85/182.03 fof(sos_36,axiom, % 180.85/182.03 atomic(tptp2) ). % 180.85/182.03 % 180.85/182.03 fof(sos_37,axiom, % 180.85/182.03 atomic(tptp1) ). % 180.85/182.03 % 180.85/182.03 fof(sos_38,axiom, % 180.85/182.03 atomic(tptp3) ). % 180.85/182.03 % 180.85/182.03 fof(sos_39,axiom, % 180.85/182.03 tptp4 != tptp3 ). % 180.85/182.03 % 180.85/182.03 fof(sos_40,axiom, % 180.85/182.03 tptp4 != tptp2 ). % 180.85/182.03 % 180.85/182.03 fof(sos_41,axiom, % 180.85/182.03 tptp4 != tptp1 ). % 180.85/182.03 % 180.85/182.03 fof(sos_42,axiom, % 180.85/182.03 tptp3 != tptp2 ). % 180.85/182.03 % 180.85/182.03 fof(sos_43,axiom, % 180.85/182.03 tptp3 != tptp1 ). % 180.85/182.03 % 180.85/182.03 fof(sos_44,axiom, % 180.85/182.03 tptp2 != tptp1 ). % 180.85/182.03 % 180.85/182.03 fof(goals,conjecture, % 180.85/182.03 ! [X101,X102] : % 180.85/182.03 ( ( occurrence_of(X102,tptp0) % 180.85/182.03 & subactivity_occurrence(X101,X102) % 180.85/182.03 & arboreal(X101) % 180.85/182.03 & ~ leaf_occ(X101,X102) ) % 180.85/182.03 => ? [X103,X104] : % 180.85/182.03 ( occurrence_of(X103,tptp3) % 180.85/182.03 & next_subocc(X101,X103,tptp0) % 180.85/182.03 & ( occurrence_of(X104,tptp2) % 180.85/182.03 | occurrence_of(X104,tptp1) ) % 180.85/182.03 & min_precedes(X103,X104,tptp0) % 180.85/182.03 & leaf(X104,tptp0) ) ) ). % 180.85/182.03 % 180.85/182.03 %------------------------------------------------------------------------------ % 180.85/182.03 %------------------------------------------- % 180.85/182.03 % Proof found % 180.85/182.03 % SZS status Theorem for theBenchmark % 180.85/182.03 % SZS output start Proof % 180.85/182.03 %ClaNum:156(EqnAxiom:68) % 180.85/182.03 %VarNum:437(SingletonVarNum:176) % 180.85/182.03 %MaxLitNum:8 % 180.85/182.03 %MaxfuncDepth:1 % 180.85/182.03 %SharedTerms:23 % 180.85/182.03 %goalClause: 73 75 76 84 151 152 % 180.85/182.03 %singleGoalClaCount:4 % 180.85/182.03 [69]P1(a1) % 180.85/182.03 [70]P1(a24) % 180.85/182.03 [71]P1(a2) % 180.85/182.03 [72]P1(a3) % 180.85/182.03 [73]P2(a4) % 180.85/182.03 [74]P3(a13) % 180.85/182.03 [75]P6(a14,a13) % 180.85/182.03 [76]P13(a4,a14) % 180.85/182.03 [77]~E(a1,a24) % 180.85/182.03 [78]~E(a1,a2) % 180.85/182.03 [79]~E(a2,a24) % 180.85/182.03 [80]~E(a1,a3) % 180.85/182.03 [81]~E(a3,a24) % 180.85/182.03 [82]~E(a3,a2) % 180.85/182.03 [83]~P1(a13) % 180.85/182.03 [84]~P7(a4,a14) % 180.85/182.03 [85]~P10(x851)+P2(x851) % 180.85/182.03 [87]~P3(x871)+P14(x871,x871) % 180.85/182.03 [86]~P4(x861)+P3(f15(x861)) % 180.85/182.03 [94]~P4(x941)+P6(x941,f15(x941)) % 180.85/182.03 [88]P10(x881)+~P15(x882,x881) % 180.85/182.03 [89]P10(x891)+~P16(x891,x892) % 180.85/182.03 [90]P4(x901)+~P6(x901,x902) % 180.85/182.03 [91]P4(x911)+~P13(x912,x911) % 180.85/182.03 [92]P4(x921)+~P13(x921,x922) % 180.85/182.03 [93]P3(x931)+~P6(x932,x931) % 180.85/182.03 [97]~P15(x971,x972)+P8(x971,x972) % 180.85/182.03 [98]~P17(x981,x982)+P13(x981,x982) % 180.85/182.03 [99]~P7(x991,x992)+P13(x991,x992) % 180.85/182.03 [102]~P8(x1022,x1021)+~P8(x1021,x1022) % 180.85/182.03 [104]~P5(x1041,x1042)+P1(f16(x1041,x1042)) % 180.85/182.03 [106]~P17(x1062,x1061)+P6(x1061,f17(x1062,x1061)) % 180.85/182.03 [107]~P7(x1072,x1071)+P6(x1071,f19(x1072,x1071)) % 180.85/182.03 [108]~P5(x1081,x1082)+P6(x1081,f16(x1081,x1082)) % 180.85/182.03 [109]~P17(x1091,x1092)+P16(x1091,f17(x1091,x1092)) % 180.85/182.03 [110]~P7(x1101,x1102)+P9(x1101,f19(x1101,x1102)) % 180.85/182.03 [111]~P16(x1111,x1112)+P5(x1111,f5(x1112,x1111)) % 180.85/182.03 [112]~P5(x1122,x1121)+P14(x1121,f16(x1122,x1121)) % 180.85/182.03 [113]~P16(x1132,x1131)+P14(f5(x1131,x1132),x1131) % 180.85/182.03 [127]P2(x1271)+~P11(x1272,x1271,x1273) % 180.85/182.03 [128]P2(x1281)+~P11(x1281,x1282,x1283) % 180.85/182.03 [129]P15(x1291,x1292)+~P12(x1291,x1292,x1293) % 180.85/182.03 [131]~P16(x1311,x1312)+~P12(x1313,x1311,x1312) % 180.85/182.03 [132]~P9(x1321,x1322)+~P12(x1321,x1323,x1322) % 180.85/182.03 [140]~P11(x1401,x1402,x1403)+P12(x1401,x1402,x1403) % 180.85/182.03 [144]~P12(x1443,x1441,x1442)+P13(x1441,f23(x1442,x1443,x1441)) % 180.85/182.03 [145]~P12(x1451,x1453,x1452)+P13(x1451,f23(x1452,x1451,x1453)) % 180.85/182.03 [146]~P12(x1461,x1463,x1462)+P5(x1461,f7(x1462,x1461,x1463)) % 180.85/182.03 [147]~P12(x1473,x1471,x1472)+P5(x1471,f8(x1472,x1473,x1471)) % 180.85/182.03 [148]~P12(x1482,x1483,x1481)+P6(f23(x1481,x1482,x1483),x1481) % 180.85/182.03 [149]~P12(x1492,x1493,x1491)+P14(f7(x1491,x1492,x1493),x1491) % 180.85/182.03 [150]~P12(x1502,x1503,x1501)+P14(f8(x1501,x1502,x1503),x1501) % 180.85/182.03 [95]~P6(x952,x951)+P1(x951)+~P2(x952) % 180.85/182.03 [96]~P6(x961,x962)+P2(x961)+~P1(x962) % 180.85/182.03 [100]~P10(x1002)+~P8(x1001,x1002)+P15(x1001,x1002) % 180.85/182.03 [101]~P10(x1011)+~P5(x1011,x1012)+P16(x1011,x1012) % 180.85/182.03 [115]~P9(x1152,x1151)+P1(x1151)+P7(x1152,f22(x1152,x1151)) % 180.85/182.03 [116]~P9(x1162,x1161)+P1(x1161)+P7(x1162,f6(x1162,x1161)) % 180.85/182.03 [117]~P9(x1172,x1171)+P1(x1171)+P6(f22(x1172,x1171),x1171) % 180.85/182.03 [118]~P9(x1182,x1181)+P1(x1181)+P6(f6(x1182,x1181),x1181) % 180.85/182.03 [119]~P6(x1192,x1191)+P1(x1191)+P16(f9(x1191,x1192),x1191) % 180.85/182.03 [120]~P6(x1202,x1201)+P1(x1201)+P13(f9(x1201,x1202),x1202) % 180.85/182.03 [133]~P16(x1331,x1332)+P9(x1331,x1332)+P12(x1331,f20(x1331,x1332),x1332) % 180.85/182.03 [134]~P9(x1341,x1342)+P16(x1341,x1342)+P12(f21(x1341,x1342),x1341,x1342) % 180.85/182.03 [103]~P6(x1033,x1031)+E(x1031,x1032)+~P6(x1033,x1032) % 180.85/182.03 [105]~P8(x1051,x1053)+P8(x1051,x1052)+~P8(x1053,x1052) % 180.85/182.03 [142]P9(x1421,x1422)+~P12(x1423,x1421,x1422)+P12(x1421,f20(x1421,x1422),x1422) % 180.85/182.03 [155]~P12(x1551,x1552,x1553)+P11(x1551,x1552,x1553)+P12(x1551,f18(x1551,x1552,x1553),x1553) % 180.85/182.03 [156]~P12(x1561,x1562,x1563)+P11(x1561,x1562,x1563)+P12(f18(x1561,x1562,x1563),x1562,x1563) % 180.85/182.03 [138]~P6(x1381,x1382)+~P12(x1384,x1383,x1382)+~P17(x1383,x1381) % 180.85/182.03 [139]~P6(x1391,x1392)+~P12(x1393,x1394,x1392)+~P7(x1393,x1391) % 180.85/182.03 [153]~P12(x1531,x1534,x1533)+P12(x1531,x1532,x1533)+~P12(x1534,x1532,x1533) % 180.85/182.03 [154]~P11(x1544,x1542,x1543)+~P12(x1541,x1542,x1543)+~P12(x1544,x1541,x1543) % 180.85/182.03 [114]~P6(x1141,x1143)+~P14(x1142,x1143)+P5(x1141,x1142)+~P1(x1143) % 180.85/182.03 [123]~P16(x1231,x1233)+~P13(x1231,x1232)+P17(x1231,x1232)+~P6(x1232,x1233) % 180.85/182.03 [124]~P13(x1241,x1242)+~P9(x1241,x1243)+P7(x1241,x1242)+~P6(x1242,x1243) % 180.85/182.03 [121]~P17(x1212,x1213)+~P17(x1211,x1213)+E(x1211,x1212)+~P6(x1213,x1214) % 180.85/182.03 [151]~P12(x1511,x1512,a13)+~P9(x1512,a13)+~P6(x1511,a1)+~P6(x1512,a2)+~P11(a4,x1511,a13) % 180.85/182.03 [152]~P12(x1521,x1522,a13)+~P9(x1522,a13)+~P6(x1521,a1)+~P6(x1522,a3)+~P11(a4,x1521,a13) % 180.85/182.03 [125]~P2(x1251)+~P13(x1251,x1252)+P7(x1251,x1252)+~P6(x1252,a13)+P6(f10(x1251),a1) % 180.85/182.03 [126]~P2(x1261)+~P13(x1261,x1262)+P7(x1261,x1262)+~P6(x1262,a13)+P6(f11(x1261),a24) % 180.85/182.03 [135]~P2(x1351)+~P13(x1351,x1352)+P7(x1351,x1352)+~P6(x1352,a13)+P11(x1351,f10(x1351),a13) % 180.85/182.03 [136]~P2(x1361)+~P13(x1361,x1362)+P7(x1361,x1362)+~P6(x1362,a13)+P12(f10(x1361),f11(x1361),a13) % 180.85/182.03 [137]~P2(x1371)+~P13(x1371,x1372)+P7(x1371,x1372)+~P6(x1372,a13)+P12(f11(x1371),f12(x1371),a13) % 180.85/182.03 [122]~P7(x1222,x1224)+~P7(x1221,x1224)+E(x1221,x1222)+~P6(x1224,x1223)+P1(x1223) % 180.85/182.03 [130]~P2(x1301)+~P13(x1301,x1302)+P7(x1301,x1302)+~P6(x1302,a13)+P6(f12(x1301),a2)+P6(f12(x1301),a3) % 180.85/182.03 [141]~P2(x1412)+~P13(x1412,x1413)+P7(x1412,x1413)+E(x1411,f12(x1412))+~P6(x1413,a13)+E(x1411,f11(x1412))+~P12(f10(x1412),x1411,a13) % 180.85/182.03 [143]P12(x1431,x1432,x1433)+~P2(x1432)+~P2(x1431)+~P13(x1432,x1434)+~P13(x1431,x1434)+E(x1431,x1432)+P12(x1432,x1431,x1433)+~P6(x1434,x1433) % 180.85/182.03 %EqnAxiom % 180.85/182.03 [1]E(x11,x11) % 180.85/182.03 [2]E(x22,x21)+~E(x21,x22) % 180.85/182.03 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 180.85/182.03 [4]~E(x41,x42)+E(f15(x41),f15(x42)) % 180.85/182.03 [5]~E(x51,x52)+E(f18(x51,x53,x54),f18(x52,x53,x54)) % 180.85/182.03 [6]~E(x61,x62)+E(f18(x63,x61,x64),f18(x63,x62,x64)) % 180.85/182.03 [7]~E(x71,x72)+E(f18(x73,x74,x71),f18(x73,x74,x72)) % 180.85/182.03 [8]~E(x81,x82)+E(f16(x81,x83),f16(x82,x83)) % 180.85/182.03 [9]~E(x91,x92)+E(f16(x93,x91),f16(x93,x92)) % 180.85/182.03 [10]~E(x101,x102)+E(f17(x101,x103),f17(x102,x103)) % 180.85/182.03 [11]~E(x111,x112)+E(f17(x113,x111),f17(x113,x112)) % 180.85/182.03 [12]~E(x121,x122)+E(f19(x121,x123),f19(x122,x123)) % 180.85/182.03 [13]~E(x131,x132)+E(f19(x133,x131),f19(x133,x132)) % 180.85/182.03 [14]~E(x141,x142)+E(f8(x141,x143,x144),f8(x142,x143,x144)) % 180.85/182.03 [15]~E(x151,x152)+E(f8(x153,x151,x154),f8(x153,x152,x154)) % 180.85/182.03 [16]~E(x161,x162)+E(f8(x163,x164,x161),f8(x163,x164,x162)) % 180.85/182.03 [17]~E(x171,x172)+E(f23(x171,x173,x174),f23(x172,x173,x174)) % 180.85/182.03 [18]~E(x181,x182)+E(f23(x183,x181,x184),f23(x183,x182,x184)) % 180.85/182.03 [19]~E(x191,x192)+E(f23(x193,x194,x191),f23(x193,x194,x192)) % 180.85/182.03 [20]~E(x201,x202)+E(f7(x201,x203,x204),f7(x202,x203,x204)) % 180.85/182.03 [21]~E(x211,x212)+E(f7(x213,x211,x214),f7(x213,x212,x214)) % 180.85/182.03 [22]~E(x221,x222)+E(f7(x223,x224,x221),f7(x223,x224,x222)) % 180.85/182.03 [23]~E(x231,x232)+E(f5(x231,x233),f5(x232,x233)) % 180.85/182.03 [24]~E(x241,x242)+E(f5(x243,x241),f5(x243,x242)) % 180.85/182.03 [25]~E(x251,x252)+E(f20(x251,x253),f20(x252,x253)) % 180.85/182.03 [26]~E(x261,x262)+E(f20(x263,x261),f20(x263,x262)) % 180.85/182.03 [27]~E(x271,x272)+E(f10(x271),f10(x272)) % 180.85/182.03 [28]~E(x281,x282)+E(f22(x281,x283),f22(x282,x283)) % 180.85/182.03 [29]~E(x291,x292)+E(f22(x293,x291),f22(x293,x292)) % 180.85/182.03 [30]~E(x301,x302)+E(f6(x301,x303),f6(x302,x303)) % 180.85/182.03 [31]~E(x311,x312)+E(f6(x313,x311),f6(x313,x312)) % 180.85/182.03 [32]~E(x321,x322)+E(f11(x321),f11(x322)) % 180.85/182.03 [33]~E(x331,x332)+E(f12(x331),f12(x332)) % 180.85/182.03 [34]~E(x341,x342)+E(f9(x341,x343),f9(x342,x343)) % 180.85/182.03 [35]~E(x351,x352)+E(f9(x353,x351),f9(x353,x352)) % 180.85/182.03 [36]~E(x361,x362)+E(f21(x361,x363),f21(x362,x363)) % 180.85/182.03 [37]~E(x371,x372)+E(f21(x373,x371),f21(x373,x372)) % 180.85/182.03 [38]~P1(x381)+P1(x382)+~E(x381,x382) % 180.85/182.03 [39]P12(x392,x393,x394)+~E(x391,x392)+~P12(x391,x393,x394) % 180.85/182.03 [40]P12(x403,x402,x404)+~E(x401,x402)+~P12(x403,x401,x404) % 180.85/182.03 [41]P12(x413,x414,x412)+~E(x411,x412)+~P12(x413,x414,x411) % 180.85/182.03 [42]P6(x422,x423)+~E(x421,x422)+~P6(x421,x423) % 180.85/182.03 [43]P6(x433,x432)+~E(x431,x432)+~P6(x433,x431) % 180.85/182.03 [44]P11(x442,x443,x444)+~E(x441,x442)+~P11(x441,x443,x444) % 180.85/182.03 [45]P11(x453,x452,x454)+~E(x451,x452)+~P11(x453,x451,x454) % 180.85/182.03 [46]P11(x463,x464,x462)+~E(x461,x462)+~P11(x463,x464,x461) % 180.85/182.03 [47]~P2(x471)+P2(x472)+~E(x471,x472) % 180.85/182.03 [48]~P3(x481)+P3(x482)+~E(x481,x482) % 180.85/182.03 [49]P13(x492,x493)+~E(x491,x492)+~P13(x491,x493) % 180.85/182.03 [50]P13(x503,x502)+~E(x501,x502)+~P13(x503,x501) % 180.85/182.03 [51]P16(x512,x513)+~E(x511,x512)+~P16(x511,x513) % 180.85/182.03 [52]P16(x523,x522)+~E(x521,x522)+~P16(x523,x521) % 180.85/182.03 [53]P15(x532,x533)+~E(x531,x532)+~P15(x531,x533) % 180.85/182.03 [54]P15(x543,x542)+~E(x541,x542)+~P15(x543,x541) % 180.85/182.03 [55]P7(x552,x553)+~E(x551,x552)+~P7(x551,x553) % 180.85/182.03 [56]P7(x563,x562)+~E(x561,x562)+~P7(x563,x561) % 180.85/182.03 [57]P9(x572,x573)+~E(x571,x572)+~P9(x571,x573) % 180.85/182.03 [58]P9(x583,x582)+~E(x581,x582)+~P9(x583,x581) % 180.85/182.03 [59]~P10(x591)+P10(x592)+~E(x591,x592) % 180.85/182.03 [60]P17(x602,x603)+~E(x601,x602)+~P17(x601,x603) % 180.85/182.03 [61]P17(x613,x612)+~E(x611,x612)+~P17(x613,x611) % 180.85/182.03 [62]~P4(x621)+P4(x622)+~E(x621,x622) % 180.85/182.03 [63]P14(x632,x633)+~E(x631,x632)+~P14(x631,x633) % 180.85/182.03 [64]P14(x643,x642)+~E(x641,x642)+~P14(x643,x641) % 180.85/182.03 [65]P5(x652,x653)+~E(x651,x652)+~P5(x651,x653) % 180.85/182.03 [66]P5(x663,x662)+~E(x661,x662)+~P5(x663,x661) % 180.85/182.03 [67]P8(x672,x673)+~E(x671,x672)+~P8(x671,x673) % 180.85/182.03 [68]P8(x683,x682)+~E(x681,x682)+~P8(x683,x681) % 180.85/182.03 % 180.85/182.03 %------------------------------------------- % 180.96/182.04 cnf(157,plain, % 180.96/182.04 (~P6(a4,a13)), % 180.96/182.04 inference(scs_inference,[],[73,83,95])). % 180.96/182.04 cnf(162,plain, % 180.96/182.04 (P6(a14,x1621)+~E(a13,x1621)), % 180.96/182.04 inference(scs_inference,[],[73,75,76,84,83,95,42,124,43])). % 180.96/182.04 cnf(213,plain, % 180.96/182.04 (~P10(a14)), % 180.96/182.04 inference(scs_inference,[],[83,75,85,95])). % 180.96/182.04 cnf(214,plain, % 180.96/182.04 (~P15(x2141,a14)), % 180.96/182.04 inference(scs_inference,[],[213,88])). % 180.96/182.04 cnf(216,plain, % 180.96/182.04 (~P16(a14,x2161)), % 180.96/182.04 inference(scs_inference,[],[213,88,89])). % 180.96/182.04 cnf(220,plain, % 180.96/182.04 (~P12(x2201,a14,x2202)), % 180.96/182.04 inference(scs_inference,[],[213,88,89,109,129])). % 180.96/182.04 cnf(226,plain, % 180.96/182.04 (P3(f15(a14))), % 180.96/182.04 inference(scs_inference,[],[75,86,90])). % 180.96/182.04 cnf(234,plain, % 180.96/182.04 (P14(x2341,f15(a14))+~E(f15(a14),x2341)), % 180.96/182.04 inference(scs_inference,[],[226,87,63])). % 180.96/182.04 cnf(235,plain, % 180.96/182.04 (P14(f15(a14),f15(a14))), % 180.96/182.04 inference(equality_inference,[],[234])). % 180.96/182.04 cnf(236,plain, % 180.96/182.04 (P14(f15(a14),x2361)+~E(f15(a14),x2361)), % 180.96/182.04 inference(scs_inference,[],[235,64])). % 180.96/182.04 cnf(240,plain, % 180.96/182.04 (P6(a14,f15(a14))), % 180.96/182.04 inference(scs_inference,[],[76,91,94])). % 180.96/182.04 cnf(241,plain, % 180.96/182.04 (P6(x2411,f15(a14))+~E(a14,x2411)), % 180.96/182.04 inference(scs_inference,[],[240,42])). % 180.96/182.04 cnf(242,plain, % 180.96/182.04 (E(a13,f15(a14))), % 180.96/182.04 inference(scs_inference,[],[75,240,42,103])). % 180.96/182.04 cnf(246,plain, % 180.96/182.04 (E(f15(a14),a13)), % 180.96/182.04 inference(scs_inference,[],[242,2])). % 180.96/182.04 cnf(249,plain, % 180.96/182.04 (~P1(f15(a14))), % 180.96/182.04 inference(scs_inference,[],[242,83,235,2,64,63,38])). % 180.96/182.04 cnf(352,plain, % 180.96/182.04 (P3(a1)), % 180.96/182.04 inference(scs_inference,[],[75,84,73,76,93,125])). % 180.96/182.04 cnf(359,plain, % 180.96/182.04 (~P8(x3591,x3592)+~P15(x3592,x3591)), % 180.96/182.04 inference(scs_inference,[],[97,102])). % 180.96/182.04 cnf(420,plain, % 180.96/182.04 (~P8(x4201,x4202)+~P12(x4202,x4201,x4203)), % 180.96/182.04 inference(scs_inference,[],[359,129])). % 180.96/182.04 cnf(449,plain, % 180.96/182.04 (~P12(x4491,x4492,x4493)+P1(f16(x4491,f7(x4493,x4491,x4492)))), % 180.96/182.04 inference(scs_inference,[],[104,146])). % 180.96/182.04 cnf(450,plain, % 180.96/182.04 (~P12(x4501,f9(a13,a14),a13)), % 180.96/182.04 inference(scs_inference,[],[83,75,131,119])). % 180.96/182.04 cnf(451,plain, % 180.96/182.04 (~P11(x4511,f9(a13,a14),a13)), % 180.96/182.04 inference(scs_inference,[],[450,140])). % 180.96/182.04 cnf(486,plain, % 180.96/182.04 (~P12(x4861,x4862,x4863)+~P15(x4862,x4861)), % 180.96/182.04 inference(scs_inference,[],[420,97])). % 180.96/182.04 cnf(504,plain, % 180.96/182.04 (~P12(x5041,x5042,x5043)+~P12(x5042,x5041,x5044)), % 180.96/182.04 inference(scs_inference,[],[486,129])). % 180.96/182.04 cnf(533,plain, % 180.96/182.04 (~P16(x5331,x5332)+P14(f5(x5332,x5331),f16(x5331,f5(x5332,x5331)))), % 180.96/182.04 inference(scs_inference,[],[112,111])). % 180.96/182.04 cnf(563,plain, % 180.96/182.04 (~P12(f11(a4),f10(a4),x5631)), % 180.96/182.04 inference(scs_inference,[],[75,84,73,76,504,136])). % 180.96/182.04 cnf(630,plain, % 180.96/182.04 (E(f16(x6301,f15(a14)),f16(x6301,a13))), % 180.96/182.04 inference(scs_inference,[],[242,9,2])). % 180.96/182.04 cnf(631,plain, % 180.96/182.04 (E(f16(x6311,a13),f16(x6311,f15(a14)))), % 180.96/182.04 inference(scs_inference,[],[630,2])). % 180.96/182.04 cnf(753,plain, % 180.96/182.04 (E(f17(f15(a14),x7531),f17(a13,x7531))), % 180.96/182.04 inference(scs_inference,[],[242,10,2])). % 180.96/182.04 cnf(754,plain, % 180.96/182.04 (E(f17(a13,x7541),f17(f15(a14),x7541))), % 180.96/182.04 inference(scs_inference,[],[753,2])). % 180.96/182.04 cnf(858,plain, % 180.96/182.04 (E(f17(x8581,f15(a14)),f17(x8581,a13))), % 180.96/182.04 inference(scs_inference,[],[242,11,2])). % 180.96/182.04 cnf(1359,plain, % 180.96/182.04 (E(f22(f18(x13591,x13592,a13),x13593),f22(f18(x13591,x13592,f15(a14)),x13593))), % 180.96/182.04 inference(scs_inference,[],[242,28,7])). % 180.96/182.04 cnf(1360,plain, % 180.96/182.04 (E(f22(x13601,f16(a13,x13602)),f22(x13601,f16(f15(a14),x13602)))), % 180.96/182.04 inference(scs_inference,[],[242,29,8])). % 180.96/182.04 cnf(1361,plain, % 180.96/182.04 (E(f6(f16(x13611,a13),x13612),f6(f16(x13611,f15(a14)),x13612))), % 180.96/182.04 inference(scs_inference,[],[242,30,9])). % 180.96/182.04 cnf(1366,plain, % 180.96/182.04 (E(f21(x13661,f8(a13,x13662,x13663)),f21(x13661,f8(f15(a14),x13662,x13663)))), % 180.96/182.04 inference(scs_inference,[],[242,37,14])). % 180.96/182.04 cnf(1367,plain, % 180.96/182.04 (P5(f12(a4),f8(a13,f11(a4),f12(a4)))), % 180.96/182.04 inference(scs_inference,[],[75,84,73,76,147,137])). % 180.96/182.04 cnf(1375,plain, % 180.96/182.04 (P5(f12(a4),x13751)+~E(f8(a13,f11(a4),f12(a4)),x13751)), % 180.96/182.04 inference(scs_inference,[],[1367,66])). % 180.96/182.04 cnf(1384,plain, % 180.96/182.04 (P6(f23(a13,f10(a4),f11(a4)),a13)), % 180.96/182.04 inference(scs_inference,[],[75,84,73,76,148,136])). % 180.96/182.04 cnf(1386,plain, % 180.96/182.04 (P6(f23(a13,f10(a4),f11(a4)),f15(a14))), % 180.96/182.04 inference(scs_inference,[],[157,242,1384,42,43])). % 180.96/182.04 cnf(1465,plain, % 180.96/182.04 (~P17(a2,f23(a13,f10(a4),f11(a4)))+~P17(a1,f23(a13,f10(a4),f11(a4)))), % 180.96/182.04 inference(scs_inference,[],[1384,78,121])). % 180.96/182.04 cnf(1614,plain, % 180.96/182.04 (~E(f16(x16141,f7(x16142,x16141,x16143)),a13)+~P12(x16141,x16143,x16142)), % 180.96/182.04 inference(scs_inference,[],[83,449,38])). % 180.96/182.04 cnf(1802,plain, % 180.96/182.04 (E(f8(x18021,f15(a13),x18022),f8(x18021,f15(f15(a14)),x18022))), % 180.96/182.04 inference(scs_inference,[],[242,15,4])). % 180.96/182.04 cnf(1803,plain, % 180.96/182.04 (E(f8(x18031,x18032,f18(a13,x18033,x18034)),f8(x18031,x18032,f18(f15(a14),x18033,x18034)))), % 180.96/182.04 inference(scs_inference,[],[242,16,5])). % 180.96/182.04 cnf(1881,plain, % 180.96/182.04 (~E(f16(f11(a4),f7(a13,f11(a4),f12(a4))),a13)), % 180.96/182.04 inference(scs_inference,[],[75,84,73,76,1614,137])). % 180.96/182.04 cnf(2360,plain, % 180.96/182.04 (~P17(a1,f23(a13,f10(a4),f11(a4)))+~P17(x23601,f23(a13,f10(a4),f11(a4)))+~E(x23601,a2)), % 180.96/182.04 inference(scs_inference,[],[1465,60])). % 180.96/182.04 cnf(2383,plain, % 180.96/182.04 (P8(f15(a14),x23831)+~P15(a13,x23831)), % 180.96/182.04 inference(scs_inference,[],[242,67,97])). % 180.96/182.04 cnf(2391,plain, % 180.96/182.04 (P8(x23911,f15(a14))+~P15(x23911,a13)), % 180.96/182.04 inference(scs_inference,[],[242,68,97])). % 180.96/182.04 cnf(2392,plain, % 180.96/182.04 (~P8(f15(a14),x23921)+~P15(x23921,a13)), % 180.96/182.04 inference(scs_inference,[],[2391,102])). % 180.96/182.04 cnf(2393,plain, % 180.96/182.04 (~P15(x23931,a13)+~P15(a13,x23931)), % 180.96/182.04 inference(scs_inference,[],[2392,2383])). % 180.96/182.04 cnf(2394,plain, % 180.96/182.04 (~P15(f15(a14),x23941)+~P15(x23941,a13)), % 180.96/182.04 inference(scs_inference,[],[246,2393,53])). % 180.96/182.04 cnf(2395,plain, % 180.96/182.04 (~P12(f15(a14),x23951,x23952)+~P15(x23951,a13)), % 180.96/182.04 inference(scs_inference,[],[2394,129])). % 180.96/182.04 cnf(2396,plain, % 180.96/182.04 (~P11(f15(a14),x23961,x23962)+~P15(x23961,a13)), % 180.96/182.04 inference(scs_inference,[],[2395,140])). % 180.96/182.04 cnf(2397,plain, % 180.96/182.04 (~P11(a13,x23971,x23972)+~P15(x23971,a13)), % 180.96/182.04 inference(scs_inference,[],[242,2396,44])). % 180.96/182.04 cnf(2398,plain, % 180.96/182.04 (~P11(a13,a13,x23981)+~P15(f15(a14),a13)), % 180.96/182.04 inference(scs_inference,[],[242,2397,45])). % 180.96/182.04 cnf(2399,plain, % 180.96/182.04 (~P11(f15(a14),a13,x23991)+~P15(f15(a14),a13)), % 180.96/182.04 inference(scs_inference,[],[246,2398,44])). % 180.96/182.04 cnf(2400,plain, % 180.96/182.04 (~P12(f15(a14),a13,x24001)+~P11(f15(a14),a13,x24002)), % 180.96/182.04 inference(scs_inference,[],[2399,129])). % 180.96/182.04 cnf(2401,plain, % 180.96/182.04 (~P11(f15(a14),a13,x24011)+~P11(f15(a14),a13,x24012)), % 180.96/182.04 inference(scs_inference,[],[2400,140])). % 180.96/182.04 cnf(2402,plain, % 180.96/182.04 (~P8(x24021,x24022)+~P15(x24022,x24023)+P8(x24021,x24023)), % 180.96/182.04 inference(scs_inference,[],[105,97])). % 180.96/182.04 cnf(2404,plain, % 180.96/182.04 (~P8(x24041,x24042)+~P8(x24042,x24043)+~P15(x24043,x24041)), % 180.96/182.04 inference(scs_inference,[],[2402,102])). % 180.96/182.04 cnf(2405,plain, % 180.96/182.04 (~P8(x24051,x24052)+~P12(x24053,x24051,x24054)+~P8(x24052,x24053)), % 180.96/182.04 inference(scs_inference,[],[2404,129])). % 180.96/182.04 cnf(2415,plain, % 180.96/182.04 (P13(f9(a13,a14),a14)), % 180.96/182.04 inference(scs_inference,[],[75,242,249,120,38])). % 180.96/182.04 cnf(2423,plain, % 180.96/182.04 (P13(x24231,a14)+~E(f9(a13,a14),x24231)), % 180.96/182.04 inference(scs_inference,[],[2415,49])). % 180.96/182.04 cnf(2448,plain, % 180.96/182.04 (~P8(x24481,x24482)+~P15(x24482,x24483)+~P12(x24483,x24481,x24484)), % 180.96/182.04 inference(scs_inference,[],[2405,97])). % 180.96/182.04 cnf(2449,plain, % 180.96/182.04 (~P12(x24491,f15(a14),x24492)+~P15(x24493,x24491)+~P15(a13,x24493)), % 180.96/182.04 inference(scs_inference,[],[2448,2383])). % 180.96/182.04 cnf(2473,plain, % 180.96/182.04 (~P12(x24731,x24732,x24733)+~P12(x24732,f15(a14),x24734)+~P15(a13,x24731)), % 180.96/182.04 inference(scs_inference,[],[2449,129])). % 180.96/182.04 cnf(2477,plain, % 180.96/182.04 (~P12(x24771,f10(a4),a13)+P12(x24771,f11(a4),a13)), % 180.96/182.04 inference(scs_inference,[],[75,84,73,76,153,136])). % 180.96/182.04 cnf(2478,plain, % 180.96/182.04 (P15(x24781,f11(a4))+~P12(x24781,f10(a4),a13)), % 180.96/182.04 inference(scs_inference,[],[2477,129])). % 180.96/182.04 cnf(2479,plain, % 180.96/182.04 (P10(f11(a4))+~P12(x24791,f10(a4),a13)), % 180.96/182.04 inference(scs_inference,[],[2478,88])). % 180.96/182.04 cnf(2480,plain, % 180.96/182.04 (P2(f11(a4))+~P12(x24801,f10(a4),a13)), % 180.96/182.04 inference(scs_inference,[],[2479,85])). % 180.96/182.04 cnf(2481,plain, % 180.96/182.04 (~P6(f11(a4),a13)+~P12(x24811,f10(a4),a13)), % 180.96/182.04 inference(scs_inference,[],[83,2480,95])). % 180.96/182.04 cnf(2482,plain, % 180.96/182.04 (~P11(x24821,f10(a4),a13)+~P6(f11(a4),a13)), % 180.96/182.04 inference(scs_inference,[],[2481,140])). % 180.96/182.04 cnf(2483,plain, % 180.96/182.04 (~P6(f11(a4),a13)), % 180.96/182.04 inference(scs_inference,[],[75,84,73,76,2482,135])). % 180.96/182.04 cnf(2484,plain, % 180.96/182.04 (~E(a14,f11(a4))), % 180.96/182.04 inference(scs_inference,[],[75,2483,42])). % 180.96/182.04 cnf(2803,plain, % 180.96/182.04 (P14(a1,a1)), % 180.96/182.04 inference(scs_inference,[],[352,87])). % 180.96/182.04 cnf(2809,plain, % 180.96/182.04 (~E(f11(a4),a14)), % 180.96/182.04 inference(scs_inference,[],[352,2484,2415,87,92,91,2])). % 180.96/182.04 cnf(2810,plain, % 180.96/182.04 (P16(f9(a13,a14),a13)), % 180.96/182.04 inference(scs_inference,[],[75,352,2484,2415,83,87,92,91,2,119])). % 180.96/182.04 cnf(2813,plain, % 180.96/182.04 (~P2(a14)), % 180.96/182.04 inference(scs_inference,[],[75,352,2484,2415,450,83,246,87,92,91,2,119,41,95])). % 180.96/182.04 cnf(2816,plain, % 180.96/182.04 (~E(a2,f15(a14))), % 180.96/182.04 inference(scs_inference,[],[75,352,2484,2483,2415,71,249,450,83,246,87,92,91,2,119,41,95,43,38])). % 180.96/182.04 cnf(2818,plain, % 180.96/182.04 (P17(f9(a13,a14),a14)), % 180.96/182.04 inference(scs_inference,[],[75,352,2484,2483,2415,71,249,73,450,83,246,87,92,91,2,119,41,95,43,38,47,123])). % 180.96/182.04 cnf(2820,plain, % 180.96/182.04 (P10(f9(a13,a14))), % 180.96/182.04 inference(scs_inference,[],[75,352,2484,2483,2415,71,249,73,450,83,246,87,92,91,2,119,41,95,43,38,47,123,89])). % 180.96/182.04 cnf(2822,plain, % 180.96/182.04 (~P15(x28221,f15(a14))+P15(x28221,a13)), % 180.96/182.04 inference(scs_inference,[],[75,352,2484,2483,2415,71,249,73,450,83,246,87,92,91,2,119,41,95,43,38,47,123,89,54])). % 180.96/182.04 cnf(2874,plain, % 180.96/182.04 (P2(f9(a13,a14))), % 180.96/182.04 inference(scs_inference,[],[2820,76,92,85])). % 180.96/182.04 cnf(2879,plain, % 180.96/182.04 (~E(a13,a2)), % 180.96/182.04 inference(scs_inference,[],[2820,2816,240,76,246,92,85,2,103,3])). % 180.96/182.04 cnf(2881,plain, % 180.96/182.04 (~E(f9(a13,a14),a14)), % 180.96/182.04 inference(scs_inference,[],[2820,2816,72,213,240,249,76,246,92,85,2,103,3,38,59])). % 180.96/182.04 cnf(2882,plain, % 180.96/182.04 (P6(f11(a4),a24)), % 180.96/182.04 inference(scs_inference,[],[75,2820,2816,72,213,240,249,84,73,76,246,92,85,2,103,3,38,59,126])). % 180.96/182.04 cnf(2884,plain, % 180.96/182.04 (P11(a4,f10(a4),a13)), % 180.96/182.04 inference(scs_inference,[],[75,2820,2816,72,213,240,249,84,73,76,246,92,85,2,103,3,38,59,126,135])). % 180.96/182.04 cnf(2886,plain, % 180.96/182.04 (P6(f10(a4),a1)), % 180.96/182.04 inference(scs_inference,[],[75,2820,2816,72,213,240,249,84,73,76,246,92,85,2,103,3,38,59,126,135,125])). % 180.96/182.04 cnf(2888,plain, % 180.96/182.04 (P12(f11(a4),f12(a4),a13)), % 180.96/182.04 inference(scs_inference,[],[75,2820,2816,72,213,240,249,84,73,76,246,92,85,2,103,3,38,59,126,135,125,137])). % 180.96/182.04 cnf(2890,plain, % 180.96/182.04 (P12(f10(a4),f11(a4),a13)), % 180.96/182.04 inference(scs_inference,[],[75,2820,2816,72,213,240,249,84,73,76,246,92,85,2,103,3,38,59,126,135,125,137,136])). % 180.96/182.04 cnf(2894,plain, % 180.96/182.04 (P6(a4,f15(a4))), % 180.96/182.04 inference(scs_inference,[],[75,2820,2816,72,213,240,249,84,73,76,246,92,85,2,103,3,38,59,126,135,125,137,136,86,94])). % 180.96/182.04 cnf(2896,plain, % 180.96/182.04 (~P16(f12(a4),a13)), % 180.96/182.04 inference(scs_inference,[],[75,2820,2816,72,213,240,249,84,73,76,246,92,85,2,103,3,38,59,126,135,125,137,136,86,94,131])). % 180.96/182.04 cnf(2898,plain, % 180.96/182.04 (P14(f15(a4),f15(a4))), % 180.96/182.04 inference(scs_inference,[],[75,2820,2816,72,213,240,249,84,73,76,246,92,85,2,103,3,38,59,126,135,125,137,136,86,94,131,87])). % 180.96/182.04 cnf(2900,plain, % 180.96/182.04 (~P9(f11(a4),a13)), % 180.96/182.04 inference(scs_inference,[],[75,2820,2816,72,213,240,249,84,73,76,246,92,85,2,103,3,38,59,126,135,125,137,136,86,94,131,87,132])). % 180.96/182.04 cnf(2902,plain, % 180.96/182.04 (~P8(f12(a4),f11(a4))), % 180.96/182.04 inference(scs_inference,[],[75,2820,2816,72,213,240,249,84,73,76,246,92,85,2,103,3,38,59,126,135,125,137,136,86,94,131,87,132,420])). % 180.96/182.04 cnf(2904,plain, % 180.96/182.04 (~P15(f12(a4),f11(a4))), % 180.96/182.04 inference(scs_inference,[],[75,2820,2816,72,213,240,249,84,73,76,246,92,85,2,103,3,38,59,126,135,125,137,136,86,94,131,87,132,420,486])). % 180.96/182.04 cnf(2906,plain, % 180.96/182.04 (~P12(f12(a4),f11(a4),x29061)), % 180.96/182.04 inference(scs_inference,[],[75,2820,2816,72,213,240,249,84,73,76,246,92,85,2,103,3,38,59,126,135,125,137,136,86,94,131,87,132,420,486,504])). % 180.96/182.04 cnf(2908,plain, % 180.96/182.04 (P3(a24)), % 180.96/182.04 inference(scs_inference,[],[75,2820,2816,72,213,240,249,84,73,76,246,92,85,2,103,3,38,59,126,135,125,137,136,86,94,131,87,132,420,486,504,93])). % 180.96/182.04 cnf(2910,plain, % 180.96/182.04 (P15(f11(a4),f12(a4))), % 180.96/182.04 inference(scs_inference,[],[75,2820,2816,72,213,240,249,84,73,76,246,92,85,2,103,3,38,59,126,135,125,137,136,86,94,131,87,132,420,486,504,93,129])). % 180.96/182.04 cnf(2912,plain, % 180.96/182.04 (P4(f11(a4))), % 180.96/182.04 inference(scs_inference,[],[75,2820,2816,72,213,240,249,84,73,76,246,92,85,2,103,3,38,59,126,135,125,137,136,86,94,131,87,132,420,486,504,93,129,90])). % 180.96/182.04 cnf(2914,plain, % 180.96/182.04 (P2(f10(a4))), % 180.96/182.04 inference(scs_inference,[],[75,2820,2816,72,213,240,249,84,73,76,246,92,85,2,103,3,38,59,126,135,125,137,136,86,94,131,87,132,420,486,504,93,129,90,127])). % 180.96/182.04 cnf(2916,plain, % 180.96/182.04 (P12(a4,f10(a4),a13)), % 180.96/182.04 inference(scs_inference,[],[75,2820,2816,72,213,240,249,84,73,76,246,92,85,2,103,3,38,59,126,135,125,137,136,86,94,131,87,132,420,486,504,93,129,90,127,140])). % 180.96/182.04 cnf(2918,plain, % 180.96/182.04 (P10(f12(a4))), % 180.96/182.04 inference(scs_inference,[],[75,2820,2816,72,213,240,249,84,73,76,246,92,85,2,103,3,38,59,126,135,125,137,136,86,94,131,87,132,420,486,504,93,129,90,127,140,88])). % 180.96/182.04 cnf(2925,plain, % 180.96/182.04 (~P12(f12(a4),f10(a4),a13)), % 180.96/182.04 inference(scs_inference,[],[75,2820,2816,563,72,213,240,249,84,73,76,246,92,85,2,103,3,38,59,126,135,125,137,136,86,94,131,87,132,420,486,504,93,129,90,127,140,88,60,138,139,153])). % 180.96/182.04 cnf(2926,plain, % 180.96/182.04 (~P12(f11(a4),f10(a4),x29261)), % 180.96/182.04 inference(rename_variables,[],[563])). % 180.96/182.04 cnf(2928,plain, % 180.96/182.04 (~P11(f10(a4),f12(a4),a13)), % 180.96/182.04 inference(scs_inference,[],[75,2820,2816,563,72,213,240,249,84,73,76,246,92,85,2,103,3,38,59,126,135,125,137,136,86,94,131,87,132,420,486,504,93,129,90,127,140,88,60,138,139,153,154])). % 180.96/182.04 cnf(2932,plain, % 180.96/182.04 (~E(f12(a4),a14)), % 180.96/182.04 inference(scs_inference,[],[75,2820,2816,563,2926,72,213,240,249,84,73,214,76,246,92,85,2,103,3,38,59,126,135,125,137,136,86,94,131,87,132,420,486,504,93,129,90,127,140,88,60,138,139,153,154,39,54])). % 180.96/182.04 cnf(2935,plain, % 180.96/182.04 (P2(f11(a4))), % 180.96/182.04 inference(scs_inference,[],[75,2820,2816,563,2926,72,213,70,240,249,84,73,214,76,246,92,85,2,103,3,38,59,126,135,125,137,136,86,94,131,87,132,420,486,504,93,129,90,127,140,88,60,138,139,153,154,39,54,52,96])). % 180.96/182.04 cnf(2937,plain, % 180.96/182.04 (P1(f15(a4))), % 180.96/182.04 inference(scs_inference,[],[75,2820,2816,563,2926,72,213,70,240,249,84,73,214,76,246,92,85,2,103,3,38,59,126,135,125,137,136,86,94,131,87,132,420,486,504,93,129,90,127,140,88,60,138,139,153,154,39,54,52,96,95])). % 180.96/182.04 cnf(2939,plain, % 180.96/182.04 (~P5(f12(a4),a13)), % 180.96/182.04 inference(scs_inference,[],[75,2820,2816,563,2926,72,213,70,240,249,84,73,214,76,246,92,85,2,103,3,38,59,126,135,125,137,136,86,94,131,87,132,420,486,504,93,129,90,127,140,88,60,138,139,153,154,39,54,52,96,95,101])). % 180.96/182.04 cnf(2941,plain, % 180.96/182.04 (P5(f10(a4),a1)), % 180.96/182.04 inference(scs_inference,[],[75,2803,2820,2816,563,2926,72,213,69,70,240,249,84,73,214,76,246,92,85,2,103,3,38,59,126,135,125,137,136,86,94,131,87,132,420,486,504,93,129,90,127,140,88,60,138,139,153,154,39,54,52,96,95,101,114])). % 180.96/182.04 cnf(2960,plain, % 180.96/182.04 (P10(f11(a4))), % 180.96/182.04 inference(scs_inference,[],[2916,2479])). % 180.96/182.04 cnf(2961,plain, % 180.96/182.04 (P12(a4,f11(a4),a13)), % 180.96/182.04 inference(scs_inference,[],[2916,2477])). % 180.96/182.04 cnf(2963,plain, % 180.96/182.04 (P8(f11(a4),f12(a4))), % 180.96/182.04 inference(scs_inference,[],[2916,2910,2477,97])). % 180.96/182.04 cnf(2965,plain, % 180.96/182.04 (~P16(f11(a4),a13)), % 180.96/182.04 inference(scs_inference,[],[2890,2916,2910,2477,97,131])). % 180.96/182.04 cnf(2967,plain, % 180.96/182.04 (~P9(f10(a4),a13)), % 180.96/182.04 inference(scs_inference,[],[2890,2916,2910,2477,97,131,132])). % 180.96/182.04 cnf(2969,plain, % 180.96/182.04 (~P8(f11(a4),f10(a4))), % 180.96/182.04 inference(scs_inference,[],[2890,2916,2910,2477,97,131,132,420])). % 180.96/182.04 cnf(2971,plain, % 180.96/182.04 (P14(a24,a24)), % 180.96/182.04 inference(scs_inference,[],[2908,2890,2916,2910,2477,97,131,132,420,87])). % 180.96/182.04 cnf(2973,plain, % 180.96/182.04 (~P12(f10(a4),a4,x29731)), % 180.96/182.04 inference(scs_inference,[],[2908,2890,2916,2910,2477,97,131,132,420,87,504])). % 180.96/182.04 cnf(2977,plain, % 180.96/182.04 (P15(f10(a4),f11(a4))), % 180.96/182.04 inference(scs_inference,[],[2908,2890,2916,2910,2477,97,131,132,420,87,504,486,129])). % 180.96/182.04 cnf(2979,plain, % 180.96/182.04 (P2(f12(a4))), % 180.96/182.04 inference(scs_inference,[],[2908,2890,2916,2910,2918,2477,97,131,132,420,87,504,486,129,85])). % 180.96/182.04 cnf(2981,plain, % 180.96/182.04 (P4(f10(a4))), % 180.96/182.04 inference(scs_inference,[],[2908,2890,2916,2886,2910,2918,2477,97,131,132,420,87,504,486,129,85,90])). % 180.96/182.04 cnf(2984,plain, % 180.96/182.04 (~P8(f12(a4),f10(a4))), % 180.96/182.04 inference(scs_inference,[],[2879,2908,2890,2902,2916,2886,2910,2918,2477,97,131,132,420,87,504,486,129,85,90,2,2402])). % 180.96/182.04 cnf(2989,plain, % 180.96/182.04 (~E(f10(a4),f12(a4))), % 180.96/182.04 inference(scs_inference,[],[2879,2908,2890,2902,2904,2916,2886,2910,2918,2477,97,131,132,420,87,504,486,129,85,90,2,2402,68,2448,53])). % 180.96/182.04 cnf(2990,plain, % 180.96/182.04 (~P12(a4,a4,a13)), % 180.96/182.04 inference(scs_inference,[],[2879,2908,2890,2902,2904,2884,2916,2886,2910,2918,2477,97,131,132,420,87,504,486,129,85,90,2,2402,68,2448,53,154])). % 180.96/182.04 cnf(2995,plain, % 180.96/182.04 (~P5(f12(a4),f15(a14))), % 180.96/182.04 inference(scs_inference,[],[2879,2908,2890,2925,2902,2904,2884,2916,2886,2910,2918,2939,78,246,2477,97,131,132,420,87,504,486,129,85,90,2,2402,68,2448,53,154,41,103,66])). % 180.96/182.04 cnf(2996,plain, % 180.96/182.04 (~E(f15(a4),f15(a14))), % 180.96/182.04 inference(scs_inference,[],[2879,2908,2890,2925,2902,2904,2884,2916,2886,2910,2918,2937,2939,78,249,246,2477,97,131,132,420,87,504,486,129,85,90,2,2402,68,2448,53,154,41,103,66,38])). % 180.96/182.04 cnf(2997,plain, % 180.96/182.04 (P5(f11(a4),a24)), % 180.96/182.04 inference(scs_inference,[],[2879,2908,2890,2925,2902,2904,2884,2916,2882,2886,2910,2918,2937,2939,78,70,249,246,2477,97,131,132,420,87,504,486,129,85,90,2,2402,68,2448,53,154,41,103,66,38,114])). % 180.96/182.04 cnf(3014,plain, % 180.96/182.04 (~P16(f10(a4),a13)), % 180.96/182.04 inference(scs_inference,[],[2977,2916,97,131])). % 180.96/182.04 cnf(3018,plain, % 180.96/182.04 (~P12(f11(a4),a4,x30181)), % 180.96/182.04 inference(scs_inference,[],[2977,2961,2916,97,131,420,504])). % 180.96/182.04 cnf(3022,plain, % 180.96/182.04 (P15(a4,f11(a4))), % 180.96/182.04 inference(scs_inference,[],[2977,2961,2916,97,131,420,504,486,129])). % 180.96/182.04 cnf(3027,plain, % 180.96/182.04 (~P12(f12(a4),f10(a4),x30271)), % 180.96/182.04 inference(scs_inference,[],[2932,2963,2977,2961,2910,2916,97,131,420,504,486,129,2,2405,2448])). % 180.96/182.04 cnf(3031,plain, % 180.96/182.04 (P8(f10(a4),f12(a4))), % 180.96/182.04 inference(scs_inference,[],[75,2932,2963,2977,2961,2910,2916,97,131,420,504,486,129,2,2405,2448,138,2402])). % 180.96/182.04 cnf(3033,plain, % 180.96/182.04 (~P11(a4,f12(a4),a13)), % 180.96/182.04 inference(scs_inference,[],[75,2932,2963,2977,2961,2910,2888,2916,97,131,420,504,486,129,2,2405,2448,138,2402,154])). % 180.96/182.04 cnf(3035,plain, % 180.96/182.04 (~P12(a4,a4,f15(a14))), % 180.96/182.04 inference(scs_inference,[],[75,2990,2932,2963,2977,2961,2910,2888,2916,246,97,131,420,504,486,129,2,2405,2448,138,2402,154,41])). % 180.96/182.04 cnf(3039,plain, % 180.96/182.04 (~P6(a14,a3)), % 180.96/182.04 inference(scs_inference,[],[75,2990,2932,2963,2977,2961,2813,2910,2888,2886,2916,72,80,246,97,131,420,504,486,129,2,2405,2448,138,2402,154,41,54,103,96])). % 180.96/182.04 cnf(3041,plain, % 180.96/182.04 (P16(f11(a4),a24)), % 180.96/182.04 inference(scs_inference,[],[75,2990,2932,2963,2977,2961,2960,2997,2813,2910,2888,2886,2916,72,80,246,97,131,420,504,486,129,2,2405,2448,138,2402,154,41,54,103,96,101])). % 180.96/182.04 cnf(3043,plain, % 180.96/182.04 (~E(a1,f15(a14))), % 180.96/182.04 inference(scs_inference,[],[75,2990,2932,2963,2977,2961,2960,2997,2813,2910,2888,2886,2916,72,80,69,249,246,97,131,420,504,486,129,2,2405,2448,138,2402,154,41,54,103,96,101,38])). % 180.96/182.04 cnf(3046,plain, % 180.96/182.04 (~E(a13,a3)), % 180.96/182.04 inference(scs_inference,[],[75,2990,2932,2963,2977,2961,2898,2960,2997,2813,2894,2937,2910,2888,2886,2916,72,80,69,249,246,97,131,420,504,486,129,2,2405,2448,138,2402,154,41,54,103,96,101,38,114,162])). % 180.96/182.04 cnf(3049,plain, % 180.96/182.04 (P12(f15(a14),a13,x30491)+~P11(f15(a14),f15(a14),x30491)), % 180.96/182.04 inference(scs_inference,[],[75,2990,2932,2963,2977,2961,2898,2960,2997,2813,2894,2937,2910,2888,2886,2916,72,80,69,249,246,97,131,420,504,486,129,2,2405,2448,138,2402,154,41,54,103,96,101,38,114,162,45,2401,140])). % 180.96/182.04 cnf(3052,plain, % 180.96/182.04 (P8(a4,f11(a4))), % 180.96/182.04 inference(scs_inference,[],[3022,97])). % 180.96/182.04 cnf(3058,plain, % 180.96/182.04 (P15(a4,f10(a4))), % 180.96/182.04 inference(scs_inference,[],[3022,2916,97,420,486,129])). % 180.96/182.04 cnf(3061,plain, % 180.96/182.04 (P10(f10(a4))), % 180.96/182.04 inference(scs_inference,[],[3046,3022,2916,97,420,486,129,2,88])). % 180.96/182.04 cnf(3066,plain, % 180.96/182.04 (P8(a4,f12(a4))), % 180.96/182.04 inference(scs_inference,[],[3046,2928,3022,2963,2916,2961,246,97,420,486,129,2,88,46,2448,105])). % 180.96/182.04 cnf(3073,plain, % 180.96/182.04 (~P6(f10(a4),f15(a14))), % 180.96/182.04 inference(scs_inference,[],[75,3046,3043,3018,2928,3022,2963,2888,2886,2916,2961,246,97,420,486,129,2,88,46,2448,105,153,138,103])). % 180.96/182.04 cnf(3076,plain, % 180.96/182.04 (P16(f10(a4),a1)), % 180.96/182.04 inference(scs_inference,[],[75,3046,3043,3018,2928,2941,3022,2963,2888,2886,2916,2961,246,242,97,420,486,129,2,88,46,2448,105,153,138,103,3,101])). % 180.96/182.04 cnf(3080,plain, % 180.96/182.04 (~E(f15(a4),a13)), % 180.96/182.04 inference(scs_inference,[],[75,3046,3043,3018,3031,2928,2941,3022,2963,2937,2888,2918,2886,2916,2961,83,246,242,97,420,486,129,2,88,46,2448,105,153,138,103,3,101,100,38])). % 180.96/182.04 cnf(3084,plain, % 180.96/182.04 (~P12(f12(a4),a4,x30841)), % 180.96/182.04 inference(scs_inference,[],[75,3046,3043,3018,3031,2928,2941,3022,2963,2937,2888,2918,2886,2916,2961,83,246,242,97,420,486,129,2,88,46,2448,105,153,138,103,3,101,100,38,241,2473,2405])). % 180.96/182.04 cnf(3095,plain, % 180.96/182.04 (~E(f11(a4),a4)), % 180.96/182.04 inference(scs_inference,[],[2984,2881,2973,3058,2890,97,2,67,40])). % 180.96/182.04 cnf(3097,plain, % 180.96/182.04 (~P6(f10(a4),a13)), % 180.96/182.04 inference(scs_inference,[],[2984,2881,2973,3073,3058,2890,242,97,2,67,40,43])). % 180.96/182.04 cnf(3100,plain, % 180.96/182.04 (~E(a24,f15(a14))), % 180.96/182.04 inference(scs_inference,[],[2984,2881,3066,2973,3073,3058,2918,70,2890,249,242,97,2,67,40,43,100,38])). % 180.96/182.04 cnf(3117,plain, % 180.96/182.04 (~E(f15(a14),f15(a4))), % 180.96/182.04 inference(scs_inference,[],[2996,2])). % 180.96/182.04 cnf(3133,plain, % 180.96/182.04 (~P11(a4,f11(a4),a13)), % 180.96/182.04 inference(scs_inference,[],[3080,2890,2916,2,154])). % 180.96/182.04 cnf(3135,plain, % 180.96/182.04 (~E(f12(a4),f9(a13,a14))), % 180.96/182.04 inference(scs_inference,[],[3080,2888,2890,2916,450,2,154,40])). % 180.96/182.04 cnf(3137,plain, % 180.96/182.04 (~P16(f11(a4),f15(a14))), % 180.96/182.04 inference(scs_inference,[],[2965,3080,2888,2890,2916,450,246,2,154,40,52])). % 180.96/182.04 cnf(3138,plain, % 180.96/182.04 (~P9(f11(a4),f15(a14))), % 180.96/182.04 inference(scs_inference,[],[2965,3080,2900,2888,2890,2916,450,246,2,154,40,52,58])). % 180.96/182.04 cnf(3151,plain, % 180.96/182.04 (~P16(f10(a4),f15(a14))), % 180.96/182.04 inference(scs_inference,[],[3014,3100,3033,3117,240,246,2,46,103,52])). % 180.96/182.04 cnf(3161,plain, % 180.96/182.04 (~P11(a4,f11(a4),f15(a14))), % 180.96/182.04 inference(scs_inference,[],[3135,3133,246,2,46])). % 180.96/182.04 cnf(3170,plain, % 180.96/182.04 (~E(f15(a14),a1)), % 180.96/182.04 inference(scs_inference,[],[3043,2])). % 180.96/182.04 cnf(3176,plain, % 180.96/182.04 (~E(a24,a2)), % 180.96/182.04 inference(scs_inference,[],[79,2])). % 180.96/182.04 cnf(3182,plain, % 180.96/182.04 (~E(f9(a13,a14),f11(a4))), % 180.96/182.04 inference(scs_inference,[],[2965,2810,82,2,51])). % 180.96/182.04 cnf(3183,plain, % 180.96/182.04 (~P6(f11(a4),a2)), % 180.96/182.04 inference(scs_inference,[],[3176,2965,2810,2882,82,2,51,103])). % 180.96/182.04 cnf(3204,plain, % 180.96/182.04 (~E(a24,a1)), % 180.96/182.04 inference(scs_inference,[],[77,2])). % 180.96/182.04 cnf(3214,plain, % 180.96/182.04 (~P6(f11(a4),a1)), % 180.96/182.04 inference(scs_inference,[],[3204,451,2884,2882,78,2,45,103])). % 180.96/182.04 cnf(3234,plain, % 180.96/182.04 (~E(a24,a3)), % 180.96/182.04 inference(scs_inference,[],[81,2])). % 180.96/182.04 cnf(3252,plain, % 180.96/182.04 (~P6(f11(a4),a3)), % 180.96/182.04 inference(scs_inference,[],[3234,3133,2884,2882,45,103])). % 180.96/182.04 cnf(3254,plain, % 180.96/182.04 (~P12(f10(a4),f10(a4),a13)), % 180.96/182.04 inference(scs_inference,[],[84,3234,2989,3133,2884,2882,73,76,75,45,103,141])). % 180.96/182.04 cnf(3256,plain, % 180.96/182.04 (~E(f11(a4),f10(a4))), % 180.96/182.04 inference(scs_inference,[],[84,3234,2989,3133,2884,2882,73,76,75,45,103,141,2])). % 180.96/182.04 cnf(3257,plain, % 180.96/182.04 (~P9(x32571,f15(a14))+~E(x32571,f11(a4))), % 180.96/182.04 inference(scs_inference,[],[84,3138,3234,2989,3133,2884,2882,73,76,75,45,103,141,2,57])). % 180.96/182.04 cnf(3261,plain, % 180.96/182.04 (~P12(f10(a4),f10(a4),f15(a14))), % 180.96/182.04 inference(scs_inference,[],[3254,246,41])). % 180.96/182.04 cnf(3292,plain, % 180.96/182.04 (~E(a13,a1)), % 180.96/182.04 inference(scs_inference,[],[3170,240,103,162])). % 180.96/182.04 cnf(3293,plain, % 180.96/182.04 (~E(a1,a13)), % 180.96/182.04 inference(scs_inference,[],[3170,240,103,162,2])). % 180.96/182.04 cnf(3329,plain, % 180.96/182.04 (~P15(f15(a14),a13)), % 180.96/182.04 inference(scs_inference,[],[242,54,2394])). % 180.96/182.04 cnf(3333,plain, % 180.96/182.04 (~P15(a13,a13)), % 180.96/182.04 inference(scs_inference,[],[3329,242,2822,53])). % 180.96/182.04 cnf(3343,plain, % 180.96/182.04 (~P8(f12(a4),x33431)+~E(x33431,f11(a4))), % 180.96/182.04 inference(scs_inference,[],[2902,68])). % 180.96/182.04 cnf(3349,plain, % 180.96/182.04 (~P12(x33491,f15(a14),x33492)+P12(x33491,a13,x33492)), % 180.96/182.04 inference(scs_inference,[],[246,40])). % 180.96/182.04 cnf(3376,plain, % 180.96/182.04 (~P12(f10(a4),x33761,f15(a14))+~E(x33761,f10(a4))), % 180.96/182.04 inference(scs_inference,[],[3261,2979,249,242,95,43,40])). % 180.96/182.04 cnf(3444,plain, % 180.96/182.04 (~P16(x34441,f15(a14))+~E(x34441,f11(a4))), % 180.96/182.04 inference(scs_inference,[],[3137,51])). % 180.96/182.04 cnf(3658,plain, % 180.96/182.04 (~P7(x36581,a14)+~P12(x36581,x36582,f15(a14))), % 180.96/182.04 inference(scs_inference,[],[240,139])). % 180.96/182.04 cnf(3695,plain, % 180.96/182.04 (~P15(f12(a4),x36951)+~E(x36951,f11(a4))), % 180.96/182.04 inference(scs_inference,[],[77,2904,3,54])). % 180.96/182.04 cnf(3709,plain, % 180.96/182.04 (~P12(f12(a4),x37091,x37092)+~E(x37091,f11(a4))), % 180.96/182.04 inference(scs_inference,[],[2906,40])). % 180.96/182.04 cnf(3717,plain, % 180.96/182.04 (~E(x37171,f10(a4))+~E(f11(a4),x37171)), % 180.96/182.04 inference(scs_inference,[],[3256,3])). % 180.96/182.04 cnf(3748,plain, % 180.96/182.04 (~P11(a4,x37481,f15(a14))+~E(x37481,f11(a4))), % 180.96/182.04 inference(scs_inference,[],[3161,45])). % 180.96/182.04 cnf(3749,plain, % 180.96/182.04 (~P9(x37491,a13)+~E(x37491,f11(a4))), % 180.96/182.04 inference(scs_inference,[],[2900,3161,45,57])). % 180.96/182.04 cnf(3755,plain, % 180.96/182.04 (~P12(a4,x37551,f15(a14))+~E(x37551,a4)), % 180.96/182.04 inference(scs_inference,[],[3035,40])). % 180.96/182.04 cnf(3756,plain, % 180.96/182.04 (~E(a4,x37561)+~P12(a4,x37561,f15(a14))), % 180.96/182.04 inference(scs_inference,[],[3035,40,2])). % 180.96/182.04 cnf(3765,plain, % 180.96/182.04 (~P11(f10(a4),x37651,a13)+~E(x37651,f12(a4))), % 180.96/182.04 inference(scs_inference,[],[2928,45])). % 180.96/182.04 cnf(3798,plain, % 180.96/182.04 (~E(f11(a4),x37981)+P4(x37981)), % 180.96/182.04 inference(scs_inference,[],[2912,2809,103,62])). % 180.96/182.04 cnf(3800,plain, % 180.96/182.04 (~P6(x38001,a2)+~E(x38001,f11(a4))), % 180.96/182.04 inference(scs_inference,[],[3183,42])). % 180.96/182.04 cnf(3826,plain, % 180.96/182.04 (~E(f11(a4),x38261)+~P6(x38261,a3)), % 180.96/182.04 inference(scs_inference,[],[3252,42,2])). % 180.96/182.04 cnf(4058,plain, % 180.96/182.04 (~E(x40581,f11(a4))+~E(x40581,a4)), % 180.96/182.04 inference(scs_inference,[],[3095,3,2])). % 180.96/182.04 cnf(4100,plain, % 180.96/182.05 (~E(x41001,f11(a4))+~E(f9(a13,a14),x41001)), % 180.96/182.05 inference(scs_inference,[],[3182,3])). % 180.96/182.05 cnf(4121,plain, % 180.96/182.05 (~E(x41211,f11(a4))+~E(a14,x41211)), % 180.96/182.05 inference(scs_inference,[],[2484,3])). % 180.96/182.05 cnf(4636,plain, % 180.96/182.05 (E(f16(f8(x46361,x46362,f18(a13,x46363,x46364)),x46365),f16(f8(x46361,x46362,f18(f15(a14),x46363,x46364)),x46365))), % 180.96/182.05 inference(scs_inference,[],[1803,4,27,32,33,8])). % 180.96/182.05 cnf(4659,plain, % 180.96/182.05 (E(f8(f8(x46591,x46592,f18(a13,x46593,x46594)),x46595,x46596),f8(f8(x46591,x46592,f18(f15(a14),x46593,x46594)),x46595,x46596))), % 180.96/182.05 inference(scs_inference,[],[1803,2890,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14])). % 180.96/182.05 cnf(4660,plain, % 180.96/182.05 (E(f8(x46601,f8(x46602,x46603,f18(a13,x46604,x46605)),x46606),f8(x46601,f8(x46602,x46603,f18(f15(a14),x46604,x46605)),x46606))), % 180.96/182.05 inference(scs_inference,[],[1803,2890,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15])). % 180.96/182.05 cnf(4661,plain, % 180.96/182.05 (E(f8(x46611,x46612,f8(x46613,x46614,f18(a13,x46615,x46616))),f8(x46611,x46612,f8(x46613,x46614,f18(f15(a14),x46615,x46616))))), % 180.96/182.05 inference(scs_inference,[],[1803,2890,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16])). % 180.96/182.05 cnf(4663,plain, % 180.96/182.05 (E(f23(x46631,f8(x46632,x46633,f18(a13,x46634,x46635)),x46636),f23(x46631,f8(x46632,x46633,f18(f15(a14),x46634,x46635)),x46636))), % 180.96/182.05 inference(scs_inference,[],[1803,2890,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18])). % 180.96/182.05 cnf(4672,plain, % 180.96/182.05 (P14(f7(a13,f10(a4),f11(a4)),a13)), % 180.96/182.05 inference(scs_inference,[],[1803,3076,2890,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149])). % 180.96/182.05 cnf(4676,plain, % 180.96/182.05 (P6(f23(a13,a4,f10(a4)),a13)), % 180.96/182.05 inference(scs_inference,[],[1803,3076,2890,2916,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149,113,148])). % 180.96/182.05 cnf(4678,plain, % 180.96/182.05 (P14(f8(a13,a4,f10(a4)),a13)), % 180.96/182.05 inference(scs_inference,[],[1803,3076,2890,2916,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149,113,148,150])). % 180.96/182.05 cnf(4682,plain, % 180.96/182.05 (P1(f16(f10(a4),a1))), % 180.96/182.05 inference(scs_inference,[],[1803,2941,3076,2890,2916,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149,113,148,150,112,104])). % 180.96/182.05 cnf(4686,plain, % 180.96/182.05 (P5(f11(a4),f8(a13,f10(a4),f11(a4)))), % 180.96/182.05 inference(scs_inference,[],[1803,2941,3076,2890,2916,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149,113,148,150,112,104,111,147])). % 180.96/182.05 cnf(4688,plain, % 180.96/182.05 (P5(f10(a4),f7(a13,f10(a4),f11(a4)))), % 180.96/182.05 inference(scs_inference,[],[1803,2941,3076,2890,2916,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149,113,148,150,112,104,111,147,146])). % 180.96/182.05 cnf(4692,plain, % 180.96/182.05 (P13(f11(a4),f23(a13,f10(a4),f11(a4)))), % 180.96/182.05 inference(scs_inference,[],[1803,2941,2912,3076,2890,2916,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149,113,148,150,112,104,111,147,146,86,144])). % 180.96/182.05 cnf(4694,plain, % 180.96/182.05 (P6(f11(a4),f15(f11(a4)))), % 180.96/182.05 inference(scs_inference,[],[1803,2941,2912,3076,2890,2916,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149,113,148,150,112,104,111,147,146,86,144,94])). % 180.96/182.05 cnf(4698,plain, % 180.96/182.05 (P6(f10(a4),f16(f10(a4),a1))), % 180.96/182.05 inference(scs_inference,[],[1803,2941,2912,3076,2890,2916,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149,113,148,150,112,104,111,147,146,86,144,94,87,108])). % 180.96/182.05 cnf(4704,plain, % 180.96/182.05 (P6(a14,f17(f9(a13,a14),a14))), % 180.96/182.05 inference(scs_inference,[],[1803,2941,2912,3076,2890,2916,2818,1384,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149,113,148,150,112,104,111,147,146,86,144,94,87,108,145,90,106])). % 180.96/182.05 cnf(4706,plain, % 180.96/182.05 (P16(f9(a13,a14),f17(f9(a13,a14),a14))), % 180.96/182.05 inference(scs_inference,[],[1803,2941,2912,3076,2890,2916,2818,1384,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149,113,148,150,112,104,111,147,146,86,144,94,87,108,145,90,106,109])). % 180.96/182.05 cnf(4713,plain, % 180.96/182.05 (P16(f9(a13,f23(a13,f10(a4),f11(a4))),a13)), % 180.96/182.05 inference(scs_inference,[],[1881,1803,2941,2912,3076,2890,2916,2818,1384,83,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149,113,148,150,112,104,111,147,146,86,144,94,87,108,145,90,106,109,93,2,120,119])). % 180.96/182.05 cnf(4715,plain, % 180.96/182.05 (P12(a4,f18(a4,f11(a4),a13),a13)), % 180.96/182.05 inference(scs_inference,[],[1881,1803,2941,2912,3076,3133,2890,2916,2961,2818,1384,83,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149,113,148,150,112,104,111,147,146,86,144,94,87,108,145,90,106,109,93,2,120,119,155])). % 180.96/182.05 cnf(4724,plain, % 180.96/182.05 (P12(f18(a4,f11(a4),a13),f11(a4),a13)), % 180.96/182.05 inference(scs_inference,[],[1881,1803,1802,2941,2912,3076,3133,2890,2916,2961,2818,1384,83,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149,113,148,150,112,104,111,147,146,86,144,94,87,108,145,90,106,109,93,2,120,119,155,139,138,3,156])). % 180.96/182.05 cnf(4728,plain, % 180.96/182.05 (P16(f12(a4),f8(a13,f11(a4),f12(a4)))), % 180.96/182.05 inference(scs_inference,[],[1881,1803,1802,2941,2912,3076,3133,2918,1367,2890,2813,2916,2961,2818,1384,83,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149,113,148,150,112,104,111,147,146,86,144,94,87,108,145,90,106,109,93,2,120,119,155,139,138,3,156,96,101])). % 180.96/182.05 cnf(4732,plain, % 180.96/182.05 (P12(f10(a4),f20(f10(a4),a13),a13)), % 180.96/182.05 inference(scs_inference,[],[1881,1803,1802,2941,2912,3076,2967,3133,2918,1367,2890,2813,2916,2961,2818,1384,83,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149,113,148,150,112,104,111,147,146,86,144,94,87,108,145,90,106,109,93,2,120,119,155,139,138,3,156,96,101,103,142])). % 180.96/182.05 cnf(4735,plain, % 180.96/182.05 (~P2(f23(a13,f10(a4),f11(a4)))), % 180.96/182.05 inference(scs_inference,[],[1881,1803,1802,2941,2912,3076,2967,3133,2918,1367,2890,2813,2916,2961,249,2818,1384,83,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149,113,148,150,112,104,111,147,146,86,144,94,87,108,145,90,106,109,93,2,120,119,155,139,138,3,156,96,101,103,142,38,95])). % 180.96/182.05 cnf(4737,plain, % 180.96/182.05 (P17(f9(a13,f23(a13,f10(a4),f11(a4))),f23(a13,f10(a4),f11(a4)))), % 180.96/182.05 inference(scs_inference,[],[1881,1803,1802,2941,2912,3076,2967,3133,2918,1367,2890,2813,2916,2961,249,2818,1384,83,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149,113,148,150,112,104,111,147,146,86,144,94,87,108,145,90,106,109,93,2,120,119,155,139,138,3,156,96,101,103,142,38,95,123])). % 180.96/182.05 cnf(4739,plain, % 180.96/182.05 (P12(f11(f10(a4)),f12(f10(a4)),a13)), % 180.96/182.05 inference(scs_inference,[],[1881,1803,1802,2941,2912,3076,2967,3133,2918,1367,2890,2813,2916,2961,249,2818,1384,2914,83,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149,113,148,150,112,104,111,147,146,86,144,94,87,108,145,90,106,109,93,2,120,119,155,139,138,3,156,96,101,103,142,38,95,123,137])). % 180.96/182.05 cnf(4741,plain, % 180.96/182.05 (P12(f10(f10(a4)),f11(f10(a4)),a13)), % 180.96/182.05 inference(scs_inference,[],[1881,1803,1802,2941,2912,3076,2967,3133,2918,1367,2890,2813,2916,2961,249,2818,1384,2914,83,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149,113,148,150,112,104,111,147,146,86,144,94,87,108,145,90,106,109,93,2,120,119,155,139,138,3,156,96,101,103,142,38,95,123,137,136])). % 180.96/182.05 cnf(4743,plain, % 180.96/182.05 (P6(f11(f10(a4)),a24)), % 180.96/182.05 inference(scs_inference,[],[1881,1803,1802,2941,2912,3076,2967,3133,2918,1367,2890,2813,2916,2961,249,2818,1384,2914,83,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149,113,148,150,112,104,111,147,146,86,144,94,87,108,145,90,106,109,93,2,120,119,155,139,138,3,156,96,101,103,142,38,95,123,137,136,126])). % 180.96/182.05 cnf(4745,plain, % 180.96/182.05 (~P16(f18(a4,f11(a4),a13),a13)), % 180.96/182.05 inference(scs_inference,[],[1881,1803,1802,2941,2912,3076,2967,3133,2918,1367,2890,2813,2916,2961,249,2818,1384,2914,83,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149,113,148,150,112,104,111,147,146,86,144,94,87,108,145,90,106,109,93,2,120,119,155,139,138,3,156,96,101,103,142,38,95,123,137,136,126,131])). % 180.96/182.05 cnf(4760,plain, % 180.96/182.05 (P15(a4,f18(a4,f11(a4),a13))), % 180.96/182.05 inference(scs_inference,[],[1881,1803,1802,2941,2912,3076,2967,3133,2918,1367,2890,2813,2916,2961,249,2818,1384,2914,83,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149,113,148,150,112,104,111,147,146,86,144,94,87,108,145,90,106,109,93,2,120,119,155,139,138,3,156,96,101,103,142,38,95,123,137,136,126,131,132,162,420,504,486,92,89,129])). % 180.96/182.05 cnf(4766,plain, % 180.96/182.05 (~P8(f12(a4),f18(a4,f11(a4),a13))), % 180.96/182.05 inference(scs_inference,[],[1881,1803,1802,2941,2912,3076,3254,2967,3133,2918,2963,1367,2890,2813,2916,2961,249,2818,1384,2914,83,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149,113,148,150,112,104,111,147,146,86,144,94,87,108,145,90,106,109,93,2,120,119,155,139,138,3,156,96,101,103,142,38,95,123,137,136,126,131,132,162,420,504,486,92,89,129,2360,153,2405])). % 180.96/182.05 cnf(4774,plain, % 180.96/182.05 (~E(f9(a13,a14),f18(a4,f11(a4),a13))), % 180.96/182.05 inference(scs_inference,[],[1881,1803,1802,2941,2912,3076,3254,2810,2967,3133,2918,2963,1367,2890,2813,2916,2961,249,2818,1384,2914,83,246,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149,113,148,150,112,104,111,147,146,86,144,94,87,108,145,90,106,109,93,2,120,119,155,139,138,3,156,96,101,103,142,38,95,123,137,136,126,131,132,162,420,504,486,92,89,129,2360,153,2405,58,154,41,60,39,51])). % 180.96/182.05 cnf(4776,plain, % 180.96/182.05 (~E(f23(a13,f10(a4),f11(a4)),f10(a4))), % 180.96/182.05 inference(scs_inference,[],[1881,1803,1802,3097,2941,2912,3076,3254,2810,2967,3133,2918,2963,1367,2890,2813,2916,2961,249,2818,1384,2874,2914,83,246,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149,113,148,150,112,104,111,147,146,86,144,94,87,108,145,90,106,109,93,2,120,119,155,139,138,3,156,96,101,103,142,38,95,123,137,136,126,131,132,162,420,504,486,92,89,129,2360,153,2405,58,154,41,60,39,51,47,42])). % 180.96/182.05 cnf(4780,plain, % 180.96/182.05 (P6(f10(f10(a4)),a1)), % 180.96/182.05 inference(scs_inference,[],[1881,1803,1802,2971,3097,2941,2912,3076,3254,2810,2967,3133,2918,2963,70,1367,2890,2813,2916,2961,249,2818,1384,2874,2914,240,83,246,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149,113,148,150,112,104,111,147,146,86,144,94,87,108,145,90,106,109,93,2,120,119,155,139,138,3,156,96,101,103,142,38,95,123,137,136,126,131,132,162,420,504,486,92,89,129,2360,153,2405,58,154,41,60,39,51,47,42,43,114,125])). % 180.96/182.05 cnf(4782,plain, % 180.96/182.05 (P11(f10(a4),f10(f10(a4)),a13)), % 180.96/182.05 inference(scs_inference,[],[1881,1803,1802,2971,3097,2941,2912,3076,3254,2810,2967,3133,2918,2963,70,1367,2890,2813,2916,2961,249,2818,1384,2874,2914,240,83,246,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149,113,148,150,112,104,111,147,146,86,144,94,87,108,145,90,106,109,93,2,120,119,155,139,138,3,156,96,101,103,142,38,95,123,137,136,126,131,132,162,420,504,486,92,89,129,2360,153,2405,58,154,41,60,39,51,47,42,43,114,125,135])). % 180.96/182.05 cnf(4790,plain, % 180.96/182.05 (P12(f10(a4),f10(f10(a4)),a13)), % 180.96/182.05 inference(scs_inference,[],[1881,1803,1802,2971,3097,2941,2912,3076,3254,2810,2967,3133,2918,2963,70,1367,2890,2813,2916,2961,249,2818,1384,2874,2914,240,83,246,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149,113,148,150,112,104,111,147,146,86,144,94,87,108,145,90,106,109,93,2,120,119,155,139,138,3,156,96,101,103,142,38,95,123,137,136,126,131,132,162,420,504,486,92,89,129,2360,153,2405,58,154,41,60,39,51,47,42,43,114,125,135,85,97,127,140])). % 180.96/182.05 cnf(4792,plain, % 180.96/182.05 (P10(f18(a4,f11(a4),a13))), % 180.96/182.05 inference(scs_inference,[],[1881,1803,1802,2971,3097,2941,2912,3076,3254,2810,2967,3133,2918,2963,70,1367,2890,2813,2916,2961,249,2818,1384,2874,2914,240,83,246,4,27,32,33,8,9,10,11,12,13,23,24,25,26,28,29,30,31,34,35,36,37,449,5,6,7,14,15,16,17,18,19,20,21,22,533,1614,149,113,148,150,112,104,111,147,146,86,144,94,87,108,145,90,106,109,93,2,120,119,155,139,138,3,156,96,101,103,142,38,95,123,137,136,126,131,132,162,420,504,486,92,89,129,2360,153,2405,58,154,41,60,39,51,47,42,43,114,125,135,85,97,127,140,88])). % 180.96/182.05 cnf(4803,plain, % 180.96/182.05 (~P12(f15(a14),a13,x48031)), % 180.96/182.05 inference(scs_inference,[],[3329,129])). % 180.96/182.05 cnf(4813,plain, % 180.96/182.05 (~P15(f12(a4),f18(a4,f11(a4),a13))), % 180.96/182.05 inference(scs_inference,[],[2813,2906,3329,4724,4735,4766,129,128,140,127,504,97])). % 180.96/182.05 cnf(4824,plain, % 180.96/182.05 (P6(f23(a13,a4,f10(a4)),f15(a14))), % 180.96/182.05 inference(scs_inference,[],[242,2813,2906,3076,2939,3329,4676,4782,4724,4735,4766,129,128,140,127,504,97,131,3349,85,3049,3765,1375,43])). % 180.96/182.05 cnf(4826,plain, % 180.96/182.05 (~P6(f23(a13,f10(a4),f11(a4)),a1)), % 180.96/182.05 inference(scs_inference,[],[242,1384,2813,2906,157,3076,2939,3329,3293,4676,4782,4724,4735,4766,129,128,140,127,504,97,131,3349,85,3049,3765,1375,43,42,103])). % 180.96/182.05 cnf(4828,plain, % 180.96/182.05 (~P5(f11(a4),a13)), % 180.96/182.05 inference(scs_inference,[],[242,1384,2813,2906,157,3076,2939,3329,3293,2965,2960,4676,4782,4724,4735,4766,129,128,140,127,504,97,131,3349,85,3049,3765,1375,43,42,103,101])). % 180.96/182.05 cnf(4830,plain, % 180.96/182.05 (P16(f9(a13,a14),f15(a14))), % 180.96/182.05 inference(scs_inference,[],[242,1384,2813,2906,157,3076,2939,3329,3293,2810,2965,2960,4676,4782,4724,4735,4766,129,128,140,127,504,97,131,3349,85,3049,3765,1375,43,42,103,101,52])). % 180.96/182.05 cnf(4833,plain, % 180.96/182.05 (~P6(f23(a13,f10(a4),f11(a4)),a24)), % 180.96/182.05 inference(scs_inference,[],[242,450,1384,2813,70,2906,157,3076,2939,3329,3293,2810,2965,2960,4676,4782,4724,4715,4735,4766,129,128,140,127,504,97,131,3349,85,3049,3765,1375,43,42,103,101,52,40,96])). % 180.96/182.05 cnf(4837,plain, % 180.96/182.05 (~E(f10(f10(a4)),f9(a13,a14))), % 180.96/182.05 inference(scs_inference,[],[242,450,214,1384,2813,70,2906,157,3076,2939,3329,451,3293,2810,2965,2960,4676,4782,4724,4715,4735,4760,4766,129,128,140,127,504,97,131,3349,85,3049,3765,1375,43,42,103,101,52,40,96,54,45])). % 180.96/182.05 cnf(4842,plain, % 180.96/182.05 (P12(a4,f11(a4),f15(a14))), % 180.96/182.05 inference(scs_inference,[],[242,450,214,1384,2961,2813,70,2906,157,3076,2939,3329,451,3293,2810,2965,2960,4676,4782,4724,4715,4735,4760,4672,4766,129,128,140,127,504,97,131,3349,85,3049,3765,1375,43,42,103,101,52,40,96,54,45,39,64,41])). % 180.96/182.05 cnf(4845,plain, % 180.96/182.05 (P12(a4,f12(a4),a13)), % 180.96/182.05 inference(scs_inference,[],[242,450,214,1384,2961,2888,2813,70,2906,157,3076,2939,3329,451,3293,2810,2965,2960,4676,4782,4724,4715,4735,4760,4672,4766,129,128,140,127,504,97,131,3349,85,3049,3765,1375,43,42,103,101,52,40,96,54,45,39,64,41,154,153])). % 180.96/182.05 cnf(4847,plain, % 180.96/182.05 (P11(a4,f10(a4),f15(a14))), % 180.96/182.05 inference(scs_inference,[],[242,450,214,1384,2961,2888,2813,70,2906,157,3076,2939,3329,451,3293,2810,2884,2965,2960,4676,4782,4724,4715,4735,4760,4672,4766,129,128,140,127,504,97,131,3349,85,3049,3765,1375,43,42,103,101,52,40,96,54,45,39,64,41,154,153,46])). % 180.96/182.05 cnf(4852,plain, % 180.96/182.05 (E(f10(f10(a4)),f11(a4))), % 180.96/182.05 inference(scs_inference,[],[73,75,242,76,450,214,2882,1384,84,2818,2961,2888,2813,70,2906,157,3076,2939,3329,451,3293,2810,2884,2965,2960,4676,4782,4724,4715,4790,4735,4760,4774,4672,4766,129,128,140,127,504,97,131,3349,85,3049,3765,1375,43,42,103,101,52,40,96,54,45,39,64,41,154,153,46,121,114,141])). % 180.96/182.05 cnf(4854,plain, % 180.96/182.05 (E(f11(a4),f10(f10(a4)))), % 180.96/182.05 inference(scs_inference,[],[73,75,242,76,450,214,2882,1384,84,2818,2961,2888,2813,70,2906,157,3076,2939,3329,451,3293,2810,2884,2965,2960,4676,4782,4724,4715,4790,4735,4760,4774,4672,4766,129,128,140,127,504,97,131,3349,85,3049,3765,1375,43,42,103,101,52,40,96,54,45,39,64,41,154,153,46,121,114,141,2])). % 180.96/182.05 cnf(4855,plain, % 180.96/182.05 (~P16(f23(a13,f10(a4),f11(a4)),x48551)), % 180.96/182.05 inference(scs_inference,[],[73,75,242,76,450,214,2882,1384,84,2818,2961,2888,2813,70,2906,157,3076,2939,3329,451,3293,2810,2884,2965,2960,4676,4782,4724,4715,4790,4735,4760,4774,4672,4766,129,128,140,127,504,97,131,3349,85,3049,3765,1375,43,42,103,101,52,40,96,54,45,39,64,41,154,153,46,121,114,141,2,89])). % 180.96/182.05 cnf(4857,plain, % 180.96/182.05 (~P15(x48571,f23(a13,f10(a4),f11(a4)))), % 180.96/182.05 inference(scs_inference,[],[73,75,242,76,450,214,2882,1384,84,2818,2961,2888,2813,70,2906,157,3076,2939,3329,451,3293,2810,2884,2965,2960,4676,4782,4724,4715,4790,4735,4760,4774,4672,4766,129,128,140,127,504,97,131,3349,85,3049,3765,1375,43,42,103,101,52,40,96,54,45,39,64,41,154,153,46,121,114,141,2,89,88])). % 180.96/182.05 cnf(4862,plain, % 180.96/182.05 (~P16(f10(f10(a4)),f15(a14))), % 180.96/182.05 inference(scs_inference,[],[73,75,242,76,450,214,2882,1384,84,2818,2961,2888,2813,70,2906,157,3076,2939,3329,451,3293,2810,2884,2965,2960,4676,4782,4724,4715,4790,4735,4760,4774,4672,4766,129,128,140,127,504,97,131,3349,85,3049,3765,1375,43,42,103,101,52,40,96,54,45,39,64,41,154,153,46,121,114,141,2,89,88,3257,3798,3343,3444])). % 180.96/182.05 cnf(4868,plain, % 180.96/182.05 (P5(f10(f10(a4)),a24)), % 180.96/182.05 inference(scs_inference,[],[73,75,242,76,450,214,2882,1384,84,2818,2961,2888,2813,70,2906,157,3076,2941,2939,3329,451,3293,2810,2884,2965,2997,2960,4676,4782,4724,4715,4790,4735,4760,4774,4672,4766,129,128,140,127,504,97,131,3349,85,3049,3765,1375,43,42,103,101,52,40,96,54,45,39,64,41,154,153,46,121,114,141,2,89,88,3257,3798,3343,3444,3695,3709,3717,4100,66,65])). % 180.96/182.05 cnf(4869,plain, % 180.96/182.05 (P10(f10(f10(a4)))), % 180.96/182.05 inference(scs_inference,[],[73,75,242,76,450,214,2882,1384,84,2818,2961,2888,2813,70,2906,157,3076,2941,2939,3329,451,3293,2810,2884,2965,2997,2960,4676,4782,4724,4715,4790,4735,4760,4774,4672,4766,129,128,140,127,504,97,131,3349,85,3049,3765,1375,43,42,103,101,52,40,96,54,45,39,64,41,154,153,46,121,114,141,2,89,88,3257,3798,3343,3444,3695,3709,3717,4100,66,65,59])). % 180.96/182.05 cnf(4870,plain, % 180.96/182.05 (P8(a4,f10(f10(a4)))), % 180.96/182.05 inference(scs_inference,[],[73,75,242,76,450,214,2882,1384,84,2818,2961,2888,2813,70,2906,157,3076,2941,2939,3329,451,3293,2810,2884,2965,3052,2997,2960,4676,4782,4724,4715,4790,4735,4760,4774,4672,4766,129,128,140,127,504,97,131,3349,85,3049,3765,1375,43,42,103,101,52,40,96,54,45,39,64,41,154,153,46,121,114,141,2,89,88,3257,3798,3343,3444,3695,3709,3717,4100,66,65,59,68])). % 180.96/182.05 cnf(4875,plain, % 180.96/182.05 (~P8(f10(f10(a4)),a4)), % 180.96/182.05 inference(scs_inference,[],[73,75,242,76,450,214,2882,1384,84,2818,2961,2888,2813,70,2906,2963,157,3076,2941,2910,2939,3329,451,3293,2810,2884,2965,3052,2997,2960,4676,4782,4724,4715,4790,4735,4760,4774,4672,4766,129,128,140,127,504,97,131,3349,85,3049,3765,1375,43,42,103,101,52,40,96,54,45,39,64,41,154,153,46,121,114,141,2,89,88,3257,3798,3343,3444,3695,3709,3717,4100,66,65,59,68,67,53,420,102])). % 180.96/182.05 cnf(4891,plain, % 180.96/182.05 (~P17(f23(a13,f10(a4),f11(a4)),x48911)), % 180.96/182.05 inference(scs_inference,[],[1803,3027,4735,3333,4855,129,2,128,140,109])). % 180.96/182.05 cnf(4894,plain, % 180.96/182.05 (~P12(f10(f10(a4)),f10(a4),x48941)), % 180.96/182.05 inference(scs_inference,[],[1803,3027,4735,3333,4790,4855,129,2,128,140,109,504])). % 180.96/182.05 cnf(4898,plain, % 180.96/182.05 (~P12(x48981,f11(a4),a24)), % 180.96/182.05 inference(scs_inference,[],[1803,3027,4735,3333,4790,3041,4855,4875,129,2,128,140,109,504,97,131])). % 180.96/182.05 cnf(4900,plain, % 180.96/182.05 (~P12(a13,f15(a14),x49001)), % 180.96/182.05 inference(scs_inference,[],[1803,3027,4735,3333,4790,3041,4855,4875,129,2,128,140,109,504,97,131,3349])). % 180.96/182.05 cnf(4909,plain, % 180.96/182.05 (~P5(f10(a4),a13)), % 180.96/182.05 inference(scs_inference,[],[2882,1803,1386,3027,2995,4735,2483,2816,3333,4790,4692,3014,3061,3041,4854,4694,4833,4686,4855,4875,4828,129,2,128,140,109,504,97,131,3349,1375,43,66,49,42,65,103,101])). % 180.96/182.05 cnf(4911,plain, % 180.96/182.05 (P16(f9(a13,f23(a13,f10(a4),f11(a4))),f15(a14))), % 180.96/182.05 inference(scs_inference,[],[242,2882,1803,1386,3027,2995,4735,2483,2816,3333,4790,4692,3014,3061,3041,4854,4694,4713,4833,4686,4855,4875,4828,129,2,128,140,109,504,97,131,3349,1375,43,66,49,42,65,103,101,52])). % 180.96/182.05 cnf(4917,plain, % 180.96/182.05 (E(f17(a13,f15(a14)),f17(f15(a14),a13))), % 180.96/182.05 inference(scs_inference,[],[242,754,450,216,2882,1803,1386,2888,858,3027,2995,4735,2483,2816,3333,4790,4692,3014,3061,3041,4854,4694,4732,4713,4833,4686,4855,4875,4828,129,2,128,140,109,504,97,131,3349,1375,43,66,49,42,65,103,101,52,40,51,39,3])). % 180.96/182.05 cnf(4920,plain, % 180.96/182.05 (P12(f11(a4),f12(a4),f15(a14))), % 180.96/182.05 inference(scs_inference,[],[242,754,450,216,2882,1803,1386,2888,858,3027,2995,4735,2483,2816,3333,4790,4692,3014,3061,3041,4854,4694,4732,4713,4833,4686,4855,4875,4828,129,2,128,140,109,504,97,131,3349,1375,43,66,49,42,65,103,101,52,40,51,39,3,41])). % 180.96/182.05 cnf(4927,plain, % 180.96/182.05 (P12(a4,f10(f10(a4)),a13)), % 180.96/182.05 inference(scs_inference,[],[242,754,450,216,2882,1384,1803,1386,2916,2888,858,3027,2995,4735,2483,2816,4782,3333,4790,4692,3014,3061,3041,4854,4694,4737,4732,4741,4713,4833,4686,4855,4678,4875,4828,129,2,128,140,109,504,97,131,3349,1375,43,66,49,42,65,103,101,52,40,51,39,3,41,64,154,138,46,153])). % 180.96/182.05 cnf(4929,plain, % 180.96/182.05 (~P8(f11(f10(a4)),a4)), % 180.96/182.05 inference(scs_inference,[],[242,754,450,216,2882,1384,1803,1386,2916,2888,858,3027,2995,4735,2483,2816,4782,3333,4790,4692,3014,3061,3041,4854,4694,4737,4732,4741,4713,4833,4870,4686,4855,4678,4875,4828,129,2,128,140,109,504,97,131,3349,1375,43,66,49,42,65,103,101,52,40,51,39,3,41,64,154,138,46,153,2405])). % 180.96/182.05 cnf(4933,plain, % 180.96/182.05 (~P14(a13,a1)), % 180.96/182.05 inference(scs_inference,[],[75,242,754,450,216,2882,2886,1384,1803,1386,2916,2818,2888,858,3027,69,2995,4735,2483,2816,4782,3333,4790,4692,3014,3061,3041,4854,4694,4737,4732,4741,4713,4837,4833,4870,4686,4855,4678,4875,4828,129,2,128,140,109,504,97,131,3349,1375,43,66,49,42,65,103,101,52,40,51,39,3,41,64,154,138,46,153,2405,121,114])). % 180.96/182.05 cnf(4952,plain, % 180.96/182.05 (E(f8(x49521,f15(f15(a14)),x49522),f8(x49521,f15(a13),x49522))), % 180.96/182.05 inference(scs_inference,[],[1802,4857,129,2])). % 180.96/182.05 cnf(4955,plain, % 180.96/182.05 (~P12(f11(f10(a4)),f10(f10(a4)),x49551)), % 180.96/182.05 inference(scs_inference,[],[3084,4741,1802,4857,129,2,140,504])). % 180.96/182.05 cnf(4957,plain, % 180.96/182.05 (~P15(f11(f10(a4)),a4)), % 180.96/182.05 inference(scs_inference,[],[3084,4741,1802,4929,4857,129,2,140,504,97])). % 180.96/182.05 cnf(4968,plain, % 180.96/182.05 (~E(f11(f10(a4)),f9(a13,a14))), % 180.96/182.05 inference(scs_inference,[],[450,2886,3084,3293,2960,4676,4741,1802,3097,3137,4698,4911,4826,4688,4929,4857,4909,129,2,140,504,97,131,43,66,42,103,101,40])). % 180.96/182.05 cnf(4970,plain, % 180.96/182.05 (P12(f11(a4),f11(f10(a4)),a13)), % 180.96/182.05 inference(scs_inference,[],[450,2886,3084,3293,2960,4676,4741,1802,3097,3137,4698,4911,4826,4688,4929,4857,4909,4852,129,2,140,504,97,131,43,66,42,103,101,40,39])). % 180.96/182.05 cnf(4971,plain, % 180.96/182.05 (E(f8(f8(x49711,x49712,f18(a13,x49713,x49714)),x49715,f18(a13,x49716,x49717)),f8(f8(x49711,x49712,f18(f15(a14),x49713,x49714)),x49715,f18(f15(a14),x49716,x49717)))), % 180.96/182.05 inference(scs_inference,[],[450,2886,1803,3084,3293,2960,4676,4741,1802,3097,3137,4659,4698,4911,4826,4688,4929,4857,4909,4852,129,2,140,504,97,131,43,66,42,103,101,40,39,3])). % 180.96/182.05 cnf(4974,plain, % 180.96/182.05 (P12(f10(a4),f10(f10(a4)),f15(a14))), % 180.96/182.05 inference(scs_inference,[],[242,450,2886,1803,3084,4790,3293,2960,4676,4741,1802,3097,3137,4659,4698,4911,4826,4688,4929,4857,4909,4852,129,2,140,504,97,131,43,66,42,103,101,40,39,3,41])). % 180.96/182.05 cnf(4977,plain, % 180.96/182.05 (P12(f10(a4),f11(f10(a4)),a13)), % 180.96/182.05 inference(scs_inference,[],[242,450,2886,1803,3084,4790,3293,2960,4676,4741,1802,4737,3097,3137,4659,4698,4911,4826,4688,4929,4857,4909,4891,4852,129,2,140,504,97,131,43,66,42,103,101,40,39,3,41,60,153])). % 180.96/182.05 cnf(4998,plain, % 180.96/182.05 (~P12(f20(f10(a4),a13),f10(a4),x49981)), % 180.96/182.05 inference(scs_inference,[],[2973,4732,140,504])). % 180.96/182.05 cnf(5002,plain, % 180.96/182.05 (E(f8(f8(x50021,x50022,f18(f15(a14),x50023,x50024)),x50025,x50026),f8(f8(x50021,x50022,f18(a13,x50023,x50024)),x50025,x50026))), % 180.96/182.05 inference(scs_inference,[],[2973,4659,4732,4706,140,504,131,2])). % 180.96/182.05 cnf(5008,plain, % 180.96/182.05 (~P5(f10(a4),f15(a14))), % 180.96/182.05 inference(scs_inference,[],[2973,2816,4854,3061,4659,4694,4732,3151,4824,4957,4706,140,504,131,2,129,42,103,101])). % 180.96/182.05 cnf(5014,plain, % 180.96/182.05 (E(f8(x50141,f15(f15(a14)),f18(a13,x50142,x50143)),f8(x50141,f15(a13),f18(f15(a14),x50142,x50143)))), % 180.96/182.05 inference(scs_inference,[],[450,1803,4790,2973,2816,4854,3061,4659,4694,4732,4739,3151,4952,4824,4955,4957,4706,140,504,131,2,129,42,103,101,40,39,3])). % 180.96/182.05 cnf(5017,plain, % 180.96/182.05 (P12(f10(f10(a4)),f11(f10(a4)),f15(a14))), % 180.96/182.05 inference(scs_inference,[],[242,450,1803,4741,4790,2973,2816,4854,3061,4659,4694,4732,4739,3151,4952,4824,4955,4957,4706,140,504,131,2,129,42,103,101,40,39,3,41])). % 180.96/182.05 cnf(5018,plain, % 180.96/182.05 (P12(a4,f20(f10(a4),a13),a13)), % 180.96/182.05 inference(scs_inference,[],[242,450,1803,2916,4741,4790,2973,2816,4854,3061,4659,4694,4732,4739,3151,4952,4824,4955,4957,4706,140,504,131,2,129,42,103,101,40,39,3,41,153])). % 180.96/182.05 cnf(5025,plain, % 180.96/182.05 (~P14(f15(a14),a1)), % 180.96/182.05 inference(scs_inference,[],[75,242,450,2886,1803,2818,2916,4741,69,4790,2973,2816,4782,4854,3061,4659,4694,4732,4739,3039,3151,4952,4824,4704,4968,4955,4957,4706,140,504,131,2,129,42,103,101,40,39,3,41,153,154,43,121,114])). % 180.96/182.05 cnf(5039,plain, % 180.96/182.05 (~P12(f12(f10(a4)),f11(f10(a4)),x50391)), % 180.96/182.05 inference(scs_inference,[],[3018,4739,140,504])). % 180.96/182.05 cnf(5041,plain, % 180.96/182.05 (~P12(x50411,f12(a4),f8(a13,f11(a4),f12(a4)))), % 180.96/182.05 inference(scs_inference,[],[3018,4739,4728,140,504,131])). % 180.96/182.05 cnf(5049,plain, % 180.96/182.05 (~P5(f10(f10(a4)),f15(a14))), % 180.96/182.05 inference(scs_inference,[],[81,3018,4739,4824,3073,4917,4743,4869,4862,4813,4728,140,504,131,2,129,42,103,101])). % 180.96/182.05 cnf(5054,plain, % 180.96/182.05 (E(f8(f8(x50541,x50542,f18(f15(a14),x50543,x50544)),x50545,f18(a13,x50546,x50547)),f8(f8(x50541,x50542,f18(a13,x50543,x50544)),x50545,f18(f15(a14),x50546,x50547)))), % 180.96/182.05 inference(scs_inference,[],[1803,81,4741,220,3018,4739,4824,3073,4917,5002,4743,5017,4869,4862,4813,4728,140,504,131,2,129,42,103,101,40,39,3])). % 180.96/182.05 cnf(5057,plain, % 180.96/182.05 (~E(a13,f8(a13,f11(a4),f12(a4)))), % 180.96/182.05 inference(scs_inference,[],[1803,2888,81,4741,220,3018,4739,4824,3073,4917,5002,4743,5017,4869,4862,4813,4728,140,504,131,2,129,42,103,101,40,39,3,41])). % 180.96/182.05 cnf(5058,plain, % 180.96/182.05 (P12(f10(f10(a4)),f12(f10(a4)),a13)), % 180.96/182.05 inference(scs_inference,[],[1803,2888,81,4741,220,3018,4739,4824,3073,4917,5002,4743,5017,4869,4862,4813,4728,140,504,131,2,129,42,103,101,40,39,3,41,153])). % 180.96/182.05 cnf(5071,plain, % 180.96/182.05 (~P11(a4,a4,a13)), % 180.96/182.05 inference(scs_inference,[],[2990,140])). % 180.96/182.05 cnf(5074,plain, % 180.96/182.05 (~P12(f11(f10(a4)),f10(a4),x50741)), % 180.96/182.05 inference(scs_inference,[],[2990,4971,4977,140,2,504])). % 180.96/182.05 cnf(5079,plain, % 180.96/182.05 (~P6(f10(f10(a4)),a13)), % 180.96/182.05 inference(scs_inference,[],[2990,3292,4927,4955,4833,4743,4971,4780,4977,140,2,504,42,39,103])). % 180.96/182.05 cnf(5087,plain, % 180.96/182.05 (P12(f10(a4),f11(f10(a4)),f15(a14))), % 180.96/182.05 inference(scs_inference,[],[242,4732,2990,3292,1802,4927,4955,4833,4743,5017,4971,4780,4977,4792,4745,4974,140,2,504,42,39,103,41,3,101,153])). % 180.96/182.05 cnf(5116,plain, % 180.96/182.05 (P12(f11(f10(a4)),f12(f10(a4)),f15(a14))), % 180.96/182.05 inference(scs_inference,[],[242,4739,1802,3254,4977,4826,4780,5054,5087,5039,5018,2,140,3376,504,42,39,3,41])). % 180.96/182.05 cnf(5117,plain, % 180.96/182.05 (P12(a4,f11(f10(a4)),a13)), % 180.96/182.05 inference(scs_inference,[],[242,2916,4739,1802,3254,4977,4826,4780,5054,5087,5039,5018,2,140,3376,504,42,39,3,41,153])). % 180.96/182.05 cnf(5138,plain, % 180.96/182.05 (E(f8(x51381,f8(x51382,x51383,f18(a13,x51384,x51385)),f18(a13,x51386,x51387)),f8(x51381,f8(x51382,x51383,f18(f15(a14),x51384,x51385)),f18(f15(a14),x51386,x51387)))), % 180.96/182.05 inference(scs_inference,[],[242,1803,3035,4927,5039,5014,4660,5117,5058,2,140,504,39,41,3])). % 180.96/182.05 cnf(5157,plain, % 180.96/182.05 (E(f8(x51571,f8(x51572,x51573,f18(f15(a14),x51574,x51575)),x51576),f8(x51571,f8(x51572,x51573,f18(a13,x51574,x51575)),x51576))), % 180.96/182.05 inference(scs_inference,[],[4660,2])). % 180.96/182.05 cnf(5162,plain, % 180.96/182.05 (P12(f11(a4),f12(f10(a4)),a13)), % 180.96/182.05 inference(scs_inference,[],[3261,4660,5058,4852,4970,2,140,504,39])). % 180.96/182.05 cnf(5188,plain, % 180.96/182.05 (E(f8(x51881,x51882,f8(x51883,x51884,f18(f15(a14),x51885,x51886))),f8(x51881,x51882,f8(x51883,x51884,f18(a13,x51885,x51886))))), % 180.96/182.05 inference(scs_inference,[],[4661,2])). % 180.96/182.05 cnf(5197,plain, % 180.96/182.05 (P12(f10(f10(a4)),f12(f10(a4)),f15(a14))), % 180.96/182.05 inference(scs_inference,[],[242,5039,5058,4661,4970,5162,2,140,504,2477,39,41])). % 180.96/182.05 cnf(5198,plain, % 180.96/182.05 (E(f8(x51981,f8(x51982,x51983,f18(f15(a14),x51984,x51985)),f18(a13,x51986,x51987)),f8(x51981,f8(x51982,x51983,f18(a13,x51984,x51985)),f18(f15(a14),x51986,x51987)))), % 180.96/182.05 inference(scs_inference,[],[242,1803,5039,5058,4661,4970,5157,5162,2,140,504,2477,39,41,3])). % 180.96/182.05 cnf(5203,plain, % 180.96/182.05 (P12(f10(a4),f12(f10(a4)),a13)), % 180.96/182.05 inference(scs_inference,[],[242,1803,4739,4790,5039,5058,4661,4970,5157,5162,2,140,504,2477,39,41,3,154,153])). % 180.96/182.05 cnf(5215,plain, % 180.96/182.05 (P12(f11(a4),f12(f10(a4)),f15(a14))), % 180.96/182.05 inference(scs_inference,[],[4955,4852,5138,5197,5203,2,140,504,39])). % 180.96/182.05 cnf(5216,plain, % 180.96/182.05 (P12(f11(a4),f11(f10(a4)),f15(a14))), % 180.96/182.05 inference(scs_inference,[],[242,4970,4955,4852,5138,5197,5203,2,140,504,39,41])). % 180.96/182.05 cnf(5222,plain, % 180.96/182.05 (P12(a4,f12(f10(a4)),a13)), % 180.96/182.05 inference(scs_inference,[],[242,2961,1802,4970,5017,4955,4852,5162,4974,5188,5138,5197,5203,2,140,504,39,41,3,154,153])). % 180.96/182.05 cnf(5245,plain, % 180.96/182.05 (P12(f10(f10(a4)),f12(a4),f15(a14))), % 180.96/182.05 inference(scs_inference,[],[4854,5198,5222,4998,4920,2,140,504,39])). % 180.96/182.05 cnf(5256,plain, % 180.96/182.05 (E(a13,f17(f9(a13,a14),a14))), % 180.96/182.05 inference(scs_inference,[],[75,242,631,4854,5203,4704,5116,5198,4636,5215,5216,5222,4998,4920,4842,2,140,504,39,41,3,154,153,3376,42,103])). % 180.96/182.05 cnf(5260,plain, % 180.96/182.05 (E(f16(f8(x52601,x52602,f18(f15(a14),x52603,x52604)),x52605),f16(f8(x52601,x52602,f18(a13,x52603,x52604)),x52605))), % 180.96/182.05 inference(scs_inference,[],[4636,2])). % 180.96/182.05 cnf(5264,plain, % 180.96/182.05 (P12(a4,f18(a4,f11(a4),a13),f15(a14))), % 180.96/182.05 inference(scs_inference,[],[242,74,4636,4715,5256,4894,2,140,48,41])). % 180.96/182.05 cnf(5272,plain, % 180.96/182.05 (P14(f15(a14),f17(f9(a13,a14),a14))), % 180.96/182.05 inference(scs_inference,[],[242,246,74,4636,5215,4715,4920,4842,5256,4894,2,140,48,41,3,154,153,3756,234,236])). % 180.96/182.05 cnf(5284,plain, % 180.96/182.05 (E(f17(f9(a13,a14),a14),a13)), % 180.96/182.05 inference(scs_inference,[],[5256,2])). % 180.96/182.05 cnf(5289,plain, % 180.96/182.05 (E(f16(f8(x52891,x52892,f18(f15(a14),x52893,x52894)),a13),f16(f8(x52891,x52892,f18(a13,x52893,x52894)),f15(a14)))), % 180.96/182.05 inference(scs_inference,[],[631,5256,4920,5260,5074,5041,2,140,41,3])). % 180.96/182.05 cnf(5292,plain, % 180.96/182.05 (~P12(f18(a4,f11(a4),a13),f10(a4),f15(a14))), % 180.96/182.05 inference(scs_inference,[],[631,5256,4920,5260,5264,5074,5041,4847,2,140,41,3,154])). % 180.96/182.05 cnf(5297,plain, % 180.96/182.05 (~P1(f17(f9(a13,a14),a14))), % 180.96/182.05 inference(scs_inference,[],[83,631,5256,4920,4974,5260,5264,5074,5025,5272,5245,5041,4847,2,140,41,3,154,153,64,38])). % 180.96/182.05 cnf(5305,plain, % 180.96/182.05 (P12(a4,f20(f10(a4),a13),f15(a14))), % 180.96/182.05 inference(scs_inference,[],[242,5041,5018,5289,2,140,41])). % 180.96/182.05 cnf(5388,plain, % 180.96/182.05 (~P11(a13,f15(a14),x53881)), % 180.96/182.05 inference(scs_inference,[],[4663,4900,2,140])). % 180.96/182.05 cnf(5574,plain, % 180.96/182.05 (~P11(x55741,f11(a4),a24)), % 180.96/182.05 inference(scs_inference,[],[1366,4898,2,140])). % 180.96/182.05 cnf(5863,plain, % 180.96/182.05 (E(f22(x58631,f16(f15(a14),x58632)),f22(x58631,f16(a13,x58632)))), % 180.96/182.05 inference(scs_inference,[],[1360,2])). % 180.96/182.05 cnf(5879,plain, % 180.96/182.05 (~P14(f15(a14),f16(f10(a4),a1))), % 180.96/182.05 inference(scs_inference,[],[4698,1359,4682,1361,5863,5008,2,3,114])). % 180.96/182.05 cnf(7868,plain, % 180.96/182.05 ($false), % 180.96/182.05 inference(scs_inference,[],[73,69,70,75,4933,5071,4776,5057,5079,5879,5388,5574,4792,4869,3214,2935,5292,5297,5049,2896,2965,5284,4694,3161,4868,4803,2981,2803,2900,2969,4780,4743,4824,2997,4735,5222,5162,2810,5245,4724,4854,5305,2818,4830,3329,4845,4870,2977,4847,4852,4842,242,246,4121,4058,3658,3826,3800,3755,3749,3748,150,23,113,32,28,22,6,27,35,18,16,149,104,37,36,31,21,34,33,26,112,24,12,85,111,30,14,7,19,17,15,4,147,2423,29,20,5,25,8,146,1375,144,86,94,155,43,139,420,138,46,44,108,60,156,54,45,145,2448,51,96,90,52,142,47,95,131,92,236,101,38,100,486,66,114,103,63,67,40,148,504,93,41,129,140,88,3,42]), % 180.96/182.05 ['proof']). % 180.96/182.05 % SZS output end Proof % 180.96/182.05 % Total time :180.190000s %------------------------------------------------------------------------------