%------------------------------------------------------------------------------ % File : Z3---4.15.1 % Problem : PUZ031_10 : TPTP v9.0.0. Released v8.2.0. % Transfm : none % Format : tptp % Command : run_E %s %d THM % Computer : n012.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 Jun 21 05:23:13 AM UTC 2025 % Result : Satisfiable 0.19s 0.41s % Output : Model 0.19s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : PUZ031_10 : TPTP v9.0.0. Released v8.2.0. % 0.12/0.12 % Command : run_E %s %d THM % 0.12/0.34 % Computer : n012.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Fri Jun 20 02:40:10 EDT 2025 % 0.12/0.34 % CPUTime : % 0.19/0.41 % SZS status Satisfiable % 0.19/0.41 % SZS output start Model % 0.19/0.41 tff(edible_val_6_type, type, ( % 0.19/0.41 edible_val_6: edible)). % 0.19/0.41 tff(animal_to_edible_type, type, ( % 0.19/0.41 animal_to_edible: animal > edible)). % 0.19/0.41 tff(animal_val_0_type, type, ( % 0.19/0.41 animal_val_0: animal)). % 0.19/0.41 tff(edible_val_7_type, type, ( % 0.19/0.41 edible_val_7: edible)). % 0.19/0.41 tff(edible_val_0_type, type, ( % 0.19/0.41 edible_val_0: edible)). % 0.19/0.41 tff(animal_val_4_type, type, ( % 0.19/0.41 animal_val_4: animal)). % 0.19/0.41 tff(animal_val_3_type, type, ( % 0.19/0.41 animal_val_3: animal)). % 0.19/0.41 tff(animal_val_1_type, type, ( % 0.19/0.41 animal_val_1: animal)). % 0.19/0.41 tff(edible_val_3_type, type, ( % 0.19/0.41 edible_val_3: edible)). % 0.19/0.41 tff(edible_val_4_type, type, ( % 0.19/0.41 edible_val_4: edible)). % 0.19/0.41 tff(edible_val_5_type, type, ( % 0.19/0.41 edible_val_5: edible)). % 0.19/0.41 tff(edible_val_2_type, type, ( % 0.19/0.41 edible_val_2: edible)). % 0.19/0.41 tff(edible_val_1_type, type, ( % 0.19/0.41 edible_val_1: edible)). % 0.19/0.41 tff(eats_type, type, ( % 0.19/0.41 eats: ( animal * edible ) > $o)). % 0.19/0.41 tff(bird_to_animal_type, type, ( % 0.19/0.41 bird_to_animal: bird > animal)). % 0.19/0.41 tff(much_smaller_type, type, ( % 0.19/0.41 much_smaller: ( animal * animal ) > $o)). % 0.19/0.41 tff(plant_to_edible_type, type, ( % 0.19/0.41 plant_to_edible: plant > edible)). % 0.19/0.41 tff(plant_val_2_type, type, ( % 0.19/0.41 plant_val_2: plant)). % 0.19/0.41 tff(edible_val_8_type, type, ( % 0.19/0.41 edible_val_8: edible)). % 0.19/0.41 tff(plant_val_0_type, type, ( % 0.19/0.41 plant_val_0: plant)). % 0.19/0.41 tff(wolf_to_animal_type, type, ( % 0.19/0.41 wolf_to_animal: wolf > animal)). % 0.19/0.41 tff(animal_val_2_type, type, ( % 0.19/0.41 animal_val_2: animal)). % 0.19/0.41 tff(snail_to_animal_type, type, ( % 0.19/0.41 snail_to_animal: snail > animal)). % 0.19/0.41 tff(fox_to_animal_type, type, ( % 0.19/0.41 fox_to_animal: fox > animal)). % 0.19/0.41 tff(caterpillar_to_animal_type, type, ( % 0.19/0.41 caterpillar_to_animal: caterpillar > animal)). % 0.19/0.41 tff(grain_to_plant_type, type, ( % 0.19/0.41 grain_to_plant: grain > plant)). % 0.19/0.41 tff(formula1, axiom, % 0.19/0.41 animal_to_edible(animal!val!0) = edible!val!6). % 0.19/0.41 tff(formula2, axiom, % 0.19/0.41 ![X0: animal] : ((~((animal!val!0 = X0))) => (animal_to_edible(X0) = ite_t(((X0 = animal!val!4) & (~(X0 = animal!val!0))), edible!val!4, ite_t(((~(X0 = animal!val!1)) & (~(X0 = animal!val!3)) & (~(X0 = animal!val!4)) & (~(X0 = animal!val!0))), edible!val!3, ite_t(((X0 = animal!val!1) & (~(X0 = animal!val!3)) & (~(X0 = animal!val!4)) & (~(X0 = animal!val!0))), edible!val!0, edible!val!7)))))). % 0.19/0.41 tff(formula3, axiom, % 0.19/0.41 ![X0: animal, X1: edible] : (eats(X0, X1) <=> ((~((X1 = animal!val!4) & (~(X1 = animal!val!0)) & (X0 = edible!val!5))) & (~((X1 = animal!val!4) & (~(X1 = animal!val!0)) & (X0 = edible!val!1))) & (~((X1 = animal!val!4) & (~(X1 = animal!val!0)) & (X0 = edible!val!2))) & (~((X1 = animal!val!3) & (~(X1 = animal!val!4)) & (~(X1 = animal!val!0)) & (X0 = edible!val!5))) & (~((X1 = animal!val!3) & (~(X1 = animal!val!4)) & (~(X1 = animal!val!0)) & (X0 = edible!val!4))) & (~((X1 = animal!val!0) & (X0 = edible!val!3)))))). % 0.19/0.41 tff(formula4, axiom, % 0.19/0.41 ![X0: bird] : (bird_to_animal(X0) = animal!val!0)). % 0.19/0.41 tff(formula5, axiom, % 0.19/0.41 ![X0: animal, X1: animal] : (much_smaller(X0, X1) <=> (((X1 = animal!val!4) & (~(X1 = animal!val!0)) & (X0 = animal!val!3) & (~(X0 = animal!val!4)) & (~(X0 = animal!val!0))) | ((~(X1 = animal!val!1)) & (~(X1 = animal!val!3)) & (~(X1 = animal!val!4)) & (~(X1 = animal!val!0)) & (X0 = animal!val!0)) | ((X1 = animal!val!1) & (~(X1 = animal!val!3)) & (~(X1 = animal!val!4)) & (~(X1 = animal!val!0)) & (X0 = animal!val!0)) | ((X1 = animal!val!0) & (X0 = animal!val!4) & (~(X0 = animal!val!0)))))). % 0.19/0.41 tff(formula6, axiom, % 0.19/0.41 plant_to_edible(plant!val!2) = edible!val!5). % 0.19/0.41 tff(formula7, axiom, % 0.19/0.41 ![X0: plant] : ((~((plant!val!2 = X0))) => (plant_to_edible(X0) = ite_t(((~(X0 = plant!val!0)) & (~(X0 = plant!val!2))), edible!val!2, ite_t(((X0 = plant!val!0) & (~(X0 = plant!val!2))), edible!val!1, edible!val!8))))). % 0.19/0.41 tff(formula8, axiom, % 0.19/0.41 ![X0: wolf] : (wolf_to_animal(X0) = animal!val!3)). % 0.19/0.41 tff(formula9, axiom, % 0.19/0.41 ![X0: snail] : (snail_to_animal(X0) = animal!val!2)). % 0.19/0.41 tff(formula10, axiom, % 0.19/0.41 ![X0: fox] : (fox_to_animal(X0) = animal!val!4)). % 0.19/0.41 tff(formula11, axiom, % 0.19/0.41 ![X0: caterpillar] : (caterpillar_to_animal(X0) = animal!val!1)). % 0.19/0.41 tff(formula12, axiom, % 0.19/0.41 ![X0: grain] : (grain_to_plant(X0) = plant!val!2)). % 0.19/0.41 % SZS output end Model % 0.19/0.41 % E exiting %------------------------------------------------------------------------------