%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LCL644+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 : n027.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:26 AM UTC 2026 % Result : Theorem 0.23s 0.53s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL644+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.07/0.34 % Computer : n027.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.35 % DateTime : Sat Sep 5 05:03:28 UTC 2026 % 0.07/0.35 % CPUTime : % 0.23/0.51 start to proof:theBenchmark % 0.23/0.52 %------------------------------------------- % 0.23/0.52 % File :CSE---1.7 % 0.23/0.52 % Problem :theBenchmark % 0.23/0.52 % Transform :cnf % 0.23/0.52 % Format :tptp:raw % 0.23/0.52 % Command :java -jar mcs_scs.jar %d %s % 0.23/0.52 % 0.23/0.52 % Result :Theorem 0.005539s % 0.23/0.52 % Output :CNFRefutation 0.005539s % 0.23/0.52 %------------------------------------------- % 0.23/0.52 %------------------------------------------------------------------------------ % 0.23/0.52 % File : LCL644+1.001 : TPTP v9.3.1. Released v4.0.0. % 0.23/0.52 % Domain : Logic Calculi (Modal Logic) % 0.23/0.52 % Problem : In K, H2 -> L, size 1 % 0.23/0.52 % Version : Especial. % 0.23/0.52 % English : % 0.23/0.52 % 0.23/0.52 % Refs : [BHS00] Balsiger et al. (2000), A Benchmark Method for the Pro % 0.23/0.52 % : [Kam08] Kaminski (2008), Email to G. Sutcliffe % 0.23/0.52 % Source : [Kam08] % 0.23/0.52 % Names : k_lin_p [BHS00] % 0.23/0.52 % 0.23/0.52 % Status : Theorem % 0.23/0.52 % Rating : 0.00 v9.3.0, 0.05 v9.1.0, 0.07 v9.0.0, 0.00 v6.1.0, 0.08 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 % 0.23/0.52 % Syntax : Number of formulae : 1 ( 0 unt; 0 def) % 0.23/0.52 % Number of atoms : 53 ( 0 equ) % 0.23/0.52 % Maximal formula atoms : 53 ( 53 avg) % 0.23/0.52 % Number of connectives : 85 ( 33 ~; 36 |; 16 &) % 0.23/0.52 % ( 0 <=>; 0 =>; 0 <=; 0 <~>) % 0.23/0.52 % Maximal formula depth : 24 ( 24 avg) % 0.23/0.52 % Maximal term depth : 1 ( 1 avg) % 0.23/0.52 % Number of predicates : 3 ( 3 usr; 0 prp; 1-2 aty) % 0.23/0.52 % Number of functors : 0 ( 0 usr; 0 con; --- aty) % 0.23/0.52 % Number of variables : 20 ( 19 !; 1 ?) % 0.23/0.52 % SPC : FOF_THM_RFO_NEQ % 0.23/0.52 % 0.23/0.52 % Comments : A naive relational encoding of the modal logic problem into % 0.23/0.52 % first-order logic. % 0.23/0.52 %------------------------------------------------------------------------------ % 0.23/0.52 fof(main,conjecture, % 0.23/0.52 ~ ? [X] : % 0.23/0.52 ~ ( ~ ( ! [Y] : % 0.23/0.52 ( ~ r1(X,Y) % 0.23/0.53 | ~ ( p2(Y) % 0.23/0.53 & ! [X] : % 0.23/0.53 ( ~ r1(Y,X) % 0.23/0.53 | p2(X) ) ) % 0.23/0.53 | p1(Y) ) % 0.23/0.53 | ! [Y] : % 0.23/0.53 ( ~ r1(X,Y) % 0.23/0.53 | p2(Y) % 0.23/0.53 | ~ ( p1(Y) % 0.23/0.53 & ! [X] : % 0.23/0.53 ( ~ r1(Y,X) % 0.23/0.53 | p1(X) ) % 0.23/0.53 & p1(Y) ) ) % 0.23/0.53 | ~ ( ! [Y] : % 0.23/0.53 ( ~ r1(X,Y) % 0.23/0.53 | ! [X] : % 0.23/0.53 ( ~ r1(Y,X) % 0.23/0.53 | ~ ( p2(X) % 0.23/0.53 & ! [Y] : % 0.23/0.53 ( ~ r1(X,Y) % 0.23/0.53 | p2(Y) ) ) % 0.23/0.53 | p1(X) ) % 0.23/0.53 | p2(Y) % 0.23/0.53 | ~ ( p1(Y) % 0.23/0.53 & ! [X] : % 0.23/0.53 ( ~ r1(Y,X) % 0.23/0.53 | p1(X) ) % 0.23/0.53 & p1(Y) ) ) % 0.23/0.53 & ! [Y] : % 0.23/0.53 ( ~ r1(X,Y) % 0.23/0.53 | ~ ( p2(Y) % 0.23/0.53 & ! [X] : % 0.23/0.53 ( ~ r1(Y,X) % 0.23/0.53 | p2(X) ) ) % 0.23/0.53 | p1(Y) % 0.23/0.53 | ! [X] : % 0.23/0.53 ( ~ r1(Y,X) % 0.23/0.53 | p2(X) % 0.23/0.53 | ~ ( p1(X) % 0.23/0.53 & ! [Y] : % 0.23/0.53 ( ~ r1(X,Y) % 0.23/0.53 | p1(Y) ) % 0.23/0.53 & p1(X) ) ) ) % 0.23/0.53 & ! [Y] : % 0.23/0.53 ( ~ r1(X,Y) % 0.23/0.53 | ~ ( p2(Y) % 0.23/0.53 & ! [X] : % 0.23/0.53 ( ~ r1(Y,X) % 0.23/0.53 | p2(X) ) ) % 0.23/0.53 | p1(Y) % 0.23/0.53 | p2(Y) % 0.23/0.53 | ~ ( p1(Y) % 0.23/0.53 & ! [X] : % 0.23/0.53 ( ~ r1(Y,X) % 0.23/0.53 | p1(X) ) % 0.23/0.53 & p1(Y) ) ) ) ) % 0.23/0.53 | ! [Y] : % 0.23/0.53 ( ~ r1(X,Y) % 0.23/0.53 | p1(Y) % 0.23/0.53 | ~ ( ! [X] : % 0.23/0.53 ( ~ r1(Y,X) % 0.23/0.53 | p1(X) ) % 0.23/0.53 & p1(Y) ) ) % 0.23/0.53 | ! [Y] : % 0.23/0.53 ( ~ r1(X,Y) % 0.23/0.53 | p1(Y) % 0.23/0.53 | ~ ( ! [X] : % 0.23/0.53 ( ~ r1(Y,X) % 0.23/0.53 | p1(X) ) % 0.23/0.53 & p1(Y) ) ) ) ). % 0.23/0.53 % 0.23/0.53 %------------------------------------------------------------------------------ % 0.23/0.53 %------------------------------------------- % 0.23/0.53 % Proof found % 0.23/0.53 % SZS status Theorem for theBenchmark % 0.23/0.53 % SZS output start Proof % 0.23/0.53 %ClaNum:121(EqnAxiom:0) % 0.23/0.53 %VarNum:560(SingletonVarNum:162) % 0.23/0.53 %MaxLitNum:11 % 0.23/0.53 %MaxfuncDepth:1 % 0.23/0.53 %SharedTerms:16 % 0.23/0.53 %goalClause: 1 2 3 4 5 6 7 8 90 92 93 94 95 96 98 100 101 102 103 104 105 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 % 0.23/0.53 %singleGoalClaCount:6 % 0.23/0.53 [1]P1(a1) % 0.23/0.53 [2]P1(a7) % 0.23/0.53 [3]P3(a2,a1) % 0.23/0.53 [4]P3(a2,a7) % 0.23/0.53 [5]~P1(a1) % 0.23/0.53 [6]~P1(a7) % 0.23/0.53 [7]P1(x71)+~P3(a1,x71) % 0.23/0.53 [8]P1(x81)+~P3(a7,x81) % 0.23/0.53 [9]P2(x91)+P4(f8(x91))+P4(f10(x91)) % 0.23/0.53 [11]P2(x111)+P4(f8(x111))+P1(f3(x111)) % 0.23/0.53 [13]P2(x131)+P4(f10(x131))+P1(f9(x131)) % 0.23/0.53 [17]P2(x171)+P1(f9(x171))+P1(f3(x171)) % 0.23/0.53 [18]P2(x181)+P4(f8(x181))+~P4(f3(x181)) % 0.23/0.53 [19]P2(x191)+P4(f8(x191))+~P1(f10(x191)) % 0.23/0.53 [20]P2(x201)+P4(f10(x201))+~P4(f9(x201)) % 0.23/0.53 [21]P2(x211)+P4(f10(x211))+~P1(f8(x211)) % 0.23/0.53 [23]P2(x231)+P1(f9(x231))+~P4(f3(x231)) % 0.23/0.53 [25]P2(x251)+P1(f9(x251))+~P1(f10(x251)) % 0.23/0.53 [27]P2(x271)+P1(f3(x271))+~P4(f9(x271)) % 0.23/0.53 [29]P2(x291)+P1(f3(x291))+~P1(f8(x291)) % 0.23/0.53 [30]P2(x301)+P3(x301,f10(x301))+P4(f8(x301)) % 0.23/0.53 [31]P2(x311)+P3(x311,f9(x311))+P4(f10(x311)) % 0.23/0.53 [33]P2(x331)+P3(x331,f10(x331))+P1(f9(x331)) % 0.23/0.53 [35]P2(x351)+P3(x351,f9(x351))+P1(f3(x351)) % 0.23/0.53 [36]P2(x361)+~P4(f9(x361))+~P4(f3(x361)) % 0.23/0.53 [37]P2(x371)+~P4(f9(x371))+~P1(f10(x371)) % 0.23/0.53 [38]P2(x381)+~P4(f3(x381))+~P1(f8(x381)) % 0.23/0.53 [39]P2(x391)+~P1(f8(x391))+~P1(f10(x391)) % 0.23/0.53 [40]P2(x401)+P3(f10(x401),f3(x401))+P4(f8(x401)) % 0.23/0.53 [41]P2(x411)+P3(f9(x411),f8(x411))+P4(f10(x411)) % 0.23/0.53 [43]P2(x431)+P3(f10(x431),f3(x431))+P1(f9(x431)) % 0.23/0.53 [45]P2(x451)+P3(f9(x451),f8(x451))+P1(f3(x451)) % 0.23/0.53 [46]P2(x461)+P3(x461,f9(x461))+~P4(f3(x461)) % 0.23/0.53 [47]P2(x471)+P3(x471,f9(x471))+~P1(f10(x471)) % 0.23/0.53 [48]P2(x481)+P3(x481,f10(x481))+~P4(f9(x481)) % 0.23/0.53 [49]P2(x491)+P3(x491,f10(x491))+~P1(f8(x491)) % 0.23/0.53 [50]P2(x501)+P3(x501,f9(x501))+P3(x501,f10(x501)) % 0.23/0.53 [51]P2(x511)+P3(f9(x511),f8(x511))+~P4(f3(x511)) % 0.23/0.53 [52]P2(x521)+P3(f9(x521),f8(x521))+~P1(f10(x521)) % 0.23/0.53 [53]P2(x531)+P3(f10(x531),f3(x531))+~P4(f9(x531)) % 0.23/0.53 [54]P2(x541)+P3(f10(x541),f3(x541))+~P1(f8(x541)) % 0.23/0.53 [55]P2(x551)+P3(x551,f9(x551))+P3(f10(x551),f3(x551)) % 0.23/0.53 [56]P2(x561)+P3(x561,f10(x561))+P3(f9(x561),f8(x561)) % 0.23/0.53 [69]P2(x691)+P3(f9(x691),f8(x691))+P3(f10(x691),f3(x691)) % 0.23/0.53 [57]P4(x571)+P2(x572)+~P3(f10(x572),x571)+P4(f8(x572)) % 0.23/0.53 [58]P4(x581)+P2(x582)+~P3(f8(x582),x581)+P4(f10(x582)) % 0.23/0.53 [60]P4(x601)+P2(x602)+~P3(f10(x602),x601)+P1(f9(x602)) % 0.23/0.53 [62]P4(x621)+P2(x622)+~P3(f8(x622),x621)+P1(f3(x622)) % 0.23/0.53 [63]P1(x631)+P2(x632)+~P3(f3(x632),x631)+P4(f8(x632)) % 0.23/0.53 [64]P1(x641)+P2(x642)+~P3(f9(x642),x641)+P4(f10(x642)) % 0.23/0.53 [66]P1(x661)+P2(x662)+~P3(f3(x662),x661)+P1(f9(x662)) % 0.23/0.53 [68]P1(x681)+P2(x682)+~P3(f9(x682),x681)+P1(f3(x682)) % 0.23/0.53 [70]P4(x701)+P2(x702)+~P3(f10(x702),x701)+~P4(f9(x702)) % 0.23/0.53 [71]P4(x711)+P2(x712)+~P3(f8(x712),x711)+~P4(f3(x712)) % 0.23/0.53 [72]P4(x721)+P2(x722)+~P3(f10(x722),x721)+~P1(f8(x722)) % 0.23/0.53 [73]P4(x731)+P2(x732)+~P3(f8(x732),x731)+~P1(f10(x732)) % 0.23/0.53 [74]P1(x741)+P2(x742)+~P3(f3(x742),x741)+~P4(f9(x742)) % 0.23/0.53 [75]P1(x751)+P2(x752)+~P3(f9(x752),x751)+~P4(f3(x752)) % 0.23/0.53 [76]P1(x761)+P2(x762)+~P3(f3(x762),x761)+~P1(f8(x762)) % 0.23/0.53 [77]P1(x771)+P2(x772)+~P3(f9(x772),x771)+~P1(f10(x772)) % 0.23/0.53 [78]P4(x781)+P2(x782)+P3(x782,f9(x782))+~P3(f10(x782),x781) % 0.23/0.53 [79]P4(x791)+P2(x792)+P3(x792,f10(x792))+~P3(f8(x792),x791) % 0.23/0.53 [80]P1(x801)+P2(x802)+P3(x802,f9(x802))+~P3(f3(x802),x801) % 0.23/0.53 [81]P1(x811)+P2(x812)+P3(x812,f10(x812))+~P3(f9(x812),x811) % 0.23/0.53 [82]P4(x821)+P2(x822)+P3(f9(x822),f8(x822))+~P3(f10(x822),x821) % 0.23/0.53 [83]P4(x831)+P2(x832)+P3(f10(x832),f3(x832))+~P3(f8(x832),x831) % 0.23/0.53 [84]P1(x841)+P2(x842)+P3(f9(x842),f8(x842))+~P3(f3(x842),x841) % 0.23/0.53 [85]P1(x851)+P2(x852)+P3(f10(x852),f3(x852))+~P3(f9(x852),x851) % 0.23/0.53 [86]P4(x861)+P4(x862)+P2(x863)+~P3(f8(x863),x861)+~P3(f10(x863),x862) % 0.23/0.53 [87]P4(x871)+P1(x872)+P2(x873)+~P3(f8(x873),x871)+~P3(f3(x873),x872) % 0.23/0.53 [88]P4(x881)+P1(x882)+P2(x883)+~P3(f9(x883),x882)+~P3(f10(x883),x881) % 0.23/0.53 [89]P1(x891)+P1(x892)+P2(x893)+~P3(f9(x893),x891)+~P3(f3(x893),x892) % 0.23/0.53 [90]~P4(x902)+~P1(x901)+P4(x901)+P1(x902)+~P3(a2,x902)+~P3(a2,x901)+P4(a4)+~P2(a2)+~P4(f5(x902))+~P1(f6(x901)) % 0.23/0.53 [92]~P4(x922)+~P1(x921)+P4(x921)+P1(x922)+~P3(a2,x922)+~P3(a2,x921)+P1(a4)+~P2(a2)+~P4(f5(x922))+~P1(f6(x921)) % 0.23/0.53 [93]~P4(x932)+~P1(x931)+P4(x931)+P1(x932)+~P3(a2,x932)+~P3(a2,x931)+~P4(a4)+~P2(a2)+~P4(f5(x932))+~P1(f6(x931)) % 0.23/0.53 [94]~P4(x942)+~P1(x941)+P4(x941)+P1(x942)+~P3(a2,x942)+~P3(a2,x941)+~P1(a4)+~P2(a2)+~P4(f5(x942))+~P1(f6(x941)) % 0.23/0.53 [95]~P4(x952)+~P1(x951)+P4(x951)+P1(x952)+P3(x952,f5(x952))+~P3(a2,x952)+~P3(a2,x951)+P4(a4)+~P2(a2)+~P1(f6(x951)) % 0.23/0.53 [96]~P4(x962)+~P1(x961)+P4(x961)+P1(x962)+P3(x961,f6(x961))+~P3(a2,x962)+~P3(a2,x961)+P4(a4)+~P2(a2)+~P4(f5(x962)) % 0.23/0.53 [98]~P4(x982)+~P1(x981)+P4(x981)+P1(x982)+P3(x982,f5(x982))+~P3(a2,x982)+~P3(a2,x981)+P1(a4)+~P2(a2)+~P1(f6(x981)) % 0.23/0.53 [100]~P4(x1002)+~P1(x1001)+P4(x1001)+P1(x1002)+P3(x1001,f6(x1001))+~P3(a2,x1002)+~P3(a2,x1001)+P1(a4)+~P2(a2)+~P4(f5(x1002)) % 0.23/0.53 [101]~P4(x1012)+~P1(x1011)+P4(x1011)+P1(x1012)+P3(x1012,f5(x1012))+~P3(a2,x1012)+~P3(a2,x1011)+~P4(a4)+~P2(a2)+~P1(f6(x1011)) % 0.23/0.53 [102]~P4(x1022)+~P1(x1021)+P4(x1021)+P1(x1022)+P3(x1022,f5(x1022))+~P3(a2,x1022)+~P3(a2,x1021)+~P1(a4)+~P2(a2)+~P1(f6(x1021)) % 0.23/0.53 [103]~P4(x1032)+~P1(x1031)+P4(x1031)+P1(x1032)+P3(x1031,f6(x1031))+~P3(a2,x1032)+~P3(a2,x1031)+~P4(a4)+~P2(a2)+~P4(f5(x1032)) % 0.23/0.53 [104]~P4(x1042)+~P1(x1041)+P4(x1041)+P1(x1042)+P3(x1041,f6(x1041))+~P3(a2,x1042)+~P3(a2,x1041)+~P1(a4)+~P2(a2)+~P4(f5(x1042)) % 0.23/0.53 [105]~P4(x1052)+~P1(x1051)+P4(x1051)+P1(x1052)+P3(x1052,f5(x1052))+P3(x1051,f6(x1051))+~P3(a2,x1052)+~P3(a2,x1051)+P4(a4)+~P2(a2) % 0.23/0.53 [107]~P4(x1072)+~P1(x1071)+P4(x1071)+P1(x1072)+P3(x1072,f5(x1072))+P3(x1071,f6(x1071))+~P3(a2,x1072)+~P3(a2,x1071)+P1(a4)+~P2(a2) % 0.23/0.53 [108]~P4(x1082)+~P1(x1081)+P4(x1081)+P1(x1082)+~P3(a2,x1082)+~P3(a2,x1081)+P3(a2,a4)+~P2(a2)+~P4(f5(x1082))+~P1(f6(x1081)) % 0.23/0.53 [109]~P4(x1092)+~P1(x1091)+P4(x1091)+P1(x1092)+P3(x1092,f5(x1092))+P3(x1091,f6(x1091))+~P3(a2,x1092)+~P3(a2,x1091)+~P4(a4)+~P2(a2) % 0.23/0.53 [110]~P4(x1102)+~P1(x1101)+P4(x1101)+P1(x1102)+P3(x1102,f5(x1102))+P3(x1101,f6(x1101))+~P3(a2,x1102)+~P3(a2,x1101)+~P1(a4)+~P2(a2) % 0.23/0.53 [111]~P4(x1112)+~P1(x1111)+P4(x1111)+P1(x1112)+P3(x1112,f5(x1112))+P3(a2,a4)+~P3(a2,x1112)+~P3(a2,x1111)+~P2(a2)+~P1(f6(x1111)) % 0.23/0.53 [112]~P4(x1122)+~P1(x1121)+P4(x1121)+P1(x1122)+P3(a2,a4)+P3(x1121,f6(x1121))+~P3(a2,x1122)+~P3(a2,x1121)+~P2(a2)+~P4(f5(x1122)) % 0.23/0.53 [113]~P4(x1132)+~P1(x1131)+P4(x1131)+P1(x1132)+P3(a2,a4)+P3(x1132,f5(x1132))+P3(x1131,f6(x1131))+~P3(a2,x1132)+~P3(a2,x1131)+~P2(a2) % 0.23/0.53 [114]~P4(x1143)+~P1(x1141)+P4(x1141)+P4(x1142)+P1(x1143)+~P3(a2,x1143)+~P3(a2,x1141)+~P3(a4,x1142)+~P2(a2)+~P4(f5(x1143))+~P1(f6(x1141)) % 0.23/0.53 [115]~P4(x1152)+~P1(x1151)+P4(x1151)+P1(x1152)+P1(x1153)+~P3(a2,x1152)+~P3(a2,x1151)+~P3(a4,x1153)+~P2(a2)+~P4(f5(x1152))+~P1(f6(x1151)) % 0.23/0.53 [116]~P4(x1163)+~P1(x1161)+P4(x1161)+P4(x1162)+P1(x1163)+P3(x1163,f5(x1163))+~P3(a2,x1163)+~P3(a2,x1161)+~P3(a4,x1162)+~P2(a2)+~P1(f6(x1161)) % 0.23/0.53 [117]~P4(x1173)+~P1(x1171)+P4(x1171)+P4(x1172)+P1(x1173)+P3(x1171,f6(x1171))+~P3(a2,x1173)+~P3(a2,x1171)+~P3(a4,x1172)+~P2(a2)+~P4(f5(x1173)) % 0.23/0.53 [118]~P4(x1182)+~P1(x1181)+P4(x1181)+P1(x1182)+P1(x1183)+P3(x1182,f5(x1182))+~P3(a2,x1182)+~P3(a2,x1181)+~P3(a4,x1183)+~P2(a2)+~P1(f6(x1181)) % 0.23/0.53 [119]~P4(x1192)+~P1(x1191)+P4(x1191)+P1(x1192)+P1(x1193)+P3(x1191,f6(x1191))+~P3(a2,x1192)+~P3(a2,x1191)+~P3(a4,x1193)+~P2(a2)+~P4(f5(x1192)) % 0.23/0.53 [120]~P4(x1203)+~P1(x1201)+P4(x1201)+P4(x1202)+P1(x1203)+P3(x1203,f5(x1203))+P3(x1201,f6(x1201))+~P3(a2,x1203)+~P3(a2,x1201)+~P3(a4,x1202)+~P2(a2) % 0.23/0.54 [121]~P4(x1212)+~P1(x1211)+P4(x1211)+P1(x1212)+P1(x1213)+P3(x1212,f5(x1212))+P3(x1211,f6(x1211))+~P3(a2,x1212)+~P3(a2,x1211)+~P3(a4,x1213)+~P2(a2) % 0.23/0.54 %EqnAxiom % 0.23/0.54 % 0.23/0.54 %------------------------------------------- % 0.23/0.54 cnf(122,plain, % 0.23/0.54 ($false), % 0.23/0.54 inference(scs_inference,[],[1,5]), % 0.23/0.54 ['proof']). % 0.23/0.54 % SZS output end Proof % 0.23/0.54 % Total time :0.005539s %------------------------------------------------------------------------------