%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : PUZ010-1 : TPTP v9.3.1. Bugfixed v1.0.1.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 08:54:17 AM UTC 2026
% Result : Unsatisfiable 183.03s 183.38s
% Output : Proof 183.13s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(people_live_somewhere,axiom,
( lives(Person,house_5)
| lives(Person,house_4)
| lives(Person,house_3)
| lives(Person,house_2)
| lives(Person,house_1)
| ~ person(Person) ),
file('theBenchmark.p',people_live_somewhere) ).
cnf(english_and_spaniard_live_apart,axiom,
( ~ lives(spaniard,H)
| ~ lives(english,H)
| ~ house(H) ),
file('theBenchmark.p',english_and_spaniard_live_apart) ).
cnf(english_and_norwegian_live_apart,axiom,
( ~ lives(norwegian,H)
| ~ lives(english,H)
| ~ house(H) ),
file('theBenchmark.p',english_and_norwegian_live_apart) ).
cnf(english_and_ukranian_live_apart,axiom,
( ~ lives(ukranian,H)
| ~ lives(english,H)
| ~ house(H) ),
file('theBenchmark.p',english_and_ukranian_live_apart) ).
cnf(english_and_japanese_live_apart,axiom,
( ~ lives(japanese,H)
| ~ lives(english,H)
| ~ house(H) ),
file('theBenchmark.p',english_and_japanese_live_apart) ).
cnf(spaniard_and_norwegian_live_apart,axiom,
( ~ lives(norwegian,H)
| ~ lives(spaniard,H)
| ~ house(H) ),
file('theBenchmark.p',spaniard_and_norwegian_live_apart) ).
cnf(spaniard_and_ukranian_live_apart,axiom,
( ~ lives(ukranian,H)
| ~ lives(spaniard,H)
| ~ house(H) ),
file('theBenchmark.p',spaniard_and_ukranian_live_apart) ).
cnf(spaniard_and_japanese_live_apart,axiom,
( ~ lives(japanese,H)
| ~ lives(spaniard,H)
| ~ house(H) ),
file('theBenchmark.p',spaniard_and_japanese_live_apart) ).
cnf(norwegian_and_ukranian_live_apart,axiom,
( ~ lives(ukranian,H)
| ~ lives(norwegian,H)
| ~ house(H) ),
file('theBenchmark.p',norwegian_and_ukranian_live_apart) ).
cnf(norwegian_and_japanese_live_apart,axiom,
( ~ lives(japanese,H)
| ~ lives(norwegian,H)
| ~ house(H) ),
file('theBenchmark.p',norwegian_and_japanese_live_apart) ).
cnf(ukranian_and_japanese_live_apart,axiom,
( ~ lives(japanese,H)
| ~ lives(ukranian,H)
| ~ house(H) ),
file('theBenchmark.p',ukranian_and_japanese_live_apart) ).
cnf(drink_something,axiom,
( drinks(Person,water)
| drinks(Person,milk)
| drinks(Person,tea)
| drinks(Person,coffee)
| drinks(Person,orange)
| ~ person(Person) ),
file('theBenchmark.p',drink_something) ).
cnf(english_and_spaniard_drink_different,axiom,
( ~ drinks(spaniard,H)
| ~ drinks(english,H)
| ~ drink(H) ),
file('theBenchmark.p',english_and_spaniard_drink_different) ).
cnf(english_and_norwegian_drink_different,axiom,
( ~ drinks(norwegian,H)
| ~ drinks(english,H)
| ~ drink(H) ),
file('theBenchmark.p',english_and_norwegian_drink_different) ).
cnf(english_and_unkranian_drink_different,axiom,
( ~ drinks(ukranian,H)
| ~ drinks(english,H)
| ~ drink(H) ),
file('theBenchmark.p',english_and_unkranian_drink_different) ).
cnf(english_and_japanese_drink_different,axiom,
( ~ drinks(japanese,H)
| ~ drinks(english,H)
| ~ drink(H) ),
file('theBenchmark.p',english_and_japanese_drink_different) ).
cnf(spaniard_and_norwegian_drink_different,axiom,
( ~ drinks(norwegian,H)
| ~ drinks(spaniard,H)
| ~ drink(H) ),
file('theBenchmark.p',spaniard_and_norwegian_drink_different) ).
cnf(spaniard_and_ukranian_drink_different,axiom,
( ~ drinks(ukranian,H)
| ~ drinks(spaniard,H)
| ~ drink(H) ),
file('theBenchmark.p',spaniard_and_ukranian_drink_different) ).
cnf(spaniard_and_japanese_drink_different,axiom,
( ~ drinks(japanese,H)
| ~ drinks(spaniard,H)
| ~ drink(H) ),
file('theBenchmark.p',spaniard_and_japanese_drink_different) ).
cnf(norwegian_and_ukranian_drink_different,axiom,
( ~ drinks(ukranian,H)
| ~ drinks(norwegian,H)
| ~ drink(H) ),
file('theBenchmark.p',norwegian_and_ukranian_drink_different) ).
cnf(norwegian_and_japanese_drink_different,axiom,
( ~ drinks(japanese,H)
| ~ drinks(norwegian,H)
| ~ drink(H) ),
file('theBenchmark.p',norwegian_and_japanese_drink_different) ).
cnf(ukranian_and_japanese_drink_different,axiom,
( ~ drinks(japanese,H)
| ~ drinks(ukranian,H)
| ~ drink(H) ),
file('theBenchmark.p',ukranian_and_japanese_drink_different) ).
cnf(drive_something,axiom,
( drives(Person,jaguar)
| drives(Person,honda)
| drives(Person,porsche)
| drives(Person,saab)
| drives(Person,masserati)
| ~ person(Person) ),
file('theBenchmark.p',drive_something) ).
cnf(english_and_spaniard_drive_different,axiom,
( ~ drives(spaniard,H)
| ~ drives(english,H)
| ~ car(H) ),
file('theBenchmark.p',english_and_spaniard_drive_different) ).
cnf(english_and_norwegian_drive_different,axiom,
( ~ drives(norwegian,H)
| ~ drives(english,H)
| ~ car(H) ),
file('theBenchmark.p',english_and_norwegian_drive_different) ).
cnf(english_and_ukranian_drive_different,axiom,
( ~ drives(ukranian,H)
| ~ drives(english,H)
| ~ car(H) ),
file('theBenchmark.p',english_and_ukranian_drive_different) ).
cnf(english_and_japanese_drive_different,axiom,
( ~ drives(japanese,H)
| ~ drives(english,H)
| ~ car(H) ),
file('theBenchmark.p',english_and_japanese_drive_different) ).
cnf(spaniard_and_norwegian_drive_different,axiom,
( ~ drives(norwegian,H)
| ~ drives(spaniard,H)
| ~ car(H) ),
file('theBenchmark.p',spaniard_and_norwegian_drive_different) ).
cnf(spaniard_and_ukranian_drive_different,axiom,
( ~ drives(ukranian,H)
| ~ drives(spaniard,H)
| ~ car(H) ),
file('theBenchmark.p',spaniard_and_ukranian_drive_different) ).
cnf(spaniard_and_japanese_drive_different,axiom,
( ~ drives(japanese,H)
| ~ drives(spaniard,H)
| ~ car(H) ),
file('theBenchmark.p',spaniard_and_japanese_drive_different) ).
cnf(norwegian_and_ukranian_drive_different,axiom,
( ~ drives(ukranian,H)
| ~ drives(norwegian,H)
| ~ car(H) ),
file('theBenchmark.p',norwegian_and_ukranian_drive_different) ).
cnf(norwegian_and_japanese_drive_different,axiom,
( ~ drives(japanese,H)
| ~ drives(norwegian,H)
| ~ car(H) ),
file('theBenchmark.p',norwegian_and_japanese_drive_different) ).
cnf(ukranian_and_japanese_drive_different,axiom,
( ~ drives(japanese,H)
| ~ drives(ukranian,H)
| ~ car(H) ),
file('theBenchmark.p',ukranian_and_japanese_drive_different) ).
cnf(own_a_pet,axiom,
( owns(Person,zebra)
| owns(Person,fox)
| owns(Person,horse)
| owns(Person,snails)
| owns(Person,dog)
| ~ person(Person) ),
file('theBenchmark.p',own_a_pet) ).
cnf(english_and_spaniard_own_different_pets,axiom,
( ~ owns(spaniard,H)
| ~ owns(english,H)
| ~ animal(H) ),
file('theBenchmark.p',english_and_spaniard_own_different_pets) ).
cnf(english_and_norwegian_own_different_pets,axiom,
( ~ owns(norwegian,H)
| ~ owns(english,H)
| ~ animal(H) ),
file('theBenchmark.p',english_and_norwegian_own_different_pets) ).
cnf(english_and_ukranian_own_different_pets,axiom,
( ~ owns(ukranian,H)
| ~ owns(english,H)
| ~ animal(H) ),
file('theBenchmark.p',english_and_ukranian_own_different_pets) ).
cnf(english_and_japanese_own_different_pets,axiom,
( ~ owns(japanese,H)
| ~ owns(english,H)
| ~ animal(H) ),
file('theBenchmark.p',english_and_japanese_own_different_pets) ).
cnf(spaniard_and_norwegian_own_different_pets,axiom,
( ~ owns(norwegian,H)
| ~ owns(spaniard,H)
| ~ animal(H) ),
file('theBenchmark.p',spaniard_and_norwegian_own_different_pets) ).
cnf(spaniard_and_ukranian_own_different_pets,axiom,
( ~ owns(ukranian,H)
| ~ owns(spaniard,H)
| ~ animal(H) ),
file('theBenchmark.p',spaniard_and_ukranian_own_different_pets) ).
cnf(spaniard_and_japanese_own_different_pets,axiom,
( ~ owns(japanese,H)
| ~ owns(spaniard,H)
| ~ animal(H) ),
file('theBenchmark.p',spaniard_and_japanese_own_different_pets) ).
cnf(norwegian_and_ukranian_own_different_pets,axiom,
( ~ owns(ukranian,H)
| ~ owns(norwegian,H)
| ~ animal(H) ),
file('theBenchmark.p',norwegian_and_ukranian_own_different_pets) ).
cnf(norwegian_and_japanese_own_different_pets,axiom,
( ~ owns(japanese,H)
| ~ owns(norwegian,H)
| ~ animal(H) ),
file('theBenchmark.p',norwegian_and_japanese_own_different_pets) ).
cnf(ukranian_and_japanese_own_different_pets,axiom,
( ~ owns(japanese,H)
| ~ owns(ukranian,H)
| ~ animal(H) ),
file('theBenchmark.p',ukranian_and_japanese_own_different_pets) ).
cnf(house_coloured,axiom,
( is_color(H,ivory)
| is_color(H,green)
| is_color(H,blue)
| is_color(H,yellow)
| is_color(H,red)
| ~ house(H) ),
file('theBenchmark.p',house_coloured) ).
cnf(houses_1_and_2_coloured_different,axiom,
( ~ is_color(house_2,H)
| ~ is_color(house_1,H)
| ~ color(H) ),
file('theBenchmark.p',houses_1_and_2_coloured_different) ).
cnf(houses_1_and_3_coloured_different,axiom,
( ~ is_color(house_3,H)
| ~ is_color(house_1,H)
| ~ color(H) ),
file('theBenchmark.p',houses_1_and_3_coloured_different) ).
cnf(houses_1_and_4_coloured_different,axiom,
( ~ is_color(house_4,H)
| ~ is_color(house_1,H)
| ~ color(H) ),
file('theBenchmark.p',houses_1_and_4_coloured_different) ).
cnf(houses_1_and_5_coloured_different,axiom,
( ~ is_color(house_5,H)
| ~ is_color(house_1,H)
| ~ color(H) ),
file('theBenchmark.p',houses_1_and_5_coloured_different) ).
cnf(houses_2_and_3_coloured_different,axiom,
( ~ is_color(house_3,H)
| ~ is_color(house_2,H)
| ~ color(H) ),
file('theBenchmark.p',houses_2_and_3_coloured_different) ).
cnf(houses_2_and_4_coloured_different,axiom,
( ~ is_color(house_4,H)
| ~ is_color(house_2,H)
| ~ color(H) ),
file('theBenchmark.p',houses_2_and_4_coloured_different) ).
cnf(houses_2_and_5_coloured_different,axiom,
( ~ is_color(house_5,H)
| ~ is_color(house_2,H)
| ~ color(H) ),
file('theBenchmark.p',houses_2_and_5_coloured_different) ).
cnf(houses_3_and_4_coloured_different,axiom,
( ~ is_color(house_4,H)
| ~ is_color(house_3,H)
| ~ color(H) ),
file('theBenchmark.p',houses_3_and_4_coloured_different) ).
cnf(houses_3_and_5_coloured_different,axiom,
( ~ is_color(house_5,H)
| ~ is_color(house_3,H)
| ~ color(H) ),
file('theBenchmark.p',houses_3_and_5_coloured_different) ).
cnf(houses_4_and_5_coloured_different,axiom,
( ~ is_color(house_5,H)
| ~ is_color(house_4,H)
| ~ color(H) ),
file('theBenchmark.p',houses_4_and_5_coloured_different) ).
cnf(english,axiom,
person(english),
file('theBenchmark.p',english) ).
cnf(spaniard,axiom,
person(spaniard),
file('theBenchmark.p',spaniard) ).
cnf(norwegian,axiom,
person(norwegian),
file('theBenchmark.p',norwegian) ).
cnf(ukranian,axiom,
person(ukranian),
file('theBenchmark.p',ukranian) ).
cnf(japanese,axiom,
person(japanese),
file('theBenchmark.p',japanese) ).
cnf(house_house_1,axiom,
house(house_1),
file('theBenchmark.p',house_house_1) ).
cnf(house_house_2,axiom,
house(house_2),
file('theBenchmark.p',house_house_2) ).
cnf(house_house_3,axiom,
house(house_3),
file('theBenchmark.p',house_house_3) ).
cnf(house_house_4,axiom,
house(house_4),
file('theBenchmark.p',house_house_4) ).
cnf(house_house_5,axiom,
house(house_5),
file('theBenchmark.p',house_house_5) ).
cnf(red,axiom,
color(red),
file('theBenchmark.p',red) ).
cnf(green,axiom,
color(green),
file('theBenchmark.p',green) ).
cnf(yellow,axiom,
color(yellow),
file('theBenchmark.p',yellow) ).
cnf(ivory,axiom,
color(ivory),
file('theBenchmark.p',ivory) ).
cnf(blue,axiom,
color(blue),
file('theBenchmark.p',blue) ).
cnf(jaguar,axiom,
car(jaguar),
file('theBenchmark.p',jaguar) ).
cnf(honda,axiom,
car(honda),
file('theBenchmark.p',honda) ).
cnf(masserati,axiom,
car(masserati),
file('theBenchmark.p',masserati) ).
cnf(porsche,axiom,
car(porsche),
file('theBenchmark.p',porsche) ).
cnf(saab,axiom,
car(saab),
file('theBenchmark.p',saab) ).
cnf(tea,axiom,
drink(tea),
file('theBenchmark.p',tea) ).
cnf(orange,axiom,
drink(orange),
file('theBenchmark.p',orange) ).
cnf(water,axiom,
drink(water),
file('theBenchmark.p',water) ).
cnf(milk,axiom,
drink(milk),
file('theBenchmark.p',milk) ).
cnf(coffee,axiom,
drink(coffee),
file('theBenchmark.p',coffee) ).
cnf(dog,axiom,
animal(dog),
file('theBenchmark.p',dog) ).
cnf(zebra,axiom,
animal(zebra),
file('theBenchmark.p',zebra) ).
cnf(snails,axiom,
animal(snails),
file('theBenchmark.p',snails) ).
cnf(horse,axiom,
animal(horse),
file('theBenchmark.p',horse) ).
cnf(fox,axiom,
animal(fox),
file('theBenchmark.p',fox) ).
cnf(english_in_red_house,axiom,
( ~ lives(english,H)
| ~ house(H)
| is_color(H,red) ),
file('theBenchmark.p',english_in_red_house) ).
cnf(spaniard_owns_dog,axiom,
owns(spaniard,dog),
file('theBenchmark.p',spaniard_owns_dog) ).
cnf(norwegian_in_house_house_1,axiom,
lives(norwegian,house_1),
file('theBenchmark.p',norwegian_in_house_house_1) ).
cnf(masserati_in_yellow_house,axiom,
( ~ lives(Person,H)
| ~ house(H)
| ~ drives(Person,masserati)
| ~ person(Person)
| is_color(H,yellow) ),
file('theBenchmark.p',masserati_in_yellow_house) ).
cnf(saab_with_fox,axiom,
( ~ lives(Person_2,House_2)
| ~ house(House_2)
| ~ drives(Person_2,saab)
| ~ person(Person_2)
| ~ lives(Person_1,House_1)
| ~ house(House_1)
| ~ owns(Person_1,fox)
| ~ person(Person_1)
| next_to(House_1,House_2) ),
file('theBenchmark.p',saab_with_fox) ).
cnf(norwegian_in_blue_house,axiom,
( ~ next_to(House_1,House_2)
| ~ house(House_2)
| ~ lives(norwegian,House_1)
| ~ house(House_1)
| is_color(House_2,blue) ),
file('theBenchmark.p',norwegian_in_blue_house) ).
cnf(porsche_with_snails,axiom,
( ~ drives(P,porsche)
| ~ person(P)
| owns(P,snails) ),
file('theBenchmark.p',porsche_with_snails) ).
cnf(honda_with_orange,axiom,
( ~ drives(P,honda)
| ~ person(P)
| drinks(P,orange) ),
file('theBenchmark.p',honda_with_orange) ).
cnf(ukranian_drinks_tea,axiom,
drinks(ukranian,tea),
file('theBenchmark.p',ukranian_drinks_tea) ).
cnf(japanese_drives_jaguar,axiom,
drives(japanese,jaguar),
file('theBenchmark.p',japanese_drives_jaguar) ).
cnf(masserati_next_to_horse,axiom,
( ~ lives(Person_2,House_2)
| ~ house(House_2)
| ~ owns(Person_2,horse)
| ~ person(Person_2)
| ~ lives(Person_1,House_1)
| ~ house(House_1)
| ~ drives(Person_1,masserati)
| ~ person(Person_1)
| next_to(House_1,House_2) ),
file('theBenchmark.p',masserati_next_to_horse) ).
cnf(coffee_in_green_house,axiom,
( ~ lives(P,H)
| ~ house(H)
| ~ drinks(P,coffee)
| ~ person(P)
| is_color(H,green) ),
file('theBenchmark.p',coffee_in_green_house) ).
cnf(green_right_of_ivory,axiom,
( ~ is_color(House_2,ivory)
| ~ house(House_2)
| ~ is_color(House_1,green)
| ~ house(House_1)
| left_of(House_2,House_1) ),
file('theBenchmark.p',green_right_of_ivory) ).
cnf(milk_in_middle,axiom,
( ~ drinks(P,milk)
| ~ person(P)
| lives(P,house_3) ),
file('theBenchmark.p',milk_in_middle) ).
cnf(left_means_next_to,axiom,
( ~ left_of(X,Y)
| next_to(X,Y) ),
file('theBenchmark.p',left_means_next_to) ).
cnf(right_mean_next_to,axiom,
( ~ left_of(Y,X)
| next_to(X,Y) ),
file('theBenchmark.p',right_mean_next_to) ).
cnf(next_to_means_left_or_right,axiom,
( left_of(Y,X)
| ~ next_to(X,Y)
| left_of(X,Y) ),
file('theBenchmark.p',next_to_means_left_or_right) ).
cnf(house_1_left_of_house_2,axiom,
left_of(house_1,house_2),
file('theBenchmark.p',house_1_left_of_house_2) ).
cnf(house_2_left_of_house_3,axiom,
left_of(house_2,house_3),
file('theBenchmark.p',house_2_left_of_house_3) ).
cnf(house_3_left_of_house_4,axiom,
left_of(house_3,house_4),
file('theBenchmark.p',house_3_left_of_house_4) ).
cnf(house_4_left_of_house_5,axiom,
left_of(house_4,house_5),
file('theBenchmark.p',house_4_left_of_house_5) ).
cnf(house_1_not_left_of_house_1,axiom,
~ left_of(house_1,house_1),
file('theBenchmark.p',house_1_not_left_of_house_1) ).
cnf(house_2_not_left_of_house_1,axiom,
~ left_of(house_2,house_1),
file('theBenchmark.p',house_2_not_left_of_house_1) ).
cnf(house_3_not_left_of_house_1,axiom,
~ left_of(house_3,house_1),
file('theBenchmark.p',house_3_not_left_of_house_1) ).
cnf(house_4_not_left_of_house_1,axiom,
~ left_of(house_4,house_1),
file('theBenchmark.p',house_4_not_left_of_house_1) ).
cnf(house_5_not_left_of_house_1,axiom,
~ left_of(house_5,house_1),
file('theBenchmark.p',house_5_not_left_of_house_1) ).
cnf(house_2_not_left_of_house_2,axiom,
~ left_of(house_2,house_2),
file('theBenchmark.p',house_2_not_left_of_house_2) ).
cnf(house_3_not_left_of_house_2,axiom,
~ left_of(house_3,house_2),
file('theBenchmark.p',house_3_not_left_of_house_2) ).
cnf(house_4_not_left_of_house_2,axiom,
~ left_of(house_4,house_2),
file('theBenchmark.p',house_4_not_left_of_house_2) ).
cnf(house_5_not_left_of_house_2,axiom,
~ left_of(house_5,house_2),
file('theBenchmark.p',house_5_not_left_of_house_2) ).
cnf(house_1_not_left_of_house_3,axiom,
~ left_of(house_1,house_3),
file('theBenchmark.p',house_1_not_left_of_house_3) ).
cnf(house_3_not_left_of_house_3,axiom,
~ left_of(house_3,house_3),
file('theBenchmark.p',house_3_not_left_of_house_3) ).
cnf(house_4_not_left_of_house_3,axiom,
~ left_of(house_4,house_3),
file('theBenchmark.p',house_4_not_left_of_house_3) ).
cnf(house_5_not_left_of_house_3,axiom,
~ left_of(house_5,house_3),
file('theBenchmark.p',house_5_not_left_of_house_3) ).
cnf(house_1_not_left_of_house_4,axiom,
~ left_of(house_1,house_4),
file('theBenchmark.p',house_1_not_left_of_house_4) ).
cnf(house_2_not_left_of_house_4,axiom,
~ left_of(house_2,house_4),
file('theBenchmark.p',house_2_not_left_of_house_4) ).
cnf(house_4_not_left_of_house_4,axiom,
~ left_of(house_4,house_4),
file('theBenchmark.p',house_4_not_left_of_house_4) ).
cnf(house_5_not_left_of_house_4,axiom,
~ left_of(house_5,house_4),
file('theBenchmark.p',house_5_not_left_of_house_4) ).
cnf(house_1_not_left_of_house_5,axiom,
~ left_of(house_1,house_5),
file('theBenchmark.p',house_1_not_left_of_house_5) ).
cnf(house_2_not_left_of_house_5,axiom,
~ left_of(house_2,house_5),
file('theBenchmark.p',house_2_not_left_of_house_5) ).
cnf(house_3_not_left_of_house_5,axiom,
~ left_of(house_3,house_5),
file('theBenchmark.p',house_3_not_left_of_house_5) ).
cnf(house_5_not_left_of_house_5,axiom,
~ left_of(house_5,house_5),
file('theBenchmark.p',house_5_not_left_of_house_5) ).
cnf(prove_configuration,negated_conjecture,
( ~ is_color(house_5,green)
| ~ is_color(house_4,ivory)
| ~ is_color(house_3,red)
| ~ is_color(house_2,blue)
| ~ is_color(house_1,yellow)
| ~ lives(spaniard,house_4)
| ~ lives(english,house_3)
| ~ lives(japanese,house_5)
| ~ lives(ukranian,house_2)
| ~ lives(norwegian,house_1)
| ~ drives(spaniard,honda)
| ~ drives(english,porsche)
| ~ drives(japanese,jaguar)
| ~ drives(ukranian,saab)
| ~ drives(norwegian,masserati)
| ~ owns(spaniard,dog)
| ~ owns(english,snails)
| ~ owns(japanese,zebra)
| ~ owns(ukranian,horse)
| ~ owns(norwegian,fox)
| ~ drinks(spaniard,orange)
| ~ drinks(english,milk)
| ~ drinks(japanese,coffee)
| ~ drinks(ukranian,tea)
| ~ drinks(norwegian,water) ),
file('theBenchmark.p',prove_configuration) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ010-1 : TPTP v9.3.1. Bugfixed v1.0.1.
% 0.00/0.03 This is a CNF_UNS_EPR_NEQ_NHN problem
% 0.00/0.04 % Command : /export/starexec/sandbox/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.11/0.37 % Computer : n009.cluster.edu
% 0.11/0.37 % Model : x86_64 x86_64
% 0.11/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.37 % Memory : 8046.5625MB
% 0.11/0.37 % OS : Linux 6.8.0-71-generic
% 0.11/0.38 % CPULimit : 300
% 0.11/0.38 % WCLimit : 300
% 0.11/0.38 % DateTime : Sat Sep 19 19:55:12 UTC 2026
% 0.11/0.38 % CPUTime :
% 183.03/183.38 % SZS status Unsatisfiable for theBenchmark
% 183.03/183.38 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------