%------------------------------------------------------------------------------ % File : Darwin---1.4.5 % Problem : NLP049-1 : TPTP v8.1.0. Released v2.4.0. % Transfm : none % Format : tptp:raw % Command : darwin -pl 0 -pmc true -to %d %s % Computer : n007.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 0s % DateTime : Mon Jul 18 01:35:59 EDT 2022 % Result : Satisfiable 54.76s 55.02s % Output : Model 54.76s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.07 % Problem : NLP049-1 : TPTP v8.1.0. Released v2.4.0. % 0.02/0.07 % Command : darwin -pl 0 -pmc true -to %d %s % 0.06/0.26 % Computer : n007.cluster.edu % 0.06/0.26 % Model : x86_64 x86_64 % 0.06/0.26 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.06/0.26 % Memory : 8042.1875MB % 0.06/0.26 % OS : Linux 3.10.0-693.el7.x86_64 % 0.06/0.26 % CPULimit : 300 % 0.06/0.26 % DateTime : Thu Jun 30 23:03:23 EDT 2022 % 0.10/0.26 % CPUTime : % 0.10/0.26 Defaulting to tptp format. % 54.76/55.02 SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 54.76/55.02 % 54.76/55.02 MODEL (CONTEXT): % 54.76/55.02 SZS output start Model for /export/starexec/sandbox2/benchmark/theBenchmark.p % 54.76/55.02 -__-v__(=0) % 54.76/55.02 +(_0 = _0) % 54.76/55.02 -(skc14 = skc12) % 54.76/55.02 -(skc14 = skc9) % 54.76/55.02 -(skc14 = skc8) % 54.76/55.02 -(skc14 = skc11) % 54.76/55.02 -(skc14 = skc13) % 54.76/55.02 -(skc14 = skf17(skc8, skc7)) % 54.76/55.02 -(skc14 = skf15(skc8, skc7)) % 54.76/55.02 -(skc14 = skf13(skc8, skc7)) % 54.76/55.02 -(skc14 = skf11(skc8, skc7)) % 54.76/55.02 -(skc14 = skf9(skc8, skc7)) % 54.76/55.02 -(skc14 = skf7(_0)) % 54.76/55.02 -(skc12 = skc14) % 54.76/55.02 -(skc12 = skc8) % 54.76/55.02 -(skc12 = skc11) % 54.76/55.02 -(skc12 = skc13) % 54.76/55.02 -(skc12 = skf17(skc8, skc7)) % 54.76/55.02 -(skc12 = skf15(skc8, skc7)) % 54.76/55.02 -(skc12 = skf13(skc8, skc7)) % 54.76/55.02 -(skc12 = skf11(skc8, skc7)) % 54.76/55.02 -(skc12 = skf9(skc8, skc7)) % 54.76/55.02 -(skc12 = skf7(_0)) % 54.76/55.02 -(skc9 = skc14) % 54.76/55.02 -(skc9 = skf17(skc8, skc7)) % 54.76/55.02 -(skc9 = skf15(skc8, skc7)) % 54.76/55.02 -(skc9 = skf13(skc8, skc7)) % 54.76/55.02 -(skc9 = skf11(skc8, skc7)) % 54.76/55.02 -(skc9 = skf9(skc8, skc7)) % 54.76/55.02 -(skc8 = skc14) % 54.76/55.02 -(skc8 = skc12) % 54.76/55.02 -(skc8 = skc11) % 54.76/55.02 -(skc8 = skc13) % 54.76/55.02 -(skc8 = skf17(skc8, skc7)) % 54.76/55.02 -(skc8 = skf15(skc8, skc7)) % 54.76/55.02 -(skc8 = skf13(skc8, skc7)) % 54.76/55.02 -(skc8 = skf11(skc8, skc7)) % 54.76/55.02 -(skc8 = skf9(skc8, skc7)) % 54.76/55.02 -(skc8 = skf7(_0)) % 54.76/55.02 -(skc11 = skc14) % 54.76/55.02 -(skc11 = skc12) % 54.76/55.02 -(skc11 = skc8) % 54.76/55.02 -(skc11 = skc13) % 54.76/55.02 -(skc11 = skf17(skc8, skc7)) % 54.76/55.02 -(skc11 = skf15(skc8, skc7)) % 54.76/55.02 -(skc11 = skf13(skc8, skc7)) % 54.76/55.02 -(skc11 = skf11(skc8, skc7)) % 54.76/55.02 -(skc11 = skf9(skc8, skc7)) % 54.76/55.02 -(skc11 = skf7(_0)) % 54.76/55.02 -(skc13 = skc14) % 54.76/55.02 -(skc13 = skc12) % 54.76/55.02 -(skc13 = skc8) % 54.76/55.02 -(skc13 = skc11) % 54.76/55.02 -(skc13 = skf7(_0)) % 54.76/55.02 -(skf17(skc8, skc7) = skc14) % 54.76/55.02 -(skf17(skc8, skc7) = skc12) % 54.76/55.02 -(skf17(skc8, skc7) = skc9) % 54.76/55.02 -(skf17(skc8, skc7) = skc8) % 54.76/55.02 -(skf17(skc8, skc7) = skc11) % 54.76/55.02 -(skf17(skc8, skc7) = skf15(skc8, skc7)) % 54.76/55.02 -(skf17(skc8, skc7) = skf13(skc8, skc7)) % 54.76/55.02 -(skf17(skc8, skc7) = skf11(skc8, skc7)) % 54.76/55.02 -(skf17(skc8, skc7) = skf9(skc8, skc7)) % 54.76/55.02 -(skf17(skc8, skc7) = skf7(_0)) % 54.76/55.02 -(skf15(skc8, skc7) = skc14) % 54.76/55.02 -(skf15(skc8, skc7) = skc12) % 54.76/55.02 -(skf15(skc8, skc7) = skc9) % 54.76/55.02 -(skf15(skc8, skc7) = skc8) % 54.76/55.02 -(skf15(skc8, skc7) = skc11) % 54.76/55.02 -(skf15(skc8, skc7) = skf17(skc8, skc7)) % 54.76/55.02 -(skf15(skc8, skc7) = skf13(skc8, skc7)) % 54.76/55.02 -(skf15(skc8, skc7) = skf11(skc8, skc7)) % 54.76/55.02 -(skf15(skc8, skc7) = skf9(skc8, skc7)) % 54.76/55.02 -(skf15(skc8, skc7) = skf7(_0)) % 54.76/55.02 -(skf13(skc8, skc7) = skc14) % 54.76/55.02 -(skf13(skc8, skc7) = skc12) % 54.76/55.02 -(skf13(skc8, skc7) = skc9) % 54.76/55.02 -(skf13(skc8, skc7) = skc8) % 54.76/55.02 -(skf13(skc8, skc7) = skc11) % 54.76/55.02 -(skf13(skc8, skc7) = skf17(skc8, skc7)) % 54.76/55.02 -(skf13(skc8, skc7) = skf15(skc8, skc7)) % 54.76/55.02 -(skf13(skc8, skc7) = skf11(skc8, skc7)) % 54.76/55.02 -(skf13(skc8, skc7) = skf9(skc8, skc7)) % 54.76/55.02 -(skf13(skc8, skc7) = skf7(_0)) % 54.76/55.02 -(skf11(skc8, skc7) = skc14) % 54.76/55.02 -(skf11(skc8, skc7) = skc12) % 54.76/55.02 -(skf11(skc8, skc7) = skc9) % 54.76/55.02 -(skf11(skc8, skc7) = skc8) % 54.76/55.02 -(skf11(skc8, skc7) = skc11) % 54.76/55.02 -(skf11(skc8, skc7) = skf17(skc8, skc7)) % 54.76/55.02 -(skf11(skc8, skc7) = skf15(skc8, skc7)) % 54.76/55.02 -(skf11(skc8, skc7) = skf13(skc8, skc7)) % 54.76/55.02 -(skf11(skc8, skc7) = skf9(skc8, skc7)) % 54.76/55.02 -(skf11(skc8, skc7) = skf7(_0)) % 54.76/55.02 -(skf9(skc8, skc7) = skc14) % 54.76/55.02 -(skf9(skc8, skc7) = skc12) % 54.76/55.02 -(skf9(skc8, skc7) = skc9) % 54.76/55.02 -(skf9(skc8, skc7) = skc8) % 54.76/55.02 -(skf9(skc8, skc7) = skc11) % 54.76/55.02 -(skf9(skc8, skc7) = skf17(skc8, skc7)) % 54.76/55.02 -(skf9(skc8, skc7) = skf15(skc8, skc7)) % 54.76/55.02 -(skf9(skc8, skc7) = skf13(skc8, skc7)) % 54.76/55.02 -(skf9(skc8, skc7) = skf11(skc8, skc7)) % 54.76/55.02 -(skf9(skc8, skc7) = skf7(_0)) % 54.76/55.02 -(skf7(_0) = skc14) % 54.76/55.02 -(skf7(_0) = skc12) % 54.76/55.02 -(skf7(_0) = skc8) % 54.76/55.02 -(skf7(_0) = skc11) % 54.76/55.02 -(skf7(_0) = skc13) % 54.76/55.02 -(skf7(_0) = skf17(skc8, skc7)) % 54.76/55.02 -(skf7(_0) = skf15(skc8, skc7)) % 54.76/55.02 -(skf7(_0) = skf13(skc8, skc7)) % 54.76/55.02 -(skf7(_0) = skf11(skc8, skc7)) % 54.76/55.02 -(skf7(_0) = skf9(skc8, skc7)) % 54.76/55.02 +__con75 % 54.76/55.02 +__con76 % 54.76/55.02 +__con77 % 54.76/55.02 +__con78 % 54.76/55.02 +__con79 % 54.76/55.02 +__con80 % 54.76/55.02 +abstraction(skc7, skc13) % 54.76/55.02 +abstraction(skc7, skf17(skc8, skc7)) % 54.76/55.02 +abstraction(skc7, skf15(skc8, skc7)) % 54.76/55.02 +abstraction(skc7, skf13(skc8, skc7)) % 54.76/55.02 +abstraction(skc7, skf11(skc8, skc7)) % 54.76/55.02 +abstraction(skc7, skf9(skc8, skc7)) % 54.76/55.02 -abstraction(skc7, skc14) % 54.76/55.02 -abstraction(skc7, skc12) % 54.76/55.02 -abstraction(skc7, skc8) % 54.76/55.02 -abstraction(skc7, skc11) % 54.76/55.02 -abstraction(skc7, skf7(_0)) % 54.76/55.02 +act(skc7, skc11) % 54.76/55.02 -act(skc7, skc14) % 54.76/55.02 -act(skc7, skc12) % 54.76/55.02 -act(skc7, skc8) % 54.76/55.02 -act(skc7, skc13) % 54.76/55.02 -act(skc7, skf17(skc8, skc7)) % 54.76/55.02 -act(skc7, skf15(skc8, skc7)) % 54.76/55.02 -act(skc7, skf13(skc8, skc7)) % 54.76/55.02 -act(skc7, skf11(skc8, skc7)) % 54.76/55.02 -act(skc7, skf9(skc8, skc7)) % 54.76/55.02 +actual_world(skc7) % 54.76/55.02 +agent(skc7, skc11, skc14) % 54.76/55.02 +agent(skc7, skf7(_0), skc9) % 54.76/55.02 -agent(skc7, skc11, skc12) % 54.76/55.02 -agent(skc7, skf7(skf17(skc8, skc7)), skf17(skc8, skc7)) % 54.76/55.02 -agent(skc7, skf7(skf15(skc8, skc7)), skf15(skc8, skc7)) % 54.76/55.02 -agent(skc7, skf7(skf13(skc8, skc7)), skf13(skc8, skc7)) % 54.76/55.02 -agent(skc7, skf7(skf11(skc8, skc7)), skf11(skc8, skc7)) % 54.76/55.02 -agent(skc7, skf7(skf9(skc8, skc7)), skf9(skc8, skc7)) % 54.76/55.02 +animate(skc7, skc14) % 54.76/55.02 -animate(skc7, skc12) % 54.76/55.02 +beverage(skc7, skc12) % 54.76/55.02 -beverage(skc7, skc14) % 54.76/55.02 -beverage(skc7, skc8) % 54.76/55.02 -beverage(skc7, skc11) % 54.76/55.02 -beverage(skc7, skc13) % 54.76/55.02 -beverage(skc7, skf17(skc8, skc7)) % 54.76/55.02 -beverage(skc7, skf15(skc8, skc7)) % 54.76/55.02 -beverage(skc7, skf13(skc8, skc7)) % 54.76/55.02 -beverage(skc7, skf11(skc8, skc7)) % 54.76/55.02 -beverage(skc7, skf9(skc8, skc7)) % 54.76/55.02 -beverage(skc7, skf7(_0)) % 54.76/55.02 +cash(skc7, skf17(skc8, skc7)) % 54.76/55.02 +cash(skc7, skf15(skc8, skc7)) % 54.76/55.02 +cash(skc7, skf13(skc8, skc7)) % 54.76/55.02 +cash(skc7, skf11(skc8, skc7)) % 54.76/55.02 +cash(skc7, skf9(skc8, skc7)) % 54.76/55.02 -cash(skc7, skc14) % 54.76/55.02 -cash(skc7, skc12) % 54.76/55.02 -cash(skc7, skc8) % 54.76/55.02 -cash(skc7, skc11) % 54.76/55.02 -cash(skc7, skf7(_0)) % 54.76/55.02 +cost(skc7, skf7(_0)) % 54.76/55.02 -cost(skc7, skc14) % 54.76/55.02 -cost(skc7, skc12) % 54.76/55.02 -cost(skc7, skc8) % 54.76/55.02 -cost(skc7, skc13) % 54.76/55.02 -cost(skc7, skf17(skc8, skc7)) % 54.76/55.02 -cost(skc7, skf15(skc8, skc7)) % 54.76/55.02 -cost(skc7, skf13(skc8, skc7)) % 54.76/55.02 -cost(skc7, skf11(skc8, skc7)) % 54.76/55.02 -cost(skc7, skf9(skc8, skc7)) % 54.76/55.02 +currency(skc7, skf17(skc8, skc7)) % 54.76/55.02 +currency(skc7, skf15(skc8, skc7)) % 54.76/55.02 +currency(skc7, skf13(skc8, skc7)) % 54.76/55.02 +currency(skc7, skf11(skc8, skc7)) % 54.76/55.02 +currency(skc7, skf9(skc8, skc7)) % 54.76/55.02 -currency(skc7, skc14) % 54.76/55.02 -currency(skc7, skc12) % 54.76/55.02 -currency(skc7, skc8) % 54.76/55.02 -currency(skc7, skc11) % 54.76/55.02 -currency(skc7, skf7(_0)) % 54.76/55.02 +dollar(skc7, skf17(skc8, skc7)) % 54.76/55.02 +dollar(skc7, skf15(skc8, skc7)) % 54.76/55.02 +dollar(skc7, skf13(skc8, skc7)) % 54.76/55.02 +dollar(skc7, skf11(skc8, skc7)) % 54.76/55.02 +dollar(skc7, skf9(skc8, skc7)) % 54.76/55.02 -dollar(skc7, skc14) % 54.76/55.02 -dollar(skc7, skc12) % 54.76/55.02 -dollar(skc7, skc8) % 54.76/55.02 -dollar(skc7, skc11) % 54.76/55.02 -dollar(skc7, skf7(_0)) % 54.76/55.02 +entity(skc7, skc14) % 54.76/55.02 +entity(skc7, skc12) % 54.76/55.02 -entity(skc7, skc8) % 54.76/55.02 -entity(skc7, skc11) % 54.76/55.02 -entity(skc7, skc13) % 54.76/55.02 -entity(skc7, skf17(skc8, skc7)) % 54.76/55.02 -entity(skc7, skf15(skc8, skc7)) % 54.76/55.02 -entity(skc7, skf13(skc8, skc7)) % 54.76/55.02 -entity(skc7, skf11(skc8, skc7)) % 54.76/55.02 -entity(skc7, skf9(skc8, skc7)) % 54.76/55.02 -entity(skc7, skf7(_0)) % 54.76/55.02 +event(skc7, skc11) % 54.76/55.02 +event(skc7, skf7(_0)) % 54.76/55.02 -event(skc7, skc14) % 54.76/55.02 -event(skc7, skc12) % 54.76/55.02 -event(skc7, skc8) % 54.76/55.02 -event(skc7, skc13) % 54.76/55.02 -event(skc7, skf17(skc8, skc7)) % 54.76/55.02 -event(skc7, skf15(skc8, skc7)) % 54.76/55.02 -event(skc7, skf13(skc8, skc7)) % 54.76/55.02 -event(skc7, skf11(skc8, skc7)) % 54.76/55.02 -event(skc7, skf9(skc8, skc7)) % 54.76/55.02 +eventuality(skc7, skc11) % 54.76/55.02 +eventuality(skc7, skf7(_0)) % 54.76/55.02 -eventuality(skc7, skc14) % 54.76/55.02 -eventuality(skc7, skc12) % 54.76/55.02 -eventuality(skc7, skc8) % 54.76/55.02 -eventuality(skc7, skc13) % 54.76/55.02 -eventuality(skc7, skf17(skc8, skc7)) % 54.76/55.02 -eventuality(skc7, skf15(skc8, skc7)) % 54.76/55.02 -eventuality(skc7, skf13(skc8, skc7)) % 54.76/55.02 -eventuality(skc7, skf11(skc8, skc7)) % 54.76/55.02 -eventuality(skc7, skf9(skc8, skc7)) % 54.76/55.02 +existent(skc7, skc14) % 54.76/55.02 +existent(skc7, skc12) % 54.76/55.02 -existent(skc7, skc11) % 54.76/55.02 -existent(skc7, skf7(_0)) % 54.76/55.02 +female(skc7, skc14) % 54.76/55.02 -female(skc7, skc12) % 54.76/55.02 -female(skc7, skc11) % 54.76/55.02 -female(skc7, skc13) % 54.76/55.02 -female(skc7, skf17(skc8, skc7)) % 54.76/55.02 -female(skc7, skf15(skc8, skc7)) % 54.76/55.02 -female(skc7, skf13(skc8, skc7)) % 54.76/55.02 -female(skc7, skf11(skc8, skc7)) % 54.76/55.02 -female(skc7, skf9(skc8, skc7)) % 54.76/55.02 -female(skc7, skf7(_0)) % 54.76/55.02 +five(skc7, skc8) % 54.76/55.02 -five(skc7, skc14) % 54.76/55.02 -five(skc7, skc12) % 54.76/55.02 -five(skc7, skc11) % 54.76/55.02 -five(skc7, skc13) % 54.76/55.02 -five(skc7, skf17(skc8, skc7)) % 54.76/55.02 -five(skc7, skf15(skc8, skc7)) % 54.76/55.02 -five(skc7, skf13(skc8, skc7)) % 54.76/55.02 -five(skc7, skf11(skc8, skc7)) % 54.76/55.02 -five(skc7, skf9(skc8, skc7)) % 54.76/55.02 -five(skc7, skf7(_0)) % 54.76/55.02 +food(skc7, skc12) % 54.76/55.02 -food(skc7, skc14) % 54.76/55.02 -food(skc7, skc8) % 54.76/55.02 -food(skc7, skc11) % 54.76/55.02 -food(skc7, skc13) % 54.76/55.02 -food(skc7, skf17(skc8, skc7)) % 54.76/55.02 -food(skc7, skf15(skc8, skc7)) % 54.76/55.02 -food(skc7, skf13(skc8, skc7)) % 54.76/55.02 -food(skc7, skf11(skc8, skc7)) % 54.76/55.02 -food(skc7, skf9(skc8, skc7)) % 54.76/55.02 -food(skc7, skf7(_0)) % 54.76/55.02 +forename(skc7, skc13) % 54.76/55.02 -forename(skc7, skc14) % 54.76/55.02 -forename(skc7, skc12) % 54.76/55.02 -forename(skc7, skc8) % 54.76/55.02 -forename(skc7, skc11) % 54.76/55.02 -forename(skc7, skf7(_0)) % 54.76/55.02 +general(skc7, skc13) % 54.76/55.02 +general(skc7, skf17(skc8, skc7)) % 54.76/55.02 +general(skc7, skf15(skc8, skc7)) % 54.76/55.02 +general(skc7, skf13(skc8, skc7)) % 54.76/55.02 +general(skc7, skf11(skc8, skc7)) % 54.76/55.02 +general(skc7, skf9(skc8, skc7)) % 54.76/55.02 -general(skc7, skc14) % 54.76/55.02 -general(skc7, skc12) % 54.76/55.02 -general(skc7, skc11) % 54.76/55.02 -general(skc7, skf7(_0)) % 54.76/55.02 +group(skc7, skc8) % 54.76/55.02 -group(skc7, skc14) % 54.76/55.02 -group(skc7, skc12) % 54.76/55.02 -group(skc7, skc11) % 54.76/55.02 -group(skc7, skc13) % 54.76/55.02 -group(skc7, skf17(skc8, skc7)) % 54.76/55.02 -group(skc7, skf15(skc8, skc7)) % 54.76/55.02 -group(skc7, skf13(skc8, skc7)) % 54.76/55.02 -group(skc7, skf11(skc8, skc7)) % 54.76/55.02 -group(skc7, skf9(skc8, skc7)) % 54.76/55.02 -group(skc7, skf7(_0)) % 54.76/55.02 +human(skc7, skc14) % 54.76/55.02 -human(skc7, skc9) % 54.76/55.02 -human(skc7, skc13) % 54.76/55.02 -human(skc7, skf17(skc8, skc7)) % 54.76/55.02 -human(skc7, skf15(skc8, skc7)) % 54.76/55.02 -human(skc7, skf13(skc8, skc7)) % 54.76/55.02 -human(skc7, skf11(skc8, skc7)) % 54.76/55.02 -human(skc7, skf9(skc8, skc7)) % 54.76/55.02 +human_person(skc7, skc14) % 54.76/55.02 -human_person(skc7, skc12) % 54.76/55.02 -human_person(skc7, skc9) % 54.76/55.02 -human_person(skc7, skc8) % 54.76/55.02 -human_person(skc7, skc11) % 54.76/55.02 -human_person(skc7, skc13) % 54.76/55.02 -human_person(skc7, skf17(skc8, skc7)) % 54.76/55.02 -human_person(skc7, skf15(skc8, skc7)) % 54.76/55.02 -human_person(skc7, skf13(skc8, skc7)) % 54.76/55.02 -human_person(skc7, skf11(skc8, skc7)) % 54.76/55.02 -human_person(skc7, skf9(skc8, skc7)) % 54.76/55.02 -human_person(skc7, skf7(_0)) % 54.76/55.02 +impartial(_0, _1) % 54.76/55.02 +living(skc7, skc14) % 54.76/55.02 -living(skc7, skc12) % 54.76/55.02 +member(skc7, skf17(skc8, skc7), skc8) % 54.76/55.02 +member(skc7, skf15(skc8, skc7), skc8) % 54.76/55.02 +member(skc7, skf13(skc8, skc7), skc8) % 54.76/55.02 +member(skc7, skf11(skc8, skc7), skc8) % 54.76/55.02 +member(skc7, skf9(skc8, skc7), skc8) % 54.76/55.02 -member(_0, _1, _1) % 54.76/55.02 -member(skc7, skc14, skc8) % 54.76/55.02 -member(skc7, skc12, skc8) % 54.76/55.02 -member(skc7, skc9, skc8) % 54.76/55.02 -member(skc7, skc11, skc8) % 54.76/55.02 -member(skc7, skf7(_0), skc8) % 54.76/55.02 +mia_forename(skc7, skc13) % 54.76/55.02 -mia_forename(skc7, skc14) % 54.76/55.02 -mia_forename(skc7, skc12) % 54.76/55.02 -mia_forename(skc7, skc8) % 54.76/55.02 -mia_forename(skc7, skc11) % 54.76/55.02 -mia_forename(skc7, skf7(_0)) % 54.76/55.02 +multiple(skc7, skc8) % 54.76/55.02 -multiple(skc7, skc14) % 54.76/55.02 -multiple(skc7, skc12) % 54.76/55.02 -multiple(skc7, skc11) % 54.76/55.02 -multiple(skc7, skc13) % 54.76/55.02 -multiple(skc7, skf17(skc8, skc7)) % 54.76/55.02 -multiple(skc7, skf15(skc8, skc7)) % 54.76/55.02 -multiple(skc7, skf13(skc8, skc7)) % 54.76/55.02 -multiple(skc7, skf11(skc8, skc7)) % 54.76/55.02 -multiple(skc7, skf9(skc8, skc7)) % 54.76/55.02 -multiple(skc7, skf7(_0)) % 54.76/55.02 +nonexistent(skc7, skc11) % 54.76/55.02 +nonexistent(skc7, skf7(_0)) % 54.76/55.02 -nonexistent(skc7, skc14) % 54.76/55.02 -nonexistent(skc7, skc12) % 54.76/55.02 +nonhuman(skc7, skc9) % 54.76/55.02 +nonhuman(skc7, skc13) % 54.76/55.02 +nonhuman(skc7, skf17(skc8, skc7)) % 54.76/55.02 +nonhuman(skc7, skf15(skc8, skc7)) % 54.76/55.02 +nonhuman(skc7, skf13(skc8, skc7)) % 54.76/55.02 +nonhuman(skc7, skf11(skc8, skc7)) % 54.76/55.02 +nonhuman(skc7, skf9(skc8, skc7)) % 54.76/55.02 -nonhuman(skc7, skc14) % 54.76/55.02 +nonliving(skc7, skc12) % 54.76/55.02 -nonliving(skc7, skc14) % 54.76/55.02 +nonreflexive(skc7, skc11) % 54.76/55.02 +nonreflexive(skc7, skf7(_0)) % 54.76/55.02 +object(skc7, skc12) % 54.76/55.02 -object(skc7, skc14) % 54.76/55.02 -object(skc7, skc8) % 54.76/55.02 -object(skc7, skc11) % 54.76/55.02 -object(skc7, skc13) % 54.76/55.02 -object(skc7, skf17(skc8, skc7)) % 54.76/55.02 -object(skc7, skf15(skc8, skc7)) % 54.76/55.02 -object(skc7, skf13(skc8, skc7)) % 54.76/55.02 -object(skc7, skf11(skc8, skc7)) % 54.76/55.02 -object(skc7, skf9(skc8, skc7)) % 54.76/55.02 -object(skc7, skf7(_0)) % 54.76/55.02 +of(skc7, skc13, skc14) % 54.76/55.02 +order(skc7, skc11) % 54.76/55.02 -order(skc7, skc14) % 54.76/55.02 -order(skc7, skc12) % 54.76/55.02 -order(skc7, skc8) % 54.76/55.02 -order(skc7, skc13) % 54.76/55.02 -order(skc7, skf17(skc8, skc7)) % 54.76/55.02 -order(skc7, skf15(skc8, skc7)) % 54.76/55.02 -order(skc7, skf13(skc8, skc7)) % 54.76/55.02 -order(skc7, skf11(skc8, skc7)) % 54.76/55.02 -order(skc7, skf9(skc8, skc7)) % 54.76/55.02 +organism(skc7, skc14) % 54.76/55.02 -organism(skc7, skc12) % 54.76/55.02 -organism(skc7, skc8) % 54.76/55.02 -organism(skc7, skc11) % 54.76/55.02 -organism(skc7, skc13) % 54.76/55.02 -organism(skc7, skf17(skc8, skc7)) % 54.76/55.02 -organism(skc7, skf15(skc8, skc7)) % 54.76/55.02 -organism(skc7, skf13(skc8, skc7)) % 54.76/55.02 -organism(skc7, skf11(skc8, skc7)) % 54.76/55.02 -organism(skc7, skf9(skc8, skc7)) % 54.76/55.02 -organism(skc7, skf7(_0)) % 54.76/55.02 +past(skc7, skc11) % 54.76/55.02 -past(skc7, skf7(_0)) % 54.76/55.02 +patient(skc7, skc11, skc12) % 54.76/55.02 +patient(skc7, skf7(skf17(skc8, skc7)), skf17(skc8, skc7)) % 54.76/55.02 +patient(skc7, skf7(skf15(skc8, skc7)), skf15(skc8, skc7)) % 54.76/55.02 +patient(skc7, skf7(skf13(skc8, skc7)), skf13(skc8, skc7)) % 54.76/55.02 +patient(skc7, skf7(skf11(skc8, skc7)), skf11(skc8, skc7)) % 54.76/55.02 +patient(skc7, skf7(skf9(skc8, skc7)), skf9(skc8, skc7)) % 54.76/55.02 -patient(skc7, skc11, skc14) % 54.76/55.02 -patient(skc7, skf7(_0), skc9) % 54.76/55.02 +possession(skc7, skf17(skc8, skc7)) % 54.76/55.02 +possession(skc7, skf15(skc8, skc7)) % 54.76/55.02 +possession(skc7, skf13(skc8, skc7)) % 54.76/55.02 +possession(skc7, skf11(skc8, skc7)) % 54.76/55.02 +possession(skc7, skf9(skc8, skc7)) % 54.76/55.02 -possession(skc7, skc14) % 54.76/55.02 -possession(skc7, skc12) % 54.76/55.02 -possession(skc7, skc8) % 54.76/55.02 -possession(skc7, skc11) % 54.76/55.02 -possession(skc7, skf7(_0)) % 54.76/55.02 +present(skc7, skf7(_0)) % 54.76/55.02 -present(skc7, skc11) % 54.76/55.02 +relation(skc7, skc13) % 54.76/55.02 -relation(skc7, skc14) % 54.76/55.02 -relation(skc7, skc12) % 54.76/55.02 -relation(skc7, skc8) % 54.76/55.02 -relation(skc7, skc11) % 54.76/55.02 -relation(skc7, skf7(_0)) % 54.76/55.02 +relname(skc7, skc13) % 54.76/55.02 -relname(skc7, skc14) % 54.76/55.02 -relname(skc7, skc12) % 54.76/55.02 -relname(skc7, skc8) % 54.76/55.02 -relname(skc7, skc11) % 54.76/55.02 -relname(skc7, skf7(_0)) % 54.76/55.02 +set(skc7, skc8) % 54.76/55.02 -set(skc7, skc14) % 54.76/55.02 -set(skc7, skc12) % 54.76/55.02 -set(skc7, skc11) % 54.76/55.02 -set(skc7, skc13) % 54.76/55.02 -set(skc7, skf17(skc8, skc7)) % 54.76/55.02 -set(skc7, skf15(skc8, skc7)) % 54.76/55.02 -set(skc7, skf13(skc8, skc7)) % 54.76/55.02 -set(skc7, skf11(skc8, skc7)) % 54.76/55.02 -set(skc7, skf9(skc8, skc7)) % 54.76/55.02 -set(skc7, skf7(_0)) % 54.76/55.02 +shake_beverage(skc7, skc12) % 54.76/55.02 -shake_beverage(skc7, skc14) % 54.76/55.02 -shake_beverage(skc7, skc8) % 54.76/55.02 -shake_beverage(skc7, skc11) % 54.76/55.02 -shake_beverage(skc7, skc13) % 54.76/55.02 -shake_beverage(skc7, skf17(skc8, skc7)) % 54.76/55.02 -shake_beverage(skc7, skf15(skc8, skc7)) % 54.76/55.02 -shake_beverage(skc7, skf13(skc8, skc7)) % 54.76/55.02 -shake_beverage(skc7, skf11(skc8, skc7)) % 54.76/55.02 -shake_beverage(skc7, skf9(skc8, skc7)) % 54.76/55.02 -shake_beverage(skc7, skf7(_0)) % 54.76/55.02 +singleton(skc7, skc14) % 54.76/55.02 +singleton(skc7, skc12) % 54.76/55.02 +singleton(skc7, skc11) % 54.76/55.02 +singleton(skc7, skc13) % 54.76/55.02 +singleton(skc7, skf17(skc8, skc7)) % 54.76/55.02 +singleton(skc7, skf15(skc8, skc7)) % 54.76/55.02 +singleton(skc7, skf13(skc8, skc7)) % 54.76/55.02 +singleton(skc7, skf11(skc8, skc7)) % 54.76/55.02 +singleton(skc7, skf9(skc8, skc7)) % 54.76/55.02 +singleton(skc7, skf7(_0)) % 54.76/55.02 -singleton(skc7, skc8) % 54.76/55.02 +specific(skc7, skc14) % 54.76/55.02 +specific(skc7, skc12) % 54.76/55.02 +specific(skc7, skc11) % 54.76/55.02 +specific(skc7, skf7(_0)) % 54.76/55.02 -specific(skc7, skc13) % 54.76/55.02 -specific(skc7, skf17(skc8, skc7)) % 54.76/55.02 -specific(skc7, skf15(skc8, skc7)) % 54.76/55.02 -specific(skc7, skf13(skc8, skc7)) % 54.76/55.02 -specific(skc7, skf11(skc8, skc7)) % 54.76/55.02 -specific(skc7, skf9(skc8, skc7)) % 54.76/55.02 +substance_matter(skc7, skc12) % 54.76/55.02 -substance_matter(skc7, skc14) % 54.76/55.02 -substance_matter(skc7, skc8) % 54.76/55.02 -substance_matter(skc7, skc11) % 54.76/55.02 -substance_matter(skc7, skc13) % 54.76/55.02 -substance_matter(skc7, skf17(skc8, skc7)) % 54.76/55.02 -substance_matter(skc7, skf15(skc8, skc7)) % 54.76/55.02 -substance_matter(skc7, skf13(skc8, skc7)) % 54.76/55.02 -substance_matter(skc7, skf11(skc8, skc7)) % 54.76/55.02 -substance_matter(skc7, skf9(skc8, skc7)) % 54.76/55.02 -substance_matter(skc7, skf7(_0)) % 54.76/55.02 +thing(skc7, skc14) % 54.76/55.02 +thing(skc7, skc12) % 54.76/55.02 +thing(skc7, skc11) % 54.76/55.02 +thing(skc7, skc13) % 54.76/55.02 +thing(skc7, skf17(skc8, skc7)) % 54.76/55.02 +thing(skc7, skf15(skc8, skc7)) % 54.76/55.02 +thing(skc7, skf13(skc8, skc7)) % 54.76/55.02 +thing(skc7, skf11(skc8, skc7)) % 54.76/55.02 +thing(skc7, skf9(skc8, skc7)) % 54.76/55.02 +thing(skc7, skf7(_0)) % 54.76/55.02 -thing(skc7, skc8) % 54.76/55.02 +unisex(skc7, skc12) % 54.76/55.02 +unisex(skc7, skc11) % 54.76/55.02 +unisex(skc7, skc13) % 54.76/55.02 +unisex(skc7, skf17(skc8, skc7)) % 54.76/55.02 +unisex(skc7, skf15(skc8, skc7)) % 54.76/55.02 +unisex(skc7, skf13(skc8, skc7)) % 54.76/55.02 +unisex(skc7, skf11(skc8, skc7)) % 54.76/55.02 +unisex(skc7, skf9(skc8, skc7)) % 54.76/55.02 +unisex(skc7, skf7(_0)) % 54.76/55.02 -unisex(skc7, skc14) % 54.76/55.02 +woman(skc7, skc14) % 54.76/55.02 -woman(skc7, skc12) % 54.76/55.02 -woman(skc7, skc9) % 54.76/55.02 -woman(skc7, skc8) % 54.76/55.02 -woman(skc7, skc11) % 54.76/55.02 -woman(skc7, skc13) % 54.76/55.02 -woman(skc7, skf17(skc8, skc7)) % 54.76/55.02 -woman(skc7, skf15(skc8, skc7)) % 54.76/55.02 -woman(skc7, skf13(skc8, skc7)) % 54.76/55.02 -woman(skc7, skf11(skc8, skc7)) % 54.76/55.02 -woman(skc7, skf9(skc8, skc7)) % 54.76/55.02 -woman(skc7, skf7(_0)) % 54.76/55.02 SZS output end Model for /export/starexec/sandbox2/benchmark/theBenchmark.p %------------------------------------------------------------------------------