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