%------------------------------------------------------------------------------ % File : E-Darwin---1.5 % Problem : LCL675+1.005 : TPTP v6.1.0. Released v4.0.0. % Transfm : none % Format : tptp:raw % Command : e-darwin -pev TPTP -pmd true -if tptp -pl 2 -pc false -ps false %s % Computer : n019.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:05:20 EDT 2014 % Result : CounterSatisfiable 43.62s % Output : Model 43.62s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : LCL675+1.005 : TPTP v6.1.0. Released v4.0.0. % % Command : e-darwin -pev TPTP -pmd true -if tptp -pl 2 -pc false -ps false %s % % Computer : n019.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 12:02:41 CDT 2014 % % CPUTime : 43.62 % 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 CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % % START OF MODEL (DIG): % p100(sK10(sK0)) % p100(sK8(sK10(sK0))) % p100(sK8(sK9(sK0))) % p100(sK6(sK8(sK10(sK0)))) % p100(sK6(sK8(sK9(sK0)))) % p100(sK6(sK7(sK10(sK0)))) % p100(sK6(sK7(sK9(sK0)))) % p100(sK4(sK6(sK8(sK10(sK0))))) % p100(sK4(sK6(sK8(sK9(sK0))))) % p100(sK4(sK6(sK7(sK10(sK0))))) % p100(sK4(sK6(sK7(sK9(sK0))))) % p100(sK4(sK5(sK8(sK10(sK0))))) % p100(sK4(sK5(sK8(sK9(sK0))))) % p100(sK4(sK5(sK7(sK10(sK0))))) % p100(sK4(sK5(sK7(sK9(sK0))))) % p100(sK2(sK4(sK6(sK8(sK10(sK0)))))) % p100(sK2(sK4(sK6(sK8(sK9(sK0)))))) % p100(sK2(sK4(sK6(sK7(sK10(sK0)))))) % p100(sK2(sK4(sK6(sK7(sK9(sK0)))))) % p100(sK2(sK4(sK5(sK8(sK10(sK0)))))) % p100(sK2(sK4(sK5(sK8(sK9(sK0)))))) % p100(sK2(sK4(sK5(sK7(sK10(sK0)))))) % p100(sK2(sK4(sK5(sK7(sK9(sK0)))))) % p100(sK2(sK3(sK6(sK8(sK10(sK0)))))) % p100(sK2(sK3(sK6(sK8(sK9(sK0)))))) % p100(sK2(sK3(sK6(sK7(sK10(sK0)))))) % p100(sK2(sK3(sK6(sK7(sK9(sK0)))))) % p100(sK2(sK3(sK5(sK8(sK10(sK0)))))) % p100(sK2(sK3(sK5(sK8(sK9(sK0)))))) % p100(sK2(sK3(sK5(sK7(sK10(sK0)))))) % p100(sK2(sK3(sK5(sK7(sK9(sK0)))))) % p100(sK1(sK4(sK6(sK8(sK10(sK0)))))) % p100(sK1(sK4(sK6(sK8(sK9(sK0)))))) % p100(sK1(sK4(sK6(sK7(sK10(sK0)))))) % p100(sK1(sK4(sK6(sK7(sK9(sK0)))))) % p100(sK1(sK4(sK5(sK8(sK10(sK0)))))) % p100(sK1(sK4(sK5(sK8(sK9(sK0)))))) % p100(sK1(sK4(sK5(sK7(sK10(sK0)))))) % p100(sK1(sK4(sK5(sK7(sK9(sK0)))))) % p100(sK1(sK3(sK6(sK8(sK10(sK0)))))) % p100(sK1(sK3(sK6(sK8(sK9(sK0)))))) % p100(sK1(sK3(sK6(sK7(sK10(sK0)))))) % p100(sK1(sK3(sK6(sK7(sK9(sK0)))))) % p100(sK1(sK3(sK5(sK8(sK10(sK0)))))) % p100(sK1(sK3(sK5(sK8(sK9(sK0)))))) % p100(sK1(sK3(sK5(sK7(sK10(sK0)))))) % p100(sK1(sK3(sK5(sK7(sK9(sK0)))))) % p100(sK9(sK0)) % p100(sK7(sK10(sK0))) % p100(sK7(sK9(sK0))) % p100(sK5(sK8(sK10(sK0)))) % p100(sK5(sK8(sK9(sK0)))) % p100(sK5(sK7(sK10(sK0)))) % p100(sK5(sK7(sK9(sK0)))) % p100(sK3(sK6(sK8(sK10(sK0))))) % p100(sK3(sK6(sK8(sK9(sK0))))) % p100(sK3(sK6(sK7(sK10(sK0))))) % p100(sK3(sK6(sK7(sK9(sK0))))) % p100(sK3(sK5(sK8(sK10(sK0))))) % p100(sK3(sK5(sK8(sK9(sK0))))) % p100(sK3(sK5(sK7(sK10(sK0))))) % p100(sK3(sK5(sK7(sK9(sK0))))) % p100(sK0) % p101(sK10(sK0)) % p101(sK8(sK10(sK0))) % p101(sK8(sK9(sK0))) % p101(sK6(sK8(sK10(sK0)))) % p101(sK6(sK8(sK9(sK0)))) % p101(sK6(sK7(sK10(sK0)))) % p101(sK6(sK7(sK9(sK0)))) % p101(sK4(sK6(sK8(sK10(sK0))))) % p101(sK4(sK6(sK8(sK9(sK0))))) % p101(sK4(sK6(sK7(sK10(sK0))))) % p101(sK4(sK6(sK7(sK9(sK0))))) % p101(sK4(sK5(sK8(sK10(sK0))))) % p101(sK4(sK5(sK8(sK9(sK0))))) % p101(sK4(sK5(sK7(sK10(sK0))))) % p101(sK4(sK5(sK7(sK9(sK0))))) % p101(sK2(sK4(sK6(sK8(sK10(sK0)))))) % p101(sK2(sK4(sK6(sK8(sK9(sK0)))))) % p101(sK2(sK4(sK6(sK7(sK10(sK0)))))) % p101(sK2(sK4(sK6(sK7(sK9(sK0)))))) % p101(sK2(sK4(sK5(sK8(sK10(sK0)))))) % p101(sK2(sK4(sK5(sK8(sK9(sK0)))))) % p101(sK2(sK4(sK5(sK7(sK10(sK0)))))) % p101(sK2(sK4(sK5(sK7(sK9(sK0)))))) % p101(sK2(sK3(sK6(sK8(sK10(sK0)))))) % p101(sK2(sK3(sK6(sK8(sK9(sK0)))))) % p101(sK2(sK3(sK6(sK7(sK10(sK0)))))) % p101(sK2(sK3(sK6(sK7(sK9(sK0)))))) % p101(sK2(sK3(sK5(sK8(sK10(sK0)))))) % p101(sK2(sK3(sK5(sK8(sK9(sK0)))))) % p101(sK2(sK3(sK5(sK7(sK10(sK0)))))) % p101(sK2(sK3(sK5(sK7(sK9(sK0)))))) % p101(sK1(sK4(sK6(sK8(sK10(sK0)))))) % p101(sK1(sK4(sK6(sK8(sK9(sK0)))))) % p101(sK1(sK4(sK6(sK7(sK10(sK0)))))) % p101(sK1(sK4(sK6(sK7(sK9(sK0)))))) % p101(sK1(sK4(sK5(sK8(sK10(sK0)))))) % p101(sK1(sK4(sK5(sK8(sK9(sK0)))))) % p101(sK1(sK4(sK5(sK7(sK10(sK0)))))) % p101(sK1(sK4(sK5(sK7(sK9(sK0)))))) % p101(sK1(sK3(sK6(sK8(sK10(sK0)))))) % p101(sK1(sK3(sK6(sK8(sK9(sK0)))))) % p101(sK1(sK3(sK6(sK7(sK10(sK0)))))) % p101(sK1(sK3(sK6(sK7(sK9(sK0)))))) % p101(sK1(sK3(sK5(sK8(sK10(sK0)))))) % p101(sK1(sK3(sK5(sK8(sK9(sK0)))))) % p101(sK1(sK3(sK5(sK7(sK10(sK0)))))) % p101(sK1(sK3(sK5(sK7(sK9(sK0)))))) % p101(sK9(sK0)) % p101(sK7(sK10(sK0))) % p101(sK7(sK9(sK0))) % p101(sK5(sK8(sK10(sK0)))) % p101(sK5(sK8(sK9(sK0)))) % p101(sK5(sK7(sK10(sK0)))) % p101(sK5(sK7(sK9(sK0)))) % p101(sK3(sK6(sK8(sK10(sK0))))) % p101(sK3(sK6(sK8(sK9(sK0))))) % p101(sK3(sK6(sK7(sK10(sK0))))) % p101(sK3(sK6(sK7(sK9(sK0))))) % p101(sK3(sK5(sK8(sK10(sK0))))) % p101(sK3(sK5(sK8(sK9(sK0))))) % p101(sK3(sK5(sK7(sK10(sK0))))) % p101(sK3(sK5(sK7(sK9(sK0))))) % p102(sK8(sK10(sK0))) % p102(sK8(sK9(sK0))) % p102(sK6(sK8(sK10(sK0)))) % p102(sK6(sK8(sK9(sK0)))) % p102(sK6(sK7(sK10(sK0)))) % p102(sK6(sK7(sK9(sK0)))) % p102(sK4(sK6(sK8(sK10(sK0))))) % p102(sK4(sK6(sK8(sK9(sK0))))) % p102(sK4(sK6(sK7(sK10(sK0))))) % p102(sK4(sK6(sK7(sK9(sK0))))) % p102(sK4(sK5(sK8(sK10(sK0))))) % p102(sK4(sK5(sK8(sK9(sK0))))) % p102(sK4(sK5(sK7(sK10(sK0))))) % p102(sK4(sK5(sK7(sK9(sK0))))) % p102(sK2(sK4(sK6(sK8(sK10(sK0)))))) % p102(sK2(sK4(sK6(sK8(sK9(sK0)))))) % p102(sK2(sK4(sK6(sK7(sK10(sK0)))))) % p102(sK2(sK4(sK6(sK7(sK9(sK0)))))) % p102(sK2(sK4(sK5(sK8(sK10(sK0)))))) % p102(sK2(sK4(sK5(sK8(sK9(sK0)))))) % p102(sK2(sK4(sK5(sK7(sK10(sK0)))))) % p102(sK2(sK4(sK5(sK7(sK9(sK0)))))) % p102(sK2(sK3(sK6(sK8(sK10(sK0)))))) % p102(sK2(sK3(sK6(sK8(sK9(sK0)))))) % p102(sK2(sK3(sK6(sK7(sK10(sK0)))))) % p102(sK2(sK3(sK6(sK7(sK9(sK0)))))) % p102(sK2(sK3(sK5(sK8(sK10(sK0)))))) % p102(sK2(sK3(sK5(sK8(sK9(sK0)))))) % p102(sK2(sK3(sK5(sK7(sK10(sK0)))))) % p102(sK2(sK3(sK5(sK7(sK9(sK0)))))) % p102(sK1(sK4(sK6(sK8(sK10(sK0)))))) % p102(sK1(sK4(sK6(sK8(sK9(sK0)))))) % p102(sK1(sK4(sK6(sK7(sK10(sK0)))))) % p102(sK1(sK4(sK6(sK7(sK9(sK0)))))) % p102(sK1(sK4(sK5(sK8(sK10(sK0)))))) % p102(sK1(sK4(sK5(sK8(sK9(sK0)))))) % p102(sK1(sK4(sK5(sK7(sK10(sK0)))))) % p102(sK1(sK4(sK5(sK7(sK9(sK0)))))) % p102(sK1(sK3(sK6(sK8(sK10(sK0)))))) % p102(sK1(sK3(sK6(sK8(sK9(sK0)))))) % p102(sK1(sK3(sK6(sK7(sK10(sK0)))))) % p102(sK1(sK3(sK6(sK7(sK9(sK0)))))) % p102(sK1(sK3(sK5(sK8(sK10(sK0)))))) % p102(sK1(sK3(sK5(sK8(sK9(sK0)))))) % p102(sK1(sK3(sK5(sK7(sK10(sK0)))))) % p102(sK1(sK3(sK5(sK7(sK9(sK0)))))) % p102(sK7(sK10(sK0))) % p102(sK7(sK9(sK0))) % p102(sK5(sK8(sK10(sK0)))) % p102(sK5(sK8(sK9(sK0)))) % p102(sK5(sK7(sK10(sK0)))) % p102(sK5(sK7(sK9(sK0)))) % p102(sK3(sK6(sK8(sK10(sK0))))) % p102(sK3(sK6(sK8(sK9(sK0))))) % p102(sK3(sK6(sK7(sK10(sK0))))) % p102(sK3(sK6(sK7(sK9(sK0))))) % p102(sK3(sK5(sK8(sK10(sK0))))) % p102(sK3(sK5(sK8(sK9(sK0))))) % p102(sK3(sK5(sK7(sK10(sK0))))) % p102(sK3(sK5(sK7(sK9(sK0))))) % p103(sK6(sK8(sK10(sK0)))) % p103(sK6(sK8(sK9(sK0)))) % p103(sK6(sK7(sK10(sK0)))) % p103(sK6(sK7(sK9(sK0)))) % p103(sK4(sK6(sK8(sK10(sK0))))) % p103(sK4(sK6(sK8(sK9(sK0))))) % p103(sK4(sK6(sK7(sK10(sK0))))) % p103(sK4(sK6(sK7(sK9(sK0))))) % p103(sK4(sK5(sK8(sK10(sK0))))) % p103(sK4(sK5(sK8(sK9(sK0))))) % p103(sK4(sK5(sK7(sK10(sK0))))) % p103(sK4(sK5(sK7(sK9(sK0))))) % p103(sK2(sK4(sK6(sK8(sK10(sK0)))))) % p103(sK2(sK4(sK6(sK8(sK9(sK0)))))) % p103(sK2(sK4(sK6(sK7(sK10(sK0)))))) % p103(sK2(sK4(sK6(sK7(sK9(sK0)))))) % p103(sK2(sK4(sK5(sK8(sK10(sK0)))))) % p103(sK2(sK4(sK5(sK8(sK9(sK0)))))) % p103(sK2(sK4(sK5(sK7(sK10(sK0)))))) % p103(sK2(sK4(sK5(sK7(sK9(sK0)))))) % p103(sK2(sK3(sK6(sK8(sK10(sK0)))))) % p103(sK2(sK3(sK6(sK8(sK9(sK0)))))) % p103(sK2(sK3(sK6(sK7(sK10(sK0)))))) % p103(sK2(sK3(sK6(sK7(sK9(sK0)))))) % p103(sK2(sK3(sK5(sK8(sK10(sK0)))))) % p103(sK2(sK3(sK5(sK8(sK9(sK0)))))) % p103(sK2(sK3(sK5(sK7(sK10(sK0)))))) % p103(sK2(sK3(sK5(sK7(sK9(sK0)))))) % p103(sK1(sK4(sK6(sK8(sK10(sK0)))))) % p103(sK1(sK4(sK6(sK8(sK9(sK0)))))) % p103(sK1(sK4(sK6(sK7(sK10(sK0)))))) % p103(sK1(sK4(sK6(sK7(sK9(sK0)))))) % p103(sK1(sK4(sK5(sK8(sK10(sK0)))))) % p103(sK1(sK4(sK5(sK8(sK9(sK0)))))) % p103(sK1(sK4(sK5(sK7(sK10(sK0)))))) % p103(sK1(sK4(sK5(sK7(sK9(sK0)))))) % p103(sK1(sK3(sK6(sK8(sK10(sK0)))))) % p103(sK1(sK3(sK6(sK8(sK9(sK0)))))) % p103(sK1(sK3(sK6(sK7(sK10(sK0)))))) % p103(sK1(sK3(sK6(sK7(sK9(sK0)))))) % p103(sK1(sK3(sK5(sK8(sK10(sK0)))))) % p103(sK1(sK3(sK5(sK8(sK9(sK0)))))) % p103(sK1(sK3(sK5(sK7(sK10(sK0)))))) % p103(sK1(sK3(sK5(sK7(sK9(sK0)))))) % p103(sK5(sK8(sK10(sK0)))) % p103(sK5(sK8(sK9(sK0)))) % p103(sK5(sK7(sK10(sK0)))) % p103(sK5(sK7(sK9(sK0)))) % p103(sK3(sK6(sK8(sK10(sK0))))) % p103(sK3(sK6(sK8(sK9(sK0))))) % p103(sK3(sK6(sK7(sK10(sK0))))) % p103(sK3(sK6(sK7(sK9(sK0))))) % p103(sK3(sK5(sK8(sK10(sK0))))) % p103(sK3(sK5(sK8(sK9(sK0))))) % p103(sK3(sK5(sK7(sK10(sK0))))) % p103(sK3(sK5(sK7(sK9(sK0))))) % p104(sK4(sK6(sK8(sK10(sK0))))) % p104(sK4(sK6(sK8(sK9(sK0))))) % p104(sK4(sK6(sK7(sK10(sK0))))) % p104(sK4(sK6(sK7(sK9(sK0))))) % p104(sK4(sK5(sK8(sK10(sK0))))) % p104(sK4(sK5(sK8(sK9(sK0))))) % p104(sK4(sK5(sK7(sK10(sK0))))) % p104(sK4(sK5(sK7(sK9(sK0))))) % p104(sK2(sK4(sK6(sK8(sK10(sK0)))))) % p104(sK2(sK4(sK6(sK8(sK9(sK0)))))) % p104(sK2(sK4(sK6(sK7(sK10(sK0)))))) % p104(sK2(sK4(sK6(sK7(sK9(sK0)))))) % p104(sK2(sK4(sK5(sK8(sK10(sK0)))))) % p104(sK2(sK4(sK5(sK8(sK9(sK0)))))) % p104(sK2(sK4(sK5(sK7(sK10(sK0)))))) % p104(sK2(sK4(sK5(sK7(sK9(sK0)))))) % p104(sK2(sK3(sK6(sK8(sK10(sK0)))))) % p104(sK2(sK3(sK6(sK8(sK9(sK0)))))) % p104(sK2(sK3(sK6(sK7(sK10(sK0)))))) % p104(sK2(sK3(sK6(sK7(sK9(sK0)))))) % p104(sK2(sK3(sK5(sK8(sK10(sK0)))))) % p104(sK2(sK3(sK5(sK8(sK9(sK0)))))) % p104(sK2(sK3(sK5(sK7(sK10(sK0)))))) % p104(sK2(sK3(sK5(sK7(sK9(sK0)))))) % p104(sK1(sK4(sK6(sK8(sK10(sK0)))))) % p104(sK1(sK4(sK6(sK8(sK9(sK0)))))) % p104(sK1(sK4(sK6(sK7(sK10(sK0)))))) % p104(sK1(sK4(sK6(sK7(sK9(sK0)))))) % p104(sK1(sK4(sK5(sK8(sK10(sK0)))))) % p104(sK1(sK4(sK5(sK8(sK9(sK0)))))) % p104(sK1(sK4(sK5(sK7(sK10(sK0)))))) % p104(sK1(sK4(sK5(sK7(sK9(sK0)))))) % p104(sK1(sK3(sK6(sK8(sK10(sK0)))))) % p104(sK1(sK3(sK6(sK8(sK9(sK0)))))) % p104(sK1(sK3(sK6(sK7(sK10(sK0)))))) % p104(sK1(sK3(sK6(sK7(sK9(sK0)))))) % p104(sK1(sK3(sK5(sK8(sK10(sK0)))))) % p104(sK1(sK3(sK5(sK8(sK9(sK0)))))) % p104(sK1(sK3(sK5(sK7(sK10(sK0)))))) % p104(sK1(sK3(sK5(sK7(sK9(sK0)))))) % p104(sK3(sK6(sK8(sK10(sK0))))) % p104(sK3(sK6(sK8(sK9(sK0))))) % p104(sK3(sK6(sK7(sK10(sK0))))) % p104(sK3(sK6(sK7(sK9(sK0))))) % p104(sK3(sK5(sK8(sK10(sK0))))) % p104(sK3(sK5(sK8(sK9(sK0))))) % p104(sK3(sK5(sK7(sK10(sK0))))) % p104(sK3(sK5(sK7(sK9(sK0))))) % p105(sK2(sK4(sK6(sK8(sK10(sK0)))))) % p105(sK2(sK4(sK6(sK8(sK9(sK0)))))) % p105(sK2(sK4(sK6(sK7(sK10(sK0)))))) % p105(sK2(sK4(sK6(sK7(sK9(sK0)))))) % p105(sK2(sK4(sK5(sK8(sK10(sK0)))))) % p105(sK2(sK4(sK5(sK8(sK9(sK0)))))) % p105(sK2(sK4(sK5(sK7(sK10(sK0)))))) % p105(sK2(sK4(sK5(sK7(sK9(sK0)))))) % p105(sK2(sK3(sK6(sK8(sK10(sK0)))))) % p105(sK2(sK3(sK6(sK8(sK9(sK0)))))) % p105(sK2(sK3(sK6(sK7(sK10(sK0)))))) % p105(sK2(sK3(sK6(sK7(sK9(sK0)))))) % p105(sK2(sK3(sK5(sK8(sK10(sK0)))))) % p105(sK2(sK3(sK5(sK8(sK9(sK0)))))) % p105(sK2(sK3(sK5(sK7(sK10(sK0)))))) % p105(sK2(sK3(sK5(sK7(sK9(sK0)))))) % p105(sK1(sK4(sK6(sK8(sK10(sK0)))))) % p105(sK1(sK4(sK6(sK8(sK9(sK0)))))) % p105(sK1(sK4(sK6(sK7(sK10(sK0)))))) % p105(sK1(sK4(sK6(sK7(sK9(sK0)))))) % p105(sK1(sK4(sK5(sK8(sK10(sK0)))))) % p105(sK1(sK4(sK5(sK8(sK9(sK0)))))) % p105(sK1(sK4(sK5(sK7(sK10(sK0)))))) % p105(sK1(sK4(sK5(sK7(sK9(sK0)))))) % p105(sK1(sK3(sK6(sK8(sK10(sK0)))))) % p105(sK1(sK3(sK6(sK8(sK9(sK0)))))) % p105(sK1(sK3(sK6(sK7(sK10(sK0)))))) % p105(sK1(sK3(sK6(sK7(sK9(sK0)))))) % p105(sK1(sK3(sK5(sK8(sK10(sK0)))))) % p105(sK1(sK3(sK5(sK8(sK9(sK0)))))) % p105(sK1(sK3(sK5(sK7(sK10(sK0)))))) % p105(sK1(sK3(sK5(sK7(sK9(sK0)))))) % p2(sK10(sK0)) % p2(sK8(sK10(sK0))) % p2(sK6(sK8(sK10(sK0)))) % p2(sK6(sK7(sK10(sK0)))) % p2(sK4(sK6(sK8(sK10(sK0))))) % p2(sK4(sK6(sK7(sK10(sK0))))) % p2(sK4(sK5(sK8(sK10(sK0))))) % p2(sK4(sK5(sK7(sK10(sK0))))) % p2(sK2(sK4(sK6(sK8(sK10(sK0)))))) % p2(sK2(sK4(sK6(sK7(sK10(sK0)))))) % p2(sK2(sK4(sK5(sK8(sK10(sK0)))))) % p2(sK2(sK4(sK5(sK7(sK10(sK0)))))) % p2(sK2(sK3(sK6(sK8(sK10(sK0)))))) % p2(sK2(sK3(sK6(sK7(sK10(sK0)))))) % p2(sK2(sK3(sK5(sK8(sK10(sK0)))))) % p2(sK2(sK3(sK5(sK7(sK10(sK0)))))) % p2(sK1(sK4(sK6(sK8(sK10(sK0)))))) % p2(sK1(sK4(sK6(sK7(sK10(sK0)))))) % p2(sK1(sK4(sK5(sK8(sK10(sK0)))))) % p2(sK1(sK4(sK5(sK7(sK10(sK0)))))) % p2(sK1(sK3(sK6(sK8(sK10(sK0)))))) % p2(sK1(sK3(sK6(sK7(sK10(sK0)))))) % p2(sK1(sK3(sK5(sK8(sK10(sK0)))))) % p2(sK1(sK3(sK5(sK7(sK10(sK0)))))) % p2(sK7(sK10(sK0))) % p2(sK5(sK8(sK10(sK0)))) % p2(sK5(sK7(sK10(sK0)))) % p2(sK3(sK6(sK8(sK10(sK0))))) % p2(sK3(sK6(sK7(sK10(sK0))))) % p2(sK3(sK5(sK8(sK10(sK0))))) % p2(sK3(sK5(sK7(sK10(sK0))))) % p3(sK8(sK10(sK0))) % p3(sK8(sK9(sK0))) % p3(sK6(sK8(sK10(sK0)))) % p3(sK6(sK8(sK9(sK0)))) % p3(sK4(sK6(sK8(sK10(sK0))))) % p3(sK4(sK6(sK8(sK9(sK0))))) % p3(sK4(sK5(sK8(sK10(sK0))))) % p3(sK4(sK5(sK8(sK9(sK0))))) % p3(sK2(sK4(sK6(sK8(sK10(sK0)))))) % p3(sK2(sK4(sK6(sK8(sK9(sK0)))))) % p3(sK2(sK4(sK5(sK8(sK10(sK0)))))) % p3(sK2(sK4(sK5(sK8(sK9(sK0)))))) % p3(sK2(sK3(sK6(sK8(sK10(sK0)))))) % p3(sK2(sK3(sK6(sK8(sK9(sK0)))))) % p3(sK2(sK3(sK5(sK8(sK10(sK0)))))) % p3(sK2(sK3(sK5(sK8(sK9(sK0)))))) % p3(sK1(sK4(sK6(sK8(sK10(sK0)))))) % p3(sK1(sK4(sK6(sK8(sK9(sK0)))))) % p3(sK1(sK4(sK5(sK8(sK10(sK0)))))) % p3(sK1(sK4(sK5(sK8(sK9(sK0)))))) % p3(sK1(sK3(sK6(sK8(sK10(sK0)))))) % p3(sK1(sK3(sK6(sK8(sK9(sK0)))))) % p3(sK1(sK3(sK5(sK8(sK10(sK0)))))) % p3(sK1(sK3(sK5(sK8(sK9(sK0)))))) % p3(sK5(sK8(sK10(sK0)))) % p3(sK5(sK8(sK9(sK0)))) % p3(sK3(sK6(sK8(sK10(sK0))))) % p3(sK3(sK6(sK8(sK9(sK0))))) % p3(sK3(sK5(sK8(sK10(sK0))))) % p3(sK3(sK5(sK8(sK9(sK0))))) % p4(sK6(sK8(sK10(sK0)))) % p4(sK6(sK8(sK9(sK0)))) % p4(sK6(sK7(sK10(sK0)))) % p4(sK6(sK7(sK9(sK0)))) % p4(sK4(sK6(sK8(sK10(sK0))))) % p4(sK4(sK6(sK8(sK9(sK0))))) % p4(sK4(sK6(sK7(sK10(sK0))))) % p4(sK4(sK6(sK7(sK9(sK0))))) % p4(sK2(sK4(sK6(sK8(sK10(sK0)))))) % p4(sK2(sK4(sK6(sK8(sK9(sK0)))))) % p4(sK2(sK4(sK6(sK7(sK10(sK0)))))) % p4(sK2(sK4(sK6(sK7(sK9(sK0)))))) % p4(sK2(sK3(sK6(sK8(sK10(sK0)))))) % p4(sK2(sK3(sK6(sK8(sK9(sK0)))))) % p4(sK2(sK3(sK6(sK7(sK10(sK0)))))) % p4(sK2(sK3(sK6(sK7(sK9(sK0)))))) % p4(sK1(sK4(sK6(sK8(sK10(sK0)))))) % p4(sK1(sK4(sK6(sK8(sK9(sK0)))))) % p4(sK1(sK4(sK6(sK7(sK10(sK0)))))) % p4(sK1(sK4(sK6(sK7(sK9(sK0)))))) % p4(sK1(sK3(sK6(sK8(sK10(sK0)))))) % p4(sK1(sK3(sK6(sK8(sK9(sK0)))))) % p4(sK1(sK3(sK6(sK7(sK10(sK0)))))) % p4(sK1(sK3(sK6(sK7(sK9(sK0)))))) % p4(sK3(sK6(sK8(sK10(sK0))))) % p4(sK3(sK6(sK8(sK9(sK0))))) % p4(sK3(sK6(sK7(sK10(sK0))))) % p4(sK3(sK6(sK7(sK9(sK0))))) % p5(sK4(sK6(sK8(sK10(sK0))))) % p5(sK4(sK6(sK8(sK9(sK0))))) % p5(sK4(sK6(sK7(sK10(sK0))))) % p5(sK4(sK6(sK7(sK9(sK0))))) % p5(sK4(sK5(sK8(sK10(sK0))))) % p5(sK4(sK5(sK8(sK9(sK0))))) % p5(sK4(sK5(sK7(sK10(sK0))))) % p5(sK4(sK5(sK7(sK9(sK0))))) % p5(sK2(sK4(sK6(sK8(sK10(sK0)))))) % p5(sK2(sK4(sK6(sK8(sK9(sK0)))))) % p5(sK2(sK4(sK6(sK7(sK10(sK0)))))) % p5(sK2(sK4(sK6(sK7(sK9(sK0)))))) % p5(sK2(sK4(sK5(sK8(sK10(sK0)))))) % p5(sK2(sK4(sK5(sK8(sK9(sK0)))))) % p5(sK2(sK4(sK5(sK7(sK10(sK0)))))) % p5(sK2(sK4(sK5(sK7(sK9(sK0)))))) % p5(sK1(sK4(sK6(sK8(sK10(sK0)))))) % p5(sK1(sK4(sK6(sK8(sK9(sK0)))))) % p5(sK1(sK4(sK6(sK7(sK10(sK0)))))) % p5(sK1(sK4(sK6(sK7(sK9(sK0)))))) % p5(sK1(sK4(sK5(sK8(sK10(sK0)))))) % p5(sK1(sK4(sK5(sK8(sK9(sK0)))))) % p5(sK1(sK4(sK5(sK7(sK10(sK0)))))) % p5(sK1(sK4(sK5(sK7(sK9(sK0)))))) % p6(sK2(sK4(sK6(sK8(sK10(sK0)))))) % p6(sK2(sK4(sK6(sK8(sK9(sK0)))))) % p6(sK2(sK4(sK6(sK7(sK10(sK0)))))) % p6(sK2(sK4(sK6(sK7(sK9(sK0)))))) % p6(sK2(sK4(sK5(sK8(sK10(sK0)))))) % p6(sK2(sK4(sK5(sK8(sK9(sK0)))))) % p6(sK2(sK4(sK5(sK7(sK10(sK0)))))) % p6(sK2(sK4(sK5(sK7(sK9(sK0)))))) % p6(sK2(sK3(sK6(sK8(sK10(sK0)))))) % p6(sK2(sK3(sK6(sK8(sK9(sK0)))))) % p6(sK2(sK3(sK6(sK7(sK10(sK0)))))) % p6(sK2(sK3(sK6(sK7(sK9(sK0)))))) % p6(sK2(sK3(sK5(sK8(sK10(sK0)))))) % p6(sK2(sK3(sK5(sK8(sK9(sK0)))))) % p6(sK2(sK3(sK5(sK7(sK10(sK0)))))) % p6(sK2(sK3(sK5(sK7(sK9(sK0)))))) % r1(_0, _0) % r1(sK10(sK0), sK8(sK10(sK0))) % r1(sK10(sK0), sK6(sK8(sK10(sK0)))) % r1(sK10(sK0), sK6(sK7(sK10(sK0)))) % r1(sK10(sK0), sK4(sK6(sK8(sK10(sK0))))) % r1(sK10(sK0), sK4(sK6(sK7(sK10(sK0))))) % r1(sK10(sK0), sK4(sK5(sK8(sK10(sK0))))) % r1(sK10(sK0), sK4(sK5(sK7(sK10(sK0))))) % r1(sK10(sK0), sK2(sK4(sK6(sK8(sK10(sK0)))))) % r1(sK10(sK0), sK2(sK4(sK6(sK7(sK10(sK0)))))) % r1(sK10(sK0), sK2(sK4(sK5(sK8(sK10(sK0)))))) % r1(sK10(sK0), sK2(sK4(sK5(sK7(sK10(sK0)))))) % r1(sK10(sK0), sK2(sK3(sK6(sK8(sK10(sK0)))))) % r1(sK10(sK0), sK2(sK3(sK6(sK7(sK10(sK0)))))) % r1(sK10(sK0), sK2(sK3(sK5(sK8(sK10(sK0)))))) % r1(sK10(sK0), sK2(sK3(sK5(sK7(sK10(sK0)))))) % r1(sK10(sK0), sK1(sK4(sK6(sK8(sK10(sK0)))))) % r1(sK10(sK0), sK1(sK4(sK6(sK7(sK10(sK0)))))) % r1(sK10(sK0), sK1(sK4(sK5(sK8(sK10(sK0)))))) % r1(sK10(sK0), sK1(sK4(sK5(sK7(sK10(sK0)))))) % r1(sK10(sK0), sK1(sK3(sK6(sK8(sK10(sK0)))))) % r1(sK10(sK0), sK1(sK3(sK6(sK7(sK10(sK0)))))) % r1(sK10(sK0), sK1(sK3(sK5(sK8(sK10(sK0)))))) % r1(sK10(sK0), sK1(sK3(sK5(sK7(sK10(sK0)))))) % r1(sK10(sK0), sK7(sK10(sK0))) % r1(sK10(sK0), sK5(sK8(sK10(sK0)))) % r1(sK10(sK0), sK5(sK7(sK10(sK0)))) % r1(sK10(sK0), sK3(sK6(sK8(sK10(sK0))))) % r1(sK10(sK0), sK3(sK6(sK7(sK10(sK0))))) % r1(sK10(sK0), sK3(sK5(sK8(sK10(sK0))))) % r1(sK10(sK0), sK3(sK5(sK7(sK10(sK0))))) % r1(sK8(sK10(sK0)), sK6(sK8(sK10(sK0)))) % r1(sK8(sK10(sK0)), sK4(sK6(sK8(sK10(sK0))))) % r1(sK8(sK10(sK0)), sK4(sK5(sK8(sK10(sK0))))) % r1(sK8(sK10(sK0)), sK2(sK4(sK6(sK8(sK10(sK0)))))) % r1(sK8(sK10(sK0)), sK2(sK4(sK5(sK8(sK10(sK0)))))) % r1(sK8(sK10(sK0)), sK2(sK3(sK6(sK8(sK10(sK0)))))) % r1(sK8(sK10(sK0)), sK2(sK3(sK5(sK8(sK10(sK0)))))) % r1(sK8(sK10(sK0)), sK1(sK4(sK6(sK8(sK10(sK0)))))) % r1(sK8(sK10(sK0)), sK1(sK4(sK5(sK8(sK10(sK0)))))) % r1(sK8(sK10(sK0)), sK1(sK3(sK6(sK8(sK10(sK0)))))) % r1(sK8(sK10(sK0)), sK1(sK3(sK5(sK8(sK10(sK0)))))) % r1(sK8(sK10(sK0)), sK5(sK8(sK10(sK0)))) % r1(sK8(sK10(sK0)), sK3(sK6(sK8(sK10(sK0))))) % r1(sK8(sK10(sK0)), sK3(sK5(sK8(sK10(sK0))))) % r1(sK8(sK9(sK0)), sK6(sK8(sK9(sK0)))) % r1(sK8(sK9(sK0)), sK4(sK6(sK8(sK9(sK0))))) % r1(sK8(sK9(sK0)), sK4(sK5(sK8(sK9(sK0))))) % r1(sK8(sK9(sK0)), sK2(sK4(sK6(sK8(sK9(sK0)))))) % r1(sK8(sK9(sK0)), sK2(sK4(sK5(sK8(sK9(sK0)))))) % r1(sK8(sK9(sK0)), sK2(sK3(sK6(sK8(sK9(sK0)))))) % r1(sK8(sK9(sK0)), sK2(sK3(sK5(sK8(sK9(sK0)))))) % r1(sK8(sK9(sK0)), sK1(sK4(sK6(sK8(sK9(sK0)))))) % r1(sK8(sK9(sK0)), sK1(sK4(sK5(sK8(sK9(sK0)))))) % r1(sK8(sK9(sK0)), sK1(sK3(sK6(sK8(sK9(sK0)))))) % r1(sK8(sK9(sK0)), sK1(sK3(sK5(sK8(sK9(sK0)))))) % r1(sK8(sK9(sK0)), sK5(sK8(sK9(sK0)))) % r1(sK8(sK9(sK0)), sK3(sK6(sK8(sK9(sK0))))) % r1(sK8(sK9(sK0)), sK3(sK5(sK8(sK9(sK0))))) % r1(sK6(sK8(sK10(sK0))), sK4(sK6(sK8(sK10(sK0))))) % r1(sK6(sK8(sK10(sK0))), sK2(sK4(sK6(sK8(sK10(sK0)))))) % r1(sK6(sK8(sK10(sK0))), sK2(sK3(sK6(sK8(sK10(sK0)))))) % r1(sK6(sK8(sK10(sK0))), sK1(sK4(sK6(sK8(sK10(sK0)))))) % r1(sK6(sK8(sK10(sK0))), sK1(sK3(sK6(sK8(sK10(sK0)))))) % r1(sK6(sK8(sK10(sK0))), sK3(sK6(sK8(sK10(sK0))))) % r1(sK6(sK8(sK9(sK0))), sK4(sK6(sK8(sK9(sK0))))) % r1(sK6(sK8(sK9(sK0))), sK2(sK4(sK6(sK8(sK9(sK0)))))) % r1(sK6(sK8(sK9(sK0))), sK2(sK3(sK6(sK8(sK9(sK0)))))) % r1(sK6(sK8(sK9(sK0))), sK1(sK4(sK6(sK8(sK9(sK0)))))) % r1(sK6(sK8(sK9(sK0))), sK1(sK3(sK6(sK8(sK9(sK0)))))) % r1(sK6(sK8(sK9(sK0))), sK3(sK6(sK8(sK9(sK0))))) % r1(sK6(sK7(sK10(sK0))), sK4(sK6(sK7(sK10(sK0))))) % r1(sK6(sK7(sK10(sK0))), sK2(sK4(sK6(sK7(sK10(sK0)))))) % r1(sK6(sK7(sK10(sK0))), sK2(sK3(sK6(sK7(sK10(sK0)))))) % r1(sK6(sK7(sK10(sK0))), sK1(sK4(sK6(sK7(sK10(sK0)))))) % r1(sK6(sK7(sK10(sK0))), sK1(sK3(sK6(sK7(sK10(sK0)))))) % r1(sK6(sK7(sK10(sK0))), sK3(sK6(sK7(sK10(sK0))))) % r1(sK6(sK7(sK9(sK0))), sK4(sK6(sK7(sK9(sK0))))) % r1(sK6(sK7(sK9(sK0))), sK2(sK4(sK6(sK7(sK9(sK0)))))) % r1(sK6(sK7(sK9(sK0))), sK2(sK3(sK6(sK7(sK9(sK0)))))) % r1(sK6(sK7(sK9(sK0))), sK1(sK4(sK6(sK7(sK9(sK0)))))) % r1(sK6(sK7(sK9(sK0))), sK1(sK3(sK6(sK7(sK9(sK0)))))) % r1(sK6(sK7(sK9(sK0))), sK3(sK6(sK7(sK9(sK0))))) % r1(sK4(sK6(sK8(sK10(sK0)))), sK2(sK4(sK6(sK8(sK10(sK0)))))) % r1(sK4(sK6(sK8(sK10(sK0)))), sK1(sK4(sK6(sK8(sK10(sK0)))))) % r1(sK4(sK6(sK8(sK9(sK0)))), sK2(sK4(sK6(sK8(sK9(sK0)))))) % r1(sK4(sK6(sK8(sK9(sK0)))), sK1(sK4(sK6(sK8(sK9(sK0)))))) % r1(sK4(sK6(sK7(sK10(sK0)))), sK2(sK4(sK6(sK7(sK10(sK0)))))) % r1(sK4(sK6(sK7(sK10(sK0)))), sK1(sK4(sK6(sK7(sK10(sK0)))))) % r1(sK4(sK6(sK7(sK9(sK0)))), sK2(sK4(sK6(sK7(sK9(sK0)))))) % r1(sK4(sK6(sK7(sK9(sK0)))), sK1(sK4(sK6(sK7(sK9(sK0)))))) % r1(sK4(sK5(sK8(sK10(sK0)))), sK2(sK4(sK5(sK8(sK10(sK0)))))) % r1(sK4(sK5(sK8(sK10(sK0)))), sK1(sK4(sK5(sK8(sK10(sK0)))))) % r1(sK4(sK5(sK8(sK9(sK0)))), sK2(sK4(sK5(sK8(sK9(sK0)))))) % r1(sK4(sK5(sK8(sK9(sK0)))), sK1(sK4(sK5(sK8(sK9(sK0)))))) % r1(sK4(sK5(sK7(sK10(sK0)))), sK2(sK4(sK5(sK7(sK10(sK0)))))) % r1(sK4(sK5(sK7(sK10(sK0)))), sK1(sK4(sK5(sK7(sK10(sK0)))))) % r1(sK4(sK5(sK7(sK9(sK0)))), sK2(sK4(sK5(sK7(sK9(sK0)))))) % r1(sK4(sK5(sK7(sK9(sK0)))), sK1(sK4(sK5(sK7(sK9(sK0)))))) % r1(sK9(sK0), sK8(sK9(sK0))) % r1(sK9(sK0), sK6(sK8(sK9(sK0)))) % r1(sK9(sK0), sK6(sK7(sK9(sK0)))) % r1(sK9(sK0), sK4(sK6(sK8(sK9(sK0))))) % r1(sK9(sK0), sK4(sK6(sK7(sK9(sK0))))) % r1(sK9(sK0), sK4(sK5(sK8(sK9(sK0))))) % r1(sK9(sK0), sK4(sK5(sK7(sK9(sK0))))) % r1(sK9(sK0), sK2(sK4(sK6(sK8(sK9(sK0)))))) % r1(sK9(sK0), sK2(sK4(sK6(sK7(sK9(sK0)))))) % r1(sK9(sK0), sK2(sK4(sK5(sK8(sK9(sK0)))))) % r1(sK9(sK0), sK2(sK4(sK5(sK7(sK9(sK0)))))) % r1(sK9(sK0), sK2(sK3(sK6(sK8(sK9(sK0)))))) % r1(sK9(sK0), sK2(sK3(sK6(sK7(sK9(sK0)))))) % r1(sK9(sK0), sK2(sK3(sK5(sK8(sK9(sK0)))))) % r1(sK9(sK0), sK2(sK3(sK5(sK7(sK9(sK0)))))) % r1(sK9(sK0), sK1(sK4(sK6(sK8(sK9(sK0)))))) % r1(sK9(sK0), sK1(sK4(sK6(sK7(sK9(sK0)))))) % r1(sK9(sK0), sK1(sK4(sK5(sK8(sK9(sK0)))))) % r1(sK9(sK0), sK1(sK4(sK5(sK7(sK9(sK0)))))) % r1(sK9(sK0), sK1(sK3(sK6(sK8(sK9(sK0)))))) % r1(sK9(sK0), sK1(sK3(sK6(sK7(sK9(sK0)))))) % r1(sK9(sK0), sK1(sK3(sK5(sK8(sK9(sK0)))))) % r1(sK9(sK0), sK1(sK3(sK5(sK7(sK9(sK0)))))) % r1(sK9(sK0), sK7(sK9(sK0))) % r1(sK9(sK0), sK5(sK8(sK9(sK0)))) % r1(sK9(sK0), sK5(sK7(sK9(sK0)))) % r1(sK9(sK0), sK3(sK6(sK8(sK9(sK0))))) % r1(sK9(sK0), sK3(sK6(sK7(sK9(sK0))))) % r1(sK9(sK0), sK3(sK5(sK8(sK9(sK0))))) % r1(sK9(sK0), sK3(sK5(sK7(sK9(sK0))))) % r1(sK7(sK10(sK0)), sK6(sK7(sK10(sK0)))) % r1(sK7(sK10(sK0)), sK4(sK6(sK7(sK10(sK0))))) % r1(sK7(sK10(sK0)), sK4(sK5(sK7(sK10(sK0))))) % r1(sK7(sK10(sK0)), sK2(sK4(sK6(sK7(sK10(sK0)))))) % r1(sK7(sK10(sK0)), sK2(sK4(sK5(sK7(sK10(sK0)))))) % r1(sK7(sK10(sK0)), sK2(sK3(sK6(sK7(sK10(sK0)))))) % r1(sK7(sK10(sK0)), sK2(sK3(sK5(sK7(sK10(sK0)))))) % r1(sK7(sK10(sK0)), sK1(sK4(sK6(sK7(sK10(sK0)))))) % r1(sK7(sK10(sK0)), sK1(sK4(sK5(sK7(sK10(sK0)))))) % r1(sK7(sK10(sK0)), sK1(sK3(sK6(sK7(sK10(sK0)))))) % r1(sK7(sK10(sK0)), sK1(sK3(sK5(sK7(sK10(sK0)))))) % r1(sK7(sK10(sK0)), sK5(sK7(sK10(sK0)))) % r1(sK7(sK10(sK0)), sK3(sK6(sK7(sK10(sK0))))) % r1(sK7(sK10(sK0)), sK3(sK5(sK7(sK10(sK0))))) % r1(sK7(sK9(sK0)), sK6(sK7(sK9(sK0)))) % r1(sK7(sK9(sK0)), sK4(sK6(sK7(sK9(sK0))))) % r1(sK7(sK9(sK0)), sK4(sK5(sK7(sK9(sK0))))) % r1(sK7(sK9(sK0)), sK2(sK4(sK6(sK7(sK9(sK0)))))) % r1(sK7(sK9(sK0)), sK2(sK4(sK5(sK7(sK9(sK0)))))) % r1(sK7(sK9(sK0)), sK2(sK3(sK6(sK7(sK9(sK0)))))) % r1(sK7(sK9(sK0)), sK2(sK3(sK5(sK7(sK9(sK0)))))) % r1(sK7(sK9(sK0)), sK1(sK4(sK6(sK7(sK9(sK0)))))) % r1(sK7(sK9(sK0)), sK1(sK4(sK5(sK7(sK9(sK0)))))) % r1(sK7(sK9(sK0)), sK1(sK3(sK6(sK7(sK9(sK0)))))) % r1(sK7(sK9(sK0)), sK1(sK3(sK5(sK7(sK9(sK0)))))) % r1(sK7(sK9(sK0)), sK5(sK7(sK9(sK0)))) % r1(sK7(sK9(sK0)), sK3(sK6(sK7(sK9(sK0))))) % r1(sK7(sK9(sK0)), sK3(sK5(sK7(sK9(sK0))))) % r1(sK5(sK8(sK10(sK0))), sK4(sK5(sK8(sK10(sK0))))) % r1(sK5(sK8(sK10(sK0))), sK2(sK4(sK5(sK8(sK10(sK0)))))) % r1(sK5(sK8(sK10(sK0))), sK2(sK3(sK5(sK8(sK10(sK0)))))) % r1(sK5(sK8(sK10(sK0))), sK1(sK4(sK5(sK8(sK10(sK0)))))) % r1(sK5(sK8(sK10(sK0))), sK1(sK3(sK5(sK8(sK10(sK0)))))) % r1(sK5(sK8(sK10(sK0))), sK3(sK5(sK8(sK10(sK0))))) % r1(sK5(sK8(sK9(sK0))), sK4(sK5(sK8(sK9(sK0))))) % r1(sK5(sK8(sK9(sK0))), sK2(sK4(sK5(sK8(sK9(sK0)))))) % r1(sK5(sK8(sK9(sK0))), sK2(sK3(sK5(sK8(sK9(sK0)))))) % r1(sK5(sK8(sK9(sK0))), sK1(sK4(sK5(sK8(sK9(sK0)))))) % r1(sK5(sK8(sK9(sK0))), sK1(sK3(sK5(sK8(sK9(sK0)))))) % r1(sK5(sK8(sK9(sK0))), sK3(sK5(sK8(sK9(sK0))))) % r1(sK5(sK7(sK10(sK0))), sK4(sK5(sK7(sK10(sK0))))) % r1(sK5(sK7(sK10(sK0))), sK2(sK4(sK5(sK7(sK10(sK0)))))) % r1(sK5(sK7(sK10(sK0))), sK2(sK3(sK5(sK7(sK10(sK0)))))) % r1(sK5(sK7(sK10(sK0))), sK1(sK4(sK5(sK7(sK10(sK0)))))) % r1(sK5(sK7(sK10(sK0))), sK1(sK3(sK5(sK7(sK10(sK0)))))) % r1(sK5(sK7(sK10(sK0))), sK3(sK5(sK7(sK10(sK0))))) % r1(sK5(sK7(sK9(sK0))), sK4(sK5(sK7(sK9(sK0))))) % r1(sK5(sK7(sK9(sK0))), sK2(sK4(sK5(sK7(sK9(sK0)))))) % r1(sK5(sK7(sK9(sK0))), sK2(sK3(sK5(sK7(sK9(sK0)))))) % r1(sK5(sK7(sK9(sK0))), sK1(sK4(sK5(sK7(sK9(sK0)))))) % r1(sK5(sK7(sK9(sK0))), sK1(sK3(sK5(sK7(sK9(sK0)))))) % r1(sK5(sK7(sK9(sK0))), sK3(sK5(sK7(sK9(sK0))))) % r1(sK3(sK6(sK8(sK10(sK0)))), sK2(sK3(sK6(sK8(sK10(sK0)))))) % r1(sK3(sK6(sK8(sK10(sK0)))), sK1(sK3(sK6(sK8(sK10(sK0)))))) % r1(sK3(sK6(sK8(sK9(sK0)))), sK2(sK3(sK6(sK8(sK9(sK0)))))) % r1(sK3(sK6(sK8(sK9(sK0)))), sK1(sK3(sK6(sK8(sK9(sK0)))))) % r1(sK3(sK6(sK7(sK10(sK0)))), sK2(sK3(sK6(sK7(sK10(sK0)))))) % r1(sK3(sK6(sK7(sK10(sK0)))), sK1(sK3(sK6(sK7(sK10(sK0)))))) % r1(sK3(sK6(sK7(sK9(sK0)))), sK2(sK3(sK6(sK7(sK9(sK0)))))) % r1(sK3(sK6(sK7(sK9(sK0)))), sK1(sK3(sK6(sK7(sK9(sK0)))))) % r1(sK3(sK5(sK8(sK10(sK0)))), sK2(sK3(sK5(sK8(sK10(sK0)))))) % r1(sK3(sK5(sK8(sK10(sK0)))), sK1(sK3(sK5(sK8(sK10(sK0)))))) % r1(sK3(sK5(sK8(sK9(sK0)))), sK2(sK3(sK5(sK8(sK9(sK0)))))) % r1(sK3(sK5(sK8(sK9(sK0)))), sK1(sK3(sK5(sK8(sK9(sK0)))))) % r1(sK3(sK5(sK7(sK10(sK0)))), sK2(sK3(sK5(sK7(sK10(sK0)))))) % r1(sK3(sK5(sK7(sK10(sK0)))), sK1(sK3(sK5(sK7(sK10(sK0)))))) % r1(sK3(sK5(sK7(sK9(sK0)))), sK2(sK3(sK5(sK7(sK9(sK0)))))) % r1(sK3(sK5(sK7(sK9(sK0)))), sK1(sK3(sK5(sK7(sK9(sK0)))))) % r1(sK0, sK10(sK0)) % r1(sK0, sK8(sK10(sK0))) % r1(sK0, sK8(sK9(sK0))) % r1(sK0, sK6(sK8(sK10(sK0)))) % r1(sK0, sK6(sK8(sK9(sK0)))) % r1(sK0, sK6(sK7(sK10(sK0)))) % r1(sK0, sK6(sK7(sK9(sK0)))) % r1(sK0, sK4(sK6(sK8(sK10(sK0))))) % r1(sK0, sK4(sK6(sK8(sK9(sK0))))) % r1(sK0, sK4(sK6(sK7(sK10(sK0))))) % r1(sK0, sK4(sK6(sK7(sK9(sK0))))) % r1(sK0, sK4(sK5(sK8(sK10(sK0))))) % r1(sK0, sK4(sK5(sK8(sK9(sK0))))) % r1(sK0, sK4(sK5(sK7(sK10(sK0))))) % r1(sK0, sK4(sK5(sK7(sK9(sK0))))) % r1(sK0, sK2(sK4(sK6(sK8(sK10(sK0)))))) % r1(sK0, sK2(sK4(sK6(sK8(sK9(sK0)))))) % r1(sK0, sK2(sK4(sK6(sK7(sK10(sK0)))))) % r1(sK0, sK2(sK4(sK6(sK7(sK9(sK0)))))) % r1(sK0, sK2(sK4(sK5(sK8(sK10(sK0)))))) % r1(sK0, sK2(sK4(sK5(sK8(sK9(sK0)))))) % r1(sK0, sK2(sK4(sK5(sK7(sK10(sK0)))))) % r1(sK0, sK2(sK4(sK5(sK7(sK9(sK0)))))) % r1(sK0, sK2(sK3(sK6(sK8(sK10(sK0)))))) % r1(sK0, sK2(sK3(sK6(sK8(sK9(sK0)))))) % r1(sK0, sK2(sK3(sK6(sK7(sK10(sK0)))))) % r1(sK0, sK2(sK3(sK6(sK7(sK9(sK0)))))) % r1(sK0, sK2(sK3(sK5(sK8(sK10(sK0)))))) % r1(sK0, sK2(sK3(sK5(sK8(sK9(sK0)))))) % r1(sK0, sK2(sK3(sK5(sK7(sK10(sK0)))))) % r1(sK0, sK2(sK3(sK5(sK7(sK9(sK0)))))) % r1(sK0, sK1(sK4(sK6(sK8(sK10(sK0)))))) % r1(sK0, sK1(sK4(sK6(sK8(sK9(sK0)))))) % r1(sK0, sK1(sK4(sK6(sK7(sK10(sK0)))))) % r1(sK0, sK1(sK4(sK6(sK7(sK9(sK0)))))) % r1(sK0, sK1(sK4(sK5(sK8(sK10(sK0)))))) % r1(sK0, sK1(sK4(sK5(sK8(sK9(sK0)))))) % r1(sK0, sK1(sK4(sK5(sK7(sK10(sK0)))))) % r1(sK0, sK1(sK4(sK5(sK7(sK9(sK0)))))) % r1(sK0, sK1(sK3(sK6(sK8(sK10(sK0)))))) % r1(sK0, sK1(sK3(sK6(sK8(sK9(sK0)))))) % r1(sK0, sK1(sK3(sK6(sK7(sK10(sK0)))))) % r1(sK0, sK1(sK3(sK6(sK7(sK9(sK0)))))) % r1(sK0, sK1(sK3(sK5(sK8(sK10(sK0)))))) % r1(sK0, sK1(sK3(sK5(sK8(sK9(sK0)))))) % r1(sK0, sK1(sK3(sK5(sK7(sK10(sK0)))))) % r1(sK0, sK1(sK3(sK5(sK7(sK9(sK0)))))) % r1(sK0, sK9(sK0)) % r1(sK0, sK7(sK10(sK0))) % r1(sK0, sK7(sK9(sK0))) % r1(sK0, sK5(sK8(sK10(sK0)))) % r1(sK0, sK5(sK8(sK9(sK0)))) % r1(sK0, sK5(sK7(sK10(sK0)))) % r1(sK0, sK5(sK7(sK9(sK0)))) % r1(sK0, sK3(sK6(sK8(sK10(sK0))))) % r1(sK0, sK3(sK6(sK8(sK9(sK0))))) % r1(sK0, sK3(sK6(sK7(sK10(sK0))))) % r1(sK0, sK3(sK6(sK7(sK9(sK0))))) % r1(sK0, sK3(sK5(sK8(sK10(sK0))))) % r1(sK0, sK3(sK5(sK8(sK9(sK0))))) % r1(sK0, sK3(sK5(sK7(sK10(sK0))))) % r1(sK0, sK3(sK5(sK7(sK9(sK0))))) % END OF MODEL % EOF %------------------------------------------------------------------------------