%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN647-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:12 EDT 2024 % Result : Unsatisfiable 182.15s 182.20s % Output : CNFRefutation 182.27s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.08 % Problem : SYN647-1 : TPTP v8.2.0. Released v2.5.0. % 0.04/0.08 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.07/0.27 % Computer : n017.cluster.edu % 0.07/0.27 % Model : x86_64 x86_64 % 0.07/0.27 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.27 % Memory : 8042.1875MB % 0.07/0.27 % OS : Linux 3.10.0-693.el7.x86_64 % 0.07/0.27 % CPULimit : 300 % 0.07/0.27 % WCLimit : 300 % 0.07/0.27 % DateTime : Sun Jun 23 20:55:39 EDT 2024 % 0.07/0.27 % CPUTime : % 0.12/0.47 start to proof:theBenchmark % 182.15/182.17 %------------------------------------------- % 182.15/182.17 % File :CSE---1.7 % 182.15/182.17 % Problem :theBenchmark % 182.15/182.17 % Transform :cnf % 182.15/182.17 % Format :tptp:raw % 182.15/182.17 % Command :java -jar mcs_scs.jar %d %s % 182.15/182.17 % 182.15/182.17 % Result :Theorem 181.670000s % 182.15/182.17 % Output :CNFRefutation 181.670000s % 182.15/182.17 %------------------------------------------- % 182.15/182.19 %-------------------------------------------------------------------------- % 182.15/182.19 % File : SYN647-1 : TPTP v8.2.0. Released v2.5.0. % 182.15/182.19 % Domain : Syntactic % 182.15/182.19 % Problem : Harrison problem 4392 % 182.15/182.19 % Version : Especial. % 182.15/182.19 % English : % 182.15/182.19 % 182.15/182.19 % Refs : [Har01] Email to G. Sutcliffe % 182.15/182.19 % Source : [Har01] % 182.15/182.19 % Names : % 182.15/182.19 % 182.15/182.19 % Status : Unsatisfiable % 182.15/182.20 % Rating : 0.18 v8.2.0, 0.29 v8.1.0, 0.50 v6.1.0, 0.43 v6.0.0, 0.33 v5.5.0, 0.44 v5.4.0, 0.50 v5.3.0, 0.55 v5.2.0, 0.46 v5.1.0, 0.44 v5.0.0, 0.33 v4.1.0, 0.40 v4.0.1, 0.43 v3.7.0, 0.29 v3.4.0, 0.40 v3.3.0, 0.33 v3.1.0, 0.17 v2.7.0, 0.38 v2.6.0, 0.17 v2.5.0 % 182.15/182.20 % Syntax : Number of clauses : 44 ( 22 unt; 0 nHn; 39 RR) % 182.15/182.20 % Number of literals : 85 ( 0 equ; 43 neg) % 182.15/182.20 % Maximal clause size : 5 ( 1 avg) % 182.15/182.20 % Maximal term depth : 27 ( 6 avg) % 182.15/182.20 % Number of predicates : 9 ( 9 usr; 0 prp; 1-2 aty) % 182.15/182.20 % Number of functors : 15 ( 15 usr; 4 con; 0-2 aty) % 182.15/182.20 % Number of variables : 64 ( 0 sgn) % 182.15/182.20 % SPC : CNF_UNS_RFO_NEQ_HRN % 182.15/182.20 % 182.15/182.20 % Comments : % 182.15/182.20 %-------------------------------------------------------------------------- % 182.15/182.20 cnf(c22_is_p18_1,negated_conjecture, % 182.15/182.20 p18(c22) ). % 182.15/182.20 % 182.15/182.20 cnf(p10_2,negated_conjecture, % 182.15/182.20 p10(X0,X0) ). % 182.15/182.20 % 182.15/182.20 cnf(p4_3,negated_conjecture, % 182.15/182.20 p4(X48,X48) ). % 182.15/182.20 % 182.15/182.20 cnf(p3_4,negated_conjecture, % 182.15/182.20 p3(X41,X41) ). % 182.15/182.20 % 182.15/182.20 cnf(p2_5,negated_conjecture, % 182.15/182.20 p2(X16,X16) ). % 182.15/182.20 % 182.15/182.20 cnf(p16_6,negated_conjecture, % 182.15/182.20 p16(X5,X5) ). % 182.15/182.20 % 182.15/182.20 cnf(not_p21_7,negated_conjecture, % 182.15/182.20 ~ p21(f17(c25),f17(c22)) ). % 182.15/182.20 % 182.15/182.20 cnf(not_p21_8,negated_conjecture, % 182.15/182.20 ~ p21(f17(c22),f17(c23)) ). % 182.15/182.20 % 182.15/182.20 cnf(p2_9,negated_conjecture, % 182.15/182.20 p2(f12(f11(c22)),f7(c24)) ). % 182.15/182.20 % 182.15/182.20 cnf(p2_10,negated_conjecture, % 182.15/182.20 p2(f12(f11(c25)),f7(c24)) ). % 182.15/182.20 % 182.15/182.20 cnf(p2_11,negated_conjecture, % 182.15/182.20 p2(f12(f11(c23)),f7(c24)) ). % 182.15/182.20 % 182.15/182.20 cnf(p20_12,negated_conjecture, % 182.15/182.20 p20(f14(f11(c25)),f14(f11(c22))) ). % 182.15/182.20 % 182.15/182.20 cnf(p19_13,negated_conjecture, % 182.15/182.20 p19(f14(f11(c23)),f14(f11(c22))) ). % 182.15/182.20 % 182.15/182.20 cnf(p2_14,negated_conjecture, % 182.15/182.20 p2(f13(f11(c23)),f13(f11(c22))) ). % 182.15/182.20 % 182.15/182.20 cnf(p18_15,negated_conjecture, % 182.15/182.20 ( p18(X10) % 182.15/182.20 | ~ p18(X11) % 182.15/182.20 | ~ p10(X11,X10) ) ). % 182.15/182.20 % 182.15/182.20 cnf(p4_16,negated_conjecture, % 182.15/182.20 ( p4(f11(X51),f11(X52)) % 182.15/182.20 | ~ p10(X51,X52) ) ). % 182.15/182.20 % 182.15/182.20 cnf(p10_17,negated_conjecture, % 182.15/182.20 ( p10(f15(X3),f15(X4)) % 182.15/182.20 | ~ p4(X3,X4) ) ). % 182.15/182.20 % 182.15/182.20 cnf(p16_18,negated_conjecture, % 182.15/182.20 ( p16(f17(X8),f17(X9)) % 182.15/182.20 | ~ p10(X8,X9) ) ). % 182.15/182.20 % 182.15/182.20 cnf(p2_19,negated_conjecture, % 182.15/182.20 ( p2(f12(X19),f12(X20)) % 182.15/182.20 | ~ p4(X19,X20) ) ). % 182.15/182.20 % 182.15/182.20 cnf(p2_20,negated_conjecture, % 182.15/182.20 ( p2(f13(X21),f13(X22)) % 182.15/182.20 | ~ p4(X21,X22) ) ). % 182.15/182.20 % 182.15/182.20 cnf(p2_21,negated_conjecture, % 182.15/182.20 ( p2(f14(X23),f14(X24)) % 182.15/182.20 | ~ p4(X23,X24) ) ). % 182.15/182.20 % 182.15/182.20 cnf(p2_22,negated_conjecture, % 182.15/182.20 ( p2(f7(X25),f7(X26)) % 182.15/182.20 | ~ p2(X25,X26) ) ). % 182.15/182.20 % 182.15/182.20 cnf(p2_23,negated_conjecture, % 182.15/182.20 ( p2(f8(X27),f8(X28)) % 182.15/182.20 | ~ p2(X27,X28) ) ). % 182.15/182.20 % 182.15/182.20 cnf(p2_24,negated_conjecture, % 182.15/182.20 ( p2(f9(X29),f9(X30)) % 182.15/182.20 | ~ p2(X29,X30) ) ). % 182.15/182.20 % 182.15/182.20 cnf(p10_25,negated_conjecture, % 182.15/182.20 ( p10(X1,X2) % 182.15/182.20 | ~ p10(X0,X1) % 182.15/182.20 | ~ p10(X0,X2) ) ). % 182.15/182.20 % 182.15/182.20 cnf(p4_26,negated_conjecture, % 182.15/182.20 ( p4(X49,X50) % 182.15/182.20 | ~ p4(X48,X49) % 182.15/182.20 | ~ p4(X48,X50) ) ). % 182.15/182.20 % 182.15/182.20 cnf(p3_27,negated_conjecture, % 182.15/182.20 ( p3(X42,X43) % 182.15/182.20 | ~ p3(X41,X42) % 182.15/182.20 | ~ p3(X41,X43) ) ). % 182.15/182.20 % 182.15/182.20 cnf(p2_28,negated_conjecture, % 182.15/182.20 ( p2(X17,X18) % 182.15/182.20 | ~ p2(X16,X17) % 182.15/182.20 | ~ p2(X16,X18) ) ). % 182.15/182.20 % 182.15/182.20 cnf(p16_29,negated_conjecture, % 182.15/182.20 ( p16(X6,X7) % 182.15/182.20 | ~ p16(X5,X6) % 182.15/182.20 | ~ p16(X5,X7) ) ). % 182.15/182.20 % 182.15/182.20 cnf(p19_30,negated_conjecture, % 182.15/182.20 ( p19(X12,X13) % 182.15/182.20 | ~ p2(X14,X12) % 182.15/182.20 | ~ p2(X15,X13) % 182.15/182.20 | ~ p19(X14,X15) ) ). % 182.15/182.20 % 182.15/182.20 cnf(p21_31,negated_conjecture, % 182.15/182.20 ( p21(X35,X36) % 182.15/182.20 | ~ p16(X38,X36) % 182.15/182.20 | ~ p21(X37,X38) % 182.15/182.20 | ~ p16(X37,X35) ) ). % 182.15/182.20 % 182.15/182.20 cnf(p20_32,negated_conjecture, % 182.15/182.20 ( p20(X31,X32) % 182.15/182.20 | ~ p2(X34,X32) % 182.15/182.20 | ~ p20(X33,X34) % 182.15/182.20 | ~ p2(X33,X31) ) ). % 182.15/182.20 % 182.15/182.20 cnf(p4_33,negated_conjecture, % 182.15/182.20 ( p4(f5(X53,X54),f5(X55,X56)) % 182.15/182.20 | ~ p2(X53,X55) % 182.15/182.20 | ~ p3(X54,X56) ) ). % 182.15/182.20 % 182.15/182.20 cnf(p3_34,negated_conjecture, % 182.15/182.20 ( p3(f6(X44,X45),f6(X46,X47)) % 182.15/182.20 | ~ p2(X44,X46) % 182.15/182.20 | ~ p2(X45,X47) ) ). % 182.15/182.20 % 182.15/182.20 cnf(p2_35,negated_conjecture, % 182.15/182.20 p2(f13(f11(c23)),f7(f8(f9(f8(f9(f9(f9(f9(f8(c24)))))))))) ). % 182.15/182.20 % 182.15/182.20 cnf(p2_36,negated_conjecture, % 182.15/182.20 p2(f13(f11(c25)),f7(f8(f9(f8(f9(f9(f9(f9(f8(c24)))))))))) ). % 182.15/182.20 % 182.15/182.20 cnf(p21_37,negated_conjecture, % 182.15/182.20 ( p21(f17(X39),f17(X40)) % 182.15/182.20 | ~ p2(f12(f11(X40)),f7(c24)) % 182.15/182.20 | ~ p2(f12(f11(X39)),f7(c24)) % 182.15/182.20 | ~ p19(f13(f11(X39)),f13(f11(X40))) ) ). % 182.15/182.20 % 182.15/182.20 cnf(p2_38,negated_conjecture, % 182.15/182.20 p2(f14(f11(c23)),f7(f8(f8(f8(f9(f8(f9(f9(f9(f9(f8(f9(f9(f8(f8(f8(f9(f8(f9(f9(f9(f8(f8(c24)))))))))))))))))))))))) ). % 182.15/182.20 % 182.15/182.20 cnf(p2_39,negated_conjecture, % 182.15/182.20 p2(f14(f11(c25)),f7(f9(f9(f9(f8(f8(f9(f9(f9(f9(f8(f9(f9(f8(f8(f8(f9(f8(f9(f9(f9(f8(f8(c24)))))))))))))))))))))))) ). % 182.15/182.20 % 182.15/182.20 cnf(p21_40,negated_conjecture, % 182.15/182.20 ( p21(f17(X39),f17(X40)) % 182.15/182.20 | ~ p2(f12(f11(X39)),f7(c24)) % 182.15/182.20 | ~ p2(f12(f11(X40)),f7(c24)) % 182.15/182.20 | ~ p2(f13(f11(X39)),f13(f11(X40))) % 182.15/182.20 | ~ p20(f14(f11(X39)),f14(f11(X40))) ) ). % 182.15/182.20 % 182.15/182.20 cnf(p4_41,negated_conjecture, % 182.15/182.20 p4(f11(c25),f5(f7(c24),f6(f7(f8(f9(f8(f9(f9(f9(f9(f8(c24))))))))),f7(f9(f9(f9(f8(f8(f9(f9(f9(f9(f8(f9(f9(f8(f8(f8(f9(f8(f9(f9(f9(f8(f8(c24)))))))))))))))))))))))))) ). % 182.15/182.20 % 182.15/182.20 cnf(p4_42,negated_conjecture, % 182.15/182.20 p4(f11(c23),f5(f7(c24),f6(f7(f8(f9(f8(f9(f9(f9(f9(f8(c24))))))))),f7(f8(f8(f8(f9(f8(f9(f9(f9(f9(f8(f9(f9(f8(f8(f8(f9(f8(f9(f9(f9(f8(f8(c24)))))))))))))))))))))))))) ). % 182.15/182.20 % 182.15/182.20 cnf(p10_43,negated_conjecture, % 182.15/182.20 p10(f15(f5(f7(c24),f6(f7(f8(f9(f8(f9(f9(f9(f9(f8(c24))))))))),f7(f8(f8(f8(f9(f8(f9(f9(f9(f9(f8(f9(f9(f8(f8(f8(f9(f8(f9(f9(f9(f8(f8(c24)))))))))))))))))))))))))),c23) ). % 182.15/182.20 % 182.15/182.20 cnf(p10_44,negated_conjecture, % 182.15/182.20 p10(f15(f5(f7(c24),f6(f7(f8(f9(f8(f9(f9(f9(f9(f8(c24))))))))),f7(f9(f9(f9(f8(f8(f9(f9(f9(f9(f8(f9(f9(f8(f8(f8(f9(f8(f9(f9(f9(f8(f8(c24)))))))))))))))))))))))))),c25) ). % 182.15/182.20 % 182.15/182.20 %-------------------------------------------------------------------------- % 182.15/182.20 %------------------------------------------- % 182.15/182.20 % Proof found % 182.15/182.20 % SZS status Theorem for theBenchmark % 182.15/182.20 % SZS output start Proof % 182.15/182.21 %ClaNum:44(EqnAxiom:0) % 182.15/182.21 %VarNum:134(SingletonVarNum:64) % 182.15/182.21 %MaxLitNum:5 % 182.15/182.21 %MaxfuncDepth:26 % 182.15/182.21 %SharedTerms:78 % 182.15/182.21 %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 % 182.15/182.21 %singleGoalClaCount:22 % 182.15/182.21 [1]P1(a1) % 182.15/182.21 [21]~P9(f13(a1),f13(a4)) % 182.15/182.21 [22]~P9(f13(a5),f13(a1)) % 182.15/182.21 [7]P6(f6(f2(a1)),f7(a3)) % 182.15/182.21 [8]P6(f6(f2(a5)),f7(a3)) % 182.15/182.21 [9]P6(f6(f2(a4)),f7(a3)) % 182.15/182.21 [10]P6(f8(f2(a4)),f8(f2(a1))) % 182.15/182.21 [11]P8(f9(f2(a5)),f9(f2(a1))) % 182.15/182.21 [12]P7(f9(f2(a4)),f9(f2(a1))) % 182.15/182.21 [13]P6(f8(f2(a5)),f7(f14(f15(f14(f15(f15(f15(f15(f14(a3)))))))))) % 182.15/182.21 [14]P6(f8(f2(a4)),f7(f14(f15(f14(f15(f15(f15(f15(f14(a3)))))))))) % 182.15/182.21 [15]P6(f9(f2(a5)),f7(f15(f15(f15(f14(f14(f15(f15(f15(f15(f14(f15(f15(f14(f14(f14(f15(f14(f15(f15(f15(f14(f14(a3)))))))))))))))))))))))) % 182.15/182.21 [16]P6(f9(f2(a4)),f7(f14(f14(f14(f15(f14(f15(f15(f15(f15(f14(f15(f15(f14(f14(f14(f15(f14(f15(f15(f15(f14(f14(a3)))))))))))))))))))))))) % 182.15/182.21 [17]P4(f2(a5),f11(f7(a3),f10(f7(f14(f15(f14(f15(f15(f15(f15(f14(a3))))))))),f7(f15(f15(f15(f14(f14(f15(f15(f15(f15(f14(f15(f15(f14(f14(f14(f15(f14(f15(f15(f15(f14(f14(a3)))))))))))))))))))))))))) % 182.15/182.21 [18]P4(f2(a4),f11(f7(a3),f10(f7(f14(f15(f14(f15(f15(f15(f15(f14(a3))))))))),f7(f14(f14(f14(f15(f14(f15(f15(f15(f15(f14(f15(f15(f14(f14(f14(f15(f14(f15(f15(f15(f14(f14(a3)))))))))))))))))))))))))) % 182.15/182.21 [19]P2(f12(f11(f7(a3),f10(f7(f14(f15(f14(f15(f15(f15(f15(f14(a3))))))))),f7(f14(f14(f14(f15(f14(f15(f15(f15(f15(f14(f15(f15(f14(f14(f14(f15(f14(f15(f15(f15(f14(f14(a3)))))))))))))))))))))))))),a4) % 182.15/182.21 [20]P2(f12(f11(f7(a3),f10(f7(f14(f15(f14(f15(f15(f15(f15(f14(a3))))))))),f7(f15(f15(f15(f14(f14(f15(f15(f15(f15(f14(f15(f15(f14(f14(f14(f15(f14(f15(f15(f15(f14(f14(a3)))))))))))))))))))))))))),a5) % 182.15/182.21 [2]P2(x21,x21) % 182.15/182.21 [3]P4(x31,x31) % 182.15/182.21 [4]P5(x41,x41) % 182.15/182.21 [5]P6(x51,x51) % 182.15/182.21 [6]P3(x61,x61) % 182.15/182.21 [24]~P4(x241,x242)+P2(f12(x241),f12(x242)) % 182.15/182.21 [25]~P2(x251,x252)+P4(f2(x251),f2(x252)) % 182.15/182.21 [26]~P4(x261,x262)+P6(f6(x261),f6(x262)) % 182.15/182.21 [27]~P6(x271,x272)+P6(f7(x271),f7(x272)) % 182.15/182.21 [28]~P4(x281,x282)+P6(f9(x281),f9(x282)) % 182.15/182.21 [29]~P4(x291,x292)+P6(f8(x291),f8(x292)) % 182.15/182.21 [30]~P6(x301,x302)+P6(f14(x301),f14(x302)) % 182.15/182.21 [31]~P6(x311,x312)+P6(f15(x311),f15(x312)) % 182.15/182.21 [32]~P2(x321,x322)+P3(f13(x321),f13(x322)) % 182.15/182.21 [23]~P2(x232,x231)+P1(x231)+~P1(x232) % 182.15/182.21 [33]~P2(x333,x331)+P2(x331,x332)+~P2(x333,x332) % 182.15/182.21 [34]~P4(x343,x341)+P4(x341,x342)+~P4(x343,x342) % 182.15/182.21 [35]~P5(x353,x351)+P5(x351,x352)+~P5(x353,x352) % 182.15/182.21 [36]~P6(x363,x361)+P6(x361,x362)+~P6(x363,x362) % 182.15/182.21 [37]~P3(x373,x371)+P3(x371,x372)+~P3(x373,x372) % 182.15/182.21 [41]~P5(x412,x414)+~P6(x411,x413)+P4(f11(x411,x412),f11(x413,x414)) % 182.15/182.21 [42]~P6(x422,x424)+~P6(x421,x423)+P5(f10(x421,x422),f10(x423,x424)) % 182.15/182.21 [43]P9(f13(x431),f13(x432))+~P7(f8(f2(x431)),f8(f2(x432)))+~P6(f6(f2(x432)),f7(a3))+~P6(f6(f2(x431)),f7(a3)) % 182.15/182.21 [38]~P9(x383,x384)+P9(x381,x382)+~P3(x383,x381)+~P3(x384,x382) % 182.15/182.21 [39]~P8(x393,x394)+P8(x391,x392)+~P6(x393,x391)+~P6(x394,x392) % 182.15/182.21 [40]~P7(x404,x403)+P7(x401,x402)+~P6(x403,x402)+~P6(x404,x401) % 182.15/182.21 [44]P9(f13(x441),f13(x442))+~P6(f8(f2(x441)),f8(f2(x442)))+~P8(f9(f2(x441)),f9(f2(x442)))+~P6(f6(f2(x442)),f7(a3))+~P6(f6(f2(x441)),f7(a3)) % 182.15/182.21 %EqnAxiom % 182.15/182.21 % 182.15/182.21 %------------------------------------------- % 182.15/182.23 cnf(54,plain, % 182.15/182.23 (P6(f7(a3),f6(f2(a5)))), % 182.15/182.23 inference(scs_inference,[],[8,5,36])). % 182.15/182.23 cnf(106,plain, % 182.15/182.23 (P2(f12(f11(f7(a3),x1061)),f12(f11(f6(f2(a5)),x1061)))), % 182.15/182.23 inference(scs_inference,[],[4,54,24,41])). % 182.15/182.23 cnf(112,plain, % 182.15/182.23 (P2(f12(f11(f6(f2(a5)),x1121)),f12(f11(f7(a3),x1121)))), % 182.15/182.23 inference(scs_inference,[],[106,2,33])). % 182.15/182.23 cnf(153,plain, % 182.15/182.23 (P6(f7(a3),f6(f2(a1)))), % 182.15/182.23 inference(scs_inference,[],[7,5,36])). % 182.15/182.23 cnf(188,plain, % 182.15/182.23 (P6(f7(a3),f6(f2(a4)))), % 182.15/182.23 inference(scs_inference,[],[9,5,36])). % 182.15/182.23 cnf(217,plain, % 182.15/182.23 (P6(f8(f2(a1)),f8(f2(a4)))), % 182.15/182.23 inference(scs_inference,[],[10,5,36])). % 182.15/182.23 cnf(238,plain, % 182.15/182.23 (P6(f7(f14(f15(f14(f15(f15(f15(f15(f14(a3))))))))),f8(f2(a5)))), % 182.15/182.23 inference(scs_inference,[],[13,5,36])). % 182.15/182.23 cnf(971,plain, % 182.15/182.23 (P2(f12(f2(f12(f11(f7(a3),x9711)))),f12(f2(f12(f11(f6(f2(a5)),x9711)))))), % 182.15/182.23 inference(scs_inference,[],[106,24,25])). % 182.15/182.23 cnf(1014,plain, % 182.15/182.23 (P2(f12(f2(f12(f11(f6(f2(a5)),x10141)))),f12(f2(f12(f11(f7(a3),x10141)))))), % 182.15/182.23 inference(scs_inference,[],[971,2,33])). % 182.15/182.23 cnf(1661,plain, % 182.15/182.23 (P6(f14(f7(f7(a3))),f14(f7(f6(f2(a4)))))), % 182.15/182.23 inference(scs_inference,[],[188,30,27])). % 182.15/182.23 cnf(1878,plain, % 182.15/182.23 (P6(f14(f7(f6(f2(a4)))),f14(f7(f7(a3))))), % 182.15/182.23 inference(scs_inference,[],[1661,5,36])). % 182.15/182.23 cnf(1992,plain, % 182.15/182.23 (P6(f7(f14(f7(f6(f2(a4))))),f7(f14(f7(f7(a3)))))), % 182.15/182.23 inference(scs_inference,[],[1014,1878,25,27])). % 182.15/182.23 cnf(1996,plain, % 182.15/182.23 (P6(f15(f14(f7(f6(f2(a4))))),f15(f14(f7(f7(a3)))))), % 182.15/182.23 inference(scs_inference,[],[1014,1878,25,27,30,31])). % 182.15/182.23 cnf(2000,plain, % 182.15/182.23 (P5(f10(f14(f7(f6(f2(a4)))),f14(f7(f6(f2(a4))))),f10(f14(f7(f7(a3))),f14(f7(f7(a3)))))), % 182.15/182.23 inference(scs_inference,[],[1014,1878,25,27,30,31,32,42])). % 182.15/182.23 cnf(2032,plain, % 182.15/182.23 (~P6(f8(f2(a5)),f8(f2(a1)))), % 182.15/182.23 inference(scs_inference,[],[1992,2000,112,22,11,8,6,7,27,32,25,30,31,41,42,38,44])). % 182.15/182.23 cnf(2179,plain, % 182.15/182.23 (P6(f14(f15(f14(f7(f6(f2(a4)))))),f14(f15(f14(f7(f7(a3))))))), % 182.15/182.23 inference(scs_inference,[],[1996,30])). % 182.15/182.23 cnf(2181,plain, % 182.15/182.23 (P6(f15(f15(f14(f7(f6(f2(a4)))))),f15(f15(f14(f7(f7(a3))))))), % 182.15/182.23 inference(scs_inference,[],[1996,30,31])). % 182.15/182.23 cnf(2185,plain, % 182.15/182.23 (P5(f10(f7(a3),f7(a3)),f10(f6(f2(a1)),f6(f2(a1))))), % 182.27/182.23 inference(scs_inference,[],[1996,153,30,31,27,42])). % 182.27/182.23 cnf(2195,plain, % 182.27/182.23 (P4(f11(f14(f15(f14(f7(f6(f2(a4)))))),f10(f7(a3),f7(a3))),f11(f14(f15(f14(f7(f7(a3))))),f10(f6(f2(a1)),f6(f2(a1)))))), % 182.27/182.23 inference(scs_inference,[],[2185,2179,30,31,27,41])). % 182.27/182.23 cnf(2197,plain, % 182.27/182.23 (P5(f10(f7(a3),f7(a3)),f10(f6(f2(a5)),f6(f2(a5))))), % 182.27/182.23 inference(scs_inference,[],[2185,2179,54,30,31,27,41,42])). % 182.27/182.23 cnf(2202,plain, % 182.27/182.23 (P6(f6(f11(f14(f15(f14(f7(f6(f2(a4)))))),f10(f7(a3),f7(a3)))),f6(f11(f14(f15(f14(f7(f7(a3))))),f10(f6(f2(a1)),f6(f2(a1))))))), % 182.27/182.23 inference(scs_inference,[],[2195,26])). % 182.27/182.23 cnf(2218,plain, % 182.27/182.23 (P4(f11(f15(f15(f14(f7(f6(f2(a4)))))),f10(f7(a3),f7(a3))),f11(f15(f15(f14(f7(f7(a3))))),f10(f6(f2(a5)),f6(f2(a5)))))), % 182.27/182.23 inference(scs_inference,[],[2197,2181,2195,26,24,25,28,29,30,31,27,41])). % 182.27/182.23 cnf(2220,plain, % 182.27/182.23 (P5(f10(f8(f2(a1)),f8(f2(a1))),f10(f8(f2(a4)),f8(f2(a4))))), % 182.27/182.23 inference(scs_inference,[],[2197,2181,2195,217,26,24,25,28,29,30,31,27,41,42])). % 182.27/182.23 cnf(2229,plain, % 182.27/182.23 (P6(f6(f11(f15(f15(f14(f7(f6(f2(a4)))))),f10(f7(a3),f7(a3)))),f6(f11(f15(f15(f14(f7(f7(a3))))),f10(f6(f2(a5)),f6(f2(a5))))))), % 182.27/182.23 inference(scs_inference,[],[2218,24,26])). % 182.27/182.23 cnf(2231,plain, % 182.27/182.23 (P6(f8(f11(f15(f15(f14(f7(f6(f2(a4)))))),f10(f7(a3),f7(a3)))),f8(f11(f15(f15(f14(f7(f7(a3))))),f10(f6(f2(a5)),f6(f2(a5))))))), % 182.27/182.23 inference(scs_inference,[],[2218,24,26,29])). % 182.27/182.23 cnf(2247,plain, % 182.27/182.23 (P4(f11(f6(f11(f14(f15(f14(f7(f6(f2(a4)))))),f10(f7(a3),f7(a3)))),f10(f8(f2(a1)),f8(f2(a1)))),f11(f6(f11(f14(f15(f14(f7(f7(a3))))),f10(f6(f2(a1)),f6(f2(a1))))),f10(f8(f2(a4)),f8(f2(a4)))))), % 182.27/182.23 inference(scs_inference,[],[2220,2218,2202,8,24,26,29,25,28,30,31,27,42,32,41])). % 182.27/182.23 cnf(2270,plain, % 182.27/182.23 (P5(f10(f8(f2(a4)),f8(f2(a4))),f10(f8(f2(a1)),f8(f2(a1))))), % 182.27/182.23 inference(scs_inference,[],[2229,2247,10,26,24,32,28,29,25,30,31,27,42])). % 182.27/182.23 cnf(2278,plain, % 182.27/182.23 (P5(f10(f6(f2(a4)),f6(f2(a4))),f10(f7(a3),f7(a3)))), % 182.27/182.23 inference(scs_inference,[],[2231,9,30,31,27,42])). % 182.27/182.23 cnf(3949,plain, % 182.27/182.24 (P6(f15(f6(f2(a1))),f15(f7(a3)))), % 182.27/182.24 inference(scs_inference,[],[7,31])). % 182.27/182.24 cnf(3951,plain, % 182.27/182.24 (P6(f14(f6(f2(a1))),f14(f7(a3)))), % 182.27/182.24 inference(scs_inference,[],[7,31,30])). % 182.27/182.24 cnf(3953,plain, % 182.27/182.24 (P6(f7(f6(f2(a1))),f7(f7(a3)))), % 182.27/182.24 inference(scs_inference,[],[7,31,30,27])). % 182.27/182.24 cnf(3955,plain, % 182.27/182.24 (P5(f10(x39551,f6(f2(a1))),f10(x39551,f7(a3)))), % 182.27/182.24 inference(scs_inference,[],[7,5,31,30,27,42])). % 182.27/182.24 cnf(3967,plain, % 182.27/182.24 (P4(f2(f12(f11(f6(f2(a1)),f10(f6(f2(a4)),f6(f2(a4)))))),f2(f12(f11(f7(a3),f10(f7(a3),f7(a3))))))), % 182.27/182.24 inference(scs_inference,[],[7,2278,5,31,30,27,42,41,28,29,26,24,25])). % 182.27/182.24 cnf(3987,plain, % 182.27/182.24 (P5(f10(f15(f6(f2(a1))),f15(f6(f2(a1)))),f10(f15(f7(a3)),f15(f7(a3))))), % 182.27/182.24 inference(scs_inference,[],[3949,3967,28,29,31,30,27,26,24,42])). % 182.27/182.24 cnf(3989,plain, % 182.27/182.24 (P4(f11(f6(f2(a1)),f10(x39891,f6(f2(a1)))),f11(f7(a3),f10(x39891,f7(a3))))), % 182.27/182.24 inference(scs_inference,[],[7,3949,3955,3967,28,29,31,30,27,26,24,42,41])). % 182.27/182.24 cnf(4008,plain, % 182.27/182.24 (P5(f10(f7(f6(f2(a1))),f7(f6(f2(a1)))),f10(f7(f7(a3)),f7(f7(a3))))), % 182.27/182.24 inference(scs_inference,[],[3953,3989,28,29,31,30,27,26,24,42])). % 182.27/182.24 cnf(4010,plain, % 182.27/182.24 (P4(f11(f6(f2(a1)),f10(f15(f6(f2(a1))),f15(f6(f2(a1))))),f11(f7(a3),f10(f15(f7(a3)),f15(f7(a3)))))), % 182.27/182.24 inference(scs_inference,[],[7,3953,3989,3987,28,29,31,30,27,26,24,42,41])). % 182.27/182.24 cnf(4020,plain, % 182.27/182.24 (P6(f15(f14(f6(f2(a1)))),f15(f14(f7(a3))))), % 182.27/182.24 inference(scs_inference,[],[3951,4010,28,29,31])). % 182.27/182.24 cnf(4022,plain, % 182.27/182.24 (P6(f14(f14(f6(f2(a1)))),f14(f14(f7(a3))))), % 182.27/182.24 inference(scs_inference,[],[3951,4010,28,29,31,30])). % 182.27/182.24 cnf(4024,plain, % 182.27/182.24 (P6(f7(f14(f6(f2(a1)))),f7(f14(f7(a3))))), % 182.27/182.24 inference(scs_inference,[],[3951,4010,28,29,31,30,27])). % 182.27/182.24 cnf(4030,plain, % 182.27/182.24 (P5(f10(f14(f6(f2(a1))),f14(f6(f2(a1)))),f10(f14(f7(a3)),f14(f7(a3))))), % 182.27/182.24 inference(scs_inference,[],[3951,4010,28,29,31,30,27,26,24,42])). % 182.27/182.24 cnf(4032,plain, % 182.27/182.24 (P4(f11(f6(f2(a1)),f10(f7(f6(f2(a1))),f7(f6(f2(a1))))),f11(f7(a3),f10(f7(f7(a3)),f7(f7(a3)))))), % 182.27/182.24 inference(scs_inference,[],[7,3951,4008,4010,28,29,31,30,27,26,24,42,41])). % 182.27/182.24 cnf(4045,plain, % 182.27/182.24 (P6(f15(f15(f14(f6(f2(a1))))),f15(f15(f14(f7(a3)))))), % 182.27/182.24 inference(scs_inference,[],[4020,4032,28,29,31])). % 182.27/182.24 cnf(4047,plain, % 182.27/182.24 (P6(f7(f15(f14(f6(f2(a1))))),f7(f15(f14(f7(a3)))))), % 182.27/182.24 inference(scs_inference,[],[4020,4032,28,29,31,27])). % 182.27/182.24 cnf(4055,plain, % 182.27/182.24 (P5(f10(f15(f14(f6(f2(a1)))),f15(f14(f6(f2(a1))))),f10(f15(f14(f7(a3))),f15(f14(f7(a3)))))), % 182.27/182.24 inference(scs_inference,[],[4020,4032,28,29,31,27,30,26,24,42])). % 182.27/182.24 cnf(4057,plain, % 182.27/182.24 (P4(f11(f6(f2(a1)),f10(f14(f6(f2(a1))),f14(f6(f2(a1))))),f11(f7(a3),f10(f14(f7(a3)),f14(f7(a3)))))), % 182.27/182.24 inference(scs_inference,[],[7,4020,4030,4032,28,29,31,27,30,26,24,42,41])). % 182.27/182.24 cnf(4067,plain, % 182.27/182.24 (P6(f15(f14(f14(f6(f2(a1))))),f15(f14(f14(f7(a3)))))), % 182.27/182.24 inference(scs_inference,[],[4022,4057,28,29,31])). % 182.27/182.24 cnf(4077,plain, % 182.27/182.24 (P5(f10(f14(f14(f6(f2(a1)))),f14(f14(f6(f2(a1))))),f10(f14(f14(f7(a3))),f14(f14(f7(a3)))))), % 182.27/182.24 inference(scs_inference,[],[4022,4057,28,29,31,30,27,26,24,42])). % 182.27/182.24 cnf(4079,plain, % 182.27/182.24 (P4(f11(f6(f2(a1)),f10(f15(f14(f6(f2(a1)))),f15(f14(f6(f2(a1)))))),f11(f7(a3),f10(f15(f14(f7(a3))),f15(f14(f7(a3))))))), % 182.27/182.24 inference(scs_inference,[],[7,4022,4057,4055,28,29,31,30,27,26,24,42,41])). % 182.27/182.24 cnf(4097,plain, % 182.27/182.24 (P2(f12(f11(f6(f2(a1)),f10(f15(f14(f6(f2(a1)))),f15(f14(f6(f2(a1))))))),f12(f11(f7(a3),f10(f15(f14(f7(a3))),f15(f14(f7(a3)))))))), % 182.27/182.24 inference(scs_inference,[],[4024,4079,28,29,31,27,30,26,24])). % 182.27/182.24 cnf(4099,plain, % 182.27/182.24 (P5(f10(f7(f14(f6(f2(a1)))),f7(f14(f6(f2(a1))))),f10(f7(f14(f7(a3))),f7(f14(f7(a3)))))), % 182.27/182.24 inference(scs_inference,[],[4024,4079,28,29,31,27,30,26,24,42])). % 182.27/182.24 cnf(4101,plain, % 182.27/182.24 (P4(f11(f6(f2(a1)),f10(f14(f14(f6(f2(a1)))),f14(f14(f6(f2(a1)))))),f11(f7(a3),f10(f14(f14(f7(a3))),f14(f14(f7(a3))))))), % 182.27/182.24 inference(scs_inference,[],[7,4024,4077,4079,28,29,31,27,30,26,24,42,41])). % 182.27/182.24 cnf(4107,plain, % 182.27/182.24 (P6(f15(f15(f15(f14(f6(f2(a1)))))),f15(f15(f15(f14(f7(a3))))))), % 182.27/182.24 inference(scs_inference,[],[4045,4101,28,29,31])). % 182.27/182.24 cnf(4115,plain, % 182.27/182.24 (P2(f12(f11(f6(f2(a1)),f10(f14(f14(f6(f2(a1)))),f14(f14(f6(f2(a1))))))),f12(f11(f7(a3),f10(f14(f14(f7(a3))),f14(f14(f7(a3)))))))), % 182.27/182.24 inference(scs_inference,[],[4045,4101,28,29,31,30,27,26,24])). % 182.27/182.24 cnf(4119,plain, % 182.27/182.24 (P4(f11(f6(f2(a1)),f10(f7(f14(f6(f2(a1)))),f7(f14(f6(f2(a1)))))),f11(f7(a3),f10(f7(f14(f7(a3))),f7(f14(f7(a3))))))), % 182.27/182.24 inference(scs_inference,[],[7,4045,4099,4101,28,29,31,30,27,26,24,42,41])). % 182.27/182.24 cnf(4137,plain, % 182.27/182.24 (P2(f12(f11(f6(f2(a1)),f10(f7(f14(f6(f2(a1)))),f7(f14(f6(f2(a1))))))),f12(f11(f7(a3),f10(f7(f14(f7(a3))),f7(f14(f7(a3)))))))), % 182.27/182.24 inference(scs_inference,[],[4107,4119,28,29,31,27,30,26,24])). % 182.27/182.24 cnf(4141,plain, % 182.27/182.24 (P4(f11(f6(f2(a1)),f10(f8(f2(a1)),f8(f2(a1)))),f11(f7(a3),f10(f8(f2(a4)),f8(f2(a4)))))), % 182.27/182.24 inference(scs_inference,[],[7,4107,4119,4047,2220,28,29,31,27,30,26,24,42,41])). % 182.27/182.24 cnf(4145,plain, % 182.27/182.24 (P6(f9(f11(f6(f2(a1)),f10(f8(f2(a1)),f8(f2(a1))))),f9(f11(f7(a3),f10(f8(f2(a4)),f8(f2(a4))))))), % 182.27/182.24 inference(scs_inference,[],[4141,28])). % 182.27/182.24 cnf(4177,plain, % 182.27/182.24 (P2(f12(f11(f6(f2(a1)),f10(f8(f2(a4)),f8(f2(a4))))),f12(f11(f7(a3),f10(f8(f2(a1)),f8(f2(a1))))))), % 182.27/182.24 inference(scs_inference,[],[7,4145,4067,2270,31,27,30,42,41,24])). % 182.27/182.24 cnf(4185,plain, % 182.27/182.24 (P6(f15(f6(f2(a5))),f15(f7(a3)))), % 182.27/182.24 inference(scs_inference,[],[8,31])). % 182.27/182.24 cnf(4189,plain, % 182.27/182.24 (P6(f14(f6(f2(a5))),f14(f7(a3)))), % 182.27/182.24 inference(scs_inference,[],[8,4177,31,25,30])). % 182.27/182.24 cnf(4191,plain, % 182.27/182.24 (P6(f7(f6(f2(a5))),f7(f7(a3)))), % 182.27/182.24 inference(scs_inference,[],[8,4177,31,25,30,27])). % 182.27/182.24 cnf(4202,plain, % 182.27/182.24 (P6(f15(f15(f6(f2(a5)))),f15(f15(f7(a3))))), % 182.27/182.24 inference(scs_inference,[],[4185,31])). % 182.27/182.24 cnf(4204,plain, % 182.27/182.24 (P6(f14(f15(f6(f2(a5)))),f14(f15(f7(a3))))), % 182.27/182.24 inference(scs_inference,[],[4185,31,30])). % 182.27/182.24 cnf(4208,plain, % 182.27/182.24 (P5(f10(f15(f6(f2(a5))),f15(f6(f2(a5)))),f10(f15(f7(a3)),f15(f7(a3))))), % 182.27/182.24 inference(scs_inference,[],[4185,31,30,27,42])). % 182.27/182.24 cnf(4212,plain, % 182.27/182.24 (P2(f12(f11(f6(f2(a5)),f10(f14(f6(f2(a1))),f14(f6(f2(a1)))))),f12(f11(f7(a3),f10(f14(f7(a3)),f14(f7(a3))))))), % 182.27/182.24 inference(scs_inference,[],[8,4185,4030,31,30,27,42,41,24])). % 182.27/182.24 cnf(4230,plain, % 182.27/182.24 (P5(f10(f14(f6(f2(a5))),f14(f6(f2(a5)))),f10(f14(f7(a3)),f14(f7(a3))))), % 182.27/182.24 inference(scs_inference,[],[4189,4191,4212,31,25,30,27,32,42])). % 182.27/182.24 cnf(4234,plain, % 182.27/182.24 (P2(f12(f11(f6(f2(a5)),f10(f15(f6(f2(a5))),f15(f6(f2(a5)))))),f12(f11(f7(a3),f10(f15(f7(a3)),f15(f7(a3))))))), % 182.27/182.24 inference(scs_inference,[],[8,4189,4191,4208,4212,31,25,30,27,32,42,41,24])). % 182.27/182.24 cnf(4252,plain, % 182.27/182.24 (P5(f10(f15(f15(f6(f2(a5)))),f15(f15(f6(f2(a5))))),f10(f15(f15(f7(a3))),f15(f15(f7(a3)))))), % 182.27/182.24 inference(scs_inference,[],[4202,4234,31,25,30,27,32,42])). % 182.27/182.24 cnf(4256,plain, % 182.27/182.24 (P2(f12(f11(f6(f2(a5)),f10(f14(f6(f2(a5))),f14(f6(f2(a5)))))),f12(f11(f7(a3),f10(f14(f7(a3)),f14(f7(a3))))))), % 182.27/182.24 inference(scs_inference,[],[8,4202,4230,4234,31,25,30,27,32,42,41,24])). % 182.27/182.24 cnf(4267,plain, % 182.27/182.24 (P6(f15(f14(f15(f6(f2(a5))))),f15(f14(f15(f7(a3)))))), % 182.27/182.24 inference(scs_inference,[],[4204,31])). % 182.27/182.24 cnf(4277,plain, % 182.27/182.24 (P5(f10(f14(f15(f6(f2(a5)))),f14(f15(f6(f2(a5))))),f10(f14(f15(f7(a3))),f14(f15(f7(a3)))))), % 182.27/182.24 inference(scs_inference,[],[4204,4256,31,25,27,30,32,42])). % 182.27/182.24 cnf(4279,plain, % 182.27/182.24 (P4(f11(f6(f2(a5)),f10(f15(f15(f6(f2(a5)))),f15(f15(f6(f2(a5)))))),f11(f7(a3),f10(f15(f15(f7(a3))),f15(f15(f7(a3))))))), % 182.27/182.24 inference(scs_inference,[],[8,4204,4252,4256,31,25,27,30,32,42,41])). % 182.27/182.24 cnf(4287,plain, % 182.27/182.24 (P2(f12(f11(f6(f2(a5)),f10(f15(f15(f6(f2(a5)))),f15(f15(f6(f2(a5))))))),f12(f11(f7(a3),f10(f15(f15(f7(a3))),f15(f15(f7(a3)))))))), % 182.27/182.24 inference(scs_inference,[],[4279,24])). % 182.27/182.24 cnf(4293,plain, % 182.27/182.24 (P6(f15(f15(f14(f15(f6(f2(a5)))))),f15(f15(f14(f15(f7(a3))))))), % 182.27/182.24 inference(scs_inference,[],[4267,4279,24,28,29,31])). % 182.27/182.24 cnf(4297,plain, % 182.27/182.24 (P6(f7(f15(f14(f15(f6(f2(a5)))))),f7(f15(f14(f15(f7(a3))))))), % 182.27/182.24 inference(scs_inference,[],[4267,4279,24,28,29,31,30,27])). % 182.27/182.24 cnf(4303,plain, % 182.27/182.24 (P4(f11(f6(f2(a5)),f10(f14(f15(f6(f2(a5)))),f14(f15(f6(f2(a5)))))),f11(f7(a3),f10(f14(f15(f7(a3))),f14(f15(f7(a3))))))), % 182.27/182.24 inference(scs_inference,[],[8,4267,4277,4279,24,28,29,31,30,27,26,42,41])). % 182.27/182.24 cnf(4738,plain, % 182.27/182.24 (P2(f12(f11(f6(f2(a5)),f10(f14(f15(f6(f2(a5)))),f14(f15(f6(f2(a5))))))),f12(f11(f7(a3),f10(f14(f15(f7(a3))),f14(f15(f7(a3)))))))), % 182.27/182.24 inference(scs_inference,[],[4303,26,24])). % 182.27/182.24 cnf(4750,plain, % 182.27/182.24 (P4(f2(f12(f11(f6(f2(a5)),f10(f15(f15(f6(f2(a5)))),f15(f15(f6(f2(a5)))))))),f2(f12(f11(f7(a3),f10(f15(f15(f7(a3))),f15(f15(f7(a3))))))))), % 182.27/182.24 inference(scs_inference,[],[4,10,4293,4287,4303,26,24,28,29,31,42,41,25])). % 182.27/182.24 cnf(4752,plain, % 182.27/182.24 (~P6(f7(f14(f15(f14(f15(f15(f15(f15(f14(a3))))))))),f8(f2(a1)))), % 182.27/182.24 inference(scs_inference,[],[4,10,4293,4287,4303,2032,238,26,24,28,29,31,42,41,25,36])). % 182.27/182.24 cnf(4774,plain, % 182.27/182.24 (P4(f2(f12(f11(f6(f2(a5)),f10(f14(f15(f6(f2(a5)))),f14(f15(f6(f2(a5)))))))),f2(f12(f11(f7(a3),f10(f14(f15(f7(a3))),f14(f15(f7(a3))))))))), % 182.27/182.24 inference(scs_inference,[],[9,4750,4738,29,28,24,26,31,25])). % 182.27/182.24 cnf(4794,plain, % 182.27/182.24 (P6(f15(f7(f15(f14(f15(f6(f2(a5))))))),f15(f7(f15(f14(f15(f7(a3)))))))), % 182.27/182.24 inference(scs_inference,[],[4774,4297,4115,29,28,26,32,24,31])). % 182.27/182.24 cnf(4798,plain, % 182.27/182.24 (P4(f2(f12(f11(f6(f2(a1)),f10(f14(f14(f6(f2(a1)))),f14(f14(f6(f2(a1)))))))),f2(f12(f11(f7(a3),f10(f14(f14(f7(a3))),f14(f14(f7(a3))))))))), % 182.27/182.24 inference(scs_inference,[],[4774,4297,4115,29,28,26,32,24,31,42,25])). % 182.27/182.24 cnf(4800,plain, % 182.27/182.24 (P6(f14(f7(f15(f14(f15(f6(f2(a5))))))),f14(f7(f15(f14(f15(f7(a3)))))))), % 182.27/182.24 inference(scs_inference,[],[4774,4297,4115,29,28,26,32,24,31,42,25,30])). % 182.27/182.24 cnf(4818,plain, % 182.27/182.24 (P4(f2(f12(f11(f6(f2(a1)),f10(f7(f14(f6(f2(a1)))),f7(f14(f6(f2(a1)))))))),f2(f12(f11(f7(a3),f10(f7(f14(f7(a3))),f7(f14(f7(a3))))))))), % 182.27/182.24 inference(scs_inference,[],[4798,4137,28,29,32,26,24,25])). % 182.27/182.24 cnf(4826,plain, % 182.27/182.24 (P6(f7(f15(f7(f15(f14(f15(f6(f2(a5)))))))),f7(f15(f7(f15(f14(f15(f7(a3))))))))), % 182.27/182.24 inference(scs_inference,[],[4798,4794,4137,28,29,32,26,24,25,42,31,30,27])). % 182.27/182.24 cnf(4848,plain, % 182.27/182.24 ($false), % 182.27/182.24 inference(scs_inference,[],[10,14,4826,4818,4800,4752,4097,26,29,28,32,31,24,42,25,30,27,36]), % 182.27/182.24 ['proof']). % 182.27/182.24 % SZS output end Proof % 182.27/182.24 % Total time :181.670000s %------------------------------------------------------------------------------