%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN712-1 : TPTP v8.2.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/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 19:06:23 EDT 2024 % Result : Unsatisfiable 58.45s 58.44s % Output : CNFRefutation 58.45s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN712-1 : TPTP v8.2.0. Released v2.5.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n023.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Sun Jun 23 23:17:39 EDT 2024 % 0.12/0.33 % CPUTime : % 0.51/0.56 start to proof:theBenchmark % 58.36/58.42 %------------------------------------------- % 58.36/58.42 % File :CSE---1.7 % 58.36/58.42 % Problem :theBenchmark % 58.36/58.42 % Transform :cnf % 58.36/58.42 % Format :tptp:raw % 58.36/58.42 % Command :java -jar mcs_scs.jar %d %s % 58.36/58.42 % 58.36/58.42 % Result :Theorem 57.810000s % 58.36/58.42 % Output :CNFRefutation 57.810000s % 58.36/58.42 %------------------------------------------- % 58.36/58.43 %-------------------------------------------------------------------------- % 58.36/58.43 % File : SYN712-1 : TPTP v8.2.0. Released v2.5.0. % 58.36/58.43 % Domain : Syntactic % 58.36/58.43 % Problem : Harrison problem 4748 % 58.36/58.43 % Version : Especial. % 58.36/58.43 % English : % 58.36/58.43 % 58.36/58.43 % Refs : [Har01] Email to G. Sutcliffe % 58.36/58.43 % Source : [Har01] % 58.36/58.43 % Names : % 58.36/58.43 % 58.36/58.43 % Status : Unsatisfiable % 58.36/58.43 % Rating : 0.00 v8.1.0, 0.25 v7.4.0, 0.17 v7.3.0, 0.25 v6.2.0, 0.17 v6.1.0, 0.07 v6.0.0, 0.11 v5.5.0, 0.06 v5.4.0, 0.11 v5.3.0, 0.20 v5.2.0, 0.15 v5.1.0, 0.12 v5.0.0, 0.13 v4.0.1, 0.14 v3.7.0, 0.00 v2.5.0 % 58.36/58.43 % Syntax : Number of clauses : 104 ( 36 unt; 0 nHn; 69 RR) % 58.36/58.43 % Number of literals : 236 ( 0 equ; 134 neg) % 58.36/58.43 % Maximal clause size : 4 ( 2 avg) % 58.36/58.43 % Maximal term depth : 9 ( 1 avg) % 58.36/58.43 % Number of predicates : 35 ( 35 usr; 0 prp; 2-2 aty) % 58.36/58.43 % Number of functors : 40 ( 40 usr; 13 con; 0-2 aty) % 58.36/58.43 % Number of variables : 285 ( 9 sgn) % 58.36/58.43 % SPC : CNF_UNS_RFO_NEQ_HRN % 58.36/58.43 % 58.36/58.43 % Comments : % 58.36/58.43 %-------------------------------------------------------------------------- % 58.36/58.43 cnf(p10_1,negated_conjecture, % 58.36/58.43 p10(X0,X0) ). % 58.36/58.43 % 58.36/58.43 cnf(p9_2,negated_conjecture, % 58.36/58.43 p9(X218,X218) ). % 58.36/58.43 % 58.36/58.43 cnf(p7_3,negated_conjecture, % 58.36/58.43 p7(X211,X211) ). % 58.36/58.43 % 58.36/58.43 cnf(p60_4,negated_conjecture, % 58.36/58.43 p60(X196,X196) ). % 58.36/58.43 % 58.36/58.43 cnf(p6_5,negated_conjecture, % 58.36/58.43 p6(X189,X189) ). % 58.36/58.43 % 58.36/58.43 cnf(p58_6,negated_conjecture, % 58.36/58.43 p58(X182,X182) ). % 58.36/58.43 % 58.36/58.43 cnf(p56_7,negated_conjecture, % 58.36/58.43 p56(X175,X175) ). % 58.36/58.43 % 58.36/58.43 cnf(p54_8,negated_conjecture, % 58.36/58.43 p54(X168,X168) ). % 58.36/58.43 % 58.36/58.43 cnf(p52_9,negated_conjecture, % 58.36/58.43 p52(X161,X161) ). % 58.36/58.43 % 58.36/58.43 cnf(p50_10,negated_conjecture, % 58.36/58.43 p50(X158,X158) ). % 58.36/58.43 % 58.36/58.43 cnf(p48_11,negated_conjecture, % 58.36/58.43 p48(X151,X151) ). % 58.36/58.43 % 58.36/58.43 cnf(p46_12,negated_conjecture, % 58.36/58.43 p46(X144,X144) ). % 58.36/58.43 % 58.36/58.43 cnf(p44_13,negated_conjecture, % 58.36/58.43 p44(X137,X137) ). % 58.36/58.43 % 58.36/58.43 cnf(p42_14,negated_conjecture, % 58.36/58.43 p42(X130,X130) ). % 58.36/58.43 % 58.36/58.43 cnf(p40_15,negated_conjecture, % 58.36/58.43 p40(X127,X127) ). % 58.36/58.43 % 58.36/58.43 cnf(p4_16,negated_conjecture, % 58.36/58.43 p4(X116,X116) ). % 58.36/58.43 % 58.36/58.43 cnf(p38_17,negated_conjecture, % 58.36/58.43 p38(X109,X109) ). % 58.36/58.43 % 58.36/58.43 cnf(p35_18,negated_conjecture, % 58.36/58.43 p35(X102,X102) ). % 58.36/58.43 % 58.36/58.43 cnf(p34_19,negated_conjecture, % 58.36/58.43 p34(X95,X95) ). % 58.36/58.43 % 58.36/58.43 cnf(p32_20,negated_conjecture, % 58.36/58.43 p32(X92,X92) ). % 58.36/58.43 % 58.36/58.43 cnf(p30_21,negated_conjecture, % 58.36/58.43 p30(X89,X89) ). % 58.36/58.43 % 58.36/58.43 cnf(p3_22,negated_conjecture, % 58.36/58.43 p3(X78,X78) ). % 58.36/58.43 % 58.36/58.43 cnf(p28_23,negated_conjecture, % 58.36/58.43 p28(X71,X71) ). % 58.36/58.43 % 58.36/58.43 cnf(p26_24,negated_conjecture, % 58.36/58.43 p26(X64,X64) ). % 58.36/58.43 % 58.36/58.43 cnf(p24_25,negated_conjecture, % 58.36/58.43 p24(X57,X57) ). % 58.36/58.43 % 58.36/58.43 cnf(p22_26,negated_conjecture, % 58.36/58.43 p22(X50,X50) ). % 58.36/58.43 % 58.36/58.43 cnf(p20_27,negated_conjecture, % 58.36/58.43 p20(X47,X47) ). % 58.36/58.43 % 58.36/58.43 cnf(p2_28,negated_conjecture, % 58.36/58.43 p2(X44,X44) ). % 58.36/58.43 % 58.36/58.43 cnf(p18_29,negated_conjecture, % 58.36/58.43 p18(X37,X37) ). % 58.36/58.43 % 58.36/58.43 cnf(p17_30,negated_conjecture, % 58.36/58.43 p17(X30,X30) ). % 58.36/58.43 % 58.36/58.43 cnf(p15_31,negated_conjecture, % 58.36/58.43 p15(X17,X17) ). % 58.36/58.43 % 58.36/58.43 cnf(p14_32,negated_conjecture, % 58.36/58.43 p14(X10,X10) ). % 58.36/58.43 % 58.36/58.43 cnf(p12_33,negated_conjecture, % 58.36/58.43 p12(X7,X7) ). % 58.36/58.43 % 58.36/58.43 cnf(p10_34,negated_conjecture, % 58.36/58.43 ( p10(X1,X2) % 58.36/58.43 | ~ p10(X0,X1) % 58.36/58.43 | ~ p10(X0,X2) ) ). % 58.36/58.43 % 58.36/58.43 cnf(p9_35,negated_conjecture, % 58.36/58.43 ( p9(X219,X220) % 58.36/58.43 | ~ p9(X218,X219) % 58.36/58.43 | ~ p9(X218,X220) ) ). % 58.36/58.43 % 58.36/58.43 cnf(p7_36,negated_conjecture, % 58.36/58.43 ( p7(X212,X213) % 58.36/58.43 | ~ p7(X211,X212) % 58.36/58.43 | ~ p7(X211,X213) ) ). % 58.36/58.43 % 58.36/58.43 cnf(p60_37,negated_conjecture, % 58.36/58.43 ( p60(X197,X198) % 58.36/58.43 | ~ p60(X196,X197) % 58.36/58.43 | ~ p60(X196,X198) ) ). % 58.36/58.43 % 58.36/58.43 cnf(p6_38,negated_conjecture, % 58.36/58.43 ( p6(X190,X191) % 58.36/58.43 | ~ p6(X189,X190) % 58.36/58.43 | ~ p6(X189,X191) ) ). % 58.36/58.43 % 58.36/58.43 cnf(p58_39,negated_conjecture, % 58.36/58.43 ( p58(X183,X184) % 58.36/58.43 | ~ p58(X182,X183) % 58.36/58.43 | ~ p58(X182,X184) ) ). % 58.36/58.43 % 58.36/58.43 cnf(p56_40,negated_conjecture, % 58.36/58.43 ( p56(X176,X177) % 58.36/58.43 | ~ p56(X175,X176) % 58.36/58.43 | ~ p56(X175,X177) ) ). % 58.36/58.43 % 58.36/58.43 cnf(p54_41,negated_conjecture, % 58.36/58.43 ( p54(X169,X170) % 58.36/58.43 | ~ p54(X168,X169) % 58.36/58.43 | ~ p54(X168,X170) ) ). % 58.36/58.43 % 58.36/58.43 cnf(p52_42,negated_conjecture, % 58.36/58.43 ( p52(X162,X163) % 58.36/58.43 | ~ p52(X161,X162) % 58.36/58.43 | ~ p52(X161,X163) ) ). % 58.36/58.43 % 58.36/58.43 cnf(p50_43,negated_conjecture, % 58.36/58.43 ( p50(X159,X160) % 58.36/58.43 | ~ p50(X158,X159) % 58.36/58.43 | ~ p50(X158,X160) ) ). % 58.36/58.43 % 58.36/58.43 cnf(p48_44,negated_conjecture, % 58.36/58.43 ( p48(X152,X153) % 58.36/58.43 | ~ p48(X151,X152) % 58.36/58.43 | ~ p48(X151,X153) ) ). % 58.36/58.43 % 58.36/58.43 cnf(p46_45,negated_conjecture, % 58.36/58.43 ( p46(X145,X146) % 58.36/58.43 | ~ p46(X144,X145) % 58.36/58.43 | ~ p46(X144,X146) ) ). % 58.36/58.43 % 58.36/58.43 cnf(p44_46,negated_conjecture, % 58.36/58.43 ( p44(X138,X139) % 58.36/58.43 | ~ p44(X137,X138) % 58.36/58.43 | ~ p44(X137,X139) ) ). % 58.36/58.43 % 58.36/58.43 cnf(p42_47,negated_conjecture, % 58.36/58.43 ( p42(X131,X132) % 58.36/58.43 | ~ p42(X130,X131) % 58.36/58.43 | ~ p42(X130,X132) ) ). % 58.36/58.43 % 58.36/58.43 cnf(p40_48,negated_conjecture, % 58.36/58.43 ( p40(X128,X129) % 58.36/58.43 | ~ p40(X127,X128) % 58.36/58.43 | ~ p40(X127,X129) ) ). % 58.36/58.43 % 58.36/58.43 cnf(p4_49,negated_conjecture, % 58.36/58.43 ( p4(X117,X118) % 58.36/58.43 | ~ p4(X116,X117) % 58.36/58.43 | ~ p4(X116,X118) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p38_50,negated_conjecture, % 58.36/58.44 ( p38(X110,X111) % 58.36/58.44 | ~ p38(X109,X110) % 58.36/58.44 | ~ p38(X109,X111) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p35_51,negated_conjecture, % 58.36/58.44 ( p35(X103,X104) % 58.36/58.44 | ~ p35(X102,X103) % 58.36/58.44 | ~ p35(X102,X104) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p34_52,negated_conjecture, % 58.36/58.44 ( p34(X96,X97) % 58.36/58.44 | ~ p34(X95,X96) % 58.36/58.44 | ~ p34(X95,X97) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p32_53,negated_conjecture, % 58.36/58.44 ( p32(X93,X94) % 58.36/58.44 | ~ p32(X92,X93) % 58.36/58.44 | ~ p32(X92,X94) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p30_54,negated_conjecture, % 58.36/58.44 ( p30(X90,X91) % 58.36/58.44 | ~ p30(X89,X90) % 58.36/58.44 | ~ p30(X89,X91) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p3_55,negated_conjecture, % 58.36/58.44 ( p3(X79,X80) % 58.36/58.44 | ~ p3(X78,X79) % 58.36/58.44 | ~ p3(X78,X80) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p28_56,negated_conjecture, % 58.36/58.44 ( p28(X72,X73) % 58.36/58.44 | ~ p28(X71,X72) % 58.36/58.44 | ~ p28(X71,X73) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p26_57,negated_conjecture, % 58.36/58.44 ( p26(X65,X66) % 58.36/58.44 | ~ p26(X64,X65) % 58.36/58.44 | ~ p26(X64,X66) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p24_58,negated_conjecture, % 58.36/58.44 ( p24(X58,X59) % 58.36/58.44 | ~ p24(X57,X58) % 58.36/58.44 | ~ p24(X57,X59) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p22_59,negated_conjecture, % 58.36/58.44 ( p22(X51,X52) % 58.36/58.44 | ~ p22(X50,X51) % 58.36/58.44 | ~ p22(X50,X52) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p20_60,negated_conjecture, % 58.36/58.44 ( p20(X48,X49) % 58.36/58.44 | ~ p20(X47,X48) % 58.36/58.44 | ~ p20(X47,X49) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p2_61,negated_conjecture, % 58.36/58.44 ( p2(X45,X46) % 58.36/58.44 | ~ p2(X44,X45) % 58.36/58.44 | ~ p2(X44,X46) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p18_62,negated_conjecture, % 58.36/58.44 ( p18(X38,X39) % 58.36/58.44 | ~ p18(X37,X38) % 58.36/58.44 | ~ p18(X37,X39) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p17_63,negated_conjecture, % 58.36/58.44 ( p17(X31,X32) % 58.36/58.44 | ~ p17(X30,X31) % 58.36/58.44 | ~ p17(X30,X32) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p15_64,negated_conjecture, % 58.36/58.44 ( p15(X18,X19) % 58.36/58.44 | ~ p15(X17,X18) % 58.36/58.44 | ~ p15(X17,X19) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p14_65,negated_conjecture, % 58.36/58.44 ( p14(X11,X12) % 58.36/58.44 | ~ p14(X10,X11) % 58.36/58.44 | ~ p14(X10,X12) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p12_66,negated_conjecture, % 58.36/58.44 ( p12(X8,X9) % 58.36/58.44 | ~ p12(X7,X8) % 58.36/58.44 | ~ p12(X7,X9) ) ). % 58.36/58.44 % 58.36/58.44 cnf(not_p62_67,negated_conjecture, % 58.36/58.44 ~ p62(f5(c64,f8(f11(f13(c65,c66),c67),c68)),c69) ). % 58.36/58.44 % 58.36/58.44 cnf(p63_68,negated_conjecture, % 58.36/58.44 ( p63(X207,X208) % 58.36/58.44 | ~ p35(X210,X207) % 58.36/58.44 | ~ p63(X210,X209) % 58.36/58.44 | ~ p15(X209,X208) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p62_69,negated_conjecture, % 58.36/58.44 ( p62(X199,X200) % 58.36/58.44 | ~ p4(X202,X199) % 58.36/58.44 | ~ p62(X202,X201) % 58.36/58.44 | ~ p32(X201,X200) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p10_70,negated_conjecture, % 58.36/58.44 ( p10(f43(X3,X4),f43(X5,X6)) % 58.36/58.44 | ~ p15(X4,X6) % 58.36/58.44 | ~ p42(X3,X5) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p9_71,negated_conjecture, % 58.36/58.44 ( p9(f13(X221,X222),f13(X223,X224)) % 58.36/58.44 | ~ p12(X221,X223) % 58.36/58.44 | ~ p4(X222,X224) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p7_72,negated_conjecture, % 58.36/58.44 ( p7(f53(X214,X215),f53(X216,X217)) % 58.36/58.44 | ~ p15(X215,X217) % 58.36/58.44 | ~ p52(X214,X216) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p6_73,negated_conjecture, % 58.36/58.44 ( p6(f11(X192,X193),f11(X194,X195)) % 58.36/58.44 | ~ p10(X193,X195) % 58.36/58.44 | ~ p9(X192,X194) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p58_74,negated_conjecture, % 58.36/58.44 ( p58(f61(X185,X186),f61(X187,X188)) % 58.36/58.44 | ~ p4(X186,X188) % 58.36/58.44 | ~ p60(X185,X187) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p56_75,negated_conjecture, % 58.36/58.44 ( p56(f59(X178,X179),f59(X180,X181)) % 58.36/58.44 | ~ p10(X179,X181) % 58.36/58.44 | ~ p58(X178,X180) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p54_76,negated_conjecture, % 58.36/58.44 ( p54(f57(X171,X172),f57(X173,X174)) % 58.36/58.44 | ~ p56(X171,X173) % 58.36/58.44 | ~ p7(X172,X174) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p52_77,negated_conjecture, % 58.36/58.44 ( p52(f55(X164,X165),f55(X166,X167)) % 58.36/58.44 | ~ p18(X165,X167) % 58.36/58.44 | ~ p54(X164,X166) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p48_78,negated_conjecture, % 58.36/58.44 ( p48(f51(X154,X155),f51(X156,X157)) % 58.36/58.44 | ~ p4(X155,X157) % 58.36/58.44 | ~ p50(X154,X156) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p46_79,negated_conjecture, % 58.36/58.44 ( p46(f49(X147,X148),f49(X149,X150)) % 58.36/58.44 | ~ p10(X148,X150) % 58.36/58.44 | ~ p48(X147,X149) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p44_80,negated_conjecture, % 58.36/58.44 ( p44(f47(X140,X141),f47(X142,X143)) % 58.36/58.44 | ~ p46(X140,X142) % 58.36/58.44 | ~ p7(X141,X143) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p42_81,negated_conjecture, % 58.36/58.44 ( p42(f45(X133,X134),f45(X135,X136)) % 58.36/58.44 | ~ p18(X134,X136) % 58.36/58.44 | ~ p44(X133,X135) ) ). % 58.36/58.44 % 58.36/58.44 cnf(p4_82,negated_conjecture, % 58.36/58.44 ( p4(f5(X123,X124),f5(X125,X126)) % 58.36/58.44 | ~ p2(X123,X125) % 58.45/58.44 | ~ p3(X124,X126) ) ). % 58.45/58.44 % 58.45/58.44 cnf(p4_83,negated_conjecture, % 58.45/58.44 ( p4(f23(X119,X120),f23(X121,X122)) % 58.45/58.44 | ~ p15(X120,X122) % 58.45/58.44 | ~ p22(X119,X121) ) ). % 58.45/58.44 % 58.45/58.44 cnf(p38_84,negated_conjecture, % 58.45/58.44 ( p38(f41(X112,X113),f41(X114,X115)) % 58.45/58.44 | ~ p18(X113,X115) % 58.45/58.44 | ~ p40(X112,X114) ) ). % 58.45/58.44 % 58.45/58.44 cnf(p35_85,negated_conjecture, % 58.45/58.44 ( p35(f36(X105,X106),f36(X107,X108)) % 58.45/58.44 | ~ p18(X106,X108) % 58.45/58.44 | ~ p34(X105,X107) ) ). % 58.45/58.44 % 58.45/58.44 cnf(p34_86,negated_conjecture, % 58.45/58.44 ( p34(f39(X98,X99),f39(X100,X101)) % 58.45/58.44 | ~ p15(X99,X101) % 58.45/58.44 | ~ p38(X98,X100) ) ). % 58.45/58.44 % 58.45/58.44 cnf(p3_87,negated_conjecture, % 58.45/58.44 ( p3(f8(X85,X86),f8(X87,X88)) % 58.45/58.44 | ~ p6(X85,X87) % 58.45/58.44 | ~ p7(X86,X88) ) ). % 58.45/58.44 % 58.45/58.44 cnf(p3_88,negated_conjecture, % 58.45/58.44 ( p3(f16(X81,X82),f16(X83,X84)) % 58.45/58.44 | ~ p14(X81,X83) % 58.45/58.44 | ~ p15(X82,X84) ) ). % 58.45/58.44 % 58.45/58.44 cnf(p28_89,negated_conjecture, % 58.45/58.44 ( p28(f31(X74,X75),f31(X76,X77)) % 58.45/58.44 | ~ p30(X74,X76) % 58.45/58.44 | ~ p4(X75,X77) ) ). % 58.45/58.44 % 58.45/58.44 cnf(p26_90,negated_conjecture, % 58.45/58.44 ( p26(f29(X67,X68),f29(X69,X70)) % 58.45/58.44 | ~ p10(X68,X70) % 58.45/58.44 | ~ p28(X67,X69) ) ). % 58.45/58.44 % 58.45/58.44 cnf(p24_91,negated_conjecture, % 58.45/58.44 ( p24(f27(X60,X61),f27(X62,X63)) % 58.45/58.44 | ~ p26(X60,X62) % 58.45/58.44 | ~ p7(X61,X63) ) ). % 58.45/58.44 % 58.45/58.44 cnf(p22_92,negated_conjecture, % 58.45/58.44 ( p22(f25(X53,X54),f25(X55,X56)) % 58.45/58.44 | ~ p18(X54,X56) % 58.45/58.44 | ~ p24(X53,X55) ) ). % 58.45/58.44 % 58.45/58.44 cnf(p18_93,negated_conjecture, % 58.45/58.44 ( p18(f37(X40,X41),f37(X42,X43)) % 58.45/58.44 | ~ p10(X40,X42) % 58.45/58.44 | ~ p32(X41,X43) ) ). % 58.45/58.44 % 58.45/58.44 cnf(p17_94,negated_conjecture, % 58.45/58.44 ( p17(f21(X33,X34),f21(X35,X36)) % 58.45/58.44 | ~ p20(X33,X35) % 58.45/58.44 | ~ p3(X34,X36) ) ). % 58.45/58.44 % 58.45/58.44 cnf(p15_95,negated_conjecture, % 58.45/58.44 ( p15(f33(X20,X21),f33(X22,X23)) % 58.45/58.44 | ~ p32(X21,X23) % 58.45/58.44 | ~ p7(X20,X22) ) ). % 58.45/58.44 % 58.45/58.44 cnf(p14_96,negated_conjecture, % 58.45/58.44 ( p14(f19(X13,X14),f19(X15,X16)) % 58.45/58.44 | ~ p17(X13,X15) % 58.45/58.44 | ~ p18(X14,X16) ) ). % 58.45/58.44 % 58.45/58.44 cnf(p62_97,negated_conjecture, % 58.45/58.44 ( p62(X203,X204) % 58.45/58.44 | ~ p62(f5(c64,f8(f11(f13(c65,X203),X205),X206)),X204) ) ). % 58.45/58.44 % 58.45/58.44 cnf(p62_98,negated_conjecture, % 58.45/58.44 ( p62(f5(c64,f8(f11(f13(c65,X203),X205),X206)),X204) % 58.45/58.44 | ~ p62(X203,X204) ) ). % 58.45/58.44 % 58.45/58.44 cnf(p62_99,negated_conjecture, % 58.45/58.44 ( p62(X24,X29) % 58.45/58.44 | ~ p62(f23(f25(f27(f29(f31(c74,X24),X25),X26),X27),X28),X29) ) ). % 58.45/58.44 % 58.45/58.44 cnf(p62_100,negated_conjecture, % 58.45/58.44 p62(f5(c64,f16(f19(f21(c70,f8(f11(f13(c65,c66),c67),c68)),c71),c72)),c69) ). % 58.45/58.44 % 58.45/58.44 cnf(not_p63_101,negated_conjecture, % 58.45/58.44 ( ~ p63(f36(f39(f41(c73,X27),X28),f37(X25,X29)),f33(X26,X29)) % 58.45/58.44 | ~ p62(f23(f25(f27(f29(f31(c74,X24),X25),X26),X27),X28),X29) ) ). % 58.45/58.44 % 58.45/58.44 cnf(p15_102,negated_conjecture, % 58.45/58.44 ( p15(f33(f53(f55(f57(f59(f61(c76,X24),X25),X26),X27),X28),X29),f33(X26,X29)) % 58.45/58.44 | ~ p62(f23(f25(f27(f29(f31(c74,X24),X25),X26),X27),X28),X29) ) ). % 58.45/58.44 % 58.45/58.44 cnf(p18_103,negated_conjecture, % 58.45/58.44 ( p18(f37(f43(f45(f47(f49(f51(c75,X24),X25),X26),X27),X28),X29),f37(X25,X29)) % 58.45/58.44 | ~ p62(f23(f25(f27(f29(f31(c74,X24),X25),X26),X27),X28),X29) ) ). % 58.45/58.44 % 58.45/58.44 cnf(p3_104,negated_conjecture, % 58.45/58.44 p3(f16(f19(f21(c70,f8(f11(f13(c65,X24),X25),X26)),X27),X28),f8(f11(f13(c65,f23(f25(f27(f29(f31(c74,X24),X25),X26),X27),X28)),f43(f45(f47(f49(f51(c75,X24),X25),X26),X27),X28)),f53(f55(f57(f59(f61(c76,X24),X25),X26),X27),X28))) ). % 58.45/58.44 % 58.45/58.44 %-------------------------------------------------------------------------- % 58.45/58.44 %------------------------------------------- % 58.45/58.44 % Proof found % 58.45/58.44 % SZS status Theorem for theBenchmark % 58.45/58.44 % SZS output start Proof % 58.45/58.44 %ClaNum:104(EqnAxiom:0) % 58.45/58.44 %VarNum:576(SingletonVarNum:285) % 58.45/58.44 %MaxLitNum:4 % 58.45/58.44 %MaxfuncDepth:7 % 58.45/58.44 %SharedTerms:23 % 58.45/58.44 %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 % 58.45/58.44 %singleGoalClaCount:36 % 58.45/58.44 [36]~P34(f20(a1,f16(f9(f8(a3,a4),a5),a6)),a7) % 58.45/58.44 [34]P34(f20(a1,f19(f18(f17(a2,f16(f9(f8(a3,a4),a5),a6)),a10),a11)),a7) % 58.45/58.44 [1]P1(x11,x11) % 58.45/58.44 [2]P2(x21,x21) % 58.45/58.44 [3]P3(x31,x31) % 58.45/58.44 [4]P4(x41,x41) % 58.45/58.44 [5]P5(x51,x51) % 58.45/58.44 [6]P6(x61,x61) % 58.45/58.44 [7]P7(x71,x71) % 58.45/58.44 [8]P8(x81,x81) % 58.45/58.44 [9]P9(x91,x91) % 58.45/58.44 [10]P10(x101,x101) % 58.45/58.44 [11]P11(x111,x111) % 58.45/58.44 [12]P12(x121,x121) % 58.45/58.44 [13]P13(x131,x131) % 58.45/58.44 [14]P14(x141,x141) % 58.45/58.44 [15]P15(x151,x151) % 58.45/58.44 [16]P16(x161,x161) % 58.45/58.44 [17]P17(x171,x171) % 58.45/58.44 [18]P18(x181,x181) % 58.45/58.45 [19]P19(x191,x191) % 58.45/58.45 [20]P20(x201,x201) % 58.45/58.45 [21]P21(x211,x211) % 58.45/58.45 [22]P22(x221,x221) % 58.45/58.45 [23]P23(x231,x231) % 58.45/58.45 [24]P24(x241,x241) % 58.45/58.45 [25]P25(x251,x251) % 58.45/58.45 [26]P26(x261,x261) % 58.45/58.45 [27]P27(x271,x271) % 58.45/58.45 [28]P28(x281,x281) % 58.45/58.45 [29]P29(x291,x291) % 58.45/58.45 [30]P30(x301,x301) % 58.45/58.45 [31]P31(x311,x311) % 58.45/58.45 [32]P32(x321,x321) % 58.45/58.45 [33]P33(x331,x331) % 58.45/58.45 [35]P22(f19(f18(f17(a2,f16(f9(f8(a3,x351),x352),x353)),x354),x355),f16(f9(f8(a3,f25(f24(f23(f22(f21(a12,x351),x352),x353),x354),x355)),f29(f28(f27(f26(f35(a14,x351),x352),x353),x354),x355)),f40(f39(f38(f37(f36(a15,x351),x352),x353),x354),x355))) % 58.45/58.45 [99]~P34(x991,x994)+P34(f20(a1,f16(f9(f8(a3,x991),x992),x993)),x994) % 58.45/58.45 [100]P34(x1001,x1002)+~P34(f20(a1,f16(f9(f8(a3,x1001),x1003),x1004)),x1002) % 58.45/58.45 [101]P34(x1011,x1012)+~P34(f25(f24(f23(f22(f21(a12,x1011),x1013),x1014),x1015),x1016),x1012) % 58.45/58.45 [102]~P35(f31(f33(f30(a13,x1021),x1022),f34(x1023,x1024)),f32(x1025,x1024))+~P34(f25(f24(f23(f22(f21(a12,x1026),x1023),x1025),x1021),x1022),x1024) % 58.45/58.45 [103]~P34(f25(f24(f23(f22(f21(a12,x1031),x1032),x1033),x1034),x1035),x1036)+P29(f34(f29(f28(f27(f26(f35(a14,x1031),x1032),x1033),x1034),x1035),x1036),f34(x1032,x1036)) % 58.45/58.45 [104]~P34(f25(f24(f23(f22(f21(a12,x1041),x1042),x1043),x1044),x1045),x1046)+P31(f32(f40(f39(f38(f37(f36(a15,x1041),x1042),x1043),x1044),x1045),x1046),f32(x1043,x1046)) % 58.45/58.45 [37]~P1(x373,x371)+P1(x371,x372)+~P1(x373,x372) % 58.45/58.45 [38]~P2(x383,x381)+P2(x381,x382)+~P2(x383,x382) % 58.45/58.45 [39]~P3(x393,x391)+P3(x391,x392)+~P3(x393,x392) % 58.45/58.45 [40]~P4(x403,x401)+P4(x401,x402)+~P4(x403,x402) % 58.45/58.45 [41]~P5(x413,x411)+P5(x411,x412)+~P5(x413,x412) % 58.45/58.45 [42]~P6(x423,x421)+P6(x421,x422)+~P6(x423,x422) % 58.45/58.45 [43]~P7(x433,x431)+P7(x431,x432)+~P7(x433,x432) % 58.45/58.45 [44]~P8(x443,x441)+P8(x441,x442)+~P8(x443,x442) % 58.45/58.45 [45]~P9(x453,x451)+P9(x451,x452)+~P9(x453,x452) % 58.45/58.45 [46]~P10(x463,x461)+P10(x461,x462)+~P10(x463,x462) % 58.45/58.45 [47]~P11(x473,x471)+P11(x471,x472)+~P11(x473,x472) % 58.45/58.45 [48]~P12(x483,x481)+P12(x481,x482)+~P12(x483,x482) % 58.45/58.45 [49]~P13(x493,x491)+P13(x491,x492)+~P13(x493,x492) % 58.45/58.45 [50]~P14(x503,x501)+P14(x501,x502)+~P14(x503,x502) % 58.45/58.45 [51]~P15(x513,x511)+P15(x511,x512)+~P15(x513,x512) % 58.45/58.45 [52]~P16(x523,x521)+P16(x521,x522)+~P16(x523,x522) % 58.45/58.45 [53]~P17(x533,x531)+P17(x531,x532)+~P17(x533,x532) % 58.45/58.45 [54]~P18(x543,x541)+P18(x541,x542)+~P18(x543,x542) % 58.45/58.45 [55]~P19(x553,x551)+P19(x551,x552)+~P19(x553,x552) % 58.45/58.45 [56]~P20(x563,x561)+P20(x561,x562)+~P20(x563,x562) % 58.45/58.45 [57]~P21(x573,x571)+P21(x571,x572)+~P21(x573,x572) % 58.45/58.45 [58]~P22(x583,x581)+P22(x581,x582)+~P22(x583,x582) % 58.45/58.45 [59]~P23(x593,x591)+P23(x591,x592)+~P23(x593,x592) % 58.45/58.45 [60]~P24(x603,x601)+P24(x601,x602)+~P24(x603,x602) % 58.45/58.45 [61]~P25(x613,x611)+P25(x611,x612)+~P25(x613,x612) % 58.45/58.45 [62]~P26(x623,x621)+P26(x621,x622)+~P26(x623,x622) % 58.45/58.45 [63]~P27(x633,x631)+P27(x631,x632)+~P27(x633,x632) % 58.45/58.45 [64]~P28(x643,x641)+P28(x641,x642)+~P28(x643,x642) % 58.45/58.45 [65]~P29(x653,x651)+P29(x651,x652)+~P29(x653,x652) % 58.45/58.45 [66]~P30(x663,x661)+P30(x661,x662)+~P30(x663,x662) % 58.45/58.45 [67]~P31(x673,x671)+P31(x671,x672)+~P31(x673,x672) % 58.45/58.45 [68]~P32(x683,x681)+P32(x681,x682)+~P32(x683,x682) % 58.45/58.45 [69]~P33(x693,x691)+P33(x691,x692)+~P33(x693,x692) % 58.45/58.45 [72]~P14(x721,x723)+~P31(x722,x724)+P1(f29(x721,x722),f29(x723,x724)) % 58.45/58.45 [73]~P16(x732,x734)+~P33(x731,x733)+P2(f8(x731,x732),f8(x733,x734)) % 58.45/58.45 [74]~P9(x741,x743)+~P31(x742,x744)+P3(f40(x741,x742),f40(x743,x744)) % 58.45/58.45 [75]~P1(x752,x754)+~P2(x751,x753)+P5(f9(x751,x752),f9(x753,x754)) % 58.45/58.45 [76]~P4(x761,x763)+~P16(x762,x764)+P6(f36(x761,x762),f36(x763,x764)) % 58.45/58.45 [77]~P1(x772,x774)+~P6(x771,x773)+P7(f37(x771,x772),f37(x773,x774)) % 58.45/58.45 [78]~P3(x782,x784)+~P7(x781,x783)+P8(f38(x781,x782),f38(x783,x784)) % 58.45/58.45 [79]~P8(x791,x793)+~P29(x792,x794)+P9(f39(x791,x792),f39(x793,x794)) % 58.45/58.45 [80]~P10(x801,x803)+~P16(x802,x804)+P11(f35(x801,x802),f35(x803,x804)) % 58.45/58.45 [81]~P1(x812,x814)+~P11(x811,x813)+P12(f26(x811,x812),f26(x813,x814)) % 58.45/58.45 [82]~P3(x822,x824)+~P12(x821,x823)+P13(f27(x821,x822),f27(x823,x824)) % 58.45/58.45 [83]~P13(x831,x833)+~P29(x832,x834)+P14(f28(x831,x832),f28(x833,x834)) % 58.45/58.45 [84]~P22(x842,x844)+~P28(x841,x843)+P16(f20(x841,x842),f20(x843,x844)) % 58.45/58.45 [85]~P26(x851,x853)+~P31(x852,x854)+P16(f25(x851,x852),f25(x853,x854)) % 58.45/58.45 [86]~P15(x861,x863)+~P29(x862,x864)+P17(f30(x861,x862),f30(x863,x864)) % 58.45/58.45 [87]~P19(x871,x873)+~P29(x872,x874)+P18(f31(x871,x872),f31(x873,x874)) % 58.45/58.45 [88]~P17(x881,x883)+~P31(x882,x884)+P19(f33(x881,x882),f33(x883,x884)) % 58.45/58.45 [89]~P3(x892,x894)+~P5(x891,x893)+P22(f16(x891,x892),f16(x893,x894)) % 58.45/58.45 [90]~P31(x902,x904)+~P32(x901,x903)+P22(f19(x901,x902),f19(x903,x904)) % 58.45/58.45 [91]~P16(x912,x914)+~P21(x911,x913)+P23(f21(x911,x912),f21(x913,x914)) % 58.45/58.45 [92]~P1(x922,x924)+~P23(x921,x923)+P24(f22(x921,x922),f22(x923,x924)) % 58.45/58.45 [93]~P3(x932,x934)+~P24(x931,x933)+P25(f23(x931,x932),f23(x933,x934)) % 58.45/58.45 [94]~P25(x941,x943)+~P29(x942,x944)+P26(f24(x941,x942),f24(x943,x944)) % 58.45/58.45 [95]~P1(x951,x953)+~P20(x952,x954)+P29(f34(x951,x952),f34(x953,x954)) % 58.45/58.45 [96]~P22(x962,x964)+~P27(x961,x963)+P30(f17(x961,x962),f17(x963,x964)) % 58.45/58.45 [97]~P3(x971,x973)+~P20(x972,x974)+P31(f32(x971,x972),f32(x973,x974)) % 58.45/58.45 [98]~P29(x982,x984)+~P30(x981,x983)+P32(f18(x981,x982),f18(x983,x984)) % 58.45/58.45 [70]~P34(x703,x704)+P34(x701,x702)+~P16(x703,x701)+~P20(x704,x702) % 58.45/58.45 [71]~P35(x713,x714)+P35(x711,x712)+~P18(x713,x711)+~P31(x714,x712) % 58.45/58.45 %EqnAxiom % 58.45/58.45 % 58.45/58.45 %------------------------------------------- % 58.45/58.45 cnf(105,plain, % 58.45/58.45 (~P34(a4,a7)), % 58.45/58.45 inference(scs_inference,[],[36,99])). % 58.45/58.45 cnf(123,plain, % 58.45/58.45 (P22(f16(f9(f8(a3,f25(f24(f23(f22(f21(a12,x1231),x1232),x1233),x1234),x1235)),f29(f28(f27(f26(f35(a14,x1231),x1232),x1233),x1234),x1235)),f40(f39(f38(f37(f36(a15,x1231),x1232),x1233),x1234),x1235)),f19(f18(f17(a2,f16(f9(f8(a3,x1231),x1232),x1233)),x1234),x1235))), % 58.45/58.45 inference(scs_inference,[],[35,22,58])). % 58.45/58.45 cnf(127,plain, % 58.45/58.45 (P16(f20(x1271,f16(f9(f8(a3,f25(f24(f23(f22(f21(a12,x1272),x1273),x1274),x1275),x1276)),f29(f28(f27(f26(f35(a14,x1272),x1273),x1274),x1275),x1276)),f40(f39(f38(f37(f36(a15,x1272),x1273),x1274),x1275),x1276))),f20(x1271,f19(f18(f17(a2,f16(f9(f8(a3,x1272),x1273),x1274)),x1275),x1276)))), % 58.45/58.45 inference(scs_inference,[],[28,123,64,84])). % 58.45/58.45 cnf(136,plain, % 58.45/58.45 (~P34(f20(a1,f16(f9(f8(a3,f25(f24(f23(f22(f21(a12,a4),x1361),x1362),x1363),x1364)),x1365),x1366)),a7)), % 58.45/58.45 inference(scs_inference,[],[105,101,100])). % 58.45/58.45 cnf(1123,plain, % 58.45/58.45 (P16(f20(x11231,f19(f18(f17(a2,f16(f9(f8(a3,x11232),x11233),x11234)),x11235),x11236)),f20(x11231,f16(f9(f8(a3,f25(f24(f23(f22(f21(a12,x11232),x11233),x11234),x11235),x11236)),f29(f28(f27(f26(f35(a14,x11232),x11233),x11234),x11235),x11236)),f40(f39(f38(f37(f36(a15,x11232),x11233),x11234),x11235),x11236))))), % 58.45/58.45 inference(scs_inference,[],[127,16,52])). % 58.45/58.45 cnf(1126,plain, % 58.45/58.45 ($false), % 58.45/58.45 inference(scs_inference,[],[1123,136,34,20,70]), % 58.45/58.45 ['proof']). % 58.45/58.45 % SZS output end Proof % 58.45/58.45 % Total time :57.810000s %------------------------------------------------------------------------------