%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN719-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:24 EDT 2024 % Result : Unsatisfiable 0.96s 1.02s % Output : CNFRefutation 0.96s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN719-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.33 % Computer : n020.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Sun Jun 23 19:43:24 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.56 start to proof:theBenchmark % 0.89/1.00 %------------------------------------------- % 0.89/1.00 % File :CSE---1.7 % 0.89/1.00 % Problem :theBenchmark % 0.89/1.00 % Transform :cnf % 0.89/1.00 % Format :tptp:raw % 0.89/1.00 % Command :java -jar mcs_scs.jar %d %s % 0.89/1.00 % 0.96/1.00 % Result :Theorem 0.390000s % 0.96/1.00 % Output :CNFRefutation 0.390000s % 0.96/1.00 %------------------------------------------- % 0.96/1.00 %-------------------------------------------------------------------------- % 0.96/1.00 % File : SYN719-1 : TPTP v8.2.0. Released v2.5.0. % 0.96/1.00 % Domain : Syntactic % 0.96/1.00 % Problem : Harrison problem 4766 % 0.96/1.00 % Version : Especial. % 0.96/1.00 % English : % 0.96/1.01 % 0.96/1.01 % Refs : [Har01] Email to G. Sutcliffe % 0.96/1.01 % Source : [Har01] % 0.96/1.01 % Names : % 0.96/1.01 % 0.96/1.01 % Status : Unsatisfiable % 0.96/1.01 % Rating : 0.00 v7.4.0, 0.17 v7.3.0, 0.00 v5.4.0, 0.06 v5.3.0, 0.15 v5.2.0, 0.00 v2.5.0 % 0.96/1.01 % Syntax : Number of clauses : 126 ( 46 unt; 0 nHn; 84 RR) % 0.96/1.01 % Number of literals : 291 ( 0 equ; 166 neg) % 0.96/1.01 % Maximal clause size : 5 ( 2 avg) % 0.96/1.01 % Maximal term depth : 7 ( 1 avg) % 0.96/1.01 % Number of predicates : 49 ( 49 usr; 0 prp; 2-2 aty) % 0.96/1.01 % Number of functors : 44 ( 44 usr; 21 con; 0-2 aty) % 0.96/1.01 % Number of variables : 310 ( 2 sgn) % 0.96/1.01 % SPC : CNF_UNS_RFO_NEQ_HRN % 0.96/1.01 % 0.96/1.01 % Comments : % 0.96/1.01 %-------------------------------------------------------------------------- % 0.96/1.01 cnf(p10_1,negated_conjecture, % 0.96/1.01 p10(X0,X0) ). % 0.96/1.01 % 0.96/1.01 cnf(p9_2,negated_conjecture, % 0.96/1.01 p9(X261,X261) ). % 0.96/1.01 % 0.96/1.01 cnf(p7_3,negated_conjecture, % 0.96/1.01 p7(X231,X231) ). % 0.96/1.01 % 0.96/1.01 cnf(p63_4,negated_conjecture, % 0.96/1.01 p63(X200,X200) ). % 0.96/1.01 % 0.96/1.01 cnf(p61_5,negated_conjecture, % 0.96/1.01 p61(X197,X197) ). % 0.96/1.01 % 0.96/1.01 cnf(p6_6,negated_conjecture, % 0.96/1.01 p6(X194,X194) ). % 0.96/1.01 % 0.96/1.01 cnf(p59_7,negated_conjecture, % 0.96/1.01 p59(X187,X187) ). % 0.96/1.01 % 0.96/1.01 cnf(p57_8,negated_conjecture, % 0.96/1.01 p57(X180,X180) ). % 0.96/1.01 % 0.96/1.01 cnf(p56_9,negated_conjecture, % 0.96/1.01 p56(X173,X173) ). % 0.96/1.01 % 0.96/1.01 cnf(p55_10,negated_conjecture, % 0.96/1.01 p55(X170,X170) ). % 0.96/1.01 % 0.96/1.01 cnf(p53_11,negated_conjecture, % 0.96/1.01 p53(X163,X163) ). % 0.96/1.01 % 0.96/1.01 cnf(p52_12,negated_conjecture, % 0.96/1.01 p52(X160,X160) ). % 0.96/1.01 % 0.96/1.01 cnf(p50_13,negated_conjecture, % 0.96/1.01 p50(X157,X157) ). % 0.96/1.01 % 0.96/1.01 cnf(p48_14,negated_conjecture, % 0.96/1.01 p48(X154,X154) ). % 0.96/1.01 % 0.96/1.01 cnf(p47_15,negated_conjecture, % 0.96/1.01 p47(X147,X147) ). % 0.96/1.01 % 0.96/1.01 cnf(p45_16,negated_conjecture, % 0.96/1.01 p45(X144,X144) ). % 0.96/1.01 % 0.96/1.01 cnf(p43_17,negated_conjecture, % 0.96/1.01 p43(X137,X137) ). % 0.96/1.01 % 0.96/1.01 cnf(p41_18,negated_conjecture, % 0.96/1.01 p41(X130,X130) ). % 0.96/1.01 % 0.96/1.01 cnf(p4_19,negated_conjecture, % 0.96/1.01 p4(X123,X123) ). % 0.96/1.01 % 0.96/1.01 cnf(p39_20,negated_conjecture, % 0.96/1.01 p39(X116,X116) ). % 0.96/1.01 % 0.96/1.01 cnf(p37_21,negated_conjecture, % 0.96/1.01 p37(X105,X105) ). % 0.96/1.01 % 0.96/1.01 cnf(p35_22,negated_conjecture, % 0.96/1.01 p35(X98,X98) ). % 0.96/1.01 % 0.96/1.01 cnf(p34_23,negated_conjecture, % 0.96/1.01 p34(X87,X87) ). % 0.96/1.01 % 0.96/1.01 cnf(p33_24,negated_conjecture, % 0.96/1.01 p33(X84,X84) ). % 0.96/1.01 % 0.96/1.01 cnf(p31_25,negated_conjecture, % 0.96/1.01 p31(X81,X81) ). % 0.96/1.01 % 0.96/1.01 cnf(p3_26,negated_conjecture, % 0.96/1.01 p3(X74,X74) ). % 0.96/1.01 % 0.96/1.01 cnf(p29_27,negated_conjecture, % 0.96/1.01 p29(X67,X67) ). % 0.96/1.01 % 0.96/1.01 cnf(p28_28,negated_conjecture, % 0.96/1.01 p28(X60,X60) ). % 0.96/1.01 % 0.96/1.01 cnf(p27_29,negated_conjecture, % 0.96/1.01 p27(X57,X57) ). % 0.96/1.01 % 0.96/1.01 cnf(p25_30,negated_conjecture, % 0.96/1.01 p25(X54,X54) ). % 0.96/1.01 % 0.96/1.01 cnf(p24_31,negated_conjecture, % 0.96/1.01 p24(X51,X51) ). % 0.96/1.01 % 0.96/1.01 cnf(p22_32,negated_conjecture, % 0.96/1.01 p22(X44,X44) ). % 0.96/1.01 % 0.96/1.01 cnf(p20_33,negated_conjecture, % 0.96/1.01 p20(X41,X41) ). % 0.96/1.01 % 0.96/1.01 cnf(p2_34,negated_conjecture, % 0.96/1.01 p2(X38,X38) ). % 0.96/1.01 % 0.96/1.01 cnf(p18_35,negated_conjecture, % 0.96/1.01 p18(X35,X35) ). % 0.96/1.01 % 0.96/1.01 cnf(p17_36,negated_conjecture, % 0.96/1.01 p17(X28,X28) ). % 0.96/1.01 % 0.96/1.01 cnf(p15_37,negated_conjecture, % 0.96/1.01 p15(X21,X21) ). % 0.96/1.01 % 0.96/1.01 cnf(p14_38,negated_conjecture, % 0.96/1.01 p14(X13,X13) ). % 0.96/1.01 % 0.96/1.01 cnf(p13_39,negated_conjecture, % 0.96/1.01 p13(X10,X10) ). % 0.96/1.01 % 0.96/1.01 cnf(p11_40,negated_conjecture, % 0.96/1.01 p11(X3,X3) ). % 0.96/1.01 % 0.96/1.01 cnf(p66_41,negated_conjecture, % 0.96/1.01 p66(f12(c78,c77),c79) ). % 0.96/1.01 % 0.96/1.01 cnf(p67_42,negated_conjecture, % 0.96/1.01 p67(f16(c80,c81),c82) ). % 0.96/1.01 % 0.96/1.01 cnf(p70_43,negated_conjecture, % 0.96/1.01 p70(f30(c88,X242),f38(c85,X243)) ). % 0.96/1.01 % 0.96/1.01 cnf(p65_44,negated_conjecture, % 0.96/1.01 p65(f5(c74,f8(c75,c76)),c77) ). % 0.96/1.01 % 0.96/1.01 cnf(p14_45,negated_conjecture, % 0.96/1.01 p14(f23(f26(c84,c85),X20),X20) ). % 0.96/1.01 % 0.96/1.01 cnf(not_p68_46,negated_conjecture, % 0.96/1.01 ~ p68(f19(f21(c83,c77),c79),c81) ). % 0.96/1.01 % 0.96/1.01 cnf(p73_47,negated_conjecture, % 0.96/1.01 ( p73(X256,X255) % 0.96/1.01 | ~ p72(f58(c90,X255),X256) ) ). % 0.96/1.01 % 0.96/1.01 cnf(p68_48,negated_conjecture, % 0.96/1.01 ( p68(X216,X215) % 0.96/1.01 | ~ p67(f16(c80,X215),X216) ) ). % 0.96/1.01 % 0.96/1.01 cnf(p70_49,negated_conjecture, % 0.96/1.01 ( p70(X230,X229) % 0.96/1.01 | ~ p69(f36(c86,X229),X230) ) ). % 0.96/1.01 % 0.96/1.01 cnf(p67_50,negated_conjecture, % 0.96/1.01 ( p67(f16(c80,X215),X216) % 0.96/1.01 | ~ p68(X216,X215) ) ). % 0.96/1.01 % 0.96/1.01 cnf(p72_51,negated_conjecture, % 0.96/1.01 ( p72(f58(c90,X255),X256) % 0.96/1.01 | ~ p73(X256,X255) ) ). % 0.96/1.01 % 0.96/1.01 cnf(p69_52,negated_conjecture, % 0.96/1.01 ( p69(f36(c86,X229),X230) % 0.96/1.01 | ~ p70(X230,X229) ) ). % 0.96/1.01 % 0.96/1.01 cnf(p10_53,negated_conjecture, % 0.96/1.01 ( p10(X1,X2) % 0.96/1.01 | ~ p10(X0,X1) % 0.96/1.01 | ~ p10(X0,X2) ) ). % 0.96/1.01 % 0.96/1.01 cnf(p9_54,negated_conjecture, % 0.96/1.01 ( p9(X262,X263) % 0.96/1.01 | ~ p9(X261,X262) % 0.96/1.01 | ~ p9(X261,X263) ) ). % 0.96/1.01 % 0.96/1.01 cnf(p7_55,negated_conjecture, % 0.96/1.01 ( p7(X232,X233) % 0.96/1.01 | ~ p7(X231,X232) % 0.96/1.01 | ~ p7(X231,X233) ) ). % 0.96/1.01 % 0.96/1.01 cnf(p63_56,negated_conjecture, % 0.96/1.01 ( p63(X201,X202) % 0.96/1.01 | ~ p63(X200,X201) % 0.96/1.01 | ~ p63(X200,X202) ) ). % 0.96/1.01 % 0.96/1.01 cnf(p61_57,negated_conjecture, % 0.96/1.01 ( p61(X198,X199) % 0.96/1.01 | ~ p61(X197,X198) % 0.96/1.01 | ~ p61(X197,X199) ) ). % 0.96/1.01 % 0.96/1.01 cnf(p6_58,negated_conjecture, % 0.96/1.01 ( p6(X195,X196) % 0.96/1.01 | ~ p6(X194,X195) % 0.96/1.01 | ~ p6(X194,X196) ) ). % 0.96/1.01 % 0.96/1.01 cnf(p59_59,negated_conjecture, % 0.96/1.01 ( p59(X188,X189) % 0.96/1.01 | ~ p59(X187,X188) % 0.96/1.01 | ~ p59(X187,X189) ) ). % 0.96/1.01 % 0.96/1.01 cnf(p57_60,negated_conjecture, % 0.96/1.01 ( p57(X181,X182) % 0.96/1.01 | ~ p57(X180,X181) % 0.96/1.01 | ~ p57(X180,X182) ) ). % 0.96/1.01 % 0.96/1.01 cnf(p56_61,negated_conjecture, % 0.96/1.01 ( p56(X174,X175) % 0.96/1.01 | ~ p56(X173,X174) % 0.96/1.01 | ~ p56(X173,X175) ) ). % 0.96/1.01 % 0.96/1.01 cnf(p55_62,negated_conjecture, % 0.96/1.01 ( p55(X171,X172) % 0.96/1.01 | ~ p55(X170,X171) % 0.96/1.01 | ~ p55(X170,X172) ) ). % 0.96/1.01 % 0.96/1.01 cnf(p53_63,negated_conjecture, % 0.96/1.01 ( p53(X164,X165) % 0.96/1.01 | ~ p53(X163,X164) % 0.96/1.01 | ~ p53(X163,X165) ) ). % 0.96/1.01 % 0.96/1.01 cnf(p52_64,negated_conjecture, % 0.96/1.01 ( p52(X161,X162) % 0.96/1.01 | ~ p52(X160,X161) % 0.96/1.01 | ~ p52(X160,X162) ) ). % 0.96/1.01 % 0.96/1.01 cnf(p50_65,negated_conjecture, % 0.96/1.01 ( p50(X158,X159) % 0.96/1.01 | ~ p50(X157,X158) % 0.96/1.01 | ~ p50(X157,X159) ) ). % 0.96/1.01 % 0.96/1.01 cnf(p48_66,negated_conjecture, % 0.96/1.01 ( p48(X155,X156) % 0.96/1.01 | ~ p48(X154,X155) % 0.96/1.01 | ~ p48(X154,X156) ) ). % 0.96/1.01 % 0.96/1.01 cnf(p47_67,negated_conjecture, % 0.96/1.01 ( p47(X148,X149) % 0.96/1.01 | ~ p47(X147,X148) % 0.96/1.01 | ~ p47(X147,X149) ) ). % 0.96/1.01 % 0.96/1.01 cnf(p45_68,negated_conjecture, % 0.96/1.01 ( p45(X145,X146) % 0.96/1.01 | ~ p45(X144,X145) % 0.96/1.01 | ~ p45(X144,X146) ) ). % 0.96/1.01 % 0.96/1.01 cnf(p43_69,negated_conjecture, % 0.96/1.02 ( p43(X138,X139) % 0.96/1.02 | ~ p43(X137,X138) % 0.96/1.02 | ~ p43(X137,X139) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p41_70,negated_conjecture, % 0.96/1.02 ( p41(X131,X132) % 0.96/1.02 | ~ p41(X130,X131) % 0.96/1.02 | ~ p41(X130,X132) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p4_71,negated_conjecture, % 0.96/1.02 ( p4(X124,X125) % 0.96/1.02 | ~ p4(X123,X124) % 0.96/1.02 | ~ p4(X123,X125) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p39_72,negated_conjecture, % 0.96/1.02 ( p39(X117,X118) % 0.96/1.02 | ~ p39(X116,X117) % 0.96/1.02 | ~ p39(X116,X118) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p37_73,negated_conjecture, % 0.96/1.02 ( p37(X106,X107) % 0.96/1.02 | ~ p37(X105,X106) % 0.96/1.02 | ~ p37(X105,X107) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p35_74,negated_conjecture, % 0.96/1.02 ( p35(X99,X100) % 0.96/1.02 | ~ p35(X98,X99) % 0.96/1.02 | ~ p35(X98,X100) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p34_75,negated_conjecture, % 0.96/1.02 ( p34(X88,X89) % 0.96/1.02 | ~ p34(X87,X88) % 0.96/1.02 | ~ p34(X87,X89) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p33_76,negated_conjecture, % 0.96/1.02 ( p33(X85,X86) % 0.96/1.02 | ~ p33(X84,X85) % 0.96/1.02 | ~ p33(X84,X86) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p31_77,negated_conjecture, % 0.96/1.02 ( p31(X82,X83) % 0.96/1.02 | ~ p31(X81,X82) % 0.96/1.02 | ~ p31(X81,X83) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p3_78,negated_conjecture, % 0.96/1.02 ( p3(X75,X76) % 0.96/1.02 | ~ p3(X74,X75) % 0.96/1.02 | ~ p3(X74,X76) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p29_79,negated_conjecture, % 0.96/1.02 ( p29(X68,X69) % 0.96/1.02 | ~ p29(X67,X68) % 0.96/1.02 | ~ p29(X67,X69) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p28_80,negated_conjecture, % 0.96/1.02 ( p28(X61,X62) % 0.96/1.02 | ~ p28(X60,X61) % 0.96/1.02 | ~ p28(X60,X62) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p27_81,negated_conjecture, % 0.96/1.02 ( p27(X58,X59) % 0.96/1.02 | ~ p27(X57,X58) % 0.96/1.02 | ~ p27(X57,X59) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p25_82,negated_conjecture, % 0.96/1.02 ( p25(X55,X56) % 0.96/1.02 | ~ p25(X54,X55) % 0.96/1.02 | ~ p25(X54,X56) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p24_83,negated_conjecture, % 0.96/1.02 ( p24(X52,X53) % 0.96/1.02 | ~ p24(X51,X52) % 0.96/1.02 | ~ p24(X51,X53) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p22_84,negated_conjecture, % 0.96/1.02 ( p22(X45,X46) % 0.96/1.02 | ~ p22(X44,X45) % 0.96/1.02 | ~ p22(X44,X46) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p20_85,negated_conjecture, % 0.96/1.02 ( p20(X42,X43) % 0.96/1.02 | ~ p20(X41,X42) % 0.96/1.02 | ~ p20(X41,X43) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p2_86,negated_conjecture, % 0.96/1.02 ( p2(X39,X40) % 0.96/1.02 | ~ p2(X38,X39) % 0.96/1.02 | ~ p2(X38,X40) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p18_87,negated_conjecture, % 0.96/1.02 ( p18(X36,X37) % 0.96/1.02 | ~ p18(X35,X36) % 0.96/1.02 | ~ p18(X35,X37) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p17_88,negated_conjecture, % 0.96/1.02 ( p17(X29,X30) % 0.96/1.02 | ~ p17(X28,X29) % 0.96/1.02 | ~ p17(X28,X30) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p15_89,negated_conjecture, % 0.96/1.02 ( p15(X22,X23) % 0.96/1.02 | ~ p15(X21,X22) % 0.96/1.02 | ~ p15(X21,X23) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p14_90,negated_conjecture, % 0.96/1.02 ( p14(X14,X15) % 0.96/1.02 | ~ p14(X13,X14) % 0.96/1.02 | ~ p14(X13,X15) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p13_91,negated_conjecture, % 0.96/1.02 ( p13(X11,X12) % 0.96/1.02 | ~ p13(X10,X11) % 0.96/1.02 | ~ p13(X10,X12) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p11_92,negated_conjecture, % 0.96/1.02 ( p11(X4,X5) % 0.96/1.02 | ~ p11(X3,X4) % 0.96/1.02 | ~ p11(X3,X5) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p73_93,negated_conjecture, % 0.96/1.02 ( p73(X257,X258) % 0.96/1.02 | ~ p56(X260,X258) % 0.96/1.02 | ~ p73(X259,X260) % 0.96/1.02 | ~ p28(X259,X257) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p65_94,negated_conjecture, % 0.96/1.02 ( p65(X203,X204) % 0.96/1.02 | ~ p4(X206,X203) % 0.96/1.02 | ~ p65(X206,X205) % 0.96/1.02 | ~ p10(X205,X204) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p66_95,negated_conjecture, % 0.96/1.02 ( p66(X207,X208) % 0.96/1.02 | ~ p18(X210,X208) % 0.96/1.02 | ~ p66(X209,X210) % 0.96/1.02 | ~ p11(X209,X207) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p67_96,negated_conjecture, % 0.96/1.02 ( p67(X211,X212) % 0.96/1.02 | ~ p67(X213,X214) % 0.96/1.02 | ~ p7(X214,X212) % 0.96/1.02 | ~ p15(X213,X211) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p68_97,negated_conjecture, % 0.96/1.02 ( p68(X217,X218) % 0.96/1.02 | ~ p68(X220,X219) % 0.96/1.02 | ~ p7(X220,X217) % 0.96/1.02 | ~ p14(X219,X218) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p69_98,negated_conjecture, % 0.96/1.02 ( p69(X225,X226) % 0.96/1.02 | ~ p35(X228,X225) % 0.96/1.02 | ~ p69(X228,X227) % 0.96/1.02 | ~ p29(X227,X226) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p70_99,negated_conjecture, % 0.96/1.02 ( p70(X238,X239) % 0.96/1.02 | ~ p34(X241,X239) % 0.96/1.02 | ~ p70(X240,X241) % 0.96/1.02 | ~ p29(X240,X238) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p71_100,negated_conjecture, % 0.96/1.02 ( p71(X247,X248) % 0.96/1.02 | ~ p53(X250,X247) % 0.96/1.02 | ~ p71(X250,X249) % 0.96/1.02 | ~ p48(X249,X248) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p72_101,negated_conjecture, % 0.96/1.02 ( p72(X251,X252) % 0.96/1.02 | ~ p57(X254,X251) % 0.96/1.02 | ~ p72(X254,X253) % 0.96/1.02 | ~ p28(X253,X252) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p11_102,negated_conjecture, % 0.96/1.02 ( p11(f12(X6,X7),f12(X8,X9)) % 0.96/1.02 | ~ p10(X7,X9) % 0.96/1.02 | ~ p9(X6,X8) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p7_103,negated_conjecture, % 0.96/1.02 ( p7(f19(X234,X235),f19(X236,X237)) % 0.96/1.02 | ~ p17(X234,X236) % 0.96/1.02 | ~ p18(X235,X237) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p59_104,negated_conjecture, % 0.96/1.02 ( p59(f64(X190,X191),f64(X192,X193)) % 0.96/1.02 | ~ p37(X191,X193) % 0.96/1.02 | ~ p63(X190,X192) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p57_105,negated_conjecture, % 0.96/1.02 ( p57(f58(X183,X184),f58(X185,X186)) % 0.96/1.02 | ~ p55(X183,X185) % 0.96/1.02 | ~ p56(X184,X186) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p56_106,negated_conjecture, % 0.96/1.02 ( p56(f60(X176,X177),f60(X178,X179)) % 0.96/1.02 | ~ p37(X177,X179) % 0.96/1.02 | ~ p59(X176,X178) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p53_107,negated_conjecture, % 0.96/1.02 ( p53(f54(X166,X167),f54(X168,X169)) % 0.96/1.02 | ~ p29(X167,X169) % 0.96/1.02 | ~ p52(X166,X168) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p47_108,negated_conjecture, % 0.96/1.02 ( p47(f51(X150,X151),f51(X152,X153)) % 0.96/1.02 | ~ p37(X151,X153) % 0.96/1.02 | ~ p50(X150,X152) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p43_109,negated_conjecture, % 0.96/1.02 ( p43(f46(X140,X141),f46(X142,X143)) % 0.96/1.02 | ~ p18(X141,X143) % 0.96/1.02 | ~ p45(X140,X142) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p41_110,negated_conjecture, % 0.96/1.02 ( p41(f44(X133,X134),f44(X135,X136)) % 0.96/1.02 | ~ p14(X134,X136) % 0.96/1.02 | ~ p43(X133,X135) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p4_111,negated_conjecture, % 0.96/1.02 ( p4(f5(X126,X127),f5(X128,X129)) % 0.96/1.02 | ~ p2(X126,X128) % 0.96/1.02 | ~ p3(X127,X129) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p39_112,negated_conjecture, % 0.96/1.02 ( p39(f42(X119,X120),f42(X121,X122)) % 0.96/1.02 | ~ p25(X120,X122) % 0.96/1.02 | ~ p41(X119,X121) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p37_113,negated_conjecture, % 0.96/1.02 ( p37(f62(X112,X113),f62(X114,X115)) % 0.96/1.02 | ~ p48(X113,X115) % 0.96/1.02 | ~ p61(X112,X114) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p37_114,negated_conjecture, % 0.96/1.02 ( p37(f40(X108,X109),f40(X110,X111)) % 0.96/1.02 | ~ p14(X109,X111) % 0.96/1.02 | ~ p39(X108,X110) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p35_115,negated_conjecture, % 0.96/1.02 ( p35(f36(X101,X102),f36(X103,X104)) % 0.96/1.02 | ~ p33(X101,X103) % 0.96/1.02 | ~ p34(X102,X104) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p34_116,negated_conjecture, % 0.96/1.02 ( p34(f49(X94,X95),f49(X96,X97)) % 0.96/1.02 | ~ p47(X94,X96) % 0.96/1.02 | ~ p48(X95,X97) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p34_117,negated_conjecture, % 0.96/1.02 ( p34(f38(X90,X91),f38(X92,X93)) % 0.96/1.02 | ~ p25(X90,X92) % 0.96/1.02 | ~ p37(X91,X93) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p3_118,negated_conjecture, % 0.96/1.02 ( p3(f8(X77,X78),f8(X79,X80)) % 0.96/1.02 | ~ p6(X77,X79) % 0.96/1.02 | ~ p7(X78,X80) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p29_119,negated_conjecture, % 0.96/1.02 ( p29(f30(X70,X71),f30(X72,X73)) % 0.96/1.02 | ~ p27(X70,X72) % 0.96/1.02 | ~ p28(X71,X73) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p28_120,negated_conjecture, % 0.96/1.02 ( p28(f32(X63,X64),f32(X65,X66)) % 0.96/1.02 | ~ p3(X64,X66) % 0.96/1.02 | ~ p31(X63,X65) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p22_121,negated_conjecture, % 0.96/1.02 ( p22(f26(X47,X48),f26(X49,X50)) % 0.96/1.02 | ~ p24(X47,X49) % 0.96/1.02 | ~ p25(X48,X50) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p17_122,negated_conjecture, % 0.96/1.02 ( p17(f21(X31,X32),f21(X33,X34)) % 0.96/1.02 | ~ p10(X32,X34) % 0.96/1.02 | ~ p20(X31,X33) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p15_123,negated_conjecture, % 0.96/1.02 ( p15(f16(X24,X25),f16(X26,X27)) % 0.96/1.02 | ~ p13(X24,X26) % 0.96/1.02 | ~ p14(X25,X27) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p14_124,negated_conjecture, % 0.96/1.02 ( p14(f23(X16,X17),f23(X18,X19)) % 0.96/1.02 | ~ p14(X17,X19) % 0.96/1.02 | ~ p22(X16,X18) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p70_125,negated_conjecture, % 0.96/1.02 ( p70(f30(c88,X244),f49(f51(c94,X245),X246)) % 0.96/1.02 | ~ p71(f54(c93,f30(c88,X244)),X246) % 0.96/1.02 | ~ p72(f58(c90,f60(f64(c91,X245),f62(c92,X246))),X244) ) ). % 0.96/1.02 % 0.96/1.02 cnf(p68_126,negated_conjecture, % 0.96/1.02 ( p68(f19(f21(c83,c77),X221),X222) % 0.96/1.02 | ~ p67(f16(c80,X224),c82) % 0.96/1.02 | ~ p66(f12(c78,c77),X221) % 0.96/1.02 | ~ p14(X222,f23(f26(c84,X223),X224)) % 0.96/1.02 | ~ p69(f36(c86,f38(X223,f40(f42(f44(f46(c87,X221),X222),X223),X224))),f30(c88,f32(c89,f8(c75,c76)))) ) ). % 0.96/1.02 % 0.96/1.02 %-------------------------------------------------------------------------- % 0.96/1.02 %------------------------------------------- % 0.96/1.02 % Proof found % 0.96/1.02 % SZS status Theorem for theBenchmark % 0.96/1.02 % SZS output start Proof % 0.96/1.02 %ClaNum:126(EqnAxiom:0) % 0.96/1.02 %VarNum:624(SingletonVarNum:310) % 0.96/1.02 %MaxLitNum:5 % 0.96/1.02 %MaxfuncDepth:6 % 0.96/1.02 %SharedTerms:34 % 0.96/1.02 %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 114 115 116 117 118 119 120 121 122 123 124 125 126 % 0.96/1.02 %singleGoalClaCount:46 % 0.96/1.02 [41]P41(f6(a1,a2),a7) % 0.96/1.02 [42]P43(f23(a8,a9),a10) % 0.96/1.02 [44]P42(f33(a3,f32(a4,a5)),a2) % 0.96/1.02 [46]~P44(f28(f27(a14,a2),a7),a9) % 0.96/1.02 [1]P1(x11,x11) % 0.96/1.02 [2]P2(x21,x21) % 0.96/1.02 [3]P3(x31,x31) % 0.96/1.02 [4]P4(x41,x41) % 0.96/1.02 [5]P5(x51,x51) % 0.96/1.02 [6]P6(x61,x61) % 0.96/1.02 [7]P7(x71,x71) % 0.96/1.02 [8]P8(x81,x81) % 0.96/1.02 [9]P9(x91,x91) % 0.96/1.02 [10]P10(x101,x101) % 0.96/1.02 [11]P11(x111,x111) % 0.96/1.02 [12]P12(x121,x121) % 0.96/1.02 [13]P13(x131,x131) % 0.96/1.02 [14]P14(x141,x141) % 0.96/1.02 [15]P15(x151,x151) % 0.96/1.02 [16]P16(x161,x161) % 0.96/1.02 [17]P17(x171,x171) % 0.96/1.02 [18]P18(x181,x181) % 0.96/1.02 [19]P19(x191,x191) % 0.96/1.02 [20]P20(x201,x201) % 0.96/1.02 [21]P21(x211,x211) % 0.96/1.02 [22]P22(x221,x221) % 0.96/1.02 [23]P23(x231,x231) % 0.96/1.02 [24]P24(x241,x241) % 0.96/1.02 [25]P25(x251,x251) % 0.96/1.02 [26]P26(x261,x261) % 0.96/1.02 [27]P27(x271,x271) % 0.96/1.02 [28]P28(x281,x281) % 0.96/1.02 [29]P29(x291,x291) % 0.96/1.02 [30]P30(x301,x301) % 0.96/1.02 [31]P31(x311,x311) % 0.96/1.02 [32]P32(x321,x321) % 0.96/1.02 [33]P33(x331,x331) % 0.96/1.02 [34]P34(x341,x341) % 0.96/1.02 [35]P35(x351,x351) % 0.96/1.02 [36]P36(x361,x361) % 0.96/1.02 [37]P37(x371,x371) % 0.96/1.02 [38]P38(x381,x381) % 0.96/1.02 [39]P39(x391,x391) % 0.96/1.02 [40]P40(x401,x401) % 0.96/1.02 [45]P38(f26(f25(a13,a12),x451),x451) % 0.96/1.02 [43]P46(f24(a11,x431),f29(a12,x432)) % 0.96/1.02 [87]~P44(x872,x871)+P43(f23(a8,x871),x872) % 0.96/1.02 [88]~P49(x882,x881)+P47(f39(a17,x881),x882) % 0.96/1.02 [89]~P46(x892,x891)+P45(f30(a15,x891),x892) % 0.96/1.02 [90]P46(x901,x902)+~P45(f30(a15,x902),x901) % 0.96/1.02 [91]P44(x911,x912)+~P43(f23(a8,x912),x911) % 0.96/1.02 [92]P49(x921,x922)+~P47(f39(a17,x922),x921) % 0.96/1.03 [47]~P1(x473,x471)+P1(x471,x472)+~P1(x473,x472) % 0.96/1.03 [48]~P2(x483,x481)+P2(x481,x482)+~P2(x483,x482) % 0.96/1.03 [49]~P3(x493,x491)+P3(x491,x492)+~P3(x493,x492) % 0.96/1.03 [50]~P4(x503,x501)+P4(x501,x502)+~P4(x503,x502) % 0.96/1.03 [51]~P5(x513,x511)+P5(x511,x512)+~P5(x513,x512) % 0.96/1.03 [52]~P6(x523,x521)+P6(x521,x522)+~P6(x523,x522) % 0.96/1.03 [53]~P7(x533,x531)+P7(x531,x532)+~P7(x533,x532) % 0.96/1.03 [54]~P8(x543,x541)+P8(x541,x542)+~P8(x543,x542) % 0.96/1.03 [55]~P9(x553,x551)+P9(x551,x552)+~P9(x553,x552) % 0.96/1.03 [56]~P10(x563,x561)+P10(x561,x562)+~P10(x563,x562) % 0.96/1.03 [57]~P11(x573,x571)+P11(x571,x572)+~P11(x573,x572) % 0.96/1.03 [58]~P12(x583,x581)+P12(x581,x582)+~P12(x583,x582) % 0.96/1.03 [59]~P13(x593,x591)+P13(x591,x592)+~P13(x593,x592) % 0.96/1.03 [60]~P14(x603,x601)+P14(x601,x602)+~P14(x603,x602) % 0.96/1.03 [61]~P15(x613,x611)+P15(x611,x612)+~P15(x613,x612) % 0.96/1.03 [62]~P16(x623,x621)+P16(x621,x622)+~P16(x623,x622) % 0.96/1.03 [63]~P17(x633,x631)+P17(x631,x632)+~P17(x633,x632) % 0.96/1.03 [64]~P18(x643,x641)+P18(x641,x642)+~P18(x643,x642) % 0.96/1.03 [65]~P19(x653,x651)+P19(x651,x652)+~P19(x653,x652) % 0.96/1.03 [66]~P20(x663,x661)+P20(x661,x662)+~P20(x663,x662) % 0.96/1.03 [67]~P21(x673,x671)+P21(x671,x672)+~P21(x673,x672) % 0.96/1.03 [68]~P22(x683,x681)+P22(x681,x682)+~P22(x683,x682) % 0.96/1.03 [69]~P23(x693,x691)+P23(x691,x692)+~P23(x693,x692) % 0.96/1.03 [70]~P24(x703,x701)+P24(x701,x702)+~P24(x703,x702) % 0.96/1.03 [71]~P25(x713,x711)+P25(x711,x712)+~P25(x713,x712) % 0.96/1.03 [72]~P26(x723,x721)+P26(x721,x722)+~P26(x723,x722) % 0.96/1.03 [73]~P27(x733,x731)+P27(x731,x732)+~P27(x733,x732) % 0.96/1.03 [74]~P28(x743,x741)+P28(x741,x742)+~P28(x743,x742) % 0.96/1.03 [75]~P29(x753,x751)+P29(x751,x752)+~P29(x753,x752) % 0.96/1.03 [76]~P30(x763,x761)+P30(x761,x762)+~P30(x763,x762) % 0.96/1.03 [77]~P31(x773,x771)+P31(x771,x772)+~P31(x773,x772) % 0.96/1.03 [78]~P32(x783,x781)+P32(x781,x782)+~P32(x783,x782) % 0.96/1.03 [79]~P33(x793,x791)+P33(x791,x792)+~P33(x793,x792) % 0.96/1.03 [80]~P34(x803,x801)+P34(x801,x802)+~P34(x803,x802) % 0.96/1.03 [81]~P35(x813,x811)+P35(x811,x812)+~P35(x813,x812) % 0.96/1.03 [82]~P36(x823,x821)+P36(x821,x822)+~P36(x823,x822) % 0.96/1.03 [83]~P37(x833,x831)+P37(x831,x832)+~P37(x833,x832) % 0.96/1.03 [84]~P38(x843,x841)+P38(x841,x842)+~P38(x843,x842) % 0.96/1.03 [85]~P39(x853,x851)+P39(x851,x852)+~P39(x853,x852) % 0.96/1.03 [86]~P40(x863,x861)+P40(x861,x862)+~P40(x863,x862) % 0.96/1.03 [125]~P48(f40(a20,f24(a11,x1251)),x1253)+P46(f24(a11,x1251),f38(f41(a19,x1252),x1253))+~P47(f39(a17,f43(f42(a21,x1252),f44(a22,x1253))),x1251) % 0.96/1.03 [102]~P35(x1022,x1024)+~P36(x1021,x1023)+P3(f28(x1021,x1022),f28(x1023,x1024)) % 0.96/1.03 [103]~P4(x1031,x1033)+~P21(x1032,x1034)+P7(f42(x1031,x1032),f42(x1033,x1034)) % 0.96/1.03 [104]~P9(x1042,x1044)+~P10(x1041,x1043)+P8(f39(x1041,x1042),f39(x1043,x1044)) % 0.96/1.03 [105]~P7(x1051,x1053)+~P21(x1052,x1054)+P9(f43(x1051,x1052),f43(x1053,x1054)) % 0.96/1.03 [106]~P12(x1061,x1063)+~P27(x1062,x1064)+P11(f40(x1061,x1062),f40(x1063,x1064)) % 0.96/1.03 [107]~P13(x1071,x1073)+~P21(x1072,x1074)+P15(f41(x1071,x1072),f41(x1073,x1074)) % 0.96/1.03 [108]~P16(x1081,x1083)+~P35(x1082,x1084)+P17(f34(x1081,x1082),f34(x1083,x1084)) % 0.96/1.03 [109]~P17(x1091,x1093)+~P38(x1092,x1094)+P18(f35(x1091,x1092),f35(x1093,x1094)) % 0.96/1.03 [110]~P26(x1102,x1104)+~P34(x1101,x1103)+P19(f33(x1101,x1102),f33(x1103,x1104)) % 0.96/1.03 [111]~P18(x1111,x1113)+~P30(x1112,x1114)+P20(f36(x1111,x1112),f36(x1113,x1114)) % 0.96/1.03 [112]~P5(x1121,x1123)+~P14(x1122,x1124)+P21(f44(x1121,x1122),f44(x1123,x1124)) % 0.96/1.03 [113]~P20(x1131,x1133)+~P38(x1132,x1134)+P21(f37(x1131,x1132),f37(x1133,x1134)) % 0.96/1.03 [114]~P23(x1142,x1144)+~P24(x1141,x1143)+P22(f30(x1141,x1142),f30(x1143,x1144)) % 0.96/1.03 [115]~P21(x1152,x1154)+~P30(x1151,x1153)+P23(f29(x1151,x1152),f29(x1153,x1154)) % 0.96/1.03 [116]~P14(x1162,x1164)+~P15(x1161,x1163)+P23(f38(x1161,x1162),f38(x1163,x1164)) % 0.96/1.03 [117]~P3(x1172,x1174)+~P6(x1171,x1173)+P26(f32(x1171,x1172),f32(x1173,x1174)) % 0.96/1.03 [118]~P28(x1182,x1184)+~P29(x1181,x1183)+P27(f24(x1181,x1182),f24(x1183,x1184)) % 0.96/1.03 [119]~P25(x1191,x1193)+~P26(x1192,x1194)+P28(f31(x1191,x1192),f31(x1193,x1194)) % 0.96/1.03 [120]~P30(x1202,x1204)+~P31(x1201,x1203)+P32(f25(x1201,x1202),f25(x1203,x1204)) % 0.96/1.03 [121]~P1(x1212,x1214)+~P33(x1211,x1213)+P36(f27(x1211,x1212),f27(x1213,x1214)) % 0.96/1.03 [122]~P38(x1222,x1224)+~P39(x1221,x1223)+P37(f23(x1221,x1222),f23(x1223,x1224)) % 0.96/1.03 [123]~P32(x1231,x1233)+~P38(x1232,x1234)+P38(f26(x1231,x1232),f26(x1233,x1234)) % 0.96/1.03 [124]~P1(x1242,x1244)+~P2(x1241,x1243)+P40(f6(x1241,x1242),f6(x1243,x1244)) % 0.96/1.03 [93]~P41(x934,x933)+P41(x931,x932)+~P35(x933,x932)+~P40(x934,x931) % 0.96/1.03 [94]~P43(x944,x943)+P43(x941,x942)+~P3(x943,x942)+~P37(x944,x941) % 0.96/1.03 [95]~P46(x954,x953)+P46(x951,x952)+~P23(x953,x952)+~P27(x954,x951) % 0.96/1.03 [96]~P42(x964,x963)+P42(x961,x962)+~P1(x963,x962)+~P19(x964,x961) % 0.96/1.03 [97]~P44(x973,x974)+P44(x971,x972)+~P3(x973,x971)+~P38(x974,x972) % 0.96/1.03 [98]~P49(x984,x983)+P49(x981,x982)+~P9(x983,x982)+~P28(x984,x981) % 0.96/1.03 [99]~P47(x993,x994)+P47(x991,x992)+~P8(x993,x991)+~P28(x994,x992) % 0.96/1.03 [100]~P45(x1003,x1004)+P45(x1001,x1002)+~P22(x1003,x1001)+~P27(x1004,x1002) % 0.96/1.03 [101]~P48(x1013,x1014)+P48(x1011,x1012)+~P11(x1013,x1011)+~P14(x1014,x1012) % 0.96/1.03 [126]~P41(f6(a1,a2),x1261)+P44(f28(f27(a14,a2),x1261),x1262)+~P38(x1262,f26(f25(a13,x1264),x1263))+~P43(f23(a8,x1263),a10)+~P45(f30(a15,f29(x1264,f37(f36(f35(f34(a16,x1261),x1262),x1264),x1263))),f24(a11,f31(a18,f32(a4,a5)))) % 0.96/1.03 %EqnAxiom % 0.96/1.03 % 0.96/1.03 %------------------------------------------- % 0.96/1.03 cnf(127,plain, % 0.96/1.03 (P44(a10,a9)), % 0.96/1.03 inference(scs_inference,[],[42,91])). % 0.96/1.03 cnf(142,plain, % 0.96/1.03 (P38(x1421,f26(f25(a13,a12),x1421))), % 0.96/1.03 inference(scs_inference,[],[45,38,84])). % 0.96/1.03 cnf(145,plain, % 0.96/1.03 (~P44(f28(f27(a14,a2),a7),f26(f25(a13,a12),a9))), % 0.96/1.03 inference(scs_inference,[],[3,45,46,38,84,97])). % 0.96/1.03 cnf(151,plain, % 0.96/1.03 (P38(x1511,f26(f25(a13,a12),x1511))), % 0.96/1.03 inference(rename_variables,[],[142])). % 0.96/1.03 cnf(153,plain, % 0.96/1.03 (P44(a10,f26(f25(a13,a12),a9))), % 0.96/1.03 inference(scs_inference,[],[127,142,151,3,45,84,97])). % 0.96/1.03 cnf(250,plain, % 0.96/1.03 (~P45(f30(a15,f29(a12,f37(f36(f35(f34(a16,a7),f26(f25(a13,a12),a9)),a12),f26(f25(a13,a12),a9)))),f24(a11,f31(a18,f32(a4,a5))))), % 0.96/1.03 inference(scs_inference,[],[153,145,142,41,87,126])). % 0.96/1.03 cnf(251,plain, % 0.96/1.03 ($false), % 0.96/1.03 inference(scs_inference,[],[250,43,89]), % 0.96/1.03 ['proof']). % 0.96/1.03 % SZS output end Proof % 0.96/1.03 % Total time :0.390000s %------------------------------------------------------------------------------