%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : NLP266_3 : TPTP v9.0.0. Released v8.2.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 : 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:50 PM UTC 2025
% Result : CounterSatisfiable 3.76s 1.99s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.06/0.13 % Problem : NLP266_3 : TPTP v9.0.0. Released v8.2.0.
% 0.06/0.14 % 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.13/0.35 % Computer : n008.cluster.edu
% 0.13/0.35 % Model : x86_64 x86_64
% 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.35 % Memory : 8042.1875MB
% 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64
% 0.13/0.35 % CPULimit : 300
% 0.13/0.35 % WCLimit : 300
% 0.13/0.35 % DateTime : Tue Apr 8 09:52:32 EDT 2025
% 0.13/0.35 % CPUTime :
% 3.50/1.98
% 3.76/1.99 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.76/1.99
% 3.76/1.99 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.76/1.99 %$ in > do > userid > number > string > entry_box > #nlpp > u > one > #skF_7 > #skF_9 > #skF_8 > #skF_5 > #skF_3 > #skF_2 > #skF_6 > #skF_4 > #skF_1
% 3.76/1.99
% 3.76/1.99 %Foreground sorts:
% 3.76/1.99 tff($ki_world, type, $ki_world: $tType ).
% 3.76/1.99
% 3.76/1.99 %Background operators:
% 3.76/1.99
% 3.76/1.99
% 3.76/1.99 %Foreground operators:
% 3.76/1.99 tff('#skF_7', type, '#skF_7': ($i * $i * $i * $i) > $ki_world).
% 3.76/1.99 tff(entry_box, type, entry_box: ($ki_world * $i) > $o).
% 3.76/1.99 tff(string, type, string: ($ki_world * $i) > $o).
% 3.76/1.99 tff('#skF_9', type, '#skF_9': ($i * $i * $i * $i) > $i).
% 3.76/1.99 tff('#skF_8', type, '#skF_8': ($i * $i * $i * $i) > $ki_world).
% 3.76/1.99 tff(u, type, u: $i).
% 3.76/1.99 tff(in, type, in: ($ki_world * $i * $i * $i) > $o).
% 3.76/1.99 tff('#skF_5', type, '#skF_5': ($ki_world * $i * $i * $i) > $i).
% 3.76/1.99 tff('#skF_3', type, '#skF_3': $ki_world > $i).
% 3.76/1.99 tff('#skF_2', type, '#skF_2': $ki_world > $i).
% 3.76/1.99 tff(number, type, number: ($ki_world * $i * $i) > $o).
% 3.76/1.99 tff(one, type, one: $i).
% 3.76/1.99 tff('#skF_6', type, '#skF_6': $ki_world).
% 3.76/1.99 tff('#skF_4', type, '#skF_4': $i).
% 3.76/1.99 tff(do, type, do: ($ki_world * $i * $i * $i) > $o).
% 3.76/1.99 tff(userid, type, userid: ($ki_world * $i * $i) > $o).
% 3.76/1.99 tff('#skF_1', type, '#skF_1': $ki_world > $ki_world).
% 3.76/1.99
% 3.76/1.99 %Saturated clause set:
% 3.76/2.00 tff(c_131, plain, (![W_357:$ki_world, I_356, B_360, S_359]: (~$ki_accessible(W_357, '#skF_8'(I_356, B_360, '#skF_5'(W_357, S_359, I_356, B_360), S_359)) | ~entry_box(W_357, B_360) | ~string(W_357, I_356) | ~$ki_accessible($ki_local_world, W_357) | ~number('#skF_7'(I_356, B_360, '#skF_5'(W_357, S_359, I_356, B_360), S_359), B_360, one) | ~entry_box('#skF_7'(I_356, B_360, '#skF_5'(W_357, S_359, I_356, B_360), S_359), B_360) | ~userid('#skF_7'(I_356, B_360, '#skF_5'(W_357, S_359, I_356, B_360), S_359), u, I_356)))).
% 3.76/2.00 tff(c_107, plain, (![I_336, W_15:$ki_world, I_111, B_127, S_339, B_337]: (in('#skF_8'(I_336, B_337, '#skF_5'(W_15, S_339, I_111, B_127), S_339), I_111, B_127, '#skF_9'(I_336, B_337, '#skF_5'(W_15, S_339, I_111, B_127), S_339)) | ~$ki_accessible(W_15, '#skF_8'(I_336, B_337, '#skF_5'(W_15, S_339, I_111, B_127), S_339)) | ~entry_box(W_15, B_127) | ~string(W_15, I_111) | ~$ki_accessible($ki_local_world, W_15) | ~number('#skF_7'(I_336, B_337, '#skF_5'(W_15, S_339, I_111, B_127), S_339), B_337, one) | ~entry_box('#skF_7'(I_336, B_337, '#skF_5'(W_15, S_339, I_111, B_127), S_339), B_337) | ~userid('#skF_7'(I_336, B_337, '#skF_5'(W_15, S_339, I_111, B_127), S_339), u, I_336)))).
% 3.76/2.00 tff(c_120, plain, (![W_350:$ki_world, I_349, B_348, S_346]: (~$ki_accessible(W_350, '#skF_8'(I_349, B_348, '#skF_5'(W_350, S_346, I_349, B_348), S_346)) | ~entry_box(W_350, B_348) | ~string(W_350, I_349) | ~$ki_accessible($ki_local_world, W_350) | $ki_accessible('#skF_6', '#skF_7'(I_349, B_348, '#skF_5'(W_350, S_346, I_349, B_348), S_346))))).
% 3.76/2.00 tff(c_78, plain, (![B_322, I_317, I_220, W_319:$ki_world, B_260, S_290]: (in('#skF_8'(I_220, B_260, '#skF_5'(W_319, S_290, I_317, B_322), S_290), I_317, B_322, '#skF_9'(I_220, B_260, '#skF_5'(W_319, S_290, I_317, B_322), S_290)) | ~$ki_accessible(W_319, '#skF_8'(I_220, B_260, '#skF_5'(W_319, S_290, I_317, B_322), S_290)) | ~entry_box(W_319, B_322) | ~string(W_319, I_317) | ~$ki_accessible($ki_local_world, W_319) | $ki_accessible('#skF_6', '#skF_7'(I_220, B_260, '#skF_5'(W_319, S_290, I_317, B_322), S_290))))).
% 3.76/2.00 tff(c_59, plain, (![I_220, B_260, A_280, S_290]: (~number('#skF_7'(I_220, B_260, A_280, S_290), B_260, one) | ~entry_box('#skF_7'(I_220, B_260, A_280, S_290), B_260) | ~userid('#skF_7'(I_220, B_260, A_280, S_290), u, I_220) | ~in('#skF_8'(I_220, B_260, A_280, S_290), I_220, B_260, '#skF_9'(I_220, B_260, A_280, S_290))))).
% 3.76/2.00 tff(c_101, plain, (![A_280, S_290]: (~$ki_accessible($ki_local_world, '#skF_7'('#skF_3'('#skF_6'), '#skF_4', A_280, S_290)) | $ki_accessible('#skF_6', '#skF_8'('#skF_3'('#skF_6'), '#skF_4', A_280, S_290))))).
% 3.76/2.00 tff(c_53, plain, (![I_220, B_260, A_280, S_290]: (~number('#skF_7'(I_220, B_260, A_280, S_290), B_260, one) | ~entry_box('#skF_7'(I_220, B_260, A_280, S_290), B_260) | ~userid('#skF_7'(I_220, B_260, A_280, S_290), u, I_220) | do('#skF_8'(I_220, B_260, A_280, S_290), S_290, A_280, '#skF_9'(I_220, B_260, A_280, S_290))))).
% 3.76/2.00 tff(c_94, plain, (![W_330:$ki_world, A_331, S_332]: ($ki_accessible('#skF_6', '#skF_8'('#skF_3'(W_330), '#skF_4', A_331, S_332)) | ~$ki_accessible(W_330, '#skF_7'('#skF_3'(W_330), '#skF_4', A_331, S_332)) | ~$ki_accessible($ki_local_world, W_330) | ~$ki_accessible($ki_local_world, '#skF_7'('#skF_3'(W_330), '#skF_4', A_331, S_332))))).
% 3.76/2.00 tff(c_83, plain, (![I_323, A_325, S_326]: (~entry_box('#skF_7'(I_323, '#skF_4', A_325, S_326), '#skF_4') | ~userid('#skF_7'(I_323, '#skF_4', A_325, S_326), u, I_323) | $ki_accessible('#skF_6', '#skF_8'(I_323, '#skF_4', A_325, S_326)) | ~$ki_accessible($ki_local_world, '#skF_7'(I_323, '#skF_4', A_325, S_326))))).
% 3.76/2.00 tff(c_49, plain, (![I_220, B_260, A_280, S_290]: (~number('#skF_7'(I_220, B_260, A_280, S_290), B_260, one) | ~entry_box('#skF_7'(I_220, B_260, A_280, S_290), B_260) | ~userid('#skF_7'(I_220, B_260, A_280, S_290), u, I_220) | $ki_accessible('#skF_6', '#skF_8'(I_220, B_260, A_280, S_290))))).
% 3.76/2.00 tff(c_51, plain, (![W_15:$ki_world, I_111, S_79, B_127, W0_138:$ki_world, S2_140]: (in(W0_138, I_111, B_127, S2_140) | ~do(W0_138, S_79, '#skF_5'(W_15, S_79, I_111, B_127), S2_140) | ~$ki_accessible(W_15, W0_138) | ~entry_box(W_15, B_127) | ~string(W_15, I_111) | ~$ki_accessible($ki_local_world, W_15)))).
% 3.76/2.00 tff(c_57, plain, (![I_220, B_260, A_280, S_290]: ($ki_accessible('#skF_6', '#skF_7'(I_220, B_260, A_280, S_290)) | ~in('#skF_8'(I_220, B_260, A_280, S_290), I_220, B_260, '#skF_9'(I_220, B_260, A_280, S_290))))).
% 3.76/2.00 tff(c_61, plain, (![I_220, B_260, A_280, S_290]: ($ki_accessible('#skF_6', '#skF_7'(I_220, B_260, A_280, S_290)) | do('#skF_8'(I_220, B_260, A_280, S_290), S_290, A_280, '#skF_9'(I_220, B_260, A_280, S_290))))).
% 3.76/2.00 tff(c_45, plain, (![I_220, B_260, A_280, S_290]: ($ki_accessible('#skF_6', '#skF_7'(I_220, B_260, A_280, S_290)) | $ki_accessible('#skF_6', '#skF_8'(I_220, B_260, A_280, S_290))))).
% 3.76/2.00 tff(c_12, plain, (![W0_12:$ki_world, W_7:$ki_world]: (userid(W0_12, u, '#skF_3'(W_7)) | ~$ki_accessible(W_7, W0_12) | ~$ki_accessible($ki_local_world, W_7)))).
% 3.76/2.00 tff(c_10, plain, (![W0_12:$ki_world, W_7:$ki_world]: (string(W0_12, '#skF_3'(W_7)) | ~$ki_accessible(W_7, W0_12) | ~$ki_accessible($ki_local_world, W_7)))).
% 3.76/2.00 tff(c_16, plain, (![W_14:$ki_world]: (number(W_14, '#skF_4', one) | ~$ki_accessible($ki_local_world, W_14)))).
% 3.76/2.00 tff(c_18, plain, (![W_14:$ki_world]: (entry_box(W_14, '#skF_4') | ~$ki_accessible($ki_local_world, W_14)))).
% 3.76/2.00 tff(c_2, plain, (![W_1:$ki_world]: ($ki_accessible(W_1, '#skF_1'(W_1))))).
% 3.82/2.00 tff(c_4, plain, (![W_3:$ki_world, X_4]: ($ki_exists_in_world_$i(W_3, X_4)))).
% 3.82/2.00 tff(c_24, plain, ($ki_accessible($ki_local_world, '#skF_6'))).
% 3.82/2.00 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.82/2.00
%------------------------------------------------------------------------------