%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : PUZ163_1 : TPTP v9.3.0. Released v9.3.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 : n001.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 : Tue May 5 06:48:51 PM UTC 2026 % Result : Satisfiable 8.74s 3.10s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : PUZ163_1 : TPTP v9.3.0. Released v9.3.0. % 0.00/0.12 % 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.16/0.33 % Computer : n001.cluster.edu % 0.16/0.33 % Model : x86_64 x86_64 % 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.16/0.33 % Memory : 8042.1875MB % 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.16/0.34 % CPULimit : 300 % 0.16/0.34 % WCLimit : 300 % 0.16/0.34 % DateTime : Tue May 5 05:04:18 EDT 2026 % 0.16/0.34 % CPUTime : % 8.74/3.10 % 8.74/3.10 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.74/3.11 % 8.74/3.11 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 8.74/3.11 %$ married > malecouple > femalecouple > #nlpp > watson > shearer > russell > peter > parker > mildred > marcia > joyce > johnstone > graves > everett > elizabeth > elaine > douglas > charles % 8.74/3.11 % 8.74/3.11 %Foreground sorts: % 8.74/3.11 tff(person, type, person: $tType ). % 8.74/3.11 % 8.74/3.11 %Background operators: % 8.74/3.11 tff(npjohnstone, type, npjohnstone: $int). % 8.74/3.11 tff(npshearer, type, npshearer: $int). % 8.74/3.11 tff(npgraves, type, npgraves: $int). % 8.74/3.11 tff(npparker, type, npparker: $int). % 8.74/3.11 tff(npwatson, type, npwatson: $int). % 8.74/3.11 % 8.74/3.11 %Foreground operators: % 8.74/3.11 tff(mildred, type, mildred: person). % 8.74/3.11 tff(femalecouple, type, femalecouple: (person * person) > $o). % 8.74/3.11 tff(douglas, type, douglas: person). % 8.74/3.11 tff(marcia, type, marcia: person). % 8.74/3.11 tff(peter, type, peter: person). % 8.74/3.11 tff(charles, type, charles: person). % 8.74/3.11 tff(shearer, type, shearer: person). % 8.74/3.11 tff(johnstone, type, johnstone: person). % 8.74/3.11 tff(russell, type, russell: person). % 8.74/3.11 tff(malecouple, type, malecouple: (person * person) > $o). % 8.74/3.11 tff(married, type, married: (person * $int) > $o). % 8.74/3.11 tff(elaine, type, elaine: person). % 8.74/3.11 tff(elizabeth, type, elizabeth: person). % 8.74/3.11 tff(parker, type, parker: person). % 8.74/3.11 tff(graves, type, graves: person). % 8.74/3.11 tff(everett, type, everett: person). % 8.74/3.11 tff(joyce, type, joyce: person). % 8.74/3.11 tff(watson, type, watson: person). % 8.74/3.11 % 8.74/3.11 %Saturated clause set: % 8.74/3.11 tff(c_1737, plain, (~femalecouple(elaine, parker))). % 9.19/3.11 tff(c_1689, plain, (![X1_274:person, M6_275a:$int]: (~married(X1_274, M6_275a) | ~femalecouple(elaine, X1_274) | $less(npjohnstone, M6_275a) | $less(npparker, M6_275a) | $less(npwatson, M6_275a) | $less(npshearer, M6_275a) | $less(30, M6_275a)))). % 9.19/3.11 tff(c_1680, plain, (![M5_269a:$int, X1_271:person, M6_272a:$int]: (~married(graves, M5_269a) | ~married(X1_271, M6_272a) | ~femalecouple(elaine, X1_271) | $less(npjohnstone, M6_272a) | $less(npparker, M6_272a) | $less(npwatson, M6_272a) | $less(npshearer, M6_272a) | $less(M5_269a, M6_272a)))). % 9.19/3.12 tff(c_1671, plain, (![M5_265a:$int, M1_264a:$int, X1_266:person, M6_268a:$int]: (~married(graves, M5_265a) | ~married(johnstone, M1_264a) | ~married(X1_266, M6_268a) | ~femalecouple(elaine, X1_266) | $less(M1_264a, M6_268a) | $less(npparker, M6_268a) | $less(npwatson, M6_268a) | $less(npshearer, M6_268a) | $less(M5_265a, M6_268a)))). % 9.19/3.12 tff(c_1662, plain, (![M1_259a:$int, M6_260a:$int, M2_258a:$int, X1_263:person, M5_261a:$int]: (~married(graves, M5_261a) | ~married(parker, M2_258a) | ~married(johnstone, M1_259a) | ~married(X1_263, M6_260a) | ~femalecouple(elaine, X1_263) | $less(M1_259a, M6_260a) | $less(M2_258a, M6_260a) | $less(npwatson, M6_260a) | $less(npshearer, M6_260a) | $less(M5_261a, M6_260a)))). % 9.19/3.12 tff(c_315, plain, (![X1_105:person, M2_102a:$int, M4_107a:$int, M5_103a:$int, M6_101a:$int, M1_104a:$int]: (~married(graves, M5_103a) | ~married(shearer, M4_107a) | ~married(parker, M2_102a) | ~married(johnstone, M1_104a) | ~married(X1_105, M6_101a) | ~femalecouple(elaine, X1_105) | $less(M1_104a, M6_101a) | $less(M2_102a, M6_101a) | $less(npwatson, M6_101a) | $less(M4_107a, M6_101a) | $less(M5_103a, M6_101a)))). % 9.19/3.12 tff(c_1648, plain, (![X1_54:person]: (~malecouple(douglas, X1_54) | ~malecouple(everett, X1_54)))). % 9.19/3.12 tff(c_1647, plain, (~malecouple(douglas, graves))). % 9.19/3.12 tff(c_1646, plain, (~femalecouple(mildred, watson))). % 9.19/3.12 tff(c_1642, plain, (~malecouple(douglas, watson))). % 9.19/3.12 tff(c_1641, plain, (~femalecouple(mildred, johnstone))). % 9.19/3.12 tff(c_1637, plain, (~malecouple(douglas, johnstone))). % 9.19/3.12 tff(c_1632, plain, (~malecouple(douglas, parker))). % 9.19/3.12 tff(c_1631, plain, (~femalecouple(mildred, shearer))). % 9.19/3.12 tff(c_1627, plain, (~malecouple(douglas, shearer))). % 9.19/3.12 tff(c_1600, plain, (![X1_54:person]: (~malecouple(charles, X1_54) | ~malecouple(everett, X1_54)))). % 9.19/3.12 tff(c_1594, plain, (![X3_18:person, M5_23a:$int, X1_16:person, M1_19a:$int, M4_22a:$int]: (~married(X3_18, M4_22a) | ~malecouple(douglas, X3_18) | ~married(johnstone, M5_23a) | ~married(X1_16, M1_19a) | ~femalecouple(joyce, X1_16) | ~$less(M1_19a, M5_23a) | ~$less(M1_19a, M4_22a)))). % 9.19/3.12 tff(c_1597, plain, (~malecouple(charles, graves))). % 9.19/3.12 tff(c_1596, plain, (~malecouple(charles, watson))). % 9.19/3.12 tff(c_1595, plain, (~malecouple(charles, johnstone))). % 9.19/3.12 tff(c_1592, plain, (~malecouple(charles, shearer))). % 9.19/3.12 tff(c_1588, plain, (![X1_54:person]: (~femalecouple(joyce, X1_54) | ~malecouple(everett, X1_54)))). % 9.19/3.12 tff(c_1590, plain, ($less(npparker, 25))). % 9.19/3.12 tff(c_1559, plain, ($less(npparker, 30))). % 9.19/3.12 tff(c_1557, plain, (~femalecouple(joyce, graves))). % 9.19/3.12 tff(c_1545, plain, (![X2_17:person, M2_20a:$int, X1_16:person, M1_19a:$int]: (~married(X2_17, M2_20a) | ~malecouple(charles, X2_17) | ~married(X1_16, M1_19a) | ~femalecouple(joyce, X1_16) | ~$less(M2_20a, M1_19a)))). % 9.19/3.12 tff(c_1551, plain, (~femalecouple(joyce, watson))). % 9.19/3.12 tff(c_1553, plain, ($less(npparker, npwatson))). % 9.19/3.12 tff(c_1541, plain, (~femalecouple(joyce, johnstone))). % 9.19/3.12 tff(c_1543, plain, ($less(npparker, npjohnstone))). % 9.19/3.12 tff(c_1535, plain, (~femalecouple(joyce, shearer))). % 9.19/3.12 tff(c_1537, plain, ($less(npparker, npshearer))). % 9.19/3.12 tff(c_1497, plain, (![X1_242:person, M1_243a:$int]: (~married(X1_242, M1_243a) | ~femalecouple(joyce, X1_242) | ~$less(npparker, M1_243a)))). % 9.19/3.12 tff(c_1488, plain, (![M3_21a:$int, X1_16:person, M1_19a:$int]: (~married(parker, M3_21a) | ~married(X1_16, M1_19a) | ~femalecouple(joyce, X1_16) | ~$less(M3_21a, M1_19a)))). % 9.19/3.12 tff(c_1475, plain, (![M5_236a:$int, M1_238a:$int]: (~married(graves, M5_236a) | ~married(johnstone, M1_238a) | $less(npparker, M1_238a) | $less(npwatson, M1_238a) | $less(npshearer, M1_238a) | $less(M5_236a, M1_238a)))). % 9.19/3.12 tff(c_1463, plain, (![M5_231a:$int, M2_233a:$int, M1_234a:$int]: (~married(graves, M5_231a) | ~married(parker, M2_233a) | ~married(johnstone, M1_234a) | $less(M2_233a, M1_234a) | $less(npwatson, M1_234a) | $less(npshearer, M1_234a) | $less(M5_231a, M1_234a)))). % 9.19/3.12 tff(c_1452, plain, (![X1_54:person]: (~malecouple(peter, X1_54) | ~malecouple(everett, X1_54)))). % 9.19/3.12 tff(c_289, plain, (![M5_92a:$int, M4_94a:$int, M2_95a:$int, M1_93a:$int]: (~married(graves, M5_92a) | ~married(shearer, M4_94a) | ~married(parker, M2_95a) | ~married(johnstone, M1_93a) | $less(M2_95a, M1_93a) | $less(npwatson, M1_93a) | $less(M4_94a, M1_93a) | $less(M5_92a, M1_93a)))). % 9.19/3.12 tff(c_1429, plain, (~malecouple(peter, parker))). % 9.19/3.12 tff(c_1424, plain, (![X2_30:person, M2_32a:$int, M3_33a:$int]: (~married(X2_30, M2_32a) | ~malecouple(peter, X2_30) | ~married(shearer, M3_33a) | ~$less($sum(10, M2_32a), M3_33a)))). % 9.19/3.12 tff(c_1428, plain, (~malecouple(peter, johnstone))). % 9.19/3.12 tff(c_1427, plain, (~malecouple(peter, watson))). % 9.19/3.12 tff(c_1426, plain, (~malecouple(peter, shearer))). % 9.19/3.12 tff(c_1425, plain, (~malecouple(peter, graves))). % 9.19/3.12 tff(c_1386, plain, (![X2_30:person, M2_32a:$int, M3_33a:$int]: (~married(X2_30, M2_32a) | ~malecouple(peter, X2_30) | ~married(shearer, M3_33a) | ~$less(M3_33a, $sum(10, M2_32a))))). % 9.19/3.12 tff(c_1392, plain, (![X1_54:person]: (~femalecouple(marcia, X1_54) | ~malecouple(everett, X1_54)))). % 9.19/3.12 tff(c_1394, plain, ($less(npshearer, 15))). % 9.19/3.12 tff(c_1384, plain, ($less(npshearer, 20))). % 9.19/3.12 tff(c_1382, plain, (~femalecouple(marcia, graves))). % 9.19/3.12 tff(c_1348, plain, ($less(npjohnstone, $sum(10, npshearer)))). % 9.19/3.12 tff(c_1346, plain, (~femalecouple(marcia, johnstone))). % 9.19/3.12 tff(c_1342, plain, (![X1_220:person, M1_221a:$int]: (~married(X1_220, M1_221a) | ~femalecouple(marcia, X1_220) | ~$less($sum(10, npshearer), M1_221a)))). % 9.19/3.12 tff(c_1327, plain, ($less(npparker, $sum(10, npshearer)))). % 9.19/3.12 tff(c_1321, plain, (![M3_33a:$int, X1_29:person, M1_31a:$int]: (~married(shearer, M3_33a) | ~married(X1_29, M1_31a) | ~femalecouple(marcia, X1_29) | ~$less($sum(10, M3_33a), M1_31a)))). % 9.19/3.12 tff(c_1333, plain, ($less(npwatson, $sum(10, npshearer)))). % 9.19/3.12 tff(c_1331, plain, (~femalecouple(marcia, watson))). % 9.19/3.12 tff(c_1325, plain, (~femalecouple(marcia, parker))). % 9.19/3.12 tff(c_1319, plain, (~$less(20, npshearer))). % 9.19/3.12 tff(c_1308, plain, (~femalecouple(marcia, shearer))). % 9.19/3.12 tff(c_1283, plain, (![X1_215:person, M1_216a:$int]: (~married(X1_215, M1_216a) | ~femalecouple(marcia, X1_215) | ~$less(M1_216a, $sum(10, npshearer))))). % 9.19/3.12 tff(c_1273, plain, (![M3_33a:$int, X1_29:person, M1_31a:$int]: (~married(shearer, M3_33a) | ~married(X1_29, M1_31a) | ~femalecouple(marcia, X1_29) | ~$less(M1_31a, $sum(10, M3_33a))))). % 9.19/3.12 tff(c_1271, plain, (![X1_54:person]: (~malecouple(russell, X1_54) | ~malecouple(everett, X1_54)))). % 9.19/3.12 tff(c_1248, plain, (~malecouple(russell, watson))). % 9.19/3.13 tff(c_1243, plain, (![X2_25:person, M2_27a:$int, X1_24:person, M1_26a:$int]: (~married(X2_25, M2_27a) | ~malecouple(russell, X2_25) | ~married(X1_24, M1_26a) | ~femalecouple(elizabeth, X1_24) | ~$less(M2_27a, $product(2, M1_26a))))). % 9.19/3.13 tff(c_1247, plain, (~malecouple(russell, shearer))). % 9.19/3.13 tff(c_1246, plain, (~malecouple(russell, johnstone))). % 9.19/3.13 tff(c_1245, plain, (~malecouple(russell, parker))). % 9.19/3.13 tff(c_1244, plain, (~malecouple(russell, graves))). % 9.19/3.13 tff(c_1202, plain, (![X2_25:person, M2_27a:$int, X1_24:person, M1_26a:$int]: (~married(X2_25, M2_27a) | ~malecouple(russell, X2_25) | ~married(X1_24, M1_26a) | ~femalecouple(elizabeth, X1_24) | ~$less($product(2, M1_26a), M2_27a)))). % 9.19/3.13 tff(c_1214, plain, ($less(npshearer, $product(2, npwatson)))). % 9.19/3.13 tff(c_1208, plain, ($less(npjohnstone, $product(2, npwatson)))). % 9.19/3.13 tff(c_1212, plain, (~femalecouple(elizabeth, shearer))). % 9.19/3.13 tff(c_1206, plain, (~femalecouple(elizabeth, johnstone))). % 9.19/3.13 tff(c_1200, plain, ($less(npparker, $product(2, npwatson)))). % 9.19/3.13 tff(c_1198, plain, (~femalecouple(elizabeth, parker))). % 9.19/3.13 tff(c_1193, plain, (~femalecouple(elizabeth, watson))). % 9.19/3.13 tff(c_1159, plain, (![X1_201:person, M1_202a:$int]: (~married(X1_201, M1_202a) | ~femalecouple(elizabeth, X1_201) | ~$less(M1_202a, $product(2, npwatson))))). % 9.19/3.13 tff(c_1139, plain, (![M3_28a:$int, X1_24:person, M1_26a:$int]: (~married(watson, M3_28a) | ~married(X1_24, M1_26a) | ~femalecouple(elizabeth, X1_24) | ~$less(M1_26a, $product(2, M3_28a))))). % 9.19/3.13 tff(c_1147, plain, (![X1_54:person]: (~femalecouple(elizabeth, X1_54) | ~malecouple(everett, X1_54)))). % 9.19/3.13 tff(c_1149, plain, ($less(npwatson, 13))). % 9.19/3.13 tff(c_1143, plain, (~$less($product(2, npwatson), npshearer))). % 9.19/3.13 tff(c_1141, plain, (~$less($product(2, npwatson), npjohnstone))). % 9.19/3.13 tff(c_1137, plain, ($less(npwatson, 15))). % 9.19/3.13 tff(c_1135, plain, (~femalecouple(elizabeth, graves))). % 9.19/3.13 tff(c_1130, plain, (~$less($product(2, npwatson), npparker))). % 9.19/3.13 tff(c_1094, plain, (![X1_195:person, M1_196a:$int]: (~married(X1_195, M1_196a) | ~femalecouple(elizabeth, X1_195) | ~$less($product(2, npwatson), M1_196a)))). % 9.19/3.13 tff(c_1085, plain, (![M3_28a:$int, X1_24:person, M1_26a:$int]: (~married(watson, M3_28a) | ~married(X1_24, M1_26a) | ~femalecouple(elizabeth, X1_24) | ~$less($product(2, M3_28a), M1_26a)))). % 9.19/3.13 tff(c_1083, plain, (~$less(30, npjohnstone))). % 9.19/3.13 tff(c_1072, plain, (![M1_38a:$int]: (~married(johnstone, M1_38a) | ~$less(30, M1_38a)))). % 9.19/3.13 tff(c_1070, plain, (~$less(30, npshearer))). % 9.19/3.13 tff(c_1059, plain, (![M4_41a:$int]: (~married(shearer, M4_41a) | ~$less(30, M4_41a)))). % 9.19/3.13 tff(c_1057, plain, (~$less(30, npparker))). % 9.19/3.13 tff(c_1046, plain, (![M2_39a:$int]: (~married(parker, M2_39a) | ~$less(30, M2_39a)))). % 9.19/3.13 tff(c_1044, plain, (~$less(30, npwatson))). % 9.19/3.13 tff(c_350, plain, (![M3_40a:$int]: (~married(watson, M3_40a) | ~$less(30, M3_40a)))). % 9.19/3.13 tff(c_1033, plain, (~$less(npjohnstone, 5))). % 9.19/3.13 tff(c_1031, plain, ($less(npparker, 5))). % 9.19/3.13 tff(c_1029, plain, (~femalecouple(mildred, parker))). % 9.19/3.13 tff(c_348, plain, (~$less(npwatson, 5))). % 9.19/3.13 tff(c_346, plain, (~$less(npshearer, 5))). % 9.19/3.13 tff(c_304, plain, (![X1_99:person, M1_100a:$int]: (~married(X1_99, M1_100a) | ~femalecouple(mildred, X1_99) | ~$less(M1_100a, 5)))). % 9.19/3.13 tff(c_79, plain, (![M3_50a:$int, M1_48a:$int, M5_52a:$int, M6_53a:$int, M2_49a:$int, M4_51a:$int, X1_47:person]: (~married(graves, M5_52a) | ~married(shearer, M4_51a) | ~married(watson, M3_50a) | ~married(parker, M2_49a) | ~married(johnstone, M1_48a) | ~married(X1_47, M6_53a) | ~femalecouple(elaine, X1_47) | $less(M1_48a, M6_53a) | $less(M2_49a, M6_53a) | $less(M3_50a, M6_53a) | $less(M4_51a, M6_53a) | $less(M5_52a, M6_53a)))). % 9.19/3.13 tff(c_306, plain, (~$less(5, npwatson))). % 9.19/3.13 tff(c_294, plain, (~$less(5, npparker))). % 9.19/3.13 tff(c_87, plain, (![M2_37a:$int, X1_35:person, M1_36a:$int]: (~married(graves, M2_37a) | ~married(X1_35, M1_36a) | ~femalecouple(mildred, X1_35) | ~$less($sum(25, M1_36a), M2_37a)))). % 9.19/3.13 tff(c_292, plain, (~$less(5, npjohnstone))). % 9.19/3.13 tff(c_265, plain, (![X1_54:person]: (~femalecouple(mildred, X1_54) | ~malecouple(everett, X1_54)))). % 9.19/3.13 tff(c_278, plain, (~$less(5, npshearer))). % 9.19/3.13 tff(c_80, plain, (![M3_44a:$int, M4_45a:$int, M1_42a:$int, M5_46a:$int, M2_43a:$int]: (~married(graves, M5_46a) | ~married(shearer, M4_45a) | ~married(watson, M3_44a) | ~married(parker, M2_43a) | ~married(johnstone, M1_42a) | $less(M2_43a, M1_42a) | $less(M3_44a, M1_42a) | $less(M4_45a, M1_42a) | $less(M5_46a, M1_42a)))). % 9.19/3.13 tff(c_276, plain, (~femalecouple(mildred, graves))). % 9.19/3.13 tff(c_243, plain, (![X1_88:person, M1_89a:$int]: (~married(X1_88, M1_89a) | ~femalecouple(mildred, X1_88) | ~$less(5, M1_89a)))). % 9.19/3.13 tff(c_86, plain, (![M2_37a:$int, X1_35:person, M1_36a:$int]: (~married(graves, M2_37a) | ~married(X1_35, M1_36a) | ~femalecouple(mildred, X1_35) | ~$less(M2_37a, $sum(25, M1_36a))))). % 9.19/3.13 tff(c_20, plain, (![C_10:person]: (shearer=C_10 | graves=C_10 | watson=C_10 | parker=C_10 | johnstone=C_10 | ~femalecouple(mildred, C_10)))). % 9.19/3.13 tff(c_12, plain, (![C_6:person]: (shearer=C_6 | graves=C_6 | watson=C_6 | parker=C_6 | johnstone=C_6 | ~femalecouple(elaine, C_6)))). % 9.19/3.13 tff(c_4, plain, (![C_2:person]: (shearer=C_2 | graves=C_2 | watson=C_2 | parker=C_2 | johnstone=C_2 | ~malecouple(douglas, C_2)))). % 9.19/3.13 tff(c_14, plain, (![C_7:person]: (shearer=C_7 | graves=C_7 | watson=C_7 | parker=C_7 | johnstone=C_7 | ~femalecouple(joyce, C_7)))). % 9.19/3.13 tff(c_8, plain, (![C_4:person]: (shearer=C_4 | graves=C_4 | watson=C_4 | parker=C_4 | johnstone=C_4 | ~malecouple(peter, C_4)))). % 9.19/3.13 tff(c_18, plain, (![C_9:person]: (shearer=C_9 | graves=C_9 | watson=C_9 | parker=C_9 | johnstone=C_9 | ~femalecouple(elizabeth, C_9)))). % 9.19/3.13 tff(c_10, plain, (![C_5:person]: (shearer=C_5 | graves=C_5 | watson=C_5 | parker=C_5 | johnstone=C_5 | ~malecouple(everett, C_5)))). % 9.19/3.13 tff(c_221, plain, (~malecouple(everett, johnstone))). % 9.19/3.13 tff(c_2, plain, (![C_1:person]: (shearer=C_1 | graves=C_1 | watson=C_1 | parker=C_1 | johnstone=C_1 | ~malecouple(russell, C_1)))). % 9.19/3.13 tff(c_220, plain, (~malecouple(everett, shearer))). % 9.19/3.13 tff(c_219, plain, (~malecouple(everett, parker))). % 9.19/3.13 tff(c_6, plain, (![C_3:person]: (shearer=C_3 | graves=C_3 | watson=C_3 | parker=C_3 | johnstone=C_3 | ~malecouple(charles, C_3)))). % 9.19/3.13 tff(c_217, plain, (~malecouple(everett, watson))). % 9.19/3.13 tff(c_207, plain, (~malecouple(everett, graves))). % 9.19/3.13 tff(c_16, plain, (![C_8:person]: (shearer=C_8 | graves=C_8 | watson=C_8 | parker=C_8 | johnstone=C_8 | ~femalecouple(marcia, C_8)))). % 9.19/3.13 tff(c_78, plain, (![X1_54:person]: (married(X1_54, 25) | ~malecouple(everett, X1_54)))). % 9.19/3.13 tff(c_144, plain, (![X_14a:$int]: (~married(graves, X_14a) | X_14a=30))). % 9.19/3.13 tff(c_59, plain, (![X_34:person]: (malecouple(douglas, X_34) | ~femalecouple(mildred, X_34)))). % 9.19/3.13 tff(c_103, plain, (![X_11a:$int]: (~married(johnstone, X_11a) | npjohnstone=X_11a))). % 9.19/3.13 tff(c_102, plain, (![X_12a:$int]: (~married(parker, X_12a) | npparker=X_12a))). % 9.19/3.14 tff(c_107, plain, (married(shearer, npshearer))). % 9.19/3.14 tff(c_115, plain, (married(watson, npwatson))). % 9.19/3.14 tff(c_119, plain, (married(parker, npparker))). % 9.19/3.14 tff(c_101, plain, (![X_13a:$int]: (~married(watson, X_13a) | npwatson=X_13a))). % 9.19/3.14 tff(c_141, plain, (npgraves=30)). % 9.19/3.14 tff(c_123, plain, (married(johnstone, npjohnstone))). % 9.19/3.14 tff(c_99, plain, (![X_15a:$int]: (~married(shearer, X_15a) | npshearer=X_15a))). % 9.19/3.14 tff(c_85, plain, (married(graves, 30))). % 9.19/3.14 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 9.19/3.14 %------------------------------------------------------------------------------