%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN691-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 : n020.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:19 EDT 2024 % Result : Unsatisfiable 58.39s 58.44s % Output : CNFRefutation 58.39s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.13 % Problem : SYN691-1 : TPTP v8.2.0. Released v2.5.0. % 0.12/0.13 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n020.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 18:47:39 EDT 2024 % 0.13/0.34 % CPUTime : % 0.55/0.57 start to proof:theBenchmark % 58.39/58.41 %------------------------------------------- % 58.39/58.41 % File :CSE---1.7 % 58.39/58.41 % Problem :theBenchmark % 58.39/58.41 % Transform :cnf % 58.39/58.41 % Format :tptp:raw % 58.39/58.41 % Command :java -jar mcs_scs.jar %d %s % 58.39/58.41 % 58.39/58.41 % Result :Theorem 57.800000s % 58.39/58.41 % Output :CNFRefutation 57.800000s % 58.39/58.41 %------------------------------------------- % 58.39/58.43 %-------------------------------------------------------------------------- % 58.39/58.43 % File : SYN691-1 : TPTP v8.2.0. Released v2.5.0. % 58.39/58.43 % Domain : Syntactic % 58.39/58.43 % Problem : Harrison problem 4624 % 58.39/58.43 % Version : Especial. % 58.39/58.43 % English : % 58.39/58.43 % 58.39/58.43 % Refs : [Har01] Email to G. Sutcliffe % 58.39/58.43 % Source : [Har01] % 58.39/58.43 % Names : % 58.39/58.43 % 58.39/58.43 % Status : Unsatisfiable % 58.39/58.43 % Rating : 0.00 v5.4.0, 0.06 v5.3.0, 0.15 v5.2.0, 0.00 v2.5.0 % 58.39/58.43 % Syntax : Number of clauses : 67 ( 24 unt; 0 nHn; 44 RR) % 58.39/58.43 % Number of literals : 149 ( 0 equ; 83 neg) % 58.39/58.43 % Maximal clause size : 4 ( 2 avg) % 58.39/58.43 % Maximal term depth : 7 ( 1 avg) % 58.39/58.43 % Number of predicates : 22 ( 22 usr; 0 prp; 2-2 aty) % 58.39/58.43 % Number of functors : 26 ( 26 usr; 10 con; 0-2 aty) % 58.39/58.43 % Number of variables : 175 ( 6 sgn) % 58.39/58.43 % SPC : CNF_UNS_RFO_NEQ_HRN % 58.39/58.43 % 58.39/58.43 % Comments : % 58.39/58.43 %-------------------------------------------------------------------------- % 58.39/58.43 cnf(p11_1,negated_conjecture, % 58.39/58.43 p11(X0,X0) ). % 58.39/58.43 % 58.39/58.43 cnf(p9_2,negated_conjecture, % 58.39/58.43 p9(X132,X132) ). % 58.39/58.43 % 58.39/58.43 cnf(p8_3,negated_conjecture, % 58.39/58.43 p8(X125,X125) ). % 58.39/58.43 % 58.39/58.43 cnf(p6_4,negated_conjecture, % 58.39/58.43 p6(X122,X122) ). % 58.39/58.43 % 58.39/58.43 cnf(p4_5,negated_conjecture, % 58.39/58.43 p4(X111,X111) ). % 58.39/58.43 % 58.39/58.43 cnf(p37_6,negated_conjecture, % 58.39/58.43 p37(X100,X100) ). % 58.39/58.43 % 58.39/58.43 cnf(p35_7,negated_conjecture, % 58.39/58.43 p35(X93,X93) ). % 58.39/58.43 % 58.39/58.43 cnf(p33_8,negated_conjecture, % 58.39/58.43 p33(X86,X86) ). % 58.39/58.43 % 58.39/58.43 cnf(p31_9,negated_conjecture, % 58.39/58.43 p31(X79,X79) ). % 58.39/58.43 % 58.39/58.43 cnf(p3_10,negated_conjecture, % 58.39/58.43 p3(X68,X68) ). % 58.39/58.43 % 58.39/58.43 cnf(p29_11,negated_conjecture, % 58.39/58.43 p29(X65,X65) ). % 58.39/58.43 % 58.39/58.43 cnf(p27_12,negated_conjecture, % 58.39/58.43 p27(X58,X58) ). % 58.39/58.43 % 58.39/58.43 cnf(p25_13,negated_conjecture, % 58.39/58.43 p25(X51,X51) ). % 58.39/58.43 % 58.39/58.43 cnf(p23_14,negated_conjecture, % 58.39/58.43 p23(X40,X40) ). % 58.39/58.43 % 58.39/58.43 cnf(p22_15,negated_conjecture, % 58.39/58.43 p22(X37,X37) ). % 58.39/58.43 % 58.39/58.43 cnf(p20_16,negated_conjecture, % 58.39/58.43 p20(X34,X34) ). % 58.39/58.43 % 58.39/58.43 cnf(p2_17,negated_conjecture, % 58.39/58.43 p2(X31,X31) ). % 58.39/58.43 % 58.39/58.43 cnf(p18_18,negated_conjecture, % 58.39/58.43 p18(X24,X24) ). % 58.39/58.43 % 58.39/58.43 cnf(p16_19,negated_conjecture, % 58.39/58.43 p16(X17,X17) ). % 58.39/58.43 % 58.39/58.43 cnf(p14_20,negated_conjecture, % 58.39/58.43 p14(X14,X14) ). % 58.39/58.43 % 58.39/58.43 cnf(p12_21,negated_conjecture, % 58.39/58.43 p12(X7,X7) ). % 58.39/58.43 % 58.39/58.43 cnf(p11_22,negated_conjecture, % 58.39/58.43 ( p11(X1,X2) % 58.39/58.43 | ~ p11(X0,X1) % 58.39/58.43 | ~ p11(X0,X2) ) ). % 58.39/58.43 % 58.39/58.43 cnf(p9_23,negated_conjecture, % 58.39/58.43 ( p9(X133,X134) % 58.39/58.43 | ~ p9(X132,X133) % 58.39/58.43 | ~ p9(X132,X134) ) ). % 58.39/58.43 % 58.39/58.43 cnf(p8_24,negated_conjecture, % 58.39/58.43 ( p8(X126,X127) % 58.39/58.43 | ~ p8(X125,X126) % 58.39/58.43 | ~ p8(X125,X127) ) ). % 58.39/58.43 % 58.39/58.43 cnf(p6_25,negated_conjecture, % 58.39/58.43 ( p6(X123,X124) % 58.39/58.43 | ~ p6(X122,X123) % 58.39/58.43 | ~ p6(X122,X124) ) ). % 58.39/58.43 % 58.39/58.43 cnf(p4_26,negated_conjecture, % 58.39/58.43 ( p4(X112,X113) % 58.39/58.43 | ~ p4(X111,X112) % 58.39/58.43 | ~ p4(X111,X113) ) ). % 58.39/58.43 % 58.39/58.43 cnf(p37_27,negated_conjecture, % 58.39/58.43 ( p37(X101,X102) % 58.39/58.43 | ~ p37(X100,X101) % 58.39/58.43 | ~ p37(X100,X102) ) ). % 58.39/58.43 % 58.39/58.43 cnf(p35_28,negated_conjecture, % 58.39/58.43 ( p35(X94,X95) % 58.39/58.43 | ~ p35(X93,X94) % 58.39/58.43 | ~ p35(X93,X95) ) ). % 58.39/58.43 % 58.39/58.43 cnf(p33_29,negated_conjecture, % 58.39/58.43 ( p33(X87,X88) % 58.39/58.43 | ~ p33(X86,X87) % 58.39/58.43 | ~ p33(X86,X88) ) ). % 58.39/58.43 % 58.39/58.43 cnf(p31_30,negated_conjecture, % 58.39/58.43 ( p31(X80,X81) % 58.39/58.43 | ~ p31(X79,X80) % 58.39/58.43 | ~ p31(X79,X81) ) ). % 58.39/58.43 % 58.39/58.43 cnf(p3_31,negated_conjecture, % 58.39/58.43 ( p3(X69,X70) % 58.39/58.43 | ~ p3(X68,X69) % 58.39/58.43 | ~ p3(X68,X70) ) ). % 58.39/58.43 % 58.39/58.43 cnf(p29_32,negated_conjecture, % 58.39/58.43 ( p29(X66,X67) % 58.39/58.43 | ~ p29(X65,X66) % 58.39/58.43 | ~ p29(X65,X67) ) ). % 58.39/58.43 % 58.39/58.43 cnf(p27_33,negated_conjecture, % 58.39/58.43 ( p27(X59,X60) % 58.39/58.43 | ~ p27(X58,X59) % 58.39/58.43 | ~ p27(X58,X60) ) ). % 58.39/58.43 % 58.39/58.43 cnf(p25_34,negated_conjecture, % 58.39/58.43 ( p25(X52,X53) % 58.39/58.43 | ~ p25(X51,X52) % 58.39/58.43 | ~ p25(X51,X53) ) ). % 58.39/58.43 % 58.39/58.43 cnf(p23_35,negated_conjecture, % 58.39/58.43 ( p23(X41,X42) % 58.39/58.43 | ~ p23(X40,X41) % 58.39/58.43 | ~ p23(X40,X42) ) ). % 58.39/58.43 % 58.39/58.43 cnf(p22_36,negated_conjecture, % 58.39/58.43 ( p22(X38,X39) % 58.39/58.43 | ~ p22(X37,X38) % 58.39/58.43 | ~ p22(X37,X39) ) ). % 58.39/58.43 % 58.39/58.43 cnf(p20_37,negated_conjecture, % 58.39/58.43 ( p20(X35,X36) % 58.39/58.43 | ~ p20(X34,X35) % 58.39/58.43 | ~ p20(X34,X36) ) ). % 58.39/58.43 % 58.39/58.43 cnf(p2_38,negated_conjecture, % 58.39/58.43 ( p2(X32,X33) % 58.39/58.43 | ~ p2(X31,X32) % 58.39/58.43 | ~ p2(X31,X33) ) ). % 58.39/58.43 % 58.39/58.43 cnf(p18_39,negated_conjecture, % 58.39/58.43 ( p18(X25,X26) % 58.39/58.43 | ~ p18(X24,X26) % 58.39/58.43 | ~ p18(X24,X25) ) ). % 58.39/58.43 % 58.39/58.43 cnf(p16_40,negated_conjecture, % 58.39/58.43 ( p16(X18,X19) % 58.39/58.43 | ~ p16(X17,X18) % 58.39/58.43 | ~ p16(X17,X19) ) ). % 58.39/58.43 % 58.39/58.43 cnf(p14_41,negated_conjecture, % 58.39/58.43 ( p14(X15,X16) % 58.39/58.43 | ~ p14(X14,X15) % 58.39/58.43 | ~ p14(X14,X16) ) ). % 58.39/58.43 % 58.39/58.43 cnf(p12_42,negated_conjecture, % 58.39/58.43 ( p12(X8,X9) % 58.39/58.43 | ~ p12(X7,X8) % 58.39/58.43 | ~ p12(X7,X9) ) ). % 58.39/58.43 % 58.39/58.43 cnf(not_p39_43,negated_conjecture, % 58.39/58.43 ~ p39(f5(c40,f10(f13(f15(c42,c43),c44),c45)),c46) ). % 58.39/58.43 % 58.39/58.43 cnf(p39_44,negated_conjecture, % 58.39/58.43 ( p39(X47,X50) % 58.39/58.43 | ~ p39(f17(f19(f21(c47,X47),X48),X49),X50) ) ). % 58.39/58.43 % 58.39/58.43 cnf(p39_45,negated_conjecture, % 58.39/58.43 ( p39(X107,X108) % 58.39/58.43 | ~ p39(X110,X109) % 58.39/58.43 | ~ p4(X110,X107) % 58.39/58.43 | ~ p22(X109,X108) ) ). % 58.39/58.44 % 58.39/58.44 cnf(p39_46,negated_conjecture, % 58.39/58.44 p39(f5(c40,f7(c41,f10(f13(f15(c42,c43),c44),c45))),c46) ). % 58.39/58.44 % 58.39/58.44 cnf(p11_47,negated_conjecture, % 58.39/58.44 ( p11(f15(X3,X4),f15(X5,X6)) % 58.39/58.44 | ~ p14(X3,X5) % 58.39/58.44 | ~ p4(X4,X6) ) ). % 58.39/58.44 % 58.39/58.44 cnf(p9_48,negated_conjecture, % 58.39/58.44 ( p9(f34(X135,X136),f34(X137,X138)) % 58.39/58.44 | ~ p33(X135,X137) % 58.39/58.44 | ~ p9(X136,X138) ) ). % 58.39/58.44 % 58.39/58.44 cnf(p8_49,negated_conjecture, % 58.39/58.44 ( p8(f13(X128,X129),f13(X130,X131)) % 58.39/58.44 | ~ p11(X128,X130) % 58.39/58.44 | ~ p12(X129,X131) ) ). % 58.39/58.44 % 58.39/58.44 cnf(p4_50,negated_conjecture, % 58.39/58.44 ( p4(f5(X118,X119),f5(X120,X121)) % 58.39/58.44 | ~ p2(X118,X120) % 58.39/58.44 | ~ p3(X119,X121) ) ). % 58.39/58.44 % 58.39/58.44 cnf(p4_51,negated_conjecture, % 58.39/58.44 ( p4(f17(X114,X115),f17(X116,X117)) % 58.39/58.44 | ~ p16(X114,X116) % 58.39/58.44 | ~ p9(X115,X117) ) ). % 58.39/58.44 % 58.39/58.44 cnf(p35_52,negated_conjecture, % 58.39/58.44 ( p35(f38(X96,X97),f38(X98,X99)) % 58.39/58.44 | ~ p37(X96,X98) % 58.39/58.44 | ~ p4(X97,X99) ) ). % 58.39/58.44 % 58.39/58.44 cnf(p33_53,negated_conjecture, % 58.39/58.44 ( p33(f36(X89,X90),f36(X91,X92)) % 58.39/58.44 | ~ p12(X90,X92) % 58.39/58.44 | ~ p35(X89,X91) ) ). % 58.39/58.44 % 58.39/58.44 cnf(p31_54,negated_conjecture, % 58.39/58.44 ( p31(f32(X82,X83),f32(X84,X85)) % 58.39/58.44 | ~ p22(X83,X85) % 58.39/58.44 | ~ p9(X82,X84) ) ). % 58.39/58.44 % 58.39/58.44 cnf(p3_55,negated_conjecture, % 58.39/58.44 ( p3(f7(X75,X76),f7(X77,X78)) % 58.39/58.44 | ~ p3(X76,X78) % 58.39/58.44 | ~ p6(X75,X77) ) ). % 58.39/58.44 % 58.39/58.44 cnf(p3_56,negated_conjecture, % 58.39/58.44 ( p3(f10(X71,X72),f10(X73,X74)) % 58.39/58.44 | ~ p8(X71,X73) % 58.39/58.44 | ~ p9(X72,X74) ) ). % 58.39/58.44 % 58.39/58.44 cnf(p27_57,negated_conjecture, % 58.39/58.44 ( p27(f30(X61,X62),f30(X63,X64)) % 58.39/58.44 | ~ p29(X61,X63) % 58.39/58.44 | ~ p4(X62,X64) ) ). % 58.39/58.44 % 58.39/58.44 cnf(p25_58,negated_conjecture, % 58.39/58.44 ( p25(f28(X54,X55),f28(X56,X57)) % 58.39/58.44 | ~ p12(X55,X57) % 58.39/58.44 | ~ p27(X54,X56) ) ). % 58.39/58.44 % 58.39/58.44 cnf(p23_59,negated_conjecture, % 58.39/58.44 ( p23(f24(X43,X44),f24(X45,X46)) % 58.39/58.44 | ~ p12(X43,X45) % 58.39/58.44 | ~ p22(X44,X46) ) ). % 58.39/58.44 % 58.39/58.44 cnf(p18_60,negated_conjecture, % 58.39/58.44 ( p18(f21(X27,X28),f21(X29,X30)) % 58.39/58.44 | ~ p20(X27,X29) % 58.39/58.44 | ~ p4(X28,X30) ) ). % 58.39/58.44 % 58.39/58.44 cnf(p16_61,negated_conjecture, % 58.39/58.44 ( p16(f19(X20,X21),f19(X22,X23)) % 58.39/58.44 | ~ p12(X21,X23) % 58.39/58.44 | ~ p18(X20,X22) ) ). % 58.39/58.44 % 58.39/58.44 cnf(p12_62,negated_conjecture, % 58.39/58.44 ( p12(f26(X10,X11),f26(X12,X13)) % 58.39/58.44 | ~ p25(X10,X12) % 58.39/58.44 | ~ p9(X11,X13) ) ). % 58.39/58.44 % 58.39/58.44 cnf(p39_63,negated_conjecture, % 58.39/58.44 ( p39(X103,X104) % 58.39/58.44 | ~ p39(f5(c40,f10(f13(f15(c42,X103),X105),X106)),X104) ) ). % 58.39/58.44 % 58.39/58.44 cnf(p39_64,negated_conjecture, % 58.39/58.44 ( p39(f5(c40,f10(f13(f15(c42,X103),X105),X106)),X104) % 58.39/58.44 | ~ p39(X103,X104) ) ). % 58.39/58.44 % 58.39/58.44 cnf(p23_65,negated_conjecture, % 58.39/58.44 ( p23(f24(f26(f28(f30(c48,X47),X48),X49),X50),f24(X48,X50)) % 58.39/58.44 | ~ p39(f17(f19(f21(c47,X47),X48),X49),X50) ) ). % 58.39/58.44 % 58.39/58.44 cnf(p31_66,negated_conjecture, % 58.39/58.44 ( p31(f32(f34(f36(f38(c49,X47),X48),X49),X50),f32(X49,X50)) % 58.39/58.44 | ~ p39(f17(f19(f21(c47,X47),X48),X49),X50) ) ). % 58.39/58.44 % 58.39/58.44 cnf(p3_67,negated_conjecture, % 58.39/58.44 p3(f7(c41,f10(f13(f15(c42,X47),X48),X49)),f10(f13(f15(c42,f17(f19(f21(c47,X47),X48),X49)),f26(f28(f30(c48,X47),X48),X49)),f34(f36(f38(c49,X47),X48),X49))) ). % 58.39/58.44 % 58.39/58.44 %-------------------------------------------------------------------------- % 58.39/58.44 %------------------------------------------- % 58.39/58.44 % Proof found % 58.39/58.44 % SZS status Theorem for theBenchmark % 58.39/58.44 % SZS output start Proof % 58.39/58.44 %ClaNum:67(EqnAxiom:0) % 58.39/58.44 %VarNum:354(SingletonVarNum:175) % 58.39/58.44 %MaxLitNum:4 % 58.39/58.44 %MaxfuncDepth:5 % 58.39/58.44 %SharedTerms:18 % 58.39/58.44 %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 % 58.39/58.44 %singleGoalClaCount:24 % 58.39/58.44 [24]~P22(f15(a1,f9(f7(f5(a3,a4),a6),a8)),a10) % 58.39/58.44 [22]P22(f15(a1,f14(a2,f9(f7(f5(a3,a4),a6),a8))),a10) % 58.39/58.44 [1]P1(x11,x11) % 58.39/58.44 [2]P2(x21,x21) % 58.39/58.44 [3]P3(x31,x31) % 58.39/58.44 [4]P4(x41,x41) % 58.39/58.44 [5]P5(x51,x51) % 58.39/58.44 [6]P6(x61,x61) % 58.39/58.44 [7]P7(x71,x71) % 58.39/58.44 [8]P8(x81,x81) % 58.39/58.44 [9]P9(x91,x91) % 58.39/58.44 [10]P10(x101,x101) % 58.39/58.44 [11]P11(x111,x111) % 58.39/58.44 [12]P12(x121,x121) % 58.39/58.44 [13]P13(x131,x131) % 58.39/58.44 [14]P14(x141,x141) % 58.39/58.44 [15]P15(x151,x151) % 58.39/58.44 [16]P16(x161,x161) % 58.39/58.44 [17]P17(x171,x171) % 58.39/58.44 [18]P18(x181,x181) % 58.39/58.44 [19]P19(x191,x191) % 58.39/58.44 [20]P20(x201,x201) % 58.39/58.44 [21]P21(x211,x211) % 58.39/58.44 [23]P10(f14(a2,f9(f7(f5(a3,x231),x232),x233)),f9(f7(f5(a3,f18(f17(f16(a11,x231),x232),x233)),f21(f20(f19(a12,x231),x232),x233)),f25(f24(f23(a13,x231),x232),x233))) % 58.39/58.44 [63]P22(x631,x632)+~P22(f18(f17(f16(a11,x631),x633),x634),x632) % 58.39/58.44 [64]~P22(x641,x644)+P22(f15(a1,f9(f7(f5(a3,x641),x642),x643)),x644) % 58.39/58.44 [65]P22(x651,x652)+~P22(f15(a1,f9(f7(f5(a3,x651),x653),x654)),x652) % 58.39/58.44 [66]~P22(f18(f17(f16(a11,x661),x662),x663),x664)+P9(f26(f25(f24(f23(a13,x661),x662),x663),x664),f26(x663,x664)) % 58.39/58.44 [67]~P22(f18(f17(f16(a11,x671),x672),x673),x674)+P14(f22(f21(f20(f19(a12,x671),x672),x673),x674),f22(x672,x674)) % 58.39/58.44 [25]~P1(x253,x251)+P1(x251,x252)+~P1(x253,x252) % 58.39/58.44 [26]~P2(x263,x261)+P2(x261,x262)+~P2(x263,x262) % 58.39/58.44 [27]~P3(x273,x271)+P3(x271,x272)+~P3(x273,x272) % 58.39/58.44 [28]~P4(x283,x281)+P4(x281,x282)+~P4(x283,x282) % 58.39/58.44 [29]~P5(x293,x291)+P5(x291,x292)+~P5(x293,x292) % 58.39/58.44 [30]~P6(x303,x301)+P6(x301,x302)+~P6(x303,x302) % 58.39/58.44 [31]~P7(x313,x311)+P7(x311,x312)+~P7(x313,x312) % 58.39/58.44 [32]~P8(x323,x321)+P8(x321,x322)+~P8(x323,x322) % 58.39/58.44 [33]~P9(x333,x331)+P9(x331,x332)+~P9(x333,x332) % 58.39/58.44 [34]~P10(x343,x341)+P10(x341,x342)+~P10(x343,x342) % 58.39/58.44 [35]~P11(x353,x351)+P11(x351,x352)+~P11(x353,x352) % 58.39/58.44 [36]~P12(x363,x361)+P12(x361,x362)+~P12(x363,x362) % 58.39/58.44 [37]~P13(x373,x371)+P13(x371,x372)+~P13(x373,x372) % 58.39/58.44 [38]~P14(x383,x381)+P14(x381,x382)+~P14(x383,x382) % 58.39/58.44 [39]~P15(x393,x391)+P15(x391,x392)+~P15(x393,x392) % 58.39/58.44 [40]~P16(x403,x401)+P16(x401,x402)+~P16(x403,x402) % 58.39/58.44 [41]~P17(x413,x411)+P17(x411,x412)+~P17(x413,x412) % 58.39/58.44 [42]~P18(x423,x421)+P18(x421,x422)+~P18(x423,x422) % 58.39/58.44 [43]~P19(x433,x431)+P19(x431,x432)+~P19(x433,x432) % 58.39/58.44 [44]~P20(x443,x441)+P20(x441,x442)+~P20(x443,x442) % 58.39/58.44 [45]~P21(x453,x451)+P21(x451,x452)+~P21(x453,x452) % 58.39/58.44 [47]~P5(x472,x474)+~P20(x471,x473)+P1(f5(x471,x472),f5(x473,x474)) % 58.39/58.44 [48]~P2(x482,x484)+~P8(x481,x483)+P2(f25(x481,x482),f25(x483,x484)) % 58.39/58.44 [49]~P1(x491,x493)+~P21(x492,x494)+P3(f7(x491,x492),f7(x493,x494)) % 58.39/58.44 [50]~P10(x502,x504)+~P17(x501,x503)+P5(f15(x501,x502),f15(x503,x504)) % 58.39/58.44 [51]~P2(x512,x514)+~P19(x511,x513)+P5(f18(x511,x512),f18(x513,x514)) % 58.39/58.44 [52]~P5(x522,x524)+~P6(x521,x523)+P7(f23(x521,x522),f23(x523,x524)) % 58.39/58.44 [53]~P7(x531,x533)+~P21(x532,x534)+P8(f24(x531,x532),f24(x533,x534)) % 58.39/58.44 [54]~P2(x541,x543)+~P15(x542,x544)+P9(f26(x541,x542),f26(x543,x544)) % 58.39/58.44 [55]~P2(x552,x554)+~P3(x551,x553)+P10(f9(x551,x552),f9(x553,x554)) % 58.39/58.44 [56]~P4(x561,x563)+~P10(x562,x564)+P10(f14(x561,x562),f14(x563,x564)) % 58.39/58.44 [57]~P5(x572,x574)+~P11(x571,x573)+P12(f19(x571,x572),f19(x573,x574)) % 58.39/58.44 [58]~P12(x581,x583)+~P21(x582,x584)+P13(f20(x581,x582),f20(x583,x584)) % 58.39/58.44 [59]~P15(x592,x594)+~P21(x591,x593)+P14(f22(x591,x592),f22(x593,x594)) % 58.39/58.44 [60]~P5(x602,x604)+~P16(x601,x603)+P18(f16(x601,x602),f16(x603,x604)) % 58.39/58.44 [61]~P18(x611,x613)+~P21(x612,x614)+P19(f17(x611,x612),f17(x613,x614)) % 58.39/58.44 [62]~P2(x622,x624)+~P13(x621,x623)+P21(f21(x621,x622),f21(x623,x624)) % 58.39/58.44 [46]~P22(x463,x464)+P22(x461,x462)+~P5(x463,x461)+~P15(x464,x462) % 58.39/58.44 %EqnAxiom % 58.39/58.44 % 58.39/58.44 %------------------------------------------- % 58.39/58.45 cnf(68,plain, % 58.39/58.45 (~P22(a4,a10)), % 58.39/58.45 inference(scs_inference,[],[24,64])). % 58.39/58.45 cnf(71,plain, % 58.39/58.45 (~P22(f15(a1,f9(f7(f5(a3,f18(f17(f16(a11,a4),x711),x712)),x713),x714)),a10)), % 58.39/58.45 inference(scs_inference,[],[68,65,63])). % 58.39/58.45 cnf(77,plain, % 58.39/58.45 (P5(f15(x771,f14(a2,f9(f7(f5(a3,x772),x773),x774))),f15(x771,f9(f7(f5(a3,f18(f17(f16(a11,x772),x773),x774)),f21(f20(f19(a12,x772),x773),x774)),f25(f24(f23(a13,x772),x773),x774))))), % 58.39/58.45 inference(scs_inference,[],[17,23,41,50])). % 58.39/58.45 cnf(109,plain, % 58.39/58.45 ($false), % 58.39/58.45 inference(scs_inference,[],[77,71,22,15,46]), % 58.39/58.45 ['proof']). % 58.39/58.45 % SZS output end Proof % 58.39/58.45 % Total time :57.800000s %------------------------------------------------------------------------------