%------------------------------------------------------------------------------
% File : Vampire-SAT---5.0.1
% Problem : PUZ010-1 : TPTP v9.3.1. Bugfixed v1.0.1.
% Transfm : none
% Format : tptp:raw
% Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue Sep 29 12:31:49 PM UTC 2026
% Result : Unsatisfiable 0.36s 0.50s
% Output : Refutation 0.36s
% Verified :
% SZS Type : Refutation
% Derivation depth : 41
% Number of leaves : 277
% Syntax : Number of formulae : 1380 ( 223 unt; 158 def)
% Number of atoms : 3907 ( 0 equ)
% Maximal formula atoms : 25 ( 2 avg)
% Number of connectives : 4863 (2336 ~;2369 |; 0 &)
% ( 158 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 172 ( 171 usr; 159 prp; 0-2 aty)
% Number of functors : 30 ( 30 usr; 30 con; 0-0 aty)
% Number of variables : 253 ( 0 sgn 253 !; 0 ?)
% Comments :
%------------------------------------------------------------------------------
fof(f1,axiom,
! [X0] :
( ~ person(X0)
| lives(X0,house_1)
| lives(X0,house_2)
| lives(X0,house_3)
| lives(X0,house_4)
| lives(X0,house_5) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',people_live_somewhere) ).
fof(f2,axiom,
! [X0] :
( ~ house(X0)
| ~ lives(english,X0)
| ~ lives(spaniard,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',english_and_spaniard_live_apart) ).
fof(f3,axiom,
! [X0] :
( ~ house(X0)
| ~ lives(english,X0)
| ~ lives(norwegian,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',english_and_norwegian_live_apart) ).
fof(f4,axiom,
! [X0] :
( ~ house(X0)
| ~ lives(english,X0)
| ~ lives(ukranian,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',english_and_ukranian_live_apart) ).
fof(f5,axiom,
! [X0] :
( ~ house(X0)
| ~ lives(english,X0)
| ~ lives(japanese,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',english_and_japanese_live_apart) ).
fof(f6,axiom,
! [X0] :
( ~ house(X0)
| ~ lives(spaniard,X0)
| ~ lives(norwegian,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',spaniard_and_norwegian_live_apart) ).
fof(f7,axiom,
! [X0] :
( ~ house(X0)
| ~ lives(spaniard,X0)
| ~ lives(ukranian,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',spaniard_and_ukranian_live_apart) ).
fof(f8,axiom,
! [X0] :
( ~ house(X0)
| ~ lives(spaniard,X0)
| ~ lives(japanese,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',spaniard_and_japanese_live_apart) ).
fof(f9,axiom,
! [X0] :
( ~ house(X0)
| ~ lives(norwegian,X0)
| ~ lives(ukranian,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',norwegian_and_ukranian_live_apart) ).
fof(f10,axiom,
! [X0] :
( ~ house(X0)
| ~ lives(norwegian,X0)
| ~ lives(japanese,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',norwegian_and_japanese_live_apart) ).
fof(f11,axiom,
! [X0] :
( ~ house(X0)
| ~ lives(ukranian,X0)
| ~ lives(japanese,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ukranian_and_japanese_live_apart) ).
fof(f12,axiom,
! [X0] :
( drinks(X0,water)
| drinks(X0,orange)
| drinks(X0,coffee)
| drinks(X0,tea)
| drinks(X0,milk)
| ~ person(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',drink_something) ).
fof(f13,axiom,
! [X0] :
( ~ drink(X0)
| ~ drinks(english,X0)
| ~ drinks(spaniard,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',english_and_spaniard_drink_different) ).
fof(f14,axiom,
! [X0] :
( ~ drink(X0)
| ~ drinks(english,X0)
| ~ drinks(norwegian,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',english_and_norwegian_drink_different) ).
fof(f15,axiom,
! [X0] :
( ~ drink(X0)
| ~ drinks(english,X0)
| ~ drinks(ukranian,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',english_and_unkranian_drink_different) ).
fof(f16,axiom,
! [X0] :
( ~ drink(X0)
| ~ drinks(english,X0)
| ~ drinks(japanese,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',english_and_japanese_drink_different) ).
fof(f17,axiom,
! [X0] :
( ~ drink(X0)
| ~ drinks(spaniard,X0)
| ~ drinks(norwegian,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',spaniard_and_norwegian_drink_different) ).
fof(f18,axiom,
! [X0] :
( ~ drink(X0)
| ~ drinks(spaniard,X0)
| ~ drinks(ukranian,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',spaniard_and_ukranian_drink_different) ).
fof(f19,axiom,
! [X0] :
( ~ drink(X0)
| ~ drinks(spaniard,X0)
| ~ drinks(japanese,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',spaniard_and_japanese_drink_different) ).
fof(f20,axiom,
! [X0] :
( ~ drink(X0)
| ~ drinks(norwegian,X0)
| ~ drinks(ukranian,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',norwegian_and_ukranian_drink_different) ).
fof(f21,axiom,
! [X0] :
( ~ drink(X0)
| ~ drinks(norwegian,X0)
| ~ drinks(japanese,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',norwegian_and_japanese_drink_different) ).
fof(f22,axiom,
! [X0] :
( ~ drink(X0)
| ~ drinks(ukranian,X0)
| ~ drinks(japanese,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ukranian_and_japanese_drink_different) ).
fof(f23,axiom,
! [X0] :
( drives(X0,jaguar)
| drives(X0,masserati)
| drives(X0,saab)
| drives(X0,porsche)
| drives(X0,honda)
| ~ person(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',drive_something) ).
fof(f24,axiom,
! [X0] :
( ~ car(X0)
| ~ drives(english,X0)
| ~ drives(spaniard,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',english_and_spaniard_drive_different) ).
fof(f25,axiom,
! [X0] :
( ~ car(X0)
| ~ drives(english,X0)
| ~ drives(norwegian,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',english_and_norwegian_drive_different) ).
fof(f26,axiom,
! [X0] :
( ~ car(X0)
| ~ drives(english,X0)
| ~ drives(ukranian,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',english_and_ukranian_drive_different) ).
fof(f27,axiom,
! [X0] :
( ~ car(X0)
| ~ drives(english,X0)
| ~ drives(japanese,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',english_and_japanese_drive_different) ).
fof(f28,axiom,
! [X0] :
( ~ car(X0)
| ~ drives(spaniard,X0)
| ~ drives(norwegian,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',spaniard_and_norwegian_drive_different) ).
fof(f29,axiom,
! [X0] :
( ~ car(X0)
| ~ drives(spaniard,X0)
| ~ drives(ukranian,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',spaniard_and_ukranian_drive_different) ).
fof(f30,axiom,
! [X0] :
( ~ car(X0)
| ~ drives(spaniard,X0)
| ~ drives(japanese,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',spaniard_and_japanese_drive_different) ).
fof(f31,axiom,
! [X0] :
( ~ car(X0)
| ~ drives(norwegian,X0)
| ~ drives(ukranian,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',norwegian_and_ukranian_drive_different) ).
fof(f32,axiom,
! [X0] :
( ~ car(X0)
| ~ drives(norwegian,X0)
| ~ drives(japanese,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',norwegian_and_japanese_drive_different) ).
fof(f33,axiom,
! [X0] :
( ~ car(X0)
| ~ drives(ukranian,X0)
| ~ drives(japanese,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ukranian_and_japanese_drive_different) ).
fof(f34,axiom,
! [X0] :
( owns(X0,zebra)
| owns(X0,dog)
| owns(X0,snails)
| owns(X0,horse)
| owns(X0,fox)
| ~ person(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',own_a_pet) ).
fof(f35,axiom,
! [X0] :
( ~ animal(X0)
| ~ owns(english,X0)
| ~ owns(spaniard,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',english_and_spaniard_own_different_pets) ).
fof(f36,axiom,
! [X0] :
( ~ animal(X0)
| ~ owns(english,X0)
| ~ owns(norwegian,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',english_and_norwegian_own_different_pets) ).
fof(f37,axiom,
! [X0] :
( ~ animal(X0)
| ~ owns(english,X0)
| ~ owns(ukranian,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',english_and_ukranian_own_different_pets) ).
fof(f38,axiom,
! [X0] :
( ~ animal(X0)
| ~ owns(english,X0)
| ~ owns(japanese,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',english_and_japanese_own_different_pets) ).
fof(f39,axiom,
! [X0] :
( ~ animal(X0)
| ~ owns(spaniard,X0)
| ~ owns(norwegian,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',spaniard_and_norwegian_own_different_pets) ).
fof(f40,axiom,
! [X0] :
( ~ animal(X0)
| ~ owns(spaniard,X0)
| ~ owns(ukranian,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',spaniard_and_ukranian_own_different_pets) ).
fof(f41,axiom,
! [X0] :
( ~ animal(X0)
| ~ owns(spaniard,X0)
| ~ owns(japanese,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',spaniard_and_japanese_own_different_pets) ).
fof(f42,axiom,
! [X0] :
( ~ animal(X0)
| ~ owns(norwegian,X0)
| ~ owns(ukranian,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',norwegian_and_ukranian_own_different_pets) ).
fof(f43,axiom,
! [X0] :
( ~ animal(X0)
| ~ owns(norwegian,X0)
| ~ owns(japanese,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',norwegian_and_japanese_own_different_pets) ).
fof(f44,axiom,
! [X0] :
( ~ animal(X0)
| ~ owns(ukranian,X0)
| ~ owns(japanese,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ukranian_and_japanese_own_different_pets) ).
fof(f45,axiom,
! [X0] :
( is_color(X0,ivory)
| is_color(X0,red)
| is_color(X0,yellow)
| is_color(X0,blue)
| is_color(X0,green)
| ~ house(X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',house_coloured) ).
fof(f46,axiom,
! [X0] :
( ~ color(X0)
| ~ is_color(house_1,X0)
| ~ is_color(house_2,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',houses_1_and_2_coloured_different) ).
fof(f47,axiom,
! [X0] :
( ~ color(X0)
| ~ is_color(house_1,X0)
| ~ is_color(house_3,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',houses_1_and_3_coloured_different) ).
fof(f48,axiom,
! [X0] :
( ~ color(X0)
| ~ is_color(house_1,X0)
| ~ is_color(house_4,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',houses_1_and_4_coloured_different) ).
fof(f49,axiom,
! [X0] :
( ~ color(X0)
| ~ is_color(house_1,X0)
| ~ is_color(house_5,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',houses_1_and_5_coloured_different) ).
fof(f50,axiom,
! [X0] :
( ~ color(X0)
| ~ is_color(house_2,X0)
| ~ is_color(house_3,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',houses_2_and_3_coloured_different) ).
fof(f51,axiom,
! [X0] :
( ~ color(X0)
| ~ is_color(house_2,X0)
| ~ is_color(house_4,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',houses_2_and_4_coloured_different) ).
fof(f52,axiom,
! [X0] :
( ~ color(X0)
| ~ is_color(house_2,X0)
| ~ is_color(house_5,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',houses_2_and_5_coloured_different) ).
fof(f53,axiom,
! [X0] :
( ~ color(X0)
| ~ is_color(house_3,X0)
| ~ is_color(house_4,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',houses_3_and_4_coloured_different) ).
fof(f54,axiom,
! [X0] :
( ~ color(X0)
| ~ is_color(house_3,X0)
| ~ is_color(house_5,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',houses_3_and_5_coloured_different) ).
fof(f55,axiom,
! [X0] :
( ~ color(X0)
| ~ is_color(house_4,X0)
| ~ is_color(house_5,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',houses_4_and_5_coloured_different) ).
fof(f56,axiom,
person(english),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',english) ).
fof(f57,axiom,
person(spaniard),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',spaniard) ).
fof(f58,axiom,
person(norwegian),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',norwegian) ).
fof(f59,axiom,
person(ukranian),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ukranian) ).
fof(f60,axiom,
person(japanese),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',japanese) ).
fof(f61,axiom,
house(house_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',house_house_1) ).
fof(f62,axiom,
house(house_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',house_house_2) ).
fof(f63,axiom,
house(house_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',house_house_3) ).
fof(f64,axiom,
house(house_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',house_house_4) ).
fof(f65,axiom,
house(house_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',house_house_5) ).
fof(f66,axiom,
color(red),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',red) ).
fof(f67,axiom,
color(green),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',green) ).
fof(f68,axiom,
color(yellow),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',yellow) ).
fof(f69,axiom,
color(ivory),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ivory) ).
fof(f70,axiom,
color(blue),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',blue) ).
fof(f71,axiom,
car(jaguar),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',jaguar) ).
fof(f74,axiom,
car(porsche),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',porsche) ).
fof(f75,axiom,
car(saab),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',saab) ).
fof(f76,axiom,
drink(tea),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',tea) ).
fof(f77,axiom,
drink(orange),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',orange) ).
fof(f78,axiom,
drink(water),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',water) ).
fof(f79,axiom,
drink(milk),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',milk) ).
fof(f80,axiom,
drink(coffee),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',coffee) ).
fof(f81,axiom,
animal(dog),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',dog) ).
fof(f82,axiom,
animal(zebra),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',zebra) ).
fof(f83,axiom,
animal(snails),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',snails) ).
fof(f85,axiom,
animal(fox),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',fox) ).
fof(f86,axiom,
! [X0] :
( is_color(X0,red)
| ~ house(X0)
| ~ lives(english,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',english_in_red_house) ).
fof(f87,axiom,
owns(spaniard,dog),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',spaniard_owns_dog) ).
fof(f88,axiom,
lives(norwegian,house_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',norwegian_in_house_house_1) ).
fof(f89,axiom,
! [X0,X1] :
( is_color(X0,yellow)
| ~ person(X1)
| ~ drives(X1,masserati)
| ~ house(X0)
| ~ lives(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',masserati_in_yellow_house) ).
fof(f90,axiom,
! [X2,X3,X0,X1] :
( next_to(X0,X1)
| ~ person(X2)
| ~ owns(X2,fox)
| ~ house(X0)
| ~ lives(X2,X0)
| ~ person(X3)
| ~ drives(X3,saab)
| ~ house(X1)
| ~ lives(X3,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',saab_with_fox) ).
fof(f91,axiom,
! [X0,X1] :
( is_color(X0,blue)
| ~ house(X1)
| ~ lives(norwegian,X1)
| ~ house(X0)
| ~ next_to(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',norwegian_in_blue_house) ).
fof(f92,axiom,
! [X0] :
( owns(X0,snails)
| ~ person(X0)
| ~ drives(X0,porsche) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',porsche_with_snails) ).
fof(f93,axiom,
! [X0] :
( ~ drives(X0,honda)
| ~ person(X0)
| drinks(X0,orange) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',honda_with_orange) ).
fof(f94,axiom,
drinks(ukranian,tea),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',ukranian_drinks_tea) ).
fof(f95,axiom,
drives(japanese,jaguar),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',japanese_drives_jaguar) ).
fof(f96,axiom,
! [X2,X3,X0,X1] :
( next_to(X0,X1)
| ~ person(X2)
| ~ drives(X2,masserati)
| ~ house(X0)
| ~ lives(X2,X0)
| ~ person(X3)
| ~ owns(X3,horse)
| ~ house(X1)
| ~ lives(X3,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',masserati_next_to_horse) ).
fof(f97,axiom,
! [X0,X1] :
( is_color(X0,green)
| ~ person(X1)
| ~ drinks(X1,coffee)
| ~ house(X0)
| ~ lives(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',coffee_in_green_house) ).
fof(f98,axiom,
! [X0,X1] :
( left_of(X0,X1)
| ~ house(X1)
| ~ is_color(X1,green)
| ~ house(X0)
| ~ is_color(X0,ivory) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',green_right_of_ivory) ).
fof(f99,axiom,
! [X0] :
( lives(X0,house_3)
| ~ person(X0)
| ~ drinks(X0,milk) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',milk_in_middle) ).
fof(f100,axiom,
! [X0,X1] :
( next_to(X0,X1)
| ~ left_of(X0,X1) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',left_means_next_to) ).
fof(f101,axiom,
! [X0,X1] :
( next_to(X0,X1)
| ~ left_of(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',right_mean_next_to) ).
fof(f102,axiom,
! [X0,X1] :
( left_of(X0,X1)
| ~ next_to(X0,X1)
| left_of(X1,X0) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',next_to_means_left_or_right) ).
fof(f103,axiom,
left_of(house_1,house_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',house_1_left_of_house_2) ).
fof(f105,axiom,
left_of(house_3,house_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',house_3_left_of_house_4) ).
fof(f107,axiom,
~ left_of(house_1,house_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',house_1_not_left_of_house_1) ).
fof(f109,axiom,
~ left_of(house_3,house_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',house_3_not_left_of_house_1) ).
fof(f110,axiom,
~ left_of(house_4,house_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',house_4_not_left_of_house_1) ).
fof(f111,axiom,
~ left_of(house_5,house_1),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',house_5_not_left_of_house_1) ).
fof(f112,axiom,
~ left_of(house_2,house_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',house_2_not_left_of_house_2) ).
fof(f114,axiom,
~ left_of(house_4,house_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',house_4_not_left_of_house_2) ).
fof(f115,axiom,
~ left_of(house_5,house_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',house_5_not_left_of_house_2) ).
fof(f116,axiom,
~ left_of(house_1,house_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',house_1_not_left_of_house_3) ).
fof(f118,axiom,
~ left_of(house_4,house_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',house_4_not_left_of_house_3) ).
fof(f119,axiom,
~ left_of(house_5,house_3),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',house_5_not_left_of_house_3) ).
fof(f120,axiom,
~ left_of(house_1,house_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',house_1_not_left_of_house_4) ).
fof(f121,axiom,
~ left_of(house_2,house_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',house_2_not_left_of_house_4) ).
fof(f122,axiom,
~ left_of(house_4,house_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',house_4_not_left_of_house_4) ).
fof(f123,axiom,
~ left_of(house_5,house_4),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',house_5_not_left_of_house_4) ).
fof(f124,axiom,
~ left_of(house_1,house_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',house_1_not_left_of_house_5) ).
fof(f125,axiom,
~ left_of(house_2,house_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',house_2_not_left_of_house_5) ).
fof(f126,axiom,
~ left_of(house_3,house_5),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',house_3_not_left_of_house_5) ).
fof(f128,negated_conjecture,
( ~ drinks(norwegian,water)
| ~ drinks(ukranian,tea)
| ~ drinks(japanese,coffee)
| ~ drinks(english,milk)
| ~ drinks(spaniard,orange)
| ~ owns(norwegian,fox)
| ~ owns(ukranian,horse)
| ~ owns(japanese,zebra)
| ~ owns(english,snails)
| ~ owns(spaniard,dog)
| ~ drives(norwegian,masserati)
| ~ drives(ukranian,saab)
| ~ drives(japanese,jaguar)
| ~ drives(english,porsche)
| ~ drives(spaniard,honda)
| ~ lives(norwegian,house_1)
| ~ lives(ukranian,house_2)
| ~ lives(japanese,house_5)
| ~ lives(english,house_3)
| ~ lives(spaniard,house_4)
| ~ is_color(house_1,yellow)
| ~ is_color(house_2,blue)
| ~ is_color(house_3,red)
| ~ is_color(house_4,ivory)
| ~ is_color(house_5,green) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',prove_configuration) ).
fof(f129,plain,
! [X0] :
( ~ lives(X0,house_5)
| ~ lives(X0,house_1)
| ~ lives(X0,house_2)
| ~ lives(X0,house_3)
| ~ lives(X0,house_4)
| ~ person(X0) ),
inference(consistent_polarity_flipping,[],[f1]) ).
fof(f130,plain,
! [X0] :
( lives(spaniard,X0)
| lives(english,X0)
| ~ house(X0) ),
inference(consistent_polarity_flipping,[],[f2]) ).
fof(f131,plain,
! [X0] :
( lives(norwegian,X0)
| lives(english,X0)
| ~ house(X0) ),
inference(consistent_polarity_flipping,[],[f3]) ).
fof(f132,plain,
! [X0] :
( lives(ukranian,X0)
| lives(english,X0)
| ~ house(X0) ),
inference(consistent_polarity_flipping,[],[f4]) ).
fof(f133,plain,
! [X0] :
( lives(japanese,X0)
| lives(english,X0)
| ~ house(X0) ),
inference(consistent_polarity_flipping,[],[f5]) ).
fof(f134,plain,
! [X0] :
( lives(norwegian,X0)
| lives(spaniard,X0)
| ~ house(X0) ),
inference(consistent_polarity_flipping,[],[f6]) ).
fof(f135,plain,
! [X0] :
( lives(ukranian,X0)
| lives(spaniard,X0)
| ~ house(X0) ),
inference(consistent_polarity_flipping,[],[f7]) ).
fof(f136,plain,
! [X0] :
( lives(japanese,X0)
| lives(spaniard,X0)
| ~ house(X0) ),
inference(consistent_polarity_flipping,[],[f8]) ).
fof(f137,plain,
! [X0] :
( lives(ukranian,X0)
| lives(norwegian,X0)
| ~ house(X0) ),
inference(consistent_polarity_flipping,[],[f9]) ).
fof(f138,plain,
! [X0] :
( lives(japanese,X0)
| lives(norwegian,X0)
| ~ house(X0) ),
inference(consistent_polarity_flipping,[],[f10]) ).
fof(f139,plain,
! [X0] :
( lives(japanese,X0)
| lives(ukranian,X0)
| ~ house(X0) ),
inference(consistent_polarity_flipping,[],[f11]) ).
fof(f140,plain,
! [X0] :
( drink(X0)
| ~ drinks(english,X0)
| ~ drinks(spaniard,X0) ),
inference(consistent_polarity_flipping,[],[f13]) ).
fof(f141,plain,
! [X0] :
( drink(X0)
| ~ drinks(english,X0)
| ~ drinks(norwegian,X0) ),
inference(consistent_polarity_flipping,[],[f14]) ).
fof(f142,plain,
! [X0] :
( drink(X0)
| ~ drinks(english,X0)
| ~ drinks(ukranian,X0) ),
inference(consistent_polarity_flipping,[],[f15]) ).
fof(f143,plain,
! [X0] :
( drink(X0)
| ~ drinks(english,X0)
| ~ drinks(japanese,X0) ),
inference(consistent_polarity_flipping,[],[f16]) ).
fof(f144,plain,
! [X0] :
( drink(X0)
| ~ drinks(spaniard,X0)
| ~ drinks(norwegian,X0) ),
inference(consistent_polarity_flipping,[],[f17]) ).
fof(f145,plain,
! [X0] :
( drink(X0)
| ~ drinks(spaniard,X0)
| ~ drinks(ukranian,X0) ),
inference(consistent_polarity_flipping,[],[f18]) ).
fof(f146,plain,
! [X0] :
( drink(X0)
| ~ drinks(spaniard,X0)
| ~ drinks(japanese,X0) ),
inference(consistent_polarity_flipping,[],[f19]) ).
fof(f147,plain,
! [X0] :
( drink(X0)
| ~ drinks(norwegian,X0)
| ~ drinks(ukranian,X0) ),
inference(consistent_polarity_flipping,[],[f20]) ).
fof(f148,plain,
! [X0] :
( drink(X0)
| ~ drinks(norwegian,X0)
| ~ drinks(japanese,X0) ),
inference(consistent_polarity_flipping,[],[f21]) ).
fof(f149,plain,
! [X0] :
( drink(X0)
| ~ drinks(ukranian,X0)
| ~ drinks(japanese,X0) ),
inference(consistent_polarity_flipping,[],[f22]) ).
fof(f150,plain,
! [X0] :
( car(X0)
| ~ drives(english,X0)
| ~ drives(spaniard,X0) ),
inference(consistent_polarity_flipping,[],[f24]) ).
fof(f151,plain,
! [X0] :
( car(X0)
| ~ drives(english,X0)
| ~ drives(norwegian,X0) ),
inference(consistent_polarity_flipping,[],[f25]) ).
fof(f152,plain,
! [X0] :
( car(X0)
| ~ drives(english,X0)
| ~ drives(ukranian,X0) ),
inference(consistent_polarity_flipping,[],[f26]) ).
fof(f153,plain,
! [X0] :
( car(X0)
| ~ drives(english,X0)
| ~ drives(japanese,X0) ),
inference(consistent_polarity_flipping,[],[f27]) ).
fof(f154,plain,
! [X0] :
( car(X0)
| ~ drives(spaniard,X0)
| ~ drives(norwegian,X0) ),
inference(consistent_polarity_flipping,[],[f28]) ).
fof(f155,plain,
! [X0] :
( car(X0)
| ~ drives(spaniard,X0)
| ~ drives(ukranian,X0) ),
inference(consistent_polarity_flipping,[],[f29]) ).
fof(f156,plain,
! [X0] :
( car(X0)
| ~ drives(spaniard,X0)
| ~ drives(japanese,X0) ),
inference(consistent_polarity_flipping,[],[f30]) ).
fof(f157,plain,
! [X0] :
( car(X0)
| ~ drives(norwegian,X0)
| ~ drives(ukranian,X0) ),
inference(consistent_polarity_flipping,[],[f31]) ).
fof(f158,plain,
! [X0] :
( car(X0)
| ~ drives(norwegian,X0)
| ~ drives(japanese,X0) ),
inference(consistent_polarity_flipping,[],[f32]) ).
fof(f159,plain,
! [X0] :
( car(X0)
| ~ drives(ukranian,X0)
| ~ drives(japanese,X0) ),
inference(consistent_polarity_flipping,[],[f33]) ).
fof(f160,plain,
! [X0] :
( animal(X0)
| ~ owns(english,X0)
| ~ owns(spaniard,X0) ),
inference(consistent_polarity_flipping,[],[f35]) ).
fof(f161,plain,
! [X0] :
( animal(X0)
| ~ owns(english,X0)
| ~ owns(norwegian,X0) ),
inference(consistent_polarity_flipping,[],[f36]) ).
fof(f162,plain,
! [X0] :
( animal(X0)
| ~ owns(english,X0)
| ~ owns(ukranian,X0) ),
inference(consistent_polarity_flipping,[],[f37]) ).
fof(f163,plain,
! [X0] :
( animal(X0)
| ~ owns(english,X0)
| ~ owns(japanese,X0) ),
inference(consistent_polarity_flipping,[],[f38]) ).
fof(f164,plain,
! [X0] :
( animal(X0)
| ~ owns(spaniard,X0)
| ~ owns(norwegian,X0) ),
inference(consistent_polarity_flipping,[],[f39]) ).
fof(f165,plain,
! [X0] :
( animal(X0)
| ~ owns(spaniard,X0)
| ~ owns(ukranian,X0) ),
inference(consistent_polarity_flipping,[],[f40]) ).
fof(f166,plain,
! [X0] :
( animal(X0)
| ~ owns(spaniard,X0)
| ~ owns(japanese,X0) ),
inference(consistent_polarity_flipping,[],[f41]) ).
fof(f167,plain,
! [X0] :
( animal(X0)
| ~ owns(norwegian,X0)
| ~ owns(ukranian,X0) ),
inference(consistent_polarity_flipping,[],[f42]) ).
fof(f168,plain,
! [X0] :
( animal(X0)
| ~ owns(norwegian,X0)
| ~ owns(japanese,X0) ),
inference(consistent_polarity_flipping,[],[f43]) ).
fof(f169,plain,
! [X0] :
( animal(X0)
| ~ owns(ukranian,X0)
| ~ owns(japanese,X0) ),
inference(consistent_polarity_flipping,[],[f44]) ).
fof(f170,plain,
! [X0] :
( color(X0)
| ~ is_color(house_1,X0)
| ~ is_color(house_2,X0) ),
inference(consistent_polarity_flipping,[],[f46]) ).
fof(f171,plain,
! [X0] :
( color(X0)
| ~ is_color(house_1,X0)
| ~ is_color(house_3,X0) ),
inference(consistent_polarity_flipping,[],[f47]) ).
fof(f172,plain,
! [X0] :
( color(X0)
| ~ is_color(house_1,X0)
| ~ is_color(house_4,X0) ),
inference(consistent_polarity_flipping,[],[f48]) ).
fof(f173,plain,
! [X0] :
( color(X0)
| ~ is_color(house_1,X0)
| ~ is_color(house_5,X0) ),
inference(consistent_polarity_flipping,[],[f49]) ).
fof(f174,plain,
! [X0] :
( color(X0)
| ~ is_color(house_2,X0)
| ~ is_color(house_3,X0) ),
inference(consistent_polarity_flipping,[],[f50]) ).
fof(f175,plain,
! [X0] :
( color(X0)
| ~ is_color(house_2,X0)
| ~ is_color(house_4,X0) ),
inference(consistent_polarity_flipping,[],[f51]) ).
fof(f176,plain,
! [X0] :
( color(X0)
| ~ is_color(house_2,X0)
| ~ is_color(house_5,X0) ),
inference(consistent_polarity_flipping,[],[f52]) ).
fof(f177,plain,
! [X0] :
( color(X0)
| ~ is_color(house_3,X0)
| ~ is_color(house_4,X0) ),
inference(consistent_polarity_flipping,[],[f53]) ).
fof(f178,plain,
! [X0] :
( color(X0)
| ~ is_color(house_3,X0)
| ~ is_color(house_5,X0) ),
inference(consistent_polarity_flipping,[],[f54]) ).
fof(f179,plain,
! [X0] :
( color(X0)
| ~ is_color(house_4,X0)
| ~ is_color(house_5,X0) ),
inference(consistent_polarity_flipping,[],[f55]) ).
fof(f180,plain,
~ color(red),
inference(consistent_polarity_flipping,[],[f66]) ).
fof(f181,plain,
~ color(green),
inference(consistent_polarity_flipping,[],[f67]) ).
fof(f182,plain,
~ color(yellow),
inference(consistent_polarity_flipping,[],[f68]) ).
fof(f183,plain,
~ color(ivory),
inference(consistent_polarity_flipping,[],[f69]) ).
fof(f184,plain,
~ color(blue),
inference(consistent_polarity_flipping,[],[f70]) ).
fof(f185,plain,
~ car(jaguar),
inference(consistent_polarity_flipping,[],[f71]) ).
fof(f188,plain,
~ car(porsche),
inference(consistent_polarity_flipping,[],[f74]) ).
fof(f189,plain,
~ car(saab),
inference(consistent_polarity_flipping,[],[f75]) ).
fof(f190,plain,
~ drink(tea),
inference(consistent_polarity_flipping,[],[f76]) ).
fof(f191,plain,
~ drink(orange),
inference(consistent_polarity_flipping,[],[f77]) ).
fof(f192,plain,
~ drink(water),
inference(consistent_polarity_flipping,[],[f78]) ).
fof(f193,plain,
~ drink(milk),
inference(consistent_polarity_flipping,[],[f79]) ).
fof(f194,plain,
~ drink(coffee),
inference(consistent_polarity_flipping,[],[f80]) ).
fof(f195,plain,
~ animal(dog),
inference(consistent_polarity_flipping,[],[f81]) ).
fof(f196,plain,
~ animal(zebra),
inference(consistent_polarity_flipping,[],[f82]) ).
fof(f197,plain,
~ animal(snails),
inference(consistent_polarity_flipping,[],[f83]) ).
fof(f199,plain,
~ animal(fox),
inference(consistent_polarity_flipping,[],[f85]) ).
fof(f200,plain,
! [X0] :
( is_color(X0,red)
| ~ house(X0)
| lives(english,X0) ),
inference(consistent_polarity_flipping,[],[f86]) ).
fof(f201,plain,
~ lives(norwegian,house_1),
inference(consistent_polarity_flipping,[],[f88]) ).
fof(f202,plain,
! [X0,X1] :
( is_color(X0,yellow)
| ~ person(X1)
| ~ drives(X1,masserati)
| ~ house(X0)
| lives(X1,X0) ),
inference(consistent_polarity_flipping,[],[f89]) ).
fof(f203,plain,
! [X2,X3,X0,X1] :
( next_to(X0,X1)
| ~ person(X2)
| ~ owns(X2,fox)
| ~ house(X0)
| lives(X2,X0)
| ~ person(X3)
| ~ drives(X3,saab)
| ~ house(X1)
| lives(X3,X1) ),
inference(consistent_polarity_flipping,[],[f90]) ).
fof(f204,plain,
! [X0,X1] :
( is_color(X0,blue)
| ~ house(X1)
| lives(norwegian,X1)
| ~ house(X0)
| ~ next_to(X1,X0) ),
inference(consistent_polarity_flipping,[],[f91]) ).
fof(f205,plain,
! [X2,X3,X0,X1] :
( next_to(X0,X1)
| ~ person(X2)
| ~ drives(X2,masserati)
| ~ house(X0)
| lives(X2,X0)
| ~ person(X3)
| ~ owns(X3,horse)
| ~ house(X1)
| lives(X3,X1) ),
inference(consistent_polarity_flipping,[],[f96]) ).
fof(f206,plain,
! [X0,X1] :
( is_color(X0,green)
| ~ person(X1)
| ~ drinks(X1,coffee)
| ~ house(X0)
| lives(X1,X0) ),
inference(consistent_polarity_flipping,[],[f97]) ).
fof(f207,plain,
! [X0,X1] :
( ~ left_of(X0,X1)
| ~ house(X1)
| ~ is_color(X1,green)
| ~ house(X0)
| ~ is_color(X0,ivory) ),
inference(consistent_polarity_flipping,[],[f98]) ).
fof(f208,plain,
! [X0] :
( ~ drinks(X0,milk)
| ~ person(X0)
| ~ lives(X0,house_3) ),
inference(consistent_polarity_flipping,[],[f99]) ).
fof(f209,plain,
! [X0,X1] :
( left_of(X0,X1)
| next_to(X0,X1) ),
inference(consistent_polarity_flipping,[],[f100]) ).
fof(f210,plain,
! [X0,X1] :
( left_of(X1,X0)
| next_to(X0,X1) ),
inference(consistent_polarity_flipping,[],[f101]) ).
fof(f211,plain,
! [X0,X1] :
( ~ left_of(X1,X0)
| ~ left_of(X0,X1)
| ~ next_to(X0,X1) ),
inference(consistent_polarity_flipping,[],[f102]) ).
fof(f212,plain,
~ left_of(house_1,house_2),
inference(consistent_polarity_flipping,[],[f103]) ).
fof(f214,plain,
~ left_of(house_3,house_4),
inference(consistent_polarity_flipping,[],[f105]) ).
fof(f216,plain,
left_of(house_1,house_1),
inference(consistent_polarity_flipping,[],[f107]) ).
fof(f218,plain,
left_of(house_3,house_1),
inference(consistent_polarity_flipping,[],[f109]) ).
fof(f219,plain,
left_of(house_4,house_1),
inference(consistent_polarity_flipping,[],[f110]) ).
fof(f220,plain,
left_of(house_5,house_1),
inference(consistent_polarity_flipping,[],[f111]) ).
fof(f221,plain,
left_of(house_2,house_2),
inference(consistent_polarity_flipping,[],[f112]) ).
fof(f223,plain,
left_of(house_4,house_2),
inference(consistent_polarity_flipping,[],[f114]) ).
fof(f224,plain,
left_of(house_5,house_2),
inference(consistent_polarity_flipping,[],[f115]) ).
fof(f225,plain,
left_of(house_1,house_3),
inference(consistent_polarity_flipping,[],[f116]) ).
fof(f227,plain,
left_of(house_4,house_3),
inference(consistent_polarity_flipping,[],[f118]) ).
fof(f228,plain,
left_of(house_5,house_3),
inference(consistent_polarity_flipping,[],[f119]) ).
fof(f229,plain,
left_of(house_1,house_4),
inference(consistent_polarity_flipping,[],[f120]) ).
fof(f230,plain,
left_of(house_2,house_4),
inference(consistent_polarity_flipping,[],[f121]) ).
fof(f231,plain,
left_of(house_4,house_4),
inference(consistent_polarity_flipping,[],[f122]) ).
fof(f232,plain,
left_of(house_5,house_4),
inference(consistent_polarity_flipping,[],[f123]) ).
fof(f233,plain,
left_of(house_1,house_5),
inference(consistent_polarity_flipping,[],[f124]) ).
fof(f234,plain,
left_of(house_2,house_5),
inference(consistent_polarity_flipping,[],[f125]) ).
fof(f235,plain,
left_of(house_3,house_5),
inference(consistent_polarity_flipping,[],[f126]) ).
fof(f237,plain,
( ~ drinks(norwegian,water)
| ~ drinks(ukranian,tea)
| ~ drinks(japanese,coffee)
| ~ drinks(english,milk)
| ~ drinks(spaniard,orange)
| ~ owns(norwegian,fox)
| ~ owns(ukranian,horse)
| ~ owns(japanese,zebra)
| ~ owns(english,snails)
| ~ owns(spaniard,dog)
| ~ drives(norwegian,masserati)
| ~ drives(ukranian,saab)
| ~ drives(japanese,jaguar)
| ~ drives(english,porsche)
| ~ drives(spaniard,honda)
| lives(norwegian,house_1)
| lives(ukranian,house_2)
| lives(japanese,house_5)
| lives(english,house_3)
| lives(spaniard,house_4)
| ~ is_color(house_1,yellow)
| ~ is_color(house_2,blue)
| ~ is_color(house_3,red)
| ~ is_color(house_4,ivory)
| ~ is_color(house_5,green) ),
inference(consistent_polarity_flipping,[],[f128]) ).
fof(f239,definition,
( spl0_1
<=> is_color(house_5,green) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f241,plain,
( ~ is_color(house_5,green)
| spl0_1 ),
inference(avatar_component_clause,[],[f239]) ).
fof(f243,definition,
( spl0_2
<=> is_color(house_4,ivory) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f245,plain,
( ~ is_color(house_4,ivory)
| spl0_2 ),
inference(avatar_component_clause,[],[f243]) ).
fof(f247,definition,
( spl0_3
<=> is_color(house_3,red) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f249,plain,
( ~ is_color(house_3,red)
| spl0_3 ),
inference(avatar_component_clause,[],[f247]) ).
fof(f251,definition,
( spl0_4
<=> is_color(house_2,blue) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f253,plain,
( ~ is_color(house_2,blue)
| spl0_4 ),
inference(avatar_component_clause,[],[f251]) ).
fof(f255,definition,
( spl0_5
<=> is_color(house_1,yellow) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f259,definition,
( spl0_6
<=> lives(spaniard,house_4) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f263,definition,
( spl0_7
<=> lives(english,house_3) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f267,definition,
( spl0_8
<=> lives(japanese,house_5) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f268,plain,
( ~ lives(japanese,house_5)
| spl0_8 ),
inference(avatar_component_clause,[],[f267]) ).
fof(f269,plain,
( lives(japanese,house_5)
| ~ spl0_8 ),
inference(avatar_component_clause,[],[f267]) ).
fof(f271,definition,
( spl0_9
<=> lives(ukranian,house_2) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f272,plain,
( ~ lives(ukranian,house_2)
| spl0_9 ),
inference(avatar_component_clause,[],[f271]) ).
fof(f275,definition,
( spl0_10
<=> lives(norwegian,house_1) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f276,plain,
( ~ lives(norwegian,house_1)
| spl0_10 ),
inference(avatar_component_clause,[],[f275]) ).
fof(f279,definition,
( spl0_11
<=> drives(spaniard,honda) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f280,plain,
( drives(spaniard,honda)
| ~ spl0_11 ),
inference(avatar_component_clause,[],[f279]) ).
fof(f283,definition,
( spl0_12
<=> drives(english,porsche) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f287,definition,
( spl0_13
<=> drives(japanese,jaguar) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f291,definition,
( spl0_14
<=> drives(ukranian,saab) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f292,plain,
( drives(ukranian,saab)
| ~ spl0_14 ),
inference(avatar_component_clause,[],[f291]) ).
fof(f295,definition,
( spl0_15
<=> drives(norwegian,masserati) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f296,plain,
( drives(norwegian,masserati)
| ~ spl0_15 ),
inference(avatar_component_clause,[],[f295]) ).
fof(f299,definition,
( spl0_16
<=> owns(spaniard,dog) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f303,definition,
( spl0_17
<=> owns(english,snails) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f305,plain,
( ~ owns(english,snails)
| spl0_17 ),
inference(avatar_component_clause,[],[f303]) ).
fof(f307,definition,
( spl0_18
<=> owns(japanese,zebra) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f309,plain,
( ~ owns(japanese,zebra)
| spl0_18 ),
inference(avatar_component_clause,[],[f307]) ).
fof(f311,definition,
( spl0_19
<=> owns(ukranian,horse) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f312,plain,
( owns(ukranian,horse)
| ~ spl0_19 ),
inference(avatar_component_clause,[],[f311]) ).
fof(f315,definition,
( spl0_20
<=> owns(norwegian,fox) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f316,plain,
( owns(norwegian,fox)
| ~ spl0_20 ),
inference(avatar_component_clause,[],[f315]) ).
fof(f319,definition,
( spl0_21
<=> drinks(spaniard,orange) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f323,definition,
( spl0_22
<=> drinks(english,milk) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f324,plain,
( drinks(english,milk)
| ~ spl0_22 ),
inference(avatar_component_clause,[],[f323]) ).
fof(f327,definition,
( spl0_23
<=> drinks(japanese,coffee) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f328,plain,
( drinks(japanese,coffee)
| ~ spl0_23 ),
inference(avatar_component_clause,[],[f327]) ).
fof(f331,definition,
( spl0_24
<=> drinks(ukranian,tea) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f335,definition,
( spl0_25
<=> drinks(norwegian,water) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f337,plain,
( ~ drinks(norwegian,water)
| spl0_25 ),
inference(avatar_component_clause,[],[f335]) ).
fof(f338,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_4
| ~ spl0_5
| spl0_6
| spl0_7
| spl0_8
| spl0_9
| spl0_10
| ~ spl0_11
| ~ spl0_12
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| ~ spl0_16
| ~ spl0_17
| ~ spl0_18
| ~ spl0_19
| ~ spl0_20
| ~ spl0_21
| ~ spl0_22
| ~ spl0_23
| ~ spl0_24
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f237,f335,f331,f327,f323,f319,f315,f311,f307,f303,f299,f295,f291,f287,f283,f279,f275,f271,f267,f263,f259,f255,f251,f247,f243,f239]) ).
fof(f339,plain,
spl0_13,
inference(avatar_split_clause,[],[f95,f287]) ).
fof(f340,plain,
spl0_24,
inference(avatar_split_clause,[],[f94,f331]) ).
fof(f341,plain,
~ spl0_10,
inference(avatar_split_clause,[],[f201,f275]) ).
fof(f342,plain,
spl0_16,
inference(avatar_split_clause,[],[f87,f299]) ).
fof(f343,plain,
next_to(house_1,house_2),
inference(resolution,[],[f209,f212]) ).
fof(f349,plain,
next_to(house_4,house_3),
inference(resolution,[],[f210,f214]) ).
fof(f351,plain,
( ~ person(english)
| ~ drives(english,porsche)
| spl0_17 ),
inference(resolution,[],[f92,f305]) ).
fof(f354,definition,
( spl0_26
<=> house(house_4) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f356,plain,
( ~ house(house_4)
| spl0_26 ),
inference(avatar_component_clause,[],[f354]) ).
fof(f358,definition,
( spl0_27
<=> lives(english,house_4) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f362,plain,
( $false
| spl0_26 ),
inference(resolution,[],[f356,f64]) ).
fof(f363,plain,
spl0_26,
inference(avatar_contradiction_clause,[],[f362]) ).
fof(f364,plain,
( lives(english,house_1)
| ~ house(house_1)
| spl0_10 ),
inference(resolution,[],[f131,f276]) ).
fof(f366,definition,
( spl0_28
<=> house(house_1) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f368,plain,
( ~ house(house_1)
| spl0_28 ),
inference(avatar_component_clause,[],[f366]) ).
fof(f370,definition,
( spl0_29
<=> lives(english,house_1) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f373,plain,
( ~ spl0_28
| spl0_29
| spl0_10 ),
inference(avatar_split_clause,[],[f364,f275,f370,f366]) ).
fof(f374,plain,
( $false
| spl0_28 ),
inference(resolution,[],[f368,f61]) ).
fof(f375,plain,
spl0_28,
inference(avatar_contradiction_clause,[],[f374]) ).
fof(f378,definition,
( spl0_30
<=> house(house_2) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f380,plain,
( ~ house(house_2)
| spl0_30 ),
inference(avatar_component_clause,[],[f378]) ).
fof(f382,definition,
( spl0_31
<=> lives(english,house_2) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f386,plain,
( $false
| spl0_30 ),
inference(resolution,[],[f380,f62]) ).
fof(f387,plain,
spl0_30,
inference(avatar_contradiction_clause,[],[f386]) ).
fof(f388,plain,
( lives(english,house_5)
| ~ house(house_5)
| spl0_8 ),
inference(resolution,[],[f133,f268]) ).
fof(f390,definition,
( spl0_32
<=> house(house_5) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f392,plain,
( ~ house(house_5)
| spl0_32 ),
inference(avatar_component_clause,[],[f390]) ).
fof(f394,definition,
( spl0_33
<=> lives(english,house_5) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f396,plain,
( lives(english,house_5)
| ~ spl0_33 ),
inference(avatar_component_clause,[],[f394]) ).
fof(f397,plain,
( ~ spl0_32
| spl0_33
| spl0_8 ),
inference(avatar_split_clause,[],[f388,f267,f394,f390]) ).
fof(f398,plain,
( $false
| spl0_32 ),
inference(resolution,[],[f392,f65]) ).
fof(f399,plain,
spl0_32,
inference(avatar_contradiction_clause,[],[f398]) ).
fof(f400,plain,
( lives(spaniard,house_1)
| ~ house(house_1)
| spl0_10 ),
inference(resolution,[],[f134,f276]) ).
fof(f402,definition,
( spl0_34
<=> lives(spaniard,house_1) ),
introduced(definition,[new_symbols(definition,[spl0_34])],[avatar_definition]) ).
fof(f405,plain,
( ~ spl0_28
| spl0_34
| spl0_10 ),
inference(avatar_split_clause,[],[f400,f275,f402,f366]) ).
fof(f406,plain,
( ~ drinks(english,orange)
| ~ drinks(spaniard,orange) ),
inference(resolution,[],[f140,f191]) ).
fof(f410,plain,
( ~ drinks(english,water)
| ~ drinks(spaniard,water) ),
inference(resolution,[],[f140,f192]) ).
fof(f412,definition,
( spl0_35
<=> drinks(spaniard,water) ),
introduced(definition,[new_symbols(definition,[spl0_35])],[avatar_definition]) ).
fof(f414,plain,
( ~ drinks(spaniard,water)
| spl0_35 ),
inference(avatar_component_clause,[],[f412]) ).
fof(f416,definition,
( spl0_36
<=> drinks(english,water) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f418,plain,
( ~ drinks(english,water)
| spl0_36 ),
inference(avatar_component_clause,[],[f416]) ).
fof(f419,plain,
( ~ spl0_35
| ~ spl0_36 ),
inference(avatar_split_clause,[],[f410,f416,f412]) ).
fof(f421,definition,
( spl0_37
<=> drinks(spaniard,tea) ),
introduced(definition,[new_symbols(definition,[spl0_37])],[avatar_definition]) ).
fof(f425,definition,
( spl0_38
<=> drinks(english,tea) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f430,definition,
( spl0_39
<=> drinks(spaniard,coffee) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f431,plain,
( drinks(spaniard,coffee)
| ~ spl0_39 ),
inference(avatar_component_clause,[],[f430]) ).
fof(f434,definition,
( spl0_40
<=> drinks(english,coffee) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f435,plain,
( drinks(english,coffee)
| ~ spl0_40 ),
inference(avatar_component_clause,[],[f434]) ).
fof(f438,plain,
( ~ drinks(english,orange)
| ~ drinks(norwegian,orange) ),
inference(resolution,[],[f141,f191]) ).
fof(f442,plain,
( ~ drinks(english,water)
| ~ drinks(norwegian,water) ),
inference(resolution,[],[f141,f192]) ).
fof(f444,definition,
( spl0_41
<=> drinks(norwegian,orange) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f448,definition,
( spl0_42
<=> drinks(english,orange) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f451,plain,
( ~ spl0_41
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f438,f448,f444]) ).
fof(f452,plain,
( ~ drinks(english,orange)
| ~ drinks(ukranian,orange) ),
inference(resolution,[],[f142,f191]) ).
fof(f454,plain,
( ~ drinks(english,tea)
| ~ drinks(ukranian,tea) ),
inference(resolution,[],[f142,f190]) ).
fof(f457,plain,
( ~ drinks(english,orange)
| ~ drinks(japanese,orange) ),
inference(resolution,[],[f143,f191]) ).
fof(f461,plain,
( ~ drinks(english,water)
| ~ drinks(japanese,water) ),
inference(resolution,[],[f143,f192]) ).
fof(f462,plain,
( ~ drinks(spaniard,orange)
| ~ drinks(norwegian,orange) ),
inference(resolution,[],[f144,f191]) ).
fof(f466,plain,
( ~ drinks(spaniard,water)
| ~ drinks(norwegian,water) ),
inference(resolution,[],[f144,f192]) ).
fof(f468,definition,
( spl0_43
<=> drinks(norwegian,milk) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f469,plain,
( drinks(norwegian,milk)
| ~ spl0_43 ),
inference(avatar_component_clause,[],[f468]) ).
fof(f472,definition,
( spl0_44
<=> drinks(spaniard,milk) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f473,plain,
( drinks(spaniard,milk)
| ~ spl0_44 ),
inference(avatar_component_clause,[],[f472]) ).
fof(f476,plain,
( ~ drinks(spaniard,orange)
| ~ drinks(ukranian,orange) ),
inference(resolution,[],[f145,f191]) ).
fof(f478,plain,
( ~ drinks(spaniard,tea)
| ~ drinks(ukranian,tea) ),
inference(resolution,[],[f145,f190]) ).
fof(f481,plain,
( ~ drinks(spaniard,orange)
| ~ drinks(japanese,orange) ),
inference(resolution,[],[f146,f191]) ).
fof(f482,plain,
( ~ drinks(spaniard,coffee)
| ~ drinks(japanese,coffee) ),
inference(resolution,[],[f146,f194]) ).
fof(f484,plain,
( ~ drinks(spaniard,milk)
| ~ drinks(japanese,milk) ),
inference(resolution,[],[f146,f193]) ).
fof(f485,plain,
( ~ drinks(spaniard,water)
| ~ drinks(japanese,water) ),
inference(resolution,[],[f146,f192]) ).
fof(f486,plain,
( ~ drinks(norwegian,orange)
| ~ drinks(ukranian,orange) ),
inference(resolution,[],[f147,f191]) ).
fof(f488,plain,
( ~ drinks(norwegian,tea)
| ~ drinks(ukranian,tea) ),
inference(resolution,[],[f147,f190]) ).
fof(f492,definition,
( spl0_45
<=> drinks(norwegian,tea) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f495,plain,
( ~ spl0_24
| ~ spl0_45 ),
inference(avatar_split_clause,[],[f488,f492,f331]) ).
fof(f501,definition,
( spl0_47
<=> drinks(norwegian,coffee) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f502,plain,
( drinks(norwegian,coffee)
| ~ spl0_47 ),
inference(avatar_component_clause,[],[f501]) ).
fof(f505,plain,
( ~ drinks(norwegian,orange)
| ~ drinks(japanese,orange) ),
inference(resolution,[],[f148,f191]) ).
fof(f509,plain,
( ~ drinks(norwegian,water)
| ~ drinks(japanese,water) ),
inference(resolution,[],[f148,f192]) ).
fof(f510,plain,
( ~ drinks(ukranian,orange)
| ~ drinks(japanese,orange) ),
inference(resolution,[],[f149,f191]) ).
fof(f512,plain,
( ~ drinks(ukranian,tea)
| ~ drinks(japanese,tea) ),
inference(resolution,[],[f149,f190]) ).
fof(f516,definition,
( spl0_48
<=> drinks(japanese,water) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f518,plain,
( ~ drinks(japanese,water)
| spl0_48 ),
inference(avatar_component_clause,[],[f516]) ).
fof(f525,definition,
( spl0_50
<=> drinks(japanese,milk) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f526,plain,
( drinks(japanese,milk)
| ~ spl0_50 ),
inference(avatar_component_clause,[],[f525]) ).
fof(f534,definition,
( spl0_52
<=> drinks(japanese,tea) ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f537,plain,
( ~ spl0_52
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f512,f331,f534]) ).
fof(f539,definition,
( spl0_53
<=> drinks(japanese,orange) ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f543,definition,
( spl0_54
<=> drinks(ukranian,orange) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f546,plain,
( ~ spl0_53
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f510,f543,f539]) ).
fof(f548,plain,
( ~ drives(english,saab)
| ~ drives(spaniard,saab) ),
inference(resolution,[],[f150,f189]) ).
fof(f549,plain,
( ~ drives(english,porsche)
| ~ drives(spaniard,porsche) ),
inference(resolution,[],[f150,f188]) ).
fof(f553,definition,
( spl0_55
<=> drives(spaniard,jaguar) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f555,plain,
( ~ drives(spaniard,jaguar)
| spl0_55 ),
inference(avatar_component_clause,[],[f553]) ).
fof(f557,definition,
( spl0_56
<=> drives(english,jaguar) ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f559,plain,
( ~ drives(english,jaguar)
| spl0_56 ),
inference(avatar_component_clause,[],[f557]) ).
fof(f562,definition,
( spl0_57
<=> drives(spaniard,saab) ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f563,plain,
( drives(spaniard,saab)
| ~ spl0_57 ),
inference(avatar_component_clause,[],[f562]) ).
fof(f566,definition,
( spl0_58
<=> drives(english,saab) ),
introduced(definition,[new_symbols(definition,[spl0_58])],[avatar_definition]) ).
fof(f569,plain,
( ~ spl0_57
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f548,f566,f562]) ).
fof(f571,definition,
( spl0_59
<=> drives(spaniard,masserati) ),
introduced(definition,[new_symbols(definition,[spl0_59])],[avatar_definition]) ).
fof(f572,plain,
( drives(spaniard,masserati)
| ~ spl0_59 ),
inference(avatar_component_clause,[],[f571]) ).
fof(f575,definition,
( spl0_60
<=> drives(english,masserati) ),
introduced(definition,[new_symbols(definition,[spl0_60])],[avatar_definition]) ).
fof(f576,plain,
( drives(english,masserati)
| ~ spl0_60 ),
inference(avatar_component_clause,[],[f575]) ).
fof(f580,plain,
( ~ drives(english,saab)
| ~ drives(norwegian,saab) ),
inference(resolution,[],[f151,f189]) ).
fof(f585,definition,
( spl0_61
<=> drives(norwegian,honda) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f586,plain,
( drives(norwegian,honda)
| ~ spl0_61 ),
inference(avatar_component_clause,[],[f585]) ).
fof(f589,definition,
( spl0_62
<=> drives(english,honda) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f590,plain,
( drives(english,honda)
| ~ spl0_62 ),
inference(avatar_component_clause,[],[f589]) ).
fof(f594,plain,
( ~ drives(english,saab)
| ~ drives(ukranian,saab) ),
inference(resolution,[],[f152,f189]) ).
fof(f595,plain,
( ~ drives(english,porsche)
| ~ drives(ukranian,porsche) ),
inference(resolution,[],[f152,f188]) ).
fof(f602,plain,
( ~ drives(english,jaguar)
| ~ drives(japanese,jaguar) ),
inference(resolution,[],[f153,f185]) ).
fof(f604,plain,
( ~ drives(spaniard,saab)
| ~ drives(norwegian,saab) ),
inference(resolution,[],[f154,f189]) ).
fof(f605,plain,
( ~ drives(spaniard,porsche)
| ~ drives(norwegian,porsche) ),
inference(resolution,[],[f154,f188]) ).
fof(f609,definition,
( spl0_63
<=> drives(norwegian,porsche) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f613,definition,
( spl0_64
<=> drives(spaniard,porsche) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f616,plain,
( ~ spl0_63
| ~ spl0_64 ),
inference(avatar_split_clause,[],[f605,f613,f609]) ).
fof(f618,plain,
( ~ drives(spaniard,saab)
| ~ drives(ukranian,saab) ),
inference(resolution,[],[f155,f189]) ).
fof(f626,plain,
( ~ drives(spaniard,jaguar)
| ~ drives(japanese,jaguar) ),
inference(resolution,[],[f156,f185]) ).
fof(f628,plain,
( ~ drives(norwegian,saab)
| ~ drives(ukranian,saab) ),
inference(resolution,[],[f157,f189]) ).
fof(f633,definition,
( spl0_65
<=> drives(ukranian,jaguar) ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f635,plain,
( ~ drives(ukranian,jaguar)
| spl0_65 ),
inference(avatar_component_clause,[],[f633]) ).
fof(f637,definition,
( spl0_66
<=> drives(norwegian,jaguar) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f639,plain,
( ~ drives(norwegian,jaguar)
| spl0_66 ),
inference(avatar_component_clause,[],[f637]) ).
fof(f645,plain,
( ~ drives(norwegian,jaguar)
| ~ drives(japanese,jaguar) ),
inference(resolution,[],[f158,f185]) ).
fof(f651,definition,
( spl0_68
<=> drives(norwegian,saab) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f659,plain,
( ~ drives(ukranian,jaguar)
| ~ drives(japanese,jaguar) ),
inference(resolution,[],[f159,f185]) ).
fof(f665,definition,
( spl0_70
<=> drives(ukranian,honda) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f666,plain,
( drives(ukranian,honda)
| ~ spl0_70 ),
inference(avatar_component_clause,[],[f665]) ).
fof(f674,definition,
( spl0_72
<=> drives(ukranian,porsche) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f683,definition,
( spl0_74
<=> drives(ukranian,masserati) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f684,plain,
( drives(ukranian,masserati)
| ~ spl0_74 ),
inference(avatar_component_clause,[],[f683]) ).
fof(f687,plain,
( ~ owns(english,dog)
| ~ owns(spaniard,dog) ),
inference(resolution,[],[f160,f195]) ).
fof(f688,plain,
( ~ owns(english,snails)
| ~ owns(spaniard,snails) ),
inference(resolution,[],[f160,f197]) ).
fof(f697,definition,
( spl0_76
<=> owns(english,zebra) ),
introduced(definition,[new_symbols(definition,[spl0_76])],[avatar_definition]) ).
fof(f699,plain,
( ~ owns(english,zebra)
| spl0_76 ),
inference(avatar_component_clause,[],[f697]) ).
fof(f706,definition,
( spl0_78
<=> owns(english,fox) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f707,plain,
( owns(english,fox)
| ~ spl0_78 ),
inference(avatar_component_clause,[],[f706]) ).
fof(f715,definition,
( spl0_80
<=> owns(english,horse) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f716,plain,
( owns(english,horse)
| ~ spl0_80 ),
inference(avatar_component_clause,[],[f715]) ).
fof(f720,definition,
( spl0_81
<=> owns(english,dog) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f723,plain,
( ~ spl0_16
| ~ spl0_81 ),
inference(avatar_split_clause,[],[f687,f720,f299]) ).
fof(f725,plain,
( ~ owns(english,snails)
| ~ owns(norwegian,snails) ),
inference(resolution,[],[f161,f197]) ).
fof(f727,plain,
( ~ owns(english,fox)
| ~ owns(norwegian,fox) ),
inference(resolution,[],[f161,f199]) ).
fof(f728,plain,
( ~ owns(english,zebra)
| ~ owns(norwegian,zebra) ),
inference(resolution,[],[f161,f196]) ).
fof(f730,plain,
( ~ owns(english,snails)
| ~ owns(ukranian,snails) ),
inference(resolution,[],[f162,f197]) ).
fof(f735,plain,
( ~ owns(english,snails)
| ~ owns(japanese,snails) ),
inference(resolution,[],[f163,f197]) ).
fof(f737,plain,
( ~ owns(english,fox)
| ~ owns(japanese,fox) ),
inference(resolution,[],[f163,f199]) ).
fof(f738,plain,
( ~ owns(english,zebra)
| ~ owns(japanese,zebra) ),
inference(resolution,[],[f163,f196]) ).
fof(f739,plain,
( ~ owns(spaniard,dog)
| ~ owns(norwegian,dog) ),
inference(resolution,[],[f164,f195]) ).
fof(f740,plain,
( ~ owns(spaniard,snails)
| ~ owns(norwegian,snails) ),
inference(resolution,[],[f164,f197]) ).
fof(f745,definition,
( spl0_82
<=> owns(norwegian,snails) ),
introduced(definition,[new_symbols(definition,[spl0_82])],[avatar_definition]) ).
fof(f747,plain,
( ~ owns(norwegian,snails)
| spl0_82 ),
inference(avatar_component_clause,[],[f745]) ).
fof(f749,definition,
( spl0_83
<=> owns(spaniard,snails) ),
introduced(definition,[new_symbols(definition,[spl0_83])],[avatar_definition]) ).
fof(f751,plain,
( ~ owns(spaniard,snails)
| spl0_83 ),
inference(avatar_component_clause,[],[f749]) ).
fof(f752,plain,
( ~ spl0_82
| ~ spl0_83 ),
inference(avatar_split_clause,[],[f740,f749,f745]) ).
fof(f754,definition,
( spl0_84
<=> owns(norwegian,dog) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f757,plain,
( ~ spl0_84
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f739,f299,f754]) ).
fof(f758,plain,
( ~ person(norwegian)
| ~ drives(norwegian,porsche)
| spl0_82 ),
inference(resolution,[],[f747,f92]) ).
fof(f759,plain,
( ~ person(spaniard)
| ~ drives(spaniard,porsche)
| spl0_83 ),
inference(resolution,[],[f751,f92]) ).
fof(f760,plain,
( ~ owns(spaniard,dog)
| ~ owns(ukranian,dog) ),
inference(resolution,[],[f165,f195]) ).
fof(f761,plain,
( ~ owns(spaniard,snails)
| ~ owns(ukranian,snails) ),
inference(resolution,[],[f165,f197]) ).
fof(f766,definition,
( spl0_85
<=> owns(ukranian,dog) ),
introduced(definition,[new_symbols(definition,[spl0_85])],[avatar_definition]) ).
fof(f769,plain,
( ~ spl0_85
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f760,f299,f766]) ).
fof(f770,plain,
( ~ owns(spaniard,dog)
| ~ owns(japanese,dog) ),
inference(resolution,[],[f166,f195]) ).
fof(f771,plain,
( ~ owns(spaniard,snails)
| ~ owns(japanese,snails) ),
inference(resolution,[],[f166,f197]) ).
fof(f776,definition,
( spl0_86
<=> owns(japanese,dog) ),
introduced(definition,[new_symbols(definition,[spl0_86])],[avatar_definition]) ).
fof(f779,plain,
( ~ spl0_86
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f770,f299,f776]) ).
fof(f781,plain,
( ~ owns(norwegian,snails)
| ~ owns(ukranian,snails) ),
inference(resolution,[],[f167,f197]) ).
fof(f784,plain,
( ~ owns(norwegian,zebra)
| ~ owns(ukranian,zebra) ),
inference(resolution,[],[f167,f196]) ).
fof(f786,definition,
( spl0_87
<=> owns(ukranian,zebra) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f788,plain,
( ~ owns(ukranian,zebra)
| spl0_87 ),
inference(avatar_component_clause,[],[f786]) ).
fof(f790,definition,
( spl0_88
<=> owns(norwegian,zebra) ),
introduced(definition,[new_symbols(definition,[spl0_88])],[avatar_definition]) ).
fof(f792,plain,
( ~ owns(norwegian,zebra)
| spl0_88 ),
inference(avatar_component_clause,[],[f790]) ).
fof(f793,plain,
( ~ spl0_87
| ~ spl0_88 ),
inference(avatar_split_clause,[],[f784,f790,f786]) ).
fof(f797,plain,
( ~ owns(norwegian,fox)
| ~ owns(japanese,fox) ),
inference(resolution,[],[f168,f199]) ).
fof(f798,plain,
( ~ owns(norwegian,zebra)
| ~ owns(japanese,zebra) ),
inference(resolution,[],[f168,f196]) ).
fof(f800,definition,
( spl0_89
<=> owns(japanese,horse) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f801,plain,
( owns(japanese,horse)
| ~ spl0_89 ),
inference(avatar_component_clause,[],[f800]) ).
fof(f804,definition,
( spl0_90
<=> owns(norwegian,horse) ),
introduced(definition,[new_symbols(definition,[spl0_90])],[avatar_definition]) ).
fof(f805,plain,
( owns(norwegian,horse)
| ~ spl0_90 ),
inference(avatar_component_clause,[],[f804]) ).
fof(f809,plain,
( ~ owns(ukranian,snails)
| ~ owns(japanese,snails) ),
inference(resolution,[],[f169,f197]) ).
fof(f812,plain,
( ~ owns(ukranian,zebra)
| ~ owns(japanese,zebra) ),
inference(resolution,[],[f169,f196]) ).
fof(f814,definition,
( spl0_91
<=> owns(japanese,fox) ),
introduced(definition,[new_symbols(definition,[spl0_91])],[avatar_definition]) ).
fof(f815,plain,
( owns(japanese,fox)
| ~ spl0_91 ),
inference(avatar_component_clause,[],[f814]) ).
fof(f818,definition,
( spl0_92
<=> owns(ukranian,fox) ),
introduced(definition,[new_symbols(definition,[spl0_92])],[avatar_definition]) ).
fof(f819,plain,
( owns(ukranian,fox)
| ~ spl0_92 ),
inference(avatar_component_clause,[],[f818]) ).
fof(f823,definition,
( spl0_93
<=> owns(japanese,snails) ),
introduced(definition,[new_symbols(definition,[spl0_93])],[avatar_definition]) ).
fof(f827,definition,
( spl0_94
<=> owns(ukranian,snails) ),
introduced(definition,[new_symbols(definition,[spl0_94])],[avatar_definition]) ).
fof(f829,plain,
( ~ owns(ukranian,snails)
| spl0_94 ),
inference(avatar_component_clause,[],[f827]) ).
fof(f830,plain,
( ~ spl0_93
| ~ spl0_94 ),
inference(avatar_split_clause,[],[f809,f827,f823]) ).
fof(f832,plain,
( ~ person(ukranian)
| ~ drives(ukranian,porsche)
| spl0_94 ),
inference(resolution,[],[f829,f92]) ).
fof(f833,plain,
( ~ is_color(house_1,red)
| ~ is_color(house_2,red) ),
inference(resolution,[],[f170,f180]) ).
fof(f834,plain,
( ~ is_color(house_1,yellow)
| ~ is_color(house_2,yellow) ),
inference(resolution,[],[f170,f182]) ).
fof(f835,plain,
( ~ is_color(house_1,blue)
| ~ is_color(house_2,blue) ),
inference(resolution,[],[f170,f184]) ).
fof(f843,definition,
( spl0_96
<=> is_color(house_1,ivory) ),
introduced(definition,[new_symbols(definition,[spl0_96])],[avatar_definition]) ).
fof(f845,plain,
( ~ is_color(house_1,ivory)
| spl0_96 ),
inference(avatar_component_clause,[],[f843]) ).
fof(f848,definition,
( spl0_97
<=> is_color(house_2,green) ),
introduced(definition,[new_symbols(definition,[spl0_97])],[avatar_definition]) ).
fof(f850,plain,
( ~ is_color(house_2,green)
| spl0_97 ),
inference(avatar_component_clause,[],[f848]) ).
fof(f852,definition,
( spl0_98
<=> is_color(house_1,green) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f854,plain,
( ~ is_color(house_1,green)
| spl0_98 ),
inference(avatar_component_clause,[],[f852]) ).
fof(f857,definition,
( spl0_99
<=> is_color(house_2,red) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f859,plain,
( ~ is_color(house_2,red)
| spl0_99 ),
inference(avatar_component_clause,[],[f857]) ).
fof(f861,definition,
( spl0_100
<=> is_color(house_1,red) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f864,plain,
( ~ spl0_99
| ~ spl0_100 ),
inference(avatar_split_clause,[],[f833,f861,f857]) ).
fof(f865,plain,
( ~ is_color(house_1,red)
| ~ is_color(house_3,red) ),
inference(resolution,[],[f171,f180]) ).
fof(f866,plain,
( ~ is_color(house_1,yellow)
| ~ is_color(house_3,yellow) ),
inference(resolution,[],[f171,f182]) ).
fof(f868,plain,
( ~ is_color(house_1,green)
| ~ is_color(house_3,green) ),
inference(resolution,[],[f171,f181]) ).
fof(f869,plain,
( ~ is_color(house_1,ivory)
| ~ is_color(house_3,ivory) ),
inference(resolution,[],[f171,f183]) ).
fof(f871,definition,
( spl0_101
<=> is_color(house_3,blue) ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f875,definition,
( spl0_102
<=> is_color(house_1,blue) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f879,plain,
( ~ is_color(house_1,red)
| ~ is_color(house_4,red) ),
inference(resolution,[],[f172,f180]) ).
fof(f880,plain,
( ~ is_color(house_1,yellow)
| ~ is_color(house_4,yellow) ),
inference(resolution,[],[f172,f182]) ).
fof(f882,plain,
( ~ is_color(house_1,green)
| ~ is_color(house_4,green) ),
inference(resolution,[],[f172,f181]) ).
fof(f883,plain,
( ~ is_color(house_1,ivory)
| ~ is_color(house_4,ivory) ),
inference(resolution,[],[f172,f183]) ).
fof(f884,plain,
( ~ is_color(house_1,red)
| ~ is_color(house_5,red) ),
inference(resolution,[],[f173,f180]) ).
fof(f885,plain,
( ~ is_color(house_1,yellow)
| ~ is_color(house_5,yellow) ),
inference(resolution,[],[f173,f182]) ).
fof(f887,plain,
( ~ is_color(house_1,green)
| ~ is_color(house_5,green) ),
inference(resolution,[],[f173,f181]) ).
fof(f888,plain,
( ~ is_color(house_1,ivory)
| ~ is_color(house_5,ivory) ),
inference(resolution,[],[f173,f183]) ).
fof(f889,plain,
( ~ is_color(house_2,red)
| ~ is_color(house_3,red) ),
inference(resolution,[],[f174,f180]) ).
fof(f891,plain,
( ~ is_color(house_2,blue)
| ~ is_color(house_3,blue) ),
inference(resolution,[],[f174,f184]) ).
fof(f895,definition,
( spl0_103
<=> is_color(house_3,yellow) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f897,plain,
( ~ is_color(house_3,yellow)
| spl0_103 ),
inference(avatar_component_clause,[],[f895]) ).
fof(f899,definition,
( spl0_104
<=> is_color(house_2,yellow) ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f901,plain,
( ~ is_color(house_2,yellow)
| spl0_104 ),
inference(avatar_component_clause,[],[f899]) ).
fof(f903,plain,
( ~ is_color(house_2,red)
| ~ is_color(house_4,red) ),
inference(resolution,[],[f175,f180]) ).
fof(f905,plain,
( ~ is_color(house_2,blue)
| ~ is_color(house_4,blue) ),
inference(resolution,[],[f175,f184]) ).
fof(f906,plain,
( ~ is_color(house_2,green)
| ~ is_color(house_4,green) ),
inference(resolution,[],[f175,f181]) ).
fof(f908,plain,
( ~ is_color(house_2,red)
| ~ is_color(house_5,red) ),
inference(resolution,[],[f176,f180]) ).
fof(f910,plain,
( ~ is_color(house_2,blue)
| ~ is_color(house_5,blue) ),
inference(resolution,[],[f176,f184]) ).
fof(f911,plain,
( ~ is_color(house_2,green)
| ~ is_color(house_5,green) ),
inference(resolution,[],[f176,f181]) ).
fof(f913,plain,
( ~ is_color(house_3,red)
| ~ is_color(house_4,red) ),
inference(resolution,[],[f177,f180]) ).
fof(f914,plain,
( ~ is_color(house_3,yellow)
| ~ is_color(house_4,yellow) ),
inference(resolution,[],[f177,f182]) ).
fof(f916,plain,
( ~ is_color(house_3,green)
| ~ is_color(house_4,green) ),
inference(resolution,[],[f177,f181]) ).
fof(f917,plain,
( ~ is_color(house_3,ivory)
| ~ is_color(house_4,ivory) ),
inference(resolution,[],[f177,f183]) ).
fof(f919,definition,
( spl0_105
<=> is_color(house_4,green) ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f921,plain,
( ~ is_color(house_4,green)
| spl0_105 ),
inference(avatar_component_clause,[],[f919]) ).
fof(f923,definition,
( spl0_106
<=> is_color(house_3,green) ),
introduced(definition,[new_symbols(definition,[spl0_106])],[avatar_definition]) ).
fof(f925,plain,
( ~ is_color(house_3,green)
| spl0_106 ),
inference(avatar_component_clause,[],[f923]) ).
fof(f926,plain,
( ~ spl0_105
| ~ spl0_106 ),
inference(avatar_split_clause,[],[f916,f923,f919]) ).
fof(f927,plain,
( ~ is_color(house_3,red)
| ~ is_color(house_5,red) ),
inference(resolution,[],[f178,f180]) ).
fof(f928,plain,
( ~ is_color(house_3,yellow)
| ~ is_color(house_5,yellow) ),
inference(resolution,[],[f178,f182]) ).
fof(f930,plain,
( ~ is_color(house_3,green)
| ~ is_color(house_5,green) ),
inference(resolution,[],[f178,f181]) ).
fof(f931,plain,
( ~ is_color(house_3,ivory)
| ~ is_color(house_5,ivory) ),
inference(resolution,[],[f178,f183]) ).
fof(f933,definition,
( spl0_107
<=> is_color(house_5,ivory) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f935,plain,
( ~ is_color(house_5,ivory)
| spl0_107 ),
inference(avatar_component_clause,[],[f933]) ).
fof(f937,definition,
( spl0_108
<=> is_color(house_3,ivory) ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f939,plain,
( ~ is_color(house_3,ivory)
| spl0_108 ),
inference(avatar_component_clause,[],[f937]) ).
fof(f940,plain,
( ~ spl0_107
| ~ spl0_108 ),
inference(avatar_split_clause,[],[f931,f937,f933]) ).
fof(f941,plain,
( ~ is_color(house_4,red)
| ~ is_color(house_5,red) ),
inference(resolution,[],[f179,f180]) ).
fof(f942,plain,
( ~ is_color(house_4,yellow)
| ~ is_color(house_5,yellow) ),
inference(resolution,[],[f179,f182]) ).
fof(f944,plain,
( ~ is_color(house_4,green)
| ~ is_color(house_5,green) ),
inference(resolution,[],[f179,f181]) ).
fof(f945,plain,
( ~ is_color(house_4,ivory)
| ~ is_color(house_5,ivory) ),
inference(resolution,[],[f179,f183]) ).
fof(f947,definition,
( spl0_109
<=> is_color(house_5,blue) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f951,definition,
( spl0_110
<=> is_color(house_4,blue) ),
introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition]) ).
fof(f953,plain,
( ~ is_color(house_4,blue)
| spl0_110 ),
inference(avatar_component_clause,[],[f951]) ).
fof(f956,definition,
( spl0_111
<=> is_color(house_5,yellow) ),
introduced(definition,[new_symbols(definition,[spl0_111])],[avatar_definition]) ).
fof(f958,plain,
( ~ is_color(house_5,yellow)
| spl0_111 ),
inference(avatar_component_clause,[],[f956]) ).
fof(f960,definition,
( spl0_112
<=> is_color(house_4,yellow) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f962,plain,
( ~ is_color(house_4,yellow)
| spl0_112 ),
inference(avatar_component_clause,[],[f960]) ).
fof(f963,plain,
( ~ spl0_111
| ~ spl0_112 ),
inference(avatar_split_clause,[],[f942,f960,f956]) ).
fof(f965,definition,
( spl0_113
<=> is_color(house_5,red) ),
introduced(definition,[new_symbols(definition,[spl0_113])],[avatar_definition]) ).
fof(f967,plain,
( ~ is_color(house_5,red)
| spl0_113 ),
inference(avatar_component_clause,[],[f965]) ).
fof(f969,definition,
( spl0_114
<=> is_color(house_4,red) ),
introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition]) ).
fof(f971,plain,
( ~ is_color(house_4,red)
| spl0_114 ),
inference(avatar_component_clause,[],[f969]) ).
fof(f972,plain,
( ~ spl0_113
| ~ spl0_114 ),
inference(avatar_split_clause,[],[f941,f969,f965]) ).
fof(f974,plain,
( ~ house(house_2)
| lives(english,house_2)
| spl0_99 ),
inference(resolution,[],[f200,f859]) ).
fof(f975,plain,
( ~ house(house_3)
| lives(english,house_3)
| spl0_3 ),
inference(resolution,[],[f200,f249]) ).
fof(f976,plain,
( ~ house(house_4)
| lives(english,house_4)
| spl0_114 ),
inference(resolution,[],[f200,f971]) ).
fof(f977,plain,
( ~ house(house_5)
| lives(english,house_5)
| spl0_113 ),
inference(resolution,[],[f200,f967]) ).
fof(f978,plain,
( spl0_33
| ~ spl0_32
| spl0_113 ),
inference(avatar_split_clause,[],[f977,f965,f390,f394]) ).
fof(f979,plain,
( spl0_27
| ~ spl0_26
| spl0_114 ),
inference(avatar_split_clause,[],[f976,f969,f354,f358]) ).
fof(f981,definition,
( spl0_115
<=> house(house_3) ),
introduced(definition,[new_symbols(definition,[spl0_115])],[avatar_definition]) ).
fof(f983,plain,
( ~ house(house_3)
| spl0_115 ),
inference(avatar_component_clause,[],[f981]) ).
fof(f984,plain,
( spl0_7
| ~ spl0_115
| spl0_3 ),
inference(avatar_split_clause,[],[f975,f247,f981,f263]) ).
fof(f985,plain,
( spl0_31
| ~ spl0_30
| spl0_99 ),
inference(avatar_split_clause,[],[f974,f857,f378,f382]) ).
fof(f986,plain,
( $false
| spl0_115 ),
inference(resolution,[],[f983,f63]) ).
fof(f987,plain,
spl0_115,
inference(avatar_contradiction_clause,[],[f986]) ).
fof(f989,plain,
! [X0,X1] :
( ~ left_of(X1,X0)
| ~ next_to(X1,X0)
| next_to(X0,X1) ),
inference(resolution,[],[f211,f209]) ).
fof(f991,plain,
( ~ left_of(house_1,house_3)
| ~ next_to(house_1,house_3) ),
inference(resolution,[],[f211,f218]) ).
fof(f992,plain,
( ~ left_of(house_1,house_4)
| ~ next_to(house_1,house_4) ),
inference(resolution,[],[f211,f219]) ).
fof(f993,plain,
( ~ left_of(house_1,house_5)
| ~ next_to(house_1,house_5) ),
inference(resolution,[],[f211,f220]) ).
fof(f998,plain,
( ~ left_of(house_3,house_5)
| ~ next_to(house_3,house_5) ),
inference(resolution,[],[f211,f228]) ).
fof(f1005,plain,
( ~ left_of(house_1,house_5)
| ~ next_to(house_5,house_1) ),
inference(resolution,[],[f211,f220]) ).
fof(f1007,plain,
( ~ left_of(house_2,house_4)
| ~ next_to(house_4,house_2) ),
inference(resolution,[],[f211,f223]) ).
fof(f1008,plain,
( ~ left_of(house_2,house_5)
| ~ next_to(house_5,house_2) ),
inference(resolution,[],[f211,f224]) ).
fof(f1010,plain,
( ~ left_of(house_3,house_5)
| ~ next_to(house_5,house_3) ),
inference(resolution,[],[f211,f228]) ).
fof(f1012,plain,
! [X0] :
( ~ left_of(X0,X0)
| ~ next_to(X0,X0) ),
inference(factoring,[],[f211]) ).
fof(f1014,definition,
( spl0_116
<=> next_to(house_5,house_3) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f1016,plain,
( ~ next_to(house_5,house_3)
| spl0_116 ),
inference(avatar_component_clause,[],[f1014]) ).
fof(f1018,definition,
( spl0_117
<=> left_of(house_3,house_5) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f1020,plain,
( ~ left_of(house_3,house_5)
| spl0_117 ),
inference(avatar_component_clause,[],[f1018]) ).
fof(f1021,plain,
( ~ spl0_116
| ~ spl0_117 ),
inference(avatar_split_clause,[],[f1010,f1018,f1014]) ).
fof(f1023,definition,
( spl0_118
<=> next_to(house_5,house_2) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f1025,plain,
( ~ next_to(house_5,house_2)
| spl0_118 ),
inference(avatar_component_clause,[],[f1023]) ).
fof(f1027,definition,
( spl0_119
<=> left_of(house_2,house_5) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f1029,plain,
( ~ left_of(house_2,house_5)
| spl0_119 ),
inference(avatar_component_clause,[],[f1027]) ).
fof(f1030,plain,
( ~ spl0_118
| ~ spl0_119 ),
inference(avatar_split_clause,[],[f1008,f1027,f1023]) ).
fof(f1032,definition,
( spl0_120
<=> next_to(house_4,house_2) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f1034,plain,
( ~ next_to(house_4,house_2)
| spl0_120 ),
inference(avatar_component_clause,[],[f1032]) ).
fof(f1036,definition,
( spl0_121
<=> left_of(house_2,house_4) ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f1038,plain,
( ~ left_of(house_2,house_4)
| spl0_121 ),
inference(avatar_component_clause,[],[f1036]) ).
fof(f1039,plain,
( ~ spl0_120
| ~ spl0_121 ),
inference(avatar_split_clause,[],[f1007,f1036,f1032]) ).
fof(f1041,definition,
( spl0_122
<=> next_to(house_5,house_1) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f1043,plain,
( ~ next_to(house_5,house_1)
| spl0_122 ),
inference(avatar_component_clause,[],[f1041]) ).
fof(f1045,definition,
( spl0_123
<=> left_of(house_1,house_5) ),
introduced(definition,[new_symbols(definition,[spl0_123])],[avatar_definition]) ).
fof(f1047,plain,
( ~ left_of(house_1,house_5)
| spl0_123 ),
inference(avatar_component_clause,[],[f1045]) ).
fof(f1048,plain,
( ~ spl0_122
| ~ spl0_123 ),
inference(avatar_split_clause,[],[f1005,f1045,f1041]) ).
fof(f1054,definition,
( spl0_125
<=> left_of(house_1,house_4) ),
introduced(definition,[new_symbols(definition,[spl0_125])],[avatar_definition]) ).
fof(f1056,plain,
( ~ left_of(house_1,house_4)
| spl0_125 ),
inference(avatar_component_clause,[],[f1054]) ).
fof(f1063,definition,
( spl0_127
<=> left_of(house_1,house_3) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f1065,plain,
( ~ left_of(house_1,house_3)
| spl0_127 ),
inference(avatar_component_clause,[],[f1063]) ).
fof(f1068,definition,
( spl0_128
<=> next_to(house_3,house_5) ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f1070,plain,
( ~ next_to(house_3,house_5)
| spl0_128 ),
inference(avatar_component_clause,[],[f1068]) ).
fof(f1071,plain,
( ~ spl0_128
| ~ spl0_117 ),
inference(avatar_split_clause,[],[f998,f1018,f1068]) ).
fof(f1083,definition,
( spl0_131
<=> next_to(house_1,house_5) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f1085,plain,
( ~ next_to(house_1,house_5)
| spl0_131 ),
inference(avatar_component_clause,[],[f1083]) ).
fof(f1086,plain,
( ~ spl0_131
| ~ spl0_123 ),
inference(avatar_split_clause,[],[f993,f1045,f1083]) ).
fof(f1088,definition,
( spl0_132
<=> next_to(house_1,house_4) ),
introduced(definition,[new_symbols(definition,[spl0_132])],[avatar_definition]) ).
fof(f1090,plain,
( ~ next_to(house_1,house_4)
| spl0_132 ),
inference(avatar_component_clause,[],[f1088]) ).
fof(f1091,plain,
( ~ spl0_132
| ~ spl0_125 ),
inference(avatar_split_clause,[],[f992,f1054,f1088]) ).
fof(f1093,definition,
( spl0_133
<=> next_to(house_1,house_3) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f1095,plain,
( ~ next_to(house_1,house_3)
| spl0_133 ),
inference(avatar_component_clause,[],[f1093]) ).
fof(f1096,plain,
( ~ spl0_133
| ~ spl0_127 ),
inference(avatar_split_clause,[],[f991,f1063,f1093]) ).
fof(f1097,plain,
( $false
| spl0_117 ),
inference(resolution,[],[f1020,f235]) ).
fof(f1100,plain,
spl0_117,
inference(avatar_contradiction_clause,[],[f1097]) ).
fof(f1103,plain,
( $false
| spl0_119 ),
inference(resolution,[],[f1029,f234]) ).
fof(f1106,plain,
spl0_119,
inference(avatar_contradiction_clause,[],[f1103]) ).
fof(f1109,plain,
( $false
| spl0_121 ),
inference(resolution,[],[f1038,f230]) ).
fof(f1112,plain,
spl0_121,
inference(avatar_contradiction_clause,[],[f1109]) ).
fof(f1115,plain,
( $false
| spl0_123 ),
inference(resolution,[],[f1047,f233]) ).
fof(f1118,plain,
spl0_123,
inference(avatar_contradiction_clause,[],[f1115]) ).
fof(f1121,plain,
( $false
| spl0_125 ),
inference(resolution,[],[f1056,f229]) ).
fof(f1124,plain,
spl0_125,
inference(avatar_contradiction_clause,[],[f1121]) ).
fof(f1127,plain,
( $false
| spl0_127 ),
inference(resolution,[],[f1065,f225]) ).
fof(f1130,plain,
spl0_127,
inference(avatar_contradiction_clause,[],[f1127]) ).
fof(f1134,plain,
( ! [X0] :
( ~ person(X0)
| ~ drives(X0,masserati)
| ~ house(house_2)
| lives(X0,house_2) )
| spl0_104 ),
inference(resolution,[],[f202,f901]) ).
fof(f1135,plain,
( ! [X0] :
( ~ person(X0)
| ~ drives(X0,masserati)
| ~ house(house_3)
| lives(X0,house_3) )
| spl0_103 ),
inference(resolution,[],[f202,f897]) ).
fof(f1136,plain,
( ! [X0] :
( ~ person(X0)
| ~ drives(X0,masserati)
| ~ house(house_4)
| lives(X0,house_4) )
| spl0_112 ),
inference(resolution,[],[f202,f962]) ).
fof(f1137,plain,
( ! [X0] :
( ~ person(X0)
| ~ drives(X0,masserati)
| ~ house(house_5)
| lives(X0,house_5) )
| spl0_111 ),
inference(resolution,[],[f202,f958]) ).
fof(f1139,definition,
( spl0_134
<=> ! [X0] :
( ~ person(X0)
| lives(X0,house_5)
| ~ drives(X0,masserati) ) ),
introduced(definition,[new_symbols(definition,[spl0_134])],[avatar_definition]) ).
fof(f1140,plain,
( ! [X0] :
( ~ drives(X0,masserati)
| lives(X0,house_5)
| ~ person(X0) )
| ~ spl0_134 ),
inference(avatar_component_clause,[],[f1139]) ).
fof(f1141,plain,
( ~ spl0_32
| spl0_134
| spl0_111 ),
inference(avatar_split_clause,[],[f1137,f956,f1139,f390]) ).
fof(f1143,definition,
( spl0_135
<=> ! [X0] :
( ~ person(X0)
| lives(X0,house_4)
| ~ drives(X0,masserati) ) ),
introduced(definition,[new_symbols(definition,[spl0_135])],[avatar_definition]) ).
fof(f1144,plain,
( ! [X0] :
( ~ drives(X0,masserati)
| lives(X0,house_4)
| ~ person(X0) )
| ~ spl0_135 ),
inference(avatar_component_clause,[],[f1143]) ).
fof(f1145,plain,
( ~ spl0_26
| spl0_135
| spl0_112 ),
inference(avatar_split_clause,[],[f1136,f960,f1143,f354]) ).
fof(f1147,definition,
( spl0_136
<=> ! [X0] :
( ~ person(X0)
| lives(X0,house_3)
| ~ drives(X0,masserati) ) ),
introduced(definition,[new_symbols(definition,[spl0_136])],[avatar_definition]) ).
fof(f1148,plain,
( ! [X0] :
( ~ drives(X0,masserati)
| lives(X0,house_3)
| ~ person(X0) )
| ~ spl0_136 ),
inference(avatar_component_clause,[],[f1147]) ).
fof(f1149,plain,
( ~ spl0_115
| spl0_136
| spl0_103 ),
inference(avatar_split_clause,[],[f1135,f895,f1147,f981]) ).
fof(f1151,definition,
( spl0_137
<=> ! [X0] :
( ~ person(X0)
| lives(X0,house_2)
| ~ drives(X0,masserati) ) ),
introduced(definition,[new_symbols(definition,[spl0_137])],[avatar_definition]) ).
fof(f1152,plain,
( ! [X0] :
( ~ drives(X0,masserati)
| lives(X0,house_2)
| ~ person(X0) )
| ~ spl0_137 ),
inference(avatar_component_clause,[],[f1151]) ).
fof(f1153,plain,
( ~ spl0_30
| spl0_137
| spl0_104 ),
inference(avatar_split_clause,[],[f1134,f899,f1151,f378]) ).
fof(f1155,definition,
( spl0_138
<=> ! [X0] :
( ~ person(X0)
| lives(X0,house_1)
| ~ drives(X0,masserati) ) ),
introduced(definition,[new_symbols(definition,[spl0_138])],[avatar_definition]) ).
fof(f1156,plain,
( ! [X0] :
( ~ drives(X0,masserati)
| lives(X0,house_1)
| ~ person(X0) )
| ~ spl0_138 ),
inference(avatar_component_clause,[],[f1155]) ).
fof(f1159,plain,
( ~ spl0_104
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f834,f255,f899]) ).
fof(f1160,plain,
( ~ spl0_112
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f880,f255,f960]) ).
fof(f1165,plain,
~ next_to(house_1,house_1),
inference(resolution,[],[f1012,f216]) ).
fof(f1166,plain,
~ next_to(house_2,house_2),
inference(resolution,[],[f1012,f221]) ).
fof(f1168,plain,
~ next_to(house_4,house_4),
inference(resolution,[],[f1012,f231]) ).
fof(f1170,plain,
! [X0,X1] :
( ~ next_to(X0,X1)
| next_to(X1,X0)
| next_to(X1,X0) ),
inference(resolution,[],[f989,f210]) ).
fof(f1193,plain,
! [X0,X1] :
( next_to(X1,X0)
| ~ next_to(X0,X1) ),
inference(duplicate_literal_removal,[],[f1170]) ).
fof(f1236,plain,
( ! [X0] :
( ~ house(X0)
| lives(norwegian,X0)
| ~ house(house_2)
| ~ next_to(X0,house_2) )
| spl0_4 ),
inference(resolution,[],[f204,f253]) ).
fof(f1238,plain,
( ! [X0] :
( ~ house(X0)
| lives(norwegian,X0)
| ~ house(house_4)
| ~ next_to(X0,house_4) )
| spl0_110 ),
inference(resolution,[],[f204,f953]) ).
fof(f1245,definition,
( spl0_140
<=> ! [X0] :
( ~ house(X0)
| ~ next_to(X0,house_4)
| lives(norwegian,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_140])],[avatar_definition]) ).
fof(f1246,plain,
( ! [X0] :
( ~ next_to(X0,house_4)
| ~ house(X0)
| lives(norwegian,X0) )
| ~ spl0_140 ),
inference(avatar_component_clause,[],[f1245]) ).
fof(f1247,plain,
( ~ spl0_26
| spl0_140
| spl0_110 ),
inference(avatar_split_clause,[],[f1238,f951,f1245,f354]) ).
fof(f1253,definition,
( spl0_142
<=> ! [X0] :
( ~ house(X0)
| ~ next_to(X0,house_2)
| lives(norwegian,X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_142])],[avatar_definition]) ).
fof(f1254,plain,
( ! [X0] :
( ~ next_to(X0,house_2)
| ~ house(X0)
| lives(norwegian,X0) )
| ~ spl0_142 ),
inference(avatar_component_clause,[],[f1253]) ).
fof(f1255,plain,
( ~ spl0_30
| spl0_142
| spl0_4 ),
inference(avatar_split_clause,[],[f1236,f251,f1253,f378]) ).
fof(f1262,plain,
( ~ house(house_1)
| lives(norwegian,house_1)
| ~ spl0_142 ),
inference(resolution,[],[f1254,f343]) ).
fof(f1265,definition,
( spl0_144
<=> lives(norwegian,house_3) ),
introduced(definition,[new_symbols(definition,[spl0_144])],[avatar_definition]) ).
fof(f1269,plain,
( spl0_10
| ~ spl0_28
| ~ spl0_142 ),
inference(avatar_split_clause,[],[f1262,f1253,f366,f275]) ).
fof(f1270,plain,
( ~ spl0_4
| ~ spl0_102 ),
inference(avatar_split_clause,[],[f835,f875,f251]) ).
fof(f1275,definition,
( spl0_145
<=> lives(spaniard,house_3) ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f1276,plain,
( ~ lives(spaniard,house_3)
| spl0_145 ),
inference(avatar_component_clause,[],[f1275]) ).
fof(f1279,plain,
( lives(english,house_3)
| ~ house(house_3)
| spl0_145 ),
inference(resolution,[],[f1276,f130]) ).
fof(f1280,plain,
( ~ spl0_115
| spl0_7
| spl0_145 ),
inference(avatar_split_clause,[],[f1279,f1275,f263,f981]) ).
fof(f1290,plain,
( ~ spl0_109
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f910,f251,f947]) ).
fof(f1295,plain,
( ! [X0] :
( ~ person(X0)
| ~ drinks(X0,coffee)
| ~ house(house_1)
| lives(X0,house_1) )
| spl0_98 ),
inference(resolution,[],[f206,f854]) ).
fof(f1296,plain,
( ! [X0] :
( ~ person(X0)
| ~ drinks(X0,coffee)
| ~ house(house_2)
| lives(X0,house_2) )
| spl0_97 ),
inference(resolution,[],[f206,f850]) ).
fof(f1297,plain,
( ! [X0] :
( ~ person(X0)
| ~ drinks(X0,coffee)
| ~ house(house_3)
| lives(X0,house_3) )
| spl0_106 ),
inference(resolution,[],[f206,f925]) ).
fof(f1298,plain,
( ! [X0] :
( ~ person(X0)
| ~ drinks(X0,coffee)
| ~ house(house_4)
| lives(X0,house_4) )
| spl0_105 ),
inference(resolution,[],[f206,f921]) ).
fof(f1299,plain,
( ! [X0] :
( ~ person(X0)
| ~ drinks(X0,coffee)
| ~ house(house_5)
| lives(X0,house_5) )
| spl0_1 ),
inference(resolution,[],[f206,f241]) ).
fof(f1301,definition,
( spl0_147
<=> ! [X0] :
( ~ person(X0)
| lives(X0,house_5)
| ~ drinks(X0,coffee) ) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f1302,plain,
( ! [X0] :
( ~ drinks(X0,coffee)
| lives(X0,house_5)
| ~ person(X0) )
| ~ spl0_147 ),
inference(avatar_component_clause,[],[f1301]) ).
fof(f1303,plain,
( ~ spl0_32
| spl0_147
| spl0_1 ),
inference(avatar_split_clause,[],[f1299,f239,f1301,f390]) ).
fof(f1305,definition,
( spl0_148
<=> ! [X0] :
( ~ person(X0)
| lives(X0,house_4)
| ~ drinks(X0,coffee) ) ),
introduced(definition,[new_symbols(definition,[spl0_148])],[avatar_definition]) ).
fof(f1306,plain,
( ! [X0] :
( ~ drinks(X0,coffee)
| lives(X0,house_4)
| ~ person(X0) )
| ~ spl0_148 ),
inference(avatar_component_clause,[],[f1305]) ).
fof(f1307,plain,
( ~ spl0_26
| spl0_148
| spl0_105 ),
inference(avatar_split_clause,[],[f1298,f919,f1305,f354]) ).
fof(f1309,definition,
( spl0_149
<=> ! [X0] :
( ~ person(X0)
| lives(X0,house_3)
| ~ drinks(X0,coffee) ) ),
introduced(definition,[new_symbols(definition,[spl0_149])],[avatar_definition]) ).
fof(f1310,plain,
( ! [X0] :
( ~ drinks(X0,coffee)
| lives(X0,house_3)
| ~ person(X0) )
| ~ spl0_149 ),
inference(avatar_component_clause,[],[f1309]) ).
fof(f1311,plain,
( ~ spl0_115
| spl0_149
| spl0_106 ),
inference(avatar_split_clause,[],[f1297,f923,f1309,f981]) ).
fof(f1313,definition,
( spl0_150
<=> ! [X0] :
( ~ person(X0)
| lives(X0,house_2)
| ~ drinks(X0,coffee) ) ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f1314,plain,
( ! [X0] :
( ~ drinks(X0,coffee)
| lives(X0,house_2)
| ~ person(X0) )
| ~ spl0_150 ),
inference(avatar_component_clause,[],[f1313]) ).
fof(f1315,plain,
( ~ spl0_30
| spl0_150
| spl0_97 ),
inference(avatar_split_clause,[],[f1296,f848,f1313,f378]) ).
fof(f1317,definition,
( spl0_151
<=> ! [X0] :
( ~ person(X0)
| lives(X0,house_1)
| ~ drinks(X0,coffee) ) ),
introduced(definition,[new_symbols(definition,[spl0_151])],[avatar_definition]) ).
fof(f1318,plain,
( ! [X0] :
( ~ drinks(X0,coffee)
| lives(X0,house_1)
| ~ person(X0) )
| ~ spl0_151 ),
inference(avatar_component_clause,[],[f1317]) ).
fof(f1319,plain,
( ~ spl0_28
| spl0_151
| spl0_98 ),
inference(avatar_split_clause,[],[f1295,f852,f1317,f366]) ).
fof(f1320,plain,
( ~ spl0_1
| ~ spl0_106 ),
inference(avatar_split_clause,[],[f930,f923,f239]) ).
fof(f1321,plain,
( ~ spl0_106
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f868,f852,f923]) ).
fof(f1322,plain,
( ~ spl0_1
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f887,f852,f239]) ).
fof(f1325,plain,
( ! [X0] :
( ~ next_to(house_4,X0)
| lives(norwegian,X0)
| ~ house(X0) )
| ~ spl0_140 ),
inference(resolution,[],[f1246,f1193]) ).
fof(f1333,plain,
( ~ spl0_110
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f905,f251,f951]) ).
fof(f1347,plain,
( ~ spl0_101
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f891,f251,f871]) ).
fof(f1355,plain,
! [X0,X1] :
( next_to(X0,X1)
| ~ is_color(X0,green)
| ~ house(X1)
| ~ is_color(X1,ivory)
| ~ house(X0) ),
inference(resolution,[],[f207,f210]) ).
fof(f1356,plain,
! [X0,X1] :
( next_to(X1,X0)
| ~ is_color(X0,green)
| ~ house(X1)
| ~ is_color(X1,ivory)
| ~ house(X0) ),
inference(resolution,[],[f207,f209]) ).
fof(f1368,plain,
( ~ house(house_3)
| ~ is_color(house_3,green)
| ~ house(house_4)
| ~ is_color(house_4,ivory) ),
inference(resolution,[],[f207,f227]) ).
fof(f1373,plain,
( ~ house(house_4)
| ~ is_color(house_4,green)
| ~ house(house_5)
| ~ is_color(house_5,ivory) ),
inference(resolution,[],[f207,f232]) ).
fof(f1386,plain,
( lives(norwegian,house_3)
| ~ house(house_3)
| ~ spl0_140 ),
inference(resolution,[],[f1325,f349]) ).
fof(f1399,plain,
( ~ is_color(house_1,green)
| ~ house(house_3)
| ~ is_color(house_3,ivory)
| ~ house(house_1)
| spl0_133 ),
inference(resolution,[],[f1355,f1095]) ).
fof(f1400,plain,
( ~ is_color(house_1,green)
| ~ house(house_4)
| ~ is_color(house_4,ivory)
| ~ house(house_1)
| spl0_132 ),
inference(resolution,[],[f1355,f1090]) ).
fof(f1442,plain,
( ~ is_color(house_3,green)
| ~ house(house_1)
| ~ is_color(house_1,ivory)
| ~ house(house_3)
| spl0_133 ),
inference(resolution,[],[f1356,f1095]) ).
fof(f1443,plain,
( ~ is_color(house_4,green)
| ~ house(house_1)
| ~ is_color(house_1,ivory)
| ~ house(house_4)
| spl0_132 ),
inference(resolution,[],[f1356,f1090]) ).
fof(f1444,plain,
( ~ is_color(house_5,green)
| ~ house(house_1)
| ~ is_color(house_1,ivory)
| ~ house(house_5)
| spl0_131 ),
inference(resolution,[],[f1356,f1085]) ).
fof(f1451,plain,
( ~ is_color(house_5,green)
| ~ house(house_3)
| ~ is_color(house_3,ivory)
| ~ house(house_5)
| spl0_128 ),
inference(resolution,[],[f1356,f1070]) ).
fof(f1457,plain,
( ~ is_color(house_1,green)
| ~ house(house_5)
| ~ is_color(house_5,ivory)
| ~ house(house_1)
| spl0_122 ),
inference(resolution,[],[f1356,f1043]) ).
fof(f1459,plain,
( ~ is_color(house_3,green)
| ~ house(house_5)
| ~ is_color(house_5,ivory)
| ~ house(house_3)
| spl0_116 ),
inference(resolution,[],[f1356,f1016]) ).
fof(f1474,plain,
( drinks(english,orange)
| drinks(english,coffee)
| drinks(english,tea)
| drinks(english,milk)
| ~ person(english)
| spl0_36 ),
inference(resolution,[],[f12,f418]) ).
fof(f1475,plain,
( drinks(spaniard,orange)
| drinks(spaniard,coffee)
| drinks(spaniard,tea)
| drinks(spaniard,milk)
| ~ person(spaniard)
| spl0_35 ),
inference(resolution,[],[f12,f414]) ).
fof(f1476,plain,
( drinks(norwegian,orange)
| drinks(norwegian,coffee)
| drinks(norwegian,tea)
| drinks(norwegian,milk)
| ~ person(norwegian)
| spl0_25 ),
inference(resolution,[],[f12,f337]) ).
fof(f1478,plain,
( drinks(japanese,orange)
| drinks(japanese,coffee)
| drinks(japanese,tea)
| drinks(japanese,milk)
| ~ person(japanese)
| spl0_48 ),
inference(resolution,[],[f12,f518]) ).
fof(f1480,definition,
( spl0_155
<=> person(japanese) ),
introduced(definition,[new_symbols(definition,[spl0_155])],[avatar_definition]) ).
fof(f1482,plain,
( ~ person(japanese)
| spl0_155 ),
inference(avatar_component_clause,[],[f1480]) ).
fof(f1483,plain,
( ~ spl0_155
| spl0_50
| spl0_52
| spl0_23
| spl0_53
| spl0_48 ),
inference(avatar_split_clause,[],[f1478,f516,f539,f327,f534,f525,f1480]) ).
fof(f1485,definition,
( spl0_156
<=> person(norwegian) ),
introduced(definition,[new_symbols(definition,[spl0_156])],[avatar_definition]) ).
fof(f1487,plain,
( ~ person(norwegian)
| spl0_156 ),
inference(avatar_component_clause,[],[f1485]) ).
fof(f1488,plain,
( ~ spl0_156
| spl0_43
| spl0_45
| spl0_47
| spl0_41
| spl0_25 ),
inference(avatar_split_clause,[],[f1476,f335,f444,f501,f492,f468,f1485]) ).
fof(f1490,definition,
( spl0_157
<=> person(spaniard) ),
introduced(definition,[new_symbols(definition,[spl0_157])],[avatar_definition]) ).
fof(f1492,plain,
( ~ person(spaniard)
| spl0_157 ),
inference(avatar_component_clause,[],[f1490]) ).
fof(f1493,plain,
( ~ spl0_157
| spl0_44
| spl0_37
| spl0_39
| spl0_21
| spl0_35 ),
inference(avatar_split_clause,[],[f1475,f412,f319,f430,f421,f472,f1490]) ).
fof(f1495,definition,
( spl0_158
<=> person(english) ),
introduced(definition,[new_symbols(definition,[spl0_158])],[avatar_definition]) ).
fof(f1497,plain,
( ~ person(english)
| spl0_158 ),
inference(avatar_component_clause,[],[f1495]) ).
fof(f1498,plain,
( ~ spl0_158
| spl0_22
| spl0_38
| spl0_40
| spl0_42
| spl0_36 ),
inference(avatar_split_clause,[],[f1474,f416,f448,f434,f425,f323,f1495]) ).
fof(f1499,plain,
( $false
| spl0_156 ),
inference(resolution,[],[f1487,f58]) ).
fof(f1500,plain,
spl0_156,
inference(avatar_contradiction_clause,[],[f1499]) ).
fof(f1501,plain,
( $false
| spl0_155 ),
inference(resolution,[],[f1482,f60]) ).
fof(f1502,plain,
spl0_155,
inference(avatar_contradiction_clause,[],[f1501]) ).
fof(f1506,plain,
( lives(japanese,house_4)
| ~ person(japanese)
| ~ spl0_23
| ~ spl0_148 ),
inference(resolution,[],[f328,f1306]) ).
fof(f1509,definition,
( spl0_159
<=> lives(japanese,house_4) ),
introduced(definition,[new_symbols(definition,[spl0_159])],[avatar_definition]) ).
fof(f1510,plain,
( ~ lives(japanese,house_4)
| spl0_159 ),
inference(avatar_component_clause,[],[f1509]) ).
fof(f1514,definition,
( spl0_160
<=> lives(japanese,house_3) ),
introduced(definition,[new_symbols(definition,[spl0_160])],[avatar_definition]) ).
fof(f1515,plain,
( ~ lives(japanese,house_3)
| spl0_160 ),
inference(avatar_component_clause,[],[f1514]) ).
fof(f1519,definition,
( spl0_161
<=> lives(japanese,house_2) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f1520,plain,
( ~ lives(japanese,house_2)
| spl0_161 ),
inference(avatar_component_clause,[],[f1519]) ).
fof(f1524,definition,
( spl0_162
<=> lives(japanese,house_1) ),
introduced(definition,[new_symbols(definition,[spl0_162])],[avatar_definition]) ).
fof(f1525,plain,
( ~ lives(japanese,house_1)
| spl0_162 ),
inference(avatar_component_clause,[],[f1524]) ).
fof(f1528,plain,
( ~ spl0_48
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f509,f335,f516]) ).
fof(f1530,plain,
( lives(ukranian,house_4)
| ~ house(house_4)
| spl0_159 ),
inference(resolution,[],[f1510,f139]) ).
fof(f1535,definition,
( spl0_163
<=> lives(ukranian,house_4) ),
introduced(definition,[new_symbols(definition,[spl0_163])],[avatar_definition]) ).
fof(f1536,plain,
( ~ lives(ukranian,house_4)
| spl0_163 ),
inference(avatar_component_clause,[],[f1535]) ).
fof(f1538,plain,
( ~ spl0_26
| spl0_163
| spl0_159 ),
inference(avatar_split_clause,[],[f1530,f1509,f1535,f354]) ).
fof(f1539,plain,
( drives(english,masserati)
| drives(english,saab)
| drives(english,porsche)
| drives(english,honda)
| ~ person(english)
| spl0_56 ),
inference(resolution,[],[f23,f559]) ).
fof(f1540,plain,
( drives(spaniard,masserati)
| drives(spaniard,saab)
| drives(spaniard,porsche)
| drives(spaniard,honda)
| ~ person(spaniard)
| spl0_55 ),
inference(resolution,[],[f23,f555]) ).
fof(f1541,plain,
( drives(norwegian,masserati)
| drives(norwegian,saab)
| drives(norwegian,porsche)
| drives(norwegian,honda)
| ~ person(norwegian)
| spl0_66 ),
inference(resolution,[],[f23,f639]) ).
fof(f1542,plain,
( drives(ukranian,masserati)
| drives(ukranian,saab)
| drives(ukranian,porsche)
| drives(ukranian,honda)
| ~ person(ukranian)
| spl0_65 ),
inference(resolution,[],[f23,f635]) ).
fof(f1544,definition,
( spl0_164
<=> person(ukranian) ),
introduced(definition,[new_symbols(definition,[spl0_164])],[avatar_definition]) ).
fof(f1546,plain,
( ~ person(ukranian)
| spl0_164 ),
inference(avatar_component_clause,[],[f1544]) ).
fof(f1547,plain,
( ~ spl0_164
| spl0_70
| spl0_72
| spl0_14
| spl0_74
| spl0_65 ),
inference(avatar_split_clause,[],[f1542,f633,f683,f291,f674,f665,f1544]) ).
fof(f1548,plain,
( ~ spl0_156
| spl0_61
| spl0_63
| spl0_68
| spl0_15
| spl0_66 ),
inference(avatar_split_clause,[],[f1541,f637,f295,f651,f609,f585,f1485]) ).
fof(f1553,plain,
( lives(ukranian,house_3)
| ~ house(house_3)
| spl0_160 ),
inference(resolution,[],[f1515,f139]) ).
fof(f1555,plain,
( lives(spaniard,house_3)
| ~ house(house_3)
| spl0_160 ),
inference(resolution,[],[f1515,f136]) ).
fof(f1557,plain,
( ~ spl0_115
| spl0_145
| spl0_160 ),
inference(avatar_split_clause,[],[f1555,f1514,f1275,f981]) ).
fof(f1559,definition,
( spl0_165
<=> lives(ukranian,house_3) ),
introduced(definition,[new_symbols(definition,[spl0_165])],[avatar_definition]) ).
fof(f1560,plain,
( ~ lives(ukranian,house_3)
| spl0_165 ),
inference(avatar_component_clause,[],[f1559]) ).
fof(f1562,plain,
( ~ spl0_115
| spl0_165
| spl0_160 ),
inference(avatar_split_clause,[],[f1553,f1514,f1559,f981]) ).
fof(f1565,plain,
( lives(spaniard,house_2)
| ~ house(house_2)
| spl0_161 ),
inference(resolution,[],[f1520,f136]) ).
fof(f1568,definition,
( spl0_166
<=> lives(spaniard,house_2) ),
introduced(definition,[new_symbols(definition,[spl0_166])],[avatar_definition]) ).
fof(f1571,plain,
( ~ spl0_30
| spl0_166
| spl0_161 ),
inference(avatar_split_clause,[],[f1565,f1519,f1568,f378]) ).
fof(f1573,plain,
( lives(norwegian,house_1)
| ~ house(house_1)
| spl0_162 ),
inference(resolution,[],[f1525,f138]) ).
fof(f1576,plain,
( ~ spl0_28
| spl0_10
| spl0_162 ),
inference(avatar_split_clause,[],[f1573,f1524,f275,f366]) ).
fof(f1578,definition,
( spl0_167
<=> lives(ukranian,house_1) ),
introduced(definition,[new_symbols(definition,[spl0_167])],[avatar_definition]) ).
fof(f1579,plain,
( ~ lives(ukranian,house_1)
| spl0_167 ),
inference(avatar_component_clause,[],[f1578]) ).
fof(f1586,plain,
( lives(spaniard,house_3)
| ~ house(house_3)
| spl0_165 ),
inference(resolution,[],[f1560,f135]) ).
fof(f1587,plain,
( lives(english,house_3)
| ~ house(house_3)
| spl0_165 ),
inference(resolution,[],[f1560,f132]) ).
fof(f1588,plain,
( ~ spl0_115
| spl0_145
| spl0_165 ),
inference(avatar_split_clause,[],[f1586,f1559,f1275,f981]) ).
fof(f1590,plain,
( lives(norwegian,house_1)
| ~ house(house_1)
| spl0_167 ),
inference(resolution,[],[f1579,f137]) ).
fof(f1593,plain,
( ~ spl0_28
| spl0_10
| spl0_167 ),
inference(avatar_split_clause,[],[f1590,f1578,f275,f366]) ).
fof(f1594,plain,
( $false
| spl0_157 ),
inference(resolution,[],[f1492,f57]) ).
fof(f1595,plain,
spl0_157,
inference(avatar_contradiction_clause,[],[f1594]) ).
fof(f1596,plain,
( ~ spl0_157
| spl0_11
| spl0_64
| spl0_57
| spl0_59
| spl0_55 ),
inference(avatar_split_clause,[],[f1540,f553,f571,f562,f613,f279,f1490]) ).
fof(f1597,plain,
( ~ spl0_41
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f462,f319,f444]) ).
fof(f1598,plain,
( ~ spl0_48
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f485,f412,f516]) ).
fof(f1599,plain,
( ~ spl0_24
| ~ spl0_37 ),
inference(avatar_split_clause,[],[f478,f421,f331]) ).
fof(f1600,plain,
( ~ person(spaniard)
| drinks(spaniard,orange)
| ~ spl0_11 ),
inference(resolution,[],[f280,f93]) ).
fof(f1601,plain,
( spl0_21
| ~ spl0_157
| ~ spl0_11 ),
inference(avatar_split_clause,[],[f1600,f279,f1490,f319]) ).
fof(f1602,plain,
( $false
| spl0_158 ),
inference(resolution,[],[f1497,f56]) ).
fof(f1603,plain,
spl0_158,
inference(avatar_contradiction_clause,[],[f1602]) ).
fof(f1604,plain,
( ~ spl0_158
| spl0_62
| spl0_12
| spl0_58
| spl0_60
| spl0_56 ),
inference(avatar_split_clause,[],[f1539,f557,f575,f566,f283,f589,f1495]) ).
fof(f1606,plain,
( ~ spl0_48
| ~ spl0_36 ),
inference(avatar_split_clause,[],[f461,f416,f516]) ).
fof(f1607,plain,
( ~ spl0_12
| ~ spl0_158
| spl0_17 ),
inference(avatar_split_clause,[],[f351,f303,f1495,f283]) ).
fof(f1608,plain,
( ~ spl0_24
| ~ spl0_38 ),
inference(avatar_split_clause,[],[f454,f425,f331]) ).
fof(f1609,plain,
( $false
| spl0_164 ),
inference(resolution,[],[f1546,f59]) ).
fof(f1610,plain,
spl0_164,
inference(avatar_contradiction_clause,[],[f1609]) ).
fof(f1618,plain,
( ~ person(norwegian)
| ~ lives(norwegian,house_3)
| ~ spl0_43 ),
inference(resolution,[],[f469,f208]) ).
fof(f1619,plain,
( ~ spl0_144
| ~ spl0_156
| ~ spl0_43 ),
inference(avatar_split_clause,[],[f1618,f468,f1485,f1265]) ).
fof(f1621,plain,
( ~ person(english)
| ~ lives(english,house_3)
| ~ spl0_22 ),
inference(resolution,[],[f324,f208]) ).
fof(f1622,plain,
( ~ spl0_7
| ~ spl0_158
| ~ spl0_22 ),
inference(avatar_split_clause,[],[f1621,f323,f1495,f263]) ).
fof(f1623,plain,
( ~ spl0_115
| spl0_7
| spl0_165 ),
inference(avatar_split_clause,[],[f1587,f1559,f263,f981]) ).
fof(f1624,plain,
( ~ spl0_21
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f406,f448,f319]) ).
fof(f1625,plain,
( ~ spl0_53
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f481,f319,f539]) ).
fof(f1628,plain,
( lives(english,house_3)
| ~ person(english)
| ~ spl0_40
| ~ spl0_149 ),
inference(resolution,[],[f435,f1310]) ).
fof(f1630,plain,
( lives(english,house_5)
| ~ person(english)
| ~ spl0_40
| ~ spl0_147 ),
inference(resolution,[],[f435,f1302]) ).
fof(f1632,plain,
( ~ person(japanese)
| ~ lives(japanese,house_3)
| ~ spl0_50 ),
inference(resolution,[],[f526,f208]) ).
fof(f1633,plain,
( ~ spl0_160
| ~ spl0_155
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f1632,f525,f1480,f1514]) ).
fof(f1635,plain,
( ~ spl0_13
| ~ spl0_55 ),
inference(avatar_split_clause,[],[f626,f553,f287]) ).
fof(f1636,plain,
( ~ spl0_50
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f484,f472,f525]) ).
fof(f1641,plain,
( lives(english,house_3)
| ~ house(house_3)
| spl0_160 ),
inference(resolution,[],[f1515,f133]) ).
fof(f1644,plain,
( owns(english,dog)
| owns(english,snails)
| owns(english,horse)
| owns(english,fox)
| ~ person(english)
| spl0_76 ),
inference(resolution,[],[f34,f699]) ).
fof(f1646,plain,
( owns(norwegian,dog)
| owns(norwegian,snails)
| owns(norwegian,horse)
| owns(norwegian,fox)
| ~ person(norwegian)
| spl0_88 ),
inference(resolution,[],[f34,f792]) ).
fof(f1647,plain,
( owns(ukranian,dog)
| owns(ukranian,snails)
| owns(ukranian,horse)
| owns(ukranian,fox)
| ~ person(ukranian)
| spl0_87 ),
inference(resolution,[],[f34,f788]) ).
fof(f1648,plain,
( owns(japanese,dog)
| owns(japanese,snails)
| owns(japanese,horse)
| owns(japanese,fox)
| ~ person(japanese)
| spl0_18 ),
inference(resolution,[],[f34,f309]) ).
fof(f1649,plain,
( ~ spl0_155
| spl0_91
| spl0_89
| spl0_93
| spl0_86
| spl0_18 ),
inference(avatar_split_clause,[],[f1648,f307,f776,f823,f800,f814,f1480]) ).
fof(f1650,plain,
( ~ spl0_164
| spl0_92
| spl0_19
| spl0_94
| spl0_85
| spl0_87 ),
inference(avatar_split_clause,[],[f1647,f786,f766,f827,f311,f818,f1544]) ).
fof(f1651,plain,
( ~ spl0_156
| spl0_20
| spl0_90
| spl0_82
| spl0_84
| spl0_88 ),
inference(avatar_split_clause,[],[f1646,f790,f754,f745,f804,f315,f1485]) ).
fof(f1652,plain,
( is_color(house_1,red)
| is_color(house_1,yellow)
| is_color(house_1,blue)
| is_color(house_1,green)
| ~ house(house_1)
| spl0_96 ),
inference(resolution,[],[f45,f845]) ).
fof(f1654,plain,
( is_color(house_3,red)
| is_color(house_3,yellow)
| is_color(house_3,blue)
| is_color(house_3,green)
| ~ house(house_3)
| spl0_108 ),
inference(resolution,[],[f45,f939]) ).
fof(f1655,plain,
( is_color(house_4,red)
| is_color(house_4,yellow)
| is_color(house_4,blue)
| is_color(house_4,green)
| ~ house(house_4)
| spl0_2 ),
inference(resolution,[],[f45,f245]) ).
fof(f1656,plain,
( is_color(house_5,red)
| is_color(house_5,yellow)
| is_color(house_5,blue)
| is_color(house_5,green)
| ~ house(house_5)
| spl0_107 ),
inference(resolution,[],[f45,f935]) ).
fof(f1657,plain,
( ~ spl0_32
| spl0_1
| spl0_109
| spl0_111
| spl0_113
| spl0_107 ),
inference(avatar_split_clause,[],[f1656,f933,f965,f956,f947,f239,f390]) ).
fof(f1658,plain,
( ~ spl0_26
| spl0_105
| spl0_110
| spl0_112
| spl0_114
| spl0_2 ),
inference(avatar_split_clause,[],[f1655,f243,f969,f960,f951,f919,f354]) ).
fof(f1673,plain,
( ~ lives(english,house_1)
| ~ lives(english,house_2)
| ~ lives(english,house_3)
| ~ lives(english,house_4)
| ~ person(english)
| ~ spl0_33 ),
inference(resolution,[],[f129,f396]) ).
fof(f1679,plain,
( ~ lives(ukranian,house_1)
| ~ lives(ukranian,house_2)
| ~ lives(ukranian,house_3)
| ~ lives(ukranian,house_4)
| ~ person(ukranian)
| lives(spaniard,house_5)
| ~ house(house_5) ),
inference(resolution,[],[f129,f135]) ).
fof(f1681,plain,
( ~ lives(japanese,house_1)
| ~ lives(japanese,house_2)
| ~ lives(japanese,house_3)
| ~ lives(japanese,house_4)
| ~ person(japanese)
| ~ spl0_8 ),
inference(resolution,[],[f129,f269]) ).
fof(f1682,plain,
( ~ lives(japanese,house_1)
| ~ lives(japanese,house_2)
| ~ lives(japanese,house_3)
| ~ lives(japanese,house_4)
| ~ person(japanese)
| lives(ukranian,house_5)
| ~ house(house_5) ),
inference(resolution,[],[f129,f139]) ).
fof(f1684,plain,
( ~ lives(japanese,house_1)
| ~ lives(japanese,house_2)
| ~ lives(japanese,house_3)
| ~ lives(japanese,house_4)
| ~ person(japanese)
| lives(spaniard,house_5)
| ~ house(house_5) ),
inference(resolution,[],[f129,f136]) ).
fof(f1686,plain,
( ~ spl0_158
| ~ spl0_27
| ~ spl0_7
| ~ spl0_31
| ~ spl0_29
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f1673,f394,f370,f382,f263,f358,f1495]) ).
fof(f1688,plain,
( ~ spl0_158
| spl0_7
| ~ spl0_40
| ~ spl0_149 ),
inference(avatar_split_clause,[],[f1628,f1309,f434,f263,f1495]) ).
fof(f1689,plain,
( ~ spl0_115
| spl0_7
| spl0_160 ),
inference(avatar_split_clause,[],[f1641,f1514,f263,f981]) ).
fof(f1690,plain,
( ~ spl0_113
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f927,f247,f965]) ).
fof(f1692,plain,
( ~ spl0_158
| spl0_33
| ~ spl0_40
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f1630,f1301,f434,f394,f1495]) ).
fof(f1693,plain,
( ~ spl0_114
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f913,f247,f969]) ).
fof(f1697,plain,
( ~ spl0_115
| spl0_106
| spl0_101
| spl0_103
| spl0_3
| spl0_108 ),
inference(avatar_split_clause,[],[f1654,f937,f247,f895,f871,f923,f981]) ).
fof(f1698,plain,
( ~ spl0_103
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f866,f255,f895]) ).
fof(f1699,plain,
( ~ spl0_2
| ~ spl0_108 ),
inference(avatar_split_clause,[],[f917,f937,f243]) ).
fof(f1702,plain,
( ~ spl0_32
| ~ spl0_108
| ~ spl0_115
| ~ spl0_1
| spl0_128 ),
inference(avatar_split_clause,[],[f1451,f1068,f239,f981,f937,f390]) ).
fof(f1703,plain,
( ~ spl0_3
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f889,f857,f247]) ).
fof(f1708,definition,
( spl0_169
<=> lives(spaniard,house_5) ),
introduced(definition,[new_symbols(definition,[spl0_169])],[avatar_definition]) ).
fof(f1710,plain,
( lives(spaniard,house_5)
| ~ spl0_169 ),
inference(avatar_component_clause,[],[f1708]) ).
fof(f1711,plain,
( ~ spl0_32
| spl0_169
| ~ spl0_164
| ~ spl0_163
| ~ spl0_165
| ~ spl0_9
| ~ spl0_167 ),
inference(avatar_split_clause,[],[f1679,f1578,f271,f1559,f1535,f1544,f1708,f390]) ).
fof(f1712,plain,
( ~ spl0_111
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f885,f255,f956]) ).
fof(f1713,plain,
( ~ spl0_32
| spl0_169
| ~ spl0_155
| ~ spl0_159
| ~ spl0_160
| ~ spl0_161
| ~ spl0_162 ),
inference(avatar_split_clause,[],[f1684,f1524,f1519,f1514,f1509,f1480,f1708,f390]) ).
fof(f1715,definition,
( spl0_170
<=> lives(ukranian,house_5) ),
introduced(definition,[new_symbols(definition,[spl0_170])],[avatar_definition]) ).
fof(f1716,plain,
( ~ lives(ukranian,house_5)
| spl0_170 ),
inference(avatar_component_clause,[],[f1715]) ).
fof(f1717,plain,
( lives(ukranian,house_5)
| ~ spl0_170 ),
inference(avatar_component_clause,[],[f1715]) ).
fof(f1718,plain,
( ~ spl0_32
| spl0_170
| ~ spl0_155
| ~ spl0_159
| ~ spl0_160
| ~ spl0_161
| ~ spl0_162 ),
inference(avatar_split_clause,[],[f1682,f1524,f1519,f1514,f1509,f1480,f1715,f390]) ).
fof(f1719,plain,
( ~ spl0_155
| ~ spl0_159
| ~ spl0_160
| ~ spl0_161
| ~ spl0_162
| ~ spl0_8 ),
inference(avatar_split_clause,[],[f1681,f267,f1524,f1519,f1514,f1509,f1480]) ).
fof(f1720,plain,
( ~ spl0_64
| ~ spl0_157
| spl0_83 ),
inference(avatar_split_clause,[],[f759,f749,f1490,f613]) ).
fof(f1721,plain,
( ~ spl0_64
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f549,f283,f613]) ).
fof(f1722,plain,
( ~ spl0_25
| ~ spl0_35 ),
inference(avatar_split_clause,[],[f466,f412,f335]) ).
fof(f1723,plain,
( ~ spl0_28
| spl0_98
| spl0_102
| spl0_5
| spl0_100
| spl0_96 ),
inference(avatar_split_clause,[],[f1652,f843,f861,f255,f875,f852,f366]) ).
fof(f1724,plain,
( ~ spl0_114
| ~ spl0_100 ),
inference(avatar_split_clause,[],[f879,f861,f969]) ).
fof(f1725,plain,
( ~ spl0_83
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f688,f303,f749]) ).
fof(f1726,plain,
( ~ spl0_13
| ~ spl0_56 ),
inference(avatar_split_clause,[],[f602,f557,f287]) ).
fof(f1727,plain,
( ~ spl0_108
| ~ spl0_96 ),
inference(avatar_split_clause,[],[f869,f843,f937]) ).
fof(f1730,plain,
( ~ spl0_26
| ~ spl0_96
| ~ spl0_28
| ~ spl0_105
| spl0_132 ),
inference(avatar_split_clause,[],[f1443,f1088,f919,f366,f843,f354]) ).
fof(f1731,plain,
( ~ spl0_158
| spl0_78
| spl0_80
| spl0_17
| spl0_81
| spl0_76 ),
inference(avatar_split_clause,[],[f1644,f697,f720,f303,f715,f706,f1495]) ).
fof(f1734,plain,
( ~ spl0_28
| ~ spl0_108
| ~ spl0_115
| ~ spl0_98
| spl0_133 ),
inference(avatar_split_clause,[],[f1399,f1093,f852,f981,f937,f366]) ).
fof(f1735,plain,
( ~ spl0_105
| ~ spl0_98 ),
inference(avatar_split_clause,[],[f882,f852,f919]) ).
fof(f1736,plain,
( ~ spl0_20
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f727,f706,f315]) ).
fof(f1737,plain,
( ~ spl0_1
| ~ spl0_97 ),
inference(avatar_split_clause,[],[f911,f848,f239]) ).
fof(f1741,plain,
( ~ spl0_18
| ~ spl0_88 ),
inference(avatar_split_clause,[],[f798,f790,f307]) ).
fof(f1742,plain,
( ~ spl0_2
| ~ spl0_96 ),
inference(avatar_split_clause,[],[f883,f843,f243]) ).
fof(f1745,plain,
( ~ spl0_32
| ~ spl0_96
| ~ spl0_28
| ~ spl0_1
| spl0_131 ),
inference(avatar_split_clause,[],[f1444,f1083,f239,f366,f843,f390]) ).
fof(f1748,plain,
( ~ spl0_3
| ~ spl0_100 ),
inference(avatar_split_clause,[],[f865,f861,f247]) ).
fof(f1751,plain,
( ~ spl0_107
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f945,f243,f933]) ).
fof(f1752,plain,
( ~ spl0_28
| ~ spl0_107
| ~ spl0_32
| ~ spl0_98
| spl0_122 ),
inference(avatar_split_clause,[],[f1457,f1041,f852,f390,f933,f366]) ).
fof(f1755,plain,
( ~ spl0_28
| ~ spl0_2
| ~ spl0_26
| ~ spl0_98
| spl0_132 ),
inference(avatar_split_clause,[],[f1400,f1088,f852,f354,f243,f366]) ).
fof(f1757,plain,
( ~ spl0_53
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f457,f448,f539]) ).
fof(f1758,plain,
( ~ spl0_155
| spl0_159
| ~ spl0_23
| ~ spl0_148 ),
inference(avatar_split_clause,[],[f1506,f1305,f327,f1509,f1480]) ).
fof(f1759,plain,
( ~ spl0_112
| ~ spl0_103 ),
inference(avatar_split_clause,[],[f914,f895,f960]) ).
fof(f1763,plain,
( ~ spl0_107
| ~ spl0_96 ),
inference(avatar_split_clause,[],[f888,f843,f933]) ).
fof(f1764,plain,
( ~ spl0_18
| ~ spl0_87 ),
inference(avatar_split_clause,[],[f812,f786,f307]) ).
fof(f1765,plain,
( ~ spl0_114
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f903,f857,f969]) ).
fof(f1766,plain,
( ~ spl0_111
| ~ spl0_103 ),
inference(avatar_split_clause,[],[f928,f895,f956]) ).
fof(f1767,plain,
( ~ spl0_91
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f737,f706,f814]) ).
fof(f1770,plain,
( ~ spl0_115
| ~ spl0_96
| ~ spl0_28
| ~ spl0_106
| spl0_133 ),
inference(avatar_split_clause,[],[f1442,f1093,f923,f366,f843,f981]) ).
fof(f1772,plain,
( ~ spl0_93
| ~ spl0_83 ),
inference(avatar_split_clause,[],[f771,f749,f823]) ).
fof(f1774,plain,
( ~ spl0_1
| ~ spl0_105 ),
inference(avatar_split_clause,[],[f944,f919,f239]) ).
fof(f1775,plain,
( ~ spl0_14
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f618,f562,f291]) ).
fof(f1777,plain,
( ~ spl0_13
| ~ spl0_65 ),
inference(avatar_split_clause,[],[f659,f633,f287]) ).
fof(f1779,plain,
( ~ spl0_72
| ~ spl0_164
| spl0_94 ),
inference(avatar_split_clause,[],[f832,f827,f1544,f674]) ).
fof(f1781,plain,
( ~ spl0_63
| ~ spl0_156
| spl0_82 ),
inference(avatar_split_clause,[],[f758,f745,f1485,f609]) ).
fof(f1783,plain,
( ~ spl0_68
| ~ spl0_57 ),
inference(avatar_split_clause,[],[f604,f562,f651]) ).
fof(f1784,plain,
( ~ spl0_13
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f645,f637,f287]) ).
fof(f1789,plain,
( ~ spl0_68
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f580,f566,f651]) ).
fof(f1790,plain,
( ~ spl0_14
| ~ spl0_58 ),
inference(avatar_split_clause,[],[f594,f566,f291]) ).
fof(f1791,plain,
( ~ spl0_93
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f735,f303,f823]) ).
fof(f1801,plain,
( lives(japanese,house_3)
| ~ person(japanese)
| ~ spl0_23
| ~ spl0_149 ),
inference(resolution,[],[f328,f1310]) ).
fof(f1809,plain,
( ! [X0,X1] :
( ~ person(X0)
| ~ owns(X0,fox)
| ~ house(house_1)
| lives(X0,house_1)
| ~ person(X1)
| ~ drives(X1,saab)
| ~ house(house_3)
| lives(X1,house_3) )
| spl0_133 ),
inference(resolution,[],[f203,f1095]) ).
fof(f1810,plain,
( ! [X0,X1] :
( ~ person(X0)
| ~ owns(X0,fox)
| ~ house(house_1)
| lives(X0,house_1)
| ~ person(X1)
| ~ drives(X1,saab)
| ~ house(house_4)
| lives(X1,house_4) )
| spl0_132 ),
inference(resolution,[],[f203,f1090]) ).
fof(f1814,plain,
! [X0,X1] :
( ~ person(X0)
| ~ owns(X0,fox)
| ~ house(house_2)
| lives(X0,house_2)
| ~ person(X1)
| ~ drives(X1,saab)
| ~ house(house_2)
| lives(X1,house_2) ),
inference(resolution,[],[f203,f1166]) ).
fof(f1821,plain,
( ! [X0,X1] :
( ~ person(X0)
| ~ owns(X0,fox)
| ~ house(house_4)
| lives(X0,house_4)
| ~ person(X1)
| ~ drives(X1,saab)
| ~ house(house_2)
| lives(X1,house_2) )
| spl0_120 ),
inference(resolution,[],[f203,f1034]) ).
fof(f1822,plain,
! [X0,X1] :
( ~ person(X0)
| ~ owns(X0,fox)
| ~ house(house_4)
| lives(X0,house_4)
| ~ person(X1)
| ~ drives(X1,saab)
| ~ house(house_4)
| lives(X1,house_4) ),
inference(resolution,[],[f203,f1168]) ).
fof(f1825,plain,
( ! [X0,X1] :
( ~ person(X0)
| ~ owns(X0,fox)
| ~ house(house_5)
| lives(X0,house_5)
| ~ person(X1)
| ~ drives(X1,saab)
| ~ house(house_2)
| lives(X1,house_2) )
| spl0_118 ),
inference(resolution,[],[f203,f1025]) ).
fof(f1826,plain,
( ! [X0,X1] :
( ~ person(X0)
| ~ owns(X0,fox)
| ~ house(house_5)
| lives(X0,house_5)
| ~ person(X1)
| ~ drives(X1,saab)
| ~ house(house_3)
| lives(X1,house_3) )
| spl0_116 ),
inference(resolution,[],[f203,f1016]) ).
fof(f1830,plain,
! [X0,X1] :
( ~ person(X0)
| ~ owns(X0,fox)
| ~ house(house_4)
| lives(X0,house_4)
| ~ person(X1)
| ~ drives(X1,saab)
| lives(X1,house_4) ),
inference(duplicate_literal_removal,[],[f1822]) ).
fof(f1834,plain,
! [X0,X1] :
( ~ person(X0)
| ~ owns(X0,fox)
| ~ house(house_2)
| lives(X0,house_2)
| ~ person(X1)
| ~ drives(X1,saab)
| lives(X1,house_2) ),
inference(duplicate_literal_removal,[],[f1814]) ).
fof(f1845,definition,
( spl0_172
<=> ! [X0] :
( ~ person(X0)
| lives(X0,house_5)
| ~ owns(X0,fox) ) ),
introduced(definition,[new_symbols(definition,[spl0_172])],[avatar_definition]) ).
fof(f1846,plain,
( ! [X0] :
( ~ owns(X0,fox)
| lives(X0,house_5)
| ~ person(X0) )
| ~ spl0_172 ),
inference(avatar_component_clause,[],[f1845]) ).
fof(f1849,definition,
( spl0_173
<=> ! [X1] :
( ~ person(X1)
| lives(X1,house_3)
| ~ drives(X1,saab) ) ),
introduced(definition,[new_symbols(definition,[spl0_173])],[avatar_definition]) ).
fof(f1850,plain,
( ! [X1] :
( ~ drives(X1,saab)
| lives(X1,house_3)
| ~ person(X1) )
| ~ spl0_173 ),
inference(avatar_component_clause,[],[f1849]) ).
fof(f1851,plain,
( ~ spl0_115
| spl0_173
| ~ spl0_32
| spl0_172
| spl0_116 ),
inference(avatar_split_clause,[],[f1826,f1014,f1845,f390,f1849,f981]) ).
fof(f1853,definition,
( spl0_174
<=> ! [X1] :
( ~ person(X1)
| lives(X1,house_2)
| ~ drives(X1,saab) ) ),
introduced(definition,[new_symbols(definition,[spl0_174])],[avatar_definition]) ).
fof(f1854,plain,
( ! [X1] :
( ~ drives(X1,saab)
| lives(X1,house_2)
| ~ person(X1) )
| ~ spl0_174 ),
inference(avatar_component_clause,[],[f1853]) ).
fof(f1855,plain,
( ~ spl0_30
| spl0_174
| ~ spl0_32
| spl0_172
| spl0_118 ),
inference(avatar_split_clause,[],[f1825,f1023,f1845,f390,f1853,f378]) ).
fof(f1865,definition,
( spl0_177
<=> ! [X1] :
( ~ person(X1)
| lives(X1,house_4)
| ~ drives(X1,saab) ) ),
introduced(definition,[new_symbols(definition,[spl0_177])],[avatar_definition]) ).
fof(f1866,plain,
( ! [X1] :
( ~ drives(X1,saab)
| lives(X1,house_4)
| ~ person(X1) )
| ~ spl0_177 ),
inference(avatar_component_clause,[],[f1865]) ).
fof(f1868,definition,
( spl0_178
<=> ! [X0] :
( ~ person(X0)
| lives(X0,house_4)
| ~ owns(X0,fox) ) ),
introduced(definition,[new_symbols(definition,[spl0_178])],[avatar_definition]) ).
fof(f1869,plain,
( ! [X0] :
( ~ owns(X0,fox)
| lives(X0,house_4)
| ~ person(X0) )
| ~ spl0_178 ),
inference(avatar_component_clause,[],[f1868]) ).
fof(f1870,plain,
( spl0_177
| ~ spl0_26
| spl0_178 ),
inference(avatar_split_clause,[],[f1830,f1868,f354,f1865]) ).
fof(f1871,plain,
( ~ spl0_30
| spl0_174
| ~ spl0_26
| spl0_178
| spl0_120 ),
inference(avatar_split_clause,[],[f1821,f1032,f1868,f354,f1853,f378]) ).
fof(f1882,definition,
( spl0_180
<=> ! [X0] :
( ~ person(X0)
| lives(X0,house_2)
| ~ owns(X0,fox) ) ),
introduced(definition,[new_symbols(definition,[spl0_180])],[avatar_definition]) ).
fof(f1883,plain,
( ! [X0] :
( ~ owns(X0,fox)
| lives(X0,house_2)
| ~ person(X0) )
| ~ spl0_180 ),
inference(avatar_component_clause,[],[f1882]) ).
fof(f1884,plain,
( spl0_174
| ~ spl0_30
| spl0_180 ),
inference(avatar_split_clause,[],[f1834,f1882,f378,f1853]) ).
fof(f1888,definition,
( spl0_181
<=> ! [X0] :
( ~ person(X0)
| lives(X0,house_1)
| ~ owns(X0,fox) ) ),
introduced(definition,[new_symbols(definition,[spl0_181])],[avatar_definition]) ).
fof(f1889,plain,
( ! [X0] :
( ~ owns(X0,fox)
| lives(X0,house_1)
| ~ person(X0) )
| ~ spl0_181 ),
inference(avatar_component_clause,[],[f1888]) ).
fof(f1891,plain,
( ~ spl0_26
| spl0_177
| ~ spl0_28
| spl0_181
| spl0_132 ),
inference(avatar_split_clause,[],[f1810,f1088,f1888,f366,f1865,f354]) ).
fof(f1892,plain,
( ~ spl0_115
| spl0_173
| ~ spl0_28
| spl0_181
| spl0_133 ),
inference(avatar_split_clause,[],[f1809,f1093,f1888,f366,f1849,f981]) ).
fof(f1903,plain,
( ~ person(spaniard)
| ~ lives(spaniard,house_3)
| ~ spl0_44 ),
inference(resolution,[],[f473,f208]) ).
fof(f1904,plain,
( ~ spl0_145
| ~ spl0_157
| ~ spl0_44 ),
inference(avatar_split_clause,[],[f1903,f472,f1490,f1275]) ).
fof(f1905,plain,
( ~ spl0_23
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f482,f430,f327]) ).
fof(f1906,plain,
( ~ spl0_25
| ~ spl0_36 ),
inference(avatar_split_clause,[],[f442,f416,f335]) ).
fof(f1915,plain,
! [X0,X1] :
( ~ person(X0)
| ~ drives(X0,masserati)
| ~ house(house_1)
| lives(X0,house_1)
| ~ person(X1)
| ~ owns(X1,horse)
| ~ house(house_1)
| lives(X1,house_1) ),
inference(resolution,[],[f205,f1165]) ).
fof(f1916,plain,
( ! [X0,X1] :
( ~ person(X0)
| ~ drives(X0,masserati)
| ~ house(house_1)
| lives(X0,house_1)
| ~ person(X1)
| ~ owns(X1,horse)
| ~ house(house_3)
| lives(X1,house_3) )
| spl0_133 ),
inference(resolution,[],[f205,f1095]) ).
fof(f1917,plain,
( ! [X0,X1] :
( ~ person(X0)
| ~ drives(X0,masserati)
| ~ house(house_1)
| lives(X0,house_1)
| ~ person(X1)
| ~ owns(X1,horse)
| ~ house(house_4)
| lives(X1,house_4) )
| spl0_132 ),
inference(resolution,[],[f205,f1090]) ).
fof(f1918,plain,
( ! [X0,X1] :
( ~ person(X0)
| ~ drives(X0,masserati)
| ~ house(house_1)
| lives(X0,house_1)
| ~ person(X1)
| ~ owns(X1,horse)
| ~ house(house_5)
| lives(X1,house_5) )
| spl0_131 ),
inference(resolution,[],[f205,f1085]) ).
fof(f1942,plain,
! [X0,X1] :
( ~ person(X0)
| ~ drives(X0,masserati)
| ~ house(house_1)
| lives(X0,house_1)
| ~ person(X1)
| ~ owns(X1,horse)
| lives(X1,house_1) ),
inference(duplicate_literal_removal,[],[f1915]) ).
fof(f1949,definition,
( spl0_183
<=> ! [X2] :
( ~ person(X2)
| lives(X2,house_5)
| ~ owns(X2,horse) ) ),
introduced(definition,[new_symbols(definition,[spl0_183])],[avatar_definition]) ).
fof(f1950,plain,
( ! [X2] :
( ~ owns(X2,horse)
| lives(X2,house_5)
| ~ person(X2) )
| ~ spl0_183 ),
inference(avatar_component_clause,[],[f1949]) ).
fof(f1956,definition,
( spl0_185
<=> ! [X2] :
( ~ person(X2)
| lives(X2,house_4)
| ~ owns(X2,horse) ) ),
introduced(definition,[new_symbols(definition,[spl0_185])],[avatar_definition]) ).
fof(f1957,plain,
( ! [X2] :
( ~ owns(X2,horse)
| lives(X2,house_4)
| ~ person(X2) )
| ~ spl0_185 ),
inference(avatar_component_clause,[],[f1956]) ).
fof(f1960,definition,
( spl0_186
<=> ! [X2] :
( ~ person(X2)
| lives(X2,house_3)
| ~ owns(X2,horse) ) ),
introduced(definition,[new_symbols(definition,[spl0_186])],[avatar_definition]) ).
fof(f1961,plain,
( ! [X2] :
( ~ owns(X2,horse)
| lives(X2,house_3)
| ~ person(X2) )
| ~ spl0_186 ),
inference(avatar_component_clause,[],[f1960]) ).
fof(f1964,definition,
( spl0_187
<=> ! [X2] :
( ~ person(X2)
| lives(X2,house_1)
| ~ owns(X2,horse) ) ),
introduced(definition,[new_symbols(definition,[spl0_187])],[avatar_definition]) ).
fof(f1965,plain,
( ! [X2] :
( ~ owns(X2,horse)
| lives(X2,house_1)
| ~ person(X2) )
| ~ spl0_187 ),
inference(avatar_component_clause,[],[f1964]) ).
fof(f1969,plain,
( lives(spaniard,house_2)
| ~ person(spaniard)
| ~ spl0_59
| ~ spl0_137 ),
inference(resolution,[],[f572,f1152]) ).
fof(f1970,plain,
( lives(spaniard,house_3)
| ~ person(spaniard)
| ~ spl0_59
| ~ spl0_136 ),
inference(resolution,[],[f572,f1148]) ).
fof(f1971,plain,
( lives(spaniard,house_4)
| ~ person(spaniard)
| ~ spl0_59
| ~ spl0_135 ),
inference(resolution,[],[f572,f1144]) ).
fof(f1972,plain,
( lives(spaniard,house_5)
| ~ person(spaniard)
| ~ spl0_59
| ~ spl0_134 ),
inference(resolution,[],[f572,f1140]) ).
fof(f1973,plain,
( ~ person(norwegian)
| drinks(norwegian,orange)
| ~ spl0_61 ),
inference(resolution,[],[f586,f93]) ).
fof(f1974,plain,
( spl0_41
| ~ spl0_156
| ~ spl0_61 ),
inference(avatar_split_clause,[],[f1973,f585,f1485,f444]) ).
fof(f1975,plain,
( ~ spl0_14
| ~ spl0_68 ),
inference(avatar_split_clause,[],[f628,f651,f291]) ).
fof(f1979,plain,
( ~ person(ukranian)
| drinks(ukranian,orange)
| ~ spl0_70 ),
inference(resolution,[],[f666,f93]) ).
fof(f1980,plain,
( spl0_54
| ~ spl0_164
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f1979,f665,f1544,f543]) ).
fof(f1981,plain,
( ~ spl0_54
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f476,f319,f543]) ).
fof(f1983,plain,
( lives(norwegian,house_1)
| ~ person(norwegian)
| ~ spl0_15
| ~ spl0_138 ),
inference(resolution,[],[f296,f1156]) ).
fof(f1988,plain,
( ~ spl0_156
| spl0_10
| ~ spl0_15
| ~ spl0_138 ),
inference(avatar_split_clause,[],[f1983,f1155,f295,f275,f1485]) ).
fof(f2011,plain,
( ~ lives(spaniard,house_1)
| ~ lives(spaniard,house_2)
| ~ lives(spaniard,house_3)
| ~ lives(spaniard,house_4)
| ~ person(spaniard)
| ~ spl0_169 ),
inference(resolution,[],[f1710,f129]) ).
fof(f2012,plain,
( ~ spl0_157
| ~ spl0_6
| ~ spl0_145
| ~ spl0_166
| ~ spl0_34
| ~ spl0_169 ),
inference(avatar_split_clause,[],[f2011,f1708,f402,f1568,f1275,f259,f1490]) ).
fof(f2014,plain,
( ~ lives(ukranian,house_1)
| ~ lives(ukranian,house_2)
| ~ lives(ukranian,house_3)
| ~ lives(ukranian,house_4)
| ~ person(ukranian)
| ~ spl0_170 ),
inference(resolution,[],[f1717,f129]) ).
fof(f2015,plain,
( ~ spl0_164
| ~ spl0_163
| ~ spl0_165
| ~ spl0_9
| ~ spl0_167
| ~ spl0_170 ),
inference(avatar_split_clause,[],[f2014,f1715,f1578,f271,f1559,f1535,f1544]) ).
fof(f2020,plain,
( lives(japanese,house_2)
| ~ person(japanese)
| ~ spl0_23
| ~ spl0_150 ),
inference(resolution,[],[f1314,f328]) ).
fof(f2022,plain,
( lives(ukranian,house_2)
| ~ person(ukranian)
| ~ spl0_14
| ~ spl0_174 ),
inference(resolution,[],[f1854,f292]) ).
fof(f2023,plain,
( ~ spl0_164
| spl0_9
| ~ spl0_14
| ~ spl0_174 ),
inference(avatar_split_clause,[],[f2022,f1853,f291,f271,f1544]) ).
fof(f2025,plain,
( lives(spaniard,house_4)
| ~ house(house_4)
| spl0_163 ),
inference(resolution,[],[f1536,f135]) ).
fof(f2027,plain,
( ~ spl0_26
| spl0_6
| spl0_163 ),
inference(avatar_split_clause,[],[f2025,f1535,f259,f354]) ).
fof(f2029,plain,
( lives(spaniard,house_2)
| ~ house(house_2)
| spl0_9 ),
inference(resolution,[],[f272,f135]) ).
fof(f2033,plain,
( lives(japanese,house_5)
| ~ person(japanese)
| ~ spl0_91
| ~ spl0_172 ),
inference(resolution,[],[f1846,f815]) ).
fof(f2034,plain,
( ~ spl0_155
| spl0_8
| ~ spl0_91
| ~ spl0_172 ),
inference(avatar_split_clause,[],[f2033,f1845,f814,f267,f1480]) ).
fof(f2037,plain,
( lives(ukranian,house_4)
| ~ person(ukranian)
| ~ spl0_14
| ~ spl0_177 ),
inference(resolution,[],[f1866,f292]) ).
fof(f2038,plain,
( lives(ukranian,house_4)
| ~ person(ukranian)
| ~ spl0_92
| ~ spl0_178 ),
inference(resolution,[],[f1869,f819]) ).
fof(f2039,plain,
( lives(ukranian,house_2)
| ~ person(ukranian)
| ~ spl0_92
| ~ spl0_180 ),
inference(resolution,[],[f1883,f819]) ).
fof(f2040,plain,
( ~ spl0_164
| spl0_9
| ~ spl0_92
| ~ spl0_180 ),
inference(avatar_split_clause,[],[f2039,f1882,f818,f271,f1544]) ).
fof(f2042,plain,
( ~ spl0_30
| spl0_166
| spl0_9 ),
inference(avatar_split_clause,[],[f2029,f271,f1568,f378]) ).
fof(f2053,plain,
( lives(japanese,house_5)
| ~ person(japanese)
| ~ spl0_89
| ~ spl0_183 ),
inference(resolution,[],[f1950,f801]) ).
fof(f2054,plain,
( ~ spl0_155
| spl0_8
| ~ spl0_89
| ~ spl0_183 ),
inference(avatar_split_clause,[],[f2053,f1949,f800,f267,f1480]) ).
fof(f2055,plain,
( ~ spl0_82
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f725,f303,f745]) ).
fof(f2057,plain,
( ~ spl0_18
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f738,f697,f307]) ).
fof(f2058,plain,
( ~ spl0_91
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f797,f315,f814]) ).
fof(f2059,plain,
( ~ spl0_94
| ~ spl0_83 ),
inference(avatar_split_clause,[],[f761,f749,f827]) ).
fof(f2060,plain,
( ~ spl0_164
| spl0_163
| ~ spl0_92
| ~ spl0_178 ),
inference(avatar_split_clause,[],[f2038,f1868,f818,f1535,f1544]) ).
fof(f2062,plain,
( ~ spl0_32
| spl0_183
| ~ spl0_28
| spl0_138
| spl0_131 ),
inference(avatar_split_clause,[],[f1918,f1083,f1155,f366,f1949,f390]) ).
fof(f2064,plain,
( ~ spl0_88
| ~ spl0_76 ),
inference(avatar_split_clause,[],[f728,f697,f790]) ).
fof(f2074,plain,
( lives(english,house_3)
| ~ person(english)
| ~ spl0_60
| ~ spl0_136 ),
inference(resolution,[],[f576,f1148]) ).
fof(f2076,plain,
( lives(english,house_5)
| ~ person(english)
| ~ spl0_60
| ~ spl0_134 ),
inference(resolution,[],[f576,f1140]) ).
fof(f2077,plain,
( ~ spl0_158
| spl0_7
| ~ spl0_60
| ~ spl0_136 ),
inference(avatar_split_clause,[],[f2074,f1147,f575,f263,f1495]) ).
fof(f2080,plain,
( ~ spl0_115
| spl0_144
| ~ spl0_140 ),
inference(avatar_split_clause,[],[f1386,f1245,f1265,f981]) ).
fof(f2083,plain,
( ~ spl0_115
| ~ spl0_107
| ~ spl0_32
| ~ spl0_106
| spl0_116 ),
inference(avatar_split_clause,[],[f1459,f1014,f923,f390,f933,f981]) ).
fof(f2085,plain,
( ~ spl0_113
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f908,f857,f965]) ).
fof(f2087,plain,
( ~ spl0_105
| ~ spl0_97 ),
inference(avatar_split_clause,[],[f906,f848,f919]) ).
fof(f2090,plain,
( ~ spl0_158
| spl0_33
| ~ spl0_60
| ~ spl0_134 ),
inference(avatar_split_clause,[],[f2076,f1139,f575,f394,f1495]) ).
fof(f2091,plain,
( ~ spl0_94
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f730,f303,f827]) ).
fof(f2092,plain,
( ~ spl0_72
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f595,f283,f674]) ).
fof(f2097,plain,
( ~ spl0_113
| ~ spl0_100 ),
inference(avatar_split_clause,[],[f884,f861,f965]) ).
fof(f2101,plain,
( ~ spl0_164
| spl0_163
| ~ spl0_14
| ~ spl0_177 ),
inference(avatar_split_clause,[],[f2037,f1865,f291,f1535,f1544]) ).
fof(f2102,plain,
( ~ spl0_157
| spl0_166
| ~ spl0_59
| ~ spl0_137 ),
inference(avatar_split_clause,[],[f1969,f1151,f571,f1568,f1490]) ).
fof(f2103,plain,
( ~ spl0_157
| spl0_6
| ~ spl0_59
| ~ spl0_135 ),
inference(avatar_split_clause,[],[f1971,f1143,f571,f259,f1490]) ).
fof(f2104,plain,
( ~ spl0_157
| spl0_169
| ~ spl0_59
| ~ spl0_134 ),
inference(avatar_split_clause,[],[f1972,f1139,f571,f1708,f1490]) ).
fof(f2105,plain,
( ~ spl0_157
| spl0_145
| ~ spl0_59
| ~ spl0_136 ),
inference(avatar_split_clause,[],[f1970,f1147,f571,f1275,f1490]) ).
fof(f2131,plain,
( lives(norwegian,house_1)
| ~ person(norwegian)
| ~ spl0_47
| ~ spl0_151 ),
inference(resolution,[],[f502,f1318]) ).
fof(f2133,plain,
( ~ spl0_156
| spl0_10
| ~ spl0_47
| ~ spl0_151 ),
inference(avatar_split_clause,[],[f2131,f1317,f501,f275,f1485]) ).
fof(f2152,plain,
( lives(spaniard,house_3)
| ~ person(spaniard)
| ~ spl0_57
| ~ spl0_173 ),
inference(resolution,[],[f563,f1850]) ).
fof(f2153,plain,
( ~ spl0_157
| spl0_145
| ~ spl0_57
| ~ spl0_173 ),
inference(avatar_split_clause,[],[f2152,f1849,f562,f1275,f1490]) ).
fof(f2154,plain,
( ~ person(english)
| drinks(english,orange)
| ~ spl0_62 ),
inference(resolution,[],[f590,f93]) ).
fof(f2156,plain,
( lives(ukranian,house_2)
| ~ person(ukranian)
| ~ spl0_74
| ~ spl0_137 ),
inference(resolution,[],[f684,f1152]) ).
fof(f2158,plain,
( lives(ukranian,house_4)
| ~ person(ukranian)
| ~ spl0_74
| ~ spl0_135 ),
inference(resolution,[],[f684,f1144]) ).
fof(f2159,plain,
( ~ spl0_164
| spl0_9
| ~ spl0_74
| ~ spl0_137 ),
inference(avatar_split_clause,[],[f2156,f1151,f683,f271,f1544]) ).
fof(f2162,plain,
( ~ spl0_2
| ~ spl0_26
| ~ spl0_106
| ~ spl0_115 ),
inference(avatar_split_clause,[],[f1368,f981,f923,f354,f243]) ).
fof(f2163,plain,
( spl0_42
| ~ spl0_158
| ~ spl0_62 ),
inference(avatar_split_clause,[],[f2154,f589,f1495,f448]) ).
fof(f2164,plain,
( ~ spl0_53
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f505,f444,f539]) ).
fof(f2165,plain,
( ~ spl0_54
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f452,f448,f543]) ).
fof(f2176,plain,
( lives(spaniard,house_4)
| ~ house(house_4)
| spl0_159 ),
inference(resolution,[],[f1510,f136]) ).
fof(f2178,plain,
( ~ spl0_26
| spl0_6
| spl0_159 ),
inference(avatar_split_clause,[],[f2176,f1509,f259,f354]) ).
fof(f2184,plain,
( lives(spaniard,house_5)
| ~ person(spaniard)
| ~ spl0_39
| ~ spl0_147 ),
inference(resolution,[],[f431,f1302]) ).
fof(f2187,plain,
( ~ spl0_157
| spl0_169
| ~ spl0_39
| ~ spl0_147 ),
inference(avatar_split_clause,[],[f2184,f1301,f430,f1708,f1490]) ).
fof(f2206,plain,
( lives(english,house_5)
| ~ house(house_5)
| spl0_170 ),
inference(resolution,[],[f1716,f132]) ).
fof(f2207,plain,
( ~ spl0_32
| spl0_33
| spl0_170 ),
inference(avatar_split_clause,[],[f2206,f1715,f394,f390]) ).
fof(f2210,plain,
( lives(spaniard,house_4)
| ~ person(spaniard)
| ~ spl0_39
| ~ spl0_148 ),
inference(resolution,[],[f1306,f431]) ).
fof(f2211,plain,
( ~ spl0_157
| spl0_6
| ~ spl0_39
| ~ spl0_148 ),
inference(avatar_split_clause,[],[f2210,f1305,f430,f259,f1490]) ).
fof(f2213,plain,
( lives(spaniard,house_2)
| ~ person(spaniard)
| ~ spl0_39
| ~ spl0_150 ),
inference(resolution,[],[f1314,f431]) ).
fof(f2216,plain,
( lives(english,house_5)
| ~ person(english)
| ~ spl0_78
| ~ spl0_172 ),
inference(resolution,[],[f1846,f707]) ).
fof(f2217,plain,
( ~ spl0_158
| spl0_33
| ~ spl0_78
| ~ spl0_172 ),
inference(avatar_split_clause,[],[f2216,f1845,f706,f394,f1495]) ).
fof(f2221,plain,
( lives(spaniard,house_4)
| ~ person(spaniard)
| ~ spl0_57
| ~ spl0_177 ),
inference(resolution,[],[f1866,f563]) ).
fof(f2222,plain,
( ~ spl0_157
| spl0_6
| ~ spl0_57
| ~ spl0_177 ),
inference(avatar_split_clause,[],[f2221,f1865,f562,f259,f1490]) ).
fof(f2225,plain,
( lives(japanese,house_4)
| ~ person(japanese)
| ~ spl0_89
| ~ spl0_185 ),
inference(resolution,[],[f1957,f801]) ).
fof(f2226,plain,
( lives(japanese,house_3)
| ~ person(japanese)
| ~ spl0_89
| ~ spl0_186 ),
inference(resolution,[],[f1961,f801]) ).
fof(f2227,plain,
( ~ spl0_155
| spl0_160
| ~ spl0_89
| ~ spl0_186 ),
inference(avatar_split_clause,[],[f2226,f1960,f800,f1514,f1480]) ).
fof(f2228,plain,
( ~ spl0_115
| spl0_186
| ~ spl0_28
| spl0_138
| spl0_133 ),
inference(avatar_split_clause,[],[f1916,f1093,f1155,f366,f1960,f981]) ).
fof(f2233,plain,
( lives(norwegian,house_1)
| ~ person(norwegian)
| ~ spl0_90
| ~ spl0_187 ),
inference(resolution,[],[f1965,f805]) ).
fof(f2234,plain,
( ~ spl0_156
| spl0_10
| ~ spl0_90
| ~ spl0_187 ),
inference(avatar_split_clause,[],[f2233,f1964,f804,f275,f1485]) ).
fof(f2235,plain,
( spl0_187
| ~ spl0_28
| spl0_138 ),
inference(avatar_split_clause,[],[f1942,f1155,f366,f1964]) ).
fof(f2236,plain,
( ~ spl0_94
| ~ spl0_82 ),
inference(avatar_split_clause,[],[f781,f745,f827]) ).
fof(f2238,plain,
( lives(english,house_3)
| ~ person(english)
| ~ spl0_80
| ~ spl0_186 ),
inference(resolution,[],[f716,f1961]) ).
fof(f2240,plain,
( lives(english,house_5)
| ~ person(english)
| ~ spl0_80
| ~ spl0_183 ),
inference(resolution,[],[f716,f1950]) ).
fof(f2241,plain,
( ~ spl0_158
| spl0_33
| ~ spl0_80
| ~ spl0_183 ),
inference(avatar_split_clause,[],[f2240,f1949,f715,f394,f1495]) ).
fof(f2243,plain,
( ~ spl0_155
| spl0_160
| ~ spl0_23
| ~ spl0_149 ),
inference(avatar_split_clause,[],[f1801,f1309,f327,f1514,f1480]) ).
fof(f2244,plain,
( ~ spl0_107
| ~ spl0_32
| ~ spl0_105
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f1373,f354,f919,f390,f933]) ).
fof(f2245,plain,
( ~ spl0_158
| spl0_7
| ~ spl0_80
| ~ spl0_186 ),
inference(avatar_split_clause,[],[f2238,f1960,f715,f263,f1495]) ).
fof(f2247,plain,
( ~ spl0_155
| spl0_159
| ~ spl0_89
| ~ spl0_185 ),
inference(avatar_split_clause,[],[f2225,f1956,f800,f1509,f1480]) ).
fof(f2248,plain,
( ~ spl0_26
| spl0_185
| ~ spl0_28
| spl0_138
| spl0_132 ),
inference(avatar_split_clause,[],[f1917,f1088,f1155,f366,f1956,f354]) ).
fof(f2250,plain,
( ~ spl0_54
| ~ spl0_41 ),
inference(avatar_split_clause,[],[f486,f444,f543]) ).
fof(f2252,plain,
( ~ spl0_155
| spl0_161
| ~ spl0_23
| ~ spl0_150 ),
inference(avatar_split_clause,[],[f2020,f1313,f327,f1519,f1480]) ).
fof(f2255,plain,
( lives(ukranian,house_5)
| ~ house(house_5)
| spl0_8 ),
inference(resolution,[],[f268,f139]) ).
fof(f2265,plain,
( lives(norwegian,house_1)
| ~ person(norwegian)
| ~ spl0_20
| ~ spl0_181 ),
inference(resolution,[],[f316,f1889]) ).
fof(f2268,plain,
( ~ spl0_156
| spl0_10
| ~ spl0_20
| ~ spl0_181 ),
inference(avatar_split_clause,[],[f2265,f1888,f315,f275,f1485]) ).
fof(f2284,plain,
( lives(japanese,house_4)
| ~ person(japanese)
| ~ spl0_91
| ~ spl0_178 ),
inference(resolution,[],[f815,f1869]) ).
fof(f2297,plain,
( lives(ukranian,house_4)
| ~ person(ukranian)
| ~ spl0_19
| ~ spl0_185 ),
inference(resolution,[],[f1957,f312]) ).
fof(f2298,plain,
( ~ spl0_164
| spl0_163
| ~ spl0_19
| ~ spl0_185 ),
inference(avatar_split_clause,[],[f2297,f1956,f311,f1535,f1544]) ).
fof(f2299,plain,
( ~ spl0_157
| spl0_166
| ~ spl0_39
| ~ spl0_150 ),
inference(avatar_split_clause,[],[f2213,f1313,f430,f1568,f1490]) ).
fof(f2301,plain,
( ~ spl0_164
| spl0_163
| ~ spl0_74
| ~ spl0_135 ),
inference(avatar_split_clause,[],[f2158,f1143,f683,f1535,f1544]) ).
fof(f2302,plain,
( ~ spl0_32
| spl0_170
| spl0_8 ),
inference(avatar_split_clause,[],[f2255,f267,f1715,f390]) ).
fof(f2304,plain,
( ~ spl0_155
| spl0_159
| ~ spl0_91
| ~ spl0_178 ),
inference(avatar_split_clause,[],[f2284,f1868,f814,f1509,f1480]) ).
cnf(s1,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_4
| ~ spl0_5
| spl0_6
| spl0_7
| spl0_8
| spl0_9
| spl0_10
| ~ spl0_11
| ~ spl0_12
| ~ spl0_13
| ~ spl0_14
| ~ spl0_15
| ~ spl0_16
| ~ spl0_17
| ~ spl0_18
| ~ spl0_19
| ~ spl0_20
| ~ spl0_21
| ~ spl0_22
| ~ spl0_23
| ~ spl0_24
| ~ spl0_25 ),
inference(sat_conversion,[],[f338]) ).
cnf(s2,plain,
spl0_13,
inference(sat_conversion,[],[f339]) ).
cnf(s3,plain,
spl0_24,
inference(sat_conversion,[],[f340]) ).
cnf(s4,plain,
~ spl0_10,
inference(sat_conversion,[],[f341]) ).
cnf(s5,plain,
spl0_16,
inference(sat_conversion,[],[f342]) ).
cnf(s7,plain,
spl0_26,
inference(sat_conversion,[],[f363]) ).
cnf(s8,plain,
( spl0_10
| ~ spl0_28
| spl0_29 ),
inference(sat_conversion,[],[f373]) ).
cnf(s9,plain,
spl0_28,
inference(sat_conversion,[],[f375]) ).
cnf(s11,plain,
spl0_30,
inference(sat_conversion,[],[f387]) ).
cnf(s12,plain,
( spl0_8
| ~ spl0_32
| spl0_33 ),
inference(sat_conversion,[],[f397]) ).
cnf(s13,plain,
spl0_32,
inference(sat_conversion,[],[f399]) ).
cnf(s14,plain,
( spl0_10
| ~ spl0_28
| spl0_34 ),
inference(sat_conversion,[],[f405]) ).
cnf(s15,plain,
( ~ spl0_35
| ~ spl0_36 ),
inference(sat_conversion,[],[f419]) ).
cnf(s18,plain,
( ~ spl0_41
| ~ spl0_42 ),
inference(sat_conversion,[],[f451]) ).
cnf(s20,plain,
( ~ spl0_24
| ~ spl0_45 ),
inference(sat_conversion,[],[f495]) ).
cnf(s24,plain,
( ~ spl0_24
| ~ spl0_52 ),
inference(sat_conversion,[],[f537]) ).
cnf(s25,plain,
( ~ spl0_53
| ~ spl0_54 ),
inference(sat_conversion,[],[f546]) ).
cnf(s27,plain,
( ~ spl0_57
| ~ spl0_58 ),
inference(sat_conversion,[],[f569]) ).
cnf(s30,plain,
( ~ spl0_63
| ~ spl0_64 ),
inference(sat_conversion,[],[f616]) ).
cnf(s39,plain,
( ~ spl0_16
| ~ spl0_81 ),
inference(sat_conversion,[],[f723]) ).
cnf(s40,plain,
( ~ spl0_82
| ~ spl0_83 ),
inference(sat_conversion,[],[f752]) ).
cnf(s41,plain,
( ~ spl0_16
| ~ spl0_84 ),
inference(sat_conversion,[],[f757]) ).
cnf(s42,plain,
( ~ spl0_16
| ~ spl0_85 ),
inference(sat_conversion,[],[f769]) ).
cnf(s43,plain,
( ~ spl0_16
| ~ spl0_86 ),
inference(sat_conversion,[],[f779]) ).
cnf(s44,plain,
( ~ spl0_87
| ~ spl0_88 ),
inference(sat_conversion,[],[f793]) ).
cnf(s47,plain,
( ~ spl0_93
| ~ spl0_94 ),
inference(sat_conversion,[],[f830]) ).
cnf(s50,plain,
( ~ spl0_99
| ~ spl0_100 ),
inference(sat_conversion,[],[f864]) ).
cnf(s53,plain,
( ~ spl0_105
| ~ spl0_106 ),
inference(sat_conversion,[],[f926]) ).
cnf(s54,plain,
( ~ spl0_107
| ~ spl0_108 ),
inference(sat_conversion,[],[f940]) ).
cnf(s56,plain,
( ~ spl0_111
| ~ spl0_112 ),
inference(sat_conversion,[],[f963]) ).
cnf(s57,plain,
( ~ spl0_113
| ~ spl0_114 ),
inference(sat_conversion,[],[f972]) ).
cnf(s58,plain,
( ~ spl0_32
| spl0_33
| spl0_113 ),
inference(sat_conversion,[],[f978]) ).
cnf(s59,plain,
( ~ spl0_26
| spl0_27
| spl0_114 ),
inference(sat_conversion,[],[f979]) ).
cnf(s60,plain,
( spl0_3
| spl0_7
| ~ spl0_115 ),
inference(sat_conversion,[],[f984]) ).
cnf(s61,plain,
( ~ spl0_30
| spl0_31
| spl0_99 ),
inference(sat_conversion,[],[f985]) ).
cnf(s62,plain,
spl0_115,
inference(sat_conversion,[],[f987]) ).
cnf(s63,plain,
( ~ spl0_116
| ~ spl0_117 ),
inference(sat_conversion,[],[f1021]) ).
cnf(s64,plain,
( ~ spl0_118
| ~ spl0_119 ),
inference(sat_conversion,[],[f1030]) ).
cnf(s65,plain,
( ~ spl0_120
| ~ spl0_121 ),
inference(sat_conversion,[],[f1039]) ).
cnf(s66,plain,
( ~ spl0_122
| ~ spl0_123 ),
inference(sat_conversion,[],[f1048]) ).
cnf(s69,plain,
( ~ spl0_117
| ~ spl0_128 ),
inference(sat_conversion,[],[f1071]) ).
cnf(s72,plain,
( ~ spl0_123
| ~ spl0_131 ),
inference(sat_conversion,[],[f1086]) ).
cnf(s73,plain,
( ~ spl0_125
| ~ spl0_132 ),
inference(sat_conversion,[],[f1091]) ).
cnf(s74,plain,
( ~ spl0_127
| ~ spl0_133 ),
inference(sat_conversion,[],[f1096]) ).
cnf(s75,plain,
spl0_117,
inference(sat_conversion,[],[f1100]) ).
cnf(s78,plain,
spl0_119,
inference(sat_conversion,[],[f1106]) ).
cnf(s81,plain,
spl0_121,
inference(sat_conversion,[],[f1112]) ).
cnf(s84,plain,
spl0_123,
inference(sat_conversion,[],[f1118]) ).
cnf(s87,plain,
spl0_125,
inference(sat_conversion,[],[f1124]) ).
cnf(s90,plain,
spl0_127,
inference(sat_conversion,[],[f1130]) ).
cnf(s93,plain,
( ~ spl0_32
| spl0_111
| spl0_134 ),
inference(sat_conversion,[],[f1141]) ).
cnf(s94,plain,
( ~ spl0_26
| spl0_112
| spl0_135 ),
inference(sat_conversion,[],[f1145]) ).
cnf(s95,plain,
( spl0_103
| ~ spl0_115
| spl0_136 ),
inference(sat_conversion,[],[f1149]) ).
cnf(s96,plain,
( ~ spl0_30
| spl0_104
| spl0_137 ),
inference(sat_conversion,[],[f1153]) ).
cnf(s99,plain,
( ~ spl0_5
| ~ spl0_104 ),
inference(sat_conversion,[],[f1159]) ).
cnf(s100,plain,
( ~ spl0_5
| ~ spl0_112 ),
inference(sat_conversion,[],[f1160]) ).
cnf(s102,plain,
( ~ spl0_26
| spl0_110
| spl0_140 ),
inference(sat_conversion,[],[f1247]) ).
cnf(s104,plain,
( spl0_4
| ~ spl0_30
| spl0_142 ),
inference(sat_conversion,[],[f1255]) ).
cnf(s108,plain,
( spl0_10
| ~ spl0_28
| ~ spl0_142 ),
inference(sat_conversion,[],[f1269]) ).
cnf(s109,plain,
( ~ spl0_4
| ~ spl0_102 ),
inference(sat_conversion,[],[f1270]) ).
cnf(s112,plain,
( spl0_7
| ~ spl0_115
| spl0_145 ),
inference(sat_conversion,[],[f1280]) ).
cnf(s114,plain,
( ~ spl0_4
| ~ spl0_109 ),
inference(sat_conversion,[],[f1290]) ).
cnf(s116,plain,
( spl0_1
| ~ spl0_32
| spl0_147 ),
inference(sat_conversion,[],[f1303]) ).
cnf(s117,plain,
( ~ spl0_26
| spl0_105
| spl0_148 ),
inference(sat_conversion,[],[f1307]) ).
cnf(s118,plain,
( spl0_106
| ~ spl0_115
| spl0_149 ),
inference(sat_conversion,[],[f1311]) ).
cnf(s119,plain,
( ~ spl0_30
| spl0_97
| spl0_150 ),
inference(sat_conversion,[],[f1315]) ).
cnf(s120,plain,
( ~ spl0_28
| spl0_98
| spl0_151 ),
inference(sat_conversion,[],[f1319]) ).
cnf(s121,plain,
( ~ spl0_1
| ~ spl0_106 ),
inference(sat_conversion,[],[f1320]) ).
cnf(s122,plain,
( ~ spl0_98
| ~ spl0_106 ),
inference(sat_conversion,[],[f1321]) ).
cnf(s123,plain,
( ~ spl0_1
| ~ spl0_98 ),
inference(sat_conversion,[],[f1322]) ).
cnf(s125,plain,
( ~ spl0_4
| ~ spl0_110 ),
inference(sat_conversion,[],[f1333]) ).
cnf(s128,plain,
( ~ spl0_4
| ~ spl0_101 ),
inference(sat_conversion,[],[f1347]) ).
cnf(s131,plain,
( spl0_23
| spl0_48
| spl0_50
| spl0_52
| spl0_53
| ~ spl0_155 ),
inference(sat_conversion,[],[f1483]) ).
cnf(s132,plain,
( spl0_25
| spl0_41
| spl0_43
| spl0_45
| spl0_47
| ~ spl0_156 ),
inference(sat_conversion,[],[f1488]) ).
cnf(s133,plain,
( spl0_21
| spl0_35
| spl0_37
| spl0_39
| spl0_44
| ~ spl0_157 ),
inference(sat_conversion,[],[f1493]) ).
cnf(s134,plain,
( spl0_22
| spl0_36
| spl0_38
| spl0_40
| spl0_42
| ~ spl0_158 ),
inference(sat_conversion,[],[f1498]) ).
cnf(s135,plain,
spl0_156,
inference(sat_conversion,[],[f1500]) ).
cnf(s136,plain,
spl0_155,
inference(sat_conversion,[],[f1502]) ).
cnf(s141,plain,
( ~ spl0_25
| ~ spl0_48 ),
inference(sat_conversion,[],[f1528]) ).
cnf(s142,plain,
( ~ spl0_26
| spl0_159
| spl0_163 ),
inference(sat_conversion,[],[f1538]) ).
cnf(s143,plain,
( spl0_14
| spl0_65
| spl0_70
| spl0_72
| spl0_74
| ~ spl0_164 ),
inference(sat_conversion,[],[f1547]) ).
cnf(s144,plain,
( spl0_15
| spl0_61
| spl0_63
| spl0_66
| spl0_68
| ~ spl0_156 ),
inference(sat_conversion,[],[f1548]) ).
cnf(s145,plain,
( ~ spl0_115
| spl0_145
| spl0_160 ),
inference(sat_conversion,[],[f1557]) ).
cnf(s146,plain,
( ~ spl0_115
| spl0_160
| spl0_165 ),
inference(sat_conversion,[],[f1562]) ).
cnf(s147,plain,
( ~ spl0_30
| spl0_161
| spl0_166 ),
inference(sat_conversion,[],[f1571]) ).
cnf(s148,plain,
( spl0_10
| ~ spl0_28
| spl0_162 ),
inference(sat_conversion,[],[f1576]) ).
cnf(s150,plain,
( ~ spl0_115
| spl0_145
| spl0_165 ),
inference(sat_conversion,[],[f1588]) ).
cnf(s151,plain,
( spl0_10
| ~ spl0_28
| spl0_167 ),
inference(sat_conversion,[],[f1593]) ).
cnf(s152,plain,
spl0_157,
inference(sat_conversion,[],[f1595]) ).
cnf(s153,plain,
( spl0_11
| spl0_55
| spl0_57
| spl0_59
| spl0_64
| ~ spl0_157 ),
inference(sat_conversion,[],[f1596]) ).
cnf(s154,plain,
( ~ spl0_21
| ~ spl0_41 ),
inference(sat_conversion,[],[f1597]) ).
cnf(s155,plain,
( ~ spl0_35
| ~ spl0_48 ),
inference(sat_conversion,[],[f1598]) ).
cnf(s156,plain,
( ~ spl0_24
| ~ spl0_37 ),
inference(sat_conversion,[],[f1599]) ).
cnf(s157,plain,
( ~ spl0_11
| spl0_21
| ~ spl0_157 ),
inference(sat_conversion,[],[f1601]) ).
cnf(s158,plain,
spl0_158,
inference(sat_conversion,[],[f1603]) ).
cnf(s159,plain,
( spl0_12
| spl0_56
| spl0_58
| spl0_60
| spl0_62
| ~ spl0_158 ),
inference(sat_conversion,[],[f1604]) ).
cnf(s161,plain,
( ~ spl0_36
| ~ spl0_48 ),
inference(sat_conversion,[],[f1606]) ).
cnf(s162,plain,
( ~ spl0_12
| spl0_17
| ~ spl0_158 ),
inference(sat_conversion,[],[f1607]) ).
cnf(s163,plain,
( ~ spl0_24
| ~ spl0_38 ),
inference(sat_conversion,[],[f1608]) ).
cnf(s164,plain,
spl0_164,
inference(sat_conversion,[],[f1610]) ).
cnf(s165,plain,
( ~ spl0_43
| ~ spl0_144
| ~ spl0_156 ),
inference(sat_conversion,[],[f1619]) ).
cnf(s167,plain,
( ~ spl0_7
| ~ spl0_22
| ~ spl0_158 ),
inference(sat_conversion,[],[f1622]) ).
cnf(s168,plain,
( spl0_7
| ~ spl0_115
| spl0_165 ),
inference(sat_conversion,[],[f1623]) ).
cnf(s169,plain,
( ~ spl0_21
| ~ spl0_42 ),
inference(sat_conversion,[],[f1624]) ).
cnf(s170,plain,
( ~ spl0_21
| ~ spl0_53 ),
inference(sat_conversion,[],[f1625]) ).
cnf(s171,plain,
( ~ spl0_50
| ~ spl0_155
| ~ spl0_160 ),
inference(sat_conversion,[],[f1633]) ).
cnf(s173,plain,
( ~ spl0_13
| ~ spl0_55 ),
inference(sat_conversion,[],[f1635]) ).
cnf(s174,plain,
( ~ spl0_44
| ~ spl0_50 ),
inference(sat_conversion,[],[f1636]) ).
cnf(s175,plain,
( spl0_18
| spl0_86
| spl0_89
| spl0_91
| spl0_93
| ~ spl0_155 ),
inference(sat_conversion,[],[f1649]) ).
cnf(s176,plain,
( spl0_19
| spl0_85
| spl0_87
| spl0_92
| spl0_94
| ~ spl0_164 ),
inference(sat_conversion,[],[f1650]) ).
cnf(s177,plain,
( spl0_20
| spl0_82
| spl0_84
| spl0_88
| spl0_90
| ~ spl0_156 ),
inference(sat_conversion,[],[f1651]) ).
cnf(s178,plain,
( spl0_1
| ~ spl0_32
| spl0_107
| spl0_109
| spl0_111
| spl0_113 ),
inference(sat_conversion,[],[f1657]) ).
cnf(s179,plain,
( spl0_2
| ~ spl0_26
| spl0_105
| spl0_110
| spl0_112
| spl0_114 ),
inference(sat_conversion,[],[f1658]) ).
cnf(s184,plain,
( ~ spl0_7
| ~ spl0_27
| ~ spl0_29
| ~ spl0_31
| ~ spl0_33
| ~ spl0_158 ),
inference(sat_conversion,[],[f1686]) ).
cnf(s186,plain,
( spl0_7
| ~ spl0_40
| ~ spl0_149
| ~ spl0_158 ),
inference(sat_conversion,[],[f1688]) ).
cnf(s187,plain,
( spl0_7
| ~ spl0_115
| spl0_160 ),
inference(sat_conversion,[],[f1689]) ).
cnf(s188,plain,
( ~ spl0_3
| ~ spl0_113 ),
inference(sat_conversion,[],[f1690]) ).
cnf(s190,plain,
( spl0_33
| ~ spl0_40
| ~ spl0_147
| ~ spl0_158 ),
inference(sat_conversion,[],[f1692]) ).
cnf(s191,plain,
( ~ spl0_3
| ~ spl0_114 ),
inference(sat_conversion,[],[f1693]) ).
cnf(s195,plain,
( spl0_3
| spl0_101
| spl0_103
| spl0_106
| spl0_108
| ~ spl0_115 ),
inference(sat_conversion,[],[f1697]) ).
cnf(s196,plain,
( ~ spl0_5
| ~ spl0_103 ),
inference(sat_conversion,[],[f1698]) ).
cnf(s197,plain,
( ~ spl0_2
| ~ spl0_108 ),
inference(sat_conversion,[],[f1699]) ).
cnf(s200,plain,
( ~ spl0_1
| ~ spl0_32
| ~ spl0_108
| ~ spl0_115
| spl0_128 ),
inference(sat_conversion,[],[f1702]) ).
cnf(s201,plain,
( ~ spl0_3
| ~ spl0_99 ),
inference(sat_conversion,[],[f1703]) ).
cnf(s205,plain,
( ~ spl0_9
| ~ spl0_32
| ~ spl0_163
| ~ spl0_164
| ~ spl0_165
| ~ spl0_167
| spl0_169 ),
inference(sat_conversion,[],[f1711]) ).
cnf(s206,plain,
( ~ spl0_5
| ~ spl0_111 ),
inference(sat_conversion,[],[f1712]) ).
cnf(s207,plain,
( ~ spl0_32
| ~ spl0_155
| ~ spl0_159
| ~ spl0_160
| ~ spl0_161
| ~ spl0_162
| spl0_169 ),
inference(sat_conversion,[],[f1713]) ).
cnf(s208,plain,
( ~ spl0_32
| ~ spl0_155
| ~ spl0_159
| ~ spl0_160
| ~ spl0_161
| ~ spl0_162
| spl0_170 ),
inference(sat_conversion,[],[f1718]) ).
cnf(s209,plain,
( ~ spl0_8
| ~ spl0_155
| ~ spl0_159
| ~ spl0_160
| ~ spl0_161
| ~ spl0_162 ),
inference(sat_conversion,[],[f1719]) ).
cnf(s210,plain,
( ~ spl0_64
| spl0_83
| ~ spl0_157 ),
inference(sat_conversion,[],[f1720]) ).
cnf(s211,plain,
( ~ spl0_12
| ~ spl0_64 ),
inference(sat_conversion,[],[f1721]) ).
cnf(s212,plain,
( ~ spl0_25
| ~ spl0_35 ),
inference(sat_conversion,[],[f1722]) ).
cnf(s213,plain,
( spl0_5
| ~ spl0_28
| spl0_96
| spl0_98
| spl0_100
| spl0_102 ),
inference(sat_conversion,[],[f1723]) ).
cnf(s214,plain,
( ~ spl0_100
| ~ spl0_114 ),
inference(sat_conversion,[],[f1724]) ).
cnf(s215,plain,
( ~ spl0_17
| ~ spl0_83 ),
inference(sat_conversion,[],[f1725]) ).
cnf(s216,plain,
( ~ spl0_13
| ~ spl0_56 ),
inference(sat_conversion,[],[f1726]) ).
cnf(s217,plain,
( ~ spl0_96
| ~ spl0_108 ),
inference(sat_conversion,[],[f1727]) ).
cnf(s220,plain,
( ~ spl0_26
| ~ spl0_28
| ~ spl0_96
| ~ spl0_105
| spl0_132 ),
inference(sat_conversion,[],[f1730]) ).
cnf(s221,plain,
( spl0_17
| spl0_76
| spl0_78
| spl0_80
| spl0_81
| ~ spl0_158 ),
inference(sat_conversion,[],[f1731]) ).
cnf(s224,plain,
( ~ spl0_28
| ~ spl0_98
| ~ spl0_108
| ~ spl0_115
| spl0_133 ),
inference(sat_conversion,[],[f1734]) ).
cnf(s225,plain,
( ~ spl0_98
| ~ spl0_105 ),
inference(sat_conversion,[],[f1735]) ).
cnf(s226,plain,
( ~ spl0_20
| ~ spl0_78 ),
inference(sat_conversion,[],[f1736]) ).
cnf(s227,plain,
( ~ spl0_1
| ~ spl0_97 ),
inference(sat_conversion,[],[f1737]) ).
cnf(s231,plain,
( ~ spl0_18
| ~ spl0_88 ),
inference(sat_conversion,[],[f1741]) ).
cnf(s232,plain,
( ~ spl0_2
| ~ spl0_96 ),
inference(sat_conversion,[],[f1742]) ).
cnf(s235,plain,
( ~ spl0_1
| ~ spl0_28
| ~ spl0_32
| ~ spl0_96
| spl0_131 ),
inference(sat_conversion,[],[f1745]) ).
cnf(s238,plain,
( ~ spl0_3
| ~ spl0_100 ),
inference(sat_conversion,[],[f1748]) ).
cnf(s241,plain,
( ~ spl0_2
| ~ spl0_107 ),
inference(sat_conversion,[],[f1751]) ).
cnf(s242,plain,
( ~ spl0_28
| ~ spl0_32
| ~ spl0_98
| ~ spl0_107
| spl0_122 ),
inference(sat_conversion,[],[f1752]) ).
cnf(s245,plain,
( ~ spl0_2
| ~ spl0_26
| ~ spl0_28
| ~ spl0_98
| spl0_132 ),
inference(sat_conversion,[],[f1755]) ).
cnf(s247,plain,
( ~ spl0_42
| ~ spl0_53 ),
inference(sat_conversion,[],[f1757]) ).
cnf(s248,plain,
( ~ spl0_23
| ~ spl0_148
| ~ spl0_155
| spl0_159 ),
inference(sat_conversion,[],[f1758]) ).
cnf(s249,plain,
( ~ spl0_103
| ~ spl0_112 ),
inference(sat_conversion,[],[f1759]) ).
cnf(s253,plain,
( ~ spl0_96
| ~ spl0_107 ),
inference(sat_conversion,[],[f1763]) ).
cnf(s254,plain,
( ~ spl0_18
| ~ spl0_87 ),
inference(sat_conversion,[],[f1764]) ).
cnf(s255,plain,
( ~ spl0_99
| ~ spl0_114 ),
inference(sat_conversion,[],[f1765]) ).
cnf(s256,plain,
( ~ spl0_103
| ~ spl0_111 ),
inference(sat_conversion,[],[f1766]) ).
cnf(s257,plain,
( ~ spl0_78
| ~ spl0_91 ),
inference(sat_conversion,[],[f1767]) ).
cnf(s260,plain,
( ~ spl0_28
| ~ spl0_96
| ~ spl0_106
| ~ spl0_115
| spl0_133 ),
inference(sat_conversion,[],[f1770]) ).
cnf(s262,plain,
( ~ spl0_83
| ~ spl0_93 ),
inference(sat_conversion,[],[f1772]) ).
cnf(s264,plain,
( ~ spl0_1
| ~ spl0_105 ),
inference(sat_conversion,[],[f1774]) ).
cnf(s265,plain,
( ~ spl0_14
| ~ spl0_57 ),
inference(sat_conversion,[],[f1775]) ).
cnf(s267,plain,
( ~ spl0_13
| ~ spl0_65 ),
inference(sat_conversion,[],[f1777]) ).
cnf(s269,plain,
( ~ spl0_72
| spl0_94
| ~ spl0_164 ),
inference(sat_conversion,[],[f1779]) ).
cnf(s271,plain,
( ~ spl0_63
| spl0_82
| ~ spl0_156 ),
inference(sat_conversion,[],[f1781]) ).
cnf(s273,plain,
( ~ spl0_57
| ~ spl0_68 ),
inference(sat_conversion,[],[f1783]) ).
cnf(s274,plain,
( ~ spl0_13
| ~ spl0_66 ),
inference(sat_conversion,[],[f1784]) ).
cnf(s279,plain,
( ~ spl0_58
| ~ spl0_68 ),
inference(sat_conversion,[],[f1789]) ).
cnf(s280,plain,
( ~ spl0_14
| ~ spl0_58 ),
inference(sat_conversion,[],[f1790]) ).
cnf(s281,plain,
( ~ spl0_17
| ~ spl0_93 ),
inference(sat_conversion,[],[f1791]) ).
cnf(s283,plain,
( ~ spl0_32
| ~ spl0_115
| spl0_116
| spl0_172
| spl0_173 ),
inference(sat_conversion,[],[f1851]) ).
cnf(s284,plain,
( ~ spl0_30
| ~ spl0_32
| spl0_118
| spl0_172
| spl0_174 ),
inference(sat_conversion,[],[f1855]) ).
cnf(s287,plain,
( ~ spl0_26
| spl0_177
| spl0_178 ),
inference(sat_conversion,[],[f1870]) ).
cnf(s288,plain,
( ~ spl0_26
| ~ spl0_30
| spl0_120
| spl0_174
| spl0_178 ),
inference(sat_conversion,[],[f1871]) ).
cnf(s295,plain,
( ~ spl0_30
| spl0_174
| spl0_180 ),
inference(sat_conversion,[],[f1884]) ).
cnf(s299,plain,
( ~ spl0_26
| ~ spl0_28
| spl0_132
| spl0_177
| spl0_181 ),
inference(sat_conversion,[],[f1891]) ).
cnf(s300,plain,
( ~ spl0_28
| ~ spl0_115
| spl0_133
| spl0_173
| spl0_181 ),
inference(sat_conversion,[],[f1892]) ).
cnf(s307,plain,
( ~ spl0_44
| ~ spl0_145
| ~ spl0_157 ),
inference(sat_conversion,[],[f1904]) ).
cnf(s308,plain,
( ~ spl0_23
| ~ spl0_39 ),
inference(sat_conversion,[],[f1905]) ).
cnf(s309,plain,
( ~ spl0_25
| ~ spl0_36 ),
inference(sat_conversion,[],[f1906]) ).
cnf(s315,plain,
( spl0_41
| ~ spl0_61
| ~ spl0_156 ),
inference(sat_conversion,[],[f1974]) ).
cnf(s316,plain,
( ~ spl0_14
| ~ spl0_68 ),
inference(sat_conversion,[],[f1975]) ).
cnf(s318,plain,
( spl0_54
| ~ spl0_70
| ~ spl0_164 ),
inference(sat_conversion,[],[f1980]) ).
cnf(s319,plain,
( ~ spl0_21
| ~ spl0_54 ),
inference(sat_conversion,[],[f1981]) ).
cnf(s320,plain,
( spl0_10
| ~ spl0_15
| ~ spl0_138
| ~ spl0_156 ),
inference(sat_conversion,[],[f1988]) ).
cnf(s322,plain,
( ~ spl0_6
| ~ spl0_34
| ~ spl0_145
| ~ spl0_157
| ~ spl0_166
| ~ spl0_169 ),
inference(sat_conversion,[],[f2012]) ).
cnf(s323,plain,
( ~ spl0_9
| ~ spl0_163
| ~ spl0_164
| ~ spl0_165
| ~ spl0_167
| ~ spl0_170 ),
inference(sat_conversion,[],[f2015]) ).
cnf(s324,plain,
( spl0_9
| ~ spl0_14
| ~ spl0_164
| ~ spl0_174 ),
inference(sat_conversion,[],[f2023]) ).
cnf(s325,plain,
( spl0_6
| ~ spl0_26
| spl0_163 ),
inference(sat_conversion,[],[f2027]) ).
cnf(s326,plain,
( spl0_8
| ~ spl0_91
| ~ spl0_155
| ~ spl0_172 ),
inference(sat_conversion,[],[f2034]) ).
cnf(s327,plain,
( spl0_9
| ~ spl0_92
| ~ spl0_164
| ~ spl0_180 ),
inference(sat_conversion,[],[f2040]) ).
cnf(s329,plain,
( spl0_9
| ~ spl0_30
| spl0_166 ),
inference(sat_conversion,[],[f2042]) ).
cnf(s332,plain,
( spl0_8
| ~ spl0_89
| ~ spl0_155
| ~ spl0_183 ),
inference(sat_conversion,[],[f2054]) ).
cnf(s333,plain,
( ~ spl0_17
| ~ spl0_82 ),
inference(sat_conversion,[],[f2055]) ).
cnf(s335,plain,
( ~ spl0_18
| ~ spl0_76 ),
inference(sat_conversion,[],[f2057]) ).
cnf(s336,plain,
( ~ spl0_20
| ~ spl0_91 ),
inference(sat_conversion,[],[f2058]) ).
cnf(s337,plain,
( ~ spl0_83
| ~ spl0_94 ),
inference(sat_conversion,[],[f2059]) ).
cnf(s338,plain,
( ~ spl0_92
| spl0_163
| ~ spl0_164
| ~ spl0_178 ),
inference(sat_conversion,[],[f2060]) ).
cnf(s340,plain,
( ~ spl0_28
| ~ spl0_32
| spl0_131
| spl0_138
| spl0_183 ),
inference(sat_conversion,[],[f2062]) ).
cnf(s342,plain,
( ~ spl0_76
| ~ spl0_88 ),
inference(sat_conversion,[],[f2064]) ).
cnf(s344,plain,
( spl0_7
| ~ spl0_60
| ~ spl0_136
| ~ spl0_158 ),
inference(sat_conversion,[],[f2077]) ).
cnf(s347,plain,
( ~ spl0_115
| ~ spl0_140
| spl0_144 ),
inference(sat_conversion,[],[f2080]) ).
cnf(s350,plain,
( ~ spl0_32
| ~ spl0_106
| ~ spl0_107
| ~ spl0_115
| spl0_116 ),
inference(sat_conversion,[],[f2083]) ).
cnf(s352,plain,
( ~ spl0_99
| ~ spl0_113 ),
inference(sat_conversion,[],[f2085]) ).
cnf(s354,plain,
( ~ spl0_97
| ~ spl0_105 ),
inference(sat_conversion,[],[f2087]) ).
cnf(s357,plain,
( spl0_33
| ~ spl0_60
| ~ spl0_134
| ~ spl0_158 ),
inference(sat_conversion,[],[f2090]) ).
cnf(s358,plain,
( ~ spl0_17
| ~ spl0_94 ),
inference(sat_conversion,[],[f2091]) ).
cnf(s359,plain,
( ~ spl0_12
| ~ spl0_72 ),
inference(sat_conversion,[],[f2092]) ).
cnf(s361,plain,
( ~ spl0_100
| ~ spl0_113 ),
inference(sat_conversion,[],[f2097]) ).
cnf(s365,plain,
( ~ spl0_14
| spl0_163
| ~ spl0_164
| ~ spl0_177 ),
inference(sat_conversion,[],[f2101]) ).
cnf(s366,plain,
( ~ spl0_59
| ~ spl0_137
| ~ spl0_157
| spl0_166 ),
inference(sat_conversion,[],[f2102]) ).
cnf(s367,plain,
( spl0_6
| ~ spl0_59
| ~ spl0_135
| ~ spl0_157 ),
inference(sat_conversion,[],[f2103]) ).
cnf(s368,plain,
( ~ spl0_59
| ~ spl0_134
| ~ spl0_157
| spl0_169 ),
inference(sat_conversion,[],[f2104]) ).
cnf(s369,plain,
( ~ spl0_59
| ~ spl0_136
| spl0_145
| ~ spl0_157 ),
inference(sat_conversion,[],[f2105]) ).
cnf(s372,plain,
( spl0_10
| ~ spl0_47
| ~ spl0_151
| ~ spl0_156 ),
inference(sat_conversion,[],[f2133]) ).
cnf(s376,plain,
( ~ spl0_57
| spl0_145
| ~ spl0_157
| ~ spl0_173 ),
inference(sat_conversion,[],[f2153]) ).
cnf(s377,plain,
( spl0_9
| ~ spl0_74
| ~ spl0_137
| ~ spl0_164 ),
inference(sat_conversion,[],[f2159]) ).
cnf(s380,plain,
( ~ spl0_2
| ~ spl0_26
| ~ spl0_106
| ~ spl0_115 ),
inference(sat_conversion,[],[f2162]) ).
cnf(s381,plain,
( spl0_42
| ~ spl0_62
| ~ spl0_158 ),
inference(sat_conversion,[],[f2163]) ).
cnf(s382,plain,
( ~ spl0_41
| ~ spl0_53 ),
inference(sat_conversion,[],[f2164]) ).
cnf(s383,plain,
( ~ spl0_42
| ~ spl0_54 ),
inference(sat_conversion,[],[f2165]) ).
cnf(s384,plain,
( spl0_6
| ~ spl0_26
| spl0_159 ),
inference(sat_conversion,[],[f2178]) ).
cnf(s385,plain,
( ~ spl0_39
| ~ spl0_147
| ~ spl0_157
| spl0_169 ),
inference(sat_conversion,[],[f2187]) ).
cnf(s386,plain,
( ~ spl0_32
| spl0_33
| spl0_170 ),
inference(sat_conversion,[],[f2207]) ).
cnf(s387,plain,
( spl0_6
| ~ spl0_39
| ~ spl0_148
| ~ spl0_157 ),
inference(sat_conversion,[],[f2211]) ).
cnf(s388,plain,
( spl0_33
| ~ spl0_78
| ~ spl0_158
| ~ spl0_172 ),
inference(sat_conversion,[],[f2217]) ).
cnf(s389,plain,
( spl0_6
| ~ spl0_57
| ~ spl0_157
| ~ spl0_177 ),
inference(sat_conversion,[],[f2222]) ).
cnf(s390,plain,
( ~ spl0_89
| ~ spl0_155
| spl0_160
| ~ spl0_186 ),
inference(sat_conversion,[],[f2227]) ).
cnf(s391,plain,
( ~ spl0_28
| ~ spl0_115
| spl0_133
| spl0_138
| spl0_186 ),
inference(sat_conversion,[],[f2228]) ).
cnf(s392,plain,
( spl0_10
| ~ spl0_90
| ~ spl0_156
| ~ spl0_187 ),
inference(sat_conversion,[],[f2234]) ).
cnf(s393,plain,
( ~ spl0_28
| spl0_138
| spl0_187 ),
inference(sat_conversion,[],[f2235]) ).
cnf(s394,plain,
( ~ spl0_82
| ~ spl0_94 ),
inference(sat_conversion,[],[f2236]) ).
cnf(s395,plain,
( spl0_33
| ~ spl0_80
| ~ spl0_158
| ~ spl0_183 ),
inference(sat_conversion,[],[f2241]) ).
cnf(s397,plain,
( ~ spl0_23
| ~ spl0_149
| ~ spl0_155
| spl0_160 ),
inference(sat_conversion,[],[f2243]) ).
cnf(s398,plain,
( ~ spl0_26
| ~ spl0_32
| ~ spl0_105
| ~ spl0_107 ),
inference(sat_conversion,[],[f2244]) ).
cnf(s399,plain,
( spl0_7
| ~ spl0_80
| ~ spl0_158
| ~ spl0_186 ),
inference(sat_conversion,[],[f2245]) ).
cnf(s401,plain,
( ~ spl0_89
| ~ spl0_155
| spl0_159
| ~ spl0_185 ),
inference(sat_conversion,[],[f2247]) ).
cnf(s402,plain,
( ~ spl0_26
| ~ spl0_28
| spl0_132
| spl0_138
| spl0_185 ),
inference(sat_conversion,[],[f2248]) ).
cnf(s404,plain,
( ~ spl0_41
| ~ spl0_54 ),
inference(sat_conversion,[],[f2250]) ).
cnf(s406,plain,
( ~ spl0_23
| ~ spl0_150
| ~ spl0_155
| spl0_161 ),
inference(sat_conversion,[],[f2252]) ).
cnf(s407,plain,
( spl0_10
| ~ spl0_20
| ~ spl0_156
| ~ spl0_181 ),
inference(sat_conversion,[],[f2268]) ).
cnf(s408,plain,
( ~ spl0_19
| spl0_163
| ~ spl0_164
| ~ spl0_185 ),
inference(sat_conversion,[],[f2298]) ).
cnf(s409,plain,
( ~ spl0_39
| ~ spl0_150
| ~ spl0_157
| spl0_166 ),
inference(sat_conversion,[],[f2299]) ).
cnf(s411,plain,
( ~ spl0_74
| ~ spl0_135
| spl0_163
| ~ spl0_164 ),
inference(sat_conversion,[],[f2301]) ).
cnf(s412,plain,
( spl0_8
| ~ spl0_32
| spl0_170 ),
inference(sat_conversion,[],[f2302]) ).
cnf(s414,plain,
( ~ spl0_91
| ~ spl0_155
| spl0_159
| ~ spl0_178 ),
inference(sat_conversion,[],[f2304]) ).
cnf(s415,plain,
( spl0_14
| spl0_65
| spl0_70
| spl0_72
| spl0_74 ),
inference(rat,[],[s143,s164]) ).
cnf(s416,plain,
( spl0_22
| spl0_36
| spl0_38
| spl0_40
| spl0_42 ),
inference(rat,[],[s134,s158]) ).
cnf(s417,plain,
( spl0_21
| spl0_35
| spl0_37
| spl0_39
| spl0_44 ),
inference(rat,[],[s133,s152]) ).
cnf(s418,plain,
( spl0_25
| spl0_41
| spl0_43
| spl0_45
| spl0_47 ),
inference(rat,[],[s132,s135]) ).
cnf(s419,plain,
( spl0_23
| spl0_48
| spl0_50
| spl0_52
| spl0_53 ),
inference(rat,[],[s131,s136]) ).
cnf(s420,plain,
~ spl0_133,
inference(rat,[],[s74,s90]) ).
cnf(s421,plain,
~ spl0_132,
inference(rat,[],[s73,s87]) ).
cnf(s422,plain,
~ spl0_131,
inference(rat,[],[s72,s84]) ).
cnf(s425,plain,
~ spl0_128,
inference(rat,[],[s69,s75]) ).
cnf(s428,plain,
~ spl0_122,
inference(rat,[],[s66,s84]) ).
cnf(s429,plain,
~ spl0_120,
inference(rat,[],[s65,s81]) ).
cnf(s430,plain,
~ spl0_118,
inference(rat,[],[s64,s78]) ).
cnf(s431,plain,
~ spl0_116,
inference(rat,[],[s63,s75]) ).
cnf(s432,plain,
( spl0_3
| spl0_7 ),
inference(rat,[],[s60,s62]) ).
cnf(s433,plain,
( spl0_8
| spl0_33 ),
inference(rat,[],[s12,s13]) ).
cnf(s435,plain,
( spl0_10
| spl0_29 ),
inference(rat,[],[s8,s9]) ).
cnf(s437,plain,
~ spl0_86,
inference(rat,[],[s43,s5]) ).
cnf(s438,plain,
~ spl0_85,
inference(rat,[],[s42,s5]) ).
cnf(s439,plain,
~ spl0_84,
inference(rat,[],[s41,s5]) ).
cnf(s440,plain,
~ spl0_81,
inference(rat,[],[s39,s5]) ).
cnf(s441,plain,
spl0_167,
inference(rat,[],[s151,s9,s4]) ).
cnf(s442,plain,
spl0_162,
inference(rat,[],[s148,s9,s4]) ).
cnf(s443,plain,
~ spl0_142,
inference(rat,[],[s108,s9,s4]) ).
cnf(s444,plain,
spl0_34,
inference(rat,[],[s14,s9,s4]) ).
cnf(s445,plain,
spl0_29,
inference(rat,[],[s435,s4]) ).
cnf(s446,plain,
spl0_4,
inference(rat,[],[s104,s11,s443]) ).
cnf(s447,plain,
~ spl0_101,
inference(rat,[],[s128,s446]) ).
cnf(s448,plain,
~ spl0_110,
inference(rat,[],[s125,s446]) ).
cnf(s449,plain,
~ spl0_109,
inference(rat,[],[s114,s446]) ).
cnf(s450,plain,
~ spl0_102,
inference(rat,[],[s109,s446]) ).
cnf(s452,plain,
spl0_140,
inference(rat,[],[s102,s7,s448]) ).
cnf(s456,plain,
spl0_144,
inference(rat,[],[s347,s62,s452]) ).
cnf(s459,plain,
~ spl0_43,
inference(rat,[],[s165,s135,s456]) ).
cnf(s460,plain,
~ spl0_38,
inference(rat,[],[s163,s3]) ).
cnf(s461,plain,
~ spl0_37,
inference(rat,[],[s156,s3]) ).
cnf(s462,plain,
~ spl0_52,
inference(rat,[],[s24,s3]) ).
cnf(s463,plain,
~ spl0_45,
inference(rat,[],[s20,s3]) ).
cnf(s464,plain,
~ spl0_66,
inference(rat,[],[s274,s2]) ).
cnf(s465,plain,
~ spl0_65,
inference(rat,[],[s267,s2]) ).
cnf(s466,plain,
~ spl0_56,
inference(rat,[],[s216,s2]) ).
cnf(s467,plain,
~ spl0_55,
inference(rat,[],[s173,s2]) ).
cnf(s468,plain,
( ~ spl0_1
| ~ spl0_2
| ~ spl0_3
| ~ spl0_5
| spl0_6
| spl0_7
| spl0_8
| spl0_9
| ~ spl0_11
| ~ spl0_12
| ~ spl0_14
| ~ spl0_15
| ~ spl0_17
| ~ spl0_18
| ~ spl0_19
| ~ spl0_20
| ~ spl0_21
| ~ spl0_22
| ~ spl0_23
| ~ spl0_25 ),
inference(rat,[],[s1,s3,s5,s2,s4,s446]) ).
cnf(s469,plain,
( ~ spl0_105
| spl0_100
| spl0_5 ),
inference(rat,[],[s213,s220,s225,s9,s450,s7,s421]) ).
cnf(s470,plain,
( ~ spl0_99
| spl0_5
| spl0_2
| spl0_1 ),
inference(rat,[],[s213,s242,s253,s178,s56,s179,s469,s50,s255,s352,s9,s450,s13,s428,s449,s7,s448]) ).
cnf(s471,plain,
( ~ spl0_98
| spl0_103
| spl0_3 ),
inference(rat,[],[s195,s122,s224,s447,s62,s9,s420]) ).
cnf(s472,plain,
( ~ spl0_113
| spl0_5
| spl0_3
| spl0_2 ),
inference(rat,[],[s195,s217,s260,s213,s471,s249,s179,s469,s57,s361,s447,s62,s9,s420,s450,s7,s448]) ).
cnf(s473,plain,
( ~ spl0_98
| spl0_113
| spl0_3
| spl0_1 ),
inference(rat,[],[s256,s178,s471,s242,s13,s449,s9,s428]) ).
cnf(s474,plain,
( spl0_5
| spl0_3
| spl0_2
| spl0_1 ),
inference(rat,[],[s256,s195,s178,s217,s253,s260,s213,s473,s214,s59,s184,s58,s472,s61,s470,s432,s447,s62,s13,s449,s9,s420,s450,s7,s445,s158,s11]) ).
cnf(s475,plain,
( ~ spl0_107
| spl0_103
| spl0_3 ),
inference(rat,[],[s195,s350,s54,s447,s62,s13,s431]) ).
cnf(s476,plain,
( ~ spl0_41
| spl0_50
| spl0_23
| spl0_40
| spl0_22 ),
inference(rat,[],[s161,s416,s419,s18,s382,s460,s462]) ).
cnf(s477,plain,
( spl0_50
| spl0_23
| spl0_40
| spl0_47
| spl0_22 ),
inference(rat,[],[s247,s419,s416,s141,s309,s418,s476,s462,s460,s459,s463]) ).
cnf(s478,plain,
( ~ spl0_58
| ~ spl0_41
| spl0_74
| spl0_59 ),
inference(rat,[],[s337,s210,s269,s153,s415,s27,s280,s318,s404,s157,s154,s152,s164,s467,s465]) ).
cnf(s479,plain,
( ~ spl0_41
| spl0_74
| spl0_59
| spl0_60 ),
inference(rat,[],[s265,s153,s415,s211,s359,s159,s478,s381,s157,s318,s18,s154,s404,s467,s152,s465,s466,s158,s164]) ).
cnf(s480,plain,
( ~ spl0_94
| spl0_11
| spl0_61
| spl0_160
| spl0_59
| spl0_6
| spl0_33 ),
inference(rat,[],[s257,s175,s221,s231,s342,s177,s395,s390,s392,s340,s391,s393,s320,s407,s144,s299,s273,s389,s153,s210,s271,s47,s337,s358,s394,s437,s136,s440,s158,s439,s135,s4,s422,s13,s9,s420,s62,s464,s421,s7,s152,s467]) ).
cnf(s481,plain,
( spl0_160
| spl0_59
| spl0_6
| spl0_60
| spl0_40
| spl0_33
| spl0_47
| ~ spl0_137
| spl0_22 ),
inference(rat,[],[s336,s175,s177,s335,s342,s221,s395,s390,s392,s340,s391,s393,s320,s144,s40,s215,s262,s30,s210,s388,s153,s284,s265,s316,s324,s415,s269,s480,s157,s318,s169,s383,s416,s309,s418,s315,s479,s377,s323,s146,s386,s325,s437,s136,s439,s135,s440,s158,s4,s422,s13,s9,s420,s62,s464,s152,s467,s430,s11,s164,s465,s460,s459,s463,s441,s7]) ).
cnf(s482,plain,
( spl0_6
| ~ spl0_150
| spl0_60
| spl0_40
| spl0_33
| spl0_47
| ~ spl0_137
| ~ spl0_135
| spl0_22 ),
inference(rat,[],[s406,s477,s209,s171,s481,s367,s384,s433,s136,s442,s152,s7]) ).
cnf(s483,plain,
( ~ spl0_50
| spl0_21
| spl0_35
| ~ spl0_6
| ~ spl0_150
| ~ spl0_147 ),
inference(rat,[],[s322,s385,s409,s145,s417,s171,s174,s444,s152,s62,s461,s136]) ).
cnf(s484,plain,
( ~ spl0_94
| spl0_59
| spl0_145
| spl0_11
| spl0_61
| spl0_33 ),
inference(rat,[],[s342,s221,s177,s395,s392,s340,s393,s320,s388,s407,s144,s283,s300,s273,s376,s153,s210,s271,s337,s358,s394,s440,s158,s439,s135,s4,s422,s13,s9,s464,s431,s62,s420,s152,s467]) ).
cnf(s485,plain,
( spl0_59
| spl0_74
| spl0_145
| spl0_159
| spl0_11
| spl0_70
| spl0_61
| spl0_33 ),
inference(rat,[],[s335,s175,s221,s401,s395,s402,s340,s320,s144,s215,s262,s30,s210,s388,s414,s153,s284,s288,s265,s316,s324,s415,s269,s484,s323,s150,s386,s142,s437,s136,s440,s158,s421,s9,s7,s422,s13,s4,s135,s464,s152,s467,s430,s11,s429,s164,s465,s441,s62]) ).
cnf(s486,plain,
( spl0_41
| ~ spl0_6
| ~ spl0_149
| ~ spl0_150
| spl0_33
| spl0_47
| ~ spl0_137
| ~ spl0_136
| spl0_22
| ~ spl0_147 ),
inference(rat,[],[s369,s485,s377,s323,s150,s307,s142,s417,s209,s308,s397,s406,s477,s483,s157,s318,s169,s383,s416,s212,s309,s418,s315,s386,s190,s433,s152,s164,s441,s62,s7,s461,s136,s442,s460,s459,s463,s135,s158,s13]) ).
cnf(s487,plain,
( spl0_3
| spl0_2
| spl0_1 ),
inference(rat,[],[s377,s479,s323,s369,s150,s307,s142,s417,s209,s308,s397,s406,s477,s483,s15,s416,s18,s154,s486,s482,s118,s119,s357,s433,s190,s386,s53,s354,s184,s179,s59,s61,s57,s352,s178,s475,s372,s120,s96,s94,s471,s95,s93,s99,s100,s196,s206,s474,s167,s432,s116,s164,s441,s152,s62,s7,s461,s136,s442,s460,s11,s158,s13,s445,s448,s449,s4,s135,s9]) ).
cnf(s488,plain,
( ~ spl0_105
| ~ spl0_3
| spl0_1 ),
inference(rat,[],[s206,s178,s469,s398,s238,s188,s13,s449,s7]) ).
cnf(s489,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s213,s242,s253,s178,s56,s100,s179,s488,s188,s191,s238,s487,s448,s7,s449,s428,s13,s450,s9]) ).
cnf(s490,plain,
( ~ spl0_113
| ~ spl0_2 ),
inference(rat,[],[s196,s195,s213,s188,s361,s380,s245,s232,s197,s447,s62,s9,s450,s421,s7]) ).
cnf(s491,plain,
spl0_1,
inference(rat,[],[s238,s213,s195,s206,s256,s178,s490,s197,s232,s241,s245,s380,s489,s9,s450,s447,s62,s13,s449,s7,s421]) ).
cnf(s492,plain,
~ spl0_105,
inference(rat,[],[s264,s491]) ).
cnf(s493,plain,
~ spl0_96,
inference(rat,[],[s235,s422,s9,s13,s491]) ).
cnf(s494,plain,
~ spl0_97,
inference(rat,[],[s227,s491]) ).
cnf(s495,plain,
~ spl0_108,
inference(rat,[],[s200,s425,s62,s13,s491]) ).
cnf(s497,plain,
~ spl0_98,
inference(rat,[],[s123,s491]) ).
cnf(s498,plain,
~ spl0_106,
inference(rat,[],[s121,s491]) ).
cnf(s499,plain,
spl0_148,
inference(rat,[],[s117,s7,s492]) ).
cnf(s500,plain,
spl0_150,
inference(rat,[],[s119,s11,s494]) ).
cnf(s501,plain,
spl0_151,
inference(rat,[],[s120,s9,s497]) ).
cnf(s502,plain,
spl0_149,
inference(rat,[],[s118,s62,s498]) ).
cnf(s503,plain,
~ spl0_47,
inference(rat,[],[s372,s135,s4,s501]) ).
cnf(s504,plain,
~ spl0_113,
inference(rat,[],[s100,s179,s213,s490,s57,s361,s7,s448,s492,s9,s493,s497,s450]) ).
cnf(s505,plain,
spl0_33,
inference(rat,[],[s58,s13,s504]) ).
cnf(s506,plain,
spl0_3,
inference(rat,[],[s184,s61,s59,s50,s214,s213,s196,s195,s432,s445,s505,s158,s11,s7,s9,s493,s497,s450,s447,s495,s498,s62]) ).
cnf(s507,plain,
~ spl0_100,
inference(rat,[],[s238,s506]) ).
cnf(s508,plain,
~ spl0_99,
inference(rat,[],[s201,s506]) ).
cnf(s509,plain,
~ spl0_114,
inference(rat,[],[s191,s506]) ).
cnf(s510,plain,
spl0_5,
inference(rat,[],[s213,s450,s497,s493,s9,s507]) ).
cnf(s511,plain,
spl0_31,
inference(rat,[],[s61,s11,s508]) ).
cnf(s512,plain,
spl0_27,
inference(rat,[],[s59,s7,s509]) ).
cnf(s513,plain,
~ spl0_111,
inference(rat,[],[s206,s510]) ).
cnf(s514,plain,
~ spl0_103,
inference(rat,[],[s196,s510]) ).
cnf(s515,plain,
~ spl0_112,
inference(rat,[],[s100,s510]) ).
cnf(s516,plain,
~ spl0_104,
inference(rat,[],[s99,s510]) ).
cnf(s517,plain,
~ spl0_7,
inference(rat,[],[s184,s158,s511,s505,s445,s512]) ).
cnf(s518,plain,
spl0_134,
inference(rat,[],[s93,s13,s513]) ).
cnf(s519,plain,
spl0_136,
inference(rat,[],[s95,s62,s514]) ).
cnf(s520,plain,
spl0_135,
inference(rat,[],[s94,s7,s515]) ).
cnf(s521,plain,
spl0_2,
inference(rat,[],[s179,s492,s509,s448,s7,s515]) ).
cnf(s522,plain,
spl0_137,
inference(rat,[],[s96,s11,s516]) ).
cnf(s523,plain,
spl0_160,
inference(rat,[],[s187,s62,s517]) ).
cnf(s524,plain,
spl0_165,
inference(rat,[],[s168,s62,s517]) ).
cnf(s525,plain,
spl0_145,
inference(rat,[],[s112,s62,s517]) ).
cnf(s526,plain,
~ spl0_40,
inference(rat,[],[s186,s158,s502,s517]) ).
cnf(s527,plain,
~ spl0_60,
inference(rat,[],[s344,s158,s519,s517]) ).
cnf(s530,plain,
~ spl0_50,
inference(rat,[],[s171,s136,s523]) ).
cnf(s531,plain,
~ spl0_44,
inference(rat,[],[s307,s152,s525]) ).
cnf(s532,plain,
( ~ spl0_42
| ~ spl0_25 ),
inference(rat,[],[s308,s417,s419,s169,s247,s212,s141,s461,s531,s530,s462]) ).
cnf(s533,plain,
( ~ spl0_72
| spl0_59
| spl0_11
| spl0_62 ),
inference(rat,[],[s153,s210,s27,s337,s159,s269,s359,s467,s152,s466,s527,s158,s164]) ).
cnf(s534,plain,
( ~ spl0_14
| spl0_59
| spl0_11
| spl0_62 ),
inference(rat,[],[s211,s153,s159,s265,s280,s467,s152,s466,s527,s158]) ).
cnf(s535,plain,
( ~ spl0_53
| ~ spl0_25 ),
inference(rat,[],[s205,s377,s411,s415,s534,s533,s368,s322,s387,s409,s318,s417,s157,s25,s170,s212,s381,s532,s13,s164,s524,s441,s522,s520,s465,s152,s518,s444,s525,s499,s500,s461,s531,s158]) ).
cnf(s536,plain,
( spl0_11
| spl0_74
| spl0_59
| ~ spl0_25 ),
inference(rat,[],[s415,s534,s533,s381,s532,s318,s319,s417,s308,s419,s535,s141,s212,s465,s164,s531,s461,s462,s530,s158]) ).
cnf(s537,plain,
( ~ spl0_78
| spl0_89
| spl0_90
| spl0_93
| spl0_82 ),
inference(rat,[],[s231,s177,s175,s226,s257,s439,s135,s437,s136]) ).
cnf(s538,plain,
( ~ spl0_72
| spl0_41 ),
inference(rat,[],[s336,s175,s177,s335,s342,s221,s537,s332,s399,s392,s340,s391,s393,s320,s144,s271,s279,s47,s358,s394,s159,s269,s359,s315,s381,s532,s209,s248,s406,s419,s535,s141,s418,s437,s136,s439,s135,s440,s158,s517,s4,s422,s13,s9,s420,s62,s464,s466,s527,s164,s442,s523,s500,s503,s463,s459,s462,s530,s499]) ).
cnf(s539,plain,
( spl0_6
| spl0_59
| spl0_41 ),
inference(rat,[],[s468,s177,s176,s231,s254,s175,s332,s392,s340,s393,s320,s144,s271,s281,s333,s358,s326,s327,s162,s284,s295,s159,s324,s280,s316,s415,s536,s377,s323,s325,s315,s381,s416,s532,s309,s209,s208,s248,s406,s318,s319,s417,s308,s419,s535,s141,s212,s418,s538,s491,s521,s506,s510,s517,s439,s135,s438,s164,s437,s136,s4,s422,s13,s9,s464,s158,s430,s11,s466,s527,s465,s522,s441,s524,s7,s531,s503,s463,s459,s461,s462,s530,s523,s442,s500,s499,s526,s460]) ).
cnf(s540,plain,
( spl0_163
| spl0_41 ),
inference(rat,[],[s44,s176,s177,s408,s392,s402,s393,s320,s144,s271,s333,s358,s407,s338,s162,s299,s287,s159,s365,s280,s316,s415,s411,s315,s381,s532,s318,s319,s417,s308,s419,s535,s141,s212,s418,s538,s438,s164,s439,s135,s4,s421,s9,s7,s464,s158,s466,s527,s465,s520,s531,s503,s463,s459,s461,s462,s530]) ).
cnf(s541,plain,
spl0_41,
inference(rat,[],[s539,s367,s322,s329,s323,s540,s208,s207,s248,s406,s419,s535,s141,s418,s520,s152,s444,s525,s11,s164,s441,s524,s136,s13,s442,s523,s499,s500,s530,s462,s459,s463,s503]) ).
cnf(s543,plain,
~ spl0_53,
inference(rat,[],[s382,s541]) ).
cnf(s544,plain,
~ spl0_21,
inference(rat,[],[s154,s541]) ).
cnf(s549,plain,
~ spl0_59,
inference(rat,[],[s322,s366,s367,s368,s444,s152,s525,s522,s520,s518]) ).
cnf(s550,plain,
spl0_74,
inference(rat,[],[s479,s527,s541,s549]) ).
cnf(s553,plain,
spl0_163,
inference(rat,[],[s411,s164,s520,s550]) ).
cnf(s554,plain,
spl0_9,
inference(rat,[],[s377,s164,s522,s550]) ).
cnf(s557,plain,
~ spl0_170,
inference(rat,[],[s323,s524,s441,s553,s164,s554]) ).
cnf(s558,plain,
spl0_169,
inference(rat,[],[s205,s553,s441,s524,s164,s13,s554]) ).
cnf(s559,plain,
spl0_8,
inference(rat,[],[s412,s13,s557]) ).
cnf(s561,plain,
spl0_6,
inference(rat,[],[s419,s155,s406,s417,s209,s387,s384,s530,s462,s543,s136,s500,s461,s544,s531,s559,s523,s442,s499,s152,s7]) ).
cnf(s562,plain,
~ spl0_166,
inference(rat,[],[s322,s558,s525,s152,s444,s561]) ).
cnf(s563,plain,
spl0_161,
inference(rat,[],[s147,s11,s562]) ).
cnf(s564,plain,
~ spl0_39,
inference(rat,[],[s409,s500,s152,s562]) ).
cnf(s565,plain,
~ spl0_159,
inference(rat,[],[s208,s523,s442,s557,s13,s136,s563]) ).
cnf(s566,plain,
spl0_35,
inference(rat,[],[s417,s531,s544,s461,s564]) ).
cnf(s567,plain,
~ spl0_23,
inference(rat,[],[s248,s499,s136,s565]) ).
cnf(s568,plain,
~ spl0_48,
inference(rat,[],[s155,s566]) ).
cnf(s571,plain,
$false,
inference(rat,[],[s419,s543,s462,s530,s568,s567]) ).
fof(f2305,plain,
$false,
inference(avatar_sat_refutation,[],[s571]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03 % Problem : PUZ010-1 : TPTP v9.3.1. Bugfixed v1.0.1.
% 0.00/0.05 % Command : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.37 % Computer : n009.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 : Sun Sep 27 22:29:15 UTC 2026
% 0.10/0.37 % CPUTime :
% 0.10/0.37 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 SAT
% 0.10/0.39 Running first-order model finding
% 0.10/0.39 Running: /export/starexec/sandbox2/solver/bin/vampire-ho --input_syntax tptp --output_axiom_names on --mode casc --intent sat -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.36/0.50 % (2471791)Will run a generic schedule for satisfiability detection.
% 0.36/0.50 % (2471798)dis+10_161_sil=256000:plsq=on:plsqr=61199697,1048576:gs=on:alpa=true:sac=on:slsq=on:cn=on:random_seed=4088471422:i=88024:add=on:rawr=on_2999 on theBenchmark for (2999ds/88024Mi)
% 0.36/0.50 % (2471797)% WARNING: option uhcvi not known.
% 0.36/0.50 % (2471796)fmb+10_1_sas=cadical:bce=on:rp=on:random_seed=3507532127_2999 on theBenchmark for (2999ds/0Mi)
% 0.36/0.50 % (2471799)dis+10_1_sil=32000:sp=arity:random_seed=3333735673:i=103:fgj=on_2999 on theBenchmark for (2999ds/103Mi)
% 0.36/0.50 % (2471800)ott+31_1_sil=16000:lcm=predicate:bce=on:newcnf=on:random_seed=2722876807:i=116_2999 on theBenchmark for (2999ds/116Mi)
% 0.36/0.50 % (2471801)ott+1_1_to=lpo:sil=16000:sp=reverse_arity:erd=off:random_seed=4061889779:i=131_2999 on theBenchmark for (2999ds/131Mi)
% 0.36/0.50 % (2471802)ott-3_16_to=lpo:sil=16000:sp=arity:fd=off:rp=on:random_seed=3145627638:i=159:bs=unit_only:nicw=on:fsr=off:amm=off_2999 on theBenchmark for (2999ds/159Mi)
% 0.36/0.50 % (2471797)dis+11_61:31_drc=ordering:lsd=5:bsr=unit_only:rp=on:newcnf=on:random_seed=4152602686:i=135531:add=off:rawr=on_2999 on theBenchmark for (2999ds/135531Mi)
% 0.36/0.50 % Detected minimum model sizes of [1]
% 0.36/0.50 % Detected maximum model sizes of [30]
% 0.36/0.50 % TRYING [1]
% 0.36/0.50 % TRYING [2]
% 0.36/0.50 % TRYING [3]
% 0.36/0.50 % TRYING [4]
% 0.36/0.50 % TRYING [5]
% 0.36/0.50 % (2471802) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2471791-2471802"...
% 0.36/0.50 % (2471801) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2471791-2471801"...
% 0.36/0.50 % (2471800) found proof, printing to "/export/starexec/sandbox2/tmp/vampire-proof-2471791-2471800"...
% 0.36/0.50 % TRYING [6]
% 0.36/0.50 % (2471802)...printing done.
% 0.36/0.50 % (2471802)Refutation found. Thanks to Tanya!
% 0.36/0.50 % SZS status Unsatisfiable for theBenchmark
% 0.36/0.50 % SZS output start Proof for theBenchmark
% See solution above
% 0.36/0.50 % (2471802)------------------------------
% 0.36/0.50 % (2471802)Version: Vampire 5.0.1 (Release build, commit 5ef7c2677 on 2026-07-16 16:54:09 +0200)
% 0.36/0.50 % (2471802)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.36/0.50 % (2471802)CaDiCaL version: 2.1.3
% 0.36/0.50 % (2471802)Termination reason: Refutation
% 0.36/0.50 % (2471802)Time elapsed: 0.047 s
% 0.36/0.50 % (2471802)Peak memory usage: 13 MB
% 0.36/0.50 % (2471802)Instructions burned: 74 (million)
% 0.36/0.50 % (2471791)Success in time 0.093 s
% 0.36/0.50 % Vampire exiting
%------------------------------------------------------------------------------