%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : NLP134+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 : n019.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 11.14s 3.71s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.12 % Problem : NLP134+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.12/0.34 % Computer : n019.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Tue Apr 8 08:43:32 EDT 2025
% 0.12/0.34 % CPUTime :
% 11.14/3.71
% 11.14/3.71 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.14/3.71
% 11.14/3.71 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.14/3.72 %$ 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
% 11.14/3.72
% 11.14/3.72 %Foreground sorts:
% 11.14/3.72
% 11.14/3.72
% 11.14/3.72 %Background operators:
% 11.14/3.72
% 11.14/3.72
% 11.14/3.72 %Foreground operators:
% 11.14/3.72 tff('#skF_10', type, '#skF_10': ($i * $i * $i * $i * $i * $i) > $i).
% 11.14/3.72 tff(two, type, two: ($i * $i) > $o).
% 11.14/3.72 tff('#skF_7', type, '#skF_7': $i > $i).
% 11.14/3.72 tff(frontseat, type, frontseat: ($i * $i) > $o).
% 11.14/3.72 tff(placename, type, placename: ($i * $i) > $o).
% 11.14/3.72 tff(member, type, member: ($i * $i * $i) > $o).
% 11.14/3.72 tff(be, type, be: ($i * $i * $i * $i) > $o).
% 11.14/3.72 tff('#skF_9', type, '#skF_9': ($i * $i * $i * $i * $i * $i) > $i).
% 11.14/3.72 tff(present, type, present: ($i * $i) > $o).
% 11.14/3.72 tff('#skF_18', type, '#skF_18': $i > $i).
% 11.14/3.72 tff(in, type, in: ($i * $i * $i) > $o).
% 11.14/3.72 tff(old, type, old: ($i * $i) > $o).
% 11.14/3.72 tff(dirty, type, dirty: ($i * $i) > $o).
% 11.14/3.72 tff('#skF_11', type, '#skF_11': $i).
% 11.14/3.72 tff('#skF_15', type, '#skF_15': $i).
% 11.14/3.72 tff(city, type, city: ($i * $i) > $o).
% 11.14/3.72 tff(young, type, young: ($i * $i) > $o).
% 11.14/3.72 tff('#skF_8', type, '#skF_8': $i > $i).
% 11.14/3.72 tff(of, type, of: ($i * $i * $i) > $o).
% 11.14/3.72 tff('#skF_19', type, '#skF_19': ($i * $i * $i * $i * $i * $i) > $i).
% 11.14/3.72 tff(actual_world, type, actual_world: $i > $o).
% 11.14/3.72 tff(agent, type, agent: ($i * $i * $i) > $o).
% 11.14/3.72 tff('#skF_16', type, '#skF_16': $i).
% 11.14/3.72 tff('#skF_14', type, '#skF_14': $i).
% 11.14/3.72 tff('#skF_5', type, '#skF_5': $i).
% 11.14/3.72 tff(group, type, group: ($i * $i) > $o).
% 11.14/3.72 tff(lonely, type, lonely: ($i * $i) > $o).
% 11.14/3.72 tff(fellow, type, fellow: ($i * $i) > $o).
% 11.14/3.72 tff('#skF_6', type, '#skF_6': $i).
% 11.14/3.72 tff('#skF_13', type, '#skF_13': $i).
% 11.14/3.72 tff('#skF_2', type, '#skF_2': $i).
% 11.14/3.72 tff('#skF_3', type, '#skF_3': $i).
% 11.14/3.72 tff(event, type, event: ($i * $i) > $o).
% 11.14/3.72 tff('#skF_1', type, '#skF_1': $i).
% 11.14/3.72 tff(down, type, down: ($i * $i * $i) > $o).
% 11.14/3.72 tff(hollywood_placename, type, hollywood_placename: ($i * $i) > $o).
% 11.14/3.72 tff(white, type, white: ($i * $i) > $o).
% 11.14/3.72 tff(barrel, type, barrel: ($i * $i) > $o).
% 11.14/3.72 tff(state, type, state: ($i * $i) > $o).
% 11.14/3.72 tff(street, type, street: ($i * $i) > $o).
% 11.14/3.72 tff('#skF_4', type, '#skF_4': $i).
% 11.14/3.72 tff('#skF_17', type, '#skF_17': $i > $i).
% 11.14/3.72 tff(chevy, type, chevy: ($i * $i) > $o).
% 11.14/3.72 tff('#skF_20', type, '#skF_20': ($i * $i * $i * $i * $i * $i) > $i).
% 11.14/3.72 tff('#skF_12', type, '#skF_12': $i).
% 11.14/3.72
% 11.14/3.72 %Saturated clause set:
% 11.14/3.72 tff(c_2598, plain, (![X11_84, X_257, V_258]: (~down('#skF_11', '#skF_18'(X11_84), X_257) | ~barrel('#skF_11', '#skF_18'(X11_84)) | ~present('#skF_11', '#skF_18'(X11_84)) | ~agent('#skF_11', '#skF_18'(X11_84), '#skF_18'(X11_84)) | ~event('#skF_11', '#skF_18'(X11_84)) | ~lonely('#skF_11', X_257) | ~street('#skF_11', X_257) | ~old('#skF_11', '#skF_18'(X11_84)) | ~dirty('#skF_11', '#skF_18'(X11_84)) | ~white('#skF_11', '#skF_18'(X11_84)) | ~chevy('#skF_11', '#skF_18'(X11_84)) | ~placename('#skF_11', V_258) | ~hollywood_placename('#skF_11', V_258) | ~city('#skF_11', '#skF_18'(X11_84)) | ~of('#skF_11', V_258, '#skF_18'(X11_84)) | ~member('#skF_11', X11_84, '#skF_16')))).
% 11.14/3.72 tff(c_2602, plain, (~chevy('#skF_11', '#skF_14'))).
% 11.14/3.72 tff(c_2592, plain, (![Y_206, W_205, X_207, V_208]: (~in('#skF_11', Y_206, W_205) | ~down('#skF_11', Y_206, X_207) | ~barrel('#skF_11', Y_206) | ~present('#skF_11', Y_206) | ~agent('#skF_11', Y_206, W_205) | ~event('#skF_11', Y_206) | ~lonely('#skF_11', X_207) | ~street('#skF_11', X_207) | ~old('#skF_11', W_205) | ~dirty('#skF_11', W_205) | ~white('#skF_11', W_205) | ~chevy('#skF_11', W_205) | ~placename('#skF_11', V_208) | ~hollywood_placename('#skF_11', V_208) | ~city('#skF_11', W_205) | ~of('#skF_11', V_208, W_205)))).
% 11.14/3.72 tff(c_2545, 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)))).
% 11.14/3.73 tff(c_2460, 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)))).
% 11.14/3.73 tff(c_2430, 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)))).
% 11.14/3.73 tff(c_2323, 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)))).
% 11.14/3.73 tff(c_2283, plain, (![X11_84]: (be('#skF_11', '#skF_17'(X11_84), X11_84, '#skF_18'(X11_84)) | ~member('#skF_11', X11_84, '#skF_16')))).
% 11.14/3.73 tff(c_2280, plain, (![X11_84]: (in('#skF_11', '#skF_18'(X11_84), '#skF_18'(X11_84)) | ~member('#skF_11', X11_84, '#skF_16')))).
% 11.14/3.73 tff(c_2271, plain, (![X11_84]: (frontseat('#skF_11', '#skF_18'(X11_84)) | ~member('#skF_11', X11_84, '#skF_16')))).
% 11.14/3.73 tff(c_2269, plain, (![X11_84]: (state('#skF_11', '#skF_17'(X11_84)) | ~member('#skF_11', X11_84, '#skF_16')))).
% 11.14/3.73 tff(c_2249, plain, (![X14_87]: (fellow('#skF_11', X14_87) | ~member('#skF_11', X14_87, '#skF_16')))).
% 11.14/3.73 tff(c_2229, plain, (![X14_87]: (young('#skF_11', X14_87) | ~member('#skF_11', X14_87, '#skF_16')))).
% 11.14/3.73 tff(c_2162, plain, (agent('#skF_1', '#skF_5', '#skF_3'))).
% 11.14/3.73 tff(c_2142, plain, (in('#skF_1', '#skF_5', '#skF_3'))).
% 11.14/3.73 tff(c_2131, plain, (of('#skF_1', '#skF_2', '#skF_3'))).
% 11.14/3.73 tff(c_2118, plain, (down('#skF_1', '#skF_5', '#skF_4'))).
% 11.14/3.73 tff(c_2092, plain, (barrel('#skF_1', '#skF_5'))).
% 11.14/3.73 tff(c_2085, plain, (chevy('#skF_1', '#skF_3'))).
% 11.14/3.73 tff(c_2084, plain, (event('#skF_1', '#skF_5'))).
% 11.14/3.73 tff(c_2083, plain, (dirty('#skF_1', '#skF_3'))).
% 11.14/3.73 tff(c_2081, plain, (white('#skF_1', '#skF_3'))).
% 11.14/3.73 tff(c_2079, plain, (lonely('#skF_1', '#skF_4'))).
% 11.14/3.73 tff(c_2078, plain, (present('#skF_1', '#skF_5'))).
% 11.14/3.73 tff(c_2077, plain, (placename('#skF_1', '#skF_2'))).
% 11.14/3.73 tff(c_2076, plain, (old('#skF_1', '#skF_3'))).
% 11.14/3.73 tff(c_2075, plain, (street('#skF_1', '#skF_4'))).
% 11.14/3.73 tff(c_2073, plain, (city('#skF_1', '#skF_3'))).
% 11.14/3.73 tff(c_2069, plain, (two('#skF_1', '#skF_6'))).
% 11.14/3.73 tff(c_2064, plain, (group('#skF_1', '#skF_6'))).
% 11.14/3.73 tff(c_2060, plain, (hollywood_placename('#skF_1', '#skF_2'))).
% 11.14/3.73 tff(c_2045, plain, (actual_world('#skF_1'))).
% 11.14/3.73 tff(c_1897, plain, (agent('#skF_11', '#skF_15', '#skF_12'))).
% 11.14/3.73 tff(c_1813, plain, (of('#skF_11', '#skF_13', '#skF_14'))).
% 11.14/3.73 tff(c_1770, plain, (down('#skF_11', '#skF_15', '#skF_14'))).
% 11.14/3.73 tff(c_1727, plain, (in('#skF_11', '#skF_15', '#skF_14'))).
% 11.14/3.73 tff(c_1711, plain, (dirty('#skF_11', '#skF_12'))).
% 11.14/3.73 tff(c_1710, plain, (present('#skF_11', '#skF_15'))).
% 11.14/3.73 tff(c_1709, plain, (hollywood_placename('#skF_11', '#skF_13'))).
% 11.14/3.73 tff(c_1708, plain, (group('#skF_11', '#skF_16'))).
% 11.14/3.73 tff(c_1706, plain, (street('#skF_11', '#skF_14'))).
% 11.14/3.73 tff(c_1705, plain, (city('#skF_11', '#skF_14'))).
% 11.14/3.73 tff(c_1703, plain, (chevy('#skF_11', '#skF_12'))).
% 11.14/3.73 tff(c_1697, plain, (event('#skF_11', '#skF_15'))).
% 11.14/3.73 tff(c_1695, plain, (barrel('#skF_11', '#skF_15'))).
% 11.14/3.73 tff(c_1694, plain, (placename('#skF_11', '#skF_13'))).
% 11.14/3.73 tff(c_1690, plain, (two('#skF_11', '#skF_16'))).
% 11.14/3.73 tff(c_1688, plain, (lonely('#skF_11', '#skF_14'))).
% 11.14/3.73 tff(c_1687, plain, (old('#skF_11', '#skF_12'))).
% 11.14/3.73 tff(c_1685, plain, (white('#skF_11', '#skF_12'))).
% 11.14/3.73 tff(c_1683, plain, (actual_world('#skF_11'))).
% 11.14/3.73 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.14/3.73
%------------------------------------------------------------------------------