%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : PUZ017-1 : TPTP v9.2.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n026.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 : Tue May 5 05:02:29 PM UTC 2026
% Result : Unsatisfiable 11.61s 9.13s
% Output : CNFRefutation 11.61s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats ran out of CPU time)
% Comments :
%------------------------------------------------------------------------------
cnf(c20,hypothesis,
( hascolor(X2,blue)
| ~ hasperson(X1,russian)
| ~ samehouse(n1,X1)
| ~ nextto(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c20) ).
cnf(house_1_has_russian,hypothesis,
hasperson(n1,russian),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_1_has_russian) ).
cnf(reflexivity_for_samehouse,axiom,
samehouse(X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_for_samehouse) ).
cnf(left_means_nextto,axiom,
( nextto(X1,X2)
| ~ left(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',left_means_nextto) ).
cnf(house_1_left_of_2,hypothesis,
left(n1,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_1_left_of_2) ).
cnf(houses_have_unique_nationals,axiom,
( sameperson(X1,X2)
| ~ hasperson(X3,X1)
| ~ hasperson(X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',houses_have_unique_nationals) ).
cnf(colours_are_unique,axiom,
( samecolor(X1,X2)
| ~ hascolor(X3,X1)
| ~ hascolor(X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',colours_are_unique) ).
cnf(houses_have_unique_colors,axiom,
( samehouse(X1,X2)
| ~ hascolor(X1,X3)
| ~ hascolor(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',houses_have_unique_colors) ).
cnf(racquetball_played_in_yellow_house1,hypothesis,
( hascolor(X1,yellow)
| ~ hasgame(X1,racquetball) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',racquetball_played_in_yellow_house1) ).
cnf(englishman_not_russian,axiom,
~ sameperson(englishman,russian),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',englishman_not_russian) ).
cnf(green_not_blue,axiom,
~ samecolor(green,blue),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',green_not_blue) ).
cnf(white_house_left_of_green2,hypothesis,
( hascolor(X2,green)
| ~ hascolor(X1,white)
| ~ left(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',white_house_left_of_green2) ).
cnf(yellow_not_blue,axiom,
~ samecolor(yellow,blue),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',yellow_not_blue) ).
cnf(house_1_not_5,axiom,
~ samehouse(n1,n5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_1_not_5) ).
cnf(englishman_lives_in_red_house2,hypothesis,
( hasperson(X1,englishman)
| ~ hascolor(X1,red) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',englishman_lives_in_red_house2) ).
cnf(house_1_not_2,axiom,
~ samehouse(n1,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_1_not_2) ).
cnf(house_1_not_4,axiom,
~ samehouse(n1,n4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_1_not_4) ).
cnf(racquetball_played_in_yellow_house2,hypothesis,
( hasgame(X1,racquetball)
| ~ hascolor(X1,yellow) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',racquetball_played_in_yellow_house2) ).
cnf(every_color_is_used,axiom,
( hascolor(n1,X1)
| hascolor(n2,X1)
| hascolor(n3,X1)
| hascolor(n4,X1)
| hascolor(n5,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_color_is_used) ).
cnf(house1_at_left,hypothesis,
~ left(X1,n1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house1_at_left) ).
cnf(white_house_left_of_green1,hypothesis,
( left(X1,X2)
| ~ hascolor(X1,white)
| ~ hascolor(X2,green) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',white_house_left_of_green1) ).
cnf(every_house_has_color,axiom,
( hascolor(X1,red)
| hascolor(X1,white)
| hascolor(X1,green)
| hascolor(X1,yellow)
| hascolor(X1,blue) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_house_has_color) ).
cnf(house_1_not_3,axiom,
~ samehouse(n1,n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_1_not_3) ).
cnf(englishman_lives_in_red_house1,hypothesis,
( hascolor(X1,red)
| ~ hasperson(X1,englishman) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',englishman_lives_in_red_house1) ).
cnf(every_natioality_is_used,axiom,
( hasperson(n1,X1)
| hasperson(n2,X1)
| hasperson(n3,X1)
| hasperson(n4,X1)
| hasperson(n5,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_natioality_is_used) ).
cnf(red_not_blue,axiom,
~ samecolor(red,blue),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',red_not_blue) ).
cnf(white_not_blue,axiom,
~ samecolor(white,blue),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',white_not_blue) ).
cnf(house_3_left_of_4,hypothesis,
left(n3,n4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_3_left_of_4) ).
cnf(houses_have_unique_drinks,axiom,
( samedrink(X1,X2)
| ~ hasdrink(X3,X1)
| ~ hasdrink(X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',houses_have_unique_drinks) ).
cnf(house_3_has_milk,hypothesis,
hasdrink(n3,milk),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_3_has_milk) ).
cnf(white_house_left_of_green3,hypothesis,
( hascolor(X1,white)
| ~ hascolor(X2,green)
| ~ left(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',white_house_left_of_green3) ).
cnf(house_4_left_of_5,hypothesis,
left(n4,n5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_4_left_of_5) ).
cnf(symmetry_of_nextto,axiom,
( nextto(X2,X1)
| ~ nextto(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',symmetry_of_nextto) ).
cnf(c11,hypothesis,
( nextto(X1,X2)
| ~ haspet(X1,rat)
| ~ hasgame(X2,racquetball) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c11) ).
cnf(lemonade_not_milk,axiom,
~ samedrink(lemonade,milk),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lemonade_not_milk) ).
cnf(house_1_not_nextto_4,hypothesis,
~ nextto(n1,n4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_1_not_nextto_4) ).
cnf(house_1_not_nextto_5,hypothesis,
~ nextto(n1,n5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_1_not_nextto_5) ).
cnf(house_1_not_nextto_3,hypothesis,
~ nextto(n1,n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_1_not_nextto_3) ).
cnf(nothing_nextto_itself,axiom,
~ nextto(X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nothing_nextto_itself) ).
cnf(red_not_green,axiom,
~ samecolor(red,green),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',red_not_green) ).
cnf(lemonade_in_green_house2,hypothesis,
( hasdrink(X1,lemonade)
| ~ hascolor(X1,green) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lemonade_in_green_house2) ).
cnf(red_not_white,axiom,
~ samecolor(red,white),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',red_not_white) ).
cnf(every_pet_is_used,axiom,
( haspet(n1,X1)
| haspet(n2,X1)
| haspet(n3,X1)
| haspet(n4,X1)
| haspet(n5,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_pet_is_used) ).
cnf(houses_have_unique_pets,axiom,
( samepet(X1,X2)
| ~ haspet(X3,X1)
| ~ haspet(X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',houses_have_unique_pets) ).
cnf(every_game_is_used,axiom,
( hasgame(n1,X1)
| hasgame(n2,X1)
| hasgame(n3,X1)
| hasgame(n4,X1)
| hasgame(n5,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_game_is_used) ).
cnf(italian_not_russian,axiom,
~ sameperson(italian,russian),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',italian_not_russian) ).
cnf(nationals_have_unique_houses,axiom,
( samehouse(X1,X2)
| ~ hasperson(X1,X3)
| ~ hasperson(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nationals_have_unique_houses) ).
cnf(green_not_yellow,axiom,
~ samecolor(green,yellow),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',green_not_yellow) ).
cnf(toad_not_rat,axiom,
~ samepet(toad,rat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',toad_not_rat) ).
cnf(italian_has_guppy1,hypothesis,
( haspet(X1,guppy)
| ~ hasperson(X1,italian) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',italian_has_guppy1) ).
cnf(house_not_nextto_itself,axiom,
( ~ samehouse(X1,X2)
| ~ nextto(X1,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_not_nextto_itself) ).
cnf(toad_lives_with_backgammon1,hypothesis,
( hasgame(X1,backgammon)
| ~ haspet(X1,toad) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',toad_lives_with_backgammon1) ).
cnf(guppy_not_rat,axiom,
~ samepet(guppy,rat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',guppy_not_rat) ).
cnf(house_4_not_5,axiom,
~ samehouse(n4,n5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_4_not_5) ).
cnf(house_2_left_of_3,hypothesis,
left(n2,n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_2_left_of_3) ).
cnf(pets_have_unique_houses,axiom,
( samehouse(X1,X2)
| ~ haspet(X1,X3)
| ~ haspet(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',pets_have_unique_houses) ).
cnf(houses_have_unique_games,axiom,
( samegame(X1,X2)
| ~ hasgame(X3,X1)
| ~ hasgame(X3,X2) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',houses_have_unique_games) ).
cnf(nothing_left_of_itself,axiom,
~ left(X1,X1),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nothing_left_of_itself) ).
cnf(house_3_not_5,axiom,
~ samehouse(n3,n5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_3_not_5) ).
cnf(c18,hypothesis,
( hasperson(X1,american)
| ~ hasgame(X1,charades) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c18) ).
cnf(backgammon_not_recquetball,axiom,
~ samegame(backgammon,racquetball),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',backgammon_not_recquetball) ).
cnf(every_house_has_a_game,axiom,
( hasgame(X1,backgammon)
| hasgame(X1,racquetball)
| hasgame(X1,quoits)
| hasgame(X1,solitaire)
| hasgame(X1,charades) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_house_has_a_game) ).
cnf(coffee_not_milk,axiom,
~ samedrink(coffee,milk),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',coffee_not_milk) ).
cnf(toad_lives_with_backgammon2,hypothesis,
( haspet(X1,toad)
| ~ hasgame(X1,backgammon) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',toad_lives_with_backgammon2) ).
cnf(every_house_has_a_pet,axiom,
( haspet(X1,guppy)
| haspet(X1,toad)
| haspet(X1,camel)
| haspet(X1,rat)
| haspet(X1,no_pet) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_house_has_a_pet) ).
cnf(englishman_not_italian,axiom,
~ sameperson(englishman,italian),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',englishman_not_italian) ).
cnf(englishman_not_american,axiom,
~ sameperson(englishman,american),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',englishman_not_american) ).
cnf(swede_drinks_coffee1,hypothesis,
( hasdrink(X1,coffee)
| ~ hasperson(X1,swede) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',swede_drinks_coffee1) ).
cnf(swede_not_russian,axiom,
~ sameperson(swede,russian),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',swede_not_russian) ).
cnf(italian_has_guppy2,hypothesis,
( hasperson(X1,italian)
| ~ haspet(X1,guppy) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',italian_has_guppy2) ).
cnf(swede_drinks_coffee2,hypothesis,
( hasperson(X1,swede)
| ~ hasdrink(X1,coffee) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',swede_drinks_coffee2) ).
cnf(every_drink_is_used,axiom,
( hasdrink(n1,X1)
| hasdrink(n2,X1)
| hasdrink(n3,X1)
| hasdrink(n4,X1)
| hasdrink(n5,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_drink_is_used) ).
cnf(italian_not_american,axiom,
~ sameperson(italian,american),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',italian_not_american) ).
cnf(guppy_not_toad,axiom,
~ samepet(guppy,toad),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',guppy_not_toad) ).
cnf(lemonade_not_coffee,axiom,
~ samedrink(lemonade,coffee),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lemonade_not_coffee) ).
cnf(house_3_not_4,axiom,
~ samehouse(n3,n4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_3_not_4) ).
cnf(c15,hypothesis,
( hasdrink(X1,vodka)
| ~ hasgame(X1,solitaire) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c15) ).
cnf(c4,hypothesis,
( nextto(X1,X2)
| ~ haspet(X1,camel)
| ~ hasgame(X2,quoits) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c4) ).
cnf(house_2_not_4,axiom,
~ samehouse(n2,n4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_2_not_4) ).
cnf(house_3_not_nextto_5,hypothesis,
~ nextto(n3,n5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_3_not_nextto_5) ).
cnf(milk_not_vodka,axiom,
~ samedrink(milk,vodka),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',milk_not_vodka) ).
cnf(swede_not_american,axiom,
~ sameperson(swede,american),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',swede_not_american) ).
cnf(italian_not_swede,axiom,
~ sameperson(italian,swede),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',italian_not_swede) ).
cnf(englishman_not_swede,axiom,
~ sameperson(englishman,swede),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',englishman_not_swede) ).
cnf(coffee_not_vodka,axiom,
~ samedrink(coffee,vodka),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',coffee_not_vodka) ).
cnf(house_2_not_nextto_4,hypothesis,
~ nextto(n2,n4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_2_not_nextto_4) ).
cnf(house_2_not_nextto_5,hypothesis,
~ nextto(n2,n5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_2_not_nextto_5) ).
cnf(games_have_unique_houses,axiom,
( samehouse(X1,X2)
| ~ hasgame(X1,X3)
| ~ hasgame(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',games_have_unique_houses) ).
cnf(lemonade_not_vodka,axiom,
~ samedrink(lemonade,vodka),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lemonade_not_vodka) ).
cnf(c17,hypothesis,
( hasgame(X1,charades)
| ~ hasperson(X1,american) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c17) ).
cnf(every_house_has_a_national,axiom,
( hasperson(X1,englishman)
| hasperson(X1,italian)
| hasperson(X1,swede)
| hasperson(X1,russian)
| hasperson(X1,american) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_house_has_a_national) ).
cnf(toad_not_camel,axiom,
~ samepet(toad,camel),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',toad_not_camel) ).
cnf(c16,hypothesis,
( hasgame(X1,solitaire)
| ~ hasdrink(X1,vodka) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c16) ).
cnf(russian_not_american,axiom,
~ sameperson(russian,american),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',russian_not_american) ).
cnf(drinks_have_unique_houses,axiom,
( samehouse(X1,X2)
| ~ hasdrink(X1,X3)
| ~ hasdrink(X2,X3) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',drinks_have_unique_houses) ).
cnf(house_2_not_5,axiom,
~ samehouse(n2,n5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_2_not_5) ).
cnf(lemonade_in_green_house1,hypothesis,
( hascolor(X1,green)
| ~ hasdrink(X1,lemonade) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lemonade_in_green_house1) ).
cnf(find_out_house_details,negated_conjecture,
( ~ hasperson(n1,X1)
| ~ hasperson(n2,X2)
| ~ hasperson(n3,X3)
| ~ hasperson(n4,X4)
| ~ hasperson(n5,X5)
| ~ hascolor(n1,X6)
| ~ hascolor(n2,X7)
| ~ hascolor(n3,X8)
| ~ hascolor(n4,X9)
| ~ hascolor(n5,X10)
| ~ hasdrink(n1,X11)
| ~ hasdrink(n2,X12)
| ~ hasdrink(n3,X13)
| ~ hasdrink(n4,X14)
| ~ hasdrink(n5,X15)
| ~ hasgame(n1,X16)
| ~ hasgame(n2,X17)
| ~ hasgame(n3,X18)
| ~ hasgame(n4,X19)
| ~ hasgame(n5,X20)
| ~ haspet(n1,X21)
| ~ haspet(n2,X22)
| ~ haspet(n3,X23)
| ~ haspet(n4,X24)
| ~ haspet(n5,X25) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',find_out_house_details) ).
cnf(vodka_not_unknown,axiom,
~ samedrink(vodka,unknown_drink),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',vodka_not_unknown) ).
cnf(coffee_not_known,axiom,
~ samedrink(coffee,unknown_drink),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',coffee_not_known) ).
cnf(milk_not_unknown,axiom,
~ samedrink(milk,unknown_drink),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',milk_not_unknown) ).
cnf(lemonade_not_unknown,axiom,
~ samedrink(lemonade,unknown_drink),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lemonade_not_unknown) ).
cnf(every_house_has_a_drink,axiom,
( hasdrink(X1,lemonade)
| hasdrink(X1,coffee)
| hasdrink(X1,milk)
| hasdrink(X1,vodka)
| hasdrink(X1,unknown_drink) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_house_has_a_drink) ).
cnf(c_0_103,hypothesis,
( hascolor(X2,blue)
| ~ hasperson(X1,russian)
| ~ samehouse(n1,X1)
| ~ nextto(X1,X2) ),
c20 ).
cnf(c_0_104,hypothesis,
hasperson(n1,russian),
house_1_has_russian ).
cnf(c_0_105,axiom,
samehouse(X1,X1),
reflexivity_for_samehouse ).
cnf(c_0_106,axiom,
( nextto(X1,X2)
| ~ left(X1,X2) ),
left_means_nextto ).
cnf(c_0_107,hypothesis,
left(n1,n2),
house_1_left_of_2 ).
cnf(c_0_108,hypothesis,
( hascolor(X1,blue)
| ~ nextto(n1,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_103,c_0_104]),c_0_105])]) ).
cnf(c_0_109,hypothesis,
nextto(n1,n2),
inference(spm,[status(thm)],[c_0_106,c_0_107]) ).
cnf(c_0_110,axiom,
( sameperson(X1,X2)
| ~ hasperson(X3,X1)
| ~ hasperson(X3,X2) ),
houses_have_unique_nationals ).
cnf(c_0_111,axiom,
( samecolor(X1,X2)
| ~ hascolor(X3,X1)
| ~ hascolor(X3,X2) ),
colours_are_unique ).
cnf(c_0_112,hypothesis,
hascolor(n2,blue),
inference(spm,[status(thm)],[c_0_108,c_0_109]) ).
cnf(c_0_113,axiom,
( samehouse(X1,X2)
| ~ hascolor(X1,X3)
| ~ hascolor(X2,X3) ),
houses_have_unique_colors ).
cnf(c_0_114,hypothesis,
( hascolor(X1,yellow)
| ~ hasgame(X1,racquetball) ),
racquetball_played_in_yellow_house1 ).
cnf(c_0_115,axiom,
~ sameperson(englishman,russian),
englishman_not_russian ).
cnf(c_0_116,hypothesis,
( sameperson(X1,russian)
| ~ hasperson(n1,X1) ),
inference(spm,[status(thm)],[c_0_110,c_0_104]) ).
cnf(c_0_117,axiom,
~ samecolor(green,blue),
green_not_blue ).
cnf(c_0_118,hypothesis,
( samecolor(X1,blue)
| ~ hascolor(n2,X1) ),
inference(spm,[status(thm)],[c_0_111,c_0_112]) ).
cnf(c_0_119,hypothesis,
( hascolor(X2,green)
| ~ hascolor(X1,white)
| ~ left(X1,X2) ),
white_house_left_of_green2 ).
cnf(c_0_120,axiom,
~ samecolor(yellow,blue),
yellow_not_blue ).
cnf(c_0_121,axiom,
~ samehouse(n1,n5),
house_1_not_5 ).
cnf(c_0_122,hypothesis,
( samehouse(X1,X2)
| ~ hasgame(X2,racquetball)
| ~ hascolor(X1,yellow) ),
inference(spm,[status(thm)],[c_0_113,c_0_114]) ).
cnf(c_0_123,hypothesis,
~ hasperson(n1,englishman),
inference(spm,[status(thm)],[c_0_115,c_0_116]) ).
cnf(c_0_124,hypothesis,
( hasperson(X1,englishman)
| ~ hascolor(X1,red) ),
englishman_lives_in_red_house2 ).
cnf(c_0_125,hypothesis,
~ hascolor(n2,green),
inference(spm,[status(thm)],[c_0_117,c_0_118]) ).
cnf(c_0_126,hypothesis,
( hascolor(n2,green)
| ~ hascolor(n1,white) ),
inference(spm,[status(thm)],[c_0_119,c_0_107]) ).
cnf(c_0_127,axiom,
~ samehouse(n1,n2),
house_1_not_2 ).
cnf(c_0_128,hypothesis,
( samehouse(X1,n2)
| ~ hascolor(X1,blue) ),
inference(spm,[status(thm)],[c_0_113,c_0_112]) ).
cnf(c_0_129,axiom,
~ samehouse(n1,n4),
house_1_not_4 ).
cnf(c_0_130,hypothesis,
( hasgame(X1,racquetball)
| ~ hascolor(X1,yellow) ),
racquetball_played_in_yellow_house2 ).
cnf(c_0_131,axiom,
( hascolor(n1,X1)
| hascolor(n2,X1)
| hascolor(n3,X1)
| hascolor(n4,X1)
| hascolor(n5,X1) ),
every_color_is_used ).
cnf(c_0_132,hypothesis,
~ hascolor(n2,yellow),
inference(spm,[status(thm)],[c_0_120,c_0_118]) ).
cnf(c_0_133,hypothesis,
~ left(X1,n1),
house1_at_left ).
cnf(c_0_134,hypothesis,
( left(X1,X2)
| ~ hascolor(X1,white)
| ~ hascolor(X2,green) ),
white_house_left_of_green1 ).
cnf(c_0_135,hypothesis,
( ~ hasgame(n5,racquetball)
| ~ hascolor(n1,yellow) ),
inference(spm,[status(thm)],[c_0_121,c_0_122]) ).
cnf(c_0_136,axiom,
( hascolor(X1,red)
| hascolor(X1,white)
| hascolor(X1,green)
| hascolor(X1,yellow)
| hascolor(X1,blue) ),
every_house_has_color ).
cnf(c_0_137,hypothesis,
~ hascolor(n1,red),
inference(spm,[status(thm)],[c_0_123,c_0_124]) ).
cnf(c_0_138,hypothesis,
~ hascolor(n1,white),
inference(spm,[status(thm)],[c_0_125,c_0_126]) ).
cnf(c_0_139,hypothesis,
~ hascolor(n1,blue),
inference(spm,[status(thm)],[c_0_127,c_0_128]) ).
cnf(c_0_140,hypothesis,
( ~ hasgame(n4,racquetball)
| ~ hascolor(n1,yellow) ),
inference(spm,[status(thm)],[c_0_129,c_0_122]) ).
cnf(c_0_141,axiom,
~ samehouse(n1,n3),
house_1_not_3 ).
cnf(c_0_142,hypothesis,
( hascolor(X1,red)
| ~ hasperson(X1,englishman) ),
englishman_lives_in_red_house1 ).
cnf(c_0_143,axiom,
( hasperson(n1,X1)
| hasperson(n2,X1)
| hasperson(n3,X1)
| hasperson(n4,X1)
| hasperson(n5,X1) ),
every_natioality_is_used ).
cnf(c_0_144,axiom,
~ samecolor(red,blue),
red_not_blue ).
cnf(c_0_145,hypothesis,
( hasgame(n4,racquetball)
| hascolor(n5,yellow)
| hascolor(n3,yellow)
| hascolor(n1,yellow) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_130,c_0_131]),c_0_132]) ).
cnf(c_0_146,hypothesis,
( ~ hascolor(n1,green)
| ~ hascolor(X1,white) ),
inference(spm,[status(thm)],[c_0_133,c_0_134]) ).
cnf(c_0_147,hypothesis,
( hascolor(n1,green)
| ~ hasgame(n5,racquetball) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_135,c_0_136]),c_0_137]),c_0_138]),c_0_139]) ).
cnf(c_0_148,axiom,
~ samecolor(white,blue),
white_not_blue ).
cnf(c_0_149,hypothesis,
( hascolor(n1,green)
| ~ hasgame(n4,racquetball) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_140,c_0_136]),c_0_137]),c_0_138]),c_0_139]) ).
cnf(c_0_150,hypothesis,
( ~ hasgame(n3,racquetball)
| ~ hascolor(n1,yellow) ),
inference(spm,[status(thm)],[c_0_141,c_0_122]) ).
cnf(c_0_151,hypothesis,
left(n3,n4),
house_3_left_of_4 ).
cnf(c_0_152,hypothesis,
( hascolor(n4,red)
| hasperson(n5,englishman)
| hasperson(n3,englishman)
| hasperson(n2,englishman) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_142,c_0_143]),c_0_123]) ).
cnf(c_0_153,hypothesis,
~ hascolor(n2,red),
inference(spm,[status(thm)],[c_0_144,c_0_118]) ).
cnf(c_0_154,axiom,
( samedrink(X1,X2)
| ~ hasdrink(X3,X1)
| ~ hasdrink(X3,X2) ),
houses_have_unique_drinks ).
cnf(c_0_155,hypothesis,
hasdrink(n3,milk),
house_3_has_milk ).
cnf(c_0_156,hypothesis,
( hascolor(X1,white)
| ~ hascolor(X2,green)
| ~ left(X1,X2) ),
white_house_left_of_green3 ).
cnf(c_0_157,hypothesis,
left(n4,n5),
house_4_left_of_5 ).
cnf(c_0_158,hypothesis,
( hasgame(n4,racquetball)
| hasgame(n3,racquetball)
| hascolor(n1,yellow)
| hascolor(n5,yellow) ),
inference(spm,[status(thm)],[c_0_130,c_0_145]) ).
cnf(c_0_159,hypothesis,
( ~ hasgame(n5,racquetball)
| ~ hascolor(X1,white) ),
inference(spm,[status(thm)],[c_0_146,c_0_147]) ).
cnf(c_0_160,hypothesis,
~ hascolor(n2,white),
inference(spm,[status(thm)],[c_0_148,c_0_118]) ).
cnf(c_0_161,hypothesis,
( ~ hasgame(n4,racquetball)
| ~ hascolor(X1,white) ),
inference(spm,[status(thm)],[c_0_146,c_0_149]) ).
cnf(c_0_162,hypothesis,
( hascolor(n1,green)
| ~ hasgame(n3,racquetball) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_150,c_0_136]),c_0_137]),c_0_138]),c_0_139]) ).
cnf(c_0_163,axiom,
( nextto(X2,X1)
| ~ nextto(X1,X2) ),
symmetry_of_nextto ).
cnf(c_0_164,hypothesis,
( nextto(X1,X2)
| ~ haspet(X1,rat)
| ~ hasgame(X2,racquetball) ),
c11 ).
cnf(c_0_165,hypothesis,
( hascolor(n4,green)
| ~ hascolor(n3,white) ),
inference(spm,[status(thm)],[c_0_119,c_0_151]) ).
cnf(c_0_166,hypothesis,
( hascolor(n4,red)
| hasperson(n3,englishman)
| hasperson(n5,englishman) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_142,c_0_152]),c_0_153]) ).
cnf(c_0_167,axiom,
~ samedrink(lemonade,milk),
lemonade_not_milk ).
cnf(c_0_168,hypothesis,
( samedrink(X1,milk)
| ~ hasdrink(n3,X1) ),
inference(spm,[status(thm)],[c_0_154,c_0_155]) ).
cnf(c_0_169,hypothesis,
( hascolor(n4,white)
| ~ hascolor(n5,green) ),
inference(spm,[status(thm)],[c_0_156,c_0_157]) ).
cnf(c_0_170,hypothesis,
( hasgame(n3,racquetball)
| hasgame(n4,racquetball)
| hasgame(n5,racquetball)
| hascolor(n1,yellow) ),
inference(spm,[status(thm)],[c_0_130,c_0_158]) ).
cnf(c_0_171,hypothesis,
~ hasgame(n5,racquetball),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_159,c_0_131]),c_0_138]),c_0_160]),c_0_159]),c_0_159]) ).
cnf(c_0_172,hypothesis,
~ hasgame(n4,racquetball),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_161,c_0_131]),c_0_138]),c_0_160]),c_0_161]),c_0_161]) ).
cnf(c_0_173,hypothesis,
( ~ hasgame(n3,racquetball)
| ~ hascolor(X1,white) ),
inference(spm,[status(thm)],[c_0_146,c_0_162]) ).
cnf(c_0_174,hypothesis,
~ nextto(n1,n4),
house_1_not_nextto_4 ).
cnf(c_0_175,hypothesis,
( nextto(X1,X2)
| ~ haspet(X2,rat)
| ~ hasgame(X1,racquetball) ),
inference(spm,[status(thm)],[c_0_163,c_0_164]) ).
cnf(c_0_176,hypothesis,
~ nextto(n1,n5),
house_1_not_nextto_5 ).
cnf(c_0_177,hypothesis,
~ nextto(n1,n3),
house_1_not_nextto_3 ).
cnf(c_0_178,axiom,
~ nextto(X1,X1),
nothing_nextto_itself ).
cnf(c_0_179,axiom,
~ samecolor(red,green),
red_not_green ).
cnf(c_0_180,hypothesis,
( samecolor(X1,green)
| ~ hascolor(n3,white)
| ~ hascolor(n4,X1) ),
inference(spm,[status(thm)],[c_0_111,c_0_165]) ).
cnf(c_0_181,hypothesis,
( hascolor(n4,red)
| hascolor(n3,red)
| hasperson(n5,englishman) ),
inference(spm,[status(thm)],[c_0_142,c_0_166]) ).
cnf(c_0_182,hypothesis,
~ hasdrink(n3,lemonade),
inference(spm,[status(thm)],[c_0_167,c_0_168]) ).
cnf(c_0_183,hypothesis,
( hasdrink(X1,lemonade)
| ~ hascolor(X1,green) ),
lemonade_in_green_house2 ).
cnf(c_0_184,axiom,
~ samecolor(red,white),
red_not_white ).
cnf(c_0_185,hypothesis,
( samecolor(X1,white)
| ~ hascolor(n5,green)
| ~ hascolor(n4,X1) ),
inference(spm,[status(thm)],[c_0_111,c_0_169]) ).
cnf(c_0_186,hypothesis,
( hasgame(n3,racquetball)
| hascolor(n1,yellow) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[c_0_170,c_0_171]),c_0_172]) ).
cnf(c_0_187,hypothesis,
~ hasgame(n3,racquetball),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_173,c_0_131]),c_0_138]),c_0_160]),c_0_173]),c_0_173]) ).
cnf(c_0_188,hypothesis,
( ~ haspet(n4,rat)
| ~ hasgame(n1,racquetball) ),
inference(spm,[status(thm)],[c_0_174,c_0_175]) ).
cnf(c_0_189,axiom,
( haspet(n1,X1)
| haspet(n2,X1)
| haspet(n3,X1)
| haspet(n4,X1)
| haspet(n5,X1) ),
every_pet_is_used ).
cnf(c_0_190,hypothesis,
( ~ haspet(n5,rat)
| ~ hasgame(n1,racquetball) ),
inference(spm,[status(thm)],[c_0_176,c_0_175]) ).
cnf(c_0_191,hypothesis,
( ~ haspet(n3,rat)
| ~ hasgame(n1,racquetball) ),
inference(spm,[status(thm)],[c_0_177,c_0_175]) ).
cnf(c_0_192,hypothesis,
( ~ haspet(X1,rat)
| ~ hasgame(X1,racquetball) ),
inference(spm,[status(thm)],[c_0_178,c_0_164]) ).
cnf(c_0_193,hypothesis,
( ~ hascolor(n3,white)
| ~ hascolor(n4,red) ),
inference(spm,[status(thm)],[c_0_179,c_0_180]) ).
cnf(c_0_194,hypothesis,
( hascolor(n3,red)
| hascolor(n4,red)
| hascolor(n5,red) ),
inference(spm,[status(thm)],[c_0_142,c_0_181]) ).
cnf(c_0_195,hypothesis,
( hascolor(n3,white)
| ~ hascolor(n4,green) ),
inference(spm,[status(thm)],[c_0_156,c_0_151]) ).
cnf(c_0_196,hypothesis,
~ hascolor(n3,green),
inference(spm,[status(thm)],[c_0_182,c_0_183]) ).
cnf(c_0_197,hypothesis,
( ~ hascolor(n5,green)
| ~ hascolor(n4,red) ),
inference(spm,[status(thm)],[c_0_184,c_0_185]) ).
cnf(c_0_198,hypothesis,
hascolor(n1,yellow),
inference(sr,[status(thm)],[c_0_186,c_0_187]) ).
cnf(c_0_199,axiom,
( samepet(X1,X2)
| ~ haspet(X3,X1)
| ~ haspet(X3,X2) ),
houses_have_unique_pets ).
cnf(c_0_200,hypothesis,
( haspet(n2,rat)
| ~ hasgame(n1,racquetball) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_188,c_0_189]),c_0_190]),c_0_191]),c_0_192]) ).
cnf(c_0_201,axiom,
( hasgame(n1,X1)
| hasgame(n2,X1)
| hasgame(n3,X1)
| hasgame(n4,X1)
| hasgame(n5,X1) ),
every_game_is_used ).
cnf(c_0_202,hypothesis,
~ hasgame(n2,racquetball),
inference(spm,[status(thm)],[c_0_132,c_0_114]) ).
cnf(c_0_203,axiom,
~ sameperson(italian,russian),
italian_not_russian ).
cnf(c_0_204,axiom,
( samehouse(X1,X2)
| ~ hasperson(X1,X3)
| ~ hasperson(X2,X3) ),
nationals_have_unique_houses ).
cnf(c_0_205,hypothesis,
( hascolor(n5,red)
| hascolor(n3,red)
| ~ hascolor(n3,white) ),
inference(spm,[status(thm)],[c_0_193,c_0_194]) ).
cnf(c_0_206,hypothesis,
( hascolor(n5,green)
| hascolor(n1,green)
| hascolor(n3,white) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_195,c_0_131]),c_0_125]),c_0_196]) ).
cnf(c_0_207,hypothesis,
( hascolor(n5,red)
| hascolor(n3,red)
| ~ hascolor(n5,green) ),
inference(spm,[status(thm)],[c_0_197,c_0_194]) ).
cnf(c_0_208,axiom,
~ samecolor(green,yellow),
green_not_yellow ).
cnf(c_0_209,hypothesis,
( samecolor(X1,yellow)
| ~ hascolor(n1,X1) ),
inference(spm,[status(thm)],[c_0_111,c_0_198]) ).
cnf(c_0_210,axiom,
~ samepet(toad,rat),
toad_not_rat ).
cnf(c_0_211,hypothesis,
( samepet(X1,rat)
| ~ haspet(n2,X1)
| ~ hasgame(n1,racquetball) ),
inference(spm,[status(thm)],[c_0_199,c_0_200]) ).
cnf(c_0_212,hypothesis,
( hasgame(n3,racquetball)
| hasgame(n1,racquetball) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_172,c_0_201]),c_0_202]),c_0_171]) ).
cnf(c_0_213,hypothesis,
( haspet(X1,guppy)
| ~ hasperson(X1,italian) ),
italian_has_guppy1 ).
cnf(c_0_214,hypothesis,
~ hasperson(n1,italian),
inference(spm,[status(thm)],[c_0_203,c_0_116]) ).
cnf(c_0_215,axiom,
( ~ samehouse(X1,X2)
| ~ nextto(X1,X2) ),
house_not_nextto_itself ).
cnf(c_0_216,hypothesis,
( samehouse(X1,X2)
| ~ hascolor(X2,red)
| ~ hasperson(X1,englishman) ),
inference(spm,[status(thm)],[c_0_204,c_0_124]) ).
cnf(c_0_217,hypothesis,
( hascolor(n1,green)
| hascolor(n3,red)
| hascolor(n5,red) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_205,c_0_206]),c_0_207]) ).
cnf(c_0_218,hypothesis,
~ hascolor(n1,green),
inference(spm,[status(thm)],[c_0_208,c_0_209]) ).
cnf(c_0_219,hypothesis,
( hasgame(X1,backgammon)
| ~ haspet(X1,toad) ),
toad_lives_with_backgammon1 ).
cnf(c_0_220,hypothesis,
( ~ haspet(n2,toad)
| ~ hasgame(n1,racquetball) ),
inference(spm,[status(thm)],[c_0_210,c_0_211]) ).
cnf(c_0_221,hypothesis,
hasgame(n1,racquetball),
inference(sr,[status(thm)],[c_0_212,c_0_187]) ).
cnf(c_0_222,hypothesis,
( haspet(n4,guppy)
| hasperson(n5,italian)
| hasperson(n3,italian)
| hasperson(n2,italian) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_213,c_0_143]),c_0_214]) ).
cnf(c_0_223,axiom,
~ samepet(guppy,rat),
guppy_not_rat ).
cnf(c_0_224,hypothesis,
( ~ hascolor(X1,red)
| ~ hasperson(X2,englishman)
| ~ nextto(X2,X1) ),
inference(spm,[status(thm)],[c_0_215,c_0_216]) ).
cnf(c_0_225,hypothesis,
( hascolor(n5,red)
| hascolor(n3,red) ),
inference(sr,[status(thm)],[c_0_217,c_0_218]) ).
cnf(c_0_226,axiom,
~ samehouse(n4,n5),
house_4_not_5 ).
cnf(c_0_227,hypothesis,
( haspet(n5,toad)
| haspet(n3,toad)
| haspet(n2,toad)
| haspet(n1,toad)
| hasgame(n4,backgammon) ),
inference(spm,[status(thm)],[c_0_219,c_0_189]) ).
cnf(c_0_228,hypothesis,
~ haspet(n2,toad),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_220,c_0_221])]) ).
cnf(c_0_229,hypothesis,
( haspet(n4,guppy)
| haspet(n2,guppy)
| hasperson(n3,italian)
| hasperson(n5,italian) ),
inference(spm,[status(thm)],[c_0_213,c_0_222]) ).
cnf(c_0_230,hypothesis,
( ~ haspet(n2,guppy)
| ~ hasgame(n1,racquetball) ),
inference(spm,[status(thm)],[c_0_223,c_0_211]) ).
cnf(c_0_231,hypothesis,
left(n2,n3),
house_2_left_of_3 ).
cnf(c_0_232,hypothesis,
( hascolor(n5,red)
| ~ hasperson(X1,englishman)
| ~ nextto(X1,n3) ),
inference(spm,[status(thm)],[c_0_224,c_0_225]) ).
cnf(c_0_233,hypothesis,
nextto(n3,n4),
inference(spm,[status(thm)],[c_0_106,c_0_151]) ).
cnf(c_0_234,hypothesis,
( ~ hascolor(n5,red)
| ~ hasperson(n4,englishman) ),
inference(spm,[status(thm)],[c_0_226,c_0_216]) ).
cnf(c_0_235,axiom,
( samehouse(X1,X2)
| ~ haspet(X1,X3)
| ~ haspet(X2,X3) ),
pets_have_unique_houses ).
cnf(c_0_236,hypothesis,
( haspet(n1,toad)
| haspet(n3,toad)
| haspet(n5,toad)
| hasgame(n4,backgammon) ),
inference(sr,[status(thm)],[c_0_227,c_0_228]) ).
cnf(c_0_237,axiom,
( samegame(X1,X2)
| ~ hasgame(X3,X1)
| ~ hasgame(X3,X2) ),
houses_have_unique_games ).
cnf(c_0_238,hypothesis,
( haspet(n2,guppy)
| haspet(n4,guppy)
| haspet(n3,guppy)
| hasperson(n5,italian) ),
inference(spm,[status(thm)],[c_0_213,c_0_229]) ).
cnf(c_0_239,hypothesis,
~ haspet(n2,guppy),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_230,c_0_221])]) ).
cnf(c_0_240,axiom,
~ left(X1,X1),
nothing_left_of_itself ).
cnf(c_0_241,axiom,
~ samehouse(n3,n5),
house_3_not_5 ).
cnf(c_0_242,hypothesis,
nextto(n2,n3),
inference(spm,[status(thm)],[c_0_106,c_0_231]) ).
cnf(c_0_243,hypothesis,
( hasperson(X1,american)
| ~ hasgame(X1,charades) ),
c18 ).
cnf(c_0_244,hypothesis,
( hascolor(n5,red)
| ~ hascolor(X1,red)
| ~ nextto(X1,n3) ),
inference(spm,[status(thm)],[c_0_232,c_0_124]) ).
cnf(c_0_245,hypothesis,
nextto(n4,n3),
inference(spm,[status(thm)],[c_0_163,c_0_233]) ).
cnf(c_0_246,hypothesis,
( ~ hascolor(n5,red)
| ~ hascolor(n4,red) ),
inference(spm,[status(thm)],[c_0_234,c_0_124]) ).
cnf(c_0_247,hypothesis,
( samehouse(X1,n2)
| ~ haspet(X1,rat)
| ~ hasgame(n1,racquetball) ),
inference(spm,[status(thm)],[c_0_235,c_0_200]) ).
cnf(c_0_248,hypothesis,
( haspet(n5,toad)
| haspet(n1,toad)
| hasgame(n4,backgammon)
| hasgame(n3,backgammon) ),
inference(spm,[status(thm)],[c_0_219,c_0_236]) ).
cnf(c_0_249,axiom,
~ samegame(backgammon,racquetball),
backgammon_not_recquetball ).
cnf(c_0_250,hypothesis,
( samegame(X1,racquetball)
| ~ hasgame(n1,X1) ),
inference(spm,[status(thm)],[c_0_237,c_0_221]) ).
cnf(c_0_251,hypothesis,
( haspet(n3,guppy)
| haspet(n4,guppy)
| hasperson(n5,italian) ),
inference(sr,[status(thm)],[c_0_238,c_0_239]) ).
cnf(c_0_252,hypothesis,
( hascolor(n1,green)
| hascolor(n5,green)
| samecolor(X1,white)
| ~ hascolor(n3,X1) ),
inference(spm,[status(thm)],[c_0_111,c_0_206]) ).
cnf(c_0_253,hypothesis,
( ~ hascolor(X1,green)
| ~ hascolor(X1,white) ),
inference(spm,[status(thm)],[c_0_240,c_0_134]) ).
cnf(c_0_254,hypothesis,
( ~ hascolor(n5,red)
| ~ hasperson(n3,englishman) ),
inference(spm,[status(thm)],[c_0_241,c_0_216]) ).
cnf(c_0_255,hypothesis,
( ~ hascolor(X1,blue)
| ~ nextto(X1,n2) ),
inference(spm,[status(thm)],[c_0_215,c_0_128]) ).
cnf(c_0_256,hypothesis,
nextto(n3,n2),
inference(spm,[status(thm)],[c_0_163,c_0_242]) ).
cnf(c_0_257,hypothesis,
( sameperson(X1,american)
| ~ hasgame(X2,charades)
| ~ hasperson(X2,X1) ),
inference(spm,[status(thm)],[c_0_110,c_0_243]) ).
cnf(c_0_258,axiom,
( hasgame(X1,backgammon)
| hasgame(X1,racquetball)
| hasgame(X1,quoits)
| hasgame(X1,solitaire)
| hasgame(X1,charades) ),
every_house_has_a_game ).
cnf(c_0_259,hypothesis,
~ hascolor(n4,red),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_244,c_0_245]),c_0_246]) ).
cnf(c_0_260,axiom,
~ samedrink(coffee,milk),
coffee_not_milk ).
cnf(c_0_261,hypothesis,
( haspet(X1,toad)
| ~ hasgame(X1,backgammon) ),
toad_lives_with_backgammon2 ).
cnf(c_0_262,axiom,
( haspet(X1,guppy)
| haspet(X1,toad)
| haspet(X1,camel)
| haspet(X1,rat)
| haspet(X1,no_pet) ),
every_house_has_a_pet ).
cnf(c_0_263,hypothesis,
( ~ haspet(X1,rat)
| ~ hasgame(n1,racquetball)
| ~ nextto(X1,n2) ),
inference(spm,[status(thm)],[c_0_215,c_0_247]) ).
cnf(c_0_264,hypothesis,
( haspet(n1,toad)
| hasgame(n3,backgammon)
| hasgame(n4,backgammon)
| hasgame(n5,backgammon) ),
inference(spm,[status(thm)],[c_0_219,c_0_248]) ).
cnf(c_0_265,hypothesis,
~ hasgame(n1,backgammon),
inference(spm,[status(thm)],[c_0_249,c_0_250]) ).
cnf(c_0_266,hypothesis,
( haspet(n4,guppy)
| haspet(n3,guppy)
| sameperson(X1,italian)
| ~ hasperson(n5,X1) ),
inference(spm,[status(thm)],[c_0_110,c_0_251]) ).
cnf(c_0_267,axiom,
~ sameperson(englishman,italian),
englishman_not_italian ).
cnf(c_0_268,hypothesis,
( hascolor(n5,red)
| hascolor(n5,green)
| hascolor(n1,green) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_252,c_0_217]),c_0_184]) ).
cnf(c_0_269,hypothesis,
( ~ hascolor(n4,green)
| ~ hascolor(n5,green) ),
inference(spm,[status(thm)],[c_0_253,c_0_169]) ).
cnf(c_0_270,hypothesis,
( ~ hascolor(n5,red)
| ~ hascolor(n3,red) ),
inference(spm,[status(thm)],[c_0_254,c_0_124]) ).
cnf(c_0_271,hypothesis,
( hasgame(X1,racquetball)
| hascolor(X1,blue)
| hascolor(X1,green)
| hascolor(X1,white)
| hascolor(X1,red) ),
inference(spm,[status(thm)],[c_0_130,c_0_136]) ).
cnf(c_0_272,hypothesis,
~ hascolor(n3,blue),
inference(spm,[status(thm)],[c_0_255,c_0_256]) ).
cnf(c_0_273,hypothesis,
( hasgame(X1,solitaire)
| hasgame(X1,quoits)
| hasgame(X1,racquetball)
| hasgame(X1,backgammon)
| sameperson(X2,american)
| ~ hasperson(X1,X2) ),
inference(spm,[status(thm)],[c_0_257,c_0_258]) ).
cnf(c_0_274,hypothesis,
( hasperson(n5,englishman)
| hasperson(n3,englishman) ),
inference(sr,[status(thm)],[c_0_166,c_0_259]) ).
cnf(c_0_275,axiom,
~ sameperson(englishman,american),
englishman_not_american ).
cnf(c_0_276,hypothesis,
( hasdrink(X1,coffee)
| ~ hasperson(X1,swede) ),
swede_drinks_coffee1 ).
cnf(c_0_277,axiom,
~ sameperson(swede,russian),
swede_not_russian ).
cnf(c_0_278,hypothesis,
~ hasdrink(n3,coffee),
inference(spm,[status(thm)],[c_0_260,c_0_168]) ).
cnf(c_0_279,hypothesis,
( hasperson(X1,italian)
| ~ haspet(X1,guppy) ),
italian_has_guppy2 ).
cnf(c_0_280,hypothesis,
( samehouse(X1,X2)
| ~ haspet(X1,toad)
| ~ hasgame(X2,backgammon) ),
inference(spm,[status(thm)],[c_0_235,c_0_261]) ).
cnf(c_0_281,hypothesis,
nextto(n4,n5),
inference(spm,[status(thm)],[c_0_106,c_0_157]) ).
cnf(c_0_282,plain,
( haspet(X1,rat)
| haspet(X1,camel)
| haspet(X1,toad)
| haspet(X1,guppy)
| samehouse(X2,X1)
| ~ haspet(X2,no_pet) ),
inference(spm,[status(thm)],[c_0_235,c_0_262]) ).
cnf(c_0_283,hypothesis,
( ~ haspet(X1,rat)
| ~ nextto(X1,n2) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_263,c_0_221])]) ).
cnf(c_0_284,hypothesis,
( samepet(X1,toad)
| ~ haspet(X2,X1)
| ~ hasgame(X2,backgammon) ),
inference(spm,[status(thm)],[c_0_199,c_0_261]) ).
cnf(c_0_285,hypothesis,
( hasgame(n5,backgammon)
| hasgame(n4,backgammon)
| hasgame(n3,backgammon) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_219,c_0_264]),c_0_265]) ).
cnf(c_0_286,hypothesis,
( haspet(n3,guppy)
| haspet(n4,guppy)
| ~ hascolor(n5,red) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_266,c_0_124]),c_0_267]) ).
cnf(c_0_287,hypothesis,
( hascolor(n5,green)
| hascolor(n5,red) ),
inference(sr,[status(thm)],[c_0_268,c_0_218]) ).
cnf(c_0_288,hypothesis,
( ~ hascolor(n5,green)
| ~ hascolor(n3,white) ),
inference(spm,[status(thm)],[c_0_269,c_0_165]) ).
cnf(c_0_289,hypothesis,
( hascolor(n3,white)
| ~ hascolor(n5,red) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_270,c_0_271]),c_0_187]),c_0_272]),c_0_196]) ).
cnf(c_0_290,hypothesis,
( hasgame(n3,backgammon)
| hasgame(n3,quoits)
| hasgame(n3,solitaire)
| hasperson(n5,englishman) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_273,c_0_274]),c_0_187]),c_0_275]) ).
cnf(c_0_291,hypothesis,
( hasperson(X1,swede)
| ~ hasdrink(X1,coffee) ),
swede_drinks_coffee2 ).
cnf(c_0_292,axiom,
( hasdrink(n1,X1)
| hasdrink(n2,X1)
| hasdrink(n3,X1)
| hasdrink(n4,X1)
| hasdrink(n5,X1) ),
every_drink_is_used ).
cnf(c_0_293,hypothesis,
( samedrink(X1,coffee)
| ~ hasdrink(X2,X1)
| ~ hasperson(X2,swede) ),
inference(spm,[status(thm)],[c_0_154,c_0_276]) ).
cnf(c_0_294,hypothesis,
~ hasperson(n1,swede),
inference(spm,[status(thm)],[c_0_277,c_0_116]) ).
cnf(c_0_295,hypothesis,
~ hasperson(n3,swede),
inference(spm,[status(thm)],[c_0_278,c_0_276]) ).
cnf(c_0_296,hypothesis,
( samehouse(X1,X2)
| ~ haspet(X2,guppy)
| ~ hasperson(X1,italian) ),
inference(spm,[status(thm)],[c_0_204,c_0_279]) ).
cnf(c_0_297,hypothesis,
( ~ haspet(X1,toad)
| ~ hasgame(X2,backgammon)
| ~ nextto(X1,X2) ),
inference(spm,[status(thm)],[c_0_215,c_0_280]) ).
cnf(c_0_298,hypothesis,
nextto(n5,n4),
inference(spm,[status(thm)],[c_0_163,c_0_281]) ).
cnf(c_0_299,plain,
( haspet(X1,rat)
| haspet(X1,camel)
| haspet(X1,toad)
| haspet(X1,guppy)
| haspet(X2,guppy)
| haspet(X2,toad)
| haspet(X2,camel)
| haspet(X2,rat)
| samehouse(X1,X2) ),
inference(spm,[status(thm)],[c_0_282,c_0_262]) ).
cnf(c_0_300,hypothesis,
~ haspet(n1,rat),
inference(spm,[status(thm)],[c_0_283,c_0_109]) ).
cnf(c_0_301,hypothesis,
~ haspet(n1,guppy),
inference(spm,[status(thm)],[c_0_214,c_0_279]) ).
cnf(c_0_302,hypothesis,
~ haspet(n5,rat),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_190,c_0_221])]) ).
cnf(c_0_303,axiom,
~ sameperson(italian,american),
italian_not_american ).
cnf(c_0_304,hypothesis,
( hasgame(n3,backgammon)
| hasgame(n5,backgammon)
| samepet(X1,toad)
| ~ haspet(n4,X1) ),
inference(spm,[status(thm)],[c_0_284,c_0_285]) ).
cnf(c_0_305,hypothesis,
( haspet(n4,guppy)
| haspet(n3,guppy)
| hascolor(n5,green) ),
inference(spm,[status(thm)],[c_0_286,c_0_287]) ).
cnf(c_0_306,axiom,
~ samepet(guppy,toad),
guppy_not_toad ).
cnf(c_0_307,hypothesis,
( ~ hascolor(n5,green)
| ~ hascolor(n5,red) ),
inference(spm,[status(thm)],[c_0_288,c_0_289]) ).
cnf(c_0_308,hypothesis,
( hasgame(n3,solitaire)
| hasgame(n3,quoits)
| hasgame(n3,backgammon)
| hascolor(n5,red) ),
inference(spm,[status(thm)],[c_0_142,c_0_290]) ).
cnf(c_0_309,hypothesis,
( hasdrink(n5,coffee)
| hasdrink(n2,coffee)
| hasdrink(n1,coffee)
| hasperson(n4,swede) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_291,c_0_292]),c_0_278]) ).
cnf(c_0_310,hypothesis,
( hasperson(n5,swede)
| hasperson(n2,swede)
| samedrink(X1,coffee)
| ~ hasdrink(n4,X1) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_293,c_0_143]),c_0_294]),c_0_295]) ).
cnf(c_0_311,axiom,
~ samedrink(lemonade,coffee),
lemonade_not_coffee ).
cnf(c_0_312,axiom,
~ samehouse(n3,n4),
house_3_not_4 ).
cnf(c_0_313,hypothesis,
~ haspet(n3,rat),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_191,c_0_221])]) ).
cnf(c_0_314,hypothesis,
( ~ haspet(n5,guppy)
| ~ hasperson(n4,italian) ),
inference(spm,[status(thm)],[c_0_226,c_0_296]) ).
cnf(c_0_315,hypothesis,
( hascolor(n3,red)
| hasperson(n5,englishman) ),
inference(sr,[status(thm)],[c_0_181,c_0_259]) ).
cnf(c_0_316,hypothesis,
( ~ haspet(n5,guppy)
| ~ hasperson(n3,italian) ),
inference(spm,[status(thm)],[c_0_241,c_0_296]) ).
cnf(c_0_317,hypothesis,
( ~ haspet(n5,toad)
| ~ hasgame(n4,backgammon) ),
inference(spm,[status(thm)],[c_0_297,c_0_298]) ).
cnf(c_0_318,plain,
( haspet(n5,camel)
| haspet(n5,toad)
| haspet(n5,guppy)
| haspet(n1,toad)
| haspet(n1,camel) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_121,c_0_299]),c_0_300]),c_0_301]),c_0_302]) ).
cnf(c_0_319,hypothesis,
( ~ haspet(n1,toad)
| ~ hasgame(n4,backgammon) ),
inference(spm,[status(thm)],[c_0_129,c_0_280]) ).
cnf(c_0_320,hypothesis,
( ~ hasgame(n1,racquetball)
| ~ hasgame(n2,backgammon) ),
inference(spm,[status(thm)],[c_0_220,c_0_261]) ).
cnf(c_0_321,hypothesis,
( hasdrink(X1,vodka)
| ~ hasgame(X1,solitaire) ),
c15 ).
cnf(c_0_322,hypothesis,
( hasgame(X1,backgammon)
| hasgame(X1,racquetball)
| hasgame(X1,quoits)
| hasgame(X1,solitaire)
| ~ haspet(X1,guppy) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_273,c_0_279]),c_0_303]) ).
cnf(c_0_323,hypothesis,
( haspet(n3,guppy)
| hasgame(n5,backgammon)
| hasgame(n3,backgammon)
| hascolor(n5,green) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_304,c_0_305]),c_0_306]) ).
cnf(c_0_324,hypothesis,
( hasgame(n3,backgammon)
| hasgame(n3,quoits)
| hasgame(n3,solitaire)
| ~ hascolor(n5,green) ),
inference(spm,[status(thm)],[c_0_307,c_0_308]) ).
cnf(c_0_325,hypothesis,
( hasdrink(n1,coffee)
| hasdrink(n5,coffee)
| hasperson(n4,swede)
| hasperson(n2,swede) ),
inference(spm,[status(thm)],[c_0_291,c_0_309]) ).
cnf(c_0_326,hypothesis,
( haspet(n4,guppy)
| hasperson(n5,italian)
| hasperson(n3,italian) ),
inference(sr,[status(thm)],[c_0_229,c_0_239]) ).
cnf(c_0_327,hypothesis,
( hasperson(n2,swede)
| hasperson(n5,swede)
| ~ hascolor(n4,green) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_310,c_0_183]),c_0_311]) ).
cnf(c_0_328,hypothesis,
( ~ haspet(n3,toad)
| ~ hasgame(n4,backgammon) ),
inference(spm,[status(thm)],[c_0_312,c_0_280]) ).
cnf(c_0_329,plain,
( haspet(n3,camel)
| haspet(n3,toad)
| haspet(n3,guppy)
| haspet(n1,toad)
| haspet(n1,camel) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_141,c_0_299]),c_0_300]),c_0_301]),c_0_313]) ).
cnf(c_0_330,hypothesis,
( ~ haspet(n3,toad)
| ~ hasgame(n5,backgammon) ),
inference(spm,[status(thm)],[c_0_241,c_0_280]) ).
cnf(c_0_331,hypothesis,
( ~ haspet(n1,toad)
| ~ hasgame(n5,backgammon) ),
inference(spm,[status(thm)],[c_0_121,c_0_280]) ).
cnf(c_0_332,hypothesis,
( nextto(X1,X2)
| ~ haspet(X1,camel)
| ~ hasgame(X2,quoits) ),
c4 ).
cnf(c_0_333,hypothesis,
( ~ haspet(n5,guppy)
| ~ haspet(n4,guppy) ),
inference(spm,[status(thm)],[c_0_314,c_0_279]) ).
cnf(c_0_334,hypothesis,
( haspet(n3,guppy)
| haspet(n4,guppy)
| hascolor(n3,red) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_266,c_0_315]),c_0_267]) ).
cnf(c_0_335,hypothesis,
( ~ haspet(n5,guppy)
| ~ haspet(n3,guppy) ),
inference(spm,[status(thm)],[c_0_316,c_0_279]) ).
cnf(c_0_336,hypothesis,
( haspet(n1,camel)
| haspet(n5,guppy)
| haspet(n5,camel)
| ~ hasgame(n4,backgammon) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_317,c_0_318]),c_0_319]) ).
cnf(c_0_337,hypothesis,
~ hasgame(n2,backgammon),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_320,c_0_221])]) ).
cnf(c_0_338,hypothesis,
( samedrink(X1,vodka)
| ~ hasgame(X2,solitaire)
| ~ hasdrink(X2,X1) ),
inference(spm,[status(thm)],[c_0_154,c_0_321]) ).
cnf(c_0_339,hypothesis,
( hasgame(n5,backgammon)
| hasgame(n3,solitaire)
| hasgame(n3,quoits)
| hasgame(n3,backgammon) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_322,c_0_323]),c_0_187]),c_0_324]) ).
cnf(c_0_340,hypothesis,
( hasdrink(n1,coffee)
| hasperson(n2,swede)
| hasperson(n4,swede)
| hasperson(n5,swede) ),
inference(spm,[status(thm)],[c_0_291,c_0_325]) ).
cnf(c_0_341,hypothesis,
( haspet(n4,guppy)
| hasperson(n5,italian)
| sameperson(X1,italian)
| ~ hasperson(n3,X1) ),
inference(spm,[status(thm)],[c_0_110,c_0_326]) ).
cnf(c_0_342,axiom,
~ samehouse(n2,n4),
house_2_not_4 ).
cnf(c_0_343,hypothesis,
( samehouse(X1,X2)
| ~ hasgame(X2,charades)
| ~ hasperson(X1,american) ),
inference(spm,[status(thm)],[c_0_204,c_0_243]) ).
cnf(c_0_344,hypothesis,
( hascolor(n5,green)
| hascolor(n1,green)
| hasperson(n5,swede)
| hasperson(n2,swede) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_327,c_0_131]),c_0_125]),c_0_196]) ).
cnf(c_0_345,hypothesis,
( haspet(n1,camel)
| haspet(n3,guppy)
| haspet(n3,camel)
| ~ hasgame(n4,backgammon) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_328,c_0_329]),c_0_319]) ).
cnf(c_0_346,hypothesis,
( haspet(n1,camel)
| haspet(n3,guppy)
| haspet(n3,camel)
| ~ hasgame(n5,backgammon) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_330,c_0_329]),c_0_331]) ).
cnf(c_0_347,hypothesis,
~ nextto(n3,n5),
house_3_not_nextto_5 ).
cnf(c_0_348,hypothesis,
( nextto(X1,X2)
| ~ haspet(X2,camel)
| ~ hasgame(X1,quoits) ),
inference(spm,[status(thm)],[c_0_163,c_0_332]) ).
cnf(c_0_349,hypothesis,
( hascolor(n3,red)
| ~ haspet(n5,guppy) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_333,c_0_334]),c_0_335]) ).
cnf(c_0_350,hypothesis,
( haspet(n5,camel)
| haspet(n5,guppy)
| haspet(n1,camel)
| hasgame(n5,backgammon)
| hasgame(n3,backgammon) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_336,c_0_201]),c_0_265]),c_0_337]) ).
cnf(c_0_351,hypothesis,
( hasgame(n3,backgammon)
| hasgame(n3,quoits)
| hasgame(n5,backgammon)
| samedrink(X1,vodka)
| ~ hasdrink(n3,X1) ),
inference(spm,[status(thm)],[c_0_338,c_0_339]) ).
cnf(c_0_352,axiom,
~ samedrink(milk,vodka),
milk_not_vodka ).
cnf(c_0_353,hypothesis,
( hasperson(n5,swede)
| hasperson(n4,swede)
| hasperson(n2,swede) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_291,c_0_340]),c_0_294]) ).
cnf(c_0_354,hypothesis,
( haspet(n4,guppy)
| hasperson(n5,italian)
| ~ hascolor(n3,red) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_341,c_0_124]),c_0_267]) ).
cnf(c_0_355,hypothesis,
( ~ hasgame(n4,charades)
| ~ hasperson(n2,american) ),
inference(spm,[status(thm)],[c_0_342,c_0_343]) ).
cnf(c_0_356,hypothesis,
( hascolor(n5,green)
| hasperson(n2,swede)
| hasperson(n5,swede) ),
inference(sr,[status(thm)],[c_0_344,c_0_218]) ).
cnf(c_0_357,axiom,
~ sameperson(swede,american),
swede_not_american ).
cnf(c_0_358,hypothesis,
( sameperson(X1,italian)
| ~ haspet(X2,guppy)
| ~ hasperson(X2,X1) ),
inference(spm,[status(thm)],[c_0_110,c_0_279]) ).
cnf(c_0_359,hypothesis,
( haspet(n3,camel)
| haspet(n3,guppy)
| haspet(n1,camel)
| hasgame(n3,backgammon) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_345,c_0_201]),c_0_265]),c_0_337]),c_0_346]) ).
cnf(c_0_360,hypothesis,
( ~ haspet(n5,camel)
| ~ hasgame(n3,quoits) ),
inference(spm,[status(thm)],[c_0_347,c_0_348]) ).
cnf(c_0_361,hypothesis,
( haspet(n1,camel)
| haspet(n5,camel)
| hasgame(n3,backgammon)
| hasgame(n5,backgammon)
| hascolor(n3,red) ),
inference(spm,[status(thm)],[c_0_349,c_0_350]) ).
cnf(c_0_362,hypothesis,
( hasgame(n5,backgammon)
| hasgame(n3,quoits)
| hasgame(n3,backgammon) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_351,c_0_155]),c_0_352]) ).
cnf(c_0_363,hypothesis,
( hasperson(n2,swede)
| hasperson(n5,swede)
| sameperson(X1,swede)
| ~ hasperson(n4,X1) ),
inference(spm,[status(thm)],[c_0_110,c_0_353]) ).
cnf(c_0_364,axiom,
~ sameperson(italian,swede),
italian_not_swede ).
cnf(c_0_365,hypothesis,
( haspet(n4,guppy)
| hascolor(n3,white)
| hasperson(n5,italian) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_354,c_0_271]),c_0_187]),c_0_272]),c_0_196]) ).
cnf(c_0_366,hypothesis,
( ~ hasgame(n4,charades)
| ~ hasgame(n2,charades) ),
inference(spm,[status(thm)],[c_0_355,c_0_243]) ).
cnf(c_0_367,hypothesis,
( hasgame(n2,quoits)
| hasgame(n2,solitaire)
| hascolor(n5,green)
| hasperson(n5,swede) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_273,c_0_356]),c_0_202]),c_0_337]),c_0_357]) ).
cnf(c_0_368,hypothesis,
( haspet(n1,camel)
| haspet(n3,camel)
| hasgame(n3,backgammon)
| sameperson(X1,italian)
| ~ hasperson(n3,X1) ),
inference(spm,[status(thm)],[c_0_358,c_0_359]) ).
cnf(c_0_369,hypothesis,
( ~ haspet(n1,camel)
| ~ hasgame(n3,quoits) ),
inference(spm,[status(thm)],[c_0_177,c_0_332]) ).
cnf(c_0_370,hypothesis,
( haspet(n1,camel)
| hasgame(n5,backgammon)
| hasgame(n3,backgammon)
| hascolor(n3,red) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_360,c_0_361]),c_0_362]) ).
cnf(c_0_371,hypothesis,
( hasperson(n5,swede)
| hasperson(n2,swede)
| ~ haspet(n4,guppy) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_363,c_0_279]),c_0_364]) ).
cnf(c_0_372,hypothesis,
( haspet(n4,guppy)
| haspet(n5,guppy)
| hascolor(n3,white) ),
inference(spm,[status(thm)],[c_0_213,c_0_365]) ).
cnf(c_0_373,hypothesis,
( hasperson(n5,swede)
| hasperson(n2,swede)
| ~ hascolor(n3,white) ),
inference(spm,[status(thm)],[c_0_327,c_0_165]) ).
cnf(c_0_374,hypothesis,
( hasgame(n4,solitaire)
| hasgame(n4,quoits)
| hasgame(n4,racquetball)
| hasgame(n4,backgammon)
| ~ hasgame(n2,charades) ),
inference(spm,[status(thm)],[c_0_366,c_0_258]) ).
cnf(c_0_375,hypothesis,
( hasdrink(n1,coffee)
| hasperson(n2,swede)
| hasperson(n4,swede)
| samedrink(X1,coffee)
| ~ hasdrink(n5,X1) ),
inference(spm,[status(thm)],[c_0_154,c_0_325]) ).
cnf(c_0_376,hypothesis,
( hasgame(n2,solitaire)
| hasgame(n2,quoits)
| hascolor(n5,green)
| sameperson(X1,swede)
| ~ hasperson(n5,X1) ),
inference(spm,[status(thm)],[c_0_110,c_0_367]) ).
cnf(c_0_377,axiom,
~ sameperson(englishman,swede),
englishman_not_swede ).
cnf(c_0_378,hypothesis,
( haspet(n3,camel)
| haspet(n1,camel)
| hasgame(n3,backgammon)
| ~ hascolor(n3,red) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_368,c_0_124]),c_0_267]) ).
cnf(c_0_379,hypothesis,
( hasgame(n3,backgammon)
| hasgame(n5,backgammon)
| hascolor(n3,red) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_369,c_0_370]),c_0_362]) ).
cnf(c_0_380,hypothesis,
( haspet(n5,guppy)
| hasperson(n2,swede)
| hasperson(n5,swede) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_371,c_0_372]),c_0_373]) ).
cnf(c_0_381,hypothesis,
( hasgame(n2,solitaire)
| hasgame(n2,quoits)
| hasgame(n4,backgammon)
| hasgame(n4,quoits)
| hasgame(n4,solitaire) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_374,c_0_258]),c_0_202]),c_0_172]),c_0_337]) ).
cnf(c_0_382,hypothesis,
( hasdrink(n1,coffee)
| hasperson(n4,swede)
| hasperson(n2,swede)
| ~ hascolor(n5,green) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_375,c_0_183]),c_0_311]) ).
cnf(c_0_383,hypothesis,
( hasgame(n2,quoits)
| hasgame(n2,solitaire)
| hascolor(n5,green) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_376,c_0_124]),c_0_377]),c_0_287]) ).
cnf(c_0_384,hypothesis,
( ~ haspet(X1,camel)
| ~ hasgame(X1,quoits) ),
inference(spm,[status(thm)],[c_0_178,c_0_332]) ).
cnf(c_0_385,hypothesis,
( haspet(n1,camel)
| haspet(n3,camel)
| hasgame(n5,backgammon)
| hasgame(n3,backgammon) ),
inference(spm,[status(thm)],[c_0_378,c_0_379]) ).
cnf(c_0_386,hypothesis,
( haspet(n5,guppy)
| hasgame(n2,quoits)
| hasgame(n2,solitaire)
| hasperson(n5,swede) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_273,c_0_380]),c_0_202]),c_0_337]),c_0_357]) ).
cnf(c_0_387,hypothesis,
~ haspet(n4,rat),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_188,c_0_221])]) ).
cnf(c_0_388,hypothesis,
( hasgame(n4,quoits)
| hasgame(n4,backgammon)
| hasgame(n2,quoits)
| hasgame(n2,solitaire)
| samedrink(X1,vodka)
| ~ hasdrink(n4,X1) ),
inference(spm,[status(thm)],[c_0_338,c_0_381]) ).
cnf(c_0_389,axiom,
~ samedrink(coffee,vodka),
coffee_not_vodka ).
cnf(c_0_390,hypothesis,
( hasgame(n2,solitaire)
| hasgame(n2,quoits)
| hasdrink(n1,coffee)
| hasperson(n2,swede)
| hasperson(n4,swede) ),
inference(spm,[status(thm)],[c_0_382,c_0_383]) ).
cnf(c_0_391,plain,
( haspet(n5,X1)
| haspet(n3,X1)
| haspet(n2,X1)
| haspet(n1,X1)
| samehouse(X2,n4)
| ~ haspet(X2,X1) ),
inference(spm,[status(thm)],[c_0_235,c_0_189]) ).
cnf(c_0_392,hypothesis,
( haspet(n1,camel)
| hasgame(n3,backgammon)
| hasgame(n5,backgammon) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_384,c_0_385]),c_0_362]) ).
cnf(c_0_393,hypothesis,
( haspet(n5,guppy)
| hasgame(n2,solitaire)
| hasgame(n2,quoits)
| samedrink(X1,coffee)
| ~ hasdrink(n5,X1) ),
inference(spm,[status(thm)],[c_0_293,c_0_386]) ).
cnf(c_0_394,hypothesis,
( ~ haspet(n4,toad)
| ~ hasgame(n3,backgammon) ),
inference(spm,[status(thm)],[c_0_297,c_0_245]) ).
cnf(c_0_395,plain,
( haspet(n4,camel)
| haspet(n4,toad)
| haspet(n4,guppy)
| haspet(n1,toad)
| haspet(n1,camel) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_129,c_0_299]),c_0_300]),c_0_301]),c_0_387]) ).
cnf(c_0_396,hypothesis,
( ~ haspet(n1,toad)
| ~ hasgame(n3,backgammon) ),
inference(spm,[status(thm)],[c_0_141,c_0_280]) ).
cnf(c_0_397,hypothesis,
( ~ haspet(n4,toad)
| ~ hasgame(n5,backgammon) ),
inference(spm,[status(thm)],[c_0_226,c_0_280]) ).
cnf(c_0_398,hypothesis,
( hasgame(n2,solitaire)
| hasgame(n2,quoits)
| hasgame(n4,backgammon)
| hasgame(n4,quoits)
| ~ hasperson(n4,swede) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_388,c_0_276]),c_0_389]) ).
cnf(c_0_399,hypothesis,
( hasgame(n2,quoits)
| hasgame(n2,solitaire)
| hasperson(n4,swede)
| hasperson(n2,swede) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_291,c_0_390]),c_0_294]) ).
cnf(c_0_400,hypothesis,
( haspet(n1,toad)
| haspet(n3,toad)
| haspet(n5,toad)
| samehouse(X1,n4)
| ~ hasgame(X1,backgammon) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_391,c_0_261]),c_0_228]) ).
cnf(c_0_401,hypothesis,
( hasgame(n5,backgammon)
| hasgame(n3,backgammon) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_369,c_0_392]),c_0_362]) ).
cnf(c_0_402,hypothesis,
( haspet(n5,guppy)
| hasgame(n2,quoits)
| hasgame(n2,solitaire) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_393,c_0_183]),c_0_311]),c_0_383]) ).
cnf(c_0_403,hypothesis,
( haspet(n1,camel)
| haspet(n4,guppy)
| haspet(n4,camel)
| ~ hasgame(n3,backgammon) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_394,c_0_395]),c_0_396]) ).
cnf(c_0_404,hypothesis,
( haspet(n1,camel)
| haspet(n4,guppy)
| haspet(n4,camel)
| ~ hasgame(n5,backgammon) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_397,c_0_395]),c_0_331]) ).
cnf(c_0_405,hypothesis,
( hasgame(n4,quoits)
| hasgame(n4,backgammon)
| hasgame(n2,quoits)
| hasgame(n2,solitaire)
| hasperson(n2,swede) ),
inference(spm,[status(thm)],[c_0_398,c_0_399]) ).
cnf(c_0_406,hypothesis,
( haspet(n5,toad)
| haspet(n3,toad)
| haspet(n1,toad) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_400,c_0_401]),c_0_312]),c_0_261]) ).
cnf(c_0_407,hypothesis,
( hasgame(n2,solitaire)
| hasgame(n2,quoits)
| samehouse(X1,n5)
| ~ haspet(X1,guppy) ),
inference(spm,[status(thm)],[c_0_235,c_0_402]) ).
cnf(c_0_408,hypothesis,
( haspet(n4,camel)
| haspet(n4,guppy)
| haspet(n1,camel) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_403,c_0_401]),c_0_404]) ).
cnf(c_0_409,hypothesis,
( hasgame(n4,backgammon)
| hasgame(n4,quoits)
| hasgame(n2,quoits)
| hasgame(n2,solitaire) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_273,c_0_405]),c_0_202]),c_0_337]),c_0_357]) ).
cnf(c_0_410,hypothesis,
~ hasgame(n4,backgammon),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_328,c_0_406]),c_0_319]),c_0_317]) ).
cnf(c_0_411,hypothesis,
( haspet(n1,camel)
| haspet(n4,camel)
| hasgame(n2,quoits)
| hasgame(n2,solitaire) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_407,c_0_408]),c_0_226]) ).
cnf(c_0_412,hypothesis,
( hasgame(n2,solitaire)
| hasgame(n2,quoits)
| hasgame(n4,quoits) ),
inference(sr,[status(thm)],[c_0_409,c_0_410]) ).
cnf(c_0_413,hypothesis,
( ~ haspet(n1,camel)
| ~ hasgame(n4,quoits) ),
inference(spm,[status(thm)],[c_0_174,c_0_332]) ).
cnf(c_0_414,hypothesis,
( haspet(n1,camel)
| hasgame(n2,solitaire)
| hasgame(n2,quoits) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_384,c_0_411]),c_0_412]) ).
cnf(c_0_415,hypothesis,
( hasgame(n2,quoits)
| hasgame(n2,solitaire) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_413,c_0_414]),c_0_412]) ).
cnf(c_0_416,hypothesis,
( hasgame(n2,quoits)
| samedrink(X1,vodka)
| ~ hasdrink(n2,X1) ),
inference(spm,[status(thm)],[c_0_338,c_0_415]) ).
cnf(c_0_417,hypothesis,
( hasgame(n2,quoits)
| ~ hasperson(n2,swede) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_416,c_0_276]),c_0_389]) ).
cnf(c_0_418,hypothesis,
( hasgame(n2,quoits)
| hascolor(n5,green)
| hasperson(n5,swede) ),
inference(spm,[status(thm)],[c_0_417,c_0_356]) ).
cnf(c_0_419,hypothesis,
( ~ haspet(X1,guppy)
| ~ hasperson(X2,italian)
| ~ nextto(X2,X1) ),
inference(spm,[status(thm)],[c_0_215,c_0_296]) ).
cnf(c_0_420,hypothesis,
( haspet(n5,guppy)
| hasgame(n2,quoits)
| hasperson(n5,swede) ),
inference(spm,[status(thm)],[c_0_417,c_0_380]) ).
cnf(c_0_421,hypothesis,
( hasgame(n2,quoits)
| hascolor(n5,green)
| sameperson(X1,swede)
| ~ hasperson(n5,X1) ),
inference(spm,[status(thm)],[c_0_110,c_0_418]) ).
cnf(c_0_422,hypothesis,
( haspet(n1,camel)
| haspet(n4,camel)
| ~ hasperson(X1,italian)
| ~ nextto(X1,n4) ),
inference(spm,[status(thm)],[c_0_419,c_0_408]) ).
cnf(c_0_423,hypothesis,
( haspet(n5,guppy)
| hasgame(n2,quoits)
| samedrink(X1,coffee)
| ~ hasdrink(n5,X1) ),
inference(spm,[status(thm)],[c_0_293,c_0_420]) ).
cnf(c_0_424,hypothesis,
( hasgame(n2,quoits)
| hascolor(n5,green) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_421,c_0_124]),c_0_377]),c_0_287]) ).
cnf(c_0_425,hypothesis,
( haspet(n4,camel)
| haspet(n1,camel)
| ~ haspet(X1,guppy)
| ~ nextto(X1,n4) ),
inference(spm,[status(thm)],[c_0_422,c_0_279]) ).
cnf(c_0_426,hypothesis,
( haspet(n5,guppy)
| hasgame(n2,quoits) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_423,c_0_183]),c_0_311]),c_0_424]) ).
cnf(c_0_427,hypothesis,
( hasgame(n4,backgammon)
| hasgame(n4,quoits)
| hasgame(n4,solitaire)
| hasperson(n2,swede)
| hasperson(n5,swede) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_273,c_0_353]),c_0_172]),c_0_357]) ).
cnf(c_0_428,hypothesis,
( haspet(n1,camel)
| haspet(n4,camel)
| hasgame(n2,quoits) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_425,c_0_426]),c_0_298])]) ).
cnf(c_0_429,hypothesis,
( hasgame(n4,solitaire)
| hasgame(n4,quoits)
| hasperson(n5,swede)
| hasperson(n2,swede) ),
inference(sr,[status(thm)],[c_0_427,c_0_410]) ).
cnf(c_0_430,hypothesis,
( hasgame(n2,quoits)
| ~ hasgame(n4,quoits) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_384,c_0_428]),c_0_413]) ).
cnf(c_0_431,hypothesis,
( hasgame(n4,solitaire)
| hasgame(n2,quoits)
| hasperson(n5,swede) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_417,c_0_429]),c_0_430]) ).
cnf(c_0_432,hypothesis,
( hasgame(n2,quoits)
| hasgame(n4,solitaire)
| sameperson(X1,swede)
| ~ hasperson(n5,X1) ),
inference(spm,[status(thm)],[c_0_110,c_0_431]) ).
cnf(c_0_433,hypothesis,
( ~ hasgame(n4,charades)
| ~ hasperson(n3,american) ),
inference(spm,[status(thm)],[c_0_312,c_0_343]) ).
cnf(c_0_434,hypothesis,
~ nextto(n2,n4),
house_2_not_nextto_4 ).
cnf(c_0_435,hypothesis,
~ nextto(n2,n5),
house_2_not_nextto_5 ).
cnf(c_0_436,axiom,
( samehouse(X1,X2)
| ~ hasgame(X1,X3)
| ~ hasgame(X2,X3) ),
games_have_unique_houses ).
cnf(c_0_437,hypothesis,
( hasgame(n4,solitaire)
| hasgame(n2,quoits) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_432,c_0_279]),c_0_364]),c_0_426]) ).
cnf(c_0_438,hypothesis,
( ~ hasgame(n4,charades)
| ~ hasgame(n3,charades) ),
inference(spm,[status(thm)],[c_0_433,c_0_243]) ).
cnf(c_0_439,hypothesis,
( ~ haspet(n4,camel)
| ~ hasgame(n2,quoits) ),
inference(spm,[status(thm)],[c_0_434,c_0_348]) ).
cnf(c_0_440,hypothesis,
( ~ haspet(n5,camel)
| ~ hasgame(n2,quoits) ),
inference(spm,[status(thm)],[c_0_435,c_0_348]) ).
cnf(c_0_441,hypothesis,
( hasgame(n2,quoits)
| samehouse(X1,n4)
| ~ hasgame(X1,solitaire) ),
inference(spm,[status(thm)],[c_0_436,c_0_437]) ).
cnf(c_0_442,hypothesis,
( hasgame(n4,solitaire)
| hasgame(n4,quoits)
| hasgame(n4,racquetball)
| hasgame(n4,backgammon)
| ~ hasgame(n3,charades) ),
inference(spm,[status(thm)],[c_0_438,c_0_258]) ).
cnf(c_0_443,hypothesis,
( haspet(n3,camel)
| haspet(n1,camel)
| ~ hasgame(n2,quoits) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_439,c_0_189]),c_0_440]),c_0_384]) ).
cnf(c_0_444,hypothesis,
hasgame(n2,quoits),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_441,c_0_415]),c_0_342]) ).
cnf(c_0_445,hypothesis,
( hasgame(n3,solitaire)
| hasgame(n3,quoits)
| hasgame(n3,backgammon)
| hasgame(n4,backgammon)
| hasgame(n4,quoits)
| hasgame(n4,solitaire) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_442,c_0_258]),c_0_172]),c_0_187]) ).
cnf(c_0_446,hypothesis,
( haspet(n1,camel)
| haspet(n3,camel) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_443,c_0_444])]) ).
cnf(c_0_447,hypothesis,
( haspet(n1,camel)
| haspet(n1,toad)
| haspet(n5,guppy)
| haspet(n5,camel)
| hasgame(n5,backgammon) ),
inference(spm,[status(thm)],[c_0_219,c_0_318]) ).
cnf(c_0_448,hypothesis,
( hasgame(n4,solitaire)
| hasgame(n4,quoits)
| hasgame(n3,backgammon)
| hasgame(n3,quoits)
| hasgame(n3,solitaire) ),
inference(sr,[status(thm)],[c_0_445,c_0_410]) ).
cnf(c_0_449,hypothesis,
~ hasgame(n3,quoits),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_384,c_0_446]),c_0_369]) ).
cnf(c_0_450,hypothesis,
( haspet(n5,camel)
| haspet(n1,toad)
| haspet(n1,camel)
| hasgame(n5,backgammon)
| ~ hasperson(X1,italian)
| ~ nextto(X1,n5) ),
inference(spm,[status(thm)],[c_0_419,c_0_447]) ).
cnf(c_0_451,hypothesis,
~ haspet(n4,camel),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_439,c_0_444])]) ).
cnf(c_0_452,hypothesis,
( hasgame(n3,solitaire)
| hasgame(n3,backgammon)
| hasgame(n4,quoits)
| hasgame(n4,solitaire) ),
inference(sr,[status(thm)],[c_0_448,c_0_449]) ).
cnf(c_0_453,hypothesis,
( haspet(n5,guppy)
| haspet(n3,guppy)
| hasgame(n4,solitaire)
| hasgame(n4,quoits)
| hasgame(n4,backgammon) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_322,c_0_189]),c_0_172]),c_0_301]),c_0_239]) ).
cnf(c_0_454,hypothesis,
( haspet(n1,camel)
| haspet(n1,toad)
| haspet(n5,camel)
| hasgame(n5,backgammon)
| ~ haspet(X1,guppy)
| ~ nextto(X1,n5) ),
inference(spm,[status(thm)],[c_0_450,c_0_279]) ).
cnf(c_0_455,hypothesis,
( haspet(n1,camel)
| haspet(n4,guppy) ),
inference(sr,[status(thm)],[c_0_408,c_0_451]) ).
cnf(c_0_456,hypothesis,
~ haspet(n5,camel),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_440,c_0_444])]) ).
cnf(c_0_457,hypothesis,
( hasgame(n4,quoits)
| hasgame(n3,backgammon)
| hasgame(n3,solitaire)
| samedrink(X1,vodka)
| ~ hasdrink(n4,X1) ),
inference(spm,[status(thm)],[c_0_338,c_0_452]) ).
cnf(c_0_458,axiom,
~ samedrink(lemonade,vodka),
lemonade_not_vodka ).
cnf(c_0_459,hypothesis,
( hasgame(n3,backgammon)
| hasgame(n3,solitaire)
| hascolor(n5,red) ),
inference(sr,[status(thm)],[c_0_308,c_0_449]) ).
cnf(c_0_460,hypothesis,
( hasgame(n5,backgammon)
| samepet(X1,toad)
| ~ haspet(n3,X1) ),
inference(spm,[status(thm)],[c_0_284,c_0_401]) ).
cnf(c_0_461,hypothesis,
( haspet(n3,guppy)
| haspet(n5,guppy)
| hasgame(n4,quoits)
| hasgame(n4,solitaire) ),
inference(sr,[status(thm)],[c_0_453,c_0_410]) ).
cnf(c_0_462,hypothesis,
( haspet(n1,toad)
| haspet(n1,camel)
| hasgame(n5,backgammon) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_454,c_0_455]),c_0_281])]),c_0_456]) ).
cnf(c_0_463,hypothesis,
( hasgame(n3,solitaire)
| hasgame(n3,backgammon)
| hasgame(n4,quoits)
| ~ hascolor(n4,green) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_457,c_0_183]),c_0_458]) ).
cnf(c_0_464,hypothesis,
( hasgame(n3,solitaire)
| hasgame(n3,backgammon)
| ~ hascolor(n5,green) ),
inference(spm,[status(thm)],[c_0_307,c_0_459]) ).
cnf(c_0_465,hypothesis,
( haspet(n5,guppy)
| hasgame(n4,solitaire)
| hasgame(n4,quoits)
| hasgame(n5,backgammon) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_460,c_0_461]),c_0_306]) ).
cnf(c_0_466,hypothesis,
( haspet(n1,camel)
| hasgame(n5,backgammon) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_219,c_0_462]),c_0_265]) ).
cnf(c_0_467,hypothesis,
( hasgame(n4,quoits)
| hasgame(n3,backgammon)
| hasgame(n3,solitaire) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_463,c_0_131]),c_0_218]),c_0_125]),c_0_196]),c_0_464]) ).
cnf(c_0_468,hypothesis,
( hasgame(n5,backgammon)
| hasgame(n4,quoits)
| hasgame(n4,solitaire)
| ~ hasperson(X1,italian)
| ~ nextto(X1,n5) ),
inference(spm,[status(thm)],[c_0_419,c_0_465]) ).
cnf(c_0_469,hypothesis,
( hasgame(n5,backgammon)
| ~ hasgame(n4,quoits) ),
inference(spm,[status(thm)],[c_0_413,c_0_466]) ).
cnf(c_0_470,hypothesis,
( hasgame(n3,solitaire)
| hasgame(n3,backgammon)
| samehouse(X1,n4)
| ~ hasgame(X1,quoits) ),
inference(spm,[status(thm)],[c_0_436,c_0_467]) ).
cnf(c_0_471,hypothesis,
( hasgame(n4,solitaire)
| hasgame(n5,backgammon)
| ~ haspet(X1,guppy)
| ~ nextto(X1,n5) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_468,c_0_279]),c_0_469]) ).
cnf(c_0_472,hypothesis,
( hasgame(n3,backgammon)
| hasgame(n3,solitaire) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_470,c_0_444]),c_0_342]) ).
cnf(c_0_473,hypothesis,
( haspet(n5,guppy)
| haspet(n3,guppy)
| hasgame(n5,backgammon)
| hasgame(n4,solitaire) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_471,c_0_189]),c_0_281])]),c_0_301]),c_0_239]) ).
cnf(c_0_474,hypothesis,
( hasgame(n3,backgammon)
| samedrink(X1,vodka)
| ~ hasdrink(n3,X1) ),
inference(spm,[status(thm)],[c_0_338,c_0_472]) ).
cnf(c_0_475,hypothesis,
( hascolor(n5,green)
| ~ haspet(n5,guppy) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_333,c_0_305]),c_0_335]) ).
cnf(c_0_476,hypothesis,
( haspet(n5,guppy)
| hasgame(n4,solitaire)
| hasgame(n5,backgammon) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_460,c_0_473]),c_0_306]) ).
cnf(c_0_477,hypothesis,
( ~ hasgame(n5,backgammon)
| ~ hasgame(n3,backgammon) ),
inference(spm,[status(thm)],[c_0_330,c_0_261]) ).
cnf(c_0_478,hypothesis,
hasgame(n3,backgammon),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_474,c_0_155]),c_0_352]) ).
cnf(c_0_479,hypothesis,
( hasgame(X1,charades)
| ~ hasperson(X1,american) ),
c17 ).
cnf(c_0_480,axiom,
( hasperson(X1,englishman)
| hasperson(X1,italian)
| hasperson(X1,swede)
| hasperson(X1,russian)
| hasperson(X1,american) ),
every_house_has_a_national ).
cnf(c_0_481,hypothesis,
( hascolor(n5,green)
| samehouse(X1,n5)
| ~ hascolor(X1,red) ),
inference(spm,[status(thm)],[c_0_113,c_0_287]) ).
cnf(c_0_482,hypothesis,
( hasgame(n5,backgammon)
| hasgame(n5,quoits)
| hasgame(n5,solitaire)
| hascolor(n3,red) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_273,c_0_315]),c_0_171]),c_0_275]) ).
cnf(c_0_483,hypothesis,
( ~ haspet(n3,camel)
| ~ hasgame(n5,quoits) ),
inference(spm,[status(thm)],[c_0_347,c_0_332]) ).
cnf(c_0_484,hypothesis,
( ~ haspet(n1,camel)
| ~ hasgame(n5,quoits) ),
inference(spm,[status(thm)],[c_0_176,c_0_332]) ).
cnf(c_0_485,hypothesis,
( hasgame(n5,backgammon)
| hasgame(n4,solitaire)
| hascolor(n5,green) ),
inference(spm,[status(thm)],[c_0_475,c_0_476]) ).
cnf(c_0_486,hypothesis,
~ hasgame(n5,backgammon),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_477,c_0_478])]) ).
cnf(c_0_487,hypothesis,
( haspet(n1,camel)
| samepet(X1,camel)
| ~ haspet(n3,X1) ),
inference(spm,[status(thm)],[c_0_199,c_0_446]) ).
cnf(c_0_488,axiom,
~ samepet(toad,camel),
toad_not_camel ).
cnf(c_0_489,hypothesis,
( hasgame(X1,charades)
| hasperson(X1,russian)
| hasperson(X1,swede)
| hasperson(X1,italian)
| hasperson(X1,englishman) ),
inference(spm,[status(thm)],[c_0_479,c_0_480]) ).
cnf(c_0_490,hypothesis,
( hasgame(n5,solitaire)
| hasgame(n5,quoits)
| hasgame(n5,backgammon)
| hascolor(n5,green) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_481,c_0_482]),c_0_241]) ).
cnf(c_0_491,hypothesis,
~ hasgame(n5,quoits),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_483,c_0_446]),c_0_484]) ).
cnf(c_0_492,hypothesis,
( hasgame(X1,solitaire)
| ~ hasdrink(X1,vodka) ),
c16 ).
cnf(c_0_493,hypothesis,
( hasgame(n4,solitaire)
| hascolor(n5,green) ),
inference(sr,[status(thm)],[c_0_485,c_0_486]) ).
cnf(c_0_494,hypothesis,
( haspet(n1,camel)
| ~ hasgame(n3,backgammon) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_487,c_0_261]),c_0_488]) ).
cnf(c_0_495,hypothesis,
( hasgame(X1,charades)
| hasperson(X1,englishman)
| hasperson(X1,italian)
| hasperson(X1,russian)
| samedrink(X2,coffee)
| ~ hasdrink(X1,X2) ),
inference(spm,[status(thm)],[c_0_293,c_0_489]) ).
cnf(c_0_496,hypothesis,
( hasgame(n5,backgammon)
| hasgame(n5,solitaire)
| hascolor(n5,green) ),
inference(sr,[status(thm)],[c_0_490,c_0_491]) ).
cnf(c_0_497,hypothesis,
( hasgame(n4,solitaire)
| hasdrink(n5,vodka)
| hasdrink(n3,vodka)
| hasdrink(n2,vodka)
| hasdrink(n1,vodka) ),
inference(spm,[status(thm)],[c_0_492,c_0_292]) ).
cnf(c_0_498,hypothesis,
( hasgame(n4,solitaire)
| hasdrink(n1,coffee)
| hasperson(n2,swede)
| hasperson(n4,swede) ),
inference(spm,[status(thm)],[c_0_382,c_0_493]) ).
cnf(c_0_499,hypothesis,
( ~ hasgame(n4,quoits)
| ~ hasgame(n3,backgammon) ),
inference(spm,[status(thm)],[c_0_413,c_0_494]) ).
cnf(c_0_500,hypothesis,
( hasgame(X1,charades)
| hasperson(X1,russian)
| hasperson(X1,italian)
| hasperson(X1,englishman)
| ~ hascolor(X1,green) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_495,c_0_183]),c_0_311]) ).
cnf(c_0_501,hypothesis,
( hasgame(n5,solitaire)
| hascolor(n5,green) ),
inference(sr,[status(thm)],[c_0_496,c_0_486]) ).
cnf(c_0_502,hypothesis,
( hasgame(n4,solitaire)
| hasdrink(n1,vodka)
| hasdrink(n3,vodka)
| hasdrink(n5,vodka)
| samedrink(X1,vodka)
| ~ hasdrink(n2,X1) ),
inference(spm,[status(thm)],[c_0_154,c_0_497]) ).
cnf(c_0_503,hypothesis,
( hasgame(n4,solitaire)
| hasperson(n4,swede)
| hasperson(n2,swede) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_291,c_0_498]),c_0_294]) ).
cnf(c_0_504,hypothesis,
~ hasgame(n4,quoits),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_499,c_0_478])]) ).
cnf(c_0_505,hypothesis,
( hasgame(n5,solitaire)
| hasgame(n5,charades)
| hasperson(n5,englishman)
| hasperson(n5,italian)
| hasperson(n5,russian) ),
inference(spm,[status(thm)],[c_0_500,c_0_501]) ).
cnf(c_0_506,hypothesis,
( hasgame(n4,solitaire)
| hasdrink(n5,vodka)
| hasdrink(n3,vodka)
| hasdrink(n1,vodka)
| ~ hasperson(n2,swede) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_502,c_0_276]),c_0_389]) ).
cnf(c_0_507,hypothesis,
( hasgame(n4,solitaire)
| hasperson(n2,swede) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_273,c_0_503]),c_0_504]),c_0_172]),c_0_410]),c_0_357]) ).
cnf(c_0_508,hypothesis,
( hasgame(n5,charades)
| hasgame(n5,solitaire)
| hasperson(n5,russian)
| hasperson(n5,englishman) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_273,c_0_505]),c_0_491]),c_0_171]),c_0_486]),c_0_303]) ).
cnf(c_0_509,hypothesis,
( hasgame(n4,solitaire)
| hasdrink(n1,vodka)
| hasdrink(n3,vodka)
| hasdrink(n5,vodka) ),
inference(spm,[status(thm)],[c_0_506,c_0_507]) ).
cnf(c_0_510,hypothesis,
( ~ hasgame(n5,charades)
| ~ hasperson(n1,american) ),
inference(spm,[status(thm)],[c_0_121,c_0_343]) ).
cnf(c_0_511,hypothesis,
( hasgame(n5,charades)
| hasgame(n5,solitaire)
| hasperson(n5,russian) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_273,c_0_508]),c_0_491]),c_0_171]),c_0_486]),c_0_275]) ).
cnf(c_0_512,axiom,
~ sameperson(russian,american),
russian_not_american ).
cnf(c_0_513,hypothesis,
( hasgame(n4,solitaire)
| hasdrink(n5,vodka)
| hasdrink(n1,vodka)
| samedrink(X1,vodka)
| ~ hasdrink(n3,X1) ),
inference(spm,[status(thm)],[c_0_154,c_0_509]) ).
cnf(c_0_514,hypothesis,
( hasgame(n4,charades)
| hasperson(n5,american)
| hasperson(n3,american)
| hasperson(n2,american)
| hasperson(n1,american) ),
inference(spm,[status(thm)],[c_0_479,c_0_143]) ).
cnf(c_0_515,axiom,
( samehouse(X1,X2)
| ~ hasdrink(X1,X3)
| ~ hasdrink(X2,X3) ),
drinks_have_unique_houses ).
cnf(c_0_516,hypothesis,
( ~ hasgame(n5,charades)
| ~ hasgame(n1,charades) ),
inference(spm,[status(thm)],[c_0_510,c_0_243]) ).
cnf(c_0_517,hypothesis,
( hasgame(n5,charades)
| hasgame(n5,solitaire) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_273,c_0_511]),c_0_491]),c_0_171]),c_0_486]),c_0_512]) ).
cnf(c_0_518,hypothesis,
( hasgame(n4,solitaire)
| hasdrink(n1,vodka)
| hasdrink(n5,vodka) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_513,c_0_155]),c_0_352]) ).
cnf(c_0_519,hypothesis,
( hasgame(n4,charades)
| hasgame(n2,charades)
| hasperson(n1,american)
| hasperson(n3,american)
| hasperson(n5,american) ),
inference(spm,[status(thm)],[c_0_479,c_0_514]) ).
cnf(c_0_520,hypothesis,
( samepet(X1,toad)
| ~ haspet(n3,X1) ),
inference(spm,[status(thm)],[c_0_284,c_0_478]) ).
cnf(c_0_521,hypothesis,
( samehouse(X1,X2)
| ~ hasgame(X2,solitaire)
| ~ hasdrink(X1,vodka) ),
inference(spm,[status(thm)],[c_0_515,c_0_321]) ).
cnf(c_0_522,hypothesis,
( hasgame(n5,solitaire)
| ~ hasgame(n1,charades) ),
inference(spm,[status(thm)],[c_0_516,c_0_517]) ).
cnf(c_0_523,hypothesis,
( hasgame(n4,solitaire)
| hasdrink(n1,vodka)
| samedrink(X1,vodka)
| ~ hasdrink(n5,X1) ),
inference(spm,[status(thm)],[c_0_154,c_0_518]) ).
cnf(c_0_524,hypothesis,
( hasgame(n2,charades)
| hasgame(n4,charades)
| hasgame(n3,charades)
| hasperson(n5,american)
| hasperson(n1,american) ),
inference(spm,[status(thm)],[c_0_479,c_0_519]) ).
cnf(c_0_525,hypothesis,
~ haspet(n3,guppy),
inference(spm,[status(thm)],[c_0_306,c_0_520]) ).
cnf(c_0_526,hypothesis,
( samehouse(X1,n5)
| ~ hasgame(n1,charades)
| ~ hasdrink(X1,vodka) ),
inference(spm,[status(thm)],[c_0_521,c_0_522]) ).
cnf(c_0_527,hypothesis,
( hasgame(n4,solitaire)
| hasdrink(n1,vodka) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_523,c_0_183]),c_0_458]),c_0_493]) ).
cnf(c_0_528,hypothesis,
( hasgame(n3,charades)
| hasgame(n4,charades)
| hasgame(n2,charades)
| hasperson(n1,american)
| sameperson(X1,american)
| ~ hasperson(n5,X1) ),
inference(spm,[status(thm)],[c_0_110,c_0_524]) ).
cnf(c_0_529,hypothesis,
( haspet(n4,guppy)
| hasperson(n5,italian) ),
inference(sr,[status(thm)],[c_0_251,c_0_525]) ).
cnf(c_0_530,hypothesis,
( samehouse(X1,n5)
| ~ hasgame(n1,charades)
| ~ hasgame(X1,solitaire) ),
inference(spm,[status(thm)],[c_0_436,c_0_522]) ).
cnf(c_0_531,hypothesis,
( hasgame(n4,solitaire)
| ~ hasgame(n1,charades) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_526,c_0_527]),c_0_121]) ).
cnf(c_0_532,hypothesis,
( haspet(n4,guppy)
| hasgame(n2,charades)
| hasgame(n4,charades)
| hasgame(n3,charades)
| hasperson(n1,american) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_528,c_0_529]),c_0_303]) ).
cnf(c_0_533,hypothesis,
~ hasgame(n1,charades),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_226,c_0_530]),c_0_531]) ).
cnf(c_0_534,axiom,
~ samehouse(n2,n5),
house_2_not_5 ).
cnf(c_0_535,hypothesis,
( ~ hasgame(n5,charades)
| ~ hasperson(n4,american) ),
inference(spm,[status(thm)],[c_0_226,c_0_343]) ).
cnf(c_0_536,hypothesis,
( haspet(n4,guppy)
| hasgame(n3,charades)
| hasgame(n4,charades)
| hasgame(n2,charades) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_479,c_0_532]),c_0_533]) ).
cnf(c_0_537,hypothesis,
( ~ hasgame(n5,charades)
| ~ hasperson(n3,american) ),
inference(spm,[status(thm)],[c_0_241,c_0_343]) ).
cnf(c_0_538,hypothesis,
( ~ hasgame(n5,charades)
| ~ hasperson(n2,american) ),
inference(spm,[status(thm)],[c_0_534,c_0_343]) ).
cnf(c_0_539,hypothesis,
( ~ hasgame(n5,charades)
| ~ hasgame(n4,charades) ),
inference(spm,[status(thm)],[c_0_535,c_0_243]) ).
cnf(c_0_540,hypothesis,
( hasgame(n2,charades)
| hasgame(n4,charades)
| hasgame(n3,charades)
| hasgame(n4,solitaire) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_322,c_0_536]),c_0_410]),c_0_172]),c_0_504]) ).
cnf(c_0_541,hypothesis,
( ~ hasgame(n5,charades)
| ~ hasgame(n3,charades) ),
inference(spm,[status(thm)],[c_0_537,c_0_243]) ).
cnf(c_0_542,hypothesis,
( ~ hasgame(n5,charades)
| ~ hasgame(n2,charades) ),
inference(spm,[status(thm)],[c_0_538,c_0_243]) ).
cnf(c_0_543,hypothesis,
( hasgame(n4,solitaire)
| ~ hasgame(n5,charades) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_539,c_0_540]),c_0_541]),c_0_542]) ).
cnf(c_0_544,hypothesis,
( samehouse(X1,n4)
| ~ hasgame(n5,charades)
| ~ hasgame(X1,solitaire) ),
inference(spm,[status(thm)],[c_0_436,c_0_543]) ).
cnf(c_0_545,hypothesis,
( ~ hasgame(n5,charades)
| ~ hasgame(n1,solitaire) ),
inference(spm,[status(thm)],[c_0_129,c_0_544]) ).
cnf(c_0_546,hypothesis,
( hascolor(X1,green)
| ~ hasdrink(X1,lemonade) ),
lemonade_in_green_house1 ).
cnf(c_0_547,hypothesis,
( hasgame(n5,solitaire)
| ~ hasgame(n1,solitaire) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_545,c_0_258]),c_0_486]),c_0_171]),c_0_491]) ).
cnf(c_0_548,hypothesis,
( hasdrink(n5,lemonade)
| hasdrink(n2,lemonade)
| hasdrink(n1,lemonade)
| hascolor(n4,green) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_546,c_0_292]),c_0_182]) ).
cnf(c_0_549,hypothesis,
( samehouse(X1,n5)
| ~ hasgame(n1,solitaire)
| ~ hasdrink(X1,vodka) ),
inference(spm,[status(thm)],[c_0_521,c_0_547]) ).
cnf(c_0_550,hypothesis,
( hasgame(n4,solitaire)
| hasgame(n1,solitaire) ),
inference(spm,[status(thm)],[c_0_492,c_0_527]) ).
cnf(c_0_551,hypothesis,
( hasdrink(n1,lemonade)
| hasdrink(n5,lemonade)
| hascolor(n4,green) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_546,c_0_548]),c_0_125]) ).
cnf(c_0_552,hypothesis,
( haspet(n4,guppy)
| hascolor(n5,red)
| hasperson(n5,italian) ),
inference(spm,[status(thm)],[c_0_354,c_0_225]) ).
cnf(c_0_553,hypothesis,
( hasgame(n5,solitaire)
| hasgame(n5,quoits)
| hasgame(n5,backgammon)
| ~ hascolor(n5,red) ),
inference(spm,[status(thm)],[c_0_270,c_0_482]) ).
cnf(c_0_554,hypothesis,
hasgame(n4,solitaire),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_549,c_0_527]),c_0_121]),c_0_550]) ).
cnf(c_0_555,plain,
( hasdrink(n5,X1)
| hasdrink(n3,X1)
| hasdrink(n2,X1)
| hasdrink(n1,X1)
| samedrink(X2,X1)
| ~ hasdrink(n4,X2) ),
inference(spm,[status(thm)],[c_0_154,c_0_292]) ).
cnf(c_0_556,hypothesis,
( hasdrink(n1,lemonade)
| hasdrink(n1,coffee)
| hascolor(n4,green)
| hasperson(n4,swede)
| hasperson(n2,swede) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_375,c_0_551]),c_0_311]) ).
cnf(c_0_557,negated_conjecture,
( ~ hasperson(n1,X1)
| ~ hasperson(n2,X2)
| ~ hasperson(n3,X3)
| ~ hasperson(n4,X4)
| ~ hasperson(n5,X5)
| ~ hascolor(n1,X6)
| ~ hascolor(n2,X7)
| ~ hascolor(n3,X8)
| ~ hascolor(n4,X9)
| ~ hascolor(n5,X10)
| ~ hasdrink(n1,X11)
| ~ hasdrink(n2,X12)
| ~ hasdrink(n3,X13)
| ~ hasdrink(n4,X14)
| ~ hasdrink(n5,X15)
| ~ hasgame(n1,X16)
| ~ hasgame(n2,X17)
| ~ hasgame(n3,X18)
| ~ hasgame(n4,X19)
| ~ hasgame(n5,X20)
| ~ haspet(n1,X21)
| ~ haspet(n2,X22)
| ~ haspet(n3,X23)
| ~ haspet(n4,X24)
| ~ haspet(n5,X25) ),
find_out_house_details ).
cnf(c_0_558,hypothesis,
( haspet(n4,guppy)
| hasgame(n5,backgammon)
| hasgame(n5,quoits)
| hasgame(n5,solitaire) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_273,c_0_552]),c_0_171]),c_0_303]),c_0_553]) ).
cnf(c_0_559,hypothesis,
( samehouse(X1,n4)
| ~ hasgame(X1,solitaire) ),
inference(spm,[status(thm)],[c_0_436,c_0_554]) ).
cnf(c_0_560,hypothesis,
( hasdrink(n1,X1)
| hasdrink(n2,X1)
| hasdrink(n3,X1)
| hasdrink(n5,X1)
| samedrink(vodka,X1)
| ~ hasgame(n4,solitaire) ),
inference(spm,[status(thm)],[c_0_555,c_0_321]) ).
cnf(c_0_561,hypothesis,
( hasgame(n1,solitaire)
| samedrink(X1,vodka)
| ~ hasdrink(n4,X1) ),
inference(spm,[status(thm)],[c_0_338,c_0_550]) ).
cnf(c_0_562,hypothesis,
( hasdrink(n1,lemonade)
| hascolor(n4,green)
| hasperson(n2,swede)
| hasperson(n4,swede) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_291,c_0_556]),c_0_294]) ).
cnf(c_0_563,negated_conjecture,
( ~ haspet(n2,X1)
| ~ haspet(n3,X2)
| ~ haspet(n4,X3)
| ~ haspet(n5,X4)
| ~ hasgame(n1,X5)
| ~ hasgame(n2,X6)
| ~ hasgame(n3,X7)
| ~ hasgame(n4,X8)
| ~ hasgame(n5,X9)
| ~ hasdrink(n1,X10)
| ~ hasdrink(n2,X11)
| ~ hasdrink(n3,X12)
| ~ hasdrink(n4,X13)
| ~ hasdrink(n5,X14)
| ~ hascolor(n1,X15)
| ~ hascolor(n2,X16)
| ~ hascolor(n3,X17)
| ~ hascolor(n4,X18)
| ~ hascolor(n5,X19)
| ~ hasperson(n1,X20)
| ~ hasperson(n2,X21)
| ~ hasperson(n3,X22)
| ~ hasperson(n4,X23)
| ~ hasperson(n5,X24) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_557,c_0_262]),c_0_301]),c_0_300]),c_0_557]),c_0_557]) ).
cnf(c_0_564,hypothesis,
haspet(n2,rat),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_200,c_0_221])]) ).
cnf(c_0_565,hypothesis,
( haspet(n4,guppy)
| hasgame(n5,solitaire)
| hasgame(n5,backgammon) ),
inference(sr,[status(thm)],[c_0_558,c_0_491]) ).
cnf(c_0_566,hypothesis,
( ~ hasgame(X1,solitaire)
| ~ nextto(X1,n4) ),
inference(spm,[status(thm)],[c_0_215,c_0_559]) ).
cnf(c_0_567,axiom,
~ samedrink(vodka,unknown_drink),
vodka_not_unknown ).
cnf(c_0_568,hypothesis,
( hasdrink(n5,X1)
| hasdrink(n3,X1)
| hasdrink(n2,X1)
| hasdrink(n1,X1)
| samedrink(vodka,X1) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_560,c_0_554])]) ).
cnf(c_0_569,hypothesis,
( hasgame(n1,solitaire)
| ~ hasperson(n4,swede) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_561,c_0_276]),c_0_389]) ).
cnf(c_0_570,hypothesis,
( hascolor(n4,green)
| hasperson(n4,swede)
| hasperson(n2,swede) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_546,c_0_562]),c_0_218]) ).
cnf(c_0_571,hypothesis,
( hasgame(n1,solitaire)
| ~ hascolor(n4,green) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_561,c_0_183]),c_0_458]) ).
cnf(c_0_572,hypothesis,
( ~ haspet(n3,X1)
| ~ haspet(n4,X2)
| ~ haspet(n5,X3)
| ~ hasgame(n1,X4)
| ~ hasgame(n2,X5)
| ~ hasgame(n3,X6)
| ~ hasgame(n4,X7)
| ~ hasgame(n5,X8)
| ~ hasdrink(n1,X9)
| ~ hasdrink(n2,X10)
| ~ hasdrink(n3,X11)
| ~ hasdrink(n4,X12)
| ~ hasdrink(n5,X13)
| ~ hascolor(n1,X14)
| ~ hascolor(n2,X15)
| ~ hascolor(n3,X16)
| ~ hascolor(n4,X17)
| ~ hascolor(n5,X18)
| ~ hasperson(n1,X19)
| ~ hasperson(n2,X20)
| ~ hasperson(n3,X21)
| ~ hasperson(n4,X22)
| ~ hasperson(n5,X23) ),
inference(spm,[status(thm)],[c_0_563,c_0_564]) ).
cnf(c_0_573,hypothesis,
( haspet(n4,guppy)
| hasgame(n5,solitaire) ),
inference(sr,[status(thm)],[c_0_565,c_0_486]) ).
cnf(c_0_574,hypothesis,
~ hasgame(n5,solitaire),
inference(spm,[status(thm)],[c_0_566,c_0_298]) ).
cnf(c_0_575,hypothesis,
( hasdrink(n1,unknown_drink)
| hasdrink(n2,unknown_drink)
| hasdrink(n3,unknown_drink)
| hasdrink(n5,unknown_drink) ),
inference(spm,[status(thm)],[c_0_567,c_0_568]) ).
cnf(c_0_576,hypothesis,
( hasgame(n1,solitaire)
| hasperson(n2,swede) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_569,c_0_570]),c_0_571]) ).
cnf(c_0_577,hypothesis,
~ hasgame(n1,solitaire),
inference(spm,[status(thm)],[c_0_129,c_0_559]) ).
cnf(c_0_578,hypothesis,
( ~ haspet(n4,X1)
| ~ haspet(n5,X2)
| ~ hasgame(n1,X3)
| ~ hasgame(n2,X4)
| ~ hasgame(n3,X5)
| ~ hasgame(n4,X6)
| ~ hasgame(n5,X7)
| ~ hasdrink(n1,X8)
| ~ hasdrink(n2,X9)
| ~ hasdrink(n3,X10)
| ~ hasdrink(n4,X11)
| ~ hasdrink(n5,X12)
| ~ hascolor(n1,X13)
| ~ hascolor(n2,X14)
| ~ hascolor(n3,X15)
| ~ hascolor(n4,X16)
| ~ hascolor(n5,X17)
| ~ hasperson(n1,X18)
| ~ hasperson(n2,X19)
| ~ hasperson(n3,X20)
| ~ hasperson(n4,X21)
| ~ hasperson(n5,X22) ),
inference(csr,[status(thm)],[inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_572,c_0_262]),c_0_313]),c_0_525]),c_0_572]),c_0_572]) ).
cnf(c_0_579,hypothesis,
haspet(n4,guppy),
inference(sr,[status(thm)],[c_0_573,c_0_574]) ).
cnf(c_0_580,hypothesis,
( hasdrink(n5,unknown_drink)
| hasdrink(n3,unknown_drink)
| hasdrink(n1,unknown_drink)
| samedrink(X1,unknown_drink)
| ~ hasdrink(n2,X1) ),
inference(spm,[status(thm)],[c_0_154,c_0_575]) ).
cnf(c_0_581,hypothesis,
hasperson(n2,swede),
inference(sr,[status(thm)],[c_0_576,c_0_577]) ).
cnf(c_0_582,axiom,
~ samedrink(coffee,unknown_drink),
coffee_not_known ).
cnf(c_0_583,hypothesis,
( ~ haspet(n5,X1)
| ~ hasgame(n1,X2)
| ~ hasgame(n2,X3)
| ~ hasgame(n3,X4)
| ~ hasgame(n4,X5)
| ~ hasgame(n5,X6)
| ~ hasdrink(n1,X7)
| ~ hasdrink(n2,X8)
| ~ hasdrink(n3,X9)
| ~ hasdrink(n4,X10)
| ~ hasdrink(n5,X11)
| ~ hascolor(n1,X12)
| ~ hascolor(n2,X13)
| ~ hascolor(n3,X14)
| ~ hascolor(n4,X15)
| ~ hascolor(n5,X16)
| ~ hasperson(n1,X17)
| ~ hasperson(n2,X18)
| ~ hasperson(n3,X19)
| ~ hasperson(n4,X20)
| ~ hasperson(n5,X21) ),
inference(spm,[status(thm)],[c_0_578,c_0_579]) ).
cnf(c_0_584,hypothesis,
~ haspet(n5,guppy),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_333,c_0_579])]) ).
cnf(c_0_585,hypothesis,
( hasdrink(n1,unknown_drink)
| hasdrink(n3,unknown_drink)
| hasdrink(n5,unknown_drink) ),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_580,c_0_276]),c_0_581])]),c_0_582]) ).
cnf(c_0_586,hypothesis,
( ~ hasgame(n1,X1)
| ~ hasgame(n2,X2)
| ~ hasgame(n3,X3)
| ~ hasgame(n4,X4)
| ~ hasgame(n5,X5)
| ~ hasdrink(n1,X6)
| ~ hasdrink(n2,X7)
| ~ hasdrink(n3,X8)
| ~ hasdrink(n4,X9)
| ~ hasdrink(n5,X10)
| ~ hascolor(n1,X11)
| ~ hascolor(n2,X12)
| ~ hascolor(n3,X13)
| ~ hascolor(n4,X14)
| ~ hascolor(n5,X15)
| ~ hasperson(n1,X16)
| ~ hasperson(n2,X17)
| ~ hasperson(n3,X18)
| ~ hasperson(n4,X19)
| ~ hasperson(n5,X20) ),
inference(csr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_583,c_0_262]),c_0_584]),c_0_456]),c_0_302]),c_0_583]) ).
cnf(c_0_587,hypothesis,
( hasdrink(n5,unknown_drink)
| hasdrink(n1,unknown_drink)
| samedrink(X1,unknown_drink)
| ~ hasdrink(n3,X1) ),
inference(spm,[status(thm)],[c_0_154,c_0_585]) ).
cnf(c_0_588,axiom,
~ samedrink(milk,unknown_drink),
milk_not_unknown ).
cnf(c_0_589,hypothesis,
( ~ hasgame(n2,X1)
| ~ hasgame(n3,X2)
| ~ hasgame(n4,X3)
| ~ hasgame(n5,X4)
| ~ hasdrink(n1,X5)
| ~ hasdrink(n2,X6)
| ~ hasdrink(n3,X7)
| ~ hasdrink(n4,X8)
| ~ hasdrink(n5,X9)
| ~ hascolor(n1,X10)
| ~ hascolor(n2,X11)
| ~ hascolor(n3,X12)
| ~ hascolor(n4,X13)
| ~ hascolor(n5,X14)
| ~ hasperson(n1,X15)
| ~ hasperson(n2,X16)
| ~ hasperson(n3,X17)
| ~ hasperson(n4,X18)
| ~ hasperson(n5,X19) ),
inference(spm,[status(thm)],[c_0_586,c_0_221]) ).
cnf(c_0_590,hypothesis,
( hasdrink(n1,unknown_drink)
| hasdrink(n5,unknown_drink) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_587,c_0_155]),c_0_588]) ).
cnf(c_0_591,hypothesis,
( hasgame(n1,solitaire)
| hascolor(n5,green) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_571,c_0_131]),c_0_218]),c_0_125]),c_0_196]) ).
cnf(c_0_592,hypothesis,
( ~ hasgame(n3,X1)
| ~ hasgame(n4,X2)
| ~ hasgame(n5,X3)
| ~ hasdrink(n1,X4)
| ~ hasdrink(n2,X5)
| ~ hasdrink(n3,X6)
| ~ hasdrink(n4,X7)
| ~ hasdrink(n5,X8)
| ~ hascolor(n1,X9)
| ~ hascolor(n2,X10)
| ~ hascolor(n3,X11)
| ~ hascolor(n4,X12)
| ~ hascolor(n5,X13)
| ~ hasperson(n1,X14)
| ~ hasperson(n2,X15)
| ~ hasperson(n3,X16)
| ~ hasperson(n4,X17)
| ~ hasperson(n5,X18) ),
inference(spm,[status(thm)],[c_0_589,c_0_444]) ).
cnf(c_0_593,hypothesis,
( hasdrink(n1,unknown_drink)
| samedrink(X1,unknown_drink)
| ~ hasdrink(n5,X1) ),
inference(spm,[status(thm)],[c_0_154,c_0_590]) ).
cnf(c_0_594,hypothesis,
hascolor(n5,green),
inference(sr,[status(thm)],[c_0_591,c_0_577]) ).
cnf(c_0_595,axiom,
~ samedrink(lemonade,unknown_drink),
lemonade_not_unknown ).
cnf(c_0_596,hypothesis,
( ~ hasgame(n4,X1)
| ~ hasgame(n5,X2)
| ~ hasdrink(n1,X3)
| ~ hasdrink(n2,X4)
| ~ hasdrink(n3,X5)
| ~ hasdrink(n4,X6)
| ~ hasdrink(n5,X7)
| ~ hascolor(n1,X8)
| ~ hascolor(n2,X9)
| ~ hascolor(n3,X10)
| ~ hascolor(n4,X11)
| ~ hascolor(n5,X12)
| ~ hasperson(n1,X13)
| ~ hasperson(n2,X14)
| ~ hasperson(n3,X15)
| ~ hasperson(n4,X16)
| ~ hasperson(n5,X17) ),
inference(spm,[status(thm)],[c_0_592,c_0_478]) ).
cnf(c_0_597,hypothesis,
hasdrink(n1,unknown_drink),
inference(sr,[status(thm)],[inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_593,c_0_183]),c_0_594])]),c_0_595]) ).
cnf(c_0_598,hypothesis,
( ~ hasgame(n5,X1)
| ~ hasdrink(n1,X2)
| ~ hasdrink(n2,X3)
| ~ hasdrink(n3,X4)
| ~ hasdrink(n4,X5)
| ~ hasdrink(n5,X6)
| ~ hascolor(n1,X7)
| ~ hascolor(n2,X8)
| ~ hascolor(n3,X9)
| ~ hascolor(n4,X10)
| ~ hascolor(n5,X11)
| ~ hasperson(n1,X12)
| ~ hasperson(n2,X13)
| ~ hasperson(n3,X14)
| ~ hasperson(n4,X15)
| ~ hasperson(n5,X16) ),
inference(spm,[status(thm)],[c_0_596,c_0_554]) ).
cnf(c_0_599,hypothesis,
( samedrink(X1,unknown_drink)
| ~ hasdrink(n1,X1) ),
inference(spm,[status(thm)],[c_0_154,c_0_597]) ).
cnf(c_0_600,hypothesis,
( ~ hasdrink(n1,X1)
| ~ hasdrink(n2,X2)
| ~ hasdrink(n3,X3)
| ~ hasdrink(n4,X4)
| ~ hasdrink(n5,X5)
| ~ hascolor(n1,X6)
| ~ hascolor(n2,X7)
| ~ hascolor(n3,X8)
| ~ hascolor(n4,X9)
| ~ hascolor(n5,X10)
| ~ hasperson(n1,X11)
| ~ hasperson(n2,X12)
| ~ hasperson(n3,X13)
| ~ hasperson(n4,X14)
| ~ hasperson(n5,X15) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_598,c_0_258]),c_0_486]),c_0_171]),c_0_491]),c_0_574]) ).
cnf(c_0_601,axiom,
( hasdrink(X1,lemonade)
| hasdrink(X1,coffee)
| hasdrink(X1,milk)
| hasdrink(X1,vodka)
| hasdrink(X1,unknown_drink) ),
every_house_has_a_drink ).
cnf(c_0_602,hypothesis,
~ hasdrink(n1,lemonade),
inference(spm,[status(thm)],[c_0_595,c_0_599]) ).
cnf(c_0_603,hypothesis,
~ hasdrink(n1,coffee),
inference(spm,[status(thm)],[c_0_582,c_0_599]) ).
cnf(c_0_604,hypothesis,
~ hasdrink(n1,milk),
inference(spm,[status(thm)],[c_0_588,c_0_599]) ).
cnf(c_0_605,hypothesis,
~ hasdrink(n1,vodka),
inference(spm,[status(thm)],[c_0_567,c_0_599]) ).
cnf(c_0_606,hypothesis,
( ~ hasdrink(n2,X1)
| ~ hasdrink(n3,X2)
| ~ hasdrink(n4,X3)
| ~ hasdrink(n5,X4)
| ~ hascolor(n1,X5)
| ~ hascolor(n2,X6)
| ~ hascolor(n3,X7)
| ~ hascolor(n4,X8)
| ~ hascolor(n5,X9)
| ~ hasperson(n1,X10)
| ~ hasperson(n2,X11)
| ~ hasperson(n3,X12)
| ~ hasperson(n4,X13)
| ~ hasperson(n5,X14) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_600,c_0_601]),c_0_602]),c_0_603]),c_0_604]),c_0_605]) ).
cnf(c_0_607,hypothesis,
( ~ hasdrink(n3,X1)
| ~ hasdrink(n4,X2)
| ~ hasdrink(n5,X3)
| ~ hascolor(n1,X4)
| ~ hascolor(n2,X5)
| ~ hascolor(n3,X6)
| ~ hascolor(n4,X7)
| ~ hascolor(n5,X8)
| ~ hasperson(n1,X9)
| ~ hasperson(n2,X10)
| ~ hasperson(n3,X11)
| ~ hasperson(n4,X12)
| ~ hasperson(n5,X13) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_606,c_0_276]),c_0_581])]) ).
cnf(c_0_608,hypothesis,
( ~ hasgame(X1,charades)
| ~ hasperson(X2,american)
| ~ nextto(X2,X1) ),
inference(spm,[status(thm)],[c_0_215,c_0_343]) ).
cnf(c_0_609,hypothesis,
( ~ hasdrink(n4,X1)
| ~ hasdrink(n5,X2)
| ~ hascolor(n1,X3)
| ~ hascolor(n2,X4)
| ~ hascolor(n3,X5)
| ~ hascolor(n4,X6)
| ~ hascolor(n5,X7)
| ~ hasperson(n1,X8)
| ~ hasperson(n2,X9)
| ~ hasperson(n3,X10)
| ~ hasperson(n4,X11)
| ~ hasperson(n5,X12) ),
inference(spm,[status(thm)],[c_0_607,c_0_155]) ).
cnf(c_0_610,hypothesis,
( hasgame(X1,solitaire)
| hasgame(X1,quoits)
| hasgame(X1,racquetball)
| hasgame(X1,backgammon)
| ~ hasperson(X2,american)
| ~ nextto(X2,X1) ),
inference(spm,[status(thm)],[c_0_608,c_0_258]) ).
cnf(c_0_611,hypothesis,
( ~ hasdrink(n5,X1)
| ~ hascolor(n1,X2)
| ~ hascolor(n2,X3)
| ~ hascolor(n3,X4)
| ~ hascolor(n4,X5)
| ~ hascolor(n5,X6)
| ~ hasperson(n1,X7)
| ~ hasperson(n2,X8)
| ~ hasperson(n3,X9)
| ~ hasperson(n4,X10)
| ~ hasperson(n5,X11) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_609,c_0_321]),c_0_554])]) ).
cnf(c_0_612,hypothesis,
( hascolor(X1,blue)
| ~ haspet(n1,camel)
| ~ hasgame(X1,quoits) ),
inference(spm,[status(thm)],[c_0_108,c_0_332]) ).
cnf(c_0_613,hypothesis,
( hasgame(X1,backgammon)
| hasgame(X1,racquetball)
| hasgame(X1,quoits)
| hasgame(X1,solitaire)
| ~ hasgame(X2,charades)
| ~ nextto(X2,X1) ),
inference(spm,[status(thm)],[c_0_610,c_0_243]) ).
cnf(c_0_614,hypothesis,
hasgame(n5,charades),
inference(sr,[status(thm)],[c_0_517,c_0_574]) ).
cnf(c_0_615,hypothesis,
( nextto(X1,X2)
| ~ hascolor(X2,green)
| ~ hascolor(X1,white) ),
inference(spm,[status(thm)],[c_0_106,c_0_134]) ).
cnf(c_0_616,hypothesis,
( samehouse(X1,n2)
| ~ hasperson(X1,swede) ),
inference(spm,[status(thm)],[c_0_204,c_0_581]) ).
cnf(c_0_617,hypothesis,
( ~ hascolor(n1,X1)
| ~ hascolor(n2,X2)
| ~ hascolor(n3,X3)
| ~ hascolor(n4,X4)
| ~ hascolor(n5,X5)
| ~ hasperson(n1,X6)
| ~ hasperson(n2,X7)
| ~ hasperson(n3,X8)
| ~ hasperson(n4,X9)
| ~ hasperson(n5,X10) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_611,c_0_183]),c_0_594])]) ).
cnf(c_0_618,hypothesis,
( hascolor(X1,blue)
| ~ hasgame(n3,backgammon)
| ~ hasgame(X1,quoits) ),
inference(spm,[status(thm)],[c_0_612,c_0_494]) ).
cnf(c_0_619,hypothesis,
( hasgame(X1,solitaire)
| hasgame(X1,quoits)
| hasgame(X1,racquetball)
| hasgame(X1,backgammon)
| ~ nextto(n5,X1) ),
inference(spm,[status(thm)],[c_0_613,c_0_614]) ).
cnf(c_0_620,hypothesis,
( nextto(X1,X2)
| ~ hascolor(X1,green)
| ~ hascolor(X2,white) ),
inference(spm,[status(thm)],[c_0_163,c_0_615]) ).
cnf(c_0_621,hypothesis,
( hasgame(X1,backgammon)
| hasgame(X1,racquetball)
| hasgame(X1,quoits)
| hasgame(X1,solitaire)
| ~ hascolor(X1,red) ),
inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_273,c_0_124]),c_0_275]) ).
cnf(c_0_622,hypothesis,
( ~ hasperson(X1,swede)
| ~ nextto(X1,n2) ),
inference(spm,[status(thm)],[c_0_215,c_0_616]) ).
cnf(c_0_623,hypothesis,
( ~ hascolor(n2,X1)
| ~ hascolor(n3,X2)
| ~ hascolor(n4,X3)
| ~ hascolor(n5,X4)
| ~ hasperson(n1,X5)
| ~ hasperson(n2,X6)
| ~ hasperson(n3,X7)
| ~ hasperson(n4,X8)
| ~ hasperson(n5,X9) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_617,c_0_114]),c_0_221])]) ).
cnf(c_0_624,hypothesis,
( hascolor(X1,blue)
| ~ hasgame(X1,quoits) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_618,c_0_478])]) ).
cnf(c_0_625,hypothesis,
( hasgame(X1,backgammon)
| hasgame(X1,racquetball)
| hasgame(X1,quoits)
| hasgame(X1,solitaire)
| ~ hascolor(X1,white) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_619,c_0_620]),c_0_594])]) ).
cnf(c_0_626,hypothesis,
( hasgame(X1,solitaire)
| hasgame(X1,quoits)
| hasgame(X1,racquetball)
| hasgame(X1,backgammon)
| hascolor(X1,white)
| hascolor(X1,green)
| hascolor(X1,blue) ),
inference(spm,[status(thm)],[c_0_621,c_0_271]) ).
cnf(c_0_627,hypothesis,
( hasgame(X1,charades)
| hasperson(X1,englishman)
| hasperson(X1,italian)
| hasperson(X1,russian)
| ~ nextto(X1,n2) ),
inference(spm,[status(thm)],[c_0_622,c_0_489]) ).
cnf(c_0_628,hypothesis,
( ~ hascolor(n3,X1)
| ~ hascolor(n4,X2)
| ~ hascolor(n5,X3)
| ~ hasperson(n1,X4)
| ~ hasperson(n2,X5)
| ~ hasperson(n3,X6)
| ~ hasperson(n4,X7)
| ~ hasperson(n5,X8) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_623,c_0_624]),c_0_444])]) ).
cnf(c_0_629,hypothesis,
~ hascolor(n3,white),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_288,c_0_594])]) ).
cnf(c_0_630,hypothesis,
( hasgame(X1,solitaire)
| hasgame(X1,racquetball)
| hasgame(X1,backgammon)
| hascolor(X1,blue)
| hascolor(X1,green) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_625,c_0_626]),c_0_624]) ).
cnf(c_0_631,hypothesis,
( hasgame(X1,charades)
| hasperson(X1,russian)
| hasperson(X1,italian)
| hasperson(X1,englishman)
| ~ hasgame(X1,racquetball) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_627,c_0_175]),c_0_564])]) ).
cnf(c_0_632,hypothesis,
( ~ hascolor(n4,X1)
| ~ hascolor(n5,X2)
| ~ hasperson(n1,X3)
| ~ hasperson(n2,X4)
| ~ hasperson(n3,X5)
| ~ hasperson(n4,X6)
| ~ hasperson(n5,X7) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_628,c_0_271]),c_0_187]),c_0_272]),c_0_196]),c_0_629]) ).
cnf(c_0_633,hypothesis,
hascolor(n4,white),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_169,c_0_594])]) ).
cnf(c_0_634,hypothesis,
( hasgame(X1,backgammon)
| hasgame(X1,solitaire)
| hasgame(X1,charades)
| hascolor(X1,blue)
| hasperson(X1,englishman)
| hasperson(X1,italian)
| hasperson(X1,russian) ),
inference(csr,[status(thm)],[inference(spm,[status(thm)],[c_0_500,c_0_630]),c_0_631]) ).
cnf(c_0_635,hypothesis,
( ~ hascolor(n5,X1)
| ~ hasperson(n1,X2)
| ~ hasperson(n2,X3)
| ~ hasperson(n3,X4)
| ~ hasperson(n4,X5)
| ~ hasperson(n5,X6) ),
inference(spm,[status(thm)],[c_0_632,c_0_633]) ).
cnf(c_0_636,hypothesis,
( haspet(X1,guppy)
| hasgame(X1,charades)
| hasgame(X1,solitaire)
| hasgame(X1,backgammon)
| hascolor(X1,blue)
| hasperson(X1,russian)
| hasperson(X1,englishman) ),
inference(spm,[status(thm)],[c_0_213,c_0_634]) ).
cnf(c_0_637,hypothesis,
( ~ hasperson(n1,X1)
| ~ hasperson(n2,X2)
| ~ hasperson(n3,X3)
| ~ hasperson(n4,X4)
| ~ hasperson(n5,X5) ),
inference(spm,[status(thm)],[c_0_635,c_0_594]) ).
cnf(c_0_638,hypothesis,
( haspet(X1,guppy)
| hasgame(X1,backgammon)
| hasgame(X1,solitaire)
| hasgame(X1,charades)
| hascolor(X1,blue)
| hascolor(X1,red)
| hasperson(X1,russian) ),
inference(spm,[status(thm)],[c_0_142,c_0_636]) ).
cnf(c_0_639,hypothesis,
( ~ hasperson(n2,X1)
| ~ hasperson(n3,X2)
| ~ hasperson(n4,X3)
| ~ hasperson(n5,X4) ),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_637,c_0_638]),c_0_301]),c_0_265]),c_0_577]),c_0_533]),c_0_139]),c_0_137]) ).
cnf(c_0_640,hypothesis,
~ hascolor(n5,red),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_307,c_0_594])]) ).
cnf(c_0_641,hypothesis,
( ~ hasperson(n3,X1)
| ~ hasperson(n4,X2)
| ~ hasperson(n5,X3) ),
inference(spm,[status(thm)],[c_0_639,c_0_581]) ).
cnf(c_0_642,hypothesis,
hascolor(n3,red),
inference(sr,[status(thm)],[c_0_225,c_0_640]) ).
cnf(c_0_643,hypothesis,
~ hasperson(n4,american),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_535,c_0_614])]) ).
cnf(c_0_644,hypothesis,
~ hasperson(n1,american),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_510,c_0_614])]) ).
cnf(c_0_645,hypothesis,
~ hasperson(n2,american),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_538,c_0_614])]) ).
cnf(c_0_646,hypothesis,
~ hasperson(n3,american),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[c_0_537,c_0_614])]) ).
cnf(c_0_647,hypothesis,
( ~ hasperson(n4,X1)
| ~ hasperson(n5,X2) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_641,c_0_124]),c_0_642])]) ).
cnf(c_0_648,hypothesis,
hasperson(n5,american),
inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(sr,[status(thm)],[inference(spm,[status(thm)],[c_0_643,c_0_143]),c_0_644]),c_0_645]),c_0_646]) ).
cnf(c_0_649,hypothesis,
~ hasperson(n5,X1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[inference(spm,[status(thm)],[c_0_647,c_0_279]),c_0_579])]) ).
cnf(c_0_650,hypothesis,
$false,
inference(sr,[status(thm)],[c_0_648,c_0_649]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.11 % Problem : PUZ017-1 : TPTP v9.2.1. Released v1.0.0.
% 0.00/0.11 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.15/0.32 % Computer : n026.cluster.edu
% 0.15/0.32 % Model : x86_64 x86_64
% 0.15/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.15/0.32 % Memory : 8042.1875MB
% 0.15/0.32 % OS : Linux 3.10.0-693.el7.x86_64
% 0.15/0.32 % CPULimit : 300
% 0.15/0.32 % WCLimit : 300
% 0.15/0.32 % DateTime : Tue May 5 01:34:38 EDT 2026
% 0.15/0.32 % CPUTime :
% 0.15/0.33 % start to proof: theBenchmark
% 11.61/9.13 % Version : CSE_E---1.7
% 11.61/9.13 % Problem : theBenchmark.p
% 11.61/9.13 % SZS status Unsatisfiable for theBenchmark.p
% 11.61/9.13 % SZS output start CNFRefutation
% See solution above
% 11.61/9.17 % Total time : 7.454s
%------------------------------------------------------------------------------