%------------------------------------------------------------------------------
% File : PyRes---1.5
% Problem : NLP038-1 : TPTP v8.1.2. Released v2.4.0.
% Transfm : none
% Format : tptp:raw
% Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% Computer : n023.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.62s 1.81s
% Output : Saturation 1.65s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
cnf(reflexivity,axiom,
X2 = X2,
theory(equality) ).
cnf(c3,axiom,
( X257 != X260
| X265 != X262
| X258 != X263
| X256 != X259
| X264 != X261
| skf16(X257,X265,X258,X256,X264) = skf16(X260,X262,X263,X259,X261) ),
theory(equality) ).
cnf(c192,plain,
( X619 != X612
| X614 != X617
| X615 != X616
| X618 != X613
| skf16(X619,X614,X615,X618,X620) = skf16(X612,X617,X616,X613,X620) ),
inference(resolution,[status(thm)],[c3,reflexivity]) ).
cnf(c351,plain,
( X1107 != X1104
| X1102 != X1103
| X1106 != X1108
| skf16(X1107,X1102,X1106,X1109,X1105) = skf16(X1104,X1103,X1108,X1109,X1105) ),
inference(resolution,[status(thm)],[c192,reflexivity]) ).
cnf(c503,plain,
( X1447 != X1446
| X1449 != X1450
| skf16(X1447,X1449,X1451,X1448,X1445) = skf16(X1446,X1450,X1451,X1448,X1445) ),
inference(resolution,[status(thm)],[c351,reflexivity]) ).
cnf(c562,plain,
( X1464 != X1462
| skf16(X1464,X1466,X1461,X1463,X1465) = skf16(X1462,X1466,X1461,X1463,X1465) ),
inference(resolution,[status(thm)],[c503,reflexivity]) ).
cnf(c561,plain,
( X1456 != X1454
| skf16(X1456,X1456,X1452,X1453,X1455) = skf16(X1454,X1454,X1452,X1453,X1455) ),
inference(factor,[status(thm)],[c503]) ).
cnf(c501,plain,
( X1395 != X1396
| X1393 != X1394
| skf16(X1395,X1393,X1395,X1397,X1392) = skf16(X1396,X1394,X1396,X1397,X1392) ),
inference(factor,[status(thm)],[c351]) ).
cnf(c554,plain,
( X1425 != X1424
| skf16(X1425,X1427,X1425,X1423,X1426) = skf16(X1424,X1427,X1424,X1423,X1426) ),
inference(resolution,[status(thm)],[c501,reflexivity]) ).
cnf(c502,plain,
( X1419 != X1418
| X1420 != X1421
| skf16(X1419,X1420,X1420,X1422,X1417) = skf16(X1418,X1421,X1421,X1422,X1417) ),
inference(factor,[status(thm)],[c351]) ).
cnf(c553,plain,
( X1412 != X1413
| skf16(X1412,X1412,X1412,X1411,X1410) = skf16(X1413,X1413,X1413,X1411,X1410) ),
inference(factor,[status(thm)],[c501]) ).
cnf(c349,plain,
( X1052 != X1048
| X1049 != X1047
| X1051 != X1053
| skf16(X1052,X1049,X1051,X1049,X1050) = skf16(X1048,X1047,X1053,X1047,X1050) ),
inference(factor,[status(thm)],[c192]) ).
cnf(c490,plain,
( X1357 != X1353
| X1354 != X1356
| skf16(X1357,X1354,X1358,X1354,X1355) = skf16(X1353,X1356,X1358,X1356,X1355) ),
inference(resolution,[status(thm)],[c349,reflexivity]) ).
cnf(c489,plain,
( X1342 != X1338
| X1339 != X1341
| skf16(X1342,X1339,X1339,X1339,X1340) = skf16(X1338,X1341,X1341,X1341,X1340) ),
inference(factor,[status(thm)],[c349]) ).
cnf(c348,plain,
( X1025 != X1022
| X1023 != X1024
| X1027 != X1028
| skf16(X1025,X1023,X1027,X1025,X1026) = skf16(X1022,X1024,X1028,X1022,X1026) ),
inference(factor,[status(thm)],[c192]) ).
cnf(c484,plain,
( X1292 != X1295
| X1293 != X1294
| skf16(X1292,X1293,X1296,X1292,X1291) = skf16(X1295,X1294,X1296,X1295,X1291) ),
inference(resolution,[status(thm)],[c348,reflexivity]) ).
cnf(c537,plain,
( X1320 != X1322
| skf16(X1320,X1323,X1319,X1320,X1321) = skf16(X1322,X1323,X1319,X1322,X1321) ),
inference(resolution,[status(thm)],[c484,reflexivity]) ).
cnf(c488,plain,
( X1314 != X1317
| X1315 != X1318
| skf16(X1314,X1315,X1314,X1315,X1316) = skf16(X1317,X1318,X1317,X1318,X1316) ),
inference(factor,[status(thm)],[c349]) ).
cnf(c536,plain,
( X1308 != X1310
| skf16(X1308,X1308,X1307,X1308,X1309) = skf16(X1310,X1310,X1307,X1310,X1309) ),
inference(factor,[status(thm)],[c484]) ).
cnf(c483,plain,
( X1287 != X1290
| X1289 != X1288
| skf16(X1287,X1289,X1289,X1287,X1286) = skf16(X1290,X1288,X1288,X1290,X1286) ),
inference(factor,[status(thm)],[c348]) ).
cnf(c482,plain,
( X1272 != X1271
| X1270 != X1273
| skf16(X1272,X1270,X1272,X1272,X1269) = skf16(X1271,X1273,X1271,X1271,X1269) ),
inference(factor,[status(thm)],[c348]) ).
cnf(c531,plain,
( X1282 != X1281
| skf16(X1282,X1280,X1282,X1282,X1279) = skf16(X1281,X1280,X1281,X1281,X1279) ),
inference(resolution,[status(thm)],[c482,reflexivity]) ).
cnf(c530,plain,
( X1276 != X1275
| skf16(X1276,X1276,X1276,X1276,X1274) = skf16(X1275,X1275,X1275,X1275,X1274) ),
inference(factor,[status(thm)],[c482]) ).
cnf(c189,plain,
( X575 != X573
| X577 != X580
| X576 != X578
| X579 != X574
| skf16(X575,X577,X576,X579,X577) = skf16(X573,X580,X578,X574,X580) ),
inference(factor,[status(thm)],[c3]) ).
cnf(c329,plain,
( X812 != X814
| X815 != X816
| X817 != X818
| skf16(X812,X815,X817,X813,X815) = skf16(X814,X816,X818,X813,X816) ),
inference(resolution,[status(thm)],[c189,reflexivity]) ).
cnf(c433,plain,
( X1085 != X1086
| X1083 != X1087
| skf16(X1085,X1083,X1088,X1084,X1083) = skf16(X1086,X1087,X1088,X1084,X1087) ),
inference(resolution,[status(thm)],[c329,reflexivity]) ).
cnf(c350,plain,
( X1079 != X1076
| X1074 != X1075
| X1077 != X1073
| skf16(X1079,X1074,X1077,X1077,X1078) = skf16(X1076,X1075,X1073,X1073,X1078) ),
inference(factor,[status(thm)],[c192]) ).
cnf(c432,plain,
( X1062 != X1064
| X1063 != X1065
| skf16(X1062,X1063,X1063,X1061,X1063) = skf16(X1064,X1065,X1065,X1061,X1065) ),
inference(factor,[status(thm)],[c329]) ).
cnf(c431,plain,
( X1041 != X1043
| X1039 != X1042
| skf16(X1041,X1039,X1041,X1040,X1039) = skf16(X1043,X1042,X1043,X1040,X1042) ),
inference(factor,[status(thm)],[c329]) ).
cnf(c327,plain,
( X765 != X767
| X766 != X768
| X769 != X770
| skf16(X765,X766,X769,X766,X766) = skf16(X767,X768,X770,X768,X768) ),
inference(factor,[status(thm)],[c189]) ).
cnf(c421,plain,
( X990 != X988
| X989 != X987
| skf16(X990,X989,X991,X989,X989) = skf16(X988,X987,X991,X987,X987) ),
inference(resolution,[status(thm)],[c327,reflexivity]) ).
cnf(c420,plain,
( X973 != X972
| X971 != X970
| skf16(X973,X971,X971,X971,X971) = skf16(X972,X970,X970,X970,X970) ),
inference(factor,[status(thm)],[c327]) ).
cnf(c419,plain,
( X961 != X960
| X962 != X959
| skf16(X961,X962,X961,X962,X962) = skf16(X960,X959,X960,X959,X959) ),
inference(factor,[status(thm)],[c327]) ).
cnf(c326,plain,
( X744 != X745
| X746 != X747
| X748 != X749
| skf16(X744,X746,X748,X744,X746) = skf16(X745,X747,X749,X745,X747) ),
inference(factor,[status(thm)],[c189]) ).
cnf(c413,plain,
( X939 != X941
| X938 != X940
| skf16(X939,X938,X942,X939,X938) = skf16(X941,X940,X942,X941,X940) ),
inference(resolution,[status(thm)],[c326,reflexivity]) ).
cnf(c412,plain,
( X924 != X923
| X921 != X922
| skf16(X924,X921,X921,X924,X921) = skf16(X923,X922,X922,X923,X922) ),
inference(factor,[status(thm)],[c326]) ).
cnf(c190,plain,
( X592 != X585
| X587 != X589
| X588 != X590
| X591 != X586
| skf16(X592,X587,X588,X591,X588) = skf16(X585,X589,X590,X586,X590) ),
inference(factor,[status(thm)],[c3]) ).
cnf(c336,plain,
( X911 != X913
| X915 != X909
| X914 != X912
| skf16(X911,X915,X914,X910,X914) = skf16(X913,X909,X912,X910,X912) ),
inference(resolution,[status(thm)],[c190,reflexivity]) ).
cnf(c411,plain,
( X904 != X905
| X903 != X906
| skf16(X904,X903,X904,X904,X903) = skf16(X905,X906,X905,X905,X906) ),
inference(factor,[status(thm)],[c326]) ).
cnf(c188,plain,
( X563 != X567
| X561 != X565
| X562 != X564
| X566 != X560
| skf16(X563,X561,X562,X566,X563) = skf16(X567,X565,X564,X560,X567) ),
inference(factor,[status(thm)],[c3]) ).
cnf(c322,plain,
( X722 != X725
| X720 != X721
| X723 != X724
| skf16(X722,X720,X723,X726,X722) = skf16(X725,X721,X724,X726,X725) ),
inference(resolution,[status(thm)],[c188,reflexivity]) ).
cnf(c406,plain,
( X877 != X878
| X875 != X879
| skf16(X877,X875,X880,X876,X877) = skf16(X878,X879,X880,X876,X878) ),
inference(resolution,[status(thm)],[c322,reflexivity]) ).
cnf(c450,plain,
( X897 != X895
| skf16(X897,X898,X894,X896,X897) = skf16(X895,X898,X894,X896,X895) ),
inference(resolution,[status(thm)],[c406,reflexivity]) ).
cnf(c335,plain,
( X886 != X889
| X890 != X885
| X887 != X888
| skf16(X886,X890,X887,X887,X887) = skf16(X889,X885,X888,X888,X888) ),
inference(factor,[status(thm)],[c190]) ).
cnf(c449,plain,
( X881 != X884
| skf16(X881,X881,X882,X883,X881) = skf16(X884,X884,X882,X883,X884) ),
inference(factor,[status(thm)],[c406]) ).
cnf(c334,plain,
( X859 != X862
| X860 != X861
| X864 != X863
| skf16(X859,X860,X864,X860,X864) = skf16(X862,X861,X863,X861,X863) ),
inference(factor,[status(thm)],[c190]) ).
cnf(c405,plain,
( X857 != X858
| X856 != X854
| skf16(X857,X856,X856,X855,X857) = skf16(X858,X854,X854,X855,X858) ),
inference(factor,[status(thm)],[c322]) ).
cnf(c404,plain,
( X834 != X832
| X831 != X835
| skf16(X834,X831,X834,X833,X834) = skf16(X832,X835,X832,X833,X832) ),
inference(factor,[status(thm)],[c322]) ).
cnf(c437,plain,
( X848 != X849
| skf16(X848,X850,X848,X847,X848) = skf16(X849,X850,X849,X847,X849) ),
inference(resolution,[status(thm)],[c404,reflexivity]) ).
cnf(c436,plain,
( X843 != X844
| skf16(X843,X843,X843,X842,X843) = skf16(X844,X844,X844,X842,X844) ),
inference(factor,[status(thm)],[c404]) ).
cnf(c333,plain,
( X837 != X838
| X841 != X836
| X840 != X839
| skf16(X837,X841,X840,X837,X840) = skf16(X838,X836,X839,X838,X839) ),
inference(factor,[status(thm)],[c190]) ).
cnf(c328,plain,
( X786 != X788
| X790 != X791
| X787 != X789
| skf16(X786,X790,X787,X787,X790) = skf16(X788,X791,X789,X789,X791) ),
inference(factor,[status(thm)],[c189]) ).
cnf(c320,plain,
( X686 != X690
| X685 != X687
| X688 != X689
| skf16(X686,X685,X688,X685,X686) = skf16(X690,X687,X689,X687,X690) ),
inference(factor,[status(thm)],[c188]) ).
cnf(c393,plain,
( X781 != X778
| X779 != X780
| skf16(X781,X779,X782,X779,X781) = skf16(X778,X780,X782,X780,X778) ),
inference(resolution,[status(thm)],[c320,reflexivity]) ).
cnf(c392,plain,
( X762 != X763
| X764 != X761
| skf16(X762,X764,X764,X764,X762) = skf16(X763,X761,X761,X761,X763) ),
inference(factor,[status(thm)],[c320]) ).
cnf(c391,plain,
( X753 != X752
| X750 != X751
| skf16(X753,X750,X753,X750,X753) = skf16(X752,X751,X752,X751,X752) ),
inference(factor,[status(thm)],[c320]) ).
cnf(c319,plain,
( X675 != X676
| X673 != X674
| X677 != X678
| skf16(X675,X673,X677,X675,X675) = skf16(X676,X674,X678,X676,X676) ),
inference(factor,[status(thm)],[c188]) ).
cnf(c386,plain,
( X730 != X727
| X728 != X729
| skf16(X730,X728,X731,X730,X730) = skf16(X727,X729,X731,X727,X727) ),
inference(resolution,[status(thm)],[c319,reflexivity]) ).
cnf(c408,plain,
( X740 != X739
| skf16(X740,X738,X737,X740,X740) = skf16(X739,X738,X737,X739,X739) ),
inference(resolution,[status(thm)],[c386,reflexivity]) ).
cnf(c407,plain,
( X733 != X734
| skf16(X733,X733,X732,X733,X733) = skf16(X734,X734,X732,X734,X734) ),
inference(factor,[status(thm)],[c386]) ).
cnf(c385,plain,
( X712 != X711
| X710 != X709
| skf16(X712,X710,X710,X712,X712) = skf16(X711,X709,X709,X711,X711) ),
inference(factor,[status(thm)],[c319]) ).
cnf(c321,plain,
( X704 != X706
| X701 != X702
| X703 != X705
| skf16(X704,X701,X703,X703,X704) = skf16(X706,X702,X705,X705,X706) ),
inference(factor,[status(thm)],[c188]) ).
cnf(c384,plain,
( X692 != X691
| X693 != X694
| skf16(X692,X693,X692,X692,X692) = skf16(X691,X694,X691,X691,X691) ),
inference(factor,[status(thm)],[c319]) ).
cnf(c395,plain,
( X699 != X700
| skf16(X699,X698,X699,X699,X699) = skf16(X700,X698,X700,X700,X700) ),
inference(resolution,[status(thm)],[c384,reflexivity]) ).
cnf(c394,plain,
( X696 != X695
| skf16(X696,X696,X696,X696,X696) = skf16(X695,X695,X695,X695,X695) ),
inference(factor,[status(thm)],[c384]) ).
cnf(clause56,negated_conjecture,
three(skc3,skc4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause56) ).
cnf(clause44,axiom,
( ~ three(X95,X96)
| member(X95,skf11(X96,X95),X96) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause44) ).
cnf(c70,plain,
member(skc3,skf11(skc4,skc3),skc4),
inference(resolution,[status(thm)],[clause44,clause56]) ).
cnf(c6,axiom,
( X287 != X289
| X292 != X290
| X288 != X291
| ~ member(X287,X292,X288)
| member(X289,X290,X291) ),
theory(equality) ).
cnf(c210,plain,
( skc3 != X642
| skf11(skc4,skc3) != X643
| skc4 != X644
| member(X642,X643,X644) ),
inference(resolution,[status(thm)],[c6,c70]) ).
cnf(c364,plain,
( skc3 != X683
| skc4 != X682
| member(X683,skf11(skc4,skc3),X682) ),
inference(resolution,[status(thm)],[c210,reflexivity]) ).
cnf(c389,plain,
( skc3 != X684
| member(X684,skf11(skc4,skc3),skc4) ),
inference(resolution,[status(thm)],[c364,reflexivity]) ).
cnf(clause42,axiom,
( ~ three(X85,X86)
| member(X85,skf15(X86,X85),X86) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause42) ).
cnf(c66,plain,
member(skc3,skf15(skc4,skc3),skc4),
inference(resolution,[status(thm)],[clause42,clause56]) ).
cnf(c209,plain,
( skc3 != X634
| skf15(skc4,skc3) != X635
| skc4 != X636
| member(X634,X635,X636) ),
inference(resolution,[status(thm)],[c6,c66]) ).
cnf(c360,plain,
( skc3 != X679
| skc4 != X680
| member(X679,skf15(skc4,skc3),X680) ),
inference(resolution,[status(thm)],[c209,reflexivity]) ).
cnf(c387,plain,
( skc3 != X681
| member(X681,skf15(skc4,skc3),skc4) ),
inference(resolution,[status(thm)],[c360,reflexivity]) ).
cnf(clause43,axiom,
( ~ three(X93,X94)
| member(X93,skf13(X94,X93),X94) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause43) ).
cnf(c69,plain,
member(skc3,skf13(skc4,skc3),skc4),
inference(resolution,[status(thm)],[clause43,clause56]) ).
cnf(c208,plain,
( skc3 != X625
| skf13(skc4,skc3) != X626
| skc4 != X627
| member(X625,X626,X627) ),
inference(resolution,[status(thm)],[c6,c69]) ).
cnf(c355,plain,
( skc3 != X670
| skc4 != X671
| member(X670,skf13(skc4,skc3),X671) ),
inference(resolution,[status(thm)],[c208,reflexivity]) ).
cnf(c382,plain,
( skc3 != X672
| member(X672,skf13(skc4,skc3),skc4) ),
inference(resolution,[status(thm)],[c355,reflexivity]) ).
cnf(clause57,negated_conjecture,
( ~ member(skc3,X97,skc4)
| young(skc3,X97) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause57) ).
cnf(c75,plain,
young(skc3,skf15(skc4,skc3)),
inference(resolution,[status(thm)],[c66,clause57]) ).
cnf(c42,axiom,
( X444 != X443
| X445 != X442
| ~ young(X444,X445)
| young(X443,X442) ),
theory(equality) ).
cnf(c266,plain,
( skc3 != X667
| skf15(skc4,skc3) != X668
| young(X667,X668) ),
inference(resolution,[status(thm)],[c42,c75]) ).
cnf(c380,plain,
( skc3 != X669
| young(X669,skf15(skc4,skc3)) ),
inference(resolution,[status(thm)],[c266,reflexivity]) ).
cnf(c120,plain,
young(skc3,skf11(skc4,skc3)),
inference(resolution,[status(thm)],[c70,clause57]) ).
cnf(c265,plain,
( skc3 != X664
| skf11(skc4,skc3) != X665
| young(X664,X665) ),
inference(resolution,[status(thm)],[c42,c120]) ).
cnf(c378,plain,
( skc3 != X666
| young(X666,skf11(skc4,skc3)) ),
inference(resolution,[status(thm)],[c265,reflexivity]) ).
cnf(c95,plain,
young(skc3,skf13(skc4,skc3)),
inference(resolution,[status(thm)],[c69,clause57]) ).
cnf(c264,plain,
( skc3 != X661
| skf13(skc4,skc3) != X662
| young(X661,X662) ),
inference(resolution,[status(thm)],[c42,c95]) ).
cnf(c376,plain,
( skc3 != X663
| young(X663,skf13(skc4,skc3)) ),
inference(resolution,[status(thm)],[c264,reflexivity]) ).
cnf(clause14,axiom,
( ~ man(X29,X30)
| male(X29,X30) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause14) ).
cnf(clause2,axiom,
( ~ guy(X5,X6)
| man(X5,X6) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause2) ).
cnf(clause58,negated_conjecture,
( ~ member(skc3,X98,skc4)
| guy(skc3,X98) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause58) ).
cnf(c94,plain,
guy(skc3,skf13(skc4,skc3)),
inference(resolution,[status(thm)],[c69,clause58]) ).
cnf(c96,plain,
man(skc3,skf13(skc4,skc3)),
inference(resolution,[status(thm)],[c94,clause2]) ).
cnf(c97,plain,
male(skc3,skf13(skc4,skc3)),
inference(resolution,[status(thm)],[c96,clause14]) ).
cnf(c20,axiom,
( X312 != X311
| X313 != X310
| ~ male(X312,X313)
| male(X311,X310) ),
theory(equality) ).
cnf(c223,plain,
( skc3 != X659
| skf13(skc4,skc3) != X658
| male(X659,X658) ),
inference(resolution,[status(thm)],[c20,c97]) ).
cnf(c374,plain,
( skc3 != X660
| male(X660,skf13(skc4,skc3)) ),
inference(resolution,[status(thm)],[c223,reflexivity]) ).
cnf(c123,plain,
guy(skc3,skf11(skc4,skc3)),
inference(resolution,[status(thm)],[c70,clause58]) ).
cnf(c124,plain,
man(skc3,skf11(skc4,skc3)),
inference(resolution,[status(thm)],[c123,clause2]) ).
cnf(c125,plain,
male(skc3,skf11(skc4,skc3)),
inference(resolution,[status(thm)],[c124,clause14]) ).
cnf(c222,plain,
( skc3 != X656
| skf11(skc4,skc3) != X655
| male(X656,X655) ),
inference(resolution,[status(thm)],[c20,c125]) ).
cnf(c372,plain,
( skc3 != X657
| male(X657,skf11(skc4,skc3)) ),
inference(resolution,[status(thm)],[c222,reflexivity]) ).
cnf(c74,plain,
guy(skc3,skf15(skc4,skc3)),
inference(resolution,[status(thm)],[c66,clause58]) ).
cnf(c76,plain,
man(skc3,skf15(skc4,skc3)),
inference(resolution,[status(thm)],[c74,clause2]) ).
cnf(c77,plain,
male(skc3,skf15(skc4,skc3)),
inference(resolution,[status(thm)],[c76,clause14]) ).
cnf(c221,plain,
( skc3 != X653
| skf15(skc4,skc3) != X652
| male(X653,X652) ),
inference(resolution,[status(thm)],[c20,c77]) ).
cnf(c370,plain,
( skc3 != X654
| male(X654,skf15(skc4,skc3)) ),
inference(resolution,[status(thm)],[c221,reflexivity]) ).
cnf(clause13,axiom,
( ~ human_person(X27,X28)
| animate(X27,X28) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause13) ).
cnf(clause3,axiom,
( ~ man(X7,X8)
| human_person(X7,X8) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause3) ).
cnf(c78,plain,
human_person(skc3,skf15(skc4,skc3)),
inference(resolution,[status(thm)],[c76,clause3]) ).
cnf(c80,plain,
animate(skc3,skf15(skc4,skc3)),
inference(resolution,[status(thm)],[c78,clause13]) ).
cnf(c19,axiom,
( X308 != X307
| X309 != X306
| ~ animate(X308,X309)
| animate(X307,X306) ),
theory(equality) ).
cnf(c220,plain,
( skc3 != X650
| skf15(skc4,skc3) != X649
| animate(X650,X649) ),
inference(resolution,[status(thm)],[c19,c80]) ).
cnf(c368,plain,
( skc3 != X651
| animate(X651,skf15(skc4,skc3)) ),
inference(resolution,[status(thm)],[c220,reflexivity]) ).
cnf(c98,plain,
human_person(skc3,skf13(skc4,skc3)),
inference(resolution,[status(thm)],[c96,clause3]) ).
cnf(c100,plain,
animate(skc3,skf13(skc4,skc3)),
inference(resolution,[status(thm)],[c98,clause13]) ).
cnf(c219,plain,
( skc3 != X647
| skf13(skc4,skc3) != X646
| animate(X647,X646) ),
inference(resolution,[status(thm)],[c19,c100]) ).
cnf(c366,plain,
( skc3 != X648
| animate(X648,skf13(skc4,skc3)) ),
inference(resolution,[status(thm)],[c219,reflexivity]) ).
cnf(c126,plain,
human_person(skc3,skf11(skc4,skc3)),
inference(resolution,[status(thm)],[c124,clause3]) ).
cnf(c128,plain,
animate(skc3,skf11(skc4,skc3)),
inference(resolution,[status(thm)],[c126,clause13]) ).
cnf(c218,plain,
( skc3 != X641
| skf11(skc4,skc3) != X640
| animate(X641,X640) ),
inference(resolution,[status(thm)],[c19,c128]) ).
cnf(c363,plain,
( skc3 != X645
| animate(X645,skf11(skc4,skc3)) ),
inference(resolution,[status(thm)],[c218,reflexivity]) ).
cnf(clause12,axiom,
( ~ human_person(X25,X26)
| human(X25,X26) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause12) ).
cnf(c129,plain,
human(skc3,skf11(skc4,skc3)),
inference(resolution,[status(thm)],[c126,clause12]) ).
cnf(c18,axiom,
( X304 != X303
| X305 != X302
| ~ human(X304,X305)
| human(X303,X302) ),
theory(equality) ).
cnf(c217,plain,
( skc3 != X637
| skf11(skc4,skc3) != X638
| human(X637,X638) ),
inference(resolution,[status(thm)],[c18,c129]) ).
cnf(c361,plain,
( skc3 != X639
| human(X639,skf11(skc4,skc3)) ),
inference(resolution,[status(thm)],[c217,reflexivity]) ).
cnf(c101,plain,
human(skc3,skf13(skc4,skc3)),
inference(resolution,[status(thm)],[c98,clause12]) ).
cnf(c216,plain,
( skc3 != X631
| skf13(skc4,skc3) != X632
| human(X631,X632) ),
inference(resolution,[status(thm)],[c18,c101]) ).
cnf(c358,plain,
( skc3 != X633
| human(X633,skf13(skc4,skc3)) ),
inference(resolution,[status(thm)],[c216,reflexivity]) ).
cnf(c81,plain,
human(skc3,skf15(skc4,skc3)),
inference(resolution,[status(thm)],[c78,clause12]) ).
cnf(c215,plain,
( skc3 != X628
| skf15(skc4,skc3) != X629
| human(X628,X629) ),
inference(resolution,[status(thm)],[c18,c81]) ).
cnf(c356,plain,
( skc3 != X630
| human(X630,skf15(skc4,skc3)) ),
inference(resolution,[status(thm)],[c215,reflexivity]) ).
cnf(clause11,axiom,
( ~ organism(X23,X24)
| living(X23,X24) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause11) ).
cnf(clause4,axiom,
( ~ human_person(X9,X10)
| organism(X9,X10) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause4) ).
cnf(c99,plain,
organism(skc3,skf13(skc4,skc3)),
inference(resolution,[status(thm)],[c98,clause4]) ).
cnf(c103,plain,
living(skc3,skf13(skc4,skc3)),
inference(resolution,[status(thm)],[c99,clause11]) ).
cnf(c17,axiom,
( X300 != X299
| X301 != X298
| ~ living(X300,X301)
| living(X299,X298) ),
theory(equality) ).
cnf(c214,plain,
( skc3 != X623
| skf13(skc4,skc3) != X622
| living(X623,X622) ),
inference(resolution,[status(thm)],[c17,c103]) ).
cnf(c353,plain,
( skc3 != X624
| living(X624,skf13(skc4,skc3)) ),
inference(resolution,[status(thm)],[c214,reflexivity]) ).
cnf(c79,plain,
organism(skc3,skf15(skc4,skc3)),
inference(resolution,[status(thm)],[c78,clause4]) ).
cnf(c83,plain,
living(skc3,skf15(skc4,skc3)),
inference(resolution,[status(thm)],[c79,clause11]) ).
cnf(c213,plain,
( skc3 != X611
| skf15(skc4,skc3) != X610
| living(X611,X610) ),
inference(resolution,[status(thm)],[c17,c83]) ).
cnf(c347,plain,
( skc3 != X621
| living(X621,skf15(skc4,skc3)) ),
inference(resolution,[status(thm)],[c213,reflexivity]) ).
cnf(c127,plain,
organism(skc3,skf11(skc4,skc3)),
inference(resolution,[status(thm)],[c126,clause4]) ).
cnf(c131,plain,
living(skc3,skf11(skc4,skc3)),
inference(resolution,[status(thm)],[c127,clause11]) ).
cnf(c212,plain,
( skc3 != X608
| skf11(skc4,skc3) != X607
| living(X608,X607) ),
inference(resolution,[status(thm)],[c17,c131]) ).
cnf(c345,plain,
( skc3 != X609
| living(X609,skf11(skc4,skc3)) ),
inference(resolution,[status(thm)],[c212,reflexivity]) ).
cnf(c191,plain,
( X606 != X599
| X600 != X604
| X601 != X602
| X603 != X605
| skf16(X606,X600,X601,X603,X603) = skf16(X599,X604,X602,X605,X605) ),
inference(factor,[status(thm)],[c3]) ).
cnf(clause10,axiom,
( ~ organism(X21,X22)
| impartial(X21,X22) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause10) ).
cnf(c82,plain,
impartial(skc3,skf15(skc4,skc3)),
inference(resolution,[status(thm)],[c79,clause10]) ).
cnf(c16,axiom,
( X275 != X274
| X276 != X273
| ~ impartial(X275,X276)
| impartial(X274,X273) ),
theory(equality) ).
cnf(c202,plain,
( skc3 != X597
| skf15(skc4,skc3) != X596
| impartial(X597,X596) ),
inference(resolution,[status(thm)],[c16,c82]) ).
cnf(c339,plain,
( skc3 != X598
| impartial(X598,skf15(skc4,skc3)) ),
inference(resolution,[status(thm)],[c202,reflexivity]) ).
cnf(c102,plain,
impartial(skc3,skf13(skc4,skc3)),
inference(resolution,[status(thm)],[c99,clause10]) ).
cnf(c201,plain,
( skc3 != X594
| skf13(skc4,skc3) != X593
| impartial(X594,X593) ),
inference(resolution,[status(thm)],[c16,c102]) ).
cnf(c337,plain,
( skc3 != X595
| impartial(X595,skf13(skc4,skc3)) ),
inference(resolution,[status(thm)],[c201,reflexivity]) ).
cnf(c130,plain,
impartial(skc3,skf11(skc4,skc3)),
inference(resolution,[status(thm)],[c127,clause10]) ).
cnf(c200,plain,
( skc3 != X583
| skf11(skc4,skc3) != X582
| impartial(X583,X582) ),
inference(resolution,[status(thm)],[c16,c130]) ).
cnf(c331,plain,
( skc3 != X584
| impartial(X584,skf11(skc4,skc3)) ),
inference(resolution,[status(thm)],[c200,reflexivity]) ).
cnf(clause9,axiom,
( ~ entity(X19,X20)
| existent(X19,X20) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause9) ).
cnf(clause5,axiom,
( ~ organism(X11,X12)
| entity(X11,X12) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause5) ).
cnf(c132,plain,
entity(skc3,skf11(skc4,skc3)),
inference(resolution,[status(thm)],[c127,clause5]) ).
cnf(c134,plain,
existent(skc3,skf11(skc4,skc3)),
inference(resolution,[status(thm)],[c132,clause9]) ).
cnf(c15,axiom,
( X268 != X267
| X269 != X266
| ~ existent(X268,X269)
| existent(X267,X266) ),
theory(equality) ).
cnf(c196,plain,
( skc3 != X571
| skf11(skc4,skc3) != X572
| existent(X571,X572) ),
inference(resolution,[status(thm)],[c15,c134]) ).
cnf(c325,plain,
( skc3 != X581
| existent(X581,skf11(skc4,skc3)) ),
inference(resolution,[status(thm)],[c196,reflexivity]) ).
cnf(c104,plain,
entity(skc3,skf13(skc4,skc3)),
inference(resolution,[status(thm)],[c99,clause5]) ).
cnf(c106,plain,
existent(skc3,skf13(skc4,skc3)),
inference(resolution,[status(thm)],[c104,clause9]) ).
cnf(c194,plain,
( skc3 != X568
| skf13(skc4,skc3) != X569
| existent(X568,X569) ),
inference(resolution,[status(thm)],[c15,c106]) ).
cnf(c323,plain,
( skc3 != X570
| existent(X570,skf13(skc4,skc3)) ),
inference(resolution,[status(thm)],[c194,reflexivity]) ).
cnf(c84,plain,
entity(skc3,skf15(skc4,skc3)),
inference(resolution,[status(thm)],[c79,clause5]) ).
cnf(c86,plain,
existent(skc3,skf15(skc4,skc3)),
inference(resolution,[status(thm)],[c84,clause9]) ).
cnf(c193,plain,
( skc3 != X557
| skf15(skc4,skc3) != X558
| existent(X557,X558) ),
inference(resolution,[status(thm)],[c15,c86]) ).
cnf(c317,plain,
( skc3 != X559
| existent(X559,skf15(skc4,skc3)) ),
inference(resolution,[status(thm)],[c193,reflexivity]) ).
cnf(clause8,axiom,
( ~ entity(X17,X18)
| specific(X17,X18) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause8) ).
cnf(c87,plain,
specific(skc3,skf15(skc4,skc3)),
inference(resolution,[status(thm)],[c84,clause8]) ).
cnf(c14,axiom,
( X215 != X214
| X216 != X213
| ~ specific(X215,X216)
| specific(X214,X213) ),
theory(equality) ).
cnf(c173,plain,
( skc3 != X554
| skf15(skc4,skc3) != X555
| specific(X554,X555) ),
inference(resolution,[status(thm)],[c14,c87]) ).
cnf(c315,plain,
( skc3 != X556
| specific(X556,skf15(skc4,skc3)) ),
inference(resolution,[status(thm)],[c173,reflexivity]) ).
cnf(c107,plain,
specific(skc3,skf13(skc4,skc3)),
inference(resolution,[status(thm)],[c104,clause8]) ).
cnf(c171,plain,
( skc3 != X551
| skf13(skc4,skc3) != X552
| specific(X551,X552) ),
inference(resolution,[status(thm)],[c14,c107]) ).
cnf(c313,plain,
( skc3 != X553
| specific(X553,skf13(skc4,skc3)) ),
inference(resolution,[status(thm)],[c171,reflexivity]) ).
cnf(c135,plain,
specific(skc3,skf11(skc4,skc3)),
inference(resolution,[status(thm)],[c132,clause8]) ).
cnf(c170,plain,
( skc3 != X548
| skf11(skc4,skc3) != X549
| specific(X548,X549) ),
inference(resolution,[status(thm)],[c14,c135]) ).
cnf(c311,plain,
( skc3 != X550
| specific(X550,skf11(skc4,skc3)) ),
inference(resolution,[status(thm)],[c170,reflexivity]) ).
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(c108,plain,
thing(skc3,skf13(skc4,skc3)),
inference(resolution,[status(thm)],[c104,clause6]) ).
cnf(c114,plain,
singleton(skc3,skf13(skc4,skc3)),
inference(resolution,[status(thm)],[c108,clause7]) ).
cnf(c13,axiom,
( X208 != X207
| X209 != X206
| ~ singleton(X208,X209)
| singleton(X207,X206) ),
theory(equality) ).
cnf(c167,plain,
( skc3 != X546
| skf13(skc4,skc3) != X545
| singleton(X546,X545) ),
inference(resolution,[status(thm)],[c13,c114]) ).
cnf(c309,plain,
( skc3 != X547
| singleton(X547,skf13(skc4,skc3)) ),
inference(resolution,[status(thm)],[c167,reflexivity]) ).
cnf(c88,plain,
thing(skc3,skf15(skc4,skc3)),
inference(resolution,[status(thm)],[c84,clause6]) ).
cnf(c91,plain,
singleton(skc3,skf15(skc4,skc3)),
inference(resolution,[status(thm)],[c88,clause7]) ).
cnf(c166,plain,
( skc3 != X543
| skf15(skc4,skc3) != X542
| singleton(X543,X542) ),
inference(resolution,[status(thm)],[c13,c91]) ).
cnf(c307,plain,
( skc3 != X544
| singleton(X544,skf15(skc4,skc3)) ),
inference(resolution,[status(thm)],[c166,reflexivity]) ).
cnf(c136,plain,
thing(skc3,skf11(skc4,skc3)),
inference(resolution,[status(thm)],[c132,clause6]) ).
cnf(c138,plain,
singleton(skc3,skf11(skc4,skc3)),
inference(resolution,[status(thm)],[c136,clause7]) ).
cnf(c165,plain,
( skc3 != X540
| skf11(skc4,skc3) != X539
| singleton(X540,X539) ),
inference(resolution,[status(thm)],[c13,c138]) ).
cnf(c305,plain,
( skc3 != X541
| singleton(X541,skf11(skc4,skc3)) ),
inference(resolution,[status(thm)],[c165,reflexivity]) ).
cnf(c12,axiom,
( X198 != X197
| X199 != X196
| ~ thing(X198,X199)
| thing(X197,X196) ),
theory(equality) ).
cnf(c160,plain,
( skc3 != X537
| skf11(skc4,skc3) != X536
| thing(X537,X536) ),
inference(resolution,[status(thm)],[c12,c136]) ).
cnf(c303,plain,
( skc3 != X538
| thing(X538,skf11(skc4,skc3)) ),
inference(resolution,[status(thm)],[c160,reflexivity]) ).
cnf(c159,plain,
( skc3 != X534
| skf15(skc4,skc3) != X533
| thing(X534,X533) ),
inference(resolution,[status(thm)],[c12,c88]) ).
cnf(c301,plain,
( skc3 != X535
| thing(X535,skf15(skc4,skc3)) ),
inference(resolution,[status(thm)],[c159,reflexivity]) ).
cnf(c158,plain,
( skc3 != X529
| skf13(skc4,skc3) != X528
| thing(X529,X528) ),
inference(resolution,[status(thm)],[c12,c108]) ).
cnf(c299,plain,
( skc3 != X532
| thing(X532,skf13(skc4,skc3)) ),
inference(resolution,[status(thm)],[c158,reflexivity]) ).
cnf(c11,axiom,
( X187 != X186
| X188 != X185
| ~ entity(X187,X188)
| entity(X186,X185) ),
theory(equality) ).
cnf(c154,plain,
( skc3 != X525
| skf13(skc4,skc3) != X526
| entity(X525,X526) ),
inference(resolution,[status(thm)],[c11,c104]) ).
cnf(c297,plain,
( skc3 != X527
| entity(X527,skf13(skc4,skc3)) ),
inference(resolution,[status(thm)],[c154,reflexivity]) ).
cnf(c153,plain,
( skc3 != X520
| skf15(skc4,skc3) != X521
| entity(X520,X521) ),
inference(resolution,[status(thm)],[c11,c84]) ).
cnf(c295,plain,
( skc3 != X522
| entity(X522,skf15(skc4,skc3)) ),
inference(resolution,[status(thm)],[c153,reflexivity]) ).
cnf(c152,plain,
( skc3 != X517
| skf11(skc4,skc3) != X518
| entity(X517,X518) ),
inference(resolution,[status(thm)],[c11,c132]) ).
cnf(c293,plain,
( skc3 != X519
| entity(X519,skf11(skc4,skc3)) ),
inference(resolution,[status(thm)],[c152,reflexivity]) ).
cnf(c10,axiom,
( X183 != X182
| X184 != X181
| ~ organism(X183,X184)
| organism(X182,X181) ),
theory(equality) ).
cnf(c151,plain,
( skc3 != X512
| skf11(skc4,skc3) != X513
| organism(X512,X513) ),
inference(resolution,[status(thm)],[c10,c127]) ).
cnf(c291,plain,
( skc3 != X514
| organism(X514,skf11(skc4,skc3)) ),
inference(resolution,[status(thm)],[c151,reflexivity]) ).
cnf(c150,plain,
( skc3 != X505
| skf13(skc4,skc3) != X506
| organism(X505,X506) ),
inference(resolution,[status(thm)],[c10,c99]) ).
cnf(c289,plain,
( skc3 != X511
| organism(X511,skf13(skc4,skc3)) ),
inference(resolution,[status(thm)],[c150,reflexivity]) ).
cnf(c149,plain,
( skc3 != X502
| skf15(skc4,skc3) != X503
| organism(X502,X503) ),
inference(resolution,[status(thm)],[c10,c79]) ).
cnf(c287,plain,
( skc3 != X504
| organism(X504,skf15(skc4,skc3)) ),
inference(resolution,[status(thm)],[c149,reflexivity]) ).
cnf(c9,axiom,
( X179 != X178
| X180 != X177
| ~ human_person(X179,X180)
| human_person(X178,X177) ),
theory(equality) ).
cnf(c148,plain,
( skc3 != X496
| skf11(skc4,skc3) != X495
| human_person(X496,X495) ),
inference(resolution,[status(thm)],[c9,c126]) ).
cnf(c285,plain,
( skc3 != X497
| human_person(X497,skf11(skc4,skc3)) ),
inference(resolution,[status(thm)],[c148,reflexivity]) ).
cnf(c147,plain,
( skc3 != X493
| skf15(skc4,skc3) != X492
| human_person(X493,X492) ),
inference(resolution,[status(thm)],[c9,c78]) ).
cnf(c283,plain,
( skc3 != X494
| human_person(X494,skf15(skc4,skc3)) ),
inference(resolution,[status(thm)],[c147,reflexivity]) ).
cnf(c146,plain,
( skc3 != X490
| skf13(skc4,skc3) != X489
| human_person(X490,X489) ),
inference(resolution,[status(thm)],[c9,c98]) ).
cnf(c281,plain,
( skc3 != X491
| human_person(X491,skf13(skc4,skc3)) ),
inference(resolution,[status(thm)],[c146,reflexivity]) ).
cnf(c8,axiom,
( X173 != X172
| X174 != X171
| ~ man(X173,X174)
| man(X172,X171) ),
theory(equality) ).
cnf(c145,plain,
( skc3 != X487
| skf13(skc4,skc3) != X486
| man(X487,X486) ),
inference(resolution,[status(thm)],[c8,c96]) ).
cnf(c279,plain,
( skc3 != X488
| man(X488,skf13(skc4,skc3)) ),
inference(resolution,[status(thm)],[c145,reflexivity]) ).
cnf(c144,plain,
( skc3 != X484
| skf15(skc4,skc3) != X483
| man(X484,X483) ),
inference(resolution,[status(thm)],[c8,c76]) ).
cnf(c277,plain,
( skc3 != X485
| man(X485,skf15(skc4,skc3)) ),
inference(resolution,[status(thm)],[c144,reflexivity]) ).
cnf(c46,axiom,
( X477 != X479
| X482 != X480
| X478 != X481
| ~ with(X477,X482,X478)
| with(X479,X480,X481) ),
theory(equality) ).
cnf(c143,plain,
( skc3 != X475
| skf11(skc4,skc3) != X474
| man(X475,X474) ),
inference(resolution,[status(thm)],[c8,c124]) ).
cnf(c275,plain,
( skc3 != X476
| man(X476,skf11(skc4,skc3)) ),
inference(resolution,[status(thm)],[c143,reflexivity]) ).
cnf(c7,axiom,
( X169 != X168
| X170 != X167
| ~ guy(X169,X170)
| guy(X168,X167) ),
theory(equality) ).
cnf(c142,plain,
( skc3 != X471
| skf13(skc4,skc3) != X472
| guy(X471,X472) ),
inference(resolution,[status(thm)],[c7,c94]) ).
cnf(c273,plain,
( skc3 != X473
| guy(X473,skf13(skc4,skc3)) ),
inference(resolution,[status(thm)],[c142,reflexivity]) ).
cnf(c45,axiom,
( X465 != X467
| X470 != X468
| X466 != X469
| ~ at(X465,X470,X466)
| at(X467,X468,X469) ),
theory(equality) ).
cnf(c141,plain,
( skc3 != X462
| skf15(skc4,skc3) != X463
| guy(X462,X463) ),
inference(resolution,[status(thm)],[c7,c74]) ).
cnf(c271,plain,
( skc3 != X464
| guy(X464,skf15(skc4,skc3)) ),
inference(resolution,[status(thm)],[c141,reflexivity]) ).
cnf(c140,plain,
( skc3 != X453
| skf11(skc4,skc3) != X454
| guy(X453,X454) ),
inference(resolution,[status(thm)],[c7,c123]) ).
cnf(c269,plain,
( skc3 != X461
| guy(X461,skf11(skc4,skc3)) ),
inference(resolution,[status(thm)],[c140,reflexivity]) ).
cnf(c44,axiom,
( X455 != X457
| X460 != X458
| X456 != X459
| ~ agent(X455,X460,X456)
| agent(X457,X458,X459) ),
theory(equality) ).
cnf(c43,axiom,
( X451 != X450
| X452 != X449
| ~ present(X451,X452)
| present(X450,X449) ),
theory(equality) ).
cnf(clause34,axiom,
( ~ furniture(X69,X70)
| instrumentality(X69,X70) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause34) ).
cnf(clause54,negated_conjecture,
table(skc3,skc5),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause54) ).
cnf(clause33,axiom,
( ~ table(X67,X68)
| furniture(X67,X68) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause33) ).
cnf(c50,plain,
furniture(skc3,skc5),
inference(resolution,[status(thm)],[clause33,clause54]) ).
cnf(c51,plain,
instrumentality(skc3,skc5),
inference(resolution,[status(thm)],[c50,clause34]) ).
cnf(clause35,axiom,
( ~ instrumentality(X71,X72)
| artifact(X71,X72) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause35) ).
cnf(c52,plain,
artifact(skc3,skc5),
inference(resolution,[status(thm)],[clause35,c51]) ).
cnf(c40,axiom,
( X440 != X439
| X441 != X438
| ~ artifact(X440,X441)
| artifact(X439,X438) ),
theory(equality) ).
cnf(c263,plain,
( skc3 != X447
| skc5 != X446
| artifact(X447,X446) ),
inference(resolution,[status(thm)],[c40,c52]) ).
cnf(c267,plain,
( skc3 != X448
| artifact(X448,skc5) ),
inference(resolution,[status(thm)],[c263,reflexivity]) ).
cnf(c39,axiom,
( X433 != X432
| X434 != X431
| ~ instrumentality(X433,X434)
| instrumentality(X432,X431) ),
theory(equality) ).
cnf(c260,plain,
( skc3 != X435
| skc5 != X436
| instrumentality(X435,X436) ),
inference(resolution,[status(thm)],[c39,c51]) ).
cnf(c261,plain,
( skc3 != X437
| instrumentality(X437,skc5) ),
inference(resolution,[status(thm)],[c260,reflexivity]) ).
cnf(c38,axiom,
( X423 != X422
| X424 != X421
| ~ furniture(X423,X424)
| furniture(X422,X421) ),
theory(equality) ).
cnf(c255,plain,
( skc3 != X428
| skc5 != X429
| furniture(X428,X429) ),
inference(resolution,[status(thm)],[c38,c50]) ).
cnf(c258,plain,
( skc3 != X430
| furniture(X430,skc5) ),
inference(resolution,[status(thm)],[c255,reflexivity]) ).
cnf(c37,axiom,
( X419 != X418
| X420 != X417
| ~ table(X419,X420)
| table(X418,X417) ),
theory(equality) ).
cnf(c254,plain,
( skc3 != X426
| skc5 != X425
| table(X426,X425) ),
inference(resolution,[status(thm)],[c37,clause54]) ).
cnf(c256,plain,
( skc3 != X427
| table(X427,skc5) ),
inference(resolution,[status(thm)],[c254,reflexivity]) ).
cnf(c36,axiom,
( X415 != X414
| X416 != X413
| ~ nonexistent(X415,X416)
| nonexistent(X414,X413) ),
theory(equality) ).
cnf(c35,axiom,
( X411 != X410
| X412 != X409
| ~ eventuality(X411,X412)
| eventuality(X410,X409) ),
theory(equality) ).
cnf(c34,axiom,
( X407 != X406
| X408 != X405
| ~ event(X407,X408)
| event(X406,X405) ),
theory(equality) ).
cnf(c33,axiom,
( X403 != X402
| X404 != X401
| ~ sit(X403,X404)
| sit(X402,X401) ),
theory(equality) ).
cnf(clause26,axiom,
( ~ object(X53,X54)
| unisex(X53,X54) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause26) ).
cnf(clause36,axiom,
( ~ artifact(X73,X74)
| object(X73,X74) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause36) ).
cnf(c53,plain,
object(skc3,skc5),
inference(resolution,[status(thm)],[clause36,c52]) ).
cnf(c57,plain,
unisex(skc3,skc5),
inference(resolution,[status(thm)],[c53,clause26]) ).
cnf(c32,axiom,
( X393 != X392
| X394 != X391
| ~ unisex(X393,X394)
| unisex(X392,X391) ),
theory(equality) ).
cnf(c249,plain,
( skc3 != X398
| skc5 != X399
| unisex(X398,X399) ),
inference(resolution,[status(thm)],[c32,c57]) ).
cnf(c252,plain,
( skc3 != X400
| unisex(X400,skc5) ),
inference(resolution,[status(thm)],[c249,reflexivity]) ).
cnf(clause24,axiom,
( ~ object(X49,X50)
| nonliving(X49,X50) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause24) ).
cnf(c55,plain,
nonliving(skc3,skc5),
inference(resolution,[status(thm)],[c53,clause24]) ).
cnf(c31,axiom,
( X389 != X388
| X390 != X387
| ~ nonliving(X389,X390)
| nonliving(X388,X387) ),
theory(equality) ).
cnf(c248,plain,
( skc3 != X396
| skc5 != X395
| nonliving(X396,X395) ),
inference(resolution,[status(thm)],[c31,c55]) ).
cnf(c250,plain,
( skc3 != X397
| nonliving(X397,skc5) ),
inference(resolution,[status(thm)],[c248,reflexivity]) ).
cnf(c30,axiom,
( X382 != X381
| X383 != X380
| ~ object(X382,X383)
| object(X381,X380) ),
theory(equality) ).
cnf(c245,plain,
( skc3 != X385
| skc5 != X384
| object(X385,X384) ),
inference(resolution,[status(thm)],[c30,c53]) ).
cnf(c246,plain,
( skc3 != X386
| object(X386,skc5) ),
inference(resolution,[status(thm)],[c245,reflexivity]) ).
cnf(c29,axiom,
( X378 != X377
| X379 != X376
| ~ substance_matter(X378,X379)
| substance_matter(X377,X376) ),
theory(equality) ).
cnf(c28,axiom,
( X374 != X373
| X375 != X372
| ~ food(X374,X375)
| food(X373,X372) ),
theory(equality) ).
cnf(c27,axiom,
( X370 != X369
| X371 != X368
| ~ meat(X370,X371)
| meat(X369,X368) ),
theory(equality) ).
cnf(c26,axiom,
( X366 != X365
| X367 != X364
| ~ burger(X366,X367)
| burger(X365,X364) ),
theory(equality) ).
cnf(clause16,axiom,
( ~ set(X33,X34)
| multiple(X33,X34) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause16) ).
cnf(clause15,axiom,
( ~ group(X31,X32)
| set(X31,X32) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause15) ).
cnf(clause59,negated_conjecture,
( ~ member(skc3,X146,skc4)
| group(skc3,skf8(X147)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause59) ).
cnf(c116,plain,
group(skc3,skf8(X148)),
inference(resolution,[status(thm)],[clause59,c69]) ).
cnf(c118,plain,
set(skc3,skf8(X150)),
inference(resolution,[status(thm)],[c116,clause15]) ).
cnf(c119,plain,
multiple(skc3,skf8(X151)),
inference(resolution,[status(thm)],[c118,clause16]) ).
cnf(c23,axiom,
( X336 != X335
| X337 != X334
| ~ multiple(X336,X337)
| multiple(X335,X334) ),
theory(equality) ).
cnf(c235,plain,
( skc3 != X355
| skf8(X354) != X356
| multiple(X355,X356) ),
inference(resolution,[status(thm)],[c23,c119]) ).
cnf(c243,plain,
( skc3 != X362
| multiple(X362,skf8(X361)) ),
inference(resolution,[status(thm)],[c235,reflexivity]) ).
cnf(c25,axiom,
( X359 != X358
| X360 != X357
| ~ hamburger(X359,X360)
| hamburger(X358,X357) ),
theory(equality) ).
cnf(c24,axiom,
( X348 != X347
| X349 != X346
| ~ three(X348,X349)
| three(X347,X346) ),
theory(equality) ).
cnf(c240,plain,
( skc3 != X351
| skc4 != X352
| three(X351,X352) ),
inference(resolution,[status(thm)],[c24,clause56]) ).
cnf(c241,plain,
( skc3 != X353
| three(X353,skc4) ),
inference(resolution,[status(thm)],[c240,reflexivity]) ).
cnf(c22,axiom,
( X326 != X325
| X327 != X324
| ~ set(X326,X327)
| set(X325,X324) ),
theory(equality) ).
cnf(c229,plain,
( skc3 != X343
| skf8(X341) != X342
| set(X343,X342) ),
inference(resolution,[status(thm)],[c22,c118]) ).
cnf(c238,plain,
( skc3 != X345
| set(X345,skf8(X344)) ),
inference(resolution,[status(thm)],[c229,reflexivity]) ).
cnf(clause55,negated_conjecture,
group(skc3,skc4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause55) ).
cnf(c47,plain,
set(skc3,skc4),
inference(resolution,[status(thm)],[clause15,clause55]) ).
cnf(c48,plain,
multiple(skc3,skc4),
inference(resolution,[status(thm)],[clause16,c47]) ).
cnf(c234,plain,
( skc3 != X338
| skc4 != X339
| multiple(X338,X339) ),
inference(resolution,[status(thm)],[c23,c48]) ).
cnf(c236,plain,
( skc3 != X340
| multiple(X340,skc4) ),
inference(resolution,[status(thm)],[c234,reflexivity]) ).
cnf(c230,plain,
( skc3 != X332
| skc4 != X331
| set(X332,X331) ),
inference(resolution,[status(thm)],[c22,c47]) ).
cnf(c232,plain,
( skc3 != X333
| set(X333,skc4) ),
inference(resolution,[status(thm)],[c230,reflexivity]) ).
cnf(c21,axiom,
( X316 != X315
| X317 != X314
| ~ group(X316,X317)
| group(X315,X314) ),
theory(equality) ).
cnf(c224,plain,
( skc3 != X321
| skf8(X323) != X322
| group(X321,X322) ),
inference(resolution,[status(thm)],[c21,c116]) ).
cnf(c228,plain,
( skc3 != X328
| group(X328,skf8(X329)) ),
inference(resolution,[status(thm)],[c224,reflexivity]) ).
cnf(c225,plain,
( skc3 != X318
| skc4 != X319
| group(X318,X319) ),
inference(resolution,[status(thm)],[c21,clause55]) ).
cnf(c226,plain,
( skc3 != X320
| group(X320,skc4) ),
inference(resolution,[status(thm)],[c225,reflexivity]) ).
cnf(c5,axiom,
( X279 != X278
| X280 != X277
| skf9(X279,X280) = skf9(X278,X277) ),
theory(equality) ).
cnf(c204,plain,
( X294 != X293
| skf9(X294,X295) = skf9(X293,X295) ),
inference(resolution,[status(thm)],[c5,reflexivity]) ).
cnf(c203,plain,
( X285 != X284
| skf9(X285,X285) = skf9(X284,X284) ),
inference(factor,[status(thm)],[c5]) ).
cnf(clause25,axiom,
( ~ object(X51,X52)
| impartial(X51,X52) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause25) ).
cnf(c54,plain,
impartial(skc3,skc5),
inference(resolution,[status(thm)],[c53,clause25]) ).
cnf(c199,plain,
( skc3 != X282
| skc5 != X281
| impartial(X282,X281) ),
inference(resolution,[status(thm)],[c16,c54]) ).
cnf(c205,plain,
( skc3 != X283
| impartial(X283,skc5) ),
inference(resolution,[status(thm)],[c199,reflexivity]) ).
cnf(clause23,axiom,
( ~ object(X47,X48)
| entity(X47,X48) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause23) ).
cnf(c56,plain,
entity(skc3,skc5),
inference(resolution,[status(thm)],[c53,clause23]) ).
cnf(c58,plain,
existent(skc3,skc5),
inference(resolution,[status(thm)],[c56,clause9]) ).
cnf(c195,plain,
( skc3 != X270
| skc5 != X271
| existent(X270,X271) ),
inference(resolution,[status(thm)],[c15,c58]) ).
cnf(c197,plain,
( skc3 != X272
| existent(X272,skc5) ),
inference(resolution,[status(thm)],[c195,reflexivity]) ).
cnf(c2,axiom,
( X244 != X243
| X245 != X242
| skf11(X244,X245) = skf11(X243,X242) ),
theory(equality) ).
cnf(c185,plain,
( X253 != X252
| skf11(X253,X251) = skf11(X252,X251) ),
inference(resolution,[status(thm)],[c2,reflexivity]) ).
cnf(c184,plain,
( X249 != X248
| skf11(X249,X249) = skf11(X248,X248) ),
inference(factor,[status(thm)],[c2]) ).
cnf(c1,axiom,
( X229 != X228
| X230 != X227
| skf13(X229,X230) = skf13(X228,X227) ),
theory(equality) ).
cnf(c180,plain,
( X240 != X239
| skf13(X240,X241) = skf13(X239,X241) ),
inference(resolution,[status(thm)],[c1,reflexivity]) ).
cnf(c179,plain,
( X236 != X237
| skf13(X236,X236) = skf13(X237,X237) ),
inference(factor,[status(thm)],[c1]) ).
cnf(c0,axiom,
( X219 != X218
| X220 != X217
| skf15(X219,X220) = skf15(X218,X217) ),
theory(equality) ).
cnf(c175,plain,
( X232 != X231
| skf15(X232,X233) = skf15(X231,X233) ),
inference(resolution,[status(thm)],[c0,reflexivity]) ).
cnf(c174,plain,
( X225 != X224
| skf15(X225,X225) = skf15(X224,X224) ),
inference(factor,[status(thm)],[c0]) ).
cnf(c59,plain,
specific(skc3,skc5),
inference(resolution,[status(thm)],[c56,clause8]) ).
cnf(c172,plain,
( skc3 != X221
| skc5 != X222
| specific(X221,X222) ),
inference(resolution,[status(thm)],[c14,c59]) ).
cnf(c176,plain,
( skc3 != X223
| specific(X223,skc5) ),
inference(resolution,[status(thm)],[c172,reflexivity]) ).
cnf(c60,plain,
thing(skc3,skc5),
inference(resolution,[status(thm)],[c56,clause6]) ).
cnf(c62,plain,
singleton(skc3,skc5),
inference(resolution,[status(thm)],[c60,clause7]) ).
cnf(c164,plain,
( skc3 != X211
| skc5 != X210
| singleton(X211,X210) ),
inference(resolution,[status(thm)],[c13,c62]) ).
cnf(c168,plain,
( skc3 != X212
| singleton(X212,skc5) ),
inference(resolution,[status(thm)],[c164,reflexivity]) ).
cnf(clause66,negated_conjecture,
( ~ member(skc3,X204,skf8(X205))
| ~ member(skc3,X205,skc4)
| with(skc3,skf9(X204,X203),X204) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause66) ).
cnf(c161,plain,
( skc3 != X201
| skc5 != X200
| thing(X201,X200) ),
inference(resolution,[status(thm)],[c12,c60]) ).
cnf(c162,plain,
( skc3 != X202
| thing(X202,skc5) ),
inference(resolution,[status(thm)],[c161,reflexivity]) ).
cnf(clause65,negated_conjecture,
( ~ member(skc3,X193,skf8(X195))
| ~ member(skc3,X195,skc4)
| at(skc3,skf9(X192,X194),skc5) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause65) ).
cnf(c155,plain,
( skc3 != X189
| skc5 != X190
| entity(X189,X190) ),
inference(resolution,[status(thm)],[c11,c56]) ).
cnf(c156,plain,
( skc3 != X191
| entity(X191,skc5) ),
inference(resolution,[status(thm)],[c155,reflexivity]) ).
cnf(clause64,negated_conjecture,
( ~ member(skc3,X175,skf8(X176))
| ~ member(skc3,X176,skc4)
| agent(skc3,skf9(X175,X176),X176) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause64) ).
cnf(clause38,axiom,
( ~ multiple(X77,X78)
| ~ singleton(X77,X78) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause38) ).
cnf(c139,plain,
~ multiple(skc3,skf11(skc4,skc3)),
inference(resolution,[status(thm)],[c138,clause38]) ).
cnf(clause40,axiom,
( ~ nonexistent(X81,X82)
| ~ existent(X81,X82) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause40) ).
cnf(c137,plain,
~ nonexistent(skc3,skf11(skc4,skc3)),
inference(resolution,[status(thm)],[c134,clause40]) ).
cnf(clause63,negated_conjecture,
( ~ member(skc3,X164,skf8(X166))
| ~ member(skc3,X166,skc4)
| sit(skc3,skf9(X163,X165)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause63) ).
cnf(clause41,axiom,
( ~ nonliving(X83,X84)
| ~ animate(X83,X84) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause41) ).
cnf(c133,plain,
~ nonliving(skc3,skf11(skc4,skc3)),
inference(resolution,[status(thm)],[c128,clause41]) ).
cnf(clause62,negated_conjecture,
( ~ member(skc3,X160,skf8(X162))
| ~ member(skc3,X162,skc4)
| present(skc3,skf9(X159,X161)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause62) ).
cnf(clause61,negated_conjecture,
( ~ member(skc3,X156,skf8(X158))
| ~ member(skc3,X158,skc4)
| event(skc3,skf9(X155,X157)) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause61) ).
cnf(clause60,negated_conjecture,
( ~ member(skc3,X153,skf8(X154))
| ~ member(skc3,X152,skc4)
| hamburger(skc3,X153) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause60) ).
cnf(c115,plain,
~ multiple(skc3,skf13(skc4,skc3)),
inference(resolution,[status(thm)],[c114,clause38]) ).
cnf(c109,plain,
~ nonexistent(skc3,skf13(skc4,skc3)),
inference(resolution,[status(thm)],[c106,clause40]) ).
cnf(clause52,axiom,
( ~ member(X143,X142,X145)
| ~ member(X143,X141,X145)
| ~ member(X143,X144,X145)
| three(X143,X145)
| member(X143,skf16(X142,X141,X144,X145,X143),X145)
| X142 = X144
| X142 = X141
| X141 = X144 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause52) ).
cnf(c105,plain,
~ nonliving(skc3,skf13(skc4,skc3)),
inference(resolution,[status(thm)],[c100,clause41]) ).
cnf(clause51,axiom,
( skf16(X137,X135,X140,X134,X138) != X140
| ~ member(X139,X137,X136)
| ~ member(X139,X135,X136)
| ~ member(X139,X140,X136)
| three(X139,X136)
| X137 = X140
| X137 = X135
| X135 = X140 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause51) ).
cnf(clause50,axiom,
( skf16(X129,X127,X132,X126,X130) != X127
| ~ member(X131,X129,X128)
| ~ member(X131,X127,X128)
| ~ member(X131,X133,X128)
| three(X131,X128)
| X129 = X133
| X129 = X127
| X127 = X133 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause50) ).
cnf(c92,plain,
~ multiple(skc3,skf15(skc4,skc3)),
inference(resolution,[status(thm)],[c91,clause38]) ).
cnf(clause49,axiom,
( skf16(X120,X118,X124,X117,X121) != X120
| ~ member(X122,X120,X119)
| ~ member(X122,X125,X119)
| ~ member(X122,X123,X119)
| three(X122,X119)
| X120 = X123
| X120 = X125
| X125 = X123 ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause49) ).
cnf(c90,plain,
~ nonexistent(skc3,skf15(skc4,skc3)),
inference(resolution,[status(thm)],[c86,clause40]) ).
cnf(clause48,axiom,
( ~ member(X115,X116,X114)
| ~ three(X115,X114)
| X116 = skf11(X114,X115)
| X116 = skf13(X114,X115)
| X116 = skf15(X114,X115) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause48) ).
cnf(c85,plain,
~ nonliving(skc3,skf15(skc4,skc3)),
inference(resolution,[status(thm)],[c80,clause41]) ).
cnf(clause47,axiom,
( skf13(X112,X113) != skf11(X112,X113)
| ~ three(X113,X112) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause47) ).
cnf(clause46,axiom,
( skf15(X110,X111) != skf13(X110,X111)
| ~ three(X111,X110) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause46) ).
cnf(c4,axiom,
( X108 != X107
| skf8(X108) = skf8(X107) ),
theory(equality) ).
cnf(clause45,axiom,
( skf15(X105,X106) != skf11(X105,X106)
| ~ three(X106,X105) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause45) ).
cnf(transitivity,axiom,
( X99 != X100
| X100 != X101
| X99 = X101 ),
theory(equality) ).
cnf(c41,axiom,
( X91 != X90
| ~ actual_world(X91)
| actual_world(X90) ),
theory(equality) ).
cnf(symmetry,axiom,
( X87 != X88
| X88 = X87 ),
theory(equality) ).
cnf(c65,plain,
~ nonexistent(skc3,skc5),
inference(resolution,[status(thm)],[clause40,c58]) ).
cnf(clause39,axiom,
( ~ living(X79,X80)
| ~ nonliving(X79,X80) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause39) ).
cnf(c64,plain,
~ living(skc3,skc5),
inference(resolution,[status(thm)],[clause39,c55]) ).
cnf(c63,plain,
~ multiple(skc3,skc5),
inference(resolution,[status(thm)],[c62,clause38]) ).
cnf(clause37,axiom,
( ~ male(X75,X76)
| ~ unisex(X75,X76) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause37) ).
cnf(c61,plain,
~ male(skc3,skc5),
inference(resolution,[status(thm)],[c57,clause37]) ).
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(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(clause1,axiom,
~ member(X3,X4,X4),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause1) ).
cnf(clause53,negated_conjecture,
actual_world(skc3),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',clause53) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : NLP038-1 : TPTP v8.1.2. Released v2.4.0.
% 0.07/0.13 % Command : pyres-fof.py -tifbsVp -nlargest -HPickGiven5 %s
% 0.13/0.34 % Computer : n023.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:37:23 EDT 2024
% 0.13/0.34 % CPUTime :
% 1.62/1.81 % Version: 1.5
% 1.62/1.81 % SZS status Satisfiable
% 1.62/1.81 % SZS output start Saturation
% See solution above
% 1.65/1.82
% 1.65/1.82 % Initial clauses : 116
% 1.65/1.82 % Processed clauses : 452
% 1.65/1.82 % Factors computed : 97
% 1.65/1.82 % Resolvents computed: 421
% 1.65/1.82 % Tautologies deleted: 3
% 1.65/1.82 % Forward subsumed : 179
% 1.65/1.82 % Backward subsumed : 48
% 1.65/1.82 % -------- CPU Time ---------
% 1.65/1.82 % User time : 1.464 s
% 1.65/1.82 % System time : 0.012 s
% 1.65/1.82 % Total time : 1.476 s
%------------------------------------------------------------------------------