%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN704-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 : n028.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:21 EDT 2024 % Result : Unsatisfiable 58.42s 58.49s % Output : CNFRefutation 58.47s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN704-1 : TPTP v8.2.0. Released v2.5.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.31 % Computer : n028.cluster.edu % 0.12/0.31 % Model : x86_64 x86_64 % 0.12/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.31 % Memory : 8042.1875MB % 0.12/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.31 % CPULimit : 300 % 0.12/0.31 % WCLimit : 300 % 0.12/0.31 % DateTime : Sun Jun 23 19:14:23 EDT 2024 % 0.17/0.32 % CPUTime : % 0.17/0.55 start to proof:theBenchmark % 58.33/58.45 %------------------------------------------- % 58.33/58.45 % File :CSE---1.7 % 58.33/58.45 % Problem :theBenchmark % 58.33/58.45 % Transform :cnf % 58.33/58.45 % Format :tptp:raw % 58.33/58.45 % Command :java -jar mcs_scs.jar %d %s % 58.33/58.45 % 58.33/58.45 % Result :Theorem 57.840000s % 58.33/58.45 % Output :CNFRefutation 57.840000s % 58.33/58.45 %------------------------------------------- % 58.42/58.48 %-------------------------------------------------------------------------- % 58.42/58.48 % File : SYN704-1 : TPTP v8.2.0. Released v2.5.0. % 58.42/58.48 % Domain : Syntactic % 58.42/58.48 % Problem : Harrison problem 4674 % 58.42/58.48 % Version : Especial. % 58.42/58.48 % English : % 58.42/58.48 % 58.42/58.48 % Refs : [Har01] Email to G. Sutcliffe % 58.42/58.48 % Source : [Har01] % 58.42/58.48 % Names : % 58.42/58.48 % 58.42/58.48 % Status : Unsatisfiable % 58.42/58.48 % Rating : 0.18 v8.2.0, 0.29 v8.1.0, 0.25 v7.4.0, 0.17 v7.3.0, 0.25 v6.2.0, 0.33 v6.1.0, 0.43 v6.0.0, 0.22 v5.5.0, 0.38 v5.4.0, 0.33 v5.3.0, 0.40 v5.2.0, 0.46 v5.1.0, 0.38 v5.0.0, 0.33 v4.0.1, 0.43 v3.4.0, 0.40 v3.3.0, 0.33 v3.1.0, 0.17 v2.7.0, 0.25 v2.6.0, 0.17 v2.5.0 % 58.42/58.48 % Syntax : Number of clauses : 80 ( 29 unt; 0 nHn; 53 RR) % 58.42/58.48 % Number of literals : 178 ( 0 equ; 99 neg) % 58.42/58.48 % Maximal clause size : 4 ( 2 avg) % 58.42/58.48 % Maximal term depth : 8 ( 1 avg) % 58.42/58.48 % Number of predicates : 26 ( 26 usr; 0 prp; 2-2 aty) % 58.42/58.48 % Number of functors : 31 ( 31 usr; 11 con; 0-2 aty) % 58.42/58.48 % Number of variables : 215 ( 10 sgn) % 58.42/58.48 % SPC : CNF_UNS_RFO_NEQ_HRN % 58.42/58.48 % 58.42/58.48 % Comments : % 58.42/58.48 %-------------------------------------------------------------------------- % 58.42/58.48 cnf(p11_1,negated_conjecture, % 58.42/58.48 p11(X0,X0) ). % 58.42/58.48 % 58.42/58.48 cnf(p9_2,negated_conjecture, % 58.42/58.48 p9(X167,X167) ). % 58.42/58.48 % 58.42/58.48 cnf(p7_3,negated_conjecture, % 58.42/58.48 p7(X162,X162) ). % 58.42/58.48 % 58.42/58.48 cnf(p6_4,negated_conjecture, % 58.42/58.48 p6(X155,X155) ). % 58.42/58.48 % 58.42/58.48 cnf(p45_5,negated_conjecture, % 58.42/58.48 p45(X144,X144) ). % 58.42/58.48 % 58.42/58.48 cnf(p43_6,negated_conjecture, % 58.42/58.48 p43(X137,X137) ). % 58.42/58.48 % 58.42/58.48 cnf(p41_7,negated_conjecture, % 58.42/58.48 p41(X130,X130) ). % 58.42/58.48 % 58.42/58.48 cnf(p4_8,negated_conjecture, % 58.42/58.48 p4(X119,X119) ). % 58.42/58.48 % 58.42/58.48 cnf(p39_9,negated_conjecture, % 58.42/58.48 p39(X112,X112) ). % 58.42/58.48 % 58.42/58.48 cnf(p37_10,negated_conjecture, % 58.42/58.48 p37(X105,X105) ). % 58.42/58.48 % 58.42/58.48 cnf(p35_11,negated_conjecture, % 58.42/58.48 p35(X102,X102) ). % 58.42/58.48 % 58.42/58.48 cnf(p33_12,negated_conjecture, % 58.42/58.48 p33(X95,X95) ). % 58.42/58.48 % 58.42/58.48 cnf(p31_13,negated_conjecture, % 58.42/58.48 p31(X88,X88) ). % 58.42/58.48 % 58.42/58.48 cnf(p3_14,negated_conjecture, % 58.42/58.48 p3(X77,X77) ). % 58.42/58.48 % 58.42/58.48 cnf(p29_15,negated_conjecture, % 58.42/58.48 p29(X70,X70) ). % 58.42/58.48 % 58.42/58.48 cnf(p27_16,negated_conjecture, % 58.42/58.48 p27(X58,X58) ). % 58.42/58.48 % 58.42/58.48 cnf(p25_17,negated_conjecture, % 58.42/58.48 p25(X55,X55) ). % 58.42/58.48 % 58.42/58.48 cnf(p23_18,negated_conjecture, % 58.42/58.48 p23(X48,X48) ). % 58.42/58.48 % 58.42/58.48 cnf(p21_19,negated_conjecture, % 58.42/58.48 p21(X41,X41) ). % 58.42/58.48 % 58.42/58.48 cnf(p2_20,negated_conjecture, % 58.42/58.48 p2(X38,X38) ). % 58.42/58.48 % 58.42/58.48 cnf(p19_21,negated_conjecture, % 58.42/58.48 p19(X31,X31) ). % 58.42/58.48 % 58.42/58.48 cnf(p17_22,negated_conjecture, % 58.42/58.48 p17(X28,X28) ). % 58.42/58.48 % 58.42/58.48 cnf(p15_23,negated_conjecture, % 58.42/58.48 p15(X21,X21) ). % 58.42/58.48 % 58.42/58.48 cnf(p14_24,negated_conjecture, % 58.42/58.48 p14(X14,X14) ). % 58.42/58.48 % 58.42/58.48 cnf(p12_25,negated_conjecture, % 58.42/58.48 p12(X7,X7) ). % 58.42/58.48 % 58.42/58.48 cnf(p7_26,negated_conjecture, % 58.42/58.48 p7(c54,c55) ). % 58.42/58.48 % 58.42/58.48 cnf(p11_27,negated_conjecture, % 58.42/58.48 ( p11(X1,X2) % 58.42/58.48 | ~ p11(X0,X1) % 58.42/58.48 | ~ p11(X0,X2) ) ). % 58.42/58.48 % 58.42/58.48 cnf(p9_28,negated_conjecture, % 58.42/58.48 ( p9(X165,X166) % 58.42/58.48 | ~ p9(X167,X165) % 58.42/58.48 | ~ p9(X167,X166) ) ). % 58.42/58.48 % 58.42/58.48 cnf(p7_29,negated_conjecture, % 58.42/58.48 ( p7(X163,X164) % 58.42/58.48 | ~ p7(X162,X163) % 58.42/58.48 | ~ p7(X162,X164) ) ). % 58.42/58.48 % 58.42/58.48 cnf(p6_30,negated_conjecture, % 58.42/58.48 ( p6(X156,X157) % 58.42/58.48 | ~ p6(X155,X156) % 58.42/58.48 | ~ p6(X155,X157) ) ). % 58.42/58.48 % 58.42/58.48 cnf(p45_31,negated_conjecture, % 58.42/58.48 ( p45(X145,X146) % 58.42/58.48 | ~ p45(X144,X145) % 58.42/58.48 | ~ p45(X144,X146) ) ). % 58.42/58.48 % 58.42/58.48 cnf(p43_32,negated_conjecture, % 58.42/58.48 ( p43(X138,X139) % 58.42/58.48 | ~ p43(X137,X138) % 58.42/58.48 | ~ p43(X137,X139) ) ). % 58.42/58.48 % 58.42/58.48 cnf(p41_33,negated_conjecture, % 58.42/58.48 ( p41(X131,X132) % 58.42/58.48 | ~ p41(X130,X131) % 58.42/58.48 | ~ p41(X130,X132) ) ). % 58.42/58.48 % 58.42/58.48 cnf(p4_34,negated_conjecture, % 58.42/58.48 ( p4(X120,X121) % 58.42/58.48 | ~ p4(X119,X120) % 58.42/58.48 | ~ p4(X119,X121) ) ). % 58.42/58.48 % 58.42/58.48 cnf(p39_35,negated_conjecture, % 58.42/58.48 ( p39(X113,X114) % 58.42/58.48 | ~ p39(X112,X113) % 58.42/58.48 | ~ p39(X112,X114) ) ). % 58.42/58.48 % 58.42/58.48 cnf(p37_36,negated_conjecture, % 58.42/58.48 ( p37(X106,X107) % 58.42/58.48 | ~ p37(X105,X106) % 58.42/58.48 | ~ p37(X105,X107) ) ). % 58.42/58.48 % 58.42/58.48 cnf(p35_37,negated_conjecture, % 58.42/58.48 ( p35(X103,X104) % 58.42/58.48 | ~ p35(X102,X103) % 58.42/58.48 | ~ p35(X102,X104) ) ). % 58.42/58.48 % 58.42/58.48 cnf(p33_38,negated_conjecture, % 58.42/58.48 ( p33(X96,X97) % 58.42/58.48 | ~ p33(X95,X96) % 58.42/58.48 | ~ p33(X95,X97) ) ). % 58.42/58.48 % 58.42/58.48 cnf(p31_39,negated_conjecture, % 58.42/58.48 ( p31(X89,X90) % 58.42/58.48 | ~ p31(X88,X89) % 58.42/58.48 | ~ p31(X88,X90) ) ). % 58.42/58.48 % 58.42/58.48 cnf(p3_40,negated_conjecture, % 58.42/58.48 ( p3(X78,X79) % 58.42/58.48 | ~ p3(X77,X78) % 58.42/58.48 | ~ p3(X77,X79) ) ). % 58.42/58.48 % 58.42/58.48 cnf(p29_41,negated_conjecture, % 58.42/58.48 ( p29(X71,X72) % 58.42/58.48 | ~ p29(X70,X71) % 58.42/58.48 | ~ p29(X70,X72) ) ). % 58.42/58.48 % 58.42/58.48 cnf(p27_42,negated_conjecture, % 58.42/58.48 ( p27(X59,X60) % 58.42/58.48 | ~ p27(X58,X59) % 58.42/58.49 | ~ p27(X58,X60) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p25_43,negated_conjecture, % 58.42/58.49 ( p25(X56,X57) % 58.42/58.49 | ~ p25(X55,X56) % 58.42/58.49 | ~ p25(X55,X57) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p23_44,negated_conjecture, % 58.42/58.49 ( p23(X49,X50) % 58.42/58.49 | ~ p23(X48,X49) % 58.42/58.49 | ~ p23(X48,X50) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p21_45,negated_conjecture, % 58.42/58.49 ( p21(X42,X43) % 58.42/58.49 | ~ p21(X41,X42) % 58.42/58.49 | ~ p21(X41,X43) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p2_46,negated_conjecture, % 58.42/58.49 ( p2(X39,X40) % 58.42/58.49 | ~ p2(X38,X39) % 58.42/58.49 | ~ p2(X38,X40) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p19_47,negated_conjecture, % 58.42/58.49 ( p19(X32,X33) % 58.42/58.49 | ~ p19(X31,X32) % 58.42/58.49 | ~ p19(X31,X33) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p17_48,negated_conjecture, % 58.42/58.49 ( p17(X29,X30) % 58.42/58.49 | ~ p17(X28,X29) % 58.42/58.49 | ~ p17(X28,X30) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p15_49,negated_conjecture, % 58.42/58.49 ( p15(X22,X23) % 58.42/58.49 | ~ p15(X21,X22) % 58.42/58.49 | ~ p15(X21,X23) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p14_50,negated_conjecture, % 58.42/58.49 ( p14(X15,X16) % 58.42/58.49 | ~ p14(X14,X15) % 58.42/58.49 | ~ p14(X14,X16) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p12_51,negated_conjecture, % 58.42/58.49 ( p12(X8,X9) % 58.42/58.49 | ~ p12(X7,X8) % 58.42/58.49 | ~ p12(X7,X9) ) ). % 58.42/58.49 % 58.42/58.49 cnf(not_p47_52,negated_conjecture, % 58.42/58.49 ~ p47(f20(f22(f24(f26(c56,X65),X66),X67),X68),X68) ). % 58.42/58.49 % 58.42/58.49 cnf(p47_53,negated_conjecture, % 58.42/58.49 ( p47(X151,X152) % 58.42/58.49 | ~ p47(X153,X154) % 58.42/58.49 | ~ p7(X154,X152) % 58.42/58.49 | ~ p4(X153,X151) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p11_54,negated_conjecture, % 58.42/58.49 ( p11(f16(X3,X4),f16(X5,X6)) % 58.42/58.49 | ~ p14(X3,X5) % 58.42/58.49 | ~ p15(X4,X6) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p6_55,negated_conjecture, % 58.42/58.49 ( p6(f10(X158,X159),f10(X160,X161)) % 58.42/58.49 | ~ p3(X159,X161) % 58.42/58.49 | ~ p9(X158,X160) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p43_56,negated_conjecture, % 58.42/58.49 ( p43(f46(X140,X141),f46(X142,X143)) % 58.42/58.49 | ~ p4(X141,X143) % 58.42/58.49 | ~ p45(X140,X142) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p41_57,negated_conjecture, % 58.42/58.49 ( p41(f44(X133,X134),f44(X135,X136)) % 58.42/58.49 | ~ p15(X134,X136) % 58.42/58.49 | ~ p43(X133,X135) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p4_58,negated_conjecture, % 58.42/58.49 ( p4(f5(X126,X127),f5(X128,X129)) % 58.42/58.49 | ~ p2(X126,X128) % 58.42/58.49 | ~ p3(X127,X129) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p4_59,negated_conjecture, % 58.42/58.49 ( p4(f20(X122,X123),f20(X124,X125)) % 58.42/58.49 | ~ p19(X122,X124) % 58.42/58.49 | ~ p7(X123,X125) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p39_60,negated_conjecture, % 58.42/58.49 ( p39(f42(X115,X116),f42(X117,X118)) % 58.42/58.49 | ~ p12(X116,X118) % 58.42/58.49 | ~ p41(X115,X117) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p37_61,negated_conjecture, % 58.42/58.49 ( p37(f38(X108,X109),f38(X110,X111)) % 58.42/58.49 | ~ p12(X108,X110) % 58.42/58.49 | ~ p7(X109,X111) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p33_62,negated_conjecture, % 58.42/58.49 ( p33(f36(X98,X99),f36(X100,X101)) % 58.42/58.49 | ~ p35(X98,X100) % 58.42/58.49 | ~ p4(X99,X101) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p31_63,negated_conjecture, % 58.42/58.49 ( p31(f34(X91,X92),f34(X93,X94)) % 58.42/58.49 | ~ p15(X92,X94) % 58.42/58.49 | ~ p33(X91,X93) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p3_64,negated_conjecture, % 58.42/58.49 ( p3(f8(X84,X85),f8(X86,X87)) % 58.42/58.49 | ~ p6(X84,X86) % 58.42/58.49 | ~ p7(X85,X87) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p3_65,negated_conjecture, % 58.42/58.49 ( p3(f13(X80,X81),f13(X82,X83)) % 58.42/58.49 | ~ p11(X80,X82) % 58.42/58.49 | ~ p12(X81,X83) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p29_66,negated_conjecture, % 58.42/58.49 ( p29(f32(X73,X74),f32(X75,X76)) % 58.42/58.49 | ~ p12(X74,X76) % 58.42/58.49 | ~ p31(X73,X75) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p27_67,negated_conjecture, % 58.42/58.49 ( p27(f28(X61,X62),f28(X63,X64)) % 58.42/58.49 | ~ p15(X61,X63) % 58.42/58.49 | ~ p7(X62,X64) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p23_68,negated_conjecture, % 58.42/58.49 ( p23(f26(X51,X52),f26(X53,X54)) % 58.42/58.49 | ~ p25(X51,X53) % 58.42/58.49 | ~ p4(X52,X54) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p21_69,negated_conjecture, % 58.42/58.49 ( p21(f24(X44,X45),f24(X46,X47)) % 58.42/58.49 | ~ p15(X45,X47) % 58.42/58.49 | ~ p23(X44,X46) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p19_70,negated_conjecture, % 58.42/58.49 ( p19(f22(X34,X35),f22(X36,X37)) % 58.42/58.49 | ~ p12(X35,X37) % 58.42/58.49 | ~ p21(X34,X36) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p15_71,negated_conjecture, % 58.42/58.49 ( p15(f30(X24,X25),f30(X26,X27)) % 58.42/58.49 | ~ p29(X24,X26) % 58.42/58.49 | ~ p7(X25,X27) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p14_72,negated_conjecture, % 58.42/58.49 ( p14(f18(X17,X18),f18(X19,X20)) % 58.42/58.49 | ~ p17(X17,X19) % 58.42/58.49 | ~ p4(X18,X20) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p12_73,negated_conjecture, % 58.42/58.49 ( p12(f40(X10,X11),f40(X12,X13)) % 58.42/58.49 | ~ p39(X10,X12) % 58.42/58.49 | ~ p7(X11,X13) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p47_74,negated_conjecture, % 58.42/58.49 ( p47(X147,X148) % 58.42/58.49 | ~ p47(f5(c48,f13(f16(f18(c50,X147),X149),X150)),X148) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p47_75,negated_conjecture, % 58.42/58.49 ( p47(X65,X69) % 58.42/58.49 | ~ p47(f20(f22(f24(f26(c56,X65),X66),X67),X68),X69) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p47_76,negated_conjecture, % 58.42/58.49 ( p47(f5(c48,f13(f16(f18(c50,X147),X149),X150)),X148) % 58.42/58.49 | ~ p47(X147,X148) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p47_77,negated_conjecture, % 58.42/58.49 p47(f5(c48,f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c54)),c55) ). % 58.42/58.49 % 58.42/58.49 cnf(p27_78,negated_conjecture, % 58.42/58.49 ( p27(f28(f30(f32(f34(f36(c57,X65),X66),X67),X68),X69),f28(X66,X69)) % 58.42/58.49 | ~ p47(f20(f22(f24(f26(c56,X65),X66),X67),X68),X69) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p37_79,negated_conjecture, % 58.42/58.49 ( p37(f38(f40(f42(f44(f46(c58,X65),X66),X67),X68),X69),f38(X67,X69)) % 58.42/58.49 | ~ p47(f20(f22(f24(f26(c56,X65),X66),X67),X68),X69) ) ). % 58.42/58.49 % 58.42/58.49 cnf(p3_80,negated_conjecture, % 58.42/58.49 p3(f8(f10(c49,f13(f16(f18(c50,X65),X66),X67)),X68),f13(f16(f18(c50,f20(f22(f24(f26(c56,X65),X66),X67),X68)),f30(f32(f34(f36(c57,X65),X66),X67),X68)),f40(f42(f44(f46(c58,X65),X66),X67),X68))) ). % 58.42/58.49 % 58.42/58.49 %-------------------------------------------------------------------------- % 58.42/58.49 %------------------------------------------- % 58.42/58.49 % Proof found % 58.42/58.49 % SZS status Theorem for theBenchmark % 58.42/58.49 % SZS output start Proof % 58.47/58.50 %ClaNum:80(EqnAxiom:0) % 58.47/58.50 %VarNum:432(SingletonVarNum:215) % 58.47/58.50 %MaxLitNum:4 % 58.47/58.50 %MaxfuncDepth:6 % 58.47/58.50 %SharedTerms:19 % 58.47/58.50 %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 % 58.47/58.50 %singleGoalClaCount:29 % 58.47/58.50 [1]P1(a1,a8) % 58.47/58.50 [27]P25(f17(a2,f16(f12(a3,f11(f10(f9(a4,a5),a6),a7)),a1)),a8) % 58.47/58.50 [2]P2(x21,x21) % 58.47/58.50 [3]P26(x31,x31) % 58.47/58.50 [4]P1(x41,x41) % 58.47/58.50 [5]P3(x51,x51) % 58.47/58.50 [6]P4(x61,x61) % 58.47/58.50 [7]P5(x71,x71) % 58.47/58.50 [8]P6(x81,x81) % 58.47/58.50 [9]P7(x91,x91) % 58.47/58.50 [10]P8(x101,x101) % 58.47/58.50 [11]P9(x111,x111) % 58.47/58.50 [12]P10(x121,x121) % 58.47/58.50 [13]P11(x131,x131) % 58.47/58.50 [14]P12(x141,x141) % 58.47/58.50 [15]P13(x151,x151) % 58.47/58.50 [16]P14(x161,x161) % 58.47/58.50 [17]P15(x171,x171) % 58.47/58.50 [18]P16(x181,x181) % 58.47/58.50 [19]P17(x191,x191) % 58.47/58.50 [20]P18(x201,x201) % 58.47/58.50 [21]P19(x211,x211) % 58.47/58.50 [22]P20(x221,x221) % 58.47/58.50 [23]P21(x231,x231) % 58.47/58.50 [24]P22(x241,x241) % 58.47/58.50 [25]P23(x251,x251) % 58.47/58.50 [26]P24(x261,x261) % 58.47/58.50 [29]~P25(f21(f20(f19(f18(a13,x291),x292),x293),x294),x294) % 58.47/58.50 [28]P13(f16(f12(a3,f11(f10(f9(a4,x281),x282),x283)),x284),f11(f10(f9(a4,f21(f20(f19(f18(a13,x281),x282),x283),x284)),f25(f24(f23(f22(a14,x281),x282),x283),x284)),f30(f29(f28(f27(a15,x281),x282),x283),x284))) % 58.47/58.50 [76]~P25(x761,x764)+P25(f17(a2,f11(f10(f9(a4,x761),x762),x763)),x764) % 58.47/58.50 [77]P25(x771,x772)+~P25(f17(a2,f11(f10(f9(a4,x771),x773),x774)),x772) % 58.47/58.50 [78]P25(x781,x782)+~P25(f21(f20(f19(f18(a13,x781),x783),x784),x785),x782) % 58.47/58.50 [79]~P25(f21(f20(f19(f18(a13,x791),x792),x793),x794),x795)+P9(f31(f30(f29(f28(f27(a15,x791),x792),x793),x794),x795),f31(x793,x795)) % 58.47/58.50 [80]~P25(f21(f20(f19(f18(a13,x801),x802),x803),x804),x805)+P15(f26(f25(f24(f23(f22(a14,x801),x802),x803),x804),x805),f26(x802,x805)) % 58.47/58.50 [30]~P2(x303,x301)+P2(x301,x302)+~P2(x303,x302) % 58.47/58.50 [31]~P26(x313,x311)+P26(x311,x312)+~P26(x313,x312) % 58.47/58.50 [32]~P1(x323,x321)+P1(x321,x322)+~P1(x323,x322) % 58.47/58.50 [33]~P3(x333,x331)+P3(x331,x332)+~P3(x333,x332) % 58.47/58.50 [34]~P4(x343,x341)+P4(x341,x342)+~P4(x343,x342) % 58.47/58.50 [35]~P5(x353,x351)+P5(x351,x352)+~P5(x353,x352) % 58.47/58.50 [36]~P6(x363,x361)+P6(x361,x362)+~P6(x363,x362) % 58.47/58.50 [37]~P7(x373,x371)+P7(x371,x372)+~P7(x373,x372) % 58.47/58.50 [38]~P8(x383,x381)+P8(x381,x382)+~P8(x383,x382) % 58.47/58.50 [39]~P9(x393,x391)+P9(x391,x392)+~P9(x393,x392) % 58.47/58.50 [40]~P10(x403,x401)+P10(x401,x402)+~P10(x403,x402) % 58.47/58.50 [41]~P11(x413,x411)+P11(x411,x412)+~P11(x413,x412) % 58.47/58.50 [42]~P12(x423,x421)+P12(x421,x422)+~P12(x423,x422) % 58.47/58.50 [43]~P13(x433,x431)+P13(x431,x432)+~P13(x433,x432) % 58.47/58.50 [44]~P14(x443,x441)+P14(x441,x442)+~P14(x443,x442) % 58.47/58.50 [45]~P15(x453,x451)+P15(x451,x452)+~P15(x453,x452) % 58.47/58.50 [46]~P16(x463,x461)+P16(x461,x462)+~P16(x463,x462) % 58.47/58.50 [47]~P17(x473,x471)+P17(x471,x472)+~P17(x473,x472) % 58.47/58.50 [48]~P18(x483,x481)+P18(x481,x482)+~P18(x483,x482) % 58.47/58.50 [49]~P19(x493,x491)+P19(x491,x492)+~P19(x493,x492) % 58.47/58.50 [50]~P20(x503,x501)+P20(x501,x502)+~P20(x503,x502) % 58.47/58.50 [51]~P21(x513,x511)+P21(x511,x512)+~P21(x513,x512) % 58.47/58.50 [52]~P22(x523,x521)+P22(x521,x522)+~P22(x523,x522) % 58.47/58.50 [53]~P23(x533,x531)+P23(x531,x532)+~P23(x533,x532) % 58.47/58.50 [54]~P24(x543,x541)+P24(x541,x542)+~P24(x543,x542) % 58.47/58.50 [56]~P22(x562,x564)+~P23(x561,x563)+P2(f10(x561,x562),f10(x563,x564)) % 58.47/58.50 [57]~P26(x571,x573)+~P13(x572,x574)+P3(f12(x571,x572),f12(x573,x574)) % 58.47/58.50 [58]~P4(x581,x583)+~P7(x582,x584)+P5(f27(x581,x582),f27(x583,x584)) % 58.47/58.50 [59]~P5(x591,x593)+~P22(x592,x594)+P6(f28(x591,x592),f28(x593,x594)) % 58.47/58.50 [60]~P1(x602,x604)+~P20(x601,x603)+P7(f21(x601,x602),f21(x603,x604)) % 58.47/58.50 [61]~P13(x612,x614)+~P19(x611,x613)+P7(f17(x611,x612),f17(x613,x614)) % 58.47/58.50 [62]~P6(x621,x623)+~P24(x622,x624)+P8(f29(x621,x622),f29(x623,x624)) % 58.47/58.50 [63]~P1(x632,x634)+~P24(x631,x633)+P9(f31(x631,x632),f31(x633,x634)) % 58.47/58.50 [64]~P7(x642,x644)+~P10(x641,x643)+P11(f22(x641,x642),f22(x643,x644)) % 58.47/58.50 [65]~P11(x651,x653)+~P22(x652,x654)+P12(f23(x651,x652),f23(x653,x654)) % 58.47/58.50 [66]~P1(x662,x664)+~P3(x661,x663)+P13(f16(x661,x662),f16(x663,x664)) % 58.47/58.50 [67]~P2(x671,x673)+~P24(x672,x674)+P13(f11(x671,x672),f11(x673,x674)) % 58.47/58.50 [68]~P12(x681,x683)+~P24(x682,x684)+P14(f24(x681,x682),f24(x683,x684)) % 58.47/58.50 [69]~P1(x692,x694)+~P22(x691,x693)+P15(f26(x691,x692),f26(x693,x694)) % 58.47/58.50 [70]~P7(x702,x704)+~P16(x701,x703)+P17(f18(x701,x702),f18(x703,x704)) % 58.47/58.50 [71]~P17(x711,x713)+~P22(x712,x714)+P18(f19(x711,x712),f19(x713,x714)) % 58.47/58.50 [72]~P18(x721,x723)+~P24(x722,x724)+P20(f20(x721,x722),f20(x723,x724)) % 58.47/58.50 [73]~P1(x732,x734)+~P14(x731,x733)+P22(f25(x731,x732),f25(x733,x734)) % 58.47/58.50 [74]~P7(x742,x744)+~P21(x741,x743)+P23(f9(x741,x742),f9(x743,x744)) % 58.47/58.50 [75]~P1(x752,x754)+~P8(x751,x753)+P24(f30(x751,x752),f30(x753,x754)) % 58.47/58.50 [55]~P25(x554,x553)+P25(x551,x552)+~P1(x553,x552)+~P7(x554,x551) % 58.47/58.50 %EqnAxiom % 58.47/58.50 % 58.47/58.50 %------------------------------------------- % 58.47/58.52 cnf(81,plain, % 58.47/58.52 (P1(a8,a1)), % 58.47/58.52 inference(scs_inference,[],[1,4,32])). % 58.47/58.52 cnf(88,plain, % 58.47/58.52 (P25(f17(a2,f16(f12(a3,f11(f10(f9(a4,a5),a6),a7)),a1)),a1)), % 58.47/58.52 inference(scs_inference,[],[81,27,9,55])). % 58.47/58.52 cnf(100,plain, % 58.47/58.52 (P13(f16(x1001,a1),f16(x1001,a8))), % 58.47/58.52 inference(scs_inference,[],[5,1,33,66])). % 58.47/58.52 cnf(101,plain, % 58.47/58.52 (P13(f16(x1011,a8),f16(x1011,a1))), % 58.47/58.52 inference(scs_inference,[],[100,15,43])). % 58.47/58.52 cnf(116,plain, % 58.47/58.52 (P7(f17(x1161,f16(x1162,a8)),f17(x1161,f16(x1162,a1)))), % 58.47/58.52 inference(scs_inference,[],[21,101,49,61])). % 58.47/58.52 cnf(117,plain, % 58.47/58.52 (P7(f17(x1171,f16(x1172,a1)),f17(x1171,f16(x1172,a8)))), % 58.47/58.52 inference(scs_inference,[],[116,9,37])). % 58.47/58.52 cnf(120,plain, % 58.47/58.52 (P23(f9(x1201,f17(x1202,f16(x1203,a1))),f9(x1201,f17(x1202,f16(x1203,a8))))), % 58.47/58.52 inference(scs_inference,[],[23,117,51,74])). % 58.47/58.52 cnf(121,plain, % 58.47/58.52 (P2(f10(f9(x1211,f17(x1212,f16(x1213,a1))),x1214),f10(f9(x1211,f17(x1212,f16(x1213,a8))),x1214))), % 58.47/58.52 inference(scs_inference,[],[24,120,52,56])). % 58.47/58.52 cnf(125,plain, % 58.47/58.52 (P23(f9(x1251,f17(x1252,f16(x1253,a8))),f9(x1251,f17(x1252,f16(x1253,a1))))), % 58.47/58.52 inference(scs_inference,[],[121,120,2,25,30,53])). % 58.47/58.52 cnf(160,plain, % 58.47/58.52 (P13(f11(f10(f9(x1601,f17(x1602,f16(x1603,a8))),x1604),x1605),f11(f10(f9(x1601,f17(x1602,f16(x1603,a1))),x1604),x1605))), % 58.47/58.52 inference(scs_inference,[],[26,24,125,67,56])). % 58.47/58.52 cnf(161,plain, % 58.47/58.52 (P13(f11(f10(f9(x1611,f17(x1612,f16(x1613,a1))),x1614),x1615),f11(f10(f9(x1611,f17(x1612,f16(x1613,a8))),x1614),x1615))), % 58.47/58.52 inference(scs_inference,[],[160,15,43])). % 58.47/58.52 cnf(168,plain, % 58.47/58.52 (P17(f18(x1681,f17(x1682,f11(f10(f9(x1683,f17(x1684,f16(x1685,a1))),x1686),x1687))),f18(x1681,f17(x1682,f11(f10(f9(x1683,f17(x1684,f16(x1685,a8))),x1686),x1687))))), % 58.47/58.52 inference(scs_inference,[],[18,21,161,70,61])). % 58.47/58.52 cnf(177,plain, % 58.47/58.52 (P25(f17(a2,f11(f10(f9(a4,f17(a2,f16(f12(a3,f11(f10(f9(a4,a5),a6),a7)),a8))),x1771),x1772)),a8)), % 58.47/58.52 inference(scs_inference,[],[1,88,117,76,55])). % 58.47/58.52 cnf(182,plain, % 58.47/58.52 (~P7(f17(a2,f16(f12(a3,f11(f10(f9(a4,a5),a6),a7)),a1)),f17(a2,f11(f10(f9(a4,f21(f20(f19(f18(a13,x1821),x1822),x1823),a8)),x1824),x1825)))), % 58.47/58.52 inference(scs_inference,[],[29,1,88,77,55])). % 58.47/58.52 cnf(1535,plain, % 58.47/58.52 ($false), % 58.47/58.52 inference(scs_inference,[],[168,182,177,101,19,28,21,77,61,47,43]), % 58.47/58.52 ['proof']). % 58.47/58.52 % SZS output end Proof % 58.47/58.52 % Total time :57.840000s %------------------------------------------------------------------------------