%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP040-1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n032.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:45 EDT 2024
% Result : Satisfiable 1.60s 1.80s
% Output : Saturation 1.60s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c3,axiom,
( X381 != X379
| X383 != X377
| X384 != X376
| X380 != X375
| X382 != X378
| skf19(X381,X383,X384,X380,X382) = skf19(X379,X377,X376,X375,X378) ),
theory(equality) ).
cnf(c86,plain,
( X557 != X550
| X551 != X556
| X549 != X553
| X555 != X552
| skf19(X557,X551,X549,X555,X554) = skf19(X550,X556,X553,X552,X554) ),
inference(resolution,[status(thm)],[c3,reflexivity]) ).
cnf(c136,plain,
( X976 != X972
| X970 != X975
| X971 != X973
| skf19(X976,X970,X971,X974,X969) = skf19(X972,X975,X973,X974,X969) ),
inference(resolution,[status(thm)],[c86,reflexivity]) ).
cnf(c234,plain,
( X1220 != X1222
| X1226 != X1224
| skf19(X1220,X1226,X1225,X1221,X1223) = skf19(X1222,X1224,X1225,X1221,X1223) ),
inference(resolution,[status(thm)],[c136,reflexivity]) ).
cnf(c281,plain,
( X1247 != X1250
| skf19(X1247,X1249,X1246,X1248,X1245) = skf19(X1250,X1249,X1246,X1248,X1245) ),
inference(resolution,[status(thm)],[c234,reflexivity]) ).
cnf(c280,plain,
( X1237 != X1240
| skf19(X1237,X1237,X1238,X1239,X1236) = skf19(X1240,X1240,X1238,X1239,X1236) ),
inference(factor,[status(thm)],[c234]) ).
cnf(c232,plain,
( X1190 != X1193
| X1192 != X1191
| skf19(X1190,X1192,X1190,X1188,X1189) = skf19(X1193,X1191,X1193,X1188,X1189) ),
inference(factor,[status(thm)],[c136]) ).
cnf(c275,plain,
( X1209 != X1211
| skf19(X1209,X1210,X1209,X1208,X1207) = skf19(X1211,X1210,X1211,X1208,X1207) ),
inference(resolution,[status(thm)],[c232,reflexivity]) ).
cnf(c274,plain,
( X1201 != X1202
| skf19(X1201,X1201,X1201,X1200,X1203) = skf19(X1202,X1202,X1202,X1200,X1203) ),
inference(factor,[status(thm)],[c232]) ).
cnf(c233,plain,
( X1194 != X1196
| X1198 != X1199
| skf19(X1194,X1198,X1198,X1195,X1197) = skf19(X1196,X1199,X1199,X1195,X1197) ),
inference(factor,[status(thm)],[c136]) ).
cnf(c134,plain,
( X922 != X920
| X923 != X918
| X919 != X921
| skf19(X922,X923,X919,X923,X917) = skf19(X920,X918,X921,X918,X917) ),
inference(factor,[status(thm)],[c86]) ).
cnf(c224,plain,
( X1141 != X1139
| X1137 != X1142
| skf19(X1141,X1137,X1140,X1137,X1138) = skf19(X1139,X1142,X1140,X1142,X1138) ),
inference(resolution,[status(thm)],[c134,reflexivity]) ).
cnf(c223,plain,
( X1118 != X1116
| X1117 != X1115
| skf19(X1118,X1117,X1117,X1117,X1119) = skf19(X1116,X1115,X1115,X1115,X1119) ),
inference(factor,[status(thm)],[c134]) ).
cnf(c133,plain,
( X896 != X891
| X892 != X895
| X893 != X894
| skf19(X896,X892,X893,X896,X890) = skf19(X891,X895,X894,X891,X890) ),
inference(factor,[status(thm)],[c86]) ).
cnf(c218,plain,
( X1090 != X1088
| X1089 != X1086
| skf19(X1090,X1089,X1085,X1090,X1087) = skf19(X1088,X1086,X1085,X1088,X1087) ),
inference(resolution,[status(thm)],[c133,reflexivity]) ).
cnf(c258,plain,
( X1103 != X1104
| skf19(X1103,X1105,X1106,X1103,X1107) = skf19(X1104,X1105,X1106,X1104,X1107) ),
inference(resolution,[status(thm)],[c218,reflexivity]) ).
cnf(c257,plain,
( X1098 != X1096
| skf19(X1098,X1098,X1097,X1098,X1099) = skf19(X1096,X1096,X1097,X1096,X1099) ),
inference(factor,[status(thm)],[c218]) ).
cnf(c222,plain,
( X1094 != X1093
| X1091 != X1095
| skf19(X1094,X1091,X1094,X1091,X1092) = skf19(X1093,X1095,X1093,X1095,X1092) ),
inference(factor,[status(thm)],[c134]) ).
cnf(c217,plain,
( X1070 != X1069
| X1067 != X1071
| skf19(X1070,X1067,X1067,X1070,X1068) = skf19(X1069,X1071,X1071,X1069,X1068) ),
inference(factor,[status(thm)],[c133]) ).
cnf(c216,plain,
( X1045 != X1048
| X1047 != X1044
| skf19(X1045,X1047,X1045,X1045,X1046) = skf19(X1048,X1044,X1048,X1048,X1046) ),
inference(factor,[status(thm)],[c133]) ).
cnf(c250,plain,
( X1065 != X1064
| skf19(X1065,X1063,X1065,X1065,X1066) = skf19(X1064,X1063,X1064,X1064,X1066) ),
inference(resolution,[status(thm)],[c216,reflexivity]) ).
cnf(c249,plain,
( X1060 != X1058
| skf19(X1060,X1060,X1060,X1060,X1059) = skf19(X1058,X1058,X1058,X1058,X1059) ),
inference(factor,[status(thm)],[c216]) ).
cnf(c135,plain,
( X948 != X946
| X945 != X947
| X949 != X944
| skf19(X948,X945,X949,X949,X943) = skf19(X946,X947,X944,X944,X943) ),
inference(factor,[status(thm)],[c86]) ).
cnf(c83,plain,
( X480 != X475
| X474 != X478
| X473 != X477
| X479 != X476
| skf19(X480,X474,X473,X479,X474) = skf19(X475,X478,X477,X476,X478) ),
inference(factor,[status(thm)],[c3]) ).
cnf(c109,plain,
( X679 != X675
| X673 != X678
| X674 != X677
| skf19(X679,X673,X674,X676,X673) = skf19(X675,X678,X677,X676,X678) ),
inference(resolution,[status(thm)],[c83,reflexivity]) ).
cnf(c169,plain,
( X835 != X838
| X833 != X834
| skf19(X835,X833,X837,X836,X833) = skf19(X838,X834,X837,X836,X834) ),
inference(resolution,[status(thm)],[c109,reflexivity]) ).
cnf(c168,plain,
( X819 != X822
| X821 != X818
| skf19(X819,X821,X821,X820,X821) = skf19(X822,X818,X818,X820,X818) ),
inference(factor,[status(thm)],[c109]) ).
cnf(c167,plain,
( X801 != X797
| X798 != X799
| skf19(X801,X798,X801,X800,X798) = skf19(X797,X799,X797,X800,X799) ),
inference(factor,[status(thm)],[c109]) ).
cnf(c84,plain,
( X506 != X500
| X501 != X505
| X499 != X503
| X504 != X502
| skf19(X506,X501,X499,X504,X499) = skf19(X500,X505,X503,X502,X503) ),
inference(factor,[status(thm)],[c3]) ).
cnf(c119,plain,
( X761 != X765
| X766 != X764
| X763 != X767
| skf19(X761,X766,X763,X762,X763) = skf19(X765,X764,X767,X762,X767) ),
inference(resolution,[status(thm)],[c84,reflexivity]) ).
cnf(c107,plain,
( X630 != X628
| X627 != X625
| X626 != X629
| skf19(X630,X627,X626,X627,X627) = skf19(X628,X625,X629,X625,X625) ),
inference(factor,[status(thm)],[c83]) ).
cnf(c156,plain,
( X747 != X748
| X750 != X746
| skf19(X747,X750,X749,X750,X750) = skf19(X748,X746,X749,X746,X746) ),
inference(resolution,[status(thm)],[c107,reflexivity]) ).
cnf(c118,plain,
( X738 != X741
| X743 != X739
| X740 != X742
| skf19(X738,X743,X740,X740,X740) = skf19(X741,X739,X742,X742,X742) ),
inference(factor,[status(thm)],[c84]) ).
cnf(c155,plain,
( X730 != X732
| X729 != X731
| skf19(X730,X729,X729,X729,X729) = skf19(X732,X731,X731,X731,X731) ),
inference(factor,[status(thm)],[c107]) ).
cnf(c117,plain,
( X718 != X721
| X720 != X722
| X719 != X723
| skf19(X718,X720,X719,X720,X719) = skf19(X721,X722,X723,X722,X723) ),
inference(factor,[status(thm)],[c84]) ).
cnf(c154,plain,
( X712 != X714
| X715 != X713
| skf19(X712,X715,X712,X715,X715) = skf19(X714,X713,X714,X713,X713) ),
inference(factor,[status(thm)],[c107]) ).
cnf(c116,plain,
( X698 != X699
| X700 != X697
| X696 != X701
| skf19(X698,X700,X696,X698,X696) = skf19(X699,X697,X701,X699,X701) ),
inference(factor,[status(thm)],[c84]) ).
cnf(c106,plain,
( X603 != X601
| X600 != X605
| X602 != X604
| skf19(X603,X600,X602,X603,X600) = skf19(X601,X605,X604,X601,X605) ),
inference(factor,[status(thm)],[c83]) ).
cnf(c149,plain,
( X692 != X693
| X691 != X695
| skf19(X692,X691,X694,X692,X691) = skf19(X693,X695,X694,X693,X695) ),
inference(resolution,[status(thm)],[c106,reflexivity]) ).
cnf(c148,plain,
( X682 != X681
| X683 != X680
| skf19(X682,X683,X683,X682,X683) = skf19(X681,X680,X680,X681,X680) ),
inference(factor,[status(thm)],[c106]) ).
cnf(c147,plain,
( X663 != X662
| X664 != X665
| skf19(X663,X664,X663,X663,X664) = skf19(X662,X665,X662,X662,X665) ),
inference(factor,[status(thm)],[c106]) ).
cnf(c108,plain,
( X657 != X655
| X652 != X656
| X654 != X653
| skf19(X657,X652,X654,X654,X652) = skf19(X655,X656,X653,X653,X656) ),
inference(factor,[status(thm)],[c83]) ).
cnf(c82,plain,
( X415 != X419
| X416 != X421
| X414 != X418
| X420 != X417
| skf19(X415,X416,X414,X420,X415) = skf19(X419,X421,X418,X417,X419) ),
inference(factor,[status(thm)],[c3]) ).
cnf(c91,plain,
( X577 != X579
| X582 != X578
| X580 != X576
| skf19(X577,X582,X580,X581,X577) = skf19(X579,X578,X576,X581,X579) ),
inference(resolution,[status(thm)],[c82,reflexivity]) ).
cnf(c142,plain,
( X634 != X638
| X636 != X637
| skf19(X634,X636,X639,X635,X634) = skf19(X638,X637,X639,X635,X638) ),
inference(resolution,[status(thm)],[c91,reflexivity]) ).
cnf(c158,plain,
( X647 != X648
| skf19(X647,X650,X651,X649,X647) = skf19(X648,X650,X651,X649,X648) ),
inference(resolution,[status(thm)],[c142,reflexivity]) ).
cnf(c157,plain,
( X641 != X643
| skf19(X641,X641,X640,X642,X641) = skf19(X643,X643,X640,X642,X643) ),
inference(factor,[status(thm)],[c142]) ).
cnf(c141,plain,
( X613 != X617
| X614 != X616
| skf19(X613,X614,X614,X615,X613) = skf19(X617,X616,X616,X615,X617) ),
inference(factor,[status(thm)],[c91]) ).
cnf(c140,plain,
( X590 != X593
| X592 != X594
| skf19(X590,X592,X590,X591,X590) = skf19(X593,X594,X593,X591,X593) ),
inference(factor,[status(thm)],[c91]) ).
cnf(c145,plain,
( X609 != X608
| skf19(X609,X606,X609,X607,X609) = skf19(X608,X606,X608,X607,X608) ),
inference(resolution,[status(thm)],[c140,reflexivity]) ).
cnf(c144,plain,
( X597 != X595
| skf19(X597,X597,X597,X596,X597) = skf19(X595,X595,X595,X596,X595) ),
inference(factor,[status(thm)],[c140]) ).
cnf(c90,plain,
( X544 != X546
| X547 != X545
| X543 != X548
| skf19(X544,X547,X543,X543,X544) = skf19(X546,X545,X548,X548,X546) ),
inference(factor,[status(thm)],[c82]) ).
cnf(c89,plain,
( X486 != X487
| X485 != X489
| X488 != X484
| skf19(X486,X485,X488,X485,X486) = skf19(X487,X489,X484,X489,X487) ),
inference(factor,[status(thm)],[c82]) ).
cnf(c112,plain,
( X531 != X529
| X528 != X532
| skf19(X531,X528,X530,X528,X531) = skf19(X529,X532,X530,X532,X529) ),
inference(resolution,[status(thm)],[c89,reflexivity]) ).
cnf(c85,plain,
( X527 != X521
| X522 != X526
| X520 != X524
| X523 != X525
| skf19(X527,X522,X520,X523,X523) = skf19(X521,X526,X524,X525,X525) ),
inference(factor,[status(thm)],[c3]) ).
cnf(c111,plain,
( X510 != X512
| X509 != X511
| skf19(X510,X509,X509,X509,X510) = skf19(X512,X511,X511,X511,X512) ),
inference(factor,[status(thm)],[c89]) ).
cnf(c110,plain,
( X491 != X493
| X492 != X490
| skf19(X491,X492,X491,X492,X491) = skf19(X493,X490,X493,X490,X493) ),
inference(factor,[status(thm)],[c89]) ).
cnf(c88,plain,
( X423 != X427
| X426 != X424
| X425 != X422
| skf19(X423,X426,X425,X423,X423) = skf19(X427,X424,X422,X427,X427) ),
inference(factor,[status(thm)],[c82]) ).
cnf(c94,plain,
( X462 != X463
| X459 != X461
| skf19(X462,X459,X460,X462,X462) = skf19(X463,X461,X460,X463,X463) ),
inference(resolution,[status(thm)],[c88,reflexivity]) ).
cnf(c103,plain,
( X472 != X471
| skf19(X472,X469,X470,X472,X472) = skf19(X471,X469,X470,X471,X471) ),
inference(resolution,[status(thm)],[c94,reflexivity]) ).
cnf(c102,plain,
( X466 != X464
| skf19(X466,X466,X465,X466,X466) = skf19(X464,X464,X465,X464,X464) ),
inference(factor,[status(thm)],[c94]) ).
cnf(c93,plain,
( X445 != X447
| X446 != X444
| skf19(X445,X446,X446,X445,X445) = skf19(X447,X444,X444,X447,X447) ),
inference(factor,[status(thm)],[c88]) ).
cnf(c92,plain,
( X431 != X428
| X430 != X429
| skf19(X431,X430,X431,X431,X431) = skf19(X428,X429,X428,X428,X428) ),
inference(factor,[status(thm)],[c88]) ).
cnf(c96,plain,
( X440 != X441
| skf19(X440,X439,X440,X440,X440) = skf19(X441,X439,X441,X441,X441) ),
inference(resolution,[status(thm)],[c92,reflexivity]) ).
cnf(c95,plain,
( X432 != X433
| skf19(X432,X432,X432,X432,X432) = skf19(X433,X433,X433,X433,X433) ),
inference(factor,[status(thm)],[c92]) ).
cnf(c47,axiom,
( X411 != X410
| X412 != X409
| X413 != X408
| ~ at(X411,X412,X413)
| at(X410,X409,X408) ),
theory(equality) ).
cnf(c46,axiom,
( X405 != X404
| X406 != X403
| X407 != X402
| ~ with(X405,X406,X407)
| with(X404,X403,X402) ),
theory(equality) ).
cnf(c45,axiom,
( X399 != X398
| X400 != X397
| X401 != X396
| ~ agent(X399,X400,X401)
| agent(X398,X397,X396) ),
theory(equality) ).
cnf(c7,axiom,
( X393 != X392
| X394 != X391
| X395 != X390
| ~ member(X393,X394,X395)
| member(X392,X391,X390) ),
theory(equality) ).
cnf(c6,axiom,
( X369 != X371
| X368 != X370
| skf12(X369,X368) = skf12(X371,X370) ),
theory(equality) ).
cnf(c80,plain,
( X387 != X386
| skf12(X387,X385) = skf12(X386,X385) ),
inference(resolution,[status(thm)],[c6,reflexivity]) ).
cnf(c79,plain,
( X372 != X373
| skf12(X372,X372) = skf12(X373,X373) ),
inference(factor,[status(thm)],[c6]) ).
cnf(c2,axiom,
( X355 != X357
| X354 != X356
| skf14(X355,X354) = skf14(X357,X356) ),
theory(equality) ).
cnf(c76,plain,
( X365 != X364
| skf14(X365,X363) = skf14(X364,X363) ),
inference(resolution,[status(thm)],[c2,reflexivity]) ).
cnf(clause66,negated_conjecture,
( ~ member(skc2,X361,skf9(X362))
| ~ member(skc2,X362,skc3)
| at(skc2,skf12(X361,X362),skf11(X362)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause66) ).
cnf(c75,plain,
( X358 != X359
| skf14(X358,X358) = skf14(X359,X359) ),
inference(factor,[status(thm)],[c2]) ).
cnf(c1,axiom,
( X341 != X343
| X340 != X342
| skf16(X341,X340) = skf16(X343,X342) ),
theory(equality) ).
cnf(c72,plain,
( X349 != X351
| skf16(X349,X350) = skf16(X351,X350) ),
inference(resolution,[status(thm)],[c1,reflexivity]) ).
cnf(clause65,negated_conjecture,
( ~ member(skc2,X347,skf9(X348))
| ~ member(skc2,X348,skc3)
| with(skc2,skf12(X347,X348),X348) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause65) ).
cnf(c71,plain,
( X344 != X345
| skf16(X344,X344) = skf16(X345,X345) ),
inference(factor,[status(thm)],[c1]) ).
cnf(c0,axiom,
( X326 != X328
| X325 != X327
| skf18(X326,X325) = skf18(X328,X327) ),
theory(equality) ).
cnf(c68,plain,
( X337 != X336
| skf18(X337,X335) = skf18(X336,X335) ),
inference(resolution,[status(thm)],[c0,reflexivity]) ).
cnf(clause64,negated_conjecture,
( ~ member(skc2,X333,skf9(X334))
| ~ member(skc2,X334,skc3)
| agent(skc2,skf12(X333,X332),X333) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause64) ).
cnf(c67,plain,
( X330 != X329
| skf18(X330,X330) = skf18(X329,X329) ),
inference(factor,[status(thm)],[c0]) ).
cnf(c44,axiom,
( X322 != X324
| X321 != X323
| ~ present(X322,X321)
| present(X324,X323) ),
theory(equality) ).
cnf(c43,axiom,
( X318 != X320
| X317 != X319
| ~ young(X318,X317)
| young(X320,X319) ),
theory(equality) ).
cnf(clause63,negated_conjecture,
( ~ member(skc2,X315,skf9(X316))
| ~ member(skc2,X316,skc3)
| sit(skc2,skf12(X313,X314)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause63) ).
cnf(c41,axiom,
( X310 != X312
| X309 != X311
| ~ artifact(X310,X309)
| artifact(X312,X311) ),
theory(equality) ).
cnf(c40,axiom,
( X306 != X308
| X305 != X307
| ~ instrumentality(X306,X305)
| instrumentality(X308,X307) ),
theory(equality) ).
cnf(c39,axiom,
( X302 != X304
| X301 != X303
| ~ furniture(X302,X301)
| furniture(X304,X303) ),
theory(equality) ).
cnf(c38,axiom,
( X298 != X300
| X297 != X299
| ~ table(X298,X297)
| table(X300,X299) ),
theory(equality) ).
cnf(c37,axiom,
( X294 != X296
| X293 != X295
| ~ nonexistent(X294,X293)
| nonexistent(X296,X295) ),
theory(equality) ).
cnf(clause62,negated_conjecture,
( ~ member(skc2,X291,skf9(X292))
| ~ member(skc2,X292,skc3)
| present(skc2,skf12(X289,X290)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause62) ).
cnf(c36,axiom,
( X286 != X288
| X285 != X287
| ~ eventuality(X286,X285)
| eventuality(X288,X287) ),
theory(equality) ).
cnf(c35,axiom,
( X282 != X284
| X281 != X283
| ~ event(X282,X281)
| event(X284,X283) ),
theory(equality) ).
cnf(c34,axiom,
( X278 != X280
| X277 != X279
| ~ sit(X278,X277)
| sit(X280,X279) ),
theory(equality) ).
cnf(c33,axiom,
( X274 != X276
| X273 != X275
| ~ unisex(X274,X273)
| unisex(X276,X275) ),
theory(equality) ).
cnf(c32,axiom,
( X270 != X272
| X269 != X271
| ~ nonliving(X270,X269)
| nonliving(X272,X271) ),
theory(equality) ).
cnf(clause61,negated_conjecture,
( ~ member(skc2,X267,skf9(X268))
| ~ member(skc2,X268,skc3)
| event(skc2,skf12(X265,X266)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause61) ).
cnf(c31,axiom,
( X262 != X264
| X261 != X263
| ~ object(X262,X261)
| object(X264,X263) ),
theory(equality) ).
cnf(c30,axiom,
( X258 != X260
| X257 != X259
| ~ substance_matter(X258,X257)
| substance_matter(X260,X259) ),
theory(equality) ).
cnf(c29,axiom,
( X254 != X256
| X253 != X255
| ~ food(X254,X253)
| food(X256,X255) ),
theory(equality) ).
cnf(c28,axiom,
( X250 != X252
| X249 != X251
| ~ meat(X250,X249)
| meat(X252,X251) ),
theory(equality) ).
cnf(c27,axiom,
( X246 != X248
| X245 != X247
| ~ burger(X246,X245)
| burger(X248,X247) ),
theory(equality) ).
cnf(clause60,negated_conjecture,
( ~ member(skc2,X243,skf9(X244))
| ~ member(skc2,X242,skc3)
| young(skc2,X243) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause60) ).
cnf(c26,axiom,
( X239 != X241
| X238 != X240
| ~ hamburger(X239,X238)
| hamburger(X241,X240) ),
theory(equality) ).
cnf(c25,axiom,
( X235 != X237
| X234 != X236
| ~ three(X235,X234)
| three(X237,X236) ),
theory(equality) ).
cnf(clause54,negated_conjecture,
group(skc2,skc3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause54) ).
cnf(clause15,axiom,
( ~ group(X31,X32)
| set(X31,X32) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause15) ).
cnf(c48,plain,
set(skc2,skc3),
inference(resolution,[status(thm)],[clause15,clause54]) ).
cnf(clause16,axiom,
( ~ set(X33,X34)
| multiple(X33,X34) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause16) ).
cnf(c49,plain,
multiple(skc2,skc3),
inference(resolution,[status(thm)],[clause16,c48]) ).
cnf(c24,axiom,
( X225 != X227
| X224 != X226
| ~ multiple(X225,X224)
| multiple(X227,X226) ),
theory(equality) ).
cnf(c64,plain,
( skc2 != X231
| skc3 != X232
| multiple(X231,X232) ),
inference(resolution,[status(thm)],[c24,c49]) ).
cnf(c65,plain,
( skc2 != X233
| multiple(X233,skc3) ),
inference(resolution,[status(thm)],[c64,reflexivity]) ).
cnf(clause59,negated_conjecture,
( ~ member(skc2,X229,skf9(X230))
| ~ member(skc2,X228,skc3)
| guy(skc2,X229) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause59) ).
cnf(c23,axiom,
( X218 != X220
| X217 != X219
| ~ set(X218,X217)
| set(X220,X219) ),
theory(equality) ).
cnf(c61,plain,
( skc2 != X221
| skc3 != X222
| set(X221,X222) ),
inference(resolution,[status(thm)],[c23,c48]) ).
cnf(c62,plain,
( skc2 != X223
| set(X223,skc3) ),
inference(resolution,[status(thm)],[c61,reflexivity]) ).
cnf(clause52,axiom,
( ~ member(X214,X216,X212)
| ~ member(X214,X215,X212)
| ~ member(X214,X213,X212)
| three(X214,X212)
| member(X214,skf19(X216,X215,X213,X212,X214),X212)
| X216 = X213
| X216 = X215
| X215 = X213 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause52) ).
cnf(c22,axiom,
( X206 != X208
| X205 != X207
| ~ group(X206,X205)
| group(X208,X207) ),
theory(equality) ).
cnf(c56,plain,
( skc2 != X210
| skc3 != X209
| group(X210,X209) ),
inference(resolution,[status(thm)],[c22,clause54]) ).
cnf(c57,plain,
( skc2 != X211
| group(X211,skc3) ),
inference(resolution,[status(thm)],[c56,reflexivity]) ).
cnf(c21,axiom,
( X202 != X204
| X201 != X203
| ~ male(X202,X201)
| male(X204,X203) ),
theory(equality) ).
cnf(clause51,axiom,
( skf19(X196,X200,X194,X199,X195) != X194
| ~ member(X198,X196,X197)
| ~ member(X198,X200,X197)
| ~ member(X198,X194,X197)
| three(X198,X197)
| X196 = X194
| X196 = X200
| X200 = X194 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause51) ).
cnf(c20,axiom,
( X191 != X193
| X190 != X192
| ~ animate(X191,X190)
| animate(X193,X192) ),
theory(equality) ).
cnf(c19,axiom,
( X187 != X189
| X186 != X188
| ~ human(X187,X186)
| human(X189,X188) ),
theory(equality) ).
cnf(c18,axiom,
( X183 != X185
| X182 != X184
| ~ living(X183,X182)
| living(X185,X184) ),
theory(equality) ).
cnf(c17,axiom,
( X179 != X181
| X178 != X180
| ~ impartial(X179,X178)
| impartial(X181,X180) ),
theory(equality) ).
cnf(c16,axiom,
( X175 != X177
| X174 != X176
| ~ existent(X175,X174)
| existent(X177,X176) ),
theory(equality) ).
cnf(clause50,axiom,
( skf19(X168,X173,X166,X172,X167) != X173
| ~ member(X170,X168,X169)
| ~ member(X170,X173,X169)
| ~ member(X170,X171,X169)
| three(X170,X169)
| X168 = X171
| X168 = X173
| X173 = X171 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause50) ).
cnf(c15,axiom,
( X163 != X165
| X162 != X164
| ~ specific(X163,X162)
| specific(X165,X164) ),
theory(equality) ).
cnf(c14,axiom,
( X159 != X161
| X158 != X160
| ~ singleton(X159,X158)
| singleton(X161,X160) ),
theory(equality) ).
cnf(c13,axiom,
( X155 != X157
| X154 != X156
| ~ thing(X155,X154)
| thing(X157,X156) ),
theory(equality) ).
cnf(c12,axiom,
( X151 != X153
| X150 != X152
| ~ entity(X151,X150)
| entity(X153,X152) ),
theory(equality) ).
cnf(c11,axiom,
( X147 != X149
| X146 != X148
| ~ organism(X147,X146)
| organism(X149,X148) ),
theory(equality) ).
cnf(clause49,axiom,
( skf19(X139,X145,X137,X144,X138) != X139
| ~ member(X141,X139,X140)
| ~ member(X141,X142,X140)
| ~ member(X141,X143,X140)
| three(X141,X140)
| X139 = X143
| X139 = X142
| X142 = X143 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause49) ).
cnf(c10,axiom,
( X134 != X136
| X133 != X135
| ~ human_person(X134,X133)
| human_person(X136,X135) ),
theory(equality) ).
cnf(c9,axiom,
( X130 != X132
| X129 != X131
| ~ man(X130,X129)
| man(X132,X131) ),
theory(equality) ).
cnf(c8,axiom,
( X126 != X128
| X125 != X127
| ~ guy(X126,X125)
| guy(X128,X127) ),
theory(equality) ).
cnf(clause58,negated_conjecture,
( ~ member(skc2,X123,skc3)
| table(skc2,skf11(X124)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause58) ).
cnf(clause57,negated_conjecture,
( ~ member(skc2,X121,skc3)
| group(skc2,skf9(X122)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause57) ).
cnf(clause48,axiom,
( ~ member(X119,X120,X118)
| ~ three(X119,X118)
| X120 = skf14(X118,X119)
| X120 = skf16(X118,X119)
| X120 = skf18(X118,X119) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause48) ).
cnf(clause56,negated_conjecture,
( ~ member(skc2,X116,skc3)
| three(skc2,skf9(X117)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause56) ).
cnf(clause47,axiom,
( skf16(X114,X115) != skf14(X114,X115)
| ~ three(X115,X114) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause47) ).
cnf(c5,axiom,
( X111 != X112
| skf11(X111) = skf11(X112) ),
theory(equality) ).
cnf(clause46,axiom,
( skf18(X108,X109) != skf16(X108,X109)
| ~ three(X109,X108) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause46) ).
cnf(c4,axiom,
( X106 != X107
| skf9(X106) = skf9(X107) ),
theory(equality) ).
cnf(transitivity,axiom,
( X100 != X102
| X102 != X101
| X100 = X101 ),
theory(equality) ).
cnf(clause55,negated_conjecture,
( ~ member(skc2,X99,skc3)
| hamburger(skc2,X99) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause55) ).
cnf(clause45,axiom,
( skf18(X97,X98) != skf14(X97,X98)
| ~ three(X98,X97) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause45) ).
cnf(clause44,axiom,
( ~ three(X95,X96)
| member(X95,skf14(X96,X95),X96) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause44) ).
cnf(clause43,axiom,
( ~ three(X93,X94)
| member(X93,skf16(X94,X93),X94) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause43) ).
cnf(c42,axiom,
( X90 != X91
| ~ actual_world(X90)
| actual_world(X91) ),
theory(equality) ).
cnf(clause42,axiom,
( ~ three(X87,X88)
| member(X87,skf18(X88,X87),X88) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause42) ).
cnf(symmetry,axiom,
( X85 != X86
| X86 = X85 ),
theory(equality) ).
cnf(clause41,axiom,
( ~ nonliving(X83,X84)
| ~ animate(X83,X84) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause41) ).
cnf(clause40,axiom,
( ~ nonexistent(X81,X82)
| ~ existent(X81,X82) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause40) ).
cnf(clause39,axiom,
( ~ living(X79,X80)
| ~ nonliving(X79,X80) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause39) ).
cnf(clause38,axiom,
( ~ multiple(X77,X78)
| ~ singleton(X77,X78) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause38) ).
cnf(clause37,axiom,
( ~ male(X75,X76)
| ~ unisex(X75,X76) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause37) ).
cnf(clause36,axiom,
( ~ artifact(X73,X74)
| object(X73,X74) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause36) ).
cnf(clause35,axiom,
( ~ instrumentality(X71,X72)
| artifact(X71,X72) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause35) ).
cnf(clause34,axiom,
( ~ furniture(X69,X70)
| instrumentality(X69,X70) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause34) ).
cnf(clause33,axiom,
( ~ table(X67,X68)
| furniture(X67,X68) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause33) ).
cnf(clause32,axiom,
( ~ eventuality(X65,X66)
| unisex(X65,X66) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause32) ).
cnf(clause31,axiom,
( ~ eventuality(X63,X64)
| nonexistent(X63,X64) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause31) ).
cnf(clause30,axiom,
( ~ eventuality(X61,X62)
| specific(X61,X62) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause30) ).
cnf(clause29,axiom,
( ~ eventuality(X59,X60)
| thing(X59,X60) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause29) ).
cnf(clause28,axiom,
( ~ event(X57,X58)
| eventuality(X57,X58) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause28) ).
cnf(clause27,axiom,
( ~ sit(X55,X56)
| event(X55,X56) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause27) ).
cnf(clause26,axiom,
( ~ object(X53,X54)
| unisex(X53,X54) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause26) ).
cnf(clause25,axiom,
( ~ object(X51,X52)
| impartial(X51,X52) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause25) ).
cnf(clause24,axiom,
( ~ object(X49,X50)
| nonliving(X49,X50) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause24) ).
cnf(clause23,axiom,
( ~ object(X47,X48)
| entity(X47,X48) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause23) ).
cnf(clause22,axiom,
( ~ substance_matter(X45,X46)
| object(X45,X46) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause22) ).
cnf(clause21,axiom,
( ~ food(X43,X44)
| substance_matter(X43,X44) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause21) ).
cnf(clause20,axiom,
( ~ meat(X41,X42)
| food(X41,X42) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause20) ).
cnf(clause19,axiom,
( ~ burger(X39,X40)
| meat(X39,X40) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause19) ).
cnf(clause18,axiom,
( ~ hamburger(X37,X38)
| burger(X37,X38) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause18) ).
cnf(clause17,axiom,
( ~ three(X35,X36)
| group(X35,X36) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause17) ).
cnf(clause14,axiom,
( ~ man(X29,X30)
| male(X29,X30) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause14) ).
cnf(clause13,axiom,
( ~ human_person(X27,X28)
| animate(X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause13) ).
cnf(clause12,axiom,
( ~ human_person(X25,X26)
| human(X25,X26) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause12) ).
cnf(clause11,axiom,
( ~ organism(X23,X24)
| living(X23,X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
cnf(clause10,axiom,
( ~ organism(X21,X22)
| impartial(X21,X22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause10) ).
cnf(clause9,axiom,
( ~ entity(X19,X20)
| existent(X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause9) ).
cnf(clause8,axiom,
( ~ entity(X17,X18)
| specific(X17,X18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
cnf(clause7,axiom,
( ~ thing(X15,X16)
| singleton(X15,X16) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause7) ).
cnf(clause6,axiom,
( ~ entity(X13,X14)
| thing(X13,X14) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause6) ).
cnf(clause5,axiom,
( ~ organism(X11,X12)
| entity(X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause5) ).
cnf(clause4,axiom,
( ~ human_person(X9,X10)
| organism(X9,X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause4) ).
cnf(clause3,axiom,
( ~ man(X7,X8)
| human_person(X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
cnf(clause2,axiom,
( ~ guy(X5,X6)
| man(X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
cnf(clause1,axiom,
~ member(X3,X4,X4),
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.03/0.10 % Problem : NLP040-1 : TPTP v8.1.2. Released v2.4.0.
% 0.03/0.11 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.11/0.30 % Computer : n032.cluster.edu
% 0.11/0.30 % Model : x86_64 x86_64
% 0.11/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.30 % Memory : 8042.1875MB
% 0.11/0.30 % OS : Linux 3.10.0-693.el7.x86_64
% 0.11/0.30 % CPULimit : 300
% 0.11/0.30 % WCLimit : 300
% 0.11/0.30 % DateTime : Wed May 8 13:31:52 EDT 2024
% 0.11/0.30 % CPUTime :
% 1.60/1.80 % Version: 1.5
% 1.60/1.80 % SZS status Satisfiable
% 1.60/1.80 % SZS output start Saturation
% See solution above
% 1.60/1.81
% 1.60/1.81 % Initial clauses : 117
% 1.60/1.81 % Processed clauses : 244
% 1.60/1.81 % Factors computed : 97
% 1.60/1.81 % Resolvents computed: 140
% 1.60/1.81 % Tautologies deleted: 3
% 1.60/1.81 % Forward subsumed : 107
% 1.60/1.81 % Backward subsumed : 47
% 1.60/1.81 % -------- CPU Time ---------
% 1.60/1.81 % User time : 1.481 s
% 1.60/1.81 % System time : 0.007 s
% 1.60/1.81 % Total time : 1.488 s
%------------------------------------------------------------------------------