%------------------------------------------------------------------------------
% File : iProver---3.9.4
% Problem : PUZ017-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% Computer : n005.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 : Fri Sep 25 02:32:42 PM UTC 2026
% Result : Unsatisfiable 2.07s 1.17s
% Output : CNFRefutation 2.07s
% Verified :
% SZS Type : Refutation
% Derivation depth : 17
% Number of leaves : 97
% Syntax : Number of formulae : 482 ( 127 unt; 0 def)
% Number of atoms : 1357 ( 0 equ)
% Maximal formula atoms : 25 ( 2 avg)
% Number of connectives : 1524 ( 649 ~; 875 |; 0 &)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 51 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 1 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 39 ( 38 usr; 26 prp; 0-2 aty)
% Number of functors : 30 ( 30 usr; 30 con; 0-0 aty)
% Number of variables : 314 ( 0 sgn 314 !; 0 ?; 207 :)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] : samehouse(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_for_samehouse) ).
fof(f2,axiom,
~ samehouse(n1,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_1_not_2) ).
fof(f3,axiom,
~ samehouse(n1,n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_1_not_3) ).
fof(f4,axiom,
~ samehouse(n1,n4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_1_not_4) ).
fof(f5,axiom,
~ samehouse(n1,n5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_1_not_5) ).
fof(f6,axiom,
~ samehouse(n2,n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_2_not_3) ).
fof(f8,axiom,
~ samehouse(n2,n5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_2_not_5) ).
fof(f9,axiom,
~ samehouse(n3,n4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_3_not_4) ).
fof(f10,axiom,
~ samehouse(n3,n5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_3_not_5) ).
fof(f13,axiom,
~ sameperson(englishman,italian),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',englishman_not_italian) ).
fof(f15,axiom,
~ sameperson(englishman,russian),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',englishman_not_russian) ).
fof(f16,axiom,
~ sameperson(englishman,american),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',englishman_not_american) ).
fof(f18,axiom,
~ sameperson(italian,russian),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',italian_not_russian) ).
fof(f19,axiom,
~ sameperson(italian,american),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',italian_not_american) ).
fof(f20,axiom,
~ sameperson(swede,russian),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',swede_not_russian) ).
fof(f21,axiom,
~ sameperson(swede,american),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',swede_not_american) ).
fof(f24,axiom,
~ samecolor(red,white),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',red_not_white) ).
fof(f25,axiom,
~ samecolor(red,green),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',red_not_green) ).
fof(f27,axiom,
~ samecolor(red,blue),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',red_not_blue) ).
fof(f28,axiom,
~ samecolor(white,green),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',white_not_green) ).
fof(f30,axiom,
~ samecolor(white,blue),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',white_not_blue) ).
fof(f31,axiom,
~ samecolor(green,yellow),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',green_not_yellow) ).
fof(f32,axiom,
~ samecolor(green,blue),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',green_not_blue) ).
fof(f33,axiom,
~ samecolor(yellow,blue),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',yellow_not_blue) ).
fof(f35,axiom,
~ samedrink(lemonade,coffee),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lemonade_not_coffee) ).
fof(f37,axiom,
~ samedrink(lemonade,vodka),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lemonade_not_vodka) ).
fof(f39,axiom,
~ samedrink(coffee,milk),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',coffee_not_milk) ).
fof(f40,axiom,
~ samedrink(coffee,vodka),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',coffee_not_vodka) ).
fof(f42,axiom,
~ samedrink(milk,vodka),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',milk_not_vodka) ).
fof(f46,axiom,
~ samegame(backgammon,racquetball),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',backgammon_not_recquetball) ).
fof(f48,axiom,
~ samegame(backgammon,solitaire),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',backgammon_not_solitaire) ).
fof(f49,axiom,
~ samegame(backgammon,charades),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',backgammon_not_charades) ).
fof(f51,axiom,
~ samegame(racquetball,solitaire),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',racquetball_not_solitaire) ).
fof(f54,axiom,
~ samegame(quoits,charades),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quoits_not_charades) ).
fof(f55,axiom,
~ samegame(solitaire,charades),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',solitaire_not_charades) ).
fof(f57,axiom,
~ samepet(guppy,toad),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',guppy_not_toad) ).
fof(f59,axiom,
~ samepet(guppy,rat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',guppy_not_rat) ).
fof(f61,axiom,
~ samepet(toad,camel),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',toad_not_camel) ).
fof(f62,axiom,
~ samepet(toad,rat),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',toad_not_rat) ).
fof(f67,axiom,
! [X0,X1] :
( nextto(X1,X0)
| ~ nextto(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',symmetry_of_nextto) ).
fof(f70,axiom,
! [X0,X1] :
( nextto(X0,X1)
| ~ left(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',left_means_nextto) ).
fof(f71,axiom,
! [X0,X1] :
( ~ nextto(X0,X1)
| ~ samehouse(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_not_nextto_itself) ).
fof(f73,axiom,
! [X0] : ~ nextto(X0,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nothing_nextto_itself) ).
fof(f74,axiom,
! [X0] :
( hasperson(X0,american)
| hasperson(X0,russian)
| hasperson(X0,swede)
| hasperson(X0,italian)
| hasperson(X0,englishman) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_house_has_a_national) ).
fof(f75,axiom,
! [X0] :
( hasperson(n5,X0)
| hasperson(n4,X0)
| hasperson(n3,X0)
| hasperson(n2,X0)
| hasperson(n1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_natioality_is_used) ).
fof(f76,axiom,
! [X0] :
( hascolor(X0,blue)
| hascolor(X0,yellow)
| hascolor(X0,green)
| hascolor(X0,white)
| hascolor(X0,red) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_house_has_color) ).
fof(f77,axiom,
! [X0] :
( hascolor(n5,X0)
| hascolor(n4,X0)
| hascolor(n3,X0)
| hascolor(n2,X0)
| hascolor(n1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_color_is_used) ).
fof(f78,axiom,
! [X0] :
( hasdrink(X0,unknown_drink)
| hasdrink(X0,vodka)
| hasdrink(X0,milk)
| hasdrink(X0,coffee)
| hasdrink(X0,lemonade) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_house_has_a_drink) ).
fof(f79,axiom,
! [X0] :
( hasdrink(n5,X0)
| hasdrink(n4,X0)
| hasdrink(n3,X0)
| hasdrink(n2,X0)
| hasdrink(n1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_drink_is_used) ).
fof(f80,axiom,
! [X0] :
( hasgame(X0,charades)
| hasgame(X0,solitaire)
| hasgame(X0,quoits)
| hasgame(X0,racquetball)
| hasgame(X0,backgammon) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_house_has_a_game) ).
fof(f81,axiom,
! [X0] :
( hasgame(n5,X0)
| hasgame(n4,X0)
| hasgame(n3,X0)
| hasgame(n2,X0)
| hasgame(n1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_game_is_used) ).
fof(f82,axiom,
! [X0] :
( haspet(X0,no_pet)
| haspet(X0,rat)
| haspet(X0,camel)
| haspet(X0,toad)
| haspet(X0,guppy) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_house_has_a_pet) ).
fof(f83,axiom,
! [X0] :
( haspet(n5,X0)
| haspet(n4,X0)
| haspet(n3,X0)
| haspet(n2,X0)
| haspet(n1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_pet_is_used) ).
fof(f84,axiom,
! [X2,X0,X1] :
( ~ hascolor(X1,X2)
| ~ hascolor(X0,X2)
| samehouse(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',houses_have_unique_colors) ).
fof(f85,axiom,
! [X2,X0,X1] :
( ~ hasperson(X1,X2)
| ~ hasperson(X0,X2)
| samehouse(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nationals_have_unique_houses) ).
fof(f86,axiom,
! [X2,X0,X1] :
( ~ hasdrink(X1,X2)
| ~ hasdrink(X0,X2)
| samehouse(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',drinks_have_unique_houses) ).
fof(f87,axiom,
! [X2,X0,X1] :
( ~ hasgame(X1,X2)
| ~ hasgame(X0,X2)
| samehouse(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',games_have_unique_houses) ).
fof(f88,axiom,
! [X2,X0,X1] :
( ~ haspet(X1,X2)
| ~ haspet(X0,X2)
| samehouse(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',pets_have_unique_houses) ).
fof(f89,axiom,
! [X2,X0,X1] :
( ~ hasperson(X2,X1)
| ~ hasperson(X2,X0)
| sameperson(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',houses_have_unique_nationals) ).
fof(f90,axiom,
! [X2,X0,X1] :
( ~ hascolor(X2,X1)
| ~ hascolor(X2,X0)
| samecolor(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',colours_are_unique) ).
fof(f91,axiom,
! [X2,X0,X1] :
( ~ hasdrink(X2,X1)
| ~ hasdrink(X2,X0)
| samedrink(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',houses_have_unique_drinks) ).
fof(f92,axiom,
! [X2,X0,X1] :
( ~ hasgame(X2,X1)
| ~ hasgame(X2,X0)
| samegame(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',houses_have_unique_games) ).
fof(f93,axiom,
! [X2,X0,X1] :
( ~ haspet(X2,X1)
| ~ haspet(X2,X0)
| samepet(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',houses_have_unique_pets) ).
fof(f94,axiom,
! [X0] :
( hascolor(X0,red)
| ~ hasperson(X0,englishman) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',englishman_lives_in_red_house1) ).
fof(f95,axiom,
! [X0] :
( ~ hascolor(X0,red)
| hasperson(X0,englishman) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',englishman_lives_in_red_house2) ).
fof(f96,axiom,
! [X0,X1] :
( left(X0,X1)
| ~ hascolor(X1,green)
| ~ hascolor(X0,white) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',white_house_left_of_green1) ).
fof(f97,axiom,
! [X0,X1] :
( ~ left(X0,X1)
| hascolor(X1,green)
| ~ hascolor(X0,white) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',white_house_left_of_green2) ).
fof(f98,axiom,
! [X0,X1] :
( ~ left(X0,X1)
| ~ hascolor(X1,green)
| hascolor(X0,white) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',white_house_left_of_green3) ).
fof(f99,axiom,
! [X0] :
( haspet(X0,guppy)
| ~ hasperson(X0,italian) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',italian_has_guppy1) ).
fof(f100,axiom,
! [X0] :
( ~ haspet(X0,guppy)
| hasperson(X0,italian) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',italian_has_guppy2) ).
fof(f101,axiom,
! [X0] :
( hascolor(X0,green)
| ~ hasdrink(X0,lemonade) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lemonade_in_green_house1) ).
fof(f102,axiom,
! [X0] :
( ~ hascolor(X0,green)
| hasdrink(X0,lemonade) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lemonade_in_green_house2) ).
fof(f103,axiom,
! [X0] :
( hasdrink(X0,coffee)
| ~ hasperson(X0,swede) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',swede_drinks_coffee1) ).
fof(f104,axiom,
! [X0] :
( ~ hasdrink(X0,coffee)
| hasperson(X0,swede) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',swede_drinks_coffee2) ).
fof(f105,axiom,
! [X0] :
( hasgame(X0,backgammon)
| ~ haspet(X0,toad) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',toad_lives_with_backgammon1) ).
fof(f106,axiom,
! [X0] :
( ~ hasgame(X0,backgammon)
| haspet(X0,toad) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',toad_lives_with_backgammon2) ).
fof(f107,axiom,
! [X0] :
( hascolor(X0,yellow)
| ~ hasgame(X0,racquetball) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',racquetball_played_in_yellow_house1) ).
fof(f108,axiom,
! [X0] :
( ~ hascolor(X0,yellow)
| hasgame(X0,racquetball) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',racquetball_played_in_yellow_house2) ).
fof(f113,axiom,
! [X2,X0,X1] :
( haspet(X1,camel)
| haspet(X0,camel)
| ~ hasgame(X2,quoits)
| ~ nextto(X2,X1)
| ~ nextto(X2,X0)
| samehouse(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c5) ).
fof(f118,axiom,
! [X0,X1] :
( hasgame(X1,racquetball)
| ~ samehouse(X0,n5)
| ~ nextto(X0,X1)
| ~ haspet(X0,rat) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c10) ).
fof(f121,axiom,
! [X0,X1] :
( haspet(X1,rat)
| ~ hasgame(X0,racquetball)
| ~ samehouse(n1,X0)
| ~ nextto(X0,X1) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c13) ).
fof(f123,axiom,
! [X0] :
( hasdrink(X0,vodka)
| ~ hasgame(X0,solitaire) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c15) ).
fof(f124,axiom,
! [X0] :
( ~ hasdrink(X0,vodka)
| hasgame(X0,solitaire) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c16) ).
fof(f125,axiom,
! [X0] :
( hasgame(X0,charades)
| ~ hasperson(X0,american) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c17) ).
fof(f126,axiom,
! [X0] :
( ~ hasgame(X0,charades)
| hasperson(X0,american) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c18) ).
fof(f128,axiom,
! [X0,X1] :
( hascolor(X1,blue)
| ~ nextto(X0,X1)
| ~ samehouse(n1,X0)
| ~ hasperson(X0,russian) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c20) ).
fof(f130,axiom,
! [X0,X1] :
( ~ hascolor(X1,blue)
| nextto(X0,X1)
| ~ hasperson(X0,russian) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c22) ).
fof(f135,axiom,
! [X0] : ~ left(n5,X0),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house5_at_right) ).
fof(f136,axiom,
left(n1,n2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_1_left_of_2) ).
fof(f137,axiom,
left(n2,n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_2_left_of_3) ).
fof(f138,axiom,
left(n3,n4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_3_left_of_4) ).
fof(f139,axiom,
left(n4,n5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_4_left_of_5) ).
fof(f140,axiom,
~ nextto(n1,n3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_1_not_nextto_3) ).
fof(f142,axiom,
~ nextto(n1,n5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_1_not_nextto_5) ).
fof(f146,axiom,
hasdrink(n3,milk),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_3_has_milk) ).
fof(f147,axiom,
hasperson(n1,russian),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_1_has_russian) ).
fof(f148,negated_conjecture,
! [X2,X21,X0,X11,X18,X6,X9,X16,X4,X15,X22,X13,X20,X3,X10,X1,X8,X19,X7,X14,X17,X24,X5,X12,X23] :
( ~ haspet(n5,X24)
| ~ haspet(n4,X23)
| ~ haspet(n3,X22)
| ~ haspet(n2,X21)
| ~ haspet(n1,X20)
| ~ hasgame(n5,X19)
| ~ hasgame(n4,X18)
| ~ hasgame(n3,X17)
| ~ hasgame(n2,X16)
| ~ hasgame(n1,X15)
| ~ hasdrink(n5,X14)
| ~ hasdrink(n4,X13)
| ~ hasdrink(n3,X12)
| ~ hasdrink(n2,X11)
| ~ hasdrink(n1,X10)
| ~ hascolor(n5,X9)
| ~ hascolor(n4,X8)
| ~ hascolor(n3,X7)
| ~ hascolor(n2,X6)
| ~ hascolor(n1,X5)
| ~ hasperson(n5,X4)
| ~ hasperson(n4,X3)
| ~ hasperson(n3,X2)
| ~ hasperson(n2,X1)
| ~ hasperson(n1,X0) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',find_out_house_details) ).
tcf(c_197,plain,
! [X0: $i] :
( hascolor(X0,red)
| ~ hasperson(X0,englishman) ),
inference(cnf_transformation,[],[f94]) ).
tcf(c_198,plain,
! [X0: $i] :
( hasperson(X0,englishman)
| ~ hascolor(X0,red) ),
inference(cnf_transformation,[],[f95]) ).
tcf(c_199,plain,
! [X0: $i,X1: $i] :
( left(X1,X0)
| ~ hascolor(X1,white)
| ~ hascolor(X0,green) ),
inference(cnf_transformation,[],[f96]) ).
tcf(c_200,plain,
! [X0: $i,X1: $i] :
( hascolor(X1,green)
| ~ hascolor(X0,white)
| ~ left(X0,X1) ),
inference(cnf_transformation,[],[f97]) ).
tcf(c_201,plain,
! [X0: $i,X1: $i] :
( hascolor(X0,white)
| ~ hascolor(X1,green)
| ~ left(X0,X1) ),
inference(cnf_transformation,[],[f98]) ).
tcf(c_202,plain,
! [X0: $i] :
( haspet(X0,guppy)
| ~ hasperson(X0,italian) ),
inference(cnf_transformation,[],[f99]) ).
tcf(c_203,plain,
! [X0: $i] :
( hasperson(X0,italian)
| ~ haspet(X0,guppy) ),
inference(cnf_transformation,[],[f100]) ).
tcf(c_204,plain,
! [X0: $i] :
( hascolor(X0,green)
| ~ hasdrink(X0,lemonade) ),
inference(cnf_transformation,[],[f101]) ).
tcf(c_205,plain,
! [X0: $i] :
( hasdrink(X0,lemonade)
| ~ hascolor(X0,green) ),
inference(cnf_transformation,[],[f102]) ).
tcf(c_206,plain,
! [X0: $i] :
( hasdrink(X0,coffee)
| ~ hasperson(X0,swede) ),
inference(cnf_transformation,[],[f103]) ).
tcf(c_207,plain,
! [X0: $i] :
( hasperson(X0,swede)
| ~ hasdrink(X0,coffee) ),
inference(cnf_transformation,[],[f104]) ).
tcf(c_208,plain,
! [X0: $i] :
( hasgame(X0,backgammon)
| ~ haspet(X0,toad) ),
inference(cnf_transformation,[],[f105]) ).
tcf(c_209,plain,
! [X0: $i] :
( haspet(X0,toad)
| ~ hasgame(X0,backgammon) ),
inference(cnf_transformation,[],[f106]) ).
tcf(c_210,plain,
! [X0: $i] :
( hascolor(X0,yellow)
| ~ hasgame(X0,racquetball) ),
inference(cnf_transformation,[],[f107]) ).
tcf(c_211,plain,
! [X0: $i] :
( hasgame(X0,racquetball)
| ~ hascolor(X0,yellow) ),
inference(cnf_transformation,[],[f108]) ).
tcf(c_216,plain,
! [X0: $i,X1: $i,X2: $i] :
( haspet(X2,camel)
| haspet(X1,camel)
| samehouse(X2,X1)
| ~ hasgame(X0,quoits)
| ~ nextto(X0,X2)
| ~ nextto(X0,X1) ),
inference(cnf_transformation,[],[f113]) ).
tcf(c_221,plain,
! [X0: $i,X1: $i] :
( hasgame(X1,racquetball)
| ~ haspet(X0,rat)
| ~ samehouse(X0,n5)
| ~ nextto(X0,X1) ),
inference(cnf_transformation,[],[f118]) ).
tcf(c_224,plain,
! [X0: $i,X1: $i] :
( haspet(X1,rat)
| ~ hasgame(X0,racquetball)
| ~ samehouse(n1,X0)
| ~ nextto(X0,X1) ),
inference(cnf_transformation,[],[f121]) ).
tcf(c_226,plain,
! [X0: $i] :
( hasdrink(X0,vodka)
| ~ hasgame(X0,solitaire) ),
inference(cnf_transformation,[],[f123]) ).
tcf(c_227,plain,
! [X0: $i] :
( hasgame(X0,solitaire)
| ~ hasdrink(X0,vodka) ),
inference(cnf_transformation,[],[f124]) ).
tcf(c_228,plain,
! [X0: $i] :
( hasgame(X0,charades)
| ~ hasperson(X0,american) ),
inference(cnf_transformation,[],[f125]) ).
tcf(c_229,plain,
! [X0: $i] :
( hasperson(X0,american)
| ~ hasgame(X0,charades) ),
inference(cnf_transformation,[],[f126]) ).
tcf(c_231,plain,
! [X0: $i,X1: $i] :
( hascolor(X1,blue)
| ~ hasperson(X0,russian)
| ~ samehouse(n1,X0)
| ~ nextto(X0,X1) ),
inference(cnf_transformation,[],[f128]) ).
tcf(c_233,plain,
! [X0: $i,X1: $i] :
( nextto(X0,X1)
| ~ hascolor(X1,blue)
| ~ hasperson(X0,russian) ),
inference(cnf_transformation,[],[f130]) ).
tcf(c_238,plain,
! [X0: $i] : ~ left(n5,X0),
inference(cnf_transformation,[],[f135]) ).
tcf(c_239,plain,
left(n1,n2),
inference(cnf_transformation,[],[f136]) ).
tcf(c_240,plain,
left(n2,n3),
inference(cnf_transformation,[],[f137]) ).
tcf(c_241,plain,
left(n3,n4),
inference(cnf_transformation,[],[f138]) ).
tcf(c_242,plain,
left(n4,n5),
inference(cnf_transformation,[],[f139]) ).
tcf(c_243,plain,
~ nextto(n1,n3),
inference(cnf_transformation,[],[f140]) ).
tcf(c_245,plain,
~ nextto(n1,n5),
inference(cnf_transformation,[],[f142]) ).
tcf(c_249,plain,
hasdrink(n3,milk),
inference(cnf_transformation,[],[f146]) ).
tcf(c_250,plain,
hasperson(n1,russian),
inference(cnf_transformation,[],[f147]) ).
tcf(c_251,negated_conjecture,
! [X0: $i,X1: $i,X2: $i,X3: $i,X4: $i,X5: $i,X6: $i,X7: $i,X8: $i,X9: $i,X10: $i,X11: $i,X12: $i,X13: $i,X14: $i,X15: $i,X16: $i,X17: $i,X18: $i,X19: $i,X20: $i,X21: $i,X22: $i,X23: $i,X24: $i] :
( ~ haspet(n5,X24)
| ~ haspet(n4,X23)
| ~ haspet(n3,X22)
| ~ haspet(n2,X21)
| ~ haspet(n1,X20)
| ~ hasgame(n5,X19)
| ~ hasgame(n4,X18)
| ~ hasgame(n3,X17)
| ~ hasgame(n2,X16)
| ~ hasgame(n1,X15)
| ~ hasdrink(n5,X14)
| ~ hasdrink(n4,X13)
| ~ hasdrink(n3,X12)
| ~ hasdrink(n2,X11)
| ~ hasdrink(n1,X10)
| ~ hascolor(n5,X9)
| ~ hascolor(n4,X8)
| ~ hascolor(n3,X7)
| ~ hascolor(n2,X6)
| ~ hascolor(n1,X5)
| ~ hasperson(n5,X4)
| ~ hasperson(n4,X3)
| ~ hasperson(n3,X2)
| ~ hasperson(n2,X1)
| ~ hasperson(n1,X0) ),
inference(cnf_transformation,[],[f148]) ).
tcf(c_252,plain,
! [X0: $i] :
( hasperson(X0,american)
| hasperson(X0,russian)
| hasperson(X0,swede)
| hasperson(X0,italian)
| hasperson(X0,englishman) ),
inference(cnf_transformation,[],[f74]) ).
tcf(c_253,plain,
~ sameperson(englishman,american),
inference(cnf_transformation,[],[f16]) ).
tcf(c_254,plain,
~ sameperson(englishman,russian),
inference(cnf_transformation,[],[f15]) ).
tcf(c_256,plain,
~ sameperson(englishman,italian),
inference(cnf_transformation,[],[f13]) ).
tcf(c_257,plain,
! [X0: $i,X1: $i,X2: $i] :
( samehouse(X2,X0)
| ~ hasperson(X2,X1)
| ~ hasperson(X0,X1) ),
inference(cnf_transformation,[],[f85]) ).
tcf(c_258,plain,
! [X0: $i] :
( hasperson(n5,X0)
| hasperson(n4,X0)
| hasperson(n3,X0)
| hasperson(n2,X0)
| hasperson(n1,X0) ),
inference(cnf_transformation,[],[f75]) ).
tcf(c_259,plain,
! [X0: $i,X1: $i,X2: $i] :
( samehouse(X2,X0)
| ~ hascolor(X2,X1)
| ~ hascolor(X0,X1) ),
inference(cnf_transformation,[],[f84]) ).
tcf(c_260,plain,
! [X0: $i] :
( hascolor(n5,X0)
| hascolor(n4,X0)
| hascolor(n3,X0)
| hascolor(n2,X0)
| hascolor(n1,X0) ),
inference(cnf_transformation,[],[f77]) ).
tcf(c_261,plain,
! [X0: $i] :
( hascolor(X0,blue)
| hascolor(X0,yellow)
| hascolor(X0,green)
| hascolor(X0,white)
| hascolor(X0,red) ),
inference(cnf_transformation,[],[f76]) ).
tcf(c_262,plain,
~ samecolor(red,blue),
inference(cnf_transformation,[],[f27]) ).
tcf(c_264,plain,
~ samecolor(red,green),
inference(cnf_transformation,[],[f25]) ).
tcf(c_265,plain,
~ samecolor(red,white),
inference(cnf_transformation,[],[f24]) ).
tcf(c_267,plain,
! [X0: $i,X1: $i] :
( nextto(X0,X1)
| ~ left(X0,X1) ),
inference(cnf_transformation,[],[f70]) ).
tcf(c_270,plain,
~ samecolor(white,blue),
inference(cnf_transformation,[],[f30]) ).
tcf(c_272,plain,
~ samecolor(white,green),
inference(cnf_transformation,[],[f28]) ).
tcf(c_273,plain,
~ samecolor(green,blue),
inference(cnf_transformation,[],[f32]) ).
tcf(c_274,plain,
~ samecolor(green,yellow),
inference(cnf_transformation,[],[f31]) ).
tcf(c_275,plain,
~ sameperson(italian,american),
inference(cnf_transformation,[],[f19]) ).
tcf(c_276,plain,
~ sameperson(italian,russian),
inference(cnf_transformation,[],[f18]) ).
tcf(c_278,plain,
! [X0: $i,X1: $i,X2: $i] :
( samehouse(X2,X0)
| ~ haspet(X2,X1)
| ~ haspet(X0,X1) ),
inference(cnf_transformation,[],[f88]) ).
tcf(c_279,plain,
! [X0: $i] :
( haspet(X0,no_pet)
| haspet(X0,rat)
| haspet(X0,camel)
| haspet(X0,toad)
| haspet(X0,guppy) ),
inference(cnf_transformation,[],[f82]) ).
tcf(c_281,plain,
~ samepet(guppy,rat),
inference(cnf_transformation,[],[f59]) ).
tcf(c_283,plain,
~ samepet(guppy,toad),
inference(cnf_transformation,[],[f57]) ).
tcf(c_284,plain,
! [X0: $i,X1: $i,X2: $i] :
( samedrink(X2,X1)
| ~ hasdrink(X0,X2)
| ~ hasdrink(X0,X1) ),
inference(cnf_transformation,[],[f91]) ).
tcf(c_285,plain,
! [X0: $i,X1: $i,X2: $i] :
( samehouse(X2,X0)
| ~ hasdrink(X2,X1)
| ~ hasdrink(X0,X1) ),
inference(cnf_transformation,[],[f86]) ).
tcf(c_286,plain,
! [X0: $i] :
( hasdrink(n5,X0)
| hasdrink(n4,X0)
| hasdrink(n3,X0)
| hasdrink(n2,X0)
| hasdrink(n1,X0) ),
inference(cnf_transformation,[],[f79]) ).
tcf(c_287,plain,
! [X0: $i] :
( hasdrink(X0,unknown_drink)
| hasdrink(X0,vodka)
| hasdrink(X0,milk)
| hasdrink(X0,coffee)
| hasdrink(X0,lemonade) ),
inference(cnf_transformation,[],[f78]) ).
tcf(c_289,plain,
~ samedrink(lemonade,vodka),
inference(cnf_transformation,[],[f37]) ).
tcf(c_291,plain,
~ samedrink(lemonade,coffee),
inference(cnf_transformation,[],[f35]) ).
tcf(c_292,plain,
~ sameperson(swede,american),
inference(cnf_transformation,[],[f21]) ).
tcf(c_293,plain,
~ sameperson(swede,russian),
inference(cnf_transformation,[],[f20]) ).
tcf(c_295,plain,
~ samedrink(coffee,vodka),
inference(cnf_transformation,[],[f40]) ).
tcf(c_296,plain,
~ samedrink(coffee,milk),
inference(cnf_transformation,[],[f39]) ).
tcf(c_297,plain,
! [X0: $i,X1: $i,X2: $i] :
( samehouse(X2,X0)
| ~ hasgame(X2,X1)
| ~ hasgame(X0,X1) ),
inference(cnf_transformation,[],[f87]) ).
tcf(c_298,plain,
! [X0: $i] :
( hasgame(X0,charades)
| hasgame(X0,solitaire)
| hasgame(X0,quoits)
| hasgame(X0,racquetball)
| hasgame(X0,backgammon) ),
inference(cnf_transformation,[],[f80]) ).
tcf(c_299,plain,
~ samegame(backgammon,charades),
inference(cnf_transformation,[],[f49]) ).
tcf(c_300,plain,
~ samegame(backgammon,solitaire),
inference(cnf_transformation,[],[f48]) ).
tcf(c_302,plain,
~ samegame(backgammon,racquetball),
inference(cnf_transformation,[],[f46]) ).
tcf(c_304,plain,
~ samepet(toad,rat),
inference(cnf_transformation,[],[f62]) ).
tcf(c_305,plain,
~ samepet(toad,camel),
inference(cnf_transformation,[],[f61]) ).
tcf(c_306,plain,
~ samecolor(yellow,blue),
inference(cnf_transformation,[],[f33]) ).
tcf(c_308,plain,
! [X0: $i,X1: $i] :
( ~ nextto(X0,X1)
| ~ samehouse(X0,X1) ),
inference(cnf_transformation,[],[f71]) ).
tcf(c_309,plain,
! [X0: $i] : samehouse(X0,X0),
inference(cnf_transformation,[],[f1]) ).
tcf(c_310,plain,
! [X0: $i] : ~ nextto(X0,X0),
inference(cnf_transformation,[],[f73]) ).
tcf(c_311,plain,
! [X0: $i,X1: $i] :
( nextto(X1,X0)
| ~ nextto(X0,X1) ),
inference(cnf_transformation,[],[f67]) ).
tcf(c_313,plain,
~ samehouse(n1,n5),
inference(cnf_transformation,[],[f5]) ).
tcf(c_314,plain,
~ samehouse(n1,n3),
inference(cnf_transformation,[],[f3]) ).
tcf(c_315,plain,
! [X0: $i] :
( haspet(n5,X0)
| haspet(n4,X0)
| haspet(n3,X0)
| haspet(n2,X0)
| haspet(n1,X0) ),
inference(cnf_transformation,[],[f83]) ).
tcf(c_316,plain,
! [X0: $i] :
( hasgame(n5,X0)
| hasgame(n4,X0)
| hasgame(n3,X0)
| hasgame(n2,X0)
| hasgame(n1,X0) ),
inference(cnf_transformation,[],[f81]) ).
tcf(c_318,plain,
~ samehouse(n3,n5),
inference(cnf_transformation,[],[f10]) ).
tcf(c_319,plain,
~ samehouse(n2,n5),
inference(cnf_transformation,[],[f8]) ).
tcf(c_321,plain,
~ samedrink(milk,vodka),
inference(cnf_transformation,[],[f42]) ).
tcf(c_322,plain,
~ samegame(solitaire,charades),
inference(cnf_transformation,[],[f55]) ).
tcf(c_324,plain,
~ samegame(racquetball,solitaire),
inference(cnf_transformation,[],[f51]) ).
tcf(c_326,plain,
~ samegame(quoits,charades),
inference(cnf_transformation,[],[f54]) ).
tcf(c_329,plain,
~ samehouse(n2,n3),
inference(cnf_transformation,[],[f6]) ).
tcf(c_330,plain,
~ samehouse(n1,n2),
inference(cnf_transformation,[],[f2]) ).
tcf(c_331,plain,
~ samehouse(n3,n4),
inference(cnf_transformation,[],[f9]) ).
tcf(c_332,plain,
~ samehouse(n1,n4),
inference(cnf_transformation,[],[f4]) ).
tcf(c_334,plain,
! [X0: $i,X1: $i,X2: $i] :
( sameperson(X2,X1)
| ~ hasperson(X0,X2)
| ~ hasperson(X0,X1) ),
inference(cnf_transformation,[],[f89]) ).
tcf(c_336,plain,
! [X0: $i,X1: $i,X2: $i] :
( samecolor(X2,X1)
| ~ hascolor(X0,X2)
| ~ hascolor(X0,X1) ),
inference(cnf_transformation,[],[f90]) ).
tcf(c_340,plain,
! [X0: $i,X1: $i,X2: $i] :
( samepet(X2,X1)
| ~ haspet(X0,X2)
| ~ haspet(X0,X1) ),
inference(cnf_transformation,[],[f93]) ).
tcf(c_343,plain,
! [X0: $i,X1: $i,X2: $i] :
( samegame(X2,X1)
| ~ hasgame(X0,X2)
| ~ hasgame(X0,X1) ),
inference(cnf_transformation,[],[f92]) ).
tcf(c_350,plain,
samehouse(n1,n1),
inference(instantiation,[status(thm)],[c_309]) ).
tcf(c_351,plain,
~ nextto(n1,n1),
inference(instantiation,[status(thm)],[c_310]) ).
tcf(c_353,plain,
~ left(n5,n1),
inference(instantiation,[status(thm)],[c_238]) ).
tcf(c_356,plain,
( hasgame(n1,solitaire)
| ~ hasdrink(n1,vodka) ),
inference(instantiation,[status(thm)],[c_227]) ).
tcf(c_358,plain,
( hasgame(n1,racquetball)
| ~ hascolor(n1,yellow) ),
inference(instantiation,[status(thm)],[c_211]) ).
tcf(c_359,plain,
( hascolor(n1,yellow)
| ~ hasgame(n1,racquetball) ),
inference(instantiation,[status(thm)],[c_210]) ).
tcf(c_362,plain,
( hasperson(n1,swede)
| ~ hasdrink(n1,coffee) ),
inference(instantiation,[status(thm)],[c_207]) ).
tcf(c_365,plain,
( hascolor(n1,green)
| ~ hasdrink(n1,lemonade) ),
inference(instantiation,[status(thm)],[c_204]) ).
tcf(c_366,plain,
( hasperson(n1,italian)
| ~ haspet(n1,guppy) ),
inference(instantiation,[status(thm)],[c_203]) ).
tcf(c_368,plain,
( hasperson(n1,englishman)
| ~ hascolor(n1,red) ),
inference(instantiation,[status(thm)],[c_198]) ).
tcf(c_370,plain,
( nextto(n1,n1)
| ~ hascolor(n1,blue)
| ~ hasperson(n1,russian) ),
inference(instantiation,[status(thm)],[c_233]) ).
tcf(c_377,plain,
( hasdrink(n1,unknown_drink)
| hasdrink(n1,vodka)
| hasdrink(n1,milk)
| hasdrink(n1,coffee)
| hasdrink(n1,lemonade) ),
inference(instantiation,[status(thm)],[c_287]) ).
tcf(c_380,plain,
( hascolor(n1,blue)
| hascolor(n1,yellow)
| hascolor(n1,green)
| hascolor(n1,white)
| hascolor(n1,red) ),
inference(instantiation,[status(thm)],[c_261]) ).
tcf(c_384,plain,
! [X0: $i] :
( ~ hasperson(X0,englishman)
| hascolor(X0,red) ),
inference(prop_impl_just,[status(thm)],[c_197]) ).
tcf(c_385,plain,
! [X0: $i] :
( hascolor(X0,red)
| ~ hasperson(X0,englishman) ),
inference(renaming,[status(thm)],[c_384]) ).
tcf(c_388,plain,
! [X0: $i] :
( ~ hasperson(X0,italian)
| haspet(X0,guppy) ),
inference(prop_impl_just,[status(thm)],[c_202]) ).
tcf(c_389,plain,
! [X0: $i] :
( haspet(X0,guppy)
| ~ hasperson(X0,italian) ),
inference(renaming,[status(thm)],[c_388]) ).
tcf(c_392,plain,
! [X0: $i] :
( ~ hasperson(X0,swede)
| hasdrink(X0,coffee) ),
inference(prop_impl_just,[status(thm)],[c_206]) ).
tcf(c_393,plain,
! [X0: $i] :
( hasdrink(X0,coffee)
| ~ hasperson(X0,swede) ),
inference(renaming,[status(thm)],[c_392]) ).
tcf(c_396,plain,
! [X0: $i] :
( ~ hasperson(X0,american)
| hasgame(X0,charades) ),
inference(prop_impl_just,[status(thm)],[c_228]) ).
tcf(c_397,plain,
! [X0: $i] :
( hasgame(X0,charades)
| ~ hasperson(X0,american) ),
inference(renaming,[status(thm)],[c_396]) ).
tcf(c_400,plain,
! [X0: $i] :
( ~ hascolor(X0,green)
| hasdrink(X0,lemonade) ),
inference(prop_impl_just,[status(thm)],[c_205]) ).
tcf(c_401,plain,
! [X0: $i] :
( hasdrink(X0,lemonade)
| ~ hascolor(X0,green) ),
inference(renaming,[status(thm)],[c_400]) ).
tcf(c_402,plain,
! [X0: $i] :
( hascolor(X0,green)
| ~ hasdrink(X0,lemonade) ),
inference(prop_impl_just,[status(thm)],[c_204]) ).
tcf(c_404,plain,
! [X0: $i] :
( ~ hascolor(X0,yellow)
| hasgame(X0,racquetball) ),
inference(prop_impl_just,[status(thm)],[c_211]) ).
tcf(c_405,plain,
! [X0: $i] :
( hasgame(X0,racquetball)
| ~ hascolor(X0,yellow) ),
inference(renaming,[status(thm)],[c_404]) ).
tcf(c_408,plain,
! [X0: $i] :
( ~ hasdrink(X0,vodka)
| hasgame(X0,solitaire) ),
inference(prop_impl_just,[status(thm)],[c_227]) ).
tcf(c_409,plain,
! [X0: $i] :
( hasgame(X0,solitaire)
| ~ hasdrink(X0,vodka) ),
inference(renaming,[status(thm)],[c_408]) ).
tcf(c_412,plain,
! [X0: $i] :
( ~ hasgame(X0,backgammon)
| haspet(X0,toad) ),
inference(prop_impl_just,[status(thm)],[c_209]) ).
tcf(c_413,plain,
! [X0: $i] :
( haspet(X0,toad)
| ~ hasgame(X0,backgammon) ),
inference(renaming,[status(thm)],[c_412]) ).
tcf(c_679,plain,
! [X0: $i,X1: $i] :
( left(X0,X1)
| ~ hasdrink(X1,lemonade)
| ~ hascolor(X0,white) ),
inference(bin_hyper_res,[status(thm)],[c_199,c_402]) ).
tcf(c_680,plain,
! [X0: $i] :
( haspet(X0,guppy)
| hasgame(X0,charades)
| hasdrink(X0,coffee)
| hascolor(X0,red)
| hasperson(X0,russian) ),
inference(bin_hyper_res,[status(thm)],[c_252,c_397,c_393,c_389,c_385]) ).
tcf(c_681,plain,
! [X0: $i] :
( hasgame(X0,racquetball)
| hasdrink(X0,lemonade)
| hascolor(X0,blue)
| hascolor(X0,white)
| hascolor(X0,red) ),
inference(bin_hyper_res,[status(thm)],[c_261,c_405,c_401]) ).
tcf(c_682,plain,
! [X0: $i] :
( hasgame(X0,solitaire)
| hasdrink(X0,unknown_drink)
| hasdrink(X0,milk)
| hasdrink(X0,coffee)
| hasdrink(X0,lemonade) ),
inference(bin_hyper_res,[status(thm)],[c_287,c_409]) ).
tcf(c_683,plain,
! [X0: $i] :
( haspet(X0,toad)
| hasgame(X0,charades)
| hasgame(X0,solitaire)
| hasgame(X0,quoits)
| hasgame(X0,racquetball) ),
inference(bin_hyper_res,[status(thm)],[c_298,c_413]) ).
tcf(c_687,plain,
( hasgame(n1,racquetball)
| hasdrink(n1,lemonade)
| hascolor(n1,blue)
| hascolor(n1,white)
| hascolor(n1,red) ),
inference(instantiation,[status(thm)],[c_681]) ).
tcf(c_1368,plain,
! [X0: $i] :
( ~ hasperson(X0,russian)
| ~ hasperson(X0,englishman) ),
inference(resolution,[status(thm)],[c_254,c_334]) ).
tcf(c_1369,plain,
( ~ hasperson(n1,russian)
| ~ hasperson(n1,englishman) ),
inference(instantiation,[status(thm)],[c_1368]) ).
tcf(c_1392,plain,
! [X0: $i] :
( ~ hasperson(X0,russian)
| ~ hasperson(X0,italian) ),
inference(resolution,[status(thm)],[c_276,c_334]) ).
tcf(c_1393,plain,
( ~ hasperson(n1,russian)
| ~ hasperson(n1,italian) ),
inference(instantiation,[status(thm)],[c_1392]) ).
tcf(c_1408,plain,
! [X0: $i] :
( ~ hasperson(X0,russian)
| ~ hasperson(X0,swede) ),
inference(resolution,[status(thm)],[c_293,c_334]) ).
tcf(c_1409,plain,
( ~ hasperson(n1,russian)
| ~ hasperson(n1,swede) ),
inference(instantiation,[status(thm)],[c_1408]) ).
tcf(c_1508,plain,
! [X0: $i] :
( ~ hascolor(X0,yellow)
| ~ hascolor(X0,green) ),
inference(resolution,[status(thm)],[c_274,c_336]) ).
tcf(c_1509,plain,
( ~ hascolor(n1,yellow)
| ~ hascolor(n1,green) ),
inference(instantiation,[status(thm)],[c_1508]) ).
tcf(c_1652,plain,
! [X0: $i] :
( ~ hasgame(X0,racquetball)
| ~ hasgame(X0,backgammon) ),
inference(resolution,[status(thm)],[c_302,c_343]) ).
tcf(c_1653,plain,
( ~ hasgame(n1,racquetball)
| ~ hasgame(n1,backgammon) ),
inference(instantiation,[status(thm)],[c_1652]) ).
tcf(c_1692,plain,
! [X0: $i] :
( ~ hasgame(X0,solitaire)
| ~ hasgame(X0,racquetball) ),
inference(resolution,[status(thm)],[c_324,c_343]) ).
tcf(c_1693,plain,
( ~ hasgame(n1,solitaire)
| ~ hasgame(n1,racquetball) ),
inference(instantiation,[status(thm)],[c_1692]) ).
tcf(c_1852,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_10
| ~ hasdrink(n3,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_10])],[c_251]) ).
tcf(c_1853,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_11
| ~ hasdrink(n4,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_11])],[c_251]) ).
tcf(c_1854,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_12
| ~ hasdrink(n2,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_12])],[c_251]) ).
tcf(c_1855,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_13
| ~ hasdrink(n5,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_13])],[c_251]) ).
tcf(c_1856,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_14
| ~ hasdrink(n1,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_14])],[c_251]) ).
tcf(c_1857,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_15
| ~ hasgame(n1,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_15])],[c_251]) ).
tcf(c_1858,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_16
| ~ hascolor(n5,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_16])],[c_251]) ).
tcf(c_1859,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_17
| ~ hasgame(n2,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_17])],[c_251]) ).
tcf(c_1860,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_18
| ~ hascolor(n4,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_18])],[c_251]) ).
tcf(c_1861,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_19
| ~ hasgame(n3,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_19])],[c_251]) ).
tcf(c_1862,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_20
| ~ hascolor(n3,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_20])],[c_251]) ).
tcf(c_1863,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_21
| ~ hasgame(n4,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_21])],[c_251]) ).
tcf(c_1864,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_22
| ~ hascolor(n2,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_22])],[c_251]) ).
tcf(c_1865,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_23
| ~ hasgame(n5,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_23])],[c_251]) ).
tcf(c_1866,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_24
| ~ hascolor(n1,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_24])],[c_251]) ).
tcf(c_1867,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_25
| ~ haspet(n1,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_25])],[c_251]) ).
tcf(c_1868,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_26
| ~ hasperson(n5,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_26])],[c_251]) ).
tcf(c_1869,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_27
| ~ haspet(n2,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_27])],[c_251]) ).
tcf(c_1870,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_28
| ~ hasperson(n4,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_28])],[c_251]) ).
tcf(c_1871,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_29
| ~ haspet(n3,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_29])],[c_251]) ).
tcf(c_1872,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_30
| ~ hasperson(n3,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_30])],[c_251]) ).
tcf(c_1873,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_31
| ~ haspet(n4,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_31])],[c_251]) ).
tcf(c_1874,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_32
| ~ hasperson(n2,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_32])],[c_251]) ).
tcf(c_1875,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_33
| ~ haspet(n5,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_33])],[c_251]) ).
tcf(c_1876,negated_conjecture,
! [X0: $i] :
( ~ iPr_def_34
| ~ hasperson(n1,X0) ),
inference(splitting,[splitting(split),new_symbols(definition,[iPr_def_34])],[c_251]) ).
tcf(c_1877,negated_conjecture,
( iPr_def_34
| iPr_def_33
| iPr_def_32
| iPr_def_31
| iPr_def_30
| iPr_def_29
| iPr_def_28
| iPr_def_27
| iPr_def_26
| iPr_def_25
| iPr_def_24
| iPr_def_23
| iPr_def_22
| iPr_def_21
| iPr_def_20
| iPr_def_19
| iPr_def_18
| iPr_def_17
| iPr_def_16
| iPr_def_15
| iPr_def_14
| iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_10 ),
inference(splitting,[splitting(split),new_symbols(definition,[])],[c_251]) ).
tcf(c_1903,plain,
( ~ iPr_def_10
| ~ hasdrink(n3,milk) ),
inference(instantiation,[status(thm)],[c_1852]) ).
tcf(c_1907,plain,
( hascolor(n2,white)
| ~ hascolor(n3,green)
| ~ left(n2,n3) ),
inference(instantiation,[status(thm)],[c_201]) ).
tcf(c_1908,plain,
( hascolor(n3,white)
| ~ hascolor(n4,green)
| ~ left(n3,n4) ),
inference(instantiation,[status(thm)],[c_201]) ).
tcf(c_1912,plain,
( hasperson(n5,italian)
| hasperson(n4,italian)
| hasperson(n3,italian)
| hasperson(n2,italian)
| hasperson(n1,italian) ),
inference(instantiation,[status(thm)],[c_258]) ).
tcf(c_1920,plain,
( hascolor(n5,white)
| hascolor(n4,white)
| hascolor(n3,white)
| hascolor(n2,white)
| hascolor(n1,white) ),
inference(instantiation,[status(thm)],[c_260]) ).
tcf(c_1922,plain,
! [X0: $i] :
( hascolor(X0,green)
| ~ hascolor(n1,white)
| ~ left(n1,X0) ),
inference(instantiation,[status(thm)],[c_200]) ).
tcf(c_1929,plain,
( hasdrink(n5,vodka)
| hasdrink(n4,vodka)
| hasdrink(n3,vodka)
| hasdrink(n2,vodka)
| hasdrink(n1,vodka) ),
inference(instantiation,[status(thm)],[c_286]) ).
tcf(c_1931,plain,
( haspet(n5,guppy)
| haspet(n4,guppy)
| haspet(n3,guppy)
| haspet(n2,guppy)
| haspet(n1,guppy) ),
inference(instantiation,[status(thm)],[c_315]) ).
tcf(c_1939,plain,
( hasgame(n5,solitaire)
| hasgame(n4,solitaire)
| hasgame(n3,solitaire)
| hasgame(n2,solitaire)
| hasgame(n1,solitaire) ),
inference(instantiation,[status(thm)],[c_316]) ).
tcf(c_1946,plain,
! [X0: $i] :
( samehouse(n1,n2)
| ~ hasperson(n2,X0)
| ~ hasperson(n1,X0) ),
inference(instantiation,[status(thm)],[c_257]) ).
tcf(c_1948,plain,
! [X0: $i] :
( samehouse(n1,n3)
| ~ hasperson(n3,X0)
| ~ hasperson(n1,X0) ),
inference(instantiation,[status(thm)],[c_257]) ).
tcf(c_1950,plain,
! [X0: $i] :
( samehouse(n1,n4)
| ~ hasperson(n4,X0)
| ~ hasperson(n1,X0) ),
inference(instantiation,[status(thm)],[c_257]) ).
tcf(c_1970,plain,
! [X0: $i] :
( samehouse(n1,n4)
| ~ hascolor(n4,X0)
| ~ hascolor(n1,X0) ),
inference(instantiation,[status(thm)],[c_259]) ).
tcf(c_1972,plain,
! [X0: $i] :
( samehouse(n1,n5)
| ~ hascolor(n5,X0)
| ~ hascolor(n1,X0) ),
inference(instantiation,[status(thm)],[c_259]) ).
tcf(c_1982,plain,
! [X0: $i] :
( samehouse(n3,n5)
| ~ hascolor(n5,X0)
| ~ hascolor(n3,X0) ),
inference(instantiation,[status(thm)],[c_259]) ).
tcf(c_1992,plain,
! [X0: $i] :
( samehouse(n1,n5)
| ~ haspet(n5,X0)
| ~ haspet(n1,X0) ),
inference(instantiation,[status(thm)],[c_278]) ).
tcf(c_2002,plain,
! [X0: $i] :
( samehouse(n3,n5)
| ~ haspet(n5,X0)
| ~ haspet(n3,X0) ),
inference(instantiation,[status(thm)],[c_278]) ).
tcf(c_2006,plain,
! [X0: $i] :
( samehouse(n1,n2)
| ~ hasdrink(n2,X0)
| ~ hasdrink(n1,X0) ),
inference(instantiation,[status(thm)],[c_285]) ).
tcf(c_2008,plain,
! [X0: $i] :
( samehouse(n1,n3)
| ~ hasdrink(n3,X0)
| ~ hasdrink(n1,X0) ),
inference(instantiation,[status(thm)],[c_285]) ).
tcf(c_2014,plain,
! [X0: $i] :
( samehouse(n2,n3)
| ~ hasdrink(n3,X0)
| ~ hasdrink(n2,X0) ),
inference(instantiation,[status(thm)],[c_285]) ).
tcf(c_2028,plain,
! [X0: $i] :
( samehouse(n1,n3)
| ~ hasgame(n3,X0)
| ~ hasgame(n1,X0) ),
inference(instantiation,[status(thm)],[c_297]) ).
tcf(c_2030,plain,
! [X0: $i] :
( samehouse(n1,n4)
| ~ hasgame(n4,X0)
| ~ hasgame(n1,X0) ),
inference(instantiation,[status(thm)],[c_297]) ).
tcf(c_2038,plain,
! [X0: $i] :
( samehouse(n2,n5)
| ~ hasgame(n5,X0)
| ~ hasgame(n2,X0) ),
inference(instantiation,[status(thm)],[c_297]) ).
tcf(c_2040,plain,
! [X0: $i] :
( samehouse(n3,n4)
| ~ hasgame(n4,X0)
| ~ hasgame(n3,X0) ),
inference(instantiation,[status(thm)],[c_297]) ).
tcf(c_2046,plain,
! [X0: $i] :
( sameperson(englishman,american)
| ~ hasperson(X0,american)
| ~ hasperson(X0,englishman) ),
inference(instantiation,[status(thm)],[c_334]) ).
tcf(c_2049,plain,
! [X0: $i] :
( sameperson(englishman,italian)
| ~ hasperson(X0,italian)
| ~ hasperson(X0,englishman) ),
inference(instantiation,[status(thm)],[c_334]) ).
tcf(c_2050,plain,
! [X0: $i] :
( samecolor(red,blue)
| ~ hascolor(X0,blue)
| ~ hascolor(X0,red) ),
inference(instantiation,[status(thm)],[c_336]) ).
tcf(c_2052,plain,
! [X0: $i] :
( samecolor(red,green)
| ~ hascolor(X0,green)
| ~ hascolor(X0,red) ),
inference(instantiation,[status(thm)],[c_336]) ).
tcf(c_2053,plain,
! [X0: $i] :
( samecolor(red,white)
| ~ hascolor(X0,white)
| ~ hascolor(X0,red) ),
inference(instantiation,[status(thm)],[c_336]) ).
tcf(c_2054,plain,
! [X0: $i] :
( samecolor(white,blue)
| ~ hascolor(X0,blue)
| ~ hascolor(X0,white) ),
inference(instantiation,[status(thm)],[c_336]) ).
tcf(c_2056,plain,
! [X0: $i] :
( samecolor(white,green)
| ~ hascolor(X0,green)
| ~ hascolor(X0,white) ),
inference(instantiation,[status(thm)],[c_336]) ).
tcf(c_2057,plain,
! [X0: $i] :
( samecolor(green,blue)
| ~ hascolor(X0,blue)
| ~ hascolor(X0,green) ),
inference(instantiation,[status(thm)],[c_336]) ).
tcf(c_2059,plain,
! [X0: $i] :
( sameperson(italian,american)
| ~ hasperson(X0,american)
| ~ hasperson(X0,italian) ),
inference(instantiation,[status(thm)],[c_334]) ).
tcf(c_2063,plain,
! [X0: $i] :
( samepet(guppy,rat)
| ~ haspet(X0,rat)
| ~ haspet(X0,guppy) ),
inference(instantiation,[status(thm)],[c_340]) ).
tcf(c_2065,plain,
! [X0: $i] :
( samepet(guppy,toad)
| ~ haspet(X0,toad)
| ~ haspet(X0,guppy) ),
inference(instantiation,[status(thm)],[c_340]) ).
tcf(c_2067,plain,
! [X0: $i] :
( samedrink(lemonade,vodka)
| ~ hasdrink(X0,vodka)
| ~ hasdrink(X0,lemonade) ),
inference(instantiation,[status(thm)],[c_284]) ).
tcf(c_2069,plain,
! [X0: $i] :
( samedrink(lemonade,coffee)
| ~ hasdrink(X0,coffee)
| ~ hasdrink(X0,lemonade) ),
inference(instantiation,[status(thm)],[c_284]) ).
tcf(c_2070,plain,
! [X0: $i] :
( sameperson(swede,american)
| ~ hasperson(X0,american)
| ~ hasperson(X0,swede) ),
inference(instantiation,[status(thm)],[c_334]) ).
tcf(c_2073,plain,
! [X0: $i] :
( samedrink(coffee,vodka)
| ~ hasdrink(X0,vodka)
| ~ hasdrink(X0,coffee) ),
inference(instantiation,[status(thm)],[c_284]) ).
tcf(c_2074,plain,
! [X0: $i] :
( samedrink(coffee,milk)
| ~ hasdrink(X0,milk)
| ~ hasdrink(X0,coffee) ),
inference(instantiation,[status(thm)],[c_284]) ).
tcf(c_2075,plain,
! [X0: $i] :
( samegame(backgammon,charades)
| ~ hasgame(X0,charades)
| ~ hasgame(X0,backgammon) ),
inference(instantiation,[status(thm)],[c_343]) ).
tcf(c_2076,plain,
! [X0: $i] :
( samegame(backgammon,solitaire)
| ~ hasgame(X0,solitaire)
| ~ hasgame(X0,backgammon) ),
inference(instantiation,[status(thm)],[c_343]) ).
tcf(c_2080,plain,
! [X0: $i] :
( samepet(toad,rat)
| ~ haspet(X0,rat)
| ~ haspet(X0,toad) ),
inference(instantiation,[status(thm)],[c_340]) ).
tcf(c_2081,plain,
! [X0: $i] :
( samepet(toad,camel)
| ~ haspet(X0,camel)
| ~ haspet(X0,toad) ),
inference(instantiation,[status(thm)],[c_340]) ).
tcf(c_2082,plain,
! [X0: $i] :
( samecolor(yellow,blue)
| ~ hascolor(X0,blue)
| ~ hascolor(X0,yellow) ),
inference(instantiation,[status(thm)],[c_336]) ).
tcf(c_2086,plain,
! [X0: $i] :
( samedrink(milk,vodka)
| ~ hasdrink(X0,vodka)
| ~ hasdrink(X0,milk) ),
inference(instantiation,[status(thm)],[c_284]) ).
tcf(c_2087,plain,
! [X0: $i] :
( samegame(solitaire,charades)
| ~ hasgame(X0,charades)
| ~ hasgame(X0,solitaire) ),
inference(instantiation,[status(thm)],[c_343]) ).
tcf(c_2091,plain,
! [X0: $i] :
( samegame(quoits,charades)
| ~ hasgame(X0,charades)
| ~ hasgame(X0,quoits) ),
inference(instantiation,[status(thm)],[c_343]) ).
tcf(c_2096,plain,
( nextto(n1,n2)
| ~ left(n1,n2) ),
inference(instantiation,[status(thm)],[c_267]) ).
tcf(c_2097,plain,
( nextto(n2,n3)
| ~ left(n2,n3) ),
inference(instantiation,[status(thm)],[c_267]) ).
tcf(c_2099,plain,
( nextto(n4,n5)
| ~ left(n4,n5) ),
inference(instantiation,[status(thm)],[c_267]) ).
tcf(c_2106,plain,
( haspet(n2,guppy)
| ~ hasperson(n2,italian) ),
inference(instantiation,[status(thm)],[c_202]) ).
tcf(c_2110,plain,
( hasdrink(n5,lemonade)
| hasdrink(n4,lemonade)
| hasdrink(n3,lemonade)
| hasdrink(n2,lemonade)
| hasdrink(n1,lemonade) ),
inference(instantiation,[status(thm)],[c_286]) ).
tcf(c_2112,plain,
( hascolor(n5,green)
| hascolor(n4,green)
| hascolor(n3,green)
| hascolor(n2,green)
| hascolor(n1,green) ),
inference(instantiation,[status(thm)],[c_260]) ).
tcf(c_2122,plain,
( hasperson(n2,swede)
| ~ hasdrink(n2,coffee) ),
inference(instantiation,[status(thm)],[c_207]) ).
tcf(c_2130,plain,
( hasperson(n2,american)
| ~ hasgame(n2,charades) ),
inference(instantiation,[status(thm)],[c_229]) ).
tcf(c_2133,plain,
( nextto(n2,n1)
| ~ nextto(n1,n2) ),
inference(instantiation,[status(thm)],[c_311]) ).
tcf(c_2138,plain,
( hascolor(n2,blue)
| ~ hasperson(n1,russian)
| ~ nextto(n1,n2)
| ~ samehouse(n1,n1) ),
inference(instantiation,[status(thm)],[c_231]) ).
tcf(c_2140,plain,
( haspet(n2,rat)
| ~ hasgame(n1,racquetball)
| ~ nextto(n1,n2)
| ~ samehouse(n1,n1) ),
inference(instantiation,[status(thm)],[c_224]) ).
tcf(c_2154,plain,
( nextto(n3,n2)
| ~ nextto(n2,n3) ),
inference(instantiation,[status(thm)],[c_311]) ).
tcf(c_2182,plain,
( hasgame(n5,backgammon)
| hasgame(n4,backgammon)
| hasgame(n3,backgammon)
| hasgame(n2,backgammon)
| hasgame(n1,backgammon) ),
inference(instantiation,[status(thm)],[c_316]) ).
tcf(c_2210,plain,
( nextto(n5,n4)
| ~ nextto(n4,n5) ),
inference(instantiation,[status(thm)],[c_311]) ).
tcf(c_2235,plain,
( hasdrink(n3,vodka)
| ~ hasgame(n3,solitaire) ),
inference(instantiation,[status(thm)],[c_226]) ).
tcf(c_2241,plain,
( hascolor(n2,green)
| ~ hascolor(n1,white)
| ~ left(n1,n2) ),
inference(instantiation,[status(thm)],[c_1922]) ).
tcf(c_2246,plain,
( samehouse(n1,n2)
| ~ hasperson(n2,russian)
| ~ hasperson(n1,russian) ),
inference(instantiation,[status(thm)],[c_1946]) ).
tcf(c_2247,plain,
( haspet(n2,guppy)
| hasgame(n2,charades)
| hasdrink(n2,coffee)
| hascolor(n2,red)
| hasperson(n2,russian) ),
inference(instantiation,[status(thm)],[c_680]) ).
tcf(c_2252,plain,
( samehouse(n1,n3)
| ~ hasperson(n3,russian)
| ~ hasperson(n1,russian) ),
inference(instantiation,[status(thm)],[c_1948]) ).
tcf(c_2253,plain,
( haspet(n3,guppy)
| hasgame(n3,charades)
| hasdrink(n3,coffee)
| hascolor(n3,red)
| hasperson(n3,russian) ),
inference(instantiation,[status(thm)],[c_680]) ).
tcf(c_2254,plain,
( samehouse(n1,n4)
| ~ hasperson(n4,russian)
| ~ hasperson(n1,russian) ),
inference(instantiation,[status(thm)],[c_1950]) ).
tcf(c_2255,plain,
( haspet(n4,guppy)
| hasgame(n4,charades)
| hasdrink(n4,coffee)
| hascolor(n4,red)
| hasperson(n4,russian) ),
inference(instantiation,[status(thm)],[c_680]) ).
tcf(c_2275,plain,
( hascolor(n4,green)
| ~ hascolor(n3,white)
| ~ left(n3,n4) ),
inference(instantiation,[status(thm)],[c_200]) ).
tcf(c_2276,plain,
( hascolor(n5,green)
| ~ hascolor(n4,white)
| ~ left(n4,n5) ),
inference(instantiation,[status(thm)],[c_200]) ).
tcf(c_2282,plain,
( hasdrink(n2,vodka)
| ~ hasgame(n2,solitaire) ),
inference(instantiation,[status(thm)],[c_226]) ).
tcf(c_2286,plain,
( samehouse(n1,n3)
| ~ hasdrink(n3,milk)
| ~ hasdrink(n1,milk) ),
inference(instantiation,[status(thm)],[c_2008]) ).
tcf(c_2288,plain,
( hasdrink(n4,vodka)
| ~ hasgame(n4,solitaire) ),
inference(instantiation,[status(thm)],[c_226]) ).
tcf(c_2290,plain,
( hasdrink(n5,vodka)
| ~ hasgame(n5,solitaire) ),
inference(instantiation,[status(thm)],[c_226]) ).
tcf(c_2293,plain,
( samehouse(n2,n3)
| ~ hasdrink(n3,milk)
| ~ hasdrink(n2,milk) ),
inference(instantiation,[status(thm)],[c_2014]) ).
tcf(c_2307,plain,
( haspet(n5,no_pet)
| haspet(n5,rat)
| haspet(n5,camel)
| haspet(n5,toad)
| haspet(n5,guppy) ),
inference(instantiation,[status(thm)],[c_279]) ).
tcf(c_2311,plain,
( samehouse(n1,n5)
| ~ haspet(n5,camel)
| ~ haspet(n1,camel) ),
inference(instantiation,[status(thm)],[c_1992]) ).
tcf(c_2327,plain,
( hascolor(n2,yellow)
| ~ hasgame(n2,racquetball) ),
inference(instantiation,[status(thm)],[c_210]) ).
tcf(c_2357,plain,
( samecolor(red,blue)
| ~ hascolor(n2,blue)
| ~ hascolor(n2,red) ),
inference(instantiation,[status(thm)],[c_2050]) ).
tcf(c_2368,plain,
( samecolor(white,blue)
| ~ hascolor(n2,blue)
| ~ hascolor(n2,white) ),
inference(instantiation,[status(thm)],[c_2054]) ).
tcf(c_2391,plain,
( samepet(guppy,rat)
| ~ haspet(n2,rat)
| ~ haspet(n2,guppy) ),
inference(instantiation,[status(thm)],[c_2063]) ).
tcf(c_2407,plain,
( sameperson(swede,american)
| ~ hasperson(n2,american)
| ~ hasperson(n2,swede) ),
inference(instantiation,[status(thm)],[c_2070]) ).
tcf(c_2415,plain,
( samedrink(coffee,vodka)
| ~ hasdrink(n2,vodka)
| ~ hasdrink(n2,coffee) ),
inference(instantiation,[status(thm)],[c_2073]) ).
tcf(c_2418,plain,
( samedrink(coffee,milk)
| ~ hasdrink(n3,milk)
| ~ hasdrink(n3,coffee) ),
inference(instantiation,[status(thm)],[c_2074]) ).
tcf(c_2435,plain,
( samecolor(yellow,blue)
| ~ hascolor(n2,blue)
| ~ hascolor(n2,yellow) ),
inference(instantiation,[status(thm)],[c_2082]) ).
tcf(c_2445,plain,
( samedrink(milk,vodka)
| ~ hasdrink(n3,vodka)
| ~ hasdrink(n3,milk) ),
inference(instantiation,[status(thm)],[c_2086]) ).
tcf(c_2448,plain,
( samegame(solitaire,charades)
| ~ hasgame(n2,charades)
| ~ hasgame(n2,solitaire) ),
inference(instantiation,[status(thm)],[c_2087]) ).
tcf(c_2470,plain,
( hasgame(n3,racquetball)
| hasdrink(n3,lemonade)
| hascolor(n3,blue)
| hascolor(n3,white)
| hascolor(n3,red) ),
inference(instantiation,[status(thm)],[c_681]) ).
tcf(c_2477,plain,
( hasgame(n5,racquetball)
| hasdrink(n5,lemonade)
| hascolor(n5,blue)
| hascolor(n5,white)
| hascolor(n5,red) ),
inference(instantiation,[status(thm)],[c_681]) ).
tcf(c_2479,plain,
( samehouse(n3,n5)
| ~ hascolor(n5,white)
| ~ hascolor(n3,white) ),
inference(instantiation,[status(thm)],[c_1982]) ).
tcf(c_2496,plain,
( haspet(n3,toad)
| hasgame(n3,charades)
| hasgame(n3,solitaire)
| hasgame(n3,quoits)
| hasgame(n3,racquetball) ),
inference(instantiation,[status(thm)],[c_683]) ).
tcf(c_2516,plain,
( samepet(toad,camel)
| ~ haspet(n3,camel)
| ~ haspet(n3,toad) ),
inference(instantiation,[status(thm)],[c_2081]) ).
tcf(c_2518,plain,
( samepet(guppy,toad)
| ~ haspet(n3,toad)
| ~ haspet(n3,guppy) ),
inference(instantiation,[status(thm)],[c_2065]) ).
tcf(c_2519,plain,
( hasgame(n3,backgammon)
| ~ haspet(n3,toad) ),
inference(instantiation,[status(thm)],[c_208]) ).
tcf(c_2532,plain,
( samedrink(lemonade,coffee)
| ~ hasdrink(n4,coffee)
| ~ hasdrink(n4,lemonade) ),
inference(instantiation,[status(thm)],[c_2069]) ).
tcf(c_2534,plain,
( samedrink(lemonade,vodka)
| ~ hasdrink(n4,vodka)
| ~ hasdrink(n4,lemonade) ),
inference(instantiation,[status(thm)],[c_2067]) ).
tcf(c_2543,plain,
( samecolor(green,blue)
| ~ hascolor(n2,blue)
| ~ hascolor(n2,green) ),
inference(instantiation,[status(thm)],[c_2057]) ).
tcf(c_2594,plain,
! [X0: $i] :
( haspet(n1,camel)
| haspet(X0,camel)
| samehouse(n1,X0)
| ~ hasgame(n2,quoits)
| ~ nextto(n2,n1)
| ~ nextto(n2,X0) ),
inference(instantiation,[status(thm)],[c_216]) ).
tcf(c_2605,plain,
( samegame(quoits,charades)
| ~ hasgame(n2,charades)
| ~ hasgame(n2,quoits) ),
inference(instantiation,[status(thm)],[c_2091]) ).
tcf(c_2614,plain,
( ~ nextto(n3,n2)
| ~ samehouse(n3,n2) ),
inference(instantiation,[status(thm)],[c_308]) ).
tcf(c_2639,plain,
( samepet(toad,rat)
| ~ haspet(n2,rat)
| ~ haspet(n2,toad) ),
inference(instantiation,[status(thm)],[c_2080]) ).
tcf(c_2646,plain,
( haspet(n2,toad)
| ~ hasgame(n2,backgammon) ),
inference(instantiation,[status(thm)],[c_209]) ).
tcf(c_2683,plain,
( hasgame(n4,racquetball)
| ~ haspet(n5,rat)
| ~ nextto(n5,n4)
| ~ samehouse(n5,n5) ),
inference(instantiation,[status(thm)],[c_221]) ).
tcf(c_2726,plain,
( hasperson(n3,italian)
| ~ haspet(n3,guppy) ),
inference(instantiation,[status(thm)],[c_203]) ).
tcf(c_2739,plain,
( samehouse(n3,n5)
| ~ hascolor(n5,red)
| ~ hascolor(n3,red) ),
inference(instantiation,[status(thm)],[c_1982]) ).
tcf(c_2818,plain,
( samehouse(n1,n3)
| ~ hasgame(n3,racquetball)
| ~ hasgame(n1,racquetball) ),
inference(instantiation,[status(thm)],[c_2028]) ).
tcf(c_2823,plain,
( sameperson(englishman,american)
| ~ hasperson(n3,american)
| ~ hasperson(n3,englishman) ),
inference(instantiation,[status(thm)],[c_2046]) ).
tcf(c_2829,plain,
( hasperson(n3,american)
| ~ hasgame(n3,charades) ),
inference(instantiation,[status(thm)],[c_229]) ).
tcf(c_2847,plain,
( haspet(n4,toad)
| ~ hasgame(n4,backgammon) ),
inference(instantiation,[status(thm)],[c_209]) ).
tcf(c_2853,plain,
( samehouse(n3,n5)
| ~ haspet(n5,toad)
| ~ haspet(n3,toad) ),
inference(instantiation,[status(thm)],[c_2002]) ).
tcf(c_2865,plain,
( sameperson(englishman,italian)
| ~ hasperson(n3,italian)
| ~ hasperson(n3,englishman) ),
inference(instantiation,[status(thm)],[c_2049]) ).
tcf(c_2892,plain,
( samegame(backgammon,charades)
| ~ hasgame(n3,charades)
| ~ hasgame(n3,backgammon) ),
inference(instantiation,[status(thm)],[c_2075]) ).
tcf(c_2905,plain,
( samehouse(n1,n4)
| ~ hascolor(n4,green)
| ~ hascolor(n1,green) ),
inference(instantiation,[status(thm)],[c_1970]) ).
tcf(c_2930,plain,
( hascolor(n3,green)
| ~ hasdrink(n3,lemonade) ),
inference(instantiation,[status(thm)],[c_204]) ).
tcf(c_2934,plain,
( hascolor(n5,green)
| ~ hasdrink(n5,lemonade) ),
inference(instantiation,[status(thm)],[c_204]) ).
tcf(c_2938,plain,
( samehouse(n1,n5)
| ~ hascolor(n5,green)
| ~ hascolor(n1,green) ),
inference(instantiation,[status(thm)],[c_1972]) ).
tcf(c_2940,plain,
( hascolor(n2,green)
| ~ hasdrink(n2,lemonade) ),
inference(instantiation,[status(thm)],[c_204]) ).
tcf(c_2964,plain,
( samecolor(red,green)
| ~ hascolor(n4,green)
| ~ hascolor(n4,red) ),
inference(instantiation,[status(thm)],[c_2052]) ).
tcf(c_2965,plain,
( samecolor(red,green)
| ~ hascolor(n5,green)
| ~ hascolor(n5,red) ),
inference(instantiation,[status(thm)],[c_2052]) ).
tcf(c_3028,plain,
! [X0: $i] :
( left(n5,X0)
| ~ hascolor(n5,white)
| ~ hasdrink(X0,lemonade) ),
inference(instantiation,[status(thm)],[c_679]) ).
tcf(c_3029,plain,
( samecolor(white,green)
| ~ hascolor(n5,green)
| ~ hascolor(n5,white) ),
inference(instantiation,[status(thm)],[c_2056]) ).
tcf(c_3030,plain,
( left(n5,n1)
| ~ hasdrink(n1,lemonade)
| ~ hascolor(n5,white) ),
inference(instantiation,[status(thm)],[c_3028]) ).
tcf(c_3035,plain,
! [X0: $i] :
( nextto(X0,n3)
| ~ hascolor(n3,blue)
| ~ hasperson(X0,russian) ),
inference(instantiation,[status(thm)],[c_233]) ).
tcf(c_3036,plain,
( nextto(n1,n3)
| ~ hascolor(n3,blue)
| ~ hasperson(n1,russian) ),
inference(instantiation,[status(thm)],[c_3035]) ).
tcf(c_3085,plain,
( samehouse(n1,n4)
| ~ hasgame(n4,racquetball)
| ~ hasgame(n1,racquetball) ),
inference(instantiation,[status(thm)],[c_2030]) ).
tcf(c_3109,plain,
( hasgame(n2,solitaire)
| hasdrink(n2,unknown_drink)
| hasdrink(n2,milk)
| hasdrink(n2,coffee)
| hasdrink(n2,lemonade) ),
inference(instantiation,[status(thm)],[c_682]) ).
tcf(c_3130,plain,
( ~ iPr_def_11
| ~ hasdrink(n4,lemonade) ),
inference(instantiation,[status(thm)],[c_1853]) ).
tcf(c_3133,plain,
( hasdrink(n4,lemonade)
| ~ hascolor(n4,green) ),
inference(instantiation,[status(thm)],[c_205]) ).
tcf(c_3134,plain,
( ~ iPr_def_11
| ~ hasdrink(n4,vodka) ),
inference(instantiation,[status(thm)],[c_1853]) ).
tcf(c_3157,plain,
( samepet(guppy,toad)
| ~ haspet(n4,toad)
| ~ haspet(n4,guppy) ),
inference(instantiation,[status(thm)],[c_2065]) ).
tcf(c_3181,plain,
( haspet(n2,toad)
| hasgame(n2,charades)
| hasgame(n2,solitaire)
| hasgame(n2,quoits)
| hasgame(n2,racquetball) ),
inference(instantiation,[status(thm)],[c_683]) ).
tcf(c_3248,plain,
! [X0: $i] :
( samehouse(n3,n2)
| ~ hasgame(n3,X0)
| ~ hasgame(n2,X0) ),
inference(instantiation,[status(thm)],[c_297]) ).
tcf(c_3348,plain,
( hasperson(n5,italian)
| ~ haspet(n5,guppy) ),
inference(instantiation,[status(thm)],[c_203]) ).
tcf(c_3362,plain,
( haspet(n5,toad)
| hasgame(n5,charades)
| hasgame(n5,solitaire)
| hasgame(n5,quoits)
| hasgame(n5,racquetball) ),
inference(instantiation,[status(thm)],[c_683]) ).
tcf(c_3501,plain,
! [X0: $i] :
( nextto(X0,n5)
| ~ hascolor(n5,blue)
| ~ hasperson(X0,russian) ),
inference(instantiation,[status(thm)],[c_233]) ).
tcf(c_3502,plain,
( nextto(n1,n5)
| ~ hascolor(n5,blue)
| ~ hasperson(n1,russian) ),
inference(instantiation,[status(thm)],[c_3501]) ).
tcf(c_3511,plain,
samehouse(n5,n5),
inference(instantiation,[status(thm)],[c_309]) ).
tcf(c_3527,plain,
( samedrink(lemonade,vodka)
| ~ hasdrink(n5,vodka)
| ~ hasdrink(n5,lemonade) ),
inference(instantiation,[status(thm)],[c_2067]) ).
tcf(c_3533,plain,
( samegame(backgammon,solitaire)
| ~ hasgame(n5,solitaire)
| ~ hasgame(n5,backgammon) ),
inference(instantiation,[status(thm)],[c_2076]) ).
tcf(c_3566,plain,
( samehouse(n1,n2)
| ~ hasdrink(n2,unknown_drink)
| ~ hasdrink(n1,unknown_drink) ),
inference(instantiation,[status(thm)],[c_2006]) ).
tcf(c_3574,plain,
( samecolor(red,white)
| ~ hascolor(n3,white)
| ~ hascolor(n3,red) ),
inference(instantiation,[status(thm)],[c_2053]) ).
tcf(c_3575,plain,
( hasperson(n3,englishman)
| ~ hascolor(n3,red) ),
inference(instantiation,[status(thm)],[c_198]) ).
tcf(c_3648,plain,
( samehouse(n2,n5)
| ~ hasgame(n5,quoits)
| ~ hasgame(n2,quoits) ),
inference(instantiation,[status(thm)],[c_2038]) ).
tcf(c_3666,plain,
( ~ iPr_def_19
| ~ hasgame(n3,backgammon) ),
inference(instantiation,[status(thm)],[c_1861]) ).
tcf(c_3757,plain,
( hascolor(n5,yellow)
| ~ hasgame(n5,racquetball) ),
inference(instantiation,[status(thm)],[c_210]) ).
tcf(c_3761,plain,
( samehouse(n1,n5)
| ~ hascolor(n5,yellow)
| ~ hascolor(n1,yellow) ),
inference(instantiation,[status(thm)],[c_1972]) ).
tcf(c_3918,plain,
( haspet(n2,guppy)
| hasgame(n2,charades)
| hascolor(n2,red)
| hasperson(n2,russian)
| ~ iPr_def_12 ),
inference(superposition,[status(thm)],[c_680,c_1854]) ).
tcf(c_4072,plain,
( hasgame(n1,racquetball)
| hascolor(n1,blue)
| hascolor(n1,white)
| hascolor(n1,red)
| ~ iPr_def_14 ),
inference(superposition,[status(thm)],[c_681,c_1856]) ).
tcf(c_4074,plain,
( hasgame(n4,racquetball)
| hascolor(n4,blue)
| hascolor(n4,white)
| hascolor(n4,red)
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_681,c_1853]) ).
tcf(c_4075,plain,
( hasgame(n5,racquetball)
| hascolor(n5,blue)
| hascolor(n5,white)
| hascolor(n5,red)
| ~ iPr_def_13 ),
inference(superposition,[status(thm)],[c_681,c_1855]) ).
tcf(c_4108,plain,
( hasgame(n4,racquetball)
| hascolor(n4,blue)
| hascolor(n4,white)
| hascolor(n4,red)
| ~ iPr_def_11 ),
inference(superposition,[status(thm)],[c_681,c_1853]) ).
tcf(c_4280,plain,
( hasgame(n1,solitaire)
| hasdrink(n1,milk)
| hasdrink(n1,coffee)
| hasdrink(n1,lemonade)
| ~ iPr_def_14 ),
inference(superposition,[status(thm)],[c_682,c_1856]) ).
tcf(c_4431,plain,
( ~ iPr_def_13
| ~ hasdrink(n5,vodka) ),
inference(instantiation,[status(thm)],[c_1855]) ).
tcf(c_4482,plain,
~ iPr_def_34,
inference(superposition,[status(thm)],[c_250,c_1876]) ).
tcf(c_4485,plain,
( iPr_def_13
| iPr_def_12
| iPr_def_11
| iPr_def_15
| iPr_def_16
| iPr_def_17
| iPr_def_18
| iPr_def_19
| iPr_def_20
| iPr_def_21
| iPr_def_22
| iPr_def_23
| iPr_def_24
| iPr_def_25
| iPr_def_26
| iPr_def_27
| iPr_def_28
| iPr_def_29
| iPr_def_30
| iPr_def_31
| iPr_def_32
| iPr_def_33 ),
inference(global_subsumption_just,[status(thm)],[c_1877,c_350,c_250,c_249,c_239,c_314,c_351,c_273,c_359,c_362,c_365,c_368,c_370,c_1369,c_1409,c_1509,c_1693,c_1877,c_1903,c_2096,c_2138,c_2241,c_2286,c_2543,c_4072,c_4280,c_4482]) ).
tcf(c_4486,negated_conjecture,
( iPr_def_33
| iPr_def_32
| iPr_def_31
| iPr_def_30
| iPr_def_29
| iPr_def_28
| iPr_def_27
| iPr_def_26
| iPr_def_25
| iPr_def_24
| iPr_def_23
| iPr_def_22
| iPr_def_21
| iPr_def_20
| iPr_def_19
| iPr_def_18
| iPr_def_17
| iPr_def_16
| iPr_def_15
| iPr_def_13
| iPr_def_12
| iPr_def_11 ),
inference(renaming,[status(thm)],[c_4485]) ).
tcf(c_4577,plain,
( haspet(n2,guppy)
| ~ iPr_def_12 ),
inference(global_subsumption_just,[status(thm)],[c_3918,c_350,c_250,c_249,c_242,c_241,c_239,c_332,c_330,c_329,c_322,c_314,c_313,c_351,c_292,c_281,c_273,c_270,c_262,c_353,c_356,c_358,c_359,c_362,c_365,c_368,c_370,c_377,c_380,c_687,c_1369,c_1409,c_1509,c_1693,c_1920,c_2096,c_2122,c_2130,c_2140,c_2138,c_2241,c_2246,c_2275,c_2276,c_2286,c_2293,c_2357,c_2368,c_2391,c_2407,c_2448,c_2543,c_2905,c_2938,c_2940,c_3030,c_3109,c_3566,c_3918]) ).
tcf(c_4579,plain,
~ iPr_def_12,
inference(global_subsumption_just,[status(thm)],[c_4577,c_350,c_250,c_242,c_241,c_239,c_332,c_313,c_351,c_281,c_273,c_270,c_353,c_358,c_368,c_370,c_380,c_687,c_1369,c_1920,c_2096,c_2140,c_2138,c_2241,c_2275,c_2276,c_2368,c_2391,c_2543,c_2905,c_2938,c_3030,c_4577]) ).
tcf(c_4581,plain,
( iPr_def_33
| iPr_def_32
| iPr_def_31
| iPr_def_30
| iPr_def_29
| iPr_def_28
| iPr_def_27
| iPr_def_26
| iPr_def_25
| iPr_def_24
| iPr_def_23
| iPr_def_22
| iPr_def_21
| iPr_def_20
| iPr_def_19
| iPr_def_18
| iPr_def_17
| iPr_def_16
| iPr_def_15
| iPr_def_13
| iPr_def_11 ),
inference(backward_subsumption_resolution,[status(thm)],[c_4486,c_4579]) ).
tcf(c_4732,plain,
( samehouse(n3,n4)
| ~ hasgame(n4,charades)
| ~ hasgame(n3,charades) ),
inference(instantiation,[status(thm)],[c_2040]) ).
tcf(c_4810,plain,
( hasgame(n2,charades)
| hasgame(n2,solitaire)
| hasgame(n2,quoits)
| hasgame(n2,racquetball)
| ~ iPr_def_27 ),
inference(superposition,[status(thm)],[c_683,c_1869]) ).
tcf(c_4811,plain,
( hasgame(n3,charades)
| hasgame(n3,solitaire)
| hasgame(n3,quoits)
| hasgame(n3,racquetball)
| ~ iPr_def_29 ),
inference(superposition,[status(thm)],[c_683,c_1871]) ).
tcf(c_4812,plain,
( hasgame(n4,charades)
| hasgame(n4,solitaire)
| hasgame(n4,quoits)
| hasgame(n4,racquetball)
| ~ iPr_def_31 ),
inference(superposition,[status(thm)],[c_683,c_1873]) ).
tcf(c_4813,plain,
( hasgame(n5,charades)
| hasgame(n5,solitaire)
| hasgame(n5,quoits)
| hasgame(n5,racquetball)
| ~ iPr_def_33 ),
inference(superposition,[status(thm)],[c_683,c_1875]) ).
tcf(c_5116,plain,
( samehouse(n3,n2)
| ~ hasgame(n3,quoits)
| ~ hasgame(n2,quoits) ),
inference(instantiation,[status(thm)],[c_3248]) ).
tcf(c_5208,plain,
hasgame(n1,racquetball),
inference(global_subsumption_just,[status(thm)],[c_4072,c_350,c_250,c_242,c_241,c_239,c_332,c_313,c_351,c_273,c_270,c_353,c_358,c_368,c_370,c_380,c_687,c_1369,c_1920,c_2096,c_2138,c_2241,c_2275,c_2276,c_2368,c_2543,c_2905,c_2938,c_3030]) ).
tcf(c_5210,plain,
~ iPr_def_15,
inference(superposition,[status(thm)],[c_5208,c_1857]) ).
tcf(c_5227,plain,
~ iPr_def_11,
inference(global_subsumption_just,[status(thm)],[c_4074,c_350,c_250,c_249,c_242,c_241,c_240,c_239,c_332,c_330,c_329,c_322,c_321,c_314,c_313,c_351,c_295,c_292,c_289,c_281,c_273,c_270,c_262,c_353,c_356,c_358,c_359,c_362,c_365,c_368,c_370,c_377,c_380,c_687,c_1369,c_1409,c_1509,c_1693,c_1907,c_1920,c_1929,c_2096,c_2110,c_2122,c_2130,c_2140,c_2138,c_2241,c_2246,c_2247,c_2275,c_2276,c_2286,c_2293,c_2357,c_2368,c_2391,c_2407,c_2415,c_2445,c_2448,c_2543,c_2905,c_2930,c_2938,c_2940,c_3030,c_3109,c_3130,c_3134,c_3527,c_3566]) ).
tcf(c_5229,plain,
( hascolor(n5,white)
| ~ iPr_def_13 ),
inference(global_subsumption_just,[status(thm)],[c_4075,c_350,c_250,c_249,c_242,c_241,c_240,c_239,c_332,c_330,c_329,c_322,c_321,c_318,c_314,c_313,c_351,c_295,c_292,c_289,c_281,c_273,c_272,c_270,c_264,c_262,c_245,c_353,c_356,c_358,c_359,c_362,c_365,c_368,c_370,c_377,c_380,c_687,c_1369,c_1409,c_1509,c_1693,c_1907,c_1908,c_1920,c_1929,c_2096,c_2112,c_2122,c_2130,c_2140,c_2138,c_2241,c_2246,c_2247,c_2275,c_2276,c_2286,c_2293,c_2357,c_2368,c_2391,c_2407,c_2415,c_2445,c_2448,c_2479,c_2534,c_2543,c_2905,c_2938,c_2940,c_2965,c_3029,c_3030,c_3109,c_3133,c_3502,c_3566,c_3757,c_3761,c_4075,c_4431]) ).
tcf(c_5231,plain,
~ iPr_def_13,
inference(global_subsumption_just,[status(thm)],[c_5229,c_350,c_250,c_242,c_241,c_240,c_239,c_332,c_318,c_313,c_351,c_273,c_272,c_270,c_353,c_358,c_359,c_368,c_370,c_380,c_687,c_1369,c_1509,c_1907,c_1908,c_1920,c_2096,c_2112,c_2138,c_2241,c_2275,c_2276,c_2368,c_2479,c_2543,c_2905,c_2938,c_3029,c_3030,c_5229]) ).
tcf(c_5249,plain,
( hasgame(n2,charades)
| hasgame(n2,quoits) ),
inference(global_subsumption_just,[status(thm)],[c_4810,c_350,c_250,c_249,c_242,c_241,c_239,c_332,c_330,c_329,c_322,c_314,c_313,c_351,c_306,c_304,c_295,c_292,c_281,c_273,c_270,c_262,c_353,c_356,c_358,c_359,c_362,c_365,c_368,c_370,c_377,c_380,c_687,c_1369,c_1409,c_1509,c_1693,c_1920,c_2096,c_2122,c_2130,c_2140,c_2138,c_2241,c_2246,c_2247,c_2275,c_2276,c_2282,c_2286,c_2293,c_2327,c_2357,c_2368,c_2391,c_2407,c_2415,c_2435,c_2448,c_2543,c_2639,c_2905,c_2938,c_2940,c_3030,c_3109,c_3181,c_3566]) ).
tcf(c_5251,plain,
hasgame(n2,quoits),
inference(global_subsumption_just,[status(thm)],[c_5249,c_350,c_250,c_249,c_242,c_241,c_239,c_332,c_330,c_329,c_322,c_314,c_313,c_351,c_306,c_304,c_295,c_292,c_281,c_273,c_270,c_262,c_353,c_356,c_358,c_359,c_362,c_365,c_368,c_370,c_377,c_380,c_687,c_1369,c_1409,c_1509,c_1693,c_1920,c_2096,c_2122,c_2130,c_2140,c_2138,c_2241,c_2246,c_2247,c_2275,c_2276,c_2282,c_2286,c_2293,c_2327,c_2357,c_2368,c_2391,c_2407,c_2415,c_2435,c_2448,c_2543,c_2639,c_2905,c_2938,c_2940,c_3030,c_3109,c_3181,c_3566]) ).
tcf(c_5253,plain,
~ iPr_def_17,
inference(superposition,[status(thm)],[c_5251,c_1859]) ).
tcf(c_5254,plain,
~ iPr_def_29,
inference(global_subsumption_just,[status(thm)],[c_4811,c_350,c_250,c_249,c_242,c_241,c_240,c_239,c_332,c_331,c_330,c_329,c_322,c_321,c_314,c_313,c_351,c_306,c_304,c_300,c_299,c_295,c_292,c_291,c_289,c_283,c_281,c_273,c_270,c_264,c_262,c_253,c_243,c_353,c_356,c_358,c_359,c_362,c_365,c_368,c_370,c_377,c_380,c_687,c_1369,c_1409,c_1509,c_1653,c_1693,c_1907,c_1920,c_1939,c_2096,c_2097,c_2122,c_2130,c_2140,c_2138,c_2154,c_2182,c_2235,c_2241,c_2246,c_2247,c_2254,c_2255,c_2275,c_2276,c_2282,c_2286,c_2288,c_2293,c_2327,c_2357,c_2368,c_2391,c_2407,c_2415,c_2435,c_2445,c_2448,c_2470,c_2534,c_2532,c_2543,c_2614,c_2639,c_2646,c_2818,c_2823,c_2829,c_2847,c_2892,c_2905,c_2930,c_2938,c_2940,c_2964,c_3030,c_3036,c_3109,c_3133,c_3157,c_3181,c_3533,c_3566,c_3575,c_4732,c_4811,c_5116]) ).
tcf(c_5256,plain,
( hasgame(n4,charades)
| hasgame(n4,solitaire) ),
inference(global_subsumption_just,[status(thm)],[c_4812,c_350,c_250,c_249,c_242,c_241,c_240,c_239,c_332,c_331,c_330,c_329,c_322,c_321,c_318,c_314,c_313,c_351,c_306,c_304,c_300,c_299,c_296,c_295,c_292,c_291,c_289,c_283,c_281,c_273,c_272,c_270,c_264,c_262,c_253,c_245,c_243,c_353,c_356,c_358,c_359,c_362,c_365,c_368,c_370,c_377,c_380,c_687,c_1369,c_1409,c_1509,c_1653,c_1693,c_1907,c_1908,c_1920,c_1939,c_2096,c_2097,c_2112,c_2122,c_2130,c_2140,c_2138,c_2154,c_2182,c_2235,c_2241,c_2246,c_2247,c_2252,c_2253,c_2254,c_2255,c_2275,c_2276,c_2282,c_2286,c_2288,c_2290,c_2293,c_2327,c_2357,c_2368,c_2391,c_2407,c_2415,c_2418,c_2435,c_2445,c_2448,c_2470,c_2477,c_2479,c_2496,c_2518,c_2534,c_2532,c_2543,c_2614,c_2639,c_2646,c_2739,c_2818,c_2823,c_2829,c_2847,c_2892,c_2905,c_2930,c_2938,c_2940,c_2964,c_3029,c_3030,c_3036,c_3109,c_3133,c_3157,c_3181,c_3502,c_3527,c_3533,c_3566,c_3575,c_3757,c_3761,c_4732,c_5116]) ).
tcf(c_5258,plain,
hasgame(n4,solitaire),
inference(global_subsumption_just,[status(thm)],[c_5256,c_350,c_250,c_249,c_242,c_241,c_240,c_239,c_332,c_331,c_330,c_329,c_322,c_321,c_318,c_314,c_313,c_351,c_306,c_304,c_300,c_299,c_296,c_295,c_292,c_291,c_289,c_283,c_281,c_273,c_272,c_270,c_264,c_262,c_253,c_245,c_243,c_353,c_356,c_358,c_359,c_362,c_365,c_368,c_370,c_377,c_380,c_687,c_1369,c_1409,c_1509,c_1653,c_1693,c_1907,c_1908,c_1920,c_1939,c_2096,c_2097,c_2112,c_2122,c_2130,c_2140,c_2138,c_2154,c_2182,c_2235,c_2241,c_2246,c_2247,c_2252,c_2253,c_2254,c_2255,c_2275,c_2276,c_2282,c_2286,c_2288,c_2290,c_2293,c_2327,c_2357,c_2368,c_2391,c_2407,c_2415,c_2418,c_2435,c_2445,c_2448,c_2470,c_2477,c_2479,c_2496,c_2518,c_2534,c_2532,c_2543,c_2614,c_2639,c_2646,c_2739,c_2818,c_2823,c_2829,c_2847,c_2892,c_2905,c_2930,c_2938,c_2940,c_2964,c_3029,c_3030,c_3036,c_3109,c_3133,c_3157,c_3181,c_3502,c_3527,c_3533,c_3566,c_3575,c_3757,c_3761,c_4732,c_5116]) ).
tcf(c_5260,plain,
~ iPr_def_21,
inference(superposition,[status(thm)],[c_5258,c_1863]) ).
tcf(c_5269,plain,
hasgame(n5,charades),
inference(global_subsumption_just,[status(thm)],[c_4813,c_350,c_250,c_249,c_242,c_241,c_240,c_239,c_332,c_331,c_330,c_329,c_322,c_321,c_319,c_318,c_314,c_313,c_351,c_306,c_304,c_300,c_299,c_296,c_295,c_292,c_291,c_289,c_283,c_281,c_273,c_272,c_270,c_264,c_262,c_253,c_245,c_243,c_353,c_356,c_358,c_359,c_362,c_365,c_368,c_370,c_377,c_380,c_687,c_1369,c_1409,c_1509,c_1653,c_1693,c_1907,c_1908,c_1920,c_1939,c_2096,c_2097,c_2112,c_2122,c_2130,c_2140,c_2138,c_2154,c_2182,c_2235,c_2241,c_2246,c_2247,c_2252,c_2253,c_2254,c_2255,c_2275,c_2276,c_2282,c_2286,c_2288,c_2290,c_2293,c_2327,c_2357,c_2368,c_2391,c_2407,c_2415,c_2418,c_2435,c_2445,c_2448,c_2470,c_2477,c_2479,c_2496,c_2518,c_2534,c_2532,c_2543,c_2614,c_2639,c_2646,c_2739,c_2818,c_2823,c_2829,c_2847,c_2853,c_2892,c_2905,c_2930,c_2938,c_2940,c_2964,c_3029,c_3030,c_3036,c_3109,c_3133,c_3157,c_3181,c_3362,c_3502,c_3527,c_3533,c_3566,c_3575,c_3648,c_3757,c_3761,c_4732,c_5116]) ).
tcf(c_5271,plain,
~ iPr_def_23,
inference(superposition,[status(thm)],[c_5269,c_1865]) ).
tcf(c_5272,plain,
( iPr_def_33
| iPr_def_32
| iPr_def_31
| iPr_def_30
| iPr_def_22
| iPr_def_18
| iPr_def_16
| iPr_def_20
| iPr_def_24
| iPr_def_25
| iPr_def_26
| iPr_def_27
| iPr_def_28 ),
inference(global_subsumption_just,[status(thm)],[c_4581,c_350,c_250,c_249,c_241,c_240,c_239,c_321,c_314,c_289,c_270,c_253,c_243,c_359,c_362,c_365,c_1409,c_1509,c_1693,c_1877,c_1903,c_1907,c_2096,c_2097,c_2138,c_2154,c_2235,c_2275,c_2286,c_2288,c_2368,c_2445,c_2470,c_2496,c_2519,c_2534,c_2614,c_2818,c_2823,c_2829,c_2930,c_3036,c_3133,c_3575,c_3666,c_4280,c_4482,c_4579,c_5116,c_5208,c_5210,c_5227,c_5231,c_5251,c_5253,c_5254,c_5258,c_5260,c_5271]) ).
tcf(c_5273,plain,
( iPr_def_33
| iPr_def_32
| iPr_def_31
| iPr_def_30
| iPr_def_28
| iPr_def_27
| iPr_def_26
| iPr_def_25
| iPr_def_24
| iPr_def_22
| iPr_def_20
| iPr_def_18
| iPr_def_16 ),
inference(renaming,[status(thm)],[c_5272]) ).
tcf(c_5344,plain,
! [X0: $i] :
( hasgame(X0,racquetball)
| hascolor(X0,blue)
| hascolor(X0,green)
| hascolor(X0,white)
| hascolor(X0,red) ),
inference(superposition,[status(thm)],[c_681,c_204]) ).
tcf(c_5386,plain,
hascolor(n1,yellow),
inference(superposition,[status(thm)],[c_5208,c_210]) ).
tcf(c_5387,plain,
~ iPr_def_24,
inference(superposition,[status(thm)],[c_5386,c_1866]) ).
tcf(c_5388,plain,
( iPr_def_33
| iPr_def_32
| iPr_def_31
| iPr_def_30
| iPr_def_28
| iPr_def_27
| iPr_def_26
| iPr_def_25
| iPr_def_22
| iPr_def_20
| iPr_def_18
| iPr_def_16 ),
inference(backward_subsumption_resolution,[status(thm)],[c_5273,c_5387]) ).
tcf(c_5452,plain,
( hasgame(n3,racquetball)
| hascolor(n3,blue)
| hascolor(n3,green)
| hascolor(n3,white)
| ~ iPr_def_20 ),
inference(superposition,[status(thm)],[c_5344,c_1862]) ).
tcf(c_5454,plain,
( hasgame(n5,racquetball)
| hascolor(n5,blue)
| hascolor(n5,green)
| hascolor(n5,white)
| ~ iPr_def_16 ),
inference(superposition,[status(thm)],[c_5344,c_1858]) ).
tcf(c_5488,plain,
hasperson(n5,american),
inference(superposition,[status(thm)],[c_5269,c_229]) ).
tcf(c_5493,plain,
nextto(n1,n2),
inference(superposition,[status(thm)],[c_239,c_267]) ).
tcf(c_5545,plain,
hascolor(n4,white),
inference(global_subsumption_just,[status(thm)],[c_4108,c_350,c_250,c_249,c_242,c_241,c_240,c_239,c_332,c_331,c_330,c_329,c_322,c_321,c_318,c_314,c_313,c_351,c_306,c_304,c_300,c_299,c_296,c_295,c_292,c_291,c_289,c_283,c_281,c_273,c_272,c_270,c_265,c_264,c_262,c_253,c_243,c_353,c_356,c_358,c_359,c_362,c_365,c_368,c_370,c_377,c_380,c_687,c_1369,c_1409,c_1509,c_1653,c_1693,c_1907,c_1908,c_1920,c_1939,c_2096,c_2097,c_2112,c_2122,c_2130,c_2140,c_2138,c_2154,c_2182,c_2235,c_2241,c_2246,c_2247,c_2252,c_2253,c_2254,c_2255,c_2275,c_2276,c_2282,c_2286,c_2288,c_2293,c_2327,c_2357,c_2368,c_2391,c_2407,c_2415,c_2418,c_2435,c_2445,c_2448,c_2470,c_2479,c_2496,c_2518,c_2534,c_2532,c_2543,c_2614,c_2639,c_2646,c_2818,c_2823,c_2829,c_2847,c_2892,c_2905,c_2930,c_2938,c_2940,c_2964,c_3029,c_3030,c_3036,c_3109,c_3133,c_3157,c_3181,c_3533,c_3566,c_3575,c_3574,c_4732,c_5116]) ).
tcf(c_5547,plain,
~ iPr_def_18,
inference(superposition,[status(thm)],[c_5545,c_1860]) ).
tcf(c_5552,plain,
( haspet(n3,camel)
| haspet(n1,camel)
| samehouse(n1,n3)
| ~ hasgame(n2,quoits)
| ~ nextto(n2,n3)
| ~ nextto(n2,n1) ),
inference(instantiation,[status(thm)],[c_2594]) ).
tcf(c_5845,plain,
~ iPr_def_26,
inference(superposition,[status(thm)],[c_5488,c_1868]) ).
tcf(c_5846,plain,
( iPr_def_33
| iPr_def_32
| iPr_def_31
| iPr_def_30
| iPr_def_28
| iPr_def_27
| iPr_def_25
| iPr_def_22
| iPr_def_20
| iPr_def_18
| iPr_def_16 ),
inference(backward_subsumption_resolution,[status(thm)],[c_5388,c_5845]) ).
tcf(c_5868,plain,
( hascolor(n2,blue)
| ~ hasperson(n1,russian)
| ~ samehouse(n1,n1) ),
inference(superposition,[status(thm)],[c_5493,c_231]) ).
tcf(c_5870,plain,
hascolor(n2,blue),
inference(forward_subsumption_resolution,[status(thm)],[c_5868,c_250,c_309]) ).
tcf(c_6113,plain,
( sameperson(italian,american)
| ~ hasperson(n5,american)
| ~ hasperson(n5,italian) ),
inference(instantiation,[status(thm)],[c_2059]) ).
tcf(c_6128,plain,
hascolor(n5,green),
inference(global_subsumption_just,[status(thm)],[c_5454,c_350,c_250,c_249,c_242,c_241,c_240,c_239,c_332,c_331,c_330,c_329,c_322,c_321,c_318,c_314,c_313,c_351,c_306,c_304,c_300,c_299,c_296,c_295,c_292,c_291,c_289,c_283,c_281,c_273,c_272,c_270,c_264,c_262,c_253,c_245,c_243,c_353,c_356,c_358,c_359,c_362,c_365,c_368,c_370,c_377,c_380,c_687,c_1369,c_1409,c_1509,c_1653,c_1693,c_1907,c_1908,c_1920,c_1939,c_2096,c_2097,c_2112,c_2122,c_2130,c_2140,c_2138,c_2154,c_2182,c_2235,c_2241,c_2246,c_2247,c_2252,c_2253,c_2254,c_2255,c_2275,c_2276,c_2282,c_2286,c_2288,c_2293,c_2327,c_2357,c_2368,c_2391,c_2407,c_2415,c_2418,c_2435,c_2445,c_2448,c_2470,c_2477,c_2479,c_2496,c_2518,c_2534,c_2532,c_2543,c_2614,c_2639,c_2646,c_2739,c_2818,c_2823,c_2829,c_2847,c_2892,c_2905,c_2930,c_2934,c_2938,c_2940,c_2964,c_3029,c_3030,c_3036,c_3109,c_3133,c_3157,c_3181,c_3502,c_3533,c_3566,c_3575,c_3757,c_3761,c_4732,c_5116]) ).
tcf(c_6131,plain,
~ iPr_def_16,
inference(superposition,[status(thm)],[c_6128,c_1858]) ).
tcf(c_6133,plain,
( iPr_def_33
| iPr_def_32
| iPr_def_31
| iPr_def_30
| iPr_def_28
| iPr_def_27
| iPr_def_25
| iPr_def_22 ),
inference(global_subsumption_just,[status(thm)],[c_5846,c_350,c_250,c_241,c_240,c_239,c_314,c_289,c_270,c_243,c_1907,c_2096,c_2138,c_2275,c_2288,c_2368,c_2534,c_2818,c_3036,c_3133,c_5208,c_5258,c_5273,c_5387,c_5452,c_5547,c_5845,c_6131]) ).
tcf(c_6151,plain,
~ iPr_def_22,
inference(superposition,[status(thm)],[c_5870,c_1864]) ).
tcf(c_6152,plain,
( iPr_def_33
| iPr_def_32
| iPr_def_31
| iPr_def_30
| iPr_def_28
| iPr_def_27
| iPr_def_25 ),
inference(backward_subsumption_resolution,[status(thm)],[c_6133,c_6151]) ).
tcf(c_6726,plain,
( ~ iPr_def_32
| ~ hasperson(n2,swede) ),
inference(instantiation,[status(thm)],[c_1874]) ).
tcf(c_6799,plain,
( ~ iPr_def_25
| ~ haspet(n1,camel) ),
inference(instantiation,[status(thm)],[c_1867]) ).
tcf(c_6849,plain,
( ~ iPr_def_27
| ~ haspet(n2,rat) ),
inference(instantiation,[status(thm)],[c_1869]) ).
tcf(c_6879,plain,
( iPr_def_33
| iPr_def_28
| iPr_def_30
| iPr_def_31 ),
inference(global_subsumption_just,[status(thm)],[c_6152,c_350,c_250,c_249,c_241,c_240,c_239,c_330,c_326,c_321,c_314,c_305,c_289,c_281,c_270,c_262,c_253,c_243,c_1907,c_2096,c_2097,c_2122,c_2140,c_2138,c_2133,c_2154,c_2235,c_2246,c_2247,c_2275,c_2288,c_2357,c_2368,c_2391,c_2445,c_2470,c_2496,c_2516,c_2534,c_2605,c_2614,c_2818,c_2823,c_2829,c_2930,c_3036,c_3133,c_3575,c_5116,c_5208,c_5251,c_5258,c_5552,c_6133,c_6151,c_6726,c_6799,c_6849]) ).
tcf(c_6880,plain,
( iPr_def_33
| iPr_def_31
| iPr_def_30
| iPr_def_28 ),
inference(renaming,[status(thm)],[c_6879]) ).
tcf(c_6894,plain,
( ~ iPr_def_28
| ~ hasperson(n4,italian) ),
inference(instantiation,[status(thm)],[c_1870]) ).
tcf(c_6900,plain,
( ~ iPr_def_30
| ~ hasperson(n3,englishman) ),
inference(instantiation,[status(thm)],[c_1872]) ).
tcf(c_6903,plain,
( ~ iPr_def_31
| ~ haspet(n4,guppy) ),
inference(instantiation,[status(thm)],[c_1873]) ).
tcf(c_6914,plain,
( ~ iPr_def_33
| ~ haspet(n5,no_pet) ),
inference(instantiation,[status(thm)],[c_1875]) ).
tcf(c_6915,plain,
$false,
inference(prop_impl_just,[status(thm)],[c_6914,c_6903,c_6900,c_6894,c_6880,c_6113,c_5552,c_5488,c_5258,c_5251,c_5208,c_5116,c_3575,c_3511,c_3348,c_3133,c_3085,c_3036,c_2930,c_2865,c_2853,c_2829,c_2823,c_2818,c_2726,c_2683,c_2614,c_2534,c_2516,c_2496,c_2470,c_2445,c_2391,c_2368,c_2311,c_2307,c_2288,c_2275,c_2235,c_2210,c_2154,c_2133,c_2138,c_2140,c_2106,c_2099,c_2097,c_2096,c_1931,c_1912,c_1907,c_1393,c_366,c_243,c_253,c_256,c_270,c_275,c_281,c_289,c_305,c_313,c_314,c_318,c_321,c_332,c_239,c_240,c_241,c_242,c_249,c_250,c_350]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ017-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.04 % Command : run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.37 % Computer : n005.cluster.edu
% 0.10/0.37 % Model : x86_64 x86_64
% 0.10/0.37 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.37 % Memory : 8046.5625MB
% 0.10/0.37 % OS : Linux 6.8.0-71-generic
% 0.10/0.37 % CPULimit : 300
% 0.10/0.37 % WCLimit : 300
% 0.10/0.37 % DateTime : Thu Sep 24 06:38:02 UTC 2026
% 0.10/0.38 % CPUTime :
% 0.10/0.38 Running run_iprover 300 /export/starexec/sandbox/benchmark/theBenchmark.p THM
% 0.10/0.42 Running EPR theorem proving
% 0.10/0.42 Running: /export/starexec/sandbox/solver/bin/iproveropt-multi-core.sh -d -n -l tptp -s epr_schedule -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 0.10/0.43
% 0.10/0.43 % ======== iProver multi-core TPTP/SMT =========
% 0.10/0.43
% 0.10/0.43 % Detected problem language: tptp
% 0.10/0.44 % Proving...
% 2.07/1.17 % SZS status Started for theBenchmark.p
% 2.07/1.17 % SZS status Unsatisfiable for theBenchmark.p
% 2.07/1.17
% 2.07/1.17 %---------------- iProver v3.9.4 (pre CASC 2026/SMT-COMP 2026) ----------------%
% 2.07/1.17
% 2.07/1.17 % ------ iProver source info
% 2.07/1.17
% 2.07/1.17 % git: date: 2026-07-19 20:42:38 +0200
% 2.07/1.17 % git: sha1: 804e7d636a263075307957e923b7a22a4035de61
% 2.07/1.17 % git: non_committed_changes: false
% 2.07/1.17
% 2.07/1.17 % ------ Parsing...% successful
% 2.07/1.17
% 2.07/1.17
% 2.07/1.17 % ------ Clausification by vclausify_rel & Parsing by iProver...% ------ preprocesses with Option_epr_non_horn_non_eq
% 2.07/1.17 %
% 2.07/1.17
% 2.07/1.17 % ------ Preprocessing... sf_s rm: 0 0s sf_e pe_s pe_e %
% 2.07/1.17
% 2.07/1.17 % ------ Preprocessing...% ------ preprocesses with Option_epr_non_horn_non_eq
% 2.07/1.17 gs_s sp: 25 0s gs_e snvd_s sp: 0 0s snvd_e
% 2.07/1.17 % ------ Proving...
% 2.07/1.17 % ------ Problem Properties
% 2.07/1.17
% 2.07/1.17 %
% 2.07/1.17 % clauses 173
% 2.07/1.17 % conjectures 26
% 2.07/1.17 % EPR 173
% 2.07/1.17 % Horn 155
% 2.07/1.17 % unary 82
% 2.07/1.17 % binary 45
% 2.07/1.17 % lits 382
% 2.07/1.17 % lits eq 0
% 2.07/1.17 % fd_pure 0
% 2.07/1.17 % fd_pseudo 0
% 2.07/1.17 % fd_cond 0
% 2.07/1.17 % fd_pseudo_cond 0
% 2.07/1.17 % AC symbols 0
% 2.07/1.17
% 2.07/1.17 % ------ Schedule EPR non Horn non eq is on
% 2.07/1.17
% 2.07/1.17 % ------ no equalities: superposition off
% 2.07/1.17
% 2.07/1.17 % ------ Input Options "--resolution_flag false" Time Limit: 70.
% 2.07/1.17
% 2.07/1.17
% 2.07/1.17 % ------
% 2.07/1.17 % Current options:
% 2.07/1.17 % ------
% 2.07/1.17
% 2.07/1.17
% 2.07/1.17 %
% 2.07/1.17
% 2.07/1.17 % ------ Proving...
% 2.07/1.17 %
% 2.07/1.17
% 2.07/1.17 % SZS status Unsatisfiable for theBenchmark.p
% 2.07/1.17
% 2.07/1.17 % SZS output start CNFRefutation for theBenchmark.p
% See solution above
% 2.07/1.18
% 2.07/1.18
%------------------------------------------------------------------------------