%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PRO014+2 : TPTP v8.2.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n021.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:47 EDT 2024 % Result : Theorem 116.86s 117.01s % Output : CNFRefutation 116.86s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : PRO014+2 : TPTP v8.2.0. Released v4.0.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.11/0.32 % Computer : n021.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 300 % 0.11/0.32 % DateTime : Thu Jun 20 06:19:23 EDT 2024 % 0.11/0.33 % CPUTime : % 0.52/0.57 start to proof:theBenchmark % 116.76/116.99 %------------------------------------------- % 116.76/116.99 % File :CSE---1.7 % 116.76/116.99 % Problem :theBenchmark % 116.76/116.99 % Transform :cnf % 116.76/116.99 % Format :tptp:raw % 116.76/116.99 % Command :java -jar mcs_scs.jar %d %s % 116.76/116.99 % 116.76/116.99 % Result :Theorem 116.180000s % 116.76/116.99 % Output :CNFRefutation 116.180000s % 116.76/116.99 %------------------------------------------- % 116.76/117.00 %------------------------------------------------------------------------------ % 116.76/117.00 % File : PRO014+2 : TPTP v8.2.0. Released v4.0.0. % 116.76/117.00 % Domain : Processes % 116.76/117.00 % Problem : PSL cliff problem coe-7.2.1 % 116.76/117.00 % Version : Especial : Reduced > Especial. % 116.76/117.00 % English : % 116.76/117.00 % Refs : [Hal09] Halcomb (2009), Email to G. Sutcliffe % 116.76/117.00 % Source : [Hal09] % 116.76/117.00 % Names : minimal-subset-p9__coe-7.2.1-pd [Hal09] % 116.76/117.00 % 116.76/117.00 % Status : Theorem % 116.76/117.00 % Rating : 0.25 v8.2.0, 0.22 v7.5.0, 0.25 v7.4.0, 0.20 v7.3.0, 0.14 v7.2.0, 0.10 v7.1.0, 0.13 v7.0.0, 0.17 v6.4.0, 0.19 v6.3.0, 0.21 v6.2.0, 0.24 v6.1.0, 0.27 v6.0.0, 0.30 v5.4.0, 0.32 v5.3.0, 0.30 v5.2.0, 0.25 v5.1.0, 0.24 v5.0.0, 0.25 v4.1.0, 0.26 v4.0.1, 0.30 v4.0.0 % 116.76/117.00 % Syntax : Number of formulae : 46 ( 12 unt; 0 def) % 116.76/117.00 % Number of atoms : 143 ( 10 equ) % 116.76/117.00 % Maximal formula atoms : 12 ( 3 avg) % 116.76/117.00 % Number of connectives : 116 ( 19 ~; 5 |; 57 &) % 116.76/117.00 % ( 7 <=>; 28 =>; 0 <=; 0 <~>) % 116.76/117.00 % Maximal formula depth : 13 ( 5 avg) % 116.76/117.00 % Maximal term depth : 1 ( 1 avg) % 116.76/117.00 % Number of predicates : 18 ( 17 usr; 0 prp; 1-3 aty) % 116.76/117.00 % Number of functors : 5 ( 5 usr; 5 con; 0-0 aty) % 116.76/117.00 % Number of variables : 104 ( 83 !; 21 ?) % 116.76/117.00 % SPC : FOF_THM_RFO_SEQ % 116.76/117.00 % 116.76/117.00 % Comments : % 116.76/117.00 %------------------------------------------------------------------------------ % 116.76/117.00 fof(sos,axiom, % 116.76/117.00 ! [X0,X1,X2,X3] : % 116.76/117.00 ( ( min_precedes(X0,X1,X3) % 116.76/117.00 & min_precedes(X1,X2,X3) ) % 116.76/117.00 => min_precedes(X0,X2,X3) ) ). % 116.76/117.00 % 116.76/117.00 fof(sos_01,axiom, % 116.76/117.00 ! [X4,X5,X6] : % 116.76/117.00 ( ( earlier(X4,X5) % 116.76/117.00 & earlier(X5,X6) ) % 116.76/117.00 => earlier(X4,X6) ) ). % 116.76/117.00 % 116.76/117.00 fof(sos_02,axiom, % 116.76/117.00 ! [X7,X8,X9,X10] : % 116.76/117.00 ( ( occurrence_of(X9,X10) % 116.76/117.00 & root_occ(X7,X9) % 116.76/117.00 & root_occ(X8,X9) ) % 116.76/117.00 => X7 = X8 ) ). % 116.76/117.00 % 116.76/117.00 fof(sos_03,axiom, % 116.76/117.00 ! [X11,X12,X13,X14] : % 116.76/117.00 ( ( occurrence_of(X13,X14) % 116.76/117.00 & ~ atomic(X14) % 116.76/117.00 & leaf_occ(X11,X13) % 116.76/117.00 & leaf_occ(X12,X13) ) % 116.76/117.01 => X11 = X12 ) ). % 116.76/117.01 % 116.76/117.01 fof(sos_04,axiom, % 116.76/117.01 ! [X15,X16,X17] : % 116.76/117.01 ( next_subocc(X15,X16,X17) % 116.76/117.01 <=> ( min_precedes(X15,X16,X17) % 116.76/117.01 & ~ ? [X18] : % 116.76/117.01 ( min_precedes(X15,X18,X17) % 116.76/117.01 & min_precedes(X18,X16,X17) ) ) ) ). % 116.76/117.01 % 116.76/117.01 fof(sos_05,axiom, % 116.76/117.01 ! [X19,X20,X21] : % 116.76/117.01 ( next_subocc(X19,X20,X21) % 116.76/117.01 => ( arboreal(X19) % 116.76/117.01 & arboreal(X20) ) ) ). % 116.76/117.01 % 116.76/117.01 fof(sos_06,axiom, % 116.76/117.01 ! [X22,X23,X24] : % 116.76/117.01 ( min_precedes(X22,X23,X24) % 116.76/117.01 => precedes(X22,X23) ) ). % 116.76/117.01 % 116.76/117.01 fof(sos_07,axiom, % 116.76/117.01 ! [X25,X26,X27] : % 116.76/117.01 ( min_precedes(X25,X26,X27) % 116.76/117.01 => ~ root(X26,X27) ) ). % 116.76/117.01 % 116.76/117.01 fof(sos_08,axiom, % 116.76/117.01 ! [X28,X29] : % 116.76/117.01 ( precedes(X28,X29) % 116.76/117.01 <=> ( earlier(X28,X29) % 116.76/117.01 & legal(X29) ) ) ). % 116.76/117.01 % 116.76/117.01 fof(sos_09,axiom, % 116.76/117.01 ! [X30,X31] : % 116.76/117.01 ( earlier(X30,X31) % 116.76/117.01 => ~ earlier(X31,X30) ) ). % 116.76/117.01 % 116.76/117.01 fof(sos_10,axiom, % 116.76/117.01 ! [X32,X33] : % 116.76/117.01 ( root_occ(X32,X33) % 116.76/117.01 <=> ? [X34] : % 116.76/117.01 ( occurrence_of(X33,X34) % 116.76/117.01 & subactivity_occurrence(X32,X33) % 116.76/117.01 & root(X32,X34) ) ) ). % 116.76/117.01 % 116.76/117.01 fof(sos_11,axiom, % 116.76/117.01 ! [X35,X36] : % 116.76/117.01 ( leaf_occ(X35,X36) % 116.76/117.01 <=> ? [X37] : % 116.76/117.01 ( occurrence_of(X36,X37) % 116.76/117.01 & subactivity_occurrence(X35,X36) % 116.76/117.01 & leaf(X35,X37) ) ) ). % 116.76/117.01 % 116.76/117.01 fof(sos_12,axiom, % 116.76/117.01 ! [X38,X39] : % 116.76/117.01 ( root(X38,X39) % 116.76/117.01 => legal(X38) ) ). % 116.76/117.01 % 116.76/117.01 fof(sos_13,axiom, % 116.76/117.01 ! [X40,X41] : % 116.76/117.01 ( occurrence_of(X40,X41) % 116.76/117.01 => ( arboreal(X40) % 116.76/117.01 <=> atomic(X41) ) ) ). % 116.76/117.01 % 116.76/117.01 fof(sos_14,axiom, % 116.76/117.01 ! [X42,X43] : % 116.76/117.01 ( leaf(X42,X43) % 116.76/117.01 <=> ( ( root(X42,X43) % 116.76/117.01 | ? [X44] : min_precedes(X44,X42,X43) ) % 116.76/117.01 & ~ ? [X45] : min_precedes(X42,X45,X43) ) ) ). % 116.76/117.01 % 116.76/117.01 fof(sos_15,axiom, % 116.76/117.01 ! [X46,X47] : % 116.76/117.01 ( atocc(X46,X47) % 116.76/117.01 <=> ? [X48] : % 116.76/117.01 ( subactivity(X47,X48) % 116.76/117.01 & atomic(X48) % 116.76/117.01 & occurrence_of(X46,X48) ) ) ). % 116.76/117.01 % 116.76/117.01 fof(sos_16,axiom, % 116.76/117.01 ! [X49,X50] : % 116.76/117.01 ( ( atocc(X49,X50) % 116.76/117.01 & legal(X49) ) % 116.76/117.01 => root(X49,X50) ) ). % 116.76/117.01 % 116.76/117.01 fof(sos_17,axiom, % 116.76/117.01 ! [X51] : % 116.76/117.01 ( legal(X51) % 116.76/117.01 => arboreal(X51) ) ). % 116.76/117.01 % 116.76/117.01 fof(sos_18,axiom, % 116.76/117.01 ! [X52] : % 116.76/117.01 ( activity_occurrence(X52) % 116.76/117.01 => ? [X53] : % 116.76/117.01 ( activity(X53) % 116.76/117.01 & occurrence_of(X52,X53) ) ) ). % 116.76/117.01 % 116.76/117.01 fof(sos_19,axiom, % 116.76/117.01 ! [X54,X55] : % 116.76/117.01 ( subactivity_occurrence(X54,X55) % 116.76/117.01 => ( activity_occurrence(X54) % 116.76/117.01 & activity_occurrence(X55) ) ) ). % 116.76/117.01 % 116.76/117.01 fof(sos_20,axiom, % 116.76/117.01 ! [X56,X57,X58] : % 116.76/117.01 ( ( occurrence_of(X56,X58) % 116.76/117.01 & root_occ(X57,X56) ) % 116.76/117.01 => ~ ? [X59] : min_precedes(X59,X57,X58) ) ). % 116.76/117.01 % 116.76/117.01 fof(sos_21,axiom, % 116.76/117.01 ! [X60,X61,X62] : % 116.76/117.01 ( ( occurrence_of(X60,X62) % 116.76/117.01 & leaf_occ(X61,X60) ) % 116.76/117.01 => ~ ? [X63] : min_precedes(X61,X63,X62) ) ). % 116.76/117.01 % 116.76/117.01 fof(sos_22,axiom, % 116.76/117.01 ! [X64,X65,X66] : % 116.76/117.01 ( ( occurrence_of(X64,X65) % 116.76/117.01 & occurrence_of(X64,X66) ) % 116.76/117.01 => X65 = X66 ) ). % 116.76/117.01 % 116.76/117.01 fof(sos_23,axiom, % 116.76/117.01 ! [X67,X68] : % 116.76/117.01 ( ( leaf(X67,X68) % 116.76/117.01 & ~ atomic(X68) ) % 116.76/117.01 => ? [X69] : % 116.76/117.01 ( occurrence_of(X69,X68) % 116.76/117.01 & leaf_occ(X67,X69) ) ) ). % 116.76/117.01 % 116.76/117.01 fof(sos_24,axiom, % 116.76/117.01 ! [X70,X71,X72] : % 116.76/117.01 ( min_precedes(X71,X72,X70) % 116.76/117.01 => ? [X73] : % 116.76/117.01 ( occurrence_of(X73,X70) % 116.76/117.01 & subactivity_occurrence(X71,X73) % 116.76/117.01 & subactivity_occurrence(X72,X73) ) ) ). % 116.76/117.01 % 116.76/117.01 fof(sos_25,axiom, % 116.76/117.01 ! [X74,X75] : % 116.76/117.01 ( ( leaf(X74,X75) % 116.76/117.01 & ~ atomic(X75) ) % 116.76/117.01 => ? [X76] : % 116.76/117.01 ( occurrence_of(X76,X75) % 116.76/117.01 & leaf_occ(X74,X76) ) ) ). % 116.76/117.01 % 116.76/117.01 fof(sos_26,axiom, % 116.76/117.01 ! [X77,X78,X79] : % 116.76/117.01 ( min_precedes(X78,X79,X77) % 116.76/117.01 => ? [X80,X81] : % 116.76/117.01 ( subactivity(X80,X77) % 116.76/117.01 & subactivity(X81,X77) % 116.76/117.01 & atocc(X78,X80) % 116.76/117.01 & atocc(X79,X81) ) ) ). % 116.76/117.01 % 116.76/117.01 fof(sos_27,axiom, % 116.76/117.01 ! [X82,X83] : % 116.76/117.01 ( root(X83,X82) % 116.76/117.01 => ? [X84] : % 116.76/117.01 ( subactivity(X84,X82) % 116.76/117.01 & atocc(X83,X84) ) ) ). % 116.76/117.01 % 116.76/117.01 fof(sos_28,axiom, % 116.76/117.01 ! [X85,X86,X87,X88] : % 116.76/117.01 ( ( occurrence_of(X86,X85) % 116.76/117.01 & arboreal(X87) % 116.76/117.01 & arboreal(X88) % 116.76/117.01 & subactivity_occurrence(X87,X86) % 116.76/117.01 & subactivity_occurrence(X88,X86) ) % 116.76/117.01 => ( min_precedes(X87,X88,X85) % 116.76/117.01 | min_precedes(X88,X87,X85) % 116.76/117.01 | X87 = X88 ) ) ). % 116.76/117.01 % 116.76/117.01 fof(sos_29,axiom, % 116.76/117.01 ! [X89,X90] : % 116.76/117.01 ( occurrence_of(X90,X89) % 116.76/117.01 => ( activity(X89) % 116.76/117.01 & activity_occurrence(X90) ) ) ). % 116.76/117.01 % 116.76/117.01 fof(sos_30,axiom, % 116.76/117.01 ! [X91,X92] : % 116.76/117.01 ( ( occurrence_of(X92,X91) % 116.76/117.01 & ~ atomic(X91) ) % 116.76/117.01 => ? [X93] : % 116.76/117.01 ( root(X93,X91) % 116.76/117.01 & subactivity_occurrence(X93,X92) ) ) ). % 116.76/117.01 % 116.76/117.01 fof(sos_31,axiom, % 116.76/117.01 ! [X94] : % 116.76/117.01 ( activity(X94) % 116.86/117.01 => subactivity(X94,X94) ) ). % 116.86/117.01 % 116.86/117.01 fof(sos_32,axiom, % 116.86/117.01 ! [X95,X96] : % 116.86/117.01 ( ( occurrence_of(X96,tptp0) % 116.86/117.01 & subactivity_occurrence(X95,X96) % 116.86/117.01 & arboreal(X95) % 116.86/117.01 & ~ leaf_occ(X95,X96) ) % 116.86/117.01 => ? [X97,X98,X99] : % 116.86/117.01 ( occurrence_of(X97,tptp3) % 116.86/117.01 & next_subocc(X95,X97,tptp0) % 116.86/117.01 & occurrence_of(X98,tptp4) % 116.86/117.01 & next_subocc(X97,X98,tptp0) % 116.86/117.01 & ( occurrence_of(X99,tptp2) % 116.86/117.01 | occurrence_of(X99,tptp1) ) % 116.86/117.01 & next_subocc(X98,X99,tptp0) % 116.86/117.01 & leaf(X99,tptp0) ) ) ). % 116.86/117.01 % 116.86/117.01 fof(sos_33,axiom, % 116.86/117.01 activity(tptp0) ). % 116.86/117.01 % 116.86/117.01 fof(sos_34,axiom, % 116.86/117.01 ~ atomic(tptp0) ). % 116.86/117.01 % 116.86/117.01 fof(sos_35,axiom, % 116.86/117.01 atomic(tptp4) ). % 116.86/117.01 % 116.86/117.01 fof(sos_36,axiom, % 116.86/117.01 atomic(tptp2) ). % 116.86/117.01 % 116.86/117.01 fof(sos_37,axiom, % 116.86/117.01 atomic(tptp1) ). % 116.86/117.01 % 116.86/117.01 fof(sos_38,axiom, % 116.86/117.01 atomic(tptp3) ). % 116.86/117.01 % 116.86/117.01 fof(sos_39,axiom, % 116.86/117.01 tptp4 != tptp3 ). % 116.86/117.01 % 116.86/117.01 fof(sos_40,axiom, % 116.86/117.01 tptp4 != tptp2 ). % 116.86/117.01 % 116.86/117.01 fof(sos_41,axiom, % 116.86/117.01 tptp4 != tptp1 ). % 116.86/117.01 % 116.86/117.01 fof(sos_42,axiom, % 116.86/117.01 tptp3 != tptp2 ). % 116.86/117.01 % 116.86/117.01 fof(sos_43,axiom, % 116.86/117.01 tptp3 != tptp1 ). % 116.86/117.01 % 116.86/117.01 fof(sos_44,axiom, % 116.86/117.01 tptp2 != tptp1 ). % 116.86/117.01 % 116.86/117.01 fof(goals,conjecture, % 116.86/117.01 ! [X100,X101] : % 116.86/117.01 ( ( occurrence_of(X101,tptp0) % 116.86/117.01 & subactivity_occurrence(X100,X101) % 116.86/117.01 & arboreal(X100) % 116.86/117.01 & ~ leaf_occ(X100,X101) ) % 116.86/117.01 => ? [X102,X103] : % 116.86/117.01 ( occurrence_of(X102,tptp3) % 116.86/117.01 & next_subocc(X100,X102,tptp0) % 116.86/117.01 & ( occurrence_of(X103,tptp2) % 116.86/117.01 | occurrence_of(X103,tptp1) ) % 116.86/117.01 & min_precedes(X102,X103,tptp0) % 116.86/117.01 & leaf(X103,tptp0) ) ) ). % 116.86/117.01 % 116.86/117.01 %------------------------------------------------------------------------------ % 116.86/117.01 %------------------------------------------- % 116.86/117.01 % Proof found % 116.86/117.01 % SZS status Theorem for theBenchmark % 116.86/117.01 % SZS output start Proof % 116.86/117.01 %ClaNum:156(EqnAxiom:68) % 116.86/117.01 %VarNum:432(SingletonVarNum:175) % 116.86/117.01 %MaxLitNum:8 % 116.86/117.01 %MaxfuncDepth:1 % 116.86/117.01 %SharedTerms:23 % 116.86/117.01 %goalClause: 73 75 76 84 151 152 % 116.86/117.01 %singleGoalClaCount:4 % 116.86/117.01 [69]P1(a1) % 116.86/117.01 [70]P1(a24) % 116.86/117.01 [71]P1(a2) % 116.86/117.01 [72]P1(a3) % 116.86/117.01 [73]P2(a4) % 116.86/117.01 [74]P3(a13) % 116.86/117.01 [75]P6(a14,a13) % 116.86/117.01 [76]P13(a4,a14) % 116.86/117.01 [77]~E(a1,a24) % 116.86/117.01 [78]~E(a1,a2) % 116.86/117.01 [79]~E(a2,a24) % 116.86/117.01 [80]~E(a1,a3) % 116.86/117.01 [81]~E(a3,a24) % 116.86/117.01 [82]~E(a3,a2) % 116.86/117.01 [83]~P1(a13) % 116.86/117.01 [84]~P7(a4,a14) % 116.86/117.01 [85]~P10(x851)+P2(x851) % 116.86/117.01 [87]~P3(x871)+P14(x871,x871) % 116.86/117.01 [86]~P4(x861)+P3(f15(x861)) % 116.86/117.01 [94]~P4(x941)+P6(x941,f15(x941)) % 116.86/117.01 [88]P10(x881)+~P15(x882,x881) % 116.86/117.01 [89]P10(x891)+~P16(x891,x892) % 116.86/117.01 [90]P4(x901)+~P6(x901,x902) % 116.86/117.01 [91]P4(x911)+~P13(x912,x911) % 116.86/117.01 [92]P4(x921)+~P13(x921,x922) % 116.86/117.01 [93]P3(x931)+~P6(x932,x931) % 116.86/117.01 [97]~P15(x971,x972)+P8(x971,x972) % 116.86/117.01 [98]~P17(x981,x982)+P13(x981,x982) % 116.86/117.01 [99]~P7(x991,x992)+P13(x991,x992) % 116.86/117.01 [102]~P8(x1022,x1021)+~P8(x1021,x1022) % 116.86/117.01 [104]~P5(x1041,x1042)+P1(f16(x1041,x1042)) % 116.86/117.01 [106]~P17(x1062,x1061)+P6(x1061,f17(x1062,x1061)) % 116.86/117.01 [107]~P7(x1072,x1071)+P6(x1071,f19(x1072,x1071)) % 116.86/117.01 [108]~P5(x1081,x1082)+P6(x1081,f16(x1081,x1082)) % 116.86/117.01 [109]~P17(x1091,x1092)+P16(x1091,f17(x1091,x1092)) % 116.86/117.01 [110]~P7(x1101,x1102)+P9(x1101,f19(x1101,x1102)) % 116.86/117.01 [111]~P16(x1111,x1112)+P5(x1111,f5(x1112,x1111)) % 116.86/117.01 [112]~P5(x1122,x1121)+P14(x1121,f16(x1122,x1121)) % 116.86/117.01 [113]~P16(x1132,x1131)+P14(f5(x1131,x1132),x1131) % 116.86/117.01 [128]P2(x1281)+~P11(x1282,x1281,x1283) % 116.86/117.01 [129]P2(x1291)+~P11(x1291,x1292,x1293) % 116.86/117.01 [130]P15(x1301,x1302)+~P12(x1301,x1302,x1303) % 116.86/117.01 [132]~P16(x1321,x1322)+~P12(x1323,x1321,x1322) % 116.86/117.01 [133]~P9(x1331,x1332)+~P12(x1331,x1333,x1332) % 116.86/117.01 [141]~P11(x1411,x1412,x1413)+P12(x1411,x1412,x1413) % 116.86/117.01 [144]~P12(x1443,x1441,x1442)+P13(x1441,f23(x1442,x1443,x1441)) % 116.86/117.02 [145]~P12(x1451,x1453,x1452)+P13(x1451,f23(x1452,x1451,x1453)) % 116.86/117.02 [146]~P12(x1461,x1463,x1462)+P5(x1461,f7(x1462,x1461,x1463)) % 116.86/117.02 [147]~P12(x1473,x1471,x1472)+P5(x1471,f8(x1472,x1473,x1471)) % 116.86/117.02 [148]~P12(x1482,x1483,x1481)+P6(f23(x1481,x1482,x1483),x1481) % 116.86/117.02 [149]~P12(x1492,x1493,x1491)+P14(f7(x1491,x1492,x1493),x1491) % 116.86/117.02 [150]~P12(x1502,x1503,x1501)+P14(f8(x1501,x1502,x1503),x1501) % 116.86/117.02 [95]~P6(x952,x951)+P1(x951)+~P2(x952) % 116.86/117.02 [96]~P6(x961,x962)+P2(x961)+~P1(x962) % 116.86/117.02 [100]~P10(x1002)+~P8(x1001,x1002)+P15(x1001,x1002) % 116.86/117.02 [101]~P10(x1011)+~P5(x1011,x1012)+P16(x1011,x1012) % 116.86/117.02 [115]~P9(x1152,x1151)+P1(x1151)+P7(x1152,f22(x1152,x1151)) % 116.86/117.02 [116]~P9(x1162,x1161)+P1(x1161)+P7(x1162,f6(x1162,x1161)) % 116.86/117.02 [117]~P9(x1172,x1171)+P1(x1171)+P6(f22(x1172,x1171),x1171) % 116.86/117.02 [118]~P9(x1182,x1181)+P1(x1181)+P6(f6(x1182,x1181),x1181) % 116.86/117.02 [119]~P6(x1192,x1191)+P1(x1191)+P16(f9(x1191,x1192),x1191) % 116.86/117.02 [120]~P6(x1202,x1201)+P1(x1201)+P13(f9(x1201,x1202),x1202) % 116.86/117.02 [134]~P16(x1341,x1342)+P9(x1341,x1342)+P12(x1341,f20(x1341,x1342),x1342) % 116.86/117.02 [135]~P9(x1351,x1352)+P16(x1351,x1352)+P12(f21(x1351,x1352),x1351,x1352) % 116.86/117.02 [103]~P6(x1033,x1031)+E(x1031,x1032)+~P6(x1033,x1032) % 116.86/117.02 [105]~P8(x1051,x1053)+P8(x1051,x1052)+~P8(x1053,x1052) % 116.86/117.02 [142]P9(x1421,x1422)+~P12(x1423,x1421,x1422)+P12(x1421,f20(x1421,x1422),x1422) % 116.86/117.02 [155]~P12(x1551,x1552,x1553)+P11(x1551,x1552,x1553)+P12(x1551,f18(x1551,x1552,x1553),x1553) % 116.86/117.02 [156]~P12(x1561,x1562,x1563)+P11(x1561,x1562,x1563)+P12(f18(x1561,x1562,x1563),x1562,x1563) % 116.86/117.02 [139]~P6(x1391,x1392)+~P12(x1394,x1393,x1392)+~P17(x1393,x1391) % 116.86/117.02 [140]~P6(x1401,x1402)+~P12(x1403,x1404,x1402)+~P7(x1403,x1401) % 116.86/117.02 [153]~P12(x1531,x1534,x1533)+P12(x1531,x1532,x1533)+~P12(x1534,x1532,x1533) % 116.86/117.02 [154]~P11(x1544,x1542,x1543)+~P12(x1541,x1542,x1543)+~P12(x1544,x1541,x1543) % 116.86/117.02 [114]~P6(x1141,x1143)+~P14(x1142,x1143)+P5(x1141,x1142)+~P1(x1143) % 116.86/117.02 [123]~P16(x1231,x1233)+~P13(x1231,x1232)+P17(x1231,x1232)+~P6(x1232,x1233) % 116.86/117.02 [124]~P13(x1241,x1242)+~P9(x1241,x1243)+P7(x1241,x1242)+~P6(x1242,x1243) % 116.86/117.02 [121]~P17(x1212,x1213)+~P17(x1211,x1213)+E(x1211,x1212)+~P6(x1213,x1214) % 116.86/117.02 [151]~P12(x1511,x1512,a13)+~P9(x1512,a13)+~P6(x1511,a1)+~P6(x1512,a2)+~P11(a4,x1511,a13) % 116.86/117.02 [152]~P12(x1521,x1522,a13)+~P9(x1522,a13)+~P6(x1521,a1)+~P6(x1522,a3)+~P11(a4,x1521,a13) % 116.86/117.02 [125]~P2(x1251)+~P13(x1251,x1252)+P7(x1251,x1252)+~P6(x1252,a13)+P6(f10(x1251),a1) % 116.86/117.02 [126]~P2(x1261)+~P13(x1261,x1262)+P7(x1261,x1262)+~P6(x1262,a13)+P6(f11(x1261),a24) % 116.86/117.02 [127]~P2(x1271)+~P13(x1271,x1272)+P7(x1271,x1272)+~P6(x1272,a13)+P9(f12(x1271),a13) % 116.86/117.02 [136]~P2(x1361)+~P13(x1361,x1362)+P7(x1361,x1362)+~P6(x1362,a13)+P11(x1361,f10(x1361),a13) % 116.86/117.02 [137]~P2(x1371)+~P13(x1371,x1372)+P7(x1371,x1372)+~P6(x1372,a13)+P11(f10(x1371),f11(x1371),a13) % 116.86/117.02 [138]~P2(x1381)+~P13(x1381,x1382)+P7(x1381,x1382)+~P6(x1382,a13)+P11(f11(x1381),f12(x1381),a13) % 116.86/117.02 [122]~P7(x1222,x1224)+~P7(x1221,x1224)+E(x1221,x1222)+~P6(x1224,x1223)+P1(x1223) % 116.86/117.02 [131]~P2(x1311)+~P13(x1311,x1312)+P7(x1311,x1312)+~P6(x1312,a13)+P6(f12(x1311),a2)+P6(f12(x1311),a3) % 116.86/117.02 [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) % 116.86/117.02 %EqnAxiom % 116.86/117.02 [1]E(x11,x11) % 116.86/117.02 [2]E(x22,x21)+~E(x21,x22) % 116.86/117.02 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 116.86/117.02 [4]~E(x41,x42)+E(f15(x41),f15(x42)) % 116.86/117.02 [5]~E(x51,x52)+E(f18(x51,x53,x54),f18(x52,x53,x54)) % 116.86/117.02 [6]~E(x61,x62)+E(f18(x63,x61,x64),f18(x63,x62,x64)) % 116.86/117.02 [7]~E(x71,x72)+E(f18(x73,x74,x71),f18(x73,x74,x72)) % 116.86/117.02 [8]~E(x81,x82)+E(f16(x81,x83),f16(x82,x83)) % 116.86/117.02 [9]~E(x91,x92)+E(f16(x93,x91),f16(x93,x92)) % 116.86/117.02 [10]~E(x101,x102)+E(f17(x101,x103),f17(x102,x103)) % 116.86/117.02 [11]~E(x111,x112)+E(f17(x113,x111),f17(x113,x112)) % 116.86/117.02 [12]~E(x121,x122)+E(f19(x121,x123),f19(x122,x123)) % 116.86/117.02 [13]~E(x131,x132)+E(f19(x133,x131),f19(x133,x132)) % 116.86/117.02 [14]~E(x141,x142)+E(f8(x141,x143,x144),f8(x142,x143,x144)) % 116.86/117.02 [15]~E(x151,x152)+E(f8(x153,x151,x154),f8(x153,x152,x154)) % 116.86/117.02 [16]~E(x161,x162)+E(f8(x163,x164,x161),f8(x163,x164,x162)) % 116.86/117.02 [17]~E(x171,x172)+E(f23(x171,x173,x174),f23(x172,x173,x174)) % 116.86/117.02 [18]~E(x181,x182)+E(f23(x183,x181,x184),f23(x183,x182,x184)) % 116.86/117.02 [19]~E(x191,x192)+E(f23(x193,x194,x191),f23(x193,x194,x192)) % 116.86/117.02 [20]~E(x201,x202)+E(f7(x201,x203,x204),f7(x202,x203,x204)) % 116.86/117.02 [21]~E(x211,x212)+E(f7(x213,x211,x214),f7(x213,x212,x214)) % 116.86/117.02 [22]~E(x221,x222)+E(f7(x223,x224,x221),f7(x223,x224,x222)) % 116.86/117.02 [23]~E(x231,x232)+E(f5(x231,x233),f5(x232,x233)) % 116.86/117.02 [24]~E(x241,x242)+E(f5(x243,x241),f5(x243,x242)) % 116.86/117.02 [25]~E(x251,x252)+E(f20(x251,x253),f20(x252,x253)) % 116.86/117.02 [26]~E(x261,x262)+E(f20(x263,x261),f20(x263,x262)) % 116.86/117.02 [27]~E(x271,x272)+E(f12(x271),f12(x272)) % 116.86/117.02 [28]~E(x281,x282)+E(f22(x281,x283),f22(x282,x283)) % 116.86/117.02 [29]~E(x291,x292)+E(f22(x293,x291),f22(x293,x292)) % 116.86/117.02 [30]~E(x301,x302)+E(f6(x301,x303),f6(x302,x303)) % 116.86/117.02 [31]~E(x311,x312)+E(f6(x313,x311),f6(x313,x312)) % 116.86/117.02 [32]~E(x321,x322)+E(f21(x321,x323),f21(x322,x323)) % 116.86/117.02 [33]~E(x331,x332)+E(f21(x333,x331),f21(x333,x332)) % 116.86/117.02 [34]~E(x341,x342)+E(f11(x341),f11(x342)) % 116.86/117.02 [35]~E(x351,x352)+E(f9(x351,x353),f9(x352,x353)) % 116.86/117.02 [36]~E(x361,x362)+E(f9(x363,x361),f9(x363,x362)) % 116.86/117.02 [37]~E(x371,x372)+E(f10(x371),f10(x372)) % 116.86/117.02 [38]~P1(x381)+P1(x382)+~E(x381,x382) % 116.86/117.02 [39]P12(x392,x393,x394)+~E(x391,x392)+~P12(x391,x393,x394) % 116.86/117.02 [40]P12(x403,x402,x404)+~E(x401,x402)+~P12(x403,x401,x404) % 116.86/117.02 [41]P12(x413,x414,x412)+~E(x411,x412)+~P12(x413,x414,x411) % 116.86/117.02 [42]P6(x422,x423)+~E(x421,x422)+~P6(x421,x423) % 116.86/117.02 [43]P6(x433,x432)+~E(x431,x432)+~P6(x433,x431) % 116.86/117.02 [44]P11(x442,x443,x444)+~E(x441,x442)+~P11(x441,x443,x444) % 116.86/117.02 [45]P11(x453,x452,x454)+~E(x451,x452)+~P11(x453,x451,x454) % 116.86/117.02 [46]P11(x463,x464,x462)+~E(x461,x462)+~P11(x463,x464,x461) % 116.86/117.02 [47]~P2(x471)+P2(x472)+~E(x471,x472) % 116.86/117.02 [48]~P3(x481)+P3(x482)+~E(x481,x482) % 116.86/117.02 [49]P13(x492,x493)+~E(x491,x492)+~P13(x491,x493) % 116.86/117.02 [50]P13(x503,x502)+~E(x501,x502)+~P13(x503,x501) % 116.86/117.02 [51]P7(x512,x513)+~E(x511,x512)+~P7(x511,x513) % 116.86/117.02 [52]P7(x523,x522)+~E(x521,x522)+~P7(x523,x521) % 116.86/117.02 [53]P9(x532,x533)+~E(x531,x532)+~P9(x531,x533) % 116.86/117.02 [54]P9(x543,x542)+~E(x541,x542)+~P9(x543,x541) % 116.86/117.02 [55]P16(x552,x553)+~E(x551,x552)+~P16(x551,x553) % 116.86/117.02 [56]P16(x563,x562)+~E(x561,x562)+~P16(x563,x561) % 116.86/117.02 [57]P14(x572,x573)+~E(x571,x572)+~P14(x571,x573) % 116.86/117.02 [58]P14(x583,x582)+~E(x581,x582)+~P14(x583,x581) % 116.86/117.02 [59]~P10(x591)+P10(x592)+~E(x591,x592) % 116.86/117.02 [60]P5(x602,x603)+~E(x601,x602)+~P5(x601,x603) % 116.86/117.02 [61]P5(x613,x612)+~E(x611,x612)+~P5(x613,x611) % 116.86/117.02 [62]~P4(x621)+P4(x622)+~E(x621,x622) % 116.86/117.02 [63]P15(x632,x633)+~E(x631,x632)+~P15(x631,x633) % 116.86/117.02 [64]P15(x643,x642)+~E(x641,x642)+~P15(x643,x641) % 116.86/117.02 [65]P8(x652,x653)+~E(x651,x652)+~P8(x651,x653) % 116.86/117.02 [66]P8(x663,x662)+~E(x661,x662)+~P8(x663,x661) % 116.86/117.02 [67]P17(x672,x673)+~E(x671,x672)+~P17(x671,x673) % 116.86/117.02 [68]P17(x683,x682)+~E(x681,x682)+~P17(x683,x681) % 116.86/117.02 % 116.86/117.02 %------------------------------------------- % 116.86/117.04 cnf(159,plain, % 116.86/117.04 (~E(a14,a4)), % 116.86/117.04 inference(scs_inference,[],[73,75,83,95,42])). % 116.86/117.04 cnf(160,plain, % 116.86/117.04 (~P9(a4,a13)), % 116.86/117.04 inference(scs_inference,[],[73,75,76,84,83,95,42,124])). % 116.86/117.04 cnf(162,plain, % 116.86/117.04 (P6(a14,x1621)+~E(a13,x1621)), % 116.86/117.04 inference(scs_inference,[],[73,75,76,84,83,95,42,124,43])). % 116.86/117.04 cnf(213,plain, % 116.86/117.04 (~P10(a14)), % 116.86/117.04 inference(scs_inference,[],[83,75,85,95])). % 116.86/117.04 cnf(214,plain, % 116.86/117.04 (~P15(x2141,a14)), % 116.86/117.04 inference(scs_inference,[],[213,88])). % 116.86/117.04 cnf(216,plain, % 116.86/117.04 (~P16(a14,x2161)), % 116.86/117.04 inference(scs_inference,[],[213,88,89])). % 116.86/117.04 cnf(220,plain, % 116.86/117.04 (~P12(x2201,a14,x2202)), % 116.86/117.04 inference(scs_inference,[],[213,88,89,109,130])). % 116.86/117.04 cnf(226,plain, % 116.86/117.04 (P3(f15(a14))), % 116.86/117.04 inference(scs_inference,[],[75,86,90])). % 116.86/117.04 cnf(227,plain, % 116.86/117.04 (~P11(x2271,a14,x2272)), % 116.86/117.04 inference(scs_inference,[],[220,141])). % 116.86/117.04 cnf(229,plain, % 116.86/117.04 (~P9(a14,x2291)), % 116.86/117.04 inference(scs_inference,[],[220,216,141,135])). % 116.86/117.04 cnf(232,plain, % 116.86/117.04 (~P7(a14,x2321)), % 116.86/117.04 inference(scs_inference,[],[220,216,141,135,110])). % 116.86/117.04 cnf(234,plain, % 116.86/117.04 (P14(x2341,f15(a14))+~E(f15(a14),x2341)), % 116.86/117.04 inference(scs_inference,[],[226,87,57])). % 116.86/117.04 cnf(235,plain, % 116.86/117.04 (P14(f15(a14),f15(a14))), % 116.86/117.04 inference(equality_inference,[],[234])). % 116.86/117.04 cnf(241,plain, % 116.86/117.04 (P6(a14,f15(a14))), % 116.86/117.04 inference(scs_inference,[],[76,91,94])). % 116.86/117.04 cnf(243,plain, % 116.86/117.04 (E(a13,x2431)+~E(f15(a14),x2431)), % 116.86/117.04 inference(scs_inference,[],[75,241,43,103])). % 116.86/117.04 cnf(249,plain, % 116.86/117.04 (E(a13,f15(a14))), % 116.86/117.04 inference(equality_inference,[],[243])). % 116.86/117.04 cnf(251,plain, % 116.86/117.04 (E(f15(a14),a13)), % 116.86/117.04 inference(scs_inference,[],[249,2])). % 116.86/117.04 cnf(254,plain, % 116.86/117.04 (~P1(f15(a14))), % 116.86/117.04 inference(scs_inference,[],[249,83,235,2,58,57,38])). % 116.86/117.04 cnf(256,plain, % 116.86/117.04 (~P6(a4,f15(a14))), % 116.86/117.04 inference(scs_inference,[],[73,249,83,235,2,58,57,38,62,95])). % 116.86/117.04 cnf(342,plain, % 116.86/117.04 (P3(a1)), % 116.86/117.04 inference(scs_inference,[],[75,84,73,76,93,125])). % 116.86/117.04 cnf(349,plain, % 116.86/117.04 (~P8(x3491,x3492)+~P15(x3492,x3491)), % 116.86/117.04 inference(scs_inference,[],[97,102])). % 116.86/117.04 cnf(409,plain, % 116.86/117.04 (~P8(x4091,x4092)+~P12(x4092,x4091,x4093)), % 116.86/117.04 inference(scs_inference,[],[349,130])). % 116.86/117.04 cnf(438,plain, % 116.86/117.04 (~P12(x4381,x4382,x4383)+P1(f16(x4381,f7(x4383,x4381,x4382)))), % 116.86/117.04 inference(scs_inference,[],[104,146])). % 116.86/117.04 cnf(439,plain, % 116.86/117.04 (~P12(x4391,f9(a13,a14),a13)), % 116.86/117.04 inference(scs_inference,[],[83,75,132,119])). % 116.86/117.04 cnf(440,plain, % 116.86/117.04 (~P11(x4401,f9(a13,a14),a13)), % 116.86/117.04 inference(scs_inference,[],[439,141])). % 116.86/117.04 cnf(450,plain, % 116.86/117.04 (~P12(f12(a4),x4501,a13)), % 116.86/117.04 inference(scs_inference,[],[75,84,73,76,133,127])). % 116.86/117.04 cnf(451,plain, % 116.86/117.04 (~P11(f12(a4),x4511,a13)), % 116.86/117.04 inference(scs_inference,[],[450,141])). % 116.86/117.04 cnf(464,plain, % 116.86/117.04 (P9(f12(a4),a13)+~P12(x4641,f12(a4),a13)), % 116.86/117.04 inference(scs_inference,[],[450,142])). % 116.86/117.04 cnf(467,plain, % 116.86/117.04 (P9(f12(a4),f15(a14))+~P12(x4671,f12(a4),a13)), % 116.86/117.04 inference(scs_inference,[],[249,450,142,54])). % 116.86/117.04 cnf(468,plain, % 116.86/117.04 (~P12(x4681,f12(a4),a13)+~E(f12(a4),a14)), % 116.86/117.04 inference(scs_inference,[],[249,229,450,142,54,53])). % 116.86/117.04 cnf(470,plain, % 116.86/117.04 (~P12(f12(a4),x4701,f15(a14))+~P12(x4702,f12(a4),a13)), % 116.86/117.04 inference(scs_inference,[],[249,229,450,142,54,53,133])). % 116.86/117.04 cnf(1194,plain, % 116.86/117.04 (~P12(x11941,x11942,x11943)+~P15(x11942,x11941)), % 116.86/117.04 inference(scs_inference,[],[409,97])). % 116.86/117.04 cnf(1566,plain, % 116.86/117.04 (~P12(x15661,x15662,x15663)+~P12(x15662,x15661,x15664)), % 116.86/117.04 inference(scs_inference,[],[1194,130])). % 116.86/117.04 cnf(1845,plain, % 116.86/117.04 (~P9(x18451,a13)+P6(f6(x18451,a13),f19(x18451,f6(x18451,a13)))), % 116.86/117.04 inference(scs_inference,[],[83,107,116])). % 116.86/117.04 cnf(1876,plain, % 116.86/117.04 (~P12(x18761,x18762,x18763)+P14(f8(x18763,x18761,x18762),f16(x18762,f8(x18763,x18761,x18762)))), % 116.86/117.04 inference(scs_inference,[],[112,147])). % 116.86/117.04 cnf(2754,plain, % 116.86/117.04 (~P11(x27541,x27542,x27543)+~P12(x27542,x27541,x27544)), % 116.86/117.04 inference(scs_inference,[],[1566,141])). % 116.86/117.04 cnf(2972,plain, % 116.86/117.04 (~P12(f10(a4),a4,x29721)), % 116.86/117.04 inference(scs_inference,[],[75,84,73,76,2754,136])). % 116.86/117.04 cnf(2973,plain, % 116.86/117.04 (~P11(f10(a4),a4,x29731)), % 116.86/117.04 inference(scs_inference,[],[2972,141])). % 116.86/117.04 cnf(3223,plain, % 116.86/117.04 (P6(f6(f12(a4),a13),f19(f12(a4),f6(f12(a4),a13)))+~P12(x32231,f12(a4),a13)), % 116.86/117.04 inference(scs_inference,[],[464,1845])). % 116.86/117.04 cnf(3254,plain, % 116.86/117.04 (~E(a14,f12(a4))+~P12(x32541,f12(a4),a13)), % 116.86/117.04 inference(scs_inference,[],[468,2])). % 116.86/117.04 cnf(4002,plain, % 116.86/117.04 (~P11(x40021,f12(a4),a13)+~E(a14,f12(a4))), % 116.86/117.04 inference(scs_inference,[],[3254,141])). % 116.86/117.04 cnf(4127,plain, % 116.86/117.04 (~E(a14,f12(a4))), % 116.86/117.04 inference(scs_inference,[],[75,84,73,76,4002,138])). % 116.86/117.04 cnf(4220,plain, % 116.86/117.04 (E(f19(x42201,f8(a13,x42202,x42203)),f19(x42201,f8(f15(a14),x42202,x42203)))), % 116.86/117.04 inference(scs_inference,[],[249,13,14])). % 116.86/117.04 cnf(4251,plain, % 116.86/117.04 (E(f5(f8(x42511,a13,x42512),x42513),f5(f8(x42511,f15(a14),x42512),x42513))), % 116.86/117.04 inference(scs_inference,[],[249,23,15])). % 116.86/117.04 cnf(4282,plain, % 116.86/117.04 (E(f5(x42821,f8(x42822,x42823,a13)),f5(x42821,f8(x42822,x42823,f15(a14))))), % 116.86/117.04 inference(scs_inference,[],[249,24,16])). % 116.86/117.04 cnf(4313,plain, % 116.86/117.04 (E(f20(f23(a13,x43131,x43132),x43133),f20(f23(f15(a14),x43131,x43132),x43133))), % 116.86/117.04 inference(scs_inference,[],[249,25,17])). % 116.86/117.04 cnf(4344,plain, % 116.86/117.04 (E(f20(x43441,f23(x43442,a13,x43443)),f20(x43441,f23(x43442,f15(a14),x43443)))), % 116.86/117.04 inference(scs_inference,[],[249,26,18])). % 116.86/117.04 cnf(4561,plain, % 116.86/117.04 (~P11(x45611,x45612,x45613)+P13(x45611,f23(x45613,x45611,x45612))), % 116.86/117.04 inference(scs_inference,[],[145,141])). % 116.86/117.04 cnf(4592,plain, % 116.86/117.04 (~P11(x45921,x45922,x45923)+P6(f23(x45923,x45921,x45922),x45923)), % 116.86/117.04 inference(scs_inference,[],[148,141])). % 116.86/117.04 cnf(4623,plain, % 116.86/117.04 (~P11(x46231,x46232,x46233)+P14(f7(x46233,x46231,x46232),x46233)), % 116.86/117.04 inference(scs_inference,[],[149,141])). % 116.86/117.04 cnf(4654,plain, % 116.86/117.04 (~P11(x46541,x46542,x46543)+P14(f8(x46543,x46541,x46542),x46543)), % 116.86/117.04 inference(scs_inference,[],[150,141])). % 116.86/117.04 cnf(4809,plain, % 116.86/117.04 (P6(f22(f12(a4),f15(a14)),f15(a14))+~P12(x48091,f12(a4),a13)), % 116.86/117.04 inference(scs_inference,[],[254,467,117])). % 116.86/117.04 cnf(5367,plain, % 116.86/117.04 (~P11(x53671,x53672,x53673)+P4(f23(x53673,x53671,x53672))), % 116.86/117.04 inference(scs_inference,[],[4561,91])). % 116.86/117.04 cnf(5398,plain, % 116.86/117.04 (~P11(x53981,x53982,x53983)+P3(f15(f23(x53983,x53981,x53982)))), % 116.86/117.04 inference(scs_inference,[],[5367,86])). % 116.86/117.04 cnf(5522,plain, % 116.86/117.04 (~P11(x55221,x55222,a13)+P14(f7(a13,x55221,x55222),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[249,4623,58])). % 116.86/117.04 cnf(5553,plain, % 116.86/117.04 (~P11(x55531,x55532,a13)+P14(f8(a13,x55531,x55532),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[249,4654,58])). % 116.86/117.04 cnf(6207,plain, % 116.86/117.04 (~E(f16(x62071,f7(x62072,x62071,x62073)),a13)+~P12(x62071,x62073,x62072)), % 116.86/117.04 inference(scs_inference,[],[83,438,38])). % 116.86/117.04 cnf(6269,plain, % 116.86/117.04 (~P11(x62691,f12(a4),a13)+~P12(f12(a4),x62692,f15(a14))), % 116.86/117.04 inference(scs_inference,[],[470,141])). % 116.86/117.04 cnf(6519,plain, % 116.86/117.04 (P14(x65191,f15(a14))+~E(f7(a13,x65192,x65193),x65191)+~P11(x65192,x65193,a13)), % 116.86/117.04 inference(scs_inference,[],[5522,57])). % 116.86/117.04 cnf(6802,plain, % 116.86/117.04 (~P11(x68021,x68022,x68023)+~E(f16(x68021,f7(x68023,x68021,x68022)),a13)), % 116.86/117.04 inference(scs_inference,[],[6207,141])). % 116.86/117.04 cnf(6895,plain, % 116.86/117.04 (~E(f16(f10(a4),f7(a13,f10(a4),f11(a4))),a13)), % 116.86/117.04 inference(scs_inference,[],[75,84,73,76,6802,137])). % 116.86/117.04 cnf(6958,plain, % 116.86/117.04 (P4(f22(f12(a4),f15(a14)))+~P12(x69581,f12(a4),a13)), % 116.86/117.04 inference(scs_inference,[],[4809,90])). % 116.86/117.04 cnf(6989,plain, % 116.86/117.04 (~P12(x69891,f12(a4),a13)+P3(f15(f22(f12(a4),f15(a14))))), % 116.86/117.04 inference(scs_inference,[],[6958,86])). % 116.86/117.04 cnf(7141,plain, % 116.86/117.04 (~E(a1,a13)), % 116.86/117.04 inference(scs_inference,[],[83,69,38])). % 116.86/117.04 cnf(7150,plain, % 116.86/117.04 (~E(a24,a13)), % 116.86/117.04 inference(scs_inference,[],[83,70,38])). % 116.86/117.04 cnf(7156,plain, % 116.86/117.04 (~P9(x71561,a13)+~E(x71561,a4)), % 116.86/117.04 inference(scs_inference,[],[160,83,71,38,53])). % 116.86/117.04 cnf(7185,plain, % 116.86/117.04 (~P6(x71851,a1)+~E(x71851,a14)), % 116.86/117.04 inference(scs_inference,[],[75,7141,103,43,243,42])). % 116.86/117.04 cnf(7201,plain, % 116.86/117.04 (~P6(x72011,a24)+~E(x72011,a14)), % 116.86/117.04 inference(scs_inference,[],[75,7150,90,103,43,243,42])). % 116.86/117.04 cnf(7230,plain, % 116.86/117.04 (~P16(x72301,x72302)+~E(x72301,a14)), % 116.86/117.04 inference(scs_inference,[],[251,7150,216,3,55])). % 116.86/117.04 cnf(7231,plain, % 116.86/117.04 (~P17(x72311,x72312)+~E(x72311,a14)), % 116.86/117.04 inference(scs_inference,[],[251,7150,216,3,55,109])). % 116.86/117.04 cnf(7238,plain, % 116.86/117.04 (~P6(x72381,a2)+~P6(x72381,a1)), % 116.86/117.04 inference(scs_inference,[],[159,78,2,103])). % 116.86/117.04 cnf(7250,plain, % 116.86/117.04 (~P6(x72501,a24)+~P6(x72501,a2)), % 116.86/117.04 inference(scs_inference,[],[4127,79,2,103])). % 116.86/117.04 cnf(7256,plain, % 116.86/117.04 (~E(a3,a1)), % 116.86/117.04 inference(scs_inference,[],[80,2])). % 116.86/117.04 cnf(7257,plain, % 116.86/117.04 (P14(a1,a1)), % 116.86/117.04 inference(scs_inference,[],[342,80,2,87])). % 116.86/117.04 cnf(7259,plain, % 116.86/117.04 (~P12(x72591,x72592,a13)+~E(x72591,f12(a4))), % 116.86/117.04 inference(scs_inference,[],[342,80,450,2,87,39])). % 116.86/117.04 cnf(7260,plain, % 116.86/117.04 (~P11(x72601,f9(a13,a14),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[342,440,251,80,450,2,87,39,46])). % 116.86/117.04 cnf(7267,plain, % 116.86/117.04 (~P11(f12(a4),x72671,f15(a14))), % 116.86/117.04 inference(scs_inference,[],[451,251,81,2,46])). % 116.86/117.04 cnf(7281,plain, % 116.86/117.04 (~P11(x72811,x72812,x72813)+~E(x72812,a14)), % 116.86/117.04 inference(scs_inference,[],[227,82,2,45])). % 116.86/117.04 cnf(7289,plain, % 116.86/117.04 (~P6(x72891,a24)+~P6(x72891,a1)), % 116.86/117.04 inference(scs_inference,[],[7260,7267,77,232,2,45,51,44,103])). % 116.86/117.04 cnf(7298,plain, % 116.86/117.04 (~P11(f10(a4),x72981,x72982)+~E(x72981,a4)), % 116.86/117.04 inference(scs_inference,[],[2973,78,2,45])). % 116.86/117.04 cnf(7303,plain, % 116.86/117.04 (~P6(x73031,a3)+~P6(x73031,a1)), % 116.86/117.04 inference(scs_inference,[],[79,80,2,103])). % 116.86/117.04 cnf(7307,plain, % 116.86/117.04 (~P6(x73071,a24)+~P6(x73071,a3)), % 116.86/117.04 inference(scs_inference,[],[81,103])). % 116.86/117.04 cnf(7378,plain, % 116.86/117.04 (P5(x73781,a1)+~P6(x73781,a1)), % 116.86/117.04 inference(scs_inference,[],[7256,7257,69,3,114])). % 116.86/117.04 cnf(7453,plain, % 116.86/117.04 (~P6(f10(a4),a2)), % 116.86/117.04 inference(scs_inference,[],[75,84,73,76,7238,125])). % 116.86/117.04 cnf(7455,plain, % 116.86/117.04 (~E(f12(a4),f10(a4))+P6(f12(a4),a3)), % 116.86/117.04 inference(scs_inference,[],[76,84,75,73,7453,42,131])). % 116.86/117.04 cnf(7468,plain, % 116.86/117.04 (~P6(f10(a4),x74681)+~E(x74681,a2)), % 116.86/117.04 inference(scs_inference,[],[7453,43])). % 116.86/117.04 cnf(7532,plain, % 116.86/117.04 (~P6(f10(a4),a24)), % 116.86/117.04 inference(scs_inference,[],[75,84,73,76,7289,125])). % 116.86/117.04 cnf(7537,plain, % 116.86/117.04 (~P6(f10(a4),x75371)+~E(x75371,a24)), % 116.86/117.04 inference(scs_inference,[],[7532,43])). % 116.86/117.04 cnf(7599,plain, % 116.86/117.04 (~P6(f10(a4),a3)), % 116.86/117.04 inference(scs_inference,[],[75,84,73,76,7303,125])). % 116.86/117.04 cnf(7601,plain, % 116.86/117.04 (~E(f12(a4),f10(a4))), % 116.86/117.04 inference(scs_inference,[],[7599,42,7455])). % 116.86/117.04 cnf(7629,plain, % 116.86/117.04 (~P6(f10(a4),x76291)+~E(x76291,a3)), % 116.86/117.04 inference(scs_inference,[],[7599,43])). % 116.86/117.04 cnf(8160,plain, % 116.86/117.04 (P5(f10(a4),a1)), % 116.86/117.04 inference(scs_inference,[],[75,84,73,76,7378,125])). % 116.86/117.04 cnf(10004,plain, % 116.86/117.04 (P16(f9(a13,a14),a13)), % 116.86/117.04 inference(scs_inference,[],[76,83,75,92,119])). % 116.86/117.04 cnf(10006,plain, % 116.86/117.04 (P13(f9(a13,a14),a14)), % 116.86/117.04 inference(scs_inference,[],[76,83,75,92,119,120])). % 116.86/117.04 cnf(10009,plain, % 116.86/117.04 (P16(f9(a13,a14),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[439,251,76,249,83,75,92,119,120,41,56])). % 116.86/117.04 cnf(10010,plain, % 116.86/117.04 (~P2(a14)), % 116.86/117.04 inference(scs_inference,[],[254,241,439,251,76,249,83,75,92,119,120,41,56,95])). % 116.86/117.04 cnf(10014,plain, % 116.86/117.04 (P17(f9(a13,a14),a14)), % 116.86/117.04 inference(scs_inference,[],[254,241,439,216,251,76,249,83,75,92,119,120,41,56,95,55,123])). % 116.86/117.04 cnf(10016,plain, % 116.86/117.04 (P3(f15(a4))), % 116.86/117.04 inference(scs_inference,[],[254,241,439,216,251,76,249,83,75,92,119,120,41,56,95,55,123,86])). % 116.86/117.04 cnf(10018,plain, % 116.86/117.04 (P6(a4,f15(a4))), % 116.86/117.04 inference(scs_inference,[],[254,241,439,216,251,76,249,83,75,92,119,120,41,56,95,55,123,86,94])). % 116.86/117.04 cnf(10021,plain, % 116.86/117.04 (P11(f11(a4),f12(a4),a13)), % 116.86/117.04 inference(scs_inference,[],[73,254,241,439,216,84,251,76,249,83,75,92,119,120,41,56,95,55,123,86,94,64,138])). % 116.86/117.04 cnf(10023,plain, % 116.86/117.04 (P6(f11(a4),a24)), % 116.86/117.04 inference(scs_inference,[],[73,254,241,439,216,84,251,76,249,83,75,92,119,120,41,56,95,55,123,86,94,64,138,126])). % 116.86/117.04 cnf(10025,plain, % 116.86/117.04 (P9(f12(a4),a13)), % 116.86/117.04 inference(scs_inference,[],[73,254,241,439,216,84,251,76,249,83,75,92,119,120,41,56,95,55,123,86,94,64,138,126,127])). % 116.86/117.04 cnf(10027,plain, % 116.86/117.04 (P11(f10(a4),f11(a4),a13)), % 116.86/117.04 inference(scs_inference,[],[73,254,241,439,216,84,251,76,249,83,75,92,119,120,41,56,95,55,123,86,94,64,138,126,127,137])). % 116.86/117.04 cnf(10029,plain, % 116.86/117.04 (P6(f10(a4),a1)), % 116.86/117.04 inference(scs_inference,[],[73,254,241,439,216,84,251,76,249,83,75,92,119,120,41,56,95,55,123,86,94,64,138,126,127,137,125])). % 116.86/117.04 cnf(10031,plain, % 116.86/117.04 (P11(a4,f10(a4),a13)), % 116.86/117.04 inference(scs_inference,[],[73,254,241,439,216,84,251,76,249,83,75,92,119,120,41,56,95,55,123,86,94,64,138,126,127,137,125,136])). % 116.86/117.04 cnf(10055,plain, % 116.86/117.04 (~P15(a13,f15(a14))+~P7(x100551,a14)+~P12(x100551,x100552,f15(a14))), % 116.86/117.04 inference(scs_inference,[],[73,254,241,439,216,84,251,76,249,83,75,92,119,120,41,56,95,55,123,86,94,64,138,126,127,137,125,136,97,102,349,7156,7185,7201,7250,7289,7298,7307,128,129,141,133,139,140])). % 116.86/117.04 cnf(10056,plain, % 116.86/117.04 (~P12(f12(a4),x100561,f15(a14))), % 116.86/117.04 inference(scs_inference,[],[10021,6269])). % 116.86/117.04 cnf(10058,plain, % 116.86/117.04 (~P6(f11(a4),a1)), % 116.86/117.04 inference(scs_inference,[],[10027,10023,7281,7289])). % 116.86/117.04 cnf(10069,plain, % 116.86/117.04 (P12(f11(a4),f12(a4),a13)), % 116.86/117.04 inference(scs_inference,[],[10025,10006,10021,10027,10023,10029,7281,7289,7250,7156,7307,7185,92,7298,141])). % 116.86/117.04 cnf(10071,plain, % 116.86/117.04 (P2(f11(a4))), % 116.86/117.04 inference(scs_inference,[],[10025,10006,10021,10027,10023,10029,7281,7289,7250,7156,7307,7185,92,7298,141,129])). % 116.86/117.04 cnf(10073,plain, % 116.86/117.04 (P2(f12(a4))), % 116.86/117.04 inference(scs_inference,[],[10025,10006,10021,10027,10023,10029,7281,7289,7250,7156,7307,7185,92,7298,141,129,128])). % 116.86/117.04 cnf(10075,plain, % 116.86/117.04 (~P12(f11(a4),f11(a4),a13)), % 116.86/117.04 inference(scs_inference,[],[10025,10006,10021,10027,10023,10029,7281,7289,7250,7156,7307,7185,92,7298,141,129,128,154])). % 116.86/117.04 cnf(10081,plain, % 116.86/117.04 (~P17(f12(a4),a14)), % 116.86/117.04 inference(scs_inference,[],[10025,10006,10021,10027,10023,10029,439,75,7281,7289,7250,7156,7307,7185,92,7298,141,129,128,154,40,140,139])). % 116.86/117.04 cnf(10083,plain, % 116.86/117.04 (P2(f10(a4))), % 116.86/117.04 inference(scs_inference,[],[10025,10006,10021,10027,10023,10029,69,439,75,7281,7289,7250,7156,7307,7185,92,7298,141,129,128,154,40,140,139,96])). % 116.86/117.04 cnf(10085,plain, % 116.86/117.04 (P11(f11(a4),f12(a4),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[10025,10006,10021,10027,10023,10029,69,439,249,75,7281,7289,7250,7156,7307,7185,92,7298,141,129,128,154,40,140,139,96,46])). % 116.86/117.04 cnf(10086,plain, % 116.86/117.04 (P1(f15(a4))), % 116.86/117.04 inference(scs_inference,[],[73,10025,10006,10021,10027,10018,10023,10029,69,439,249,75,7281,7289,7250,7156,7307,7185,92,7298,141,129,128,154,40,140,139,96,46,95])). % 116.86/117.04 cnf(10090,plain, % 116.86/117.04 (~E(f15(a4),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[73,10025,10006,10021,10027,10018,10023,10029,256,69,439,450,249,75,7281,7289,7250,7156,7307,7185,92,7298,141,129,128,154,40,140,139,96,46,95,39,43])). % 116.86/117.04 cnf(10093,plain, % 116.86/117.04 (P9(f12(a4),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[73,10025,10006,10021,10027,10018,10023,10029,10031,256,69,439,450,249,75,451,7281,7289,7250,7156,7307,7185,92,7298,141,129,128,154,40,140,139,96,46,95,39,43,44,54])). % 116.86/117.04 cnf(10094,plain, % 116.86/117.04 (~P16(f12(a4),a13)), % 116.86/117.04 inference(scs_inference,[],[73,10025,10006,10021,10027,10018,10023,10029,10031,256,69,439,450,249,75,451,7281,7289,7250,7156,7307,7185,92,7298,141,129,128,154,40,140,139,96,46,95,39,43,44,54,132])). % 116.86/117.04 cnf(10100,plain, % 116.86/117.04 (~P12(f12(a4),f11(a4),x101001)), % 116.86/117.04 inference(scs_inference,[],[73,10025,10006,10021,10027,10018,10023,10029,10031,256,69,439,450,249,75,451,7281,7289,7250,7156,7307,7185,92,7298,141,129,128,154,40,140,139,96,46,95,39,43,44,54,132,409,1194,1566])). % 116.86/117.04 cnf(10104,plain, % 116.86/117.04 (P15(f11(a4),f12(a4))), % 116.86/117.04 inference(scs_inference,[],[73,10025,10006,10021,10027,10018,10023,10029,10031,256,69,439,450,249,75,451,7281,7289,7250,7156,7307,7185,92,7298,141,129,128,154,40,140,139,96,46,95,39,43,44,54,132,409,1194,1566,2754,130])). % 116.86/117.04 cnf(10108,plain, % 116.86/117.04 (~P9(f11(a4),a13)), % 116.86/117.04 inference(scs_inference,[],[73,10025,10006,10021,10027,10018,10023,10029,10031,256,69,439,450,249,75,451,7281,7289,7250,7156,7307,7185,92,7298,141,129,128,154,40,140,139,96,46,95,39,43,44,54,132,409,1194,1566,2754,130,97,133])). % 116.86/117.04 cnf(10114,plain, % 116.86/117.04 (~P5(f12(a4),a13)), % 116.86/117.04 inference(scs_inference,[],[73,10025,10006,10021,10027,10018,10023,10029,10031,256,69,439,450,249,75,451,7281,7289,7250,7156,7307,7185,92,7298,141,129,128,154,40,140,139,96,46,95,39,43,44,54,132,409,1194,1566,2754,130,97,133,88,105,101])). % 116.86/117.04 cnf(10121,plain, % 116.86/117.04 (P6(f6(f12(a4),a13),f19(f12(a4),f6(f12(a4),a13)))), % 116.86/117.04 inference(scs_inference,[],[10069,3223])). % 116.86/117.04 cnf(10122,plain, % 116.86/117.04 (P6(f22(f12(a4),f15(a14)),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[10069,4809])). % 116.86/117.04 cnf(10124,plain, % 116.86/117.04 (P4(f22(f12(a4),f15(a14)))), % 116.86/117.04 inference(scs_inference,[],[10069,6958])). % 116.86/117.04 cnf(10125,plain, % 116.86/117.04 (P3(f15(f22(f12(a4),f15(a14))))), % 116.86/117.04 inference(scs_inference,[],[10069,6989])). % 116.86/117.04 cnf(10127,plain, % 116.86/117.04 (P12(f11(a4),f12(a4),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[10085,141])). % 116.86/117.04 cnf(10129,plain, % 116.86/117.04 (~P9(f11(a4),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[10085,141,133])). % 116.86/117.04 cnf(10133,plain, % 116.86/117.04 (~P5(f12(a4),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[10114,10085,251,141,133,154,61])). % 116.86/117.04 cnf(10137,plain, % 116.86/117.04 (P11(a4,f10(a4),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[10081,10058,10108,10114,10085,10014,10031,10025,10029,251,249,141,133,154,61,67,42,53,46])). % 116.86/117.04 cnf(10138,plain, % 116.86/117.04 (~P16(f12(a4),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[10081,10058,10108,10114,10085,10014,10031,10025,10029,251,249,141,133,154,61,67,42,53,46,132])). % 116.86/117.04 cnf(10144,plain, % 116.86/117.04 (P12(a4,f10(a4),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[10137,141])). % 116.86/117.04 cnf(10150,plain, % 116.86/117.04 (P11(f10(a4),f11(a4),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[10137,7260,10027,249,141,154,45,46])). % 116.86/117.04 cnf(10153,plain, % 116.86/117.04 (~P8(f10(a4),a4)), % 116.86/117.04 inference(scs_inference,[],[10137,7260,10027,249,141,154,45,46,1194,409])). % 116.86/117.04 cnf(10155,plain, % 116.86/117.04 (~P16(f10(a4),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[10137,7260,10027,249,141,154,45,46,1194,409,132])). % 116.86/117.04 cnf(10157,plain, % 116.86/117.04 (P15(a4,f10(a4))), % 116.86/117.04 inference(scs_inference,[],[10137,7260,10027,249,141,154,45,46,1194,409,132,130])). % 116.86/117.04 cnf(10159,plain, % 116.86/117.04 (P8(a4,f10(a4))), % 116.86/117.04 inference(scs_inference,[],[10137,7260,10027,249,141,154,45,46,1194,409,132,130,97])). % 116.86/117.04 cnf(10161,plain, % 116.86/117.04 (P10(f10(a4))), % 116.86/117.04 inference(scs_inference,[],[10137,7260,10027,249,141,154,45,46,1194,409,132,130,97,88])). % 116.86/117.04 cnf(10167,plain, % 116.86/117.04 (P16(f10(a4),a1)), % 116.86/117.04 inference(scs_inference,[],[10100,10137,7260,10027,8160,241,249,141,154,45,46,1194,409,132,130,97,88,153,139,101])). % 116.86/117.04 cnf(10171,plain, % 116.86/117.04 (P12(f10(a4),f11(a4),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[10150,141])). % 116.86/117.04 cnf(10173,plain, % 116.86/117.04 (~P12(f10(a4),f10(a4),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[10150,141,154])). % 116.86/117.04 cnf(10187,plain, % 116.86/117.04 (P8(f10(a4),f11(a4))), % 116.86/117.04 inference(scs_inference,[],[10150,141,154,2754,132,1194,409,1566,130,97])). % 116.86/117.04 cnf(10189,plain, % 116.86/117.04 (~P9(f10(a4),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[10150,141,154,2754,132,1194,409,1566,130,97,133])). % 116.86/117.04 cnf(10200,plain, % 116.86/117.04 (~P5(f11(a4),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[10153,10157,10150,241,141,154,2754,132,1194,409,1566,130,97,133,88,10055,63,140,105,101])). % 116.86/117.04 cnf(10206,plain, % 116.86/117.04 (P12(a4,f10(a4),a13)), % 116.86/117.04 inference(scs_inference,[],[10031,141])). % 116.86/117.04 cnf(10212,plain, % 116.86/117.04 (~P12(a4,a4,a13)), % 116.86/117.04 inference(scs_inference,[],[10171,10187,10159,10031,241,141,105,139,154])). % 116.86/117.04 cnf(10218,plain, % 116.86/117.04 (~P16(f10(a4),a13)), % 116.86/117.04 inference(scs_inference,[],[10171,10187,10200,10159,10031,10023,70,241,141,105,139,154,114,349,132])). % 116.86/117.04 cnf(10231,plain, % 116.86/117.04 (P12(f10(a4),f11(a4),a13)), % 116.86/117.04 inference(scs_inference,[],[10027,141])). % 116.86/117.04 cnf(10236,plain, % 116.86/117.04 (~P12(f10(a4),f10(a4),a13)), % 116.86/117.04 inference(scs_inference,[],[10173,2972,10027,249,141,153,41])). % 116.86/117.04 cnf(10239,plain, % 116.86/117.04 (~P9(f10(a4),a13)), % 116.86/117.04 inference(scs_inference,[],[10173,2972,10027,249,141,153,41,132,133])). % 116.86/117.04 cnf(10245,plain, % 116.86/117.04 (~E(f10(a4),a4)), % 116.86/117.04 inference(scs_inference,[],[10212,10206,40])). % 116.86/117.04 cnf(10246,plain, % 116.86/117.04 (~E(a4,f10(a4))), % 116.86/117.04 inference(scs_inference,[],[10212,10236,10206,40,39])). % 116.86/117.04 cnf(10410,plain, % 116.86/117.04 (~P14(x104101,f15(a4))+P1(f16(a4,x104101))), % 116.86/117.04 inference(scs_inference,[],[10086,10018,114,104])). % 116.86/117.04 cnf(10412,plain, % 116.86/117.04 (~P14(x104121,f15(a4))+P14(x104121,f16(a4,x104121))), % 116.86/117.04 inference(scs_inference,[],[10086,10018,114,104,112])). % 116.86/117.04 cnf(10414,plain, % 116.86/117.04 (~P14(x104141,f15(a4))+P6(a4,f16(a4,x104141))), % 116.86/117.04 inference(scs_inference,[],[10086,10018,114,104,112,108])). % 116.86/117.04 cnf(10456,plain, % 116.86/117.04 (~P12(f10(a4),f12(a4),a13)+~P6(f12(a4),a3)), % 116.86/117.04 inference(scs_inference,[],[10025,10031,10029,152])). % 116.86/117.04 cnf(10539,plain, % 116.86/117.04 (~P14(f15(a14),a3)+P6(f12(a4),a2)), % 116.86/117.04 inference(scs_inference,[],[72,10133,73,84,76,75,114,131])). % 116.86/117.04 cnf(10562,plain, % 116.86/117.04 (~P6(f12(a4),a3)+~P14(a13,a3)), % 116.86/117.04 inference(scs_inference,[],[72,10114,114])). % 116.86/117.04 cnf(12174,plain, % 116.86/117.04 (~P12(x121741,f10(a4),a1)), % 116.86/117.04 inference(scs_inference,[],[10167,132])). % 116.86/117.04 cnf(12183,plain, % 116.86/117.04 (~P13(a4,f10(a4))+~P13(f10(a4),x121831)+~E(x121831,f10(a4))), % 116.86/117.04 inference(scs_inference,[],[12174,10083,10246,2972,73,10029,143,50])). % 116.86/117.04 cnf(12226,plain, % 116.86/117.04 (P3(a24)), % 116.86/117.04 inference(scs_inference,[],[10023,93])). % 116.86/117.04 cnf(12231,plain, % 116.86/117.04 (P14(a24,a24)), % 116.86/117.04 inference(scs_inference,[],[12226,87])). % 116.86/117.04 cnf(12240,plain, % 116.86/117.04 (P14(f15(a4),f15(a4))), % 116.86/117.04 inference(scs_inference,[],[10016,87])). % 116.86/117.04 cnf(12246,plain, % 116.86/117.04 (P10(f9(a13,a14))), % 116.86/117.04 inference(scs_inference,[],[10004,89])). % 116.86/117.04 cnf(12250,plain, % 116.86/117.04 (P4(f11(a4))), % 116.86/117.04 inference(scs_inference,[],[10075,10004,10023,89,141,90])). % 116.86/117.04 cnf(12836,plain, % 116.86/117.04 (P14(f5(a1,f10(a4)),a1)), % 116.86/117.04 inference(scs_inference,[],[10167,113])). % 116.86/117.04 cnf(12841,plain, % 116.86/117.04 (P13(a4,f23(f15(a14),a4,f10(a4)))), % 116.86/117.04 inference(scs_inference,[],[4220,10144,10085,10167,113,5367,34,145])). % 116.86/117.04 cnf(12843,plain, % 116.86/117.04 (P14(f7(f15(a14),a4,f10(a4)),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[4220,10144,10085,10167,113,5367,34,145,149])). % 116.86/117.04 cnf(12845,plain, % 116.86/117.04 (P14(f8(f15(a14),a4,f10(a4)),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[4220,10144,10085,10167,113,5367,34,145,149,150])). % 116.86/117.04 cnf(12860,plain, % 116.86/117.04 (E(f20(f19(x128601,f8(a13,x128602,x128603)),x128604),f20(f19(x128601,f8(f15(a14),x128602,x128603)),x128604))), % 116.86/117.04 inference(scs_inference,[],[4220,10144,10085,10167,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25])). % 116.86/117.04 cnf(12861,plain, % 116.86/117.04 (E(f20(x128611,f19(x128612,f8(a13,x128613,x128614))),f20(x128611,f19(x128612,f8(f15(a14),x128613,x128614))))), % 116.86/117.04 inference(scs_inference,[],[4220,10144,10085,10167,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26])). % 116.86/117.04 cnf(12868,plain, % 116.86/117.04 (P1(f16(a4,f7(f15(a14),a4,f10(a4))))), % 116.86/117.04 inference(scs_inference,[],[4220,10144,10085,10167,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26,28,29,30,31,32,35,438])). % 116.86/117.04 cnf(12887,plain, % 116.86/117.04 (P6(f23(f15(a14),f11(a4),f12(a4)),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[4220,10121,12240,10144,10085,10167,8160,10027,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26,28,29,30,31,32,35,438,10412,6207,6802,5522,5553,1876,4,93,112,4592])). % 116.86/117.04 cnf(12889,plain, % 116.86/117.04 (P6(f23(f15(a14),a4,f10(a4)),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[4220,10121,12240,10144,10085,10167,8160,10027,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26,28,29,30,31,32,35,438,10412,6207,6802,5522,5553,1876,4,93,112,4592,148])). % 116.86/117.04 cnf(12893,plain, % 116.86/117.04 (P13(f10(a4),f23(f15(a14),a4,f10(a4)))), % 116.86/117.04 inference(scs_inference,[],[4220,10121,12240,10144,10085,10167,8160,10027,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26,28,29,30,31,32,35,438,10412,6207,6802,5522,5553,1876,4,93,112,4592,148,91,144])). % 116.86/117.04 cnf(12895,plain, % 116.86/117.04 (P16(f9(a13,a14),f17(f9(a13,a14),a14))), % 116.86/117.04 inference(scs_inference,[],[4220,10121,12240,10144,10085,10167,8160,10027,10014,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26,28,29,30,31,32,35,438,10412,6207,6802,5522,5553,1876,4,93,112,4592,148,91,144,109])). % 116.86/117.04 cnf(12897,plain, % 116.86/117.04 (~E(a13,f16(f10(a4),f7(a13,f10(a4),f11(a4))))), % 116.86/117.04 inference(scs_inference,[],[6895,4220,10121,12240,10144,10085,10167,8160,10027,10014,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26,28,29,30,31,32,35,438,10412,6207,6802,5522,5553,1876,4,93,112,4592,148,91,144,109,2])). % 116.86/117.04 cnf(12898,plain, % 116.86/117.04 (P6(f22(f12(a4),a13),a13)), % 116.86/117.04 inference(scs_inference,[],[6895,4220,10121,12240,10144,10085,10167,8160,10027,10014,83,10025,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26,28,29,30,31,32,35,438,10412,6207,6802,5522,5553,1876,4,93,112,4592,148,91,144,109,2,117])). % 116.86/117.04 cnf(12900,plain, % 116.86/117.04 (P6(f6(f12(a4),f15(a14)),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[6895,4220,10121,12240,10144,10093,10085,10167,8160,10027,254,10014,83,10025,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26,28,29,30,31,32,35,438,10412,6207,6802,5522,5553,1876,4,93,112,4592,148,91,144,109,2,117,118])). % 116.86/117.04 cnf(12909,plain, % 116.86/117.04 (P16(f9(f15(a14),f22(f12(a4),f15(a14))),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[10122,6895,4220,10121,12240,10144,10093,256,10085,10167,8160,10027,254,10014,83,10025,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26,28,29,30,31,32,35,438,10412,6207,6802,5522,5553,1876,4,93,112,4592,148,91,144,109,2,117,118,116,120,115,42,119])). % 116.86/117.04 cnf(12913,plain, % 116.86/117.04 (~P17(f10(a4),f22(f12(a4),f15(a14)))), % 116.86/117.04 inference(scs_inference,[],[10122,6895,4220,10121,12240,10144,10093,256,10085,10167,8160,10027,254,10014,83,10025,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26,28,29,30,31,32,35,438,10412,6207,6802,5522,5553,1876,4,93,112,4592,148,91,144,109,2,117,118,116,120,115,42,119,140,139])). % 116.86/117.04 cnf(12915,plain, % 116.86/117.04 (P12(f21(f12(a4),f15(a14)),f12(a4),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[10138,10122,6895,4220,10121,12240,10144,10093,256,10085,10167,8160,10027,254,10014,83,10025,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26,28,29,30,31,32,35,438,10412,6207,6802,5522,5553,1876,4,93,112,4592,148,91,144,109,2,117,118,116,120,115,42,119,140,139,135])). % 116.86/117.04 cnf(12917,plain, % 116.86/117.04 (~P12(f11(a4),f21(f12(a4),f15(a14)),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[10138,10122,6895,4220,10121,12240,10144,10093,256,10085,10167,8160,10027,254,10014,83,10025,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26,28,29,30,31,32,35,438,10412,6207,6802,5522,5553,1876,4,93,112,4592,148,91,144,109,2,117,118,116,120,115,42,119,140,139,135,154])). % 116.86/117.04 cnf(12919,plain, % 116.86/117.04 (~P2(f22(f12(a4),f15(a14)))), % 116.86/117.04 inference(scs_inference,[],[10138,10122,6895,4220,10121,12240,10144,10093,256,10085,10167,8160,10027,254,10014,83,10025,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26,28,29,30,31,32,35,438,10412,6207,6802,5522,5553,1876,4,93,112,4592,148,91,144,109,2,117,118,116,120,115,42,119,140,139,135,154,95])). % 116.86/117.04 cnf(12922,plain, % 116.86/117.04 (P12(f10(a4),f20(f10(a4),f15(a14)),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[10138,10189,10122,6895,4220,10121,12240,10144,10127,10093,256,10085,10167,8160,10027,254,10014,83,10025,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26,28,29,30,31,32,35,438,10412,6207,6802,5522,5553,1876,4,93,112,4592,148,91,144,109,2,117,118,116,120,115,42,119,140,139,135,154,95,40,142])). % 116.86/117.04 cnf(12925,plain, % 116.86/117.04 (E(f5(f8(x129251,a13,x129252),f8(x129253,x129254,a13)),f5(f8(x129251,f15(a14),x129252),f8(x129253,x129254,f15(a14))))), % 116.86/117.04 inference(scs_inference,[],[10138,10189,10122,6895,4220,4251,4282,10121,12240,10144,10127,10093,256,10085,10167,8160,10027,254,10014,251,83,10025,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26,28,29,30,31,32,35,438,10412,6207,6802,5522,5553,1876,4,93,112,4592,148,91,144,109,2,117,118,116,120,115,42,119,140,139,135,154,95,40,142,43,3])). % 116.86/117.04 cnf(12928,plain, % 116.86/117.04 (P17(f9(f15(a14),f22(f12(a4),f15(a14))),f22(f12(a4),f15(a14)))), % 116.86/117.04 inference(scs_inference,[],[10138,10189,10122,6895,4220,4251,4282,10121,12240,10144,10127,10093,256,10085,10167,8160,10027,254,10014,251,83,10025,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26,28,29,30,31,32,35,438,10412,6207,6802,5522,5553,1876,4,93,112,4592,148,91,144,109,2,117,118,116,120,115,42,119,140,139,135,154,95,40,142,43,3,123])). % 116.86/117.04 cnf(12930,plain, % 116.86/117.04 (P6(a14,f17(f9(a13,a14),a14))), % 116.86/117.04 inference(scs_inference,[],[10138,10189,10122,6895,4220,4251,4282,10121,12240,10144,10127,10093,256,10085,10167,8160,10027,254,10014,251,83,10025,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26,28,29,30,31,32,35,438,10412,6207,6802,5522,5553,1876,4,93,112,4592,148,91,144,109,2,117,118,116,120,115,42,119,140,139,135,154,95,40,142,43,3,123,106])). % 116.86/117.04 cnf(12936,plain, % 116.86/117.04 (P5(f10(a4),f8(f15(a14),a4,f10(a4)))), % 116.86/117.04 inference(scs_inference,[],[10138,10189,10122,6895,4220,4251,4282,10121,12240,10144,10127,10093,256,10085,10004,10167,8160,10027,254,10014,251,83,10025,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26,28,29,30,31,32,35,438,10412,6207,6802,5522,5553,1876,4,93,112,4592,148,91,144,109,2,117,118,116,120,115,42,119,140,139,135,154,95,40,142,43,3,123,106,111,27,37,147])). % 116.86/117.04 cnf(12938,plain, % 116.86/117.04 (P1(f16(a4,f15(a4)))), % 116.86/117.04 inference(scs_inference,[],[10138,10189,10122,6895,4220,4251,4282,10121,12240,10144,10127,10093,256,10085,10004,10167,8160,10027,254,10014,251,83,10025,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26,28,29,30,31,32,35,438,10412,6207,6802,5522,5553,1876,4,93,112,4592,148,91,144,109,2,117,118,116,120,115,42,119,140,139,135,154,95,40,142,43,3,123,106,111,27,37,147,10410])). % 116.86/117.04 cnf(12965,plain, % 116.86/117.04 (P6(f22(f12(a4),f15(a14)),f15(f22(f12(a4),f15(a14))))), % 116.86/117.04 inference(scs_inference,[],[10138,10189,10122,10124,6895,4220,4251,4282,10121,12240,10144,10127,10093,256,10085,10004,10167,8160,10027,254,10014,251,83,10025,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26,28,29,30,31,32,35,438,10412,6207,6802,5522,5553,1876,4,93,112,4592,148,91,144,109,2,117,118,116,120,115,42,119,140,139,135,154,95,40,142,43,3,123,106,111,27,37,147,10410,8,10,12,33,36,10414,5,6,7,14,15,16,17,18,19,20,21,22,7231,146,104,94])). % 116.86/117.04 cnf(12971,plain, % 116.86/117.04 (P13(f12(a4),f6(f12(a4),f15(a14)))), % 116.86/117.04 inference(scs_inference,[],[10138,10189,10122,10124,6895,4220,4251,4282,10121,12240,10144,10127,10093,256,12250,10085,10004,10167,8160,10027,254,10014,251,83,10025,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26,28,29,30,31,32,35,438,10412,6207,6802,5522,5553,1876,4,93,112,4592,148,91,144,109,2,117,118,116,120,115,42,119,140,139,135,154,95,40,142,43,3,123,106,111,27,37,147,10410,8,10,12,33,36,10414,5,6,7,14,15,16,17,18,19,20,21,22,7231,146,104,94,86,110,99])). % 116.86/117.04 cnf(12973,plain, % 116.86/117.04 (~P10(f22(f12(a4),f15(a14)))), % 116.86/117.04 inference(scs_inference,[],[10138,10189,10122,10124,6895,4220,4251,4282,10121,12240,10144,10127,10093,256,12250,10085,10004,10167,8160,10027,254,10014,251,83,10025,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26,28,29,30,31,32,35,438,10412,6207,6802,5522,5553,1876,4,93,112,4592,148,91,144,109,2,117,118,116,120,115,42,119,140,139,135,154,95,40,142,43,3,123,106,111,27,37,147,10410,8,10,12,33,36,10414,5,6,7,14,15,16,17,18,19,20,21,22,7231,146,104,94,86,110,99,85])). % 116.86/117.04 cnf(12985,plain, % 116.86/117.04 (P6(f10(a4),f16(f10(a4),a1))), % 116.86/117.04 inference(scs_inference,[],[10138,10189,10122,10124,10125,6895,4220,4251,4282,10121,12240,10144,10127,10093,256,12250,10085,10004,10167,8160,10027,254,10014,251,83,10025,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26,28,29,30,31,32,35,438,10412,6207,6802,5522,5553,1876,4,93,112,4592,148,91,144,109,2,117,118,116,120,115,42,119,140,139,135,154,95,40,142,43,3,123,106,111,27,37,147,10410,8,10,12,33,36,10414,5,6,7,14,15,16,17,18,19,20,21,22,7231,146,104,94,86,110,99,85,409,87,1566,129,130,108])). % 116.86/117.04 cnf(12987,plain, % 116.86/117.04 (~P16(f20(f10(a4),f15(a14)),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[10138,10189,10122,10124,10125,6895,4220,4251,4282,10121,12240,10144,10127,10093,256,12250,10085,10004,10167,8160,10027,254,10014,251,83,10025,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26,28,29,30,31,32,35,438,10412,6207,6802,5522,5553,1876,4,93,112,4592,148,91,144,109,2,117,118,116,120,115,42,119,140,139,135,154,95,40,142,43,3,123,106,111,27,37,147,10410,8,10,12,33,36,10414,5,6,7,14,15,16,17,18,19,20,21,22,7231,146,104,94,86,110,99,85,409,87,1566,129,130,108,132])). % 116.86/117.04 cnf(12993,plain, % 116.86/117.04 (~P16(f22(f12(a4),f15(a14)),x129931)), % 116.86/117.04 inference(scs_inference,[],[10138,10189,10122,10124,10125,6895,4220,4251,4282,10121,12240,10144,10127,10093,256,12250,10085,10004,10167,8160,10027,254,10014,251,83,10025,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26,28,29,30,31,32,35,438,10412,6207,6802,5522,5553,1876,4,93,112,4592,148,91,144,109,2,117,118,116,120,115,42,119,140,139,135,154,95,40,142,43,3,123,106,111,27,37,147,10410,8,10,12,33,36,10414,5,6,7,14,15,16,17,18,19,20,21,22,7231,146,104,94,86,110,99,85,409,87,1566,129,130,108,132,97,133,89])). % 116.86/117.04 cnf(12995,plain, % 116.86/117.04 (~P15(x129951,f22(f12(a4),f15(a14)))), % 116.86/117.04 inference(scs_inference,[],[10138,10189,10122,10124,10125,6895,4220,4251,4282,10121,12240,10144,10127,10093,256,12250,10085,10004,10167,8160,10027,254,10014,251,83,10025,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26,28,29,30,31,32,35,438,10412,6207,6802,5522,5553,1876,4,93,112,4592,148,91,144,109,2,117,118,116,120,115,42,119,140,139,135,154,95,40,142,43,3,123,106,111,27,37,147,10410,8,10,12,33,36,10414,5,6,7,14,15,16,17,18,19,20,21,22,7231,146,104,94,86,110,99,85,409,87,1566,129,130,108,132,97,133,89,88])). % 116.86/117.04 cnf(13002,plain, % 116.86/117.04 (~P6(a14,f16(a4,f7(f15(a14),a4,f10(a4))))), % 116.86/117.04 inference(scs_inference,[],[10138,10189,10122,10124,10125,6895,4220,4251,4282,10121,12240,10144,10127,10104,10093,256,10010,12250,10085,10004,10056,10167,8160,10027,254,10014,251,83,10025,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26,28,29,30,31,32,35,438,10412,6207,6802,5522,5553,1876,4,93,112,4592,148,91,144,109,2,117,118,116,120,115,42,119,140,139,135,154,95,40,142,43,3,123,106,111,27,37,147,10410,8,10,12,33,36,10414,5,6,7,14,15,16,17,18,19,20,21,22,7231,146,104,94,86,110,99,85,409,87,1566,129,130,108,132,97,133,89,88,6519,39,64,96])). % 116.86/117.04 cnf(13004,plain, % 116.86/117.04 (~P12(f20(f10(a4),f15(a14)),f10(a4),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[10138,10189,10122,10124,10125,6895,4220,4251,4282,10121,12240,10144,10127,10104,10093,256,10010,12250,10085,10004,10056,10167,10173,8160,10027,254,10014,251,83,10025,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26,28,29,30,31,32,35,438,10412,6207,6802,5522,5553,1876,4,93,112,4592,148,91,144,109,2,117,118,116,120,115,42,119,140,139,135,154,95,40,142,43,3,123,106,111,27,37,147,10410,8,10,12,33,36,10414,5,6,7,14,15,16,17,18,19,20,21,22,7231,146,104,94,86,110,99,85,409,87,1566,129,130,108,132,97,133,89,88,6519,39,64,96,153])). % 116.86/117.04 cnf(13017,plain, % 116.86/117.04 (~P11(f11(a4),f21(f12(a4),f15(a14)),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[10138,10189,10122,10124,10125,6895,4220,4251,4282,10121,12240,10161,10144,10127,10104,12246,10093,256,10010,12250,10085,10004,10056,10167,10173,8160,10027,254,10014,10071,84,76,251,83,10025,113,5367,34,145,149,150,4561,4623,4654,5398,9,11,13,23,24,25,26,28,29,30,31,32,35,438,10412,6207,6802,5522,5553,1876,4,93,112,4592,148,91,144,109,2,117,118,116,120,115,42,119,140,139,135,154,95,40,142,43,3,123,106,111,27,37,147,10410,8,10,12,33,36,10414,5,6,7,14,15,16,17,18,19,20,21,22,7231,146,104,94,86,110,99,85,409,87,1566,129,130,108,132,97,133,89,88,6519,39,64,96,153,56,47,59,101,124,107,7537,7468,141])). % 116.86/117.04 cnf(13055,plain, % 116.86/117.04 (~P16(f22(f12(a4),f15(a14)),x130551)), % 116.86/117.04 inference(rename_variables,[],[12993])). % 116.86/117.04 cnf(13059,plain, % 116.86/117.04 (~P12(x130591,f22(f12(a4),f15(a14)),x130592)), % 116.86/117.04 inference(scs_inference,[],[12915,12922,12985,12993,12995,13002,10137,10150,10021,162,7629,5367,5553,4654,4623,6207,5398,5522,4561,4592,109,1566,130])). % 116.86/117.04 cnf(13063,plain, % 116.86/117.04 (E(f5(f8(x130631,f15(a14),x130632),f8(x130633,x130634,f15(a14))),f5(f8(x130631,a13,x130632),f8(x130633,x130634,a13)))), % 116.86/117.04 inference(scs_inference,[],[12915,12922,12895,12985,12993,12995,13002,12925,10137,10150,10021,162,7629,5367,5553,4654,4623,6207,5398,5522,4561,4592,109,1566,130,132,2])). % 116.86/117.04 cnf(13064,plain, % 116.86/117.04 (~P9(f21(f12(a4),f15(a14)),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[12915,12922,12895,12985,12993,12995,13002,12925,10137,10150,10021,162,7629,5367,5553,4654,4623,6207,5398,5522,4561,4592,109,1566,130,132,2,133])). % 116.86/117.04 cnf(13068,plain, % 116.86/117.04 (P6(f6(f12(a4),a13),a13)), % 116.86/117.04 inference(scs_inference,[],[12915,12922,12895,12985,12993,12995,12909,13002,12925,10137,10150,10021,83,10025,162,7629,5367,5553,4654,4623,6207,5398,5522,4561,4592,109,1566,130,132,2,133,89,118])). % 116.86/117.04 cnf(13070,plain, % 116.86/117.04 (P7(f12(a4),f6(f12(a4),a13))), % 116.86/117.04 inference(scs_inference,[],[12915,12922,12895,12985,12993,12995,12909,13002,12925,10137,10150,10021,83,10025,162,7629,5367,5553,4654,4623,6207,5398,5522,4561,4592,109,1566,130,132,2,133,89,118,116])). % 116.86/117.04 cnf(13074,plain, % 116.86/117.04 (P7(f12(a4),f22(f12(a4),a13))), % 116.86/117.04 inference(scs_inference,[],[12887,12915,12922,12895,12985,12993,12995,12909,13002,12925,10137,10150,10021,254,83,10025,162,7629,5367,5553,4654,4623,6207,5398,5522,4561,4592,109,1566,130,132,2,133,89,118,116,120,115])). % 116.86/117.04 cnf(13078,plain, % 116.86/117.04 (P16(f9(f15(a14),f23(f15(a14),f11(a4),f12(a4))),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[12887,12915,12922,12895,12985,12993,13055,12995,12909,13002,12925,10137,10150,10021,254,83,10025,162,7629,5367,5553,4654,4623,6207,5398,5522,4561,4592,109,1566,130,132,2,133,89,118,116,120,115,55,119])). % 116.86/117.04 cnf(13082,plain, % 116.86/117.04 (~P1(f17(f9(a13,a14),a14))), % 116.86/117.04 inference(scs_inference,[],[12887,12915,12922,12895,12930,12985,12993,13055,12995,12909,13002,12925,10010,10137,10150,10021,254,83,10025,162,7629,5367,5553,4654,4623,6207,5398,5522,4561,4592,109,1566,130,132,2,133,89,118,116,120,115,55,119,140,96])). % 116.86/117.04 cnf(13092,plain, % 116.86/117.04 (P12(f21(f12(a4),a13),f12(a4),a13)), % 116.86/117.04 inference(scs_inference,[],[10094,12887,12915,12922,12917,13004,12895,12919,12930,12973,12985,12993,13055,12995,12938,12909,13002,12925,10010,10137,10150,10021,10144,254,73,249,83,10025,162,7629,5367,5553,4654,4623,6207,5398,5522,4561,4592,109,1566,130,132,2,133,89,118,116,120,115,55,119,140,96,153,139,41,47,38,59,135])). % 116.86/117.04 cnf(13094,plain, % 116.86/117.04 (~P2(f23(f15(a14),f11(a4),f12(a4)))), % 116.86/117.04 inference(scs_inference,[],[10094,12887,12915,12922,12917,13004,12895,12919,12930,12973,12985,12993,13055,12995,12938,12909,13002,12925,10010,10137,10150,10021,10144,254,73,249,83,10025,162,7629,5367,5553,4654,4623,6207,5398,5522,4561,4592,109,1566,130,132,2,133,89,118,116,120,115,55,119,140,96,153,139,41,47,38,59,135,95])). % 116.86/117.04 cnf(13096,plain, % 116.86/117.04 (P12(f11(a4),f20(f11(a4),f15(a14)),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[10129,10094,12887,12915,12922,12917,13004,12895,12919,12930,12973,12985,12993,13055,12995,12938,12909,13002,12925,10171,10010,10137,10150,10021,10144,254,73,249,83,10025,162,7629,5367,5553,4654,4623,6207,5398,5522,4561,4592,109,1566,130,132,2,133,89,118,116,120,115,55,119,140,96,153,139,41,47,38,59,135,95,142])). % 116.86/117.04 cnf(13099,plain, % 116.86/117.04 (E(f20(f23(a13,x130991,x130992),f19(x130993,f8(a13,x130994,x130995))),f20(f23(f15(a14),x130991,x130992),f19(x130993,f8(f15(a14),x130994,x130995))))), % 116.86/117.04 inference(scs_inference,[],[10129,10094,12887,12915,12922,12917,13004,12895,12919,12930,12973,12985,12993,13055,12995,12938,12909,13002,12925,12861,4313,10171,10010,10137,10150,10021,10144,254,73,251,249,83,10025,162,7629,5367,5553,4654,4623,6207,5398,5522,4561,4592,109,1566,130,132,2,133,89,118,116,120,115,55,119,140,96,153,139,41,47,38,59,135,95,142,43,3])). % 116.86/117.04 cnf(13102,plain, % 116.86/117.04 (P16(f10(a4),f8(f15(a14),a4,f10(a4)))), % 116.86/117.04 inference(scs_inference,[],[10129,10094,12887,12915,12922,12917,13004,12895,12919,12930,12936,12973,12985,12993,13055,12995,12938,12909,13002,12925,12861,4313,10161,10171,10010,10137,10150,10021,10144,254,73,251,249,83,10025,162,7629,5367,5553,4654,4623,6207,5398,5522,4561,4592,109,1566,130,132,2,133,89,118,116,120,115,55,119,140,96,153,139,41,47,38,59,135,95,142,43,3,101])). % 116.86/117.04 cnf(13104,plain, % 116.86/117.04 (P5(f10(a4),f5(a1,f10(a4)))), % 116.86/117.04 inference(scs_inference,[],[10129,10094,12887,12915,12922,12917,13004,12836,12895,12919,12930,12936,12973,12985,12993,13055,12995,12938,12909,13002,12925,12861,4313,10161,10171,10010,10137,10150,10021,69,10144,254,73,10029,251,249,83,10025,162,7629,5367,5553,4654,4623,6207,5398,5522,4561,4592,109,1566,130,132,2,133,89,118,116,120,115,55,119,140,96,153,139,41,47,38,59,135,95,142,43,3,101,114])). % 116.86/117.04 cnf(13106,plain, % 116.86/117.04 (P17(f9(f15(a14),f23(f15(a14),f11(a4),f12(a4))),f23(f15(a14),f11(a4),f12(a4)))), % 116.86/117.04 inference(scs_inference,[],[10129,10094,12887,12915,12922,12917,13004,12836,12895,12919,12930,12936,12973,12985,12993,13055,12995,12938,12909,13002,12925,12861,4313,10161,10171,10010,10137,10150,10021,69,10144,254,73,10029,251,249,83,10025,162,7629,5367,5553,4654,4623,6207,5398,5522,4561,4592,109,1566,130,132,2,133,89,118,116,120,115,55,119,140,96,153,139,41,47,38,59,135,95,142,43,3,101,114,123])). % 116.86/117.04 cnf(13108,plain, % 116.86/117.04 (P2(f9(f15(a14),f22(f12(a4),f15(a14))))), % 116.86/117.04 inference(scs_inference,[],[10129,10094,12887,12915,12922,12917,13004,12836,12895,12919,12930,12936,12973,12985,12993,13055,12995,12938,12909,13002,12925,12861,4313,10161,10171,10010,10137,10150,10021,69,10144,254,73,10029,251,249,83,10025,162,7629,5367,5553,4654,4623,6207,5398,5522,4561,4592,109,1566,130,132,2,133,89,118,116,120,115,55,119,140,96,153,139,41,47,38,59,135,95,142,43,3,101,114,123,85])). % 116.86/117.04 cnf(13115,plain, % 116.86/117.04 (~E(f21(f12(a4),a13),f12(a4))), % 116.86/117.04 inference(scs_inference,[],[10129,10094,12843,12887,12915,12922,12917,13004,12836,12893,12895,12919,12930,12936,12973,12985,12993,13055,12995,12913,12938,12909,13002,12928,12925,12861,4313,10161,10171,10010,10137,10150,10021,69,10144,254,73,10029,251,249,83,10025,162,7629,5367,5553,4654,4623,6207,5398,5522,4561,4592,109,1566,130,132,2,133,89,118,116,120,115,55,119,140,96,153,139,41,47,38,59,135,95,142,43,3,101,114,123,85,12183,67,58,7230,7259])). % 116.86/117.04 cnf(13142,plain, % 116.86/117.04 (~P10(f23(f15(a14),f11(a4),f12(a4)))), % 116.86/117.04 inference(scs_inference,[],[13092,13070,13094,10027,10031,4623,5553,5367,4654,5522,5398,6207,4561,99,4592,85])). % 116.86/117.04 cnf(13148,plain, % 116.86/117.04 (~P12(x131481,f10(a4),f8(f15(a14),a4,f10(a4)))), % 116.86/117.04 inference(scs_inference,[],[13092,13070,13094,13102,13106,10027,10031,4623,5553,5367,4654,5522,5398,6207,4561,99,4592,85,109,1566,132])). % 116.86/117.04 cnf(13153,plain, % 116.86/117.04 (P10(f9(f15(a14),f23(f15(a14),f11(a4),f12(a4))))), % 116.86/117.04 inference(scs_inference,[],[13092,13115,13070,13094,13102,13078,13106,10027,10031,4623,5553,5367,4654,5522,5398,6207,4561,99,4592,85,109,1566,132,2,133,89])). % 116.86/117.04 cnf(13155,plain, % 116.86/117.04 (P13(f9(f15(a14),f23(f15(a14),a4,f10(a4))),f23(f15(a14),a4,f10(a4)))), % 116.86/117.04 inference(scs_inference,[],[12889,13092,13115,13070,13094,13102,13078,13106,10027,10031,254,4623,5553,5367,4654,5522,5398,6207,4561,99,4592,85,109,1566,132,2,133,89,120])). % 116.86/117.04 cnf(13157,plain, % 116.86/117.04 (P16(f9(f15(a14),f23(f15(a14),a4,f10(a4))),f15(a14))), % 116.86/117.04 inference(scs_inference,[],[12889,13092,13115,13070,13094,13102,13078,13106,10027,10031,254,4623,5553,5367,4654,5522,5398,6207,4561,99,4592,85,109,1566,132,2,133,89,120,119])). % 116.86/117.04 cnf(13173,plain, % 116.86/117.04 (~P2(f23(f15(a14),a4,f10(a4)))), % 116.86/117.04 inference(scs_inference,[],[12889,13092,13115,12898,13059,13070,13094,13102,13078,13108,12868,13106,12993,10027,10031,10021,254,251,4623,5553,5367,4654,5522,5398,6207,4561,99,4592,85,109,1566,132,2,133,89,120,119,140,96,139,56,135,47,154,95])). % 116.86/117.04 cnf(13175,plain, % 116.86/117.04 (P12(f10(a4),f20(f10(a4),a13),a13)), % 116.86/117.04 inference(scs_inference,[],[10239,12889,13092,13115,12898,13059,13070,13094,13102,13078,13108,12868,13106,12993,10027,10031,10021,254,10206,251,4623,5553,5367,4654,5522,5398,6207,4561,99,4592,85,109,1566,132,2,133,89,120,119,140,96,139,56,135,47,154,95,142])). % 116.86/117.04 cnf(13181,plain, % 116.86/117.04 (P16(f10(a4),f5(a1,f10(a4)))), % 116.86/117.04 inference(scs_inference,[],[10239,12889,13092,13115,12898,13059,13070,13094,13104,13102,13078,13108,12868,13106,13063,12993,4251,10161,10027,10031,10021,254,10206,251,4623,5553,5367,4654,5522,5398,6207,4561,99,4592,85,109,1566,132,2,133,89,120,119,140,96,139,56,135,47,154,95,142,43,3,101])). % 116.86/117.04 cnf(13185,plain, % 116.86/117.04 (P15(f21(f12(a4),a13),f12(a4))), % 116.86/117.04 inference(scs_inference,[],[10239,12889,13092,13115,12898,13059,13070,13094,13104,13102,13078,13108,12868,13106,13063,12993,4251,10161,10027,10031,10021,254,10206,251,4623,5553,5367,4654,5522,5398,6207,4561,99,4592,85,109,1566,132,2,133,89,120,119,140,96,139,56,135,47,154,95,142,43,3,101,110,130])). % 116.86/117.04 cnf(13218,plain, % 116.86/117.04 (~P12(f20(f10(a4),a13),f10(a4),x132181)), % 116.86/117.04 inference(scs_inference,[],[13175,13153,13074,10150,10021,4623,5398,4654,5367,6207,4561,110,4592,85,1566])). % 116.86/117.04 cnf(13240,plain, % 116.86/117.04 (~P11(a4,f20(f10(a4),a13),a13)), % 116.86/117.04 inference(scs_inference,[],[10218,12900,13185,13082,13142,13175,13181,13153,12965,13074,13099,12922,12919,12930,10150,10021,10206,4623,5398,4654,5367,6207,4561,110,4592,85,1566,132,97,2,133,89,120,119,140,96,139,56,154])). % 116.86/117.04 cnf(13242,plain, % 116.86/117.04 (~E(f9(f15(a14),f22(f12(a4),f15(a14))),f23(f15(a14),a4,f10(a4)))), % 116.86/117.04 inference(scs_inference,[],[10218,12900,13185,13082,13142,13173,13175,13181,13153,12965,13074,13099,12922,12919,13108,12930,10150,10021,10206,4623,5398,4654,5367,6207,4561,110,4592,85,1566,132,97,2,133,89,120,119,140,96,139,56,154,47])). % 116.86/117.04 cnf(13254,plain, % 116.86/117.04 (~P6(f23(f15(a14),a4,f10(a4)),f8(f15(a14),a4,f10(a4)))), % 116.86/117.04 inference(scs_inference,[],[10218,12900,13185,12841,13082,13142,13173,13175,13148,13181,13157,13153,13155,12965,13074,13099,12860,4344,10108,12922,12893,12919,13108,12930,10231,10245,12889,2972,10150,10021,254,10206,10083,73,251,4623,5398,4654,5367,6207,4561,110,4592,85,1566,132,97,2,133,89,120,119,140,96,139,56,154,47,59,95,142,43,3,123,143])). % 116.86/117.04 cnf(13258,plain, % 116.86/117.04 (~P17(f23(f15(a14),f11(a4),f12(a4)),x132581)), % 116.86/117.04 inference(scs_inference,[],[10218,12900,13185,12841,13082,13142,13173,13175,13148,13181,13157,13153,13155,12965,13074,13099,12860,4344,10108,12922,12893,12919,13108,12930,10231,10245,12889,2972,10150,10021,254,10206,10083,73,251,4623,5398,4654,5367,6207,4561,110,4592,85,1566,132,97,2,133,89,120,119,140,96,139,56,154,47,59,95,142,43,3,123,143,109])). % 116.86/117.04 cnf(13341,plain, % 116.86/117.04 ($false), % 116.86/117.04 inference(scs_inference,[],[73,10073,75,10025,83,10069,249,251,76,10029,241,10023,84,7601,10014,4220,10206,439,10144,214,10122,69,10031,13092,12889,10090,13175,70,13094,12922,10161,10009,10231,10121,13142,6895,13148,13157,10155,12938,13096,12936,12928,13070,13074,13068,13242,12897,13254,12971,13218,12231,12845,12987,13258,13017,13240,13064,243,88,2,132,130,1566,91,409,99,110,141,7230,58,101,3,43,103,45,95,40,154,38,56,41,139,67,153,96,140,42,46,55,64,61,39,54,121,114,151,122,131,97,7307,10539,10562,10456]), % 116.86/117.04 ['proof']). % 116.86/117.06 % SZS output end Proof % 116.86/117.06 % Total time :116.180000s %------------------------------------------------------------------------------