%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LCL668+1.001 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % Computer : n006.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8046.5625MB % OS : Linux 6.8.0-71-generic % CPULimit : 300s % WCLimit : 300s % DateTime : Mon Sep 7 11:19:33 AM UTC 2026 % Result : Theorem 11.44s 11.65s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL668+1.001 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.03 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.10/0.35 % Computer : n006.cluster.edu % 0.10/0.35 % Model : x86_64 x86_64 % 0.10/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.35 % Memory : 8046.5625MB % 0.10/0.35 % OS : Linux 6.8.0-71-generic % 0.10/0.35 % CPULimit : 300 % 0.10/0.35 % WCLimit : 300 % 0.10/0.35 % DateTime : Sat Sep 5 07:03:01 UTC 2026 % 0.10/0.35 % CPUTime : % 0.23/0.51 start to proof:theBenchmark % 11.44/11.63 %------------------------------------------- % 11.44/11.63 % File :CSE---1.7 % 11.44/11.63 % Problem :theBenchmark % 11.44/11.63 % Transform :cnf % 11.44/11.63 % Format :tptp:raw % 11.44/11.63 % Command :java -jar mcs_scs.jar %d %s % 11.44/11.63 % 11.44/11.63 % Result :Theorem 11.122023s % 11.44/11.63 % Output :CNFRefutation 11.122023s % 11.44/11.63 %------------------------------------------- % 11.44/11.63 %------------------------------------------------------------------------------ % 11.44/11.63 % File : LCL668+1.001 : TPTP v9.3.1. Released v4.0.0. % 11.44/11.63 % Domain : Logic Calculi (Modal Logic) % 11.44/11.63 % Problem : In KT, black and white polygon with odd number of vertices, size 1 % 11.44/11.63 % Version : Especial. % 11.44/11.63 % English : If we have a polygon with n vertices, and all the vertices are % 11.44/11.64 % either black or white, then two adjacent vertices have the same % 11.44/11.64 % colour. % 11.44/11.64 % 11.44/11.64 % Refs : [BHS00] Balsiger et al. (2000), A Benchmark Method for the Pro % 11.44/11.64 % : [Kam08] Kaminski (2008), Email to G. Sutcliffe % 11.44/11.64 % Source : [Kam08] % 11.44/11.64 % Names : kt_poly_p [BHS00] % 11.44/11.64 % 11.44/11.64 % Status : Theorem % 11.44/11.64 % Rating : 0.00 v9.3.0, 0.10 v9.1.0, 0.13 v9.0.0, 0.00 v7.5.0, 0.14 v7.4.0, 0.00 v7.0.0, 0.07 v6.4.0, 0.00 v6.2.0, 0.09 v6.1.0, 0.16 v6.0.0, 0.25 v5.5.0, 0.33 v5.4.0, 0.30 v5.2.0, 0.07 v5.0.0, 0.25 v4.1.0, 0.28 v4.0.1, 0.26 v4.0.0 % 11.44/11.64 % Syntax : Number of formulae : 2 ( 1 unt; 0 def) % 11.44/11.64 % Number of atoms : 85 ( 0 equ) % 11.44/11.64 % Maximal formula atoms : 84 ( 42 avg) % 11.44/11.64 % Number of connectives : 168 ( 85 ~; 63 |; 20 &) % 11.44/11.64 % ( 0 <=>; 0 =>; 0 <=; 0 <~>) % 11.44/11.64 % Maximal formula depth : 46 ( 24 avg) % 11.44/11.64 % Maximal term depth : 1 ( 1 avg) % 11.44/11.64 % Number of predicates : 11 ( 11 usr; 0 prp; 1-2 aty) % 11.44/11.64 % Number of functors : 0 ( 0 usr; 0 con; --- aty) % 11.44/11.64 % Number of variables : 49 ( 48 !; 1 ?) % 11.44/11.64 % SPC : FOF_THM_RFO_NEQ % 11.44/11.64 % 11.44/11.64 % Comments : A naive relational encoding of the modal logic problem into % 11.44/11.64 % first-order logic. % 11.44/11.64 %------------------------------------------------------------------------------ % 11.44/11.64 fof(reflexivity,axiom, % 11.44/11.64 ! [X] : r1(X,X) ). % 11.44/11.64 % 11.44/11.64 fof(main,conjecture, % 11.44/11.64 ~ ? [X] : % 11.44/11.64 ~ ( ! [Y] : % 11.44/11.64 ( ~ r1(X,Y) % 11.44/11.64 | ! [X] : % 11.44/11.64 ( ~ r1(Y,X) % 11.44/11.64 | ! [Y] : % 11.44/11.64 ( ~ r1(X,Y) % 11.44/11.64 | ! [X] : % 11.44/11.64 ( ~ r1(Y,X) % 11.44/11.64 | ! [Y] : % 11.44/11.64 ( ~ r1(X,Y) % 11.44/11.64 | ! [X] : % 11.44/11.64 ( ~ r1(Y,X) % 11.44/11.64 | ( ~ p12(X) % 11.44/11.64 & ~ p10(X) % 11.44/11.64 & ~ p8(X) % 11.44/11.64 & ~ p6(X) % 11.44/11.64 & ~ p4(X) % 11.44/11.64 & ~ p2(X) ) ) ) ) ) ) ) % 11.44/11.64 | ! [Y] : % 11.44/11.64 ( ~ r1(X,Y) % 11.44/11.64 | p7(Y) ) % 11.44/11.64 | ~ ! [Y] : % 11.44/11.64 ( ~ r1(X,Y) % 11.44/11.64 | ~ ( ~ ! [X] : % 11.44/11.64 ( ~ r1(Y,X) % 11.44/11.64 | ! [Y] : % 11.44/11.64 ( ~ r1(X,Y) % 11.44/11.64 | ! [X] : % 11.44/11.64 ( ~ r1(Y,X) % 11.44/11.64 | ! [Y] : % 11.44/11.64 ( ~ r1(X,Y) % 11.44/11.64 | ! [X] : % 11.44/11.64 ( ~ r1(Y,X) % 11.44/11.64 | ! [Y] : % 11.44/11.64 ( ~ r1(X,Y) % 11.44/11.64 | ! [X] : % 11.44/11.64 ( ~ r1(Y,X) % 11.44/11.64 | ~ ( ( ~ p5(X) % 11.44/11.64 & ~ p1(X) ) % 11.44/11.64 | ( p1(X) % 11.44/11.64 & p5(X) ) ) ) ) ) ) ) ) ) % 11.44/11.64 | ! [X] : % 11.44/11.64 ( ~ r1(Y,X) % 11.44/11.64 | p6(X) ) % 11.44/11.64 | ~ ! [X] : % 11.44/11.64 ( ~ r1(Y,X) % 11.44/11.64 | ~ ( ~ ! [Y] : % 11.44/11.64 ( ~ r1(X,Y) % 11.44/11.64 | ! [X] : % 11.44/11.64 ( ~ r1(Y,X) % 11.44/11.64 | ! [Y] : % 11.44/11.64 ( ~ r1(X,Y) % 11.44/11.64 | ! [X] : % 11.44/11.64 ( ~ r1(Y,X) % 11.44/11.64 | ! [Y] : % 11.44/11.64 ( ~ r1(X,Y) % 11.44/11.64 | ! [X] : % 11.44/11.64 ( ~ r1(Y,X) % 11.44/11.64 | ~ ( ( ~ p4(X) % 11.44/11.64 & ~ p5(X) ) % 11.44/11.64 | ( p5(X) % 11.44/11.64 & p4(X) ) ) ) ) ) ) ) ) % 11.44/11.64 | ! [Y] : % 11.44/11.64 ( ~ r1(X,Y) % 11.44/11.64 | p5(Y) ) % 11.44/11.64 | ~ ! [Y] : % 11.44/11.64 ( ~ r1(X,Y) % 11.44/11.64 | ~ ( ~ ! [X] : % 11.44/11.64 ( ~ r1(Y,X) % 11.44/11.65 | ! [Y] : % 11.44/11.65 ( ~ r1(X,Y) % 11.44/11.65 | ! [X] : % 11.44/11.65 ( ~ r1(Y,X) % 11.44/11.65 | ! [Y] : % 11.44/11.65 ( ~ r1(X,Y) % 11.44/11.65 | ! [X] : % 11.44/11.65 ( ~ r1(Y,X) % 11.44/11.65 | ~ ( ( ~ p3(X) % 11.44/11.65 & ~ p4(X) ) % 11.44/11.65 | ( p4(X) % 11.44/11.65 & p3(X) ) ) ) ) ) ) ) % 11.44/11.65 | ! [X] : % 11.44/11.65 ( ~ r1(Y,X) % 11.44/11.65 | p4(X) ) % 11.44/11.65 | ~ ! [X] : % 11.44/11.65 ( ~ r1(Y,X) % 11.44/11.65 | ~ ( ~ ! [Y] : % 11.44/11.65 ( ~ r1(X,Y) % 11.44/11.65 | ! [X] : % 11.44/11.65 ( ~ r1(Y,X) % 11.44/11.65 | ! [Y] : % 11.44/11.65 ( ~ r1(X,Y) % 11.44/11.65 | ! [X] : % 11.44/11.65 ( ~ r1(Y,X) % 11.44/11.65 | ~ ( ( ~ p2(X) % 11.44/11.65 & ~ p3(X) ) % 11.44/11.65 | ( p3(X) % 11.44/11.65 & p2(X) ) ) ) ) ) ) % 11.44/11.65 | ! [Y] : % 11.44/11.65 ( ~ r1(X,Y) % 11.44/11.65 | p3(Y) ) % 11.44/11.65 | ~ ! [Y] : % 11.44/11.65 ( ~ r1(X,Y) % 11.44/11.65 | ~ ~ ! [X] : % 11.44/11.65 ( ~ r1(Y,X) % 11.44/11.65 | ! [Y] : % 11.44/11.65 ( ~ r1(X,Y) % 11.44/11.65 | ! [X] : % 11.44/11.65 ( ~ r1(Y,X) % 11.44/11.65 | ~ ( ( ~ p1(X) % 11.44/11.65 & ~ p2(X) ) % 11.44/11.65 | ( p2(X) % 11.44/11.65 & p1(X) ) ) ) ) ) ) ) ) ) ) ) ) ) ) % 11.44/11.65 | ! [Y] : % 11.44/11.65 ( ~ r1(X,Y) % 11.44/11.65 | ! [X] : % 11.44/11.65 ( ~ r1(Y,X) % 11.44/11.65 | ! [Y] : % 11.44/11.65 ( ~ r1(X,Y) % 11.44/11.65 | ! [X] : % 11.44/11.65 ( ~ r1(Y,X) % 11.44/11.65 | ! [Y] : % 11.44/11.65 ( ~ r1(X,Y) % 11.44/11.65 | ! [X] : % 11.44/11.65 ( ~ r1(Y,X) % 11.44/11.65 | ( p6(X) % 11.44/11.65 & p5(X) % 11.44/11.65 & p4(X) % 11.44/11.65 & p3(X) % 11.44/11.65 & p2(X) % 11.44/11.65 & p1(X) ) ) ) ) ) ) ) ) ). % 11.44/11.65 % 11.44/11.65 %------------------------------------------------------------------------------ % 11.44/11.65 %------------------------------------------- % 11.44/11.65 % Proof found % 11.44/11.65 % SZS status Theorem for theBenchmark % 11.44/11.65 % SZS output start Proof % 11.44/11.65 %ClaNum:35(EqnAxiom:0) % 11.44/11.65 %VarNum:228(SingletonVarNum:101) % 11.44/11.65 %MaxLitNum:10 % 11.44/11.65 %MaxfuncDepth:1 % 11.44/11.65 %SharedTerms:40 % 11.44/11.65 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 12 13 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 % 11.44/11.65 %singleGoalClaCount:14 % 11.44/11.65 [1]P1(a1,a11) % 11.44/11.65 [2]P1(a1,a12) % 11.44/11.65 [3]P1(a1,a2) % 11.44/11.65 [4]P1(a11,a13) % 11.44/11.65 [5]P1(a13,a14) % 11.44/11.65 [6]P1(a14,a15) % 11.44/11.65 [7]P1(a15,a16) % 11.44/11.65 [8]P1(a16,a17) % 11.44/11.65 [9]P1(a2,a6) % 11.44/11.65 [10]P1(a6,a7) % 11.44/11.65 [11]P1(a7,a8) % 11.44/11.65 [12]P1(a8,a9) % 11.44/11.65 [13]P1(a9,a10) % 11.44/11.65 [15]~P2(a12) % 11.44/11.65 [14]P1(x141,x141) % 11.44/11.65 [18]~P1(a1,x181)+~P6(f18(x181)) % 11.44/11.65 [19]~P1(a1,x191)+P1(x191,f18(x191)) % 11.44/11.65 [20]~P1(x202,x201)+~P1(a1,x202)+P1(x201,f3(x202,x201)) % 11.44/11.65 [21]~P1(x211,x212)+~P1(a1,x211)+~P10(f3(x211,x212)) % 11.44/11.65 [22]~P1(x223,x221)+~P1(x222,x223)+~P1(a1,x222)+P1(x221,f4(x222,x223,x221)) % 11.44/11.65 [33]~P1(x331,x332)+~P1(x333,x331)+~P1(a1,x333)+~P7(f4(x333,x331,x332)) % 11.44/11.65 [34]~P1(x344,x341)+~P1(x343,x344)+~P1(x342,x343)+~P1(a1,x342)+P1(x341,f5(x342,x343,x344,x341)) % 11.44/11.65 [35]~P1(x351,x352)+~P1(x353,x351)+~P1(x354,x353)+~P1(a1,x354)+~P9(f5(x354,x353,x351,x352)) % 11.44/11.65 [16]P3(a17)+P4(a17)+P11(a17)+P6(a17)+P7(a17)+P8(a17) % 11.44/11.65 [17]~P6(a10)+~P7(a10)+~P8(a10)+~P10(a10)+~P5(a10)+~P9(a10) % 11.44/11.65 [23]P10(x231)+~P1(x238,x231)+P7(x231)+~P1(x232,x233)+~P1(x233,x234)+~P1(x234,x235)+~P1(x235,x236)+~P1(x236,x237)+~P1(x237,x238)+~P1(a1,x232) % 11.44/11.65 [24]P9(x241)+~P1(x248,x241)+P7(x241)+~P1(x242,x243)+~P1(x243,x244)+~P1(x244,x245)+~P1(x245,x246)+~P1(x246,x247)+~P1(x247,x248)+~P1(a1,x242) % 11.44/11.65 [25]P5(x251)+~P1(x258,x251)+P8(x251)+~P1(x252,x253)+~P1(x253,x254)+~P1(x254,x255)+~P1(x255,x256)+~P1(x256,x257)+~P1(x257,x258)+~P1(a1,x252) % 11.44/11.65 [26]P9(x261)+~P1(x268,x261)+P8(x261)+~P1(x262,x263)+~P1(x263,x264)+~P1(x264,x265)+~P1(x265,x266)+~P1(x266,x267)+~P1(x267,x268)+~P1(a1,x262) % 11.44/11.65 [27]P5(x271)+~P1(x278,x271)+P10(x271)+~P1(x272,x273)+~P1(x273,x274)+~P1(x274,x275)+~P1(x275,x276)+~P1(x276,x277)+~P1(x277,x278)+~P1(a1,x272) % 11.44/11.65 [28]~P10(x281)+~P1(x288,x281)+~P7(x281)+~P1(x282,x283)+~P1(x283,x284)+~P1(x284,x285)+~P1(x285,x286)+~P1(x286,x287)+~P1(x287,x288)+~P1(a1,x282) % 11.44/11.65 [29]~P9(x291)+~P1(x298,x291)+~P7(x291)+~P1(x292,x293)+~P1(x293,x294)+~P1(x294,x295)+~P1(x295,x296)+~P1(x296,x297)+~P1(x297,x298)+~P1(a1,x292) % 11.44/11.65 [30]~P5(x301)+~P1(x308,x301)+~P8(x301)+~P1(x302,x303)+~P1(x303,x304)+~P1(x304,x305)+~P1(x305,x306)+~P1(x306,x307)+~P1(x307,x308)+~P1(a1,x302) % 11.44/11.65 [31]~P9(x311)+~P1(x318,x311)+~P8(x311)+~P1(x312,x313)+~P1(x313,x314)+~P1(x314,x315)+~P1(x315,x316)+~P1(x316,x317)+~P1(x317,x318)+~P1(a1,x312) % 11.44/11.65 [32]~P5(x321)+~P1(x328,x321)+~P10(x321)+~P1(x322,x323)+~P1(x323,x324)+~P1(x324,x325)+~P1(x325,x326)+~P1(x326,x327)+~P1(x327,x328)+~P1(a1,x322) % 11.44/11.65 %EqnAxiom % 11.44/11.65 % 11.44/11.65 %------------------------------------------- % 11.44/11.65 cnf(39,plain, % 11.44/11.65 (P1(x391,x391)), % 11.44/11.65 inference(rename_variables,[],[14])). % 11.44/11.65 cnf(41,plain, % 11.44/11.65 (P1(a1,f5(a1,a1,a1,a1))), % 11.44/11.65 inference(scs_inference,[],[1,4,14,39,20,22,34])). % 11.44/11.65 cnf(250,plain, % 11.44/11.65 (~P10(f3(a11,f18(a11)))), % 11.44/11.65 inference(scs_inference,[],[1,21,19])). % 11.44/11.65 cnf(1738,plain, % 11.44/11.65 (~P7(f4(a12,a12,f18(a12)))), % 11.44/11.65 inference(scs_inference,[],[2,14,19,33])). % 11.44/11.65 cnf(8868,plain, % 11.44/11.65 (P1(x88681,x88681)), % 11.44/11.65 inference(rename_variables,[],[14])). % 11.44/11.65 cnf(8872,plain, % 11.44/11.65 (P1(x88721,x88721)), % 11.44/11.65 inference(rename_variables,[],[14])). % 11.44/11.65 cnf(8875,plain, % 11.44/11.65 (P1(x88751,x88751)), % 11.44/11.65 inference(rename_variables,[],[14])). % 11.44/11.65 cnf(8878,plain, % 11.44/11.65 (P1(x88781,x88781)), % 11.44/11.66 inference(rename_variables,[],[14])). % 11.44/11.66 cnf(8881,plain, % 11.44/11.66 (P1(x88811,x88811)), % 11.44/11.66 inference(rename_variables,[],[14])). % 11.44/11.66 cnf(8883,plain, % 11.44/11.66 (P8(a1)+P5(a1)), % 11.44/11.66 inference(scs_inference,[],[14,8868,8872,8875,8878,8881,1,250,1738,20,22,34,24,27,25])). % 11.44/11.66 cnf(8884,plain, % 11.44/11.66 (P1(x88841,x88841)), % 11.44/11.66 inference(rename_variables,[],[14])). % 11.44/11.66 cnf(8886,plain, % 11.44/11.66 (P8(a1)+P9(a1)), % 11.44/11.66 inference(scs_inference,[],[14,8868,8872,8875,8878,8881,8884,1,250,1738,20,22,34,24,27,25,26])). % 11.44/11.66 cnf(8887,plain, % 11.44/11.66 (P1(x88871,x88871)), % 11.44/11.66 inference(rename_variables,[],[14])). % 11.44/11.66 cnf(8889,plain, % 11.44/11.66 (~P7(a1)+~P10(a1)), % 11.44/11.66 inference(scs_inference,[],[14,8868,8872,8875,8878,8881,8884,8887,1,250,1738,20,22,34,24,27,25,26,28])). % 11.44/11.66 cnf(8893,plain, % 11.44/11.66 (P1(x88931,x88931)), % 11.44/11.66 inference(rename_variables,[],[14])). % 11.44/11.66 cnf(8897,plain, % 11.44/11.66 (P1(x88971,x88971)), % 11.44/11.66 inference(rename_variables,[],[14])). % 11.44/11.66 cnf(8900,plain, % 11.44/11.66 (P1(x89001,x89001)), % 11.44/11.66 inference(rename_variables,[],[14])). % 11.44/11.66 cnf(8902,plain, % 11.44/11.66 (~P7(a1)+~P9(a1)), % 11.44/11.66 inference(scs_inference,[],[14,8893,8897,8900,1,2,3,20,22,34,29])). % 11.44/11.66 cnf(8903,plain, % 11.44/11.66 (P1(x89031,x89031)), % 11.44/11.66 inference(rename_variables,[],[14])). % 11.44/11.66 cnf(8905,plain, % 11.44/11.66 (~P8(a1)+~P9(a1)), % 11.44/11.66 inference(scs_inference,[],[14,8893,8897,8900,8903,1,2,3,20,22,34,29,31])). % 11.44/11.66 cnf(8906,plain, % 11.44/11.66 (P1(x89061,x89061)), % 11.44/11.66 inference(rename_variables,[],[14])). % 11.44/11.66 cnf(8908,plain, % 11.44/11.66 (~P8(a1)+~P5(a1)), % 11.44/11.66 inference(scs_inference,[],[14,8893,8897,8900,8903,8906,1,2,3,20,22,34,29,31,30])). % 11.44/11.66 cnf(8963,plain, % 11.44/11.66 (P1(x89631,x89631)), % 11.44/11.66 inference(rename_variables,[],[14])). % 11.44/11.66 cnf(8966,plain, % 11.44/11.66 (P1(x89661,x89661)), % 11.44/11.66 inference(rename_variables,[],[14])). % 11.44/11.66 cnf(8968,plain, % 11.44/11.66 (~P10(a1)+~P5(a1)), % 11.44/11.66 inference(scs_inference,[],[14,8963,8966,1,41,22,34,32])). % 11.44/11.66 cnf(9672,plain, % 11.44/11.66 (P9(a1)+~P10(a1)), % 11.44/11.66 inference(scs_inference,[],[14,8889,24])). % 11.44/11.66 cnf(9930,plain, % 11.44/11.66 (P10(a1)+~P9(a1)), % 11.44/11.66 inference(scs_inference,[],[14,8902,23])). % 11.44/11.66 cnf(10177,plain, % 11.44/11.66 (~P5(a1)+~P9(a1)), % 11.44/11.66 inference(scs_inference,[],[8968,9930])). % 11.44/11.66 cnf(10683,plain, % 11.44/11.66 (~P10(a1)+~P8(a1)), % 11.44/11.66 inference(scs_inference,[],[9672,8905])). % 11.44/11.66 cnf(10856,plain, % 11.44/11.66 (~P9(a1)+P8(a1)), % 11.44/11.66 inference(scs_inference,[],[10177,8883])). % 11.44/11.66 cnf(11129,plain, % 11.44/11.66 (P8(a1)), % 11.44/11.66 inference(scs_inference,[],[10856,8886])). % 11.44/11.66 cnf(11131,plain, % 11.44/11.66 (~P5(a1)), % 11.44/11.66 inference(scs_inference,[],[11129,8908])). % 11.44/11.66 cnf(11132,plain, % 11.44/11.66 (~P10(a1)), % 11.44/11.66 inference(scs_inference,[],[11129,10683])). % 11.44/11.66 cnf(11145,plain, % 11.44/11.66 ($false), % 11.44/11.66 inference(scs_inference,[],[11131,11132,14,27]), % 11.44/11.66 ['proof']). % 11.44/11.66 % SZS output end Proof % 11.44/11.66 % Total time :11.122023s %------------------------------------------------------------------------------