%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN711-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 : n019.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 3.84s 3.94s % Output : CNFRefutation 3.84s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : SYN711-1 : TPTP v8.2.0. Released v2.5.0. % 0.12/0.13 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n019.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sun Jun 23 21:15:09 EDT 2024 % 0.13/0.34 % CPUTime : % 0.49/0.59 start to proof:theBenchmark % 3.84/3.92 %------------------------------------------- % 3.84/3.92 % File :CSE---1.7 % 3.84/3.92 % Problem :theBenchmark % 3.84/3.92 % Transform :cnf % 3.84/3.92 % Format :tptp:raw % 3.84/3.92 % Command :java -jar mcs_scs.jar %d %s % 3.84/3.92 % 3.84/3.92 % Result :Theorem 3.270000s % 3.84/3.92 % Output :CNFRefutation 3.270000s % 3.84/3.92 %------------------------------------------- % 3.84/3.93 %-------------------------------------------------------------------------- % 3.84/3.93 % File : SYN711-1 : TPTP v8.2.0. Released v2.5.0. % 3.84/3.93 % Domain : Syntactic % 3.84/3.93 % Problem : Harrison problem 4711 % 3.84/3.93 % Version : Especial. % 3.84/3.93 % English : % 3.84/3.93 % 3.84/3.93 % Refs : [Har01] Email to G. Sutcliffe % 3.84/3.93 % Source : [Har01] % 3.84/3.93 % Names : % 3.84/3.93 % 3.84/3.93 % Status : Unsatisfiable % 3.84/3.93 % Rating : 0.27 v8.2.0, 0.29 v8.1.0, 0.25 v7.4.0, 0.33 v7.3.0, 0.25 v6.2.0, 0.33 v6.1.0, 0.50 v6.0.0, 0.44 v5.5.0, 0.50 v5.4.0, 0.56 v5.3.0, 0.50 v5.2.0, 0.69 v5.1.0, 0.56 v5.0.0, 0.53 v4.0.1, 0.43 v3.7.0, 0.29 v3.4.0, 0.40 v3.3.0, 0.33 v2.7.0, 0.38 v2.6.0, 0.17 v2.5.0 % 3.84/3.93 % Syntax : Number of clauses : 89 ( 45 unt; 0 nHn; 77 RR) % 3.84/3.93 % Number of literals : 172 ( 0 equ; 87 neg) % 3.84/3.93 % Maximal clause size : 5 ( 1 avg) % 3.84/3.93 % Maximal term depth : 85 ( 11 avg) % 3.84/3.93 % Number of predicates : 19 ( 19 usr; 0 prp; 1-2 aty) % 3.84/3.93 % Number of functors : 43 ( 43 usr; 19 con; 0-4 aty) % 3.84/3.93 % Number of variables : 151 ( 0 sgn) % 3.84/3.93 % SPC : CNF_UNS_RFO_NEQ_HRN % 3.84/3.93 % 3.84/3.93 % Comments : % 3.84/3.93 %-------------------------------------------------------------------------- % 3.84/3.93 cnf(c46_is_p39_1,negated_conjecture, % 3.84/3.93 p39(c46) ). % 3.84/3.93 % 3.84/3.93 cnf(c56_is_p39_2,negated_conjecture, % 3.84/3.93 p39(c56) ). % 3.84/3.93 % 3.84/3.93 cnf(c47_is_p39_3,negated_conjecture, % 3.84/3.93 p39(c47) ). % 3.84/3.93 % 3.84/3.93 cnf(c58_is_not_p45_4,negated_conjecture, % 3.84/3.93 ~ p45(c58) ). % 3.84/3.93 % 3.84/3.93 cnf(c55_is_not_p45_5,negated_conjecture, % 3.84/3.93 ~ p45(c55) ). % 3.84/3.93 % 3.84/3.93 cnf(c57_is_not_p45_6,negated_conjecture, % 3.84/3.93 ~ p45(c57) ). % 3.84/3.93 % 3.84/3.93 cnf(p17_7,negated_conjecture, % 3.84/3.93 p17(X0,X0) ). % 3.84/3.93 % 3.84/3.93 cnf(p9_8,negated_conjecture, % 3.84/3.93 p9(X134,X134) ). % 3.84/3.93 % 3.84/3.93 cnf(p6_9,negated_conjecture, % 3.84/3.93 p6(X99,X99) ). % 3.84/3.93 % 3.84/3.93 cnf(p5_10,negated_conjecture, % 3.84/3.93 p5(X92,X92) ). % 3.84/3.93 % 3.84/3.93 cnf(p33_11,negated_conjecture, % 3.84/3.93 p33(X58,X58) ). % 3.84/3.93 % 3.84/3.93 cnf(p3_12,negated_conjecture, % 3.84/3.93 p3(X53,X53) ). % 3.84/3.93 % 3.84/3.93 cnf(p28_13,negated_conjecture, % 3.84/3.93 p28(X50,X50) ). % 3.84/3.93 % 3.84/3.93 cnf(p26_14,negated_conjecture, % 3.84/3.93 p26(X43,X43) ). % 3.84/3.93 % 3.84/3.93 cnf(p24_15,negated_conjecture, % 3.84/3.93 p24(X36,X36) ). % 3.84/3.93 % 3.84/3.93 cnf(p22_16,negated_conjecture, % 3.84/3.93 p22(X17,X17) ). % 3.84/3.93 % 3.84/3.93 cnf(p2_17,negated_conjecture, % 3.84/3.93 p2(X14,X14) ). % 3.84/3.93 % 3.84/3.93 cnf(p19_18,negated_conjecture, % 3.84/3.93 p19(X7,X7) ). % 3.84/3.93 % 3.84/3.93 cnf(p44_19,negated_conjecture, % 3.84/3.93 p44(c58,f34(c52)) ). % 3.84/3.93 % 3.84/3.93 cnf(p44_20,negated_conjecture, % 3.84/3.93 p44(c55,f34(c52)) ). % 3.84/3.93 % 3.84/3.93 cnf(p44_21,negated_conjecture, % 3.84/3.93 p44(c56,f34(c52)) ). % 3.84/3.93 % 3.84/3.93 cnf(p44_22,negated_conjecture, % 3.84/3.93 p44(c57,f34(c52)) ). % 3.84/3.93 % 3.84/3.93 cnf(p40_23,negated_conjecture, % 3.84/3.93 p40(f7(c46),f4(c48)) ). % 3.84/3.93 % 3.84/3.93 cnf(p40_24,negated_conjecture, % 3.84/3.93 p40(f7(c47),f4(c48)) ). % 3.84/3.93 % 3.84/3.93 cnf(p42_25,negated_conjecture, % 3.84/3.93 p42(f16(c62),f16(f7(c46))) ). % 3.84/3.93 % 3.84/3.93 cnf(p42_26,negated_conjecture, % 3.84/3.93 ( p42(X73,X74) % 3.84/3.93 | ~ p41(X73,X74) ) ). % 3.84/3.93 % 3.84/3.93 cnf(p39_27,negated_conjecture, % 3.84/3.93 ( p39(X63) % 3.84/3.93 | ~ p39(X64) % 3.84/3.93 | ~ p5(X64,X63) ) ). % 3.84/3.93 % 3.84/3.93 cnf(p45_28,negated_conjecture, % 3.84/3.93 ( p45(X90) % 3.84/3.93 | ~ p45(X91) % 3.84/3.93 | ~ p5(X91,X90) ) ). % 3.84/3.93 % 3.84/3.93 cnf(p41_29,negated_conjecture, % 3.84/3.93 p41(f8(f10(f11(f12(c49)))),f7(c46)) ). % 3.84/3.93 % 3.84/3.93 cnf(p9_30,negated_conjecture, % 3.84/3.93 ( p9(f15(X141),f15(X142)) % 3.84/3.93 | ~ p9(X141,X142) ) ). % 3.84/3.93 % 3.84/3.93 cnf(p3_31,negated_conjecture, % 3.84/3.93 ( p3(f4(X56),f4(X57)) % 3.84/3.93 | ~ p2(X56,X57) ) ). % 3.84/3.93 % 3.84/3.93 cnf(p33_32,negated_conjecture, % 3.84/3.93 ( p33(f34(X61),f34(X62)) % 3.84/3.93 | ~ p2(X61,X62) ) ). % 3.84/3.93 % 3.84/3.93 cnf(p5_33,negated_conjecture, % 3.84/3.93 ( p5(f18(X95),f18(X96)) % 3.84/3.93 | ~ p17(X95,X96) ) ). % 3.84/3.93 % 3.84/3.93 cnf(p5_34,negated_conjecture, % 3.84/3.93 ( p5(f23(X97),f23(X98)) % 3.84/3.93 | ~ p22(X97,X98) ) ). % 3.84/3.93 % 3.84/3.93 cnf(p6_35,negated_conjecture, % 3.84/3.93 ( p6(f10(X102),f10(X103)) % 3.84/3.93 | ~ p9(X102,X103) ) ). % 3.84/3.93 % 3.84/3.93 cnf(p6_36,negated_conjecture, % 3.84/3.93 ( p6(f13(X104),f13(X105)) % 3.84/3.93 | ~ p6(X104,X105) ) ). % 3.84/3.93 % 3.84/3.93 cnf(p6_37,negated_conjecture, % 3.84/3.93 ( p6(f16(X110),f16(X111)) % 3.84/3.93 | ~ p6(X110,X111) ) ). % 3.84/3.93 % 3.84/3.93 cnf(p6_38,negated_conjecture, % 3.84/3.93 ( p6(f38(X128),f38(X129)) % 3.84/3.93 | ~ p6(X128,X129) ) ). % 3.84/3.93 % 3.84/3.93 cnf(p6_39,negated_conjecture, % 3.84/3.93 ( p6(f7(X130),f7(X131)) % 3.84/3.93 | ~ p5(X130,X131) ) ). % 3.84/3.93 % 3.84/3.93 cnf(p6_40,negated_conjecture, % 3.84/3.93 ( p6(f8(X132),f8(X133)) % 3.84/3.93 | ~ p6(X132,X133) ) ). % 3.84/3.93 % 3.84/3.93 cnf(p9_41,negated_conjecture, % 3.84/3.93 ( p9(f11(X137),f11(X138)) % 3.84/3.93 | ~ p9(X137,X138) ) ). % 3.84/3.93 % 3.84/3.93 cnf(p9_42,negated_conjecture, % 3.84/3.93 ( p9(f12(X139),f12(X140)) % 3.84/3.93 | ~ p9(X139,X140) ) ). % 3.84/3.93 % 3.84/3.93 cnf(p17_43,negated_conjecture, % 3.84/3.93 ( p17(X1,X2) % 3.84/3.93 | ~ p17(X0,X1) % 3.84/3.93 | ~ p17(X0,X2) ) ). % 3.84/3.93 % 3.84/3.93 cnf(p9_44,negated_conjecture, % 3.84/3.93 ( p9(X135,X136) % 3.84/3.93 | ~ p9(X134,X135) % 3.84/3.93 | ~ p9(X134,X136) ) ). % 3.84/3.93 % 3.84/3.93 cnf(p6_45,negated_conjecture, % 3.84/3.93 ( p6(X100,X101) % 3.84/3.93 | ~ p6(X99,X100) % 3.84/3.94 | ~ p6(X99,X101) ) ). % 3.84/3.94 % 3.84/3.94 cnf(p5_46,negated_conjecture, % 3.84/3.94 ( p5(X93,X94) % 3.84/3.94 | ~ p5(X92,X93) % 3.84/3.94 | ~ p5(X92,X94) ) ). % 3.84/3.94 % 3.84/3.94 cnf(p42_47,negated_conjecture, % 3.84/3.94 ( p42(X75,X76) % 3.84/3.94 | ~ p42(X75,X77) % 3.84/3.94 | ~ p42(X77,X76) ) ). % 3.84/3.94 % 3.84/3.94 cnf(p33_48,negated_conjecture, % 3.84/3.94 ( p33(X59,X60) % 3.84/3.94 | ~ p33(X58,X59) % 3.84/3.94 | ~ p33(X58,X60) ) ). % 3.84/3.94 % 3.84/3.94 cnf(p3_49,negated_conjecture, % 3.84/3.94 ( p3(X54,X55) % 3.84/3.94 | ~ p3(X53,X54) % 3.84/3.94 | ~ p3(X53,X55) ) ). % 3.84/3.94 % 3.84/3.94 cnf(p28_50,negated_conjecture, % 3.84/3.94 ( p28(X51,X52) % 3.84/3.94 | ~ p28(X50,X51) % 3.84/3.94 | ~ p28(X50,X52) ) ). % 3.84/3.94 % 3.84/3.94 cnf(p26_51,negated_conjecture, % 3.84/3.94 ( p26(X44,X45) % 3.84/3.94 | ~ p26(X43,X44) % 3.84/3.94 | ~ p26(X43,X45) ) ). % 3.84/3.94 % 3.84/3.94 cnf(p24_52,negated_conjecture, % 3.84/3.94 ( p24(X37,X38) % 3.84/3.94 | ~ p24(X36,X37) % 3.84/3.94 | ~ p24(X36,X38) ) ). % 3.84/3.94 % 3.84/3.94 cnf(p22_53,negated_conjecture, % 3.84/3.94 ( p22(X18,X19) % 3.84/3.94 | ~ p22(X17,X18) % 3.84/3.94 | ~ p22(X17,X19) ) ). % 3.84/3.94 % 3.84/3.94 cnf(p2_54,negated_conjecture, % 3.84/3.94 ( p2(X15,X16) % 3.84/3.94 | ~ p2(X14,X15) % 3.84/3.94 | ~ p2(X14,X16) ) ). % 3.84/3.94 % 3.84/3.94 cnf(p19_55,negated_conjecture, % 3.84/3.94 ( p19(X8,X9) % 3.84/3.94 | ~ p19(X7,X8) % 3.84/3.94 | ~ p19(X7,X9) ) ). % 3.84/3.94 % 3.84/3.94 cnf(p6_56,negated_conjecture, % 3.84/3.94 p6(f7(c56),f37(f35(f7(c50),f7(c46)),f7(c55))) ). % 3.84/3.94 % 3.84/3.94 cnf(p5_57,negated_conjecture, % 3.84/3.94 p5(f23(f31(f27(c52,f30(c53,c1)),c50,c46,c55)),c56) ). % 3.84/3.94 % 3.84/3.94 cnf(p5_58,negated_conjecture, % 3.84/3.94 p5(f23(f25(f27(c52,f30(c53,c1)),c47,c57,c54)),c58) ). % 3.84/3.94 % 3.84/3.94 cnf(p5_59,negated_conjecture, % 3.84/3.94 p5(f23(f25(f27(c52,f30(c53,c1)),c50,c46,c54)),c55) ). % 3.84/3.94 % 3.84/3.94 cnf(p5_60,negated_conjecture, % 3.84/3.94 p5(f23(f25(f27(c52,f30(c53,c1)),c51,c46,c56)),c57) ). % 3.84/3.94 % 3.84/3.94 cnf(p40_61,negated_conjecture, % 3.84/3.94 ( p40(X65,X66) % 3.84/3.94 | ~ p40(X68,X67) % 3.84/3.94 | ~ p6(X68,X65) % 3.84/3.94 | ~ p3(X67,X66) ) ). % 3.84/3.94 % 3.84/3.94 cnf(p44_62,negated_conjecture, % 3.84/3.94 ( p44(X86,X87) % 3.84/3.94 | ~ p44(X89,X88) % 3.84/3.94 | ~ p5(X89,X86) % 3.84/3.94 | ~ p33(X88,X87) ) ). % 3.84/3.94 % 3.84/3.94 cnf(p43_63,negated_conjecture, % 3.84/3.94 ( p43(X82,X83) % 3.84/3.94 | ~ p6(X84,X82) % 3.84/3.94 | ~ p6(X85,X83) % 3.84/3.94 | ~ p43(X84,X85) ) ). % 3.84/3.94 % 3.84/3.94 cnf(p42_64,negated_conjecture, % 3.84/3.94 ( p42(X78,X79) % 3.84/3.94 | ~ p6(X80,X78) % 3.84/3.94 | ~ p6(X81,X79) % 3.84/3.94 | ~ p42(X80,X81) ) ). % 3.84/3.94 % 3.84/3.94 cnf(p41_65,negated_conjecture, % 3.84/3.94 ( p41(X69,X70) % 3.84/3.94 | ~ p6(X71,X69) % 3.84/3.94 | ~ p6(X72,X70) % 3.84/3.94 | ~ p41(X71,X72) ) ). % 3.84/3.94 % 3.84/3.94 cnf(p17_66,negated_conjecture, % 3.84/3.94 ( p17(f20(X3,X4),f20(X5,X6)) % 3.84/3.94 | ~ p19(X4,X6) % 3.84/3.94 | ~ p9(X3,X5) ) ). % 3.84/3.94 % 3.84/3.94 cnf(p6_67,negated_conjecture, % 3.84/3.94 ( p6(f37(X124,X125),f37(X126,X127)) % 3.84/3.94 | ~ p6(X124,X126) % 3.84/3.94 | ~ p6(X125,X127) ) ). % 3.84/3.94 % 3.84/3.94 cnf(p6_68,negated_conjecture, % 3.84/3.94 ( p6(f36(X120,X121),f36(X122,X123)) % 3.84/3.94 | ~ p6(X120,X122) % 3.84/3.94 | ~ p6(X121,X123) ) ). % 3.84/3.94 % 3.84/3.94 cnf(p6_69,negated_conjecture, % 3.84/3.94 ( p6(f35(X116,X117),f35(X118,X119)) % 3.84/3.94 | ~ p6(X116,X118) % 3.84/3.94 | ~ p6(X117,X119) ) ). % 3.84/3.94 % 3.84/3.94 cnf(p6_70,negated_conjecture, % 3.84/3.94 ( p6(f32(X112,X113),f32(X114,X115)) % 3.84/3.94 | ~ p6(X112,X114) % 3.84/3.94 | ~ p6(X113,X115) ) ). % 3.84/3.94 % 3.84/3.94 cnf(p6_71,negated_conjecture, % 3.84/3.94 ( p6(f14(X106,X107),f14(X108,X109)) % 3.84/3.94 | ~ p6(X106,X108) % 3.84/3.94 | ~ p9(X107,X109) ) ). % 3.84/3.94 % 3.84/3.94 cnf(p24_72,negated_conjecture, % 3.84/3.94 ( p24(f27(X39,X40),f27(X41,X42)) % 3.84/3.94 | ~ p2(X39,X41) % 3.84/3.94 | ~ p26(X40,X42) ) ). % 3.84/3.94 % 3.84/3.94 cnf(p19_73,negated_conjecture, % 3.84/3.94 ( p19(f21(X10,X11),f21(X12,X13)) % 3.84/3.94 | ~ p9(X10,X12) % 3.84/3.94 | ~ p9(X11,X13) ) ). % 3.84/3.94 % 3.84/3.94 cnf(p6_74,negated_conjecture, % 3.84/3.94 p6(f7(c55),f35(f7(c50),f35(f7(c46),f36(f10(f11(f12(c49))),c59)))) ). % 3.84/3.94 % 3.84/3.94 cnf(p42_75,negated_conjecture, % 3.84/3.94 p42(f16(c59),f13(f14(f10(f11(f15(f12(c49)))),f11(f15(f15(f15(f15(f15(f15(f12(c49))))))))))) ). % 3.84/3.94 % 3.84/3.94 cnf(p42_76,negated_conjecture, % 3.84/3.94 p42(f16(c61),f13(f14(f10(f11(f15(f12(c49)))),f11(f15(f15(f15(f15(f15(f15(f12(c49))))))))))) ). % 3.84/3.94 % 3.84/3.94 cnf(p42_77,negated_conjecture, % 3.84/3.94 p42(f16(c60),f13(f14(f10(f11(f15(f12(c49)))),f11(f15(f15(f15(f15(f15(f15(f12(c49))))))))))) ). % 3.84/3.94 % 3.84/3.94 cnf(not_p42_78,negated_conjecture, % 3.84/3.94 ~ p42(f16(c62),f13(f14(f10(f11(f15(f12(c49)))),f11(f15(f15(f15(f15(f12(f15(f12(c49))))))))))) ). % 3.84/3.94 % 3.84/3.94 cnf(p6_79,negated_conjecture, % 3.84/3.94 p6(f7(c57),f35(f37(f7(c51),f35(f7(c50),c59)),f35(f7(c46),f36(f10(f11(f12(c49))),c60)))) ). % 3.84/3.94 % 3.84/3.94 cnf(p41_80,negated_conjecture, % 3.84/3.94 p41(f16(f7(c46)),f13(f14(f10(f11(f15(f12(c49)))),f11(f15(f15(f15(f15(f12(f15(f12(c49))))))))))) ). % 3.84/3.94 % 3.84/3.94 cnf(p22_81,negated_conjecture, % 3.84/3.94 ( p22(f25(X20,X21,X22,X23),f25(X24,X25,X26,X27)) % 3.84/3.94 | ~ p5(X22,X26) % 3.84/3.94 | ~ p5(X23,X27) % 3.84/3.94 | ~ p24(X20,X24) % 3.84/3.94 | ~ p5(X21,X25) ) ). % 3.84/3.94 % 3.84/3.94 cnf(p22_82,negated_conjecture, % 3.84/3.94 ( p22(f31(X28,X29,X30,X31),f31(X32,X33,X34,X35)) % 3.84/3.94 | ~ p5(X30,X34) % 3.84/3.94 | ~ p5(X31,X35) % 3.84/3.94 | ~ p24(X28,X32) % 3.84/3.94 | ~ p5(X29,X33) ) ). % 3.84/3.94 % 3.84/3.94 cnf(p43_83,negated_conjecture, % 3.84/3.94 p43(f13(f14(f10(f11(f15(f12(c49)))),f11(f12(f15(f12(f12(f12(f12(f15(f15(f15(f15(f15(f15(f15(f15(f12(c49)))))))))))))))))),f7(c46)) ). % 3.84/3.94 % 3.84/3.94 cnf(p43_84,negated_conjecture, % 3.84/3.94 p43(f13(f14(f10(f11(f15(f12(c49)))),f11(f12(f15(f12(f12(f12(f12(f15(f15(f15(f15(f15(f15(f15(f15(f12(c49)))))))))))))))))),f7(c47)) ). % 3.84/3.94 % 3.84/3.94 cnf(p6_85,negated_conjecture, % 3.84/3.94 p6(f7(c58),f35(f7(c47),f35(f37(f7(c51),f35(f7(c50),c59)),f35(f7(c46),f35(f36(f10(f11(f12(c49))),c60),f36(f10(f11(f12(c49))),c61)))))) ). % 3.84/3.94 % 3.84/3.94 cnf(p6_86,negated_conjecture, % 3.84/3.94 p6(f35(f7(c46),f13(f35(f10(f11(f15(f12(c49)))),f35(f36(f10(f11(f12(c49))),c62),f35(f36(f10(f11(f12(c49))),c62),f38(f10(f11(f15(f12(c49)))))))))),c63) ). % 3.84/3.94 % 3.84/3.94 cnf(p5_87,negated_conjecture, % 3.84/3.94 p5(f18(f20(f11(c49),f21(f11(f12(f12(f12(f12(f12(f12(f12(f12(f12(f12(f12(f12(f12(f12(f12(f12(c49))))))))))))))))),f11(f12(f12(f15(f12(f12(f12(f15(f12(f15(f15(f15(f15(f12(f12(f12(f12(f12(f12(f12(f15(f12(f15(f15(f15(f15(f15(f12(f12(f12(f15(f12(f15(f12(f15(f15(f12(f15(f12(f15(f15(f12(f12(f15(f12(f12(f12(f15(f15(f15(f12(f15(f12(f15(f12(f15(f12(f15(f15(f15(f12(f12(f12(f15(f12(c49)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),c50) ). % 3.84/3.94 % 3.84/3.94 cnf(p5_88,negated_conjecture, % 3.84/3.94 p5(f18(f20(f11(c49),f21(f11(f12(f12(f12(f12(f12(f12(f15(f12(f12(f12(f12(f12(f12(f12(f12(f12(c49))))))))))))))))),f11(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f12(f12(f12(f12(f15(f12(f15(f15(f15(f12(f15(f15(f12(f15(f12(f12(f15(f15(f15(f15(f15(f12(f15(f12(f12(f15(f12(f12(f12(f12(f12(f12(f12(f12(f12(f12(f15(f15(f15(f15(f12(f15(f12(f12(f12(f12(f12(f15(f12(c49)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),c51) ). % 3.84/3.94 % 3.84/3.94 cnf(p42_89,negated_conjecture, % 3.84/3.94 p42(f16(f7(c46)),f32(f10(f11(f12(c49))),f10(f11(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f15(f12(c49))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ). % 3.84/3.94 % 3.84/3.94 %-------------------------------------------------------------------------- % 3.84/3.94 %------------------------------------------- % 3.84/3.94 % Proof found % 3.84/3.94 % SZS status Theorem for theBenchmark % 3.84/3.94 % SZS output start Proof % 3.84/3.94 %ClaNum:89(EqnAxiom:0) % 3.84/3.94 %VarNum:302(SingletonVarNum:151) % 3.84/3.94 %MaxLitNum:5 % 3.84/3.94 %MaxfuncDepth:84 % 3.84/3.94 %SharedTerms:358 % 3.84/3.94 %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 % 3.84/3.94 %singleGoalClaCount:45 % 3.84/3.94 [1]P1(a1) % 3.84/3.94 [2]P1(a3) % 3.84/3.94 [3]P1(a4) % 3.84/3.94 [42]~P19(a14) % 3.84/3.94 [43]~P19(a10) % 3.84/3.94 [44]~P19(a15) % 3.84/3.94 [16]P14(a3,f13(a5)) % 3.84/3.94 [17]P14(a14,f13(a5)) % 3.84/3.94 [18]P14(a10,f13(a5)) % 3.84/3.94 [19]P14(a15,f13(a5)) % 3.84/3.94 [20]P15(f37(a1),f38(a6)) % 3.84/3.94 [21]P15(f37(a4),f38(a6)) % 3.84/3.94 [22]P16(f20(a16),f20(f37(a1))) % 3.84/3.94 [24]P12(f37(a3),f40(f39(f37(a8),f37(a1)),f37(a10))) % 3.84/3.94 [23]P17(f43(f23(f22(f21(a7)))),f37(a1)) % 3.84/3.94 [27]P13(f30(f35(f29(a5,f28(a11,a2)),a8,a1,a10)),a3) % 3.84/3.94 [28]P13(f30(f34(f29(a5,f28(a11,a2)),a4,a15,a12)),a14) % 3.84/3.94 [29]P13(f30(f34(f29(a5,f28(a11,a2)),a8,a1,a12)),a10) % 3.84/3.94 [30]P13(f30(f34(f29(a5,f28(a11,a2)),a9,a1,a3)),a15) % 3.84/3.94 [25]P12(f37(a10),f39(f37(a8),f39(f37(a1),f41(f23(f22(f21(a7))),a17)))) % 3.84/3.94 [26]P12(f37(a15),f39(f40(f37(a9),f39(f37(a8),a17)),f39(f37(a1),f41(f23(f22(f21(a7))),a18)))) % 3.84/3.94 [31]P12(f37(a14),f39(f37(a4),f39(f40(f37(a9),f39(f37(a8),a17)),f39(f37(a1),f39(f41(f23(f22(f21(a7))),a18),f41(f23(f22(f21(a7))),a19)))))) % 3.84/3.94 [32]P16(f20(a17),f27(f26(f23(f22(f25(f21(a7)))),f22(f25(f25(f25(f25(f25(f25(f21(a7))))))))))) % 3.84/3.94 [33]P16(f20(a19),f27(f26(f23(f22(f25(f21(a7)))),f22(f25(f25(f25(f25(f25(f25(f21(a7))))))))))) % 3.84/3.94 [34]P16(f20(a18),f27(f26(f23(f22(f25(f21(a7)))),f22(f25(f25(f25(f25(f25(f25(f21(a7))))))))))) % 3.84/3.94 [35]P17(f20(f37(a1)),f27(f26(f23(f22(f25(f21(a7)))),f22(f25(f25(f25(f25(f21(f25(f21(a7))))))))))) % 3.84/3.94 [36]P12(f39(f37(a1),f27(f39(f23(f22(f25(f21(a7)))),f39(f41(f23(f22(f21(a7))),a16),f39(f41(f23(f22(f21(a7))),a16),f42(f23(f22(f25(f21(a7)))))))))),a24) % 3.84/3.94 [45]~P16(f20(a16),f27(f26(f23(f22(f25(f21(a7)))),f22(f25(f25(f25(f25(f21(f25(f21(a7))))))))))) % 3.84/3.94 [37]P18(f27(f26(f23(f22(f25(f21(a7)))),f22(f21(f25(f21(f21(f21(f21(f25(f25(f25(f25(f25(f25(f25(f25(f21(a7)))))))))))))))))),f37(a1)) % 3.84/3.94 [38]P18(f27(f26(f23(f22(f25(f21(a7)))),f22(f21(f25(f21(f21(f21(f21(f25(f25(f25(f25(f25(f25(f25(f25(f21(a7)))))))))))))))))),f37(a4)) % 3.84/3.94 [39]P13(f33(f32(f22(a7),f31(f22(f21(f21(f21(f21(f21(f21(f21(f21(f21(f21(f21(f21(f21(f21(f21(f21(a7))))))))))))))))),f22(f21(f21(f25(f21(f21(f21(f25(f21(f25(f25(f25(f25(f21(f21(f21(f21(f21(f21(f21(f25(f21(f25(f25(f25(f25(f25(f21(f21(f21(f25(f21(f25(f21(f25(f25(f21(f25(f21(f25(f25(f21(f21(f25(f21(f21(f21(f25(f25(f25(f21(f25(f21(f25(f21(f25(f21(f25(f25(f25(f21(f21(f21(f25(f21(a7)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),a8) % 3.84/3.94 [40]P13(f33(f32(f22(a7),f31(f22(f21(f21(f21(f21(f21(f21(f25(f21(f21(f21(f21(f21(f21(f21(f21(f21(a7))))))))))))))))),f22(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f21(f21(f21(f21(f25(f21(f25(f25(f25(f21(f25(f25(f21(f25(f21(f21(f25(f25(f25(f25(f25(f21(f25(f21(f21(f25(f21(f21(f21(f21(f21(f21(f21(f21(f21(f21(f25(f25(f25(f25(f21(f25(f21(f21(f21(f21(f21(f25(f21(a7)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),a9) % 3.84/3.94 [41]P16(f20(f37(a1)),f36(f23(f22(f21(a7))),f23(f22(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f25(f21(a7))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) % 3.84/3.94 [4]P2(x41,x41) % 3.84/3.94 [5]P11(x51,x51) % 3.84/3.94 [6]P12(x61,x61) % 3.84/3.94 [7]P13(x71,x71) % 3.84/3.94 [8]P3(x81,x81) % 3.84/3.94 [9]P4(x91,x91) % 3.84/3.94 [10]P5(x101,x101) % 3.84/3.94 [11]P6(x111,x111) % 3.84/3.94 [12]P7(x121,x121) % 3.84/3.94 [13]P8(x131,x131) % 3.84/3.94 [14]P9(x141,x141) % 3.84/3.94 [15]P10(x151,x151) % 3.84/3.94 [48]~P17(x481,x482)+P16(x481,x482) % 3.84/3.94 [49]~P11(x491,x492)+P11(f21(x491),f21(x492)) % 3.84/3.94 [50]~P11(x501,x502)+P11(f22(x501),f22(x502)) % 3.84/3.94 [51]~P11(x511,x512)+P11(f25(x511),f25(x512)) % 3.84/3.94 [52]~P13(x521,x522)+P12(f37(x521),f37(x522)) % 3.84/3.94 [53]~P12(x531,x532)+P12(f20(x531),f20(x532)) % 3.84/3.94 [54]~P11(x541,x542)+P12(f23(x541),f23(x542)) % 3.84/3.94 [55]~P12(x551,x552)+P12(f43(x551),f43(x552)) % 3.84/3.94 [56]~P12(x561,x562)+P12(f27(x561),f27(x562)) % 3.84/3.94 [57]~P12(x571,x572)+P12(f42(x571),f42(x572)) % 3.84/3.94 [58]~P2(x581,x582)+P13(f33(x581),f33(x582)) % 3.84/3.94 [59]~P8(x591,x592)+P13(f30(x591),f30(x592)) % 3.84/3.94 [60]~P9(x601,x602)+P3(f13(x601),f13(x602)) % 3.84/3.94 [61]~P9(x611,x612)+P4(f38(x611),f38(x612)) % 3.84/3.94 [46]~P13(x462,x461)+P1(x461)+~P1(x462) % 3.84/3.94 [47]~P13(x472,x471)+P19(x471)+~P19(x472) % 3.84/3.94 [62]~P2(x623,x621)+P2(x621,x622)+~P2(x623,x622) % 3.84/3.94 [63]~P11(x633,x631)+P11(x631,x632)+~P11(x633,x632) % 3.84/3.94 [64]~P12(x643,x641)+P12(x641,x642)+~P12(x643,x642) % 3.84/3.94 [65]~P13(x653,x651)+P13(x651,x652)+~P13(x653,x652) % 3.84/3.94 [66]~P3(x663,x661)+P3(x661,x662)+~P3(x663,x662) % 3.84/3.94 [67]~P4(x673,x671)+P4(x671,x672)+~P4(x673,x672) % 3.84/3.94 [68]~P5(x683,x681)+P5(x681,x682)+~P5(x683,x682) % 3.84/3.94 [69]~P6(x693,x691)+P6(x691,x692)+~P6(x693,x692) % 3.84/3.94 [70]~P7(x703,x701)+P7(x701,x702)+~P7(x703,x702) % 3.84/3.94 [71]~P8(x713,x711)+P8(x711,x712)+~P8(x713,x712) % 3.84/3.94 [72]~P9(x723,x721)+P9(x721,x722)+~P9(x723,x722) % 3.84/3.94 [73]~P10(x733,x731)+P10(x731,x732)+~P10(x733,x732) % 3.84/3.94 [74]~P16(x741,x743)+P16(x741,x742)+~P16(x743,x742) % 3.84/3.94 [80]~P11(x801,x803)+~P10(x802,x804)+P2(f32(x801,x802),f32(x803,x804)) % 3.84/3.94 [81]~P12(x812,x814)+~P12(x811,x813)+P12(f39(x811,x812),f39(x813,x814)) % 3.84/3.94 [82]~P12(x822,x824)+~P12(x821,x823)+P12(f40(x821,x822),f40(x823,x824)) % 3.84/3.94 [83]~P12(x832,x834)+~P12(x831,x833)+P12(f41(x831,x832),f41(x833,x834)) % 3.84/3.94 [84]~P12(x842,x844)+~P12(x841,x843)+P12(f36(x841,x842),f36(x843,x844)) % 3.84/3.94 [85]~P11(x852,x854)+~P12(x851,x853)+P12(f26(x851,x852),f26(x853,x854)) % 3.84/3.94 [86]~P6(x862,x864)+~P9(x861,x863)+P7(f29(x861,x862),f29(x863,x864)) % 3.84/3.94 [87]~P11(x872,x874)+~P11(x871,x873)+P10(f31(x871,x872),f31(x873,x874)) % 3.84/3.94 [75]~P14(x753,x754)+P14(x751,x752)+~P13(x753,x751)+~P3(x754,x752) % 3.84/3.94 [76]~P15(x763,x764)+P15(x761,x762)+~P12(x763,x761)+~P4(x764,x762) % 3.84/3.94 [77]~P16(x774,x773)+P16(x771,x772)+~P12(x773,x772)+~P12(x774,x771) % 3.84/3.94 [78]~P17(x784,x783)+P17(x781,x782)+~P12(x783,x782)+~P12(x784,x781) % 3.84/3.94 [79]~P18(x794,x793)+P18(x791,x792)+~P12(x793,x792)+~P12(x794,x791) % 3.84/3.94 [88]~P13(x884,x888)+~P13(x883,x887)+~P13(x882,x886)+~P7(x881,x885)+P8(f35(x881,x882,x883,x884),f35(x885,x886,x887,x888)) % 3.84/3.95 [89]~P13(x894,x898)+~P13(x893,x897)+~P13(x892,x896)+~P7(x891,x895)+P8(f34(x891,x892,x893,x894),f34(x895,x896,x897,x898)) % 3.84/3.95 %EqnAxiom % 3.84/3.95 % 3.84/3.95 %------------------------------------------- % 3.84/3.95 cnf(645,plain, % 3.84/3.95 (~P12(x6451,f20(a16))+~P16(x6451,f27(f26(f23(f22(f25(f21(a7)))),f22(f25(f25(f25(f25(f21(f25(f21(a7)))))))))))), % 3.84/3.95 inference(scs_inference,[],[6,45,77])). % 3.84/3.95 cnf(655,plain, % 3.84/3.95 (~P16(f20(f37(a1)),f27(f26(f23(f22(f25(f21(a7)))),f22(f25(f25(f25(f25(f21(f25(f21(a7)))))))))))), % 3.84/3.95 inference(scs_inference,[],[6,22,645,74])). % 3.84/3.95 cnf(656,plain, % 3.84/3.95 ($false), % 3.84/3.95 inference(scs_inference,[],[655,35,48]), % 3.84/3.95 ['proof']). % 3.84/3.95 % SZS output end Proof % 3.84/3.95 % Total time :3.270000s %------------------------------------------------------------------------------