%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : MSC009+1 : TPTP v9.0.0. Released v2.0.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 : n013.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:45:08 PM UTC 2025
% Result : Satisfiable 3.52s 1.95s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.01/0.11 % Problem : MSC009+1 : TPTP v9.0.0. Released v2.0.0.
% 0.11/0.12 % 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.33 % Computer : n013.cluster.edu
% 0.12/0.33 % Model : x86_64 x86_64
% 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.33 % Memory : 8042.1875MB
% 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.33 % CPULimit : 300
% 0.12/0.33 % WCLimit : 300
% 0.12/0.33 % DateTime : Tue Apr 8 07:58:17 EDT 2025
% 0.18/0.33 % CPUTime :
% 3.52/1.95
% 3.52/1.95 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.52/1.95
% 3.52/1.95 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.52/1.96 %$ sex > child > person > parent_with_sons_only > parent > mother > male > grandparent > female > father > #nlpp > #skF_5 > #skF_6 > #skF_2 > #skF_4 > #skF_1 > #skF_3
% 3.52/1.96
% 3.52/1.96 %Foreground sorts:
% 3.52/1.96
% 3.52/1.96
% 3.52/1.96 %Background operators:
% 3.52/1.96
% 3.52/1.96
% 3.52/1.96 %Foreground operators:
% 3.52/1.96 tff(mother, type, mother: $i > $o).
% 3.52/1.96 tff('#skF_5', type, '#skF_5': $i > $i).
% 3.52/1.96 tff('#skF_6', type, '#skF_6': ($i * $i) > $i).
% 3.52/1.96 tff(sex, type, sex: ($i * $i) > $o).
% 3.52/1.96 tff('#skF_2', type, '#skF_2': $i > $i).
% 3.52/1.96 tff('#skF_4', type, '#skF_4': $i > $i).
% 3.52/1.96 tff(parent_with_sons_only, type, parent_with_sons_only: $i > $o).
% 3.52/1.96 tff('#skF_1', type, '#skF_1': $i > $i).
% 3.52/1.96 tff(parent, type, parent: $i > $o).
% 3.52/1.96 tff(child, type, child: ($i * $i) > $o).
% 3.52/1.96 tff(female, type, female: $i > $o).
% 3.52/1.96 tff(father, type, father: $i > $o).
% 3.52/1.96 tff('#skF_3', type, '#skF_3': $i > $i).
% 3.52/1.96 tff(male, type, male: $i > $o).
% 3.52/1.96 tff(person, type, person: $i > $o).
% 3.52/1.96 tff(grandparent, type, grandparent: $i > $o).
% 3.52/1.96
% 3.52/1.96 %Saturated clause set:
% 3.52/1.96 tff(c_327, plain, (![X_93]: (parent_with_sons_only(X_93) | ~parent(X_93) | ~father('#skF_5'(X_93))))).
% 3.52/1.96 tff(c_308, plain, (![X_91]: (mother('#skF_5'(X_91)) | parent_with_sons_only(X_91) | ~parent(X_91) | ~grandparent('#skF_5'(X_91))))).
% 3.52/1.96 tff(c_296, plain, (![X_90]: (mother('#skF_5'(X_90)) | parent_with_sons_only(X_90) | ~parent(X_90) | ~parent('#skF_5'(X_90))))).
% 3.52/1.96 tff(c_281, plain, (![X_87, X_19]: (parent_with_sons_only(X_87) | ~parent(X_87) | ~child(X_19, '#skF_5'(X_87)) | ~parent_with_sons_only(X_19)))).
% 3.52/1.96 tff(c_262, plain, (![X_83]: (parent_with_sons_only(X_83) | ~parent(X_83) | ~person('#skF_5'(X_83)) | female('#skF_1'('#skF_5'(X_83)))))).
% 3.52/1.96 tff(c_208, plain, (![X_72]: (~male('#skF_3'('#skF_5'(X_72))) | parent_with_sons_only(X_72) | ~parent(X_72) | ~mother('#skF_5'(X_72))))).
% 3.52/1.96 tff(c_209, plain, (![X_72]: (~male('#skF_1'('#skF_5'(X_72))) | parent_with_sons_only(X_72) | ~parent(X_72) | ~person('#skF_5'(X_72))))).
% 3.52/1.96 tff(c_255, plain, (![X_15]: (person('#skF_4'(X_15)) | ~parent_with_sons_only(X_15) | ~grandparent(X_15)))).
% 3.52/1.96 tff(c_242, plain, (![Y_28, X_19]: (person(Y_28) | ~child(X_19, Y_28) | ~parent_with_sons_only(X_19)))).
% 3.52/1.96 tff(c_48, plain, (![Y_28, X_19]: (sex(Y_28, '#skF_6'(X_19, Y_28)) | ~child(X_19, Y_28) | ~parent_with_sons_only(X_19)))).
% 3.52/1.96 tff(c_195, plain, (![X_67]: (grandparent(X_67) | parent_with_sons_only(X_67) | ~parent(X_67) | ~grandparent('#skF_5'(X_67))))).
% 3.52/1.96 tff(c_194, plain, (![X_67]: (grandparent(X_67) | parent_with_sons_only(X_67) | ~parent(X_67) | ~mother('#skF_5'(X_67))))).
% 3.52/1.96 tff(c_50, plain, (![Z_27, X_19]: (~male(Z_27) | ~sex('#skF_5'(X_19), Z_27) | parent_with_sons_only(X_19) | ~parent(X_19)))).
% 3.52/1.96 tff(c_183, plain, (![X_65, Y_66]: (~female('#skF_6'(X_65, Y_66)) | ~child(X_65, Y_66) | ~parent_with_sons_only(X_65)))).
% 3.52/1.96 tff(c_132, plain, (![X_2]: (mother(X_2) | ~female('#skF_1'(X_2)) | ~parent(X_2) | ~person(X_2)))).
% 3.52/1.96 tff(c_143, plain, (![X_19]: (grandparent(X_19) | ~parent('#skF_5'(X_19)) | parent_with_sons_only(X_19) | ~parent(X_19)))).
% 3.52/1.96 tff(c_46, plain, (![X_19, Y_28]: (male('#skF_6'(X_19, Y_28)) | ~child(X_19, Y_28) | ~parent_with_sons_only(X_19)))).
% 3.52/1.96 tff(c_158, plain, (![X_59]: (grandparent(X_59) | ~parent(X_59) | ~father('#skF_2'(X_59))))).
% 3.52/1.96 tff(c_14, plain, (![X_6, Y_9]: (parent(X_6) | ~person(Y_9) | ~child(X_6, Y_9) | ~person(X_6)))).
% 3.52/1.96 tff(c_157, plain, (![X_59]: (grandparent(X_59) | ~parent(X_59) | ~grandparent('#skF_2'(X_59))))).
% 3.52/1.96 tff(c_156, plain, (![X_59]: (grandparent(X_59) | ~parent(X_59) | ~mother('#skF_2'(X_59))))).
% 3.52/1.97 tff(c_145, plain, (![X_6]: (grandparent(X_6) | ~parent('#skF_2'(X_6)) | ~parent(X_6)))).
% 3.52/1.97 tff(c_36, plain, (![X_15, Y_18]: (grandparent(X_15) | ~parent(Y_18) | ~child(X_15, Y_18) | ~parent(X_15)))).
% 3.52/1.97 tff(c_22, plain, (![X_10, Y_13]: (mother(X_10) | ~female(Y_13) | ~sex(X_10, Y_13) | ~parent(X_10)))).
% 3.52/1.97 tff(c_81, plain, (![X_15]: (father('#skF_4'(X_15)) | mother('#skF_4'(X_15)) | ~grandparent(X_15)))).
% 3.52/1.97 tff(c_117, plain, (![X_10]: (person(X_10) | ~mother(X_10)))).
% 3.52/1.97 tff(c_52, plain, (![X_19]: (child(X_19, '#skF_5'(X_19)) | parent_with_sons_only(X_19) | ~parent(X_19)))).
% 3.52/1.97 tff(c_12, plain, (![Y_5, X_2]: (~male(Y_5) | person(X_2) | ~sex(X_2, Y_5)))).
% 3.52/1.97 tff(c_10, plain, (![Y_5, X_2]: (~female(Y_5) | person(X_2) | ~sex(X_2, Y_5)))).
% 3.52/1.97 tff(c_83, plain, (![X_15]: (father(X_15) | mother(X_15) | ~grandparent(X_15)))).
% 3.52/1.97 tff(c_40, plain, (![X_15]: (child(X_15, '#skF_4'(X_15)) | ~grandparent(X_15)))).
% 3.52/1.97 tff(c_26, plain, (![X_10]: (sex(X_10, '#skF_3'(X_10)) | ~mother(X_10)))).
% 3.52/1.97 tff(c_8, plain, (![X_2]: (sex(X_2, '#skF_1'(X_2)) | ~person(X_2)))).
% 3.52/1.97 tff(c_18, plain, (![X_6]: (child(X_6, '#skF_2'(X_6)) | ~parent(X_6)))).
% 3.52/1.97 tff(c_30, plain, (![X_14]: (father(X_14) | mother(X_14) | ~parent(X_14)))).
% 3.52/1.97 tff(c_24, plain, (![X_10]: (female('#skF_3'(X_10)) | ~mother(X_10)))).
% 3.52/1.97 tff(c_16, plain, (![X_6]: (person('#skF_2'(X_6)) | ~parent(X_6)))).
% 3.52/1.97 tff(c_38, plain, (![X_15]: (parent('#skF_4'(X_15)) | ~grandparent(X_15)))).
% 3.52/1.97 tff(c_28, plain, (![X_10]: (parent(X_10) | ~mother(X_10)))).
% 3.52/1.97 tff(c_4, plain, (![X_1]: (female(X_1) | male(X_1)))).
% 3.52/1.97 tff(c_42, plain, (![X_15]: (parent(X_15) | ~grandparent(X_15)))).
% 3.52/1.97 tff(c_32, plain, (![X_14]: (~mother(X_14) | ~father(X_14)))).
% 3.52/1.97 tff(c_20, plain, (![X_6]: (person(X_6) | ~parent(X_6)))).
% 3.52/1.97 tff(c_34, plain, (![X_14]: (parent(X_14) | ~father(X_14)))).
% 3.52/1.97 tff(c_2, plain, (![X_1]: (~male(X_1) | ~female(X_1)))).
% 3.52/1.97 tff(c_44, plain, (![X_19]: (parent(X_19) | ~parent_with_sons_only(X_19)))).
% 3.52/1.97 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 3.52/1.97
%------------------------------------------------------------------------------