%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN703-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 : n001.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 1.77s 1.86s % Output : CNFRefutation 1.77s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN703-1 : TPTP v8.2.0. Released v2.5.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n001.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 18:20:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.53/0.57 start to proof:theBenchmark % 1.77/1.85 %------------------------------------------- % 1.77/1.85 % File :CSE---1.7 % 1.77/1.85 % Problem :theBenchmark % 1.77/1.85 % Transform :cnf % 1.77/1.85 % Format :tptp:raw % 1.77/1.85 % Command :java -jar mcs_scs.jar %d %s % 1.77/1.85 % 1.77/1.85 % Result :Theorem 1.230000s % 1.77/1.85 % Output :CNFRefutation 1.230000s % 1.77/1.85 %------------------------------------------- % 1.77/1.85 %-------------------------------------------------------------------------- % 1.77/1.85 % File : SYN703-1 : TPTP v8.2.0. Released v2.5.0. % 1.77/1.85 % Domain : Syntactic % 1.77/1.85 % Problem : Harrison problem 4673 % 1.77/1.85 % Version : Especial. % 1.77/1.85 % English : % 1.77/1.85 % 1.77/1.85 % Refs : [Har01] Email to G. Sutcliffe % 1.77/1.85 % Source : [Har01] % 1.77/1.85 % Names : % 1.77/1.85 % 1.77/1.85 % Status : Unsatisfiable % 1.77/1.85 % 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 % 1.77/1.85 % Syntax : Number of clauses : 80 ( 29 unt; 0 nHn; 53 RR) % 1.77/1.85 % Number of literals : 178 ( 0 equ; 100 neg) % 1.77/1.85 % Maximal clause size : 4 ( 2 avg) % 1.77/1.85 % Maximal term depth : 8 ( 1 avg) % 1.77/1.85 % Number of predicates : 26 ( 26 usr; 0 prp; 2-2 aty) % 1.77/1.85 % Number of functors : 31 ( 31 usr; 11 con; 0-2 aty) % 1.77/1.85 % Number of variables : 215 ( 10 sgn) % 1.77/1.85 % SPC : CNF_UNS_RFO_NEQ_HRN % 1.77/1.85 % 1.77/1.85 % Comments : % 1.77/1.85 %-------------------------------------------------------------------------- % 1.77/1.85 cnf(p9_1,negated_conjecture, % 1.77/1.85 p9(X161,X161) ). % 1.77/1.85 % 1.77/1.85 cnf(p10_2,negated_conjecture, % 1.77/1.85 p10(X2,X2) ). % 1.77/1.85 % 1.77/1.85 cnf(p12_3,negated_conjecture, % 1.77/1.85 p12(X7,X7) ). % 1.77/1.85 % 1.77/1.85 cnf(p14_4,negated_conjecture, % 1.77/1.85 p14(X10,X10) ). % 1.77/1.85 % 1.77/1.85 cnf(p15_5,negated_conjecture, % 1.77/1.85 p15(X17,X17) ). % 1.77/1.85 % 1.77/1.85 cnf(p17_6,negated_conjecture, % 1.77/1.85 p17(X20,X20) ). % 1.77/1.85 % 1.77/1.85 cnf(p19_7,negated_conjecture, % 1.77/1.85 p19(X23,X23) ). % 1.77/1.85 % 1.77/1.85 cnf(p2_8,negated_conjecture, % 1.77/1.85 p2(X30,X30) ). % 1.77/1.85 % 1.77/1.85 cnf(p21_9,negated_conjecture, % 1.77/1.85 p21(X33,X33) ). % 1.77/1.85 % 1.77/1.85 cnf(p23_10,negated_conjecture, % 1.77/1.85 p23(X40,X40) ). % 1.77/1.85 % 1.77/1.85 cnf(p25_11,negated_conjecture, % 1.77/1.85 p25(X47,X47) ). % 1.77/1.85 % 1.77/1.85 cnf(p27_12,negated_conjecture, % 1.77/1.85 p27(X50,X50) ). % 1.77/1.85 % 1.77/1.85 cnf(p29_13,negated_conjecture, % 1.77/1.85 p29(X62,X62) ). % 1.77/1.85 % 1.77/1.85 cnf(p3_14,negated_conjecture, % 1.77/1.85 p3(X69,X69) ). % 1.77/1.85 % 1.77/1.85 cnf(p31_15,negated_conjecture, % 1.77/1.85 p31(X80,X80) ). % 1.77/1.85 % 1.77/1.85 cnf(p33_16,negated_conjecture, % 1.77/1.85 p33(X87,X87) ). % 1.77/1.85 % 1.77/1.85 cnf(p35_17,negated_conjecture, % 1.77/1.85 p35(X94,X94) ). % 1.77/1.85 % 1.77/1.85 cnf(p37_18,negated_conjecture, % 1.77/1.85 p37(X97,X97) ). % 1.77/1.85 % 1.77/1.85 cnf(p39_19,negated_conjecture, % 1.77/1.85 p39(X104,X104) ). % 1.77/1.85 % 1.77/1.85 cnf(p4_20,negated_conjecture, % 1.77/1.85 p4(X111,X111) ). % 1.77/1.85 % 1.77/1.85 cnf(p41_21,negated_conjecture, % 1.77/1.85 p41(X122,X122) ). % 1.77/1.85 % 1.77/1.85 cnf(p43_22,negated_conjecture, % 1.77/1.85 p43(X129,X129) ). % 1.77/1.85 % 1.77/1.85 cnf(p45_23,negated_conjecture, % 1.77/1.85 p45(X136,X136) ). % 1.77/1.85 % 1.77/1.85 cnf(p6_24,negated_conjecture, % 1.77/1.85 p6(X147,X147) ). % 1.77/1.85 % 1.77/1.85 cnf(p7_25,negated_conjecture, % 1.77/1.85 p7(X154,X154) ). % 1.77/1.85 % 1.77/1.85 cnf(p10_26,negated_conjecture, % 1.77/1.85 ( p10(X0,X1) % 1.77/1.85 | ~ p10(X2,X0) % 1.77/1.85 | ~ p10(X2,X1) ) ). % 1.77/1.85 % 1.77/1.85 cnf(p9_27,negated_conjecture, % 1.77/1.85 ( p9(X162,X163) % 1.77/1.85 | ~ p9(X161,X162) % 1.77/1.85 | ~ p9(X161,X163) ) ). % 1.77/1.85 % 1.77/1.85 cnf(p7_28,negated_conjecture, % 1.77/1.85 ( p7(X155,X156) % 1.77/1.85 | ~ p7(X154,X155) % 1.77/1.85 | ~ p7(X154,X156) ) ). % 1.77/1.85 % 1.77/1.85 cnf(p6_29,negated_conjecture, % 1.77/1.85 ( p6(X148,X149) % 1.77/1.85 | ~ p6(X147,X148) % 1.77/1.85 | ~ p6(X147,X149) ) ). % 1.77/1.85 % 1.77/1.85 cnf(p45_30,negated_conjecture, % 1.77/1.85 ( p45(X137,X138) % 1.77/1.85 | ~ p45(X136,X137) % 1.77/1.85 | ~ p45(X136,X138) ) ). % 1.77/1.85 % 1.77/1.85 cnf(p43_31,negated_conjecture, % 1.77/1.85 ( p43(X130,X131) % 1.77/1.85 | ~ p43(X129,X130) % 1.77/1.85 | ~ p43(X129,X131) ) ). % 1.77/1.85 % 1.77/1.85 cnf(p41_32,negated_conjecture, % 1.77/1.85 ( p41(X123,X124) % 1.77/1.85 | ~ p41(X122,X123) % 1.77/1.85 | ~ p41(X122,X124) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p4_33,negated_conjecture, % 1.77/1.86 ( p4(X112,X113) % 1.77/1.86 | ~ p4(X111,X112) % 1.77/1.86 | ~ p4(X111,X113) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p39_34,negated_conjecture, % 1.77/1.86 ( p39(X105,X106) % 1.77/1.86 | ~ p39(X104,X105) % 1.77/1.86 | ~ p39(X104,X106) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p37_35,negated_conjecture, % 1.77/1.86 ( p37(X98,X99) % 1.77/1.86 | ~ p37(X97,X98) % 1.77/1.86 | ~ p37(X97,X99) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p35_36,negated_conjecture, % 1.77/1.86 ( p35(X95,X96) % 1.77/1.86 | ~ p35(X94,X95) % 1.77/1.86 | ~ p35(X94,X96) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p33_37,negated_conjecture, % 1.77/1.86 ( p33(X88,X89) % 1.77/1.86 | ~ p33(X87,X88) % 1.77/1.86 | ~ p33(X87,X89) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p31_38,negated_conjecture, % 1.77/1.86 ( p31(X81,X82) % 1.77/1.86 | ~ p31(X80,X81) % 1.77/1.86 | ~ p31(X80,X82) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p3_39,negated_conjecture, % 1.77/1.86 ( p3(X70,X71) % 1.77/1.86 | ~ p3(X69,X70) % 1.77/1.86 | ~ p3(X69,X71) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p29_40,negated_conjecture, % 1.77/1.86 ( p29(X63,X64) % 1.77/1.86 | ~ p29(X62,X63) % 1.77/1.86 | ~ p29(X62,X64) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p27_41,negated_conjecture, % 1.77/1.86 ( p27(X51,X52) % 1.77/1.86 | ~ p27(X50,X51) % 1.77/1.86 | ~ p27(X50,X52) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p25_42,negated_conjecture, % 1.77/1.86 ( p25(X48,X49) % 1.77/1.86 | ~ p25(X47,X48) % 1.77/1.86 | ~ p25(X47,X49) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p23_43,negated_conjecture, % 1.77/1.86 ( p23(X41,X42) % 1.77/1.86 | ~ p23(X40,X41) % 1.77/1.86 | ~ p23(X40,X42) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p21_44,negated_conjecture, % 1.77/1.86 ( p21(X34,X35) % 1.77/1.86 | ~ p21(X33,X34) % 1.77/1.86 | ~ p21(X33,X35) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p2_45,negated_conjecture, % 1.77/1.86 ( p2(X31,X32) % 1.77/1.86 | ~ p2(X30,X31) % 1.77/1.86 | ~ p2(X30,X32) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p19_46,negated_conjecture, % 1.77/1.86 ( p19(X24,X25) % 1.77/1.86 | ~ p19(X23,X24) % 1.77/1.86 | ~ p19(X23,X25) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p17_47,negated_conjecture, % 1.77/1.86 ( p17(X21,X22) % 1.77/1.86 | ~ p17(X20,X21) % 1.77/1.86 | ~ p17(X20,X22) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p15_48,negated_conjecture, % 1.77/1.86 ( p15(X18,X19) % 1.77/1.86 | ~ p15(X17,X18) % 1.77/1.86 | ~ p15(X17,X19) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p14_49,negated_conjecture, % 1.77/1.86 ( p14(X11,X12) % 1.77/1.86 | ~ p14(X10,X11) % 1.77/1.86 | ~ p14(X10,X12) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p12_50,negated_conjecture, % 1.77/1.86 ( p12(X8,X9) % 1.77/1.86 | ~ p12(X7,X8) % 1.77/1.86 | ~ p12(X7,X9) ) ). % 1.77/1.86 % 1.77/1.86 cnf(not_p47_51,negated_conjecture, % 1.77/1.86 ~ p47(f5(c48,f8(f11(f13(c49,c50),c51),c52)),c53) ). % 1.77/1.86 % 1.77/1.86 cnf(not_p47_52,negated_conjecture, % 1.77/1.86 ~ p47(f20(f22(f24(f26(c56,X57),X58),X59),X60),X60) ). % 1.77/1.86 % 1.77/1.86 cnf(p47_53,negated_conjecture, % 1.77/1.86 ( p47(X143,X144) % 1.77/1.86 | ~ p4(X146,X143) % 1.77/1.86 | ~ p47(X146,X145) % 1.77/1.86 | ~ p15(X145,X144) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p10_54,negated_conjecture, % 1.77/1.86 ( p10(f30(X3,X4),f30(X5,X6)) % 1.77/1.86 | ~ p15(X4,X6) % 1.77/1.86 | ~ p29(X3,X5) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p9_55,negated_conjecture, % 1.77/1.86 ( p9(f13(X164,X165),f13(X166,X167)) % 1.77/1.86 | ~ p12(X164,X166) % 1.77/1.86 | ~ p4(X165,X167) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p7_56,negated_conjecture, % 1.77/1.86 ( p7(f40(X157,X158),f40(X159,X160)) % 1.77/1.86 | ~ p15(X158,X160) % 1.77/1.86 | ~ p39(X157,X159) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p6_57,negated_conjecture, % 1.77/1.86 ( p6(f11(X150,X151),f11(X152,X153)) % 1.77/1.86 | ~ p10(X151,X153) % 1.77/1.86 | ~ p9(X150,X152) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p43_58,negated_conjecture, % 1.77/1.86 ( p43(f46(X132,X133),f46(X134,X135)) % 1.77/1.86 | ~ p4(X133,X135) % 1.77/1.86 | ~ p45(X132,X134) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p41_59,negated_conjecture, % 1.77/1.86 ( p41(f44(X125,X126),f44(X127,X128)) % 1.77/1.86 | ~ p10(X126,X128) % 1.77/1.86 | ~ p43(X125,X127) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p4_60,negated_conjecture, % 1.77/1.86 ( p4(f5(X118,X119),f5(X120,X121)) % 1.77/1.86 | ~ p2(X118,X120) % 1.77/1.86 | ~ p3(X119,X121) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p4_61,negated_conjecture, % 1.77/1.86 ( p4(f20(X114,X115),f20(X116,X117)) % 1.77/1.86 | ~ p15(X115,X117) % 1.77/1.86 | ~ p19(X114,X116) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p39_62,negated_conjecture, % 1.77/1.86 ( p39(f42(X107,X108),f42(X109,X110)) % 1.77/1.86 | ~ p41(X107,X109) % 1.77/1.86 | ~ p7(X108,X110) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p37_63,negated_conjecture, % 1.77/1.86 ( p37(f38(X100,X101),f38(X102,X103)) % 1.77/1.86 | ~ p15(X101,X103) % 1.77/1.86 | ~ p7(X100,X102) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p33_64,negated_conjecture, % 1.77/1.86 ( p33(f36(X90,X91),f36(X92,X93)) % 1.77/1.86 | ~ p35(X90,X92) % 1.77/1.86 | ~ p4(X91,X93) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p31_65,negated_conjecture, % 1.77/1.86 ( p31(f34(X83,X84),f34(X85,X86)) % 1.77/1.86 | ~ p10(X84,X86) % 1.77/1.86 | ~ p33(X83,X85) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p3_66,negated_conjecture, % 1.77/1.86 ( p3(f8(X76,X77),f8(X78,X79)) % 1.77/1.86 | ~ p6(X76,X78) % 1.77/1.86 | ~ p7(X77,X79) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p3_67,negated_conjecture, % 1.77/1.86 ( p3(f16(X72,X73),f16(X74,X75)) % 1.77/1.86 | ~ p14(X72,X74) % 1.77/1.86 | ~ p15(X73,X75) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p29_68,negated_conjecture, % 1.77/1.86 ( p29(f32(X65,X66),f32(X67,X68)) % 1.77/1.86 | ~ p31(X65,X67) % 1.77/1.86 | ~ p7(X66,X68) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p27_69,negated_conjecture, % 1.77/1.86 ( p27(f28(X53,X54),f28(X55,X56)) % 1.77/1.86 | ~ p10(X53,X55) % 1.77/1.86 | ~ p15(X54,X56) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p23_70,negated_conjecture, % 1.77/1.86 ( p23(f26(X43,X44),f26(X45,X46)) % 1.77/1.86 | ~ p25(X43,X45) % 1.77/1.86 | ~ p4(X44,X46) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p21_71,negated_conjecture, % 1.77/1.86 ( p21(f24(X36,X37),f24(X38,X39)) % 1.77/1.86 | ~ p10(X37,X39) % 1.77/1.86 | ~ p23(X36,X38) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p19_72,negated_conjecture, % 1.77/1.86 ( p19(f22(X26,X27),f22(X28,X29)) % 1.77/1.86 | ~ p21(X26,X28) % 1.77/1.86 | ~ p7(X27,X29) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p14_73,negated_conjecture, % 1.77/1.86 ( p14(f18(X13,X14),f18(X15,X16)) % 1.77/1.86 | ~ p17(X13,X15) % 1.77/1.86 | ~ p3(X14,X16) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p47_74,negated_conjecture, % 1.77/1.86 ( p47(X139,X140) % 1.77/1.86 | ~ p47(f5(c48,f8(f11(f13(c49,X139),X141),X142)),X140) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p47_75,negated_conjecture, % 1.77/1.86 ( p47(X57,X61) % 1.77/1.86 | ~ p47(f20(f22(f24(f26(c56,X57),X58),X59),X60),X61) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p47_76,negated_conjecture, % 1.77/1.86 ( p47(f5(c48,f8(f11(f13(c49,X139),X141),X142)),X140) % 1.77/1.86 | ~ p47(X139,X140) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p47_77,negated_conjecture, % 1.77/1.86 p47(f5(c48,f16(f18(c54,f8(f11(f13(c49,c50),c51),c52)),c55)),c53) ). % 1.77/1.86 % 1.77/1.86 cnf(p27_78,negated_conjecture, % 1.77/1.86 ( p27(f28(f30(f32(f34(f36(c57,X57),X58),X59),X60),X61),f28(X58,X61)) % 1.77/1.86 | ~ p47(f20(f22(f24(f26(c56,X57),X58),X59),X60),X61) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p37_79,negated_conjecture, % 1.77/1.86 ( p37(f38(f40(f42(f44(f46(c58,X57),X58),X59),X60),X61),f38(X59,X61)) % 1.77/1.86 | ~ p47(f20(f22(f24(f26(c56,X57),X58),X59),X60),X61) ) ). % 1.77/1.86 % 1.77/1.86 cnf(p3_80,negated_conjecture, % 1.77/1.86 p3(f16(f18(c54,f8(f11(f13(c49,X57),X58),X59)),X60),f8(f11(f13(c49,f20(f22(f24(f26(c56,X57),X58),X59),X60)),f30(f32(f34(f36(c57,X57),X58),X59),X60)),f40(f42(f44(f46(c58,X57),X58),X59),X60))) ). % 1.77/1.86 % 1.77/1.86 %-------------------------------------------------------------------------- % 1.77/1.86 %------------------------------------------- % 1.77/1.86 % Proof found % 1.77/1.86 % SZS status Theorem for theBenchmark % 1.77/1.86 % SZS output start Proof % 1.77/1.86 %ClaNum:80(EqnAxiom:0) % 1.77/1.86 %VarNum:432(SingletonVarNum:215) % 1.77/1.86 %MaxLitNum:4 % 1.77/1.86 %MaxfuncDepth:6 % 1.77/1.86 %SharedTerms:20 % 1.77/1.86 %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 % 1.77/1.86 %singleGoalClaCount:29 % 1.77/1.86 [28]~P25(f17(a1,f14(f9(f8(a3,a4),a5),a6)),a7) % 1.77/1.86 [26]P25(f17(a1,f16(f15(a2,f14(f9(f8(a3,a4),a5),a6)),a10)),a7) % 1.77/1.86 [1]P1(x11,x11) % 1.77/1.86 [2]P2(x21,x21) % 1.77/1.86 [3]P3(x31,x31) % 1.77/1.86 [4]P4(x41,x41) % 1.77/1.86 [5]P5(x51,x51) % 1.77/1.86 [6]P6(x61,x61) % 1.77/1.86 [7]P7(x71,x71) % 1.77/1.86 [8]P8(x81,x81) % 1.77/1.86 [9]P9(x91,x91) % 1.77/1.86 [10]P10(x101,x101) % 1.77/1.86 [11]P11(x111,x111) % 1.77/1.86 [12]P12(x121,x121) % 1.77/1.86 [13]P13(x131,x131) % 1.77/1.86 [14]P14(x141,x141) % 1.77/1.86 [15]P15(x151,x151) % 1.77/1.86 [16]P16(x161,x161) % 1.77/1.86 [17]P17(x171,x171) % 1.77/1.86 [18]P18(x181,x181) % 1.77/1.86 [19]P19(x191,x191) % 1.77/1.86 [20]P20(x201,x201) % 1.77/1.86 [21]P21(x211,x211) % 1.77/1.86 [22]P22(x221,x221) % 1.77/1.86 [23]P23(x231,x231) % 1.77/1.86 [24]P24(x241,x241) % 1.77/1.86 [25]P26(x251,x251) % 1.77/1.86 [29]~P25(f21(f20(f19(f18(a11,x291),x292),x293),x294),x294) % 1.77/1.86 [27]P14(f16(f15(a2,f14(f9(f8(a3,x271),x272),x273)),x274),f14(f9(f8(a3,f21(f20(f19(f18(a11,x271),x272),x273),x274)),f25(f24(f23(f22(a12,x271),x272),x273),x274)),f30(f29(f28(f27(a13,x271),x272),x273),x274))) % 1.77/1.86 [76]~P25(x761,x764)+P25(f17(a1,f14(f9(f8(a3,x761),x762),x763)),x764) % 1.77/1.86 [77]P25(x771,x772)+~P25(f17(a1,f14(f9(f8(a3,x771),x773),x774)),x772) % 1.77/1.86 [78]P25(x781,x782)+~P25(f21(f20(f19(f18(a11,x781),x783),x784),x785),x782) % 1.77/1.86 [79]~P25(f21(f20(f19(f18(a11,x791),x792),x793),x794),x795)+P12(f26(f25(f24(f23(f22(a12,x791),x792),x793),x794),x795),f26(x792,x795)) % 1.77/1.86 [80]~P25(f21(f20(f19(f18(a11,x801),x802),x803),x804),x805)+P18(f31(f30(f29(f28(f27(a13,x801),x802),x803),x804),x805),f31(x803,x805)) % 1.77/1.86 [30]~P1(x303,x301)+P1(x301,x302)+~P1(x303,x302) % 1.77/1.86 [31]~P2(x313,x311)+P2(x311,x312)+~P2(x313,x312) % 1.77/1.86 [32]~P3(x323,x321)+P3(x321,x322)+~P3(x323,x322) % 1.77/1.86 [33]~P4(x333,x331)+P4(x331,x332)+~P4(x333,x332) % 1.77/1.86 [34]~P5(x343,x341)+P5(x341,x342)+~P5(x343,x342) % 1.77/1.86 [35]~P6(x353,x351)+P6(x351,x352)+~P6(x353,x352) % 1.77/1.86 [36]~P7(x363,x361)+P7(x361,x362)+~P7(x363,x362) % 1.77/1.86 [37]~P8(x373,x371)+P8(x371,x372)+~P8(x373,x372) % 1.77/1.86 [38]~P9(x383,x381)+P9(x381,x382)+~P9(x383,x382) % 1.77/1.86 [39]~P10(x393,x391)+P10(x391,x392)+~P10(x393,x392) % 1.77/1.86 [40]~P11(x403,x401)+P11(x401,x402)+~P11(x403,x402) % 1.77/1.86 [41]~P12(x413,x411)+P12(x411,x412)+~P12(x413,x412) % 1.77/1.87 [42]~P13(x423,x421)+P13(x421,x422)+~P13(x423,x422) % 1.77/1.87 [43]~P14(x433,x431)+P14(x431,x432)+~P14(x433,x432) % 1.77/1.87 [44]~P15(x443,x441)+P15(x441,x442)+~P15(x443,x442) % 1.77/1.87 [45]~P16(x453,x451)+P16(x451,x452)+~P16(x453,x452) % 1.77/1.87 [46]~P17(x463,x461)+P17(x461,x462)+~P17(x463,x462) % 1.77/1.87 [47]~P18(x473,x471)+P18(x471,x472)+~P18(x473,x472) % 1.77/1.87 [48]~P19(x483,x481)+P19(x481,x482)+~P19(x483,x482) % 1.77/1.87 [49]~P20(x493,x491)+P20(x491,x492)+~P20(x493,x492) % 1.77/1.87 [50]~P21(x503,x501)+P21(x501,x502)+~P21(x503,x502) % 1.77/1.87 [51]~P22(x513,x511)+P22(x511,x512)+~P22(x513,x512) % 1.77/1.87 [52]~P23(x523,x521)+P23(x521,x522)+~P23(x523,x522) % 1.77/1.87 [53]~P24(x533,x531)+P24(x531,x532)+~P24(x533,x532) % 1.77/1.87 [54]~P26(x543,x541)+P26(x541,x542)+~P26(x543,x542) % 1.77/1.87 [56]~P3(x561,x563)+~P20(x562,x564)+P1(f8(x561,x562),f8(x563,x564)) % 1.77/1.87 [57]~P5(x572,x574)+~P13(x571,x573)+P2(f25(x571,x572),f25(x573,x574)) % 1.77/1.87 [58]~P6(x581,x583)+~P14(x582,x584)+P4(f15(x581,x582),f15(x583,x584)) % 1.77/1.87 [59]~P9(x591,x593)+~P26(x592,x594)+P7(f20(x591,x592),f20(x593,x594)) % 1.77/1.87 [60]~P2(x602,x604)+~P10(x601,x603)+P9(f19(x601,x602),f19(x603,x604)) % 1.77/1.87 [61]~P11(x611,x613)+~P20(x612,x614)+P10(f18(x611,x612),f18(x613,x614)) % 1.77/1.87 [62]~P2(x621,x623)+~P5(x622,x624)+P12(f26(x621,x622),f26(x623,x624)) % 1.77/1.87 [63]~P15(x631,x633)+~P26(x632,x634)+P13(f24(x631,x632),f24(x633,x634)) % 1.77/1.87 [64]~P24(x641,x643)+~P26(x642,x644)+P14(f14(x641,x642),f14(x643,x644)) % 1.77/1.87 [65]~P4(x651,x653)+~P5(x652,x654)+P14(f16(x651,x652),f16(x653,x654)) % 1.77/1.87 [66]~P2(x662,x664)+~P16(x661,x663)+P15(f23(x661,x662),f23(x663,x664)) % 1.77/1.87 [67]~P17(x671,x673)+~P20(x672,x674)+P16(f22(x671,x672),f22(x673,x674)) % 1.77/1.87 [68]~P5(x682,x684)+~P26(x681,x683)+P18(f31(x681,x682),f31(x683,x684)) % 1.77/1.87 [69]~P21(x691,x693)+~P26(x692,x694)+P19(f29(x691,x692),f29(x693,x694)) % 1.77/1.87 [70]~P8(x701,x703)+~P14(x702,x704)+P20(f17(x701,x702),f17(x703,x704)) % 1.77/1.87 [71]~P5(x712,x714)+~P7(x711,x713)+P20(f21(x711,x712),f21(x713,x714)) % 1.77/1.87 [72]~P2(x722,x724)+~P22(x721,x723)+P21(f28(x721,x722),f28(x723,x724)) % 1.77/1.87 [73]~P20(x732,x734)+~P23(x731,x733)+P22(f27(x731,x732),f27(x733,x734)) % 1.77/1.87 [74]~P1(x741,x743)+~P2(x742,x744)+P24(f9(x741,x742),f9(x743,x744)) % 1.77/1.87 [75]~P5(x752,x754)+~P19(x751,x753)+P26(f30(x751,x752),f30(x753,x754)) % 1.77/1.87 [55]~P25(x554,x553)+P25(x551,x552)+~P5(x553,x552)+~P20(x554,x551) % 1.77/1.87 %EqnAxiom % 1.77/1.87 % 1.77/1.87 %------------------------------------------- % 1.77/1.87 cnf(81,plain, % 1.77/1.87 (~P25(a4,a7)), % 1.77/1.87 inference(scs_inference,[],[28,76])). % 1.77/1.87 cnf(99,plain, % 1.77/1.87 (~P25(f17(a1,f14(f9(f8(a3,f21(f20(f19(f18(a11,a4),x991),x992),x993)),x994),x995)),a7)), % 1.77/1.87 inference(scs_inference,[],[81,77,78])). % 1.77/1.87 cnf(122,plain, % 1.77/1.87 ($false), % 1.77/1.87 inference(scs_inference,[],[27,8,5,26,99,70,55]), % 1.77/1.87 ['proof']). % 1.77/1.87 % SZS output end Proof % 1.77/1.87 % Total time :1.230000s %------------------------------------------------------------------------------