%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : NLP192+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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n012.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 110.93s 92.62s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : NLP192+1 : TPTP v9.0.0. Released v2.4.0.
% 0.10/0.12 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.12/0.33 % Computer : n012.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Tue Apr 8 09:09:29 EDT 2025
% 0.12/0.33 % CPUTime :
% 110.93/92.62
% 110.93/92.62 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 110.93/92.63
% 110.93/92.63 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 110.93/92.63 %$ 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_36 > #skF_35 > #skF_37 > #skF_11 > #skF_31 > #skF_25 > #skF_7 > #skF_10 > #skF_34 > #skF_26 > #skF_5 > #skF_6 > #skF_2 > #skF_3 > #skF_1 > #skF_21 > #skF_9 > #skF_38 > #skF_32 > #skF_33 > #skF_8 > #skF_30 > #skF_13 > #skF_20 > #skF_16 > #skF_4 > #skF_22 > #skF_14 > #skF_29 > #skF_28 > #skF_19 > #skF_18 > #skF_24 > #skF_27 > #skF_23 > #skF_40 > #skF_17 > #skF_15 > #skF_12 > #skF_39
% 110.93/92.63
% 110.93/92.63 %Foreground sorts:
% 110.93/92.63
% 110.93/92.63
% 110.93/92.63 %Background operators:
% 110.93/92.63
% 110.93/92.63
% 110.93/92.63 %Foreground operators:
% 110.93/92.63 tff(cheap, type, cheap: ($i * $i) > $o).
% 110.93/92.63 tff(wear, type, wear: ($i * $i) > $o).
% 110.93/92.63 tff('#skF_36', type, '#skF_36': ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $i).
% 110.93/92.63 tff(two, type, two: ($i * $i) > $o).
% 110.93/92.63 tff('#skF_35', type, '#skF_35': ($i * $i) > $i).
% 110.93/92.63 tff(frontseat, type, frontseat: ($i * $i) > $o).
% 110.93/92.63 tff(placename, type, placename: ($i * $i) > $o).
% 110.93/92.63 tff(member, type, member: ($i * $i * $i) > $o).
% 110.93/92.63 tff(forename, type, forename: ($i * $i) > $o).
% 110.93/92.63 tff('#skF_37', type, '#skF_37': ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $i).
% 110.93/92.63 tff(be, type, be: ($i * $i * $i * $i) > $o).
% 110.93/92.63 tff(wheel, type, wheel: ($i * $i) > $o).
% 110.93/92.63 tff(black, type, black: ($i * $i) > $o).
% 110.93/92.63 tff(present, type, present: ($i * $i) > $o).
% 110.93/92.63 tff(in, type, in: ($i * $i * $i) > $o).
% 110.93/92.63 tff(old, type, old: ($i * $i) > $o).
% 110.93/92.63 tff(dirty, type, dirty: ($i * $i) > $o).
% 110.93/92.63 tff(behind, type, behind: ($i * $i * $i) > $o).
% 110.93/92.63 tff('#skF_11', type, '#skF_11': $i).
% 110.93/92.63 tff('#skF_31', type, '#skF_31': $i).
% 110.93/92.63 tff(city, type, city: ($i * $i) > $o).
% 110.93/92.63 tff('#skF_25', type, '#skF_25': $i).
% 110.93/92.63 tff(young, type, young: ($i * $i) > $o).
% 110.93/92.63 tff(of, type, of: ($i * $i * $i) > $o).
% 110.93/92.63 tff('#skF_7', type, '#skF_7': $i).
% 110.93/92.63 tff(actual_world, type, actual_world: $i > $o).
% 110.93/92.63 tff(agent, type, agent: ($i * $i * $i) > $o).
% 110.93/92.63 tff('#skF_10', type, '#skF_10': $i).
% 110.93/92.63 tff('#skF_34', type, '#skF_34': $i > $i).
% 110.93/92.63 tff('#skF_26', type, '#skF_26': $i).
% 110.93/92.63 tff('#skF_5', type, '#skF_5': $i).
% 110.93/92.63 tff(group, type, group: ($i * $i) > $o).
% 110.93/92.63 tff(lonely, type, lonely: ($i * $i) > $o).
% 110.93/92.63 tff(jules_forename, type, jules_forename: ($i * $i) > $o).
% 110.93/92.63 tff(fellow, type, fellow: ($i * $i) > $o).
% 110.93/92.63 tff('#skF_6', type, '#skF_6': $i).
% 110.93/92.63 tff('#skF_2', type, '#skF_2': $i).
% 110.93/92.63 tff('#skF_3', type, '#skF_3': $i).
% 110.93/92.63 tff(event, type, event: ($i * $i) > $o).
% 110.93/92.63 tff('#skF_1', type, '#skF_1': $i).
% 110.93/92.63 tff(down, type, down: ($i * $i * $i) > $o).
% 110.93/92.63 tff(patient, type, patient: ($i * $i * $i) > $o).
% 110.93/92.63 tff(hollywood_placename, type, hollywood_placename: ($i * $i) > $o).
% 110.93/92.63 tff(white, type, white: ($i * $i) > $o).
% 110.93/92.63 tff('#skF_21', type, '#skF_21': $i).
% 110.93/92.63 tff('#skF_9', type, '#skF_9': $i).
% 110.93/92.63 tff('#skF_38', type, '#skF_38': ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $i).
% 110.93/92.63 tff(barrel, type, barrel: ($i * $i) > $o).
% 110.93/92.63 tff('#skF_32', type, '#skF_32': $i).
% 110.93/92.63 tff(state, type, state: ($i * $i) > $o).
% 110.93/92.63 tff('#skF_33', type, '#skF_33': $i > $i).
% 110.93/92.63 tff(street, type, street: ($i * $i) > $o).
% 110.93/92.63 tff('#skF_8', type, '#skF_8': $i).
% 110.93/92.63 tff('#skF_30', type, '#skF_30': $i).
% 110.93/92.63 tff('#skF_13', type, '#skF_13': $i > $i).
% 110.93/92.63 tff(man, type, man: ($i * $i) > $o).
% 110.93/92.63 tff('#skF_20', type, '#skF_20': ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $i).
% 110.93/92.63 tff('#skF_16', type, '#skF_16': ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $i).
% 110.93/92.63 tff('#skF_4', type, '#skF_4': $i).
% 110.93/92.63 tff('#skF_22', type, '#skF_22': $i).
% 110.93/92.63 tff('#skF_14', type, '#skF_14': $i > $i).
% 110.93/92.63 tff('#skF_29', type, '#skF_29': $i).
% 110.93/92.63 tff('#skF_28', type, '#skF_28': $i).
% 110.93/92.63 tff('#skF_19', type, '#skF_19': ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $i).
% 110.93/92.63 tff('#skF_18', type, '#skF_18': ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $i).
% 110.93/92.63 tff('#skF_24', type, '#skF_24': $i).
% 110.93/92.63 tff('#skF_27', type, '#skF_27': $i).
% 110.93/92.63 tff('#skF_23', type, '#skF_23': $i).
% 110.93/92.63 tff(nonreflexive, type, nonreflexive: ($i * $i) > $o).
% 110.93/92.63 tff(chevy, type, chevy: ($i * $i) > $o).
% 110.93/92.63 tff('#skF_40', type, '#skF_40': ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $i).
% 110.93/92.63 tff('#skF_17', type, '#skF_17': ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $i).
% 110.93/92.63 tff(coat, type, coat: ($i * $i) > $o).
% 110.93/92.63 tff('#skF_15', type, '#skF_15': ($i * $i) > $i).
% 110.93/92.63 tff('#skF_12', type, '#skF_12': $i).
% 110.93/92.63 tff('#skF_39', type, '#skF_39': ($i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i * $i) > $i).
% 110.93/92.63
% 110.93/92.63 %Saturated clause set:
% 110.93/92.64 tff(c_30860, plain, (~chevy('#skF_21', '#skF_27'))).
% 111.04/92.64 tff(c_30853, plain, (![X2_2591, Z_2598, V_2593, W_2597, Y_2595, X1_2590, X5_2596, X6_2594]: (~behind('#skF_21', X6_2594, Y_2595) | ~be('#skF_21', X5_2596, V_2593, X6_2594) | ~state('#skF_21', X5_2596) | ~in('#skF_21', X2_2591, X1_2590) | ~down('#skF_21', X2_2591, X1_2590) | ~barrel('#skF_21', X2_2591) | ~present('#skF_21', X2_2591) | ~agent('#skF_21', X2_2591, Y_2595) | ~event('#skF_21', X2_2591) | ~lonely('#skF_21', X1_2590) | ~street('#skF_21', X1_2590) | ~placename('#skF_21', Z_2598) | ~hollywood_placename('#skF_21', Z_2598) | ~city('#skF_21', X1_2590) | ~of('#skF_21', Z_2598, X1_2590) | ~old('#skF_21', Y_2595) | ~dirty('#skF_21', Y_2595) | ~white('#skF_21', Y_2595) | ~chevy('#skF_21', Y_2595) | ~wheel('#skF_21', Y_2595) | ~forename('#skF_21', W_2597) | ~jules_forename('#skF_21', W_2597) | ~man('#skF_21', V_2593) | ~of('#skF_21', W_2597, V_2593)))).
% 111.04/92.64 tff(c_23016, plain, (![V_243, W_244, U_203, X1_248, X2_249, X_245, Y_246, X4_251, X8_270, X6_253, X5_252, X3_250, Z_247, X13_276, X9_271]: (~in(U_203, X9_271, X_245) | ~be(U_203, X8_270, '#skF_36'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X9_271) | ~state(U_203, X8_270) | ~young(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~fellow(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~wear(U_203, X13_276) | ~nonreflexive(U_203, X13_276) | ~present(U_203, X13_276) | ~patient(U_203, X13_276, '#skF_38'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~agent(U_203, X13_276, '#skF_39'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~event(U_203, X13_276) | ~cheap(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~black(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~coat(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~behind(U_203, X6_253, Y_246) | ~be(U_203, X5_252, V_243, X6_253) | ~state(U_203, X5_252) | ~group(U_203, X4_251) | ~group(U_203, X3_250) | ~two(U_203, X3_250) | ~in(U_203, X2_249, X1_248) | ~down(U_203, X2_249, X1_248) | ~barrel(U_203, X2_249) | ~present(U_203, X2_249) | ~agent(U_203, X2_249, Y_246) | ~event(U_203, X2_249) | ~lonely(U_203, X1_248) | ~street(U_203, X1_248) | ~placename(U_203, Z_247) | ~hollywood_placename(U_203, Z_247) | ~city(U_203, X1_248) | ~of(U_203, Z_247, X1_248) | ~old(U_203, Y_246) | ~dirty(U_203, Y_246) | ~white(U_203, Y_246) | ~chevy(U_203, Y_246) | ~frontseat(U_203, X_245) | ~wheel(U_203, Y_246) | ~forename(U_203, W_244) | ~jules_forename(U_203, W_244) | ~man(U_203, V_243) | ~of(U_203, W_244, V_243) | ~actual_world(U_203)))).
% 111.04/92.64 tff(c_22949, plain, (![V_243, W_244, U_203, X1_248, X2_249, X_245, Y_246, X4_251, X6_253, X5_252, X3_250, Z_247, X13_276]: (member(U_203, '#skF_36'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | ~young(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~fellow(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~wear(U_203, X13_276) | ~nonreflexive(U_203, X13_276) | ~present(U_203, X13_276) | ~patient(U_203, X13_276, '#skF_38'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~agent(U_203, X13_276, '#skF_39'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~event(U_203, X13_276) | ~cheap(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~black(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~coat(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~behind(U_203, X6_253, Y_246) | ~be(U_203, X5_252, V_243, X6_253) | ~state(U_203, X5_252) | ~group(U_203, X4_251) | ~group(U_203, X3_250) | ~two(U_203, X3_250) | ~in(U_203, X2_249, X1_248) | ~down(U_203, X2_249, X1_248) | ~barrel(U_203, X2_249) | ~present(U_203, X2_249) | ~agent(U_203, X2_249, Y_246) | ~event(U_203, X2_249) | ~lonely(U_203, X1_248) | ~street(U_203, X1_248) | ~placename(U_203, Z_247) | ~hollywood_placename(U_203, Z_247) | ~city(U_203, X1_248) | ~of(U_203, Z_247, X1_248) | ~old(U_203, Y_246) | ~dirty(U_203, Y_246) | ~white(U_203, Y_246) | ~chevy(U_203, Y_246) | ~frontseat(U_203, X_245) | ~wheel(U_203, Y_246) | ~forename(U_203, W_244) | ~jules_forename(U_203, W_244) | ~man(U_203, V_243) | ~of(U_203, W_244, V_243) | ~actual_world(U_203)))).
% 111.04/92.64 tff(c_21268, plain, (![V_243, W_244, U_203, X1_248, X2_249, X_245, Y_246, X4_251, X8_270, X6_253, X5_252, X3_250, Z_247, X13_276, X9_271]: (~in(U_203, X9_271, X_245) | ~be(U_203, X8_270, '#skF_36'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X9_271) | ~state(U_203, X8_270) | member(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | ~wear(U_203, X13_276) | ~nonreflexive(U_203, X13_276) | ~present(U_203, X13_276) | ~patient(U_203, X13_276, '#skF_38'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~agent(U_203, X13_276, '#skF_39'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~event(U_203, X13_276) | ~cheap(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~black(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~coat(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~behind(U_203, X6_253, Y_246) | ~be(U_203, X5_252, V_243, X6_253) | ~state(U_203, X5_252) | ~group(U_203, X4_251) | ~group(U_203, X3_250) | ~two(U_203, X3_250) | ~in(U_203, X2_249, X1_248) | ~down(U_203, X2_249, X1_248) | ~barrel(U_203, X2_249) | ~present(U_203, X2_249) | ~agent(U_203, X2_249, Y_246) | ~event(U_203, X2_249) | ~lonely(U_203, X1_248) | ~street(U_203, X1_248) | ~placename(U_203, Z_247) | ~hollywood_placename(U_203, Z_247) | ~city(U_203, X1_248) | ~of(U_203, Z_247, X1_248) | ~old(U_203, Y_246) | ~dirty(U_203, Y_246) | ~white(U_203, Y_246) | ~chevy(U_203, Y_246) | ~frontseat(U_203, X_245) | ~wheel(U_203, Y_246) | ~forename(U_203, W_244) | ~jules_forename(U_203, W_244) | ~man(U_203, V_243) | ~of(U_203, W_244, V_243) | ~actual_world(U_203)))).
% 111.04/92.64 tff(c_21202, plain, (![V_243, W_244, U_203, X1_248, X2_249, X_245, Y_246, X4_251, X6_253, X5_252, X3_250, Z_247, X13_276]: (member(U_203, '#skF_36'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | member(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | ~wear(U_203, X13_276) | ~nonreflexive(U_203, X13_276) | ~present(U_203, X13_276) | ~patient(U_203, X13_276, '#skF_38'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~agent(U_203, X13_276, '#skF_39'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~event(U_203, X13_276) | ~cheap(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~black(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~coat(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~behind(U_203, X6_253, Y_246) | ~be(U_203, X5_252, V_243, X6_253) | ~state(U_203, X5_252) | ~group(U_203, X4_251) | ~group(U_203, X3_250) | ~two(U_203, X3_250) | ~in(U_203, X2_249, X1_248) | ~down(U_203, X2_249, X1_248) | ~barrel(U_203, X2_249) | ~present(U_203, X2_249) | ~agent(U_203, X2_249, Y_246) | ~event(U_203, X2_249) | ~lonely(U_203, X1_248) | ~street(U_203, X1_248) | ~placename(U_203, Z_247) | ~hollywood_placename(U_203, Z_247) | ~city(U_203, X1_248) | ~of(U_203, Z_247, X1_248) | ~old(U_203, Y_246) | ~dirty(U_203, Y_246) | ~white(U_203, Y_246) | ~chevy(U_203, Y_246) | ~frontseat(U_203, X_245) | ~wheel(U_203, Y_246) | ~forename(U_203, W_244) | ~jules_forename(U_203, W_244) | ~man(U_203, V_243) | ~of(U_203, W_244, V_243) | ~actual_world(U_203)))).
% 111.04/92.65 tff(c_20865, plain, (![V_243, W_244, U_203, X1_248, X2_249, X_245, Y_246, X4_251, X8_270, X6_253, X5_252, X3_250, Z_247, X9_271]: (~in(U_203, X9_271, X_245) | ~be(U_203, X8_270, '#skF_36'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X9_271) | ~state(U_203, X8_270) | ~young(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~fellow(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | member(U_203, '#skF_38'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X4_251) | ~cheap(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~black(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~coat(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~behind(U_203, X6_253, Y_246) | ~be(U_203, X5_252, V_243, X6_253) | ~state(U_203, X5_252) | ~group(U_203, X4_251) | ~group(U_203, X3_250) | ~two(U_203, X3_250) | ~in(U_203, X2_249, X1_248) | ~down(U_203, X2_249, X1_248) | ~barrel(U_203, X2_249) | ~present(U_203, X2_249) | ~agent(U_203, X2_249, Y_246) | ~event(U_203, X2_249) | ~lonely(U_203, X1_248) | ~street(U_203, X1_248) | ~placename(U_203, Z_247) | ~hollywood_placename(U_203, Z_247) | ~city(U_203, X1_248) | ~of(U_203, Z_247, X1_248) | ~old(U_203, Y_246) | ~dirty(U_203, Y_246) | ~white(U_203, Y_246) | ~chevy(U_203, Y_246) | ~frontseat(U_203, X_245) | ~wheel(U_203, Y_246) | ~forename(U_203, W_244) | ~jules_forename(U_203, W_244) | ~man(U_203, V_243) | ~of(U_203, W_244, V_243) | ~actual_world(U_203)))).
% 111.04/92.65 tff(c_20857, plain, (![V_243, W_244, U_203, X1_248, X2_249, X_245, Y_246, X4_251, X8_270, X6_253, X5_252, X3_250, Z_247, X9_271]: (~in(U_203, X9_271, X_245) | ~be(U_203, X8_270, '#skF_36'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X9_271) | ~state(U_203, X8_270) | ~young(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~fellow(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | member(U_203, '#skF_39'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | ~cheap(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~black(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~coat(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~behind(U_203, X6_253, Y_246) | ~be(U_203, X5_252, V_243, X6_253) | ~state(U_203, X5_252) | ~group(U_203, X4_251) | ~group(U_203, X3_250) | ~two(U_203, X3_250) | ~in(U_203, X2_249, X1_248) | ~down(U_203, X2_249, X1_248) | ~barrel(U_203, X2_249) | ~present(U_203, X2_249) | ~agent(U_203, X2_249, Y_246) | ~event(U_203, X2_249) | ~lonely(U_203, X1_248) | ~street(U_203, X1_248) | ~placename(U_203, Z_247) | ~hollywood_placename(U_203, Z_247) | ~city(U_203, X1_248) | ~of(U_203, Z_247, X1_248) | ~old(U_203, Y_246) | ~dirty(U_203, Y_246) | ~white(U_203, Y_246) | ~chevy(U_203, Y_246) | ~frontseat(U_203, X_245) | ~wheel(U_203, Y_246) | ~forename(U_203, W_244) | ~jules_forename(U_203, W_244) | ~man(U_203, V_243) | ~of(U_203, W_244, V_243) | ~actual_world(U_203)))).
% 111.04/92.65 tff(c_20849, plain, (![V_243, W_244, U_203, X1_248, X2_249, X_245, Y_246, X4_251, X8_270, X6_253, X5_252, X3_250, Z_247, X13_276, X9_271]: (~in(U_203, X9_271, X_245) | ~be(U_203, X8_270, '#skF_36'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X9_271) | ~state(U_203, X8_270) | ~young(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~fellow(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~wear(U_203, X13_276) | ~nonreflexive(U_203, X13_276) | ~present(U_203, X13_276) | ~patient(U_203, X13_276, '#skF_38'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~agent(U_203, X13_276, '#skF_39'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~event(U_203, X13_276) | member(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X4_251) | ~behind(U_203, X6_253, Y_246) | ~be(U_203, X5_252, V_243, X6_253) | ~state(U_203, X5_252) | ~group(U_203, X4_251) | ~group(U_203, X3_250) | ~two(U_203, X3_250) | ~in(U_203, X2_249, X1_248) | ~down(U_203, X2_249, X1_248) | ~barrel(U_203, X2_249) | ~present(U_203, X2_249) | ~agent(U_203, X2_249, Y_246) | ~event(U_203, X2_249) | ~lonely(U_203, X1_248) | ~street(U_203, X1_248) | ~placename(U_203, Z_247) | ~hollywood_placename(U_203, Z_247) | ~city(U_203, X1_248) | ~of(U_203, Z_247, X1_248) | ~old(U_203, Y_246) | ~dirty(U_203, Y_246) | ~white(U_203, Y_246) | ~chevy(U_203, Y_246) | ~frontseat(U_203, X_245) | ~wheel(U_203, Y_246) | ~forename(U_203, W_244) | ~jules_forename(U_203, W_244) | ~man(U_203, V_243) | ~of(U_203, W_244, V_243) | ~actual_world(U_203)))).
% 111.04/92.65 tff(c_19586, plain, (![V_243, W_244, U_203, X1_248, X2_249, X_245, Y_246, X4_251, X6_253, X5_252, X3_250, Z_247]: (member(U_203, '#skF_36'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | ~young(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~fellow(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | member(U_203, '#skF_39'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | ~cheap(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~black(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~coat(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~behind(U_203, X6_253, Y_246) | ~be(U_203, X5_252, V_243, X6_253) | ~state(U_203, X5_252) | ~group(U_203, X4_251) | ~group(U_203, X3_250) | ~two(U_203, X3_250) | ~in(U_203, X2_249, X1_248) | ~down(U_203, X2_249, X1_248) | ~barrel(U_203, X2_249) | ~present(U_203, X2_249) | ~agent(U_203, X2_249, Y_246) | ~event(U_203, X2_249) | ~lonely(U_203, X1_248) | ~street(U_203, X1_248) | ~placename(U_203, Z_247) | ~hollywood_placename(U_203, Z_247) | ~city(U_203, X1_248) | ~of(U_203, Z_247, X1_248) | ~old(U_203, Y_246) | ~dirty(U_203, Y_246) | ~white(U_203, Y_246) | ~chevy(U_203, Y_246) | ~frontseat(U_203, X_245) | ~wheel(U_203, Y_246) | ~forename(U_203, W_244) | ~jules_forename(U_203, W_244) | ~man(U_203, V_243) | ~of(U_203, W_244, V_243) | ~actual_world(U_203)))).
% 111.04/92.65 tff(c_19479, plain, (![V_243, W_244, U_203, X1_248, X2_249, X_245, Y_246, X4_251, X6_253, X5_252, X3_250, Z_247]: (member(U_203, '#skF_36'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | ~young(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~fellow(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | member(U_203, '#skF_38'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X4_251) | ~cheap(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~black(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~coat(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~behind(U_203, X6_253, Y_246) | ~be(U_203, X5_252, V_243, X6_253) | ~state(U_203, X5_252) | ~group(U_203, X4_251) | ~group(U_203, X3_250) | ~two(U_203, X3_250) | ~in(U_203, X2_249, X1_248) | ~down(U_203, X2_249, X1_248) | ~barrel(U_203, X2_249) | ~present(U_203, X2_249) | ~agent(U_203, X2_249, Y_246) | ~event(U_203, X2_249) | ~lonely(U_203, X1_248) | ~street(U_203, X1_248) | ~placename(U_203, Z_247) | ~hollywood_placename(U_203, Z_247) | ~city(U_203, X1_248) | ~of(U_203, Z_247, X1_248) | ~old(U_203, Y_246) | ~dirty(U_203, Y_246) | ~white(U_203, Y_246) | ~chevy(U_203, Y_246) | ~frontseat(U_203, X_245) | ~wheel(U_203, Y_246) | ~forename(U_203, W_244) | ~jules_forename(U_203, W_244) | ~man(U_203, V_243) | ~of(U_203, W_244, V_243) | ~actual_world(U_203)))).
% 111.04/92.65 tff(c_19471, plain, (![V_243, W_244, U_203, X1_248, X2_249, X_245, Y_246, X4_251, X6_253, X5_252, X3_250, Z_247, X13_276]: (member(U_203, '#skF_36'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | ~young(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~fellow(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~wear(U_203, X13_276) | ~nonreflexive(U_203, X13_276) | ~present(U_203, X13_276) | ~patient(U_203, X13_276, '#skF_38'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~agent(U_203, X13_276, '#skF_39'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~event(U_203, X13_276) | member(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X4_251) | ~behind(U_203, X6_253, Y_246) | ~be(U_203, X5_252, V_243, X6_253) | ~state(U_203, X5_252) | ~group(U_203, X4_251) | ~group(U_203, X3_250) | ~two(U_203, X3_250) | ~in(U_203, X2_249, X1_248) | ~down(U_203, X2_249, X1_248) | ~barrel(U_203, X2_249) | ~present(U_203, X2_249) | ~agent(U_203, X2_249, Y_246) | ~event(U_203, X2_249) | ~lonely(U_203, X1_248) | ~street(U_203, X1_248) | ~placename(U_203, Z_247) | ~hollywood_placename(U_203, Z_247) | ~city(U_203, X1_248) | ~of(U_203, Z_247, X1_248) | ~old(U_203, Y_246) | ~dirty(U_203, Y_246) | ~white(U_203, Y_246) | ~chevy(U_203, Y_246) | ~frontseat(U_203, X_245) | ~wheel(U_203, Y_246) | ~forename(U_203, W_244) | ~jules_forename(U_203, W_244) | ~man(U_203, V_243) | ~of(U_203, W_244, V_243) | ~actual_world(U_203)))).
% 111.04/92.65 tff(c_15033, plain, (![V_243, W_244, U_203, X1_248, X2_249, X_245, Y_246, X4_251, X8_270, X6_253, X5_252, X3_250, Z_247, X9_271]: (~in(U_203, X9_271, X_245) | ~be(U_203, X8_270, '#skF_36'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X9_271) | ~state(U_203, X8_270) | member(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | member(U_203, '#skF_38'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X4_251) | ~cheap(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~black(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~coat(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~behind(U_203, X6_253, Y_246) | ~be(U_203, X5_252, V_243, X6_253) | ~state(U_203, X5_252) | ~group(U_203, X4_251) | ~group(U_203, X3_250) | ~two(U_203, X3_250) | ~in(U_203, X2_249, X1_248) | ~down(U_203, X2_249, X1_248) | ~barrel(U_203, X2_249) | ~present(U_203, X2_249) | ~agent(U_203, X2_249, Y_246) | ~event(U_203, X2_249) | ~lonely(U_203, X1_248) | ~street(U_203, X1_248) | ~placename(U_203, Z_247) | ~hollywood_placename(U_203, Z_247) | ~city(U_203, X1_248) | ~of(U_203, Z_247, X1_248) | ~old(U_203, Y_246) | ~dirty(U_203, Y_246) | ~white(U_203, Y_246) | ~chevy(U_203, Y_246) | ~frontseat(U_203, X_245) | ~wheel(U_203, Y_246) | ~forename(U_203, W_244) | ~jules_forename(U_203, W_244) | ~man(U_203, V_243) | ~of(U_203, W_244, V_243) | ~actual_world(U_203)))).
% 111.04/92.65 tff(c_15025, plain, (![V_243, W_244, U_203, X1_248, X2_249, X_245, Y_246, X4_251, X8_270, X6_253, X5_252, X3_250, Z_247, X9_271]: (~in(U_203, X9_271, X_245) | ~be(U_203, X8_270, '#skF_36'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X9_271) | ~state(U_203, X8_270) | member(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | member(U_203, '#skF_39'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | ~cheap(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~black(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~coat(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~behind(U_203, X6_253, Y_246) | ~be(U_203, X5_252, V_243, X6_253) | ~state(U_203, X5_252) | ~group(U_203, X4_251) | ~group(U_203, X3_250) | ~two(U_203, X3_250) | ~in(U_203, X2_249, X1_248) | ~down(U_203, X2_249, X1_248) | ~barrel(U_203, X2_249) | ~present(U_203, X2_249) | ~agent(U_203, X2_249, Y_246) | ~event(U_203, X2_249) | ~lonely(U_203, X1_248) | ~street(U_203, X1_248) | ~placename(U_203, Z_247) | ~hollywood_placename(U_203, Z_247) | ~city(U_203, X1_248) | ~of(U_203, Z_247, X1_248) | ~old(U_203, Y_246) | ~dirty(U_203, Y_246) | ~white(U_203, Y_246) | ~chevy(U_203, Y_246) | ~frontseat(U_203, X_245) | ~wheel(U_203, Y_246) | ~forename(U_203, W_244) | ~jules_forename(U_203, W_244) | ~man(U_203, V_243) | ~of(U_203, W_244, V_243) | ~actual_world(U_203)))).
% 111.04/92.65 tff(c_15017, plain, (![V_243, W_244, U_203, X1_248, X2_249, X_245, Y_246, X4_251, X8_270, X6_253, X5_252, X3_250, Z_247, X13_276, X9_271]: (~in(U_203, X9_271, X_245) | ~be(U_203, X8_270, '#skF_36'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X9_271) | ~state(U_203, X8_270) | member(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | ~wear(U_203, X13_276) | ~nonreflexive(U_203, X13_276) | ~present(U_203, X13_276) | ~patient(U_203, X13_276, '#skF_38'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~agent(U_203, X13_276, '#skF_39'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~event(U_203, X13_276) | member(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X4_251) | ~behind(U_203, X6_253, Y_246) | ~be(U_203, X5_252, V_243, X6_253) | ~state(U_203, X5_252) | ~group(U_203, X4_251) | ~group(U_203, X3_250) | ~two(U_203, X3_250) | ~in(U_203, X2_249, X1_248) | ~down(U_203, X2_249, X1_248) | ~barrel(U_203, X2_249) | ~present(U_203, X2_249) | ~agent(U_203, X2_249, Y_246) | ~event(U_203, X2_249) | ~lonely(U_203, X1_248) | ~street(U_203, X1_248) | ~placename(U_203, Z_247) | ~hollywood_placename(U_203, Z_247) | ~city(U_203, X1_248) | ~of(U_203, Z_247, X1_248) | ~old(U_203, Y_246) | ~dirty(U_203, Y_246) | ~white(U_203, Y_246) | ~chevy(U_203, Y_246) | ~frontseat(U_203, X_245) | ~wheel(U_203, Y_246) | ~forename(U_203, W_244) | ~jules_forename(U_203, W_244) | ~man(U_203, V_243) | ~of(U_203, W_244, V_243) | ~actual_world(U_203)))).
% 111.04/92.65 tff(c_14689, plain, (![V_243, W_244, U_203, X1_248, X2_249, X_245, Y_246, X4_251, X6_253, X5_252, X3_250, Z_247]: (member(U_203, '#skF_36'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | member(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | member(U_203, '#skF_39'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | ~cheap(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~black(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~coat(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~behind(U_203, X6_253, Y_246) | ~be(U_203, X5_252, V_243, X6_253) | ~state(U_203, X5_252) | ~group(U_203, X4_251) | ~group(U_203, X3_250) | ~two(U_203, X3_250) | ~in(U_203, X2_249, X1_248) | ~down(U_203, X2_249, X1_248) | ~barrel(U_203, X2_249) | ~present(U_203, X2_249) | ~agent(U_203, X2_249, Y_246) | ~event(U_203, X2_249) | ~lonely(U_203, X1_248) | ~street(U_203, X1_248) | ~placename(U_203, Z_247) | ~hollywood_placename(U_203, Z_247) | ~city(U_203, X1_248) | ~of(U_203, Z_247, X1_248) | ~old(U_203, Y_246) | ~dirty(U_203, Y_246) | ~white(U_203, Y_246) | ~chevy(U_203, Y_246) | ~frontseat(U_203, X_245) | ~wheel(U_203, Y_246) | ~forename(U_203, W_244) | ~jules_forename(U_203, W_244) | ~man(U_203, V_243) | ~of(U_203, W_244, V_243) | ~actual_world(U_203)))).
% 111.04/92.65 tff(c_14471, plain, (![V_243, W_244, U_203, X1_248, X2_249, X_245, Y_246, X4_251, X6_253, X5_252, X3_250, Z_247]: (member(U_203, '#skF_36'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | member(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | member(U_203, '#skF_38'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X4_251) | ~cheap(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~black(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~coat(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~behind(U_203, X6_253, Y_246) | ~be(U_203, X5_252, V_243, X6_253) | ~state(U_203, X5_252) | ~group(U_203, X4_251) | ~group(U_203, X3_250) | ~two(U_203, X3_250) | ~in(U_203, X2_249, X1_248) | ~down(U_203, X2_249, X1_248) | ~barrel(U_203, X2_249) | ~present(U_203, X2_249) | ~agent(U_203, X2_249, Y_246) | ~event(U_203, X2_249) | ~lonely(U_203, X1_248) | ~street(U_203, X1_248) | ~placename(U_203, Z_247) | ~hollywood_placename(U_203, Z_247) | ~city(U_203, X1_248) | ~of(U_203, Z_247, X1_248) | ~old(U_203, Y_246) | ~dirty(U_203, Y_246) | ~white(U_203, Y_246) | ~chevy(U_203, Y_246) | ~frontseat(U_203, X_245) | ~wheel(U_203, Y_246) | ~forename(U_203, W_244) | ~jules_forename(U_203, W_244) | ~man(U_203, V_243) | ~of(U_203, W_244, V_243) | ~actual_world(U_203)))).
% 111.04/92.65 tff(c_14463, plain, (![V_243, W_244, U_203, X1_248, X2_249, X_245, Y_246, X4_251, X6_253, X5_252, X3_250, Z_247, X13_276]: (member(U_203, '#skF_36'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | member(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | ~wear(U_203, X13_276) | ~nonreflexive(U_203, X13_276) | ~present(U_203, X13_276) | ~patient(U_203, X13_276, '#skF_38'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~agent(U_203, X13_276, '#skF_39'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~event(U_203, X13_276) | member(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X4_251) | ~behind(U_203, X6_253, Y_246) | ~be(U_203, X5_252, V_243, X6_253) | ~state(U_203, X5_252) | ~group(U_203, X4_251) | ~group(U_203, X3_250) | ~two(U_203, X3_250) | ~in(U_203, X2_249, X1_248) | ~down(U_203, X2_249, X1_248) | ~barrel(U_203, X2_249) | ~present(U_203, X2_249) | ~agent(U_203, X2_249, Y_246) | ~event(U_203, X2_249) | ~lonely(U_203, X1_248) | ~street(U_203, X1_248) | ~placename(U_203, Z_247) | ~hollywood_placename(U_203, Z_247) | ~city(U_203, X1_248) | ~of(U_203, Z_247, X1_248) | ~old(U_203, Y_246) | ~dirty(U_203, Y_246) | ~white(U_203, Y_246) | ~chevy(U_203, Y_246) | ~frontseat(U_203, X_245) | ~wheel(U_203, Y_246) | ~forename(U_203, W_244) | ~jules_forename(U_203, W_244) | ~man(U_203, V_243) | ~of(U_203, W_244, V_243) | ~actual_world(U_203)))).
% 111.04/92.65 tff(c_13775, plain, (![V_243, W_244, U_203, X1_248, X2_249, X_245, Y_246, X4_251, X8_270, X6_253, X5_252, X3_250, Z_247, X9_271]: (~in(U_203, X9_271, X_245) | ~be(U_203, X8_270, '#skF_36'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X9_271) | ~state(U_203, X8_270) | ~young(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~fellow(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | member(U_203, '#skF_38'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X4_251) | member(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X4_251) | ~behind(U_203, X6_253, Y_246) | ~be(U_203, X5_252, V_243, X6_253) | ~state(U_203, X5_252) | ~group(U_203, X4_251) | ~group(U_203, X3_250) | ~two(U_203, X3_250) | ~in(U_203, X2_249, X1_248) | ~down(U_203, X2_249, X1_248) | ~barrel(U_203, X2_249) | ~present(U_203, X2_249) | ~agent(U_203, X2_249, Y_246) | ~event(U_203, X2_249) | ~lonely(U_203, X1_248) | ~street(U_203, X1_248) | ~placename(U_203, Z_247) | ~hollywood_placename(U_203, Z_247) | ~city(U_203, X1_248) | ~of(U_203, Z_247, X1_248) | ~old(U_203, Y_246) | ~dirty(U_203, Y_246) | ~white(U_203, Y_246) | ~chevy(U_203, Y_246) | ~frontseat(U_203, X_245) | ~wheel(U_203, Y_246) | ~forename(U_203, W_244) | ~jules_forename(U_203, W_244) | ~man(U_203, V_243) | ~of(U_203, W_244, V_243) | ~actual_world(U_203)))).
% 111.04/92.65 tff(c_13767, plain, (![V_243, W_244, U_203, X1_248, X2_249, X_245, Y_246, X4_251, X8_270, X6_253, X5_252, X3_250, Z_247, X9_271]: (~in(U_203, X9_271, X_245) | ~be(U_203, X8_270, '#skF_36'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X9_271) | ~state(U_203, X8_270) | ~young(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~fellow(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | member(U_203, '#skF_39'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | member(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X4_251) | ~behind(U_203, X6_253, Y_246) | ~be(U_203, X5_252, V_243, X6_253) | ~state(U_203, X5_252) | ~group(U_203, X4_251) | ~group(U_203, X3_250) | ~two(U_203, X3_250) | ~in(U_203, X2_249, X1_248) | ~down(U_203, X2_249, X1_248) | ~barrel(U_203, X2_249) | ~present(U_203, X2_249) | ~agent(U_203, X2_249, Y_246) | ~event(U_203, X2_249) | ~lonely(U_203, X1_248) | ~street(U_203, X1_248) | ~placename(U_203, Z_247) | ~hollywood_placename(U_203, Z_247) | ~city(U_203, X1_248) | ~of(U_203, Z_247, X1_248) | ~old(U_203, Y_246) | ~dirty(U_203, Y_246) | ~white(U_203, Y_246) | ~chevy(U_203, Y_246) | ~frontseat(U_203, X_245) | ~wheel(U_203, Y_246) | ~forename(U_203, W_244) | ~jules_forename(U_203, W_244) | ~man(U_203, V_243) | ~of(U_203, W_244, V_243) | ~actual_world(U_203)))).
% 111.04/92.65 tff(c_12864, plain, (![V_243, W_244, U_203, X1_248, X2_249, X_245, Y_246, X4_251, X6_253, X5_252, X3_250, Z_247]: (member(U_203, '#skF_36'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | ~young(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~fellow(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | member(U_203, '#skF_39'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | member(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X4_251) | ~behind(U_203, X6_253, Y_246) | ~be(U_203, X5_252, V_243, X6_253) | ~state(U_203, X5_252) | ~group(U_203, X4_251) | ~group(U_203, X3_250) | ~two(U_203, X3_250) | ~in(U_203, X2_249, X1_248) | ~down(U_203, X2_249, X1_248) | ~barrel(U_203, X2_249) | ~present(U_203, X2_249) | ~agent(U_203, X2_249, Y_246) | ~event(U_203, X2_249) | ~lonely(U_203, X1_248) | ~street(U_203, X1_248) | ~placename(U_203, Z_247) | ~hollywood_placename(U_203, Z_247) | ~city(U_203, X1_248) | ~of(U_203, Z_247, X1_248) | ~old(U_203, Y_246) | ~dirty(U_203, Y_246) | ~white(U_203, Y_246) | ~chevy(U_203, Y_246) | ~frontseat(U_203, X_245) | ~wheel(U_203, Y_246) | ~forename(U_203, W_244) | ~jules_forename(U_203, W_244) | ~man(U_203, V_243) | ~of(U_203, W_244, V_243) | ~actual_world(U_203)))).
% 111.04/92.65 tff(c_11984, plain, (![V_243, W_244, U_203, X1_248, X2_249, X_245, Y_246, X4_251, X6_253, X5_252, X3_250, Z_247]: (member(U_203, '#skF_36'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | ~young(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | ~fellow(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253)) | member(U_203, '#skF_38'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X4_251) | member(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X4_251) | ~behind(U_203, X6_253, Y_246) | ~be(U_203, X5_252, V_243, X6_253) | ~state(U_203, X5_252) | ~group(U_203, X4_251) | ~group(U_203, X3_250) | ~two(U_203, X3_250) | ~in(U_203, X2_249, X1_248) | ~down(U_203, X2_249, X1_248) | ~barrel(U_203, X2_249) | ~present(U_203, X2_249) | ~agent(U_203, X2_249, Y_246) | ~event(U_203, X2_249) | ~lonely(U_203, X1_248) | ~street(U_203, X1_248) | ~placename(U_203, Z_247) | ~hollywood_placename(U_203, Z_247) | ~city(U_203, X1_248) | ~of(U_203, Z_247, X1_248) | ~old(U_203, Y_246) | ~dirty(U_203, Y_246) | ~white(U_203, Y_246) | ~chevy(U_203, Y_246) | ~frontseat(U_203, X_245) | ~wheel(U_203, Y_246) | ~forename(U_203, W_244) | ~jules_forename(U_203, W_244) | ~man(U_203, V_243) | ~of(U_203, W_244, V_243) | ~actual_world(U_203)))).
% 111.04/92.65 tff(c_11860, plain, (![V_243, W_244, U_203, X1_248, X2_249, X_245, Y_246, X4_251, X8_270, X6_253, X5_252, X3_250, Z_247, X9_271]: (~in(U_203, X9_271, X_245) | ~be(U_203, X8_270, '#skF_36'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X9_271) | ~state(U_203, X8_270) | member(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | member(U_203, '#skF_38'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X4_251) | member(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X4_251) | ~behind(U_203, X6_253, Y_246) | ~be(U_203, X5_252, V_243, X6_253) | ~state(U_203, X5_252) | ~group(U_203, X4_251) | ~group(U_203, X3_250) | ~two(U_203, X3_250) | ~in(U_203, X2_249, X1_248) | ~down(U_203, X2_249, X1_248) | ~barrel(U_203, X2_249) | ~present(U_203, X2_249) | ~agent(U_203, X2_249, Y_246) | ~event(U_203, X2_249) | ~lonely(U_203, X1_248) | ~street(U_203, X1_248) | ~placename(U_203, Z_247) | ~hollywood_placename(U_203, Z_247) | ~city(U_203, X1_248) | ~of(U_203, Z_247, X1_248) | ~old(U_203, Y_246) | ~dirty(U_203, Y_246) | ~white(U_203, Y_246) | ~chevy(U_203, Y_246) | ~frontseat(U_203, X_245) | ~wheel(U_203, Y_246) | ~forename(U_203, W_244) | ~jules_forename(U_203, W_244) | ~man(U_203, V_243) | ~of(U_203, W_244, V_243) | ~actual_world(U_203)))).
% 111.04/92.65 tff(c_11852, plain, (![V_243, W_244, U_203, X1_248, X2_249, X_245, Y_246, X4_251, X8_270, X6_253, X5_252, X3_250, Z_247, X9_271]: (~in(U_203, X9_271, X_245) | ~be(U_203, X8_270, '#skF_36'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X9_271) | ~state(U_203, X8_270) | member(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | member(U_203, '#skF_39'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | member(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X4_251) | ~behind(U_203, X6_253, Y_246) | ~be(U_203, X5_252, V_243, X6_253) | ~state(U_203, X5_252) | ~group(U_203, X4_251) | ~group(U_203, X3_250) | ~two(U_203, X3_250) | ~in(U_203, X2_249, X1_248) | ~down(U_203, X2_249, X1_248) | ~barrel(U_203, X2_249) | ~present(U_203, X2_249) | ~agent(U_203, X2_249, Y_246) | ~event(U_203, X2_249) | ~lonely(U_203, X1_248) | ~street(U_203, X1_248) | ~placename(U_203, Z_247) | ~hollywood_placename(U_203, Z_247) | ~city(U_203, X1_248) | ~of(U_203, Z_247, X1_248) | ~old(U_203, Y_246) | ~dirty(U_203, Y_246) | ~white(U_203, Y_246) | ~chevy(U_203, Y_246) | ~frontseat(U_203, X_245) | ~wheel(U_203, Y_246) | ~forename(U_203, W_244) | ~jules_forename(U_203, W_244) | ~man(U_203, V_243) | ~of(U_203, W_244, V_243) | ~actual_world(U_203)))).
% 111.04/92.65 tff(c_11749, plain, (~two('#skF_21', '#skF_30'))).
% 111.04/92.66 tff(c_10912, plain, (![V_243, W_244, U_203, X1_248, X2_249, X_245, Y_246, X4_251, X6_253, X5_252, X3_250, Z_247]: (member(U_203, '#skF_36'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | member(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | member(U_203, '#skF_38'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X4_251) | member(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X4_251) | ~behind(U_203, X6_253, Y_246) | ~be(U_203, X5_252, V_243, X6_253) | ~state(U_203, X5_252) | ~group(U_203, X4_251) | ~group(U_203, X3_250) | ~two(U_203, X3_250) | ~in(U_203, X2_249, X1_248) | ~down(U_203, X2_249, X1_248) | ~barrel(U_203, X2_249) | ~present(U_203, X2_249) | ~agent(U_203, X2_249, Y_246) | ~event(U_203, X2_249) | ~lonely(U_203, X1_248) | ~street(U_203, X1_248) | ~placename(U_203, Z_247) | ~hollywood_placename(U_203, Z_247) | ~city(U_203, X1_248) | ~of(U_203, Z_247, X1_248) | ~old(U_203, Y_246) | ~dirty(U_203, Y_246) | ~white(U_203, Y_246) | ~chevy(U_203, Y_246) | ~frontseat(U_203, X_245) | ~wheel(U_203, Y_246) | ~forename(U_203, W_244) | ~jules_forename(U_203, W_244) | ~man(U_203, V_243) | ~of(U_203, W_244, V_243) | ~actual_world(U_203)))).
% 111.04/92.66 tff(c_10777, plain, (![V_243, W_244, U_203, X1_248, X2_249, X_245, Y_246, X4_251, X6_253, X5_252, X3_250, Z_247]: (member(U_203, '#skF_36'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | member(U_203, '#skF_37'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | member(U_203, '#skF_39'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X3_250) | member(U_203, '#skF_40'(X2_249, X_245, V_243, X1_248, X4_251, W_244, X3_250, Y_246, Z_247, X5_252, U_203, X6_253), X4_251) | ~behind(U_203, X6_253, Y_246) | ~be(U_203, X5_252, V_243, X6_253) | ~state(U_203, X5_252) | ~group(U_203, X4_251) | ~group(U_203, X3_250) | ~two(U_203, X3_250) | ~in(U_203, X2_249, X1_248) | ~down(U_203, X2_249, X1_248) | ~barrel(U_203, X2_249) | ~present(U_203, X2_249) | ~agent(U_203, X2_249, Y_246) | ~event(U_203, X2_249) | ~lonely(U_203, X1_248) | ~street(U_203, X1_248) | ~placename(U_203, Z_247) | ~hollywood_placename(U_203, Z_247) | ~city(U_203, X1_248) | ~of(U_203, Z_247, X1_248) | ~old(U_203, Y_246) | ~dirty(U_203, Y_246) | ~white(U_203, Y_246) | ~chevy(U_203, Y_246) | ~frontseat(U_203, X_245) | ~wheel(U_203, Y_246) | ~forename(U_203, W_244) | ~jules_forename(U_203, W_244) | ~man(U_203, V_243) | ~of(U_203, W_244, V_243) | ~actual_world(U_203)))).
% 111.04/92.66 tff(c_10659, plain, (![X31_196, X32_200]: (patient('#skF_21', '#skF_35'(X31_196, X32_200), X31_196) | ~member('#skF_21', X32_200, '#skF_29') | ~member('#skF_21', X31_196, '#skF_30')))).
% 111.04/92.66 tff(c_10656, plain, (![X31_196, X32_200]: (agent('#skF_21', '#skF_35'(X31_196, X32_200), X32_200) | ~member('#skF_21', X32_200, '#skF_29') | ~member('#skF_21', X31_196, '#skF_30')))).
% 111.04/92.66 tff(c_10654, plain, (![X31_196, X32_200]: (wear('#skF_21', '#skF_35'(X31_196, X32_200)) | ~member('#skF_21', X32_200, '#skF_29') | ~member('#skF_21', X31_196, '#skF_30')))).
% 111.04/92.66 tff(c_10652, plain, (![X31_196, X32_200]: (nonreflexive('#skF_21', '#skF_35'(X31_196, X32_200)) | ~member('#skF_21', X32_200, '#skF_29') | ~member('#skF_21', X31_196, '#skF_30')))).
% 111.04/92.66 tff(c_10650, plain, (![X31_196, X32_200]: (event('#skF_21', '#skF_35'(X31_196, X32_200)) | ~member('#skF_21', X32_200, '#skF_29') | ~member('#skF_21', X31_196, '#skF_30')))).
% 111.04/92.66 tff(c_10648, plain, (![X31_196, X32_200]: (present('#skF_21', '#skF_35'(X31_196, X32_200)) | ~member('#skF_21', X32_200, '#skF_29') | ~member('#skF_21', X31_196, '#skF_30')))).
% 111.04/92.66 tff(c_10616, plain, (![X27_192]: (be('#skF_21', '#skF_33'(X27_192), X27_192, '#skF_34'(X27_192)) | ~member('#skF_21', X27_192, '#skF_29')))).
% 111.04/92.66 tff(c_10368, plain, (![X27_192]: (in('#skF_21', '#skF_34'(X27_192), '#skF_24') | ~member('#skF_21', X27_192, '#skF_29')))).
% 111.04/92.66 tff(c_10290, plain, (![X27_192]: (state('#skF_21', '#skF_33'(X27_192)) | ~member('#skF_21', X27_192, '#skF_29')))).
% 111.04/92.66 tff(c_10244, plain, (![X34_202]: (cheap('#skF_21', X34_202) | ~member('#skF_21', X34_202, '#skF_30')))).
% 111.04/92.66 tff(c_10241, plain, (![X34_202]: (black('#skF_21', X34_202) | ~member('#skF_21', X34_202, '#skF_30')))).
% 111.04/92.66 tff(c_10236, plain, (![X30_195]: (fellow('#skF_21', X30_195) | ~member('#skF_21', X30_195, '#skF_29')))).
% 111.04/92.66 tff(c_10232, plain, (![X34_202]: (coat('#skF_21', X34_202) | ~member('#skF_21', X34_202, '#skF_30')))).
% 111.04/92.66 tff(c_10228, plain, (![X30_195]: (young('#skF_21', X30_195) | ~member('#skF_21', X30_195, '#skF_29')))).
% 111.04/92.66 tff(c_10149, plain, (be('#skF_1', '#skF_11', '#skF_2', '#skF_12'))).
% 111.04/92.66 tff(c_10067, plain, (of('#skF_1', '#skF_6', '#skF_7'))).
% 111.04/92.66 tff(c_10059, plain, (of('#skF_1', '#skF_3', '#skF_2'))).
% 111.04/92.66 tff(c_10056, plain, (down('#skF_1', '#skF_8', '#skF_7'))).
% 111.04/92.66 tff(c_10053, plain, (in('#skF_1', '#skF_8', '#skF_7'))).
% 111.04/92.66 tff(c_10050, plain, (agent('#skF_1', '#skF_8', '#skF_5'))).
% 111.04/92.66 tff(c_10045, plain, (behind('#skF_1', '#skF_12', '#skF_5'))).
% 111.04/92.66 tff(c_9887, plain, (wheel('#skF_1', '#skF_5'))).
% 111.04/92.66 tff(c_9886, plain, (white('#skF_1', '#skF_5'))).
% 111.04/92.66 tff(c_9881, plain, (jules_forename('#skF_1', '#skF_3'))).
% 111.04/92.66 tff(c_9879, plain, (chevy('#skF_1', '#skF_5'))).
% 111.04/92.66 tff(c_9876, plain, (man('#skF_1', '#skF_2'))).
% 111.04/92.66 tff(c_9874, plain, (forename('#skF_1', '#skF_3'))).
% 111.04/92.66 tff(c_9872, plain, (city('#skF_1', '#skF_7'))).
% 111.04/92.66 tff(c_9869, plain, (frontseat('#skF_1', '#skF_4'))).
% 111.04/92.66 tff(c_9866, plain, (dirty('#skF_1', '#skF_5'))).
% 111.04/92.66 tff(c_9865, plain, (old('#skF_1', '#skF_5'))).
% 111.04/92.66 tff(c_9861, plain, (hollywood_placename('#skF_1', '#skF_6'))).
% 111.04/92.66 tff(c_9860, plain, (lonely('#skF_1', '#skF_7'))).
% 111.04/92.66 tff(c_9857, plain, (placename('#skF_1', '#skF_6'))).
% 111.04/92.66 tff(c_9856, plain, (street('#skF_1', '#skF_7'))).
% 111.04/92.66 tff(c_9854, plain, (event('#skF_1', '#skF_8'))).
% 111.04/92.66 tff(c_9853, plain, (barrel('#skF_1', '#skF_8'))).
% 111.04/92.66 tff(c_9852, plain, (present('#skF_1', '#skF_8'))).
% 111.04/92.66 tff(c_9846, plain, (two('#skF_1', '#skF_9'))).
% 111.04/92.66 tff(c_9845, plain, (group('#skF_1', '#skF_10'))).
% 111.04/92.66 tff(c_9843, plain, (state('#skF_1', '#skF_11'))).
% 111.04/92.66 tff(c_9841, plain, (group('#skF_1', '#skF_9'))).
% 111.04/92.66 tff(c_9807, plain, (actual_world('#skF_1'))).
% 111.04/92.66 tff(c_9636, plain, (be('#skF_21', '#skF_31', '#skF_22', '#skF_32'))).
% 111.04/92.66 tff(c_9329, plain, (behind('#skF_21', '#skF_32', '#skF_27'))).
% 111.04/92.66 tff(c_9301, plain, (agent('#skF_21', '#skF_28', '#skF_25'))).
% 111.04/92.66 tff(c_9292, plain, (down('#skF_21', '#skF_28', '#skF_27'))).
% 111.04/92.66 tff(c_9177, plain, (in('#skF_21', '#skF_28', '#skF_27'))).
% 111.04/92.66 tff(c_9162, plain, (of('#skF_21', '#skF_26', '#skF_27'))).
% 111.04/92.66 tff(c_9102, plain, (of('#skF_21', '#skF_23', '#skF_22'))).
% 111.04/92.66 tff(c_9015, plain, (old('#skF_21', '#skF_25'))).
% 111.04/92.66 tff(c_9014, plain, (state('#skF_21', '#skF_31'))).
% 111.04/92.66 tff(c_9013, plain, (wheel('#skF_21', '#skF_27'))).
% 111.04/92.66 tff(c_9010, plain, (man('#skF_21', '#skF_22'))).
% 111.04/92.66 tff(c_9003, plain, (city('#skF_21', '#skF_27'))).
% 111.04/92.66 tff(c_9002, plain, (frontseat('#skF_21', '#skF_24'))).
% 111.04/92.66 tff(c_9000, plain, (present('#skF_21', '#skF_28'))).
% 111.04/92.66 tff(c_8998, plain, (two('#skF_21', '#skF_29'))).
% 111.04/92.66 tff(c_8997, plain, (jules_forename('#skF_21', '#skF_23'))).
% 111.04/92.66 tff(c_8995, plain, (dirty('#skF_21', '#skF_25'))).
% 111.04/92.66 tff(c_8994, plain, (event('#skF_21', '#skF_28'))).
% 111.04/92.66 tff(c_8993, plain, (group('#skF_21', '#skF_30'))).
% 111.04/92.66 tff(c_8992, plain, (barrel('#skF_21', '#skF_28'))).
% 111.04/92.66 tff(c_8991, plain, (group('#skF_21', '#skF_29'))).
% 111.04/92.66 tff(c_8990, plain, (hollywood_placename('#skF_21', '#skF_26'))).
% 111.04/92.66 tff(c_8989, plain, (placename('#skF_21', '#skF_26'))).
% 111.04/92.66 tff(c_8988, plain, (forename('#skF_21', '#skF_23'))).
% 111.04/92.66 tff(c_8987, plain, (white('#skF_21', '#skF_25'))).
% 111.04/92.66 tff(c_8986, plain, (lonely('#skF_21', '#skF_27'))).
% 111.04/92.66 tff(c_8984, plain, (chevy('#skF_21', '#skF_25'))).
% 111.04/92.66 tff(c_8983, plain, (street('#skF_21', '#skF_27'))).
% 111.04/92.66 tff(c_8979, plain, (actual_world('#skF_21'))).
% 111.04/92.66 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 111.04/92.66
%------------------------------------------------------------------------------