%------------------------------------------------------------------------------ % File : FEST---2.0.1 % Problem : PUZ031_10 : TPTP v9.0.0. Released v8.2.0. % Transfm : none % Format : tptp:raw % Command : run_fest %s %d % Computer : n021.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 : 300s % DateTime : Sat Mar 29 08:44:16 AM UTC 2025 % Result : Satisfiable 130.50s 19.91s % Output : Model 130.50s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.11 % Problem : PUZ031_10 : TPTP v9.0.0. Released v8.2.0. % 0.04/0.11 % Command : run_fest %s %d % 0.11/0.32 % Computer : n021.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 300 % 0.11/0.32 % DateTime : Fri Mar 28 20:40:35 EDT 2025 % 0.11/0.32 % CPUTime : % 130.50/19.91 % SZS status Satisfiable for /export/starexec/sandbox/tmp/tmp.mkNHZeERsG/FEST_18141.smt2 % 130.50/19.91 % SZS output start Model % 130.50/19.91 tptp.plant: tptp.plant_0, tptp.plant_1 % 130.50/19.91 tptp.wolf: tptp.wolf_1, tptp.wolf_0 % 130.50/19.91 tptp.animal: tptp.animal_1, tptp.animal_0, tptp.animal_2 % 130.50/19.91 tptp.caterpillar: tptp.caterpillar_1, tptp.caterpillar_0 % 130.50/19.91 tptp.edible: tptp.edible_1, tptp.edible_0 % 130.50/19.91 tptp.fox: tptp.fox_1, tptp.fox_0 % 130.50/19.91 tptp.grain: tptp.grain_0, tptp.grain_1 % 130.50/19.91 tptp.bird: tptp.bird_0, tptp.bird_1 % 130.50/19.91 tptp.snail: tptp.snail_0, tptp.snail_1, <tptp.snail_2, i: 0 <= i> % 130.50/19.91 tptp.bird_to_animal(tptp.bird_1) -> <tptp.animal_0, 0> % 130.50/19.91 tptp.bird_to_animal(tptp.bird_0) -> <tptp.animal_0, 0> % 130.50/19.91 tptp.wolf_to_animal(tptp.wolf_1) -> <tptp.animal_2, 0> % 130.50/19.91 tptp.wolf_to_animal(tptp.wolf_0) -> <tptp.animal_2, 0> % 130.50/19.91 tptp.snail_to_animal(tptp.snail_1) -> <tptp.animal_0, 0> % 130.50/19.91 tptp.snail_to_animal(tptp.snail_0) -> <tptp.animal_0, 0> % 130.50/19.91 tptp.snail_to_animal(<tptp.snail_2, i_1>) -> <tptp.animal_0, 0> % 130.50/19.91 tptp.animal_to_edible(tptp.animal_1) -> <tptp.edible_0, 0> % 130.50/19.91 tptp.animal_to_edible(tptp.animal_0) -> <tptp.edible_1, 0> % 130.50/19.91 tptp.animal_to_edible(tptp.animal_2) -> <tptp.edible_0, 0> % 130.50/19.91 tptp.fox_to_animal(tptp.fox_0) -> <tptp.animal_2, 0> % 130.50/19.91 tptp.fox_to_animal(tptp.fox_1) -> <tptp.animal_2, 0> % 130.50/19.91 tptp.plant_to_edible(tptp.plant_0) -> <tptp.edible_0, 0> % 130.50/19.91 tptp.plant_to_edible(tptp.plant_1) -> <tptp.edible_0, 0> % 130.50/19.91 tptp.grain_to_plant(tptp.grain_1) -> <tptp.plant_0, 0> % 130.50/19.91 tptp.grain_to_plant(tptp.grain_0) -> <tptp.plant_0, 0> % 130.50/19.91 tptp.caterpillar_to_animal(tptp.caterpillar_0) -> <tptp.animal_1, 0> % 130.50/19.91 tptp.caterpillar_to_animal(tptp.caterpillar_1) -> <tptp.animal_1, 0> % 130.50/19.91 tptp.much_smaller(tptp.animal_1, tptp.animal_1): True % 130.50/19.91 tptp.much_smaller(tptp.animal_1, tptp.animal_0): True % 130.50/19.91 tptp.much_smaller(tptp.animal_1, tptp.animal_2): False % 130.50/19.91 tptp.much_smaller(tptp.animal_0, tptp.animal_1): True % 130.50/19.91 tptp.much_smaller(tptp.animal_0, tptp.animal_0): True % 130.50/19.91 tptp.much_smaller(tptp.animal_0, tptp.animal_2): True % 130.50/19.91 tptp.much_smaller(tptp.animal_2, tptp.animal_1): False % 130.50/19.91 tptp.much_smaller(tptp.animal_2, tptp.animal_0): True % 130.50/19.91 tptp.much_smaller(tptp.animal_2, tptp.animal_2): True % 130.50/19.91 tptp.eats(tptp.animal_1, tptp.edible_0): True % 130.50/19.91 tptp.eats(tptp.animal_1, tptp.edible_1): True % 130.50/19.91 tptp.eats(tptp.animal_0, tptp.edible_0): True % 130.50/19.91 tptp.eats(tptp.animal_0, tptp.edible_1): False % 130.50/19.91 tptp.eats(tptp.animal_2, tptp.edible_0): False % 130.50/19.91 tptp.eats(tptp.animal_2, tptp.edible_1): True % 130.50/19.91 % SZS output end Model % 130.50/19.91 % FEST exiting % 130.50/19.91 % FEST exiting %------------------------------------------------------------------------------