%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN717-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 : n021.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:24 EDT 2024 % Result : Unsatisfiable 0.68s 0.77s % Output : CNFRefutation 0.68s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN717-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.11/0.33 % Computer : n021.cluster.edu % 0.11/0.33 % Model : x86_64 x86_64 % 0.11/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.33 % Memory : 8042.1875MB % 0.11/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.33 % CPULimit : 300 % 0.11/0.33 % WCLimit : 300 % 0.11/0.33 % DateTime : Sun Jun 23 23:39:39 EDT 2024 % 0.11/0.33 % CPUTime : % 0.19/0.55 start to proof:theBenchmark % 0.68/0.74 %------------------------------------------- % 0.68/0.74 % File :CSE---1.7 % 0.68/0.75 % Problem :theBenchmark % 0.68/0.75 % Transform :cnf % 0.68/0.75 % Format :tptp:raw % 0.68/0.75 % Command :java -jar mcs_scs.jar %d %s % 0.68/0.75 % 0.68/0.75 % Result :Theorem 0.150000s % 0.68/0.75 % Output :CNFRefutation 0.150000s % 0.68/0.75 %------------------------------------------- % 0.68/0.75 %-------------------------------------------------------------------------- % 0.68/0.75 % File : SYN717-1 : TPTP v8.2.0. Released v2.5.0. % 0.68/0.75 % Domain : Syntactic % 0.68/0.75 % Problem : Harrison problem 4760 % 0.68/0.75 % Version : Especial. % 0.68/0.75 % English : % 0.68/0.75 % 0.68/0.75 % Refs : [Har01] Email to G. Sutcliffe % 0.68/0.75 % Source : [Har01] % 0.68/0.75 % Names : % 0.68/0.75 % 0.68/0.75 % Status : Unsatisfiable % 0.68/0.75 % Rating : 0.00 v7.4.0, 0.17 v7.1.0, 0.33 v7.0.0, 0.25 v6.3.0, 0.29 v6.2.0, 0.11 v6.1.0, 0.00 v5.0.0, 0.07 v4.1.0, 0.00 v2.5.0 % 0.68/0.75 % Syntax : Number of clauses : 113 ( 46 unt; 2 nHn; 76 RR) % 0.68/0.75 % Number of literals : 248 ( 0 equ; 135 neg) % 0.68/0.75 % Maximal clause size : 4 ( 2 avg) % 0.68/0.75 % Maximal term depth : 6 ( 1 avg) % 0.68/0.75 % Number of predicates : 38 ( 38 usr; 0 prp; 2-2 aty) % 0.68/0.75 % Number of functors : 51 ( 51 usr; 29 con; 0-2 aty) % 0.68/0.75 % Number of variables : 258 ( 2 sgn) % 0.68/0.75 % SPC : CNF_UNS_RFO_NEQ_NHN % 0.68/0.75 % 0.68/0.75 % Comments : % 0.68/0.75 %-------------------------------------------------------------------------- % 0.68/0.75 cnf(p10_1,negated_conjecture, % 0.68/0.75 p10(X0,X0) ). % 0.68/0.75 % 0.68/0.75 cnf(p9_2,negated_conjecture, % 0.68/0.75 p9(X202,X202) ). % 0.68/0.75 % 0.68/0.75 cnf(p7_3,negated_conjecture, % 0.68/0.75 p7(X195,X195) ). % 0.68/0.75 % 0.68/0.75 cnf(p6_4,negated_conjecture, % 0.68/0.75 p6(X183,X183) ). % 0.68/0.75 % 0.68/0.75 cnf(p57_5,negated_conjecture, % 0.68/0.75 p57(X176,X176) ). % 0.68/0.75 % 0.68/0.75 cnf(p55_6,negated_conjecture, % 0.68/0.75 p55(X169,X169) ). % 0.68/0.75 % 0.68/0.75 cnf(p53_7,negated_conjecture, % 0.68/0.75 p53(X162,X162) ). % 0.68/0.75 % 0.68/0.75 cnf(p52_8,negated_conjecture, % 0.68/0.75 p52(X159,X159) ). % 0.68/0.75 % 0.68/0.75 cnf(p50_9,negated_conjecture, % 0.68/0.75 p50(X156,X156) ). % 0.68/0.75 % 0.68/0.75 cnf(p49_10,negated_conjecture, % 0.68/0.75 p49(X153,X153) ). % 0.68/0.75 % 0.68/0.75 cnf(p47_11,negated_conjecture, % 0.68/0.75 p47(X146,X146) ). % 0.68/0.75 % 0.68/0.75 cnf(p46_12,negated_conjecture, % 0.68/0.75 p46(X143,X143) ). % 0.68/0.75 % 0.68/0.75 cnf(p44_13,negated_conjecture, % 0.68/0.75 p44(X136,X136) ). % 0.68/0.75 % 0.68/0.75 cnf(p41_14,negated_conjecture, % 0.68/0.75 p41(X133,X133) ). % 0.68/0.75 % 0.68/0.75 cnf(p4_15,negated_conjecture, % 0.68/0.75 p4(X122,X122) ). % 0.68/0.75 % 0.68/0.75 cnf(p39_16,negated_conjecture, % 0.68/0.75 p39(X115,X115) ). % 0.68/0.75 % 0.68/0.75 cnf(p37_17,negated_conjecture, % 0.68/0.75 p37(X112,X112) ). % 0.68/0.75 % 0.68/0.75 cnf(p35_18,negated_conjecture, % 0.68/0.75 p35(X109,X109) ). % 0.68/0.75 % 0.68/0.75 cnf(p34_19,negated_conjecture, % 0.68/0.75 p34(X106,X106) ). % 0.68/0.75 % 0.68/0.75 cnf(p32_20,negated_conjecture, % 0.68/0.75 p32(X103,X103) ). % 0.68/0.75 % 0.68/0.75 cnf(p30_21,negated_conjecture, % 0.68/0.75 p30(X96,X96) ). % 0.68/0.75 % 0.68/0.75 cnf(p3_22,negated_conjecture, % 0.68/0.75 p3(X89,X89) ). % 0.68/0.75 % 0.68/0.75 cnf(p28_23,negated_conjecture, % 0.68/0.75 p28(X82,X82) ). % 0.68/0.75 % 0.68/0.75 cnf(p27_24,negated_conjecture, % 0.68/0.75 p27(X75,X75) ). % 0.68/0.75 % 0.68/0.75 cnf(p26_25,negated_conjecture, % 0.68/0.75 p26(X72,X72) ). % 0.68/0.75 % 0.68/0.75 cnf(p24_26,negated_conjecture, % 0.68/0.75 p24(X65,X65) ). % 0.68/0.75 % 0.68/0.75 cnf(p23_27,negated_conjecture, % 0.68/0.75 p23(X58,X58) ). % 0.68/0.75 % 0.68/0.75 cnf(p22_28,negated_conjecture, % 0.68/0.75 p22(X55,X55) ). % 0.68/0.75 % 0.68/0.75 cnf(p20_29,negated_conjecture, % 0.68/0.75 p20(X48,X48) ). % 0.68/0.75 % 0.68/0.75 cnf(p2_30,negated_conjecture, % 0.68/0.75 p2(X45,X45) ). % 0.68/0.75 % 0.68/0.75 cnf(p19_31,negated_conjecture, % 0.68/0.75 p19(X27,X27) ). % 0.68/0.75 % 0.68/0.75 cnf(p18_32,negated_conjecture, % 0.68/0.75 p18(X24,X24) ). % 0.68/0.75 % 0.68/0.75 cnf(p16_33,negated_conjecture, % 0.68/0.75 p16(X21,X21) ). % 0.68/0.75 % 0.68/0.75 cnf(p14_34,negated_conjecture, % 0.68/0.75 p14(X14,X14) ). % 0.68/0.75 % 0.68/0.75 cnf(p12_35,negated_conjecture, % 0.68/0.75 p12(X11,X11) ). % 0.68/0.75 % 0.68/0.75 cnf(p23_36,negated_conjecture, % 0.68/0.75 p23(c79,c77) ). % 0.68/0.75 % 0.68/0.75 cnf(p59_37,negated_conjecture, % 0.68/0.75 p59(c64,c72) ). % 0.68/0.75 % 0.68/0.75 cnf(p59_38,negated_conjecture, % 0.68/0.75 p59(c64,c69) ). % 0.68/0.75 % 0.68/0.75 cnf(p59_39,negated_conjecture, % 0.68/0.75 p59(c64,c63) ). % 0.68/0.75 % 0.68/0.75 cnf(p59_40,negated_conjecture, % 0.68/0.75 p59(c62,c69) ). % 0.68/0.75 % 0.68/0.75 cnf(p59_41,negated_conjecture, % 0.68/0.75 p59(c62,c63) ). % 0.68/0.75 % 0.68/0.75 cnf(p60_42,negated_conjecture, % 0.68/0.75 p60(f25(c75,c79),f21(c76,c78)) ). % 0.68/0.75 % 0.68/0.75 cnf(p3_43,negated_conjecture, % 0.68/0.75 p3(f15(f17(c70,c71),c69),c72) ). % 0.68/0.75 % 0.68/0.75 cnf(p59_44,negated_conjecture, % 0.68/0.76 p59(f29(c73,f31(f33(c74,c77),c78)),c72) ). % 0.68/0.76 % 0.68/0.76 cnf(not_p4_45,negated_conjecture, % 0.68/0.76 ~ p4(f8(c65,f11(f13(c66,c63),c67)),c80) ). % 0.68/0.76 % 0.68/0.76 cnf(p10_46,negated_conjecture, % 0.68/0.76 ( p10(X1,X2) % 0.68/0.76 | ~ p10(X0,X1) % 0.68/0.76 | ~ p10(X0,X2) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p9_47,negated_conjecture, % 0.68/0.76 ( p9(X203,X204) % 0.68/0.76 | ~ p9(X202,X203) % 0.68/0.76 | ~ p9(X202,X204) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p7_48,negated_conjecture, % 0.68/0.76 ( p7(X196,X197) % 0.68/0.76 | ~ p7(X195,X196) % 0.68/0.76 | ~ p7(X195,X197) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p6_49,negated_conjecture, % 0.68/0.76 ( p6(X184,X185) % 0.68/0.76 | ~ p6(X183,X184) % 0.68/0.76 | ~ p6(X183,X185) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p57_50,negated_conjecture, % 0.68/0.76 ( p57(X177,X178) % 0.68/0.76 | ~ p57(X176,X177) % 0.68/0.76 | ~ p57(X176,X178) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p55_51,negated_conjecture, % 0.68/0.76 ( p55(X170,X171) % 0.68/0.76 | ~ p55(X169,X170) % 0.68/0.76 | ~ p55(X169,X171) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p53_52,negated_conjecture, % 0.68/0.76 ( p53(X163,X164) % 0.68/0.76 | ~ p53(X162,X163) % 0.68/0.76 | ~ p53(X162,X164) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p52_53,negated_conjecture, % 0.68/0.76 ( p52(X160,X161) % 0.68/0.76 | ~ p52(X159,X160) % 0.68/0.76 | ~ p52(X159,X161) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p50_54,negated_conjecture, % 0.68/0.76 ( p50(X157,X158) % 0.68/0.76 | ~ p50(X156,X157) % 0.68/0.76 | ~ p50(X156,X158) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p49_55,negated_conjecture, % 0.68/0.76 ( p49(X154,X155) % 0.68/0.76 | ~ p49(X153,X154) % 0.68/0.76 | ~ p49(X153,X155) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p47_56,negated_conjecture, % 0.68/0.76 ( p47(X147,X148) % 0.68/0.76 | ~ p47(X146,X147) % 0.68/0.76 | ~ p47(X146,X148) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p46_57,negated_conjecture, % 0.68/0.76 ( p46(X144,X145) % 0.68/0.76 | ~ p46(X143,X144) % 0.68/0.76 | ~ p46(X143,X145) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p44_58,negated_conjecture, % 0.68/0.76 ( p44(X137,X138) % 0.68/0.76 | ~ p44(X136,X137) % 0.68/0.76 | ~ p44(X136,X138) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p41_59,negated_conjecture, % 0.68/0.76 ( p41(X134,X135) % 0.68/0.76 | ~ p41(X133,X134) % 0.68/0.76 | ~ p41(X133,X135) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p4_60,negated_conjecture, % 0.68/0.76 ( p4(X123,X124) % 0.68/0.76 | ~ p4(X122,X123) % 0.68/0.76 | ~ p4(X122,X124) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p39_61,negated_conjecture, % 0.68/0.76 ( p39(X116,X117) % 0.68/0.76 | ~ p39(X115,X116) % 0.68/0.76 | ~ p39(X115,X117) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p37_62,negated_conjecture, % 0.68/0.76 ( p37(X113,X114) % 0.68/0.76 | ~ p37(X112,X113) % 0.68/0.76 | ~ p37(X112,X114) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p35_63,negated_conjecture, % 0.68/0.76 ( p35(X110,X111) % 0.68/0.76 | ~ p35(X109,X110) % 0.68/0.76 | ~ p35(X109,X111) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p34_64,negated_conjecture, % 0.68/0.76 ( p34(X107,X108) % 0.68/0.76 | ~ p34(X106,X107) % 0.68/0.76 | ~ p34(X106,X108) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p32_65,negated_conjecture, % 0.68/0.76 ( p32(X104,X105) % 0.68/0.76 | ~ p32(X103,X104) % 0.68/0.76 | ~ p32(X103,X105) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p30_66,negated_conjecture, % 0.68/0.76 ( p30(X97,X98) % 0.68/0.76 | ~ p30(X96,X97) % 0.68/0.76 | ~ p30(X96,X98) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p3_67,negated_conjecture, % 0.68/0.76 ( p3(X90,X91) % 0.68/0.76 | ~ p3(X89,X90) % 0.68/0.76 | ~ p3(X89,X91) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p28_68,negated_conjecture, % 0.68/0.76 ( p28(X83,X84) % 0.68/0.76 | ~ p28(X82,X83) % 0.68/0.76 | ~ p28(X82,X84) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p27_69,negated_conjecture, % 0.68/0.76 ( p27(X76,X77) % 0.68/0.76 | ~ p27(X75,X76) % 0.68/0.76 | ~ p27(X75,X77) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p26_70,negated_conjecture, % 0.68/0.76 ( p26(X73,X74) % 0.68/0.76 | ~ p26(X72,X73) % 0.68/0.76 | ~ p26(X72,X74) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p24_71,negated_conjecture, % 0.68/0.76 ( p24(X66,X67) % 0.68/0.76 | ~ p24(X65,X66) % 0.68/0.76 | ~ p24(X65,X67) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p23_72,negated_conjecture, % 0.68/0.76 ( p23(X59,X60) % 0.68/0.76 | ~ p23(X58,X59) % 0.68/0.76 | ~ p23(X58,X60) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p22_73,negated_conjecture, % 0.68/0.76 ( p22(X56,X57) % 0.68/0.76 | ~ p22(X55,X56) % 0.68/0.76 | ~ p22(X55,X57) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p20_74,negated_conjecture, % 0.68/0.76 ( p20(X49,X50) % 0.68/0.76 | ~ p20(X48,X49) % 0.68/0.76 | ~ p20(X48,X50) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p2_75,negated_conjecture, % 0.68/0.76 ( p2(X46,X47) % 0.68/0.76 | ~ p2(X45,X46) % 0.68/0.76 | ~ p2(X45,X47) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p19_76,negated_conjecture, % 0.68/0.76 ( p19(X28,X29) % 0.68/0.76 | ~ p19(X27,X28) % 0.68/0.76 | ~ p19(X27,X29) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p18_77,negated_conjecture, % 0.68/0.76 ( p18(X25,X26) % 0.68/0.76 | ~ p18(X24,X25) % 0.68/0.76 | ~ p18(X24,X26) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p16_78,negated_conjecture, % 0.68/0.76 ( p16(X22,X23) % 0.68/0.76 | ~ p16(X21,X22) % 0.68/0.76 | ~ p16(X21,X23) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p14_79,negated_conjecture, % 0.68/0.76 ( p14(X15,X16) % 0.68/0.76 | ~ p14(X14,X15) % 0.68/0.76 | ~ p14(X14,X16) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p12_80,negated_conjecture, % 0.68/0.76 ( p12(X12,X13) % 0.68/0.76 | ~ p12(X11,X12) % 0.68/0.76 | ~ p12(X11,X13) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p4_81,negated_conjecture, % 0.68/0.76 p4(f8(c65,f11(f13(c66,c63),c67)),f5(c68,c69)) ). % 0.68/0.76 % 0.68/0.76 cnf(p61_82,negated_conjecture, % 0.68/0.76 ( p61(X190,X191) % 0.68/0.76 | ~ p53(X193,X190) % 0.68/0.76 | ~ p61(X193,X192) % 0.68/0.76 | ~ p10(X192,X191) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p59_83,negated_conjecture, % 0.68/0.76 ( p59(X179,X180) % 0.68/0.76 | ~ p3(X182,X180) % 0.68/0.76 | ~ p59(X181,X182) % 0.68/0.76 | ~ p28(X181,X179) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p60_84,negated_conjecture, % 0.68/0.76 ( p60(X186,X187) % 0.68/0.76 | ~ p24(X189,X186) % 0.68/0.76 | ~ p60(X189,X188) % 0.68/0.76 | ~ p20(X188,X187) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p9_85,negated_conjecture, % 0.68/0.76 ( p9(f13(X205,X206),f13(X207,X208)) % 0.68/0.76 | ~ p12(X205,X207) % 0.68/0.76 | ~ p3(X206,X208) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p10_86,negated_conjecture, % 0.68/0.76 ( p10(f45(X3,X4),f45(X5,X6)) % 0.68/0.76 | ~ p3(X4,X6) % 0.68/0.76 | ~ p44(X3,X5) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p10_87,negated_conjecture, % 0.68/0.76 ( p10(f56(X7,X8),f56(X9,X10)) % 0.68/0.76 | ~ p10(X8,X10) % 0.68/0.76 | ~ p55(X7,X9) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p14_88,negated_conjecture, % 0.68/0.76 ( p14(f17(X17,X18),f17(X19,X20)) % 0.68/0.76 | ~ p16(X17,X19) % 0.68/0.76 | ~ p3(X18,X20) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p19_89,negated_conjecture, % 0.68/0.76 ( p19(f36(X30,X31),f36(X32,X33)) % 0.68/0.76 | ~ p34(X30,X32) % 0.68/0.76 | ~ p35(X31,X33) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p19_90,negated_conjecture, % 0.68/0.76 ( p19(f40(X34,X35),f40(X36,X37)) % 0.68/0.76 | ~ p19(X35,X37) % 0.68/0.76 | ~ p39(X34,X36) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p19_91,negated_conjecture, % 0.68/0.76 ( p19(f43(X41,X42),f43(X43,X44)) % 0.68/0.76 | ~ p23(X42,X44) % 0.68/0.76 | ~ p35(X41,X43) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p20_92,negated_conjecture, % 0.68/0.76 ( p20(f21(X51,X52),f21(X53,X54)) % 0.68/0.76 | ~ p18(X51,X53) % 0.68/0.76 | ~ p19(X52,X54) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p23_93,negated_conjecture, % 0.68/0.76 ( p23(f38(X61,X62),f38(X63,X64)) % 0.68/0.76 | ~ p35(X62,X64) % 0.68/0.76 | ~ p37(X61,X63) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p24_94,negated_conjecture, % 0.68/0.76 ( p24(f25(X68,X69),f25(X70,X71)) % 0.68/0.76 | ~ p22(X68,X70) % 0.68/0.76 | ~ p23(X69,X71) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p27_95,negated_conjecture, % 0.68/0.76 ( p27(f31(X78,X79),f31(X80,X81)) % 0.68/0.76 | ~ p19(X79,X81) % 0.68/0.76 | ~ p30(X78,X80) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p28_96,negated_conjecture, % 0.68/0.76 ( p28(f29(X85,X86),f29(X87,X88)) % 0.68/0.76 | ~ p26(X85,X87) % 0.68/0.76 | ~ p27(X86,X88) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p3_97,negated_conjecture, % 0.68/0.76 ( p3(f15(X92,X93),f15(X94,X95)) % 0.68/0.76 | ~ p14(X92,X94) % 0.68/0.76 | ~ p3(X93,X95) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p30_98,negated_conjecture, % 0.68/0.76 ( p30(f33(X99,X100),f33(X101,X102)) % 0.68/0.76 | ~ p23(X100,X102) % 0.68/0.76 | ~ p32(X99,X101) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p39_99,negated_conjecture, % 0.68/0.76 ( p39(f42(X118,X119),f42(X120,X121)) % 0.68/0.76 | ~ p35(X119,X121) % 0.68/0.76 | ~ p41(X118,X120) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p4_100,negated_conjecture, % 0.68/0.76 ( p4(f5(X125,X126),f5(X127,X128)) % 0.68/0.76 | ~ p2(X125,X127) % 0.68/0.76 | ~ p3(X126,X128) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p4_101,negated_conjecture, % 0.68/0.76 ( p4(f8(X129,X130),f8(X131,X132)) % 0.68/0.76 | ~ p6(X129,X131) % 0.68/0.76 | ~ p7(X130,X132) ) ). % 0.68/0.76 % 0.68/0.76 cnf(p44_102,negated_conjecture, % 0.68/0.77 ( p44(f48(X139,X140),f48(X141,X142)) % 0.68/0.77 | ~ p46(X139,X141) % 0.68/0.77 | ~ p47(X140,X142) ) ). % 0.68/0.77 % 0.68/0.77 cnf(p47_103,negated_conjecture, % 0.68/0.77 ( p47(f51(X149,X150),f51(X151,X152)) % 0.68/0.77 | ~ p49(X149,X151) % 0.68/0.77 | ~ p50(X150,X152) ) ). % 0.68/0.77 % 0.68/0.77 cnf(p53_104,negated_conjecture, % 0.68/0.77 ( p53(f54(X165,X166),f54(X167,X168)) % 0.68/0.77 | ~ p35(X166,X168) % 0.68/0.77 | ~ p52(X165,X167) ) ). % 0.68/0.77 % 0.68/0.77 cnf(p55_105,negated_conjecture, % 0.68/0.77 ( p55(f58(X172,X173),f58(X174,X175)) % 0.68/0.77 | ~ p10(X173,X175) % 0.68/0.77 | ~ p57(X172,X174) ) ). % 0.68/0.77 % 0.68/0.77 cnf(p7_106,negated_conjecture, % 0.68/0.77 ( p7(f11(X198,X199),f11(X200,X201)) % 0.68/0.77 | ~ p10(X199,X201) % 0.68/0.77 | ~ p9(X198,X200) ) ). % 0.68/0.77 % 0.68/0.77 cnf(not_p60_107,negated_conjecture, % 0.68/0.77 ( ~ p60(f25(c75,X209),f21(c76,X212)) % 0.68/0.77 | ~ p59(f29(c73,f31(f33(c74,X211),X212)),c72) % 0.68/0.77 | ~ p59(f29(c73,f31(f33(c74,X209),X210)),c72) ) ). % 0.68/0.77 % 0.68/0.77 cnf(p61_108,negated_conjecture, % 0.68/0.77 ( p61(f54(c86,X194),f45(f48(c88,f51(c89,c90)),c69)) % 0.68/0.77 | ~ p61(f54(c86,X194),f56(f58(c87,f45(f48(c88,f51(c89,c90)),c63)),c67)) ) ). % 0.68/0.77 % 0.68/0.77 cnf(p61_109,negated_conjecture, % 0.68/0.77 ( p61(f54(c86,X194),f56(f58(c87,f45(f48(c88,f51(c89,c90)),c63)),c67)) % 0.68/0.77 | ~ p61(f54(c86,X194),f45(f48(c88,f51(c89,c90)),c69)) ) ). % 0.68/0.77 % 0.68/0.77 cnf(p19_110,negated_conjecture, % 0.68/0.77 ( p19(f43(X38,X39),f40(f42(c81,X38),X40)) % 0.68/0.77 | p59(f29(c73,f31(f33(c74,f38(c82,X38)),f36(c83,X38))),c72) % 0.68/0.77 | ~ p59(f29(c73,f31(f33(c74,X39),X40)),c69) ) ). % 0.68/0.77 % 0.68/0.77 cnf(p19_111,negated_conjecture, % 0.68/0.77 ( p19(f43(X38,X39),f40(f42(c81,X38),X40)) % 0.68/0.77 | p59(f29(c73,f31(f33(c74,f38(c84,X38)),f36(c85,X38))),c69) % 0.68/0.77 | ~ p59(f29(c73,f31(f33(c74,X39),X40)),c72) ) ). % 0.68/0.77 % 0.68/0.77 cnf(p19_112,negated_conjecture, % 0.68/0.77 ( p19(f43(X38,X39),f40(f42(c81,X38),X40)) % 0.68/0.77 | ~ p59(f29(c73,f31(f33(c74,X39),X40)),c72) % 0.68/0.77 | ~ p19(f43(X38,f38(c84,X38)),f40(f42(c81,X38),f36(c85,X38))) ) ). % 0.68/0.77 % 0.68/0.77 cnf(p19_113,negated_conjecture, % 0.68/0.77 ( p19(f43(X38,X39),f40(f42(c81,X38),X40)) % 0.68/0.77 | ~ p59(f29(c73,f31(f33(c74,X39),X40)),c69) % 0.68/0.77 | ~ p19(f43(X38,f38(c82,X38)),f40(f42(c81,X38),f36(c83,X38))) ) ). % 0.68/0.77 % 0.68/0.77 %-------------------------------------------------------------------------- % 0.68/0.77 %------------------------------------------- % 0.68/0.77 % Proof found % 0.68/0.77 % SZS status Theorem for theBenchmark % 0.68/0.77 % SZS output start Proof % 0.68/0.77 %ClaNum:113(EqnAxiom:0) % 0.68/0.77 %VarNum:526(SingletonVarNum:258) % 0.68/0.77 %MaxLitNum:4 % 0.68/0.77 %MaxfuncDepth:5 % 0.68/0.77 %SharedTerms:57 % 0.68/0.77 %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 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 % 0.68/0.77 %singleGoalClaCount:46 % 0.68/0.77 [1]P1(a1,a2) % 0.68/0.77 [2]P11(a3,a6) % 0.68/0.77 [3]P11(a3,a7) % 0.68/0.77 [4]P11(a3,a4) % 0.68/0.77 [5]P11(a5,a7) % 0.68/0.77 [6]P11(a5,a4) % 0.68/0.77 [42]P37(f19(a14,a1),f20(a17,a18)) % 0.68/0.77 [43]P29(f22(f21(a12,a13),a7),a6) % 0.68/0.77 [44]P11(f38(a15,f37(f36(a16,a2),a18)),a6) % 0.68/0.77 [45]P22(f39(a8,f24(f23(a9,a4),a10)),f40(a11,a7)) % 0.68/0.77 [46]~P22(f39(a8,f24(f23(a9,a4),a10)),a25) % 0.68/0.77 [7]P2(x71,x71) % 0.68/0.77 [8]P34(x81,x81) % 0.68/0.77 [9]P35(x91,x91) % 0.68/0.77 [10]P36(x101,x101) % 0.68/0.77 [11]P12(x111,x111) % 0.68/0.77 [12]P13(x121,x121) % 0.68/0.77 [13]P14(x131,x131) % 0.68/0.77 [14]P15(x141,x141) % 0.68/0.77 [15]P16(x151,x151) % 0.68/0.77 [16]P17(x161,x161) % 0.68/0.77 [17]P18(x171,x171) % 0.68/0.77 [18]P19(x181,x181) % 0.68/0.77 [19]P20(x191,x191) % 0.68/0.77 [20]P21(x201,x201) % 0.68/0.77 [21]P22(x211,x211) % 0.68/0.77 [22]P23(x221,x221) % 0.68/0.77 [23]P24(x231,x231) % 0.68/0.77 [24]P25(x241,x241) % 0.68/0.77 [25]P26(x251,x251) % 0.68/0.77 [26]P27(x261,x261) % 0.68/0.77 [27]P28(x271,x271) % 0.68/0.77 [28]P29(x281,x281) % 0.68/0.77 [29]P30(x291,x291) % 0.68/0.77 [30]P31(x301,x301) % 0.68/0.77 [31]P32(x311,x311) % 0.68/0.77 [32]P33(x321,x321) % 0.68/0.77 [33]P1(x331,x331) % 0.68/0.77 [34]P3(x341,x341) % 0.68/0.77 [35]P4(x351,x351) % 0.68/0.77 [36]P5(x361,x361) % 0.68/0.77 [37]P6(x371,x371) % 0.68/0.77 [38]P7(x381,x381) % 0.68/0.77 [39]P8(x391,x391) % 0.68/0.77 [40]P9(x401,x401) % 0.68/0.77 [41]P10(x411,x411) % 0.68/0.77 [112]~P38(f49(a31,x1121),f41(f47(a33,f50(a34,a35)),a7))+P38(f49(a31,x1121),f48(f51(a32,f41(f47(a33,f50(a34,a35)),a4)),a10)) % 0.68/0.77 [113]P38(f49(a31,x1131),f41(f47(a33,f50(a34,a35)),a7))+~P38(f49(a31,x1131),f48(f51(a32,f41(f47(a33,f50(a34,a35)),a4)),a10)) % 0.68/0.77 [47]~P2(x473,x471)+P2(x471,x472)+~P2(x473,x472) % 0.68/0.77 [48]~P34(x483,x481)+P34(x481,x482)+~P34(x483,x482) % 0.68/0.77 [49]~P35(x493,x491)+P35(x491,x492)+~P35(x493,x492) % 0.68/0.77 [50]~P36(x503,x501)+P36(x501,x502)+~P36(x503,x502) % 0.68/0.77 [51]~P12(x513,x511)+P12(x511,x512)+~P12(x513,x512) % 0.68/0.77 [52]~P13(x523,x521)+P13(x521,x522)+~P13(x523,x522) % 0.68/0.77 [53]~P14(x533,x531)+P14(x531,x532)+~P14(x533,x532) % 0.68/0.77 [54]~P15(x543,x541)+P15(x541,x542)+~P15(x543,x542) % 0.68/0.77 [55]~P16(x553,x551)+P16(x551,x552)+~P16(x553,x552) % 0.68/0.77 [56]~P17(x563,x561)+P17(x561,x562)+~P17(x563,x562) % 0.68/0.77 [57]~P18(x573,x571)+P18(x571,x572)+~P18(x573,x572) % 0.68/0.77 [58]~P19(x583,x581)+P19(x581,x582)+~P19(x583,x582) % 0.68/0.77 [59]~P20(x593,x591)+P20(x591,x592)+~P20(x593,x592) % 0.68/0.77 [60]~P21(x603,x601)+P21(x601,x602)+~P21(x603,x602) % 0.68/0.77 [61]~P22(x613,x611)+P22(x611,x612)+~P22(x613,x612) % 0.68/0.77 [62]~P23(x623,x621)+P23(x621,x622)+~P23(x623,x622) % 0.68/0.77 [63]~P24(x633,x631)+P24(x631,x632)+~P24(x633,x632) % 0.68/0.77 [64]~P25(x643,x641)+P25(x641,x642)+~P25(x643,x642) % 0.68/0.77 [65]~P26(x653,x651)+P26(x651,x652)+~P26(x653,x652) % 0.68/0.77 [66]~P27(x663,x661)+P27(x661,x662)+~P27(x663,x662) % 0.68/0.77 [67]~P28(x673,x671)+P28(x671,x672)+~P28(x673,x672) % 0.68/0.77 [68]~P29(x683,x681)+P29(x681,x682)+~P29(x683,x682) % 0.68/0.77 [69]~P30(x693,x691)+P30(x691,x692)+~P30(x693,x692) % 0.68/0.77 [70]~P31(x703,x701)+P31(x701,x702)+~P31(x703,x702) % 0.68/0.77 [71]~P32(x713,x711)+P32(x711,x712)+~P32(x713,x712) % 0.68/0.77 [72]~P33(x723,x721)+P33(x721,x722)+~P33(x723,x722) % 0.68/0.77 [73]~P1(x733,x731)+P1(x731,x732)+~P1(x733,x732) % 0.68/0.77 [74]~P3(x743,x741)+P3(x741,x742)+~P3(x743,x742) % 0.68/0.77 [75]~P4(x753,x751)+P4(x751,x752)+~P4(x753,x752) % 0.68/0.77 [76]~P5(x763,x761)+P5(x761,x762)+~P5(x763,x762) % 0.68/0.77 [77]~P6(x773,x771)+P6(x771,x772)+~P6(x773,x772) % 0.68/0.77 [78]~P7(x783,x781)+P7(x781,x782)+~P7(x783,x782) % 0.68/0.77 [79]~P8(x793,x791)+P8(x791,x792)+~P8(x793,x792) % 0.68/0.77 [80]~P9(x803,x801)+P9(x801,x802)+~P9(x803,x802) % 0.68/0.77 [81]~P10(x813,x811)+P10(x811,x812)+~P10(x813,x812) % 0.68/0.77 [108]P6(f46(x1081,x1082),f45(f42(a26,x1081),x1083))+~P6(f46(x1081,f43(a27,x1081)),f45(f42(a26,x1081),f44(a30,x1081)))+~P11(f38(a15,f37(f36(a16,x1082),x1083)),a6) % 0.68/0.77 [109]P6(f46(x1091,x1092),f45(f42(a26,x1091),x1093))+~P6(f46(x1091,f43(a28,x1091)),f45(f42(a26,x1091),f44(a29,x1091)))+~P11(f38(a15,f37(f36(a16,x1092),x1093)),a7) % 0.68/0.77 [110]P6(f46(x1101,x1102),f45(f42(a26,x1101),x1103))+~P11(f38(a15,f37(f36(a16,x1102),x1103)),a7)+P11(f38(a15,f37(f36(a16,f43(a28,x1101)),f44(a29,x1101))),a6) % 0.68/0.77 [111]P6(f46(x1111,x1112),f45(f42(a26,x1111),x1113))+~P11(f38(a15,f37(f36(a16,x1112),x1113)),a6)+P11(f38(a15,f37(f36(a16,f43(a27,x1111)),f44(a30,x1111))),a7) % 0.68/0.77 [85]~P20(x851,x853)+~P29(x852,x854)+P2(f41(x851,x852),f41(x853,x854)) % 0.68/0.77 [86]~P2(x862,x864)+~P13(x861,x863)+P2(f48(x861,x862),f48(x863,x864)) % 0.68/0.77 [87]~P29(x872,x874)+~P10(x871,x873)+P34(f23(x871,x872),f23(x873,x874)) % 0.68/0.77 [88]~P2(x882,x884)+~P34(x881,x883)+P35(f24(x881,x882),f24(x883,x884)) % 0.68/0.77 [89]~P2(x892,x894)+~P12(x891,x893)+P13(f51(x891,x892),f51(x893,x894)) % 0.68/0.77 [90]~P15(x901,x903)+~P25(x902,x904)+P14(f49(x901,x902),f49(x903,x904)) % 0.68/0.77 [91]~P16(x912,x914)+~P17(x911,x913)+P18(f50(x911,x912),f50(x913,x914)) % 0.68/0.77 [92]~P18(x922,x924)+~P19(x921,x923)+P20(f47(x921,x922),f47(x923,x924)) % 0.68/0.77 [93]~P35(x932,x934)+~P36(x931,x933)+P22(f39(x931,x932),f39(x933,x934)) % 0.68/0.77 [94]~P29(x942,x944)+~P5(x941,x943)+P22(f40(x941,x942),f40(x943,x944)) % 0.68/0.77 [95]~P21(x951,x953)+~P25(x952,x954)+P23(f42(x951,x952),f42(x953,x954)) % 0.68/0.77 [96]~P27(x961,x963)+~P1(x962,x964)+P28(f36(x961,x962),f36(x963,x964)) % 0.68/0.77 [97]~P29(x972,x974)+~P9(x971,x973)+P29(f22(x971,x972),f22(x973,x974)) % 0.68/0.77 [98]~P31(x982,x984)+~P32(x981,x983)+P30(f38(x981,x982),f38(x983,x984)) % 0.68/0.77 [99]~P28(x991,x993)+~P6(x992,x994)+P31(f37(x991,x992),f37(x993,x994)) % 0.68/0.77 [100]~P1(x1002,x1004)+~P3(x1001,x1003)+P33(f19(x1001,x1002),f19(x1003,x1004)) % 0.68/0.77 [101]~P24(x1011,x1013)+~P25(x1012,x1014)+P1(f43(x1011,x1012),f43(x1013,x1014)) % 0.68/0.77 [102]~P6(x1022,x1024)+~P7(x1021,x1023)+P4(f20(x1021,x1022),f20(x1023,x1024)) % 0.68/0.77 [103]~P25(x1032,x1034)+~P26(x1031,x1033)+P6(f44(x1031,x1032),f44(x1033,x1034)) % 0.68/0.77 [104]~P23(x1041,x1043)+~P6(x1042,x1044)+P6(f45(x1041,x1042),f45(x1043,x1044)) % 0.68/0.77 [105]~P25(x1051,x1053)+~P1(x1052,x1054)+P6(f46(x1051,x1052),f46(x1053,x1054)) % 0.68/0.77 [106]~P29(x1062,x1064)+~P8(x1061,x1063)+P9(f21(x1061,x1062),f21(x1063,x1064)) % 0.68/0.77 [107]~P37(f19(a14,x1071),f20(a17,x1072))+~P11(f38(a15,f37(f36(a16,x1073),x1072)),a6)+~P11(f38(a15,f37(f36(a16,x1071),x1074)),a6) % 0.68/0.77 [82]~P11(x824,x823)+P11(x821,x822)+~P29(x823,x822)+~P30(x824,x821) % 0.68/0.77 [83]~P37(x833,x834)+P37(x831,x832)+~P33(x833,x831)+~P4(x834,x832) % 0.68/0.77 [84]~P38(x844,x843)+P38(x841,x842)+~P2(x843,x842)+~P14(x844,x841) % 0.68/0.77 %EqnAxiom % 0.68/0.77 % 0.68/0.77 %------------------------------------------- % 0.68/0.77 cnf(117,plain, % 0.68/0.77 (~P37(f19(a14,a2),f20(a17,a18))), % 0.68/0.77 inference(scs_inference,[],[1,33,44,73,107])). % 0.68/0.77 cnf(157,plain, % 0.68/0.77 (P33(f19(x1571,a1),f19(x1571,a2))), % 0.68/0.77 inference(scs_inference,[],[34,1,74,100])). % 0.68/0.77 cnf(158,plain, % 0.68/0.77 ($false), % 0.68/0.77 inference(scs_inference,[],[117,157,35,42,83]), % 0.68/0.77 ['proof']). % 0.68/0.77 % SZS output end Proof % 0.68/0.77 % Total time :0.150000s %------------------------------------------------------------------------------