%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PRO011+4 : 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 : n026.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:45 EDT 2024 % Result : Theorem 117.28s 117.41s % Output : CNFRefutation 117.28s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : PRO011+4 : 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.12/0.34 % Computer : n026.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Thu Jun 20 06:41:09 EDT 2024 % 0.12/0.34 % CPUTime : % 0.56/0.60 start to proof:theBenchmark % 117.28/117.39 %------------------------------------------- % 117.28/117.39 % File :CSE---1.7 % 117.28/117.39 % Problem :theBenchmark % 117.28/117.39 % Transform :cnf % 117.28/117.39 % Format :tptp:raw % 117.28/117.39 % Command :java -jar mcs_scs.jar %d %s % 117.28/117.39 % 117.28/117.39 % Result :Theorem 116.620000s % 117.28/117.39 % Output :CNFRefutation 116.620000s % 117.28/117.39 %------------------------------------------- % 117.28/117.40 %------------------------------------------------------------------------------ % 117.28/117.40 % File : PRO011+4 : TPTP v8.2.0. Released v4.0.0. % 117.28/117.40 % Domain : Processes % 117.28/117.40 % Problem : PSL cliff problem coe-7.1.3-subocc % 117.28/117.40 % Version : Especial : Augmented > Especial. % 117.28/117.40 % English : % 117.28/117.40 % Refs : [Hal09] Halcomb (2009), Email to G. Sutcliffe % 117.28/117.40 % Source : [Hal09] % 117.28/117.40 % Names : unique-cat-p9x__coe-7.1.3-subocc-pd [Hal09] % 117.28/117.40 % 117.28/117.40 % Status : Theorem % 117.28/117.41 % Rating : 0.17 v8.2.0, 0.14 v7.5.0, 0.16 v7.4.0, 0.13 v7.3.0, 0.14 v7.2.0, 0.10 v7.1.0, 0.13 v7.0.0, 0.07 v6.4.0, 0.08 v6.2.0, 0.16 v6.1.0, 0.17 v5.5.0, 0.19 v5.4.0, 0.18 v5.3.0, 0.19 v5.2.0, 0.05 v5.1.0, 0.14 v5.0.0, 0.12 v4.1.0, 0.13 v4.0.1, 0.17 v4.0.0 % 117.28/117.41 % Syntax : Number of formulae : 46 ( 12 unt; 0 def) % 117.28/117.41 % Number of atoms : 147 ( 12 equ) % 117.28/117.41 % Maximal formula atoms : 10 ( 3 avg) % 117.28/117.41 % Number of connectives : 121 ( 20 ~; 4 |; 60 &) % 117.28/117.41 % ( 7 <=>; 30 =>; 0 <=; 0 <~>) % 117.28/117.41 % Maximal formula depth : 13 ( 6 avg) % 117.28/117.41 % Maximal term depth : 1 ( 1 avg) % 117.28/117.41 % Number of predicates : 18 ( 17 usr; 0 prp; 1-3 aty) % 117.28/117.41 % Number of functors : 5 ( 5 usr; 5 con; 0-0 aty) % 117.28/117.41 % Number of variables : 110 ( 89 !; 21 ?) % 117.28/117.41 % SPC : FOF_THM_RFO_SEQ % 117.28/117.41 % 117.28/117.41 % Comments : % 117.28/117.41 %------------------------------------------------------------------------------ % 117.28/117.41 fof(sos,axiom, % 117.28/117.41 ! [X0,X1] : % 117.28/117.41 ( ( occurrence_of(X1,X0) % 117.28/117.41 & ~ atomic(X0) ) % 117.28/117.41 => ? [X2] : % 117.28/117.41 ( root(X2,X0) % 117.28/117.41 & subactivity_occurrence(X2,X1) ) ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_01,axiom, % 117.28/117.41 ! [X3,X4,X5,X6,X7] : % 117.28/117.41 ( ( occurrence_of(X4,X3) % 117.28/117.41 & root_occ(X6,X4) % 117.28/117.41 & leaf_occ(X7,X4) % 117.28/117.41 & subactivity_occurrence(X5,X4) % 117.28/117.41 & min_precedes(X6,X5,X3) % 117.28/117.41 & X5 != X7 ) % 117.28/117.41 => min_precedes(X5,X7,X3) ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_02,axiom, % 117.28/117.41 ! [X8,X9,X10,X11] : % 117.28/117.41 ( ( occurrence_of(X9,X8) % 117.28/117.41 & subactivity_occurrence(X10,X9) % 117.28/117.41 & leaf_occ(X11,X9) % 117.28/117.41 & arboreal(X10) % 117.28/117.41 & ~ min_precedes(X10,X11,X8) ) % 117.28/117.41 => X11 = X10 ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_03,axiom, % 117.28/117.41 ! [X12,X13] : % 117.28/117.41 ( occurrence_of(X13,X12) % 117.28/117.41 => ( activity(X12) % 117.28/117.41 & activity_occurrence(X13) ) ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_04,axiom, % 117.28/117.41 ! [X14,X15,X16,X17] : % 117.28/117.41 ( ( occurrence_of(X15,X14) % 117.28/117.41 & arboreal(X16) % 117.28/117.41 & arboreal(X17) % 117.28/117.41 & subactivity_occurrence(X16,X15) % 117.28/117.41 & subactivity_occurrence(X17,X15) ) % 117.28/117.41 => ( min_precedes(X16,X17,X14) % 117.28/117.41 | min_precedes(X17,X16,X14) % 117.28/117.41 | X16 = X17 ) ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_05,axiom, % 117.28/117.41 ! [X18,X19] : % 117.28/117.41 ( root(X19,X18) % 117.28/117.41 => ? [X20] : % 117.28/117.41 ( subactivity(X20,X18) % 117.28/117.41 & atocc(X19,X20) ) ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_06,axiom, % 117.28/117.41 ! [X21,X22,X23] : % 117.28/117.41 ( min_precedes(X22,X23,X21) % 117.28/117.41 => ? [X24] : % 117.28/117.41 ( occurrence_of(X24,X21) % 117.28/117.41 & subactivity_occurrence(X22,X24) % 117.28/117.41 & subactivity_occurrence(X23,X24) ) ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_07,axiom, % 117.28/117.41 ! [X25,X26] : % 117.28/117.41 ( ( leaf(X25,X26) % 117.28/117.41 & ~ atomic(X26) ) % 117.28/117.41 => ? [X27] : % 117.28/117.41 ( occurrence_of(X27,X26) % 117.28/117.41 & leaf_occ(X25,X27) ) ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_08,axiom, % 117.28/117.41 ! [X28,X29,X30] : % 117.28/117.41 ( ( occurrence_of(X28,X29) % 117.28/117.41 & occurrence_of(X28,X30) ) % 117.28/117.41 => X29 = X30 ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_09,axiom, % 117.28/117.41 ! [X31,X32,X33] : % 117.28/117.41 ( ( occurrence_of(X31,X33) % 117.28/117.41 & leaf_occ(X32,X31) ) % 117.28/117.41 => ~ ? [X34] : min_precedes(X32,X34,X33) ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_10,axiom, % 117.28/117.41 ! [X35,X36,X37] : % 117.28/117.41 ( ( occurrence_of(X35,X37) % 117.28/117.41 & root_occ(X36,X35) ) % 117.28/117.41 => ~ ? [X38] : min_precedes(X38,X36,X37) ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_11,axiom, % 117.28/117.41 ! [X39,X40] : % 117.28/117.41 ( subactivity_occurrence(X39,X40) % 117.28/117.41 => ( activity_occurrence(X39) % 117.28/117.41 & activity_occurrence(X40) ) ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_12,axiom, % 117.28/117.41 ! [X41] : % 117.28/117.41 ( activity_occurrence(X41) % 117.28/117.41 => ? [X42] : % 117.28/117.41 ( activity(X42) % 117.28/117.41 & occurrence_of(X41,X42) ) ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_13,axiom, % 117.28/117.41 ! [X43] : % 117.28/117.41 ( legal(X43) % 117.28/117.41 => arboreal(X43) ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_14,axiom, % 117.28/117.41 ! [X44,X45] : % 117.28/117.41 ( atocc(X44,X45) % 117.28/117.41 <=> ? [X46] : % 117.28/117.41 ( subactivity(X45,X46) % 117.28/117.41 & atomic(X46) % 117.28/117.41 & occurrence_of(X44,X46) ) ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_15,axiom, % 117.28/117.41 ! [X47,X48] : % 117.28/117.41 ( leaf(X47,X48) % 117.28/117.41 <=> ( ( root(X47,X48) % 117.28/117.41 | ? [X49] : min_precedes(X49,X47,X48) ) % 117.28/117.41 & ~ ? [X50] : min_precedes(X47,X50,X48) ) ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_16,axiom, % 117.28/117.41 ! [X51,X52] : % 117.28/117.41 ( occurrence_of(X51,X52) % 117.28/117.41 => ( arboreal(X51) % 117.28/117.41 <=> atomic(X52) ) ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_17,axiom, % 117.28/117.41 ! [X53,X54] : % 117.28/117.41 ( root(X53,X54) % 117.28/117.41 => legal(X53) ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_18,axiom, % 117.28/117.41 ! [X55,X56] : % 117.28/117.41 ( leaf_occ(X55,X56) % 117.28/117.41 <=> ? [X57] : % 117.28/117.41 ( occurrence_of(X56,X57) % 117.28/117.41 & subactivity_occurrence(X55,X56) % 117.28/117.41 & leaf(X55,X57) ) ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_19,axiom, % 117.28/117.41 ! [X58,X59] : % 117.28/117.41 ( root_occ(X58,X59) % 117.28/117.41 <=> ? [X60] : % 117.28/117.41 ( occurrence_of(X59,X60) % 117.28/117.41 & subactivity_occurrence(X58,X59) % 117.28/117.41 & root(X58,X60) ) ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_20,axiom, % 117.28/117.41 ! [X61,X62] : % 117.28/117.41 ( earlier(X61,X62) % 117.28/117.41 => ~ earlier(X62,X61) ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_21,axiom, % 117.28/117.41 ! [X63,X64] : % 117.28/117.41 ( precedes(X63,X64) % 117.28/117.41 <=> ( earlier(X63,X64) % 117.28/117.41 & legal(X64) ) ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_22,axiom, % 117.28/117.41 ! [X65,X66,X67] : % 117.28/117.41 ( min_precedes(X65,X66,X67) % 117.28/117.41 => ~ root(X66,X67) ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_23,axiom, % 117.28/117.41 ! [X68,X69,X70] : % 117.28/117.41 ( min_precedes(X68,X69,X70) % 117.28/117.41 => ? [X71] : % 117.28/117.41 ( root(X71,X70) % 117.28/117.41 & min_precedes(X71,X69,X70) ) ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_24,axiom, % 117.28/117.41 ! [X72,X73,X74] : % 117.28/117.41 ( min_precedes(X72,X73,X74) % 117.28/117.41 => precedes(X72,X73) ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_25,axiom, % 117.28/117.41 ! [X75,X76,X77] : % 117.28/117.41 ( next_subocc(X75,X76,X77) % 117.28/117.41 => ( arboreal(X75) % 117.28/117.41 & arboreal(X76) ) ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_26,axiom, % 117.28/117.41 ! [X78,X79,X80] : % 117.28/117.41 ( next_subocc(X78,X79,X80) % 117.28/117.41 <=> ( min_precedes(X78,X79,X80) % 117.28/117.41 & ~ ? [X81] : % 117.28/117.41 ( min_precedes(X78,X81,X80) % 117.28/117.41 & min_precedes(X81,X79,X80) ) ) ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_27,axiom, % 117.28/117.41 ! [X82,X83,X84,X85] : % 117.28/117.41 ( ( min_precedes(X82,X83,X84) % 117.28/117.41 & occurrence_of(X85,X84) % 117.28/117.41 & subactivity_occurrence(X83,X85) ) % 117.28/117.41 => subactivity_occurrence(X82,X85) ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_28,axiom, % 117.28/117.41 ! [X86,X87,X88,X89] : % 117.28/117.41 ( ( occurrence_of(X88,X89) % 117.28/117.41 & ~ atomic(X89) % 117.28/117.41 & leaf_occ(X86,X88) % 117.28/117.41 & leaf_occ(X87,X88) ) % 117.28/117.41 => X86 = X87 ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_29,axiom, % 117.28/117.41 ! [X90,X91,X92,X93] : % 117.28/117.41 ( ( occurrence_of(X92,X93) % 117.28/117.41 & root_occ(X90,X92) % 117.28/117.41 & root_occ(X91,X92) ) % 117.28/117.41 => X90 = X91 ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_30,axiom, % 117.28/117.41 ! [X94,X95,X96] : % 117.28/117.41 ( ( earlier(X94,X95) % 117.28/117.41 & earlier(X95,X96) ) % 117.28/117.41 => earlier(X94,X96) ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_31,axiom, % 117.28/117.41 ! [X97,X98,X99,X100] : % 117.28/117.41 ( ( min_precedes(X97,X98,X100) % 117.28/117.41 & min_precedes(X97,X99,X100) % 117.28/117.41 & precedes(X98,X99) ) % 117.28/117.41 => min_precedes(X98,X99,X100) ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_32,axiom, % 117.28/117.41 ! [X101] : % 117.28/117.41 ( occurrence_of(X101,tptp0) % 117.28/117.41 => ? [X102,X103,X104] : % 117.28/117.41 ( occurrence_of(X102,tptp3) % 117.28/117.41 & root_occ(X102,X101) % 117.28/117.41 & occurrence_of(X103,tptp4) % 117.28/117.41 & next_subocc(X102,X103,tptp0) % 117.28/117.41 & ( occurrence_of(X104,tptp1) % 117.28/117.41 | occurrence_of(X104,tptp2) ) % 117.28/117.41 & next_subocc(X103,X104,tptp0) % 117.28/117.41 & leaf_occ(X104,X101) ) ) ). % 117.28/117.41 % 117.28/117.41 fof(sos_33,axiom, % 117.28/117.41 activity(tptp0) ). % 117.28/117.41 % 117.28/117.41 fof(sos_34,axiom, % 117.28/117.41 ~ atomic(tptp0) ). % 117.28/117.41 % 117.28/117.41 fof(sos_35,axiom, % 117.28/117.41 atomic(tptp4) ). % 117.28/117.41 % 117.28/117.41 fof(sos_36,axiom, % 117.28/117.41 atomic(tptp1) ). % 117.28/117.41 % 117.28/117.41 fof(sos_37,axiom, % 117.28/117.41 atomic(tptp2) ). % 117.28/117.41 % 117.28/117.41 fof(sos_38,axiom, % 117.28/117.41 atomic(tptp3) ). % 117.28/117.41 % 117.28/117.41 fof(sos_39,axiom, % 117.28/117.41 tptp4 != tptp3 ). % 117.28/117.41 % 117.28/117.41 fof(sos_40,axiom, % 117.28/117.41 tptp4 != tptp1 ). % 117.28/117.41 % 117.28/117.41 fof(sos_41,axiom, % 117.28/117.41 tptp4 != tptp2 ). % 117.28/117.41 % 117.28/117.41 fof(sos_42,axiom, % 117.28/117.41 tptp3 != tptp1 ). % 117.28/117.41 % 117.28/117.41 fof(sos_43,axiom, % 117.28/117.41 tptp3 != tptp2 ). % 117.28/117.41 % 117.28/117.41 fof(sos_44,axiom, % 117.28/117.41 tptp1 != tptp2 ). % 117.28/117.41 % 117.28/117.41 fof(goals,conjecture, % 117.28/117.41 ! [X105] : % 117.28/117.41 ( occurrence_of(X105,tptp0) % 117.28/117.41 => ? [X106,X107] : % 117.28/117.41 ( leaf_occ(X107,X105) % 117.28/117.41 & ( occurrence_of(X107,tptp1) % 117.28/117.41 => ~ ? [X108] : % 117.28/117.41 ( occurrence_of(X108,tptp2) % 117.28/117.41 & subactivity_occurrence(X108,X105) % 117.28/117.41 & min_precedes(X106,X108,tptp0) ) ) % 117.28/117.41 & ( occurrence_of(X107,tptp2) % 117.28/117.41 => ~ ? [X109] : % 117.28/117.41 ( occurrence_of(X109,tptp1) % 117.28/117.41 & subactivity_occurrence(X109,X105) % 117.28/117.41 & min_precedes(X106,X109,tptp0) ) ) ) ) ). % 117.28/117.41 % 117.28/117.41 %------------------------------------------------------------------------------ % 117.28/117.41 %------------------------------------------- % 117.28/117.41 % Proof found % 117.28/117.41 % SZS status Theorem for theBenchmark % 117.28/117.41 % SZS output start Proof % 117.28/117.42 %ClaNum:163(EqnAxiom:67) % 117.28/117.42 %VarNum:472(SingletonVarNum:195) % 117.28/117.42 %MaxLitNum:8 % 117.28/117.42 %MaxfuncDepth:1 % 117.28/117.42 %SharedTerms:19 % 117.28/117.42 %goalClause: 73 101 120 121 122 123 131 132 133 134 138 139 145 146 147 148 151 % 117.28/117.42 %singleGoalClaCount:1 % 117.28/117.42 [68]P1(a1) % 117.28/117.42 [69]P1(a23) % 117.28/117.42 [70]P1(a2) % 117.28/117.42 [71]P1(a22) % 117.28/117.42 [72]P2(a3) % 117.28/117.42 [73]P6(a4,a3) % 117.28/117.42 [74]~E(a1,a23) % 117.28/117.42 [75]~E(a1,a2) % 117.28/117.42 [76]~E(a2,a23) % 117.28/117.42 [77]~E(a1,a22) % 117.28/117.42 [78]~E(a22,a23) % 117.28/117.42 [79]~E(a22,a2) % 117.28/117.42 [80]~P1(a3) % 117.28/117.42 [81]~P7(x811)+P3(x811) % 117.28/117.42 [82]~P4(x821)+P2(f11(x821)) % 117.28/117.42 [89]~P4(x891)+P6(x891,f11(x891)) % 117.28/117.42 [95]~P6(x951,a3)+P6(f5(x951),a1) % 117.28/117.42 [96]~P6(x961,a3)+P6(f9(x961),a23) % 117.28/117.42 [97]~P6(x971,a3)+P16(f5(x971),x971) % 117.28/117.42 [98]~P6(x981,a3)+P8(f10(x981),x981) % 117.28/117.42 [127]~P6(x1271,a3)+P11(f5(x1271),f9(x1271),a3) % 117.28/117.42 [128]~P6(x1281,a3)+P11(f9(x1281),f10(x1281),a3) % 117.28/117.42 [83]P2(x831)+~P6(x832,x831) % 117.28/117.42 [84]P4(x841)+~P6(x841,x842) % 117.28/117.42 [85]P4(x851)+~P13(x852,x851) % 117.28/117.42 [86]P4(x861)+~P13(x861,x862) % 117.28/117.42 [87]P7(x871)+~P14(x871,x872) % 117.28/117.42 [88]P7(x881)+~P15(x882,x881) % 117.28/117.42 [92]~P16(x921,x922)+P13(x921,x922) % 117.28/117.42 [93]~P8(x931,x932)+P13(x931,x932) % 117.28/117.42 [94]~P15(x941,x942)+P9(x941,x942) % 117.28/117.42 [100]~P9(x1002,x1001)+~P9(x1001,x1002) % 117.28/117.42 [103]~P5(x1031,x1032)+P1(f18(x1031,x1032)) % 117.28/117.42 [106]~P5(x1061,x1062)+P6(x1061,f18(x1061,x1062)) % 117.28/117.42 [107]~P8(x1072,x1071)+P6(x1071,f19(x1072,x1071)) % 117.28/117.42 [108]~P16(x1082,x1081)+P6(x1081,f6(x1082,x1081)) % 117.28/117.42 [109]~P16(x1091,x1092)+P14(x1091,f6(x1091,x1092)) % 117.28/117.42 [110]~P5(x1102,x1101)+P17(x1101,f18(x1102,x1101)) % 117.28/117.42 [111]~P14(x1111,x1112)+P5(x1111,f12(x1112,x1111)) % 117.28/117.42 [112]~P8(x1121,x1122)+P10(x1121,f19(x1121,x1122)) % 117.28/117.42 [113]~P14(x1132,x1131)+P17(f12(x1131,x1132),x1131) % 117.28/117.42 [129]P3(x1291)+~P11(x1292,x1291,x1293) % 117.28/117.42 [130]P3(x1301)+~P11(x1301,x1302,x1303) % 117.28/117.42 [135]P15(x1351,x1352)+~P12(x1351,x1352,x1353) % 117.28/117.42 [136]~P14(x1361,x1362)+~P12(x1363,x1361,x1362) % 117.28/117.42 [137]~P10(x1371,x1372)+~P12(x1371,x1373,x1372) % 117.28/117.42 [149]~P11(x1491,x1492,x1493)+P12(x1491,x1492,x1493) % 117.28/117.42 [154]~P12(x1543,x1541,x1542)+P13(x1541,f17(x1542,x1543,x1541)) % 117.28/117.42 [155]~P12(x1551,x1553,x1552)+P13(x1551,f17(x1552,x1551,x1553)) % 117.28/117.42 [156]~P12(x1562,x1563,x1561)+P6(f17(x1561,x1562,x1563),x1561) % 117.28/117.42 [157]~P12(x1571,x1572,x1573)+P14(f7(x1571,x1572,x1573),x1573) % 117.28/117.42 [159]~P12(x1591,x1592,x1593)+P12(f7(x1591,x1592,x1593),x1592,x1593) % 117.28/117.42 [101]P6(x1011,a22)+~P8(x1011,a4)+P6(x1011,a2) % 117.28/117.42 [104]~P6(x1041,a3)+P6(f10(x1041),a2)+P6(f10(x1041),a22) % 117.28/117.42 [90]~P6(x902,x901)+P1(x901)+~P3(x902) % 117.28/117.42 [91]~P6(x911,x912)+P3(x911)+~P1(x912) % 117.28/117.42 [99]~P7(x992)+~P9(x991,x992)+P15(x991,x992) % 117.28/117.42 [115]~P10(x1152,x1151)+P1(x1151)+P8(x1152,f16(x1152,x1151)) % 117.28/117.42 [116]~P10(x1162,x1161)+P1(x1161)+P6(f16(x1162,x1161),x1161) % 117.28/117.42 [117]~P6(x1172,x1171)+P1(x1171)+P14(f13(x1171,x1172),x1171) % 117.28/117.42 [118]~P6(x1182,x1181)+P1(x1181)+P13(f13(x1181,x1182),x1182) % 117.28/117.42 [120]~P8(x1201,a4)+P6(x1201,a2)+P6(f14(x1202,x1201),a2) % 117.28/117.42 [121]~P8(x1211,a4)+P6(x1211,a2)+P13(f14(x1212,x1211),a4) % 117.28/117.42 [122]~P8(x1221,a4)+P6(x1221,a22)+P6(f15(x1222,x1221),a22) % 117.28/117.42 [123]~P8(x1231,a4)+P6(x1231,a22)+P13(f15(x1232,x1231),a4) % 117.28/117.42 [131]~P8(x1312,a4)+P6(f14(x1311,x1312),a2)+P6(f15(x1311,x1312),a22) % 117.28/117.42 [132]~P8(x1322,a4)+P13(f14(x1321,x1322),a4)+P6(f15(x1321,x1322),a22) % 117.28/117.42 [133]~P8(x1332,a4)+P13(f15(x1331,x1332),a4)+P6(f14(x1331,x1332),a2) % 117.28/117.42 [134]~P8(x1342,a4)+P13(f14(x1341,x1342),a4)+P13(f15(x1341,x1342),a4) % 117.28/117.42 [138]~P8(x1381,a4)+P6(x1381,a2)+P12(x1382,f14(x1382,x1381),a3) % 117.28/117.42 [139]~P8(x1391,a4)+P6(x1391,a22)+P12(x1392,f15(x1392,x1391),a3) % 117.28/117.42 [140]~P14(x1401,x1402)+P10(x1401,x1402)+P12(x1401,f20(x1401,x1402),x1402) % 117.28/117.42 [141]~P10(x1411,x1412)+P14(x1411,x1412)+P12(f21(x1411,x1412),x1411,x1412) % 117.28/117.42 [145]~P8(x1452,a4)+P12(x1451,f14(x1451,x1452),a3)+P6(f15(x1451,x1452),a22) % 117.28/117.42 [146]~P8(x1462,a4)+P12(x1461,f15(x1461,x1462),a3)+P6(f14(x1461,x1462),a2) % 117.28/117.42 [147]~P8(x1472,a4)+P12(x1471,f14(x1471,x1472),a3)+P13(f15(x1471,x1472),a4) % 117.28/117.42 [148]~P8(x1482,a4)+P12(x1481,f15(x1481,x1482),a3)+P13(f14(x1481,x1482),a4) % 117.28/117.42 [151]~P8(x1512,a4)+P12(x1511,f14(x1511,x1512),a3)+P12(x1511,f15(x1511,x1512),a3) % 117.28/117.42 [102]~P6(x1023,x1021)+E(x1021,x1022)+~P6(x1023,x1022) % 117.28/117.42 [105]~P9(x1051,x1053)+P9(x1051,x1052)+~P9(x1053,x1052) % 117.28/117.42 [152]P10(x1521,x1522)+~P12(x1523,x1521,x1522)+P12(x1521,f20(x1521,x1522),x1522) % 117.28/117.42 [162]~P12(x1621,x1622,x1623)+P11(x1621,x1622,x1623)+P12(x1621,f8(x1621,x1622,x1623),x1623) % 117.28/117.42 [163]~P12(x1631,x1632,x1633)+P11(x1631,x1632,x1633)+P12(f8(x1631,x1632,x1633),x1632,x1633) % 117.28/117.42 [142]~P6(x1421,x1422)+~P12(x1424,x1423,x1422)+~P16(x1423,x1421) % 117.28/117.42 [143]~P6(x1431,x1432)+~P12(x1433,x1434,x1432)+~P8(x1433,x1431) % 117.28/117.42 [161]~P11(x1614,x1612,x1613)+~P12(x1611,x1612,x1613)+~P12(x1614,x1611,x1613) % 117.28/117.42 [114]~P6(x1141,x1143)+~P17(x1142,x1143)+P5(x1141,x1142)+~P1(x1143) % 117.28/117.42 [125]~P14(x1251,x1253)+~P13(x1251,x1252)+P16(x1251,x1252)+~P6(x1252,x1253) % 117.28/117.42 [126]~P13(x1261,x1262)+~P10(x1261,x1263)+P8(x1261,x1262)+~P6(x1262,x1263) % 117.28/117.42 [119]~P16(x1192,x1193)+~P16(x1191,x1193)+E(x1191,x1192)+~P6(x1193,x1194) % 117.28/117.42 [150]~P12(x1501,x1504,x1503)+P13(x1501,x1502)+~P6(x1502,x1503)+~P13(x1504,x1502) % 117.28/117.42 [160]~P15(x1601,x1602)+~P12(x1604,x1601,x1603)+P12(x1601,x1602,x1603)+~P12(x1604,x1602,x1603) % 117.28/117.42 [124]~P8(x1242,x1244)+~P8(x1241,x1244)+E(x1241,x1242)+~P6(x1244,x1243)+P1(x1243) % 117.28/117.42 [144]~P3(x1441)+~P13(x1441,x1444)+~P8(x1442,x1444)+E(x1441,x1442)+P12(x1441,x1442,x1443)+~P6(x1444,x1443) % 117.28/117.42 [158]~P13(x1582,x1584)+~P8(x1581,x1584)+~P12(x1585,x1582,x1583)+E(x1581,x1582)+P12(x1582,x1581,x1583)+~P6(x1584,x1583)+~P16(x1585,x1584) % 117.28/117.42 [153]P12(x1531,x1532,x1533)+~P3(x1532)+~P3(x1531)+~P13(x1532,x1534)+~P13(x1531,x1534)+E(x1531,x1532)+P12(x1532,x1531,x1533)+~P6(x1534,x1533) % 117.28/117.42 %EqnAxiom % 117.28/117.42 [1]E(x11,x11) % 117.28/117.42 [2]E(x22,x21)+~E(x21,x22) % 117.28/117.42 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 117.28/117.42 [4]~E(x41,x42)+E(f11(x41),f11(x42)) % 117.28/117.42 [5]~E(x51,x52)+E(f8(x51,x53,x54),f8(x52,x53,x54)) % 117.28/117.42 [6]~E(x61,x62)+E(f8(x63,x61,x64),f8(x63,x62,x64)) % 117.28/117.42 [7]~E(x71,x72)+E(f8(x73,x74,x71),f8(x73,x74,x72)) % 117.28/117.42 [8]~E(x81,x82)+E(f5(x81),f5(x82)) % 117.28/117.42 [9]~E(x91,x92)+E(f9(x91),f9(x92)) % 117.28/117.42 [10]~E(x101,x102)+E(f7(x101,x103,x104),f7(x102,x103,x104)) % 117.28/117.42 [11]~E(x111,x112)+E(f7(x113,x111,x114),f7(x113,x112,x114)) % 117.28/117.42 [12]~E(x121,x122)+E(f7(x123,x124,x121),f7(x123,x124,x122)) % 117.28/117.42 [13]~E(x131,x132)+E(f10(x131),f10(x132)) % 117.28/117.42 [14]~E(x141,x142)+E(f18(x141,x143),f18(x142,x143)) % 117.28/117.42 [15]~E(x151,x152)+E(f18(x153,x151),f18(x153,x152)) % 117.28/117.42 [16]~E(x161,x162)+E(f20(x161,x163),f20(x162,x163)) % 117.28/117.42 [17]~E(x171,x172)+E(f20(x173,x171),f20(x173,x172)) % 117.28/117.42 [18]~E(x181,x182)+E(f14(x181,x183),f14(x182,x183)) % 117.28/117.42 [19]~E(x191,x192)+E(f14(x193,x191),f14(x193,x192)) % 117.28/117.42 [20]~E(x201,x202)+E(f15(x201,x203),f15(x202,x203)) % 117.28/117.42 [21]~E(x211,x212)+E(f15(x213,x211),f15(x213,x212)) % 117.28/117.42 [22]~E(x221,x222)+E(f19(x221,x223),f19(x222,x223)) % 117.28/117.42 [23]~E(x231,x232)+E(f19(x233,x231),f19(x233,x232)) % 117.28/117.42 [24]~E(x241,x242)+E(f6(x241,x243),f6(x242,x243)) % 117.28/117.42 [25]~E(x251,x252)+E(f6(x253,x251),f6(x253,x252)) % 117.28/117.42 [26]~E(x261,x262)+E(f17(x261,x263,x264),f17(x262,x263,x264)) % 117.28/117.42 [27]~E(x271,x272)+E(f17(x273,x271,x274),f17(x273,x272,x274)) % 117.28/117.42 [28]~E(x281,x282)+E(f17(x283,x284,x281),f17(x283,x284,x282)) % 117.28/117.42 [29]~E(x291,x292)+E(f21(x291,x293),f21(x292,x293)) % 117.28/117.42 [30]~E(x301,x302)+E(f21(x303,x301),f21(x303,x302)) % 117.28/117.42 [31]~E(x311,x312)+E(f12(x311,x313),f12(x312,x313)) % 117.28/117.42 [32]~E(x321,x322)+E(f12(x323,x321),f12(x323,x322)) % 117.28/117.42 [33]~E(x331,x332)+E(f13(x331,x333),f13(x332,x333)) % 117.28/117.42 [34]~E(x341,x342)+E(f13(x343,x341),f13(x343,x342)) % 117.28/117.42 [35]~E(x351,x352)+E(f16(x351,x353),f16(x352,x353)) % 117.28/117.42 [36]~E(x361,x362)+E(f16(x363,x361),f16(x363,x362)) % 117.28/117.42 [37]~P1(x371)+P1(x372)+~E(x371,x372) % 117.28/117.42 [38]P12(x382,x383,x384)+~E(x381,x382)+~P12(x381,x383,x384) % 117.28/117.42 [39]P12(x393,x392,x394)+~E(x391,x392)+~P12(x393,x391,x394) % 117.28/117.42 [40]P12(x403,x404,x402)+~E(x401,x402)+~P12(x403,x404,x401) % 117.28/117.42 [41]P8(x412,x413)+~E(x411,x412)+~P8(x411,x413) % 117.28/117.42 [42]P8(x423,x422)+~E(x421,x422)+~P8(x423,x421) % 117.28/117.43 [43]P11(x432,x433,x434)+~E(x431,x432)+~P11(x431,x433,x434) % 117.28/117.43 [44]P11(x443,x442,x444)+~E(x441,x442)+~P11(x443,x441,x444) % 117.28/117.43 [45]P11(x453,x454,x452)+~E(x451,x452)+~P11(x453,x454,x451) % 117.28/117.43 [46]~P2(x461)+P2(x462)+~E(x461,x462) % 117.28/117.43 [47]P6(x472,x473)+~E(x471,x472)+~P6(x471,x473) % 117.28/117.43 [48]P6(x483,x482)+~E(x481,x482)+~P6(x483,x481) % 117.28/117.43 [49]P16(x492,x493)+~E(x491,x492)+~P16(x491,x493) % 117.28/117.43 [50]P16(x503,x502)+~E(x501,x502)+~P16(x503,x501) % 117.28/117.43 [51]~P3(x511)+P3(x512)+~E(x511,x512) % 117.28/117.43 [52]~P7(x521)+P7(x522)+~E(x521,x522) % 117.28/117.43 [53]P10(x532,x533)+~E(x531,x532)+~P10(x531,x533) % 117.28/117.43 [54]P10(x543,x542)+~E(x541,x542)+~P10(x543,x541) % 117.28/117.43 [55]~P4(x551)+P4(x552)+~E(x551,x552) % 117.28/117.43 [56]P13(x562,x563)+~E(x561,x562)+~P13(x561,x563) % 117.28/117.43 [57]P13(x573,x572)+~E(x571,x572)+~P13(x573,x571) % 117.28/117.43 [58]P14(x582,x583)+~E(x581,x582)+~P14(x581,x583) % 117.28/117.43 [59]P14(x593,x592)+~E(x591,x592)+~P14(x593,x591) % 117.28/117.43 [60]P9(x602,x603)+~E(x601,x602)+~P9(x601,x603) % 117.28/117.43 [61]P9(x613,x612)+~E(x611,x612)+~P9(x613,x611) % 117.28/117.43 [62]P15(x622,x623)+~E(x621,x622)+~P15(x621,x623) % 117.28/117.43 [63]P15(x633,x632)+~E(x631,x632)+~P15(x633,x631) % 117.28/117.43 [64]P5(x642,x643)+~E(x641,x642)+~P5(x641,x643) % 117.28/117.43 [65]P5(x653,x652)+~E(x651,x652)+~P5(x653,x651) % 117.28/117.43 [66]P17(x662,x663)+~E(x661,x662)+~P17(x661,x663) % 117.28/117.43 [67]P17(x673,x672)+~E(x671,x672)+~P17(x673,x671) % 117.28/117.43 % 117.28/117.43 %------------------------------------------- % 117.28/117.45 cnf(164,plain, % 117.28/117.45 (~P3(a4)), % 117.28/117.45 inference(scs_inference,[],[73,80,90])). % 117.28/117.45 cnf(166,plain, % 117.28/117.45 (~P6(a4,a1)), % 117.28/117.45 inference(scs_inference,[],[73,68,80,90,91])). % 117.28/117.45 cnf(168,plain, % 117.28/117.45 (~E(a3,a1)), % 117.28/117.45 inference(scs_inference,[],[73,68,80,90,91,48])). % 117.28/117.45 cnf(171,plain, % 117.28/117.45 (~P14(a4,x1711)), % 117.28/117.45 inference(scs_inference,[],[73,68,80,90,91,48,81,87])). % 117.28/117.45 cnf(173,plain, % 117.28/117.45 (~P16(a4,x1731)), % 117.28/117.45 inference(scs_inference,[],[73,68,80,90,91,48,81,87,109])). % 117.28/117.45 cnf(175,plain, % 117.28/117.45 (~P11(x1751,a4,x1752)), % 117.28/117.45 inference(scs_inference,[],[73,68,80,90,91,48,81,87,109,129])). % 117.28/117.45 cnf(181,plain, % 117.28/117.45 (P6(x1811,a3)+~E(a4,x1811)), % 117.28/117.45 inference(scs_inference,[],[73,68,80,90,91,48,81,87,109,129,130,88,47])). % 117.28/117.45 cnf(182,plain, % 117.28/117.45 (~P12(x1821,a4,x1822)), % 117.28/117.45 inference(scs_inference,[],[73,68,80,90,91,48,81,87,109,129,130,88,47,135])). % 117.28/117.45 cnf(193,plain, % 117.28/117.45 (~P6(a4,a23)), % 117.28/117.45 inference(scs_inference,[],[182,164,171,69,141,91])). % 117.28/117.45 cnf(195,plain, % 117.28/117.45 (~P8(a4,x1951)), % 117.28/117.45 inference(scs_inference,[],[182,164,171,69,141,91,112])). % 117.28/117.45 cnf(200,plain, % 117.28/117.45 (~P6(a4,a2)), % 117.28/117.45 inference(scs_inference,[],[164,70,91])). % 117.28/117.45 cnf(275,plain, % 117.28/117.45 (~P13(x2751,x2752)+P6(x2752,f11(x2752))), % 117.28/117.45 inference(scs_inference,[],[85,89])). % 117.28/117.45 cnf(291,plain, % 117.28/117.45 (~P13(x2911,x2912)+P2(f11(x2911))), % 117.28/117.45 inference(scs_inference,[],[86,82])). % 117.28/117.45 cnf(307,plain, % 117.28/117.45 (~E(a1,a3)), % 117.28/117.45 inference(scs_inference,[],[73,166,2,48])). % 117.28/117.45 cnf(370,plain, % 117.28/117.45 (~P9(x3701,x3702)+~P15(x3702,x3701)), % 117.28/117.45 inference(scs_inference,[],[94,100])). % 117.28/117.45 cnf(743,plain, % 117.28/117.45 (~P9(x7431,x7432)+~P12(x7432,x7431,x7433)), % 117.28/117.45 inference(scs_inference,[],[370,135])). % 117.28/117.45 cnf(759,plain, % 117.28/117.45 (~P12(x7591,x7592,a3)+P6(f5(f17(a3,x7591,x7592)),a1)), % 117.28/117.45 inference(scs_inference,[],[95,156])). % 117.28/117.45 cnf(775,plain, % 117.28/117.45 (~E(a4,x7751)+P6(f9(x7751),a23)), % 117.28/117.45 inference(scs_inference,[],[96,181])). % 117.28/117.45 cnf(776,plain, % 117.28/117.45 (P6(f9(a4),a23)), % 117.28/117.45 inference(equality_inference,[],[775])). % 117.28/117.45 cnf(827,plain, % 117.28/117.45 (P13(f5(a4),a4)), % 117.28/117.45 inference(scs_inference,[],[73,97,92])). % 117.28/117.45 cnf(850,plain, % 117.28/117.45 (P13(f10(a4),a4)), % 117.28/117.45 inference(scs_inference,[],[73,98,93])). % 117.28/117.45 cnf(871,plain, % 117.28/117.45 (~P14(x8711,x8712)+P1(f18(x8711,f12(x8712,x8711)))), % 117.28/117.45 inference(scs_inference,[],[103,111])). % 117.28/117.45 cnf(887,plain, % 117.28/117.45 (~P12(x8871,f13(a3,a4),a3)), % 117.28/117.45 inference(scs_inference,[],[80,73,136,117])). % 117.28/117.45 cnf(888,plain, % 117.28/117.45 (~P11(x8881,f13(a3,a4),a3)), % 117.28/117.45 inference(scs_inference,[],[887,149])). % 117.28/117.45 cnf(911,plain, % 117.28/117.45 (~P12(x9111,x9112,f19(x9111,x9113))+~P8(x9111,x9113)), % 117.28/117.45 inference(scs_inference,[],[137,112])). % 117.28/117.45 cnf(960,plain, % 117.28/117.45 (~P12(x9601,x9602,x9603)+~P15(x9602,x9601)), % 117.28/117.45 inference(scs_inference,[],[743,94])). % 117.28/117.45 cnf(976,plain, % 117.28/117.45 (~P12(x9761,x9762,x9763)+~P12(x9762,x9761,x9764)), % 117.28/117.45 inference(scs_inference,[],[960,135])). % 117.28/117.45 cnf(992,plain, % 117.28/117.45 (~E(x9921,x9922)+E(f11(x9922),f11(x9921))), % 117.28/117.45 inference(scs_inference,[],[4,2])). % 117.28/117.45 cnf(1009,plain, % 117.28/117.45 (~E(x10091,x10092)+E(f5(f8(x10091,x10093,x10094)),f5(f8(x10092,x10093,x10094)))), % 117.28/117.45 inference(scs_inference,[],[8,5])). % 117.28/117.45 cnf(1026,plain, % 117.28/117.45 (~E(x10261,x10262)+E(f9(f8(x10263,x10261,x10264)),f9(f8(x10263,x10262,x10264)))), % 117.28/117.45 inference(scs_inference,[],[9,6])). % 117.28/117.45 cnf(1043,plain, % 117.28/117.45 (~E(x10431,x10432)+E(f10(f8(x10433,x10434,x10431)),f10(f8(x10433,x10434,x10432)))), % 117.28/117.45 inference(scs_inference,[],[13,7])). % 117.28/117.45 cnf(1060,plain, % 117.28/117.45 (~P14(x10601,x10602)+P6(x10601,f18(x10601,f12(x10602,x10601)))), % 117.28/117.45 inference(scs_inference,[],[106,111])). % 117.28/117.45 cnf(1076,plain, % 117.28/117.45 (P6(a4,f19(f10(a4),a4))), % 117.28/117.45 inference(scs_inference,[],[73,107,98])). % 117.28/117.45 cnf(1079,plain, % 117.28/117.45 (E(a3,f19(f10(a4),a4))), % 117.28/117.45 inference(scs_inference,[],[73,166,1076,48,47,102])). % 117.28/117.45 cnf(1086,plain, % 117.28/117.45 (E(f19(f10(a4),a4),a3)), % 117.28/117.45 inference(scs_inference,[],[1079,2])). % 117.28/117.45 cnf(1088,plain, % 117.28/117.45 (~P1(f19(f10(a4),a4))), % 117.28/117.45 inference(scs_inference,[],[1079,307,80,2,3,37])). % 117.28/117.45 cnf(1309,plain, % 117.28/117.45 (P6(a4,f6(f5(a4),a4))), % 117.28/117.45 inference(scs_inference,[],[73,108,97])). % 117.28/117.45 cnf(1312,plain, % 117.28/117.45 (E(a3,f6(f5(a4),a4))), % 117.28/117.45 inference(scs_inference,[],[73,200,1309,48,47,102])). % 117.28/117.45 cnf(1319,plain, % 117.28/117.45 (E(f6(f5(a4),a4),a3)), % 117.28/117.45 inference(scs_inference,[],[1312,2])). % 117.28/117.45 cnf(1321,plain, % 117.28/117.45 (~P1(f6(f5(a4),a4))), % 117.28/117.45 inference(scs_inference,[],[1312,307,80,2,3,37])). % 117.28/117.45 cnf(1555,plain, % 117.28/117.45 (~P14(x15551,x15552)+P17(f12(x15552,x15551),f18(x15551,f12(x15552,x15551)))), % 117.28/117.45 inference(scs_inference,[],[110,111])). % 117.28/117.45 cnf(1571,plain, % 117.28/117.45 (P17(f12(a3,f13(a3,a4)),a3)), % 117.28/117.45 inference(scs_inference,[],[80,73,113,117])). % 117.28/117.45 cnf(1572,plain, % 117.28/117.45 (P17(x15721,a3)+~E(f12(a3,f13(a3,a4)),x15721)), % 117.28/117.45 inference(scs_inference,[],[1571,66])). % 117.28/117.45 cnf(1573,plain, % 117.28/117.45 (P17(x15731,f19(f10(a4),a4))+~E(f12(a3,f13(a3,a4)),x15731)), % 117.28/117.45 inference(scs_inference,[],[1079,1571,66,67])). % 117.28/117.45 cnf(1578,plain, % 117.28/117.45 (P17(f12(a3,f13(a3,a4)),f19(f10(a4),a4))), % 117.28/117.45 inference(equality_inference,[],[1573])). % 117.28/117.45 cnf(2900,plain, % 117.28/117.45 (~P12(x29001,x29002,a3)+P11(f5(f17(a3,x29001,x29002)),f9(f17(a3,x29001,x29002)),a3)), % 117.28/117.45 inference(scs_inference,[],[127,156])). % 117.28/117.45 cnf(2916,plain, % 117.28/117.45 (~E(f18(x29161,f12(x29162,x29161)),a3)+~P14(x29161,x29162)), % 117.28/117.45 inference(scs_inference,[],[80,871,37])). % 117.28/117.45 cnf(2932,plain, % 117.28/117.45 (~P12(f10(a4),x29321,f19(f10(a4),a4))), % 117.28/117.45 inference(scs_inference,[],[73,911,98])). % 117.28/117.45 cnf(2933,plain, % 117.28/117.45 (~P11(f10(a4),x29331,f19(f10(a4),a4))), % 117.28/117.45 inference(scs_inference,[],[2932,149])). % 117.28/117.45 cnf(4084,plain, % 117.28/117.45 (~P6(f9(a4),a1)), % 117.28/117.45 inference(scs_inference,[],[776,74,102])). % 117.28/117.45 cnf(4088,plain, % 117.28/117.45 (~E(f5(f17(a3,x40881,x40882)),f9(a4))+~P12(x40881,x40882,a3)), % 117.28/117.45 inference(scs_inference,[],[776,74,102,48,47,759])). % 117.28/117.45 cnf(4091,plain, % 117.28/117.45 (~P11(x40911,x40912,a3)+~E(f5(f17(a3,x40911,x40912)),f9(a4))), % 117.28/117.45 inference(scs_inference,[],[776,74,102,48,47,759,95,149])). % 117.28/117.45 cnf(4109,plain, % 117.28/117.45 (~P6(x41091,a2)+~P6(x41091,a1)), % 117.28/117.45 inference(scs_inference,[],[75,102])). % 117.28/117.45 cnf(4115,plain, % 117.28/117.45 (~P6(x41151,a22)+~P6(x41151,a1)), % 117.28/117.45 inference(scs_inference,[],[77,102])). % 117.28/117.45 cnf(4143,plain, % 117.28/117.45 (~P6(f5(a4),a2)), % 117.28/117.45 inference(scs_inference,[],[73,4109,95])). % 117.28/117.45 cnf(4159,plain, % 117.28/117.45 (~P12(x41591,x41592,a3)+~E(x41592,f13(a3,a4))), % 117.28/117.45 inference(scs_inference,[],[887,776,75,2,83,39])). % 117.28/117.45 cnf(4183,plain, % 117.28/117.45 (~P11(x41831,x41832,x41833)+~E(x41832,a4)), % 117.28/117.45 inference(scs_inference,[],[175,44])). % 117.28/117.45 cnf(4194,plain, % 117.28/117.45 (~P12(x41941,x41942,x41943)+~E(x41942,a4)), % 117.28/117.45 inference(scs_inference,[],[182,39])). % 117.28/117.45 cnf(4230,plain, % 117.28/117.45 (~P6(f5(a4),a22)), % 117.28/117.45 inference(scs_inference,[],[73,4115,95])). % 117.28/117.45 cnf(4231,plain, % 117.28/117.45 (~P6(f5(a4),x42311)+~E(x42311,a22)), % 117.28/117.45 inference(scs_inference,[],[4230,48])). % 117.28/117.45 cnf(4232,plain, % 117.28/117.45 (~E(a22,x42321)+~P6(f5(a4),x42321)), % 117.28/117.45 inference(scs_inference,[],[4230,48,2])). % 117.28/117.45 cnf(4286,plain, % 117.28/117.45 (P6(a4,f11(a4))), % 117.28/117.45 inference(scs_inference,[],[827,275])). % 117.28/117.45 cnf(5053,plain, % 117.28/117.45 (~P12(x50531,f10(a4),f11(a4))+P13(x50531,a4)), % 117.28/117.45 inference(scs_inference,[],[850,4286,150])). % 117.28/117.45 cnf(5055,plain, % 117.28/117.45 (P2(f11(x50551))+~P12(x50551,f10(a4),f11(a4))), % 117.28/117.45 inference(scs_inference,[],[850,4286,150,291])). % 117.28/117.45 cnf(5241,plain, % 117.28/117.45 (~P12(x52411,f10(a4),f11(a4))+P13(f7(x52411,f10(a4),f11(a4)),a4)), % 117.28/117.45 inference(scs_inference,[],[5053,159])). % 117.28/117.45 cnf(5322,plain, % 117.28/117.45 (E(f18(f11(a3),x53221),f18(f11(f19(f10(a4),a4)),x53221))), % 117.28/117.45 inference(scs_inference,[],[1079,14,4])). % 117.28/117.45 cnf(5338,plain, % 117.28/117.45 (E(f18(x53381,f8(a3,x53382,x53383)),f18(x53381,f8(f19(f10(a4),a4),x53382,x53383)))), % 117.28/117.45 inference(scs_inference,[],[1079,15,5])). % 117.28/117.45 cnf(5546,plain, % 117.28/117.45 (E(f12(x55461,f13(a3,x55462)),f12(x55461,f13(f19(f10(a4),a4),x55462)))), % 117.28/117.45 inference(scs_inference,[],[1079,32,33])). % 117.28/117.45 cnf(5578,plain, % 117.28/117.45 (E(f16(x55781,f11(f19(f10(a4),a4))),f16(x55781,f11(a3)))), % 117.28/117.45 inference(scs_inference,[],[1079,36,992])). % 117.28/117.45 cnf(5674,plain, % 117.28/117.45 (~P14(x56741,x56742)+P2(f18(x56741,f12(x56742,x56741)))), % 117.28/117.45 inference(scs_inference,[],[1060,83])). % 117.28/117.45 cnf(5690,plain, % 117.28/117.45 (~E(f18(x56901,f12(x56902,x56901)),x56903)+~P14(x56901,x56902)+P2(x56903)), % 117.28/117.45 inference(scs_inference,[],[5674,46])). % 117.28/117.45 cnf(6249,plain, % 117.28/117.45 (~E(a1,x62491)+~E(a3,x62491)), % 117.28/117.45 inference(scs_inference,[],[168,3,2])). % 117.28/117.45 cnf(6290,plain, % 117.28/117.45 (~P16(x62901,a4)+~P16(a3,a4)+~E(a1,x62901)), % 117.28/117.45 inference(scs_inference,[],[73,6249,119])). % 117.28/117.45 cnf(6292,plain, % 117.28/117.45 (P8(f10(a4),a4)), % 117.28/117.45 inference(scs_inference,[],[73,98])). % 117.28/117.45 cnf(6294,plain, % 117.28/117.45 (P11(f9(a4),f10(a4),a3)), % 117.28/117.45 inference(scs_inference,[],[73,98,128])). % 117.28/117.45 cnf(6296,plain, % 117.28/117.45 (P11(f5(a4),f9(a4),a3)), % 117.28/117.45 inference(scs_inference,[],[73,98,128,127])). % 117.28/117.45 cnf(6298,plain, % 117.28/117.45 (P16(f5(a4),a4)), % 117.28/117.45 inference(scs_inference,[],[73,98,128,127,97])). % 117.28/117.45 cnf(6300,plain, % 117.28/117.45 (P4(f5(a4))), % 117.28/117.45 inference(scs_inference,[],[73,827,98,128,127,97,86])). % 117.28/117.45 cnf(6304,plain, % 117.28/117.45 (P3(f10(a4))), % 117.28/117.45 inference(scs_inference,[],[73,776,827,98,128,127,97,86,84,129])). % 117.28/117.45 cnf(6306,plain, % 117.28/117.45 (P6(f5(a4),a1)), % 117.28/117.45 inference(scs_inference,[],[73,776,827,98,128,127,97,86,84,129,95])). % 117.28/117.45 cnf(6308,plain, % 117.28/117.45 (P3(f9(a4))), % 117.28/117.45 inference(scs_inference,[],[73,776,827,98,128,127,97,86,84,129,95,130])). % 117.28/117.45 cnf(6310,plain, % 117.28/117.45 (P12(f9(a4),f10(a4),a3)), % 117.28/117.45 inference(scs_inference,[],[73,776,827,98,128,127,97,86,84,129,95,130,149])). % 117.28/117.45 cnf(6316,plain, % 117.28/117.45 (P14(f13(a3,a4),a3)), % 117.28/117.45 inference(scs_inference,[],[73,80,776,827,98,128,127,97,86,84,129,95,130,149,142,143,117])). % 117.28/117.45 cnf(6318,plain, % 117.28/117.45 (P13(f13(a3,a4),a4)), % 117.28/117.45 inference(scs_inference,[],[73,80,776,827,98,128,127,97,86,84,129,95,130,149,142,143,117,118])). % 117.28/117.45 cnf(6322,plain, % 117.28/117.45 (~P12(f9(a4),f9(a4),a3)), % 117.28/117.45 inference(scs_inference,[],[73,4230,4143,80,776,827,98,128,127,97,86,84,129,95,130,149,142,143,117,118,101,161])). % 117.28/117.45 cnf(6329,plain, % 117.28/117.45 (P3(f5(a4))), % 117.28/117.45 inference(scs_inference,[],[73,4286,171,4230,68,193,195,4143,80,776,827,98,128,127,97,86,84,129,95,130,149,142,143,117,118,101,161,41,48,58,91])). % 117.28/117.45 cnf(6333,plain, % 117.28/117.45 (~P10(f5(a4),a3)), % 117.28/117.45 inference(scs_inference,[],[73,4286,171,4230,68,193,195,4143,173,80,776,827,98,128,127,97,86,84,129,95,130,149,142,143,117,118,101,161,41,48,58,91,49,126])). % 117.28/117.45 cnf(6335,plain, % 117.28/117.45 (P16(f13(a3,a4),a4)), % 117.28/117.45 inference(scs_inference,[],[73,4286,171,4230,68,193,195,4143,173,80,776,827,98,128,127,97,86,84,129,95,130,149,142,143,117,118,101,161,41,48,58,91,49,126,125])). % 117.28/117.45 cnf(6337,plain, % 117.28/117.45 (P13(f9(a4),a4)), % 117.28/117.45 inference(scs_inference,[],[73,4286,171,4230,68,193,195,4143,173,80,776,827,850,98,128,127,97,86,84,129,95,130,149,142,143,117,118,101,161,41,48,58,91,49,126,125,150])). % 117.28/117.45 cnf(6339,plain, % 117.28/117.45 (~P14(f10(a4),a3)), % 117.28/117.45 inference(scs_inference,[],[73,4286,171,4230,68,193,195,4143,173,80,776,827,850,98,128,127,97,86,84,129,95,130,149,142,143,117,118,101,161,41,48,58,91,49,126,125,150,136])). % 117.28/117.45 cnf(6341,plain, % 117.28/117.45 (~P10(f9(a4),a3)), % 117.28/117.45 inference(scs_inference,[],[73,4286,171,4230,68,193,195,4143,173,80,776,827,850,98,128,127,97,86,84,129,95,130,149,142,143,117,118,101,161,41,48,58,91,49,126,125,150,136,137])). % 117.28/117.45 cnf(6347,plain, % 117.28/117.45 (~P12(f10(a4),f9(a4),x63471)), % 117.28/117.45 inference(scs_inference,[],[73,4286,171,4230,68,193,195,4143,173,80,776,827,850,98,128,127,97,86,84,129,95,130,149,142,143,117,118,101,161,41,48,58,91,49,126,125,150,136,137,743,960,976])). % 117.28/117.45 cnf(6349,plain, % 117.28/117.45 (P15(f9(a4),f10(a4))), % 117.28/117.45 inference(scs_inference,[],[73,4286,171,4230,68,193,195,4143,173,80,776,827,850,98,128,127,97,86,84,129,95,130,149,142,143,117,118,101,161,41,48,58,91,49,126,125,150,136,137,743,960,976,135])). % 117.28/117.45 cnf(6351,plain, % 117.28/117.45 (P7(f10(a4))), % 117.28/117.45 inference(scs_inference,[],[73,4286,171,4230,68,193,195,4143,173,80,776,827,850,98,128,127,97,86,84,129,95,130,149,142,143,117,118,101,161,41,48,58,91,49,126,125,150,136,137,743,960,976,135,88])). % 117.28/117.45 cnf(6353,plain, % 117.28/117.45 (P7(f13(a3,a4))), % 117.28/117.45 inference(scs_inference,[],[73,4286,171,4230,68,193,195,4143,173,80,776,827,850,98,128,127,97,86,84,129,95,130,149,142,143,117,118,101,161,41,48,58,91,49,126,125,150,136,137,743,960,976,135,88,87])). % 117.28/117.45 cnf(6357,plain, % 117.28/117.45 (P9(f9(a4),f10(a4))), % 117.28/117.45 inference(scs_inference,[],[73,4286,171,4230,68,193,195,4143,173,80,776,827,850,98,128,127,97,86,84,129,95,130,149,142,143,117,118,101,161,41,48,58,91,49,126,125,150,136,137,743,960,976,135,88,87,105,94])). % 117.28/117.45 cnf(6361,plain, % 117.28/117.45 (P4(f13(a3,a4))), % 117.28/117.45 inference(scs_inference,[],[6318,86])). % 117.28/117.45 cnf(6363,plain, % 117.28/117.45 (P12(f5(a4),f9(a4),a3)), % 117.28/117.45 inference(scs_inference,[],[6318,6296,86,149])). % 117.28/117.45 cnf(6365,plain, % 117.28/117.45 (~P16(f9(a4),a4)), % 117.28/117.45 inference(scs_inference,[],[73,6318,6296,86,149,142])). % 117.28/117.45 cnf(6367,plain, % 117.28/117.45 (~E(f10(a4),f9(a4))), % 117.28/117.45 inference(scs_inference,[],[73,6318,6296,6310,6322,86,149,142,39])). % 117.28/117.45 cnf(6368,plain, % 117.28/117.45 (~P12(f5(a4),f5(a4),a3)), % 117.28/117.45 inference(scs_inference,[],[73,6318,6296,6310,6322,86,149,142,39,161])). % 117.28/117.45 cnf(6370,plain, % 117.28/117.45 (~E(f5(a4),f9(a4))), % 117.28/117.45 inference(scs_inference,[],[73,6318,6296,6310,6322,6306,4084,86,149,142,39,161,47])). % 117.28/117.45 cnf(6371,plain, % 117.28/117.45 (~P1(f11(a4))), % 117.28/117.45 inference(scs_inference,[],[73,6318,6296,6310,6322,6306,4286,4084,164,86,149,142,39,161,47,91])). % 117.28/117.45 cnf(6373,plain, % 117.28/117.45 (~P15(f9(a4),f9(a4))), % 117.28/117.45 inference(scs_inference,[],[73,6318,6296,6310,6322,6306,4286,4084,164,86,149,142,39,161,47,91,160])). % 117.28/117.45 cnf(6375,plain, % 117.28/117.45 (~P14(f9(a4),a3)), % 117.28/117.45 inference(scs_inference,[],[73,6318,6296,6310,6322,6306,4286,4084,164,86,149,142,39,161,47,91,160,136])). % 117.28/117.45 cnf(6377,plain, % 117.28/117.45 (~P15(f9(a4),f5(a4))), % 117.28/117.45 inference(scs_inference,[],[73,6318,6296,6310,6322,6306,4286,4084,164,86,149,142,39,161,47,91,160,136,960])). % 117.28/117.45 cnf(6379,plain, % 117.28/117.45 (~P12(f9(a4),f5(a4),x63791)), % 117.28/117.45 inference(scs_inference,[],[73,6318,6296,6310,6322,6306,4286,4084,164,86,149,142,39,161,47,91,160,136,960,976])). % 117.28/117.45 cnf(6383,plain, % 117.28/117.45 (P15(f5(a4),f9(a4))), % 117.28/117.45 inference(scs_inference,[],[73,6318,6296,6310,6322,6306,4286,4084,164,86,149,142,39,161,47,91,160,136,960,976,743,135])). % 117.28/117.45 cnf(6387,plain, % 117.28/117.45 (~E(f5(a4),f10(a4))), % 117.28/117.45 inference(scs_inference,[],[73,6347,6318,6296,6310,6322,6306,4286,4084,164,86,149,142,39,161,47,91,160,136,960,976,743,135,88,38])). % 117.28/117.45 cnf(6389,plain, % 117.28/117.45 (~P12(x63891,f13(a3,a4),x63892)+~E(x63892,a3)), % 117.28/117.45 inference(scs_inference,[],[73,6347,6318,6296,6310,6322,6306,4286,4084,164,887,86,149,142,39,161,47,91,160,136,960,976,743,135,88,38,40])). % 117.28/117.45 cnf(6394,plain, % 117.28/117.45 (P9(f5(a4),f9(a4))), % 117.28/117.45 inference(scs_inference,[],[6383,94])). % 117.28/117.45 cnf(6396,plain, % 117.28/117.45 (P4(f10(a4))), % 117.28/117.45 inference(scs_inference,[],[6383,850,94,86])). % 117.28/117.45 cnf(6398,plain, % 117.28/117.45 (~E(f10(a4),f5(a4))), % 117.28/117.45 inference(scs_inference,[],[6377,6383,6349,850,94,86,63])). % 117.28/117.45 cnf(6399,plain, % 117.28/117.45 (~P12(x63991,f5(a4),f11(a4))), % 117.28/117.45 inference(scs_inference,[],[6377,6383,6349,6298,4286,850,94,86,63,142])). % 117.28/117.45 cnf(6401,plain, % 117.28/117.45 (~P11(x64011,f13(a3,a4),x64012)+~E(x64012,a3)), % 117.28/117.45 inference(scs_inference,[],[6377,6383,6349,6298,4286,888,850,94,86,63,142,45])). % 117.28/117.45 cnf(6406,plain, % 117.28/117.45 (P9(f5(a4),f10(a4))), % 117.28/117.45 inference(scs_inference,[],[6394,6357,105])). % 117.28/117.45 cnf(6412,plain, % 117.28/117.45 (P12(f5(a4),f9(a4),f11(a4))), % 117.28/117.45 inference(scs_inference,[],[6370,6394,6379,6308,6329,6337,6335,6357,4286,827,105,370,6290,153])). % 117.28/117.45 cnf(6415,plain, % 117.28/117.45 (~P14(f9(a4),f11(a4))), % 117.28/117.45 inference(scs_inference,[],[6370,6394,6379,6308,6329,6337,6335,6357,4286,827,105,370,6290,153,136])). % 117.28/117.45 cnf(6421,plain, % 117.28/117.45 (~P6(f10(a4),f11(a4))), % 117.28/117.45 inference(scs_inference,[],[6304,6371,90])). % 117.28/117.45 cnf(6427,plain, % 117.28/117.45 (P12(f9(a4),f10(a4),f11(a4))), % 117.28/117.45 inference(scs_inference,[],[73,6367,6406,6412,6304,6351,6292,6371,6337,6298,4286,90,99,104,158])). % 117.28/117.45 cnf(6429,plain, % 117.28/117.45 (P12(f5(a4),f10(a4),f11(a4))), % 117.28/117.45 inference(scs_inference,[],[73,6387,6367,6399,6406,6412,6304,6351,6292,6329,6371,6337,6298,4286,827,850,90,99,104,158,153])). % 117.28/117.45 cnf(6443,plain, % 117.28/117.45 (~P12(f10(a4),f5(a4),x64431)), % 117.28/117.45 inference(scs_inference,[],[6427,6429,137,976])). % 117.28/117.45 cnf(6445,plain, % 117.28/117.45 (~P14(f10(a4),f11(a4))), % 117.28/117.45 inference(scs_inference,[],[6427,6429,137,976,136])). % 117.28/117.45 cnf(6454,plain, % 117.28/117.45 (~E(f13(a3,a4),f10(a4))), % 117.28/117.45 inference(scs_inference,[],[6339,6316,58])). % 117.28/117.45 cnf(6455,plain, % 117.28/117.45 (~E(f13(a3,a4),f9(a4))), % 117.28/117.45 inference(scs_inference,[],[6365,6339,6316,6335,58,49])). % 117.28/117.45 cnf(6456,plain, % 117.28/117.45 (~P8(f13(a3,a4),a4)), % 117.28/117.45 inference(scs_inference,[],[73,6365,6339,6316,6363,6337,6298,6335,887,58,49,158])). % 117.28/117.45 cnf(6459,plain, % 117.28/117.45 (P12(f5(a4),f10(a4),a3)), % 117.28/117.45 inference(scs_inference,[],[73,6365,6339,6443,6398,6316,6363,6329,6304,6337,6298,6335,827,850,887,58,49,158,153])). % 117.28/117.45 cnf(6468,plain, % 117.28/117.45 (~P10(f13(a3,a4),a3)), % 117.28/117.45 inference(scs_inference,[],[73,6368,6421,6456,6318,6363,4286,39,47,126])). % 117.28/117.45 cnf(6505,plain, % 117.28/117.45 (P12(f10(a4),f10(a4),a3)+~P15(f10(a4),f10(a4))), % 117.28/117.45 inference(scs_inference,[],[6459,160])). % 117.28/117.45 cnf(6519,plain, % 117.28/117.45 (~P3(f13(a3,a4))+P12(f13(a3,a4),f10(a4),a3)), % 117.28/117.45 inference(scs_inference,[],[73,6454,6292,6318,144])). % 117.28/117.45 cnf(6522,plain, % 117.28/117.45 (~P3(f13(a3,a4))+P12(f13(a3,a4),f9(a4),a3)), % 117.28/117.45 inference(scs_inference,[],[73,6455,6308,6337,6318,887,153])). % 117.28/117.45 cnf(6620,plain, % 117.28/117.45 (~P14(f9(a4),x66201)+~E(x66201,a3)), % 117.28/117.45 inference(scs_inference,[],[6375,6399,40,59])). % 117.28/117.45 cnf(6656,plain, % 117.28/117.45 (~P14(x66561,f11(a4))+~E(x66561,f10(a4))), % 117.28/117.45 inference(scs_inference,[],[6445,58])). % 117.28/117.45 cnf(6661,plain, % 117.28/117.45 (~P14(f10(a4),x66611)+~E(x66611,a3)), % 117.28/117.45 inference(scs_inference,[],[6339,59])). % 117.28/117.45 cnf(6682,plain, % 117.28/117.45 (~E(f10(a4),x66821)+P6(x66821,f11(x66821))), % 117.28/117.45 inference(scs_inference,[],[6396,55,82,89])). % 117.28/117.45 cnf(6687,plain, % 117.28/117.45 (P6(f10(a4),f11(f10(a4)))), % 117.28/117.45 inference(equality_inference,[],[6682])). % 117.28/117.45 cnf(6855,plain, % 117.28/117.45 (~E(f9(a4),f13(a3,a4))), % 117.28/117.45 inference(scs_inference,[],[887,6363,39])). % 117.28/117.45 cnf(6923,plain, % 117.28/117.45 (~P3(f13(a3,a4))+P12(f13(a3,a4),f9(a4),f11(a4))+P12(f9(a4),f13(a3,a4),f11(a4))), % 117.28/117.45 inference(scs_inference,[],[6855,6337,6308,6318,4286,153])). % 117.28/117.45 cnf(7004,plain, % 117.28/117.45 (~P6(f10(a4),a3)), % 117.28/117.45 inference(scs_inference,[],[80,6304,90])). % 117.28/117.45 cnf(7814,plain, % 117.28/117.45 (~P3(f13(a3,a4))+P12(f13(a3,a4),f10(a4),f11(a4))), % 117.28/117.45 inference(scs_inference,[],[6318,6454,6292,4286,144])). % 117.28/117.45 cnf(8593,plain, % 117.28/117.45 (~P15(f10(a4),f10(a4))), % 117.28/117.45 inference(scs_inference,[],[6505,976])). % 117.28/117.45 cnf(8598,plain, % 117.28/117.45 (P15(f13(a3,a4),f10(a4))+~P3(f13(a3,a4))), % 117.28/117.45 inference(scs_inference,[],[6519,135])). % 117.28/117.45 cnf(8602,plain, % 117.28/117.45 (P15(f13(a3,a4),f10(a4))), % 117.28/117.45 inference(scs_inference,[],[6353,8598,81])). % 117.28/117.45 cnf(8603,plain, % 117.28/117.45 (P9(f13(a3,a4),f10(a4))), % 117.28/117.45 inference(scs_inference,[],[8602,94])). % 117.28/117.45 cnf(8607,plain, % 117.28/117.45 (~P9(f10(a4),f13(a3,a4))), % 117.28/117.45 inference(scs_inference,[],[8602,94,370,100])). % 117.28/117.45 cnf(8620,plain, % 117.28/117.45 (~P9(x86201,f13(a3,a4))+~P9(f10(a4),x86201)), % 117.28/117.45 inference(scs_inference,[],[8607,105])). % 117.28/117.45 cnf(8645,plain, % 117.28/117.45 (~P9(x86451,f13(a3,a4))+~P15(f10(a4),x86451)), % 117.28/117.45 inference(scs_inference,[],[8620,94])). % 117.28/117.45 cnf(8664,plain, % 117.28/117.45 (~P15(x86641,f13(a3,a4))+~P15(f10(a4),x86641)), % 117.28/117.45 inference(scs_inference,[],[8645,94])). % 117.28/117.45 cnf(8666,plain, % 117.28/117.45 (~P12(x86661,f13(a3,a4),x86662)+~P15(f10(a4),x86661)), % 117.28/117.45 inference(scs_inference,[],[8664,135])). % 117.28/117.45 cnf(8696,plain, % 117.28/117.45 (~P12(x86961,f13(a3,a4),x86962)+~P12(f10(a4),x86961,x86963)), % 117.28/117.45 inference(scs_inference,[],[8666,135])). % 117.28/117.45 cnf(8699,plain, % 117.28/117.45 (~P3(f13(a3,a4))+P13(f9(a4),f17(a3,f13(a3,a4),f9(a4)))), % 117.28/117.45 inference(scs_inference,[],[6522,154])). % 117.28/117.45 cnf(8833,plain, % 117.28/117.45 (~P12(x88331,f13(a3,a4),x88332)+~P11(f10(a4),x88331,x88333)), % 117.28/117.45 inference(scs_inference,[],[8696,149])). % 117.28/117.45 cnf(8916,plain, % 117.28/117.45 (~P3(f13(a3,a4))+P12(f13(a3,a4),f9(a4),f11(a4))+~P11(f10(a4),f9(a4),x89161)), % 117.28/117.45 inference(scs_inference,[],[6318,6337,6308,4286,6855,8833,153])). % 117.28/117.45 cnf(9027,plain, % 117.28/117.45 (P12(f13(a3,a4),f10(a4),f11(a4))), % 117.28/117.45 inference(scs_inference,[],[6353,7814,81])). % 117.28/117.45 cnf(9211,plain, % 117.28/117.45 (P5(f13(a3,a4),x92111)+~E(f12(a3,f13(a3,a4)),x92111)), % 117.28/117.45 inference(scs_inference,[],[6316,65,111])). % 117.28/117.45 cnf(9212,plain, % 117.28/117.45 (P5(f13(a3,a4),f12(a3,f13(a3,a4)))), % 117.28/117.45 inference(equality_inference,[],[9211])). % 117.28/117.45 cnf(9438,plain, % 117.28/117.45 (P3(f13(a3,a4))), % 117.28/117.45 inference(scs_inference,[],[6353,81])). % 117.28/117.45 cnf(9441,plain, % 117.28/117.45 (P12(f13(a3,a4),f9(a4),a3)), % 117.28/117.45 inference(scs_inference,[],[6353,81,8916,6522])). % 117.28/117.45 cnf(9448,plain, % 117.28/117.45 (P12(f13(a3,a4),f10(a4),a3)), % 117.28/117.45 inference(scs_inference,[],[9438,6519])). % 117.28/117.45 cnf(9453,plain, % 117.28/117.45 (P12(f9(a4),f13(a3,a4),f11(a4))+P12(f13(a3,a4),f9(a4),f11(a4))), % 117.28/117.45 inference(scs_inference,[],[9438,6923])). % 117.28/117.45 cnf(9458,plain, % 117.28/117.45 (P13(f9(a4),f17(a3,f13(a3,a4),f9(a4)))), % 117.28/117.45 inference(scs_inference,[],[9438,8699])). % 117.28/117.45 cnf(9465,plain, % 117.28/117.45 (~P12(f9(a4),f13(a3,a4),x94651)), % 117.28/117.45 inference(scs_inference,[],[9441,6373,960,135,743,976])). % 117.28/117.45 cnf(9469,plain, % 117.28/117.45 (P12(f13(a3,a4),f9(a4),f11(a4))), % 117.28/117.45 inference(scs_inference,[],[9438,9441,6373,6371,960,135,743,976,90,9453])). % 117.28/117.45 cnf(9474,plain, % 117.28/117.45 (P15(f13(a3,a4),f9(a4))), % 117.28/117.45 inference(scs_inference,[],[9469,135])). % 117.28/117.45 cnf(9502,plain, % 117.28/117.45 (~P11(f13(a3,a4),f10(a4),f11(a4))), % 117.28/117.45 inference(scs_inference,[],[9474,9469,6427,6306,83,94,161])). % 117.28/117.45 cnf(9550,plain, % 117.28/117.45 (~P11(f5(a4),f5(a4),x95501)+~E(x95501,a3)), % 117.28/117.45 inference(scs_inference,[],[6368,149,45])). % 117.28/117.45 cnf(9826,plain, % 117.28/117.45 (P13(f5(a4),f17(f11(a4),f5(a4),f10(a4)))), % 117.28/117.45 inference(scs_inference,[],[9212,6429,1312,1319,6335,103,106,108,110,992,6620,6661,4,155])). % 117.28/117.45 cnf(9848,plain, % 117.28/117.45 (E(f12(a3,x98481),f12(f6(f5(a4),a4),x98481))), % 117.28/117.45 inference(scs_inference,[],[9212,6316,6429,1312,1319,6335,103,106,108,110,992,6620,6661,4,155,157,871,5674,6656,14,15,16,17,18,19,20,21,22,23,24,29,30,31])). % 117.28/117.45 cnf(9863,plain, % 117.28/117.45 (E(f12(x98631,f13(a3,x98632)),f12(x98631,f13(f19(f10(a4),a4),x98632)))), % 117.28/117.45 inference(rename_variables,[],[5546])). % 117.28/117.45 cnf(9876,plain, % 117.28/117.45 (P12(f7(f5(a4),f10(a4),f11(a4)),f10(a4),f11(a4))), % 117.28/117.45 inference(scs_inference,[],[9212,9458,5546,6300,6316,6429,9027,9448,1312,1319,6292,6335,103,106,108,110,992,6620,6661,4,155,157,871,5674,6656,14,15,16,17,18,19,20,21,22,23,24,29,30,31,32,34,36,2916,6389,5055,5,6,7,1009,1043,9211,2900,112,291,156,89,130,159])). % 117.28/117.45 cnf(9881,plain, % 117.28/117.45 (P5(f13(a3,a4),f12(f6(f5(a4),a4),f13(a3,a4)))), % 117.28/117.45 inference(scs_inference,[],[9212,9458,5578,5546,6300,6316,6429,9027,9448,1312,1319,6292,6335,103,106,108,110,992,6620,6661,4,155,157,871,5674,6656,14,15,16,17,18,19,20,21,22,23,24,29,30,31,32,34,36,2916,6389,5055,5,6,7,1009,1043,9211,2900,112,291,156,89,130,159,2,149,65])). % 117.28/117.45 cnf(9882,plain, % 117.28/117.45 (P8(f10(a4),f16(f10(a4),f19(f10(a4),a4)))), % 117.28/117.45 inference(scs_inference,[],[9212,9458,5578,5546,1088,6300,6316,6429,9027,9448,1312,1319,6292,6335,103,106,108,110,992,6620,6661,4,155,157,871,5674,6656,14,15,16,17,18,19,20,21,22,23,24,29,30,31,32,34,36,2916,6389,5055,5,6,7,1009,1043,9211,2900,112,291,156,89,130,159,2,149,65,115])). % 117.28/117.45 cnf(9886,plain, % 117.28/117.45 (P12(f8(f13(a3,a4),f10(a4),f11(a4)),f10(a4),f11(a4))), % 117.28/117.45 inference(scs_inference,[],[9212,9458,5578,5546,1321,1088,9502,6300,6316,6429,9027,9448,1309,1312,1319,6292,6335,103,106,108,110,992,6620,6661,4,155,157,871,5674,6656,14,15,16,17,18,19,20,21,22,23,24,29,30,31,32,34,36,2916,6389,5055,5,6,7,1009,1043,9211,2900,112,291,156,89,130,159,2,149,65,115,117,163])). % 117.28/117.45 cnf(9891,plain, % 117.28/117.45 (~P6(a4,f18(f7(f5(a4),f10(a4),f11(a4)),f12(f11(a4),f7(f5(a4),f10(a4),f11(a4)))))), % 117.28/117.45 inference(scs_inference,[],[9212,9458,5578,5546,1321,1088,9502,6300,6415,6316,6429,9027,9448,164,1309,1312,1319,6292,6335,103,106,108,110,992,6620,6661,4,155,157,871,5674,6656,14,15,16,17,18,19,20,21,22,23,24,29,30,31,32,34,36,2916,6389,5055,5,6,7,1009,1043,9211,2900,112,291,156,89,130,159,2,149,65,115,117,163,58,162,91])). % 117.28/117.45 cnf(9893,plain, % 117.28/117.45 (P12(f9(a4),f20(f9(a4),a3),a3)), % 117.28/117.45 inference(scs_inference,[],[6341,9212,9458,5578,5546,1321,1088,9502,6300,6415,6316,6429,9027,9448,9441,164,1309,1312,1319,6292,6335,103,106,108,110,992,6620,6661,4,155,157,871,5674,6656,14,15,16,17,18,19,20,21,22,23,24,29,30,31,32,34,36,2916,6389,5055,5,6,7,1009,1043,9211,2900,112,291,156,89,130,159,2,149,65,115,117,163,58,162,91,152])). % 117.28/117.45 cnf(9897,plain, % 117.28/117.45 (P6(f16(f10(a4),f19(f10(a4),a4)),f19(f10(a4),a4))), % 117.28/117.45 inference(scs_inference,[],[6341,9212,9458,5578,5546,1321,1088,9502,6300,6415,6316,6429,9027,9448,9441,164,1309,1312,1319,6292,6335,103,106,108,110,992,6620,6661,4,155,157,871,5674,6656,14,15,16,17,18,19,20,21,22,23,24,29,30,31,32,34,36,2916,6389,5055,5,6,7,1009,1043,9211,2900,112,291,156,89,130,159,2,149,65,115,117,163,58,162,91,152,118,116])). % 117.28/117.45 cnf(9899,plain, % 117.28/117.45 (P12(f13(a3,a4),f20(f13(a3,a4),a3),a3)), % 117.28/117.45 inference(scs_inference,[],[6341,6468,9212,9458,5578,5546,1321,1088,9502,6300,6415,6316,6429,9027,9448,9441,164,1309,1312,1319,6292,6335,103,106,108,110,992,6620,6661,4,155,157,871,5674,6656,14,15,16,17,18,19,20,21,22,23,24,29,30,31,32,34,36,2916,6389,5055,5,6,7,1009,1043,9211,2900,112,291,156,89,130,159,2,149,65,115,117,163,58,162,91,152,118,116,140])). % 117.28/117.45 cnf(9904,plain, % 117.28/117.45 (~P16(f9(f17(a3,f13(a3,a4),f10(a4))),a4)), % 117.28/117.45 inference(scs_inference,[],[6341,6468,6687,9212,9458,5578,5546,1321,1088,9502,6300,6375,6415,6316,6429,9027,9448,9441,164,1309,1312,1319,1086,6292,6335,6304,73,103,106,108,110,992,6620,6661,4,155,157,871,5674,6656,14,15,16,17,18,19,20,21,22,23,24,29,30,31,32,34,36,2916,6389,5055,5,6,7,1009,1043,9211,2900,112,291,156,89,130,159,2,149,65,115,117,163,58,162,91,152,118,116,140,90,59,142])). % 117.28/117.45 cnf(9909,plain, % 117.28/117.45 (E(f12(x99091,f13(a3,x99092)),f12(x99091,f13(f19(f10(a4),a4),x99092)))), % 117.28/117.45 inference(rename_variables,[],[5546])). % 117.28/117.45 cnf(9918,plain, % 117.28/117.45 (E(f18(f11(a3),x99181),f18(f11(f19(f10(a4),a4)),x99181))), % 117.28/117.45 inference(rename_variables,[],[5322])). % 117.28/117.45 cnf(9920,plain, % 117.28/117.45 (P13(f7(f5(a4),f10(a4),f11(a4)),a4)), % 117.28/117.45 inference(scs_inference,[],[6333,6341,6468,6687,9212,9458,1578,5578,5338,5546,9863,5322,1321,1088,6421,9502,6300,6375,6415,6316,6429,9027,9448,9441,164,1309,1312,1319,1086,887,6292,6335,850,6304,4286,73,103,106,108,110,992,6620,6661,4,155,157,871,5674,6656,14,15,16,17,18,19,20,21,22,23,24,29,30,31,32,34,36,2916,6389,5055,5,6,7,1009,1043,9211,2900,112,291,156,89,130,159,2,149,65,115,117,163,58,162,91,152,118,116,140,90,59,142,161,66,39,51,143,54,3,47,150])). % 117.28/117.45 cnf(9922,plain, % 117.28/117.45 (P16(f13(f6(f5(a4),a4),a4),a4)), % 117.28/117.45 inference(scs_inference,[],[6333,6341,6468,6687,9212,9458,1578,5578,5338,5546,9863,5322,1321,1088,6421,9502,6300,6375,6415,6316,6429,9027,9448,9441,164,1309,1312,1319,1086,887,6292,6335,850,6304,4286,73,103,106,108,110,992,6620,6661,4,155,157,871,5674,6656,14,15,16,17,18,19,20,21,22,23,24,29,30,31,32,34,36,2916,6389,5055,5,6,7,1009,1043,9211,2900,112,291,156,89,130,159,2,149,65,115,117,163,58,162,91,152,118,116,140,90,59,142,161,66,39,51,143,54,3,47,150,125])). % 117.28/117.45 cnf(9934,plain, % 117.28/117.45 (P6(f7(f5(a4),f10(a4),f11(a4)),f18(f7(f5(a4),f10(a4),f11(a4)),f12(f11(a4),f7(f5(a4),f10(a4),f11(a4)))))), % 117.28/117.45 inference(scs_inference,[],[6333,6341,6468,6687,9212,9458,1578,5578,5338,5546,9863,5322,1321,1088,6421,9502,6300,6375,6415,6316,6429,9027,9448,9441,164,1309,9465,1312,9438,1319,1086,6855,887,6292,6335,850,6337,6308,6304,4286,73,6318,103,106,108,110,992,6620,6661,4,155,157,871,5674,6656,14,15,16,17,18,19,20,21,22,23,24,29,30,31,32,34,36,2916,6389,5055,5,6,7,1009,1043,9211,2900,112,291,156,89,130,159,2,149,65,115,117,163,58,162,91,152,118,116,140,90,59,142,161,66,39,51,143,54,3,47,150,125,153,911,8,9,13,154,1060])). % 117.28/117.45 cnf(9937,plain, % 117.28/117.45 (E(f13(a3,x99371),f13(f6(f5(a4),a4),x99371))), % 117.28/117.45 inference(scs_inference,[],[6333,6341,6468,6687,9212,9458,1578,5578,5338,5546,9863,5322,1321,1088,6421,9502,6300,6375,6415,6316,6429,9027,9448,9441,164,1309,9465,1312,9438,1319,1086,6855,887,6292,6335,850,6337,6308,6304,4286,73,6318,103,106,108,110,992,6620,6661,4,155,157,871,5674,6656,14,15,16,17,18,19,20,21,22,23,24,29,30,31,32,34,36,2916,6389,5055,5,6,7,1009,1043,9211,2900,112,291,156,89,130,159,2,149,65,115,117,163,58,162,91,152,118,116,140,90,59,142,161,66,39,51,143,54,3,47,150,125,153,911,8,9,13,154,1060,25,33])). % 117.28/117.45 cnf(9956,plain, % 117.28/117.45 (P17(f12(f6(f5(a4),a4),f13(a3,a4)),f19(f10(a4),a4))), % 117.28/117.45 inference(scs_inference,[],[6333,6341,6468,6687,9212,9458,1578,5578,5338,5546,9863,9909,5322,1321,1088,6421,9502,6300,6375,6294,6415,6316,6429,9027,9448,9441,164,1309,9465,1312,9438,1319,1086,6855,887,6292,6335,850,6337,6308,6304,4286,73,6318,103,106,108,110,992,6620,6661,4,155,157,871,5674,6656,14,15,16,17,18,19,20,21,22,23,24,29,30,31,32,34,36,2916,6389,5055,5,6,7,1009,1043,9211,2900,112,291,156,89,130,159,2,149,65,115,117,163,58,162,91,152,118,116,140,90,59,142,161,66,39,51,143,54,3,47,150,125,153,911,8,9,13,154,1060,25,33,35,6401,9550,10,11,12,26,27,28,1555,1572,1026,4088,4091,1573])). % 117.28/117.45 cnf(9972,plain, % 117.28/117.45 (P14(f5(a4),f6(f5(a4),a4))), % 117.28/117.45 inference(scs_inference,[],[6333,6341,6468,6687,9212,9458,1578,5578,5338,5546,9863,9909,5322,1321,1088,6421,9502,6300,6375,6294,6415,6316,6429,9027,9448,9441,164,1309,9465,1312,9438,1319,1086,6855,887,6292,6298,6335,850,6337,6308,6304,4286,73,6318,103,106,108,110,992,6620,6661,4,155,157,871,5674,6656,14,15,16,17,18,19,20,21,22,23,24,29,30,31,32,34,36,2916,6389,5055,5,6,7,1009,1043,9211,2900,112,291,156,89,130,159,2,149,65,115,117,163,58,162,91,152,118,116,140,90,59,142,161,66,39,51,143,54,3,47,150,125,153,911,8,9,13,154,1060,25,33,35,6401,9550,10,11,12,26,27,28,1555,1572,1026,4088,4091,1573,5241,4183,4159,5053,4194,4231,4232,87,759,275,109])). % 117.28/117.45 cnf(9980,plain, % 117.28/117.45 (P4(f17(f11(a4),f5(a4),f10(a4)))), % 117.28/117.45 inference(scs_inference,[],[6333,6341,6468,6687,9212,9458,1578,5578,5338,5546,9863,9909,5322,1321,1088,6421,9502,6300,6375,6294,6415,6316,6429,9027,9448,9441,164,1309,9465,1312,9438,1319,1086,6855,887,6292,6298,6335,850,6337,6308,6304,4286,73,6318,103,106,108,110,992,6620,6661,4,155,157,871,5674,6656,14,15,16,17,18,19,20,21,22,23,24,29,30,31,32,34,36,2916,6389,5055,5,6,7,1009,1043,9211,2900,112,291,156,89,130,159,2,149,65,115,117,163,58,162,91,152,118,116,140,90,59,142,161,66,39,51,143,54,3,47,150,125,153,911,8,9,13,154,1060,25,33,35,6401,9550,10,11,12,26,27,28,1555,1572,1026,4088,4091,1573,5241,4183,4159,5053,4194,4231,4232,87,759,275,109,135,85,370,84])). % 117.28/117.45 cnf(9986,plain, % 117.28/117.45 (~P12(x99861,f7(f5(a4),f10(a4),f11(a4)),f11(a4))), % 117.28/117.45 inference(scs_inference,[],[6333,6341,6468,6687,9212,9458,1578,5578,5338,5546,9863,9909,5322,1321,1088,6421,9502,6300,6375,6294,6415,6316,6429,9027,9448,9441,164,1309,9465,1312,9438,1319,1086,6855,887,6292,6298,6335,850,6337,6308,6304,4286,73,6318,103,106,108,110,992,6620,6661,4,155,157,871,5674,6656,14,15,16,17,18,19,20,21,22,23,24,29,30,31,32,34,36,2916,6389,5055,5,6,7,1009,1043,9211,2900,112,291,156,89,130,159,2,149,65,115,117,163,58,162,91,152,118,116,140,90,59,142,161,66,39,51,143,54,3,47,150,125,153,911,8,9,13,154,1060,25,33,35,6401,9550,10,11,12,26,27,28,1555,1572,1026,4088,4091,1573,5241,4183,4159,5053,4194,4231,4232,87,759,275,109,135,85,370,84,743,129,136])). % 117.28/117.45 cnf(9997,plain, % 117.28/117.45 (P13(f9(a4),f17(f6(f5(a4),a4),f13(a3,a4),f9(a4)))), % 117.28/117.45 inference(scs_inference,[],[6333,6341,6468,6687,9212,9458,1578,5578,5338,5546,9863,9909,5322,9918,1321,1088,6421,9502,6300,6375,6294,6415,6316,6429,9027,9448,9441,164,1309,9465,1312,9438,1319,1086,6855,887,6292,6298,6335,850,6337,6308,6304,4286,73,6318,103,106,108,110,992,6620,6661,4,155,157,871,5674,6656,14,15,16,17,18,19,20,21,22,23,24,29,30,31,32,34,36,2916,6389,5055,5,6,7,1009,1043,9211,2900,112,291,156,89,130,159,2,149,65,115,117,163,58,162,91,152,118,116,140,90,59,142,161,66,39,51,143,54,3,47,150,125,153,911,8,9,13,154,1060,25,33,35,6401,9550,10,11,12,26,27,28,1555,1572,1026,4088,4091,1573,5241,4183,4159,5053,4194,4231,4232,87,759,275,109,135,85,370,84,743,129,136,86,976,81,5690,57])). % 117.28/117.45 cnf(10004,plain, % 117.28/117.45 (~P8(f17(f11(a4),f5(a4),f10(a4)),a4)), % 117.28/117.45 inference(scs_inference,[],[6333,6341,6468,6687,9212,9458,1578,5578,5338,5546,9863,9909,5322,9918,7004,1321,1088,6421,2933,9502,6300,6375,6294,6415,6368,6316,6429,9027,9448,9441,164,1309,9465,1312,1571,9438,1319,1086,6855,1079,887,6292,6298,6335,850,6337,6308,6304,4286,73,6318,103,106,108,110,992,6620,6661,4,155,157,871,5674,6656,14,15,16,17,18,19,20,21,22,23,24,29,30,31,32,34,36,2916,6389,5055,5,6,7,1009,1043,9211,2900,112,291,156,89,130,159,2,149,65,115,117,163,58,162,91,152,118,116,140,90,59,142,161,66,39,51,143,54,3,47,150,125,153,911,8,9,13,154,1060,25,33,35,6401,9550,10,11,12,26,27,28,1555,1572,1026,4088,4091,1573,5241,4183,4159,5053,4194,4231,4232,87,759,275,109,135,85,370,84,743,129,136,86,976,81,5690,57,40,45,48,67,114,124])). % 117.28/117.45 cnf(10153,plain, % 117.28/117.45 (E(f13(a3,x101531),f13(f6(f5(a4),a4),x101531))), % 117.28/117.45 inference(rename_variables,[],[9937])). % 117.28/117.45 cnf(10160,plain, % 117.28/117.45 (E(f13(a3,x101601),f13(f6(f5(a4),a4),x101601))), % 117.28/117.45 inference(rename_variables,[],[9937])). % 117.28/117.45 cnf(10162,plain, % 117.28/117.45 (E(f13(a3,x101621),f13(f6(f5(a4),a4),x101621))), % 117.28/117.45 inference(rename_variables,[],[9937])). % 117.28/117.45 cnf(10167,plain, % 117.28/117.45 (~P12(f10(a4),x101671,a3)), % 117.28/117.45 inference(scs_inference,[],[73,168,6306,6335,6292,1079,80,6454,1086,1319,6427,6363,6353,6294,8593,6421,6687,6361,5338,6333,8603,9848,9937,10153,10160,9922,9897,9934,9882,9826,9920,9997,9876,9886,9893,9899,9972,9891,9980,9881,2,159,976,86,136,156,89,84,743,82,85,135,291,960,112,109,275,83,759,1043,6,22,34,8,28,20,25,29,6389,12,36,6401,32,111,113,992,5,11,14,21,23,26,27,31,35,154,155,4088,103,18,87,871,10,13,15,30,6661,1572,9,4159,4194,108,5055,1009,17,19,24,9550,157,1026,4,7,16,33,5674,5053,110,1555,4109,5241,106,1060,37,52,47,62,102,67,60,3,54,48,45,40,143])). % 117.28/117.45 cnf(10186,plain, % 117.28/117.45 (P12(f10(a4),f14(f10(a4),f10(a4)),a3)), % 117.28/117.45 inference(scs_inference,[],[73,168,6306,6304,6298,6335,6292,1079,80,6454,1086,1319,9438,6427,6363,6353,9441,6316,6310,1321,6294,8593,6421,6687,6361,5338,5546,6333,6351,8603,9848,9937,10153,10160,10162,9922,9897,9934,9882,9826,9920,9997,9876,9886,9893,9899,9986,9972,9891,9956,9980,9904,10004,9881,2,159,976,86,136,156,89,84,743,82,85,135,291,960,112,109,275,83,759,1043,6,22,34,8,28,20,25,29,6389,12,36,6401,32,111,113,992,5,11,14,21,23,26,27,31,35,154,155,4088,103,18,87,871,10,13,15,30,6661,1572,9,4159,4194,108,5055,1009,17,19,24,9550,157,1026,4,7,16,33,5674,5053,110,1555,4109,5241,106,1060,37,52,47,62,102,67,60,3,54,48,45,40,143,51,39,66,49,161,59,142,99,90,41,151])). % 117.28/117.45 cnf(10243,plain, % 117.28/117.45 ($false), % 117.28/117.45 inference(scs_inference,[],[10186,10167]), % 117.28/117.45 ['proof']). % 117.28/117.45 % SZS output end Proof % 117.28/117.45 % Total time :116.620000s %------------------------------------------------------------------------------