%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN709-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 : n001.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:22 EDT 2024 % Result : Unsatisfiable 0.50s 0.79s % Output : CNFRefutation 0.50s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.10 % Problem : SYN709-1 : TPTP v8.2.0. Released v2.5.0. % 0.06/0.10 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.10/0.31 % Computer : n001.cluster.edu % 0.10/0.31 % Model : x86_64 x86_64 % 0.10/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.31 % Memory : 8042.1875MB % 0.10/0.31 % OS : Linux 3.10.0-693.el7.x86_64 % 0.10/0.31 % CPULimit : 300 % 0.10/0.31 % WCLimit : 300 % 0.10/0.31 % DateTime : Sun Jun 23 19:42:39 EDT 2024 % 0.10/0.31 % CPUTime : % 0.16/0.53 start to proof:theBenchmark % 0.50/0.77 %------------------------------------------- % 0.50/0.77 % File :CSE---1.7 % 0.50/0.77 % Problem :theBenchmark % 0.50/0.77 % Transform :cnf % 0.50/0.77 % Format :tptp:raw % 0.50/0.77 % Command :java -jar mcs_scs.jar %d %s % 0.50/0.77 % 0.50/0.77 % Result :Theorem 0.190000s % 0.50/0.77 % Output :CNFRefutation 0.190000s % 0.50/0.77 %------------------------------------------- % 0.50/0.77 %-------------------------------------------------------------------------- % 0.50/0.77 % File : SYN709-1 : TPTP v8.2.0. Released v2.5.0. % 0.50/0.77 % Domain : Syntactic % 0.50/0.77 % Problem : Harrison problem 4692 % 0.50/0.77 % Version : Especial. % 0.50/0.77 % English : % 0.50/0.77 % 0.50/0.77 % Refs : [Har01] Email to G. Sutcliffe % 0.50/0.77 % Source : [Har01] % 0.50/0.77 % Names : % 0.50/0.77 % 0.50/0.77 % Status : Unsatisfiable % 0.50/0.77 % Rating : 0.00 v8.1.0, 0.25 v7.4.0, 0.17 v7.3.0, 0.25 v6.2.0, 0.17 v6.1.0, 0.07 v6.0.0, 0.11 v5.5.0, 0.06 v5.3.0, 0.15 v5.2.0, 0.08 v5.1.0, 0.06 v5.0.0, 0.07 v4.0.1, 0.14 v3.7.0, 0.00 v2.5.0 % 0.50/0.78 % Syntax : Number of clauses : 83 ( 35 unt; 0 nHn; 55 RR) % 0.50/0.78 % Number of literals : 181 ( 0 equ; 100 neg) % 0.50/0.78 % Maximal clause size : 4 ( 2 avg) % 0.50/0.78 % Maximal term depth : 5 ( 1 avg) % 0.50/0.78 % Number of predicates : 30 ( 30 usr; 0 prp; 2-2 aty) % 0.50/0.78 % Number of functors : 37 ( 37 usr; 21 con; 0-2 aty) % 0.50/0.78 % Number of variables : 193 ( 0 sgn) % 0.50/0.78 % SPC : CNF_UNS_RFO_NEQ_HRN % 0.50/0.78 % 0.50/0.78 % Comments : % 0.50/0.78 %-------------------------------------------------------------------------- % 0.50/0.78 cnf(p10_1,negated_conjecture, % 0.50/0.78 p10(X0,X0) ). % 0.50/0.78 % 0.50/0.78 cnf(p9_2,negated_conjecture, % 0.50/0.78 p9(X156,X156) ). % 0.50/0.78 % 0.50/0.78 cnf(p7_3,negated_conjecture, % 0.50/0.78 p7(X153,X153) ). % 0.50/0.78 % 0.50/0.78 cnf(p6_4,negated_conjecture, % 0.50/0.78 p6(X150,X150) ). % 0.50/0.78 % 0.50/0.78 cnf(p42_5,negated_conjecture, % 0.50/0.78 p42(X127,X127) ). % 0.50/0.78 % 0.50/0.78 cnf(p40_6,negated_conjecture, % 0.50/0.78 p40(X124,X124) ). % 0.50/0.78 % 0.50/0.78 cnf(p4_7,negated_conjecture, % 0.50/0.78 p4(X117,X117) ). % 0.50/0.78 % 0.50/0.78 cnf(p38_8,negated_conjecture, % 0.50/0.78 p38(X110,X110) ). % 0.50/0.78 % 0.50/0.78 cnf(p36_9,negated_conjecture, % 0.50/0.78 p36(X103,X103) ). % 0.50/0.78 % 0.50/0.78 cnf(p35_10,negated_conjecture, % 0.50/0.78 p35(X96,X96) ). % 0.50/0.78 % 0.50/0.78 cnf(p32_11,negated_conjecture, % 0.50/0.78 p32(X93,X93) ). % 0.50/0.78 % 0.50/0.78 cnf(p30_12,negated_conjecture, % 0.50/0.78 p30(X86,X86) ). % 0.50/0.78 % 0.50/0.78 cnf(p3_13,negated_conjecture, % 0.50/0.78 p3(X79,X79) ). % 0.50/0.78 % 0.50/0.78 cnf(p29_14,negated_conjecture, % 0.50/0.78 p29(X72,X72) ). % 0.50/0.78 % 0.50/0.78 cnf(p27_15,negated_conjecture, % 0.50/0.78 p27(X69,X69) ). % 0.50/0.78 % 0.50/0.78 cnf(p26_16,negated_conjecture, % 0.50/0.78 p26(X66,X66) ). % 0.50/0.78 % 0.50/0.78 cnf(p24_17,negated_conjecture, % 0.50/0.78 p24(X59,X59) ). % 0.50/0.78 % 0.50/0.78 cnf(p22_18,negated_conjecture, % 0.50/0.78 p22(X52,X52) ). % 0.50/0.78 % 0.50/0.78 cnf(p21_19,negated_conjecture, % 0.50/0.78 p21(X49,X49) ). % 0.50/0.78 % 0.50/0.78 cnf(p2_20,negated_conjecture, % 0.50/0.78 p2(X46,X46) ). % 0.50/0.78 % 0.50/0.78 cnf(p19_21,negated_conjecture, % 0.50/0.78 p19(X26,X26) ). % 0.50/0.78 % 0.50/0.78 cnf(p18_22,negated_conjecture, % 0.50/0.78 p18(X23,X23) ). % 0.50/0.78 % 0.50/0.78 cnf(p16_23,negated_conjecture, % 0.50/0.78 p16(X20,X20) ). % 0.50/0.78 % 0.50/0.78 cnf(p15_24,negated_conjecture, % 0.50/0.78 p15(X17,X17) ). % 0.50/0.78 % 0.50/0.78 cnf(p13_25,negated_conjecture, % 0.50/0.78 p13(X14,X14) ). % 0.50/0.78 % 0.50/0.78 cnf(p11_26,negated_conjecture, % 0.50/0.78 p11(X3,X3) ). % 0.50/0.78 % 0.50/0.78 cnf(p44_27,negated_conjecture, % 0.50/0.78 p44(c48,c49) ). % 0.50/0.78 % 0.50/0.78 cnf(p44_28,negated_conjecture, % 0.50/0.78 p44(c50,c49) ). % 0.50/0.78 % 0.50/0.78 cnf(p46_29,negated_conjecture, % 0.50/0.78 p46(f23(c58,c56),f20(c59,c60)) ). % 0.50/0.78 % 0.50/0.78 cnf(p44_30,negated_conjecture, % 0.50/0.78 p44(f5(c51,f8(c52,c53)),c49) ). % 0.50/0.78 % 0.50/0.78 cnf(p45_31,negated_conjecture, % 0.50/0.78 p45(f12(f14(c54,f17(c61,c49)),c56),c57) ). % 0.50/0.78 % 0.50/0.78 cnf(not_p45_32,negated_conjecture, % 0.50/0.78 ~ p45(f12(f14(c54,f17(c55,c49)),c56),c57) ). % 0.50/0.78 % 0.50/0.78 cnf(p10_33,negated_conjecture, % 0.50/0.78 ( p10(X1,X2) % 0.50/0.78 | ~ p10(X0,X2) % 0.50/0.78 | ~ p10(X0,X1) ) ). % 0.50/0.78 % 0.50/0.78 cnf(p9_34,negated_conjecture, % 0.50/0.78 ( p9(X157,X158) % 0.50/0.78 | ~ p9(X156,X157) % 0.50/0.78 | ~ p9(X156,X158) ) ). % 0.50/0.78 % 0.50/0.78 cnf(p7_35,negated_conjecture, % 0.50/0.78 ( p7(X154,X155) % 0.50/0.78 | ~ p7(X153,X154) % 0.50/0.78 | ~ p7(X153,X155) ) ). % 0.50/0.78 % 0.50/0.78 cnf(p6_36,negated_conjecture, % 0.50/0.78 ( p6(X151,X152) % 0.50/0.78 | ~ p6(X150,X151) % 0.50/0.78 | ~ p6(X150,X152) ) ). % 0.50/0.78 % 0.50/0.78 cnf(p42_37,negated_conjecture, % 0.50/0.78 ( p42(X128,X129) % 0.50/0.78 | ~ p42(X127,X128) % 0.50/0.78 | ~ p42(X127,X129) ) ). % 0.50/0.78 % 0.50/0.78 cnf(p40_38,negated_conjecture, % 0.50/0.78 ( p40(X125,X126) % 0.50/0.78 | ~ p40(X124,X125) % 0.50/0.78 | ~ p40(X124,X126) ) ). % 0.50/0.78 % 0.50/0.78 cnf(p4_39,negated_conjecture, % 0.50/0.78 ( p4(X118,X119) % 0.50/0.78 | ~ p4(X117,X118) % 0.50/0.78 | ~ p4(X117,X119) ) ). % 0.50/0.78 % 0.50/0.78 cnf(p38_40,negated_conjecture, % 0.50/0.78 ( p38(X111,X112) % 0.50/0.78 | ~ p38(X110,X111) % 0.50/0.78 | ~ p38(X110,X112) ) ). % 0.50/0.78 % 0.50/0.78 cnf(p36_41,negated_conjecture, % 0.50/0.78 ( p36(X104,X105) % 0.50/0.78 | ~ p36(X103,X104) % 0.50/0.78 | ~ p36(X103,X105) ) ). % 0.50/0.78 % 0.50/0.78 cnf(p35_42,negated_conjecture, % 0.50/0.78 ( p35(X97,X98) % 0.50/0.78 | ~ p35(X96,X97) % 0.50/0.78 | ~ p35(X96,X98) ) ). % 0.50/0.78 % 0.50/0.78 cnf(p32_43,negated_conjecture, % 0.50/0.78 ( p32(X94,X95) % 0.50/0.78 | ~ p32(X93,X94) % 0.50/0.78 | ~ p32(X93,X95) ) ). % 0.50/0.78 % 0.50/0.78 cnf(p30_44,negated_conjecture, % 0.50/0.78 ( p30(X87,X88) % 0.50/0.78 | ~ p30(X86,X87) % 0.50/0.78 | ~ p30(X86,X88) ) ). % 0.50/0.78 % 0.50/0.78 cnf(p3_45,negated_conjecture, % 0.50/0.78 ( p3(X80,X81) % 0.50/0.78 | ~ p3(X79,X80) % 0.50/0.78 | ~ p3(X79,X81) ) ). % 0.50/0.78 % 0.50/0.78 cnf(p29_46,negated_conjecture, % 0.50/0.78 ( p29(X73,X74) % 0.50/0.78 | ~ p29(X72,X73) % 0.50/0.78 | ~ p29(X72,X74) ) ). % 0.50/0.78 % 0.50/0.78 cnf(p27_47,negated_conjecture, % 0.50/0.78 ( p27(X70,X71) % 0.50/0.78 | ~ p27(X69,X70) % 0.50/0.78 | ~ p27(X69,X71) ) ). % 0.50/0.78 % 0.50/0.78 cnf(p26_48,negated_conjecture, % 0.50/0.78 ( p26(X67,X68) % 0.50/0.78 | ~ p26(X66,X67) % 0.50/0.78 | ~ p26(X66,X68) ) ). % 0.50/0.78 % 0.50/0.78 cnf(p24_49,negated_conjecture, % 0.50/0.78 ( p24(X60,X61) % 0.50/0.78 | ~ p24(X59,X60) % 0.50/0.78 | ~ p24(X59,X61) ) ). % 0.50/0.78 % 0.50/0.78 cnf(p22_50,negated_conjecture, % 0.50/0.78 ( p22(X53,X54) % 0.50/0.78 | ~ p22(X52,X53) % 0.50/0.78 | ~ p22(X52,X54) ) ). % 0.50/0.78 % 0.50/0.78 cnf(p21_51,negated_conjecture, % 0.50/0.78 ( p21(X50,X51) % 0.50/0.78 | ~ p21(X49,X50) % 0.50/0.78 | ~ p21(X49,X51) ) ). % 0.50/0.78 % 0.50/0.78 cnf(p2_52,negated_conjecture, % 0.50/0.78 ( p2(X47,X48) % 0.50/0.78 | ~ p2(X46,X47) % 0.50/0.78 | ~ p2(X46,X48) ) ). % 0.50/0.78 % 0.50/0.78 cnf(p19_53,negated_conjecture, % 0.50/0.78 ( p19(X27,X28) % 0.50/0.78 | ~ p19(X26,X27) % 0.50/0.78 | ~ p19(X26,X28) ) ). % 0.50/0.78 % 0.50/0.78 cnf(p18_54,negated_conjecture, % 0.50/0.78 ( p18(X24,X25) % 0.50/0.78 | ~ p18(X23,X24) % 0.50/0.78 | ~ p18(X23,X25) ) ). % 0.50/0.78 % 0.50/0.78 cnf(p16_55,negated_conjecture, % 0.50/0.78 ( p16(X21,X22) % 0.50/0.78 | ~ p16(X20,X21) % 0.50/0.78 | ~ p16(X20,X22) ) ). % 0.50/0.78 % 0.50/0.78 cnf(p15_56,negated_conjecture, % 0.50/0.78 ( p15(X18,X19) % 0.50/0.78 | ~ p15(X17,X18) % 0.50/0.78 | ~ p15(X17,X19) ) ). % 0.50/0.78 % 0.50/0.78 cnf(p13_57,negated_conjecture, % 0.50/0.78 ( p13(X15,X16) % 0.50/0.78 | ~ p13(X14,X15) % 0.50/0.78 | ~ p13(X14,X16) ) ). % 0.50/0.78 % 0.50/0.78 cnf(p11_58,negated_conjecture, % 0.50/0.78 ( p11(X4,X5) % 0.50/0.78 | ~ p11(X3,X4) % 0.50/0.78 | ~ p11(X3,X5) ) ). % 0.50/0.78 % 0.50/0.78 cnf(p19_59,negated_conjecture, % 0.50/0.78 p19(f25(f28(c64,X33),f34(c66,X34)),f34(X33,X34)) ). % 0.50/0.78 % 0.50/0.78 cnf(p47_60,negated_conjecture, % 0.50/0.78 ( p47(X142,X143) % 0.50/0.78 | ~ p30(X145,X142) % 0.50/0.78 | ~ p47(X145,X144) % 0.50/0.78 | ~ p19(X144,X143) ) ). % 0.50/0.78 % 0.50/0.78 cnf(p44_61,negated_conjecture, % 0.50/0.78 ( p44(X130,X131) % 0.50/0.78 | ~ p4(X133,X130) % 0.50/0.78 | ~ p44(X133,X132) % 0.50/0.78 | ~ p16(X132,X131) ) ). % 0.50/0.78 % 0.50/0.78 cnf(p45_62,negated_conjecture, % 0.50/0.78 ( p45(X134,X135) % 0.50/0.78 | ~ p11(X137,X134) % 0.50/0.78 | ~ p45(X137,X136) % 0.50/0.79 | ~ p10(X136,X135) ) ). % 0.50/0.79 % 0.50/0.79 cnf(p46_63,negated_conjecture, % 0.50/0.79 ( p46(X138,X139) % 0.50/0.79 | ~ p22(X141,X138) % 0.50/0.79 | ~ p46(X141,X140) % 0.50/0.79 | ~ p11(X140,X139) ) ). % 0.50/0.79 % 0.50/0.79 cnf(not_p47_64,negated_conjecture, % 0.50/0.79 ~ p47(f31(f33(c62,c63),f34(c65,c56)),f25(f28(c64,c65),c60)) ). % 0.50/0.79 % 0.50/0.79 cnf(p11_65,negated_conjecture, % 0.50/0.79 ( p11(f12(X6,X7),f12(X8,X9)) % 0.50/0.79 | ~ p10(X7,X9) % 0.50/0.79 | ~ p9(X6,X8) ) ). % 0.50/0.79 % 0.50/0.79 cnf(p9_66,negated_conjecture, % 0.50/0.79 ( p9(f17(X163,X164),f17(X165,X166)) % 0.50/0.79 | ~ p15(X163,X165) % 0.50/0.79 | ~ p16(X164,X166) ) ). % 0.50/0.79 % 0.50/0.79 cnf(p9_67,negated_conjecture, % 0.50/0.79 ( p9(f14(X159,X160),f14(X161,X162)) % 0.50/0.79 | ~ p13(X159,X161) % 0.50/0.79 | ~ p9(X160,X162) ) ). % 0.50/0.79 % 0.50/0.79 cnf(p4_68,negated_conjecture, % 0.50/0.79 ( p4(f5(X120,X121),f5(X122,X123)) % 0.50/0.79 | ~ p2(X120,X122) % 0.50/0.79 | ~ p3(X121,X123) ) ). % 0.50/0.79 % 0.50/0.79 cnf(p38_69,negated_conjecture, % 0.50/0.79 ( p38(f41(X113,X114),f41(X115,X116)) % 0.50/0.79 | ~ p24(X114,X116) % 0.50/0.79 | ~ p40(X113,X115) ) ). % 0.50/0.79 % 0.50/0.79 cnf(p36_70,negated_conjecture, % 0.50/0.79 ( p36(f39(X106,X107),f39(X108,X109)) % 0.50/0.79 | ~ p36(X107,X109) % 0.50/0.79 | ~ p38(X106,X108) ) ). % 0.50/0.79 % 0.50/0.79 cnf(p35_71,negated_conjecture, % 0.50/0.79 ( p35(f43(X99,X100),f43(X101,X102)) % 0.50/0.79 | ~ p10(X100,X102) % 0.50/0.79 | ~ p42(X99,X101) ) ). % 0.50/0.79 % 0.50/0.79 cnf(p30_72,negated_conjecture, % 0.50/0.79 ( p30(f31(X89,X90),f31(X91,X92)) % 0.50/0.79 | ~ p19(X90,X92) % 0.50/0.79 | ~ p29(X89,X91) ) ). % 0.50/0.79 % 0.50/0.79 cnf(p3_73,negated_conjecture, % 0.50/0.79 ( p3(f8(X82,X83),f8(X84,X85)) % 0.50/0.79 | ~ p6(X82,X84) % 0.50/0.79 | ~ p7(X83,X85) ) ). % 0.50/0.79 % 0.50/0.79 cnf(p29_74,negated_conjecture, % 0.50/0.79 ( p29(f33(X75,X76),f33(X77,X78)) % 0.50/0.79 | ~ p29(X76,X78) % 0.50/0.79 | ~ p32(X75,X77) ) ). % 0.50/0.79 % 0.50/0.79 cnf(p24_75,negated_conjecture, % 0.50/0.79 ( p24(f28(X62,X63),f28(X64,X65)) % 0.50/0.79 | ~ p26(X62,X64) % 0.50/0.79 | ~ p27(X63,X65) ) ). % 0.50/0.79 % 0.50/0.79 cnf(p22_76,negated_conjecture, % 0.50/0.79 ( p22(f23(X55,X56),f23(X57,X58)) % 0.50/0.79 | ~ p10(X56,X58) % 0.50/0.79 | ~ p21(X55,X57) ) ). % 0.50/0.79 % 0.50/0.79 cnf(p19_77,negated_conjecture, % 0.50/0.79 ( p19(f37(X42,X43),f37(X44,X45)) % 0.50/0.79 | ~ p35(X42,X44) % 0.50/0.79 | ~ p36(X43,X45) ) ). % 0.50/0.79 % 0.50/0.79 cnf(p19_78,negated_conjecture, % 0.50/0.79 ( p19(f34(X38,X39),f34(X40,X41)) % 0.50/0.79 | ~ p10(X39,X41) % 0.50/0.79 | ~ p27(X38,X40) ) ). % 0.50/0.79 % 0.50/0.79 cnf(p19_79,negated_conjecture, % 0.50/0.79 ( p19(f25(X29,X30),f25(X31,X32)) % 0.50/0.79 | ~ p19(X30,X32) % 0.50/0.79 | ~ p24(X29,X31) ) ). % 0.50/0.79 % 0.50/0.79 cnf(p11_80,negated_conjecture, % 0.50/0.79 ( p11(f20(X10,X11),f20(X12,X13)) % 0.50/0.79 | ~ p18(X10,X12) % 0.50/0.79 | ~ p19(X11,X13) ) ). % 0.50/0.79 % 0.50/0.79 cnf(p47_81,negated_conjecture, % 0.50/0.79 ( p47(f31(f33(c62,c63),f34(c66,X148)),X149) % 0.50/0.79 | ~ p46(f23(c58,X148),f20(c59,X149)) ) ). % 0.50/0.79 % 0.50/0.79 cnf(p19_82,negated_conjecture, % 0.50/0.79 p19(f25(f28(c64,X35),f37(f43(c67,X36),X37)),f37(f43(c67,X36),f39(f41(c68,f28(c64,X35)),X37))) ). % 0.50/0.79 % 0.50/0.79 cnf(p47_83,negated_conjecture, % 0.50/0.79 ( p47(f31(f33(c62,c63),f25(f28(c64,c65),X146)),f25(f28(c64,c65),X147)) % 0.50/0.79 | ~ p47(f31(f33(c62,c63),X146),X147) ) ). % 0.50/0.79 % 0.50/0.79 %-------------------------------------------------------------------------- % 0.50/0.79 %------------------------------------------- % 0.50/0.79 % Proof found % 0.50/0.79 % SZS status Theorem for theBenchmark % 0.50/0.79 % SZS output start Proof % 0.50/0.79 %ClaNum:83(EqnAxiom:0) % 0.50/0.79 %VarNum:386(SingletonVarNum:193) % 0.50/0.79 %MaxLitNum:4 % 0.50/0.79 %MaxfuncDepth:4 % 0.50/0.79 %SharedTerms:43 % 0.50/0.79 %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 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 % 0.50/0.79 %singleGoalClaCount:35 % 0.50/0.79 [1]P1(a1,a2) % 0.50/0.79 [2]P1(a3,a2) % 0.50/0.79 [29]P28(f12(a4,a5),f15(a13,a14)) % 0.50/0.79 [30]P1(f28(a6,f27(a7,a8)),a2) % 0.50/0.79 [35]~P30(f33(f32(a18,a19),f31(a21,a5)),f30(f29(a16,a21),a14)) % 0.50/0.79 [32]P29(f24(f23(a9,f22(a17,a2)),a5),a11) % 0.50/0.79 [34]~P29(f24(f23(a9,f22(a10,a2)),a5),a11) % 0.50/0.79 [3]P2(x31,x31) % 0.50/0.79 [4]P25(x41,x41) % 0.50/0.79 [5]P26(x51,x51) % 0.50/0.79 [6]P27(x61,x61) % 0.50/0.79 [7]P3(x71,x71) % 0.50/0.79 [8]P4(x81,x81) % 0.50/0.79 [9]P5(x91,x91) % 0.50/0.79 [10]P6(x101,x101) % 0.50/0.79 [11]P7(x111,x111) % 0.50/0.79 [12]P8(x121,x121) % 0.50/0.79 [13]P9(x131,x131) % 0.50/0.79 [14]P10(x141,x141) % 0.50/0.79 [15]P11(x151,x151) % 0.50/0.79 [16]P12(x161,x161) % 0.50/0.79 [17]P13(x171,x171) % 0.50/0.79 [18]P14(x181,x181) % 0.50/0.79 [19]P15(x191,x191) % 0.50/0.79 [20]P16(x201,x201) % 0.50/0.79 [21]P17(x211,x211) % 0.50/0.79 [22]P18(x221,x221) % 0.50/0.79 [23]P19(x231,x231) % 0.50/0.79 [24]P20(x241,x241) % 0.50/0.79 [25]P21(x251,x251) % 0.50/0.79 [26]P22(x261,x261) % 0.50/0.79 [27]P23(x271,x271) % 0.50/0.79 [28]P24(x281,x281) % 0.50/0.79 [31]P19(f30(f29(a16,x311),f31(a20,x312)),f31(x311,x312)) % 0.50/0.79 [33]P19(f30(f29(a16,x331),f35(f34(a25,x332),x333)),f35(f34(a25,x332),f37(f36(a26,f29(a16,x331)),x333))) % 0.50/0.79 [82]~P28(f12(a4,x821),f15(a13,x822))+P30(f33(f32(a18,a19),f31(a20,x821)),x822) % 0.50/0.79 [83]~P30(f33(f32(a18,a19),x831),x832)+P30(f33(f32(a18,a19),f30(f29(a16,a21),x831)),f30(f29(a16,a21),x832)) % 0.50/0.79 [36]~P2(x363,x361)+P2(x361,x362)+~P2(x363,x362) % 0.50/0.79 [37]~P25(x373,x371)+P25(x371,x372)+~P25(x373,x372) % 0.50/0.79 [38]~P26(x383,x381)+P26(x381,x382)+~P26(x383,x382) % 0.50/0.79 [39]~P27(x393,x391)+P27(x391,x392)+~P27(x393,x392) % 0.50/0.79 [40]~P3(x403,x401)+P3(x401,x402)+~P3(x403,x402) % 0.50/0.79 [41]~P4(x413,x411)+P4(x411,x412)+~P4(x413,x412) % 0.50/0.79 [42]~P5(x423,x421)+P5(x421,x422)+~P5(x423,x422) % 0.50/0.79 [43]~P6(x433,x431)+P6(x431,x432)+~P6(x433,x432) % 0.50/0.79 [44]~P7(x443,x441)+P7(x441,x442)+~P7(x443,x442) % 0.50/0.79 [45]~P8(x453,x451)+P8(x451,x452)+~P8(x453,x452) % 0.50/0.79 [46]~P9(x463,x461)+P9(x461,x462)+~P9(x463,x462) % 0.50/0.79 [47]~P10(x473,x471)+P10(x471,x472)+~P10(x473,x472) % 0.50/0.79 [48]~P11(x483,x481)+P11(x481,x482)+~P11(x483,x482) % 0.50/0.79 [49]~P12(x493,x491)+P12(x491,x492)+~P12(x493,x492) % 0.50/0.79 [50]~P13(x503,x501)+P13(x501,x502)+~P13(x503,x502) % 0.50/0.79 [51]~P14(x513,x511)+P14(x511,x512)+~P14(x513,x512) % 0.50/0.79 [52]~P15(x523,x521)+P15(x521,x522)+~P15(x523,x522) % 0.50/0.79 [53]~P16(x533,x531)+P16(x531,x532)+~P16(x533,x532) % 0.50/0.79 [54]~P17(x543,x541)+P17(x541,x542)+~P17(x543,x542) % 0.50/0.79 [55]~P18(x553,x551)+P18(x551,x552)+~P18(x553,x552) % 0.50/0.79 [56]~P19(x563,x561)+P19(x561,x562)+~P19(x563,x562) % 0.50/0.79 [57]~P20(x573,x571)+P20(x571,x572)+~P20(x573,x572) % 0.50/0.79 [58]~P21(x583,x581)+P21(x581,x582)+~P21(x583,x582) % 0.50/0.79 [59]~P22(x593,x591)+P22(x591,x592)+~P22(x593,x592) % 0.50/0.79 [60]~P23(x603,x601)+P23(x601,x602)+~P23(x603,x602) % 0.50/0.79 [61]~P24(x613,x611)+P24(x611,x612)+~P24(x613,x612) % 0.50/0.79 [66]~P21(x662,x664)+~P22(x661,x663)+P25(f22(x661,x662),f22(x663,x664)) % 0.50/0.79 [67]~P25(x672,x674)+~P23(x671,x673)+P25(f23(x671,x672),f23(x673,x674)) % 0.50/0.79 [68]~P11(x682,x684)+~P18(x681,x683)+P5(f28(x681,x682),f28(x683,x684)) % 0.50/0.79 [69]~P4(x691,x693)+~P15(x692,x694)+P6(f36(x691,x692),f36(x693,x694)) % 0.50/0.79 [70]~P6(x701,x703)+~P7(x702,x704)+P7(f37(x701,x702),f37(x703,x704)) % 0.50/0.79 [71]~P2(x712,x714)+~P3(x711,x713)+P8(f34(x711,x712),f34(x713,x714)) % 0.50/0.79 [72]~P12(x721,x723)+~P19(x722,x724)+P10(f33(x721,x722),f33(x723,x724)) % 0.50/0.79 [73]~P26(x732,x734)+~P27(x731,x733)+P11(f27(x731,x732),f27(x733,x734)) % 0.50/0.79 [74]~P9(x741,x743)+~P12(x742,x744)+P12(f32(x741,x742),f32(x743,x744)) % 0.50/0.79 [75]~P13(x752,x754)+~P14(x751,x753)+P15(f29(x751,x752),f29(x753,x754)) % 0.50/0.79 [76]~P2(x762,x764)+~P17(x761,x763)+P16(f12(x761,x762),f12(x763,x764)) % 0.50/0.79 [77]~P2(x772,x774)+~P13(x771,x773)+P19(f31(x771,x772),f31(x773,x774)) % 0.50/0.79 [78]~P15(x781,x783)+~P19(x782,x784)+P19(f30(x781,x782),f30(x783,x784)) % 0.50/0.79 [79]~P7(x792,x794)+~P8(x791,x793)+P19(f35(x791,x792),f35(x793,x794)) % 0.50/0.79 [80]~P19(x802,x804)+~P20(x801,x803)+P24(f15(x801,x802),f15(x803,x804)) % 0.50/0.79 [81]~P2(x812,x814)+~P25(x811,x813)+P24(f24(x811,x812),f24(x813,x814)) % 0.50/0.79 [62]~P1(x623,x624)+P1(x621,x622)+~P5(x623,x621)+~P21(x624,x622) % 0.50/0.79 [63]~P28(x633,x634)+P28(x631,x632)+~P16(x633,x631)+~P24(x634,x632) % 0.50/0.79 [64]~P29(x644,x643)+P29(x641,x642)+~P2(x643,x642)+~P24(x644,x641) % 0.50/0.79 [65]~P30(x653,x654)+P30(x651,x652)+~P10(x653,x651)+~P19(x654,x652) % 0.50/0.79 %EqnAxiom % 0.50/0.79 % 0.50/0.79 %------------------------------------------- % 0.50/0.79 cnf(84,plain, % 0.50/0.79 (P30(f33(f32(a18,a19),f30(f29(a16,a21),f31(a20,a5))),f30(f29(a16,a21),a14))), % 0.50/0.79 inference(scs_inference,[],[29,82,83])). % 0.50/0.79 cnf(85,plain, % 0.50/0.79 (P19(f31(x851,x852),f30(f29(a16,x851),f31(a20,x852)))), % 0.50/0.79 inference(scs_inference,[],[31,23,56])). % 0.50/0.79 cnf(122,plain, % 0.50/0.79 (P10(f33(x1221,f31(x1222,x1223)),f33(x1221,f30(f29(a16,x1222),f31(a20,x1223))))), % 0.50/0.79 inference(scs_inference,[],[85,16,72,49])). % 0.50/0.79 cnf(130,plain, % 0.50/0.79 (P10(f33(x1301,f30(f29(a16,x1302),f31(a20,x1303))),f33(x1301,f31(x1302,x1303)))), % 0.50/0.79 inference(scs_inference,[],[122,14,47])). % 0.50/0.79 cnf(148,plain, % 0.50/0.79 ($false), % 0.50/0.79 inference(scs_inference,[],[23,130,84,35,65]), % 0.50/0.79 ['proof']). % 0.50/0.79 % SZS output end Proof % 0.50/0.79 % Total time :0.190000s %------------------------------------------------------------------------------