%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : SYN710-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 : n028.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 1.12s 1.21s % Output : CNFRefutation 1.12s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.14 % Problem : SYN710-1 : TPTP v8.2.0. Released v2.5.0. % 0.08/0.14 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.13/0.35 % Computer : n028.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Mon Jun 24 00:07:38 EDT 2024 % 0.13/0.35 % CPUTime : % 0.46/0.59 start to proof:theBenchmark % 1.12/1.20 %------------------------------------------- % 1.12/1.20 % File :CSE---1.7 % 1.12/1.20 % Problem :theBenchmark % 1.12/1.20 % Transform :cnf % 1.12/1.20 % Format :tptp:raw % 1.12/1.20 % Command :java -jar mcs_scs.jar %d %s % 1.12/1.20 % 1.12/1.20 % Result :Theorem 0.560000s % 1.12/1.20 % Output :CNFRefutation 0.560000s % 1.12/1.20 %------------------------------------------- % 1.12/1.20 %-------------------------------------------------------------------------- % 1.12/1.20 % File : SYN710-1 : TPTP v8.2.0. Released v2.5.0. % 1.12/1.20 % Domain : Syntactic % 1.12/1.20 % Problem : Harrison problem 4703 % 1.12/1.20 % Version : Especial. % 1.12/1.20 % English : % 1.12/1.20 % 1.12/1.20 % Refs : [Har01] Email to G. Sutcliffe % 1.12/1.20 % Source : [Har01] % 1.12/1.20 % Names : % 1.12/1.20 % 1.12/1.20 % Status : Unsatisfiable % 1.12/1.20 % Rating : 0.00 v6.3.0, 0.14 v6.2.0, 0.00 v2.5.0 % 1.12/1.20 % Syntax : Number of clauses : 87 ( 26 unt; 12 nHn; 63 RR) % 1.12/1.20 % Number of literals : 211 ( 0 equ; 114 neg) % 1.12/1.20 % Maximal clause size : 4 ( 2 avg) % 1.12/1.20 % Maximal term depth : 4 ( 1 avg) % 1.12/1.20 % Number of predicates : 24 ( 24 usr; 0 prp; 2-2 aty) % 1.12/1.20 % Number of functors : 30 ( 30 usr; 18 con; 0-2 aty) % 1.12/1.20 % Number of variables : 198 ( 6 sgn) % 1.12/1.20 % SPC : CNF_UNS_RFO_NEQ_NHN % 1.12/1.20 % 1.12/1.20 % Comments : % 1.12/1.20 %-------------------------------------------------------------------------- % 1.12/1.20 cnf(p10_1,negated_conjecture, % 1.12/1.20 p10(X0,X0) ). % 1.12/1.20 % 1.12/1.20 cnf(p8_2,negated_conjecture, % 1.12/1.20 p8(X130,X130) ). % 1.12/1.20 % 1.12/1.20 cnf(p7_3,negated_conjecture, % 1.12/1.20 p7(X115,X115) ). % 1.12/1.20 % 1.12/1.20 cnf(p6_4,negated_conjecture, % 1.12/1.20 p6(X112,X112) ). % 1.12/1.20 % 1.12/1.20 cnf(p4_5,negated_conjecture, % 1.12/1.20 p4(X105,X105) ). % 1.12/1.20 % 1.12/1.20 cnf(p31_6,negated_conjecture, % 1.12/1.20 p31(X69,X69) ). % 1.12/1.20 % 1.12/1.20 cnf(p3_7,negated_conjecture, % 1.12/1.20 p3(X66,X66) ). % 1.12/1.20 % 1.12/1.20 cnf(p29_8,negated_conjecture, % 1.12/1.20 p29(X59,X59) ). % 1.12/1.20 % 1.12/1.20 cnf(p28_9,negated_conjecture, % 1.12/1.20 p28(X56,X56) ). % 1.12/1.20 % 1.12/1.20 cnf(p26_10,negated_conjecture, % 1.12/1.20 p26(X53,X53) ). % 1.12/1.20 % 1.12/1.20 cnf(p24_11,negated_conjecture, % 1.12/1.20 p24(X46,X46) ). % 1.12/1.20 % 1.12/1.20 cnf(p23_12,negated_conjecture, % 1.12/1.20 p23(X39,X39) ). % 1.12/1.20 % 1.12/1.20 cnf(p21_13,negated_conjecture, % 1.12/1.20 p21(X36,X36) ). % 1.12/1.20 % 1.12/1.20 cnf(p2_14,negated_conjecture, % 1.12/1.20 p2(X33,X33) ). % 1.12/1.20 % 1.12/1.20 cnf(p19_15,negated_conjecture, % 1.12/1.20 p19(X26,X26) ). % 1.12/1.20 % 1.12/1.20 cnf(p17_16,negated_conjecture, % 1.12/1.20 p17(X23,X23) ). % 1.12/1.20 % 1.12/1.20 cnf(p15_17,negated_conjecture, % 1.12/1.20 p15(X16,X16) ). % 1.12/1.20 % 1.12/1.20 cnf(p14_18,negated_conjecture, % 1.12/1.20 p14(X10,X10) ). % 1.12/1.20 % 1.12/1.20 cnf(p12_19,negated_conjecture, % 1.12/1.20 p12(X3,X3) ). % 1.12/1.20 % 1.12/1.20 cnf(p33_20,negated_conjecture, % 1.12/1.20 p33(c38,c39) ). % 1.12/1.20 % 1.12/1.20 cnf(p33_21,negated_conjecture, % 1.12/1.20 p33(c43,c45) ). % 1.12/1.20 % 1.12/1.20 cnf(not_p7_22,negated_conjecture, % 1.12/1.20 ~ p7(c43,c44) ). % 1.12/1.20 % 1.12/1.20 cnf(p34_23,negated_conjecture, % 1.12/1.20 p34(c40,f5(c41,c42)) ). % 1.12/1.20 % 1.12/1.20 cnf(p33_24,negated_conjecture, % 1.12/1.20 p33(f11(c46,c39),f9(c47,c43)) ). % 1.12/1.20 % 1.12/1.20 cnf(not_p33_25,negated_conjecture, % 1.12/1.20 ~ p33(f11(c46,c50),f9(c47,c43)) ). % 1.12/1.20 % 1.12/1.20 cnf(p37_26,negated_conjecture, % 1.12/1.20 ( p37(X96,X95) % 1.12/1.20 | ~ p35(f30(c53,X95),X96) ) ). % 1.12/1.20 % 1.12/1.20 cnf(p36_27,negated_conjecture, % 1.12/1.20 ( p36(X83,X82) % 1.12/1.20 | ~ p33(f18(c51,X82),X83) ) ). % 1.12/1.20 % 1.12/1.20 cnf(p33_28,negated_conjecture, % 1.12/1.20 ( p33(f18(c51,X82),X83) % 1.12/1.20 | ~ p36(X83,X82) ) ). % 1.12/1.20 % 1.12/1.20 cnf(p35_29,negated_conjecture, % 1.12/1.20 ( p35(f30(c53,X95),X96) % 1.12/1.20 | ~ p37(X96,X95) ) ). % 1.12/1.20 % 1.12/1.20 cnf(p10_30,negated_conjecture, % 1.12/1.20 ( p10(X1,X2) % 1.12/1.20 | ~ p10(X0,X1) % 1.12/1.20 | ~ p10(X0,X2) ) ). % 1.12/1.20 % 1.12/1.20 cnf(p8_31,negated_conjecture, % 1.12/1.20 ( p8(X131,X132) % 1.12/1.20 | ~ p8(X130,X131) % 1.12/1.20 | ~ p8(X130,X132) ) ). % 1.12/1.20 % 1.12/1.20 cnf(p7_32,negated_conjecture, % 1.12/1.20 ( p7(X116,X117) % 1.12/1.20 | ~ p7(X115,X116) % 1.12/1.20 | ~ p7(X115,X117) ) ). % 1.12/1.20 % 1.12/1.20 cnf(p6_33,negated_conjecture, % 1.12/1.20 ( p6(X113,X114) % 1.12/1.20 | ~ p6(X112,X113) % 1.12/1.20 | ~ p6(X112,X114) ) ). % 1.12/1.20 % 1.12/1.20 cnf(p4_34,negated_conjecture, % 1.12/1.20 ( p4(X106,X107) % 1.12/1.20 | ~ p4(X105,X106) % 1.12/1.20 | ~ p4(X105,X107) ) ). % 1.12/1.20 % 1.12/1.20 cnf(p31_35,negated_conjecture, % 1.12/1.20 ( p31(X70,X71) % 1.12/1.21 | ~ p31(X69,X70) % 1.12/1.21 | ~ p31(X69,X71) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p3_36,negated_conjecture, % 1.12/1.21 ( p3(X67,X68) % 1.12/1.21 | ~ p3(X66,X67) % 1.12/1.21 | ~ p3(X66,X68) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p29_37,negated_conjecture, % 1.12/1.21 ( p29(X60,X61) % 1.12/1.21 | ~ p29(X59,X60) % 1.12/1.21 | ~ p29(X59,X61) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p28_38,negated_conjecture, % 1.12/1.21 ( p28(X57,X58) % 1.12/1.21 | ~ p28(X56,X57) % 1.12/1.21 | ~ p28(X56,X58) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p26_39,negated_conjecture, % 1.12/1.21 ( p26(X54,X55) % 1.12/1.21 | ~ p26(X53,X54) % 1.12/1.21 | ~ p26(X53,X55) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p24_40,negated_conjecture, % 1.12/1.21 ( p24(X47,X48) % 1.12/1.21 | ~ p24(X46,X47) % 1.12/1.21 | ~ p24(X46,X48) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p23_41,negated_conjecture, % 1.12/1.21 ( p23(X40,X41) % 1.12/1.21 | ~ p23(X39,X40) % 1.12/1.21 | ~ p23(X39,X41) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p21_42,negated_conjecture, % 1.12/1.21 ( p21(X37,X38) % 1.12/1.21 | ~ p21(X36,X37) % 1.12/1.21 | ~ p21(X36,X38) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p2_43,negated_conjecture, % 1.12/1.21 ( p2(X34,X35) % 1.12/1.21 | ~ p2(X33,X34) % 1.12/1.21 | ~ p2(X33,X35) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p19_44,negated_conjecture, % 1.12/1.21 ( p19(X27,X28) % 1.12/1.21 | ~ p19(X26,X27) % 1.12/1.21 | ~ p19(X26,X28) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p17_45,negated_conjecture, % 1.12/1.21 ( p17(X24,X25) % 1.12/1.21 | ~ p17(X23,X25) % 1.12/1.21 | ~ p17(X23,X24) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p15_46,negated_conjecture, % 1.12/1.21 ( p15(X17,X18) % 1.12/1.21 | ~ p15(X16,X17) % 1.12/1.21 | ~ p15(X16,X18) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p14_47,negated_conjecture, % 1.12/1.21 ( p14(X11,X12) % 1.12/1.21 | ~ p14(X10,X11) % 1.12/1.21 | ~ p14(X10,X12) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p12_48,negated_conjecture, % 1.12/1.21 ( p12(X4,X5) % 1.12/1.21 | ~ p12(X3,X4) % 1.12/1.21 | ~ p12(X3,X5) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p33_49,negated_conjecture, % 1.12/1.21 ( p33(c38,X78) % 1.12/1.21 | ~ p33(f32(c55,f5(c41,c42)),X78) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p33_50,negated_conjecture, % 1.12/1.21 p33(f11(c46,f13(f16(c48,c49),c50)),f9(c47,c43)) ). % 1.12/1.21 % 1.12/1.21 cnf(p33_51,negated_conjecture, % 1.12/1.21 ( p33(f11(c46,c39),X78) % 1.12/1.21 | ~ p33(f32(c55,f5(c41,c42)),X78) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p35_52,negated_conjecture, % 1.12/1.21 ( p35(f30(c53,X92),f25(f27(c54,X94),X93)) % 1.12/1.21 | ~ p7(X92,X94) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p33_53,negated_conjecture, % 1.12/1.21 ( p33(f18(c51,X13),f13(f16(c48,X14),X15)) % 1.12/1.21 | ~ p15(X13,X14) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p33_54,negated_conjecture, % 1.12/1.21 ( p33(X72,X73) % 1.12/1.21 | ~ p7(X74,X72) % 1.12/1.21 | ~ p8(X75,X73) % 1.12/1.21 | ~ p33(X74,X75) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p37_55,negated_conjecture, % 1.12/1.21 ( p37(X101,X102) % 1.12/1.21 | ~ p37(X103,X104) % 1.12/1.21 | ~ p7(X104,X102) % 1.12/1.21 | ~ p24(X103,X101) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p36_56,negated_conjecture, % 1.12/1.21 ( p36(X97,X98) % 1.12/1.21 | ~ p36(X100,X99) % 1.12/1.21 | ~ p8(X100,X97) % 1.12/1.21 | ~ p15(X99,X98) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p35_57,negated_conjecture, % 1.12/1.21 ( p35(X88,X89) % 1.12/1.21 | ~ p29(X91,X88) % 1.12/1.21 | ~ p35(X91,X90) % 1.12/1.21 | ~ p24(X90,X89) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p34_58,negated_conjecture, % 1.12/1.21 ( p34(X84,X85) % 1.12/1.21 | ~ p34(X86,X87) % 1.12/1.21 | ~ p4(X87,X85) % 1.12/1.21 | ~ p3(X86,X84) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p33_59,negated_conjecture, % 1.12/1.21 ( p33(c38,X76) % 1.12/1.21 | p33(c38,X77) % 1.12/1.21 | ~ p33(c43,X76) % 1.12/1.21 | ~ p33(c43,X77) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p8_60,negated_conjecture, % 1.12/1.21 ( p8(f9(X137,X138),f9(X139,X140)) % 1.12/1.21 | ~ p6(X137,X139) % 1.12/1.21 | ~ p7(X138,X140) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p12_61,negated_conjecture, % 1.12/1.21 ( p12(f16(X6,X7),f16(X8,X9)) % 1.12/1.21 | ~ p14(X6,X8) % 1.12/1.21 | ~ p15(X7,X9) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p15_62,negated_conjecture, % 1.12/1.21 ( p15(f20(X19,X20),f20(X21,X22)) % 1.12/1.21 | ~ p19(X19,X21) % 1.12/1.21 | ~ p8(X20,X22) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p19_63,negated_conjecture, % 1.12/1.21 ( p19(f22(X29,X30),f22(X31,X32)) % 1.12/1.21 | ~ p21(X29,X31) % 1.12/1.21 | ~ p8(X30,X32) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p23_64,negated_conjecture, % 1.12/1.21 ( p23(f27(X42,X43),f27(X44,X45)) % 1.12/1.21 | ~ p26(X42,X44) % 1.12/1.21 | ~ p7(X43,X45) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p24_65,negated_conjecture, % 1.12/1.21 ( p24(f25(X49,X50),f25(X51,X52)) % 1.12/1.21 | ~ p23(X49,X51) % 1.12/1.21 | ~ p24(X50,X52) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p29_66,negated_conjecture, % 1.12/1.21 ( p29(f30(X62,X63),f30(X64,X65)) % 1.12/1.21 | ~ p28(X62,X64) % 1.12/1.21 | ~ p7(X63,X65) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p4_67,negated_conjecture, % 1.12/1.21 ( p4(f5(X108,X109),f5(X110,X111)) % 1.12/1.21 | ~ p2(X108,X110) % 1.12/1.21 | ~ p3(X109,X111) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p7_68,negated_conjecture, % 1.12/1.21 ( p7(f11(X118,X119),f11(X120,X121)) % 1.12/1.21 | ~ p10(X118,X120) % 1.12/1.21 | ~ p8(X119,X121) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p7_69,negated_conjecture, % 1.12/1.21 ( p7(f18(X122,X123),f18(X124,X125)) % 1.12/1.21 | ~ p15(X123,X125) % 1.12/1.21 | ~ p17(X122,X124) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p7_70,negated_conjecture, % 1.12/1.21 ( p7(f32(X126,X127),f32(X128,X129)) % 1.12/1.21 | ~ p31(X126,X128) % 1.12/1.21 | ~ p4(X127,X129) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p8_71,negated_conjecture, % 1.12/1.21 ( p8(f13(X133,X134),f13(X135,X136)) % 1.12/1.21 | ~ p12(X133,X135) % 1.12/1.21 | ~ p8(X134,X136) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p33_72,negated_conjecture, % 1.12/1.21 ( p33(f11(c46,X79),X80) % 1.12/1.21 | p33(f18(c51,f20(f22(c52,X79),X80)),X79) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p33_73,negated_conjecture, % 1.12/1.21 ( p33(f11(c46,X79),X80) % 1.12/1.21 | ~ p33(f18(c51,f20(f22(c52,X79),X80)),X80) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p35_74,negated_conjecture, % 1.12/1.21 ( p35(f30(c53,X92),f25(f27(c54,X94),X93)) % 1.12/1.21 | ~ p35(f30(c53,X92),X93) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p33_75,negated_conjecture, % 1.12/1.21 ( p33(f18(c51,X13),f13(f16(c48,X14),X15)) % 1.12/1.21 | ~ p33(f18(c51,X13),X15) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p33_76,negated_conjecture, % 1.12/1.21 ( p33(c38,X76) % 1.12/1.21 | p33(f11(c46,X76),X77) % 1.12/1.21 | ~ p33(c43,X76) % 1.12/1.21 | ~ p33(c43,X77) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p33_77,negated_conjecture, % 1.12/1.21 ( p33(c38,X77) % 1.12/1.21 | p33(f11(c46,X77),X76) % 1.12/1.21 | ~ p33(c43,X76) % 1.12/1.21 | ~ p33(c43,X77) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p33_78,negated_conjecture, % 1.12/1.21 ( p33(c38,X76) % 1.12/1.21 | p33(f11(c46,c39),X76) % 1.12/1.21 | ~ p33(c43,X76) % 1.12/1.21 | ~ p33(c43,X77) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p33_79,negated_conjecture, % 1.12/1.21 ( p33(c38,X77) % 1.12/1.21 | p33(f11(c46,c39),X77) % 1.12/1.21 | ~ p33(c43,X76) % 1.12/1.21 | ~ p33(c43,X77) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p33_80,negated_conjecture, % 1.12/1.21 ( p33(f18(c51,X81),X80) % 1.12/1.21 | ~ p33(f11(c46,X79),X80) % 1.12/1.21 | ~ p33(f18(c51,X81),X79) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p33_81,negated_conjecture, % 1.12/1.21 ( p33(f32(c55,f5(c41,c42)),X78) % 1.12/1.21 | ~ p33(c38,X78) % 1.12/1.21 | ~ p33(f11(c46,c39),X78) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p33_82,negated_conjecture, % 1.12/1.21 ( p33(f11(c46,X76),X77) % 1.12/1.21 | p33(f11(c46,X77),X76) % 1.12/1.21 | ~ p33(c43,X76) % 1.12/1.21 | ~ p33(c43,X77) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p33_83,negated_conjecture, % 1.12/1.21 ( p33(f11(c46,X76),X77) % 1.12/1.21 | p33(f11(c46,c39),X77) % 1.12/1.21 | ~ p33(c43,X76) % 1.12/1.21 | ~ p33(c43,X77) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p33_84,negated_conjecture, % 1.12/1.21 ( p33(f11(c46,X77),X76) % 1.12/1.21 | p33(f11(c46,c39),X76) % 1.12/1.21 | ~ p33(c43,X76) % 1.12/1.21 | ~ p33(c43,X77) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p33_85,negated_conjecture, % 1.12/1.21 ( p33(f11(c46,c39),X76) % 1.12/1.21 | p33(f11(c46,c39),X77) % 1.12/1.21 | ~ p33(c43,X76) % 1.12/1.21 | ~ p33(c43,X77) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p15_86,negated_conjecture, % 1.12/1.21 ( p15(X13,X14) % 1.12/1.21 | p33(f18(c51,X13),X15) % 1.12/1.21 | ~ p33(f18(c51,X13),f13(f16(c48,X14),X15)) ) ). % 1.12/1.21 % 1.12/1.21 cnf(p7_87,negated_conjecture, % 1.12/1.21 ( p7(X92,X94) % 1.12/1.21 | p35(f30(c53,X92),X93) % 1.12/1.21 | ~ p35(f30(c53,X92),f25(f27(c54,X94),X93)) ) ). % 1.12/1.21 % 1.12/1.21 %-------------------------------------------------------------------------- % 1.12/1.21 %------------------------------------------- % 1.12/1.21 % Proof found % 1.12/1.21 % SZS status Theorem for theBenchmark % 1.12/1.21 % SZS output start Proof % 1.12/1.21 %ClaNum:87(EqnAxiom:0) % 1.12/1.21 %VarNum:375(SingletonVarNum:186) % 1.12/1.21 %MaxLitNum:4 % 1.12/1.21 %MaxfuncDepth:3 % 1.12/1.21 %SharedTerms:33 % 1.12/1.21 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 60 61 62 63 64 65 66 67 68 69 70 71 72 75 76 77 78 79 80 81 82 83 84 85 86 87 % 1.12/1.21 %singleGoalClaCount:26 % 1.12/1.21 [1]P1(a1,a2) % 1.12/1.21 [2]P1(a3,a7) % 1.12/1.21 [25]~P18(a3,a8) % 1.12/1.21 [22]P21(a4,f9(a5,a6)) % 1.12/1.21 [23]P1(f11(a10,a2),f30(a12,a3)) % 1.12/1.21 [26]~P1(f11(a10,a15),f30(a12,a3)) % 1.12/1.21 [24]P1(f11(a10,f22(f21(a13,a14),a15)),f30(a12,a3)) % 1.12/1.21 [3]P2(x31,x31) % 1.12/1.21 [4]P17(x41,x41) % 1.12/1.21 [5]P18(x51,x51) % 1.12/1.21 [6]P19(x61,x61) % 1.12/1.21 [7]P20(x71,x71) % 1.12/1.21 [8]P3(x81,x81) % 1.12/1.21 [9]P4(x91,x91) % 1.12/1.21 [10]P5(x101,x101) % 1.12/1.21 [11]P6(x111,x111) % 1.12/1.21 [12]P7(x121,x121) % 1.12/1.21 [13]P8(x131,x131) % 1.12/1.21 [14]P9(x141,x141) % 1.12/1.21 [15]P10(x151,x151) % 1.12/1.21 [16]P11(x161,x161) % 1.12/1.21 [17]P12(x171,x171) % 1.12/1.21 [18]P13(x181,x181) % 1.12/1.21 [19]P14(x191,x191) % 1.12/1.21 [20]P15(x201,x201) % 1.12/1.21 [21]P16(x211,x211) % 1.12/1.21 [78]P1(a1,x781)+~P1(f29(a20,f9(a5,a6)),x781) % 1.12/1.21 [81]P1(f11(a10,a2),x811)+~P1(f29(a20,f9(a5,a6)),x811) % 1.12/1.21 [46]~P22(x462,x461)+P1(f23(a16,x461),x462) % 1.12/1.22 [47]~P24(x472,x471)+P23(f24(a17,x471),x472) % 1.12/1.22 [49]P24(x491,x492)+~P23(f24(a17,x492),x491) % 1.12/1.22 [50]P22(x501,x502)+~P1(f23(a16,x502),x501) % 1.12/1.22 [84]P1(f11(a10,x841),x842)+P1(f23(a16,f27(f26(a18,x841),x842)),x841) % 1.12/1.22 [87]P1(f11(a10,x871),x872)+~P1(f23(a16,f27(f26(a18,x871),x872)),x872) % 1.12/1.22 [76]~P14(x761,x762)+P1(f23(a16,x761),f22(f21(a13,x762),x763)) % 1.12/1.22 [77]~P18(x771,x772)+P23(f24(a17,x771),f25(f28(a19,x772),x773)) % 1.12/1.22 [82]~P1(f23(a16,x821),x823)+P1(f23(a16,x821),f22(f21(a13,x822),x823)) % 1.12/1.22 [83]~P23(f24(a17,x831),x833)+P23(f24(a17,x831),f25(f28(a19,x832),x833)) % 1.12/1.22 [79]~P1(a1,x791)+~P1(f11(a10,a2),x791)+P1(f29(a20,f9(a5,a6)),x791) % 1.12/1.22 [27]~P2(x273,x271)+P2(x271,x272)+~P2(x273,x272) % 1.12/1.22 [28]~P17(x283,x281)+P17(x281,x282)+~P17(x283,x282) % 1.12/1.22 [29]~P18(x293,x291)+P18(x291,x292)+~P18(x293,x292) % 1.12/1.22 [30]~P19(x303,x301)+P19(x301,x302)+~P19(x303,x302) % 1.12/1.22 [31]~P20(x313,x311)+P20(x311,x312)+~P20(x313,x312) % 1.12/1.22 [32]~P3(x323,x321)+P3(x321,x322)+~P3(x323,x322) % 1.12/1.22 [33]~P4(x333,x331)+P4(x331,x332)+~P4(x333,x332) % 1.12/1.22 [34]~P5(x343,x341)+P5(x341,x342)+~P5(x343,x342) % 1.12/1.22 [35]~P6(x353,x351)+P6(x351,x352)+~P6(x353,x352) % 1.12/1.22 [36]~P7(x363,x361)+P7(x361,x362)+~P7(x363,x362) % 1.12/1.22 [37]~P8(x373,x371)+P8(x371,x372)+~P8(x373,x372) % 1.12/1.22 [38]~P9(x383,x381)+P9(x381,x382)+~P9(x383,x382) % 1.12/1.22 [39]~P10(x393,x391)+P10(x391,x392)+~P10(x393,x392) % 1.12/1.22 [40]~P11(x403,x401)+P11(x401,x402)+~P11(x403,x402) % 1.12/1.22 [41]~P12(x413,x411)+P12(x411,x412)+~P12(x413,x412) % 1.12/1.22 [42]~P13(x423,x421)+P13(x421,x422)+~P13(x423,x422) % 1.12/1.22 [43]~P14(x433,x431)+P14(x431,x432)+~P14(x433,x432) % 1.12/1.22 [44]~P15(x443,x441)+P15(x441,x442)+~P15(x443,x442) % 1.12/1.22 [45]~P16(x453,x451)+P16(x451,x452)+~P16(x453,x452) % 1.12/1.22 [80]~P1(f23(a16,x801),x803)+P1(f23(a16,x801),x802)+~P1(f11(a10,x803),x802) % 1.12/1.22 [85]P18(x851,x852)+P23(f24(a17,x851),x853)+~P23(f24(a17,x851),f25(f28(a19,x852),x853)) % 1.12/1.22 [86]P14(x861,x862)+P1(f23(a16,x861),x863)+~P1(f23(a16,x861),f22(f21(a13,x862),x863)) % 1.12/1.22 [61]~P18(x612,x614)+~P19(x611,x613)+P17(f30(x611,x612),f30(x613,x614)) % 1.12/1.22 [62]~P17(x622,x624)+~P16(x621,x623)+P17(f22(x621,x622),f22(x623,x624)) % 1.12/1.22 [63]~P2(x631,x633)+~P17(x632,x634)+P18(f11(x631,x632),f11(x633,x634)) % 1.12/1.22 [64]~P13(x641,x643)+~P14(x642,x644)+P18(f23(x641,x642),f23(x643,x644)) % 1.12/1.22 [65]~P20(x652,x654)+~P3(x651,x653)+P18(f29(x651,x652),f29(x653,x654)) % 1.12/1.22 [66]~P4(x662,x664)+~P11(x661,x663)+P20(f9(x661,x662),f9(x663,x664)) % 1.12/1.22 [67]~P18(x672,x674)+~P6(x671,x673)+P5(f24(x671,x672),f24(x673,x674)) % 1.12/1.22 [68]~P8(x682,x684)+~P9(x681,x683)+P8(f25(x681,x682),f25(x683,x684)) % 1.12/1.22 [69]~P18(x692,x694)+~P7(x691,x693)+P9(f28(x691,x692),f28(x693,x694)) % 1.12/1.22 [70]~P17(x702,x704)+~P10(x701,x703)+P12(f26(x701,x702),f26(x703,x704)) % 1.12/1.22 [71]~P17(x712,x714)+~P12(x711,x713)+P14(f27(x711,x712),f27(x713,x714)) % 1.12/1.22 [72]~P14(x722,x724)+~P15(x721,x723)+P16(f21(x721,x722),f21(x723,x724)) % 1.12/1.22 [48]~P1(a3,x481)+~P1(a3,x482)+P1(a1,x481)+P1(a1,x482) % 1.12/1.22 [60]~P1(a3,x601)+~P1(a3,x602)+P1(f11(a10,a2),x602)+P1(f11(a10,a2),x601) % 1.12/1.22 [75]~P1(a3,x751)+~P1(a3,x752)+P1(f11(a10,x752),x751)+P1(f11(a10,x751),x752) % 1.12/1.22 [51]~P1(x514,x513)+P1(x511,x512)+~P17(x513,x512)+~P18(x514,x511) % 1.12/1.22 [52]~P21(x524,x523)+P21(x521,x522)+~P20(x523,x522)+~P4(x524,x521) % 1.12/1.22 [53]~P24(x534,x533)+P24(x531,x532)+~P18(x533,x532)+~P8(x534,x531) % 1.12/1.22 [54]~P23(x543,x544)+P23(x541,x542)+~P5(x543,x541)+~P8(x544,x542) % 1.12/1.22 [55]~P22(x553,x554)+P22(x551,x552)+~P17(x553,x551)+~P14(x554,x552) % 1.12/1.22 %EqnAxiom % 1.12/1.22 % 1.12/1.22 %------------------------------------------- % 1.12/1.22 cnf(97,plain, % 1.12/1.22 (P1(f23(a16,x971),f30(a12,a3))+~P1(f23(a16,x971),f22(f21(a13,a14),a15))), % 1.12/1.22 inference(scs_inference,[],[24,80])). % 1.12/1.22 cnf(505,plain, % 1.12/1.22 (~P1(f23(a16,f27(f26(a18,a15),f30(a12,a3))),f22(f21(a13,a14),a15))), % 1.12/1.22 inference(scs_inference,[],[26,97,87])). % 1.12/1.22 cnf(508,plain, % 1.12/1.22 ($false), % 1.12/1.22 inference(scs_inference,[],[505,26,82,84]), % 1.12/1.22 ['proof']). % 1.12/1.22 % SZS output end Proof % 1.12/1.22 % Total time :0.560000s %------------------------------------------------------------------------------