%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : LCL950_17 : TPTP v9.3.1. 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 : n017.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Mon Sep 7 11:13:01 AM UTC 2026
% Result : Theorem 4.22s 2.59s
% Output : CNFRefutation 4.56s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : LCL950_17 : TPTP v9.3.1. Released v8.2.0.
% 0.00/0.04 % 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.10/0.38 % Computer : n017.cluster.edu
% 0.10/0.38 % Model : x86_64 x86_64
% 0.10/0.38 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.10/0.38 % Memory : 8046.5625MB
% 0.10/0.38 % OS : Linux 6.8.0-71-generic
% 0.10/0.38 % CPULimit : 300
% 0.10/0.38 % WCLimit : 300
% 0.10/0.38 % DateTime : Sat Sep 5 17:12:07 UTC 2026
% 0.10/0.38 % CPUTime :
% 4.22/2.59 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.22/2.59
% 4.22/2.59 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 4.56/2.62 %$ member > intersect > #nlpp > #skF_9 > #skF_5 > #skF_14 > #skF_6 > #skF_1 > #skF_7 > #skF_10 > #skF_11 > #skF_4 > #skF_2 > #skF_3 > #skF_13 > #skF_8 > #skF_12
% 4.56/2.62
% 4.56/2.62 %Foreground sorts:
% 4.56/2.62 tff($ki_world, type, $ki_world: $tType ).
% 4.56/2.62
% 4.56/2.62 %Background operators:
% 4.56/2.62
% 4.56/2.62
% 4.56/2.62 %Foreground operators:
% 4.56/2.62 tff('#skF_9', type, '#skF_9': $ki_world).
% 4.56/2.62 tff('#skF_5', type, '#skF_5': ($i * $ki_world * $i * $ki_world * $i * $ki_world) > $ki_world).
% 4.56/2.62 tff('#skF_14', type, '#skF_14': $ki_world).
% 4.56/2.62 tff('#skF_6', type, '#skF_6': ($i * $ki_world * $ki_world * $i * $ki_world) > $ki_world).
% 4.56/2.62 tff('#skF_1', type, '#skF_1': $ki_world > $i).
% 4.56/2.62 tff('#skF_7', type, '#skF_7': $ki_world).
% 4.56/2.62 tff(member, type, member: ($ki_world * $i * $i) > $o).
% 4.56/2.62 tff(intersect, type, intersect: ($ki_world * $i * $i) > $o).
% 4.56/2.62 tff('#skF_10', type, '#skF_10': $i).
% 4.56/2.62 tff('#skF_11', type, '#skF_11': $ki_world).
% 4.56/2.62 tff('#skF_4', type, '#skF_4': ($i * $ki_world * $i * $ki_world * $i * $ki_world) > $ki_world).
% 4.56/2.62 tff('#skF_2', type, '#skF_2': ($i * $ki_world * $ki_world * $i * $ki_world) > $ki_world).
% 4.56/2.62 tff('#skF_3', type, '#skF_3': ($i * $ki_world * $ki_world * $i * $ki_world) > $i).
% 4.56/2.62 tff('#skF_13', type, '#skF_13': $ki_world).
% 4.56/2.62 tff('#skF_8', type, '#skF_8': $i).
% 4.56/2.62 tff('#skF_12', type, '#skF_12': $i).
% 4.56/2.62
% 4.56/2.64 tff(f_30, axiom, (![W:$ki_world, V:$ki_world]: $ki_accessible(W, V)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', mrel_universal)).
% 4.56/2.64 tff(f_148, negated_conjecture, ~(![W:$ki_world]: ($ki_accessible($ki_local_world, W) => (![B]: ($ki_exists_in_world_$i(W, B) => (![W0:$ki_world]: ($ki_accessible(W, W0) => (![C]: ($ki_exists_in_world_$i(W0, C) => (![W1:$ki_world]: ($ki_accessible(W0, W1) => (![D]: ($ki_exists_in_world_$i(W1, D) => (![W2:$ki_world]: ($ki_accessible(W1, W2) => (((![W3:$ki_world]: ($ki_accessible(W2, W3) => member(W3, B, C))) & (![W3:$ki_world]: ($ki_accessible(W2, W3) => member(W3, B, D)))) => (![W3:$ki_world]: ($ki_accessible(W2, W3) => intersect(W3, C, D)))))))))))))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', verify)).
% 4.56/2.64 tff(f_32, axiom, (![W:$ki_world, X]: $ki_exists_in_world_$i(W, X)), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', $ki_exists_in_world_$i_const)).
% 4.56/2.64 tff(f_88, axiom, (![W:$ki_world]: ($ki_accessible($ki_local_world, W) => (![B]: ($ki_exists_in_world_$i(W, B) => (![W0:$ki_world]: ($ki_accessible(W, W0) => (![C]: ($ki_exists_in_world_$i(W0, C) => ((![W1:$ki_world]: ($ki_accessible(W0, W1) => ((![W2:$ki_world]: ($ki_accessible(W1, W2) => intersect(W2, B, C))) => (?[D]: (($ki_exists_in_world_$i(W1, D) & (![W2:$ki_world]: ($ki_accessible(W1, W2) => member(W2, D, B)))) & (![W2:$ki_world]: ($ki_accessible(W1, W2) => member(W2, D, C)))))))) & (![W1:$ki_world]: ($ki_accessible(W0, W1) => ((?[D]: (($ki_exists_in_world_$i(W1, D) & (![W2:$ki_world]: ($ki_accessible(W1, W2) => member(W2, D, B)))) & (![W2:$ki_world]: ($ki_accessible(W1, W2) => member(W2, D, C))))) => (![W2:$ki_world]: ($ki_accessible(W1, W2) => intersect(W2, B, C))))))))))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', intersect_defn)).
% 4.56/2.64 tff(f_112, axiom, (![W:$ki_world]: ($ki_accessible($ki_local_world, W) => (![B]: ($ki_exists_in_world_$i(W, B) => (![W0:$ki_world]: ($ki_accessible(W, W0) => (![C]: ($ki_exists_in_world_$i(W0, C) => (![W1:$ki_world]: ($ki_accessible(W0, W1) => ((![W2:$ki_world]: ($ki_accessible(W1, W2) => intersect(W2, B, C))) => (![W2:$ki_world]: ($ki_accessible(W1, W2) => intersect(W2, C, B)))))))))))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', symmetry_of_intersect)).
% 4.56/2.64 tff(c_2, plain, (![W_1:$ki_world, V_2:$ki_world]: ($ki_accessible(W_1, V_2))), inference(cnfTransformation, [status(thm)], [f_30])).
% 4.56/2.64 tff(c_38, plain, (![W3_1029:$ki_world]: (member(W3_1029, '#skF_8', '#skF_10') | ~$ki_accessible('#skF_13', W3_1029))), inference(cnfTransformation, [status(thm)], [f_148])).
% 4.56/2.64 tff(c_86, plain, (![W3_1029:$ki_world]: (member(W3_1029, '#skF_8', '#skF_10'))), inference(demodulation, [status(thm), theory('equality')], [c_2, c_38])).
% 4.56/2.64 tff(c_36, plain, (![W3_1030:$ki_world]: (member(W3_1030, '#skF_8', '#skF_12') | ~$ki_accessible('#skF_13', W3_1030))), inference(cnfTransformation, [status(thm)], [f_148])).
% 4.56/2.64 tff(c_88, plain, (![W3_1030:$ki_world]: (member(W3_1030, '#skF_8', '#skF_12'))), inference(demodulation, [status(thm), theory('equality')], [c_2, c_36])).
% 4.56/2.64 tff(c_4, plain, (![W_3:$ki_world, X_4]: ($ki_exists_in_world_$i(W_3, X_4))), inference(cnfTransformation, [status(thm)], [f_32])).
% 4.56/2.64 tff(c_8, plain, (![W1_423:$ki_world, W_7:$ki_world, W2_433:$ki_world, D_430, W0_331:$ki_world, C_385, B_223]: (~member('#skF_4'(C_385, W1_423, D_430, W0_331, B_223, W_7), D_430, B_223) | ~member('#skF_5'(C_385, W1_423, D_430, W0_331, B_223, W_7), D_430, C_385) | intersect(W2_433, B_223, C_385) | ~$ki_accessible(W1_423, W2_433) | ~$ki_exists_in_world_$i(W1_423, D_430) | ~$ki_accessible(W0_331, W1_423) | ~$ki_exists_in_world_$i(W0_331, C_385) | ~$ki_accessible(W_7, W0_331) | ~$ki_exists_in_world_$i(W_7, B_223) | ~$ki_accessible($ki_local_world, W_7))), inference(cnfTransformation, [status(thm)], [f_88])).
% 4.56/2.64 tff(c_78, plain, (![W1_423:$ki_world, W_7:$ki_world, W2_433:$ki_world, D_430, W0_331:$ki_world, C_385, B_223]: (~member('#skF_4'(C_385, W1_423, D_430, W0_331, B_223, W_7), D_430, B_223) | ~member('#skF_5'(C_385, W1_423, D_430, W0_331, B_223, W_7), D_430, C_385) | intersect(W2_433, B_223, C_385) | ~$ki_accessible(W1_423, W2_433) | ~$ki_accessible(W0_331, W1_423) | ~$ki_accessible(W_7, W0_331) | ~$ki_accessible($ki_local_world, W_7))), inference(demodulation, [status(thm), theory('equality')], [c_4, c_4, c_4, c_8])).
% 4.56/2.64 tff(c_117, plain, (![W2_1058:$ki_world, C_1055, W0_1059:$ki_world, W_1061:$ki_world, D_1057, B_1060, W1_1056:$ki_world]: (~member('#skF_4'(C_1055, W1_1056, D_1057, W0_1059, B_1060, W_1061), D_1057, B_1060) | ~member('#skF_5'(C_1055, W1_1056, D_1057, W0_1059, B_1060, W_1061), D_1057, C_1055) | intersect(W2_1058, B_1060, C_1055))), inference(demodulation, [status(thm), theory('equality')], [c_2, c_2, c_2, c_2, c_78])).
% 4.56/2.64 tff(c_126, plain, (![W1_1066:$ki_world, W_1065:$ki_world, C_1062, W2_1063:$ki_world, W0_1064:$ki_world]: (~member('#skF_5'(C_1062, W1_1066, '#skF_8', W0_1064, '#skF_12', W_1065), '#skF_8', C_1062) | intersect(W2_1063, '#skF_12', C_1062))), inference(resolution, [status(thm)], [c_88, c_117])).
% 4.56/2.64 tff(c_149, plain, (![W2_1068:$ki_world]: (intersect(W2_1068, '#skF_12', '#skF_10'))), inference(resolution, [status(thm)], [c_86, c_126])).
% 4.56/2.64 tff(c_28, plain, (![C_518, W1_524:$ki_world, W2_527:$ki_world, W_434:$ki_world, B_482, W0_506:$ki_world]: (~intersect('#skF_6'(C_518, W0_506, W_434, B_482, W1_524), B_482, C_518) | intersect(W2_527, C_518, B_482) | ~$ki_accessible(W1_524, W2_527) | ~$ki_accessible(W0_506, W1_524) | ~$ki_exists_in_world_$i(W0_506, C_518) | ~$ki_accessible(W_434, W0_506) | ~$ki_exists_in_world_$i(W_434, B_482) | ~$ki_accessible($ki_local_world, W_434))), inference(cnfTransformation, [status(thm)], [f_112])).
% 4.56/2.64 tff(c_58, plain, (![C_518, W1_524:$ki_world, W2_527:$ki_world, W_434:$ki_world, B_482, W0_506:$ki_world]: (~intersect('#skF_6'(C_518, W0_506, W_434, B_482, W1_524), B_482, C_518) | intersect(W2_527, C_518, B_482) | ~$ki_accessible(W1_524, W2_527) | ~$ki_accessible(W0_506, W1_524) | ~$ki_accessible(W_434, W0_506) | ~$ki_accessible($ki_local_world, W_434))), inference(demodulation, [status(thm), theory('equality')], [c_4, c_4, c_28])).
% 4.56/2.64 tff(c_91, plain, (![C_518, W1_524:$ki_world, W2_527:$ki_world, W_434:$ki_world, B_482, W0_506:$ki_world]: (~intersect('#skF_6'(C_518, W0_506, W_434, B_482, W1_524), B_482, C_518) | intersect(W2_527, C_518, B_482))), inference(demodulation, [status(thm), theory('equality')], [c_2, c_2, c_2, c_2, c_58])).
% 4.56/2.64 tff(c_161, plain, (![W2_527:$ki_world]: (intersect(W2_527, '#skF_10', '#skF_12'))), inference(resolution, [status(thm)], [c_149, c_91])).
% 4.56/2.64 tff(c_32, plain, (~intersect('#skF_14', '#skF_10', '#skF_12')), inference(cnfTransformation, [status(thm)], [f_148])).
% 4.56/2.64 tff(c_164, plain, $false, inference(demodulation, [status(thm), theory('equality')], [c_161, c_32])).
% 4.56/2.64 % SZS output end CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------