%------------------------------------------------------------------------------
% File : Leo-III---1.8.0
% Problem : PUZ017-1 : TPTP v9.3.1. Released v1.0.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 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 : Sun Sep 27 08:21:06 AM UTC 2026
% Result : Unsatisfiable 7.43s 2.34s
% Output : Refutation 7.93s
% Verified :
% SZS Type : Refutation
% Derivation depth : 2
% Number of leaves : 148
% Syntax : Number of formulae : 297 ( 165 unt; 0 typ; 0 def)
% Number of atoms : 665 ( 0 equ; 0 cnn)
% Maximal formula atoms : 25 ( 2 avg)
% Number of connectives : 2104 ( 408 ~; 368 |; 0 &;1328 @)
% ( 0 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 53 ( 6 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 44 ( 43 usr; 31 con; 0-2 aty)
% Number of variables : 310 ( 0 ^; 310 !; 0 ?; 310 :)
% Comments :
%------------------------------------------------------------------------------
thf(hasperson_decl,type,
hasperson: $i > $i > $o ).
thf(n1_decl,type,
n1: $i ).
thf(n2_decl,type,
n2: $i ).
thf(n3_decl,type,
n3: $i ).
thf(n4_decl,type,
n4: $i ).
thf(n5_decl,type,
n5: $i ).
thf(hascolor_decl,type,
hascolor: $i > $i > $o ).
thf(hasdrink_decl,type,
hasdrink: $i > $i > $o ).
thf(hasgame_decl,type,
hasgame: $i > $i > $o ).
thf(haspet_decl,type,
haspet: $i > $i > $o ).
thf(samepet_decl,type,
samepet: $i > $i > $o ).
thf(camel_decl,type,
camel: $i ).
thf(rat_decl,type,
rat: $i ).
thf(guppy_decl,type,
guppy: $i ).
thf(no_pet_decl,type,
no_pet: $i ).
thf(nextto_decl,type,
nextto: $i > $i > $o ).
thf(sameperson_decl,type,
sameperson: $i > $i > $o ).
thf(italian_decl,type,
italian: $i ).
thf(russian_decl,type,
russian: $i ).
thf(samegame_decl,type,
samegame: $i > $i > $o ).
thf(solitaire_decl,type,
solitaire: $i ).
thf(charades_decl,type,
charades: $i ).
thf(left_decl,type,
left: $i > $i > $o ).
thf(samecolor_decl,type,
samecolor: $i > $i > $o ).
thf(white_decl,type,
white: $i ).
thf(green_decl,type,
green: $i ).
thf(toad_decl,type,
toad: $i ).
thf(american_decl,type,
american: $i ).
thf(swede_decl,type,
swede: $i ).
thf(yellow_decl,type,
yellow: $i ).
thf(blue_decl,type,
blue: $i ).
thf(backgammon_decl,type,
backgammon: $i ).
thf(samedrink_decl,type,
samedrink: $i > $i > $o ).
thf(lemonade_decl,type,
lemonade: $i ).
thf(unknown_drink_decl,type,
unknown_drink: $i ).
thf(samehouse_decl,type,
samehouse: $i > $i > $o ).
thf(quoits_decl,type,
quoits: $i ).
thf(milk_decl,type,
milk: $i ).
thf(red_decl,type,
red: $i ).
thf(vodka_decl,type,
vodka: $i ).
thf(coffee_decl,type,
coffee: $i ).
thf(englishman_decl,type,
englishman: $i ).
thf(racquetball_decl,type,
racquetball: $i ).
thf(113,axiom,
! [B: $i,A: $i] :
( ( quoits @ ( B @ hasgame ) )
| ~ ( B @ ( A @ nextto ) )
| ~ ( A @ ( n1 @ samehouse ) )
| ~ ( camel @ ( A @ haspet ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c2) ).
thf(365,plain,
! [B: $i,A: $i] :
( ( quoits @ ( B @ hasgame ) )
| ~ ( B @ ( A @ nextto ) )
| ~ ( A @ ( n1 @ samehouse ) )
| ~ ( camel @ ( A @ haspet ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[113]) ).
thf(53,axiom,
! [A: $i] : ( A @ ( A @ samehouse ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_for_samehouse) ).
thf(249,plain,
! [A: $i] : ( A @ ( A @ samehouse ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[53]) ).
thf(45,axiom,
~ ( yellow @ ( green @ samecolor ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',green_not_yellow) ).
thf(234,plain,
~ ( yellow @ ( green @ samecolor ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[45]) ).
thf(106,axiom,
! [A: $i] :
( ( yellow @ ( A @ hascolor ) )
| ~ ( racquetball @ ( A @ hasgame ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',racquetball_played_in_yellow_house1) ).
thf(352,plain,
! [A: $i] :
( ( yellow @ ( A @ hascolor ) )
| ~ ( racquetball @ ( A @ hasgame ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[106]) ).
thf(35,axiom,
~ ( unknown_drink @ ( vodka @ samedrink ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',vodka_not_unknown) ).
thf(217,plain,
~ ( unknown_drink @ ( vodka @ samedrink ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[35]) ).
thf(84,axiom,
! [A: $i] :
( ( A @ ( n5 @ hasperson ) )
| ( A @ ( n4 @ hasperson ) )
| ( A @ ( n3 @ hasperson ) )
| ( A @ ( n2 @ hasperson ) )
| ( A @ ( n1 @ hasperson ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_natioality_is_used) ).
thf(308,plain,
! [A: $i] :
( ( A @ ( n5 @ hasperson ) )
| ( A @ ( n4 @ hasperson ) )
| ( A @ ( n3 @ hasperson ) )
| ( A @ ( n2 @ hasperson ) )
| ( A @ ( n1 @ hasperson ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[84]) ).
thf(52,axiom,
~ ( solitaire @ ( backgammon @ samegame ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',backgammon_not_solitaire) ).
thf(247,plain,
~ ( solitaire @ ( backgammon @ samegame ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[52]) ).
thf(121,axiom,
! [B: $i,A: $i] :
( ( racquetball @ ( B @ hasgame ) )
| ~ ( A @ ( n1 @ samehouse ) )
| ~ ( B @ ( A @ nextto ) )
| ~ ( rat @ ( A @ haspet ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c9) ).
thf(379,plain,
! [B: $i,A: $i] :
( ( racquetball @ ( B @ hasgame ) )
| ~ ( A @ ( n1 @ samehouse ) )
| ~ ( B @ ( A @ nextto ) )
| ~ ( rat @ ( A @ haspet ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[121]) ).
thf(64,axiom,
~ ( rat @ ( toad @ samepet ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',toad_not_rat) ).
thf(269,plain,
~ ( rat @ ( toad @ samepet ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[64]) ).
thf(124,axiom,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ hasgame ) )
| ~ ( C @ ( A @ hasgame ) )
| ( B @ ( A @ samehouse ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',games_have_unique_houses) ).
thf(385,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ hasgame ) )
| ~ ( C @ ( A @ hasgame ) )
| ( B @ ( A @ samehouse ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[124]) ).
thf(100,axiom,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ left ) )
| ~ ( green @ ( B @ hascolor ) )
| ( white @ ( A @ hascolor ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',white_house_left_of_green3) ).
thf(340,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ left ) )
| ~ ( green @ ( B @ hascolor ) )
| ( white @ ( A @ hascolor ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[100]) ).
thf(3,axiom,
~ ( no_pet @ ( guppy @ samepet ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',guppy_is_pet) ).
thf(153,plain,
~ ( no_pet @ ( guppy @ samepet ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[3]) ).
thf(19,axiom,
~ ( quoits @ ( backgammon @ samegame ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',backgammon_not_quoits) ).
thf(185,plain,
~ ( quoits @ ( backgammon @ samegame ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[19]) ).
thf(140,axiom,
! [B: $i,A: $i] :
( ( camel @ ( B @ haspet ) )
| ~ ( quoits @ ( A @ hasgame ) )
| ~ ( B @ ( A @ nextto ) )
| ~ ( A @ ( n1 @ samehouse ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c6) ).
thf(417,plain,
! [B: $i,A: $i] :
( ( camel @ ( B @ haspet ) )
| ~ ( quoits @ ( A @ hasgame ) )
| ~ ( B @ ( A @ nextto ) )
| ~ ( A @ ( n1 @ samehouse ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[140]) ).
thf(74,axiom,
! [C: $i,B: $i,A: $i] :
( ( rat @ ( B @ haspet ) )
| ( rat @ ( A @ haspet ) )
| ~ ( racquetball @ ( C @ hasgame ) )
| ~ ( B @ ( C @ nextto ) )
| ~ ( A @ ( C @ nextto ) )
| ( B @ ( A @ samehouse ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c12) ).
thf(288,plain,
! [C: $i,B: $i,A: $i] :
( ( rat @ ( B @ haspet ) )
| ( rat @ ( A @ haspet ) )
| ~ ( racquetball @ ( C @ hasgame ) )
| ~ ( B @ ( C @ nextto ) )
| ~ ( A @ ( C @ nextto ) )
| ( B @ ( A @ samehouse ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[74]) ).
thf(90,axiom,
~ ( n5 @ ( n3 @ nextto ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_3_not_nextto_5) ).
thf(320,plain,
~ ( n5 @ ( n3 @ nextto ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[90]) ).
thf(126,axiom,
! [A: $i] :
( ~ ( vodka @ ( A @ hasdrink ) )
| ( solitaire @ ( A @ hasgame ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c16) ).
thf(389,plain,
! [A: $i] :
( ~ ( vodka @ ( A @ hasdrink ) )
| ( solitaire @ ( A @ hasgame ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[126]) ).
thf(117,axiom,
n4 @ ( n3 @ left ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_3_left_of_4) ).
thf(372,plain,
n4 @ ( n3 @ left ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[117]) ).
thf(102,axiom,
! [A: $i] :
( ( red @ ( A @ hascolor ) )
| ~ ( englishman @ ( A @ hasperson ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',englishman_lives_in_red_house1) ).
thf(344,plain,
! [A: $i] :
( ( red @ ( A @ hascolor ) )
| ~ ( englishman @ ( A @ hasperson ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[102]) ).
thf(5,axiom,
~ ( russian @ ( italian @ sameperson ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',italian_not_russian) ).
thf(157,plain,
~ ( russian @ ( italian @ sameperson ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[5]) ).
thf(21,axiom,
~ ( charades @ ( quoits @ samegame ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quoits_not_charades) ).
thf(189,plain,
~ ( charades @ ( quoits @ samegame ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[21]) ).
thf(142,axiom,
! [B: $i,A: $i] :
( ~ ( blue @ ( B @ hascolor ) )
| ( B @ ( A @ nextto ) )
| ~ ( russian @ ( A @ hasperson ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c22) ).
thf(421,plain,
! [B: $i,A: $i] :
( ~ ( blue @ ( B @ hascolor ) )
| ( B @ ( A @ nextto ) )
| ~ ( russian @ ( A @ hasperson ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[142]) ).
thf(72,axiom,
~ ( n2 @ ( n1 @ samehouse ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_1_not_2) ).
thf(284,plain,
~ ( n2 @ ( n1 @ samehouse ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[72]) ).
thf(88,axiom,
! [A: $i] :
( ( no_pet @ ( A @ haspet ) )
| ( rat @ ( A @ haspet ) )
| ( camel @ ( A @ haspet ) )
| ( toad @ ( A @ haspet ) )
| ( guppy @ ( A @ haspet ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_house_has_a_pet) ).
thf(316,plain,
! [A: $i] :
( ( no_pet @ ( A @ haspet ) )
| ( rat @ ( A @ haspet ) )
| ( camel @ ( A @ haspet ) )
| ( toad @ ( A @ haspet ) )
| ( guppy @ ( A @ haspet ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[88]) ).
thf(60,axiom,
~ ( white @ ( red @ samecolor ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',red_not_white) ).
thf(261,plain,
~ ( white @ ( red @ samecolor ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[60]) ).
thf(16,axiom,
~ ( camel @ ( guppy @ samepet ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',guppy_not_camel) ).
thf(179,plain,
~ ( camel @ ( guppy @ samepet ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[16]) ).
thf(32,axiom,
~ ( charades @ ( racquetball @ samegame ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',racquetball_not_charades) ).
thf(211,plain,
~ ( charades @ ( racquetball @ samegame ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[32]) ).
thf(47,axiom,
~ ( swede @ ( englishman @ sameperson ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',englishman_not_swede) ).
thf(238,plain,
~ ( swede @ ( englishman @ sameperson ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[47]) ).
thf(104,axiom,
! [B: $i,A: $i] :
( ( quoits @ ( B @ hasgame ) )
| ~ ( B @ ( A @ nextto ) )
| ~ ( n5 @ ( A @ samehouse ) )
| ~ ( camel @ ( A @ haspet ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c3) ).
thf(348,plain,
! [B: $i,A: $i] :
( ( quoits @ ( B @ hasgame ) )
| ~ ( B @ ( A @ nextto ) )
| ~ ( n5 @ ( A @ samehouse ) )
| ~ ( camel @ ( A @ haspet ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[104]) ).
thf(130,axiom,
! [B: $i,A: $i] :
( ( blue @ ( B @ hascolor ) )
| ~ ( B @ ( A @ nextto ) )
| ~ ( A @ ( n1 @ samehouse ) )
| ~ ( russian @ ( A @ hasperson ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c20) ).
thf(397,plain,
! [B: $i,A: $i] :
( ( blue @ ( B @ hascolor ) )
| ~ ( B @ ( A @ nextto ) )
| ~ ( A @ ( n1 @ samehouse ) )
| ~ ( russian @ ( A @ hasperson ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[130]) ).
thf(37,axiom,
~ ( racquetball @ ( backgammon @ samegame ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',backgammon_not_recquetball) ).
thf(221,plain,
~ ( racquetball @ ( backgammon @ samegame ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[37]) ).
thf(137,axiom,
~ ( n5 @ ( n2 @ samehouse ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_2_not_5) ).
thf(411,plain,
~ ( n5 @ ( n2 @ samehouse ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[137]) ).
thf(146,axiom,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ hascolor ) )
| ~ ( A @ ( C @ hascolor ) )
| ( B @ ( A @ samecolor ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',colours_are_unique) ).
thf(428,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ hascolor ) )
| ~ ( A @ ( C @ hascolor ) )
| ( B @ ( A @ samecolor ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[146]) ).
thf(62,axiom,
~ ( no_pet @ ( toad @ samepet ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',toad_is_pet) ).
thf(265,plain,
~ ( no_pet @ ( toad @ samepet ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[62]) ).
thf(86,axiom,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ left ) )
| ( green @ ( B @ hascolor ) )
| ~ ( white @ ( A @ hascolor ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',white_house_left_of_green2) ).
thf(312,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ left ) )
| ( green @ ( B @ hascolor ) )
| ~ ( white @ ( A @ hascolor ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[86]) ).
thf(76,axiom,
! [B: $i,A: $i] :
( ( racquetball @ ( B @ hasgame ) )
| ~ ( n5 @ ( A @ samehouse ) )
| ~ ( B @ ( A @ nextto ) )
| ~ ( rat @ ( A @ haspet ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c10) ).
thf(292,plain,
! [B: $i,A: $i] :
( ( racquetball @ ( B @ hasgame ) )
| ~ ( n5 @ ( A @ samehouse ) )
| ~ ( B @ ( A @ nextto ) )
| ~ ( rat @ ( A @ haspet ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[76]) ).
thf(44,axiom,
! [A: $i] : ( A @ ( A @ samedrink ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_for_samedrink) ).
thf(233,plain,
! [A: $i] : ( A @ ( A @ samedrink ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[44]) ).
thf(27,axiom,
~ ( swede @ ( italian @ sameperson ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',italian_not_swede) ).
thf(201,plain,
~ ( swede @ ( italian @ sameperson ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[27]) ).
thf(122,axiom,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ hasgame ) )
| ~ ( A @ ( C @ hasgame ) )
| ( B @ ( A @ samegame ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',houses_have_unique_games) ).
thf(381,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ hasgame ) )
| ~ ( A @ ( C @ hasgame ) )
| ( B @ ( A @ samegame ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[122]) ).
thf(97,axiom,
! [B: $i,A: $i] :
( ( blue @ ( B @ hascolor ) )
| ~ ( B @ ( A @ nextto ) )
| ~ ( n5 @ ( A @ samehouse ) )
| ~ ( russian @ ( A @ hasperson ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c21) ).
thf(334,plain,
! [B: $i,A: $i] :
( ( blue @ ( B @ hascolor ) )
| ~ ( B @ ( A @ nextto ) )
| ~ ( n5 @ ( A @ samehouse ) )
| ~ ( russian @ ( A @ hasperson ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[97]) ).
thf(81,axiom,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ hasperson ) )
| ~ ( A @ ( C @ hasperson ) )
| ( B @ ( A @ sameperson ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',houses_have_unique_nationals) ).
thf(302,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ hasperson ) )
| ~ ( A @ ( C @ hasperson ) )
| ( B @ ( A @ sameperson ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[81]) ).
thf(144,axiom,
~ ( n3 @ ( n1 @ nextto ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_1_not_nextto_3) ).
thf(424,plain,
~ ( n3 @ ( n1 @ nextto ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[144]) ).
thf(135,axiom,
~ ( n5 @ ( n3 @ samehouse ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_3_not_5) ).
thf(407,plain,
~ ( n5 @ ( n3 @ samehouse ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[135]) ).
thf(67,axiom,
~ ( n4 @ ( n1 @ samehouse ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_1_not_4) ).
thf(275,plain,
~ ( n4 @ ( n1 @ samehouse ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[67]) ).
thf(9,axiom,
~ ( toad @ ( guppy @ samepet ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',guppy_not_toad) ).
thf(165,plain,
~ ( toad @ ( guppy @ samepet ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[9]) ).
thf(42,axiom,
~ ( solitaire @ ( racquetball @ samegame ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',racquetball_not_solitaire) ).
thf(229,plain,
~ ( solitaire @ ( racquetball @ samegame ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[42]) ).
thf(55,axiom,
! [A: $i] :
~ ( A @ ( A @ left ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nothing_left_of_itself) ).
thf(252,plain,
! [A: $i] :
~ ( A @ ( A @ left ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[55]) ).
thf(25,axiom,
~ ( milk @ ( coffee @ samedrink ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',coffee_not_milk) ).
thf(197,plain,
~ ( milk @ ( coffee @ samedrink ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[25]) ).
thf(92,axiom,
! [A: $i] :
( ~ ( charades @ ( A @ hasgame ) )
| ( american @ ( A @ hasperson ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c18) ).
thf(324,plain,
! [A: $i] :
( ~ ( charades @ ( A @ hasgame ) )
| ( american @ ( A @ hasperson ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[92]) ).
thf(133,axiom,
! [C: $i,B: $i,A: $i] :
( ( blue @ ( C @ hascolor ) )
| ( blue @ ( B @ hascolor ) )
| ~ ( C @ ( A @ nextto ) )
| ~ ( B @ ( A @ nextto ) )
| ( C @ ( B @ samehouse ) )
| ~ ( russian @ ( A @ hasperson ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c19) ).
thf(403,plain,
! [C: $i,B: $i,A: $i] :
( ( blue @ ( C @ hascolor ) )
| ( blue @ ( B @ hascolor ) )
| ~ ( C @ ( A @ nextto ) )
| ~ ( B @ ( A @ nextto ) )
| ( C @ ( B @ samehouse ) )
| ~ ( russian @ ( A @ hasperson ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[133]) ).
thf(108,axiom,
! [A: $i] :
( ( charades @ ( A @ hasgame ) )
| ( solitaire @ ( A @ hasgame ) )
| ( quoits @ ( A @ hasgame ) )
| ( racquetball @ ( A @ hasgame ) )
| ( backgammon @ ( A @ hasgame ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_house_has_a_game) ).
thf(356,plain,
! [A: $i] :
( ( charades @ ( A @ hasgame ) )
| ( solitaire @ ( A @ hasgame ) )
| ( quoits @ ( A @ hasgame ) )
| ( racquetball @ ( A @ hasgame ) )
| ( backgammon @ ( A @ hasgame ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[108]) ).
thf(11,axiom,
~ ( american @ ( swede @ sameperson ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',swede_not_american) ).
thf(169,plain,
~ ( american @ ( swede @ sameperson ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[11]) ).
thf(39,axiom,
! [A: $i] : ( A @ ( A @ samepet ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_for_samepet) ).
thf(225,plain,
! [A: $i] : ( A @ ( A @ samepet ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[39]) ).
thf(23,axiom,
~ ( vodka @ ( lemonade @ samedrink ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lemonade_not_vodka) ).
thf(193,plain,
~ ( vodka @ ( lemonade @ samedrink ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[23]) ).
thf(94,axiom,
! [A: $i] :
( ( coffee @ ( A @ hasdrink ) )
| ~ ( swede @ ( A @ hasperson ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',swede_drinks_coffee1) ).
thf(328,plain,
! [A: $i] :
( ( coffee @ ( A @ hasdrink ) )
| ~ ( swede @ ( A @ hasperson ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[94]) ).
thf(57,axiom,
~ ( blue @ ( red @ samecolor ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',red_not_blue) ).
thf(256,plain,
~ ( blue @ ( red @ samecolor ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[57]) ).
thf(128,axiom,
~ ( n4 @ ( n2 @ samehouse ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_2_not_4) ).
thf(393,plain,
~ ( n4 @ ( n2 @ samehouse ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[128]) ).
thf(13,axiom,
~ ( blue @ ( yellow @ samecolor ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',yellow_not_blue) ).
thf(173,plain,
~ ( blue @ ( yellow @ samecolor ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[13]) ).
thf(116,axiom,
milk @ ( n3 @ hasdrink ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_3_has_milk) ).
thf(371,plain,
milk @ ( n3 @ hasdrink ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[116]) ).
thf(50,axiom,
! [A: $i] : ( A @ ( A @ samecolor ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_for_samecolor) ).
thf(244,plain,
! [A: $i] : ( A @ ( A @ samecolor ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[50]) ).
thf(110,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ left ) )
| ~ ( green @ ( B @ hascolor ) )
| ~ ( white @ ( A @ hascolor ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',white_house_left_of_green1) ).
thf(360,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ left ) )
| ~ ( green @ ( B @ hascolor ) )
| ~ ( white @ ( A @ hascolor ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[110]) ).
thf(29,axiom,
~ ( quoits @ ( racquetball @ samegame ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',racquetball_not_quoits) ).
thf(205,plain,
~ ( quoits @ ( racquetball @ samegame ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[29]) ).
thf(79,axiom,
! [A: $i] :
( ( A @ ( n5 @ hasgame ) )
| ( A @ ( n4 @ hasgame ) )
| ( A @ ( n3 @ hasgame ) )
| ( A @ ( n2 @ hasgame ) )
| ( A @ ( n1 @ hasgame ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_game_is_used) ).
thf(298,plain,
! [A: $i] :
( ( A @ ( n5 @ hasgame ) )
| ( A @ ( n4 @ hasgame ) )
| ( A @ ( n3 @ hasgame ) )
| ( A @ ( n2 @ hasgame ) )
| ( A @ ( n1 @ hasgame ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[79]) ).
thf(147,axiom,
! [A: $i] :
( ( backgammon @ ( A @ hasgame ) )
| ~ ( toad @ ( A @ haspet ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',toad_lives_with_backgammon1) ).
thf(430,plain,
! [A: $i] :
( ( backgammon @ ( A @ hasgame ) )
| ~ ( toad @ ( A @ haspet ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[147]) ).
thf(7,axiom,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ left ) )
| ~ ( B @ ( A @ left ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',non_symmetry_of_left) ).
thf(161,plain,
! [B: $i,A: $i] :
( ~ ( A @ ( B @ left ) )
| ~ ( B @ ( A @ left ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[7]) ).
thf(69,axiom,
! [A: $i] :
~ ( A @ ( n5 @ left ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house5_at_right) ).
thf(279,plain,
! [A: $i] :
~ ( A @ ( n5 @ left ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[69]) ).
thf(78,axiom,
~ ( n5 @ ( n1 @ nextto ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_1_not_nextto_5) ).
thf(296,plain,
~ ( n5 @ ( n1 @ nextto ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[78]) ).
thf(1,negated_conjecture,
! [Y: $i,X: $i,W: $i,V: $i,U: $i,T: $i,S: $i,R: $i,Q: $i,P: $i,O: $i,N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( Y @ ( n5 @ haspet ) )
| ~ ( X @ ( n4 @ haspet ) )
| ~ ( W @ ( n3 @ haspet ) )
| ~ ( V @ ( n2 @ haspet ) )
| ~ ( U @ ( n1 @ haspet ) )
| ~ ( T @ ( n5 @ hasgame ) )
| ~ ( S @ ( n4 @ hasgame ) )
| ~ ( R @ ( n3 @ hasgame ) )
| ~ ( Q @ ( n2 @ hasgame ) )
| ~ ( P @ ( n1 @ hasgame ) )
| ~ ( O @ ( n5 @ hasdrink ) )
| ~ ( N @ ( n4 @ hasdrink ) )
| ~ ( M @ ( n3 @ hasdrink ) )
| ~ ( L @ ( n2 @ hasdrink ) )
| ~ ( K @ ( n1 @ hasdrink ) )
| ~ ( J @ ( n5 @ hascolor ) )
| ~ ( I @ ( n4 @ hascolor ) )
| ~ ( H @ ( n3 @ hascolor ) )
| ~ ( G @ ( n2 @ hascolor ) )
| ~ ( F @ ( n1 @ hascolor ) )
| ~ ( E @ ( n5 @ hasperson ) )
| ~ ( D @ ( n4 @ hasperson ) )
| ~ ( C @ ( n3 @ hasperson ) )
| ~ ( B @ ( n2 @ hasperson ) )
| ~ ( A @ ( n1 @ hasperson ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',find_out_house_details) ).
thf(149,plain,
! [Y: $i,X: $i,W: $i,V: $i,U: $i,T: $i,S: $i,R: $i,Q: $i,P: $i,O: $i,N: $i,M: $i,L: $i,K: $i,J: $i,I: $i,H: $i,G: $i,F: $i,E: $i,D: $i,C: $i,B: $i,A: $i] :
( ~ ( Y @ ( n5 @ haspet ) )
| ~ ( X @ ( n4 @ haspet ) )
| ~ ( W @ ( n3 @ haspet ) )
| ~ ( V @ ( n2 @ haspet ) )
| ~ ( U @ ( n1 @ haspet ) )
| ~ ( T @ ( n5 @ hasgame ) )
| ~ ( S @ ( n4 @ hasgame ) )
| ~ ( R @ ( n3 @ hasgame ) )
| ~ ( Q @ ( n2 @ hasgame ) )
| ~ ( P @ ( n1 @ hasgame ) )
| ~ ( O @ ( n5 @ hasdrink ) )
| ~ ( N @ ( n4 @ hasdrink ) )
| ~ ( M @ ( n3 @ hasdrink ) )
| ~ ( L @ ( n2 @ hasdrink ) )
| ~ ( K @ ( n1 @ hasdrink ) )
| ~ ( J @ ( n5 @ hascolor ) )
| ~ ( I @ ( n4 @ hascolor ) )
| ~ ( H @ ( n3 @ hascolor ) )
| ~ ( G @ ( n2 @ hascolor ) )
| ~ ( F @ ( n1 @ hascolor ) )
| ~ ( E @ ( n5 @ hasperson ) )
| ~ ( D @ ( n4 @ hasperson ) )
| ~ ( C @ ( n3 @ hasperson ) )
| ~ ( B @ ( n2 @ hasperson ) )
| ~ ( A @ ( n1 @ hasperson ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[1]) ).
thf(119,axiom,
! [A: $i] :
( ( charades @ ( A @ hasgame ) )
| ~ ( american @ ( A @ hasperson ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c17) ).
thf(375,plain,
! [A: $i] :
( ( charades @ ( A @ hasgame ) )
| ~ ( american @ ( A @ hasperson ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[119]) ).
thf(143,axiom,
n2 @ ( n1 @ left ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_1_left_of_2) ).
thf(423,plain,
n2 @ ( n1 @ left ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[143]) ).
thf(22,axiom,
~ ( yellow @ ( red @ samecolor ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',red_not_yellow) ).
thf(191,plain,
~ ( yellow @ ( red @ samecolor ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[22]) ).
thf(73,axiom,
! [A: $i] :
( ( unknown_drink @ ( A @ hasdrink ) )
| ( vodka @ ( A @ hasdrink ) )
| ( milk @ ( A @ hasdrink ) )
| ( coffee @ ( A @ hasdrink ) )
| ( lemonade @ ( A @ hasdrink ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_house_has_a_drink) ).
thf(286,plain,
! [A: $i] :
( ( unknown_drink @ ( A @ hasdrink ) )
| ( vodka @ ( A @ hasdrink ) )
| ( milk @ ( A @ hasdrink ) )
| ( coffee @ ( A @ hasdrink ) )
| ( lemonade @ ( A @ hasdrink ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[73]) ).
thf(70,axiom,
! [A: $i] :
( ~ ( coffee @ ( A @ hasdrink ) )
| ( swede @ ( A @ hasperson ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',swede_drinks_coffee2) ).
thf(281,plain,
! [A: $i] :
( ~ ( coffee @ ( A @ hasdrink ) )
| ( swede @ ( A @ hasperson ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[70]) ).
thf(59,axiom,
~ ( unknown_drink @ ( milk @ samedrink ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',milk_not_unknown) ).
thf(259,plain,
~ ( unknown_drink @ ( milk @ samedrink ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[59]) ).
thf(138,axiom,
~ ( n5 @ ( n2 @ nextto ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_2_not_nextto_5) ).
thf(413,plain,
~ ( n5 @ ( n2 @ nextto ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[138]) ).
thf(127,axiom,
! [C: $i,B: $i,A: $i] :
( ( camel @ ( B @ haspet ) )
| ( camel @ ( A @ haspet ) )
| ~ ( quoits @ ( C @ hasgame ) )
| ~ ( B @ ( C @ nextto ) )
| ~ ( A @ ( C @ nextto ) )
| ( B @ ( A @ samehouse ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c5) ).
thf(391,plain,
! [C: $i,B: $i,A: $i] :
( ( camel @ ( B @ haspet ) )
| ( camel @ ( A @ haspet ) )
| ~ ( quoits @ ( C @ hasgame ) )
| ~ ( B @ ( C @ nextto ) )
| ~ ( A @ ( C @ nextto ) )
| ( B @ ( A @ samehouse ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[127]) ).
thf(46,axiom,
~ ( solitaire @ ( quoits @ samegame ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',quoits_not_solitaire) ).
thf(236,plain,
~ ( solitaire @ ( quoits @ samegame ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[46]) ).
thf(17,axiom,
~ ( no_pet @ ( rat @ samepet ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',rat_is_pet) ).
thf(181,plain,
~ ( no_pet @ ( rat @ samepet ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[17]) ).
thf(105,axiom,
! [A: $i] :
( ~ ( yellow @ ( A @ hascolor ) )
| ( racquetball @ ( A @ hasgame ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',racquetball_played_in_yellow_house2) ).
thf(350,plain,
! [A: $i] :
( ~ ( yellow @ ( A @ hascolor ) )
| ( racquetball @ ( A @ hasgame ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[105]) ).
thf(6,axiom,
~ ( charades @ ( solitaire @ samegame ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',solitaire_not_charades) ).
thf(159,plain,
~ ( charades @ ( solitaire @ samegame ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[6]) ).
thf(20,axiom,
~ ( milk @ ( lemonade @ samedrink ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lemonade_not_milk) ).
thf(187,plain,
~ ( milk @ ( lemonade @ samedrink ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[20]) ).
thf(36,axiom,
~ ( rat @ ( guppy @ samepet ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',guppy_not_rat) ).
thf(219,plain,
~ ( rat @ ( guppy @ samepet ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[36]) ).
thf(141,axiom,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ hasdrink ) )
| ~ ( A @ ( C @ hasdrink ) )
| ( B @ ( A @ samedrink ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',houses_have_unique_drinks) ).
thf(419,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ hasdrink ) )
| ~ ( A @ ( C @ hasdrink ) )
| ( B @ ( A @ samedrink ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[141]) ).
thf(120,axiom,
~ ( n4 @ ( n1 @ nextto ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_1_not_nextto_4) ).
thf(377,plain,
~ ( n4 @ ( n1 @ nextto ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[120]) ).
thf(111,axiom,
n5 @ ( n4 @ left ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_4_left_of_5) ).
thf(362,plain,
n5 @ ( n4 @ left ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[111]) ).
thf(51,axiom,
~ ( russian @ ( swede @ sameperson ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',swede_not_russian) ).
thf(245,plain,
~ ( russian @ ( swede @ sameperson ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[51]) ).
thf(89,axiom,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ haspet ) )
| ~ ( C @ ( A @ haspet ) )
| ( B @ ( A @ samehouse ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',pets_have_unique_houses) ).
thf(318,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ haspet ) )
| ~ ( C @ ( A @ haspet ) )
| ( B @ ( A @ samehouse ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[89]) ).
thf(65,axiom,
! [A: $i] :
( ( american @ ( A @ hasperson ) )
| ( russian @ ( A @ hasperson ) )
| ( swede @ ( A @ hasperson ) )
| ( italian @ ( A @ hasperson ) )
| ( englishman @ ( A @ hasperson ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_house_has_a_national) ).
thf(271,plain,
! [A: $i] :
( ( american @ ( A @ hasperson ) )
| ( russian @ ( A @ hasperson ) )
| ( swede @ ( A @ hasperson ) )
| ( italian @ ( A @ hasperson ) )
| ( englishman @ ( A @ hasperson ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[65]) ).
thf(125,axiom,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ hasdrink ) )
| ~ ( C @ ( A @ hasdrink ) )
| ( B @ ( A @ samehouse ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',drinks_have_unique_houses) ).
thf(387,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ hasdrink ) )
| ~ ( C @ ( A @ hasdrink ) )
| ( B @ ( A @ samehouse ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[125]) ).
thf(114,axiom,
! [A: $i] :
( ( blue @ ( A @ hascolor ) )
| ( yellow @ ( A @ hascolor ) )
| ( green @ ( A @ hascolor ) )
| ( white @ ( A @ hascolor ) )
| ( red @ ( A @ hascolor ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_house_has_color) ).
thf(367,plain,
! [A: $i] :
( ( blue @ ( A @ hascolor ) )
| ( yellow @ ( A @ hascolor ) )
| ( green @ ( A @ hascolor ) )
| ( white @ ( A @ hascolor ) )
| ( red @ ( A @ hascolor ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[114]) ).
thf(33,axiom,
! [B: $i,A: $i] :
( ( A @ ( B @ left ) )
| ( B @ ( A @ left ) )
| ~ ( B @ ( A @ nextto ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nextto_means_left) ).
thf(213,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ left ) )
| ( B @ ( A @ left ) )
| ~ ( B @ ( A @ nextto ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[33]) ).
thf(48,axiom,
~ ( american @ ( russian @ sameperson ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',russian_not_american) ).
thf(240,plain,
~ ( american @ ( russian @ sameperson ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[48]) ).
thf(4,axiom,
! [B: $i,A: $i] :
( ( A @ ( B @ nextto ) )
| ~ ( B @ ( A @ nextto ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',symmetry_of_nextto) ).
thf(155,plain,
! [B: $i,A: $i] :
( ( A @ ( B @ nextto ) )
| ~ ( B @ ( A @ nextto ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[4]) ).
thf(95,axiom,
! [A: $i] :
( ( A @ ( n5 @ hasdrink ) )
| ( A @ ( n4 @ hasdrink ) )
| ( A @ ( n3 @ hasdrink ) )
| ( A @ ( n2 @ hasdrink ) )
| ( A @ ( n1 @ hasdrink ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_drink_is_used) ).
thf(330,plain,
! [A: $i] :
( ( A @ ( n5 @ hasdrink ) )
| ( A @ ( n4 @ hasdrink ) )
| ( A @ ( n3 @ hasdrink ) )
| ( A @ ( n2 @ hasdrink ) )
| ( A @ ( n1 @ hasdrink ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[95]) ).
thf(131,axiom,
! [A: $i] :
~ ( n1 @ ( A @ left ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house1_at_left) ).
thf(399,plain,
! [A: $i] :
~ ( n1 @ ( A @ left ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[131]) ).
thf(38,axiom,
~ ( camel @ ( toad @ samepet ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',toad_not_camel) ).
thf(223,plain,
~ ( camel @ ( toad @ samepet ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[38]) ).
thf(83,axiom,
! [B: $i,A: $i] :
( ~ ( quoits @ ( B @ hasgame ) )
| ( B @ ( A @ nextto ) )
| ~ ( camel @ ( A @ haspet ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c4) ).
thf(306,plain,
! [B: $i,A: $i] :
( ~ ( quoits @ ( B @ hasgame ) )
| ( B @ ( A @ nextto ) )
| ~ ( camel @ ( A @ haspet ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[83]) ).
thf(40,axiom,
! [A: $i] : ( A @ ( A @ samegame ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_for_samegame) ).
thf(226,plain,
! [A: $i] : ( A @ ( A @ samegame ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[40]) ).
thf(63,axiom,
~ ( blue @ ( green @ samecolor ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',green_not_blue) ).
thf(267,plain,
~ ( blue @ ( green @ samecolor ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[63]) ).
thf(10,axiom,
~ ( american @ ( italian @ sameperson ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',italian_not_american) ).
thf(167,plain,
~ ( american @ ( italian @ sameperson ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[10]) ).
thf(145,axiom,
! [A: $i] :
( ( A @ ( n5 @ hascolor ) )
| ( A @ ( n4 @ hascolor ) )
| ( A @ ( n3 @ hascolor ) )
| ( A @ ( n2 @ hascolor ) )
| ( A @ ( n1 @ hascolor ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_color_is_used) ).
thf(426,plain,
! [A: $i] :
( ( A @ ( n5 @ hascolor ) )
| ( A @ ( n4 @ hascolor ) )
| ( A @ ( n3 @ hascolor ) )
| ( A @ ( n2 @ hascolor ) )
| ( A @ ( n1 @ hascolor ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[145]) ).
thf(31,axiom,
~ ( blue @ ( white @ samecolor ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',white_not_blue) ).
thf(209,plain,
~ ( blue @ ( white @ samecolor ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[31]) ).
thf(101,axiom,
! [B: $i,A: $i] :
( ~ ( racquetball @ ( B @ hasgame ) )
| ( B @ ( A @ nextto ) )
| ~ ( rat @ ( A @ haspet ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c11) ).
thf(342,plain,
! [B: $i,A: $i] :
( ~ ( racquetball @ ( B @ hasgame ) )
| ( B @ ( A @ nextto ) )
| ~ ( rat @ ( A @ haspet ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[101]) ).
thf(136,axiom,
! [C: $i,B: $i,A: $i] :
( ( russian @ ( B @ hasperson ) )
| ( russian @ ( A @ hasperson ) )
| ~ ( blue @ ( C @ hascolor ) )
| ~ ( B @ ( C @ nextto ) )
| ~ ( A @ ( C @ nextto ) )
| ( B @ ( A @ samehouse ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c23) ).
thf(409,plain,
! [C: $i,B: $i,A: $i] :
( ( russian @ ( B @ hasperson ) )
| ( russian @ ( A @ hasperson ) )
| ~ ( blue @ ( C @ hascolor ) )
| ~ ( B @ ( C @ nextto ) )
| ~ ( A @ ( C @ nextto ) )
| ( B @ ( A @ samehouse ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[136]) ).
thf(61,axiom,
! [B: $i,A: $i] :
( ( B @ ( A @ nextto ) )
| ~ ( B @ ( A @ left ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',left_means_nextto) ).
thf(263,plain,
! [B: $i,A: $i] :
( ( B @ ( A @ nextto ) )
| ~ ( B @ ( A @ left ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[61]) ).
thf(85,axiom,
! [A: $i] :
( ~ ( green @ ( A @ hascolor ) )
| ( lemonade @ ( A @ hasdrink ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lemonade_in_green_house2) ).
thf(310,plain,
! [A: $i] :
( ~ ( green @ ( A @ hascolor ) )
| ( lemonade @ ( A @ hasdrink ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[85]) ).
thf(26,axiom,
~ ( italian @ ( englishman @ sameperson ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',englishman_not_italian) ).
thf(199,plain,
~ ( italian @ ( englishman @ sameperson ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[26]) ).
thf(15,axiom,
~ ( unknown_drink @ ( lemonade @ samedrink ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lemonade_not_unknown) ).
thf(177,plain,
~ ( unknown_drink @ ( lemonade @ samedrink ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[15]) ).
thf(99,axiom,
~ ( n4 @ ( n2 @ nextto ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_2_not_nextto_4) ).
thf(338,plain,
~ ( n4 @ ( n2 @ nextto ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[99]) ).
thf(98,axiom,
! [A: $i] :
( ( green @ ( A @ hascolor ) )
| ~ ( lemonade @ ( A @ hasdrink ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lemonade_in_green_house1) ).
thf(336,plain,
! [A: $i] :
( ( green @ ( A @ hascolor ) )
| ~ ( lemonade @ ( A @ hasdrink ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[98]) ).
thf(14,axiom,
~ ( charades @ ( backgammon @ samegame ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',backgammon_not_charades) ).
thf(175,plain,
~ ( charades @ ( backgammon @ samegame ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[14]) ).
thf(87,axiom,
! [A: $i] :
( ( vodka @ ( A @ hasdrink ) )
| ~ ( solitaire @ ( A @ hasgame ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c15) ).
thf(314,plain,
! [A: $i] :
( ( vodka @ ( A @ hasdrink ) )
| ~ ( solitaire @ ( A @ hasgame ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[87]) ).
thf(112,axiom,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ hascolor ) )
| ~ ( C @ ( A @ hascolor ) )
| ( B @ ( A @ samehouse ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',houses_have_unique_colors) ).
thf(363,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ hascolor ) )
| ~ ( C @ ( A @ hascolor ) )
| ( B @ ( A @ samehouse ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[112]) ).
thf(28,axiom,
! [A: $i] :
~ ( A @ ( A @ nextto ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nothing_nextto_itself) ).
thf(203,plain,
! [A: $i] :
~ ( A @ ( A @ nextto ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[28]) ).
thf(54,axiom,
~ ( unknown_drink @ ( coffee @ samedrink ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',coffee_not_known) ).
thf(250,plain,
~ ( unknown_drink @ ( coffee @ samedrink ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[54]) ).
thf(43,axiom,
~ ( russian @ ( englishman @ sameperson ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',englishman_not_russian) ).
thf(231,plain,
~ ( russian @ ( englishman @ sameperson ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[43]) ).
thf(82,axiom,
! [B: $i,A: $i] :
( ( russian @ ( B @ hasperson ) )
| ~ ( A @ ( n1 @ samehouse ) )
| ~ ( blue @ ( A @ hascolor ) )
| ~ ( B @ ( A @ nextto ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c24) ).
thf(304,plain,
! [B: $i,A: $i] :
( ( russian @ ( B @ hasperson ) )
| ~ ( A @ ( n1 @ samehouse ) )
| ~ ( blue @ ( A @ hascolor ) )
| ~ ( B @ ( A @ nextto ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[82]) ).
thf(58,axiom,
! [A: $i] : ( A @ ( A @ sameperson ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',reflexivity_for_sameperson) ).
thf(258,plain,
! [A: $i] : ( A @ ( A @ sameperson ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[58]) ).
thf(132,axiom,
! [C: $i,B: $i,A: $i] :
( ( quoits @ ( C @ hasgame ) )
| ( quoits @ ( B @ hasgame ) )
| ~ ( C @ ( A @ nextto ) )
| ~ ( B @ ( A @ nextto ) )
| ( C @ ( B @ samehouse ) )
| ~ ( camel @ ( A @ haspet ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c1) ).
thf(401,plain,
! [C: $i,B: $i,A: $i] :
( ( quoits @ ( C @ hasgame ) )
| ( quoits @ ( B @ hasgame ) )
| ~ ( C @ ( A @ nextto ) )
| ~ ( B @ ( A @ nextto ) )
| ( C @ ( B @ samehouse ) )
| ~ ( camel @ ( A @ haspet ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[132]) ).
thf(12,axiom,
~ ( no_pet @ ( camel @ samepet ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',camel_is_pet) ).
thf(171,plain,
~ ( no_pet @ ( camel @ samepet ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[12]) ).
thf(75,axiom,
~ ( n5 @ ( n1 @ samehouse ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_1_not_5) ).
thf(290,plain,
~ ( n5 @ ( n1 @ samehouse ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[75]) ).
thf(30,axiom,
~ ( yellow @ ( white @ samecolor ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',white_not_yellow) ).
thf(207,plain,
~ ( yellow @ ( white @ samecolor ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[30]) ).
thf(123,axiom,
~ ( n5 @ ( n4 @ samehouse ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_4_not_5) ).
thf(383,plain,
~ ( n5 @ ( n4 @ samehouse ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[123]) ).
thf(103,axiom,
! [A: $i] :
( ( A @ ( n5 @ haspet ) )
| ( A @ ( n4 @ haspet ) )
| ( A @ ( n3 @ haspet ) )
| ( A @ ( n2 @ haspet ) )
| ( A @ ( n1 @ haspet ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',every_pet_is_used) ).
thf(346,plain,
! [A: $i] :
( ( A @ ( n5 @ haspet ) )
| ( A @ ( n4 @ haspet ) )
| ( A @ ( n3 @ haspet ) )
| ( A @ ( n2 @ haspet ) )
| ( A @ ( n1 @ haspet ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[103]) ).
thf(2,axiom,
~ ( rat @ ( camel @ samepet ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',camel_not_rat) ).
thf(151,plain,
~ ( rat @ ( camel @ samepet ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[2]) ).
thf(80,axiom,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ haspet ) )
| ~ ( A @ ( C @ haspet ) )
| ( B @ ( A @ samepet ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',houses_have_unique_pets) ).
thf(300,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( B @ ( C @ haspet ) )
| ~ ( A @ ( C @ haspet ) )
| ( B @ ( A @ samepet ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[80]) ).
thf(148,axiom,
n3 @ ( n2 @ left ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_2_left_of_3) ).
thf(432,plain,
n3 @ ( n2 @ left ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[148]) ).
thf(134,axiom,
! [B: $i,A: $i] :
( ( russian @ ( B @ hasperson ) )
| ~ ( n5 @ ( A @ samehouse ) )
| ~ ( blue @ ( A @ hascolor ) )
| ~ ( B @ ( A @ nextto ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c25) ).
thf(405,plain,
! [B: $i,A: $i] :
( ( russian @ ( B @ hasperson ) )
| ~ ( n5 @ ( A @ samehouse ) )
| ~ ( blue @ ( A @ hascolor ) )
| ~ ( B @ ( A @ nextto ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[134]) ).
thf(18,axiom,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ nextto ) )
| ~ ( B @ ( A @ samehouse ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_not_nextto_itself) ).
thf(183,plain,
! [B: $i,A: $i] :
( ~ ( B @ ( A @ nextto ) )
| ~ ( B @ ( A @ samehouse ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[18]) ).
thf(66,axiom,
! [A: $i] :
( ~ ( guppy @ ( A @ haspet ) )
| ( italian @ ( A @ hasperson ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',italian_has_guppy2) ).
thf(273,plain,
! [A: $i] :
( ~ ( guppy @ ( A @ haspet ) )
| ( italian @ ( A @ hasperson ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[66]) ).
thf(118,axiom,
! [C: $i,B: $i,A: $i] :
( ( racquetball @ ( C @ hasgame ) )
| ( racquetball @ ( B @ hasgame ) )
| ~ ( C @ ( A @ nextto ) )
| ~ ( B @ ( A @ nextto ) )
| ( C @ ( B @ samehouse ) )
| ~ ( rat @ ( A @ haspet ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c8) ).
thf(373,plain,
! [C: $i,B: $i,A: $i] :
( ( racquetball @ ( C @ hasgame ) )
| ( racquetball @ ( B @ hasgame ) )
| ~ ( C @ ( A @ nextto ) )
| ~ ( B @ ( A @ nextto ) )
| ( C @ ( B @ samehouse ) )
| ~ ( rat @ ( A @ haspet ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[118]) ).
thf(93,axiom,
! [A: $i] :
( ~ ( backgammon @ ( A @ hasgame ) )
| ( toad @ ( A @ haspet ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',toad_lives_with_backgammon2) ).
thf(326,plain,
! [A: $i] :
( ~ ( backgammon @ ( A @ hasgame ) )
| ( toad @ ( A @ haspet ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[93]) ).
thf(49,axiom,
~ ( green @ ( red @ samecolor ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',red_not_green) ).
thf(242,plain,
~ ( green @ ( red @ samecolor ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[49]) ).
thf(77,axiom,
! [A: $i] :
( ~ ( red @ ( A @ hascolor ) )
| ( englishman @ ( A @ hasperson ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',englishman_lives_in_red_house2) ).
thf(294,plain,
! [A: $i] :
( ~ ( red @ ( A @ hascolor ) )
| ( englishman @ ( A @ hasperson ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[77]) ).
thf(109,axiom,
~ ( n3 @ ( n1 @ samehouse ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_1_not_3) ).
thf(358,plain,
~ ( n3 @ ( n1 @ samehouse ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[109]) ).
thf(24,axiom,
~ ( coffee @ ( lemonade @ samedrink ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',lemonade_not_coffee) ).
thf(195,plain,
~ ( coffee @ ( lemonade @ samedrink ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[24]) ).
thf(71,axiom,
russian @ ( n1 @ hasperson ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_1_has_russian) ).
thf(283,plain,
russian @ ( n1 @ hasperson ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[71]) ).
thf(139,axiom,
~ ( n4 @ ( n3 @ samehouse ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_3_not_4) ).
thf(415,plain,
~ ( n4 @ ( n3 @ samehouse ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[139]) ).
thf(129,axiom,
! [A: $i] :
( ( guppy @ ( A @ haspet ) )
| ~ ( italian @ ( A @ hasperson ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',italian_has_guppy1) ).
thf(395,plain,
! [A: $i] :
( ( guppy @ ( A @ haspet ) )
| ~ ( italian @ ( A @ hasperson ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[129]) ).
thf(96,axiom,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ hasperson ) )
| ~ ( C @ ( A @ hasperson ) )
| ( B @ ( A @ samehouse ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',nationals_have_unique_houses) ).
thf(332,plain,
! [C: $i,B: $i,A: $i] :
( ~ ( C @ ( B @ hasperson ) )
| ~ ( C @ ( A @ hasperson ) )
| ( B @ ( A @ samehouse ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[96]) ).
thf(8,axiom,
~ ( green @ ( white @ samecolor ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',white_not_green) ).
thf(163,plain,
~ ( green @ ( white @ samecolor ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[8]) ).
thf(68,axiom,
! [B: $i,A: $i] :
( ( rat @ ( B @ haspet ) )
| ~ ( racquetball @ ( A @ hasgame ) )
| ~ ( n5 @ ( A @ samehouse ) )
| ~ ( B @ ( A @ nextto ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c14) ).
thf(277,plain,
! [B: $i,A: $i] :
( ( rat @ ( B @ haspet ) )
| ~ ( racquetball @ ( A @ hasgame ) )
| ~ ( n5 @ ( A @ samehouse ) )
| ~ ( B @ ( A @ nextto ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[68]) ).
thf(115,axiom,
~ ( n3 @ ( n2 @ samehouse ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',house_2_not_3) ).
thf(369,plain,
~ ( n3 @ ( n2 @ samehouse ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[115]) ).
thf(91,axiom,
! [B: $i,A: $i] :
( ( camel @ ( B @ haspet ) )
| ~ ( quoits @ ( A @ hasgame ) )
| ~ ( B @ ( A @ nextto ) )
| ~ ( n5 @ ( A @ samehouse ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c7) ).
thf(322,plain,
! [B: $i,A: $i] :
( ( camel @ ( B @ haspet ) )
| ~ ( quoits @ ( A @ hasgame ) )
| ~ ( B @ ( A @ nextto ) )
| ~ ( n5 @ ( A @ samehouse ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[91]) ).
thf(107,axiom,
! [B: $i,A: $i] :
( ( rat @ ( B @ haspet ) )
| ~ ( racquetball @ ( A @ hasgame ) )
| ~ ( A @ ( n1 @ samehouse ) )
| ~ ( B @ ( A @ nextto ) ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',c13) ).
thf(354,plain,
! [B: $i,A: $i] :
( ( rat @ ( B @ haspet ) )
| ~ ( racquetball @ ( A @ hasgame ) )
| ~ ( A @ ( n1 @ samehouse ) )
| ~ ( B @ ( A @ nextto ) ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[107]) ).
thf(34,axiom,
~ ( vodka @ ( coffee @ samedrink ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',coffee_not_vodka) ).
thf(215,plain,
~ ( vodka @ ( coffee @ samedrink ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[34]) ).
thf(56,axiom,
~ ( american @ ( englishman @ sameperson ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',englishman_not_american) ).
thf(254,plain,
~ ( american @ ( englishman @ sameperson ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[56]) ).
thf(41,axiom,
~ ( vodka @ ( milk @ samedrink ) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',milk_not_vodka) ).
thf(227,plain,
~ ( vodka @ ( milk @ samedrink ) ),
inference(defexp_and_simp_and_etaexpand,[status(thm)],[41]) ).
thf(653,plain,
$false,
inference(e,[status(thm)],[365,249,234,352,217,308,247,379,269,385,340,153,185,417,288,320,389,372,344,157,189,421,284,316,261,179,211,238,348,397,221,411,428,265,312,292,233,201,381,334,302,424,407,275,165,229,252,197,324,403,356,169,225,193,328,256,393,173,371,244,360,205,298,430,161,279,296,149,375,423,191,286,281,259,413,391,236,181,350,159,187,219,419,377,362,245,318,271,387,367,213,240,155,330,399,223,306,226,267,167,426,209,342,409,263,310,199,177,338,336,175,314,363,203,250,231,304,258,401,171,290,207,383,346,151,300,432,405,183,273,373,326,242,294,358,195,283,415,395,332,163,277,369,322,354,215,254,227]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ017-1 : TPTP v9.3.1. Released v1.0.0.
% 0.00/0.07 % Command : java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.13/0.39 % Computer : n005.cluster.edu
% 0.13/0.39 % Model : x86_64 x86_64
% 0.13/0.39 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.39 % Memory : 8046.5625MB
% 0.13/0.39 % OS : Linux 6.8.0-71-generic
% 0.13/0.39 % CPULimit : 300
% 0.13/0.39 % WCLimit : 300
% 0.13/0.39 % DateTime : Sat Sep 26 05:04:17 UTC 2026
% 0.13/0.39 % CPUTime :
% 0.13/0.39 Running java -Xss128m -Xmx2g -Xms1g -jar /export/starexec/sandbox/solver/bin/leo3.jar /export/starexec/sandbox/benchmark/theBenchmark.p -t 300 -p --atp eprover=/export/starexec/sandbox/solver/bin/externals/eprover --instantiate 39
% 0.72/0.70 % [INFO] Parsing problem /export/starexec/sandbox/benchmark/theBenchmark.p ...
% 0.95/0.84 % [INFO] Parsing done (140ms).
% 0.95/0.85 % [INFO] Running in sequential loop mode.
% 1.83/1.06 % [INFO] eprover registered as external prover.
% 1.83/1.06 % [INFO] Scanning for conjecture ...
% 2.16/1.14 % [INFO] Found a conjecture (or negated_conjecture) and 147 axioms. Running axiom selection ...
% 2.37/1.24 % [INFO] Axiom selection finished. Selected 147 axioms (removed 0 axioms).
% 2.37/1.29 % [INFO] Problem is propositional (TPTP CNF).
% 2.37/1.30 % [INFO] Type checking passed.
% 2.72/1.30 % [CONFIG] Using configuration: timeout(300) with strategy<name(default),share(1.0),primSubst(3),sos(false),unifierCount(4),uniDepth(8),boolExt(true),choice(true),renaming(true),funcspec(false), domConstr(0),specialInstances(39),restrictUniAttempts(true),termOrdering(CPO)>. Searching for refutation ...
% 7.43/2.34 % External prover 'e' found a proof!
% 7.43/2.34 % [INFO] Killing All external provers ...
% 7.43/2.34 % Time passed: 1847ms (effective reasoning time: 1481ms)
% 7.43/2.34 % Axioms used in derivation (147): coffee_not_milk, racquetball_played_in_yellow_house2, every_house_has_color, toad_not_rat, racquetball_not_solitaire, guppy_is_pet, house_1_not_4, reflexivity_for_samehouse, houses_have_unique_drinks, italian_not_russian, backgammon_not_solitaire, milk_not_vodka, swede_drinks_coffee2, c3, house_3_not_5, c4, englishman_lives_in_red_house1, every_game_is_used, toad_lives_with_backgammon1, white_house_left_of_green2, englishman_not_swede, every_color_is_used, c11, c8, lemonade_in_green_house1, c22, every_house_has_a_pet, vodka_not_unknown, englishman_not_russian, house_4_left_of_5, house_2_not_3, pets_have_unique_houses, c15, house_1_not_nextto_5, houses_have_unique_nationals, white_not_yellow, reflexivity_for_samegame, c19, swede_not_russian, red_not_green, house5_at_right, rat_is_pet, quoits_not_solitaire, house_3_not_nextto_5, toad_lives_with_backgammon2, white_house_left_of_green3, italian_has_guppy1, house_2_not_nextto_4, englishman_lives_in_red_house2, houses_have_unique_pets, quoits_not_charades, c5, house_1_not_3, c2, house_3_not_4, house_2_left_of_3, nationals_have_unique_houses, camel_is_pet, house_1_not_nextto_4, reflexivity_for_samepet, nothing_left_of_itself, every_house_has_a_game, c9, c12, c23, swede_not_american, lemonade_not_vodka, green_not_yellow, c16, symmetry_of_nextto, racquetball_not_quoits, reflexivity_for_sameperson, c21, white_not_blue, every_house_has_a_national, backgammon_not_recquetball, toad_is_pet, c1, guppy_not_camel, c6, red_not_white, house_2_not_5, house_1_not_2, italian_not_swede, c18, every_pet_is_used, house_1_left_of_2, house_3_has_milk, lemonade_not_coffee, house1_at_left, house_2_not_nextto_5, c24, racquetball_not_charades, englishman_not_american, red_not_yellow, guppy_not_rat, russian_not_american, lemonade_in_green_house2, reflexivity_for_samecolor, colours_are_unique, c13, houses_have_unique_games, italian_not_american, reflexivity_for_samedrink, c20, house_3_left_of_4, red_not_blue, house_1_not_nextto_3, yellow_not_blue, games_have_unique_houses, backgammon_not_quoits, nothing_nextto_itself, c7, swede_drinks_coffee1, guppy_not_toad, lemonade_not_milk, house_1_has_russian, lemonade_not_unknown, englishman_not_italian, left_means_nextto, house_1_not_5, houses_have_unique_colors, c17, coffee_not_known, white_house_left_of_green1, every_drink_is_used, italian_has_guppy2, white_not_green, non_symmetry_of_left, c14, camel_not_rat, solitaire_not_charades, nextto_means_left, green_not_blue, toad_not_camel, every_house_has_a_drink, milk_not_unknown, drinks_have_unique_houses, racquetball_played_in_yellow_house1, c10, coffee_not_vodka, c25, house_not_nextto_itself, house_2_not_4, backgammon_not_charades, every_natioality_is_used, house_4_not_5
% 7.43/2.34 % No. of inferences in proof: 297
% 7.43/2.34 % SZS status Unsatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p : 1847 ms resp. 1481 ms w/o parsing
% 7.93/2.41 % SZS output start Refutation for /export/starexec/sandbox/benchmark/theBenchmark.p
% See solution above
% 7.93/2.42 % [INFO] Killing All external provers ...
%------------------------------------------------------------------------------