%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LCL650+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:28 AM UTC 2026 % Result : Theorem 58.35s 58.57s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL650+1.001 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.02 % Command : java -jar /export/starexec/sandbox2/solver/bin/mcs_scs.jar %d %s % 0.07/0.34 % Computer : n006.cluster.edu % 0.07/0.34 % Model : x86_64 x86_64 % 0.07/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.07/0.34 % Memory : 8046.5625MB % 0.07/0.34 % OS : Linux 6.8.0-71-generic % 0.07/0.34 % CPULimit : 300 % 0.07/0.34 % WCLimit : 300 % 0.07/0.34 % DateTime : Sat Sep 5 19:59:46 UTC 2026 % 0.07/0.34 % CPUTime : % 0.24/0.49 start to proof:theBenchmark % 58.35/58.56 %------------------------------------------- % 58.35/58.56 % File :CSE---1.7 % 58.35/58.56 % Problem :theBenchmark % 58.35/58.56 % Transform :cnf % 58.35/58.56 % Format :tptp:raw % 58.35/58.56 % Command :java -jar mcs_scs.jar %d %s % 58.35/58.56 % 58.35/58.56 % Result :Theorem 58.055240s % 58.35/58.56 % Output :CNFRefutation 58.055240s % 58.35/58.56 %------------------------------------------- % 58.35/58.56 %------------------------------------------------------------------------------ % 58.35/58.56 % File : LCL650+1.001 : TPTP v9.3.1. Released v4.0.0. % 58.35/58.56 % Domain : Logic Calculi (Modal Logic) % 58.35/58.56 % Problem : In K, black and white polygon with odd number of vertices, size 1 % 58.35/58.56 % Version : Especial. % 58.35/58.56 % English : If we have a polygon with n vertices, and all the vertices are % 58.35/58.56 % either black or white, then two adjacent vertices have the same % 58.35/58.56 % colour. % 58.35/58.56 % 58.35/58.56 % Refs : [BHS00] Balsiger et al. (2000), A Benchmark Method for the Pro % 58.35/58.56 % : [Kam08] Kaminski (2008), Email to G. Sutcliffe % 58.35/58.56 % Source : [Kam08] % 58.35/58.56 % Names : k_poly_p [BHS00] % 58.35/58.56 % 58.35/58.56 % Status : Theorem % 58.35/58.56 % Rating : 0.00 v9.1.0, 0.07 v9.0.0, 0.00 v6.1.0, 0.04 v6.0.0, 0.25 v5.5.0, 0.12 v5.4.0, 0.13 v5.3.0, 0.22 v5.2.0, 0.07 v5.0.0, 0.05 v4.1.0, 0.06 v4.0.1, 0.05 v4.0.0 % 58.35/58.56 % Syntax : Number of formulae : 1 ( 0 unt; 0 def) % 58.35/58.56 % Number of atoms : 43 ( 0 equ) % 58.35/58.56 % Maximal formula atoms : 43 ( 43 avg) % 58.35/58.56 % Number of connectives : 86 ( 44 ~; 30 |; 12 &) % 58.35/58.56 % ( 0 <=>; 0 =>; 0 <=; 0 <~>) % 58.35/58.56 % Maximal formula depth : 30 ( 30 avg) % 58.35/58.56 % Maximal term depth : 1 ( 1 avg) % 58.35/58.56 % Number of predicates : 8 ( 8 usr; 0 prp; 1-2 aty) % 58.35/58.56 % Number of functors : 0 ( 0 usr; 0 con; --- aty) % 58.35/58.56 % Number of variables : 21 ( 20 !; 1 ?) % 58.35/58.56 % SPC : FOF_THM_RFO_NEQ % 58.35/58.56 % 58.35/58.56 % Comments : A naive relational encoding of the modal logic problem into % 58.35/58.56 % first-order logic. % 58.35/58.56 %------------------------------------------------------------------------------ % 58.35/58.56 fof(main,conjecture, % 58.35/58.56 ~ ? [X] : % 58.35/58.56 ~ ( ! [Y] : % 58.35/58.56 ( ~ r1(X,Y) % 58.35/58.56 | ! [X] : % 58.35/58.56 ( ~ r1(Y,X) % 58.35/58.56 | ! [Y] : % 58.35/58.56 ( ~ r1(X,Y) % 58.35/58.56 | ! [X] : % 58.35/58.56 ( ~ r1(Y,X) % 58.35/58.56 | ( ~ p8(X) % 58.35/58.56 & ~ p6(X) % 58.35/58.56 & ~ p4(X) % 58.35/58.56 & ~ p2(X) ) ) ) ) ) % 58.35/58.56 | ! [Y] : % 58.35/58.56 ( ~ r1(X,Y) % 58.35/58.56 | p5(Y) ) % 58.35/58.56 | ~ ! [Y] : % 58.35/58.56 ( ~ r1(X,Y) % 58.35/58.56 | ~ ( ~ ! [X] : % 58.35/58.56 ( ~ r1(Y,X) % 58.35/58.56 | ! [Y] : % 58.35/58.56 ( ~ r1(X,Y) % 58.35/58.56 | ! [X] : % 58.35/58.56 ( ~ r1(Y,X) % 58.35/58.56 | ~ ( ( ~ p3(X) % 58.35/58.56 & ~ p1(X) ) % 58.35/58.56 | ( p1(X) % 58.35/58.56 & p3(X) ) ) ) ) ) % 58.35/58.56 | ! [X] : % 58.35/58.56 ( ~ r1(Y,X) % 58.35/58.57 | p4(X) ) % 58.35/58.57 | ~ ! [X] : % 58.35/58.57 ( ~ r1(Y,X) % 58.35/58.57 | ~ ( ~ ! [Y] : % 58.35/58.57 ( ~ r1(X,Y) % 58.35/58.57 | ! [X] : % 58.35/58.57 ( ~ r1(Y,X) % 58.35/58.57 | ~ ( ( ~ p2(X) % 58.35/58.57 & ~ p3(X) ) % 58.35/58.57 | ( p3(X) % 58.35/58.57 & p2(X) ) ) ) ) % 58.35/58.57 | ! [Y] : % 58.35/58.57 ( ~ r1(X,Y) % 58.35/58.57 | p3(Y) ) % 58.35/58.57 | ~ ! [Y] : % 58.35/58.57 ( ~ r1(X,Y) % 58.35/58.57 | ~ ~ ! [X] : % 58.35/58.57 ( ~ r1(Y,X) % 58.35/58.57 | ~ ( ( ~ p1(X) % 58.35/58.57 & ~ p2(X) ) % 58.35/58.57 | ( p2(X) % 58.35/58.57 & p1(X) ) ) ) ) ) ) ) ) % 58.35/58.57 | ! [Y] : % 58.35/58.57 ( ~ r1(X,Y) % 58.35/58.57 | ! [X] : % 58.35/58.57 ( ~ r1(Y,X) % 58.35/58.57 | ! [Y] : % 58.35/58.57 ( ~ r1(X,Y) % 58.35/58.57 | ! [X] : % 58.35/58.57 ( ~ r1(Y,X) % 58.35/58.57 | ( p4(X) % 58.35/58.57 & p3(X) % 58.35/58.57 & p2(X) % 58.35/58.57 & p1(X) ) ) ) ) ) ) ). % 58.35/58.57 % 58.35/58.57 %------------------------------------------------------------------------------ % 58.35/58.57 %------------------------------------------- % 58.35/58.57 % Proof found % 58.35/58.57 % SZS status Theorem for theBenchmark % 58.35/58.57 % SZS output start Proof % 58.35/58.57 %ClaNum:22(EqnAxiom:0) % 58.35/58.57 %VarNum:70(SingletonVarNum:30) % 58.35/58.57 %MaxLitNum:6 % 58.35/58.57 %MaxfuncDepth:1 % 58.35/58.57 %SharedTerms:28 % 58.35/58.57 %goalClause: 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 % 58.35/58.57 %singleGoalClaCount:10 % 58.35/58.57 [1]P1(a1,a5) % 58.35/58.57 [2]P1(a1,a6) % 58.35/58.57 [3]P1(a1,a10) % 58.35/58.57 [4]P1(a5,a7) % 58.35/58.57 [5]P1(a7,a8) % 58.35/58.57 [6]P1(a8,a9) % 58.35/58.57 [7]P1(a10,a2) % 58.35/58.57 [8]P1(a2,a3) % 58.35/58.57 [9]P1(a3,a4) % 58.35/58.57 [10]~P2(a6) % 58.35/58.57 [13]~P1(a1,x131)+~P3(f11(x131)) % 58.35/58.57 [14]~P1(a1,x141)+P1(x141,f11(x141)) % 58.35/58.57 [15]~P1(x152,x151)+~P1(a1,x152)+P1(x151,f12(x152,x151)) % 58.35/58.57 [16]~P1(x161,x162)+~P1(a1,x161)+~P6(f12(x161,x162)) % 58.35/58.57 [11]P7(a9)+P8(a9)+P3(a9)+P4(a9) % 58.35/58.57 [12]~P3(a4)+~P4(a4)+~P6(a4)+~P5(a4) % 58.35/58.57 [17]P6(x171)+~P1(x174,x171)+P4(x171)+~P1(x172,x173)+~P1(x173,x174)+~P1(a1,x172) % 58.35/58.57 [18]P5(x181)+~P1(x184,x181)+P4(x181)+~P1(x182,x183)+~P1(x183,x184)+~P1(a1,x182) % 58.35/58.57 [19]P5(x191)+~P1(x194,x191)+P6(x191)+~P1(x192,x193)+~P1(x193,x194)+~P1(a1,x192) % 58.35/58.57 [20]~P6(x201)+~P1(x204,x201)+~P4(x201)+~P1(x202,x203)+~P1(x203,x204)+~P1(a1,x202) % 58.35/58.57 [21]~P5(x211)+~P1(x214,x211)+~P4(x211)+~P1(x212,x213)+~P1(x213,x214)+~P1(a1,x212) % 58.35/58.57 [22]~P5(x221)+~P1(x224,x221)+~P6(x221)+~P1(x222,x223)+~P1(x223,x224)+~P1(a1,x222) % 58.35/58.57 %EqnAxiom % 58.35/58.57 % 58.35/58.57 %------------------------------------------- % 58.47/58.67 cnf(115753,plain, % 58.47/58.67 (P6(a9)+P5(a9)), % 58.47/58.67 inference(scs_inference,[],[1,6,4,2,7,3,5,14,16,19])). % 58.47/58.67 cnf(115791,plain, % 58.47/58.67 (~P4(a9)+P6(a9)), % 58.47/58.67 inference(scs_inference,[],[6,5,4,1,115753,21])). % 58.47/58.67 cnf(115816,plain, % 58.47/58.67 (~P4(a9)), % 58.47/58.67 inference(scs_inference,[],[1,6,4,5,20,19,115791])). % 58.47/58.67 cnf(115821,plain, % 58.47/58.67 (P6(a9)), % 58.47/58.67 inference(scs_inference,[],[1,115816,6,4,5,16,17])). % 58.47/58.67 cnf(115826,plain, % 58.47/58.67 ($false), % 58.47/58.67 inference(scs_inference,[],[1,115821,115816,6,4,5,18,22]), % 58.47/58.67 ['proof']). % 58.57/58.70 % SZS output end Proof % 58.57/58.70 % Total time :58.055240s %------------------------------------------------------------------------------