%------------------------------------------------------------------------------
% File : Prover9---2026-6A
% Problem : PUZ017-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Sun Sep 27 08:23:06 AM UTC 2026
% Result : Unsatisfiable 43.68s 6.75s
% Output : CNFRefutation 43.68s
% Verified :
% SZS Type : Refutation
% Derivation depth : 106
% Number of leaves : 105
% Syntax : Number of formulae : 766 ( 184 unt; 0 def)
% Number of atoms : 2414 ( 0 equ)
% Maximal formula atoms : 25 ( 3 avg)
% Number of connectives : 2623 ( 975 ~;1648 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 51 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 14 ( 13 usr; 1 prp; 0-2 aty)
% Number of functors : 30 ( 30 usr; 30 con; 0-0 aty)
% Number of variables : 670 ( 395 sgn 101 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(house_1_not_2,axiom,
~ samehouse(n1,n2),
file('theBenchmark.p',house_1_not_2) ).
cnf(c_1,plain,
~ samehouse(n1,n2),
inference(clausify,[status(thm)],[house_1_not_2]) ).
fof(house_1_not_3,axiom,
~ samehouse(n1,n3),
file('theBenchmark.p',house_1_not_3) ).
cnf(c_3,plain,
~ samehouse(n1,n3),
inference(clausify,[status(thm)],[house_1_not_3]) ).
fof(house_1_not_4,axiom,
~ samehouse(n1,n4),
file('theBenchmark.p',house_1_not_4) ).
cnf(c_4,plain,
~ samehouse(n1,n4),
inference(clausify,[status(thm)],[house_1_not_4]) ).
fof(house_1_not_5,axiom,
~ samehouse(n1,n5),
file('theBenchmark.p',house_1_not_5) ).
cnf(c_5,plain,
~ samehouse(n1,n5),
inference(clausify,[status(thm)],[house_1_not_5]) ).
fof(house_2_not_3,axiom,
~ samehouse(n2,n3),
file('theBenchmark.p',house_2_not_3) ).
cnf(c_6,plain,
~ samehouse(n2,n3),
inference(clausify,[status(thm)],[house_2_not_3]) ).
fof(house_2_not_4,axiom,
~ samehouse(n2,n4),
file('theBenchmark.p',house_2_not_4) ).
cnf(c_7,plain,
~ samehouse(n2,n4),
inference(clausify,[status(thm)],[house_2_not_4]) ).
fof(house_2_not_5,axiom,
~ samehouse(n2,n5),
file('theBenchmark.p',house_2_not_5) ).
cnf(c_8,plain,
~ samehouse(n2,n5),
inference(clausify,[status(thm)],[house_2_not_5]) ).
fof(house_3_not_4,axiom,
~ samehouse(n3,n4),
file('theBenchmark.p',house_3_not_4) ).
cnf(c_9,plain,
~ samehouse(n3,n4),
inference(clausify,[status(thm)],[house_3_not_4]) ).
fof(house_3_not_5,axiom,
~ samehouse(n3,n5),
file('theBenchmark.p',house_3_not_5) ).
cnf(c_10,plain,
~ samehouse(n3,n5),
inference(clausify,[status(thm)],[house_3_not_5]) ).
fof(house_4_not_5,axiom,
~ samehouse(n4,n5),
file('theBenchmark.p',house_4_not_5) ).
cnf(c_11,plain,
~ samehouse(n4,n5),
inference(clausify,[status(thm)],[house_4_not_5]) ).
fof(house_not_nextto_itself,axiom,
! [VAR_0,VAR_1] :
( ~ nextto(VAR_0,VAR_1)
| ~ samehouse(VAR_0,VAR_1) ),
file('theBenchmark.p',house_not_nextto_itself) ).
cnf(c_12,plain,
( ~ nextto(A,B)
| ~ samehouse(A,B) ),
inference(clausify,[status(thm)],[house_not_nextto_itself]) ).
fof(houses_have_unique_colors,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ hascolor(VAR_1,VAR_2)
| ~ hascolor(VAR_0,VAR_2)
| samehouse(VAR_0,VAR_1) ),
file('theBenchmark.p',houses_have_unique_colors) ).
cnf(c_13,plain,
( ~ hascolor(B,C)
| ~ hascolor(A,C)
| samehouse(A,B) ),
inference(clausify,[status(thm)],[houses_have_unique_colors]) ).
fof(nationals_have_unique_houses,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ hasperson(VAR_1,VAR_2)
| ~ hasperson(VAR_0,VAR_2)
| samehouse(VAR_0,VAR_1) ),
file('theBenchmark.p',nationals_have_unique_houses) ).
cnf(c_14,plain,
( ~ hasperson(B,C)
| ~ hasperson(A,C)
| samehouse(A,B) ),
inference(clausify,[status(thm)],[nationals_have_unique_houses]) ).
fof(games_have_unique_houses,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ hasgame(VAR_1,VAR_2)
| ~ hasgame(VAR_0,VAR_2)
| samehouse(VAR_0,VAR_1) ),
file('theBenchmark.p',games_have_unique_houses) ).
cnf(c_16,plain,
( ~ hasgame(B,C)
| ~ hasgame(A,C)
| samehouse(A,B) ),
inference(clausify,[status(thm)],[games_have_unique_houses]) ).
fof(pets_have_unique_houses,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ haspet(VAR_1,VAR_2)
| ~ haspet(VAR_0,VAR_2)
| samehouse(VAR_0,VAR_1) ),
file('theBenchmark.p',pets_have_unique_houses) ).
cnf(c_17,plain,
( ~ haspet(B,C)
| ~ haspet(A,C)
| samehouse(A,B) ),
inference(clausify,[status(thm)],[pets_have_unique_houses]) ).
fof(c2,axiom,
! [VAR_0,VAR_1] :
( hasgame(VAR_1,quoits)
| ~ nextto(VAR_0,VAR_1)
| ~ samehouse(n1,VAR_0)
| ~ haspet(VAR_0,camel) ),
file('theBenchmark.p',c2) ).
cnf(c_19,plain,
( hasgame(B,quoits)
| ~ nextto(A,B)
| ~ samehouse(n1,A)
| ~ haspet(A,camel) ),
inference(clausify,[status(thm)],[c2]) ).
fof(c3,axiom,
! [VAR_0,VAR_1] :
( hasgame(VAR_1,quoits)
| ~ nextto(VAR_0,VAR_1)
| ~ samehouse(VAR_0,n5)
| ~ haspet(VAR_0,camel) ),
file('theBenchmark.p',c3) ).
cnf(c_20,plain,
( hasgame(B,quoits)
| ~ nextto(A,B)
| ~ samehouse(A,n5)
| ~ haspet(A,camel) ),
inference(clausify,[status(thm)],[c3]) ).
fof(c5,axiom,
! [VAR_0,VAR_1,VAR_2] :
( haspet(VAR_1,camel)
| haspet(VAR_0,camel)
| ~ hasgame(VAR_2,quoits)
| ~ nextto(VAR_2,VAR_1)
| ~ nextto(VAR_2,VAR_0)
| samehouse(VAR_0,VAR_1) ),
file('theBenchmark.p',c5) ).
cnf(c_21,plain,
( haspet(B,camel)
| haspet(A,camel)
| ~ hasgame(C,quoits)
| ~ nextto(C,B)
| ~ nextto(C,A)
| samehouse(A,B) ),
inference(clausify,[status(thm)],[c5]) ).
fof(c13,axiom,
! [VAR_0,VAR_1] :
( haspet(VAR_1,rat)
| ~ hasgame(VAR_0,racquetball)
| ~ samehouse(n1,VAR_0)
| ~ nextto(VAR_0,VAR_1) ),
file('theBenchmark.p',c13) ).
cnf(c_28,plain,
( haspet(B,rat)
| ~ hasgame(A,racquetball)
| ~ samehouse(n1,A)
| ~ nextto(A,B) ),
inference(clausify,[status(thm)],[c13]) ).
fof(c20,axiom,
! [VAR_0,VAR_1] :
( hascolor(VAR_1,blue)
| ~ nextto(VAR_0,VAR_1)
| ~ samehouse(n1,VAR_0)
| ~ hasperson(VAR_0,russian) ),
file('theBenchmark.p',c20) ).
cnf(c_31,plain,
( hascolor(B,blue)
| ~ nextto(A,B)
| ~ samehouse(n1,A)
| ~ hasperson(A,russian) ),
inference(clausify,[status(thm)],[c20]) ).
fof(c24,axiom,
! [VAR_0,VAR_1] :
( hasperson(VAR_1,russian)
| ~ samehouse(n1,VAR_0)
| ~ hascolor(VAR_0,blue)
| ~ nextto(VAR_0,VAR_1) ),
file('theBenchmark.p',c24) ).
cnf(c_34,plain,
( hasperson(B,russian)
| ~ samehouse(n1,A)
| ~ hascolor(A,blue)
| ~ nextto(A,B) ),
inference(clausify,[status(thm)],[c24]) ).
fof(russian_not_american,axiom,
~ sameperson(russian,american),
file('theBenchmark.p',russian_not_american) ).
cnf(c_36,plain,
~ sameperson(russian,american),
inference(clausify,[status(thm)],[russian_not_american]) ).
fof(houses_have_unique_nationals,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ hasperson(VAR_2,VAR_1)
| ~ hasperson(VAR_2,VAR_0)
| sameperson(VAR_0,VAR_1) ),
file('theBenchmark.p',houses_have_unique_nationals) ).
cnf(c_37,plain,
( ~ hasperson(C,B)
| ~ hasperson(C,A)
| sameperson(A,B) ),
inference(clausify,[status(thm)],[houses_have_unique_nationals]) ).
fof(swede_not_american,axiom,
~ sameperson(swede,american),
file('theBenchmark.p',swede_not_american) ).
cnf(c_38,plain,
~ sameperson(swede,american),
inference(clausify,[status(thm)],[swede_not_american]) ).
fof(swede_not_russian,axiom,
~ sameperson(swede,russian),
file('theBenchmark.p',swede_not_russian) ).
cnf(c_39,plain,
~ sameperson(swede,russian),
inference(clausify,[status(thm)],[swede_not_russian]) ).
fof(italian_not_american,axiom,
~ sameperson(italian,american),
file('theBenchmark.p',italian_not_american) ).
cnf(c_40,plain,
~ sameperson(italian,american),
inference(clausify,[status(thm)],[italian_not_american]) ).
fof(italian_not_russian,axiom,
~ sameperson(italian,russian),
file('theBenchmark.p',italian_not_russian) ).
cnf(c_41,plain,
~ sameperson(italian,russian),
inference(clausify,[status(thm)],[italian_not_russian]) ).
fof(italian_not_swede,axiom,
~ sameperson(italian,swede),
file('theBenchmark.p',italian_not_swede) ).
cnf(c_42,plain,
~ sameperson(italian,swede),
inference(clausify,[status(thm)],[italian_not_swede]) ).
fof(englishman_not_american,axiom,
~ sameperson(englishman,american),
file('theBenchmark.p',englishman_not_american) ).
cnf(c_43,plain,
~ sameperson(englishman,american),
inference(clausify,[status(thm)],[englishman_not_american]) ).
fof(englishman_not_russian,axiom,
~ sameperson(englishman,russian),
file('theBenchmark.p',englishman_not_russian) ).
cnf(c_44,plain,
~ sameperson(englishman,russian),
inference(clausify,[status(thm)],[englishman_not_russian]) ).
fof(englishman_not_swede,axiom,
~ sameperson(englishman,swede),
file('theBenchmark.p',englishman_not_swede) ).
cnf(c_45,plain,
~ sameperson(englishman,swede),
inference(clausify,[status(thm)],[englishman_not_swede]) ).
fof(englishman_not_italian,axiom,
~ sameperson(englishman,italian),
file('theBenchmark.p',englishman_not_italian) ).
cnf(c_46,plain,
~ sameperson(englishman,italian),
inference(clausify,[status(thm)],[englishman_not_italian]) ).
fof(red_not_white,axiom,
~ samecolor(red,white),
file('theBenchmark.p',red_not_white) ).
cnf(c_48,plain,
~ samecolor(red,white),
inference(clausify,[status(thm)],[red_not_white]) ).
fof(red_not_green,axiom,
~ samecolor(red,green),
file('theBenchmark.p',red_not_green) ).
cnf(c_50,plain,
~ samecolor(red,green),
inference(clausify,[status(thm)],[red_not_green]) ).
fof(red_not_yellow,axiom,
~ samecolor(red,yellow),
file('theBenchmark.p',red_not_yellow) ).
cnf(c_51,plain,
~ samecolor(red,yellow),
inference(clausify,[status(thm)],[red_not_yellow]) ).
fof(red_not_blue,axiom,
~ samecolor(red,blue),
file('theBenchmark.p',red_not_blue) ).
cnf(c_52,plain,
~ samecolor(red,blue),
inference(clausify,[status(thm)],[red_not_blue]) ).
fof(white_not_blue,axiom,
~ samecolor(white,blue),
file('theBenchmark.p',white_not_blue) ).
cnf(c_55,plain,
~ samecolor(white,blue),
inference(clausify,[status(thm)],[white_not_blue]) ).
fof(green_not_yellow,axiom,
~ samecolor(green,yellow),
file('theBenchmark.p',green_not_yellow) ).
cnf(c_56,plain,
~ samecolor(green,yellow),
inference(clausify,[status(thm)],[green_not_yellow]) ).
fof(green_not_blue,axiom,
~ samecolor(green,blue),
file('theBenchmark.p',green_not_blue) ).
cnf(c_57,plain,
~ samecolor(green,blue),
inference(clausify,[status(thm)],[green_not_blue]) ).
fof(colours_are_unique,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ hascolor(VAR_2,VAR_1)
| ~ hascolor(VAR_2,VAR_0)
| samecolor(VAR_0,VAR_1) ),
file('theBenchmark.p',colours_are_unique) ).
cnf(c_59,plain,
( ~ hascolor(C,B)
| ~ hascolor(C,A)
| samecolor(A,B) ),
inference(clausify,[status(thm)],[colours_are_unique]) ).
fof(vodka_not_unknown,axiom,
~ samedrink(vodka,unknown_drink),
file('theBenchmark.p',vodka_not_unknown) ).
cnf(c_60,plain,
~ samedrink(vodka,unknown_drink),
inference(clausify,[status(thm)],[vodka_not_unknown]) ).
fof(houses_have_unique_drinks,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ hasdrink(VAR_2,VAR_1)
| ~ hasdrink(VAR_2,VAR_0)
| samedrink(VAR_0,VAR_1) ),
file('theBenchmark.p',houses_have_unique_drinks) ).
cnf(c_61,plain,
( ~ hasdrink(C,B)
| ~ hasdrink(C,A)
| samedrink(A,B) ),
inference(clausify,[status(thm)],[houses_have_unique_drinks]) ).
fof(milk_not_unknown,axiom,
~ samedrink(milk,unknown_drink),
file('theBenchmark.p',milk_not_unknown) ).
cnf(c_62,plain,
~ samedrink(milk,unknown_drink),
inference(clausify,[status(thm)],[milk_not_unknown]) ).
fof(milk_not_vodka,axiom,
~ samedrink(milk,vodka),
file('theBenchmark.p',milk_not_vodka) ).
cnf(c_63,plain,
~ samedrink(milk,vodka),
inference(clausify,[status(thm)],[milk_not_vodka]) ).
fof(coffee_not_known,axiom,
~ samedrink(coffee,unknown_drink),
file('theBenchmark.p',coffee_not_known) ).
cnf(c_64,plain,
~ samedrink(coffee,unknown_drink),
inference(clausify,[status(thm)],[coffee_not_known]) ).
fof(coffee_not_vodka,axiom,
~ samedrink(coffee,vodka),
file('theBenchmark.p',coffee_not_vodka) ).
cnf(c_65,plain,
~ samedrink(coffee,vodka),
inference(clausify,[status(thm)],[coffee_not_vodka]) ).
fof(coffee_not_milk,axiom,
~ samedrink(coffee,milk),
file('theBenchmark.p',coffee_not_milk) ).
cnf(c_66,plain,
~ samedrink(coffee,milk),
inference(clausify,[status(thm)],[coffee_not_milk]) ).
fof(lemonade_not_unknown,axiom,
~ samedrink(lemonade,unknown_drink),
file('theBenchmark.p',lemonade_not_unknown) ).
cnf(c_67,plain,
~ samedrink(lemonade,unknown_drink),
inference(clausify,[status(thm)],[lemonade_not_unknown]) ).
fof(lemonade_not_vodka,axiom,
~ samedrink(lemonade,vodka),
file('theBenchmark.p',lemonade_not_vodka) ).
cnf(c_68,plain,
~ samedrink(lemonade,vodka),
inference(clausify,[status(thm)],[lemonade_not_vodka]) ).
fof(lemonade_not_milk,axiom,
~ samedrink(lemonade,milk),
file('theBenchmark.p',lemonade_not_milk) ).
cnf(c_69,plain,
~ samedrink(lemonade,milk),
inference(clausify,[status(thm)],[lemonade_not_milk]) ).
fof(lemonade_not_coffee,axiom,
~ samedrink(lemonade,coffee),
file('theBenchmark.p',lemonade_not_coffee) ).
cnf(c_70,plain,
~ samedrink(lemonade,coffee),
inference(clausify,[status(thm)],[lemonade_not_coffee]) ).
fof(backgammon_not_recquetball,axiom,
~ samegame(backgammon,racquetball),
file('theBenchmark.p',backgammon_not_recquetball) ).
cnf(c_72,plain,
~ samegame(backgammon,racquetball),
inference(clausify,[status(thm)],[backgammon_not_recquetball]) ).
fof(backgammon_not_solitaire,axiom,
~ samegame(backgammon,solitaire),
file('theBenchmark.p',backgammon_not_solitaire) ).
cnf(c_75,plain,
~ samegame(backgammon,solitaire),
inference(clausify,[status(thm)],[backgammon_not_solitaire]) ).
fof(backgammon_not_charades,axiom,
~ samegame(backgammon,charades),
file('theBenchmark.p',backgammon_not_charades) ).
cnf(c_76,plain,
~ samegame(backgammon,charades),
inference(clausify,[status(thm)],[backgammon_not_charades]) ).
fof(racquetball_not_solitaire,axiom,
~ samegame(racquetball,solitaire),
file('theBenchmark.p',racquetball_not_solitaire) ).
cnf(c_78,plain,
~ samegame(racquetball,solitaire),
inference(clausify,[status(thm)],[racquetball_not_solitaire]) ).
fof(quoits_not_solitaire,axiom,
~ samegame(quoits,solitaire),
file('theBenchmark.p',quoits_not_solitaire) ).
cnf(c_80,plain,
~ samegame(quoits,solitaire),
inference(clausify,[status(thm)],[quoits_not_solitaire]) ).
fof(solitaire_not_charades,axiom,
~ samegame(solitaire,charades),
file('theBenchmark.p',solitaire_not_charades) ).
cnf(c_82,plain,
~ samegame(solitaire,charades),
inference(clausify,[status(thm)],[solitaire_not_charades]) ).
fof(houses_have_unique_games,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ hasgame(VAR_2,VAR_1)
| ~ hasgame(VAR_2,VAR_0)
| samegame(VAR_0,VAR_1) ),
file('theBenchmark.p',houses_have_unique_games) ).
cnf(c_83,plain,
( ~ hasgame(C,B)
| ~ hasgame(C,A)
| samegame(A,B) ),
inference(clausify,[status(thm)],[houses_have_unique_games]) ).
fof(rat_is_pet,axiom,
~ samepet(rat,no_pet),
file('theBenchmark.p',rat_is_pet) ).
cnf(c_84,plain,
~ samepet(rat,no_pet),
inference(clausify,[status(thm)],[rat_is_pet]) ).
fof(houses_have_unique_pets,axiom,
! [VAR_0,VAR_1,VAR_2] :
( ~ haspet(VAR_2,VAR_1)
| ~ haspet(VAR_2,VAR_0)
| samepet(VAR_0,VAR_1) ),
file('theBenchmark.p',houses_have_unique_pets) ).
cnf(c_85,plain,
( ~ haspet(C,B)
| ~ haspet(C,A)
| samepet(A,B) ),
inference(clausify,[status(thm)],[houses_have_unique_pets]) ).
fof(camel_is_pet,axiom,
~ samepet(camel,no_pet),
file('theBenchmark.p',camel_is_pet) ).
cnf(c_86,plain,
~ samepet(camel,no_pet),
inference(clausify,[status(thm)],[camel_is_pet]) ).
fof(camel_not_rat,axiom,
~ samepet(camel,rat),
file('theBenchmark.p',camel_not_rat) ).
cnf(c_87,plain,
~ samepet(camel,rat),
inference(clausify,[status(thm)],[camel_not_rat]) ).
fof(toad_is_pet,axiom,
~ samepet(toad,no_pet),
file('theBenchmark.p',toad_is_pet) ).
cnf(c_88,plain,
~ samepet(toad,no_pet),
inference(clausify,[status(thm)],[toad_is_pet]) ).
fof(toad_not_rat,axiom,
~ samepet(toad,rat),
file('theBenchmark.p',toad_not_rat) ).
cnf(c_89,plain,
~ samepet(toad,rat),
inference(clausify,[status(thm)],[toad_not_rat]) ).
fof(toad_not_camel,axiom,
~ samepet(toad,camel),
file('theBenchmark.p',toad_not_camel) ).
cnf(c_90,plain,
~ samepet(toad,camel),
inference(clausify,[status(thm)],[toad_not_camel]) ).
fof(guppy_is_pet,axiom,
~ samepet(guppy,no_pet),
file('theBenchmark.p',guppy_is_pet) ).
cnf(c_91,plain,
~ samepet(guppy,no_pet),
inference(clausify,[status(thm)],[guppy_is_pet]) ).
fof(guppy_not_rat,axiom,
~ samepet(guppy,rat),
file('theBenchmark.p',guppy_not_rat) ).
cnf(c_92,plain,
~ samepet(guppy,rat),
inference(clausify,[status(thm)],[guppy_not_rat]) ).
fof(guppy_not_camel,axiom,
~ samepet(guppy,camel),
file('theBenchmark.p',guppy_not_camel) ).
cnf(c_93,plain,
~ samepet(guppy,camel),
inference(clausify,[status(thm)],[guppy_not_camel]) ).
fof(guppy_not_toad,axiom,
~ samepet(guppy,toad),
file('theBenchmark.p',guppy_not_toad) ).
cnf(c_94,plain,
~ samepet(guppy,toad),
inference(clausify,[status(thm)],[guppy_not_toad]) ).
cnf(c_96,plain,
( ~ haspet(A,toad)
| ~ haspet(A,guppy) ),
inference(resolve,[status(thm)],[c_94,c_85]) ).
cnf(c_97,plain,
( ~ haspet(A,camel)
| ~ haspet(A,guppy) ),
inference(resolve,[status(thm)],[c_93,c_85]) ).
cnf(c_98,plain,
( ~ haspet(A,rat)
| ~ haspet(A,guppy) ),
inference(resolve,[status(thm)],[c_92,c_85]) ).
cnf(c_99,plain,
( ~ haspet(A,no_pet)
| ~ haspet(A,guppy) ),
inference(resolve,[status(thm)],[c_91,c_85]) ).
cnf(c_100,plain,
( ~ haspet(A,camel)
| ~ haspet(A,toad) ),
inference(resolve,[status(thm)],[c_90,c_85]) ).
cnf(c_101,plain,
( ~ haspet(A,rat)
| ~ haspet(A,toad) ),
inference(resolve,[status(thm)],[c_89,c_85]) ).
cnf(c_102,plain,
( ~ haspet(A,no_pet)
| ~ haspet(A,toad) ),
inference(resolve,[status(thm)],[c_88,c_85]) ).
cnf(c_103,plain,
( ~ haspet(A,rat)
| ~ haspet(A,camel) ),
inference(resolve,[status(thm)],[c_87,c_85]) ).
cnf(c_104,plain,
( ~ haspet(A,no_pet)
| ~ haspet(A,camel) ),
inference(resolve,[status(thm)],[c_86,c_85]) ).
cnf(c_105,plain,
( ~ haspet(A,no_pet)
| ~ haspet(A,rat) ),
inference(resolve,[status(thm)],[c_84,c_85]) ).
cnf(c_106,plain,
( ~ hasdrink(A,coffee)
| ~ hasdrink(A,lemonade) ),
inference(resolve,[status(thm)],[c_70,c_61]) ).
cnf(c_107,plain,
( ~ hasdrink(A,milk)
| ~ hasdrink(A,lemonade) ),
inference(resolve,[status(thm)],[c_69,c_61]) ).
cnf(c_108,plain,
( ~ hasdrink(A,vodka)
| ~ hasdrink(A,lemonade) ),
inference(resolve,[status(thm)],[c_68,c_61]) ).
cnf(c_109,plain,
( ~ hasdrink(A,unknown_drink)
| ~ hasdrink(A,lemonade) ),
inference(resolve,[status(thm)],[c_67,c_61]) ).
cnf(c_110,plain,
( ~ hasdrink(A,milk)
| ~ hasdrink(A,coffee) ),
inference(resolve,[status(thm)],[c_66,c_61]) ).
cnf(c_111,plain,
( ~ hasdrink(A,vodka)
| ~ hasdrink(A,coffee) ),
inference(resolve,[status(thm)],[c_65,c_61]) ).
cnf(c_112,plain,
( ~ hasdrink(A,unknown_drink)
| ~ hasdrink(A,coffee) ),
inference(resolve,[status(thm)],[c_64,c_61]) ).
cnf(c_113,plain,
( ~ hasdrink(A,vodka)
| ~ hasdrink(A,milk) ),
inference(resolve,[status(thm)],[c_63,c_61]) ).
cnf(c_114,plain,
( ~ hasdrink(A,unknown_drink)
| ~ hasdrink(A,milk) ),
inference(resolve,[status(thm)],[c_62,c_61]) ).
cnf(c_115,plain,
( ~ hasdrink(A,unknown_drink)
| ~ hasdrink(A,vodka) ),
inference(resolve,[status(thm)],[c_60,c_61]) ).
cnf(c_116,plain,
( ~ hasperson(A,italian)
| ~ hasperson(A,englishman) ),
inference(resolve,[status(thm)],[c_46,c_37]) ).
cnf(c_117,plain,
( ~ hasperson(A,swede)
| ~ hasperson(A,englishman) ),
inference(resolve,[status(thm)],[c_45,c_37]) ).
cnf(c_118,plain,
( ~ hasperson(A,russian)
| ~ hasperson(A,englishman) ),
inference(resolve,[status(thm)],[c_44,c_37]) ).
cnf(c_119,plain,
( ~ hasperson(A,american)
| ~ hasperson(A,englishman) ),
inference(resolve,[status(thm)],[c_43,c_37]) ).
cnf(c_120,plain,
( ~ hasperson(A,swede)
| ~ hasperson(A,italian) ),
inference(resolve,[status(thm)],[c_42,c_37]) ).
cnf(c_121,plain,
( ~ hasperson(A,russian)
| ~ hasperson(A,italian) ),
inference(resolve,[status(thm)],[c_41,c_37]) ).
cnf(c_122,plain,
( ~ hasperson(A,american)
| ~ hasperson(A,italian) ),
inference(resolve,[status(thm)],[c_40,c_37]) ).
cnf(c_123,plain,
( ~ hasperson(A,russian)
| ~ hasperson(A,swede) ),
inference(resolve,[status(thm)],[c_39,c_37]) ).
cnf(c_124,plain,
( ~ hasperson(A,american)
| ~ hasperson(A,swede) ),
inference(resolve,[status(thm)],[c_38,c_37]) ).
cnf(c_125,plain,
( ~ hasperson(A,american)
| ~ hasperson(A,russian) ),
inference(resolve,[status(thm)],[c_36,c_37]) ).
fof(symmetry_of_nextto,axiom,
! [VAR_0,VAR_1] :
( nextto(VAR_1,VAR_0)
| ~ nextto(VAR_0,VAR_1) ),
file('theBenchmark.p',symmetry_of_nextto) ).
cnf(c_126,plain,
( nextto(B,A)
| ~ nextto(A,B) ),
inference(clausify,[status(thm)],[symmetry_of_nextto]) ).
fof(left_means_nextto,axiom,
! [VAR_0,VAR_1] :
( nextto(VAR_0,VAR_1)
| ~ left(VAR_0,VAR_1) ),
file('theBenchmark.p',left_means_nextto) ).
cnf(c_129,plain,
( nextto(A,B)
| ~ left(A,B) ),
inference(clausify,[status(thm)],[left_means_nextto]) ).
fof(every_house_has_a_national,axiom,
! [VAR_0] :
( hasperson(VAR_0,american)
| hasperson(VAR_0,russian)
| hasperson(VAR_0,swede)
| hasperson(VAR_0,italian)
| hasperson(VAR_0,englishman) ),
file('theBenchmark.p',every_house_has_a_national) ).
cnf(c_132,plain,
( hasperson(A,american)
| hasperson(A,russian)
| hasperson(A,swede)
| hasperson(A,italian)
| hasperson(A,englishman) ),
inference(clausify,[status(thm)],[every_house_has_a_national]) ).
fof(every_natioality_is_used,axiom,
! [VAR_0] :
( hasperson(n5,VAR_0)
| hasperson(n4,VAR_0)
| hasperson(n3,VAR_0)
| hasperson(n2,VAR_0)
| hasperson(n1,VAR_0) ),
file('theBenchmark.p',every_natioality_is_used) ).
cnf(c_133,plain,
( hasperson(n5,A)
| hasperson(n4,A)
| hasperson(n3,A)
| hasperson(n2,A)
| hasperson(n1,A) ),
inference(clausify,[status(thm)],[every_natioality_is_used]) ).
fof(every_house_has_color,axiom,
! [VAR_0] :
( hascolor(VAR_0,blue)
| hascolor(VAR_0,yellow)
| hascolor(VAR_0,green)
| hascolor(VAR_0,white)
| hascolor(VAR_0,red) ),
file('theBenchmark.p',every_house_has_color) ).
cnf(c_134,plain,
( hascolor(A,blue)
| hascolor(A,yellow)
| hascolor(A,green)
| hascolor(A,white)
| hascolor(A,red) ),
inference(clausify,[status(thm)],[every_house_has_color]) ).
fof(every_color_is_used,axiom,
! [VAR_0] :
( hascolor(n5,VAR_0)
| hascolor(n4,VAR_0)
| hascolor(n3,VAR_0)
| hascolor(n2,VAR_0)
| hascolor(n1,VAR_0) ),
file('theBenchmark.p',every_color_is_used) ).
cnf(c_135,plain,
( hascolor(n5,A)
| hascolor(n4,A)
| hascolor(n3,A)
| hascolor(n2,A)
| hascolor(n1,A) ),
inference(clausify,[status(thm)],[every_color_is_used]) ).
fof(every_drink_is_used,axiom,
! [VAR_0] :
( hasdrink(n5,VAR_0)
| hasdrink(n4,VAR_0)
| hasdrink(n3,VAR_0)
| hasdrink(n2,VAR_0)
| hasdrink(n1,VAR_0) ),
file('theBenchmark.p',every_drink_is_used) ).
cnf(c_137,plain,
( hasdrink(n5,A)
| hasdrink(n4,A)
| hasdrink(n3,A)
| hasdrink(n2,A)
| hasdrink(n1,A) ),
inference(clausify,[status(thm)],[every_drink_is_used]) ).
fof(every_house_has_a_game,axiom,
! [VAR_0] :
( hasgame(VAR_0,charades)
| hasgame(VAR_0,solitaire)
| hasgame(VAR_0,quoits)
| hasgame(VAR_0,racquetball)
| hasgame(VAR_0,backgammon) ),
file('theBenchmark.p',every_house_has_a_game) ).
cnf(c_138,plain,
( hasgame(A,charades)
| hasgame(A,solitaire)
| hasgame(A,quoits)
| hasgame(A,racquetball)
| hasgame(A,backgammon) ),
inference(clausify,[status(thm)],[every_house_has_a_game]) ).
fof(every_pet_is_used,axiom,
! [VAR_0] :
( haspet(n5,VAR_0)
| haspet(n4,VAR_0)
| haspet(n3,VAR_0)
| haspet(n2,VAR_0)
| haspet(n1,VAR_0) ),
file('theBenchmark.p',every_pet_is_used) ).
cnf(c_141,plain,
( haspet(n5,A)
| haspet(n4,A)
| haspet(n3,A)
| haspet(n2,A)
| haspet(n1,A) ),
inference(clausify,[status(thm)],[every_pet_is_used]) ).
fof(englishman_lives_in_red_house1,axiom,
! [VAR_0] :
( hascolor(VAR_0,red)
| ~ hasperson(VAR_0,englishman) ),
file('theBenchmark.p',englishman_lives_in_red_house1) ).
cnf(c_142,plain,
( hascolor(A,red)
| ~ hasperson(A,englishman) ),
inference(clausify,[status(thm)],[englishman_lives_in_red_house1]) ).
fof(englishman_lives_in_red_house2,axiom,
! [VAR_0] :
( ~ hascolor(VAR_0,red)
| hasperson(VAR_0,englishman) ),
file('theBenchmark.p',englishman_lives_in_red_house2) ).
cnf(c_143,plain,
( ~ hascolor(A,red)
| hasperson(A,englishman) ),
inference(clausify,[status(thm)],[englishman_lives_in_red_house2]) ).
fof(white_house_left_of_green1,axiom,
! [VAR_0,VAR_1] :
( left(VAR_0,VAR_1)
| ~ hascolor(VAR_1,green)
| ~ hascolor(VAR_0,white) ),
file('theBenchmark.p',white_house_left_of_green1) ).
cnf(c_144,plain,
( left(A,B)
| ~ hascolor(B,green)
| ~ hascolor(A,white) ),
inference(clausify,[status(thm)],[white_house_left_of_green1]) ).
fof(white_house_left_of_green2,axiom,
! [VAR_0,VAR_1] :
( ~ left(VAR_0,VAR_1)
| hascolor(VAR_1,green)
| ~ hascolor(VAR_0,white) ),
file('theBenchmark.p',white_house_left_of_green2) ).
cnf(c_145,plain,
( ~ left(A,B)
| hascolor(B,green)
| ~ hascolor(A,white) ),
inference(clausify,[status(thm)],[white_house_left_of_green2]) ).
fof(white_house_left_of_green3,axiom,
! [VAR_0,VAR_1] :
( ~ left(VAR_0,VAR_1)
| ~ hascolor(VAR_1,green)
| hascolor(VAR_0,white) ),
file('theBenchmark.p',white_house_left_of_green3) ).
cnf(c_146,plain,
( ~ left(A,B)
| ~ hascolor(B,green)
| hascolor(A,white) ),
inference(clausify,[status(thm)],[white_house_left_of_green3]) ).
fof(italian_has_guppy1,axiom,
! [VAR_0] :
( haspet(VAR_0,guppy)
| ~ hasperson(VAR_0,italian) ),
file('theBenchmark.p',italian_has_guppy1) ).
cnf(c_147,plain,
( haspet(A,guppy)
| ~ hasperson(A,italian) ),
inference(clausify,[status(thm)],[italian_has_guppy1]) ).
fof(italian_has_guppy2,axiom,
! [VAR_0] :
( ~ haspet(VAR_0,guppy)
| hasperson(VAR_0,italian) ),
file('theBenchmark.p',italian_has_guppy2) ).
cnf(c_148,plain,
( ~ haspet(A,guppy)
| hasperson(A,italian) ),
inference(clausify,[status(thm)],[italian_has_guppy2]) ).
fof(lemonade_in_green_house1,axiom,
! [VAR_0] :
( hascolor(VAR_0,green)
| ~ hasdrink(VAR_0,lemonade) ),
file('theBenchmark.p',lemonade_in_green_house1) ).
cnf(c_149,plain,
( hascolor(A,green)
| ~ hasdrink(A,lemonade) ),
inference(clausify,[status(thm)],[lemonade_in_green_house1]) ).
fof(lemonade_in_green_house2,axiom,
! [VAR_0] :
( ~ hascolor(VAR_0,green)
| hasdrink(VAR_0,lemonade) ),
file('theBenchmark.p',lemonade_in_green_house2) ).
cnf(c_150,plain,
( ~ hascolor(A,green)
| hasdrink(A,lemonade) ),
inference(clausify,[status(thm)],[lemonade_in_green_house2]) ).
fof(swede_drinks_coffee1,axiom,
! [VAR_0] :
( hasdrink(VAR_0,coffee)
| ~ hasperson(VAR_0,swede) ),
file('theBenchmark.p',swede_drinks_coffee1) ).
cnf(c_151,plain,
( hasdrink(A,coffee)
| ~ hasperson(A,swede) ),
inference(clausify,[status(thm)],[swede_drinks_coffee1]) ).
fof(swede_drinks_coffee2,axiom,
! [VAR_0] :
( ~ hasdrink(VAR_0,coffee)
| hasperson(VAR_0,swede) ),
file('theBenchmark.p',swede_drinks_coffee2) ).
cnf(c_152,plain,
( ~ hasdrink(A,coffee)
| hasperson(A,swede) ),
inference(clausify,[status(thm)],[swede_drinks_coffee2]) ).
fof(toad_lives_with_backgammon1,axiom,
! [VAR_0] :
( hasgame(VAR_0,backgammon)
| ~ haspet(VAR_0,toad) ),
file('theBenchmark.p',toad_lives_with_backgammon1) ).
cnf(c_153,plain,
( hasgame(A,backgammon)
| ~ haspet(A,toad) ),
inference(clausify,[status(thm)],[toad_lives_with_backgammon1]) ).
fof(toad_lives_with_backgammon2,axiom,
! [VAR_0] :
( ~ hasgame(VAR_0,backgammon)
| haspet(VAR_0,toad) ),
file('theBenchmark.p',toad_lives_with_backgammon2) ).
cnf(c_154,plain,
( ~ hasgame(A,backgammon)
| haspet(A,toad) ),
inference(clausify,[status(thm)],[toad_lives_with_backgammon2]) ).
fof(racquetball_played_in_yellow_house1,axiom,
! [VAR_0] :
( hascolor(VAR_0,yellow)
| ~ hasgame(VAR_0,racquetball) ),
file('theBenchmark.p',racquetball_played_in_yellow_house1) ).
cnf(c_155,plain,
( hascolor(A,yellow)
| ~ hasgame(A,racquetball) ),
inference(clausify,[status(thm)],[racquetball_played_in_yellow_house1]) ).
fof(racquetball_played_in_yellow_house2,axiom,
! [VAR_0] :
( ~ hascolor(VAR_0,yellow)
| hasgame(VAR_0,racquetball) ),
file('theBenchmark.p',racquetball_played_in_yellow_house2) ).
cnf(c_156,plain,
( ~ hascolor(A,yellow)
| hasgame(A,racquetball) ),
inference(clausify,[status(thm)],[racquetball_played_in_yellow_house2]) ).
fof(c15,axiom,
! [VAR_0] :
( hasdrink(VAR_0,vodka)
| ~ hasgame(VAR_0,solitaire) ),
file('theBenchmark.p',c15) ).
cnf(c_159,plain,
( hasdrink(A,vodka)
| ~ hasgame(A,solitaire) ),
inference(clausify,[status(thm)],[c15]) ).
fof(c16,axiom,
! [VAR_0] :
( ~ hasdrink(VAR_0,vodka)
| hasgame(VAR_0,solitaire) ),
file('theBenchmark.p',c16) ).
cnf(c_160,plain,
( ~ hasdrink(A,vodka)
| hasgame(A,solitaire) ),
inference(clausify,[status(thm)],[c16]) ).
fof(c17,axiom,
! [VAR_0] :
( hasgame(VAR_0,charades)
| ~ hasperson(VAR_0,american) ),
file('theBenchmark.p',c17) ).
cnf(c_161,plain,
( hasgame(A,charades)
| ~ hasperson(A,american) ),
inference(clausify,[status(thm)],[c17]) ).
fof(c18,axiom,
! [VAR_0] :
( ~ hasgame(VAR_0,charades)
| hasperson(VAR_0,american) ),
file('theBenchmark.p',c18) ).
cnf(c_162,plain,
( ~ hasgame(A,charades)
| hasperson(A,american) ),
inference(clausify,[status(thm)],[c18]) ).
fof(house1_at_left,axiom,
! [VAR_0] : ~ left(VAR_0,n1),
file('theBenchmark.p',house1_at_left) ).
cnf(c_164,plain,
~ left(A,n1),
inference(clausify,[status(thm)],[house1_at_left]) ).
fof(house_1_left_of_2,axiom,
left(n1,n2),
file('theBenchmark.p',house_1_left_of_2) ).
cnf(c_166,plain,
left(n1,n2),
inference(clausify,[status(thm)],[house_1_left_of_2]) ).
fof(house_2_left_of_3,axiom,
left(n2,n3),
file('theBenchmark.p',house_2_left_of_3) ).
cnf(c_167,plain,
left(n2,n3),
inference(clausify,[status(thm)],[house_2_left_of_3]) ).
fof(house_3_left_of_4,axiom,
left(n3,n4),
file('theBenchmark.p',house_3_left_of_4) ).
cnf(c_168,plain,
left(n3,n4),
inference(clausify,[status(thm)],[house_3_left_of_4]) ).
fof(house_4_left_of_5,axiom,
left(n4,n5),
file('theBenchmark.p',house_4_left_of_5) ).
cnf(c_169,plain,
left(n4,n5),
inference(clausify,[status(thm)],[house_4_left_of_5]) ).
fof(house_3_has_milk,axiom,
hasdrink(n3,milk),
file('theBenchmark.p',house_3_has_milk) ).
cnf(c_176,plain,
hasdrink(n3,milk),
inference(clausify,[status(thm)],[house_3_has_milk]) ).
fof(house_1_has_russian,axiom,
hasperson(n1,russian),
file('theBenchmark.p',house_1_has_russian) ).
cnf(c_177,plain,
hasperson(n1,russian),
inference(clausify,[status(thm)],[house_1_has_russian]) ).
fof(find_out_house_details,axiom,
! [VAR_0,VAR_1,VAR_2,VAR_3,VAR_4,VAR_5,VAR_6,VAR_7,VAR_8,VAR_9,VAR_10,VAR_11,VAR_12,VAR_13,VAR_14,VAR_15,VAR_16,VAR_17,VAR_18,VAR_19,VAR_20,VAR_21,VAR_22,VAR_23,VAR_24] :
( ~ haspet(n5,VAR_24)
| ~ haspet(n4,VAR_23)
| ~ haspet(n3,VAR_22)
| ~ haspet(n2,VAR_21)
| ~ haspet(n1,VAR_20)
| ~ hasgame(n5,VAR_19)
| ~ hasgame(n4,VAR_18)
| ~ hasgame(n3,VAR_17)
| ~ hasgame(n2,VAR_16)
| ~ hasgame(n1,VAR_15)
| ~ hasdrink(n5,VAR_14)
| ~ hasdrink(n4,VAR_13)
| ~ hasdrink(n3,VAR_12)
| ~ hasdrink(n2,VAR_11)
| ~ hasdrink(n1,VAR_10)
| ~ hascolor(n5,VAR_9)
| ~ hascolor(n4,VAR_8)
| ~ hascolor(n3,VAR_7)
| ~ hascolor(n2,VAR_6)
| ~ hascolor(n1,VAR_5)
| ~ hasperson(n5,VAR_4)
| ~ hasperson(n4,VAR_3)
| ~ hasperson(n3,VAR_2)
| ~ hasperson(n2,VAR_1)
| ~ hasperson(n1,VAR_0) ),
file('theBenchmark.p',find_out_house_details) ).
cnf(c_178,plain,
( ~ haspet(n5,V24)
| ~ haspet(n4,V23)
| ~ haspet(n3,V22)
| ~ haspet(n2,V21)
| ~ haspet(n1,V20)
| ~ hasgame(n5,V19)
| ~ hasgame(n4,V18)
| ~ hasgame(n3,V17)
| ~ hasgame(n2,V16)
| ~ hasgame(n1,V15)
| ~ hasdrink(n5,V14)
| ~ hasdrink(n4,V13)
| ~ hasdrink(n3,V12)
| ~ hasdrink(n2,V11)
| ~ hasdrink(n1,V10)
| ~ hascolor(n5,V9)
| ~ hascolor(n4,V8)
| ~ hascolor(n3,V7)
| ~ hascolor(n2,V6)
| ~ hascolor(n1,F)
| ~ hasperson(n5,E)
| ~ hasperson(n4,D)
| ~ hasperson(n3,C)
| ~ hasperson(n2,B)
| ~ hasperson(n1,A) ),
inference(clausify,[status(thm)],[find_out_house_details]) ).
cnf(c_182,plain,
( ~ hascolor(n4,A)
| ~ hascolor(n3,A) ),
inference(resolve,[status(thm)],[c_13,c_9]) ).
cnf(c_185,plain,
( ~ hascolor(n3,A)
| ~ hascolor(n2,A) ),
inference(resolve,[status(thm)],[c_13,c_6]) ).
cnf(c_186,plain,
( ~ hascolor(n5,A)
| ~ hascolor(n1,A) ),
inference(resolve,[status(thm)],[c_13,c_5]) ).
cnf(c_187,plain,
( ~ hascolor(n4,A)
| ~ hascolor(n1,A) ),
inference(resolve,[status(thm)],[c_13,c_4]) ).
cnf(c_188,plain,
( ~ hascolor(n3,A)
| ~ hascolor(n1,A) ),
inference(resolve,[status(thm)],[c_13,c_3]) ).
cnf(c_190,plain,
( ~ nextto(A,C)
| ~ hasperson(C,B)
| ~ hasperson(A,B) ),
inference(resolve,[status(thm)],[c_14,c_12]) ).
cnf(c_198,plain,
( ~ hasperson(n4,A)
| ~ hasperson(n1,A) ),
inference(resolve,[status(thm)],[c_14,c_4]) ).
cnf(c_199,plain,
( ~ hasperson(n3,A)
| ~ hasperson(n1,A) ),
inference(resolve,[status(thm)],[c_14,c_3]) ).
cnf(c_200,plain,
( ~ hasperson(n2,A)
| ~ hasperson(n1,A) ),
inference(resolve,[status(thm)],[c_14,c_1]) ).
cnf(c_212,plain,
( ~ nextto(A,C)
| ~ hasgame(C,B)
| ~ hasgame(A,B) ),
inference(resolve,[status(thm)],[c_16,c_12]) ).
cnf(c_213,plain,
( ~ hasgame(n5,A)
| ~ hasgame(n4,A) ),
inference(resolve,[status(thm)],[c_16,c_11]) ).
cnf(c_214,plain,
( ~ hasgame(n5,A)
| ~ hasgame(n3,A) ),
inference(resolve,[status(thm)],[c_16,c_10]) ).
cnf(c_215,plain,
( ~ hasgame(n4,A)
| ~ hasgame(n3,A) ),
inference(resolve,[status(thm)],[c_16,c_9]) ).
cnf(c_216,plain,
( ~ hasgame(n5,A)
| ~ hasgame(n2,A) ),
inference(resolve,[status(thm)],[c_16,c_8]) ).
cnf(c_217,plain,
( ~ hasgame(n4,A)
| ~ hasgame(n2,A) ),
inference(resolve,[status(thm)],[c_16,c_7]) ).
cnf(c_220,plain,
( ~ hasgame(n4,A)
| ~ hasgame(n1,A) ),
inference(resolve,[status(thm)],[c_16,c_4]) ).
cnf(c_221,plain,
( ~ hasgame(n3,A)
| ~ hasgame(n1,A) ),
inference(resolve,[status(thm)],[c_16,c_3]) ).
cnf(c_222,plain,
( ~ hasgame(n2,A)
| ~ hasgame(n1,A) ),
inference(resolve,[status(thm)],[c_16,c_1]) ).
cnf(c_245,plain,
( ~ haspet(A,C)
| ~ haspet(n1,C)
| hasgame(B,quoits)
| ~ nextto(A,B)
| ~ haspet(A,camel) ),
inference(resolve,[status(thm)],[c_19,c_17]) ).
cnf(c_250,plain,
( ~ haspet(n5,C)
| ~ haspet(A,C)
| hasgame(B,quoits)
| ~ nextto(A,B)
| ~ haspet(A,camel) ),
inference(resolve,[status(thm)],[c_20,c_17]) ).
cnf(c_264,plain,
( haspet(n3,camel)
| haspet(n1,camel)
| ~ hasgame(A,quoits)
| ~ nextto(A,n3)
| ~ nextto(A,n1) ),
inference(resolve,[status(thm)],[c_21,c_3]) ).
cnf(c_323,plain,
( ~ hasgame(A,C)
| ~ hasgame(n1,C)
| haspet(B,rat)
| ~ hasgame(A,racquetball)
| ~ nextto(A,B) ),
inference(resolve,[status(thm)],[c_28,c_16]) ).
cnf(c_360,plain,
( ~ hasperson(A,C)
| ~ hasperson(n1,C)
| hascolor(B,blue)
| ~ nextto(A,B)
| ~ hasperson(A,russian) ),
inference(resolve,[status(thm)],[c_31,c_14]) ).
cnf(c_390,plain,
( ~ hascolor(A,C)
| ~ hascolor(n1,C)
| hasperson(B,russian)
| ~ hascolor(A,blue)
| ~ nextto(A,B) ),
inference(resolve,[status(thm)],[c_34,c_13]) ).
cnf(c_401,plain,
( ~ hascolor(A,blue)
| ~ hascolor(A,green) ),
inference(resolve,[status(thm)],[c_59,c_57]) ).
cnf(c_402,plain,
( ~ hascolor(A,yellow)
| ~ hascolor(A,green) ),
inference(resolve,[status(thm)],[c_59,c_56]) ).
cnf(c_403,plain,
( ~ hascolor(A,blue)
| ~ hascolor(A,white) ),
inference(resolve,[status(thm)],[c_59,c_55]) ).
cnf(c_406,plain,
( ~ hascolor(A,blue)
| ~ hascolor(A,red) ),
inference(resolve,[status(thm)],[c_59,c_52]) ).
cnf(c_407,plain,
( ~ hascolor(A,yellow)
| ~ hascolor(A,red) ),
inference(resolve,[status(thm)],[c_59,c_51]) ).
cnf(c_408,plain,
( ~ hascolor(A,green)
| ~ hascolor(A,red) ),
inference(resolve,[status(thm)],[c_59,c_50]) ).
cnf(c_409,plain,
( ~ hascolor(A,white)
| ~ hascolor(A,red) ),
inference(resolve,[status(thm)],[c_59,c_48]) ).
cnf(c_410,plain,
( ~ hasgame(A,charades)
| ~ hasgame(A,solitaire) ),
inference(resolve,[status(thm)],[c_83,c_82]) ).
cnf(c_412,plain,
( ~ hasgame(A,solitaire)
| ~ hasgame(A,quoits) ),
inference(resolve,[status(thm)],[c_83,c_80]) ).
cnf(c_414,plain,
( ~ hasgame(A,solitaire)
| ~ hasgame(A,racquetball) ),
inference(resolve,[status(thm)],[c_83,c_78]) ).
cnf(c_416,plain,
( ~ hasgame(A,charades)
| ~ hasgame(A,backgammon) ),
inference(resolve,[status(thm)],[c_83,c_76]) ).
cnf(c_417,plain,
( ~ hasgame(A,solitaire)
| ~ hasgame(A,backgammon) ),
inference(resolve,[status(thm)],[c_83,c_75]) ).
cnf(c_419,plain,
( ~ hasgame(A,racquetball)
| ~ hasgame(A,backgammon) ),
inference(resolve,[status(thm)],[c_83,c_72]) ).
cnf(c_421,plain,
( ~ haspet(n1,camel)
| hasgame(B,quoits)
| ~ nextto(A,B)
| ~ haspet(A,camel) ),
inference(factor,[status(thm)],[c_245]) ).
cnf(c_11760,plain,
( ~ haspet(n5,camel)
| hasgame(A,quoits)
| ~ nextto(n5,A)
| ~ haspet(n5,camel) ),
inference(factor,[status(thm)],[c_250]) ).
cnf(c_423,plain,
( hasgame(A,quoits)
| ~ nextto(n5,A)
| ~ haspet(n5,camel) ),
inference(copy,[status(thm)],[c_11760]) ).
cnf(c_442,plain,
( ~ hasgame(n1,racquetball)
| haspet(B,rat)
| ~ hasgame(A,racquetball)
| ~ nextto(A,B) ),
inference(factor,[status(thm)],[c_323]) ).
cnf(c_11761,plain,
( ~ hasperson(n1,russian)
| hascolor(B,blue)
| ~ nextto(A,B)
| ~ hasperson(A,russian) ),
inference(factor,[status(thm)],[c_360]) ).
cnf(c_456,plain,
( hascolor(B,blue)
| ~ nextto(A,B)
| ~ hasperson(A,russian) ),
inference(resolve,[status(thm)],[c_177,c_11761]) ).
cnf(c_466,plain,
( ~ hascolor(n1,blue)
| hasperson(B,russian)
| ~ hascolor(A,blue)
| ~ nextto(A,B) ),
inference(factor,[status(thm)],[c_390]) ).
cnf(c_493,plain,
( ~ hasdrink(n4,vodka)
| hasdrink(n5,unknown_drink)
| hasdrink(n3,unknown_drink)
| hasdrink(n2,unknown_drink)
| hasdrink(n1,unknown_drink) ),
inference(resolve,[status(thm)],[c_137,c_115]) ).
cnf(c_521,plain,
( ~ haspet(n4,guppy)
| haspet(n5,no_pet)
| haspet(n3,no_pet)
| haspet(n2,no_pet)
| haspet(n1,no_pet) ),
inference(resolve,[status(thm)],[c_141,c_99]) ).
cnf(c_525,plain,
( ~ haspet(n4,guppy)
| haspet(n5,camel)
| haspet(n3,camel)
| haspet(n2,camel)
| haspet(n1,camel) ),
inference(resolve,[status(thm)],[c_141,c_97]) ).
cnf(c_529,plain,
( hasperson(n5,englishman)
| hasperson(n3,englishman)
| hasperson(n2,englishman)
| hasperson(n1,englishman)
| hascolor(n4,red) ),
inference(resolve,[status(thm)],[c_142,c_133]) ).
cnf(c_535,plain,
( hasperson(n5,italian)
| hasperson(n3,italian)
| hasperson(n2,italian)
| hasperson(n1,italian)
| haspet(n4,guppy) ),
inference(resolve,[status(thm)],[c_147,c_133]) ).
cnf(c_537,plain,
( hasdrink(n5,lemonade)
| hasdrink(n3,lemonade)
| hasdrink(n2,lemonade)
| hasdrink(n1,lemonade)
| hascolor(n4,green) ),
inference(resolve,[status(thm)],[c_149,c_137]) ).
cnf(c_538,plain,
( hascolor(n5,green)
| hascolor(n3,green)
| hascolor(n2,green)
| hascolor(n1,green)
| hasdrink(n4,lemonade) ),
inference(resolve,[status(thm)],[c_150,c_135]) ).
cnf(c_540,plain,
( hasperson(A,american)
| hasperson(A,russian)
| hasperson(A,italian)
| hasperson(A,englishman)
| hasdrink(A,coffee) ),
inference(resolve,[status(thm)],[c_151,c_132]) ).
cnf(c_541,plain,
( hasdrink(n5,coffee)
| hasdrink(n3,coffee)
| hasdrink(n2,coffee)
| hasdrink(n1,coffee)
| hasperson(n4,swede) ),
inference(resolve,[status(thm)],[c_152,c_137]) ).
cnf(c_542,plain,
( haspet(n5,toad)
| haspet(n3,toad)
| haspet(n2,toad)
| haspet(n1,toad)
| hasgame(n4,backgammon) ),
inference(resolve,[status(thm)],[c_153,c_141]) ).
cnf(c_546,plain,
( hascolor(A,blue)
| hascolor(A,green)
| hascolor(A,white)
| hascolor(A,red)
| hasgame(A,racquetball) ),
inference(resolve,[status(thm)],[c_156,c_134]) ).
cnf(c_552,plain,
( hasgame(A,charades)
| hasgame(A,quoits)
| hasgame(A,racquetball)
| hasgame(A,backgammon)
| hasdrink(A,vodka) ),
inference(resolve,[status(thm)],[c_159,c_138]) ).
cnf(c_553,plain,
( hasdrink(n5,vodka)
| hasdrink(n3,vodka)
| hasdrink(n2,vodka)
| hasdrink(n1,vodka)
| hasgame(n4,solitaire) ),
inference(resolve,[status(thm)],[c_160,c_137]) ).
cnf(c_554,plain,
( hasperson(n5,american)
| hasperson(n3,american)
| hasperson(n2,american)
| hasperson(n1,american)
| hasgame(n4,charades) ),
inference(resolve,[status(thm)],[c_161,c_133]) ).
cnf(c_558,plain,
( hascolor(n2,green)
| ~ hascolor(n1,white) ),
inference(resolve,[status(thm)],[c_166,c_145]) ).
cnf(c_559,plain,
nextto(n1,n2),
inference(resolve,[status(thm)],[c_166,c_129]) ).
cnf(c_560,plain,
( ~ hascolor(n3,green)
| hascolor(n2,white) ),
inference(resolve,[status(thm)],[c_167,c_146]) ).
cnf(c_562,plain,
nextto(n2,n3),
inference(resolve,[status(thm)],[c_167,c_129]) ).
cnf(c_564,plain,
( ~ hascolor(n4,green)
| hascolor(n3,white) ),
inference(resolve,[status(thm)],[c_168,c_146]) ).
cnf(c_565,plain,
( hascolor(n4,green)
| ~ hascolor(n3,white) ),
inference(resolve,[status(thm)],[c_168,c_145]) ).
cnf(c_568,plain,
( ~ hascolor(n5,green)
| hascolor(n4,white) ),
inference(resolve,[status(thm)],[c_169,c_146]) ).
cnf(c_569,plain,
( hascolor(n5,green)
| ~ hascolor(n4,white) ),
inference(resolve,[status(thm)],[c_169,c_145]) ).
cnf(c_570,plain,
nextto(n4,n5),
inference(resolve,[status(thm)],[c_169,c_129]) ).
cnf(c_571,plain,
~ hasdrink(n3,unknown_drink),
inference(resolve,[status(thm)],[c_176,c_114]) ).
cnf(c_572,plain,
~ hasdrink(n3,vodka),
inference(resolve,[status(thm)],[c_176,c_113]) ).
cnf(c_573,plain,
~ hasdrink(n3,coffee),
inference(resolve,[status(thm)],[c_176,c_110]) ).
cnf(c_574,plain,
~ hasdrink(n3,lemonade),
inference(resolve,[status(thm)],[c_176,c_107]) ).
cnf(c_578,plain,
( ~ hasdrink(n4,vodka)
| hasdrink(n5,unknown_drink)
| hasdrink(n2,unknown_drink)
| hasdrink(n1,unknown_drink) ),
inference(resolve,[status(thm)],[c_571,c_493]) ).
cnf(c_579,plain,
( hasdrink(n5,vodka)
| hasdrink(n2,vodka)
| hasdrink(n1,vodka)
| hasgame(n4,solitaire) ),
inference(resolve,[status(thm)],[c_572,c_553]) ).
cnf(c_584,plain,
( hasdrink(n5,coffee)
| hasdrink(n2,coffee)
| hasdrink(n1,coffee)
| hasperson(n4,swede) ),
inference(resolve,[status(thm)],[c_573,c_541]) ).
cnf(c_589,plain,
( hasdrink(n5,lemonade)
| hasdrink(n2,lemonade)
| hasdrink(n1,lemonade)
| hascolor(n4,green) ),
inference(resolve,[status(thm)],[c_574,c_537]) ).
cnf(c_595,plain,
~ hasperson(n1,american),
inference(resolve,[status(thm)],[c_177,c_125]) ).
cnf(c_596,plain,
~ hasperson(n1,swede),
inference(resolve,[status(thm)],[c_177,c_123]) ).
cnf(c_597,plain,
~ hasperson(n1,italian),
inference(resolve,[status(thm)],[c_177,c_121]) ).
cnf(c_598,plain,
~ hasperson(n1,englishman),
inference(resolve,[status(thm)],[c_177,c_118]) ).
cnf(c_599,plain,
( hasperson(n5,american)
| hasperson(n3,american)
| hasperson(n2,american)
| hasgame(n4,charades) ),
inference(resolve,[status(thm)],[c_595,c_554]) ).
cnf(c_609,plain,
( hasperson(n5,italian)
| hasperson(n3,italian)
| hasperson(n2,italian)
| haspet(n4,guppy) ),
inference(resolve,[status(thm)],[c_597,c_535]) ).
cnf(c_614,plain,
( hasperson(n5,englishman)
| hasperson(n3,englishman)
| hasperson(n2,englishman)
| hascolor(n4,red) ),
inference(resolve,[status(thm)],[c_598,c_529]) ).
cnf(c_619,plain,
( ~ haspet(n5,V23)
| ~ haspet(n4,V22)
| ~ haspet(n3,V21)
| ~ haspet(n2,V20)
| ~ haspet(n1,V19)
| ~ hasgame(n5,V18)
| ~ hasgame(n4,V17)
| ~ hasgame(n3,V16)
| ~ hasgame(n2,V15)
| ~ hasgame(n1,V14)
| ~ hasdrink(n5,V13)
| ~ hasdrink(n4,V12)
| ~ hasdrink(n3,V11)
| ~ hasdrink(n2,V10)
| ~ hasdrink(n1,V9)
| ~ hascolor(n5,V8)
| ~ hascolor(n4,V7)
| ~ hascolor(n3,V6)
| ~ hascolor(n2,F)
| ~ hascolor(n1,E)
| ~ hasperson(n5,D)
| ~ hasperson(n4,C)
| ~ hasperson(n3,B)
| ~ hasperson(n2,A) ),
inference(resolve,[status(thm)],[c_178,c_177]) ).
cnf(c_670,plain,
( hascolor(n3,blue)
| hascolor(n3,green)
| hascolor(n3,white)
| hascolor(n3,red)
| ~ hascolor(n1,yellow) ),
inference(resolve,[status(thm)],[c_188,c_134]) ).
cnf(c_703,plain,
~ hasperson(n4,russian),
inference(resolve,[status(thm)],[c_198,c_177]) ).
cnf(c_711,plain,
~ hasperson(n3,russian),
inference(resolve,[status(thm)],[c_199,c_177]) ).
cnf(c_719,plain,
~ hasperson(n2,russian),
inference(resolve,[status(thm)],[c_200,c_177]) ).
cnf(c_769,plain,
( hasgame(n2,charades)
| hasgame(n2,quoits)
| hasgame(n2,racquetball)
| hasgame(n2,backgammon)
| ~ hasgame(n5,solitaire) ),
inference(resolve,[status(thm)],[c_216,c_138]) ).
cnf(c_950,plain,
( hascolor(n5,green)
| hascolor(n3,green)
| hascolor(n2,green)
| hascolor(n1,green)
| ~ hascolor(n4,red) ),
inference(resolve,[status(thm)],[c_408,c_135]) ).
cnf(c_11762,plain,
( ~ hascolor(n1,blue)
| hasperson(n2,russian)
| ~ hascolor(n1,blue) ),
inference(resolve,[status(thm)],[c_559,c_466]) ).
cnf(c_11763,plain,
( hasperson(n2,russian)
| ~ hascolor(n1,blue) ),
inference(copy,[status(thm)],[c_11762]) ).
cnf(c_974,plain,
~ hascolor(n1,blue),
inference(resolve,[status(thm)],[c_719,c_11763]) ).
cnf(c_11764,plain,
( hascolor(n2,blue)
| ~ hasperson(n1,russian) ),
inference(resolve,[status(thm)],[c_559,c_456]) ).
cnf(c_975,plain,
hascolor(n2,blue),
inference(resolve,[status(thm)],[c_177,c_11764]) ).
cnf(c_11765,plain,
( ~ hasgame(n1,racquetball)
| haspet(n2,rat)
| ~ hasgame(n1,racquetball) ),
inference(resolve,[status(thm)],[c_559,c_442]) ).
cnf(c_976,plain,
( haspet(n2,rat)
| ~ hasgame(n1,racquetball) ),
inference(copy,[status(thm)],[c_11765]) ).
cnf(c_11766,plain,
( ~ haspet(n1,camel)
| hasgame(n2,quoits)
| ~ haspet(n1,camel) ),
inference(resolve,[status(thm)],[c_559,c_421]) ).
cnf(c_979,plain,
( hasgame(n2,quoits)
| ~ haspet(n1,camel) ),
inference(copy,[status(thm)],[c_11766]) ).
cnf(c_980,plain,
nextto(n2,n1),
inference(resolve,[status(thm)],[c_559,c_126]) ).
cnf(c_11767,plain,
( haspet(n3,camel)
| haspet(n1,camel)
| ~ hasgame(n2,quoits)
| ~ nextto(n2,n1) ),
inference(resolve,[status(thm)],[c_562,c_264]) ).
cnf(c_1007,plain,
( haspet(n3,camel)
| haspet(n1,camel)
| ~ hasgame(n2,quoits) ),
inference(resolve,[status(thm)],[c_980,c_11767]) ).
cnf(c_1096,plain,
nextto(n5,n4),
inference(resolve,[status(thm)],[c_570,c_126]) ).
cnf(c_1097,plain,
~ hascolor(n2,red),
inference(resolve,[status(thm)],[c_975,c_406]) ).
cnf(c_1098,plain,
~ hascolor(n2,white),
inference(resolve,[status(thm)],[c_975,c_403]) ).
cnf(c_1099,plain,
~ hascolor(n2,green),
inference(resolve,[status(thm)],[c_975,c_401]) ).
cnf(c_1102,plain,
~ hascolor(n3,blue),
inference(resolve,[status(thm)],[c_975,c_185]) ).
cnf(c_1113,plain,
~ hascolor(n3,green),
inference(resolve,[status(thm)],[c_1098,c_560]) ).
cnf(c_11768,plain,
( hascolor(n5,green)
| hascolor(n3,green)
| hascolor(n1,green)
| ~ hascolor(n4,red) ),
inference(resolve,[status(thm)],[c_1099,c_950]) ).
cnf(c_1116,plain,
( hascolor(n5,green)
| hascolor(n1,green)
| ~ hascolor(n4,red) ),
inference(resolve,[status(thm)],[c_1113,c_11768]) ).
cnf(c_1118,plain,
~ hascolor(n1,white),
inference(resolve,[status(thm)],[c_1099,c_558]) ).
cnf(c_11769,plain,
( hascolor(n5,green)
| hascolor(n3,green)
| hascolor(n1,green)
| hasdrink(n4,lemonade) ),
inference(resolve,[status(thm)],[c_1099,c_538]) ).
cnf(c_1119,plain,
( hascolor(n5,green)
| hascolor(n1,green)
| hasdrink(n4,lemonade) ),
inference(resolve,[status(thm)],[c_1113,c_11769]) ).
cnf(c_11770,plain,
( hascolor(n3,blue)
| hascolor(n3,white)
| hascolor(n3,red)
| ~ hascolor(n1,yellow) ),
inference(resolve,[status(thm)],[c_1113,c_670]) ).
cnf(c_1126,plain,
( hascolor(n3,white)
| hascolor(n3,red)
| ~ hascolor(n1,yellow) ),
inference(resolve,[status(thm)],[c_1102,c_11770]) ).
cnf(c_1206,plain,
( hasgame(n4,quoits)
| ~ haspet(n5,camel) ),
inference(resolve,[status(thm)],[c_1096,c_423]) ).
cnf(c_11771,plain,
( hascolor(n5,green)
| hascolor(n3,green)
| hascolor(n2,green)
| hascolor(n1,green)
| hascolor(n3,white) ),
inference(resolve,[status(thm)],[c_564,c_135]) ).
cnf(c_11772,plain,
( hascolor(n5,green)
| hascolor(n3,green)
| hascolor(n1,green)
| hascolor(n3,white) ),
inference(resolve,[status(thm)],[c_1099,c_11771]) ).
cnf(c_1207,plain,
( hascolor(n5,green)
| hascolor(n1,green)
| hascolor(n3,white) ),
inference(resolve,[status(thm)],[c_1113,c_11772]) ).
cnf(c_11773,plain,
( hascolor(n5,white)
| hascolor(n3,white)
| hascolor(n2,white)
| hascolor(n1,white)
| hascolor(n5,green) ),
inference(resolve,[status(thm)],[c_569,c_135]) ).
cnf(c_11774,plain,
( hascolor(n5,white)
| hascolor(n3,white)
| hascolor(n2,white)
| hascolor(n5,green) ),
inference(resolve,[status(thm)],[c_1118,c_11773]) ).
cnf(c_1208,plain,
( hascolor(n5,white)
| hascolor(n3,white)
| hascolor(n5,green) ),
inference(resolve,[status(thm)],[c_1098,c_11774]) ).
cnf(c_1217,plain,
( ~ haspet(n5,V22)
| ~ haspet(n4,V21)
| ~ haspet(n3,V20)
| ~ haspet(n2,V19)
| ~ haspet(n1,V18)
| ~ hasgame(n5,V17)
| ~ hasgame(n4,V16)
| ~ hasgame(n3,V15)
| ~ hasgame(n2,V14)
| ~ hasgame(n1,V13)
| ~ hasdrink(n5,V12)
| ~ hasdrink(n4,V11)
| ~ hasdrink(n3,V10)
| ~ hasdrink(n2,V9)
| ~ hasdrink(n1,V8)
| ~ hascolor(n5,V7)
| ~ hascolor(n4,V6)
| ~ hascolor(n3,F)
| ~ hascolor(n1,E)
| ~ hasperson(n5,D)
| ~ hasperson(n4,C)
| ~ hasperson(n3,B)
| ~ hasperson(n2,A) ),
inference(resolve,[status(thm)],[c_619,c_975]) ).
cnf(c_1252,plain,
( ~ haspet(n5,V21)
| ~ haspet(n4,V20)
| ~ haspet(n3,V19)
| ~ haspet(n2,V18)
| ~ haspet(n1,V17)
| ~ hasgame(n5,V16)
| ~ hasgame(n4,V15)
| ~ hasgame(n3,V14)
| ~ hasgame(n2,V13)
| ~ hasgame(n1,V12)
| ~ hasdrink(n5,V11)
| ~ hasdrink(n4,V10)
| ~ hasdrink(n2,V9)
| ~ hasdrink(n1,V8)
| ~ hascolor(n5,V7)
| ~ hascolor(n4,V6)
| ~ hascolor(n3,F)
| ~ hascolor(n1,E)
| ~ hasperson(n5,D)
| ~ hasperson(n4,C)
| ~ hasperson(n3,B)
| ~ hasperson(n2,A) ),
inference(resolve,[status(thm)],[c_1217,c_176]) ).
cnf(c_1305,plain,
( ~ hasdrink(n4,vodka)
| hascolor(n5,green)
| hascolor(n1,green) ),
inference(resolve,[status(thm)],[c_1119,c_108]) ).
cnf(c_1306,plain,
( ~ hasdrink(n4,coffee)
| hascolor(n5,green)
| hascolor(n1,green) ),
inference(resolve,[status(thm)],[c_1119,c_106]) ).
cnf(c_11775,plain,
( hascolor(n1,blue)
| hascolor(n1,green)
| hascolor(n1,white)
| hascolor(n1,red)
| hascolor(n3,white)
| hascolor(n3,red) ),
inference(resolve,[status(thm)],[c_1126,c_134]) ).
cnf(c_11776,plain,
( hascolor(n1,blue)
| hascolor(n1,green)
| hascolor(n1,red)
| hascolor(n3,white)
| hascolor(n3,red) ),
inference(resolve,[status(thm)],[c_1118,c_11775]) ).
cnf(c_1307,plain,
( hascolor(n1,green)
| hascolor(n1,red)
| hascolor(n3,white)
| hascolor(n3,red) ),
inference(resolve,[status(thm)],[c_974,c_11776]) ).
cnf(c_1318,plain,
( ~ hascolor(n3,red)
| hascolor(n5,green)
| hascolor(n1,green) ),
inference(resolve,[status(thm)],[c_1207,c_409]) ).
cnf(c_1331,plain,
( hascolor(n4,green)
| hascolor(n5,white)
| hascolor(n5,green) ),
inference(resolve,[status(thm)],[c_1208,c_565]) ).
cnf(c_1332,plain,
( ~ hascolor(n3,red)
| hascolor(n5,white)
| hascolor(n5,green) ),
inference(resolve,[status(thm)],[c_1208,c_409]) ).
cnf(c_11777,plain,
( hasdrink(n5,vodka)
| hasdrink(n3,vodka)
| hasdrink(n2,vodka)
| hasdrink(n1,vodka)
| hascolor(n5,green)
| hascolor(n1,green) ),
inference(resolve,[status(thm)],[c_1305,c_137]) ).
cnf(c_1343,plain,
( hasdrink(n5,vodka)
| hasdrink(n2,vodka)
| hasdrink(n1,vodka)
| hascolor(n5,green)
| hascolor(n1,green) ),
inference(resolve,[status(thm)],[c_572,c_11777]) ).
cnf(c_1346,plain,
( ~ hascolor(n4,red)
| hascolor(n5,white)
| hascolor(n5,green) ),
inference(resolve,[status(thm)],[c_1331,c_408]) ).
cnf(c_1352,plain,
( ~ hascolor(n1,green)
| hascolor(n5,white)
| hascolor(n5,green) ),
inference(resolve,[status(thm)],[c_1331,c_187]) ).
cnf(c_1383,plain,
( hasgame(n2,solitaire)
| hasdrink(n5,vodka)
| hasdrink(n1,vodka)
| hasgame(n4,solitaire) ),
inference(resolve,[status(thm)],[c_579,c_160]) ).
cnf(c_1385,plain,
( ~ hasdrink(n2,coffee)
| hasdrink(n5,vodka)
| hasdrink(n1,vodka)
| hasgame(n4,solitaire) ),
inference(resolve,[status(thm)],[c_579,c_111]) ).
cnf(c_1393,plain,
( hasperson(n2,swede)
| hasdrink(n5,coffee)
| hasdrink(n1,coffee)
| hasperson(n4,swede) ),
inference(resolve,[status(thm)],[c_584,c_152]) ).
cnf(c_11778,plain,
( hascolor(n2,green)
| hasdrink(n5,lemonade)
| hasdrink(n1,lemonade)
| hascolor(n4,green) ),
inference(resolve,[status(thm)],[c_589,c_149]) ).
cnf(c_1402,plain,
( hasdrink(n5,lemonade)
| hasdrink(n1,lemonade)
| hascolor(n4,green) ),
inference(resolve,[status(thm)],[c_1099,c_11778]) ).
cnf(c_1413,plain,
( hascolor(n1,green)
| hasdrink(n5,lemonade)
| hascolor(n4,green) ),
inference(resolve,[status(thm)],[c_1402,c_149]) ).
cnf(c_1427,plain,
( ~ hasdrink(n5,vodka)
| hascolor(n1,green)
| hascolor(n4,green) ),
inference(resolve,[status(thm)],[c_1413,c_108]) ).
cnf(c_1434,plain,
( hasgame(n2,charades)
| hasperson(n5,american)
| hasperson(n3,american)
| hasgame(n4,charades) ),
inference(resolve,[status(thm)],[c_599,c_161]) ).
cnf(c_1464,plain,
( haspet(n2,guppy)
| hasperson(n5,italian)
| hasperson(n3,italian)
| haspet(n4,guppy) ),
inference(resolve,[status(thm)],[c_609,c_147]) ).
cnf(c_11779,plain,
( hascolor(n2,red)
| hasperson(n5,englishman)
| hasperson(n3,englishman)
| hascolor(n4,red) ),
inference(resolve,[status(thm)],[c_614,c_142]) ).
cnf(c_1481,plain,
( hasperson(n5,englishman)
| hasperson(n3,englishman)
| hascolor(n4,red) ),
inference(resolve,[status(thm)],[c_1097,c_11779]) ).
cnf(c_1486,plain,
( hascolor(n3,red)
| hasperson(n5,englishman)
| hascolor(n4,red) ),
inference(resolve,[status(thm)],[c_1481,c_142]) ).
cnf(c_1499,plain,
( hascolor(n5,red)
| hascolor(n3,red)
| hascolor(n4,red) ),
inference(resolve,[status(thm)],[c_1486,c_142]) ).
cnf(c_1500,plain,
( ~ hasperson(n5,american)
| hascolor(n3,red)
| hascolor(n4,red) ),
inference(resolve,[status(thm)],[c_1486,c_119]) ).
cnf(c_11780,plain,
( hascolor(n5,green)
| hascolor(n1,green)
| hasperson(n4,american)
| hasperson(n4,russian)
| hasperson(n4,italian)
| hasperson(n4,englishman) ),
inference(resolve,[status(thm)],[c_540,c_1306]) ).
cnf(c_1505,plain,
( hascolor(n5,green)
| hascolor(n1,green)
| hasperson(n4,american)
| hasperson(n4,italian)
| hasperson(n4,englishman) ),
inference(resolve,[status(thm)],[c_703,c_11780]) ).
cnf(c_11781,plain,
( hasperson(n3,american)
| hasperson(n3,russian)
| hasperson(n3,italian)
| hasperson(n3,englishman) ),
inference(resolve,[status(thm)],[c_540,c_573]) ).
cnf(c_1512,plain,
( hasperson(n3,american)
| hasperson(n3,italian)
| hasperson(n3,englishman) ),
inference(resolve,[status(thm)],[c_711,c_11781]) ).
cnf(c_1543,plain,
( hascolor(n5,white)
| hascolor(n5,green)
| hascolor(n5,red)
| hascolor(n3,red) ),
inference(resolve,[status(thm)],[c_1499,c_1346]) ).
cnf(c_1546,plain,
( hascolor(n5,green)
| hascolor(n1,green)
| hascolor(n5,red)
| hascolor(n3,red) ),
inference(resolve,[status(thm)],[c_1499,c_1116]) ).
cnf(c_1548,plain,
( ~ hascolor(n4,green)
| hascolor(n5,red)
| hascolor(n3,red) ),
inference(resolve,[status(thm)],[c_1499,c_408]) ).
cnf(c_1554,plain,
( ~ hascolor(n1,red)
| hascolor(n5,red)
| hascolor(n3,red) ),
inference(resolve,[status(thm)],[c_1499,c_187]) ).
cnf(c_1563,plain,
( ~ haspet(n2,rat)
| haspet(n5,toad)
| haspet(n3,toad)
| haspet(n1,toad)
| hasgame(n4,backgammon) ),
inference(resolve,[status(thm)],[c_542,c_101]) ).
cnf(c_1576,plain,
( haspet(n3,guppy)
| hasperson(n3,american)
| hasperson(n3,englishman) ),
inference(resolve,[status(thm)],[c_1512,c_147]) ).
cnf(c_1610,plain,
( hascolor(n3,red)
| haspet(n3,guppy)
| hasperson(n3,american) ),
inference(resolve,[status(thm)],[c_1576,c_142]) ).
cnf(c_11782,plain,
( hascolor(n5,red)
| hascolor(n3,red)
| hascolor(n1,blue)
| hascolor(n1,green)
| hascolor(n1,white)
| hasgame(n1,racquetball) ),
inference(resolve,[status(thm)],[c_546,c_1554]) ).
cnf(c_11783,plain,
( hascolor(n5,red)
| hascolor(n3,red)
| hascolor(n1,blue)
| hascolor(n1,green)
| hasgame(n1,racquetball) ),
inference(resolve,[status(thm)],[c_1118,c_11782]) ).
cnf(c_1625,plain,
( hascolor(n5,red)
| hascolor(n3,red)
| hascolor(n1,green)
| hasgame(n1,racquetball) ),
inference(resolve,[status(thm)],[c_974,c_11783]) ).
cnf(c_11784,plain,
( ~ hascolor(n3,red)
| hascolor(n1,blue)
| hascolor(n1,green)
| hascolor(n1,white)
| hasgame(n1,racquetball) ),
inference(resolve,[status(thm)],[c_546,c_188]) ).
cnf(c_11785,plain,
( ~ hascolor(n3,red)
| hascolor(n1,blue)
| hascolor(n1,green)
| hasgame(n1,racquetball) ),
inference(resolve,[status(thm)],[c_1118,c_11784]) ).
cnf(c_1646,plain,
( ~ hascolor(n3,red)
| hascolor(n1,green)
| hasgame(n1,racquetball) ),
inference(resolve,[status(thm)],[c_974,c_11785]) ).
cnf(c_11786,plain,
( ~ hascolor(n5,red)
| hascolor(n1,blue)
| hascolor(n1,green)
| hascolor(n1,white)
| hasgame(n1,racquetball) ),
inference(resolve,[status(thm)],[c_546,c_186]) ).
cnf(c_11787,plain,
( ~ hascolor(n5,red)
| hascolor(n1,blue)
| hascolor(n1,green)
| hasgame(n1,racquetball) ),
inference(resolve,[status(thm)],[c_1118,c_11786]) ).
cnf(c_1650,plain,
( ~ hascolor(n5,red)
| hascolor(n1,green)
| hasgame(n1,racquetball) ),
inference(resolve,[status(thm)],[c_974,c_11787]) ).
cnf(c_1670,plain,
( hasgame(n3,charades)
| hascolor(n3,red)
| haspet(n3,guppy) ),
inference(resolve,[status(thm)],[c_1610,c_161]) ).
cnf(c_1679,plain,
( hascolor(n5,green)
| hascolor(n1,green)
| hasgame(n3,charades)
| haspet(n3,guppy) ),
inference(resolve,[status(thm)],[c_1670,c_1318]) ).
cnf(c_1738,plain,
( hasgame(n3,charades)
| hasgame(n3,quoits)
| hasgame(n3,racquetball)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_552,c_572]) ).
cnf(c_1825,plain,
( hasperson(n3,englishman)
| hascolor(n1,green)
| hascolor(n1,red)
| hascolor(n3,white) ),
inference(resolve,[status(thm)],[c_1307,c_143]) ).
cnf(c_1835,plain,
( hasgame(n1,solitaire)
| hasgame(n2,solitaire)
| hasdrink(n5,vodka)
| hasgame(n4,solitaire) ),
inference(resolve,[status(thm)],[c_1383,c_160]) ).
cnf(c_11788,plain,
( hasperson(n1,swede)
| hasperson(n2,swede)
| hasdrink(n5,coffee)
| hasperson(n4,swede) ),
inference(resolve,[status(thm)],[c_1393,c_152]) ).
cnf(c_1850,plain,
( hasperson(n2,swede)
| hasdrink(n5,coffee)
| hasperson(n4,swede) ),
inference(resolve,[status(thm)],[c_596,c_11788]) ).
cnf(c_1861,plain,
( hasperson(n5,swede)
| hasperson(n2,swede)
| hasperson(n4,swede) ),
inference(resolve,[status(thm)],[c_1850,c_152]) ).
cnf(c_1863,plain,
( ~ hasdrink(n5,vodka)
| hasperson(n2,swede)
| hasperson(n4,swede) ),
inference(resolve,[status(thm)],[c_1850,c_111]) ).
cnf(c_1864,plain,
( ~ hasdrink(n5,lemonade)
| hasperson(n2,swede)
| hasperson(n4,swede) ),
inference(resolve,[status(thm)],[c_1850,c_106]) ).
cnf(c_1877,plain,
( hasdrink(n4,coffee)
| hasperson(n5,swede)
| hasperson(n2,swede) ),
inference(resolve,[status(thm)],[c_1861,c_151]) ).
cnf(c_1886,plain,
( hascolor(n5,green)
| hascolor(n1,green)
| hasperson(n5,swede)
| hasperson(n2,swede) ),
inference(resolve,[status(thm)],[c_1877,c_1306]) ).
cnf(c_1914,plain,
( hasgame(n3,charades)
| hasgame(n2,charades)
| hasperson(n5,american)
| hasgame(n4,charades) ),
inference(resolve,[status(thm)],[c_1434,c_161]) ).
cnf(c_1917,plain,
( ~ hasperson(n3,englishman)
| hasgame(n2,charades)
| hasperson(n5,american)
| hasgame(n4,charades) ),
inference(resolve,[status(thm)],[c_1434,c_119]) ).
cnf(c_1924,plain,
( ~ hasperson(n3,american)
| haspet(n2,guppy)
| hasperson(n5,italian)
| haspet(n4,guppy) ),
inference(resolve,[status(thm)],[c_1464,c_122]) ).
cnf(c_1926,plain,
( ~ hasperson(n3,englishman)
| haspet(n2,guppy)
| hasperson(n5,italian)
| haspet(n4,guppy) ),
inference(resolve,[status(thm)],[c_1464,c_116]) ).
cnf(c_11789,plain,
( hascolor(n5,white)
| hascolor(n5,green)
| hascolor(n5,white)
| hascolor(n5,green)
| hascolor(n5,red) ),
inference(resolve,[status(thm)],[c_1543,c_1332]) ).
cnf(c_11790,plain,
( hascolor(n5,white)
| hascolor(n5,white)
| hascolor(n5,green)
| hascolor(n5,red) ),
inference(copy,[status(thm)],[c_11789]) ).
cnf(c_1937,plain,
( hascolor(n5,white)
| hascolor(n5,green)
| hascolor(n5,red) ),
inference(copy,[status(thm)],[c_11790]) ).
cnf(c_1938,plain,
( hascolor(n1,green)
| hasgame(n1,racquetball)
| hascolor(n5,white)
| hascolor(n5,green) ),
inference(resolve,[status(thm)],[c_1937,c_1650]) ).
cnf(c_11791,plain,
( hascolor(n5,green)
| hascolor(n1,green)
| hascolor(n5,green)
| hascolor(n1,green)
| hascolor(n5,red) ),
inference(resolve,[status(thm)],[c_1546,c_1318]) ).
cnf(c_11792,plain,
( hascolor(n5,green)
| hascolor(n5,green)
| hascolor(n1,green)
| hascolor(n5,red) ),
inference(copy,[status(thm)],[c_11791]) ).
cnf(c_1977,plain,
( hascolor(n5,green)
| hascolor(n1,green)
| hascolor(n5,red) ),
inference(copy,[status(thm)],[c_11792]) ).
cnf(c_1980,plain,
( ~ hascolor(n1,yellow)
| hascolor(n5,green)
| hascolor(n5,red) ),
inference(resolve,[status(thm)],[c_1977,c_402]) ).
cnf(c_11793,plain,
( hascolor(n1,green)
| hasgame(n1,racquetball)
| hascolor(n5,red)
| hascolor(n1,green)
| hasgame(n1,racquetball) ),
inference(resolve,[status(thm)],[c_1625,c_1646]) ).
cnf(c_11794,plain,
( hascolor(n1,green)
| hascolor(n5,red)
| hascolor(n1,green)
| hasgame(n1,racquetball) ),
inference(copy,[status(thm)],[c_11793]) ).
cnf(c_2007,plain,
( hascolor(n5,red)
| hascolor(n1,green)
| hasgame(n1,racquetball) ),
inference(copy,[status(thm)],[c_11794]) ).
cnf(c_2016,plain,
( ~ hascolor(n5,green)
| hascolor(n5,red)
| hasgame(n1,racquetball) ),
inference(resolve,[status(thm)],[c_2007,c_186]) ).
cnf(c_11795,plain,
( left(A,n1)
| ~ hascolor(A,white)
| hascolor(n5,red)
| hasgame(n1,racquetball) ),
inference(resolve,[status(thm)],[c_2007,c_144]) ).
cnf(c_2020,plain,
( ~ hascolor(A,white)
| hascolor(n5,red)
| hasgame(n1,racquetball) ),
inference(resolve,[status(thm)],[c_164,c_11795]) ).
cnf(c_2078,plain,
( ~ hascolor(n1,yellow)
| hascolor(n5,green)
| hasgame(n3,charades)
| haspet(n3,guppy) ),
inference(resolve,[status(thm)],[c_1679,c_402]) ).
cnf(c_2091,plain,
( ~ hasgame(n4,charades)
| hasgame(n3,quoits)
| hasgame(n3,racquetball)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_1738,c_215]) ).
cnf(c_2095,plain,
( hasperson(n3,american)
| hasgame(n3,quoits)
| hasgame(n3,racquetball)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_1738,c_162]) ).
cnf(c_2136,plain,
( ~ hasperson(n3,american)
| hascolor(n1,green)
| hascolor(n1,red)
| hascolor(n3,white) ),
inference(resolve,[status(thm)],[c_1825,c_119]) ).
cnf(c_2139,plain,
( hasperson(n2,swede)
| hasperson(n4,swede)
| hasgame(n1,solitaire)
| hasgame(n2,solitaire)
| hasgame(n4,solitaire) ),
inference(resolve,[status(thm)],[c_1835,c_1863]) ).
cnf(c_2140,plain,
( hascolor(n1,green)
| hascolor(n4,green)
| hasgame(n1,solitaire)
| hasgame(n2,solitaire)
| hasgame(n4,solitaire) ),
inference(resolve,[status(thm)],[c_1835,c_1427]) ).
cnf(c_2149,plain,
( hasgame(n5,solitaire)
| hasgame(n1,solitaire)
| hasgame(n2,solitaire)
| hasgame(n4,solitaire) ),
inference(resolve,[status(thm)],[c_1835,c_160]) ).
cnf(c_2210,plain,
( hasdrink(n2,coffee)
| hascolor(n5,green)
| hascolor(n1,green)
| hasperson(n5,swede) ),
inference(resolve,[status(thm)],[c_1886,c_151]) ).
cnf(c_2229,plain,
( hascolor(n1,green)
| hascolor(n1,red)
| hascolor(n3,white)
| hasgame(n2,charades)
| hasperson(n5,american)
| hasgame(n4,charades) ),
inference(resolve,[status(thm)],[c_1917,c_1825]) ).
cnf(c_2244,plain,
( hascolor(n1,green)
| hascolor(n1,red)
| hascolor(n3,white)
| haspet(n2,guppy)
| hasperson(n5,italian)
| haspet(n4,guppy) ),
inference(resolve,[status(thm)],[c_1926,c_1825]) ).
cnf(c_11796,plain,
( hascolor(n5,white)
| hascolor(n5,green)
| hasgame(n1,racquetball)
| hascolor(n5,white)
| hascolor(n5,green) ),
inference(resolve,[status(thm)],[c_1938,c_1352]) ).
cnf(c_11797,plain,
( hascolor(n5,white)
| hasgame(n1,racquetball)
| hascolor(n5,white)
| hascolor(n5,green) ),
inference(copy,[status(thm)],[c_11796]) ).
cnf(c_2246,plain,
( hasgame(n1,racquetball)
| hascolor(n5,white)
| hascolor(n5,green) ),
inference(copy,[status(thm)],[c_11797]) ).
cnf(c_11798,plain,
( hascolor(n5,red)
| hasgame(n1,racquetball)
| hasgame(n1,racquetball)
| hascolor(n5,green) ),
inference(resolve,[status(thm)],[c_2246,c_2020]) ).
cnf(c_2247,plain,
( hascolor(n5,red)
| hasgame(n1,racquetball)
| hascolor(n5,green) ),
inference(copy,[status(thm)],[c_11798]) ).
cnf(c_2251,plain,
( ~ hascolor(n5,red)
| hasgame(n1,racquetball)
| hascolor(n5,green) ),
inference(resolve,[status(thm)],[c_2246,c_409]) ).
cnf(c_11799,plain,
( hasgame(n1,racquetball)
| hascolor(n5,green)
| hasgame(n1,racquetball)
| hascolor(n5,green) ),
inference(resolve,[status(thm)],[c_2251,c_2247]) ).
cnf(c_11800,plain,
( hasgame(n1,racquetball)
| hasgame(n1,racquetball)
| hascolor(n5,green) ),
inference(copy,[status(thm)],[c_11799]) ).
cnf(c_2281,plain,
( hasgame(n1,racquetball)
| hascolor(n5,green) ),
inference(copy,[status(thm)],[c_11800]) ).
cnf(c_11801,plain,
( hascolor(n5,red)
| hasgame(n1,racquetball)
| hasgame(n1,racquetball) ),
inference(resolve,[status(thm)],[c_2281,c_2016]) ).
cnf(c_2282,plain,
( hascolor(n5,red)
| hasgame(n1,racquetball) ),
inference(copy,[status(thm)],[c_11801]) ).
cnf(c_2285,plain,
( ~ hascolor(n5,red)
| hasgame(n1,racquetball) ),
inference(resolve,[status(thm)],[c_2281,c_408]) ).
cnf(c_11802,plain,
( hasgame(n1,racquetball)
| hasgame(n1,racquetball) ),
inference(resolve,[status(thm)],[c_2285,c_2282]) ).
cnf(c_2324,plain,
hasgame(n1,racquetball),
inference(copy,[status(thm)],[c_11802]) ).
cnf(c_2325,plain,
haspet(n2,rat),
inference(resolve,[status(thm)],[c_2324,c_976]) ).
cnf(c_2328,plain,
( haspet(n5,toad)
| haspet(n3,toad)
| haspet(n1,toad)
| hasgame(n4,backgammon) ),
inference(resolve,[status(thm)],[c_2325,c_1563]) ).
cnf(c_2331,plain,
( ~ haspet(n5,V20)
| ~ haspet(n4,V19)
| ~ haspet(n3,V18)
| ~ haspet(n2,V17)
| ~ haspet(n1,V16)
| ~ hasgame(n5,V15)
| ~ hasgame(n4,V14)
| ~ hasgame(n3,V13)
| ~ hasgame(n2,V12)
| ~ hasdrink(n5,V11)
| ~ hasdrink(n4,V10)
| ~ hasdrink(n2,V9)
| ~ hasdrink(n1,V8)
| ~ hascolor(n5,V7)
| ~ hascolor(n4,V6)
| ~ hascolor(n3,F)
| ~ hascolor(n1,E)
| ~ hasperson(n5,D)
| ~ hasperson(n4,C)
| ~ hasperson(n3,B)
| ~ hasperson(n2,A) ),
inference(resolve,[status(thm)],[c_2324,c_1252]) ).
cnf(c_2332,plain,
~ hasgame(n1,backgammon),
inference(resolve,[status(thm)],[c_2324,c_419]) ).
cnf(c_2334,plain,
~ hasgame(n1,solitaire),
inference(resolve,[status(thm)],[c_2324,c_414]) ).
cnf(c_2339,plain,
~ hasgame(n2,racquetball),
inference(resolve,[status(thm)],[c_2324,c_222]) ).
cnf(c_2340,plain,
~ hasgame(n3,racquetball),
inference(resolve,[status(thm)],[c_2324,c_221]) ).
cnf(c_2341,plain,
~ hasgame(n4,racquetball),
inference(resolve,[status(thm)],[c_2324,c_220]) ).
cnf(c_2346,plain,
hascolor(n1,yellow),
inference(resolve,[status(thm)],[c_2324,c_155]) ).
cnf(c_2398,plain,
( hasgame(n5,solitaire)
| hasgame(n2,solitaire)
| hasgame(n4,solitaire) ),
inference(resolve,[status(thm)],[c_2334,c_2149]) ).
cnf(c_2406,plain,
( hascolor(n1,green)
| hascolor(n4,green)
| hasgame(n2,solitaire)
| hasgame(n4,solitaire) ),
inference(resolve,[status(thm)],[c_2334,c_2140]) ).
cnf(c_2407,plain,
( hasperson(n2,swede)
| hasperson(n4,swede)
| hasgame(n2,solitaire)
| hasgame(n4,solitaire) ),
inference(resolve,[status(thm)],[c_2334,c_2139]) ).
cnf(c_2456,plain,
( hasgame(n2,charades)
| hasgame(n2,quoits)
| hasgame(n2,backgammon)
| ~ hasgame(n5,solitaire) ),
inference(resolve,[status(thm)],[c_2339,c_769]) ).
cnf(c_2476,plain,
( hasperson(n3,american)
| hasgame(n3,quoits)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_2340,c_2095]) ).
cnf(c_2480,plain,
( ~ hasgame(n4,charades)
| hasgame(n3,quoits)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_2340,c_2091]) ).
cnf(c_2541,plain,
( hascolor(n5,green)
| hasgame(n3,charades)
| haspet(n3,guppy) ),
inference(resolve,[status(thm)],[c_2346,c_2078]) ).
cnf(c_2542,plain,
( hascolor(n5,green)
| hascolor(n5,red) ),
inference(resolve,[status(thm)],[c_2346,c_1980]) ).
cnf(c_2580,plain,
~ haspet(n2,no_pet),
inference(resolve,[status(thm)],[c_2325,c_105]) ).
cnf(c_2581,plain,
~ haspet(n2,camel),
inference(resolve,[status(thm)],[c_2325,c_103]) ).
cnf(c_2582,plain,
~ haspet(n2,toad),
inference(resolve,[status(thm)],[c_2325,c_101]) ).
cnf(c_2583,plain,
~ haspet(n2,guppy),
inference(resolve,[status(thm)],[c_2325,c_98]) ).
cnf(c_2588,plain,
( ~ haspet(n4,guppy)
| haspet(n5,no_pet)
| haspet(n3,no_pet)
| haspet(n1,no_pet) ),
inference(resolve,[status(thm)],[c_2580,c_521]) ).
cnf(c_2615,plain,
( ~ haspet(n4,guppy)
| haspet(n5,camel)
| haspet(n3,camel)
| haspet(n1,camel) ),
inference(resolve,[status(thm)],[c_2581,c_525]) ).
cnf(c_2627,plain,
( hascolor(n1,green)
| hascolor(n1,red)
| hascolor(n3,white)
| hasperson(n5,italian)
| haspet(n4,guppy) ),
inference(resolve,[status(thm)],[c_2583,c_2244]) ).
cnf(c_2644,plain,
( ~ hasperson(n3,american)
| hasperson(n5,italian)
| haspet(n4,guppy) ),
inference(resolve,[status(thm)],[c_2583,c_1924]) ).
cnf(c_2667,plain,
~ hascolor(n1,red),
inference(resolve,[status(thm)],[c_2346,c_407]) ).
cnf(c_2668,plain,
~ hascolor(n1,green),
inference(resolve,[status(thm)],[c_2346,c_402]) ).
cnf(c_11803,plain,
( hascolor(n1,green)
| hascolor(n3,white)
| hasperson(n5,italian)
| haspet(n4,guppy) ),
inference(resolve,[status(thm)],[c_2667,c_2627]) ).
cnf(c_2677,plain,
( hascolor(n3,white)
| hasperson(n5,italian)
| haspet(n4,guppy) ),
inference(resolve,[status(thm)],[c_2668,c_11803]) ).
cnf(c_11804,plain,
( hascolor(n1,green)
| hascolor(n3,white)
| hasgame(n2,charades)
| hasperson(n5,american)
| hasgame(n4,charades) ),
inference(resolve,[status(thm)],[c_2667,c_2229]) ).
cnf(c_2678,plain,
( hascolor(n3,white)
| hasgame(n2,charades)
| hasperson(n5,american)
| hasgame(n4,charades) ),
inference(resolve,[status(thm)],[c_2668,c_11804]) ).
cnf(c_11805,plain,
( ~ hasperson(n3,american)
| hascolor(n1,green)
| hascolor(n3,white) ),
inference(resolve,[status(thm)],[c_2667,c_2136]) ).
cnf(c_2681,plain,
( ~ hasperson(n3,american)
| hascolor(n3,white) ),
inference(resolve,[status(thm)],[c_2668,c_11805]) ).
cnf(c_2695,plain,
( hascolor(n4,green)
| hasgame(n2,solitaire)
| hasgame(n4,solitaire) ),
inference(resolve,[status(thm)],[c_2668,c_2406]) ).
cnf(c_2699,plain,
( hasdrink(n2,coffee)
| hascolor(n5,green)
| hasperson(n5,swede) ),
inference(resolve,[status(thm)],[c_2668,c_2210]) ).
cnf(c_2727,plain,
( hascolor(n5,green)
| hasperson(n4,american)
| hasperson(n4,italian)
| hasperson(n4,englishman) ),
inference(resolve,[status(thm)],[c_2668,c_1505]) ).
cnf(c_2730,plain,
( ~ hasdrink(n5,vodka)
| hascolor(n4,green) ),
inference(resolve,[status(thm)],[c_2668,c_1427]) ).
cnf(c_2742,plain,
( hasdrink(n5,vodka)
| hasdrink(n2,vodka)
| hasdrink(n1,vodka)
| hascolor(n5,green) ),
inference(resolve,[status(thm)],[c_2668,c_1343]) ).
cnf(c_2777,plain,
( hasperson(n5,englishman)
| hascolor(n5,green) ),
inference(resolve,[status(thm)],[c_2542,c_143]) ).
cnf(c_2799,plain,
( ~ haspet(n5,V19)
| ~ haspet(n4,V18)
| ~ haspet(n3,V17)
| ~ haspet(n2,V16)
| ~ haspet(n1,V15)
| ~ hasgame(n5,V14)
| ~ hasgame(n4,V13)
| ~ hasgame(n3,V12)
| ~ hasgame(n2,V11)
| ~ hasdrink(n5,V10)
| ~ hasdrink(n4,V9)
| ~ hasdrink(n2,V8)
| ~ hasdrink(n1,V7)
| ~ hascolor(n5,V6)
| ~ hascolor(n4,F)
| ~ hascolor(n3,E)
| ~ hasperson(n5,D)
| ~ hasperson(n4,C)
| ~ hasperson(n3,B)
| ~ hasperson(n2,A) ),
inference(resolve,[status(thm)],[c_2331,c_2346]) ).
cnf(c_2876,plain,
( ~ haspet(n5,V18)
| ~ haspet(n4,V17)
| ~ haspet(n3,V16)
| ~ haspet(n1,V15)
| ~ hasgame(n5,V14)
| ~ hasgame(n4,V13)
| ~ hasgame(n3,V12)
| ~ hasgame(n2,V11)
| ~ hasdrink(n5,V10)
| ~ hasdrink(n4,V9)
| ~ hasdrink(n2,V8)
| ~ hasdrink(n1,V7)
| ~ hascolor(n5,V6)
| ~ hascolor(n4,F)
| ~ hascolor(n3,E)
| ~ hasperson(n5,D)
| ~ hasperson(n4,C)
| ~ hasperson(n3,B)
| ~ hasperson(n2,A) ),
inference(resolve,[status(thm)],[c_2799,c_2325]) ).
cnf(c_2897,plain,
( hasgame(n3,charades)
| hasgame(n2,charades)
| hasgame(n4,charades)
| ~ haspet(n5,V17)
| ~ haspet(n4,V16)
| ~ haspet(n3,V15)
| ~ haspet(n1,V14)
| ~ hasgame(n5,V13)
| ~ hasgame(n4,V12)
| ~ hasgame(n3,V11)
| ~ hasgame(n2,V10)
| ~ hasdrink(n5,V9)
| ~ hasdrink(n4,V8)
| ~ hasdrink(n2,V7)
| ~ hasdrink(n1,V6)
| ~ hascolor(n5,F)
| ~ hascolor(n4,E)
| ~ hascolor(n3,D)
| ~ hasperson(n4,C)
| ~ hasperson(n3,B)
| ~ hasperson(n2,A) ),
inference(resolve,[status(thm)],[c_2876,c_1914]) ).
cnf(c_2948,plain,
( ~ nextto(n5,A)
| ~ hasperson(A,englishman)
| hascolor(n5,green) ),
inference(resolve,[status(thm)],[c_2777,c_190]) ).
cnf(c_2949,plain,
( ~ hasperson(n5,american)
| hascolor(n5,green) ),
inference(resolve,[status(thm)],[c_2777,c_119]) ).
cnf(c_2950,plain,
( ~ hasperson(n5,swede)
| hascolor(n5,green) ),
inference(resolve,[status(thm)],[c_2777,c_117]) ).
cnf(c_2961,plain,
( ~ hasgame(n4,charades)
| hasgame(n5,solitaire)
| hasgame(n2,solitaire) ),
inference(resolve,[status(thm)],[c_2398,c_410]) ).
cnf(c_2965,plain,
( hasdrink(n4,vodka)
| hasgame(n5,solitaire)
| hasgame(n2,solitaire) ),
inference(resolve,[status(thm)],[c_2398,c_159]) ).
cnf(c_2969,plain,
( hascolor(n3,white)
| hasgame(n3,quoits)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_2476,c_2681]) ).
cnf(c_3000,plain,
( hasdrink(n5,lemonade)
| hasgame(n3,charades)
| haspet(n3,guppy) ),
inference(resolve,[status(thm)],[c_2541,c_150]) ).
cnf(c_3019,plain,
( hasgame(n3,quoits)
| hasgame(n3,backgammon)
| hasperson(n5,italian)
| haspet(n4,guppy) ),
inference(resolve,[status(thm)],[c_2644,c_2476]) ).
cnf(c_3035,plain,
( ~ hasperson(n5,american)
| hascolor(n3,white)
| haspet(n4,guppy) ),
inference(resolve,[status(thm)],[c_2677,c_122]) ).
cnf(c_3040,plain,
( hascolor(n5,red)
| hascolor(n3,red)
| hasgame(n2,solitaire)
| hasgame(n4,solitaire) ),
inference(resolve,[status(thm)],[c_2695,c_1548]) ).
cnf(c_3042,plain,
( hascolor(n3,white)
| hasgame(n2,solitaire)
| hasgame(n4,solitaire) ),
inference(resolve,[status(thm)],[c_2695,c_564]) ).
cnf(c_3050,plain,
( hasdrink(n4,lemonade)
| hasgame(n2,solitaire)
| hasgame(n4,solitaire) ),
inference(resolve,[status(thm)],[c_2695,c_150]) ).
cnf(c_3063,plain,
( ~ hasdrink(n2,vodka)
| hascolor(n5,green)
| hasperson(n5,swede) ),
inference(resolve,[status(thm)],[c_2699,c_111]) ).
cnf(c_3094,plain,
( hasdrink(n5,unknown_drink)
| hasdrink(n2,unknown_drink)
| hasdrink(n1,unknown_drink)
| hasgame(n5,solitaire)
| hasgame(n2,solitaire) ),
inference(resolve,[status(thm)],[c_2965,c_578]) ).
cnf(c_3100,plain,
( ~ hasdrink(n4,coffee)
| hasgame(n5,solitaire)
| hasgame(n2,solitaire) ),
inference(resolve,[status(thm)],[c_2965,c_111]) ).
cnf(c_3104,plain,
( hascolor(n4,green)
| hasgame(n3,quoits)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_2969,c_565]) ).
cnf(c_3105,plain,
( ~ hascolor(n3,red)
| hasgame(n3,quoits)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_2969,c_409]) ).
cnf(c_3132,plain,
( ~ hasdrink(n5,vodka)
| hasgame(n3,charades)
| haspet(n3,guppy) ),
inference(resolve,[status(thm)],[c_3000,c_108]) ).
cnf(c_3191,plain,
( ~ hascolor(n3,red)
| hasgame(n2,solitaire)
| hasgame(n4,solitaire) ),
inference(resolve,[status(thm)],[c_3042,c_409]) ).
cnf(c_3211,plain,
( ~ hasdrink(n4,coffee)
| hasgame(n2,solitaire)
| hasgame(n4,solitaire) ),
inference(resolve,[status(thm)],[c_3050,c_106]) ).
cnf(c_3232,plain,
( hascolor(n5,red)
| hascolor(n3,red)
| hasgame(n3,quoits)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_3104,c_1548]) ).
cnf(c_3239,plain,
( hasdrink(n4,lemonade)
| hasgame(n3,quoits)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_3104,c_150]) ).
cnf(c_3335,plain,
( ~ hasdrink(n4,vodka)
| hasgame(n3,quoits)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_3239,c_108]) ).
cnf(c_11806,plain,
( hasgame(n4,charades)
| hasgame(n4,quoits)
| hasgame(n4,racquetball)
| hasgame(n4,backgammon)
| hasgame(n3,quoits)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_3335,c_552]) ).
cnf(c_3367,plain,
( hasgame(n4,charades)
| hasgame(n4,quoits)
| hasgame(n4,backgammon)
| hasgame(n3,quoits)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_2341,c_11806]) ).
cnf(c_3391,plain,
( hasgame(n3,backgammon)
| haspet(n5,toad)
| haspet(n1,toad)
| hasgame(n4,backgammon) ),
inference(resolve,[status(thm)],[c_2328,c_153]) ).
cnf(c_3423,plain,
( hasdrink(n4,coffee)
| hasperson(n2,swede)
| hasgame(n2,solitaire)
| hasgame(n4,solitaire) ),
inference(resolve,[status(thm)],[c_2407,c_151]) ).
cnf(c_11807,plain,
( hascolor(n3,white)
| haspet(n4,guppy)
| hascolor(n3,white)
| hasgame(n2,charades)
| hasgame(n4,charades) ),
inference(resolve,[status(thm)],[c_2678,c_3035]) ).
cnf(c_3532,plain,
( haspet(n4,guppy)
| hascolor(n3,white)
| hasgame(n2,charades)
| hasgame(n4,charades) ),
inference(copy,[status(thm)],[c_11807]) ).
cnf(c_3540,plain,
( hasgame(n5,charades)
| hascolor(n3,white)
| hasgame(n2,charades)
| hasgame(n4,charades) ),
inference(resolve,[status(thm)],[c_2678,c_161]) ).
cnf(c_3594,plain,
( haspet(n4,guppy)
| hascolor(n5,green)
| hasperson(n4,american)
| hasperson(n4,englishman) ),
inference(resolve,[status(thm)],[c_2727,c_147]) ).
cnf(c_11808,plain,
( hascolor(n5,green)
| hasperson(n5,swede)
| hasdrink(n5,vodka)
| hasdrink(n1,vodka)
| hascolor(n5,green) ),
inference(resolve,[status(thm)],[c_2742,c_3063]) ).
cnf(c_3618,plain,
( hasperson(n5,swede)
| hasdrink(n5,vodka)
| hasdrink(n1,vodka)
| hascolor(n5,green) ),
inference(copy,[status(thm)],[c_11808]) ).
cnf(c_11809,plain,
( hasgame(n2,solitaire)
| hasgame(n4,solitaire)
| hascolor(n5,red)
| hasgame(n2,solitaire)
| hasgame(n4,solitaire) ),
inference(resolve,[status(thm)],[c_3040,c_3191]) ).
cnf(c_11810,plain,
( hasgame(n2,solitaire)
| hascolor(n5,red)
| hasgame(n2,solitaire)
| hasgame(n4,solitaire) ),
inference(copy,[status(thm)],[c_11809]) ).
cnf(c_3706,plain,
( hascolor(n5,red)
| hasgame(n2,solitaire)
| hasgame(n4,solitaire) ),
inference(copy,[status(thm)],[c_11810]) ).
cnf(c_3713,plain,
( hasperson(n5,englishman)
| hasgame(n2,solitaire)
| hasgame(n4,solitaire) ),
inference(resolve,[status(thm)],[c_3706,c_143]) ).
cnf(c_3726,plain,
( ~ hasperson(n5,american)
| hasgame(n2,solitaire)
| hasgame(n4,solitaire) ),
inference(resolve,[status(thm)],[c_3713,c_119]) ).
cnf(c_11811,plain,
( hasgame(n3,quoits)
| hasgame(n3,backgammon)
| hascolor(n5,red)
| hasgame(n3,quoits)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_3232,c_3105]) ).
cnf(c_11812,plain,
( hasgame(n3,quoits)
| hascolor(n5,red)
| hasgame(n3,quoits)
| hasgame(n3,backgammon) ),
inference(copy,[status(thm)],[c_11811]) ).
cnf(c_3891,plain,
( hascolor(n5,red)
| hasgame(n3,quoits)
| hasgame(n3,backgammon) ),
inference(copy,[status(thm)],[c_11812]) ).
cnf(c_3898,plain,
( hasperson(n5,englishman)
| hasgame(n3,quoits)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_3891,c_143]) ).
cnf(c_3910,plain,
( ~ hasperson(n5,italian)
| hasgame(n3,quoits)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_3898,c_116]) ).
cnf(c_11813,plain,
( hasgame(n3,quoits)
| hasgame(n3,backgammon)
| haspet(n4,guppy)
| hasgame(n3,quoits)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_3910,c_3019]) ).
cnf(c_11814,plain,
( hasgame(n3,quoits)
| haspet(n4,guppy)
| hasgame(n3,quoits)
| hasgame(n3,backgammon) ),
inference(copy,[status(thm)],[c_11813]) ).
cnf(c_3915,plain,
( haspet(n4,guppy)
| hasgame(n3,quoits)
| hasgame(n3,backgammon) ),
inference(copy,[status(thm)],[c_11814]) ).
cnf(c_3933,plain,
( ~ haspet(n4,toad)
| hasgame(n3,quoits)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_3915,c_96]) ).
cnf(c_11815,plain,
( hasgame(n1,backgammon)
| hasgame(n3,backgammon)
| haspet(n5,toad)
| hasgame(n4,backgammon) ),
inference(resolve,[status(thm)],[c_3391,c_153]) ).
cnf(c_4081,plain,
( hasgame(n3,backgammon)
| haspet(n5,toad)
| hasgame(n4,backgammon) ),
inference(resolve,[status(thm)],[c_2332,c_11815]) ).
cnf(c_4088,plain,
( hasgame(n5,backgammon)
| hasgame(n3,backgammon)
| hasgame(n4,backgammon) ),
inference(resolve,[status(thm)],[c_4081,c_153]) ).
cnf(c_4097,plain,
( ~ hasgame(n4,solitaire)
| hasgame(n5,backgammon)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_4088,c_417]) ).
cnf(c_4098,plain,
( ~ hasgame(n4,charades)
| hasgame(n5,backgammon)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_4088,c_416]) ).
cnf(c_4102,plain,
( haspet(n4,toad)
| hasgame(n5,backgammon)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_4088,c_154]) ).
cnf(c_4115,plain,
( ~ haspet(n4,guppy)
| hasgame(n5,backgammon)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_4102,c_96]) ).
cnf(c_11816,plain,
( hasgame(n2,solitaire)
| hasgame(n4,solitaire)
| hasperson(n2,swede)
| hasgame(n2,solitaire)
| hasgame(n4,solitaire) ),
inference(resolve,[status(thm)],[c_3423,c_3211]) ).
cnf(c_11817,plain,
( hasgame(n2,solitaire)
| hasperson(n2,swede)
| hasgame(n2,solitaire)
| hasgame(n4,solitaire) ),
inference(copy,[status(thm)],[c_11816]) ).
cnf(c_4138,plain,
( hasperson(n2,swede)
| hasgame(n2,solitaire)
| hasgame(n4,solitaire) ),
inference(copy,[status(thm)],[c_11817]) ).
cnf(c_4148,plain,
( ~ hasperson(n2,american)
| hasgame(n2,solitaire)
| hasgame(n4,solitaire) ),
inference(resolve,[status(thm)],[c_4138,c_124]) ).
cnf(c_11818,plain,
( ~ nextto(n5,n4)
| hascolor(n5,green)
| haspet(n4,guppy)
| hascolor(n5,green)
| hasperson(n4,american) ),
inference(resolve,[status(thm)],[c_3594,c_2948]) ).
cnf(c_11819,plain,
( ~ nextto(n5,n4)
| haspet(n4,guppy)
| hascolor(n5,green)
| hasperson(n4,american) ),
inference(copy,[status(thm)],[c_11818]) ).
cnf(c_4249,plain,
( haspet(n4,guppy)
| hascolor(n5,green)
| hasperson(n4,american) ),
inference(resolve,[status(thm)],[c_1096,c_11819]) ).
cnf(c_4259,plain,
( hasgame(n4,charades)
| haspet(n4,guppy)
| hascolor(n5,green) ),
inference(resolve,[status(thm)],[c_4249,c_161]) ).
cnf(c_4266,plain,
( hascolor(n4,white)
| hasgame(n4,charades)
| haspet(n4,guppy) ),
inference(resolve,[status(thm)],[c_4259,c_568]) ).
cnf(c_4299,plain,
( ~ hascolor(n3,white)
| hasgame(n4,charades)
| haspet(n4,guppy) ),
inference(resolve,[status(thm)],[c_4266,c_182]) ).
cnf(c_11820,plain,
( haspet(n4,guppy)
| hasgame(n2,charades)
| hasgame(n4,charades)
| hasgame(n4,charades)
| haspet(n4,guppy) ),
inference(resolve,[status(thm)],[c_4299,c_3532]) ).
cnf(c_11821,plain,
( haspet(n4,guppy)
| hasgame(n2,charades)
| hasgame(n4,charades)
| haspet(n4,guppy) ),
inference(copy,[status(thm)],[c_11820]) ).
cnf(c_4336,plain,
( hasgame(n2,charades)
| hasgame(n4,charades)
| haspet(n4,guppy) ),
inference(copy,[status(thm)],[c_11821]) ).
cnf(c_4345,plain,
( hasgame(n5,backgammon)
| hasgame(n3,backgammon)
| hasgame(n2,charades)
| hasgame(n4,charades) ),
inference(resolve,[status(thm)],[c_4336,c_4115]) ).
cnf(c_11822,plain,
( hasgame(n1,solitaire)
| hasperson(n5,swede)
| hasdrink(n5,vodka)
| hascolor(n5,green) ),
inference(resolve,[status(thm)],[c_3618,c_160]) ).
cnf(c_4471,plain,
( hasperson(n5,swede)
| hasdrink(n5,vodka)
| hascolor(n5,green) ),
inference(resolve,[status(thm)],[c_2334,c_11822]) ).
cnf(c_4480,plain,
( hasgame(n5,solitaire)
| hasperson(n5,swede)
| hascolor(n5,green) ),
inference(resolve,[status(thm)],[c_4471,c_160]) ).
cnf(c_11823,plain,
( hascolor(n5,green)
| hasgame(n5,solitaire)
| hascolor(n5,green) ),
inference(resolve,[status(thm)],[c_4480,c_2950]) ).
cnf(c_4484,plain,
( hasgame(n5,solitaire)
| hascolor(n5,green) ),
inference(copy,[status(thm)],[c_11823]) ).
cnf(c_4489,plain,
( hascolor(n4,white)
| hasgame(n5,solitaire) ),
inference(resolve,[status(thm)],[c_4484,c_568]) ).
cnf(c_4498,plain,
( hasdrink(n5,lemonade)
| hasgame(n5,solitaire) ),
inference(resolve,[status(thm)],[c_4484,c_150]) ).
cnf(c_4509,plain,
( ~ hascolor(n3,white)
| hasgame(n5,solitaire) ),
inference(resolve,[status(thm)],[c_4489,c_182]) ).
cnf(c_4515,plain,
( hasperson(n2,swede)
| hasperson(n4,swede)
| hasgame(n5,solitaire) ),
inference(resolve,[status(thm)],[c_4498,c_1864]) ).
cnf(c_4548,plain,
( hasgame(n5,charades)
| hasgame(n2,charades)
| hasgame(n4,charades)
| hasgame(n5,solitaire) ),
inference(resolve,[status(thm)],[c_4509,c_3540]) ).
cnf(c_4620,plain,
( hasdrink(n4,coffee)
| hasperson(n2,swede)
| hasgame(n5,solitaire) ),
inference(resolve,[status(thm)],[c_4515,c_151]) ).
cnf(c_4621,plain,
( ~ hasperson(n4,american)
| hasperson(n2,swede)
| hasgame(n5,solitaire) ),
inference(resolve,[status(thm)],[c_4515,c_124]) ).
cnf(c_11824,plain,
( hasgame(n5,solitaire)
| hasgame(n2,solitaire)
| hasperson(n2,swede)
| hasgame(n5,solitaire) ),
inference(resolve,[status(thm)],[c_4620,c_3100]) ).
cnf(c_4674,plain,
( hasgame(n2,solitaire)
| hasperson(n2,swede)
| hasgame(n5,solitaire) ),
inference(copy,[status(thm)],[c_11824]) ).
cnf(c_4702,plain,
( hasdrink(n2,coffee)
| hasgame(n2,solitaire)
| hasgame(n5,solitaire) ),
inference(resolve,[status(thm)],[c_4674,c_151]) ).
cnf(c_4703,plain,
( ~ hasperson(n2,american)
| hasgame(n2,solitaire)
| hasgame(n5,solitaire) ),
inference(resolve,[status(thm)],[c_4674,c_124]) ).
cnf(c_4728,plain,
( ~ hasdrink(n2,unknown_drink)
| hasgame(n2,solitaire)
| hasgame(n5,solitaire) ),
inference(resolve,[status(thm)],[c_4702,c_112]) ).
cnf(c_11825,plain,
( hasgame(n5,backgammon)
| hasgame(n3,backgammon)
| hasgame(n5,backgammon)
| hasgame(n3,backgammon)
| hasgame(n2,charades) ),
inference(resolve,[status(thm)],[c_4345,c_4098]) ).
cnf(c_11826,plain,
( hasgame(n5,backgammon)
| hasgame(n5,backgammon)
| hasgame(n3,backgammon)
| hasgame(n2,charades) ),
inference(copy,[status(thm)],[c_11825]) ).
cnf(c_5246,plain,
( hasgame(n5,backgammon)
| hasgame(n3,backgammon)
| hasgame(n2,charades) ),
inference(copy,[status(thm)],[c_11826]) ).
cnf(c_5249,plain,
( ~ hasgame(n2,solitaire)
| hasgame(n5,backgammon)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_5246,c_410]) ).
cnf(c_5256,plain,
( hasperson(n2,american)
| hasgame(n5,backgammon)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_5246,c_162]) ).
cnf(c_5271,plain,
( hasgame(n2,solitaire)
| hasgame(n4,solitaire)
| hasgame(n5,backgammon)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_5256,c_4148]) ).
cnf(c_11827,plain,
( hasgame(n5,solitaire)
| hasgame(n2,solitaire)
| hasgame(n5,charades)
| hasgame(n2,charades)
| hasgame(n5,solitaire) ),
inference(resolve,[status(thm)],[c_4548,c_2961]) ).
cnf(c_5453,plain,
( hasgame(n2,solitaire)
| hasgame(n5,charades)
| hasgame(n2,charades)
| hasgame(n5,solitaire) ),
inference(copy,[status(thm)],[c_11827]) ).
cnf(c_5462,plain,
( hasperson(n4,american)
| hasgame(n5,charades)
| hasgame(n2,charades)
| hasgame(n5,solitaire) ),
inference(resolve,[status(thm)],[c_4548,c_162]) ).
cnf(c_11828,plain,
( hasgame(n5,backgammon)
| hasgame(n3,backgammon)
| hasgame(n2,solitaire)
| hasgame(n5,backgammon)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_5271,c_4097]) ).
cnf(c_11829,plain,
( hasgame(n5,backgammon)
| hasgame(n2,solitaire)
| hasgame(n5,backgammon)
| hasgame(n3,backgammon) ),
inference(copy,[status(thm)],[c_11828]) ).
cnf(c_5753,plain,
( hasgame(n2,solitaire)
| hasgame(n5,backgammon)
| hasgame(n3,backgammon) ),
inference(copy,[status(thm)],[c_11829]) ).
cnf(c_11830,plain,
( hasgame(n5,backgammon)
| hasgame(n3,backgammon)
| hasgame(n5,backgammon)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_5753,c_5249]) ).
cnf(c_11831,plain,
( hasgame(n5,backgammon)
| hasgame(n5,backgammon)
| hasgame(n3,backgammon) ),
inference(copy,[status(thm)],[c_11830]) ).
cnf(c_5754,plain,
( hasgame(n5,backgammon)
| hasgame(n3,backgammon) ),
inference(copy,[status(thm)],[c_11831]) ).
cnf(c_5758,plain,
( ~ hasgame(n3,charades)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_5754,c_416]) ).
cnf(c_5763,plain,
( haspet(n3,toad)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_5754,c_154]) ).
cnf(c_5771,plain,
( ~ haspet(n3,no_pet)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_5763,c_102]) ).
cnf(c_5772,plain,
( ~ haspet(n3,camel)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_5763,c_100]) ).
cnf(c_5773,plain,
( ~ haspet(n3,guppy)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_5763,c_96]) ).
cnf(c_5988,plain,
( hasdrink(n2,vodka)
| hasgame(n5,charades)
| hasgame(n2,charades)
| hasgame(n5,solitaire) ),
inference(resolve,[status(thm)],[c_5453,c_159]) ).
cnf(c_11832,plain,
( hasperson(n2,swede)
| hasgame(n5,solitaire)
| hasgame(n5,charades)
| hasgame(n2,charades)
| hasgame(n5,solitaire) ),
inference(resolve,[status(thm)],[c_5462,c_4621]) ).
cnf(c_5989,plain,
( hasperson(n2,swede)
| hasgame(n5,charades)
| hasgame(n2,charades)
| hasgame(n5,solitaire) ),
inference(copy,[status(thm)],[c_11832]) ).
cnf(c_6319,plain,
( ~ hasdrink(n2,coffee)
| hasgame(n5,charades)
| hasgame(n2,charades)
| hasgame(n5,solitaire) ),
inference(resolve,[status(thm)],[c_5988,c_111]) ).
cnf(c_6325,plain,
( hasdrink(n2,coffee)
| hasgame(n5,charades)
| hasgame(n2,charades)
| hasgame(n5,solitaire) ),
inference(resolve,[status(thm)],[c_5989,c_151]) ).
cnf(c_11833,plain,
( hasgame(n5,charades)
| hasgame(n2,charades)
| hasgame(n5,solitaire)
| hasgame(n5,charades)
| hasgame(n2,charades)
| hasgame(n5,solitaire) ),
inference(resolve,[status(thm)],[c_6325,c_6319]) ).
cnf(c_11834,plain,
( hasgame(n5,charades)
| hasgame(n2,charades)
| hasgame(n5,charades)
| hasgame(n2,charades)
| hasgame(n5,solitaire) ),
inference(copy,[status(thm)],[c_11833]) ).
cnf(c_11835,plain,
( hasgame(n5,charades)
| hasgame(n5,charades)
| hasgame(n2,charades)
| hasgame(n5,solitaire) ),
inference(copy,[status(thm)],[c_11834]) ).
cnf(c_6556,plain,
( hasgame(n5,charades)
| hasgame(n2,charades)
| hasgame(n5,solitaire) ),
inference(copy,[status(thm)],[c_11835]) ).
cnf(c_6560,plain,
( ~ hasgame(n2,solitaire)
| hasgame(n5,charades)
| hasgame(n5,solitaire) ),
inference(resolve,[status(thm)],[c_6556,c_410]) ).
cnf(c_6565,plain,
( hasperson(n2,american)
| hasgame(n5,charades)
| hasgame(n5,solitaire) ),
inference(resolve,[status(thm)],[c_6556,c_162]) ).
cnf(c_11836,plain,
( hasgame(n2,solitaire)
| hasgame(n5,solitaire)
| hasgame(n5,charades)
| hasgame(n5,solitaire) ),
inference(resolve,[status(thm)],[c_6565,c_4703]) ).
cnf(c_6567,plain,
( hasgame(n2,solitaire)
| hasgame(n5,charades)
| hasgame(n5,solitaire) ),
inference(copy,[status(thm)],[c_11836]) ).
cnf(c_11837,plain,
( hasgame(n5,charades)
| hasgame(n5,solitaire)
| hasgame(n5,charades)
| hasgame(n5,solitaire) ),
inference(resolve,[status(thm)],[c_6567,c_6560]) ).
cnf(c_11838,plain,
( hasgame(n5,charades)
| hasgame(n5,charades)
| hasgame(n5,solitaire) ),
inference(copy,[status(thm)],[c_11837]) ).
cnf(c_6582,plain,
( hasgame(n5,charades)
| hasgame(n5,solitaire) ),
inference(copy,[status(thm)],[c_11838]) ).
cnf(c_6587,plain,
( hasgame(n2,charades)
| hasgame(n2,quoits)
| hasgame(n2,backgammon)
| hasgame(n5,charades) ),
inference(resolve,[status(thm)],[c_6582,c_2456]) ).
cnf(c_6603,plain,
( hasdrink(n5,vodka)
| hasgame(n5,charades) ),
inference(resolve,[status(thm)],[c_6582,c_159]) ).
cnf(c_6609,plain,
( hasgame(n3,charades)
| haspet(n3,guppy)
| hasgame(n5,charades) ),
inference(resolve,[status(thm)],[c_6603,c_3132]) ).
cnf(c_6611,plain,
( hascolor(n4,green)
| hasgame(n5,charades) ),
inference(resolve,[status(thm)],[c_6603,c_2730]) ).
cnf(c_6612,plain,
( hasperson(n2,swede)
| hasperson(n4,swede)
| hasgame(n5,charades) ),
inference(resolve,[status(thm)],[c_6603,c_1863]) ).
cnf(c_6636,plain,
( hasdrink(n4,lemonade)
| hasgame(n5,charades) ),
inference(resolve,[status(thm)],[c_6611,c_150]) ).
cnf(c_6660,plain,
( ~ hasdrink(n4,coffee)
| hasgame(n5,charades) ),
inference(resolve,[status(thm)],[c_6636,c_106]) ).
cnf(c_6717,plain,
( hasgame(n5,backgammon)
| hasgame(n3,charades)
| hasgame(n5,charades) ),
inference(resolve,[status(thm)],[c_6609,c_5773]) ).
cnf(c_6732,plain,
( ~ haspet(n3,toad)
| hasgame(n3,charades)
| hasgame(n5,charades) ),
inference(resolve,[status(thm)],[c_6609,c_96]) ).
cnf(c_6750,plain,
( hasdrink(n4,coffee)
| hasperson(n2,swede)
| hasgame(n5,charades) ),
inference(resolve,[status(thm)],[c_6612,c_151]) ).
cnf(c_11839,plain,
( hasgame(n5,backgammon)
| hasgame(n5,backgammon)
| hasgame(n5,charades) ),
inference(resolve,[status(thm)],[c_6717,c_5758]) ).
cnf(c_6835,plain,
( hasgame(n5,backgammon)
| hasgame(n5,charades) ),
inference(copy,[status(thm)],[c_11839]) ).
cnf(c_6846,plain,
( hasperson(n5,american)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_6835,c_162]) ).
cnf(c_6856,plain,
( hasgame(n2,solitaire)
| hasgame(n4,solitaire)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_6846,c_3726]) ).
cnf(c_6859,plain,
( hascolor(n3,white)
| haspet(n4,guppy)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_6846,c_3035]) ).
cnf(c_6860,plain,
( hascolor(n5,green)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_6846,c_2949]) ).
cnf(c_6865,plain,
( hascolor(n3,red)
| hascolor(n4,red)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_6846,c_1500]) ).
cnf(c_6879,plain,
( hascolor(n4,white)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_6860,c_568]) ).
cnf(c_6888,plain,
( hasdrink(n5,lemonade)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_6860,c_150]) ).
cnf(c_6893,plain,
( ~ hascolor(n4,red)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_6879,c_409]) ).
cnf(c_6894,plain,
( ~ hascolor(n3,white)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_6879,c_182]) ).
cnf(c_6900,plain,
( hasperson(n2,swede)
| hasperson(n4,swede)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_6888,c_1864]) ).
cnf(c_6910,plain,
( ~ hasdrink(n5,unknown_drink)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_6888,c_109]) ).
cnf(c_6911,plain,
( ~ hasdrink(n5,vodka)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_6888,c_108]) ).
cnf(c_11840,plain,
( hasgame(n5,charades)
| hasperson(n2,swede)
| hasgame(n5,charades) ),
inference(resolve,[status(thm)],[c_6750,c_6660]) ).
cnf(c_6923,plain,
( hasperson(n2,swede)
| hasgame(n5,charades) ),
inference(copy,[status(thm)],[c_11840]) ).
cnf(c_6933,plain,
( ~ hasperson(n2,american)
| hasgame(n5,charades) ),
inference(resolve,[status(thm)],[c_6923,c_124]) ).
cnf(c_6979,plain,
( ~ hasgame(n4,quoits)
| hasgame(n2,solitaire)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_6856,c_412]) ).
cnf(c_11841,plain,
( hasgame(n5,backgammon)
| haspet(n4,guppy)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_6859,c_6894]) ).
cnf(c_6983,plain,
( haspet(n4,guppy)
| hasgame(n5,backgammon) ),
inference(copy,[status(thm)],[c_11841]) ).
cnf(c_6985,plain,
( haspet(n5,camel)
| haspet(n3,camel)
| haspet(n1,camel)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_6983,c_2615]) ).
cnf(c_6986,plain,
( haspet(n5,no_pet)
| haspet(n3,no_pet)
| haspet(n1,no_pet)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_6983,c_2588]) ).
cnf(c_6995,plain,
( hasperson(n4,italian)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_6983,c_148]) ).
cnf(c_7027,plain,
( ~ hasperson(n4,swede)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_6995,c_120]) ).
cnf(c_11842,plain,
( hasgame(n5,backgammon)
| hascolor(n3,red)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_6865,c_6893]) ).
cnf(c_7035,plain,
( hascolor(n3,red)
| hasgame(n5,backgammon) ),
inference(copy,[status(thm)],[c_11842]) ).
cnf(c_7041,plain,
( hasperson(n3,englishman)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_7035,c_143]) ).
cnf(c_11843,plain,
( hasgame(n5,backgammon)
| hasperson(n2,swede)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_6900,c_7027]) ).
cnf(c_7047,plain,
( hasperson(n2,swede)
| hasgame(n5,backgammon) ),
inference(copy,[status(thm)],[c_11843]) ).
cnf(c_7053,plain,
( hasdrink(n2,coffee)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_7047,c_151]) ).
cnf(c_7056,plain,
( hasdrink(n5,vodka)
| hasdrink(n1,vodka)
| hasgame(n4,solitaire)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_7053,c_1385]) ).
cnf(c_7065,plain,
( ~ hasdrink(n2,vodka)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_7053,c_111]) ).
cnf(c_7124,plain,
( hasperson(n2,american)
| hasgame(n2,quoits)
| hasgame(n2,backgammon)
| hasgame(n5,charades) ),
inference(resolve,[status(thm)],[c_6587,c_162]) ).
cnf(c_11844,plain,
( hasgame(n5,backgammon)
| haspet(n5,camel)
| haspet(n1,camel)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_6985,c_5772]) ).
cnf(c_7183,plain,
( haspet(n5,camel)
| haspet(n1,camel)
| hasgame(n5,backgammon) ),
inference(copy,[status(thm)],[c_11844]) ).
cnf(c_7186,plain,
( hasgame(n2,quoits)
| haspet(n5,camel)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_7183,c_979]) ).
cnf(c_7203,plain,
( hasgame(n4,quoits)
| hasgame(n2,quoits)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_7186,c_1206]) ).
cnf(c_11845,plain,
( hasgame(n2,solitaire)
| hasgame(n5,backgammon)
| hasgame(n2,quoits)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_7203,c_6979]) ).
cnf(c_7231,plain,
( hasgame(n2,solitaire)
| hasgame(n2,quoits)
| hasgame(n5,backgammon) ),
inference(copy,[status(thm)],[c_11845]) ).
cnf(c_7250,plain,
( hasdrink(n2,vodka)
| hasgame(n2,quoits)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_7231,c_159]) ).
cnf(c_11846,plain,
( hasgame(n5,backgammon)
| hasgame(n2,quoits)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_7250,c_7065]) ).
cnf(c_7251,plain,
( hasgame(n2,quoits)
| hasgame(n5,backgammon) ),
inference(copy,[status(thm)],[c_11846]) ).
cnf(c_7257,plain,
( haspet(n3,camel)
| haspet(n1,camel)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_7251,c_1007]) ).
cnf(c_7258,plain,
( ~ hasgame(n2,solitaire)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_7251,c_412]) ).
cnf(c_11847,plain,
( hasgame(n5,backgammon)
| haspet(n1,camel)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_7257,c_5772]) ).
cnf(c_7264,plain,
( haspet(n1,camel)
| hasgame(n5,backgammon) ),
inference(copy,[status(thm)],[c_11847]) ).
cnf(c_7274,plain,
( ~ haspet(n1,no_pet)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_7264,c_104]) ).
cnf(c_11848,plain,
( hasgame(n5,backgammon)
| haspet(n5,no_pet)
| haspet(n1,no_pet)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_6986,c_5771]) ).
cnf(c_7275,plain,
( haspet(n5,no_pet)
| haspet(n1,no_pet)
| hasgame(n5,backgammon) ),
inference(copy,[status(thm)],[c_11848]) ).
cnf(c_11849,plain,
( hasgame(n5,backgammon)
| haspet(n5,no_pet)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_7275,c_7274]) ).
cnf(c_7276,plain,
( haspet(n5,no_pet)
| hasgame(n5,backgammon) ),
inference(copy,[status(thm)],[c_11849]) ).
cnf(c_11850,plain,
( hasgame(n1,solitaire)
| hasdrink(n5,vodka)
| hasgame(n4,solitaire)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_7056,c_160]) ).
cnf(c_7296,plain,
( hasdrink(n5,vodka)
| hasgame(n4,solitaire)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_2334,c_11850]) ).
cnf(c_11851,plain,
( hasgame(n5,backgammon)
| hasgame(n4,solitaire)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_7296,c_6911]) ).
cnf(c_7297,plain,
( hasgame(n4,solitaire)
| hasgame(n5,backgammon) ),
inference(copy,[status(thm)],[c_11851]) ).
cnf(c_7303,plain,
( hasdrink(n4,vodka)
| hasgame(n5,backgammon) ),
inference(resolve,[status(thm)],[c_7297,c_159]) ).
cnf(c_11852,plain,
( hasgame(n5,charades)
| hasgame(n2,quoits)
| hasgame(n2,backgammon)
| hasgame(n5,charades) ),
inference(resolve,[status(thm)],[c_7124,c_6933]) ).
cnf(c_7337,plain,
( hasgame(n2,quoits)
| hasgame(n2,backgammon)
| hasgame(n5,charades) ),
inference(copy,[status(thm)],[c_11852]) ).
cnf(c_11853,plain,
( haspet(n2,toad)
| hasgame(n2,quoits)
| hasgame(n5,charades) ),
inference(resolve,[status(thm)],[c_7337,c_154]) ).
cnf(c_7344,plain,
( hasgame(n2,quoits)
| hasgame(n5,charades) ),
inference(resolve,[status(thm)],[c_2582,c_11853]) ).
cnf(c_7356,plain,
( ~ hasgame(n4,quoits)
| hasgame(n5,charades) ),
inference(resolve,[status(thm)],[c_7344,c_217]) ).
cnf(c_7358,plain,
( ~ nextto(n2,A)
| ~ hasgame(A,quoits)
| hasgame(n5,charades) ),
inference(resolve,[status(thm)],[c_7344,c_212]) ).
cnf(c_11854,plain,
( hasgame(n2,solitaire)
| hasgame(n5,solitaire)
| hasdrink(n5,unknown_drink)
| hasdrink(n1,unknown_drink)
| hasgame(n5,solitaire)
| hasgame(n2,solitaire) ),
inference(resolve,[status(thm)],[c_3094,c_4728]) ).
cnf(c_11855,plain,
( hasgame(n2,solitaire)
| hasdrink(n5,unknown_drink)
| hasdrink(n1,unknown_drink)
| hasgame(n5,solitaire)
| hasgame(n2,solitaire) ),
inference(copy,[status(thm)],[c_11854]) ).
cnf(c_8180,plain,
( hasdrink(n5,unknown_drink)
| hasdrink(n1,unknown_drink)
| hasgame(n5,solitaire)
| hasgame(n2,solitaire) ),
inference(copy,[status(thm)],[c_11855]) ).
cnf(c_9909,plain,
( hasgame(n5,backgammon)
| hasgame(n3,charades)
| hasgame(n2,charades)
| hasgame(n4,charades)
| ~ haspet(n4,V16)
| ~ haspet(n3,V15)
| ~ haspet(n1,V14)
| ~ hasgame(n5,V13)
| ~ hasgame(n4,V12)
| ~ hasgame(n3,V11)
| ~ hasgame(n2,V10)
| ~ hasdrink(n5,V9)
| ~ hasdrink(n4,V8)
| ~ hasdrink(n2,V7)
| ~ hasdrink(n1,V6)
| ~ hascolor(n5,F)
| ~ hascolor(n4,E)
| ~ hascolor(n3,D)
| ~ hasperson(n4,C)
| ~ hasperson(n3,B)
| ~ hasperson(n2,A) ),
inference(resolve,[status(thm)],[c_2897,c_7276]) ).
cnf(c_11856,plain,
( hasgame(n3,quoits)
| hasgame(n3,backgammon)
| hasgame(n4,quoits)
| hasgame(n4,backgammon)
| hasgame(n3,quoits)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_3367,c_2480]) ).
cnf(c_11857,plain,
( hasgame(n3,quoits)
| hasgame(n4,quoits)
| hasgame(n4,backgammon)
| hasgame(n3,quoits)
| hasgame(n3,backgammon) ),
inference(copy,[status(thm)],[c_11856]) ).
cnf(c_10360,plain,
( hasgame(n4,quoits)
| hasgame(n4,backgammon)
| hasgame(n3,quoits)
| hasgame(n3,backgammon) ),
inference(copy,[status(thm)],[c_11857]) ).
cnf(c_10371,plain,
( haspet(n4,toad)
| hasgame(n4,quoits)
| hasgame(n3,quoits)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_10360,c_154]) ).
cnf(c_11858,plain,
( hasgame(n3,quoits)
| hasgame(n3,backgammon)
| hasgame(n4,quoits)
| hasgame(n3,quoits)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_10371,c_3933]) ).
cnf(c_11859,plain,
( hasgame(n3,quoits)
| hasgame(n4,quoits)
| hasgame(n3,quoits)
| hasgame(n3,backgammon) ),
inference(copy,[status(thm)],[c_11858]) ).
cnf(c_10410,plain,
( hasgame(n4,quoits)
| hasgame(n3,quoits)
| hasgame(n3,backgammon) ),
inference(copy,[status(thm)],[c_11859]) ).
cnf(c_10412,plain,
( hasgame(n5,charades)
| hasgame(n3,quoits)
| hasgame(n3,backgammon) ),
inference(resolve,[status(thm)],[c_10410,c_7356]) ).
cnf(c_10445,plain,
( ~ hasgame(n3,charades)
| hasgame(n5,charades)
| hasgame(n3,quoits) ),
inference(resolve,[status(thm)],[c_10412,c_416]) ).
cnf(c_10449,plain,
( haspet(n3,toad)
| hasgame(n5,charades)
| hasgame(n3,quoits) ),
inference(resolve,[status(thm)],[c_10412,c_154]) ).
cnf(c_11860,plain,
( hasgame(n3,charades)
| hasgame(n5,charades)
| hasgame(n5,charades)
| hasgame(n3,quoits) ),
inference(resolve,[status(thm)],[c_10449,c_6732]) ).
cnf(c_10740,plain,
( hasgame(n3,charades)
| hasgame(n5,charades)
| hasgame(n3,quoits) ),
inference(copy,[status(thm)],[c_11860]) ).
cnf(c_11861,plain,
( hasgame(n5,charades)
| hasgame(n3,quoits)
| hasgame(n5,charades)
| hasgame(n3,quoits) ),
inference(resolve,[status(thm)],[c_10740,c_10445]) ).
cnf(c_11862,plain,
( hasgame(n5,charades)
| hasgame(n5,charades)
| hasgame(n3,quoits) ),
inference(copy,[status(thm)],[c_11861]) ).
cnf(c_11084,plain,
( hasgame(n5,charades)
| hasgame(n3,quoits) ),
inference(copy,[status(thm)],[c_11862]) ).
cnf(c_11863,plain,
( ~ nextto(n2,n3)
| hasgame(n5,charades)
| hasgame(n5,charades) ),
inference(resolve,[status(thm)],[c_11084,c_7358]) ).
cnf(c_11864,plain,
( ~ nextto(n2,n3)
| hasgame(n5,charades) ),
inference(copy,[status(thm)],[c_11863]) ).
cnf(c_11087,plain,
hasgame(n5,charades),
inference(resolve,[status(thm)],[c_562,c_11864]) ).
cnf(c_11100,plain,
~ hasgame(n5,backgammon),
inference(resolve,[status(thm)],[c_11087,c_416]) ).
cnf(c_11102,plain,
~ hasgame(n5,solitaire),
inference(resolve,[status(thm)],[c_11087,c_410]) ).
cnf(c_11106,plain,
~ hasgame(n2,charades),
inference(resolve,[status(thm)],[c_11087,c_216]) ).
cnf(c_11107,plain,
~ hasgame(n3,charades),
inference(resolve,[status(thm)],[c_11087,c_214]) ).
cnf(c_11108,plain,
~ hasgame(n4,charades),
inference(resolve,[status(thm)],[c_11087,c_213]) ).
cnf(c_11865,plain,
( hasgame(n5,backgammon)
| hasgame(n3,charades)
| hasgame(n2,charades)
| ~ haspet(n4,V16)
| ~ haspet(n3,V15)
| ~ haspet(n1,V14)
| ~ hasgame(n5,V13)
| ~ hasgame(n4,V12)
| ~ hasgame(n3,V11)
| ~ hasgame(n2,V10)
| ~ hasdrink(n5,V9)
| ~ hasdrink(n4,V8)
| ~ hasdrink(n2,V7)
| ~ hasdrink(n1,V6)
| ~ hascolor(n5,F)
| ~ hascolor(n4,E)
| ~ hascolor(n3,D)
| ~ hasperson(n4,C)
| ~ hasperson(n3,B)
| ~ hasperson(n2,A) ),
inference(resolve,[status(thm)],[c_11108,c_9909]) ).
cnf(c_11866,plain,
( hasgame(n5,backgammon)
| hasgame(n3,charades)
| ~ haspet(n4,V16)
| ~ haspet(n3,V15)
| ~ haspet(n1,V14)
| ~ hasgame(n5,V13)
| ~ hasgame(n4,V12)
| ~ hasgame(n3,V11)
| ~ hasgame(n2,V10)
| ~ hasdrink(n5,V9)
| ~ hasdrink(n4,V8)
| ~ hasdrink(n2,V7)
| ~ hasdrink(n1,V6)
| ~ hascolor(n5,F)
| ~ hascolor(n4,E)
| ~ hascolor(n3,D)
| ~ hasperson(n4,C)
| ~ hasperson(n3,B)
| ~ hasperson(n2,A) ),
inference(resolve,[status(thm)],[c_11106,c_11865]) ).
cnf(c_11867,plain,
( hasgame(n5,backgammon)
| ~ haspet(n4,V16)
| ~ haspet(n3,V15)
| ~ haspet(n1,V14)
| ~ hasgame(n5,V13)
| ~ hasgame(n4,V12)
| ~ hasgame(n3,V11)
| ~ hasgame(n2,V10)
| ~ hasdrink(n5,V9)
| ~ hasdrink(n4,V8)
| ~ hasdrink(n2,V7)
| ~ hasdrink(n1,V6)
| ~ hascolor(n5,F)
| ~ hascolor(n4,E)
| ~ hascolor(n3,D)
| ~ hasperson(n4,C)
| ~ hasperson(n3,B)
| ~ hasperson(n2,A) ),
inference(resolve,[status(thm)],[c_11107,c_11866]) ).
cnf(c_11146,plain,
( ~ haspet(n4,V16)
| ~ haspet(n3,V15)
| ~ haspet(n1,V14)
| ~ hasgame(n5,V13)
| ~ hasgame(n4,V12)
| ~ hasgame(n3,V11)
| ~ hasgame(n2,V10)
| ~ hasdrink(n5,V9)
| ~ hasdrink(n4,V8)
| ~ hasdrink(n2,V7)
| ~ hasdrink(n1,V6)
| ~ hascolor(n5,F)
| ~ hascolor(n4,E)
| ~ hascolor(n3,D)
| ~ hasperson(n4,C)
| ~ hasperson(n3,B)
| ~ hasperson(n2,A) ),
inference(resolve,[status(thm)],[c_11100,c_11867]) ).
cnf(c_11270,plain,
hasdrink(n4,vodka),
inference(resolve,[status(thm)],[c_11100,c_7303]) ).
cnf(c_11275,plain,
hasgame(n4,solitaire),
inference(resolve,[status(thm)],[c_11100,c_7297]) ).
cnf(c_11294,plain,
haspet(n1,camel),
inference(resolve,[status(thm)],[c_11100,c_7264]) ).
cnf(c_11300,plain,
~ hasgame(n2,solitaire),
inference(resolve,[status(thm)],[c_11100,c_7258]) ).
cnf(c_11303,plain,
hasgame(n2,quoits),
inference(resolve,[status(thm)],[c_11100,c_7251]) ).
cnf(c_11310,plain,
hasdrink(n2,coffee),
inference(resolve,[status(thm)],[c_11100,c_7053]) ).
cnf(c_11315,plain,
hasperson(n2,swede),
inference(resolve,[status(thm)],[c_11100,c_7047]) ).
cnf(c_11321,plain,
hasperson(n3,englishman),
inference(resolve,[status(thm)],[c_11100,c_7041]) ).
cnf(c_11327,plain,
hascolor(n3,red),
inference(resolve,[status(thm)],[c_11100,c_7035]) ).
cnf(c_11337,plain,
hasperson(n4,italian),
inference(resolve,[status(thm)],[c_11100,c_6995]) ).
cnf(c_11343,plain,
haspet(n4,guppy),
inference(resolve,[status(thm)],[c_11100,c_6983]) ).
cnf(c_11346,plain,
~ hasdrink(n5,unknown_drink),
inference(resolve,[status(thm)],[c_11100,c_6910]) ).
cnf(c_11365,plain,
hasdrink(n5,lemonade),
inference(resolve,[status(thm)],[c_11100,c_6888]) ).
cnf(c_11373,plain,
hascolor(n4,white),
inference(resolve,[status(thm)],[c_11100,c_6879]) ).
cnf(c_11386,plain,
hascolor(n5,green),
inference(resolve,[status(thm)],[c_11100,c_6860]) ).
cnf(c_11394,plain,
haspet(n3,toad),
inference(resolve,[status(thm)],[c_11100,c_5763]) ).
cnf(c_11401,plain,
hasgame(n3,backgammon),
inference(resolve,[status(thm)],[c_11100,c_5754]) ).
cnf(c_11868,plain,
( hasdrink(n5,unknown_drink)
| hasdrink(n1,unknown_drink)
| hasgame(n5,solitaire) ),
inference(resolve,[status(thm)],[c_11300,c_8180]) ).
cnf(c_11869,plain,
( hasdrink(n5,unknown_drink)
| hasdrink(n1,unknown_drink) ),
inference(resolve,[status(thm)],[c_11102,c_11868]) ).
cnf(c_11442,plain,
hasdrink(n1,unknown_drink),
inference(resolve,[status(thm)],[c_11346,c_11869]) ).
cnf(c_11521,plain,
( ~ haspet(n4,V15)
| ~ haspet(n3,V14)
| ~ haspet(n1,V13)
| ~ hasgame(n5,V12)
| ~ hasgame(n4,V11)
| ~ hasgame(n3,V10)
| ~ hasgame(n2,V9)
| ~ hasdrink(n5,V8)
| ~ hasdrink(n4,V7)
| ~ hasdrink(n2,V6)
| ~ hasdrink(n1,F)
| ~ hascolor(n5,E)
| ~ hascolor(n4,D)
| ~ hascolor(n3,C)
| ~ hasperson(n4,B)
| ~ hasperson(n3,A) ),
inference(resolve,[status(thm)],[c_11146,c_11315]) ).
cnf(c_11587,plain,
( ~ haspet(n4,V14)
| ~ haspet(n3,V13)
| ~ haspet(n1,V12)
| ~ hasgame(n5,V11)
| ~ hasgame(n4,V10)
| ~ hasgame(n3,V9)
| ~ hasgame(n2,V8)
| ~ hasdrink(n5,V7)
| ~ hasdrink(n4,V6)
| ~ hasdrink(n2,F)
| ~ hasdrink(n1,E)
| ~ hascolor(n5,D)
| ~ hascolor(n4,C)
| ~ hascolor(n3,B)
| ~ hasperson(n4,A) ),
inference(resolve,[status(thm)],[c_11521,c_11321]) ).
cnf(c_11603,plain,
( ~ haspet(n4,V13)
| ~ haspet(n3,V12)
| ~ haspet(n1,V11)
| ~ hasgame(n5,V10)
| ~ hasgame(n4,V9)
| ~ hasgame(n3,V8)
| ~ hasgame(n2,V7)
| ~ hasdrink(n5,V6)
| ~ hasdrink(n4,F)
| ~ hasdrink(n2,E)
| ~ hasdrink(n1,D)
| ~ hascolor(n5,C)
| ~ hascolor(n4,B)
| ~ hascolor(n3,A) ),
inference(resolve,[status(thm)],[c_11587,c_11337]) ).
cnf(c_11618,plain,
( ~ haspet(n4,V12)
| ~ haspet(n3,V11)
| ~ haspet(n1,V10)
| ~ hasgame(n5,V9)
| ~ hasgame(n4,V8)
| ~ hasgame(n3,V7)
| ~ hasgame(n2,V6)
| ~ hasdrink(n5,F)
| ~ hasdrink(n4,E)
| ~ hasdrink(n2,D)
| ~ hasdrink(n1,C)
| ~ hascolor(n5,B)
| ~ hascolor(n4,A) ),
inference(resolve,[status(thm)],[c_11603,c_11327]) ).
cnf(c_11632,plain,
( ~ haspet(n4,V11)
| ~ haspet(n3,V10)
| ~ haspet(n1,V9)
| ~ hasgame(n5,V8)
| ~ hasgame(n4,V7)
| ~ hasgame(n3,V6)
| ~ hasgame(n2,F)
| ~ hasdrink(n5,E)
| ~ hasdrink(n4,D)
| ~ hasdrink(n2,C)
| ~ hasdrink(n1,B)
| ~ hascolor(n5,A) ),
inference(resolve,[status(thm)],[c_11618,c_11373]) ).
cnf(c_11664,plain,
( ~ haspet(n4,V10)
| ~ haspet(n3,V9)
| ~ haspet(n1,V8)
| ~ hasgame(n5,V7)
| ~ hasgame(n4,V6)
| ~ hasgame(n3,F)
| ~ hasgame(n2,E)
| ~ hasdrink(n5,D)
| ~ hasdrink(n4,C)
| ~ hasdrink(n2,B)
| ~ hasdrink(n1,A) ),
inference(resolve,[status(thm)],[c_11632,c_11386]) ).
cnf(c_11676,plain,
( ~ haspet(n4,V9)
| ~ haspet(n3,V8)
| ~ haspet(n1,V7)
| ~ hasgame(n5,V6)
| ~ hasgame(n4,F)
| ~ hasgame(n3,E)
| ~ hasgame(n2,D)
| ~ hasdrink(n5,C)
| ~ hasdrink(n4,B)
| ~ hasdrink(n2,A) ),
inference(resolve,[status(thm)],[c_11664,c_11442]) ).
cnf(c_11687,plain,
( ~ haspet(n4,V8)
| ~ haspet(n3,V7)
| ~ haspet(n1,V6)
| ~ hasgame(n5,F)
| ~ hasgame(n4,E)
| ~ hasgame(n3,D)
| ~ hasgame(n2,C)
| ~ hasdrink(n5,B)
| ~ hasdrink(n4,A) ),
inference(resolve,[status(thm)],[c_11676,c_11310]) ).
cnf(c_11697,plain,
( ~ haspet(n4,V7)
| ~ haspet(n3,V6)
| ~ haspet(n1,F)
| ~ hasgame(n5,E)
| ~ hasgame(n4,D)
| ~ hasgame(n3,C)
| ~ hasgame(n2,B)
| ~ hasdrink(n5,A) ),
inference(resolve,[status(thm)],[c_11687,c_11270]) ).
cnf(c_11709,plain,
( ~ haspet(n4,V6)
| ~ haspet(n3,F)
| ~ haspet(n1,E)
| ~ hasgame(n5,D)
| ~ hasgame(n4,C)
| ~ hasgame(n3,B)
| ~ hasgame(n2,A) ),
inference(resolve,[status(thm)],[c_11697,c_11365]) ).
cnf(c_11717,plain,
( ~ haspet(n4,F)
| ~ haspet(n3,E)
| ~ haspet(n1,D)
| ~ hasgame(n5,C)
| ~ hasgame(n4,B)
| ~ hasgame(n3,A) ),
inference(resolve,[status(thm)],[c_11709,c_11303]) ).
cnf(c_11724,plain,
( ~ haspet(n4,E)
| ~ haspet(n3,D)
| ~ haspet(n1,C)
| ~ hasgame(n5,B)
| ~ hasgame(n4,A) ),
inference(resolve,[status(thm)],[c_11717,c_11401]) ).
cnf(c_11730,plain,
( ~ haspet(n4,D)
| ~ haspet(n3,C)
| ~ haspet(n1,B)
| ~ hasgame(n5,A) ),
inference(resolve,[status(thm)],[c_11724,c_11275]) ).
cnf(c_11735,plain,
( ~ haspet(n4,C)
| ~ haspet(n3,B)
| ~ haspet(n1,A) ),
inference(resolve,[status(thm)],[c_11730,c_11087]) ).
cnf(c_11739,plain,
( ~ haspet(n4,B)
| ~ haspet(n3,A) ),
inference(resolve,[status(thm)],[c_11735,c_11294]) ).
cnf(c_11758,plain,
~ haspet(n4,A),
inference(resolve,[status(thm)],[c_11739,c_11394]) ).
cnf(c_11759,plain,
$false,
inference(resolve,[status(thm)],[c_11758,c_11343]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ017-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.36 % Computer : n009.cluster.edu
% 0.10/0.36 % Model : x86_64 x86_64
% 0.10/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.36 % Memory : 8046.5625MB
% 0.10/0.36 % OS : Linux 6.8.0-71-generic
% 0.10/0.36 % CPULimit : 300
% 0.10/0.36 % WCLimit : 300
% 0.10/0.36 % DateTime : Sat Sep 26 05:04:44 UTC 2026
% 0.10/0.36 % CPUTime :
% 0.10/0.36 % Prover9 (64) version 2026-6A, July 2026, CASC-J13.
% 0.10/0.36 % Process 3402664 was started by sandbox on n009,
% 0.10/0.36 % Sat Sep 26 05:04:44 2026
% 0.10/0.36 % The command was "/export/starexec/sandbox/solver/bin/prover9 -casc 300 -f /export/starexec/sandbox/benchmark/theBenchmark.p".
% 0.10/0.37
% 0.10/0.37 % From the command line: assign(max_seconds, 300).
% 43.68/6.75
% 43.68/6.75 % given #500 (T,wt=14): 1599 hascolor(n3,red) | hascolor(n5,red) | -hasperson(n4,italian). [resolve(1557,c,116,a)].
% 43.68/6.75
% 43.68/6.75 % given #1000 (T,wt=14): 3023 haspet(n4,guppy) | hasperson(n5,italian) | -hasperson(n2,italian). [resolve(2660,b,196,b)].
% 43.68/6.75
% 43.68/6.75 % given #1500 (W,wt=17): 3580 hascolor(n4,green) | hascolor(n3,red) | hascolor(n5,red) | -hasperson(n5,swede). [resolve(2724,a,194,a)].
% 43.68/6.75
% 43.68/6.75 % given #2000 (T,wt=17): 5138 hasgame(n4,charades) | hasgame(n4,solitaire) | hasgame(n2,solitaire) | -haspet(n4,no_pet). [resolve(4264,a,99,a)].
% 43.68/6.75
% 43.68/6.75 % given #2500 (W,wt=11): 6880 hasgame(n5,backgammon) | -hascolor(n5,red). [resolve(6860,b,408,b)].
% 43.68/6.75
% 43.68/6.75 % given #3000 (T,wt=11): 11364 hascolor(A,white) | -left(A,n5). [back_unit_del(6889),unit_del(a,11100)].
% 43.68/6.75
% 43.68/6.75 % SZS status Unsatisfiable for theBenchmark
% 43.68/6.75
% 43.68/6.75 % Proof 1 at 5.11 (+ 0.86) seconds.
% 43.68/6.75 % Length of proof is 551.
% 43.68/6.75 % Level of proof is 73.
% 43.68/6.75 % Maximum clause weight is 80.000.
% 43.68/6.75 % Given clauses 3139.
% 43.68/6.75
% 43.68/6.75 % SZS output start CNFRefutation for theBenchmark
% See solution above
%------------------------------------------------------------------------------