%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN687-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 : n025.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 0.59s 0.68s % Output : CNFRefutation 0.59s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SYN687-1 : TPTP v8.2.0. Released v2.5.0. % 0.07/0.12 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.33 % Computer : n025.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Sun Jun 23 19:34:24 EDT 2024 % 0.13/0.33 % CPUTime : % 0.46/0.60 start to proof:theBenchmark % 0.59/0.67 %------------------------------------------- % 0.59/0.67 % File :CSE---1.7 % 0.59/0.67 % Problem :theBenchmark % 0.59/0.67 % Transform :cnf % 0.59/0.67 % Format :tptp:raw % 0.59/0.67 % Command :java -jar mcs_scs.jar %d %s % 0.59/0.67 % 0.59/0.67 % Result :Theorem 0.020000s % 0.59/0.67 % Output :CNFRefutation 0.020000s % 0.59/0.67 %------------------------------------------- % 0.59/0.67 %-------------------------------------------------------------------------- % 0.59/0.67 % File : SYN687-1 : TPTP v8.2.0. Released v2.5.0. % 0.59/0.67 % Domain : Syntactic % 0.59/0.67 % Problem : Harrison problem 4601 % 0.59/0.67 % Version : Especial. % 0.59/0.67 % English : % 0.59/0.67 % 0.59/0.67 % Refs : [Har01] Email to G. Sutcliffe % 0.59/0.67 % Source : [Har01] % 0.59/0.67 % Names : % 0.59/0.67 % 0.59/0.67 % Status : Unsatisfiable % 0.59/0.67 % Rating : 0.08 v8.2.0, 0.14 v8.1.0, 0.00 v7.5.0, 0.17 v7.1.0, 0.33 v7.0.0, 0.38 v6.3.0, 0.14 v6.2.0, 0.00 v5.4.0, 0.10 v5.2.0, 0.00 v5.1.0, 0.09 v5.0.0, 0.29 v4.1.0, 0.12 v4.0.1, 0.00 v4.0.0, 0.14 v3.4.0, 0.25 v3.3.0, 0.33 v3.2.0, 0.00 v3.1.0, 0.33 v2.7.0, 0.12 v2.6.0, 0.33 v2.5.0 % 0.59/0.67 % Syntax : Number of clauses : 60 ( 20 unt; 3 nHn; 39 RR) % 0.59/0.67 % Number of literals : 146 ( 0 equ; 84 neg) % 0.59/0.67 % Maximal clause size : 6 ( 2 avg) % 0.59/0.67 % Maximal term depth : 6 ( 2 avg) % 0.59/0.67 % Number of predicates : 20 ( 20 usr; 0 prp; 2-2 aty) % 0.59/0.67 % Number of functors : 26 ( 26 usr; 12 con; 0-2 aty) % 0.59/0.67 % Number of variables : 159 ( 0 sgn) % 0.59/0.67 % SPC : CNF_UNS_RFO_NEQ_NHN % 0.59/0.67 % 0.59/0.67 % Comments : % 0.59/0.67 %-------------------------------------------------------------------------- % 0.59/0.67 cnf(p10_1,negated_conjecture, % 0.59/0.67 p10(X0,X0) ). % 0.59/0.67 % 0.59/0.67 cnf(p8_2,negated_conjecture, % 0.59/0.67 p8(X127,X127) ). % 0.59/0.67 % 0.59/0.67 cnf(p6_3,negated_conjecture, % 0.59/0.67 p6(X120,X120) ). % 0.59/0.67 % 0.59/0.67 cnf(p4_4,negated_conjecture, % 0.59/0.67 p4(X109,X109) ). % 0.59/0.67 % 0.59/0.67 cnf(p33_5,negated_conjecture, % 0.59/0.67 p33(X95,X95) ). % 0.59/0.67 % 0.59/0.67 cnf(p31_6,negated_conjecture, % 0.59/0.67 p31(X92,X92) ). % 0.59/0.67 % 0.59/0.67 cnf(p3_7,negated_conjecture, % 0.59/0.67 p3(X77,X77) ). % 0.59/0.67 % 0.59/0.67 cnf(p29_8,negated_conjecture, % 0.59/0.67 p29(X70,X70) ). % 0.59/0.67 % 0.59/0.67 cnf(p27_9,negated_conjecture, % 0.59/0.67 p27(X67,X67) ). % 0.59/0.67 % 0.59/0.67 cnf(p25_10,negated_conjecture, % 0.59/0.67 p25(X60,X60) ). % 0.59/0.67 % 0.59/0.67 cnf(p23_11,negated_conjecture, % 0.59/0.67 p23(X57,X57) ). % 0.59/0.67 % 0.59/0.67 cnf(p21_12,negated_conjecture, % 0.59/0.67 p21(X50,X50) ). % 0.59/0.67 % 0.59/0.67 cnf(p2_13,negated_conjecture, % 0.59/0.67 p2(X39,X39) ). % 0.59/0.67 % 0.59/0.67 cnf(p19_14,negated_conjecture, % 0.59/0.67 p19(X27,X27) ). % 0.59/0.67 % 0.59/0.67 cnf(p17_15,negated_conjecture, % 0.59/0.67 p17(X24,X24) ). % 0.59/0.67 % 0.59/0.67 cnf(p15_16,negated_conjecture, % 0.59/0.67 p15(X17,X17) ). % 0.59/0.67 % 0.59/0.67 cnf(p13_17,negated_conjecture, % 0.59/0.67 p13(X10,X10) ). % 0.59/0.67 % 0.59/0.67 cnf(p11_18,negated_conjecture, % 0.59/0.67 p11(X3,X3) ). % 0.59/0.67 % 0.59/0.67 cnf(p34_19,negated_conjecture, % 0.59/0.67 p34(c36,c37) ). % 0.59/0.67 % 0.59/0.67 cnf(p10_20,negated_conjecture, % 0.59/0.67 ( p10(X1,X2) % 0.59/0.67 | ~ p10(X0,X1) % 0.59/0.67 | ~ p10(X0,X2) ) ). % 0.59/0.67 % 0.59/0.67 cnf(p8_21,negated_conjecture, % 0.59/0.67 ( p8(X128,X129) % 0.59/0.67 | ~ p8(X127,X128) % 0.59/0.67 | ~ p8(X127,X129) ) ). % 0.59/0.67 % 0.59/0.67 cnf(p6_22,negated_conjecture, % 0.59/0.67 ( p6(X121,X122) % 0.59/0.67 | ~ p6(X120,X121) % 0.59/0.67 | ~ p6(X120,X122) ) ). % 0.59/0.67 % 0.59/0.67 cnf(p4_23,negated_conjecture, % 0.59/0.67 ( p4(X110,X111) % 0.59/0.67 | ~ p4(X109,X110) % 0.59/0.67 | ~ p4(X109,X111) ) ). % 0.59/0.67 % 0.59/0.67 cnf(p33_24,negated_conjecture, % 0.59/0.67 ( p33(X96,X97) % 0.59/0.67 | ~ p33(X95,X96) % 0.59/0.67 | ~ p33(X95,X97) ) ). % 0.59/0.67 % 0.59/0.67 cnf(p31_25,negated_conjecture, % 0.59/0.67 ( p31(X93,X94) % 0.59/0.67 | ~ p31(X92,X93) % 0.59/0.67 | ~ p31(X92,X94) ) ). % 0.59/0.67 % 0.59/0.67 cnf(p3_26,negated_conjecture, % 0.59/0.67 ( p3(X78,X79) % 0.59/0.67 | ~ p3(X77,X78) % 0.59/0.67 | ~ p3(X77,X79) ) ). % 0.59/0.67 % 0.59/0.67 cnf(p29_27,negated_conjecture, % 0.59/0.67 ( p29(X71,X72) % 0.59/0.67 | ~ p29(X70,X71) % 0.59/0.68 | ~ p29(X70,X72) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p27_28,negated_conjecture, % 0.59/0.68 ( p27(X68,X69) % 0.59/0.68 | ~ p27(X67,X68) % 0.59/0.68 | ~ p27(X67,X69) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p25_29,negated_conjecture, % 0.59/0.68 ( p25(X61,X62) % 0.59/0.68 | ~ p25(X60,X61) % 0.59/0.68 | ~ p25(X60,X62) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p23_30,negated_conjecture, % 0.59/0.68 ( p23(X58,X59) % 0.59/0.68 | ~ p23(X57,X58) % 0.59/0.68 | ~ p23(X57,X59) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p21_31,negated_conjecture, % 0.59/0.68 ( p21(X51,X52) % 0.59/0.68 | ~ p21(X50,X51) % 0.59/0.68 | ~ p21(X50,X52) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p2_32,negated_conjecture, % 0.59/0.68 ( p2(X40,X41) % 0.59/0.68 | ~ p2(X39,X40) % 0.59/0.68 | ~ p2(X39,X41) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p19_33,negated_conjecture, % 0.59/0.68 ( p19(X28,X29) % 0.59/0.68 | ~ p19(X27,X28) % 0.59/0.68 | ~ p19(X27,X29) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p17_34,negated_conjecture, % 0.59/0.68 ( p17(X25,X26) % 0.59/0.68 | ~ p17(X24,X25) % 0.59/0.68 | ~ p17(X24,X26) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p15_35,negated_conjecture, % 0.59/0.68 ( p15(X18,X19) % 0.59/0.68 | ~ p15(X17,X18) % 0.59/0.68 | ~ p15(X17,X19) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p13_36,negated_conjecture, % 0.59/0.68 ( p13(X11,X12) % 0.59/0.68 | ~ p13(X10,X11) % 0.59/0.68 | ~ p13(X10,X12) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p11_37,negated_conjecture, % 0.59/0.68 ( p11(X4,X5) % 0.59/0.68 | ~ p11(X3,X4) % 0.59/0.68 | ~ p11(X3,X5) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p35_38,negated_conjecture, % 0.59/0.68 ( p35(X102,X103) % 0.59/0.68 | ~ p3(X105,X103) % 0.59/0.68 | ~ p35(X104,X105) % 0.59/0.68 | ~ p11(X104,X102) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p34_39,negated_conjecture, % 0.59/0.68 ( p34(X98,X99) % 0.59/0.68 | ~ p33(X101,X98) % 0.59/0.68 | ~ p34(X101,X100) % 0.59/0.68 | ~ p10(X100,X99) ) ). % 0.59/0.68 % 0.59/0.68 cnf(not_p4_40,negated_conjecture, % 0.59/0.68 ~ p4(f5(X130,f7(c38,X130)),f5(f9(c39,X130),f7(c38,X130))) ). % 0.59/0.68 % 0.59/0.68 cnf(p11_41,negated_conjecture, % 0.59/0.68 ( p11(f12(X6,X7),f12(X8,X9)) % 0.59/0.68 | ~ p10(X6,X8) % 0.59/0.68 | ~ p3(X7,X9) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p6_42,negated_conjecture, % 0.59/0.68 ( p6(f20(X123,X124),f20(X125,X126)) % 0.59/0.68 | ~ p19(X123,X125) % 0.59/0.68 | ~ p2(X124,X126) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p4_43,negated_conjecture, % 0.59/0.68 ( p4(f5(X112,X113),f5(X114,X115)) % 0.59/0.68 | ~ p2(X112,X114) % 0.59/0.68 | ~ p3(X113,X115) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p3_44,negated_conjecture, % 0.59/0.68 ( p3(f7(X88,X89),f7(X90,X91)) % 0.59/0.68 | ~ p2(X89,X91) % 0.59/0.68 | ~ p6(X88,X90) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p3_45,negated_conjecture, % 0.59/0.68 ( p3(f30(X84,X85),f30(X86,X87)) % 0.59/0.68 | ~ p29(X84,X86) % 0.59/0.68 | ~ p8(X85,X87) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p3_46,negated_conjecture, % 0.59/0.68 ( p3(f14(X80,X81),f14(X82,X83)) % 0.59/0.68 | ~ p13(X80,X82) % 0.59/0.68 | ~ p3(X81,X83) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p29_47,negated_conjecture, % 0.59/0.68 ( p29(f32(X73,X74),f32(X75,X76)) % 0.59/0.68 | ~ p10(X74,X76) % 0.59/0.68 | ~ p31(X73,X75) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p25_48,negated_conjecture, % 0.59/0.68 ( p25(f28(X63,X64),f28(X65,X66)) % 0.59/0.68 | ~ p10(X64,X66) % 0.59/0.68 | ~ p27(X63,X65) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p21_49,negated_conjecture, % 0.59/0.68 ( p21(f24(X53,X54),f24(X55,X56)) % 0.59/0.68 | ~ p10(X54,X56) % 0.59/0.68 | ~ p23(X53,X55) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p2_50,negated_conjecture, % 0.59/0.68 ( p2(f9(X46,X47),f9(X48,X49)) % 0.59/0.68 | ~ p2(X47,X49) % 0.59/0.68 | ~ p8(X46,X48) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p2_51,negated_conjecture, % 0.59/0.68 ( p2(f26(X42,X43),f26(X44,X45)) % 0.59/0.68 | ~ p25(X42,X44) % 0.59/0.68 | ~ p8(X43,X45) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p19_52,negated_conjecture, % 0.59/0.68 ( p19(f22(X30,X31),f22(X32,X33)) % 0.59/0.68 | ~ p21(X30,X32) % 0.59/0.68 | ~ p8(X31,X33) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p15_53,negated_conjecture, % 0.59/0.68 ( p15(f18(X20,X21),f18(X22,X23)) % 0.59/0.68 | ~ p17(X20,X22) % 0.59/0.68 | ~ p2(X21,X23) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p13_54,negated_conjecture, % 0.59/0.68 ( p13(f16(X13,X14),f16(X15,X16)) % 0.59/0.68 | ~ p15(X13,X15) % 0.59/0.68 | ~ p2(X14,X16) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p4_55,negated_conjecture, % 0.59/0.68 ( p4(f5(f9(c39,X106),X108),f5(f9(c39,X107),X108)) % 0.59/0.68 | p35(f12(c37,f14(f16(f18(c40,X106),X107),X108)),X108) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p4_56,negated_conjecture, % 0.59/0.68 ( p4(f5(f9(c39,X106),X108),f5(f9(c39,X107),X108)) % 0.59/0.68 | ~ p4(f5(X106,f14(f16(f18(c40,X106),X107),X108)),f5(X107,f14(f16(f18(c40,X106),X107),X108))) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p4_57,negated_conjecture, % 0.59/0.68 ( p4(f5(f26(f28(c46,X116),X117),X118),f5(f26(f28(c47,X116),X117),X118)) % 0.59/0.68 | p4(f5(f26(f28(c46,X116),X117),X119),f5(f9(X117,f26(f28(c46,X116),X117)),X119)) % 0.59/0.68 | ~ p34(c36,X116) % 0.59/0.68 | ~ p35(f12(X116,X118),f30(f32(c45,X116),X117)) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p4_58,negated_conjecture, % 0.59/0.68 ( p4(f5(f26(f28(c46,X116),X117),X119),f5(f9(X117,f26(f28(c46,X116),X117)),X119)) % 0.59/0.68 | ~ p34(c36,X116) % 0.59/0.68 | ~ p4(f5(f9(X117,f26(f28(c46,X116),X117)),f30(f32(c45,X116),X117)),f5(f9(X117,f26(f28(c47,X116),X117)),f30(f32(c45,X116),X117))) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p2_59,negated_conjecture, % 0.59/0.68 ( p2(X34,X35) % 0.59/0.68 | p4(f5(f26(f28(c42,X36),X37),X38),f5(f26(f28(c43,X36),X37),X38)) % 0.59/0.68 | ~ p34(c36,X36) % 0.59/0.68 | ~ p35(f12(X36,X38),f30(f32(c41,X36),X37)) % 0.59/0.68 | ~ p4(f5(X34,f7(f20(f22(f24(c44,X36),X37),X34),X35)),f5(f9(X37,X34),f7(f20(f22(f24(c44,X36),X37),X34),X35))) % 0.59/0.68 | ~ p4(f5(X35,f7(f20(f22(f24(c44,X36),X37),X34),X35)),f5(f9(X37,X35),f7(f20(f22(f24(c44,X36),X37),X34),X35))) ) ). % 0.59/0.68 % 0.59/0.68 cnf(p2_60,negated_conjecture, % 0.59/0.68 ( p2(X34,X35) % 0.59/0.68 | ~ p34(c36,X36) % 0.59/0.68 | ~ p4(f5(X34,f7(f20(f22(f24(c44,X36),X37),X34),X35)),f5(f9(X37,X34),f7(f20(f22(f24(c44,X36),X37),X34),X35))) % 0.59/0.68 | ~ p4(f5(X35,f7(f20(f22(f24(c44,X36),X37),X34),X35)),f5(f9(X37,X35),f7(f20(f22(f24(c44,X36),X37),X34),X35))) % 0.59/0.68 | ~ p4(f5(f9(X37,f26(f28(c42,X36),X37)),f30(f32(c41,X36),X37)),f5(f9(X37,f26(f28(c43,X36),X37)),f30(f32(c41,X36),X37))) ) ). % 0.59/0.68 % 0.59/0.68 %-------------------------------------------------------------------------- % 0.59/0.68 %------------------------------------------- % 0.59/0.68 % Proof found % 0.59/0.68 % SZS status Theorem for theBenchmark % 0.59/0.68 % SZS output start Proof % 0.59/0.68 %ClaNum:60(EqnAxiom:0) % 0.59/0.68 %VarNum:402(SingletonVarNum:159) % 0.59/0.68 %MaxLitNum:6 % 0.59/0.68 %MaxfuncDepth:5 % 0.59/0.68 %SharedTerms:13 % 0.59/0.68 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 % 0.59/0.68 %singleGoalClaCount:20 % 0.59/0.68 [1]P1(a1,a2) % 0.59/0.68 [2]P2(x21,x21) % 0.59/0.68 [3]P17(x31,x31) % 0.59/0.68 [4]P18(x41,x41) % 0.59/0.68 [5]P19(x51,x51) % 0.59/0.68 [6]P3(x61,x61) % 0.59/0.68 [7]P4(x71,x71) % 0.59/0.68 [8]P5(x81,x81) % 0.59/0.68 [9]P6(x91,x91) % 0.59/0.68 [10]P7(x101,x101) % 0.59/0.68 [11]P8(x111,x111) % 0.59/0.68 [12]P9(x121,x121) % 0.59/0.68 [13]P10(x131,x131) % 0.59/0.68 [14]P11(x141,x141) % 0.59/0.68 [15]P12(x151,x151) % 0.59/0.68 [16]P13(x161,x161) % 0.59/0.68 [17]P14(x171,x171) % 0.59/0.68 [18]P15(x181,x181) % 0.59/0.68 [19]P16(x191,x191) % 0.59/0.68 [20]~P19(f5(x201,f4(a3,x201)),f5(f26(a6,x201),f4(a3,x201))) % 0.59/0.68 [55]P19(f5(f26(a6,x551),x552),f5(f26(a6,x553),x552))+P20(f9(a2,f8(f19(f18(a10,x551),x553),x552)),x552) % 0.59/0.68 [57]P19(f5(f26(a6,x571),x572),f5(f26(a6,x573),x572))+~P19(f5(x571,f8(f19(f18(a10,x571),x573),x572)),f5(x573,f8(f19(f18(a10,x571),x573),x572))) % 0.59/0.68 [21]~P2(x213,x211)+P2(x211,x212)+~P2(x213,x212) % 0.59/0.68 [22]~P17(x223,x221)+P17(x221,x222)+~P17(x223,x222) % 0.59/0.68 [23]~P18(x233,x231)+P18(x231,x232)+~P18(x233,x232) % 0.59/0.68 [24]~P19(x243,x241)+P19(x241,x242)+~P19(x243,x242) % 0.59/0.68 [25]~P3(x253,x251)+P3(x251,x252)+~P3(x253,x252) % 0.59/0.68 [26]~P4(x263,x261)+P4(x261,x262)+~P4(x263,x262) % 0.59/0.68 [27]~P5(x273,x271)+P5(x271,x272)+~P5(x273,x272) % 0.59/0.68 [28]~P6(x283,x281)+P6(x281,x282)+~P6(x283,x282) % 0.59/0.68 [29]~P7(x293,x291)+P7(x291,x292)+~P7(x293,x292) % 0.59/0.68 [30]~P8(x303,x301)+P8(x301,x302)+~P8(x303,x302) % 0.59/0.68 [31]~P9(x313,x311)+P9(x311,x312)+~P9(x313,x312) % 0.59/0.68 [32]~P10(x323,x321)+P10(x321,x322)+~P10(x323,x322) % 0.59/0.68 [33]~P11(x333,x331)+P11(x331,x332)+~P11(x333,x332) % 0.59/0.68 [34]~P12(x343,x341)+P12(x341,x342)+~P12(x343,x342) % 0.59/0.68 [35]~P13(x353,x351)+P13(x351,x352)+~P13(x353,x352) % 0.59/0.68 [36]~P14(x363,x361)+P14(x361,x362)+~P14(x363,x362) % 0.59/0.68 [37]~P15(x373,x371)+P15(x371,x372)+~P15(x373,x372) % 0.59/0.68 [38]~P16(x383,x381)+P16(x381,x382)+~P16(x383,x382) % 0.59/0.68 [58]~P1(a1,x581)+~P19(f5(f26(x582,f24(f21(a11,x581),x582)),f20(f25(a12,x581),x582)),f5(f26(x582,f24(f21(a17,x581),x582)),f20(f25(a12,x581),x582)))+P19(f5(f24(f21(a11,x581),x582),x583),f5(f26(x582,f24(f21(a11,x581),x582)),x583)) % 0.59/0.68 [41]~P11(x412,x414)+~P12(x411,x413)+P18(f7(x411,x412),f7(x413,x414)) % 0.59/0.68 [42]~P5(x422,x424)+~P11(x421,x423)+P19(f5(x421,x422),f5(x423,x424)) % 0.59/0.68 [43]~P18(x431,x433)+~P11(x432,x434)+P5(f4(x431,x432),f4(x433,x434)) % 0.59/0.68 [44]~P17(x442,x444)+~P6(x441,x443)+P5(f20(x441,x442),f20(x443,x444)) % 0.59/0.68 [45]~P5(x452,x454)+~P15(x451,x453)+P5(f8(x451,x452),f8(x453,x454)) % 0.59/0.68 [46]~P2(x462,x464)+~P4(x461,x463)+P6(f25(x461,x462),f25(x463,x464)) % 0.59/0.68 [47]~P2(x472,x474)+~P7(x471,x473)+P8(f21(x471,x472),f21(x473,x474)) % 0.59/0.68 [48]~P2(x482,x484)+~P9(x481,x483)+P10(f22(x481,x482),f22(x483,x484)) % 0.59/0.68 [49]~P17(x491,x493)+~P11(x492,x494)+P11(f26(x491,x492),f26(x493,x494)) % 0.59/0.68 [50]~P17(x502,x504)+~P8(x501,x503)+P11(f24(x501,x502),f24(x503,x504)) % 0.59/0.68 [51]~P17(x512,x514)+~P10(x511,x513)+P12(f23(x511,x512),f23(x513,x514)) % 0.59/0.68 [52]~P11(x522,x524)+~P13(x521,x523)+P14(f18(x521,x522),f18(x523,x524)) % 0.59/0.68 [53]~P11(x532,x534)+~P14(x531,x533)+P15(f19(x531,x532),f19(x533,x534)) % 0.59/0.68 [54]~P2(x541,x543)+~P5(x542,x544)+P16(f9(x541,x542),f9(x543,x544)) % 0.59/0.68 [39]~P1(x394,x393)+P1(x391,x392)+~P2(x393,x392)+~P3(x394,x391) % 0.59/0.68 [40]~P20(x404,x403)+P20(x401,x402)+~P5(x403,x402)+~P16(x404,x401) % 0.59/0.68 [56]~P1(a1,x561)+~P20(f9(x561,x563),f20(f25(a12,x561),x562))+P19(f5(f24(f21(a11,x561),x562),x563),f5(f24(f21(a17,x561),x562),x563))+P19(f5(f24(f21(a11,x561),x562),x564),f5(f26(x562,f24(f21(a11,x561),x562)),x564)) % 0.59/0.68 [60]P11(x601,x602)+~P1(a1,x603)+~P19(f5(f26(x604,f24(f21(a13,x603),x604)),f20(f25(a14,x603),x604)),f5(f26(x604,f24(f21(a15,x603),x604)),f20(f25(a14,x603),x604)))+~P19(f5(x601,f4(f7(f23(f22(a16,x603),x604),x601),x602)),f5(f26(x604,x601),f4(f7(f23(f22(a16,x603),x604),x601),x602)))+~P19(f5(x602,f4(f7(f23(f22(a16,x603),x604),x601),x602)),f5(f26(x604,x602),f4(f7(f23(f22(a16,x603),x604),x601),x602))) % 0.59/0.68 [59]P11(x591,x592)+~P1(a1,x593)+~P20(f9(x593,x595),f20(f25(a14,x593),x594))+P19(f5(f24(f21(a13,x593),x594),x595),f5(f24(f21(a15,x593),x594),x595))+~P19(f5(x591,f4(f7(f23(f22(a16,x593),x594),x591),x592)),f5(f26(x594,x591),f4(f7(f23(f22(a16,x593),x594),x591),x592)))+~P19(f5(x592,f4(f7(f23(f22(a16,x593),x594),x591),x592)),f5(f26(x594,x592),f4(f7(f23(f22(a16,x593),x594),x591),x592))) % 0.59/0.68 %EqnAxiom % 0.59/0.68 % 0.59/0.68 %------------------------------------------- % 0.59/0.68 cnf(64,plain, % 0.59/0.68 (~P19(f5(f26(a6,f24(f21(a11,a2),a6)),f20(f25(a12,a2),a6)),f5(f26(a6,f24(f21(a17,a2),a6)),f20(f25(a12,a2),a6)))), % 0.59/0.68 inference(scs_inference,[],[1,8,20,42,58])). % 0.59/0.68 cnf(78,plain, % 0.59/0.68 (~P20(f9(a2,x781),f20(f25(a12,a2),a6))+P19(f5(f24(f21(a11,a2),a6),x781),f5(f24(f21(a17,a2),a6),x781))), % 0.59/0.68 inference(scs_inference,[],[1,64,3,8,20,42,49,56])). % 0.59/0.68 cnf(91,plain, % 0.59/0.68 (~P20(f9(a2,f8(f19(f18(a10,f24(f21(a11,a2),a6)),f24(f21(a17,a2),a6)),f20(f25(a12,a2),a6))),f20(f25(a12,a2),a6))), % 0.59/0.68 inference(scs_inference,[],[64,78,57])). % 0.59/0.68 cnf(92,plain, % 0.59/0.68 ($false), % 0.59/0.68 inference(scs_inference,[],[91,64,55]), % 0.59/0.68 ['proof']). % 0.59/0.68 % SZS output end Proof % 0.59/0.68 % Total time :0.020000s %------------------------------------------------------------------------------