%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LCL686+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 : n028.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:39 AM UTC 2026 % Result : Theorem 2.73s 2.95s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.02 % Problem : LCL686+1.005 : 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.08/0.35 % Computer : n028.cluster.edu % 0.08/0.35 % Model : x86_64 x86_64 % 0.08/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.08/0.35 % Memory : 8046.5625MB % 0.08/0.35 % OS : Linux 6.8.0-71-generic % 0.08/0.35 % CPULimit : 300 % 0.08/0.35 % WCLimit : 300 % 0.08/0.35 % DateTime : Fri Sep 4 18:48:58 UTC 2026 % 0.11/0.35 % CPUTime : % 0.22/0.51 start to proof:theBenchmark % 2.73/2.93 %------------------------------------------- % 2.73/2.93 % File :CSE---1.7 % 2.73/2.93 % Problem :theBenchmark % 2.73/2.93 % Transform :cnf % 2.73/2.93 % Format :tptp:raw % 2.73/2.93 % Command :java -jar mcs_scs.jar %d %s % 2.73/2.93 % 2.73/2.93 % Result :Theorem 2.431616s % 2.73/2.93 % Output :CNFRefutation 2.431616s % 2.73/2.93 %------------------------------------------- % 2.73/2.93 %------------------------------------------------------------------------------ % 2.73/2.93 % File : LCL686+1.005 : TPTP v9.3.1. Released v4.0.0. % 2.73/2.93 % Domain : Logic Calculi (Modal Logic) % 2.73/2.93 % Problem : In S4, formula provable in S5 embedding, size 5 % 2.73/2.93 % Version : Especial. % 2.73/2.93 % English : % 2.73/2.93 % 2.73/2.93 % Refs : [BHS00] Balsiger et al. (2000), A Benchmark Method for the Pro % 2.73/2.93 % : [Kam08] Kaminski (2008), Email to G. Sutcliffe % 2.73/2.93 % Source : [Kam08] % 2.73/2.93 % Names : s4_s5_p [BHS00] % 2.73/2.93 % 2.73/2.93 % Status : Theorem % 2.73/2.94 % Rating : 0.00 v9.1.0, 0.07 v9.0.0, 0.00 v7.5.0, 0.05 v7.4.0, 0.00 v6.3.0, 0.08 v6.2.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.11 v4.0.0 % 2.73/2.94 % Syntax : Number of formulae : 3 ( 1 unt; 0 def) % 2.73/2.94 % Number of atoms : 144 ( 0 equ) % 2.73/2.94 % Maximal formula atoms : 140 ( 48 avg) % 2.73/2.94 % Number of connectives : 257 ( 116 ~; 87 |; 53 &) % 2.73/2.94 % ( 0 <=>; 1 =>; 0 <=; 0 <~>) % 2.73/2.94 % Maximal formula depth : 55 ( 21 avg) % 2.73/2.94 % Maximal term depth : 1 ( 1 avg) % 2.73/2.94 % Number of predicates : 17 ( 16 usr; 1 prp; 0-2 aty) % 2.73/2.94 % Number of functors : 0 ( 0 usr; 0 con; --- aty) % 2.73/2.94 % Number of variables : 37 ( 36 !; 1 ?) % 2.73/2.94 % SPC : FOF_THM_RFO_NEQ % 2.73/2.94 % 2.73/2.94 % Comments : A naive relational encoding of the modal logic problem into % 2.73/2.94 % first-order logic. % 2.73/2.94 %------------------------------------------------------------------------------ % 2.73/2.94 fof(reflexivity,axiom, % 2.73/2.94 ! [X] : r1(X,X) ). % 2.73/2.94 % 2.73/2.94 fof(transitivity,axiom, % 2.73/2.94 ! [X,Y,Z] : % 2.73/2.94 ( ( r1(X,Y) % 2.73/2.94 & r1(Y,Z) ) % 2.73/2.94 => r1(X,Z) ) ). % 2.73/2.94 % 2.73/2.94 fof(main,conjecture, % 2.73/2.94 ~ ? [X] : % 2.73/2.94 ~ ( ! [Y] : % 2.73/2.94 ( ~ r1(X,Y) % 2.73/2.94 | ~ p15(Y) % 2.73/2.94 | ! [X] : % 2.73/2.94 ( ~ r1(Y,X) % 2.73/2.94 | ~ p1(X) ) ) % 2.73/2.94 | ! [Y] : % 2.73/2.94 ( ~ r1(X,Y) % 2.73/2.94 | ~ ! [X] : % 2.73/2.94 ( ~ r1(Y,X) % 2.73/2.94 | ~ ( ! [Y] : % 2.73/2.94 ( ~ r1(X,Y) % 2.73/2.94 | ! [X] : % 2.73/2.94 ( ~ r1(Y,X) % 2.73/2.94 | ! [Y] : % 2.73/2.94 ( ~ r1(X,Y) % 2.73/2.94 | ! [X] : % 2.73/2.94 ( ~ r1(Y,X) % 2.73/2.94 | ! [Y] : % 2.73/2.94 ( ~ r1(X,Y) % 2.73/2.94 | ! [X] : % 2.73/2.94 ( ~ r1(Y,X) % 2.73/2.94 | ! [Y] : % 2.73/2.94 ( ~ r1(X,Y) % 2.73/2.94 | ! [X] : % 2.73/2.94 ( ~ r1(Y,X) % 2.73/2.94 | ! [Y] : % 2.73/2.94 ( ~ r1(X,Y) % 2.73/2.94 | ! [X] : % 2.73/2.94 ( ~ r1(Y,X) % 2.73/2.94 | ! [Y] : % 2.73/2.94 ( ~ r1(X,Y) % 2.73/2.94 | ! [X] : % 2.73/2.94 ( ~ r1(Y,X) % 2.73/2.94 | ! [Y] : % 2.73/2.94 ( ~ r1(X,Y) % 2.73/2.94 | $false ) % 2.73/2.94 | ~ ! [Y] : % 2.73/2.94 ( ~ r1(X,Y) % 2.73/2.94 | ~ ( ( p14(Y) % 2.73/2.94 & ~ p13(Y) ) % 2.73/2.94 | ( ~ p14(Y) % 2.73/2.94 & p13(Y) ) ) ) ) % 2.73/2.94 | ~ ! [X] : % 2.73/2.94 ( ~ r1(Y,X) % 2.73/2.94 | ~ ( ( p13(X) % 2.73/2.94 & ~ p12(X) ) % 2.73/2.94 | ( ~ p13(X) % 2.73/2.94 & p12(X) ) ) ) ) % 2.73/2.94 | ~ ! [Y] : % 2.73/2.94 ( ~ r1(X,Y) % 2.73/2.94 | ~ ( ( p12(Y) % 2.73/2.94 & ~ p11(Y) ) % 2.73/2.94 | ( ~ p12(Y) % 2.73/2.94 & p11(Y) ) ) ) ) % 2.73/2.94 | ~ ! [X] : % 2.73/2.94 ( ~ r1(Y,X) % 2.73/2.94 | ~ ( ( p11(X) % 2.73/2.94 & ~ p10(X) ) % 2.73/2.94 | ( ~ p11(X) % 2.73/2.94 & p10(X) ) ) ) ) % 2.73/2.94 | ~ ! [Y] : % 2.73/2.94 ( ~ r1(X,Y) % 2.73/2.94 | ~ ( ( p10(Y) % 2.73/2.94 & ~ p9(Y) ) % 2.73/2.94 | ( ~ p10(Y) % 2.73/2.94 & p9(Y) ) ) ) ) % 2.73/2.94 | ~ ! [X] : % 2.73/2.94 ( ~ r1(Y,X) % 2.73/2.94 | ~ ( ( p9(X) % 2.73/2.94 & ~ p8(X) ) % 2.73/2.94 | ( ~ p9(X) % 2.73/2.94 & p8(X) ) ) ) ) % 2.73/2.94 | ~ ! [Y] : % 2.73/2.94 ( ~ r1(X,Y) % 2.73/2.94 | ~ ( ( p8(Y) % 2.73/2.94 & ~ p7(Y) ) % 2.73/2.94 | ( ~ p8(Y) % 2.73/2.94 & p7(Y) ) ) ) ) % 2.73/2.94 | ~ ! [X] : % 2.73/2.94 ( ~ r1(Y,X) % 2.73/2.94 | ~ ( ( p7(X) % 2.73/2.94 & ~ p6(X) ) % 2.73/2.94 | ( ~ p7(X) % 2.73/2.94 & p6(X) ) ) ) ) % 2.73/2.94 | ~ ! [Y] : % 2.73/2.94 ( ~ r1(X,Y) % 2.73/2.94 | ~ ( ( p6(Y) % 2.73/2.94 & ~ p5(Y) ) % 2.73/2.94 | ( ~ p6(Y) % 2.73/2.94 & p5(Y) ) ) ) ) % 2.73/2.94 | ~ ! [X] : % 2.73/2.94 ( ~ r1(Y,X) % 2.73/2.94 | ~ ( ( p5(X) % 2.73/2.94 & ~ p4(X) ) % 2.73/2.94 | ( ~ p5(X) % 2.73/2.94 & p4(X) ) ) ) ) % 2.73/2.94 | ~ ! [Y] : % 2.73/2.94 ( ~ r1(X,Y) % 2.73/2.94 | ~ ( ( p4(Y) % 2.73/2.94 & ~ p3(Y) ) % 2.73/2.94 | ( ~ p4(Y) % 2.73/2.94 & p3(Y) ) ) ) ) % 2.73/2.94 | ~ ! [X] : % 2.73/2.94 ( ~ r1(Y,X) % 2.73/2.94 | ~ ( ( p3(X) % 2.73/2.94 & ~ p2(X) ) % 2.73/2.94 | ( ~ p3(X) % 2.73/2.94 & p2(X) ) ) ) ) % 2.73/2.94 | ~ ! [Y] : % 2.73/2.94 ( ~ r1(X,Y) % 2.73/2.94 | ~ ( ( p2(Y) % 2.73/2.94 & ~ p1(Y) ) % 2.73/2.94 | ( ~ p2(Y) % 2.73/2.94 & p1(Y) ) ) ) % 2.73/2.94 | ! [Y] : % 2.73/2.94 ( ~ r1(X,Y) % 2.73/2.94 | p15(Y) ) % 2.73/2.94 | ! [Y] : % 2.73/2.94 ( ~ r1(X,Y) % 2.73/2.94 | ( ~ p13(Y) % 2.73/2.94 & ~ p14(Y) ) % 2.73/2.94 | ( p14(Y) % 2.73/2.94 & p13(Y) ) % 2.73/2.94 | ( ~ p12(Y) % 2.73/2.95 & ~ p13(Y) ) % 2.73/2.95 | ( p13(Y) % 2.73/2.95 & p12(Y) ) % 2.73/2.95 | ( ~ p11(Y) % 2.73/2.95 & ~ p12(Y) ) % 2.73/2.95 | ( p12(Y) % 2.73/2.95 & p11(Y) ) % 2.73/2.95 | ( ~ p10(Y) % 2.73/2.95 & ~ p11(Y) ) % 2.73/2.95 | ( p11(Y) % 2.73/2.95 & p10(Y) ) % 2.73/2.95 | ( ~ p9(Y) % 2.73/2.95 & ~ p10(Y) ) % 2.73/2.95 | ( p10(Y) % 2.73/2.95 & p9(Y) ) % 2.73/2.95 | ( ~ p8(Y) % 2.73/2.95 & ~ p9(Y) ) % 2.73/2.95 | ( p9(Y) % 2.73/2.95 & p8(Y) ) % 2.73/2.95 | ( ~ p7(Y) % 2.73/2.95 & ~ p8(Y) ) % 2.73/2.95 | ( p8(Y) % 2.73/2.95 & p7(Y) ) % 2.73/2.95 | ( ~ p6(Y) % 2.73/2.95 & ~ p7(Y) ) % 2.73/2.95 | ( p7(Y) % 2.73/2.95 & p6(Y) ) % 2.73/2.95 | ( ~ p5(Y) % 2.73/2.95 & ~ p6(Y) ) % 2.73/2.95 | ( p6(Y) % 2.73/2.95 & p5(Y) ) % 2.73/2.95 | ( ~ p4(Y) % 2.73/2.95 & ~ p5(Y) ) % 2.73/2.95 | ( p5(Y) % 2.73/2.95 & p4(Y) ) % 2.73/2.95 | ( ~ p3(Y) % 2.73/2.95 & ~ p4(Y) ) % 2.73/2.95 | ( p4(Y) % 2.73/2.95 & p3(Y) ) % 2.73/2.95 | ( ~ p2(Y) % 2.73/2.95 & ~ p3(Y) ) % 2.73/2.95 | ( p3(Y) % 2.73/2.95 & p2(Y) ) % 2.73/2.95 | ( ~ p1(Y) % 2.73/2.95 & ~ p2(Y) ) % 2.73/2.95 | ( p2(Y) % 2.73/2.95 & p1(Y) ) ) ) ) ) ) ). % 2.73/2.95 % 2.73/2.95 %------------------------------------------------------------------------------ % 2.73/2.95 %------------------------------------------- % 2.73/2.95 % Proof found % 2.73/2.95 % SZS status Theorem for theBenchmark % 2.73/2.95 % SZS output start Proof % 2.73/2.95 %ClaNum:76(EqnAxiom:0) % 2.73/2.95 %VarNum:265(SingletonVarNum:99) % 2.73/2.95 %MaxLitNum:4 % 2.73/2.95 %MaxfuncDepth:1 % 2.73/2.95 %SharedTerms:9 % 2.73/2.95 %goalClause: 1 2 3 4 5 8 % 2.73/2.95 %singleGoalClaCount:5 % 2.73/2.95 [1]P1(a1) % 2.73/2.95 [2]P2(a13) % 2.73/2.95 [3]P9(a2,a1) % 2.73/2.95 [4]P9(a2,a14) % 2.73/2.95 [5]P9(a1,a13) % 2.73/2.95 [6]P9(x61,x61) % 2.73/2.95 [8]P3(x81)+~P9(a14,x81) % 2.73/2.95 [7]~P3(x71)+~P1(f3(x71)) % 2.73/2.95 [9]~P3(x91)+P9(x91,f15(x91)) % 2.73/2.95 [10]~P3(x101)+P9(x101,f3(x101)) % 2.73/2.95 [11]~P3(x111)+P9(x111,f12(x111)) % 2.73/2.95 [25]~P3(x251)+P9(f15(x251),f16(x251)) % 2.73/2.95 [26]~P3(x261)+P9(f16(x261),f17(x261)) % 2.73/2.95 [27]~P3(x271)+P9(f17(x271),f18(x271)) % 2.73/2.95 [28]~P3(x281)+P9(f18(x281),f19(x281)) % 2.73/2.95 [29]~P3(x291)+P9(f19(x291),f4(x291)) % 2.73/2.95 [30]~P3(x301)+P9(f4(x301),f5(x301)) % 2.73/2.95 [31]~P3(x311)+P9(f5(x311),f6(x311)) % 2.73/2.95 [32]~P3(x321)+P9(f6(x321),f7(x321)) % 2.73/2.95 [33]~P3(x331)+P9(f7(x331),f8(x331)) % 2.73/2.95 [34]~P3(x341)+P9(f8(x341),f9(x341)) % 2.73/2.95 [35]~P3(x351)+P9(f9(x351),f10(x351)) % 2.73/2.95 [36]~P3(x361)+P9(f10(x361),f11(x361)) % 2.73/2.95 [12]~P3(x121)+P2(f12(x121))+P10(f12(x121)) % 2.73/2.95 [13]~P3(x131)+P4(f12(x131))+P5(f12(x131)) % 2.73/2.95 [14]~P3(x141)+P5(f12(x141))+P6(f12(x141)) % 2.73/2.95 [15]~P3(x151)+P6(f12(x151))+P7(f12(x151)) % 2.73/2.95 [16]~P3(x161)+P7(f12(x161))+P8(f12(x161)) % 2.73/2.95 [17]~P3(x171)+P8(f12(x171))+P11(f12(x171)) % 2.73/2.95 [18]~P3(x181)+P11(f12(x181))+P12(f12(x181)) % 2.73/2.95 [19]~P3(x191)+P12(f12(x191))+P13(f12(x191)) % 2.73/2.95 [20]~P3(x201)+P13(f12(x201))+P14(f12(x201)) % 2.73/2.95 [21]~P3(x211)+P14(f12(x211))+P15(f12(x211)) % 2.73/2.95 [22]~P3(x221)+P15(f12(x221))+P16(f12(x221)) % 2.73/2.95 [23]~P3(x231)+P16(f12(x231))+P17(f12(x231)) % 2.73/2.95 [24]~P3(x241)+P17(f12(x241))+P10(f12(x241)) % 2.73/2.95 [37]~P3(x371)+~P2(f12(x371))+~P10(f12(x371)) % 2.73/2.95 [38]~P3(x381)+~P4(f12(x381))+~P5(f12(x381)) % 2.73/2.95 [39]~P3(x391)+~P5(f12(x391))+~P6(f12(x391)) % 2.73/2.95 [40]~P3(x401)+~P6(f12(x401))+~P7(f12(x401)) % 2.73/2.95 [41]~P3(x411)+~P7(f12(x411))+~P8(f12(x411)) % 2.73/2.95 [42]~P3(x421)+~P8(f12(x421))+~P11(f12(x421)) % 2.73/2.95 [43]~P3(x431)+~P11(f12(x431))+~P12(f12(x431)) % 2.73/2.95 [44]~P3(x441)+~P12(f12(x441))+~P13(f12(x441)) % 2.73/2.95 [45]~P3(x451)+~P13(f12(x451))+~P14(f12(x451)) % 2.73/2.95 [46]~P3(x461)+~P14(f12(x461))+~P15(f12(x461)) % 2.73/2.95 [47]~P3(x471)+~P15(f12(x471))+~P16(f12(x471)) % 2.73/2.95 [48]~P3(x481)+~P16(f12(x481))+~P17(f12(x481)) % 2.73/2.95 [49]~P3(x491)+~P17(f12(x491))+~P10(f12(x491)) % 2.73/2.95 [76]~P9(x761,x763)+P9(x761,x762)+~P9(x763,x762) % 2.73/2.95 [50]~P10(x501)+~P9(x502,x501)+P2(x501)+~P3(x502) % 2.73/2.95 [51]~P2(x511)+~P9(x512,x511)+P10(x511)+~P3(x512) % 2.73/2.95 [52]~P5(x521)+P4(x521)+~P3(x522)+~P9(f10(x522),x521) % 2.73/2.95 [53]~P4(x531)+P5(x531)+~P3(x532)+~P9(f10(x532),x531) % 2.73/2.95 [54]~P6(x541)+P5(x541)+~P3(x542)+~P9(f9(x542),x541) % 2.73/2.95 [55]~P5(x551)+P6(x551)+~P3(x552)+~P9(f9(x552),x551) % 2.73/2.95 [56]~P7(x561)+P6(x561)+~P3(x562)+~P9(f8(x562),x561) % 2.73/2.95 [57]~P6(x571)+P7(x571)+~P3(x572)+~P9(f8(x572),x571) % 2.73/2.95 [58]~P8(x581)+P7(x581)+~P3(x582)+~P9(f7(x582),x581) % 2.73/2.95 [59]~P7(x591)+P8(x591)+~P3(x592)+~P9(f7(x592),x591) % 2.73/2.95 [60]~P11(x601)+P8(x601)+~P3(x602)+~P9(f6(x602),x601) % 2.73/2.95 [61]~P8(x611)+P11(x611)+~P3(x612)+~P9(f6(x612),x611) % 2.73/2.95 [62]~P12(x621)+P11(x621)+~P3(x622)+~P9(f5(x622),x621) % 2.73/2.95 [63]~P11(x631)+P12(x631)+~P3(x632)+~P9(f5(x632),x631) % 2.73/2.95 [64]~P13(x641)+P12(x641)+~P3(x642)+~P9(f4(x642),x641) % 2.73/2.95 [65]~P12(x651)+P13(x651)+~P3(x652)+~P9(f4(x652),x651) % 2.73/2.95 [66]~P14(x661)+P13(x661)+~P3(x662)+~P9(f19(x662),x661) % 2.73/2.95 [67]~P13(x671)+P14(x671)+~P3(x672)+~P9(f19(x672),x671) % 2.73/2.95 [68]~P15(x681)+P14(x681)+~P3(x682)+~P9(f18(x682),x681) % 2.73/2.95 [69]~P14(x691)+P15(x691)+~P3(x692)+~P9(f18(x692),x691) % 2.73/2.95 [70]~P16(x701)+P15(x701)+~P3(x702)+~P9(f17(x702),x701) % 2.73/2.95 [71]~P15(x711)+P16(x711)+~P3(x712)+~P9(f17(x712),x711) % 2.73/2.95 [72]~P17(x721)+P16(x721)+~P3(x722)+~P9(f16(x722),x721) % 2.73/2.95 [73]~P16(x731)+P17(x731)+~P3(x732)+~P9(f16(x732),x731) % 2.73/2.95 [74]~P10(x741)+P17(x741)+~P3(x742)+~P9(f15(x742),x741) % 2.73/2.95 [75]~P17(x751)+P10(x751)+~P3(x752)+~P9(f15(x752),x751) % 2.73/2.95 %EqnAxiom % 2.73/2.95 % 2.73/2.95 %------------------------------------------- % 2.73/2.95 cnf(77,plain, % 2.73/2.95 (P3(a14)), % 2.73/2.95 inference(scs_inference,[],[6,8])). % 2.73/2.95 cnf(296,plain, % 2.73/2.95 (P9(a14,f15(a14))), % 2.73/2.95 inference(scs_inference,[],[6,9,8])). % 2.73/2.95 cnf(297,plain, % 2.73/2.95 (P3(f15(a14))), % 2.73/2.95 inference(scs_inference,[],[296,8])). % 2.73/2.95 cnf(912,plain, % 2.73/2.95 (P7(f12(f15(a14)))+P8(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[296,16,8])). % 2.73/2.95 cnf(913,plain, % 2.73/2.95 (P8(f12(f15(a14)))+~P6(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[297,912,40])). % 2.73/2.95 cnf(914,plain, % 2.73/2.95 (~P6(f12(f15(a14)))+~P7(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[297,913,41])). % 2.73/2.95 cnf(915,plain, % 2.73/2.95 (~P7(f12(f15(a14)))+P5(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[297,914,14])). % 2.73/2.95 cnf(916,plain, % 2.73/2.95 (P5(f12(f15(a14)))+P8(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[915,912])). % 2.73/2.95 cnf(917,plain, % 2.73/2.95 (P8(f12(f15(a14)))+~P4(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[297,916,38])). % 2.73/2.95 cnf(918,plain, % 2.73/2.95 (~P4(f12(f15(a14)))+~P11(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[297,917,42])). % 2.73/2.95 cnf(919,plain, % 2.73/2.95 (~P11(f12(f15(a14)))+P5(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[297,918,13])). % 2.73/2.95 cnf(920,plain, % 2.73/2.95 (P5(f12(f15(a14)))+P12(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[297,919,18])). % 2.73/2.95 cnf(921,plain, % 2.73/2.95 (P12(f12(f15(a14)))+~P6(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[297,920,39])). % 2.73/2.95 cnf(922,plain, % 2.73/2.95 (~P6(f12(f15(a14)))+~P11(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[297,921,43])). % 2.73/2.95 cnf(923,plain, % 2.73/2.95 (~P11(f12(f15(a14)))+P7(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[297,922,15])). % 2.73/2.95 cnf(924,plain, % 2.73/2.95 (P7(f12(f15(a14)))+P12(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[297,923,18])). % 2.73/2.95 cnf(925,plain, % 2.73/2.95 (P12(f12(f15(a14)))+~P8(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[297,924,41])). % 2.73/2.95 cnf(937,plain, % 2.73/2.95 (P16(f12(f15(a14)))+P17(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[296,23,8])). % 2.73/2.95 cnf(938,plain, % 2.73/2.95 (P17(f12(f15(a14)))+~P15(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[297,937,47])). % 2.73/2.95 cnf(939,plain, % 2.73/2.95 (~P15(f12(f15(a14)))+~P16(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[297,938,48])). % 2.73/2.95 cnf(940,plain, % 2.73/2.95 (~P16(f12(f15(a14)))+P14(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[297,939,21])). % 2.73/2.95 cnf(941,plain, % 2.73/2.95 (P14(f12(f15(a14)))+P17(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[940,937])). % 2.73/2.95 cnf(942,plain, % 2.73/2.95 (P17(f12(f15(a14)))+~P13(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[297,941,45])). % 2.73/2.95 cnf(943,plain, % 2.73/2.95 (~P13(f12(f15(a14)))+~P10(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[297,942,49])). % 2.73/2.95 cnf(944,plain, % 2.73/2.95 (~P10(f12(f15(a14)))+P12(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[297,943,19])). % 2.73/2.95 cnf(945,plain, % 2.73/2.95 (P12(f12(f15(a14)))+P2(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[297,944,12])). % 2.73/2.95 cnf(946,plain, % 2.73/2.95 (P2(f12(f15(a14)))+~P11(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[297,945,43])). % 2.73/2.95 cnf(947,plain, % 2.73/2.95 (~P11(f12(f15(a14)))+~P10(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[297,946,37])). % 2.73/2.95 cnf(948,plain, % 2.73/2.95 (~P10(f12(f15(a14)))+P8(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[297,947,17])). % 2.73/2.95 cnf(949,plain, % 2.73/2.95 (P8(f12(f15(a14)))+P17(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[297,948,24])). % 2.73/2.95 cnf(950,plain, % 2.73/2.95 (P17(f12(f15(a14)))+P12(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[949,925])). % 2.73/2.95 cnf(951,plain, % 2.73/2.95 (P12(f12(f15(a14)))+~P16(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[297,950,48])). % 2.73/2.95 cnf(952,plain, % 2.73/2.95 (~P16(f12(f15(a14)))+~P13(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[297,951,44])). % 2.73/2.95 cnf(953,plain, % 2.73/2.95 (~P13(f12(f15(a14)))+P15(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[297,952,22])). % 2.73/2.95 cnf(954,plain, % 2.73/2.95 (P15(f12(f15(a14)))+P14(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[297,953,20])). % 2.73/2.95 cnf(1761,plain, % 2.73/2.95 (P9(f15(a14),f15(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[296,8,9])). % 2.73/2.95 cnf(1762,plain, % 2.73/2.95 (P9(a14,f15(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[296,1761,76])). % 2.73/2.95 cnf(1766,plain, % 2.73/2.95 (P9(f15(a14),f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[296,8,11])). % 2.73/2.95 cnf(1769,plain, % 2.73/2.95 (P17(f12(f15(a14)))+~P10(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[4,77,1762,1766,76,74])). % 2.73/2.95 cnf(1796,plain, % 2.73/2.95 (~P10(f12(f15(a14)))+~P16(f12(f15(a14)))), % 2.73/2.95 inference(scs_inference,[],[297,1769,48])). % 2.73/2.95 cnf(1805,plain, % 2.73/2.96 (~P17(f12(f15(a14)))+~P16(f12(f15(a14)))), % 2.73/2.96 inference(scs_inference,[],[296,77,1766,76,8,75,944,948,1796])). % 2.73/2.96 cnf(1810,plain, % 2.73/2.96 (~P17(f12(f15(a14)))+~P13(f12(f15(a14)))), % 2.73/2.96 inference(scs_inference,[],[296,297,77,1766,76,8,75,944,948,1796,23,42,44])). % 2.73/2.96 cnf(1841,plain, % 2.73/2.96 (~P16(f12(f15(a14)))+P8(f12(f15(a14)))), % 2.73/2.96 inference(scs_inference,[],[1805,949])). % 2.73/2.96 cnf(1843,plain, % 2.73/2.96 (~P13(f12(f15(a14)))+~P15(f12(f15(a14)))), % 2.73/2.96 inference(scs_inference,[],[1810,938])). % 2.73/2.96 cnf(1848,plain, % 2.73/2.96 (~P15(f12(f15(a14)))+P14(f12(f15(a14)))), % 2.73/2.96 inference(scs_inference,[],[297,1843,20])). % 2.73/2.96 cnf(1853,plain, % 2.73/2.96 (P14(f12(f15(a14)))), % 2.73/2.96 inference(scs_inference,[],[1848,954])). % 2.73/2.96 cnf(1865,plain, % 2.73/2.96 ($false), % 2.73/2.96 inference(scs_inference,[],[297,77,1766,1853,46,22,48,74,942,950,1841,24]), % 2.73/2.96 ['proof']). % 2.73/2.96 % SZS output end Proof % 2.73/2.96 % Total time :2.431616s %------------------------------------------------------------------------------