%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP039-1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n026.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 : Thu May 9 17:33:44 EDT 2024
% Result : Satisfiable 1.81s 2.00s
% Output : Saturation 1.81s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c3,axiom,
( X252 != X250
| X249 != X254
| X257 != X251
| X255 != X256
| X253 != X258
| skf19(X252,X249,X257,X255,X253) = skf19(X250,X254,X251,X256,X258) ),
theory(equality) ).
cnf(c172,plain,
( X660 != X659
| X663 != X662
| X658 != X657
| X655 != X661
| skf19(X660,X663,X658,X655,X656) = skf19(X659,X662,X657,X661,X656) ),
inference(resolution,[status(thm)],[c3,reflexivity]) ).
cnf(c344,plain,
( X1148 != X1145
| X1150 != X1147
| X1146 != X1143
| skf19(X1148,X1150,X1146,X1144,X1149) = skf19(X1145,X1147,X1143,X1144,X1149) ),
inference(resolution,[status(thm)],[c172,reflexivity]) ).
cnf(c504,plain,
( X1506 != X1511
| X1509 != X1505
| skf19(X1506,X1509,X1507,X1510,X1508) = skf19(X1511,X1505,X1507,X1510,X1508) ),
inference(resolution,[status(thm)],[c344,reflexivity]) ).
cnf(c566,plain,
( X1522 != X1518
| skf19(X1522,X1517,X1520,X1521,X1519) = skf19(X1518,X1517,X1520,X1521,X1519) ),
inference(resolution,[status(thm)],[c504,reflexivity]) ).
cnf(c565,plain,
( X1516 != X1514
| skf19(X1516,X1516,X1513,X1515,X1512) = skf19(X1514,X1514,X1513,X1515,X1512) ),
inference(factor,[status(thm)],[c504]) ).
cnf(c503,plain,
( X1486 != X1491
| X1489 != X1488
| skf19(X1486,X1489,X1489,X1490,X1487) = skf19(X1491,X1488,X1488,X1490,X1487) ),
inference(factor,[status(thm)],[c344]) ).
cnf(c502,plain,
( X1463 != X1462
| X1461 != X1460
| skf19(X1463,X1461,X1463,X1464,X1465) = skf19(X1462,X1460,X1462,X1464,X1465) ),
inference(factor,[status(thm)],[c344]) ).
cnf(c559,plain,
( X1480 != X1481
| skf19(X1480,X1479,X1480,X1477,X1478) = skf19(X1481,X1479,X1481,X1477,X1478) ),
inference(resolution,[status(thm)],[c502,reflexivity]) ).
cnf(c558,plain,
( X1473 != X1472
| skf19(X1473,X1473,X1473,X1470,X1471) = skf19(X1472,X1472,X1472,X1470,X1471) ),
inference(factor,[status(thm)],[c502]) ).
cnf(c342,plain,
( X1097 != X1094
| X1096 != X1092
| X1095 != X1093
| skf19(X1097,X1096,X1095,X1096,X1098) = skf19(X1094,X1092,X1093,X1092,X1098) ),
inference(factor,[status(thm)],[c172]) ).
cnf(c491,plain,
( X1408 != X1411
| X1410 != X1409
| skf19(X1408,X1410,X1407,X1410,X1406) = skf19(X1411,X1409,X1407,X1409,X1406) ),
inference(resolution,[status(thm)],[c342,reflexivity]) ).
cnf(c490,plain,
( X1399 != X1402
| X1400 != X1401
| skf19(X1399,X1400,X1400,X1400,X1398) = skf19(X1402,X1401,X1401,X1401,X1398) ),
inference(factor,[status(thm)],[c342]) ).
cnf(c489,plain,
( X1386 != X1387
| X1385 != X1384
| skf19(X1386,X1385,X1386,X1385,X1383) = skf19(X1387,X1384,X1387,X1384,X1383) ),
inference(factor,[status(thm)],[c342]) ).
cnf(c341,plain,
( X1069 != X1066
| X1072 != X1070
| X1068 != X1067
| skf19(X1069,X1072,X1068,X1069,X1071) = skf19(X1066,X1070,X1067,X1066,X1071) ),
inference(factor,[status(thm)],[c172]) ).
cnf(c486,plain,
( X1358 != X1359
| X1363 != X1360
| skf19(X1358,X1363,X1361,X1358,X1362) = skf19(X1359,X1360,X1361,X1359,X1362) ),
inference(resolution,[status(thm)],[c341,reflexivity]) ).
cnf(c542,plain,
( X1378 != X1375
| skf19(X1378,X1377,X1376,X1378,X1374) = skf19(X1375,X1377,X1376,X1375,X1374) ),
inference(resolution,[status(thm)],[c486,reflexivity]) ).
cnf(c541,plain,
( X1368 != X1367
| skf19(X1368,X1368,X1370,X1368,X1369) = skf19(X1367,X1367,X1370,X1367,X1369) ),
inference(factor,[status(thm)],[c486]) ).
cnf(c484,plain,
( X1313 != X1315
| X1317 != X1314
| skf19(X1313,X1317,X1313,X1313,X1316) = skf19(X1315,X1314,X1315,X1315,X1316) ),
inference(factor,[status(thm)],[c341]) ).
cnf(c533,plain,
( X1344 != X1347
| skf19(X1344,X1345,X1344,X1344,X1346) = skf19(X1347,X1345,X1347,X1347,X1346) ),
inference(resolution,[status(thm)],[c484,reflexivity]) ).
cnf(c485,plain,
( X1338 != X1339
| X1337 != X1340
| skf19(X1338,X1337,X1337,X1338,X1341) = skf19(X1339,X1340,X1340,X1339,X1341) ),
inference(factor,[status(thm)],[c341]) ).
cnf(c532,plain,
( X1334 != X1336
| skf19(X1334,X1334,X1334,X1334,X1335) = skf19(X1336,X1336,X1336,X1336,X1335) ),
inference(factor,[status(thm)],[c484]) ).
cnf(c169,plain,
( X622 != X621
| X618 != X617
| X620 != X619
| X616 != X623
| skf19(X622,X618,X620,X616,X618) = skf19(X621,X617,X619,X623,X617) ),
inference(factor,[status(thm)],[c3]) ).
cnf(c322,plain,
( X861 != X862
| X860 != X857
| X859 != X858
| skf19(X861,X860,X859,X856,X860) = skf19(X862,X857,X858,X856,X857) ),
inference(resolution,[status(thm)],[c169,reflexivity]) ).
cnf(c435,plain,
( X1152 != X1156
| X1154 != X1155
| skf19(X1152,X1154,X1151,X1153,X1154) = skf19(X1156,X1155,X1151,X1153,X1155) ),
inference(resolution,[status(thm)],[c322,reflexivity]) ).
cnf(c434,plain,
( X1129 != X1132
| X1128 != X1131
| skf19(X1129,X1128,X1128,X1130,X1128) = skf19(X1132,X1131,X1131,X1130,X1131) ),
inference(factor,[status(thm)],[c322]) ).
cnf(c343,plain,
( X1122 != X1119
| X1124 != X1121
| X1120 != X1118
| skf19(X1122,X1124,X1120,X1120,X1123) = skf19(X1119,X1121,X1118,X1118,X1123) ),
inference(factor,[status(thm)],[c172]) ).
cnf(c433,plain,
( X1106 != X1109
| X1108 != X1110
| skf19(X1106,X1108,X1106,X1107,X1108) = skf19(X1109,X1110,X1109,X1107,X1110) ),
inference(factor,[status(thm)],[c322]) ).
cnf(c320,plain,
( X817 != X819
| X818 != X816
| X815 != X814
| skf19(X817,X818,X815,X818,X818) = skf19(X819,X816,X814,X816,X816) ),
inference(factor,[status(thm)],[c169]) ).
cnf(c422,plain,
( X1056 != X1055
| X1057 != X1058
| skf19(X1056,X1057,X1054,X1057,X1057) = skf19(X1055,X1058,X1054,X1058,X1058) ),
inference(resolution,[status(thm)],[c320,reflexivity]) ).
cnf(c421,plain,
( X1037 != X1036
| X1039 != X1038
| skf19(X1037,X1039,X1039,X1039,X1039) = skf19(X1036,X1038,X1038,X1038,X1038) ),
inference(factor,[status(thm)],[c320]) ).
cnf(c420,plain,
( X1022 != X1020
| X1019 != X1021
| skf19(X1022,X1019,X1022,X1019,X1019) = skf19(X1020,X1021,X1020,X1021,X1021) ),
inference(factor,[status(thm)],[c320]) ).
cnf(c319,plain,
( X797 != X796
| X795 != X792
| X794 != X793
| skf19(X797,X795,X794,X797,X795) = skf19(X796,X792,X793,X796,X792) ),
inference(factor,[status(thm)],[c169]) ).
cnf(c415,plain,
( X1005 != X1007
| X1006 != X1008
| skf19(X1005,X1006,X1004,X1005,X1006) = skf19(X1007,X1008,X1004,X1007,X1008) ),
inference(resolution,[status(thm)],[c319,reflexivity]) ).
cnf(c414,plain,
( X988 != X987
| X989 != X990
| skf19(X988,X989,X989,X988,X989) = skf19(X987,X990,X990,X987,X990) ),
inference(factor,[status(thm)],[c319]) ).
cnf(c413,plain,
( X971 != X972
| X973 != X970
| skf19(X971,X973,X971,X971,X973) = skf19(X972,X970,X972,X972,X970) ),
inference(factor,[status(thm)],[c319]) ).
cnf(c168,plain,
( X606 != X605
| X611 != X610
| X608 != X607
| X604 != X609
| skf19(X606,X611,X608,X604,X606) = skf19(X605,X610,X607,X609,X605) ),
inference(factor,[status(thm)],[c3]) ).
cnf(c315,plain,
( X773 != X771
| X772 != X775
| X774 != X770
| skf19(X773,X772,X774,X769,X773) = skf19(X771,X775,X770,X769,X771) ),
inference(resolution,[status(thm)],[c168,reflexivity]) ).
cnf(c407,plain,
( X944 != X945
| X946 != X941
| skf19(X944,X946,X942,X943,X944) = skf19(X945,X941,X942,X943,X945) ),
inference(resolution,[status(thm)],[c315,reflexivity]) ).
cnf(c457,plain,
( X965 != X964
| skf19(X965,X961,X962,X963,X965) = skf19(X964,X961,X962,X963,X964) ),
inference(resolution,[status(thm)],[c407,reflexivity]) ).
cnf(c170,plain,
( X634 != X633
| X637 != X636
| X632 != X631
| X630 != X635
| skf19(X634,X637,X632,X630,X632) = skf19(X633,X636,X631,X635,X631) ),
inference(factor,[status(thm)],[c3]) ).
cnf(c330,plain,
( X956 != X959
| X960 != X957
| X954 != X958
| skf19(X956,X960,X954,X955,X954) = skf19(X959,X957,X958,X955,X958) ),
inference(resolution,[status(thm)],[c170,reflexivity]) ).
cnf(c456,plain,
( X948 != X947
| skf19(X948,X948,X950,X949,X948) = skf19(X947,X947,X950,X949,X947) ),
inference(factor,[status(thm)],[c407]) ).
cnf(c329,plain,
( X928 != X932
| X933 != X929
| X930 != X931
| skf19(X928,X933,X930,X930,X930) = skf19(X932,X929,X931,X931,X931) ),
inference(factor,[status(thm)],[c170]) ).
cnf(c406,plain,
( X921 != X923
| X924 != X922
| skf19(X921,X924,X924,X920,X921) = skf19(X923,X922,X922,X920,X923) ),
inference(factor,[status(thm)],[c315]) ).
cnf(c405,plain,
( X901 != X899
| X900 != X897
| skf19(X901,X900,X901,X898,X901) = skf19(X899,X897,X899,X898,X899) ),
inference(factor,[status(thm)],[c315]) ).
cnf(c444,plain,
( X913 != X915
| skf19(X913,X914,X913,X916,X913) = skf19(X915,X914,X915,X916,X915) ),
inference(resolution,[status(thm)],[c405,reflexivity]) ).
cnf(c328,plain,
( X906 != X910
| X908 != X909
| X905 != X907
| skf19(X906,X908,X905,X908,X905) = skf19(X910,X909,X907,X909,X907) ),
inference(factor,[status(thm)],[c170]) ).
cnf(c443,plain,
( X903 != X902
| skf19(X903,X903,X903,X904,X903) = skf19(X902,X902,X902,X904,X902) ),
inference(factor,[status(thm)],[c405]) ).
cnf(c327,plain,
( X885 != X886
| X887 != X883
| X882 != X884
| skf19(X885,X887,X882,X885,X882) = skf19(X886,X883,X884,X886,X884) ),
inference(factor,[status(thm)],[c170]) ).
cnf(c313,plain,
( X743 != X742
| X744 != X746
| X745 != X741
| skf19(X743,X744,X745,X744,X743) = skf19(X742,X746,X741,X746,X742) ),
inference(factor,[status(thm)],[c168]) ).
cnf(c394,plain,
( X848 != X844
| X845 != X847
| skf19(X848,X845,X846,X845,X848) = skf19(X844,X847,X846,X847,X844) ),
inference(resolution,[status(thm)],[c313,reflexivity]) ).
cnf(c321,plain,
( X836 != X838
| X834 != X833
| X837 != X835
| skf19(X836,X834,X837,X837,X834) = skf19(X838,X833,X835,X835,X833) ),
inference(factor,[status(thm)],[c169]) ).
cnf(c393,plain,
( X827 != X830
| X829 != X828
| skf19(X827,X829,X829,X829,X827) = skf19(X830,X828,X828,X828,X830) ),
inference(factor,[status(thm)],[c313]) ).
cnf(c392,plain,
( X812 != X811
| X810 != X813
| skf19(X812,X810,X812,X810,X812) = skf19(X811,X813,X811,X813,X811) ),
inference(factor,[status(thm)],[c313]) ).
cnf(c312,plain,
( X732 != X734
| X731 != X735
| X733 != X730
| skf19(X732,X731,X733,X732,X732) = skf19(X734,X735,X730,X734,X734) ),
inference(factor,[status(thm)],[c168]) ).
cnf(c388,plain,
( X789 != X787
| X790 != X791
| skf19(X789,X790,X788,X789,X789) = skf19(X787,X791,X788,X787,X787) ),
inference(resolution,[status(thm)],[c312,reflexivity]) ).
cnf(c412,plain,
( X805 != X806
| skf19(X805,X803,X804,X805,X805) = skf19(X806,X803,X804,X806,X806) ),
inference(resolution,[status(thm)],[c388,reflexivity]) ).
cnf(c411,plain,
( X800 != X798
| skf19(X800,X800,X799,X800,X800) = skf19(X798,X798,X799,X798,X798) ),
inference(factor,[status(thm)],[c388]) ).
cnf(c387,plain,
( X779 != X777
| X778 != X776
| skf19(X779,X778,X778,X779,X779) = skf19(X777,X776,X776,X777,X777) ),
inference(factor,[status(thm)],[c312]) ).
cnf(c386,plain,
( X759 != X758
| X757 != X760
| skf19(X759,X757,X759,X759,X759) = skf19(X758,X760,X758,X758,X758) ),
inference(factor,[status(thm)],[c312]) ).
cnf(c402,plain,
( X764 != X765
| skf19(X764,X766,X764,X764,X764) = skf19(X765,X766,X765,X765,X765) ),
inference(resolution,[status(thm)],[c386,reflexivity]) ).
cnf(c401,plain,
( X762 != X761
| skf19(X762,X762,X762,X762,X762) = skf19(X761,X761,X761,X761,X761) ),
inference(factor,[status(thm)],[c386]) ).
cnf(c314,plain,
( X753 != X751
| X752 != X756
| X754 != X755
| skf19(X753,X752,X754,X754,X753) = skf19(X751,X756,X755,X755,X751) ),
inference(factor,[status(thm)],[c168]) ).
cnf(clause54,negated_conjecture,
three(skc2,skc3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause54) ).
cnf(clause44,axiom,
( ~ three(X96,X95)
| member(X96,skf14(X95,X96),X95) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause44) ).
cnf(c55,plain,
member(skc2,skf14(skc3,skc2),skc3),
inference(resolution,[status(thm)],[clause44,clause54]) ).
cnf(c7,axiom,
( X291 != X289
| X288 != X292
| X293 != X290
| ~ member(X291,X288,X293)
| member(X289,X292,X290) ),
theory(equality) ).
cnf(c190,plain,
( skc2 != X686
| skf14(skc3,skc2) != X687
| skc3 != X685
| member(X686,X687,X685) ),
inference(resolution,[status(thm)],[c7,c55]) ).
cnf(c357,plain,
( skc2 != X748
| skc3 != X749
| member(X748,skf14(skc3,skc2),X749) ),
inference(resolution,[status(thm)],[c190,reflexivity]) ).
cnf(c396,plain,
( skc2 != X750
| member(X750,skf14(skc3,skc2),skc3) ),
inference(resolution,[status(thm)],[c357,reflexivity]) ).
cnf(clause42,axiom,
( ~ three(X92,X91)
| member(X92,skf18(X91,X92),X91) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause42) ).
cnf(c53,plain,
member(skc2,skf18(skc3,skc2),skc3),
inference(resolution,[status(thm)],[clause42,clause54]) ).
cnf(c189,plain,
( skc2 != X679
| skf18(skc3,skc2) != X680
| skc3 != X678
| member(X679,X680,X678) ),
inference(resolution,[status(thm)],[c7,c53]) ).
cnf(c353,plain,
( skc2 != X739
| skc3 != X740
| member(X739,skf18(skc3,skc2),X740) ),
inference(resolution,[status(thm)],[c189,reflexivity]) ).
cnf(c391,plain,
( skc2 != X747
| member(X747,skf18(skc3,skc2),skc3) ),
inference(resolution,[status(thm)],[c353,reflexivity]) ).
cnf(clause43,axiom,
( ~ three(X94,X93)
| member(X94,skf16(X93,X94),X93) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause43) ).
cnf(c54,plain,
member(skc2,skf16(skc3,skc2),skc3),
inference(resolution,[status(thm)],[clause43,clause54]) ).
cnf(c188,plain,
( skc2 != X671
| skf16(skc3,skc2) != X672
| skc3 != X670
| member(X671,X672,X670) ),
inference(resolution,[status(thm)],[c7,c54]) ).
cnf(c349,plain,
( skc2 != X737
| skc3 != X736
| member(X737,skf16(skc3,skc2),X736) ),
inference(resolution,[status(thm)],[c188,reflexivity]) ).
cnf(c389,plain,
( skc2 != X738
| member(X738,skf16(skc3,skc2),skc3) ),
inference(resolution,[status(thm)],[c349,reflexivity]) ).
cnf(clause56,negated_conjecture,
( ~ member(skc2,X97,skc3)
| young(skc2,X97) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause56) ).
cnf(c80,plain,
young(skc2,skf16(skc3,skc2)),
inference(resolution,[status(thm)],[c54,clause56]) ).
cnf(c43,axiom,
( X506 != X504
| X505 != X507
| ~ young(X506,X505)
| young(X504,X507) ),
theory(equality) ).
cnf(c272,plain,
( skc2 != X728
| skf16(skc3,skc2) != X727
| young(X728,X727) ),
inference(resolution,[status(thm)],[c43,c80]) ).
cnf(c384,plain,
( skc2 != X729
| young(X729,skf16(skc3,skc2)) ),
inference(resolution,[status(thm)],[c272,reflexivity]) ).
cnf(c60,plain,
young(skc2,skf18(skc3,skc2)),
inference(resolution,[status(thm)],[c53,clause56]) ).
cnf(c271,plain,
( skc2 != X725
| skf18(skc3,skc2) != X724
| young(X725,X724) ),
inference(resolution,[status(thm)],[c43,c60]) ).
cnf(c382,plain,
( skc2 != X726
| young(X726,skf18(skc3,skc2)) ),
inference(resolution,[status(thm)],[c271,reflexivity]) ).
cnf(c126,plain,
young(skc2,skf14(skc3,skc2)),
inference(resolution,[status(thm)],[c55,clause56]) ).
cnf(c270,plain,
( skc2 != X722
| skf14(skc3,skc2) != X721
| young(X722,X721) ),
inference(resolution,[status(thm)],[c43,c126]) ).
cnf(c380,plain,
( skc2 != X723
| young(X723,skf14(skc3,skc2)) ),
inference(resolution,[status(thm)],[c270,reflexivity]) ).
cnf(clause14,axiom,
( ~ man(X30,X29)
| male(X30,X29) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause14) ).
cnf(clause2,axiom,
( ~ guy(X6,X5)
| man(X6,X5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
cnf(clause57,negated_conjecture,
( ~ member(skc2,X98,skc3)
| guy(skc2,X98) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause57) ).
cnf(c81,plain,
guy(skc2,skf16(skc3,skc2)),
inference(resolution,[status(thm)],[c54,clause57]) ).
cnf(c82,plain,
man(skc2,skf16(skc3,skc2)),
inference(resolution,[status(thm)],[c81,clause2]) ).
cnf(c83,plain,
male(skc2,skf16(skc3,skc2)),
inference(resolution,[status(thm)],[c82,clause14]) ).
cnf(c21,axiom,
( X351 != X349
| X350 != X352
| ~ male(X351,X350)
| male(X349,X352) ),
theory(equality) ).
cnf(c227,plain,
( skc2 != X718
| skf16(skc3,skc2) != X719
| male(X718,X719) ),
inference(resolution,[status(thm)],[c21,c83]) ).
cnf(c378,plain,
( skc2 != X720
| male(X720,skf16(skc3,skc2)) ),
inference(resolution,[status(thm)],[c227,reflexivity]) ).
cnf(c125,plain,
guy(skc2,skf14(skc3,skc2)),
inference(resolution,[status(thm)],[c55,clause57]) ).
cnf(c128,plain,
man(skc2,skf14(skc3,skc2)),
inference(resolution,[status(thm)],[c125,clause2]) ).
cnf(c129,plain,
male(skc2,skf14(skc3,skc2)),
inference(resolution,[status(thm)],[c128,clause14]) ).
cnf(c226,plain,
( skc2 != X715
| skf14(skc3,skc2) != X716
| male(X715,X716) ),
inference(resolution,[status(thm)],[c21,c129]) ).
cnf(c376,plain,
( skc2 != X717
| male(X717,skf14(skc3,skc2)) ),
inference(resolution,[status(thm)],[c226,reflexivity]) ).
cnf(c61,plain,
guy(skc2,skf18(skc3,skc2)),
inference(resolution,[status(thm)],[c53,clause57]) ).
cnf(c62,plain,
man(skc2,skf18(skc3,skc2)),
inference(resolution,[status(thm)],[c61,clause2]) ).
cnf(c63,plain,
male(skc2,skf18(skc3,skc2)),
inference(resolution,[status(thm)],[c62,clause14]) ).
cnf(c225,plain,
( skc2 != X712
| skf18(skc3,skc2) != X713
| male(X712,X713) ),
inference(resolution,[status(thm)],[c21,c63]) ).
cnf(c374,plain,
( skc2 != X714
| male(X714,skf18(skc3,skc2)) ),
inference(resolution,[status(thm)],[c225,reflexivity]) ).
cnf(clause13,axiom,
( ~ human_person(X28,X27)
| animate(X28,X27) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause13) ).
cnf(clause3,axiom,
( ~ man(X8,X7)
| human_person(X8,X7) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
cnf(c64,plain,
human_person(skc2,skf18(skc3,skc2)),
inference(resolution,[status(thm)],[c62,clause3]) ).
cnf(c66,plain,
animate(skc2,skf18(skc3,skc2)),
inference(resolution,[status(thm)],[c64,clause13]) ).
cnf(c20,axiom,
( X347 != X345
| X346 != X348
| ~ animate(X347,X346)
| animate(X345,X348) ),
theory(equality) ).
cnf(c224,plain,
( skc2 != X710
| skf18(skc3,skc2) != X709
| animate(X710,X709) ),
inference(resolution,[status(thm)],[c20,c66]) ).
cnf(c372,plain,
( skc2 != X711
| animate(X711,skf18(skc3,skc2)) ),
inference(resolution,[status(thm)],[c224,reflexivity]) ).
cnf(c130,plain,
human_person(skc2,skf14(skc3,skc2)),
inference(resolution,[status(thm)],[c128,clause3]) ).
cnf(c132,plain,
animate(skc2,skf14(skc3,skc2)),
inference(resolution,[status(thm)],[c130,clause13]) ).
cnf(c223,plain,
( skc2 != X707
| skf14(skc3,skc2) != X706
| animate(X707,X706) ),
inference(resolution,[status(thm)],[c20,c132]) ).
cnf(c370,plain,
( skc2 != X708
| animate(X708,skf14(skc3,skc2)) ),
inference(resolution,[status(thm)],[c223,reflexivity]) ).
cnf(c84,plain,
human_person(skc2,skf16(skc3,skc2)),
inference(resolution,[status(thm)],[c82,clause3]) ).
cnf(c86,plain,
animate(skc2,skf16(skc3,skc2)),
inference(resolution,[status(thm)],[c84,clause13]) ).
cnf(c222,plain,
( skc2 != X704
| skf16(skc3,skc2) != X703
| animate(X704,X703) ),
inference(resolution,[status(thm)],[c20,c86]) ).
cnf(c368,plain,
( skc2 != X705
| animate(X705,skf16(skc3,skc2)) ),
inference(resolution,[status(thm)],[c222,reflexivity]) ).
cnf(clause12,axiom,
( ~ human_person(X26,X25)
| human(X26,X25) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause12) ).
cnf(c67,plain,
human(skc2,skf18(skc3,skc2)),
inference(resolution,[status(thm)],[c64,clause12]) ).
cnf(c19,axiom,
( X343 != X341
| X342 != X344
| ~ human(X343,X342)
| human(X341,X344) ),
theory(equality) ).
cnf(c221,plain,
( skc2 != X701
| skf18(skc3,skc2) != X700
| human(X701,X700) ),
inference(resolution,[status(thm)],[c19,c67]) ).
cnf(c366,plain,
( skc2 != X702
| human(X702,skf18(skc3,skc2)) ),
inference(resolution,[status(thm)],[c221,reflexivity]) ).
cnf(c87,plain,
human(skc2,skf16(skc3,skc2)),
inference(resolution,[status(thm)],[c84,clause12]) ).
cnf(c220,plain,
( skc2 != X698
| skf16(skc3,skc2) != X697
| human(X698,X697) ),
inference(resolution,[status(thm)],[c19,c87]) ).
cnf(c364,plain,
( skc2 != X699
| human(X699,skf16(skc3,skc2)) ),
inference(resolution,[status(thm)],[c220,reflexivity]) ).
cnf(c133,plain,
human(skc2,skf14(skc3,skc2)),
inference(resolution,[status(thm)],[c130,clause12]) ).
cnf(c219,plain,
( skc2 != X695
| skf14(skc3,skc2) != X694
| human(X695,X694) ),
inference(resolution,[status(thm)],[c19,c133]) ).
cnf(c362,plain,
( skc2 != X696
| human(X696,skf14(skc3,skc2)) ),
inference(resolution,[status(thm)],[c219,reflexivity]) ).
cnf(clause11,axiom,
( ~ organism(X24,X23)
| living(X24,X23) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
cnf(clause4,axiom,
( ~ human_person(X10,X9)
| organism(X10,X9) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause4) ).
cnf(c131,plain,
organism(skc2,skf14(skc3,skc2)),
inference(resolution,[status(thm)],[c130,clause4]) ).
cnf(c134,plain,
living(skc2,skf14(skc3,skc2)),
inference(resolution,[status(thm)],[c131,clause11]) ).
cnf(c18,axiom,
( X338 != X336
| X337 != X339
| ~ living(X338,X337)
| living(X336,X339) ),
theory(equality) ).
cnf(c218,plain,
( skc2 != X691
| skf14(skc3,skc2) != X692
| living(X691,X692) ),
inference(resolution,[status(thm)],[c18,c134]) ).
cnf(c360,plain,
( skc2 != X693
| living(X693,skf14(skc3,skc2)) ),
inference(resolution,[status(thm)],[c218,reflexivity]) ).
cnf(c65,plain,
organism(skc2,skf18(skc3,skc2)),
inference(resolution,[status(thm)],[c64,clause4]) ).
cnf(c68,plain,
living(skc2,skf18(skc3,skc2)),
inference(resolution,[status(thm)],[c65,clause11]) ).
cnf(c217,plain,
( skc2 != X688
| skf18(skc3,skc2) != X689
| living(X688,X689) ),
inference(resolution,[status(thm)],[c18,c68]) ).
cnf(c358,plain,
( skc2 != X690
| living(X690,skf18(skc3,skc2)) ),
inference(resolution,[status(thm)],[c217,reflexivity]) ).
cnf(c85,plain,
organism(skc2,skf16(skc3,skc2)),
inference(resolution,[status(thm)],[c84,clause4]) ).
cnf(c88,plain,
living(skc2,skf16(skc3,skc2)),
inference(resolution,[status(thm)],[c85,clause11]) ).
cnf(c216,plain,
( skc2 != X682
| skf16(skc3,skc2) != X683
| living(X682,X683) ),
inference(resolution,[status(thm)],[c18,c88]) ).
cnf(c355,plain,
( skc2 != X684
| living(X684,skf16(skc3,skc2)) ),
inference(resolution,[status(thm)],[c216,reflexivity]) ).
cnf(clause10,axiom,
( ~ organism(X22,X21)
| impartial(X22,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause10) ).
cnf(c136,plain,
impartial(skc2,skf14(skc3,skc2)),
inference(resolution,[status(thm)],[c131,clause10]) ).
cnf(c17,axiom,
( X323 != X321
| X322 != X324
| ~ impartial(X323,X322)
| impartial(X321,X324) ),
theory(equality) ).
cnf(c211,plain,
( skc2 != X677
| skf14(skc3,skc2) != X676
| impartial(X677,X676) ),
inference(resolution,[status(thm)],[c17,c136]) ).
cnf(c352,plain,
( skc2 != X681
| impartial(X681,skf14(skc3,skc2)) ),
inference(resolution,[status(thm)],[c211,reflexivity]) ).
cnf(c90,plain,
impartial(skc2,skf16(skc3,skc2)),
inference(resolution,[status(thm)],[c85,clause10]) ).
cnf(c209,plain,
( skc2 != X674
| skf16(skc3,skc2) != X673
| impartial(X674,X673) ),
inference(resolution,[status(thm)],[c17,c90]) ).
cnf(c350,plain,
( skc2 != X675
| impartial(X675,skf16(skc3,skc2)) ),
inference(resolution,[status(thm)],[c209,reflexivity]) ).
cnf(c70,plain,
impartial(skc2,skf18(skc3,skc2)),
inference(resolution,[status(thm)],[c65,clause10]) ).
cnf(c208,plain,
( skc2 != X668
| skf18(skc3,skc2) != X667
| impartial(X668,X667) ),
inference(resolution,[status(thm)],[c17,c70]) ).
cnf(c347,plain,
( skc2 != X669
| impartial(X669,skf18(skc3,skc2)) ),
inference(resolution,[status(thm)],[c208,reflexivity]) ).
cnf(clause9,axiom,
( ~ entity(X20,X19)
| existent(X20,X19) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause9) ).
cnf(clause5,axiom,
( ~ organism(X12,X11)
| entity(X12,X11) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause5) ).
cnf(c135,plain,
entity(skc2,skf14(skc3,skc2)),
inference(resolution,[status(thm)],[c131,clause5]) ).
cnf(c138,plain,
existent(skc2,skf14(skc3,skc2)),
inference(resolution,[status(thm)],[c135,clause9]) ).
cnf(c16,axiom,
( X319 != X317
| X318 != X320
| ~ existent(X319,X318)
| existent(X317,X320) ),
theory(equality) ).
cnf(c206,plain,
( skc2 != X664
| skf14(skc3,skc2) != X665
| existent(X664,X665) ),
inference(resolution,[status(thm)],[c16,c138]) ).
cnf(c345,plain,
( skc2 != X666
| existent(X666,skf14(skc3,skc2)) ),
inference(resolution,[status(thm)],[c206,reflexivity]) ).
cnf(c69,plain,
entity(skc2,skf18(skc3,skc2)),
inference(resolution,[status(thm)],[c65,clause5]) ).
cnf(c73,plain,
existent(skc2,skf18(skc3,skc2)),
inference(resolution,[status(thm)],[c69,clause9]) ).
cnf(c205,plain,
( skc2 != X652
| skf18(skc3,skc2) != X653
| existent(X652,X653) ),
inference(resolution,[status(thm)],[c16,c73]) ).
cnf(c339,plain,
( skc2 != X654
| existent(X654,skf18(skc3,skc2)) ),
inference(resolution,[status(thm)],[c205,reflexivity]) ).
cnf(c89,plain,
entity(skc2,skf16(skc3,skc2)),
inference(resolution,[status(thm)],[c85,clause5]) ).
cnf(c92,plain,
existent(skc2,skf16(skc3,skc2)),
inference(resolution,[status(thm)],[c89,clause9]) ).
cnf(c204,plain,
( skc2 != X641
| skf16(skc3,skc2) != X642
| existent(X641,X642) ),
inference(resolution,[status(thm)],[c16,c92]) ).
cnf(c333,plain,
( skc2 != X651
| existent(X651,skf16(skc3,skc2)) ),
inference(resolution,[status(thm)],[c204,reflexivity]) ).
cnf(c171,plain,
( X648 != X647
| X650 != X649
| X646 != X645
| X644 != X643
| skf19(X648,X650,X646,X644,X644) = skf19(X647,X649,X645,X643,X643) ),
inference(factor,[status(thm)],[c3]) ).
cnf(clause8,axiom,
( ~ entity(X18,X17)
| specific(X18,X17) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
cnf(c139,plain,
specific(skc2,skf14(skc3,skc2)),
inference(resolution,[status(thm)],[c135,clause8]) ).
cnf(c15,axiom,
( X308 != X306
| X307 != X309
| ~ specific(X308,X307)
| specific(X306,X309) ),
theory(equality) ).
cnf(c200,plain,
( skc2 != X638
| skf14(skc3,skc2) != X639
| specific(X638,X639) ),
inference(resolution,[status(thm)],[c15,c139]) ).
cnf(c331,plain,
( skc2 != X640
| specific(X640,skf14(skc3,skc2)) ),
inference(resolution,[status(thm)],[c200,reflexivity]) ).
cnf(c93,plain,
specific(skc2,skf16(skc3,skc2)),
inference(resolution,[status(thm)],[c89,clause8]) ).
cnf(c199,plain,
( skc2 != X627
| skf16(skc3,skc2) != X628
| specific(X627,X628) ),
inference(resolution,[status(thm)],[c15,c93]) ).
cnf(c325,plain,
( skc2 != X629
| specific(X629,skf16(skc3,skc2)) ),
inference(resolution,[status(thm)],[c199,reflexivity]) ).
cnf(c74,plain,
specific(skc2,skf18(skc3,skc2)),
inference(resolution,[status(thm)],[c69,clause8]) ).
cnf(c198,plain,
( skc2 != X624
| skf18(skc3,skc2) != X625
| specific(X624,X625) ),
inference(resolution,[status(thm)],[c15,c74]) ).
cnf(c323,plain,
( skc2 != X626
| specific(X626,skf18(skc3,skc2)) ),
inference(resolution,[status(thm)],[c198,reflexivity]) ).
cnf(clause7,axiom,
( ~ thing(X16,X15)
| singleton(X16,X15) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause7) ).
cnf(clause6,axiom,
( ~ entity(X14,X13)
| thing(X14,X13) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause6) ).
cnf(c140,plain,
thing(skc2,skf14(skc3,skc2)),
inference(resolution,[status(thm)],[c135,clause6]) ).
cnf(c142,plain,
singleton(skc2,skf14(skc3,skc2)),
inference(resolution,[status(thm)],[c140,clause7]) ).
cnf(c14,axiom,
( X299 != X297
| X298 != X300
| ~ singleton(X299,X298)
| singleton(X297,X300) ),
theory(equality) ).
cnf(c195,plain,
( skc2 != X614
| skf14(skc3,skc2) != X613
| singleton(X614,X613) ),
inference(resolution,[status(thm)],[c14,c142]) ).
cnf(c317,plain,
( skc2 != X615
| singleton(X615,skf14(skc3,skc2)) ),
inference(resolution,[status(thm)],[c195,reflexivity]) ).
cnf(c94,plain,
thing(skc2,skf16(skc3,skc2)),
inference(resolution,[status(thm)],[c89,clause6]) ).
cnf(c100,plain,
singleton(skc2,skf16(skc3,skc2)),
inference(resolution,[status(thm)],[c94,clause7]) ).
cnf(c194,plain,
( skc2 != X603
| skf16(skc3,skc2) != X602
| singleton(X603,X602) ),
inference(resolution,[status(thm)],[c14,c100]) ).
cnf(c311,plain,
( skc2 != X612
| singleton(X612,skf16(skc3,skc2)) ),
inference(resolution,[status(thm)],[c194,reflexivity]) ).
cnf(c75,plain,
thing(skc2,skf18(skc3,skc2)),
inference(resolution,[status(thm)],[c69,clause6]) ).
cnf(c77,plain,
singleton(skc2,skf18(skc3,skc2)),
inference(resolution,[status(thm)],[c75,clause7]) ).
cnf(c193,plain,
( skc2 != X600
| skf18(skc3,skc2) != X599
| singleton(X600,X599) ),
inference(resolution,[status(thm)],[c14,c77]) ).
cnf(c309,plain,
( skc2 != X601
| singleton(X601,skf18(skc3,skc2)) ),
inference(resolution,[status(thm)],[c193,reflexivity]) ).
cnf(c13,axiom,
( X271 != X269
| X270 != X272
| ~ thing(X271,X270)
| thing(X269,X272) ),
theory(equality) ).
cnf(c182,plain,
( skc2 != X595
| skf16(skc3,skc2) != X594
| thing(X595,X594) ),
inference(resolution,[status(thm)],[c13,c94]) ).
cnf(c307,plain,
( skc2 != X596
| thing(X596,skf16(skc3,skc2)) ),
inference(resolution,[status(thm)],[c182,reflexivity]) ).
cnf(c181,plain,
( skc2 != X592
| skf18(skc3,skc2) != X591
| thing(X592,X591) ),
inference(resolution,[status(thm)],[c13,c75]) ).
cnf(c305,plain,
( skc2 != X593
| thing(X593,skf18(skc3,skc2)) ),
inference(resolution,[status(thm)],[c181,reflexivity]) ).
cnf(c180,plain,
( skc2 != X589
| skf14(skc3,skc2) != X588
| thing(X589,X588) ),
inference(resolution,[status(thm)],[c13,c140]) ).
cnf(c303,plain,
( skc2 != X590
| thing(X590,skf14(skc3,skc2)) ),
inference(resolution,[status(thm)],[c180,reflexivity]) ).
cnf(c12,axiom,
( X261 != X259
| X260 != X262
| ~ entity(X261,X260)
| entity(X259,X262) ),
theory(equality) ).
cnf(c176,plain,
( skc2 != X583
| skf18(skc3,skc2) != X584
| entity(X583,X584) ),
inference(resolution,[status(thm)],[c12,c69]) ).
cnf(c301,plain,
( skc2 != X587
| entity(X587,skf18(skc3,skc2)) ),
inference(resolution,[status(thm)],[c176,reflexivity]) ).
cnf(c175,plain,
( skc2 != X580
| skf16(skc3,skc2) != X581
| entity(X580,X581) ),
inference(resolution,[status(thm)],[c12,c89]) ).
cnf(c299,plain,
( skc2 != X582
| entity(X582,skf16(skc3,skc2)) ),
inference(resolution,[status(thm)],[c175,reflexivity]) ).
cnf(c174,plain,
( skc2 != X575
| skf14(skc3,skc2) != X576
| entity(X575,X576) ),
inference(resolution,[status(thm)],[c12,c135]) ).
cnf(c297,plain,
( skc2 != X577
| entity(X577,skf14(skc3,skc2)) ),
inference(resolution,[status(thm)],[c174,reflexivity]) ).
cnf(c11,axiom,
( X247 != X245
| X246 != X248
| ~ organism(X247,X246)
| organism(X245,X248) ),
theory(equality) ).
cnf(c167,plain,
( skc2 != X572
| skf16(skc3,skc2) != X573
| organism(X572,X573) ),
inference(resolution,[status(thm)],[c11,c85]) ).
cnf(c295,plain,
( skc2 != X574
| organism(X574,skf16(skc3,skc2)) ),
inference(resolution,[status(thm)],[c167,reflexivity]) ).
cnf(c166,plain,
( skc2 != X565
| skf18(skc3,skc2) != X566
| organism(X565,X566) ),
inference(resolution,[status(thm)],[c11,c65]) ).
cnf(c293,plain,
( skc2 != X567
| organism(X567,skf18(skc3,skc2)) ),
inference(resolution,[status(thm)],[c166,reflexivity]) ).
cnf(c165,plain,
( skc2 != X558
| skf14(skc3,skc2) != X559
| organism(X558,X559) ),
inference(resolution,[status(thm)],[c11,c131]) ).
cnf(c291,plain,
( skc2 != X564
| organism(X564,skf14(skc3,skc2)) ),
inference(resolution,[status(thm)],[c165,reflexivity]) ).
cnf(c10,axiom,
( X231 != X229
| X230 != X232
| ~ human_person(X231,X230)
| human_person(X229,X232) ),
theory(equality) ).
cnf(c160,plain,
( skc2 != X556
| skf14(skc3,skc2) != X555
| human_person(X556,X555) ),
inference(resolution,[status(thm)],[c10,c130]) ).
cnf(c289,plain,
( skc2 != X557
| human_person(X557,skf14(skc3,skc2)) ),
inference(resolution,[status(thm)],[c160,reflexivity]) ).
cnf(c159,plain,
( skc2 != X553
| skf18(skc3,skc2) != X552
| human_person(X553,X552) ),
inference(resolution,[status(thm)],[c10,c64]) ).
cnf(c287,plain,
( skc2 != X554
| human_person(X554,skf18(skc3,skc2)) ),
inference(resolution,[status(thm)],[c159,reflexivity]) ).
cnf(c158,plain,
( skc2 != X550
| skf16(skc3,skc2) != X549
| human_person(X550,X549) ),
inference(resolution,[status(thm)],[c10,c84]) ).
cnf(c285,plain,
( skc2 != X551
| human_person(X551,skf16(skc3,skc2)) ),
inference(resolution,[status(thm)],[c158,reflexivity]) ).
cnf(c9,axiom,
( X215 != X213
| X214 != X216
| ~ man(X215,X214)
| man(X213,X216) ),
theory(equality) ).
cnf(c153,plain,
( skc2 != X546
| skf18(skc3,skc2) != X547
| man(X546,X547) ),
inference(resolution,[status(thm)],[c9,c62]) ).
cnf(c283,plain,
( skc2 != X548
| man(X548,skf18(skc3,skc2)) ),
inference(resolution,[status(thm)],[c153,reflexivity]) ).
cnf(c152,plain,
( skc2 != X537
| skf16(skc3,skc2) != X538
| man(X537,X538) ),
inference(resolution,[status(thm)],[c9,c82]) ).
cnf(c281,plain,
( skc2 != X545
| man(X545,skf16(skc3,skc2)) ),
inference(resolution,[status(thm)],[c152,reflexivity]) ).
cnf(c47,axiom,
( X542 != X540
| X539 != X543
| X544 != X541
| ~ at(X542,X539,X544)
| at(X540,X543,X541) ),
theory(equality) ).
cnf(c151,plain,
( skc2 != X534
| skf14(skc3,skc2) != X535
| man(X534,X535) ),
inference(resolution,[status(thm)],[c9,c128]) ).
cnf(c279,plain,
( skc2 != X536
| man(X536,skf14(skc3,skc2)) ),
inference(resolution,[status(thm)],[c151,reflexivity]) ).
cnf(c46,axiom,
( X531 != X529
| X528 != X532
| X533 != X530
| ~ with(X531,X528,X533)
| with(X529,X532,X530) ),
theory(equality) ).
cnf(c8,axiom,
( X199 != X197
| X198 != X200
| ~ guy(X199,X198)
| guy(X197,X200) ),
theory(equality) ).
cnf(c146,plain,
( skc2 != X526
| skf16(skc3,skc2) != X525
| guy(X526,X525) ),
inference(resolution,[status(thm)],[c8,c81]) ).
cnf(c277,plain,
( skc2 != X527
| guy(X527,skf16(skc3,skc2)) ),
inference(resolution,[status(thm)],[c146,reflexivity]) ).
cnf(c145,plain,
( skc2 != X523
| skf18(skc3,skc2) != X522
| guy(X523,X522) ),
inference(resolution,[status(thm)],[c8,c61]) ).
cnf(c275,plain,
( skc2 != X524
| guy(X524,skf18(skc3,skc2)) ),
inference(resolution,[status(thm)],[c145,reflexivity]) ).
cnf(c45,axiom,
( X519 != X517
| X516 != X520
| X521 != X518
| ~ agent(X519,X516,X521)
| agent(X517,X520,X518) ),
theory(equality) ).
cnf(c144,plain,
( skc2 != X514
| skf14(skc3,skc2) != X513
| guy(X514,X513) ),
inference(resolution,[status(thm)],[c8,c125]) ).
cnf(c273,plain,
( skc2 != X515
| guy(X515,skf14(skc3,skc2)) ),
inference(resolution,[status(thm)],[c144,reflexivity]) ).
cnf(c44,axiom,
( X511 != X509
| X510 != X512
| ~ present(X511,X510)
| present(X509,X512) ),
theory(equality) ).
cnf(clause35,axiom,
( ~ instrumentality(X72,X71)
| artifact(X72,X71) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause35) ).
cnf(clause34,axiom,
( ~ furniture(X70,X69)
| instrumentality(X70,X69) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause34) ).
cnf(clause33,axiom,
( ~ table(X68,X67)
| furniture(X68,X67) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause33) ).
cnf(clause59,negated_conjecture,
( ~ member(skc2,X156,skc3)
| table(skc2,skf11(X155)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause59) ).
cnf(c105,plain,
table(skc2,skf11(X157)),
inference(resolution,[status(thm)],[clause59,c54]) ).
cnf(c107,plain,
furniture(skc2,skf11(X159)),
inference(resolution,[status(thm)],[c105,clause33]) ).
cnf(c108,plain,
instrumentality(skc2,skf11(X160)),
inference(resolution,[status(thm)],[c107,clause34]) ).
cnf(c109,plain,
artifact(skc2,skf11(X161)),
inference(resolution,[status(thm)],[c108,clause35]) ).
cnf(c41,axiom,
( X491 != X489
| X490 != X492
| ~ artifact(X491,X490)
| artifact(X489,X492) ),
theory(equality) ).
cnf(c265,plain,
( skc2 != X499
| skf11(X501) != X500
| artifact(X499,X500) ),
inference(resolution,[status(thm)],[c41,c109]) ).
cnf(c268,plain,
( skc2 != X503
| artifact(X503,skf11(X502)) ),
inference(resolution,[status(thm)],[c265,reflexivity]) ).
cnf(c40,axiom,
( X487 != X485
| X486 != X488
| ~ instrumentality(X487,X486)
| instrumentality(X485,X488) ),
theory(equality) ).
cnf(c264,plain,
( skc2 != X495
| skf11(X494) != X493
| instrumentality(X495,X493) ),
inference(resolution,[status(thm)],[c40,c108]) ).
cnf(c266,plain,
( skc2 != X497
| instrumentality(X497,skf11(X496)) ),
inference(resolution,[status(thm)],[c264,reflexivity]) ).
cnf(c39,axiom,
( X476 != X474
| X475 != X477
| ~ furniture(X476,X475)
| furniture(X474,X477) ),
theory(equality) ).
cnf(c261,plain,
( skc2 != X481
| skf11(X479) != X480
| furniture(X481,X480) ),
inference(resolution,[status(thm)],[c39,c107]) ).
cnf(c262,plain,
( skc2 != X482
| furniture(X482,skf11(X483)) ),
inference(resolution,[status(thm)],[c261,reflexivity]) ).
cnf(c38,axiom,
( X467 != X465
| X466 != X468
| ~ table(X467,X466)
| table(X465,X468) ),
theory(equality) ).
cnf(c258,plain,
( skc2 != X470
| skf11(X471) != X469
| table(X470,X469) ),
inference(resolution,[status(thm)],[c38,c105]) ).
cnf(c259,plain,
( skc2 != X473
| table(X473,skf11(X472)) ),
inference(resolution,[status(thm)],[c258,reflexivity]) ).
cnf(c37,axiom,
( X463 != X461
| X462 != X464
| ~ nonexistent(X463,X462)
| nonexistent(X461,X464) ),
theory(equality) ).
cnf(c36,axiom,
( X459 != X457
| X458 != X460
| ~ eventuality(X459,X458)
| eventuality(X457,X460) ),
theory(equality) ).
cnf(c35,axiom,
( X455 != X453
| X454 != X456
| ~ event(X455,X454)
| event(X453,X456) ),
theory(equality) ).
cnf(c34,axiom,
( X451 != X449
| X450 != X452
| ~ sit(X451,X450)
| sit(X449,X452) ),
theory(equality) ).
cnf(clause26,axiom,
( ~ object(X54,X53)
| unisex(X54,X53) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause26) ).
cnf(clause36,axiom,
( ~ artifact(X74,X73)
| object(X74,X73) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause36) ).
cnf(c110,plain,
object(skc2,skf11(X165)),
inference(resolution,[status(thm)],[c109,clause36]) ).
cnf(c112,plain,
unisex(skc2,skf11(X167)),
inference(resolution,[status(thm)],[c110,clause26]) ).
cnf(c33,axiom,
( X440 != X438
| X439 != X441
| ~ unisex(X440,X439)
| unisex(X438,X441) ),
theory(equality) ).
cnf(c255,plain,
( skc2 != X444
| skf11(X443) != X445
| unisex(X444,X445) ),
inference(resolution,[status(thm)],[c33,c112]) ).
cnf(c256,plain,
( skc2 != X446
| unisex(X446,skf11(X447)) ),
inference(resolution,[status(thm)],[c255,reflexivity]) ).
cnf(clause24,axiom,
( ~ object(X50,X49)
| nonliving(X50,X49) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause24) ).
cnf(c114,plain,
nonliving(skc2,skf11(X169)),
inference(resolution,[status(thm)],[c110,clause24]) ).
cnf(c32,axiom,
( X425 != X423
| X424 != X426
| ~ nonliving(X425,X424)
| nonliving(X423,X426) ),
theory(equality) ).
cnf(c250,plain,
( skc2 != X433
| skf11(X434) != X435
| nonliving(X433,X435) ),
inference(resolution,[status(thm)],[c32,c114]) ).
cnf(c253,plain,
( skc2 != X437
| nonliving(X437,skf11(X436)) ),
inference(resolution,[status(thm)],[c250,reflexivity]) ).
cnf(c31,axiom,
( X421 != X419
| X420 != X422
| ~ object(X421,X420)
| object(X419,X422) ),
theory(equality) ).
cnf(c249,plain,
( skc2 != X428
| skf11(X427) != X429
| object(X428,X429) ),
inference(resolution,[status(thm)],[c31,c110]) ).
cnf(c251,plain,
( skc2 != X430
| object(X430,skf11(X431)) ),
inference(resolution,[status(thm)],[c249,reflexivity]) ).
cnf(c30,axiom,
( X417 != X415
| X416 != X418
| ~ substance_matter(X417,X416)
| substance_matter(X415,X418) ),
theory(equality) ).
cnf(c29,axiom,
( X413 != X411
| X412 != X414
| ~ food(X413,X412)
| food(X411,X414) ),
theory(equality) ).
cnf(c28,axiom,
( X409 != X407
| X408 != X410
| ~ meat(X409,X408)
| meat(X407,X410) ),
theory(equality) ).
cnf(c27,axiom,
( X404 != X402
| X403 != X405
| ~ burger(X404,X403)
| burger(X402,X405) ),
theory(equality) ).
cnf(clause16,axiom,
( ~ set(X34,X33)
| multiple(X34,X33) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause16) ).
cnf(clause15,axiom,
( ~ group(X32,X31)
| set(X32,X31) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause15) ).
cnf(clause58,negated_conjecture,
( ~ member(skc2,X150,skc3)
| group(skc2,skf9(X149)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause58) ).
cnf(c101,plain,
group(skc2,skf9(X151)),
inference(resolution,[status(thm)],[clause58,c54]) ).
cnf(c103,plain,
set(skc2,skf9(X153)),
inference(resolution,[status(thm)],[c101,clause15]) ).
cnf(c104,plain,
multiple(skc2,skf9(X154)),
inference(resolution,[status(thm)],[c103,clause16]) ).
cnf(c24,axiom,
( X369 != X367
| X368 != X370
| ~ multiple(X369,X368)
| multiple(X367,X370) ),
theory(equality) ).
cnf(c237,plain,
( skc2 != X397
| skf9(X398) != X399
| multiple(X397,X399) ),
inference(resolution,[status(thm)],[c24,c104]) ).
cnf(c247,plain,
( skc2 != X400
| multiple(X400,skf9(X401)) ),
inference(resolution,[status(thm)],[c237,reflexivity]) ).
cnf(c23,axiom,
( X359 != X357
| X358 != X360
| ~ set(X359,X358)
| set(X357,X360) ),
theory(equality) ).
cnf(c231,plain,
( skc2 != X392
| skf9(X391) != X393
| set(X392,X393) ),
inference(resolution,[status(thm)],[c23,c103]) ).
cnf(c245,plain,
( skc2 != X394
| set(X394,skf9(X395)) ),
inference(resolution,[status(thm)],[c231,reflexivity]) ).
cnf(c26,axiom,
( X389 != X387
| X388 != X390
| ~ hamburger(X389,X388)
| hamburger(X387,X390) ),
theory(equality) ).
cnf(c25,axiom,
( X379 != X377
| X378 != X380
| ~ three(X379,X378)
| three(X377,X380) ),
theory(equality) ).
cnf(c241,plain,
( skc2 != X385
| skc3 != X384
| three(X385,X384) ),
inference(resolution,[status(thm)],[c25,clause54]) ).
cnf(c243,plain,
( skc2 != X386
| three(X386,skc3) ),
inference(resolution,[status(thm)],[c241,reflexivity]) ).
cnf(c22,axiom,
( X355 != X353
| X354 != X356
| ~ group(X355,X354)
| group(X353,X356) ),
theory(equality) ).
cnf(c228,plain,
( skc2 != X375
| skf9(X376) != X374
| group(X375,X374) ),
inference(resolution,[status(thm)],[c22,c101]) ).
cnf(c240,plain,
( skc2 != X381
| group(X381,skf9(X382)) ),
inference(resolution,[status(thm)],[c228,reflexivity]) ).
cnf(clause55,negated_conjecture,
group(skc2,skc3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause55) ).
cnf(c48,plain,
set(skc2,skc3),
inference(resolution,[status(thm)],[clause15,clause55]) ).
cnf(c49,plain,
multiple(skc2,skc3),
inference(resolution,[status(thm)],[clause16,c48]) ).
cnf(c236,plain,
( skc2 != X371
| skc3 != X372
| multiple(X371,X372) ),
inference(resolution,[status(thm)],[c24,c49]) ).
cnf(c238,plain,
( skc2 != X373
| multiple(X373,skc3) ),
inference(resolution,[status(thm)],[c236,reflexivity]) ).
cnf(c230,plain,
( skc2 != X364
| skc3 != X365
| set(X364,X365) ),
inference(resolution,[status(thm)],[c23,c48]) ).
cnf(c234,plain,
( skc2 != X366
| set(X366,skc3) ),
inference(resolution,[status(thm)],[c230,reflexivity]) ).
cnf(c229,plain,
( skc2 != X362
| skc3 != X361
| group(X362,X361) ),
inference(resolution,[status(thm)],[c22,clause55]) ).
cnf(c232,plain,
( skc2 != X363
| group(X363,skc3) ),
inference(resolution,[status(thm)],[c229,reflexivity]) ).
cnf(clause25,axiom,
( ~ object(X52,X51)
| impartial(X52,X51) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause25) ).
cnf(c113,plain,
impartial(skc2,skf11(X168)),
inference(resolution,[status(thm)],[c110,clause25]) ).
cnf(c210,plain,
( skc2 != X332
| skf11(X333) != X331
| impartial(X332,X331) ),
inference(resolution,[status(thm)],[c17,c113]) ).
cnf(c214,plain,
( skc2 != X334
| impartial(X334,skf11(X335)) ),
inference(resolution,[status(thm)],[c210,reflexivity]) ).
cnf(clause23,axiom,
( ~ object(X48,X47)
| entity(X48,X47) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause23) ).
cnf(c111,plain,
entity(skc2,skf11(X166)),
inference(resolution,[status(thm)],[c110,clause23]) ).
cnf(c115,plain,
existent(skc2,skf11(X174)),
inference(resolution,[status(thm)],[c111,clause9]) ).
cnf(c207,plain,
( skc2 != X325
| skf11(X326) != X327
| existent(X325,X327) ),
inference(resolution,[status(thm)],[c16,c115]) ).
cnf(c212,plain,
( skc2 != X328
| existent(X328,skf11(X329)) ),
inference(resolution,[status(thm)],[c207,reflexivity]) ).
cnf(c116,plain,
specific(skc2,skf11(X175)),
inference(resolution,[status(thm)],[c111,clause8]) ).
cnf(c201,plain,
( skc2 != X312
| skf11(X311) != X313
| specific(X312,X313) ),
inference(resolution,[status(thm)],[c15,c116]) ).
cnf(c202,plain,
( skc2 != X315
| specific(X315,skf11(X314)) ),
inference(resolution,[status(thm)],[c201,reflexivity]) ).
cnf(c117,plain,
thing(skc2,skf11(X176)),
inference(resolution,[status(thm)],[c111,clause6]) ).
cnf(c121,plain,
singleton(skc2,skf11(X184)),
inference(resolution,[status(thm)],[c117,clause7]) ).
cnf(c192,plain,
( skc2 != X303
| skf11(X301) != X302
| singleton(X303,X302) ),
inference(resolution,[status(thm)],[c14,c121]) ).
cnf(c196,plain,
( skc2 != X304
| singleton(X304,skf11(X305)) ),
inference(resolution,[status(thm)],[c192,reflexivity]) ).
cnf(c179,plain,
( skc2 != X287
| skf11(X285) != X286
| thing(X287,X286) ),
inference(resolution,[status(thm)],[c13,c117]) ).
cnf(c187,plain,
( skc2 != X294
| thing(X294,skf11(X295)) ),
inference(resolution,[status(thm)],[c179,reflexivity]) ).
cnf(c6,axiom,
( X275 != X273
| X274 != X276
| skf12(X275,X274) = skf12(X273,X276) ),
theory(equality) ).
cnf(c184,plain,
( X280 != X282
| skf12(X280,X281) = skf12(X282,X281) ),
inference(resolution,[status(thm)],[c6,reflexivity]) ).
cnf(c183,plain,
( X277 != X278
| skf12(X277,X277) = skf12(X278,X278) ),
inference(factor,[status(thm)],[c6]) ).
cnf(c173,plain,
( skc2 != X263
| skf11(X264) != X265
| entity(X263,X265) ),
inference(resolution,[status(thm)],[c12,c111]) ).
cnf(c177,plain,
( skc2 != X266
| entity(X266,skf11(X267)) ),
inference(resolution,[status(thm)],[c173,reflexivity]) ).
cnf(c2,axiom,
( X235 != X233
| X234 != X236
| skf14(X235,X234) = skf14(X233,X236) ),
theory(equality) ).
cnf(c162,plain,
( X240 != X241
| skf14(X240,X242) = skf14(X241,X242) ),
inference(resolution,[status(thm)],[c2,reflexivity]) ).
cnf(c161,plain,
( X237 != X238
| skf14(X237,X237) = skf14(X238,X238) ),
inference(factor,[status(thm)],[c2]) ).
cnf(c1,axiom,
( X219 != X217
| X218 != X220
| skf16(X219,X218) = skf16(X217,X220) ),
theory(equality) ).
cnf(c155,plain,
( X224 != X225
| skf16(X224,X226) = skf16(X225,X226) ),
inference(resolution,[status(thm)],[c1,reflexivity]) ).
cnf(c154,plain,
( X222 != X221
| skf16(X222,X222) = skf16(X221,X221) ),
inference(factor,[status(thm)],[c1]) ).
cnf(c0,axiom,
( X203 != X201
| X202 != X204
| skf18(X203,X202) = skf18(X201,X204) ),
theory(equality) ).
cnf(c148,plain,
( X210 != X209
| skf18(X210,X208) = skf18(X209,X208) ),
inference(resolution,[status(thm)],[c0,reflexivity]) ).
cnf(c147,plain,
( X205 != X206
| skf18(X205,X205) = skf18(X206,X206) ),
inference(factor,[status(thm)],[c0]) ).
cnf(clause38,axiom,
( ~ multiple(X78,X77)
| ~ singleton(X78,X77) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause38) ).
cnf(c143,plain,
~ multiple(skc2,skf14(skc3,skc2)),
inference(resolution,[status(thm)],[c142,clause38]) ).
cnf(clause40,axiom,
( ~ nonexistent(X82,X81)
| ~ existent(X82,X81) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause40) ).
cnf(c141,plain,
~ nonexistent(skc2,skf14(skc3,skc2)),
inference(resolution,[status(thm)],[c138,clause40]) ).
cnf(clause66,negated_conjecture,
( ~ member(skc2,X196,skf9(X195))
| ~ member(skc2,X195,skc3)
| at(skc2,skf12(X196,X195),skf11(X195)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause66) ).
cnf(clause41,axiom,
( ~ nonliving(X84,X83)
| ~ animate(X84,X83) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause41) ).
cnf(c137,plain,
~ nonliving(skc2,skf14(skc3,skc2)),
inference(resolution,[status(thm)],[c132,clause41]) ).
cnf(clause65,negated_conjecture,
( ~ member(skc2,X193,skf9(X192))
| ~ member(skc2,X192,skc3)
| with(skc2,skf12(X193,X194),X193) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause65) ).
cnf(clause64,negated_conjecture,
( ~ member(skc2,X191,skf9(X190))
| ~ member(skc2,X190,skc3)
| agent(skc2,skf12(X191,X190),X190) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause64) ).
cnf(clause63,negated_conjecture,
( ~ member(skc2,X188,skf9(X186))
| ~ member(skc2,X186,skc3)
| sit(skc2,skf12(X189,X187)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause63) ).
cnf(c123,plain,
~ multiple(skc2,skf16(skc3,skc2)),
inference(resolution,[status(thm)],[c100,clause38]) ).
cnf(c122,plain,
~ multiple(skc2,skf11(X185)),
inference(resolution,[status(thm)],[c121,clause38]) ).
cnf(c120,plain,
~ nonexistent(skc2,skf11(X183)),
inference(resolution,[status(thm)],[c115,clause40]) ).
cnf(clause62,negated_conjecture,
( ~ member(skc2,X181,skf9(X179))
| ~ member(skc2,X179,skc3)
| present(skc2,skf12(X182,X180)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause62) ).
cnf(clause39,axiom,
( ~ living(X80,X79)
| ~ nonliving(X80,X79) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause39) ).
cnf(c119,plain,
~ living(skc2,skf11(X178)),
inference(resolution,[status(thm)],[c114,clause39]) ).
cnf(clause37,axiom,
( ~ male(X76,X75)
| ~ unisex(X76,X75) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause37) ).
cnf(c118,plain,
~ male(skc2,skf11(X177)),
inference(resolution,[status(thm)],[c112,clause37]) ).
cnf(clause61,negated_conjecture,
( ~ member(skc2,X172,skf9(X170))
| ~ member(skc2,X170,skc3)
| event(skc2,skf12(X173,X171)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause61) ).
cnf(clause60,negated_conjecture,
( ~ member(skc2,X163,skf9(X162))
| ~ member(skc2,X164,skc3)
| hamburger(skc2,X163) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause60) ).
cnf(c99,plain,
~ nonexistent(skc2,skf16(skc3,skc2)),
inference(resolution,[status(thm)],[c92,clause40]) ).
cnf(c91,plain,
~ nonliving(skc2,skf16(skc3,skc2)),
inference(resolution,[status(thm)],[c86,clause41]) ).
cnf(clause52,axiom,
( ~ member(X147,X144,X146)
| ~ member(X147,X148,X146)
| ~ member(X147,X145,X146)
| three(X147,X146)
| member(X147,skf19(X144,X148,X145,X146,X147),X146)
| X144 = X145
| X144 = X148
| X148 = X145 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause52) ).
cnf(clause51,axiom,
( skf19(X141,X137,X139,X143,X138) != X139
| ~ member(X142,X141,X140)
| ~ member(X142,X137,X140)
| ~ member(X142,X139,X140)
| three(X142,X140)
| X141 = X139
| X141 = X137
| X137 = X139 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause51) ).
cnf(clause50,axiom,
( skf19(X134,X129,X132,X136,X131) != X129
| ~ member(X135,X134,X133)
| ~ member(X135,X129,X133)
| ~ member(X135,X130,X133)
| three(X135,X133)
| X134 = X130
| X134 = X129
| X129 = X130 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause50) ).
cnf(c78,plain,
~ multiple(skc2,skf18(skc3,skc2)),
inference(resolution,[status(thm)],[c77,clause38]) ).
cnf(c76,plain,
~ nonexistent(skc2,skf18(skc3,skc2)),
inference(resolution,[status(thm)],[c73,clause40]) ).
cnf(clause49,axiom,
( skf19(X125,X120,X123,X127,X122) != X125
| ~ member(X126,X125,X124)
| ~ member(X126,X121,X124)
| ~ member(X126,X128,X124)
| three(X126,X124)
| X125 = X128
| X125 = X121
| X121 = X128 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause49) ).
cnf(c71,plain,
~ nonliving(skc2,skf18(skc3,skc2)),
inference(resolution,[status(thm)],[c66,clause41]) ).
cnf(clause48,axiom,
( ~ member(X118,X117,X119)
| ~ three(X118,X119)
| X117 = skf14(X119,X118)
| X117 = skf16(X119,X118)
| X117 = skf18(X119,X118) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause48) ).
cnf(clause47,axiom,
( skf16(X116,X115) != skf14(X116,X115)
| ~ three(X115,X116) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause47) ).
cnf(clause46,axiom,
( skf18(X114,X113) != skf16(X114,X113)
| ~ three(X113,X114) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause46) ).
cnf(c5,axiom,
( X111 != X110
| skf11(X111) = skf11(X110) ),
theory(equality) ).
cnf(c4,axiom,
( X108 != X107
| skf9(X108) = skf9(X107) ),
theory(equality) ).
cnf(clause45,axiom,
( skf18(X104,X103) != skf14(X104,X103)
| ~ three(X103,X104) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause45) ).
cnf(transitivity,axiom,
( X99 != X100
| X100 != X101
| X99 = X101 ),
theory(equality) ).
cnf(c42,axiom,
( X89 != X88
| ~ actual_world(X89)
| actual_world(X88) ),
theory(equality) ).
cnf(symmetry,axiom,
( X85 != X86
| X86 = X85 ),
theory(equality) ).
cnf(clause32,axiom,
( ~ eventuality(X66,X65)
| unisex(X66,X65) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause32) ).
cnf(clause31,axiom,
( ~ eventuality(X64,X63)
| nonexistent(X64,X63) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause31) ).
cnf(clause30,axiom,
( ~ eventuality(X62,X61)
| specific(X62,X61) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause30) ).
cnf(clause29,axiom,
( ~ eventuality(X60,X59)
| thing(X60,X59) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause29) ).
cnf(clause28,axiom,
( ~ event(X58,X57)
| eventuality(X58,X57) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause28) ).
cnf(clause27,axiom,
( ~ sit(X56,X55)
| event(X56,X55) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause27) ).
cnf(clause22,axiom,
( ~ substance_matter(X46,X45)
| object(X46,X45) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause22) ).
cnf(clause21,axiom,
( ~ food(X44,X43)
| substance_matter(X44,X43) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause21) ).
cnf(clause20,axiom,
( ~ meat(X42,X41)
| food(X42,X41) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause20) ).
cnf(clause19,axiom,
( ~ burger(X40,X39)
| meat(X40,X39) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause19) ).
cnf(clause18,axiom,
( ~ hamburger(X38,X37)
| burger(X38,X37) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause18) ).
cnf(clause17,axiom,
( ~ three(X36,X35)
| group(X36,X35) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause17) ).
cnf(clause1,axiom,
~ member(X4,X3,X3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
cnf(clause53,negated_conjecture,
actual_world(skc2),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause53) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.11/0.12 % Problem : NLP039-1 : TPTP v8.1.2. Released v2.4.0.
% 0.11/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n026.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 : Wed May 8 13:46:53 EDT 2024
% 0.13/0.34 % CPUTime :
% 1.81/2.00 % Version: 1.5
% 1.81/2.00 % SZS status Satisfiable
% 1.81/2.00 % SZS output start Saturation
% See solution above
% 1.81/2.01
% 1.81/2.01 % Initial clauses : 117
% 1.81/2.01 % Processed clauses : 454
% 1.81/2.01 % Factors computed : 97
% 1.81/2.01 % Resolvents computed: 424
% 1.81/2.01 % Tautologies deleted: 3
% 1.81/2.01 % Forward subsumed : 181
% 1.81/2.01 % Backward subsumed : 49
% 1.81/2.01 % -------- CPU Time ---------
% 1.81/2.01 % User time : 1.634 s
% 1.81/2.01 % System time : 0.014 s
% 1.81/2.01 % Total time : 1.648 s
%------------------------------------------------------------------------------