%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : PLA053_15 : 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 : n004.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 08:23:09 PM UTC 2025
% Result : CounterSatisfiable 3.29s 1.81s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.03/0.12 % Problem : PLA053_15 : TPTP v9.0.0. Released v8.2.0.
% 0.03/0.13 % 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.34 % Computer : n004.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 16:48:22 EDT 2025
% 0.13/0.34 % CPUTime :
% 3.29/1.80
% 3.29/1.81 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.29/1.81
% 3.29/1.81 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.29/1.81 %$ h > defused > bomb > #nlpp > #skF_7 > #skF_3 > #skF_2 > #skF_5 > #skF_6 > #skF_4 > #skF_1
% 3.29/1.81
% 3.29/1.81 %Foreground sorts:
% 3.29/1.81 tff($ki_world, type, $ki_world: $tType ).
% 3.29/1.81
% 3.29/1.81 %Background operators:
% 3.29/1.81
% 3.29/1.81
% 3.29/1.81 %Foreground operators:
% 3.29/1.81 tff(defused, type, defused: ($ki_world * $i) > $o).
% 3.29/1.81 tff('#skF_7', type, '#skF_7': $i).
% 3.29/1.81 tff(h, type, h: ($ki_world * $i) > $o).
% 3.29/1.81 tff('#skF_3', type, '#skF_3': $ki_world > $i).
% 3.29/1.81 tff(bomb, type, bomb: ($ki_world * $i) > $o).
% 3.29/1.81 tff('#skF_2', type, '#skF_2': $ki_world > $i).
% 3.29/1.81 tff('#skF_5', type, '#skF_5': ($ki_world * $i) > $i).
% 3.29/1.81 tff('#skF_6', type, '#skF_6': $ki_world).
% 3.29/1.81 tff('#skF_4', type, '#skF_4': $i).
% 3.29/1.81 tff('#skF_1', type, '#skF_1': $ki_world > $ki_world).
% 3.29/1.81
% 3.29/1.81 %Saturated clause set:
% 3.29/1.81 tff(c_91, plain, (~$ki_accessible('#skF_6', '#skF_6'))).
% 3.35/1.82 tff(c_82, plain, (![X_62, W_63:$ki_world]: (defused('#skF_6', X_62) | ~bomb('#skF_6', X_62) | ~$ki_accessible(W_63, '#skF_6') | ~$ki_exists_in_world_$i(W_63, X_62) | ~$ki_accessible($ki_local_world, W_63) | ~$ki_exists_in_world_$i('#skF_6', '#skF_5'(W_63, X_62))))).
% 3.35/1.82 tff(c_16, plain, (![W0_37:$ki_world, X_32, W_24:$ki_world]: (defused(W0_37, X_32) | ~h(W0_37, '#skF_5'(W_24, X_32)) | ~bomb(W0_37, X_32) | ~$ki_accessible(W_24, W0_37) | ~$ki_exists_in_world_$i(W_24, X_32) | ~$ki_accessible($ki_local_world, W_24)))).
% 3.35/1.82 tff(c_74, plain, (![W_1:$ki_world, X_57]: (bomb('#skF_1'(W_1), X_57) | ~h(W_1, '#skF_4') | ~bomb(W_1, X_57) | ~$ki_exists_in_world_$i(W_1, X_57) | ~$ki_accessible($ki_local_world, W_1)))).
% 3.35/1.82 tff(c_12, plain, (![W0_23:$ki_world, X_21, W_17:$ki_world]: (bomb(W0_23, X_21) | ~$ki_accessible(W_17, W0_23) | ~h(W_17, '#skF_4') | ~bomb(W_17, X_21) | ~$ki_exists_in_world_$i(W_17, X_21) | ~$ki_accessible($ki_local_world, W_17)))).
% 3.35/1.82 tff(c_68, plain, (~$ki_accessible($ki_local_world, $ki_local_world))).
% 3.35/1.82 tff(c_44, plain, (![W_1:$ki_world, X_49]: ($ki_exists_in_world_$i('#skF_1'(W_1), X_49) | ~$ki_exists_in_world_$i(W_1, X_49)))).
% 3.35/1.82 tff(c_59, plain, ($ki_exists_in_world_$i('#skF_6', '#skF_2'($ki_local_world)))).
% 3.35/1.82 tff(c_60, plain, ($ki_exists_in_world_$i('#skF_6', '#skF_4'))).
% 3.35/1.82 tff(c_18, plain, (![W_24:$ki_world, X_32]: ($ki_exists_in_world_$i(W_24, '#skF_5'(W_24, X_32)) | ~$ki_exists_in_world_$i(W_24, X_32) | ~$ki_accessible($ki_local_world, W_24)))).
% 3.35/1.82 tff(c_45, plain, (![X_49]: ($ki_exists_in_world_$i('#skF_6', X_49) | ~$ki_exists_in_world_$i($ki_local_world, X_49)))).
% 3.35/1.82 tff(c_4, plain, (![V_4:$ki_world, X_5, W_3:$ki_world]: ($ki_exists_in_world_$i(V_4, X_5) | ~$ki_accessible(W_3, V_4) | ~$ki_exists_in_world_$i(W_3, X_5)))).
% 3.35/1.82 tff(c_10, plain, (![W_8:$ki_world]: ($ki_exists_in_world_$i(W_8, '#skF_3'(W_8)) | ~$ki_accessible($ki_local_world, W_8)))).
% 3.35/1.82 tff(c_8, plain, (![W_8:$ki_world]: (bomb(W_8, '#skF_3'(W_8)) | ~$ki_accessible($ki_local_world, W_8)))).
% 3.35/1.82 tff(c_36, plain, (~defused('#skF_6', '#skF_7'))).
% 3.35/1.82 tff(c_35, plain, (bomb('#skF_6', '#skF_7'))).
% 3.35/1.82 tff(c_26, plain, (![D_42]: (h('#skF_6', D_42) | ~$ki_exists_in_world_$i('#skF_6', D_42)))).
% 3.35/1.82 tff(c_2, plain, (![W_1:$ki_world]: ($ki_accessible(W_1, '#skF_1'(W_1))))).
% 3.35/1.82 tff(c_6, plain, (![W_6:$ki_world]: ($ki_exists_in_world_$i(W_6, '#skF_2'(W_6))))).
% 3.35/1.82 tff(c_14, plain, ($ki_exists_in_world_$i($ki_local_world, '#skF_4'))).
% 3.35/1.82 tff(c_20, plain, ($ki_exists_in_world_$i('#skF_6', '#skF_7'))).
% 3.35/1.82 tff(c_22, plain, ($ki_accessible($ki_local_world, '#skF_6'))).
% 3.35/1.82 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.35/1.82
%------------------------------------------------------------------------------