%------------------------------------------------------------------------------ % File : CSE---1.7 % Problem : LCL674+1.010 : 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 : n026.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 116.81s 117.06s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.03 % Problem : LCL674+1.010 : 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.10/0.36 % Computer : n026.cluster.edu % 0.10/0.36 % Model : x86_64 x86_64 % 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.10/0.36 % Memory : 8046.5625MB % 0.10/0.36 % OS : Linux 6.8.0-71-generic % 0.02/0.36 % CPULimit : 300 % 0.02/0.36 % WCLimit : 300 % 0.02/0.36 % DateTime : Sat Sep 5 21:14:41 UTC 2026 % 0.02/0.36 % CPUTime : % 0.25/0.53 start to proof:theBenchmark % 116.81/117.04 %------------------------------------------- % 116.81/117.04 % File :CSE---1.7 % 116.81/117.04 % Problem :theBenchmark % 116.81/117.04 % Transform :cnf % 116.81/117.04 % Format :tptp:raw % 116.81/117.04 % Command :java -jar mcs_scs.jar %d %s % 116.81/117.04 % 116.81/117.04 % Result :Theorem 116.346099s % 116.81/117.04 % Output :CNFRefutation 116.346099s % 116.81/117.04 %------------------------------------------- % 116.81/117.05 %------------------------------------------------------------------------------ % 116.81/117.05 % File : LCL674+1.010 : TPTP v9.3.1. Released v4.0.0. % 116.81/117.05 % Domain : Logic Calculi (Modal Logic) % 116.81/117.05 % Problem : In S4, the branching formula made provable, size 10 % 116.81/117.05 % Version : Especial. % 116.81/117.05 % English : The branching formula plus a negation symbol in front and an % 116.81/117.05 % additional subformula to make the formula provable. % 116.81/117.05 % 116.81/117.05 % Refs : [BHS00] Balsiger et al. (2000), A Benchmark Method for the Pro % 116.81/117.05 % : [Kam08] Kaminski (2008), Email to G. Sutcliffe % 116.81/117.05 % Source : [Kam08] % 116.81/117.05 % Names : s4_branch_p [BHS00] % 116.81/117.05 % 116.81/117.05 % Status : Theorem % 116.81/117.05 % Rating : 0.00 v9.3.0, 0.05 v9.1.0, 0.13 v9.0.0, 0.00 v8.1.0, 0.14 v7.5.0, 0.10 v7.4.0, 0.06 v7.3.0, 0.00 v7.0.0, 0.07 v6.3.0, 0.08 v6.2.0, 0.09 v6.1.0, 0.16 v6.0.0, 0.25 v5.5.0, 0.21 v5.4.0, 0.22 v5.2.0, 0.07 v5.0.0, 0.15 v4.1.0, 0.22 v4.0.1, 0.26 v4.0.0 % 116.81/117.05 % Syntax : Number of formulae : 3 ( 1 unt; 0 def) % 116.81/117.05 % Number of atoms : 230 ( 0 equ) % 116.81/117.05 % Maximal formula atoms : 226 ( 76 avg) % 116.81/117.05 % Number of connectives : 432 ( 205 ~; 121 |; 105 &) % 116.81/117.05 % ( 0 <=>; 1 =>; 0 <=; 0 <~>) % 116.81/117.05 % Maximal formula depth : 42 ( 17 avg) % 116.81/117.05 % Maximal term depth : 1 ( 1 avg) % 116.81/117.05 % Number of predicates : 24 ( 24 usr; 0 prp; 1-2 aty) % 116.81/117.05 % Number of functors : 0 ( 0 usr; 0 con; --- aty) % 116.81/117.05 % Number of variables : 49 ( 48 !; 1 ?) % 116.81/117.05 % SPC : FOF_THM_RFO_NEQ % 116.81/117.05 % 116.81/117.05 % Comments : A naive relational encoding of the modal logic problem into % 116.81/117.05 % first-order logic. % 116.81/117.05 %------------------------------------------------------------------------------ % 116.81/117.05 fof(reflexivity,axiom, % 116.81/117.05 ! [X] : r1(X,X) ). % 116.81/117.05 % 116.81/117.05 fof(transitivity,axiom, % 116.81/117.05 ! [X,Y,Z] : % 116.81/117.05 ( ( r1(X,Y) % 116.81/117.05 & r1(Y,Z) ) % 116.81/117.05 => r1(X,Z) ) ). % 116.81/117.05 % 116.81/117.05 fof(main,conjecture, % 116.81/117.05 ~ ? [X] : % 116.81/117.05 ~ ( ~ ! [Y] : % 116.81/117.05 ( ~ r1(X,Y) % 116.81/117.05 | p5(Y) ) % 116.81/117.05 | ~ ( ! [Y] : % 116.81/117.05 ( ~ r1(X,Y) % 116.81/117.05 | ( ( ( ~ ! [X] : % 116.81/117.05 ( ~ r1(Y,X) % 116.81/117.05 | ~ ( ~ p11(X) % 116.81/117.05 & ~ p111(X) % 116.81/117.05 & p110(X) ) ) % 116.81/117.05 & ~ ! [X] : % 116.81/117.05 ( ~ r1(Y,X) % 116.81/117.05 | ~ ( p11(X) % 116.81/117.05 & ~ p111(X) % 116.81/117.05 & p110(X) ) ) ) % 116.81/117.05 | ~ ( ~ p110(Y) % 116.81/117.05 & p109(Y) ) ) % 116.81/117.05 & ( ( ~ ! [X] : % 116.81/117.05 ( ~ r1(Y,X) % 116.81/117.05 | ~ ( ~ p10(X) % 116.81/117.05 & ~ p110(X) % 116.81/117.05 & p109(X) ) ) % 116.81/117.05 & ~ ! [X] : % 116.81/117.05 ( ~ r1(Y,X) % 116.81/117.05 | ~ ( p10(X) % 116.81/117.05 & ~ p110(X) % 116.81/117.05 & p109(X) ) ) ) % 116.81/117.05 | ~ ( ~ p109(Y) % 116.81/117.05 & p108(Y) ) ) % 116.81/117.05 & ( ( ~ ! [X] : % 116.81/117.05 ( ~ r1(Y,X) % 116.81/117.05 | ~ ( ~ p9(X) % 116.81/117.05 & ~ p109(X) % 116.81/117.05 & p108(X) ) ) % 116.81/117.05 & ~ ! [X] : % 116.81/117.05 ( ~ r1(Y,X) % 116.81/117.05 | ~ ( p9(X) % 116.81/117.05 & ~ p109(X) % 116.81/117.05 & p108(X) ) ) ) % 116.81/117.05 | ~ ( ~ p108(Y) % 116.81/117.05 & p107(Y) ) ) % 116.81/117.05 & ( ( ~ ! [X] : % 116.81/117.05 ( ~ r1(Y,X) % 116.81/117.05 | ~ ( ~ p8(X) % 116.81/117.05 & ~ p108(X) % 116.81/117.05 & p107(X) ) ) % 116.81/117.05 & ~ ! [X] : % 116.81/117.05 ( ~ r1(Y,X) % 116.81/117.05 | ~ ( p8(X) % 116.81/117.05 & ~ p108(X) % 116.81/117.05 & p107(X) ) ) ) % 116.81/117.05 | ~ ( ~ p107(Y) % 116.81/117.05 & p106(Y) ) ) % 116.81/117.05 & ( ( ~ ! [X] : % 116.81/117.05 ( ~ r1(Y,X) % 116.81/117.05 | ~ ( ~ p7(X) % 116.81/117.05 & ~ p107(X) % 116.81/117.05 & p106(X) ) ) % 116.81/117.05 & ~ ! [X] : % 116.81/117.05 ( ~ r1(Y,X) % 116.81/117.05 | ~ ( p7(X) % 116.81/117.05 & ~ p107(X) % 116.81/117.05 & p106(X) ) ) ) % 116.81/117.05 | ~ ( ~ p106(Y) % 116.81/117.05 & p105(Y) ) ) % 116.81/117.05 & ( ( ~ ! [X] : % 116.81/117.05 ( ~ r1(Y,X) % 116.81/117.05 | ~ ( ~ p6(X) % 116.81/117.05 & ~ p106(X) % 116.81/117.05 & p105(X) ) ) % 116.81/117.05 & ~ ! [X] : % 116.81/117.05 ( ~ r1(Y,X) % 116.81/117.05 | ~ ( p6(X) % 116.81/117.05 & ~ p106(X) % 116.81/117.05 & p105(X) ) ) ) % 116.81/117.05 | ~ ( ~ p105(Y) % 116.81/117.05 & p104(Y) ) ) % 116.81/117.05 & ( ( ~ ! [X] : % 116.81/117.05 ( ~ r1(Y,X) % 116.81/117.05 | ~ ( ~ p5(X) % 116.81/117.05 & ~ p105(X) % 116.81/117.05 & p104(X) ) ) % 116.81/117.05 & ~ ! [X] : % 116.81/117.05 ( ~ r1(Y,X) % 116.81/117.06 | ~ ( p5(X) % 116.81/117.06 & ~ p105(X) % 116.81/117.06 & p104(X) ) ) ) % 116.81/117.06 | ~ ( ~ p104(Y) % 116.81/117.06 & p103(Y) ) ) % 116.81/117.06 & ( ( ~ ! [X] : % 116.81/117.06 ( ~ r1(Y,X) % 116.81/117.06 | ~ ( ~ p4(X) % 116.81/117.06 & ~ p104(X) % 116.81/117.06 & p103(X) ) ) % 116.81/117.06 & ~ ! [X] : % 116.81/117.06 ( ~ r1(Y,X) % 116.81/117.06 | ~ ( p4(X) % 116.81/117.06 & ~ p104(X) % 116.81/117.06 & p103(X) ) ) ) % 116.81/117.06 | ~ ( ~ p103(Y) % 116.81/117.06 & p102(Y) ) ) % 116.81/117.06 & ( ( ~ ! [X] : % 116.81/117.06 ( ~ r1(Y,X) % 116.81/117.06 | ~ ( ~ p3(X) % 116.81/117.06 & ~ p103(X) % 116.81/117.06 & p102(X) ) ) % 116.81/117.06 & ~ ! [X] : % 116.81/117.06 ( ~ r1(Y,X) % 116.81/117.06 | ~ ( p3(X) % 116.81/117.06 & ~ p103(X) % 116.81/117.06 & p102(X) ) ) ) % 116.81/117.06 | ~ ( ~ p102(Y) % 116.81/117.06 & p101(Y) ) ) % 116.81/117.06 & ( ( ~ ! [X] : % 116.81/117.06 ( ~ r1(Y,X) % 116.81/117.06 | ~ ( ~ p2(X) % 116.81/117.06 & ~ p102(X) % 116.81/117.06 & p101(X) ) ) % 116.81/117.06 & ~ ! [X] : % 116.81/117.06 ( ~ r1(Y,X) % 116.81/117.06 | ~ ( p2(X) % 116.81/117.06 & ~ p102(X) % 116.81/117.06 & p101(X) ) ) ) % 116.81/117.06 | ~ ( ~ p101(Y) % 116.81/117.06 & p100(Y) ) ) % 116.81/117.06 & ( ( ( ! [X] : % 116.81/117.06 ( ~ r1(Y,X) % 116.81/117.06 | ~ p11(X) % 116.81/117.06 | ~ p110(X) ) % 116.81/117.06 | p11(Y) ) % 116.81/117.06 & ( ! [X] : % 116.81/117.06 ( ~ r1(Y,X) % 116.81/117.06 | p11(X) % 116.81/117.06 | ~ p110(X) ) % 116.81/117.06 | ~ p11(Y) ) ) % 116.81/117.06 | ~ p110(Y) ) % 116.81/117.06 & ( ( ( ! [X] : % 116.81/117.06 ( ~ r1(Y,X) % 116.81/117.06 | ~ p10(X) % 116.81/117.06 | ~ p109(X) ) % 116.81/117.06 | p10(Y) ) % 116.81/117.06 & ( ! [X] : % 116.81/117.06 ( ~ r1(Y,X) % 116.81/117.06 | p10(X) % 116.81/117.06 | ~ p109(X) ) % 116.81/117.06 | ~ p10(Y) ) ) % 116.81/117.06 | ~ p109(Y) ) % 116.81/117.06 & ( ( ( ! [X] : % 116.81/117.06 ( ~ r1(Y,X) % 116.81/117.06 | ~ p9(X) % 116.81/117.06 | ~ p108(X) ) % 116.81/117.06 | p9(Y) ) % 116.81/117.06 & ( ! [X] : % 116.81/117.06 ( ~ r1(Y,X) % 116.81/117.06 | p9(X) % 116.81/117.06 | ~ p108(X) ) % 116.81/117.06 | ~ p9(Y) ) ) % 116.81/117.06 | ~ p108(Y) ) % 116.81/117.06 & ( ( ( ! [X] : % 116.81/117.06 ( ~ r1(Y,X) % 116.81/117.06 | ~ p8(X) % 116.81/117.06 | ~ p107(X) ) % 116.81/117.06 | p8(Y) ) % 116.81/117.06 & ( ! [X] : % 116.81/117.06 ( ~ r1(Y,X) % 116.81/117.06 | p8(X) % 116.81/117.06 | ~ p107(X) ) % 116.81/117.06 | ~ p8(Y) ) ) % 116.81/117.06 | ~ p107(Y) ) % 116.81/117.06 & ( ( ( ! [X] : % 116.81/117.06 ( ~ r1(Y,X) % 116.81/117.06 | ~ p7(X) % 116.81/117.06 | ~ p106(X) ) % 116.81/117.06 | p7(Y) ) % 116.81/117.06 & ( ! [X] : % 116.81/117.06 ( ~ r1(Y,X) % 116.81/117.06 | p7(X) % 116.81/117.06 | ~ p106(X) ) % 116.81/117.06 | ~ p7(Y) ) ) % 116.81/117.06 | ~ p106(Y) ) % 116.81/117.06 & ( ( ( ! [X] : % 116.81/117.06 ( ~ r1(Y,X) % 116.81/117.06 | ~ p6(X) % 116.81/117.06 | ~ p105(X) ) % 116.81/117.06 | p6(Y) ) % 116.81/117.06 & ( ! [X] : % 116.81/117.06 ( ~ r1(Y,X) % 116.81/117.06 | p6(X) % 116.81/117.06 | ~ p105(X) ) % 116.81/117.06 | ~ p6(Y) ) ) % 116.81/117.06 | ~ p105(Y) ) % 116.81/117.06 & ( ( ( ! [X] : % 116.81/117.06 ( ~ r1(Y,X) % 116.81/117.06 | ~ p5(X) % 116.81/117.06 | ~ p104(X) ) % 116.81/117.06 | p5(Y) ) % 116.81/117.06 & ( ! [X] : % 116.81/117.06 ( ~ r1(Y,X) % 116.81/117.06 | p5(X) % 116.81/117.06 | ~ p104(X) ) % 116.81/117.06 | ~ p5(Y) ) ) % 116.81/117.06 | ~ p104(Y) ) % 116.81/117.06 & ( ( ( ! [X] : % 116.81/117.06 ( ~ r1(Y,X) % 116.81/117.06 | ~ p4(X) % 116.81/117.06 | ~ p103(X) ) % 116.81/117.06 | p4(Y) ) % 116.81/117.06 & ( ! [X] : % 116.81/117.06 ( ~ r1(Y,X) % 116.81/117.06 | p4(X) % 116.81/117.06 | ~ p103(X) ) % 116.81/117.06 | ~ p4(Y) ) ) % 116.81/117.06 | ~ p103(Y) ) % 116.81/117.06 & ( ( ( ! [X] : % 116.81/117.06 ( ~ r1(Y,X) % 116.81/117.06 | ~ p3(X) % 116.81/117.06 | ~ p102(X) ) % 116.81/117.06 | p3(Y) ) % 116.81/117.06 & ( ! [X] : % 116.81/117.06 ( ~ r1(Y,X) % 116.81/117.06 | p3(X) % 116.81/117.06 | ~ p102(X) ) % 116.81/117.06 | ~ p3(Y) ) ) % 116.81/117.06 | ~ p102(Y) ) % 116.81/117.06 & ( ( ( ! [X] : % 116.81/117.06 ( ~ r1(Y,X) % 116.81/117.06 | ~ p2(X) % 116.81/117.06 | ~ p101(X) ) % 116.81/117.06 | p2(Y) ) % 116.81/117.06 & ( ! [X] : % 116.81/117.06 ( ~ r1(Y,X) % 116.81/117.06 | p2(X) % 116.81/117.06 | ~ p101(X) ) % 116.81/117.06 | ~ p2(Y) ) ) % 116.81/117.06 | ~ p101(Y) ) % 116.81/117.06 & ( ( ( ! [X] : % 116.81/117.06 ( ~ r1(Y,X) % 116.81/117.06 | ~ p1(X) % 116.81/117.06 | ~ p100(X) ) % 116.81/117.06 | p1(Y) ) % 116.81/117.06 & ( ! [X] : % 116.81/117.06 ( ~ r1(Y,X) % 116.81/117.06 | p1(X) % 116.81/117.06 | ~ p100(X) ) % 116.81/117.06 | ~ p1(Y) ) ) % 116.81/117.06 | ~ p100(Y) ) % 116.81/117.06 & ( p110(Y) % 116.81/117.06 | ~ p111(Y) ) % 116.81/117.06 & ( p109(Y) % 116.81/117.06 | ~ p110(Y) ) % 116.81/117.06 & ( p108(Y) % 116.81/117.06 | ~ p109(Y) ) % 116.81/117.06 & ( p107(Y) % 116.81/117.06 | ~ p108(Y) ) % 116.81/117.06 & ( p106(Y) % 116.81/117.06 | ~ p107(Y) ) % 116.81/117.06 & ( p105(Y) % 116.81/117.06 | ~ p106(Y) ) % 116.81/117.06 & ( p104(Y) % 116.81/117.06 | ~ p105(Y) ) % 116.81/117.06 & ( p103(Y) % 116.81/117.06 | ~ p104(Y) ) % 116.81/117.06 & ( p102(Y) % 116.81/117.06 | ~ p103(Y) ) % 116.81/117.06 & ( p101(Y) % 116.81/117.06 | ~ p102(Y) ) % 116.81/117.06 & ( p100(Y) % 116.81/117.06 | ~ p101(Y) ) ) ) % 116.81/117.06 & ~ p101(X) % 116.81/117.06 & p100(X) ) ) ). % 116.81/117.06 % 116.81/117.06 %------------------------------------------------------------------------------ % 116.81/117.06 %------------------------------------------- % 116.81/117.06 % Proof found % 116.81/117.06 % SZS status Theorem for theBenchmark % 116.81/117.06 % SZS output start Proof % 116.81/117.06 %ClaNum:119(EqnAxiom:0) % 116.81/117.06 %VarNum:539(SingletonVarNum:141) % 116.81/117.06 %MaxLitNum:6 % 116.81/117.06 %MaxfuncDepth:1 % 116.81/117.06 %SharedTerms:3 % 116.81/117.06 %goalClause: 1 3 15 16 % 116.81/117.06 %singleGoalClaCount:2 % 116.81/117.06 [1]P1(a1) % 116.81/117.06 [3]~P6(a1) % 116.81/117.06 [2]P5(x21,x21) % 116.81/117.06 [15]P18(x151)+~P5(a1,x151) % 116.81/117.06 [16]P2(x161)+~P5(a1,x161) % 116.81/117.06 [4]~P17(x41)+~P2(x41)+P7(x41) % 116.81/117.06 [5]~P7(x51)+~P2(x51)+P8(x51) % 116.81/117.06 [6]~P8(x61)+~P2(x61)+P9(x61) % 116.81/117.06 [7]~P9(x71)+~P2(x71)+P10(x71) % 116.81/117.06 [8]~P10(x81)+~P2(x81)+P11(x81) % 116.81/117.06 [9]~P11(x91)+~P2(x91)+P12(x91) % 116.81/117.06 [10]~P12(x101)+~P2(x101)+P13(x101) % 116.81/117.06 [11]~P13(x111)+~P2(x111)+P14(x111) % 116.81/117.06 [12]~P14(x121)+~P2(x121)+P15(x121) % 116.81/117.06 [13]~P15(x131)+~P2(x131)+P6(x131) % 116.81/117.06 [14]~P6(x141)+~P2(x141)+P1(x141) % 116.81/117.06 [119]~P5(x1191,x1193)+P5(x1191,x1192)+~P5(x1193,x1192) % 116.81/117.06 [17]~P8(x171)+~P2(x171)+P7(x171)+P16(f12(x171)) % 116.81/117.06 [18]~P8(x181)+~P2(x181)+P7(x181)+P7(f13(x181)) % 116.81/117.06 [19]~P8(x191)+~P2(x191)+P7(x191)+P7(f12(x191)) % 116.81/117.06 [20]~P9(x201)+~P2(x201)+P8(x201)+P8(f16(x201)) % 116.81/117.06 [21]~P9(x211)+~P2(x211)+P8(x211)+P8(f17(x211)) % 116.81/117.06 [22]~P9(x221)+~P2(x221)+P8(x221)+P3(f17(x221)) % 116.81/117.06 [23]~P10(x231)+~P2(x231)+P9(x231)+P9(f18(x231)) % 116.81/117.06 [24]~P10(x241)+~P2(x241)+P9(x241)+P9(f19(x241)) % 116.81/117.06 [25]~P10(x251)+~P2(x251)+P9(x251)+P22(f19(x251)) % 116.81/117.06 [26]~P11(x261)+~P2(x261)+P10(x261)+P10(f20(x261)) % 116.81/117.06 [27]~P11(x271)+~P2(x271)+P10(x271)+P10(f21(x271)) % 116.81/117.06 [28]~P11(x281)+~P2(x281)+P10(x281)+P23(f21(x281)) % 116.81/117.06 [29]~P12(x291)+~P2(x291)+P11(x291)+P11(f2(x291)) % 116.81/117.06 [30]~P12(x301)+~P2(x301)+P11(x301)+P11(f3(x301)) % 116.81/117.06 [31]~P12(x311)+~P2(x311)+P11(x311)+P24(f3(x311)) % 116.81/117.06 [32]~P13(x321)+~P2(x321)+P12(x321)+P12(f4(x321)) % 116.81/117.06 [33]~P13(x331)+~P2(x331)+P12(x331)+P12(f5(x331)) % 116.81/117.06 [34]~P13(x341)+~P2(x341)+P12(x341)+P25(f5(x341)) % 116.81/117.06 [35]~P14(x351)+~P2(x351)+P13(x351)+P18(f6(x351)) % 116.81/117.06 [36]~P14(x361)+~P2(x361)+P13(x361)+P13(f7(x361)) % 116.81/117.07 [37]~P14(x371)+~P2(x371)+P13(x371)+P13(f6(x371)) % 116.81/117.07 [38]~P15(x381)+~P2(x381)+P14(x381)+P14(f8(x381)) % 116.81/117.07 [39]~P15(x391)+~P2(x391)+P14(x391)+P14(f9(x391)) % 116.81/117.07 [40]~P15(x401)+~P2(x401)+P14(x401)+P19(f9(x401)) % 116.81/117.07 [41]~P6(x411)+~P2(x411)+P15(x411)+P15(f10(x411)) % 116.81/117.07 [42]~P6(x421)+~P2(x421)+P15(x421)+P15(f11(x421)) % 116.81/117.07 [43]~P6(x431)+~P2(x431)+P15(x431)+P20(f11(x431)) % 116.81/117.07 [44]~P1(x441)+~P2(x441)+P6(x441)+P6(f14(x441)) % 116.81/117.07 [45]~P1(x451)+~P2(x451)+P6(x451)+P6(f15(x451)) % 116.81/117.07 [46]~P1(x461)+~P2(x461)+P6(x461)+P21(f15(x461)) % 116.81/117.07 [47]~P8(x471)+~P2(x471)+P7(x471)+~P16(f13(x471)) % 116.81/117.07 [48]~P8(x481)+~P2(x481)+P7(x481)+~P17(f13(x481)) % 116.81/117.07 [49]~P8(x491)+~P2(x491)+P7(x491)+~P17(f12(x491)) % 116.81/117.07 [50]~P9(x501)+~P2(x501)+P8(x501)+~P7(f16(x501)) % 116.81/117.07 [51]~P9(x511)+~P2(x511)+P8(x511)+~P7(f17(x511)) % 116.81/117.07 [52]~P9(x521)+~P2(x521)+P8(x521)+~P3(f16(x521)) % 116.81/117.07 [53]~P10(x531)+~P2(x531)+P9(x531)+~P8(f18(x531)) % 116.81/117.07 [54]~P10(x541)+~P2(x541)+P9(x541)+~P8(f19(x541)) % 116.81/117.07 [55]~P10(x551)+~P2(x551)+P9(x551)+~P22(f18(x551)) % 116.81/117.07 [56]~P11(x561)+~P2(x561)+P10(x561)+~P9(f20(x561)) % 116.81/117.07 [57]~P11(x571)+~P2(x571)+P10(x571)+~P9(f21(x571)) % 116.81/117.07 [58]~P11(x581)+~P2(x581)+P10(x581)+~P23(f20(x581)) % 116.81/117.07 [59]~P12(x591)+~P2(x591)+P11(x591)+~P10(f2(x591)) % 116.81/117.07 [60]~P12(x601)+~P2(x601)+P11(x601)+~P10(f3(x601)) % 116.81/117.07 [61]~P12(x611)+~P2(x611)+P11(x611)+~P24(f2(x611)) % 116.81/117.07 [62]~P13(x621)+~P2(x621)+P12(x621)+~P11(f4(x621)) % 116.81/117.07 [63]~P13(x631)+~P2(x631)+P12(x631)+~P11(f5(x631)) % 116.81/117.07 [64]~P13(x641)+~P2(x641)+P12(x641)+~P25(f4(x641)) % 116.81/117.07 [65]~P14(x651)+~P2(x651)+P13(x651)+~P18(f7(x651)) % 116.81/117.07 [66]~P14(x661)+~P2(x661)+P13(x661)+~P12(f7(x661)) % 116.81/117.07 [67]~P14(x671)+~P2(x671)+P13(x671)+~P12(f6(x671)) % 116.81/117.07 [68]~P15(x681)+~P2(x681)+P14(x681)+~P13(f8(x681)) % 116.81/117.07 [69]~P15(x691)+~P2(x691)+P14(x691)+~P13(f9(x691)) % 116.81/117.07 [70]~P15(x701)+~P2(x701)+P14(x701)+~P19(f8(x701)) % 116.81/117.07 [71]~P6(x711)+~P2(x711)+P15(x711)+~P14(f10(x711)) % 116.81/117.07 [72]~P6(x721)+~P2(x721)+P15(x721)+~P14(f11(x721)) % 116.81/117.07 [73]~P6(x731)+~P2(x731)+P15(x731)+~P20(f10(x731)) % 116.81/117.07 [74]~P1(x741)+~P2(x741)+P6(x741)+~P15(f14(x741)) % 116.81/117.07 [75]~P1(x751)+~P2(x751)+P6(x751)+~P15(f15(x751)) % 116.81/117.07 [76]~P1(x761)+~P2(x761)+P6(x761)+~P21(f14(x761)) % 116.81/117.07 [77]~P8(x771)+~P2(x771)+P7(x771)+P5(x771,f13(x771)) % 116.81/117.07 [78]~P8(x781)+~P2(x781)+P7(x781)+P5(x781,f12(x781)) % 116.81/117.07 [79]~P9(x791)+~P2(x791)+P8(x791)+P5(x791,f16(x791)) % 116.81/117.07 [80]~P9(x801)+~P2(x801)+P8(x801)+P5(x801,f17(x801)) % 116.81/117.07 [81]~P10(x811)+~P2(x811)+P9(x811)+P5(x811,f18(x811)) % 116.81/117.07 [82]~P10(x821)+~P2(x821)+P9(x821)+P5(x821,f19(x821)) % 116.81/117.07 [83]~P11(x831)+~P2(x831)+P10(x831)+P5(x831,f20(x831)) % 116.81/117.07 [84]~P11(x841)+~P2(x841)+P10(x841)+P5(x841,f21(x841)) % 116.81/117.07 [85]~P12(x851)+~P2(x851)+P11(x851)+P5(x851,f2(x851)) % 116.81/117.07 [86]~P12(x861)+~P2(x861)+P11(x861)+P5(x861,f3(x861)) % 116.81/117.07 [87]~P13(x871)+~P2(x871)+P12(x871)+P5(x871,f4(x871)) % 116.81/117.07 [88]~P13(x881)+~P2(x881)+P12(x881)+P5(x881,f5(x881)) % 116.81/117.07 [89]~P14(x891)+~P2(x891)+P13(x891)+P5(x891,f7(x891)) % 116.81/117.07 [90]~P14(x901)+~P2(x901)+P13(x901)+P5(x901,f6(x901)) % 116.81/117.07 [91]~P15(x911)+~P2(x911)+P14(x911)+P5(x911,f8(x911)) % 116.81/117.07 [92]~P15(x921)+~P2(x921)+P14(x921)+P5(x921,f9(x921)) % 116.81/117.07 [93]~P6(x931)+~P2(x931)+P15(x931)+P5(x931,f10(x931)) % 116.81/117.07 [94]~P6(x941)+~P2(x941)+P15(x941)+P5(x941,f11(x941)) % 116.81/117.07 [95]~P1(x951)+~P2(x951)+P6(x951)+P5(x951,f14(x951)) % 116.81/117.07 [96]~P1(x961)+~P2(x961)+P6(x961)+P5(x961,f15(x961)) % 116.81/117.07 [97]~P13(x971)+~P13(x972)+~P2(x972)+~P5(x972,x971)+P18(x971)+~P18(x972) % 116.81/117.07 [98]~P13(x982)+~P13(x981)+~P2(x981)+~P5(x981,x982)+P18(x981)+~P18(x982) % 116.81/117.07 [99]~P7(x991)+~P7(x992)+~P2(x992)+~P5(x992,x991)+P16(x991)+~P16(x992) % 116.81/117.07 [100]~P7(x1002)+~P7(x1001)+~P2(x1001)+~P5(x1001,x1002)+P16(x1001)+~P16(x1002) % 116.81/117.07 [101]~P8(x1011)+~P3(x1012)+~P2(x1012)+~P5(x1012,x1011)+P3(x1011)+~P8(x1012) % 116.81/117.07 [102]~P8(x1021)+~P3(x1022)+~P2(x1021)+~P5(x1021,x1022)+P3(x1021)+~P8(x1022) % 116.81/117.07 [103]~P9(x1031)+~P22(x1032)+~P2(x1032)+~P5(x1032,x1031)+P22(x1031)+~P9(x1032) % 116.81/117.07 [104]~P9(x1041)+~P22(x1042)+~P2(x1041)+~P5(x1041,x1042)+P22(x1041)+~P9(x1042) % 116.81/117.07 [105]~P10(x1051)+~P23(x1052)+~P2(x1052)+~P5(x1052,x1051)+P23(x1051)+~P10(x1052) % 116.81/117.07 [106]~P10(x1061)+~P23(x1062)+~P2(x1061)+~P5(x1061,x1062)+P23(x1061)+~P10(x1062) % 116.81/117.07 [107]~P11(x1071)+~P24(x1072)+~P2(x1072)+~P5(x1072,x1071)+P24(x1071)+~P11(x1072) % 116.81/117.07 [108]~P11(x1081)+~P24(x1082)+~P2(x1081)+~P5(x1081,x1082)+P24(x1081)+~P11(x1082) % 116.81/117.07 [109]~P12(x1091)+~P25(x1092)+~P2(x1092)+~P5(x1092,x1091)+P25(x1091)+~P12(x1092) % 116.81/117.07 [110]~P12(x1101)+~P25(x1102)+~P2(x1101)+~P5(x1101,x1102)+P25(x1101)+~P12(x1102) % 116.81/117.07 [111]~P14(x1111)+~P19(x1112)+~P2(x1112)+~P5(x1112,x1111)+P19(x1111)+~P14(x1112) % 116.81/117.07 [112]~P14(x1121)+~P19(x1122)+~P2(x1121)+~P5(x1121,x1122)+P19(x1121)+~P14(x1122) % 116.81/117.07 [113]~P15(x1131)+~P20(x1132)+~P2(x1132)+~P5(x1132,x1131)+P20(x1131)+~P15(x1132) % 116.81/117.07 [114]~P15(x1141)+~P20(x1142)+~P2(x1141)+~P5(x1141,x1142)+P20(x1141)+~P15(x1142) % 116.81/117.07 [115]~P6(x1151)+~P21(x1152)+~P2(x1152)+~P5(x1152,x1151)+P21(x1151)+~P6(x1152) % 116.81/117.07 [116]~P6(x1161)+~P21(x1162)+~P2(x1161)+~P5(x1161,x1162)+P21(x1161)+~P6(x1162) % 116.81/117.07 [117]~P1(x1171)+~P4(x1172)+~P2(x1172)+~P5(x1172,x1171)+P4(x1171)+~P1(x1172) % 116.81/117.07 [118]~P1(x1181)+~P4(x1182)+~P2(x1181)+~P5(x1181,x1182)+P4(x1181)+~P1(x1182) % 116.81/117.07 %EqnAxiom % 116.81/117.07 % 116.81/117.07 %------------------------------------------- % 116.81/117.08 cnf(121,plain, % 116.81/117.08 (P5(x1211,x1211)), % 116.81/117.08 inference(rename_variables,[],[2])). % 116.81/117.08 cnf(123,plain, % 116.81/117.08 (P2(a1)), % 116.81/117.08 inference(scs_inference,[],[2,121,15,16])). % 116.81/117.08 cnf(1863,plain, % 116.81/117.08 (~P2(f14(a1))+~P6(f14(a1))+P15(f10(f14(a1)))), % 116.81/117.08 inference(scs_inference,[],[123,3,1,41,74])). % 116.81/117.08 cnf(1927,plain, % 116.81/117.08 (P15(f10(f14(a1)))+~P2(f14(a1))), % 116.81/117.08 inference(scs_inference,[],[123,3,1,1863,44])). % 116.81/117.08 cnf(1991,plain, % 116.81/117.08 (~P2(f10(f14(a1)))+P6(f10(f14(a1)))+~P2(f14(a1))), % 116.81/117.08 inference(scs_inference,[],[1927,13])). % 116.81/117.08 cnf(2053,plain, % 116.81/117.08 (P6(f10(f14(a1)))+~P2(f14(a1))+~P5(a1,f10(f14(a1)))), % 116.81/117.08 inference(scs_inference,[],[1991,16])). % 116.81/117.08 cnf(2181,plain, % 116.81/117.08 (~P2(f15(a1))+~P6(f15(a1))+P15(f11(f15(a1)))), % 116.81/117.08 inference(scs_inference,[],[123,3,1,42,75])). % 116.81/117.08 cnf(2243,plain, % 116.81/117.08 (P15(f11(f15(a1)))+~P2(f15(a1))), % 116.81/117.08 inference(scs_inference,[],[123,3,1,2181,45])). % 116.81/117.08 cnf(2307,plain, % 116.81/117.08 (~P2(f11(f15(a1)))+P6(f11(f15(a1)))+~P2(f15(a1))), % 116.81/117.08 inference(scs_inference,[],[2243,13])). % 116.81/117.08 cnf(4131,plain, % 116.81/117.08 (~P2(f15(a1))+~P6(f15(a1))+~P14(f10(f15(a1)))), % 116.81/117.08 inference(scs_inference,[],[123,3,1,71,75])). % 116.81/117.08 cnf(4194,plain, % 116.81/117.08 (~P14(f10(f15(a1)))+~P2(f15(a1))), % 116.81/117.08 inference(scs_inference,[],[123,3,1,4131,45])). % 116.81/117.08 cnf(4450,plain, % 116.81/117.08 (~P2(f14(a1))+~P6(f14(a1))+~P14(f11(f14(a1)))), % 116.81/117.08 inference(scs_inference,[],[123,3,1,72,74])). % 116.81/117.08 cnf(4515,plain, % 116.81/117.08 (~P14(f11(f14(a1)))+~P2(f14(a1))), % 116.81/117.08 inference(scs_inference,[],[123,3,1,4450,44])). % 116.81/117.08 cnf(4768,plain, % 116.81/117.08 (~P2(f15(a1))+~P6(f15(a1))+~P20(f10(f15(a1)))), % 116.81/117.08 inference(scs_inference,[],[123,3,1,73,75])). % 116.81/117.08 cnf(4831,plain, % 116.81/117.08 (~P20(f10(f15(a1)))+~P2(f15(a1))), % 116.81/117.08 inference(scs_inference,[],[123,3,1,4768,45])). % 116.81/117.08 cnf(4895,plain, % 116.81/117.08 (~P20(f10(f15(a1)))+~P5(a1,f15(a1))), % 116.81/117.08 inference(scs_inference,[],[4831,16])). % 116.81/117.08 cnf(4958,plain, % 116.81/117.08 (~P20(f10(f15(a1)))), % 116.81/117.08 inference(scs_inference,[],[123,3,1,4895,96])). % 116.81/117.08 cnf(6023,plain, % 116.81/117.08 (~P2(f14(a1))+~P6(f14(a1))+P5(f14(a1),f10(f14(a1)))), % 116.81/117.08 inference(scs_inference,[],[123,3,1,93,74])). % 116.81/117.08 cnf(6087,plain, % 116.81/117.08 (P5(f14(a1),f10(f14(a1)))+~P6(f14(a1))+~P5(a1,f14(a1))), % 116.81/117.08 inference(scs_inference,[],[6023,16])). % 116.81/117.08 cnf(6151,plain, % 116.81/117.08 (P5(f14(a1),f10(f14(a1)))+~P6(f14(a1))), % 116.81/117.08 inference(scs_inference,[],[123,3,1,6087,95])). % 116.81/117.08 cnf(6215,plain, % 116.81/117.08 (P5(f14(a1),f10(f14(a1)))), % 116.81/117.08 inference(scs_inference,[],[123,3,1,6151,44])). % 116.81/117.08 cnf(6283,plain, % 116.81/117.08 (~P2(f15(a1))+~P6(f15(a1))+P5(f15(a1),f11(f15(a1)))), % 116.81/117.08 inference(scs_inference,[],[123,3,1,94,75])). % 116.81/117.08 cnf(6348,plain, % 116.81/117.08 (P5(f15(a1),f11(f15(a1)))+~P6(f15(a1))+~P5(a1,f15(a1))), % 116.81/117.08 inference(scs_inference,[],[6283,16])). % 116.81/117.08 cnf(6411,plain, % 116.81/117.08 (P5(f15(a1),f11(f15(a1)))+~P6(f15(a1))), % 116.81/117.08 inference(scs_inference,[],[123,3,1,6348,96])). % 116.81/117.08 cnf(6476,plain, % 116.81/117.08 (P5(f15(a1),f11(f15(a1)))), % 116.81/117.08 inference(scs_inference,[],[123,3,1,6411,45])). % 116.81/117.08 cnf(6725,plain, % 116.81/117.08 (P21(f15(a1))), % 116.81/117.08 inference(scs_inference,[],[2,3,1,16,46])). % 116.81/117.08 cnf(6790,plain, % 116.81/117.08 (P2(f14(a1))), % 116.81/117.08 inference(scs_inference,[],[123,3,1,16,95])). % 116.81/117.08 cnf(6791,plain, % 116.81/117.08 (P15(f10(f14(a1)))), % 116.81/117.08 inference(scs_inference,[],[6790,1927])). % 116.81/117.08 cnf(6793,plain, % 116.81/117.08 (P6(f10(f14(a1)))+~P5(a1,f10(f14(a1)))), % 116.81/117.08 inference(scs_inference,[],[6790,2053])). % 116.81/117.08 cnf(6794,plain, % 116.81/117.08 (~P14(f11(f14(a1)))), % 116.81/117.08 inference(scs_inference,[],[6790,4515])). % 116.81/117.08 cnf(7939,plain, % 116.81/117.08 (~P5(a1,f14(a1))+P6(f10(f14(a1)))), % 116.81/117.08 inference(scs_inference,[],[6215,6793,119])). % 116.81/117.08 cnf(8007,plain, % 116.81/117.08 (P6(f10(f14(a1)))), % 116.81/117.08 inference(scs_inference,[],[123,3,1,7939,95])). % 116.81/117.08 cnf(8955,plain, % 116.81/117.08 (~P21(f14(a1))), % 116.81/117.08 inference(scs_inference,[],[2,3,1,16,76])). % 116.81/117.08 cnf(9018,plain, % 116.81/117.08 (P2(f15(a1))), % 116.81/117.08 inference(scs_inference,[],[123,3,1,16,96])). % 116.81/117.08 cnf(9019,plain, % 116.81/117.08 (P15(f11(f15(a1)))), % 116.81/117.08 inference(scs_inference,[],[9018,2243])). % 116.81/117.08 cnf(9020,plain, % 116.81/117.08 (~P2(f11(f15(a1)))+P6(f11(f15(a1)))), % 116.81/117.08 inference(scs_inference,[],[9018,2307])). % 116.81/117.08 cnf(9022,plain, % 116.81/117.08 (~P14(f10(f15(a1)))), % 116.81/117.08 inference(scs_inference,[],[9018,4194])). % 116.81/117.08 cnf(11276,plain, % 116.81/117.08 (P6(f14(a1))), % 116.81/117.08 inference(scs_inference,[],[2,3,1,16,44])). % 116.81/117.08 cnf(11446,plain, % 116.81/117.08 (P6(f15(a1))), % 116.81/117.08 inference(scs_inference,[],[2,3,1,16,45])). % 116.81/117.08 cnf(11627,plain, % 116.81/117.08 (P5(a1,f15(a1))), % 116.81/117.08 inference(scs_inference,[],[2,3,1,16,96])). % 116.81/117.08 cnf(11628,plain, % 116.81/117.08 (P5(a1,f11(f15(a1)))), % 116.81/117.08 inference(scs_inference,[],[11627,6476,119])). % 116.81/117.08 cnf(11630,plain, % 116.81/117.08 (P2(f11(f15(a1)))), % 116.81/117.08 inference(scs_inference,[],[11627,6476,119,16])). % 116.81/117.08 cnf(11650,plain, % 116.81/117.08 (P6(f11(f15(a1)))), % 116.81/117.08 inference(scs_inference,[],[11630,9020])). % 116.81/117.08 cnf(18709,plain, % 116.81/117.08 (~P15(f10(f15(a1)))+~P5(a1,f10(f15(a1)))+P14(f8(f10(f15(a1))))), % 116.81/117.08 inference(scs_inference,[],[9022,38,16])). % 116.81/117.08 cnf(18827,plain, % 116.81/117.08 (~P15(f11(f14(a1)))+~P5(a1,f11(f14(a1)))+P14(f9(f11(f14(a1))))), % 116.81/117.08 inference(scs_inference,[],[6794,39,16])). % 116.81/117.08 cnf(20298,plain, % 116.81/117.08 (~P15(f11(f14(a1)))+~P5(a1,f11(f14(a1)))+~P19(f8(f11(f14(a1))))), % 116.81/117.08 inference(scs_inference,[],[6794,70,16])). % 116.81/117.08 cnf(21326,plain, % 116.81/117.08 (~P15(f11(f14(a1)))+P5(f11(f14(a1)),f9(f11(f14(a1))))+~P5(a1,f11(f14(a1)))), % 116.81/117.08 inference(scs_inference,[],[6794,92,16])). % 116.81/117.08 cnf(21491,plain, % 116.81/117.08 (P14(f11(f15(a1)))+P14(f8(f11(f15(a1))))), % 116.81/117.08 inference(scs_inference,[],[11628,9019,16,38])). % 116.81/117.08 cnf(26799,plain, % 116.81/117.08 (~P2(f10(f15(a1)))+P15(f15(a1))+P14(f8(f10(f15(a1))))), % 116.81/117.08 inference(scs_inference,[],[9022,9018,11446,38,41])). % 116.81/117.08 cnf(27606,plain, % 116.81/117.08 (P15(f15(a1))+P15(f10(f15(a1)))), % 116.81/117.08 inference(scs_inference,[],[9018,123,3,1,41,45])). % 116.81/117.08 cnf(27646,plain, % 116.81/117.08 (P15(f10(f15(a1)))), % 116.81/117.08 inference(scs_inference,[],[123,3,1,27606,75])). % 116.81/117.08 cnf(27647,plain, % 116.81/117.08 (~P5(a1,f10(f15(a1)))+P14(f8(f10(f15(a1))))), % 116.81/117.08 inference(scs_inference,[],[27646,18709])). % 116.81/117.08 cnf(27901,plain, % 116.81/117.08 (P15(f14(a1))+P15(f11(f14(a1)))), % 116.81/117.08 inference(scs_inference,[],[6790,123,3,1,42,44])). % 116.81/117.08 cnf(28022,plain, % 116.81/117.08 (P15(f11(f14(a1)))), % 116.81/117.08 inference(scs_inference,[],[123,3,1,27901,74])). % 116.81/117.08 cnf(28023,plain, % 116.81/117.08 (~P5(a1,f11(f14(a1)))+P14(f9(f11(f14(a1))))), % 116.81/117.08 inference(scs_inference,[],[28022,18827])). % 116.81/117.08 cnf(28025,plain, % 116.81/117.08 (~P5(a1,f11(f14(a1)))+~P19(f8(f11(f14(a1))))), % 116.81/117.08 inference(scs_inference,[],[28022,20298])). % 116.81/117.08 cnf(28026,plain, % 116.81/117.08 (~P5(a1,f11(f14(a1)))+P5(f11(f14(a1)),f9(f11(f14(a1))))), % 116.81/117.08 inference(scs_inference,[],[28022,21326])). % 116.81/117.08 cnf(28405,plain, % 116.81/117.08 (P15(f15(a1))+P20(f11(f15(a1)))), % 116.81/117.08 inference(scs_inference,[],[9018,123,3,1,43,45])). % 116.81/117.08 cnf(28466,plain, % 116.81/117.08 (P20(f11(f15(a1)))), % 116.81/117.08 inference(scs_inference,[],[123,3,1,28405,75])). % 116.81/117.08 cnf(28693,plain, % 116.81/117.08 (P15(f14(a1))+~P14(f10(f14(a1)))), % 116.81/117.08 inference(scs_inference,[],[6790,123,3,1,71,44])). % 116.81/117.08 cnf(29000,plain, % 116.81/117.08 (~P14(f10(f14(a1)))), % 116.81/117.08 inference(scs_inference,[],[123,3,1,28693,74])). % 116.81/117.08 cnf(29001,plain, % 116.81/117.08 (~P2(f10(f14(a1)))+~P13(f10(f14(a1)))), % 116.81/117.08 inference(scs_inference,[],[29000,11])). % 116.81/117.08 cnf(29063,plain, % 116.81/117.08 (~P2(f10(f14(a1)))+~P12(f10(f14(a1)))), % 116.81/117.08 inference(scs_inference,[],[29001,10])). % 116.81/117.08 cnf(29315,plain, % 116.81/117.08 (~P2(f10(f14(a1)))+~P11(f10(f14(a1)))), % 116.81/117.08 inference(scs_inference,[],[29063,9])). % 116.81/117.08 cnf(29373,plain, % 116.81/117.08 (~P11(f10(f14(a1)))+~P5(a1,f10(f14(a1)))), % 116.81/117.08 inference(scs_inference,[],[29315,16])). % 116.81/117.08 cnf(29694,plain, % 116.81/117.08 (P15(f15(a1))+~P14(f11(f15(a1)))), % 116.81/117.08 inference(scs_inference,[],[9018,123,3,1,72,45])). % 116.81/117.09 cnf(29828,plain, % 116.81/117.09 (P5(a1,f14(a1))), % 116.81/117.09 inference(scs_inference,[],[1,3,123,95])). % 116.81/117.09 cnf(29830,plain, % 116.81/117.09 (~P15(f14(a1))), % 116.81/117.09 inference(scs_inference,[],[1,3,123,95,74])). % 116.81/117.09 cnf(29832,plain, % 116.81/117.09 (~P15(f15(a1))), % 116.81/117.09 inference(scs_inference,[],[1,3,123,95,74,75])). % 116.81/117.09 cnf(29846,plain, % 116.81/117.09 (P14(f8(f10(f15(a1))))+~P2(f10(f15(a1)))), % 116.81/117.09 inference(scs_inference,[],[29832,26799])). % 116.81/117.09 cnf(29851,plain, % 116.81/117.09 (~P14(f11(f15(a1)))), % 116.81/117.09 inference(scs_inference,[],[29832,29694])). % 116.81/117.09 cnf(29854,plain, % 116.81/117.09 (~P5(f15(a1),f14(a1))), % 116.81/117.09 inference(scs_inference,[],[11276,8955,6725,11446,6790,9018,116,115])). % 116.81/117.09 cnf(30898,plain, % 116.81/117.09 (P5(f15(a1),f10(f15(a1)))), % 116.81/117.09 inference(scs_inference,[],[11627,29832,11446,16,93])). % 116.81/117.09 cnf(31232,plain, % 116.81/117.09 (P5(a1,f11(f14(a1)))), % 116.81/117.09 inference(scs_inference,[],[29828,6790,11276,29830,119,94])). % 116.81/117.09 cnf(31257,plain, % 116.81/117.09 (P5(a1,f10(f15(a1)))), % 116.81/117.09 inference(scs_inference,[],[11627,11446,9018,29832,119,93])). % 116.81/117.09 cnf(31271,plain, % 116.81/117.09 (P5(a1,f10(f14(a1)))), % 116.81/117.09 inference(scs_inference,[],[29828,11276,29830,6790,119,93])). % 116.81/117.09 cnf(31311,plain, % 116.81/117.09 (~P5(f15(a1),a1)), % 116.81/117.09 inference(scs_inference,[],[29854,3,123,1,119,95])). % 116.81/117.09 cnf(31352,plain, % 116.81/117.09 (~P5(f11(f15(a1)),a1)), % 116.81/117.09 inference(scs_inference,[],[31311,11446,29832,9018,119,94])). % 116.81/117.09 cnf(31410,plain, % 116.81/117.09 (~P2(f11(f15(a1)))+~P15(f11(f15(a1)))+P14(f9(f11(f15(a1))))), % 116.81/117.09 inference(scs_inference,[],[9018,11446,29832,39,72])). % 116.81/117.09 cnf(31421,plain, % 116.81/117.09 (~P2(f11(f15(a1)))+P14(f11(f15(a1)))+P14(f9(f11(f15(a1))))), % 116.81/117.09 inference(scs_inference,[],[9018,11446,29832,39,42])). % 116.81/117.09 cnf(31434,plain, % 116.81/117.09 (~P2(f11(f15(a1)))+~P15(f11(f15(a1)))+P19(f9(f11(f15(a1))))), % 116.81/117.09 inference(scs_inference,[],[9018,11446,29832,40,72])). % 116.81/117.09 cnf(31571,plain, % 116.81/117.09 (~P2(f10(f15(a1)))+P14(f10(f15(a1)))+P5(f10(f15(a1)),f8(f10(f15(a1))))), % 116.81/117.09 inference(scs_inference,[],[9018,29832,11446,41,91])). % 116.81/117.09 cnf(31589,plain, % 116.81/117.09 (~P2(f10(f14(a1)))+P14(f10(f14(a1)))+P5(f10(f14(a1)),f8(f10(f14(a1))))), % 116.81/117.09 inference(scs_inference,[],[6790,29830,11276,41,91])). % 116.81/117.09 cnf(31718,plain, % 116.81/117.09 (P5(f14(a1),f11(f14(a1)))), % 116.81/117.09 inference(scs_inference,[],[6790,29830,1,123,3,94,44])). % 116.81/117.09 cnf(33428,plain, % 116.81/117.09 (~P2(f11(f14(a1)))+~P15(f11(f14(a1)))+P14(f8(f11(f14(a1))))), % 116.81/117.09 inference(scs_inference,[],[6790,29830,11276,38,72])). % 116.81/117.09 cnf(33480,plain, % 116.81/117.09 (P14(f8(f11(f15(a1))))), % 116.81/117.09 inference(scs_inference,[],[29851,21491])). % 116.81/117.09 cnf(33491,plain, % 116.81/117.09 (P14(f8(f10(f15(a1))))), % 116.81/117.09 inference(scs_inference,[],[31257,27647])). % 116.81/117.09 cnf(33495,plain, % 116.81/117.09 (P14(f9(f11(f14(a1))))), % 116.81/117.09 inference(scs_inference,[],[31232,28023])). % 116.81/117.09 cnf(33497,plain, % 116.81/117.09 (~P19(f8(f11(f14(a1))))), % 116.81/117.09 inference(scs_inference,[],[31232,28025])). % 116.81/117.09 cnf(33498,plain, % 116.81/117.09 (P5(f11(f14(a1)),f9(f11(f14(a1))))), % 116.81/117.09 inference(scs_inference,[],[31232,28026])). % 116.81/117.09 cnf(33501,plain, % 116.81/117.09 (~P11(f10(f14(a1)))), % 116.81/117.09 inference(scs_inference,[],[31271,29373])). % 116.81/117.09 cnf(33502,plain, % 116.81/117.09 (P14(f9(f11(f15(a1))))), % 116.81/117.09 inference(scs_inference,[],[9019,11630,31410])). % 116.81/117.09 cnf(33503,plain, % 116.81/117.09 (P14(f9(f11(f15(a1))))), % 116.81/117.09 inference(scs_inference,[],[29851,11630,31421])). % 116.81/117.09 cnf(33504,plain, % 116.81/117.09 (P19(f9(f11(f15(a1))))), % 116.81/117.09 inference(scs_inference,[],[9019,11630,31434])). % 116.81/117.09 cnf(33511,plain, % 116.81/117.09 (P5(f10(f15(a1)),f8(f10(f15(a1))))+~P2(f10(f15(a1)))), % 116.81/117.09 inference(scs_inference,[],[9022,31571])). % 116.81/117.09 cnf(33512,plain, % 116.81/117.09 (P5(f10(f14(a1)),f8(f10(f14(a1))))+~P2(f10(f14(a1)))), % 116.81/117.09 inference(scs_inference,[],[29000,31589])). % 116.81/117.09 cnf(33514,plain, % 116.81/117.09 (P14(f8(f11(f14(a1))))+~P2(f11(f14(a1)))), % 116.81/117.09 inference(scs_inference,[],[28022,33428])). % 116.81/117.09 cnf(33516,plain, % 116.81/117.09 (P2(f10(f15(a1)))), % 116.81/117.09 inference(scs_inference,[],[31257,16])). % 116.81/117.09 cnf(33520,plain, % 116.81/117.09 (P6(f10(f15(a1)))), % 116.81/117.09 inference(scs_inference,[],[31257,27646,16,15,13])). % 116.81/117.09 cnf(33526,plain, % 116.81/117.09 (~P13(f8(f10(f15(a1))))), % 116.81/117.09 inference(scs_inference,[],[31257,27646,9022,16,15,13,14,39,68])). % 116.81/117.09 cnf(33528,plain, % 116.81/117.09 (~P13(f9(f11(f15(a1))))), % 116.81/117.09 inference(scs_inference,[],[31257,27646,29851,9022,11630,9019,16,15,13,14,39,68,69])). % 116.81/117.09 cnf(33532,plain, % 116.81/117.09 (P5(f11(f15(a1)),f8(f11(f15(a1))))), % 116.81/117.09 inference(scs_inference,[],[31257,27646,29851,9022,11630,9019,16,15,13,14,39,68,69,70,91])). % 116.81/117.09 cnf(33534,plain, % 116.81/117.09 (P5(f11(f15(a1)),f9(f11(f15(a1))))), % 116.81/117.09 inference(scs_inference,[],[31257,27646,29851,9022,11630,9019,16,15,13,14,39,68,69,70,91,92])). % 116.81/117.09 cnf(33536,plain, % 116.81/117.09 (~P21(f10(f14(a1)))), % 116.81/117.09 inference(scs_inference,[],[6790,31257,27646,29851,8007,9022,11630,6215,8955,11276,9019,16,15,13,14,39,68,69,70,91,92,116])). % 116.81/117.09 cnf(33553,plain, % 116.81/117.09 (P14(f8(f10(f15(a1))))), % 116.81/117.09 inference(scs_inference,[],[33516,29846])). % 116.81/117.09 cnf(33555,plain, % 116.81/117.09 (P5(a1,f9(f11(f14(a1))))), % 116.81/117.09 inference(scs_inference,[],[31232,33498,119])). % 116.81/117.09 cnf(33559,plain, % 116.81/117.09 (P21(f10(f15(a1)))), % 116.81/117.09 inference(scs_inference,[],[31232,33516,33520,33498,30898,27646,9022,11446,9018,6725,119,92,115])). % 116.81/117.09 cnf(33561,plain, % 116.81/117.09 (~P2(f10(f14(a1)))+~P10(f10(f14(a1)))), % 116.81/117.09 inference(scs_inference,[],[31232,33501,33516,33520,33498,30898,27646,9022,11446,9018,6725,119,92,115,8])). % 116.81/117.09 cnf(33565,plain, % 116.81/117.09 (~P13(f8(f11(f15(a1))))), % 116.81/117.09 inference(scs_inference,[],[31232,33501,33516,33520,33498,30898,29851,27646,9022,11630,11446,9018,9019,6725,119,92,115,8,70,68])). % 116.81/117.09 cnf(33570,plain, % 116.81/117.09 (P5(f10(f15(a1)),f8(f10(f15(a1))))), % 116.81/117.09 inference(scs_inference,[],[33516,33511])). % 116.81/117.09 cnf(33573,plain, % 116.81/117.09 (~P2(f8(f11(f15(a1))))+P13(f7(f8(f11(f15(a1)))))), % 116.81/117.09 inference(scs_inference,[],[33536,33559,33480,33565,33520,33516,8007,115,36])). % 116.81/117.09 cnf(33575,plain, % 116.81/117.09 (~P5(f14(a1),f10(f15(a1)))), % 116.81/117.09 inference(scs_inference,[],[33536,33559,33480,33565,33520,33516,8007,8955,11276,6790,115,36,116])). % 116.81/117.09 cnf(33583,plain, % 116.81/117.09 (P2(f10(f14(a1)))), % 116.81/117.09 inference(scs_inference,[],[31271,16])). % 116.81/117.09 cnf(33585,plain, % 116.81/117.09 (P5(f15(a1),f8(f10(f15(a1))))), % 116.81/117.09 inference(scs_inference,[],[31271,33570,30898,16,119])). % 116.81/117.09 cnf(33587,plain, % 116.81/117.09 (P14(f8(f10(f14(a1))))), % 116.81/117.09 inference(scs_inference,[],[6791,31271,33570,30898,29000,16,119,38])). % 116.81/117.09 cnf(33595,plain, % 116.81/117.09 (~P13(f8(f10(f14(a1))))), % 116.81/117.09 inference(scs_inference,[],[6791,31271,33570,30898,29000,16,119,38,40,39,70,68])). % 116.81/117.09 cnf(33601,plain, % 116.81/117.09 (~P10(f10(f14(a1)))), % 116.81/117.09 inference(scs_inference,[],[6791,31271,33570,33536,30898,33559,29000,33520,8007,6476,11446,11650,9018,6725,16,119,38,40,39,70,68,115,116,33561])). % 116.81/117.09 cnf(33622,plain, % 116.81/117.09 (P5(f10(f14(a1)),f8(f10(f14(a1))))), % 116.81/117.09 inference(scs_inference,[],[33583,33512])). % 116.81/117.09 cnf(33628,plain, % 116.81/117.09 (~P2(f9(f11(f15(a1))))+P18(f6(f9(f11(f15(a1)))))), % 116.81/117.09 inference(scs_inference,[],[31718,33583,33601,33502,33528,33575,119,7,35])). % 116.81/117.09 cnf(33630,plain, % 116.81/117.09 (P2(f9(f11(f14(a1))))), % 116.81/117.09 inference(scs_inference,[],[31718,33583,33601,33502,33528,33555,33575,119,7,35,16])). % 116.81/117.09 cnf(33638,plain, % 116.81/117.09 (P15(f9(f11(f14(a1))))), % 116.81/117.09 inference(scs_inference,[],[33495,33630,12])). % 116.81/117.09 cnf(33656,plain, % 116.81/117.09 (P5(a1,f8(f10(f15(a1))))), % 116.81/117.09 inference(scs_inference,[],[33585,31232,11627,15,119])). % 116.81/117.09 cnf(33660,plain, % 116.81/117.09 (~P5(f10(f15(a1)),f11(f15(a1)))), % 116.81/117.09 inference(scs_inference,[],[33585,31232,4958,27646,33516,11630,11627,28466,9019,15,119,113,114])). % 116.81/117.09 cnf(33672,plain, % 116.81/117.09 (~P2(f8(f10(f14(a1))))+~P12(f7(f8(f10(f14(a1)))))), % 116.81/117.09 inference(scs_inference,[],[31352,33587,33595,33532,119,66])). % 116.81/117.09 cnf(33676,plain, % 116.81/117.09 (P15(f9(f11(f15(a1))))+~P2(f9(f11(f15(a1))))), % 116.81/117.09 inference(scs_inference,[],[31352,33503,33587,33595,33638,33532,33630,119,66,13,12])). % 116.81/117.09 cnf(33682,plain, % 116.81/117.09 (P2(f8(f10(f15(a1))))), % 116.81/117.09 inference(scs_inference,[],[33660,33656,6476,119,16])). % 116.81/117.09 cnf(33686,plain, % 116.81/117.09 (~P18(f7(f8(f10(f15(a1)))))), % 116.81/117.09 inference(scs_inference,[],[33660,33553,33656,33495,33526,33630,6476,119,16,89,65])). % 116.81/117.09 cnf(33698,plain, % 116.81/117.09 (~P5(a1,f7(f8(f10(f15(a1)))))), % 116.81/117.09 inference(scs_inference,[],[33686,15])). % 116.81/117.09 cnf(33700,plain, % 116.81/117.09 (P5(a1,f8(f10(f14(a1))))), % 116.81/117.09 inference(scs_inference,[],[33622,33686,31271,15,119])). % 116.81/117.09 cnf(33702,plain, % 116.81/117.09 (~P12(f6(f8(f10(f15(a1)))))), % 116.81/117.09 inference(scs_inference,[],[33682,33622,33686,33491,31271,33526,15,119,67])). % 116.81/117.09 cnf(33708,plain, % 116.81/117.09 (P5(f8(f10(f15(a1))),f7(f8(f10(f15(a1)))))), % 116.81/117.09 inference(scs_inference,[],[33682,33622,33686,33491,31271,33526,15,119,67,90,66,89])). % 116.81/117.09 cnf(33717,plain, % 116.81/117.09 (P2(f11(f14(a1)))), % 116.81/117.09 inference(scs_inference,[],[31232,16])). % 116.81/117.09 cnf(33733,plain, % 116.81/117.09 (P14(f8(f11(f14(a1))))), % 116.81/117.09 inference(scs_inference,[],[33717,33514])). % 116.81/117.09 cnf(33737,plain, % 116.81/117.09 (P2(f8(f10(f14(a1))))), % 116.81/117.09 inference(scs_inference,[],[33656,33700,15,16])). % 116.81/117.09 cnf(33744,plain, % 116.81/117.09 (P5(a1,f8(f11(f15(a1))))), % 116.81/117.09 inference(scs_inference,[],[11628,33526,33682,33491,33656,33532,33700,15,16,33672,12,10,119])). % 116.81/117.09 cnf(33760,plain, % 116.81/117.09 (P5(f11(f14(a1)),f8(f11(f14(a1))))), % 116.81/117.09 inference(scs_inference,[],[11628,33526,33682,6794,33491,28022,33656,33532,33587,33595,33717,33700,15,16,33672,12,10,119,9,13,14,8,89,35,67,91])). % 116.81/117.09 cnf(33762,plain, % 116.81/117.09 (P13(f7(f8(f10(f14(a1)))))), % 116.81/117.09 inference(scs_inference,[],[11628,33526,33682,6794,33491,28022,33656,33532,33587,33595,33717,33700,15,16,33672,12,10,119,9,13,14,8,89,35,67,91,36])). % 116.81/117.09 cnf(33768,plain, % 116.81/117.09 (P19(f9(f11(f14(a1))))), % 116.81/117.09 inference(scs_inference,[],[11628,33526,33682,6794,33491,28022,33656,33532,33587,33595,33717,33700,15,16,33672,12,10,119,9,13,14,8,89,35,67,91,36,65,90,40])). % 116.81/117.09 cnf(33785,plain, % 116.81/117.09 (P2(f8(f11(f15(a1))))), % 116.81/117.09 inference(scs_inference,[],[33744,16])). % 116.81/117.09 cnf(33789,plain, % 116.81/117.09 (P13(f7(f8(f11(f15(a1)))))), % 116.81/117.09 inference(scs_inference,[],[33555,33744,16,15,33573])). % 116.81/117.09 cnf(33794,plain, % 116.81/117.09 (P5(a1,f9(f11(f15(a1))))), % 116.81/117.09 inference(scs_inference,[],[11628,33587,33595,33555,33737,33534,33744,16,15,33573,12,10,119])). % 116.81/117.09 cnf(33810,plain, % 116.81/117.09 (~P5(f9(f11(f14(a1))),f8(f11(f14(a1))))), % 116.81/117.09 inference(scs_inference,[],[11628,33630,33587,33595,33495,33555,33480,33565,33737,33534,33744,33733,33497,33768,16,15,33573,12,10,119,66,90,65,35,67,89,37,111])). % 116.81/117.09 cnf(33816,plain, % 116.81/117.09 (~P11(f8(f10(f14(a1))))), % 116.81/117.09 inference(scs_inference,[],[11628,33630,33587,33595,33495,33555,33480,33565,33737,33534,33744,33733,33497,33768,16,15,33573,12,10,119,66,90,65,35,67,89,37,111,7,13,9])). % 116.81/117.09 cnf(33826,plain, % 116.81/117.09 (P2(f9(f11(f15(a1))))), % 116.81/117.09 inference(scs_inference,[],[33700,33794,15,16])). % 116.81/117.09 cnf(33834,plain, % 116.81/117.09 (P15(f8(f11(f15(a1))))), % 116.81/117.09 inference(scs_inference,[],[33480,33737,33700,33785,33794,33816,15,16,33676,33628,13,8,12])). % 116.81/117.09 cnf(33840,plain, % 116.81/117.09 (~P5(f9(f11(f14(a1))),f11(f14(a1)))), % 116.81/117.09 inference(scs_inference,[],[33480,33565,33737,33700,33785,33810,33760,33794,33816,15,16,33676,33628,13,8,12,14,10,119])). % 116.81/117.09 cnf(33864,plain, % 116.81/117.09 (~P11(f8(f11(f15(a1))))), % 116.81/117.09 inference(scs_inference,[],[33480,33565,33737,33700,33502,33733,33528,33497,33785,33810,33760,33794,33762,33816,33504,15,16,33676,33628,13,8,12,14,10,119,90,66,35,65,36,89,67,37,111,11,7,9])). % 116.81/117.09 cnf(33866,plain, % 116.81/117.09 (~P8(f8(f10(f14(a1))))), % 116.81/117.09 inference(scs_inference,[],[33480,33565,33737,33700,33502,33733,33528,33497,33785,33810,33760,33794,33762,33816,33504,15,16,33676,33628,13,8,12,14,10,119,90,66,35,65,36,89,67,37,111,11,7,9,6])). % 116.81/117.09 cnf(33881,plain, % 116.81/117.09 (~P12(f9(f11(f15(a1))))), % 116.81/117.09 inference(scs_inference,[],[33737,33528,33785,31232,33744,33826,33840,33834,33864,33866,15,5,13,8,119,10])). % 116.81/117.09 cnf(33889,plain, % 116.81/117.09 (~P8(f8(f11(f15(a1))))), % 116.81/117.09 inference(scs_inference,[],[33737,33528,33785,31232,33744,33826,33840,33834,33864,33866,33702,15,5,13,8,119,10,9,14,7,6])). % 116.81/117.09 cnf(33912,plain, % 116.81/117.09 (~P8(f9(f11(f15(a1))))), % 116.81/117.09 inference(scs_inference,[],[33785,31718,33840,33794,33826,33789,33889,33881,15,9,5,8,119,7,11,6])). % 116.81/117.09 cnf(33922,plain, % 116.81/117.09 ($false), % 116.81/117.09 inference(scs_inference,[],[33826,33656,33698,33708,33912,5,119]), % 116.81/117.09 ['proof']). % 116.81/117.09 % SZS output end Proof % 116.81/117.09 % Total time :116.346099s %------------------------------------------------------------------------------