%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : NLP191+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 : n029.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:33 PM UTC 2025
% Result : CounterSatisfiable 120.18s 101.27s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : NLP191+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.13/0.34 % Computer : n029.cluster.edu
% 0.13/0.34 % Model : x86_64 x86_64
% 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34 % Memory : 8042.1875MB
% 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34 % CPULimit : 300
% 0.13/0.34 % WCLimit : 300
% 0.13/0.34 % DateTime : Tue Apr 8 09:09:34 EDT 2025
% 0.13/0.34 % CPUTime :
% 120.18/101.27
% 120.18/101.27 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 120.18/101.27
% 120.18/101.27 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 120.29/101.28 %$ be > patient > of > member > in > down > behind > agent > young > white > wheel > wear > two > street > state > present > placename > old > nonreflexive > man > lonely > jules_forename > hollywood_placename > group > frontseat > forename > fellow > event > dirty > coat > city > chevy > cheap > black > barrel > actual_world > #nlpp > #skF_33 > #skF_37 > #skF_35 > #skF_11 > #skF_31 > #skF_25 > #skF_7 > #skF_10 > #skF_17 > #skF_34 > #skF_26 > #skF_5 > #skF_6 > #skF_2 > #skF_3 > #skF_1 > #skF_21 > #skF_9 > #skF_38 > #skF_36 > #skF_20 > #skF_32 > #skF_8 > #skF_30 > #skF_13 > #skF_16 > #skF_4 > #skF_22 > #skF_41 > #skF_14 > #skF_29 > #skF_28 > #skF_24 > #skF_27 > #skF_23 > #skF_40 > #skF_19 > #skF_15 > #skF_18 > #skF_12 > #skF_39
% 120.29/101.28
% 120.29/101.28 %Foreground sorts:
% 120.29/101.28
% 120.29/101.28
% 120.29/101.28 %Background operators:
% 120.29/101.28
% 120.29/101.28
% 120.29/101.28 %Foreground operators:
% 120.29/101.28 tff(cheap, type, cheap: ($i * $i) > $o).
% 120.29/101.28 tff(wear, type, wear: ($i * $i) > $o).
% 120.29/101.28 tff(two, type, two: ($i * $i) > $o).
% 120.29/101.28 tff('#skF_33', type, '#skF_33': $i).
% 120.29/101.28 tff(frontseat, type, frontseat: ($i * $i) > $o).
% 120.29/101.28 tff(placename, type, placename: ($i * $i) > $o).
% 120.29/101.28 tff(member, type, member: ($i * $i * $i) > $o).
% 120.29/101.28 tff(forename, type, forename: ($i * $i) > $o).
% 120.29/101.28 tff('#skF_37', type, '#skF_37': ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $i).
% 120.29/101.28 tff(be, type, be: ($i * $i * $i * $i) > $o).
% 120.29/101.28 tff(wheel, type, wheel: ($i * $i) > $o).
% 120.29/101.28 tff(black, type, black: ($i * $i) > $o).
% 120.29/101.28 tff(present, type, present: ($i * $i) > $o).
% 120.29/101.28 tff(in, type, in: ($i * $i * $i) > $o).
% 120.29/101.28 tff(old, type, old: ($i * $i) > $o).
% 120.29/101.28 tff(dirty, type, dirty: ($i * $i) > $o).
% 120.29/101.28 tff('#skF_35', type, '#skF_35': $i > $i).
% 120.29/101.28 tff(behind, type, behind: ($i * $i * $i) > $o).
% 120.29/101.28 tff('#skF_11', type, '#skF_11': $i).
% 120.29/101.28 tff('#skF_31', type, '#skF_31': $i).
% 120.29/101.28 tff(city, type, city: ($i * $i) > $o).
% 120.29/101.28 tff('#skF_25', type, '#skF_25': $i).
% 120.29/101.28 tff(young, type, young: ($i * $i) > $o).
% 120.29/101.28 tff(of, type, of: ($i * $i * $i) > $o).
% 120.29/101.28 tff('#skF_7', type, '#skF_7': $i).
% 120.29/101.28 tff(actual_world, type, actual_world: $i > $o).
% 120.29/101.28 tff(agent, type, agent: ($i * $i * $i) > $o).
% 120.29/101.28 tff('#skF_10', type, '#skF_10': $i).
% 120.29/101.28 tff('#skF_17', type, '#skF_17': ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $i).
% 120.29/101.28 tff('#skF_34', type, '#skF_34': $i > $i).
% 120.29/101.28 tff('#skF_26', type, '#skF_26': $i).
% 120.29/101.28 tff('#skF_5', type, '#skF_5': $i).
% 120.29/101.28 tff(group, type, group: ($i * $i) > $o).
% 120.29/101.28 tff(lonely, type, lonely: ($i * $i) > $o).
% 120.29/101.28 tff(jules_forename, type, jules_forename: ($i * $i) > $o).
% 120.29/101.28 tff(fellow, type, fellow: ($i * $i) > $o).
% 120.29/101.28 tff('#skF_6', type, '#skF_6': $i).
% 120.29/101.28 tff('#skF_2', type, '#skF_2': $i).
% 120.29/101.28 tff('#skF_3', type, '#skF_3': $i).
% 120.29/101.28 tff(event, type, event: ($i * $i) > $o).
% 120.29/101.28 tff('#skF_1', type, '#skF_1': $i).
% 120.29/101.28 tff(down, type, down: ($i * $i * $i) > $o).
% 120.29/101.28 tff(patient, type, patient: ($i * $i * $i) > $o).
% 120.29/101.28 tff(hollywood_placename, type, hollywood_placename: ($i * $i) > $o).
% 120.29/101.28 tff(white, type, white: ($i * $i) > $o).
% 120.29/101.28 tff('#skF_21', type, '#skF_21': $i).
% 120.29/101.28 tff('#skF_9', type, '#skF_9': $i).
% 120.29/101.28 tff('#skF_38', type, '#skF_38': ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $i).
% 120.29/101.28 tff('#skF_36', type, '#skF_36': ($i * $i) > $i).
% 120.29/101.28 tff('#skF_20', type, '#skF_20': ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $i).
% 120.29/101.28 tff(barrel, type, barrel: ($i * $i) > $o).
% 120.29/101.28 tff('#skF_32', type, '#skF_32': $i).
% 120.29/101.28 tff(state, type, state: ($i * $i) > $o).
% 120.29/101.28 tff(street, type, street: ($i * $i) > $o).
% 120.29/101.28 tff('#skF_8', type, '#skF_8': $i).
% 120.29/101.28 tff('#skF_30', type, '#skF_30': $i).
% 120.29/101.28 tff('#skF_13', type, '#skF_13': $i > $i).
% 120.29/101.28 tff(man, type, man: ($i * $i) > $o).
% 120.29/101.28 tff('#skF_16', type, '#skF_16': ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $i).
% 120.29/101.28 tff('#skF_4', type, '#skF_4': $i).
% 120.29/101.28 tff('#skF_22', type, '#skF_22': $i).
% 120.29/101.28 tff('#skF_41', type, '#skF_41': ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $i).
% 120.29/101.28 tff('#skF_14', type, '#skF_14': $i > $i).
% 120.29/101.28 tff('#skF_29', type, '#skF_29': $i).
% 120.29/101.28 tff('#skF_28', type, '#skF_28': $i).
% 120.29/101.28 tff('#skF_24', type, '#skF_24': $i).
% 120.29/101.28 tff('#skF_27', type, '#skF_27': $i).
% 120.29/101.28 tff('#skF_23', type, '#skF_23': $i).
% 120.29/101.28 tff(nonreflexive, type, nonreflexive: ($i * $i) > $o).
% 120.29/101.28 tff(chevy, type, chevy: ($i * $i) > $o).
% 120.29/101.28 tff('#skF_40', type, '#skF_40': ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $i).
% 120.29/101.28 tff('#skF_19', type, '#skF_19': ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $i).
% 120.29/101.28 tff(coat, type, coat: ($i * $i) > $o).
% 120.29/101.28 tff('#skF_15', type, '#skF_15': ($i * $i) > $i).
% 120.29/101.28 tff('#skF_18', type, '#skF_18': ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $i).
% 120.29/101.28 tff('#skF_12', type, '#skF_12': $i).
% 120.29/101.28 tff('#skF_39', type, '#skF_39': ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $i).
% 120.29/101.28
% 120.29/101.28 %Saturated clause set:
% 120.29/101.28 tff(c_37010, plain, (~chevy('#skF_21', '#skF_24'))).
% 120.29/101.28 tff(c_37003, plain, (![Z_2893, W_2895, X2_2897, V_2891, X5_2899, X6_2894, X1_2896, Y_2892]: (~behind('#skF_21', X6_2894, Y_2892) | ~be('#skF_21', X5_2899, V_2891, X6_2894) | ~state('#skF_21', X5_2899) | ~in('#skF_21', X2_2897, X1_2896) | ~down('#skF_21', X2_2897, X1_2896) | ~barrel('#skF_21', X2_2897) | ~present('#skF_21', X2_2897) | ~agent('#skF_21', X2_2897, Y_2892) | ~event('#skF_21', X2_2897) | ~lonely('#skF_21', X1_2896) | ~street('#skF_21', X1_2896) | ~placename('#skF_21', Z_2893) | ~hollywood_placename('#skF_21', Z_2893) | ~city('#skF_21', X1_2896) | ~of('#skF_21', Z_2893, X1_2896) | ~old('#skF_21', Y_2892) | ~dirty('#skF_21', Y_2892) | ~white('#skF_21', Y_2892) | ~chevy('#skF_21', Y_2892) | ~wheel('#skF_21', Y_2892) | ~forename('#skF_21', W_2895) | ~jules_forename('#skF_21', W_2895) | ~man('#skF_21', V_2891) | ~of('#skF_21', W_2895, V_2891)))).
% 120.29/101.28 tff(c_23045, plain, (![Y_249, X2_252, V_246, X9_274, Z_250, X_248, X8_273, X13_279, X6_256, X3_253, W_247, U_206, X5_255, X1_251, X4_254]: (~in(U_206, X9_274, X_248) | ~be(U_206, X8_273, '#skF_37'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X9_274) | ~state(U_206, X8_273) | ~young(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~fellow(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~wear(U_206, X13_279) | ~nonreflexive(U_206, X13_279) | ~present(U_206, X13_279) | ~patient(U_206, X13_279, '#skF_39'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~agent(U_206, X13_279, '#skF_40'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~event(U_206, X13_279) | ~cheap(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~black(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~coat(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~behind(U_206, X6_256, Y_249) | ~be(U_206, X5_255, V_246, X6_256) | ~state(U_206, X5_255) | ~group(U_206, X4_254) | ~group(U_206, X3_253) | ~two(U_206, X3_253) | ~in(U_206, X2_252, X1_251) | ~down(U_206, X2_252, X1_251) | ~barrel(U_206, X2_252) | ~present(U_206, X2_252) | ~agent(U_206, X2_252, Y_249) | ~event(U_206, X2_252) | ~lonely(U_206, X1_251) | ~street(U_206, X1_251) | ~placename(U_206, Z_250) | ~hollywood_placename(U_206, Z_250) | ~city(U_206, X1_251) | ~of(U_206, Z_250, X1_251) | ~old(U_206, Y_249) | ~dirty(U_206, Y_249) | ~white(U_206, Y_249) | ~chevy(U_206, Y_249) | ~frontseat(U_206, X_248) | ~wheel(U_206, Y_249) | ~forename(U_206, W_247) | ~jules_forename(U_206, W_247) | ~man(U_206, V_246) | ~of(U_206, W_247, V_246) | ~actual_world(U_206)))).
% 120.29/101.29 tff(c_22979, plain, (![Y_249, X2_252, V_246, Z_250, X_248, X13_279, X6_256, X3_253, W_247, U_206, X5_255, X1_251, X4_254]: (member(U_206, '#skF_37'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | ~young(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~fellow(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~wear(U_206, X13_279) | ~nonreflexive(U_206, X13_279) | ~present(U_206, X13_279) | ~patient(U_206, X13_279, '#skF_39'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~agent(U_206, X13_279, '#skF_40'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~event(U_206, X13_279) | ~cheap(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~black(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~coat(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~behind(U_206, X6_256, Y_249) | ~be(U_206, X5_255, V_246, X6_256) | ~state(U_206, X5_255) | ~group(U_206, X4_254) | ~group(U_206, X3_253) | ~two(U_206, X3_253) | ~in(U_206, X2_252, X1_251) | ~down(U_206, X2_252, X1_251) | ~barrel(U_206, X2_252) | ~present(U_206, X2_252) | ~agent(U_206, X2_252, Y_249) | ~event(U_206, X2_252) | ~lonely(U_206, X1_251) | ~street(U_206, X1_251) | ~placename(U_206, Z_250) | ~hollywood_placename(U_206, Z_250) | ~city(U_206, X1_251) | ~of(U_206, Z_250, X1_251) | ~old(U_206, Y_249) | ~dirty(U_206, Y_249) | ~white(U_206, Y_249) | ~chevy(U_206, Y_249) | ~frontseat(U_206, X_248) | ~wheel(U_206, Y_249) | ~forename(U_206, W_247) | ~jules_forename(U_206, W_247) | ~man(U_206, V_246) | ~of(U_206, W_247, V_246) | ~actual_world(U_206)))).
% 120.29/101.29 tff(c_21239, plain, (![Y_249, X2_252, V_246, X9_274, Z_250, X_248, X8_273, X13_279, X6_256, X3_253, W_247, U_206, X5_255, X1_251, X4_254]: (~in(U_206, X9_274, X_248) | ~be(U_206, X8_273, '#skF_37'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X9_274) | ~state(U_206, X8_273) | member(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | ~wear(U_206, X13_279) | ~nonreflexive(U_206, X13_279) | ~present(U_206, X13_279) | ~patient(U_206, X13_279, '#skF_39'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~agent(U_206, X13_279, '#skF_40'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~event(U_206, X13_279) | ~cheap(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~black(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~coat(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~behind(U_206, X6_256, Y_249) | ~be(U_206, X5_255, V_246, X6_256) | ~state(U_206, X5_255) | ~group(U_206, X4_254) | ~group(U_206, X3_253) | ~two(U_206, X3_253) | ~in(U_206, X2_252, X1_251) | ~down(U_206, X2_252, X1_251) | ~barrel(U_206, X2_252) | ~present(U_206, X2_252) | ~agent(U_206, X2_252, Y_249) | ~event(U_206, X2_252) | ~lonely(U_206, X1_251) | ~street(U_206, X1_251) | ~placename(U_206, Z_250) | ~hollywood_placename(U_206, Z_250) | ~city(U_206, X1_251) | ~of(U_206, Z_250, X1_251) | ~old(U_206, Y_249) | ~dirty(U_206, Y_249) | ~white(U_206, Y_249) | ~chevy(U_206, Y_249) | ~frontseat(U_206, X_248) | ~wheel(U_206, Y_249) | ~forename(U_206, W_247) | ~jules_forename(U_206, W_247) | ~man(U_206, V_246) | ~of(U_206, W_247, V_246) | ~actual_world(U_206)))).
% 120.29/101.29 tff(c_21173, plain, (![Y_249, X2_252, V_246, Z_250, X_248, X13_279, X6_256, X3_253, W_247, U_206, X5_255, X1_251, X4_254]: (member(U_206, '#skF_37'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | member(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | ~wear(U_206, X13_279) | ~nonreflexive(U_206, X13_279) | ~present(U_206, X13_279) | ~patient(U_206, X13_279, '#skF_39'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~agent(U_206, X13_279, '#skF_40'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~event(U_206, X13_279) | ~cheap(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~black(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~coat(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~behind(U_206, X6_256, Y_249) | ~be(U_206, X5_255, V_246, X6_256) | ~state(U_206, X5_255) | ~group(U_206, X4_254) | ~group(U_206, X3_253) | ~two(U_206, X3_253) | ~in(U_206, X2_252, X1_251) | ~down(U_206, X2_252, X1_251) | ~barrel(U_206, X2_252) | ~present(U_206, X2_252) | ~agent(U_206, X2_252, Y_249) | ~event(U_206, X2_252) | ~lonely(U_206, X1_251) | ~street(U_206, X1_251) | ~placename(U_206, Z_250) | ~hollywood_placename(U_206, Z_250) | ~city(U_206, X1_251) | ~of(U_206, Z_250, X1_251) | ~old(U_206, Y_249) | ~dirty(U_206, Y_249) | ~white(U_206, Y_249) | ~chevy(U_206, Y_249) | ~frontseat(U_206, X_248) | ~wheel(U_206, Y_249) | ~forename(U_206, W_247) | ~jules_forename(U_206, W_247) | ~man(U_206, V_246) | ~of(U_206, W_247, V_246) | ~actual_world(U_206)))).
% 120.35/101.29 tff(c_20779, plain, (![Y_249, X2_252, V_246, X9_274, Z_250, X_248, X8_273, X6_256, X3_253, W_247, U_206, X5_255, X1_251, X4_254]: (~in(U_206, X9_274, X_248) | ~be(U_206, X8_273, '#skF_37'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X9_274) | ~state(U_206, X8_273) | ~young(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~fellow(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | member(U_206, '#skF_40'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | ~cheap(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~black(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~coat(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~behind(U_206, X6_256, Y_249) | ~be(U_206, X5_255, V_246, X6_256) | ~state(U_206, X5_255) | ~group(U_206, X4_254) | ~group(U_206, X3_253) | ~two(U_206, X3_253) | ~in(U_206, X2_252, X1_251) | ~down(U_206, X2_252, X1_251) | ~barrel(U_206, X2_252) | ~present(U_206, X2_252) | ~agent(U_206, X2_252, Y_249) | ~event(U_206, X2_252) | ~lonely(U_206, X1_251) | ~street(U_206, X1_251) | ~placename(U_206, Z_250) | ~hollywood_placename(U_206, Z_250) | ~city(U_206, X1_251) | ~of(U_206, Z_250, X1_251) | ~old(U_206, Y_249) | ~dirty(U_206, Y_249) | ~white(U_206, Y_249) | ~chevy(U_206, Y_249) | ~frontseat(U_206, X_248) | ~wheel(U_206, Y_249) | ~forename(U_206, W_247) | ~jules_forename(U_206, W_247) | ~man(U_206, V_246) | ~of(U_206, W_247, V_246) | ~actual_world(U_206)))).
% 120.35/101.29 tff(c_20770, plain, (![Y_249, X2_252, V_246, X9_274, Z_250, X_248, X8_273, X6_256, X3_253, W_247, U_206, X5_255, X1_251, X4_254]: (~in(U_206, X9_274, X_248) | ~be(U_206, X8_273, '#skF_37'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X9_274) | ~state(U_206, X8_273) | ~young(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~fellow(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | member(U_206, '#skF_39'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X4_254) | ~cheap(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~black(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~coat(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~behind(U_206, X6_256, Y_249) | ~be(U_206, X5_255, V_246, X6_256) | ~state(U_206, X5_255) | ~group(U_206, X4_254) | ~group(U_206, X3_253) | ~two(U_206, X3_253) | ~in(U_206, X2_252, X1_251) | ~down(U_206, X2_252, X1_251) | ~barrel(U_206, X2_252) | ~present(U_206, X2_252) | ~agent(U_206, X2_252, Y_249) | ~event(U_206, X2_252) | ~lonely(U_206, X1_251) | ~street(U_206, X1_251) | ~placename(U_206, Z_250) | ~hollywood_placename(U_206, Z_250) | ~city(U_206, X1_251) | ~of(U_206, Z_250, X1_251) | ~old(U_206, Y_249) | ~dirty(U_206, Y_249) | ~white(U_206, Y_249) | ~chevy(U_206, Y_249) | ~frontseat(U_206, X_248) | ~wheel(U_206, Y_249) | ~forename(U_206, W_247) | ~jules_forename(U_206, W_247) | ~man(U_206, V_246) | ~of(U_206, W_247, V_246) | ~actual_world(U_206)))).
% 120.35/101.29 tff(c_20762, plain, (![Y_249, X2_252, V_246, X9_274, Z_250, X_248, X8_273, X13_279, X6_256, X3_253, W_247, U_206, X5_255, X1_251, X4_254]: (~in(U_206, X9_274, X_248) | ~be(U_206, X8_273, '#skF_37'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X9_274) | ~state(U_206, X8_273) | ~young(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~fellow(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~wear(U_206, X13_279) | ~nonreflexive(U_206, X13_279) | ~present(U_206, X13_279) | ~patient(U_206, X13_279, '#skF_39'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~agent(U_206, X13_279, '#skF_40'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~event(U_206, X13_279) | member(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X4_254) | ~behind(U_206, X6_256, Y_249) | ~be(U_206, X5_255, V_246, X6_256) | ~state(U_206, X5_255) | ~group(U_206, X4_254) | ~group(U_206, X3_253) | ~two(U_206, X3_253) | ~in(U_206, X2_252, X1_251) | ~down(U_206, X2_252, X1_251) | ~barrel(U_206, X2_252) | ~present(U_206, X2_252) | ~agent(U_206, X2_252, Y_249) | ~event(U_206, X2_252) | ~lonely(U_206, X1_251) | ~street(U_206, X1_251) | ~placename(U_206, Z_250) | ~hollywood_placename(U_206, Z_250) | ~city(U_206, X1_251) | ~of(U_206, Z_250, X1_251) | ~old(U_206, Y_249) | ~dirty(U_206, Y_249) | ~white(U_206, Y_249) | ~chevy(U_206, Y_249) | ~frontseat(U_206, X_248) | ~wheel(U_206, Y_249) | ~forename(U_206, W_247) | ~jules_forename(U_206, W_247) | ~man(U_206, V_246) | ~of(U_206, W_247, V_246) | ~actual_world(U_206)))).
% 120.35/101.29 tff(c_19500, plain, (![Y_249, X2_252, V_246, Z_250, X_248, X6_256, X3_253, W_247, U_206, X5_255, X1_251, X4_254]: (member(U_206, '#skF_37'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | ~young(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~fellow(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | member(U_206, '#skF_40'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | ~cheap(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~black(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~coat(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~behind(U_206, X6_256, Y_249) | ~be(U_206, X5_255, V_246, X6_256) | ~state(U_206, X5_255) | ~group(U_206, X4_254) | ~group(U_206, X3_253) | ~two(U_206, X3_253) | ~in(U_206, X2_252, X1_251) | ~down(U_206, X2_252, X1_251) | ~barrel(U_206, X2_252) | ~present(U_206, X2_252) | ~agent(U_206, X2_252, Y_249) | ~event(U_206, X2_252) | ~lonely(U_206, X1_251) | ~street(U_206, X1_251) | ~placename(U_206, Z_250) | ~hollywood_placename(U_206, Z_250) | ~city(U_206, X1_251) | ~of(U_206, Z_250, X1_251) | ~old(U_206, Y_249) | ~dirty(U_206, Y_249) | ~white(U_206, Y_249) | ~chevy(U_206, Y_249) | ~frontseat(U_206, X_248) | ~wheel(U_206, Y_249) | ~forename(U_206, W_247) | ~jules_forename(U_206, W_247) | ~man(U_206, V_246) | ~of(U_206, W_247, V_246) | ~actual_world(U_206)))).
% 120.35/101.29 tff(c_19393, plain, (![Y_249, X2_252, V_246, Z_250, X_248, X6_256, X3_253, W_247, U_206, X5_255, X1_251, X4_254]: (member(U_206, '#skF_37'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | ~young(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~fellow(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | member(U_206, '#skF_39'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X4_254) | ~cheap(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~black(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~coat(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~behind(U_206, X6_256, Y_249) | ~be(U_206, X5_255, V_246, X6_256) | ~state(U_206, X5_255) | ~group(U_206, X4_254) | ~group(U_206, X3_253) | ~two(U_206, X3_253) | ~in(U_206, X2_252, X1_251) | ~down(U_206, X2_252, X1_251) | ~barrel(U_206, X2_252) | ~present(U_206, X2_252) | ~agent(U_206, X2_252, Y_249) | ~event(U_206, X2_252) | ~lonely(U_206, X1_251) | ~street(U_206, X1_251) | ~placename(U_206, Z_250) | ~hollywood_placename(U_206, Z_250) | ~city(U_206, X1_251) | ~of(U_206, Z_250, X1_251) | ~old(U_206, Y_249) | ~dirty(U_206, Y_249) | ~white(U_206, Y_249) | ~chevy(U_206, Y_249) | ~frontseat(U_206, X_248) | ~wheel(U_206, Y_249) | ~forename(U_206, W_247) | ~jules_forename(U_206, W_247) | ~man(U_206, V_246) | ~of(U_206, W_247, V_246) | ~actual_world(U_206)))).
% 120.35/101.30 tff(c_19385, plain, (![Y_249, X2_252, V_246, Z_250, X_248, X13_279, X6_256, X3_253, W_247, U_206, X5_255, X1_251, X4_254]: (member(U_206, '#skF_37'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | ~young(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~fellow(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~wear(U_206, X13_279) | ~nonreflexive(U_206, X13_279) | ~present(U_206, X13_279) | ~patient(U_206, X13_279, '#skF_39'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~agent(U_206, X13_279, '#skF_40'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~event(U_206, X13_279) | member(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X4_254) | ~behind(U_206, X6_256, Y_249) | ~be(U_206, X5_255, V_246, X6_256) | ~state(U_206, X5_255) | ~group(U_206, X4_254) | ~group(U_206, X3_253) | ~two(U_206, X3_253) | ~in(U_206, X2_252, X1_251) | ~down(U_206, X2_252, X1_251) | ~barrel(U_206, X2_252) | ~present(U_206, X2_252) | ~agent(U_206, X2_252, Y_249) | ~event(U_206, X2_252) | ~lonely(U_206, X1_251) | ~street(U_206, X1_251) | ~placename(U_206, Z_250) | ~hollywood_placename(U_206, Z_250) | ~city(U_206, X1_251) | ~of(U_206, Z_250, X1_251) | ~old(U_206, Y_249) | ~dirty(U_206, Y_249) | ~white(U_206, Y_249) | ~chevy(U_206, Y_249) | ~frontseat(U_206, X_248) | ~wheel(U_206, Y_249) | ~forename(U_206, W_247) | ~jules_forename(U_206, W_247) | ~man(U_206, V_246) | ~of(U_206, W_247, V_246) | ~actual_world(U_206)))).
% 120.35/101.30 tff(c_14952, plain, (![Y_249, X2_252, V_246, X9_274, Z_250, X_248, X8_273, X6_256, X3_253, W_247, U_206, X5_255, X1_251, X4_254]: (~in(U_206, X9_274, X_248) | ~be(U_206, X8_273, '#skF_37'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X9_274) | ~state(U_206, X8_273) | member(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | member(U_206, '#skF_40'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | ~cheap(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~black(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~coat(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~behind(U_206, X6_256, Y_249) | ~be(U_206, X5_255, V_246, X6_256) | ~state(U_206, X5_255) | ~group(U_206, X4_254) | ~group(U_206, X3_253) | ~two(U_206, X3_253) | ~in(U_206, X2_252, X1_251) | ~down(U_206, X2_252, X1_251) | ~barrel(U_206, X2_252) | ~present(U_206, X2_252) | ~agent(U_206, X2_252, Y_249) | ~event(U_206, X2_252) | ~lonely(U_206, X1_251) | ~street(U_206, X1_251) | ~placename(U_206, Z_250) | ~hollywood_placename(U_206, Z_250) | ~city(U_206, X1_251) | ~of(U_206, Z_250, X1_251) | ~old(U_206, Y_249) | ~dirty(U_206, Y_249) | ~white(U_206, Y_249) | ~chevy(U_206, Y_249) | ~frontseat(U_206, X_248) | ~wheel(U_206, Y_249) | ~forename(U_206, W_247) | ~jules_forename(U_206, W_247) | ~man(U_206, V_246) | ~of(U_206, W_247, V_246) | ~actual_world(U_206)))).
% 120.35/101.30 tff(c_14943, plain, (![Y_249, X2_252, V_246, X9_274, Z_250, X_248, X8_273, X6_256, X3_253, W_247, U_206, X5_255, X1_251, X4_254]: (~in(U_206, X9_274, X_248) | ~be(U_206, X8_273, '#skF_37'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X9_274) | ~state(U_206, X8_273) | member(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | member(U_206, '#skF_39'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X4_254) | ~cheap(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~black(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~coat(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~behind(U_206, X6_256, Y_249) | ~be(U_206, X5_255, V_246, X6_256) | ~state(U_206, X5_255) | ~group(U_206, X4_254) | ~group(U_206, X3_253) | ~two(U_206, X3_253) | ~in(U_206, X2_252, X1_251) | ~down(U_206, X2_252, X1_251) | ~barrel(U_206, X2_252) | ~present(U_206, X2_252) | ~agent(U_206, X2_252, Y_249) | ~event(U_206, X2_252) | ~lonely(U_206, X1_251) | ~street(U_206, X1_251) | ~placename(U_206, Z_250) | ~hollywood_placename(U_206, Z_250) | ~city(U_206, X1_251) | ~of(U_206, Z_250, X1_251) | ~old(U_206, Y_249) | ~dirty(U_206, Y_249) | ~white(U_206, Y_249) | ~chevy(U_206, Y_249) | ~frontseat(U_206, X_248) | ~wheel(U_206, Y_249) | ~forename(U_206, W_247) | ~jules_forename(U_206, W_247) | ~man(U_206, V_246) | ~of(U_206, W_247, V_246) | ~actual_world(U_206)))).
% 120.35/101.30 tff(c_14931, plain, (![Y_249, X2_252, V_246, X9_274, Z_250, X_248, X8_273, X13_279, X6_256, X3_253, W_247, U_206, X5_255, X1_251, X4_254]: (~in(U_206, X9_274, X_248) | ~be(U_206, X8_273, '#skF_37'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X9_274) | ~state(U_206, X8_273) | member(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | ~wear(U_206, X13_279) | ~nonreflexive(U_206, X13_279) | ~present(U_206, X13_279) | ~patient(U_206, X13_279, '#skF_39'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~agent(U_206, X13_279, '#skF_40'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~event(U_206, X13_279) | member(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X4_254) | ~behind(U_206, X6_256, Y_249) | ~be(U_206, X5_255, V_246, X6_256) | ~state(U_206, X5_255) | ~group(U_206, X4_254) | ~group(U_206, X3_253) | ~two(U_206, X3_253) | ~in(U_206, X2_252, X1_251) | ~down(U_206, X2_252, X1_251) | ~barrel(U_206, X2_252) | ~present(U_206, X2_252) | ~agent(U_206, X2_252, Y_249) | ~event(U_206, X2_252) | ~lonely(U_206, X1_251) | ~street(U_206, X1_251) | ~placename(U_206, Z_250) | ~hollywood_placename(U_206, Z_250) | ~city(U_206, X1_251) | ~of(U_206, Z_250, X1_251) | ~old(U_206, Y_249) | ~dirty(U_206, Y_249) | ~white(U_206, Y_249) | ~chevy(U_206, Y_249) | ~frontseat(U_206, X_248) | ~wheel(U_206, Y_249) | ~forename(U_206, W_247) | ~jules_forename(U_206, W_247) | ~man(U_206, V_246) | ~of(U_206, W_247, V_246) | ~actual_world(U_206)))).
% 120.35/101.30 tff(c_14477, plain, (![Y_249, X2_252, V_246, Z_250, X_248, X6_256, X3_253, W_247, U_206, X5_255, X1_251, X4_254]: (member(U_206, '#skF_37'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | member(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | member(U_206, '#skF_39'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X4_254) | ~cheap(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~black(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~coat(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~behind(U_206, X6_256, Y_249) | ~be(U_206, X5_255, V_246, X6_256) | ~state(U_206, X5_255) | ~group(U_206, X4_254) | ~group(U_206, X3_253) | ~two(U_206, X3_253) | ~in(U_206, X2_252, X1_251) | ~down(U_206, X2_252, X1_251) | ~barrel(U_206, X2_252) | ~present(U_206, X2_252) | ~agent(U_206, X2_252, Y_249) | ~event(U_206, X2_252) | ~lonely(U_206, X1_251) | ~street(U_206, X1_251) | ~placename(U_206, Z_250) | ~hollywood_placename(U_206, Z_250) | ~city(U_206, X1_251) | ~of(U_206, Z_250, X1_251) | ~old(U_206, Y_249) | ~dirty(U_206, Y_249) | ~white(U_206, Y_249) | ~chevy(U_206, Y_249) | ~frontseat(U_206, X_248) | ~wheel(U_206, Y_249) | ~forename(U_206, W_247) | ~jules_forename(U_206, W_247) | ~man(U_206, V_246) | ~of(U_206, W_247, V_246) | ~actual_world(U_206)))).
% 120.35/101.30 tff(c_14387, plain, (![Y_249, X2_252, V_246, Z_250, X_248, X6_256, X3_253, W_247, U_206, X5_255, X1_251, X4_254]: (member(U_206, '#skF_37'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | member(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | member(U_206, '#skF_40'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | ~cheap(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~black(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~coat(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~behind(U_206, X6_256, Y_249) | ~be(U_206, X5_255, V_246, X6_256) | ~state(U_206, X5_255) | ~group(U_206, X4_254) | ~group(U_206, X3_253) | ~two(U_206, X3_253) | ~in(U_206, X2_252, X1_251) | ~down(U_206, X2_252, X1_251) | ~barrel(U_206, X2_252) | ~present(U_206, X2_252) | ~agent(U_206, X2_252, Y_249) | ~event(U_206, X2_252) | ~lonely(U_206, X1_251) | ~street(U_206, X1_251) | ~placename(U_206, Z_250) | ~hollywood_placename(U_206, Z_250) | ~city(U_206, X1_251) | ~of(U_206, Z_250, X1_251) | ~old(U_206, Y_249) | ~dirty(U_206, Y_249) | ~white(U_206, Y_249) | ~chevy(U_206, Y_249) | ~frontseat(U_206, X_248) | ~wheel(U_206, Y_249) | ~forename(U_206, W_247) | ~jules_forename(U_206, W_247) | ~man(U_206, V_246) | ~of(U_206, W_247, V_246) | ~actual_world(U_206)))).
% 120.35/101.30 tff(c_14377, plain, (![Y_249, X2_252, V_246, Z_250, X_248, X13_279, X6_256, X3_253, W_247, U_206, X5_255, X1_251, X4_254]: (member(U_206, '#skF_37'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | member(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | ~wear(U_206, X13_279) | ~nonreflexive(U_206, X13_279) | ~present(U_206, X13_279) | ~patient(U_206, X13_279, '#skF_39'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~agent(U_206, X13_279, '#skF_40'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~event(U_206, X13_279) | member(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X4_254) | ~behind(U_206, X6_256, Y_249) | ~be(U_206, X5_255, V_246, X6_256) | ~state(U_206, X5_255) | ~group(U_206, X4_254) | ~group(U_206, X3_253) | ~two(U_206, X3_253) | ~in(U_206, X2_252, X1_251) | ~down(U_206, X2_252, X1_251) | ~barrel(U_206, X2_252) | ~present(U_206, X2_252) | ~agent(U_206, X2_252, Y_249) | ~event(U_206, X2_252) | ~lonely(U_206, X1_251) | ~street(U_206, X1_251) | ~placename(U_206, Z_250) | ~hollywood_placename(U_206, Z_250) | ~city(U_206, X1_251) | ~of(U_206, Z_250, X1_251) | ~old(U_206, Y_249) | ~dirty(U_206, Y_249) | ~white(U_206, Y_249) | ~chevy(U_206, Y_249) | ~frontseat(U_206, X_248) | ~wheel(U_206, Y_249) | ~forename(U_206, W_247) | ~jules_forename(U_206, W_247) | ~man(U_206, V_246) | ~of(U_206, W_247, V_246) | ~actual_world(U_206)))).
% 120.35/101.30 tff(c_13718, plain, (![Y_249, X2_252, V_246, X9_274, Z_250, X_248, X8_273, X6_256, X3_253, W_247, U_206, X5_255, X1_251, X4_254]: (~in(U_206, X9_274, X_248) | ~be(U_206, X8_273, '#skF_37'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X9_274) | ~state(U_206, X8_273) | ~young(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~fellow(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | member(U_206, '#skF_39'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X4_254) | member(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X4_254) | ~behind(U_206, X6_256, Y_249) | ~be(U_206, X5_255, V_246, X6_256) | ~state(U_206, X5_255) | ~group(U_206, X4_254) | ~group(U_206, X3_253) | ~two(U_206, X3_253) | ~in(U_206, X2_252, X1_251) | ~down(U_206, X2_252, X1_251) | ~barrel(U_206, X2_252) | ~present(U_206, X2_252) | ~agent(U_206, X2_252, Y_249) | ~event(U_206, X2_252) | ~lonely(U_206, X1_251) | ~street(U_206, X1_251) | ~placename(U_206, Z_250) | ~hollywood_placename(U_206, Z_250) | ~city(U_206, X1_251) | ~of(U_206, Z_250, X1_251) | ~old(U_206, Y_249) | ~dirty(U_206, Y_249) | ~white(U_206, Y_249) | ~chevy(U_206, Y_249) | ~frontseat(U_206, X_248) | ~wheel(U_206, Y_249) | ~forename(U_206, W_247) | ~jules_forename(U_206, W_247) | ~man(U_206, V_246) | ~of(U_206, W_247, V_246) | ~actual_world(U_206)))).
% 120.35/101.30 tff(c_13710, plain, (![Y_249, X2_252, V_246, X9_274, Z_250, X_248, X8_273, X6_256, X3_253, W_247, U_206, X5_255, X1_251, X4_254]: (~in(U_206, X9_274, X_248) | ~be(U_206, X8_273, '#skF_37'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X9_274) | ~state(U_206, X8_273) | ~young(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~fellow(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | member(U_206, '#skF_40'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | member(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X4_254) | ~behind(U_206, X6_256, Y_249) | ~be(U_206, X5_255, V_246, X6_256) | ~state(U_206, X5_255) | ~group(U_206, X4_254) | ~group(U_206, X3_253) | ~two(U_206, X3_253) | ~in(U_206, X2_252, X1_251) | ~down(U_206, X2_252, X1_251) | ~barrel(U_206, X2_252) | ~present(U_206, X2_252) | ~agent(U_206, X2_252, Y_249) | ~event(U_206, X2_252) | ~lonely(U_206, X1_251) | ~street(U_206, X1_251) | ~placename(U_206, Z_250) | ~hollywood_placename(U_206, Z_250) | ~city(U_206, X1_251) | ~of(U_206, Z_250, X1_251) | ~old(U_206, Y_249) | ~dirty(U_206, Y_249) | ~white(U_206, Y_249) | ~chevy(U_206, Y_249) | ~frontseat(U_206, X_248) | ~wheel(U_206, Y_249) | ~forename(U_206, W_247) | ~jules_forename(U_206, W_247) | ~man(U_206, V_246) | ~of(U_206, W_247, V_246) | ~actual_world(U_206)))).
% 120.35/101.30 tff(c_12088, plain, (![Y_249, X2_252, V_246, Z_250, X_248, X6_256, X3_253, W_247, U_206, X5_255, X1_251, X4_254]: (member(U_206, '#skF_37'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | ~young(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~fellow(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | member(U_206, '#skF_39'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X4_254) | member(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X4_254) | ~behind(U_206, X6_256, Y_249) | ~be(U_206, X5_255, V_246, X6_256) | ~state(U_206, X5_255) | ~group(U_206, X4_254) | ~group(U_206, X3_253) | ~two(U_206, X3_253) | ~in(U_206, X2_252, X1_251) | ~down(U_206, X2_252, X1_251) | ~barrel(U_206, X2_252) | ~present(U_206, X2_252) | ~agent(U_206, X2_252, Y_249) | ~event(U_206, X2_252) | ~lonely(U_206, X1_251) | ~street(U_206, X1_251) | ~placename(U_206, Z_250) | ~hollywood_placename(U_206, Z_250) | ~city(U_206, X1_251) | ~of(U_206, Z_250, X1_251) | ~old(U_206, Y_249) | ~dirty(U_206, Y_249) | ~white(U_206, Y_249) | ~chevy(U_206, Y_249) | ~frontseat(U_206, X_248) | ~wheel(U_206, Y_249) | ~forename(U_206, W_247) | ~jules_forename(U_206, W_247) | ~man(U_206, V_246) | ~of(U_206, W_247, V_246) | ~actual_world(U_206)))).
% 120.35/101.30 tff(c_11928, plain, (![Y_249, X2_252, V_246, Z_250, X_248, X6_256, X3_253, W_247, U_206, X5_255, X1_251, X4_254]: (member(U_206, '#skF_37'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | ~young(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | ~fellow(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254)) | member(U_206, '#skF_40'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | member(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X4_254) | ~behind(U_206, X6_256, Y_249) | ~be(U_206, X5_255, V_246, X6_256) | ~state(U_206, X5_255) | ~group(U_206, X4_254) | ~group(U_206, X3_253) | ~two(U_206, X3_253) | ~in(U_206, X2_252, X1_251) | ~down(U_206, X2_252, X1_251) | ~barrel(U_206, X2_252) | ~present(U_206, X2_252) | ~agent(U_206, X2_252, Y_249) | ~event(U_206, X2_252) | ~lonely(U_206, X1_251) | ~street(U_206, X1_251) | ~placename(U_206, Z_250) | ~hollywood_placename(U_206, Z_250) | ~city(U_206, X1_251) | ~of(U_206, Z_250, X1_251) | ~old(U_206, Y_249) | ~dirty(U_206, Y_249) | ~white(U_206, Y_249) | ~chevy(U_206, Y_249) | ~frontseat(U_206, X_248) | ~wheel(U_206, Y_249) | ~forename(U_206, W_247) | ~jules_forename(U_206, W_247) | ~man(U_206, V_246) | ~of(U_206, W_247, V_246) | ~actual_world(U_206)))).
% 120.35/101.30 tff(c_11846, plain, (![Y_249, X2_252, V_246, X9_274, Z_250, X_248, X8_273, X6_256, X3_253, W_247, U_206, X5_255, X1_251, X4_254]: (~in(U_206, X9_274, X_248) | ~be(U_206, X8_273, '#skF_37'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X9_274) | ~state(U_206, X8_273) | member(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | member(U_206, '#skF_39'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X4_254) | member(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X4_254) | ~behind(U_206, X6_256, Y_249) | ~be(U_206, X5_255, V_246, X6_256) | ~state(U_206, X5_255) | ~group(U_206, X4_254) | ~group(U_206, X3_253) | ~two(U_206, X3_253) | ~in(U_206, X2_252, X1_251) | ~down(U_206, X2_252, X1_251) | ~barrel(U_206, X2_252) | ~present(U_206, X2_252) | ~agent(U_206, X2_252, Y_249) | ~event(U_206, X2_252) | ~lonely(U_206, X1_251) | ~street(U_206, X1_251) | ~placename(U_206, Z_250) | ~hollywood_placename(U_206, Z_250) | ~city(U_206, X1_251) | ~of(U_206, Z_250, X1_251) | ~old(U_206, Y_249) | ~dirty(U_206, Y_249) | ~white(U_206, Y_249) | ~chevy(U_206, Y_249) | ~frontseat(U_206, X_248) | ~wheel(U_206, Y_249) | ~forename(U_206, W_247) | ~jules_forename(U_206, W_247) | ~man(U_206, V_246) | ~of(U_206, W_247, V_246) | ~actual_world(U_206)))).
% 120.35/101.30 tff(c_11815, plain, (![Y_249, X2_252, V_246, X9_274, Z_250, X_248, X8_273, X6_256, X3_253, W_247, U_206, X5_255, X1_251, X4_254]: (~in(U_206, X9_274, X_248) | ~be(U_206, X8_273, '#skF_37'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X9_274) | ~state(U_206, X8_273) | member(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | member(U_206, '#skF_40'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | member(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X4_254) | ~behind(U_206, X6_256, Y_249) | ~be(U_206, X5_255, V_246, X6_256) | ~state(U_206, X5_255) | ~group(U_206, X4_254) | ~group(U_206, X3_253) | ~two(U_206, X3_253) | ~in(U_206, X2_252, X1_251) | ~down(U_206, X2_252, X1_251) | ~barrel(U_206, X2_252) | ~present(U_206, X2_252) | ~agent(U_206, X2_252, Y_249) | ~event(U_206, X2_252) | ~lonely(U_206, X1_251) | ~street(U_206, X1_251) | ~placename(U_206, Z_250) | ~hollywood_placename(U_206, Z_250) | ~city(U_206, X1_251) | ~of(U_206, Z_250, X1_251) | ~old(U_206, Y_249) | ~dirty(U_206, Y_249) | ~white(U_206, Y_249) | ~chevy(U_206, Y_249) | ~frontseat(U_206, X_248) | ~wheel(U_206, Y_249) | ~forename(U_206, W_247) | ~jules_forename(U_206, W_247) | ~man(U_206, V_246) | ~of(U_206, W_247, V_246) | ~actual_world(U_206)))).
% 120.35/101.30 tff(c_11739, plain, (~two('#skF_21', '#skF_31'))).
% 120.35/101.30 tff(c_10870, plain, (![Y_249, X2_252, V_246, Z_250, X_248, X6_256, X3_253, W_247, U_206, X5_255, X1_251, X4_254]: (member(U_206, '#skF_37'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | member(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | member(U_206, '#skF_39'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X4_254) | member(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X4_254) | ~behind(U_206, X6_256, Y_249) | ~be(U_206, X5_255, V_246, X6_256) | ~state(U_206, X5_255) | ~group(U_206, X4_254) | ~group(U_206, X3_253) | ~two(U_206, X3_253) | ~in(U_206, X2_252, X1_251) | ~down(U_206, X2_252, X1_251) | ~barrel(U_206, X2_252) | ~present(U_206, X2_252) | ~agent(U_206, X2_252, Y_249) | ~event(U_206, X2_252) | ~lonely(U_206, X1_251) | ~street(U_206, X1_251) | ~placename(U_206, Z_250) | ~hollywood_placename(U_206, Z_250) | ~city(U_206, X1_251) | ~of(U_206, Z_250, X1_251) | ~old(U_206, Y_249) | ~dirty(U_206, Y_249) | ~white(U_206, Y_249) | ~chevy(U_206, Y_249) | ~frontseat(U_206, X_248) | ~wheel(U_206, Y_249) | ~forename(U_206, W_247) | ~jules_forename(U_206, W_247) | ~man(U_206, V_246) | ~of(U_206, W_247, V_246) | ~actual_world(U_206)))).
% 120.35/101.30 tff(c_10759, plain, (![Y_249, X2_252, V_246, Z_250, X_248, X6_256, X3_253, W_247, U_206, X5_255, X1_251, X4_254]: (member(U_206, '#skF_37'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | member(U_206, '#skF_38'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | member(U_206, '#skF_40'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X3_253) | member(U_206, '#skF_41'(X3_253, X5_255, X_248, U_206, W_247, X6_256, X1_251, Z_250, Y_249, V_246, X2_252, X4_254), X4_254) | ~behind(U_206, X6_256, Y_249) | ~be(U_206, X5_255, V_246, X6_256) | ~state(U_206, X5_255) | ~group(U_206, X4_254) | ~group(U_206, X3_253) | ~two(U_206, X3_253) | ~in(U_206, X2_252, X1_251) | ~down(U_206, X2_252, X1_251) | ~barrel(U_206, X2_252) | ~present(U_206, X2_252) | ~agent(U_206, X2_252, Y_249) | ~event(U_206, X2_252) | ~lonely(U_206, X1_251) | ~street(U_206, X1_251) | ~placename(U_206, Z_250) | ~hollywood_placename(U_206, Z_250) | ~city(U_206, X1_251) | ~of(U_206, Z_250, X1_251) | ~old(U_206, Y_249) | ~dirty(U_206, Y_249) | ~white(U_206, Y_249) | ~chevy(U_206, Y_249) | ~frontseat(U_206, X_248) | ~wheel(U_206, Y_249) | ~forename(U_206, W_247) | ~jules_forename(U_206, W_247) | ~man(U_206, V_246) | ~of(U_206, W_247, V_246) | ~actual_world(U_206)))).
% 120.35/101.30 tff(c_10659, plain, (![X32_199, X33_203]: (patient('#skF_21', '#skF_36'(X32_199, X33_203), X32_199) | ~member('#skF_21', X33_203, '#skF_30') | ~member('#skF_21', X32_199, '#skF_31')))).
% 120.35/101.30 tff(c_10656, plain, (![X32_199, X33_203]: (agent('#skF_21', '#skF_36'(X32_199, X33_203), X33_203) | ~member('#skF_21', X33_203, '#skF_30') | ~member('#skF_21', X32_199, '#skF_31')))).
% 120.35/101.30 tff(c_10654, plain, (![X32_199, X33_203]: (wear('#skF_21', '#skF_36'(X32_199, X33_203)) | ~member('#skF_21', X33_203, '#skF_30') | ~member('#skF_21', X32_199, '#skF_31')))).
% 120.35/101.30 tff(c_10652, plain, (![X32_199, X33_203]: (nonreflexive('#skF_21', '#skF_36'(X32_199, X33_203)) | ~member('#skF_21', X33_203, '#skF_30') | ~member('#skF_21', X32_199, '#skF_31')))).
% 120.35/101.30 tff(c_10650, plain, (![X32_199, X33_203]: (event('#skF_21', '#skF_36'(X32_199, X33_203)) | ~member('#skF_21', X33_203, '#skF_30') | ~member('#skF_21', X32_199, '#skF_31')))).
% 120.35/101.30 tff(c_10648, plain, (![X32_199, X33_203]: (present('#skF_21', '#skF_36'(X32_199, X33_203)) | ~member('#skF_21', X33_203, '#skF_30') | ~member('#skF_21', X32_199, '#skF_31')))).
% 120.35/101.30 tff(c_10616, plain, (![X28_195]: (be('#skF_21', '#skF_34'(X28_195), X28_195, '#skF_35'(X28_195)) | ~member('#skF_21', X28_195, '#skF_30')))).
% 120.35/101.30 tff(c_10368, plain, (![X28_195]: (in('#skF_21', '#skF_35'(X28_195), '#skF_25') | ~member('#skF_21', X28_195, '#skF_30')))).
% 120.35/101.30 tff(c_10290, plain, (![X28_195]: (state('#skF_21', '#skF_34'(X28_195)) | ~member('#skF_21', X28_195, '#skF_30')))).
% 120.35/101.30 tff(c_10244, plain, (![X35_205]: (cheap('#skF_21', X35_205) | ~member('#skF_21', X35_205, '#skF_31')))).
% 120.35/101.30 tff(c_10241, plain, (![X35_205]: (black('#skF_21', X35_205) | ~member('#skF_21', X35_205, '#skF_31')))).
% 120.35/101.30 tff(c_10236, plain, (![X31_198]: (fellow('#skF_21', X31_198) | ~member('#skF_21', X31_198, '#skF_30')))).
% 120.35/101.30 tff(c_10232, plain, (![X35_205]: (coat('#skF_21', X35_205) | ~member('#skF_21', X35_205, '#skF_31')))).
% 120.35/101.30 tff(c_10228, plain, (![X31_198]: (young('#skF_21', X31_198) | ~member('#skF_21', X31_198, '#skF_30')))).
% 120.35/101.30 tff(c_10149, plain, (be('#skF_1', '#skF_11', '#skF_2', '#skF_12'))).
% 120.35/101.30 tff(c_10067, plain, (of('#skF_1', '#skF_6', '#skF_7'))).
% 120.35/101.30 tff(c_10059, plain, (of('#skF_1', '#skF_3', '#skF_2'))).
% 120.35/101.30 tff(c_10056, plain, (down('#skF_1', '#skF_8', '#skF_7'))).
% 120.35/101.30 tff(c_10053, plain, (in('#skF_1', '#skF_8', '#skF_7'))).
% 120.35/101.30 tff(c_10050, plain, (agent('#skF_1', '#skF_8', '#skF_5'))).
% 120.35/101.31 tff(c_10045, plain, (behind('#skF_1', '#skF_12', '#skF_5'))).
% 120.35/101.31 tff(c_9887, plain, (wheel('#skF_1', '#skF_5'))).
% 120.35/101.31 tff(c_9886, plain, (white('#skF_1', '#skF_5'))).
% 120.35/101.31 tff(c_9881, plain, (jules_forename('#skF_1', '#skF_3'))).
% 120.35/101.31 tff(c_9879, plain, (chevy('#skF_1', '#skF_5'))).
% 120.35/101.31 tff(c_9876, plain, (man('#skF_1', '#skF_2'))).
% 120.35/101.31 tff(c_9874, plain, (forename('#skF_1', '#skF_3'))).
% 120.35/101.31 tff(c_9872, plain, (city('#skF_1', '#skF_7'))).
% 120.35/101.31 tff(c_9869, plain, (frontseat('#skF_1', '#skF_4'))).
% 120.35/101.31 tff(c_9866, plain, (dirty('#skF_1', '#skF_5'))).
% 120.35/101.31 tff(c_9865, plain, (old('#skF_1', '#skF_5'))).
% 120.35/101.31 tff(c_9861, plain, (hollywood_placename('#skF_1', '#skF_6'))).
% 120.35/101.31 tff(c_9860, plain, (lonely('#skF_1', '#skF_7'))).
% 120.35/101.31 tff(c_9857, plain, (placename('#skF_1', '#skF_6'))).
% 120.35/101.31 tff(c_9856, plain, (street('#skF_1', '#skF_7'))).
% 120.35/101.31 tff(c_9854, plain, (event('#skF_1', '#skF_8'))).
% 120.35/101.31 tff(c_9853, plain, (barrel('#skF_1', '#skF_8'))).
% 120.35/101.31 tff(c_9852, plain, (present('#skF_1', '#skF_8'))).
% 120.35/101.31 tff(c_9846, plain, (two('#skF_1', '#skF_9'))).
% 120.35/101.31 tff(c_9845, plain, (group('#skF_1', '#skF_10'))).
% 120.35/101.31 tff(c_9843, plain, (state('#skF_1', '#skF_11'))).
% 120.35/101.31 tff(c_9841, plain, (group('#skF_1', '#skF_9'))).
% 120.35/101.31 tff(c_9807, plain, (actual_world('#skF_1'))).
% 120.35/101.31 tff(c_9636, plain, (be('#skF_21', '#skF_32', '#skF_22', '#skF_33'))).
% 120.35/101.31 tff(c_9329, plain, (behind('#skF_21', '#skF_33', '#skF_24'))).
% 120.35/101.31 tff(c_9301, plain, (agent('#skF_21', '#skF_29', '#skF_26'))).
% 120.35/101.31 tff(c_9292, plain, (down('#skF_21', '#skF_29', '#skF_28'))).
% 120.35/101.31 tff(c_9177, plain, (in('#skF_21', '#skF_29', '#skF_28'))).
% 120.35/101.31 tff(c_9162, plain, (of('#skF_21', '#skF_27', '#skF_28'))).
% 120.35/101.31 tff(c_9102, plain, (of('#skF_21', '#skF_23', '#skF_22'))).
% 120.35/101.31 tff(c_9015, plain, (old('#skF_21', '#skF_26'))).
% 120.35/101.31 tff(c_9014, plain, (state('#skF_21', '#skF_32'))).
% 120.35/101.31 tff(c_9013, plain, (wheel('#skF_21', '#skF_24'))).
% 120.35/101.31 tff(c_9010, plain, (man('#skF_21', '#skF_22'))).
% 120.35/101.31 tff(c_9003, plain, (city('#skF_21', '#skF_28'))).
% 120.35/101.31 tff(c_9002, plain, (frontseat('#skF_21', '#skF_25'))).
% 120.35/101.31 tff(c_9000, plain, (present('#skF_21', '#skF_29'))).
% 120.35/101.31 tff(c_8998, plain, (two('#skF_21', '#skF_30'))).
% 120.35/101.31 tff(c_8997, plain, (jules_forename('#skF_21', '#skF_23'))).
% 120.35/101.31 tff(c_8995, plain, (dirty('#skF_21', '#skF_26'))).
% 120.35/101.31 tff(c_8994, plain, (event('#skF_21', '#skF_29'))).
% 120.35/101.31 tff(c_8993, plain, (group('#skF_21', '#skF_31'))).
% 120.35/101.31 tff(c_8992, plain, (barrel('#skF_21', '#skF_29'))).
% 120.35/101.31 tff(c_8991, plain, (group('#skF_21', '#skF_30'))).
% 120.35/101.31 tff(c_8990, plain, (hollywood_placename('#skF_21', '#skF_27'))).
% 120.35/101.31 tff(c_8989, plain, (placename('#skF_21', '#skF_27'))).
% 120.35/101.31 tff(c_8988, plain, (forename('#skF_21', '#skF_23'))).
% 120.35/101.31 tff(c_8987, plain, (white('#skF_21', '#skF_26'))).
% 120.35/101.31 tff(c_8986, plain, (lonely('#skF_21', '#skF_28'))).
% 120.35/101.31 tff(c_8984, plain, (chevy('#skF_21', '#skF_26'))).
% 120.35/101.31 tff(c_8983, plain, (street('#skF_21', '#skF_28'))).
% 120.35/101.31 tff(c_8979, plain, (actual_world('#skF_21'))).
% 120.35/101.31 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 120.35/101.31
%------------------------------------------------------------------------------