%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN702-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 : n032.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 2.20s 2.31s % Output : CNFRefutation 2.20s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.09 % Problem : SYN702-1 : TPTP v8.2.0. Released v2.5.0. % 0.03/0.09 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.09/0.28 % Computer : n032.cluster.edu % 0.09/0.28 % Model : x86_64 x86_64 % 0.09/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.28 % Memory : 8042.1875MB % 0.09/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.28 % CPULimit : 300 % 0.09/0.28 % WCLimit : 300 % 0.09/0.28 % DateTime : Sun Jun 23 19:26:54 EDT 2024 % 0.09/0.28 % CPUTime : % 0.13/0.44 start to proof:theBenchmark % 2.20/2.29 %------------------------------------------- % 2.20/2.29 % File :CSE---1.7 % 2.20/2.29 % Problem :theBenchmark % 2.20/2.29 % Transform :cnf % 2.20/2.29 % Format :tptp:raw % 2.20/2.29 % Command :java -jar mcs_scs.jar %d %s % 2.20/2.29 % 2.20/2.29 % Result :Theorem 1.810000s % 2.20/2.29 % Output :CNFRefutation 1.810000s % 2.20/2.29 %------------------------------------------- % 2.20/2.30 %-------------------------------------------------------------------------- % 2.20/2.30 % File : SYN702-1 : TPTP v8.2.0. Released v2.5.0. % 2.20/2.30 % Domain : Syntactic % 2.20/2.30 % Problem : Harrison problem 4672 % 2.20/2.30 % Version : Especial. % 2.20/2.30 % English : % 2.20/2.30 % 2.20/2.30 % Refs : [Har01] Email to G. Sutcliffe % 2.20/2.30 % Source : [Har01] % 2.20/2.30 % Names : % 2.20/2.30 % 2.20/2.30 % Status : Unsatisfiable % 2.20/2.30 % 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.00 v5.3.0, 0.10 v5.2.0, 0.00 v2.5.0 % 2.20/2.30 % Syntax : Number of clauses : 79 ( 28 unt; 0 nHn; 52 RR) % 2.20/2.30 % Number of literals : 177 ( 0 equ; 99 neg) % 2.20/2.30 % Maximal clause size : 4 ( 2 avg) % 2.20/2.30 % Maximal term depth : 8 ( 1 avg) % 2.20/2.30 % Number of predicates : 26 ( 26 usr; 0 prp; 2-2 aty) % 2.20/2.30 % Number of functors : 30 ( 30 usr; 10 con; 0-2 aty) % 2.20/2.30 % Number of variables : 215 ( 10 sgn) % 2.20/2.30 % SPC : CNF_UNS_RFO_NEQ_HRN % 2.20/2.30 % 2.20/2.30 % Comments : % 2.20/2.30 %-------------------------------------------------------------------------- % 2.20/2.30 cnf(p11_1,negated_conjecture, % 2.20/2.30 p11(X0,X0) ). % 2.20/2.30 % 2.20/2.30 cnf(p9_2,negated_conjecture, % 2.20/2.30 p9(X167,X167) ). % 2.20/2.30 % 2.20/2.30 cnf(p7_3,negated_conjecture, % 2.20/2.30 p7(X162,X162) ). % 2.20/2.30 % 2.20/2.30 cnf(p6_4,negated_conjecture, % 2.20/2.30 p6(X155,X155) ). % 2.20/2.30 % 2.20/2.30 cnf(p45_5,negated_conjecture, % 2.20/2.30 p45(X144,X144) ). % 2.20/2.30 % 2.20/2.30 cnf(p43_6,negated_conjecture, % 2.20/2.30 p43(X137,X137) ). % 2.20/2.30 % 2.20/2.30 cnf(p41_7,negated_conjecture, % 2.20/2.30 p41(X130,X130) ). % 2.20/2.30 % 2.20/2.30 cnf(p4_8,negated_conjecture, % 2.20/2.30 p4(X119,X119) ). % 2.20/2.30 % 2.20/2.30 cnf(p39_9,negated_conjecture, % 2.20/2.30 p39(X112,X112) ). % 2.20/2.30 % 2.20/2.30 cnf(p37_10,negated_conjecture, % 2.20/2.30 p37(X105,X105) ). % 2.20/2.30 % 2.20/2.30 cnf(p35_11,negated_conjecture, % 2.20/2.30 p35(X102,X102) ). % 2.20/2.30 % 2.20/2.30 cnf(p33_12,negated_conjecture, % 2.20/2.30 p33(X95,X95) ). % 2.20/2.30 % 2.20/2.30 cnf(p31_13,negated_conjecture, % 2.20/2.30 p31(X88,X88) ). % 2.20/2.30 % 2.20/2.30 cnf(p3_14,negated_conjecture, % 2.20/2.30 p3(X77,X77) ). % 2.20/2.30 % 2.20/2.30 cnf(p29_15,negated_conjecture, % 2.20/2.30 p29(X70,X70) ). % 2.20/2.30 % 2.20/2.30 cnf(p27_16,negated_conjecture, % 2.20/2.30 p27(X58,X58) ). % 2.20/2.30 % 2.20/2.30 cnf(p25_17,negated_conjecture, % 2.20/2.30 p25(X55,X55) ). % 2.20/2.30 % 2.20/2.30 cnf(p23_18,negated_conjecture, % 2.20/2.30 p23(X48,X48) ). % 2.20/2.30 % 2.20/2.30 cnf(p21_19,negated_conjecture, % 2.20/2.30 p21(X41,X41) ). % 2.20/2.30 % 2.20/2.30 cnf(p2_20,negated_conjecture, % 2.20/2.30 p2(X38,X38) ). % 2.20/2.30 % 2.20/2.30 cnf(p19_21,negated_conjecture, % 2.20/2.30 p19(X31,X31) ). % 2.20/2.30 % 2.20/2.30 cnf(p17_22,negated_conjecture, % 2.20/2.30 p17(X28,X28) ). % 2.20/2.30 % 2.20/2.30 cnf(p15_23,negated_conjecture, % 2.20/2.30 p15(X21,X21) ). % 2.20/2.30 % 2.20/2.30 cnf(p14_24,negated_conjecture, % 2.20/2.30 p14(X14,X14) ). % 2.20/2.30 % 2.20/2.30 cnf(p12_25,negated_conjecture, % 2.20/2.30 p12(X7,X7) ). % 2.20/2.30 % 2.20/2.30 cnf(p11_26,negated_conjecture, % 2.20/2.30 ( p11(X1,X2) % 2.20/2.30 | ~ p11(X0,X1) % 2.20/2.30 | ~ p11(X0,X2) ) ). % 2.20/2.30 % 2.20/2.30 cnf(p9_27,negated_conjecture, % 2.20/2.30 ( p9(X165,X166) % 2.20/2.30 | ~ p9(X167,X165) % 2.20/2.30 | ~ p9(X167,X166) ) ). % 2.20/2.30 % 2.20/2.30 cnf(p7_28,negated_conjecture, % 2.20/2.30 ( p7(X163,X164) % 2.20/2.30 | ~ p7(X162,X163) % 2.20/2.30 | ~ p7(X162,X164) ) ). % 2.20/2.30 % 2.20/2.30 cnf(p6_29,negated_conjecture, % 2.20/2.30 ( p6(X156,X157) % 2.20/2.30 | ~ p6(X155,X156) % 2.20/2.30 | ~ p6(X155,X157) ) ). % 2.20/2.30 % 2.20/2.30 cnf(p45_30,negated_conjecture, % 2.20/2.30 ( p45(X145,X146) % 2.20/2.30 | ~ p45(X144,X145) % 2.20/2.30 | ~ p45(X144,X146) ) ). % 2.20/2.30 % 2.20/2.30 cnf(p43_31,negated_conjecture, % 2.20/2.30 ( p43(X138,X139) % 2.20/2.30 | ~ p43(X137,X138) % 2.20/2.30 | ~ p43(X137,X139) ) ). % 2.20/2.30 % 2.20/2.30 cnf(p41_32,negated_conjecture, % 2.20/2.30 ( p41(X131,X132) % 2.20/2.30 | ~ p41(X130,X131) % 2.20/2.30 | ~ p41(X130,X132) ) ). % 2.20/2.30 % 2.20/2.30 cnf(p4_33,negated_conjecture, % 2.20/2.30 ( p4(X120,X121) % 2.20/2.30 | ~ p4(X119,X120) % 2.20/2.30 | ~ p4(X119,X121) ) ). % 2.20/2.30 % 2.20/2.30 cnf(p39_34,negated_conjecture, % 2.20/2.30 ( p39(X113,X114) % 2.20/2.30 | ~ p39(X112,X113) % 2.20/2.30 | ~ p39(X112,X114) ) ). % 2.20/2.30 % 2.20/2.30 cnf(p37_35,negated_conjecture, % 2.20/2.30 ( p37(X106,X107) % 2.20/2.30 | ~ p37(X105,X106) % 2.20/2.30 | ~ p37(X105,X107) ) ). % 2.20/2.30 % 2.20/2.30 cnf(p35_36,negated_conjecture, % 2.20/2.30 ( p35(X103,X104) % 2.20/2.30 | ~ p35(X102,X103) % 2.20/2.30 | ~ p35(X102,X104) ) ). % 2.20/2.30 % 2.20/2.30 cnf(p33_37,negated_conjecture, % 2.20/2.30 ( p33(X96,X97) % 2.20/2.30 | ~ p33(X95,X96) % 2.20/2.30 | ~ p33(X95,X97) ) ). % 2.20/2.30 % 2.20/2.30 cnf(p31_38,negated_conjecture, % 2.20/2.30 ( p31(X89,X90) % 2.20/2.30 | ~ p31(X88,X89) % 2.20/2.30 | ~ p31(X88,X90) ) ). % 2.20/2.30 % 2.20/2.30 cnf(p3_39,negated_conjecture, % 2.20/2.30 ( p3(X78,X79) % 2.20/2.30 | ~ p3(X77,X78) % 2.20/2.30 | ~ p3(X77,X79) ) ). % 2.20/2.30 % 2.20/2.30 cnf(p29_40,negated_conjecture, % 2.20/2.30 ( p29(X71,X72) % 2.20/2.30 | ~ p29(X70,X71) % 2.20/2.30 | ~ p29(X70,X72) ) ). % 2.20/2.30 % 2.20/2.30 cnf(p27_41,negated_conjecture, % 2.20/2.30 ( p27(X59,X60) % 2.20/2.30 | ~ p27(X58,X59) % 2.20/2.30 | ~ p27(X58,X60) ) ). % 2.20/2.30 % 2.20/2.30 cnf(p25_42,negated_conjecture, % 2.20/2.30 ( p25(X56,X57) % 2.20/2.30 | ~ p25(X55,X56) % 2.20/2.30 | ~ p25(X55,X57) ) ). % 2.20/2.30 % 2.20/2.30 cnf(p23_43,negated_conjecture, % 2.20/2.30 ( p23(X49,X50) % 2.20/2.30 | ~ p23(X48,X49) % 2.20/2.30 | ~ p23(X48,X50) ) ). % 2.20/2.30 % 2.20/2.30 cnf(p21_44,negated_conjecture, % 2.20/2.30 ( p21(X42,X43) % 2.20/2.30 | ~ p21(X41,X42) % 2.20/2.30 | ~ p21(X41,X43) ) ). % 2.20/2.30 % 2.20/2.30 cnf(p2_45,negated_conjecture, % 2.20/2.30 ( p2(X39,X40) % 2.20/2.30 | ~ p2(X38,X39) % 2.20/2.30 | ~ p2(X38,X40) ) ). % 2.20/2.30 % 2.20/2.30 cnf(p19_46,negated_conjecture, % 2.20/2.30 ( p19(X32,X33) % 2.20/2.30 | ~ p19(X31,X32) % 2.20/2.30 | ~ p19(X31,X33) ) ). % 2.20/2.30 % 2.20/2.30 cnf(p17_47,negated_conjecture, % 2.20/2.30 ( p17(X29,X30) % 2.20/2.30 | ~ p17(X28,X29) % 2.20/2.30 | ~ p17(X28,X30) ) ). % 2.20/2.30 % 2.20/2.30 cnf(p15_48,negated_conjecture, % 2.20/2.30 ( p15(X22,X23) % 2.20/2.30 | ~ p15(X21,X22) % 2.20/2.30 | ~ p15(X21,X23) ) ). % 2.20/2.30 % 2.20/2.30 cnf(p14_49,negated_conjecture, % 2.20/2.30 ( p14(X15,X16) % 2.20/2.30 | ~ p14(X14,X15) % 2.20/2.30 | ~ p14(X14,X16) ) ). % 2.20/2.30 % 2.20/2.30 cnf(p12_50,negated_conjecture, % 2.20/2.30 ( p12(X8,X9) % 2.20/2.31 | ~ p12(X7,X8) % 2.20/2.31 | ~ p12(X7,X9) ) ). % 2.20/2.31 % 2.20/2.31 cnf(not_p47_51,negated_conjecture, % 2.20/2.31 ~ p47(f20(f22(f24(f26(c55,X65),X66),X67),X68),X68) ). % 2.20/2.31 % 2.20/2.31 cnf(p47_52,negated_conjecture, % 2.20/2.31 ( p47(X151,X152) % 2.20/2.31 | ~ p47(X153,X154) % 2.20/2.31 | ~ p7(X154,X152) % 2.20/2.31 | ~ p4(X153,X151) ) ). % 2.20/2.31 % 2.20/2.31 cnf(p11_53,negated_conjecture, % 2.20/2.31 ( p11(f16(X3,X4),f16(X5,X6)) % 2.20/2.31 | ~ p14(X3,X5) % 2.20/2.31 | ~ p15(X4,X6) ) ). % 2.20/2.31 % 2.20/2.31 cnf(p6_54,negated_conjecture, % 2.20/2.31 ( p6(f10(X158,X159),f10(X160,X161)) % 2.20/2.31 | ~ p3(X159,X161) % 2.20/2.31 | ~ p9(X158,X160) ) ). % 2.20/2.31 % 2.20/2.31 cnf(p43_55,negated_conjecture, % 2.20/2.31 ( p43(f46(X140,X141),f46(X142,X143)) % 2.20/2.31 | ~ p4(X141,X143) % 2.20/2.31 | ~ p45(X140,X142) ) ). % 2.20/2.31 % 2.20/2.31 cnf(p41_56,negated_conjecture, % 2.20/2.31 ( p41(f44(X133,X134),f44(X135,X136)) % 2.20/2.31 | ~ p15(X134,X136) % 2.20/2.31 | ~ p43(X133,X135) ) ). % 2.20/2.31 % 2.20/2.31 cnf(p4_57,negated_conjecture, % 2.20/2.31 ( p4(f5(X126,X127),f5(X128,X129)) % 2.20/2.31 | ~ p2(X126,X128) % 2.20/2.31 | ~ p3(X127,X129) ) ). % 2.20/2.31 % 2.20/2.31 cnf(p4_58,negated_conjecture, % 2.20/2.31 ( p4(f20(X122,X123),f20(X124,X125)) % 2.20/2.31 | ~ p19(X122,X124) % 2.20/2.31 | ~ p7(X123,X125) ) ). % 2.20/2.31 % 2.20/2.31 cnf(p39_59,negated_conjecture, % 2.20/2.31 ( p39(f42(X115,X116),f42(X117,X118)) % 2.20/2.31 | ~ p12(X116,X118) % 2.20/2.31 | ~ p41(X115,X117) ) ). % 2.20/2.31 % 2.20/2.31 cnf(p37_60,negated_conjecture, % 2.20/2.31 ( p37(f38(X108,X109),f38(X110,X111)) % 2.20/2.31 | ~ p12(X108,X110) % 2.20/2.31 | ~ p7(X109,X111) ) ). % 2.20/2.31 % 2.20/2.31 cnf(p33_61,negated_conjecture, % 2.20/2.31 ( p33(f36(X98,X99),f36(X100,X101)) % 2.20/2.31 | ~ p35(X98,X100) % 2.20/2.31 | ~ p4(X99,X101) ) ). % 2.20/2.31 % 2.20/2.31 cnf(p31_62,negated_conjecture, % 2.20/2.31 ( p31(f34(X91,X92),f34(X93,X94)) % 2.20/2.31 | ~ p15(X92,X94) % 2.20/2.31 | ~ p33(X91,X93) ) ). % 2.20/2.31 % 2.20/2.31 cnf(p3_63,negated_conjecture, % 2.20/2.31 ( p3(f8(X84,X85),f8(X86,X87)) % 2.20/2.31 | ~ p6(X84,X86) % 2.20/2.31 | ~ p7(X85,X87) ) ). % 2.20/2.31 % 2.20/2.31 cnf(p3_64,negated_conjecture, % 2.20/2.31 ( p3(f13(X80,X81),f13(X82,X83)) % 2.20/2.31 | ~ p11(X80,X82) % 2.20/2.31 | ~ p12(X81,X83) ) ). % 2.20/2.31 % 2.20/2.31 cnf(p29_65,negated_conjecture, % 2.20/2.31 ( p29(f32(X73,X74),f32(X75,X76)) % 2.20/2.31 | ~ p12(X74,X76) % 2.20/2.31 | ~ p31(X73,X75) ) ). % 2.20/2.31 % 2.20/2.31 cnf(p27_66,negated_conjecture, % 2.20/2.31 ( p27(f28(X61,X62),f28(X63,X64)) % 2.20/2.31 | ~ p15(X61,X63) % 2.20/2.31 | ~ p7(X62,X64) ) ). % 2.20/2.31 % 2.20/2.31 cnf(p23_67,negated_conjecture, % 2.20/2.31 ( p23(f26(X51,X52),f26(X53,X54)) % 2.20/2.31 | ~ p25(X51,X53) % 2.20/2.31 | ~ p4(X52,X54) ) ). % 2.20/2.31 % 2.20/2.31 cnf(p21_68,negated_conjecture, % 2.20/2.31 ( p21(f24(X44,X45),f24(X46,X47)) % 2.20/2.31 | ~ p15(X45,X47) % 2.20/2.31 | ~ p23(X44,X46) ) ). % 2.20/2.31 % 2.20/2.31 cnf(p19_69,negated_conjecture, % 2.20/2.31 ( p19(f22(X34,X35),f22(X36,X37)) % 2.20/2.31 | ~ p12(X35,X37) % 2.20/2.31 | ~ p21(X34,X36) ) ). % 2.20/2.31 % 2.20/2.31 cnf(p15_70,negated_conjecture, % 2.20/2.31 ( p15(f30(X24,X25),f30(X26,X27)) % 2.20/2.31 | ~ p29(X24,X26) % 2.20/2.31 | ~ p7(X25,X27) ) ). % 2.20/2.31 % 2.20/2.31 cnf(p14_71,negated_conjecture, % 2.20/2.31 ( p14(f18(X17,X18),f18(X19,X20)) % 2.20/2.31 | ~ p17(X17,X19) % 2.20/2.31 | ~ p4(X18,X20) ) ). % 2.20/2.31 % 2.20/2.31 cnf(p12_72,negated_conjecture, % 2.20/2.31 ( p12(f40(X10,X11),f40(X12,X13)) % 2.20/2.31 | ~ p39(X10,X12) % 2.20/2.31 | ~ p7(X11,X13) ) ). % 2.20/2.31 % 2.20/2.31 cnf(p47_73,negated_conjecture, % 2.20/2.31 ( p47(X147,X148) % 2.20/2.31 | ~ p47(f5(c48,f13(f16(f18(c50,X147),X149),X150)),X148) ) ). % 2.20/2.31 % 2.20/2.31 cnf(p47_74,negated_conjecture, % 2.20/2.31 ( p47(X65,X69) % 2.20/2.31 | ~ p47(f20(f22(f24(f26(c55,X65),X66),X67),X68),X69) ) ). % 2.20/2.31 % 2.20/2.31 cnf(p47_75,negated_conjecture, % 2.20/2.31 ( p47(f5(c48,f13(f16(f18(c50,X147),X149),X150)),X148) % 2.20/2.31 | ~ p47(X147,X148) ) ). % 2.20/2.31 % 2.20/2.31 cnf(p47_76,negated_conjecture, % 2.20/2.31 p47(f5(c48,f8(f10(c49,f13(f16(f18(c50,c51),c52),c53)),c54)),c54) ). % 2.20/2.31 % 2.20/2.31 cnf(p27_77,negated_conjecture, % 2.20/2.31 ( p27(f28(f30(f32(f34(f36(c56,X65),X66),X67),X68),X69),f28(X66,X69)) % 2.20/2.31 | ~ p47(f20(f22(f24(f26(c55,X65),X66),X67),X68),X69) ) ). % 2.20/2.31 % 2.20/2.31 cnf(p37_78,negated_conjecture, % 2.20/2.31 ( p37(f38(f40(f42(f44(f46(c57,X65),X66),X67),X68),X69),f38(X67,X69)) % 2.20/2.31 | ~ p47(f20(f22(f24(f26(c55,X65),X66),X67),X68),X69) ) ). % 2.20/2.31 % 2.20/2.31 cnf(p3_79,negated_conjecture, % 2.20/2.31 p3(f8(f10(c49,f13(f16(f18(c50,X65),X66),X67)),X68),f13(f16(f18(c50,f20(f22(f24(f26(c55,X65),X66),X67),X68)),f30(f32(f34(f36(c56,X65),X66),X67),X68)),f40(f42(f44(f46(c57,X65),X66),X67),X68))) ). % 2.20/2.31 % 2.20/2.31 %-------------------------------------------------------------------------- % 2.20/2.31 %------------------------------------------- % 2.20/2.31 % Proof found % 2.20/2.31 % SZS status Theorem for theBenchmark % 2.20/2.31 % SZS output start Proof % 2.20/2.31 %ClaNum:79(EqnAxiom:0) % 2.20/2.31 %VarNum:432(SingletonVarNum:215) % 2.20/2.31 %MaxLitNum:4 % 2.20/2.31 %MaxfuncDepth:6 % 2.20/2.31 %SharedTerms:17 % 2.20/2.31 %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 % 2.20/2.31 %singleGoalClaCount:28 % 2.20/2.31 [26]P26(f16(a1,f15(f10(a2,f9(f7(f5(a3,a4),a6),a8)),a11)),a11) % 2.20/2.31 [1]P1(x11,x11) % 2.20/2.31 [2]P2(x21,x21) % 2.20/2.31 [3]P3(x31,x31) % 2.20/2.31 [4]P4(x41,x41) % 2.20/2.31 [5]P5(x51,x51) % 2.20/2.31 [6]P6(x61,x61) % 2.20/2.31 [7]P7(x71,x71) % 2.20/2.31 [8]P8(x81,x81) % 2.20/2.31 [9]P9(x91,x91) % 2.20/2.31 [10]P10(x101,x101) % 2.20/2.31 [11]P11(x111,x111) % 2.20/2.31 [12]P12(x121,x121) % 2.20/2.31 [13]P13(x131,x131) % 2.20/2.31 [14]P14(x141,x141) % 2.20/2.31 [15]P15(x151,x151) % 2.20/2.31 [16]P16(x161,x161) % 2.20/2.31 [17]P17(x171,x171) % 2.20/2.31 [18]P18(x181,x181) % 2.20/2.31 [19]P19(x191,x191) % 2.20/2.31 [20]P20(x201,x201) % 2.20/2.31 [21]P21(x211,x211) % 2.20/2.31 [22]P22(x221,x221) % 2.20/2.31 [23]P23(x231,x231) % 2.20/2.31 [24]P24(x241,x241) % 2.20/2.31 [25]P25(x251,x251) % 2.20/2.31 [28]~P26(f20(f19(f18(f17(a12,x281),x282),x283),x284),x284) % 2.20/2.31 [27]P14(f15(f10(a2,f9(f7(f5(a3,x271),x272),x273)),x274),f9(f7(f5(a3,f20(f19(f18(f17(a12,x271),x272),x273),x274)),f24(f23(f22(f21(a13,x271),x272),x273),x274)),f29(f28(f27(f26(a14,x271),x272),x273),x274))) % 2.20/2.31 [75]~P26(x751,x754)+P26(f16(a1,f9(f7(f5(a3,x751),x752),x753)),x754) % 2.20/2.31 [76]P26(x761,x762)+~P26(f16(a1,f9(f7(f5(a3,x761),x763),x764)),x762) % 2.20/2.31 [77]P26(x771,x772)+~P26(f20(f19(f18(f17(a12,x771),x773),x774),x775),x772) % 2.20/2.31 [78]~P26(f20(f19(f18(f17(a12,x781),x782),x783),x784),x785)+P10(f30(f29(f28(f27(f26(a14,x781),x782),x783),x784),x785),f30(x783,x785)) % 2.20/2.31 [79]~P26(f20(f19(f18(f17(a12,x791),x792),x793),x794),x795)+P16(f25(f24(f23(f22(f21(a13,x791),x792),x793),x794),x795),f25(x792,x795)) % 2.20/2.31 [29]~P1(x293,x291)+P1(x291,x292)+~P1(x293,x292) % 2.20/2.31 [30]~P2(x303,x301)+P2(x301,x302)+~P2(x303,x302) % 2.20/2.31 [31]~P3(x313,x311)+P3(x311,x312)+~P3(x313,x312) % 2.20/2.31 [32]~P4(x323,x321)+P4(x321,x322)+~P4(x323,x322) % 2.20/2.31 [33]~P5(x333,x331)+P5(x331,x332)+~P5(x333,x332) % 2.20/2.31 [34]~P6(x343,x341)+P6(x341,x342)+~P6(x343,x342) % 2.20/2.31 [35]~P7(x353,x351)+P7(x351,x352)+~P7(x353,x352) % 2.20/2.31 [36]~P8(x363,x361)+P8(x361,x362)+~P8(x363,x362) % 2.20/2.31 [37]~P9(x373,x371)+P9(x371,x372)+~P9(x373,x372) % 2.20/2.31 [38]~P10(x383,x381)+P10(x381,x382)+~P10(x383,x382) % 2.20/2.31 [39]~P11(x393,x391)+P11(x391,x392)+~P11(x393,x392) % 2.20/2.31 [40]~P12(x403,x401)+P12(x401,x402)+~P12(x403,x402) % 2.20/2.31 [41]~P13(x413,x411)+P13(x411,x412)+~P13(x413,x412) % 2.20/2.31 [42]~P14(x423,x421)+P14(x421,x422)+~P14(x423,x422) % 2.20/2.31 [43]~P15(x433,x431)+P15(x431,x432)+~P15(x433,x432) % 2.20/2.31 [44]~P16(x443,x441)+P16(x441,x442)+~P16(x443,x442) % 2.20/2.31 [45]~P17(x453,x451)+P17(x451,x452)+~P17(x453,x452) % 2.20/2.31 [46]~P18(x463,x461)+P18(x461,x462)+~P18(x463,x462) % 2.20/2.31 [47]~P19(x473,x471)+P19(x471,x472)+~P19(x473,x472) % 2.20/2.31 [48]~P20(x483,x481)+P20(x481,x482)+~P20(x483,x482) % 2.20/2.31 [49]~P21(x493,x491)+P21(x491,x492)+~P21(x493,x492) % 2.20/2.31 [50]~P22(x503,x501)+P22(x501,x502)+~P22(x503,x502) % 2.20/2.31 [51]~P23(x513,x511)+P23(x511,x512)+~P23(x513,x512) % 2.20/2.31 [52]~P24(x523,x521)+P24(x521,x522)+~P24(x523,x522) % 2.20/2.31 [53]~P25(x533,x531)+P25(x531,x532)+~P25(x533,x532) % 2.20/2.31 [55]~P23(x552,x554)+~P24(x551,x553)+P1(f7(x551,x552),f7(x553,x554)) % 2.20/2.31 [56]~P2(x561,x563)+~P14(x562,x564)+P4(f10(x561,x562),f10(x563,x564)) % 2.20/2.31 [57]~P5(x571,x573)+~P8(x572,x574)+P6(f26(x571,x572),f26(x573,x574)) % 2.20/2.31 [58]~P6(x581,x583)+~P23(x582,x584)+P7(f27(x581,x582),f27(x583,x584)) % 2.20/2.31 [59]~P3(x592,x594)+~P21(x591,x593)+P8(f20(x591,x592),f20(x593,x594)) % 2.20/2.31 [60]~P14(x602,x604)+~P20(x601,x603)+P8(f16(x601,x602),f16(x603,x604)) % 2.20/2.31 [61]~P7(x611,x613)+~P25(x612,x614)+P9(f28(x611,x612),f28(x613,x614)) % 2.20/2.31 [62]~P3(x622,x624)+~P25(x621,x623)+P10(f30(x621,x622),f30(x623,x624)) % 2.20/2.31 [63]~P8(x632,x634)+~P11(x631,x633)+P12(f21(x631,x632),f21(x633,x634)) % 2.20/2.31 [64]~P12(x641,x643)+~P23(x642,x644)+P13(f22(x641,x642),f22(x643,x644)) % 2.20/2.31 [65]~P3(x652,x654)+~P4(x651,x653)+P14(f15(x651,x652),f15(x653,x654)) % 2.20/2.31 [66]~P1(x661,x663)+~P25(x662,x664)+P14(f9(x661,x662),f9(x663,x664)) % 2.20/2.31 [67]~P13(x671,x673)+~P25(x672,x674)+P15(f23(x671,x672),f23(x673,x674)) % 2.20/2.31 [68]~P3(x682,x684)+~P23(x681,x683)+P16(f25(x681,x682),f25(x683,x684)) % 2.20/2.31 [69]~P8(x692,x694)+~P17(x691,x693)+P18(f17(x691,x692),f17(x693,x694)) % 2.20/2.31 [70]~P18(x701,x703)+~P23(x702,x704)+P19(f18(x701,x702),f18(x703,x704)) % 2.20/2.31 [71]~P19(x711,x713)+~P25(x712,x714)+P21(f19(x711,x712),f19(x713,x714)) % 2.20/2.31 [72]~P3(x722,x724)+~P15(x721,x723)+P23(f24(x721,x722),f24(x723,x724)) % 2.20/2.31 [73]~P8(x732,x734)+~P22(x731,x733)+P24(f5(x731,x732),f5(x733,x734)) % 2.20/2.31 [74]~P3(x742,x744)+~P9(x741,x743)+P25(f29(x741,x742),f29(x743,x744)) % 2.20/2.31 [54]~P26(x544,x543)+P26(x541,x542)+~P3(x543,x542)+~P8(x544,x541) % 2.20/2.31 %EqnAxiom % 2.20/2.31 % 2.20/2.31 %------------------------------------------- % 2.20/2.31 cnf(80,plain, % 2.20/2.31 (P26(f16(a1,f9(f7(f5(a3,x801),x802),x803)),x804)+~P26(f16(a1,f9(f7(f5(a3,x801),x805),x806)),x804)), % 2.20/2.31 inference(scs_inference,[],[75,76])). % 2.20/2.31 cnf(103,plain, % 2.20/2.31 (~P26(f16(a1,f9(f7(f5(a3,f20(f19(f18(f17(a12,x1031),x1032),x1033),x1034)),x1035),x1036)),x1034)), % 2.20/2.31 inference(scs_inference,[],[28,76,80])). % 2.20/2.31 cnf(122,plain, % 2.20/2.31 ($false), % 2.20/2.31 inference(scs_inference,[],[27,20,3,26,103,60,54]), % 2.20/2.31 ['proof']). % 2.20/2.31 % SZS output end Proof % 2.20/2.31 % Total time :1.810000s %------------------------------------------------------------------------------