%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : PRO009+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 : n023.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:43 EDT 2024 % Result : Theorem 58.69s 58.82s % Output : CNFRefutation 58.69s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.10 % Problem : PRO009+2 : TPTP v8.2.0. Released v4.0.0. % 0.00/0.10 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.09/0.30 % Computer : n023.cluster.edu % 0.09/0.30 % Model : x86_64 x86_64 % 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.30 % Memory : 8042.1875MB % 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.30 % CPULimit : 300 % 0.09/0.30 % WCLimit : 300 % 0.09/0.30 % DateTime : Thu Jun 20 06:41:09 EDT 2024 % 0.09/0.30 % CPUTime : % 0.15/0.53 start to proof:theBenchmark % 58.69/58.80 %------------------------------------------- % 58.69/58.80 % File :CSE---1.7 % 58.69/58.80 % Problem :theBenchmark % 58.69/58.80 % Transform :cnf % 58.69/58.80 % Format :tptp:raw % 58.69/58.80 % Command :java -jar mcs_scs.jar %d %s % 58.69/58.80 % 58.69/58.80 % Result :Theorem 58.160000s % 58.69/58.80 % Output :CNFRefutation 58.160000s % 58.69/58.80 %------------------------------------------- % 58.69/58.80 %------------------------------------------------------------------------------ % 58.69/58.80 % File : PRO009+2 : TPTP v8.2.0. Released v4.0.0. % 58.69/58.80 % Domain : Processes % 58.69/58.80 % Problem : PSL cliff problem coe-7.1.2 % 58.69/58.80 % Version : Especial : Reduced > Especial. % 58.69/58.81 % English : % 58.69/58.81 % Refs : [Hal09] Halcomb (2009), Email to G. Sutcliffe % 58.69/58.81 % Source : [Hal09] % 58.69/58.81 % Names : minimal-subset-p9__coe-7.1.2-pd [Hal09] % 58.69/58.81 % 58.69/58.81 % Status : Theorem % 58.69/58.81 % Rating : 0.19 v8.2.0, 0.17 v7.5.0, 0.19 v7.4.0, 0.13 v7.3.0, 0.14 v7.2.0, 0.10 v7.1.0, 0.09 v7.0.0, 0.07 v6.4.0, 0.12 v6.3.0, 0.08 v6.2.0, 0.12 v6.1.0, 0.13 v5.5.0, 0.19 v5.4.0, 0.21 v5.3.0, 0.30 v5.2.0, 0.15 v5.1.0, 0.19 v5.0.0, 0.21 v4.1.0, 0.26 v4.0.0 % 58.69/58.81 % Syntax : Number of formulae : 46 ( 12 unt; 0 def) % 58.69/58.81 % Number of atoms : 137 ( 10 equ) % 58.69/58.81 % Maximal formula atoms : 9 ( 2 avg) % 58.69/58.81 % Number of connectives : 108 ( 17 ~; 5 |; 51 &) % 58.69/58.81 % ( 7 <=>; 28 =>; 0 <=; 0 <~>) % 58.69/58.81 % Maximal formula depth : 12 ( 5 avg) % 58.69/58.81 % Maximal term depth : 1 ( 1 avg) % 58.69/58.81 % Number of predicates : 18 ( 17 usr; 0 prp; 1-3 aty) % 58.69/58.81 % Number of functors : 5 ( 5 usr; 5 con; 0-0 aty) % 58.69/58.81 % Number of variables : 102 ( 81 !; 21 ?) % 58.69/58.81 % SPC : FOF_THM_RFO_SEQ % 58.69/58.81 % 58.69/58.81 % Comments : % 58.69/58.81 %------------------------------------------------------------------------------ % 58.69/58.81 fof(sos,axiom, % 58.69/58.81 ! [X0,X1,X2,X3] : % 58.69/58.81 ( ( min_precedes(X0,X1,X3) % 58.69/58.81 & min_precedes(X1,X2,X3) ) % 58.69/58.81 => min_precedes(X0,X2,X3) ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_01,axiom, % 58.69/58.81 ! [X4,X5,X6] : % 58.69/58.81 ( ( earlier(X4,X5) % 58.69/58.81 & earlier(X5,X6) ) % 58.69/58.81 => earlier(X4,X6) ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_02,axiom, % 58.69/58.81 ! [X7,X8,X9,X10] : % 58.69/58.81 ( ( occurrence_of(X9,X10) % 58.69/58.81 & root_occ(X7,X9) % 58.69/58.81 & root_occ(X8,X9) ) % 58.69/58.81 => X7 = X8 ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_03,axiom, % 58.69/58.81 ! [X11,X12,X13,X14] : % 58.69/58.81 ( ( occurrence_of(X13,X14) % 58.69/58.81 & ~ atomic(X14) % 58.69/58.81 & leaf_occ(X11,X13) % 58.69/58.81 & leaf_occ(X12,X13) ) % 58.69/58.81 => X11 = X12 ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_04,axiom, % 58.69/58.81 ! [X15,X16,X17] : % 58.69/58.81 ( next_subocc(X15,X16,X17) % 58.69/58.81 <=> ( min_precedes(X15,X16,X17) % 58.69/58.81 & ~ ? [X18] : % 58.69/58.81 ( min_precedes(X15,X18,X17) % 58.69/58.81 & min_precedes(X18,X16,X17) ) ) ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_05,axiom, % 58.69/58.81 ! [X19,X20,X21] : % 58.69/58.81 ( next_subocc(X19,X20,X21) % 58.69/58.81 => ( arboreal(X19) % 58.69/58.81 & arboreal(X20) ) ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_06,axiom, % 58.69/58.81 ! [X22,X23,X24] : % 58.69/58.81 ( min_precedes(X22,X23,X24) % 58.69/58.81 => precedes(X22,X23) ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_07,axiom, % 58.69/58.81 ! [X25,X26,X27] : % 58.69/58.81 ( min_precedes(X25,X26,X27) % 58.69/58.81 => ~ root(X26,X27) ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_08,axiom, % 58.69/58.81 ! [X28,X29] : % 58.69/58.81 ( precedes(X28,X29) % 58.69/58.81 <=> ( earlier(X28,X29) % 58.69/58.81 & legal(X29) ) ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_09,axiom, % 58.69/58.81 ! [X30,X31] : % 58.69/58.81 ( earlier(X30,X31) % 58.69/58.81 => ~ earlier(X31,X30) ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_10,axiom, % 58.69/58.81 ! [X32,X33] : % 58.69/58.81 ( root_occ(X32,X33) % 58.69/58.81 <=> ? [X34] : % 58.69/58.81 ( occurrence_of(X33,X34) % 58.69/58.81 & subactivity_occurrence(X32,X33) % 58.69/58.81 & root(X32,X34) ) ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_11,axiom, % 58.69/58.81 ! [X35,X36] : % 58.69/58.81 ( leaf_occ(X35,X36) % 58.69/58.81 <=> ? [X37] : % 58.69/58.81 ( occurrence_of(X36,X37) % 58.69/58.81 & subactivity_occurrence(X35,X36) % 58.69/58.81 & leaf(X35,X37) ) ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_12,axiom, % 58.69/58.81 ! [X38,X39] : % 58.69/58.81 ( root(X38,X39) % 58.69/58.81 => legal(X38) ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_13,axiom, % 58.69/58.81 ! [X40,X41] : % 58.69/58.81 ( occurrence_of(X40,X41) % 58.69/58.81 => ( arboreal(X40) % 58.69/58.81 <=> atomic(X41) ) ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_14,axiom, % 58.69/58.81 ! [X42,X43] : % 58.69/58.81 ( leaf(X42,X43) % 58.69/58.81 <=> ( ( root(X42,X43) % 58.69/58.81 | ? [X44] : min_precedes(X44,X42,X43) ) % 58.69/58.81 & ~ ? [X45] : min_precedes(X42,X45,X43) ) ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_15,axiom, % 58.69/58.81 ! [X46,X47] : % 58.69/58.81 ( atocc(X46,X47) % 58.69/58.81 <=> ? [X48] : % 58.69/58.81 ( subactivity(X47,X48) % 58.69/58.81 & atomic(X48) % 58.69/58.81 & occurrence_of(X46,X48) ) ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_16,axiom, % 58.69/58.81 ! [X49,X50] : % 58.69/58.81 ( ( atocc(X49,X50) % 58.69/58.81 & legal(X49) ) % 58.69/58.81 => root(X49,X50) ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_17,axiom, % 58.69/58.81 ! [X51] : % 58.69/58.81 ( legal(X51) % 58.69/58.81 => arboreal(X51) ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_18,axiom, % 58.69/58.81 ! [X52] : % 58.69/58.81 ( activity_occurrence(X52) % 58.69/58.81 => ? [X53] : % 58.69/58.81 ( activity(X53) % 58.69/58.81 & occurrence_of(X52,X53) ) ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_19,axiom, % 58.69/58.81 ! [X54,X55] : % 58.69/58.81 ( subactivity_occurrence(X54,X55) % 58.69/58.81 => ( activity_occurrence(X54) % 58.69/58.81 & activity_occurrence(X55) ) ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_20,axiom, % 58.69/58.81 ! [X56,X57,X58] : % 58.69/58.81 ( ( occurrence_of(X56,X58) % 58.69/58.81 & root_occ(X57,X56) ) % 58.69/58.81 => ~ ? [X59] : min_precedes(X59,X57,X58) ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_21,axiom, % 58.69/58.81 ! [X60,X61,X62] : % 58.69/58.81 ( ( occurrence_of(X60,X62) % 58.69/58.81 & leaf_occ(X61,X60) ) % 58.69/58.81 => ~ ? [X63] : min_precedes(X61,X63,X62) ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_22,axiom, % 58.69/58.81 ! [X64,X65,X66] : % 58.69/58.81 ( ( occurrence_of(X64,X65) % 58.69/58.81 & occurrence_of(X64,X66) ) % 58.69/58.81 => X65 = X66 ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_23,axiom, % 58.69/58.81 ! [X67,X68] : % 58.69/58.81 ( ( leaf(X67,X68) % 58.69/58.81 & ~ atomic(X68) ) % 58.69/58.81 => ? [X69] : % 58.69/58.81 ( occurrence_of(X69,X68) % 58.69/58.81 & leaf_occ(X67,X69) ) ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_24,axiom, % 58.69/58.81 ! [X70,X71,X72] : % 58.69/58.81 ( min_precedes(X71,X72,X70) % 58.69/58.81 => ? [X73] : % 58.69/58.81 ( occurrence_of(X73,X70) % 58.69/58.81 & subactivity_occurrence(X71,X73) % 58.69/58.81 & subactivity_occurrence(X72,X73) ) ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_25,axiom, % 58.69/58.81 ! [X74,X75] : % 58.69/58.81 ( ( leaf(X74,X75) % 58.69/58.81 & ~ atomic(X75) ) % 58.69/58.81 => ? [X76] : % 58.69/58.81 ( occurrence_of(X76,X75) % 58.69/58.81 & leaf_occ(X74,X76) ) ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_26,axiom, % 58.69/58.81 ! [X77,X78,X79] : % 58.69/58.81 ( min_precedes(X78,X79,X77) % 58.69/58.81 => ? [X80,X81] : % 58.69/58.81 ( subactivity(X80,X77) % 58.69/58.81 & subactivity(X81,X77) % 58.69/58.81 & atocc(X78,X80) % 58.69/58.81 & atocc(X79,X81) ) ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_27,axiom, % 58.69/58.81 ! [X82,X83] : % 58.69/58.81 ( root(X83,X82) % 58.69/58.81 => ? [X84] : % 58.69/58.81 ( subactivity(X84,X82) % 58.69/58.81 & atocc(X83,X84) ) ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_28,axiom, % 58.69/58.81 ! [X85,X86,X87,X88] : % 58.69/58.81 ( ( occurrence_of(X86,X85) % 58.69/58.81 & arboreal(X87) % 58.69/58.81 & arboreal(X88) % 58.69/58.81 & subactivity_occurrence(X87,X86) % 58.69/58.81 & subactivity_occurrence(X88,X86) ) % 58.69/58.81 => ( min_precedes(X87,X88,X85) % 58.69/58.81 | min_precedes(X88,X87,X85) % 58.69/58.81 | X87 = X88 ) ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_29,axiom, % 58.69/58.81 ! [X89,X90] : % 58.69/58.81 ( occurrence_of(X90,X89) % 58.69/58.81 => ( activity(X89) % 58.69/58.81 & activity_occurrence(X90) ) ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_30,axiom, % 58.69/58.81 ! [X91,X92] : % 58.69/58.81 ( ( occurrence_of(X92,X91) % 58.69/58.81 & ~ atomic(X91) ) % 58.69/58.81 => ? [X93] : % 58.69/58.81 ( root(X93,X91) % 58.69/58.81 & subactivity_occurrence(X93,X92) ) ) ). % 58.69/58.81 % 58.69/58.81 fof(sos_31,axiom, % 58.69/58.81 ! [X94] : % 58.69/58.81 ( activity(X94) % 58.69/58.82 => subactivity(X94,X94) ) ). % 58.69/58.82 % 58.69/58.82 fof(sos_32,axiom, % 58.69/58.82 ! [X95] : % 58.69/58.82 ( occurrence_of(X95,tptp0) % 58.69/58.82 => ? [X96,X97,X98] : % 58.69/58.82 ( occurrence_of(X96,tptp3) % 58.69/58.82 & root_occ(X96,X95) % 58.69/58.82 & occurrence_of(X97,tptp4) % 58.69/58.82 & next_subocc(X96,X97,tptp0) % 58.69/58.82 & ( occurrence_of(X98,tptp2) % 58.69/58.82 | occurrence_of(X98,tptp1) ) % 58.69/58.82 & next_subocc(X97,X98,tptp0) % 58.69/58.82 & leaf_occ(X98,X95) ) ) ). % 58.69/58.82 % 58.69/58.82 fof(sos_33,axiom, % 58.69/58.82 activity(tptp0) ). % 58.69/58.82 % 58.69/58.82 fof(sos_34,axiom, % 58.69/58.82 ~ atomic(tptp0) ). % 58.69/58.82 % 58.69/58.82 fof(sos_35,axiom, % 58.69/58.82 atomic(tptp4) ). % 58.69/58.82 % 58.69/58.82 fof(sos_36,axiom, % 58.69/58.82 atomic(tptp2) ). % 58.69/58.82 % 58.69/58.82 fof(sos_37,axiom, % 58.69/58.82 atomic(tptp1) ). % 58.69/58.82 % 58.69/58.82 fof(sos_38,axiom, % 58.69/58.82 atomic(tptp3) ). % 58.69/58.82 % 58.69/58.82 fof(sos_39,axiom, % 58.69/58.82 tptp4 != tptp3 ). % 58.69/58.82 % 58.69/58.82 fof(sos_40,axiom, % 58.69/58.82 tptp4 != tptp2 ). % 58.69/58.82 % 58.69/58.82 fof(sos_41,axiom, % 58.69/58.82 tptp4 != tptp1 ). % 58.69/58.82 % 58.69/58.82 fof(sos_42,axiom, % 58.69/58.82 tptp3 != tptp2 ). % 58.69/58.82 % 58.69/58.82 fof(sos_43,axiom, % 58.69/58.82 tptp3 != tptp1 ). % 58.69/58.82 % 58.69/58.82 fof(sos_44,axiom, % 58.69/58.82 tptp2 != tptp1 ). % 58.69/58.82 % 58.69/58.82 fof(goals,conjecture, % 58.69/58.82 ! [X99] : % 58.69/58.82 ( occurrence_of(X99,tptp0) % 58.69/58.82 => ? [X100,X101] : % 58.69/58.82 ( occurrence_of(X100,tptp3) % 58.69/58.82 & root_occ(X100,X99) % 58.69/58.82 & ( occurrence_of(X101,tptp2) % 58.69/58.82 | occurrence_of(X101,tptp1) ) % 58.69/58.82 & min_precedes(X100,X101,tptp0) % 58.69/58.82 & leaf_occ(X101,X99) ) ) ). % 58.69/58.82 % 58.69/58.82 %------------------------------------------------------------------------------ % 58.69/58.82 %------------------------------------------- % 58.69/58.82 % Proof found % 58.69/58.82 % SZS status Theorem for theBenchmark % 58.69/58.82 % SZS output start Proof % 58.69/58.82 %ClaNum:153(EqnAxiom:68) % 58.69/58.82 %VarNum:398(SingletonVarNum:168) % 58.69/58.82 %MaxLitNum:8 % 58.69/58.82 %MaxfuncDepth:1 % 58.69/58.82 %SharedTerms:19 % 58.69/58.82 %goalClause: 74 139 140 % 58.69/58.82 %singleGoalClaCount:1 % 58.69/58.82 [69]P1(a1) % 58.69/58.82 [70]P1(a23) % 58.69/58.82 [71]P1(a2) % 58.69/58.82 [72]P1(a3) % 58.69/58.82 [73]P2(a4) % 58.69/58.82 [74]P6(a5,a4) % 58.69/58.82 [75]~E(a1,a23) % 58.69/58.82 [76]~E(a1,a2) % 58.69/58.82 [77]~E(a2,a23) % 58.69/58.82 [78]~E(a1,a3) % 58.69/58.82 [79]~E(a3,a23) % 58.69/58.82 [80]~E(a3,a2) % 58.69/58.82 [81]~P1(a4) % 58.69/58.82 [82]~P7(x821)+P3(x821) % 58.69/58.82 [84]~P2(x841)+P13(x841,x841) % 58.69/58.82 [83]~P4(x831)+P2(f14(x831)) % 58.69/58.82 [91]~P4(x911)+P6(x911,f14(x911)) % 58.69/58.82 [97]~P6(x971,a4)+P6(f6(x971),a1) % 58.69/58.82 [98]~P6(x981,a4)+P6(f12(x981),a23) % 58.69/58.82 [99]~P6(x991,a4)+P16(f6(x991),x991) % 58.69/58.82 [100]~P6(x1001,a4)+P9(f13(x1001),x1001) % 58.69/58.82 [127]~P6(x1271,a4)+P11(f6(x1271),f12(x1271),a4) % 58.69/58.82 [128]~P6(x1281,a4)+P11(f12(x1281),f13(x1281),a4) % 58.69/58.82 [85]P7(x851)+~P14(x852,x851) % 58.69/58.82 [86]P7(x861)+~P15(x861,x862) % 58.69/58.82 [87]P4(x871)+~P6(x871,x872) % 58.69/58.82 [88]P4(x881)+~P17(x882,x881) % 58.69/58.82 [89]P4(x891)+~P17(x891,x892) % 58.69/58.82 [90]P2(x901)+~P6(x902,x901) % 58.69/58.82 [94]~P14(x941,x942)+P8(x941,x942) % 58.69/58.82 [95]~P16(x951,x952)+P17(x951,x952) % 58.69/58.82 [96]~P9(x961,x962)+P17(x961,x962) % 58.69/58.82 [103]~P8(x1032,x1031)+~P8(x1031,x1032) % 58.69/58.82 [105]~P5(x1051,x1052)+P1(f15(x1051,x1052)) % 58.69/58.82 [108]~P16(x1082,x1081)+P6(x1081,f16(x1082,x1081)) % 58.69/58.82 [109]~P9(x1092,x1091)+P6(x1091,f18(x1092,x1091)) % 58.69/58.82 [110]~P5(x1101,x1102)+P6(x1101,f15(x1101,x1102)) % 58.69/58.82 [111]~P16(x1111,x1112)+P15(x1111,f16(x1111,x1112)) % 58.69/58.82 [112]~P9(x1121,x1122)+P10(x1121,f18(x1121,x1122)) % 58.69/58.82 [113]~P15(x1131,x1132)+P5(x1131,f7(x1132,x1131)) % 58.69/58.82 [114]~P5(x1142,x1141)+P13(x1141,f15(x1142,x1141)) % 58.69/58.82 [115]~P15(x1152,x1151)+P13(f7(x1151,x1152),x1151) % 58.69/58.82 [129]P3(x1291)+~P11(x1292,x1291,x1293) % 58.69/58.82 [130]P3(x1301)+~P11(x1301,x1302,x1303) % 58.69/58.82 [131]P14(x1311,x1312)+~P12(x1311,x1312,x1313) % 58.69/58.82 [132]~P15(x1321,x1322)+~P12(x1323,x1321,x1322) % 58.69/58.82 [133]~P10(x1331,x1332)+~P12(x1331,x1333,x1332) % 58.69/58.82 [138]~P11(x1381,x1382,x1383)+P12(x1381,x1382,x1383) % 58.69/58.82 [143]~P12(x1433,x1431,x1432)+P17(x1431,f22(x1432,x1433,x1431)) % 58.69/58.82 [144]~P12(x1441,x1443,x1442)+P17(x1441,f22(x1442,x1441,x1443)) % 58.69/58.82 [145]~P12(x1451,x1453,x1452)+P5(x1451,f9(x1452,x1451,x1453)) % 58.69/58.82 [146]~P12(x1463,x1461,x1462)+P5(x1461,f10(x1462,x1463,x1461)) % 58.69/58.82 [147]~P12(x1472,x1473,x1471)+P6(f22(x1471,x1472,x1473),x1471) % 58.69/58.82 [148]~P12(x1482,x1483,x1481)+P13(f9(x1481,x1482,x1483),x1481) % 58.69/58.82 [149]~P12(x1492,x1493,x1491)+P13(f10(x1491,x1492,x1493),x1491) % 58.69/58.82 [106]~P6(x1061,a4)+P6(f13(x1061),a2)+P6(f13(x1061),a3) % 58.69/58.82 [92]~P6(x922,x921)+P1(x921)+~P3(x922) % 58.69/58.82 [93]~P6(x931,x932)+P3(x931)+~P1(x932) % 58.69/58.82 [101]~P7(x1012)+~P8(x1011,x1012)+P14(x1011,x1012) % 58.69/58.82 [102]~P7(x1021)+~P5(x1021,x1022)+P15(x1021,x1022) % 58.69/58.82 [117]~P10(x1172,x1171)+P1(x1171)+P9(x1172,f21(x1172,x1171)) % 58.69/58.82 [118]~P10(x1182,x1181)+P1(x1181)+P9(x1182,f8(x1182,x1181)) % 58.69/58.82 [119]~P10(x1192,x1191)+P1(x1191)+P6(f21(x1192,x1191),x1191) % 58.69/58.82 [120]~P10(x1202,x1201)+P1(x1201)+P6(f8(x1202,x1201),x1201) % 58.69/58.82 [121]~P6(x1212,x1211)+P1(x1211)+P15(f11(x1211,x1212),x1211) % 58.69/58.82 [122]~P6(x1222,x1221)+P1(x1221)+P17(f11(x1221,x1222),x1222) % 58.69/58.82 [134]~P15(x1341,x1342)+P10(x1341,x1342)+P12(x1341,f19(x1341,x1342),x1342) % 58.69/58.82 [135]~P10(x1351,x1352)+P15(x1351,x1352)+P12(f20(x1351,x1352),x1351,x1352) % 58.69/58.82 [104]~P6(x1043,x1041)+E(x1041,x1042)+~P6(x1043,x1042) % 58.69/58.82 [107]~P8(x1071,x1073)+P8(x1071,x1072)+~P8(x1073,x1072) % 58.69/58.82 [141]P10(x1411,x1412)+~P12(x1413,x1411,x1412)+P12(x1411,f19(x1411,x1412),x1412) % 58.69/58.82 [152]~P12(x1521,x1522,x1523)+P11(x1521,x1522,x1523)+P12(x1521,f17(x1521,x1522,x1523),x1523) % 58.69/58.82 [153]~P12(x1531,x1532,x1533)+P11(x1531,x1532,x1533)+P12(f17(x1531,x1532,x1533),x1532,x1533) % 58.69/58.82 [136]~P6(x1361,x1362)+~P12(x1364,x1363,x1362)+~P16(x1363,x1361) % 58.69/58.82 [137]~P6(x1371,x1372)+~P12(x1373,x1374,x1372)+~P9(x1373,x1371) % 58.69/58.82 [150]~P12(x1501,x1504,x1503)+P12(x1501,x1502,x1503)+~P12(x1504,x1502,x1503) % 58.69/58.82 [151]~P11(x1514,x1512,x1513)+~P12(x1511,x1512,x1513)+~P12(x1514,x1511,x1513) % 58.69/58.82 [116]~P6(x1161,x1163)+~P13(x1162,x1163)+P5(x1161,x1162)+~P1(x1163) % 58.69/58.82 [125]~P15(x1251,x1253)+~P17(x1251,x1252)+P16(x1251,x1252)+~P6(x1252,x1253) % 58.69/58.82 [126]~P17(x1261,x1262)+~P10(x1261,x1263)+P9(x1261,x1262)+~P6(x1262,x1263) % 58.69/58.82 [123]~P16(x1232,x1233)+~P16(x1231,x1233)+E(x1231,x1232)+~P6(x1233,x1234) % 58.69/58.82 [139]~P12(x1391,x1392,a4)+~P16(x1391,a5)+~P9(x1392,a5)+~P6(x1391,a1)+~P6(x1392,a2) % 58.69/58.82 [140]~P12(x1401,x1402,a4)+~P16(x1401,a5)+~P9(x1402,a5)+~P6(x1401,a1)+~P6(x1402,a3) % 58.69/58.82 [124]~P9(x1242,x1244)+~P9(x1241,x1244)+E(x1241,x1242)+~P6(x1244,x1243)+P1(x1243) % 58.69/58.82 [142]P12(x1421,x1422,x1423)+~P3(x1422)+~P3(x1421)+~P17(x1422,x1424)+~P17(x1421,x1424)+E(x1421,x1422)+P12(x1422,x1421,x1423)+~P6(x1424,x1423) % 58.69/58.82 %EqnAxiom % 58.69/58.82 [1]E(x11,x11) % 58.69/58.82 [2]E(x22,x21)+~E(x21,x22) % 58.69/58.82 [3]E(x31,x33)+~E(x31,x32)+~E(x32,x33) % 58.69/58.82 [4]~E(x41,x42)+E(f14(x41),f14(x42)) % 58.69/58.82 [5]~E(x51,x52)+E(f17(x51,x53,x54),f17(x52,x53,x54)) % 58.69/58.82 [6]~E(x61,x62)+E(f17(x63,x61,x64),f17(x63,x62,x64)) % 58.69/58.82 [7]~E(x71,x72)+E(f17(x73,x74,x71),f17(x73,x74,x72)) % 58.69/58.82 [8]~E(x81,x82)+E(f6(x81),f6(x82)) % 58.69/58.82 [9]~E(x91,x92)+E(f12(x91),f12(x92)) % 58.69/58.82 [10]~E(x101,x102)+E(f10(x101,x103,x104),f10(x102,x103,x104)) % 58.69/58.82 [11]~E(x111,x112)+E(f10(x113,x111,x114),f10(x113,x112,x114)) % 58.69/58.82 [12]~E(x121,x122)+E(f10(x123,x124,x121),f10(x123,x124,x122)) % 58.69/58.82 [13]~E(x131,x132)+E(f13(x131),f13(x132)) % 58.69/58.82 [14]~E(x141,x142)+E(f15(x141,x143),f15(x142,x143)) % 58.69/58.82 [15]~E(x151,x152)+E(f15(x153,x151),f15(x153,x152)) % 58.69/58.82 [16]~E(x161,x162)+E(f22(x161,x163,x164),f22(x162,x163,x164)) % 58.69/58.82 [17]~E(x171,x172)+E(f22(x173,x171,x174),f22(x173,x172,x174)) % 58.69/58.82 [18]~E(x181,x182)+E(f22(x183,x184,x181),f22(x183,x184,x182)) % 58.69/58.82 [19]~E(x191,x192)+E(f19(x191,x193),f19(x192,x193)) % 58.69/58.82 [20]~E(x201,x202)+E(f19(x203,x201),f19(x203,x202)) % 58.69/58.82 [21]~E(x211,x212)+E(f16(x211,x213),f16(x212,x213)) % 58.69/58.82 [22]~E(x221,x222)+E(f16(x223,x221),f16(x223,x222)) % 58.69/58.82 [23]~E(x231,x232)+E(f18(x231,x233),f18(x232,x233)) % 58.69/58.82 [24]~E(x241,x242)+E(f18(x243,x241),f18(x243,x242)) % 58.69/58.82 [25]~E(x251,x252)+E(f20(x251,x253),f20(x252,x253)) % 58.69/58.82 [26]~E(x261,x262)+E(f20(x263,x261),f20(x263,x262)) % 58.69/58.82 [27]~E(x271,x272)+E(f9(x271,x273,x274),f9(x272,x273,x274)) % 58.69/58.82 [28]~E(x281,x282)+E(f9(x283,x281,x284),f9(x283,x282,x284)) % 58.69/58.82 [29]~E(x291,x292)+E(f9(x293,x294,x291),f9(x293,x294,x292)) % 58.69/58.82 [30]~E(x301,x302)+E(f11(x301,x303),f11(x302,x303)) % 58.69/58.82 [31]~E(x311,x312)+E(f11(x313,x311),f11(x313,x312)) % 58.69/58.82 [32]~E(x321,x322)+E(f7(x321,x323),f7(x322,x323)) % 58.69/58.82 [33]~E(x331,x332)+E(f7(x333,x331),f7(x333,x332)) % 58.69/58.82 [34]~E(x341,x342)+E(f8(x341,x343),f8(x342,x343)) % 58.69/58.82 [35]~E(x351,x352)+E(f8(x353,x351),f8(x353,x352)) % 58.69/58.82 [36]~E(x361,x362)+E(f21(x361,x363),f21(x362,x363)) % 58.69/58.82 [37]~E(x371,x372)+E(f21(x373,x371),f21(x373,x372)) % 58.69/58.82 [38]~P1(x381)+P1(x382)+~E(x381,x382) % 58.69/58.82 [39]P12(x392,x393,x394)+~E(x391,x392)+~P12(x391,x393,x394) % 58.69/58.82 [40]P12(x403,x402,x404)+~E(x401,x402)+~P12(x403,x401,x404) % 58.69/58.82 [41]P12(x413,x414,x412)+~E(x411,x412)+~P12(x413,x414,x411) % 58.69/58.82 [42]P13(x422,x423)+~E(x421,x422)+~P13(x421,x423) % 58.69/58.82 [43]P13(x433,x432)+~E(x431,x432)+~P13(x433,x431) % 58.69/58.82 [44]P11(x442,x443,x444)+~E(x441,x442)+~P11(x441,x443,x444) % 58.69/58.82 [45]P11(x453,x452,x454)+~E(x451,x452)+~P11(x453,x451,x454) % 58.69/58.82 [46]P11(x463,x464,x462)+~E(x461,x462)+~P11(x463,x464,x461) % 58.69/58.82 [47]~P2(x471)+P2(x472)+~E(x471,x472) % 58.69/58.82 [48]P6(x482,x483)+~E(x481,x482)+~P6(x481,x483) % 58.69/58.82 [49]P6(x493,x492)+~E(x491,x492)+~P6(x493,x491) % 58.69/58.82 [50]P10(x502,x503)+~E(x501,x502)+~P10(x501,x503) % 58.69/58.82 [51]P10(x513,x512)+~E(x511,x512)+~P10(x513,x511) % 58.69/58.82 [52]~P3(x521)+P3(x522)+~E(x521,x522) % 58.69/58.82 [53]~P7(x531)+P7(x532)+~E(x531,x532) % 58.69/58.82 [54]P15(x542,x543)+~E(x541,x542)+~P15(x541,x543) % 58.69/58.82 [55]P15(x553,x552)+~E(x551,x552)+~P15(x553,x551) % 58.69/58.82 [56]~P4(x561)+P4(x562)+~E(x561,x562) % 58.69/58.82 [57]P9(x572,x573)+~E(x571,x572)+~P9(x571,x573) % 58.69/58.82 [58]P9(x583,x582)+~E(x581,x582)+~P9(x583,x581) % 58.69/58.82 [59]P5(x592,x593)+~E(x591,x592)+~P5(x591,x593) % 58.69/58.82 [60]P5(x603,x602)+~E(x601,x602)+~P5(x603,x601) % 58.69/58.82 [61]P8(x612,x613)+~E(x611,x612)+~P8(x611,x613) % 58.69/58.82 [62]P8(x623,x622)+~E(x621,x622)+~P8(x623,x621) % 58.69/58.82 [63]P14(x632,x633)+~E(x631,x632)+~P14(x631,x633) % 58.69/58.82 [64]P14(x643,x642)+~E(x641,x642)+~P14(x643,x641) % 58.69/58.82 [65]P16(x652,x653)+~E(x651,x652)+~P16(x651,x653) % 58.69/58.82 [66]P16(x663,x662)+~E(x661,x662)+~P16(x663,x661) % 58.69/58.82 [67]P17(x672,x673)+~E(x671,x672)+~P17(x671,x673) % 58.69/58.82 [68]P17(x683,x682)+~E(x681,x682)+~P17(x683,x681) % 58.69/58.82 % 58.69/58.82 %------------------------------------------- % 58.69/58.82 cnf(154,plain, % 58.69/58.82 (~P3(a5)), % 58.69/58.82 inference(scs_inference,[],[74,81,92])). % 58.69/58.82 cnf(156,plain, % 58.69/58.82 (~P6(a5,a1)), % 58.69/58.82 inference(scs_inference,[],[74,69,81,92,93])). % 58.69/58.82 cnf(161,plain, % 58.69/58.82 (~P15(a5,x1611)), % 58.69/58.82 inference(scs_inference,[],[74,69,81,92,93,49,82,86])). % 58.69/58.82 cnf(167,plain, % 58.69/58.82 (~P11(a5,x1671,x1672)), % 58.69/58.82 inference(scs_inference,[],[74,69,81,92,93,49,82,86,111,129,130])). % 58.69/58.82 cnf(171,plain, % 58.69/58.82 (~P12(x1711,a5,x1712)), % 58.69/58.82 inference(scs_inference,[],[74,69,81,92,93,49,82,86,111,129,130,85,131])). % 58.69/58.82 cnf(175,plain, % 58.69/58.82 (P6(x1751,a4)+~E(a5,x1751)), % 58.69/58.82 inference(scs_inference,[],[74,69,81,92,93,49,82,86,111,129,130,85,131,135,48])). % 58.69/58.82 cnf(180,plain, % 58.69/58.82 (~P10(a5,x1801)), % 58.69/58.82 inference(scs_inference,[],[161,171,135])). % 58.69/58.82 cnf(183,plain, % 58.69/58.82 (~P6(a5,a23)), % 58.69/58.82 inference(scs_inference,[],[154,161,70,171,135,93])). % 58.69/58.82 cnf(190,plain, % 58.69/58.82 (~P6(a5,a2)), % 58.69/58.82 inference(scs_inference,[],[154,71,93])). % 58.69/58.82 cnf(238,plain, % 58.69/58.82 (~P17(x2381,x2382)+P2(f14(x2381))), % 58.69/58.82 inference(scs_inference,[],[89,83])). % 58.69/58.82 cnf(239,plain, % 58.69/58.82 (P13(a4,a4)), % 58.69/58.82 inference(scs_inference,[],[74,90,84])). % 58.69/58.82 cnf(240,plain, % 58.69/58.82 (P13(a4,x2401)+~E(a4,x2401)), % 58.69/58.82 inference(scs_inference,[],[239,43])). % 58.69/58.82 cnf(241,plain, % 58.69/58.82 (P13(x2411,a4)+~E(a4,x2411)), % 58.69/58.82 inference(scs_inference,[],[239,43,42])). % 58.69/58.82 cnf(244,plain, % 58.69/58.82 (~E(a4,a3)), % 58.69/58.82 inference(scs_inference,[],[72,81,2,38])). % 58.69/58.82 cnf(248,plain, % 58.69/58.82 (~P8(x2481,x2482)+~P14(x2482,x2481)), % 58.69/58.82 inference(scs_inference,[],[94,103])). % 58.69/58.82 cnf(253,plain, % 58.69/58.82 (P2(f14(x2531))+~P9(x2531,x2532)), % 58.69/58.82 inference(scs_inference,[],[96,238])). % 58.69/58.82 cnf(284,plain, % 58.69/58.82 (~P8(x2841,x2842)+~P12(x2842,x2841,x2843)), % 58.69/58.82 inference(scs_inference,[],[248,131])). % 58.69/58.82 cnf(288,plain, % 58.69/58.82 (~E(a4,a23)), % 58.69/58.82 inference(scs_inference,[],[183,74,49])). % 58.69/58.82 cnf(300,plain, % 58.69/58.82 (~E(a4,a2)), % 58.69/58.82 inference(scs_inference,[],[190,74,49])). % 58.69/58.82 cnf(311,plain, % 58.69/58.82 (~E(a5,x3111)+P6(f12(x3111),a23)), % 58.69/58.82 inference(scs_inference,[],[98,175])). % 58.69/58.82 cnf(312,plain, % 58.69/58.82 (P6(f12(a5),a23)), % 58.69/58.82 inference(equality_inference,[],[311])). % 58.69/58.82 cnf(325,plain, % 58.69/58.82 (P17(f6(a5),a5)), % 58.69/58.82 inference(scs_inference,[],[74,99,95])). % 58.69/58.82 cnf(330,plain, % 58.69/58.82 (P17(f13(a5),a5)), % 58.69/58.82 inference(scs_inference,[],[74,100,96])). % 58.69/58.82 cnf(356,plain, % 58.69/58.82 (~P12(x3561,x3562,x3563)+~P14(x3562,x3561)), % 58.69/58.82 inference(scs_inference,[],[284,94])). % 58.69/58.82 cnf(381,plain, % 58.69/58.82 (~P12(x3811,x3812,x3813)+~P12(x3812,x3811,x3814)), % 58.69/58.82 inference(scs_inference,[],[356,131])). % 58.69/58.82 cnf(390,plain, % 58.69/58.82 (P6(a5,f16(f6(a5),a5))), % 58.69/58.82 inference(scs_inference,[],[74,108,99])). % 58.69/58.82 cnf(393,plain, % 58.69/58.82 (E(a4,f16(f6(a5),a5))), % 58.69/58.82 inference(scs_inference,[],[74,156,390,49,48,104])). % 58.69/58.82 cnf(403,plain, % 58.69/58.82 (E(f16(f6(a5),a5),a4)), % 58.69/58.82 inference(scs_inference,[],[393,240,241,2])). % 58.69/58.82 cnf(404,plain, % 58.69/58.82 (~P1(f16(f6(a5),a5))), % 58.69/58.82 inference(scs_inference,[],[393,81,240,241,2,38])). % 58.69/58.82 cnf(629,plain, % 58.69/58.82 (~P15(x6291,x6292)+P6(x6291,f15(x6291,f7(x6292,x6291)))), % 58.69/58.82 inference(scs_inference,[],[110,113])). % 58.69/58.82 cnf(680,plain, % 58.69/58.82 (~P11(x6801,x6802,x6803)+~P12(x6802,x6801,x6804)), % 58.69/58.82 inference(scs_inference,[],[381,138])). % 58.69/58.82 cnf(754,plain, % 58.69/58.82 (~E(a23,a4)), % 58.69/58.82 inference(scs_inference,[],[74,288,312,104,48,49])). % 58.69/58.82 cnf(894,plain, % 58.69/58.82 (~P11(x8941,x8942,x8943)+P17(x8941,f22(x8943,x8941,x8942))), % 58.69/58.82 inference(scs_inference,[],[144,138])). % 58.69/58.82 cnf(903,plain, % 58.69/58.82 (~P15(x9031,x9032)+P4(x9031)), % 58.69/58.82 inference(scs_inference,[],[629,87])). % 58.69/58.82 cnf(920,plain, % 58.69/58.82 (~P11(x9201,x9202,x9203)+P4(x9201)), % 58.69/58.82 inference(scs_inference,[],[894,89])). % 58.69/58.82 cnf(1124,plain, % 58.69/58.82 (P15(f11(a4,a5),f16(f6(a5),a5))), % 58.69/58.82 inference(scs_inference,[],[393,81,74,55,121])). % 58.69/58.82 cnf(1127,plain, % 58.69/58.82 (~P11(x11271,f11(a4,a5),f16(f6(a5),a5))), % 58.69/58.82 inference(scs_inference,[],[1124,132,138])). % 58.69/58.82 cnf(1131,plain, % 58.69/58.82 (P15(f11(a4,a5),a4)), % 58.69/58.82 inference(scs_inference,[],[403,161,1124,132,138,54,55])). % 58.69/58.82 cnf(1160,plain, % 58.69/58.83 (~P8(x11601,x11602)+~P14(x11602,x11603)+P8(x11601,x11603)), % 58.69/58.83 inference(scs_inference,[],[107,94])). % 58.69/58.83 cnf(1162,plain, % 58.69/58.83 (~P8(x11621,x11622)+~P8(x11622,x11623)+~P14(x11623,x11621)), % 58.69/58.83 inference(scs_inference,[],[1160,103])). % 58.69/58.83 cnf(1163,plain, % 58.69/58.83 (~P8(x11631,x11632)+~P12(x11633,x11631,x11634)+~P8(x11632,x11633)), % 58.69/58.83 inference(scs_inference,[],[1162,131])). % 58.69/58.83 cnf(1164,plain, % 58.69/58.83 (~P10(x11641,a4)+P2(f14(x11641))), % 58.69/58.83 inference(scs_inference,[],[81,118,253])). % 58.69/58.83 cnf(1172,plain, % 58.69/58.83 (P17(f11(a4,a5),a5)), % 58.69/58.83 inference(scs_inference,[],[74,393,404,122,38])). % 58.69/58.83 cnf(1193,plain, % 58.69/58.83 (~P12(x11931,f6(a5),a4)), % 58.69/58.83 inference(scs_inference,[],[74,136,99])). % 58.69/58.83 cnf(1194,plain, % 58.69/58.83 (~P11(x11941,f6(a5),a4)), % 58.69/58.83 inference(scs_inference,[],[1193,138])). % 58.69/58.83 cnf(1215,plain, % 58.69/58.83 (~P12(f13(a5),x12151,a4)), % 58.69/58.83 inference(scs_inference,[],[74,137,100])). % 58.69/58.83 cnf(1234,plain, % 58.69/58.83 (~P12(x12341,f13(a5),a4)+~E(f13(a5),a5)), % 58.69/58.83 inference(scs_inference,[],[180,1215,141,50])). % 58.69/58.83 cnf(1239,plain, % 58.69/58.83 (~P12(f13(a5),x12391,f16(f6(a5),a5))+~P12(x12392,f13(a5),a4)), % 58.69/58.83 inference(scs_inference,[],[393,180,1215,141,50,51,1164,133])). % 58.69/58.83 cnf(1248,plain, % 58.69/58.83 (~E(a5,f13(a5))+~P12(x12481,f13(a5),a4)), % 58.69/58.83 inference(scs_inference,[],[1234,2])). % 58.69/58.83 cnf(1251,plain, % 58.69/58.83 (~P11(x12511,f13(a5),a4)+~E(a5,f13(a5))), % 58.69/58.83 inference(scs_inference,[],[1248,138])). % 58.69/58.83 cnf(1252,plain, % 58.69/58.83 (~E(a5,f13(a5))), % 58.69/58.83 inference(scs_inference,[],[74,1251,128])). % 58.69/58.83 cnf(1259,plain, % 58.69/58.83 (~P11(x12591,f13(a5),a4)+~P12(f13(a5),x12592,f16(f6(a5),a5))), % 58.69/58.83 inference(scs_inference,[],[1239,138])). % 58.69/58.83 cnf(1262,plain, % 58.69/58.83 (~P12(f13(a5),x12621,f16(f6(a5),a5))), % 58.69/58.83 inference(scs_inference,[],[74,1259,128])). % 58.69/58.83 cnf(1263,plain, % 58.69/58.83 (~P11(f13(a5),x12631,f16(f6(a5),a5))), % 58.69/58.83 inference(scs_inference,[],[1262,138])). % 58.69/58.83 cnf(1268,plain, % 58.69/58.83 (~P8(x12681,x12682)+~P14(x12682,x12683)+~P12(x12683,x12681,x12684)), % 58.69/58.83 inference(scs_inference,[],[1163,94])). % 58.69/58.83 cnf(1282,plain, % 58.69/58.83 (P11(f6(a5),f12(a5),f16(f6(a5),a5))), % 58.69/58.83 inference(scs_inference,[],[393,74,46,127])). % 58.69/58.83 cnf(1283,plain, % 58.69/58.83 (~E(f6(a5),f13(a5))), % 58.69/58.83 inference(scs_inference,[],[1263,1282,44])). % 58.69/58.83 cnf(1287,plain, % 58.69/58.83 (P11(f6(a5),f12(a5),a4)), % 58.69/58.83 inference(scs_inference,[],[1127,1263,403,1282,44,45,46])). % 58.69/58.83 cnf(1300,plain, % 58.69/58.83 (~E(f12(a5),f6(a5))), % 58.69/58.83 inference(scs_inference,[],[1194,1287,45])). % 58.69/58.83 cnf(1314,plain, % 58.69/58.83 (~P16(f13(a5),a5)+~P16(f6(a5),a5)), % 58.69/58.83 inference(scs_inference,[],[74,1283,123])). % 58.69/58.83 cnf(1322,plain, % 58.69/58.83 (~P16(f6(a5),a5)+~P16(f12(a5),a5)), % 58.69/58.83 inference(scs_inference,[],[74,1300,123])). % 58.69/58.83 cnf(1342,plain, % 58.69/58.83 (~P16(f13(a5),a5)), % 58.69/58.83 inference(scs_inference,[],[74,1314,99])). % 58.69/58.83 cnf(1343,plain, % 58.69/58.83 (~P15(f13(a5),a4)), % 58.69/58.83 inference(scs_inference,[],[74,1342,330,125])). % 58.69/58.83 cnf(1360,plain, % 58.69/58.83 (~E(f11(a4,a5),f13(a5))), % 58.69/58.83 inference(scs_inference,[],[1343,1131,54])). % 58.69/58.83 cnf(1361,plain, % 58.69/58.83 (~P9(f13(a5),a5)+~P9(f11(a4,a5),a5)), % 58.69/58.83 inference(scs_inference,[],[74,1343,81,1131,54,124])). % 58.69/58.83 cnf(1366,plain, % 58.69/58.83 (~P16(x13661,a5)+~E(x13661,f12(a5))+~P16(f6(a5),a5)), % 58.69/58.83 inference(scs_inference,[],[1322,65])). % 58.69/58.83 cnf(1386,plain, % 58.69/58.83 (~P10(f11(a4,a5),a4)+~P9(f13(a5),a5)), % 58.69/58.83 inference(scs_inference,[],[74,1172,1361,126])). % 58.69/58.83 cnf(1387,plain, % 58.69/58.83 (~P9(f13(a5),a5)+P12(f11(a4,a5),f19(f11(a4,a5),a4),a4)), % 58.69/58.83 inference(scs_inference,[],[1131,1386,134])). % 58.69/58.83 cnf(1400,plain, % 58.69/58.83 (P12(f11(a4,a5),f19(f11(a4,a5),a4),a4)), % 58.69/58.83 inference(scs_inference,[],[74,1387,100])). % 58.69/58.83 cnf(1469,plain, % 58.69/58.83 (~E(f6(a5),a5)), % 58.69/58.83 inference(scs_inference,[],[167,1287,44])). % 58.69/58.83 cnf(1685,plain, % 58.69/58.83 (P6(a5,f14(a5))), % 58.69/58.83 inference(scs_inference,[],[74,87,91])). % 58.69/58.83 cnf(1688,plain, % 58.69/58.83 (E(a4,f14(a5))), % 58.69/58.83 inference(scs_inference,[],[74,156,1685,49,48,104])). % 58.69/58.83 cnf(1696,plain, % 58.69/58.83 (E(f14(a5),a4)), % 58.69/58.83 inference(scs_inference,[],[1688,2])). % 58.69/58.83 cnf(1700,plain, % 58.69/58.83 (~P1(f14(a5))), % 58.69/58.83 inference(scs_inference,[],[754,1688,81,2,241,240,3,38])). % 58.69/58.83 cnf(1983,plain, % 58.69/58.83 (P11(f6(a5),f12(a5),f14(a5))), % 58.69/58.83 inference(scs_inference,[],[1688,1400,1287,41,46])). % 58.69/58.83 cnf(1984,plain, % 58.69/58.83 (P15(f11(a4,a5),f14(a5))), % 58.69/58.83 inference(scs_inference,[],[1688,1400,1287,1131,41,46,55])). % 58.69/58.83 cnf(3513,plain, % 58.69/58.83 (P6(f6(a5),a1)), % 58.69/58.83 inference(scs_inference,[],[74,312,90,97])). % 58.69/58.83 cnf(3515,plain, % 58.69/58.83 (P11(f12(a5),f13(a5),a4)), % 58.69/58.83 inference(scs_inference,[],[74,312,90,97,128])). % 58.69/58.83 cnf(3522,plain, % 58.69/58.83 (P16(f6(a5),a5)), % 58.69/58.83 inference(scs_inference,[],[74,1252,330,312,90,97,128,2,88,89,99])). % 58.69/58.83 cnf(3528,plain, % 58.69/58.83 (P9(f13(a5),a5)), % 58.69/58.83 inference(scs_inference,[],[74,1252,1984,330,312,90,97,128,2,88,89,99,920,903,100])). % 58.69/58.83 cnf(3532,plain, % 58.69/58.83 (P14(f6(a5),f12(a5))), % 58.69/58.83 inference(scs_inference,[],[74,1252,1984,1983,330,312,90,97,128,2,88,89,99,920,903,100,138,131])). % 58.69/58.83 cnf(3536,plain, % 58.69/58.83 (P3(f6(a5))), % 58.69/58.83 inference(scs_inference,[],[74,1252,1984,1983,330,312,90,97,128,2,88,89,99,920,903,100,138,131,129,130])). % 58.69/58.83 cnf(3542,plain, % 58.69/58.83 (P16(f11(a4,a5),a5)), % 58.69/58.83 inference(scs_inference,[],[74,1252,1984,1983,76,330,1131,312,1172,90,97,128,2,88,89,99,920,903,100,138,131,129,130,104,151,125])). % 58.69/58.83 cnf(3544,plain, % 58.69/58.83 (P13(a23,a23)), % 58.69/58.83 inference(scs_inference,[],[74,1252,1984,1983,76,330,1131,312,1172,90,97,128,2,88,89,99,920,903,100,138,131,129,130,104,151,125,84])). % 58.69/58.83 cnf(3546,plain, % 58.69/58.83 (P8(f6(a5),f12(a5))), % 58.69/58.83 inference(scs_inference,[],[74,1252,1984,1983,76,330,1131,312,1172,90,97,128,2,88,89,99,920,903,100,138,131,129,130,104,151,125,84,94])). % 58.69/58.83 cnf(3548,plain, % 58.69/58.83 (~P8(f12(a5),f6(a5))), % 58.69/58.83 inference(scs_inference,[],[74,1252,1984,1983,76,330,1131,312,1172,90,97,128,2,88,89,99,920,903,100,138,131,129,130,104,151,125,84,94,103])). % 58.69/58.83 cnf(3552,plain, % 58.69/58.83 (~P15(f12(a5),f14(a5))), % 58.69/58.83 inference(scs_inference,[],[74,1252,1984,1983,76,330,1131,312,1172,90,97,128,2,88,89,99,920,903,100,138,131,129,130,104,151,125,84,94,103,248,132])). % 58.69/58.83 cnf(3554,plain, % 58.69/58.83 (P7(f12(a5))), % 58.69/58.83 inference(scs_inference,[],[74,1252,1984,1983,76,330,1131,312,1172,90,97,128,2,88,89,99,920,903,100,138,131,129,130,104,151,125,84,94,103,248,132,85])). % 58.69/58.83 cnf(3567,plain, % 58.69/58.83 (~E(x35671,f12(a5))+~P16(x35671,a5)), % 58.69/58.83 inference(scs_inference,[],[3522,1366])). % 58.69/58.83 cnf(3596,plain, % 58.69/58.83 (P3(f13(a5))), % 58.69/58.83 inference(scs_inference,[],[3515,3513,3542,1469,3567,90,84,2,138,129])). % 58.69/58.83 cnf(3605,plain, % 58.69/58.83 (P8(f6(a5),f13(a5))), % 58.69/58.83 inference(scs_inference,[],[74,3515,3513,3532,3546,3542,1469,1194,1696,3567,90,84,2,138,129,131,1268,137,46,1160])). % 58.69/58.83 cnf(3614,plain, % 58.69/58.83 (~P12(f12(a5),f12(a5),a4)), % 58.69/58.83 inference(scs_inference,[],[74,3552,3515,3513,3532,3546,3542,1700,1469,1194,78,71,1215,1688,1696,3567,90,84,2,138,129,131,1268,137,46,1160,55,104,141,38,151])). % 58.69/58.83 cnf(3616,plain, % 58.69/58.83 (P5(f12(a5),a23)), % 58.69/58.83 inference(scs_inference,[],[74,3544,3552,3515,3513,3532,3546,3542,1700,1469,1194,78,71,70,1215,1688,1696,312,3567,90,84,2,138,129,131,1268,137,46,1160,55,104,141,38,151,116])). % 58.69/58.83 cnf(3624,plain, % 58.69/58.83 (P8(f12(a5),f13(a5))), % 58.69/58.83 inference(scs_inference,[],[74,3544,3552,3515,3513,3532,3546,3542,1700,1469,1194,78,71,70,1215,1688,1696,312,3567,90,84,2,138,129,131,1268,137,46,1160,55,104,141,38,151,116,284,356,680,94])). % 58.69/58.83 cnf(3632,plain, % 58.69/58.83 (P7(f13(a5))), % 58.69/58.83 inference(scs_inference,[],[74,3544,3552,3515,3513,3532,3546,3542,1700,1469,1194,78,71,70,1215,1688,1696,312,3567,90,84,2,138,129,131,1268,137,46,1160,55,104,141,38,151,116,284,356,680,94,248,133,381,85])). % 58.69/58.83 cnf(3679,plain, % 58.69/58.83 (~P12(f13(a5),f6(a5),x36791)), % 58.69/58.83 inference(scs_inference,[],[3624,1360,3546,1287,2,138,1163])). % 58.69/58.83 cnf(3685,plain, % 58.69/58.83 (~E(a1,f14(a5))), % 58.69/58.83 inference(scs_inference,[],[3605,3616,3624,3632,3554,1700,1360,3546,69,1287,2,138,1163,101,102,38])). % 58.69/58.83 cnf(3699,plain, % 58.69/58.83 (~P6(f6(a5),f14(a5))), % 58.69/58.83 inference(scs_inference,[],[3614,3685,3548,3624,300,3513,1696,2,62,41,104])). % 58.69/58.83 cnf(3702,plain, % 58.69/58.83 (P12(f6(a5),f13(a5),a4)), % 58.69/58.83 inference(scs_inference,[],[74,3614,3679,3596,3685,3536,3548,3624,300,3513,1283,330,325,1688,1696,2,62,41,104,54,142])). % 58.69/58.83 cnf(3719,plain, % 58.69/58.83 ($false), % 58.69/58.83 inference(scs_inference,[],[74,3699,3702,3528,3522,244,3513,1193,1688,1696,2,49,41,139,140,106]), % 58.69/58.83 ['proof']). % 58.69/58.83 % SZS output end Proof % 58.69/58.83 % Total time :58.160000s %------------------------------------------------------------------------------