%------------------------------------------------------------------------------ % File : E-Darwin---1.5 % Problem : NLP033-1 : TPTP v6.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : e-darwin -pev TPTP -pmd true -if tptp -pl 2 -pc false -ps false %s % Computer : n026.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:06:10 EDT 2014 % Result : Satisfiable 279.45s % Output : Model 279.45s % Verified : % SZS Type : None (Parsing solution fails) % Syntax : Number of formulae : 0 % Comments : %------------------------------------------------------------------------------ %----ERROR: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % % Problem : NLP033-1 : TPTP v6.1.0. Released v2.4.0. % % Command : e-darwin -pev TPTP -pmd true -if tptp -pl 2 -pc false -ps false %s % % Computer : n026.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 : Fri Jul 25 17:27:46 CDT 2014 % % CPUTime : 279.45 % 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): % actual_world(skc5) % actual_world(skc52) % agent(skc5, skf13(skc5, skf19(skc5, _0, skf17(skc5, _1, skf26(skc5, skf22(skc5, skf15(_2, skc5, _3, _4))))), _5, _6), skf19(skc5, _0, skf17(skc5, _1, skf26(skc5, skf22(skc5, skf15(_2, skc5, _3, _4)))))) % agent(skc5, skf13(skc5, skf19(skc5, _0, skf17(skc5, _1, skf26(skc5, skf17(skc5, _2, skf19(skc5, _3, _4))))), _5, _6), skf19(skc5, _0, skf17(skc5, _1, skf26(skc5, skf17(skc5, _2, skf19(skc5, _3, _4)))))) % agent(skc5, skf13(skc5, skf19(skc5, _0, skf17(skc5, _1, skf26(skc5, skf17(skc5, _2, skf15(_3, skc5, _4, _5))))), _6, _7), skf19(skc5, _0, skf17(skc5, _1, skf26(skc5, skf17(skc5, _2, skf15(_3, skc5, _4, _5)))))) % agent(skc5, skf13(skc5, skf26(skc5, skf17(skc5, _0, skf26(skc5, skf22(skc5, skf15(_1, skc5, _2, _3))))), _4, _5), skf26(skc5, skf17(skc5, _0, skf26(skc5, skf22(skc5, skf15(_1, skc5, _2, _3)))))) % agent(skc5, skf13(skc5, skf26(skc5, skf17(skc5, _0, skf26(skc5, skf17(skc5, _1, skf19(skc5, _2, _3))))), _4, _5), skf26(skc5, skf17(skc5, _0, skf26(skc5, skf17(skc5, _1, skf19(skc5, _2, _3)))))) % agent(skc5, skf13(skc5, skf26(skc5, skf17(skc5, _0, skf26(skc5, skf17(skc5, _1, skf15(_2, skc5, _3, _4))))), _5, _6), skf26(skc5, skf17(skc5, _0, skf26(skc5, skf17(skc5, _1, skf15(_2, skc5, _3, _4)))))) % agent(skc5, skf13(skc5, skf26(skc5, skf17(skc5, _0, skf15(skf22(skc5, skf15(_1, skc5, _2, _3)), skc5, _4, _5))), _6, _7), skf26(skc5, skf17(skc5, _0, skf15(skf22(skc5, skf15(_1, skc5, _2, _3)), skc5, _4, _5)))) % agent(skc5, skf13(skc5, skf26(skc5, skf17(skc5, _0, skf15(skf17(skc5, _1, skf19(skc5, _2, _3)), skc5, _4, _5))), _6, _7), skf26(skc5, skf17(skc5, _0, skf15(skf17(skc5, _1, skf19(skc5, _2, _3)), skc5, _4, _5)))) % agent(skc5, skf13(skc5, skf26(skc5, skf17(skc5, _0, skf15(skf17(skc5, _1, skf15(_2, skc5, _3, _4)), skc5, _5, _6))), _7, _8), skf26(skc5, skf17(skc5, _0, skf15(skf17(skc5, _1, skf15(_2, skc5, _3, _4)), skc5, _5, _6)))) % agent(skc5, skf13(skc5, skf15(skf17(skc5, _0, skf26(skc5, skf22(skc5, skf15(_1, skc5, _2, _3)))), skc5, _4, _5), _6, _7), skf15(skf17(skc5, _0, skf26(skc5, skf22(skc5, skf15(_1, skc5, _2, _3)))), skc5, _4, _5)) % agent(skc5, skf13(skc5, skf15(skf17(skc5, _0, skf26(skc5, skf17(skc5, _1, skf19(skc5, _2, _3)))), skc5, _4, _5), _6, _7), skf15(skf17(skc5, _0, skf26(skc5, skf17(skc5, _1, skf19(skc5, _2, _3)))), skc5, _4, _5)) % agent(skc5, skf13(skc5, skf15(skf17(skc5, _0, skf26(skc5, skf17(skc5, _1, skf15(_2, skc5, _3, _4)))), skc5, _5, _6), _7, _8), skf15(skf17(skc5, _0, skf26(skc5, skf17(skc5, _1, skf15(_2, skc5, _3, _4)))), skc5, _5, _6)) % agent(skc5, skf13(skc5, skf15(skf17(skc5, _0, skf15(skf22(skc5, skf15(_1, skc5, _2, _3)), skc5, _4, _5)), skc5, _6, _7), _8, _9), skf15(skf17(skc5, _0, skf15(skf22(skc5, skf15(_1, skc5, _2, _3)), skc5, _4, _5)), skc5, _6, _7)) % agent(skc5, skf13(skc5, skf15(skf17(skc5, _0, skf15(skf17(skc5, _1, skf19(skc5, _2, _3)), skc5, _4, _5)), skc5, _6, _7), _8, _9), skf15(skf17(skc5, _0, skf15(skf17(skc5, _1, skf19(skc5, _2, _3)), skc5, _4, _5)), skc5, _6, _7)) % agent(skc5, skf13(skc5, skf15(skf17(skc5, _0, skf15(skf17(skc5, _1, skf15(_2, skc5, _3, _4)), skc5, _5, _6)), skc5, _7, _8), _9, _10), skf15(skf17(skc5, _0, skf15(skf17(skc5, _1, skf15(_2, skc5, _3, _4)), skc5, _5, _6)), skc5, _7, _8)) % agent(skc52, skf13(skc52, skf19(skc52, _0, skf17(skc52, _1, skf26(skc52, skf22(skc52, skf15(_2, skc52, _3, _4))))), _5, _6), skf19(skc52, _0, skf17(skc52, _1, skf26(skc52, skf22(skc52, skf15(_2, skc52, _3, _4)))))) % agent(skc52, skf13(skc52, skf19(skc52, _0, skf17(skc52, _1, skf26(skc52, skf17(skc52, _2, skf19(skc52, _3, _4))))), _5, _6), skf19(skc52, _0, skf17(skc52, _1, skf26(skc52, skf17(skc52, _2, skf19(skc52, _3, _4)))))) % agent(skc52, skf13(skc52, skf19(skc52, _0, skf17(skc52, _1, skf26(skc52, skf17(skc52, _2, skf15(_3, skc52, _4, _5))))), _6, _7), skf19(skc52, _0, skf17(skc52, _1, skf26(skc52, skf17(skc52, _2, skf15(_3, skc52, _4, _5)))))) % agent(skc52, skf13(skc52, skf26(skc52, skf17(skc52, _0, skf26(skc52, skf22(skc52, skf15(_1, skc52, _2, _3))))), _4, _5), skf26(skc52, skf17(skc52, _0, skf26(skc52, skf22(skc52, skf15(_1, skc52, _2, _3)))))) % agent(skc52, skf13(skc52, skf26(skc52, skf17(skc52, _0, skf26(skc52, skf17(skc52, _1, skf19(skc52, _2, _3))))), _4, _5), skf26(skc52, skf17(skc52, _0, skf26(skc52, skf17(skc52, _1, skf19(skc52, _2, _3)))))) % agent(skc52, skf13(skc52, skf26(skc52, skf17(skc52, _0, skf26(skc52, skf17(skc52, _1, skf15(_2, skc52, _3, _4))))), _5, _6), skf26(skc52, skf17(skc52, _0, skf26(skc52, skf17(skc52, _1, skf15(_2, skc52, _3, _4)))))) % agent(skc52, skf13(skc52, skf26(skc52, skf17(skc52, _0, skf15(skf22(skc52, skf15(_1, skc52, _2, _3)), skc52, _4, _5))), _6, _7), skf26(skc52, skf17(skc52, _0, skf15(skf22(skc52, skf15(_1, skc52, _2, _3)), skc52, _4, _5)))) % agent(skc52, skf13(skc52, skf26(skc52, skf17(skc52, _0, skf15(skf17(skc52, _1, skf19(skc52, _2, _3)), skc52, _4, _5))), _6, _7), skf26(skc52, skf17(skc52, _0, skf15(skf17(skc52, _1, skf19(skc52, _2, _3)), skc52, _4, _5)))) % agent(skc52, skf13(skc52, skf26(skc52, skf17(skc52, _0, skf15(skf17(skc52, _1, skf15(_2, skc52, _3, _4)), skc52, _5, _6))), _7, _8), skf26(skc52, skf17(skc52, _0, skf15(skf17(skc52, _1, skf15(_2, skc52, _3, _4)), skc52, _5, _6)))) % agent(skc52, skf13(skc52, skf15(skf17(skc52, _0, skf26(skc52, skf22(skc52, skf15(_1, skc52, _2, _3)))), skc52, _4, _5), _6, _7), skf15(skf17(skc52, _0, skf26(skc52, skf22(skc52, skf15(_1, skc52, _2, _3)))), skc52, _4, _5)) % agent(skc52, skf13(skc52, skf15(skf17(skc52, _0, skf26(skc52, skf17(skc52, _1, skf19(skc52, _2, _3)))), skc52, _4, _5), _6, _7), skf15(skf17(skc52, _0, skf26(skc52, skf17(skc52, _1, skf19(skc52, _2, _3)))), skc52, _4, _5)) % agent(skc52, skf13(skc52, skf15(skf17(skc52, _0, skf26(skc52, skf17(skc52, _1, skf15(_2, skc52, _3, _4)))), skc52, _5, _6), _7, _8), skf15(skf17(skc52, _0, skf26(skc52, skf17(skc52, _1, skf15(_2, skc52, _3, _4)))), skc52, _5, _6)) % agent(skc52, skf13(skc52, skf15(skf17(skc52, _0, skf15(skf22(skc52, skf15(_1, skc52, _2, _3)), skc52, _4, _5)), skc52, _6, _7), _8, _9), skf15(skf17(skc52, _0, skf15(skf22(skc52, skf15(_1, skc52, _2, _3)), skc52, _4, _5)), skc52, _6, _7)) % agent(skc52, skf13(skc52, skf15(skf17(skc52, _0, skf15(skf17(skc52, _1, skf19(skc52, _2, _3)), skc52, _4, _5)), skc52, _6, _7), _8, _9), skf15(skf17(skc52, _0, skf15(skf17(skc52, _1, skf19(skc52, _2, _3)), skc52, _4, _5)), skc52, _6, _7)) % agent(skc52, skf13(skc52, skf15(skf17(skc52, _0, skf15(skf17(skc52, _1, skf15(_2, skc52, _3, _4)), skc52, _5, _6)), skc52, _7, _8), _9, _10), skf15(skf17(skc52, _0, skf15(skf17(skc52, _1, skf15(_2, skc52, _3, _4)), skc52, _5, _6)), skc52, _7, _8)) % at(skc5, skf13(skc5, skf19(skc5, _0, skf17(skc5, _1, skf26(skc5, skf22(skc5, skf15(_2, skc5, _3, _4))))), skf26(skc5, skf22(skc5, skf15(_2, skc5, _3, _4))), _1), _1) % at(skc5, skf13(skc5, skf19(skc5, _0, skf17(skc5, _1, skf26(skc5, skf17(skc5, _2, skf19(skc5, _3, _4))))), skf26(skc5, skf17(skc5, _2, skf19(skc5, _3, _4))), _1), _1) % at(skc5, skf13(skc5, skf19(skc5, _0, skf17(skc5, _1, skf26(skc5, skf17(skc5, _2, skf15(_3, skc5, _4, _5))))), skf26(skc5, skf17(skc5, _2, skf15(_3, skc5, _4, _5))), _1), _1) % at(skc5, skf13(skc5, skf26(skc5, skf17(skc5, _0, skf26(skc5, skf22(skc5, skf15(_1, skc5, _2, _3))))), skf26(skc5, skf22(skc5, skf15(_1, skc5, _2, _3))), _0), _0) % at(skc5, skf13(skc5, skf26(skc5, skf17(skc5, _0, skf26(skc5, skf17(skc5, _1, skf19(skc5, _2, _3))))), skf26(skc5, skf17(skc5, _1, skf19(skc5, _2, _3))), _0), _0) % at(skc5, skf13(skc5, skf26(skc5, skf17(skc5, _0, skf26(skc5, skf17(skc5, _1, skf15(_2, skc5, _3, _4))))), skf26(skc5, skf17(skc5, _1, skf15(_2, skc5, _3, _4))), _0), _0) % at(skc5, skf13(skc5, skf26(skc5, skf17(skc5, _0, skf15(skf22(skc5, skf15(_1, skc5, _2, _3)), skc5, _4, _5))), skf15(skf22(skc5, skf15(_1, skc5, _2, _3)), skc5, _4, _5), _0), _0) % at(skc5, skf13(skc5, skf26(skc5, skf17(skc5, _0, skf15(skf17(skc5, _1, skf19(skc5, _2, _3)), skc5, _4, _5))), skf15(skf17(skc5, _1, skf19(skc5, _2, _3)), skc5, _4, _5), _0), _0) % at(skc5, skf13(skc5, skf26(skc5, skf17(skc5, _0, skf15(skf17(skc5, _1, skf15(_2, skc5, _3, _4)), skc5, _5, _6))), skf15(skf17(skc5, _1, skf15(_2, skc5, _3, _4)), skc5, _5, _6), _0), _0) % at(skc5, skf13(skc5, skf15(skf17(skc5, _0, skf26(skc5, skf22(skc5, skf15(_1, skc5, _2, _3)))), skc5, _4, _5), skf26(skc5, skf22(skc5, skf15(_1, skc5, _2, _3))), _0), _0) % at(skc5, skf13(skc5, skf15(skf17(skc5, _0, skf26(skc5, skf17(skc5, _1, skf19(skc5, _2, _3)))), skc5, _4, _5), skf26(skc5, skf17(skc5, _1, skf19(skc5, _2, _3))), _0), _0) % at(skc5, skf13(skc5, skf15(skf17(skc5, _0, skf26(skc5, skf17(skc5, _1, skf15(_2, skc5, _3, _4)))), skc5, _5, _6), skf26(skc5, skf17(skc5, _1, skf15(_2, skc5, _3, _4))), _0), _0) % at(skc5, skf13(skc5, skf15(skf17(skc5, _0, skf15(skf22(skc5, skf15(_1, skc5, _2, _3)), skc5, _4, _5)), skc5, _6, _7), skf15(skf22(skc5, skf15(_1, skc5, _2, _3)), skc5, _4, _5), _0), _0) % at(skc5, skf13(skc5, skf15(skf17(skc5, _0, skf15(skf17(skc5, _1, skf19(skc5, _2, _3)), skc5, _4, _5)), skc5, _6, _7), skf15(skf17(skc5, _1, skf19(skc5, _2, _3)), skc5, _4, _5), _0), _0) % at(skc5, skf13(skc5, skf15(skf17(skc5, _0, skf15(skf17(skc5, _1, skf15(_2, skc5, _3, _4)), skc5, _5, _6)), skc5, _7, _8), skf15(skf17(skc5, _1, skf15(_2, skc5, _3, _4)), skc5, _5, _6), _0), _0) % at(skc52, skf13(skc52, skf19(skc52, _0, skf17(skc52, _1, skf26(skc52, skf22(skc52, skf15(_2, skc52, _3, _4))))), skf26(skc52, skf22(skc52, skf15(_2, skc52, _3, _4))), _1), _1) % at(skc52, skf13(skc52, skf19(skc52, _0, skf17(skc52, _1, skf26(skc52, skf17(skc52, _2, skf19(skc52, _3, _4))))), skf26(skc52, skf17(skc52, _2, skf19(skc52, _3, _4))), _1), _1) % at(skc52, skf13(skc52, skf19(skc52, _0, skf17(skc52, _1, skf26(skc52, skf17(skc52, _2, skf15(_3, skc52, _4, _5))))), skf26(skc52, skf17(skc52, _2, skf15(_3, skc52, _4, _5))), _1), _1) % at(skc52, skf13(skc52, skf26(skc52, skf17(skc52, _0, skf26(skc52, skf22(skc52, skf15(_1, skc52, _2, _3))))), skf26(skc52, skf22(skc52, skf15(_1, skc52, _2, _3))), _0), _0) % at(skc52, skf13(skc52, skf26(skc52, skf17(skc52, _0, skf26(skc52, skf17(skc52, _1, skf19(skc52, _2, _3))))), skf26(skc52, skf17(skc52, _1, skf19(skc52, _2, _3))), _0), _0) % at(skc52, skf13(skc52, skf26(skc52, skf17(skc52, _0, skf26(skc52, skf17(skc52, _1, skf15(_2, skc52, _3, _4))))), skf26(skc52, skf17(skc52, _1, skf15(_2, skc52, _3, _4))), _0), _0) % at(skc52, skf13(skc52, skf26(skc52, skf17(skc52, _0, skf15(skf22(skc52, skf15(_1, skc52, _2, _3)), skc52, _4, _5))), skf15(skf22(skc52, skf15(_1, skc52, _2, _3)), skc52, _4, _5), _0), _0) % at(skc52, skf13(skc52, skf26(skc52, skf17(skc52, _0, skf15(skf17(skc52, _1, skf19(skc52, _2, _3)), skc52, _4, _5))), skf15(skf17(skc52, _1, skf19(skc52, _2, _3)), skc52, _4, _5), _0), _0) % at(skc52, skf13(skc52, skf26(skc52, skf17(skc52, _0, skf15(skf17(skc52, _1, skf15(_2, skc52, _3, _4)), skc52, _5, _6))), skf15(skf17(skc52, _1, skf15(_2, skc52, _3, _4)), skc52, _5, _6), _0), _0) % at(skc52, skf13(skc52, skf15(skf17(skc52, _0, skf26(skc52, skf22(skc52, skf15(_1, skc52, _2, _3)))), skc52, _4, _5), skf26(skc52, skf22(skc52, skf15(_1, skc52, _2, _3))), _0), _0) % at(skc52, skf13(skc52, skf15(skf17(skc52, _0, skf26(skc52, skf17(skc52, _1, skf19(skc52, _2, _3)))), skc52, _4, _5), skf26(skc52, skf17(skc52, _1, skf19(skc52, _2, _3))), _0), _0) % at(skc52, skf13(skc52, skf15(skf17(skc52, _0, skf26(skc52, skf17(skc52, _1, skf15(_2, skc52, _3, _4)))), skc52, _5, _6), skf26(skc52, skf17(skc52, _1, skf15(_2, skc52, _3, _4))), _0), _0) % at(skc52, skf13(skc52, skf15(skf17(skc52, _0, skf15(skf22(skc52, skf15(_1, skc52, _2, _3)), skc52, _4, _5)), skc52, _6, _7), skf15(skf22(skc52, skf15(_1, skc52, _2, _3)), skc52, _4, _5), _0), _0) % at(skc52, skf13(skc52, skf15(skf17(skc52, _0, skf15(skf17(skc52, _1, skf19(skc52, _2, _3)), skc52, _4, _5)), skc52, _6, _7), skf15(skf17(skc52, _1, skf19(skc52, _2, _3)), skc52, _4, _5), _0), _0) % at(skc52, skf13(skc52, skf15(skf17(skc52, _0, skf15(skf17(skc52, _1, skf15(_2, skc52, _3, _4)), skc52, _5, _6)), skc52, _7, _8), skf15(skf17(skc52, _1, skf15(_2, skc52, _3, _4)), skc52, _5, _6), _0), _0) % event(_0, skf13(_0, _1, _2, _3)) % group(_0, skf22(_0, _1)) -- exceptions: % group(skc52, skf22(skc52, skf19(skc52, _0, _1))) % group(skc52, skf22(skc52, skf15(_0, skc52, _1, _2))) % group(skc5, skf22(skc5, skf15(_0, skc5, _1, _2))) % group(_0, skf17(_0, _1, _2)) % group(skc52, skc53) % guy(skc5, skf26(skc5, skf17(skc5, _0, _1))) % guy(_0, skf19(_0, _1, skf22(_0, _2))) % guy(_0, skf19(_0, _1, skf17(_0, _2, _3))) % guy(_0, skf15(skf22(_0, _1), _0, _2, _3)) % guy(_0, skf15(skf17(_0, _1, _2), _0, _3, _4)) % guy(skc52, skf26(skc52, skf17(skc52, _0, _1))) % member(skc5, skf19(skc5, _0, skf22(skc5, skf19(skc5, _1, _2))), skf22(skc5, skf19(skc5, _1, _2))) % member(skc5, skf26(skc5, _0), _0) % member(skc5, skf15(skf22(skc5, skf19(skc5, _0, _1)), skc5, _2, _3), skf22(skc5, skf19(skc5, _0, _1))) % member(skc5, skf15(skf22(skc5, skf15(_0, skc5, _1, _2)), skc5, _3, _4), skf22(skc5, skf15(_0, skc5, _1, _2))) % member(skc5, skf15(skf17(skc5, _0, skf19(skc5, _1, _2)), skc5, _3, _4), skf17(skc5, _0, skf19(skc5, _1, _2))) % member(skc5, skf15(skf17(skc5, _0, skf15(_1, skc5, _2, _3)), skc5, _4, _5), skf17(skc5, _0, skf15(_1, skc5, _2, _3))) % member(_0, skf19(_0, _1, _2), _2) -- exceptions: % member(_0, skf19(_0, _1, skf22(_0, skf19(_0, _2, _3))), skf22(_0, skf19(_0, _2, _3))) % member(_0, skf19(_0, _1, skf22(_0, skf15(_2, _0, _3, _4))), skf22(_0, skf15(_2, _0, _3, _4))) % member(_0, skf19(_0, _1, skf17(_0, _2, skf19(_0, _3, _4))), skf17(_0, _2, skf19(_0, _3, _4))) % member(_0, skf19(_0, _1, skf17(_0, _2, skf15(_3, _0, _4, _5))), skf17(_0, _2, skf15(_3, _0, _4, _5))) % member(skc52, skf19(skc52, _0, skc53), skc53) % member(_0, skf15(_1, _0, _2, _3), _1) -- exceptions: % member(_0, skf15(skf22(_0, skf19(_0, _1, _2)), _0, _3, _4), skf22(_0, skf19(_0, _1, _2))) % member(_0, skf15(skf22(_0, skf15(_1, _0, _2, _3)), _0, _4, _5), skf22(_0, skf15(_1, _0, _2, _3))) % member(_0, skf15(skf17(_0, _1, skf19(_0, _2, _3)), _0, _4, _5), skf17(_0, _1, skf19(_0, _2, _3))) % member(_0, skf15(skf17(_0, _1, skf15(_2, _0, _3, _4)), _0, _5, _6), skf17(_0, _1, skf15(_2, _0, _3, _4))) % member(skc52, skf15(skc53, skc52, _0, _1), skc53) % member(skc52, skf19(skc52, _0, skf22(skc52, skf19(skc52, _1, _2))), skf22(skc52, skf19(skc52, _1, _2))) % member(skc52, skf26(skc52, _0), _0) -- exceptions: % member(skc52, skf26(skc52, skc53), skc53) % member(skc52, skf15(skf22(skc52, skf19(skc52, _0, _1)), skc52, _2, _3), skf22(skc52, skf19(skc52, _0, _1))) % member(skc52, skf15(skf22(skc52, skf15(_0, skc52, _1, _2)), skc52, _3, _4), skf22(skc52, skf15(_0, skc52, _1, _2))) % member(skc52, skf15(skf17(skc52, _0, skf19(skc52, _1, _2)), skc52, _3, _4), skf17(skc52, _0, skf19(skc52, _1, _2))) % member(skc52, skf15(skf17(skc52, _0, skf15(_1, skc52, _2, _3)), skc52, _4, _5), skf17(skc52, _0, skf15(_1, skc52, _2, _3))) % present(_0, skf13(_0, _1, _2, _3)) % sit(_0, skf13(_0, _1, _2, _3)) % ssSkP0(_0, _1, skc53, skc52) % ssSkP0(skf19(_0, _1, _2), _3, skf17(_0, _3, skf19(_0, _1, _2)), _0) -- exceptions: % ssSkP0(skf19(skc52, _0, _1), _2, skf17(skc52, _2, skf19(skc52, _0, _1)), skc52) % ssSkP0(skf19(skc5, _0, _1), _2, skf17(skc5, _2, skf19(skc5, _0, _1)), skc5) % ssSkP0(skf19(_0, _1, _2), skf23(_0, skf19(_0, _1, _2)), skf22(_0, skf19(_0, _1, _2)), _0) -- exceptions: % ssSkP0(skf19(skc52, _0, _1), skf23(skc52, skf19(skc52, _0, _1)), skf22(skc52, skf19(skc52, _0, _1)), skc52) % ssSkP0(skf19(skc5, _0, _1), skf23(skc5, skf19(skc5, _0, _1)), skf22(skc5, skf19(skc5, _0, _1)), skc5) % ssSkP0(_0, _1, skf22(_2, skf19(_2, _3, _4)), _2) -- exceptions: % ssSkP0(_0, _1, skf22(skc52, skf19(skc52, _2, _3)), skc52) % ssSkP0(_0, _1, skf22(skc5, skf19(skc5, _2, _3)), skc5) % ssSkP0(_0, _1, skf22(_2, skf15(_3, _2, _4, _5)), _2) -- exceptions: % ssSkP0(_0, _1, skf22(skc52, skf15(_2, skc52, _3, _4)), skc52) % ssSkP0(_0, _1, skf22(skc5, skf15(_2, skc5, _3, _4)), skc5) % ssSkP0(_0, _1, skf17(_2, _3, skf19(_2, _4, _5)), _2) -- exceptions: % ssSkP0(_0, _1, skf17(skc52, _2, skf19(skc52, _3, _4)), skc52) % ssSkP0(_0, _1, skf17(skc5, _2, skf19(skc5, _3, _4)), skc5) % ssSkP0(_0, _1, skf17(_2, _3, skf15(_4, _2, _5, _6)), _2) -- exceptions: % ssSkP0(_0, _1, skf17(skc52, _2, skf15(_3, skc52, _4, _5)), skc52) % ssSkP0(_0, _1, skf17(skc5, _2, skf15(_3, skc5, _4, _5)), skc5) % ssSkP0(skf15(skf22(skc5, skf15(_0, skc5, _1, _2)), skc5, _3, _4), _5, skf17(skc5, _5, skf15(skf22(skc5, skf15(_0, skc5, _1, _2)), skc5, _3, _4)), skc5) % ssSkP0(skf15(skf22(skc52, skf15(_0, skc52, _1, _2)), skc52, _3, _4), _5, skf17(skc52, _5, skf15(skf22(skc52, skf15(_0, skc52, _1, _2)), skc52, _3, _4)), skc52) % ssSkP0(skf15(_0, _1, _2, _3), _4, skf17(_1, _4, skf15(_0, _1, _2, _3)), _1) -- exceptions: % ssSkP0(skf15(_0, skc52, _1, _2), _3, skf17(skc52, _3, skf15(_0, skc52, _1, _2)), skc52) % ssSkP0(skf15(_0, skc5, _1, _2), _3, skf17(skc5, _3, skf15(_0, skc5, _1, _2)), skc5) % ssSkP0(skf15(_0, _1, _2, _3), skf23(_1, skf15(_0, _1, _2, _3)), skf22(_1, skf15(_0, _1, _2, _3)), _1) -- exceptions: % ssSkP0(skf15(_0, skc52, _1, _2), skf23(skc52, skf15(_0, skc52, _1, _2)), skf22(skc52, skf15(_0, skc52, _1, _2)), skc52) % ssSkP0(skf15(_0, skc5, _1, _2), skf23(skc5, skf15(_0, skc5, _1, _2)), skf22(skc5, skf15(_0, skc5, _1, _2)), skc5) % ssSkP0(skf15(skf17(skc5, _0, skf19(skc5, _1, _2)), skc5, _3, _4), _5, skf17(skc5, _5, skf15(skf17(skc5, _0, skf19(skc5, _1, _2)), skc5, _3, _4)), skc5) % ssSkP0(skf15(skf17(skc5, _0, skf15(_1, skc5, _2, _3)), skc5, _4, _5), _6, skf17(skc5, _6, skf15(skf17(skc5, _0, skf15(_1, skc5, _2, _3)), skc5, _4, _5)), skc5) % ssSkP0(skf15(skf17(skc52, _0, skf19(skc52, _1, _2)), skc52, _3, _4), _5, skf17(skc52, _5, skf15(skf17(skc52, _0, skf19(skc52, _1, _2)), skc52, _3, _4)), skc52) % ssSkP0(skf15(skf17(skc52, _0, skf15(_1, skc52, _2, _3)), skc52, _4, _5), _6, skf17(skc52, _6, skf15(skf17(skc52, _0, skf15(_1, skc52, _2, _3)), skc52, _4, _5)), skc52) % ssSkP0(skf26(skc5, skf22(skc5, skf15(_0, skc5, _1, _2))), _3, skf17(skc5, _3, skf26(skc5, skf22(skc5, skf15(_0, skc5, _1, _2)))), skc5) % ssSkP0(skf26(skc5, skf17(skc5, _0, skf19(skc5, _1, _2))), _3, skf17(skc5, _3, skf26(skc5, skf17(skc5, _0, skf19(skc5, _1, _2)))), skc5) % ssSkP0(skf26(skc5, skf17(skc5, _0, skf15(_1, skc5, _2, _3))), _4, skf17(skc5, _4, skf26(skc5, skf17(skc5, _0, skf15(_1, skc5, _2, _3)))), skc5) % ssSkP0(skf26(skc52, skf22(skc52, skf15(_0, skc52, _1, _2))), _3, skf17(skc52, _3, skf26(skc52, skf22(skc52, skf15(_0, skc52, _1, _2)))), skc52) % ssSkP0(skf26(skc52, skf17(skc52, _0, skf19(skc52, _1, _2))), _3, skf17(skc52, _3, skf26(skc52, skf17(skc52, _0, skf19(skc52, _1, _2)))), skc52) % ssSkP0(skf26(skc52, skf17(skc52, _0, skf15(_1, skc52, _2, _3))), _4, skf17(skc52, _4, skf26(skc52, skf17(skc52, _0, skf15(_1, skc52, _2, _3)))), skc52) % ssSkP1(_0, skc53, skc52) % ssSkP1(_0, skf22(skc5, skf15(_1, skc5, _2, _3)), skc5) % ssSkP1(_0, skf22(_1, skf19(_1, _2, _3)), _1) -- exceptions: % ssSkP1(_0, skf22(skc52, skf19(skc52, _1, _2)), skc52) % ssSkP1(_0, skf22(skc5, skf19(skc5, _1, _2)), skc5) % ssSkP1(_0, skf22(skc52, skf15(_1, skc52, _2, _3)), skc52) % ssSkP1(_0, _1, _2) -- exceptions: % ssSkP1(_0, _1, skc52) % ssSkP1(_0, _1, skc5) % ssSkP1(_0, skf17(skc5, _1, skf19(skc5, _2, _3)), skc5) % ssSkP1(_0, skf17(skc5, _1, skf15(_2, skc5, _3, _4)), skc5) % ssSkP1(_0, skf17(skc52, _1, skf19(skc52, _2, _3)), skc52) % ssSkP1(_0, skf17(skc52, _1, skf15(_2, skc52, _3, _4)), skc52) % ssSkP2(_0, _1) -- exceptions: % ssSkP2(_0, skc52) % ssSkP2(_0, skc5) % ssSkP2(skc53, skc52) % table(_0, skf23(_0, _1)) -- exceptions: % table(skc52, skf23(skc52, _0)) % table(skc5, skf23(skc5, _0)) % three(_0, skf22(_0, _1)) -- exceptions: % three(skc5, skf22(skc5, skf19(skc5, _0, _1))) % three(_0, skf17(_0, _1, _2)) % with(skc5, skf13(skc5, skf19(skc5, _0, skf17(skc5, _1, skf26(skc5, skf22(skc5, skf15(_2, skc5, _3, _4))))), skf26(skc5, skf22(skc5, skf15(_2, skc5, _3, _4))), _5), skf26(skc5, skf22(skc5, skf15(_2, skc5, _3, _4)))) % with(skc5, skf13(skc5, skf19(skc5, _0, skf17(skc5, _1, skf26(skc5, skf17(skc5, _2, skf19(skc5, _3, _4))))), skf26(skc5, skf17(skc5, _2, skf19(skc5, _3, _4))), _5), skf26(skc5, skf17(skc5, _2, skf19(skc5, _3, _4)))) % with(skc5, skf13(skc5, skf19(skc5, _0, skf17(skc5, _1, skf26(skc5, skf17(skc5, _2, skf15(_3, skc5, _4, _5))))), skf26(skc5, skf17(skc5, _2, skf15(_3, skc5, _4, _5))), _6), skf26(skc5, skf17(skc5, _2, skf15(_3, skc5, _4, _5)))) % with(skc5, skf13(skc5, skf26(skc5, skf17(skc5, _0, skf26(skc5, skf22(skc5, skf15(_1, skc5, _2, _3))))), skf26(skc5, skf22(skc5, skf15(_1, skc5, _2, _3))), _4), skf26(skc5, skf22(skc5, skf15(_1, skc5, _2, _3)))) % with(skc5, skf13(skc5, skf26(skc5, skf17(skc5, _0, skf26(skc5, skf17(skc5, _1, skf19(skc5, _2, _3))))), skf26(skc5, skf17(skc5, _1, skf19(skc5, _2, _3))), _4), skf26(skc5, skf17(skc5, _1, skf19(skc5, _2, _3)))) % with(skc5, skf13(skc5, skf26(skc5, skf17(skc5, _0, skf26(skc5, skf17(skc5, _1, skf15(_2, skc5, _3, _4))))), skf26(skc5, skf17(skc5, _1, skf15(_2, skc5, _3, _4))), _5), skf26(skc5, skf17(skc5, _1, skf15(_2, skc5, _3, _4)))) % with(skc5, skf13(skc5, skf26(skc5, skf17(skc5, _0, skf15(skf22(skc5, skf15(_1, skc5, _2, _3)), skc5, _4, _5))), skf15(skf22(skc5, skf15(_1, skc5, _2, _3)), skc5, _4, _5), _6), skf15(skf22(skc5, skf15(_1, skc5, _2, _3)), skc5, _4, _5)) % with(skc5, skf13(skc5, skf26(skc5, skf17(skc5, _0, skf15(skf17(skc5, _1, skf19(skc5, _2, _3)), skc5, _4, _5))), skf15(skf17(skc5, _1, skf19(skc5, _2, _3)), skc5, _4, _5), _6), skf15(skf17(skc5, _1, skf19(skc5, _2, _3)), skc5, _4, _5)) % with(skc5, skf13(skc5, skf26(skc5, skf17(skc5, _0, skf15(skf17(skc5, _1, skf15(_2, skc5, _3, _4)), skc5, _5, _6))), skf15(skf17(skc5, _1, skf15(_2, skc5, _3, _4)), skc5, _5, _6), _7), skf15(skf17(skc5, _1, skf15(_2, skc5, _3, _4)), skc5, _5, _6)) % with(skc5, skf13(skc5, skf15(skf17(skc5, _0, skf26(skc5, skf22(skc5, skf15(_1, skc5, _2, _3)))), skc5, _4, _5), skf26(skc5, skf22(skc5, skf15(_1, skc5, _2, _3))), _6), skf26(skc5, skf22(skc5, skf15(_1, skc5, _2, _3)))) % with(skc5, skf13(skc5, skf15(skf17(skc5, _0, skf26(skc5, skf17(skc5, _1, skf19(skc5, _2, _3)))), skc5, _4, _5), skf26(skc5, skf17(skc5, _1, skf19(skc5, _2, _3))), _6), skf26(skc5, skf17(skc5, _1, skf19(skc5, _2, _3)))) % with(skc5, skf13(skc5, skf15(skf17(skc5, _0, skf26(skc5, skf17(skc5, _1, skf15(_2, skc5, _3, _4)))), skc5, _5, _6), skf26(skc5, skf17(skc5, _1, skf15(_2, skc5, _3, _4))), _7), skf26(skc5, skf17(skc5, _1, skf15(_2, skc5, _3, _4)))) % with(skc5, skf13(skc5, skf15(skf17(skc5, _0, skf15(skf22(skc5, skf15(_1, skc5, _2, _3)), skc5, _4, _5)), skc5, _6, _7), skf15(skf22(skc5, skf15(_1, skc5, _2, _3)), skc5, _4, _5), _8), skf15(skf22(skc5, skf15(_1, skc5, _2, _3)), skc5, _4, _5)) % with(skc5, skf13(skc5, skf15(skf17(skc5, _0, skf15(skf17(skc5, _1, skf19(skc5, _2, _3)), skc5, _4, _5)), skc5, _6, _7), skf15(skf17(skc5, _1, skf19(skc5, _2, _3)), skc5, _4, _5), _8), skf15(skf17(skc5, _1, skf19(skc5, _2, _3)), skc5, _4, _5)) % with(skc5, skf13(skc5, skf15(skf17(skc5, _0, skf15(skf17(skc5, _1, skf15(_2, skc5, _3, _4)), skc5, _5, _6)), skc5, _7, _8), skf15(skf17(skc5, _1, skf15(_2, skc5, _3, _4)), skc5, _5, _6), _9), skf15(skf17(skc5, _1, skf15(_2, skc5, _3, _4)), skc5, _5, _6)) % with(skc52, skf13(skc52, skf19(skc52, _0, skf17(skc52, _1, skf26(skc52, skf22(skc52, skf15(_2, skc52, _3, _4))))), skf26(skc52, skf22(skc52, skf15(_2, skc52, _3, _4))), _5), skf26(skc52, skf22(skc52, skf15(_2, skc52, _3, _4)))) % with(skc52, skf13(skc52, skf19(skc52, _0, skf17(skc52, _1, skf26(skc52, skf17(skc52, _2, skf19(skc52, _3, _4))))), skf26(skc52, skf17(skc52, _2, skf19(skc52, _3, _4))), _5), skf26(skc52, skf17(skc52, _2, skf19(skc52, _3, _4)))) % with(skc52, skf13(skc52, skf19(skc52, _0, skf17(skc52, _1, skf26(skc52, skf17(skc52, _2, skf15(_3, skc52, _4, _5))))), skf26(skc52, skf17(skc52, _2, skf15(_3, skc52, _4, _5))), _6), skf26(skc52, skf17(skc52, _2, skf15(_3, skc52, _4, _5)))) % with(skc52, skf13(skc52, skf26(skc52, skf17(skc52, _0, skf26(skc52, skf22(skc52, skf15(_1, skc52, _2, _3))))), skf26(skc52, skf22(skc52, skf15(_1, skc52, _2, _3))), _4), skf26(skc52, skf22(skc52, skf15(_1, skc52, _2, _3)))) % with(skc52, skf13(skc52, skf26(skc52, skf17(skc52, _0, skf26(skc52, skf17(skc52, _1, skf19(skc52, _2, _3))))), skf26(skc52, skf17(skc52, _1, skf19(skc52, _2, _3))), _4), skf26(skc52, skf17(skc52, _1, skf19(skc52, _2, _3)))) % with(skc52, skf13(skc52, skf26(skc52, skf17(skc52, _0, skf26(skc52, skf17(skc52, _1, skf15(_2, skc52, _3, _4))))), skf26(skc52, skf17(skc52, _1, skf15(_2, skc52, _3, _4))), _5), skf26(skc52, skf17(skc52, _1, skf15(_2, skc52, _3, _4)))) % with(skc52, skf13(skc52, skf26(skc52, skf17(skc52, _0, skf15(skf22(skc52, skf15(_1, skc52, _2, _3)), skc52, _4, _5))), skf15(skf22(skc52, skf15(_1, skc52, _2, _3)), skc52, _4, _5), _6), skf15(skf22(skc52, skf15(_1, skc52, _2, _3)), skc52, _4, _5)) % with(skc52, skf13(skc52, skf26(skc52, skf17(skc52, _0, skf15(skf17(skc52, _1, skf19(skc52, _2, _3)), skc52, _4, _5))), skf15(skf17(skc52, _1, skf19(skc52, _2, _3)), skc52, _4, _5), _6), skf15(skf17(skc52, _1, skf19(skc52, _2, _3)), skc52, _4, _5)) % with(skc52, skf13(skc52, skf26(skc52, skf17(skc52, _0, skf15(skf17(skc52, _1, skf15(_2, skc52, _3, _4)), skc52, _5, _6))), skf15(skf17(skc52, _1, skf15(_2, skc52, _3, _4)), skc52, _5, _6), _7), skf15(skf17(skc52, _1, skf15(_2, skc52, _3, _4)), skc52, _5, _6)) % with(skc52, skf13(skc52, skf15(skf17(skc52, _0, skf26(skc52, skf22(skc52, skf15(_1, skc52, _2, _3)))), skc52, _4, _5), skf26(skc52, skf22(skc52, skf15(_1, skc52, _2, _3))), _6), skf26(skc52, skf22(skc52, skf15(_1, skc52, _2, _3)))) % with(skc52, skf13(skc52, skf15(skf17(skc52, _0, skf26(skc52, skf17(skc52, _1, skf19(skc52, _2, _3)))), skc52, _4, _5), skf26(skc52, skf17(skc52, _1, skf19(skc52, _2, _3))), _6), skf26(skc52, skf17(skc52, _1, skf19(skc52, _2, _3)))) % with(skc52, skf13(skc52, skf15(skf17(skc52, _0, skf26(skc52, skf17(skc52, _1, skf15(_2, skc52, _3, _4)))), skc52, _5, _6), skf26(skc52, skf17(skc52, _1, skf15(_2, skc52, _3, _4))), _7), skf26(skc52, skf17(skc52, _1, skf15(_2, skc52, _3, _4)))) % with(skc52, skf13(skc52, skf15(skf17(skc52, _0, skf15(skf22(skc52, skf15(_1, skc52, _2, _3)), skc52, _4, _5)), skc52, _6, _7), skf15(skf22(skc52, skf15(_1, skc52, _2, _3)), skc52, _4, _5), _8), skf15(skf22(skc52, skf15(_1, skc52, _2, _3)), skc52, _4, _5)) % with(skc52, skf13(skc52, skf15(skf17(skc52, _0, skf15(skf17(skc52, _1, skf19(skc52, _2, _3)), skc52, _4, _5)), skc52, _6, _7), skf15(skf17(skc52, _1, skf19(skc52, _2, _3)), skc52, _4, _5), _8), skf15(skf17(skc52, _1, skf19(skc52, _2, _3)), skc52, _4, _5)) % with(skc52, skf13(skc52, skf15(skf17(skc52, _0, skf15(skf17(skc52, _1, skf15(_2, skc52, _3, _4)), skc52, _5, _6)), skc52, _7, _8), skf15(skf17(skc52, _1, skf15(_2, skc52, _3, _4)), skc52, _5, _6), _9), skf15(skf17(skc52, _1, skf15(_2, skc52, _3, _4)), skc52, _5, _6)) % young(skc5, skf26(skc5, skf17(skc5, _0, _1))) % young(_0, skf19(_0, _1, skf22(_0, _2))) % young(_0, skf19(_0, _1, skf17(_0, _2, _3))) % young(_0, skf15(skf22(_0, _1), _0, _2, _3)) % young(_0, skf15(skf17(_0, _1, _2), _0, _3, _4)) % young(skc52, skf26(skc52, skf17(skc52, _0, _1))) % END OF MODEL % EOF %------------------------------------------------------------------------------