%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : NLP137+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 : n011.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:22 PM UTC 2025
% Result : CounterSatisfiable 10.81s 3.89s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : NLP137+1 : TPTP v9.0.0. Released v2.4.0.
% 0.06/0.13 % 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.13/0.34 % Computer : n011.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 08:43:48 EDT 2025
% 0.13/0.34 % CPUTime :
% 10.81/3.89
% 10.81/3.89 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.81/3.89
% 10.81/3.89 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.81/3.90 %$ be > of > member > in > down > agent > young > white > two > street > state > present > placename > old > lonely > hollywood_placename > group > frontseat > fellow > event > dirty > city > chevy > barrel > actual_world > #nlpp > #skF_10 > #skF_9 > #skF_21 > #skF_18 > #skF_17 > #skF_15 > #skF_19 > #skF_8 > #skF_7 > #skF_11 > #skF_16 > #skF_14 > #skF_5 > #skF_6 > #skF_13 > #skF_2 > #skF_3 > #skF_1 > #skF_4 > #skF_12 > #skF_20
% 10.81/3.90
% 10.81/3.90 %Foreground sorts:
% 10.81/3.90
% 10.81/3.90
% 10.81/3.90 %Background operators:
% 10.81/3.90
% 10.81/3.90
% 10.81/3.90 %Foreground operators:
% 10.81/3.90 tff('#skF_10', type, '#skF_10': ($i * $i * $i * $i * $i * $i) > $i).
% 10.81/3.90 tff('#skF_9', type, '#skF_9': $i > $i).
% 10.81/3.90 tff(two, type, two: ($i * $i) > $o).
% 10.81/3.90 tff(frontseat, type, frontseat: ($i * $i) > $o).
% 10.81/3.90 tff(placename, type, placename: ($i * $i) > $o).
% 10.81/3.90 tff(member, type, member: ($i * $i * $i) > $o).
% 10.81/3.90 tff(be, type, be: ($i * $i * $i * $i) > $o).
% 10.81/3.90 tff('#skF_21', type, '#skF_21': ($i * $i * $i * $i * $i * $i * $i) > $i).
% 10.81/3.90 tff(present, type, present: ($i * $i) > $o).
% 10.81/3.90 tff('#skF_18', type, '#skF_18': $i > $i).
% 10.81/3.90 tff(in, type, in: ($i * $i * $i) > $o).
% 10.81/3.90 tff('#skF_17', type, '#skF_17': $i).
% 10.81/3.90 tff(old, type, old: ($i * $i) > $o).
% 10.81/3.90 tff(dirty, type, dirty: ($i * $i) > $o).
% 10.81/3.90 tff('#skF_15', type, '#skF_15': $i).
% 10.81/3.90 tff('#skF_19', type, '#skF_19': $i > $i).
% 10.81/3.90 tff(city, type, city: ($i * $i) > $o).
% 10.81/3.90 tff(young, type, young: ($i * $i) > $o).
% 10.81/3.90 tff('#skF_8', type, '#skF_8': $i > $i).
% 10.81/3.90 tff(of, type, of: ($i * $i * $i) > $o).
% 10.81/3.90 tff('#skF_7', type, '#skF_7': $i).
% 10.81/3.90 tff('#skF_11', type, '#skF_11': ($i * $i * $i * $i * $i * $i) > $i).
% 10.81/3.90 tff(actual_world, type, actual_world: $i > $o).
% 10.81/3.90 tff(agent, type, agent: ($i * $i * $i) > $o).
% 10.81/3.90 tff('#skF_16', type, '#skF_16': $i).
% 10.81/3.90 tff('#skF_14', type, '#skF_14': $i).
% 10.81/3.90 tff('#skF_5', type, '#skF_5': $i).
% 10.81/3.90 tff(group, type, group: ($i * $i) > $o).
% 10.81/3.90 tff(lonely, type, lonely: ($i * $i) > $o).
% 10.81/3.90 tff(fellow, type, fellow: ($i * $i) > $o).
% 10.81/3.90 tff('#skF_6', type, '#skF_6': $i).
% 10.81/3.90 tff('#skF_13', type, '#skF_13': $i).
% 10.81/3.90 tff('#skF_2', type, '#skF_2': $i).
% 10.81/3.90 tff('#skF_3', type, '#skF_3': $i).
% 10.81/3.90 tff(event, type, event: ($i * $i) > $o).
% 10.81/3.90 tff('#skF_1', type, '#skF_1': $i).
% 10.81/3.90 tff(down, type, down: ($i * $i * $i) > $o).
% 10.81/3.90 tff(hollywood_placename, type, hollywood_placename: ($i * $i) > $o).
% 10.81/3.90 tff(white, type, white: ($i * $i) > $o).
% 10.81/3.90 tff(barrel, type, barrel: ($i * $i) > $o).
% 10.81/3.90 tff(state, type, state: ($i * $i) > $o).
% 10.81/3.90 tff(street, type, street: ($i * $i) > $o).
% 10.81/3.90 tff('#skF_4', type, '#skF_4': $i).
% 10.81/3.90 tff(chevy, type, chevy: ($i * $i) > $o).
% 10.81/3.90 tff('#skF_12', type, '#skF_12': $i).
% 10.81/3.90 tff('#skF_20', type, '#skF_20': ($i * $i * $i * $i * $i * $i * $i) > $i).
% 10.81/3.90
% 10.81/3.90 %Saturated clause set:
% 10.81/3.90 tff(c_2652, plain, (![X1_245, X_247, W_249, Z_250, Y_244, V_248]: (~in('#skF_12', '#skF_19'('#skF_20'('#skF_12', Y_244, X1_245, X_247, V_248, W_249, Z_250)), '#skF_20'('#skF_12', Y_244, X1_245, X_247, V_248, W_249, Z_250)) | ~state('#skF_12', '#skF_18'('#skF_20'('#skF_12', Y_244, X1_245, X_247, V_248, W_249, Z_250))) | ~young('#skF_12', '#skF_21'('#skF_12', Y_244, X1_245, X_247, V_248, W_249, Z_250)) | ~fellow('#skF_12', '#skF_21'('#skF_12', Y_244, X1_245, X_247, V_248, W_249, Z_250)) | ~group('#skF_12', X1_245) | ~two('#skF_12', X1_245) | ~in('#skF_12', Z_250, V_248) | ~down('#skF_12', Z_250, Y_244) | ~barrel('#skF_12', Z_250) | ~present('#skF_12', Z_250) | ~agent('#skF_12', Z_250, X_247) | ~event('#skF_12', Z_250) | ~lonely('#skF_12', Y_244) | ~street('#skF_12', Y_244) | ~old('#skF_12', X_247) | ~dirty('#skF_12', X_247) | ~white('#skF_12', X_247) | ~chevy('#skF_12', X_247) | ~placename('#skF_12', W_249) | ~hollywood_placename('#skF_12', W_249) | ~city('#skF_12', V_248) | ~of('#skF_12', W_249, V_248) | ~member('#skF_12', '#skF_20'('#skF_12', Y_244, X1_245, X_247, V_248, W_249, Z_250), '#skF_17')))).
% 10.81/3.90 tff(c_2644, plain, (![V_108, W_109, Z_112, U_89, X_110, Y_111, X4_123, X3_122, X1_113]: (~in(U_89, X4_123, '#skF_20'(U_89, Y_111, X1_113, X_110, V_108, W_109, Z_112)) | ~be(U_89, X3_122, '#skF_20'(U_89, Y_111, X1_113, X_110, V_108, W_109, Z_112), X4_123) | ~state(U_89, X3_122) | ~young(U_89, '#skF_21'(U_89, Y_111, X1_113, X_110, V_108, W_109, Z_112)) | ~fellow(U_89, '#skF_21'(U_89, Y_111, X1_113, X_110, V_108, W_109, Z_112)) | ~group(U_89, X1_113) | ~two(U_89, X1_113) | ~in(U_89, Z_112, V_108) | ~down(U_89, Z_112, Y_111) | ~barrel(U_89, Z_112) | ~present(U_89, Z_112) | ~agent(U_89, Z_112, X_110) | ~event(U_89, Z_112) | ~lonely(U_89, Y_111) | ~street(U_89, Y_111) | ~old(U_89, X_110) | ~dirty(U_89, X_110) | ~white(U_89, X_110) | ~chevy(U_89, X_110) | ~placename(U_89, W_109) | ~hollywood_placename(U_89, W_109) | ~city(U_89, V_108) | ~of(U_89, W_109, V_108) | ~actual_world(U_89)))).
% 10.81/3.90 tff(c_2623, plain, (![X_232, Z_235, X1_230, Y_229, V_233, W_234]: (~in('#skF_12', '#skF_19'('#skF_20'('#skF_12', Y_229, X1_230, X_232, V_233, W_234, Z_235)), '#skF_20'('#skF_12', Y_229, X1_230, X_232, V_233, W_234, Z_235)) | ~state('#skF_12', '#skF_18'('#skF_20'('#skF_12', Y_229, X1_230, X_232, V_233, W_234, Z_235))) | member('#skF_12', '#skF_21'('#skF_12', Y_229, X1_230, X_232, V_233, W_234, Z_235), X1_230) | ~group('#skF_12', X1_230) | ~two('#skF_12', X1_230) | ~in('#skF_12', Z_235, V_233) | ~down('#skF_12', Z_235, Y_229) | ~barrel('#skF_12', Z_235) | ~present('#skF_12', Z_235) | ~agent('#skF_12', Z_235, X_232) | ~event('#skF_12', Z_235) | ~lonely('#skF_12', Y_229) | ~street('#skF_12', Y_229) | ~old('#skF_12', X_232) | ~dirty('#skF_12', X_232) | ~white('#skF_12', X_232) | ~chevy('#skF_12', X_232) | ~placename('#skF_12', W_234) | ~hollywood_placename('#skF_12', W_234) | ~city('#skF_12', V_233) | ~of('#skF_12', W_234, V_233) | ~member('#skF_12', '#skF_20'('#skF_12', Y_229, X1_230, X_232, V_233, W_234, Z_235), '#skF_17')))).
% 10.81/3.90 tff(c_2616, plain, (![V_108, W_109, Z_112, U_89, X_110, Y_111, X4_123, X3_122, X1_113]: (~in(U_89, X4_123, '#skF_20'(U_89, Y_111, X1_113, X_110, V_108, W_109, Z_112)) | ~be(U_89, X3_122, '#skF_20'(U_89, Y_111, X1_113, X_110, V_108, W_109, Z_112), X4_123) | ~state(U_89, X3_122) | member(U_89, '#skF_21'(U_89, Y_111, X1_113, X_110, V_108, W_109, Z_112), X1_113) | ~group(U_89, X1_113) | ~two(U_89, X1_113) | ~in(U_89, Z_112, V_108) | ~down(U_89, Z_112, Y_111) | ~barrel(U_89, Z_112) | ~present(U_89, Z_112) | ~agent(U_89, Z_112, X_110) | ~event(U_89, Z_112) | ~lonely(U_89, Y_111) | ~street(U_89, Y_111) | ~old(U_89, X_110) | ~dirty(U_89, X_110) | ~white(U_89, X_110) | ~chevy(U_89, X_110) | ~placename(U_89, W_109) | ~hollywood_placename(U_89, W_109) | ~city(U_89, V_108) | ~of(U_89, W_109, V_108) | ~actual_world(U_89)))).
% 10.81/3.90 tff(c_2576, plain, (![X_170, Y_169, V_172, W_171, Z_173]: (fellow('#skF_12', '#skF_20'('#skF_12', Y_169, '#skF_17', X_170, V_172, W_171, Z_173)) | ~in('#skF_12', Z_173, V_172) | ~down('#skF_12', Z_173, Y_169) | ~barrel('#skF_12', Z_173) | ~present('#skF_12', Z_173) | ~agent('#skF_12', Z_173, X_170) | ~event('#skF_12', Z_173) | ~lonely('#skF_12', Y_169) | ~street('#skF_12', Y_169) | ~old('#skF_12', X_170) | ~dirty('#skF_12', X_170) | ~white('#skF_12', X_170) | ~chevy('#skF_12', X_170) | ~placename('#skF_12', W_171) | ~hollywood_placename('#skF_12', W_171) | ~city('#skF_12', V_172) | ~of('#skF_12', W_171, V_172)))).
% 10.81/3.90 tff(c_2556, plain, (![X_155, W_156, Z_158, Y_154, V_157]: (~fellow('#skF_12', '#skF_21'('#skF_12', Y_154, '#skF_17', X_155, V_157, W_156, Z_158)) | young('#skF_12', '#skF_20'('#skF_12', Y_154, '#skF_17', X_155, V_157, W_156, Z_158)) | ~in('#skF_12', Z_158, V_157) | ~down('#skF_12', Z_158, Y_154) | ~barrel('#skF_12', Z_158) | ~present('#skF_12', Z_158) | ~agent('#skF_12', Z_158, X_155) | ~event('#skF_12', Z_158) | ~lonely('#skF_12', Y_154) | ~street('#skF_12', Y_154) | ~old('#skF_12', X_155) | ~dirty('#skF_12', X_155) | ~white('#skF_12', X_155) | ~chevy('#skF_12', X_155) | ~placename('#skF_12', W_156) | ~hollywood_placename('#skF_12', W_156) | ~city('#skF_12', V_157) | ~of('#skF_12', W_156, V_157)))).
% 10.81/3.90 tff(c_2529, plain, (![V_108, W_109, Z_112, U_89, X_110, Y_111, X1_113]: (member(U_89, '#skF_20'(U_89, Y_111, X1_113, X_110, V_108, W_109, Z_112), X1_113) | ~young(U_89, '#skF_21'(U_89, Y_111, X1_113, X_110, V_108, W_109, Z_112)) | ~fellow(U_89, '#skF_21'(U_89, Y_111, X1_113, X_110, V_108, W_109, Z_112)) | ~group(U_89, X1_113) | ~two(U_89, X1_113) | ~in(U_89, Z_112, V_108) | ~down(U_89, Z_112, Y_111) | ~barrel(U_89, Z_112) | ~present(U_89, Z_112) | ~agent(U_89, Z_112, X_110) | ~event(U_89, Z_112) | ~lonely(U_89, Y_111) | ~street(U_89, Y_111) | ~old(U_89, X_110) | ~dirty(U_89, X_110) | ~white(U_89, X_110) | ~chevy(U_89, X_110) | ~placename(U_89, W_109) | ~hollywood_placename(U_89, W_109) | ~city(U_89, V_108) | ~of(U_89, W_109, V_108) | ~actual_world(U_89)))).
% 10.81/3.90 tff(c_2527, plain, (![Y_131, X_133, V_134, W_135, Z_136]: (~fellow('#skF_12', '#skF_21'('#skF_12', Y_131, '#skF_17', X_133, V_134, W_135, Z_136)) | frontseat('#skF_12', '#skF_20'('#skF_12', Y_131, '#skF_17', X_133, V_134, W_135, Z_136)) | ~in('#skF_12', Z_136, V_134) | ~down('#skF_12', Z_136, Y_131) | ~barrel('#skF_12', Z_136) | ~present('#skF_12', Z_136) | ~agent('#skF_12', Z_136, X_133) | ~event('#skF_12', Z_136) | ~lonely('#skF_12', Y_131) | ~street('#skF_12', Y_131) | ~old('#skF_12', X_133) | ~dirty('#skF_12', X_133) | ~white('#skF_12', X_133) | ~chevy('#skF_12', X_133) | ~placename('#skF_12', W_135) | ~hollywood_placename('#skF_12', W_135) | ~city('#skF_12', V_134) | ~of('#skF_12', W_135, V_134)))).
% 10.81/3.91 tff(c_2508, plain, (![V_108, W_109, Z_112, U_89, X_110, Y_111, X1_113]: (frontseat(U_89, '#skF_20'(U_89, Y_111, X1_113, X_110, V_108, W_109, Z_112)) | ~young(U_89, '#skF_21'(U_89, Y_111, X1_113, X_110, V_108, W_109, Z_112)) | ~fellow(U_89, '#skF_21'(U_89, Y_111, X1_113, X_110, V_108, W_109, Z_112)) | ~group(U_89, X1_113) | ~two(U_89, X1_113) | ~in(U_89, Z_112, V_108) | ~down(U_89, Z_112, Y_111) | ~barrel(U_89, Z_112) | ~present(U_89, Z_112) | ~agent(U_89, Z_112, X_110) | ~event(U_89, Z_112) | ~lonely(U_89, Y_111) | ~street(U_89, Y_111) | ~old(U_89, X_110) | ~dirty(U_89, X_110) | ~white(U_89, X_110) | ~chevy(U_89, X_110) | ~placename(U_89, W_109) | ~hollywood_placename(U_89, W_109) | ~city(U_89, V_108) | ~of(U_89, W_109, V_108) | ~actual_world(U_89)))).
% 10.81/3.91 tff(c_2428, plain, (![X_170, Y_169, V_172, W_171, Z_173]: (young('#skF_12', '#skF_20'('#skF_12', Y_169, '#skF_17', X_170, V_172, W_171, Z_173)) | fellow('#skF_12', '#skF_21'('#skF_12', Y_169, '#skF_17', X_170, V_172, W_171, Z_173)) | ~in('#skF_12', Z_173, V_172) | ~down('#skF_12', Z_173, Y_169) | ~barrel('#skF_12', Z_173) | ~present('#skF_12', Z_173) | ~agent('#skF_12', Z_173, X_170) | ~event('#skF_12', Z_173) | ~lonely('#skF_12', Y_169) | ~street('#skF_12', Y_169) | ~old('#skF_12', X_170) | ~dirty('#skF_12', X_170) | ~white('#skF_12', X_170) | ~chevy('#skF_12', X_170) | ~placename('#skF_12', W_171) | ~hollywood_placename('#skF_12', W_171) | ~city('#skF_12', V_172) | ~of('#skF_12', W_171, V_172)))).
% 10.81/3.91 tff(c_2409, plain, (![V_151, Y_148, Z_153, W_152, X_150]: (fellow('#skF_12', '#skF_21'('#skF_12', Y_148, '#skF_17', X_150, V_151, W_152, Z_153)) | member('#skF_12', '#skF_20'('#skF_12', Y_148, '#skF_17', X_150, V_151, W_152, Z_153), '#skF_17') | ~in('#skF_12', Z_153, V_151) | ~down('#skF_12', Z_153, Y_148) | ~barrel('#skF_12', Z_153) | ~present('#skF_12', Z_153) | ~agent('#skF_12', Z_153, X_150) | ~event('#skF_12', Z_153) | ~lonely('#skF_12', Y_148) | ~street('#skF_12', Y_148) | ~old('#skF_12', X_150) | ~dirty('#skF_12', X_150) | ~white('#skF_12', X_150) | ~chevy('#skF_12', X_150) | ~placename('#skF_12', W_152) | ~hollywood_placename('#skF_12', W_152) | ~city('#skF_12', V_151) | ~of('#skF_12', W_152, V_151)))).
% 10.81/3.91 tff(c_2417, plain, (![X_155, W_156, Z_158, Y_154, V_157]: (young('#skF_12', '#skF_20'('#skF_12', Y_154, '#skF_17', X_155, V_157, W_156, Z_158)) | young('#skF_12', '#skF_21'('#skF_12', Y_154, '#skF_17', X_155, V_157, W_156, Z_158)) | ~in('#skF_12', Z_158, V_157) | ~down('#skF_12', Z_158, Y_154) | ~barrel('#skF_12', Z_158) | ~present('#skF_12', Z_158) | ~agent('#skF_12', Z_158, X_155) | ~event('#skF_12', Z_158) | ~lonely('#skF_12', Y_154) | ~street('#skF_12', Y_154) | ~old('#skF_12', X_155) | ~dirty('#skF_12', X_155) | ~white('#skF_12', X_155) | ~chevy('#skF_12', X_155) | ~placename('#skF_12', W_156) | ~hollywood_placename('#skF_12', W_156) | ~city('#skF_12', V_157) | ~of('#skF_12', W_156, V_157)))).
% 10.81/3.91 tff(c_2406, plain, (![V_151, Y_148, Z_153, W_152, X_150]: (young('#skF_12', '#skF_21'('#skF_12', Y_148, '#skF_17', X_150, V_151, W_152, Z_153)) | member('#skF_12', '#skF_20'('#skF_12', Y_148, '#skF_17', X_150, V_151, W_152, Z_153), '#skF_17') | ~in('#skF_12', Z_153, V_151) | ~down('#skF_12', Z_153, Y_148) | ~barrel('#skF_12', Z_153) | ~present('#skF_12', Z_153) | ~agent('#skF_12', Z_153, X_150) | ~event('#skF_12', Z_153) | ~lonely('#skF_12', Y_148) | ~street('#skF_12', Y_148) | ~old('#skF_12', X_150) | ~dirty('#skF_12', X_150) | ~white('#skF_12', X_150) | ~chevy('#skF_12', X_150) | ~placename('#skF_12', W_152) | ~hollywood_placename('#skF_12', W_152) | ~city('#skF_12', V_151) | ~of('#skF_12', W_152, V_151)))).
% 10.81/3.91 tff(c_2394, plain, (![V_108, W_109, Z_112, U_89, X_110, Y_111, X1_113]: (member(U_89, '#skF_20'(U_89, Y_111, X1_113, X_110, V_108, W_109, Z_112), X1_113) | member(U_89, '#skF_21'(U_89, Y_111, X1_113, X_110, V_108, W_109, Z_112), X1_113) | ~group(U_89, X1_113) | ~two(U_89, X1_113) | ~in(U_89, Z_112, V_108) | ~down(U_89, Z_112, Y_111) | ~barrel(U_89, Z_112) | ~present(U_89, Z_112) | ~agent(U_89, Z_112, X_110) | ~event(U_89, Z_112) | ~lonely(U_89, Y_111) | ~street(U_89, Y_111) | ~old(U_89, X_110) | ~dirty(U_89, X_110) | ~white(U_89, X_110) | ~chevy(U_89, X_110) | ~placename(U_89, W_109) | ~hollywood_placename(U_89, W_109) | ~city(U_89, V_108) | ~of(U_89, W_109, V_108) | ~actual_world(U_89)))).
% 10.81/3.91 tff(c_2391, plain, (![Y_131, X_133, V_134, W_135, Z_136]: (fellow('#skF_12', '#skF_21'('#skF_12', Y_131, '#skF_17', X_133, V_134, W_135, Z_136)) | frontseat('#skF_12', '#skF_20'('#skF_12', Y_131, '#skF_17', X_133, V_134, W_135, Z_136)) | ~in('#skF_12', Z_136, V_134) | ~down('#skF_12', Z_136, Y_131) | ~barrel('#skF_12', Z_136) | ~present('#skF_12', Z_136) | ~agent('#skF_12', Z_136, X_133) | ~event('#skF_12', Z_136) | ~lonely('#skF_12', Y_131) | ~street('#skF_12', Y_131) | ~old('#skF_12', X_133) | ~dirty('#skF_12', X_133) | ~white('#skF_12', X_133) | ~chevy('#skF_12', X_133) | ~placename('#skF_12', W_135) | ~hollywood_placename('#skF_12', W_135) | ~city('#skF_12', V_134) | ~of('#skF_12', W_135, V_134)))).
% 10.81/3.91 tff(c_2388, plain, (![Y_131, X_133, V_134, W_135, Z_136]: (young('#skF_12', '#skF_21'('#skF_12', Y_131, '#skF_17', X_133, V_134, W_135, Z_136)) | frontseat('#skF_12', '#skF_20'('#skF_12', Y_131, '#skF_17', X_133, V_134, W_135, Z_136)) | ~in('#skF_12', Z_136, V_134) | ~down('#skF_12', Z_136, Y_131) | ~barrel('#skF_12', Z_136) | ~present('#skF_12', Z_136) | ~agent('#skF_12', Z_136, X_133) | ~event('#skF_12', Z_136) | ~lonely('#skF_12', Y_131) | ~street('#skF_12', Y_131) | ~old('#skF_12', X_133) | ~dirty('#skF_12', X_133) | ~white('#skF_12', X_133) | ~chevy('#skF_12', X_133) | ~placename('#skF_12', W_135) | ~hollywood_placename('#skF_12', W_135) | ~city('#skF_12', V_134) | ~of('#skF_12', W_135, V_134)))).
% 10.81/3.91 tff(c_2376, plain, (![V_108, W_109, Z_112, U_89, X_110, Y_111, X1_113]: (frontseat(U_89, '#skF_20'(U_89, Y_111, X1_113, X_110, V_108, W_109, Z_112)) | member(U_89, '#skF_21'(U_89, Y_111, X1_113, X_110, V_108, W_109, Z_112), X1_113) | ~group(U_89, X1_113) | ~two(U_89, X1_113) | ~in(U_89, Z_112, V_108) | ~down(U_89, Z_112, Y_111) | ~barrel(U_89, Z_112) | ~present(U_89, Z_112) | ~agent(U_89, Z_112, X_110) | ~event(U_89, Z_112) | ~lonely(U_89, Y_111) | ~street(U_89, Y_111) | ~old(U_89, X_110) | ~dirty(U_89, X_110) | ~white(U_89, X_110) | ~chevy(U_89, X_110) | ~placename(U_89, W_109) | ~hollywood_placename(U_89, W_109) | ~city(U_89, V_108) | ~of(U_89, W_109, V_108) | ~actual_world(U_89)))).
% 10.81/3.91 tff(c_2316, plain, (![X12_85]: (be('#skF_12', '#skF_18'(X12_85), X12_85, '#skF_19'(X12_85)) | ~member('#skF_12', X12_85, '#skF_17')))).
% 10.81/3.91 tff(c_2302, plain, (![X12_85]: (in('#skF_12', '#skF_19'(X12_85), '#skF_19'(X12_85)) | ~member('#skF_12', X12_85, '#skF_17')))).
% 10.81/3.91 tff(c_2281, plain, (![X12_85]: (frontseat('#skF_12', '#skF_19'(X12_85)) | ~member('#skF_12', X12_85, '#skF_17')))).
% 10.81/3.91 tff(c_2272, plain, (![X12_85]: (state('#skF_12', '#skF_18'(X12_85)) | ~member('#skF_12', X12_85, '#skF_17')))).
% 10.81/3.91 tff(c_2248, plain, (![X15_88]: (young('#skF_12', X15_88) | ~member('#skF_12', X15_88, '#skF_17')))).
% 10.81/3.91 tff(c_2233, plain, (![X15_88]: (fellow('#skF_12', X15_88) | ~member('#skF_12', X15_88, '#skF_17')))).
% 10.81/3.91 tff(c_2184, plain, (down('#skF_1', '#skF_6', '#skF_5'))).
% 10.81/3.91 tff(c_2181, plain, (of('#skF_1', '#skF_3', '#skF_2'))).
% 10.81/3.91 tff(c_2171, plain, (in('#skF_1', '#skF_6', '#skF_2'))).
% 10.81/3.91 tff(c_2170, plain, (agent('#skF_1', '#skF_6', '#skF_4'))).
% 10.81/3.91 tff(c_2146, plain, (white('#skF_1', '#skF_4'))).
% 10.81/3.91 tff(c_2138, plain, (hollywood_placename('#skF_1', '#skF_3'))).
% 10.81/3.91 tff(c_2137, plain, (city('#skF_1', '#skF_2'))).
% 10.81/3.91 tff(c_2136, plain, (old('#skF_1', '#skF_4'))).
% 10.81/3.91 tff(c_2133, plain, (group('#skF_1', '#skF_7'))).
% 10.81/3.91 tff(c_2132, plain, (barrel('#skF_1', '#skF_6'))).
% 10.81/3.91 tff(c_2130, plain, (placename('#skF_1', '#skF_3'))).
% 10.81/3.91 tff(c_2129, plain, (present('#skF_1', '#skF_6'))).
% 10.81/3.91 tff(c_2128, plain, (dirty('#skF_1', '#skF_4'))).
% 10.81/3.91 tff(c_2127, plain, (lonely('#skF_1', '#skF_5'))).
% 10.81/3.91 tff(c_2124, plain, (event('#skF_1', '#skF_6'))).
% 10.81/3.91 tff(c_2123, plain, (two('#skF_1', '#skF_7'))).
% 10.81/3.91 tff(c_2118, plain, (street('#skF_1', '#skF_5'))).
% 10.81/3.91 tff(c_2116, plain, (chevy('#skF_1', '#skF_4'))).
% 10.81/3.91 tff(c_2098, plain, (actual_world('#skF_1'))).
% 10.81/3.91 tff(c_1934, plain, (agent('#skF_12', '#skF_16', '#skF_13'))).
% 10.81/3.91 tff(c_1842, plain, (down('#skF_12', '#skF_16', '#skF_15'))).
% 10.81/3.91 tff(c_1836, plain, (of('#skF_12', '#skF_14', '#skF_15'))).
% 10.81/3.91 tff(c_1815, plain, (in('#skF_12', '#skF_16', '#skF_15'))).
% 10.81/3.91 tff(c_1763, plain, (dirty('#skF_12', '#skF_13'))).
% 10.81/3.91 tff(c_1761, plain, (barrel('#skF_12', '#skF_16'))).
% 10.81/3.91 tff(c_1760, plain, (hollywood_placename('#skF_12', '#skF_14'))).
% 10.81/3.91 tff(c_1755, plain, (street('#skF_12', '#skF_15'))).
% 10.81/3.91 tff(c_1753, plain, (present('#skF_12', '#skF_16'))).
% 10.81/3.91 tff(c_1752, plain, (chevy('#skF_12', '#skF_13'))).
% 10.81/3.91 tff(c_1751, plain, (group('#skF_12', '#skF_17'))).
% 10.81/3.91 tff(c_1749, plain, (event('#skF_12', '#skF_16'))).
% 10.81/3.91 tff(c_1748, plain, (city('#skF_12', '#skF_15'))).
% 10.81/3.91 tff(c_1745, plain, (placename('#skF_12', '#skF_14'))).
% 10.81/3.91 tff(c_1744, plain, (lonely('#skF_12', '#skF_15'))).
% 10.81/3.91 tff(c_1743, plain, (two('#skF_12', '#skF_17'))).
% 10.81/3.91 tff(c_1741, plain, (old('#skF_12', '#skF_13'))).
% 10.81/3.91 tff(c_1739, plain, (white('#skF_12', '#skF_13'))).
% 10.81/3.91 tff(c_1737, plain, (actual_world('#skF_12'))).
% 10.81/3.91 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.81/3.91
%------------------------------------------------------------------------------