%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN708-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:22 EDT 2024 % Result : Unsatisfiable 58.74s 58.93s % Output : CNFRefutation 58.74s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN708-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 : n021.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 23:27:09 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.55 start to proof:theBenchmark % 58.74/58.90 %------------------------------------------- % 58.74/58.90 % File :CSE---1.7 % 58.74/58.90 % Problem :theBenchmark % 58.74/58.90 % Transform :cnf % 58.74/58.90 % Format :tptp:raw % 58.74/58.90 % Command :java -jar mcs_scs.jar %d %s % 58.74/58.90 % 58.74/58.90 % Result :Theorem 58.170000s % 58.74/58.90 % Output :CNFRefutation 58.170000s % 58.74/58.90 %------------------------------------------- % 58.74/58.91 %-------------------------------------------------------------------------- % 58.74/58.91 % File : SYN708-1 : TPTP v8.2.0. Released v2.5.0. % 58.74/58.91 % Domain : Syntactic % 58.74/58.91 % Problem : Harrison problem 4691 % 58.74/58.91 % Version : Especial. % 58.74/58.91 % English : % 58.74/58.91 % 58.74/58.91 % Refs : [Har01] Email to G. Sutcliffe % 58.74/58.91 % Source : [Har01] % 58.74/58.91 % Names : % 58.74/58.91 % 58.74/58.91 % Status : Unsatisfiable % 58.74/58.91 % Rating : 0.27 v8.2.0, 0.29 v8.1.0, 0.50 v6.1.0, 0.64 v6.0.0, 0.56 v5.5.0, 0.62 v5.4.0, 0.61 v5.3.0, 0.65 v5.2.0, 0.69 v5.1.0, 0.62 v5.0.0, 0.53 v4.1.0, 0.60 v4.0.1, 0.71 v3.7.0, 0.57 v3.4.0, 0.40 v3.3.0, 0.33 v3.1.0, 0.17 v2.7.0, 0.25 v2.6.0, 0.17 v2.5.0 % 58.74/58.91 % Syntax : Number of clauses : 83 ( 38 unt; 0 nHn; 76 RR) % 58.74/58.91 % Number of literals : 164 ( 0 equ; 86 neg) % 58.74/58.91 % Maximal clause size : 4 ( 1 avg) % 58.74/58.91 % Maximal term depth : 28 ( 5 avg) % 58.74/58.91 % Number of predicates : 17 ( 17 usr; 0 prp; 1-2 aty) % 58.74/58.91 % Number of functors : 41 ( 41 usr; 17 con; 0-2 aty) % 58.74/58.91 % Number of variables : 132 ( 0 sgn) % 58.74/58.91 % SPC : CNF_UNS_RFO_NEQ_HRN % 58.74/58.91 % 58.74/58.91 % Comments : % 58.74/58.91 %-------------------------------------------------------------------------- % 58.74/58.91 cnf(c56_is_p38_1,negated_conjecture, % 58.74/58.91 p38(c56) ). % 58.74/58.91 % 58.74/58.91 cnf(c56_is_not_p34_2,negated_conjecture, % 58.74/58.91 ~ p34(c56) ). % 58.74/58.91 % 58.74/58.91 cnf(p10_3,negated_conjecture, % 58.74/58.91 p10(X0,X0) ). % 58.74/58.91 % 58.74/58.91 cnf(p9_4,negated_conjecture, % 58.74/58.91 p9(X113,X113) ). % 58.74/58.91 % 58.74/58.91 cnf(p32_5,negated_conjecture, % 58.74/58.91 p32(X74,X74) ). % 58.74/58.91 % 58.74/58.91 cnf(p3_6,negated_conjecture, % 58.74/58.91 p3(X69,X69) ). % 58.74/58.91 % 58.74/58.91 cnf(p2_7,negated_conjecture, % 58.74/58.91 p2(X52,X52) ). % 58.74/58.91 % 58.74/58.91 cnf(p16_8,negated_conjecture, % 58.74/58.91 p16(X18,X18) ). % 58.74/58.91 % 58.74/58.91 cnf(p12_9,negated_conjecture, % 58.74/58.91 p12(X11,X11) ). % 58.74/58.91 % 58.74/58.91 cnf(p33_10,negated_conjecture, % 58.74/58.91 p33(c54,c55) ). % 58.74/58.91 % 58.74/58.91 cnf(not_p35_11,negated_conjecture, % 58.74/58.91 ~ p35(c56,c58) ). % 58.74/58.91 % 58.74/58.91 cnf(not_p35_12,negated_conjecture, % 58.74/58.91 ~ p35(c56,c57) ). % 58.74/58.91 % 58.74/58.91 cnf(p37_13,negated_conjecture, % 58.74/58.91 p37(f15(c56),c48) ). % 58.74/58.91 % 58.74/58.91 cnf(not_p36_14,negated_conjecture, % 58.74/58.91 ~ p36(f15(c56),c47) ). % 58.74/58.91 % 58.74/58.92 cnf(p38_15,negated_conjecture, % 58.74/58.92 ( p38(f15(X27)) % 58.74/58.92 | ~ p38(X27) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p39_16,negated_conjecture, % 58.74/58.92 p39(f18(f19(c56)),f17(c59)) ). % 58.74/58.92 % 58.74/58.92 cnf(p40_17,negated_conjecture, % 58.74/58.92 ( p40(X103) % 58.74/58.92 | ~ p40(X104) % 58.74/58.92 | ~ p10(X104,X103) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p34_18,negated_conjecture, % 58.74/58.92 ( p34(X81) % 58.74/58.92 | ~ p34(X82) % 58.74/58.92 | ~ p10(X82,X81) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p38_19,negated_conjecture, % 58.74/58.92 ( p38(X97) % 58.74/58.92 | ~ p38(X98) % 58.74/58.92 | ~ p10(X98,X97) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p10_20,negated_conjecture, % 58.74/58.92 ( p10(f11(X3),f11(X4)) % 58.74/58.92 | ~ p9(X3,X4) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p9_21,negated_conjecture, % 58.74/58.92 ( p9(f27(X120),f27(X121)) % 58.74/58.92 | ~ p10(X120,X121) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p3_22,negated_conjecture, % 58.74/58.92 ( p3(f4(X72),f4(X73)) % 58.74/58.92 | ~ p2(X72,X73) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p2_23,negated_conjecture, % 58.74/58.92 ( p2(f7(X63),f7(X64)) % 58.74/58.92 | ~ p2(X63,X64) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p2_24,negated_conjecture, % 58.74/58.92 ( p2(f6(X61),f6(X62)) % 58.74/58.92 | ~ p2(X61,X62) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p2_25,negated_conjecture, % 58.74/58.92 ( p2(f5(X59),f5(X60)) % 58.74/58.92 | ~ p2(X59,X60) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p2_26,negated_conjecture, % 58.74/58.92 ( p2(f31(X57),f31(X58)) % 58.74/58.92 | ~ p2(X57,X58) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p2_27,negated_conjecture, % 58.74/58.92 ( p2(f26(X55),f26(X56)) % 58.74/58.92 | ~ p9(X55,X56) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p16_28,negated_conjecture, % 58.74/58.92 ( p16(f28(X42),f28(X43)) % 58.74/58.92 | ~ p16(X42,X43) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p16_29,negated_conjecture, % 58.74/58.92 ( p16(f24(X36),f24(X37)) % 58.74/58.92 | ~ p2(X36,X37) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p16_30,negated_conjecture, % 58.74/58.92 ( p16(f23(X34),f23(X35)) % 58.74/58.92 | ~ p16(X34,X35) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p16_31,negated_conjecture, % 58.74/58.92 ( p16(f22(X32),f22(X33)) % 58.74/58.92 | ~ p16(X32,X33) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p16_32,negated_conjecture, % 58.74/58.92 ( p16(f19(X25),f19(X26)) % 58.74/58.92 | ~ p10(X25,X26) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p16_33,negated_conjecture, % 58.74/58.92 ( p16(f18(X23),f18(X24)) % 58.74/58.92 | ~ p16(X23,X24) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p16_34,negated_conjecture, % 58.74/58.92 ( p16(f17(X21),f17(X22)) % 58.74/58.92 | ~ p12(X21,X22) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p10_35,negated_conjecture, % 58.74/58.92 ( p10(f15(X5),f15(X6)) % 58.74/58.92 | ~ p10(X5,X6) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p16_36,negated_conjecture, % 58.74/58.92 ( p16(f19(f15(X27)),f28(f19(X27))) % 58.74/58.92 | ~ p38(X27) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p10_37,negated_conjecture, % 58.74/58.92 ( p10(X1,X2) % 58.74/58.92 | ~ p10(X0,X1) % 58.74/58.92 | ~ p10(X0,X2) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p9_38,negated_conjecture, % 58.74/58.92 ( p9(X114,X115) % 58.74/58.92 | ~ p9(X113,X114) % 58.74/58.92 | ~ p9(X113,X115) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p32_39,negated_conjecture, % 58.74/58.92 ( p32(X75,X76) % 58.74/58.92 | ~ p32(X74,X75) % 58.74/58.92 | ~ p32(X74,X76) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p3_40,negated_conjecture, % 58.74/58.92 ( p3(X70,X71) % 58.74/58.92 | ~ p3(X69,X71) % 58.74/58.92 | ~ p3(X69,X70) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p2_41,negated_conjecture, % 58.74/58.92 ( p2(X53,X54) % 58.74/58.92 | ~ p2(X52,X53) % 58.74/58.92 | ~ p2(X52,X54) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p16_42,negated_conjecture, % 58.74/58.92 ( p16(X19,X20) % 58.74/58.92 | ~ p16(X18,X19) % 58.74/58.92 | ~ p16(X18,X20) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p12_43,negated_conjecture, % 58.74/58.92 ( p12(X12,X13) % 58.74/58.92 | ~ p12(X11,X12) % 58.74/58.92 | ~ p12(X11,X13) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p3_44,negated_conjecture, % 58.74/58.92 p3(c43,f4(f5(f6(f6(f6(f6(f6(f7(c44))))))))) ). % 58.74/58.92 % 58.74/58.92 cnf(p41_45,negated_conjecture, % 58.74/58.92 p41(f5(c44),f5(f7(f7(f7(f7(f7(f7(f7(c44))))))))) ). % 58.74/58.92 % 58.74/58.92 cnf(p37_46,negated_conjecture, % 58.74/58.92 ( p37(X91,X92) % 58.74/58.92 | ~ p38(X91) % 58.74/58.92 | ~ p38(X92) % 58.74/58.92 | ~ p39(f19(X91),f19(X92)) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p42_47,negated_conjecture, % 58.74/58.92 ( p42(X109,X110) % 58.74/58.92 | ~ p16(X112,X110) % 58.74/58.92 | ~ p42(X111,X112) % 58.74/58.92 | ~ p16(X111,X109) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p33_48,negated_conjecture, % 58.74/58.92 ( p33(X77,X78) % 58.74/58.92 | ~ p32(X80,X78) % 58.74/58.92 | ~ p33(X79,X80) % 58.74/58.92 | ~ p32(X79,X77) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p35_49,negated_conjecture, % 58.74/58.92 ( p35(X83,X84) % 58.74/58.92 | ~ p10(X86,X84) % 58.74/58.92 | ~ p35(X85,X86) % 58.74/58.92 | ~ p10(X85,X83) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p36_50,negated_conjecture, % 58.74/58.92 ( p36(X87,X88) % 58.74/58.92 | ~ p10(X90,X88) % 58.74/58.92 | ~ p36(X89,X90) % 58.74/58.92 | ~ p10(X89,X87) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p37_51,negated_conjecture, % 58.74/58.92 ( p37(X93,X94) % 58.74/58.92 | ~ p10(X96,X94) % 58.74/58.92 | ~ p37(X95,X96) % 58.74/58.92 | ~ p10(X95,X93) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p39_52,negated_conjecture, % 58.74/58.92 ( p39(X99,X100) % 58.74/58.92 | ~ p16(X102,X100) % 58.74/58.92 | ~ p39(X101,X102) % 58.74/58.92 | ~ p16(X101,X99) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p41_53,negated_conjecture, % 58.74/58.92 ( p41(X105,X106) % 58.74/58.92 | ~ p2(X108,X106) % 58.74/58.92 | ~ p41(X107,X108) % 58.74/58.92 | ~ p2(X107,X105) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p39_54,negated_conjecture, % 58.74/58.92 ( p39(f19(X91),f19(X92)) % 58.74/58.92 | ~ p38(X92) % 58.74/58.92 | ~ p38(X91) % 58.74/58.92 | ~ p37(X91,X92) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p9_55,negated_conjecture, % 58.74/58.92 ( p9(f13(X116,X117),f13(X118,X119)) % 58.74/58.92 | ~ p12(X117,X119) % 58.74/58.92 | ~ p2(X116,X118) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p10_56,negated_conjecture, % 58.74/58.92 ( p10(f20(X7,X8),f20(X9,X10)) % 58.74/58.92 | ~ p10(X7,X9) % 58.74/58.92 | ~ p10(X8,X10) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p12_57,negated_conjecture, % 58.74/58.92 ( p12(f14(X14,X15),f14(X16,X17)) % 58.74/58.92 | ~ p2(X14,X16) % 58.74/58.92 | ~ p2(X15,X17) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p16_58,negated_conjecture, % 58.74/58.92 ( p16(f21(X28,X29),f21(X30,X31)) % 58.74/58.92 | ~ p16(X28,X30) % 58.74/58.92 | ~ p16(X29,X31) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p16_59,negated_conjecture, % 58.74/58.92 ( p16(f25(X38,X39),f25(X40,X41)) % 58.74/58.92 | ~ p16(X38,X40) % 58.74/58.92 | ~ p16(X39,X41) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p16_60,negated_conjecture, % 58.74/58.92 ( p16(f29(X44,X45),f29(X46,X47)) % 58.74/58.92 | ~ p16(X44,X46) % 58.74/58.92 | ~ p16(X45,X47) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p16_61,negated_conjecture, % 58.74/58.92 ( p16(f30(X48,X49),f30(X50,X51)) % 58.74/58.92 | ~ p16(X48,X50) % 58.74/58.92 | ~ p2(X49,X51) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p2_62,negated_conjecture, % 58.74/58.92 ( p2(f8(X65,X66),f8(X67,X68)) % 58.74/58.92 | ~ p2(X66,X68) % 58.74/58.92 | ~ p2(X65,X67) ) ). % 58.74/58.92 % 58.74/58.92 cnf(p3_63,negated_conjecture, % 58.74/58.92 p3(c45,f4(f8(f5(f6(f7(c44))),f5(f7(f6(f6(f7(c44)))))))) ). % 58.74/58.92 % 58.74/58.92 cnf(f11_is_p38_64,negated_conjecture, % 58.74/58.92 p38(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44))))) ). % 58.74/58.92 % 58.74/58.92 cnf(p10_65,negated_conjecture, % 58.74/58.92 p10(c46,f11(f13(f5(c44),f14(f5(f7(f7(f7(f7(f7(f7(f7(c44)))))))),f5(c44))))) ). % 58.74/58.92 % 58.74/58.92 cnf(p10_66,negated_conjecture, % 58.74/58.92 p10(c48,f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44))))) ). % 58.74/58.92 % 58.74/58.92 cnf(f20_is_p40_67,negated_conjecture, % 58.74/58.92 p40(f20(f11(f13(f5(c44),f14(f5(f7(f7(f7(f7(f7(f7(f7(c44)))))))),f5(c44)))),c56)) ). % 58.74/58.92 % 58.74/58.92 cnf(f20_is_p38_68,negated_conjecture, % 58.74/58.92 p38(f20(f11(f13(f5(c44),f14(f5(f7(f7(f7(f7(f7(f7(f7(c44)))))))),f5(c44)))),c56)) ). % 58.74/58.92 % 58.74/58.92 cnf(not_p39_69,negated_conjecture, % 58.74/58.92 ~ p39(f28(f19(c56)),f19(f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(c44)))))) ). % 58.74/58.92 % 58.74/58.92 cnf(p10_70,negated_conjecture, % 58.74/58.92 p10(c52,f11(f13(f5(c44),f14(f5(f6(f7(f7(f7(f7(f7(f7(c44)))))))),f5(f6(f6(f7(f6(f6(f6(f7(c44)))))))))))) ). % 58.74/58.92 % 58.74/58.92 cnf(p39_71,negated_conjecture, % 58.74/58.92 p39(f19(f20(f11(f13(f5(c44),f14(f5(f7(f7(f7(f7(f7(f7(f7(c44)))))))),f5(c44)))),c56)),f24(f5(f6(f7(c44))))) ). % 58.74/58.92 % 58.74/58.92 cnf(p39_72,negated_conjecture, % 58.74/58.92 p39(f23(f24(f5(f6(f7(c44))))),f19(f20(f11(f13(f5(c44),f14(f5(f7(f7(f7(f7(f7(f7(f7(c44)))))))),f5(c44)))),c56))) ). % 58.74/58.92 % 58.74/58.92 cnf(p2_73,negated_conjecture, % 58.74/58.92 p2(f26(f27(f20(f11(f13(f5(c44),f14(f5(f7(f7(f7(f7(f7(f7(f7(c44)))))))),f5(c44)))),c56))),f5(f7(f7(f7(f7(f7(f7(f7(c44))))))))) ). % 58.74/58.92 % 58.74/58.92 cnf(p39_74,negated_conjecture, % 58.74/58.93 p39(f21(f19(f11(f13(f5(c44),f14(f5(f7(f7(f7(f7(f7(f7(f7(c44)))))))),f5(c44))))),f19(c56)),f25(f24(f5(f6(f7(c44)))),f23(f24(f5(f6(f6(f7(c44)))))))) ). % 58.74/58.93 % 58.74/58.93 cnf(p39_75,negated_conjecture, % 58.74/58.93 p39(f21(f23(f24(f5(f6(f7(c44))))),f23(f24(f5(f6(f6(f7(c44))))))),f21(f19(f11(f13(f5(c44),f14(f5(f7(f7(f7(f7(f7(f7(f7(c44)))))))),f5(c44))))),f19(c56))) ). % 58.74/58.93 % 58.74/58.93 cnf(p10_76,negated_conjecture, % 58.74/58.93 p10(c50,f11(f13(f5(c44),f14(f5(f7(f6(f6(f7(f7(f7(f7(c44)))))))),f5(f6(f6(f6(f6(f6(f6(f6(f6(f6(f7(f6(f6(f7(f7(f7(f6(f7(f6(f6(f6(f7(f7(c44))))))))))))))))))))))))))) ). % 58.74/58.93 % 58.74/58.93 cnf(p10_77,negated_conjecture, % 58.74/58.93 p10(c53,f11(f13(f5(c44),f14(f5(f6(f6(f7(f7(f7(f7(f7(c44)))))))),f5(f6(f6(f7(f7(f6(f7(f7(f7(f6(f7(f6(f7(f6(f7(f6(f7(f6(f7(f6(f7(f6(f7(c44))))))))))))))))))))))))))) ). % 58.74/58.93 % 58.74/58.93 cnf(p10_78,negated_conjecture, % 58.74/58.93 p10(c51,f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f7(f7(c44)))))))),f5(f6(f7(f7(f7(f6(f6(f6(f7(f6(f7(f7(f7(f7(f7(f6(f7(f7(f7(f7(f7(f7(f7(c44))))))))))))))))))))))))))) ). % 58.74/58.93 % 58.74/58.93 cnf(p10_79,negated_conjecture, % 58.74/58.93 p10(c49,f11(f13(f5(c44),f14(f5(f6(f6(f7(f6(f6(f6(f6(f7(c44))))))))),f5(f7(f7(f6(f7(f7(f7(f6(f6(f6(f7(f6(f7(f6(f7(f6(f7(f6(f6(f6(f7(f7(f7(c44))))))))))))))))))))))))))) ). % 58.74/58.93 % 58.74/58.93 cnf(p10_80,negated_conjecture, % 58.74/58.93 p10(c47,f11(f13(f5(c44),f14(f5(f6(f7(f7(f6(f6(f6(f6(f7(c44))))))))),f5(f6(f7(f6(f7(f7(f7(f6(f7(f7(f7(f6(f7(f6(f7(f7(f6(f6(f6(f7(f7(f7(f6(f7(c44)))))))))))))))))))))))))))) ). % 58.74/58.93 % 58.74/58.93 cnf(p42_81,negated_conjecture, % 58.74/58.93 p42(f29(f30(f24(f5(f6(f7(c44)))),f5(f7(f7(f7(f7(f7(f7(f7(c44))))))))),f30(f24(f5(f6(f7(c44)))),f5(f7(f7(f7(f7(f7(f7(f7(c44)))))))))),f28(f19(f20(f11(f13(f5(c44),f14(f5(f7(f7(f7(f7(f7(f7(f7(c44)))))))),f5(c44)))),c56)))) ). % 58.74/58.93 % 58.74/58.93 cnf(p39_82,negated_conjecture, % 58.74/58.93 p39(f28(f19(f20(f11(f13(f5(c44),f14(f5(f7(f7(f7(f7(f7(f7(f7(c44)))))))),f5(c44)))),c56))),f29(f30(f24(f5(f6(f7(c44)))),f31(f5(f7(f7(f7(f7(f7(f7(f7(c44)))))))))),f30(f24(f5(f6(f7(c44)))),f5(f7(f7(f7(f7(f7(f7(f7(c44))))))))))) ). % 58.74/58.93 % 58.74/58.93 cnf(p16_83,negated_conjecture, % 58.74/58.93 p16(f19(f20(f11(f13(f5(c44),f14(f5(f7(f7(f7(f7(f7(f7(f7(c44)))))))),f5(c44)))),c56)),f21(f21(f19(f11(f13(f5(c44),f14(f5(f7(f7(f7(f7(f7(f7(f7(c44)))))))),f5(c44))))),f19(c56)),f22(f21(f19(f11(f13(f5(c44),f14(f5(f7(f7(f7(f7(f7(f7(f7(c44)))))))),f5(c44))))),f19(c56))))) ). % 58.74/58.93 % 58.74/58.93 %-------------------------------------------------------------------------- % 58.74/58.93 %------------------------------------------- % 58.74/58.93 % Proof found % 58.74/58.93 % SZS status Theorem for theBenchmark % 58.74/58.93 % SZS output start Proof % 58.74/58.93 %ClaNum:83(EqnAxiom:0) % 58.74/58.93 %VarNum:269(SingletonVarNum:132) % 58.74/58.93 %MaxLitNum:4 % 58.74/58.93 %MaxfuncDepth:27 % 58.74/58.93 %SharedTerms:197 % 58.74/58.93 %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 % 58.74/58.93 %singleGoalClaCount:38 % 58.74/58.93 [1]P1(a1) % 58.74/58.93 [2]P2(a2,a14) % 58.74/58.93 [34]~P10(a1) % 58.74/58.93 [35]~P11(a1,a17) % 58.74/58.93 [36]~P11(a1,a18) % 58.74/58.93 [10]P9(f15(a1),a3) % 58.74/58.93 [37]~P12(f15(a1),a8) % 58.74/58.93 [11]P14(f23(f22(a1)),f24(a16)) % 58.74/58.93 [15]P1(f21(f20(f27(a5),f19(f27(f26(f25(f25(f26(f26(f25(f25(a5)))))))),f27(a5))))) % 58.74/58.93 [16]P3(a3,f21(f20(f27(a5),f19(f27(f26(f25(f25(f26(f26(f25(f25(a5)))))))),f27(a5))))) % 58.74/58.93 [17]P3(a7,f21(f20(f27(a5),f19(f27(f25(f25(f25(f25(f25(f25(f25(a5)))))))),f27(a5))))) % 58.74/58.93 [19]P1(f29(f21(f20(f27(a5),f19(f27(f25(f25(f25(f25(f25(f25(f25(a5)))))))),f27(a5)))),a1)) % 58.74/58.93 [20]P16(f29(f21(f20(f27(a5),f19(f27(f25(f25(f25(f25(f25(f25(f25(a5)))))))),f27(a5)))),a1)) % 58.74/58.93 [38]~P14(f39(f22(a1)),f22(f21(f20(f27(a5),f19(f27(f26(f25(f25(f26(f26(f25(f25(a5)))))))),f27(a5)))))) % 58.74/58.93 [21]P14(f22(f29(f21(f20(f27(a5),f19(f27(f25(f25(f25(f25(f25(f25(f25(a5)))))))),f27(a5)))),a1)),f30(f27(f26(f25(a5))))) % 58.74/58.93 [22]P14(f31(f30(f27(f26(f25(a5))))),f22(f29(f21(f20(f27(a5),f19(f27(f25(f25(f25(f25(f25(f25(f25(a5)))))))),f27(a5)))),a1))) % 58.74/58.93 [28]P7(f22(f29(f21(f20(f27(a5),f19(f27(f25(f25(f25(f25(f25(f25(f25(a5)))))))),f27(a5)))),a1)),f32(f32(f22(f21(f20(f27(a5),f19(f27(f25(f25(f25(f25(f25(f25(f25(a5)))))))),f27(a5))))),f22(a1)),f33(f32(f22(f21(f20(f27(a5),f19(f27(f25(f25(f25(f25(f25(f25(f25(a5)))))))),f27(a5))))),f22(a1))))) % 58.74/58.93 [12]P5(a4,f28(f41(f27(f26(f25(a5))),f27(f25(f26(f26(f25(a5)))))))) % 58.74/58.93 [23]P14(f32(f22(f21(f20(f27(a5),f19(f27(f25(f25(f25(f25(f25(f25(f25(a5)))))))),f27(a5))))),f22(a1)),f34(f30(f27(f26(f25(a5)))),f31(f30(f27(f26(f26(f25(a5)))))))) % 58.74/58.93 [24]P14(f32(f31(f30(f27(f26(f25(a5))))),f31(f30(f27(f26(f26(f25(a5))))))),f32(f22(f21(f20(f27(a5),f19(f27(f25(f25(f25(f25(f25(f25(f25(a5)))))))),f27(a5))))),f22(a1))) % 58.74/58.93 [13]P5(a6,f28(f27(f26(f26(f26(f26(f26(f25(a5))))))))) % 58.74/58.93 [14]P15(f27(a5),f27(f25(f25(f25(f25(f25(f25(f25(a5))))))))) % 58.74/58.93 [25]P6(f36(f35(f29(f21(f20(f27(a5),f19(f27(f25(f25(f25(f25(f25(f25(f25(a5)))))))),f27(a5)))),a1))),f27(f25(f25(f25(f25(f25(f25(f25(a5))))))))) % 58.74/58.93 [26]P17(f38(f37(f30(f27(f26(f25(a5)))),f27(f25(f25(f25(f25(f25(f25(f25(a5))))))))),f37(f30(f27(f26(f25(a5)))),f27(f25(f25(f25(f25(f25(f25(f25(a5)))))))))),f39(f22(f29(f21(f20(f27(a5),f19(f27(f25(f25(f25(f25(f25(f25(f25(a5)))))))),f27(a5)))),a1)))) % 58.74/58.93 [27]P14(f39(f22(f29(f21(f20(f27(a5),f19(f27(f25(f25(f25(f25(f25(f25(f25(a5)))))))),f27(a5)))),a1))),f38(f37(f30(f27(f26(f25(a5)))),f40(f27(f25(f25(f25(f25(f25(f25(f25(a5)))))))))),f37(f30(f27(f26(f25(a5)))),f27(f25(f25(f25(f25(f25(f25(f25(a5))))))))))) % 58.74/58.93 [18]P3(a9,f21(f20(f27(a5),f19(f27(f26(f25(f25(f25(f25(f25(f25(a5)))))))),f27(f26(f26(f25(f26(f26(f26(f25(a5)))))))))))) % 58.74/58.93 [29]P3(a10,f21(f20(f27(a5),f19(f27(f25(f26(f26(f25(f25(f25(f25(a5)))))))),f27(f26(f26(f26(f26(f26(f26(f26(f26(f26(f25(f26(f26(f25(f25(f25(f26(f25(f26(f26(f26(f25(f25(a5))))))))))))))))))))))))))) % 58.74/58.93 [30]P3(a13,f21(f20(f27(a5),f19(f27(f26(f26(f25(f25(f25(f25(f25(a5)))))))),f27(f26(f26(f25(f25(f26(f25(f25(f25(f26(f25(f26(f25(f26(f25(f26(f25(f26(f25(f26(f25(f26(f25(a5))))))))))))))))))))))))))) % 58.74/58.93 [31]P3(a12,f21(f20(f27(a5),f19(f27(f26(f25(f25(f26(f26(f25(f25(a5)))))))),f27(f26(f25(f25(f25(f26(f26(f26(f25(f26(f25(f25(f25(f25(f25(f26(f25(f25(f25(f25(f25(f25(f25(a5))))))))))))))))))))))))))) % 58.74/58.93 [32]P3(a11,f21(f20(f27(a5),f19(f27(f26(f26(f25(f26(f26(f26(f26(f25(a5))))))))),f27(f25(f25(f26(f25(f25(f25(f26(f26(f26(f25(f26(f25(f26(f25(f26(f25(f26(f26(f26(f25(f25(f25(a5))))))))))))))))))))))))))) % 58.74/58.93 [33]P3(a8,f21(f20(f27(a5),f19(f27(f26(f25(f25(f26(f26(f26(f26(f25(a5))))))))),f27(f26(f25(f26(f25(f25(f25(f26(f25(f25(f25(f26(f25(f26(f25(f25(f26(f26(f26(f25(f25(f25(f26(f25(a5)))))))))))))))))))))))))))) % 58.74/58.93 [3]P3(x31,x31) % 58.74/58.93 [4]P13(x41,x41) % 58.74/58.93 [5]P4(x51,x51) % 58.74/58.93 [6]P5(x61,x61) % 58.74/58.93 [7]P6(x71,x71) % 58.74/58.93 [8]P7(x81,x81) % 58.74/58.93 [9]P8(x91,x91) % 58.74/58.93 [39]~P1(x391)+P1(f15(x391)) % 58.74/58.93 [59]~P1(x591)+P7(f22(f15(x591)),f39(f22(x591))) % 58.74/58.93 [43]~P3(x431,x432)+P3(f15(x431),f15(x432)) % 58.74/58.93 [44]~P13(x441,x442)+P3(f21(x441),f21(x442)) % 58.74/58.93 [45]~P3(x451,x452)+P13(f35(x451),f35(x452)) % 58.74/58.93 [46]~P6(x461,x462)+P5(f28(x461),f28(x462)) % 58.74/58.93 [47]~P6(x471,x472)+P6(f25(x471),f25(x472)) % 58.74/58.93 [48]~P6(x481,x482)+P6(f26(x481),f26(x482)) % 58.74/58.93 [49]~P6(x491,x492)+P6(f27(x491),f27(x492)) % 58.74/58.93 [50]~P6(x501,x502)+P6(f40(x501),f40(x502)) % 58.74/58.93 [51]~P13(x511,x512)+P6(f36(x511),f36(x512)) % 58.74/58.93 [52]~P3(x521,x522)+P7(f22(x521),f22(x522)) % 58.74/58.93 [53]~P7(x531,x532)+P7(f23(x531),f23(x532)) % 58.74/58.93 [54]~P8(x541,x542)+P7(f24(x541),f24(x542)) % 58.74/58.93 [55]~P7(x551,x552)+P7(f39(x551),f39(x552)) % 58.74/58.93 [56]~P6(x561,x562)+P7(f30(x561),f30(x562)) % 58.74/58.93 [57]~P7(x571,x572)+P7(f31(x571),f31(x572)) % 58.74/58.93 [58]~P7(x581,x582)+P7(f33(x581),f33(x582)) % 58.74/58.93 [40]~P3(x402,x401)+P1(x401)+~P1(x402) % 58.74/58.93 [41]~P3(x412,x411)+P10(x411)+~P10(x412) % 58.74/58.93 [42]~P3(x422,x421)+P16(x421)+~P16(x422) % 58.74/58.93 [60]~P3(x603,x601)+P3(x601,x602)+~P3(x603,x602) % 58.74/58.93 [61]~P13(x613,x611)+P13(x611,x612)+~P13(x613,x612) % 58.74/58.93 [62]~P4(x623,x621)+P4(x621,x622)+~P4(x623,x622) % 58.74/58.93 [63]~P5(x633,x631)+P5(x631,x632)+~P5(x633,x632) % 58.74/58.93 [64]~P6(x643,x641)+P6(x641,x642)+~P6(x643,x642) % 58.74/58.93 [65]~P7(x653,x651)+P7(x651,x652)+~P7(x653,x652) % 58.74/58.93 [66]~P8(x663,x661)+P8(x661,x662)+~P8(x663,x662) % 58.74/58.93 [76]~P3(x762,x764)+~P3(x761,x763)+P3(f29(x761,x762),f29(x763,x764)) % 58.74/58.93 [77]~P6(x771,x773)+~P8(x772,x774)+P13(f20(x771,x772),f20(x773,x774)) % 58.74/58.93 [78]~P6(x782,x784)+~P6(x781,x783)+P6(f41(x781,x782),f41(x783,x784)) % 58.74/58.93 [79]~P7(x792,x794)+~P7(x791,x793)+P7(f32(x791,x792),f32(x793,x794)) % 58.74/58.93 [80]~P7(x802,x804)+~P7(x801,x803)+P7(f34(x801,x802),f34(x803,x804)) % 58.74/58.93 [81]~P7(x812,x814)+~P7(x811,x813)+P7(f38(x811,x812),f38(x813,x814)) % 58.74/58.93 [82]~P6(x822,x824)+~P7(x821,x823)+P7(f37(x821,x822),f37(x823,x824)) % 58.74/58.93 [83]~P6(x832,x834)+~P6(x831,x833)+P8(f19(x831,x832),f19(x833,x834)) % 58.74/58.93 [67]~P1(x672)+~P1(x671)+~P9(x671,x672)+P14(f22(x671),f22(x672)) % 58.74/58.93 [68]~P1(x682)+~P1(x681)+P9(x681,x682)+~P14(f22(x681),f22(x682)) % 58.74/58.93 [69]~P2(x693,x694)+P2(x691,x692)+~P4(x693,x691)+~P4(x694,x692) % 58.74/58.93 [70]~P11(x703,x704)+P11(x701,x702)+~P3(x703,x701)+~P3(x704,x702) % 58.74/58.93 [71]~P9(x713,x714)+P9(x711,x712)+~P3(x713,x711)+~P3(x714,x712) % 58.74/58.93 [72]~P12(x723,x724)+P12(x721,x722)+~P3(x723,x721)+~P3(x724,x722) % 58.74/58.93 [73]~P14(x733,x734)+P14(x731,x732)+~P7(x733,x731)+~P7(x734,x732) % 58.74/58.93 [74]~P15(x743,x744)+P15(x741,x742)+~P6(x743,x741)+~P6(x744,x742) % 58.74/58.93 [75]~P17(x753,x754)+P17(x751,x752)+~P7(x753,x751)+~P7(x754,x752) % 58.74/58.93 %EqnAxiom % 58.74/58.93 % 58.74/58.93 %------------------------------------------- % 58.74/58.93 cnf(87,plain, % 58.74/58.93 (P3(f21(f20(f27(a5),f19(f27(f26(f25(f25(f26(f26(f25(f25(a5)))))))),f27(a5)))),a3)), % 58.74/58.93 inference(scs_inference,[],[16,3,60])). % 58.74/58.93 cnf(88,plain, % 58.74/58.93 (P3(x881,x881)), % 58.74/58.93 inference(rename_variables,[],[3])). % 58.74/58.93 cnf(96,plain, % 58.74/58.93 (P9(f15(a1),f21(f20(f27(a5),f19(f27(f26(f25(f25(f26(f26(f25(f25(a5)))))))),f27(a5)))))), % 58.74/58.93 inference(scs_inference,[],[10,16,28,25,7,8,3,88,60,64,65,71])). % 58.74/58.93 cnf(144,plain, % 58.74/58.93 (P1(f15(a1))), % 58.74/58.93 inference(scs_inference,[],[1,3,39,40])). % 58.74/58.93 cnf(199,plain, % 58.74/58.93 (P6(f36(f35(f21(f20(f27(a5),f19(f27(f26(f25(f25(f26(f26(f25(f25(a5)))))))),f27(a5)))))),f36(f35(a3)))), % 58.74/58.93 inference(scs_inference,[],[87,51,45])). % 58.74/58.93 cnf(728,plain, % 58.74/58.93 (P14(f22(f15(a1)),f22(f21(f20(f27(a5),f19(f27(f26(f25(f25(f26(f26(f25(f25(a5)))))))),f27(a5))))))), % 58.74/58.93 inference(scs_inference,[],[1,96,15,39,67])). % 58.74/58.93 cnf(778,plain, % 58.74/58.93 (P13(f35(f15(f21(f20(f27(a5),f19(f27(f26(f25(f25(f26(f26(f25(f25(a5)))))))),f27(a5)))))),f35(f15(a3)))), % 58.74/58.93 inference(scs_inference,[],[87,43,45])). % 58.74/58.93 cnf(787,plain, % 58.74/58.93 (P3(f29(f15(f21(f20(f27(a5),f19(f27(f26(f25(f25(f26(f26(f25(f25(a5)))))))),f27(a5))))),f15(f21(f20(f27(a5),f19(f27(f26(f25(f25(f26(f26(f25(f25(a5)))))))),f27(a5)))))),f29(f15(a3),f15(a3)))), % 58.74/58.93 inference(scs_inference,[],[87,43,76])). % 58.74/58.93 cnf(1855,plain, % 58.74/58.93 (P7(f23(f22(f15(a1))),f23(f39(f22(a1))))), % 58.74/58.93 inference(scs_inference,[],[1,53,59])). % 58.74/58.93 cnf(1971,plain, % 58.74/58.93 (P7(f39(f23(f23(f22(f15(a1))))),f39(f23(f23(f39(f22(a1))))))), % 58.74/58.93 inference(scs_inference,[],[1855,53,55])). % 58.74/58.93 cnf(1972,plain, % 58.74/58.93 (P7(f23(f39(f22(a1))),f23(f22(f15(a1))))), % 58.74/58.93 inference(scs_inference,[],[1855,8,65])). % 58.74/58.93 cnf(2070,plain, % 58.74/58.93 (P7(f39(f23(f23(f39(f22(a1))))),f39(f23(f23(f22(f15(a1))))))), % 58.74/58.93 inference(scs_inference,[],[1971,8,65])). % 58.74/58.93 cnf(2255,plain, % 58.74/58.93 ($false), % 58.74/58.93 inference(scs_inference,[],[1,38,778,728,2070,1972,144,199,787,16,8,39,43,44,45,46,47,48,49,50,51,52,53,55,56,57,58,59,76,79,80,81,73]), % 58.74/58.93 ['proof']). % 58.74/58.93 % SZS output end Proof % 58.74/58.93 % Total time :58.170000s %------------------------------------------------------------------------------