%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : NLP122+1 : TPTP v9.0.0. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n026.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Apr 9 07:48:18 PM UTC 2025
% Result : Theorem 8.47s 3.02s
% Output : CNFRefutation 9.26s
% Verified :
% SZS Type : Refutation
% Derivation depth : 8
% Number of leaves : 1
% Syntax : Number of formulae : 989 ( 412 unt; 0 typ; 0 def)
% Number of atoms : 3468 ( 0 equ)
% Maximal formula atoms : 68 ( 3 avg)
% Number of connectives : 4875 (2396 ~;2412 |; 65 &)
% ( 0 <=>; 2 =>; 0 <=; 0 <~>)
% Maximal formula depth : 45 ( 4 avg)
% Maximal term depth : 1 ( 1 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of predicates : 18 ( 17 usr; 1 prp; 0-3 aty)
% Number of functors : 10 ( 10 usr; 10 con; 0-0 aty)
% Number of variables : 596 ( 576 !; 20 ?; 0 :)
% Comments :
%------------------------------------------------------------------------------
%$ of > in > down > agent > white > street > present > placename > old > lonely > hollywood_placename > event > dirty > city > chevy > barrel > actual_world > #nlpp > #skF_7 > #skF_10 > #skF_5 > #skF_6 > #skF_2 > #skF_3 > #skF_1 > #skF_9 > #skF_8 > #skF_4
%Foreground sorts:
%Background operators:
%Foreground operators:
tff(placename,type,
placename: ( $i * $i ) > $o ).
tff(present,type,
present: ( $i * $i ) > $o ).
tff(in,type,
in: ( $i * $i * $i ) > $o ).
tff(old,type,
old: ( $i * $i ) > $o ).
tff(dirty,type,
dirty: ( $i * $i ) > $o ).
tff(city,type,
city: ( $i * $i ) > $o ).
tff(of,type,
of: ( $i * $i * $i ) > $o ).
tff('#skF_7',type,
'#skF_7': $i ).
tff(actual_world,type,
actual_world: $i > $o ).
tff(agent,type,
agent: ( $i * $i * $i ) > $o ).
tff('#skF_10',type,
'#skF_10': $i ).
tff('#skF_5',type,
'#skF_5': $i ).
tff(lonely,type,
lonely: ( $i * $i ) > $o ).
tff('#skF_6',type,
'#skF_6': $i ).
tff('#skF_2',type,
'#skF_2': $i ).
tff('#skF_3',type,
'#skF_3': $i ).
tff(event,type,
event: ( $i * $i ) > $o ).
tff('#skF_1',type,
'#skF_1': $i ).
tff(down,type,
down: ( $i * $i * $i ) > $o ).
tff(hollywood_placename,type,
hollywood_placename: ( $i * $i ) > $o ).
tff(white,type,
white: ( $i * $i ) > $o ).
tff('#skF_9',type,
'#skF_9': $i ).
tff(barrel,type,
barrel: ( $i * $i ) > $o ).
tff(street,type,
street: ( $i * $i ) > $o ).
tff('#skF_8',type,
'#skF_8': $i ).
tff('#skF_4',type,
'#skF_4': $i ).
tff(chevy,type,
chevy: ( $i * $i ) > $o ).
tff(f_173,negated_conjecture,
~ ~ ~ ( ( ? [U] :
( actual_world(U)
& ? [V,W,X,Y] :
( of(U,V,W)
& city(U,W)
& hollywood_placename(U,V)
& placename(U,V)
& chevy(U,W)
& white(U,W)
& dirty(U,W)
& old(U,W)
& street(U,X)
& lonely(U,X)
& event(U,Y)
& agent(U,Y,W)
& present(U,Y)
& barrel(U,Y)
& down(U,Y,X)
& in(U,Y,W) ) )
=> ? [Z] :
( actual_world(Z)
& ? [X1,X2,X3,X4] :
( street(Z,X1)
& lonely(Z,X1)
& of(Z,X2,X3)
& city(Z,X3)
& hollywood_placename(Z,X2)
& placename(Z,X2)
& chevy(Z,X3)
& white(Z,X3)
& dirty(Z,X3)
& old(Z,X3)
& event(Z,X4)
& agent(Z,X4,X3)
& present(Z,X4)
& barrel(Z,X4)
& down(Z,X4,X1)
& in(Z,X4,X3) ) ) )
& ( ? [Z] :
( actual_world(Z)
& ? [X1,X2,X3,X4] :
( street(Z,X1)
& lonely(Z,X1)
& of(Z,X2,X3)
& city(Z,X3)
& hollywood_placename(Z,X2)
& placename(Z,X2)
& chevy(Z,X3)
& white(Z,X3)
& dirty(Z,X3)
& old(Z,X3)
& event(Z,X4)
& agent(Z,X4,X3)
& present(Z,X4)
& barrel(Z,X4)
& down(Z,X4,X1)
& in(Z,X4,X3) ) )
=> ? [U] :
( actual_world(U)
& ? [V,W,X,Y] :
( of(U,V,W)
& city(U,W)
& hollywood_placename(U,V)
& placename(U,V)
& chevy(U,W)
& white(U,W)
& dirty(U,W)
& old(U,W)
& street(U,X)
& lonely(U,X)
& event(U,Y)
& agent(U,Y,W)
& present(U,Y)
& barrel(U,Y)
& down(U,Y,X)
& in(U,Y,W) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',co1) ).
tff(c_612,plain,
( actual_world('#skF_1')
| street('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_657,plain,
street('#skF_6','#skF_7'),
inference(splitLeft,[status(thm)],[c_612]) ).
tff(c_576,plain,
( actual_world('#skF_1')
| lonely('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_652,plain,
lonely('#skF_6','#skF_7'),
inference(splitLeft,[status(thm)],[c_576]) ).
tff(c_108,plain,
( actual_world('#skF_1')
| down('#skF_6','#skF_10','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_708,plain,
down('#skF_6','#skF_10','#skF_7'),
inference(splitLeft,[status(thm)],[c_108]) ).
tff(c_468,plain,
( actual_world('#skF_1')
| hollywood_placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_666,plain,
hollywood_placename('#skF_6','#skF_8'),
inference(splitLeft,[status(thm)],[c_468]) ).
tff(c_432,plain,
( actual_world('#skF_1')
| placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_671,plain,
placename('#skF_6','#skF_8'),
inference(splitLeft,[status(thm)],[c_432]) ).
tff(c_540,plain,
( actual_world('#skF_1')
| of('#skF_6','#skF_8','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_763,plain,
of('#skF_6','#skF_8','#skF_9'),
inference(splitLeft,[status(thm)],[c_540]) ).
tff(c_648,plain,
( actual_world('#skF_1')
| actual_world('#skF_6') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_649,plain,
actual_world('#skF_6'),
inference(splitLeft,[status(thm)],[c_648]) ).
tff(c_504,plain,
( actual_world('#skF_1')
| city('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_656,plain,
city('#skF_6','#skF_9'),
inference(splitLeft,[status(thm)],[c_504]) ).
tff(c_396,plain,
( actual_world('#skF_1')
| chevy('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_654,plain,
chevy('#skF_6','#skF_9'),
inference(splitLeft,[status(thm)],[c_396]) ).
tff(c_360,plain,
( actual_world('#skF_1')
| white('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_655,plain,
white('#skF_6','#skF_9'),
inference(splitLeft,[status(thm)],[c_360]) ).
tff(c_324,plain,
( actual_world('#skF_1')
| dirty('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_665,plain,
dirty('#skF_6','#skF_9'),
inference(splitLeft,[status(thm)],[c_324]) ).
tff(c_288,plain,
( actual_world('#skF_1')
| old('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_667,plain,
old('#skF_6','#skF_9'),
inference(splitLeft,[status(thm)],[c_288]) ).
tff(c_252,plain,
( actual_world('#skF_1')
| event('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_660,plain,
event('#skF_6','#skF_10'),
inference(splitLeft,[status(thm)],[c_252]) ).
tff(c_216,plain,
( actual_world('#skF_1')
| agent('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_792,plain,
agent('#skF_6','#skF_10','#skF_9'),
inference(splitLeft,[status(thm)],[c_216]) ).
tff(c_180,plain,
( actual_world('#skF_1')
| present('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_658,plain,
present('#skF_6','#skF_10'),
inference(splitLeft,[status(thm)],[c_180]) ).
tff(c_144,plain,
( actual_world('#skF_1')
| barrel('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_653,plain,
barrel('#skF_6','#skF_10'),
inference(splitLeft,[status(thm)],[c_144]) ).
tff(c_72,plain,
( actual_world('#skF_1')
| in('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_717,plain,
in('#skF_6','#skF_10','#skF_9'),
inference(splitLeft,[status(thm)],[c_72]) ).
tff(c_30,plain,
! [X_25,W_24,Y_26,U_18,V_23] :
( hollywood_placename('#skF_1','#skF_2')
| ~ in(U_18,Y_26,W_24)
| ~ down(U_18,Y_26,X_25)
| ~ barrel(U_18,Y_26)
| ~ present(U_18,Y_26)
| ~ agent(U_18,Y_26,W_24)
| ~ event(U_18,Y_26)
| ~ lonely(U_18,X_25)
| ~ street(U_18,X_25)
| ~ old(U_18,W_24)
| ~ dirty(U_18,W_24)
| ~ white(U_18,W_24)
| ~ chevy(U_18,W_24)
| ~ placename(U_18,V_23)
| ~ hollywood_placename(U_18,V_23)
| ~ city(U_18,W_24)
| ~ of(U_18,V_23,W_24)
| ~ actual_world(U_18) ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1241,plain,
! [Y_108,X_104,U_106,W_107,V_105] :
( ~ in(U_106,Y_108,W_107)
| ~ down(U_106,Y_108,X_104)
| ~ barrel(U_106,Y_108)
| ~ present(U_106,Y_108)
| ~ agent(U_106,Y_108,W_107)
| ~ event(U_106,Y_108)
| ~ lonely(U_106,X_104)
| ~ street(U_106,X_104)
| ~ old(U_106,W_107)
| ~ dirty(U_106,W_107)
| ~ white(U_106,W_107)
| ~ chevy(U_106,W_107)
| ~ placename(U_106,V_105)
| ~ hollywood_placename(U_106,V_105)
| ~ city(U_106,W_107)
| ~ of(U_106,V_105,W_107)
| ~ actual_world(U_106) ),
inference(splitLeft,[status(thm)],[c_30]) ).
tff(c_1243,plain,
! [X_104,V_105] :
( ~ down('#skF_6','#skF_10',X_104)
| ~ barrel('#skF_6','#skF_10')
| ~ present('#skF_6','#skF_10')
| ~ agent('#skF_6','#skF_10','#skF_9')
| ~ event('#skF_6','#skF_10')
| ~ lonely('#skF_6',X_104)
| ~ street('#skF_6',X_104)
| ~ old('#skF_6','#skF_9')
| ~ dirty('#skF_6','#skF_9')
| ~ white('#skF_6','#skF_9')
| ~ chevy('#skF_6','#skF_9')
| ~ placename('#skF_6',V_105)
| ~ hollywood_placename('#skF_6',V_105)
| ~ city('#skF_6','#skF_9')
| ~ of('#skF_6',V_105,'#skF_9')
| ~ actual_world('#skF_6') ),
inference(resolution,[status(thm)],[c_717,c_1241]) ).
tff(c_1246,plain,
! [X_104,V_105] :
( ~ down('#skF_6','#skF_10',X_104)
| ~ lonely('#skF_6',X_104)
| ~ street('#skF_6',X_104)
| ~ placename('#skF_6',V_105)
| ~ hollywood_placename('#skF_6',V_105)
| ~ of('#skF_6',V_105,'#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_649,c_656,c_654,c_655,c_665,c_667,c_660,c_792,c_658,c_653,c_1243]) ).
tff(c_1248,plain,
! [V_109] :
( ~ placename('#skF_6',V_109)
| ~ hollywood_placename('#skF_6',V_109)
| ~ of('#skF_6',V_109,'#skF_9') ),
inference(splitLeft,[status(thm)],[c_1246]) ).
tff(c_1251,plain,
( ~ placename('#skF_6','#skF_8')
| ~ hollywood_placename('#skF_6','#skF_8') ),
inference(resolution,[status(thm)],[c_763,c_1248]) ).
tff(c_1255,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_666,c_671,c_1251]) ).
tff(c_1257,plain,
! [X_110] :
( ~ down('#skF_6','#skF_10',X_110)
| ~ lonely('#skF_6',X_110)
| ~ street('#skF_6',X_110) ),
inference(splitRight,[status(thm)],[c_1246]) ).
tff(c_1260,plain,
( ~ lonely('#skF_6','#skF_7')
| ~ street('#skF_6','#skF_7') ),
inference(resolution,[status(thm)],[c_708,c_1257]) ).
tff(c_1264,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_657,c_652,c_1260]) ).
tff(c_1265,plain,
hollywood_placename('#skF_1','#skF_2'),
inference(splitRight,[status(thm)],[c_30]) ).
tff(c_28,plain,
! [X_25,W_24,Y_26,U_18,V_23] :
( placename('#skF_1','#skF_2')
| ~ in(U_18,Y_26,W_24)
| ~ down(U_18,Y_26,X_25)
| ~ barrel(U_18,Y_26)
| ~ present(U_18,Y_26)
| ~ agent(U_18,Y_26,W_24)
| ~ event(U_18,Y_26)
| ~ lonely(U_18,X_25)
| ~ street(U_18,X_25)
| ~ old(U_18,W_24)
| ~ dirty(U_18,W_24)
| ~ white(U_18,W_24)
| ~ chevy(U_18,W_24)
| ~ placename(U_18,V_23)
| ~ hollywood_placename(U_18,V_23)
| ~ city(U_18,W_24)
| ~ of(U_18,V_23,W_24)
| ~ actual_world(U_18) ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1215,plain,
! [X_97,U_99,Y_101,V_98,W_100] :
( ~ in(U_99,Y_101,W_100)
| ~ down(U_99,Y_101,X_97)
| ~ barrel(U_99,Y_101)
| ~ present(U_99,Y_101)
| ~ agent(U_99,Y_101,W_100)
| ~ event(U_99,Y_101)
| ~ lonely(U_99,X_97)
| ~ street(U_99,X_97)
| ~ old(U_99,W_100)
| ~ dirty(U_99,W_100)
| ~ white(U_99,W_100)
| ~ chevy(U_99,W_100)
| ~ placename(U_99,V_98)
| ~ hollywood_placename(U_99,V_98)
| ~ city(U_99,W_100)
| ~ of(U_99,V_98,W_100)
| ~ actual_world(U_99) ),
inference(splitLeft,[status(thm)],[c_28]) ).
tff(c_1217,plain,
! [X_97,V_98] :
( ~ down('#skF_6','#skF_10',X_97)
| ~ barrel('#skF_6','#skF_10')
| ~ present('#skF_6','#skF_10')
| ~ agent('#skF_6','#skF_10','#skF_9')
| ~ event('#skF_6','#skF_10')
| ~ lonely('#skF_6',X_97)
| ~ street('#skF_6',X_97)
| ~ old('#skF_6','#skF_9')
| ~ dirty('#skF_6','#skF_9')
| ~ white('#skF_6','#skF_9')
| ~ chevy('#skF_6','#skF_9')
| ~ placename('#skF_6',V_98)
| ~ hollywood_placename('#skF_6',V_98)
| ~ city('#skF_6','#skF_9')
| ~ of('#skF_6',V_98,'#skF_9')
| ~ actual_world('#skF_6') ),
inference(resolution,[status(thm)],[c_717,c_1215]) ).
tff(c_1220,plain,
! [X_97,V_98] :
( ~ down('#skF_6','#skF_10',X_97)
| ~ lonely('#skF_6',X_97)
| ~ street('#skF_6',X_97)
| ~ placename('#skF_6',V_98)
| ~ hollywood_placename('#skF_6',V_98)
| ~ of('#skF_6',V_98,'#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_649,c_656,c_654,c_655,c_665,c_667,c_660,c_792,c_658,c_653,c_1217]) ).
tff(c_1222,plain,
! [V_102] :
( ~ placename('#skF_6',V_102)
| ~ hollywood_placename('#skF_6',V_102)
| ~ of('#skF_6',V_102,'#skF_9') ),
inference(splitLeft,[status(thm)],[c_1220]) ).
tff(c_1225,plain,
( ~ placename('#skF_6','#skF_8')
| ~ hollywood_placename('#skF_6','#skF_8') ),
inference(resolution,[status(thm)],[c_763,c_1222]) ).
tff(c_1229,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_666,c_671,c_1225]) ).
tff(c_1231,plain,
! [X_103] :
( ~ down('#skF_6','#skF_10',X_103)
| ~ lonely('#skF_6',X_103)
| ~ street('#skF_6',X_103) ),
inference(splitRight,[status(thm)],[c_1220]) ).
tff(c_1234,plain,
( ~ lonely('#skF_6','#skF_7')
| ~ street('#skF_6','#skF_7') ),
inference(resolution,[status(thm)],[c_708,c_1231]) ).
tff(c_1238,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_657,c_652,c_1234]) ).
tff(c_1239,plain,
placename('#skF_1','#skF_2'),
inference(splitRight,[status(thm)],[c_28]) ).
tff(c_34,plain,
! [X_25,W_24,Y_26,U_18,V_23] :
( of('#skF_1','#skF_2','#skF_3')
| ~ in(U_18,Y_26,W_24)
| ~ down(U_18,Y_26,X_25)
| ~ barrel(U_18,Y_26)
| ~ present(U_18,Y_26)
| ~ agent(U_18,Y_26,W_24)
| ~ event(U_18,Y_26)
| ~ lonely(U_18,X_25)
| ~ street(U_18,X_25)
| ~ old(U_18,W_24)
| ~ dirty(U_18,W_24)
| ~ white(U_18,W_24)
| ~ chevy(U_18,W_24)
| ~ placename(U_18,V_23)
| ~ hollywood_placename(U_18,V_23)
| ~ city(U_18,W_24)
| ~ of(U_18,V_23,W_24)
| ~ actual_world(U_18) ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1321,plain,
! [U_127,V_126,X_125,W_128,Y_129] :
( ~ in(U_127,Y_129,W_128)
| ~ down(U_127,Y_129,X_125)
| ~ barrel(U_127,Y_129)
| ~ present(U_127,Y_129)
| ~ agent(U_127,Y_129,W_128)
| ~ event(U_127,Y_129)
| ~ lonely(U_127,X_125)
| ~ street(U_127,X_125)
| ~ old(U_127,W_128)
| ~ dirty(U_127,W_128)
| ~ white(U_127,W_128)
| ~ chevy(U_127,W_128)
| ~ placename(U_127,V_126)
| ~ hollywood_placename(U_127,V_126)
| ~ city(U_127,W_128)
| ~ of(U_127,V_126,W_128)
| ~ actual_world(U_127) ),
inference(splitLeft,[status(thm)],[c_34]) ).
tff(c_1323,plain,
! [X_125,V_126] :
( ~ down('#skF_6','#skF_10',X_125)
| ~ barrel('#skF_6','#skF_10')
| ~ present('#skF_6','#skF_10')
| ~ agent('#skF_6','#skF_10','#skF_9')
| ~ event('#skF_6','#skF_10')
| ~ lonely('#skF_6',X_125)
| ~ street('#skF_6',X_125)
| ~ old('#skF_6','#skF_9')
| ~ dirty('#skF_6','#skF_9')
| ~ white('#skF_6','#skF_9')
| ~ chevy('#skF_6','#skF_9')
| ~ placename('#skF_6',V_126)
| ~ hollywood_placename('#skF_6',V_126)
| ~ city('#skF_6','#skF_9')
| ~ of('#skF_6',V_126,'#skF_9')
| ~ actual_world('#skF_6') ),
inference(resolution,[status(thm)],[c_717,c_1321]) ).
tff(c_1326,plain,
! [X_125,V_126] :
( ~ down('#skF_6','#skF_10',X_125)
| ~ lonely('#skF_6',X_125)
| ~ street('#skF_6',X_125)
| ~ placename('#skF_6',V_126)
| ~ hollywood_placename('#skF_6',V_126)
| ~ of('#skF_6',V_126,'#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_649,c_656,c_654,c_655,c_665,c_667,c_660,c_792,c_658,c_653,c_1323]) ).
tff(c_1328,plain,
! [V_130] :
( ~ placename('#skF_6',V_130)
| ~ hollywood_placename('#skF_6',V_130)
| ~ of('#skF_6',V_130,'#skF_9') ),
inference(splitLeft,[status(thm)],[c_1326]) ).
tff(c_1331,plain,
( ~ placename('#skF_6','#skF_8')
| ~ hollywood_placename('#skF_6','#skF_8') ),
inference(resolution,[status(thm)],[c_763,c_1328]) ).
tff(c_1335,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_666,c_671,c_1331]) ).
tff(c_1337,plain,
! [X_131] :
( ~ down('#skF_6','#skF_10',X_131)
| ~ lonely('#skF_6',X_131)
| ~ street('#skF_6',X_131) ),
inference(splitRight,[status(thm)],[c_1326]) ).
tff(c_1340,plain,
( ~ lonely('#skF_6','#skF_7')
| ~ street('#skF_6','#skF_7') ),
inference(resolution,[status(thm)],[c_708,c_1337]) ).
tff(c_1344,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_657,c_652,c_1340]) ).
tff(c_1345,plain,
of('#skF_1','#skF_2','#skF_3'),
inference(splitRight,[status(thm)],[c_34]) ).
tff(c_18,plain,
! [X_25,W_24,Y_26,U_18,V_23] :
( street('#skF_1','#skF_4')
| ~ in(U_18,Y_26,W_24)
| ~ down(U_18,Y_26,X_25)
| ~ barrel(U_18,Y_26)
| ~ present(U_18,Y_26)
| ~ agent(U_18,Y_26,W_24)
| ~ event(U_18,Y_26)
| ~ lonely(U_18,X_25)
| ~ street(U_18,X_25)
| ~ old(U_18,W_24)
| ~ dirty(U_18,W_24)
| ~ white(U_18,W_24)
| ~ chevy(U_18,W_24)
| ~ placename(U_18,V_23)
| ~ hollywood_placename(U_18,V_23)
| ~ city(U_18,W_24)
| ~ of(U_18,V_23,W_24)
| ~ actual_world(U_18) ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1100,plain,
! [W_72,V_70,Y_73,U_71,X_69] :
( ~ in(U_71,Y_73,W_72)
| ~ down(U_71,Y_73,X_69)
| ~ barrel(U_71,Y_73)
| ~ present(U_71,Y_73)
| ~ agent(U_71,Y_73,W_72)
| ~ event(U_71,Y_73)
| ~ lonely(U_71,X_69)
| ~ street(U_71,X_69)
| ~ old(U_71,W_72)
| ~ dirty(U_71,W_72)
| ~ white(U_71,W_72)
| ~ chevy(U_71,W_72)
| ~ placename(U_71,V_70)
| ~ hollywood_placename(U_71,V_70)
| ~ city(U_71,W_72)
| ~ of(U_71,V_70,W_72)
| ~ actual_world(U_71) ),
inference(splitLeft,[status(thm)],[c_18]) ).
tff(c_1102,plain,
! [X_69,V_70] :
( ~ down('#skF_6','#skF_10',X_69)
| ~ barrel('#skF_6','#skF_10')
| ~ present('#skF_6','#skF_10')
| ~ agent('#skF_6','#skF_10','#skF_9')
| ~ event('#skF_6','#skF_10')
| ~ lonely('#skF_6',X_69)
| ~ street('#skF_6',X_69)
| ~ old('#skF_6','#skF_9')
| ~ dirty('#skF_6','#skF_9')
| ~ white('#skF_6','#skF_9')
| ~ chevy('#skF_6','#skF_9')
| ~ placename('#skF_6',V_70)
| ~ hollywood_placename('#skF_6',V_70)
| ~ city('#skF_6','#skF_9')
| ~ of('#skF_6',V_70,'#skF_9')
| ~ actual_world('#skF_6') ),
inference(resolution,[status(thm)],[c_717,c_1100]) ).
tff(c_1105,plain,
! [X_69,V_70] :
( ~ down('#skF_6','#skF_10',X_69)
| ~ lonely('#skF_6',X_69)
| ~ street('#skF_6',X_69)
| ~ placename('#skF_6',V_70)
| ~ hollywood_placename('#skF_6',V_70)
| ~ of('#skF_6',V_70,'#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_649,c_656,c_654,c_655,c_665,c_667,c_660,c_792,c_658,c_653,c_1102]) ).
tff(c_1107,plain,
! [V_74] :
( ~ placename('#skF_6',V_74)
| ~ hollywood_placename('#skF_6',V_74)
| ~ of('#skF_6',V_74,'#skF_9') ),
inference(splitLeft,[status(thm)],[c_1105]) ).
tff(c_1110,plain,
( ~ placename('#skF_6','#skF_8')
| ~ hollywood_placename('#skF_6','#skF_8') ),
inference(resolution,[status(thm)],[c_763,c_1107]) ).
tff(c_1114,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_666,c_671,c_1110]) ).
tff(c_1116,plain,
! [X_75] :
( ~ down('#skF_6','#skF_10',X_75)
| ~ lonely('#skF_6',X_75)
| ~ street('#skF_6',X_75) ),
inference(splitRight,[status(thm)],[c_1105]) ).
tff(c_1119,plain,
( ~ lonely('#skF_6','#skF_7')
| ~ street('#skF_6','#skF_7') ),
inference(resolution,[status(thm)],[c_708,c_1116]) ).
tff(c_1123,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_657,c_652,c_1119]) ).
tff(c_1124,plain,
street('#skF_1','#skF_4'),
inference(splitRight,[status(thm)],[c_18]) ).
tff(c_16,plain,
! [X_25,W_24,Y_26,U_18,V_23] :
( lonely('#skF_1','#skF_4')
| ~ in(U_18,Y_26,W_24)
| ~ down(U_18,Y_26,X_25)
| ~ barrel(U_18,Y_26)
| ~ present(U_18,Y_26)
| ~ agent(U_18,Y_26,W_24)
| ~ event(U_18,Y_26)
| ~ lonely(U_18,X_25)
| ~ street(U_18,X_25)
| ~ old(U_18,W_24)
| ~ dirty(U_18,W_24)
| ~ white(U_18,W_24)
| ~ chevy(U_18,W_24)
| ~ placename(U_18,V_23)
| ~ hollywood_placename(U_18,V_23)
| ~ city(U_18,W_24)
| ~ of(U_18,V_23,W_24)
| ~ actual_world(U_18) ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1133,plain,
! [X_76,U_78,W_79,V_77,Y_80] :
( ~ in(U_78,Y_80,W_79)
| ~ down(U_78,Y_80,X_76)
| ~ barrel(U_78,Y_80)
| ~ present(U_78,Y_80)
| ~ agent(U_78,Y_80,W_79)
| ~ event(U_78,Y_80)
| ~ lonely(U_78,X_76)
| ~ street(U_78,X_76)
| ~ old(U_78,W_79)
| ~ dirty(U_78,W_79)
| ~ white(U_78,W_79)
| ~ chevy(U_78,W_79)
| ~ placename(U_78,V_77)
| ~ hollywood_placename(U_78,V_77)
| ~ city(U_78,W_79)
| ~ of(U_78,V_77,W_79)
| ~ actual_world(U_78) ),
inference(splitLeft,[status(thm)],[c_16]) ).
tff(c_1135,plain,
! [X_76,V_77] :
( ~ down('#skF_6','#skF_10',X_76)
| ~ barrel('#skF_6','#skF_10')
| ~ present('#skF_6','#skF_10')
| ~ agent('#skF_6','#skF_10','#skF_9')
| ~ event('#skF_6','#skF_10')
| ~ lonely('#skF_6',X_76)
| ~ street('#skF_6',X_76)
| ~ old('#skF_6','#skF_9')
| ~ dirty('#skF_6','#skF_9')
| ~ white('#skF_6','#skF_9')
| ~ chevy('#skF_6','#skF_9')
| ~ placename('#skF_6',V_77)
| ~ hollywood_placename('#skF_6',V_77)
| ~ city('#skF_6','#skF_9')
| ~ of('#skF_6',V_77,'#skF_9')
| ~ actual_world('#skF_6') ),
inference(resolution,[status(thm)],[c_717,c_1133]) ).
tff(c_1138,plain,
! [X_76,V_77] :
( ~ down('#skF_6','#skF_10',X_76)
| ~ lonely('#skF_6',X_76)
| ~ street('#skF_6',X_76)
| ~ placename('#skF_6',V_77)
| ~ hollywood_placename('#skF_6',V_77)
| ~ of('#skF_6',V_77,'#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_649,c_656,c_654,c_655,c_665,c_667,c_660,c_792,c_658,c_653,c_1135]) ).
tff(c_1141,plain,
! [V_81] :
( ~ placename('#skF_6',V_81)
| ~ hollywood_placename('#skF_6',V_81)
| ~ of('#skF_6',V_81,'#skF_9') ),
inference(splitLeft,[status(thm)],[c_1138]) ).
tff(c_1144,plain,
( ~ placename('#skF_6','#skF_8')
| ~ hollywood_placename('#skF_6','#skF_8') ),
inference(resolution,[status(thm)],[c_763,c_1141]) ).
tff(c_1148,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_666,c_671,c_1144]) ).
tff(c_1150,plain,
! [X_82] :
( ~ down('#skF_6','#skF_10',X_82)
| ~ lonely('#skF_6',X_82)
| ~ street('#skF_6',X_82) ),
inference(splitRight,[status(thm)],[c_1138]) ).
tff(c_1153,plain,
( ~ lonely('#skF_6','#skF_7')
| ~ street('#skF_6','#skF_7') ),
inference(resolution,[status(thm)],[c_708,c_1150]) ).
tff(c_1157,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_657,c_652,c_1153]) ).
tff(c_1158,plain,
lonely('#skF_1','#skF_4'),
inference(splitRight,[status(thm)],[c_16]) ).
tff(c_6,plain,
! [X_25,W_24,Y_26,U_18,V_23] :
( down('#skF_1','#skF_5','#skF_4')
| ~ in(U_18,Y_26,W_24)
| ~ down(U_18,Y_26,X_25)
| ~ barrel(U_18,Y_26)
| ~ present(U_18,Y_26)
| ~ agent(U_18,Y_26,W_24)
| ~ event(U_18,Y_26)
| ~ lonely(U_18,X_25)
| ~ street(U_18,X_25)
| ~ old(U_18,W_24)
| ~ dirty(U_18,W_24)
| ~ white(U_18,W_24)
| ~ chevy(U_18,W_24)
| ~ placename(U_18,V_23)
| ~ hollywood_placename(U_18,V_23)
| ~ city(U_18,W_24)
| ~ of(U_18,V_23,W_24)
| ~ actual_world(U_18) ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1348,plain,
! [Y_136,V_133,U_134,X_132,W_135] :
( ~ in(U_134,Y_136,W_135)
| ~ down(U_134,Y_136,X_132)
| ~ barrel(U_134,Y_136)
| ~ present(U_134,Y_136)
| ~ agent(U_134,Y_136,W_135)
| ~ event(U_134,Y_136)
| ~ lonely(U_134,X_132)
| ~ street(U_134,X_132)
| ~ old(U_134,W_135)
| ~ dirty(U_134,W_135)
| ~ white(U_134,W_135)
| ~ chevy(U_134,W_135)
| ~ placename(U_134,V_133)
| ~ hollywood_placename(U_134,V_133)
| ~ city(U_134,W_135)
| ~ of(U_134,V_133,W_135)
| ~ actual_world(U_134) ),
inference(splitLeft,[status(thm)],[c_6]) ).
tff(c_1350,plain,
! [X_132,V_133] :
( ~ down('#skF_6','#skF_10',X_132)
| ~ barrel('#skF_6','#skF_10')
| ~ present('#skF_6','#skF_10')
| ~ agent('#skF_6','#skF_10','#skF_9')
| ~ event('#skF_6','#skF_10')
| ~ lonely('#skF_6',X_132)
| ~ street('#skF_6',X_132)
| ~ old('#skF_6','#skF_9')
| ~ dirty('#skF_6','#skF_9')
| ~ white('#skF_6','#skF_9')
| ~ chevy('#skF_6','#skF_9')
| ~ placename('#skF_6',V_133)
| ~ hollywood_placename('#skF_6',V_133)
| ~ city('#skF_6','#skF_9')
| ~ of('#skF_6',V_133,'#skF_9')
| ~ actual_world('#skF_6') ),
inference(resolution,[status(thm)],[c_717,c_1348]) ).
tff(c_1353,plain,
! [X_132,V_133] :
( ~ down('#skF_6','#skF_10',X_132)
| ~ lonely('#skF_6',X_132)
| ~ street('#skF_6',X_132)
| ~ placename('#skF_6',V_133)
| ~ hollywood_placename('#skF_6',V_133)
| ~ of('#skF_6',V_133,'#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_649,c_656,c_654,c_655,c_665,c_667,c_660,c_792,c_658,c_653,c_1350]) ).
tff(c_1355,plain,
! [V_137] :
( ~ placename('#skF_6',V_137)
| ~ hollywood_placename('#skF_6',V_137)
| ~ of('#skF_6',V_137,'#skF_9') ),
inference(splitLeft,[status(thm)],[c_1353]) ).
tff(c_1358,plain,
( ~ placename('#skF_6','#skF_8')
| ~ hollywood_placename('#skF_6','#skF_8') ),
inference(resolution,[status(thm)],[c_763,c_1355]) ).
tff(c_1362,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_666,c_671,c_1358]) ).
tff(c_1365,plain,
! [X_138] :
( ~ down('#skF_6','#skF_10',X_138)
| ~ lonely('#skF_6',X_138)
| ~ street('#skF_6',X_138) ),
inference(splitRight,[status(thm)],[c_1353]) ).
tff(c_1368,plain,
( ~ lonely('#skF_6','#skF_7')
| ~ street('#skF_6','#skF_7') ),
inference(resolution,[status(thm)],[c_708,c_1365]) ).
tff(c_1372,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_657,c_652,c_1368]) ).
tff(c_1373,plain,
down('#skF_1','#skF_5','#skF_4'),
inference(splitRight,[status(thm)],[c_6]) ).
tff(c_36,plain,
! [X_25,W_24,Y_26,U_18,V_23] :
( actual_world('#skF_1')
| ~ in(U_18,Y_26,W_24)
| ~ down(U_18,Y_26,X_25)
| ~ barrel(U_18,Y_26)
| ~ present(U_18,Y_26)
| ~ agent(U_18,Y_26,W_24)
| ~ event(U_18,Y_26)
| ~ lonely(U_18,X_25)
| ~ street(U_18,X_25)
| ~ old(U_18,W_24)
| ~ dirty(U_18,W_24)
| ~ white(U_18,W_24)
| ~ chevy(U_18,W_24)
| ~ placename(U_18,V_23)
| ~ hollywood_placename(U_18,V_23)
| ~ city(U_18,W_24)
| ~ of(U_18,V_23,W_24)
| ~ actual_world(U_18) ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_940,plain,
! [V_28,Y_31,U_29,W_30,X_27] :
( ~ in(U_29,Y_31,W_30)
| ~ down(U_29,Y_31,X_27)
| ~ barrel(U_29,Y_31)
| ~ present(U_29,Y_31)
| ~ agent(U_29,Y_31,W_30)
| ~ event(U_29,Y_31)
| ~ lonely(U_29,X_27)
| ~ street(U_29,X_27)
| ~ old(U_29,W_30)
| ~ dirty(U_29,W_30)
| ~ white(U_29,W_30)
| ~ chevy(U_29,W_30)
| ~ placename(U_29,V_28)
| ~ hollywood_placename(U_29,V_28)
| ~ city(U_29,W_30)
| ~ of(U_29,V_28,W_30)
| ~ actual_world(U_29) ),
inference(splitLeft,[status(thm)],[c_36]) ).
tff(c_942,plain,
! [X_27,V_28] :
( ~ down('#skF_6','#skF_10',X_27)
| ~ barrel('#skF_6','#skF_10')
| ~ present('#skF_6','#skF_10')
| ~ agent('#skF_6','#skF_10','#skF_9')
| ~ event('#skF_6','#skF_10')
| ~ lonely('#skF_6',X_27)
| ~ street('#skF_6',X_27)
| ~ old('#skF_6','#skF_9')
| ~ dirty('#skF_6','#skF_9')
| ~ white('#skF_6','#skF_9')
| ~ chevy('#skF_6','#skF_9')
| ~ placename('#skF_6',V_28)
| ~ hollywood_placename('#skF_6',V_28)
| ~ city('#skF_6','#skF_9')
| ~ of('#skF_6',V_28,'#skF_9')
| ~ actual_world('#skF_6') ),
inference(resolution,[status(thm)],[c_717,c_940]) ).
tff(c_945,plain,
! [X_27,V_28] :
( ~ down('#skF_6','#skF_10',X_27)
| ~ lonely('#skF_6',X_27)
| ~ street('#skF_6',X_27)
| ~ placename('#skF_6',V_28)
| ~ hollywood_placename('#skF_6',V_28)
| ~ of('#skF_6',V_28,'#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_649,c_656,c_654,c_655,c_665,c_667,c_660,c_792,c_658,c_653,c_942]) ).
tff(c_947,plain,
! [V_32] :
( ~ placename('#skF_6',V_32)
| ~ hollywood_placename('#skF_6',V_32)
| ~ of('#skF_6',V_32,'#skF_9') ),
inference(splitLeft,[status(thm)],[c_945]) ).
tff(c_950,plain,
( ~ placename('#skF_6','#skF_8')
| ~ hollywood_placename('#skF_6','#skF_8') ),
inference(resolution,[status(thm)],[c_763,c_947]) ).
tff(c_954,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_666,c_671,c_950]) ).
tff(c_956,plain,
! [X_33] :
( ~ down('#skF_6','#skF_10',X_33)
| ~ lonely('#skF_6',X_33)
| ~ street('#skF_6',X_33) ),
inference(splitRight,[status(thm)],[c_945]) ).
tff(c_959,plain,
( ~ lonely('#skF_6','#skF_7')
| ~ street('#skF_6','#skF_7') ),
inference(resolution,[status(thm)],[c_708,c_956]) ).
tff(c_963,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_657,c_652,c_959]) ).
tff(c_964,plain,
actual_world('#skF_1'),
inference(splitRight,[status(thm)],[c_36]) ).
tff(c_32,plain,
! [X_25,W_24,Y_26,U_18,V_23] :
( city('#skF_1','#skF_3')
| ~ in(U_18,Y_26,W_24)
| ~ down(U_18,Y_26,X_25)
| ~ barrel(U_18,Y_26)
| ~ present(U_18,Y_26)
| ~ agent(U_18,Y_26,W_24)
| ~ event(U_18,Y_26)
| ~ lonely(U_18,X_25)
| ~ street(U_18,X_25)
| ~ old(U_18,W_24)
| ~ dirty(U_18,W_24)
| ~ white(U_18,W_24)
| ~ chevy(U_18,W_24)
| ~ placename(U_18,V_23)
| ~ hollywood_placename(U_18,V_23)
| ~ city(U_18,W_24)
| ~ of(U_18,V_23,W_24)
| ~ actual_world(U_18) ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1020,plain,
! [V_49,X_48,U_50,W_51,Y_52] :
( ~ in(U_50,Y_52,W_51)
| ~ down(U_50,Y_52,X_48)
| ~ barrel(U_50,Y_52)
| ~ present(U_50,Y_52)
| ~ agent(U_50,Y_52,W_51)
| ~ event(U_50,Y_52)
| ~ lonely(U_50,X_48)
| ~ street(U_50,X_48)
| ~ old(U_50,W_51)
| ~ dirty(U_50,W_51)
| ~ white(U_50,W_51)
| ~ chevy(U_50,W_51)
| ~ placename(U_50,V_49)
| ~ hollywood_placename(U_50,V_49)
| ~ city(U_50,W_51)
| ~ of(U_50,V_49,W_51)
| ~ actual_world(U_50) ),
inference(splitLeft,[status(thm)],[c_32]) ).
tff(c_1022,plain,
! [X_48,V_49] :
( ~ down('#skF_6','#skF_10',X_48)
| ~ barrel('#skF_6','#skF_10')
| ~ present('#skF_6','#skF_10')
| ~ agent('#skF_6','#skF_10','#skF_9')
| ~ event('#skF_6','#skF_10')
| ~ lonely('#skF_6',X_48)
| ~ street('#skF_6',X_48)
| ~ old('#skF_6','#skF_9')
| ~ dirty('#skF_6','#skF_9')
| ~ white('#skF_6','#skF_9')
| ~ chevy('#skF_6','#skF_9')
| ~ placename('#skF_6',V_49)
| ~ hollywood_placename('#skF_6',V_49)
| ~ city('#skF_6','#skF_9')
| ~ of('#skF_6',V_49,'#skF_9')
| ~ actual_world('#skF_6') ),
inference(resolution,[status(thm)],[c_717,c_1020]) ).
tff(c_1025,plain,
! [X_48,V_49] :
( ~ down('#skF_6','#skF_10',X_48)
| ~ lonely('#skF_6',X_48)
| ~ street('#skF_6',X_48)
| ~ placename('#skF_6',V_49)
| ~ hollywood_placename('#skF_6',V_49)
| ~ of('#skF_6',V_49,'#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_649,c_656,c_654,c_655,c_665,c_667,c_660,c_792,c_658,c_653,c_1022]) ).
tff(c_1027,plain,
! [V_53] :
( ~ placename('#skF_6',V_53)
| ~ hollywood_placename('#skF_6',V_53)
| ~ of('#skF_6',V_53,'#skF_9') ),
inference(splitLeft,[status(thm)],[c_1025]) ).
tff(c_1030,plain,
( ~ placename('#skF_6','#skF_8')
| ~ hollywood_placename('#skF_6','#skF_8') ),
inference(resolution,[status(thm)],[c_763,c_1027]) ).
tff(c_1034,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_666,c_671,c_1030]) ).
tff(c_1036,plain,
! [X_54] :
( ~ down('#skF_6','#skF_10',X_54)
| ~ lonely('#skF_6',X_54)
| ~ street('#skF_6',X_54) ),
inference(splitRight,[status(thm)],[c_1025]) ).
tff(c_1039,plain,
( ~ lonely('#skF_6','#skF_7')
| ~ street('#skF_6','#skF_7') ),
inference(resolution,[status(thm)],[c_708,c_1036]) ).
tff(c_1043,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_657,c_652,c_1039]) ).
tff(c_1044,plain,
city('#skF_1','#skF_3'),
inference(splitRight,[status(thm)],[c_32]) ).
tff(c_26,plain,
! [X_25,W_24,Y_26,U_18,V_23] :
( chevy('#skF_1','#skF_3')
| ~ in(U_18,Y_26,W_24)
| ~ down(U_18,Y_26,X_25)
| ~ barrel(U_18,Y_26)
| ~ present(U_18,Y_26)
| ~ agent(U_18,Y_26,W_24)
| ~ event(U_18,Y_26)
| ~ lonely(U_18,X_25)
| ~ street(U_18,X_25)
| ~ old(U_18,W_24)
| ~ dirty(U_18,W_24)
| ~ white(U_18,W_24)
| ~ chevy(U_18,W_24)
| ~ placename(U_18,V_23)
| ~ hollywood_placename(U_18,V_23)
| ~ city(U_18,W_24)
| ~ of(U_18,V_23,W_24)
| ~ actual_world(U_18) ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1267,plain,
! [W_114,X_111,U_113,V_112,Y_115] :
( ~ in(U_113,Y_115,W_114)
| ~ down(U_113,Y_115,X_111)
| ~ barrel(U_113,Y_115)
| ~ present(U_113,Y_115)
| ~ agent(U_113,Y_115,W_114)
| ~ event(U_113,Y_115)
| ~ lonely(U_113,X_111)
| ~ street(U_113,X_111)
| ~ old(U_113,W_114)
| ~ dirty(U_113,W_114)
| ~ white(U_113,W_114)
| ~ chevy(U_113,W_114)
| ~ placename(U_113,V_112)
| ~ hollywood_placename(U_113,V_112)
| ~ city(U_113,W_114)
| ~ of(U_113,V_112,W_114)
| ~ actual_world(U_113) ),
inference(splitLeft,[status(thm)],[c_26]) ).
tff(c_1269,plain,
! [X_111,V_112] :
( ~ down('#skF_6','#skF_10',X_111)
| ~ barrel('#skF_6','#skF_10')
| ~ present('#skF_6','#skF_10')
| ~ agent('#skF_6','#skF_10','#skF_9')
| ~ event('#skF_6','#skF_10')
| ~ lonely('#skF_6',X_111)
| ~ street('#skF_6',X_111)
| ~ old('#skF_6','#skF_9')
| ~ dirty('#skF_6','#skF_9')
| ~ white('#skF_6','#skF_9')
| ~ chevy('#skF_6','#skF_9')
| ~ placename('#skF_6',V_112)
| ~ hollywood_placename('#skF_6',V_112)
| ~ city('#skF_6','#skF_9')
| ~ of('#skF_6',V_112,'#skF_9')
| ~ actual_world('#skF_6') ),
inference(resolution,[status(thm)],[c_717,c_1267]) ).
tff(c_1272,plain,
! [X_111,V_112] :
( ~ down('#skF_6','#skF_10',X_111)
| ~ lonely('#skF_6',X_111)
| ~ street('#skF_6',X_111)
| ~ placename('#skF_6',V_112)
| ~ hollywood_placename('#skF_6',V_112)
| ~ of('#skF_6',V_112,'#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_649,c_656,c_654,c_655,c_665,c_667,c_660,c_792,c_658,c_653,c_1269]) ).
tff(c_1274,plain,
! [V_116] :
( ~ placename('#skF_6',V_116)
| ~ hollywood_placename('#skF_6',V_116)
| ~ of('#skF_6',V_116,'#skF_9') ),
inference(splitLeft,[status(thm)],[c_1272]) ).
tff(c_1277,plain,
( ~ placename('#skF_6','#skF_8')
| ~ hollywood_placename('#skF_6','#skF_8') ),
inference(resolution,[status(thm)],[c_763,c_1274]) ).
tff(c_1281,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_666,c_671,c_1277]) ).
tff(c_1283,plain,
! [X_117] :
( ~ down('#skF_6','#skF_10',X_117)
| ~ lonely('#skF_6',X_117)
| ~ street('#skF_6',X_117) ),
inference(splitRight,[status(thm)],[c_1272]) ).
tff(c_1286,plain,
( ~ lonely('#skF_6','#skF_7')
| ~ street('#skF_6','#skF_7') ),
inference(resolution,[status(thm)],[c_708,c_1283]) ).
tff(c_1290,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_657,c_652,c_1286]) ).
tff(c_1291,plain,
chevy('#skF_1','#skF_3'),
inference(splitRight,[status(thm)],[c_26]) ).
tff(c_24,plain,
! [X_25,W_24,Y_26,U_18,V_23] :
( white('#skF_1','#skF_3')
| ~ in(U_18,Y_26,W_24)
| ~ down(U_18,Y_26,X_25)
| ~ barrel(U_18,Y_26)
| ~ present(U_18,Y_26)
| ~ agent(U_18,Y_26,W_24)
| ~ event(U_18,Y_26)
| ~ lonely(U_18,X_25)
| ~ street(U_18,X_25)
| ~ old(U_18,W_24)
| ~ dirty(U_18,W_24)
| ~ white(U_18,W_24)
| ~ chevy(U_18,W_24)
| ~ placename(U_18,V_23)
| ~ hollywood_placename(U_18,V_23)
| ~ city(U_18,W_24)
| ~ of(U_18,V_23,W_24)
| ~ actual_world(U_18) ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1046,plain,
! [W_58,V_56,U_57,X_55,Y_59] :
( ~ in(U_57,Y_59,W_58)
| ~ down(U_57,Y_59,X_55)
| ~ barrel(U_57,Y_59)
| ~ present(U_57,Y_59)
| ~ agent(U_57,Y_59,W_58)
| ~ event(U_57,Y_59)
| ~ lonely(U_57,X_55)
| ~ street(U_57,X_55)
| ~ old(U_57,W_58)
| ~ dirty(U_57,W_58)
| ~ white(U_57,W_58)
| ~ chevy(U_57,W_58)
| ~ placename(U_57,V_56)
| ~ hollywood_placename(U_57,V_56)
| ~ city(U_57,W_58)
| ~ of(U_57,V_56,W_58)
| ~ actual_world(U_57) ),
inference(splitLeft,[status(thm)],[c_24]) ).
tff(c_1048,plain,
! [X_55,V_56] :
( ~ down('#skF_6','#skF_10',X_55)
| ~ barrel('#skF_6','#skF_10')
| ~ present('#skF_6','#skF_10')
| ~ agent('#skF_6','#skF_10','#skF_9')
| ~ event('#skF_6','#skF_10')
| ~ lonely('#skF_6',X_55)
| ~ street('#skF_6',X_55)
| ~ old('#skF_6','#skF_9')
| ~ dirty('#skF_6','#skF_9')
| ~ white('#skF_6','#skF_9')
| ~ chevy('#skF_6','#skF_9')
| ~ placename('#skF_6',V_56)
| ~ hollywood_placename('#skF_6',V_56)
| ~ city('#skF_6','#skF_9')
| ~ of('#skF_6',V_56,'#skF_9')
| ~ actual_world('#skF_6') ),
inference(resolution,[status(thm)],[c_717,c_1046]) ).
tff(c_1051,plain,
! [X_55,V_56] :
( ~ down('#skF_6','#skF_10',X_55)
| ~ lonely('#skF_6',X_55)
| ~ street('#skF_6',X_55)
| ~ placename('#skF_6',V_56)
| ~ hollywood_placename('#skF_6',V_56)
| ~ of('#skF_6',V_56,'#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_649,c_656,c_654,c_655,c_665,c_667,c_660,c_792,c_658,c_653,c_1048]) ).
tff(c_1053,plain,
! [V_60] :
( ~ placename('#skF_6',V_60)
| ~ hollywood_placename('#skF_6',V_60)
| ~ of('#skF_6',V_60,'#skF_9') ),
inference(splitLeft,[status(thm)],[c_1051]) ).
tff(c_1056,plain,
( ~ placename('#skF_6','#skF_8')
| ~ hollywood_placename('#skF_6','#skF_8') ),
inference(resolution,[status(thm)],[c_763,c_1053]) ).
tff(c_1060,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_666,c_671,c_1056]) ).
tff(c_1062,plain,
! [X_61] :
( ~ down('#skF_6','#skF_10',X_61)
| ~ lonely('#skF_6',X_61)
| ~ street('#skF_6',X_61) ),
inference(splitRight,[status(thm)],[c_1051]) ).
tff(c_1065,plain,
( ~ lonely('#skF_6','#skF_7')
| ~ street('#skF_6','#skF_7') ),
inference(resolution,[status(thm)],[c_708,c_1062]) ).
tff(c_1069,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_657,c_652,c_1065]) ).
tff(c_1070,plain,
white('#skF_1','#skF_3'),
inference(splitRight,[status(thm)],[c_24]) ).
tff(c_22,plain,
! [X_25,W_24,Y_26,U_18,V_23] :
( dirty('#skF_1','#skF_3')
| ~ in(U_18,Y_26,W_24)
| ~ down(U_18,Y_26,X_25)
| ~ barrel(U_18,Y_26)
| ~ present(U_18,Y_26)
| ~ agent(U_18,Y_26,W_24)
| ~ event(U_18,Y_26)
| ~ lonely(U_18,X_25)
| ~ street(U_18,X_25)
| ~ old(U_18,W_24)
| ~ dirty(U_18,W_24)
| ~ white(U_18,W_24)
| ~ chevy(U_18,W_24)
| ~ placename(U_18,V_23)
| ~ hollywood_placename(U_18,V_23)
| ~ city(U_18,W_24)
| ~ of(U_18,V_23,W_24)
| ~ actual_world(U_18) ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_992,plain,
! [V_42,X_41,U_43,Y_45,W_44] :
( ~ in(U_43,Y_45,W_44)
| ~ down(U_43,Y_45,X_41)
| ~ barrel(U_43,Y_45)
| ~ present(U_43,Y_45)
| ~ agent(U_43,Y_45,W_44)
| ~ event(U_43,Y_45)
| ~ lonely(U_43,X_41)
| ~ street(U_43,X_41)
| ~ old(U_43,W_44)
| ~ dirty(U_43,W_44)
| ~ white(U_43,W_44)
| ~ chevy(U_43,W_44)
| ~ placename(U_43,V_42)
| ~ hollywood_placename(U_43,V_42)
| ~ city(U_43,W_44)
| ~ of(U_43,V_42,W_44)
| ~ actual_world(U_43) ),
inference(splitLeft,[status(thm)],[c_22]) ).
tff(c_994,plain,
! [X_41,V_42] :
( ~ down('#skF_6','#skF_10',X_41)
| ~ barrel('#skF_6','#skF_10')
| ~ present('#skF_6','#skF_10')
| ~ agent('#skF_6','#skF_10','#skF_9')
| ~ event('#skF_6','#skF_10')
| ~ lonely('#skF_6',X_41)
| ~ street('#skF_6',X_41)
| ~ old('#skF_6','#skF_9')
| ~ dirty('#skF_6','#skF_9')
| ~ white('#skF_6','#skF_9')
| ~ chevy('#skF_6','#skF_9')
| ~ placename('#skF_6',V_42)
| ~ hollywood_placename('#skF_6',V_42)
| ~ city('#skF_6','#skF_9')
| ~ of('#skF_6',V_42,'#skF_9')
| ~ actual_world('#skF_6') ),
inference(resolution,[status(thm)],[c_717,c_992]) ).
tff(c_997,plain,
! [X_41,V_42] :
( ~ down('#skF_6','#skF_10',X_41)
| ~ lonely('#skF_6',X_41)
| ~ street('#skF_6',X_41)
| ~ placename('#skF_6',V_42)
| ~ hollywood_placename('#skF_6',V_42)
| ~ of('#skF_6',V_42,'#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_649,c_656,c_654,c_655,c_665,c_667,c_660,c_792,c_658,c_653,c_994]) ).
tff(c_999,plain,
! [V_46] :
( ~ placename('#skF_6',V_46)
| ~ hollywood_placename('#skF_6',V_46)
| ~ of('#skF_6',V_46,'#skF_9') ),
inference(splitLeft,[status(thm)],[c_997]) ).
tff(c_1002,plain,
( ~ placename('#skF_6','#skF_8')
| ~ hollywood_placename('#skF_6','#skF_8') ),
inference(resolution,[status(thm)],[c_763,c_999]) ).
tff(c_1006,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_666,c_671,c_1002]) ).
tff(c_1008,plain,
! [X_47] :
( ~ down('#skF_6','#skF_10',X_47)
| ~ lonely('#skF_6',X_47)
| ~ street('#skF_6',X_47) ),
inference(splitRight,[status(thm)],[c_997]) ).
tff(c_1011,plain,
( ~ lonely('#skF_6','#skF_7')
| ~ street('#skF_6','#skF_7') ),
inference(resolution,[status(thm)],[c_708,c_1008]) ).
tff(c_1015,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_657,c_652,c_1011]) ).
tff(c_1016,plain,
dirty('#skF_1','#skF_3'),
inference(splitRight,[status(thm)],[c_22]) ).
tff(c_20,plain,
! [X_25,W_24,Y_26,U_18,V_23] :
( old('#skF_1','#skF_3')
| ~ in(U_18,Y_26,W_24)
| ~ down(U_18,Y_26,X_25)
| ~ barrel(U_18,Y_26)
| ~ present(U_18,Y_26)
| ~ agent(U_18,Y_26,W_24)
| ~ event(U_18,Y_26)
| ~ lonely(U_18,X_25)
| ~ street(U_18,X_25)
| ~ old(U_18,W_24)
| ~ dirty(U_18,W_24)
| ~ white(U_18,W_24)
| ~ chevy(U_18,W_24)
| ~ placename(U_18,V_23)
| ~ hollywood_placename(U_18,V_23)
| ~ city(U_18,W_24)
| ~ of(U_18,V_23,W_24)
| ~ actual_world(U_18) ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1161,plain,
! [W_86,Y_87,X_83,V_84,U_85] :
( ~ in(U_85,Y_87,W_86)
| ~ down(U_85,Y_87,X_83)
| ~ barrel(U_85,Y_87)
| ~ present(U_85,Y_87)
| ~ agent(U_85,Y_87,W_86)
| ~ event(U_85,Y_87)
| ~ lonely(U_85,X_83)
| ~ street(U_85,X_83)
| ~ old(U_85,W_86)
| ~ dirty(U_85,W_86)
| ~ white(U_85,W_86)
| ~ chevy(U_85,W_86)
| ~ placename(U_85,V_84)
| ~ hollywood_placename(U_85,V_84)
| ~ city(U_85,W_86)
| ~ of(U_85,V_84,W_86)
| ~ actual_world(U_85) ),
inference(splitLeft,[status(thm)],[c_20]) ).
tff(c_1163,plain,
! [X_83,V_84] :
( ~ down('#skF_6','#skF_10',X_83)
| ~ barrel('#skF_6','#skF_10')
| ~ present('#skF_6','#skF_10')
| ~ agent('#skF_6','#skF_10','#skF_9')
| ~ event('#skF_6','#skF_10')
| ~ lonely('#skF_6',X_83)
| ~ street('#skF_6',X_83)
| ~ old('#skF_6','#skF_9')
| ~ dirty('#skF_6','#skF_9')
| ~ white('#skF_6','#skF_9')
| ~ chevy('#skF_6','#skF_9')
| ~ placename('#skF_6',V_84)
| ~ hollywood_placename('#skF_6',V_84)
| ~ city('#skF_6','#skF_9')
| ~ of('#skF_6',V_84,'#skF_9')
| ~ actual_world('#skF_6') ),
inference(resolution,[status(thm)],[c_717,c_1161]) ).
tff(c_1166,plain,
! [X_83,V_84] :
( ~ down('#skF_6','#skF_10',X_83)
| ~ lonely('#skF_6',X_83)
| ~ street('#skF_6',X_83)
| ~ placename('#skF_6',V_84)
| ~ hollywood_placename('#skF_6',V_84)
| ~ of('#skF_6',V_84,'#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_649,c_656,c_654,c_655,c_665,c_667,c_660,c_792,c_658,c_653,c_1163]) ).
tff(c_1168,plain,
! [V_88] :
( ~ placename('#skF_6',V_88)
| ~ hollywood_placename('#skF_6',V_88)
| ~ of('#skF_6',V_88,'#skF_9') ),
inference(splitLeft,[status(thm)],[c_1166]) ).
tff(c_1171,plain,
( ~ placename('#skF_6','#skF_8')
| ~ hollywood_placename('#skF_6','#skF_8') ),
inference(resolution,[status(thm)],[c_763,c_1168]) ).
tff(c_1175,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_666,c_671,c_1171]) ).
tff(c_1178,plain,
! [X_89] :
( ~ down('#skF_6','#skF_10',X_89)
| ~ lonely('#skF_6',X_89)
| ~ street('#skF_6',X_89) ),
inference(splitRight,[status(thm)],[c_1166]) ).
tff(c_1181,plain,
( ~ lonely('#skF_6','#skF_7')
| ~ street('#skF_6','#skF_7') ),
inference(resolution,[status(thm)],[c_708,c_1178]) ).
tff(c_1185,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_657,c_652,c_1181]) ).
tff(c_1186,plain,
old('#skF_1','#skF_3'),
inference(splitRight,[status(thm)],[c_20]) ).
tff(c_14,plain,
! [X_25,W_24,Y_26,U_18,V_23] :
( event('#skF_1','#skF_5')
| ~ in(U_18,Y_26,W_24)
| ~ down(U_18,Y_26,X_25)
| ~ barrel(U_18,Y_26)
| ~ present(U_18,Y_26)
| ~ agent(U_18,Y_26,W_24)
| ~ event(U_18,Y_26)
| ~ lonely(U_18,X_25)
| ~ street(U_18,X_25)
| ~ old(U_18,W_24)
| ~ dirty(U_18,W_24)
| ~ white(U_18,W_24)
| ~ chevy(U_18,W_24)
| ~ placename(U_18,V_23)
| ~ hollywood_placename(U_18,V_23)
| ~ city(U_18,W_24)
| ~ of(U_18,V_23,W_24)
| ~ actual_world(U_18) ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1072,plain,
! [V_63,U_64,W_65,Y_66,X_62] :
( ~ in(U_64,Y_66,W_65)
| ~ down(U_64,Y_66,X_62)
| ~ barrel(U_64,Y_66)
| ~ present(U_64,Y_66)
| ~ agent(U_64,Y_66,W_65)
| ~ event(U_64,Y_66)
| ~ lonely(U_64,X_62)
| ~ street(U_64,X_62)
| ~ old(U_64,W_65)
| ~ dirty(U_64,W_65)
| ~ white(U_64,W_65)
| ~ chevy(U_64,W_65)
| ~ placename(U_64,V_63)
| ~ hollywood_placename(U_64,V_63)
| ~ city(U_64,W_65)
| ~ of(U_64,V_63,W_65)
| ~ actual_world(U_64) ),
inference(splitLeft,[status(thm)],[c_14]) ).
tff(c_1074,plain,
! [X_62,V_63] :
( ~ down('#skF_6','#skF_10',X_62)
| ~ barrel('#skF_6','#skF_10')
| ~ present('#skF_6','#skF_10')
| ~ agent('#skF_6','#skF_10','#skF_9')
| ~ event('#skF_6','#skF_10')
| ~ lonely('#skF_6',X_62)
| ~ street('#skF_6',X_62)
| ~ old('#skF_6','#skF_9')
| ~ dirty('#skF_6','#skF_9')
| ~ white('#skF_6','#skF_9')
| ~ chevy('#skF_6','#skF_9')
| ~ placename('#skF_6',V_63)
| ~ hollywood_placename('#skF_6',V_63)
| ~ city('#skF_6','#skF_9')
| ~ of('#skF_6',V_63,'#skF_9')
| ~ actual_world('#skF_6') ),
inference(resolution,[status(thm)],[c_717,c_1072]) ).
tff(c_1077,plain,
! [X_62,V_63] :
( ~ down('#skF_6','#skF_10',X_62)
| ~ lonely('#skF_6',X_62)
| ~ street('#skF_6',X_62)
| ~ placename('#skF_6',V_63)
| ~ hollywood_placename('#skF_6',V_63)
| ~ of('#skF_6',V_63,'#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_649,c_656,c_654,c_655,c_665,c_667,c_660,c_792,c_658,c_653,c_1074]) ).
tff(c_1080,plain,
! [V_67] :
( ~ placename('#skF_6',V_67)
| ~ hollywood_placename('#skF_6',V_67)
| ~ of('#skF_6',V_67,'#skF_9') ),
inference(splitLeft,[status(thm)],[c_1077]) ).
tff(c_1083,plain,
( ~ placename('#skF_6','#skF_8')
| ~ hollywood_placename('#skF_6','#skF_8') ),
inference(resolution,[status(thm)],[c_763,c_1080]) ).
tff(c_1087,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_666,c_671,c_1083]) ).
tff(c_1089,plain,
! [X_68] :
( ~ down('#skF_6','#skF_10',X_68)
| ~ lonely('#skF_6',X_68)
| ~ street('#skF_6',X_68) ),
inference(splitRight,[status(thm)],[c_1077]) ).
tff(c_1092,plain,
( ~ lonely('#skF_6','#skF_7')
| ~ street('#skF_6','#skF_7') ),
inference(resolution,[status(thm)],[c_708,c_1089]) ).
tff(c_1096,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_657,c_652,c_1092]) ).
tff(c_1097,plain,
event('#skF_1','#skF_5'),
inference(splitRight,[status(thm)],[c_14]) ).
tff(c_12,plain,
! [X_25,W_24,Y_26,U_18,V_23] :
( agent('#skF_1','#skF_5','#skF_3')
| ~ in(U_18,Y_26,W_24)
| ~ down(U_18,Y_26,X_25)
| ~ barrel(U_18,Y_26)
| ~ present(U_18,Y_26)
| ~ agent(U_18,Y_26,W_24)
| ~ event(U_18,Y_26)
| ~ lonely(U_18,X_25)
| ~ street(U_18,X_25)
| ~ old(U_18,W_24)
| ~ dirty(U_18,W_24)
| ~ white(U_18,W_24)
| ~ chevy(U_18,W_24)
| ~ placename(U_18,V_23)
| ~ hollywood_placename(U_18,V_23)
| ~ city(U_18,W_24)
| ~ of(U_18,V_23,W_24)
| ~ actual_world(U_18) ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1295,plain,
! [W_121,V_119,Y_122,U_120,X_118] :
( ~ in(U_120,Y_122,W_121)
| ~ down(U_120,Y_122,X_118)
| ~ barrel(U_120,Y_122)
| ~ present(U_120,Y_122)
| ~ agent(U_120,Y_122,W_121)
| ~ event(U_120,Y_122)
| ~ lonely(U_120,X_118)
| ~ street(U_120,X_118)
| ~ old(U_120,W_121)
| ~ dirty(U_120,W_121)
| ~ white(U_120,W_121)
| ~ chevy(U_120,W_121)
| ~ placename(U_120,V_119)
| ~ hollywood_placename(U_120,V_119)
| ~ city(U_120,W_121)
| ~ of(U_120,V_119,W_121)
| ~ actual_world(U_120) ),
inference(splitLeft,[status(thm)],[c_12]) ).
tff(c_1297,plain,
! [X_118,V_119] :
( ~ down('#skF_6','#skF_10',X_118)
| ~ barrel('#skF_6','#skF_10')
| ~ present('#skF_6','#skF_10')
| ~ agent('#skF_6','#skF_10','#skF_9')
| ~ event('#skF_6','#skF_10')
| ~ lonely('#skF_6',X_118)
| ~ street('#skF_6',X_118)
| ~ old('#skF_6','#skF_9')
| ~ dirty('#skF_6','#skF_9')
| ~ white('#skF_6','#skF_9')
| ~ chevy('#skF_6','#skF_9')
| ~ placename('#skF_6',V_119)
| ~ hollywood_placename('#skF_6',V_119)
| ~ city('#skF_6','#skF_9')
| ~ of('#skF_6',V_119,'#skF_9')
| ~ actual_world('#skF_6') ),
inference(resolution,[status(thm)],[c_717,c_1295]) ).
tff(c_1300,plain,
! [X_118,V_119] :
( ~ down('#skF_6','#skF_10',X_118)
| ~ lonely('#skF_6',X_118)
| ~ street('#skF_6',X_118)
| ~ placename('#skF_6',V_119)
| ~ hollywood_placename('#skF_6',V_119)
| ~ of('#skF_6',V_119,'#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_649,c_656,c_654,c_655,c_665,c_667,c_660,c_792,c_658,c_653,c_1297]) ).
tff(c_1302,plain,
! [V_123] :
( ~ placename('#skF_6',V_123)
| ~ hollywood_placename('#skF_6',V_123)
| ~ of('#skF_6',V_123,'#skF_9') ),
inference(splitLeft,[status(thm)],[c_1300]) ).
tff(c_1305,plain,
( ~ placename('#skF_6','#skF_8')
| ~ hollywood_placename('#skF_6','#skF_8') ),
inference(resolution,[status(thm)],[c_763,c_1302]) ).
tff(c_1309,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_666,c_671,c_1305]) ).
tff(c_1311,plain,
! [X_124] :
( ~ down('#skF_6','#skF_10',X_124)
| ~ lonely('#skF_6',X_124)
| ~ street('#skF_6',X_124) ),
inference(splitRight,[status(thm)],[c_1300]) ).
tff(c_1314,plain,
( ~ lonely('#skF_6','#skF_7')
| ~ street('#skF_6','#skF_7') ),
inference(resolution,[status(thm)],[c_708,c_1311]) ).
tff(c_1318,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_657,c_652,c_1314]) ).
tff(c_1319,plain,
agent('#skF_1','#skF_5','#skF_3'),
inference(splitRight,[status(thm)],[c_12]) ).
tff(c_10,plain,
! [X_25,W_24,Y_26,U_18,V_23] :
( present('#skF_1','#skF_5')
| ~ in(U_18,Y_26,W_24)
| ~ down(U_18,Y_26,X_25)
| ~ barrel(U_18,Y_26)
| ~ present(U_18,Y_26)
| ~ agent(U_18,Y_26,W_24)
| ~ event(U_18,Y_26)
| ~ lonely(U_18,X_25)
| ~ street(U_18,X_25)
| ~ old(U_18,W_24)
| ~ dirty(U_18,W_24)
| ~ white(U_18,W_24)
| ~ chevy(U_18,W_24)
| ~ placename(U_18,V_23)
| ~ hollywood_placename(U_18,V_23)
| ~ city(U_18,W_24)
| ~ of(U_18,V_23,W_24)
| ~ actual_world(U_18) ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_966,plain,
! [V_35,U_36,Y_38,X_34,W_37] :
( ~ in(U_36,Y_38,W_37)
| ~ down(U_36,Y_38,X_34)
| ~ barrel(U_36,Y_38)
| ~ present(U_36,Y_38)
| ~ agent(U_36,Y_38,W_37)
| ~ event(U_36,Y_38)
| ~ lonely(U_36,X_34)
| ~ street(U_36,X_34)
| ~ old(U_36,W_37)
| ~ dirty(U_36,W_37)
| ~ white(U_36,W_37)
| ~ chevy(U_36,W_37)
| ~ placename(U_36,V_35)
| ~ hollywood_placename(U_36,V_35)
| ~ city(U_36,W_37)
| ~ of(U_36,V_35,W_37)
| ~ actual_world(U_36) ),
inference(splitLeft,[status(thm)],[c_10]) ).
tff(c_968,plain,
! [X_34,V_35] :
( ~ down('#skF_6','#skF_10',X_34)
| ~ barrel('#skF_6','#skF_10')
| ~ present('#skF_6','#skF_10')
| ~ agent('#skF_6','#skF_10','#skF_9')
| ~ event('#skF_6','#skF_10')
| ~ lonely('#skF_6',X_34)
| ~ street('#skF_6',X_34)
| ~ old('#skF_6','#skF_9')
| ~ dirty('#skF_6','#skF_9')
| ~ white('#skF_6','#skF_9')
| ~ chevy('#skF_6','#skF_9')
| ~ placename('#skF_6',V_35)
| ~ hollywood_placename('#skF_6',V_35)
| ~ city('#skF_6','#skF_9')
| ~ of('#skF_6',V_35,'#skF_9')
| ~ actual_world('#skF_6') ),
inference(resolution,[status(thm)],[c_717,c_966]) ).
tff(c_971,plain,
! [X_34,V_35] :
( ~ down('#skF_6','#skF_10',X_34)
| ~ lonely('#skF_6',X_34)
| ~ street('#skF_6',X_34)
| ~ placename('#skF_6',V_35)
| ~ hollywood_placename('#skF_6',V_35)
| ~ of('#skF_6',V_35,'#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_649,c_656,c_654,c_655,c_665,c_667,c_660,c_792,c_658,c_653,c_968]) ).
tff(c_973,plain,
! [V_39] :
( ~ placename('#skF_6',V_39)
| ~ hollywood_placename('#skF_6',V_39)
| ~ of('#skF_6',V_39,'#skF_9') ),
inference(splitLeft,[status(thm)],[c_971]) ).
tff(c_976,plain,
( ~ placename('#skF_6','#skF_8')
| ~ hollywood_placename('#skF_6','#skF_8') ),
inference(resolution,[status(thm)],[c_763,c_973]) ).
tff(c_980,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_666,c_671,c_976]) ).
tff(c_982,plain,
! [X_40] :
( ~ down('#skF_6','#skF_10',X_40)
| ~ lonely('#skF_6',X_40)
| ~ street('#skF_6',X_40) ),
inference(splitRight,[status(thm)],[c_971]) ).
tff(c_985,plain,
( ~ lonely('#skF_6','#skF_7')
| ~ street('#skF_6','#skF_7') ),
inference(resolution,[status(thm)],[c_708,c_982]) ).
tff(c_989,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_657,c_652,c_985]) ).
tff(c_990,plain,
present('#skF_1','#skF_5'),
inference(splitRight,[status(thm)],[c_10]) ).
tff(c_8,plain,
! [X_25,W_24,Y_26,U_18,V_23] :
( barrel('#skF_1','#skF_5')
| ~ in(U_18,Y_26,W_24)
| ~ down(U_18,Y_26,X_25)
| ~ barrel(U_18,Y_26)
| ~ present(U_18,Y_26)
| ~ agent(U_18,Y_26,W_24)
| ~ event(U_18,Y_26)
| ~ lonely(U_18,X_25)
| ~ street(U_18,X_25)
| ~ old(U_18,W_24)
| ~ dirty(U_18,W_24)
| ~ white(U_18,W_24)
| ~ chevy(U_18,W_24)
| ~ placename(U_18,V_23)
| ~ hollywood_placename(U_18,V_23)
| ~ city(U_18,W_24)
| ~ of(U_18,V_23,W_24)
| ~ actual_world(U_18) ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1189,plain,
! [W_93,V_91,Y_94,U_92,X_90] :
( ~ in(U_92,Y_94,W_93)
| ~ down(U_92,Y_94,X_90)
| ~ barrel(U_92,Y_94)
| ~ present(U_92,Y_94)
| ~ agent(U_92,Y_94,W_93)
| ~ event(U_92,Y_94)
| ~ lonely(U_92,X_90)
| ~ street(U_92,X_90)
| ~ old(U_92,W_93)
| ~ dirty(U_92,W_93)
| ~ white(U_92,W_93)
| ~ chevy(U_92,W_93)
| ~ placename(U_92,V_91)
| ~ hollywood_placename(U_92,V_91)
| ~ city(U_92,W_93)
| ~ of(U_92,V_91,W_93)
| ~ actual_world(U_92) ),
inference(splitLeft,[status(thm)],[c_8]) ).
tff(c_1191,plain,
! [X_90,V_91] :
( ~ down('#skF_6','#skF_10',X_90)
| ~ barrel('#skF_6','#skF_10')
| ~ present('#skF_6','#skF_10')
| ~ agent('#skF_6','#skF_10','#skF_9')
| ~ event('#skF_6','#skF_10')
| ~ lonely('#skF_6',X_90)
| ~ street('#skF_6',X_90)
| ~ old('#skF_6','#skF_9')
| ~ dirty('#skF_6','#skF_9')
| ~ white('#skF_6','#skF_9')
| ~ chevy('#skF_6','#skF_9')
| ~ placename('#skF_6',V_91)
| ~ hollywood_placename('#skF_6',V_91)
| ~ city('#skF_6','#skF_9')
| ~ of('#skF_6',V_91,'#skF_9')
| ~ actual_world('#skF_6') ),
inference(resolution,[status(thm)],[c_717,c_1189]) ).
tff(c_1194,plain,
! [X_90,V_91] :
( ~ down('#skF_6','#skF_10',X_90)
| ~ lonely('#skF_6',X_90)
| ~ street('#skF_6',X_90)
| ~ placename('#skF_6',V_91)
| ~ hollywood_placename('#skF_6',V_91)
| ~ of('#skF_6',V_91,'#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_649,c_656,c_654,c_655,c_665,c_667,c_660,c_792,c_658,c_653,c_1191]) ).
tff(c_1196,plain,
! [V_95] :
( ~ placename('#skF_6',V_95)
| ~ hollywood_placename('#skF_6',V_95)
| ~ of('#skF_6',V_95,'#skF_9') ),
inference(splitLeft,[status(thm)],[c_1194]) ).
tff(c_1199,plain,
( ~ placename('#skF_6','#skF_8')
| ~ hollywood_placename('#skF_6','#skF_8') ),
inference(resolution,[status(thm)],[c_763,c_1196]) ).
tff(c_1203,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_666,c_671,c_1199]) ).
tff(c_1205,plain,
! [X_96] :
( ~ down('#skF_6','#skF_10',X_96)
| ~ lonely('#skF_6',X_96)
| ~ street('#skF_6',X_96) ),
inference(splitRight,[status(thm)],[c_1194]) ).
tff(c_1208,plain,
( ~ lonely('#skF_6','#skF_7')
| ~ street('#skF_6','#skF_7') ),
inference(resolution,[status(thm)],[c_708,c_1205]) ).
tff(c_1212,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_657,c_652,c_1208]) ).
tff(c_1213,plain,
barrel('#skF_1','#skF_5'),
inference(splitRight,[status(thm)],[c_8]) ).
tff(c_4,plain,
! [X_25,W_24,Y_26,U_18,V_23] :
( in('#skF_1','#skF_5','#skF_3')
| ~ in(U_18,Y_26,W_24)
| ~ down(U_18,Y_26,X_25)
| ~ barrel(U_18,Y_26)
| ~ present(U_18,Y_26)
| ~ agent(U_18,Y_26,W_24)
| ~ event(U_18,Y_26)
| ~ lonely(U_18,X_25)
| ~ street(U_18,X_25)
| ~ old(U_18,W_24)
| ~ dirty(U_18,W_24)
| ~ white(U_18,W_24)
| ~ chevy(U_18,W_24)
| ~ placename(U_18,V_23)
| ~ hollywood_placename(U_18,V_23)
| ~ city(U_18,W_24)
| ~ of(U_18,V_23,W_24)
| ~ actual_world(U_18) ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1377,plain,
! [U_141,X_139,Y_143,V_140,W_142] :
( ~ in(U_141,Y_143,W_142)
| ~ down(U_141,Y_143,X_139)
| ~ barrel(U_141,Y_143)
| ~ present(U_141,Y_143)
| ~ agent(U_141,Y_143,W_142)
| ~ event(U_141,Y_143)
| ~ lonely(U_141,X_139)
| ~ street(U_141,X_139)
| ~ old(U_141,W_142)
| ~ dirty(U_141,W_142)
| ~ white(U_141,W_142)
| ~ chevy(U_141,W_142)
| ~ placename(U_141,V_140)
| ~ hollywood_placename(U_141,V_140)
| ~ city(U_141,W_142)
| ~ of(U_141,V_140,W_142)
| ~ actual_world(U_141) ),
inference(splitLeft,[status(thm)],[c_4]) ).
tff(c_1379,plain,
! [X_139,V_140] :
( ~ down('#skF_6','#skF_10',X_139)
| ~ barrel('#skF_6','#skF_10')
| ~ present('#skF_6','#skF_10')
| ~ agent('#skF_6','#skF_10','#skF_9')
| ~ event('#skF_6','#skF_10')
| ~ lonely('#skF_6',X_139)
| ~ street('#skF_6',X_139)
| ~ old('#skF_6','#skF_9')
| ~ dirty('#skF_6','#skF_9')
| ~ white('#skF_6','#skF_9')
| ~ chevy('#skF_6','#skF_9')
| ~ placename('#skF_6',V_140)
| ~ hollywood_placename('#skF_6',V_140)
| ~ city('#skF_6','#skF_9')
| ~ of('#skF_6',V_140,'#skF_9')
| ~ actual_world('#skF_6') ),
inference(resolution,[status(thm)],[c_717,c_1377]) ).
tff(c_1382,plain,
! [X_139,V_140] :
( ~ down('#skF_6','#skF_10',X_139)
| ~ lonely('#skF_6',X_139)
| ~ street('#skF_6',X_139)
| ~ placename('#skF_6',V_140)
| ~ hollywood_placename('#skF_6',V_140)
| ~ of('#skF_6',V_140,'#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_649,c_656,c_654,c_655,c_665,c_667,c_660,c_792,c_658,c_653,c_1379]) ).
tff(c_1384,plain,
! [V_144] :
( ~ placename('#skF_6',V_144)
| ~ hollywood_placename('#skF_6',V_144)
| ~ of('#skF_6',V_144,'#skF_9') ),
inference(splitLeft,[status(thm)],[c_1382]) ).
tff(c_1387,plain,
( ~ placename('#skF_6','#skF_8')
| ~ hollywood_placename('#skF_6','#skF_8') ),
inference(resolution,[status(thm)],[c_763,c_1384]) ).
tff(c_1391,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_666,c_671,c_1387]) ).
tff(c_1393,plain,
! [X_145] :
( ~ down('#skF_6','#skF_10',X_145)
| ~ lonely('#skF_6',X_145)
| ~ street('#skF_6',X_145) ),
inference(splitRight,[status(thm)],[c_1382]) ).
tff(c_1396,plain,
( ~ lonely('#skF_6','#skF_7')
| ~ street('#skF_6','#skF_7') ),
inference(resolution,[status(thm)],[c_708,c_1393]) ).
tff(c_1400,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_657,c_652,c_1396]) ).
tff(c_1401,plain,
in('#skF_1','#skF_5','#skF_3'),
inference(splitRight,[status(thm)],[c_4]) ).
tff(c_2,plain,
! [X_25,X3_12,X4_13,W_24,Y_26,U_18,Z_5,X1_10,X2_11,V_23] :
( ~ in(Z_5,X4_13,X3_12)
| ~ down(Z_5,X4_13,X1_10)
| ~ barrel(Z_5,X4_13)
| ~ present(Z_5,X4_13)
| ~ agent(Z_5,X4_13,X3_12)
| ~ event(Z_5,X4_13)
| ~ old(Z_5,X3_12)
| ~ dirty(Z_5,X3_12)
| ~ white(Z_5,X3_12)
| ~ chevy(Z_5,X3_12)
| ~ placename(Z_5,X2_11)
| ~ hollywood_placename(Z_5,X2_11)
| ~ city(Z_5,X3_12)
| ~ of(Z_5,X2_11,X3_12)
| ~ lonely(Z_5,X1_10)
| ~ street(Z_5,X1_10)
| ~ actual_world(Z_5)
| ~ in(U_18,Y_26,W_24)
| ~ down(U_18,Y_26,X_25)
| ~ barrel(U_18,Y_26)
| ~ present(U_18,Y_26)
| ~ agent(U_18,Y_26,W_24)
| ~ event(U_18,Y_26)
| ~ lonely(U_18,X_25)
| ~ street(U_18,X_25)
| ~ old(U_18,W_24)
| ~ dirty(U_18,W_24)
| ~ white(U_18,W_24)
| ~ chevy(U_18,W_24)
| ~ placename(U_18,V_23)
| ~ hollywood_placename(U_18,V_23)
| ~ city(U_18,W_24)
| ~ of(U_18,V_23,W_24)
| ~ actual_world(U_18) ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1403,plain,
! [Y_150,V_147,U_148,X_146,W_149] :
( ~ in(U_148,Y_150,W_149)
| ~ down(U_148,Y_150,X_146)
| ~ barrel(U_148,Y_150)
| ~ present(U_148,Y_150)
| ~ agent(U_148,Y_150,W_149)
| ~ event(U_148,Y_150)
| ~ lonely(U_148,X_146)
| ~ street(U_148,X_146)
| ~ old(U_148,W_149)
| ~ dirty(U_148,W_149)
| ~ white(U_148,W_149)
| ~ chevy(U_148,W_149)
| ~ placename(U_148,V_147)
| ~ hollywood_placename(U_148,V_147)
| ~ city(U_148,W_149)
| ~ of(U_148,V_147,W_149)
| ~ actual_world(U_148) ),
inference(splitLeft,[status(thm)],[c_2]) ).
tff(c_1407,plain,
! [X_146,V_147] :
( ~ down('#skF_6','#skF_10',X_146)
| ~ barrel('#skF_6','#skF_10')
| ~ present('#skF_6','#skF_10')
| ~ agent('#skF_6','#skF_10','#skF_9')
| ~ event('#skF_6','#skF_10')
| ~ lonely('#skF_6',X_146)
| ~ street('#skF_6',X_146)
| ~ old('#skF_6','#skF_9')
| ~ dirty('#skF_6','#skF_9')
| ~ white('#skF_6','#skF_9')
| ~ chevy('#skF_6','#skF_9')
| ~ placename('#skF_6',V_147)
| ~ hollywood_placename('#skF_6',V_147)
| ~ city('#skF_6','#skF_9')
| ~ of('#skF_6',V_147,'#skF_9')
| ~ actual_world('#skF_6') ),
inference(resolution,[status(thm)],[c_717,c_1403]) ).
tff(c_1413,plain,
! [X_146,V_147] :
( ~ down('#skF_6','#skF_10',X_146)
| ~ lonely('#skF_6',X_146)
| ~ street('#skF_6',X_146)
| ~ placename('#skF_6',V_147)
| ~ hollywood_placename('#skF_6',V_147)
| ~ of('#skF_6',V_147,'#skF_9') ),
inference(demodulation,[status(thm),theory(equality)],[c_649,c_656,c_654,c_655,c_665,c_667,c_660,c_792,c_658,c_653,c_1407]) ).
tff(c_1416,plain,
! [V_151] :
( ~ placename('#skF_6',V_151)
| ~ hollywood_placename('#skF_6',V_151)
| ~ of('#skF_6',V_151,'#skF_9') ),
inference(splitLeft,[status(thm)],[c_1413]) ).
tff(c_1419,plain,
( ~ placename('#skF_6','#skF_8')
| ~ hollywood_placename('#skF_6','#skF_8') ),
inference(resolution,[status(thm)],[c_763,c_1416]) ).
tff(c_1423,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_666,c_671,c_1419]) ).
tff(c_1425,plain,
! [X_152] :
( ~ down('#skF_6','#skF_10',X_152)
| ~ lonely('#skF_6',X_152)
| ~ street('#skF_6',X_152) ),
inference(splitRight,[status(thm)],[c_1413]) ).
tff(c_1428,plain,
( ~ lonely('#skF_6','#skF_7')
| ~ street('#skF_6','#skF_7') ),
inference(resolution,[status(thm)],[c_708,c_1425]) ).
tff(c_1432,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_657,c_652,c_1428]) ).
tff(c_1434,plain,
! [X2_156,X1_154,X3_153,Z_155,X4_157] :
( ~ in(Z_155,X4_157,X3_153)
| ~ down(Z_155,X4_157,X1_154)
| ~ barrel(Z_155,X4_157)
| ~ present(Z_155,X4_157)
| ~ agent(Z_155,X4_157,X3_153)
| ~ event(Z_155,X4_157)
| ~ old(Z_155,X3_153)
| ~ dirty(Z_155,X3_153)
| ~ white(Z_155,X3_153)
| ~ chevy(Z_155,X3_153)
| ~ placename(Z_155,X2_156)
| ~ hollywood_placename(Z_155,X2_156)
| ~ city(Z_155,X3_153)
| ~ of(Z_155,X2_156,X3_153)
| ~ lonely(Z_155,X1_154)
| ~ street(Z_155,X1_154)
| ~ actual_world(Z_155) ),
inference(splitRight,[status(thm)],[c_2]) ).
tff(c_1436,plain,
! [X1_154,X2_156] :
( ~ down('#skF_1','#skF_5',X1_154)
| ~ barrel('#skF_1','#skF_5')
| ~ present('#skF_1','#skF_5')
| ~ agent('#skF_1','#skF_5','#skF_3')
| ~ event('#skF_1','#skF_5')
| ~ old('#skF_1','#skF_3')
| ~ dirty('#skF_1','#skF_3')
| ~ white('#skF_1','#skF_3')
| ~ chevy('#skF_1','#skF_3')
| ~ placename('#skF_1',X2_156)
| ~ hollywood_placename('#skF_1',X2_156)
| ~ city('#skF_1','#skF_3')
| ~ of('#skF_1',X2_156,'#skF_3')
| ~ lonely('#skF_1',X1_154)
| ~ street('#skF_1',X1_154)
| ~ actual_world('#skF_1') ),
inference(resolution,[status(thm)],[c_1401,c_1434]) ).
tff(c_1441,plain,
! [X1_154,X2_156] :
( ~ down('#skF_1','#skF_5',X1_154)
| ~ placename('#skF_1',X2_156)
| ~ hollywood_placename('#skF_1',X2_156)
| ~ of('#skF_1',X2_156,'#skF_3')
| ~ lonely('#skF_1',X1_154)
| ~ street('#skF_1',X1_154) ),
inference(demodulation,[status(thm),theory(equality)],[c_964,c_1044,c_1291,c_1070,c_1016,c_1186,c_1097,c_1319,c_990,c_1213,c_1436]) ).
tff(c_1446,plain,
! [X1_158] :
( ~ down('#skF_1','#skF_5',X1_158)
| ~ lonely('#skF_1',X1_158)
| ~ street('#skF_1',X1_158) ),
inference(splitLeft,[status(thm)],[c_1441]) ).
tff(c_1449,plain,
( ~ lonely('#skF_1','#skF_4')
| ~ street('#skF_1','#skF_4') ),
inference(resolution,[status(thm)],[c_1373,c_1446]) ).
tff(c_1453,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1124,c_1158,c_1449]) ).
tff(c_1455,plain,
! [X2_159] :
( ~ placename('#skF_1',X2_159)
| ~ hollywood_placename('#skF_1',X2_159)
| ~ of('#skF_1',X2_159,'#skF_3') ),
inference(splitRight,[status(thm)],[c_1441]) ).
tff(c_1458,plain,
( ~ placename('#skF_1','#skF_2')
| ~ hollywood_placename('#skF_1','#skF_2') ),
inference(resolution,[status(thm)],[c_1345,c_1455]) ).
tff(c_1462,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1265,c_1239,c_1458]) ).
tff(c_1464,plain,
~ agent('#skF_6','#skF_10','#skF_9'),
inference(splitRight,[status(thm)],[c_216]) ).
tff(c_210,plain,
( hollywood_placename('#skF_1','#skF_2')
| agent('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1542,plain,
hollywood_placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_1464,c_210]) ).
tff(c_208,plain,
( placename('#skF_1','#skF_2')
| agent('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1558,plain,
placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_1464,c_208]) ).
tff(c_214,plain,
( of('#skF_1','#skF_2','#skF_3')
| agent('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1608,plain,
of('#skF_1','#skF_2','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_1464,c_214]) ).
tff(c_198,plain,
( street('#skF_1','#skF_4')
| agent('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1510,plain,
street('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_1464,c_198]) ).
tff(c_196,plain,
( lonely('#skF_1','#skF_4')
| agent('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1590,plain,
lonely('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_1464,c_196]) ).
tff(c_186,plain,
( down('#skF_1','#skF_5','#skF_4')
| agent('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1606,plain,
down('#skF_1','#skF_5','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_1464,c_186]) ).
tff(c_1463,plain,
actual_world('#skF_1'),
inference(splitRight,[status(thm)],[c_216]) ).
tff(c_212,plain,
( city('#skF_1','#skF_3')
| agent('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1565,plain,
city('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_1464,c_212]) ).
tff(c_206,plain,
( chevy('#skF_1','#skF_3')
| agent('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1522,plain,
chevy('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_1464,c_206]) ).
tff(c_204,plain,
( white('#skF_1','#skF_3')
| agent('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1530,plain,
white('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_1464,c_204]) ).
tff(c_202,plain,
( dirty('#skF_1','#skF_3')
| agent('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1571,plain,
dirty('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_1464,c_202]) ).
tff(c_200,plain,
( old('#skF_1','#skF_3')
| agent('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1582,plain,
old('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_1464,c_200]) ).
tff(c_194,plain,
( event('#skF_1','#skF_5')
| agent('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1505,plain,
event('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_1464,c_194]) ).
tff(c_192,plain,
( agent('#skF_1','#skF_5','#skF_3')
| agent('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1600,plain,
agent('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_1464,c_192]) ).
tff(c_190,plain,
( present('#skF_1','#skF_5')
| agent('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1559,plain,
present('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_1464,c_190]) ).
tff(c_188,plain,
( barrel('#skF_1','#skF_5')
| agent('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1512,plain,
barrel('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_1464,c_188]) ).
tff(c_184,plain,
( in('#skF_1','#skF_5','#skF_3')
| agent('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1595,plain,
in('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_1464,c_184]) ).
tff(c_182,plain,
! [X3_12,X4_13,Z_5,X1_10,X2_11] :
( ~ in(Z_5,X4_13,X3_12)
| ~ down(Z_5,X4_13,X1_10)
| ~ barrel(Z_5,X4_13)
| ~ present(Z_5,X4_13)
| ~ agent(Z_5,X4_13,X3_12)
| ~ event(Z_5,X4_13)
| ~ old(Z_5,X3_12)
| ~ dirty(Z_5,X3_12)
| ~ white(Z_5,X3_12)
| ~ chevy(Z_5,X3_12)
| ~ placename(Z_5,X2_11)
| ~ hollywood_placename(Z_5,X2_11)
| ~ city(Z_5,X3_12)
| ~ of(Z_5,X2_11,X3_12)
| ~ lonely(Z_5,X1_10)
| ~ street(Z_5,X1_10)
| ~ actual_world(Z_5)
| agent('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1638,plain,
! [X1_161,X2_163,X4_164,X3_160,Z_162] :
( ~ in(Z_162,X4_164,X3_160)
| ~ down(Z_162,X4_164,X1_161)
| ~ barrel(Z_162,X4_164)
| ~ present(Z_162,X4_164)
| ~ agent(Z_162,X4_164,X3_160)
| ~ event(Z_162,X4_164)
| ~ old(Z_162,X3_160)
| ~ dirty(Z_162,X3_160)
| ~ white(Z_162,X3_160)
| ~ chevy(Z_162,X3_160)
| ~ placename(Z_162,X2_163)
| ~ hollywood_placename(Z_162,X2_163)
| ~ city(Z_162,X3_160)
| ~ of(Z_162,X2_163,X3_160)
| ~ lonely(Z_162,X1_161)
| ~ street(Z_162,X1_161)
| ~ actual_world(Z_162) ),
inference(negUnitSimplification,[status(thm)],[c_1464,c_182]) ).
tff(c_1640,plain,
! [X1_161,X2_163] :
( ~ down('#skF_1','#skF_5',X1_161)
| ~ barrel('#skF_1','#skF_5')
| ~ present('#skF_1','#skF_5')
| ~ agent('#skF_1','#skF_5','#skF_3')
| ~ event('#skF_1','#skF_5')
| ~ old('#skF_1','#skF_3')
| ~ dirty('#skF_1','#skF_3')
| ~ white('#skF_1','#skF_3')
| ~ chevy('#skF_1','#skF_3')
| ~ placename('#skF_1',X2_163)
| ~ hollywood_placename('#skF_1',X2_163)
| ~ city('#skF_1','#skF_3')
| ~ of('#skF_1',X2_163,'#skF_3')
| ~ lonely('#skF_1',X1_161)
| ~ street('#skF_1',X1_161)
| ~ actual_world('#skF_1') ),
inference(resolution,[status(thm)],[c_1595,c_1638]) ).
tff(c_1645,plain,
! [X1_161,X2_163] :
( ~ down('#skF_1','#skF_5',X1_161)
| ~ placename('#skF_1',X2_163)
| ~ hollywood_placename('#skF_1',X2_163)
| ~ of('#skF_1',X2_163,'#skF_3')
| ~ lonely('#skF_1',X1_161)
| ~ street('#skF_1',X1_161) ),
inference(demodulation,[status(thm),theory(equality)],[c_1463,c_1565,c_1522,c_1530,c_1571,c_1582,c_1505,c_1600,c_1559,c_1512,c_1640]) ).
tff(c_1650,plain,
! [X1_165] :
( ~ down('#skF_1','#skF_5',X1_165)
| ~ lonely('#skF_1',X1_165)
| ~ street('#skF_1',X1_165) ),
inference(splitLeft,[status(thm)],[c_1645]) ).
tff(c_1653,plain,
( ~ lonely('#skF_1','#skF_4')
| ~ street('#skF_1','#skF_4') ),
inference(resolution,[status(thm)],[c_1606,c_1650]) ).
tff(c_1657,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1510,c_1590,c_1653]) ).
tff(c_1659,plain,
! [X2_166] :
( ~ placename('#skF_1',X2_166)
| ~ hollywood_placename('#skF_1',X2_166)
| ~ of('#skF_1',X2_166,'#skF_3') ),
inference(splitRight,[status(thm)],[c_1645]) ).
tff(c_1662,plain,
( ~ placename('#skF_1','#skF_2')
| ~ hollywood_placename('#skF_1','#skF_2') ),
inference(resolution,[status(thm)],[c_1608,c_1659]) ).
tff(c_1666,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1542,c_1558,c_1662]) ).
tff(c_1668,plain,
~ of('#skF_6','#skF_8','#skF_9'),
inference(splitRight,[status(thm)],[c_540]) ).
tff(c_534,plain,
( hollywood_placename('#skF_1','#skF_2')
| of('#skF_6','#skF_8','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1782,plain,
hollywood_placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_1668,c_534]) ).
tff(c_532,plain,
( placename('#skF_1','#skF_2')
| of('#skF_6','#skF_8','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1743,plain,
placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_1668,c_532]) ).
tff(c_538,plain,
( of('#skF_1','#skF_2','#skF_3')
| of('#skF_6','#skF_8','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1831,plain,
of('#skF_1','#skF_2','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_1668,c_538]) ).
tff(c_522,plain,
( street('#skF_1','#skF_4')
| of('#skF_6','#skF_8','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1752,plain,
street('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_1668,c_522]) ).
tff(c_520,plain,
( lonely('#skF_1','#skF_4')
| of('#skF_6','#skF_8','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1799,plain,
lonely('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_1668,c_520]) ).
tff(c_510,plain,
( down('#skF_1','#skF_5','#skF_4')
| of('#skF_6','#skF_8','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1834,plain,
down('#skF_1','#skF_5','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_1668,c_510]) ).
tff(c_1667,plain,
actual_world('#skF_1'),
inference(splitRight,[status(thm)],[c_540]) ).
tff(c_536,plain,
( city('#skF_1','#skF_3')
| of('#skF_6','#skF_8','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1741,plain,
city('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_1668,c_536]) ).
tff(c_530,plain,
( chevy('#skF_1','#skF_3')
| of('#skF_6','#skF_8','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1790,plain,
chevy('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_1668,c_530]) ).
tff(c_528,plain,
( white('#skF_1','#skF_3')
| of('#skF_6','#skF_8','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1789,plain,
white('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_1668,c_528]) ).
tff(c_526,plain,
( dirty('#skF_1','#skF_3')
| of('#skF_6','#skF_8','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1766,plain,
dirty('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_1668,c_526]) ).
tff(c_524,plain,
( old('#skF_1','#skF_3')
| of('#skF_6','#skF_8','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1816,plain,
old('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_1668,c_524]) ).
tff(c_518,plain,
( event('#skF_1','#skF_5')
| of('#skF_6','#skF_8','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1819,plain,
event('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_1668,c_518]) ).
tff(c_516,plain,
( agent('#skF_1','#skF_5','#skF_3')
| of('#skF_6','#skF_8','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1836,plain,
agent('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_1668,c_516]) ).
tff(c_514,plain,
( present('#skF_1','#skF_5')
| of('#skF_6','#skF_8','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1818,plain,
present('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_1668,c_514]) ).
tff(c_512,plain,
( barrel('#skF_1','#skF_5')
| of('#skF_6','#skF_8','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1756,plain,
barrel('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_1668,c_512]) ).
tff(c_508,plain,
( in('#skF_1','#skF_5','#skF_3')
| of('#skF_6','#skF_8','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1841,plain,
in('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_1668,c_508]) ).
tff(c_506,plain,
! [X3_12,X4_13,Z_5,X1_10,X2_11] :
( ~ in(Z_5,X4_13,X3_12)
| ~ down(Z_5,X4_13,X1_10)
| ~ barrel(Z_5,X4_13)
| ~ present(Z_5,X4_13)
| ~ agent(Z_5,X4_13,X3_12)
| ~ event(Z_5,X4_13)
| ~ old(Z_5,X3_12)
| ~ dirty(Z_5,X3_12)
| ~ white(Z_5,X3_12)
| ~ chevy(Z_5,X3_12)
| ~ placename(Z_5,X2_11)
| ~ hollywood_placename(Z_5,X2_11)
| ~ city(Z_5,X3_12)
| ~ of(Z_5,X2_11,X3_12)
| ~ lonely(Z_5,X1_10)
| ~ street(Z_5,X1_10)
| ~ actual_world(Z_5)
| of('#skF_6','#skF_8','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_1874,plain,
! [X2_170,X1_168,X3_167,X4_171,Z_169] :
( ~ in(Z_169,X4_171,X3_167)
| ~ down(Z_169,X4_171,X1_168)
| ~ barrel(Z_169,X4_171)
| ~ present(Z_169,X4_171)
| ~ agent(Z_169,X4_171,X3_167)
| ~ event(Z_169,X4_171)
| ~ old(Z_169,X3_167)
| ~ dirty(Z_169,X3_167)
| ~ white(Z_169,X3_167)
| ~ chevy(Z_169,X3_167)
| ~ placename(Z_169,X2_170)
| ~ hollywood_placename(Z_169,X2_170)
| ~ city(Z_169,X3_167)
| ~ of(Z_169,X2_170,X3_167)
| ~ lonely(Z_169,X1_168)
| ~ street(Z_169,X1_168)
| ~ actual_world(Z_169) ),
inference(negUnitSimplification,[status(thm)],[c_1668,c_506]) ).
tff(c_1876,plain,
! [X1_168,X2_170] :
( ~ down('#skF_1','#skF_5',X1_168)
| ~ barrel('#skF_1','#skF_5')
| ~ present('#skF_1','#skF_5')
| ~ agent('#skF_1','#skF_5','#skF_3')
| ~ event('#skF_1','#skF_5')
| ~ old('#skF_1','#skF_3')
| ~ dirty('#skF_1','#skF_3')
| ~ white('#skF_1','#skF_3')
| ~ chevy('#skF_1','#skF_3')
| ~ placename('#skF_1',X2_170)
| ~ hollywood_placename('#skF_1',X2_170)
| ~ city('#skF_1','#skF_3')
| ~ of('#skF_1',X2_170,'#skF_3')
| ~ lonely('#skF_1',X1_168)
| ~ street('#skF_1',X1_168)
| ~ actual_world('#skF_1') ),
inference(resolution,[status(thm)],[c_1841,c_1874]) ).
tff(c_1881,plain,
! [X1_168,X2_170] :
( ~ down('#skF_1','#skF_5',X1_168)
| ~ placename('#skF_1',X2_170)
| ~ hollywood_placename('#skF_1',X2_170)
| ~ of('#skF_1',X2_170,'#skF_3')
| ~ lonely('#skF_1',X1_168)
| ~ street('#skF_1',X1_168) ),
inference(demodulation,[status(thm),theory(equality)],[c_1667,c_1741,c_1790,c_1789,c_1766,c_1816,c_1819,c_1836,c_1818,c_1756,c_1876]) ).
tff(c_1886,plain,
! [X1_172] :
( ~ down('#skF_1','#skF_5',X1_172)
| ~ lonely('#skF_1',X1_172)
| ~ street('#skF_1',X1_172) ),
inference(splitLeft,[status(thm)],[c_1881]) ).
tff(c_1889,plain,
( ~ lonely('#skF_1','#skF_4')
| ~ street('#skF_1','#skF_4') ),
inference(resolution,[status(thm)],[c_1834,c_1886]) ).
tff(c_1893,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1752,c_1799,c_1889]) ).
tff(c_1895,plain,
! [X2_173] :
( ~ placename('#skF_1',X2_173)
| ~ hollywood_placename('#skF_1',X2_173)
| ~ of('#skF_1',X2_173,'#skF_3') ),
inference(splitRight,[status(thm)],[c_1881]) ).
tff(c_1898,plain,
( ~ placename('#skF_1','#skF_2')
| ~ hollywood_placename('#skF_1','#skF_2') ),
inference(resolution,[status(thm)],[c_1831,c_1895]) ).
tff(c_1902,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_1782,c_1743,c_1898]) ).
tff(c_1904,plain,
~ in('#skF_6','#skF_10','#skF_9'),
inference(splitRight,[status(thm)],[c_72]) ).
tff(c_66,plain,
( hollywood_placename('#skF_1','#skF_2')
| in('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2056,plain,
hollywood_placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_1904,c_66]) ).
tff(c_64,plain,
( placename('#skF_1','#skF_2')
| in('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2102,plain,
placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_1904,c_64]) ).
tff(c_70,plain,
( of('#skF_1','#skF_2','#skF_3')
| in('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2117,plain,
of('#skF_1','#skF_2','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_1904,c_70]) ).
tff(c_54,plain,
( street('#skF_1','#skF_4')
| in('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2098,plain,
street('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_1904,c_54]) ).
tff(c_52,plain,
( lonely('#skF_1','#skF_4')
| in('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2051,plain,
lonely('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_1904,c_52]) ).
tff(c_42,plain,
( down('#skF_1','#skF_5','#skF_4')
| in('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2114,plain,
down('#skF_1','#skF_5','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_1904,c_42]) ).
tff(c_1903,plain,
actual_world('#skF_1'),
inference(splitRight,[status(thm)],[c_72]) ).
tff(c_68,plain,
( city('#skF_1','#skF_3')
| in('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2021,plain,
city('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_1904,c_68]) ).
tff(c_62,plain,
( chevy('#skF_1','#skF_3')
| in('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2050,plain,
chevy('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_1904,c_62]) ).
tff(c_60,plain,
( white('#skF_1','#skF_3')
| in('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2080,plain,
white('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_1904,c_60]) ).
tff(c_58,plain,
( dirty('#skF_1','#skF_3')
| in('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2047,plain,
dirty('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_1904,c_58]) ).
tff(c_56,plain,
( old('#skF_1','#skF_3')
| in('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2099,plain,
old('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_1904,c_56]) ).
tff(c_50,plain,
( event('#skF_1','#skF_5')
| in('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2026,plain,
event('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_1904,c_50]) ).
tff(c_48,plain,
( agent('#skF_1','#skF_5','#skF_3')
| in('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2124,plain,
agent('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_1904,c_48]) ).
tff(c_46,plain,
( present('#skF_1','#skF_5')
| in('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2018,plain,
present('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_1904,c_46]) ).
tff(c_44,plain,
( barrel('#skF_1','#skF_5')
| in('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2033,plain,
barrel('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_1904,c_44]) ).
tff(c_40,plain,
( in('#skF_1','#skF_5','#skF_3')
| in('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2121,plain,
in('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_1904,c_40]) ).
tff(c_38,plain,
! [X3_12,X4_13,Z_5,X1_10,X2_11] :
( ~ in(Z_5,X4_13,X3_12)
| ~ down(Z_5,X4_13,X1_10)
| ~ barrel(Z_5,X4_13)
| ~ present(Z_5,X4_13)
| ~ agent(Z_5,X4_13,X3_12)
| ~ event(Z_5,X4_13)
| ~ old(Z_5,X3_12)
| ~ dirty(Z_5,X3_12)
| ~ white(Z_5,X3_12)
| ~ chevy(Z_5,X3_12)
| ~ placename(Z_5,X2_11)
| ~ hollywood_placename(Z_5,X2_11)
| ~ city(Z_5,X3_12)
| ~ of(Z_5,X2_11,X3_12)
| ~ lonely(Z_5,X1_10)
| ~ street(Z_5,X1_10)
| ~ actual_world(Z_5)
| in('#skF_6','#skF_10','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2155,plain,
! [X2_177,X1_175,X4_178,X3_174,Z_176] :
( ~ in(Z_176,X4_178,X3_174)
| ~ down(Z_176,X4_178,X1_175)
| ~ barrel(Z_176,X4_178)
| ~ present(Z_176,X4_178)
| ~ agent(Z_176,X4_178,X3_174)
| ~ event(Z_176,X4_178)
| ~ old(Z_176,X3_174)
| ~ dirty(Z_176,X3_174)
| ~ white(Z_176,X3_174)
| ~ chevy(Z_176,X3_174)
| ~ placename(Z_176,X2_177)
| ~ hollywood_placename(Z_176,X2_177)
| ~ city(Z_176,X3_174)
| ~ of(Z_176,X2_177,X3_174)
| ~ lonely(Z_176,X1_175)
| ~ street(Z_176,X1_175)
| ~ actual_world(Z_176) ),
inference(negUnitSimplification,[status(thm)],[c_1904,c_38]) ).
tff(c_2157,plain,
! [X1_175,X2_177] :
( ~ down('#skF_1','#skF_5',X1_175)
| ~ barrel('#skF_1','#skF_5')
| ~ present('#skF_1','#skF_5')
| ~ agent('#skF_1','#skF_5','#skF_3')
| ~ event('#skF_1','#skF_5')
| ~ old('#skF_1','#skF_3')
| ~ dirty('#skF_1','#skF_3')
| ~ white('#skF_1','#skF_3')
| ~ chevy('#skF_1','#skF_3')
| ~ placename('#skF_1',X2_177)
| ~ hollywood_placename('#skF_1',X2_177)
| ~ city('#skF_1','#skF_3')
| ~ of('#skF_1',X2_177,'#skF_3')
| ~ lonely('#skF_1',X1_175)
| ~ street('#skF_1',X1_175)
| ~ actual_world('#skF_1') ),
inference(resolution,[status(thm)],[c_2121,c_2155]) ).
tff(c_2160,plain,
! [X1_175,X2_177] :
( ~ down('#skF_1','#skF_5',X1_175)
| ~ placename('#skF_1',X2_177)
| ~ hollywood_placename('#skF_1',X2_177)
| ~ of('#skF_1',X2_177,'#skF_3')
| ~ lonely('#skF_1',X1_175)
| ~ street('#skF_1',X1_175) ),
inference(demodulation,[status(thm),theory(equality)],[c_1903,c_2021,c_2050,c_2080,c_2047,c_2099,c_2026,c_2124,c_2018,c_2033,c_2157]) ).
tff(c_2163,plain,
! [X1_179] :
( ~ down('#skF_1','#skF_5',X1_179)
| ~ lonely('#skF_1',X1_179)
| ~ street('#skF_1',X1_179) ),
inference(splitLeft,[status(thm)],[c_2160]) ).
tff(c_2166,plain,
( ~ lonely('#skF_1','#skF_4')
| ~ street('#skF_1','#skF_4') ),
inference(resolution,[status(thm)],[c_2114,c_2163]) ).
tff(c_2170,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2098,c_2051,c_2166]) ).
tff(c_2172,plain,
! [X2_180] :
( ~ placename('#skF_1',X2_180)
| ~ hollywood_placename('#skF_1',X2_180)
| ~ of('#skF_1',X2_180,'#skF_3') ),
inference(splitRight,[status(thm)],[c_2160]) ).
tff(c_2175,plain,
( ~ placename('#skF_1','#skF_2')
| ~ hollywood_placename('#skF_1','#skF_2') ),
inference(resolution,[status(thm)],[c_2117,c_2172]) ).
tff(c_2179,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2056,c_2102,c_2175]) ).
tff(c_2181,plain,
~ down('#skF_6','#skF_10','#skF_7'),
inference(splitRight,[status(thm)],[c_108]) ).
tff(c_102,plain,
( hollywood_placename('#skF_1','#skF_2')
| down('#skF_6','#skF_10','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2382,plain,
hollywood_placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_2181,c_102]) ).
tff(c_100,plain,
( placename('#skF_1','#skF_2')
| down('#skF_6','#skF_10','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2346,plain,
placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_2181,c_100]) ).
tff(c_106,plain,
( of('#skF_1','#skF_2','#skF_3')
| down('#skF_6','#skF_10','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2402,plain,
of('#skF_1','#skF_2','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_2181,c_106]) ).
tff(c_90,plain,
( street('#skF_1','#skF_4')
| down('#skF_6','#skF_10','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2299,plain,
street('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_2181,c_90]) ).
tff(c_88,plain,
( lonely('#skF_1','#skF_4')
| down('#skF_6','#skF_10','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2331,plain,
lonely('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_2181,c_88]) ).
tff(c_78,plain,
( down('#skF_1','#skF_5','#skF_4')
| down('#skF_6','#skF_10','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2397,plain,
down('#skF_1','#skF_5','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_2181,c_78]) ).
tff(c_2180,plain,
actual_world('#skF_1'),
inference(splitRight,[status(thm)],[c_108]) ).
tff(c_104,plain,
( city('#skF_1','#skF_3')
| down('#skF_6','#skF_10','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2315,plain,
city('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_2181,c_104]) ).
tff(c_98,plain,
( chevy('#skF_1','#skF_3')
| down('#skF_6','#skF_10','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2390,plain,
chevy('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_2181,c_98]) ).
tff(c_96,plain,
( white('#skF_1','#skF_3')
| down('#skF_6','#skF_10','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2392,plain,
white('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_2181,c_96]) ).
tff(c_94,plain,
( dirty('#skF_1','#skF_3')
| down('#skF_6','#skF_10','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2309,plain,
dirty('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_2181,c_94]) ).
tff(c_92,plain,
( old('#skF_1','#skF_3')
| down('#skF_6','#skF_10','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2361,plain,
old('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_2181,c_92]) ).
tff(c_86,plain,
( event('#skF_1','#skF_5')
| down('#skF_6','#skF_10','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2310,plain,
event('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_2181,c_86]) ).
tff(c_84,plain,
( agent('#skF_1','#skF_5','#skF_3')
| down('#skF_6','#skF_10','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2408,plain,
agent('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_2181,c_84]) ).
tff(c_82,plain,
( present('#skF_1','#skF_5')
| down('#skF_6','#skF_10','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2316,plain,
present('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_2181,c_82]) ).
tff(c_80,plain,
( barrel('#skF_1','#skF_5')
| down('#skF_6','#skF_10','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2320,plain,
barrel('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_2181,c_80]) ).
tff(c_76,plain,
( in('#skF_1','#skF_5','#skF_3')
| down('#skF_6','#skF_10','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2409,plain,
in('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_2181,c_76]) ).
tff(c_74,plain,
! [X3_12,X4_13,Z_5,X1_10,X2_11] :
( ~ in(Z_5,X4_13,X3_12)
| ~ down(Z_5,X4_13,X1_10)
| ~ barrel(Z_5,X4_13)
| ~ present(Z_5,X4_13)
| ~ agent(Z_5,X4_13,X3_12)
| ~ event(Z_5,X4_13)
| ~ old(Z_5,X3_12)
| ~ dirty(Z_5,X3_12)
| ~ white(Z_5,X3_12)
| ~ chevy(Z_5,X3_12)
| ~ placename(Z_5,X2_11)
| ~ hollywood_placename(Z_5,X2_11)
| ~ city(Z_5,X3_12)
| ~ of(Z_5,X2_11,X3_12)
| ~ lonely(Z_5,X1_10)
| ~ street(Z_5,X1_10)
| ~ actual_world(Z_5)
| down('#skF_6','#skF_10','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2444,plain,
! [X1_182,Z_183,X3_181,X2_184,X4_185] :
( ~ in(Z_183,X4_185,X3_181)
| ~ down(Z_183,X4_185,X1_182)
| ~ barrel(Z_183,X4_185)
| ~ present(Z_183,X4_185)
| ~ agent(Z_183,X4_185,X3_181)
| ~ event(Z_183,X4_185)
| ~ old(Z_183,X3_181)
| ~ dirty(Z_183,X3_181)
| ~ white(Z_183,X3_181)
| ~ chevy(Z_183,X3_181)
| ~ placename(Z_183,X2_184)
| ~ hollywood_placename(Z_183,X2_184)
| ~ city(Z_183,X3_181)
| ~ of(Z_183,X2_184,X3_181)
| ~ lonely(Z_183,X1_182)
| ~ street(Z_183,X1_182)
| ~ actual_world(Z_183) ),
inference(negUnitSimplification,[status(thm)],[c_2181,c_74]) ).
tff(c_2446,plain,
! [X1_182,X2_184] :
( ~ down('#skF_1','#skF_5',X1_182)
| ~ barrel('#skF_1','#skF_5')
| ~ present('#skF_1','#skF_5')
| ~ agent('#skF_1','#skF_5','#skF_3')
| ~ event('#skF_1','#skF_5')
| ~ old('#skF_1','#skF_3')
| ~ dirty('#skF_1','#skF_3')
| ~ white('#skF_1','#skF_3')
| ~ chevy('#skF_1','#skF_3')
| ~ placename('#skF_1',X2_184)
| ~ hollywood_placename('#skF_1',X2_184)
| ~ city('#skF_1','#skF_3')
| ~ of('#skF_1',X2_184,'#skF_3')
| ~ lonely('#skF_1',X1_182)
| ~ street('#skF_1',X1_182)
| ~ actual_world('#skF_1') ),
inference(resolution,[status(thm)],[c_2409,c_2444]) ).
tff(c_2451,plain,
! [X1_182,X2_184] :
( ~ down('#skF_1','#skF_5',X1_182)
| ~ placename('#skF_1',X2_184)
| ~ hollywood_placename('#skF_1',X2_184)
| ~ of('#skF_1',X2_184,'#skF_3')
| ~ lonely('#skF_1',X1_182)
| ~ street('#skF_1',X1_182) ),
inference(demodulation,[status(thm),theory(equality)],[c_2180,c_2315,c_2390,c_2392,c_2309,c_2361,c_2310,c_2408,c_2316,c_2320,c_2446]) ).
tff(c_2456,plain,
! [X1_186] :
( ~ down('#skF_1','#skF_5',X1_186)
| ~ lonely('#skF_1',X1_186)
| ~ street('#skF_1',X1_186) ),
inference(splitLeft,[status(thm)],[c_2451]) ).
tff(c_2459,plain,
( ~ lonely('#skF_1','#skF_4')
| ~ street('#skF_1','#skF_4') ),
inference(resolution,[status(thm)],[c_2397,c_2456]) ).
tff(c_2463,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2299,c_2331,c_2459]) ).
tff(c_2465,plain,
! [X2_187] :
( ~ placename('#skF_1',X2_187)
| ~ hollywood_placename('#skF_1',X2_187)
| ~ of('#skF_1',X2_187,'#skF_3') ),
inference(splitRight,[status(thm)],[c_2451]) ).
tff(c_2468,plain,
( ~ placename('#skF_1','#skF_2')
| ~ hollywood_placename('#skF_1','#skF_2') ),
inference(resolution,[status(thm)],[c_2402,c_2465]) ).
tff(c_2472,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2382,c_2346,c_2468]) ).
tff(c_2474,plain,
~ placename('#skF_6','#skF_8'),
inference(splitRight,[status(thm)],[c_432]) ).
tff(c_426,plain,
( hollywood_placename('#skF_1','#skF_2')
| placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2570,plain,
hollywood_placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_2474,c_426]) ).
tff(c_424,plain,
( placename('#skF_1','#skF_2')
| placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2561,plain,
placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_2474,c_424]) ).
tff(c_430,plain,
( of('#skF_1','#skF_2','#skF_3')
| placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2715,plain,
of('#skF_1','#skF_2','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_2474,c_430]) ).
tff(c_414,plain,
( street('#skF_1','#skF_4')
| placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2550,plain,
street('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_2474,c_414]) ).
tff(c_412,plain,
( lonely('#skF_1','#skF_4')
| placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2548,plain,
lonely('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_2474,c_412]) ).
tff(c_402,plain,
( down('#skF_1','#skF_5','#skF_4')
| placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2696,plain,
down('#skF_1','#skF_5','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_2474,c_402]) ).
tff(c_2473,plain,
actual_world('#skF_1'),
inference(splitRight,[status(thm)],[c_432]) ).
tff(c_428,plain,
( city('#skF_1','#skF_3')
| placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2581,plain,
city('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_2474,c_428]) ).
tff(c_422,plain,
( chevy('#skF_1','#skF_3')
| placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2579,plain,
chevy('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_2474,c_422]) ).
tff(c_420,plain,
( white('#skF_1','#skF_3')
| placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2563,plain,
white('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_2474,c_420]) ).
tff(c_418,plain,
( dirty('#skF_1','#skF_3')
| placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2568,plain,
dirty('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_2474,c_418]) ).
tff(c_416,plain,
( old('#skF_1','#skF_3')
| placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2562,plain,
old('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_2474,c_416]) ).
tff(c_410,plain,
( event('#skF_1','#skF_5')
| placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2536,plain,
event('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_2474,c_410]) ).
tff(c_408,plain,
( agent('#skF_1','#skF_5','#skF_3')
| placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2642,plain,
agent('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_2474,c_408]) ).
tff(c_406,plain,
( present('#skF_1','#skF_5')
| placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2533,plain,
present('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_2474,c_406]) ).
tff(c_404,plain,
( barrel('#skF_1','#skF_5')
| placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2525,plain,
barrel('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_2474,c_404]) ).
tff(c_400,plain,
( in('#skF_1','#skF_5','#skF_3')
| placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2723,plain,
in('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_2474,c_400]) ).
tff(c_398,plain,
! [X3_12,X4_13,Z_5,X1_10,X2_11] :
( ~ in(Z_5,X4_13,X3_12)
| ~ down(Z_5,X4_13,X1_10)
| ~ barrel(Z_5,X4_13)
| ~ present(Z_5,X4_13)
| ~ agent(Z_5,X4_13,X3_12)
| ~ event(Z_5,X4_13)
| ~ old(Z_5,X3_12)
| ~ dirty(Z_5,X3_12)
| ~ white(Z_5,X3_12)
| ~ chevy(Z_5,X3_12)
| ~ placename(Z_5,X2_11)
| ~ hollywood_placename(Z_5,X2_11)
| ~ city(Z_5,X3_12)
| ~ of(Z_5,X2_11,X3_12)
| ~ lonely(Z_5,X1_10)
| ~ street(Z_5,X1_10)
| ~ actual_world(Z_5)
| placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2744,plain,
! [X1_189,Z_190,X2_191,X3_188,X4_192] :
( ~ in(Z_190,X4_192,X3_188)
| ~ down(Z_190,X4_192,X1_189)
| ~ barrel(Z_190,X4_192)
| ~ present(Z_190,X4_192)
| ~ agent(Z_190,X4_192,X3_188)
| ~ event(Z_190,X4_192)
| ~ old(Z_190,X3_188)
| ~ dirty(Z_190,X3_188)
| ~ white(Z_190,X3_188)
| ~ chevy(Z_190,X3_188)
| ~ placename(Z_190,X2_191)
| ~ hollywood_placename(Z_190,X2_191)
| ~ city(Z_190,X3_188)
| ~ of(Z_190,X2_191,X3_188)
| ~ lonely(Z_190,X1_189)
| ~ street(Z_190,X1_189)
| ~ actual_world(Z_190) ),
inference(negUnitSimplification,[status(thm)],[c_2474,c_398]) ).
tff(c_2746,plain,
! [X1_189,X2_191] :
( ~ down('#skF_1','#skF_5',X1_189)
| ~ barrel('#skF_1','#skF_5')
| ~ present('#skF_1','#skF_5')
| ~ agent('#skF_1','#skF_5','#skF_3')
| ~ event('#skF_1','#skF_5')
| ~ old('#skF_1','#skF_3')
| ~ dirty('#skF_1','#skF_3')
| ~ white('#skF_1','#skF_3')
| ~ chevy('#skF_1','#skF_3')
| ~ placename('#skF_1',X2_191)
| ~ hollywood_placename('#skF_1',X2_191)
| ~ city('#skF_1','#skF_3')
| ~ of('#skF_1',X2_191,'#skF_3')
| ~ lonely('#skF_1',X1_189)
| ~ street('#skF_1',X1_189)
| ~ actual_world('#skF_1') ),
inference(resolution,[status(thm)],[c_2723,c_2744]) ).
tff(c_2749,plain,
! [X1_189,X2_191] :
( ~ down('#skF_1','#skF_5',X1_189)
| ~ placename('#skF_1',X2_191)
| ~ hollywood_placename('#skF_1',X2_191)
| ~ of('#skF_1',X2_191,'#skF_3')
| ~ lonely('#skF_1',X1_189)
| ~ street('#skF_1',X1_189) ),
inference(demodulation,[status(thm),theory(equality)],[c_2473,c_2581,c_2579,c_2563,c_2568,c_2562,c_2536,c_2642,c_2533,c_2525,c_2746]) ).
tff(c_2752,plain,
! [X1_193] :
( ~ down('#skF_1','#skF_5',X1_193)
| ~ lonely('#skF_1',X1_193)
| ~ street('#skF_1',X1_193) ),
inference(splitLeft,[status(thm)],[c_2749]) ).
tff(c_2755,plain,
( ~ lonely('#skF_1','#skF_4')
| ~ street('#skF_1','#skF_4') ),
inference(resolution,[status(thm)],[c_2696,c_2752]) ).
tff(c_2759,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2550,c_2548,c_2755]) ).
tff(c_2761,plain,
! [X2_194] :
( ~ placename('#skF_1',X2_194)
| ~ hollywood_placename('#skF_1',X2_194)
| ~ of('#skF_1',X2_194,'#skF_3') ),
inference(splitRight,[status(thm)],[c_2749]) ).
tff(c_2764,plain,
( ~ placename('#skF_1','#skF_2')
| ~ hollywood_placename('#skF_1','#skF_2') ),
inference(resolution,[status(thm)],[c_2715,c_2761]) ).
tff(c_2768,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2570,c_2561,c_2764]) ).
tff(c_2770,plain,
~ old('#skF_6','#skF_9'),
inference(splitRight,[status(thm)],[c_288]) ).
tff(c_282,plain,
( hollywood_placename('#skF_1','#skF_2')
| old('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2919,plain,
hollywood_placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_2770,c_282]) ).
tff(c_280,plain,
( placename('#skF_1','#skF_2')
| old('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2892,plain,
placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_2770,c_280]) ).
tff(c_286,plain,
( of('#skF_1','#skF_2','#skF_3')
| old('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3014,plain,
of('#skF_1','#skF_2','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_2770,c_286]) ).
tff(c_270,plain,
( street('#skF_1','#skF_4')
| old('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2925,plain,
street('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_2770,c_270]) ).
tff(c_268,plain,
( lonely('#skF_1','#skF_4')
| old('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2915,plain,
lonely('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_2770,c_268]) ).
tff(c_258,plain,
( down('#skF_1','#skF_5','#skF_4')
| old('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2948,plain,
down('#skF_1','#skF_5','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_2770,c_258]) ).
tff(c_2769,plain,
actual_world('#skF_1'),
inference(splitRight,[status(thm)],[c_288]) ).
tff(c_284,plain,
( city('#skF_1','#skF_3')
| old('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2888,plain,
city('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_2770,c_284]) ).
tff(c_278,plain,
( chevy('#skF_1','#skF_3')
| old('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2898,plain,
chevy('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_2770,c_278]) ).
tff(c_276,plain,
( white('#skF_1','#skF_3')
| old('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2902,plain,
white('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_2770,c_276]) ).
tff(c_274,plain,
( dirty('#skF_1','#skF_3')
| old('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2923,plain,
dirty('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_2770,c_274]) ).
tff(c_272,plain,
( old('#skF_1','#skF_3')
| old('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2899,plain,
old('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_2770,c_272]) ).
tff(c_266,plain,
( event('#skF_1','#skF_5')
| old('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2917,plain,
event('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_2770,c_266]) ).
tff(c_264,plain,
( agent('#skF_1','#skF_5','#skF_3')
| old('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2964,plain,
agent('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_2770,c_264]) ).
tff(c_262,plain,
( present('#skF_1','#skF_5')
| old('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2912,plain,
present('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_2770,c_262]) ).
tff(c_260,plain,
( barrel('#skF_1','#skF_5')
| old('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_2907,plain,
barrel('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_2770,c_260]) ).
tff(c_256,plain,
( in('#skF_1','#skF_5','#skF_3')
| old('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3000,plain,
in('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_2770,c_256]) ).
tff(c_254,plain,
! [X3_12,X4_13,Z_5,X1_10,X2_11] :
( ~ in(Z_5,X4_13,X3_12)
| ~ down(Z_5,X4_13,X1_10)
| ~ barrel(Z_5,X4_13)
| ~ present(Z_5,X4_13)
| ~ agent(Z_5,X4_13,X3_12)
| ~ event(Z_5,X4_13)
| ~ old(Z_5,X3_12)
| ~ dirty(Z_5,X3_12)
| ~ white(Z_5,X3_12)
| ~ chevy(Z_5,X3_12)
| ~ placename(Z_5,X2_11)
| ~ hollywood_placename(Z_5,X2_11)
| ~ city(Z_5,X3_12)
| ~ of(Z_5,X2_11,X3_12)
| ~ lonely(Z_5,X1_10)
| ~ street(Z_5,X1_10)
| ~ actual_world(Z_5)
| old('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3056,plain,
! [X3_195,X1_196,Z_197,X4_199,X2_198] :
( ~ in(Z_197,X4_199,X3_195)
| ~ down(Z_197,X4_199,X1_196)
| ~ barrel(Z_197,X4_199)
| ~ present(Z_197,X4_199)
| ~ agent(Z_197,X4_199,X3_195)
| ~ event(Z_197,X4_199)
| ~ old(Z_197,X3_195)
| ~ dirty(Z_197,X3_195)
| ~ white(Z_197,X3_195)
| ~ chevy(Z_197,X3_195)
| ~ placename(Z_197,X2_198)
| ~ hollywood_placename(Z_197,X2_198)
| ~ city(Z_197,X3_195)
| ~ of(Z_197,X2_198,X3_195)
| ~ lonely(Z_197,X1_196)
| ~ street(Z_197,X1_196)
| ~ actual_world(Z_197) ),
inference(negUnitSimplification,[status(thm)],[c_2770,c_254]) ).
tff(c_3058,plain,
! [X1_196,X2_198] :
( ~ down('#skF_1','#skF_5',X1_196)
| ~ barrel('#skF_1','#skF_5')
| ~ present('#skF_1','#skF_5')
| ~ agent('#skF_1','#skF_5','#skF_3')
| ~ event('#skF_1','#skF_5')
| ~ old('#skF_1','#skF_3')
| ~ dirty('#skF_1','#skF_3')
| ~ white('#skF_1','#skF_3')
| ~ chevy('#skF_1','#skF_3')
| ~ placename('#skF_1',X2_198)
| ~ hollywood_placename('#skF_1',X2_198)
| ~ city('#skF_1','#skF_3')
| ~ of('#skF_1',X2_198,'#skF_3')
| ~ lonely('#skF_1',X1_196)
| ~ street('#skF_1',X1_196)
| ~ actual_world('#skF_1') ),
inference(resolution,[status(thm)],[c_3000,c_3056]) ).
tff(c_3061,plain,
! [X1_196,X2_198] :
( ~ down('#skF_1','#skF_5',X1_196)
| ~ placename('#skF_1',X2_198)
| ~ hollywood_placename('#skF_1',X2_198)
| ~ of('#skF_1',X2_198,'#skF_3')
| ~ lonely('#skF_1',X1_196)
| ~ street('#skF_1',X1_196) ),
inference(demodulation,[status(thm),theory(equality)],[c_2769,c_2888,c_2898,c_2902,c_2923,c_2899,c_2917,c_2964,c_2912,c_2907,c_3058]) ).
tff(c_3063,plain,
! [X1_200] :
( ~ down('#skF_1','#skF_5',X1_200)
| ~ lonely('#skF_1',X1_200)
| ~ street('#skF_1',X1_200) ),
inference(splitLeft,[status(thm)],[c_3061]) ).
tff(c_3066,plain,
( ~ lonely('#skF_1','#skF_4')
| ~ street('#skF_1','#skF_4') ),
inference(resolution,[status(thm)],[c_2948,c_3063]) ).
tff(c_3070,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2925,c_2915,c_3066]) ).
tff(c_3072,plain,
! [X2_201] :
( ~ placename('#skF_1',X2_201)
| ~ hollywood_placename('#skF_1',X2_201)
| ~ of('#skF_1',X2_201,'#skF_3') ),
inference(splitRight,[status(thm)],[c_3061]) ).
tff(c_3075,plain,
( ~ placename('#skF_1','#skF_2')
| ~ hollywood_placename('#skF_1','#skF_2') ),
inference(resolution,[status(thm)],[c_3014,c_3072]) ).
tff(c_3079,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_2919,c_2892,c_3075]) ).
tff(c_3081,plain,
~ hollywood_placename('#skF_6','#skF_8'),
inference(splitRight,[status(thm)],[c_468]) ).
tff(c_462,plain,
( hollywood_placename('#skF_1','#skF_2')
| hollywood_placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3212,plain,
hollywood_placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_3081,c_462]) ).
tff(c_460,plain,
( placename('#skF_1','#skF_2')
| hollywood_placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3219,plain,
placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_3081,c_460]) ).
tff(c_466,plain,
( of('#skF_1','#skF_2','#skF_3')
| hollywood_placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3299,plain,
of('#skF_1','#skF_2','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_3081,c_466]) ).
tff(c_450,plain,
( street('#skF_1','#skF_4')
| hollywood_placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3220,plain,
street('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_3081,c_450]) ).
tff(c_448,plain,
( lonely('#skF_1','#skF_4')
| hollywood_placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3210,plain,
lonely('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_3081,c_448]) ).
tff(c_438,plain,
( down('#skF_1','#skF_5','#skF_4')
| hollywood_placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3315,plain,
down('#skF_1','#skF_5','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_3081,c_438]) ).
tff(c_3080,plain,
actual_world('#skF_1'),
inference(splitRight,[status(thm)],[c_468]) ).
tff(c_464,plain,
( city('#skF_1','#skF_3')
| hollywood_placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3202,plain,
city('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_3081,c_464]) ).
tff(c_458,plain,
( chevy('#skF_1','#skF_3')
| hollywood_placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3237,plain,
chevy('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_3081,c_458]) ).
tff(c_456,plain,
( white('#skF_1','#skF_3')
| hollywood_placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3232,plain,
white('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_3081,c_456]) ).
tff(c_454,plain,
( dirty('#skF_1','#skF_3')
| hollywood_placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3239,plain,
dirty('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_3081,c_454]) ).
tff(c_452,plain,
( old('#skF_1','#skF_3')
| hollywood_placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3234,plain,
old('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_3081,c_452]) ).
tff(c_446,plain,
( event('#skF_1','#skF_5')
| hollywood_placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3216,plain,
event('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_3081,c_446]) ).
tff(c_444,plain,
( agent('#skF_1','#skF_5','#skF_3')
| hollywood_placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3259,plain,
agent('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_3081,c_444]) ).
tff(c_442,plain,
( present('#skF_1','#skF_5')
| hollywood_placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3206,plain,
present('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_3081,c_442]) ).
tff(c_440,plain,
( barrel('#skF_1','#skF_5')
| hollywood_placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3201,plain,
barrel('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_3081,c_440]) ).
tff(c_436,plain,
( in('#skF_1','#skF_5','#skF_3')
| hollywood_placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3296,plain,
in('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_3081,c_436]) ).
tff(c_434,plain,
! [X3_12,X4_13,Z_5,X1_10,X2_11] :
( ~ in(Z_5,X4_13,X3_12)
| ~ down(Z_5,X4_13,X1_10)
| ~ barrel(Z_5,X4_13)
| ~ present(Z_5,X4_13)
| ~ agent(Z_5,X4_13,X3_12)
| ~ event(Z_5,X4_13)
| ~ old(Z_5,X3_12)
| ~ dirty(Z_5,X3_12)
| ~ white(Z_5,X3_12)
| ~ chevy(Z_5,X3_12)
| ~ placename(Z_5,X2_11)
| ~ hollywood_placename(Z_5,X2_11)
| ~ city(Z_5,X3_12)
| ~ of(Z_5,X2_11,X3_12)
| ~ lonely(Z_5,X1_10)
| ~ street(Z_5,X1_10)
| ~ actual_world(Z_5)
| hollywood_placename('#skF_6','#skF_8') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3363,plain,
! [X3_202,Z_204,X2_205,X1_203,X4_206] :
( ~ in(Z_204,X4_206,X3_202)
| ~ down(Z_204,X4_206,X1_203)
| ~ barrel(Z_204,X4_206)
| ~ present(Z_204,X4_206)
| ~ agent(Z_204,X4_206,X3_202)
| ~ event(Z_204,X4_206)
| ~ old(Z_204,X3_202)
| ~ dirty(Z_204,X3_202)
| ~ white(Z_204,X3_202)
| ~ chevy(Z_204,X3_202)
| ~ placename(Z_204,X2_205)
| ~ hollywood_placename(Z_204,X2_205)
| ~ city(Z_204,X3_202)
| ~ of(Z_204,X2_205,X3_202)
| ~ lonely(Z_204,X1_203)
| ~ street(Z_204,X1_203)
| ~ actual_world(Z_204) ),
inference(negUnitSimplification,[status(thm)],[c_3081,c_434]) ).
tff(c_3365,plain,
! [X1_203,X2_205] :
( ~ down('#skF_1','#skF_5',X1_203)
| ~ barrel('#skF_1','#skF_5')
| ~ present('#skF_1','#skF_5')
| ~ agent('#skF_1','#skF_5','#skF_3')
| ~ event('#skF_1','#skF_5')
| ~ old('#skF_1','#skF_3')
| ~ dirty('#skF_1','#skF_3')
| ~ white('#skF_1','#skF_3')
| ~ chevy('#skF_1','#skF_3')
| ~ placename('#skF_1',X2_205)
| ~ hollywood_placename('#skF_1',X2_205)
| ~ city('#skF_1','#skF_3')
| ~ of('#skF_1',X2_205,'#skF_3')
| ~ lonely('#skF_1',X1_203)
| ~ street('#skF_1',X1_203)
| ~ actual_world('#skF_1') ),
inference(resolution,[status(thm)],[c_3296,c_3363]) ).
tff(c_3368,plain,
! [X1_203,X2_205] :
( ~ down('#skF_1','#skF_5',X1_203)
| ~ placename('#skF_1',X2_205)
| ~ hollywood_placename('#skF_1',X2_205)
| ~ of('#skF_1',X2_205,'#skF_3')
| ~ lonely('#skF_1',X1_203)
| ~ street('#skF_1',X1_203) ),
inference(demodulation,[status(thm),theory(equality)],[c_3080,c_3202,c_3237,c_3232,c_3239,c_3234,c_3216,c_3259,c_3206,c_3201,c_3365]) ).
tff(c_3371,plain,
! [X1_207] :
( ~ down('#skF_1','#skF_5',X1_207)
| ~ lonely('#skF_1',X1_207)
| ~ street('#skF_1',X1_207) ),
inference(splitLeft,[status(thm)],[c_3368]) ).
tff(c_3374,plain,
( ~ lonely('#skF_1','#skF_4')
| ~ street('#skF_1','#skF_4') ),
inference(resolution,[status(thm)],[c_3315,c_3371]) ).
tff(c_3378,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_3220,c_3210,c_3374]) ).
tff(c_3380,plain,
! [X2_208] :
( ~ placename('#skF_1',X2_208)
| ~ hollywood_placename('#skF_1',X2_208)
| ~ of('#skF_1',X2_208,'#skF_3') ),
inference(splitRight,[status(thm)],[c_3368]) ).
tff(c_3383,plain,
( ~ placename('#skF_1','#skF_2')
| ~ hollywood_placename('#skF_1','#skF_2') ),
inference(resolution,[status(thm)],[c_3299,c_3380]) ).
tff(c_3387,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_3212,c_3219,c_3383]) ).
tff(c_3389,plain,
~ dirty('#skF_6','#skF_9'),
inference(splitRight,[status(thm)],[c_324]) ).
tff(c_318,plain,
( hollywood_placename('#skF_1','#skF_2')
| dirty('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3428,plain,
hollywood_placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_3389,c_318]) ).
tff(c_316,plain,
( placename('#skF_1','#skF_2')
| dirty('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3452,plain,
placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_3389,c_316]) ).
tff(c_322,plain,
( of('#skF_1','#skF_2','#skF_3')
| dirty('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3640,plain,
of('#skF_1','#skF_2','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_3389,c_322]) ).
tff(c_306,plain,
( street('#skF_1','#skF_4')
| dirty('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3487,plain,
street('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_3389,c_306]) ).
tff(c_304,plain,
( lonely('#skF_1','#skF_4')
| dirty('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3484,plain,
lonely('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_3389,c_304]) ).
tff(c_294,plain,
( down('#skF_1','#skF_5','#skF_4')
| dirty('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3602,plain,
down('#skF_1','#skF_5','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_3389,c_294]) ).
tff(c_3388,plain,
actual_world('#skF_1'),
inference(splitRight,[status(thm)],[c_324]) ).
tff(c_320,plain,
( city('#skF_1','#skF_3')
| dirty('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3460,plain,
city('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_3389,c_320]) ).
tff(c_314,plain,
( chevy('#skF_1','#skF_3')
| dirty('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3473,plain,
chevy('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_3389,c_314]) ).
tff(c_312,plain,
( white('#skF_1','#skF_3')
| dirty('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3478,plain,
white('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_3389,c_312]) ).
tff(c_310,plain,
( dirty('#skF_1','#skF_3')
| dirty('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3474,plain,
dirty('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_3389,c_310]) ).
tff(c_308,plain,
( old('#skF_1','#skF_3')
| dirty('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3480,plain,
old('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_3389,c_308]) ).
tff(c_302,plain,
( event('#skF_1','#skF_5')
| dirty('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3497,plain,
event('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_3389,c_302]) ).
tff(c_300,plain,
( agent('#skF_1','#skF_5','#skF_3')
| dirty('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3564,plain,
agent('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_3389,c_300]) ).
tff(c_298,plain,
( present('#skF_1','#skF_5')
| dirty('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3515,plain,
present('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_3389,c_298]) ).
tff(c_296,plain,
( barrel('#skF_1','#skF_5')
| dirty('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3498,plain,
barrel('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_3389,c_296]) ).
tff(c_292,plain,
( in('#skF_1','#skF_5','#skF_3')
| dirty('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3551,plain,
in('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_3389,c_292]) ).
tff(c_290,plain,
! [X3_12,X4_13,Z_5,X1_10,X2_11] :
( ~ in(Z_5,X4_13,X3_12)
| ~ down(Z_5,X4_13,X1_10)
| ~ barrel(Z_5,X4_13)
| ~ present(Z_5,X4_13)
| ~ agent(Z_5,X4_13,X3_12)
| ~ event(Z_5,X4_13)
| ~ old(Z_5,X3_12)
| ~ dirty(Z_5,X3_12)
| ~ white(Z_5,X3_12)
| ~ chevy(Z_5,X3_12)
| ~ placename(Z_5,X2_11)
| ~ hollywood_placename(Z_5,X2_11)
| ~ city(Z_5,X3_12)
| ~ of(Z_5,X2_11,X3_12)
| ~ lonely(Z_5,X1_10)
| ~ street(Z_5,X1_10)
| ~ actual_world(Z_5)
| dirty('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3672,plain,
! [X3_209,X2_212,Z_211,X1_210,X4_213] :
( ~ in(Z_211,X4_213,X3_209)
| ~ down(Z_211,X4_213,X1_210)
| ~ barrel(Z_211,X4_213)
| ~ present(Z_211,X4_213)
| ~ agent(Z_211,X4_213,X3_209)
| ~ event(Z_211,X4_213)
| ~ old(Z_211,X3_209)
| ~ dirty(Z_211,X3_209)
| ~ white(Z_211,X3_209)
| ~ chevy(Z_211,X3_209)
| ~ placename(Z_211,X2_212)
| ~ hollywood_placename(Z_211,X2_212)
| ~ city(Z_211,X3_209)
| ~ of(Z_211,X2_212,X3_209)
| ~ lonely(Z_211,X1_210)
| ~ street(Z_211,X1_210)
| ~ actual_world(Z_211) ),
inference(negUnitSimplification,[status(thm)],[c_3389,c_290]) ).
tff(c_3674,plain,
! [X1_210,X2_212] :
( ~ down('#skF_1','#skF_5',X1_210)
| ~ barrel('#skF_1','#skF_5')
| ~ present('#skF_1','#skF_5')
| ~ agent('#skF_1','#skF_5','#skF_3')
| ~ event('#skF_1','#skF_5')
| ~ old('#skF_1','#skF_3')
| ~ dirty('#skF_1','#skF_3')
| ~ white('#skF_1','#skF_3')
| ~ chevy('#skF_1','#skF_3')
| ~ placename('#skF_1',X2_212)
| ~ hollywood_placename('#skF_1',X2_212)
| ~ city('#skF_1','#skF_3')
| ~ of('#skF_1',X2_212,'#skF_3')
| ~ lonely('#skF_1',X1_210)
| ~ street('#skF_1',X1_210)
| ~ actual_world('#skF_1') ),
inference(resolution,[status(thm)],[c_3551,c_3672]) ).
tff(c_3677,plain,
! [X1_210,X2_212] :
( ~ down('#skF_1','#skF_5',X1_210)
| ~ placename('#skF_1',X2_212)
| ~ hollywood_placename('#skF_1',X2_212)
| ~ of('#skF_1',X2_212,'#skF_3')
| ~ lonely('#skF_1',X1_210)
| ~ street('#skF_1',X1_210) ),
inference(demodulation,[status(thm),theory(equality)],[c_3388,c_3460,c_3473,c_3478,c_3474,c_3480,c_3497,c_3564,c_3515,c_3498,c_3674]) ).
tff(c_3680,plain,
! [X1_214] :
( ~ down('#skF_1','#skF_5',X1_214)
| ~ lonely('#skF_1',X1_214)
| ~ street('#skF_1',X1_214) ),
inference(splitLeft,[status(thm)],[c_3677]) ).
tff(c_3683,plain,
( ~ lonely('#skF_1','#skF_4')
| ~ street('#skF_1','#skF_4') ),
inference(resolution,[status(thm)],[c_3602,c_3680]) ).
tff(c_3687,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_3487,c_3484,c_3683]) ).
tff(c_3689,plain,
! [X2_215] :
( ~ placename('#skF_1',X2_215)
| ~ hollywood_placename('#skF_1',X2_215)
| ~ of('#skF_1',X2_215,'#skF_3') ),
inference(splitRight,[status(thm)],[c_3677]) ).
tff(c_3692,plain,
( ~ placename('#skF_1','#skF_2')
| ~ hollywood_placename('#skF_1','#skF_2') ),
inference(resolution,[status(thm)],[c_3640,c_3689]) ).
tff(c_3696,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_3428,c_3452,c_3692]) ).
tff(c_3698,plain,
~ event('#skF_6','#skF_10'),
inference(splitRight,[status(thm)],[c_252]) ).
tff(c_246,plain,
( hollywood_placename('#skF_1','#skF_2')
| event('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3856,plain,
hollywood_placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_3698,c_246]) ).
tff(c_244,plain,
( placename('#skF_1','#skF_2')
| event('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3850,plain,
placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_3698,c_244]) ).
tff(c_250,plain,
( of('#skF_1','#skF_2','#skF_3')
| event('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3922,plain,
of('#skF_1','#skF_2','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_3698,c_250]) ).
tff(c_234,plain,
( street('#skF_1','#skF_4')
| event('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3818,plain,
street('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_3698,c_234]) ).
tff(c_232,plain,
( lonely('#skF_1','#skF_4')
| event('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3817,plain,
lonely('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_3698,c_232]) ).
tff(c_222,plain,
( down('#skF_1','#skF_5','#skF_4')
| event('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3915,plain,
down('#skF_1','#skF_5','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_3698,c_222]) ).
tff(c_3697,plain,
actual_world('#skF_1'),
inference(splitRight,[status(thm)],[c_252]) ).
tff(c_248,plain,
( city('#skF_1','#skF_3')
| event('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3853,plain,
city('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_3698,c_248]) ).
tff(c_242,plain,
( chevy('#skF_1','#skF_3')
| event('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3860,plain,
chevy('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_3698,c_242]) ).
tff(c_240,plain,
( white('#skF_1','#skF_3')
| event('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3861,plain,
white('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_3698,c_240]) ).
tff(c_238,plain,
( dirty('#skF_1','#skF_3')
| event('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3824,plain,
dirty('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_3698,c_238]) ).
tff(c_236,plain,
( old('#skF_1','#skF_3')
| event('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3837,plain,
old('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_3698,c_236]) ).
tff(c_230,plain,
( event('#skF_1','#skF_5')
| event('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3852,plain,
event('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_3698,c_230]) ).
tff(c_228,plain,
( agent('#skF_1','#skF_5','#skF_3')
| event('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3923,plain,
agent('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_3698,c_228]) ).
tff(c_226,plain,
( present('#skF_1','#skF_5')
| event('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3815,plain,
present('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_3698,c_226]) ).
tff(c_224,plain,
( barrel('#skF_1','#skF_5')
| event('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3828,plain,
barrel('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_3698,c_224]) ).
tff(c_220,plain,
( in('#skF_1','#skF_5','#skF_3')
| event('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3954,plain,
in('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_3698,c_220]) ).
tff(c_218,plain,
! [X3_12,X4_13,Z_5,X1_10,X2_11] :
( ~ in(Z_5,X4_13,X3_12)
| ~ down(Z_5,X4_13,X1_10)
| ~ barrel(Z_5,X4_13)
| ~ present(Z_5,X4_13)
| ~ agent(Z_5,X4_13,X3_12)
| ~ event(Z_5,X4_13)
| ~ old(Z_5,X3_12)
| ~ dirty(Z_5,X3_12)
| ~ white(Z_5,X3_12)
| ~ chevy(Z_5,X3_12)
| ~ placename(Z_5,X2_11)
| ~ hollywood_placename(Z_5,X2_11)
| ~ city(Z_5,X3_12)
| ~ of(Z_5,X2_11,X3_12)
| ~ lonely(Z_5,X1_10)
| ~ street(Z_5,X1_10)
| ~ actual_world(Z_5)
| event('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_3979,plain,
! [X2_219,X3_216,X4_220,X1_217,Z_218] :
( ~ in(Z_218,X4_220,X3_216)
| ~ down(Z_218,X4_220,X1_217)
| ~ barrel(Z_218,X4_220)
| ~ present(Z_218,X4_220)
| ~ agent(Z_218,X4_220,X3_216)
| ~ event(Z_218,X4_220)
| ~ old(Z_218,X3_216)
| ~ dirty(Z_218,X3_216)
| ~ white(Z_218,X3_216)
| ~ chevy(Z_218,X3_216)
| ~ placename(Z_218,X2_219)
| ~ hollywood_placename(Z_218,X2_219)
| ~ city(Z_218,X3_216)
| ~ of(Z_218,X2_219,X3_216)
| ~ lonely(Z_218,X1_217)
| ~ street(Z_218,X1_217)
| ~ actual_world(Z_218) ),
inference(negUnitSimplification,[status(thm)],[c_3698,c_218]) ).
tff(c_3981,plain,
! [X1_217,X2_219] :
( ~ down('#skF_1','#skF_5',X1_217)
| ~ barrel('#skF_1','#skF_5')
| ~ present('#skF_1','#skF_5')
| ~ agent('#skF_1','#skF_5','#skF_3')
| ~ event('#skF_1','#skF_5')
| ~ old('#skF_1','#skF_3')
| ~ dirty('#skF_1','#skF_3')
| ~ white('#skF_1','#skF_3')
| ~ chevy('#skF_1','#skF_3')
| ~ placename('#skF_1',X2_219)
| ~ hollywood_placename('#skF_1',X2_219)
| ~ city('#skF_1','#skF_3')
| ~ of('#skF_1',X2_219,'#skF_3')
| ~ lonely('#skF_1',X1_217)
| ~ street('#skF_1',X1_217)
| ~ actual_world('#skF_1') ),
inference(resolution,[status(thm)],[c_3954,c_3979]) ).
tff(c_3984,plain,
! [X1_217,X2_219] :
( ~ down('#skF_1','#skF_5',X1_217)
| ~ placename('#skF_1',X2_219)
| ~ hollywood_placename('#skF_1',X2_219)
| ~ of('#skF_1',X2_219,'#skF_3')
| ~ lonely('#skF_1',X1_217)
| ~ street('#skF_1',X1_217) ),
inference(demodulation,[status(thm),theory(equality)],[c_3697,c_3853,c_3860,c_3861,c_3824,c_3837,c_3852,c_3923,c_3815,c_3828,c_3981]) ).
tff(c_3987,plain,
! [X1_221] :
( ~ down('#skF_1','#skF_5',X1_221)
| ~ lonely('#skF_1',X1_221)
| ~ street('#skF_1',X1_221) ),
inference(splitLeft,[status(thm)],[c_3984]) ).
tff(c_3990,plain,
( ~ lonely('#skF_1','#skF_4')
| ~ street('#skF_1','#skF_4') ),
inference(resolution,[status(thm)],[c_3915,c_3987]) ).
tff(c_3994,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_3818,c_3817,c_3990]) ).
tff(c_3996,plain,
! [X2_222] :
( ~ placename('#skF_1',X2_222)
| ~ hollywood_placename('#skF_1',X2_222)
| ~ of('#skF_1',X2_222,'#skF_3') ),
inference(splitRight,[status(thm)],[c_3984]) ).
tff(c_3999,plain,
( ~ placename('#skF_1','#skF_2')
| ~ hollywood_placename('#skF_1','#skF_2') ),
inference(resolution,[status(thm)],[c_3922,c_3996]) ).
tff(c_4003,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_3856,c_3850,c_3999]) ).
tff(c_4005,plain,
~ present('#skF_6','#skF_10'),
inference(splitRight,[status(thm)],[c_180]) ).
tff(c_174,plain,
( hollywood_placename('#skF_1','#skF_2')
| present('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4094,plain,
hollywood_placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_4005,c_174]) ).
tff(c_172,plain,
( placename('#skF_1','#skF_2')
| present('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4090,plain,
placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_4005,c_172]) ).
tff(c_178,plain,
( of('#skF_1','#skF_2','#skF_3')
| present('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4268,plain,
of('#skF_1','#skF_2','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4005,c_178]) ).
tff(c_162,plain,
( street('#skF_1','#skF_4')
| present('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4089,plain,
street('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_4005,c_162]) ).
tff(c_160,plain,
( lonely('#skF_1','#skF_4')
| present('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4087,plain,
lonely('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_4005,c_160]) ).
tff(c_150,plain,
( down('#skF_1','#skF_5','#skF_4')
| present('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4185,plain,
down('#skF_1','#skF_5','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_4005,c_150]) ).
tff(c_4004,plain,
actual_world('#skF_1'),
inference(splitRight,[status(thm)],[c_180]) ).
tff(c_176,plain,
( city('#skF_1','#skF_3')
| present('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4109,plain,
city('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4005,c_176]) ).
tff(c_170,plain,
( chevy('#skF_1','#skF_3')
| present('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4081,plain,
chevy('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4005,c_170]) ).
tff(c_168,plain,
( white('#skF_1','#skF_3')
| present('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4093,plain,
white('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4005,c_168]) ).
tff(c_166,plain,
( dirty('#skF_1','#skF_3')
| present('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4085,plain,
dirty('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4005,c_166]) ).
tff(c_164,plain,
( old('#skF_1','#skF_3')
| present('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4083,plain,
old('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4005,c_164]) ).
tff(c_158,plain,
( event('#skF_1','#skF_5')
| present('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4082,plain,
event('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_4005,c_158]) ).
tff(c_156,plain,
( agent('#skF_1','#skF_5','#skF_3')
| present('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4261,plain,
agent('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4005,c_156]) ).
tff(c_154,plain,
( present('#skF_1','#skF_5')
| present('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4072,plain,
present('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_4005,c_154]) ).
tff(c_152,plain,
( barrel('#skF_1','#skF_5')
| present('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4071,plain,
barrel('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_4005,c_152]) ).
tff(c_148,plain,
( in('#skF_1','#skF_5','#skF_3')
| present('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4177,plain,
in('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4005,c_148]) ).
tff(c_146,plain,
! [X3_12,X4_13,Z_5,X1_10,X2_11] :
( ~ in(Z_5,X4_13,X3_12)
| ~ down(Z_5,X4_13,X1_10)
| ~ barrel(Z_5,X4_13)
| ~ present(Z_5,X4_13)
| ~ agent(Z_5,X4_13,X3_12)
| ~ event(Z_5,X4_13)
| ~ old(Z_5,X3_12)
| ~ dirty(Z_5,X3_12)
| ~ white(Z_5,X3_12)
| ~ chevy(Z_5,X3_12)
| ~ placename(Z_5,X2_11)
| ~ hollywood_placename(Z_5,X2_11)
| ~ city(Z_5,X3_12)
| ~ of(Z_5,X2_11,X3_12)
| ~ lonely(Z_5,X1_10)
| ~ street(Z_5,X1_10)
| ~ actual_world(Z_5)
| present('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4303,plain,
! [X2_226,X4_227,X1_224,Z_225,X3_223] :
( ~ in(Z_225,X4_227,X3_223)
| ~ down(Z_225,X4_227,X1_224)
| ~ barrel(Z_225,X4_227)
| ~ present(Z_225,X4_227)
| ~ agent(Z_225,X4_227,X3_223)
| ~ event(Z_225,X4_227)
| ~ old(Z_225,X3_223)
| ~ dirty(Z_225,X3_223)
| ~ white(Z_225,X3_223)
| ~ chevy(Z_225,X3_223)
| ~ placename(Z_225,X2_226)
| ~ hollywood_placename(Z_225,X2_226)
| ~ city(Z_225,X3_223)
| ~ of(Z_225,X2_226,X3_223)
| ~ lonely(Z_225,X1_224)
| ~ street(Z_225,X1_224)
| ~ actual_world(Z_225) ),
inference(negUnitSimplification,[status(thm)],[c_4005,c_146]) ).
tff(c_4305,plain,
! [X1_224,X2_226] :
( ~ down('#skF_1','#skF_5',X1_224)
| ~ barrel('#skF_1','#skF_5')
| ~ present('#skF_1','#skF_5')
| ~ agent('#skF_1','#skF_5','#skF_3')
| ~ event('#skF_1','#skF_5')
| ~ old('#skF_1','#skF_3')
| ~ dirty('#skF_1','#skF_3')
| ~ white('#skF_1','#skF_3')
| ~ chevy('#skF_1','#skF_3')
| ~ placename('#skF_1',X2_226)
| ~ hollywood_placename('#skF_1',X2_226)
| ~ city('#skF_1','#skF_3')
| ~ of('#skF_1',X2_226,'#skF_3')
| ~ lonely('#skF_1',X1_224)
| ~ street('#skF_1',X1_224)
| ~ actual_world('#skF_1') ),
inference(resolution,[status(thm)],[c_4177,c_4303]) ).
tff(c_4308,plain,
! [X1_224,X2_226] :
( ~ down('#skF_1','#skF_5',X1_224)
| ~ placename('#skF_1',X2_226)
| ~ hollywood_placename('#skF_1',X2_226)
| ~ of('#skF_1',X2_226,'#skF_3')
| ~ lonely('#skF_1',X1_224)
| ~ street('#skF_1',X1_224) ),
inference(demodulation,[status(thm),theory(equality)],[c_4004,c_4109,c_4081,c_4093,c_4085,c_4083,c_4082,c_4261,c_4072,c_4071,c_4305]) ).
tff(c_4310,plain,
! [X1_228] :
( ~ down('#skF_1','#skF_5',X1_228)
| ~ lonely('#skF_1',X1_228)
| ~ street('#skF_1',X1_228) ),
inference(splitLeft,[status(thm)],[c_4308]) ).
tff(c_4313,plain,
( ~ lonely('#skF_1','#skF_4')
| ~ street('#skF_1','#skF_4') ),
inference(resolution,[status(thm)],[c_4185,c_4310]) ).
tff(c_4317,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4089,c_4087,c_4313]) ).
tff(c_4320,plain,
! [X2_229] :
( ~ placename('#skF_1',X2_229)
| ~ hollywood_placename('#skF_1',X2_229)
| ~ of('#skF_1',X2_229,'#skF_3') ),
inference(splitRight,[status(thm)],[c_4308]) ).
tff(c_4323,plain,
( ~ placename('#skF_1','#skF_2')
| ~ hollywood_placename('#skF_1','#skF_2') ),
inference(resolution,[status(thm)],[c_4268,c_4320]) ).
tff(c_4327,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4094,c_4090,c_4323]) ).
tff(c_4329,plain,
~ street('#skF_6','#skF_7'),
inference(splitRight,[status(thm)],[c_612]) ).
tff(c_606,plain,
( hollywood_placename('#skF_1','#skF_2')
| street('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4455,plain,
hollywood_placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_4329,c_606]) ).
tff(c_604,plain,
( placename('#skF_1','#skF_2')
| street('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4451,plain,
placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_4329,c_604]) ).
tff(c_610,plain,
( of('#skF_1','#skF_2','#skF_3')
| street('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4570,plain,
of('#skF_1','#skF_2','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4329,c_610]) ).
tff(c_594,plain,
( street('#skF_1','#skF_4')
| street('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4432,plain,
street('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_4329,c_594]) ).
tff(c_592,plain,
( lonely('#skF_1','#skF_4')
| street('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4430,plain,
lonely('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_4329,c_592]) ).
tff(c_582,plain,
( down('#skF_1','#skF_5','#skF_4')
| street('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4560,plain,
down('#skF_1','#skF_5','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_4329,c_582]) ).
tff(c_4328,plain,
actual_world('#skF_1'),
inference(splitRight,[status(thm)],[c_612]) ).
tff(c_608,plain,
( city('#skF_1','#skF_3')
| street('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4424,plain,
city('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4329,c_608]) ).
tff(c_602,plain,
( chevy('#skF_1','#skF_3')
| street('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4490,plain,
chevy('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4329,c_602]) ).
tff(c_600,plain,
( white('#skF_1','#skF_3')
| street('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4483,plain,
white('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4329,c_600]) ).
tff(c_598,plain,
( dirty('#skF_1','#skF_3')
| street('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4495,plain,
dirty('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4329,c_598]) ).
tff(c_596,plain,
( old('#skF_1','#skF_3')
| street('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4441,plain,
old('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4329,c_596]) ).
tff(c_590,plain,
( event('#skF_1','#skF_5')
| street('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4408,plain,
event('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_4329,c_590]) ).
tff(c_588,plain,
( agent('#skF_1','#skF_5','#skF_3')
| street('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4533,plain,
agent('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4329,c_588]) ).
tff(c_586,plain,
( present('#skF_1','#skF_5')
| street('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4351,plain,
present('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_4329,c_586]) ).
tff(c_584,plain,
( barrel('#skF_1','#skF_5')
| street('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4386,plain,
barrel('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_4329,c_584]) ).
tff(c_580,plain,
( in('#skF_1','#skF_5','#skF_3')
| street('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4588,plain,
in('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4329,c_580]) ).
tff(c_578,plain,
! [X3_12,X4_13,Z_5,X1_10,X2_11] :
( ~ in(Z_5,X4_13,X3_12)
| ~ down(Z_5,X4_13,X1_10)
| ~ barrel(Z_5,X4_13)
| ~ present(Z_5,X4_13)
| ~ agent(Z_5,X4_13,X3_12)
| ~ event(Z_5,X4_13)
| ~ old(Z_5,X3_12)
| ~ dirty(Z_5,X3_12)
| ~ white(Z_5,X3_12)
| ~ chevy(Z_5,X3_12)
| ~ placename(Z_5,X2_11)
| ~ hollywood_placename(Z_5,X2_11)
| ~ city(Z_5,X3_12)
| ~ of(Z_5,X2_11,X3_12)
| ~ lonely(Z_5,X1_10)
| ~ street(Z_5,X1_10)
| ~ actual_world(Z_5)
| street('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4623,plain,
! [X4_234,X2_233,X3_230,Z_232,X1_231] :
( ~ in(Z_232,X4_234,X3_230)
| ~ down(Z_232,X4_234,X1_231)
| ~ barrel(Z_232,X4_234)
| ~ present(Z_232,X4_234)
| ~ agent(Z_232,X4_234,X3_230)
| ~ event(Z_232,X4_234)
| ~ old(Z_232,X3_230)
| ~ dirty(Z_232,X3_230)
| ~ white(Z_232,X3_230)
| ~ chevy(Z_232,X3_230)
| ~ placename(Z_232,X2_233)
| ~ hollywood_placename(Z_232,X2_233)
| ~ city(Z_232,X3_230)
| ~ of(Z_232,X2_233,X3_230)
| ~ lonely(Z_232,X1_231)
| ~ street(Z_232,X1_231)
| ~ actual_world(Z_232) ),
inference(negUnitSimplification,[status(thm)],[c_4329,c_578]) ).
tff(c_4625,plain,
! [X1_231,X2_233] :
( ~ down('#skF_1','#skF_5',X1_231)
| ~ barrel('#skF_1','#skF_5')
| ~ present('#skF_1','#skF_5')
| ~ agent('#skF_1','#skF_5','#skF_3')
| ~ event('#skF_1','#skF_5')
| ~ old('#skF_1','#skF_3')
| ~ dirty('#skF_1','#skF_3')
| ~ white('#skF_1','#skF_3')
| ~ chevy('#skF_1','#skF_3')
| ~ placename('#skF_1',X2_233)
| ~ hollywood_placename('#skF_1',X2_233)
| ~ city('#skF_1','#skF_3')
| ~ of('#skF_1',X2_233,'#skF_3')
| ~ lonely('#skF_1',X1_231)
| ~ street('#skF_1',X1_231)
| ~ actual_world('#skF_1') ),
inference(resolution,[status(thm)],[c_4588,c_4623]) ).
tff(c_4628,plain,
! [X1_231,X2_233] :
( ~ down('#skF_1','#skF_5',X1_231)
| ~ placename('#skF_1',X2_233)
| ~ hollywood_placename('#skF_1',X2_233)
| ~ of('#skF_1',X2_233,'#skF_3')
| ~ lonely('#skF_1',X1_231)
| ~ street('#skF_1',X1_231) ),
inference(demodulation,[status(thm),theory(equality)],[c_4328,c_4424,c_4490,c_4483,c_4495,c_4441,c_4408,c_4533,c_4351,c_4386,c_4625]) ).
tff(c_4631,plain,
! [X1_235] :
( ~ down('#skF_1','#skF_5',X1_235)
| ~ lonely('#skF_1',X1_235)
| ~ street('#skF_1',X1_235) ),
inference(splitLeft,[status(thm)],[c_4628]) ).
tff(c_4634,plain,
( ~ lonely('#skF_1','#skF_4')
| ~ street('#skF_1','#skF_4') ),
inference(resolution,[status(thm)],[c_4560,c_4631]) ).
tff(c_4638,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4432,c_4430,c_4634]) ).
tff(c_4640,plain,
! [X2_236] :
( ~ placename('#skF_1',X2_236)
| ~ hollywood_placename('#skF_1',X2_236)
| ~ of('#skF_1',X2_236,'#skF_3') ),
inference(splitRight,[status(thm)],[c_4628]) ).
tff(c_4643,plain,
( ~ placename('#skF_1','#skF_2')
| ~ hollywood_placename('#skF_1','#skF_2') ),
inference(resolution,[status(thm)],[c_4570,c_4640]) ).
tff(c_4647,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4455,c_4451,c_4643]) ).
tff(c_4649,plain,
~ city('#skF_6','#skF_9'),
inference(splitRight,[status(thm)],[c_504]) ).
tff(c_498,plain,
( hollywood_placename('#skF_1','#skF_2')
| city('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4690,plain,
hollywood_placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_4649,c_498]) ).
tff(c_496,plain,
( placename('#skF_1','#skF_2')
| city('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4686,plain,
placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_4649,c_496]) ).
tff(c_502,plain,
( of('#skF_1','#skF_2','#skF_3')
| city('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4897,plain,
of('#skF_1','#skF_2','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4649,c_502]) ).
tff(c_486,plain,
( street('#skF_1','#skF_4')
| city('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4739,plain,
street('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_4649,c_486]) ).
tff(c_484,plain,
( lonely('#skF_1','#skF_4')
| city('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4720,plain,
lonely('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_4649,c_484]) ).
tff(c_474,plain,
( down('#skF_1','#skF_5','#skF_4')
| city('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4846,plain,
down('#skF_1','#skF_5','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_4649,c_474]) ).
tff(c_4648,plain,
actual_world('#skF_1'),
inference(splitRight,[status(thm)],[c_504]) ).
tff(c_500,plain,
( city('#skF_1','#skF_3')
| city('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4702,plain,
city('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4649,c_500]) ).
tff(c_494,plain,
( chevy('#skF_1','#skF_3')
| city('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4788,plain,
chevy('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4649,c_494]) ).
tff(c_492,plain,
( white('#skF_1','#skF_3')
| city('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4711,plain,
white('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4649,c_492]) ).
tff(c_490,plain,
( dirty('#skF_1','#skF_3')
| city('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4806,plain,
dirty('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4649,c_490]) ).
tff(c_488,plain,
( old('#skF_1','#skF_3')
| city('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4731,plain,
old('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4649,c_488]) ).
tff(c_482,plain,
( event('#skF_1','#skF_5')
| city('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4741,plain,
event('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_4649,c_482]) ).
tff(c_480,plain,
( agent('#skF_1','#skF_5','#skF_3')
| city('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4819,plain,
agent('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4649,c_480]) ).
tff(c_478,plain,
( present('#skF_1','#skF_5')
| city('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4749,plain,
present('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_4649,c_478]) ).
tff(c_476,plain,
( barrel('#skF_1','#skF_5')
| city('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4768,plain,
barrel('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_4649,c_476]) ).
tff(c_472,plain,
( in('#skF_1','#skF_5','#skF_3')
| city('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4900,plain,
in('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4649,c_472]) ).
tff(c_470,plain,
! [X3_12,X4_13,Z_5,X1_10,X2_11] :
( ~ in(Z_5,X4_13,X3_12)
| ~ down(Z_5,X4_13,X1_10)
| ~ barrel(Z_5,X4_13)
| ~ present(Z_5,X4_13)
| ~ agent(Z_5,X4_13,X3_12)
| ~ event(Z_5,X4_13)
| ~ old(Z_5,X3_12)
| ~ dirty(Z_5,X3_12)
| ~ white(Z_5,X3_12)
| ~ chevy(Z_5,X3_12)
| ~ placename(Z_5,X2_11)
| ~ hollywood_placename(Z_5,X2_11)
| ~ city(Z_5,X3_12)
| ~ of(Z_5,X2_11,X3_12)
| ~ lonely(Z_5,X1_10)
| ~ street(Z_5,X1_10)
| ~ actual_world(Z_5)
| city('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_4951,plain,
! [X4_241,X2_240,Z_239,X3_237,X1_238] :
( ~ in(Z_239,X4_241,X3_237)
| ~ down(Z_239,X4_241,X1_238)
| ~ barrel(Z_239,X4_241)
| ~ present(Z_239,X4_241)
| ~ agent(Z_239,X4_241,X3_237)
| ~ event(Z_239,X4_241)
| ~ old(Z_239,X3_237)
| ~ dirty(Z_239,X3_237)
| ~ white(Z_239,X3_237)
| ~ chevy(Z_239,X3_237)
| ~ placename(Z_239,X2_240)
| ~ hollywood_placename(Z_239,X2_240)
| ~ city(Z_239,X3_237)
| ~ of(Z_239,X2_240,X3_237)
| ~ lonely(Z_239,X1_238)
| ~ street(Z_239,X1_238)
| ~ actual_world(Z_239) ),
inference(negUnitSimplification,[status(thm)],[c_4649,c_470]) ).
tff(c_4953,plain,
! [X1_238,X2_240] :
( ~ down('#skF_1','#skF_5',X1_238)
| ~ barrel('#skF_1','#skF_5')
| ~ present('#skF_1','#skF_5')
| ~ agent('#skF_1','#skF_5','#skF_3')
| ~ event('#skF_1','#skF_5')
| ~ old('#skF_1','#skF_3')
| ~ dirty('#skF_1','#skF_3')
| ~ white('#skF_1','#skF_3')
| ~ chevy('#skF_1','#skF_3')
| ~ placename('#skF_1',X2_240)
| ~ hollywood_placename('#skF_1',X2_240)
| ~ city('#skF_1','#skF_3')
| ~ of('#skF_1',X2_240,'#skF_3')
| ~ lonely('#skF_1',X1_238)
| ~ street('#skF_1',X1_238)
| ~ actual_world('#skF_1') ),
inference(resolution,[status(thm)],[c_4900,c_4951]) ).
tff(c_4956,plain,
! [X1_238,X2_240] :
( ~ down('#skF_1','#skF_5',X1_238)
| ~ placename('#skF_1',X2_240)
| ~ hollywood_placename('#skF_1',X2_240)
| ~ of('#skF_1',X2_240,'#skF_3')
| ~ lonely('#skF_1',X1_238)
| ~ street('#skF_1',X1_238) ),
inference(demodulation,[status(thm),theory(equality)],[c_4648,c_4702,c_4788,c_4711,c_4806,c_4731,c_4741,c_4819,c_4749,c_4768,c_4953]) ).
tff(c_4958,plain,
! [X1_242] :
( ~ down('#skF_1','#skF_5',X1_242)
| ~ lonely('#skF_1',X1_242)
| ~ street('#skF_1',X1_242) ),
inference(splitLeft,[status(thm)],[c_4956]) ).
tff(c_4961,plain,
( ~ lonely('#skF_1','#skF_4')
| ~ street('#skF_1','#skF_4') ),
inference(resolution,[status(thm)],[c_4846,c_4958]) ).
tff(c_4965,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4739,c_4720,c_4961]) ).
tff(c_4967,plain,
! [X2_243] :
( ~ placename('#skF_1',X2_243)
| ~ hollywood_placename('#skF_1',X2_243)
| ~ of('#skF_1',X2_243,'#skF_3') ),
inference(splitRight,[status(thm)],[c_4956]) ).
tff(c_4970,plain,
( ~ placename('#skF_1','#skF_2')
| ~ hollywood_placename('#skF_1','#skF_2') ),
inference(resolution,[status(thm)],[c_4897,c_4967]) ).
tff(c_4974,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_4690,c_4686,c_4970]) ).
tff(c_4976,plain,
~ white('#skF_6','#skF_9'),
inference(splitRight,[status(thm)],[c_360]) ).
tff(c_354,plain,
( hollywood_placename('#skF_1','#skF_2')
| white('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5023,plain,
hollywood_placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_4976,c_354]) ).
tff(c_352,plain,
( placename('#skF_1','#skF_2')
| white('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5022,plain,
placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_4976,c_352]) ).
tff(c_358,plain,
( of('#skF_1','#skF_2','#skF_3')
| white('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5168,plain,
of('#skF_1','#skF_2','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4976,c_358]) ).
tff(c_342,plain,
( street('#skF_1','#skF_4')
| white('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5004,plain,
street('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_4976,c_342]) ).
tff(c_340,plain,
( lonely('#skF_1','#skF_4')
| white('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5011,plain,
lonely('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_4976,c_340]) ).
tff(c_330,plain,
( down('#skF_1','#skF_5','#skF_4')
| white('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5220,plain,
down('#skF_1','#skF_5','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_4976,c_330]) ).
tff(c_4975,plain,
actual_world('#skF_1'),
inference(splitRight,[status(thm)],[c_360]) ).
tff(c_356,plain,
( city('#skF_1','#skF_3')
| white('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5031,plain,
city('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4976,c_356]) ).
tff(c_350,plain,
( chevy('#skF_1','#skF_3')
| white('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5018,plain,
chevy('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4976,c_350]) ).
tff(c_348,plain,
( white('#skF_1','#skF_3')
| white('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5013,plain,
white('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4976,c_348]) ).
tff(c_346,plain,
( dirty('#skF_1','#skF_3')
| white('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5008,plain,
dirty('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4976,c_346]) ).
tff(c_344,plain,
( old('#skF_1','#skF_3')
| white('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5006,plain,
old('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4976,c_344]) ).
tff(c_338,plain,
( event('#skF_1','#skF_5')
| white('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5000,plain,
event('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_4976,c_338]) ).
tff(c_336,plain,
( agent('#skF_1','#skF_5','#skF_3')
| white('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5215,plain,
agent('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4976,c_336]) ).
tff(c_334,plain,
( present('#skF_1','#skF_5')
| white('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5045,plain,
present('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_4976,c_334]) ).
tff(c_332,plain,
( barrel('#skF_1','#skF_5')
| white('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5050,plain,
barrel('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_4976,c_332]) ).
tff(c_328,plain,
( in('#skF_1','#skF_5','#skF_3')
| white('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5154,plain,
in('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_4976,c_328]) ).
tff(c_326,plain,
! [X3_12,X4_13,Z_5,X1_10,X2_11] :
( ~ in(Z_5,X4_13,X3_12)
| ~ down(Z_5,X4_13,X1_10)
| ~ barrel(Z_5,X4_13)
| ~ present(Z_5,X4_13)
| ~ agent(Z_5,X4_13,X3_12)
| ~ event(Z_5,X4_13)
| ~ old(Z_5,X3_12)
| ~ dirty(Z_5,X3_12)
| ~ white(Z_5,X3_12)
| ~ chevy(Z_5,X3_12)
| ~ placename(Z_5,X2_11)
| ~ hollywood_placename(Z_5,X2_11)
| ~ city(Z_5,X3_12)
| ~ of(Z_5,X2_11,X3_12)
| ~ lonely(Z_5,X1_10)
| ~ street(Z_5,X1_10)
| ~ actual_world(Z_5)
| white('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5309,plain,
! [Z_253,X1_252,X4_255,X2_254,X3_251] :
( ~ in(Z_253,X4_255,X3_251)
| ~ down(Z_253,X4_255,X1_252)
| ~ barrel(Z_253,X4_255)
| ~ present(Z_253,X4_255)
| ~ agent(Z_253,X4_255,X3_251)
| ~ event(Z_253,X4_255)
| ~ old(Z_253,X3_251)
| ~ dirty(Z_253,X3_251)
| ~ white(Z_253,X3_251)
| ~ chevy(Z_253,X3_251)
| ~ placename(Z_253,X2_254)
| ~ hollywood_placename(Z_253,X2_254)
| ~ city(Z_253,X3_251)
| ~ of(Z_253,X2_254,X3_251)
| ~ lonely(Z_253,X1_252)
| ~ street(Z_253,X1_252)
| ~ actual_world(Z_253) ),
inference(negUnitSimplification,[status(thm)],[c_4976,c_326]) ).
tff(c_5311,plain,
! [X1_252,X2_254] :
( ~ down('#skF_1','#skF_5',X1_252)
| ~ barrel('#skF_1','#skF_5')
| ~ present('#skF_1','#skF_5')
| ~ agent('#skF_1','#skF_5','#skF_3')
| ~ event('#skF_1','#skF_5')
| ~ old('#skF_1','#skF_3')
| ~ dirty('#skF_1','#skF_3')
| ~ white('#skF_1','#skF_3')
| ~ chevy('#skF_1','#skF_3')
| ~ placename('#skF_1',X2_254)
| ~ hollywood_placename('#skF_1',X2_254)
| ~ city('#skF_1','#skF_3')
| ~ of('#skF_1',X2_254,'#skF_3')
| ~ lonely('#skF_1',X1_252)
| ~ street('#skF_1',X1_252)
| ~ actual_world('#skF_1') ),
inference(resolution,[status(thm)],[c_5154,c_5309]) ).
tff(c_5314,plain,
! [X1_252,X2_254] :
( ~ down('#skF_1','#skF_5',X1_252)
| ~ placename('#skF_1',X2_254)
| ~ hollywood_placename('#skF_1',X2_254)
| ~ of('#skF_1',X2_254,'#skF_3')
| ~ lonely('#skF_1',X1_252)
| ~ street('#skF_1',X1_252) ),
inference(demodulation,[status(thm),theory(equality)],[c_4975,c_5031,c_5018,c_5013,c_5008,c_5006,c_5000,c_5215,c_5045,c_5050,c_5311]) ).
tff(c_5316,plain,
! [X1_256] :
( ~ down('#skF_1','#skF_5',X1_256)
| ~ lonely('#skF_1',X1_256)
| ~ street('#skF_1',X1_256) ),
inference(splitLeft,[status(thm)],[c_5314]) ).
tff(c_5319,plain,
( ~ lonely('#skF_1','#skF_4')
| ~ street('#skF_1','#skF_4') ),
inference(resolution,[status(thm)],[c_5220,c_5316]) ).
tff(c_5323,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_5004,c_5011,c_5319]) ).
tff(c_5326,plain,
! [X2_257] :
( ~ placename('#skF_1',X2_257)
| ~ hollywood_placename('#skF_1',X2_257)
| ~ of('#skF_1',X2_257,'#skF_3') ),
inference(splitRight,[status(thm)],[c_5314]) ).
tff(c_5329,plain,
( ~ placename('#skF_1','#skF_2')
| ~ hollywood_placename('#skF_1','#skF_2') ),
inference(resolution,[status(thm)],[c_5168,c_5326]) ).
tff(c_5333,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_5023,c_5022,c_5329]) ).
tff(c_5335,plain,
~ chevy('#skF_6','#skF_9'),
inference(splitRight,[status(thm)],[c_396]) ).
tff(c_390,plain,
( hollywood_placename('#skF_1','#skF_2')
| chevy('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5369,plain,
hollywood_placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_5335,c_390]) ).
tff(c_388,plain,
( placename('#skF_1','#skF_2')
| chevy('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5358,plain,
placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_5335,c_388]) ).
tff(c_394,plain,
( of('#skF_1','#skF_2','#skF_3')
| chevy('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5513,plain,
of('#skF_1','#skF_2','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_5335,c_394]) ).
tff(c_378,plain,
( street('#skF_1','#skF_4')
| chevy('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5392,plain,
street('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_5335,c_378]) ).
tff(c_376,plain,
( lonely('#skF_1','#skF_4')
| chevy('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5391,plain,
lonely('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_5335,c_376]) ).
tff(c_366,plain,
( down('#skF_1','#skF_5','#skF_4')
| chevy('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5556,plain,
down('#skF_1','#skF_5','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_5335,c_366]) ).
tff(c_5334,plain,
actual_world('#skF_1'),
inference(splitRight,[status(thm)],[c_396]) ).
tff(c_392,plain,
( city('#skF_1','#skF_3')
| chevy('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5400,plain,
city('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_5335,c_392]) ).
tff(c_386,plain,
( chevy('#skF_1','#skF_3')
| chevy('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5388,plain,
chevy('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_5335,c_386]) ).
tff(c_384,plain,
( white('#skF_1','#skF_3')
| chevy('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5384,plain,
white('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_5335,c_384]) ).
tff(c_382,plain,
( dirty('#skF_1','#skF_3')
| chevy('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5383,plain,
dirty('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_5335,c_382]) ).
tff(c_380,plain,
( old('#skF_1','#skF_3')
| chevy('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5398,plain,
old('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_5335,c_380]) ).
tff(c_374,plain,
( event('#skF_1','#skF_5')
| chevy('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5395,plain,
event('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_5335,c_374]) ).
tff(c_372,plain,
( agent('#skF_1','#skF_5','#skF_3')
| chevy('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5510,plain,
agent('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_5335,c_372]) ).
tff(c_370,plain,
( present('#skF_1','#skF_5')
| chevy('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5390,plain,
present('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_5335,c_370]) ).
tff(c_368,plain,
( barrel('#skF_1','#skF_5')
| chevy('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5382,plain,
barrel('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_5335,c_368]) ).
tff(c_364,plain,
( in('#skF_1','#skF_5','#skF_3')
| chevy('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5515,plain,
in('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_5335,c_364]) ).
tff(c_362,plain,
! [X3_12,X4_13,Z_5,X1_10,X2_11] :
( ~ in(Z_5,X4_13,X3_12)
| ~ down(Z_5,X4_13,X1_10)
| ~ barrel(Z_5,X4_13)
| ~ present(Z_5,X4_13)
| ~ agent(Z_5,X4_13,X3_12)
| ~ event(Z_5,X4_13)
| ~ old(Z_5,X3_12)
| ~ dirty(Z_5,X3_12)
| ~ white(Z_5,X3_12)
| ~ chevy(Z_5,X3_12)
| ~ placename(Z_5,X2_11)
| ~ hollywood_placename(Z_5,X2_11)
| ~ city(Z_5,X3_12)
| ~ of(Z_5,X2_11,X3_12)
| ~ lonely(Z_5,X1_10)
| ~ street(Z_5,X1_10)
| ~ actual_world(Z_5)
| chevy('#skF_6','#skF_9') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5697,plain,
! [X1_273,X2_275,Z_274,X4_276,X3_272] :
( ~ in(Z_274,X4_276,X3_272)
| ~ down(Z_274,X4_276,X1_273)
| ~ barrel(Z_274,X4_276)
| ~ present(Z_274,X4_276)
| ~ agent(Z_274,X4_276,X3_272)
| ~ event(Z_274,X4_276)
| ~ old(Z_274,X3_272)
| ~ dirty(Z_274,X3_272)
| ~ white(Z_274,X3_272)
| ~ chevy(Z_274,X3_272)
| ~ placename(Z_274,X2_275)
| ~ hollywood_placename(Z_274,X2_275)
| ~ city(Z_274,X3_272)
| ~ of(Z_274,X2_275,X3_272)
| ~ lonely(Z_274,X1_273)
| ~ street(Z_274,X1_273)
| ~ actual_world(Z_274) ),
inference(negUnitSimplification,[status(thm)],[c_5335,c_362]) ).
tff(c_5699,plain,
! [X1_273,X2_275] :
( ~ down('#skF_1','#skF_5',X1_273)
| ~ barrel('#skF_1','#skF_5')
| ~ present('#skF_1','#skF_5')
| ~ agent('#skF_1','#skF_5','#skF_3')
| ~ event('#skF_1','#skF_5')
| ~ old('#skF_1','#skF_3')
| ~ dirty('#skF_1','#skF_3')
| ~ white('#skF_1','#skF_3')
| ~ chevy('#skF_1','#skF_3')
| ~ placename('#skF_1',X2_275)
| ~ hollywood_placename('#skF_1',X2_275)
| ~ city('#skF_1','#skF_3')
| ~ of('#skF_1',X2_275,'#skF_3')
| ~ lonely('#skF_1',X1_273)
| ~ street('#skF_1',X1_273)
| ~ actual_world('#skF_1') ),
inference(resolution,[status(thm)],[c_5515,c_5697]) ).
tff(c_5702,plain,
! [X1_273,X2_275] :
( ~ down('#skF_1','#skF_5',X1_273)
| ~ placename('#skF_1',X2_275)
| ~ hollywood_placename('#skF_1',X2_275)
| ~ of('#skF_1',X2_275,'#skF_3')
| ~ lonely('#skF_1',X1_273)
| ~ street('#skF_1',X1_273) ),
inference(demodulation,[status(thm),theory(equality)],[c_5334,c_5400,c_5388,c_5384,c_5383,c_5398,c_5395,c_5510,c_5390,c_5382,c_5699]) ).
tff(c_5704,plain,
! [X1_277] :
( ~ down('#skF_1','#skF_5',X1_277)
| ~ lonely('#skF_1',X1_277)
| ~ street('#skF_1',X1_277) ),
inference(splitLeft,[status(thm)],[c_5702]) ).
tff(c_5707,plain,
( ~ lonely('#skF_1','#skF_4')
| ~ street('#skF_1','#skF_4') ),
inference(resolution,[status(thm)],[c_5556,c_5704]) ).
tff(c_5711,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_5392,c_5391,c_5707]) ).
tff(c_5713,plain,
! [X2_278] :
( ~ placename('#skF_1',X2_278)
| ~ hollywood_placename('#skF_1',X2_278)
| ~ of('#skF_1',X2_278,'#skF_3') ),
inference(splitRight,[status(thm)],[c_5702]) ).
tff(c_5716,plain,
( ~ placename('#skF_1','#skF_2')
| ~ hollywood_placename('#skF_1','#skF_2') ),
inference(resolution,[status(thm)],[c_5513,c_5713]) ).
tff(c_5720,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_5369,c_5358,c_5716]) ).
tff(c_5722,plain,
~ barrel('#skF_6','#skF_10'),
inference(splitRight,[status(thm)],[c_144]) ).
tff(c_138,plain,
( hollywood_placename('#skF_1','#skF_2')
| barrel('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5757,plain,
hollywood_placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_5722,c_138]) ).
tff(c_136,plain,
( placename('#skF_1','#skF_2')
| barrel('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5748,plain,
placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_5722,c_136]) ).
tff(c_142,plain,
( of('#skF_1','#skF_2','#skF_3')
| barrel('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5956,plain,
of('#skF_1','#skF_2','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_5722,c_142]) ).
tff(c_126,plain,
( street('#skF_1','#skF_4')
| barrel('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5782,plain,
street('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_5722,c_126]) ).
tff(c_124,plain,
( lonely('#skF_1','#skF_4')
| barrel('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5770,plain,
lonely('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_5722,c_124]) ).
tff(c_114,plain,
( down('#skF_1','#skF_5','#skF_4')
| barrel('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5986,plain,
down('#skF_1','#skF_5','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_5722,c_114]) ).
tff(c_5721,plain,
actual_world('#skF_1'),
inference(splitRight,[status(thm)],[c_144]) ).
tff(c_140,plain,
( city('#skF_1','#skF_3')
| barrel('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5745,plain,
city('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_5722,c_140]) ).
tff(c_134,plain,
( chevy('#skF_1','#skF_3')
| barrel('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5753,plain,
chevy('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_5722,c_134]) ).
tff(c_132,plain,
( white('#skF_1','#skF_3')
| barrel('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5752,plain,
white('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_5722,c_132]) ).
tff(c_130,plain,
( dirty('#skF_1','#skF_3')
| barrel('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5754,plain,
dirty('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_5722,c_130]) ).
tff(c_128,plain,
( old('#skF_1','#skF_3')
| barrel('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5761,plain,
old('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_5722,c_128]) ).
tff(c_122,plain,
( event('#skF_1','#skF_5')
| barrel('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5773,plain,
event('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_5722,c_122]) ).
tff(c_120,plain,
( agent('#skF_1','#skF_5','#skF_3')
| barrel('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5903,plain,
agent('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_5722,c_120]) ).
tff(c_118,plain,
( present('#skF_1','#skF_5')
| barrel('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5780,plain,
present('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_5722,c_118]) ).
tff(c_116,plain,
( barrel('#skF_1','#skF_5')
| barrel('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5776,plain,
barrel('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_5722,c_116]) ).
tff(c_112,plain,
( in('#skF_1','#skF_5','#skF_3')
| barrel('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_5922,plain,
in('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_5722,c_112]) ).
tff(c_110,plain,
! [X3_12,X4_13,Z_5,X1_10,X2_11] :
( ~ in(Z_5,X4_13,X3_12)
| ~ down(Z_5,X4_13,X1_10)
| ~ barrel(Z_5,X4_13)
| ~ present(Z_5,X4_13)
| ~ agent(Z_5,X4_13,X3_12)
| ~ event(Z_5,X4_13)
| ~ old(Z_5,X3_12)
| ~ dirty(Z_5,X3_12)
| ~ white(Z_5,X3_12)
| ~ chevy(Z_5,X3_12)
| ~ placename(Z_5,X2_11)
| ~ hollywood_placename(Z_5,X2_11)
| ~ city(Z_5,X3_12)
| ~ of(Z_5,X2_11,X3_12)
| ~ lonely(Z_5,X1_10)
| ~ street(Z_5,X1_10)
| ~ actual_world(Z_5)
| barrel('#skF_6','#skF_10') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6013,plain,
! [X2_282,X3_279,X1_280,X4_283,Z_281] :
( ~ in(Z_281,X4_283,X3_279)
| ~ down(Z_281,X4_283,X1_280)
| ~ barrel(Z_281,X4_283)
| ~ present(Z_281,X4_283)
| ~ agent(Z_281,X4_283,X3_279)
| ~ event(Z_281,X4_283)
| ~ old(Z_281,X3_279)
| ~ dirty(Z_281,X3_279)
| ~ white(Z_281,X3_279)
| ~ chevy(Z_281,X3_279)
| ~ placename(Z_281,X2_282)
| ~ hollywood_placename(Z_281,X2_282)
| ~ city(Z_281,X3_279)
| ~ of(Z_281,X2_282,X3_279)
| ~ lonely(Z_281,X1_280)
| ~ street(Z_281,X1_280)
| ~ actual_world(Z_281) ),
inference(negUnitSimplification,[status(thm)],[c_5722,c_110]) ).
tff(c_6015,plain,
! [X1_280,X2_282] :
( ~ down('#skF_1','#skF_5',X1_280)
| ~ barrel('#skF_1','#skF_5')
| ~ present('#skF_1','#skF_5')
| ~ agent('#skF_1','#skF_5','#skF_3')
| ~ event('#skF_1','#skF_5')
| ~ old('#skF_1','#skF_3')
| ~ dirty('#skF_1','#skF_3')
| ~ white('#skF_1','#skF_3')
| ~ chevy('#skF_1','#skF_3')
| ~ placename('#skF_1',X2_282)
| ~ hollywood_placename('#skF_1',X2_282)
| ~ city('#skF_1','#skF_3')
| ~ of('#skF_1',X2_282,'#skF_3')
| ~ lonely('#skF_1',X1_280)
| ~ street('#skF_1',X1_280)
| ~ actual_world('#skF_1') ),
inference(resolution,[status(thm)],[c_5922,c_6013]) ).
tff(c_6018,plain,
! [X1_280,X2_282] :
( ~ down('#skF_1','#skF_5',X1_280)
| ~ placename('#skF_1',X2_282)
| ~ hollywood_placename('#skF_1',X2_282)
| ~ of('#skF_1',X2_282,'#skF_3')
| ~ lonely('#skF_1',X1_280)
| ~ street('#skF_1',X1_280) ),
inference(demodulation,[status(thm),theory(equality)],[c_5721,c_5745,c_5753,c_5752,c_5754,c_5761,c_5773,c_5903,c_5780,c_5776,c_6015]) ).
tff(c_6020,plain,
! [X1_284] :
( ~ down('#skF_1','#skF_5',X1_284)
| ~ lonely('#skF_1',X1_284)
| ~ street('#skF_1',X1_284) ),
inference(splitLeft,[status(thm)],[c_6018]) ).
tff(c_6023,plain,
( ~ lonely('#skF_1','#skF_4')
| ~ street('#skF_1','#skF_4') ),
inference(resolution,[status(thm)],[c_5986,c_6020]) ).
tff(c_6027,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_5782,c_5770,c_6023]) ).
tff(c_6029,plain,
! [X2_285] :
( ~ placename('#skF_1',X2_285)
| ~ hollywood_placename('#skF_1',X2_285)
| ~ of('#skF_1',X2_285,'#skF_3') ),
inference(splitRight,[status(thm)],[c_6018]) ).
tff(c_6032,plain,
( ~ placename('#skF_1','#skF_2')
| ~ hollywood_placename('#skF_1','#skF_2') ),
inference(resolution,[status(thm)],[c_5956,c_6029]) ).
tff(c_6036,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_5757,c_5748,c_6032]) ).
tff(c_6038,plain,
~ lonely('#skF_6','#skF_7'),
inference(splitRight,[status(thm)],[c_576]) ).
tff(c_570,plain,
( hollywood_placename('#skF_1','#skF_2')
| lonely('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6109,plain,
hollywood_placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_6038,c_570]) ).
tff(c_568,plain,
( placename('#skF_1','#skF_2')
| lonely('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6116,plain,
placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_6038,c_568]) ).
tff(c_574,plain,
( of('#skF_1','#skF_2','#skF_3')
| lonely('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6279,plain,
of('#skF_1','#skF_2','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_6038,c_574]) ).
tff(c_558,plain,
( street('#skF_1','#skF_4')
| lonely('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6196,plain,
street('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_6038,c_558]) ).
tff(c_556,plain,
( lonely('#skF_1','#skF_4')
| lonely('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6180,plain,
lonely('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_6038,c_556]) ).
tff(c_546,plain,
( down('#skF_1','#skF_5','#skF_4')
| lonely('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6300,plain,
down('#skF_1','#skF_5','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_6038,c_546]) ).
tff(c_6037,plain,
actual_world('#skF_1'),
inference(splitRight,[status(thm)],[c_576]) ).
tff(c_572,plain,
( city('#skF_1','#skF_3')
| lonely('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6063,plain,
city('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_6038,c_572]) ).
tff(c_566,plain,
( chevy('#skF_1','#skF_3')
| lonely('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6140,plain,
chevy('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_6038,c_566]) ).
tff(c_564,plain,
( white('#skF_1','#skF_3')
| lonely('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6143,plain,
white('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_6038,c_564]) ).
tff(c_562,plain,
( dirty('#skF_1','#skF_3')
| lonely('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6157,plain,
dirty('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_6038,c_562]) ).
tff(c_560,plain,
( old('#skF_1','#skF_3')
| lonely('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6167,plain,
old('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_6038,c_560]) ).
tff(c_554,plain,
( event('#skF_1','#skF_5')
| lonely('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6149,plain,
event('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_6038,c_554]) ).
tff(c_552,plain,
( agent('#skF_1','#skF_5','#skF_3')
| lonely('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6263,plain,
agent('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_6038,c_552]) ).
tff(c_550,plain,
( present('#skF_1','#skF_5')
| lonely('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6183,plain,
present('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_6038,c_550]) ).
tff(c_548,plain,
( barrel('#skF_1','#skF_5')
| lonely('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6185,plain,
barrel('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_6038,c_548]) ).
tff(c_544,plain,
( in('#skF_1','#skF_5','#skF_3')
| lonely('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6222,plain,
in('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_6038,c_544]) ).
tff(c_542,plain,
! [X3_12,X4_13,Z_5,X1_10,X2_11] :
( ~ in(Z_5,X4_13,X3_12)
| ~ down(Z_5,X4_13,X1_10)
| ~ barrel(Z_5,X4_13)
| ~ present(Z_5,X4_13)
| ~ agent(Z_5,X4_13,X3_12)
| ~ event(Z_5,X4_13)
| ~ old(Z_5,X3_12)
| ~ dirty(Z_5,X3_12)
| ~ white(Z_5,X3_12)
| ~ chevy(Z_5,X3_12)
| ~ placename(Z_5,X2_11)
| ~ hollywood_placename(Z_5,X2_11)
| ~ city(Z_5,X3_12)
| ~ of(Z_5,X2_11,X3_12)
| ~ lonely(Z_5,X1_10)
| ~ street(Z_5,X1_10)
| ~ actual_world(Z_5)
| lonely('#skF_6','#skF_7') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6345,plain,
! [X4_290,X2_289,X3_286,Z_288,X1_287] :
( ~ in(Z_288,X4_290,X3_286)
| ~ down(Z_288,X4_290,X1_287)
| ~ barrel(Z_288,X4_290)
| ~ present(Z_288,X4_290)
| ~ agent(Z_288,X4_290,X3_286)
| ~ event(Z_288,X4_290)
| ~ old(Z_288,X3_286)
| ~ dirty(Z_288,X3_286)
| ~ white(Z_288,X3_286)
| ~ chevy(Z_288,X3_286)
| ~ placename(Z_288,X2_289)
| ~ hollywood_placename(Z_288,X2_289)
| ~ city(Z_288,X3_286)
| ~ of(Z_288,X2_289,X3_286)
| ~ lonely(Z_288,X1_287)
| ~ street(Z_288,X1_287)
| ~ actual_world(Z_288) ),
inference(negUnitSimplification,[status(thm)],[c_6038,c_542]) ).
tff(c_6347,plain,
! [X1_287,X2_289] :
( ~ down('#skF_1','#skF_5',X1_287)
| ~ barrel('#skF_1','#skF_5')
| ~ present('#skF_1','#skF_5')
| ~ agent('#skF_1','#skF_5','#skF_3')
| ~ event('#skF_1','#skF_5')
| ~ old('#skF_1','#skF_3')
| ~ dirty('#skF_1','#skF_3')
| ~ white('#skF_1','#skF_3')
| ~ chevy('#skF_1','#skF_3')
| ~ placename('#skF_1',X2_289)
| ~ hollywood_placename('#skF_1',X2_289)
| ~ city('#skF_1','#skF_3')
| ~ of('#skF_1',X2_289,'#skF_3')
| ~ lonely('#skF_1',X1_287)
| ~ street('#skF_1',X1_287)
| ~ actual_world('#skF_1') ),
inference(resolution,[status(thm)],[c_6222,c_6345]) ).
tff(c_6350,plain,
! [X1_287,X2_289] :
( ~ down('#skF_1','#skF_5',X1_287)
| ~ placename('#skF_1',X2_289)
| ~ hollywood_placename('#skF_1',X2_289)
| ~ of('#skF_1',X2_289,'#skF_3')
| ~ lonely('#skF_1',X1_287)
| ~ street('#skF_1',X1_287) ),
inference(demodulation,[status(thm),theory(equality)],[c_6037,c_6063,c_6140,c_6143,c_6157,c_6167,c_6149,c_6263,c_6183,c_6185,c_6347]) ).
tff(c_6353,plain,
! [X1_291] :
( ~ down('#skF_1','#skF_5',X1_291)
| ~ lonely('#skF_1',X1_291)
| ~ street('#skF_1',X1_291) ),
inference(splitLeft,[status(thm)],[c_6350]) ).
tff(c_6356,plain,
( ~ lonely('#skF_1','#skF_4')
| ~ street('#skF_1','#skF_4') ),
inference(resolution,[status(thm)],[c_6300,c_6353]) ).
tff(c_6360,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_6196,c_6180,c_6356]) ).
tff(c_6362,plain,
! [X2_292] :
( ~ placename('#skF_1',X2_292)
| ~ hollywood_placename('#skF_1',X2_292)
| ~ of('#skF_1',X2_292,'#skF_3') ),
inference(splitRight,[status(thm)],[c_6350]) ).
tff(c_6365,plain,
( ~ placename('#skF_1','#skF_2')
| ~ hollywood_placename('#skF_1','#skF_2') ),
inference(resolution,[status(thm)],[c_6279,c_6362]) ).
tff(c_6369,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_6109,c_6116,c_6365]) ).
tff(c_6371,plain,
~ actual_world('#skF_6'),
inference(splitRight,[status(thm)],[c_648]) ).
tff(c_642,plain,
( hollywood_placename('#skF_1','#skF_2')
| actual_world('#skF_6') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6380,plain,
hollywood_placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_6371,c_642]) ).
tff(c_640,plain,
( placename('#skF_1','#skF_2')
| actual_world('#skF_6') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6383,plain,
placename('#skF_1','#skF_2'),
inference(negUnitSimplification,[status(thm)],[c_6371,c_640]) ).
tff(c_646,plain,
( of('#skF_1','#skF_2','#skF_3')
| actual_world('#skF_6') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6405,plain,
of('#skF_1','#skF_2','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_6371,c_646]) ).
tff(c_630,plain,
( street('#skF_1','#skF_4')
| actual_world('#skF_6') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6387,plain,
street('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_6371,c_630]) ).
tff(c_628,plain,
( lonely('#skF_1','#skF_4')
| actual_world('#skF_6') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6388,plain,
lonely('#skF_1','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_6371,c_628]) ).
tff(c_618,plain,
( down('#skF_1','#skF_5','#skF_4')
| actual_world('#skF_6') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6399,plain,
down('#skF_1','#skF_5','#skF_4'),
inference(negUnitSimplification,[status(thm)],[c_6371,c_618]) ).
tff(c_6370,plain,
actual_world('#skF_1'),
inference(splitRight,[status(thm)],[c_648]) ).
tff(c_644,plain,
( city('#skF_1','#skF_3')
| actual_world('#skF_6') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6391,plain,
city('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_6371,c_644]) ).
tff(c_638,plain,
( chevy('#skF_1','#skF_3')
| actual_world('#skF_6') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6392,plain,
chevy('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_6371,c_638]) ).
tff(c_636,plain,
( white('#skF_1','#skF_3')
| actual_world('#skF_6') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6381,plain,
white('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_6371,c_636]) ).
tff(c_634,plain,
( dirty('#skF_1','#skF_3')
| actual_world('#skF_6') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6382,plain,
dirty('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_6371,c_634]) ).
tff(c_632,plain,
( old('#skF_1','#skF_3')
| actual_world('#skF_6') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6372,plain,
old('#skF_1','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_6371,c_632]) ).
tff(c_626,plain,
( event('#skF_1','#skF_5')
| actual_world('#skF_6') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6393,plain,
event('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_6371,c_626]) ).
tff(c_624,plain,
( agent('#skF_1','#skF_5','#skF_3')
| actual_world('#skF_6') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6498,plain,
agent('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_6371,c_624]) ).
tff(c_622,plain,
( present('#skF_1','#skF_5')
| actual_world('#skF_6') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6386,plain,
present('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_6371,c_622]) ).
tff(c_620,plain,
( barrel('#skF_1','#skF_5')
| actual_world('#skF_6') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6376,plain,
barrel('#skF_1','#skF_5'),
inference(negUnitSimplification,[status(thm)],[c_6371,c_620]) ).
tff(c_616,plain,
( in('#skF_1','#skF_5','#skF_3')
| actual_world('#skF_6') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6431,plain,
in('#skF_1','#skF_5','#skF_3'),
inference(negUnitSimplification,[status(thm)],[c_6371,c_616]) ).
tff(c_614,plain,
! [X3_12,X4_13,Z_5,X1_10,X2_11] :
( ~ in(Z_5,X4_13,X3_12)
| ~ down(Z_5,X4_13,X1_10)
| ~ barrel(Z_5,X4_13)
| ~ present(Z_5,X4_13)
| ~ agent(Z_5,X4_13,X3_12)
| ~ event(Z_5,X4_13)
| ~ old(Z_5,X3_12)
| ~ dirty(Z_5,X3_12)
| ~ white(Z_5,X3_12)
| ~ chevy(Z_5,X3_12)
| ~ placename(Z_5,X2_11)
| ~ hollywood_placename(Z_5,X2_11)
| ~ city(Z_5,X3_12)
| ~ of(Z_5,X2_11,X3_12)
| ~ lonely(Z_5,X1_10)
| ~ street(Z_5,X1_10)
| ~ actual_world(Z_5)
| actual_world('#skF_6') ),
inference(cnfTransformation,[status(thm)],[f_173]) ).
tff(c_6661,plain,
! [X2_296,X3_293,Z_295,X4_297,X1_294] :
( ~ in(Z_295,X4_297,X3_293)
| ~ down(Z_295,X4_297,X1_294)
| ~ barrel(Z_295,X4_297)
| ~ present(Z_295,X4_297)
| ~ agent(Z_295,X4_297,X3_293)
| ~ event(Z_295,X4_297)
| ~ old(Z_295,X3_293)
| ~ dirty(Z_295,X3_293)
| ~ white(Z_295,X3_293)
| ~ chevy(Z_295,X3_293)
| ~ placename(Z_295,X2_296)
| ~ hollywood_placename(Z_295,X2_296)
| ~ city(Z_295,X3_293)
| ~ of(Z_295,X2_296,X3_293)
| ~ lonely(Z_295,X1_294)
| ~ street(Z_295,X1_294)
| ~ actual_world(Z_295) ),
inference(negUnitSimplification,[status(thm)],[c_6371,c_614]) ).
tff(c_6663,plain,
! [X1_294,X2_296] :
( ~ down('#skF_1','#skF_5',X1_294)
| ~ barrel('#skF_1','#skF_5')
| ~ present('#skF_1','#skF_5')
| ~ agent('#skF_1','#skF_5','#skF_3')
| ~ event('#skF_1','#skF_5')
| ~ old('#skF_1','#skF_3')
| ~ dirty('#skF_1','#skF_3')
| ~ white('#skF_1','#skF_3')
| ~ chevy('#skF_1','#skF_3')
| ~ placename('#skF_1',X2_296)
| ~ hollywood_placename('#skF_1',X2_296)
| ~ city('#skF_1','#skF_3')
| ~ of('#skF_1',X2_296,'#skF_3')
| ~ lonely('#skF_1',X1_294)
| ~ street('#skF_1',X1_294)
| ~ actual_world('#skF_1') ),
inference(resolution,[status(thm)],[c_6431,c_6661]) ).
tff(c_6666,plain,
! [X1_294,X2_296] :
( ~ down('#skF_1','#skF_5',X1_294)
| ~ placename('#skF_1',X2_296)
| ~ hollywood_placename('#skF_1',X2_296)
| ~ of('#skF_1',X2_296,'#skF_3')
| ~ lonely('#skF_1',X1_294)
| ~ street('#skF_1',X1_294) ),
inference(demodulation,[status(thm),theory(equality)],[c_6370,c_6391,c_6392,c_6381,c_6382,c_6372,c_6393,c_6498,c_6386,c_6376,c_6663]) ).
tff(c_6668,plain,
! [X1_298] :
( ~ down('#skF_1','#skF_5',X1_298)
| ~ lonely('#skF_1',X1_298)
| ~ street('#skF_1',X1_298) ),
inference(splitLeft,[status(thm)],[c_6666]) ).
tff(c_6671,plain,
( ~ lonely('#skF_1','#skF_4')
| ~ street('#skF_1','#skF_4') ),
inference(resolution,[status(thm)],[c_6399,c_6668]) ).
tff(c_6675,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_6387,c_6388,c_6671]) ).
tff(c_6678,plain,
! [X2_299] :
( ~ placename('#skF_1',X2_299)
| ~ hollywood_placename('#skF_1',X2_299)
| ~ of('#skF_1',X2_299,'#skF_3') ),
inference(splitRight,[status(thm)],[c_6666]) ).
tff(c_6681,plain,
( ~ placename('#skF_1','#skF_2')
| ~ hollywood_placename('#skF_1','#skF_2') ),
inference(resolution,[status(thm)],[c_6405,c_6678]) ).
tff(c_6685,plain,
$false,
inference(demodulation,[status(thm),theory(equality)],[c_6380,c_6383,c_6681]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NLP122+1 : TPTP v9.0.0. Released v2.4.0.
% 0.03/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.12/0.34 % Computer : n026.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Tue Apr 8 08:38:23 EDT 2025
% 0.12/0.34 % CPUTime :
% 8.47/3.02 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 9.26/3.14
% 9.26/3.14 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% See solution above
%------------------------------------------------------------------------------