%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : NLP131+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 : n008.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:20 PM UTC 2025
% Result : CounterSatisfiable 12.15s 4.24s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.12/0.12 % Problem : NLP131+1 : TPTP v9.0.0. Released v2.4.0.
% 0.12/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.14/0.34 % Computer : n008.cluster.edu
% 0.14/0.34 % Model : x86_64 x86_64
% 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.34 % Memory : 8042.1875MB
% 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.14/0.34 % CPULimit : 300
% 0.14/0.34 % WCLimit : 300
% 0.14/0.34 % DateTime : Tue Apr 8 08:42:02 EDT 2025
% 0.20/0.34 % CPUTime :
% 12.15/4.24
% 12.15/4.24 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.15/4.24
% 12.15/4.24 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.15/4.25 %$ 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
% 12.15/4.25
% 12.15/4.25 %Foreground sorts:
% 12.15/4.25
% 12.15/4.25
% 12.15/4.25 %Background operators:
% 12.15/4.25
% 12.15/4.25
% 12.15/4.25 %Foreground operators:
% 12.15/4.25 tff('#skF_10', type, '#skF_10': ($i * $i * $i * $i * $i * $i) > $i).
% 12.15/4.25 tff(two, type, two: ($i * $i) > $o).
% 12.15/4.25 tff('#skF_7', type, '#skF_7': $i > $i).
% 12.15/4.25 tff(frontseat, type, frontseat: ($i * $i) > $o).
% 12.15/4.25 tff(placename, type, placename: ($i * $i) > $o).
% 12.15/4.25 tff(member, type, member: ($i * $i * $i) > $o).
% 12.15/4.25 tff(be, type, be: ($i * $i * $i * $i) > $o).
% 12.15/4.25 tff('#skF_9', type, '#skF_9': ($i * $i * $i * $i * $i * $i) > $i).
% 12.15/4.25 tff(present, type, present: ($i * $i) > $o).
% 12.15/4.25 tff('#skF_18', type, '#skF_18': $i > $i).
% 12.15/4.25 tff(in, type, in: ($i * $i * $i) > $o).
% 12.15/4.25 tff(old, type, old: ($i * $i) > $o).
% 12.15/4.25 tff(dirty, type, dirty: ($i * $i) > $o).
% 12.15/4.25 tff('#skF_11', type, '#skF_11': $i).
% 12.15/4.25 tff('#skF_15', type, '#skF_15': $i).
% 12.15/4.25 tff(city, type, city: ($i * $i) > $o).
% 12.15/4.25 tff(young, type, young: ($i * $i) > $o).
% 12.15/4.25 tff('#skF_8', type, '#skF_8': $i > $i).
% 12.15/4.25 tff(of, type, of: ($i * $i * $i) > $o).
% 12.15/4.25 tff('#skF_19', type, '#skF_19': ($i * $i * $i * $i * $i * $i) > $i).
% 12.15/4.25 tff(actual_world, type, actual_world: $i > $o).
% 12.15/4.25 tff(agent, type, agent: ($i * $i * $i) > $o).
% 12.15/4.25 tff('#skF_16', type, '#skF_16': $i).
% 12.15/4.25 tff('#skF_14', type, '#skF_14': $i).
% 12.15/4.25 tff('#skF_5', type, '#skF_5': $i).
% 12.15/4.25 tff(group, type, group: ($i * $i) > $o).
% 12.15/4.25 tff(lonely, type, lonely: ($i * $i) > $o).
% 12.15/4.25 tff(fellow, type, fellow: ($i * $i) > $o).
% 12.15/4.25 tff('#skF_6', type, '#skF_6': $i).
% 12.15/4.25 tff('#skF_13', type, '#skF_13': $i).
% 12.15/4.25 tff('#skF_2', type, '#skF_2': $i).
% 12.15/4.25 tff('#skF_3', type, '#skF_3': $i).
% 12.15/4.25 tff(event, type, event: ($i * $i) > $o).
% 12.15/4.25 tff('#skF_1', type, '#skF_1': $i).
% 12.15/4.25 tff(down, type, down: ($i * $i * $i) > $o).
% 12.15/4.25 tff(hollywood_placename, type, hollywood_placename: ($i * $i) > $o).
% 12.15/4.25 tff(white, type, white: ($i * $i) > $o).
% 12.15/4.25 tff(barrel, type, barrel: ($i * $i) > $o).
% 12.15/4.25 tff(state, type, state: ($i * $i) > $o).
% 12.15/4.25 tff(street, type, street: ($i * $i) > $o).
% 12.15/4.25 tff('#skF_4', type, '#skF_4': $i).
% 12.15/4.25 tff('#skF_17', type, '#skF_17': $i > $i).
% 12.15/4.25 tff(chevy, type, chevy: ($i * $i) > $o).
% 12.15/4.25 tff('#skF_20', type, '#skF_20': ($i * $i * $i * $i * $i * $i) > $i).
% 12.15/4.25 tff('#skF_12', type, '#skF_12': $i).
% 12.15/4.25
% 12.15/4.25 %Saturated clause set:
% 12.15/4.25 tff(c_2807, plain, (![X11_84, X_274, V_275]: (~down('#skF_11', '#skF_18'(X11_84), X_274) | ~barrel('#skF_11', '#skF_18'(X11_84)) | ~present('#skF_11', '#skF_18'(X11_84)) | ~agent('#skF_11', '#skF_18'(X11_84), X11_84) | ~event('#skF_11', '#skF_18'(X11_84)) | ~lonely('#skF_11', X_274) | ~street('#skF_11', X_274) | ~old('#skF_11', X11_84) | ~dirty('#skF_11', X11_84) | ~white('#skF_11', X11_84) | ~chevy('#skF_11', X11_84) | ~placename('#skF_11', V_275) | ~hollywood_placename('#skF_11', V_275) | ~city('#skF_11', X11_84) | ~of('#skF_11', V_275, X11_84) | ~member('#skF_11', X11_84, '#skF_16') | ~frontseat('#skF_11', X11_84)))).
% 12.15/4.25 tff(c_2811, plain, (~chevy('#skF_11', '#skF_14'))).
% 12.15/4.25 tff(c_2801, plain, (![Y_127, W_126, X_129, V_131]: (~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)))).
% 12.15/4.26 tff(c_2696, plain, (![X_108, X3_120, Y_109, W_107, X2_119, V_106, Z_110, U_88]: (~in(U_88, X3_120, '#skF_19'(W_107, Y_109, Z_110, X_108, U_88, V_106)) | ~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) | ~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)))).
% 12.15/4.26 tff(c_2650, plain, (![X_108, X3_120, Y_109, W_107, X2_119, V_106, Z_110, U_88]: (~in(U_88, X3_120, '#skF_19'(W_107, Y_109, Z_110, X_108, U_88, V_106)) | ~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) | 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)))).
% 12.15/4.26 tff(c_2585, 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)))).
% 12.15/4.26 tff(c_2570, plain, (![X_108, Y_109, W_107, V_106, Z_110, U_88]: (frontseat(U_88, '#skF_19'(W_107, Y_109, Z_110, X_108, U_88, V_106)) | ~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)))).
% 12.15/4.26 tff(c_2456, 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)))).
% 12.15/4.26 tff(c_2438, plain, (![X_108, Y_109, W_107, V_106, Z_110, U_88]: (frontseat(U_88, '#skF_19'(W_107, Y_109, Z_110, X_108, U_88, V_106)) | 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)))).
% 12.15/4.26 tff(c_2360, 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)))).
% 12.15/4.26 tff(c_2358, plain, (![X11_84]: (in('#skF_11', '#skF_18'(X11_84), X11_84) | ~member('#skF_11', X11_84, '#skF_16') | ~frontseat('#skF_11', X11_84)))).
% 12.15/4.26 tff(c_2351, plain, (![X11_84]: (state('#skF_11', '#skF_17'(X11_84)) | ~member('#skF_11', X11_84, '#skF_16') | ~frontseat('#skF_11', X11_84)))).
% 12.15/4.26 tff(c_2257, plain, (![X14_87]: (young('#skF_11', X14_87) | ~member('#skF_11', X14_87, '#skF_16')))).
% 12.15/4.26 tff(c_2243, plain, (![X14_87]: (fellow('#skF_11', X14_87) | ~member('#skF_11', X14_87, '#skF_16')))).
% 12.15/4.26 tff(c_2232, plain, (agent('#skF_1', '#skF_5', '#skF_3'))).
% 12.15/4.26 tff(c_2228, plain, (in('#skF_1', '#skF_5', '#skF_3'))).
% 12.15/4.26 tff(c_2226, plain, (of('#skF_1', '#skF_2', '#skF_3'))).
% 12.15/4.26 tff(c_2225, plain, (down('#skF_1', '#skF_5', '#skF_4'))).
% 12.15/4.26 tff(c_2216, plain, (barrel('#skF_1', '#skF_5'))).
% 12.15/4.26 tff(c_2206, plain, (event('#skF_1', '#skF_5'))).
% 12.15/4.26 tff(c_2199, plain, (present('#skF_1', '#skF_5'))).
% 12.15/4.26 tff(c_2194, plain, (dirty('#skF_1', '#skF_3'))).
% 12.15/4.26 tff(c_2188, plain, (city('#skF_1', '#skF_3'))).
% 12.15/4.26 tff(c_2184, plain, (white('#skF_1', '#skF_3'))).
% 12.15/4.26 tff(c_2182, plain, (placename('#skF_1', '#skF_2'))).
% 12.15/4.26 tff(c_2181, plain, (hollywood_placename('#skF_1', '#skF_2'))).
% 12.15/4.26 tff(c_2180, plain, (old('#skF_1', '#skF_3'))).
% 12.15/4.26 tff(c_2179, plain, (lonely('#skF_1', '#skF_4'))).
% 12.15/4.26 tff(c_2177, plain, (street('#skF_1', '#skF_4'))).
% 12.15/4.26 tff(c_2176, plain, (two('#skF_1', '#skF_6'))).
% 12.15/4.26 tff(c_2168, plain, (chevy('#skF_1', '#skF_3'))).
% 12.15/4.26 tff(c_2166, plain, (group('#skF_1', '#skF_6'))).
% 12.15/4.26 tff(c_2163, plain, (actual_world('#skF_1'))).
% 12.15/4.26 tff(c_2031, plain, (agent('#skF_11', '#skF_15', '#skF_12'))).
% 12.15/4.26 tff(c_1968, plain, (of('#skF_11', '#skF_13', '#skF_14'))).
% 12.15/4.26 tff(c_1862, plain, (down('#skF_11', '#skF_15', '#skF_14'))).
% 12.15/4.26 tff(c_1839, plain, (in('#skF_11', '#skF_15', '#skF_14'))).
% 12.15/4.26 tff(c_1828, plain, (city('#skF_11', '#skF_14'))).
% 12.15/4.26 tff(c_1827, plain, (group('#skF_11', '#skF_16'))).
% 12.15/4.26 tff(c_1826, plain, (present('#skF_11', '#skF_15'))).
% 12.15/4.26 tff(c_1824, plain, (street('#skF_11', '#skF_14'))).
% 12.15/4.26 tff(c_1823, plain, (chevy('#skF_11', '#skF_12'))).
% 12.15/4.26 tff(c_1822, plain, (barrel('#skF_11', '#skF_15'))).
% 12.15/4.26 tff(c_1821, plain, (dirty('#skF_11', '#skF_12'))).
% 12.15/4.26 tff(c_1819, plain, (event('#skF_11', '#skF_15'))).
% 12.15/4.26 tff(c_1816, plain, (lonely('#skF_11', '#skF_14'))).
% 12.15/4.26 tff(c_1814, plain, (hollywood_placename('#skF_11', '#skF_13'))).
% 12.15/4.26 tff(c_1812, plain, (two('#skF_11', '#skF_16'))).
% 12.15/4.26 tff(c_1808, plain, (white('#skF_11', '#skF_12'))).
% 12.15/4.26 tff(c_1805, plain, (placename('#skF_11', '#skF_13'))).
% 12.15/4.26 tff(c_1803, plain, (old('#skF_11', '#skF_12'))).
% 12.15/4.26 tff(c_1801, plain, (actual_world('#skF_11'))).
% 12.15/4.26 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 12.15/4.26
%------------------------------------------------------------------------------