%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : NLP135+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 : n018.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:21 PM UTC 2025
% Result : CounterSatisfiable 13.52s 4.47s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.10/0.11 % Problem : NLP135+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/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.11/0.31 % Computer : n018.cluster.edu
% 0.11/0.31 % Model : x86_64 x86_64
% 0.11/0.31 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.31 % Memory : 8042.1875MB
% 0.11/0.31 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.31 % CPULimit : 300
% 0.11/0.31 % WCLimit : 300
% 0.11/0.31 % DateTime : Tue Apr 8 08:43:17 EDT 2025
% 0.16/0.31 % CPUTime :
% 13.52/4.47
% 13.52/4.47 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.52/4.47
% 13.52/4.47 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.80/4.48 %$ 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_7 > #skF_9 > #skF_18 > #skF_11 > #skF_15 > #skF_8 > #skF_19 > #skF_16 > #skF_14 > #skF_5 > #skF_6 > #skF_13 > #skF_2 > #skF_3 > #skF_1 > #skF_4 > #skF_17 > #skF_20 > #skF_12
% 13.80/4.48
% 13.80/4.48 %Foreground sorts:
% 13.80/4.48
% 13.80/4.48
% 13.80/4.48 %Background operators:
% 13.80/4.48
% 13.80/4.48
% 13.80/4.48 %Foreground operators:
% 13.80/4.48 tff('#skF_10', type, '#skF_10': ($i * $i * $i * $i * $i * $i) > $i).
% 13.80/4.48 tff(two, type, two: ($i * $i) > $o).
% 13.80/4.48 tff('#skF_7', type, '#skF_7': $i > $i).
% 13.80/4.48 tff(frontseat, type, frontseat: ($i * $i) > $o).
% 13.80/4.48 tff(placename, type, placename: ($i * $i) > $o).
% 13.80/4.48 tff(member, type, member: ($i * $i * $i) > $o).
% 13.80/4.48 tff(be, type, be: ($i * $i * $i * $i) > $o).
% 13.80/4.48 tff('#skF_9', type, '#skF_9': ($i * $i * $i * $i * $i * $i) > $i).
% 13.80/4.48 tff(present, type, present: ($i * $i) > $o).
% 13.80/4.48 tff('#skF_18', type, '#skF_18': $i > $i).
% 13.80/4.48 tff(in, type, in: ($i * $i * $i) > $o).
% 13.80/4.48 tff(old, type, old: ($i * $i) > $o).
% 13.80/4.48 tff(dirty, type, dirty: ($i * $i) > $o).
% 13.80/4.48 tff('#skF_11', type, '#skF_11': $i).
% 13.80/4.48 tff('#skF_15', type, '#skF_15': $i).
% 13.80/4.48 tff(city, type, city: ($i * $i) > $o).
% 13.80/4.48 tff(young, type, young: ($i * $i) > $o).
% 13.80/4.48 tff('#skF_8', type, '#skF_8': $i > $i).
% 13.80/4.48 tff(of, type, of: ($i * $i * $i) > $o).
% 13.80/4.48 tff('#skF_19', type, '#skF_19': ($i * $i * $i * $i * $i * $i) > $i).
% 13.80/4.48 tff(actual_world, type, actual_world: $i > $o).
% 13.80/4.48 tff(agent, type, agent: ($i * $i * $i) > $o).
% 13.80/4.48 tff('#skF_16', type, '#skF_16': $i).
% 13.80/4.48 tff('#skF_14', type, '#skF_14': $i).
% 13.80/4.48 tff('#skF_5', type, '#skF_5': $i).
% 13.80/4.48 tff(group, type, group: ($i * $i) > $o).
% 13.80/4.48 tff(lonely, type, lonely: ($i * $i) > $o).
% 13.80/4.48 tff(fellow, type, fellow: ($i * $i) > $o).
% 13.80/4.48 tff('#skF_6', type, '#skF_6': $i).
% 13.80/4.48 tff('#skF_13', type, '#skF_13': $i).
% 13.80/4.48 tff('#skF_2', type, '#skF_2': $i).
% 13.80/4.48 tff('#skF_3', type, '#skF_3': $i).
% 13.80/4.48 tff(event, type, event: ($i * $i) > $o).
% 13.80/4.48 tff('#skF_1', type, '#skF_1': $i).
% 13.80/4.48 tff(down, type, down: ($i * $i * $i) > $o).
% 13.80/4.48 tff(hollywood_placename, type, hollywood_placename: ($i * $i) > $o).
% 13.80/4.48 tff(white, type, white: ($i * $i) > $o).
% 13.80/4.48 tff(barrel, type, barrel: ($i * $i) > $o).
% 13.80/4.48 tff(state, type, state: ($i * $i) > $o).
% 13.80/4.48 tff(street, type, street: ($i * $i) > $o).
% 13.80/4.48 tff('#skF_4', type, '#skF_4': $i).
% 13.80/4.48 tff('#skF_17', type, '#skF_17': $i > $i).
% 13.80/4.48 tff(chevy, type, chevy: ($i * $i) > $o).
% 13.80/4.48 tff('#skF_20', type, '#skF_20': ($i * $i * $i * $i * $i * $i) > $i).
% 13.80/4.48 tff('#skF_12', type, '#skF_12': $i).
% 13.80/4.48
% 13.80/4.48 %Saturated clause set:
% 13.80/4.49 tff(c_2569, plain, (![X_108, X3_120, Y_109, W_107, X2_119, V_106, Z_110, U_88]: (~in(U_88, X3_120, X3_120) | ~be(U_88, X2_119, '#skF_19'(W_107, Y_109, Z_110, X_108, U_88, V_106), X3_120) | ~state(U_88, X2_119) | ~frontseat(U_88, X3_120) | ~young(U_88, '#skF_20'(W_107, Y_109, Z_110, X_108, U_88, V_106)) | ~fellow(U_88, '#skF_20'(W_107, Y_109, Z_110, X_108, U_88, V_106)) | ~group(U_88, Z_110) | ~two(U_88, Z_110) | ~in(U_88, Y_109, W_107) | ~down(U_88, Y_109, X_108) | ~barrel(U_88, Y_109) | ~present(U_88, Y_109) | ~agent(U_88, Y_109, W_107) | ~event(U_88, Y_109) | ~lonely(U_88, X_108) | ~street(U_88, X_108) | ~old(U_88, W_107) | ~dirty(U_88, W_107) | ~white(U_88, W_107) | ~chevy(U_88, W_107) | ~placename(U_88, V_106) | ~hollywood_placename(U_88, V_106) | ~city(U_88, W_107) | ~of(U_88, V_106, W_107) | ~actual_world(U_88)))).
% 13.80/4.49 tff(c_2527, plain, (![X_108, X3_120, Y_109, W_107, X2_119, V_106, Z_110, U_88]: (~in(U_88, X3_120, X3_120) | ~be(U_88, X2_119, '#skF_19'(W_107, Y_109, Z_110, X_108, U_88, V_106), X3_120) | ~state(U_88, X2_119) | ~frontseat(U_88, X3_120) | member(U_88, '#skF_20'(W_107, Y_109, Z_110, X_108, U_88, V_106), Z_110) | ~group(U_88, Z_110) | ~two(U_88, Z_110) | ~in(U_88, Y_109, W_107) | ~down(U_88, Y_109, X_108) | ~barrel(U_88, Y_109) | ~present(U_88, Y_109) | ~agent(U_88, Y_109, W_107) | ~event(U_88, Y_109) | ~lonely(U_88, X_108) | ~street(U_88, X_108) | ~old(U_88, W_107) | ~dirty(U_88, W_107) | ~white(U_88, W_107) | ~chevy(U_88, W_107) | ~placename(U_88, V_106) | ~hollywood_placename(U_88, V_106) | ~city(U_88, W_107) | ~of(U_88, V_106, W_107) | ~actual_world(U_88)))).
% 13.80/4.49 tff(c_2500, plain, (![W_156, Y_157, X_159, V_161]: (young('#skF_11', '#skF_19'(W_156, Y_157, '#skF_16', X_159, '#skF_11', V_161)) | ~young('#skF_11', '#skF_20'(W_156, Y_157, '#skF_16', X_159, '#skF_11', V_161)) | ~fellow('#skF_11', '#skF_20'(W_156, Y_157, '#skF_16', X_159, '#skF_11', V_161)) | ~in('#skF_11', Y_157, W_156) | ~down('#skF_11', Y_157, X_159) | ~barrel('#skF_11', Y_157) | ~present('#skF_11', Y_157) | ~agent('#skF_11', Y_157, W_156) | ~event('#skF_11', Y_157) | ~lonely('#skF_11', X_159) | ~street('#skF_11', X_159) | ~old('#skF_11', W_156) | ~dirty('#skF_11', W_156) | ~white('#skF_11', W_156) | ~chevy('#skF_11', W_156) | ~placename('#skF_11', V_161) | ~hollywood_placename('#skF_11', V_161) | ~city('#skF_11', W_156) | ~of('#skF_11', V_161, W_156)))).
% 13.80/4.49 tff(c_2505, plain, (![W_132, Y_133, X_134, V_135]: (~fellow('#skF_11', '#skF_20'(W_132, Y_133, '#skF_16', X_134, '#skF_11', V_135)) | fellow('#skF_11', '#skF_19'(W_132, Y_133, '#skF_16', X_134, '#skF_11', V_135)) | ~in('#skF_11', Y_133, W_132) | ~down('#skF_11', Y_133, X_134) | ~barrel('#skF_11', Y_133) | ~present('#skF_11', Y_133) | ~agent('#skF_11', Y_133, W_132) | ~event('#skF_11', Y_133) | ~lonely('#skF_11', X_134) | ~street('#skF_11', X_134) | ~old('#skF_11', W_132) | ~dirty('#skF_11', W_132) | ~white('#skF_11', W_132) | ~chevy('#skF_11', W_132) | ~placename('#skF_11', V_135) | ~hollywood_placename('#skF_11', V_135) | ~city('#skF_11', W_132) | ~of('#skF_11', V_135, W_132)))).
% 13.80/4.49 tff(c_2485, plain, (![X_108, Y_109, W_107, V_106, Z_110, U_88]: (member(U_88, '#skF_19'(W_107, Y_109, Z_110, X_108, U_88, V_106), Z_110) | ~young(U_88, '#skF_20'(W_107, Y_109, Z_110, X_108, U_88, V_106)) | ~fellow(U_88, '#skF_20'(W_107, Y_109, Z_110, X_108, U_88, V_106)) | ~group(U_88, Z_110) | ~two(U_88, Z_110) | ~in(U_88, Y_109, W_107) | ~down(U_88, Y_109, X_108) | ~barrel(U_88, Y_109) | ~present(U_88, Y_109) | ~agent(U_88, Y_109, W_107) | ~event(U_88, Y_109) | ~lonely(U_88, X_108) | ~street(U_88, X_108) | ~old(U_88, W_107) | ~dirty(U_88, W_107) | ~white(U_88, W_107) | ~chevy(U_88, W_107) | ~placename(U_88, V_106) | ~hollywood_placename(U_88, V_106) | ~city(U_88, W_107) | ~of(U_88, V_106, W_107) | ~actual_world(U_88)))).
% 13.80/4.49 tff(c_2409, plain, (![W_144, Y_145, X_146, V_147]: (fellow('#skF_11', '#skF_20'(W_144, Y_145, '#skF_16', X_146, '#skF_11', V_147)) | young('#skF_11', '#skF_19'(W_144, Y_145, '#skF_16', X_146, '#skF_11', V_147)) | ~in('#skF_11', Y_145, W_144) | ~down('#skF_11', Y_145, X_146) | ~barrel('#skF_11', Y_145) | ~present('#skF_11', Y_145) | ~agent('#skF_11', Y_145, W_144) | ~event('#skF_11', Y_145) | ~lonely('#skF_11', X_146) | ~street('#skF_11', X_146) | ~old('#skF_11', W_144) | ~dirty('#skF_11', W_144) | ~white('#skF_11', W_144) | ~chevy('#skF_11', W_144) | ~placename('#skF_11', V_147) | ~hollywood_placename('#skF_11', V_147) | ~city('#skF_11', W_144) | ~of('#skF_11', V_147, W_144)))).
% 13.80/4.50 tff(c_2410, plain, (![W_144, Y_145, X_146, V_147]: (young('#skF_11', '#skF_20'(W_144, Y_145, '#skF_16', X_146, '#skF_11', V_147)) | young('#skF_11', '#skF_19'(W_144, Y_145, '#skF_16', X_146, '#skF_11', V_147)) | ~in('#skF_11', Y_145, W_144) | ~down('#skF_11', Y_145, X_146) | ~barrel('#skF_11', Y_145) | ~present('#skF_11', Y_145) | ~agent('#skF_11', Y_145, W_144) | ~event('#skF_11', Y_145) | ~lonely('#skF_11', X_146) | ~street('#skF_11', X_146) | ~old('#skF_11', W_144) | ~dirty('#skF_11', W_144) | ~white('#skF_11', W_144) | ~chevy('#skF_11', W_144) | ~placename('#skF_11', V_147) | ~hollywood_placename('#skF_11', V_147) | ~city('#skF_11', W_144) | ~of('#skF_11', V_147, W_144)))).
% 13.80/4.50 tff(c_2390, plain, (![W_126, Y_127, X_129, V_131]: (young('#skF_11', '#skF_19'(W_126, Y_127, '#skF_16', X_129, '#skF_11', V_131)) | member('#skF_11', '#skF_20'(W_126, Y_127, '#skF_16', X_129, '#skF_11', V_131), '#skF_16') | ~in('#skF_11', Y_127, W_126) | ~down('#skF_11', Y_127, X_129) | ~barrel('#skF_11', Y_127) | ~present('#skF_11', Y_127) | ~agent('#skF_11', Y_127, W_126) | ~event('#skF_11', Y_127) | ~lonely('#skF_11', X_129) | ~street('#skF_11', X_129) | ~old('#skF_11', W_126) | ~dirty('#skF_11', W_126) | ~white('#skF_11', W_126) | ~chevy('#skF_11', W_126) | ~placename('#skF_11', V_131) | ~hollywood_placename('#skF_11', V_131) | ~city('#skF_11', W_126) | ~of('#skF_11', V_131, W_126)))).
% 13.80/4.50 tff(c_2399, plain, (![W_132, Y_133, X_134, V_135]: (young('#skF_11', '#skF_20'(W_132, Y_133, '#skF_16', X_134, '#skF_11', V_135)) | fellow('#skF_11', '#skF_19'(W_132, Y_133, '#skF_16', X_134, '#skF_11', V_135)) | ~in('#skF_11', Y_133, W_132) | ~down('#skF_11', Y_133, X_134) | ~barrel('#skF_11', Y_133) | ~present('#skF_11', Y_133) | ~agent('#skF_11', Y_133, W_132) | ~event('#skF_11', Y_133) | ~lonely('#skF_11', X_134) | ~street('#skF_11', X_134) | ~old('#skF_11', W_132) | ~dirty('#skF_11', W_132) | ~white('#skF_11', W_132) | ~chevy('#skF_11', W_132) | ~placename('#skF_11', V_135) | ~hollywood_placename('#skF_11', V_135) | ~city('#skF_11', W_132) | ~of('#skF_11', V_135, W_132)))).
% 13.80/4.50 tff(c_2398, plain, (![W_132, Y_133, X_134, V_135]: (fellow('#skF_11', '#skF_20'(W_132, Y_133, '#skF_16', X_134, '#skF_11', V_135)) | fellow('#skF_11', '#skF_19'(W_132, Y_133, '#skF_16', X_134, '#skF_11', V_135)) | ~in('#skF_11', Y_133, W_132) | ~down('#skF_11', Y_133, X_134) | ~barrel('#skF_11', Y_133) | ~present('#skF_11', Y_133) | ~agent('#skF_11', Y_133, W_132) | ~event('#skF_11', Y_133) | ~lonely('#skF_11', X_134) | ~street('#skF_11', X_134) | ~old('#skF_11', W_132) | ~dirty('#skF_11', W_132) | ~white('#skF_11', W_132) | ~chevy('#skF_11', W_132) | ~placename('#skF_11', V_135) | ~hollywood_placename('#skF_11', V_135) | ~city('#skF_11', W_132) | ~of('#skF_11', V_135, W_132)))).
% 13.80/4.50 tff(c_2387, plain, (![W_126, Y_127, X_129, V_131]: (fellow('#skF_11', '#skF_19'(W_126, Y_127, '#skF_16', X_129, '#skF_11', V_131)) | member('#skF_11', '#skF_20'(W_126, Y_127, '#skF_16', X_129, '#skF_11', V_131), '#skF_16') | ~in('#skF_11', Y_127, W_126) | ~down('#skF_11', Y_127, X_129) | ~barrel('#skF_11', Y_127) | ~present('#skF_11', Y_127) | ~agent('#skF_11', Y_127, W_126) | ~event('#skF_11', Y_127) | ~lonely('#skF_11', X_129) | ~street('#skF_11', X_129) | ~old('#skF_11', W_126) | ~dirty('#skF_11', W_126) | ~white('#skF_11', W_126) | ~chevy('#skF_11', W_126) | ~placename('#skF_11', V_131) | ~hollywood_placename('#skF_11', V_131) | ~city('#skF_11', W_126) | ~of('#skF_11', V_131, W_126)))).
% 13.80/4.50 tff(c_2375, plain, (![X_108, Y_109, W_107, V_106, Z_110, U_88]: (member(U_88, '#skF_19'(W_107, Y_109, Z_110, X_108, U_88, V_106), Z_110) | member(U_88, '#skF_20'(W_107, Y_109, Z_110, X_108, U_88, V_106), Z_110) | ~group(U_88, Z_110) | ~two(U_88, Z_110) | ~in(U_88, Y_109, W_107) | ~down(U_88, Y_109, X_108) | ~barrel(U_88, Y_109) | ~present(U_88, Y_109) | ~agent(U_88, Y_109, W_107) | ~event(U_88, Y_109) | ~lonely(U_88, X_108) | ~street(U_88, X_108) | ~old(U_88, W_107) | ~dirty(U_88, W_107) | ~white(U_88, W_107) | ~chevy(U_88, W_107) | ~placename(U_88, V_106) | ~hollywood_placename(U_88, V_106) | ~city(U_88, W_107) | ~of(U_88, V_106, W_107) | ~actual_world(U_88)))).
% 13.80/4.50 tff(c_2316, plain, (![X11_84]: (be('#skF_11', '#skF_17'(X11_84), X11_84, '#skF_18'(X11_84)) | ~member('#skF_11', X11_84, '#skF_16') | ~frontseat('#skF_11', X11_84)))).
% 13.80/4.50 tff(c_2314, plain, (![X11_84]: (in('#skF_11', '#skF_18'(X11_84), X11_84) | ~member('#skF_11', X11_84, '#skF_16') | ~frontseat('#skF_11', X11_84)))).
% 13.80/4.50 tff(c_2309, plain, (![X11_84]: (state('#skF_11', '#skF_17'(X11_84)) | ~member('#skF_11', X11_84, '#skF_16') | ~frontseat('#skF_11', X11_84)))).
% 13.80/4.50 tff(c_2247, plain, (![X14_87]: (fellow('#skF_11', X14_87) | ~member('#skF_11', X14_87, '#skF_16')))).
% 13.80/4.50 tff(c_2236, plain, (![X14_87]: (young('#skF_11', X14_87) | ~member('#skF_11', X14_87, '#skF_16')))).
% 13.80/4.50 tff(c_2194, plain, (down('#skF_1', '#skF_5', '#skF_4'))).
% 13.80/4.50 tff(c_2170, plain, (agent('#skF_1', '#skF_5', '#skF_3'))).
% 13.80/4.50 tff(c_2167, plain, (in('#skF_1', '#skF_5', '#skF_3'))).
% 13.80/4.50 tff(c_2163, plain, (of('#skF_1', '#skF_2', '#skF_3'))).
% 13.80/4.50 tff(c_2153, plain, (barrel('#skF_1', '#skF_5'))).
% 13.80/4.50 tff(c_2152, plain, (city('#skF_1', '#skF_3'))).
% 13.80/4.50 tff(c_2150, plain, (event('#skF_1', '#skF_5'))).
% 13.80/4.50 tff(c_2147, plain, (street('#skF_1', '#skF_4'))).
% 13.80/4.50 tff(c_2145, plain, (present('#skF_1', '#skF_5'))).
% 13.80/4.50 tff(c_2143, plain, (chevy('#skF_1', '#skF_3'))).
% 13.80/4.50 tff(c_2139, plain, (dirty('#skF_1', '#skF_3'))).
% 13.80/4.50 tff(c_2134, plain, (hollywood_placename('#skF_1', '#skF_2'))).
% 13.80/4.50 tff(c_2131, plain, (lonely('#skF_1', '#skF_4'))).
% 13.80/4.50 tff(c_2120, plain, (old('#skF_1', '#skF_3'))).
% 13.80/4.50 tff(c_2115, plain, (white('#skF_1', '#skF_3'))).
% 13.80/4.50 tff(c_2113, plain, (placename('#skF_1', '#skF_2'))).
% 13.80/4.50 tff(c_2107, plain, (group('#skF_1', '#skF_6'))).
% 13.80/4.50 tff(c_2106, plain, (two('#skF_1', '#skF_6'))).
% 13.80/4.50 tff(c_2098, plain, (actual_world('#skF_1'))).
% 13.80/4.50 tff(c_1964, plain, (of('#skF_11', '#skF_12', '#skF_13'))).
% 13.80/4.50 tff(c_1936, plain, (agent('#skF_11', '#skF_15', '#skF_13'))).
% 13.80/4.50 tff(c_1788, plain, (down('#skF_11', '#skF_15', '#skF_14'))).
% 13.80/4.50 tff(c_1769, plain, (in('#skF_11', '#skF_15', '#skF_13'))).
% 13.80/4.50 tff(c_1765, plain, (white('#skF_11', '#skF_13'))).
% 13.80/4.50 tff(c_1761, plain, (hollywood_placename('#skF_11', '#skF_12'))).
% 13.80/4.50 tff(c_1760, plain, (lonely('#skF_11', '#skF_14'))).
% 13.80/4.50 tff(c_1759, plain, (present('#skF_11', '#skF_15'))).
% 13.80/4.50 tff(c_1758, plain, (group('#skF_11', '#skF_16'))).
% 13.80/4.50 tff(c_1757, plain, (old('#skF_11', '#skF_13'))).
% 13.80/4.50 tff(c_1755, plain, (chevy('#skF_11', '#skF_13'))).
% 13.80/4.50 tff(c_1752, plain, (two('#skF_11', '#skF_16'))).
% 13.80/4.50 tff(c_1749, plain, (event('#skF_11', '#skF_15'))).
% 13.80/4.50 tff(c_1747, plain, (barrel('#skF_11', '#skF_15'))).
% 13.80/4.51 tff(c_1745, plain, (street('#skF_11', '#skF_14'))).
% 13.80/4.51 tff(c_1744, plain, (city('#skF_11', '#skF_13'))).
% 13.80/4.51 tff(c_1742, plain, (dirty('#skF_11', '#skF_13'))).
% 13.80/4.51 tff(c_1739, plain, (placename('#skF_11', '#skF_12'))).
% 13.80/4.51 tff(c_1737, plain, (actual_world('#skF_11'))).
% 13.80/4.51 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 13.80/4.51
%------------------------------------------------------------------------------