%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LCL674+1.005 : 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 : 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:35 AM UTC 2026 % Result : Theorem 29.68s 29.81s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL674+1.005 : 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.08/0.33 % Computer : n016.cluster.edu % 0.08/0.33 % Model : x86_64 x86_64 % 0.08/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.33 % Memory : 8046.5625MB % 0.08/0.33 % OS : Linux 6.8.0-71-generic % 0.08/0.33 % CPULimit : 300 % 0.08/0.33 % WCLimit : 300 % 0.08/0.33 % DateTime : Sat Sep 5 02:10:14 UTC 2026 % 0.08/0.34 % CPUTime : % 0.25/0.50 start to proof:theBenchmark % 29.68/29.80 %------------------------------------------- % 29.68/29.80 % File :CSE---1.7 % 29.68/29.80 % Problem :theBenchmark % 29.68/29.80 % Transform :cnf % 29.68/29.80 % Format :tptp:raw % 29.68/29.80 % Command :java -jar mcs_scs.jar %d %s % 29.68/29.80 % 29.68/29.80 % Result :Theorem 29.306089s % 29.68/29.80 % Output :CNFRefutation 29.306089s % 29.68/29.80 %------------------------------------------- % 29.68/29.80 %------------------------------------------------------------------------------ % 29.68/29.80 % File : LCL674+1.005 : TPTP v9.3.1. Released v4.0.0. % 29.68/29.80 % Domain : Logic Calculi (Modal Logic) % 29.68/29.80 % Problem : In S4, the branching formula made provable, size 5 % 29.68/29.80 % Version : Especial. % 29.68/29.80 % English : The branching formula plus a negation symbol in front and an % 29.68/29.80 % additional subformula to make the formula provable. % 29.68/29.80 % 29.68/29.80 % Refs : [BHS00] Balsiger et al. (2000), A Benchmark Method for the Pro % 29.68/29.80 % : [Kam08] Kaminski (2008), Email to G. Sutcliffe % 29.68/29.80 % Source : [Kam08] % 29.68/29.80 % Names : s4_branch_p [BHS00] % 29.68/29.80 % 29.68/29.80 % Status : Theorem % 29.68/29.80 % Rating : 0.00 v9.1.0, 0.07 v9.0.0, 0.00 v6.4.0, 0.07 v6.3.0, 0.08 v6.2.0, 0.09 v6.1.0, 0.08 v6.0.0, 0.25 v5.5.0, 0.12 v5.4.0, 0.13 v5.3.0, 0.17 v5.2.0, 0.07 v5.0.0, 0.05 v4.1.0, 0.11 v4.0.1, 0.16 v4.0.0 % 29.68/29.80 % Syntax : Number of formulae : 3 ( 1 unt; 0 def) % 29.68/29.80 % Number of atoms : 125 ( 0 equ) % 29.68/29.80 % Maximal formula atoms : 121 ( 41 avg) % 29.68/29.80 % Number of connectives : 232 ( 110 ~; 66 |; 55 &) % 29.68/29.81 % ( 0 <=>; 1 =>; 0 <=; 0 <~>) % 29.68/29.81 % Maximal formula depth : 27 ( 12 avg) % 29.68/29.81 % Maximal term depth : 1 ( 1 avg) % 29.68/29.81 % Number of predicates : 14 ( 14 usr; 0 prp; 1-2 aty) % 29.68/29.81 % Number of functors : 0 ( 0 usr; 0 con; --- aty) % 29.68/29.81 % Number of variables : 29 ( 28 !; 1 ?) % 29.68/29.81 % SPC : FOF_THM_RFO_NEQ % 29.68/29.81 % 29.68/29.81 % Comments : A naive relational encoding of the modal logic problem into % 29.68/29.81 % first-order logic. % 29.68/29.81 %------------------------------------------------------------------------------ % 29.68/29.81 fof(reflexivity,axiom, % 29.68/29.81 ! [X] : r1(X,X) ). % 29.68/29.81 % 29.68/29.81 fof(transitivity,axiom, % 29.68/29.81 ! [X,Y,Z] : % 29.68/29.81 ( ( r1(X,Y) % 29.68/29.81 & r1(Y,Z) ) % 29.68/29.81 => r1(X,Z) ) ). % 29.68/29.81 % 29.68/29.81 fof(main,conjecture, % 29.68/29.81 ~ ? [X] : % 29.68/29.81 ~ ( ~ ! [Y] : % 29.68/29.81 ( ~ r1(X,Y) % 29.68/29.81 | p3(Y) ) % 29.68/29.81 | ~ ( ! [Y] : % 29.68/29.81 ( ~ r1(X,Y) % 29.68/29.81 | ( ( ( ~ ! [X] : % 29.68/29.81 ( ~ r1(Y,X) % 29.68/29.81 | ~ ( ~ p6(X) % 29.68/29.81 & ~ p106(X) % 29.68/29.81 & p105(X) ) ) % 29.68/29.81 & ~ ! [X] : % 29.68/29.81 ( ~ r1(Y,X) % 29.68/29.81 | ~ ( p6(X) % 29.68/29.81 & ~ p106(X) % 29.68/29.81 & p105(X) ) ) ) % 29.68/29.81 | ~ ( ~ p105(Y) % 29.68/29.81 & p104(Y) ) ) % 29.68/29.81 & ( ( ~ ! [X] : % 29.68/29.81 ( ~ r1(Y,X) % 29.68/29.81 | ~ ( ~ p5(X) % 29.68/29.81 & ~ p105(X) % 29.68/29.81 & p104(X) ) ) % 29.68/29.81 & ~ ! [X] : % 29.68/29.81 ( ~ r1(Y,X) % 29.68/29.81 | ~ ( p5(X) % 29.68/29.81 & ~ p105(X) % 29.68/29.81 & p104(X) ) ) ) % 29.68/29.81 | ~ ( ~ p104(Y) % 29.68/29.81 & p103(Y) ) ) % 29.68/29.81 & ( ( ~ ! [X] : % 29.68/29.81 ( ~ r1(Y,X) % 29.68/29.81 | ~ ( ~ p4(X) % 29.68/29.81 & ~ p104(X) % 29.68/29.81 & p103(X) ) ) % 29.68/29.81 & ~ ! [X] : % 29.68/29.81 ( ~ r1(Y,X) % 29.68/29.81 | ~ ( p4(X) % 29.68/29.81 & ~ p104(X) % 29.68/29.81 & p103(X) ) ) ) % 29.68/29.81 | ~ ( ~ p103(Y) % 29.68/29.81 & p102(Y) ) ) % 29.68/29.81 & ( ( ~ ! [X] : % 29.68/29.81 ( ~ r1(Y,X) % 29.68/29.81 | ~ ( ~ p3(X) % 29.68/29.81 & ~ p103(X) % 29.68/29.81 & p102(X) ) ) % 29.68/29.81 & ~ ! [X] : % 29.68/29.81 ( ~ r1(Y,X) % 29.68/29.81 | ~ ( p3(X) % 29.68/29.81 & ~ p103(X) % 29.68/29.81 & p102(X) ) ) ) % 29.68/29.81 | ~ ( ~ p102(Y) % 29.68/29.81 & p101(Y) ) ) % 29.68/29.81 & ( ( ~ ! [X] : % 29.68/29.81 ( ~ r1(Y,X) % 29.68/29.81 | ~ ( ~ p2(X) % 29.68/29.81 & ~ p102(X) % 29.68/29.81 & p101(X) ) ) % 29.68/29.81 & ~ ! [X] : % 29.68/29.81 ( ~ r1(Y,X) % 29.68/29.81 | ~ ( p2(X) % 29.68/29.81 & ~ p102(X) % 29.68/29.81 & p101(X) ) ) ) % 29.68/29.81 | ~ ( ~ p101(Y) % 29.68/29.81 & p100(Y) ) ) % 29.68/29.81 & ( ( ( ! [X] : % 29.68/29.81 ( ~ r1(Y,X) % 29.68/29.81 | ~ p6(X) % 29.68/29.81 | ~ p105(X) ) % 29.68/29.81 | p6(Y) ) % 29.68/29.81 & ( ! [X] : % 29.68/29.81 ( ~ r1(Y,X) % 29.68/29.81 | p6(X) % 29.68/29.81 | ~ p105(X) ) % 29.68/29.81 | ~ p6(Y) ) ) % 29.68/29.81 | ~ p105(Y) ) % 29.68/29.81 & ( ( ( ! [X] : % 29.68/29.81 ( ~ r1(Y,X) % 29.68/29.81 | ~ p5(X) % 29.68/29.81 | ~ p104(X) ) % 29.68/29.81 | p5(Y) ) % 29.68/29.81 & ( ! [X] : % 29.68/29.81 ( ~ r1(Y,X) % 29.68/29.81 | p5(X) % 29.68/29.81 | ~ p104(X) ) % 29.68/29.81 | ~ p5(Y) ) ) % 29.68/29.81 | ~ p104(Y) ) % 29.68/29.81 & ( ( ( ! [X] : % 29.68/29.81 ( ~ r1(Y,X) % 29.68/29.81 | ~ p4(X) % 29.68/29.81 | ~ p103(X) ) % 29.68/29.81 | p4(Y) ) % 29.68/29.81 & ( ! [X] : % 29.68/29.81 ( ~ r1(Y,X) % 29.68/29.81 | p4(X) % 29.68/29.81 | ~ p103(X) ) % 29.68/29.81 | ~ p4(Y) ) ) % 29.68/29.81 | ~ p103(Y) ) % 29.68/29.81 & ( ( ( ! [X] : % 29.68/29.81 ( ~ r1(Y,X) % 29.68/29.81 | ~ p3(X) % 29.68/29.81 | ~ p102(X) ) % 29.68/29.81 | p3(Y) ) % 29.68/29.81 & ( ! [X] : % 29.68/29.81 ( ~ r1(Y,X) % 29.68/29.81 | p3(X) % 29.68/29.81 | ~ p102(X) ) % 29.68/29.81 | ~ p3(Y) ) ) % 29.68/29.81 | ~ p102(Y) ) % 29.68/29.81 & ( ( ( ! [X] : % 29.68/29.81 ( ~ r1(Y,X) % 29.68/29.81 | ~ p2(X) % 29.68/29.81 | ~ p101(X) ) % 29.68/29.81 | p2(Y) ) % 29.68/29.81 & ( ! [X] : % 29.68/29.81 ( ~ r1(Y,X) % 29.68/29.81 | p2(X) % 29.68/29.81 | ~ p101(X) ) % 29.68/29.81 | ~ p2(Y) ) ) % 29.68/29.81 | ~ p101(Y) ) % 29.68/29.81 & ( ( ( ! [X] : % 29.68/29.81 ( ~ r1(Y,X) % 29.68/29.81 | ~ p1(X) % 29.68/29.81 | ~ p100(X) ) % 29.68/29.81 | p1(Y) ) % 29.68/29.81 & ( ! [X] : % 29.68/29.81 ( ~ r1(Y,X) % 29.68/29.81 | p1(X) % 29.68/29.81 | ~ p100(X) ) % 29.68/29.81 | ~ p1(Y) ) ) % 29.68/29.81 | ~ p100(Y) ) % 29.68/29.81 & ( p105(Y) % 29.68/29.81 | ~ p106(Y) ) % 29.68/29.81 & ( p104(Y) % 29.68/29.81 | ~ p105(Y) ) % 29.68/29.81 & ( p103(Y) % 29.68/29.81 | ~ p104(Y) ) % 29.68/29.81 & ( p102(Y) % 29.68/29.81 | ~ p103(Y) ) % 29.68/29.81 & ( p101(Y) % 29.68/29.81 | ~ p102(Y) ) % 29.68/29.81 & ( p100(Y) % 29.68/29.81 | ~ p101(Y) ) ) ) % 29.68/29.81 & ~ p101(X) % 29.68/29.81 & p100(X) ) ) ). % 29.68/29.81 % 29.68/29.81 %------------------------------------------------------------------------------ % 29.68/29.81 %------------------------------------------- % 29.68/29.81 % Proof found % 29.68/29.81 % SZS status Theorem for theBenchmark % 29.68/29.81 % SZS output start Proof % 29.68/29.81 %ClaNum:64(EqnAxiom:0) % 29.68/29.81 %VarNum:284(SingletonVarNum:76) % 29.68/29.82 %MaxLitNum:6 % 29.68/29.82 %MaxfuncDepth:1 % 29.68/29.82 %SharedTerms:3 % 29.68/29.82 %goalClause: 1 3 10 11 % 29.68/29.82 %singleGoalClaCount:2 % 29.68/29.82 [1]P1(a1) % 29.68/29.82 [3]~P5(a1) % 29.68/29.82 [2]P4(x21,x21) % 29.68/29.82 [10]P11(x101)+~P4(a1,x101) % 29.68/29.82 [11]P2(x111)+~P4(a1,x111) % 29.68/29.82 [4]~P10(x41)+~P2(x41)+P6(x41) % 29.68/29.82 [5]~P6(x51)+~P2(x51)+P7(x51) % 29.68/29.82 [6]~P7(x61)+~P2(x61)+P8(x61) % 29.68/29.82 [7]~P8(x71)+~P2(x71)+P9(x71) % 29.68/29.82 [8]~P9(x81)+~P2(x81)+P5(x81) % 29.68/29.82 [9]~P5(x91)+~P2(x91)+P1(x91) % 29.68/29.82 [64]~P4(x641,x643)+P4(x641,x642)+~P4(x643,x642) % 29.68/29.82 [12]~P7(x121)+~P2(x121)+P6(x121)+P13(f4(x121)) % 29.68/29.82 [13]~P7(x131)+~P2(x131)+P6(x131)+P6(f5(x131)) % 29.68/29.82 [14]~P7(x141)+~P2(x141)+P6(x141)+P6(f4(x141)) % 29.68/29.82 [15]~P8(x151)+~P2(x151)+P7(x151)+P7(f6(x151)) % 29.68/29.82 [16]~P8(x161)+~P2(x161)+P7(x161)+P7(f7(x161)) % 29.68/29.82 [17]~P8(x171)+~P2(x171)+P7(x171)+P14(f7(x171)) % 29.68/29.82 [18]~P9(x181)+~P2(x181)+P8(x181)+P8(f8(x181)) % 29.68/29.82 [19]~P9(x191)+~P2(x191)+P8(x191)+P8(f9(x191)) % 29.68/29.82 [20]~P9(x201)+~P2(x201)+P8(x201)+P15(f9(x201)) % 29.68/29.82 [21]~P5(x211)+~P2(x211)+P9(x211)+P11(f10(x211)) % 29.68/29.82 [22]~P5(x221)+~P2(x221)+P9(x221)+P9(f11(x221)) % 29.68/29.82 [23]~P5(x231)+~P2(x231)+P9(x231)+P9(f10(x231)) % 29.68/29.82 [24]~P1(x241)+~P2(x241)+P5(x241)+P5(f2(x241)) % 29.68/29.82 [25]~P1(x251)+~P2(x251)+P5(x251)+P5(f3(x251)) % 29.68/29.82 [26]~P1(x261)+~P2(x261)+P5(x261)+P12(f3(x261)) % 29.68/29.82 [27]~P7(x271)+~P2(x271)+P6(x271)+~P13(f5(x271)) % 29.68/29.82 [28]~P7(x281)+~P2(x281)+P6(x281)+~P10(f5(x281)) % 29.68/29.82 [29]~P7(x291)+~P2(x291)+P6(x291)+~P10(f4(x291)) % 29.68/29.82 [30]~P8(x301)+~P2(x301)+P7(x301)+~P6(f6(x301)) % 29.68/29.82 [31]~P8(x311)+~P2(x311)+P7(x311)+~P6(f7(x311)) % 29.68/29.82 [32]~P8(x321)+~P2(x321)+P7(x321)+~P14(f6(x321)) % 29.68/29.82 [33]~P9(x331)+~P2(x331)+P8(x331)+~P7(f8(x331)) % 29.68/29.82 [34]~P9(x341)+~P2(x341)+P8(x341)+~P7(f9(x341)) % 29.68/29.82 [35]~P9(x351)+~P2(x351)+P8(x351)+~P15(f8(x351)) % 29.68/29.82 [36]~P5(x361)+~P2(x361)+P9(x361)+~P11(f11(x361)) % 29.68/29.82 [37]~P5(x371)+~P2(x371)+P9(x371)+~P8(f11(x371)) % 29.68/29.82 [38]~P5(x381)+~P2(x381)+P9(x381)+~P8(f10(x381)) % 29.68/29.82 [39]~P1(x391)+~P2(x391)+P5(x391)+~P9(f2(x391)) % 29.68/29.82 [40]~P1(x401)+~P2(x401)+P5(x401)+~P9(f3(x401)) % 29.68/29.82 [41]~P1(x411)+~P2(x411)+P5(x411)+~P12(f2(x411)) % 29.68/29.82 [42]~P7(x421)+~P2(x421)+P6(x421)+P4(x421,f5(x421)) % 29.68/29.82 [43]~P7(x431)+~P2(x431)+P6(x431)+P4(x431,f4(x431)) % 29.68/29.82 [44]~P8(x441)+~P2(x441)+P7(x441)+P4(x441,f6(x441)) % 29.68/29.82 [45]~P8(x451)+~P2(x451)+P7(x451)+P4(x451,f7(x451)) % 29.68/29.82 [46]~P9(x461)+~P2(x461)+P8(x461)+P4(x461,f8(x461)) % 29.68/29.82 [47]~P9(x471)+~P2(x471)+P8(x471)+P4(x471,f9(x471)) % 29.68/29.82 [48]~P5(x481)+~P2(x481)+P9(x481)+P4(x481,f11(x481)) % 29.68/29.82 [49]~P5(x491)+~P2(x491)+P9(x491)+P4(x491,f10(x491)) % 29.68/29.82 [50]~P1(x501)+~P2(x501)+P5(x501)+P4(x501,f2(x501)) % 29.68/29.82 [51]~P1(x511)+~P2(x511)+P5(x511)+P4(x511,f3(x511)) % 29.68/29.82 [52]~P9(x521)+~P9(x522)+~P2(x522)+~P4(x522,x521)+P11(x521)+~P11(x522) % 29.68/29.82 [53]~P9(x532)+~P9(x531)+~P2(x531)+~P4(x531,x532)+P11(x531)+~P11(x532) % 29.68/29.82 [54]~P6(x541)+~P6(x542)+~P2(x542)+~P4(x542,x541)+P13(x541)+~P13(x542) % 29.68/29.82 [55]~P6(x552)+~P6(x551)+~P2(x551)+~P4(x551,x552)+P13(x551)+~P13(x552) % 29.68/29.82 [56]~P7(x561)+~P14(x562)+~P2(x562)+~P4(x562,x561)+P14(x561)+~P7(x562) % 29.68/29.82 [57]~P7(x571)+~P14(x572)+~P2(x571)+~P4(x571,x572)+P14(x571)+~P7(x572) % 29.68/29.82 [58]~P8(x581)+~P15(x582)+~P2(x582)+~P4(x582,x581)+P15(x581)+~P8(x582) % 29.68/29.82 [59]~P8(x591)+~P15(x592)+~P2(x591)+~P4(x591,x592)+P15(x591)+~P8(x592) % 29.68/29.82 [60]~P5(x601)+~P12(x602)+~P2(x602)+~P4(x602,x601)+P12(x601)+~P5(x602) % 29.68/29.82 [61]~P5(x611)+~P12(x612)+~P2(x611)+~P4(x611,x612)+P12(x611)+~P5(x612) % 29.68/29.82 [62]~P1(x621)+~P3(x622)+~P2(x622)+~P4(x622,x621)+P3(x621)+~P1(x622) % 29.68/29.82 [63]~P1(x631)+~P3(x632)+~P2(x631)+~P4(x631,x632)+P3(x631)+~P1(x632) % 29.68/29.82 %EqnAxiom % 29.68/29.82 % 29.68/29.82 %------------------------------------------- % 29.68/29.83 cnf(66,plain, % 29.68/29.83 (P4(x661,x661)), % 29.68/29.83 inference(rename_variables,[],[2])). % 29.68/29.83 cnf(68,plain, % 29.68/29.83 (P2(a1)), % 29.68/29.83 inference(scs_inference,[],[2,66,10,11])). % 29.68/29.83 cnf(2539,plain, % 29.68/29.83 (~P2(f2(a1))+~P5(f2(a1))+~P8(f11(f2(a1)))), % 29.68/29.83 inference(scs_inference,[],[68,3,1,37,39])). % 29.68/29.83 cnf(2609,plain, % 29.68/29.83 (~P8(f11(f2(a1)))+~P2(f2(a1))), % 29.68/29.83 inference(scs_inference,[],[68,3,1,2539,24])). % 29.68/29.83 cnf(3651,plain, % 29.68/29.83 (~P2(f2(a1))+~P5(f2(a1))+P4(f2(a1),f11(f2(a1)))), % 29.68/29.83 inference(scs_inference,[],[68,3,1,48,39])). % 29.68/29.83 cnf(3720,plain, % 29.68/29.83 (P4(f2(a1),f11(f2(a1)))+~P5(f2(a1))+~P4(a1,f2(a1))), % 29.68/29.83 inference(scs_inference,[],[3651,11])). % 29.68/29.83 cnf(3788,plain, % 29.68/29.83 (P4(f2(a1),f11(f2(a1)))+~P5(f2(a1))), % 29.68/29.83 inference(scs_inference,[],[68,3,1,3720,50])). % 29.68/29.83 cnf(3857,plain, % 29.68/29.83 (P4(f2(a1),f11(f2(a1)))), % 29.68/29.83 inference(scs_inference,[],[68,3,1,3788,24])). % 29.68/29.83 cnf(6858,plain, % 29.68/29.83 (P2(f2(a1))), % 29.68/29.83 inference(scs_inference,[],[68,3,1,11,50])). % 29.68/29.83 cnf(6859,plain, % 29.68/29.83 (~P8(f11(f2(a1)))), % 29.68/29.83 inference(scs_inference,[],[6858,2609])). % 29.68/29.83 cnf(8677,plain, % 29.68/29.83 (P5(f2(a1))), % 29.68/29.83 inference(scs_inference,[],[2,3,1,11,24])). % 29.68/29.83 cnf(19951,plain, % 29.68/29.83 (P4(a1,f2(a1))), % 29.68/29.83 inference(scs_inference,[],[2,3,1,11,50])). % 29.68/29.83 cnf(20003,plain, % 29.68/29.83 (~P9(f2(a1))), % 29.68/29.83 inference(scs_inference,[],[2,3,1,11,39])). % 29.68/29.83 cnf(26161,plain, % 29.68/29.83 ($false), % 29.68/29.83 inference(scs_inference,[],[6858,19951,6859,8677,20003,3857,64,11,10,6,36]), % 29.68/29.83 ['proof']). % 29.68/29.83 % SZS output end Proof % 29.68/29.83 % Total time :29.306089s %------------------------------------------------------------------------------