%------------------------------------------------------------------------------
% File : Vampire---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 THM
% Computer : n003.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:04 PM UTC 2026
% Result : Unsatisfiable 3.00s 1.28s
% Output : Refutation 3.72s
% Verified :
% SZS Type : Refutation
% Derivation depth : 48
% Number of leaves : 264
% Syntax : Number of formulae : 1158 ( 194 unt; 147 def)
% Number of atoms : 3041 ( 0 equ)
% Maximal formula atoms : 25 ( 2 avg)
% Number of connectives : 3819 (1936 ~;1736 |; 0 &)
% ( 147 <=>; 0 =>; 0 <=; 0 <~>)
% Maximal formula depth : 26 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of predicates : 161 ( 160 usr; 148 prp; 0-2 aty)
% Number of functors : 30 ( 30 usr; 30 con; 0-0 aty)
% Number of variables : 166 ( 0 sgn 166 !; 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] :
( ~ person(X0)
| drinks(X0,orange)
| drinks(X0,coffee)
| drinks(X0,tea)
| drinks(X0,milk)
| drinks(X0,water) ),
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] :
( ~ person(X0)
| drives(X0,masserati)
| drives(X0,saab)
| drives(X0,porsche)
| drives(X0,honda)
| drives(X0,jaguar) ),
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] :
( ~ person(X0)
| owns(X0,dog)
| owns(X0,snails)
| owns(X0,horse)
| owns(X0,fox)
| owns(X0,zebra) ),
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] :
( ~ house(X0)
| is_color(X0,red)
| is_color(X0,yellow)
| is_color(X0,blue)
| is_color(X0,green)
| is_color(X0,ivory) ),
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] :
( ~ house(X0)
| is_color(X0,red)
| ~ 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] :
( ~ person(X1)
| is_color(X0,yellow)
| ~ 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] :
( ~ next_to(X1,X0)
| ~ house(X1)
| ~ lives(norwegian,X1)
| ~ house(X0)
| is_color(X0,blue) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',norwegian_in_blue_house) ).
fof(f92,axiom,
! [X0] :
( ~ person(X0)
| owns(X0,snails)
| ~ drives(X0,porsche) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',porsche_with_snails) ).
fof(f93,axiom,
! [X0] :
( ~ person(X0)
| drinks(X0,orange)
| ~ drives(X0,honda) ),
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] :
( ~ person(X1)
| is_color(X0,green)
| ~ 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] :
( ~ person(X0)
| lives(X0,house_3)
| ~ 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(f102,axiom,
! [X0,X1] :
( ~ next_to(X0,X1)
| left_of(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(f113,axiom,
~ left_of(house_3,house_2),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',house_3_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(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(f130,definition,
( spl0_1
<=> is_color(house_5,green) ),
introduced(definition,[new_symbols(definition,[spl0_1])],[avatar_definition]) ).
fof(f133,definition,
( spl0_2
<=> is_color(house_4,ivory) ),
introduced(definition,[new_symbols(definition,[spl0_2])],[avatar_definition]) ).
fof(f136,definition,
( spl0_3
<=> is_color(house_3,red) ),
introduced(definition,[new_symbols(definition,[spl0_3])],[avatar_definition]) ).
fof(f139,definition,
( spl0_4
<=> is_color(house_2,blue) ),
introduced(definition,[new_symbols(definition,[spl0_4])],[avatar_definition]) ).
fof(f140,plain,
( ~ is_color(house_2,blue)
| spl0_4 ),
inference(avatar_component_clause,[],[f139]) ).
fof(f142,definition,
( spl0_5
<=> is_color(house_1,yellow) ),
introduced(definition,[new_symbols(definition,[spl0_5])],[avatar_definition]) ).
fof(f145,definition,
( spl0_6
<=> lives(spaniard,house_4) ),
introduced(definition,[new_symbols(definition,[spl0_6])],[avatar_definition]) ).
fof(f148,definition,
( spl0_7
<=> lives(english,house_3) ),
introduced(definition,[new_symbols(definition,[spl0_7])],[avatar_definition]) ).
fof(f151,definition,
( spl0_8
<=> lives(japanese,house_5) ),
introduced(definition,[new_symbols(definition,[spl0_8])],[avatar_definition]) ).
fof(f154,definition,
( spl0_9
<=> lives(ukranian,house_2) ),
introduced(definition,[new_symbols(definition,[spl0_9])],[avatar_definition]) ).
fof(f157,definition,
( spl0_10
<=> lives(norwegian,house_1) ),
introduced(definition,[new_symbols(definition,[spl0_10])],[avatar_definition]) ).
fof(f158,plain,
( ~ lives(norwegian,house_1)
| spl0_10 ),
inference(avatar_component_clause,[],[f157]) ).
fof(f160,definition,
( spl0_11
<=> drives(spaniard,honda) ),
introduced(definition,[new_symbols(definition,[spl0_11])],[avatar_definition]) ).
fof(f163,definition,
( spl0_12
<=> drives(english,porsche) ),
introduced(definition,[new_symbols(definition,[spl0_12])],[avatar_definition]) ).
fof(f166,definition,
( spl0_13
<=> drives(japanese,jaguar) ),
introduced(definition,[new_symbols(definition,[spl0_13])],[avatar_definition]) ).
fof(f167,plain,
( ~ drives(japanese,jaguar)
| spl0_13 ),
inference(avatar_component_clause,[],[f166]) ).
fof(f169,definition,
( spl0_14
<=> drives(ukranian,saab) ),
introduced(definition,[new_symbols(definition,[spl0_14])],[avatar_definition]) ).
fof(f172,definition,
( spl0_15
<=> drives(norwegian,masserati) ),
introduced(definition,[new_symbols(definition,[spl0_15])],[avatar_definition]) ).
fof(f175,definition,
( spl0_16
<=> owns(spaniard,dog) ),
introduced(definition,[new_symbols(definition,[spl0_16])],[avatar_definition]) ).
fof(f176,plain,
( ~ owns(spaniard,dog)
| spl0_16 ),
inference(avatar_component_clause,[],[f175]) ).
fof(f178,definition,
( spl0_17
<=> owns(english,snails) ),
introduced(definition,[new_symbols(definition,[spl0_17])],[avatar_definition]) ).
fof(f181,definition,
( spl0_18
<=> owns(japanese,zebra) ),
introduced(definition,[new_symbols(definition,[spl0_18])],[avatar_definition]) ).
fof(f184,definition,
( spl0_19
<=> owns(ukranian,horse) ),
introduced(definition,[new_symbols(definition,[spl0_19])],[avatar_definition]) ).
fof(f187,definition,
( spl0_20
<=> owns(norwegian,fox) ),
introduced(definition,[new_symbols(definition,[spl0_20])],[avatar_definition]) ).
fof(f190,definition,
( spl0_21
<=> drinks(spaniard,orange) ),
introduced(definition,[new_symbols(definition,[spl0_21])],[avatar_definition]) ).
fof(f193,definition,
( spl0_22
<=> drinks(english,milk) ),
introduced(definition,[new_symbols(definition,[spl0_22])],[avatar_definition]) ).
fof(f196,definition,
( spl0_23
<=> drinks(japanese,coffee) ),
introduced(definition,[new_symbols(definition,[spl0_23])],[avatar_definition]) ).
fof(f199,definition,
( spl0_24
<=> drinks(ukranian,tea) ),
introduced(definition,[new_symbols(definition,[spl0_24])],[avatar_definition]) ).
fof(f200,plain,
( ~ drinks(ukranian,tea)
| spl0_24 ),
inference(avatar_component_clause,[],[f199]) ).
fof(f202,definition,
( spl0_25
<=> drinks(norwegian,water) ),
introduced(definition,[new_symbols(definition,[spl0_25])],[avatar_definition]) ).
fof(f204,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,[],[f128,f202,f199,f196,f193,f190,f187,f184,f181,f178,f175,f172,f169,f166,f163,f160,f157,f154,f151,f148,f145,f142,f139,f136,f133,f130]) ).
fof(f207,plain,
( ~ lives(english,house_3)
| ~ lives(spaniard,house_3) ),
inference(resolution,[],[f2,f63]) ).
fof(f209,plain,
( ~ lives(english,house_5)
| ~ lives(spaniard,house_5) ),
inference(resolution,[],[f2,f65]) ).
fof(f211,definition,
( spl0_26
<=> lives(spaniard,house_5) ),
introduced(definition,[new_symbols(definition,[spl0_26])],[avatar_definition]) ).
fof(f214,definition,
( spl0_27
<=> lives(english,house_5) ),
introduced(definition,[new_symbols(definition,[spl0_27])],[avatar_definition]) ).
fof(f216,plain,
( ~ spl0_26
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f209,f214,f211]) ).
fof(f218,definition,
( spl0_28
<=> lives(english,house_4) ),
introduced(definition,[new_symbols(definition,[spl0_28])],[avatar_definition]) ).
fof(f222,definition,
( spl0_29
<=> lives(spaniard,house_3) ),
introduced(definition,[new_symbols(definition,[spl0_29])],[avatar_definition]) ).
fof(f224,plain,
( ~ spl0_29
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f207,f148,f222]) ).
fof(f226,definition,
( spl0_30
<=> lives(spaniard,house_2) ),
introduced(definition,[new_symbols(definition,[spl0_30])],[avatar_definition]) ).
fof(f229,definition,
( spl0_31
<=> lives(english,house_2) ),
introduced(definition,[new_symbols(definition,[spl0_31])],[avatar_definition]) ).
fof(f233,definition,
( spl0_32
<=> lives(spaniard,house_1) ),
introduced(definition,[new_symbols(definition,[spl0_32])],[avatar_definition]) ).
fof(f236,definition,
( spl0_33
<=> lives(english,house_1) ),
introduced(definition,[new_symbols(definition,[spl0_33])],[avatar_definition]) ).
fof(f239,plain,
( ~ lives(english,house_1)
| ~ lives(norwegian,house_1) ),
inference(resolution,[],[f3,f61]) ).
fof(f254,plain,
( ~ lives(english,house_3)
| ~ lives(ukranian,house_3) ),
inference(resolution,[],[f4,f63]) ).
fof(f256,plain,
( ~ lives(english,house_5)
| ~ lives(ukranian,house_5) ),
inference(resolution,[],[f4,f65]) ).
fof(f260,plain,
( ~ lives(english,house_3)
| ~ lives(japanese,house_3) ),
inference(resolution,[],[f5,f63]) ).
fof(f262,plain,
( ~ lives(english,house_5)
| ~ lives(japanese,house_5) ),
inference(resolution,[],[f5,f65]) ).
fof(f264,definition,
( spl0_36
<=> lives(japanese,house_2) ),
introduced(definition,[new_symbols(definition,[spl0_36])],[avatar_definition]) ).
fof(f267,plain,
( ~ lives(spaniard,house_1)
| ~ lives(norwegian,house_1) ),
inference(resolution,[],[f6,f61]) ).
fof(f277,definition,
( spl0_38
<=> lives(norwegian,house_3) ),
introduced(definition,[new_symbols(definition,[spl0_38])],[avatar_definition]) ).
fof(f280,plain,
( ~ spl0_10
| ~ spl0_32 ),
inference(avatar_split_clause,[],[f267,f233,f157]) ).
fof(f281,plain,
( $false
| spl0_10 ),
inference(resolution,[],[f158,f88]) ).
fof(f282,plain,
spl0_10,
inference(avatar_contradiction_clause,[],[f281]) ).
fof(f284,plain,
( ~ lives(spaniard,house_2)
| ~ lives(ukranian,house_2) ),
inference(resolution,[],[f7,f62]) ).
fof(f285,plain,
( ~ lives(spaniard,house_3)
| ~ lives(ukranian,house_3) ),
inference(resolution,[],[f7,f63]) ).
fof(f286,plain,
( ~ lives(spaniard,house_4)
| ~ lives(ukranian,house_4) ),
inference(resolution,[],[f7,f64]) ).
fof(f287,plain,
( ~ lives(spaniard,house_5)
| ~ lives(ukranian,house_5) ),
inference(resolution,[],[f7,f65]) ).
fof(f289,definition,
( spl0_39
<=> lives(ukranian,house_5) ),
introduced(definition,[new_symbols(definition,[spl0_39])],[avatar_definition]) ).
fof(f291,plain,
( ~ spl0_39
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f287,f211,f289]) ).
fof(f293,definition,
( spl0_40
<=> lives(ukranian,house_3) ),
introduced(definition,[new_symbols(definition,[spl0_40])],[avatar_definition]) ).
fof(f295,plain,
( ~ spl0_40
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f285,f222,f293]) ).
fof(f298,plain,
( ~ lives(spaniard,house_3)
| ~ lives(japanese,house_3) ),
inference(resolution,[],[f8,f63]) ).
fof(f299,plain,
( ~ lives(spaniard,house_4)
| ~ lives(japanese,house_4) ),
inference(resolution,[],[f8,f64]) ).
fof(f300,plain,
( ~ lives(spaniard,house_5)
| ~ lives(japanese,house_5) ),
inference(resolution,[],[f8,f65]) ).
fof(f302,definition,
( spl0_41
<=> lives(japanese,house_3) ),
introduced(definition,[new_symbols(definition,[spl0_41])],[avatar_definition]) ).
fof(f304,plain,
( ~ spl0_41
| ~ spl0_29 ),
inference(avatar_split_clause,[],[f298,f222,f302]) ).
fof(f305,plain,
( ~ lives(norwegian,house_1)
| ~ lives(ukranian,house_1) ),
inference(resolution,[],[f9,f61]) ).
fof(f311,definition,
( spl0_42
<=> lives(ukranian,house_4) ),
introduced(definition,[new_symbols(definition,[spl0_42])],[avatar_definition]) ).
fof(f315,definition,
( spl0_43
<=> lives(ukranian,house_1) ),
introduced(definition,[new_symbols(definition,[spl0_43])],[avatar_definition]) ).
fof(f317,plain,
( ~ spl0_43
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f305,f157,f315]) ).
fof(f318,plain,
( ~ lives(norwegian,house_1)
| ~ lives(japanese,house_1) ),
inference(resolution,[],[f10,f61]) ).
fof(f324,definition,
( spl0_44
<=> lives(japanese,house_1) ),
introduced(definition,[new_symbols(definition,[spl0_44])],[avatar_definition]) ).
fof(f326,plain,
( ~ spl0_44
| ~ spl0_10 ),
inference(avatar_split_clause,[],[f318,f157,f324]) ).
fof(f328,plain,
( ~ lives(ukranian,house_2)
| ~ lives(japanese,house_2) ),
inference(resolution,[],[f11,f62]) ).
fof(f329,plain,
( ~ lives(ukranian,house_3)
| ~ lives(japanese,house_3) ),
inference(resolution,[],[f11,f63]) ).
fof(f330,plain,
( ~ lives(ukranian,house_4)
| ~ lives(japanese,house_4) ),
inference(resolution,[],[f11,f64]) ).
fof(f331,plain,
( ~ lives(ukranian,house_5)
| ~ lives(japanese,house_5) ),
inference(resolution,[],[f11,f65]) ).
fof(f332,plain,
( ~ spl0_8
| ~ spl0_39 ),
inference(avatar_split_clause,[],[f331,f289,f151]) ).
fof(f334,definition,
( spl0_45
<=> lives(japanese,house_4) ),
introduced(definition,[new_symbols(definition,[spl0_45])],[avatar_definition]) ).
fof(f336,plain,
( ~ spl0_45
| ~ spl0_42 ),
inference(avatar_split_clause,[],[f330,f311,f334]) ).
fof(f337,plain,
( ~ drinks(english,orange)
| ~ drinks(spaniard,orange) ),
inference(resolution,[],[f13,f77]) ).
fof(f341,plain,
( ~ drinks(english,water)
| ~ drinks(spaniard,water) ),
inference(resolution,[],[f13,f78]) ).
fof(f343,definition,
( spl0_46
<=> drinks(spaniard,water) ),
introduced(definition,[new_symbols(definition,[spl0_46])],[avatar_definition]) ).
fof(f346,definition,
( spl0_47
<=> drinks(english,water) ),
introduced(definition,[new_symbols(definition,[spl0_47])],[avatar_definition]) ).
fof(f348,plain,
( ~ spl0_46
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f341,f346,f343]) ).
fof(f350,definition,
( spl0_48
<=> drinks(spaniard,milk) ),
introduced(definition,[new_symbols(definition,[spl0_48])],[avatar_definition]) ).
fof(f354,definition,
( spl0_49
<=> drinks(spaniard,tea) ),
introduced(definition,[new_symbols(definition,[spl0_49])],[avatar_definition]) ).
fof(f357,definition,
( spl0_50
<=> drinks(english,tea) ),
introduced(definition,[new_symbols(definition,[spl0_50])],[avatar_definition]) ).
fof(f361,definition,
( spl0_51
<=> drinks(spaniard,coffee) ),
introduced(definition,[new_symbols(definition,[spl0_51])],[avatar_definition]) ).
fof(f364,definition,
( spl0_52
<=> drinks(english,coffee) ),
introduced(definition,[new_symbols(definition,[spl0_52])],[avatar_definition]) ).
fof(f368,definition,
( spl0_53
<=> drinks(english,orange) ),
introduced(definition,[new_symbols(definition,[spl0_53])],[avatar_definition]) ).
fof(f370,plain,
( ~ spl0_21
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f337,f368,f190]) ).
fof(f371,plain,
( ~ drinks(english,orange)
| ~ drinks(norwegian,orange) ),
inference(resolution,[],[f14,f77]) ).
fof(f375,plain,
( ~ drinks(english,water)
| ~ drinks(norwegian,water) ),
inference(resolution,[],[f14,f78]) ).
fof(f377,definition,
( spl0_54
<=> drinks(norwegian,orange) ),
introduced(definition,[new_symbols(definition,[spl0_54])],[avatar_definition]) ).
fof(f379,plain,
( ~ spl0_54
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f371,f368,f377]) ).
fof(f380,plain,
( ~ drinks(english,orange)
| ~ drinks(ukranian,orange) ),
inference(resolution,[],[f15,f77]) ).
fof(f382,plain,
( ~ drinks(english,tea)
| ~ drinks(ukranian,tea) ),
inference(resolution,[],[f15,f76]) ).
fof(f385,plain,
( ~ drinks(english,orange)
| ~ drinks(japanese,orange) ),
inference(resolution,[],[f16,f77]) ).
fof(f389,plain,
( ~ drinks(english,water)
| ~ drinks(japanese,water) ),
inference(resolution,[],[f16,f78]) ).
fof(f390,plain,
( ~ drinks(spaniard,orange)
| ~ drinks(norwegian,orange) ),
inference(resolution,[],[f17,f77]) ).
fof(f394,plain,
( ~ drinks(spaniard,water)
| ~ drinks(norwegian,water) ),
inference(resolution,[],[f17,f78]) ).
fof(f395,plain,
( ~ spl0_25
| ~ spl0_46 ),
inference(avatar_split_clause,[],[f394,f343,f202]) ).
fof(f397,definition,
( spl0_55
<=> drinks(norwegian,milk) ),
introduced(definition,[new_symbols(definition,[spl0_55])],[avatar_definition]) ).
fof(f401,definition,
( spl0_56
<=> drinks(norwegian,tea) ),
introduced(definition,[new_symbols(definition,[spl0_56])],[avatar_definition]) ).
fof(f405,definition,
( spl0_57
<=> drinks(norwegian,coffee) ),
introduced(definition,[new_symbols(definition,[spl0_57])],[avatar_definition]) ).
fof(f408,plain,
( ~ drinks(spaniard,orange)
| ~ drinks(ukranian,orange) ),
inference(resolution,[],[f18,f77]) ).
fof(f410,plain,
( ~ drinks(spaniard,tea)
| ~ drinks(ukranian,tea) ),
inference(resolution,[],[f18,f76]) ).
fof(f421,plain,
( ~ spl0_24
| ~ spl0_49 ),
inference(avatar_split_clause,[],[f410,f354,f199]) ).
fof(f426,plain,
( $false
| spl0_24 ),
inference(resolution,[],[f200,f94]) ).
fof(f427,plain,
spl0_24,
inference(avatar_contradiction_clause,[],[f426]) ).
fof(f428,plain,
( ~ drinks(spaniard,orange)
| ~ drinks(japanese,orange) ),
inference(resolution,[],[f19,f77]) ).
fof(f429,plain,
( ~ drinks(spaniard,coffee)
| ~ drinks(japanese,coffee) ),
inference(resolution,[],[f19,f80]) ).
fof(f431,plain,
( ~ drinks(spaniard,milk)
| ~ drinks(japanese,milk) ),
inference(resolution,[],[f19,f79]) ).
fof(f434,definition,
( spl0_61
<=> drinks(japanese,water) ),
introduced(definition,[new_symbols(definition,[spl0_61])],[avatar_definition]) ).
fof(f438,definition,
( spl0_62
<=> drinks(japanese,milk) ),
introduced(definition,[new_symbols(definition,[spl0_62])],[avatar_definition]) ).
fof(f440,plain,
( ~ spl0_62
| ~ spl0_48 ),
inference(avatar_split_clause,[],[f431,f350,f438]) ).
fof(f441,plain,
( ~ spl0_23
| ~ spl0_51 ),
inference(avatar_split_clause,[],[f429,f361,f196]) ).
fof(f442,plain,
( ~ drinks(norwegian,orange)
| ~ drinks(ukranian,orange) ),
inference(resolution,[],[f20,f77]) ).
fof(f444,plain,
( ~ drinks(norwegian,tea)
| ~ drinks(ukranian,tea) ),
inference(resolution,[],[f20,f76]) ).
fof(f448,definition,
( spl0_63
<=> drinks(ukranian,orange) ),
introduced(definition,[new_symbols(definition,[spl0_63])],[avatar_definition]) ).
fof(f450,plain,
( ~ spl0_63
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f442,f377,f448]) ).
fof(f451,plain,
( ~ drinks(norwegian,orange)
| ~ drinks(japanese,orange) ),
inference(resolution,[],[f21,f77]) ).
fof(f455,plain,
( ~ drinks(norwegian,water)
| ~ drinks(japanese,water) ),
inference(resolution,[],[f21,f78]) ).
fof(f457,definition,
( spl0_64
<=> drinks(japanese,orange) ),
introduced(definition,[new_symbols(definition,[spl0_64])],[avatar_definition]) ).
fof(f459,plain,
( ~ spl0_64
| ~ spl0_54 ),
inference(avatar_split_clause,[],[f451,f377,f457]) ).
fof(f460,plain,
( ~ drinks(ukranian,orange)
| ~ drinks(japanese,orange) ),
inference(resolution,[],[f22,f77]) ).
fof(f462,plain,
( ~ drinks(ukranian,tea)
| ~ drinks(japanese,tea) ),
inference(resolution,[],[f22,f76]) ).
fof(f466,definition,
( spl0_65
<=> drinks(japanese,tea) ),
introduced(definition,[new_symbols(definition,[spl0_65])],[avatar_definition]) ).
fof(f468,plain,
( ~ spl0_65
| ~ spl0_24 ),
inference(avatar_split_clause,[],[f462,f199,f466]) ).
fof(f469,plain,
( ~ spl0_64
| ~ spl0_63 ),
inference(avatar_split_clause,[],[f460,f448,f457]) ).
fof(f471,plain,
( ~ drives(english,saab)
| ~ drives(spaniard,saab) ),
inference(resolution,[],[f24,f75]) ).
fof(f472,plain,
( ~ drives(english,porsche)
| ~ drives(spaniard,porsche) ),
inference(resolution,[],[f24,f74]) ).
fof(f476,definition,
( spl0_66
<=> drives(spaniard,jaguar) ),
introduced(definition,[new_symbols(definition,[spl0_66])],[avatar_definition]) ).
fof(f479,definition,
( spl0_67
<=> drives(english,jaguar) ),
introduced(definition,[new_symbols(definition,[spl0_67])],[avatar_definition]) ).
fof(f483,definition,
( spl0_68
<=> drives(english,honda) ),
introduced(definition,[new_symbols(definition,[spl0_68])],[avatar_definition]) ).
fof(f487,definition,
( spl0_69
<=> drives(spaniard,porsche) ),
introduced(definition,[new_symbols(definition,[spl0_69])],[avatar_definition]) ).
fof(f489,plain,
( ~ spl0_69
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f472,f163,f487]) ).
fof(f491,definition,
( spl0_70
<=> drives(spaniard,saab) ),
introduced(definition,[new_symbols(definition,[spl0_70])],[avatar_definition]) ).
fof(f494,definition,
( spl0_71
<=> drives(english,saab) ),
introduced(definition,[new_symbols(definition,[spl0_71])],[avatar_definition]) ).
fof(f496,plain,
( ~ spl0_70
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f471,f494,f491]) ).
fof(f498,definition,
( spl0_72
<=> drives(spaniard,masserati) ),
introduced(definition,[new_symbols(definition,[spl0_72])],[avatar_definition]) ).
fof(f501,definition,
( spl0_73
<=> drives(english,masserati) ),
introduced(definition,[new_symbols(definition,[spl0_73])],[avatar_definition]) ).
fof(f505,plain,
( ~ drives(english,saab)
| ~ drives(norwegian,saab) ),
inference(resolution,[],[f25,f75]) ).
fof(f506,plain,
( ~ drives(english,porsche)
| ~ drives(norwegian,porsche) ),
inference(resolution,[],[f25,f74]) ).
fof(f510,definition,
( spl0_74
<=> drives(norwegian,honda) ),
introduced(definition,[new_symbols(definition,[spl0_74])],[avatar_definition]) ).
fof(f514,definition,
( spl0_75
<=> drives(norwegian,saab) ),
introduced(definition,[new_symbols(definition,[spl0_75])],[avatar_definition]) ).
fof(f516,plain,
( ~ spl0_75
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f505,f494,f514]) ).
fof(f518,plain,
( ~ drives(english,saab)
| ~ drives(ukranian,saab) ),
inference(resolution,[],[f26,f75]) ).
fof(f519,plain,
( ~ drives(english,porsche)
| ~ drives(ukranian,porsche) ),
inference(resolution,[],[f26,f74]) ).
fof(f522,plain,
( ~ spl0_14
| ~ spl0_71 ),
inference(avatar_split_clause,[],[f518,f494,f169]) ).
fof(f527,plain,
( ~ drives(english,jaguar)
| ~ drives(japanese,jaguar) ),
inference(resolution,[],[f27,f71]) ).
fof(f533,plain,
( ~ drives(spaniard,saab)
| ~ drives(norwegian,saab) ),
inference(resolution,[],[f28,f75]) ).
fof(f534,plain,
( ~ drives(spaniard,porsche)
| ~ drives(norwegian,porsche) ),
inference(resolution,[],[f28,f74]) ).
fof(f538,definition,
( spl0_77
<=> drives(norwegian,jaguar) ),
introduced(definition,[new_symbols(definition,[spl0_77])],[avatar_definition]) ).
fof(f542,definition,
( spl0_78
<=> drives(norwegian,porsche) ),
introduced(definition,[new_symbols(definition,[spl0_78])],[avatar_definition]) ).
fof(f544,plain,
( ~ spl0_78
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f534,f487,f542]) ).
fof(f547,plain,
( ~ drives(spaniard,saab)
| ~ drives(ukranian,saab) ),
inference(resolution,[],[f29,f75]) ).
fof(f548,plain,
( ~ drives(spaniard,porsche)
| ~ drives(ukranian,porsche) ),
inference(resolution,[],[f29,f74]) ).
fof(f552,definition,
( spl0_79
<=> drives(ukranian,jaguar) ),
introduced(definition,[new_symbols(definition,[spl0_79])],[avatar_definition]) ).
fof(f556,definition,
( spl0_80
<=> drives(ukranian,porsche) ),
introduced(definition,[new_symbols(definition,[spl0_80])],[avatar_definition]) ).
fof(f558,plain,
( ~ spl0_80
| ~ spl0_69 ),
inference(avatar_split_clause,[],[f548,f487,f556]) ).
fof(f560,definition,
( spl0_81
<=> drives(ukranian,masserati) ),
introduced(definition,[new_symbols(definition,[spl0_81])],[avatar_definition]) ).
fof(f567,plain,
( ~ drives(spaniard,jaguar)
| ~ drives(japanese,jaguar) ),
inference(resolution,[],[f30,f71]) ).
fof(f577,plain,
( ~ drives(norwegian,saab)
| ~ drives(ukranian,saab) ),
inference(resolution,[],[f31,f75]) ).
fof(f578,plain,
( ~ drives(norwegian,porsche)
| ~ drives(ukranian,porsche) ),
inference(resolution,[],[f31,f74]) ).
fof(f582,definition,
( spl0_84
<=> drives(ukranian,honda) ),
introduced(definition,[new_symbols(definition,[spl0_84])],[avatar_definition]) ).
fof(f589,plain,
( ~ drives(norwegian,jaguar)
| ~ drives(japanese,jaguar) ),
inference(resolution,[],[f32,f71]) ).
fof(f594,plain,
( ~ drives(ukranian,jaguar)
| ~ drives(japanese,jaguar) ),
inference(resolution,[],[f33,f71]) ).
fof(f595,plain,
( ~ spl0_13
| ~ spl0_79 ),
inference(avatar_split_clause,[],[f594,f552,f166]) ).
fof(f600,plain,
( $false
| spl0_13 ),
inference(resolution,[],[f167,f95]) ).
fof(f601,plain,
spl0_13,
inference(avatar_contradiction_clause,[],[f600]) ).
fof(f602,plain,
( ~ owns(english,dog)
| ~ owns(spaniard,dog) ),
inference(resolution,[],[f35,f81]) ).
fof(f603,plain,
( ~ owns(english,snails)
| ~ owns(spaniard,snails) ),
inference(resolution,[],[f35,f83]) ).
fof(f611,definition,
( spl0_87
<=> owns(english,zebra) ),
introduced(definition,[new_symbols(definition,[spl0_87])],[avatar_definition]) ).
fof(f618,definition,
( spl0_89
<=> owns(english,fox) ),
introduced(definition,[new_symbols(definition,[spl0_89])],[avatar_definition]) ).
fof(f625,definition,
( spl0_91
<=> owns(english,horse) ),
introduced(definition,[new_symbols(definition,[spl0_91])],[avatar_definition]) ).
fof(f629,definition,
( spl0_92
<=> owns(spaniard,snails) ),
introduced(definition,[new_symbols(definition,[spl0_92])],[avatar_definition]) ).
fof(f631,plain,
( ~ spl0_92
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f603,f178,f629]) ).
fof(f633,definition,
( spl0_93
<=> owns(english,dog) ),
introduced(definition,[new_symbols(definition,[spl0_93])],[avatar_definition]) ).
fof(f635,plain,
( ~ spl0_16
| ~ spl0_93 ),
inference(avatar_split_clause,[],[f602,f633,f175]) ).
fof(f636,plain,
( $false
| spl0_16 ),
inference(resolution,[],[f176,f87]) ).
fof(f637,plain,
spl0_16,
inference(avatar_contradiction_clause,[],[f636]) ).
fof(f639,plain,
( ~ owns(english,snails)
| ~ owns(norwegian,snails) ),
inference(resolution,[],[f36,f83]) ).
fof(f641,plain,
( ~ owns(english,fox)
| ~ owns(norwegian,fox) ),
inference(resolution,[],[f36,f85]) ).
fof(f642,plain,
( ~ owns(english,zebra)
| ~ owns(norwegian,zebra) ),
inference(resolution,[],[f36,f82]) ).
fof(f643,plain,
( ~ spl0_20
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f641,f618,f187]) ).
fof(f645,plain,
( ~ owns(english,snails)
| ~ owns(ukranian,snails) ),
inference(resolution,[],[f37,f83]) ).
fof(f650,definition,
( spl0_94
<=> owns(ukranian,fox) ),
introduced(definition,[new_symbols(definition,[spl0_94])],[avatar_definition]) ).
fof(f654,plain,
( ~ owns(english,snails)
| ~ owns(japanese,snails) ),
inference(resolution,[],[f38,f83]) ).
fof(f656,plain,
( ~ owns(english,fox)
| ~ owns(japanese,fox) ),
inference(resolution,[],[f38,f85]) ).
fof(f657,plain,
( ~ owns(english,zebra)
| ~ owns(japanese,zebra) ),
inference(resolution,[],[f38,f82]) ).
fof(f658,plain,
( ~ owns(spaniard,dog)
| ~ owns(norwegian,dog) ),
inference(resolution,[],[f39,f81]) ).
fof(f659,plain,
( ~ owns(spaniard,snails)
| ~ owns(norwegian,snails) ),
inference(resolution,[],[f39,f83]) ).
fof(f664,definition,
( spl0_95
<=> owns(norwegian,zebra) ),
introduced(definition,[new_symbols(definition,[spl0_95])],[avatar_definition]) ).
fof(f668,definition,
( spl0_96
<=> owns(norwegian,horse) ),
introduced(definition,[new_symbols(definition,[spl0_96])],[avatar_definition]) ).
fof(f672,definition,
( spl0_97
<=> owns(norwegian,snails) ),
introduced(definition,[new_symbols(definition,[spl0_97])],[avatar_definition]) ).
fof(f674,plain,
( ~ spl0_97
| ~ spl0_92 ),
inference(avatar_split_clause,[],[f659,f629,f672]) ).
fof(f676,definition,
( spl0_98
<=> owns(norwegian,dog) ),
introduced(definition,[new_symbols(definition,[spl0_98])],[avatar_definition]) ).
fof(f678,plain,
( ~ spl0_98
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f658,f175,f676]) ).
fof(f679,plain,
( ~ owns(spaniard,dog)
| ~ owns(ukranian,dog) ),
inference(resolution,[],[f40,f81]) ).
fof(f686,definition,
( spl0_99
<=> owns(ukranian,snails) ),
introduced(definition,[new_symbols(definition,[spl0_99])],[avatar_definition]) ).
fof(f690,definition,
( spl0_100
<=> owns(ukranian,dog) ),
introduced(definition,[new_symbols(definition,[spl0_100])],[avatar_definition]) ).
fof(f692,plain,
( ~ spl0_100
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f679,f175,f690]) ).
fof(f693,plain,
( ~ owns(spaniard,dog)
| ~ owns(japanese,dog) ),
inference(resolution,[],[f41,f81]) ).
fof(f694,plain,
( ~ owns(spaniard,snails)
| ~ owns(japanese,snails) ),
inference(resolution,[],[f41,f83]) ).
fof(f699,definition,
( spl0_101
<=> owns(japanese,horse) ),
introduced(definition,[new_symbols(definition,[spl0_101])],[avatar_definition]) ).
fof(f703,definition,
( spl0_102
<=> owns(japanese,snails) ),
introduced(definition,[new_symbols(definition,[spl0_102])],[avatar_definition]) ).
fof(f705,plain,
( ~ spl0_102
| ~ spl0_92 ),
inference(avatar_split_clause,[],[f694,f629,f703]) ).
fof(f707,definition,
( spl0_103
<=> owns(japanese,dog) ),
introduced(definition,[new_symbols(definition,[spl0_103])],[avatar_definition]) ).
fof(f709,plain,
( ~ spl0_103
| ~ spl0_16 ),
inference(avatar_split_clause,[],[f693,f175,f707]) ).
fof(f711,plain,
( ~ owns(norwegian,snails)
| ~ owns(ukranian,snails) ),
inference(resolution,[],[f42,f83]) ).
fof(f714,plain,
( ~ owns(norwegian,zebra)
| ~ owns(ukranian,zebra) ),
inference(resolution,[],[f42,f82]) ).
fof(f716,definition,
( spl0_104
<=> owns(ukranian,zebra) ),
introduced(definition,[new_symbols(definition,[spl0_104])],[avatar_definition]) ).
fof(f718,plain,
( ~ spl0_104
| ~ spl0_95 ),
inference(avatar_split_clause,[],[f714,f664,f716]) ).
fof(f722,plain,
( ~ owns(norwegian,fox)
| ~ owns(japanese,fox) ),
inference(resolution,[],[f43,f85]) ).
fof(f723,plain,
( ~ owns(norwegian,zebra)
| ~ owns(japanese,zebra) ),
inference(resolution,[],[f43,f82]) ).
fof(f725,plain,
( ~ owns(ukranian,snails)
| ~ owns(japanese,snails) ),
inference(resolution,[],[f44,f83]) ).
fof(f728,plain,
( ~ owns(ukranian,zebra)
| ~ owns(japanese,zebra) ),
inference(resolution,[],[f44,f82]) ).
fof(f729,plain,
( ~ spl0_18
| ~ spl0_104 ),
inference(avatar_split_clause,[],[f728,f716,f181]) ).
fof(f731,definition,
( spl0_105
<=> owns(japanese,fox) ),
introduced(definition,[new_symbols(definition,[spl0_105])],[avatar_definition]) ).
fof(f734,plain,
( ~ is_color(house_1,red)
| ~ is_color(house_2,red) ),
inference(resolution,[],[f46,f66]) ).
fof(f735,plain,
( ~ is_color(house_1,yellow)
| ~ is_color(house_2,yellow) ),
inference(resolution,[],[f46,f68]) ).
fof(f736,plain,
( ~ is_color(house_1,blue)
| ~ is_color(house_2,blue) ),
inference(resolution,[],[f46,f70]) ).
fof(f743,definition,
( spl0_107
<=> is_color(house_1,ivory) ),
introduced(definition,[new_symbols(definition,[spl0_107])],[avatar_definition]) ).
fof(f747,definition,
( spl0_108
<=> is_color(house_2,green) ),
introduced(definition,[new_symbols(definition,[spl0_108])],[avatar_definition]) ).
fof(f750,definition,
( spl0_109
<=> is_color(house_1,green) ),
introduced(definition,[new_symbols(definition,[spl0_109])],[avatar_definition]) ).
fof(f754,definition,
( spl0_110
<=> is_color(house_1,blue) ),
introduced(definition,[new_symbols(definition,[spl0_110])],[avatar_definition]) ).
fof(f756,plain,
( ~ spl0_4
| ~ spl0_110 ),
inference(avatar_split_clause,[],[f736,f754,f139]) ).
fof(f758,definition,
( spl0_111
<=> is_color(house_2,yellow) ),
introduced(definition,[new_symbols(definition,[spl0_111])],[avatar_definition]) ).
fof(f760,plain,
( ~ spl0_111
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f735,f142,f758]) ).
fof(f762,definition,
( spl0_112
<=> is_color(house_2,red) ),
introduced(definition,[new_symbols(definition,[spl0_112])],[avatar_definition]) ).
fof(f765,definition,
( spl0_113
<=> is_color(house_1,red) ),
introduced(definition,[new_symbols(definition,[spl0_113])],[avatar_definition]) ).
fof(f767,plain,
( ~ spl0_112
| ~ spl0_113 ),
inference(avatar_split_clause,[],[f734,f765,f762]) ).
fof(f768,plain,
( ~ is_color(house_1,red)
| ~ is_color(house_3,red) ),
inference(resolution,[],[f47,f66]) ).
fof(f769,plain,
( ~ is_color(house_1,yellow)
| ~ is_color(house_3,yellow) ),
inference(resolution,[],[f47,f68]) ).
fof(f771,plain,
( ~ is_color(house_1,green)
| ~ is_color(house_3,green) ),
inference(resolution,[],[f47,f67]) ).
fof(f772,plain,
( ~ is_color(house_1,ivory)
| ~ is_color(house_3,ivory) ),
inference(resolution,[],[f47,f69]) ).
fof(f774,definition,
( spl0_114
<=> is_color(house_3,ivory) ),
introduced(definition,[new_symbols(definition,[spl0_114])],[avatar_definition]) ).
fof(f776,plain,
( ~ spl0_114
| ~ spl0_107 ),
inference(avatar_split_clause,[],[f772,f743,f774]) ).
fof(f778,definition,
( spl0_115
<=> is_color(house_3,green) ),
introduced(definition,[new_symbols(definition,[spl0_115])],[avatar_definition]) ).
fof(f780,plain,
( ~ spl0_115
| ~ spl0_109 ),
inference(avatar_split_clause,[],[f771,f750,f778]) ).
fof(f782,definition,
( spl0_116
<=> is_color(house_3,blue) ),
introduced(definition,[new_symbols(definition,[spl0_116])],[avatar_definition]) ).
fof(f786,definition,
( spl0_117
<=> is_color(house_3,yellow) ),
introduced(definition,[new_symbols(definition,[spl0_117])],[avatar_definition]) ).
fof(f788,plain,
( ~ spl0_117
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f769,f142,f786]) ).
fof(f789,plain,
( ~ spl0_3
| ~ spl0_113 ),
inference(avatar_split_clause,[],[f768,f765,f136]) ).
fof(f790,plain,
( ~ is_color(house_1,red)
| ~ is_color(house_4,red) ),
inference(resolution,[],[f48,f66]) ).
fof(f791,plain,
( ~ is_color(house_1,yellow)
| ~ is_color(house_4,yellow) ),
inference(resolution,[],[f48,f68]) ).
fof(f793,plain,
( ~ is_color(house_1,green)
| ~ is_color(house_4,green) ),
inference(resolution,[],[f48,f67]) ).
fof(f794,plain,
( ~ is_color(house_1,ivory)
| ~ is_color(house_4,ivory) ),
inference(resolution,[],[f48,f69]) ).
fof(f796,definition,
( spl0_118
<=> is_color(house_4,blue) ),
introduced(definition,[new_symbols(definition,[spl0_118])],[avatar_definition]) ).
fof(f797,plain,
( ~ is_color(house_4,blue)
| spl0_118 ),
inference(avatar_component_clause,[],[f796]) ).
fof(f799,plain,
( ~ is_color(house_1,red)
| ~ is_color(house_5,red) ),
inference(resolution,[],[f49,f66]) ).
fof(f800,plain,
( ~ is_color(house_1,yellow)
| ~ is_color(house_5,yellow) ),
inference(resolution,[],[f49,f68]) ).
fof(f802,plain,
( ~ is_color(house_1,green)
| ~ is_color(house_5,green) ),
inference(resolution,[],[f49,f67]) ).
fof(f803,plain,
( ~ is_color(house_1,ivory)
| ~ is_color(house_5,ivory) ),
inference(resolution,[],[f49,f69]) ).
fof(f804,plain,
( ~ is_color(house_2,red)
| ~ is_color(house_3,red) ),
inference(resolution,[],[f50,f66]) ).
fof(f806,plain,
( ~ is_color(house_2,blue)
| ~ is_color(house_3,blue) ),
inference(resolution,[],[f50,f70]) ).
fof(f811,plain,
( ~ spl0_3
| ~ spl0_112 ),
inference(avatar_split_clause,[],[f804,f762,f136]) ).
fof(f812,plain,
( ~ is_color(house_2,red)
| ~ is_color(house_4,red) ),
inference(resolution,[],[f51,f66]) ).
fof(f814,plain,
( ~ is_color(house_2,blue)
| ~ is_color(house_4,blue) ),
inference(resolution,[],[f51,f70]) ).
fof(f819,definition,
( spl0_119
<=> is_color(house_4,yellow) ),
introduced(definition,[new_symbols(definition,[spl0_119])],[avatar_definition]) ).
fof(f823,definition,
( spl0_120
<=> is_color(house_4,red) ),
introduced(definition,[new_symbols(definition,[spl0_120])],[avatar_definition]) ).
fof(f825,plain,
( ~ spl0_120
| ~ spl0_112 ),
inference(avatar_split_clause,[],[f812,f762,f823]) ).
fof(f826,plain,
( ~ is_color(house_2,red)
| ~ is_color(house_5,red) ),
inference(resolution,[],[f52,f66]) ).
fof(f828,plain,
( ~ is_color(house_2,blue)
| ~ is_color(house_5,blue) ),
inference(resolution,[],[f52,f70]) ).
fof(f829,plain,
( ~ is_color(house_2,green)
| ~ is_color(house_5,green) ),
inference(resolution,[],[f52,f67]) ).
fof(f832,definition,
( spl0_121
<=> is_color(house_5,ivory) ),
introduced(definition,[new_symbols(definition,[spl0_121])],[avatar_definition]) ).
fof(f836,definition,
( spl0_122
<=> is_color(house_5,yellow) ),
introduced(definition,[new_symbols(definition,[spl0_122])],[avatar_definition]) ).
fof(f840,definition,
( spl0_123
<=> is_color(house_5,red) ),
introduced(definition,[new_symbols(definition,[spl0_123])],[avatar_definition]) ).
fof(f842,plain,
( ~ spl0_123
| ~ spl0_112 ),
inference(avatar_split_clause,[],[f826,f762,f840]) ).
fof(f843,plain,
( ~ is_color(house_3,red)
| ~ is_color(house_4,red) ),
inference(resolution,[],[f53,f66]) ).
fof(f844,plain,
( ~ is_color(house_3,yellow)
| ~ is_color(house_4,yellow) ),
inference(resolution,[],[f53,f68]) ).
fof(f846,plain,
( ~ is_color(house_3,green)
| ~ is_color(house_4,green) ),
inference(resolution,[],[f53,f67]) ).
fof(f847,plain,
( ~ is_color(house_3,ivory)
| ~ is_color(house_4,ivory) ),
inference(resolution,[],[f53,f69]) ).
fof(f849,definition,
( spl0_124
<=> is_color(house_4,green) ),
introduced(definition,[new_symbols(definition,[spl0_124])],[avatar_definition]) ).
fof(f851,plain,
( ~ spl0_124
| ~ spl0_115 ),
inference(avatar_split_clause,[],[f846,f778,f849]) ).
fof(f852,plain,
( ~ is_color(house_3,red)
| ~ is_color(house_5,red) ),
inference(resolution,[],[f54,f66]) ).
fof(f853,plain,
( ~ is_color(house_3,yellow)
| ~ is_color(house_5,yellow) ),
inference(resolution,[],[f54,f68]) ).
fof(f855,plain,
( ~ is_color(house_3,green)
| ~ is_color(house_5,green) ),
inference(resolution,[],[f54,f67]) ).
fof(f856,plain,
( ~ is_color(house_3,ivory)
| ~ is_color(house_5,ivory) ),
inference(resolution,[],[f54,f69]) ).
fof(f857,plain,
( ~ is_color(house_4,red)
| ~ is_color(house_5,red) ),
inference(resolution,[],[f55,f66]) ).
fof(f858,plain,
( ~ is_color(house_4,yellow)
| ~ is_color(house_5,yellow) ),
inference(resolution,[],[f55,f68]) ).
fof(f860,plain,
( ~ is_color(house_4,green)
| ~ is_color(house_5,green) ),
inference(resolution,[],[f55,f67]) ).
fof(f861,plain,
( ~ is_color(house_4,ivory)
| ~ is_color(house_5,ivory) ),
inference(resolution,[],[f55,f69]) ).
fof(f863,definition,
( spl0_125
<=> is_color(house_5,blue) ),
introduced(definition,[new_symbols(definition,[spl0_125])],[avatar_definition]) ).
fof(f867,plain,
( is_color(house_2,red)
| ~ lives(english,house_2) ),
inference(resolution,[],[f86,f62]) ).
fof(f868,plain,
( is_color(house_3,red)
| ~ lives(english,house_3) ),
inference(resolution,[],[f86,f63]) ).
fof(f869,plain,
( is_color(house_4,red)
| ~ lives(english,house_4) ),
inference(resolution,[],[f86,f64]) ).
fof(f870,plain,
( is_color(house_5,red)
| ~ lives(english,house_5) ),
inference(resolution,[],[f86,f65]) ).
fof(f871,plain,
( owns(english,snails)
| ~ drives(english,porsche) ),
inference(resolution,[],[f92,f56]) ).
fof(f872,plain,
( owns(spaniard,snails)
| ~ drives(spaniard,porsche) ),
inference(resolution,[],[f92,f57]) ).
fof(f874,plain,
( owns(ukranian,snails)
| ~ drives(ukranian,porsche) ),
inference(resolution,[],[f92,f59]) ).
fof(f878,plain,
( drinks(english,orange)
| ~ drives(english,honda) ),
inference(resolution,[],[f93,f56]) ).
fof(f879,plain,
( drinks(spaniard,orange)
| ~ drives(spaniard,honda) ),
inference(resolution,[],[f93,f57]) ).
fof(f880,plain,
( drinks(norwegian,orange)
| ~ drives(norwegian,honda) ),
inference(resolution,[],[f93,f58]) ).
fof(f881,plain,
( drinks(ukranian,orange)
| ~ drives(ukranian,honda) ),
inference(resolution,[],[f93,f59]) ).
fof(f884,plain,
( ~ spl0_84
| spl0_63 ),
inference(avatar_split_clause,[],[f881,f448,f582]) ).
fof(f885,plain,
( lives(english,house_3)
| ~ drinks(english,milk) ),
inference(resolution,[],[f99,f56]) ).
fof(f886,plain,
( lives(spaniard,house_3)
| ~ drinks(spaniard,milk) ),
inference(resolution,[],[f99,f57]) ).
fof(f887,plain,
( lives(norwegian,house_3)
| ~ drinks(norwegian,milk) ),
inference(resolution,[],[f99,f58]) ).
fof(f889,plain,
( lives(japanese,house_3)
| ~ drinks(japanese,milk) ),
inference(resolution,[],[f99,f60]) ).
fof(f891,plain,
( ~ spl0_48
| spl0_29 ),
inference(avatar_split_clause,[],[f886,f222,f350]) ).
fof(f894,plain,
! [X0] :
( is_color(X0,yellow)
| ~ drives(english,masserati)
| ~ house(X0)
| ~ lives(english,X0) ),
inference(resolution,[],[f89,f56]) ).
fof(f895,plain,
! [X0] :
( is_color(X0,yellow)
| ~ drives(spaniard,masserati)
| ~ house(X0)
| ~ lives(spaniard,X0) ),
inference(resolution,[],[f89,f57]) ).
fof(f897,plain,
! [X0] :
( is_color(X0,yellow)
| ~ drives(ukranian,masserati)
| ~ house(X0)
| ~ lives(ukranian,X0) ),
inference(resolution,[],[f89,f59]) ).
fof(f900,definition,
( spl0_126
<=> ! [X0] :
( is_color(X0,yellow)
| ~ lives(spaniard,X0)
| ~ house(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_126])],[avatar_definition]) ).
fof(f901,plain,
( ! [X0] :
( ~ house(X0)
| ~ lives(spaniard,X0)
| is_color(X0,yellow) )
| ~ spl0_126 ),
inference(avatar_component_clause,[],[f900]) ).
fof(f902,plain,
( ~ spl0_72
| spl0_126 ),
inference(avatar_split_clause,[],[f895,f900,f498]) ).
fof(f904,plain,
! [X0,X1] :
( is_color(X1,blue)
| ~ lives(norwegian,X0)
| ~ house(X1)
| ~ house(X0)
| ~ left_of(X0,X1) ),
inference(resolution,[],[f91,f100]) ).
fof(f905,plain,
! [X0] :
( is_color(X0,green)
| ~ drinks(english,coffee)
| ~ house(X0)
| ~ lives(english,X0) ),
inference(resolution,[],[f97,f56]) ).
fof(f906,plain,
! [X0] :
( is_color(X0,green)
| ~ drinks(spaniard,coffee)
| ~ house(X0)
| ~ lives(spaniard,X0) ),
inference(resolution,[],[f97,f57]) ).
fof(f907,plain,
! [X0] :
( is_color(X0,green)
| ~ drinks(norwegian,coffee)
| ~ house(X0)
| ~ lives(norwegian,X0) ),
inference(resolution,[],[f97,f58]) ).
fof(f909,plain,
! [X0] :
( is_color(X0,green)
| ~ drinks(japanese,coffee)
| ~ house(X0)
| ~ lives(japanese,X0) ),
inference(resolution,[],[f97,f60]) ).
fof(f911,definition,
( spl0_127
<=> ! [X0] :
( is_color(X0,green)
| ~ lives(spaniard,X0)
| ~ house(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_127])],[avatar_definition]) ).
fof(f912,plain,
( ! [X0] :
( ~ house(X0)
| ~ lives(spaniard,X0)
| is_color(X0,green) )
| ~ spl0_127 ),
inference(avatar_component_clause,[],[f911]) ).
fof(f913,plain,
( ~ spl0_51
| spl0_127 ),
inference(avatar_split_clause,[],[f906,f911,f361]) ).
fof(f916,plain,
( ~ house(house_1)
| ~ is_color(house_1,green)
| ~ house(house_3)
| ~ is_color(house_3,ivory) ),
inference(resolution,[],[f98,f109]) ).
fof(f917,plain,
( ~ house(house_1)
| ~ is_color(house_1,green)
| ~ house(house_4)
| ~ is_color(house_4,ivory) ),
inference(resolution,[],[f98,f110]) ).
fof(f918,plain,
( ~ house(house_1)
| ~ is_color(house_1,green)
| ~ house(house_5)
| ~ is_color(house_5,ivory) ),
inference(resolution,[],[f98,f111]) ).
fof(f920,plain,
( ~ house(house_2)
| ~ is_color(house_2,green)
| ~ house(house_3)
| ~ is_color(house_3,ivory) ),
inference(resolution,[],[f98,f113]) ).
fof(f923,plain,
( ~ house(house_3)
| ~ is_color(house_3,green)
| ~ house(house_1)
| ~ is_color(house_1,ivory) ),
inference(resolution,[],[f98,f116]) ).
fof(f925,plain,
( ~ house(house_3)
| ~ is_color(house_3,green)
| ~ house(house_4)
| ~ is_color(house_4,ivory) ),
inference(resolution,[],[f98,f118]) ).
fof(f926,plain,
( ~ house(house_3)
| ~ is_color(house_3,green)
| ~ house(house_5)
| ~ is_color(house_5,ivory) ),
inference(resolution,[],[f98,f119]) ).
fof(f927,plain,
( ~ house(house_4)
| ~ is_color(house_4,green)
| ~ house(house_1)
| ~ is_color(house_1,ivory) ),
inference(resolution,[],[f98,f120]) ).
fof(f930,plain,
( ~ house(house_4)
| ~ is_color(house_4,green)
| ~ house(house_5)
| ~ is_color(house_5,ivory) ),
inference(resolution,[],[f98,f123]) ).
fof(f931,plain,
( ~ house(house_5)
| ~ is_color(house_5,green)
| ~ house(house_1)
| ~ is_color(house_1,ivory) ),
inference(resolution,[],[f98,f124]) ).
fof(f933,plain,
( ~ house(house_5)
| ~ is_color(house_5,green)
| ~ house(house_3)
| ~ is_color(house_3,ivory) ),
inference(resolution,[],[f98,f126]) ).
fof(f941,definition,
( spl0_128
<=> house(house_5) ),
introduced(definition,[new_symbols(definition,[spl0_128])],[avatar_definition]) ).
fof(f942,plain,
( ~ house(house_5)
| spl0_128 ),
inference(avatar_component_clause,[],[f941]) ).
fof(f944,definition,
( spl0_129
<=> house(house_4) ),
introduced(definition,[new_symbols(definition,[spl0_129])],[avatar_definition]) ).
fof(f945,plain,
( ~ house(house_4)
| spl0_129 ),
inference(avatar_component_clause,[],[f944]) ).
fof(f946,plain,
( ~ spl0_121
| ~ spl0_128
| ~ spl0_124
| ~ spl0_129 ),
inference(avatar_split_clause,[],[f930,f944,f849,f941,f832]) ).
fof(f956,definition,
( spl0_131
<=> house(house_3) ),
introduced(definition,[new_symbols(definition,[spl0_131])],[avatar_definition]) ).
fof(f957,plain,
( ~ house(house_3)
| spl0_131 ),
inference(avatar_component_clause,[],[f956]) ).
fof(f963,definition,
( spl0_133
<=> house(house_2) ),
introduced(definition,[new_symbols(definition,[spl0_133])],[avatar_definition]) ).
fof(f964,plain,
( ~ house(house_2)
| spl0_133 ),
inference(avatar_component_clause,[],[f963]) ).
fof(f970,definition,
( spl0_135
<=> house(house_1) ),
introduced(definition,[new_symbols(definition,[spl0_135])],[avatar_definition]) ).
fof(f971,plain,
( ~ house(house_1)
| spl0_135 ),
inference(avatar_component_clause,[],[f970]) ).
fof(f976,plain,
( $false
| spl0_133 ),
inference(resolution,[],[f964,f62]) ).
fof(f977,plain,
spl0_133,
inference(avatar_contradiction_clause,[],[f976]) ).
fof(f978,plain,
( ~ spl0_125
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f828,f139,f863]) ).
fof(f979,plain,
( $false
| spl0_129 ),
inference(resolution,[],[f945,f64]) ).
fof(f980,plain,
spl0_129,
inference(avatar_contradiction_clause,[],[f979]) ).
fof(f981,plain,
( ~ spl0_118
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f814,f139,f796]) ).
fof(f982,plain,
( $false
| spl0_131 ),
inference(resolution,[],[f957,f63]) ).
fof(f983,plain,
spl0_131,
inference(avatar_contradiction_clause,[],[f982]) ).
fof(f986,plain,
( ~ spl0_116
| ~ spl0_4 ),
inference(avatar_split_clause,[],[f806,f139,f782]) ).
fof(f989,plain,
( $false
| spl0_135 ),
inference(resolution,[],[f971,f61]) ).
fof(f990,plain,
spl0_135,
inference(avatar_contradiction_clause,[],[f989]) ).
fof(f999,plain,
( lives(english,house_1)
| lives(english,house_2)
| lives(english,house_3)
| lives(english,house_4)
| lives(english,house_5) ),
inference(resolution,[],[f1,f56]) ).
fof(f1000,plain,
( lives(spaniard,house_1)
| lives(spaniard,house_2)
| lives(spaniard,house_3)
| lives(spaniard,house_4)
| lives(spaniard,house_5) ),
inference(resolution,[],[f1,f57]) ).
fof(f1002,plain,
( lives(ukranian,house_1)
| lives(ukranian,house_2)
| lives(ukranian,house_3)
| lives(ukranian,house_4)
| lives(ukranian,house_5) ),
inference(resolution,[],[f1,f59]) ).
fof(f1003,plain,
( lives(japanese,house_1)
| lives(japanese,house_2)
| lives(japanese,house_3)
| lives(japanese,house_4)
| lives(japanese,house_5) ),
inference(resolution,[],[f1,f60]) ).
fof(f1009,plain,
( spl0_8
| spl0_45
| spl0_41
| spl0_36
| spl0_44 ),
inference(avatar_split_clause,[],[f1003,f324,f264,f302,f334,f151]) ).
fof(f1015,plain,
( spl0_39
| spl0_42
| spl0_40
| spl0_9
| spl0_43 ),
inference(avatar_split_clause,[],[f1002,f315,f154,f293,f311,f289]) ).
fof(f1020,plain,
( spl0_26
| spl0_6
| spl0_29
| spl0_30
| spl0_32 ),
inference(avatar_split_clause,[],[f1000,f233,f226,f222,f145,f211]) ).
fof(f1026,plain,
( spl0_27
| spl0_28
| spl0_7
| spl0_31
| spl0_33 ),
inference(avatar_split_clause,[],[f999,f236,f229,f148,f218,f214]) ).
fof(f1027,plain,
( ~ spl0_36
| ~ spl0_9 ),
inference(avatar_split_clause,[],[f328,f154,f264]) ).
fof(f1028,plain,
( ~ spl0_41
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f260,f148,f302]) ).
fof(f1030,plain,
( ~ spl0_7
| spl0_3 ),
inference(avatar_split_clause,[],[f868,f136,f148]) ).
fof(f1031,plain,
( ~ spl0_42
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f286,f145,f311]) ).
fof(f1032,plain,
( ~ spl0_39
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f256,f214,f289]) ).
fof(f1033,plain,
( ~ spl0_8
| ~ spl0_27 ),
inference(avatar_split_clause,[],[f262,f214,f151]) ).
fof(f1035,plain,
( ~ spl0_27
| spl0_123 ),
inference(avatar_split_clause,[],[f870,f840,f214]) ).
fof(f1038,plain,
( ~ spl0_28
| spl0_120 ),
inference(avatar_split_clause,[],[f869,f823,f218]) ).
fof(f1039,plain,
( ~ spl0_8
| ~ spl0_26 ),
inference(avatar_split_clause,[],[f300,f211,f151]) ).
fof(f1040,plain,
( ~ spl0_10
| ~ spl0_33 ),
inference(avatar_split_clause,[],[f239,f236,f157]) ).
fof(f1047,plain,
( ! [X0] :
( ~ lives(norwegian,X0)
| ~ house(house_4)
| ~ house(X0)
| ~ left_of(X0,house_4) )
| spl0_118 ),
inference(resolution,[],[f904,f797]) ).
fof(f1049,definition,
( spl0_137
<=> ! [X0] :
( ~ lives(norwegian,X0)
| ~ left_of(X0,house_4)
| ~ house(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_137])],[avatar_definition]) ).
fof(f1050,plain,
( ! [X0] :
( ~ house(X0)
| ~ left_of(X0,house_4)
| ~ lives(norwegian,X0) )
| ~ spl0_137 ),
inference(avatar_component_clause,[],[f1049]) ).
fof(f1051,plain,
( ~ spl0_129
| spl0_137
| spl0_118 ),
inference(avatar_split_clause,[],[f1047,f796,f1049,f944]) ).
fof(f1057,definition,
( spl0_139
<=> ! [X0] :
( ~ lives(norwegian,X0)
| ~ left_of(X0,house_2)
| ~ house(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_139])],[avatar_definition]) ).
fof(f1058,plain,
( ! [X0] :
( ~ house(X0)
| ~ left_of(X0,house_2)
| ~ lives(norwegian,X0) )
| ~ spl0_139 ),
inference(avatar_component_clause,[],[f1057]) ).
fof(f1067,plain,
( ! [X0] :
( ~ lives(norwegian,X0)
| ~ house(house_2)
| ~ house(X0)
| ~ left_of(X0,house_2) )
| spl0_4 ),
inference(resolution,[],[f140,f904]) ).
fof(f1069,plain,
( ~ spl0_133
| spl0_139
| spl0_4 ),
inference(avatar_split_clause,[],[f1067,f139,f1057,f963]) ).
fof(f1080,plain,
( ~ left_of(house_1,house_2)
| ~ lives(norwegian,house_1)
| ~ spl0_139 ),
inference(resolution,[],[f1058,f61]) ).
fof(f1086,definition,
( spl0_143
<=> left_of(house_1,house_2) ),
introduced(definition,[new_symbols(definition,[spl0_143])],[avatar_definition]) ).
fof(f1087,plain,
( ~ left_of(house_1,house_2)
| spl0_143 ),
inference(avatar_component_clause,[],[f1086]) ).
fof(f1088,plain,
( ~ spl0_10
| ~ spl0_143
| ~ spl0_139 ),
inference(avatar_split_clause,[],[f1080,f1057,f1086,f157]) ).
fof(f1089,plain,
( $false
| spl0_128 ),
inference(resolution,[],[f942,f65]) ).
fof(f1090,plain,
spl0_128,
inference(avatar_contradiction_clause,[],[f1089]) ).
fof(f1091,plain,
( $false
| spl0_143 ),
inference(resolution,[],[f1087,f103]) ).
fof(f1093,plain,
spl0_143,
inference(avatar_contradiction_clause,[],[f1091]) ).
fof(f1119,plain,
( ~ left_of(house_3,house_4)
| ~ lives(norwegian,house_3)
| ~ spl0_137 ),
inference(resolution,[],[f1050,f63]) ).
fof(f1142,plain,
( drinks(english,orange)
| drinks(english,coffee)
| drinks(english,tea)
| drinks(english,milk)
| drinks(english,water) ),
inference(resolution,[],[f12,f56]) ).
fof(f1143,plain,
( drinks(spaniard,orange)
| drinks(spaniard,coffee)
| drinks(spaniard,tea)
| drinks(spaniard,milk)
| drinks(spaniard,water) ),
inference(resolution,[],[f12,f57]) ).
fof(f1144,plain,
( drinks(norwegian,orange)
| drinks(norwegian,coffee)
| drinks(norwegian,tea)
| drinks(norwegian,milk)
| drinks(norwegian,water) ),
inference(resolution,[],[f12,f58]) ).
fof(f1146,plain,
( drinks(japanese,orange)
| drinks(japanese,coffee)
| drinks(japanese,tea)
| drinks(japanese,milk)
| drinks(japanese,water) ),
inference(resolution,[],[f12,f60]) ).
fof(f1152,plain,
( spl0_61
| spl0_62
| spl0_65
| spl0_23
| spl0_64 ),
inference(avatar_split_clause,[],[f1146,f457,f196,f466,f438,f434]) ).
fof(f1158,plain,
( spl0_25
| spl0_55
| spl0_56
| spl0_57
| spl0_54 ),
inference(avatar_split_clause,[],[f1144,f377,f405,f401,f397,f202]) ).
fof(f1164,plain,
( spl0_46
| spl0_48
| spl0_49
| spl0_51
| spl0_21 ),
inference(avatar_split_clause,[],[f1143,f190,f361,f354,f350,f343]) ).
fof(f1170,plain,
( spl0_47
| spl0_22
| spl0_50
| spl0_52
| spl0_53 ),
inference(avatar_split_clause,[],[f1142,f368,f364,f357,f193,f346]) ).
fof(f1172,definition,
( spl0_144
<=> ! [X0] :
( is_color(X0,green)
| ~ lives(japanese,X0)
| ~ house(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_144])],[avatar_definition]) ).
fof(f1173,plain,
( ! [X0] :
( ~ house(X0)
| ~ lives(japanese,X0)
| is_color(X0,green) )
| ~ spl0_144 ),
inference(avatar_component_clause,[],[f1172]) ).
fof(f1174,plain,
( ~ spl0_23
| spl0_144 ),
inference(avatar_split_clause,[],[f909,f1172,f196]) ).
fof(f1175,plain,
( ~ spl0_64
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f428,f190,f457]) ).
fof(f1176,plain,
( ~ spl0_61
| ~ spl0_25 ),
inference(avatar_split_clause,[],[f455,f202,f434]) ).
fof(f1177,plain,
( ~ spl0_54
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f390,f190,f377]) ).
fof(f1178,plain,
( ~ spl0_25
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f375,f346,f202]) ).
fof(f1179,plain,
( ~ spl0_61
| ~ spl0_47 ),
inference(avatar_split_clause,[],[f389,f346,f434]) ).
fof(f1181,plain,
( ~ spl0_31
| spl0_112 ),
inference(avatar_split_clause,[],[f867,f762,f229]) ).
fof(f1182,plain,
( ~ spl0_22
| spl0_7 ),
inference(avatar_split_clause,[],[f885,f148,f193]) ).
fof(f1184,plain,
( ~ spl0_55
| spl0_38 ),
inference(avatar_split_clause,[],[f887,f277,f397]) ).
fof(f1186,plain,
( ~ spl0_24
| ~ spl0_50 ),
inference(avatar_split_clause,[],[f382,f357,f199]) ).
fof(f1187,plain,
( ~ spl0_45
| ~ spl0_6 ),
inference(avatar_split_clause,[],[f299,f145,f334]) ).
fof(f1190,definition,
( spl0_145
<=> ! [X0] :
( is_color(X0,green)
| ~ lives(english,X0)
| ~ house(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_145])],[avatar_definition]) ).
fof(f1191,plain,
( ! [X0] :
( ~ house(X0)
| ~ lives(english,X0)
| is_color(X0,green) )
| ~ spl0_145 ),
inference(avatar_component_clause,[],[f1190]) ).
fof(f1192,plain,
( ~ spl0_52
| spl0_145 ),
inference(avatar_split_clause,[],[f905,f1190,f364]) ).
fof(f1199,definition,
( spl0_147
<=> left_of(house_3,house_4) ),
introduced(definition,[new_symbols(definition,[spl0_147])],[avatar_definition]) ).
fof(f1200,plain,
( ~ left_of(house_3,house_4)
| spl0_147 ),
inference(avatar_component_clause,[],[f1199]) ).
fof(f1201,plain,
( ~ spl0_38
| ~ spl0_147
| ~ spl0_137 ),
inference(avatar_split_clause,[],[f1119,f1049,f1199,f277]) ).
fof(f1202,plain,
( ~ spl0_24
| ~ spl0_56 ),
inference(avatar_split_clause,[],[f444,f401,f199]) ).
fof(f1204,plain,
( drives(english,masserati)
| drives(english,saab)
| drives(english,porsche)
| drives(english,honda)
| drives(english,jaguar) ),
inference(resolution,[],[f23,f56]) ).
fof(f1205,plain,
( drives(spaniard,masserati)
| drives(spaniard,saab)
| drives(spaniard,porsche)
| drives(spaniard,honda)
| drives(spaniard,jaguar) ),
inference(resolution,[],[f23,f57]) ).
fof(f1206,plain,
( drives(norwegian,masserati)
| drives(norwegian,saab)
| drives(norwegian,porsche)
| drives(norwegian,honda)
| drives(norwegian,jaguar) ),
inference(resolution,[],[f23,f58]) ).
fof(f1207,plain,
( drives(ukranian,masserati)
| drives(ukranian,saab)
| drives(ukranian,porsche)
| drives(ukranian,honda)
| drives(ukranian,jaguar) ),
inference(resolution,[],[f23,f59]) ).
fof(f1214,plain,
( spl0_79
| spl0_84
| spl0_80
| spl0_14
| spl0_81 ),
inference(avatar_split_clause,[],[f1207,f560,f169,f556,f582,f552]) ).
fof(f1220,plain,
( spl0_77
| spl0_74
| spl0_78
| spl0_75
| spl0_15 ),
inference(avatar_split_clause,[],[f1206,f172,f514,f542,f510,f538]) ).
fof(f1226,plain,
( spl0_66
| spl0_11
| spl0_69
| spl0_70
| spl0_72 ),
inference(avatar_split_clause,[],[f1205,f498,f491,f487,f160,f476]) ).
fof(f1232,plain,
( spl0_67
| spl0_68
| spl0_12
| spl0_71
| spl0_73 ),
inference(avatar_split_clause,[],[f1204,f501,f494,f163,f483,f479]) ).
fof(f1239,plain,
( ~ spl0_12
| spl0_17 ),
inference(avatar_split_clause,[],[f871,f178,f163]) ).
fof(f1240,plain,
( ~ spl0_74
| spl0_54 ),
inference(avatar_split_clause,[],[f880,f377,f510]) ).
fof(f1242,plain,
( ~ spl0_14
| ~ spl0_75 ),
inference(avatar_split_clause,[],[f577,f514,f169]) ).
fof(f1245,plain,
( ~ spl0_80
| spl0_99 ),
inference(avatar_split_clause,[],[f874,f686,f556]) ).
fof(f1246,plain,
( ~ spl0_80
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f519,f163,f556]) ).
fof(f1248,plain,
( ~ spl0_63
| ~ spl0_21 ),
inference(avatar_split_clause,[],[f408,f190,f448]) ).
fof(f1249,plain,
( ~ spl0_75
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f533,f491,f514]) ).
fof(f1250,plain,
( ~ spl0_14
| ~ spl0_70 ),
inference(avatar_split_clause,[],[f547,f491,f169]) ).
fof(f1254,definition,
( spl0_149
<=> ! [X0] :
( is_color(X0,green)
| ~ lives(norwegian,X0)
| ~ house(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_149])],[avatar_definition]) ).
fof(f1255,plain,
( ! [X0] :
( ~ house(X0)
| ~ lives(norwegian,X0)
| is_color(X0,green) )
| ~ spl0_149 ),
inference(avatar_component_clause,[],[f1254]) ).
fof(f1256,plain,
( ~ spl0_57
| spl0_149 ),
inference(avatar_split_clause,[],[f907,f1254,f405]) ).
fof(f1258,plain,
( ~ spl0_11
| spl0_21 ),
inference(avatar_split_clause,[],[f879,f190,f160]) ).
fof(f1259,plain,
( ~ spl0_63
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f380,f368,f448]) ).
fof(f1260,plain,
( ~ spl0_64
| ~ spl0_53 ),
inference(avatar_split_clause,[],[f385,f368,f457]) ).
fof(f1263,definition,
( spl0_150
<=> ! [X0] :
( is_color(X0,yellow)
| ~ lives(ukranian,X0)
| ~ house(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_150])],[avatar_definition]) ).
fof(f1264,plain,
( ! [X0] :
( ~ house(X0)
| ~ lives(ukranian,X0)
| is_color(X0,yellow) )
| ~ spl0_150 ),
inference(avatar_component_clause,[],[f1263]) ).
fof(f1265,plain,
( ~ spl0_81
| spl0_150 ),
inference(avatar_split_clause,[],[f897,f1263,f560]) ).
fof(f1268,plain,
( ~ spl0_69
| spl0_92 ),
inference(avatar_split_clause,[],[f872,f629,f487]) ).
fof(f1270,plain,
( ~ spl0_68
| spl0_53 ),
inference(avatar_split_clause,[],[f878,f368,f483]) ).
fof(f1271,plain,
( ~ spl0_62
| spl0_41 ),
inference(avatar_split_clause,[],[f889,f302,f438]) ).
fof(f1277,definition,
( spl0_151
<=> ! [X0] :
( is_color(X0,yellow)
| ~ lives(english,X0)
| ~ house(X0) ) ),
introduced(definition,[new_symbols(definition,[spl0_151])],[avatar_definition]) ).
fof(f1278,plain,
( ! [X0] :
( ~ house(X0)
| ~ lives(english,X0)
| is_color(X0,yellow) )
| ~ spl0_151 ),
inference(avatar_component_clause,[],[f1277]) ).
fof(f1279,plain,
( ~ spl0_73
| spl0_151 ),
inference(avatar_split_clause,[],[f894,f1277,f501]) ).
fof(f1280,plain,
( ~ spl0_13
| ~ spl0_67 ),
inference(avatar_split_clause,[],[f527,f479,f166]) ).
fof(f1281,plain,
( ~ spl0_13
| ~ spl0_77 ),
inference(avatar_split_clause,[],[f589,f538,f166]) ).
fof(f1283,plain,
( ~ spl0_80
| ~ spl0_78 ),
inference(avatar_split_clause,[],[f578,f542,f556]) ).
fof(f1286,plain,
( ~ spl0_78
| ~ spl0_12 ),
inference(avatar_split_clause,[],[f506,f163,f542]) ).
fof(f1287,plain,
( ~ spl0_13
| ~ spl0_66 ),
inference(avatar_split_clause,[],[f567,f476,f166]) ).
fof(f1288,plain,
( ~ spl0_99
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f645,f178,f686]) ).
fof(f1289,plain,
( ~ spl0_99
| ~ spl0_97 ),
inference(avatar_split_clause,[],[f711,f672,f686]) ).
fof(f1290,plain,
( ~ spl0_97
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f639,f178,f672]) ).
fof(f1294,plain,
( owns(english,dog)
| owns(english,snails)
| owns(english,horse)
| owns(english,fox)
| owns(english,zebra) ),
inference(resolution,[],[f34,f56]) ).
fof(f1296,plain,
( owns(norwegian,dog)
| owns(norwegian,snails)
| owns(norwegian,horse)
| owns(norwegian,fox)
| owns(norwegian,zebra) ),
inference(resolution,[],[f34,f58]) ).
fof(f1297,plain,
( owns(ukranian,dog)
| owns(ukranian,snails)
| owns(ukranian,horse)
| owns(ukranian,fox)
| owns(ukranian,zebra) ),
inference(resolution,[],[f34,f59]) ).
fof(f1298,plain,
( owns(japanese,dog)
| owns(japanese,snails)
| owns(japanese,horse)
| owns(japanese,fox)
| owns(japanese,zebra) ),
inference(resolution,[],[f34,f60]) ).
fof(f1303,plain,
( spl0_18
| spl0_105
| spl0_101
| spl0_102
| spl0_103 ),
inference(avatar_split_clause,[],[f1298,f707,f703,f699,f731,f181]) ).
fof(f1308,plain,
( spl0_104
| spl0_94
| spl0_19
| spl0_99
| spl0_100 ),
inference(avatar_split_clause,[],[f1297,f690,f686,f184,f650,f716]) ).
fof(f1313,plain,
( spl0_95
| spl0_20
| spl0_96
| spl0_97
| spl0_98 ),
inference(avatar_split_clause,[],[f1296,f676,f672,f668,f187,f664]) ).
fof(f1316,plain,
( is_color(house_1,red)
| is_color(house_1,yellow)
| is_color(house_1,blue)
| is_color(house_1,green)
| is_color(house_1,ivory) ),
inference(resolution,[],[f45,f61]) ).
fof(f1318,plain,
( is_color(house_3,red)
| is_color(house_3,yellow)
| is_color(house_3,blue)
| is_color(house_3,green)
| is_color(house_3,ivory) ),
inference(resolution,[],[f45,f63]) ).
fof(f1319,plain,
( is_color(house_4,red)
| is_color(house_4,yellow)
| is_color(house_4,blue)
| is_color(house_4,green)
| is_color(house_4,ivory) ),
inference(resolution,[],[f45,f64]) ).
fof(f1320,plain,
( is_color(house_5,red)
| is_color(house_5,yellow)
| is_color(house_5,blue)
| is_color(house_5,green)
| is_color(house_5,ivory) ),
inference(resolution,[],[f45,f65]) ).
fof(f1325,plain,
( spl0_121
| spl0_1
| spl0_125
| spl0_122
| spl0_123 ),
inference(avatar_split_clause,[],[f1320,f840,f836,f863,f130,f832]) ).
fof(f1330,plain,
( spl0_2
| spl0_124
| spl0_118
| spl0_119
| spl0_120 ),
inference(avatar_split_clause,[],[f1319,f823,f819,f796,f849,f133]) ).
fof(f1340,plain,
( spl0_107
| spl0_109
| spl0_110
| spl0_5
| spl0_113 ),
inference(avatar_split_clause,[],[f1316,f765,f142,f754,f750,f743]) ).
fof(f1341,plain,
( ~ spl0_1
| ~ spl0_124 ),
inference(avatar_split_clause,[],[f860,f849,f130]) ).
fof(f1342,plain,
( ~ spl0_120
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f843,f136,f823]) ).
fof(f1343,plain,
( ~ spl0_119
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f791,f142,f819]) ).
fof(f1346,plain,
! [X2,X3,X0,X1] :
( left_of(X3,X1)
| ~ owns(X0,fox)
| ~ house(X1)
| ~ lives(X0,X1)
| ~ person(X2)
| ~ drives(X2,saab)
| ~ house(X3)
| ~ lives(X2,X3)
| left_of(X1,X3)
| ~ person(X0) ),
inference(resolution,[],[f90,f102]) ).
fof(f1356,plain,
! [X2,X3,X0,X1] :
( left_of(X3,X1)
| ~ drives(X0,masserati)
| ~ house(X1)
| ~ lives(X0,X1)
| ~ person(X2)
| ~ owns(X2,horse)
| ~ house(X3)
| ~ lives(X2,X3)
| left_of(X1,X3)
| ~ person(X0) ),
inference(resolution,[],[f96,f102]) ).
fof(f1366,plain,
( ~ lives(spaniard,house_2)
| is_color(house_2,yellow)
| ~ spl0_126 ),
inference(resolution,[],[f901,f62]) ).
fof(f1367,plain,
( ~ lives(spaniard,house_3)
| is_color(house_3,yellow)
| ~ spl0_126 ),
inference(resolution,[],[f901,f63]) ).
fof(f1368,plain,
( ~ lives(spaniard,house_4)
| is_color(house_4,yellow)
| ~ spl0_126 ),
inference(resolution,[],[f901,f64]) ).
fof(f1369,plain,
( ~ lives(spaniard,house_5)
| is_color(house_5,yellow)
| ~ spl0_126 ),
inference(resolution,[],[f901,f65]) ).
fof(f1370,plain,
( spl0_119
| ~ spl0_6
| ~ spl0_126 ),
inference(avatar_split_clause,[],[f1368,f900,f145,f819]) ).
fof(f1371,plain,
( $false
| spl0_147 ),
inference(resolution,[],[f1200,f105]) ).
fof(f1373,plain,
spl0_147,
inference(avatar_contradiction_clause,[],[f1371]) ).
fof(f1375,plain,
( ~ lives(spaniard,house_2)
| is_color(house_2,green)
| ~ spl0_127 ),
inference(resolution,[],[f912,f62]) ).
fof(f1376,plain,
( ~ lives(spaniard,house_3)
| is_color(house_3,green)
| ~ spl0_127 ),
inference(resolution,[],[f912,f63]) ).
fof(f1377,plain,
( ~ lives(spaniard,house_4)
| is_color(house_4,green)
| ~ spl0_127 ),
inference(resolution,[],[f912,f64]) ).
fof(f1380,plain,
( ~ spl0_122
| ~ spl0_5 ),
inference(avatar_split_clause,[],[f800,f142,f836]) ).
fof(f1381,plain,
( ~ spl0_123
| ~ spl0_3 ),
inference(avatar_split_clause,[],[f852,f136,f840]) ).
fof(f1382,plain,
( ~ spl0_124
| ~ spl0_109 ),
inference(avatar_split_clause,[],[f793,f750,f849]) ).
fof(f1383,plain,
( ~ spl0_1
| ~ spl0_109 ),
inference(avatar_split_clause,[],[f802,f750,f130]) ).
fof(f1384,plain,
( ~ spl0_2
| ~ spl0_129
| ~ spl0_109
| ~ spl0_135 ),
inference(avatar_split_clause,[],[f917,f970,f750,f944,f133]) ).
fof(f1385,plain,
( ~ spl0_2
| ~ spl0_107 ),
inference(avatar_split_clause,[],[f794,f743,f133]) ).
fof(f1386,plain,
( ~ spl0_107
| ~ spl0_135
| ~ spl0_124
| ~ spl0_129 ),
inference(avatar_split_clause,[],[f927,f944,f849,f970,f743]) ).
fof(f1387,plain,
( ~ spl0_107
| ~ spl0_135
| ~ spl0_1
| ~ spl0_128 ),
inference(avatar_split_clause,[],[f931,f941,f130,f970,f743]) ).
fof(f1391,plain,
( ~ spl0_40
| ~ spl0_7 ),
inference(avatar_split_clause,[],[f254,f148,f293]) ).
fof(f1395,plain,
! [X0,X1] :
( ~ owns(X0,fox)
| ~ house(house_1)
| ~ lives(X0,house_1)
| ~ person(X1)
| ~ drives(X1,saab)
| ~ house(house_3)
| ~ lives(X1,house_3)
| left_of(house_1,house_3)
| ~ person(X0) ),
inference(resolution,[],[f1346,f109]) ).
fof(f1396,plain,
! [X0,X1] :
( ~ owns(X0,fox)
| ~ house(house_1)
| ~ lives(X0,house_1)
| ~ person(X1)
| ~ drives(X1,saab)
| ~ house(house_4)
| ~ lives(X1,house_4)
| left_of(house_1,house_4)
| ~ person(X0) ),
inference(resolution,[],[f1346,f110]) ).
fof(f1398,plain,
! [X0,X1] :
( ~ owns(X0,fox)
| ~ house(house_2)
| ~ lives(X0,house_2)
| ~ person(X1)
| ~ drives(X1,saab)
| ~ house(house_2)
| ~ lives(X1,house_2)
| left_of(house_2,house_2)
| ~ person(X0) ),
inference(resolution,[],[f1346,f112]) ).
fof(f1408,plain,
! [X0,X1] :
( ~ owns(X0,fox)
| ~ house(house_4)
| ~ lives(X0,house_4)
| ~ person(X1)
| ~ drives(X1,saab)
| ~ house(house_4)
| ~ lives(X1,house_4)
| left_of(house_4,house_4)
| ~ person(X0) ),
inference(resolution,[],[f1346,f122]) ).
fof(f1411,plain,
! [X0,X1] :
( ~ owns(X0,fox)
| ~ house(house_5)
| ~ lives(X0,house_5)
| ~ person(X1)
| ~ drives(X1,saab)
| ~ house(house_2)
| ~ lives(X1,house_2)
| left_of(house_5,house_2)
| ~ person(X0) ),
inference(resolution,[],[f1346,f125]) ).
fof(f1412,plain,
! [X0,X1] :
( ~ owns(X0,fox)
| ~ house(house_5)
| ~ lives(X0,house_5)
| ~ person(X1)
| ~ drives(X1,saab)
| ~ house(house_3)
| ~ lives(X1,house_3)
| left_of(house_5,house_3)
| ~ person(X0) ),
inference(resolution,[],[f1346,f126]) ).
fof(f1415,plain,
! [X0,X1] :
( ~ owns(X0,fox)
| ~ house(house_4)
| ~ lives(X0,house_4)
| ~ person(X1)
| ~ drives(X1,saab)
| ~ lives(X1,house_4)
| left_of(house_4,house_4)
| ~ person(X0) ),
inference(duplicate_literal_removal,[],[f1408]) ).
fof(f1417,plain,
! [X0,X1] :
( ~ owns(X0,fox)
| ~ house(house_2)
| ~ lives(X0,house_2)
| ~ person(X1)
| ~ drives(X1,saab)
| ~ lives(X1,house_2)
| left_of(house_2,house_2)
| ~ person(X0) ),
inference(duplicate_literal_removal,[],[f1398]) ).
fof(f1426,definition,
( spl0_158
<=> ! [X0] :
( ~ owns(X0,fox)
| ~ person(X0)
| ~ lives(X0,house_5) ) ),
introduced(definition,[new_symbols(definition,[spl0_158])],[avatar_definition]) ).
fof(f1427,plain,
( ! [X0] :
( ~ person(X0)
| ~ owns(X0,fox)
| ~ lives(X0,house_5) )
| ~ spl0_158 ),
inference(avatar_component_clause,[],[f1426]) ).
fof(f1430,definition,
( spl0_159
<=> left_of(house_5,house_3) ),
introduced(definition,[new_symbols(definition,[spl0_159])],[avatar_definition]) ).
fof(f1431,plain,
( left_of(house_5,house_3)
| ~ spl0_159 ),
inference(avatar_component_clause,[],[f1430]) ).
fof(f1433,definition,
( spl0_160
<=> ! [X1] :
( ~ person(X1)
| ~ lives(X1,house_3)
| ~ drives(X1,saab) ) ),
introduced(definition,[new_symbols(definition,[spl0_160])],[avatar_definition]) ).
fof(f1434,plain,
( ! [X1] :
( ~ person(X1)
| ~ lives(X1,house_3)
| ~ drives(X1,saab) )
| ~ spl0_160 ),
inference(avatar_component_clause,[],[f1433]) ).
fof(f1435,plain,
( spl0_159
| ~ spl0_131
| spl0_160
| ~ spl0_128
| spl0_158 ),
inference(avatar_split_clause,[],[f1412,f1426,f941,f1433,f956,f1430]) ).
fof(f1437,definition,
( spl0_161
<=> left_of(house_5,house_2) ),
introduced(definition,[new_symbols(definition,[spl0_161])],[avatar_definition]) ).
fof(f1438,plain,
( left_of(house_5,house_2)
| ~ spl0_161 ),
inference(avatar_component_clause,[],[f1437]) ).
fof(f1440,definition,
( spl0_162
<=> ! [X1] :
( ~ person(X1)
| ~ lives(X1,house_2)
| ~ drives(X1,saab) ) ),
introduced(definition,[new_symbols(definition,[spl0_162])],[avatar_definition]) ).
fof(f1441,plain,
( ! [X1] :
( ~ person(X1)
| ~ lives(X1,house_2)
| ~ drives(X1,saab) )
| ~ spl0_162 ),
inference(avatar_component_clause,[],[f1440]) ).
fof(f1442,plain,
( spl0_161
| ~ spl0_133
| spl0_162
| ~ spl0_128
| spl0_158 ),
inference(avatar_split_clause,[],[f1411,f1426,f941,f1440,f963,f1437]) ).
fof(f1451,definition,
( spl0_165
<=> left_of(house_4,house_4) ),
introduced(definition,[new_symbols(definition,[spl0_165])],[avatar_definition]) ).
fof(f1452,plain,
( left_of(house_4,house_4)
| ~ spl0_165 ),
inference(avatar_component_clause,[],[f1451]) ).
fof(f1454,definition,
( spl0_166
<=> ! [X1] :
( ~ person(X1)
| ~ lives(X1,house_4)
| ~ drives(X1,saab) ) ),
introduced(definition,[new_symbols(definition,[spl0_166])],[avatar_definition]) ).
fof(f1455,plain,
( ! [X1] :
( ~ person(X1)
| ~ lives(X1,house_4)
| ~ drives(X1,saab) )
| ~ spl0_166 ),
inference(avatar_component_clause,[],[f1454]) ).
fof(f1457,definition,
( spl0_167
<=> ! [X0] :
( ~ owns(X0,fox)
| ~ person(X0)
| ~ lives(X0,house_4) ) ),
introduced(definition,[new_symbols(definition,[spl0_167])],[avatar_definition]) ).
fof(f1458,plain,
( ! [X0] :
( ~ person(X0)
| ~ owns(X0,fox)
| ~ lives(X0,house_4) )
| ~ spl0_167 ),
inference(avatar_component_clause,[],[f1457]) ).
fof(f1459,plain,
( spl0_165
| spl0_166
| ~ spl0_129
| spl0_167 ),
inference(avatar_split_clause,[],[f1415,f1457,f944,f1454,f1451]) ).
fof(f1487,definition,
( spl0_175
<=> ! [X0] :
( ~ owns(X0,fox)
| ~ person(X0)
| ~ lives(X0,house_2) ) ),
introduced(definition,[new_symbols(definition,[spl0_175])],[avatar_definition]) ).
fof(f1488,plain,
( ! [X0] :
( ~ person(X0)
| ~ owns(X0,fox)
| ~ lives(X0,house_2) )
| ~ spl0_175 ),
inference(avatar_component_clause,[],[f1487]) ).
fof(f1495,definition,
( spl0_177
<=> left_of(house_2,house_2) ),
introduced(definition,[new_symbols(definition,[spl0_177])],[avatar_definition]) ).
fof(f1496,plain,
( left_of(house_2,house_2)
| ~ spl0_177 ),
inference(avatar_component_clause,[],[f1495]) ).
fof(f1497,plain,
( spl0_177
| spl0_162
| ~ spl0_133
| spl0_175 ),
inference(avatar_split_clause,[],[f1417,f1487,f963,f1440,f1495]) ).
fof(f1499,definition,
( spl0_178
<=> left_of(house_1,house_5) ),
introduced(definition,[new_symbols(definition,[spl0_178])],[avatar_definition]) ).
fof(f1500,plain,
( left_of(house_1,house_5)
| ~ spl0_178 ),
inference(avatar_component_clause,[],[f1499]) ).
fof(f1502,definition,
( spl0_179
<=> ! [X0] :
( ~ owns(X0,fox)
| ~ person(X0)
| ~ lives(X0,house_1) ) ),
introduced(definition,[new_symbols(definition,[spl0_179])],[avatar_definition]) ).
fof(f1503,plain,
( ! [X0] :
( ~ person(X0)
| ~ owns(X0,fox)
| ~ lives(X0,house_1) )
| ~ spl0_179 ),
inference(avatar_component_clause,[],[f1502]) ).
fof(f1506,definition,
( spl0_180
<=> left_of(house_1,house_4) ),
introduced(definition,[new_symbols(definition,[spl0_180])],[avatar_definition]) ).
fof(f1507,plain,
( left_of(house_1,house_4)
| ~ spl0_180 ),
inference(avatar_component_clause,[],[f1506]) ).
fof(f1508,plain,
( spl0_180
| ~ spl0_129
| spl0_166
| ~ spl0_135
| spl0_179 ),
inference(avatar_split_clause,[],[f1396,f1502,f970,f1454,f944,f1506]) ).
fof(f1510,definition,
( spl0_181
<=> left_of(house_1,house_3) ),
introduced(definition,[new_symbols(definition,[spl0_181])],[avatar_definition]) ).
fof(f1511,plain,
( left_of(house_1,house_3)
| ~ spl0_181 ),
inference(avatar_component_clause,[],[f1510]) ).
fof(f1512,plain,
( spl0_181
| ~ spl0_131
| spl0_160
| ~ spl0_135
| spl0_179 ),
inference(avatar_split_clause,[],[f1395,f1502,f970,f1433,f956,f1510]) ).
fof(f1514,definition,
( spl0_182
<=> left_of(house_1,house_1) ),
introduced(definition,[new_symbols(definition,[spl0_182])],[avatar_definition]) ).
fof(f1515,plain,
( left_of(house_1,house_1)
| ~ spl0_182 ),
inference(avatar_component_clause,[],[f1514]) ).
fof(f1517,plain,
( $false
| ~ spl0_165 ),
inference(resolution,[],[f1452,f122]) ).
fof(f1518,plain,
~ spl0_165,
inference(avatar_contradiction_clause,[],[f1517]) ).
fof(f1520,plain,
( ~ lives(japanese,house_2)
| is_color(house_2,green)
| ~ spl0_144 ),
inference(resolution,[],[f1173,f62]) ).
fof(f1524,plain,
( spl0_108
| ~ spl0_36
| ~ spl0_144 ),
inference(avatar_split_clause,[],[f1520,f1172,f264,f747]) ).
fof(f1525,plain,
( ~ spl0_1
| ~ spl0_108 ),
inference(avatar_split_clause,[],[f829,f747,f130]) ).
fof(f1529,plain,
( ~ lives(english,house_3)
| is_color(house_3,green)
| ~ spl0_145 ),
inference(resolution,[],[f1191,f63]) ).
fof(f1531,plain,
( ~ lives(english,house_5)
| is_color(house_5,green)
| ~ spl0_145 ),
inference(resolution,[],[f1191,f65]) ).
fof(f1537,plain,
( ~ lives(ukranian,house_2)
| is_color(house_2,yellow)
| ~ spl0_150 ),
inference(resolution,[],[f1264,f62]) ).
fof(f1539,plain,
( ~ lives(ukranian,house_4)
| is_color(house_4,yellow)
| ~ spl0_150 ),
inference(resolution,[],[f1264,f64]) ).
fof(f1540,plain,
( ~ lives(ukranian,house_5)
| is_color(house_5,yellow)
| ~ spl0_150 ),
inference(resolution,[],[f1264,f65]) ).
fof(f1542,plain,
( spl0_111
| ~ spl0_9
| ~ spl0_150 ),
inference(avatar_split_clause,[],[f1537,f1263,f154,f758]) ).
fof(f1544,plain,
( ~ spl0_121
| ~ spl0_2 ),
inference(avatar_split_clause,[],[f861,f133,f832]) ).
fof(f1545,plain,
( ~ spl0_121
| ~ spl0_107 ),
inference(avatar_split_clause,[],[f803,f743,f832]) ).
fof(f1547,plain,
( spl0_122
| ~ spl0_39
| ~ spl0_150 ),
inference(avatar_split_clause,[],[f1540,f1263,f289,f836]) ).
fof(f1548,plain,
( ~ spl0_9
| ~ spl0_30 ),
inference(avatar_split_clause,[],[f284,f226,f154]) ).
fof(f1549,plain,
( ~ spl0_122
| ~ spl0_119 ),
inference(avatar_split_clause,[],[f858,f819,f836]) ).
fof(f1550,plain,
( ~ spl0_121
| ~ spl0_128
| ~ spl0_109
| ~ spl0_135 ),
inference(avatar_split_clause,[],[f918,f970,f750,f941,f832]) ).
fof(f1551,plain,
( spl0_111
| ~ spl0_30
| ~ spl0_126 ),
inference(avatar_split_clause,[],[f1366,f900,f226,f758]) ).
fof(f1553,plain,
( spl0_117
| ~ spl0_29
| ~ spl0_126 ),
inference(avatar_split_clause,[],[f1367,f900,f222,f786]) ).
fof(f1554,plain,
( spl0_122
| ~ spl0_26
| ~ spl0_126 ),
inference(avatar_split_clause,[],[f1369,f900,f211,f836]) ).
fof(f1555,plain,
( ~ spl0_120
| ~ spl0_113 ),
inference(avatar_split_clause,[],[f790,f765,f823]) ).
fof(f1561,plain,
( spl0_87
| spl0_89
| spl0_91
| spl0_17
| spl0_93 ),
inference(avatar_split_clause,[],[f1294,f633,f178,f625,f618,f611]) ).
fof(f1564,plain,
( spl0_114
| spl0_115
| spl0_116
| spl0_117
| spl0_3 ),
inference(avatar_split_clause,[],[f1318,f136,f786,f782,f778,f774]) ).
fof(f1565,plain,
( ~ spl0_123
| ~ spl0_120 ),
inference(avatar_split_clause,[],[f857,f823,f840]) ).
fof(f1566,plain,
( ~ spl0_123
| ~ spl0_113 ),
inference(avatar_split_clause,[],[f799,f765,f840]) ).
fof(f1567,plain,
( ~ spl0_119
| ~ spl0_117 ),
inference(avatar_split_clause,[],[f844,f786,f819]) ).
fof(f1568,plain,
( ~ spl0_122
| ~ spl0_117 ),
inference(avatar_split_clause,[],[f853,f786,f836]) ).
fof(f1570,plain,
( ~ spl0_1
| ~ spl0_115 ),
inference(avatar_split_clause,[],[f855,f778,f130]) ).
fof(f1571,plain,
( ~ spl0_121
| ~ spl0_128
| ~ spl0_115
| ~ spl0_131 ),
inference(avatar_split_clause,[],[f926,f956,f778,f941,f832]) ).
fof(f1572,plain,
( ~ spl0_2
| ~ spl0_129
| ~ spl0_115
| ~ spl0_131 ),
inference(avatar_split_clause,[],[f925,f956,f778,f944,f133]) ).
fof(f1573,plain,
( ~ spl0_107
| ~ spl0_135
| ~ spl0_115
| ~ spl0_131 ),
inference(avatar_split_clause,[],[f923,f956,f778,f970,f743]) ).
fof(f1575,plain,
( ~ spl0_18
| ~ spl0_87 ),
inference(avatar_split_clause,[],[f657,f611,f181]) ).
fof(f1576,plain,
( ~ spl0_2
| ~ spl0_114 ),
inference(avatar_split_clause,[],[f847,f774,f133]) ).
fof(f1577,plain,
( ~ spl0_121
| ~ spl0_114 ),
inference(avatar_split_clause,[],[f856,f774,f832]) ).
fof(f1578,plain,
( ~ spl0_114
| ~ spl0_131
| ~ spl0_1
| ~ spl0_128 ),
inference(avatar_split_clause,[],[f933,f941,f130,f956,f774]) ).
fof(f1579,plain,
( ~ spl0_114
| ~ spl0_131
| ~ spl0_109
| ~ spl0_135 ),
inference(avatar_split_clause,[],[f916,f970,f750,f956,f774]) ).
fof(f1580,plain,
( ~ spl0_114
| ~ spl0_131
| ~ spl0_108
| ~ spl0_133 ),
inference(avatar_split_clause,[],[f920,f963,f747,f956,f774]) ).
fof(f1582,plain,
! [X0,X1] :
( ~ drives(X0,masserati)
| ~ house(house_1)
| ~ lives(X0,house_1)
| ~ person(X1)
| ~ owns(X1,horse)
| ~ house(house_1)
| ~ lives(X1,house_1)
| left_of(house_1,house_1)
| ~ person(X0) ),
inference(resolution,[],[f1356,f107]) ).
fof(f1584,plain,
! [X0,X1] :
( ~ drives(X0,masserati)
| ~ house(house_1)
| ~ lives(X0,house_1)
| ~ person(X1)
| ~ owns(X1,horse)
| ~ house(house_3)
| ~ lives(X1,house_3)
| left_of(house_1,house_3)
| ~ person(X0) ),
inference(resolution,[],[f1356,f109]) ).
fof(f1585,plain,
! [X0,X1] :
( ~ drives(X0,masserati)
| ~ house(house_1)
| ~ lives(X0,house_1)
| ~ person(X1)
| ~ owns(X1,horse)
| ~ house(house_4)
| ~ lives(X1,house_4)
| left_of(house_1,house_4)
| ~ person(X0) ),
inference(resolution,[],[f1356,f110]) ).
fof(f1586,plain,
! [X0,X1] :
( ~ drives(X0,masserati)
| ~ house(house_1)
| ~ lives(X0,house_1)
| ~ person(X1)
| ~ owns(X1,horse)
| ~ house(house_5)
| ~ lives(X1,house_5)
| left_of(house_1,house_5)
| ~ person(X0) ),
inference(resolution,[],[f1356,f111]) ).
fof(f1607,plain,
! [X0,X1] :
( ~ drives(X0,masserati)
| ~ house(house_1)
| ~ lives(X0,house_1)
| ~ person(X1)
| ~ owns(X1,horse)
| ~ lives(X1,house_1)
| left_of(house_1,house_1)
| ~ person(X0) ),
inference(duplicate_literal_removal,[],[f1582]) ).
fof(f1609,definition,
( spl0_183
<=> ! [X1] :
( ~ person(X1)
| ~ lives(X1,house_5)
| ~ owns(X1,horse) ) ),
introduced(definition,[new_symbols(definition,[spl0_183])],[avatar_definition]) ).
fof(f1610,plain,
( ! [X1] :
( ~ person(X1)
| ~ lives(X1,house_5)
| ~ owns(X1,horse) )
| ~ spl0_183 ),
inference(avatar_component_clause,[],[f1609]) ).
fof(f1616,definition,
( spl0_185
<=> ! [X1] :
( ~ person(X1)
| ~ lives(X1,house_3)
| ~ owns(X1,horse) ) ),
introduced(definition,[new_symbols(definition,[spl0_185])],[avatar_definition]) ).
fof(f1617,plain,
( ! [X1] :
( ~ person(X1)
| ~ lives(X1,house_3)
| ~ owns(X1,horse) )
| ~ spl0_185 ),
inference(avatar_component_clause,[],[f1616]) ).
fof(f1624,definition,
( spl0_187
<=> ! [X1] :
( ~ person(X1)
| ~ lives(X1,house_1)
| ~ owns(X1,horse) ) ),
introduced(definition,[new_symbols(definition,[spl0_187])],[avatar_definition]) ).
fof(f1625,plain,
( ! [X1] :
( ~ person(X1)
| ~ lives(X1,house_1)
| ~ owns(X1,horse) )
| ~ spl0_187 ),
inference(avatar_component_clause,[],[f1624]) ).
fof(f1628,definition,
( spl0_188
<=> ! [X1] :
( ~ person(X1)
| ~ lives(X1,house_4)
| ~ owns(X1,horse) ) ),
introduced(definition,[new_symbols(definition,[spl0_188])],[avatar_definition]) ).
fof(f1629,plain,
( ! [X1] :
( ~ person(X1)
| ~ lives(X1,house_4)
| ~ owns(X1,horse) )
| ~ spl0_188 ),
inference(avatar_component_clause,[],[f1628]) ).
fof(f1649,definition,
( spl0_192
<=> ! [X0] :
( ~ drives(X0,masserati)
| ~ person(X0)
| ~ lives(X0,house_1) ) ),
introduced(definition,[new_symbols(definition,[spl0_192])],[avatar_definition]) ).
fof(f1650,plain,
( ! [X0] :
( ~ person(X0)
| ~ drives(X0,masserati)
| ~ lives(X0,house_1) )
| ~ spl0_192 ),
inference(avatar_component_clause,[],[f1649]) ).
fof(f1651,plain,
( spl0_178
| ~ spl0_128
| spl0_183
| ~ spl0_135
| spl0_192 ),
inference(avatar_split_clause,[],[f1586,f1649,f970,f1609,f941,f1499]) ).
fof(f1652,plain,
( spl0_180
| ~ spl0_129
| spl0_188
| ~ spl0_135
| spl0_192 ),
inference(avatar_split_clause,[],[f1585,f1649,f970,f1628,f944,f1506]) ).
fof(f1653,plain,
( spl0_181
| ~ spl0_131
| spl0_185
| ~ spl0_135
| spl0_192 ),
inference(avatar_split_clause,[],[f1584,f1649,f970,f1616,f956,f1510]) ).
fof(f1654,plain,
( spl0_182
| spl0_187
| ~ spl0_135
| spl0_192 ),
inference(avatar_split_clause,[],[f1607,f1649,f970,f1624,f1514]) ).
fof(f1664,plain,
( ~ lives(norwegian,house_1)
| is_color(house_1,green)
| ~ spl0_149 ),
inference(resolution,[],[f1255,f61]) ).
fof(f1669,plain,
( spl0_109
| ~ spl0_10
| ~ spl0_149 ),
inference(avatar_split_clause,[],[f1664,f1254,f157,f750]) ).
fof(f1676,plain,
( ~ lives(japanese,house_4)
| is_color(house_4,green)
| ~ spl0_144 ),
inference(resolution,[],[f1173,f64]) ).
fof(f1682,plain,
( ~ lives(english,house_3)
| is_color(house_3,yellow)
| ~ spl0_151 ),
inference(resolution,[],[f1278,f63]) ).
fof(f1684,plain,
( ~ lives(english,house_5)
| is_color(house_5,yellow)
| ~ spl0_151 ),
inference(resolution,[],[f1278,f65]) ).
fof(f1744,plain,
( ~ owns(ukranian,fox)
| ~ lives(ukranian,house_4)
| ~ spl0_167 ),
inference(resolution,[],[f1458,f59]) ).
fof(f1754,plain,
( ~ owns(ukranian,fox)
| ~ lives(ukranian,house_2)
| ~ spl0_175 ),
inference(resolution,[],[f1488,f59]) ).
fof(f1767,plain,
( ~ spl0_18
| ~ spl0_95 ),
inference(avatar_split_clause,[],[f723,f664,f181]) ).
fof(f1775,plain,
( ~ spl0_102
| ~ spl0_99 ),
inference(avatar_split_clause,[],[f725,f686,f703]) ).
fof(f1776,plain,
( ~ spl0_95
| ~ spl0_87 ),
inference(avatar_split_clause,[],[f642,f611,f664]) ).
fof(f1777,plain,
( ~ spl0_105
| ~ spl0_20 ),
inference(avatar_split_clause,[],[f722,f187,f731]) ).
fof(f1779,plain,
( ~ spl0_105
| ~ spl0_89 ),
inference(avatar_split_clause,[],[f656,f618,f731]) ).
fof(f1780,plain,
( $false
| ~ spl0_159 ),
inference(resolution,[],[f1431,f119]) ).
fof(f1781,plain,
~ spl0_159,
inference(avatar_contradiction_clause,[],[f1780]) ).
fof(f1791,plain,
( $false
| ~ spl0_181 ),
inference(resolution,[],[f1511,f116]) ).
fof(f1792,plain,
~ spl0_181,
inference(avatar_contradiction_clause,[],[f1791]) ).
fof(f1805,plain,
( $false
| ~ spl0_177 ),
inference(resolution,[],[f1496,f112]) ).
fof(f1806,plain,
~ spl0_177,
inference(avatar_contradiction_clause,[],[f1805]) ).
fof(f1808,plain,
( ~ spl0_9
| ~ spl0_94
| ~ spl0_175 ),
inference(avatar_split_clause,[],[f1754,f1487,f650,f154]) ).
fof(f1809,plain,
( ~ spl0_42
| ~ spl0_94
| ~ spl0_167 ),
inference(avatar_split_clause,[],[f1744,f1457,f650,f311]) ).
fof(f1820,plain,
( ~ owns(japanese,fox)
| ~ lives(japanese,house_5)
| ~ spl0_158 ),
inference(resolution,[],[f1427,f60]) ).
fof(f1821,plain,
( ~ lives(english,house_3)
| ~ drives(english,saab)
| ~ spl0_160 ),
inference(resolution,[],[f1434,f56]) ).
fof(f1822,plain,
( ~ lives(spaniard,house_3)
| ~ drives(spaniard,saab)
| ~ spl0_160 ),
inference(resolution,[],[f1434,f57]) ).
fof(f1832,plain,
( ~ lives(spaniard,house_4)
| ~ drives(spaniard,saab)
| ~ spl0_166 ),
inference(resolution,[],[f1455,f57]) ).
fof(f1834,plain,
( ~ lives(ukranian,house_4)
| ~ drives(ukranian,saab)
| ~ spl0_166 ),
inference(resolution,[],[f1455,f59]) ).
fof(f1837,plain,
( $false
| ~ spl0_180 ),
inference(resolution,[],[f1507,f120]) ).
fof(f1838,plain,
~ spl0_180,
inference(avatar_contradiction_clause,[],[f1837]) ).
fof(f1840,plain,
( $false
| ~ spl0_161 ),
inference(resolution,[],[f1438,f115]) ).
fof(f1841,plain,
~ spl0_161,
inference(avatar_contradiction_clause,[],[f1840]) ).
fof(f1889,plain,
( ~ drives(norwegian,masserati)
| ~ lives(norwegian,house_1)
| ~ spl0_192 ),
inference(resolution,[],[f1650,f58]) ).
fof(f1893,plain,
( $false
| ~ spl0_182 ),
inference(resolution,[],[f1515,f107]) ).
fof(f1894,plain,
~ spl0_182,
inference(avatar_contradiction_clause,[],[f1893]) ).
fof(f1899,plain,
( ~ lives(japanese,house_3)
| ~ owns(japanese,horse)
| ~ spl0_185 ),
inference(resolution,[],[f1617,f60]) ).
fof(f1902,plain,
( ~ lives(norwegian,house_1)
| ~ owns(norwegian,horse)
| ~ spl0_187 ),
inference(resolution,[],[f1625,f58]) ).
fof(f1905,plain,
( ~ spl0_96
| ~ spl0_10
| ~ spl0_187 ),
inference(avatar_split_clause,[],[f1902,f1624,f157,f668]) ).
fof(f1909,plain,
( ~ spl0_102
| ~ spl0_17 ),
inference(avatar_split_clause,[],[f654,f178,f703]) ).
fof(f1911,plain,
( $false
| ~ spl0_178 ),
inference(resolution,[],[f1500,f124]) ).
fof(f1912,plain,
~ spl0_178,
inference(avatar_contradiction_clause,[],[f1911]) ).
fof(f1922,plain,
( ~ lives(ukranian,house_2)
| ~ drives(ukranian,saab)
| ~ spl0_162 ),
inference(resolution,[],[f1441,f59]) ).
fof(f1926,plain,
( ~ owns(norwegian,fox)
| ~ lives(norwegian,house_1)
| ~ spl0_179 ),
inference(resolution,[],[f1503,f58]) ).
fof(f1929,plain,
( ~ lives(english,house_5)
| ~ owns(english,horse)
| ~ spl0_183 ),
inference(resolution,[],[f1610,f56]) ).
fof(f1933,plain,
( ~ lives(japanese,house_5)
| ~ owns(japanese,horse)
| ~ spl0_183 ),
inference(resolution,[],[f1610,f60]) ).
fof(f1937,plain,
( ~ lives(ukranian,house_4)
| ~ owns(ukranian,horse)
| ~ spl0_188 ),
inference(resolution,[],[f1629,f59]) ).
fof(f1938,plain,
( ~ lives(japanese,house_4)
| ~ owns(japanese,horse)
| ~ spl0_188 ),
inference(resolution,[],[f1629,f60]) ).
fof(f1939,plain,
( ~ spl0_19
| ~ spl0_42
| ~ spl0_188 ),
inference(avatar_split_clause,[],[f1937,f1628,f311,f184]) ).
fof(f1940,plain,
( spl0_108
| ~ spl0_30
| ~ spl0_127 ),
inference(avatar_split_clause,[],[f1375,f911,f226,f747]) ).
fof(f1941,plain,
( spl0_124
| ~ spl0_6
| ~ spl0_127 ),
inference(avatar_split_clause,[],[f1377,f911,f145,f849]) ).
fof(f1943,plain,
( spl0_119
| ~ spl0_42
| ~ spl0_150 ),
inference(avatar_split_clause,[],[f1539,f1263,f311,f819]) ).
fof(f1944,plain,
( ~ spl0_14
| ~ spl0_42
| ~ spl0_166 ),
inference(avatar_split_clause,[],[f1834,f1454,f311,f169]) ).
fof(f1945,plain,
( ~ spl0_101
| ~ spl0_8
| ~ spl0_183 ),
inference(avatar_split_clause,[],[f1933,f1609,f151,f699]) ).
fof(f1953,plain,
( ~ spl0_41
| ~ spl0_40 ),
inference(avatar_split_clause,[],[f329,f293,f302]) ).
fof(f1964,plain,
( spl0_117
| ~ spl0_7
| ~ spl0_151 ),
inference(avatar_split_clause,[],[f1682,f1277,f148,f786]) ).
fof(f1965,plain,
( spl0_122
| ~ spl0_27
| ~ spl0_151 ),
inference(avatar_split_clause,[],[f1684,f1277,f214,f836]) ).
fof(f1966,plain,
( ~ spl0_10
| ~ spl0_15
| ~ spl0_192 ),
inference(avatar_split_clause,[],[f1889,f1649,f172,f157]) ).
fof(f1977,plain,
( ~ spl0_70
| ~ spl0_6
| ~ spl0_166 ),
inference(avatar_split_clause,[],[f1832,f1454,f145,f491]) ).
fof(f1978,plain,
( ~ spl0_14
| ~ spl0_9
| ~ spl0_162 ),
inference(avatar_split_clause,[],[f1922,f1440,f154,f169]) ).
fof(f1984,plain,
( spl0_124
| ~ spl0_45
| ~ spl0_144 ),
inference(avatar_split_clause,[],[f1676,f1172,f334,f849]) ).
fof(f1987,plain,
( ~ spl0_101
| ~ spl0_41
| ~ spl0_185 ),
inference(avatar_split_clause,[],[f1899,f1616,f302,f699]) ).
fof(f1989,plain,
( ~ spl0_101
| ~ spl0_45
| ~ spl0_188 ),
inference(avatar_split_clause,[],[f1938,f1628,f334,f699]) ).
fof(f1992,plain,
( spl0_115
| ~ spl0_29
| ~ spl0_127 ),
inference(avatar_split_clause,[],[f1376,f911,f222,f778]) ).
fof(f1994,plain,
( ~ spl0_8
| ~ spl0_105
| ~ spl0_158 ),
inference(avatar_split_clause,[],[f1820,f1426,f731,f151]) ).
fof(f1997,plain,
( ~ spl0_10
| ~ spl0_20
| ~ spl0_179 ),
inference(avatar_split_clause,[],[f1926,f1502,f187,f157]) ).
fof(f1999,plain,
( ~ spl0_91
| ~ spl0_27
| ~ spl0_183 ),
inference(avatar_split_clause,[],[f1929,f1609,f214,f625]) ).
fof(f2001,plain,
( spl0_115
| ~ spl0_7
| ~ spl0_145 ),
inference(avatar_split_clause,[],[f1529,f1190,f148,f778]) ).
fof(f2002,plain,
( spl0_1
| ~ spl0_27
| ~ spl0_145 ),
inference(avatar_split_clause,[],[f1531,f1190,f214,f130]) ).
fof(f2006,plain,
( ~ spl0_71
| ~ spl0_7
| ~ spl0_160 ),
inference(avatar_split_clause,[],[f1821,f1433,f148,f494]) ).
fof(f2007,plain,
( ~ spl0_70
| ~ spl0_29
| ~ spl0_160 ),
inference(avatar_split_clause,[],[f1822,f1433,f222,f491]) ).
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,[],[f204]) ).
cnf(s2,plain,
( ~ spl0_26
| ~ spl0_27 ),
inference(sat_conversion,[],[f216]) ).
cnf(s4,plain,
( ~ spl0_7
| ~ spl0_29 ),
inference(sat_conversion,[],[f224]) ).
cnf(s13,plain,
( ~ spl0_10
| ~ spl0_32 ),
inference(sat_conversion,[],[f280]) ).
cnf(s14,plain,
spl0_10,
inference(sat_conversion,[],[f282]) ).
cnf(s15,plain,
( ~ spl0_26
| ~ spl0_39 ),
inference(sat_conversion,[],[f291]) ).
cnf(s16,plain,
( ~ spl0_29
| ~ spl0_40 ),
inference(sat_conversion,[],[f295]) ).
cnf(s17,plain,
( ~ spl0_29
| ~ spl0_41 ),
inference(sat_conversion,[],[f304]) ).
cnf(s19,plain,
( ~ spl0_10
| ~ spl0_43 ),
inference(sat_conversion,[],[f317]) ).
cnf(s20,plain,
( ~ spl0_10
| ~ spl0_44 ),
inference(sat_conversion,[],[f326]) ).
cnf(s21,plain,
( ~ spl0_8
| ~ spl0_39 ),
inference(sat_conversion,[],[f332]) ).
cnf(s22,plain,
( ~ spl0_42
| ~ spl0_45 ),
inference(sat_conversion,[],[f336]) ).
cnf(s23,plain,
( ~ spl0_46
| ~ spl0_47 ),
inference(sat_conversion,[],[f348]) ).
cnf(s27,plain,
( ~ spl0_21
| ~ spl0_53 ),
inference(sat_conversion,[],[f370]) ).
cnf(s28,plain,
( ~ spl0_53
| ~ spl0_54 ),
inference(sat_conversion,[],[f379]) ).
cnf(s29,plain,
( ~ spl0_25
| ~ spl0_46 ),
inference(sat_conversion,[],[f395]) ).
cnf(s35,plain,
( ~ spl0_24
| ~ spl0_49 ),
inference(sat_conversion,[],[f421]) ).
cnf(s37,plain,
spl0_24,
inference(sat_conversion,[],[f427]) ).
cnf(s39,plain,
( ~ spl0_48
| ~ spl0_62 ),
inference(sat_conversion,[],[f440]) ).
cnf(s40,plain,
( ~ spl0_23
| ~ spl0_51 ),
inference(sat_conversion,[],[f441]) ).
cnf(s41,plain,
( ~ spl0_54
| ~ spl0_63 ),
inference(sat_conversion,[],[f450]) ).
cnf(s42,plain,
( ~ spl0_54
| ~ spl0_64 ),
inference(sat_conversion,[],[f459]) ).
cnf(s43,plain,
( ~ spl0_24
| ~ spl0_65 ),
inference(sat_conversion,[],[f468]) ).
cnf(s44,plain,
( ~ spl0_63
| ~ spl0_64 ),
inference(sat_conversion,[],[f469]) ).
cnf(s47,plain,
( ~ spl0_12
| ~ spl0_69 ),
inference(sat_conversion,[],[f489]) ).
cnf(s48,plain,
( ~ spl0_70
| ~ spl0_71 ),
inference(sat_conversion,[],[f496]) ).
cnf(s51,plain,
( ~ spl0_71
| ~ spl0_75 ),
inference(sat_conversion,[],[f516]) ).
cnf(s52,plain,
( ~ spl0_14
| ~ spl0_71 ),
inference(sat_conversion,[],[f522]) ).
cnf(s55,plain,
( ~ spl0_69
| ~ spl0_78 ),
inference(sat_conversion,[],[f544]) ).
cnf(s58,plain,
( ~ spl0_69
| ~ spl0_80 ),
inference(sat_conversion,[],[f558]) ).
cnf(s63,plain,
( ~ spl0_13
| ~ spl0_79 ),
inference(sat_conversion,[],[f595]) ).
cnf(s65,plain,
spl0_13,
inference(sat_conversion,[],[f601]) ).
cnf(s69,plain,
( ~ spl0_17
| ~ spl0_92 ),
inference(sat_conversion,[],[f631]) ).
cnf(s70,plain,
( ~ spl0_16
| ~ spl0_93 ),
inference(sat_conversion,[],[f635]) ).
cnf(s71,plain,
spl0_16,
inference(sat_conversion,[],[f637]) ).
cnf(s72,plain,
( ~ spl0_20
| ~ spl0_89 ),
inference(sat_conversion,[],[f643]) ).
cnf(s76,plain,
( ~ spl0_92
| ~ spl0_97 ),
inference(sat_conversion,[],[f674]) ).
cnf(s77,plain,
( ~ spl0_16
| ~ spl0_98 ),
inference(sat_conversion,[],[f678]) ).
cnf(s80,plain,
( ~ spl0_16
| ~ spl0_100 ),
inference(sat_conversion,[],[f692]) ).
cnf(s82,plain,
( ~ spl0_92
| ~ spl0_102 ),
inference(sat_conversion,[],[f705]) ).
cnf(s83,plain,
( ~ spl0_16
| ~ spl0_103 ),
inference(sat_conversion,[],[f709]) ).
cnf(s84,plain,
( ~ spl0_95
| ~ spl0_104 ),
inference(sat_conversion,[],[f718]) ).
cnf(s85,plain,
( ~ spl0_18
| ~ spl0_104 ),
inference(sat_conversion,[],[f729]) ).
cnf(s89,plain,
( ~ spl0_4
| ~ spl0_110 ),
inference(sat_conversion,[],[f756]) ).
cnf(s90,plain,
( ~ spl0_5
| ~ spl0_111 ),
inference(sat_conversion,[],[f760]) ).
cnf(s91,plain,
( ~ spl0_112
| ~ spl0_113 ),
inference(sat_conversion,[],[f767]) ).
cnf(s92,plain,
( ~ spl0_107
| ~ spl0_114 ),
inference(sat_conversion,[],[f776]) ).
cnf(s93,plain,
( ~ spl0_109
| ~ spl0_115 ),
inference(sat_conversion,[],[f780]) ).
cnf(s95,plain,
( ~ spl0_5
| ~ spl0_117 ),
inference(sat_conversion,[],[f788]) ).
cnf(s96,plain,
( ~ spl0_3
| ~ spl0_113 ),
inference(sat_conversion,[],[f789]) ).
cnf(s100,plain,
( ~ spl0_3
| ~ spl0_112 ),
inference(sat_conversion,[],[f811]) ).
cnf(s103,plain,
( ~ spl0_112
| ~ spl0_120 ),
inference(sat_conversion,[],[f825]) ).
cnf(s106,plain,
( ~ spl0_112
| ~ spl0_123 ),
inference(sat_conversion,[],[f842]) ).
cnf(s107,plain,
( ~ spl0_115
| ~ spl0_124 ),
inference(sat_conversion,[],[f851]) ).
cnf(s110,plain,
( spl0_63
| ~ spl0_84 ),
inference(sat_conversion,[],[f884]) ).
cnf(s111,plain,
( spl0_29
| ~ spl0_48 ),
inference(sat_conversion,[],[f891]) ).
cnf(s112,plain,
( ~ spl0_72
| spl0_126 ),
inference(sat_conversion,[],[f902]) ).
cnf(s113,plain,
( ~ spl0_51
| spl0_127 ),
inference(sat_conversion,[],[f913]) ).
cnf(s114,plain,
( ~ spl0_121
| ~ spl0_124
| ~ spl0_128
| ~ spl0_129 ),
inference(sat_conversion,[],[f946]) ).
cnf(s119,plain,
spl0_133,
inference(sat_conversion,[],[f977]) ).
cnf(s120,plain,
( ~ spl0_4
| ~ spl0_125 ),
inference(sat_conversion,[],[f978]) ).
cnf(s121,plain,
spl0_129,
inference(sat_conversion,[],[f980]) ).
cnf(s122,plain,
( ~ spl0_4
| ~ spl0_118 ),
inference(sat_conversion,[],[f981]) ).
cnf(s123,plain,
spl0_131,
inference(sat_conversion,[],[f983]) ).
cnf(s126,plain,
( ~ spl0_4
| ~ spl0_116 ),
inference(sat_conversion,[],[f986]) ).
cnf(s128,plain,
spl0_135,
inference(sat_conversion,[],[f990]) ).
cnf(s131,plain,
( spl0_8
| spl0_36
| spl0_41
| spl0_44
| spl0_45 ),
inference(sat_conversion,[],[f1009]) ).
cnf(s132,plain,
( spl0_9
| spl0_39
| spl0_40
| spl0_42
| spl0_43 ),
inference(sat_conversion,[],[f1015]) ).
cnf(s133,plain,
( spl0_6
| spl0_26
| spl0_29
| spl0_30
| spl0_32 ),
inference(sat_conversion,[],[f1020]) ).
cnf(s134,plain,
( spl0_7
| spl0_27
| spl0_28
| spl0_31
| spl0_33 ),
inference(sat_conversion,[],[f1026]) ).
cnf(s135,plain,
( ~ spl0_9
| ~ spl0_36 ),
inference(sat_conversion,[],[f1027]) ).
cnf(s136,plain,
( ~ spl0_7
| ~ spl0_41 ),
inference(sat_conversion,[],[f1028]) ).
cnf(s137,plain,
( spl0_3
| ~ spl0_7 ),
inference(sat_conversion,[],[f1030]) ).
cnf(s138,plain,
( ~ spl0_6
| ~ spl0_42 ),
inference(sat_conversion,[],[f1031]) ).
cnf(s139,plain,
( ~ spl0_27
| ~ spl0_39 ),
inference(sat_conversion,[],[f1032]) ).
cnf(s140,plain,
( ~ spl0_8
| ~ spl0_27 ),
inference(sat_conversion,[],[f1033]) ).
cnf(s141,plain,
( ~ spl0_27
| spl0_123 ),
inference(sat_conversion,[],[f1035]) ).
cnf(s143,plain,
( ~ spl0_28
| spl0_120 ),
inference(sat_conversion,[],[f1038]) ).
cnf(s144,plain,
( ~ spl0_8
| ~ spl0_26 ),
inference(sat_conversion,[],[f1039]) ).
cnf(s145,plain,
( ~ spl0_10
| ~ spl0_33 ),
inference(sat_conversion,[],[f1040]) ).
cnf(s148,plain,
( spl0_118
| ~ spl0_129
| spl0_137 ),
inference(sat_conversion,[],[f1051]) ).
cnf(s153,plain,
( spl0_4
| ~ spl0_133
| spl0_139 ),
inference(sat_conversion,[],[f1069]) ).
cnf(s156,plain,
( ~ spl0_10
| ~ spl0_139
| ~ spl0_143 ),
inference(sat_conversion,[],[f1088]) ).
cnf(s157,plain,
spl0_128,
inference(sat_conversion,[],[f1090]) ).
cnf(s158,plain,
spl0_143,
inference(sat_conversion,[],[f1093]) ).
cnf(s163,plain,
( spl0_23
| spl0_61
| spl0_62
| spl0_64
| spl0_65 ),
inference(sat_conversion,[],[f1152]) ).
cnf(s164,plain,
( spl0_25
| spl0_54
| spl0_55
| spl0_56
| spl0_57 ),
inference(sat_conversion,[],[f1158]) ).
cnf(s165,plain,
( spl0_21
| spl0_46
| spl0_48
| spl0_49
| spl0_51 ),
inference(sat_conversion,[],[f1164]) ).
cnf(s166,plain,
( spl0_22
| spl0_47
| spl0_50
| spl0_52
| spl0_53 ),
inference(sat_conversion,[],[f1170]) ).
cnf(s167,plain,
( ~ spl0_23
| spl0_144 ),
inference(sat_conversion,[],[f1174]) ).
cnf(s168,plain,
( ~ spl0_21
| ~ spl0_64 ),
inference(sat_conversion,[],[f1175]) ).
cnf(s169,plain,
( ~ spl0_25
| ~ spl0_61 ),
inference(sat_conversion,[],[f1176]) ).
cnf(s170,plain,
( ~ spl0_21
| ~ spl0_54 ),
inference(sat_conversion,[],[f1177]) ).
cnf(s171,plain,
( ~ spl0_25
| ~ spl0_47 ),
inference(sat_conversion,[],[f1178]) ).
cnf(s172,plain,
( ~ spl0_47
| ~ spl0_61 ),
inference(sat_conversion,[],[f1179]) ).
cnf(s173,plain,
( ~ spl0_31
| spl0_112 ),
inference(sat_conversion,[],[f1181]) ).
cnf(s174,plain,
( spl0_7
| ~ spl0_22 ),
inference(sat_conversion,[],[f1182]) ).
cnf(s175,plain,
( spl0_38
| ~ spl0_55 ),
inference(sat_conversion,[],[f1184]) ).
cnf(s177,plain,
( ~ spl0_24
| ~ spl0_50 ),
inference(sat_conversion,[],[f1186]) ).
cnf(s178,plain,
( ~ spl0_6
| ~ spl0_45 ),
inference(sat_conversion,[],[f1187]) ).
cnf(s180,plain,
( ~ spl0_52
| spl0_145 ),
inference(sat_conversion,[],[f1192]) ).
cnf(s183,plain,
( ~ spl0_38
| ~ spl0_137
| ~ spl0_147 ),
inference(sat_conversion,[],[f1201]) ).
cnf(s184,plain,
( ~ spl0_24
| ~ spl0_56 ),
inference(sat_conversion,[],[f1202]) ).
cnf(s186,plain,
( spl0_14
| spl0_79
| spl0_80
| spl0_81
| spl0_84 ),
inference(sat_conversion,[],[f1214]) ).
cnf(s187,plain,
( spl0_15
| spl0_74
| spl0_75
| spl0_77
| spl0_78 ),
inference(sat_conversion,[],[f1220]) ).
cnf(s188,plain,
( spl0_11
| spl0_66
| spl0_69
| spl0_70
| spl0_72 ),
inference(sat_conversion,[],[f1226]) ).
cnf(s189,plain,
( spl0_12
| spl0_67
| spl0_68
| spl0_71
| spl0_73 ),
inference(sat_conversion,[],[f1232]) ).
cnf(s192,plain,
( ~ spl0_12
| spl0_17 ),
inference(sat_conversion,[],[f1239]) ).
cnf(s193,plain,
( spl0_54
| ~ spl0_74 ),
inference(sat_conversion,[],[f1240]) ).
cnf(s195,plain,
( ~ spl0_14
| ~ spl0_75 ),
inference(sat_conversion,[],[f1242]) ).
cnf(s197,plain,
( ~ spl0_80
| spl0_99 ),
inference(sat_conversion,[],[f1245]) ).
cnf(s198,plain,
( ~ spl0_12
| ~ spl0_80 ),
inference(sat_conversion,[],[f1246]) ).
cnf(s200,plain,
( ~ spl0_21
| ~ spl0_63 ),
inference(sat_conversion,[],[f1248]) ).
cnf(s201,plain,
( ~ spl0_70
| ~ spl0_75 ),
inference(sat_conversion,[],[f1249]) ).
cnf(s202,plain,
( ~ spl0_14
| ~ spl0_70 ),
inference(sat_conversion,[],[f1250]) ).
cnf(s205,plain,
( ~ spl0_57
| spl0_149 ),
inference(sat_conversion,[],[f1256]) ).
cnf(s207,plain,
( ~ spl0_11
| spl0_21 ),
inference(sat_conversion,[],[f1258]) ).
cnf(s208,plain,
( ~ spl0_53
| ~ spl0_63 ),
inference(sat_conversion,[],[f1259]) ).
cnf(s209,plain,
( ~ spl0_53
| ~ spl0_64 ),
inference(sat_conversion,[],[f1260]) ).
cnf(s211,plain,
( ~ spl0_81
| spl0_150 ),
inference(sat_conversion,[],[f1265]) ).
cnf(s213,plain,
( ~ spl0_69
| spl0_92 ),
inference(sat_conversion,[],[f1268]) ).
cnf(s215,plain,
( spl0_53
| ~ spl0_68 ),
inference(sat_conversion,[],[f1270]) ).
cnf(s216,plain,
( spl0_41
| ~ spl0_62 ),
inference(sat_conversion,[],[f1271]) ).
cnf(s221,plain,
( ~ spl0_73
| spl0_151 ),
inference(sat_conversion,[],[f1279]) ).
cnf(s222,plain,
( ~ spl0_13
| ~ spl0_67 ),
inference(sat_conversion,[],[f1280]) ).
cnf(s223,plain,
( ~ spl0_13
| ~ spl0_77 ),
inference(sat_conversion,[],[f1281]) ).
cnf(s225,plain,
( ~ spl0_78
| ~ spl0_80 ),
inference(sat_conversion,[],[f1283]) ).
cnf(s227,plain,
( ~ spl0_12
| ~ spl0_78 ),
inference(sat_conversion,[],[f1286]) ).
cnf(s228,plain,
( ~ spl0_13
| ~ spl0_66 ),
inference(sat_conversion,[],[f1287]) ).
cnf(s229,plain,
( ~ spl0_17
| ~ spl0_99 ),
inference(sat_conversion,[],[f1288]) ).
cnf(s230,plain,
( ~ spl0_97
| ~ spl0_99 ),
inference(sat_conversion,[],[f1289]) ).
cnf(s231,plain,
( ~ spl0_17
| ~ spl0_97 ),
inference(sat_conversion,[],[f1290]) ).
cnf(s233,plain,
( spl0_18
| spl0_101
| spl0_102
| spl0_103
| spl0_105 ),
inference(sat_conversion,[],[f1303]) ).
cnf(s234,plain,
( spl0_19
| spl0_94
| spl0_99
| spl0_100
| spl0_104 ),
inference(sat_conversion,[],[f1308]) ).
cnf(s235,plain,
( spl0_20
| spl0_95
| spl0_96
| spl0_97
| spl0_98 ),
inference(sat_conversion,[],[f1313]) ).
cnf(s238,plain,
( spl0_1
| spl0_121
| spl0_122
| spl0_123
| spl0_125 ),
inference(sat_conversion,[],[f1325]) ).
cnf(s239,plain,
( spl0_2
| spl0_118
| spl0_119
| spl0_120
| spl0_124 ),
inference(sat_conversion,[],[f1330]) ).
cnf(s241,plain,
( spl0_5
| spl0_107
| spl0_109
| spl0_110
| spl0_113 ),
inference(sat_conversion,[],[f1340]) ).
cnf(s242,plain,
( ~ spl0_1
| ~ spl0_124 ),
inference(sat_conversion,[],[f1341]) ).
cnf(s243,plain,
( ~ spl0_3
| ~ spl0_120 ),
inference(sat_conversion,[],[f1342]) ).
cnf(s244,plain,
( ~ spl0_5
| ~ spl0_119 ),
inference(sat_conversion,[],[f1343]) ).
cnf(s248,plain,
( ~ spl0_6
| spl0_119
| ~ spl0_126 ),
inference(sat_conversion,[],[f1370]) ).
cnf(s249,plain,
spl0_147,
inference(sat_conversion,[],[f1373]) ).
cnf(s251,plain,
( ~ spl0_5
| ~ spl0_122 ),
inference(sat_conversion,[],[f1380]) ).
cnf(s252,plain,
( ~ spl0_3
| ~ spl0_123 ),
inference(sat_conversion,[],[f1381]) ).
cnf(s253,plain,
( ~ spl0_109
| ~ spl0_124 ),
inference(sat_conversion,[],[f1382]) ).
cnf(s254,plain,
( ~ spl0_1
| ~ spl0_109 ),
inference(sat_conversion,[],[f1383]) ).
cnf(s255,plain,
( ~ spl0_2
| ~ spl0_109
| ~ spl0_129
| ~ spl0_135 ),
inference(sat_conversion,[],[f1384]) ).
cnf(s256,plain,
( ~ spl0_2
| ~ spl0_107 ),
inference(sat_conversion,[],[f1385]) ).
cnf(s257,plain,
( ~ spl0_107
| ~ spl0_124
| ~ spl0_129
| ~ spl0_135 ),
inference(sat_conversion,[],[f1386]) ).
cnf(s258,plain,
( ~ spl0_1
| ~ spl0_107
| ~ spl0_128
| ~ spl0_135 ),
inference(sat_conversion,[],[f1387]) ).
cnf(s262,plain,
( ~ spl0_7
| ~ spl0_40 ),
inference(sat_conversion,[],[f1391]) ).
cnf(s265,plain,
( ~ spl0_128
| ~ spl0_131
| spl0_158
| spl0_159
| spl0_160 ),
inference(sat_conversion,[],[f1435]) ).
cnf(s266,plain,
( ~ spl0_128
| ~ spl0_133
| spl0_158
| spl0_161
| spl0_162 ),
inference(sat_conversion,[],[f1442]) ).
cnf(s268,plain,
( ~ spl0_129
| spl0_165
| spl0_166
| spl0_167 ),
inference(sat_conversion,[],[f1459]) ).
cnf(s276,plain,
( ~ spl0_133
| spl0_162
| spl0_175
| spl0_177 ),
inference(sat_conversion,[],[f1497]) ).
cnf(s278,plain,
( ~ spl0_129
| ~ spl0_135
| spl0_166
| spl0_179
| spl0_180 ),
inference(sat_conversion,[],[f1508]) ).
cnf(s279,plain,
( ~ spl0_131
| ~ spl0_135
| spl0_160
| spl0_179
| spl0_181 ),
inference(sat_conversion,[],[f1512]) ).
cnf(s281,plain,
~ spl0_165,
inference(sat_conversion,[],[f1518]) ).
cnf(s282,plain,
( ~ spl0_36
| spl0_108
| ~ spl0_144 ),
inference(sat_conversion,[],[f1524]) ).
cnf(s283,plain,
( ~ spl0_1
| ~ spl0_108 ),
inference(sat_conversion,[],[f1525]) ).
cnf(s288,plain,
( ~ spl0_9
| spl0_111
| ~ spl0_150 ),
inference(sat_conversion,[],[f1542]) ).
cnf(s290,plain,
( ~ spl0_2
| ~ spl0_121 ),
inference(sat_conversion,[],[f1544]) ).
cnf(s291,plain,
( ~ spl0_107
| ~ spl0_121 ),
inference(sat_conversion,[],[f1545]) ).
cnf(s293,plain,
( ~ spl0_39
| spl0_122
| ~ spl0_150 ),
inference(sat_conversion,[],[f1547]) ).
cnf(s294,plain,
( ~ spl0_9
| ~ spl0_30 ),
inference(sat_conversion,[],[f1548]) ).
cnf(s295,plain,
( ~ spl0_119
| ~ spl0_122 ),
inference(sat_conversion,[],[f1549]) ).
cnf(s296,plain,
( ~ spl0_109
| ~ spl0_121
| ~ spl0_128
| ~ spl0_135 ),
inference(sat_conversion,[],[f1550]) ).
cnf(s297,plain,
( ~ spl0_30
| spl0_111
| ~ spl0_126 ),
inference(sat_conversion,[],[f1551]) ).
cnf(s298,plain,
( ~ spl0_29
| spl0_117
| ~ spl0_126 ),
inference(sat_conversion,[],[f1553]) ).
cnf(s299,plain,
( ~ spl0_26
| spl0_122
| ~ spl0_126 ),
inference(sat_conversion,[],[f1554]) ).
cnf(s300,plain,
( ~ spl0_113
| ~ spl0_120 ),
inference(sat_conversion,[],[f1555]) ).
cnf(s302,plain,
( spl0_17
| spl0_87
| spl0_89
| spl0_91
| spl0_93 ),
inference(sat_conversion,[],[f1561]) ).
cnf(s303,plain,
( spl0_3
| spl0_114
| spl0_115
| spl0_116
| spl0_117 ),
inference(sat_conversion,[],[f1564]) ).
cnf(s304,plain,
( ~ spl0_120
| ~ spl0_123 ),
inference(sat_conversion,[],[f1565]) ).
cnf(s305,plain,
( ~ spl0_113
| ~ spl0_123 ),
inference(sat_conversion,[],[f1566]) ).
cnf(s306,plain,
( ~ spl0_117
| ~ spl0_119 ),
inference(sat_conversion,[],[f1567]) ).
cnf(s307,plain,
( ~ spl0_117
| ~ spl0_122 ),
inference(sat_conversion,[],[f1568]) ).
cnf(s309,plain,
( ~ spl0_1
| ~ spl0_115 ),
inference(sat_conversion,[],[f1570]) ).
cnf(s310,plain,
( ~ spl0_115
| ~ spl0_121
| ~ spl0_128
| ~ spl0_131 ),
inference(sat_conversion,[],[f1571]) ).
cnf(s311,plain,
( ~ spl0_2
| ~ spl0_115
| ~ spl0_129
| ~ spl0_131 ),
inference(sat_conversion,[],[f1572]) ).
cnf(s312,plain,
( ~ spl0_107
| ~ spl0_115
| ~ spl0_131
| ~ spl0_135 ),
inference(sat_conversion,[],[f1573]) ).
cnf(s314,plain,
( ~ spl0_18
| ~ spl0_87 ),
inference(sat_conversion,[],[f1575]) ).
cnf(s315,plain,
( ~ spl0_2
| ~ spl0_114 ),
inference(sat_conversion,[],[f1576]) ).
cnf(s316,plain,
( ~ spl0_114
| ~ spl0_121 ),
inference(sat_conversion,[],[f1577]) ).
cnf(s317,plain,
( ~ spl0_1
| ~ spl0_114
| ~ spl0_128
| ~ spl0_131 ),
inference(sat_conversion,[],[f1578]) ).
cnf(s318,plain,
( ~ spl0_109
| ~ spl0_114
| ~ spl0_131
| ~ spl0_135 ),
inference(sat_conversion,[],[f1579]) ).
cnf(s319,plain,
( ~ spl0_108
| ~ spl0_114
| ~ spl0_131
| ~ spl0_133 ),
inference(sat_conversion,[],[f1580]) ).
cnf(s334,plain,
( ~ spl0_128
| ~ spl0_135
| spl0_178
| spl0_183
| spl0_192 ),
inference(sat_conversion,[],[f1651]) ).
cnf(s335,plain,
( ~ spl0_129
| ~ spl0_135
| spl0_180
| spl0_188
| spl0_192 ),
inference(sat_conversion,[],[f1652]) ).
cnf(s336,plain,
( ~ spl0_131
| ~ spl0_135
| spl0_181
| spl0_185
| spl0_192 ),
inference(sat_conversion,[],[f1653]) ).
cnf(s337,plain,
( ~ spl0_135
| spl0_182
| spl0_187
| spl0_192 ),
inference(sat_conversion,[],[f1654]) ).
cnf(s340,plain,
( ~ spl0_10
| spl0_109
| ~ spl0_149 ),
inference(sat_conversion,[],[f1669]) ).
cnf(s354,plain,
( ~ spl0_18
| ~ spl0_95 ),
inference(sat_conversion,[],[f1767]) ).
cnf(s359,plain,
( ~ spl0_99
| ~ spl0_102 ),
inference(sat_conversion,[],[f1775]) ).
cnf(s360,plain,
( ~ spl0_87
| ~ spl0_95 ),
inference(sat_conversion,[],[f1776]) ).
cnf(s361,plain,
( ~ spl0_20
| ~ spl0_105 ),
inference(sat_conversion,[],[f1777]) ).
cnf(s363,plain,
( ~ spl0_89
| ~ spl0_105 ),
inference(sat_conversion,[],[f1779]) ).
cnf(s364,plain,
~ spl0_159,
inference(sat_conversion,[],[f1781]) ).
cnf(s368,plain,
~ spl0_181,
inference(sat_conversion,[],[f1792]) ).
cnf(s377,plain,
~ spl0_177,
inference(sat_conversion,[],[f1806]) ).
cnf(s379,plain,
( ~ spl0_9
| ~ spl0_94
| ~ spl0_175 ),
inference(sat_conversion,[],[f1808]) ).
cnf(s380,plain,
( ~ spl0_42
| ~ spl0_94
| ~ spl0_167 ),
inference(sat_conversion,[],[f1809]) ).
cnf(s383,plain,
~ spl0_180,
inference(sat_conversion,[],[f1838]) ).
cnf(s385,plain,
~ spl0_161,
inference(sat_conversion,[],[f1841]) ).
cnf(s387,plain,
~ spl0_182,
inference(sat_conversion,[],[f1894]) ).
cnf(s388,plain,
( ~ spl0_10
| ~ spl0_96
| ~ spl0_187 ),
inference(sat_conversion,[],[f1905]) ).
cnf(s392,plain,
( ~ spl0_17
| ~ spl0_102 ),
inference(sat_conversion,[],[f1909]) ).
cnf(s394,plain,
~ spl0_178,
inference(sat_conversion,[],[f1912]) ).
cnf(s401,plain,
( ~ spl0_19
| ~ spl0_42
| ~ spl0_188 ),
inference(sat_conversion,[],[f1939]) ).
cnf(s402,plain,
( ~ spl0_30
| spl0_108
| ~ spl0_127 ),
inference(sat_conversion,[],[f1940]) ).
cnf(s403,plain,
( ~ spl0_6
| spl0_124
| ~ spl0_127 ),
inference(sat_conversion,[],[f1941]) ).
cnf(s405,plain,
( ~ spl0_42
| spl0_119
| ~ spl0_150 ),
inference(sat_conversion,[],[f1943]) ).
cnf(s406,plain,
( ~ spl0_14
| ~ spl0_42
| ~ spl0_166 ),
inference(sat_conversion,[],[f1944]) ).
cnf(s407,plain,
( ~ spl0_8
| ~ spl0_101
| ~ spl0_183 ),
inference(sat_conversion,[],[f1945]) ).
cnf(s415,plain,
( ~ spl0_40
| ~ spl0_41 ),
inference(sat_conversion,[],[f1953]) ).
cnf(s426,plain,
( ~ spl0_7
| spl0_117
| ~ spl0_151 ),
inference(sat_conversion,[],[f1964]) ).
cnf(s427,plain,
( ~ spl0_27
| spl0_122
| ~ spl0_151 ),
inference(sat_conversion,[],[f1965]) ).
cnf(s428,plain,
( ~ spl0_10
| ~ spl0_15
| ~ spl0_192 ),
inference(sat_conversion,[],[f1966]) ).
cnf(s436,plain,
( ~ spl0_6
| ~ spl0_70
| ~ spl0_166 ),
inference(sat_conversion,[],[f1977]) ).
cnf(s437,plain,
( ~ spl0_9
| ~ spl0_14
| ~ spl0_162 ),
inference(sat_conversion,[],[f1978]) ).
cnf(s443,plain,
( ~ spl0_45
| spl0_124
| ~ spl0_144 ),
inference(sat_conversion,[],[f1984]) ).
cnf(s446,plain,
( ~ spl0_41
| ~ spl0_101
| ~ spl0_185 ),
inference(sat_conversion,[],[f1987]) ).
cnf(s448,plain,
( ~ spl0_45
| ~ spl0_101
| ~ spl0_188 ),
inference(sat_conversion,[],[f1989]) ).
cnf(s451,plain,
( ~ spl0_29
| spl0_115
| ~ spl0_127 ),
inference(sat_conversion,[],[f1992]) ).
cnf(s453,plain,
( ~ spl0_8
| ~ spl0_105
| ~ spl0_158 ),
inference(sat_conversion,[],[f1994]) ).
cnf(s456,plain,
( ~ spl0_10
| ~ spl0_20
| ~ spl0_179 ),
inference(sat_conversion,[],[f1997]) ).
cnf(s458,plain,
( ~ spl0_27
| ~ spl0_91
| ~ spl0_183 ),
inference(sat_conversion,[],[f1999]) ).
cnf(s460,plain,
( ~ spl0_7
| spl0_115
| ~ spl0_145 ),
inference(sat_conversion,[],[f2001]) ).
cnf(s461,plain,
( spl0_1
| ~ spl0_27
| ~ spl0_145 ),
inference(sat_conversion,[],[f2002]) ).
cnf(s465,plain,
( ~ spl0_7
| ~ spl0_71
| ~ spl0_160 ),
inference(sat_conversion,[],[f2006]) ).
cnf(s466,plain,
( ~ spl0_29
| ~ spl0_70
| ~ spl0_160 ),
inference(sat_conversion,[],[f2007]) ).
cnf(s469,plain,
( ~ spl0_135
| spl0_187
| spl0_192 ),
inference(rat,[],[s337,s387]) ).
cnf(s470,plain,
( ~ spl0_131
| ~ spl0_135
| spl0_185
| spl0_192 ),
inference(rat,[],[s336,s368]) ).
cnf(s471,plain,
( ~ spl0_129
| ~ spl0_135
| spl0_188
| spl0_192 ),
inference(rat,[],[s335,s383]) ).
cnf(s472,plain,
( ~ spl0_128
| ~ spl0_135
| spl0_183
| spl0_192 ),
inference(rat,[],[s334,s394]) ).
cnf(s483,plain,
( ~ spl0_131
| ~ spl0_135
| spl0_160
| spl0_179 ),
inference(rat,[],[s279,s368]) ).
cnf(s484,plain,
( ~ spl0_129
| ~ spl0_135
| spl0_166
| spl0_179 ),
inference(rat,[],[s278,s383]) ).
cnf(s486,plain,
( ~ spl0_133
| spl0_162
| spl0_175 ),
inference(rat,[],[s276,s377]) ).
cnf(s493,plain,
( ~ spl0_129
| spl0_166
| spl0_167 ),
inference(rat,[],[s268,s281]) ).
cnf(s495,plain,
( ~ spl0_128
| ~ spl0_133
| spl0_158
| spl0_162 ),
inference(rat,[],[s266,s385]) ).
cnf(s496,plain,
( ~ spl0_128
| ~ spl0_131
| spl0_158
| spl0_160 ),
inference(rat,[],[s265,s364]) ).
cnf(s497,plain,
( ~ spl0_38
| ~ spl0_137 ),
inference(rat,[],[s183,s249]) ).
cnf(s499,plain,
( ~ spl0_10
| ~ spl0_139 ),
inference(rat,[],[s156,s158]) ).
cnf(s506,plain,
( ~ spl0_121
| ~ spl0_124 ),
inference(rat,[],[s114,s121,s157]) ).
cnf(s507,plain,
~ spl0_103,
inference(rat,[],[s83,s71]) ).
cnf(s508,plain,
~ spl0_100,
inference(rat,[],[s80,s71]) ).
cnf(s509,plain,
~ spl0_98,
inference(rat,[],[s77,s71]) ).
cnf(s510,plain,
~ spl0_93,
inference(rat,[],[s70,s71]) ).
cnf(s511,plain,
~ spl0_66,
inference(rat,[],[s228,s65]) ).
cnf(s512,plain,
~ spl0_77,
inference(rat,[],[s223,s65]) ).
cnf(s513,plain,
~ spl0_67,
inference(rat,[],[s222,s65]) ).
cnf(s514,plain,
~ spl0_79,
inference(rat,[],[s63,s65]) ).
cnf(s515,plain,
~ spl0_56,
inference(rat,[],[s184,s37]) ).
cnf(s516,plain,
~ spl0_50,
inference(rat,[],[s177,s37]) ).
cnf(s517,plain,
~ spl0_65,
inference(rat,[],[s43,s37]) ).
cnf(s518,plain,
~ spl0_49,
inference(rat,[],[s35,s37]) ).
cnf(s520,plain,
~ spl0_139,
inference(rat,[],[s499,s14]) ).
cnf(s521,plain,
~ spl0_33,
inference(rat,[],[s145,s14]) ).
cnf(s522,plain,
~ spl0_44,
inference(rat,[],[s20,s14]) ).
cnf(s523,plain,
~ spl0_43,
inference(rat,[],[s19,s14]) ).
cnf(s524,plain,
spl0_4,
inference(rat,[],[s153,s119,s520]) ).
cnf(s525,plain,
~ spl0_116,
inference(rat,[],[s126,s524]) ).
cnf(s526,plain,
~ spl0_118,
inference(rat,[],[s122,s524]) ).
cnf(s527,plain,
~ spl0_125,
inference(rat,[],[s120,s524]) ).
cnf(s528,plain,
~ spl0_110,
inference(rat,[],[s89,s524]) ).
cnf(s531,plain,
spl0_137,
inference(rat,[],[s148,s121,s526]) ).
cnf(s537,plain,
~ spl0_38,
inference(rat,[],[s497,s531]) ).
cnf(s538,plain,
~ spl0_55,
inference(rat,[],[s175,s537]) ).
cnf(s539,plain,
~ spl0_32,
inference(rat,[],[s13,s14]) ).
cnf(s540,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,s37,s71,s65,s14,s524]) ).
cnf(s542,plain,
( ~ spl0_109
| spl0_120
| spl0_3
| spl0_2 ),
inference(rat,[],[s306,s239,s303,s93,s253,s318,s526,s525,s123,s128]) ).
cnf(s543,plain,
( ~ spl0_112
| spl0_5
| spl0_3
| spl0_2
| spl0_1 ),
inference(rat,[],[s295,s239,s238,s257,s291,s241,s542,s91,s103,s106,s526,s527,s121,s128,s528]) ).
cnf(s544,plain,
( ~ spl0_109
| spl0_123
| spl0_3
| spl0_1 ),
inference(rat,[],[s307,s238,s303,s93,s296,s318,s527,s525,s157,s128,s123]) ).
cnf(s545,plain,
( ~ spl0_120
| spl0_5
| spl0_3
| spl0_1 ),
inference(rat,[],[s307,s303,s238,s92,s291,s312,s241,s544,s300,s304,s525,s527,s123,s128,s528]) ).
cnf(s546,plain,
( spl0_5
| spl0_3
| spl0_2
| spl0_1 ),
inference(rat,[],[s306,s303,s239,s92,s257,s312,s241,s305,s141,s134,s542,s143,s545,s173,s543,s137,s525,s526,s121,s128,s123,s528,s521]) ).
cnf(s547,plain,
( ~ spl0_109
| spl0_117
| spl0_3 ),
inference(rat,[],[s303,s93,s318,s525,s123,s128]) ).
cnf(s548,plain,
( ~ spl0_115
| ~ spl0_5
| spl0_2
| spl0_1 ),
inference(rat,[],[s304,s239,s238,s107,s310,s251,s244,s526,s527,s157,s123]) ).
cnf(s549,plain,
( ~ spl0_71
| spl0_81
| spl0_72
| spl0_84
| spl0_11 ),
inference(rat,[],[s58,s188,s186,s48,s52,s511,s514]) ).
cnf(s550,plain,
( ~ spl0_48
| spl0_61
| spl0_68
| spl0_84
| spl0_64
| spl0_11
| spl0_73
| spl0_39
| spl0_8
| spl0_108
| spl0_111
| spl0_117 ),
inference(rat,[],[s202,s188,s186,s47,s198,s189,s549,s211,s288,s132,s22,s131,s282,s167,s112,s163,s298,s16,s17,s39,s111,s511,s514,s513,s523,s522,s517]) ).
cnf(s551,plain,
( ~ spl0_54
| spl0_21
| spl0_73
| spl0_52
| spl0_26
| spl0_39
| spl0_8
| spl0_108
| spl0_115
| spl0_111
| spl0_117
| spl0_119
| spl0_22 ),
inference(rat,[],[s202,s188,s186,s47,s198,s189,s549,s211,s288,s132,s112,s415,s138,s248,s216,s133,s163,s402,s451,s40,s113,s165,s550,s23,s172,s166,s215,s110,s28,s41,s42,s207,s511,s514,s513,s523,s539,s517,s518,s516]) ).
cnf(s552,plain,
( ~ spl0_29
| ~ spl0_80
| spl0_36
| spl0_74
| spl0_11
| ~ spl0_27
| spl0_117 ),
inference(rat,[],[s363,s233,s302,s354,s360,s235,s448,s458,s388,s471,s472,s469,s428,s456,s187,s483,s201,s466,s188,s112,s131,s298,s17,s140,s225,s58,s359,s230,s229,s197,s507,s510,s509,s14,s128,s121,s157,s512,s123,s511,s522]) ).
cnf(s553,plain,
( ~ spl0_80
| ~ spl0_9
| spl0_74
| spl0_11
| ~ spl0_27
| spl0_117
| spl0_119 ),
inference(rat,[],[s363,s233,s302,s354,s360,s235,s446,s458,s388,s470,s472,s469,s428,s456,s187,s484,s201,s436,s188,s131,s112,s178,s248,s133,s552,s229,s230,s359,s58,s197,s225,s140,s2,s294,s135,s507,s510,s509,s14,s128,s123,s157,s512,s121,s511,s522,s539]) ).
cnf(s554,plain,
( ~ spl0_105
| spl0_91
| spl0_96
| spl0_17
| spl0_97 ),
inference(rat,[],[s360,s235,s302,s361,s363,s509,s510]) ).
cnf(s555,plain,
( ~ spl0_29
| spl0_75
| spl0_70
| spl0_36
| spl0_74
| spl0_11
| ~ spl0_27
| spl0_117 ),
inference(rat,[],[s72,s302,s235,s314,s354,s233,s554,s448,s458,s388,s471,s472,s469,s428,s187,s69,s76,s82,s55,s213,s188,s112,s131,s298,s17,s140,s510,s509,s507,s14,s128,s121,s157,s512,s511,s522]) ).
cnf(s556,plain,
( ~ spl0_9
| spl0_84
| spl0_74
| spl0_11
| ~ spl0_27
| spl0_111
| spl0_117
| spl0_119 ),
inference(rat,[],[s72,s302,s235,s314,s354,s233,s554,s446,s458,s388,s470,s472,s469,s428,s187,s69,s76,s82,s55,s213,s188,s131,s112,s178,s248,s133,s555,s195,s202,s186,s553,s211,s135,s288,s294,s140,s2,s510,s509,s507,s14,s128,s123,s157,s512,s511,s522,s539,s514]) ).
cnf(s558,plain,
( spl0_29
| spl0_9
| spl0_64
| spl0_46
| spl0_61
| spl0_21
| spl0_26
| spl0_39
| spl0_108 ),
inference(rat,[],[s132,s415,s138,s216,s133,s163,s402,s40,s113,s165,s111,s523,s539,s517,s518]) ).
cnf(s559,plain,
( spl0_21
| spl0_73
| spl0_52
| ~ spl0_27
| spl0_108
| spl0_115
| spl0_57
| spl0_111
| spl0_117
| spl0_119
| spl0_22 ),
inference(rat,[],[s282,s131,s167,s22,s163,s132,s216,s16,s17,s558,s556,s110,s208,s209,s166,s29,s169,s171,s164,s193,s551,s207,s140,s139,s2,s522,s517,s523,s516,s538,s515]) ).
cnf(s560,plain,
( spl0_73
| spl0_22
| spl0_52
| ~ spl0_27
| spl0_108
| spl0_115
| spl0_57
| spl0_111
| spl0_117
| spl0_119 ),
inference(rat,[],[s171,s166,s164,s27,s170,s559,s515,s538,s516]) ).
cnf(s561,plain,
( spl0_3
| spl0_2
| spl0_1 ),
inference(rat,[],[s560,s221,s180,s427,s461,s134,s173,s143,s106,s304,s238,s316,s319,s303,s548,s205,s340,s547,s90,s95,s244,s251,s546,s174,s137,s521,s527,s123,s119,s525,s14]) ).
cnf(s562,plain,
( ~ spl0_5
| spl0_2
| spl0_1 ),
inference(rat,[],[s506,s239,s238,s244,s251,s252,s243,s561,s526,s527]) ).
cnf(s563,plain,
( ~ spl0_124
| spl0_5
| spl0_113 ),
inference(rat,[],[s241,s253,s257,s528,s121,s128]) ).
cnf(s564,plain,
( spl0_2
| spl0_1 ),
inference(rat,[],[s241,s291,s296,s238,s295,s239,s563,s562,s96,s243,s252,s561,s526,s527,s128,s157,s528]) ).
cnf(s565,plain,
( ~ spl0_117
| spl0_1 ),
inference(rat,[],[s305,s241,s238,s95,s307,s290,s256,s255,s564,s528,s527,s128,s121]) ).
cnf(s566,plain,
spl0_1,
inference(rat,[],[s251,s241,s238,s96,s252,s303,s565,s255,s256,s290,s311,s315,s564,s528,s527,s525,s121,s128,s123]) ).
cnf(s567,plain,
~ spl0_114,
inference(rat,[],[s317,s123,s157,s566]) ).
cnf(s568,plain,
~ spl0_115,
inference(rat,[],[s309,s566]) ).
cnf(s570,plain,
~ spl0_108,
inference(rat,[],[s283,s566]) ).
cnf(s571,plain,
~ spl0_107,
inference(rat,[],[s258,s128,s157,s566]) ).
cnf(s572,plain,
~ spl0_109,
inference(rat,[],[s254,s566]) ).
cnf(s573,plain,
~ spl0_124,
inference(rat,[],[s242,s566]) ).
cnf(s574,plain,
~ spl0_149,
inference(rat,[],[s340,s14,s572]) ).
cnf(s575,plain,
~ spl0_57,
inference(rat,[],[s205,s574]) ).
cnf(s576,plain,
spl0_3,
inference(rat,[],[s134,s173,s143,s141,s91,s300,s305,s241,s95,s303,s137,s521,s571,s528,s572,s568,s525,s567]) ).
cnf(s577,plain,
~ spl0_123,
inference(rat,[],[s252,s576]) ).
cnf(s578,plain,
~ spl0_120,
inference(rat,[],[s243,s576]) ).
cnf(s579,plain,
~ spl0_112,
inference(rat,[],[s100,s576]) ).
cnf(s580,plain,
~ spl0_113,
inference(rat,[],[s96,s576]) ).
cnf(s581,plain,
~ spl0_27,
inference(rat,[],[s141,s577]) ).
cnf(s582,plain,
~ spl0_28,
inference(rat,[],[s143,s578]) ).
cnf(s583,plain,
~ spl0_31,
inference(rat,[],[s173,s579]) ).
cnf(s584,plain,
spl0_5,
inference(rat,[],[s241,s572,s528,s571,s580]) ).
cnf(s585,plain,
spl0_7,
inference(rat,[],[s134,s521,s583,s581,s582]) ).
cnf(s586,plain,
~ spl0_122,
inference(rat,[],[s251,s584]) ).
cnf(s587,plain,
~ spl0_119,
inference(rat,[],[s244,s584]) ).
cnf(s588,plain,
~ spl0_117,
inference(rat,[],[s95,s584]) ).
cnf(s589,plain,
~ spl0_111,
inference(rat,[],[s90,s584]) ).
cnf(s590,plain,
~ spl0_40,
inference(rat,[],[s262,s585]) ).
cnf(s591,plain,
~ spl0_41,
inference(rat,[],[s136,s585]) ).
cnf(s592,plain,
~ spl0_29,
inference(rat,[],[s4,s585]) ).
cnf(s593,plain,
~ spl0_145,
inference(rat,[],[s460,s568,s585]) ).
cnf(s594,plain,
~ spl0_151,
inference(rat,[],[s426,s588,s585]) ).
cnf(s595,plain,
spl0_2,
inference(rat,[],[s239,s573,s578,s526,s587]) ).
cnf(s596,plain,
~ spl0_62,
inference(rat,[],[s216,s591]) ).
cnf(s597,plain,
~ spl0_48,
inference(rat,[],[s111,s592]) ).
cnf(s598,plain,
~ spl0_52,
inference(rat,[],[s180,s593]) ).
cnf(s599,plain,
~ spl0_73,
inference(rat,[],[s221,s594]) ).
cnf(s601,plain,
( ~ spl0_25
| spl0_21
| spl0_22 ),
inference(rat,[],[s163,s40,s209,s165,s166,s29,s169,s171,s596,s517,s518,s597,s516,s598]) ).
cnf(s602,plain,
( spl0_21
| spl0_22 ),
inference(rat,[],[s40,s165,s163,s23,s172,s166,s28,s42,s164,s601,s575,s515,s538,s598,s516,s517,s596,s597,s518]) ).
cnf(s603,plain,
spl0_22,
inference(rat,[],[s171,s166,s164,s27,s170,s602,s516,s598,s538,s515,s575]) ).
cnf(s604,plain,
( spl0_81
| spl0_72
| spl0_84
| spl0_68
| spl0_11 ),
inference(rat,[],[s202,s188,s186,s47,s198,s189,s549,s511,s514,s513,s599]) ).
cnf(s605,plain,
( ~ spl0_25
| spl0_21 ),
inference(rat,[],[s132,s405,s288,s211,s604,s112,s110,s215,s15,s299,s44,s209,s133,s163,s403,s402,s40,s113,s165,s29,s169,s207,s590,s523,s587,s589,s586,s592,s539,s596,s517,s573,s570,s518,s597]) ).
cnf(s606,plain,
( ~ spl0_9
| spl0_21 ),
inference(rat,[],[s133,s299,s248,s112,s604,s211,s288,s294,s207,s110,s41,s215,s28,s164,s605,s592,s539,s586,s587,s589,s575,s515,s538]) ).
cnf(s607,plain,
( ~ spl0_150
| spl0_9 ),
inference(rat,[],[s132,s405,s293,s590,s523,s587,s586]) ).
cnf(s608,plain,
~ spl0_126,
inference(rat,[],[s299,s133,s297,s248,s586,s592,s539,s589,s587]) ).
cnf(s609,plain,
~ spl0_72,
inference(rat,[],[s112,s608]) ).
cnf(s610,plain,
spl0_21,
inference(rat,[],[s604,s215,s110,s211,s28,s41,s607,s164,s606,s605,s207,s609,s538,s515,s575]) ).
cnf(s611,plain,
~ spl0_63,
inference(rat,[],[s200,s610]) ).
cnf(s612,plain,
~ spl0_54,
inference(rat,[],[s170,s610]) ).
cnf(s613,plain,
~ spl0_64,
inference(rat,[],[s168,s610]) ).
cnf(s614,plain,
~ spl0_53,
inference(rat,[],[s27,s610]) ).
cnf(s615,plain,
~ spl0_84,
inference(rat,[],[s110,s611]) ).
cnf(s616,plain,
~ spl0_74,
inference(rat,[],[s193,s612]) ).
cnf(s617,plain,
spl0_25,
inference(rat,[],[s164,s575,s515,s538,s612]) ).
cnf(s618,plain,
~ spl0_68,
inference(rat,[],[s215,s614]) ).
cnf(s620,plain,
~ spl0_61,
inference(rat,[],[s169,s617]) ).
cnf(s622,plain,
spl0_23,
inference(rat,[],[s163,s517,s613,s596,s620]) ).
cnf(s623,plain,
spl0_144,
inference(rat,[],[s167,s622]) ).
cnf(s625,plain,
~ spl0_36,
inference(rat,[],[s282,s570,s623]) ).
cnf(s626,plain,
~ spl0_45,
inference(rat,[],[s443,s573,s623]) ).
cnf(s627,plain,
spl0_8,
inference(rat,[],[s131,s591,s522,s625,s626]) ).
cnf(s628,plain,
~ spl0_26,
inference(rat,[],[s144,s627]) ).
cnf(s629,plain,
~ spl0_39,
inference(rat,[],[s21,s627]) ).
cnf(s630,plain,
~ spl0_150,
inference(rat,[],[s607,s288,s589]) ).
cnf(s631,plain,
~ spl0_81,
inference(rat,[],[s211,s630]) ).
cnf(s632,plain,
spl0_11,
inference(rat,[],[s604,s615,s618,s609,s631]) ).
cnf(s633,plain,
( ~ spl0_14
| ~ spl0_9 ),
inference(rat,[],[s540,s234,s235,s85,s354,s233,s407,s388,s472,s469,s428,s229,s231,s392,s187,s192,s227,s453,s379,s189,s495,s486,s52,s195,s437,s133,s294,s566,s595,s576,s585,s584,s627,s632,s610,s603,s622,s617,s508,s509,s507,s14,s157,s128,s512,s616,s513,s618,s599,s119,s539,s628,s592]) ).
cnf(s634,plain,
~ spl0_80,
inference(rat,[],[s354,s233,s235,s407,s388,s472,s469,s428,s453,s456,s187,s496,s483,s51,s465,s230,s359,s189,s197,s198,s225,s507,s509,s627,s14,s157,s128,s512,s616,s123,s585,s513,s618,s599]) ).
cnf(s635,plain,
spl0_14,
inference(rat,[],[s186,s615,s631,s514,s634]) ).
cnf(s637,plain,
~ spl0_75,
inference(rat,[],[s195,s635]) ).
cnf(s639,plain,
~ spl0_71,
inference(rat,[],[s52,s635]) ).
cnf(s640,plain,
~ spl0_9,
inference(rat,[],[s633,s635]) ).
cnf(s641,plain,
spl0_12,
inference(rat,[],[s189,s599,s618,s513,s639]) ).
cnf(s642,plain,
spl0_42,
inference(rat,[],[s132,s523,s629,s590,s640]) ).
cnf(s643,plain,
~ spl0_78,
inference(rat,[],[s227,s641]) ).
cnf(s644,plain,
spl0_17,
inference(rat,[],[s192,s641]) ).
cnf(s646,plain,
~ spl0_166,
inference(rat,[],[s406,s635,s642]) ).
cnf(s649,plain,
spl0_15,
inference(rat,[],[s187,s616,s512,s637,s643]) ).
cnf(s651,plain,
~ spl0_97,
inference(rat,[],[s231,s644]) ).
cnf(s652,plain,
~ spl0_99,
inference(rat,[],[s229,s644]) ).
cnf(s654,plain,
spl0_167,
inference(rat,[],[s493,s121,s646]) ).
cnf(s655,plain,
spl0_179,
inference(rat,[],[s484,s121,s128,s646]) ).
cnf(s658,plain,
~ spl0_192,
inference(rat,[],[s428,s14,s649]) ).
cnf(s662,plain,
~ spl0_94,
inference(rat,[],[s380,s642,s654]) ).
cnf(s663,plain,
~ spl0_20,
inference(rat,[],[s456,s14,s655]) ).
cnf(s665,plain,
spl0_187,
inference(rat,[],[s469,s128,s658]) ).
cnf(s668,plain,
spl0_188,
inference(rat,[],[s471,s121,s128,s658]) ).
cnf(s670,plain,
~ spl0_96,
inference(rat,[],[s388,s14,s665]) ).
cnf(s673,plain,
~ spl0_19,
inference(rat,[],[s401,s642,s668]) ).
cnf(s674,plain,
spl0_95,
inference(rat,[],[s235,s509,s663,s651,s670]) ).
cnf(s675,plain,
spl0_104,
inference(rat,[],[s234,s652,s508,s662,s673]) ).
cnf(s679,plain,
$false,
inference(rat,[],[s84,s675,s674]) ).
fof(f2010,plain,
$false,
inference(avatar_sat_refutation,[],[s679]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % 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 THM
% 0.12/0.35 % Computer : n003.cluster.edu
% 0.12/0.35 % Model : x86_64 x86_64
% 0.12/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.35 % Memory : 8046.5625MB
% 0.12/0.35 % OS : Linux 6.8.0-71-generic
% 0.12/0.35 % CPULimit : 300
% 0.12/0.35 % WCLimit : 300
% 0.12/0.35 % DateTime : Sun Sep 27 22:30:57 UTC 2026
% 0.05/0.36 % CPUTime :
% 0.05/0.36 Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.05/0.39 Running first-order theorem proving
% 0.05/0.39 Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.00/1.28 % (982165)Input is clausal, will run a generic CNF schedule.
% 3.00/1.28 % (982178)lrs+1002_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=ground:npcc=on:sp=reverse_frequency:spb=intro:random_seed=882878880:i=137899:s2at=10:gtgl=3:kws=precedence:add=on:bd=preordered:gtg=position_2999 on theBenchmark for (2999ds/137899Mi)
% 3.00/1.28 % (982180)dis-1002_1_to=lpo:sil=16000:fd=off:random_seed=2090157915:st=1.5:i=114:aac=none:ins=7:ss=axioms:fsd=on_2999 on theBenchmark for (2999ds/114Mi)
% 3.00/1.28 % (982179)lrs+10_1_sil=8000:sp=occurrence:random_seed=1192150040:i=107:sd=3:ss=axioms:sgt=8_2999 on theBenchmark for (2999ds/107Mi)
% 3.00/1.28 % (982176)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:drc=off:sp=weighted_frequency:spb=goal:fd=preordered:foolp=on:random_seed=2063301193:i=140167_2999 on theBenchmark for (2999ds/140167Mi)
% 3.00/1.28 % (982177)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:npcc=on:urr=on:br=off:random_seed=924301711:i=132376:av=off_2999 on theBenchmark for (2999ds/132376Mi)
% 3.00/1.28 % (982181)dis-1011_1_sil=16000:fde=unused:s2agt=70:random_seed=4087994956:s2a=on:i=180:gtg=position_2999 on theBenchmark for (2999ds/180Mi)
% 3.00/1.28 % (982182)dis-21_1_sil=8000:lcm=predicate:random_seed=3973940907:st=5:avsq=on:i=117:avsqr=1,16:sd=3:aac=none:ep=RS:fsr=off:ss=included_2999 on theBenchmark for (2999ds/117Mi)
% 3.00/1.28 % (982182)First to succeed.
% 3.00/1.28 % (982180)Also succeeded, but the first one will report.
% 3.00/1.28 % (982182)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-982165"
% 3.00/1.28 % (982179)Also succeeded, but the first one will report.
% 3.00/1.28 % (982181)Also succeeded, but the first one will report.
% 3.00/1.28 % (982182)Refutation found. Thanks to Tanya!
% 3.00/1.28 % SZS status Unsatisfiable for theBenchmark
% 3.00/1.28 % SZS output start Proof for theBenchmark
% See solution above
% 3.72/1.47 % (982182)------------------------------
% 3.72/1.47 % (982182)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 3.72/1.47 % (982182)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 3.72/1.47 % (982182)CaDiCaL version: 2.1.3
% 3.72/1.47 % (982182)Termination reason: Refutation
% 3.72/1.47 % (982182)Time elapsed: 0.036 s
% 3.72/1.47 % (982182)Peak memory usage: 90 MB
% 3.72/1.47 % (982182)Instructions burned: 60 (million)
% 3.72/1.47 % (982182)------------------------------
% 3.72/1.47 % (982182)------------------------------
% 3.72/1.47 % (982165)Success in time 0.443 s
% 3.72/1.47 % Vampire exiting
%------------------------------------------------------------------------------