%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LCL656+1.005 : TPTP v9.3.1. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % Computer : n016.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:30 AM UTC 2026 % Result : Theorem 115.91s 116.12s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL656+1.005 : TPTP v9.3.1. Released v4.0.0. % 0.00/0.03 % Command : java -jar /export/starexec/sandbox/solver/bin/mcs_scs.jar %d %s % 0.09/0.36 % Computer : n016.cluster.edu % 0.09/0.36 % Model : x86_64 x86_64 % 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.36 % Memory : 8046.5625MB % 0.09/0.36 % OS : Linux 6.8.0-71-generic % 0.09/0.36 % CPULimit : 300 % 0.09/0.36 % WCLimit : 300 % 0.09/0.36 % DateTime : Sat Sep 5 17:29:44 UTC 2026 % 0.09/0.36 % CPUTime : % 0.27/0.46 start to proof:theBenchmark % 115.91/116.10 %------------------------------------------- % 115.91/116.10 % File :CSE---1.7 % 115.91/116.10 % Problem :theBenchmark % 115.91/116.10 % Transform :cnf % 115.91/116.10 % Format :tptp:raw % 115.91/116.10 % Command :java -jar mcs_scs.jar %d %s % 115.91/116.10 % 115.91/116.10 % Result :Theorem 115.601196s % 115.91/116.10 % Output :CNFRefutation 115.601196s % 115.91/116.10 %------------------------------------------- % 115.91/116.11 %------------------------------------------------------------------------------ % 115.91/116.11 % File : LCL656+1.005 : TPTP v9.3.1. Released v4.0.0. % 115.91/116.11 % Domain : Logic Calculi (Modal Logic) % 115.91/116.11 % Problem : In KT, the branching formula made provable, size 5 % 115.91/116.11 % Version : Especial. % 115.91/116.11 % English : The branching formula plus a negation symbol in front and an % 115.91/116.11 % additional subformula to make the formula provable. % 115.91/116.11 % 115.91/116.11 % Refs : [BHS00] Balsiger et al. (2000), A Benchmark Method for the Pro % 115.91/116.11 % : [Kam08] Kaminski (2008), Email to G. Sutcliffe % 115.91/116.11 % Source : [Kam08] % 115.91/116.11 % Names : kt_branch_p [BHS00] % 115.91/116.11 % 115.91/116.11 % Status : Theorem % 115.91/116.11 % Rating : 0.00 v9.3.0, 0.05 v9.1.0, 0.07 v9.0.0, 0.00 v7.5.0, 0.05 v7.4.0, 0.00 v6.4.0, 0.07 v6.3.0, 0.00 v6.2.0, 0.09 v6.1.0, 0.16 v6.0.0, 0.25 v5.4.0, 0.22 v5.3.0, 0.30 v5.2.0, 0.07 v5.0.0, 0.15 v4.1.0, 0.17 v4.0.1, 0.21 v4.0.0 % 115.91/116.11 % Syntax : Number of formulae : 2 ( 1 unt; 0 def) % 115.91/116.11 % Number of atoms : 130 ( 0 equ) % 115.91/116.11 % Maximal formula atoms : 129 ( 65 avg) % 115.91/116.11 % Number of connectives : 246 ( 118 ~; 74 |; 54 &) % 115.91/116.11 % ( 0 <=>; 0 =>; 0 <=; 0 <~>) % 115.91/116.11 % Maximal formula depth : 35 ( 19 avg) % 115.91/116.11 % Maximal term depth : 1 ( 1 avg) % 115.91/116.11 % Number of predicates : 14 ( 14 usr; 0 prp; 1-2 aty) % 115.91/116.11 % Number of functors : 0 ( 0 usr; 0 con; --- aty) % 115.91/116.11 % Number of variables : 34 ( 33 !; 1 ?) % 115.91/116.11 % SPC : FOF_THM_RFO_NEQ % 115.91/116.11 % 115.91/116.11 % Comments : A naive relational encoding of the modal logic problem into % 115.91/116.11 % first-order logic. % 115.91/116.11 %------------------------------------------------------------------------------ % 115.91/116.11 fof(reflexivity,axiom, % 115.91/116.11 ! [X] : r1(X,X) ). % 115.91/116.11 % 115.91/116.11 fof(main,conjecture, % 115.91/116.11 ~ ? [X] : % 115.91/116.11 ~ ( ~ ! [Y] : % 115.91/116.11 ( ~ r1(X,Y) % 115.91/116.11 | ! [X] : % 115.91/116.11 ( ~ r1(Y,X) % 115.91/116.11 | ! [Y] : % 115.91/116.11 ( ~ r1(X,Y) % 115.91/116.11 | ! [X] : % 115.91/116.11 ( ~ r1(Y,X) % 115.91/116.11 | ! [Y] : % 115.91/116.11 ( ~ r1(X,Y) % 115.91/116.11 | p3(Y) ) ) ) ) ) % 115.91/116.11 | ~ ( ! [Y] : % 115.91/116.11 ( ~ r1(X,Y) % 115.91/116.11 | ! [X] : % 115.91/116.11 ( ~ r1(Y,X) % 115.91/116.11 | ! [Y] : % 115.91/116.11 ( ~ r1(X,Y) % 115.91/116.11 | ! [X] : % 115.91/116.11 ( ~ r1(Y,X) % 115.91/116.11 | ! [Y] : % 115.91/116.11 ( ~ r1(X,Y) % 115.91/116.11 | ( ( ( ~ ! [X] : % 115.91/116.11 ( ~ r1(Y,X) % 115.91/116.11 | ~ ( ~ p6(X) % 115.91/116.11 & ~ p106(X) % 115.91/116.11 & p105(X) ) ) % 115.91/116.11 & ~ ! [X] : % 115.91/116.11 ( ~ r1(Y,X) % 115.91/116.11 | ~ ( p6(X) % 115.91/116.11 & ~ p106(X) % 115.91/116.11 & p105(X) ) ) ) % 115.91/116.11 | ~ ( ~ p105(Y) % 115.91/116.11 & p104(Y) ) ) % 115.91/116.11 & ( ( ~ ! [X] : % 115.91/116.11 ( ~ r1(Y,X) % 115.91/116.11 | ~ ( ~ p5(X) % 115.91/116.11 & ~ p105(X) % 115.91/116.11 & p104(X) ) ) % 115.91/116.11 & ~ ! [X] : % 115.91/116.11 ( ~ r1(Y,X) % 115.91/116.11 | ~ ( p5(X) % 115.91/116.11 & ~ p105(X) % 115.91/116.11 & p104(X) ) ) ) % 115.91/116.11 | ~ ( ~ p104(Y) % 115.91/116.11 & p103(Y) ) ) % 115.91/116.11 & ( ( ~ ! [X] : % 115.91/116.11 ( ~ r1(Y,X) % 115.91/116.11 | ~ ( ~ p4(X) % 115.91/116.11 & ~ p104(X) % 115.91/116.11 & p103(X) ) ) % 115.91/116.11 & ~ ! [X] : % 115.91/116.11 ( ~ r1(Y,X) % 115.91/116.11 | ~ ( p4(X) % 115.91/116.11 & ~ p104(X) % 115.91/116.11 & p103(X) ) ) ) % 115.91/116.11 | ~ ( ~ p103(Y) % 115.91/116.11 & p102(Y) ) ) % 115.91/116.11 & ( ( ~ ! [X] : % 115.91/116.11 ( ~ r1(Y,X) % 115.91/116.11 | ~ ( ~ p3(X) % 115.91/116.11 & ~ p103(X) % 115.91/116.11 & p102(X) ) ) % 115.91/116.11 & ~ ! [X] : % 115.91/116.11 ( ~ r1(Y,X) % 115.91/116.11 | ~ ( p3(X) % 115.91/116.11 & ~ p103(X) % 115.91/116.11 & p102(X) ) ) ) % 115.91/116.11 | ~ ( ~ p102(Y) % 115.91/116.11 & p101(Y) ) ) % 115.91/116.11 & ( ( ~ ! [X] : % 115.91/116.11 ( ~ r1(Y,X) % 115.91/116.11 | ~ ( ~ p2(X) % 115.91/116.11 & ~ p102(X) % 115.91/116.11 & p101(X) ) ) % 115.91/116.11 & ~ ! [X] : % 115.91/116.12 ( ~ r1(Y,X) % 115.91/116.12 | ~ ( p2(X) % 115.91/116.12 & ~ p102(X) % 115.91/116.12 & p101(X) ) ) ) % 115.91/116.12 | ~ ( ~ p101(Y) % 115.91/116.12 & p100(Y) ) ) % 115.91/116.12 & ( ( ( ! [X] : % 115.91/116.12 ( ~ r1(Y,X) % 115.91/116.12 | ~ p6(X) % 115.91/116.12 | ~ p105(X) ) % 115.91/116.12 | p6(Y) ) % 115.91/116.12 & ( ! [X] : % 115.91/116.12 ( ~ r1(Y,X) % 115.91/116.12 | p6(X) % 115.91/116.12 | ~ p105(X) ) % 115.91/116.12 | ~ p6(Y) ) ) % 115.91/116.12 | ~ p105(Y) ) % 115.91/116.12 & ( ( ( ! [X] : % 115.91/116.12 ( ~ r1(Y,X) % 115.91/116.12 | ~ p5(X) % 115.91/116.12 | ~ p104(X) ) % 115.91/116.12 | p5(Y) ) % 115.91/116.12 & ( ! [X] : % 115.91/116.12 ( ~ r1(Y,X) % 115.91/116.12 | p5(X) % 115.91/116.12 | ~ p104(X) ) % 115.91/116.12 | ~ p5(Y) ) ) % 115.91/116.12 | ~ p104(Y) ) % 115.91/116.12 & ( ( ( ! [X] : % 115.91/116.12 ( ~ r1(Y,X) % 115.91/116.12 | ~ p4(X) % 115.91/116.12 | ~ p103(X) ) % 115.91/116.12 | p4(Y) ) % 115.91/116.12 & ( ! [X] : % 115.91/116.12 ( ~ r1(Y,X) % 115.91/116.12 | p4(X) % 115.91/116.12 | ~ p103(X) ) % 115.91/116.12 | ~ p4(Y) ) ) % 115.91/116.12 | ~ p103(Y) ) % 115.91/116.12 & ( ( ( ! [X] : % 115.91/116.12 ( ~ r1(Y,X) % 115.91/116.12 | ~ p3(X) % 115.91/116.12 | ~ p102(X) ) % 115.91/116.12 | p3(Y) ) % 115.91/116.12 & ( ! [X] : % 115.91/116.12 ( ~ r1(Y,X) % 115.91/116.12 | p3(X) % 115.91/116.12 | ~ p102(X) ) % 115.91/116.12 | ~ p3(Y) ) ) % 115.91/116.12 | ~ p102(Y) ) % 115.91/116.12 & ( ( ( ! [X] : % 115.91/116.12 ( ~ r1(Y,X) % 115.91/116.12 | ~ p2(X) % 115.91/116.12 | ~ p101(X) ) % 115.91/116.12 | p2(Y) ) % 115.91/116.12 & ( ! [X] : % 115.91/116.12 ( ~ r1(Y,X) % 115.91/116.12 | p2(X) % 115.91/116.12 | ~ p101(X) ) % 115.91/116.12 | ~ p2(Y) ) ) % 115.91/116.12 | ~ p101(Y) ) % 115.91/116.12 & ( ( ( ! [X] : % 115.91/116.12 ( ~ r1(Y,X) % 115.91/116.12 | ~ p1(X) % 115.91/116.12 | ~ p100(X) ) % 115.91/116.12 | p1(Y) ) % 115.91/116.12 & ( ! [X] : % 115.91/116.12 ( ~ r1(Y,X) % 115.91/116.12 | p1(X) % 115.91/116.12 | ~ p100(X) ) % 115.91/116.12 | ~ p1(Y) ) ) % 115.91/116.12 | ~ p100(Y) ) % 115.91/116.12 & ( p105(Y) % 115.91/116.12 | ~ p106(Y) ) % 115.91/116.12 & ( p104(Y) % 115.91/116.12 | ~ p105(Y) ) % 115.91/116.12 & ( p103(Y) % 115.91/116.12 | ~ p104(Y) ) % 115.91/116.12 & ( p102(Y) % 115.91/116.12 | ~ p103(Y) ) % 115.91/116.12 & ( p101(Y) % 115.91/116.12 | ~ p102(Y) ) % 115.91/116.12 & ( p100(Y) % 115.91/116.12 | ~ p101(Y) ) ) ) ) ) ) ) % 115.91/116.12 & ~ p101(X) % 115.91/116.12 & p100(X) ) ) ). % 115.91/116.12 % 115.91/116.12 %------------------------------------------------------------------------------ % 115.91/116.12 %------------------------------------------- % 115.91/116.12 % Proof found % 115.91/116.12 % SZS status Theorem for theBenchmark % 115.91/116.12 % SZS output start Proof % 115.91/116.12 %ClaNum:63(EqnAxiom:0) % 115.91/116.12 %VarNum:294(SingletonVarNum:81) % 115.91/116.12 %MaxLitNum:6 % 115.91/116.12 %MaxfuncDepth:1 % 115.91/116.12 %SharedTerms:3 % 115.91/116.12 %goalClause: 1 3 62 63 % 115.91/116.12 %singleGoalClaCount:2 % 115.91/116.12 [1]P1(a1) % 115.91/116.12 [3]~P5(a1) % 115.91/116.12 [2]P4(x21,x21) % 115.91/116.12 [4]~P10(x41)+~P2(x41)+P6(x41) % 115.91/116.12 [5]~P6(x51)+~P2(x51)+P7(x51) % 115.91/116.12 [6]~P7(x61)+~P2(x61)+P8(x61) % 115.91/116.12 [7]~P8(x71)+~P2(x71)+P9(x71) % 115.91/116.12 [8]~P9(x81)+~P2(x81)+P5(x81) % 115.91/116.12 [9]~P5(x91)+~P2(x91)+P1(x91) % 115.91/116.12 [10]~P7(x101)+~P2(x101)+P6(x101)+P11(f4(x101)) % 115.91/116.12 [11]~P7(x111)+~P2(x111)+P6(x111)+P6(f5(x111)) % 115.91/116.12 [12]~P7(x121)+~P2(x121)+P6(x121)+P6(f4(x121)) % 115.91/116.12 [13]~P8(x131)+~P2(x131)+P7(x131)+P7(f6(x131)) % 115.91/116.12 [14]~P8(x141)+~P2(x141)+P7(x141)+P7(f7(x141)) % 115.91/116.12 [15]~P8(x151)+~P2(x151)+P7(x151)+P12(f7(x151)) % 115.91/116.12 [16]~P9(x161)+~P2(x161)+P8(x161)+P8(f8(x161)) % 115.91/116.12 [17]~P9(x171)+~P2(x171)+P8(x171)+P8(f9(x171)) % 115.91/116.12 [18]~P9(x181)+~P2(x181)+P8(x181)+P13(f9(x181)) % 115.91/116.12 [19]~P5(x191)+~P2(x191)+P9(x191)+P14(f10(x191)) % 115.91/116.12 [20]~P5(x201)+~P2(x201)+P9(x201)+P9(f11(x201)) % 115.91/116.12 [21]~P5(x211)+~P2(x211)+P9(x211)+P9(f10(x211)) % 115.91/116.12 [22]~P1(x221)+~P2(x221)+P5(x221)+P5(f2(x221)) % 115.91/116.12 [23]~P1(x231)+~P2(x231)+P5(x231)+P5(f3(x231)) % 115.91/116.12 [24]~P1(x241)+~P2(x241)+P5(x241)+P15(f3(x241)) % 115.91/116.12 [25]~P7(x251)+~P2(x251)+P6(x251)+~P11(f5(x251)) % 115.91/116.12 [26]~P7(x261)+~P2(x261)+P6(x261)+~P10(f5(x261)) % 115.91/116.12 [27]~P7(x271)+~P2(x271)+P6(x271)+~P10(f4(x271)) % 115.91/116.12 [28]~P8(x281)+~P2(x281)+P7(x281)+~P6(f6(x281)) % 115.91/116.12 [29]~P8(x291)+~P2(x291)+P7(x291)+~P6(f7(x291)) % 115.91/116.12 [30]~P8(x301)+~P2(x301)+P7(x301)+~P12(f6(x301)) % 115.91/116.12 [31]~P9(x311)+~P2(x311)+P8(x311)+~P7(f8(x311)) % 115.91/116.12 [32]~P9(x321)+~P2(x321)+P8(x321)+~P7(f9(x321)) % 115.91/116.12 [33]~P9(x331)+~P2(x331)+P8(x331)+~P13(f8(x331)) % 115.91/116.12 [34]~P5(x341)+~P2(x341)+P9(x341)+~P14(f11(x341)) % 115.91/116.12 [35]~P5(x351)+~P2(x351)+P9(x351)+~P8(f11(x351)) % 115.91/116.12 [36]~P5(x361)+~P2(x361)+P9(x361)+~P8(f10(x361)) % 115.91/116.12 [37]~P1(x371)+~P2(x371)+P5(x371)+~P9(f2(x371)) % 115.91/116.12 [38]~P1(x381)+~P2(x381)+P5(x381)+~P9(f3(x381)) % 115.91/116.12 [39]~P1(x391)+~P2(x391)+P5(x391)+~P15(f2(x391)) % 115.91/116.12 [40]~P7(x401)+~P2(x401)+P6(x401)+P4(x401,f5(x401)) % 115.91/116.12 [41]~P7(x411)+~P2(x411)+P6(x411)+P4(x411,f4(x411)) % 115.91/116.12 [42]~P8(x421)+~P2(x421)+P7(x421)+P4(x421,f6(x421)) % 115.91/116.12 [43]~P8(x431)+~P2(x431)+P7(x431)+P4(x431,f7(x431)) % 115.91/116.12 [44]~P9(x441)+~P2(x441)+P8(x441)+P4(x441,f8(x441)) % 115.91/116.12 [45]~P9(x451)+~P2(x451)+P8(x451)+P4(x451,f9(x451)) % 115.91/116.12 [46]~P5(x461)+~P2(x461)+P9(x461)+P4(x461,f11(x461)) % 115.91/116.12 [47]~P5(x471)+~P2(x471)+P9(x471)+P4(x471,f10(x471)) % 115.91/116.12 [48]~P1(x481)+~P2(x481)+P5(x481)+P4(x481,f2(x481)) % 115.91/116.12 [49]~P1(x491)+~P2(x491)+P5(x491)+P4(x491,f3(x491)) % 115.91/116.12 [50]~P9(x501)+~P9(x502)+~P2(x502)+~P4(x502,x501)+P14(x501)+~P14(x502) % 115.91/116.12 [51]~P9(x512)+~P9(x511)+~P2(x511)+~P4(x511,x512)+P14(x511)+~P14(x512) % 115.91/116.12 [52]~P6(x521)+~P6(x522)+~P2(x522)+~P4(x522,x521)+P11(x521)+~P11(x522) % 115.91/116.12 [53]~P6(x532)+~P6(x531)+~P2(x531)+~P4(x531,x532)+P11(x531)+~P11(x532) % 115.91/116.12 [54]~P7(x541)+~P12(x542)+~P2(x542)+~P4(x542,x541)+P12(x541)+~P7(x542) % 115.91/116.12 [55]~P7(x551)+~P12(x552)+~P2(x551)+~P4(x551,x552)+P12(x551)+~P7(x552) % 115.91/116.12 [56]~P8(x561)+~P13(x562)+~P2(x562)+~P4(x562,x561)+P13(x561)+~P8(x562) % 115.91/116.12 [57]~P8(x571)+~P13(x572)+~P2(x571)+~P4(x571,x572)+P13(x571)+~P8(x572) % 115.91/116.12 [58]~P5(x581)+~P15(x582)+~P2(x582)+~P4(x582,x581)+P15(x581)+~P5(x582) % 115.91/116.12 [59]~P5(x591)+~P15(x592)+~P2(x591)+~P4(x591,x592)+P15(x591)+~P5(x592) % 115.91/116.12 [60]~P1(x601)+~P3(x602)+~P2(x602)+~P4(x602,x601)+P3(x601)+~P1(x602) % 115.91/116.12 [61]~P1(x611)+~P3(x612)+~P2(x611)+~P4(x611,x612)+P3(x611)+~P1(x612) % 115.91/116.12 [62]P14(x621)+~P4(x622,x621)+~P4(x623,x622)+~P4(x624,x623)+~P4(x625,x624)+~P4(a1,x625) % 115.91/116.12 [63]P2(x631)+~P4(x632,x631)+~P4(x633,x632)+~P4(x634,x633)+~P4(x635,x634)+~P4(a1,x635) % 115.91/116.12 %EqnAxiom % 115.91/116.12 % 115.91/116.12 %------------------------------------------- % 116.12/116.20 cnf(65,plain, % 116.12/116.20 (P4(x651,x651)), % 116.12/116.20 inference(rename_variables,[],[2])). % 116.12/116.20 cnf(67,plain, % 116.12/116.20 (P2(a1)), % 116.12/116.20 inference(scs_inference,[],[2,65,62,63])). % 116.12/116.20 cnf(129261,plain, % 116.12/116.20 (P5(f2(a1))), % 116.12/116.20 inference(scs_inference,[],[1,3,67,22])). % 116.12/116.20 cnf(129263,plain, % 116.12/116.20 (P5(f3(a1))), % 116.12/116.20 inference(scs_inference,[],[1,3,67,22,23])). % 116.12/116.20 cnf(129265,plain, % 116.12/116.20 (P15(f3(a1))), % 116.12/116.20 inference(scs_inference,[],[1,3,67,22,23,24])). % 116.12/116.20 cnf(129269,plain, % 116.12/116.20 (~P9(f3(a1))), % 116.12/116.20 inference(scs_inference,[],[1,3,67,22,23,24,37,38])). % 116.12/116.20 cnf(129271,plain, % 116.12/116.20 (~P15(f2(a1))), % 116.12/116.20 inference(scs_inference,[],[1,3,67,22,23,24,37,38,39])). % 116.12/116.20 cnf(129275,plain, % 116.12/116.20 (P4(a1,f3(a1))), % 116.12/116.20 inference(scs_inference,[],[1,3,67,22,23,24,37,38,39,48,49])). % 116.12/116.20 cnf(129300,plain, % 116.12/116.20 (P4(x1293001,x1293001)), % 116.12/116.20 inference(rename_variables,[],[2])). % 116.12/116.20 cnf(129301,plain, % 116.12/116.20 (P4(x1293011,x1293011)), % 116.12/116.20 inference(rename_variables,[],[2])). % 116.12/116.20 cnf(129303,plain, % 116.12/116.20 (P2(f3(a1))), % 116.12/116.20 inference(scs_inference,[],[129275,2,129301,129300,62,63])). % 116.12/116.20 cnf(129400,plain, % 116.12/116.20 (P14(x1294001)+~P4(f3(a1),x1294001)), % 116.12/116.20 inference(scs_inference,[],[129275,2,62])). % 116.12/116.20 cnf(129416,plain, % 116.12/116.20 (~P4(f3(a1),x1294161)+P2(x1294161)), % 116.12/116.20 inference(scs_inference,[],[129303,129265,129271,129275,129261,129263,2,58,63])). % 116.12/116.20 cnf(129554,plain, % 116.12/116.20 (~P4(f3(a1),f11(f3(a1)))), % 116.12/116.20 inference(scs_inference,[],[129269,129303,129263,129400,34])). % 116.12/116.20 cnf(130361,plain, % 116.12/116.20 (P4(f3(a1),f11(f3(a1)))), % 116.12/116.20 inference(scs_inference,[],[2,129263,129269,129416,46])). % 116.12/116.20 cnf(155231,plain, % 116.12/116.20 ($false), % 116.12/116.20 inference(scs_inference,[],[130361,129554]), % 116.12/116.20 ['proof']). % 116.12/116.23 % SZS output end Proof % 116.12/116.23 % Total time :115.601196s %------------------------------------------------------------------------------