%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN718-1 : TPTP v8.2.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n024.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 19:06:24 EDT 2024 % Result : Unsatisfiable 58.74s 58.80s % Output : CNFRefutation 58.74s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SYN718-1 : TPTP v8.2.0. Released v2.5.0. % 0.11/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.32 % Computer : n024.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.32 % CPULimit : 300 % 0.12/0.32 % WCLimit : 300 % 0.12/0.32 % DateTime : Sun Jun 23 18:27:39 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.55 start to proof:theBenchmark % 58.74/58.77 %------------------------------------------- % 58.74/58.77 % File :CSE---1.7 % 58.74/58.77 % Problem :theBenchmark % 58.74/58.77 % Transform :cnf % 58.74/58.77 % Format :tptp:raw % 58.74/58.77 % Command :java -jar mcs_scs.jar %d %s % 58.74/58.77 % 58.74/58.77 % Result :Theorem 58.170000s % 58.74/58.77 % Output :CNFRefutation 58.170000s % 58.74/58.77 %------------------------------------------- % 58.74/58.78 %-------------------------------------------------------------------------- % 58.74/58.78 % File : SYN718-1 : TPTP v8.2.0. Released v2.5.0. % 58.74/58.78 % Domain : Syntactic % 58.74/58.78 % Problem : Harrison problem 4761 % 58.74/58.78 % Version : Especial. % 58.74/58.78 % English : % 58.74/58.78 % 58.74/58.78 % Refs : [Har01] Email to G. Sutcliffe % 58.74/58.78 % Source : [Har01] % 58.74/58.78 % Names : % 58.74/58.78 % 58.74/58.78 % Status : Unsatisfiable % 58.74/58.78 % Rating : 0.25 v8.2.0, 0.14 v8.1.0, 0.00 v7.1.0, 0.17 v7.0.0, 0.25 v6.3.0, 0.14 v6.2.0, 0.11 v6.1.0, 0.00 v5.0.0, 0.14 v4.1.0, 0.00 v2.5.0 % 58.74/58.78 % Syntax : Number of clauses : 118 ( 43 unt; 5 nHn; 84 RR) % 58.74/58.78 % Number of literals : 276 ( 0 equ; 157 neg) % 58.74/58.78 % Maximal clause size : 4 ( 2 avg) % 58.74/58.78 % Maximal term depth : 7 ( 1 avg) % 58.74/58.78 % Number of predicates : 39 ( 39 usr; 0 prp; 2-2 aty) % 58.74/58.78 % Number of functors : 53 ( 53 usr; 31 con; 0-2 aty) % 58.74/58.78 % Number of variables : 300 ( 7 sgn) % 58.74/58.78 % SPC : CNF_UNS_RFO_NEQ_NHN % 58.74/58.78 % 58.74/58.78 % Comments : % 58.74/58.78 %-------------------------------------------------------------------------- % 58.74/58.78 cnf(p11_1,negated_conjecture, % 58.74/58.78 p11(X0,X0) ). % 58.74/58.78 % 58.74/58.78 cnf(p9_2,negated_conjecture, % 58.74/58.78 p9(X237,X237) ). % 58.74/58.78 % 58.74/58.78 cnf(p7_3,negated_conjecture, % 58.74/58.78 p7(X230,X230) ). % 58.74/58.78 % 58.74/58.78 cnf(p6_4,negated_conjecture, % 58.74/58.78 p6(X211,X211) ). % 58.74/58.78 % 58.74/58.78 cnf(p58_5,negated_conjecture, % 58.74/58.78 p58(X204,X204) ). % 58.74/58.78 % 58.74/58.78 cnf(p54_6,negated_conjecture, % 58.74/58.78 p54(X181,X181) ). % 58.74/58.78 % 58.74/58.78 cnf(p52_7,negated_conjecture, % 58.74/58.78 p52(X174,X174) ). % 58.74/58.78 % 58.74/58.78 cnf(p50_8,negated_conjecture, % 58.74/58.78 p50(X167,X167) ). % 58.74/58.78 % 58.74/58.78 cnf(p49_9,negated_conjecture, % 58.74/58.78 p49(X164,X164) ). % 58.74/58.78 % 58.74/58.78 cnf(p47_10,negated_conjecture, % 58.74/58.78 p47(X161,X161) ). % 58.74/58.78 % 58.74/58.78 cnf(p45_11,negated_conjecture, % 58.74/58.78 p45(X154,X154) ). % 58.74/58.78 % 58.74/58.78 cnf(p43_12,negated_conjecture, % 58.74/58.78 p43(X147,X147) ). % 58.74/58.78 % 58.74/58.78 cnf(p41_13,negated_conjecture, % 58.74/58.78 p41(X144,X144) ). % 58.74/58.78 % 58.74/58.78 cnf(p4_14,negated_conjecture, % 58.74/58.78 p4(X133,X133) ). % 58.74/58.78 % 58.74/58.78 cnf(p39_15,negated_conjecture, % 58.74/58.78 p39(X126,X126) ). % 58.74/58.78 % 58.74/58.78 cnf(p37_16,negated_conjecture, % 58.74/58.78 p37(X119,X119) ). % 58.74/58.78 % 58.74/58.78 cnf(p35_17,negated_conjecture, % 58.74/58.78 p35(X116,X116) ). % 58.74/58.78 % 58.74/58.78 cnf(p33_18,negated_conjecture, % 58.74/58.78 p33(X105,X105) ). % 58.74/58.78 % 58.74/58.78 cnf(p31_19,negated_conjecture, % 58.74/58.78 p31(X102,X102) ). % 58.74/58.78 % 58.74/58.78 cnf(p3_20,negated_conjecture, % 58.74/58.78 p3(X75,X75) ). % 58.74/58.78 % 58.74/58.78 cnf(p29_21,negated_conjecture, % 58.74/58.78 p29(X72,X72) ). % 58.74/58.78 % 58.74/58.78 cnf(p27_22,negated_conjecture, % 58.74/58.78 p27(X69,X69) ). % 58.74/58.78 % 58.74/58.78 cnf(p25_23,negated_conjecture, % 58.74/58.78 p25(X58,X58) ). % 58.74/58.78 % 58.74/58.78 cnf(p23_24,negated_conjecture, % 58.74/58.78 p23(X55,X55) ). % 58.74/58.78 % 58.74/58.78 cnf(p21_25,negated_conjecture, % 58.74/58.78 p21(X48,X48) ). % 58.74/58.78 % 58.74/58.78 cnf(p20_26,negated_conjecture, % 58.74/58.78 p20(X41,X41) ). % 58.74/58.78 % 58.74/58.78 cnf(p2_27,negated_conjecture, % 58.74/58.78 p2(X38,X38) ). % 58.74/58.78 % 58.74/58.78 cnf(p18_28,negated_conjecture, % 58.74/58.78 p18(X23,X23) ). % 58.74/58.78 % 58.74/58.78 cnf(p16_29,negated_conjecture, % 58.74/58.78 p16(X12,X12) ). % 58.74/58.78 % 58.74/58.78 cnf(p15_30,negated_conjecture, % 58.74/58.78 p15(X9,X9) ). % 58.74/58.78 % 58.74/58.78 cnf(p14_31,negated_conjecture, % 58.74/58.79 p14(X6,X6) ). % 58.74/58.79 % 58.74/58.79 cnf(p12_32,negated_conjecture, % 58.74/58.79 p12(X3,X3) ). % 58.74/58.79 % 58.74/58.79 cnf(p60_33,negated_conjecture, % 58.74/58.79 p60(c77,c70) ). % 58.74/58.79 % 58.74/58.79 cnf(p55_34,negated_conjecture, % 58.74/58.79 p55(c63,c64) ). % 58.74/58.79 % 58.74/58.79 cnf(p59_35,negated_conjecture, % 58.74/58.79 p59(c74,f28(c75,c78)) ). % 58.74/58.79 % 58.74/58.79 cnf(p3_36,negated_conjecture, % 58.74/58.79 p3(c84,f10(c72,c73)) ). % 58.74/58.79 % 58.74/58.79 cnf(p59_37,negated_conjecture, % 58.74/58.79 p59(c74,f28(c75,c76)) ). % 58.74/58.79 % 58.74/58.79 cnf(p16_38,negated_conjecture, % 58.74/58.79 p16(f17(c68,c69),c70) ). % 58.74/58.79 % 58.74/58.79 cnf(p11_39,negated_conjecture, % 58.74/58.79 ( p11(X1,X2) % 58.74/58.79 | ~ p11(X0,X1) % 58.74/58.79 | ~ p11(X0,X2) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p9_40,negated_conjecture, % 58.74/58.79 ( p9(X238,X239) % 58.74/58.79 | ~ p9(X237,X238) % 58.74/58.79 | ~ p9(X237,X239) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p7_41,negated_conjecture, % 58.74/58.79 ( p7(X231,X232) % 58.74/58.79 | ~ p7(X230,X231) % 58.74/58.79 | ~ p7(X230,X232) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p6_42,negated_conjecture, % 58.74/58.79 ( p6(X212,X213) % 58.74/58.79 | ~ p6(X211,X212) % 58.74/58.79 | ~ p6(X211,X213) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p58_43,negated_conjecture, % 58.74/58.79 ( p58(X205,X206) % 58.74/58.79 | ~ p58(X204,X205) % 58.74/58.79 | ~ p58(X204,X206) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p54_44,negated_conjecture, % 58.74/58.79 ( p54(X182,X183) % 58.74/58.79 | ~ p54(X181,X182) % 58.74/58.79 | ~ p54(X181,X183) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p52_45,negated_conjecture, % 58.74/58.79 ( p52(X175,X176) % 58.74/58.79 | ~ p52(X174,X175) % 58.74/58.79 | ~ p52(X174,X176) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p50_46,negated_conjecture, % 58.74/58.79 ( p50(X168,X169) % 58.74/58.79 | ~ p50(X167,X168) % 58.74/58.79 | ~ p50(X167,X169) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p49_47,negated_conjecture, % 58.74/58.79 ( p49(X165,X166) % 58.74/58.79 | ~ p49(X164,X165) % 58.74/58.79 | ~ p49(X164,X166) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p47_48,negated_conjecture, % 58.74/58.79 ( p47(X162,X163) % 58.74/58.79 | ~ p47(X161,X162) % 58.74/58.79 | ~ p47(X161,X163) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p45_49,negated_conjecture, % 58.74/58.79 ( p45(X155,X156) % 58.74/58.79 | ~ p45(X154,X155) % 58.74/58.79 | ~ p45(X154,X156) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p43_50,negated_conjecture, % 58.74/58.79 ( p43(X148,X149) % 58.74/58.79 | ~ p43(X147,X148) % 58.74/58.79 | ~ p43(X147,X149) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p41_51,negated_conjecture, % 58.74/58.79 ( p41(X145,X146) % 58.74/58.79 | ~ p41(X144,X145) % 58.74/58.79 | ~ p41(X144,X146) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p4_52,negated_conjecture, % 58.74/58.79 ( p4(X134,X135) % 58.74/58.79 | ~ p4(X133,X134) % 58.74/58.79 | ~ p4(X133,X135) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p39_53,negated_conjecture, % 58.74/58.79 ( p39(X127,X128) % 58.74/58.79 | ~ p39(X126,X127) % 58.74/58.79 | ~ p39(X126,X128) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p37_54,negated_conjecture, % 58.74/58.79 ( p37(X120,X121) % 58.74/58.79 | ~ p37(X119,X120) % 58.74/58.79 | ~ p37(X119,X121) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p35_55,negated_conjecture, % 58.74/58.79 ( p35(X117,X118) % 58.74/58.79 | ~ p35(X116,X117) % 58.74/58.79 | ~ p35(X116,X118) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p33_56,negated_conjecture, % 58.74/58.79 ( p33(X106,X107) % 58.74/58.79 | ~ p33(X105,X106) % 58.74/58.79 | ~ p33(X105,X107) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p31_57,negated_conjecture, % 58.74/58.79 ( p31(X103,X104) % 58.74/58.79 | ~ p31(X102,X103) % 58.74/58.79 | ~ p31(X102,X104) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p3_58,negated_conjecture, % 58.74/58.79 ( p3(X76,X77) % 58.74/58.79 | ~ p3(X75,X76) % 58.74/58.79 | ~ p3(X75,X77) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p29_59,negated_conjecture, % 58.74/58.79 ( p29(X73,X74) % 58.74/58.79 | ~ p29(X72,X73) % 58.74/58.79 | ~ p29(X72,X74) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p27_60,negated_conjecture, % 58.74/58.79 ( p27(X70,X71) % 58.74/58.79 | ~ p27(X69,X70) % 58.74/58.79 | ~ p27(X69,X71) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p25_61,negated_conjecture, % 58.74/58.79 ( p25(X59,X60) % 58.74/58.79 | ~ p25(X58,X59) % 58.74/58.79 | ~ p25(X58,X60) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p23_62,negated_conjecture, % 58.74/58.79 ( p23(X56,X57) % 58.74/58.79 | ~ p23(X55,X56) % 58.74/58.79 | ~ p23(X55,X57) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p21_63,negated_conjecture, % 58.74/58.79 ( p21(X49,X50) % 58.74/58.79 | ~ p21(X48,X49) % 58.74/58.79 | ~ p21(X48,X50) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p20_64,negated_conjecture, % 58.74/58.79 ( p20(X42,X43) % 58.74/58.79 | ~ p20(X41,X42) % 58.74/58.79 | ~ p20(X41,X43) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p2_65,negated_conjecture, % 58.74/58.79 ( p2(X39,X40) % 58.74/58.79 | ~ p2(X38,X39) % 58.74/58.79 | ~ p2(X38,X40) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p18_66,negated_conjecture, % 58.74/58.79 ( p18(X24,X25) % 58.74/58.79 | ~ p18(X23,X24) % 58.74/58.79 | ~ p18(X23,X25) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p16_67,negated_conjecture, % 58.74/58.79 ( p16(X13,X14) % 58.74/58.79 | ~ p16(X12,X13) % 58.74/58.79 | ~ p16(X12,X14) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p15_68,negated_conjecture, % 58.74/58.79 ( p15(X10,X11) % 58.74/58.79 | ~ p15(X9,X10) % 58.74/58.79 | ~ p15(X9,X11) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p14_69,negated_conjecture, % 58.74/58.79 ( p14(X7,X8) % 58.74/58.79 | ~ p14(X6,X7) % 58.74/58.79 | ~ p14(X6,X8) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p12_70,negated_conjecture, % 58.74/58.79 ( p12(X4,X5) % 58.74/58.79 | ~ p12(X3,X4) % 58.74/58.79 | ~ p12(X3,X5) ) ). % 58.74/58.79 % 58.74/58.79 cnf(not_p3_71,negated_conjecture, % 58.74/58.79 ~ p3(f19(f5(c66,f10(c72,c73)),c83),f10(c72,c73)) ). % 58.74/58.79 % 58.74/58.79 cnf(p57_72,negated_conjecture, % 58.74/58.79 ( p57(f26(f30(c85,X197),X198),X199) % 58.74/58.79 | ~ p57(f26(X197,X198),X199) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p62_73,negated_conjecture, % 58.74/58.79 ( p62(X226,X227) % 58.74/58.79 | ~ p52(X229,X226) % 58.74/58.79 | ~ p62(X229,X228) % 58.74/58.79 | ~ p18(X228,X227) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p55_74,negated_conjecture, % 58.74/58.79 ( p55(X184,X185) % 58.74/58.79 | ~ p54(X187,X184) % 58.74/58.79 | ~ p55(X187,X186) % 58.74/58.79 | ~ p12(X186,X185) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p56_75,negated_conjecture, % 58.74/58.79 ( p56(X188,X189) % 58.74/58.79 | ~ p56(X191,X190) % 58.74/58.79 | ~ p7(X191,X188) % 58.74/58.79 | ~ p4(X190,X189) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p57_76,negated_conjecture, % 58.74/58.79 ( p57(X193,X194) % 58.74/58.79 | ~ p25(X196,X193) % 58.74/58.79 | ~ p57(X196,X195) % 58.74/58.79 | ~ p21(X195,X194) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p59_77,negated_conjecture, % 58.74/58.79 ( p59(X207,X208) % 58.74/58.79 | ~ p58(X210,X207) % 58.74/58.79 | ~ p59(X210,X209) % 58.74/58.79 | ~ p25(X209,X208) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p60_78,negated_conjecture, % 58.74/58.79 ( p60(X218,X219) % 58.74/58.79 | ~ p16(X221,X219) % 58.74/58.79 | ~ p60(X220,X221) % 58.74/58.79 | ~ p15(X220,X218) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p61_79,negated_conjecture, % 58.74/58.79 ( p61(X222,X223) % 58.74/58.79 | ~ p50(X225,X222) % 58.74/58.79 | ~ p61(X225,X224) % 58.74/58.79 | ~ p3(X224,X223) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p57_80,negated_conjecture, % 58.74/58.79 p57(f26(c70,f22(f24(c71,c81),c82)),f22(f24(c71,c83),c84)) ). % 58.74/58.79 % 58.74/58.79 cnf(p57_81,negated_conjecture, % 58.74/58.79 p57(f26(c70,f22(f24(c71,c79),c80)),f22(f24(c71,c81),c82)) ). % 58.74/58.79 % 58.74/58.79 cnf(p56_82,negated_conjecture, % 58.74/58.79 p56(f8(f13(c65,c64),f5(c66,f10(c67,X192))),f5(c66,X192)) ). % 58.74/58.79 % 58.74/58.79 cnf(p16_83,negated_conjecture, % 58.74/58.79 ( p16(f17(X15,X16),f17(X17,X18)) % 58.74/58.79 | ~ p14(X15,X17) % 58.74/58.79 | ~ p15(X16,X18) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p9_84,negated_conjecture, % 58.74/58.79 ( p9(f32(X240,X241),f32(X242,X243)) % 58.74/58.79 | ~ p3(X241,X243) % 58.74/58.79 | ~ p31(X240,X242) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p7_85,negated_conjecture, % 58.74/58.79 ( p7(f8(X233,X234),f8(X235,X236)) % 58.74/58.79 | ~ p4(X234,X236) % 58.74/58.79 | ~ p6(X233,X235) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p6_86,negated_conjecture, % 58.74/58.79 ( p6(f13(X214,X215),f13(X216,X217)) % 58.74/58.79 | ~ p11(X214,X216) % 58.74/58.79 | ~ p12(X215,X217) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p52_87,negated_conjecture, % 58.74/58.79 ( p52(f53(X177,X178),f53(X179,X180)) % 58.74/58.79 | ~ p12(X177,X179) % 58.74/58.79 | ~ p18(X178,X180) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p50_88,negated_conjecture, % 58.74/58.79 ( p50(f51(X170,X171),f51(X172,X173)) % 58.74/58.79 | ~ p3(X171,X173) % 58.74/58.79 | ~ p49(X170,X172) ) ). % 58.74/58.79 % 58.74/58.79 cnf(p45_89,negated_conjecture, % 58.74/58.79 ( p45(f48(X157,X158),f48(X159,X160)) % 58.74/58.79 | ~ p3(X158,X160) % 58.74/58.79 | ~ p47(X157,X159) ) ). % 58.74/58.79 % 58.74/58.80 cnf(p43_90,negated_conjecture, % 58.74/58.80 ( p43(f46(X150,X151),f46(X152,X153)) % 58.74/58.80 | ~ p3(X151,X153) % 58.74/58.80 | ~ p45(X150,X152) ) ). % 58.74/58.80 % 58.74/58.80 cnf(p4_91,negated_conjecture, % 58.74/58.80 ( p4(f5(X140,X141),f5(X142,X143)) % 58.74/58.80 | ~ p2(X140,X142) % 58.74/58.80 | ~ p3(X141,X143) ) ). % 58.74/58.80 % 58.74/58.80 cnf(p4_92,negated_conjecture, % 58.74/58.80 ( p4(f38(X136,X137),f38(X138,X139)) % 58.74/58.80 | ~ p18(X137,X139) % 58.74/58.80 | ~ p37(X136,X138) ) ). % 58.74/58.80 % 58.74/58.80 cnf(p39_93,negated_conjecture, % 58.74/58.80 ( p39(f42(X129,X130),f42(X131,X132)) % 58.74/58.80 | ~ p3(X130,X132) % 58.74/58.80 | ~ p41(X129,X131) ) ). % 58.74/58.80 % 58.74/58.80 cnf(p37_94,negated_conjecture, % 58.74/58.80 ( p37(f40(X122,X123),f40(X124,X125)) % 58.74/58.80 | ~ p3(X123,X125) % 58.74/58.80 | ~ p39(X122,X124) ) ). % 58.74/58.80 % 58.74/58.80 cnf(p33_95,negated_conjecture, % 58.74/58.80 ( p33(f44(X112,X113),f44(X114,X115)) % 58.74/58.80 | ~ p18(X113,X115) % 58.74/58.80 | ~ p43(X112,X114) ) ). % 58.74/58.80 % 58.74/58.80 cnf(p33_96,negated_conjecture, % 58.74/58.80 ( p33(f36(X108,X109),f36(X110,X111)) % 58.74/58.80 | ~ p3(X109,X111) % 58.74/58.80 | ~ p35(X108,X110) ) ). % 58.74/58.80 % 58.74/58.80 cnf(p3_97,negated_conjecture, % 58.74/58.80 ( p3(f19(X96,X97),f19(X98,X99)) % 58.74/58.80 | ~ p18(X97,X99) % 58.74/58.80 | ~ p4(X96,X98) ) ). % 58.74/58.80 % 58.74/58.80 cnf(p3_98,negated_conjecture, % 58.74/58.80 ( p3(f10(X92,X93),f10(X94,X95)) % 58.74/58.80 | ~ p3(X93,X95) % 58.74/58.80 | ~ p9(X92,X94) ) ). % 58.74/58.80 % 58.74/58.80 cnf(p25_99,negated_conjecture, % 58.74/58.80 ( p25(f28(X65,X66),f28(X67,X68)) % 58.74/58.80 | ~ p25(X66,X68) % 58.74/58.80 | ~ p27(X65,X67) ) ). % 58.74/58.80 % 58.74/58.80 cnf(p25_100,negated_conjecture, % 58.74/58.80 ( p25(f26(X61,X62),f26(X63,X64)) % 58.74/58.80 | ~ p16(X61,X63) % 58.74/58.80 | ~ p21(X62,X64) ) ). % 58.74/58.80 % 58.74/58.80 cnf(p21_101,negated_conjecture, % 58.74/58.80 ( p21(f22(X51,X52),f22(X53,X54)) % 58.74/58.80 | ~ p20(X51,X53) % 58.74/58.80 | ~ p3(X52,X54) ) ). % 58.74/58.80 % 58.74/58.80 cnf(p20_102,negated_conjecture, % 58.74/58.80 ( p20(f24(X44,X45),f24(X46,X47)) % 58.74/58.80 | ~ p18(X45,X47) % 58.74/58.80 | ~ p23(X44,X46) ) ). % 58.74/58.80 % 58.74/58.80 cnf(p18_103,negated_conjecture, % 58.74/58.80 ( p18(f34(X34,X35),f34(X36,X37)) % 58.74/58.80 | ~ p18(X35,X37) % 58.74/58.80 | ~ p33(X34,X36) ) ). % 58.74/58.80 % 58.74/58.80 cnf(p16_104,negated_conjecture, % 58.74/58.80 ( p16(f30(X19,X20),f30(X21,X22)) % 58.74/58.80 | ~ p16(X20,X22) % 58.74/58.80 | ~ p29(X19,X21) ) ). % 58.74/58.80 % 58.74/58.80 cnf(not_p57_105,negated_conjecture, % 58.74/58.80 ~ p57(f26(f30(c85,c70),f22(f24(c71,c79),c80)),f22(f24(c71,c83),f10(c72,c73))) ). % 58.74/58.80 % 58.74/58.80 cnf(p18_106,negated_conjecture, % 58.74/58.80 ( p18(X30,X31) % 58.74/58.80 | p62(f53(c64,X30),X31) % 58.74/58.80 | ~ p57(f26(c70,f22(f24(c71,X30),X32)),f22(f24(c71,X31),X33)) ) ). % 58.74/58.80 % 58.74/58.80 cnf(p57_107,negated_conjecture, % 58.74/58.80 ( p57(f26(f30(c85,X200),X201),X202) % 58.74/58.80 | ~ p57(f26(f30(c85,X200),X201),X203) % 58.74/58.80 | ~ p57(f26(f30(c85,X200),X203),X202) ) ). % 58.74/58.80 % 58.74/58.80 cnf(p18_108,negated_conjecture, % 58.74/58.80 ( p18(X26,X27) % 58.74/58.80 | ~ p3(f19(f5(c66,X28),X26),f10(c72,c73)) % 58.74/58.80 | ~ p57(f26(c70,f22(f24(c71,X26),X28)),f22(f24(c71,X27),X29)) ) ). % 58.74/58.80 % 58.74/58.80 cnf(p3_109,negated_conjecture, % 58.74/58.80 ( p3(X78,X79) % 58.74/58.80 | ~ p57(f26(c70,f22(f24(c71,X80),X78)),f22(f24(c71,X81),X82)) % 58.74/58.80 | ~ p57(f26(c70,f22(f24(c71,X83),X79)),f22(f24(c71,X81),X82)) ) ). % 58.74/58.80 % 58.74/58.80 cnf(p62_110,negated_conjecture, % 58.74/58.80 ( p62(f53(c64,X30),X31) % 58.74/58.80 | p61(f51(c92,f19(f5(c66,X32),X31)),f19(f5(c66,X33),X31)) % 58.74/58.80 | ~ p57(f26(c70,f22(f24(c71,X30),X32)),f22(f24(c71,X31),X33)) ) ). % 58.74/58.80 % 58.74/58.80 cnf(not_p57_111,negated_conjecture, % 58.74/58.80 ( ~ p57(f26(c70,f22(f24(c71,X101),X100)),f22(f24(c71,X244),X245)) % 58.74/58.80 | ~ p3(f19(f5(c66,X100),X101),f19(f5(c66,f10(f32(c88,X100),f10(c72,f10(c89,c73)))),X101)) ) ). % 58.74/58.80 % 58.74/58.80 cnf(p3_112,negated_conjecture, % 58.74/58.80 ( p3(f19(f5(c66,X100),X101),f19(f5(c66,f10(f32(c88,X100),f10(c72,f10(c89,c73)))),X101)) % 58.74/58.80 | p57(f26(c70,f22(f24(c71,X101),X100)),f22(f24(c71,f34(f36(c86,X100),X101)),f19(f5(c87,X100),X101))) ) ). % 58.74/58.80 % 58.74/58.80 cnf(p3_113,negated_conjecture, % 58.74/58.80 ( p3(X88,f10(c72,c73)) % 58.74/58.80 | ~ p61(f51(c92,X90),c80) % 58.74/58.80 | ~ p57(f26(c70,f22(f24(c71,X89),X90)),f22(f24(c71,X91),X88)) % 58.74/58.80 | ~ p3(f19(f5(c66,f10(c72,c73)),f34(f44(f46(f48(c93,X90),X88),X89),X91)),f10(c72,c73)) ) ). % 58.74/58.80 % 58.74/58.80 cnf(p3_114,negated_conjecture, % 58.74/58.80 ( p3(X84,f10(c72,c73)) % 58.74/58.80 | p57(f26(c70,f22(f24(c71,X85),X84)),f22(f24(c71,f34(f44(f46(f48(c90,X86),X84),X87),X85)),f19(f38(f40(f42(c91,X86),X84),X87),X85))) % 58.74/58.80 | ~ p57(f26(c70,f22(f24(c71,X87),X86)),f22(f24(c71,X85),X84)) ) ). % 58.74/58.80 % 58.74/58.80 cnf(p3_115,negated_conjecture, % 58.74/58.80 ( p3(X88,f10(c72,c73)) % 58.74/58.80 | p57(f26(f30(c85,c70),f22(f24(c71,X89),X90)),f22(f24(c71,f34(f44(f46(f48(c93,X90),X88),X89),X91)),f10(c72,c73))) % 58.74/58.80 | ~ p61(f51(c92,X90),c80) % 58.74/58.80 | ~ p57(f26(c70,f22(f24(c71,X89),X90)),f22(f24(c71,X91),X88)) ) ). % 58.74/58.80 % 58.74/58.80 cnf(not_p61_116,negated_conjecture, % 58.74/58.80 ( ~ p61(f51(c92,X90),c80) % 58.74/58.80 | ~ p3(f19(f5(c66,f10(c72,c73)),X91),f10(c72,c73)) % 58.74/58.80 | ~ p57(f26(c70,f22(f24(c71,X89),X90)),f22(f24(c71,X91),X88)) % 58.74/58.80 | ~ p3(f19(f5(c66,f10(c72,c73)),f34(f44(f46(f48(c93,X90),X88),X89),X91)),f10(c72,c73)) ) ). % 58.74/58.80 % 58.74/58.80 cnf(p57_117,negated_conjecture, % 58.74/58.80 ( p57(f26(c70,f22(f24(c71,X85),X84)),f22(f24(c71,f34(f44(f46(f48(c90,X86),X84),X87),X85)),f19(f38(f40(f42(c91,X86),X84),X87),X85))) % 58.74/58.80 | ~ p3(f19(f5(c66,f10(c72,c73)),X85),f10(c72,c73)) % 58.74/58.80 | ~ p57(f26(c70,f22(f24(c71,X87),X86)),f22(f24(c71,X85),X84)) ) ). % 58.74/58.80 % 58.74/58.80 cnf(p57_118,negated_conjecture, % 58.74/58.80 ( p57(f26(f30(c85,c70),f22(f24(c71,X89),X90)),f22(f24(c71,f34(f44(f46(f48(c93,X90),X88),X89),X91)),f10(c72,c73))) % 58.74/58.80 | ~ p61(f51(c92,X90),c80) % 58.74/58.80 | ~ p3(f19(f5(c66,f10(c72,c73)),X91),f10(c72,c73)) % 58.74/58.80 | ~ p57(f26(c70,f22(f24(c71,X89),X90)),f22(f24(c71,X91),X88)) ) ). % 58.74/58.80 % 58.74/58.80 %-------------------------------------------------------------------------- % 58.74/58.80 %------------------------------------------- % 58.74/58.80 % Proof found % 58.74/58.80 % SZS status Theorem for theBenchmark % 58.74/58.80 % SZS output start Proof % 58.74/58.80 %ClaNum:118(EqnAxiom:0) % 58.74/58.80 %VarNum:633(SingletonVarNum:300) % 58.74/58.80 %MaxLitNum:4 % 58.74/58.80 %MaxfuncDepth:5 % 58.74/58.80 %SharedTerms:61 % 58.74/58.80 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 % 58.74/58.80 %singleGoalClaCount:43 % 58.74/58.80 [1]P1(a1,a2) % 58.74/58.80 [2]P2(a3,a4) % 58.74/58.80 [35]P18(a16,f23(a10,a12)) % 58.74/58.80 [36]P35(a13,f33(a14,a17)) % 58.74/58.80 [37]P35(a13,f33(a14,a15)) % 58.74/58.80 [38]P27(f34(a5,a9),a2) % 58.74/58.80 [39]P33(f39(a2,f37(f36(a11,a18),a21)),f37(f36(a11,a22),a16)) % 58.74/58.80 [40]P33(f39(a2,f37(f36(a11,a19),a20)),f37(f36(a11,a18),a21)) % 58.74/58.80 [42]~P18(f38(f40(a7,f23(a10,a12)),a22),f23(a10,a12)) % 58.74/58.80 [43]~P33(f39(f41(a24,a2),f37(f36(a11,a19),a20)),f37(f36(a11,a22),f23(a10,a12))) % 58.74/58.80 [3]P3(x31,x31) % 58.74/58.80 [4]P36(x41,x41) % 58.74/58.80 [5]P37(x51,x51) % 58.74/58.80 [6]P31(x61,x61) % 58.74/58.80 [7]P32(x71,x71) % 58.74/58.80 [8]P4(x81,x81) % 58.74/58.80 [9]P5(x91,x91) % 58.74/58.80 [10]P6(x101,x101) % 58.74/58.80 [11]P7(x111,x111) % 58.74/58.80 [12]P8(x121,x121) % 58.74/58.80 [13]P9(x131,x131) % 58.74/58.80 [14]P10(x141,x141) % 58.74/58.80 [15]P11(x151,x151) % 58.74/58.80 [16]P12(x161,x161) % 58.74/58.80 [17]P13(x171,x171) % 58.74/58.80 [18]P14(x181,x181) % 58.74/58.80 [19]P15(x191,x191) % 58.74/58.80 [20]P16(x201,x201) % 58.74/58.80 [21]P17(x211,x211) % 58.74/58.80 [22]P18(x221,x221) % 58.74/58.80 [23]P19(x231,x231) % 58.74/58.80 [24]P20(x241,x241) % 58.74/58.80 [25]P21(x251,x251) % 58.74/58.80 [26]P22(x261,x261) % 58.74/58.80 [27]P23(x271,x271) % 58.74/58.80 [28]P24(x281,x281) % 58.74/58.80 [29]P25(x291,x291) % 58.74/58.80 [30]P26(x301,x301) % 58.74/58.80 [31]P27(x311,x311) % 58.74/58.80 [32]P28(x321,x321) % 58.74/58.80 [33]P29(x331,x331) % 58.74/58.80 [34]P30(x341,x341) % 58.74/58.80 [41]P34(f51(f35(a6,a4),f40(a7,f23(a8,x411))),f40(a7,x411)) % 58.74/58.80 [111]P33(f39(a2,f37(f36(a11,x1112),x1111)),f37(f36(a11,f47(f46(a27,x1111),x1112)),f38(f40(a28,x1111),x1112)))+P18(f38(f40(a7,x1111),x1112),f38(f40(a7,f23(f42(a26,x1111),f23(a10,f23(a29,a12)))),x1112)) % 58.74/58.80 [105]~P33(f39(x1051,x1052),x1053)+P33(f39(f41(a24,x1051),x1052),x1053) % 58.74/58.80 [112]~P33(f39(a2,f37(f36(a11,x1121),x1122)),f37(f36(a11,x1123),x1124))+~P18(f38(f40(a7,x1122),x1121),f38(f40(a7,f23(f42(a26,x1122),f23(a10,f23(a29,a12)))),x1121)) % 58.74/58.80 [44]~P3(x443,x441)+P3(x441,x442)+~P3(x443,x442) % 58.74/58.80 [45]~P36(x453,x451)+P36(x451,x452)+~P36(x453,x452) % 58.74/58.80 [46]~P37(x463,x461)+P37(x461,x462)+~P37(x463,x462) % 58.74/58.80 [47]~P31(x473,x471)+P31(x471,x472)+~P31(x473,x472) % 58.74/58.80 [48]~P32(x483,x481)+P32(x481,x482)+~P32(x483,x482) % 58.74/58.80 [49]~P4(x493,x491)+P4(x491,x492)+~P4(x493,x492) % 58.74/58.80 [50]~P5(x503,x501)+P5(x501,x502)+~P5(x503,x502) % 58.74/58.80 [51]~P6(x513,x511)+P6(x511,x512)+~P6(x513,x512) % 58.74/58.80 [52]~P7(x523,x521)+P7(x521,x522)+~P7(x523,x522) % 58.74/58.80 [53]~P8(x533,x531)+P8(x531,x532)+~P8(x533,x532) % 58.74/58.80 [54]~P9(x543,x541)+P9(x541,x542)+~P9(x543,x542) % 58.74/58.80 [55]~P10(x553,x551)+P10(x551,x552)+~P10(x553,x552) % 58.74/58.80 [56]~P11(x563,x561)+P11(x561,x562)+~P11(x563,x562) % 58.74/58.80 [57]~P12(x573,x571)+P12(x571,x572)+~P12(x573,x572) % 58.74/58.80 [58]~P13(x583,x581)+P13(x581,x582)+~P13(x583,x582) % 58.74/58.80 [59]~P14(x593,x591)+P14(x591,x592)+~P14(x593,x592) % 58.74/58.80 [60]~P15(x603,x601)+P15(x601,x602)+~P15(x603,x602) % 58.74/58.80 [61]~P16(x613,x611)+P16(x611,x612)+~P16(x613,x612) % 58.74/58.80 [62]~P17(x623,x621)+P17(x621,x622)+~P17(x623,x622) % 58.74/58.80 [63]~P18(x633,x631)+P18(x631,x632)+~P18(x633,x632) % 58.74/58.80 [64]~P19(x643,x641)+P19(x641,x642)+~P19(x643,x642) % 58.74/58.80 [65]~P20(x653,x651)+P20(x651,x652)+~P20(x653,x652) % 58.74/58.80 [66]~P21(x663,x661)+P21(x661,x662)+~P21(x663,x662) % 58.74/58.80 [67]~P22(x673,x671)+P22(x671,x672)+~P22(x673,x672) % 58.74/58.80 [68]~P23(x683,x681)+P23(x681,x682)+~P23(x683,x682) % 58.74/58.80 [69]~P24(x693,x691)+P24(x691,x692)+~P24(x693,x692) % 58.74/58.80 [70]~P25(x703,x701)+P25(x701,x702)+~P25(x703,x702) % 58.74/58.80 [71]~P26(x713,x711)+P26(x711,x712)+~P26(x713,x712) % 58.74/58.80 [72]~P27(x723,x721)+P27(x721,x722)+~P27(x723,x722) % 58.74/58.80 [73]~P28(x733,x731)+P28(x731,x732)+~P28(x733,x732) % 58.74/58.80 [74]~P29(x743,x741)+P29(x741,x742)+~P29(x743,x742) % 58.74/58.80 [75]~P30(x753,x751)+P30(x751,x752)+~P30(x753,x752) % 58.74/58.80 [83]~P17(x831,x833)+~P18(x832,x834)+P36(f42(x831,x832),f42(x833,x834)) % 58.74/58.80 [84]~P31(x841,x843)+~P12(x842,x844)+P37(f51(x841,x842),f51(x843,x844)) % 58.74/58.80 [85]~P3(x851,x853)+~P30(x852,x854)+P31(f35(x851,x852),f35(x853,x854)) % 58.74/58.80 [86]~P26(x862,x864)+~P30(x861,x863)+P5(f52(x861,x862),f52(x863,x864)) % 58.74/58.80 [87]~P7(x871,x873)+~P18(x872,x874)+P6(f53(x871,x872),f53(x873,x874)) % 58.74/58.80 [88]~P8(x881,x883)+~P18(x882,x884)+P9(f43(x881,x882),f43(x883,x884)) % 58.74/58.80 [89]~P9(x891,x893)+~P18(x892,x894)+P10(f44(x891,x892),f44(x893,x894)) % 58.74/58.80 [90]~P18(x902,x904)+~P25(x901,x903)+P12(f40(x901,x902),f40(x903,x904)) % 58.74/58.80 [91]~P14(x911,x913)+~P26(x912,x914)+P12(f45(x911,x912),f45(x913,x914)) % 58.74/58.80 [92]~P11(x921,x923)+~P18(x922,x924)+P13(f48(x921,x922),f48(x923,x924)) % 58.74/58.80 [93]~P13(x931,x933)+~P18(x932,x934)+P14(f49(x931,x932),f49(x933,x934)) % 58.74/58.80 [94]~P10(x941,x943)+~P26(x942,x944)+P16(f50(x941,x942),f50(x943,x944)) % 58.74/58.80 [95]~P15(x951,x953)+~P18(x952,x954)+P16(f46(x951,x952),f46(x953,x954)) % 58.74/58.80 [96]~P36(x961,x963)+~P18(x962,x964)+P18(f23(x961,x962),f23(x963,x964)) % 58.74/58.80 [97]~P12(x971,x973)+~P26(x972,x974)+P18(f38(x971,x972),f38(x973,x974)) % 58.74/58.80 [98]~P20(x981,x983)+~P21(x982,x984)+P21(f33(x981,x982),f33(x983,x984)) % 58.74/58.80 [99]~P23(x992,x994)+~P27(x991,x993)+P21(f39(x991,x992),f39(x993,x994)) % 58.74/58.80 [100]~P18(x1002,x1004)+~P24(x1001,x1003)+P23(f37(x1001,x1002),f37(x1003,x1004)) % 58.74/58.80 [101]~P22(x1011,x1013)+~P26(x1012,x1014)+P24(f36(x1011,x1012),f36(x1013,x1014)) % 58.74/58.80 [102]~P16(x1021,x1023)+~P26(x1022,x1024)+P26(f47(x1021,x1022),f47(x1023,x1024)) % 58.74/58.80 [103]~P28(x1032,x1034)+~P29(x1031,x1033)+P27(f34(x1031,x1032),f34(x1033,x1034)) % 58.74/58.80 [104]~P19(x1041,x1043)+~P27(x1042,x1044)+P27(f41(x1041,x1042),f41(x1043,x1044)) % 58.74/58.80 [106]~P33(f39(f41(a24,x1061),x1062),x1064)+~P33(f39(f41(a24,x1061),x1064),x1063)+P33(f39(f41(a24,x1061),x1062),x1063) % 58.74/58.80 [107]P26(x1071,x1072)+P38(f52(a4,x1071),x1072)+~P33(f39(a2,f37(f36(a11,x1071),x1073)),f37(f36(a11,x1072),x1074)) % 58.74/58.80 [108]P26(x1081,x1082)+~P18(f38(f40(a7,x1083),x1081),f23(a10,a12))+~P33(f39(a2,f37(f36(a11,x1081),x1083)),f37(f36(a11,x1082),x1084)) % 58.74/58.80 [109]P38(f52(a4,x1091),x1092)+~P33(f39(a2,f37(f36(a11,x1091),x1093)),f37(f36(a11,x1092),x1094))+P39(f53(a25,f38(f40(a7,x1093),x1092)),f38(f40(a7,x1094),x1092)) % 58.74/58.80 [117]P18(x1171,f23(a10,a12))+~P33(f39(a2,f37(f36(a11,x1174),x1173)),f37(f36(a11,x1172),x1171))+P33(f39(a2,f37(f36(a11,x1172),x1171)),f37(f36(a11,f47(f50(f44(f43(a30,x1173),x1171),x1174),x1172)),f38(f45(f49(f48(a31,x1173),x1171),x1174),x1172))) % 58.74/58.80 [118]~P18(f38(f40(a7,f23(a10,a12)),x1181),f23(a10,a12))+~P33(f39(a2,f37(f36(a11,x1184),x1183)),f37(f36(a11,x1181),x1182))+P33(f39(a2,f37(f36(a11,x1181),x1182)),f37(f36(a11,f47(f50(f44(f43(a30,x1183),x1182),x1184),x1181)),f38(f45(f49(f48(a31,x1183),x1182),x1184),x1181))) % 58.74/58.80 [110]P18(x1101,x1102)+~P33(f39(a2,f37(f36(a11,x1106),x1101)),f37(f36(a11,x1104),x1105))+~P33(f39(a2,f37(f36(a11,x1103),x1102)),f37(f36(a11,x1104),x1105)) % 58.74/58.80 [76]~P1(x764,x763)+P1(x761,x762)+~P27(x763,x762)+~P28(x764,x761) % 58.74/58.80 [77]~P2(x773,x774)+P2(x771,x772)+~P4(x773,x771)+~P30(x774,x772) % 58.74/58.80 [78]~P35(x783,x784)+P35(x781,x782)+~P32(x783,x781)+~P21(x784,x782) % 58.74/58.80 [79]~P33(x793,x794)+P33(x791,x792)+~P21(x793,x791)+~P23(x794,x792) % 58.74/58.80 [80]~P38(x803,x804)+P38(x801,x802)+~P5(x803,x801)+~P26(x804,x802) % 58.74/58.80 [81]~P34(x813,x814)+P34(x811,x812)+~P37(x813,x811)+~P12(x814,x812) % 58.74/58.80 [82]~P39(x823,x824)+P39(x821,x822)+~P6(x823,x821)+~P18(x824,x822) % 58.74/58.80 [115]P18(x1151,f23(a10,a12))+~P39(f53(a25,x1153),a20)+P33(f39(f41(a24,a2),f37(f36(a11,x1152),x1153)),f37(f36(a11,f47(f50(f44(f43(a32,x1153),x1151),x1152),x1154)),f23(a10,a12)))+~P33(f39(a2,f37(f36(a11,x1152),x1153)),f37(f36(a11,x1154),x1151)) % 58.74/58.80 [116]~P39(f53(a25,x1162),a20)+~P18(f38(f40(a7,f23(a10,a12)),x1164),f23(a10,a12))+P33(f39(f41(a24,a2),f37(f36(a11,x1161),x1162)),f37(f36(a11,f47(f50(f44(f43(a32,x1162),x1163),x1161),x1164)),f23(a10,a12)))+~P33(f39(a2,f37(f36(a11,x1161),x1162)),f37(f36(a11,x1164),x1163)) % 58.74/58.80 [113]P18(x1131,f23(a10,a12))+~P39(f53(a25,x1132),a20)+~P33(f39(a2,f37(f36(a11,x1133),x1132)),f37(f36(a11,x1134),x1131))+~P18(f38(f40(a7,f23(a10,a12)),f47(f50(f44(f43(a32,x1132),x1131),x1133),x1134)),f23(a10,a12)) % 58.74/58.80 [114]~P39(f53(a25,x1141),a20)+~P18(f38(f40(a7,f23(a10,a12)),x1142),f23(a10,a12))+~P33(f39(a2,f37(f36(a11,x1143),x1141)),f37(f36(a11,x1142),x1144))+~P18(f38(f40(a7,f23(a10,a12)),f47(f50(f44(f43(a32,x1141),x1144),x1143),x1142)),f23(a10,a12)) % 58.74/58.80 %EqnAxiom % 58.74/58.80 % 58.74/58.80 %------------------------------------------- % 58.74/58.80 cnf(130,plain, % 58.74/58.80 (P18(f23(a10,a12),a16)), % 58.74/58.80 inference(scs_inference,[],[35,22,63])). % 58.74/58.80 cnf(147,plain, % 58.74/58.80 (P27(a2,f34(a5,a9))), % 58.74/58.80 inference(scs_inference,[],[38,31,72])). % 58.74/58.80 cnf(468,plain, % 58.74/58.80 (P18(f23(x4681,f23(a10,a12)),f23(x4681,a16))), % 58.74/58.80 inference(scs_inference,[],[4,130,45,96])). % 58.74/58.80 cnf(661,plain, % 58.74/58.80 (P9(f43(x6611,f23(x6612,f23(a10,a12))),f43(x6611,f23(x6612,a16)))), % 58.74/58.80 inference(scs_inference,[],[12,468,53,88])). % 58.74/58.80 cnf(712,plain, % 58.74/58.80 (P13(f48(x7121,f23(x7122,f23(a10,a12))),f48(x7121,f23(x7122,a16)))), % 58.74/58.80 inference(scs_inference,[],[15,468,56,92])). % 58.74/58.80 cnf(713,plain, % 58.74/58.80 (P13(f48(x7131,f23(x7132,a16)),f48(x7131,f23(x7132,f23(a10,a12))))), % 58.74/58.80 inference(scs_inference,[],[712,17,58])). % 58.74/58.80 cnf(780,plain, % 58.74/58.80 (P36(f42(x7801,f23(x7802,f23(a10,a12))),f42(x7801,f23(x7802,a16)))), % 58.74/58.80 inference(scs_inference,[],[21,468,62,83])). % 58.74/58.80 cnf(799,plain, % 58.74/58.80 (P27(f41(x7991,a2),f41(x7991,f34(a5,a9)))), % 58.74/58.80 inference(scs_inference,[],[23,147,64,104])). % 58.74/58.80 cnf(811,plain, % 58.74/58.80 (P27(f41(x8111,f34(a5,a9)),f41(x8111,a2))), % 58.74/58.80 inference(scs_inference,[],[799,31,72])). % 58.74/58.80 cnf(898,plain, % 58.74/58.80 (P21(f39(f41(x8981,a2),x8982),f39(f41(x8981,f34(a5,a9)),x8982))), % 58.74/58.80 inference(scs_inference,[],[27,799,68,99])). % 58.74/58.80 cnf(902,plain, % 58.74/58.80 (~P33(f39(f41(a24,f34(a5,a9)),f37(f36(a11,a19),a20)),f37(f36(a11,a22),f23(a10,a12)))), % 58.74/58.80 inference(scs_inference,[],[898,25,43,27,66,79])). % 58.74/58.80 cnf(960,plain, % 58.74/58.80 (P23(f37(x9601,f23(a10,a12)),f37(x9601,a16))), % 58.74/58.80 inference(scs_inference,[],[28,130,69,100])). % 58.74/58.80 cnf(961,plain, % 58.74/58.80 (P23(f37(x9611,a16),f37(x9611,f23(a10,a12)))), % 58.74/58.80 inference(scs_inference,[],[960,27,68])). % 58.74/58.80 cnf(972,plain, % 58.74/58.80 (~P33(f39(f41(a24,a2),f37(f36(a11,a19),a20)),f37(f36(a11,a22),a16))), % 58.74/58.80 inference(scs_inference,[],[898,902,961,79])). % 58.74/58.80 cnf(1336,plain, % 58.74/58.80 (P12(f40(x13361,f23(a10,a12)),f40(x13361,a16))), % 58.74/58.80 inference(scs_inference,[],[29,130,70,90])). % 58.74/58.80 cnf(1337,plain, % 58.74/58.80 (P12(f40(x13371,a16),f40(x13371,f23(a10,a12)))), % 58.74/58.80 inference(scs_inference,[],[1336,16,57])). % 58.74/58.80 cnf(1576,plain, % 58.74/58.80 (P14(f49(f48(x15761,f23(x15762,f23(a10,a12))),f23(a10,a12)),f49(f48(x15761,f23(x15762,f23(a10,a12))),a16))), % 58.74/58.80 inference(scs_inference,[],[130,713,93,58])). % 58.74/58.80 cnf(1577,plain, % 58.74/58.80 (P14(f49(f48(x15771,f23(x15772,f23(a10,a12))),a16),f49(f48(x15771,f23(x15772,f23(a10,a12))),f23(a10,a12)))), % 58.74/58.80 inference(scs_inference,[],[1576,18,59])). % 58.74/58.80 cnf(1595,plain, % 58.74/58.80 (P16(f50(f44(f43(x15951,f23(x15952,f23(a10,a12))),f23(x15953,f23(a10,a12))),x15954),f50(f44(f43(x15951,f23(x15952,a16)),f23(x15953,a16)),x15954))), % 58.74/58.80 inference(scs_inference,[],[30,661,468,94,89])). % 58.74/58.80 cnf(1611,plain, % 58.74/58.80 (P18(f38(f40(x16111,f23(a10,a12)),x16112),f38(f40(x16111,a16),x16112))), % 58.74/58.80 inference(scs_inference,[],[30,29,130,97,90])). % 58.74/58.80 cnf(1627,plain, % 58.74/58.80 (P21(f33(x16271,f39(f41(x16272,a2),x16273)),f33(x16271,f39(f41(x16272,f34(a5,a9)),x16273)))), % 58.74/58.80 inference(scs_inference,[],[898,24,98,65])). % 58.74/58.80 cnf(1638,plain, % 58.74/58.80 (P21(f33(x16381,f39(f41(x16382,f34(a5,a9)),x16383)),f33(x16381,f39(f41(x16382,a2),x16383)))), % 58.74/58.80 inference(scs_inference,[],[1627,25,66])). % 58.74/58.80 cnf(7583,plain, % 58.74/58.80 (P18(f23(x75831,a16),f23(x75831,f23(a10,a12)))), % 58.74/58.80 inference(scs_inference,[],[468,22,63])). % 58.74/58.80 cnf(8566,plain, % 58.74/58.80 (~P33(f39(f41(a24,a2),f37(f36(a11,a19),a20)),f37(f36(a11,a18),a21))), % 58.74/58.80 inference(scs_inference,[],[7583,1611,1595,811,13,17,780,11,12,15,19,21,1577,29,24,1638,23,1337,30,972,39,112,105,83,87,88,89,90,91,92,93,95,96,97,98,102,104,106])). % 58.74/58.80 cnf(8781,plain, % 58.74/58.80 ($false), % 58.74/58.80 inference(scs_inference,[],[8566,40,105]), % 58.74/58.80 ['proof']). % 58.74/58.80 % SZS output end Proof % 58.74/58.80 % Total time :58.170000s %------------------------------------------------------------------------------