%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN617-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 : n017.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:07 EDT 2024 % Result : Unsatisfiable 184.90s 184.91s % Output : CNFRefutation 184.98s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : SYN617-1 : TPTP v8.2.0. Released v2.5.0. % 0.04/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.13/0.34 % Computer : n017.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Sun Jun 23 22:17:39 EDT 2024 % 0.13/0.34 % CPUTime : % 0.53/0.57 start to proof:theBenchmark % 184.86/184.87 %------------------------------------------- % 184.86/184.87 % File :CSE---1.7 % 184.86/184.87 % Problem :theBenchmark % 184.86/184.87 % Transform :cnf % 184.86/184.87 % Format :tptp:raw % 184.86/184.87 % Command :java -jar mcs_scs.jar %d %s % 184.86/184.87 % 184.86/184.87 % Result :Theorem 184.230000s % 184.86/184.87 % Output :CNFRefutation 184.230000s % 184.86/184.87 %------------------------------------------- % 184.90/184.90 %-------------------------------------------------------------------------- % 184.90/184.90 % File : SYN617-1 : TPTP v8.2.0. Released v2.5.0. % 184.90/184.90 % Domain : Syntactic % 184.90/184.90 % Problem : Harrison problem 3908 % 184.90/184.90 % Version : Especial. % 184.90/184.90 % English : % 184.90/184.90 % 184.90/184.90 % Refs : [Har01] Email to G. Sutcliffe % 184.90/184.90 % Source : [Har01] % 184.90/184.90 % Names : % 184.90/184.90 % 184.90/184.90 % Status : Unsatisfiable % 184.90/184.90 % Rating : 0.45 v8.2.0, 0.29 v8.1.0, 0.25 v7.4.0, 0.33 v7.3.0, 0.25 v6.2.0, 0.33 v6.1.0, 0.50 v6.0.0, 0.44 v5.5.0, 0.50 v5.4.0, 0.56 v5.3.0, 0.65 v5.2.0, 0.69 v5.1.0, 0.62 v5.0.0, 0.53 v4.0.1, 0.71 v3.7.0, 0.57 v3.4.0, 0.40 v3.3.0, 0.33 v3.2.0, 0.67 v3.1.0, 0.50 v2.7.0, 0.38 v2.6.0, 0.33 v2.5.0 % 184.90/184.90 % Syntax : Number of clauses : 32 ( 13 unt; 0 nHn; 21 RR) % 184.90/184.90 % Number of literals : 63 ( 0 equ; 32 neg) % 184.90/184.90 % Maximal clause size : 4 ( 1 avg) % 184.90/184.90 % Maximal term depth : 6 ( 1 avg) % 184.90/184.90 % Number of predicates : 6 ( 6 usr; 0 prp; 2-2 aty) % 184.90/184.90 % Number of functors : 17 ( 17 usr; 5 con; 0-2 aty) % 184.90/184.90 % Number of variables : 70 ( 2 sgn) % 184.90/184.90 % SPC : CNF_UNS_RFO_NEQ_HRN % 184.90/184.90 % 184.90/184.90 % Comments : % 184.90/184.90 %-------------------------------------------------------------------------- % 184.90/184.90 cnf(p11_1,negated_conjecture, % 184.90/184.90 p11(X0,X0) ). % 184.90/184.90 % 184.90/184.90 cnf(p9_2,negated_conjecture, % 184.90/184.90 p9(X53,X53) ). % 184.90/184.90 % 184.90/184.90 cnf(p7_3,negated_conjecture, % 184.90/184.90 p7(X42,X42) ). % 184.90/184.90 % 184.90/184.90 cnf(p2_4,negated_conjecture, % 184.90/184.90 p2(X27,X27) ). % 184.90/184.90 % 184.90/184.90 cnf(p13_5,negated_conjecture, % 184.90/184.90 p13(X11,X11) ). % 184.90/184.90 % 184.90/184.90 cnf(p19_6,negated_conjecture, % 184.90/184.90 p19(c21,c22) ). % 184.90/184.90 % 184.90/184.90 cnf(p11_7,negated_conjecture, % 184.90/184.90 p11(f12(f14(X5,X6)),X6) ). % 184.90/184.90 % 184.90/184.90 cnf(p7_8,negated_conjecture, % 184.90/184.90 p7(f8(f10(X51,X52)),X52) ). % 184.90/184.90 % 184.90/184.90 cnf(p9_9,negated_conjecture, % 184.90/184.90 p9(f18(f5(c20),X64),f17(X64)) ). % 184.90/184.90 % 184.90/184.90 cnf(p13_10,negated_conjecture, % 184.90/184.90 p13(f15(f5(c20),X20),f16(X20)) ). % 184.90/184.90 % 184.90/184.90 cnf(p11_11,negated_conjecture, % 184.90/184.90 ( p11(f12(X3),f12(X4)) % 184.90/184.90 | ~ p11(X3,X4) ) ). % 184.90/184.90 % 184.90/184.90 cnf(p9_12,negated_conjecture, % 184.90/184.90 ( p9(f17(X56),f17(X57)) % 184.90/184.90 | ~ p7(X56,X57) ) ). % 184.90/184.90 % 184.90/184.90 cnf(p7_13,negated_conjecture, % 184.90/184.90 ( p7(f8(X49),f8(X50)) % 184.90/184.90 | ~ p7(X49,X50) ) ). % 184.90/184.90 % 184.90/184.90 cnf(p2_14,negated_conjecture, % 184.90/184.90 ( p2(f6(X40),f6(X41)) % 184.90/184.90 | ~ p2(X40,X41) ) ). % 184.90/184.90 % 184.90/184.90 cnf(p2_15,negated_conjecture, % 184.90/184.90 ( p2(f5(X38),f5(X39)) % 184.90/184.90 | ~ p2(X38,X39) ) ). % 184.90/184.90 % 184.90/184.90 cnf(p2_16,negated_conjecture, % 184.90/184.90 ( p2(f3(X30),f3(X31)) % 184.90/184.90 | ~ p2(X30,X31) ) ). % 184.90/184.90 % 184.90/184.90 cnf(p13_17,negated_conjecture, % 184.90/184.90 ( p13(f16(X21),f16(X22)) % 184.90/184.90 | ~ p11(X21,X22) ) ). % 184.90/184.90 % 184.90/184.90 cnf(p9_18,negated_conjecture, % 184.90/184.90 p9(f18(f3(X62),X63),f18(X62,f8(X63))) ). % 184.90/184.90 % 184.90/184.90 cnf(p13_19,negated_conjecture, % 184.90/184.90 p13(f15(f3(X18),X19),f15(X18,f12(X19))) ). % 184.90/184.90 % 184.90/184.90 cnf(p11_20,negated_conjecture, % 184.90/184.90 ( p11(X1,X2) % 184.90/184.90 | ~ p11(X0,X1) % 184.90/184.90 | ~ p11(X0,X2) ) ). % 184.90/184.90 % 184.90/184.90 cnf(p9_21,negated_conjecture, % 184.90/184.90 ( p9(X54,X55) % 184.90/184.90 | ~ p9(X53,X54) % 184.90/184.90 | ~ p9(X53,X55) ) ). % 184.90/184.90 % 184.90/184.90 cnf(p7_22,negated_conjecture, % 184.90/184.90 ( p7(X43,X44) % 184.90/184.90 | ~ p7(X42,X43) % 184.90/184.90 | ~ p7(X42,X44) ) ). % 184.90/184.90 % 184.90/184.90 cnf(p2_23,negated_conjecture, % 184.90/184.90 ( p2(X28,X29) % 184.90/184.90 | ~ p2(X27,X28) % 184.90/184.90 | ~ p2(X27,X29) ) ). % 184.90/184.90 % 184.90/184.90 cnf(p13_24,negated_conjecture, % 184.90/184.90 ( p13(X12,X13) % 184.90/184.90 | ~ p13(X11,X12) % 184.90/184.90 | ~ p13(X11,X13) ) ). % 184.90/184.90 % 184.90/184.90 cnf(p19_25,negated_conjecture, % 184.90/184.90 ( p19(X23,X24) % 184.90/184.90 | ~ p2(X25,X23) % 184.90/184.90 | ~ p2(X26,X24) % 184.90/184.90 | ~ p19(X25,X26) ) ). % 184.90/184.90 % 184.90/184.90 cnf(p9_26,negated_conjecture, % 184.90/184.90 ( p9(f18(X58,X59),f18(X60,X61)) % 184.90/184.90 | ~ p2(X58,X60) % 184.90/184.90 | ~ p7(X59,X61) ) ). % 184.90/184.90 % 184.90/184.90 cnf(p11_27,negated_conjecture, % 184.90/184.90 ( p11(f14(X7,X8),f14(X9,X10)) % 184.90/184.90 | ~ p11(X8,X10) % 184.90/184.90 | ~ p13(X7,X9) ) ). % 184.90/184.90 % 184.90/184.90 cnf(p13_28,negated_conjecture, % 184.90/184.90 ( p13(f15(X14,X15),f15(X16,X17)) % 184.90/184.90 | ~ p11(X15,X17) % 184.90/184.90 | ~ p2(X14,X16) ) ). % 184.90/184.90 % 184.90/184.90 cnf(p2_29,negated_conjecture, % 184.90/184.90 ( p2(f4(X32,X33),f4(X34,X35)) % 184.90/184.90 | ~ p2(X32,X34) % 184.90/184.90 | ~ p2(X33,X35) ) ). % 184.90/184.90 % 184.90/184.90 cnf(p7_30,negated_conjecture, % 184.90/184.90 ( p7(f10(X45,X46),f10(X47,X48)) % 184.90/184.90 | ~ p7(X46,X48) % 184.90/184.90 | ~ p9(X45,X47) ) ). % 184.90/184.91 % 184.90/184.91 cnf(p2_31,negated_conjecture, % 184.90/184.91 ( p2(f4(f4(f3(X36),f5(f6(c20))),X37),f3(f4(f4(X36,f5(f6(c20))),X37))) % 184.90/184.91 | ~ p19(X37,X36) ) ). % 184.90/184.91 % 184.90/184.91 cnf(not_p13_32,negated_conjecture, % 184.90/184.91 ~ p13(f15(f4(f4(f3(c22),f5(f6(c20))),c21),f14(c23,c24)),f15(f4(f4(c22,f5(f6(c20))),c21),c24)) ). % 184.90/184.91 % 184.90/184.91 %-------------------------------------------------------------------------- % 184.90/184.91 %------------------------------------------- % 184.90/184.91 % Proof found % 184.90/184.91 % SZS status Theorem for theBenchmark % 184.90/184.91 % SZS output start Proof % 184.90/184.93 %ClaNum:32(EqnAxiom:0) % 184.90/184.93 %VarNum:140(SingletonVarNum:70) % 184.90/184.93 %MaxLitNum:4 % 184.90/184.93 %MaxfuncDepth:5 % 184.90/184.93 %SharedTerms:18 % 184.90/184.93 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 % 184.90/184.93 %singleGoalClaCount:13 % 184.90/184.93 [1]P1(a1,a3) % 184.90/184.93 [13]~P3(f7(f15(f15(f14(a3),f4(f17(a2))),a1),f8(a11,a12)),f7(f15(f15(a3,f4(f17(a2))),a1),a12)) % 184.90/184.93 [2]P2(x21,x21) % 184.90/184.93 [3]P4(x31,x31) % 184.90/184.93 [4]P5(x41,x41) % 184.90/184.93 [5]P6(x51,x51) % 184.90/184.93 [6]P3(x61,x61) % 184.90/184.93 [7]P4(f5(f4(a2),x71),f6(x71)) % 184.90/184.93 [8]P3(f7(f4(a2),x81),f13(x81)) % 184.90/184.93 [9]P2(f9(f8(x91,x92)),x92) % 184.90/184.93 [10]P5(f16(f10(x101,x102)),x102) % 184.90/184.93 [11]P4(f5(f14(x111),x112),f5(x111,f16(x112))) % 184.90/184.93 [12]P3(f7(f14(x121),x122),f7(x121,f9(x122))) % 184.90/184.93 [14]~P2(x141,x142)+P2(f9(x141),f9(x142)) % 184.90/184.93 [15]~P5(x151,x152)+P4(f6(x151),f6(x152)) % 184.90/184.93 [16]~P5(x161,x162)+P5(f16(x161),f16(x162)) % 184.90/184.93 [17]~P6(x171,x172)+P6(f4(x171),f4(x172)) % 184.90/184.93 [18]~P6(x181,x182)+P6(f17(x181),f17(x182)) % 184.90/184.93 [19]~P6(x191,x192)+P6(f14(x191),f14(x192)) % 184.90/184.93 [20]~P2(x201,x202)+P3(f13(x201),f13(x202)) % 184.90/184.93 [32]~P1(x322,x321)+P6(f15(f15(f14(x321),f4(f17(a2))),x322),f14(f15(f15(x321,f4(f17(a2))),x322))) % 184.90/184.93 [21]~P2(x213,x211)+P2(x211,x212)+~P2(x213,x212) % 184.90/184.93 [22]~P4(x223,x221)+P4(x221,x222)+~P4(x223,x222) % 184.90/184.93 [23]~P5(x233,x231)+P5(x231,x232)+~P5(x233,x232) % 184.90/184.93 [24]~P6(x243,x241)+P6(x241,x242)+~P6(x243,x242) % 184.90/184.93 [25]~P3(x253,x251)+P3(x251,x252)+~P3(x253,x252) % 184.90/184.93 [27]~P2(x272,x274)+~P3(x271,x273)+P2(f8(x271,x272),f8(x273,x274)) % 184.90/184.93 [28]~P5(x282,x284)+~P6(x281,x283)+P4(f5(x281,x282),f5(x283,x284)) % 184.90/184.93 [29]~P4(x291,x293)+~P5(x292,x294)+P5(f10(x291,x292),f10(x293,x294)) % 184.90/184.93 [30]~P6(x302,x304)+~P6(x301,x303)+P6(f15(x301,x302),f15(x303,x304)) % 184.90/184.93 [31]~P2(x312,x314)+~P6(x311,x313)+P3(f7(x311,x312),f7(x313,x314)) % 184.90/184.93 [26]~P1(x264,x263)+P1(x261,x262)+~P6(x263,x262)+~P6(x264,x261) % 184.90/184.93 %EqnAxiom % 184.90/184.93 % 184.90/184.93 %------------------------------------------- % 184.98/184.96 cnf(37,plain, % 184.98/184.96 (P4(f5(x371,f16(x372)),f5(f14(x371),x372))), % 184.98/184.96 inference(scs_inference,[],[11,3,22])). % 184.98/184.96 cnf(40,plain, % 184.98/184.96 (P3(f7(x401,f9(x402)),f7(f14(x401),x402))), % 184.98/184.96 inference(scs_inference,[],[11,12,3,6,22,25])). % 184.98/184.96 cnf(48,plain, % 184.98/184.96 (P6(f4(f15(f15(f14(a3),f4(f17(a2))),a1)),f4(f14(f15(f15(a3,f4(f17(a2))),a1))))), % 184.98/184.96 inference(scs_inference,[],[1,17,32])). % 184.98/184.96 cnf(53,plain, % 184.98/184.96 (P6(f14(f15(f15(f14(a3),f4(f17(a2))),a1)),f14(f14(f15(f15(a3,f4(f17(a2))),a1))))), % 184.98/184.96 inference(scs_inference,[],[1,19,32])). % 184.98/184.96 cnf(65,plain, % 184.98/184.96 (P2(x651,f9(f8(x652,x651)))), % 184.98/184.96 inference(scs_inference,[],[9,2,21])). % 184.98/184.96 cnf(69,plain, % 184.98/184.96 (P2(x691,f9(f8(x692,f9(f8(x693,x691)))))), % 184.98/184.96 inference(scs_inference,[],[9,65,21])). % 184.98/184.96 cnf(73,plain, % 184.98/184.96 (P2(x731,f9(f8(x732,f9(f8(x733,f9(f8(x734,x731)))))))), % 184.98/184.96 inference(scs_inference,[],[9,69,21])). % 184.98/184.96 cnf(78,plain, % 184.98/184.96 (P5(x781,f16(f10(x782,x781)))), % 184.98/184.96 inference(scs_inference,[],[10,4,23])). % 184.98/184.96 cnf(81,plain, % 184.98/184.96 (P2(f9(f8(x811,f9(f8(x812,f9(f8(x813,x814)))))),f9(f8(x815,x814)))), % 184.98/184.96 inference(scs_inference,[],[10,73,65,4,23,21])). % 184.98/184.96 cnf(85,plain, % 184.98/184.96 (P5(x851,f16(f10(x852,f16(f10(x853,x851)))))), % 184.98/184.96 inference(scs_inference,[],[10,78,23])). % 184.98/184.96 cnf(88,plain, % 184.98/184.96 (P2(f9(f8(x881,x882)),f9(f8(x883,f9(f8(x884,f9(f8(x885,x882)))))))), % 184.98/184.96 inference(scs_inference,[],[10,78,81,2,23,21])). % 184.98/184.96 cnf(92,plain, % 184.98/184.96 (P5(x921,f16(f10(x922,f16(f10(x923,f16(f10(x924,x921)))))))), % 184.98/184.96 inference(scs_inference,[],[10,85,23])). % 184.98/184.96 cnf(95,plain, % 184.98/184.96 (P2(f9(f8(x951,f9(f8(x952,f9(f8(x953,x954)))))),x954)), % 184.98/184.96 inference(scs_inference,[],[10,85,88,9,23,21])). % 184.98/184.96 cnf(99,plain, % 184.98/184.96 (P2(f9(f8(x991,x992)),f9(f8(x993,f9(f8(x994,x992)))))), % 184.98/184.96 inference(scs_inference,[],[81,9,21])). % 184.98/184.96 cnf(102,plain, % 184.98/184.96 (P2(f9(f8(x1021,f9(f8(x1022,x1023)))),f9(f8(x1024,f9(f8(x1025,x1023)))))), % 184.98/184.96 inference(scs_inference,[],[99,65,21])). % 184.98/184.96 cnf(105,plain, % 184.98/184.96 (P4(f5(x1051,f16(f16(f10(x1052,x1053)))),f5(x1051,f16(x1053)))), % 184.98/184.96 inference(scs_inference,[],[5,10,28,16])). % 184.98/184.96 cnf(109,plain, % 184.98/184.96 (P2(f9(f8(x1091,f9(f8(x1092,x1093)))),f9(f8(x1094,x1093)))), % 184.98/184.96 inference(scs_inference,[],[105,102,3,9,22,21])). % 184.98/184.96 cnf(113,plain, % 184.98/184.96 (P2(f9(f8(x1131,f9(f8(x1132,x1133)))),x1133)), % 184.98/184.96 inference(scs_inference,[],[109,95,21])). % 184.98/184.96 cnf(134,plain, % 184.98/184.96 (P2(f9(f8(x1341,x1342)),f9(f8(x1343,x1342)))), % 184.98/184.96 inference(scs_inference,[],[109,9,21])). % 184.98/184.96 cnf(139,plain, % 184.98/184.96 (P3(f13(f9(x1391)),f13(f9(f9(f8(x1392,x1391)))))), % 184.98/184.96 inference(scs_inference,[],[65,14,20])). % 184.98/184.96 cnf(141,plain, % 184.98/184.96 (P3(f13(f9(f9(f8(x1411,x1412)))),f13(f9(x1412)))), % 184.98/184.96 inference(scs_inference,[],[139,6,25])). % 184.98/184.96 cnf(144,plain, % 184.98/184.96 (P2(f8(f13(f9(f9(f8(x1441,x1442)))),f9(x1443)),f8(f13(f9(x1442)),f9(f9(f8(x1444,f9(f8(x1445,x1443)))))))), % 184.98/184.96 inference(scs_inference,[],[69,141,14,27])). % 184.98/184.96 cnf(147,plain, % 184.98/184.96 (P5(f16(f10(x1471,x1472)),f16(f10(x1473,f16(f10(x1474,f16(f10(x1475,x1472)))))))), % 184.98/184.96 inference(scs_inference,[],[78,92,23])). % 184.98/184.96 cnf(151,plain, % 184.98/184.96 (P5(f16(f10(x1511,x1512)),f16(f10(x1513,f16(f10(x1514,x1512)))))), % 184.98/184.96 inference(scs_inference,[],[78,85,23])). % 184.98/184.96 cnf(155,plain, % 184.98/184.96 (P5(f16(f10(x1551,f16(f10(x1552,x1553)))),x1553)), % 184.98/184.96 inference(scs_inference,[],[78,10,23])). % 184.98/184.96 cnf(159,plain, % 184.98/184.96 (P5(f16(f10(x1591,f16(f10(x1592,f16(f10(x1593,x1594)))))),x1594)), % 184.98/184.96 inference(scs_inference,[],[78,155,23])). % 184.98/184.96 cnf(165,plain, % 184.98/184.96 (P5(f16(f10(x1651,f16(f10(x1652,x1653)))),f16(f10(x1654,x1653)))), % 184.98/184.96 inference(scs_inference,[],[85,78,23])). % 184.98/184.96 cnf(169,plain, % 184.98/184.96 (P5(f16(f10(x1691,x1692)),f16(f10(x1693,x1692)))), % 184.98/184.96 inference(scs_inference,[],[165,10,23])). % 184.98/184.96 cnf(178,plain, % 184.98/184.96 (P5(f16(f10(x1781,f16(f10(x1782,f16(f10(x1783,x1784)))))),f16(f10(x1785,x1784)))), % 184.98/184.96 inference(scs_inference,[],[147,4,23])). % 184.98/184.96 cnf(182,plain, % 184.98/184.96 (P4(f5(x1821,f16(f16(f10(x1822,x1823)))),f5(x1821,f16(f16(f10(x1824,x1823)))))), % 184.98/184.96 inference(scs_inference,[],[169,5,16,28])). % 184.98/184.96 cnf(233,plain, % 184.98/184.96 (P5(f10(f5(x2331,f16(x2332)),f16(x2333)),f10(f5(f14(x2331),x2332),f16(x2333)))), % 184.98/184.96 inference(scs_inference,[],[4,37,16,29])). % 184.98/184.96 cnf(235,plain, % 184.98/184.96 (P5(f10(f5(f14(x2351),x2352),f16(x2353)),f16(f10(x2354,f16(f10(x2355,f10(f5(x2351,f16(x2352)),f16(x2353)))))))), % 184.98/184.96 inference(scs_inference,[],[233,85,23])). % 184.98/184.96 cnf(239,plain, % 184.98/184.96 (P5(f16(f10(x2391,f16(f10(x2392,f10(f5(x2393,f16(x2394)),f16(x2395)))))),f10(f5(f14(x2393),x2394),f16(x2395)))), % 184.98/184.96 inference(scs_inference,[],[235,4,23])). % 184.98/184.96 cnf(243,plain, % 184.98/184.96 (P5(f10(f5(f14(x2431),x2432),f16(x2433)),f10(f5(x2431,f16(x2432)),f16(x2433)))), % 184.98/184.96 inference(scs_inference,[],[239,155,23])). % 184.98/184.96 cnf(246,plain, % 184.98/184.96 (P4(f6(f16(f10(f5(f14(x2461),x2462),f16(x2463)))),f6(f16(f10(f5(x2461,f16(x2462)),f16(x2463)))))), % 184.98/184.96 inference(scs_inference,[],[243,16,15])). % 184.98/184.96 cnf(247,plain, % 184.98/184.96 (P4(f6(f16(f10(f5(x2471,f16(x2472)),f16(x2473)))),f6(f16(f10(f5(f14(x2471),x2472),f16(x2473)))))), % 184.98/184.96 inference(scs_inference,[],[246,3,22])). % 184.98/184.96 cnf(254,plain, % 184.98/184.96 (P5(f10(f5(f14(x2541),x2542),f16(x2543)),f16(f10(x2544,f10(f5(x2541,f16(x2542)),f16(x2543)))))), % 184.98/184.96 inference(scs_inference,[],[239,10,23])). % 184.98/184.96 cnf(258,plain, % 184.98/184.96 (P5(f16(f10(x2581,f10(f5(x2582,f16(x2583)),f16(x2584)))),f16(f10(x2585,f10(f5(f14(x2582),x2583),f16(x2584)))))), % 184.98/184.96 inference(scs_inference,[],[254,78,23])). % 184.98/184.96 cnf(262,plain, % 184.98/184.96 (P5(f16(f10(x2621,f10(f5(f14(x2622),x2623),f16(x2624)))),f10(f5(x2622,f16(x2623)),f16(x2624)))), % 184.98/184.96 inference(scs_inference,[],[258,10,23])). % 184.98/184.96 cnf(266,plain, % 184.98/184.96 (P5(f10(f5(x2661,f16(x2662)),f16(x2663)),f16(f10(x2664,f10(f5(f14(x2661),x2662),f16(x2663)))))), % 184.98/184.96 inference(scs_inference,[],[262,4,23])). % 184.98/184.96 cnf(270,plain, % 184.98/184.96 (P5(f16(f10(x2701,f10(f5(f14(x2702),x2703),f16(x2704)))),f16(f10(x2705,f10(f5(x2702,f16(x2703)),f16(x2704)))))), % 184.98/184.96 inference(scs_inference,[],[266,78,23])). % 184.98/184.96 cnf(274,plain, % 184.98/184.96 (P5(f16(f10(x2741,f10(f5(x2742,f16(x2743)),f16(x2744)))),f10(f5(f14(x2742),x2743),f16(x2744)))), % 184.98/184.96 inference(scs_inference,[],[270,10,23])). % 184.98/184.96 cnf(290,plain, % 184.98/184.96 (P4(f6(f16(f16(f10(x2901,x2902)))),f6(f16(x2902)))), % 184.98/184.96 inference(scs_inference,[],[10,16,15])). % 184.98/184.96 cnf(291,plain, % 184.98/184.96 (P4(f6(f16(x2911)),f6(f16(f16(f10(x2912,x2911)))))), % 184.98/184.96 inference(scs_inference,[],[290,3,22])). % 184.98/184.96 cnf(294,plain, % 184.98/184.96 (P5(f10(f6(f16(x2941)),f16(f16(f10(x2942,x2943)))),f10(f6(f16(f16(f10(x2944,x2941)))),f16(x2943)))), % 184.98/184.96 inference(scs_inference,[],[10,291,16,29])). % 184.98/184.96 cnf(296,plain, % 184.98/184.96 (P5(f10(f6(f16(f16(f10(x2961,x2962)))),f16(x2963)),f10(f6(f16(x2962)),f16(f16(f10(x2964,x2963)))))), % 184.98/184.96 inference(scs_inference,[],[294,4,23])). % 184.98/184.96 cnf(313,plain, % 184.98/184.96 (P4(f5(f4(x3131),f10(f5(x3132,f16(x3133)),f16(x3134))),f5(f4(x3131),f10(f5(f14(x3132),x3133),f16(x3134))))), % 184.98/184.96 inference(scs_inference,[],[5,233,17,28])). % 184.98/184.96 cnf(327,plain, % 184.98/184.96 (P3(f7(f17(x3271),x3272),f7(f17(x3271),f9(f8(x3273,x3272))))), % 184.98/184.96 inference(scs_inference,[],[5,65,18,31])). % 184.98/184.96 cnf(332,plain, % 184.98/184.96 (P3(f7(f17(x3321),f9(f8(x3322,x3323))),f7(f17(x3321),x3323))), % 184.98/184.96 inference(scs_inference,[],[327,6,25])). % 184.98/184.96 cnf(361,plain, % 184.98/184.96 (P3(f7(f14(x3611),x3612),f7(f14(x3611),f9(f8(x3613,x3612))))), % 184.98/184.96 inference(scs_inference,[],[5,65,19,31])). % 184.98/184.96 cnf(363,plain, % 184.98/184.96 (P3(f7(f14(x3631),f9(f8(x3632,x3633))),f7(f14(x3631),f9(f8(x3634,x3633))))), % 184.98/184.96 inference(scs_inference,[],[5,134,19,31])). % 184.98/184.96 cnf(371,plain, % 184.98/184.96 (P3(f7(f14(x3711),f9(f8(x3712,f9(f8(x3713,x3714))))),f7(f14(x3711),x3714))), % 184.98/184.96 inference(scs_inference,[],[5,113,19,31])). % 184.98/184.96 cnf(387,plain, % 184.98/184.96 (P2(f8(f13(x3871),x3871),f8(f13(f9(f8(x3872,x3871))),f9(f8(x3872,x3871))))), % 184.98/184.96 inference(scs_inference,[],[65,20,27])). % 184.98/184.96 cnf(388,plain, % 184.98/184.96 (P2(f8(f13(f9(f8(x3881,x3882))),f9(f8(x3881,x3882))),f9(f8(x3883,f8(f13(x3882),x3882))))), % 184.98/184.96 inference(scs_inference,[],[387,65,21])). % 184.98/184.96 cnf(392,plain, % 184.98/184.96 (P2(f8(f13(f9(f8(x3921,x3922))),f9(f8(x3921,x3922))),f8(f13(x3922),x3922))), % 184.98/184.97 inference(scs_inference,[],[387,2,21])). % 184.98/184.97 cnf(395,plain, % 184.98/184.97 (P2(f8(f13(f8(f13(f9(f8(x3951,x3952))),f9(f8(x3951,x3952)))),f8(f13(f9(f8(x3951,x3952))),f9(f8(x3951,x3952)))),f8(f13(f8(f13(x3952),x3952)),f8(f13(x3952),x3952)))), % 184.98/184.97 inference(scs_inference,[],[392,20,27])). % 184.98/184.97 cnf(396,plain, % 184.98/184.97 (P2(f9(f8(x3961,f8(f13(x3962),x3962))),f8(f13(f9(f8(x3963,x3962))),f9(f8(x3963,x3962))))), % 184.98/184.97 inference(scs_inference,[],[388,2,21])). % 184.98/184.97 cnf(401,plain, % 184.98/184.97 (P2(f8(f13(x4011),x4011),f9(f8(x4012,f8(f13(f9(f8(x4013,x4011))),f9(f8(x4013,x4011))))))), % 184.98/184.97 inference(scs_inference,[],[392,65,21])). % 184.98/184.97 cnf(405,plain, % 184.98/184.97 (P2(f9(f8(x4051,f8(f13(f9(f8(x4052,x4053))),f9(f8(x4052,x4053))))),f8(f13(x4053),x4053))), % 184.98/184.97 inference(scs_inference,[],[401,2,21])). % 184.98/184.97 cnf(410,plain, % 184.98/184.97 (P2(f8(f13(f8(f13(x4101),x4101)),f8(f13(x4101),x4101)),f8(f13(f8(f13(f9(f8(x4102,x4101))),f9(f8(x4102,x4101)))),f8(f13(f9(f8(x4102,x4101))),f9(f8(x4102,x4101)))))), % 184.98/184.97 inference(scs_inference,[],[387,20,27])). % 184.98/184.97 cnf(421,plain, % 184.98/184.97 (P3(f7(f14(x4211),f9(f8(x4212,x4213))),f7(f14(x4211),x4213))), % 184.98/184.97 inference(scs_inference,[],[361,6,25])). % 184.98/184.97 cnf(524,plain, % 184.98/184.97 (P3(f7(f15(f15(f14(a3),f4(f17(a2))),a1),x5241),f7(f14(f15(f15(a3,f4(f17(a2))),a1)),x5241))), % 184.98/184.97 inference(scs_inference,[],[1,2,32,31])). % 184.98/184.97 cnf(811,plain, % 184.98/184.97 (P2(f8(f7(f17(x8111),f9(f8(x8112,x8113))),f9(f8(x8114,x8115))),f8(f7(f17(x8111),x8113),f9(f8(x8114,x8115))))), % 184.98/184.97 inference(scs_inference,[],[134,332,21,27])). % 184.98/184.97 cnf(812,plain, % 184.98/184.97 (P2(f8(f7(f17(x8121),x8122),f9(f8(x8123,x8124))),f9(f8(x8125,f8(f7(f17(x8121),f9(f8(x8126,x8122))),f9(f8(x8123,x8124))))))), % 184.98/184.97 inference(scs_inference,[],[811,65,21])). % 184.98/184.97 cnf(816,plain, % 184.98/184.97 (P2(f9(f8(x8161,f8(f7(f17(x8162),f9(f8(x8163,x8164))),f9(f8(x8165,x8166))))),f8(f7(f17(x8162),x8164),f9(f8(x8165,x8166))))), % 184.98/184.97 inference(scs_inference,[],[812,2,21])). % 184.98/184.97 cnf(819,plain, % 184.98/184.97 (P2(f8(f7(f17(x8191),x8192),f9(f8(x8193,x8194))),f8(f7(f17(x8191),f9(f8(x8195,x8192))),f9(f8(x8193,x8194))))), % 184.98/184.97 inference(scs_inference,[],[816,9,21])). % 184.98/184.97 cnf(838,plain, % 184.98/184.97 (P2(f8(f7(f17(x8381),f9(f8(x8382,x8383))),f9(f8(x8384,x8385))),f9(f8(x8386,f8(f7(f17(x8381),x8383),f9(f8(x8384,x8385))))))), % 184.98/184.97 inference(scs_inference,[],[819,65,21])). % 184.98/184.97 cnf(841,plain, % 184.98/184.97 (P2(f9(f8(x8411,f8(f7(f17(x8412),x8413),f9(f8(x8414,x8415))))),f8(f7(f17(x8412),f9(f8(x8416,x8413))),f9(f8(x8414,x8415))))), % 184.98/184.97 inference(scs_inference,[],[838,2,21])). % 184.98/184.97 cnf(888,plain, % 184.98/184.97 (P5(f10(f6(f10(f5(x8881,f16(x8882)),f16(x8883))),f10(f5(x8881,f16(x8882)),f16(x8883))),f10(f6(f10(f5(f14(x8881),x8882),f16(x8883))),f10(f5(f14(x8881),x8882),f16(x8883))))), % 184.98/184.97 inference(scs_inference,[],[233,15,29])). % 184.98/184.97 cnf(889,plain, % 184.98/184.97 (P5(f10(f6(f10(f5(f14(x8891),x8892),f16(x8893))),f10(f5(f14(x8891),x8892),f16(x8893))),f10(f6(f10(f5(x8891,f16(x8892)),f16(x8893))),f10(f5(x8891,f16(x8892)),f16(x8893))))), % 184.98/184.97 inference(scs_inference,[],[888,4,23])). % 184.98/184.97 cnf(913,plain, % 184.98/184.97 (P5(f10(f6(f16(f10(x9131,x9132))),f16(f10(x9131,x9132))),f10(f6(x9132),x9132))), % 184.98/184.97 inference(scs_inference,[],[10,15,29])). % 184.98/184.97 cnf(914,plain, % 184.98/184.97 (P5(f10(f6(f10(f6(f16(f10(x9141,x9142))),f16(f10(x9141,x9142)))),f10(f6(f16(f10(x9141,x9142))),f16(f10(x9141,x9142)))),f10(f6(f10(f6(x9142),x9142)),f10(f6(x9142),x9142)))), % 184.98/184.97 inference(scs_inference,[],[913,15,29])). % 184.98/184.97 cnf(915,plain, % 184.98/184.97 (P5(f10(f6(x9151),x9151),f16(f10(x9152,f10(f6(f16(f10(x9153,x9151))),f16(f10(x9153,x9151))))))), % 184.98/184.97 inference(scs_inference,[],[913,78,23])). % 184.98/184.97 cnf(919,plain, % 184.98/184.97 (P5(f16(f10(x9191,f10(f6(f16(f10(x9192,x9193))),f16(f10(x9192,x9193))))),f10(f6(x9193),x9193))), % 184.98/184.97 inference(scs_inference,[],[915,4,23])). % 184.98/184.97 cnf(923,plain, % 184.98/184.97 (P5(f10(f6(x9231),x9231),f10(f6(f16(f10(x9232,x9231))),f16(f10(x9232,x9231))))), % 184.98/184.97 inference(scs_inference,[],[919,10,23])). % 184.98/184.97 cnf(927,plain, % 184.98/184.97 (P5(f10(f6(f16(f10(x9271,x9272))),f16(f10(x9271,x9272))),f16(f10(x9273,f10(f6(x9272),x9272))))), % 184.98/184.97 inference(scs_inference,[],[923,78,23])). % 184.98/184.97 cnf(931,plain, % 184.98/184.97 (P5(f16(f10(x9311,f10(f6(x9312),x9312))),f10(f6(f16(f10(x9313,x9312))),f16(f10(x9313,x9312))))), % 184.98/184.97 inference(scs_inference,[],[927,4,23])). % 184.98/184.97 cnf(1064,plain, % 184.98/184.97 (P5(f10(f6(f16(f10(f5(x10641,f16(x10642)),f16(x10643)))),f16(x10644)),f10(f6(f16(f10(f5(f14(x10641),x10642),f16(x10643)))),f16(x10644)))), % 184.98/184.97 inference(scs_inference,[],[4,247,16,29])). % 184.98/184.97 cnf(1071,plain, % 184.98/184.97 (P5(f16(f10(f5(f4(a2),x10711),f10(f6(f16(f10(f5(x10712,f16(x10713)),f16(x10714)))),f16(x10715)))),f16(f10(f6(x10711),f10(f6(f16(f10(f5(f14(x10712),x10713),f16(x10714)))),f16(x10715)))))), % 184.98/184.97 inference(scs_inference,[],[7,1064,16,29])). % 184.98/184.97 cnf(1074,plain, % 184.98/184.97 (P5(f10(f5(x10741,f16(f16(f10(x10742,x10743)))),f16(f16(f10(x10744,x10745)))),f10(f5(x10741,f16(f16(f10(x10746,x10743)))),f16(x10745)))), % 184.98/184.97 inference(scs_inference,[],[10,182,16,29])). % 184.98/184.97 cnf(1095,plain, % 184.98/184.97 (P5(f10(f5(f4(x10951),f10(f5(x10952,f16(x10953)),f16(x10954))),f16(f16(f10(x10955,f16(f10(x10956,x10957)))))),f10(f5(f4(x10951),f10(f5(f14(x10952),x10953),f16(x10954))),f16(x10957)))), % 184.98/184.97 inference(scs_inference,[],[155,313,16,29])). % 184.98/184.97 cnf(1271,plain, % 184.98/184.97 (P2(f8(f13(f9(f8(x12711,f9(f8(x12712,x12713))))),f9(f8(x12711,f9(f8(x12712,x12713))))),f8(f13(x12713),x12713))), % 184.98/184.97 inference(scs_inference,[],[113,20,27])). % 184.98/184.97 cnf(1456,plain, % 184.98/184.97 (P2(f8(f13(f9(x14561)),f9(f8(x14562,x14563))),f8(f13(f9(f9(f8(x14564,x14561)))),f9(f8(x14562,x14563))))), % 184.98/184.97 inference(scs_inference,[],[65,139,21,27])). % 184.98/184.97 cnf(1464,plain, % 184.98/184.97 (P2(f8(f7(f14(x14641),f9(f8(x14642,x14643))),f9(f8(x14644,x14645))),f8(f7(f14(x14641),x14643),f9(f8(x14644,x14645))))), % 184.98/184.97 inference(scs_inference,[],[81,421,21,27])). % 184.98/184.97 cnf(1466,plain, % 184.98/184.97 (P2(f8(f7(f14(x14661),x14662),f9(f8(x14663,x14664))),f9(f8(x14665,f8(f7(f14(x14661),f9(f8(x14666,x14662))),f9(f8(x14663,x14664))))))), % 184.98/184.97 inference(scs_inference,[],[1464,65,21])). % 184.98/184.97 cnf(1470,plain, % 184.98/184.97 (P2(f9(f8(x14701,f8(f7(f14(x14702),f9(f8(x14703,x14704))),f9(f8(x14705,x14706))))),f8(f7(f14(x14702),x14704),f9(f8(x14705,x14706))))), % 184.98/184.97 inference(scs_inference,[],[1466,2,21])). % 184.98/184.97 cnf(1473,plain, % 184.98/184.97 (P2(f8(f7(f14(x14731),x14732),f9(f8(x14733,x14734))),f8(f7(f14(x14731),f9(f8(x14735,x14732))),f9(f8(x14733,x14734))))), % 184.98/184.97 inference(scs_inference,[],[1470,9,21])). % 184.98/184.97 cnf(1476,plain, % 184.98/184.97 (P2(f8(f13(f9(f9(f8(x14761,x14762)))),f8(f7(f14(x14763),f9(f8(x14764,x14765))),f9(f8(x14766,x14767)))),f8(f13(f9(x14762)),f8(f7(f14(x14763),f9(f8(x14764,x14765))),f9(f8(x14766,x14767)))))), % 184.98/184.97 inference(scs_inference,[],[1473,141,21,27])). % 184.98/184.97 cnf(1479,plain, % 184.98/184.97 (P2(f8(f7(f14(x14791),f9(f8(x14792,f9(f8(x14793,x14794))))),x14795),f8(f7(f14(x14791),x14794),x14795))), % 184.98/184.97 inference(scs_inference,[],[95,371,21,27])). % 184.98/184.97 cnf(1482,plain, % 184.98/184.97 (P2(f8(f7(f17(x14821),x14822),f8(f7(f14(x14823),x14824),x14825)),f8(f7(f17(x14821),f9(f8(x14826,x14822))),f8(f7(f14(x14823),x14824),x14825)))), % 184.98/184.97 inference(scs_inference,[],[1479,327,21,27])). % 184.98/184.97 cnf(1489,plain, % 184.98/184.97 (P2(f8(f7(f14(x14891),f9(f8(x14892,x14893))),x14894),f8(f7(f14(x14891),f9(f8(x14895,x14893))),x14894))), % 184.98/184.97 inference(scs_inference,[],[113,363,21,27])). % 184.98/184.97 cnf(1522,plain, % 184.98/184.97 (P2(f8(f7(f14(x15221),f9(f8(x15222,x15223))),f9(f8(x15224,x15225))),f9(f8(x15226,f8(f7(f14(x15221),x15223),f9(f8(x15224,x15225))))))), % 184.98/184.97 inference(scs_inference,[],[1473,65,21])). % 184.98/184.97 cnf(1528,plain, % 184.98/184.97 (P2(f9(f8(x15281,f8(f7(f14(x15282),x15283),f9(f8(x15284,x15285))))),f8(f7(f14(x15282),f9(f8(x15286,x15283))),f9(f8(x15284,x15285))))), % 184.98/184.97 inference(scs_inference,[],[1522,2,21])). % 184.98/184.97 cnf(1637,plain, % 184.98/184.97 (P5(f10(f5(f4(x16371),f10(f5(f14(x16372),x16373),f16(x16374))),f16(x16375)),f10(f5(f4(x16371),f10(f5(x16372,f16(x16373)),f16(x16374))),f16(f16(f10(x16376,f16(f10(x16377,x16375)))))))), % 184.98/184.97 inference(scs_inference,[],[1095,4,23])). % 184.98/184.97 cnf(1662,plain, % 184.98/184.97 (P6(f15(f15(f14(a3),f4(f17(a2))),a1),f14(f15(f15(a3,f4(f17(a2))),a1)))), % 184.98/184.97 inference(scs_inference,[],[1,395,914,14,15,16,20,32])). % 184.98/184.97 cnf(1684,plain, % 184.98/184.97 (P6(f15(f15(f15(f14(a3),f4(f17(a2))),a1),x16841),f15(f14(f15(f15(a3,f4(f17(a2))),a1)),x16841))), % 184.98/184.97 inference(scs_inference,[],[1662,1074,1271,1528,155,5,14,20,15,16,28,30])). % 184.98/184.97 cnf(1693,plain, % 184.98/184.97 (P2(f9(f9(f8(x16931,x16932))),f9(x16932))), % 184.98/184.97 inference(scs_inference,[],[9,14])). % 184.98/184.97 cnf(1797,plain, % 184.98/184.97 (P5(f16(f16(f10(x17971,f10(f5(x17972,f16(x17973)),f16(x17974))))),f16(f16(f10(x17975,f10(f5(f14(x17972),x17973),f16(x17974))))))), % 184.98/184.97 inference(scs_inference,[],[1456,258,841,14,20,15,16])). % 184.98/184.97 cnf(1803,plain, % 184.98/184.97 (P2(f9(f8(f13(f9(f8(x18031,x18032))),f9(f8(x18031,x18032)))),f9(f9(f8(x18033,f8(f13(x18032),x18032)))))), % 184.98/184.97 inference(scs_inference,[],[388,14])). % 184.98/184.97 cnf(1823,plain, % 184.98/184.97 (P2(f9(f8(x18231,x18232)),f9(f9(f8(x18233,f8(f13(x18232),x18232)))))), % 184.98/184.97 inference(scs_inference,[],[1803,1482,296,9,14,20,15,16,21])). % 184.98/184.97 cnf(1829,plain, % 184.98/184.97 (P2(f9(f9(f8(x18291,x18292))),f9(f9(f9(f8(x18293,f8(f13(x18292),x18292))))))), % 184.98/184.97 inference(scs_inference,[],[1823,14])). % 184.98/184.97 cnf(1860,plain, % 184.98/184.97 (P2(f9(f9(f8(x18601,x18602))),f9(f9(f8(x18603,x18602))))), % 184.98/184.97 inference(scs_inference,[],[134,14])). % 184.98/184.97 cnf(1872,plain, % 184.98/184.97 (P2(f9(f9(f9(f8(x18721,x18722)))),f9(f9(f9(f8(x18723,x18722)))))), % 184.98/184.97 inference(scs_inference,[],[1860,14])). % 184.98/184.97 cnf(1874,plain, % 184.98/184.97 (P3(f13(f8(f7(f14(x18741),f9(f8(x18742,x18743))),f9(f8(x18744,x18745)))),f13(f8(f7(f14(x18741),x18743),f9(f8(x18744,x18745)))))), % 184.98/184.97 inference(scs_inference,[],[1860,1464,14,20])). % 184.98/184.97 cnf(1878,plain, % 184.98/184.97 (P5(f16(f16(f10(x18781,f16(f10(x18782,x18783))))),f16(f16(f10(x18784,x18783))))), % 184.98/184.97 inference(scs_inference,[],[1860,1464,85,165,14,20,15,16])). % 184.98/184.97 cnf(1894,plain, % 184.98/184.97 (P2(f9(f8(x18941,f9(f9(f9(f8(x18942,x18943)))))),f9(f9(f9(f8(x18944,x18943)))))), % 184.98/184.97 inference(scs_inference,[],[1872,1878,913,65,14,20,16,15,21])). % 184.98/184.97 cnf(1922,plain, % 184.98/184.97 (P2(f9(f8(x19221,f9(f9(f8(x19222,x19223))))),f9(f9(f9(f8(x19224,f8(f13(x19223),x19223))))))), % 184.98/184.97 inference(scs_inference,[],[1829,1894,923,151,65,14,20,16,15,21])). % 184.98/184.97 cnf(1928,plain, % 184.98/184.97 (P4(f6(f16(f10(x19281,f10(f5(f14(x19282),x19283),f16(x19284))))),f6(f10(f5(x19282,f16(x19283)),f16(x19284))))), % 184.98/184.97 inference(scs_inference,[],[1528,262,20,15])). % 184.98/184.97 cnf(1930,plain, % 184.98/184.97 (P2(f9(x19301),f9(f9(f8(x19302,f9(f8(x19303,x19301))))))), % 184.98/184.97 inference(scs_inference,[],[1528,262,69,20,15,14])). % 184.98/184.97 cnf(1941,plain, % 184.98/184.97 (P2(f9(f9(x19411)),f9(f9(f9(f8(x19412,f9(f8(x19413,x19411)))))))), % 184.98/184.97 inference(scs_inference,[],[1930,1489,274,15,16,20,14])). % 184.98/184.97 cnf(2011,plain, % 184.98/184.97 (P3(f13(f9(f8(x20111,x20112))),f13(x20112))), % 184.98/184.97 inference(scs_inference,[],[294,9,16,20])). % 184.98/184.97 cnf(2024,plain, % 184.98/184.97 (P2(f9(f9(f8(x20241,f8(f13(x20242),x20242)))),f9(f8(f13(f9(f8(x20243,x20242))),f9(f8(x20243,x20242)))))), % 184.98/184.97 inference(scs_inference,[],[159,387,396,16,20,14])). % 184.98/184.97 cnf(2028,plain, % 184.98/184.97 (P2(f8(f13(f9(f8(x20281,x20282))),f9(f9(f8(x20283,x20284)))),f8(f13(x20282),f9(f9(f8(x20285,x20284)))))), % 184.98/184.97 inference(scs_inference,[],[2011,1860,159,387,396,16,20,14,15,27])). % 184.98/184.97 cnf(2038,plain, % 184.98/184.97 (P2(f9(f8(f13(f9(f8(x20381,x20382))),f9(f9(f8(x20383,x20384))))),f9(f8(f13(x20382),f9(f9(f8(x20385,x20384))))))), % 184.98/184.97 inference(scs_inference,[],[2028,178,16,20,14])). % 184.98/184.97 cnf(2047,plain, % 184.98/184.97 (P5(f16(f16(f10(x20471,x20472))),f16(f16(f10(x20473,x20472))))), % 184.98/184.97 inference(scs_inference,[],[169,16])). % 184.98/184.97 cnf(2062,plain, % 184.98/184.97 (P5(f10(f6(f16(f16(f10(x20621,x20622)))),f16(f16(f10(x20621,x20622)))),f10(f6(f16(f16(f10(x20623,x20622)))),f16(f16(f10(x20623,x20622)))))), % 184.98/184.97 inference(scs_inference,[],[2047,15,29])). % 184.98/184.97 cnf(2067,plain, % 184.98/184.97 (P2(f9(f9(f8(x20671,f9(f8(x20672,x20673))))),f9(f9(f8(x20674,f9(f8(x20675,x20673))))))), % 184.98/184.97 inference(scs_inference,[],[2062,388,102,20,16,14])). % 184.98/184.97 cnf(2076,plain, % 184.98/184.97 (P5(f16(f16(f16(f10(x20761,x20762)))),f16(f16(f16(f10(x20763,x20762)))))), % 184.98/184.97 inference(scs_inference,[],[2047,16])). % 184.98/184.97 cnf(2088,plain, % 184.98/184.97 (P2(f9(f9(f8(x20881,x20882))),f9(f8(f13(x20883),f9(f9(f8(x20884,x20882))))))), % 184.98/184.97 inference(scs_inference,[],[1928,2067,2038,2047,889,6,81,9,16,20,14,15,29,27,21])). % 184.98/184.97 cnf(2094,plain, % 184.98/184.97 (P5(f16(f16(f16(f16(f10(x20941,x20942))))),f16(f16(f16(f16(f10(x20943,x20942))))))), % 184.98/184.97 inference(scs_inference,[],[2076,134,20,16])). % 184.98/184.97 cnf(2105,plain, % 184.98/184.97 (P2(f9(x21051),f9(f9(f8(x21052,x21051))))), % 184.98/184.97 inference(scs_inference,[],[2094,69,65,16,20,14])). % 184.98/184.97 cnf(2117,plain, % 184.98/184.97 (P5(f16(f16(f10(x21171,f10(f5(f14(x21172),x21173),f16(x21174))))),f16(f10(f5(x21172,f16(x21173)),f16(x21174))))), % 184.98/184.97 inference(scs_inference,[],[262,109,20,16])). % 184.98/184.97 cnf(2119,plain, % 184.98/184.97 (P2(f9(f9(x21191)),f9(f9(f9(f8(x21192,x21191)))))), % 184.98/184.97 inference(scs_inference,[],[2105,262,109,20,16,14])). % 184.98/184.97 cnf(2134,plain, % 184.98/184.97 (P2(f9(f9(f9(x21341))),f9(f9(f9(f9(f8(x21342,x21341))))))), % 184.98/184.97 inference(scs_inference,[],[2119,2117,16,20,14])). % 184.98/184.97 cnf(2136,plain, % 184.98/184.97 (P4(f6(f16(f10(x21361,f16(f10(x21362,x21363))))),f6(f16(f10(x21364,x21363))))), % 184.98/184.97 inference(scs_inference,[],[2119,2117,165,16,20,14,15])). % 184.98/184.97 cnf(2144,plain, % 184.98/184.97 (P3(f13(f9(f9(f9(x21441)))),f13(f9(f9(f9(f9(f8(x21442,x21441)))))))), % 184.98/184.97 inference(scs_inference,[],[2134,20])). % 184.98/184.97 cnf(2146,plain, % 184.98/184.97 (P5(f16(f10(f5(f14(x21461),x21462),f16(x21463))),f16(f16(f10(x21464,f10(f5(x21461,f16(x21462)),f16(x21463))))))), % 184.98/184.97 inference(scs_inference,[],[2134,254,20,16])). % 184.98/184.97 cnf(2150,plain, % 184.98/184.97 (P4(f6(f16(f10(x21501,f10(f6(x21502),x21502)))),f6(f10(f6(f16(f10(x21503,x21502))),f16(f10(x21503,x21502)))))), % 184.98/184.97 inference(scs_inference,[],[2134,254,931,20,16,14,15])). % 184.98/184.97 cnf(2152,plain, % 184.98/184.97 (P2(f8(x21521,f9(f9(f9(x21522)))),f8(x21521,f9(f9(f9(f9(f8(x21523,x21522)))))))), % 184.98/184.97 inference(scs_inference,[],[2134,254,931,6,20,16,14,15,27])). % 184.98/184.97 cnf(2155,plain, % 184.98/184.97 (P5(f16(f10(f6(f16(f10(x21551,x21552))),f16(f10(x21551,x21552)))),f16(f16(f10(x21553,f10(f6(x21552),x21552)))))), % 184.98/184.97 inference(scs_inference,[],[927,16])). % 184.98/184.97 cnf(2159,plain, % 184.98/184.97 (P2(f9(f9(f8(x21591,f8(f13(f9(f8(x21592,x21593))),f9(f8(x21592,x21593)))))),f9(f8(f13(x21593),x21593)))), % 184.98/184.97 inference(scs_inference,[],[927,99,405,16,20,14])). % 184.98/184.97 cnf(2170,plain, % 184.98/184.97 (P2(f9(f9(f8(x21701,f9(f8(x21702,x21703))))),f9(x21703))), % 184.98/184.97 inference(scs_inference,[],[2155,396,113,20,16,14])). % 184.98/184.97 cnf(2172,plain, % 184.98/184.97 (P4(f6(f16(f10(x21721,x21722))),f6(x21722))), % 184.98/184.97 inference(scs_inference,[],[2155,10,396,113,20,16,14,15])). % 184.98/184.97 cnf(2181,plain, % 184.98/184.97 (P2(f9(f9(f9(f8(x21811,f9(f8(x21812,x21813)))))),f9(f9(x21813)))), % 184.98/184.97 inference(scs_inference,[],[2170,919,102,16,20,14])). % 184.98/184.97 cnf(2195,plain, % 184.98/184.97 (P5(f16(f16(f10(x21951,x21952))),f16(x21952))), % 184.98/184.97 inference(scs_inference,[],[2181,10,20,16])). % 184.98/184.97 cnf(2199,plain, % 184.98/184.97 (P5(f10(f6(f16(f16(f10(x21991,x21992)))),f16(f16(f10(x21991,x21992)))),f10(f6(f16(x21992)),f16(x21992)))), % 184.98/184.97 inference(scs_inference,[],[2195,15,29])). % 184.98/184.97 cnf(2210,plain, % 184.98/184.97 (P5(f10(f6(f16(f10(x22101,x22102))),f10(f6(f16(f16(f10(x22103,x22104)))),f16(f16(f10(x22103,x22104))))),f10(f6(x22102),f10(f6(f16(x22104)),f16(x22104))))), % 184.98/184.97 inference(scs_inference,[],[2172,2199,65,95,5,16,20,14,15,28,29])). % 184.98/184.97 cnf(2216,plain, % 184.98/184.97 (P3(f13(f8(f13(f9(f8(x22161,x22162))),f9(f8(x22161,x22162)))),f13(f8(f13(x22162),x22162)))), % 184.98/184.97 inference(scs_inference,[],[392,20])). % 184.98/184.97 cnf(2239,plain, % 184.98/184.97 (P3(f13(f9(f8(x22391,f9(f8(x22392,x22393))))),f13(x22393))), % 184.98/184.97 inference(scs_inference,[],[113,20])). % 184.98/184.97 cnf(2246,plain, % 184.98/184.97 (P5(f16(f16(f16(f10(x22461,x22462)))),f16(f16(x22462)))), % 184.98/184.97 inference(scs_inference,[],[2195,16])). % 184.98/184.97 cnf(2250,plain, % 184.98/184.97 (P4(f6(f16(f16(f16(f10(x22501,x22502))))),f6(f16(f16(x22502))))), % 184.98/184.97 inference(scs_inference,[],[2195,95,16,20,15])). % 184.98/184.97 cnf(2252,plain, % 184.98/184.97 (P2(f8(f13(f9(f8(x22521,f9(f8(x22522,x22523))))),f9(f9(f8(x22524,x22525)))),f8(f13(x22523),f9(x22525)))), % 184.98/184.97 inference(scs_inference,[],[2239,2195,1693,95,16,20,15,27])). % 184.98/184.97 cnf(2259,plain, % 184.98/184.97 (P5(f16(f16(f16(f16(f10(x22591,x22592))))),f16(f16(f16(x22592))))), % 184.98/184.97 inference(scs_inference,[],[2252,2246,20,16])). % 184.98/184.97 cnf(2278,plain, % 184.98/184.97 (P2(f9(f8(f13(f8(f13(f9(f8(x22781,x22782))),f9(f8(x22781,x22782)))),f9(x22783))),f9(f8(f13(f8(f13(x22782),x22782)),f9(f9(f8(x22784,x22783))))))), % 184.98/184.97 inference(scs_inference,[],[2216,2250,2259,2246,2105,16,15,29,27,20,14])). % 184.98/184.97 cnf(2289,plain, % 184.98/184.97 (P5(f16(x22891),f16(f16(f10(x22892,x22891))))), % 184.98/184.97 inference(scs_inference,[],[78,16])). % 184.98/184.97 cnf(2291,plain, % 184.98/184.97 (P5(f10(f6(f16(x22911)),f16(x22911)),f10(f6(f16(f16(f10(x22912,x22911)))),f16(f16(f10(x22912,x22911)))))), % 184.98/184.97 inference(scs_inference,[],[2289,15,29])). % 184.98/184.97 cnf(2292,plain, % 184.98/184.97 (P5(f16(f10(f6(f16(x22921)),f16(x22921))),f16(f10(f6(f16(f16(f10(x22922,x22921)))),f16(f16(f10(x22922,x22921))))))), % 184.98/184.97 inference(scs_inference,[],[2291,16])). % 184.98/184.97 cnf(2298,plain, % 184.98/184.97 (P5(f10(x22981,f10(f6(f16(x22982)),f16(x22982))),f10(x22981,f10(f6(f16(f16(f10(x22983,x22982)))),f16(f16(f10(x22983,x22982))))))), % 184.98/184.97 inference(scs_inference,[],[2291,3,5,16,15,28,29])). % 184.98/184.97 cnf(2304,plain, % 184.98/184.97 (P5(f16(f16(x23041)),f16(f16(f16(f10(x23042,x23041)))))), % 184.98/184.97 inference(scs_inference,[],[2289,16])). % 184.98/184.97 cnf(2308,plain, % 184.98/184.97 (P5(f10(f6(f16(f10(x23081,f16(f10(x23082,x23083))))),f16(x23084)),f10(f6(f16(f10(x23085,x23083))),f16(f16(f10(x23086,x23084)))))), % 184.98/184.97 inference(scs_inference,[],[2136,2289,16,15,29])). % 184.98/184.97 cnf(2314,plain, % 184.98/184.97 (P5(f16(f10(f6(f16(f10(x23141,f16(f10(x23142,x23143))))),f16(x23144))),f16(f10(f6(f16(f10(x23145,x23143))),f16(f16(f10(x23146,x23144))))))), % 184.98/184.97 inference(scs_inference,[],[2308,16])). % 184.98/184.97 cnf(2321,plain, % 184.98/184.97 (P5(f16(f16(f16(x23211))),f16(f16(f16(f16(f10(x23212,x23211))))))), % 184.98/184.97 inference(scs_inference,[],[2304,16])). % 184.98/184.97 cnf(2330,plain, % 184.98/184.97 (P5(x23301,f16(f10(f6(f16(f10(x23302,x23303))),f16(f16(f10(x23304,f10(x23305,x23301)))))))), % 184.98/184.97 inference(scs_inference,[],[2314,2321,155,16,23])). % 184.98/184.97 cnf(2335,plain, % 184.98/184.97 (P2(x23351,f9(f8(f13(f8(f13(x23352),x23352)),f9(f9(f8(x23353,f8(x23354,x23351)))))))), % 184.98/184.97 inference(scs_inference,[],[2278,113,21])). % 184.98/184.97 cnf(2373,plain, % 184.98/184.97 (P5(f16(f16(f10(f5(f14(x23731),x23732),f16(x23733)))),f16(f16(f16(f10(x23734,f10(f5(x23731,f16(x23732)),f16(x23733)))))))), % 184.98/184.97 inference(scs_inference,[],[2159,2152,2146,20,14,16])). % 184.98/184.97 cnf(2379,plain, % 184.98/184.97 (P2(f9(f8(f13(f8(f13(x23791),x23791)),f9(f9(f8(x23792,f8(x23793,x23794)))))),x23794)), % 184.98/184.97 inference(scs_inference,[],[2,1874,2335,2159,2152,2146,2292,20,14,16,15,27,21])). % 184.98/184.97 cnf(2544,plain, % 184.98/184.97 (P2(x25441,f9(f9(f9(f8(x25442,f8(f13(f8(x25443,x25441)),f8(x25443,x25441)))))))), % 184.98/184.97 inference(scs_inference,[],[410,1922,1071,1797,2379,1684,2105,147,10,20,16,15,14,31,23,21])). % 184.98/184.97 cnf(2601,plain, % 184.98/184.97 (P5(f16(f10(x26011,f10(f6(f16(x26012)),f16(x26012)))),f16(f10(x26011,f10(f6(f16(f16(f10(x26013,x26012)))),f16(f16(f10(x26013,x26012)))))))), % 184.98/184.97 inference(scs_inference,[],[2088,2298,20,16])). % 184.98/184.97 cnf(2640,plain, % 184.98/184.97 (P5(f16(f10(f6(f16(f10(x26401,x26402))),f16(f16(f10(x26403,f10(x26404,x26405)))))),x26405)), % 184.98/184.97 inference(scs_inference,[],[4,2150,1941,2330,2210,53,1662,1693,20,16,14,29,28,31,23])). % 184.98/184.97 cnf(2773,plain, % 184.98/184.97 (P3(f7(x27731,f9(f9(f8(x27732,f8(f13(x27733),x27733))))),f7(x27731,f9(f8(f13(f9(f8(x27734,x27733))),f9(f8(x27734,x27733))))))), % 184.98/184.97 inference(scs_inference,[],[5,2024,1479,401,14,20,31])). % 184.98/184.97 cnf(2921,plain, % 184.98/184.97 (P5(f10(f6(f16(x29211)),f16(x29211)),f16(f10(x29212,f10(f6(f16(f16(f10(x29213,x29211)))),f16(f16(f10(x29213,x29211)))))))), % 184.98/184.97 inference(scs_inference,[],[6,1476,2601,2544,2373,1637,1684,10,134,14,20,16,15,31,27,23])). % 184.98/184.97 cnf(2933,plain, % 184.98/184.97 (P6(f15(x29331,f15(f15(f14(a3),f4(f17(a2))),a1)),f15(x29331,f14(f15(f15(a3,f4(f17(a2))),a1))))), % 184.98/184.97 inference(scs_inference,[],[2335,2921,1662,5,14,20,15,16,30])). % 184.98/184.97 cnf(3063,plain, % 184.98/184.97 (P2(x30631,f9(f9(f8(x30632,f8(x30633,x30631)))))), % 184.98/184.97 inference(scs_inference,[],[9,2144,2379,2933,65,31,27,21])). % 184.98/184.97 cnf(3066,plain, % 184.98/184.97 (P2(f9(x30661),f9(f9(f9(f8(x30662,f8(x30663,x30661))))))), % 184.98/184.97 inference(scs_inference,[],[9,2144,2379,2933,65,31,27,21,14])). % 184.98/184.97 cnf(3068,plain, % 184.98/184.97 (P3(f13(x30681),f13(f9(f9(f8(x30682,f8(x30683,x30681))))))), % 184.98/184.97 inference(scs_inference,[],[9,2144,2379,2933,65,31,27,21,14,20])). % 184.98/184.97 cnf(3077,plain, % 184.98/184.97 (P2(f8(f13(x30771),f9(f8(x30772,x30773))),f8(f13(f9(f9(f8(x30774,f8(x30775,x30771))))),x30773))), % 184.98/184.97 inference(scs_inference,[],[9,3066,3068,1662,14,20,31,27])). % 184.98/184.97 cnf(3095,plain, % 184.98/184.97 (P3(f7(x30951,f9(f8(x30952,x30953))),f7(x30951,x30953))), % 184.98/184.97 inference(scs_inference,[],[9,3077,5,20,31])). % 184.98/184.97 cnf(3097,plain, % 184.98/184.97 (~P3(f7(f15(f15(f14(a3),f4(f17(a2))),a1),f9(f8(x30971,f8(a11,a12)))),f7(f15(f15(a3,f4(f17(a2))),a1),a12))), % 184.98/184.97 inference(scs_inference,[],[9,3077,13,5,20,31,25])). % 184.98/184.97 cnf(3100,plain, % 184.98/184.97 (~P3(f7(f15(f15(f14(a3),f4(f17(a2))),a1),f9(f8(x31001,f9(f8(x31002,f8(a11,a12)))))),f7(f15(f15(a3,f4(f17(a2))),a1),a12))), % 184.98/184.97 inference(scs_inference,[],[3095,3097,25])). % 184.98/184.97 cnf(3101,plain, % 184.98/184.97 (P3(f7(x31011,f9(f8(x31012,x31013))),f7(x31011,x31013))), % 184.98/184.97 inference(rename_variables,[],[3095])). % 184.98/184.97 cnf(3107,plain, % 184.98/184.97 (P2(f9(f9(f8(x31071,f8(x31072,f9(f8(x31073,x31074)))))),x31074)), % 184.98/184.97 inference(scs_inference,[],[9,3095,3101,3063,3097,25,27,20,21])). % 184.98/184.97 cnf(3110,plain, % 184.98/184.97 (P2(f9(f9(f9(f8(x31101,f8(x31102,f9(f8(x31103,x31104))))))),f9(x31104))), % 184.98/184.97 inference(scs_inference,[],[9,3095,3101,3063,3097,25,27,20,21,14])). % 184.98/184.97 cnf(3117,plain, % 184.98/184.97 (~P3(f7(f15(f15(f14(a3),f4(f17(a2))),a1),f9(f9(f8(x31171,f8(f13(f8(a11,a12)),f8(a11,a12)))))),f7(f15(f15(a3,f4(f17(a2))),a1),a12))), % 184.98/184.97 inference(scs_inference,[],[3107,3110,2773,3100,14,20,25])). % 184.98/184.97 cnf(3140,plain, % 184.98/184.97 (~P3(f7(f14(f15(f15(f14(a3),f4(f17(a2))),a1)),f9(f8(x31401,f8(f13(f8(a11,a12)),f8(a11,a12))))),f7(f15(f15(a3,f4(f17(a2))),a1),a12))), % 184.98/184.97 inference(scs_inference,[],[3117,12,25])). % 184.98/184.97 cnf(3172,plain, % 184.98/184.97 (P5(x31721,f16(f16(f10(x31722,f10(x31723,x31721)))))), % 184.98/184.97 inference(scs_inference,[],[10,3140,2640,12,5,28,25,23])). % 184.98/184.97 cnf(3316,plain, % 184.98/184.97 (P2(f9(f9(f8(x33161,f8(x33162,x33163)))),x33163)), % 184.98/184.97 inference(scs_inference,[],[9,2379,21])). % 184.98/184.97 cnf(3325,plain, % 184.98/184.97 (P5(f16(f16(f10(x33251,f10(x33252,x33253)))),x33253)), % 184.98/184.97 inference(scs_inference,[],[10,2640,23])). % 184.98/184.97 cnf(3333,plain, % 184.98/184.97 (P5(f10(x33331,f16(f16(f10(x33332,x33333)))),f10(x33331,f16(x33333)))), % 184.98/184.97 inference(scs_inference,[],[10,3,16,29])). % 184.98/184.97 cnf(3335,plain, % 184.98/184.97 (P6(f4(f14(f15(f15(a3,f4(f17(a2))),a1))),f4(f15(f15(f14(a3),f4(f17(a2))),a1)))), % 184.98/184.97 inference(scs_inference,[],[48,5,24])). % 184.98/184.97 cnf(3354,plain, % 184.98/184.97 (P2(f9(f8(x33541,x33542)),f9(f9(f8(x33543,f8(x33544,x33542)))))), % 184.98/184.97 inference(scs_inference,[],[65,3063,21])). % 184.98/184.97 cnf(3393,plain, % 184.98/184.97 (P5(f16(f10(x33931,x33932)),f16(f16(f10(x33933,f10(x33934,x33932)))))), % 184.98/184.97 inference(scs_inference,[],[78,3172,23])). % 184.98/184.97 cnf(3433,plain, % 184.98/184.97 (P2(f8(f13(f9(x34331)),f9(f9(f8(x34332,f9(f8(x34333,x34334)))))),f8(f13(f9(f9(f8(x34335,x34331)))),f9(x34334)))), % 184.98/184.97 inference(scs_inference,[],[144,2,21])). % 184.98/184.97 cnf(3566,plain, % 184.98/184.97 (P3(f7(f14(f15(f15(a3,f4(f17(a2))),a1)),x35661),f7(f15(f15(f14(a3),f4(f17(a2))),a1),x35661))), % 184.98/184.97 inference(scs_inference,[],[524,6,25])). % 184.98/184.97 cnf(3714,plain, % 184.98/184.97 (P5(f10(f5(f4(a2),x37141),x37142),f10(f6(x37141),x37142))), % 184.98/184.97 inference(scs_inference,[],[4,7,3354,14,29])). % 184.98/184.97 cnf(3716,plain, % 184.98/184.97 (P2(f8(x37161,f9(f8(x37162,x37163))),f8(x37161,x37163))), % 184.98/184.97 inference(scs_inference,[],[6,9,4,7,3354,14,29,27])). % 184.98/184.97 cnf(3722,plain, % 184.98/184.97 (P5(f16(f16(f16(f10(x37221,f10(x37222,x37223))))),f16(x37223))), % 184.98/184.97 inference(scs_inference,[],[6,9,4,7,3354,3325,14,29,27,20,15,16])). % 184.98/184.97 cnf(3730,plain, % 184.98/184.97 (P2(f9(f9(f9(f8(x37301,f8(x37302,x37303))))),f9(x37303))), % 184.98/184.97 inference(scs_inference,[],[3316,14])). % 184.98/184.97 cnf(3732,plain, % 184.98/184.97 (P5(f10(x37321,f16(f10(x37322,x37323))),f10(x37321,x37323))), % 184.98/184.97 inference(scs_inference,[],[3,10,3316,14,29])). % 184.98/184.97 cnf(3738,plain, % 184.98/184.97 (P3(f13(f8(x37381,f9(f8(x37382,x37383)))),f13(f8(x37381,x37383)))), % 184.98/184.97 inference(scs_inference,[],[3,2,10,8,3716,3722,3316,14,29,27,15,20])). % 184.98/184.97 cnf(3747,plain, % 184.98/184.97 (P2(f9(f9(f9(f9(f8(x37471,f8(x37472,x37473)))))),f9(f9(x37473)))), % 184.98/184.97 inference(scs_inference,[],[4,11,3730,29,14])). % 184.98/184.97 cnf(3751,plain, % 184.98/184.97 (P3(f13(f9(f9(f9(f8(x37511,f8(x37512,x37513)))))),f13(f9(x37513)))), % 184.98/184.97 inference(scs_inference,[],[6,4,11,3730,29,14,27,20])). % 184.98/184.97 cnf(3753,plain, % 184.98/184.97 (P4(f6(f10(x37531,f16(f10(x37532,x37533)))),f6(f10(x37531,x37533)))), % 184.98/184.97 inference(scs_inference,[],[6,4,11,3732,3730,29,14,27,20,15])). % 184.98/184.97 cnf(3757,plain, % 184.98/184.97 (P4(f5(x37571,f10(x37572,f16(f10(x37573,x37574)))),f5(x37571,f10(x37572,x37574)))), % 184.98/184.97 inference(scs_inference,[],[6,4,11,5,3732,3730,3393,29,14,27,20,15,16,28])). % 184.98/184.97 cnf(3792,plain, % 184.98/184.97 (P3(f13(f9(f9(f8(x37921,f8(x37922,x37923))))),f13(x37923))), % 184.98/184.97 inference(scs_inference,[],[3,2,3738,3714,3316,3393,29,27,15,16,20])). % 184.98/184.97 cnf(3794,plain, % 184.98/184.97 (P5(f10(f5(x37941,f10(x37942,f16(f10(x37943,x37944)))),x37945),f10(f5(x37941,f10(x37942,x37944)),x37945))), % 184.98/184.97 inference(scs_inference,[],[4,3757,29])). % 184.98/184.97 cnf(3796,plain, % 184.98/184.97 (P2(f8(x37961,f8(x37962,f9(f8(x37963,x37964)))),f8(x37961,f8(x37962,x37964)))), % 184.98/184.97 inference(scs_inference,[],[6,4,3757,3716,29,27])). % 184.98/184.97 cnf(3806,plain, % 184.98/184.97 (P5(f10(x38061,f10(x38062,f16(f10(x38063,x38064)))),f10(x38061,f10(x38062,x38064)))), % 184.98/184.97 inference(scs_inference,[],[3,3732,29])). % 184.98/184.97 cnf(3808,plain, % 184.98/184.97 (P2(f8(f13(f9(f9(f8(x38081,f8(x38082,x38083))))),x38084),f8(f13(x38083),x38084))), % 184.98/184.97 inference(scs_inference,[],[3,2,3792,3732,29,27])). % 184.98/184.97 cnf(3810,plain, % 184.98/184.97 (P4(f6(f10(x38101,f16(f16(f10(x38102,x38103))))),f6(f10(x38101,f16(x38103))))), % 184.98/184.97 inference(scs_inference,[],[3,2,3792,3732,3333,29,27,15])). % 184.98/184.97 cnf(3814,plain, % 184.98/184.97 (P5(f10(f6(f10(x38141,f16(f10(x38142,x38143)))),x38144),f10(f6(f10(x38141,x38143)),x38144))), % 184.98/184.97 inference(scs_inference,[],[4,3753,29])). % 184.98/184.97 cnf(3816,plain, % 184.98/184.97 (P2(f8(x38161,f8(x38162,f8(x38163,f9(f8(x38164,x38165))))),f8(x38161,f8(x38162,f8(x38163,x38165))))), % 184.98/184.97 inference(scs_inference,[],[6,4,3796,3753,29,27])). % 184.98/184.97 cnf(3822,plain, % 184.98/184.97 (P5(f10(x38221,f10(x38222,f10(x38223,f16(f10(x38224,x38225))))),f10(x38221,f10(x38222,f10(x38223,x38225))))), % 184.98/184.97 inference(scs_inference,[],[3,3806,29])). % 184.98/184.97 cnf(3880,plain, % 184.98/184.97 (P5(f16(f10(x38801,f10(x38802,f10(x38803,f16(f10(x38804,x38805)))))),f16(f10(x38801,f10(x38802,f10(x38803,x38805)))))), % 184.98/184.97 inference(scs_inference,[],[3,9,8,5,3808,3433,3794,3822,3335,14,29,27,28,15,31,20,16])). % 184.98/184.97 cnf(3882,plain, % 184.98/184.97 (P2(f9(f9(f9(f9(f9(f8(x38821,f8(x38822,x38823))))))),f9(f9(f9(x38823))))), % 184.98/184.97 inference(scs_inference,[],[3747,14])). % 184.98/184.97 cnf(3884,plain, % 184.98/184.97 (P2(f8(x38841,f9(f9(f9(f9(f8(x38842,f8(x38843,x38844))))))),f8(x38841,f9(f9(x38844))))), % 184.98/184.97 inference(scs_inference,[],[6,3747,14,27])). % 184.98/184.97 cnf(3901,plain, % 184.98/184.97 (P2(f8(f13(f9(f9(f9(f8(x39011,f8(x39012,x39013)))))),x39014),f8(f13(f9(x39013)),x39014))), % 184.98/184.97 inference(scs_inference,[],[2,3751,3816,14,27])). % 184.98/184.97 cnf(3903,plain, % 184.98/184.97 (P5(f10(x39031,f10(f6(f10(x39032,f16(f10(x39033,x39034)))),x39035)),f10(x39031,f10(f6(f10(x39032,x39034)),x39035)))), % 184.98/184.97 inference(scs_inference,[],[3,2,3751,3816,3814,14,27,29])). % 184.98/184.97 cnf(3971,plain, % 184.98/184.97 (P2(f8(f7(f14(x39711),x39712),f9(f8(x39713,x39714))),f8(f7(x39711,f9(x39712)),x39714))), % 184.98/184.97 inference(scs_inference,[],[3,9,12,3884,3880,29,14,27])). % 184.98/184.97 cnf(3999,plain, % 184.98/184.97 (~P3(f7(f14(f15(f15(a3,f4(f17(a2))),a1)),f8(a11,a12)),f7(f15(f15(a3,f4(f17(a2))),a1),a12))), % 184.98/184.97 inference(scs_inference,[],[6,4,13,5,3971,3810,3901,3882,3903,3566,29,14,27,28,31,20,15,16,25])). % 184.98/184.97 cnf(4069,plain, % 184.98/184.97 ($false), % 184.98/184.97 inference(scs_inference,[],[3999,3095,40,25]), % 184.98/184.97 ['proof']). % 184.98/184.97 % SZS output end Proof % 184.98/184.97 % Total time :184.230000s %------------------------------------------------------------------------------