%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN646-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 : n023.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 180.82s 180.79s % Output : CNFRefutation 180.91s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN646-1 : TPTP v8.2.0. Released v2.5.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n023.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 22:11:54 EDT 2024 % 0.12/0.33 % CPUTime : % 0.45/0.59 start to proof:theBenchmark % 180.74/180.75 %------------------------------------------- % 180.74/180.75 % File :CSE---1.7 % 180.74/180.75 % Problem :theBenchmark % 180.74/180.75 % Transform :cnf % 180.74/180.75 % Format :tptp:raw % 180.74/180.75 % Command :java -jar mcs_scs.jar %d %s % 180.74/180.75 % 180.74/180.75 % Result :Theorem 180.120000s % 180.74/180.75 % Output :CNFRefutation 180.120000s % 180.74/180.75 %------------------------------------------- % 180.82/180.78 %-------------------------------------------------------------------------- % 180.82/180.78 % File : SYN646-1 : TPTP v8.2.0. Released v2.5.0. % 180.82/180.78 % Domain : Syntactic % 180.82/180.78 % Problem : Harrison problem 4391 % 180.82/180.78 % Version : Especial. % 180.82/180.78 % English : % 180.82/180.78 % 180.82/180.78 % Refs : [Har01] Email to G. Sutcliffe % 180.82/180.78 % Source : [Har01] % 180.82/180.78 % Names : % 180.82/180.78 % 180.82/180.78 % Status : Unsatisfiable % 180.82/180.78 % Rating : 0.18 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.43 v6.0.0, 0.33 v5.5.0, 0.44 v5.3.0, 0.45 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 % 180.82/180.78 % Syntax : Number of clauses : 44 ( 22 unt; 0 nHn; 39 RR) % 180.82/180.78 % Number of literals : 85 ( 0 equ; 43 neg) % 180.82/180.78 % Maximal clause size : 5 ( 1 avg) % 180.82/180.78 % Maximal term depth : 27 ( 6 avg) % 180.82/180.78 % Number of predicates : 9 ( 9 usr; 0 prp; 1-2 aty) % 180.82/180.78 % Number of functors : 15 ( 15 usr; 4 con; 0-2 aty) % 180.82/180.78 % Number of variables : 64 ( 0 sgn) % 180.82/180.78 % SPC : CNF_UNS_RFO_NEQ_HRN % 180.82/180.78 % 180.82/180.78 % Comments : % 180.82/180.78 %-------------------------------------------------------------------------- % 180.82/180.78 cnf(c22_is_p18_1,negated_conjecture, % 180.82/180.78 p18(c22) ). % 180.82/180.78 % 180.82/180.78 cnf(p10_2,negated_conjecture, % 180.82/180.78 p10(X0,X0) ). % 180.82/180.78 % 180.82/180.78 cnf(p4_3,negated_conjecture, % 180.82/180.78 p4(X48,X48) ). % 180.82/180.78 % 180.82/180.78 cnf(p3_4,negated_conjecture, % 180.82/180.78 p3(X41,X41) ). % 180.82/180.78 % 180.82/180.78 cnf(p2_5,negated_conjecture, % 180.82/180.78 p2(X16,X16) ). % 180.82/180.78 % 180.82/180.78 cnf(p16_6,negated_conjecture, % 180.82/180.78 p16(X5,X5) ). % 180.82/180.78 % 180.82/180.78 cnf(not_p21_7,negated_conjecture, % 180.82/180.78 ~ p21(f17(c25),f17(c22)) ). % 180.82/180.78 % 180.82/180.78 cnf(not_p21_8,negated_conjecture, % 180.82/180.78 ~ p21(f17(c22),f17(c23)) ). % 180.82/180.78 % 180.82/180.78 cnf(p2_9,negated_conjecture, % 180.82/180.78 p2(f12(f11(c22)),f7(c24)) ). % 180.82/180.78 % 180.82/180.78 cnf(p2_10,negated_conjecture, % 180.82/180.78 p2(f12(f11(c25)),f7(c24)) ). % 180.82/180.78 % 180.82/180.78 cnf(p2_11,negated_conjecture, % 180.82/180.78 p2(f12(f11(c23)),f7(c24)) ). % 180.82/180.78 % 180.82/180.78 cnf(p20_12,negated_conjecture, % 180.82/180.78 p20(f14(f11(c25)),f14(f11(c22))) ). % 180.82/180.78 % 180.82/180.78 cnf(p19_13,negated_conjecture, % 180.82/180.78 p19(f14(f11(c23)),f14(f11(c22))) ). % 180.82/180.78 % 180.82/180.78 cnf(p2_14,negated_conjecture, % 180.82/180.78 p2(f13(f11(c23)),f13(f11(c22))) ). % 180.82/180.78 % 180.82/180.78 cnf(p18_15,negated_conjecture, % 180.82/180.78 ( p18(X10) % 180.82/180.78 | ~ p18(X11) % 180.82/180.78 | ~ p10(X11,X10) ) ). % 180.82/180.78 % 180.82/180.78 cnf(p4_16,negated_conjecture, % 180.82/180.78 ( p4(f11(X51),f11(X52)) % 180.82/180.78 | ~ p10(X51,X52) ) ). % 180.82/180.78 % 180.82/180.78 cnf(p10_17,negated_conjecture, % 180.82/180.78 ( p10(f15(X3),f15(X4)) % 180.82/180.78 | ~ p4(X3,X4) ) ). % 180.82/180.78 % 180.82/180.78 cnf(p16_18,negated_conjecture, % 180.82/180.78 ( p16(f17(X8),f17(X9)) % 180.82/180.78 | ~ p10(X8,X9) ) ). % 180.82/180.78 % 180.82/180.78 cnf(p2_19,negated_conjecture, % 180.82/180.78 ( p2(f12(X19),f12(X20)) % 180.82/180.78 | ~ p4(X19,X20) ) ). % 180.82/180.78 % 180.82/180.78 cnf(p2_20,negated_conjecture, % 180.82/180.78 ( p2(f13(X21),f13(X22)) % 180.82/180.78 | ~ p4(X21,X22) ) ). % 180.82/180.78 % 180.82/180.78 cnf(p2_21,negated_conjecture, % 180.82/180.78 ( p2(f14(X23),f14(X24)) % 180.82/180.78 | ~ p4(X23,X24) ) ). % 180.82/180.78 % 180.82/180.78 cnf(p2_22,negated_conjecture, % 180.82/180.78 ( p2(f7(X25),f7(X26)) % 180.82/180.78 | ~ p2(X25,X26) ) ). % 180.82/180.78 % 180.82/180.78 cnf(p2_23,negated_conjecture, % 180.82/180.78 ( p2(f8(X27),f8(X28)) % 180.82/180.78 | ~ p2(X27,X28) ) ). % 180.82/180.78 % 180.82/180.78 cnf(p2_24,negated_conjecture, % 180.82/180.78 ( p2(f9(X29),f9(X30)) % 180.82/180.78 | ~ p2(X29,X30) ) ). % 180.82/180.78 % 180.82/180.78 cnf(p10_25,negated_conjecture, % 180.82/180.78 ( p10(X1,X2) % 180.82/180.78 | ~ p10(X0,X1) % 180.82/180.78 | ~ p10(X0,X2) ) ). % 180.82/180.78 % 180.82/180.78 cnf(p4_26,negated_conjecture, % 180.82/180.78 ( p4(X49,X50) % 180.82/180.78 | ~ p4(X48,X49) % 180.82/180.78 | ~ p4(X48,X50) ) ). % 180.82/180.78 % 180.82/180.78 cnf(p3_27,negated_conjecture, % 180.82/180.78 ( p3(X42,X43) % 180.82/180.78 | ~ p3(X41,X42) % 180.82/180.78 | ~ p3(X41,X43) ) ). % 180.82/180.78 % 180.82/180.78 cnf(p2_28,negated_conjecture, % 180.82/180.78 ( p2(X17,X18) % 180.82/180.78 | ~ p2(X16,X17) % 180.82/180.78 | ~ p2(X16,X18) ) ). % 180.82/180.78 % 180.82/180.78 cnf(p16_29,negated_conjecture, % 180.82/180.78 ( p16(X6,X7) % 180.82/180.78 | ~ p16(X5,X6) % 180.82/180.78 | ~ p16(X5,X7) ) ). % 180.82/180.78 % 180.82/180.78 cnf(p19_30,negated_conjecture, % 180.82/180.78 ( p19(X12,X13) % 180.82/180.78 | ~ p2(X14,X12) % 180.82/180.78 | ~ p2(X15,X13) % 180.82/180.78 | ~ p19(X14,X15) ) ). % 180.82/180.78 % 180.82/180.78 cnf(p21_31,negated_conjecture, % 180.82/180.78 ( p21(X35,X36) % 180.82/180.78 | ~ p16(X38,X36) % 180.82/180.78 | ~ p21(X37,X38) % 180.82/180.78 | ~ p16(X37,X35) ) ). % 180.82/180.78 % 180.82/180.78 cnf(p20_32,negated_conjecture, % 180.82/180.78 ( p20(X31,X32) % 180.82/180.78 | ~ p2(X34,X32) % 180.82/180.78 | ~ p20(X33,X34) % 180.82/180.78 | ~ p2(X33,X31) ) ). % 180.82/180.78 % 180.82/180.78 cnf(p4_33,negated_conjecture, % 180.82/180.78 ( p4(f5(X53,X54),f5(X55,X56)) % 180.82/180.78 | ~ p2(X53,X55) % 180.82/180.78 | ~ p3(X54,X56) ) ). % 180.82/180.79 % 180.82/180.79 cnf(p3_34,negated_conjecture, % 180.82/180.79 ( p3(f6(X44,X45),f6(X46,X47)) % 180.82/180.79 | ~ p2(X44,X46) % 180.82/180.79 | ~ p2(X45,X47) ) ). % 180.82/180.79 % 180.82/180.79 cnf(p2_35,negated_conjecture, % 180.82/180.79 p2(f13(f11(c23)),f7(f8(f9(f8(f9(f9(f9(f9(f8(c24)))))))))) ). % 180.82/180.79 % 180.82/180.79 cnf(p2_36,negated_conjecture, % 180.82/180.79 p2(f13(f11(c25)),f7(f8(f9(f8(f9(f9(f9(f9(f8(c24)))))))))) ). % 180.82/180.79 % 180.82/180.79 cnf(p21_37,negated_conjecture, % 180.82/180.79 ( p21(f17(X39),f17(X40)) % 180.82/180.79 | ~ p2(f12(f11(X40)),f7(c24)) % 180.82/180.79 | ~ p2(f12(f11(X39)),f7(c24)) % 180.82/180.79 | ~ p19(f13(f11(X39)),f13(f11(X40))) ) ). % 180.82/180.79 % 180.82/180.79 cnf(p2_38,negated_conjecture, % 180.82/180.79 p2(f14(f11(c23)),f7(f8(f8(f8(f8(f9(f9(f8(f9(f9(f9(f8(f8(f9(f8(f9(f8(f9(f8(f8(f8(f9(f8(c24)))))))))))))))))))))))) ). % 180.82/180.79 % 180.82/180.79 cnf(p2_39,negated_conjecture, % 180.82/180.79 p2(f14(f11(c25)),f7(f9(f9(f9(f9(f8(f9(f8(f9(f9(f9(f8(f8(f9(f8(f9(f8(f9(f8(f8(f8(f9(f8(c24)))))))))))))))))))))))) ). % 180.82/180.79 % 180.82/180.79 cnf(p21_40,negated_conjecture, % 180.82/180.79 ( p21(f17(X39),f17(X40)) % 180.82/180.79 | ~ p2(f12(f11(X39)),f7(c24)) % 180.82/180.79 | ~ p2(f12(f11(X40)),f7(c24)) % 180.82/180.79 | ~ p2(f13(f11(X39)),f13(f11(X40))) % 180.82/180.79 | ~ p20(f14(f11(X39)),f14(f11(X40))) ) ). % 180.82/180.79 % 180.82/180.79 cnf(p4_41,negated_conjecture, % 180.82/180.79 p4(f11(c25),f5(f7(c24),f6(f7(f8(f9(f8(f9(f9(f9(f9(f8(c24))))))))),f7(f9(f9(f9(f9(f8(f9(f8(f9(f9(f9(f8(f8(f9(f8(f9(f8(f9(f8(f8(f8(f9(f8(c24)))))))))))))))))))))))))) ). % 180.82/180.79 % 180.82/180.79 cnf(p4_42,negated_conjecture, % 180.82/180.79 p4(f11(c23),f5(f7(c24),f6(f7(f8(f9(f8(f9(f9(f9(f9(f8(c24))))))))),f7(f8(f8(f8(f8(f9(f9(f8(f9(f9(f9(f8(f8(f9(f8(f9(f8(f9(f8(f8(f8(f9(f8(c24)))))))))))))))))))))))))) ). % 180.82/180.79 % 180.82/180.79 cnf(p10_43,negated_conjecture, % 180.82/180.79 p10(f15(f5(f7(c24),f6(f7(f8(f9(f8(f9(f9(f9(f9(f8(c24))))))))),f7(f8(f8(f8(f8(f9(f9(f8(f9(f9(f9(f8(f8(f9(f8(f9(f8(f9(f8(f8(f8(f9(f8(c24)))))))))))))))))))))))))),c23) ). % 180.82/180.79 % 180.82/180.79 cnf(p10_44,negated_conjecture, % 180.82/180.79 p10(f15(f5(f7(c24),f6(f7(f8(f9(f8(f9(f9(f9(f9(f8(c24))))))))),f7(f9(f9(f9(f9(f8(f9(f8(f9(f9(f9(f8(f8(f9(f8(f9(f8(f9(f8(f8(f8(f9(f8(c24)))))))))))))))))))))))))),c25) ). % 180.82/180.79 % 180.82/180.79 %-------------------------------------------------------------------------- % 180.82/180.79 %------------------------------------------- % 180.82/180.79 % Proof found % 180.82/180.79 % SZS status Theorem for theBenchmark % 180.82/180.79 % SZS output start Proof % 180.82/180.81 %ClaNum:44(EqnAxiom:0) % 180.82/180.81 %VarNum:134(SingletonVarNum:64) % 180.82/180.81 %MaxLitNum:5 % 180.82/180.81 %MaxfuncDepth:26 % 180.82/180.81 %SharedTerms:78 % 180.82/180.81 %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 % 180.82/180.81 %singleGoalClaCount:22 % 180.82/180.81 [1]P1(a1) % 180.82/180.81 [21]~P9(f13(a1),f13(a4)) % 180.82/180.81 [22]~P9(f13(a5),f13(a1)) % 180.82/180.81 [7]P6(f6(f2(a1)),f7(a3)) % 180.82/180.81 [8]P6(f6(f2(a5)),f7(a3)) % 180.82/180.81 [9]P6(f6(f2(a4)),f7(a3)) % 180.82/180.81 [10]P6(f8(f2(a4)),f8(f2(a1))) % 180.82/180.81 [11]P8(f9(f2(a5)),f9(f2(a1))) % 180.82/180.81 [12]P7(f9(f2(a4)),f9(f2(a1))) % 180.82/180.81 [13]P6(f8(f2(a5)),f7(f14(f15(f14(f15(f15(f15(f15(f14(a3)))))))))) % 180.82/180.81 [14]P6(f8(f2(a4)),f7(f14(f15(f14(f15(f15(f15(f15(f14(a3)))))))))) % 180.82/180.81 [15]P6(f9(f2(a5)),f7(f15(f15(f15(f15(f14(f15(f14(f15(f15(f15(f14(f14(f15(f14(f15(f14(f15(f14(f14(f14(f15(f14(a3)))))))))))))))))))))))) % 180.82/180.81 [16]P6(f9(f2(a4)),f7(f14(f14(f14(f14(f15(f15(f14(f15(f15(f15(f14(f14(f15(f14(f15(f14(f15(f14(f14(f14(f15(f14(a3)))))))))))))))))))))))) % 180.82/180.81 [17]P4(f2(a5),f11(f7(a3),f10(f7(f14(f15(f14(f15(f15(f15(f15(f14(a3))))))))),f7(f15(f15(f15(f15(f14(f15(f14(f15(f15(f15(f14(f14(f15(f14(f15(f14(f15(f14(f14(f14(f15(f14(a3)))))))))))))))))))))))))) % 180.82/180.81 [18]P4(f2(a4),f11(f7(a3),f10(f7(f14(f15(f14(f15(f15(f15(f15(f14(a3))))))))),f7(f14(f14(f14(f14(f15(f15(f14(f15(f15(f15(f14(f14(f15(f14(f15(f14(f15(f14(f14(f14(f15(f14(a3)))))))))))))))))))))))))) % 180.82/180.81 [19]P2(f12(f11(f7(a3),f10(f7(f14(f15(f14(f15(f15(f15(f15(f14(a3))))))))),f7(f14(f14(f14(f14(f15(f15(f14(f15(f15(f15(f14(f14(f15(f14(f15(f14(f15(f14(f14(f14(f15(f14(a3)))))))))))))))))))))))))),a4) % 180.82/180.81 [20]P2(f12(f11(f7(a3),f10(f7(f14(f15(f14(f15(f15(f15(f15(f14(a3))))))))),f7(f15(f15(f15(f15(f14(f15(f14(f15(f15(f15(f14(f14(f15(f14(f15(f14(f15(f14(f14(f14(f15(f14(a3)))))))))))))))))))))))))),a5) % 180.82/180.81 [2]P2(x21,x21) % 180.82/180.81 [3]P4(x31,x31) % 180.82/180.81 [4]P5(x41,x41) % 180.82/180.81 [5]P6(x51,x51) % 180.82/180.81 [6]P3(x61,x61) % 180.82/180.81 [24]~P4(x241,x242)+P2(f12(x241),f12(x242)) % 180.82/180.81 [25]~P2(x251,x252)+P4(f2(x251),f2(x252)) % 180.82/180.81 [26]~P4(x261,x262)+P6(f6(x261),f6(x262)) % 180.82/180.81 [27]~P6(x271,x272)+P6(f7(x271),f7(x272)) % 180.82/180.81 [28]~P4(x281,x282)+P6(f9(x281),f9(x282)) % 180.82/180.81 [29]~P4(x291,x292)+P6(f8(x291),f8(x292)) % 180.82/180.81 [30]~P6(x301,x302)+P6(f14(x301),f14(x302)) % 180.82/180.81 [31]~P6(x311,x312)+P6(f15(x311),f15(x312)) % 180.82/180.81 [32]~P2(x321,x322)+P3(f13(x321),f13(x322)) % 180.82/180.81 [23]~P2(x232,x231)+P1(x231)+~P1(x232) % 180.82/180.81 [33]~P2(x333,x331)+P2(x331,x332)+~P2(x333,x332) % 180.82/180.81 [34]~P4(x343,x341)+P4(x341,x342)+~P4(x343,x342) % 180.82/180.81 [35]~P5(x353,x351)+P5(x351,x352)+~P5(x353,x352) % 180.82/180.81 [36]~P6(x363,x361)+P6(x361,x362)+~P6(x363,x362) % 180.82/180.81 [37]~P3(x373,x371)+P3(x371,x372)+~P3(x373,x372) % 180.82/180.81 [41]~P5(x412,x414)+~P6(x411,x413)+P4(f11(x411,x412),f11(x413,x414)) % 180.82/180.81 [42]~P6(x422,x424)+~P6(x421,x423)+P5(f10(x421,x422),f10(x423,x424)) % 180.82/180.81 [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)) % 180.82/180.81 [38]~P9(x383,x384)+P9(x381,x382)+~P3(x383,x381)+~P3(x384,x382) % 180.82/180.81 [39]~P8(x393,x394)+P8(x391,x392)+~P6(x393,x391)+~P6(x394,x392) % 180.82/180.81 [40]~P7(x404,x403)+P7(x401,x402)+~P6(x403,x402)+~P6(x404,x401) % 180.82/180.81 [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)) % 180.82/180.81 %EqnAxiom % 180.82/180.81 % 180.82/180.81 %------------------------------------------- % 180.91/180.84 cnf(54,plain, % 180.91/180.84 (P6(f7(a3),f6(f2(a5)))), % 180.91/180.84 inference(scs_inference,[],[8,5,36])). % 180.91/180.84 cnf(105,plain, % 180.91/180.84 (P2(f12(f11(f7(a3),x1051)),f12(f11(f6(f2(a5)),x1051)))), % 180.91/180.84 inference(scs_inference,[],[4,54,24,41])). % 180.91/180.84 cnf(111,plain, % 180.91/180.84 (P2(f12(f11(f6(f2(a5)),x1111)),f12(f11(f7(a3),x1111)))), % 180.91/180.84 inference(scs_inference,[],[105,2,33])). % 180.91/180.84 cnf(118,plain, % 180.91/180.84 (P6(f7(f14(f7(a3))),f7(f14(f6(f2(a5)))))), % 180.91/180.84 inference(scs_inference,[],[54,27,30])). % 180.91/180.84 cnf(133,plain, % 180.91/180.84 (P6(f15(f7(f7(a3))),f15(f7(f6(f2(a5)))))), % 180.91/180.84 inference(scs_inference,[],[54,31,27])). % 180.91/180.84 cnf(152,plain, % 180.91/180.84 (P6(f7(a3),f6(f2(a1)))), % 180.91/180.84 inference(scs_inference,[],[7,5,36])). % 180.91/180.84 cnf(187,plain, % 180.91/180.84 (P6(f7(a3),f6(f2(a4)))), % 180.91/180.84 inference(scs_inference,[],[9,5,36])). % 180.91/180.84 cnf(216,plain, % 180.91/180.84 (P6(f8(f2(a1)),f8(f2(a4)))), % 180.91/180.84 inference(scs_inference,[],[10,5,36])). % 180.91/180.84 cnf(235,plain, % 180.91/180.84 (P6(f7(f14(f15(f14(f15(f15(f15(f15(f14(a3))))))))),f8(f2(a5)))), % 180.91/180.84 inference(scs_inference,[],[13,5,36])). % 180.91/180.84 cnf(303,plain, % 180.91/180.84 (P6(f7(f14(f6(f2(a5)))),f7(f14(f7(a3))))), % 180.91/180.84 inference(scs_inference,[],[118,5,36])). % 180.91/180.84 cnf(351,plain, % 180.91/180.84 (P6(f15(f7(f6(f2(a5)))),f15(f7(f7(a3))))), % 180.91/180.84 inference(scs_inference,[],[133,5,36])). % 180.91/180.84 cnf(671,plain, % 180.91/180.84 (P2(f12(f2(f12(f11(f7(a3),x6711)))),f12(f2(f12(f11(f6(f2(a5)),x6711)))))), % 180.91/180.84 inference(scs_inference,[],[105,24,25])). % 180.91/180.84 cnf(736,plain, % 180.91/180.84 (P2(f12(f2(f12(f11(f6(f2(a5)),x7361)))),f12(f2(f12(f11(f7(a3),x7361)))))), % 180.91/180.84 inference(scs_inference,[],[671,2,33])). % 180.91/180.84 cnf(1255,plain, % 180.91/180.84 (P6(f14(f7(f6(f2(a1)))),f14(f7(f7(a3))))), % 180.91/180.84 inference(scs_inference,[],[7,27,30])). % 180.91/180.84 cnf(1260,plain, % 180.91/180.84 (P6(f14(f7(f6(f2(a4)))),f14(f7(f7(a3))))), % 180.91/180.84 inference(scs_inference,[],[9,27,30])). % 180.91/180.84 cnf(1641,plain, % 180.91/180.84 (P6(f14(f7(f7(a3))),f14(f7(f6(f2(a1)))))), % 180.91/180.84 inference(scs_inference,[],[1255,5,36])). % 180.91/180.84 cnf(1650,plain, % 180.91/180.84 (P6(f14(f7(f7(a3))),f14(f7(f6(f2(a4)))))), % 180.91/180.84 inference(scs_inference,[],[1260,5,36])). % 180.91/180.84 cnf(2154,plain, % 180.91/180.84 (P6(f15(f14(f7(f7(a3)))),f15(f14(f7(f6(f2(a4))))))), % 180.91/180.84 inference(scs_inference,[],[736,1650,25,27,30,31])). % 180.91/180.84 cnf(2169,plain, % 180.91/180.84 (~P3(x21691,f13(a5))+~P9(x21691,f13(a1))), % 180.91/180.84 inference(scs_inference,[],[22,736,1650,21,11,15,216,8,9,7,6,5,25,27,30,31,32,42,43,39,44,23,38])). % 180.91/180.84 cnf(2172,plain, % 180.91/180.84 (~P6(f8(f2(a5)),f8(f2(a1)))), % 180.91/180.84 inference(scs_inference,[],[6,11,8,7,2169,44])). % 180.91/180.84 cnf(2218,plain, % 180.91/180.84 (P5(f10(f14(f7(f6(f2(a1)))),f14(f7(f6(f2(a1))))),f10(f14(f7(f7(a3))),f14(f7(f7(a3)))))), % 180.91/180.84 inference(scs_inference,[],[2154,1255,30,31,27,42])). % 180.91/180.84 cnf(2224,plain, % 180.91/180.84 (P6(f14(f14(f7(f7(a3)))),f14(f14(f7(f6(f2(a1))))))), % 180.91/180.84 inference(scs_inference,[],[1641,30])). % 180.91/180.84 cnf(2226,plain, % 180.91/180.84 (P6(f7(f14(f7(f7(a3)))),f7(f14(f7(f6(f2(a1))))))), % 180.91/180.84 inference(scs_inference,[],[1641,30,27])). % 180.91/180.84 cnf(2230,plain, % 180.91/180.84 (P5(f10(f15(f7(f6(f2(a5)))),f15(f7(f6(f2(a5))))),f10(f15(f7(f7(a3))),f15(f7(f7(a3)))))), % 180.91/180.84 inference(scs_inference,[],[1641,351,30,27,31,42])). % 180.91/180.84 cnf(2234,plain, % 180.91/180.84 (P4(f11(f14(f7(f7(a3))),f10(f14(f7(f6(f2(a1)))),f14(f7(f6(f2(a1)))))),f11(f14(f7(f6(f2(a1)))),f10(f14(f7(f7(a3))),f14(f7(f7(a3))))))), % 180.91/180.84 inference(scs_inference,[],[2218,1641,111,351,30,27,31,42,23,41])). % 180.91/180.84 cnf(2250,plain, % 180.91/180.84 (P4(f11(f14(f14(f7(f7(a3)))),f10(f15(f7(f6(f2(a5)))),f15(f7(f6(f2(a5)))))),f11(f14(f14(f7(f6(f2(a1))))),f10(f15(f7(f7(a3))),f15(f7(f7(a3))))))), % 180.91/180.84 inference(scs_inference,[],[2224,2230,2234,24,26,28,29,30,31,27,41])). % 180.91/180.84 cnf(2252,plain, % 180.91/180.84 (P5(f10(f7(f14(f6(f2(a5)))),f7(f14(f6(f2(a5))))),f10(f7(f14(f7(a3))),f7(f14(f7(a3)))))), % 180.91/180.84 inference(scs_inference,[],[2224,2230,2234,303,24,26,28,29,30,31,27,41,42])). % 180.91/180.84 cnf(2274,plain, % 180.91/180.84 (P5(f10(f7(a3),f7(a3)),f10(f6(f2(a4)),f6(f2(a4))))), % 180.91/180.84 inference(scs_inference,[],[2226,2252,2250,187,28,24,29,26,30,31,27,41,42])). % 180.91/180.84 cnf(2295,plain, % 180.91/180.84 (P6(f14(f14(f7(f6(f2(a4))))),f14(f14(f7(f7(a3)))))), % 180.91/180.84 inference(scs_inference,[],[1260,30])). % 180.91/180.84 cnf(2308,plain, % 180.91/180.84 (P6(f15(f14(f14(f7(f6(f2(a4)))))),f15(f14(f14(f7(f7(a3))))))), % 180.91/180.84 inference(scs_inference,[],[2295,30,31])). % 180.91/180.84 cnf(2310,plain, % 180.91/180.84 (P6(f7(f14(f14(f7(f6(f2(a4)))))),f7(f14(f14(f7(f7(a3))))))), % 180.91/180.84 inference(scs_inference,[],[2295,30,31,27])). % 180.91/180.84 cnf(2385,plain, % 180.91/180.84 (P5(f10(f8(f2(a4)),f8(f2(a4))),f10(f8(f2(a1)),f8(f2(a1))))), % 180.91/180.84 inference(scs_inference,[],[2308,10,30,31,27,42])). % 180.91/180.84 cnf(2395,plain, % 180.91/180.84 (P4(f11(f7(f14(f14(f7(f6(f2(a4)))))),f10(f8(f2(a4)),f8(f2(a4)))),f11(f7(f14(f14(f7(f7(a3))))),f10(f8(f2(a1)),f8(f2(a1)))))), % 180.91/180.84 inference(scs_inference,[],[2385,2310,152,30,31,27,42,41])). % 180.91/180.84 cnf(2403,plain, % 180.91/180.84 (P6(f6(f11(f7(f14(f14(f7(f6(f2(a4)))))),f10(f8(f2(a4)),f8(f2(a4))))),f6(f11(f7(f14(f14(f7(f7(a3))))),f10(f8(f2(a1)),f8(f2(a1))))))), % 180.91/180.84 inference(scs_inference,[],[2395,28,24,25,26])). % 180.91/180.84 cnf(2405,plain, % 180.91/180.84 (P6(f8(f11(f7(f14(f14(f7(f6(f2(a4)))))),f10(f8(f2(a4)),f8(f2(a4))))),f8(f11(f7(f14(f14(f7(f7(a3))))),f10(f8(f2(a1)),f8(f2(a1))))))), % 180.91/180.84 inference(scs_inference,[],[2395,28,24,25,26,29])). % 180.91/180.84 cnf(2438,plain, % 180.91/180.84 (P5(f10(f6(f2(a4)),f6(f2(a4))),f10(f7(a3),f7(a3)))), % 180.91/180.84 inference(scs_inference,[],[2403,9,30,31,27,42])). % 180.91/180.84 cnf(2449,plain, % 180.91/180.84 (P5(f10(f6(f2(a1)),f6(f2(a1))),f10(f7(a3),f7(a3)))), % 180.91/180.84 inference(scs_inference,[],[2405,7,30,31,27,42])). % 180.91/180.84 cnf(2451,plain, % 180.91/180.84 (P4(f11(f8(f11(f7(f14(f14(f7(f6(f2(a4)))))),f10(f8(f2(a4)),f8(f2(a4))))),f10(f6(f2(a4)),f6(f2(a4)))),f11(f8(f11(f7(f14(f14(f7(f7(a3))))),f10(f8(f2(a1)),f8(f2(a1))))),f10(f7(a3),f7(a3))))), % 180.91/180.84 inference(scs_inference,[],[2438,2405,7,30,31,27,42,41])). % 180.91/180.84 cnf(2457,plain, % 180.91/180.84 (P6(f9(f11(f8(f11(f7(f14(f14(f7(f6(f2(a4)))))),f10(f8(f2(a4)),f8(f2(a4))))),f10(f6(f2(a4)),f6(f2(a4))))),f9(f11(f8(f11(f7(f14(f14(f7(f7(a3))))),f10(f8(f2(a1)),f8(f2(a1))))),f10(f7(a3),f7(a3)))))), % 180.91/180.84 inference(scs_inference,[],[2451,28])). % 180.91/180.84 cnf(2463,plain, % 180.91/180.84 (P4(f2(f12(f11(f8(f11(f7(f14(f14(f7(f6(f2(a4)))))),f10(f8(f2(a4)),f8(f2(a4))))),f10(f6(f2(a4)),f6(f2(a4)))))),f2(f12(f11(f8(f11(f7(f14(f14(f7(f7(a3))))),f10(f8(f2(a1)),f8(f2(a1))))),f10(f7(a3),f7(a3))))))), % 180.91/180.84 inference(scs_inference,[],[2451,28,24,26,25])). % 180.91/180.84 cnf(2485,plain, % 180.91/180.84 (P6(f14(f9(f11(f8(f11(f7(f14(f14(f7(f6(f2(a4)))))),f10(f8(f2(a4)),f8(f2(a4))))),f10(f6(f2(a4)),f6(f2(a4)))))),f14(f9(f11(f8(f11(f7(f14(f14(f7(f7(a3))))),f10(f8(f2(a1)),f8(f2(a1))))),f10(f7(a3),f7(a3))))))), % 180.91/180.84 inference(scs_inference,[],[2457,2463,24,28,29,26,30])). % 180.91/180.84 cnf(2503,plain, % 180.91/180.84 (P4(f11(f14(f9(f11(f8(f11(f7(f14(f14(f7(f6(f2(a4)))))),f10(f8(f2(a4)),f8(f2(a4))))),f10(f6(f2(a4)),f6(f2(a4)))))),f10(f6(f2(a1)),f6(f2(a1)))),f11(f14(f9(f11(f8(f11(f7(f14(f14(f7(f7(a3))))),f10(f8(f2(a1)),f8(f2(a1))))),f10(f7(a3),f7(a3))))),f10(f7(a3),f7(a3))))), % 180.91/180.84 inference(scs_inference,[],[2485,2449,30,31,27,41])). % 180.91/180.84 cnf(2518,plain, % 180.91/180.84 (P6(f8(f11(f14(f9(f11(f8(f11(f7(f14(f14(f7(f6(f2(a4)))))),f10(f8(f2(a4)),f8(f2(a4))))),f10(f6(f2(a4)),f6(f2(a4)))))),f10(f6(f2(a1)),f6(f2(a1))))),f8(f11(f14(f9(f11(f8(f11(f7(f14(f14(f7(f7(a3))))),f10(f8(f2(a1)),f8(f2(a1))))),f10(f7(a3),f7(a3))))),f10(f7(a3),f7(a3)))))), % 180.91/180.84 inference(scs_inference,[],[2503,28,24,25,26,29])). % 180.91/180.84 cnf(2877,plain, % 180.91/180.84 (P6(f14(f8(f11(f14(f9(f11(f8(f11(f7(f14(f14(f7(f6(f2(a4)))))),f10(f8(f2(a4)),f8(f2(a4))))),f10(f6(f2(a4)),f6(f2(a4)))))),f10(f6(f2(a1)),f6(f2(a1)))))),f14(f8(f11(f14(f9(f11(f8(f11(f7(f14(f14(f7(f7(a3))))),f10(f8(f2(a1)),f8(f2(a1))))),f10(f7(a3),f7(a3))))),f10(f7(a3),f7(a3))))))), % 180.91/180.84 inference(scs_inference,[],[2518,30])). % 180.91/180.84 cnf(2894,plain, % 180.91/180.84 (P4(f11(f14(f8(f11(f14(f9(f11(f8(f11(f7(f14(f14(f7(f6(f2(a4)))))),f10(f8(f2(a4)),f8(f2(a4))))),f10(f6(f2(a4)),f6(f2(a4)))))),f10(f6(f2(a1)),f6(f2(a1)))))),f10(f6(f2(a1)),f6(f2(a1)))),f11(f14(f8(f11(f14(f9(f11(f8(f11(f7(f14(f14(f7(f7(a3))))),f10(f8(f2(a1)),f8(f2(a1))))),f10(f7(a3),f7(a3))))),f10(f7(a3),f7(a3))))),f10(f7(a3),f7(a3))))), % 180.91/180.84 inference(scs_inference,[],[2877,2449,5,30,27,31,42,41])). % 180.91/180.84 cnf(2897,plain, % 180.91/180.84 (P6(f9(f11(f14(f8(f11(f14(f9(f11(f8(f11(f7(f14(f14(f7(f6(f2(a4)))))),f10(f8(f2(a4)),f8(f2(a4))))),f10(f6(f2(a4)),f6(f2(a4)))))),f10(f6(f2(a1)),f6(f2(a1)))))),f10(f6(f2(a1)),f6(f2(a1))))),f9(f11(f14(f8(f11(f14(f9(f11(f8(f11(f7(f14(f14(f7(f7(a3))))),f10(f8(f2(a1)),f8(f2(a1))))),f10(f7(a3),f7(a3))))),f10(f7(a3),f7(a3))))),f10(f7(a3),f7(a3)))))), % 180.91/180.84 inference(scs_inference,[],[2894,28])). % 180.91/180.84 cnf(2903,plain, % 180.91/180.84 (P6(f8(f11(f14(f8(f11(f14(f9(f11(f8(f11(f7(f14(f14(f7(f6(f2(a4)))))),f10(f8(f2(a4)),f8(f2(a4))))),f10(f6(f2(a4)),f6(f2(a4)))))),f10(f6(f2(a1)),f6(f2(a1)))))),f10(f6(f2(a1)),f6(f2(a1))))),f8(f11(f14(f8(f11(f14(f9(f11(f8(f11(f7(f14(f14(f7(f7(a3))))),f10(f8(f2(a1)),f8(f2(a1))))),f10(f7(a3),f7(a3))))),f10(f7(a3),f7(a3))))),f10(f7(a3),f7(a3)))))), % 180.91/180.84 inference(scs_inference,[],[2894,28,24,26,29])). % 180.91/180.84 cnf(3349,plain, % 180.91/180.84 (P6(f14(f9(f11(f14(f8(f11(f14(f9(f11(f8(f11(f7(f14(f14(f7(f6(f2(a4)))))),f10(f8(f2(a4)),f8(f2(a4))))),f10(f6(f2(a4)),f6(f2(a4)))))),f10(f6(f2(a1)),f6(f2(a1)))))),f10(f6(f2(a1)),f6(f2(a1)))))),f14(f9(f11(f14(f8(f11(f14(f9(f11(f8(f11(f7(f14(f14(f7(f7(a3))))),f10(f8(f2(a1)),f8(f2(a1))))),f10(f7(a3),f7(a3))))),f10(f7(a3),f7(a3))))),f10(f7(a3),f7(a3))))))), % 180.91/180.84 inference(scs_inference,[],[2897,30])). % 180.91/180.84 cnf(3351,plain, % 180.91/180.84 (P6(f7(f9(f11(f14(f8(f11(f14(f9(f11(f8(f11(f7(f14(f14(f7(f6(f2(a4)))))),f10(f8(f2(a4)),f8(f2(a4))))),f10(f6(f2(a4)),f6(f2(a4)))))),f10(f6(f2(a1)),f6(f2(a1)))))),f10(f6(f2(a1)),f6(f2(a1)))))),f7(f9(f11(f14(f8(f11(f14(f9(f11(f8(f11(f7(f14(f14(f7(f7(a3))))),f10(f8(f2(a1)),f8(f2(a1))))),f10(f7(a3),f7(a3))))),f10(f7(a3),f7(a3))))),f10(f7(a3),f7(a3))))))), % 180.91/180.84 inference(scs_inference,[],[2897,30,27])). % 180.91/180.84 cnf(3364,plain, % 180.91/180.84 (P4(f11(f14(f9(f11(f14(f8(f11(f14(f9(f11(f8(f11(f7(f14(f14(f7(f6(f2(a4)))))),f10(f8(f2(a4)),f8(f2(a4))))),f10(f6(f2(a4)),f6(f2(a4)))))),f10(f6(f2(a1)),f6(f2(a1)))))),f10(f6(f2(a1)),f6(f2(a1)))))),f10(f7(a3),f7(a3))),f11(f14(f9(f11(f14(f8(f11(f14(f9(f11(f8(f11(f7(f14(f14(f7(f7(a3))))),f10(f8(f2(a1)),f8(f2(a1))))),f10(f7(a3),f7(a3))))),f10(f7(a3),f7(a3))))),f10(f7(a3),f7(a3))))),f10(f6(f2(a4)),f6(f2(a4)))))), % 180.91/180.84 inference(scs_inference,[],[3349,2274,30,27,31,41])). % 180.91/180.84 cnf(3386,plain, % 180.91/180.84 (P4(f2(f12(f11(f14(f9(f11(f14(f8(f11(f14(f9(f11(f8(f11(f7(f14(f14(f7(f6(f2(a4)))))),f10(f8(f2(a4)),f8(f2(a4))))),f10(f6(f2(a4)),f6(f2(a4)))))),f10(f6(f2(a1)),f6(f2(a1)))))),f10(f6(f2(a1)),f6(f2(a1)))))),f10(f7(a3),f7(a3))))),f2(f12(f11(f14(f9(f11(f14(f8(f11(f14(f9(f11(f8(f11(f7(f14(f14(f7(f7(a3))))),f10(f8(f2(a1)),f8(f2(a1))))),f10(f7(a3),f7(a3))))),f10(f7(a3),f7(a3))))),f10(f7(a3),f7(a3))))),f10(f6(f2(a4)),f6(f2(a4)))))))), % 180.91/180.84 inference(scs_inference,[],[3351,3364,5,28,29,26,24,30,27,31,42,32,25])). % 180.91/180.84 cnf(3418,plain, % 180.91/180.84 (P6(f14(f8(f11(f14(f8(f11(f14(f9(f11(f8(f11(f7(f14(f14(f7(f6(f2(a4)))))),f10(f8(f2(a4)),f8(f2(a4))))),f10(f6(f2(a4)),f6(f2(a4)))))),f10(f6(f2(a1)),f6(f2(a1)))))),f10(f6(f2(a1)),f6(f2(a1)))))),f14(f8(f11(f14(f8(f11(f14(f9(f11(f8(f11(f7(f14(f14(f7(f7(a3))))),f10(f8(f2(a1)),f8(f2(a1))))),f10(f7(a3),f7(a3))))),f10(f7(a3),f7(a3))))),f10(f7(a3),f7(a3))))))), % 180.91/180.84 inference(scs_inference,[],[2903,30])). % 180.91/180.84 cnf(3422,plain, % 180.91/180.84 (P6(f15(f8(f11(f14(f8(f11(f14(f9(f11(f8(f11(f7(f14(f14(f7(f6(f2(a4)))))),f10(f8(f2(a4)),f8(f2(a4))))),f10(f6(f2(a4)),f6(f2(a4)))))),f10(f6(f2(a1)),f6(f2(a1)))))),f10(f6(f2(a1)),f6(f2(a1)))))),f15(f8(f11(f14(f8(f11(f14(f9(f11(f8(f11(f7(f14(f14(f7(f7(a3))))),f10(f8(f2(a1)),f8(f2(a1))))),f10(f7(a3),f7(a3))))),f10(f7(a3),f7(a3))))),f10(f7(a3),f7(a3))))))), % 180.91/180.84 inference(scs_inference,[],[2903,30,27,31])). % 180.91/180.84 cnf(3430,plain, % 180.91/180.84 (P4(f11(f15(f8(f11(f14(f8(f11(f14(f9(f11(f8(f11(f7(f14(f14(f7(f6(f2(a4)))))),f10(f8(f2(a4)),f8(f2(a4))))),f10(f6(f2(a4)),f6(f2(a4)))))),f10(f6(f2(a1)),f6(f2(a1)))))),f10(f6(f2(a1)),f6(f2(a1)))))),f10(f15(f7(f6(f2(a5)))),f15(f7(f6(f2(a5)))))),f11(f15(f8(f11(f14(f8(f11(f14(f9(f11(f8(f11(f7(f14(f14(f7(f7(a3))))),f10(f8(f2(a1)),f8(f2(a1))))),f10(f7(a3),f7(a3))))),f10(f7(a3),f7(a3))))),f10(f7(a3),f7(a3))))),f10(f15(f7(f7(a3))),f15(f7(f7(a3))))))), % 180.91/180.84 inference(scs_inference,[],[3422,2230,30,27,31,41])). % 180.91/180.84 cnf(3447,plain, % 180.91/180.84 (P2(f12(f11(f15(f8(f11(f14(f8(f11(f14(f9(f11(f8(f11(f7(f14(f14(f7(f6(f2(a4)))))),f10(f8(f2(a4)),f8(f2(a4))))),f10(f6(f2(a4)),f6(f2(a4)))))),f10(f6(f2(a1)),f6(f2(a1)))))),f10(f6(f2(a1)),f6(f2(a1)))))),f10(f15(f7(f6(f2(a5)))),f15(f7(f6(f2(a5))))))),f12(f11(f15(f8(f11(f14(f8(f11(f14(f9(f11(f8(f11(f7(f14(f14(f7(f7(a3))))),f10(f8(f2(a1)),f8(f2(a1))))),f10(f7(a3),f7(a3))))),f10(f7(a3),f7(a3))))),f10(f7(a3),f7(a3))))),f10(f15(f7(f7(a3))),f15(f7(f7(a3)))))))), % 180.91/180.84 inference(scs_inference,[],[3430,3418,28,29,30,26,27,24])). % 180.91/180.84 cnf(3537,plain, % 180.91/180.84 (P6(f14(f14(f7(f6(f2(a1))))),f14(f14(f7(f7(a3)))))), % 180.91/180.84 inference(scs_inference,[],[1255,30])). % 180.91/180.84 cnf(3549,plain, % 180.91/180.84 (P6(f15(f14(f14(f7(f6(f2(a1)))))),f15(f14(f14(f7(f7(a3))))))), % 180.91/180.84 inference(scs_inference,[],[3537,30,27,31])). % 180.91/180.84 cnf(3592,plain, % 180.91/180.84 (P4(f11(f15(f14(f14(f7(f6(f2(a1)))))),f10(f6(f2(a1)),f6(f2(a1)))),f11(f15(f14(f14(f7(f7(a3))))),f10(f7(a3),f7(a3))))), % 180.91/180.84 inference(scs_inference,[],[3549,2449,30,27,31,41])). % 180.91/180.84 cnf(3600,plain, % 180.91/180.84 (P6(f6(f11(f15(f14(f14(f7(f6(f2(a1)))))),f10(f6(f2(a1)),f6(f2(a1))))),f6(f11(f15(f14(f14(f7(f7(a3))))),f10(f7(a3),f7(a3)))))), % 180.91/180.84 inference(scs_inference,[],[3592,28,29,26])). % 180.91/180.84 cnf(3933,plain, % 180.91/180.84 (P6(f7(f6(f11(f15(f14(f14(f7(f6(f2(a1)))))),f10(f6(f2(a1)),f6(f2(a1)))))),f7(f6(f11(f15(f14(f14(f7(f7(a3))))),f10(f7(a3),f7(a3))))))), % 180.91/180.84 inference(scs_inference,[],[3600,27])). % 180.91/180.84 cnf(3942,plain, % 180.91/180.84 (P6(f15(f7(f6(f11(f15(f14(f14(f7(f6(f2(a1)))))),f10(f6(f2(a1)),f6(f2(a1))))))),f15(f7(f6(f11(f15(f14(f14(f7(f7(a3))))),f10(f7(a3),f7(a3)))))))), % 180.91/180.84 inference(scs_inference,[],[3933,31])). % 180.91/180.84 cnf(4180,plain, % 180.91/180.84 (~P6(f8(f2(a1)),f8(f2(a5)))), % 180.91/180.84 inference(scs_inference,[],[5,2172,36])). % 180.91/180.84 cnf(4201,plain, % 180.91/180.84 (~P6(f7(f14(f15(f14(f15(f15(f15(f15(f14(a3))))))))),f8(f2(a1)))), % 180.91/180.84 inference(scs_inference,[],[235,4180,36])). % 180.91/180.84 cnf(4454,plain, % 180.91/180.84 ($false), % 180.91/180.84 inference(scs_inference,[],[10,4,14,4201,3447,3386,3942,31,42,28,32,41,24,26,27,30,29,25,36]), % 180.91/180.84 ['proof']). % 180.91/180.84 % SZS output end Proof % 180.91/180.84 % Total time :180.120000s %------------------------------------------------------------------------------