%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN714-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 : n025.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:23 EDT 2024 % Result : Unsatisfiable 0.66s 1.01s % Output : CNFRefutation 0.66s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.05/0.15 % Problem : SYN714-1 : TPTP v8.2.0. Released v2.5.0. % 0.05/0.15 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.14/0.37 % Computer : n025.cluster.edu % 0.14/0.37 % Model : x86_64 x86_64 % 0.14/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.37 % Memory : 8042.1875MB % 0.14/0.37 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.37 % CPULimit : 300 % 0.14/0.37 % WCLimit : 300 % 0.14/0.37 % DateTime : Sun Jun 23 21:30:39 EDT 2024 % 0.14/0.37 % CPUTime : % 0.55/0.69 start to proof:theBenchmark % 0.66/0.99 %------------------------------------------- % 0.66/0.99 % File :CSE---1.7 % 0.66/0.99 % Problem :theBenchmark % 0.66/0.99 % Transform :cnf % 0.66/0.99 % Format :tptp:raw % 0.66/0.99 % Command :java -jar mcs_scs.jar %d %s % 0.66/0.99 % 0.66/0.99 % Result :Theorem 0.240000s % 0.66/0.99 % Output :CNFRefutation 0.240000s % 0.66/0.99 %------------------------------------------- % 0.66/0.99 %-------------------------------------------------------------------------- % 0.66/0.99 % File : SYN714-1 : TPTP v8.2.0. Released v2.5.0. % 0.66/0.99 % Domain : Syntactic % 0.66/0.99 % Problem : Harrison problem 4753 % 0.66/0.99 % Version : Especial. % 0.66/1.00 % English : % 0.66/1.00 % 0.66/1.00 % Refs : [Har01] Email to G. Sutcliffe % 0.66/1.00 % Source : [Har01] % 0.66/1.00 % Names : % 0.66/1.00 % 0.66/1.00 % Status : Unsatisfiable % 0.66/1.00 % Rating : 0.00 v5.5.0, 0.12 v5.4.0, 0.10 v5.2.0, 0.00 v5.0.0, 0.07 v4.1.0, 0.00 v4.0.1, 0.20 v4.0.0, 0.14 v3.4.0, 0.25 v3.3.0, 0.33 v3.1.0, 0.17 v2.7.0, 0.00 v2.6.0, 0.33 v2.5.0 % 0.66/1.00 % Syntax : Number of clauses : 105 ( 31 unt; 13 nHn; 79 RR) % 0.66/1.00 % Number of literals : 275 ( 0 equ; 149 neg) % 0.66/1.00 % Maximal clause size : 5 ( 2 avg) % 0.66/1.00 % Maximal term depth : 3 ( 1 avg) % 0.66/1.00 % Number of predicates : 32 ( 32 usr; 0 prp; 1-3 aty) % 0.66/1.00 % Number of functors : 35 ( 35 usr; 11 con; 0-3 aty) % 0.66/1.00 % Number of variables : 245 ( 4 sgn) % 0.66/1.00 % SPC : CNF_UNS_RFO_NEQ_NHN % 0.66/1.00 % 0.66/1.00 % Comments : % 0.66/1.00 %-------------------------------------------------------------------------- % 0.66/1.00 cnf(c62_is_p48_1,negated_conjecture, % 0.66/1.00 p48(c62) ). % 0.66/1.00 % 0.66/1.00 cnf(c60_is_p47_2,negated_conjecture, % 0.66/1.00 p47(c60) ). % 0.66/1.00 % 0.66/1.00 cnf(p10_3,negated_conjecture, % 0.66/1.00 p10(X0,X0) ). % 0.66/1.00 % 0.66/1.00 cnf(p7_4,negated_conjecture, % 0.66/1.00 p7(X201,X201) ). % 0.66/1.00 % 0.66/1.00 cnf(p5_5,negated_conjecture, % 0.66/1.00 p5(X141,X141) ). % 0.66/1.00 % 0.66/1.00 cnf(p42_6,negated_conjecture, % 0.66/1.00 p42(X120,X120) ). % 0.66/1.00 % 0.66/1.00 cnf(p40_7,negated_conjecture, % 0.66/1.00 p40(X115,X115) ). % 0.66/1.00 % 0.66/1.00 cnf(p36_8,negated_conjecture, % 0.66/1.00 p36(X112,X112) ). % 0.66/1.00 % 0.66/1.00 cnf(p33_9,negated_conjecture, % 0.66/1.00 p33(X105,X105) ). % 0.66/1.00 % 0.66/1.00 cnf(p32_10,negated_conjecture, % 0.66/1.00 p32(X98,X98) ). % 0.66/1.00 % 0.66/1.00 cnf(p30_11,negated_conjecture, % 0.66/1.00 p30(X95,X95) ). % 0.66/1.00 % 0.66/1.00 cnf(p3_12,negated_conjecture, % 0.66/1.00 p3(X80,X80) ). % 0.66/1.00 % 0.66/1.00 cnf(p28_13,negated_conjecture, % 0.66/1.00 p28(X73,X73) ). % 0.66/1.00 % 0.66/1.00 cnf(p26_14,negated_conjecture, % 0.66/1.00 p26(X64,X64) ). % 0.66/1.00 % 0.66/1.00 cnf(p24_15,negated_conjecture, % 0.66/1.00 p24(X55,X55) ). % 0.66/1.00 % 0.66/1.00 cnf(p23_16,negated_conjecture, % 0.66/1.00 p23(X48,X48) ). % 0.66/1.00 % 0.66/1.00 cnf(p2_17,negated_conjecture, % 0.66/1.00 p2(X35,X35) ). % 0.66/1.00 % 0.66/1.00 cnf(p19_18,negated_conjecture, % 0.66/1.00 p19(X30,X30) ). % 0.66/1.00 % 0.66/1.00 cnf(p18_19,negated_conjecture, % 0.66/1.00 p18(X23,X23) ). % 0.66/1.00 % 0.66/1.00 cnf(p16_20,negated_conjecture, % 0.66/1.00 p16(X12,X12) ). % 0.66/1.00 % 0.66/1.00 cnf(p15_21,negated_conjecture, % 0.66/1.00 p15(X7,X7) ). % 0.66/1.00 % 0.66/1.00 cnf(p51_22,negated_conjecture, % 0.66/1.00 p51(c66,c67) ). % 0.66/1.00 % 0.66/1.00 cnf(p53_23,negated_conjecture, % 0.66/1.00 p53(c68,f17(c66)) ). % 0.66/1.00 % 0.66/1.00 cnf(not_p16_24,negated_conjecture, % 0.66/1.00 ~ p16(f17(c66),c65) ). % 0.66/1.00 % 0.66/1.00 cnf(p10_25,negated_conjecture, % 0.66/1.00 p10(f11(c62),f11(c60)) ). % 0.66/1.00 % 0.66/1.00 cnf(p49_26,negated_conjecture, % 0.66/1.00 p49(f4(c60),f4(c62)) ). % 0.66/1.00 % 0.66/1.00 cnf(p3_27,negated_conjecture, % 0.66/1.00 p3(f12(c62),f12(c60)) ). % 0.66/1.00 % 0.66/1.00 cnf(p52_28,negated_conjecture, % 0.66/1.00 p52(f20(f21(c62,c64)),c66) ). % 0.66/1.00 % 0.66/1.00 cnf(p2_29,negated_conjecture, % 0.66/1.00 p2(f22(c58,c60,c61),c62) ). % 0.66/1.00 % 0.66/1.00 cnf(p47_30,negated_conjecture, % 0.66/1.00 ( p47(X133) % 0.66/1.00 | ~ p47(X134) % 0.66/1.00 | ~ p2(X134,X133) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p48_31,negated_conjecture, % 0.66/1.00 ( p48(X135) % 0.66/1.00 | ~ p48(X136) % 0.66/1.00 | ~ p2(X136,X135) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p49_32,negated_conjecture, % 0.66/1.00 p49(f4(c62),f13(f14(c63),f4(c60))) ). % 0.66/1.00 % 0.66/1.00 cnf(not_p50_33,negated_conjecture, % 0.66/1.00 ~ p50(c66,f25(f27(c59,c68),c67),c60) ). % 0.66/1.00 % 0.66/1.00 cnf(p40_34,negated_conjecture, % 0.66/1.00 ( p40(f41(X118),f41(X119)) % 0.66/1.00 | ~ p15(X118,X119) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p10_35,negated_conjecture, % 0.66/1.00 ( p10(f11(X3),f11(X4)) % 0.66/1.00 | ~ p2(X3,X4) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p10_36,negated_conjecture, % 0.66/1.00 ( p10(f31(X5),f31(X6)) % 0.66/1.00 | ~ p30(X5,X6) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p15_37,negated_conjecture, % 0.66/1.00 ( p15(f38(X10),f38(X11)) % 0.66/1.00 | ~ p15(X10,X11) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p16_38,negated_conjecture, % 0.66/1.00 ( p16(f17(X21),f17(X22)) % 0.66/1.00 | ~ p15(X21,X22) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p19_39,negated_conjecture, % 0.66/1.00 ( p19(f20(X33),f20(X34)) % 0.66/1.00 | ~ p18(X33,X34) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p24_40,negated_conjecture, % 0.66/1.00 ( p24(f39(X62),f39(X63)) % 0.66/1.00 | ~ p15(X62,X63) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p3_41,negated_conjecture, % 0.66/1.00 ( p3(f12(X83),f12(X84)) % 0.66/1.00 | ~ p2(X83,X84) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p3_42,negated_conjecture, % 0.66/1.00 ( p3(f14(X89),f14(X90)) % 0.66/1.00 | ~ p3(X89,X90) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p3_43,negated_conjecture, % 0.66/1.00 ( p3(f37(X91),f37(X92)) % 0.66/1.00 | ~ p36(X91,X92) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p3_44,negated_conjecture, % 0.66/1.00 ( p3(f4(X93),f4(X94)) % 0.66/1.00 | ~ p2(X93,X94) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p10_45,negated_conjecture, % 0.66/1.00 ( p10(X1,X2) % 0.66/1.00 | ~ p10(X0,X1) % 0.66/1.00 | ~ p10(X0,X2) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p7_46,negated_conjecture, % 0.66/1.00 ( p7(X202,X203) % 0.66/1.00 | ~ p7(X201,X202) % 0.66/1.00 | ~ p7(X201,X203) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p5_47,negated_conjecture, % 0.66/1.00 ( p5(X142,X143) % 0.66/1.00 | ~ p5(X141,X142) % 0.66/1.00 | ~ p5(X141,X143) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p42_48,negated_conjecture, % 0.66/1.00 ( p42(X121,X122) % 0.66/1.00 | ~ p42(X120,X121) % 0.66/1.00 | ~ p42(X120,X122) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p40_49,negated_conjecture, % 0.66/1.00 ( p40(X116,X117) % 0.66/1.00 | ~ p40(X115,X116) % 0.66/1.00 | ~ p40(X115,X117) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p36_50,negated_conjecture, % 0.66/1.00 ( p36(X113,X114) % 0.66/1.00 | ~ p36(X112,X113) % 0.66/1.00 | ~ p36(X112,X114) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p33_51,negated_conjecture, % 0.66/1.00 ( p33(X106,X107) % 0.66/1.00 | ~ p33(X105,X106) % 0.66/1.00 | ~ p33(X105,X107) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p32_52,negated_conjecture, % 0.66/1.00 ( p32(X99,X100) % 0.66/1.00 | ~ p32(X98,X99) % 0.66/1.00 | ~ p32(X98,X100) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p30_53,negated_conjecture, % 0.66/1.00 ( p30(X96,X97) % 0.66/1.00 | ~ p30(X95,X96) % 0.66/1.00 | ~ p30(X95,X97) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p3_54,negated_conjecture, % 0.66/1.00 ( p3(X81,X82) % 0.66/1.00 | ~ p3(X80,X81) % 0.66/1.00 | ~ p3(X80,X82) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p28_55,negated_conjecture, % 0.66/1.00 ( p28(X74,X75) % 0.66/1.00 | ~ p28(X73,X74) % 0.66/1.00 | ~ p28(X73,X75) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p26_56,negated_conjecture, % 0.66/1.00 ( p26(X65,X66) % 0.66/1.00 | ~ p26(X64,X65) % 0.66/1.00 | ~ p26(X64,X66) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p24_57,negated_conjecture, % 0.66/1.00 ( p24(X56,X57) % 0.66/1.00 | ~ p24(X55,X56) % 0.66/1.00 | ~ p24(X55,X57) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p23_58,negated_conjecture, % 0.66/1.00 ( p23(X49,X50) % 0.66/1.00 | ~ p23(X48,X49) % 0.66/1.00 | ~ p23(X48,X50) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p2_59,negated_conjecture, % 0.66/1.00 ( p2(X36,X37) % 0.66/1.00 | ~ p2(X35,X36) % 0.66/1.00 | ~ p2(X35,X37) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p19_60,negated_conjecture, % 0.66/1.00 ( p19(X31,X32) % 0.66/1.00 | ~ p19(X30,X31) % 0.66/1.00 | ~ p19(X30,X32) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p18_61,negated_conjecture, % 0.66/1.00 ( p18(X24,X25) % 0.66/1.00 | ~ p18(X23,X24) % 0.66/1.00 | ~ p18(X23,X25) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p16_62,negated_conjecture, % 0.66/1.00 ( p16(X13,X14) % 0.66/1.00 | ~ p16(X12,X13) % 0.66/1.00 | ~ p16(X12,X14) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p15_63,negated_conjecture, % 0.66/1.00 ( p15(X8,X9) % 0.66/1.00 | ~ p15(X7,X8) % 0.66/1.00 | ~ p15(X7,X9) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p50_64,negated_conjecture, % 0.66/1.00 ( p50(c66,f25(f27(c59,X160),c67),c62) % 0.66/1.00 | ~ p53(X160,f17(c66)) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p57_65,negated_conjecture, % 0.66/1.00 ( p57(X197,X198) % 0.66/1.00 | ~ p5(X200,X198) % 0.66/1.00 | ~ p57(X199,X200) % 0.66/1.00 | ~ p5(X199,X197) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p45_66,negated_conjecture, % 0.66/1.00 ( p45(X125,X126) % 0.66/1.00 | ~ p5(X127,X125) % 0.66/1.00 | ~ p5(X128,X126) % 0.66/1.00 | ~ p45(X127,X128) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p46_67,negated_conjecture, % 0.66/1.00 ( p46(X129,X130) % 0.66/1.00 | ~ p46(X132,X131) % 0.66/1.00 | ~ p7(X132,X129) % 0.66/1.00 | ~ p3(X131,X130) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p49_68,negated_conjecture, % 0.66/1.00 ( p49(X137,X138) % 0.66/1.00 | ~ p3(X140,X138) % 0.66/1.00 | ~ p49(X139,X140) % 0.66/1.00 | ~ p3(X139,X137) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p51_69,negated_conjecture, % 0.66/1.00 ( p51(X161,X162) % 0.66/1.00 | ~ p24(X164,X162) % 0.66/1.00 | ~ p51(X163,X164) % 0.66/1.00 | ~ p15(X163,X161) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p52_70,negated_conjecture, % 0.66/1.00 ( p52(X169,X170) % 0.66/1.00 | ~ p19(X172,X169) % 0.66/1.00 | ~ p52(X172,X171) % 0.66/1.00 | ~ p15(X171,X170) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p53_71,negated_conjecture, % 0.66/1.00 ( p53(X173,X174) % 0.66/1.00 | ~ p26(X176,X173) % 0.66/1.00 | ~ p53(X176,X175) % 0.66/1.00 | ~ p16(X175,X174) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p54_72,negated_conjecture, % 0.66/1.00 ( p54(X177,X178) % 0.66/1.00 | ~ p30(X180,X177) % 0.66/1.00 | ~ p54(X180,X179) % 0.66/1.00 | ~ p28(X179,X178) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p55_73,negated_conjecture, % 0.66/1.00 ( p55(X185,X186) % 0.66/1.00 | ~ p5(X188,X185) % 0.66/1.00 | ~ p55(X188,X187) % 0.66/1.00 | ~ p10(X187,X186) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p56_74,negated_conjecture, % 0.66/1.00 ( p56(X189,X190) % 0.66/1.00 | ~ p36(X192,X189) % 0.66/1.00 | ~ p56(X192,X191) % 0.66/1.00 | ~ p33(X191,X190) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p45_75,negated_conjecture, % 0.66/1.00 ( p45(X123,c61) % 0.66/1.00 | ~ p46(f8(f9(c58,X123),X124),f4(f6(c59,c60))) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p7_76,negated_conjecture, % 0.66/1.00 ( p7(f8(X204,X205),f8(X206,X207)) % 0.66/1.00 | ~ p5(X204,X206) % 0.66/1.00 | ~ p5(X205,X207) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p18_77,negated_conjecture, % 0.66/1.00 ( p18(f21(X26,X27),f21(X28,X29)) % 0.66/1.00 | ~ p18(X27,X29) % 0.66/1.00 | ~ p2(X26,X28) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p2_78,negated_conjecture, % 0.66/1.00 ( p2(f6(X44,X45),f6(X46,X47)) % 0.66/1.00 | ~ p2(X45,X47) % 0.66/1.00 | ~ p5(X44,X46) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p23_79,negated_conjecture, % 0.66/1.00 ( p23(f27(X51,X52),f27(X53,X54)) % 0.66/1.00 | ~ p26(X52,X54) % 0.66/1.00 | ~ p5(X51,X53) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p24_80,negated_conjecture, % 0.66/1.00 ( p24(f25(X58,X59),f25(X60,X61)) % 0.66/1.00 | ~ p23(X58,X60) % 0.66/1.00 | ~ p24(X59,X61) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p28_81,negated_conjecture, % 0.66/1.00 ( p28(f29(X76,X77),f29(X78,X79)) % 0.66/1.00 | ~ p28(X77,X79) % 0.66/1.00 | ~ p7(X76,X78) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p3_82,negated_conjecture, % 0.66/1.00 ( p3(f13(X85,X86),f13(X87,X88)) % 0.66/1.00 | ~ p3(X85,X87) % 0.66/1.00 | ~ p3(X86,X88) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p32_83,negated_conjecture, % 0.66/1.00 ( p32(f35(X101,X102),f35(X103,X104)) % 0.66/1.00 | ~ p5(X101,X103) % 0.66/1.00 | ~ p7(X102,X104) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p33_84,negated_conjecture, % 0.66/1.00 ( p33(f34(X108,X109),f34(X110,X111)) % 0.66/1.00 | ~ p32(X108,X110) % 0.66/1.00 | ~ p33(X109,X111) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p5_85,negated_conjecture, % 0.66/1.00 ( p5(f9(X150,X151),f9(X152,X153)) % 0.66/1.00 | ~ p5(X150,X152) % 0.66/1.00 | ~ p5(X151,X153) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p56_86,negated_conjecture, % 0.66/1.00 ( p56(X193,f34(f35(X194,X195),X196)) % 0.66/1.00 | ~ p56(X193,X196) % 0.66/1.00 | ~ p46(X195,f37(X193)) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p51_87,negated_conjecture, % 0.66/1.00 ( p51(X165,f25(f27(X166,X167),X168)) % 0.66/1.00 | ~ p51(X165,X168) % 0.66/1.00 | ~ p53(X167,f17(X165)) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p54_88,negated_conjecture, % 0.66/1.00 ( p54(X181,f29(f8(X182,X183),X184)) % 0.66/1.00 | ~ p54(X181,X184) % 0.66/1.00 | ~ p55(X183,f31(X181)) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p50_89,negated_conjecture, % 0.66/1.00 ( p50(X154,X155,X156) % 0.66/1.00 | ~ p15(X157,X154) % 0.66/1.00 | ~ p2(X158,X156) % 0.66/1.00 | ~ p24(X159,X155) % 0.66/1.00 | ~ p50(X157,X159,X158) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p2_90,negated_conjecture, % 0.66/1.00 ( p2(f22(X38,X39,X40),f22(X41,X42,X43)) % 0.66/1.00 | ~ p5(X38,X41) % 0.66/1.00 | ~ p5(X40,X43) % 0.66/1.00 | ~ p2(X39,X42) ) ). % 0.66/1.00 % 0.66/1.00 cnf(p5_91,negated_conjecture, % 0.66/1.00 ( p5(f43(X144,X145,X146),f43(X147,X148,X149)) % 0.66/1.00 | ~ p42(X146,X149) % 0.66/1.00 | ~ p5(X145,X148) % 0.66/1.01 | ~ p15(X144,X147) ) ). % 0.66/1.01 % 0.66/1.01 cnf(p26_92,negated_conjecture, % 0.66/1.01 ( p26(f44(X67,X68,X69),f44(X70,X71,X72)) % 0.66/1.01 | ~ p42(X69,X72) % 0.66/1.01 | ~ p5(X68,X71) % 0.66/1.01 | ~ p15(X67,X70) ) ). % 0.66/1.01 % 0.66/1.01 cnf(p51_93,negated_conjecture, % 0.66/1.01 ( p51(X17,f39(X17)) % 0.66/1.01 | p16(f17(X17),c65) % 0.66/1.01 | p16(f17(f38(X17)),f17(X17)) % 0.66/1.01 | ~ p52(f20(f21(c60,c64)),X17) ) ). % 0.66/1.01 % 0.66/1.01 cnf(p51_94,negated_conjecture, % 0.66/1.01 ( p51(X17,f39(X17)) % 0.66/1.01 | p16(f17(X17),c65) % 0.66/1.01 | p40(f41(f38(X17)),f41(X17)) % 0.66/1.01 | ~ p52(f20(f21(c60,c64)),X17) ) ). % 0.66/1.01 % 0.66/1.01 cnf(p51_95,negated_conjecture, % 0.66/1.01 ( p51(X17,f39(X17)) % 0.66/1.01 | p16(f17(X17),c65) % 0.66/1.01 | p52(f20(f21(c62,c64)),f38(X17)) % 0.66/1.01 | ~ p52(f20(f21(c60,c64)),X17) ) ). % 0.66/1.01 % 0.66/1.01 cnf(p16_96,negated_conjecture, % 0.66/1.01 ( p16(f17(X17),c65) % 0.66/1.01 | p16(f17(f38(X17)),f17(X17)) % 0.66/1.01 | ~ p50(X17,f39(X17),c60) % 0.66/1.01 | ~ p52(f20(f21(c60,c64)),X17) ) ). % 0.66/1.01 % 0.66/1.01 cnf(p16_97,negated_conjecture, % 0.66/1.01 ( p16(f17(X17),c65) % 0.66/1.01 | p40(f41(f38(X17)),f41(X17)) % 0.66/1.01 | ~ p50(X17,f39(X17),c60) % 0.66/1.01 | ~ p52(f20(f21(c60,c64)),X17) ) ). % 0.66/1.01 % 0.66/1.01 cnf(p16_98,negated_conjecture, % 0.66/1.01 ( p16(f17(X15),c65) % 0.66/1.01 | p50(X15,X16,c60) % 0.66/1.01 | ~ p51(X15,X16) % 0.66/1.01 | ~ p50(X15,X16,c62) % 0.66/1.01 | ~ p52(f20(f21(c62,c64)),X15) ) ). % 0.66/1.01 % 0.66/1.01 cnf(p16_99,negated_conjecture, % 0.66/1.01 ( p16(f17(X17),c65) % 0.66/1.01 | p52(f20(f21(c62,c64)),f38(X17)) % 0.66/1.01 | ~ p50(X17,f39(X17),c60) % 0.66/1.01 | ~ p52(f20(f21(c60,c64)),X17) ) ). % 0.66/1.01 % 0.66/1.01 cnf(p51_100,negated_conjecture, % 0.66/1.01 ( p51(X17,f39(X17)) % 0.66/1.01 | p16(f17(X17),c65) % 0.66/1.01 | p50(f38(X17),X20,c62) % 0.66/1.01 | ~ p51(f38(X17),X20) % 0.66/1.01 | ~ p52(f20(f21(c60,c64)),X17) ) ). % 0.66/1.01 % 0.66/1.01 cnf(p16_101,negated_conjecture, % 0.66/1.01 ( p16(f17(X17),c65) % 0.66/1.01 | p50(f38(X17),X20,c62) % 0.66/1.01 | ~ p51(f38(X17),X20) % 0.66/1.01 | ~ p50(X17,f39(X17),c60) % 0.66/1.01 | ~ p52(f20(f21(c60,c64)),X17) ) ). % 0.66/1.01 % 0.66/1.01 cnf(p51_102,negated_conjecture, % 0.66/1.01 ( p51(X17,f39(X17)) % 0.66/1.01 | p16(f17(X17),c65) % 0.66/1.01 | p57(c61,f43(X17,X18,X19)) % 0.66/1.01 | p26(f44(f38(X17),X18,X19),f44(X17,X18,X19)) % 0.66/1.01 | ~ p52(f20(f21(c60,c64)),X17) ) ). % 0.66/1.01 % 0.66/1.01 cnf(p16_103,negated_conjecture, % 0.66/1.01 ( p16(f17(X17),c65) % 0.66/1.01 | p57(c61,f43(X17,X18,X19)) % 0.66/1.01 | p26(f44(f38(X17),X18,X19),f44(X17,X18,X19)) % 0.66/1.01 | ~ p50(X17,f39(X17),c60) % 0.66/1.01 | ~ p52(f20(f21(c60,c64)),X17) ) ). % 0.66/1.01 % 0.66/1.01 cnf(p51_104,negated_conjecture, % 0.66/1.01 ( p51(X17,f39(X17)) % 0.66/1.01 | p16(f17(X17),c65) % 0.66/1.01 | p5(X18,f9(c58,f43(X17,X18,X19))) % 0.66/1.01 | p26(f44(f38(X17),X18,X19),f44(X17,X18,X19)) % 0.66/1.01 | ~ p52(f20(f21(c60,c64)),X17) ) ). % 0.66/1.01 % 0.66/1.01 cnf(p16_105,negated_conjecture, % 0.66/1.01 ( p16(f17(X17),c65) % 0.66/1.01 | p5(X18,f9(c58,f43(X17,X18,X19))) % 0.66/1.01 | p26(f44(f38(X17),X18,X19),f44(X17,X18,X19)) % 0.66/1.01 | ~ p50(X17,f39(X17),c60) % 0.66/1.01 | ~ p52(f20(f21(c60,c64)),X17) ) ). % 0.66/1.01 % 0.66/1.01 %-------------------------------------------------------------------------- % 0.66/1.01 %------------------------------------------- % 0.66/1.01 % Proof found % 0.66/1.01 % SZS status Theorem for theBenchmark % 0.66/1.01 % SZS output start Proof % 0.66/1.01 %ClaNum:105(EqnAxiom:0) % 0.66/1.01 %VarNum:553(SingletonVarNum:245) % 0.66/1.01 %MaxLitNum:5 % 0.66/1.01 %MaxfuncDepth:2 % 0.66/1.01 %SharedTerms:41 % 0.66/1.01 %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 % 0.66/1.01 %singleGoalClaCount:31 % 0.66/1.01 [1]P1(a1) % 0.66/1.01 [2]P2(a2) % 0.66/1.01 [3]P22(a6,a10) % 0.66/1.01 [23]P27(a11,f12(a6)) % 0.66/1.01 [24]P3(f13(a1),f13(a2)) % 0.66/1.01 [25]P10(f14(a1),f14(a2)) % 0.66/1.01 [26]P24(f17(a2),f17(a1)) % 0.66/1.01 [29]P15(f20(a3,a2,a5),a1) % 0.66/1.01 [30]~P18(f12(a6),a9) % 0.66/1.01 [27]P24(f17(a1),f16(f15(a7),f17(a2))) % 0.66/1.01 [28]P28(f19(f18(a1,a8)),a6) % 0.66/1.01 [31]~P25(a6,f22(f21(a4,a11),a10),a2) % 0.66/1.01 [4]P3(x41,x41) % 0.66/1.01 [5]P26(x51,x51) % 0.66/1.01 [6]P23(x61,x61) % 0.66/1.01 [7]P4(x71,x71) % 0.66/1.01 [8]P5(x81,x81) % 0.66/1.01 [9]P6(x91,x91) % 0.66/1.01 [10]P7(x101,x101) % 0.66/1.01 [11]P8(x111,x111) % 0.66/1.01 [12]P9(x121,x121) % 0.66/1.01 [13]P10(x131,x131) % 0.66/1.01 [14]P11(x141,x141) % 0.66/1.01 [15]P12(x151,x151) % 0.66/1.01 [16]P13(x161,x161) % 0.66/1.01 [17]P14(x171,x171) % 0.66/1.01 [18]P15(x181,x181) % 0.66/1.01 [19]P16(x191,x191) % 0.66/1.01 [20]P17(x201,x201) % 0.66/1.01 [21]P18(x211,x211) % 0.66/1.01 [22]P19(x221,x221) % 0.66/1.01 [87]~P27(x871,f12(a6))+P25(a6,f22(f21(a4,x871),a10),a1) % 0.66/1.01 [34]~P15(x341,x342)+P3(f13(x341),f13(x342)) % 0.66/1.01 [35]~P9(x351,x352)+P3(f23(x351),f23(x352)) % 0.66/1.01 [36]~P19(x361,x362)+P5(f30(x361),f30(x362)) % 0.66/1.01 [37]~P15(x371,x372)+P10(f17(x371),f17(x372)) % 0.66/1.01 [38]~P15(x381,x382)+P10(f14(x381),f14(x382)) % 0.66/1.01 [39]~P10(x391,x392)+P10(f15(x391),f15(x392)) % 0.66/1.01 [40]~P6(x401,x402)+P10(f25(x401),f25(x402)) % 0.66/1.01 [41]~P19(x411,x412)+P13(f28(x411),f28(x412)) % 0.66/1.01 [42]~P17(x421,x422)+P16(f19(x421),f19(x422)) % 0.66/1.01 [43]~P19(x431,x432)+P18(f12(x431),f12(x432)) % 0.66/1.01 [44]~P19(x441,x442)+P19(f29(x441),f29(x442)) % 0.66/1.01 [92]P20(x921,a5)+~P21(f31(f35(a3,x921),x922),f17(f32(a4,a2))) % 0.66/1.01 [32]~P15(x322,x321)+P1(x321)+~P1(x322) % 0.66/1.01 [33]~P15(x332,x331)+P2(x331)+~P2(x332) % 0.66/1.01 [45]~P3(x453,x451)+P3(x451,x452)+~P3(x453,x452) % 0.66/1.01 [46]~P26(x463,x461)+P26(x461,x462)+~P26(x463,x462) % 0.66/1.01 [47]~P23(x473,x471)+P23(x471,x472)+~P23(x473,x472) % 0.66/1.01 [48]~P4(x483,x481)+P4(x481,x482)+~P4(x483,x482) % 0.66/1.01 [49]~P5(x493,x491)+P5(x491,x492)+~P5(x493,x492) % 0.66/1.01 [50]~P6(x503,x501)+P6(x501,x502)+~P6(x503,x502) % 0.66/1.01 [51]~P7(x513,x511)+P7(x511,x512)+~P7(x513,x512) % 0.66/1.01 [52]~P8(x523,x521)+P8(x521,x522)+~P8(x523,x522) % 0.66/1.01 [53]~P9(x533,x531)+P9(x531,x532)+~P9(x533,x532) % 0.66/1.01 [54]~P10(x543,x541)+P10(x541,x542)+~P10(x543,x542) % 0.66/1.01 [55]~P11(x553,x551)+P11(x551,x552)+~P11(x553,x552) % 0.66/1.01 [56]~P12(x563,x561)+P12(x561,x562)+~P12(x563,x562) % 0.66/1.01 [57]~P13(x573,x571)+P13(x571,x572)+~P13(x573,x572) % 0.66/1.01 [58]~P14(x583,x581)+P14(x581,x582)+~P14(x583,x582) % 0.66/1.01 [59]~P15(x593,x591)+P15(x591,x592)+~P15(x593,x592) % 0.66/1.01 [60]~P16(x603,x601)+P16(x601,x602)+~P16(x603,x602) % 0.66/1.01 [61]~P17(x613,x611)+P17(x611,x612)+~P17(x613,x612) % 0.66/1.01 [62]~P18(x623,x621)+P18(x621,x622)+~P18(x623,x622) % 0.66/1.01 [63]~P19(x633,x631)+P19(x631,x632)+~P19(x633,x632) % 0.66/1.01 [74]~P23(x742,x744)+~P23(x741,x743)+P26(f31(x741,x742),f31(x743,x744)) % 0.66/1.01 [75]~P23(x752,x754)+~P23(x751,x753)+P23(f35(x751,x752),f35(x753,x754)) % 0.66/1.01 [76]~P7(x762,x764)+~P8(x761,x763)+P7(f26(x761,x762),f26(x763,x764)) % 0.66/1.01 [77]~P26(x772,x774)+~P23(x771,x773)+P8(f27(x771,x772),f27(x773,x774)) % 0.66/1.01 [78]~P10(x782,x784)+~P10(x781,x783)+P10(f16(x781,x782),f16(x783,x784)) % 0.66/1.01 [79]~P26(x791,x793)+~P11(x792,x794)+P11(f24(x791,x792),f24(x793,x794)) % 0.66/1.01 [80]~P13(x802,x804)+~P14(x801,x803)+P13(f22(x801,x802),f22(x803,x804)) % 0.66/1.01 [81]~P23(x811,x813)+~P12(x812,x814)+P14(f21(x811,x812),f21(x813,x814)) % 0.66/1.01 [82]~P23(x821,x823)+~P15(x822,x824)+P15(f32(x821,x822),f32(x823,x824)) % 0.66/1.01 [83]~P15(x831,x833)+~P17(x832,x834)+P17(f18(x831,x832),f18(x833,x834)) % 0.66/1.01 [84]~P22(x841,x844)+~P27(x843,f12(x841))+P22(x841,f22(f21(x842,x843),x844)) % 0.66/1.01 [85]~P30(x851,x854)+~P31(x853,f23(x851))+P30(x851,f24(f31(x852,x853),x854)) % 0.66/1.01 [86]~P32(x861,x864)+~P21(x863,f25(x861))+P32(x861,f26(f27(x862,x863),x864)) % 0.66/1.01 [88]P22(x881,f28(x881))+P18(f12(x881),a9)+P5(f30(f29(x881)),f30(x881))+~P28(f19(f18(a2,a8)),x881) % 0.66/1.01 [89]P22(x891,f28(x891))+P18(f12(x891),a9)+P18(f12(f29(x891)),f12(x891))+~P28(f19(f18(a2,a8)),x891) % 0.66/1.01 [90]P22(x901,f28(x901))+P18(f12(x901),a9)+P28(f19(f18(a1,a8)),f29(x901))+~P28(f19(f18(a2,a8)),x901) % 0.66/1.01 [94]~P25(x941,f28(x941),a2)+P5(f30(f29(x941)),f30(x941))+P18(f12(x941),a9)+~P28(f19(f18(a2,a8)),x941) % 0.66/1.01 [95]~P25(x951,f28(x951),a2)+P18(f12(f29(x951)),f12(x951))+P18(f12(x951),a9)+~P28(f19(f18(a2,a8)),x951) % 0.66/1.01 [96]~P25(x961,f28(x961),a2)+P18(f12(x961),a9)+P28(f19(f18(a1,a8)),f29(x961))+~P28(f19(f18(a2,a8)),x961) % 0.66/1.01 [64]~P22(x644,x643)+P22(x641,x642)+~P13(x643,x642)+~P19(x644,x641) % 0.66/1.01 [65]~P27(x653,x654)+P27(x651,x652)+~P12(x653,x651)+~P18(x654,x652) % 0.66/1.01 [66]~P24(x663,x664)+P24(x661,x662)+~P10(x663,x661)+~P10(x664,x662) % 0.66/1.01 [67]~P28(x673,x674)+P28(x671,x672)+~P16(x673,x671)+~P19(x674,x672) % 0.66/1.01 [68]~P29(x683,x684)+P29(x681,x682)+~P23(x683,x681)+~P23(x684,x682) % 0.66/1.01 [69]~P20(x694,x693)+P20(x691,x692)+~P23(x693,x692)+~P23(x694,x691) % 0.66/1.01 [70]~P21(x703,x704)+P21(x701,x702)+~P26(x703,x701)+~P10(x704,x702) % 0.66/1.01 [71]~P30(x713,x714)+P30(x711,x712)+~P9(x713,x711)+~P11(x714,x712) % 0.66/1.01 [72]~P31(x724,x723)+P31(x721,x722)+~P3(x723,x722)+~P23(x724,x721) % 0.66/1.01 [73]~P32(x733,x734)+P32(x731,x732)+~P6(x733,x731)+~P7(x734,x732) % 0.66/1.01 [98]~P23(x982,x985)+~P4(x983,x986)+~P19(x981,x984)+P23(f33(x981,x982,x983),f33(x984,x985,x986)) % 0.66/1.01 [99]~P23(x992,x995)+~P4(x993,x996)+~P19(x991,x994)+P12(f34(x991,x992,x993),f34(x994,x995,x996)) % 0.66/1.01 [100]~P23(x1003,x1006)+~P23(x1001,x1004)+~P15(x1002,x1005)+P15(f20(x1001,x1002,x1003),f20(x1004,x1005,x1006)) % 0.66/1.01 [93]~P22(f29(x931),x932)+P22(x931,f28(x931))+P25(f29(x931),x932,a1)+P18(f12(x931),a9)+~P28(f19(f18(a2,a8)),x931) % 0.66/1.01 [97]~P22(x971,x972)+~P25(x971,x972,a1)+P25(x971,x972,a2)+P18(f12(x971),a9)+~P28(f19(f18(a1,a8)),x971) % 0.66/1.01 [101]~P22(f29(x1011),x1012)+~P25(x1011,f28(x1011),a2)+P25(f29(x1011),x1012,a1)+P18(f12(x1011),a9)+~P28(f19(f18(a2,a8)),x1011) % 0.66/1.01 [102]P22(x1021,f28(x1021))+P18(f12(x1021),a9)+P12(f34(f29(x1021),x1022,x1023),f34(x1021,x1022,x1023))+P29(a5,f33(x1021,x1022,x1023))+~P28(f19(f18(a2,a8)),x1021) % 0.66/1.01 [103]~P25(x1031,f28(x1031),a2)+P12(f34(f29(x1031),x1032,x1033),f34(x1031,x1032,x1033))+P18(f12(x1031),a9)+P29(a5,f33(x1031,x1032,x1033))+~P28(f19(f18(a2,a8)),x1031) % 0.66/1.01 [104]P22(x1041,f28(x1041))+P18(f12(x1041),a9)+P12(f34(f29(x1041),x1042,x1043),f34(x1041,x1042,x1043))+~P28(f19(f18(a2,a8)),x1041)+P23(x1042,f35(a3,f33(x1041,x1042,x1043))) % 0.66/1.01 [105]~P25(x1051,f28(x1051),a2)+P12(f34(f29(x1051),x1052,x1053),f34(x1051,x1052,x1053))+P18(f12(x1051),a9)+~P28(f19(f18(a2,a8)),x1051)+P23(x1052,f35(a3,f33(x1051,x1052,x1053))) % 0.66/1.01 [91]~P25(x916,x914,x915)+P25(x911,x912,x913)+~P13(x914,x912)+~P15(x915,x913)+~P19(x916,x911) % 0.66/1.01 %EqnAxiom % 0.66/1.01 % 0.66/1.01 %------------------------------------------- % 0.66/1.01 cnf(112,plain, % 0.66/1.01 (P10(f14(a2),f14(a1))), % 0.66/1.01 inference(scs_inference,[],[24,25,4,13,45,54])). % 0.66/1.01 cnf(140,plain, % 0.66/1.01 (~P22(a6,f22(f21(a4,a11),a10))+~P25(a6,f22(f21(a4,a11),a10),a1)), % 0.66/1.01 inference(scs_inference,[],[112,13,6,31,28,30,24,66,72,97])). % 0.66/1.01 cnf(190,plain, % 0.66/1.01 (~P22(a6,f22(f21(a4,a11),a10))), % 0.66/1.01 inference(scs_inference,[],[23,140,87])). % 0.66/1.01 cnf(191,plain, % 0.66/1.01 ($false), % 0.66/1.01 inference(scs_inference,[],[190,3,23,84]), % 0.66/1.01 ['proof']). % 0.66/1.01 % SZS output end Proof % 0.66/1.01 % Total time :0.240000s %------------------------------------------------------------------------------