%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN686-1 : TPTP v8.2.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n019.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:18 EDT 2024 % Result : Unsatisfiable 241.43s 241.41s % Output : CNFRefutation 241.55s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SYN686-1 : TPTP v8.2.0. Released v2.5.0. % 0.03/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.12/0.33 % Computer : n019.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 23:14:53 EDT 2024 % 0.12/0.33 % CPUTime : % 0.51/0.56 start to proof:theBenchmark % 241.37/241.36 %------------------------------------------- % 241.37/241.36 % File :CSE---1.7 % 241.37/241.36 % Problem :theBenchmark % 241.37/241.36 % Transform :cnf % 241.37/241.36 % Format :tptp:raw % 241.37/241.36 % Command :java -jar mcs_scs.jar %d %s % 241.37/241.36 % 241.37/241.37 % Result :Theorem 240.760000s % 241.37/241.37 % Output :CNFRefutation 240.760000s % 241.37/241.37 %------------------------------------------- % 241.43/241.40 %-------------------------------------------------------------------------- % 241.43/241.40 % File : SYN686-1 : TPTP v8.2.0. Released v2.5.0. % 241.43/241.40 % Domain : Syntactic % 241.43/241.40 % Problem : Harrison problem 4589 % 241.43/241.40 % Version : Especial. % 241.43/241.40 % English : % 241.43/241.40 % 241.43/241.40 % Refs : [Har01] Email to G. Sutcliffe % 241.43/241.40 % Source : [Har01] % 241.43/241.40 % Names : % 241.43/241.40 % 241.43/241.40 % Status : Unsatisfiable % 241.43/241.40 % Rating : 0.00 v5.4.0, 0.10 v5.3.0, 0.00 v5.0.0, 0.07 v4.1.0, 0.00 v2.5.0 % 241.43/241.40 % Syntax : Number of clauses : 58 ( 22 unt; 1 nHn; 42 RR) % 241.43/241.40 % Number of literals : 131 ( 0 equ; 73 neg) % 241.43/241.40 % Maximal clause size : 4 ( 2 avg) % 241.43/241.40 % Maximal term depth : 6 ( 1 avg) % 241.43/241.40 % Number of predicates : 18 ( 18 usr; 0 prp; 2-2 aty) % 241.43/241.40 % Number of functors : 26 ( 26 usr; 14 con; 0-2 aty) % 241.43/241.40 % Number of variables : 134 ( 0 sgn) % 241.43/241.40 % SPC : CNF_UNS_RFO_NEQ_NHN % 241.43/241.40 % 241.43/241.40 % Comments : % 241.43/241.40 %-------------------------------------------------------------------------- % 241.43/241.40 cnf(p11_1,negated_conjecture, % 241.43/241.40 p11(X0,X0) ). % 241.43/241.40 % 241.43/241.40 cnf(p9_2,negated_conjecture, % 241.43/241.40 p9(X102,X102) ). % 241.43/241.40 % 241.43/241.40 cnf(p8_3,negated_conjecture, % 241.43/241.40 p8(X91,X91) ). % 241.43/241.40 % 241.43/241.40 cnf(p6_4,negated_conjecture, % 241.43/241.40 p6(X88,X88) ). % 241.43/241.40 % 241.43/241.40 cnf(p4_5,negated_conjecture, % 241.43/241.40 p4(X81,X81) ). % 241.43/241.40 % 241.43/241.40 cnf(p3_6,negated_conjecture, % 241.43/241.40 p3(X57,X57) ). % 241.43/241.40 % 241.43/241.40 cnf(p28_7,negated_conjecture, % 241.43/241.40 p28(X54,X54) ). % 241.43/241.40 % 241.43/241.40 cnf(p26_8,negated_conjecture, % 241.43/241.40 p26(X47,X47) ). % 241.43/241.40 % 241.43/241.40 cnf(p24_9,negated_conjecture, % 241.43/241.40 p24(X44,X44) ). % 241.43/241.40 % 241.43/241.40 cnf(p22_10,negated_conjecture, % 241.43/241.40 p22(X37,X37) ). % 241.43/241.40 % 241.43/241.40 cnf(p20_11,negated_conjecture, % 241.43/241.40 p20(X34,X34) ). % 241.43/241.40 % 241.43/241.40 cnf(p2_12,negated_conjecture, % 241.43/241.40 p2(X27,X27) ). % 241.43/241.40 % 241.43/241.40 cnf(p18_13,negated_conjecture, % 241.43/241.40 p18(X20,X20) ). % 241.43/241.40 % 241.43/241.40 cnf(p16_14,negated_conjecture, % 241.43/241.40 p16(X13,X13) ). % 241.43/241.40 % 241.43/241.40 cnf(p14_15,negated_conjecture, % 241.43/241.41 p14(X6,X6) ). % 241.43/241.41 % 241.43/241.41 cnf(p13_16,negated_conjecture, % 241.43/241.41 p13(X3,X3) ). % 241.43/241.41 % 241.43/241.41 cnf(p3_17,negated_conjecture, % 241.43/241.41 p3(c36,f7(c33,c34)) ). % 241.43/241.41 % 241.43/241.41 cnf(p3_18,negated_conjecture, % 241.43/241.41 p3(c42,f7(c33,c34)) ). % 241.43/241.41 % 241.43/241.41 cnf(p4_19,negated_conjecture, % 241.43/241.41 p4(f5(c32,c36),c37) ). % 241.43/241.41 % 241.43/241.41 cnf(p4_20,negated_conjecture, % 241.43/241.41 p4(f5(c32,f7(c33,c34)),c35) ). % 241.43/241.41 % 241.43/241.41 cnf(p30_21,negated_conjecture, % 241.43/241.41 p30(f10(f12(c39,c36),c37),c41) ). % 241.43/241.41 % 241.43/241.41 cnf(not_p30_22,negated_conjecture, % 241.43/241.41 ~ p30(f10(f12(c39,f7(c33,c34)),c35),c41) ). % 241.43/241.41 % 241.43/241.41 cnf(p11_23,negated_conjecture, % 241.43/241.41 ( p11(X1,X2) % 241.43/241.41 | ~ p11(X0,X1) % 241.43/241.41 | ~ p11(X0,X2) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p9_24,negated_conjecture, % 241.43/241.41 ( p9(X103,X104) % 241.43/241.41 | ~ p9(X102,X103) % 241.43/241.41 | ~ p9(X102,X104) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p8_25,negated_conjecture, % 241.43/241.41 ( p8(X92,X93) % 241.43/241.41 | ~ p8(X91,X92) % 241.43/241.41 | ~ p8(X91,X93) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p6_26,negated_conjecture, % 241.43/241.41 ( p6(X89,X90) % 241.43/241.41 | ~ p6(X88,X89) % 241.43/241.41 | ~ p6(X88,X90) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p4_27,negated_conjecture, % 241.43/241.41 ( p4(X82,X83) % 241.43/241.41 | ~ p4(X81,X82) % 241.43/241.41 | ~ p4(X81,X83) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p3_28,negated_conjecture, % 241.43/241.41 ( p3(X58,X59) % 241.43/241.41 | ~ p3(X57,X58) % 241.43/241.41 | ~ p3(X57,X59) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p28_29,negated_conjecture, % 241.43/241.41 ( p28(X55,X56) % 241.43/241.41 | ~ p28(X54,X55) % 241.43/241.41 | ~ p28(X54,X56) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p26_30,negated_conjecture, % 241.43/241.41 ( p26(X48,X49) % 241.43/241.41 | ~ p26(X47,X49) % 241.43/241.41 | ~ p26(X47,X48) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p24_31,negated_conjecture, % 241.43/241.41 ( p24(X45,X46) % 241.43/241.41 | ~ p24(X44,X45) % 241.43/241.41 | ~ p24(X44,X46) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p22_32,negated_conjecture, % 241.43/241.41 ( p22(X38,X39) % 241.43/241.41 | ~ p22(X37,X38) % 241.43/241.41 | ~ p22(X37,X39) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p20_33,negated_conjecture, % 241.43/241.41 ( p20(X35,X36) % 241.43/241.41 | ~ p20(X34,X35) % 241.43/241.41 | ~ p20(X34,X36) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p2_34,negated_conjecture, % 241.43/241.41 ( p2(X28,X29) % 241.43/241.41 | ~ p2(X27,X28) % 241.43/241.41 | ~ p2(X27,X29) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p18_35,negated_conjecture, % 241.43/241.41 ( p18(X21,X22) % 241.43/241.41 | ~ p18(X20,X21) % 241.43/241.41 | ~ p18(X20,X22) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p16_36,negated_conjecture, % 241.43/241.41 ( p16(X14,X15) % 241.43/241.41 | ~ p16(X13,X14) % 241.43/241.41 | ~ p16(X13,X15) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p14_37,negated_conjecture, % 241.43/241.41 ( p14(X7,X8) % 241.43/241.41 | ~ p14(X6,X7) % 241.43/241.41 | ~ p14(X6,X8) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p13_38,negated_conjecture, % 241.43/241.41 ( p13(X4,X5) % 241.43/241.41 | ~ p13(X3,X4) % 241.43/241.41 | ~ p13(X3,X5) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p30_39,negated_conjecture, % 241.43/241.41 ( p30(X68,X69) % 241.43/241.41 | ~ p4(X71,X69) % 241.43/241.41 | ~ p9(X70,X68) % 241.43/241.41 | ~ p30(X70,X71) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p31_40,negated_conjecture, % 241.43/241.41 ( p31(X77,X78) % 241.43/241.41 | ~ p3(X80,X78) % 241.43/241.41 | ~ p31(X79,X80) % 241.43/241.41 | ~ p14(X79,X77) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p9_41,negated_conjecture, % 241.43/241.41 ( p9(f10(X105,X106),f10(X107,X108)) % 241.43/241.41 | ~ p4(X106,X108) % 241.43/241.41 | ~ p8(X105,X107) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p14_42,negated_conjecture, % 241.43/241.41 ( p14(f15(X9,X10),f15(X11,X12)) % 241.43/241.41 | ~ p13(X9,X11) % 241.43/241.41 | ~ p3(X10,X12) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p16_43,negated_conjecture, % 241.43/241.41 ( p16(f19(X16,X17),f19(X18,X19)) % 241.43/241.41 | ~ p18(X16,X18) % 241.43/241.41 | ~ p4(X17,X19) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p18_44,negated_conjecture, % 241.43/241.41 ( p18(f21(X23,X24),f21(X25,X26)) % 241.43/241.41 | ~ p20(X23,X25) % 241.43/241.41 | ~ p4(X24,X26) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p2_45,negated_conjecture, % 241.43/241.41 ( p2(f27(X30,X31),f27(X32,X33)) % 241.43/241.41 | ~ p26(X30,X32) % 241.43/241.41 | ~ p4(X31,X33) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p22_46,negated_conjecture, % 241.43/241.41 ( p22(f25(X40,X41),f25(X42,X43)) % 241.43/241.41 | ~ p24(X40,X42) % 241.43/241.41 | ~ p3(X41,X43) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p26_47,negated_conjecture, % 241.43/241.41 ( p26(f29(X50,X51),f29(X52,X53)) % 241.43/241.41 | ~ p28(X50,X52) % 241.43/241.41 | ~ p4(X51,X53) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p3_48,negated_conjecture, % 241.43/241.41 ( p3(f17(X60,X61),f17(X62,X63)) % 241.43/241.41 | ~ p16(X60,X62) % 241.43/241.41 | ~ p2(X61,X63) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p3_49,negated_conjecture, % 241.43/241.41 ( p3(f7(X64,X65),f7(X66,X67)) % 241.43/241.41 | ~ p3(X65,X67) % 241.43/241.41 | ~ p6(X64,X66) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p4_50,negated_conjecture, % 241.43/241.41 ( p4(f5(X84,X85),f5(X86,X87)) % 241.43/241.41 | ~ p2(X84,X86) % 241.43/241.41 | ~ p3(X85,X87) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p8_51,negated_conjecture, % 241.43/241.41 ( p8(f12(X94,X95),f12(X96,X97)) % 241.43/241.41 | ~ p11(X94,X96) % 241.43/241.41 | ~ p3(X95,X97) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p8_52,negated_conjecture, % 241.43/241.41 ( p8(f23(X98,X99),f23(X100,X101)) % 241.43/241.41 | ~ p11(X99,X101) % 241.43/241.41 | ~ p22(X98,X100) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p4_53,negated_conjecture, % 241.43/241.41 ( p4(f5(f27(f29(c45,X74),X75),c36),X75) % 241.43/241.41 | ~ p30(f10(f23(f25(c43,c36),c39),X74),X75) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p30_54,negated_conjecture, % 241.43/241.41 ( p30(f10(f12(c39,X72),f5(c32,X72)),f5(c32,f7(c40,X72))) % 241.43/241.41 | ~ p31(f15(c38,X72),c36) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p4_55,negated_conjecture, % 241.43/241.41 ( p4(f5(f27(f29(c45,X74),X75),f7(c33,c34)),X74) % 241.43/241.41 | ~ p30(f10(f23(f25(c43,c36),c39),X74),X75) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p30_56,negated_conjecture, % 241.43/241.41 ( p30(f10(f23(f25(c43,c36),c39),X74),X75) % 241.43/241.41 | p31(f15(c38,f17(f19(f21(c44,X74),X75),X76)),c36) % 241.43/241.41 | ~ p4(f5(X76,c36),X75) % 241.43/241.41 | ~ p4(f5(X76,f7(c33,c34)),X74) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p30_57,negated_conjecture, % 241.43/241.41 ( p30(f10(f12(c39,X73),f5(f27(f29(c45,X74),X75),X73)),f5(f27(f29(c45,X74),X75),f7(c40,X73))) % 241.43/241.41 | ~ p31(f15(c38,X73),c36) % 241.43/241.41 | ~ p30(f10(f23(f25(c43,c36),c39),X74),X75) ) ). % 241.43/241.41 % 241.43/241.41 cnf(p30_58,negated_conjecture, % 241.43/241.41 ( p30(f10(f23(f25(c43,c36),c39),X74),X75) % 241.43/241.41 | ~ p4(f5(X76,c36),X75) % 241.43/241.41 | ~ p4(f5(X76,f7(c33,c34)),X74) % 241.43/241.41 | ~ p30(f10(f12(c39,f17(f19(f21(c44,X74),X75),X76)),f5(X76,f17(f19(f21(c44,X74),X75),X76))),f5(X76,f7(c40,f17(f19(f21(c44,X74),X75),X76)))) ) ). % 241.43/241.41 % 241.43/241.41 %-------------------------------------------------------------------------- % 241.43/241.41 %------------------------------------------- % 241.43/241.41 % Proof found % 241.43/241.41 % SZS status Theorem for theBenchmark % 241.43/241.41 % SZS output start Proof % 241.43/241.44 %ClaNum:58(EqnAxiom:0) % 241.43/241.44 %VarNum:290(SingletonVarNum:134) % 241.43/241.44 %MaxLitNum:4 % 241.43/241.44 %MaxfuncDepth:5 % 241.43/241.44 %SharedTerms:29 % 241.43/241.44 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 % 241.43/241.44 %singleGoalClaCount:22 % 241.43/241.44 [17]P6(a1,f6(a2,a4)) % 241.43/241.44 [18]P6(a7,f6(a2,a4)) % 241.43/241.44 [19]P5(f13(a3,a1),a8) % 241.43/241.44 [20]P5(f13(a3,f6(a2,a4)),a5) % 241.43/241.44 [21]P17(f15(f14(a9,a1),a8),a11) % 241.43/241.44 [22]~P17(f15(f14(a9,f6(a2,a4)),a5),a11) % 241.43/241.44 [1]P1(x11,x11) % 241.43/241.44 [2]P2(x21,x21) % 241.43/241.44 [3]P3(x31,x31) % 241.43/241.44 [4]P4(x41,x41) % 241.43/241.44 [5]P5(x51,x51) % 241.43/241.44 [6]P6(x61,x61) % 241.43/241.44 [7]P7(x71,x71) % 241.43/241.44 [8]P8(x81,x81) % 241.43/241.44 [9]P9(x91,x91) % 241.43/241.44 [10]P10(x101,x101) % 241.43/241.44 [11]P11(x111,x111) % 241.43/241.44 [12]P12(x121,x121) % 241.43/241.44 [13]P13(x131,x131) % 241.43/241.44 [14]P14(x141,x141) % 241.43/241.44 [15]P15(x151,x151) % 241.43/241.44 [16]P16(x161,x161) % 241.43/241.44 [53]~P18(f21(a10,x531),a1)+P17(f15(f14(a9,x531),f13(a3,x531)),f13(a3,f6(a12,x531))) % 241.43/241.44 [54]~P17(f15(f19(f25(a17,a1),a9),x541),x542)+P5(f13(f26(f24(a16,x541),x542),a1),x542) % 241.43/241.44 [55]P5(f13(f26(f24(a16,x551),x552),f6(a2,a4)),x551)+~P17(f15(f19(f25(a17,a1),a9),x551),x552) % 241.43/241.44 [23]~P1(x233,x231)+P1(x231,x232)+~P1(x233,x232) % 241.43/241.44 [24]~P2(x243,x241)+P2(x241,x242)+~P2(x243,x242) % 241.43/241.44 [25]~P3(x253,x251)+P3(x251,x252)+~P3(x253,x252) % 241.43/241.44 [26]~P4(x263,x261)+P4(x261,x262)+~P4(x263,x262) % 241.43/241.44 [27]~P5(x273,x271)+P5(x271,x272)+~P5(x273,x272) % 241.43/241.44 [28]~P6(x283,x281)+P6(x281,x282)+~P6(x283,x282) % 241.43/241.44 [29]~P7(x293,x291)+P7(x291,x292)+~P7(x293,x292) % 241.43/241.44 [30]~P8(x303,x301)+P8(x301,x302)+~P8(x303,x302) % 241.43/241.44 [31]~P9(x313,x311)+P9(x311,x312)+~P9(x313,x312) % 241.43/241.44 [32]~P10(x323,x321)+P10(x321,x322)+~P10(x323,x322) % 241.43/241.44 [33]~P11(x333,x331)+P11(x331,x332)+~P11(x333,x332) % 241.43/241.44 [34]~P12(x343,x341)+P12(x341,x342)+~P12(x343,x342) % 241.43/241.44 [35]~P13(x353,x351)+P13(x351,x352)+~P13(x353,x352) % 241.43/241.44 [36]~P14(x363,x361)+P14(x361,x362)+~P14(x363,x362) % 241.43/241.44 [37]~P15(x373,x371)+P15(x371,x372)+~P15(x373,x372) % 241.43/241.44 [38]~P16(x383,x381)+P16(x381,x382)+~P16(x383,x382) % 241.43/241.44 [57]~P18(f21(a10,x571),a1)+~P17(f15(f19(f25(a17,a1),a9),x572),x573)+P17(f15(f14(a9,x571),f13(f26(f24(a16,x572),x573),x571)),f13(f26(f24(a16,x572),x573),f6(a12,x571))) % 241.43/241.44 [41]~P3(x411,x413)+~P5(x412,x414)+P2(f15(x411,x412),f15(x413,x414)) % 241.43/241.44 [42]~P1(x421,x423)+~P6(x422,x424)+P3(f14(x421,x422),f14(x423,x424)) % 241.43/241.44 [43]~P1(x432,x434)+~P10(x431,x433)+P3(f19(x431,x432),f19(x433,x434)) % 241.43/241.44 [44]~P6(x442,x444)+~P12(x441,x443)+P5(f13(x441,x442),f13(x443,x444)) % 241.43/241.44 [45]~P4(x451,x453)+~P6(x452,x454)+P6(f6(x451,x452),f6(x453,x454)) % 241.43/241.44 [46]~P12(x462,x464)+~P14(x461,x463)+P6(f20(x461,x462),f20(x463,x464)) % 241.43/241.44 [47]~P5(x472,x474)+~P7(x471,x473)+P8(f24(x471,x472),f24(x473,x474)) % 241.43/241.44 [48]~P6(x482,x484)+~P9(x481,x483)+P10(f25(x481,x482),f25(x483,x484)) % 241.43/241.44 [49]~P5(x492,x494)+~P8(x491,x493)+P12(f26(x491,x492),f26(x493,x494)) % 241.43/241.44 [50]~P5(x502,x504)+~P11(x501,x503)+P13(f22(x501,x502),f22(x503,x504)) % 241.43/241.44 [51]~P5(x512,x514)+~P13(x511,x513)+P14(f23(x511,x512),f23(x513,x514)) % 241.43/241.44 [52]~P6(x522,x524)+~P16(x521,x523)+P15(f21(x521,x522),f21(x523,x524)) % 241.43/241.44 [56]~P5(f13(x563,a1),x562)+~P5(f13(x563,f6(a2,a4)),x561)+P17(f15(f19(f25(a17,a1),a9),x561),x562)+P18(f21(a10,f20(f23(f22(a18,x561),x562),x563)),a1) % 241.43/241.44 [58]~P5(f13(x583,a1),x582)+~P5(f13(x583,f6(a2,a4)),x581)+P17(f15(f19(f25(a17,a1),a9),x581),x582)+~P17(f15(f14(a9,f20(f23(f22(a18,x581),x582),x583)),f13(x583,f20(f23(f22(a18,x581),x582),x583))),f13(x583,f6(a12,f20(f23(f22(a18,x581),x582),x583)))) % 241.43/241.44 [39]~P17(x393,x394)+P17(x391,x392)+~P2(x393,x391)+~P5(x394,x392) % 241.43/241.44 [40]~P18(x404,x403)+P18(x401,x402)+~P6(x403,x402)+~P15(x404,x401) % 241.43/241.44 %EqnAxiom % 241.43/241.44 % 241.43/241.44 %------------------------------------------- % 241.55/241.48 cnf(66,plain, % 241.55/241.48 (P5(a5,f13(a3,f6(a2,a4)))), % 241.55/241.48 inference(scs_inference,[],[20,5,27])). % 241.55/241.48 cnf(69,plain, % 241.55/241.48 (P6(f6(a2,a4),a7)), % 241.55/241.48 inference(scs_inference,[],[18,20,5,6,27,28])). % 241.55/241.48 cnf(102,plain, % 241.55/241.48 (P6(f6(a2,a4),a1)), % 241.55/241.48 inference(scs_inference,[],[17,6,28])). % 241.55/241.48 cnf(110,plain, % 241.55/241.48 (P5(a8,f13(a3,a1))), % 241.55/241.48 inference(scs_inference,[],[19,5,27])). % 241.55/241.48 cnf(193,plain, % 241.55/241.48 (P6(f6(x1931,f6(a2,a4)),f6(x1931,a7))), % 241.55/241.48 inference(scs_inference,[],[4,69,26,45])). % 241.55/241.48 cnf(196,plain, % 241.55/241.48 (P8(f24(x1961,a5),f24(x1961,f13(a3,f6(a2,a4))))), % 241.55/241.48 inference(scs_inference,[],[7,66,29,47])). % 241.55/241.48 cnf(197,plain, % 241.55/241.48 (P8(f24(x1971,f13(a3,f6(a2,a4))),f24(x1971,a5))), % 241.55/241.48 inference(scs_inference,[],[196,8,30])). % 241.55/241.48 cnf(200,plain, % 241.55/241.48 (P10(f25(x2001,f6(a2,a4)),f25(x2001,a7))), % 241.55/241.48 inference(scs_inference,[],[9,69,31,48])). % 241.55/241.48 cnf(201,plain, % 241.55/241.48 (P10(f25(x2011,a7),f25(x2011,f6(a2,a4)))), % 241.55/241.48 inference(scs_inference,[],[200,10,32])). % 241.55/241.48 cnf(204,plain, % 241.55/241.48 (P13(f22(x2041,a8),f22(x2041,f13(a3,a1)))), % 241.55/241.48 inference(scs_inference,[],[11,110,33,50])). % 241.55/241.48 cnf(205,plain, % 241.55/241.48 (P13(f22(x2051,f13(a3,a1)),f22(x2051,a8))), % 241.55/241.48 inference(scs_inference,[],[204,13,35])). % 241.55/241.48 cnf(208,plain, % 241.55/241.48 (P5(f13(x2081,f6(a2,a4)),f13(x2081,a7))), % 241.55/241.48 inference(scs_inference,[],[12,69,34,44])). % 241.55/241.48 cnf(209,plain, % 241.55/241.48 (P5(f13(x2091,a7),f13(x2091,f6(a2,a4)))), % 241.55/241.48 inference(scs_inference,[],[208,5,27])). % 241.55/241.48 cnf(231,plain, % 241.55/241.48 (P6(f6(x2311,a7),f6(x2311,f6(a2,a4)))), % 241.55/241.48 inference(scs_inference,[],[193,6,28])). % 241.55/241.48 cnf(291,plain, % 241.55/241.48 (P3(f19(f25(x2911,a7),x2912),f19(f25(x2911,f6(a2,a4)),x2912))), % 241.55/241.48 inference(scs_inference,[],[201,1,43,23])). % 241.55/241.48 cnf(312,plain, % 241.55/241.48 (P3(f19(f25(x3121,f6(a2,a4)),x3122),f19(f25(x3121,a7),x3122))), % 241.55/241.48 inference(scs_inference,[],[291,3,25])). % 241.55/241.48 cnf(1017,plain, % 241.55/241.48 (P3(f14(x10171,f6(x10172,a7)),f14(x10171,f6(x10172,f6(a2,a4))))), % 241.55/241.48 inference(scs_inference,[],[1,312,231,20,41,42])). % 241.55/241.48 cnf(1019,plain, % 241.55/241.48 (P5(f13(x10191,f6(x10192,a7)),f13(x10191,f6(x10192,f6(a2,a4))))), % 241.55/241.48 inference(scs_inference,[],[1,312,231,20,12,41,42,44])). % 241.55/241.48 cnf(1021,plain, % 241.55/241.48 (P6(f6(x10211,f6(x10212,a7)),f6(x10211,f6(x10212,f6(a2,a4))))), % 241.55/241.48 inference(scs_inference,[],[1,312,4,231,20,12,41,42,44,45])). % 241.55/241.48 cnf(1025,plain, % 241.55/241.48 (P12(f26(f24(x10251,f13(a3,f6(a2,a4))),f13(a3,f6(a2,a4))),f26(f24(x10251,a5),a5))), % 241.55/241.48 inference(scs_inference,[],[1,197,312,4,9,231,20,12,41,42,44,45,48,49])). % 241.55/241.48 cnf(1027,plain, % 241.55/241.48 (P13(f22(x10271,f13(a3,f6(a2,a4))),f22(x10271,a5))), % 241.55/241.48 inference(scs_inference,[],[1,197,312,4,9,231,11,20,12,41,42,44,45,48,49,50])). % 241.55/241.48 cnf(1029,plain, % 241.55/241.48 (P14(f23(f22(x10291,f13(a3,a1)),f13(a3,f6(a2,a4))),f23(f22(x10291,a8),a5))), % 241.55/241.48 inference(scs_inference,[],[1,205,197,312,4,9,231,11,20,12,41,42,44,45,48,49,50,51])). % 241.55/241.48 cnf(1033,plain, % 241.55/241.48 (~P2(f15(f14(a9,a1),a8),f15(f14(a9,f6(a2,a4)),a5))), % 241.55/241.48 inference(scs_inference,[],[1,205,197,312,4,9,16,231,11,20,21,22,12,5,41,42,44,45,48,49,50,51,52,39])). % 241.55/241.48 cnf(1038,plain, % 241.55/241.48 (P6(f20(x10381,f26(f24(x10382,f13(a3,f6(a2,a4))),f13(a3,f6(a2,a4)))),f20(x10381,f26(f24(x10382,a5),a5)))), % 241.55/241.48 inference(scs_inference,[],[1,14,205,197,312,4,9,16,231,11,20,21,22,12,5,41,42,44,45,48,49,50,51,52,39,43,46])). % 241.55/241.48 cnf(1046,plain, % 241.55/241.48 (P8(f24(x10461,f13(x10462,f6(x10463,a7))),f24(x10461,f13(x10462,f6(x10463,f6(a2,a4)))))), % 241.55/241.48 inference(scs_inference,[],[1019,7,47])). % 241.55/241.48 cnf(1048,plain, % 241.55/241.48 (P13(f22(x10481,f13(x10482,f6(x10483,a7))),f22(x10481,f13(x10482,f6(x10483,f6(a2,a4)))))), % 241.55/241.48 inference(scs_inference,[],[1019,11,7,47,50])). % 241.55/241.48 cnf(1050,plain, % 241.55/241.48 (P10(f25(x10501,f6(x10502,f6(x10503,a7))),f25(x10501,f6(x10502,f6(x10503,f6(a2,a4)))))), % 241.55/241.48 inference(scs_inference,[],[1019,1021,9,11,7,47,50,48])). % 241.55/241.48 cnf(1054,plain, % 241.55/241.48 (P14(f23(f22(x10541,f13(a3,f6(a2,a4))),f13(x10542,f6(x10543,a7))),f23(f22(x10541,a5),f13(x10542,f6(x10543,f6(a2,a4)))))), % 241.55/241.48 inference(scs_inference,[],[1,1027,1019,1021,9,11,7,47,50,48,42,51])). % 241.55/241.48 cnf(1056,plain, % 241.55/241.48 (P5(f13(f26(f24(x10561,f13(a3,f6(a2,a4))),f13(a3,f6(a2,a4))),f6(x10562,f6(x10563,a7))),f13(f26(f24(x10561,a5),a5),f6(x10562,f6(x10563,f6(a2,a4)))))), % 241.55/241.48 inference(scs_inference,[],[1,1027,1019,1021,1025,9,11,7,47,50,48,42,51,44])). % 241.55/241.48 cnf(1058,plain, % 241.55/241.48 (P12(f26(x10581,f13(x10582,f6(x10583,a7))),f26(x10581,f13(x10582,f6(x10583,f6(a2,a4)))))), % 241.55/241.48 inference(scs_inference,[],[1,1027,1019,1021,1025,8,9,11,7,47,50,48,42,51,44,49])). % 241.55/241.48 cnf(1066,plain, % 241.55/241.48 (P6(f6(x10661,f6(x10662,f6(x10663,a7))),f6(x10661,f6(x10662,f6(x10663,f6(a2,a4)))))), % 241.55/241.48 inference(scs_inference,[],[1,1027,1017,1019,1021,1029,1025,8,4,9,16,11,7,47,50,48,42,51,44,49,52,46,41,45])). % 241.55/241.48 cnf(1089,plain, % 241.55/241.48 (P12(f26(f24(x10891,f13(x10892,f6(x10893,a7))),f13(x10894,f6(x10895,a7))),f26(f24(x10891,f13(x10892,f6(x10893,f6(a2,a4)))),f13(x10894,f6(x10895,f6(a2,a4)))))), % 241.55/241.48 inference(scs_inference,[],[1046,1056,1019,11,50,49])). % 241.55/241.48 cnf(1091,plain, % 241.55/241.48 (P14(f23(f22(x10911,f13(x10912,f6(x10913,a7))),f13(x10914,f6(x10915,a7))),f23(f22(x10911,f13(x10912,f6(x10913,f6(a2,a4)))),f13(x10914,f6(x10915,f6(a2,a4)))))), % 241.55/241.48 inference(scs_inference,[],[1046,1048,1056,1019,11,50,49,51])). % 241.55/241.48 cnf(1095,plain, % 241.55/241.48 (P10(f25(x10951,f6(x10952,f6(x10953,f6(x10954,a7)))),f25(x10951,f6(x10952,f6(x10953,f6(x10954,f6(a2,a4))))))), % 241.55/241.48 inference(scs_inference,[],[1046,1048,1066,1056,9,1019,11,7,50,49,51,47,48])). % 241.55/241.48 cnf(1101,plain, % 241.55/241.48 (P6(f6(x11011,f6(x11012,f6(x11013,f6(x11014,a7)))),f6(x11011,f6(x11012,f6(x11013,f6(x11014,f6(a2,a4))))))), % 241.55/241.48 inference(scs_inference,[],[1046,1048,1058,1066,1056,4,9,16,1019,11,7,50,49,51,47,48,52,44,45])). % 241.55/241.48 cnf(1115,plain, % 241.55/241.48 (P10(f25(x11151,f20(x11152,f26(f24(x11153,f13(a3,f6(a2,a4))),f13(a3,f6(a2,a4))))),f25(x11151,f20(x11152,f26(f24(x11153,a5),a5))))), % 241.55/241.48 inference(scs_inference,[],[1038,9,48])). % 241.55/241.48 cnf(1119,plain, % 241.55/241.48 (P13(f22(x11191,a5),f22(x11191,f13(a3,f6(a2,a4))))), % 241.55/241.48 inference(scs_inference,[],[1038,1025,9,11,66,48,44,50])). % 241.55/241.48 cnf(1123,plain, % 241.55/241.48 (P6(f6(x11231,f20(x11232,f26(f24(x11233,f13(a3,f6(a2,a4))),f13(a3,f6(a2,a4))))),f6(x11231,f20(x11232,f26(f24(x11233,a5),a5))))), % 241.55/241.48 inference(scs_inference,[],[1,1038,1025,4,9,11,66,48,44,50,42,45])). % 241.55/241.48 cnf(1129,plain, % 241.55/241.48 (P8(f24(x11291,a8),f24(x11291,f13(a3,a1)))), % 241.55/241.48 inference(scs_inference,[],[1,1038,1089,14,1025,4,9,16,11,7,110,66,48,44,50,42,45,52,46,47])). % 241.55/241.48 cnf(1149,plain, % 241.55/241.48 (P12(f26(f24(x11491,a8),f13(x11492,f6(x11493,a7))),f26(f24(x11491,f13(a3,a1)),f13(x11492,f6(x11493,f6(a2,a4)))))), % 241.55/241.48 inference(scs_inference,[],[1,1129,1101,1091,1115,1089,1058,17,4,9,16,1019,43,44,48,45,46,52,42,49])). % 241.55/241.48 cnf(1151,plain, % 241.55/241.48 (P13(f22(x11511,f13(x11512,f6(a2,a4))),f22(x11511,f13(x11512,a7)))), % 241.55/241.48 inference(scs_inference,[],[1,1129,1101,1091,1115,1089,1058,17,4,9,16,1019,11,208,43,44,48,45,46,52,42,49,50])). % 241.55/241.48 cnf(1161,plain, % 241.55/241.48 (P3(f19(f25(x11611,f6(x11612,f6(x11613,a7))),x11614),f19(f25(x11611,f6(x11612,f6(x11613,f6(a2,a4)))),x11614))), % 241.55/241.48 inference(scs_inference,[],[1,1050,43])). % 241.55/241.48 cnf(1177,plain, % 241.55/241.48 (P5(f13(f26(f24(x11771,a8),f13(x11772,f6(x11773,a7))),f6(x11774,f6(a2,a4))),f13(f26(f24(x11771,f13(a3,a1)),f13(x11772,f6(x11773,f6(a2,a4)))),f6(x11774,a7)))), % 241.55/241.48 inference(scs_inference,[],[1149,193,44])). % 241.55/241.48 cnf(1187,plain, % 241.55/241.48 (P14(f23(f22(x11871,a5),f13(x11872,f6(x11873,a7))),f23(f22(x11871,f13(a3,f6(a2,a4))),f13(x11872,f6(x11873,f6(a2,a4)))))), % 241.55/241.48 inference(scs_inference,[],[1123,1119,1029,1149,1058,193,4,9,16,1019,44,46,45,52,48,51])). % 241.55/241.48 cnf(1193,plain, % 241.55/241.48 (P8(f24(x11931,f13(a3,a1)),f24(x11931,a8))), % 241.55/241.48 inference(scs_inference,[],[1,1095,1123,7,19,43,42,47])). % 241.55/241.48 cnf(1197,plain, % 241.55/241.48 (P12(f26(f24(x11971,f13(a3,a1)),f13(x11972,f6(x11973,a7))),f26(f24(x11971,a8),f13(x11972,f6(x11973,f6(a2,a4)))))), % 241.55/241.48 inference(scs_inference,[],[1193,1019,49])). % 241.55/241.48 cnf(1201,plain, % 241.55/241.48 (P13(f22(x12011,f13(x12012,a7)),f22(x12011,f13(x12012,f6(a2,a4))))), % 241.55/241.48 inference(scs_inference,[],[1193,1161,11,1019,209,49,41,50])). % 241.55/241.48 cnf(1207,plain, % 241.55/241.48 (P10(f25(x12071,a1),f25(x12071,f6(a2,a4)))), % 241.55/241.48 inference(scs_inference,[],[17,9,48])). % 241.55/241.48 cnf(1213,plain, % 241.55/241.48 (P14(f23(f22(x12131,f13(x12132,a7)),a8),f23(f22(x12131,f13(x12132,f6(a2,a4))),f13(a3,a1)))), % 241.55/241.48 inference(scs_inference,[],[1201,1187,1025,17,9,16,110,48,46,52,51])). % 241.55/241.48 cnf(1215,plain, % 241.55/241.48 (P6(f6(x12151,a1),f6(x12151,f6(a2,a4)))), % 241.55/241.48 inference(scs_inference,[],[1201,1187,1025,17,4,9,16,110,48,46,52,51,45])). % 241.55/241.48 cnf(1223,plain, % 241.55/241.48 (P6(f6(x12231,f6(x12232,a1)),f6(x12231,f6(x12232,f6(a2,a4))))), % 241.55/241.48 inference(scs_inference,[],[1,1207,1215,4,43,42,45])). % 241.55/241.48 cnf(1227,plain, % 241.55/241.48 (P10(f25(x12271,f6(x12272,a1)),f25(x12271,f6(x12272,f6(a2,a4))))), % 241.55/241.48 inference(scs_inference,[],[1,1207,1215,1197,4,9,43,42,45,44,48])). % 241.55/241.48 cnf(1231,plain, % 241.55/241.48 (P8(f24(x12311,f13(x12312,f6(a2,a4))),f24(x12311,f13(x12312,a7)))), % 241.55/241.48 inference(scs_inference,[],[1,1207,1215,1197,4,9,16,7,208,43,42,45,44,48,52,47])). % 241.55/241.48 cnf(1235,plain, % 241.55/241.48 (P3(f19(f25(x12351,f6(x12352,a1)),x12353),f19(f25(x12351,f6(x12352,f6(a2,a4))),x12353))), % 241.55/241.48 inference(scs_inference,[],[1,1227,43])). % 241.55/241.48 cnf(1239,plain, % 241.55/241.48 (P6(f6(x12391,f6(x12392,f6(x12393,a1))),f6(x12391,f6(x12392,f6(x12393,f6(a2,a4)))))), % 241.55/241.48 inference(scs_inference,[],[1,1223,1227,4,43,42,45])). % 241.55/241.48 cnf(1241,plain, % 241.55/241.48 (P10(f25(x12411,f6(x12412,f6(x12413,a1))),f25(x12411,f6(x12412,f6(x12413,f6(a2,a4)))))), % 241.55/241.48 inference(scs_inference,[],[1,1223,1227,4,9,43,42,45,48])). % 241.55/241.48 cnf(1247,plain, % 241.55/241.48 (P12(f26(f24(x12471,f13(x12472,f6(a2,a4))),f13(a3,f6(a2,a4))),f26(f24(x12471,f13(x12472,a7)),a5))), % 241.55/241.48 inference(scs_inference,[],[1,1231,1223,1227,1197,4,9,16,20,43,42,45,48,44,52,49])). % 241.55/241.48 cnf(1259,plain, % 241.55/241.48 (P6(f6(x12591,f6(x12592,f6(x12593,f6(x12594,a1)))),f6(x12591,f6(x12592,f6(x12593,f6(x12594,f6(a2,a4))))))), % 241.55/241.48 inference(scs_inference,[],[1,1247,1239,1241,1213,4,42,43,46,45])). % 241.55/241.48 cnf(1263,plain, % 241.55/241.48 (P10(f25(x12631,f6(x12632,f6(x12633,f6(x12634,a1)))),f25(x12631,f6(x12632,f6(x12633,f6(x12634,f6(a2,a4))))))), % 241.55/241.48 inference(scs_inference,[],[1,1247,1239,1241,1213,4,9,42,43,46,45,44,48])). % 241.55/241.48 cnf(1277,plain, % 241.55/241.48 (P5(f13(f26(f24(x12771,f13(x12772,f6(a2,a4))),f13(a3,f6(a2,a4))),f6(x12773,a1)),f13(f26(f24(x12771,f13(x12772,a7)),a5),f6(x12773,f6(a2,a4))))), % 241.55/241.48 inference(scs_inference,[],[1,1259,1263,1054,1247,1215,4,9,42,43,45,46,48,44])). % 241.55/241.48 cnf(1283,plain, % 241.55/241.48 (P13(f22(x12831,f13(f26(f24(x12832,f13(x12833,f6(a2,a4))),f13(a3,f6(a2,a4))),f6(x12834,a1))),f22(x12831,f13(f26(f24(x12832,f13(x12833,a7)),a5),f6(x12834,f6(a2,a4)))))), % 241.55/241.48 inference(scs_inference,[],[1,1259,1263,1151,1054,1247,1215,11,1019,4,9,16,42,43,45,46,48,44,52,51,50])). % 241.55/241.48 cnf(1287,plain, % 241.55/241.48 (P8(f24(x12871,f13(f26(f24(x12872,f13(x12873,f6(a2,a4))),f13(a3,f6(a2,a4))),f6(x12874,a1))),f24(x12871,f13(f26(f24(x12872,f13(x12873,a7)),a5),f6(x12874,f6(a2,a4)))))), % 241.55/241.48 inference(scs_inference,[],[1277,1193,7,49,47])). % 241.55/241.48 cnf(1307,plain, % 241.55/241.48 (P8(f24(x13071,f13(x13072,a7)),f24(x13071,f13(x13072,f6(a2,a4))))), % 241.55/241.48 inference(scs_inference,[],[1235,1287,1277,110,7,209,49,41,47])). % 241.55/241.48 cnf(1497,plain, % 241.55/241.48 (P6(f6(x14971,f6(a2,a4)),f6(x14971,a1))), % 241.55/241.48 inference(scs_inference,[],[102,4,45])). % 241.55/241.48 cnf(1501,plain, % 241.55/241.48 (P10(f25(x15011,f6(a2,a4)),f25(x15011,a1))), % 241.55/241.48 inference(scs_inference,[],[102,4,9,16,45,52,48])). % 241.55/241.48 cnf(1504,plain, % 241.55/241.48 (P6(f6(x15041,f6(x15042,f6(a2,a4))),f6(x15041,f6(x15042,a1)))), % 241.55/241.48 inference(scs_inference,[],[1497,4,45])). % 241.55/241.48 cnf(1510,plain, % 241.55/241.48 (P10(f25(x15101,f6(x15102,f6(a2,a4))),f25(x15101,f6(x15102,a1)))), % 241.55/241.48 inference(scs_inference,[],[1497,1501,4,9,16,1,45,43,52,48])). % 241.55/241.48 cnf(1517,plain, % 241.55/241.48 (P6(f6(x15171,f6(x15172,f6(x15173,f6(a2,a4)))),f6(x15171,f6(x15172,f6(x15173,a1))))), % 241.55/241.48 inference(scs_inference,[],[1504,4,45])). % 241.55/241.48 cnf(1523,plain, % 241.55/241.48 (P10(f25(x15231,f6(x15232,f6(x15233,f6(a2,a4)))),f25(x15231,f6(x15232,f6(x15233,a1))))), % 241.55/241.48 inference(scs_inference,[],[1504,1510,4,9,16,1,45,43,52,48])). % 241.55/241.48 cnf(1536,plain, % 241.55/241.48 (P3(f14(x15361,f6(x15362,f6(x15363,f6(x15364,f6(a2,a4))))),f14(x15361,f6(x15362,f6(x15363,f6(x15364,a1)))))), % 241.55/241.48 inference(scs_inference,[],[1517,1523,4,9,16,1,45,43,52,48,42])). % 241.55/241.48 cnf(1571,plain, % 241.55/241.48 (P6(f6(x15711,f6(x15712,f6(a2,a4))),f6(x15711,f6(x15712,a7)))), % 241.55/241.48 inference(scs_inference,[],[4,193,45])). % 241.55/241.48 cnf(1575,plain, % 241.55/241.48 (P10(f25(x15751,f6(x15752,f6(a2,a4))),f25(x15751,f6(x15752,a7)))), % 241.55/241.48 inference(scs_inference,[],[4,193,9,16,45,52,48])). % 241.55/241.48 cnf(1578,plain, % 241.55/241.48 (P6(f6(x15781,f6(x15782,f6(x15783,f6(a2,a4)))),f6(x15781,f6(x15782,f6(x15783,a7))))), % 241.55/241.48 inference(scs_inference,[],[4,1571,45])). % 241.55/241.48 cnf(1584,plain, % 241.55/241.48 (P10(f25(x15841,f6(x15842,f6(x15843,f6(a2,a4)))),f25(x15841,f6(x15842,f6(x15843,a7))))), % 241.55/241.48 inference(scs_inference,[],[4,1571,1575,9,16,1,45,43,52,48])). % 241.55/241.48 cnf(1601,plain, % 241.55/241.48 (P3(f14(x16011,f6(x16012,f6(x16013,f6(x16014,f6(a2,a4))))),f14(x16011,f6(x16012,f6(x16013,f6(x16014,a7)))))), % 241.55/241.48 inference(scs_inference,[],[4,1578,1584,9,16,1,45,43,52,48,42])). % 241.55/241.48 cnf(1617,plain, % 241.55/241.48 (P3(f14(x16171,a1),f14(x16171,f6(a2,a4)))), % 241.55/241.48 inference(scs_inference,[],[17,1,42])). % 241.55/241.48 cnf(1666,plain, % 241.55/241.48 (P14(f23(f22(x16661,f13(f26(f24(x16662,f13(x16663,f6(a2,a4))),f13(a3,f6(a2,a4))),f6(x16664,a1))),x16665),f23(f22(x16661,f13(f26(f24(x16662,f13(x16663,a7)),a5),f6(x16664,f6(a2,a4)))),x16665))), % 241.55/241.48 inference(scs_inference,[],[5,1283,51])). % 241.55/241.48 cnf(1668,plain, % 241.55/241.48 (P12(f26(f24(x16681,f13(x16682,f6(a2,a4))),x16683),f26(f24(x16681,f13(x16682,a7)),x16683))), % 241.55/241.48 inference(scs_inference,[],[5,1231,1283,51,49])). % 241.55/241.48 cnf(1678,plain, % 241.55/241.48 (P12(f26(f24(x16781,f13(x16782,a7)),x16783),f26(f24(x16781,f13(x16782,f6(a2,a4))),x16783))), % 241.55/241.48 inference(scs_inference,[],[5,1668,1536,1666,1307,1504,12,46,44,41,49])). % 241.55/241.48 cnf(2324,plain, % 241.55/241.48 (P12(f26(x23241,f13(f26(f24(x23242,a8),f13(x23243,f6(x23244,a7))),f6(x23245,f6(a2,a4)))),f26(x23241,f13(f26(f24(x23242,f13(a3,a1)),f13(x23243,f6(x23244,f6(a2,a4)))),f6(x23245,a7))))), % 241.55/241.48 inference(scs_inference,[],[1177,8,3,41,49])). % 241.55/241.48 cnf(2630,plain, % 241.55/241.48 (~P5(a8,a5)), % 241.55/241.48 inference(scs_inference,[],[1617,1033,41])). % 241.55/241.48 cnf(4917,plain, % 241.55/241.48 (~P5(f13(a3,a1),a5)), % 241.55/241.48 inference(scs_inference,[],[14,19,2630,2324,46,27])). % 241.55/241.48 cnf(4921,plain, % 241.55/241.48 (P14(f23(x49211,f13(a3,f6(a2,a4))),f23(x49211,a5))), % 241.55/241.48 inference(scs_inference,[],[20,12,14,13,19,17,2630,2324,46,27,44,51])). % 241.55/241.48 cnf(4923,plain, % 241.55/241.48 (P12(f26(x49231,f13(a3,f6(a2,a4))),f26(x49231,a5))), % 241.55/241.48 inference(scs_inference,[],[20,12,14,8,13,19,17,2630,2324,46,27,44,51,49])). % 241.55/241.48 cnf(4941,plain, % 241.55/241.48 (P6(f20(f23(x49411,f13(a3,f6(a2,a4))),x49412),f20(f23(x49411,a5),x49412))), % 241.55/241.48 inference(scs_inference,[],[12,4921,46])). % 241.55/241.48 cnf(5014,plain, % 241.55/241.48 (P6(f20(x50141,f26(x50142,f13(a3,f6(a2,a4)))),f20(x50141,f26(x50142,a5)))), % 241.55/241.48 inference(scs_inference,[],[14,4923,46])). % 241.55/241.48 cnf(5022,plain, % 241.55/241.48 (P12(f26(x50221,f13(a3,a1)),f26(x50221,a8))), % 241.55/241.48 inference(scs_inference,[],[20,12,14,8,13,19,4941,4923,1617,46,44,41,51,49])). % 241.55/241.48 cnf(5062,plain, % 241.55/241.48 (P5(f13(x50621,f20(x50622,f26(x50623,f13(a3,f6(a2,a4))))),f13(x50621,f20(x50622,f26(x50623,a5))))), % 241.55/241.48 inference(scs_inference,[],[12,14,5014,5022,46,44])). % 241.55/241.48 cnf(5149,plain, % 241.55/241.48 (P6(f20(x51491,f26(f24(x51492,f13(x51493,f6(a2,a4))),x51494)),f20(x51491,f26(f24(x51492,f13(x51493,a7)),x51494)))), % 241.55/241.48 inference(scs_inference,[],[14,1668,46])). % 241.55/241.48 cnf(5173,plain, % 241.55/241.48 (P5(f13(x51731,f20(x51732,f26(f24(x51733,f13(x51734,f6(a2,a4))),x51735))),f13(x51731,f20(x51732,f26(f24(x51733,f13(x51734,a7)),x51735))))), % 241.55/241.48 inference(scs_inference,[],[20,12,14,5149,1678,1601,46,41,44])). % 241.55/241.48 cnf(5181,plain, % 241.55/241.48 (P6(f6(x51811,f20(x51812,f26(f24(x51813,f13(x51814,f6(a2,a4))),x51815))),f6(x51811,f20(x51812,f26(f24(x51813,f13(x51814,a7)),x51815))))), % 241.55/241.49 inference(scs_inference,[],[1,20,12,4,14,8,13,5149,5062,1678,1601,46,41,44,51,49,42,45])). % 241.55/241.49 cnf(7309,plain, % 241.55/241.49 (P5(f13(x73091,f6(a2,a4)),f13(x73091,a1))), % 241.55/241.49 inference(scs_inference,[],[1,209,12,7,11,4,9,16,3,14,13,8,102,1247,5181,5173,42,52,47,50,48,45,46,51,49,41,44])). % 241.55/241.49 cnf(8029,plain, % 241.55/241.49 ($false), % 241.55/241.49 inference(scs_inference,[],[4917,7309,20,27]), % 241.55/241.49 ['proof']). % 241.55/241.49 % SZS output end Proof % 241.55/241.49 % Total time :240.760000s %------------------------------------------------------------------------------