%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : PUZ128+2 : TPTP v9.0.0. Released v4.0.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 : n006.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:25:19 PM UTC 2025
% Result : Theorem 3.27s 1.78s
% Output : CNFRefutation 3.27s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----WARNING: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : PUZ128+2 : TPTP v9.0.0. Released v4.0.0.
% 0.07/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 : n006.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 17:29:38 EDT 2025
% 0.13/0.34 % CPUTime :
% 3.27/1.78 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.27/1.79
% 3.27/1.79 % SZS output start CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.27/1.80 %$ relation > patricide > parent > #nlpp > of > Thersandros > Polyneikes > Oedipus > Iokaste > #skF_5 > #skF_2 > #skF_3 > #skF_1 > #skF_6 > #skF_4
% 3.27/1.80
% 3.27/1.80 %Foreground sorts:
% 3.27/1.80
% 3.27/1.80
% 3.27/1.80 %Background operators:
% 3.27/1.80
% 3.27/1.80
% 3.27/1.80 %Foreground operators:
% 3.27/1.80 tff(Thersandros, type, Thersandros: $i).
% 3.27/1.80 tff(Iokaste, type, Iokaste: $i).
% 3.27/1.80 tff(parent, type, parent: $i > $o).
% 3.27/1.80 tff(of, type, of: $i).
% 3.27/1.80 tff(Oedipus, type, Oedipus: $i).
% 3.27/1.80 tff('#skF_5', type, '#skF_5': $i).
% 3.27/1.80 tff('#skF_2', type, '#skF_2': $i).
% 3.27/1.80 tff('#skF_3', type, '#skF_3': $i).
% 3.27/1.80 tff('#skF_1', type, '#skF_1': $i).
% 3.27/1.80 tff('#skF_6', type, '#skF_6': ($i * $i * $i * $i) > $i).
% 3.27/1.80 tff(Polyneikes, type, Polyneikes: $i).
% 3.27/1.80 tff('#skF_4', type, '#skF_4': $i).
% 3.27/1.80 tff(relation, type, relation: ($i * $i * $i) > $o).
% 3.27/1.80 tff(patricide, type, patricide: $i > $o).
% 3.27/1.80
% 3.27/1.81 tff(f_63, axiom, (?[A, B, C, D, E]: ((((((((((((((parent(A) & relation(A, of, Oedipus)) & (Iokaste = A)) & parent(B)) & relation(B, of, Polyneikes)) & (Iokaste = B)) & parent(C)) & relation(C, of, Polyneikes)) & (Oedipus = C)) & parent(D)) & relation(D, of, Thersandros)) & (Polyneikes = D)) & patricide(E)) & (Oedipus = E)) & ~(?[F]: (patricide(F) & (Thersandros = F))))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', background)).
% 3.27/1.81 tff(f_86, negated_conjecture, ~(?[A, B, C, D]: ((((((((parent(A) & patricide(B)) & parent(C)) & $true) & ~(?[E]: (patricide(E) & (D = E)))) & relation(C, of, D)) & (B = C)) & relation(A, of, B)) & (Iokaste = A))), file('/export/starexec/sandbox2/benchmark/theBenchmark.p', prove)).
% 3.27/1.81 tff(c_2, plain, (~patricide(Thersandros)), inference(cnfTransformation, [status(thm)], [f_63])).
% 3.27/1.81 tff(c_14, plain, (Oedipus='#skF_3'), inference(cnfTransformation, [status(thm)], [f_63])).
% 3.27/1.81 tff(c_4, plain, (Oedipus='#skF_5'), inference(cnfTransformation, [status(thm)], [f_63])).
% 3.27/1.81 tff(c_48, plain, ('#skF_5'='#skF_3'), inference(demodulation, [status(thm), theory('equality')], [c_14, c_4])).
% 3.27/1.81 tff(c_6, plain, (patricide('#skF_5')), inference(cnfTransformation, [status(thm)], [f_63])).
% 3.27/1.81 tff(c_49, plain, (patricide('#skF_3')), inference(demodulation, [status(thm), theory('equality')], [c_48, c_6])).
% 3.27/1.81 tff(c_18, plain, (parent('#skF_3')), inference(cnfTransformation, [status(thm)], [f_63])).
% 3.27/1.81 tff(c_8, plain, (Polyneikes='#skF_4'), inference(cnfTransformation, [status(thm)], [f_63])).
% 3.27/1.81 tff(c_16, plain, (relation('#skF_3', of, Polyneikes)), inference(cnfTransformation, [status(thm)], [f_63])).
% 3.27/1.81 tff(c_47, plain, (relation('#skF_3', of, '#skF_4')), inference(demodulation, [status(thm), theory('equality')], [c_8, c_16])).
% 3.27/1.81 tff(c_28, plain, (relation('#skF_1', of, Oedipus)), inference(cnfTransformation, [status(thm)], [f_63])).
% 3.27/1.81 tff(c_45, plain, (relation('#skF_1', of, '#skF_3')), inference(demodulation, [status(thm), theory('equality')], [c_14, c_28])).
% 3.27/1.81 tff(c_30, plain, (parent('#skF_1')), inference(cnfTransformation, [status(thm)], [f_63])).
% 3.27/1.81 tff(c_26, plain, (Iokaste='#skF_1'), inference(cnfTransformation, [status(thm)], [f_63])).
% 3.27/1.81 tff(c_32, plain, (![C_5, D_6]: ('#skF_6'(Iokaste, C_5, C_5, D_6)=D_6 | ~relation(Iokaste, of, C_5) | ~relation(C_5, of, D_6) | ~parent(C_5) | ~patricide(C_5) | ~parent(Iokaste))), inference(cnfTransformation, [status(thm)], [f_86])).
% 3.27/1.81 tff(c_36, plain, (![C_5, D_6]: ('#skF_6'('#skF_1', C_5, C_5, D_6)=D_6 | ~relation('#skF_1', of, C_5) | ~relation(C_5, of, D_6) | ~parent(C_5) | ~patricide(C_5) | ~parent('#skF_1'))), inference(demodulation, [status(thm), theory('equality')], [c_26, c_26, c_26, c_32])).
% 3.27/1.81 tff(c_71, plain, (![C_10, D_11]: ('#skF_6'('#skF_1', C_10, C_10, D_11)=D_11 | ~relation('#skF_1', of, C_10) | ~relation(C_10, of, D_11) | ~parent(C_10) | ~patricide(C_10))), inference(demodulation, [status(thm), theory('equality')], [c_30, c_36])).
% 3.27/1.81 tff(c_73, plain, (![D_11]: ('#skF_6'('#skF_1', '#skF_3', '#skF_3', D_11)=D_11 | ~relation('#skF_3', of, D_11) | ~parent('#skF_3') | ~patricide('#skF_3'))), inference(resolution, [status(thm)], [c_45, c_71])).
% 3.27/1.81 tff(c_82, plain, (![D_12]: ('#skF_6'('#skF_1', '#skF_3', '#skF_3', D_12)=D_12 | ~relation('#skF_3', of, D_12))), inference(demodulation, [status(thm), theory('equality')], [c_49, c_18, c_73])).
% 3.27/1.81 tff(c_86, plain, ('#skF_6'('#skF_1', '#skF_3', '#skF_3', '#skF_4')='#skF_4'), inference(resolution, [status(thm)], [c_47, c_82])).
% 3.27/1.81 tff(c_34, plain, (![C_5, D_6]: (patricide('#skF_6'(Iokaste, C_5, C_5, D_6)) | ~relation(Iokaste, of, C_5) | ~relation(C_5, of, D_6) | ~parent(C_5) | ~patricide(C_5) | ~parent(Iokaste))), inference(cnfTransformation, [status(thm)], [f_86])).
% 3.27/1.81 tff(c_35, plain, (![C_5, D_6]: (patricide('#skF_6'('#skF_1', C_5, C_5, D_6)) | ~relation('#skF_1', of, C_5) | ~relation(C_5, of, D_6) | ~parent(C_5) | ~patricide(C_5) | ~parent('#skF_1'))), inference(demodulation, [status(thm), theory('equality')], [c_26, c_26, c_26, c_34])).
% 3.27/1.81 tff(c_38, plain, (![C_5, D_6]: (patricide('#skF_6'('#skF_1', C_5, C_5, D_6)) | ~relation('#skF_1', of, C_5) | ~relation(C_5, of, D_6) | ~parent(C_5) | ~patricide(C_5))), inference(demodulation, [status(thm), theory('equality')], [c_30, c_35])).
% 3.27/1.81 tff(c_90, plain, (patricide('#skF_4') | ~relation('#skF_1', of, '#skF_3') | ~relation('#skF_3', of, '#skF_4') | ~parent('#skF_3') | ~patricide('#skF_3')), inference(superposition, [status(thm), theory('equality')], [c_86, c_38])).
% 3.27/1.81 tff(c_94, plain, (patricide('#skF_4')), inference(demodulation, [status(thm), theory('equality')], [c_49, c_18, c_47, c_45, c_90])).
% 3.27/1.81 tff(c_12, plain, (parent('#skF_4')), inference(cnfTransformation, [status(thm)], [f_63])).
% 3.27/1.81 tff(c_10, plain, (relation('#skF_4', of, Thersandros)), inference(cnfTransformation, [status(thm)], [f_63])).
% 3.27/1.81 tff(c_20, plain, (Iokaste='#skF_2'), inference(cnfTransformation, [status(thm)], [f_63])).
% 3.27/1.81 tff(c_41, plain, ('#skF_2'='#skF_1'), inference(demodulation, [status(thm), theory('equality')], [c_26, c_20])).
% 3.27/1.81 tff(c_22, plain, (relation('#skF_2', of, Polyneikes)), inference(cnfTransformation, [status(thm)], [f_63])).
% 3.27/1.81 tff(c_43, plain, (relation('#skF_1', of, Polyneikes)), inference(demodulation, [status(thm), theory('equality')], [c_41, c_22])).
% 3.27/1.81 tff(c_46, plain, (relation('#skF_1', of, '#skF_4')), inference(demodulation, [status(thm), theory('equality')], [c_8, c_43])).
% 3.27/1.81 tff(c_75, plain, (![D_11]: ('#skF_6'('#skF_1', '#skF_4', '#skF_4', D_11)=D_11 | ~relation('#skF_4', of, D_11) | ~parent('#skF_4') | ~patricide('#skF_4'))), inference(resolution, [status(thm)], [c_46, c_71])).
% 3.27/1.81 tff(c_81, plain, (![D_11]: ('#skF_6'('#skF_1', '#skF_4', '#skF_4', D_11)=D_11 | ~relation('#skF_4', of, D_11) | ~patricide('#skF_4'))), inference(demodulation, [status(thm), theory('equality')], [c_12, c_75])).
% 3.27/1.81 tff(c_98, plain, (![D_13]: ('#skF_6'('#skF_1', '#skF_4', '#skF_4', D_13)=D_13 | ~relation('#skF_4', of, D_13))), inference(demodulation, [status(thm), theory('equality')], [c_94, c_81])).
% 3.27/1.81 tff(c_102, plain, ('#skF_6'('#skF_1', '#skF_4', '#skF_4', Thersandros)=Thersandros), inference(resolution, [status(thm)], [c_10, c_98])).
% 3.27/1.81 tff(c_106, plain, (patricide(Thersandros) | ~relation('#skF_1', of, '#skF_4') | ~relation('#skF_4', of, Thersandros) | ~parent('#skF_4') | ~patricide('#skF_4')), inference(superposition, [status(thm), theory('equality')], [c_102, c_38])).
% 3.27/1.81 tff(c_110, plain, (patricide(Thersandros)), inference(demodulation, [status(thm), theory('equality')], [c_94, c_12, c_10, c_46, c_106])).
% 3.27/1.81 tff(c_112, plain, $false, inference(negUnitSimplification, [status(thm)], [c_2, c_110])).
% 3.27/1.81 % SZS output end CNFRefutation for /export/starexec/sandbox2/benchmark/theBenchmark.p
%------------------------------------------------------------------------------