%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : MSC009-1 : TPTP v9.0.0. Released v1.2.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 : n017.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.59s 1.94s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.12 % Problem : MSC009-1 : TPTP v9.0.0. Released v1.2.0. % 0.02/0.13 % 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.14/0.34 % Computer : n017.cluster.edu % 0.14/0.34 % Model : x86_64 x86_64 % 0.14/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.34 % Memory : 8042.1875MB % 0.14/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.34 % CPULimit : 300 % 0.14/0.34 % WCLimit : 300 % 0.14/0.34 % DateTime : Tue Apr 8 07:56:55 EDT 2025 % 0.14/0.34 % CPUTime : % 3.59/1.94 % 3.59/1.94 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.59/1.94 % 3.59/1.94 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.59/1.95 %$ sex > child > person > parent_with_sons_only > parent > mother > male > grandparent > female > father > child_with_parent > #nlpp > sex_of3 > sex_of2 > sex_of1 > female_child_of > child_of2 > child_of1 % 3.59/1.95 % 3.59/1.95 %Foreground sorts: % 3.59/1.95 % 3.59/1.95 % 3.59/1.95 %Background operators: % 3.59/1.95 % 3.59/1.95 % 3.59/1.95 %Foreground operators: % 3.59/1.95 tff(mother, type, mother: $i > $o). % 3.59/1.95 tff(sex, type, sex: ($i * $i) > $o). % 3.59/1.95 tff(child_of2, type, child_of2: $i > $i). % 3.59/1.95 tff(parent_with_sons_only, type, parent_with_sons_only: $i > $o). % 3.59/1.95 tff(parent, type, parent: $i > $o). % 3.59/1.95 tff(child, type, child: ($i * $i) > $o). % 3.59/1.95 tff(child_with_parent, type, child_with_parent: $i > $o). % 3.59/1.95 tff(female, type, female: $i > $o). % 3.59/1.95 tff(sex_of2, type, sex_of2: $i > $i). % 3.59/1.95 tff(father, type, father: $i > $o). % 3.59/1.95 tff(sex_of1, type, sex_of1: $i > $i). % 3.59/1.95 tff(child_of1, type, child_of1: $i > $i). % 3.59/1.95 tff(sex_of3, type, sex_of3: $i > $i). % 3.59/1.95 tff(male, type, male: $i > $o). % 3.59/1.95 tff(person, type, person: $i > $o). % 3.59/1.95 tff(female_child_of, type, female_child_of: $i > $i). % 3.59/1.95 tff(grandparent, type, grandparent: $i > $o). % 3.59/1.95 % 3.59/1.95 %Saturated clause set: % 3.59/1.95 tff(c_331, plain, (![X_94]: (grandparent(X_94) | parent_with_sons_only(X_94) | ~parent(X_94) | ~mother(female_child_of(X_94))))). % 3.59/1.95 tff(c_332, plain, (![X_94]: (grandparent(X_94) | parent_with_sons_only(X_94) | ~parent(X_94) | ~grandparent(female_child_of(X_94))))). % 3.59/1.95 tff(c_330, plain, (![X_94]: (grandparent(X_94) | parent_with_sons_only(X_94) | ~parent(X_94) | ~father(female_child_of(X_94))))). % 3.59/1.95 tff(c_180, plain, (![X_30]: (grandparent(X_30) | ~parent(female_child_of(X_30)) | parent_with_sons_only(X_30) | ~parent(X_30)))). % 3.59/1.95 tff(c_292, plain, (![X_24]: (mother(child_of2(X_24)) | child_with_parent(child_of2(X_24)) | ~grandparent(X_24)))). % 3.59/1.95 tff(c_295, plain, (![X_22]: (mother(X_22) | child_with_parent(X_22) | ~grandparent(X_22)))). % 3.59/1.95 tff(c_304, plain, (![X_90]: (child_with_parent(X_90) | ~father(X_90)))). % 3.59/1.95 tff(c_278, plain, (![X_9]: (mother(X_9) | child_with_parent(X_9) | ~parent(X_9)))). % 3.59/1.95 tff(c_242, plain, (![X_3]: (mother(X_3) | ~female(sex_of1(X_3)) | ~parent(X_3) | ~person(X_3)))). % 3.59/1.96 tff(c_91, plain, (![X_24]: (father(child_of2(X_24)) | mother(child_of2(X_24)) | ~grandparent(X_24)))). % 3.59/1.96 tff(c_204, plain, (![X_73]: (grandparent(X_73) | ~parent(X_73) | ~mother(child_of1(X_73))))). % 3.59/1.96 tff(c_205, plain, (![X_73]: (grandparent(X_73) | ~parent(X_73) | ~grandparent(child_of1(X_73))))). % 3.59/1.96 tff(c_203, plain, (![X_73]: (grandparent(X_73) | ~parent(X_73) | ~father(child_of1(X_73))))). % 3.59/1.96 tff(c_28, plain, (![X_17, Y_18]: (mother(X_17) | ~female(Y_18) | ~sex(X_17, Y_18) | ~parent(X_17)))). % 3.59/1.96 tff(c_187, plain, (![X_71]: (child_with_parent(X_71) | ~person(X_71) | female(sex_of1(X_71))))). % 3.59/1.96 tff(c_126, plain, (![X_23]: (child_with_parent(child_of2(X_23)) | ~parent_with_sons_only(X_23) | ~grandparent(X_23)))). % 3.59/1.96 tff(c_125, plain, (![X_10]: (child_with_parent(child_of1(X_10)) | ~parent_with_sons_only(X_10) | ~parent(X_10)))). % 3.59/1.96 tff(c_20, plain, (![X_12, Y_13]: (parent(X_12) | ~person(Y_13) | ~child(X_12, Y_13) | ~person(X_12)))). % 3.59/1.96 tff(c_213, plain, (![Y_33]: (person(Y_33) | ~child_with_parent(Y_33)))). % 3.59/1.96 tff(c_181, plain, (![X_10]: (grandparent(X_10) | ~parent(child_of1(X_10)) | ~parent(X_10)))). % 3.59/1.96 tff(c_152, plain, (![X_15]: (child_with_parent(X_15) | ~male(sex_of2(X_15)) | ~mother(X_15)))). % 3.59/1.96 tff(c_151, plain, (![X_3]: (child_with_parent(X_3) | ~male(sex_of1(X_3)) | ~person(X_3)))). % 3.59/1.96 tff(c_42, plain, (![X_25, Y_26]: (grandparent(X_25) | ~parent(Y_26) | ~child(X_25, Y_26) | ~parent(X_25)))). % 3.59/1.96 tff(c_168, plain, (![X_16]: (person(X_16) | ~mother(X_16)))). % 3.59/1.96 tff(c_48, plain, (![X_30]: (parent_with_sons_only(X_30) | child(X_30, female_child_of(X_30)) | ~parent(X_30)))). % 3.59/1.96 tff(c_56, plain, (![Y_34, Z_35]: (child_with_parent(Y_34) | ~male(Z_35) | ~sex(Y_34, Z_35)))). % 3.59/1.96 tff(c_10, plain, (![X_5, Y_6]: (person(X_5) | ~male(Y_6) | ~sex(X_5, Y_6)))). % 3.59/1.96 tff(c_50, plain, (![X_31]: (parent_with_sons_only(X_31) | ~child_with_parent(female_child_of(X_31)) | ~parent(X_31)))). % 3.59/1.96 tff(c_46, plain, (![Y_29, X_28]: (child_with_parent(Y_29) | ~child(X_28, Y_29) | ~parent_with_sons_only(X_28)))). % 3.59/1.96 tff(c_94, plain, (![X_22]: (father(X_22) | mother(X_22) | ~grandparent(X_22)))). % 3.59/1.96 tff(c_12, plain, (![X_7, Y_8]: (person(X_7) | ~female(Y_8) | ~sex(X_7, Y_8)))). % 3.59/1.96 tff(c_16, plain, (![X_10]: (child(X_10, child_of1(X_10)) | ~parent(X_10)))). % 3.59/1.96 tff(c_6, plain, (![X_3]: (sex(X_3, sex_of1(X_3)) | ~person(X_3)))). % 3.59/1.96 tff(c_24, plain, (![X_15]: (sex(X_15, sex_of2(X_15)) | ~mother(X_15)))). % 3.59/1.96 tff(c_52, plain, (![Y_32]: (sex(Y_32, sex_of3(Y_32)) | ~child_with_parent(Y_32)))). % 3.59/1.96 tff(c_38, plain, (![X_23]: (child(X_23, child_of2(X_23)) | ~grandparent(X_23)))). % 3.59/1.96 tff(c_34, plain, (![X_21]: (father(X_21) | mother(X_21) | ~parent(X_21)))). % 3.59/1.96 tff(c_75, plain, (![Y_46]: (~female(sex_of3(Y_46)) | ~child_with_parent(Y_46)))). % 3.59/1.96 tff(c_26, plain, (![X_16]: (female(sex_of2(X_16)) | ~mother(X_16)))). % 3.59/1.96 tff(c_54, plain, (![Y_33]: (male(sex_of3(Y_33)) | ~child_with_parent(Y_33)))). % 3.59/1.96 tff(c_18, plain, (![X_11]: (person(child_of1(X_11)) | ~parent(X_11)))). % 3.59/1.96 tff(c_40, plain, (![X_24]: (parent(child_of2(X_24)) | ~grandparent(X_24)))). % 3.59/1.96 tff(c_2, plain, (![X_1]: (~male(X_1) | ~female(X_1)))). % 3.59/1.96 tff(c_30, plain, (![X_19]: (parent(X_19) | ~father(X_19)))). % 3.59/1.96 tff(c_4, plain, (![X_2]: (female(X_2) | male(X_2)))). % 3.59/1.96 tff(c_32, plain, (![X_20]: (~mother(X_20) | ~father(X_20)))). % 3.59/1.96 tff(c_14, plain, (![X_9]: (person(X_9) | ~parent(X_9)))). % 3.59/1.96 tff(c_22, plain, (![X_14]: (parent(X_14) | ~mother(X_14)))). % 3.59/1.96 tff(c_36, plain, (![X_22]: (parent(X_22) | ~grandparent(X_22)))). % 3.59/1.96 tff(c_44, plain, (![X_27]: (parent(X_27) | ~parent_with_sons_only(X_27)))). % 3.59/1.96 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 3.59/1.96 %------------------------------------------------------------------------------