%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN706-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 : n022.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:22 EDT 2024 % Result : Unsatisfiable 1.81s 1.92s % Output : CNFRefutation 1.81s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN706-1 : TPTP v8.2.0. Released v2.5.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n022.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 23:15:54 EDT 2024 % 0.13/0.34 % CPUTime : % 0.63/0.65 start to proof:theBenchmark % 1.81/1.90 %------------------------------------------- % 1.81/1.90 % File :CSE---1.7 % 1.81/1.90 % Problem :theBenchmark % 1.81/1.90 % Transform :cnf % 1.81/1.90 % Format :tptp:raw % 1.81/1.90 % Command :java -jar mcs_scs.jar %d %s % 1.81/1.90 % 1.81/1.90 % Result :Theorem 1.200000s % 1.81/1.90 % Output :CNFRefutation 1.200000s % 1.81/1.90 %------------------------------------------- % 1.81/1.90 %-------------------------------------------------------------------------- % 1.81/1.90 % File : SYN706-1 : TPTP v8.2.0. Released v2.5.0. % 1.81/1.90 % Domain : Syntactic % 1.81/1.90 % Problem : Harrison problem 4685 % 1.81/1.90 % Version : Especial. % 1.81/1.90 % English : % 1.81/1.90 % 1.81/1.90 % Refs : [Har01] Email to G. Sutcliffe % 1.81/1.90 % Source : [Har01] % 1.81/1.90 % Names : % 1.81/1.90 % 1.81/1.90 % Status : Unsatisfiable % 1.81/1.90 % 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.08 v5.1.0, 0.06 v5.0.0, 0.07 v4.0.1, 0.14 v3.7.0, 0.00 v2.5.0 % 1.81/1.90 % Syntax : Number of clauses : 81 ( 31 unt; 0 nHn; 51 RR) % 1.81/1.90 % Number of literals : 182 ( 0 equ; 103 neg) % 1.81/1.90 % Maximal clause size : 4 ( 2 avg) % 1.81/1.90 % Maximal term depth : 6 ( 1 avg) % 1.81/1.90 % Number of predicates : 30 ( 30 usr; 0 prp; 2-2 aty) % 1.81/1.90 % Number of functors : 31 ( 31 usr; 14 con; 0-2 aty) % 1.81/1.90 % Number of variables : 199 ( 2 sgn) % 1.81/1.90 % SPC : CNF_UNS_RFO_NEQ_HRN % 1.81/1.90 % 1.81/1.90 % Comments : % 1.81/1.90 %-------------------------------------------------------------------------- % 1.81/1.90 cnf(p10_1,negated_conjecture, % 1.81/1.90 p10(X0,X0) ). % 1.81/1.90 % 1.81/1.90 cnf(p9_2,negated_conjecture, % 1.81/1.90 p9(X168,X168) ). % 1.81/1.90 % 1.81/1.90 cnf(p7_3,negated_conjecture, % 1.81/1.90 p7(X159,X159) ). % 1.81/1.90 % 1.81/1.90 cnf(p6_4,negated_conjecture, % 1.81/1.90 p6(X152,X152) ). % 1.81/1.90 % 1.81/1.90 cnf(p47_5,negated_conjecture, % 1.81/1.90 p47(X143,X143) ). % 1.81/1.90 % 1.81/1.90 cnf(p43_6,negated_conjecture, % 1.81/1.90 p43(X125,X125) ). % 1.81/1.90 % 1.81/1.90 cnf(p41_7,negated_conjecture, % 1.81/1.90 p41(X118,X118) ). % 1.81/1.90 % 1.81/1.90 cnf(p4_8,negated_conjecture, % 1.81/1.90 p4(X105,X105) ). % 1.81/1.90 % 1.81/1.90 cnf(p39_9,negated_conjecture, % 1.81/1.90 p39(X102,X102) ). % 1.81/1.90 % 1.81/1.90 cnf(p37_10,negated_conjecture, % 1.81/1.90 p37(X95,X95) ). % 1.81/1.90 % 1.81/1.90 cnf(p36_11,negated_conjecture, % 1.81/1.90 p36(X88,X88) ). % 1.81/1.90 % 1.81/1.90 cnf(p33_12,negated_conjecture, % 1.81/1.90 p33(X85,X85) ). % 1.81/1.90 % 1.81/1.90 cnf(p3_13,negated_conjecture, % 1.81/1.90 p3(X78,X78) ). % 1.81/1.90 % 1.81/1.90 cnf(p29_14,negated_conjecture, % 1.81/1.90 p29(X71,X71) ). % 1.81/1.90 % 1.81/1.90 cnf(p27_15,negated_conjecture, % 1.81/1.90 p27(X64,X64) ). % 1.81/1.90 % 1.81/1.90 cnf(p26_16,negated_conjecture, % 1.81/1.90 p26(X61,X61) ). % 1.81/1.90 % 1.81/1.90 cnf(p24_17,negated_conjecture, % 1.81/1.90 p24(X54,X54) ). % 1.81/1.90 % 1.81/1.91 cnf(p22_18,negated_conjecture, % 1.81/1.91 p22(X47,X47) ). % 1.81/1.91 % 1.81/1.91 cnf(p21_19,negated_conjecture, % 1.81/1.91 p21(X44,X44) ). % 1.81/1.91 % 1.81/1.91 cnf(p2_20,negated_conjecture, % 1.81/1.91 p2(X41,X41) ). % 1.81/1.91 % 1.81/1.91 cnf(p19_21,negated_conjecture, % 1.81/1.91 p19(X34,X34) ). % 1.81/1.91 % 1.81/1.91 cnf(p18_22,negated_conjecture, % 1.81/1.91 p18(X31,X31) ). % 1.81/1.91 % 1.81/1.91 cnf(p16_23,negated_conjecture, % 1.81/1.91 p16(X24,X24) ). % 1.81/1.91 % 1.81/1.91 cnf(p15_24,negated_conjecture, % 1.81/1.91 p15(X21,X21) ). % 1.81/1.91 % 1.81/1.91 cnf(p13_25,negated_conjecture, % 1.81/1.91 p13(X14,X14) ). % 1.81/1.91 % 1.81/1.91 cnf(p12_26,negated_conjecture, % 1.81/1.91 p12(X7,X7) ). % 1.81/1.91 % 1.81/1.91 cnf(p45_27,negated_conjecture, % 1.81/1.91 p45(f20(c52,c50),c58) ). % 1.81/1.91 % 1.81/1.91 cnf(not_p4_28,negated_conjecture, % 1.81/1.91 ~ p4(f5(c49,c50),c51) ). % 1.81/1.91 % 1.81/1.91 cnf(not_p48_29,negated_conjecture, % 1.81/1.91 ~ p48(f38(f40(c59,c50),c58),c60) ). % 1.81/1.91 % 1.81/1.91 cnf(p10_30,negated_conjecture, % 1.81/1.91 ( p10(X1,X2) % 1.81/1.91 | ~ p10(X0,X1) % 1.81/1.91 | ~ p10(X0,X2) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p9_31,negated_conjecture, % 1.81/1.91 ( p9(X169,X170) % 1.81/1.91 | ~ p9(X168,X170) % 1.81/1.91 | ~ p9(X168,X169) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p7_32,negated_conjecture, % 1.81/1.91 ( p7(X160,X161) % 1.81/1.91 | ~ p7(X159,X160) % 1.81/1.91 | ~ p7(X159,X161) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p6_33,negated_conjecture, % 1.81/1.91 ( p6(X153,X154) % 1.81/1.91 | ~ p6(X152,X153) % 1.81/1.91 | ~ p6(X152,X154) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p47_34,negated_conjecture, % 1.81/1.91 ( p47(X144,X145) % 1.81/1.91 | ~ p47(X143,X144) % 1.81/1.91 | ~ p47(X143,X145) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p43_35,negated_conjecture, % 1.81/1.91 ( p43(X126,X127) % 1.81/1.91 | ~ p43(X125,X126) % 1.81/1.91 | ~ p43(X125,X127) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p41_36,negated_conjecture, % 1.81/1.91 ( p41(X119,X120) % 1.81/1.91 | ~ p41(X118,X119) % 1.81/1.91 | ~ p41(X118,X120) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p4_37,negated_conjecture, % 1.81/1.91 ( p4(X106,X107) % 1.81/1.91 | ~ p4(X105,X106) % 1.81/1.91 | ~ p4(X105,X107) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p39_38,negated_conjecture, % 1.81/1.91 ( p39(X103,X104) % 1.81/1.91 | ~ p39(X102,X103) % 1.81/1.91 | ~ p39(X102,X104) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p37_39,negated_conjecture, % 1.81/1.91 ( p37(X96,X97) % 1.81/1.91 | ~ p37(X95,X96) % 1.81/1.91 | ~ p37(X95,X97) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p36_40,negated_conjecture, % 1.81/1.91 ( p36(X89,X90) % 1.81/1.91 | ~ p36(X88,X89) % 1.81/1.91 | ~ p36(X88,X90) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p33_41,negated_conjecture, % 1.81/1.91 ( p33(X86,X87) % 1.81/1.91 | ~ p33(X85,X86) % 1.81/1.91 | ~ p33(X85,X87) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p3_42,negated_conjecture, % 1.81/1.91 ( p3(X79,X80) % 1.81/1.91 | ~ p3(X78,X79) % 1.81/1.91 | ~ p3(X78,X80) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p29_43,negated_conjecture, % 1.81/1.91 ( p29(X72,X73) % 1.81/1.91 | ~ p29(X71,X72) % 1.81/1.91 | ~ p29(X71,X73) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p27_44,negated_conjecture, % 1.81/1.91 ( p27(X65,X66) % 1.81/1.91 | ~ p27(X64,X65) % 1.81/1.91 | ~ p27(X64,X66) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p26_45,negated_conjecture, % 1.81/1.91 ( p26(X62,X63) % 1.81/1.91 | ~ p26(X61,X62) % 1.81/1.91 | ~ p26(X61,X63) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p24_46,negated_conjecture, % 1.81/1.91 ( p24(X55,X56) % 1.81/1.91 | ~ p24(X54,X55) % 1.81/1.91 | ~ p24(X54,X56) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p22_47,negated_conjecture, % 1.81/1.91 ( p22(X48,X49) % 1.81/1.91 | ~ p22(X47,X48) % 1.81/1.91 | ~ p22(X47,X49) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p21_48,negated_conjecture, % 1.81/1.91 ( p21(X45,X46) % 1.81/1.91 | ~ p21(X44,X45) % 1.81/1.91 | ~ p21(X44,X46) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p2_49,negated_conjecture, % 1.81/1.91 ( p2(X42,X43) % 1.81/1.91 | ~ p2(X41,X42) % 1.81/1.91 | ~ p2(X41,X43) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p19_50,negated_conjecture, % 1.81/1.91 ( p19(X35,X36) % 1.81/1.91 | ~ p19(X34,X35) % 1.81/1.91 | ~ p19(X34,X36) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p18_51,negated_conjecture, % 1.81/1.91 ( p18(X32,X33) % 1.81/1.91 | ~ p18(X31,X32) % 1.81/1.91 | ~ p18(X31,X33) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p16_52,negated_conjecture, % 1.81/1.91 ( p16(X25,X26) % 1.81/1.91 | ~ p16(X24,X25) % 1.81/1.91 | ~ p16(X24,X26) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p15_53,negated_conjecture, % 1.81/1.91 ( p15(X22,X23) % 1.81/1.91 | ~ p15(X21,X22) % 1.81/1.91 | ~ p15(X21,X23) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p13_54,negated_conjecture, % 1.81/1.91 ( p13(X15,X16) % 1.81/1.91 | ~ p13(X14,X15) % 1.81/1.91 | ~ p13(X14,X16) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p12_55,negated_conjecture, % 1.81/1.91 ( p12(X8,X9) % 1.81/1.91 | ~ p12(X7,X8) % 1.81/1.91 | ~ p12(X7,X9) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p45_56,negated_conjecture, % 1.81/1.91 ( p45(X128,X129) % 1.81/1.91 | ~ p45(X130,X131) % 1.81/1.91 | ~ p7(X131,X129) % 1.81/1.91 | ~ p19(X130,X128) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p48_57,negated_conjecture, % 1.81/1.91 ( p48(X146,X147) % 1.81/1.91 | ~ p47(X149,X147) % 1.81/1.91 | ~ p48(X148,X149) % 1.81/1.91 | ~ p37(X148,X146) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p46_58,negated_conjecture, % 1.81/1.91 ( p46(X138,X139) % 1.81/1.91 | ~ p4(X141,X139) % 1.81/1.91 | ~ p46(X140,X141) % 1.81/1.91 | ~ p22(X140,X138) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p7_59,negated_conjecture, % 1.81/1.91 p7(f8(f11(c54,f14(f17(c55,X166),f35(X167,X166))),X167),X167) ). % 1.81/1.91 % 1.81/1.91 cnf(p4_60,negated_conjecture, % 1.81/1.91 p4(f25(f28(c56,f31(f34(c57,X112),f32(X113,X112))),X113),X113) ). % 1.81/1.91 % 1.81/1.91 cnf(p10_61,negated_conjecture, % 1.81/1.91 ( p10(f14(X3,X4),f14(X5,X6)) % 1.81/1.91 | ~ p12(X3,X5) % 1.81/1.91 | ~ p13(X4,X6) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p7_62,negated_conjecture, % 1.81/1.91 ( p7(f8(X162,X163),f8(X164,X165)) % 1.81/1.91 | ~ p6(X162,X164) % 1.81/1.91 | ~ p7(X163,X165) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p6_63,negated_conjecture, % 1.81/1.91 ( p6(f11(X155,X156),f11(X157,X158)) % 1.81/1.91 | ~ p10(X156,X158) % 1.81/1.91 | ~ p9(X155,X157) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p41_64,negated_conjecture, % 1.81/1.91 ( p41(f44(X121,X122),f44(X123,X124)) % 1.81/1.91 | ~ p43(X121,X123) % 1.81/1.91 | ~ p7(X122,X124) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p4_65,negated_conjecture, % 1.81/1.91 ( p4(f5(X114,X115),f5(X116,X117)) % 1.81/1.91 | ~ p2(X114,X116) % 1.81/1.91 | ~ p3(X115,X117) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p4_66,negated_conjecture, % 1.81/1.91 ( p4(f25(X108,X109),f25(X110,X111)) % 1.81/1.91 | ~ p24(X108,X110) % 1.81/1.91 | ~ p4(X109,X111) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p37_67,negated_conjecture, % 1.81/1.91 ( p37(f38(X98,X99),f38(X100,X101)) % 1.81/1.91 | ~ p36(X98,X100) % 1.81/1.91 | ~ p7(X99,X101) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p36_68,negated_conjecture, % 1.81/1.91 ( p36(f40(X91,X92),f40(X93,X94)) % 1.81/1.91 | ~ p3(X92,X94) % 1.81/1.91 | ~ p39(X91,X93) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p30_69,negated_conjecture, % 1.81/1.91 ( p30(f32(X81,X82),f32(X83,X84)) % 1.81/1.91 | ~ p13(X82,X84) % 1.81/1.91 | ~ p4(X81,X83) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p29_70,negated_conjecture, % 1.81/1.91 ( p29(f34(X74,X75),f34(X76,X77)) % 1.81/1.91 | ~ p13(X75,X77) % 1.81/1.91 | ~ p33(X74,X76) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p27_71,negated_conjecture, % 1.81/1.91 ( p27(f31(X67,X68),f31(X69,X70)) % 1.81/1.91 | ~ p29(X67,X69) % 1.81/1.91 | ~ p30(X68,X70) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p24_72,negated_conjecture, % 1.81/1.91 ( p24(f28(X57,X58),f28(X59,X60)) % 1.81/1.91 | ~ p26(X57,X59) % 1.81/1.91 | ~ p27(X58,X60) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p22_73,negated_conjecture, % 1.81/1.91 ( p22(f23(X50,X51),f23(X52,X53)) % 1.81/1.91 | ~ p13(X51,X53) % 1.81/1.91 | ~ p21(X50,X52) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p19_74,negated_conjecture, % 1.81/1.91 ( p19(f20(X37,X38),f20(X39,X40)) % 1.81/1.91 | ~ p18(X37,X39) % 1.81/1.91 | ~ p3(X38,X40) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p16_75,negated_conjecture, % 1.81/1.91 ( p16(f42(X27,X28),f42(X29,X30)) % 1.81/1.91 | ~ p3(X28,X30) % 1.81/1.91 | ~ p41(X27,X29) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p13_76,negated_conjecture, % 1.81/1.91 ( p13(f35(X17,X18),f35(X19,X20)) % 1.81/1.91 | ~ p16(X18,X20) % 1.81/1.91 | ~ p7(X17,X19) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p12_77,negated_conjecture, % 1.81/1.91 ( p12(f17(X10,X11),f17(X12,X13)) % 1.81/1.91 | ~ p15(X10,X12) % 1.81/1.91 | ~ p16(X11,X13) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p46_78,negated_conjecture, % 1.81/1.91 ( p46(f23(c53,f35(X137,X142)),f5(c49,X136)) % 1.81/1.91 | ~ p45(f20(c52,X136),X137) ) ). % 1.81/1.91 % 1.81/1.91 cnf(p45_79,negated_conjecture, % 1.81/1.91 ( p45(f20(c52,X136),X137) % 1.81/1.92 | ~ p46(f23(c53,f35(X137,f42(f44(c62,X137),X136))),f5(c49,X136)) ) ). % 1.81/1.92 % 1.81/1.92 cnf(p45_80,negated_conjecture, % 1.81/1.92 ( p45(f20(c52,X132),f8(f11(c54,f14(f17(c55,X133),X134)),X135)) % 1.81/1.92 | ~ p45(f20(c52,X132),X135) % 1.81/1.92 | ~ p46(f23(c53,X134),f5(c49,X132)) ) ). % 1.81/1.92 % 1.81/1.92 cnf(p48_81,negated_conjecture, % 1.81/1.92 ( p48(f38(f40(c59,c50),f8(f11(c54,f14(f17(c55,c61),X150)),X151)),c60) % 1.81/1.92 | ~ p45(f20(c52,c50),X151) % 1.81/1.92 | ~ p46(f23(c53,X150),f5(c49,c50)) ) ). % 1.81/1.92 % 1.81/1.92 %-------------------------------------------------------------------------- % 1.81/1.92 %------------------------------------------- % 1.81/1.92 % Proof found % 1.81/1.92 % SZS status Theorem for theBenchmark % 1.81/1.92 % SZS output start Proof % 1.81/1.92 %ClaNum:81(EqnAxiom:0) % 1.81/1.92 %VarNum:401(SingletonVarNum:199) % 1.81/1.92 %MaxLitNum:4 % 1.81/1.92 %MaxfuncDepth:5 % 1.81/1.92 %SharedTerms:22 % 1.81/1.92 %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 % 1.81/1.92 %singleGoalClaCount:31 % 1.81/1.92 [27]P28(f5(a1,a2),a6) % 1.81/1.92 [30]~P8(f27(a3,a2),a4) % 1.81/1.92 [31]~P30(f29(f28(a15,a2),a6),a16) % 1.81/1.92 [1]P1(x11,x11) % 1.81/1.92 [2]P2(x21,x21) % 1.81/1.92 [3]P3(x31,x31) % 1.81/1.92 [4]P4(x41,x41) % 1.81/1.92 [5]P5(x51,x51) % 1.81/1.92 [6]P6(x61,x61) % 1.81/1.92 [7]P7(x71,x71) % 1.81/1.92 [8]P8(x81,x81) % 1.81/1.92 [9]P9(x91,x91) % 1.81/1.92 [10]P10(x101,x101) % 1.81/1.92 [11]P11(x111,x111) % 1.81/1.92 [12]P12(x121,x121) % 1.81/1.92 [13]P13(x131,x131) % 1.81/1.92 [14]P14(x141,x141) % 1.81/1.92 [15]P15(x151,x151) % 1.81/1.92 [16]P16(x161,x161) % 1.81/1.92 [17]P17(x171,x171) % 1.81/1.92 [18]P18(x181,x181) % 1.81/1.92 [19]P19(x191,x191) % 1.81/1.92 [20]P20(x201,x201) % 1.81/1.92 [21]P21(x211,x211) % 1.81/1.92 [22]P22(x221,x221) % 1.81/1.92 [23]P23(x231,x231) % 1.81/1.92 [24]P24(x241,x241) % 1.81/1.92 [25]P25(x251,x251) % 1.81/1.92 [26]P26(x261,x261) % 1.81/1.92 [28]P3(f26(f14(a7,f13(f12(a9,x281),f19(x282,x281))),x282),x282) % 1.81/1.92 [29]P8(f24(f23(a10,f22(f20(a11,x291),f21(x292,x291))),x292),x292) % 1.81/1.92 [80]P28(f5(a1,x801),x802)+~P29(f25(a8,f19(x802,f31(f30(a17,x802),x801))),f27(a3,x801)) % 1.81/1.92 [78]~P28(f5(a1,x783),x781)+P29(f25(a8,f19(x781,x782)),f27(a3,x783)) % 1.81/1.92 [81]~P28(f5(a1,a2),x812)+~P29(f25(a8,x811),f27(a3,a2))+P30(f29(f28(a15,a2),f26(f14(a7,f13(f12(a9,a18),x811)),x812)),a16) % 1.81/1.92 [32]~P1(x323,x321)+P1(x321,x322)+~P1(x323,x322) % 1.81/1.92 [33]~P2(x333,x331)+P2(x331,x332)+~P2(x333,x332) % 1.81/1.92 [34]~P3(x343,x341)+P3(x341,x342)+~P3(x343,x342) % 1.81/1.92 [35]~P4(x353,x351)+P4(x351,x352)+~P4(x353,x352) % 1.81/1.92 [36]~P5(x363,x361)+P5(x361,x362)+~P5(x363,x362) % 1.81/1.92 [37]~P6(x373,x371)+P6(x371,x372)+~P6(x373,x372) % 1.81/1.92 [38]~P7(x383,x381)+P7(x381,x382)+~P7(x383,x382) % 1.81/1.92 [39]~P8(x393,x391)+P8(x391,x392)+~P8(x393,x392) % 1.81/1.92 [40]~P9(x403,x401)+P9(x401,x402)+~P9(x403,x402) % 1.81/1.92 [41]~P10(x413,x411)+P10(x411,x412)+~P10(x413,x412) % 1.81/1.92 [42]~P11(x423,x421)+P11(x421,x422)+~P11(x423,x422) % 1.81/1.92 [43]~P12(x433,x431)+P12(x431,x432)+~P12(x433,x432) % 1.81/1.92 [44]~P13(x443,x441)+P13(x441,x442)+~P13(x443,x442) % 1.81/1.92 [45]~P14(x453,x451)+P14(x451,x452)+~P14(x453,x452) % 1.81/1.92 [46]~P15(x463,x461)+P15(x461,x462)+~P15(x463,x462) % 1.81/1.92 [47]~P16(x473,x471)+P16(x471,x472)+~P16(x473,x472) % 1.81/1.92 [48]~P17(x483,x481)+P17(x481,x482)+~P17(x483,x482) % 1.81/1.92 [49]~P18(x493,x491)+P18(x491,x492)+~P18(x493,x492) % 1.81/1.92 [50]~P19(x503,x501)+P19(x501,x502)+~P19(x503,x502) % 1.81/1.92 [51]~P20(x513,x511)+P20(x511,x512)+~P20(x513,x512) % 1.81/1.92 [52]~P21(x523,x521)+P21(x521,x522)+~P21(x523,x522) % 1.81/1.92 [53]~P22(x533,x531)+P22(x531,x532)+~P22(x533,x532) % 1.81/1.92 [54]~P23(x543,x541)+P23(x541,x542)+~P23(x543,x542) % 1.81/1.92 [55]~P24(x553,x551)+P24(x551,x552)+~P24(x553,x552) % 1.81/1.92 [56]~P25(x563,x561)+P25(x561,x562)+~P25(x563,x562) % 1.81/1.92 [57]~P26(x573,x571)+P26(x571,x572)+~P26(x573,x572) % 1.81/1.92 [61]~P25(x612,x614)+~P26(x611,x613)+P1(f13(x611,x612),f13(x613,x614)) % 1.81/1.92 [62]~P3(x622,x624)+~P4(x621,x623)+P3(f26(x621,x622),f26(x623,x624)) % 1.81/1.92 [63]~P1(x632,x634)+~P2(x631,x633)+P4(f14(x631,x632),f14(x633,x634)) % 1.81/1.92 [64]~P3(x642,x644)+~P6(x641,x643)+P7(f30(x641,x642),f30(x643,x644)) % 1.81/1.92 [65]~P13(x652,x654)+~P20(x651,x653)+P8(f27(x651,x652),f27(x653,x654)) % 1.81/1.92 [66]~P8(x662,x664)+~P17(x661,x663)+P8(f24(x661,x662),f24(x663,x664)) % 1.81/1.92 [67]~P3(x672,x674)+~P11(x671,x673)+P10(f29(x671,x672),f29(x673,x674)) % 1.81/1.92 [68]~P9(x681,x683)+~P13(x682,x684)+P11(f28(x681,x682),f28(x683,x684)) % 1.81/1.92 [69]~P12(x691,x693)+~P25(x692,x694)+P14(f20(x691,x692),f20(x693,x694)) % 1.81/1.92 [70]~P14(x701,x703)+~P27(x702,x704)+P15(f22(x701,x702),f22(x703,x704)) % 1.81/1.92 [71]~P15(x712,x714)+~P16(x711,x713)+P17(f23(x711,x712),f23(x713,x714)) % 1.81/1.92 [72]~P19(x721,x723)+~P25(x722,x724)+P18(f25(x721,x722),f25(x723,x724)) % 1.81/1.92 [73]~P13(x732,x734)+~P22(x731,x733)+P21(f5(x731,x732),f5(x733,x734)) % 1.81/1.92 [74]~P7(x741,x743)+~P13(x742,x744)+P23(f31(x741,x742),f31(x743,x744)) % 1.81/1.92 [75]~P3(x751,x753)+~P23(x752,x754)+P25(f19(x751,x752),f19(x753,x754)) % 1.81/1.92 [76]~P23(x762,x764)+~P24(x761,x763)+P26(f12(x761,x762),f12(x763,x764)) % 1.81/1.92 [77]~P8(x771,x773)+~P25(x772,x774)+P27(f21(x771,x772),f21(x773,x774)) % 1.81/1.92 [79]~P28(f5(a1,x791),x794)+~P29(f25(a8,x793),f27(a3,x791))+P28(f5(a1,x791),f26(f14(a7,f13(f12(a9,x792),x793)),x794)) % 1.81/1.92 [58]~P28(x584,x583)+P28(x581,x582)+~P3(x583,x582)+~P21(x584,x581) % 1.81/1.92 [59]~P30(x594,x593)+P30(x591,x592)+~P5(x593,x592)+~P10(x594,x591) % 1.81/1.92 [60]~P29(x604,x603)+P29(x601,x602)+~P8(x603,x602)+~P18(x604,x601) % 1.81/1.92 %EqnAxiom % 1.81/1.92 % 1.81/1.92 %------------------------------------------- % 1.81/1.92 cnf(82,plain, % 1.81/1.92 (~P28(x821,f26(f14(a7,f13(f12(a9,x822),f19(x823,x822))),x823))+P28(x821,x823)), % 1.81/1.92 inference(scs_inference,[],[21,28,58])). % 1.81/1.92 cnf(91,plain, % 1.81/1.92 (P3(x911,f26(f14(a7,f13(f12(a9,x912),f19(x911,x912))),x911))), % 1.81/1.92 inference(scs_inference,[],[28,3,34])). % 1.81/1.92 cnf(97,plain, % 1.81/1.92 (P28(f5(a1,a2),f26(f14(a7,f13(f12(a9,x971),f19(a6,x971))),a6))), % 1.81/1.92 inference(scs_inference,[],[91,27,21,58])). % 1.81/1.92 cnf(101,plain, % 1.81/1.92 (P29(f25(a8,f19(a6,x1011)),f27(a3,a2))), % 1.81/1.92 inference(scs_inference,[],[97,82,78])). % 1.81/1.92 cnf(141,plain, % 1.81/1.92 (P28(f5(a1,a2),f26(f14(a7,f13(f12(a9,x1411),f19(a6,x1412))),a6))), % 1.81/1.92 inference(scs_inference,[],[97,101,82,79])). % 1.81/1.92 cnf(142,plain, % 1.81/1.92 (P30(f29(f28(a15,a2),f26(f14(a7,f13(f12(a9,a18),f19(a6,x1421))),a6)),a16)), % 1.81/1.92 inference(scs_inference,[],[141,101,82,81])). % 1.81/1.92 cnf(227,plain, % 1.81/1.92 (P10(f29(x2271,f26(f14(a7,f13(f12(a9,x2272),f19(x2273,x2272))),x2273)),f29(x2271,x2273))), % 1.81/1.92 inference(scs_inference,[],[28,11,67,42])). % 1.81/1.92 cnf(231,plain, % 1.81/1.92 ($false), % 1.81/1.92 inference(scs_inference,[],[227,142,5,10,31,41,59]), % 1.81/1.92 ['proof']). % 1.81/1.92 % SZS output end Proof % 1.81/1.92 % Total time :1.200000s %------------------------------------------------------------------------------