%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN698-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:20 EDT 2024 % Result : Unsatisfiable 186.94s 186.96s % Output : CNFRefutation 186.94s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SYN698-1 : TPTP v8.2.0. Released v2.5.0. % 0.06/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n028.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 20:05:53 EDT 2024 % 0.12/0.33 % CPUTime : % 0.19/0.56 start to proof:theBenchmark % 186.94/186.93 %------------------------------------------- % 186.94/186.93 % File :CSE---1.7 % 186.94/186.93 % Problem :theBenchmark % 186.94/186.93 % Transform :cnf % 186.94/186.93 % Format :tptp:raw % 186.94/186.93 % Command :java -jar mcs_scs.jar %d %s % 186.94/186.93 % 186.94/186.93 % Result :Theorem 186.340000s % 186.94/186.93 % Output :CNFRefutation 186.340000s % 186.94/186.93 %------------------------------------------- % 186.94/186.95 %-------------------------------------------------------------------------- % 186.94/186.95 % File : SYN698-1 : TPTP v8.2.0. Released v2.5.0. % 186.94/186.95 % Domain : Syntactic % 186.94/186.95 % Problem : Harrison problem 4650 % 186.94/186.95 % Version : Especial. % 186.94/186.95 % English : % 186.94/186.95 % 186.94/186.95 % Refs : [Har01] Email to G. Sutcliffe % 186.94/186.95 % Source : [Har01] % 186.94/186.95 % Names : % 186.94/186.95 % 186.94/186.95 % Status : Unsatisfiable % 186.94/186.95 % Rating : 0.08 v8.2.0, 0.14 v8.1.0, 0.00 v7.4.0, 0.17 v7.0.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.36 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 % 186.94/186.95 % Syntax : Number of clauses : 74 ( 31 unt; 2 nHn; 64 RR) % 186.94/186.95 % Number of literals : 156 ( 0 equ; 82 neg) % 186.94/186.95 % Maximal clause size : 5 ( 2 avg) % 186.94/186.95 % Maximal term depth : 6 ( 1 avg) % 186.94/186.95 % Number of predicates : 18 ( 18 usr; 0 prp; 1-3 aty) % 186.94/186.95 % Number of functors : 29 ( 29 usr; 15 con; 0-2 aty) % 186.94/186.95 % Number of variables : 132 ( 5 sgn) % 186.94/186.95 % SPC : CNF_UNS_RFO_NEQ_NHN % 186.94/186.95 % 186.94/186.95 % Comments : % 186.94/186.95 %-------------------------------------------------------------------------- % 186.94/186.95 cnf(c34_is_p25_1,negated_conjecture, % 186.94/186.95 p25(c34) ). % 186.94/186.95 % 186.94/186.95 cnf(c36_is_p29_2,negated_conjecture, % 186.94/186.95 p29(c36) ). % 186.94/186.95 % 186.94/186.95 cnf(f18_is_p30_3,negated_conjecture, % 186.94/186.95 p30(f18(c41)) ). % 186.94/186.95 % 186.94/186.95 cnf(f16_is_p28_4,negated_conjecture, % 186.94/186.95 p28(f16(c38)) ). % 186.94/186.95 % 186.94/186.95 cnf(f16_is_p28_5,negated_conjecture, % 186.94/186.95 p28(f16(c39)) ). % 186.94/186.95 % 186.94/186.95 cnf(f18_is_p30_6,negated_conjecture, % 186.94/186.95 p30(f18(c40)) ). % 186.94/186.95 % 186.94/186.95 cnf(p10_7,negated_conjecture, % 186.94/186.95 p10(X5,X5) ). % 186.94/186.95 % 186.94/186.95 cnf(p7_8,negated_conjecture, % 186.94/186.95 p7(X112,X112) ). % 186.94/186.95 % 186.94/186.95 cnf(p6_9,negated_conjecture, % 186.94/186.95 p6(X109,X109) ). % 186.94/186.95 % 186.94/186.95 cnf(p3_10,negated_conjecture, % 186.94/186.95 p3(X88,X88) ). % 186.94/186.95 % 186.94/186.95 cnf(p21_11,negated_conjecture, % 186.94/186.95 p21(X68,X68) ). % 186.94/186.95 % 186.94/186.95 cnf(p2_12,negated_conjecture, % 186.94/186.95 p2(X43,X43) ). % 186.94/186.95 % 186.94/186.95 cnf(p17_13,negated_conjecture, % 186.94/186.95 p17(X28,X28) ). % 186.94/186.95 % 186.94/186.95 cnf(p14_14,negated_conjecture, % 186.94/186.95 p14(X19,X19) ). % 186.94/186.95 % 186.94/186.95 cnf(p12_15,negated_conjecture, % 186.94/186.95 p12(X12,X12) ). % 186.94/186.95 % 186.94/186.95 cnf(p10_16,negated_conjecture, % 186.94/186.95 p10(c45,c48) ). % 186.94/186.95 % 186.94/186.95 cnf(p31_17,negated_conjecture, % 186.94/186.95 p31(c47,c42) ). % 186.94/186.95 % 186.94/186.95 cnf(p2_18,negated_conjecture, % 186.94/186.95 p2(c44,c46) ). % 186.94/186.95 % 186.94/186.95 cnf(p31_19,negated_conjecture, % 186.94/186.95 p31(c46,f5(c42)) ). % 186.94/186.95 % 186.94/186.95 cnf(p2_20,negated_conjecture, % 186.94/186.95 p2(c47,f9(c37)) ). % 186.94/186.95 % 186.94/186.95 cnf(p31_21,negated_conjecture, % 186.94/186.95 p31(c44,f5(c42)) ). % 186.94/186.95 % 186.94/186.95 cnf(p7_22,negated_conjecture, % 186.94/186.95 p7(f8(c35),c36) ). % 186.94/186.95 % 186.94/186.95 cnf(p32_23,negated_conjecture, % 186.94/186.95 p32(f22(c34,c45),c43) ). % 186.94/186.95 % 186.94/186.95 cnf(p31_24,negated_conjecture, % 186.94/186.95 p31(f23(c44,f9(f20(c37))),c46) ). % 186.94/186.95 % 186.94/186.95 cnf(p26_25,negated_conjecture, % 186.94/186.95 p26(c34,f4(f5(X79)),f4(X79)) ). % 186.94/186.95 % 186.94/186.95 cnf(p25_26,negated_conjecture, % 186.94/186.95 ( p25(X71) % 186.94/186.95 | ~ p25(X72) % 186.94/186.95 | ~ p21(X72,X71) ) ). % 186.94/186.95 % 186.94/186.95 cnf(p30_27,negated_conjecture, % 186.94/186.95 ( p30(X93) % 186.94/186.95 | ~ p30(X94) % 186.94/186.95 | ~ p17(X94,X93) ) ). % 186.94/186.95 % 186.94/186.95 cnf(p29_28,negated_conjecture, % 186.94/186.95 ( p29(X86) % 186.94/186.95 | ~ p29(X87) % 186.94/186.95 | ~ p7(X87,X86) ) ). % 186.94/186.95 % 186.94/186.95 cnf(p28_29,negated_conjecture, % 186.94/186.95 ( p28(X84) % 186.94/186.95 | ~ p28(X85) % 186.94/186.95 | ~ p14(X85,X84) ) ). % 186.94/186.95 % 186.94/186.95 cnf(p7_30,negated_conjecture, % 186.94/186.95 ( p7(f8(X115),f8(X116)) % 186.94/186.95 | ~ p6(X115,X116) ) ). % 186.94/186.95 % 186.94/186.95 cnf(p14_31,negated_conjecture, % 186.94/186.95 ( p14(f16(X26),f16(X27)) % 186.94/186.95 | ~ p14(X26,X27) ) ). % 186.94/186.95 % 186.94/186.95 cnf(p17_32,negated_conjecture, % 186.94/186.95 ( p17(f18(X31),f18(X32)) % 186.94/186.95 | ~ p17(X31,X32) ) ). % 186.94/186.95 % 186.94/186.95 cnf(p2_33,negated_conjecture, % 186.94/186.95 ( p2(f20(X56),f20(X57)) % 186.94/186.95 | ~ p2(X56,X57) ) ). % 186.94/186.95 % 186.94/186.95 cnf(p2_34,negated_conjecture, % 186.94/186.95 ( p2(f24(X62),f24(X63)) % 186.94/186.95 | ~ p2(X62,X63) ) ). % 186.94/186.95 % 186.94/186.95 cnf(p2_35,negated_conjecture, % 186.94/186.95 ( p2(f5(X64),f5(X65)) % 186.94/186.95 | ~ p2(X64,X65) ) ). % 186.94/186.95 % 186.94/186.95 cnf(p2_36,negated_conjecture, % 186.94/186.95 ( p2(f9(X66),f9(X67)) % 186.94/186.95 | ~ p2(X66,X67) ) ). % 186.94/186.95 % 186.94/186.95 cnf(p3_37,negated_conjecture, % 186.94/186.95 ( p3(f4(X91),f4(X92)) % 186.94/186.95 | ~ p2(X91,X92) ) ). % 186.94/186.95 % 186.94/186.95 cnf(p10_38,negated_conjecture, % 186.94/186.95 ( p10(X6,X7) % 186.94/186.95 | ~ p10(X5,X6) % 186.94/186.95 | ~ p10(X5,X7) ) ). % 186.94/186.95 % 186.94/186.95 cnf(p7_39,negated_conjecture, % 186.94/186.95 ( p7(X113,X114) % 186.94/186.95 | ~ p7(X112,X113) % 186.94/186.95 | ~ p7(X112,X114) ) ). % 186.94/186.95 % 186.94/186.95 cnf(p6_40,negated_conjecture, % 186.94/186.95 ( p6(X110,X111) % 186.94/186.95 | ~ p6(X109,X110) % 186.94/186.95 | ~ p6(X109,X111) ) ). % 186.94/186.95 % 186.94/186.95 cnf(p3_41,negated_conjecture, % 186.94/186.95 ( p3(X89,X90) % 186.94/186.95 | ~ p3(X88,X89) % 186.94/186.95 | ~ p3(X88,X90) ) ). % 186.94/186.95 % 186.94/186.95 cnf(p21_42,negated_conjecture, % 186.94/186.95 ( p21(X69,X70) % 186.94/186.95 | ~ p21(X68,X69) % 186.94/186.95 | ~ p21(X68,X70) ) ). % 186.94/186.95 % 186.94/186.95 cnf(p2_43,negated_conjecture, % 186.94/186.96 ( p2(X44,X45) % 186.94/186.96 | ~ p2(X43,X44) % 186.94/186.96 | ~ p2(X43,X45) ) ). % 186.94/186.96 % 186.94/186.96 cnf(p17_44,negated_conjecture, % 186.94/186.96 ( p17(X29,X30) % 186.94/186.96 | ~ p17(X28,X29) % 186.94/186.96 | ~ p17(X28,X30) ) ). % 186.94/186.96 % 186.94/186.96 cnf(p14_45,negated_conjecture, % 186.94/186.96 ( p14(X20,X21) % 186.94/186.96 | ~ p14(X19,X20) % 186.94/186.96 | ~ p14(X19,X21) ) ). % 186.94/186.96 % 186.94/186.96 cnf(p12_46,negated_conjecture, % 186.94/186.96 ( p12(X13,X14) % 186.94/186.96 | ~ p12(X12,X13) % 186.94/186.96 | ~ p12(X12,X14) ) ). % 186.94/186.96 % 186.94/186.96 cnf(p33_47,negated_conjecture, % 186.94/186.96 p33(f11(f4(f5(c42)),c45),f11(f4(c42),c45)) ). % 186.94/186.96 % 186.94/186.96 cnf(p31_48,negated_conjecture, % 186.94/186.96 ( p31(X95,f24(X95)) % 186.94/186.96 | ~ p31(X95,c44) % 186.94/186.96 | ~ p31(X95,f5(c42)) ) ). % 186.94/186.96 % 186.94/186.96 cnf(p31_49,negated_conjecture, % 186.94/186.96 ( p31(f24(X95),f5(c42)) % 186.94/186.96 | ~ p31(X95,c44) % 186.94/186.96 | ~ p31(X95,f5(c42)) ) ). % 186.94/186.96 % 186.94/186.96 cnf(p33_50,negated_conjecture, % 186.94/186.96 ( p33(X105,X106) % 186.94/186.96 | ~ p2(X108,X106) % 186.94/186.96 | ~ p33(X107,X108) % 186.94/186.96 | ~ p2(X107,X105) ) ). % 186.94/186.96 % 186.94/186.96 cnf(p27_51,negated_conjecture, % 186.94/186.96 ( p27(X80,X81) % 186.94/186.96 | ~ p14(X83,X80) % 186.94/186.96 | ~ p27(X83,X82) % 186.94/186.96 | ~ p12(X82,X81) ) ). % 186.94/186.96 % 186.94/186.96 cnf(p31_52,negated_conjecture, % 186.94/186.96 ( p31(X96,X97) % 186.94/186.96 | ~ p2(X99,X97) % 186.94/186.96 | ~ p31(X98,X99) % 186.94/186.96 | ~ p2(X98,X96) ) ). % 186.94/186.96 % 186.94/186.96 cnf(p32_53,negated_conjecture, % 186.94/186.96 ( p32(X100,X101) % 186.94/186.96 | ~ p17(X103,X100) % 186.94/186.96 | ~ p32(X103,X102) % 186.94/186.96 | ~ p10(X102,X101) ) ). % 186.94/186.96 % 186.94/186.96 cnf(p2_54,negated_conjecture, % 186.94/186.96 p2(f11(f4(c47),c48),f19(f11(f4(c42),c48),f9(f20(c37)))) ). % 186.94/186.96 % 186.94/186.96 cnf(p31_55,negated_conjecture, % 186.94/186.96 p31(f11(f4(c42),c45),f11(f4(f23(c42,f9(f20(c37)))),c45)) ). % 186.94/186.96 % 186.94/186.96 cnf(p2_56,negated_conjecture, % 186.94/186.96 p2(f11(f4(f23(c44,f9(f20(c37)))),c43),f11(f4(c44),c43)) ). % 186.94/186.96 % 186.94/186.96 cnf(not_p2_57,negated_conjecture, % 186.94/186.96 ~ p2(f11(f4(c46),c43),f11(f4(f23(c44,f9(f20(c37)))),c43)) ). % 186.94/186.96 % 186.94/186.96 cnf(p10_58,negated_conjecture, % 186.94/186.96 ( p10(X0,c43) % 186.94/186.96 | ~ p31(f11(f4(f5(c42)),X0),f11(f4(c42),X0)) ) ). % 186.94/186.96 % 186.94/186.96 cnf(p12_59,negated_conjecture, % 186.94/186.96 ( p12(f13(X15,X16),f13(X17,X18)) % 186.94/186.96 | ~ p10(X15,X17) % 186.94/186.96 | ~ p2(X16,X18) ) ). % 186.94/186.96 % 186.94/186.96 cnf(p2_60,negated_conjecture, % 186.94/186.96 ( p2(f23(X58,X59),f23(X60,X61)) % 186.94/186.96 | ~ p2(X58,X60) % 186.94/186.96 | ~ p2(X59,X61) ) ). % 186.94/186.96 % 186.94/186.96 cnf(p2_61,negated_conjecture, % 186.94/186.96 ( p2(f19(X52,X53),f19(X54,X55)) % 186.94/186.96 | ~ p2(X52,X54) % 186.94/186.96 | ~ p2(X53,X55) ) ). % 186.94/186.96 % 186.94/186.96 cnf(p2_62,negated_conjecture, % 186.94/186.96 ( p2(f11(X46,X47),f11(X48,X49)) % 186.94/186.96 | ~ p10(X47,X49) % 186.94/186.96 | ~ p3(X46,X48) ) ). % 186.94/186.96 % 186.94/186.96 cnf(p17_63,negated_conjecture, % 186.94/186.96 ( p17(f22(X33,X34),f22(X35,X36)) % 186.94/186.96 | ~ p10(X34,X36) % 186.94/186.96 | ~ p21(X33,X35) ) ). % 186.94/186.96 % 186.94/186.96 cnf(p14_64,negated_conjecture, % 186.94/186.96 ( p14(f15(X22,X23),f15(X24,X25)) % 186.94/186.96 | ~ p12(X23,X25) % 186.94/186.96 | ~ p7(X22,X24) ) ). % 186.94/186.96 % 186.94/186.96 cnf(p2_65,negated_conjecture, % 186.94/186.96 p2(f19(f11(f4(f5(c42)),c43),f9(f20(c37))),f11(f4(c42),c43)) ). % 186.94/186.96 % 186.94/186.96 cnf(p32_66,negated_conjecture, % 186.94/186.96 ( p32(f22(c34,X104),c43) % 186.94/186.96 | ~ p33(f11(f4(f5(c42)),X104),f11(f4(c42),X104)) ) ). % 186.94/186.96 % 186.94/186.96 cnf(p2_67,negated_conjecture, % 186.94/186.96 ( p2(f11(f4(X51),c48),f11(f4(c47),c48)) % 186.94/186.96 | ~ p31(X51,c42) % 186.94/186.96 | ~ p31(c47,X51) ) ). % 186.94/186.96 % 186.94/186.96 cnf(p2_68,negated_conjecture, % 186.94/186.96 ( p2(f11(f4(X50),c43),f11(f4(c44),c43)) % 186.94/186.96 | ~ p31(c44,X50) % 186.94/186.96 | ~ p31(X50,f5(c42)) ) ). % 186.94/186.96 % 186.94/186.96 cnf(p10_69,negated_conjecture, % 186.94/186.96 ( p10(X1,X2) % 186.94/186.96 | p32(f22(c34,X1),X2) % 186.94/186.96 | ~ p27(f15(c36,f13(X1,X3)),f13(X2,X4)) ) ). % 186.94/186.96 % 186.94/186.96 cnf(not_p31_70,negated_conjecture, % 186.94/186.96 ( ~ p31(X95,c44) % 186.94/186.96 | ~ p31(X95,f5(c42)) % 186.94/186.96 | ~ p2(f11(f4(f24(X95)),c43),f11(f4(X95),c43)) ) ). % 186.94/186.96 % 186.94/186.96 cnf(p26_71,negated_conjecture, % 186.94/186.96 ( p26(X73,X74,X75) % 186.94/186.96 | ~ p3(X78,X75) % 186.94/186.96 | ~ p3(X77,X74) % 186.94/186.96 | ~ p21(X76,X73) % 186.94/186.96 | ~ p26(X76,X77,X78) ) ). % 186.94/186.96 % 186.94/186.96 cnf(p10_72,negated_conjecture, % 186.94/186.96 ( p10(X8,X9) % 186.94/186.96 | ~ p2(f11(f4(X10),X8),f9(c37)) % 186.94/186.96 | ~ p27(f15(c36,f13(X8,X10)),f13(X9,X11)) ) ). % 186.94/186.96 % 186.94/186.96 cnf(p2_73,negated_conjecture, % 186.94/186.96 ( p2(X37,X38) % 186.94/186.96 | ~ p27(f15(c36,f13(X39,X37)),f13(X40,X41)) % 186.94/186.96 | ~ p27(f15(c36,f13(X42,X38)),f13(X40,X41)) ) ). % 186.94/186.96 % 186.94/186.96 cnf(p32_74,negated_conjecture, % 186.94/186.96 ( p32(f22(c34,X1),X2) % 186.94/186.96 | p31(f11(f4(X3),X2),f11(f4(X4),X2)) % 186.94/186.96 | ~ p27(f15(c36,f13(X1,X3)),f13(X2,X4)) ) ). % 186.94/186.96 % 186.94/186.96 %-------------------------------------------------------------------------- % 186.94/186.96 %------------------------------------------- % 186.94/186.96 % Proof found % 186.94/186.96 % SZS status Theorem for theBenchmark % 186.94/186.96 % SZS output start Proof % 186.94/186.96 %ClaNum:74(EqnAxiom:0) % 186.94/186.96 %VarNum:273(SingletonVarNum:132) % 186.94/186.96 %MaxLitNum:5 % 186.94/186.96 %MaxfuncDepth:5 % 186.94/186.96 %SharedTerms:67 % 186.94/186.96 %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 % 186.94/186.96 %singleGoalClaCount:31 % 186.94/186.96 [1]P1(a1) % 186.94/186.96 [2]P8(a2) % 186.94/186.96 [7]P2(a11,a15) % 186.94/186.96 [8]P3(a12,a16) % 186.94/186.96 [9]P14(a17,a13) % 186.94/186.96 [3]P12(f9(a4)) % 186.94/186.96 [4]P12(f9(a5)) % 186.94/186.96 [5]P9(f10(a6)) % 186.94/186.96 [6]P9(f10(a8)) % 186.94/186.96 [19]P3(a17,f21(a7)) % 186.94/186.96 [20]P14(a12,f22(a13)) % 186.94/186.96 [21]P14(a16,f22(a13)) % 186.94/186.96 [22]P15(f29(a3),a2) % 186.94/186.96 [23]P17(f23(a1,a11),a14) % 186.94/186.96 [24]P14(f26(a12,f21(f24(a7))),a16) % 186.94/186.96 [26]P18(f18(f27(f22(a13)),a11),f18(f27(a13),a11)) % 186.94/186.96 [27]P3(f18(f27(a17),a15),f25(f18(f27(a13),a15),f21(f24(a7)))) % 186.94/186.96 [28]P3(f25(f18(f27(f22(a13)),a14),f21(f24(a7))),f18(f27(a13),a14)) % 186.94/186.96 [29]P14(f18(f27(a13),a11),f18(f27(f26(a13,f21(f24(a7)))),a11)) % 186.94/186.96 [30]P3(f18(f27(f26(a12,f21(f24(a7)))),a14),f18(f27(a12),a14)) % 186.94/186.96 [31]~P3(f18(f27(a16),a14),f18(f27(f26(a12,f21(f24(a7)))),a14)) % 186.94/186.96 [10]P2(x101,x101) % 186.94/186.96 [11]P15(x111,x111) % 186.94/186.96 [12]P16(x121,x121) % 186.94/186.96 [13]P13(x131,x131) % 186.94/186.96 [14]P7(x141,x141) % 186.94/186.96 [15]P3(x151,x151) % 186.94/186.96 [16]P4(x161,x161) % 186.94/186.96 [17]P5(x171,x171) % 186.94/186.96 [18]P6(x181,x181) % 186.94/186.96 [25]P10(a1,f27(f22(x251)),f27(x251)) % 186.94/186.96 [67]P2(x671,a14)+~P14(f18(f27(f22(a13)),x671),f18(f27(a13),x671)) % 186.94/186.96 [68]P17(f23(a1,x681),a14)+~P18(f18(f27(f22(a13)),x681),f18(f27(a13),x681)) % 186.94/186.96 [36]~P16(x361,x362)+P15(f29(x361),f29(x362)) % 186.94/186.96 [37]~P3(x371,x372)+P13(f27(x371),f27(x372)) % 186.94/186.96 [38]~P3(x381,x382)+P3(f22(x381),f22(x382)) % 186.94/186.96 [39]~P3(x391,x392)+P3(f21(x391),f21(x392)) % 186.94/186.96 [40]~P3(x401,x402)+P3(f24(x401),f24(x402)) % 186.94/186.96 [41]~P3(x411,x412)+P3(f28(x411),f28(x412)) % 186.94/186.96 [42]~P4(x421,x422)+P4(f9(x421),f9(x422)) % 186.94/186.96 [43]~P5(x431,x432)+P5(f10(x431),f10(x432)) % 186.94/186.96 [53]~P14(x531,a12)+P14(x531,f28(x531))+~P14(x531,f22(a13)) % 186.94/186.96 [54]~P14(x541,a12)+~P14(x541,f22(a13))+P14(f28(x541),f22(a13)) % 186.94/186.96 [65]~P14(x651,a13)+~P14(a17,x651)+P3(f18(f27(x651),a15),f18(f27(a17),a15)) % 186.94/186.96 [66]~P14(a12,x661)+~P14(x661,f22(a13))+P3(f18(f27(x661),a14),f18(f27(a12),a14)) % 186.94/186.96 [70]~P14(x701,a12)+~P14(x701,f22(a13))+~P3(f18(f27(f28(x701)),a14),f18(f27(x701),a14)) % 186.94/186.96 [32]~P7(x322,x321)+P1(x321)+~P1(x322) % 186.94/186.96 [33]~P15(x332,x331)+P8(x331)+~P8(x332) % 186.94/186.96 [34]~P4(x342,x341)+P12(x341)+~P12(x342) % 186.94/186.96 [35]~P5(x352,x351)+P9(x351)+~P9(x352) % 186.94/186.96 [44]~P2(x443,x441)+P2(x441,x442)+~P2(x443,x442) % 186.94/186.96 [45]~P15(x453,x451)+P15(x451,x452)+~P15(x453,x452) % 186.94/186.96 [46]~P16(x463,x461)+P16(x461,x462)+~P16(x463,x462) % 186.94/186.96 [47]~P13(x473,x471)+P13(x471,x472)+~P13(x473,x472) % 186.94/186.96 [48]~P7(x483,x481)+P7(x481,x482)+~P7(x483,x482) % 186.94/186.96 [49]~P3(x493,x491)+P3(x491,x492)+~P3(x493,x492) % 186.94/186.96 [50]~P4(x503,x501)+P4(x501,x502)+~P4(x503,x502) % 186.94/186.96 [51]~P5(x513,x511)+P5(x511,x512)+~P5(x513,x512) % 186.94/186.96 [52]~P6(x523,x521)+P6(x521,x522)+~P6(x523,x522) % 186.94/186.96 [59]~P3(x592,x594)+~P3(x591,x593)+P3(f26(x591,x592),f26(x593,x594)) % 186.94/186.96 [60]~P2(x602,x604)+~P13(x601,x603)+P3(f18(x601,x602),f18(x603,x604)) % 186.94/186.96 [61]~P3(x612,x614)+~P3(x611,x613)+P3(f25(x611,x612),f25(x613,x614)) % 186.94/186.96 [62]~P2(x622,x624)+~P7(x621,x623)+P4(f23(x621,x622),f23(x623,x624)) % 186.94/186.96 [63]~P15(x631,x633)+~P6(x632,x634)+P5(f19(x631,x632),f19(x633,x634)) % 186.94/186.96 [64]~P2(x641,x643)+~P3(x642,x644)+P6(f20(x641,x642),f20(x643,x644)) % 186.94/186.96 [71]P2(x711,x712)+P17(f23(a1,x711),x712)+~P11(f19(a2,f20(x711,x713)),f20(x712,x714)) % 186.94/186.96 [72]P2(x721,x722)+~P11(f19(a2,f20(x721,x723)),f20(x722,x724))+~P3(f18(f27(x723),x721),f21(a7)) % 186.94/186.96 [73]P17(f23(a1,x731),x732)+P14(f18(f27(x733),x732),f18(f27(x734),x732))+~P11(f19(a2,f20(x731,x733)),f20(x732,x734)) % 186.94/186.96 [74]P3(x741,x742)+~P11(f19(a2,f20(x743,x742)),f20(x744,x745))+~P11(f19(a2,f20(x746,x741)),f20(x744,x745)) % 186.94/186.96 [55]~P14(x553,x554)+P14(x551,x552)+~P3(x553,x551)+~P3(x554,x552) % 186.94/186.96 [56]~P17(x564,x563)+P17(x561,x562)+~P2(x563,x562)+~P4(x564,x561) % 186.94/186.96 [57]~P18(x573,x574)+P18(x571,x572)+~P3(x573,x571)+~P3(x574,x572) % 186.94/186.96 [58]~P11(x583,x584)+P11(x581,x582)+~P5(x583,x581)+~P6(x584,x582) % 186.94/186.96 [69]~P10(x696,x694,x695)+P10(x691,x692,x693)+~P13(x694,x692)+~P13(x695,x693)+~P7(x696,x691) % 186.94/186.96 %EqnAxiom % 186.94/186.96 % 186.94/186.96 %------------------------------------------- % 186.94/186.98 cnf(87,plain, % 186.94/186.98 (P3(a16,a12)), % 186.94/186.98 inference(scs_inference,[],[8,15,49])). % 186.94/186.98 cnf(114,plain, % 186.94/186.98 (P2(a15,a11)), % 186.94/186.98 inference(scs_inference,[],[7,10,44])). % 186.94/186.98 cnf(193,plain, % 186.94/186.98 (P15(a2,f29(a3))), % 186.94/186.98 inference(scs_inference,[],[22,11,45])). % 186.94/186.98 cnf(198,plain, % 186.94/186.98 (P3(f22(f21(a16)),f22(f21(a12)))), % 186.94/186.98 inference(scs_inference,[],[87,38,39])). % 186.94/186.98 cnf(203,plain, % 186.94/186.98 (P3(f24(f28(a16)),f24(f28(a12)))), % 186.94/186.98 inference(scs_inference,[],[87,40,41])). % 186.94/186.98 cnf(208,plain, % 186.94/186.98 (P4(f9(f23(x2081,a15)),f9(f23(x2081,a11)))), % 186.94/186.98 inference(scs_inference,[],[114,14,42,62])). % 186.94/186.98 cnf(209,plain, % 186.94/186.98 (P4(f9(f23(x2091,a11)),f9(f23(x2091,a15)))), % 186.94/186.98 inference(scs_inference,[],[208,16,50])). % 186.94/186.98 cnf(217,plain, % 186.94/186.98 (P5(f10(f19(a2,x2171)),f10(f19(f29(a3),x2171)))), % 186.94/186.98 inference(scs_inference,[],[193,18,43,63])). % 186.94/186.98 cnf(218,plain, % 186.94/186.98 (P5(f10(f19(f29(a3),x2181)),f10(f19(a2,x2181)))), % 186.94/186.98 inference(scs_inference,[],[217,17,51])). % 186.94/186.98 cnf(336,plain, % 186.94/186.98 (P3(f18(x3361,a15),f18(x3361,a11))), % 186.94/186.98 inference(scs_inference,[],[13,114,47,60])). % 186.94/186.98 cnf(348,plain, % 186.94/186.98 (P6(f20(a11,f22(f21(a16))),f20(a11,f22(f21(a12))))), % 186.94/186.98 inference(scs_inference,[],[198,114,64,44])). % 186.94/186.98 cnf(1491,plain, % 186.94/186.98 (P13(f27(f22(f18(x14911,a15))),f27(f22(f18(x14911,a11))))), % 186.94/186.98 inference(scs_inference,[],[336,38,37])). % 186.94/186.98 cnf(1520,plain, % 186.94/186.98 (P13(f27(f22(f18(x15201,a11))),f27(f22(f18(x15201,a15))))), % 186.94/186.98 inference(scs_inference,[],[1491,13,47])). % 186.94/186.98 cnf(1895,plain, % 186.94/186.98 (P3(f28(f26(f22(f21(a16)),f22(f21(a16)))),f28(f26(f22(f21(a12)),f22(f21(a12)))))), % 186.94/186.98 inference(scs_inference,[],[198,41,59])). % 186.94/186.98 cnf(2075,plain, % 186.94/186.98 (P3(f28(f22(a12)),f28(f22(a16)))), % 186.94/186.98 inference(scs_inference,[],[8,41,38])). % 186.94/186.98 cnf(2581,plain, % 186.94/186.98 (P4(f9(f9(f23(x25811,a15))),f9(f9(f23(x25811,a11))))), % 186.94/186.98 inference(scs_inference,[],[1895,208,38,39,40,41,42])). % 186.94/186.98 cnf(2587,plain, % 186.94/186.98 (P3(f26(f28(f22(a12)),f28(f22(a12))),f26(f28(f22(a16)),f28(f22(a16))))), % 186.94/186.98 inference(scs_inference,[],[1895,2075,217,208,38,39,40,41,42,43,37,59])). % 186.94/186.98 cnf(2589,plain, % 186.94/186.98 (P3(f25(f28(f22(a12)),f28(f22(a12))),f25(f28(f22(a16)),f28(f22(a16))))), % 186.94/186.98 inference(scs_inference,[],[1895,2075,217,208,38,39,40,41,42,43,37,59,61])). % 186.94/186.98 cnf(2612,plain, % 186.94/186.98 (P4(f9(f9(f9(f23(x26121,a15)))),f9(f9(f9(f23(x26121,a11)))))), % 186.94/186.98 inference(scs_inference,[],[2581,2587,37,41,40,42])). % 186.94/186.98 cnf(2641,plain, % 186.94/186.98 (P4(f9(f9(f23(x26411,a11))),f9(f9(f23(x26411,a15))))), % 186.94/186.98 inference(scs_inference,[],[2589,209,37,42])). % 186.94/186.98 cnf(2651,plain, % 186.94/186.98 (P5(f10(f10(f19(f29(a3),x26511))),f10(f10(f19(a2,x26511))))), % 186.94/186.98 inference(scs_inference,[],[2589,218,209,37,42,40,39,38,41,43])). % 186.94/186.98 cnf(2655,plain, % 186.94/186.98 (P3(f25(f24(f28(a16)),f24(f28(a16))),f25(f24(f28(a12)),f24(f28(a12))))), % 186.94/186.98 inference(scs_inference,[],[2589,203,7,218,209,37,42,40,39,38,41,43,64,61])). % 186.94/186.98 cnf(2678,plain, % 186.94/186.98 (P4(f9(f9(f9(f23(x26781,a11)))),f9(f9(f9(f23(x26781,a15)))))), % 186.94/186.98 inference(scs_inference,[],[2641,2655,39,37,40,38,42])). % 186.94/186.98 cnf(2684,plain, % 186.94/186.98 (P3(f25(f18(x26841,a15),f18(x26841,a15)),f25(f18(x26841,a11),f18(x26841,a11)))), % 186.94/186.98 inference(scs_inference,[],[2641,2655,2651,336,39,37,40,38,42,43,41,61])). % 186.94/186.98 cnf(2690,plain, % 186.94/186.98 (P3(f26(f18(x26901,a15),f18(x26901,a15)),f26(f18(x26901,a11),f18(x26901,a11)))), % 186.94/186.98 inference(scs_inference,[],[2641,2655,2651,11,336,348,7,39,37,40,38,42,43,41,61,64,63,59])). % 186.94/186.98 cnf(2708,plain, % 186.94/186.98 (P3(f25(f25(f18(x27081,a15),f18(x27081,a15)),f25(f18(x27081,a15),f18(x27081,a15))),f25(f25(f18(x27081,a11),f18(x27081,a11)),f25(f18(x27081,a11),f18(x27081,a11))))), % 186.94/186.98 inference(scs_inference,[],[2684,7,40,39,38,41,37,64,61])). % 186.94/186.98 cnf(2840,plain, % 186.94/186.98 (P3(f25(f26(f18(x28401,a15),f18(x28401,a15)),f26(f18(x28401,a15),f18(x28401,a15))),f25(f26(f18(x28401,a11),f18(x28401,a11)),f26(f18(x28401,a11),f18(x28401,a11))))), % 186.94/186.98 inference(scs_inference,[],[2708,2690,7,41,40,37,38,39,64,61])). % 186.94/186.98 cnf(2842,plain, % 186.94/186.98 (P3(f26(f26(f18(x28421,a15),f18(x28421,a15)),f26(f18(x28421,a15),f18(x28421,a15))),f26(f26(f18(x28421,a11),f18(x28421,a11)),f26(f18(x28421,a11),f18(x28421,a11))))), % 186.94/186.98 inference(scs_inference,[],[2708,2690,7,41,40,37,38,39,64,61,59])). % 186.94/186.98 cnf(2861,plain, % 186.94/186.98 (P3(f25(a17,a17),f25(f21(a7),f21(a7)))), % 186.94/186.98 inference(scs_inference,[],[2840,19,37,41,38,39,40,61])). % 186.94/186.98 cnf(2865,plain, % 186.94/186.98 (P3(f26(a17,a17),f26(f21(a7),f21(a7)))), % 186.94/186.98 inference(scs_inference,[],[2840,19,7,37,41,38,39,40,61,64,59])). % 186.94/186.98 cnf(2871,plain, % 186.94/186.98 (P3(f22(f25(a17,a17)),f22(f25(f21(a7),f21(a7))))), % 186.94/186.98 inference(scs_inference,[],[2861,38])). % 186.94/186.98 cnf(2873,plain, % 186.94/186.98 (P13(f27(f25(a17,a17)),f27(f25(f21(a7),f21(a7))))), % 186.94/186.98 inference(scs_inference,[],[2861,38,37])). % 186.94/186.98 cnf(2875,plain, % 186.94/186.98 (P3(f21(f25(a17,a17)),f21(f25(f21(a7),f21(a7))))), % 186.94/186.98 inference(scs_inference,[],[2861,38,37,39])). % 186.94/186.98 cnf(2877,plain, % 186.94/186.98 (P3(f24(f25(a17,a17)),f24(f25(f21(a7),f21(a7))))), % 186.94/186.98 inference(scs_inference,[],[2861,38,37,39,40])). % 186.94/186.98 cnf(2881,plain, % 186.94/186.98 (P6(f20(a11,f25(a17,a17)),f20(a15,f25(f21(a7),f21(a7))))), % 186.94/186.98 inference(scs_inference,[],[2861,7,38,37,39,40,41,64])). % 186.94/186.98 cnf(2902,plain, % 186.94/186.98 (P13(f27(f22(f25(a17,a17))),f27(f22(f25(f21(a7),f21(a7)))))), % 186.94/186.98 inference(scs_inference,[],[2871,39,38,40,41,37])). % 186.94/186.98 cnf(2910,plain, % 186.94/186.98 (P6(f20(x29101,f22(f25(a17,a17))),f20(x29101,f22(f25(f21(a7),f21(a7)))))), % 186.94/186.98 inference(scs_inference,[],[2871,2873,2881,11,10,39,38,40,41,37,60,63,61,64])). % 186.94/186.98 cnf(2927,plain, % 186.94/186.98 (P3(f21(f21(f25(a17,a17))),f21(f21(f25(f21(a7),f21(a7)))))), % 186.94/186.98 inference(scs_inference,[],[2875,40,39])). % 186.94/186.98 cnf(2931,plain, % 186.94/186.98 (P13(f27(f21(f25(a17,a17))),f27(f21(f25(f21(a7),f21(a7)))))), % 186.94/186.98 inference(scs_inference,[],[2875,40,39,41,37])). % 186.94/186.98 cnf(2933,plain, % 186.94/186.98 (P3(f22(f21(f25(a17,a17))),f22(f21(f25(f21(a7),f21(a7)))))), % 186.94/186.98 inference(scs_inference,[],[2875,40,39,41,37,38])). % 186.94/186.98 cnf(2941,plain, % 186.94/186.98 (P6(f20(a11,f21(f25(a17,a17))),f20(a15,f21(f25(f21(a7),f21(a7)))))), % 186.94/186.98 inference(scs_inference,[],[2875,2910,2902,22,7,40,39,41,37,38,63,60,61,64])). % 186.94/186.98 cnf(2956,plain, % 186.94/186.98 (P13(f27(f24(f25(a17,a17))),f27(f24(f25(f21(a7),f21(a7)))))), % 186.94/186.98 inference(scs_inference,[],[2877,41,40,37])). % 186.94/186.98 cnf(2960,plain, % 186.94/186.98 (P3(f21(f24(f25(a17,a17))),f21(f24(f25(f21(a7),f21(a7)))))), % 186.94/186.98 inference(scs_inference,[],[2877,41,40,37,38,39])). % 186.94/186.98 cnf(2966,plain, % 186.94/186.98 (P6(f20(x29661,f24(f25(a17,a17))),f20(x29661,f24(f25(f21(a7),f21(a7)))))), % 186.94/186.98 inference(scs_inference,[],[2877,2931,2941,193,10,41,40,37,38,39,60,63,64])). % 186.94/186.98 cnf(3056,plain, % 186.94/186.98 (P3(f26(f26(a17,a17),f26(a17,a17)),f26(f26(f21(a7),f21(a7)),f26(f21(a7),f21(a7))))), % 186.94/186.98 inference(scs_inference,[],[2960,2865,37,41,38,39,40,59])). % 186.94/186.98 cnf(3068,plain, % 186.94/186.98 (P3(f21(f26(f26(a17,a17),f26(a17,a17))),f21(f26(f26(f21(a7),f21(a7)),f26(f21(a7),f21(a7)))))), % 186.94/186.98 inference(scs_inference,[],[3056,37,38,39])). % 186.94/186.98 cnf(3074,plain, % 186.94/186.98 (P6(f20(a11,f26(f26(a17,a17),f26(a17,a17))),f20(a15,f26(f26(f21(a7),f21(a7)),f26(f21(a7),f21(a7)))))), % 186.94/186.98 inference(scs_inference,[],[3056,7,37,38,39,41,40,64])). % 186.94/186.98 cnf(3137,plain, % 186.94/186.98 (P3(f25(a12,a12),f25(a16,a16))), % 186.94/186.98 inference(scs_inference,[],[3068,3074,2956,11,10,8,37,41,38,39,40,60,64,63,61])). % 186.94/186.98 cnf(3139,plain, % 186.94/186.98 (P3(f26(a12,a12),f26(a16,a16))), % 186.94/186.98 inference(scs_inference,[],[3068,3074,2956,11,10,8,37,41,38,39,40,60,64,63,61,59])). % 186.94/186.98 cnf(3143,plain, % 186.94/186.98 (P3(f22(f25(a12,a12)),f22(f25(a16,a16)))), % 186.94/186.98 inference(scs_inference,[],[3137,38])). % 186.94/186.98 cnf(3145,plain, % 186.94/186.98 (P13(f27(f25(a12,a12)),f27(f25(a16,a16)))), % 186.94/186.98 inference(scs_inference,[],[3137,38,37])). % 186.94/186.98 cnf(3147,plain, % 186.94/186.98 (P3(f21(f25(a12,a12)),f21(f25(a16,a16)))), % 186.94/186.98 inference(scs_inference,[],[3137,38,37,39])). % 186.94/186.98 cnf(3149,plain, % 186.94/186.98 (P3(f28(f25(a12,a12)),f28(f25(a16,a16)))), % 186.94/186.98 inference(scs_inference,[],[3137,38,37,39,41])). % 186.94/186.98 cnf(3151,plain, % 186.94/186.98 (P3(f24(f25(a12,a12)),f24(f25(a16,a16)))), % 186.94/186.98 inference(scs_inference,[],[3137,38,37,39,41,40])). % 186.94/186.98 cnf(3153,plain, % 186.94/186.98 (P6(f20(a11,f25(a12,a12)),f20(a15,f25(a16,a16)))), % 186.94/186.98 inference(scs_inference,[],[3137,7,38,37,39,41,40,64])). % 186.94/186.98 cnf(3155,plain, % 186.94/186.98 (P3(f26(f25(a12,a12),f25(a12,a12)),f26(f25(a16,a16),f25(a16,a16)))), % 186.94/186.98 inference(scs_inference,[],[3137,7,38,37,39,41,40,64,59])). % 186.94/186.98 cnf(3157,plain, % 186.94/186.98 (P3(f25(f25(a12,a12),f25(a12,a12)),f25(f25(a16,a16),f25(a16,a16)))), % 186.94/186.98 inference(scs_inference,[],[3137,7,38,37,39,41,40,64,59,61])). % 186.94/186.98 cnf(3169,plain, % 186.94/186.98 (P13(f27(f22(f25(a12,a12))),f27(f22(f25(a16,a16))))), % 186.94/186.98 inference(scs_inference,[],[3143,38,39,41,37])). % 186.94/186.98 cnf(3173,plain, % 186.94/186.98 (P3(f18(f27(f25(a12,a12)),x31731),f18(f27(f25(a16,a16)),x31731))), % 186.94/186.98 inference(scs_inference,[],[3143,3145,10,38,39,41,37,40,60])). % 186.94/186.98 cnf(3177,plain, % 186.94/186.98 (P6(f20(x31771,f22(f25(a12,a12))),f20(x31771,f22(f25(a16,a16))))), % 186.94/186.98 inference(scs_inference,[],[3143,3145,3153,193,10,38,39,41,37,40,60,63,64])). % 186.94/186.98 cnf(3179,plain, % 186.94/186.98 (P3(f25(f22(f25(a12,a12)),f22(f25(a12,a12))),f25(f22(f25(a16,a16)),f22(f25(a16,a16))))), % 186.94/186.98 inference(scs_inference,[],[3143,3145,3153,193,10,38,39,41,37,40,60,63,64,61])). % 186.94/186.98 cnf(3220,plain, % 186.94/186.98 (~P3(f18(f27(a13),a11),x32201)+P14(x32201,f18(f27(f26(a13,f21(f24(a7)))),a11))), % 186.94/186.98 inference(scs_inference,[],[3173,3177,3169,29,11,208,7,15,38,41,37,39,40,60,64,63,59,61,34,55])). % 186.94/186.98 cnf(3320,plain, % 186.94/186.98 (P3(f25(f21(f25(a12,a12)),f21(f25(a12,a12))),f25(f21(f25(a16,a16)),f21(f25(a16,a16))))), % 186.94/186.98 inference(scs_inference,[],[3179,3147,38,39,41,37,40,61])). % 186.94/186.98 cnf(3366,plain, % 186.94/186.98 (P3(f25(f28(f25(a12,a12)),f28(f25(a12,a12))),f25(f28(f25(a16,a16)),f28(f25(a16,a16))))), % 186.94/186.98 inference(scs_inference,[],[3320,3149,10,38,37,41,39,40,64,61])). % 186.94/186.98 cnf(3388,plain, % 186.94/186.98 (P3(f25(f24(f25(a12,a12)),f24(f25(a12,a12))),f25(f24(f25(a16,a16)),f24(f25(a16,a16))))), % 186.94/186.98 inference(scs_inference,[],[3366,3151,7,38,41,37,39,40,64,61])). % 186.94/186.98 cnf(3408,plain, % 186.94/186.98 (P3(f25(f26(f25(a12,a12),f25(a12,a12)),f26(f25(a12,a12),f25(a12,a12))),f25(f26(f25(a16,a16),f25(a16,a16)),f26(f25(a16,a16),f25(a16,a16))))), % 186.94/186.98 inference(scs_inference,[],[3388,3155,10,38,37,41,39,40,64,61])). % 186.94/186.98 cnf(3433,plain, % 186.94/186.98 (P3(f25(f25(f25(a12,a12),f25(a12,a12)),f25(f25(a12,a12),f25(a12,a12))),f25(f25(f25(a16,a16),f25(a16,a16)),f25(f25(a16,a16),f25(a16,a16))))), % 186.94/186.98 inference(scs_inference,[],[3408,3157,7,38,41,39,37,40,64,61])). % 186.94/186.98 cnf(3459,plain, % 186.94/186.98 (P3(f26(f26(a12,a12),f26(a12,a12)),f26(f26(a16,a16),f26(a16,a16)))), % 186.94/186.98 inference(scs_inference,[],[3433,3139,7,38,39,37,41,40,64,61,59])). % 186.94/186.98 cnf(3473,plain, % 186.94/186.98 (P3(f25(f26(f26(a12,a12),f26(a12,a12)),f26(f26(a12,a12),f26(a12,a12))),f25(f26(f26(a16,a16),f26(a16,a16)),f26(f26(a16,a16),f26(a16,a16))))), % 186.94/186.98 inference(scs_inference,[],[3459,7,38,37,41,39,40,64,61])). % 186.94/186.98 cnf(3684,plain, % 186.94/186.98 (P3(f26(a16,a16),f26(a12,a12))), % 186.94/186.98 inference(scs_inference,[],[3473,87,38,41,39,37,40,59])). % 186.94/186.98 cnf(3686,plain, % 186.94/186.98 (P3(f25(a16,a16),f25(a12,a12))), % 186.94/186.98 inference(scs_inference,[],[3473,87,38,41,39,37,40,59,61])). % 186.94/186.98 cnf(3697,plain, % 186.94/186.98 (P3(f22(f26(a16,a16)),f22(f26(a12,a12)))), % 186.94/186.98 inference(scs_inference,[],[3684,38])). % 186.94/186.98 cnf(3699,plain, % 186.94/186.98 (P3(f24(f26(a16,a16)),f24(f26(a12,a12)))), % 186.94/186.98 inference(scs_inference,[],[3684,38,40])). % 186.94/186.98 cnf(3701,plain, % 186.94/186.98 (P3(f21(f26(a16,a16)),f21(f26(a12,a12)))), % 186.94/186.98 inference(scs_inference,[],[3684,38,40,39])). % 186.94/186.98 cnf(3703,plain, % 186.94/186.98 (P13(f27(f26(a16,a16)),f27(f26(a12,a12)))), % 186.94/186.98 inference(scs_inference,[],[3684,38,40,39,37])). % 186.94/186.98 cnf(3707,plain, % 186.94/186.98 (P6(f20(x37071,f26(a16,a16)),f20(x37071,f26(a12,a12)))), % 186.94/186.98 inference(scs_inference,[],[3684,10,38,40,39,37,41,64])). % 186.94/186.98 cnf(3709,plain, % 186.94/186.98 (P3(f25(f26(a16,a16),f26(a16,a16)),f25(f26(a12,a12),f26(a12,a12)))), % 186.94/186.98 inference(scs_inference,[],[3684,10,38,40,39,37,41,64,61])). % 186.94/186.98 cnf(3711,plain, % 186.94/186.98 (P3(f26(f26(a16,a16),f26(a16,a16)),f26(f26(a12,a12),f26(a12,a12)))), % 186.94/186.98 inference(scs_inference,[],[3684,10,38,40,39,37,41,64,61,59])). % 186.94/186.98 cnf(3717,plain, % 186.94/186.98 (P3(f21(f25(a16,a16)),f21(f25(a12,a12)))), % 186.94/186.98 inference(scs_inference,[],[3686,38,39])). % 186.94/186.98 cnf(3719,plain, % 186.94/186.98 (P3(f28(f25(a16,a16)),f28(f25(a12,a12)))), % 186.94/186.98 inference(scs_inference,[],[3686,38,39,41])). % 186.94/186.98 cnf(3721,plain, % 186.94/186.98 (P13(f27(f25(a16,a16)),f27(f25(a12,a12)))), % 186.94/186.98 inference(scs_inference,[],[3686,38,39,41,37])). % 186.94/186.98 cnf(3729,plain, % 186.94/186.98 (P6(f20(a11,f25(a16,a16)),f20(a15,f25(a12,a12)))), % 186.94/186.98 inference(scs_inference,[],[3686,3707,3703,193,7,38,39,41,37,40,63,60,64])). % 186.94/186.98 cnf(3731,plain, % 186.94/186.98 (P3(f26(f25(a16,a16),f25(a16,a16)),f26(f25(a12,a12),f25(a12,a12)))), % 186.94/186.98 inference(scs_inference,[],[3686,3707,3703,193,7,38,39,41,37,40,63,60,64,59])). % 186.94/186.98 cnf(3746,plain, % 186.94/186.98 (P13(f27(f22(f26(a16,a16))),f27(f22(f26(a12,a12))))), % 186.94/186.98 inference(scs_inference,[],[3697,38,41,37])). % 186.94/186.98 cnf(3754,plain, % 186.94/186.98 (P3(f18(f27(f25(a16,a16)),x37541),f18(f27(f25(a12,a12)),x37541))), % 186.94/186.98 inference(scs_inference,[],[3697,3721,3729,11,10,38,41,37,40,39,63,60])). % 186.94/186.98 cnf(3756,plain, % 186.94/186.98 (P6(f20(x37561,f22(f26(a16,a16))),f20(x37561,f22(f26(a12,a12))))), % 186.94/186.98 inference(scs_inference,[],[3697,3721,3729,11,10,38,41,37,40,39,63,60,64])). % 186.94/186.98 cnf(3760,plain, % 186.94/186.98 (P3(f26(f22(f26(a16,a16)),f22(f26(a16,a16))),f26(f22(f26(a12,a12)),f22(f26(a12,a12))))), % 186.94/186.98 inference(scs_inference,[],[3697,3721,3729,11,10,38,41,37,40,39,63,60,64,61,59])). % 186.94/186.98 cnf(3772,plain, % 186.94/186.98 (P3(f21(f24(f26(a16,a16))),f21(f24(f26(a12,a12))))), % 186.94/186.98 inference(scs_inference,[],[3699,38,41,37,40,39])). % 186.94/186.98 cnf(3778,plain, % 186.94/186.98 (P6(f20(a11,f24(f26(a16,a16))),f20(a15,f24(f26(a12,a12))))), % 186.94/186.98 inference(scs_inference,[],[3699,3756,3746,22,7,38,41,37,40,39,63,60,64])). % 186.94/186.98 cnf(3780,plain, % 186.94/186.98 (P3(f26(f24(f26(a16,a16)),f24(f26(a16,a16))),f26(f24(f26(a12,a12)),f24(f26(a12,a12))))), % 186.94/186.98 inference(scs_inference,[],[3699,3756,3746,22,7,38,41,37,40,39,63,60,64,59])). % 186.94/186.98 cnf(3874,plain, % 186.94/186.98 (P5(f19(x38741,f20(x38742,f26(a16,a16))),f19(x38741,f20(x38742,f26(a12,a12))))), % 186.94/186.98 inference(scs_inference,[],[3772,3707,11,10,38,41,37,39,40,64,59,61,63])). % 186.94/186.98 cnf(3902,plain, % 186.94/186.98 (P3(f26(f21(f26(a16,a16)),f21(f26(a16,a16))),f26(f21(f26(a12,a12)),f21(f26(a12,a12))))), % 186.94/186.98 inference(scs_inference,[],[3874,3780,3701,7,43,38,37,41,40,39,64,59])). % 186.94/186.98 cnf(3959,plain, % 186.94/186.98 (P3(f26(f26(f26(a16,a16),f26(a16,a16)),f26(f26(a16,a16),f26(a16,a16))),f26(f26(f26(a12,a12),f26(a12,a12)),f26(f26(a12,a12),f26(a12,a12))))), % 186.94/186.98 inference(scs_inference,[],[3902,3711,10,38,37,41,40,39,64,59])). % 186.94/186.98 cnf(3985,plain, % 186.94/186.98 (P3(f26(f25(f26(a16,a16),f26(a16,a16)),f25(f26(a16,a16),f26(a16,a16))),f26(f25(f26(a12,a12),f26(a12,a12)),f25(f26(a12,a12),f26(a12,a12))))), % 186.94/186.98 inference(scs_inference,[],[3959,3709,7,38,41,37,40,39,64,59])). % 186.94/186.98 cnf(4005,plain, % 186.94/186.98 (P3(f26(f26(f25(a16,a16),f25(a16,a16)),f26(f25(a16,a16),f25(a16,a16))),f26(f26(f25(a12,a12),f25(a12,a12)),f26(f25(a12,a12),f25(a12,a12))))), % 186.94/186.98 inference(scs_inference,[],[3985,3731,10,38,41,37,40,39,64,59])). % 186.94/186.98 cnf(4060,plain, % 186.94/186.98 (P3(f26(f21(f25(a16,a16)),f21(f25(a16,a16))),f26(f21(f25(a12,a12)),f21(f25(a12,a12))))), % 186.94/186.98 inference(scs_inference,[],[4005,3717,10,38,41,37,40,39,64,59])). % 186.94/186.98 cnf(4093,plain, % 186.94/186.98 (P3(f26(f28(f25(a16,a16)),f28(f25(a16,a16))),f26(f28(f25(a12,a12)),f28(f25(a12,a12))))), % 186.94/186.98 inference(scs_inference,[],[4060,3719,7,38,41,37,40,39,64,59])). % 186.94/186.98 cnf(4095,plain, % 186.94/186.98 (P3(f25(f28(f25(a16,a16)),f28(f25(a16,a16))),f25(f28(f25(a12,a12)),f28(f25(a12,a12))))), % 186.94/186.98 inference(scs_inference,[],[4060,3719,7,38,41,37,40,39,64,59,61])). % 186.94/186.98 cnf(4185,plain, % 186.94/186.98 (P13(f27(f26(f28(f25(a16,a16)),f28(f25(a16,a16)))),f27(f26(f28(f25(a12,a12)),f28(f25(a12,a12)))))), % 186.94/186.98 inference(scs_inference,[],[4093,38,41,37])). % 186.94/186.98 cnf(4223,plain, % 186.94/186.98 (P5(f10(f19(f29(a3),f20(x42231,f26(a16,a16)))),f10(f19(a2,f20(x42231,f26(a12,a12)))))), % 186.94/186.98 inference(scs_inference,[],[4185,4095,3754,3707,22,25,13,14,38,41,37,39,40,59,61,69,63,43])). % 186.94/186.98 cnf(4772,plain, % 186.94/186.98 (P5(f10(f19(a2,f20(a11,f25(a16,a16)))),f10(f19(f29(a3),f20(a15,f25(a12,a12)))))), % 186.94/186.98 inference(scs_inference,[],[3760,3729,193,38,41,40,37,39,63,43])). % 186.94/186.98 cnf(5114,plain, % 186.94/186.98 (P5(f19(f29(a3),f20(x51141,f24(f25(a17,a17)))),f19(a2,f20(x51141,f24(f25(f21(a7),f21(a7))))))), % 186.94/186.98 inference(scs_inference,[],[2927,2966,22,40,38,41,37,39,63])). % 186.94/186.98 cnf(5139,plain, % 186.94/186.98 (P13(f27(f22(f21(f25(a17,a17)))),f27(f22(f21(f25(f21(a7),f21(a7))))))), % 186.94/186.98 inference(scs_inference,[],[2933,39,40,38,41,37])). % 186.94/186.98 cnf(5149,plain, % 186.94/186.98 (P13(f27(f26(f26(f18(x51491,a15),f18(x51491,a15)),f26(f18(x51491,a15),f18(x51491,a15)))),f27(f26(f26(f18(x51491,a11),f18(x51491,a11)),f26(f18(x51491,a11),f18(x51491,a11)))))), % 186.94/186.98 inference(scs_inference,[],[2842,39,40,38,41,37])). % 186.94/186.98 cnf(5151,plain, % 186.94/186.98 (P3(f18(x51511,a11),f18(x51511,a15))), % 186.94/186.98 inference(scs_inference,[],[2842,7,13,39,40,38,41,37,60])). % 186.94/186.98 cnf(5156,plain, % 186.94/186.98 (~P13(f27(f22(f22(f21(f25(a17,a17))))),x51561)+P10(a1,x51561,f27(f22(f21(f25(f21(a7),f21(a7))))))), % 186.94/186.98 inference(scs_inference,[],[5139,2842,26,25,7,13,14,15,39,40,38,41,37,60,57,69])). % 186.94/186.98 cnf(5164,plain, % 186.94/186.98 (P3(f21(f18(x51641,a11)),f21(f18(x51641,a15)))), % 186.94/186.98 inference(scs_inference,[],[5151,39])). % 186.94/186.98 cnf(5168,plain, % 186.94/186.98 (P3(f22(f18(x51681,a11)),f22(f18(x51681,a15)))), % 186.94/186.98 inference(scs_inference,[],[5151,39,40,38])). % 186.94/186.98 cnf(5172,plain, % 186.94/186.98 (P13(f27(f18(x51721,a11)),f27(f18(x51721,a15)))), % 186.94/186.98 inference(scs_inference,[],[5151,39,40,38,41,37])). % 186.94/186.98 cnf(5174,plain, % 186.94/186.98 (P3(f25(f18(x51741,a11),f18(x51741,a11)),f25(f18(x51741,a15),f18(x51741,a15)))), % 186.94/186.98 inference(scs_inference,[],[5151,39,40,38,41,37,61])). % 186.94/186.98 cnf(5176,plain, % 186.94/186.98 (P6(f20(x51761,f18(x51762,a11)),f20(x51761,f18(x51762,a15)))), % 186.94/186.98 inference(scs_inference,[],[5151,10,39,40,38,41,37,61,64])). % 186.94/186.98 cnf(5178,plain, % 186.94/186.98 (P3(f26(f18(x51781,a11),f18(x51781,a11)),f26(f18(x51781,a15),f18(x51781,a15)))), % 186.94/186.98 inference(scs_inference,[],[5151,10,39,40,38,41,37,61,64,59])). % 186.94/186.98 cnf(5190,plain, % 186.94/186.98 (P5(f19(a2,f20(x51901,f22(f25(a12,a12)))),f19(f29(a3),f20(x51901,f22(f25(a16,a16)))))), % 186.94/186.98 inference(scs_inference,[],[5151,5149,5114,3177,193,25,10,13,14,39,40,38,41,37,61,64,59,69,3220,35,63])). % 186.94/186.98 cnf(5198,plain, % 186.94/186.98 (P3(f21(f25(f18(x51981,a11),f18(x51981,a11))),f21(f25(f18(x51981,a15),f18(x51981,a15))))), % 186.94/186.98 inference(scs_inference,[],[5174,39])). % 186.94/186.98 cnf(5200,plain, % 186.94/186.98 (P3(f24(f25(f18(x52001,a11),f18(x52001,a11))),f24(f25(f18(x52001,a15),f18(x52001,a15))))), % 186.94/186.98 inference(scs_inference,[],[5174,39,40])). % 186.94/186.98 cnf(5206,plain, % 186.94/186.98 (P13(f27(f25(f18(x52061,a11),f18(x52061,a11))),f27(f25(f18(x52061,a15),f18(x52061,a15))))), % 186.94/186.98 inference(scs_inference,[],[5174,39,40,38,41,37])). % 186.94/186.98 cnf(5210,plain, % 186.94/186.98 (P6(f20(a11,f25(f18(x52101,a11),f18(x52101,a11))),f20(a15,f25(f18(x52101,a15),f18(x52101,a15))))), % 186.94/186.98 inference(scs_inference,[],[5174,7,39,40,38,41,37,61,64])). % 186.94/186.98 cnf(5218,plain, % 186.94/186.98 (P5(f10(f19(x52181,f20(x52182,f18(x52183,a11)))),f10(f19(x52181,f20(x52182,f18(x52183,a15)))))), % 186.94/186.98 inference(scs_inference,[],[5176,5174,5172,11,7,39,40,38,41,37,61,64,59,60,63,43])). % 186.94/186.98 cnf(5233,plain, % 186.94/186.98 (P3(f28(f26(f18(x52331,a11),f18(x52331,a11))),f28(f26(f18(x52331,a15),f18(x52331,a15))))), % 186.94/186.98 inference(scs_inference,[],[5178,39,40,38,41])). % 186.94/186.98 cnf(5235,plain, % 186.94/186.98 (P13(f27(f26(f18(x52351,a11),f18(x52351,a11))),f27(f26(f18(x52351,a15),f18(x52351,a15))))), % 186.94/186.98 inference(scs_inference,[],[5178,39,40,38,41,37])). % 186.94/186.98 cnf(5245,plain, % 186.94/186.98 (P5(f19(f29(a3),f20(a11,f25(f18(x52451,a11),f18(x52451,a11)))),f19(a2,f20(a15,f25(f18(x52451,a15),f18(x52451,a15)))))), % 186.94/186.98 inference(scs_inference,[],[5178,5206,5210,22,10,39,40,38,41,37,61,64,59,60,63])). % 186.94/186.98 cnf(5250,plain, % 186.94/186.98 (P3(f21(f21(f18(x52501,a11))),f21(f21(f18(x52501,a15))))), % 186.94/186.98 inference(scs_inference,[],[5164,39])). % 186.94/186.98 cnf(5252,plain, % 186.94/186.98 (P3(f24(f21(f18(x52521,a11))),f24(f21(f18(x52521,a15))))), % 186.94/186.98 inference(scs_inference,[],[5164,39,40])). % 186.94/186.98 cnf(5305,plain, % 186.94/186.98 (P6(f20(a11,f22(f18(x53051,a11))),f20(a15,f22(f18(x53051,a15))))), % 186.94/186.98 inference(scs_inference,[],[5168,5198,7,39,40,38,37,41,61,64])). % 186.94/186.98 cnf(5336,plain, % 186.94/186.98 (P5(f19(a2,f20(a11,f22(f18(x53361,a11)))),f19(f29(a3),f20(a15,f22(f18(x53361,a15)))))), % 186.94/186.98 inference(scs_inference,[],[5200,5305,5235,193,10,39,40,38,41,37,61,64,59,60,63])). % 186.94/186.98 cnf(5445,plain, % 186.94/186.98 (P13(f27(f28(f26(f18(x54451,a11),f18(x54451,a11)))),f27(f28(f26(f18(x54451,a15),f18(x54451,a15)))))), % 186.94/186.98 inference(scs_inference,[],[5233,39,40,38,37])). % 186.94/186.98 cnf(5479,plain, % 186.94/186.98 (P3(f18(f27(f18(x54791,a11)),x54792),f18(f27(f18(x54791,a15)),x54792))), % 186.94/186.98 inference(scs_inference,[],[5445,5250,5172,25,10,13,14,39,40,38,41,37,61,59,69,60])). % 186.94/186.98 cnf(5487,plain, % 186.94/186.98 (P13(f27(f18(f27(f18(x54871,a11)),x54872)),f27(f18(f27(f18(x54871,a15)),x54872)))), % 186.94/186.98 inference(scs_inference,[],[5479,39,40,38,37])). % 186.94/186.98 cnf(5517,plain, % 186.94/186.98 (P10(a1,f27(f22(f18(f27(f18(x55171,a11)),a15))),f27(f18(f27(f18(x55171,a15)),a11)))), % 186.94/186.98 inference(scs_inference,[],[5487,5252,1520,25,7,14,39,40,38,41,37,61,64,59,69])). % 186.94/186.98 cnf(6459,plain, % 186.94/186.98 (P5(f19(f29(a3),f20(a11,f24(f26(a16,a16)))),f19(a2,f20(a15,f24(f26(a12,a12)))))), % 186.94/186.98 inference(scs_inference,[],[22,27,3778,41,39,40,38,37,63])). % 186.94/186.98 cnf(6477,plain, % 186.94/186.98 (P4(f9(f9(f9(f9(f23(x64771,a15))))),f9(f9(f9(f9(f23(x64771,a11))))))), % 186.94/186.98 inference(scs_inference,[],[13,6459,2612,5156,43,42])). % 186.94/186.98 cnf(6521,plain, % 186.94/186.98 (P3(f24(a17),f24(f21(a7)))), % 186.94/186.98 inference(scs_inference,[],[10,30,27,19,15,5245,2678,43,42,59,61,64,39,40])). % 186.94/186.98 cnf(6523,plain, % 186.94/186.98 (P3(f28(a17),f28(f21(a7)))), % 186.94/186.98 inference(scs_inference,[],[10,30,27,19,15,5245,2678,43,42,59,61,64,39,40,41])). % 186.94/186.98 cnf(6527,plain, % 186.94/186.98 (P13(f27(a17),f27(f21(a7)))), % 186.94/186.98 inference(scs_inference,[],[10,30,27,19,15,5245,2678,43,42,59,61,64,39,40,41,38,37])). % 186.94/186.98 cnf(6555,plain, % 186.94/186.98 (P13(f27(a12),f27(a16))), % 186.94/186.98 inference(scs_inference,[],[30,7,8,15,5190,43,64,39,59,61,40,41,37])). % 186.94/186.98 cnf(6559,plain, % 186.94/186.98 (P3(f18(f27(a17),x65591),f18(f27(f21(a7)),x65591))), % 186.94/186.98 inference(scs_inference,[],[10,30,7,8,15,6527,5190,43,64,39,59,61,40,41,37,38,60])). % 186.94/186.98 cnf(6576,plain, % 186.94/186.98 (P3(f26(f18(f27(a17),x65761),f18(f27(a17),x65761)),f26(f18(f27(f21(a7)),x65761),f18(f27(f21(a7)),x65761)))), % 186.94/186.98 inference(scs_inference,[],[10,19,6559,4772,43,64,61,39,59])). % 186.94/186.98 cnf(6624,plain, % 186.94/186.98 (P6(f20(x66241,a12),f20(x66241,a16))), % 186.94/186.98 inference(scs_inference,[],[14,10,13,8,5517,5218,1491,43,69,64])). % 186.94/186.98 cnf(6626,plain, % 186.94/186.98 (P3(f26(f24(a17),f24(a17)),f26(f24(f21(a7)),f24(f21(a7))))), % 186.94/186.98 inference(scs_inference,[],[14,10,13,8,6521,5517,5218,1491,43,69,64,59])). % 186.94/186.98 cnf(6630,plain, % 186.94/186.98 (P3(f25(f24(a17),f24(a17)),f25(f24(f21(a7)),f24(f21(a7))))), % 186.94/186.98 inference(scs_inference,[],[14,10,13,8,6576,6521,5517,5218,1491,43,69,64,59,40,61])). % 186.94/186.98 cnf(6646,plain, % 186.94/186.98 (P3(f24(f26(f24(a17),f24(a17))),f24(f26(f24(f21(a7)),f24(f21(a7)))))), % 186.94/186.98 inference(scs_inference,[],[6626,5336,43,40])). % 186.94/186.98 cnf(6648,plain, % 186.94/186.98 (P3(f25(f26(f24(a17),f24(a17)),f26(f24(a17),f24(a17))),f25(f26(f24(f21(a7)),f24(f21(a7))),f26(f24(f21(a7)),f24(f21(a7)))))), % 186.94/186.98 inference(scs_inference,[],[6626,5336,43,40,61])). % 186.94/186.98 cnf(6681,plain, % 186.94/186.98 (P5(f19(f29(a3),f20(x66811,a12)),f19(a2,f20(x66811,a16)))), % 186.94/186.98 inference(scs_inference,[],[22,6646,6630,6624,4223,43,59,61,40,39,41,37,38,63])). % 186.94/186.98 cnf(6687,plain, % 186.94/186.98 (P5(f10(f19(f29(a3),f20(x66871,a12))),f10(f19(a2,f20(x66871,a16))))), % 186.94/186.98 inference(scs_inference,[],[6681,43])). % 186.94/186.98 cnf(6689,plain, % 186.94/186.98 (P3(f25(f28(a17),f28(a17)),f25(f28(f21(a7)),f28(f21(a7))))), % 186.94/186.98 inference(scs_inference,[],[6681,6523,43,61])). % 186.94/186.98 cnf(6693,plain, % 186.94/186.98 (P3(f26(f28(a17),f28(a17)),f26(f28(f21(a7)),f28(f21(a7))))), % 186.94/186.98 inference(scs_inference,[],[6648,6681,6523,43,61,40,59])). % 186.94/186.98 cnf(6704,plain, % 186.94/186.98 (P5(f10(f10(f19(f29(a3),f20(x67041,a12)))),f10(f10(f19(a2,f20(x67041,a16)))))), % 186.94/186.98 inference(scs_inference,[],[6687,43])). % 186.94/186.98 cnf(6706,plain, % 186.94/186.98 (P3(f25(f25(f28(a17),f28(a17)),f25(f28(a17),f28(a17))),f25(f25(f28(f21(a7)),f28(f21(a7))),f25(f28(f21(a7)),f28(f21(a7)))))), % 186.94/186.98 inference(scs_inference,[],[6687,6689,43,61])). % 186.94/186.98 cnf(6744,plain, % 186.94/186.98 (~P3(f18(f27(a12),a14),f18(f27(f26(a12,f21(f24(a7)))),a14))), % 186.94/186.98 inference(scs_inference,[],[10,31,6704,6706,6555,6693,6477,43,40,61,59,39,41,37,38,34,60,49])). % 186.94/186.98 cnf(6752,plain, % 186.94/186.98 ($false), % 186.94/186.98 inference(scs_inference,[],[30,15,6744,49]), % 186.94/186.98 ['proof']). % 186.94/186.99 % SZS output end Proof % 186.94/186.99 % Total time :186.340000s %------------------------------------------------------------------------------