%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN688-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:18 EDT 2024 % Result : Unsatisfiable 28.91s 29.00s % Output : CNFRefutation 28.91s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : SYN688-1 : TPTP v8.2.0. Released v2.5.0. % 0.08/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n020.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Sun Jun 23 18:37:09 EDT 2024 % 0.13/0.34 % CPUTime : % 0.62/0.65 start to proof:theBenchmark % 28.91/28.99 %------------------------------------------- % 28.91/28.99 % File :CSE---1.7 % 28.91/28.99 % Problem :theBenchmark % 28.91/28.99 % Transform :cnf % 28.91/28.99 % Format :tptp:raw % 28.91/28.99 % Command :java -jar mcs_scs.jar %d %s % 28.91/28.99 % 28.91/28.99 % Result :Theorem 28.290000s % 28.91/28.99 % Output :CNFRefutation 28.290000s % 28.91/28.99 %------------------------------------------- % 28.91/28.99 %-------------------------------------------------------------------------- % 28.91/28.99 % File : SYN688-1 : TPTP v8.2.0. Released v2.5.0. % 28.91/28.99 % Domain : Syntactic % 28.91/28.99 % Problem : Harrison problem 4605 % 28.91/28.99 % Version : Especial. % 28.91/28.99 % English : % 28.91/28.99 % 28.91/28.99 % Refs : [Har01] Email to G. Sutcliffe % 28.91/28.99 % Source : [Har01] % 28.91/28.99 % Names : % 28.91/28.99 % 28.91/28.99 % Status : Unsatisfiable % 28.91/28.99 % Rating : 0.00 v8.1.0, 0.25 v7.4.0, 0.17 v7.3.0, 0.25 v6.2.0, 0.17 v6.1.0, 0.07 v6.0.0, 0.11 v5.5.0, 0.06 v5.4.0, 0.11 v5.3.0, 0.20 v5.2.0, 0.08 v5.1.0, 0.06 v5.0.0, 0.07 v4.0.1, 0.14 v3.7.0, 0.00 v2.5.0 % 28.91/28.99 % Syntax : Number of clauses : 62 ( 28 unt; 0 nHn; 55 RR) % 28.91/28.99 % Number of literals : 129 ( 0 equ; 72 neg) % 28.91/28.99 % Maximal clause size : 4 ( 2 avg) % 28.91/28.99 % Maximal term depth : 28 ( 5 avg) % 28.91/28.99 % Number of predicates : 15 ( 15 usr; 0 prp; 1-2 aty) % 28.91/28.99 % Number of functors : 30 ( 30 usr; 17 con; 0-2 aty) % 28.91/28.99 % Number of variables : 100 ( 0 sgn) % 28.91/28.99 % SPC : CNF_UNS_RFO_NEQ_HRN % 28.91/28.99 % 28.91/28.99 % Comments : % 28.91/28.99 %-------------------------------------------------------------------------- % 28.91/28.99 cnf(c34_is_p27_1,negated_conjecture, % 28.91/28.99 p27(c34) ). % 28.91/28.99 % 28.91/28.99 cnf(c43_is_p27_2,negated_conjecture, % 28.91/28.99 p27(c43) ). % 28.91/28.99 % 28.91/28.99 cnf(c35_is_p27_3,negated_conjecture, % 28.91/28.99 p27(c35) ). % 28.91/28.99 % 28.91/28.99 cnf(c43_is_not_p23_4,negated_conjecture, % 28.91/28.99 ~ p23(c43) ). % 28.91/28.99 % 28.91/28.99 cnf(p10_5,negated_conjecture, % 28.91/28.99 p10(X0,X0) ). % 28.91/28.99 % 28.91/28.99 cnf(p9_6,negated_conjecture, % 28.91/28.99 p9(X81,X81) ). % 28.91/28.99 % 28.91/28.99 cnf(p3_7,negated_conjecture, % 28.91/28.99 p3(X74,X74) ). % 28.91/28.99 % 28.91/28.99 cnf(p21_8,negated_conjecture, % 28.91/28.99 p21(X39,X39) ). % 28.91/28.99 % 28.91/28.99 cnf(p2_9,negated_conjecture, % 28.91/28.99 p2(X26,X26) ). % 28.91/28.99 % 28.91/28.99 cnf(p18_10,negated_conjecture, % 28.91/28.99 p18(X18,X18) ). % 28.91/28.99 % 28.91/28.99 cnf(p12_11,negated_conjecture, % 28.91/28.99 p12(X11,X11) ). % 28.91/28.99 % 28.91/28.99 cnf(p22_12,negated_conjecture, % 28.91/28.99 p22(c41,c42) ). % 28.91/28.99 % 28.91/28.99 cnf(not_p24_13,negated_conjecture, % 28.91/28.99 ~ p24(c43,c46) ). % 28.91/28.99 % 28.91/28.99 cnf(not_p24_14,negated_conjecture, % 28.91/28.99 ~ p24(c43,c45) ). % 28.91/28.99 % 28.91/28.99 cnf(not_p26_15,negated_conjecture, % 28.91/28.99 ~ p26(f17(c43),c35) ). % 28.91/29.00 % 28.91/29.00 cnf(not_p25_16,negated_conjecture, % 28.91/29.00 ~ p25(f17(c43),c34) ). % 28.91/29.00 % 28.91/29.00 cnf(p27_17,negated_conjecture, % 28.91/29.00 ( p27(f17(X23)) % 28.91/29.00 | ~ p27(X23) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p28_18,negated_conjecture, % 28.91/29.00 p28(f20(f19(c43)),f19(c34)) ). % 28.91/29.00 % 28.91/29.00 cnf(p3_19,negated_conjecture, % 28.91/29.00 p3(f15(f16(c43,c36)),c44) ). % 28.91/29.00 % 28.91/29.00 cnf(p23_20,negated_conjecture, % 28.91/29.00 ( p23(X46) % 28.91/29.00 | ~ p23(X47) % 28.91/29.00 | ~ p10(X47,X46) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p27_21,negated_conjecture, % 28.91/29.00 ( p27(X64) % 28.91/29.00 | ~ p27(X65) % 28.91/29.00 | ~ p10(X65,X64) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p3_22,negated_conjecture, % 28.91/29.00 ( p3(f4(X79),f4(X80)) % 28.91/29.00 | ~ p2(X79,X80) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p10_23,negated_conjecture, % 28.91/29.00 ( p10(f11(X3),f11(X4)) % 28.91/29.00 | ~ p9(X3,X4) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p10_24,negated_conjecture, % 28.91/29.00 ( p10(f17(X9),f17(X10)) % 28.91/29.00 | ~ p10(X9,X10) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p18_25,negated_conjecture, % 28.91/29.00 ( p18(f19(X21),f19(X22)) % 28.91/29.00 | ~ p10(X21,X22) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p18_26,negated_conjecture, % 28.91/29.00 ( p18(f20(X24),f20(X25)) % 28.91/29.00 | ~ p18(X24,X25) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p2_27,negated_conjecture, % 28.91/29.00 ( p2(f5(X29),f5(X30)) % 28.91/29.00 | ~ p2(X29,X30) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p2_28,negated_conjecture, % 28.91/29.00 ( p2(f6(X31),f6(X32)) % 28.91/29.00 | ~ p2(X31,X32) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p2_29,negated_conjecture, % 28.91/29.00 ( p2(f7(X33),f7(X34)) % 28.91/29.00 | ~ p2(X33,X34) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p3_30,negated_conjecture, % 28.91/29.00 ( p3(f15(X77),f15(X78)) % 28.91/29.00 | ~ p10(X77,X78) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p18_31,negated_conjecture, % 28.91/29.00 ( p18(f19(f17(X23)),f20(f19(X23))) % 28.91/29.00 | ~ p27(X23) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p10_32,negated_conjecture, % 28.91/29.00 ( p10(X1,X2) % 28.91/29.00 | ~ p10(X0,X1) % 28.91/29.00 | ~ p10(X0,X2) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p9_33,negated_conjecture, % 28.91/29.00 ( p9(X82,X83) % 28.91/29.00 | ~ p9(X81,X82) % 28.91/29.00 | ~ p9(X81,X83) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p3_34,negated_conjecture, % 28.91/29.00 ( p3(X75,X76) % 28.91/29.00 | ~ p3(X74,X75) % 28.91/29.00 | ~ p3(X74,X76) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p21_35,negated_conjecture, % 28.91/29.00 ( p21(X40,X41) % 28.91/29.00 | ~ p21(X39,X40) % 28.91/29.00 | ~ p21(X39,X41) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p2_36,negated_conjecture, % 28.91/29.00 ( p2(X27,X28) % 28.91/29.00 | ~ p2(X26,X27) % 28.91/29.00 | ~ p2(X26,X28) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p18_37,negated_conjecture, % 28.91/29.00 ( p18(X19,X20) % 28.91/29.00 | ~ p18(X18,X19) % 28.91/29.00 | ~ p18(X18,X20) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p12_38,negated_conjecture, % 28.91/29.00 ( p12(X12,X13) % 28.91/29.00 | ~ p12(X11,X12) % 28.91/29.00 | ~ p12(X11,X13) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p3_39,negated_conjecture, % 28.91/29.00 p3(c30,f4(f5(f6(f6(f6(f6(f6(f7(c31))))))))) ). % 28.91/29.00 % 28.91/29.00 cnf(p25_40,negated_conjecture, % 28.91/29.00 ( p25(X56,X57) % 28.91/29.00 | ~ p27(X56) % 28.91/29.00 | ~ p27(X57) % 28.91/29.00 | ~ p28(f19(X56),f19(X57)) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p26_41,negated_conjecture, % 28.91/29.00 ( p26(X62,X63) % 28.91/29.00 | ~ p27(X62) % 28.91/29.00 | ~ p27(X63) % 28.91/29.00 | ~ p29(f19(X62),f19(X63)) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p22_42,negated_conjecture, % 28.91/29.00 ( p22(X42,X43) % 28.91/29.00 | ~ p21(X45,X43) % 28.91/29.00 | ~ p22(X44,X45) % 28.91/29.00 | ~ p21(X44,X42) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p29_43,negated_conjecture, % 28.91/29.00 ( p29(X70,X71) % 28.91/29.00 | ~ p18(X73,X71) % 28.91/29.00 | ~ p29(X72,X73) % 28.91/29.00 | ~ p18(X72,X70) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p28_44,negated_conjecture, % 28.91/29.00 ( p28(X66,X67) % 28.91/29.00 | ~ p18(X69,X67) % 28.91/29.00 | ~ p28(X68,X69) % 28.91/29.00 | ~ p18(X68,X66) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p26_45,negated_conjecture, % 28.91/29.00 ( p26(X58,X59) % 28.91/29.00 | ~ p10(X61,X59) % 28.91/29.00 | ~ p26(X60,X61) % 28.91/29.00 | ~ p10(X60,X58) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p25_46,negated_conjecture, % 28.91/29.00 ( p25(X52,X53) % 28.91/29.00 | ~ p10(X55,X53) % 28.91/29.00 | ~ p25(X54,X55) % 28.91/29.00 | ~ p10(X54,X52) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p24_47,negated_conjecture, % 28.91/29.00 ( p24(X48,X49) % 28.91/29.00 | ~ p10(X51,X49) % 28.91/29.00 | ~ p24(X50,X51) % 28.91/29.00 | ~ p10(X50,X48) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p29_48,negated_conjecture, % 28.91/29.00 ( p29(f19(X62),f19(X63)) % 28.91/29.00 | ~ p27(X63) % 28.91/29.00 | ~ p27(X62) % 28.91/29.00 | ~ p26(X62,X63) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p28_49,negated_conjecture, % 28.91/29.00 ( p28(f19(X56),f19(X57)) % 28.91/29.00 | ~ p27(X57) % 28.91/29.00 | ~ p27(X56) % 28.91/29.00 | ~ p25(X56,X57) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p9_50,negated_conjecture, % 28.91/29.00 ( p9(f13(X84,X85),f13(X86,X87)) % 28.91/29.00 | ~ p12(X85,X87) % 28.91/29.00 | ~ p2(X84,X86) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p10_51,negated_conjecture, % 28.91/29.00 ( p10(f16(X5,X6),f16(X7,X8)) % 28.91/29.00 | ~ p10(X5,X7) % 28.91/29.00 | ~ p10(X6,X8) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p12_52,negated_conjecture, % 28.91/29.00 ( p12(f14(X14,X15),f14(X16,X17)) % 28.91/29.00 | ~ p2(X14,X16) % 28.91/29.00 | ~ p2(X15,X17) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p2_53,negated_conjecture, % 28.91/29.00 ( p2(f8(X35,X36),f8(X37,X38)) % 28.91/29.00 | ~ p2(X36,X38) % 28.91/29.00 | ~ p2(X35,X37) ) ). % 28.91/29.00 % 28.91/29.00 cnf(p3_54,negated_conjecture, % 28.91/29.00 p3(c32,f4(f8(f5(f6(f7(c31))),f5(f7(f6(f6(f7(c31)))))))) ). % 28.91/29.00 % 28.91/29.00 cnf(p10_55,negated_conjecture, % 28.91/29.00 p10(c33,f11(f13(f5(c31),f14(f5(f7(f7(f7(f7(f7(f7(f7(c31)))))))),f5(c31))))) ). % 28.91/29.00 % 28.91/29.00 cnf(p10_56,negated_conjecture, % 28.91/29.00 p10(c35,f11(f13(f5(c31),f14(f5(f6(f7(f7(f6(f6(f7(f7(c31)))))))),f5(c31))))) ). % 28.91/29.00 % 28.91/29.00 cnf(p10_57,negated_conjecture, % 28.91/29.00 p10(c39,f11(f13(f5(c31),f14(f5(f6(f7(f7(f7(f7(f7(f7(c31)))))))),f5(f6(f6(f7(f6(f6(f6(f7(c31)))))))))))) ). % 28.91/29.00 % 28.91/29.00 cnf(p10_58,negated_conjecture, % 28.91/29.00 p10(c40,f11(f13(f5(c31),f14(f5(f6(f6(f7(f7(f7(f7(f7(c31)))))))),f5(f6(f6(f7(f7(f6(f7(f7(f7(f6(f7(f6(f7(f6(f7(f6(f7(f6(f7(f6(f7(f6(f7(c31))))))))))))))))))))))))))) ). % 28.91/29.00 % 28.91/29.00 cnf(p10_59,negated_conjecture, % 28.91/29.00 p10(c37,f11(f13(f5(c31),f14(f5(f7(f6(f6(f7(f7(f7(f7(c31)))))))),f5(f6(f6(f6(f6(f6(f6(f6(f6(f6(f7(f6(f6(f7(f7(f7(f6(f7(f6(f6(f6(f7(f7(c31))))))))))))))))))))))))))) ). % 28.91/29.00 % 28.91/29.00 cnf(p10_60,negated_conjecture, % 28.91/29.00 p10(c38,f11(f13(f5(c31),f14(f5(f6(f7(f7(f6(f6(f7(f7(c31)))))))),f5(f6(f7(f7(f7(f6(f6(f6(f7(f6(f7(f7(f7(f7(f7(f6(f7(f7(f7(f7(f7(f7(f7(c31))))))))))))))))))))))))))) ). % 28.91/29.00 % 28.91/29.00 cnf(p10_61,negated_conjecture, % 28.91/29.00 p10(c36,f11(f13(f5(c31),f14(f5(f6(f6(f7(f6(f6(f6(f6(f7(c31))))))))),f5(f7(f7(f6(f7(f7(f7(f6(f6(f6(f7(f6(f7(f6(f7(f6(f7(f6(f6(f6(f7(f7(f7(c31))))))))))))))))))))))))))) ). % 28.91/29.00 % 28.91/29.00 cnf(p10_62,negated_conjecture, % 28.91/29.00 p10(c34,f11(f13(f5(c31),f14(f5(f6(f7(f7(f6(f6(f6(f6(f7(c31))))))))),f5(f6(f7(f6(f7(f7(f7(f6(f7(f7(f7(f6(f7(f6(f7(f7(f6(f6(f6(f7(f7(f7(f6(f7(c31)))))))))))))))))))))))))))) ). % 28.91/29.00 % 28.91/29.00 %-------------------------------------------------------------------------- % 28.91/29.00 %------------------------------------------- % 28.91/29.00 % Proof found % 28.91/29.00 % SZS status Theorem for theBenchmark % 28.91/29.00 % SZS output start Proof % 28.91/29.00 %ClaNum:62(EqnAxiom:0) % 28.91/29.00 %VarNum:209(SingletonVarNum:100) % 28.91/29.00 %MaxLitNum:4 % 28.91/29.00 %MaxfuncDepth:27 % 28.91/29.00 %SharedTerms:166 % 28.91/29.00 %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 % 28.91/29.00 %singleGoalClaCount:28 % 28.91/29.00 [1]P1(a1) % 28.91/29.00 [2]P1(a6) % 28.91/29.00 [3]P1(a7) % 28.91/29.00 [4]P2(a8,a14) % 28.91/29.00 [24]~P8(a6) % 28.91/29.00 [25]~P9(a6,a22) % 28.91/29.00 [26]~P9(a6,a23) % 28.91/29.00 [27]~P10(f24(a6),a7) % 28.91/29.00 [28]~P11(f24(a6),a1) % 28.91/29.00 [12]P14(f25(f15(a6)),f15(a1)) % 28.91/29.00 [13]P13(f17(f16(a6,a9)),a18) % 28.91/29.00 [16]P3(a7,f21(f20(f28(a3),f19(f28(f27(f26(f26(f27(f27(f26(f26(a3)))))))),f28(a3))))) % 28.91/29.00 [17]P3(a5,f21(f20(f28(a3),f19(f28(f26(f26(f26(f26(f26(f26(f26(a3)))))))),f28(a3))))) % 28.91/29.00 [14]P13(a2,f29(f30(f28(f27(f26(a3))),f28(f26(f27(f27(f26(a3)))))))) % 28.91/29.00 [15]P13(a4,f29(f28(f27(f27(f27(f27(f27(f26(a3))))))))) % 28.91/29.00 [18]P3(a10,f21(f20(f28(a3),f19(f28(f27(f26(f26(f26(f26(f26(f26(a3)))))))),f28(f27(f27(f26(f27(f27(f27(f26(a3)))))))))))) % 28.91/29.00 [19]P3(a13,f21(f20(f28(a3),f19(f28(f27(f27(f26(f26(f26(f26(f26(a3)))))))),f28(f27(f27(f26(f26(f27(f26(f26(f26(f27(f26(f27(f26(f27(f26(f27(f26(f27(f26(f27(f26(f27(f26(a3))))))))))))))))))))))))))) % 28.91/29.00 [20]P3(a11,f21(f20(f28(a3),f19(f28(f26(f27(f27(f26(f26(f26(f26(a3)))))))),f28(f27(f27(f27(f27(f27(f27(f27(f27(f27(f26(f27(f27(f26(f26(f26(f27(f26(f27(f27(f27(f26(f26(a3))))))))))))))))))))))))))) % 28.91/29.00 [21]P3(a12,f21(f20(f28(a3),f19(f28(f27(f26(f26(f27(f27(f26(f26(a3)))))))),f28(f27(f26(f26(f26(f27(f27(f27(f26(f27(f26(f26(f26(f26(f26(f27(f26(f26(f26(f26(f26(f26(f26(a3))))))))))))))))))))))))))) % 28.91/29.00 [22]P3(a9,f21(f20(f28(a3),f19(f28(f27(f27(f26(f27(f27(f27(f27(f26(a3))))))))),f28(f26(f26(f27(f26(f26(f26(f27(f27(f27(f26(f27(f26(f27(f26(f27(f26(f27(f27(f27(f26(f26(f26(a3))))))))))))))))))))))))))) % 28.91/29.00 [23]P3(a1,f21(f20(f28(a3),f19(f28(f27(f26(f26(f27(f27(f27(f27(f26(a3))))))))),f28(f27(f26(f27(f26(f26(f26(f27(f26(f26(f26(f27(f26(f27(f26(f26(f27(f27(f27(f26(f26(f26(f27(f26(a3)))))))))))))))))))))))))))) % 28.91/29.00 [5]P3(x51,x51) % 28.91/29.00 [6]P12(x61,x61) % 28.91/29.00 [7]P13(x71,x71) % 28.91/29.00 [8]P4(x81,x81) % 28.91/29.00 [9]P5(x91,x91) % 28.91/29.00 [10]P6(x101,x101) % 28.91/29.00 [11]P7(x111,x111) % 28.91/29.00 [29]~P1(x291)+P1(f24(x291)) % 28.91/29.00 [41]~P1(x411)+P6(f15(f24(x411)),f25(f15(x411))) % 28.91/29.00 [32]~P3(x321,x322)+P3(f24(x321),f24(x322)) % 28.91/29.00 [33]~P12(x331,x332)+P3(f21(x331),f21(x332)) % 28.91/29.00 [34]~P3(x341,x342)+P13(f17(x341),f17(x342)) % 28.91/29.01 [35]~P5(x351,x352)+P13(f29(x351),f29(x352)) % 28.91/29.01 [36]~P5(x361,x362)+P5(f28(x361),f28(x362)) % 28.91/29.01 [37]~P5(x371,x372)+P5(f27(x371),f27(x372)) % 28.91/29.01 [38]~P5(x381,x382)+P5(f26(x381),f26(x382)) % 28.91/29.01 [39]~P3(x391,x392)+P6(f15(x391),f15(x392)) % 28.91/29.01 [40]~P6(x401,x402)+P6(f25(x401),f25(x402)) % 28.91/29.01 [30]~P3(x302,x301)+P1(x301)+~P1(x302) % 28.91/29.01 [31]~P3(x312,x311)+P8(x311)+~P8(x312) % 28.91/29.01 [42]~P3(x423,x421)+P3(x421,x422)+~P3(x423,x422) % 28.91/29.01 [43]~P12(x433,x431)+P12(x431,x432)+~P12(x433,x432) % 28.91/29.01 [44]~P13(x443,x441)+P13(x441,x442)+~P13(x443,x442) % 28.91/29.01 [45]~P4(x453,x451)+P4(x451,x452)+~P4(x453,x452) % 28.91/29.01 [46]~P5(x463,x461)+P5(x461,x462)+~P5(x463,x462) % 28.91/29.01 [47]~P6(x473,x471)+P6(x471,x472)+~P6(x473,x472) % 28.91/29.01 [48]~P7(x483,x481)+P7(x481,x482)+~P7(x483,x482) % 28.91/29.01 [59]~P3(x592,x594)+~P3(x591,x593)+P3(f16(x591,x592),f16(x593,x594)) % 28.91/29.01 [60]~P5(x601,x603)+~P7(x602,x604)+P12(f20(x601,x602),f20(x603,x604)) % 28.91/29.01 [61]~P5(x612,x614)+~P5(x611,x613)+P5(f30(x611,x612),f30(x613,x614)) % 28.91/29.01 [62]~P5(x622,x624)+~P5(x621,x623)+P7(f19(x621,x622),f19(x623,x624)) % 28.91/29.01 [49]~P1(x492)+~P1(x491)+~P11(x491,x492)+P14(f15(x491),f15(x492)) % 28.91/29.01 [50]~P1(x502)+~P1(x501)+~P10(x501,x502)+P15(f15(x501),f15(x502)) % 28.91/29.01 [51]~P1(x512)+~P1(x511)+P10(x511,x512)+~P15(f15(x511),f15(x512)) % 28.91/29.01 [52]~P1(x522)+~P1(x521)+P11(x521,x522)+~P14(f15(x521),f15(x522)) % 28.91/29.01 [53]~P2(x533,x534)+P2(x531,x532)+~P4(x533,x531)+~P4(x534,x532) % 28.91/29.01 [54]~P9(x543,x544)+P9(x541,x542)+~P3(x543,x541)+~P3(x544,x542) % 28.91/29.01 [55]~P10(x553,x554)+P10(x551,x552)+~P3(x553,x551)+~P3(x554,x552) % 28.91/29.01 [56]~P11(x563,x564)+P11(x561,x562)+~P3(x563,x561)+~P3(x564,x562) % 28.91/29.01 [57]~P14(x573,x574)+P14(x571,x572)+~P6(x573,x571)+~P6(x574,x572) % 28.91/29.01 [58]~P15(x583,x584)+P15(x581,x582)+~P6(x583,x581)+~P6(x584,x582) % 28.91/29.01 %EqnAxiom % 28.91/29.01 % 28.91/29.01 %------------------------------------------- % 28.91/29.01 cnf(104,plain, % 28.91/29.01 (P1(f24(a6))), % 28.91/29.01 inference(scs_inference,[],[2,5,29,30])). % 28.91/29.01 cnf(276,plain, % 28.91/29.01 (~P3(x2761,a1)+~P11(f24(a6),x2761)), % 28.91/29.01 inference(scs_inference,[],[5,28,56])). % 28.91/29.01 cnf(282,plain, % 28.91/29.01 (~P14(f15(f24(a6)),f15(a1))), % 28.91/29.01 inference(scs_inference,[],[5,1,104,276,52])). % 28.91/29.01 cnf(1501,plain, % 28.91/29.01 (P6(f15(f24(a6)),f25(f15(a6)))), % 28.91/29.01 inference(scs_inference,[],[2,5,30,41])). % 28.91/29.01 cnf(1560,plain, % 28.91/29.01 (P6(x15601,x15601)), % 28.91/29.01 inference(rename_variables,[],[10])). % 28.91/29.01 cnf(1562,plain, % 28.91/29.01 ($false), % 28.91/29.01 inference(scs_inference,[],[1501,282,10,1560,12,47,57]), % 28.91/29.01 ['proof']). % 28.91/29.01 % SZS output end Proof % 28.91/29.01 % Total time :28.290000s %------------------------------------------------------------------------------