%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PRO010+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 : n018.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:44 EDT 2024 % Result : Theorem 116.74s 116.90s % Output : CNFRefutation 116.82s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : PRO010+2 : TPTP v8.2.0. Released v4.0.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.11/0.33 % Computer : n018.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Thu Jun 20 06:31:53 EDT 2024 % 0.11/0.33 % CPUTime : % 0.18/0.56 start to proof:theBenchmark % 116.70/116.88 %------------------------------------------- % 116.70/116.88 % File :CSE---1.7 % 116.70/116.88 % Problem :theBenchmark % 116.70/116.88 % Transform :cnf % 116.70/116.88 % Format :tptp:raw % 116.70/116.88 % Command :java -jar mcs_scs.jar %d %s % 116.70/116.88 % 116.70/116.88 % Result :Theorem 116.120000s % 116.70/116.88 % Output :CNFRefutation 116.120000s % 116.70/116.88 %------------------------------------------- % 116.70/116.89 %------------------------------------------------------------------------------ % 116.70/116.89 % File : PRO010+2 : TPTP v8.2.0. Released v4.0.0. % 116.70/116.89 % Domain : Processes % 116.70/116.89 % Problem : PSL cliff problem coe-7.1.3 % 116.70/116.89 % Version : Especial : Reduced > Especial. % 116.70/116.89 % English : % 116.70/116.89 % Refs : [Hal09] Halcomb (2009), Email to G. Sutcliffe % 116.70/116.89 % Source : [Hal09] % 116.70/116.89 % Names : minimal-subset-p9__coe-7.1.3-pd [Hal09] % 116.70/116.89 % 116.70/116.89 % Status : Theorem % 116.70/116.89 % Rating : 0.19 v8.2.0, 0.22 v7.5.0, 0.25 v7.4.0, 0.20 v7.3.0, 0.21 v7.2.0, 0.17 v7.1.0, 0.22 v7.0.0, 0.13 v6.4.0, 0.15 v6.3.0, 0.12 v6.2.0, 0.20 v6.0.0, 0.13 v5.5.0, 0.15 v5.4.0, 0.14 v5.3.0, 0.19 v5.2.0, 0.10 v5.1.0, 0.19 v5.0.0, 0.17 v4.0.1, 0.22 v4.0.0 % 116.70/116.89 % Syntax : Number of formulae : 46 ( 12 unt; 0 def) % 116.70/116.89 % Number of atoms : 138 ( 10 equ) % 116.70/116.89 % Maximal formula atoms : 9 ( 3 avg) % 116.70/116.89 % Number of connectives : 111 ( 19 ~; 4 |; 51 &) % 116.70/116.89 % ( 7 <=>; 30 =>; 0 <=; 0 <~>) % 116.70/116.89 % Maximal formula depth : 12 ( 5 avg) % 116.70/116.89 % Maximal term depth : 1 ( 1 avg) % 116.70/116.89 % Number of predicates : 18 ( 17 usr; 0 prp; 1-3 aty) % 116.70/116.89 % Number of functors : 5 ( 5 usr; 5 con; 0-0 aty) % 116.70/116.89 % Number of variables : 104 ( 81 !; 23 ?) % 116.70/116.89 % SPC : FOF_THM_RFO_SEQ % 116.70/116.89 % 116.70/116.89 % Comments : % 116.70/116.89 %------------------------------------------------------------------------------ % 116.70/116.89 fof(sos,axiom, % 116.70/116.89 ! [X0,X1,X2,X3] : % 116.70/116.89 ( ( min_precedes(X0,X1,X3) % 116.70/116.89 & min_precedes(X1,X2,X3) ) % 116.70/116.89 => min_precedes(X0,X2,X3) ) ). % 116.70/116.89 % 116.70/116.89 fof(sos_01,axiom, % 116.70/116.89 ! [X4,X5,X6] : % 116.70/116.89 ( ( earlier(X4,X5) % 116.70/116.89 & earlier(X5,X6) ) % 116.70/116.89 => earlier(X4,X6) ) ). % 116.70/116.89 % 116.70/116.89 fof(sos_02,axiom, % 116.70/116.89 ! [X7,X8,X9,X10] : % 116.70/116.89 ( ( occurrence_of(X9,X10) % 116.70/116.89 & root_occ(X7,X9) % 116.70/116.89 & root_occ(X8,X9) ) % 116.70/116.89 => X7 = X8 ) ). % 116.70/116.89 % 116.70/116.89 fof(sos_03,axiom, % 116.70/116.89 ! [X11,X12,X13,X14] : % 116.70/116.89 ( ( occurrence_of(X13,X14) % 116.70/116.89 & ~ atomic(X14) % 116.70/116.89 & leaf_occ(X11,X13) % 116.70/116.89 & leaf_occ(X12,X13) ) % 116.70/116.89 => X11 = X12 ) ). % 116.70/116.89 % 116.70/116.89 fof(sos_04,axiom, % 116.70/116.89 ! [X15,X16,X17] : % 116.70/116.89 ( next_subocc(X15,X16,X17) % 116.70/116.89 <=> ( min_precedes(X15,X16,X17) % 116.70/116.89 & ~ ? [X18] : % 116.70/116.89 ( min_precedes(X15,X18,X17) % 116.70/116.89 & min_precedes(X18,X16,X17) ) ) ) ). % 116.70/116.89 % 116.70/116.89 fof(sos_05,axiom, % 116.70/116.89 ! [X19,X20,X21] : % 116.70/116.89 ( next_subocc(X19,X20,X21) % 116.70/116.89 => ( arboreal(X19) % 116.70/116.89 & arboreal(X20) ) ) ). % 116.70/116.89 % 116.70/116.89 fof(sos_06,axiom, % 116.70/116.89 ! [X22,X23,X24] : % 116.70/116.89 ( min_precedes(X22,X23,X24) % 116.70/116.89 => precedes(X22,X23) ) ). % 116.70/116.89 % 116.70/116.89 fof(sos_07,axiom, % 116.74/116.89 ! [X25,X26,X27] : % 116.74/116.89 ( min_precedes(X25,X26,X27) % 116.74/116.89 => ~ root(X26,X27) ) ). % 116.74/116.89 % 116.74/116.89 fof(sos_08,axiom, % 116.74/116.89 ! [X28,X29] : % 116.74/116.89 ( precedes(X28,X29) % 116.74/116.89 <=> ( earlier(X28,X29) % 116.74/116.89 & legal(X29) ) ) ). % 116.74/116.89 % 116.74/116.89 fof(sos_09,axiom, % 116.74/116.89 ! [X30,X31] : % 116.74/116.89 ( earlier(X30,X31) % 116.74/116.89 => ~ earlier(X31,X30) ) ). % 116.74/116.89 % 116.74/116.89 fof(sos_10,axiom, % 116.74/116.89 ! [X32,X33] : % 116.74/116.89 ( root_occ(X32,X33) % 116.74/116.89 <=> ? [X34] : % 116.74/116.89 ( occurrence_of(X33,X34) % 116.74/116.89 & subactivity_occurrence(X32,X33) % 116.74/116.89 & root(X32,X34) ) ) ). % 116.74/116.89 % 116.74/116.89 fof(sos_11,axiom, % 116.74/116.89 ! [X35,X36] : % 116.74/116.89 ( leaf_occ(X35,X36) % 116.74/116.89 <=> ? [X37] : % 116.74/116.89 ( occurrence_of(X36,X37) % 116.74/116.89 & subactivity_occurrence(X35,X36) % 116.74/116.89 & leaf(X35,X37) ) ) ). % 116.74/116.89 % 116.74/116.89 fof(sos_12,axiom, % 116.74/116.89 ! [X38,X39] : % 116.74/116.89 ( root(X38,X39) % 116.74/116.89 => legal(X38) ) ). % 116.74/116.89 % 116.74/116.89 fof(sos_13,axiom, % 116.74/116.89 ! [X40,X41] : % 116.74/116.89 ( occurrence_of(X40,X41) % 116.74/116.89 => ( arboreal(X40) % 116.74/116.89 <=> atomic(X41) ) ) ). % 116.74/116.89 % 116.74/116.89 fof(sos_14,axiom, % 116.74/116.89 ! [X42,X43] : % 116.74/116.89 ( leaf(X42,X43) % 116.74/116.89 <=> ( ( root(X42,X43) % 116.74/116.89 | ? [X44] : min_precedes(X44,X42,X43) ) % 116.74/116.89 & ~ ? [X45] : min_precedes(X42,X45,X43) ) ) ). % 116.74/116.89 % 116.74/116.89 fof(sos_15,axiom, % 116.74/116.89 ! [X46,X47] : % 116.74/116.89 ( atocc(X46,X47) % 116.74/116.89 <=> ? [X48] : % 116.74/116.89 ( subactivity(X47,X48) % 116.74/116.89 & atomic(X48) % 116.74/116.89 & occurrence_of(X46,X48) ) ) ). % 116.74/116.89 % 116.74/116.89 fof(sos_16,axiom, % 116.74/116.89 ! [X49,X50] : % 116.74/116.89 ( ( atocc(X49,X50) % 116.74/116.89 & legal(X49) ) % 116.74/116.89 => root(X49,X50) ) ). % 116.74/116.90 % 116.74/116.90 fof(sos_17,axiom, % 116.74/116.90 ! [X51] : % 116.74/116.90 ( legal(X51) % 116.74/116.90 => arboreal(X51) ) ). % 116.74/116.90 % 116.74/116.90 fof(sos_18,axiom, % 116.74/116.90 ! [X52] : % 116.74/116.90 ( activity_occurrence(X52) % 116.74/116.90 => ? [X53] : % 116.74/116.90 ( activity(X53) % 116.74/116.90 & occurrence_of(X52,X53) ) ) ). % 116.74/116.90 % 116.74/116.90 fof(sos_19,axiom, % 116.74/116.90 ! [X54,X55] : % 116.74/116.90 ( subactivity_occurrence(X54,X55) % 116.74/116.90 => ( activity_occurrence(X54) % 116.74/116.90 & activity_occurrence(X55) ) ) ). % 116.74/116.90 % 116.74/116.90 fof(sos_20,axiom, % 116.74/116.90 ! [X56,X57,X58] : % 116.74/116.90 ( ( occurrence_of(X56,X58) % 116.74/116.90 & root_occ(X57,X56) ) % 116.74/116.90 => ~ ? [X59] : min_precedes(X59,X57,X58) ) ). % 116.74/116.90 % 116.74/116.90 fof(sos_21,axiom, % 116.74/116.90 ! [X60,X61,X62] : % 116.74/116.90 ( ( occurrence_of(X60,X62) % 116.74/116.90 & leaf_occ(X61,X60) ) % 116.74/116.90 => ~ ? [X63] : min_precedes(X61,X63,X62) ) ). % 116.74/116.90 % 116.74/116.90 fof(sos_22,axiom, % 116.74/116.90 ! [X64,X65,X66] : % 116.74/116.90 ( ( occurrence_of(X64,X65) % 116.74/116.90 & occurrence_of(X64,X66) ) % 116.74/116.90 => X65 = X66 ) ). % 116.74/116.90 % 116.74/116.90 fof(sos_23,axiom, % 116.74/116.90 ! [X67,X68] : % 116.74/116.90 ( ( leaf(X67,X68) % 116.74/116.90 & ~ atomic(X68) ) % 116.74/116.90 => ? [X69] : % 116.74/116.90 ( occurrence_of(X69,X68) % 116.74/116.90 & leaf_occ(X67,X69) ) ) ). % 116.74/116.90 % 116.74/116.90 fof(sos_24,axiom, % 116.74/116.90 ! [X70,X71,X72] : % 116.74/116.90 ( min_precedes(X71,X72,X70) % 116.74/116.90 => ? [X73] : % 116.74/116.90 ( occurrence_of(X73,X70) % 116.74/116.90 & subactivity_occurrence(X71,X73) % 116.74/116.90 & subactivity_occurrence(X72,X73) ) ) ). % 116.74/116.90 % 116.74/116.90 fof(sos_25,axiom, % 116.74/116.90 ! [X74,X75] : % 116.74/116.90 ( ( leaf(X74,X75) % 116.74/116.90 & ~ atomic(X75) ) % 116.74/116.90 => ? [X76] : % 116.74/116.90 ( occurrence_of(X76,X75) % 116.74/116.90 & leaf_occ(X74,X76) ) ) ). % 116.74/116.90 % 116.74/116.90 fof(sos_26,axiom, % 116.74/116.90 ! [X77,X78,X79] : % 116.74/116.90 ( min_precedes(X78,X79,X77) % 116.74/116.90 => ? [X80,X81] : % 116.74/116.90 ( subactivity(X80,X77) % 116.74/116.90 & subactivity(X81,X77) % 116.74/116.90 & atocc(X78,X80) % 116.74/116.90 & atocc(X79,X81) ) ) ). % 116.74/116.90 % 116.74/116.90 fof(sos_27,axiom, % 116.74/116.90 ! [X82,X83] : % 116.74/116.90 ( root(X83,X82) % 116.74/116.90 => ? [X84] : % 116.74/116.90 ( subactivity(X84,X82) % 116.74/116.90 & atocc(X83,X84) ) ) ). % 116.74/116.90 % 116.74/116.90 fof(sos_28,axiom, % 116.74/116.90 ! [X85,X86,X87,X88] : % 116.74/116.90 ( ( occurrence_of(X86,X85) % 116.74/116.90 & arboreal(X87) % 116.74/116.90 & arboreal(X88) % 116.74/116.90 & subactivity_occurrence(X87,X86) % 116.74/116.90 & subactivity_occurrence(X88,X86) ) % 116.74/116.90 => ( min_precedes(X87,X88,X85) % 116.74/116.90 | min_precedes(X88,X87,X85) % 116.74/116.90 | X87 = X88 ) ) ). % 116.74/116.90 % 116.74/116.90 fof(sos_29,axiom, % 116.74/116.90 ! [X89,X90] : % 116.74/116.90 ( occurrence_of(X90,X89) % 116.74/116.90 => ( activity(X89) % 116.74/116.90 & activity_occurrence(X90) ) ) ). % 116.74/116.90 % 116.74/116.90 fof(sos_30,axiom, % 116.74/116.90 ! [X91,X92] : % 116.74/116.90 ( ( occurrence_of(X92,X91) % 116.74/116.90 & ~ atomic(X91) ) % 116.74/116.90 => ? [X93] : % 116.74/116.90 ( root(X93,X91) % 116.74/116.90 & subactivity_occurrence(X93,X92) ) ) ). % 116.74/116.90 % 116.74/116.90 fof(sos_31,axiom, % 116.74/116.90 ! [X94] : % 116.74/116.90 ( activity(X94) % 116.74/116.90 => subactivity(X94,X94) ) ). % 116.74/116.90 % 116.74/116.90 fof(sos_32,axiom, % 116.74/116.90 ! [X95] : % 116.74/116.90 ( occurrence_of(X95,tptp0) % 116.74/116.90 => ? [X96,X97,X98] : % 116.74/116.90 ( occurrence_of(X96,tptp3) % 116.74/116.90 & root_occ(X96,X95) % 116.74/116.90 & occurrence_of(X97,tptp4) % 116.74/116.90 & next_subocc(X96,X97,tptp0) % 116.74/116.90 & ( occurrence_of(X98,tptp1) % 116.74/116.90 | occurrence_of(X98,tptp2) ) % 116.74/116.90 & next_subocc(X97,X98,tptp0) % 116.74/116.90 & leaf_occ(X98,X95) ) ) ). % 116.74/116.90 % 116.74/116.90 fof(sos_33,axiom, % 116.74/116.90 activity(tptp0) ). % 116.74/116.90 % 116.74/116.90 fof(sos_34,axiom, % 116.74/116.90 ~ atomic(tptp0) ). % 116.74/116.90 % 116.74/116.90 fof(sos_35,axiom, % 116.74/116.90 atomic(tptp4) ). % 116.74/116.90 % 116.74/116.90 fof(sos_36,axiom, % 116.74/116.90 atomic(tptp1) ). % 116.74/116.90 % 116.74/116.90 fof(sos_37,axiom, % 116.74/116.90 atomic(tptp2) ). % 116.74/116.90 % 116.74/116.90 fof(sos_38,axiom, % 116.74/116.90 atomic(tptp3) ). % 116.74/116.90 % 116.74/116.90 fof(sos_39,axiom, % 116.74/116.90 tptp4 != tptp3 ). % 116.74/116.90 % 116.74/116.90 fof(sos_40,axiom, % 116.74/116.90 tptp4 != tptp1 ). % 116.74/116.90 % 116.74/116.90 fof(sos_41,axiom, % 116.74/116.90 tptp4 != tptp2 ). % 116.74/116.90 % 116.74/116.90 fof(sos_42,axiom, % 116.74/116.90 tptp3 != tptp1 ). % 116.74/116.90 % 116.74/116.90 fof(sos_43,axiom, % 116.74/116.90 tptp3 != tptp2 ). % 116.74/116.90 % 116.74/116.90 fof(sos_44,axiom, % 116.74/116.90 tptp1 != tptp2 ). % 116.74/116.90 % 116.74/116.90 fof(goals,conjecture, % 116.74/116.90 ! [X99] : % 116.74/116.90 ( occurrence_of(X99,tptp0) % 116.74/116.90 => ? [X100,X101] : % 116.74/116.90 ( leaf_occ(X101,X99) % 116.74/116.90 & ( occurrence_of(X101,tptp1) % 116.74/116.90 => ~ ? [X102] : % 116.74/116.90 ( occurrence_of(X102,tptp2) % 116.74/116.90 & min_precedes(X100,X102,tptp0) ) ) % 116.74/116.90 & ( occurrence_of(X101,tptp2) % 116.74/116.90 => ~ ? [X103] : % 116.74/116.90 ( occurrence_of(X103,tptp1) % 116.74/116.90 & min_precedes(X100,X103,tptp0) ) ) ) ) ). % 116.74/116.90 % 116.74/116.90 %------------------------------------------------------------------------------ % 116.74/116.90 %------------------------------------------- % 116.74/116.90 % Proof found % 116.74/116.90 % SZS status Theorem for theBenchmark % 116.74/116.90 % SZS output start Proof % 116.74/116.90 %ClaNum:164(EqnAxiom:72) % 116.74/116.90 %VarNum:431(SingletonVarNum:181) % 116.74/116.90 %MaxLitNum:8 % 116.74/116.90 %MaxfuncDepth:1 % 116.74/116.90 %SharedTerms:19 % 116.74/116.90 %goalClause: 78 108 129 130 138 142 143 148 149 151 % 116.74/116.90 %singleGoalClaCount:1 % 116.74/116.90 [73]P1(a1) % 116.74/116.90 [74]P1(a25) % 116.74/116.90 [75]P1(a2) % 116.74/116.90 [76]P1(a24) % 116.74/116.90 [77]P2(a3) % 116.74/116.90 [78]P6(a4,a3) % 116.74/116.90 [79]~E(a1,a25) % 116.74/116.90 [80]~E(a1,a2) % 116.74/116.90 [81]~E(a2,a25) % 116.74/116.90 [82]~E(a1,a24) % 116.74/116.90 [83]~E(a24,a25) % 116.74/116.90 [84]~E(a24,a2) % 116.74/116.90 [85]~P1(a3) % 116.74/116.90 [86]~P7(x861)+P3(x861) % 116.74/116.90 [88]~P2(x881)+P13(x881,x881) % 116.74/116.90 [87]~P4(x871)+P2(f13(x871)) % 116.74/116.90 [95]~P4(x951)+P6(x951,f13(x951)) % 116.74/116.90 [101]~P6(x1011,a3)+P6(f5(x1011),a1) % 116.74/116.90 [102]~P6(x1021,a3)+P6(f11(x1021),a25) % 116.74/116.90 [103]~P6(x1031,a3)+P16(f5(x1031),x1031) % 116.74/116.90 [104]~P6(x1041,a3)+P9(f12(x1041),x1041) % 116.74/116.90 [134]~P6(x1341,a3)+P11(f5(x1341),f11(x1341),a3) % 116.74/116.90 [135]~P6(x1351,a3)+P11(f11(x1351),f12(x1351),a3) % 116.74/116.90 [89]P7(x891)+~P14(x892,x891) % 116.74/116.90 [90]P7(x901)+~P15(x901,x902) % 116.74/116.90 [91]P4(x911)+~P6(x911,x912) % 116.74/116.90 [92]P4(x921)+~P17(x922,x921) % 116.74/116.90 [93]P4(x931)+~P17(x931,x932) % 116.74/116.90 [94]P2(x941)+~P6(x942,x941) % 116.74/116.90 [98]~P14(x981,x982)+P8(x981,x982) % 116.74/116.90 [99]~P16(x991,x992)+P17(x991,x992) % 116.74/116.90 [100]~P9(x1001,x1002)+P17(x1001,x1002) % 116.74/116.90 [107]~P8(x1072,x1071)+~P8(x1071,x1072) % 116.74/116.90 [110]~P5(x1101,x1102)+P1(f14(x1101,x1102)) % 116.74/116.90 [113]~P16(x1132,x1131)+P6(x1131,f15(x1132,x1131)) % 116.74/116.90 [114]~P9(x1142,x1141)+P6(x1141,f19(x1142,x1141)) % 116.74/116.90 [115]~P5(x1151,x1152)+P6(x1151,f14(x1151,x1152)) % 116.74/116.90 [116]~P16(x1161,x1162)+P15(x1161,f15(x1161,x1162)) % 116.74/116.90 [117]~P9(x1171,x1172)+P10(x1171,f19(x1171,x1172)) % 116.74/116.90 [118]~P15(x1181,x1182)+P5(x1181,f6(x1182,x1181)) % 116.74/116.90 [119]~P5(x1192,x1191)+P13(x1191,f14(x1192,x1191)) % 116.74/116.90 [120]~P15(x1202,x1201)+P13(f6(x1201,x1202),x1201) % 116.74/116.90 [136]P3(x1361)+~P11(x1362,x1361,x1363) % 116.74/116.90 [137]P3(x1371)+~P11(x1371,x1372,x1373) % 116.74/116.90 [139]P14(x1391,x1392)+~P12(x1391,x1392,x1393) % 116.74/116.90 [140]~P15(x1401,x1402)+~P12(x1403,x1401,x1402) % 116.74/116.90 [141]~P10(x1411,x1412)+~P12(x1411,x1413,x1412) % 116.74/116.90 [150]~P11(x1501,x1502,x1503)+P12(x1501,x1502,x1503) % 116.74/116.90 [154]~P12(x1543,x1541,x1542)+P17(x1541,f23(x1542,x1543,x1541)) % 116.74/116.90 [155]~P12(x1551,x1553,x1552)+P17(x1551,f23(x1552,x1551,x1553)) % 116.74/116.90 [156]~P12(x1561,x1563,x1562)+P5(x1561,f8(x1562,x1561,x1563)) % 116.74/116.90 [157]~P12(x1573,x1571,x1572)+P5(x1571,f9(x1572,x1573,x1571)) % 116.74/116.90 [158]~P12(x1582,x1583,x1581)+P6(f23(x1581,x1582,x1583),x1581) % 116.74/116.90 [159]~P12(x1592,x1593,x1591)+P13(f8(x1591,x1592,x1593),x1591) % 116.74/116.90 [160]~P12(x1602,x1603,x1601)+P13(f9(x1601,x1602,x1603),x1601) % 116.74/116.90 [108]P6(x1081,a24)+~P9(x1081,a4)+P6(x1081,a2) % 116.74/116.90 [111]~P6(x1111,a3)+P6(f12(x1111),a2)+P6(f12(x1111),a24) % 116.74/116.90 [96]~P6(x962,x961)+P1(x961)+~P3(x962) % 116.74/116.90 [97]~P6(x971,x972)+P3(x971)+~P1(x972) % 116.74/116.90 [105]~P7(x1052)+~P8(x1051,x1052)+P14(x1051,x1052) % 116.74/116.90 [106]~P7(x1061)+~P5(x1061,x1062)+P15(x1061,x1062) % 116.74/116.90 [122]~P10(x1222,x1221)+P1(x1221)+P9(x1222,f22(x1222,x1221)) % 116.74/116.90 [123]~P10(x1232,x1231)+P1(x1231)+P9(x1232,f7(x1232,x1231)) % 116.74/116.90 [124]~P10(x1242,x1241)+P1(x1241)+P6(f22(x1242,x1241),x1241) % 116.74/116.90 [125]~P10(x1252,x1251)+P1(x1251)+P6(f7(x1252,x1251),x1251) % 116.74/116.90 [126]~P6(x1262,x1261)+P1(x1261)+P15(f10(x1261,x1262),x1261) % 116.74/116.90 [127]~P6(x1272,x1271)+P1(x1271)+P17(f10(x1271,x1272),x1272) % 116.74/116.90 [129]~P9(x1291,a4)+P6(x1291,a2)+P6(f16(x1292,x1291),a2) % 116.74/116.90 [130]~P9(x1301,a4)+P6(x1301,a24)+P6(f17(x1302,x1301),a24) % 116.74/116.90 [138]~P9(x1382,a4)+P6(f16(x1381,x1382),a2)+P6(f17(x1381,x1382),a24) % 116.74/116.90 [142]~P9(x1421,a4)+P6(x1421,a2)+P12(x1422,f16(x1422,x1421),a3) % 116.74/116.90 [143]~P9(x1431,a4)+P6(x1431,a24)+P12(x1432,f17(x1432,x1431),a3) % 116.74/116.90 [144]~P15(x1441,x1442)+P10(x1441,x1442)+P12(x1441,f20(x1441,x1442),x1442) % 116.74/116.90 [145]~P10(x1451,x1452)+P15(x1451,x1452)+P12(f21(x1451,x1452),x1451,x1452) % 116.74/116.90 [148]~P9(x1482,a4)+P12(x1481,f16(x1481,x1482),a3)+P6(f17(x1481,x1482),a24) % 116.74/116.90 [149]~P9(x1492,a4)+P12(x1491,f17(x1491,x1492),a3)+P6(f16(x1491,x1492),a2) % 116.74/116.90 [151]~P9(x1512,a4)+P12(x1511,f16(x1511,x1512),a3)+P12(x1511,f17(x1511,x1512),a3) % 116.74/116.90 [109]~P6(x1093,x1091)+E(x1091,x1092)+~P6(x1093,x1092) % 116.74/116.90 [112]~P8(x1121,x1123)+P8(x1121,x1122)+~P8(x1123,x1122) % 116.74/116.90 [152]P10(x1521,x1522)+~P12(x1523,x1521,x1522)+P12(x1521,f20(x1521,x1522),x1522) % 116.74/116.90 [163]~P12(x1631,x1632,x1633)+P11(x1631,x1632,x1633)+P12(x1631,f18(x1631,x1632,x1633),x1633) % 116.74/116.90 [164]~P12(x1641,x1642,x1643)+P11(x1641,x1642,x1643)+P12(f18(x1641,x1642,x1643),x1642,x1643) % 116.74/116.90 [146]~P6(x1461,x1462)+~P12(x1464,x1463,x1462)+~P16(x1463,x1461) % 116.74/116.90 [147]~P6(x1471,x1472)+~P12(x1473,x1474,x1472)+~P9(x1473,x1471) % 116.74/116.90 [161]~P12(x1611,x1614,x1613)+P12(x1611,x1612,x1613)+~P12(x1614,x1612,x1613) % 116.74/116.90 [162]~P11(x1624,x1622,x1623)+~P12(x1621,x1622,x1623)+~P12(x1624,x1621,x1623) % 116.74/116.91 [121]~P6(x1211,x1213)+~P13(x1212,x1213)+P5(x1211,x1212)+~P1(x1213) % 116.74/116.91 [132]~P15(x1321,x1323)+~P17(x1321,x1322)+P16(x1321,x1322)+~P6(x1322,x1323) % 116.74/116.91 [133]~P17(x1331,x1332)+~P10(x1331,x1333)+P9(x1331,x1332)+~P6(x1332,x1333) % 116.74/116.91 [128]~P16(x1282,x1283)+~P16(x1281,x1283)+E(x1281,x1282)+~P6(x1283,x1284) % 116.74/116.91 [131]~P9(x1312,x1314)+~P9(x1311,x1314)+E(x1311,x1312)+~P6(x1314,x1313)+P1(x1313) % 116.74/116.91 [153]P12(x1531,x1532,x1533)+~P3(x1532)+~P3(x1531)+~P17(x1532,x1534)+~P17(x1531,x1534)+E(x1531,x1532)+P12(x1532,x1531,x1533)+~P6(x1534,x1533) % 116.74/116.91 %EqnAxiom % 116.74/116.91 [1]E(x11,x11) % 116.74/116.91 [2]E(x22,x21)+~E(x21,x22) % 116.74/116.91 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 116.74/116.91 [4]~E(x41,x42)+E(f13(x41),f13(x42)) % 116.74/116.91 [5]~E(x51,x52)+E(f18(x51,x53,x54),f18(x52,x53,x54)) % 116.74/116.91 [6]~E(x61,x62)+E(f18(x63,x61,x64),f18(x63,x62,x64)) % 116.74/116.91 [7]~E(x71,x72)+E(f18(x73,x74,x71),f18(x73,x74,x72)) % 116.74/116.91 [8]~E(x81,x82)+E(f5(x81),f5(x82)) % 116.74/116.91 [9]~E(x91,x92)+E(f11(x91),f11(x92)) % 116.74/116.91 [10]~E(x101,x102)+E(f9(x101,x103,x104),f9(x102,x103,x104)) % 116.74/116.91 [11]~E(x111,x112)+E(f9(x113,x111,x114),f9(x113,x112,x114)) % 116.74/116.91 [12]~E(x121,x122)+E(f9(x123,x124,x121),f9(x123,x124,x122)) % 116.74/116.91 [13]~E(x131,x132)+E(f12(x131),f12(x132)) % 116.74/116.91 [14]~E(x141,x142)+E(f14(x141,x143),f14(x142,x143)) % 116.74/116.91 [15]~E(x151,x152)+E(f14(x153,x151),f14(x153,x152)) % 116.74/116.91 [16]~E(x161,x162)+E(f23(x161,x163,x164),f23(x162,x163,x164)) % 116.74/116.91 [17]~E(x171,x172)+E(f23(x173,x171,x174),f23(x173,x172,x174)) % 116.74/116.91 [18]~E(x181,x182)+E(f23(x183,x184,x181),f23(x183,x184,x182)) % 116.74/116.91 [19]~E(x191,x192)+E(f17(x191,x193),f17(x192,x193)) % 116.74/116.91 [20]~E(x201,x202)+E(f17(x203,x201),f17(x203,x202)) % 116.74/116.91 [21]~E(x211,x212)+E(f15(x211,x213),f15(x212,x213)) % 116.74/116.91 [22]~E(x221,x222)+E(f15(x223,x221),f15(x223,x222)) % 116.74/116.91 [23]~E(x231,x232)+E(f19(x231,x233),f19(x232,x233)) % 116.74/116.91 [24]~E(x241,x242)+E(f19(x243,x241),f19(x243,x242)) % 116.74/116.91 [25]~E(x251,x252)+E(f16(x251,x253),f16(x252,x253)) % 116.74/116.91 [26]~E(x261,x262)+E(f16(x263,x261),f16(x263,x262)) % 116.74/116.91 [27]~E(x271,x272)+E(f20(x271,x273),f20(x272,x273)) % 116.74/116.91 [28]~E(x281,x282)+E(f20(x283,x281),f20(x283,x282)) % 116.74/116.91 [29]~E(x291,x292)+E(f21(x291,x293),f21(x292,x293)) % 116.74/116.91 [30]~E(x301,x302)+E(f21(x303,x301),f21(x303,x302)) % 116.74/116.91 [31]~E(x311,x312)+E(f6(x311,x313),f6(x312,x313)) % 116.74/116.91 [32]~E(x321,x322)+E(f6(x323,x321),f6(x323,x322)) % 116.74/116.91 [33]~E(x331,x332)+E(f8(x331,x333,x334),f8(x332,x333,x334)) % 116.74/116.91 [34]~E(x341,x342)+E(f8(x343,x341,x344),f8(x343,x342,x344)) % 116.74/116.91 [35]~E(x351,x352)+E(f8(x353,x354,x351),f8(x353,x354,x352)) % 116.74/116.91 [36]~E(x361,x362)+E(f10(x361,x363),f10(x362,x363)) % 116.74/116.91 [37]~E(x371,x372)+E(f10(x373,x371),f10(x373,x372)) % 116.74/116.91 [38]~E(x381,x382)+E(f22(x381,x383),f22(x382,x383)) % 116.74/116.91 [39]~E(x391,x392)+E(f22(x393,x391),f22(x393,x392)) % 116.74/116.91 [40]~E(x401,x402)+E(f7(x401,x403),f7(x402,x403)) % 116.74/116.91 [41]~E(x411,x412)+E(f7(x413,x411),f7(x413,x412)) % 116.74/116.91 [42]~P1(x421)+P1(x422)+~E(x421,x422) % 116.74/116.91 [43]P12(x432,x433,x434)+~E(x431,x432)+~P12(x431,x433,x434) % 116.74/116.91 [44]P12(x443,x442,x444)+~E(x441,x442)+~P12(x443,x441,x444) % 116.74/116.91 [45]P12(x453,x454,x452)+~E(x451,x452)+~P12(x453,x454,x451) % 116.74/116.91 [46]P13(x462,x463)+~E(x461,x462)+~P13(x461,x463) % 116.74/116.91 [47]P13(x473,x472)+~E(x471,x472)+~P13(x473,x471) % 116.74/116.91 [48]P11(x482,x483,x484)+~E(x481,x482)+~P11(x481,x483,x484) % 116.74/116.91 [49]P11(x493,x492,x494)+~E(x491,x492)+~P11(x493,x491,x494) % 116.74/116.91 [50]P11(x503,x504,x502)+~E(x501,x502)+~P11(x503,x504,x501) % 116.74/116.91 [51]~P2(x511)+P2(x512)+~E(x511,x512) % 116.74/116.91 [52]P6(x522,x523)+~E(x521,x522)+~P6(x521,x523) % 116.74/116.91 [53]P6(x533,x532)+~E(x531,x532)+~P6(x533,x531) % 116.74/116.91 [54]P9(x542,x543)+~E(x541,x542)+~P9(x541,x543) % 116.74/116.91 [55]P9(x553,x552)+~E(x551,x552)+~P9(x553,x551) % 116.74/116.91 [56]~P3(x561)+P3(x562)+~E(x561,x562) % 116.74/116.91 [57]~P7(x571)+P7(x572)+~E(x571,x572) % 116.74/116.91 [58]P10(x582,x583)+~E(x581,x582)+~P10(x581,x583) % 116.74/116.91 [59]P10(x593,x592)+~E(x591,x592)+~P10(x593,x591) % 116.74/116.91 [60]~P4(x601)+P4(x602)+~E(x601,x602) % 116.74/116.91 [61]P15(x612,x613)+~E(x611,x612)+~P15(x611,x613) % 116.74/116.91 [62]P15(x623,x622)+~E(x621,x622)+~P15(x623,x621) % 116.74/116.91 [63]P17(x632,x633)+~E(x631,x632)+~P17(x631,x633) % 116.74/116.91 [64]P17(x643,x642)+~E(x641,x642)+~P17(x643,x641) % 116.74/116.91 [65]P16(x652,x653)+~E(x651,x652)+~P16(x651,x653) % 116.74/116.91 [66]P16(x663,x662)+~E(x661,x662)+~P16(x663,x661) % 116.74/116.91 [67]P14(x672,x673)+~E(x671,x672)+~P14(x671,x673) % 116.74/116.91 [68]P14(x683,x682)+~E(x681,x682)+~P14(x683,x681) % 116.74/116.91 [69]P8(x692,x693)+~E(x691,x692)+~P8(x691,x693) % 116.74/116.91 [70]P8(x703,x702)+~E(x701,x702)+~P8(x703,x701) % 116.74/116.91 [71]P5(x712,x713)+~E(x711,x712)+~P5(x711,x713) % 116.74/116.91 [72]P5(x723,x722)+~E(x721,x722)+~P5(x723,x721) % 116.74/116.91 % 116.74/116.91 %------------------------------------------- % 116.74/116.91 cnf(165,plain, % 116.74/116.91 (~P3(a4)), % 116.74/116.91 inference(scs_inference,[],[78,85,96])). % 116.74/116.91 cnf(167,plain, % 116.74/116.91 (~P6(a4,a1)), % 116.74/116.91 inference(scs_inference,[],[78,73,85,96,97])). % 116.74/116.91 cnf(170,plain, % 116.74/116.91 (~P7(a4)), % 116.74/116.91 inference(scs_inference,[],[78,73,85,96,97,53,86])). % 116.74/116.91 cnf(178,plain, % 116.74/116.91 (~P11(a4,x1781,x1782)), % 116.74/116.91 inference(scs_inference,[],[78,73,85,96,97,53,86,90,116,136,137])). % 116.74/116.91 cnf(182,plain, % 116.74/116.91 (P6(x1821,a3)+~E(a4,x1821)), % 116.74/116.91 inference(scs_inference,[],[78,73,85,96,97,53,86,90,116,136,137,89,52])). % 116.74/116.91 cnf(183,plain, % 116.74/116.91 (~P12(x1831,a4,x1832)), % 116.74/116.91 inference(scs_inference,[],[78,73,85,96,97,53,86,90,116,136,137,89,52,139])). % 116.74/116.91 cnf(201,plain, % 116.74/116.91 (~P6(a4,a2)), % 116.74/116.91 inference(scs_inference,[],[165,75,97])). % 116.74/116.91 cnf(206,plain, % 116.74/116.91 (~P6(a4,a24)), % 116.74/116.91 inference(scs_inference,[],[165,76,97])). % 116.74/116.91 cnf(248,plain, % 116.74/116.91 (~P17(x2481,x2482)+P6(x2482,f13(x2482))), % 116.74/116.91 inference(scs_inference,[],[92,95])). % 116.74/116.91 cnf(249,plain, % 116.74/116.91 (~P17(x2491,x2492)+P2(f13(x2491))), % 116.74/116.91 inference(scs_inference,[],[93,87])). % 116.74/116.91 cnf(250,plain, % 116.74/116.91 (P13(a3,a3)), % 116.74/116.91 inference(scs_inference,[],[78,94,88])). % 116.74/116.91 cnf(251,plain, % 116.74/116.91 (P13(x2511,a3)+~E(a3,x2511)), % 116.74/116.91 inference(scs_inference,[],[250,46])). % 116.74/116.91 cnf(252,plain, % 116.74/116.91 (P13(a3,x2521)+~E(a3,x2521)), % 116.74/116.91 inference(scs_inference,[],[250,46,47])). % 116.74/116.91 cnf(255,plain, % 116.74/116.91 (~E(a3,a24)), % 116.74/116.91 inference(scs_inference,[],[76,85,2,42])). % 116.74/116.91 cnf(259,plain, % 116.74/116.91 (~P8(x2591,x2592)+~P14(x2592,x2591)), % 116.74/116.91 inference(scs_inference,[],[98,107])). % 116.74/116.91 cnf(263,plain, % 116.74/116.91 (P6(x2631,f13(x2631))+~P16(x2632,x2631)), % 116.74/116.91 inference(scs_inference,[],[99,248])). % 116.74/116.91 cnf(295,plain, % 116.74/116.91 (~P8(x2951,x2952)+~P12(x2952,x2951,x2953)), % 116.74/116.91 inference(scs_inference,[],[259,139])). % 116.74/116.91 cnf(310,plain, % 116.74/116.91 (~P12(x3101,x3102,a3)+P6(f5(f23(a3,x3101,x3102)),a1)), % 116.74/116.91 inference(scs_inference,[],[101,158])). % 116.74/116.91 cnf(311,plain, % 116.74/116.91 (~E(a3,a2)), % 116.74/116.91 inference(scs_inference,[],[201,78,53])). % 116.74/116.91 cnf(322,plain, % 116.74/116.91 (~E(a4,x3221)+P6(f11(x3221),a25)), % 116.74/116.91 inference(scs_inference,[],[102,182])). % 116.74/116.91 cnf(323,plain, % 116.74/116.91 (P6(f11(a4),a25)), % 116.74/116.91 inference(equality_inference,[],[322])). % 116.74/116.91 cnf(336,plain, % 116.74/116.91 (P17(f5(a4),a4)), % 116.74/116.91 inference(scs_inference,[],[78,103,99])). % 116.74/116.91 cnf(337,plain, % 116.74/116.91 (P17(x3371,a4)+~E(f5(a4),x3371)), % 116.74/116.91 inference(scs_inference,[],[336,63])). % 116.74/116.91 cnf(341,plain, % 116.74/116.91 (P17(f12(a4),a4)), % 116.74/116.91 inference(scs_inference,[],[78,104,100])). % 116.74/116.91 cnf(343,plain, % 116.74/116.91 (P17(x3431,a4)+~E(f12(a4),x3431)), % 116.74/116.91 inference(scs_inference,[],[341,64,63])). % 116.74/116.91 cnf(346,plain, % 116.74/116.91 (~P15(x3461,x3462)+P1(f14(x3461,f6(x3462,x3461)))), % 116.74/116.91 inference(scs_inference,[],[110,118])). % 116.74/116.91 cnf(347,plain, % 116.74/116.91 (~P12(x3471,f10(a3,a4),a3)), % 116.74/116.91 inference(scs_inference,[],[85,78,140,126])). % 116.74/116.91 cnf(357,plain, % 116.74/116.91 (~P12(x3571,x3572,f19(x3571,x3573))+~P9(x3571,x3573)), % 116.74/116.91 inference(scs_inference,[],[141,117])). % 116.74/116.91 cnf(358,plain, % 116.74/116.91 (~P16(x3581,x3582)+P4(x3582)), % 116.74/116.91 inference(scs_inference,[],[263,91])). % 116.74/116.91 cnf(359,plain, % 116.74/116.91 (~P16(x3591,x3592)+P2(f13(x3592))), % 116.74/116.91 inference(scs_inference,[],[358,87])). % 116.74/116.91 cnf(367,plain, % 116.74/116.91 (~P12(x3671,x3672,x3673)+~P14(x3672,x3671)), % 116.74/116.91 inference(scs_inference,[],[295,98])). % 116.74/116.91 cnf(392,plain, % 116.74/116.91 (~P12(x3921,x3922,x3923)+~P12(x3922,x3921,x3924)), % 116.74/116.91 inference(scs_inference,[],[367,139])). % 116.74/116.91 cnf(393,plain, % 116.74/116.91 (~E(x3931,x3932)+E(f13(x3932),f13(x3931))), % 116.74/116.91 inference(scs_inference,[],[4,2])). % 116.74/116.91 cnf(395,plain, % 116.74/116.91 (~E(x3951,x3952)+E(f5(f18(x3951,x3953,x3954)),f5(f18(x3952,x3953,x3954)))), % 116.74/116.91 inference(scs_inference,[],[8,5])). % 116.74/116.91 cnf(397,plain, % 116.74/116.91 (~E(x3971,x3972)+E(f11(f18(x3973,x3971,x3974)),f11(f18(x3973,x3972,x3974)))), % 116.74/116.91 inference(scs_inference,[],[9,6])). % 116.74/116.91 cnf(399,plain, % 116.74/116.91 (~E(x3991,x3992)+E(f12(f18(x3993,x3994,x3991)),f12(f18(x3993,x3994,x3992)))), % 116.74/116.91 inference(scs_inference,[],[13,7])). % 116.74/116.91 cnf(401,plain, % 116.74/116.91 (P6(a4,f15(f5(a4),a4))), % 116.74/116.91 inference(scs_inference,[],[78,113,103])). % 116.74/116.91 cnf(404,plain, % 116.74/116.91 (E(a3,f15(f5(a4),a4))), % 116.74/116.91 inference(scs_inference,[],[78,167,401,53,52,109])). % 116.74/116.91 cnf(411,plain, % 116.74/116.91 (P6(a4,f19(f12(a4),a4))), % 116.74/116.91 inference(scs_inference,[],[78,114,104])). % 116.74/116.91 cnf(414,plain, % 116.74/116.91 (E(f15(f5(a4),a4),a3)), % 116.74/116.91 inference(scs_inference,[],[404,251,252,2])). % 116.74/116.91 cnf(415,plain, % 116.74/116.91 (~P1(f15(f5(a4),a4))), % 116.74/116.91 inference(scs_inference,[],[404,85,251,252,2,42])). % 116.74/116.91 cnf(435,plain, % 116.74/116.91 (~P4(a3)+P4(f15(f5(a4),a4))), % 116.74/116.91 inference(scs_inference,[],[404,206,401,53,60])). % 116.74/116.91 cnf(436,plain, % 116.74/116.91 (~P6(a3,x4361)+P4(f15(f5(a4),a4))), % 116.74/116.91 inference(scs_inference,[],[404,206,401,53,60,91])). % 116.74/116.91 cnf(452,plain, % 116.74/116.91 (P4(f15(f5(a4),a4))+~E(f5(a4),a3)), % 116.74/116.91 inference(scs_inference,[],[404,206,401,53,60,91,358,92,93,99,100,115,118,337])). % 116.74/116.91 cnf(453,plain, % 116.74/116.91 (P4(f15(f5(a4),a4))+~E(f12(a4),a3)), % 116.74/116.91 inference(scs_inference,[],[404,206,401,53,60,91,358,92,93,99,100,115,118,337,343])). % 116.74/116.91 cnf(454,plain, % 116.74/116.91 (~E(f5(a4),f15(f5(a4),a4))+P4(f15(f5(a4),a4))), % 116.74/116.91 inference(scs_inference,[],[404,206,414,401,53,60,91,358,92,93,99,100,115,118,337,343,3])). % 116.74/116.91 cnf(461,plain, % 116.74/116.91 (P4(a3)+~E(f12(a4),a3)), % 116.74/116.91 inference(scs_inference,[],[201,414,411,53,60,452,453])). % 116.74/116.91 cnf(466,plain, % 116.74/116.91 (~P9(x4661,f15(f5(a4),a4))+P4(a3)), % 116.74/116.91 inference(scs_inference,[],[201,414,411,53,60,452,453,358,92,100])). % 116.74/116.91 cnf(470,plain, % 116.74/116.91 (P4(a3)+~E(f5(a4),f15(f5(a4),a4))), % 116.74/116.91 inference(scs_inference,[],[201,414,411,53,60,452,453,358,92,100,93,337])). % 116.74/116.91 cnf(494,plain, % 116.74/116.91 (~E(a4,a3)+P4(f15(f5(a4),a4))), % 116.74/116.91 inference(scs_inference,[],[411,52,436])). % 116.74/116.91 cnf(545,plain, % 116.74/116.91 (~E(a3,f12(a4))+P4(a3)), % 116.74/116.91 inference(scs_inference,[],[461,2])). % 116.74/116.91 cnf(547,plain, % 116.74/116.91 (~P6(a4,f12(a4))+P4(a3)), % 116.74/116.91 inference(scs_inference,[],[78,545,109])). % 116.74/116.91 cnf(556,plain, % 116.74/116.91 (P6(a3,f13(a3))+~P6(a4,f12(a4))), % 116.74/116.91 inference(scs_inference,[],[547,95])). % 116.74/116.91 cnf(567,plain, % 116.74/116.91 (~P6(f11(a4),a2)), % 116.74/116.91 inference(scs_inference,[],[81,323,109])). % 116.74/116.91 cnf(571,plain, % 116.74/116.91 (~P6(f11(a4),a24)), % 116.74/116.91 inference(scs_inference,[],[83,323,109])). % 116.74/116.91 cnf(575,plain, % 116.74/116.91 (~P15(x5751,x5752)+P13(f6(x5752,x5751),f14(x5751,f6(x5752,x5751)))), % 116.74/116.91 inference(scs_inference,[],[119,118])). % 116.74/116.91 cnf(576,plain, % 116.74/116.91 (P13(f6(a3,f10(a3,a4)),a3)), % 116.74/116.91 inference(scs_inference,[],[85,78,120,126])). % 116.74/116.91 cnf(605,plain, % 116.74/116.91 (~P11(x6051,x6052,x6053)+~P12(x6052,x6051,x6054)), % 116.74/116.91 inference(scs_inference,[],[392,150])). % 116.74/116.91 cnf(653,plain, % 116.74/116.91 (~P9(x6531,f15(f5(a4),a4))+P4(f15(f5(a4),a4))), % 116.74/116.91 inference(scs_inference,[],[466,435])). % 116.74/116.91 cnf(661,plain, % 116.74/116.91 (~E(a3,a4)+P4(f15(f5(a4),a4))), % 116.74/116.91 inference(scs_inference,[],[494,2])). % 116.74/116.91 cnf(667,plain, % 116.74/116.91 (P4(f15(f5(a4),a4))+~P6(a4,f12(a4))), % 116.74/116.91 inference(scs_inference,[],[556,436])). % 116.74/116.91 cnf(672,plain, % 116.74/116.91 (~P12(f11(a4),f5(a4),x6721)), % 116.74/116.91 inference(scs_inference,[],[78,605,134])). % 116.74/116.91 cnf(673,plain, % 116.74/116.91 (~P11(f11(a4),f5(a4),x6731)), % 116.74/116.91 inference(scs_inference,[],[672,150])). % 116.74/116.91 cnf(695,plain, % 116.74/116.91 (~E(f15(f5(a4),a4),a4)+P4(f15(f5(a4),a4))), % 116.74/116.91 inference(scs_inference,[],[404,661,3])). % 116.74/116.91 cnf(700,plain, % 116.74/116.91 (~P12(x7001,x7002,a3)+P11(f11(f23(a3,x7001,x7002)),f12(f23(a3,x7001,x7002)),a3)), % 116.74/116.91 inference(scs_inference,[],[135,158])). % 116.74/116.91 cnf(701,plain, % 116.74/116.91 (~E(f14(x7011,f6(x7012,x7011)),a3)+~P15(x7011,x7012)), % 116.74/116.91 inference(scs_inference,[],[85,346,42])). % 116.74/116.91 cnf(702,plain, % 116.74/116.91 (~P12(f12(a4),x7021,f19(f12(a4),a4))), % 116.74/116.91 inference(scs_inference,[],[78,357,104])). % 116.74/116.91 cnf(705,plain, % 116.74/116.91 (~P6(a4,f5(a4))+P4(a3)), % 116.74/116.91 inference(scs_inference,[],[401,470,109])). % 116.74/116.91 cnf(706,plain, % 116.74/116.91 (P4(f15(f5(a4),a4))+~P6(a4,f5(a4))), % 116.74/116.91 inference(scs_inference,[],[705,435])). % 116.74/116.91 cnf(755,plain, % 116.74/116.91 (~E(a3,f5(a4))+P4(f15(f5(a4),a4))), % 116.74/116.91 inference(scs_inference,[],[78,706,53])). % 116.74/116.91 cnf(784,plain, % 116.74/116.91 (E(f14(f13(a3),x7841),f14(f13(f15(f5(a4),a4)),x7841))), % 116.74/116.91 inference(scs_inference,[],[404,14,4])). % 116.74/116.91 cnf(785,plain, % 116.74/116.91 (E(f14(x7851,f18(a3,x7852,x7853)),f14(x7851,f18(f15(f5(a4),a4),x7852,x7853)))), % 116.74/116.91 inference(scs_inference,[],[404,15,5])). % 116.74/116.91 cnf(803,plain, % 116.74/116.91 (~P11(x8031,x8032,x8033)+P17(x8032,f23(x8033,x8031,x8032))), % 116.74/116.91 inference(scs_inference,[],[154,150])). % 116.74/116.91 cnf(804,plain, % 116.74/116.91 (~P11(x8041,x8042,x8043)+P17(x8041,f23(x8043,x8041,x8042))), % 116.74/116.91 inference(scs_inference,[],[155,150])). % 116.74/116.91 cnf(805,plain, % 116.74/116.91 (~P11(x8051,x8052,x8053)+P5(x8052,f9(x8053,x8051,x8052))), % 116.74/116.91 inference(scs_inference,[],[157,150])). % 116.74/116.91 cnf(806,plain, % 116.74/116.91 (~P11(x8061,x8062,x8063)+P13(f8(x8063,x8061,x8062),x8063)), % 116.74/116.91 inference(scs_inference,[],[159,150])). % 116.74/116.91 cnf(807,plain, % 116.74/116.91 (~P11(x8071,x8072,x8073)+P13(f9(x8073,x8071,x8072),x8073)), % 116.74/116.91 inference(scs_inference,[],[160,150])). % 116.74/116.91 cnf(816,plain, % 116.74/116.91 (~E(f14(f10(a3,a4),f6(a3,f10(a3,a4))),a3)), % 116.74/116.91 inference(scs_inference,[],[85,78,701,126])). % 116.74/116.91 cnf(825,plain, % 116.74/116.92 (~P11(x8251,x8252,x8253)+P4(f23(x8253,x8251,x8252))), % 116.74/116.92 inference(scs_inference,[],[803,92])). % 116.74/116.92 cnf(826,plain, % 116.74/116.92 (~P11(x8261,x8262,x8263)+P2(f13(f23(x8263,x8261,x8262)))), % 116.74/116.92 inference(scs_inference,[],[825,87])). % 116.74/116.92 cnf(827,plain, % 116.74/116.92 (~P11(x8271,x8272,x8273)+P4(x8271)), % 116.74/116.92 inference(scs_inference,[],[804,93])). % 116.74/116.92 cnf(828,plain, % 116.74/116.92 (~P11(x8281,x8282,x8283)+P6(x8281,f13(x8281))), % 116.74/116.92 inference(scs_inference,[],[827,95])). % 116.74/116.92 cnf(829,plain, % 116.74/116.92 (~P11(x8291,x8292,x8293)+P2(f13(x8291))), % 116.74/116.92 inference(scs_inference,[],[828,94])). % 116.74/116.92 cnf(830,plain, % 116.74/116.92 (P13(f13(x8301),f13(x8301))+~P11(x8301,x8302,x8303)), % 116.74/116.92 inference(scs_inference,[],[829,88])). % 116.74/116.92 cnf(833,plain, % 116.74/116.92 (~P11(x8331,x8332,x8333)+P1(f14(x8332,f9(x8333,x8331,x8332)))), % 116.74/116.92 inference(scs_inference,[],[805,110])). % 116.74/116.92 cnf(849,plain, % 116.74/116.92 (~P11(x8491,x8492,a3)+P6(f5(f23(a3,x8491,x8492)),a1)), % 116.74/116.92 inference(scs_inference,[],[310,150])). % 116.74/116.92 cnf(869,plain, % 116.74/116.92 (~E(a4,f15(f5(a4),a4))+P4(f15(f5(a4),a4))), % 116.74/116.92 inference(scs_inference,[],[695,2])). % 116.74/116.92 cnf(882,plain, % 116.74/116.92 (~E(f14(x8821,f9(x8822,x8823,x8821)),a3)+~P11(x8823,x8821,x8822)), % 116.74/116.92 inference(scs_inference,[],[85,833,42])). % 116.74/116.92 cnf(883,plain, % 116.74/116.92 (P6(f5(f23(a3,f5(a4),f11(a4))),a1)), % 116.74/116.92 inference(scs_inference,[],[78,849,134])). % 116.74/116.92 cnf(884,plain, % 116.74/116.92 (~P6(a4,a4)+P4(f15(f5(a4),a4))), % 116.74/116.92 inference(scs_inference,[],[401,869,109])). % 116.74/116.92 cnf(887,plain, % 116.74/116.92 (~P15(x8871,x8872)+P13(x8873,f14(x8871,f6(x8872,x8871)))+~E(f6(x8872,x8871),x8873)), % 116.74/116.92 inference(scs_inference,[],[575,46])). % 116.74/116.92 cnf(934,plain, % 116.74/116.92 (P15(f10(a3,a4),f15(f5(a4),a4))), % 116.74/116.92 inference(scs_inference,[],[404,85,78,62,126])). % 116.74/116.92 cnf(937,plain, % 116.74/116.92 (~P11(x9371,f10(a3,a4),f15(f5(a4),a4))), % 116.74/116.92 inference(scs_inference,[],[934,140,150])). % 116.74/116.92 cnf(939,plain, % 116.74/116.92 (P15(f10(a3,a4),a3)), % 116.74/116.92 inference(scs_inference,[],[414,934,140,150,62])). % 116.74/116.92 cnf(965,plain, % 116.74/116.92 (P5(f10(a3,a4),x9651)+~E(f6(a3,f10(a3,a4)),x9651)), % 116.74/116.92 inference(scs_inference,[],[939,72,118])). % 116.74/116.92 cnf(966,plain, % 116.74/116.92 (P5(f10(a3,a4),f6(a3,f10(a3,a4)))), % 116.74/116.92 inference(equality_inference,[],[965])). % 116.74/116.92 cnf(967,plain, % 116.74/116.92 (P5(x9671,f6(a3,f10(a3,a4)))+~E(f10(a3,a4),x9671)), % 116.74/116.92 inference(scs_inference,[],[966,71])). % 116.74/116.92 cnf(975,plain, % 116.74/116.92 (P6(f12(a4),a2)+P6(f12(a4),a24)), % 116.74/116.92 inference(scs_inference,[],[78,108,104])). % 116.74/116.92 cnf(976,plain, % 116.74/116.92 (~P6(f12(a4),a3)+P6(f12(a4),a24)), % 116.74/116.92 inference(scs_inference,[],[311,975,109])). % 116.74/116.92 cnf(977,plain, % 116.74/116.92 (~E(a4,f12(a4))+P6(f12(a4),a24)), % 116.74/116.92 inference(scs_inference,[],[976,182])). % 116.74/116.92 cnf(978,plain, % 116.74/116.92 (~E(f12(a4),a4)+P6(f12(a4),a24)), % 116.74/116.92 inference(scs_inference,[],[977,2])). % 116.74/116.92 cnf(979,plain, % 116.74/116.92 (~E(x9791,a4)+~E(f12(a4),x9791)+P6(f12(a4),a24)), % 116.74/116.92 inference(scs_inference,[],[978,3])). % 116.74/116.92 cnf(980,plain, % 116.74/116.92 (~P8(x9801,x9802)+~P14(x9802,x9803)+P8(x9801,x9803)), % 116.74/116.92 inference(scs_inference,[],[112,98])). % 116.74/116.92 cnf(981,plain, % 116.74/116.92 (~P8(x9811,x9812)+~P8(x9812,x9813)+~P14(x9813,x9811)), % 116.74/116.92 inference(scs_inference,[],[980,107])). % 116.74/116.92 cnf(982,plain, % 116.74/116.92 (~P8(x9821,x9822)+~P12(x9823,x9821,x9824)+~P8(x9822,x9823)), % 116.74/116.92 inference(scs_inference,[],[981,139])). % 116.74/116.92 cnf(991,plain, % 116.74/116.92 (P17(f10(a3,a4),a4)), % 116.74/116.92 inference(scs_inference,[],[78,404,415,127,42])). % 116.74/116.92 cnf(998,plain, % 116.74/116.92 (~P12(x9981,f5(a4),a3)), % 116.74/116.92 inference(scs_inference,[],[78,146,103])). % 116.74/116.92 cnf(999,plain, % 116.74/116.92 (~P11(x9991,f5(a4),a3)), % 116.74/116.92 inference(scs_inference,[],[998,150])). % 116.74/116.92 cnf(1035,plain, % 116.74/116.92 (~P8(x10351,x10352)+~P14(x10352,x10353)+~P12(x10353,x10351,x10354)), % 116.74/116.92 inference(scs_inference,[],[982,98])). % 116.74/116.92 cnf(1039,plain, % 116.74/116.92 (P11(f5(a4),f11(a4),f15(f5(a4),a4))), % 116.74/116.92 inference(scs_inference,[],[404,78,50,134])). % 116.74/116.92 cnf(1040,plain, % 116.74/116.92 (~E(f5(a4),a4)), % 116.74/116.92 inference(scs_inference,[],[178,1039,48])). % 116.74/116.92 cnf(1044,plain, % 116.74/116.92 (P11(f5(a4),f11(a4),a3)), % 116.74/116.92 inference(scs_inference,[],[414,937,178,1039,48,49,50])). % 116.74/116.92 cnf(1095,plain, % 116.74/116.92 (~E(a4,x10951)+P6(f12(a4),a24)+~E(f12(x10951),a4)), % 116.74/116.92 inference(scs_inference,[],[979,13])). % 116.74/116.92 cnf(1097,plain, % 116.74/116.92 (P3(f12(a4))+~E(f12(x10971),a4)+~E(a4,x10971)), % 116.74/116.92 inference(scs_inference,[],[76,1095,97])). % 116.74/116.92 cnf(1098,plain, % 116.74/116.92 (~E(f12(a4),a4)+~E(a4,x10981)+~E(f12(x10981),a4)), % 116.74/116.92 inference(scs_inference,[],[165,1097,56])). % 116.74/116.92 cnf(1099,plain, % 116.74/116.92 (~E(a4,f12(a4))), % 116.74/116.92 inference(scs_inference,[],[1098,2])). % 116.74/116.92 cnf(1104,plain, % 116.74/116.92 (~P12(f10(a3,a4),x11041,a3)+P12(f10(a3,a4),f20(f10(a3,a4),a3),a3)), % 116.74/116.92 inference(scs_inference,[],[939,144,141])). % 116.74/116.92 cnf(1105,plain, % 116.74/116.92 (~P11(f10(a3,a4),x11051,a3)+P12(f10(a3,a4),f20(f10(a3,a4),a3),a3)), % 116.74/116.92 inference(scs_inference,[],[1104,150])). % 116.74/116.92 cnf(1106,plain, % 116.74/116.92 (~P11(f10(a3,a4),x11061,f15(f5(a4),a4))+P12(f10(a3,a4),f20(f10(a3,a4),a3),a3)), % 116.74/116.92 inference(scs_inference,[],[414,1105,50])). % 116.74/116.92 cnf(1107,plain, % 116.74/116.92 (~E(f5(a4),f10(a3,a4))+P12(f10(a3,a4),f20(f10(a3,a4),a3),a3)), % 116.74/116.92 inference(scs_inference,[],[1039,1106,48])). % 116.74/116.92 cnf(1108,plain, % 116.74/116.92 (~E(f10(a3,a4),f5(a4))+P12(f10(a3,a4),f20(f10(a3,a4),a3),a3)), % 116.74/116.92 inference(scs_inference,[],[1107,2])). % 116.74/116.92 cnf(1121,plain, % 116.74/116.92 (~P12(f11(a4),f11(a4),a3)), % 116.74/116.92 inference(scs_inference,[],[1044,162,150])). % 116.74/116.92 cnf(1192,plain, % 116.74/116.92 (~P1(f19(f12(a4),a4))), % 116.74/116.92 inference(scs_inference,[],[411,165,97])). % 116.74/116.92 cnf(1220,plain, % 116.74/116.92 (~E(x12201,a4)+~P7(x12201)), % 116.74/116.92 inference(scs_inference,[],[165,86,57])). % 116.74/116.92 cnf(1319,plain, % 116.74/116.92 (P3(f10(a3,a4))), % 116.74/116.92 inference(scs_inference,[],[934,90,86])). % 116.74/116.92 cnf(1322,plain, % 116.74/116.92 (P7(f10(f19(f12(a4),a4),a4))), % 116.74/116.92 inference(scs_inference,[],[1192,411,90,126])). % 116.74/116.92 cnf(1323,plain, % 116.74/116.92 (~P6(f10(a3,a4),a3)), % 116.74/116.92 inference(scs_inference,[],[85,1319,96])). % 116.74/116.92 cnf(1326,plain, % 116.74/116.92 (P15(f10(a3,a4),f6(a3,f10(a3,a4)))), % 116.74/116.92 inference(scs_inference,[],[939,966,90,106])). % 116.74/116.92 cnf(1327,plain, % 116.74/116.92 (~P12(x13271,f10(a3,a4),f6(a3,f10(a3,a4)))), % 116.74/116.92 inference(scs_inference,[],[1326,140])). % 116.74/116.92 cnf(1329,plain, % 116.74/116.92 (~P11(x13291,f10(a3,a4),f6(a3,f10(a3,a4)))), % 116.74/116.92 inference(scs_inference,[],[1326,140,150])). % 116.74/116.92 cnf(1331,plain, % 116.74/116.92 (~P6(f10(a3,a4),f15(f5(a4),a4))), % 116.74/116.92 inference(scs_inference,[],[415,1319,1326,140,150,96])). % 116.74/116.92 cnf(1335,plain, % 116.74/116.92 (P6(a4,f13(a4))), % 116.74/116.92 inference(scs_inference,[],[78,91,95])). % 116.74/116.92 cnf(1338,plain, % 116.74/116.92 (E(a3,f13(a4))), % 116.74/116.92 inference(scs_inference,[],[78,167,1335,53,52,109])). % 116.74/116.92 cnf(1345,plain, % 116.74/116.92 (E(f13(a4),a3)), % 116.74/116.92 inference(scs_inference,[],[1338,252,2])). % 116.74/116.92 cnf(1347,plain, % 116.74/116.92 (~P1(f13(a4))), % 116.74/116.92 inference(scs_inference,[],[1338,85,252,2,251,42])). % 116.74/116.92 cnf(1348,plain, % 116.74/116.92 (E(f15(f5(a4),a4),f13(a4))), % 116.74/116.92 inference(scs_inference,[],[1338,414,85,252,2,251,42,3])). % 116.74/116.92 cnf(1364,plain, % 116.74/116.92 (E(f13(a4),f15(f5(a4),a4))), % 116.74/116.92 inference(scs_inference,[],[1348,2])). % 116.74/116.92 cnf(1448,plain, % 116.74/116.92 (P4(f13(a4))+~P9(x14481,f15(f5(a4),a4))), % 116.74/116.92 inference(scs_inference,[],[1348,60,494,667,706,755,884,454,653])). % 116.74/116.92 cnf(1504,plain, % 116.74/116.92 (P11(f5(a4),f11(a4),f13(a4))), % 116.74/116.92 inference(scs_inference,[],[1338,1044,50])). % 116.74/116.92 cnf(1505,plain, % 116.74/116.92 (P15(f10(a3,a4),f13(a4))), % 116.74/116.92 inference(scs_inference,[],[1338,1044,939,50,62])). % 116.74/116.92 cnf(1507,plain, % 116.74/116.92 (~P12(x15071,f10(a3,a4),f13(a4))), % 116.74/116.92 inference(scs_inference,[],[1338,576,1044,939,50,62,47,140])). % 116.74/116.92 cnf(1626,plain, % 116.74/116.92 (~P9(x16261,a3)+P4(f13(a4))), % 116.74/116.92 inference(scs_inference,[],[404,1448,55])). % 116.74/116.92 cnf(1627,plain, % 116.74/116.92 (P6(f13(a4),f13(f13(a4)))+~P9(x16271,a3)), % 116.74/116.92 inference(scs_inference,[],[1626,95])). % 116.74/116.92 cnf(1661,plain, % 116.74/116.92 (P2(f13(f13(a4)))+~P9(x16611,a3)), % 116.74/116.92 inference(scs_inference,[],[1627,94])). % 116.74/116.92 cnf(1662,plain, % 116.74/116.92 (~E(f13(f13(a4)),x16621)+P2(x16621)+~P9(x16622,a3)), % 116.74/116.92 inference(scs_inference,[],[1661,51])). % 116.74/116.92 cnf(1933,plain, % 116.74/116.92 (P4(f23(a3,f5(a4),f11(a4)))), % 116.74/116.92 inference(scs_inference,[],[1044,92,803])). % 116.74/116.92 cnf(1936,plain, % 116.74/116.92 (P4(f10(f19(f12(a4),a4),a4))), % 116.74/116.92 inference(scs_inference,[],[1192,411,93,127])). % 116.74/116.92 cnf(1937,plain, % 116.74/116.92 (P6(f10(a3,a4),f13(f10(a3,a4)))), % 116.74/116.92 inference(scs_inference,[],[991,93,95])). % 116.74/116.92 cnf(1939,plain, % 116.74/116.92 (P6(x19391,f13(f10(a3,a4)))+~E(f10(a3,a4),x19391)), % 116.74/116.92 inference(scs_inference,[],[1323,1937,53,52])). % 116.74/116.92 cnf(2107,plain, % 116.74/116.92 (P2(a1)), % 116.74/116.92 inference(scs_inference,[],[78,94,101])). % 116.74/116.92 cnf(2109,plain, % 116.74/116.92 (P2(f14(f10(a3,a4),f6(a3,f10(a3,a4))))), % 116.74/116.92 inference(scs_inference,[],[966,94,115])). % 116.74/116.92 cnf(2117,plain, % 116.74/116.92 (P13(a25,a25)), % 116.74/116.92 inference(scs_inference,[],[323,94,88])). % 116.74/116.92 cnf(2318,plain, % 116.74/116.92 (~P7(x23181)+~E(a4,x23181)), % 116.74/116.92 inference(scs_inference,[],[1220,2])). % 116.74/116.92 cnf(3612,plain, % 116.74/116.92 (P13(a1,a1)), % 116.74/116.92 inference(scs_inference,[],[2107,88])). % 116.74/116.92 cnf(3616,plain, % 116.74/116.92 (P9(f12(a4),a4)), % 116.74/116.92 inference(scs_inference,[],[2107,78,88,103,104])). % 116.74/116.92 cnf(3618,plain, % 116.74/116.92 (P6(f5(a4),a1)), % 116.74/116.92 inference(scs_inference,[],[2107,78,88,103,104,101])). % 116.74/116.92 cnf(3620,plain, % 116.74/116.92 (P11(f11(a4),f12(a4),a3)), % 116.74/116.92 inference(scs_inference,[],[2107,78,88,103,104,101,135])). % 116.74/116.92 cnf(3626,plain, % 116.74/116.92 (P3(f5(a4))), % 116.74/116.92 inference(scs_inference,[],[2107,1504,78,88,103,104,101,135,150,136,137])). % 116.74/116.92 cnf(3631,plain, % 116.74/116.92 (P4(f12(a4))), % 116.74/116.92 inference(scs_inference,[],[2107,1504,1099,1505,341,78,88,103,104,101,135,150,136,137,90,2,93])). % 116.74/116.92 cnf(3633,plain, % 116.74/116.92 (~P9(f5(a4),a4)), % 116.74/116.92 inference(scs_inference,[],[2107,1504,1099,1505,341,1335,78,88,103,104,101,135,150,136,137,90,2,93,147])). % 116.74/116.92 cnf(3635,plain, % 116.74/116.92 (~P12(f11(a4),f11(a4),f13(a4))), % 116.74/116.92 inference(scs_inference,[],[2107,1504,1099,1121,1505,341,1335,1345,78,88,103,104,101,135,150,136,137,90,2,93,147,45])). % 116.74/116.92 cnf(3640,plain, % 116.74/116.92 (~P6(f5(a4),a2)), % 116.74/116.92 inference(scs_inference,[],[2107,1504,1099,1121,571,567,80,1505,341,1335,1345,78,88,103,104,101,135,150,136,137,90,2,93,147,45,108,162,109])). % 116.74/116.92 cnf(3642,plain, % 116.74/116.92 (~E(a1,f13(a4))), % 116.74/116.92 inference(scs_inference,[],[73,2107,1347,1504,1099,1121,571,567,80,1505,341,1335,1345,78,88,103,104,101,135,150,136,137,90,2,93,147,45,108,162,109,42])). % 116.74/116.92 cnf(3643,plain, % 116.74/116.92 (P5(f5(a4),a1)), % 116.74/116.92 inference(scs_inference,[],[73,2107,1347,1504,1099,1121,571,567,80,1505,341,1335,1345,78,88,103,104,101,135,150,136,137,90,2,93,147,45,108,162,109,42,121])). % 116.74/116.92 cnf(3645,plain, % 116.74/116.92 (P16(f10(a3,a4),a4)), % 116.74/116.92 inference(scs_inference,[],[73,2107,1347,1504,1099,1121,571,567,80,1505,341,1335,1345,991,78,88,103,104,101,135,150,136,137,90,2,93,147,45,108,162,109,42,121,132])). % 116.74/116.92 cnf(3647,plain, % 116.74/116.92 (~P10(f5(a4),f13(a4))), % 116.74/116.92 inference(scs_inference,[],[73,2107,1347,1504,1099,1121,571,567,80,1505,341,1335,1345,991,78,88,103,104,101,135,150,136,137,90,2,93,147,45,108,162,109,42,121,132,141])). % 116.74/116.92 cnf(3649,plain, % 116.74/116.92 (~P8(f11(a4),f5(a4))), % 116.74/116.92 inference(scs_inference,[],[73,2107,1347,1504,1099,1121,571,567,80,1505,341,1335,1345,991,78,88,103,104,101,135,150,136,137,90,2,93,147,45,108,162,109,42,121,132,141,295])). % 116.74/116.92 cnf(3651,plain, % 116.74/116.92 (~P14(f11(a4),f5(a4))), % 116.74/116.92 inference(scs_inference,[],[73,2107,1347,1504,1099,1121,571,567,80,1505,341,1335,1345,991,78,88,103,104,101,135,150,136,137,90,2,93,147,45,108,162,109,42,121,132,141,295,367])). % 116.74/116.92 cnf(3653,plain, % 116.74/116.92 (P14(f5(a4),f11(a4))), % 116.74/116.92 inference(scs_inference,[],[73,2107,1347,1504,1099,1121,571,567,80,1505,341,1335,1345,991,78,88,103,104,101,135,150,136,137,90,2,93,147,45,108,162,109,42,121,132,141,295,367,139])). % 116.74/116.92 cnf(3655,plain, % 116.74/116.92 (~P15(f11(a4),f13(a4))), % 116.74/116.92 inference(scs_inference,[],[73,2107,1347,1504,1099,1121,571,567,80,1505,341,1335,1345,991,78,88,103,104,101,135,150,136,137,90,2,93,147,45,108,162,109,42,121,132,141,295,367,139,140])). % 116.74/116.92 cnf(3657,plain, % 116.74/116.92 (P7(f11(a4))), % 116.74/116.92 inference(scs_inference,[],[73,2107,1347,1504,1099,1121,571,567,80,1505,341,1335,1345,991,78,88,103,104,101,135,150,136,137,90,2,93,147,45,108,162,109,42,121,132,141,295,367,139,140,89])). % 116.74/116.92 cnf(3676,plain, % 116.74/116.92 (P8(f5(a4),f11(a4))), % 116.74/116.92 inference(scs_inference,[],[3653,98])). % 116.74/116.92 cnf(3678,plain, % 116.74/116.92 (P12(f11(a4),f12(a4),a3)), % 116.74/116.92 inference(scs_inference,[],[3653,3620,98,150])). % 116.74/116.92 cnf(3680,plain, % 116.74/116.92 (P3(f12(a4))), % 116.74/116.92 inference(scs_inference,[],[3653,3620,98,150,136])). % 116.74/116.92 cnf(3685,plain, % 116.74/116.92 (~P10(f5(a4),a3)), % 116.74/116.92 inference(scs_inference,[],[3647,3653,3620,1040,1338,98,150,136,2,1035,59])). % 116.74/116.92 cnf(3688,plain, % 116.74/116.92 (~P15(f11(a4),a3)), % 116.74/116.92 inference(scs_inference,[],[3655,3647,3653,3620,1040,1338,78,98,150,136,2,1035,59,146,62])). % 116.74/116.92 cnf(3689,plain, % 116.74/116.92 (~P12(x36891,f5(a4),f13(a4))), % 116.74/116.92 inference(scs_inference,[],[3655,3647,3653,3620,1040,998,1338,1345,78,98,150,136,2,1035,59,146,62,45])). % 116.74/116.92 cnf(3690,plain, % 116.74/116.92 (~P6(f5(a4),f13(a4))), % 116.74/116.92 inference(scs_inference,[],[3655,3647,3653,3620,3618,3642,1040,998,1338,1345,78,98,150,136,2,1035,59,146,62,45,109])). % 116.74/116.92 cnf(3695,plain, % 116.74/116.92 (E(f10(a3,a4),f5(a4))), % 116.74/116.92 inference(scs_inference,[],[3655,3647,3626,3653,3620,3618,3642,1040,1347,2117,74,75,998,336,1338,347,1345,323,991,1319,78,98,150,136,2,1035,59,146,62,45,109,42,121,153])). % 116.74/116.92 cnf(3703,plain, % 116.74/116.92 (~P10(f11(a4),a3)), % 116.74/116.92 inference(scs_inference,[],[3655,3647,3626,3653,3620,3618,3642,1040,1347,2117,74,75,998,336,1338,347,1345,323,991,1319,78,98,150,136,2,1035,59,146,62,45,109,42,121,153,392,605,141])). % 116.74/116.92 cnf(3709,plain, % 116.74/116.92 (P14(f11(a4),f12(a4))), % 116.74/116.92 inference(scs_inference,[],[3655,3647,3626,3653,3620,3618,3642,1040,1347,2117,74,75,998,336,1338,347,1345,323,991,1319,78,98,150,136,2,1035,59,146,62,45,109,42,121,153,392,605,141,295,367,139])). % 116.74/116.92 cnf(3713,plain, % 116.74/116.92 (P7(f12(a4))), % 116.74/116.92 inference(scs_inference,[],[3655,3647,3626,3653,3620,3618,3642,1040,1347,2117,74,75,998,336,1338,347,1345,323,991,1319,78,98,150,136,2,1035,59,146,62,45,109,42,121,153,392,605,141,295,367,139,140,89])). % 116.74/116.92 cnf(3719,plain, % 116.74/116.92 (~E(f5(a4),f12(a4))), % 116.74/116.92 inference(scs_inference,[],[3655,3647,3651,3626,3653,3620,3618,3642,1040,1347,672,2117,74,75,998,336,1338,347,1345,323,991,1319,78,98,150,136,2,1035,59,146,62,45,109,42,121,153,392,605,141,295,367,139,140,89,54,58,68,44,67])). % 116.74/116.92 cnf(3720,plain, % 116.74/116.92 (~P8(f11(a4),f10(a3,a4))), % 116.74/116.92 inference(scs_inference,[],[3655,3649,3647,3651,3626,3653,3620,3618,3642,1040,1347,672,2117,74,75,998,336,1338,347,1345,323,991,1319,78,98,150,136,2,1035,59,146,62,45,109,42,121,153,392,605,141,295,367,139,140,89,54,58,68,44,67,70])). % 116.74/116.92 cnf(3726,plain, % 116.74/116.92 (~P6(f10(a3,a4),a2)), % 116.74/116.92 inference(scs_inference,[],[3655,3649,3647,3651,3626,3653,3620,3618,3640,3642,673,1040,1347,672,2117,74,75,998,336,1338,347,1345,323,991,1319,78,98,150,136,2,1035,59,146,62,45,109,42,121,153,392,605,141,295,367,139,140,89,54,58,68,44,67,70,980,105,49,52])). % 116.74/116.92 cnf(3727,plain, % 116.74/116.92 (P15(f5(a4),f13(a4))), % 116.74/116.92 inference(scs_inference,[],[3655,3649,3647,3651,3626,3653,3620,3618,3640,3642,673,1040,1347,672,2117,74,75,998,1505,336,1338,347,1345,323,991,1319,78,98,150,136,2,1035,59,146,62,45,109,42,121,153,392,605,141,295,367,139,140,89,54,58,68,44,67,70,980,105,49,52,61])). % 116.74/116.92 cnf(3730,plain, % 116.74/116.92 (~P15(f12(a4),f13(a4))), % 116.74/116.92 inference(scs_inference,[],[3655,3649,3647,3651,3626,3653,3657,3620,3618,3640,3642,673,1040,1347,672,2117,74,75,998,1505,341,336,1335,1338,347,1345,323,991,1319,78,98,150,136,2,1035,59,146,62,45,109,42,121,153,392,605,141,295,367,139,140,89,54,58,68,44,67,70,980,105,49,52,61,106,132])). % 116.74/116.92 cnf(3732,plain, % 116.74/116.92 (~P14(f12(a4),f5(a4))), % 116.74/116.92 inference(scs_inference,[],[3655,3649,3647,3651,3626,3653,3657,3620,3618,3640,3642,673,1040,1347,672,2117,74,75,998,1505,341,336,1335,1338,347,1345,323,991,1319,78,98,150,136,2,1035,59,146,62,45,109,42,121,153,392,605,141,295,367,139,140,89,54,58,68,44,67,70,980,105,49,52,61,106,132,259])). % 116.74/116.92 cnf(3741,plain, % 116.74/116.92 (P12(f10(a3,a4),f20(f10(a3,a4),a3),a3)), % 116.74/116.92 inference(scs_inference,[],[3695,1108])). % 116.74/116.92 cnf(3744,plain, % 116.74/116.92 (P12(f5(a4),f11(a4),a3)), % 116.74/116.92 inference(scs_inference,[],[3709,1044,98,150])). % 116.74/116.92 cnf(3746,plain, % 116.74/116.92 (P7(f5(a4))), % 116.74/116.92 inference(scs_inference,[],[3709,3727,1044,98,150,90])). % 116.74/116.92 cnf(3748,plain, % 116.74/116.92 (~E(f12(a4),f5(a4))), % 116.74/116.92 inference(scs_inference,[],[3709,3719,3727,1044,98,150,90,2])). % 116.74/116.92 cnf(3749,plain, % 116.74/116.92 (~P12(f12(a4),f5(a4),x37491)), % 116.74/116.92 inference(scs_inference,[],[3676,3709,3719,3727,1044,98,150,90,2,982])). % 116.74/116.92 cnf(3754,plain, % 116.74/116.92 (~P10(f10(a3,a4),a3)), % 116.74/116.92 inference(scs_inference,[],[3685,3676,3720,3695,3709,3719,3727,3732,1044,98,150,90,2,982,112,68,58])). % 116.74/116.92 cnf(3755,plain, % 116.74/116.92 (~P9(f10(a3,a4),a4)), % 116.74/116.92 inference(scs_inference,[],[3633,3685,3676,3720,3695,3709,3719,3727,3732,1044,98,150,90,2,982,112,68,58,54])). % 116.74/116.92 cnf(3756,plain, % 116.74/116.92 (~E(f12(a4),f10(a3,a4))), % 116.74/116.92 inference(scs_inference,[],[3633,3685,3676,3720,3695,3709,3719,3727,3732,1044,98,150,90,2,982,112,68,58,54,70])). % 116.74/116.92 cnf(3758,plain, % 116.74/116.92 (~E(a1,a3)), % 116.74/116.92 inference(scs_inference,[],[73,3633,3685,3676,3720,3695,3690,3709,3719,3727,3732,1044,1338,85,98,150,90,2,982,112,68,58,54,70,53,42])). % 116.74/116.92 cnf(3760,plain, % 116.74/116.92 (~P5(f12(a4),f13(a4))), % 116.74/116.92 inference(scs_inference,[],[73,3633,3685,3688,3676,3720,3695,3690,3709,3713,3719,3727,3730,3732,939,1044,1338,85,98,150,90,2,982,112,68,58,54,70,53,42,61,106])). % 116.74/116.92 cnf(3775,plain, % 116.74/116.92 (~E(f10(a3,a4),f12(a4))), % 116.74/116.92 inference(scs_inference,[],[3756,2])). % 116.74/116.92 cnf(3776,plain, % 116.74/116.92 (~P12(f12(a4),f10(a3,a4),x37761)), % 116.74/116.92 inference(scs_inference,[],[3756,3749,3695,2,44])). % 116.74/116.92 cnf(3778,plain, % 116.74/116.92 (P15(f5(a4),a1)), % 116.74/116.92 inference(scs_inference,[],[3643,3756,3749,3746,1347,3695,76,2,44,42,106])). % 116.74/116.92 cnf(3785,plain, % 116.74/116.92 (~E(f12(a4),f11(a4))), % 116.74/116.92 inference(scs_inference,[],[3678,1121,255,2,44])). % 116.74/116.92 cnf(3802,plain, % 116.74/116.92 (~E(f12(a4),x38021)+P6(x38021,f13(x38021))), % 116.74/116.92 inference(scs_inference,[],[3775,3785,3631,3776,3680,341,1335,991,1319,2,153,605,139,60,87,95])). % 116.74/116.92 cnf(3811,plain, % 116.74/116.92 (P6(f12(a4),f13(f12(a4)))), % 116.74/116.92 inference(equality_inference,[],[3802])). % 116.74/116.92 cnf(3815,plain, % 116.74/116.92 (~E(a24,a1)), % 116.74/116.92 inference(scs_inference,[],[82,2])). % 116.74/116.92 cnf(3816,plain, % 116.74/116.92 (~P11(x38161,f5(a4),f13(a4))), % 116.74/116.92 inference(scs_inference,[],[999,82,1345,2,50])). % 116.74/116.92 cnf(3892,plain, % 116.74/116.92 (~P6(f12(a4),f13(a4))), % 116.74/116.92 inference(scs_inference,[],[3680,1347,96])). % 116.74/116.92 cnf(3899,plain, % 116.74/116.92 (~P6(f12(a4),a3)), % 116.74/116.92 inference(scs_inference,[],[3892,1338,53])). % 116.74/116.92 cnf(3909,plain, % 116.74/116.92 (P12(f5(a4),f12(a4),a3)), % 116.74/116.92 inference(scs_inference,[],[3748,3626,3680,998,341,336,78,153])). % 116.74/116.92 cnf(3975,plain, % 116.74/116.92 (~P6(f10(a3,a4),a24)), % 116.74/116.92 inference(scs_inference,[],[3755,3815,3618,3695,109,55,52])). % 116.74/116.92 cnf(4014,plain, % 116.74/116.92 (~P6(f10(a3,a4),a25)), % 116.74/116.92 inference(scs_inference,[],[3618,79,3695,109,52])). % 116.74/116.92 cnf(4078,plain, % 116.74/116.92 (~P12(x40781,f13(a4),x40782)+P12(x40781,a3,x40782)), % 116.74/116.92 inference(scs_inference,[],[1345,44])). % 116.74/116.92 cnf(4110,plain, % 116.74/116.92 (E(f5(a4),f10(a3,a4))), % 116.74/116.92 inference(scs_inference,[],[3689,1507,3626,336,1335,991,1319,153])). % 116.74/116.92 cnf(4126,plain, % 116.74/116.92 (P15(f10(a3,a4),a1)), % 116.74/116.92 inference(scs_inference,[],[4110,3778,61])). % 116.74/116.92 cnf(4135,plain, % 116.74/116.92 (P5(f10(a3,a4),a1)), % 116.74/116.92 inference(scs_inference,[],[3643,4110,71])). % 116.74/116.92 cnf(4154,plain, % 116.74/116.92 (P14(f10(a3,a4),f11(a4))), % 116.74/116.92 inference(scs_inference,[],[3657,3676,4110,69,105])). % 116.74/116.92 cnf(4156,plain, % 116.74/116.92 (~P6(f10(a3,a4),x41561)+~E(x41561,a2)), % 116.74/116.92 inference(scs_inference,[],[3726,3657,3676,4110,69,105,53])). % 116.74/116.92 cnf(4160,plain, % 116.74/116.92 (~E(a2,x41601)+~P6(f10(a3,a4),x41601)), % 116.74/116.92 inference(scs_inference,[],[3726,3775,3657,3676,3680,4110,341,347,991,1319,78,69,105,53,153,2])). % 116.74/116.92 cnf(4187,plain, % 116.74/116.92 (~P6(f10(a3,a4),x41871)+~E(x41871,a25)), % 116.74/116.92 inference(scs_inference,[],[4014,53])). % 116.74/116.92 cnf(4188,plain, % 116.74/116.92 (~E(a25,x41881)+~P6(f10(a3,a4),x41881)), % 116.74/116.92 inference(scs_inference,[],[4014,53,2])). % 116.74/116.92 cnf(4277,plain, % 116.74/116.92 (~P6(f10(a3,a4),x42771)+~E(x42771,a24)), % 116.74/116.92 inference(scs_inference,[],[3975,53])). % 116.74/116.92 cnf(4278,plain, % 116.74/116.92 (~E(a24,x42781)+~P6(f10(a3,a4),x42781)), % 116.74/116.92 inference(scs_inference,[],[3975,53,2])). % 116.74/116.92 cnf(4645,plain, % 116.74/116.92 (P15(f5(a4),a3)), % 116.74/116.92 inference(scs_inference,[],[939,3695,61])). % 116.74/116.92 cnf(4868,plain, % 116.74/116.92 (~P11(x48681,f13(a4),x48682)+P12(x48681,a3,x48682)), % 116.74/116.92 inference(scs_inference,[],[4078,150])). % 116.74/116.92 cnf(4951,plain, % 116.74/116.92 (P5(f12(a4),f9(a3,f11(a4),f12(a4)))), % 116.74/116.92 inference(scs_inference,[],[4645,1364,3620,120,828,825,8,9,13,346,803,804,805])). % 116.74/116.92 cnf(5055,plain, % 116.74/116.92 (P14(f10(a3,a4),f20(f10(a3,a4),a3))), % 116.74/116.92 inference(scs_inference,[],[411,4645,1933,3741,1936,1322,4135,3909,1364,3620,3645,3695,120,828,825,8,9,13,346,803,804,805,806,807,830,826,14,15,19,20,21,22,23,24,25,26,27,28,29,30,31,32,37,38,39,40,41,701,833,5,6,7,10,11,12,16,17,18,33,34,35,575,882,310,849,395,397,399,967,700,393,4,248,1220,2318,154,155,113,156,110,87,159,157,367,158,392,103,295,119,160,95,94,36,605,139])). % 116.74/116.92 cnf(5057,plain, % 116.74/116.92 (P8(f10(a3,a4),f20(f10(a3,a4),a3))), % 116.74/116.92 inference(scs_inference,[],[411,4645,1933,3741,1936,1322,4135,3909,1364,3620,3645,3695,120,828,825,8,9,13,346,803,804,805,806,807,830,826,14,15,19,20,21,22,23,24,25,26,27,28,29,30,31,32,37,38,39,40,41,701,833,5,6,7,10,11,12,16,17,18,33,34,35,575,882,310,849,395,397,399,967,700,393,4,248,1220,2318,154,155,113,156,110,87,159,157,367,158,392,103,295,119,160,95,94,36,605,139,98])). % 116.74/116.92 cnf(5059,plain, % 116.74/116.92 (P6(f10(a3,a4),f14(f10(a3,a4),a1))), % 116.74/116.92 inference(scs_inference,[],[411,4645,1933,3741,1936,1322,4135,3909,1364,3620,3645,3695,120,828,825,8,9,13,346,803,804,805,806,807,830,826,14,15,19,20,21,22,23,24,25,26,27,28,29,30,31,32,37,38,39,40,41,701,833,5,6,7,10,11,12,16,17,18,33,34,35,575,882,310,849,395,397,399,967,700,393,4,248,1220,2318,154,155,113,156,110,87,159,157,367,158,392,103,295,119,160,95,94,36,605,139,98,115])). % 116.74/116.92 cnf(5067,plain, % 116.74/116.92 (P5(f5(a4),f6(a3,f5(a4)))), % 116.74/116.92 inference(scs_inference,[],[411,4645,1933,3741,2109,1936,1322,4135,3909,1364,3620,3645,3695,3616,120,828,825,8,9,13,346,803,804,805,806,807,830,826,14,15,19,20,21,22,23,24,25,26,27,28,29,30,31,32,37,38,39,40,41,701,833,5,6,7,10,11,12,16,17,18,33,34,35,575,882,310,849,395,397,399,967,700,393,4,248,1220,2318,154,155,113,156,110,87,159,157,367,158,392,103,295,119,160,95,94,36,605,139,98,115,99,88,117,118])). % 116.74/116.92 cnf(5100,plain, % 116.74/116.92 (P12(f5(a4),f20(f5(a4),a3),a3)), % 116.74/116.92 inference(scs_inference,[],[411,4645,1933,3741,2109,1936,1322,816,4135,3685,3727,3909,1364,3620,1039,3645,3695,3616,1192,120,828,825,8,9,13,346,803,804,805,806,807,830,826,14,15,19,20,21,22,23,24,25,26,27,28,29,30,31,32,37,38,39,40,41,701,833,5,6,7,10,11,12,16,17,18,33,34,35,575,882,310,849,395,397,399,967,700,393,4,248,1220,2318,154,155,113,156,110,87,159,157,367,158,392,103,295,119,160,95,94,36,605,139,98,115,99,88,117,118,116,140,89,150,358,827,86,2,136,137,93,91,887,122,123,162,144])). % 116.74/116.92 cnf(5115,plain, % 116.74/116.92 (P12(f11(a4),f20(f11(a4),a3),a3)), % 116.74/116.92 inference(scs_inference,[],[411,4645,1331,1933,3741,2109,1936,1322,816,4135,3754,3685,3655,3727,3909,3744,1364,3620,3703,1348,1039,3645,4110,3695,3616,1192,414,78,120,828,825,8,9,13,346,803,804,805,806,807,830,826,14,15,19,20,21,22,23,24,25,26,27,28,29,30,31,32,37,38,39,40,41,701,833,5,6,7,10,11,12,16,17,18,33,34,35,575,882,310,849,395,397,399,967,700,393,4,248,1220,2318,154,155,113,156,110,87,159,157,367,158,392,103,295,119,160,95,94,36,605,139,98,115,99,88,117,118,116,140,89,150,358,827,86,2,136,137,93,91,887,122,123,162,144,59,124,127,52,126,146,62,125,152])). % 116.74/116.92 cnf(5119,plain, % 116.74/116.92 (~P14(f20(f10(a3,a4),a3),f5(a4))), % 116.74/116.92 inference(scs_inference,[],[411,4645,1331,1933,3741,2109,1936,1322,816,4135,3754,3685,3655,3727,3635,3909,3744,1364,3620,3703,1348,1039,3645,4110,3695,3616,1192,414,78,120,828,825,8,9,13,346,803,804,805,806,807,830,826,14,15,19,20,21,22,23,24,25,26,27,28,29,30,31,32,37,38,39,40,41,701,833,5,6,7,10,11,12,16,17,18,33,34,35,575,882,310,849,395,397,399,967,700,393,4,248,1220,2318,154,155,113,156,110,87,159,157,367,158,392,103,295,119,160,95,94,36,605,139,98,115,99,88,117,118,116,140,89,150,358,827,86,2,136,137,93,91,887,122,123,162,144,59,124,127,52,126,146,62,125,152,45,65,68])). % 116.74/116.92 cnf(5176,plain, % 116.74/116.92 (~P12(f20(f11(a4),a3),f11(a4),a3)), % 116.74/116.92 inference(scs_inference,[],[411,4645,1331,1933,3741,3811,1329,2109,1936,1322,816,883,785,784,4135,3612,1327,3899,170,3754,3685,3655,3816,3727,3635,3713,3909,702,3744,1364,3620,3758,1121,3703,3760,1348,3748,1039,73,3645,3626,165,336,3680,341,4110,3695,3616,1192,414,1937,78,120,828,825,8,9,13,346,803,804,805,806,807,830,826,14,15,19,20,21,22,23,24,25,26,27,28,29,30,31,32,37,38,39,40,41,701,833,5,6,7,10,11,12,16,17,18,33,34,35,575,882,310,849,395,397,399,967,700,393,4,248,1220,2318,154,155,113,156,110,87,159,157,367,158,392,103,295,119,160,95,94,36,605,139,98,115,99,88,117,118,116,140,89,150,358,827,86,2,136,137,93,91,887,122,123,162,144,59,124,127,52,126,146,62,125,152,45,65,68,70,44,3,109,50,72,53,49,96,61,57,106,56,97,121,132,153,249,829,114,4156,4160,4187,4188,4277,4278,102,359,263,182,104,141,100,92,1662,161])). % 116.74/116.92 cnf(5178,plain, % 116.74/116.92 (~P12(f12(a4),x51781,f15(f10(a3,a4),a4))), % 116.74/116.92 inference(scs_inference,[],[411,4645,1331,1933,3741,3811,1329,2109,1936,1322,816,883,785,784,4135,3612,1327,3899,170,3754,3685,3655,3816,3727,3635,3713,3909,702,3744,1364,3620,3758,1121,3703,3760,1348,3748,1039,73,3645,3626,165,336,3680,341,4110,3695,3616,1192,414,1937,78,120,828,825,8,9,13,346,803,804,805,806,807,830,826,14,15,19,20,21,22,23,24,25,26,27,28,29,30,31,32,37,38,39,40,41,701,833,5,6,7,10,11,12,16,17,18,33,34,35,575,882,310,849,395,397,399,967,700,393,4,248,1220,2318,154,155,113,156,110,87,159,157,367,158,392,103,295,119,160,95,94,36,605,139,98,115,99,88,117,118,116,140,89,150,358,827,86,2,136,137,93,91,887,122,123,162,144,59,124,127,52,126,146,62,125,152,45,65,68,70,44,3,109,50,72,53,49,96,61,57,106,56,97,121,132,153,249,829,114,4156,4160,4187,4188,4277,4278,102,359,263,182,104,141,100,92,1662,161,147])). % 116.74/116.92 cnf(5180,plain, % 116.74/116.92 (~P8(f20(f11(a4),a3),f10(a3,a4))), % 116.74/116.92 inference(scs_inference,[],[411,4645,1331,1933,3741,3811,1329,2109,1936,1322,816,883,785,784,4135,3612,1327,3899,4154,170,3754,3685,3655,3816,3727,3635,3713,3909,702,3744,1364,3620,3758,1121,3703,3760,1348,3748,1039,73,3645,3626,165,336,3680,341,4110,3695,3616,1192,414,1937,78,120,828,825,8,9,13,346,803,804,805,806,807,830,826,14,15,19,20,21,22,23,24,25,26,27,28,29,30,31,32,37,38,39,40,41,701,833,5,6,7,10,11,12,16,17,18,33,34,35,575,882,310,849,395,397,399,967,700,393,4,248,1220,2318,154,155,113,156,110,87,159,157,367,158,392,103,295,119,160,95,94,36,605,139,98,115,99,88,117,118,116,140,89,150,358,827,86,2,136,137,93,91,887,122,123,162,144,59,124,127,52,126,146,62,125,152,45,65,68,70,44,3,109,50,72,53,49,96,61,57,106,56,97,121,132,153,249,829,114,4156,4160,4187,4188,4277,4278,102,359,263,182,104,141,100,92,1662,161,147,1035])). % 116.74/116.92 cnf(5231,plain, % 116.74/116.92 (~P12(f12(a4),x52311,a3)), % 116.74/116.92 inference(scs_inference,[],[78,183,404,3616,4110,3695,3741,3620,4645,3760,3657,3655,4126,3678,3811,3899,5059,5100,5055,5057,5176,5178,4951,5067,5180,5119,150,140,98,139,392,4277,4278,4160,4156,4188,4187,4868,1939,106,53,72,71,50,44,69,45,43,67,62,52,147])). % 116.74/116.92 cnf(5237,plain, % 116.74/116.92 (P12(f12(a4),f16(f12(a4),f12(a4)),a3)), % 116.74/116.92 inference(scs_inference,[],[78,183,404,3616,1044,4110,3695,3741,3620,4645,3760,3744,3657,3655,4126,3678,3811,3899,5059,5100,5115,5055,5057,5176,5178,4951,5067,5180,5119,150,140,98,139,392,4277,4278,4160,4156,4188,4187,4868,1939,106,53,72,71,50,44,69,45,43,67,62,52,147,161,162,151])). % 116.74/116.92 cnf(5261,plain, % 116.74/116.92 ($false), % 116.74/116.92 inference(scs_inference,[],[5237,5231]), % 116.74/116.92 ['proof']). % 116.82/116.92 % SZS output end Proof % 116.82/116.92 % Total time :116.120000s %------------------------------------------------------------------------------