%------------------------------------------------------------------------------ % File : E-Darwin---1.5 % Problem : SYN823-1 : TPTP v6.1.0. Released v2.5.0. % Transfm : none % Format : tptp:raw % Command : e-darwin -pev TPTP -pmd true -if tptp -pl 2 -pc false -ps false %s % Computer : n017.star.cs.uiowa.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2609 0 2.40GHz % Memory : 16127.75MB % OS : Linux 2.6.32-431.20.3.el6.x86_64 % CPULimit : 300s % DateTime : Fri Aug 1 22:18:25 EDT 2014 % Result : Satisfiable 0.31s % Output : Model 0.31s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : SYN823-1 : TPTP v6.1.0. Released v2.5.0. % % Command : e-darwin -pev TPTP -pmd true -if tptp -pl 2 -pc false -ps false %s % % Computer : n017.star.cs.uiowa.edu % % Model : x86_64 x86_64 % % CPU : Intel(R) Xeon(R) CPU E5-2609 0 @ 2.40GHz % % Memory : 16127.75MB % % OS : Linux 2.6.32-431.20.3.el6.x86_64 % % CPULimit : 300 % % DateTime : Sat Jul 26 13:10:21 CDT 2014 % % CPUTime: 0.31 % E-Darwin 1.5 2012/06/20 (based on Darwin 1.3) % % % Defaulting to tptp format. % Parsing /export/starexec/sandbox/benchmark/theBenchmark.p ... % % % % Proving ... % % % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % % START OF MODEL (DIG): % ssNder1_0 % ssNder1_10r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9) % ssNder1_11r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10) % ssNder1_12r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11) % ssNder1_13r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12) % ssNder1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13) % ssNder1_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14) % ssNder1_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15) % ssNder1_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16) % ssNder1_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17) % ssNder1_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18) % ssNder1_1r1(_0) % ssNder1_2r1r1(_0, _1) % ssNder1_3r1r1r1(_0, _1, _2) % ssNder1_4r1r1r1r1(_0, _1, _2, _3) % ssNder1_5r1r1r1r1r1(_0, _1, _2, _3, _4) % ssNder1_6r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5) % ssNder1_7r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6) % ssNder1_8r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7) % ssNder1_9r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8) % ssPv11_10r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9) % ssPv11_11r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10) % ssPv11_12r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11) % ssPv11_13r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12) % ssPv11_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13) % ssPv11_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14) % ssPv11_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15) % ssPv11_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16) % ssPv11_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17) % ssPv11_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18) % ssPv11_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19) % ssPv12_3r1r1r1(_0, _1, _2) % ssPv12_6r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5) % ssPv12_7r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6) % ssPv13_10r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, skc16, _7, _8) % ssPv13_11r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, skc16, _7, _8, _9) % ssPv13_12r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, skc16, _7, _8, _9, _10) % ssPv13_13r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, skc16, _7, _8, _9, _10, _11) % ssPv13_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, skc16, _7, _8, _9, _10, _11, _12) % ssPv13_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, skc16, _7, _8, _9, _10, _11, _12, _13) % ssPv13_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, skc16, _7, _8, _9, _10, _11, _12, _13, _14) % ssPv13_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, skc16, _7, _8, _9, _10, _11, _12, _13, _14, _15) % ssPv13_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, skc16, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16) % ssPv13_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, skc16, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17) % ssPv13_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, skc16, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18) % ssPv13_8r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, skc16) % ssPv13_9r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, skc16, _7) % ssPv14_10r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, skc18, _6, _7, _8) % ssPv14_11r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, skc18, _6, _7, _8, _9) % ssPv14_12r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, skc18, _6, _7, _8, _9, _10) % ssPv14_13r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, skc18, _6, _7, _8, _9, _10, _11) % ssPv14_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, skc18, _6, _7, _8, _9, _10, _11, _12) % ssPv14_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, skc18, _6, _7, _8, _9, _10, _11, _12, _13) % ssPv14_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, skc18, _6, _7, _8, _9, _10, _11, _12, _13, _14) % ssPv14_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, skc18, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15) % ssPv14_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, skc18, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16) % ssPv14_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, skc18, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17) % ssPv14_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, skc18, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18) % ssPv14_7r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, skc18) % ssPv14_8r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, skc18, _6) % ssPv14_9r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, skc18, _6, _7) % ssPv15_10r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, skc20, _5, _6, _7, _8) % ssPv15_11r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, skc20, _5, _6, _7, _8, _9) % ssPv15_12r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, skc20, _5, _6, _7, _8, _9, _10) % ssPv15_13r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, skc20, _5, _6, _7, _8, _9, _10, _11) % ssPv15_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, skc20, _5, _6, _7, _8, _9, _10, _11, _12) % ssPv15_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, skc20, _5, _6, _7, _8, _9, _10, _11, _12, _13) % ssPv15_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, skc20, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14) % ssPv15_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, skc20, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15) % ssPv15_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, skc20, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16) % ssPv15_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, skc20, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17) % ssPv15_1r1(_0) % ssPv15_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, skc20, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18) % ssPv15_6r1r1r1r1r1r1(_0, _1, _2, _3, _4, skc20) % ssPv15_7r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, skc20, _5) % ssPv15_8r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, skc20, _5, _6) % ssPv15_9r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, skc20, _5, _6, _7) % ssPv16_10r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, skc22, _4, _5, _6, _7, _8) % ssPv16_11r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, skc22, _4, _5, _6, _7, _8, _9) % ssPv16_12r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, skc22, _4, _5, _6, _7, _8, _9, _10) % ssPv16_13r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, skc22, _4, _5, _6, _7, _8, _9, _10, _11) % ssPv16_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, skc22, _4, _5, _6, _7, _8, _9, _10, _11, _12) % ssPv16_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, skc22, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13) % ssPv16_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, skc22, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14) % ssPv16_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, skc22, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15) % ssPv16_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, skc22, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16) % ssPv16_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, skc22, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17) % ssPv16_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, skc22, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18) % ssPv16_5r1r1r1r1r1(_0, _1, _2, _3, skc22) % ssPv16_6r1r1r1r1r1r1(_0, _1, _2, _3, skc22, _4) % ssPv16_7r1r1r1r1r1r1r1(_0, _1, _2, _3, skc22, _4, _5) % ssPv16_8r1r1r1r1r1r1r1r1(_0, _1, _2, _3, skc22, _4, _5, _6) % ssPv16_9r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, skc22, _4, _5, _6, _7) % ssPv17_10r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9) % ssPv17_11r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10) % ssPv17_12r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11) % ssPv17_13r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12) % ssPv17_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13) % ssPv17_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14) % ssPv17_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15) % ssPv17_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16) % ssPv17_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17) % ssPv17_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18) % ssPv17_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19) % ssPv17_4r1r1r1r1(_0, _1, _2, _3) % ssPv17_5r1r1r1r1r1(_0, _1, _2, _3, _4) % ssPv17_6r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5) % ssPv17_7r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6) % ssPv17_8r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7) % ssPv17_9r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8) % ssPv18_10r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9) % ssPv18_11r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10) % ssPv18_12r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11) % ssPv18_13r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12) % ssPv18_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13) % ssPv18_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14) % ssPv18_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15) % ssPv18_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16) % ssPv18_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17) % ssPv18_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18) % ssPv18_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19) % ssPv18_3r1r1r1(_0, _1, _2) % ssPv18_4r1r1r1r1(_0, _1, _2, _3) % ssPv18_5r1r1r1r1r1(_0, _1, _2, _3, _4) % ssPv18_6r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5) % ssPv18_7r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6) % ssPv18_8r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7) % ssPv18_9r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8) % ssPv1_12r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11) % ssPv1_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, skc18, _6, _7, _8, _9, _10, _11, _12) % ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, skc18, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18) % ssPv1_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, skc23, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18) % ssPv1_8r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7) % ssPv20_10r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9) % ssPv20_11r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10) % ssPv20_12r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11) % ssPv20_13r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12) % ssPv20_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13) % ssPv20_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14) % ssPv20_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15) % ssPv20_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16) % ssPv20_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17) % ssPv20_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18) % ssPv20_1r1(_0) % ssPv20_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19) % ssPv20_2r1r1(_0, _1) % ssPv20_3r1r1r1(_0, _1, _2) % ssPv20_4r1r1r1r1(_0, _1, _2, _3) % ssPv20_5r1r1r1r1r1(_0, _1, _2, _3, _4) % ssPv20_6r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5) % ssPv20_7r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6) % ssPv20_8r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7) % ssPv20_9r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8) % ssPv4_5r1r1r1r1r1(_0, _1, _2, _3, _4) % ssPv4_8r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7) % ssPv5_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, skc12) % ssPv5_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, skc12, _15) % ssPv5_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, skc12, _15, _16) % ssPv5_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, skc12, _15, _16, _17) % ssPv5_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, skc12, _15, _16, _17, _18) % ssPv5_5r1r1r1r1r1(_0, _1, _2, _3, _4) % ssPv7_11r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10) % ssPv7_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, skc14) % ssPv7_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, skc14, _13) % ssPv7_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, skc14, _13, _14) % ssPv7_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, skc14, _13, _14, _15) % ssPv7_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, skc14, _13, _14, _15, _16) % ssPv7_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, skc14, _13, _14, _15, _16, _17) % ssPv7_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, skc14, _13, _14, _15, _16, _17, _18) % ssPv7_5r1r1r1r1r1(_0, _1, _2, _3, _4) % ssPv7_7r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6) % ssPv9_12r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11) % ssPv9_13r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12) % ssPv9_14r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13) % ssPv9_15r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14) % ssPv9_16r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15) % ssPv9_17r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16) % ssPv9_18r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17) % ssPv9_19r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18) % ssPv9_20r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1r1(_0, _1, _2, _3, _4, _5, _6, _7, _8, _9, _10, _11, _12, _13, _14, _15, _16, _17, _18, _19) % ssPv9_5r1r1r1r1r1(_0, _1, _2, _3, _4) % END OF MODEL % EOF %------------------------------------------------------------------------------