%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN694-1 : TPTP v8.2.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n028.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:19 EDT 2024 % Result : Unsatisfiable 185.25s 185.42s % Output : CNFRefutation 185.35s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.09 % Problem : SYN694-1 : TPTP v8.2.0. Released v2.5.0. % 0.00/0.09 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.10/0.28 % Computer : n028.cluster.edu % 0.10/0.28 % Model : x86_64 x86_64 % 0.10/0.28 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.28 % Memory : 8042.1875MB % 0.10/0.28 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.28 % CPULimit : 300 % 0.10/0.28 % WCLimit : 300 % 0.10/0.28 % DateTime : Sun Jun 23 21:42:23 EDT 2024 % 0.10/0.29 % CPUTime : % 0.14/0.53 start to proof:theBenchmark % 185.25/185.40 %------------------------------------------- % 185.25/185.40 % File :CSE---1.7 % 185.25/185.40 % Problem :theBenchmark % 185.25/185.40 % Transform :cnf % 185.25/185.40 % Format :tptp:raw % 185.25/185.40 % Command :java -jar mcs_scs.jar %d %s % 185.25/185.40 % 185.25/185.40 % Result :Theorem 184.670000s % 185.25/185.40 % Output :CNFRefutation 184.670000s % 185.25/185.40 %------------------------------------------- % 185.25/185.41 %-------------------------------------------------------------------------- % 185.25/185.41 % File : SYN694-1 : TPTP v8.2.0. Released v2.5.0. % 185.25/185.41 % Domain : Syntactic % 185.25/185.41 % Problem : Harrison problem 4644 % 185.25/185.41 % Version : Especial. % 185.25/185.41 % English : % 185.25/185.41 % 185.25/185.41 % Refs : [Har01] Email to G. Sutcliffe % 185.25/185.41 % Source : [Har01] % 185.25/185.41 % Names : % 185.25/185.41 % 185.25/185.41 % Status : Unsatisfiable % 185.25/185.41 % Rating : 0.08 v8.2.0, 0.14 v8.1.0, 0.00 v7.4.0, 0.17 v7.0.0, 0.12 v6.3.0, 0.00 v6.2.0, 0.11 v6.1.0, 0.14 v5.5.0, 0.25 v5.4.0, 0.30 v5.2.0, 0.10 v5.1.0, 0.18 v5.0.0, 0.29 v4.1.0, 0.25 v4.0.1, 0.20 v4.0.0, 0.29 v3.4.0, 0.25 v3.3.0, 0.33 v2.7.0, 0.00 v2.6.0, 0.33 v2.5.0 % 185.25/185.41 % Syntax : Number of clauses : 73 ( 30 unt; 2 nHn; 63 RR) % 185.25/185.41 % Number of literals : 155 ( 0 equ; 82 neg) % 185.25/185.41 % Maximal clause size : 5 ( 2 avg) % 185.25/185.41 % Maximal term depth : 6 ( 1 avg) % 185.25/185.41 % Number of predicates : 18 ( 18 usr; 0 prp; 1-3 aty) % 185.25/185.41 % Number of functors : 28 ( 28 usr; 14 con; 0-2 aty) % 185.25/185.41 % Number of variables : 132 ( 5 sgn) % 185.25/185.41 % SPC : CNF_UNS_RFO_NEQ_NHN % 185.25/185.41 % 185.25/185.41 % Comments : % 185.25/185.41 %-------------------------------------------------------------------------- % 185.25/185.41 cnf(c34_is_p25_1,negated_conjecture, % 185.25/185.41 p25(c34) ). % 185.25/185.41 % 185.25/185.41 cnf(c36_is_p29_2,negated_conjecture, % 185.25/185.41 p29(c36) ). % 185.25/185.41 % 185.25/185.41 cnf(f18_is_p30_3,negated_conjecture, % 185.25/185.41 p30(f18(c41)) ). % 185.25/185.41 % 185.25/185.41 cnf(f16_is_p28_4,negated_conjecture, % 185.25/185.41 p28(f16(c38)) ). % 185.25/185.41 % 185.25/185.41 cnf(f16_is_p28_5,negated_conjecture, % 185.25/185.41 p28(f16(c39)) ). % 185.25/185.41 % 185.25/185.41 cnf(f18_is_p30_6,negated_conjecture, % 185.25/185.41 p30(f18(c40)) ). % 185.25/185.41 % 185.25/185.41 cnf(p10_7,negated_conjecture, % 185.25/185.41 p10(X5,X5) ). % 185.25/185.41 % 185.25/185.41 cnf(p7_8,negated_conjecture, % 185.25/185.41 p7(X112,X112) ). % 185.25/185.41 % 185.25/185.41 cnf(p6_9,negated_conjecture, % 185.25/185.41 p6(X109,X109) ). % 185.25/185.41 % 185.25/185.41 cnf(p3_10,negated_conjecture, % 185.25/185.41 p3(X88,X88) ). % 185.25/185.41 % 185.25/185.41 cnf(p21_11,negated_conjecture, % 185.25/185.41 p21(X68,X68) ). % 185.25/185.41 % 185.25/185.41 cnf(p2_12,negated_conjecture, % 185.25/185.41 p2(X43,X43) ). % 185.25/185.41 % 185.25/185.41 cnf(p17_13,negated_conjecture, % 185.25/185.41 p17(X28,X28) ). % 185.25/185.41 % 185.25/185.41 cnf(p14_14,negated_conjecture, % 185.25/185.41 p14(X19,X19) ). % 185.25/185.41 % 185.25/185.41 cnf(p12_15,negated_conjecture, % 185.25/185.41 p12(X12,X12) ). % 185.25/185.41 % 185.25/185.41 cnf(p10_16,negated_conjecture, % 185.25/185.41 p10(c43,c47) ). % 185.25/185.41 % 185.25/185.41 cnf(p31_17,negated_conjecture, % 185.25/185.41 p31(c46,c42) ). % 185.25/185.41 % 185.25/185.41 cnf(p2_18,negated_conjecture, % 185.25/185.41 p2(c44,c45) ). % 185.25/185.41 % 185.25/185.41 cnf(p31_19,negated_conjecture, % 185.25/185.41 p31(c45,f5(c42)) ). % 185.25/185.41 % 185.25/185.41 cnf(p2_20,negated_conjecture, % 185.25/185.41 p2(c46,f9(c37)) ). % 185.25/185.41 % 185.25/185.41 cnf(p31_21,negated_conjecture, % 185.25/185.41 p31(c44,f5(c42)) ). % 185.25/185.41 % 185.25/185.41 cnf(p7_22,negated_conjecture, % 185.25/185.41 p7(f8(c35),c36) ). % 185.25/185.41 % 185.25/185.41 cnf(p31_23,negated_conjecture, % 185.25/185.41 p31(f23(c44,f9(f20(c37))),c45) ). % 185.25/185.41 % 185.25/185.41 cnf(p26_24,negated_conjecture, % 185.25/185.41 p26(c34,f4(f5(X79)),f4(X79)) ). % 185.25/185.41 % 185.25/185.41 cnf(p25_25,negated_conjecture, % 185.25/185.41 ( p25(X71) % 185.25/185.41 | ~ p25(X72) % 185.25/185.41 | ~ p21(X72,X71) ) ). % 185.25/185.41 % 185.25/185.41 cnf(p30_26,negated_conjecture, % 185.25/185.41 ( p30(X93) % 185.25/185.41 | ~ p30(X94) % 185.25/185.41 | ~ p17(X94,X93) ) ). % 185.25/185.41 % 185.25/185.41 cnf(p29_27,negated_conjecture, % 185.25/185.41 ( p29(X86) % 185.25/185.41 | ~ p29(X87) % 185.25/185.41 | ~ p7(X87,X86) ) ). % 185.25/185.41 % 185.25/185.41 cnf(p28_28,negated_conjecture, % 185.25/185.41 ( p28(X84) % 185.25/185.41 | ~ p28(X85) % 185.25/185.41 | ~ p14(X85,X84) ) ). % 185.25/185.41 % 185.25/185.41 cnf(p7_29,negated_conjecture, % 185.25/185.41 ( p7(f8(X115),f8(X116)) % 185.25/185.41 | ~ p6(X115,X116) ) ). % 185.25/185.41 % 185.25/185.41 cnf(p14_30,negated_conjecture, % 185.25/185.41 ( p14(f16(X26),f16(X27)) % 185.25/185.41 | ~ p14(X26,X27) ) ). % 185.25/185.41 % 185.25/185.41 cnf(p17_31,negated_conjecture, % 185.25/185.41 ( p17(f18(X31),f18(X32)) % 185.25/185.41 | ~ p17(X31,X32) ) ). % 185.25/185.41 % 185.25/185.41 cnf(p2_32,negated_conjecture, % 185.25/185.41 ( p2(f20(X56),f20(X57)) % 185.25/185.41 | ~ p2(X56,X57) ) ). % 185.25/185.41 % 185.25/185.41 cnf(p2_33,negated_conjecture, % 185.25/185.41 ( p2(f24(X62),f24(X63)) % 185.25/185.41 | ~ p2(X62,X63) ) ). % 185.25/185.41 % 185.25/185.41 cnf(p2_34,negated_conjecture, % 185.25/185.41 ( p2(f5(X64),f5(X65)) % 185.25/185.41 | ~ p2(X64,X65) ) ). % 185.25/185.41 % 185.25/185.41 cnf(p2_35,negated_conjecture, % 185.25/185.41 ( p2(f9(X66),f9(X67)) % 185.25/185.41 | ~ p2(X66,X67) ) ). % 185.25/185.41 % 185.25/185.41 cnf(p3_36,negated_conjecture, % 185.25/185.41 ( p3(f4(X91),f4(X92)) % 185.25/185.41 | ~ p2(X91,X92) ) ). % 185.25/185.41 % 185.25/185.41 cnf(p10_37,negated_conjecture, % 185.25/185.41 ( p10(X6,X7) % 185.25/185.41 | ~ p10(X5,X6) % 185.25/185.41 | ~ p10(X5,X7) ) ). % 185.25/185.41 % 185.25/185.41 cnf(p7_38,negated_conjecture, % 185.25/185.41 ( p7(X113,X114) % 185.25/185.41 | ~ p7(X112,X113) % 185.25/185.41 | ~ p7(X112,X114) ) ). % 185.25/185.41 % 185.25/185.41 cnf(p6_39,negated_conjecture, % 185.25/185.41 ( p6(X110,X111) % 185.25/185.41 | ~ p6(X109,X110) % 185.25/185.41 | ~ p6(X109,X111) ) ). % 185.25/185.41 % 185.25/185.41 cnf(p3_40,negated_conjecture, % 185.25/185.41 ( p3(X89,X90) % 185.25/185.41 | ~ p3(X88,X89) % 185.25/185.41 | ~ p3(X88,X90) ) ). % 185.25/185.41 % 185.25/185.41 cnf(p21_41,negated_conjecture, % 185.25/185.41 ( p21(X69,X70) % 185.25/185.41 | ~ p21(X68,X69) % 185.25/185.41 | ~ p21(X68,X70) ) ). % 185.25/185.41 % 185.25/185.41 cnf(p2_42,negated_conjecture, % 185.25/185.41 ( p2(X44,X45) % 185.25/185.41 | ~ p2(X43,X44) % 185.25/185.41 | ~ p2(X43,X45) ) ). % 185.25/185.41 % 185.25/185.41 cnf(p17_43,negated_conjecture, % 185.25/185.41 ( p17(X29,X30) % 185.25/185.41 | ~ p17(X28,X29) % 185.25/185.41 | ~ p17(X28,X30) ) ). % 185.25/185.41 % 185.25/185.41 cnf(p14_44,negated_conjecture, % 185.25/185.41 ( p14(X20,X21) % 185.25/185.41 | ~ p14(X19,X20) % 185.25/185.41 | ~ p14(X19,X21) ) ). % 185.25/185.41 % 185.25/185.41 cnf(p12_45,negated_conjecture, % 185.25/185.41 ( p12(X13,X14) % 185.25/185.41 | ~ p12(X12,X13) % 185.25/185.41 | ~ p12(X12,X14) ) ). % 185.25/185.41 % 185.25/185.41 cnf(p31_46,negated_conjecture, % 185.25/185.41 p31(f11(f4(f5(c42)),c43),f11(f4(c42),c43)) ). % 185.25/185.42 % 185.25/185.42 cnf(p31_47,negated_conjecture, % 185.25/185.42 ( p31(X95,f24(X95)) % 185.25/185.42 | ~ p31(X95,c44) % 185.25/185.42 | ~ p31(X95,f5(c42)) ) ). % 185.25/185.42 % 185.25/185.42 cnf(p31_48,negated_conjecture, % 185.25/185.42 ( p31(f24(X95),f5(c42)) % 185.25/185.42 | ~ p31(X95,c44) % 185.25/185.42 | ~ p31(X95,f5(c42)) ) ). % 185.25/185.42 % 185.25/185.42 cnf(p33_49,negated_conjecture, % 185.25/185.42 ( p33(X105,X106) % 185.25/185.42 | ~ p2(X108,X106) % 185.25/185.42 | ~ p33(X107,X108) % 185.25/185.42 | ~ p2(X107,X105) ) ). % 185.25/185.42 % 185.25/185.42 cnf(p27_50,negated_conjecture, % 185.25/185.42 ( p27(X80,X81) % 185.25/185.42 | ~ p14(X83,X80) % 185.25/185.42 | ~ p27(X83,X82) % 185.25/185.42 | ~ p12(X82,X81) ) ). % 185.25/185.42 % 185.25/185.42 cnf(p31_51,negated_conjecture, % 185.25/185.42 ( p31(X96,X97) % 185.25/185.42 | ~ p2(X99,X97) % 185.25/185.42 | ~ p31(X98,X99) % 185.25/185.42 | ~ p2(X98,X96) ) ). % 185.25/185.42 % 185.25/185.42 cnf(p32_52,negated_conjecture, % 185.25/185.42 ( p32(X100,X101) % 185.25/185.42 | ~ p17(X103,X100) % 185.25/185.42 | ~ p32(X103,X102) % 185.25/185.42 | ~ p10(X102,X101) ) ). % 185.25/185.42 % 185.25/185.42 cnf(p2_53,negated_conjecture, % 185.25/185.42 p2(f11(f4(c46),c47),f19(f11(f4(c42),c47),f9(f20(c37)))) ). % 185.25/185.42 % 185.25/185.42 cnf(p31_54,negated_conjecture, % 185.25/185.42 p31(f11(f4(c42),c43),f11(f4(f23(c42,f9(f20(c37)))),c43)) ). % 185.25/185.42 % 185.25/185.42 cnf(p2_55,negated_conjecture, % 185.25/185.42 p2(f11(f4(f23(c44,f9(f20(c37)))),c43),f11(f4(c44),c43)) ). % 185.25/185.42 % 185.25/185.42 cnf(not_p2_56,negated_conjecture, % 185.25/185.42 ~ p2(f11(f4(c45),c43),f11(f4(f23(c44,f9(f20(c37)))),c43)) ). % 185.25/185.42 % 185.25/185.42 cnf(p10_57,negated_conjecture, % 185.25/185.42 ( p10(X0,c43) % 185.25/185.42 | ~ p31(f11(f4(f5(c42)),X0),f11(f4(c42),X0)) ) ). % 185.25/185.42 % 185.25/185.42 cnf(p12_58,negated_conjecture, % 185.25/185.42 ( p12(f13(X15,X16),f13(X17,X18)) % 185.25/185.42 | ~ p10(X15,X17) % 185.25/185.42 | ~ p2(X16,X18) ) ). % 185.25/185.42 % 185.25/185.42 cnf(p2_59,negated_conjecture, % 185.25/185.42 ( p2(f23(X58,X59),f23(X60,X61)) % 185.25/185.42 | ~ p2(X58,X60) % 185.25/185.42 | ~ p2(X59,X61) ) ). % 185.25/185.42 % 185.25/185.42 cnf(p2_60,negated_conjecture, % 185.25/185.42 ( p2(f19(X52,X53),f19(X54,X55)) % 185.25/185.42 | ~ p2(X52,X54) % 185.25/185.42 | ~ p2(X53,X55) ) ). % 185.25/185.42 % 185.25/185.42 cnf(p2_61,negated_conjecture, % 185.25/185.42 ( p2(f11(X46,X47),f11(X48,X49)) % 185.25/185.42 | ~ p10(X47,X49) % 185.25/185.42 | ~ p3(X46,X48) ) ). % 185.25/185.42 % 185.25/185.42 cnf(p17_62,negated_conjecture, % 185.25/185.42 ( p17(f22(X33,X34),f22(X35,X36)) % 185.25/185.42 | ~ p10(X34,X36) % 185.25/185.42 | ~ p21(X33,X35) ) ). % 185.25/185.42 % 185.25/185.42 cnf(p14_63,negated_conjecture, % 185.25/185.42 ( p14(f15(X22,X23),f15(X24,X25)) % 185.25/185.42 | ~ p12(X23,X25) % 185.25/185.42 | ~ p7(X22,X24) ) ). % 185.25/185.42 % 185.25/185.42 cnf(p2_64,negated_conjecture, % 185.25/185.42 p2(f19(f11(f4(f5(c42)),c43),f9(f20(c37))),f11(f4(c42),c43)) ). % 185.25/185.42 % 185.25/185.42 cnf(p32_65,negated_conjecture, % 185.25/185.42 ( p32(f22(c34,X104),c43) % 185.25/185.42 | ~ p33(f11(f4(f5(c42)),X104),f11(f4(c42),X104)) ) ). % 185.25/185.42 % 185.25/185.42 cnf(p2_66,negated_conjecture, % 185.25/185.42 ( p2(f11(f4(X51),c47),f11(f4(c46),c47)) % 185.25/185.42 | ~ p31(X51,c42) % 185.25/185.42 | ~ p31(c46,X51) ) ). % 185.25/185.42 % 185.25/185.42 cnf(p2_67,negated_conjecture, % 185.25/185.42 ( p2(f11(f4(X50),c43),f11(f4(c44),c43)) % 185.25/185.42 | ~ p31(c44,X50) % 185.25/185.42 | ~ p31(X50,f5(c42)) ) ). % 185.25/185.42 % 185.25/185.42 cnf(p10_68,negated_conjecture, % 185.25/185.42 ( p10(X1,X2) % 185.25/185.42 | p32(f22(c34,X1),X2) % 185.25/185.42 | ~ p27(f15(c36,f13(X1,X3)),f13(X2,X4)) ) ). % 185.25/185.42 % 185.25/185.42 cnf(not_p31_69,negated_conjecture, % 185.25/185.42 ( ~ p31(X95,c44) % 185.25/185.42 | ~ p31(X95,f5(c42)) % 185.25/185.42 | ~ p2(f11(f4(f24(X95)),c43),f11(f4(X95),c43)) ) ). % 185.25/185.42 % 185.25/185.42 cnf(p26_70,negated_conjecture, % 185.25/185.42 ( p26(X73,X74,X75) % 185.25/185.42 | ~ p3(X78,X75) % 185.25/185.42 | ~ p3(X77,X74) % 185.25/185.42 | ~ p21(X76,X73) % 185.25/185.42 | ~ p26(X76,X77,X78) ) ). % 185.25/185.42 % 185.25/185.42 cnf(p10_71,negated_conjecture, % 185.25/185.42 ( p10(X8,X9) % 185.25/185.42 | ~ p2(f11(f4(X10),X8),f9(c37)) % 185.25/185.42 | ~ p27(f15(c36,f13(X8,X10)),f13(X9,X11)) ) ). % 185.25/185.42 % 185.25/185.42 cnf(p2_72,negated_conjecture, % 185.25/185.42 ( p2(X37,X38) % 185.25/185.42 | ~ p27(f15(c36,f13(X39,X37)),f13(X40,X41)) % 185.25/185.42 | ~ p27(f15(c36,f13(X42,X38)),f13(X40,X41)) ) ). % 185.25/185.42 % 185.25/185.42 cnf(p32_73,negated_conjecture, % 185.25/185.42 ( p32(f22(c34,X1),X2) % 185.25/185.42 | p31(f11(f4(X3),X2),f11(f4(X4),X2)) % 185.25/185.42 | ~ p27(f15(c36,f13(X1,X3)),f13(X2,X4)) ) ). % 185.25/185.42 % 185.25/185.42 %-------------------------------------------------------------------------- % 185.25/185.42 %------------------------------------------- % 185.25/185.42 % Proof found % 185.25/185.42 % SZS status Theorem for theBenchmark % 185.25/185.42 % SZS output start Proof % 185.25/185.42 %ClaNum:73(EqnAxiom:0) % 185.25/185.42 %VarNum:273(SingletonVarNum:132) % 185.25/185.42 %MaxLitNum:5 % 185.25/185.42 %MaxfuncDepth:5 % 185.25/185.42 %SharedTerms:62 % 185.25/185.42 %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 % 185.25/185.42 %singleGoalClaCount:30 % 185.25/185.42 [1]P1(a1) % 185.25/185.42 [2]P8(a2) % 185.25/185.42 [7]P2(a11,a13) % 185.25/185.42 [8]P3(a14,a15) % 185.25/185.42 [9]P14(a16,a12) % 185.25/185.42 [3]P12(f9(a4)) % 185.25/185.42 [4]P12(f9(a5)) % 185.25/185.42 [5]P9(f10(a6)) % 185.25/185.42 [6]P9(f10(a8)) % 185.25/185.42 [19]P3(a16,f20(a7)) % 185.25/185.42 [20]P14(a14,f21(a12)) % 185.25/185.42 [21]P14(a15,f21(a12)) % 185.25/185.42 [22]P15(f28(a3),a2) % 185.25/185.42 [23]P14(f24(a14,f20(f22(a7))),a15) % 185.25/185.42 [25]P14(f17(f26(f21(a12)),a11),f17(f26(a12),a11)) % 185.25/185.42 [26]P3(f17(f26(a16),a13),f23(f17(f26(a12),a13),f20(f22(a7)))) % 185.25/185.42 [27]P3(f23(f17(f26(f21(a12)),a11),f20(f22(a7))),f17(f26(a12),a11)) % 185.25/185.42 [28]P14(f17(f26(a12),a11),f17(f26(f24(a12,f20(f22(a7)))),a11)) % 185.25/185.42 [29]P3(f17(f26(f24(a14,f20(f22(a7)))),a11),f17(f26(a14),a11)) % 185.25/185.42 [30]~P3(f17(f26(a15),a11),f17(f26(f24(a14,f20(f22(a7)))),a11)) % 185.25/185.42 [10]P2(x101,x101) % 185.25/185.42 [11]P15(x111,x111) % 185.25/185.42 [12]P16(x121,x121) % 185.25/185.42 [13]P13(x131,x131) % 185.25/185.42 [14]P7(x141,x141) % 185.25/185.42 [15]P3(x151,x151) % 185.25/185.42 [16]P4(x161,x161) % 185.25/185.42 [17]P5(x171,x171) % 185.25/185.42 [18]P6(x181,x181) % 185.25/185.42 [24]P10(a1,f26(f21(x241)),f26(x241)) % 185.25/185.42 [66]P2(x661,a11)+~P14(f17(f26(f21(a12)),x661),f17(f26(a12),x661)) % 185.25/185.42 [67]P18(f25(a1,x671),a11)+~P17(f17(f26(f21(a12)),x671),f17(f26(a12),x671)) % 185.25/185.42 [35]~P16(x351,x352)+P15(f28(x351),f28(x352)) % 185.25/185.42 [36]~P3(x361,x362)+P13(f26(x361),f26(x362)) % 185.25/185.42 [37]~P3(x371,x372)+P3(f21(x371),f21(x372)) % 185.25/185.42 [38]~P3(x381,x382)+P3(f20(x381),f20(x382)) % 185.25/185.42 [39]~P3(x391,x392)+P3(f22(x391),f22(x392)) % 185.25/185.42 [40]~P3(x401,x402)+P3(f27(x401),f27(x402)) % 185.25/185.42 [41]~P4(x411,x412)+P4(f9(x411),f9(x412)) % 185.25/185.42 [42]~P5(x421,x422)+P5(f10(x421),f10(x422)) % 185.25/185.42 [52]~P14(x521,a14)+P14(x521,f27(x521))+~P14(x521,f21(a12)) % 185.25/185.42 [53]~P14(x531,a14)+~P14(x531,f21(a12))+P14(f27(x531),f21(a12)) % 185.25/185.42 [64]~P14(x641,a12)+~P14(a16,x641)+P3(f17(f26(x641),a13),f17(f26(a16),a13)) % 185.25/185.42 [65]~P14(a14,x651)+~P14(x651,f21(a12))+P3(f17(f26(x651),a11),f17(f26(a14),a11)) % 185.25/185.42 [69]~P14(x691,a14)+~P14(x691,f21(a12))+~P3(f17(f26(f27(x691)),a11),f17(f26(x691),a11)) % 185.25/185.42 [31]~P7(x312,x311)+P1(x311)+~P1(x312) % 185.25/185.42 [32]~P15(x322,x321)+P8(x321)+~P8(x322) % 185.25/185.42 [33]~P4(x332,x331)+P12(x331)+~P12(x332) % 185.25/185.42 [34]~P5(x342,x341)+P9(x341)+~P9(x342) % 185.25/185.42 [43]~P2(x433,x431)+P2(x431,x432)+~P2(x433,x432) % 185.25/185.42 [44]~P15(x443,x441)+P15(x441,x442)+~P15(x443,x442) % 185.25/185.42 [45]~P16(x453,x451)+P16(x451,x452)+~P16(x453,x452) % 185.25/185.42 [46]~P13(x463,x461)+P13(x461,x462)+~P13(x463,x462) % 185.25/185.42 [47]~P7(x473,x471)+P7(x471,x472)+~P7(x473,x472) % 185.25/185.42 [48]~P3(x483,x481)+P3(x481,x482)+~P3(x483,x482) % 185.25/185.42 [49]~P4(x493,x491)+P4(x491,x492)+~P4(x493,x492) % 185.25/185.42 [50]~P5(x503,x501)+P5(x501,x502)+~P5(x503,x502) % 185.25/185.42 [51]~P6(x513,x511)+P6(x511,x512)+~P6(x513,x512) % 185.25/185.42 [58]~P3(x582,x584)+~P3(x581,x583)+P3(f24(x581,x582),f24(x583,x584)) % 185.25/185.42 [59]~P2(x592,x594)+~P13(x591,x593)+P3(f17(x591,x592),f17(x593,x594)) % 185.25/185.42 [60]~P3(x602,x604)+~P3(x601,x603)+P3(f23(x601,x602),f23(x603,x604)) % 185.25/185.42 [61]~P2(x612,x614)+~P7(x611,x613)+P4(f25(x611,x612),f25(x613,x614)) % 185.25/185.42 [62]~P15(x621,x623)+~P6(x622,x624)+P5(f18(x621,x622),f18(x623,x624)) % 185.25/185.42 [63]~P2(x631,x633)+~P3(x632,x634)+P6(f19(x631,x632),f19(x633,x634)) % 185.25/185.42 [70]P2(x701,x702)+P18(f25(a1,x701),x702)+~P11(f18(a2,f19(x701,x703)),f19(x702,x704)) % 185.25/185.42 [71]P2(x711,x712)+~P11(f18(a2,f19(x711,x713)),f19(x712,x714))+~P3(f17(f26(x713),x711),f20(a7)) % 185.25/185.42 [72]P18(f25(a1,x721),x722)+P14(f17(f26(x723),x722),f17(f26(x724),x722))+~P11(f18(a2,f19(x721,x723)),f19(x722,x724)) % 185.25/185.42 [73]P3(x731,x732)+~P11(f18(a2,f19(x733,x732)),f19(x734,x735))+~P11(f18(a2,f19(x736,x731)),f19(x734,x735)) % 185.25/185.42 [54]~P14(x543,x544)+P14(x541,x542)+~P3(x543,x541)+~P3(x544,x542) % 185.25/185.42 [55]~P17(x553,x554)+P17(x551,x552)+~P3(x553,x551)+~P3(x554,x552) % 185.25/185.42 [56]~P11(x563,x564)+P11(x561,x562)+~P5(x563,x561)+~P6(x564,x562) % 185.25/185.42 [57]~P18(x574,x573)+P18(x571,x572)+~P2(x573,x572)+~P4(x574,x571) % 185.25/185.42 [68]~P10(x686,x684,x685)+P10(x681,x682,x683)+~P13(x684,x682)+~P13(x685,x683)+~P7(x686,x681) % 185.25/185.42 %EqnAxiom % 185.25/185.42 % 185.25/185.42 %------------------------------------------- % 185.35/185.44 cnf(86,plain, % 185.35/185.44 (P2(a13,a11)), % 185.35/185.44 inference(scs_inference,[],[7,10,43])). % 185.35/185.44 cnf(89,plain, % 185.35/185.44 (P3(a15,a14)), % 185.35/185.44 inference(scs_inference,[],[7,8,10,15,43,48])). % 185.35/185.44 cnf(157,plain, % 185.35/185.44 (P3(f20(a7),a16)), % 185.35/185.44 inference(scs_inference,[],[19,15,48])). % 185.35/185.44 cnf(195,plain, % 185.35/185.44 (P15(a2,f28(a3))), % 185.35/185.44 inference(scs_inference,[],[22,11,44])). % 185.35/185.44 cnf(199,plain, % 185.35/185.44 (P3(f21(f20(a15)),f21(f20(a14)))), % 185.35/185.44 inference(scs_inference,[],[89,37,38])). % 185.35/185.44 cnf(204,plain, % 185.35/185.44 (P3(f22(f27(a15)),f22(f27(a14)))), % 185.35/185.44 inference(scs_inference,[],[89,39,40])). % 185.35/185.44 cnf(209,plain, % 185.35/185.44 (P4(f9(f25(x2091,a13)),f9(f25(x2091,a11)))), % 185.35/185.44 inference(scs_inference,[],[86,14,41,61])). % 185.35/185.44 cnf(210,plain, % 185.35/185.44 (P4(f9(f25(x2101,a11)),f9(f25(x2101,a13)))), % 185.35/185.44 inference(scs_inference,[],[209,16,49])). % 185.35/185.44 cnf(219,plain, % 185.35/185.44 (P5(f10(f18(a2,x2191)),f10(f18(f28(a3),x2191)))), % 185.35/185.44 inference(scs_inference,[],[195,18,42,62])). % 185.35/185.44 cnf(220,plain, % 185.35/185.44 (P5(f10(f18(f28(a3),x2201)),f10(f18(a2,x2201)))), % 185.35/185.44 inference(scs_inference,[],[219,17,50])). % 185.35/185.44 cnf(260,plain, % 185.35/185.44 (~P17(x2601,f17(f26(f24(a14,f20(f22(a7)))),a11))+P17(x2601,f17(f26(a14),a11))), % 185.35/185.44 inference(scs_inference,[],[29,15,55])). % 185.35/185.44 cnf(264,plain, % 185.35/185.44 (~P3(f17(f26(f24(a14,f20(f22(a7)))),a11),f17(f26(a15),a11))), % 185.35/185.44 inference(scs_inference,[],[30,15,48])). % 185.35/185.44 cnf(292,plain, % 185.35/185.44 (P6(f19(a11,a15),f19(a11,a14))), % 185.35/185.44 inference(scs_inference,[],[25,89,66,63])). % 185.35/185.44 cnf(293,plain, % 185.35/185.44 (P6(f19(a11,a14),f19(a11,a15))), % 185.35/185.44 inference(scs_inference,[],[292,18,51])). % 185.35/185.44 cnf(349,plain, % 185.35/185.44 (P3(f17(x3491,a13),f17(x3491,a11))), % 185.35/185.44 inference(scs_inference,[],[13,86,46,59])). % 185.35/185.44 cnf(350,plain, % 185.35/185.44 (~P3(f17(f26(a15),a13),f17(f26(f24(a14,f20(f22(a7)))),a11))), % 185.35/185.44 inference(scs_inference,[],[264,349,48])). % 185.35/185.44 cnf(363,plain, % 185.35/185.44 (~P17(x3631,f17(x3632,a13))+P17(x3631,f17(x3632,a11))), % 185.35/185.44 inference(scs_inference,[],[349,15,55])). % 185.35/185.44 cnf(368,plain, % 185.35/185.44 (~P3(f17(f26(f24(a14,f20(f22(a7)))),a13),f17(f26(a15),a13))), % 185.35/185.44 inference(scs_inference,[],[350,349,48])). % 185.35/185.44 cnf(392,plain, % 185.35/185.44 (~P3(f17(f26(a15),a13),f17(f26(f24(a14,f20(f22(a7)))),a13))), % 185.35/185.44 inference(scs_inference,[],[368,15,48])). % 185.35/185.44 cnf(826,plain, % 185.35/185.44 (P3(f17(f26(a15),a13),f17(f26(a14),a11))), % 185.35/185.44 inference(scs_inference,[],[89,86,36,59])). % 185.35/185.44 cnf(1594,plain, % 185.35/185.44 (P17(x15941,f17(f26(a14),a11))+~P17(x15941,f17(f26(f24(a14,f20(f22(a7)))),a13))), % 185.35/185.44 inference(scs_inference,[],[363,260])). % 185.35/185.44 cnf(1595,plain, % 185.35/185.44 (~P17(f21(f20(a15)),f17(f26(f24(a14,f20(f22(a7)))),a13))+P17(f21(f20(a14)),f17(f26(a14),a11))), % 185.35/185.44 inference(scs_inference,[],[199,15,1594,55])). % 185.35/185.44 cnf(1596,plain, % 185.35/185.44 (~P3(f17(f26(a14),a11),x15961)+P17(f21(f20(a14)),x15961)+~P17(f21(f20(a15)),f17(f26(f24(a14,f20(f22(a7)))),a13))), % 185.35/185.44 inference(scs_inference,[],[15,1595,55])). % 185.35/185.44 cnf(1597,plain, % 185.35/185.44 (~P3(f17(f26(a14),a11),f17(x15971,a13))+P17(f21(f20(a14)),f17(x15971,a11))+~P17(f21(f20(a15)),f17(f26(f24(a14,f20(f22(a7)))),a13))), % 185.35/185.44 inference(scs_inference,[],[363,1596])). % 185.35/185.44 cnf(1708,plain, % 185.35/185.44 (P6(f19(a11,f21(f20(a15))),f19(a11,f21(f20(a14))))), % 185.35/185.44 inference(scs_inference,[],[25,199,66,63])). % 185.35/185.44 cnf(1709,plain, % 185.35/185.44 (P6(f19(a11,f21(f20(a14))),f19(a11,f21(f20(a15))))), % 185.35/185.44 inference(scs_inference,[],[1708,18,51])). % 185.35/185.44 cnf(2394,plain, % 185.35/185.44 (P3(f23(f22(f27(a15)),f22(f27(a15))),f23(f22(f27(a14)),f22(f27(a14))))), % 185.35/185.44 inference(scs_inference,[],[29,204,210,220,37,38,39,40,41,42,36,58,60])). % 185.35/185.44 cnf(2426,plain, % 185.35/185.44 (P4(f9(f9(f25(x24261,a13))),f9(f9(f25(x24261,a11))))), % 185.35/185.44 inference(scs_inference,[],[2394,209,40,41])). % 185.35/185.44 cnf(2428,plain, % 185.35/185.44 (P5(f10(f10(f18(a2,x24281))),f10(f10(f18(f28(a3),x24281))))), % 185.35/185.44 inference(scs_inference,[],[2394,209,219,40,41,42])). % 185.35/185.44 cnf(2454,plain, % 185.35/185.44 (P4(f9(f9(f9(f25(x24541,a13)))),f9(f9(f9(f25(x24541,a11)))))), % 185.35/185.44 inference(scs_inference,[],[2426,41])). % 185.35/185.44 cnf(2458,plain, % 185.35/185.44 (P3(f21(f22(f27(a15))),f21(f22(f27(a14))))), % 185.35/185.44 inference(scs_inference,[],[2426,204,41,40,37])). % 185.35/185.44 cnf(2472,plain, % 185.35/185.44 (P3(f24(f17(f26(a15),a13),f17(f26(a15),a13)),f24(f17(f26(a14),a11),f17(f26(a14),a11)))), % 185.35/185.44 inference(scs_inference,[],[2426,2428,204,826,7,41,40,37,36,38,39,42,63,60,58])). % 185.35/185.44 cnf(2523,plain, % 185.35/185.44 (P5(f18(f28(a3),f19(a11,f21(f20(a14)))),f18(a2,f19(a11,f21(f20(a15)))))), % 185.35/185.44 inference(scs_inference,[],[2458,22,1709,36,38,40,37,39,62])). % 185.35/185.44 cnf(2929,plain, % 185.35/185.44 (P3(f24(a14,a14),f24(a15,a15))), % 185.35/185.44 inference(scs_inference,[],[2472,8,36,38,37,39,40,58])). % 185.35/185.44 cnf(2931,plain, % 185.35/185.44 (P3(f23(a14,a14),f23(a15,a15))), % 185.35/185.44 inference(scs_inference,[],[2472,8,36,38,37,39,40,58,60])). % 185.35/185.44 cnf(2940,plain, % 185.35/185.44 (P13(f26(f24(a14,a14)),f26(f24(a15,a15)))), % 185.35/185.44 inference(scs_inference,[],[2929,36])). % 185.35/185.44 cnf(2942,plain, % 185.35/185.44 (P3(f20(f24(a14,a14)),f20(f24(a15,a15)))), % 185.35/185.44 inference(scs_inference,[],[2929,36,38])). % 185.35/185.44 cnf(2944,plain, % 185.35/185.44 (P3(f22(f24(a14,a14)),f22(f24(a15,a15)))), % 185.35/185.44 inference(scs_inference,[],[2929,36,38,39])). % 185.35/185.44 cnf(2946,plain, % 185.35/185.44 (P3(f21(f24(a14,a14)),f21(f24(a15,a15)))), % 185.35/185.44 inference(scs_inference,[],[2929,36,38,39,37])). % 185.35/185.44 cnf(2948,plain, % 185.35/185.44 (P3(f27(f24(a14,a14)),f27(f24(a15,a15)))), % 185.35/185.44 inference(scs_inference,[],[2929,36,38,39,37,40])). % 185.35/185.44 cnf(2950,plain, % 185.35/185.44 (P6(f19(a11,f24(a14,a14)),f19(a13,f24(a15,a15)))), % 185.35/185.44 inference(scs_inference,[],[2929,7,36,38,39,37,40,63])). % 185.35/185.44 cnf(2952,plain, % 185.35/185.44 (P3(f24(f24(a14,a14),f24(a14,a14)),f24(f24(a15,a15),f24(a15,a15)))), % 185.35/185.44 inference(scs_inference,[],[2929,7,36,38,39,37,40,63,58])). % 185.35/185.44 cnf(2977,plain, % 185.35/185.44 (P6(f19(x29771,f20(f24(a14,a14))),f19(x29771,f20(f24(a15,a15))))), % 185.35/185.44 inference(scs_inference,[],[2942,2950,11,10,36,38,37,39,40,62,63])). % 185.35/185.44 cnf(2981,plain, % 185.35/185.44 (P3(f24(f20(f24(a14,a14)),f20(f24(a14,a14))),f24(f20(f24(a15,a15)),f20(f24(a15,a15))))), % 185.35/185.44 inference(scs_inference,[],[2940,2942,2950,11,10,36,38,37,39,40,62,63,59,58])). % 185.35/185.44 cnf(2990,plain, % 185.35/185.44 (P13(f26(f22(f24(a14,a14))),f26(f22(f24(a15,a15))))), % 185.35/185.44 inference(scs_inference,[],[2944,36])). % 185.35/185.44 cnf(3002,plain, % 185.35/185.44 (P6(f19(a11,f22(f24(a14,a14))),f19(a13,f22(f24(a15,a15))))), % 185.35/185.44 inference(scs_inference,[],[2944,2977,22,7,36,38,39,37,40,62,63])). % 185.35/185.44 cnf(3029,plain, % 185.35/185.44 (P3(f24(f21(f24(a14,a14)),f21(f24(a14,a14))),f24(f21(f24(a15,a15)),f21(f24(a15,a15))))), % 185.35/185.44 inference(scs_inference,[],[2946,2990,3002,11,10,36,38,37,39,40,62,63,59,58])). % 185.35/185.44 cnf(3133,plain, % 185.35/185.44 (P3(f24(f27(f24(a14,a14)),f27(f24(a14,a14))),f24(f27(f24(a15,a15)),f27(f24(a15,a15))))), % 185.35/185.44 inference(scs_inference,[],[3029,2948,36,38,37,39,40,58])). % 185.35/185.44 cnf(3165,plain, % 185.35/185.44 (P5(f10(f18(f28(a3),f19(a11,f24(a14,a14)))),f10(f18(a2,f19(a13,f24(a15,a15)))))), % 185.35/185.44 inference(scs_inference,[],[3133,2952,2950,2940,22,7,36,38,37,39,40,63,58,60,62,59,42])). % 185.35/185.44 cnf(3391,plain, % 185.35/185.44 (P3(f23(f23(a14,a14),f23(a14,a14)),f23(f23(a15,a15),f23(a15,a15)))), % 185.35/185.44 inference(scs_inference,[],[2981,2931,36,38,37,39,40,60])). % 185.35/185.44 cnf(3419,plain, % 185.35/185.44 (P3(f23(f23(f23(a14,a14),f23(a14,a14)),f23(f23(a14,a14),f23(a14,a14))),f23(f23(f23(a15,a15),f23(a15,a15)),f23(f23(a15,a15),f23(a15,a15))))), % 185.35/185.44 inference(scs_inference,[],[3391,10,36,38,39,37,40,63,60])). % 185.35/185.44 cnf(3421,plain, % 185.35/185.44 (P3(f24(f23(f23(a14,a14),f23(a14,a14)),f23(f23(a14,a14),f23(a14,a14))),f24(f23(f23(a15,a15),f23(a15,a15)),f23(f23(a15,a15),f23(a15,a15))))), % 185.35/185.44 inference(scs_inference,[],[3391,10,36,38,39,37,40,63,60,58])). % 185.35/185.44 cnf(3617,plain, % 185.35/185.44 (P3(f23(f20(a7),f20(a7)),f23(a16,a16))), % 185.35/185.44 inference(scs_inference,[],[3421,157,36,38,39,37,40,60])). % 185.35/185.44 cnf(3619,plain, % 185.35/185.44 (P3(f24(f20(a7),f20(a7)),f24(a16,a16))), % 185.35/185.44 inference(scs_inference,[],[3421,157,36,38,39,37,40,60,58])). % 185.35/185.44 cnf(3624,plain, % 185.35/185.44 (P13(f26(f23(f20(a7),f20(a7))),f26(f23(a16,a16)))), % 185.35/185.44 inference(scs_inference,[],[3617,36])). % 185.35/185.44 cnf(3626,plain, % 185.35/185.44 (P3(f20(f23(f20(a7),f20(a7))),f20(f23(a16,a16)))), % 185.35/185.44 inference(scs_inference,[],[3617,36,38])). % 185.35/185.44 cnf(3634,plain, % 185.35/185.44 (P6(f19(x36341,f23(f20(a7),f20(a7))),f19(x36341,f23(a16,a16)))), % 185.35/185.44 inference(scs_inference,[],[3617,10,36,38,37,39,40,63])). % 185.35/185.44 cnf(3644,plain, % 185.35/185.44 (P13(f26(f24(f20(a7),f20(a7))),f26(f24(a16,a16)))), % 185.35/185.44 inference(scs_inference,[],[3619,36])). % 185.35/185.44 cnf(3658,plain, % 185.35/185.44 (P6(f19(a11,f24(f20(a7),f20(a7))),f19(a13,f24(a16,a16)))), % 185.35/185.44 inference(scs_inference,[],[3619,3634,3624,22,7,36,38,39,37,40,62,59,63])). % 185.35/185.44 cnf(3678,plain, % 185.35/185.44 (P3(f17(f26(f24(f20(a7),f20(a7))),x36781),f17(f26(f24(a16,a16)),x36781))), % 185.35/185.44 inference(scs_inference,[],[3626,3644,3658,11,10,36,38,37,39,40,62,59])). % 185.35/185.44 cnf(3939,plain, % 185.35/185.44 (P3(f23(f17(x39391,a13),f17(x39391,a13)),f23(f17(x39391,a11),f17(x39391,a11)))), % 185.35/185.44 inference(scs_inference,[],[3678,7,349,36,38,37,39,40,63,60])). % 185.35/185.44 cnf(3960,plain, % 185.35/185.44 (P3(f23(f23(f17(x39601,a13),f17(x39601,a13)),f23(f17(x39601,a13),f17(x39601,a13))),f23(f23(f17(x39601,a11),f17(x39601,a11)),f23(f17(x39601,a11),f17(x39601,a11))))), % 185.35/185.44 inference(scs_inference,[],[3939,10,36,38,37,39,40,63,60])). % 185.35/185.44 cnf(4172,plain, % 185.35/185.44 (P3(f23(a15,a15),f23(a14,a14))), % 185.35/185.44 inference(scs_inference,[],[3960,89,36,38,37,39,40,60])). % 185.35/185.44 cnf(4174,plain, % 185.35/185.44 (P3(f24(a15,a15),f24(a14,a14))), % 185.35/185.44 inference(scs_inference,[],[3960,89,36,38,37,39,40,60,58])). % 185.35/185.44 cnf(4178,plain, % 185.35/185.44 (P13(f26(f23(a15,a15)),f26(f23(a14,a14)))), % 185.35/185.44 inference(scs_inference,[],[4172,36])). % 185.35/185.44 cnf(4188,plain, % 185.35/185.44 (P6(f19(x41881,f23(a15,a15)),f19(x41881,f23(a14,a14)))), % 185.35/185.44 inference(scs_inference,[],[4172,10,36,38,37,39,40,63])). % 185.35/185.44 cnf(4196,plain, % 185.35/185.44 (P13(f26(f24(a15,a15)),f26(f24(a14,a14)))), % 185.35/185.44 inference(scs_inference,[],[4174,36])). % 185.35/185.44 cnf(4198,plain, % 185.35/185.44 (P3(f20(f24(a15,a15)),f20(f24(a14,a14)))), % 185.35/185.44 inference(scs_inference,[],[4174,36,38])). % 185.35/185.44 cnf(4210,plain, % 185.35/185.44 (P6(f19(a11,f24(a15,a15)),f19(a13,f24(a14,a14)))), % 185.35/185.44 inference(scs_inference,[],[4174,4188,4178,22,7,36,38,37,39,40,62,59,63])). % 185.35/185.44 cnf(4212,plain, % 185.35/185.44 (P3(f23(f24(a15,a15),f24(a15,a15)),f23(f24(a14,a14),f24(a14,a14)))), % 185.35/185.44 inference(scs_inference,[],[4174,4188,4178,22,7,36,38,37,39,40,62,59,63,60])). % 185.35/185.44 cnf(4214,plain, % 185.35/185.44 (P3(f24(f24(a15,a15),f24(a15,a15)),f24(f24(a14,a14),f24(a14,a14)))), % 185.35/185.44 inference(scs_inference,[],[4174,4188,4178,22,7,36,38,37,39,40,62,59,63,60,58])). % 185.35/185.44 cnf(4222,plain, % 185.35/185.44 (P13(f26(f23(f24(a15,a15),f24(a15,a15))),f26(f23(f24(a14,a14),f24(a14,a14))))), % 185.35/185.44 inference(scs_inference,[],[4212,36])). % 185.35/185.44 cnf(4236,plain, % 185.35/185.44 (P6(f19(x42361,f23(f24(a15,a15),f24(a15,a15))),f19(x42361,f23(f24(a14,a14),f24(a14,a14))))), % 185.35/185.44 inference(scs_inference,[],[4212,4196,4210,195,10,36,38,39,37,40,62,59,63])). % 185.35/185.44 cnf(4266,plain, % 185.35/185.44 (P6(f19(a11,f24(f24(a15,a15),f24(a15,a15))),f19(a13,f24(f24(a14,a14),f24(a14,a14))))), % 185.35/185.44 inference(scs_inference,[],[4214,4236,4222,11,7,36,38,37,39,40,62,59,63])). % 185.35/185.44 cnf(4287,plain, % 185.35/185.44 (P5(f18(f28(a3),f19(a11,f24(f24(a15,a15),f24(a15,a15)))),f18(a2,f19(a13,f24(f24(a14,a14),f24(a14,a14)))))), % 185.35/185.44 inference(scs_inference,[],[4198,4266,22,36,38,39,37,40,62])). % 185.35/185.44 cnf(5243,plain, % 185.35/185.44 (P3(f17(x52431,a11),f17(x52431,a13))), % 185.35/185.44 inference(scs_inference,[],[3419,7,13,38,37,36,39,40,59])). % 185.35/185.44 cnf(6168,plain, % 185.35/185.44 (P3(f20(a16),f20(f20(a7)))), % 185.35/185.44 inference(scs_inference,[],[26,22,19,7,15,293,60,58,63,62,38])). % 185.35/185.44 cnf(6170,plain, % 185.35/185.44 (P3(f21(a16),f21(f20(a7)))), % 185.35/185.44 inference(scs_inference,[],[26,22,19,7,15,293,60,58,63,62,38,37])). % 185.35/185.44 cnf(6178,plain, % 185.35/185.44 (P5(f10(f18(f28(a3),f19(a11,a14))),f10(f18(a2,f19(a11,a15))))), % 185.35/185.44 inference(scs_inference,[],[26,22,19,7,15,293,60,58,63,62,38,37,39,40,36,42])). % 185.35/185.44 cnf(6182,plain, % 185.35/185.44 (P6(f19(x61821,f17(f26(a16),a13)),f19(x61821,f23(f17(f26(a12),a13),f20(f22(a7)))))), % 185.35/185.44 inference(scs_inference,[],[26,10,6168,60,63])). % 185.35/185.44 cnf(6186,plain, % 185.35/185.44 (P5(f10(f10(f18(f28(a3),f19(a11,a14)))),f10(f10(f18(a2,f19(a11,a15)))))), % 185.35/185.44 inference(scs_inference,[],[26,27,10,6178,6168,60,63,37,42])). % 185.35/185.44 cnf(6215,plain, % 185.35/185.44 (P3(f23(f21(a16),f21(a16)),f23(f21(f20(a7)),f21(f20(a7))))), % 185.35/185.44 inference(scs_inference,[],[6170,2454,41,60])). % 185.35/185.44 cnf(6217,plain, % 185.35/185.44 (P3(f21(a14),f21(a15))), % 185.35/185.44 inference(scs_inference,[],[8,6170,2454,41,60,37])). % 185.35/185.44 cnf(6227,plain, % 185.35/185.44 (P3(f24(f21(a16),f21(a16)),f24(f21(f20(a7)),f21(f20(a7))))), % 185.35/185.44 inference(scs_inference,[],[22,27,8,7,6186,6182,6170,2454,41,60,37,62,63,39,42,58])). % 185.35/185.44 cnf(6233,plain, % 185.35/185.44 (P13(f26(a14),f26(a15))), % 185.35/185.44 inference(scs_inference,[],[22,27,8,7,6186,6182,6170,2454,41,60,37,62,63,39,42,58,38,40,36])). % 185.35/185.44 cnf(6246,plain, % 185.35/185.44 (P3(f23(f23(f21(a16),f21(a16)),f23(f21(a16),f21(a16))),f23(f23(f21(f20(a7)),f21(f20(a7))),f23(f21(f20(a7)),f21(f20(a7)))))), % 185.35/185.44 inference(scs_inference,[],[6215,60])). % 185.35/185.44 cnf(6273,plain, % 185.35/185.44 (P3(f23(f24(f21(a16),f21(a16)),f24(f21(a16),f21(a16))),f23(f24(f21(f20(a7)),f21(f20(a7))),f24(f21(f20(a7)),f21(f20(a7)))))), % 185.35/185.44 inference(scs_inference,[],[6227,60])). % 185.35/185.44 cnf(6281,plain, % 185.35/185.44 (P6(f19(a11,a14),f19(a13,a15))), % 185.35/185.44 inference(scs_inference,[],[8,7,6246,6227,4287,60,37,39,42,63])). % 185.35/185.44 cnf(6285,plain, % 185.35/185.44 (P3(f24(f24(f21(a16),f21(a16)),f24(f21(a16),f21(a16))),f24(f24(f21(f20(a7)),f21(f20(a7))),f24(f21(f20(a7)),f21(f20(a7)))))), % 185.35/185.44 inference(scs_inference,[],[8,7,6246,6227,4287,60,37,39,42,63,38,58])). % 185.35/185.44 cnf(6301,plain, % 185.35/185.44 (P3(f23(f21(a14),f21(a14)),f23(f21(a15),f21(a15)))), % 185.35/185.44 inference(scs_inference,[],[6273,6217,3165,42,39,37,60])). % 185.35/185.44 cnf(6349,plain, % 185.35/185.44 (~P3(f17(f26(a14),a11),f17(f26(f24(a14,f20(f22(a7)))),a13))), % 185.35/185.44 inference(scs_inference,[],[22,29,7,6233,6285,6301,6281,2523,392,39,37,42,60,36,38,58,40,59,62,55,1597,1596,48])). % 185.35/185.44 cnf(6357,plain, % 185.35/185.44 ($false), % 185.35/185.44 inference(scs_inference,[],[29,6349,5243,48]), % 185.35/185.44 ['proof']). % 185.35/185.45 % SZS output end Proof % 185.35/185.45 % Total time :184.670000s %------------------------------------------------------------------------------